15 |
15 |
16 definition SEQ_set where |
16 definition SEQ_set where |
17 "SEQ_set A n \<equiv> {RSEQ r1 r2 | r1 r2. r1 \<in> A \<and> r2 \<in> A \<and> rsize r1 + rsize r2 \<le> n}" |
17 "SEQ_set A n \<equiv> {RSEQ r1 r2 | r1 r2. r1 \<in> A \<and> r2 \<in> A \<and> rsize r1 + rsize r2 \<le> n}" |
18 |
18 |
19 definition SEQ_set_cartesian where |
19 definition SEQ_set_cartesian where |
20 "SEQ_set_cartesian A n = {RSEQ r1 r2 | r1 r2. r1 \<in> A \<and> r2 \<in> A}" |
20 "SEQ_set_cartesian A = {RSEQ r1 r2 | r1 r2. r1 \<in> A \<and> r2 \<in> A}" |
21 |
21 |
22 definition ALT_set where |
22 definition ALT_set where |
23 "ALT_set A n \<equiv> {RALTS rs | rs. set rs \<subseteq> A \<and> sum_list (map rsize rs) \<le> n}" |
23 "ALT_set A n \<equiv> {RALTS rs | rs. set rs \<subseteq> A \<and> sum_list (map rsize rs) \<le> n}" |
24 |
24 |
|
25 definition ALTs_set |
|
26 where |
|
27 "ALTs_set A n \<equiv> {RALTS rs | rs. \<forall>r \<in> set rs. r \<in> A \<and> sum_list (map rsize rs) \<le> n}" |
|
28 |
|
29 |
|
30 |
|
31 lemma alts_set_2defs: |
|
32 shows "ALT_set A n = ALTs_set A n" |
|
33 apply(subgoal_tac "ALT_set A n \<subseteq> ALTs_set A n") |
|
34 apply(subgoal_tac "ALTs_set A n \<subseteq> ALT_set A n") |
|
35 apply auto[1] |
|
36 prefer 2 |
|
37 using ALT_set_def ALTs_set_def apply fastforce |
|
38 apply(subgoal_tac "\<forall>r \<in> ALTs_set A n. r \<in> ALT_set A n") |
|
39 apply blast |
|
40 apply(rule ballI) |
|
41 apply(subgoal_tac "\<exists>rs. r = RALTS rs \<and> sum_list (map rsize rs) \<le> n") |
|
42 prefer 2 |
|
43 using ALTs_set_def apply fastforce |
|
44 apply(erule exE) |
|
45 apply(subgoal_tac "set rs \<subseteq> A") |
|
46 prefer 2 |
|
47 apply (simp add: ALTs_set_def subsetI) |
|
48 using ALT_set_def by blast |
|
49 |
|
50 |
25 |
51 |
26 definition |
52 definition |
27 "sizeNregex N \<equiv> {r. rsize r \<le> N}" |
53 "sizeNregex N \<equiv> {r. rsize r \<le> N}" |
|
54 |
|
55 |
|
56 |
|
57 lemma sizenregex_induct1: |
|
58 "sizeNregex (Suc n) = (({RZERO, RONE} \<union> {RCHAR c| c. True}) |
|
59 \<union> (RSTAR ` sizeNregex n) \<union> |
|
60 (SEQ_set (sizeNregex n) n) |
|
61 \<union> (ALTs_set (sizeNregex n) n))" |
|
62 apply(auto) |
|
63 apply(case_tac x) |
|
64 apply(auto simp add: SEQ_set_def) |
|
65 using sizeNregex_def apply force |
|
66 using sizeNregex_def apply auto[1] |
|
67 apply (simp add: sizeNregex_def) |
|
68 apply (simp add: sizeNregex_def) |
|
69 apply (simp add: ALTs_set_def) |
|
70 apply (metis imageI list.set_map member_le_sum_list order_trans) |
|
71 apply (simp add: sizeNregex_def) |
|
72 apply (simp add: sizeNregex_def) |
|
73 apply (simp add: sizeNregex_def) |
|
74 using sizeNregex_def apply force |
|
75 apply (simp add: sizeNregex_def) |
|
76 apply (simp add: sizeNregex_def) |
|
77 apply (simp add: ALTs_set_def) |
|
78 apply(simp add: sizeNregex_def) |
|
79 apply(auto) |
|
80 using ex_in_conv by fastforce |
|
81 |
|
82 lemma sizeN_inclusion: |
|
83 shows "sizeNregex n \<subseteq> sizeNregex (Suc n)" |
|
84 by (simp add: Collect_mono sizeNregex_def) |
|
85 |
|
86 lemma ralts_nil_in_altset: |
|
87 shows " RALTS [] \<in> ALT_set (sizeNregex n) n " |
|
88 using ALT_set_def by auto |
|
89 |
28 |
90 |
29 lemma sizenregex_induct: |
91 lemma sizenregex_induct: |
30 shows "sizeNregex (Suc n) = sizeNregex n \<union> {RZERO, RONE, RALTS []} \<union> {RCHAR c| c. True} \<union> |
92 shows "sizeNregex (Suc n) = sizeNregex n \<union> {RZERO, RONE, RALTS []} \<union> {RCHAR c| c. True} \<union> |
31 SEQ_set ( sizeNregex n) n \<union> ALT_set (sizeNregex n) n \<union> (RSTAR ` (sizeNregex n))" |
93 SEQ_set ( sizeNregex n) n \<union> ALT_set (sizeNregex n) n \<union> (RSTAR ` (sizeNregex n))" |
32 sorry |
94 apply(subgoal_tac "sizeNregex (Suc n) = {RZERO, RONE, RALTS []} \<union> {RCHAR c| c. True} \<union> |
|
95 SEQ_set ( sizeNregex n) n \<union> ALT_set (sizeNregex n) n \<union> (RSTAR ` (sizeNregex n))") |
|
96 using sizeN_inclusion apply blast |
|
97 apply(subgoal_tac " {RZERO, RONE, RALTS []} \<union> {RCHAR c |c. True} \<union> SEQ_set (sizeNregex n) n \<union> |
|
98 ALT_set (sizeNregex n) n \<union> |
|
99 RSTAR ` sizeNregex n = (({RZERO, RONE} \<union> {RCHAR c| c. True}) |
|
100 \<union> (RSTAR ` sizeNregex n) \<union> |
|
101 (SEQ_set (sizeNregex n) n) |
|
102 \<union> (ALTs_set (sizeNregex n) n))") |
|
103 using sizenregex_induct1 apply presburger |
|
104 apply(subgoal_tac "{RZERO, RONE} \<union> {RCHAR c |c. True} \<union> SEQ_set (sizeNregex n) n \<union> |
|
105 ALT_set (sizeNregex n) n \<union> |
|
106 RSTAR ` sizeNregex n = |
|
107 {RZERO, RONE} \<union> {RCHAR c |c. True} \<union> RSTAR ` sizeNregex n \<union> SEQ_set (sizeNregex n) n \<union> |
|
108 ALTs_set (sizeNregex n) n ") |
|
109 prefer 2 |
|
110 using alts_set_2defs apply auto[1] |
|
111 apply(subgoal_tac " {RZERO, RONE, RALTS []} \<union> {RCHAR c |c. True} \<union> SEQ_set (sizeNregex n) n \<union> |
|
112 ALT_set (sizeNregex n) n \<union> |
|
113 RSTAR ` sizeNregex n = |
|
114 {RZERO, RONE} \<union> {RCHAR c |c. True} \<union> SEQ_set (sizeNregex n) n \<union> |
|
115 (insert (RALTS []) (ALT_set (sizeNregex n) n)) \<union> |
|
116 RSTAR ` sizeNregex n") |
|
117 prefer 2 |
|
118 apply fastforce |
|
119 by (simp add: insert_absorb ralts_nil_in_altset) |
|
120 |
|
121 |
|
122 |
|
123 lemma s4: |
|
124 "SEQ_set A n \<subseteq> SEQ_set_cartesian A" |
|
125 using SEQ_set_cartesian_def SEQ_set_def by fastforce |
|
126 |
|
127 lemma s5: |
|
128 "finite A \<Longrightarrow> finite (SEQ_set_cartesian A)" |
|
129 apply(subgoal_tac "SEQ_set_cartesian A = (\<lambda>(x1, x2). RSEQ x1 x2) ` (A \<times> A)") |
|
130 apply simp |
|
131 unfolding SEQ_set_cartesian_def |
|
132 apply(auto) |
|
133 done |
|
134 |
|
135 thm size_list_def |
|
136 |
|
137 definition ALTs_set_length |
|
138 where |
|
139 "ALTs_set_length A n l \<equiv> {RALTS rs | rs. \<forall>r \<in> set rs. r \<in> A |
|
140 \<and> sum_list (map rsize rs) \<le> n |
|
141 \<and> length rs \<le> l}" |
|
142 |
|
143 |
|
144 definition ALTs_set_length2 |
|
145 where |
|
146 "ALTs_set_length2 A l \<equiv> {RALTS rs | rs. \<forall>r \<in> set rs. r \<in> A \<and> length rs \<le> l}" |
|
147 |
|
148 definition set_length2 |
|
149 where |
|
150 "set_length2 A l \<equiv> {rs. \<forall>r \<in> set rs. r \<in> A \<and> length rs \<le> l}" |
|
151 |
|
152 |
|
153 lemma r000: |
|
154 shows "ALTs_set_length A n l \<subseteq> ALTs_set_length2 A l" |
|
155 apply(auto simp add: ALTs_set_length2_def ALTs_set_length_def) |
|
156 done |
|
157 |
|
158 |
|
159 lemma r02: |
|
160 shows "set_length2 A 0 \<subseteq> {[]}" |
|
161 apply(auto simp add: set_length2_def) |
|
162 apply(case_tac x) |
|
163 apply(auto) |
|
164 done |
|
165 |
|
166 lemma r03: |
|
167 shows "set_length2 A (Suc n) \<subseteq> |
|
168 {[]} \<union> (\<lambda>(h, t). h # t) ` (A \<times> (set_length2 A n))" |
|
169 apply(auto simp add: set_length2_def) |
|
170 apply(case_tac x) |
|
171 apply(auto) |
|
172 done |
|
173 |
|
174 lemma r1: |
|
175 assumes "finite A" |
|
176 shows "finite (set_length2 A n)" |
|
177 using assms |
|
178 apply(induct n) |
|
179 apply(rule finite_subset) |
|
180 apply(rule r02) |
|
181 apply(simp) |
|
182 apply(rule finite_subset) |
|
183 apply(rule r03) |
|
184 apply(simp) |
|
185 done |
|
186 |
|
187 lemma size_sum_more_than_len: |
|
188 shows "sum_list (map rsize rs) \<ge> length rs" |
|
189 apply(induct rs) |
|
190 apply simp |
|
191 apply simp |
|
192 apply(subgoal_tac "rsize a \<ge> 1") |
|
193 apply linarith |
|
194 using size_geq1 by auto |
|
195 |
|
196 |
|
197 lemma sum_list_len: |
|
198 shows " sum_list (map rsize rs) \<le> n \<Longrightarrow> length rs \<le> n" |
|
199 by (meson order.trans size_sum_more_than_len) |
|
200 |
|
201 |
|
202 |
|
203 |
|
204 lemma t2: |
|
205 shows "ALTs_set A n \<subseteq> ALTs_set_length A n n" |
|
206 unfolding ALTs_set_length_def ALTs_set_def |
|
207 apply(auto) |
|
208 using sum_list_len by blast |
|
209 |
|
210 |
|
211 thm ALTs_set_def |
|
212 |
|
213 lemma s8_aux: |
|
214 assumes "finite A" |
|
215 shows "finite (ALTs_set_length A n n)" |
|
216 proof - |
|
217 have "finite A" by fact |
|
218 then have "finite (set_length2 A n)" |
|
219 by (simp add: r1) |
|
220 moreover have "(RALTS ` (set_length2 A n)) = ALTs_set_length2 A n" |
|
221 unfolding ALTs_set_length2_def set_length2_def |
|
222 by (auto) |
|
223 ultimately have "finite (ALTs_set_length2 A n)" |
|
224 by (metis finite_imageI) |
|
225 then show ?thesis |
|
226 by (metis infinite_super r000) |
|
227 qed |
|
228 |
|
229 lemma s1: |
|
230 shows "{r::rrexp . rsize r = 1} = ({RZERO, RONE, RALTS []} \<union> {RCHAR c| c. True})" |
|
231 apply(auto) |
|
232 apply(case_tac x) |
|
233 apply(simp_all) |
|
234 apply (metis One_nat_def Suc_n_not_le_n size_geq1) |
|
235 apply (metis One_nat_def Suc_n_not_le_n ex_in_conv set_empty2 size_geq1) |
|
236 by (metis not_one_le_zero size_geq1) |
|
237 |
|
238 |
|
239 |
|
240 lemma char_finite: |
|
241 shows "finite {RCHAR c |c. True}" |
|
242 apply simp |
|
243 apply(subgoal_tac "finite (RCHAR ` (UNIV::char set))") |
|
244 prefer 2 |
|
245 apply simp |
|
246 by (simp add: full_SetCompr_eq) |
|
247 |
|
248 |
|
249 lemma finite_size_n: |
|
250 shows |
|
251 "finite (sizeNregex n)" |
|
252 apply(induct n) |
|
253 apply(simp add: sizeNregex_def) |
|
254 apply (metis (mono_tags, lifting) not_finite_existsD not_one_le_zero size_geq1) |
|
255 apply(subst sizenregex_induct1) |
|
256 apply(simp only: finite_Un) |
|
257 apply(rule conjI)+ |
|
258 apply(simp) |
|
259 using char_finite apply blast |
|
260 apply(simp) |
|
261 apply(rule finite_subset) |
|
262 apply(rule s4) |
|
263 apply(rule s5) |
|
264 apply(simp) |
|
265 apply(rule finite_subset) |
|
266 apply(rule t2) |
|
267 apply(rule s8_aux) |
|
268 apply(simp) |
|
269 done |
|
270 |
33 |
271 |
34 |
272 |
35 lemma chars_finite: |
273 lemma chars_finite: |
36 shows "finite (RCHAR ` (UNIV::(char set)))" |
274 shows "finite (RCHAR ` (UNIV::(char set)))" |
37 apply(simp) |
275 apply(simp) |
51 apply (simp add: SEQ_set_def) |
289 apply (simp add: SEQ_set_def) |
52 apply (simp add: ALT_set_def) |
290 apply (simp add: ALT_set_def) |
53 apply(simp add: full_SetCompr_eq) |
291 apply(simp add: full_SetCompr_eq) |
54 using non_zero_size not_less_eq_eq sizeNregex_def by fastforce |
292 using non_zero_size not_less_eq_eq sizeNregex_def by fastforce |
55 |
293 |
56 lemma seq_included_in_cart: |
|
57 shows "SEQ_set A n \<subseteq> SEQ_set_cartesian A n" |
|
58 using SEQ_set_cartesian_def SEQ_set_def by fastforce |
|
59 |
|
60 lemma finite_seq: |
|
61 shows " finite (sizeNregex n) \<Longrightarrow> finite (SEQ_set (sizeNregex n) n)" |
|
62 apply(rule finite_subset) |
|
63 sorry |
|
64 |
|
65 |
|
66 lemma finite_size_n: |
|
67 shows "finite (sizeNregex n)" |
|
68 apply(induct n) |
|
69 apply (metis Collect_empty_eq finite.emptyI non_zero_size not_less_eq_eq sizeNregex_def) |
|
70 apply(subst sizenregex_induct) |
|
71 apply(subst finite_Un)+ |
|
72 apply(rule conjI)+ |
|
73 apply simp |
|
74 apply simp |
|
75 apply (simp add: full_SetCompr_eq) |
|
76 |
|
77 sorry |
|
78 |
294 |
79 lemma three_easy_cases0: shows |
295 lemma three_easy_cases0: shows |
80 "rsize (rders_simp RZERO s) \<le> Suc 0" |
296 "rsize (rders_simp RZERO s) \<le> Suc 0" |
81 sorry |
297 apply(induct s) |
|
298 apply simp |
|
299 apply simp |
|
300 done |
82 |
301 |
83 |
302 |
84 lemma three_easy_cases1: shows |
303 lemma three_easy_cases1: shows |
85 "rsize (rders_simp RONE s) \<le> Suc 0" |
304 "rsize (rders_simp RONE s) \<le> Suc 0" |
86 sorry |
305 apply(induct s) |
|
306 apply simp |
|
307 apply simp |
|
308 using three_easy_cases0 by auto |
|
309 |
87 |
310 |
88 lemma three_easy_casesC: shows |
311 lemma three_easy_casesC: shows |
89 "rsize (rders_simp (RCHAR c) s) \<le> Suc 0" |
312 "rsize (rders_simp (RCHAR c) s) \<le> Suc 0" |
90 |
313 apply(induct s) |
91 sorry |
314 apply simp |
|
315 apply simp |
|
316 apply(case_tac " a = c") |
|
317 using three_easy_cases1 apply blast |
|
318 apply simp |
|
319 using three_easy_cases0 by force |
|
320 |
92 |
321 |
93 |
322 |
94 |
323 |
95 |
324 |
96 end |
325 end |