|
1 |
|
2 theory ClosedForms |
|
3 imports "Lexer" "PDerivs" |
|
4 begin |
|
5 |
|
6 |
|
7 datatype rrexp = |
|
8 RZERO |
|
9 | RONE |
|
10 | RCHAR char |
|
11 | RSEQ rrexp rrexp |
|
12 | RALTS "rrexp list" |
|
13 | RSTAR rrexp |
|
14 |
|
15 abbreviation |
|
16 "RALT r1 r2 \<equiv> RALTS [r1, r2]" |
|
17 |
|
18 |
|
19 |
|
20 fun |
|
21 rnullable :: "rrexp \<Rightarrow> bool" |
|
22 where |
|
23 "rnullable (RZERO) = False" |
|
24 | "rnullable (RONE ) = True" |
|
25 | "rnullable (RCHAR c) = False" |
|
26 | "rnullable (RALTS rs) = (\<exists>r \<in> set rs. rnullable r)" |
|
27 | "rnullable (RSEQ r1 r2) = (rnullable r1 \<and> rnullable r2)" |
|
28 | "rnullable (RSTAR r) = True" |
|
29 |
|
30 |
|
31 fun |
|
32 rder :: "char \<Rightarrow> rrexp \<Rightarrow> rrexp" |
|
33 where |
|
34 "rder c (RZERO) = RZERO" |
|
35 | "rder c (RONE) = RZERO" |
|
36 | "rder c (RCHAR d) = (if c = d then RONE else RZERO)" |
|
37 | "rder c (RALTS rs) = RALTS (map (rder c) rs)" |
|
38 | "rder c (RSEQ r1 r2) = |
|
39 (if rnullable r1 |
|
40 then RALT (RSEQ (rder c r1) r2) (rder c r2) |
|
41 else RSEQ (rder c r1) r2)" |
|
42 | "rder c (RSTAR r) = RSEQ (rder c r) (RSTAR r)" |
|
43 |
|
44 |
|
45 fun |
|
46 rders :: "rrexp \<Rightarrow> string \<Rightarrow> rrexp" |
|
47 where |
|
48 "rders r [] = r" |
|
49 | "rders r (c#s) = rders (rder c r) s" |
|
50 |
|
51 fun rdistinct :: "'a list \<Rightarrow>'a set \<Rightarrow> 'a list" |
|
52 where |
|
53 "rdistinct [] acc = []" |
|
54 | "rdistinct (x#xs) acc = |
|
55 (if x \<in> acc then rdistinct xs acc |
|
56 else x # (rdistinct xs ({x} \<union> acc)))" |
|
57 |
|
58 |
|
59 |
|
60 |
|
61 |
|
62 fun rflts :: "rrexp list \<Rightarrow> rrexp list" |
|
63 where |
|
64 "rflts [] = []" |
|
65 | "rflts (RZERO # rs) = rflts rs" |
|
66 | "rflts ((RALTS rs1) # rs) = rs1 @ rflts rs" |
|
67 | "rflts (r1 # rs) = r1 # rflts rs" |
|
68 |
|
69 |
|
70 fun rsimp_ALTs :: " rrexp list \<Rightarrow> rrexp" |
|
71 where |
|
72 "rsimp_ALTs [] = RZERO" |
|
73 | "rsimp_ALTs [r] = r" |
|
74 | "rsimp_ALTs rs = RALTS rs" |
|
75 |
|
76 fun rsimp_SEQ :: " rrexp \<Rightarrow> rrexp \<Rightarrow> rrexp" |
|
77 where |
|
78 "rsimp_SEQ RZERO _ = RZERO" |
|
79 | "rsimp_SEQ _ RZERO = RZERO" |
|
80 | "rsimp_SEQ RONE r2 = r2" |
|
81 | "rsimp_SEQ r1 r2 = RSEQ r1 r2" |
|
82 |
|
83 |
|
84 fun rsimp :: "rrexp \<Rightarrow> rrexp" |
|
85 where |
|
86 "rsimp (RSEQ r1 r2) = rsimp_SEQ (rsimp r1) (rsimp r2)" |
|
87 | "rsimp (RALTS rs) = rsimp_ALTs (rdistinct (rflts (map rsimp rs)) {}) " |
|
88 | "rsimp r = r" |
|
89 |
|
90 |
|
91 fun |
|
92 rders_simp :: "rrexp \<Rightarrow> string \<Rightarrow> rrexp" |
|
93 where |
|
94 "rders_simp r [] = r" |
|
95 | "rders_simp r (c#s) = rders_simp (rsimp (rder c r)) s" |
|
96 |
|
97 fun rsize :: "rrexp \<Rightarrow> nat" where |
|
98 "rsize RZERO = 1" |
|
99 | "rsize (RONE) = 1" |
|
100 | "rsize (RCHAR c) = 1" |
|
101 | "rsize (RALTS rs) = Suc (sum_list (map rsize rs))" |
|
102 | "rsize (RSEQ r1 r2) = Suc (rsize r1 + rsize r2)" |
|
103 | "rsize (RSTAR r) = Suc (rsize r)" |
|
104 |
|
105 |
|
106 fun rlist_size :: "rrexp list \<Rightarrow> nat" where |
|
107 "rlist_size (r # rs) = rsize r + rlist_size rs" |
|
108 | "rlist_size [] = 0" |
|
109 |
|
110 fun vsuf :: "char list \<Rightarrow> rrexp \<Rightarrow> char list list" where |
|
111 "vsuf [] _ = []" |
|
112 |"vsuf (c#cs) r1 = (if (rnullable r1) then (vsuf cs (rder c r1)) @ [c # cs] |
|
113 else (vsuf cs (rder c r1)) |
|
114 ) " |
|
115 |
|
116 lemma seq_closed_form: shows |
|
117 "rsimp (rders_simp (RSEQ r1 r2) s) = |
|
118 rsimp ( RALTS ( (RSEQ (rders_simp r1 s) r2) # |
|
119 (map (rders r2) (vsuf s r1)) |
|
120 ) |
|
121 )" |
|
122 apply(induct s) |
|
123 apply simp |
|
124 sorry |
|
125 |
|
126 |
|
127 fun star_update :: "char \<Rightarrow> rrexp \<Rightarrow> char list list \<Rightarrow> char list list" where |
|
128 "star_update c r [] = []" |
|
129 |"star_update c r (s # Ss) = (if (rnullable (rders_simp r s)) |
|
130 then (s@[c]) # [c] # (star_update c r Ss) |
|
131 else (s@[c]) # (star_update c r Ss) )" |
|
132 |
|
133 fun star_updates :: "char list \<Rightarrow> rrexp \<Rightarrow> char list list \<Rightarrow> char list list" |
|
134 where |
|
135 "star_updates [] r Ss = Ss" |
|
136 | "star_updates (c # cs) r Ss = star_updates cs r (star_update c r Ss)" |
|
137 |
|
138 |
|
139 lemma star_closed_form: |
|
140 shows "rders_simp (RSTAR r0) (c#s) = |
|
141 rsimp ( RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) (star_updates s r [[c]]) ) ))" |
|
142 apply(induct s) |
|
143 apply simp |
|
144 sorry |
|
145 |
|
146 |
|
147 lemma star_closed_form_bounded_by_rdistinct_list_estimate: |
|
148 shows "rsize (rsimp ( RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) |
|
149 (star_updates s r [[c]]) ) ))) \<le> |
|
150 Suc (sum_list (map rsize (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) |
|
151 (star_updates s r [[c]]) ) {}) ) )" |
|
152 |
|
153 sorry |
|
154 |
|
155 lemma distinct_list_rexp_up_to_certain_size_bouded_by_set_enumerating_up_to_that_size: |
|
156 shows "\<forall>r\<in> set rs. (rsize r ) \<le> N \<Longrightarrow> sum_list (map rsize (rdistinct rs {})) \<le> |
|
157 (card (rexp_enum N))* N" |
|
158 sorry |
|
159 |
|
160 |
|
161 lemma ind_hypo_on_ders_leads_to_stars_bounded: |
|
162 shows "\<forall>s. rsize (rders_simp r0 s) \<le> N \<Longrightarrow> |
|
163 (sum_list (map rsize (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) |
|
164 (star_updates s r [[c]]) ) {}) ) ) \<le> |
|
165 (card (rexp_enum (Suc (N + rsize (RSTAR r0))))) * (Suc (N + rsize (RSTAR r0))) |
|
166 " |
|
167 sorry |
|
168 |
|
169 lemma r0_bounded_star_bounded: |
|
170 shows "\<forall>s. rsize (rders_simp r0 s) \<le> N \<Longrightarrow> |
|
171 \<forall>s. rsize (rders_simp (RSTAR r0) s) \<le> |
|
172 (card (rexp_enum (Suc (N + rsize (RSTAR r0))))) * (Suc (N + rsize (RSTAR r0)))" |
|
173 |
|
174 sorry |
|
175 |
|
176 |
|
177 (*some basic facts about rsimp*) |
|
178 lemma hand_made_def_rlist_size: |
|
179 shows "rlist_size rs = sum_list (map rsize rs)" |
|
180 proof (induct rs) |
|
181 case Nil show ?case by simp |
|
182 next |
|
183 case (Cons a rs) thus ?case |
|
184 by simp |
|
185 qed |
|
186 |
|
187 lemma rder_rsimp_ALTs_commute: |
|
188 shows " (rder x (rsimp_ALTs rs)) = rsimp_ALTs (map (rder x) rs)" |
|
189 apply(induct rs) |
|
190 apply simp |
|
191 apply(case_tac rs) |
|
192 apply simp |
|
193 apply auto |
|
194 done |
|
195 |
|
196 |
|
197 lemma rsimp_aalts_smaller: |
|
198 shows "rsize (rsimp_ALTs rs) \<le> rsize (RALTS rs)" |
|
199 apply(induct rs) |
|
200 apply simp |
|
201 apply simp |
|
202 apply(case_tac "rs = []") |
|
203 apply simp |
|
204 apply(subgoal_tac "\<exists>rsp ap. rs = ap # rsp") |
|
205 apply(erule exE)+ |
|
206 apply simp |
|
207 apply simp |
|
208 by(meson neq_Nil_conv) |
|
209 |
|
210 |
|
211 |
|
212 |
|
213 |
|
214 lemma rSEQ_mono: |
|
215 shows "rsize (rsimp_SEQ r1 r2) \<le>rsize ( RSEQ r1 r2)" |
|
216 apply auto |
|
217 apply(induct r1) |
|
218 apply auto |
|
219 apply(case_tac "r2") |
|
220 apply simp_all |
|
221 apply(case_tac r2) |
|
222 apply simp_all |
|
223 apply(case_tac r2) |
|
224 apply simp_all |
|
225 apply(case_tac r2) |
|
226 apply simp_all |
|
227 apply(case_tac r2) |
|
228 apply simp_all |
|
229 done |
|
230 |
|
231 lemma ralts_cap_mono: |
|
232 shows "rsize (RALTS rs) \<le> Suc ( sum_list (map rsize rs)) " |
|
233 by simp |
|
234 |
|
235 lemma rflts_def_idiot: |
|
236 shows "\<lbrakk> a \<noteq> RZERO; \<nexists>rs1. a = RALTS rs1\<rbrakk> |
|
237 \<Longrightarrow> rflts (a # rs) = a # rflts rs" |
|
238 apply(case_tac a) |
|
239 apply simp_all |
|
240 done |
|
241 |
|
242 |
|
243 lemma rflts_mono: |
|
244 shows "sum_list (map rsize (rflts rs))\<le> sum_list (map rsize rs)" |
|
245 apply(induct rs) |
|
246 apply simp |
|
247 apply(case_tac "a = RZERO") |
|
248 apply simp |
|
249 apply(case_tac "\<exists>rs1. a = RALTS rs1") |
|
250 apply(erule exE) |
|
251 apply simp |
|
252 apply(subgoal_tac "rflts (a # rs) = a # (rflts rs)") |
|
253 prefer 2 |
|
254 using rflts_def_idiot apply blast |
|
255 apply simp |
|
256 done |
|
257 |
|
258 lemma rdistinct_smaller: shows "sum_list (map rsize (rdistinct rs ss)) \<le> |
|
259 sum_list (map rsize rs )" |
|
260 apply (induct rs arbitrary: ss) |
|
261 apply simp |
|
262 by (simp add: trans_le_add2) |
|
263 |
|
264 lemma rdistinct_phi_smaller: "sum_list (map rsize (rdistinct rs {})) \<le> sum_list (map rsize rs)" |
|
265 by (simp add: rdistinct_smaller) |
|
266 |
|
267 |
|
268 lemma rsimp_alts_mono : |
|
269 shows "\<And>x. (\<And>xa. xa \<in> set x \<Longrightarrow> rsize (rsimp xa) \<le> rsize xa) \<Longrightarrow> |
|
270 rsize (rsimp_ALTs (rdistinct (rflts (map rsimp x)) {})) \<le> Suc (sum_list (map rsize x))" |
|
271 apply(subgoal_tac "rsize (rsimp_ALTs (rdistinct (rflts (map rsimp x)) {} )) |
|
272 \<le> rsize (RALTS (rdistinct (rflts (map rsimp x)) {} ))") |
|
273 prefer 2 |
|
274 using rsimp_aalts_smaller apply auto[1] |
|
275 apply(subgoal_tac "rsize (RALTS (rdistinct (rflts (map rsimp x)) {})) \<le>Suc( sum_list (map rsize (rdistinct (rflts (map rsimp x)) {})))") |
|
276 prefer 2 |
|
277 using ralts_cap_mono apply blast |
|
278 apply(subgoal_tac "sum_list (map rsize (rdistinct (rflts (map rsimp x)) {})) \<le> |
|
279 sum_list (map rsize ( (rflts (map rsimp x))))") |
|
280 prefer 2 |
|
281 using rdistinct_smaller apply presburger |
|
282 apply(subgoal_tac "sum_list (map rsize (rflts (map rsimp x))) \<le> |
|
283 sum_list (map rsize (map rsimp x))") |
|
284 prefer 2 |
|
285 using rflts_mono apply blast |
|
286 apply(subgoal_tac "sum_list (map rsize (map rsimp x)) \<le> sum_list (map rsize x)") |
|
287 prefer 2 |
|
288 |
|
289 apply (simp add: sum_list_mono) |
|
290 by linarith |
|
291 |
|
292 |
|
293 |
|
294 |
|
295 |
|
296 lemma rsimp_mono: |
|
297 shows "rsize (rsimp r) \<le> rsize r" |
|
298 apply(induct r) |
|
299 apply simp_all |
|
300 apply(subgoal_tac "rsize (rsimp_SEQ (rsimp r1) (rsimp r2)) \<le> rsize (RSEQ (rsimp r1) (rsimp r2))") |
|
301 apply force |
|
302 using rSEQ_mono |
|
303 apply presburger |
|
304 using rsimp_alts_mono by auto |
|
305 |
|
306 lemma idiot: |
|
307 shows "rsimp_SEQ RONE r = r" |
|
308 apply(case_tac r) |
|
309 apply simp_all |
|
310 done |
|
311 |
|
312 lemma no_alt_short_list_after_simp: |
|
313 shows "RALTS rs = rsimp r \<Longrightarrow> rsimp_ALTs rs = RALTS rs" |
|
314 sorry |
|
315 |
|
316 lemma no_further_dB_after_simp: |
|
317 shows "RALTS rs = rsimp r \<Longrightarrow> rdistinct rs {} = rs" |
|
318 sorry |
|
319 |
|
320 |
|
321 lemma idiot2: |
|
322 shows " \<lbrakk>r1 \<noteq> RZERO; r1 \<noteq> RONE;r2 \<noteq> RZERO\<rbrakk> |
|
323 \<Longrightarrow> rsimp_SEQ r1 r2 = RSEQ r1 r2" |
|
324 apply(case_tac r1) |
|
325 apply(case_tac r2) |
|
326 apply simp_all |
|
327 apply(case_tac r2) |
|
328 apply simp_all |
|
329 apply(case_tac r2) |
|
330 apply simp_all |
|
331 apply(case_tac r2) |
|
332 apply simp_all |
|
333 apply(case_tac r2) |
|
334 apply simp_all |
|
335 done |
|
336 |
|
337 lemma rders__onechar: |
|
338 shows " (rders_simp r [c]) = (rsimp (rders r [c]))" |
|
339 by simp |
|
340 |
|
341 lemma rders_append: |
|
342 "rders c (s1 @ s2) = rders (rders c s1) s2" |
|
343 apply(induct s1 arbitrary: c s2) |
|
344 apply(simp_all) |
|
345 done |
|
346 |
|
347 lemma rders_simp_append: |
|
348 "rders_simp c (s1 @ s2) = rders_simp (rders_simp c s1) s2" |
|
349 apply(induct s1 arbitrary: c s2) |
|
350 apply(simp_all) |
|
351 done |
|
352 |
|
353 lemma inside_simp_removal: |
|
354 shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)" |
|
355 sorry |
|
356 |
|
357 lemma set_related_list: |
|
358 shows "distinct rs \<Longrightarrow> length rs = card (set rs)" |
|
359 by (simp add: distinct_card) |
|
360 (*this section deals with the property of distinctBy: creates a list without duplicates*) |
|
361 lemma rdistinct_never_added_twice: |
|
362 shows "rdistinct (a # rs) {a} = rdistinct rs {a}" |
|
363 by force |
|
364 |
|
365 |
|
366 lemma rdistinct_does_the_job: |
|
367 shows "distinct (rdistinct rs s)" |
|
368 apply(induct rs arbitrary: s) |
|
369 apply simp |
|
370 apply simp |
|
371 sorry |
|
372 |
|
373 lemma rders_simp_same_simpders: |
|
374 shows "s \<noteq> [] \<Longrightarrow> rders_simp r s = rsimp (rders r s)" |
|
375 apply(induct s rule: rev_induct) |
|
376 apply simp |
|
377 apply(case_tac "xs = []") |
|
378 apply simp |
|
379 apply(simp add: rders_append rders_simp_append) |
|
380 using inside_simp_removal by blast |
|
381 |
|
382 lemma simp_helps_der_pierce: |
|
383 shows " rsimp |
|
384 (rder x |
|
385 (rsimp_ALTs rs)) = |
|
386 rsimp |
|
387 (rsimp_ALTs |
|
388 (map (rder x ) |
|
389 rs |
|
390 ) |
|
391 )" |
|
392 sorry |
|
393 |
|
394 |
|
395 lemma rders_simp_one_char: |
|
396 shows "rders_simp r [c] = rsimp (rder c r)" |
|
397 apply auto |
|
398 done |
|
399 |
|
400 lemma rsimp_idem: |
|
401 shows "rsimp (rsimp r) = rsimp r" |
|
402 sorry |
|
403 |
|
404 corollary rsimp_inner_idem1: |
|
405 shows "rsimp r = RSEQ r1 r2 \<Longrightarrow> rsimp r1 = r1 \<and> rsimp r2 = r2" |
|
406 |
|
407 sorry |
|
408 |
|
409 corollary rsimp_inner_idem2: |
|
410 shows "rsimp r = RALTS rs \<Longrightarrow> \<forall>r' \<in> (set rs). rsimp r' = r'" |
|
411 sorry |
|
412 |
|
413 corollary rsimp_inner_idem3: |
|
414 shows "rsimp r = RALTS rs \<Longrightarrow> map rsimp rs = rs" |
|
415 by (meson map_idI rsimp_inner_idem2) |
|
416 |
|
417 corollary rsimp_inner_idem4: |
|
418 shows "rsimp r = RALTS rs \<Longrightarrow> flts rs = rs" |
|
419 sorry |
|
420 |
|
421 |
|
422 lemma head_one_more_simp: |
|
423 shows "map rsimp (r # rs) = map rsimp (( rsimp r) # rs)" |
|
424 by (simp add: rsimp_idem) |
|
425 |
|
426 lemma head_one_more_dersimp: |
|
427 shows "map rsimp ((rder x (rders_simp r s) # rs)) = map rsimp ((rders_simp r (s@[x]) ) # rs)" |
|
428 using head_one_more_simp rders_simp_append rders_simp_one_char by presburger |
|
429 |
|
430 |
|
431 |
|
432 |
|
433 lemma ders_simp_nullability: |
|
434 shows "rnullable (rders r s) = rnullable (rders_simp r s)" |
|
435 sorry |
|
436 |
|
437 lemma first_elem_seqder: |
|
438 shows "\<not>rnullable r1p \<Longrightarrow> map rsimp (rder x (RSEQ r1p r2) |
|
439 # rs) = map rsimp ((RSEQ (rder x r1p) r2) # rs) " |
|
440 by auto |
|
441 |
|
442 lemma first_elem_seqder1: |
|
443 shows "\<not>rnullable (rders_simp r xs) \<Longrightarrow> map rsimp ( (rder x (RSEQ (rders_simp r xs) r2)) # rs) = |
|
444 map rsimp ( (RSEQ (rsimp (rder x (rders_simp r xs))) r2) # rs)" |
|
445 by (simp add: rsimp_idem) |
|
446 |
|
447 lemma first_elem_seqdersimps: |
|
448 shows "\<not>rnullable (rders_simp r xs) \<Longrightarrow> map rsimp ( (rder x (RSEQ (rders_simp r xs) r2)) # rs) = |
|
449 map rsimp ( (RSEQ (rders_simp r (xs @ [x])) r2) # rs)" |
|
450 using first_elem_seqder1 rders_simp_append by auto |
|
451 |
|
452 |
|
453 |
|
454 |
|
455 |
|
456 lemma seq_update_seq_ders: |
|
457 shows "rsimp (rder c ( rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) # |
|
458 (map (rders_simp r2) Ss))))) = |
|
459 rsimp (RALTS ((RSEQ (rders_simp r1 (s @ [c])) r2) # |
|
460 (map (rders_simp r2) (seq_update c (rders_simp r1 s) Ss)))) " |
|
461 sorry |
|
462 |
|
463 lemma seq_ders_closed_form1: |
|
464 shows "\<exists>Ss. rders_simp (RSEQ r1 r2) [c] = rsimp (RALTS ((RSEQ (rders_simp r1 [c]) r2) # |
|
465 (map ( rders_simp r2 ) Ss)))" |
|
466 apply(case_tac "rnullable r1") |
|
467 apply(subgoal_tac " rders_simp (RSEQ r1 r2) [c] = |
|
468 rsimp (RALTS ((RSEQ (rders_simp r1 [c]) r2) # (map (rders_simp r2) [[c]])))") |
|
469 prefer 2 |
|
470 apply (simp add: rsimp_idem) |
|
471 apply(rule_tac x = "[[c]]" in exI) |
|
472 apply simp |
|
473 apply(subgoal_tac " rders_simp (RSEQ r1 r2) [c] = |
|
474 rsimp (RALTS ((RSEQ (rders_simp r1 [c]) r2) # (map (rders_simp r2) [])))") |
|
475 apply blast |
|
476 apply(simp add: rsimp_idem) |
|
477 sorry |
|
478 |
|
479 |
|
480 |
|
481 |
|
482 |
|
483 |
|
484 |
|
485 |
|
486 lemma simp_flatten2: |
|
487 shows "rsimp (RALTS (r # [RALTS rs])) = rsimp (RALTS (r # rs))" |
|
488 sorry |
|
489 |
|
490 |
|
491 lemma simp_flatten: |
|
492 shows "rsimp (RALTS ((RALTS rsa) # rsb)) = rsimp (RALTS (rsa @ rsb))" |
|
493 |
|
494 sorry |
|
495 |
|
496 |
|
497 |
|
498 (*^^^^^^^^^nullable_seq_with_list1 related ^^^^^^^^^^^^^^^^*) |
|
499 |
|
500 |
|
501 |
|
502 |
|
503 |
|
504 |
|
505 |
|
506 |
|
507 |
|
508 |
|
509 |
|
510 lemma non_zero_size: |
|
511 shows "rsize r \<ge> Suc 0" |
|
512 apply(induct r) |
|
513 apply auto done |
|
514 |
|
515 corollary size_geq1: |
|
516 shows "rsize r \<ge> 1" |
|
517 by (simp add: non_zero_size) |
|
518 |
|
519 |
|
520 lemma rexp_size_induct: |
|
521 shows "\<And>N r x5 a list. |
|
522 \<lbrakk> rsize r = Suc N; r = RALTS x5; |
|
523 x5 = a # list\<rbrakk> \<Longrightarrow>\<exists>i j. rsize a = i \<and> rsize (RALTS list) = j \<and> i + j = Suc N \<and> i \<le> N \<and> j \<le> N" |
|
524 apply(rule_tac x = "rsize a" in exI) |
|
525 apply(rule_tac x = "rsize (RALTS list)" in exI) |
|
526 apply(subgoal_tac "rsize a \<ge> 1") |
|
527 prefer 2 |
|
528 using One_nat_def non_zero_size apply presburger |
|
529 apply(subgoal_tac "rsize (RALTS list) \<ge> 1 ") |
|
530 prefer 2 |
|
531 using size_geq1 apply blast |
|
532 apply simp |
|
533 done |
|
534 |
|
535 definition SEQ_set where |
|
536 "SEQ_set A n \<equiv> {RSEQ r1 r2 | r1 r2. r1 \<in> A \<and> r2 \<in> A \<and> rsize r1 + rsize r2 \<le> n}" |
|
537 |
|
538 definition SEQ_set_cartesian where |
|
539 "SEQ_set_cartesian A n = {RSEQ r1 r2 | r1 r2. r1 \<in> A \<and> r2 \<in> A}" |
|
540 |
|
541 definition ALT_set where |
|
542 "ALT_set A n \<equiv> {RALTS rs | rs. set rs \<subseteq> A \<and> sum_list (map rsize rs) \<le> n}" |
|
543 |
|
544 |
|
545 definition |
|
546 "sizeNregex N \<equiv> {r. rsize r \<le> N}" |
|
547 |
|
548 lemma sizenregex_induct: |
|
549 shows "sizeNregex (Suc n) = sizeNregex n \<union> {RZERO, RONE, RALTS []} \<union> {RCHAR c| c. True} \<union> |
|
550 SEQ_set ( sizeNregex n) n \<union> ALT_set (sizeNregex n) n \<union> (RSTAR ` (sizeNregex n))" |
|
551 sorry |
|
552 |
|
553 |
|
554 lemma chars_finite: |
|
555 shows "finite (RCHAR ` (UNIV::(char set)))" |
|
556 apply(simp) |
|
557 done |
|
558 |
|
559 thm full_SetCompr_eq |
|
560 |
|
561 lemma size1finite: |
|
562 shows "finite (sizeNregex (Suc 0))" |
|
563 apply(subst sizenregex_induct) |
|
564 apply(subst finite_Un)+ |
|
565 apply(subgoal_tac "sizeNregex 0 = {}") |
|
566 apply(rule conjI)+ |
|
567 apply (metis Collect_empty_eq finite.emptyI non_zero_size not_less_eq_eq sizeNregex_def) |
|
568 apply simp |
|
569 apply (simp add: full_SetCompr_eq) |
|
570 apply (simp add: SEQ_set_def) |
|
571 apply (simp add: ALT_set_def) |
|
572 apply(simp add: full_SetCompr_eq) |
|
573 using non_zero_size not_less_eq_eq sizeNregex_def by fastforce |
|
574 |
|
575 lemma seq_included_in_cart: |
|
576 shows "SEQ_set A n \<subseteq> SEQ_set_cartesian A n" |
|
577 using SEQ_set_cartesian_def SEQ_set_def by fastforce |
|
578 |
|
579 lemma finite_seq: |
|
580 shows " finite (sizeNregex n) \<Longrightarrow> finite (SEQ_set (sizeNregex n) n)" |
|
581 apply(rule finite_subset) |
|
582 sorry |
|
583 |
|
584 |
|
585 lemma finite_size_n: |
|
586 shows "finite (sizeNregex n)" |
|
587 apply(induct n) |
|
588 apply (metis Collect_empty_eq finite.emptyI non_zero_size not_less_eq_eq sizeNregex_def) |
|
589 apply(subst sizenregex_induct) |
|
590 apply(subst finite_Un)+ |
|
591 apply(rule conjI)+ |
|
592 apply simp |
|
593 apply simp |
|
594 apply (simp add: full_SetCompr_eq) |
|
595 |
|
596 sorry |
|
597 |
|
598 |
|
599 |
|
600 |
|
601 |
|
602 |
|
603 |
|
604 |
|
605 |
|
606 |
|
607 |
|
608 |
|
609 |
|
610 |
|
611 |
|
612 |
|
613 |
|
614 |
|
615 |
|
616 |
|
617 |
|
618 lemma star_update_case1: |
|
619 shows "rnullable (rders_simp r s) \<Longrightarrow> star_update c r (s # Ss) = (s @ [c]) # [c] # (star_update c r Ss)" |
|
620 |
|
621 by force |
|
622 |
|
623 lemma star_update_case2: |
|
624 shows "\<not>rnullable (rders_simp r s) \<Longrightarrow> star_update c r (s # Ss) = (s @ [c]) # (star_update c r Ss)" |
|
625 by simp |
|
626 |
|
627 lemma bubble_break: shows "rflts [r, RZERO] = rflts [r]" |
|
628 apply(case_tac r) |
|
629 apply simp+ |
|
630 done |
|
631 |
|
632 lemma rsimp_alts_idem_aux1: |
|
633 shows "rsimp_ALTs (rdistinct (rflts [rsimp a]) {}) = rsimp (RALTS [a])" |
|
634 by force |
|
635 |
|
636 |
|
637 |
|
638 lemma rsimp_alts_idem_aux2: |
|
639 shows "rsimp a = rsimp (RALTS [a])" |
|
640 apply(simp) |
|
641 apply(case_tac "rsimp a") |
|
642 apply simp+ |
|
643 apply (metis no_alt_short_list_after_simp no_further_dB_after_simp) |
|
644 by simp |
|
645 |
|
646 lemma rsimp_alts_idem: |
|
647 shows "rsimp (rsimp_ALTs (a # as)) = rsimp (rsimp_ALTs (a # [(rsimp (rsimp_ALTs as))] ))" |
|
648 apply(induct as) |
|
649 apply(subgoal_tac "rsimp (rsimp_ALTs [a, rsimp (rsimp_ALTs [])]) = rsimp (rsimp_ALTs [a, RZERO])") |
|
650 prefer 2 |
|
651 apply simp |
|
652 using bubble_break rsimp_alts_idem_aux2 apply auto[1] |
|
653 apply(case_tac as) |
|
654 apply(subgoal_tac "rsimp_ALTs( aa # as) = aa") |
|
655 prefer 2 |
|
656 apply simp |
|
657 using head_one_more_simp apply fastforce |
|
658 apply(subgoal_tac "rsimp_ALTs (aa # as) = RALTS (aa # as)") |
|
659 prefer 2 |
|
660 |
|
661 using rsimp_ALTs.simps(3) apply presburger |
|
662 |
|
663 apply(simp only:) |
|
664 apply(subgoal_tac "rsimp_ALTs (a # aa # aaa # list) = RALTS (a # aa # aaa # list)") |
|
665 prefer 2 |
|
666 using rsimp_ALTs.simps(3) apply presburger |
|
667 apply(simp only:) |
|
668 apply(subgoal_tac "rsimp_ALTs [a, rsimp (RALTS (aa # aaa # list))] = RALTS (a # [rsimp (RALTS (aa # aaa # list))])") |
|
669 prefer 2 |
|
670 |
|
671 using rsimp_ALTs.simps(3) apply presburger |
|
672 apply(simp only:) |
|
673 using simp_flatten2 |
|
674 apply(subgoal_tac " rsimp (RALT a (rsimp (RALTS (aa # aaa # list)))) = rsimp (RALT a ((RALTS (aa # aaa # list)))) ") |
|
675 prefer 2 |
|
676 |
|
677 apply (metis head_one_more_simp list.simps(9) rsimp.simps(2)) |
|
678 apply (simp only:) |
|
679 done |
|
680 |
|
681 |
|
682 lemma rsimp_alts_idem2: |
|
683 shows "rsimp (rsimp_ALTs (a # as)) = rsimp (rsimp_ALTs ((rsimp a) # [(rsimp (rsimp_ALTs as))] ))" |
|
684 using head_one_more_simp rsimp_alts_idem by auto |
|
685 |
|
686 |
|
687 lemma evolution_step1: |
|
688 shows "rsimp |
|
689 (rsimp_ALTs |
|
690 (rder x (rsimp_SEQ (rders_simp r a) (RSTAR r)) # map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) = |
|
691 rsimp |
|
692 (rsimp_ALTs |
|
693 (rder x (rsimp_SEQ (rders_simp r a) (RSTAR r)) # [(rsimp (rsimp_ALTs (map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)))])) " |
|
694 using rsimp_alts_idem by auto |
|
695 |
|
696 lemma evolution_step2: |
|
697 assumes " rsimp (rsimp_ALTs (map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) = |
|
698 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))" |
|
699 shows "rsimp |
|
700 (rsimp_ALTs |
|
701 (rder x (rsimp_SEQ (rders_simp r a) (RSTAR r)) # map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) = |
|
702 rsimp |
|
703 (rsimp_ALTs |
|
704 (rder x (rsimp_SEQ (rders_simp r a) (RSTAR r)) # [ rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))])) " |
|
705 by (simp add: assms rsimp_alts_idem) |
|
706 |
|
707 lemma rsimp_seq_aux1: |
|
708 shows "r = RONE \<and> r2 = RSTAR r0 \<Longrightarrow> rsimp_SEQ r r2 = r2" |
|
709 apply simp |
|
710 done |
|
711 |
|
712 lemma multiple_alts_simp_flatten: |
|
713 shows "rsimp (RALT (RALT r1 r2) (rsimp_ALTs rs)) = rsimp (RALTS (r1 # r2 # rs))" |
|
714 by (metis Cons_eq_appendI append_self_conv2 rsimp_ALTs.simps(2) rsimp_ALTs.simps(3) rsimp_alts_idem simp_flatten) |
|
715 |
|
716 |
|
717 lemma evo3_main_aux1: |
|
718 shows "rsimp |
|
719 (RALT (RALT (RSEQ (rsimp (rders_simp r (a @ [x]))) (RSTAR r)) (RSEQ (rders_simp r [x]) (RSTAR r))) |
|
720 (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))) = |
|
721 rsimp |
|
722 (RALTS |
|
723 (RSEQ (rders_simp r (a @ [x])) (RSTAR r) # |
|
724 RSEQ (rders_simp r [x]) (RSTAR r) # map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))" |
|
725 apply(subgoal_tac "rsimp |
|
726 (RALT (RALT (RSEQ (rsimp (rders_simp r (a @ [x]))) (RSTAR r)) (RSEQ (rders_simp r [x]) (RSTAR r))) |
|
727 (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))) = |
|
728 rsimp |
|
729 (RALT (RALT (RSEQ ( (rders_simp r (a @ [x]))) (RSTAR r)) (RSEQ (rders_simp r [x]) (RSTAR r))) |
|
730 (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))) ") |
|
731 prefer 2 |
|
732 apply (simp add: rsimp_idem) |
|
733 apply (simp only:) |
|
734 apply(subst multiple_alts_simp_flatten) |
|
735 by simp |
|
736 |
|
737 |
|
738 lemma evo3_main_nullable: |
|
739 shows " |
|
740 \<And>a Ss. |
|
741 \<lbrakk>rsimp (rsimp_ALTs (map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) = |
|
742 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))); |
|
743 rders_simp r a \<noteq> RONE; rders_simp r a \<noteq> RZERO; rnullable (rders_simp r a)\<rbrakk> |
|
744 \<Longrightarrow> rsimp |
|
745 (rsimp_ALTs |
|
746 [rder x (RSEQ (rders_simp r a) (RSTAR r)), |
|
747 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))]) = |
|
748 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r (a # Ss))))" |
|
749 apply(subgoal_tac "rder x (RSEQ (rders_simp r a) (RSTAR r)) |
|
750 = RALT (RSEQ (rder x (rders_simp r a)) (RSTAR r)) (RSEQ (rder x r) (RSTAR r))") |
|
751 prefer 2 |
|
752 apply simp |
|
753 apply(simp only:) |
|
754 apply(subgoal_tac "star_update x r (a # Ss) = (a @ [x]) # [x] # (star_update x r Ss)") |
|
755 prefer 2 |
|
756 using star_update_case1 apply presburger |
|
757 apply(simp only:) |
|
758 apply(subst List.list.map(2))+ |
|
759 apply(subgoal_tac "rsimp |
|
760 (rsimp_ALTs |
|
761 [RALT (RSEQ (rder x (rders_simp r a)) (RSTAR r)) (RSEQ (rder x r) (RSTAR r)), |
|
762 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))]) = |
|
763 rsimp |
|
764 (RALTS |
|
765 [RALT (RSEQ (rder x (rders_simp r a)) (RSTAR r)) (RSEQ (rder x r) (RSTAR r)), |
|
766 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))])") |
|
767 prefer 2 |
|
768 using rsimp_ALTs.simps(3) apply presburger |
|
769 apply(simp only:) |
|
770 apply(subgoal_tac " rsimp |
|
771 (rsimp_ALTs |
|
772 (rsimp_SEQ (rders_simp r (a @ [x])) (RSTAR r) # |
|
773 rsimp_SEQ (rders_simp r [x]) (RSTAR r) # map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))) |
|
774 = |
|
775 rsimp |
|
776 (RALTS |
|
777 (rsimp_SEQ (rders_simp r (a @ [x])) (RSTAR r) # |
|
778 rsimp_SEQ (rders_simp r [x]) (RSTAR r) # map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))") |
|
779 |
|
780 prefer 2 |
|
781 using rsimp_ALTs.simps(3) apply presburger |
|
782 apply (simp only:) |
|
783 apply(subgoal_tac " rsimp |
|
784 (RALT (RALT (RSEQ (rder x (rders_simp r a)) (RSTAR r)) (RSEQ ( (rder x r)) (RSTAR r))) |
|
785 (rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))))) = |
|
786 rsimp |
|
787 (RALT (RALT (RSEQ (rsimp (rder x (rders_simp r a))) (RSTAR r)) (RSEQ (rsimp (rder x r)) (RSTAR r))) |
|
788 (rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))))") |
|
789 prefer 2 |
|
790 apply (simp add: rsimp_idem) |
|
791 apply(simp only:) |
|
792 apply(subgoal_tac " rsimp |
|
793 (RALT (RALT (RSEQ (rsimp (rder x (rders_simp r a))) (RSTAR r)) (RSEQ (rsimp (rder x r)) (RSTAR r))) |
|
794 (rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))))) = |
|
795 rsimp |
|
796 (RALT (RALT (RSEQ (rsimp (rders_simp r (a @ [x]))) (RSTAR r)) (RSEQ (rders_simp r [x]) (RSTAR r))) |
|
797 (rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))))") |
|
798 prefer 2 |
|
799 using rders_simp_append rders_simp_one_char rsimp_idem apply presburger |
|
800 apply(simp only:) |
|
801 apply(subgoal_tac " rsimp |
|
802 (RALTS |
|
803 (rsimp_SEQ (rders_simp r (a @ [x])) (RSTAR r) # |
|
804 rsimp_SEQ (rders_simp r [x]) (RSTAR r) # map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))) = |
|
805 rsimp |
|
806 (RALTS |
|
807 (RSEQ (rders_simp r (a @ [x])) (RSTAR r) # |
|
808 RSEQ (rders_simp r [x]) (RSTAR r) # map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))") |
|
809 prefer 2 |
|
810 apply (smt (z3) idiot2 list.simps(9) rrexp.distinct(9) rsimp.simps(1) rsimp.simps(2) rsimp.simps(3) rsimp.simps(4) rsimp.simps(6) rsimp_idem) |
|
811 apply(simp only:) |
|
812 apply(subgoal_tac " rsimp |
|
813 (RALT (RALT (RSEQ (rsimp (rders_simp r (a @ [x]))) (RSTAR r)) (RSEQ (rders_simp r [x]) (RSTAR r))) |
|
814 (rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))))) = |
|
815 rsimp |
|
816 (RALT (RALT (RSEQ (rsimp (rders_simp r (a @ [x]))) (RSTAR r)) (RSEQ (rders_simp r [x]) (RSTAR r))) |
|
817 ( (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))))) ") |
|
818 prefer 2 |
|
819 using rsimp_idem apply force |
|
820 apply(simp only:) |
|
821 using evo3_main_aux1 by blast |
|
822 |
|
823 |
|
824 lemma evo3_main_not1: |
|
825 shows " \<not>rnullable (rders_simp r a) \<Longrightarrow> rder x (RSEQ (rders_simp r a) (RSTAR r)) = RSEQ (rder x (rders_simp r a)) (RSTAR r)" |
|
826 by fastforce |
|
827 |
|
828 |
|
829 lemma evo3_main_not2: |
|
830 shows "\<not>rnullable (rders_simp r a) \<Longrightarrow> rsimp |
|
831 (rsimp_ALTs |
|
832 (rder x (RSEQ (rders_simp r a) (RSTAR r)) # rs)) = rsimp |
|
833 (rsimp_ALTs |
|
834 ((RSEQ (rders_simp r (a @ [x])) (RSTAR r)) # rs))" |
|
835 by (simp add: rders_simp_append rsimp_alts_idem2 rsimp_idem) |
|
836 |
|
837 lemma evo3_main_not3: |
|
838 shows "rsimp |
|
839 (rsimp_ALTs |
|
840 (rsimp_SEQ r1 (RSTAR r) # rs)) = |
|
841 rsimp (rsimp_ALTs |
|
842 (RSEQ r1 (RSTAR r) # rs))" |
|
843 by (metis idiot2 rrexp.distinct(9) rsimp.simps(1) rsimp.simps(3) rsimp.simps(4) rsimp.simps(6) rsimp_alts_idem rsimp_alts_idem2) |
|
844 |
|
845 |
|
846 lemma evo3_main_notnullable: |
|
847 shows "\<And>a Ss. |
|
848 \<lbrakk>rsimp (rsimp_ALTs (map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) = |
|
849 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))); |
|
850 rders_simp r a \<noteq> RONE; rders_simp r a \<noteq> RZERO; \<not>rnullable (rders_simp r a)\<rbrakk> |
|
851 \<Longrightarrow> rsimp |
|
852 (rsimp_ALTs |
|
853 [rder x (RSEQ (rders_simp r a) (RSTAR r)), |
|
854 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))]) = |
|
855 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r (a # Ss))))" |
|
856 apply(subst star_update_case2) |
|
857 apply simp |
|
858 apply(subst List.list.map(2)) |
|
859 apply(subst evo3_main_not2) |
|
860 apply simp |
|
861 apply(subst evo3_main_not3) |
|
862 using rsimp_alts_idem by presburger |
|
863 |
|
864 |
|
865 lemma evo3_aux2: |
|
866 shows "rders_simp r a = RONE \<Longrightarrow> rsimp_SEQ (rders_simp (rders_simp r a) [x]) (RSTAR r) = RZERO" |
|
867 by simp |
|
868 lemma evo3_aux3: |
|
869 shows "rsimp (rsimp_ALTs (RZERO # rs)) = rsimp (rsimp_ALTs rs)" |
|
870 by (metis list.simps(8) list.simps(9) rdistinct.simps(1) rflts.simps(1) rflts.simps(2) rsimp.simps(2) rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3) rsimp_alts_idem) |
|
871 |
|
872 lemma evo3_aux4: |
|
873 shows " rsimp |
|
874 (rsimp_ALTs |
|
875 [RSEQ (rder x r) (RSTAR r), |
|
876 rsimp (rsimp_ALTs rs)]) = |
|
877 rsimp |
|
878 (rsimp_ALTs |
|
879 (rsimp_SEQ (rders_simp r [x]) (RSTAR r) # rs))" |
|
880 by (metis rders_simp_one_char rsimp.simps(1) rsimp.simps(6) rsimp_alts_idem rsimp_alts_idem2) |
|
881 |
|
882 lemma evo3_aux5: |
|
883 shows "rders_simp r a \<noteq> RONE \<and> rders_simp r a \<noteq> RZERO \<Longrightarrow> rsimp_SEQ (rders_simp r a) (RSTAR r) = RSEQ (rders_simp r a) (RSTAR r)" |
|
884 using idiot2 by blast |
|
885 |
|
886 |
|
887 lemma evolution_step3: |
|
888 shows" \<And>a Ss. |
|
889 rsimp (rsimp_ALTs (map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) = |
|
890 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss))) \<Longrightarrow> |
|
891 rsimp |
|
892 (rsimp_ALTs |
|
893 [rder x (rsimp_SEQ (rders_simp r a) (RSTAR r)), |
|
894 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)))]) = |
|
895 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r (a # Ss))))" |
|
896 apply(case_tac "rders_simp r a = RONE") |
|
897 apply(subst rsimp_seq_aux1) |
|
898 apply simp |
|
899 apply(subst rder.simps(6)) |
|
900 apply(subgoal_tac "rnullable (rders_simp r a)") |
|
901 prefer 2 |
|
902 using rnullable.simps(2) apply presburger |
|
903 apply(subst star_update_case1) |
|
904 apply simp |
|
905 |
|
906 apply(subst List.list.map)+ |
|
907 apply(subst rders_simp_append) |
|
908 apply(subst evo3_aux2) |
|
909 apply simp |
|
910 apply(subst evo3_aux3) |
|
911 apply(subst evo3_aux4) |
|
912 apply simp |
|
913 apply(case_tac "rders_simp r a = RZERO") |
|
914 |
|
915 apply (simp add: rsimp_alts_idem2) |
|
916 apply(subgoal_tac "rders_simp r (a @ [x]) = RZERO") |
|
917 prefer 2 |
|
918 using rder.simps(1) rders_simp_append rders_simp_one_char rsimp.simps(3) apply presburger |
|
919 using rflts.simps(2) rsimp.simps(3) rsimp_SEQ.simps(1) apply presburger |
|
920 apply(subst evo3_aux5) |
|
921 apply simp |
|
922 apply(case_tac "rnullable (rders_simp r a) ") |
|
923 using evo3_main_nullable apply blast |
|
924 using evo3_main_notnullable apply blast |
|
925 done |
|
926 |
|
927 (* |
|
928 proof (prove) |
|
929 goal (1 subgoal): |
|
930 1. map f (a # s) = f a # map f s |
|
931 Auto solve_direct: the current goal can be solved directly with |
|
932 HOL.nitpick_simp(115): map ?f (?x21.0 # ?x22.0) = ?f ?x21.0 # map ?f ?x22.0 |
|
933 List.list.map(2): map ?f (?x21.0 # ?x22.0) = ?f ?x21.0 # map ?f ?x22.0 |
|
934 List.list.simps(9): map ?f (?x21.0 # ?x22.0) = ?f ?x21.0 # map ?f ?x22.0 |
|
935 *) |
|
936 lemma starseq_list_evolution: |
|
937 fixes r :: rrexp and Ss :: "char list list" and x :: char |
|
938 shows "rsimp (rsimp_ALTs (map (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss) ) = |
|
939 rsimp (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) (star_update x r Ss)) )" |
|
940 apply(induct Ss) |
|
941 apply simp |
|
942 apply(subst List.list.map(2)) |
|
943 apply(subst evolution_step2) |
|
944 apply simp |
|
945 |
|
946 |
|
947 sorry |
|
948 |
|
949 |
|
950 lemma star_seqs_produce_star_seqs: |
|
951 shows "rsimp (rsimp_ALTs (map (rder x \<circ> (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) |
|
952 = rsimp (rsimp_ALTs (map ( (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r)))) Ss))" |
|
953 by (meson comp_apply) |
|
954 |
|
955 lemma map_der_lambda_composition: |
|
956 shows "map (rder x) (map (\<lambda>s. f s) Ss) = map (\<lambda>s. (rder x (f s))) Ss" |
|
957 by force |
|
958 |
|
959 lemma ralts_vs_rsimpalts: |
|
960 shows "rsimp (RALTS rs) = rsimp (rsimp_ALTs rs)" |
|
961 by (metis evo3_aux3 rsimp_ALTs.simps(2) rsimp_ALTs.simps(3) simp_flatten2) |
|
962 |
|
963 |
|
964 lemma linearity_of_list_of_star_or_starseqs: |
|
965 fixes r::rrexp and Ss::"char list list" and x::char |
|
966 shows "\<exists>Ssa. rsimp (rder x (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss))) = |
|
967 rsimp (RALTS ( (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ssa)))" |
|
968 apply(subst rder_rsimp_ALTs_commute) |
|
969 apply(subst map_der_lambda_composition) |
|
970 using starseq_list_evolution |
|
971 apply(rule_tac x = "star_update x r Ss" in exI) |
|
972 apply(subst ralts_vs_rsimpalts) |
|
973 by simp |
|
974 |
|
975 |
|
976 |
|
977 (*certified correctness---does not depend on any previous sorry*) |
|
978 lemma star_list_push_der: shows " \<lbrakk>xs \<noteq> [] \<Longrightarrow> \<exists>Ss. rders_simp (RSTAR r) xs = rsimp (RALTS (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss)); |
|
979 xs @ [x] \<noteq> []; xs \<noteq> []\<rbrakk> \<Longrightarrow> |
|
980 \<exists>Ss. rders_simp (RSTAR r ) (xs @ [x]) = |
|
981 rsimp (RALTS (map (\<lambda>s1. (rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r))) ) Ss) )" |
|
982 apply(subgoal_tac "\<exists>Ss. rders_simp (RSTAR r) xs = rsimp (RALTS (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss))") |
|
983 prefer 2 |
|
984 apply blast |
|
985 apply(erule exE) |
|
986 apply(subgoal_tac "rders_simp (RSTAR r) (xs @ [x]) = rsimp (rder x (rsimp (RALTS (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss))))") |
|
987 prefer 2 |
|
988 using rders_simp_append |
|
989 using rders_simp_one_char apply presburger |
|
990 apply(rule_tac x= "Ss" in exI) |
|
991 apply(subgoal_tac " rsimp (rder x (rsimp (RALTS (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss)))) = |
|
992 rsimp (rsimp (rder x (RALTS (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss))))") |
|
993 prefer 2 |
|
994 using inside_simp_removal rsimp_idem apply presburger |
|
995 apply(subgoal_tac "rsimp (rsimp (rder x (RALTS (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss)))) = |
|
996 rsimp (rsimp (RALTS (map (rder x) (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss))))") |
|
997 prefer 2 |
|
998 using rder.simps(4) apply presburger |
|
999 apply(subgoal_tac "rsimp (rsimp (RALTS (map (rder x) (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss)))) = |
|
1000 rsimp (rsimp (RALTS (map (\<lambda>s1. (rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r)))) Ss)))") |
|
1001 apply (metis rsimp_idem) |
|
1002 by (metis map_der_lambda_composition) |
|
1003 |
|
1004 |
|
1005 |
|
1006 end |