15 definition RALT_set where |
15 definition RALT_set where |
16 "RALT_set A n \<equiv> {RALTS rs | rs. set rs \<subseteq> A \<and> rsizes rs \<le> n}" |
16 "RALT_set A n \<equiv> {RALTS rs | rs. set rs \<subseteq> A \<and> rsizes rs \<le> n}" |
17 |
17 |
18 definition RALTs_set where |
18 definition RALTs_set where |
19 "RALTs_set A n \<equiv> {RALTS rs | rs. \<forall>r \<in> set rs. r \<in> A \<and> rsizes rs \<le> n}" |
19 "RALTs_set A n \<equiv> {RALTS rs | rs. \<forall>r \<in> set rs. r \<in> A \<and> rsizes rs \<le> n}" |
|
20 |
|
21 definition RNTIMES_set where |
|
22 "RNTIMES_set A n \<equiv> {RNTIMES r m | m r. r \<in> A \<and> rsize r + m \<le> n}" |
|
23 |
20 |
24 |
21 definition |
25 definition |
22 "sizeNregex N \<equiv> {r. rsize r \<le> N}" |
26 "sizeNregex N \<equiv> {r. rsize r \<le> N}" |
23 |
27 |
24 |
28 |
25 lemma sizenregex_induct1: |
29 lemma sizenregex_induct1: |
26 "sizeNregex (Suc n) = (({RZERO, RONE} \<union> {RCHAR c| c. True}) |
30 "sizeNregex (Suc n) = (({RZERO, RONE} \<union> {RCHAR c| c. True}) |
27 \<union> (RSTAR ` sizeNregex n) |
31 \<union> (RSTAR ` sizeNregex n) |
28 \<union> (RSEQ_set (sizeNregex n) n) |
32 \<union> (RSEQ_set (sizeNregex n) n) |
29 \<union> (RALTs_set (sizeNregex n) n))" |
33 \<union> (RALTs_set (sizeNregex n) n)) |
|
34 \<union> (RNTIMES_set (sizeNregex n) n)" |
30 apply(auto) |
35 apply(auto) |
31 apply(case_tac x) |
36 apply(case_tac x) |
32 apply(auto simp add: RSEQ_set_def) |
37 apply(auto simp add: RSEQ_set_def) |
33 using sizeNregex_def apply force |
38 using sizeNregex_def apply force |
34 using sizeNregex_def apply auto[1] |
39 using sizeNregex_def apply auto[1] |
35 apply (simp add: sizeNregex_def) |
40 apply (simp add: sizeNregex_def) |
36 apply (simp add: sizeNregex_def) |
41 apply (simp add: sizeNregex_def) |
37 apply (simp add: RALTs_set_def) |
42 apply (simp add: RALTs_set_def) |
38 apply (metis imageI list.set_map member_le_sum_list order_trans) |
43 apply (metis imageI list.set_map member_le_sum_list order_trans) |
39 apply (simp add: sizeNregex_def) |
44 apply (simp add: sizeNregex_def) |
40 apply (simp add: sizeNregex_def) |
45 apply (simp add: sizeNregex_def) |
|
46 apply (simp add: RNTIMES_set_def) |
41 apply (simp add: sizeNregex_def) |
47 apply (simp add: sizeNregex_def) |
42 using sizeNregex_def apply force |
48 using sizeNregex_def apply force |
43 apply (simp add: sizeNregex_def) |
49 apply (simp add: sizeNregex_def) |
44 apply (simp add: sizeNregex_def) |
50 apply (simp add: sizeNregex_def) |
45 apply (simp add: RALTs_set_def) |
51 apply (simp add: sizeNregex_def) |
|
52 apply (simp add: RALTs_set_def) |
46 apply(simp add: sizeNregex_def) |
53 apply(simp add: sizeNregex_def) |
47 apply(auto) |
54 apply(auto) |
48 using ex_in_conv by fastforce |
55 using ex_in_conv apply fastforce |
|
56 apply (simp add: RNTIMES_set_def) |
|
57 apply(simp add: sizeNregex_def) |
|
58 by force |
|
59 |
49 |
60 |
50 lemma s4: |
61 lemma s4: |
51 "RSEQ_set A n \<subseteq> RSEQ_set_cartesian A" |
62 "RSEQ_set A n \<subseteq> RSEQ_set_cartesian A" |
52 using RSEQ_set_cartesian_def RSEQ_set_def by fastforce |
63 using RSEQ_set_cartesian_def RSEQ_set_def by fastforce |
53 |
64 |
153 apply(subgoal_tac "finite (RCHAR ` (UNIV::char set))") |
164 apply(subgoal_tac "finite (RCHAR ` (UNIV::char set))") |
154 prefer 2 |
165 prefer 2 |
155 apply simp |
166 apply simp |
156 by (simp add: full_SetCompr_eq) |
167 by (simp add: full_SetCompr_eq) |
157 |
168 |
|
169 thm RNTIMES_set_def |
|
170 |
|
171 lemma s9_aux0: |
|
172 shows "RNTIMES_set (insert r A) n \<subseteq> RNTIMES_set A n \<union> (\<Union> i \<in> {..n}. {RNTIMES r i})" |
|
173 apply(auto simp add: RNTIMES_set_def) |
|
174 done |
|
175 |
|
176 lemma s9_aux: |
|
177 assumes "finite A" |
|
178 shows "finite (RNTIMES_set A n)" |
|
179 using assms |
|
180 apply(induct A arbitrary: n) |
|
181 apply(auto simp add: RNTIMES_set_def)[1] |
|
182 apply(subgoal_tac "finite (RNTIMES_set F n \<union> (\<Union> i \<in> {..n}. {RNTIMES x i}))") |
|
183 apply (metis finite_subset s9_aux0) |
|
184 by blast |
158 |
185 |
159 lemma finite_size_n: |
186 lemma finite_size_n: |
160 shows "finite (sizeNregex n)" |
187 shows "finite (sizeNregex n)" |
161 apply(induct n) |
188 apply(induct n) |
162 apply(simp add: sizeNregex_def) |
189 apply(simp add: sizeNregex_def) |