| changeset 642 | 6c13f76c070b |
| parent 558 | 671a83abccf3 |
| 641:cf7a5c863831 | 642:6c13f76c070b |
|---|---|
1 theory ClosedForms |
1 theory ClosedForms |
2 imports "HarderProps" |
2 imports "BasicIdentities" |
3 begin |
3 begin |
4 |
4 |
5 |
5 lemma flts_middle0: |
6 shows "rflts (rsa @ RZERO # rsb) = rflts (rsa @ rsb)" |
|
7 apply(induct rsa) |
|
8 apply simp |
|
9 by (metis append_Cons rflts.simps(2) rflts.simps(3) rflts_def_idiot) |
|
10 |
|
11 |
|
12 |
|
13 lemma simp_flatten_aux0: |
|
14 shows "rsimp (RALTS rs) = rsimp (RALTS (map rsimp rs))" |
|
15 by (metis append_Nil head_one_more_simp identity_wwo0 list.simps(8) rdistinct.simps(1) rflts.simps(1) rsimp.simps(2) rsimp_ALTs.simps(1) rsimp_ALTs.simps(3) simp_flatten spawn_simp_rsimpalts) |
|
16 |
|
6 |
17 |
7 inductive |
18 inductive |
8 hrewrite:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ h\<leadsto> _" [99, 99] 99) |
19 hrewrite:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ h\<leadsto> _" [99, 99] 99) |
9 where |
20 where |
10 "RSEQ RZERO r2 h\<leadsto> RZERO" |
21 "RSEQ RZERO r2 h\<leadsto> RZERO" |
54 lemma hrewrites_seq_contexts: |
65 lemma hrewrites_seq_contexts: |
55 shows "\<lbrakk>r1 h\<leadsto>* r2; r3 h\<leadsto>* r4\<rbrakk> \<Longrightarrow> RSEQ r1 r3 h\<leadsto>* RSEQ r2 r4" |
66 shows "\<lbrakk>r1 h\<leadsto>* r2; r3 h\<leadsto>* r4\<rbrakk> \<Longrightarrow> RSEQ r1 r3 h\<leadsto>* RSEQ r2 r4" |
56 by (meson hreal_trans hrewrites_seq_context hrewrites_seq_context2) |
67 by (meson hreal_trans hrewrites_seq_context hrewrites_seq_context2) |
57 |
68 |
58 |
69 |
59 |
70 lemma simp_removes_duplicate1: |
60 |
71 shows " a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ [a])) = rsimp (RALTS (rsa))" |
72 and " rsimp (RALTS (a1 # rsa @ [a1])) = rsimp (RALTS (a1 # rsa))" |
|
73 apply(induct rsa arbitrary: a1) |
|
74 apply simp |
|
75 apply simp |
|
76 prefer 2 |
|
77 apply(case_tac "a = aa") |
|
78 apply simp |
|
79 apply simp |
|
80 apply (metis Cons_eq_appendI Cons_eq_map_conv distinct_removes_duplicate_flts list.set_intros(2)) |
|
81 apply (metis append_Cons append_Nil distinct_removes_duplicate_flts list.set_intros(1) list.simps(8) list.simps(9)) |
|
82 by (metis (mono_tags, lifting) append_Cons distinct_removes_duplicate_flts list.set_intros(1) list.simps(8) list.simps(9) map_append rsimp.simps(2)) |
|
83 |
|
84 lemma simp_removes_duplicate2: |
|
85 shows "a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ [a] @ rsb)) = rsimp (RALTS (rsa @ rsb))" |
|
86 apply(induct rsb arbitrary: rsa) |
|
87 apply simp |
|
88 using distinct_removes_duplicate_flts apply auto[1] |
|
89 by (metis append.assoc head_one_more_simp rsimp.simps(2) simp_flatten simp_removes_duplicate1(1)) |
|
90 |
|
91 lemma simp_removes_duplicate3: |
|
92 shows "a \<in> set rsa \<Longrightarrow> rsimp (RALTS (rsa @ a # rsb)) = rsimp (RALTS (rsa @ rsb))" |
|
93 using simp_removes_duplicate2 by auto |
|
94 |
|
95 (* |
|
96 lemma distinct_removes_middle4: |
|
97 shows "a \<in> set rsa \<Longrightarrow> rdistinct (rsa @ [a] @ rsb) rset = rdistinct (rsa @ rsb) rset" |
|
98 using distinct_removes_middle(1) by fastforce |
|
99 *) |
|
100 |
|
101 (* |
|
102 lemma distinct_removes_middle_list: |
|
103 shows "\<forall>a \<in> set x. a \<in> set rsa \<Longrightarrow> rdistinct (rsa @ x @ rsb) rset = rdistinct (rsa @ rsb) rset" |
|
104 apply(induct x) |
|
105 apply simp |
|
106 by (simp add: distinct_removes_middle3) |
|
107 *) |
|
61 |
108 |
62 inductive frewrite:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>f _" [10, 10] 10) |
109 inductive frewrite:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>f _" [10, 10] 10) |
63 where |
110 where |
64 "(RZERO # rs) \<leadsto>f rs" |
111 "(RZERO # rs) \<leadsto>f rs" |
65 | "((RALTS rs) # rsa) \<leadsto>f (rs @ rsa)" |
112 | "((RALTS rs) # rsa) \<leadsto>f (rs @ rsa)" |
209 apply(induct rsa rsb rule: grewrites.induct) |
256 apply(induct rsa rsb rule: grewrites.induct) |
210 apply(case_tac rs) |
257 apply(case_tac rs) |
211 apply simp |
258 apply simp |
212 using grewrites_append apply blast |
259 using grewrites_append apply blast |
213 by (meson greal_trans grewrites.simps grewrites_concat) |
260 by (meson greal_trans grewrites.simps grewrites_concat) |
261 |
|
262 fun alt_set:: "rrexp \<Rightarrow> rrexp set" |
|
263 where |
|
264 "alt_set (RALTS rs) = set rs \<union> \<Union> (alt_set ` (set rs))" |
|
265 | "alt_set r = {r}" |
|
214 |
266 |
215 |
267 |
216 lemma grewrite_cases_middle: |
268 lemma grewrite_cases_middle: |
217 shows "rs1 \<leadsto>g rs2 \<Longrightarrow> |
269 shows "rs1 \<leadsto>g rs2 \<Longrightarrow> |
218 (\<exists>rsa rsb rsc. rs1 = (rsa @ [RALTS rsb] @ rsc) \<and> rs2 = (rsa @ rsb @ rsc)) \<or> |
270 (\<exists>rsa rsb rsc. rs1 = (rsa @ [RALTS rsb] @ rsc) \<and> rs2 = (rsa @ rsb @ rsc)) \<or> |
223 apply blast |
275 apply blast |
224 apply (metis append_Cons append_Nil) |
276 apply (metis append_Cons append_Nil) |
225 apply (metis append_Cons) |
277 apply (metis append_Cons) |
226 by blast |
278 by blast |
227 |
279 |
280 |
|
281 lemma good_singleton: |
|
282 shows "good a \<and> nonalt a \<Longrightarrow> rflts [a] = [a]" |
|
283 using good.simps(1) k0b by blast |
|
284 |
|
285 |
|
286 |
|
287 |
|
288 |
|
289 |
|
290 |
|
291 lemma all_that_same_elem: |
|
292 shows "\<lbrakk> a \<in> rset; rdistinct rs {a} = []\<rbrakk> |
|
293 \<Longrightarrow> rdistinct (rs @ rsb) rset = rdistinct rsb rset" |
|
294 apply(induct rs) |
|
295 apply simp |
|
296 apply(subgoal_tac "aa = a") |
|
297 apply simp |
|
298 by (metis empty_iff insert_iff list.discI rdistinct.simps(2)) |
|
299 |
|
300 lemma distinct_early_app1: |
|
301 shows "rset1 \<subseteq> rset \<Longrightarrow> rdistinct rs rset = rdistinct (rdistinct rs rset1) rset" |
|
302 apply(induct rs arbitrary: rset rset1) |
|
303 apply simp |
|
304 apply simp |
|
305 apply(case_tac "a \<in> rset1") |
|
306 apply simp |
|
307 apply(case_tac "a \<in> rset") |
|
308 apply simp+ |
|
309 |
|
310 apply blast |
|
311 apply(case_tac "a \<in> rset1") |
|
312 apply simp+ |
|
313 apply(case_tac "a \<in> rset") |
|
314 apply simp |
|
315 apply (metis insert_subsetI) |
|
316 apply simp |
|
317 by (meson insert_mono) |
|
318 |
|
319 |
|
320 lemma distinct_early_app: |
|
321 shows " rdistinct (rs @ rsb) rset = rdistinct (rdistinct rs {} @ rsb) rset" |
|
322 apply(induct rsb) |
|
323 apply simp |
|
324 using distinct_early_app1 apply blast |
|
325 by (metis distinct_early_app1 distinct_once_enough empty_subsetI) |
|
326 |
|
327 |
|
328 lemma distinct_eq_interesting1: |
|
329 shows "a \<in> rset \<Longrightarrow> rdistinct (rs @ rsb) rset = rdistinct (rdistinct (a # rs) {} @ rsb) rset" |
|
330 apply(subgoal_tac "rdistinct (rdistinct (a # rs) {} @ rsb) rset = rdistinct (rdistinct rs {} @ rsb) rset") |
|
331 apply(simp only:) |
|
332 using distinct_early_app apply blast |
|
333 by (metis append_Cons distinct_early_app rdistinct.simps(2)) |
|
334 |
|
335 |
|
336 |
|
337 lemma good_flatten_aux_aux1: |
|
338 shows "\<lbrakk> size rs \<ge>2; |
|
339 \<forall>r \<in> set rs. good r \<and> r \<noteq> RZERO \<and> nonalt r; \<forall>r \<in> set rsb. good r \<and> r \<noteq> RZERO \<and> nonalt r \<rbrakk> |
|
340 \<Longrightarrow> rdistinct (rs @ rsb) rset = |
|
341 rdistinct (rflts [rsimp_ALTs (rdistinct rs {})] @ rsb) rset" |
|
342 apply(induct rs arbitrary: rset) |
|
343 apply simp |
|
344 apply(case_tac "a \<in> rset") |
|
345 apply simp |
|
346 apply(case_tac "rdistinct rs {a}") |
|
347 apply simp |
|
348 apply(subst good_singleton) |
|
349 apply force |
|
350 apply simp |
|
351 apply (meson all_that_same_elem) |
|
352 apply(subgoal_tac "rflts [rsimp_ALTs (a # rdistinct rs {a})] = a # rdistinct rs {a} ") |
|
353 prefer 2 |
|
354 using k0a rsimp_ALTs.simps(3) apply presburger |
|
355 apply(simp only:) |
|
356 apply(subgoal_tac "rdistinct (rs @ rsb) rset = rdistinct ((rdistinct (a # rs) {}) @ rsb) rset ") |
|
357 apply (metis insert_absorb insert_is_Un insert_not_empty rdistinct.simps(2)) |
|
358 apply (meson distinct_eq_interesting1) |
|
359 apply simp |
|
360 apply(case_tac "rdistinct rs {a}") |
|
361 prefer 2 |
|
362 apply(subgoal_tac "rsimp_ALTs (a # rdistinct rs {a}) = RALTS (a # rdistinct rs {a})") |
|
363 apply(simp only:) |
|
364 apply(subgoal_tac "a # rdistinct (rs @ rsb) (insert a rset) = |
|
365 rdistinct (rflts [RALTS (a # rdistinct rs {a})] @ rsb) rset") |
|
366 apply simp |
|
367 apply (metis append_Cons distinct_early_app empty_iff insert_is_Un k0a rdistinct.simps(2)) |
|
368 using rsimp_ALTs.simps(3) apply presburger |
|
369 by (metis Un_insert_left append_Cons distinct_early_app empty_iff good_singleton rdistinct.simps(2) rsimp_ALTs.simps(2) sup_bot_left) |
|
370 |
|
371 |
|
372 |
|
373 |
|
374 |
|
375 lemma good_flatten_aux_aux: |
|
376 shows "\<lbrakk>\<exists>a aa lista list. rs = a # list \<and> list = aa # lista; |
|
377 \<forall>r \<in> set rs. good r \<and> r \<noteq> RZERO \<and> nonalt r; \<forall>r \<in> set rsb. good r \<and> r \<noteq> RZERO \<and> nonalt r \<rbrakk> |
|
378 \<Longrightarrow> rdistinct (rs @ rsb) rset = |
|
379 rdistinct (rflts [rsimp_ALTs (rdistinct rs {})] @ rsb) rset" |
|
380 apply(erule exE)+ |
|
381 apply(subgoal_tac "size rs \<ge> 2") |
|
382 apply (metis good_flatten_aux_aux1) |
|
383 by (simp add: Suc_leI length_Cons less_add_Suc1) |
|
384 |
|
385 |
|
386 |
|
387 lemma good_flatten_aux: |
|
388 shows " \<lbrakk>\<forall>r\<in>set rs. good r \<or> r = RZERO; \<forall>r\<in>set rsa . good r \<or> r = RZERO; |
|
389 \<forall>r\<in>set rsb. good r \<or> r = RZERO; |
|
390 rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (rsa @ rs @ rsb)) {}); |
|
391 rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = |
|
392 rsimp_ALTs (rdistinct (rflts (rsa @ [rsimp (RALTS rs)] @ rsb)) {}); |
|
393 map rsimp rsa = rsa; map rsimp rsb = rsb; map rsimp rs = rs; |
|
394 rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} = |
|
395 rdistinct (rflts rsa) {} @ rdistinct (rflts rs @ rflts rsb) (set (rflts rsa)); |
|
396 rdistinct (rflts rsa @ rflts [rsimp (RALTS rs)] @ rflts rsb) {} = |
|
397 rdistinct (rflts rsa) {} @ rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))\<rbrakk> |
|
398 \<Longrightarrow> rdistinct (rflts rs @ rflts rsb) rset = |
|
399 rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) rset" |
|
400 apply simp |
|
401 apply(case_tac "rflts rs ") |
|
402 apply simp |
|
403 apply(case_tac "list") |
|
404 apply simp |
|
405 apply(case_tac "a \<in> rset") |
|
406 apply simp |
|
407 apply (metis append.left_neutral append_Cons equals0D k0b list.set_intros(1) nonalt_flts_rd qqq1 rdistinct.simps(2)) |
|
408 apply simp |
|
409 apply (metis Un_insert_left append_Cons append_Nil ex_in_conv flts_single1 insertI1 list.simps(15) nonalt_flts_rd nonazero.elims(3) qqq1 rdistinct.simps(2) sup_bot_left) |
|
410 apply(subgoal_tac "\<forall>r \<in> set (rflts rs). good r \<and> r \<noteq> RZERO \<and> nonalt r") |
|
411 prefer 2 |
|
412 apply (metis Diff_empty flts3 nonalt_flts_rd qqq1 rdistinct_set_equality1) |
|
413 apply(subgoal_tac "\<forall>r \<in> set (rflts rsb). good r \<and> r \<noteq> RZERO \<and> nonalt r") |
|
414 prefer 2 |
|
415 apply (metis Diff_empty flts3 good.simps(1) nonalt_flts_rd rdistinct_set_equality1) |
|
416 by (smt (verit, ccfv_threshold) good_flatten_aux_aux) |
|
417 |
|
418 |
|
419 |
|
420 |
|
421 lemma good_flatten_middle: |
|
422 shows "\<lbrakk>\<forall>r \<in> set rs. good r \<or> r = RZERO; \<forall>r \<in> set rsa. good r \<or> r = RZERO; \<forall>r \<in> set rsb. good r \<or> r = RZERO\<rbrakk> \<Longrightarrow> |
|
423 rsimp (RALTS (rsa @ rs @ rsb)) = rsimp (RALTS (rsa @ [RALTS rs] @ rsb))" |
|
424 apply(subgoal_tac "rsimp (RALTS (rsa @ rs @ rsb)) = rsimp_ALTs (rdistinct (rflts (map rsimp rsa @ |
|
425 map rsimp rs @ map rsimp rsb)) {})") |
|
426 prefer 2 |
|
427 apply simp |
|
428 apply(simp only:) |
|
429 apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp_ALTs (rdistinct (rflts (map rsimp rsa @ |
|
430 [rsimp (RALTS rs)] @ map rsimp rsb)) {})") |
|
431 prefer 2 |
|
432 apply simp |
|
433 apply(simp only:) |
|
434 apply(subgoal_tac "map rsimp rsa = rsa") |
|
435 prefer 2 |
|
436 apply (metis map_idI rsimp.simps(3) test) |
|
437 apply(simp only:) |
|
438 apply(subgoal_tac "map rsimp rsb = rsb") |
|
439 prefer 2 |
|
440 apply (metis map_idI rsimp.simps(3) test) |
|
441 apply(simp only:) |
|
442 apply(subst k00)+ |
|
443 apply(subgoal_tac "map rsimp rs = rs") |
|
444 apply(simp only:) |
|
445 prefer 2 |
|
446 apply (metis map_idI rsimp.simps(3) test) |
|
447 apply(subgoal_tac "rdistinct (rflts rsa @ rflts rs @ rflts rsb) {} = |
|
448 rdistinct (rflts rsa) {} @ rdistinct (rflts rs @ rflts rsb) (set (rflts rsa))") |
|
449 apply(simp only:) |
|
450 prefer 2 |
|
451 using rdistinct_concat_general apply blast |
|
452 apply(subgoal_tac "rdistinct (rflts rsa @ rflts [rsimp (RALTS rs)] @ rflts rsb) {} = |
|
453 rdistinct (rflts rsa) {} @ rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))") |
|
454 apply(simp only:) |
|
455 prefer 2 |
|
456 using rdistinct_concat_general apply blast |
|
457 apply(subgoal_tac "rdistinct (rflts rs @ rflts rsb) (set (rflts rsa)) = |
|
458 rdistinct (rflts [rsimp (RALTS rs)] @ rflts rsb) (set (rflts rsa))") |
|
459 apply presburger |
|
460 using good_flatten_aux by blast |
|
461 |
|
462 |
|
463 lemma simp_flatten3: |
|
464 shows "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = rsimp (RALTS (rsa @ rs @ rsb))" |
|
465 apply(subgoal_tac "rsimp (RALTS (rsa @ [RALTS rs] @ rsb)) = |
|
466 rsimp (RALTS (map rsimp rsa @ [rsimp (RALTS rs)] @ map rsimp rsb)) ") |
|
467 prefer 2 |
|
468 apply (metis append.left_neutral append_Cons list.simps(9) map_append simp_flatten_aux0) |
|
469 apply (simp only:) |
|
470 apply(subgoal_tac "rsimp (RALTS (rsa @ rs @ rsb)) = |
|
471 rsimp (RALTS (map rsimp rsa @ map rsimp rs @ map rsimp rsb))") |
|
472 prefer 2 |
|
473 apply (metis map_append simp_flatten_aux0) |
|
474 apply(simp only:) |
|
475 apply(subgoal_tac "rsimp (RALTS (map rsimp rsa @ map rsimp rs @ map rsimp rsb)) = |
|
476 rsimp (RALTS (map rsimp rsa @ [RALTS (map rsimp rs)] @ map rsimp rsb))") |
|
477 |
|
478 apply (metis (no_types, lifting) head_one_more_simp map_append simp_flatten_aux0) |
|
479 apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsa). good r \<or> r = RZERO") |
|
480 apply(subgoal_tac "\<forall>r \<in> set (map rsimp rs). good r \<or> r = RZERO") |
|
481 apply(subgoal_tac "\<forall>r \<in> set (map rsimp rsb). good r \<or> r = RZERO") |
|
482 |
|
483 using good_flatten_middle apply presburger |
|
484 |
|
485 apply (simp add: good1) |
|
486 apply (simp add: good1) |
|
487 apply (simp add: good1) |
|
488 |
|
489 done |
|
228 |
490 |
229 |
491 |
230 |
492 |
231 |
493 |
232 |
494 |
275 apply(case_tac "rnullable x41") |
537 apply(case_tac "rnullable x41") |
276 apply simp+ |
538 apply simp+ |
277 apply (simp add: frewrites_alt) |
539 apply (simp add: frewrites_alt) |
278 apply (simp add: frewrites_cons) |
540 apply (simp add: frewrites_cons) |
279 apply (simp add: frewrites_append) |
541 apply (simp add: frewrites_append) |
280 by (simp add: frewrites_cons) |
542 apply (simp add: frewrites_cons) |
281 |
543 apply (auto simp add: frewrites_cons) |
544 using frewrite.intros(1) many_steps_later by blast |
|
545 |
|
282 |
546 |
283 lemma gstar0: |
547 lemma gstar0: |
284 shows "rsa @ (rdistinct rs (set rsa)) \<leadsto>g* rsa @ (rdistinct rs (insert RZERO (set rsa)))" |
548 shows "rsa @ (rdistinct rs (set rsa)) \<leadsto>g* rsa @ (rdistinct rs (insert RZERO (set rsa)))" |
285 apply(induct rs arbitrary: rsa) |
549 apply(induct rs arbitrary: rsa) |
286 apply simp |
550 apply simp |
378 lemma r_finite1: |
642 lemma r_finite1: |
379 shows "r = RALTS (r # rs) = False" |
643 shows "r = RALTS (r # rs) = False" |
380 apply(induct r) |
644 apply(induct r) |
381 apply simp+ |
645 apply simp+ |
382 apply (metis list.set_intros(1)) |
646 apply (metis list.set_intros(1)) |
383 by blast |
647 apply blast |
648 by simp |
|
384 |
649 |
385 |
650 |
386 |
651 |
387 lemma grewrite_singleton: |
652 lemma grewrite_singleton: |
388 shows "[r] \<leadsto>g r # rs \<Longrightarrow> rs = []" |
653 shows "[r] \<leadsto>g r # rs \<Longrightarrow> rs = []" |
602 shows "rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts rs)) {})) |
867 shows "rsimp (rsimp_ALTs (rdistinct (map (rder x) (rflts rs)) {})) |
603 = rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) rs)) {}))" |
868 = rsimp (rsimp_ALTs (rdistinct (rflts (map (rder x) rs)) {}))" |
604 by (metis append.right_neutral grewrite.intros(2) grewrite_simpalts rsimp_ALTs.simps(2) simp_der_flts) |
869 by (metis append.right_neutral grewrite.intros(2) grewrite_simpalts rsimp_ALTs.simps(2) simp_der_flts) |
605 |
870 |
606 |
871 |
607 |
872 lemma basic_regex_property1: |
873 shows "rnullable r \<Longrightarrow> rsimp r \<noteq> RZERO" |
|
874 apply(induct r rule: rsimp.induct) |
|
875 apply(auto) |
|
876 apply (metis idiot idiot2 rrexp.distinct(5)) |
|
877 by (metis der_simp_nullability rnullable.simps(1) rnullable.simps(4) rsimp.simps(2)) |
|
878 |
|
879 |
|
880 lemma inside_simp_seq_nullable: |
|
881 shows |
|
882 "\<And>r1 r2. |
|
883 \<lbrakk>rsimp (rder x (rsimp r1)) = rsimp (rder x r1); rsimp (rder x (rsimp r2)) = rsimp (rder x r2); |
|
884 rnullable r1\<rbrakk> |
|
885 \<Longrightarrow> rsimp (rder x (rsimp_SEQ (rsimp r1) (rsimp r2))) = |
|
886 rsimp_ALTs (rdistinct (rflts [rsimp_SEQ (rsimp (rder x r1)) (rsimp r2), rsimp (rder x r2)]) {})" |
|
887 apply(case_tac "rsimp r1 = RONE") |
|
888 apply(simp) |
|
889 apply(subst basic_rsimp_SEQ_property1) |
|
890 apply (simp add: idem_after_simp1) |
|
891 apply(case_tac "rsimp r1 = RZERO") |
|
892 |
|
893 using basic_regex_property1 apply blast |
|
894 apply(case_tac "rsimp r2 = RZERO") |
|
895 |
|
896 apply (simp add: basic_rsimp_SEQ_property3) |
|
897 apply(subst idiot2) |
|
898 apply simp+ |
|
899 apply(subgoal_tac "rnullable (rsimp r1)") |
|
900 apply simp |
|
901 using rsimp_idem apply presburger |
|
902 using der_simp_nullability by presburger |
|
903 |
|
608 |
904 |
609 |
905 |
610 lemma grewrite_ralts: |
906 lemma grewrite_ralts: |
611 shows "rs \<leadsto>g rs' \<Longrightarrow> RALTS rs h\<leadsto>* RALTS rs'" |
907 shows "rs \<leadsto>g rs' \<Longrightarrow> RALTS rs h\<leadsto>* RALTS rs'" |
612 by (smt (verit) grewrite_cases_middle hr_in_rstar hrewrite.intros(11) hrewrite.intros(7) hrewrite.intros(8)) |
908 by (smt (verit) grewrite_cases_middle hr_in_rstar hrewrite.intros(11) hrewrite.intros(7) hrewrite.intros(8)) |
752 apply(subgoal_tac "RALTS (map rsimp x) h\<leadsto>* rsimp_ALTs (rdistinct (rflts (map rsimp x)) {}) ") |
1048 apply(subgoal_tac "RALTS (map rsimp x) h\<leadsto>* rsimp_ALTs (rdistinct (rflts (map rsimp x)) {}) ") |
753 using hreal_trans apply blast |
1049 using hreal_trans apply blast |
754 apply (meson flts_gstar greal_trans grewrites_ralts_rsimpalts gstar_rdistinct) |
1050 apply (meson flts_gstar greal_trans grewrites_ralts_rsimpalts gstar_rdistinct) |
755 |
1051 |
756 apply (simp add: grewrites_ralts hrewrites_list) |
1052 apply (simp add: grewrites_ralts hrewrites_list) |
757 by simp |
1053 by simp_all |
758 |
1054 |
759 lemma interleave_aux1: |
1055 lemma interleave_aux1: |
760 shows " RALT (RSEQ RZERO r1) r h\<leadsto>* r" |
1056 shows " RALT (RSEQ RZERO r1) r h\<leadsto>* r" |
761 apply(subgoal_tac "RSEQ RZERO r1 h\<leadsto>* RZERO") |
1057 apply(subgoal_tac "RSEQ RZERO r1 h\<leadsto>* RZERO") |
762 apply(subgoal_tac "RALT (RSEQ RZERO r1) r h\<leadsto>* RALT RZERO r") |
1058 apply(subgoal_tac "RALT (RSEQ RZERO r1) r h\<leadsto>* RALT RZERO r") |
813 apply simp |
1109 apply simp |
814 by (meson hreal_trans interleave1) |
1110 by (meson hreal_trans interleave1) |
815 |
1111 |
816 |
1112 |
817 |
1113 |
818 lemma inside_simp_seq_nullable: |
|
819 shows |
|
820 "\<And>r1 r2. |
|
821 \<lbrakk>rsimp (rder x (rsimp r1)) = rsimp (rder x r1); rsimp (rder x (rsimp r2)) = rsimp (rder x r2); |
|
822 rnullable r1\<rbrakk> |
|
823 \<Longrightarrow> rsimp (rder x (rsimp_SEQ (rsimp r1) (rsimp r2))) = |
|
824 rsimp_ALTs (rdistinct (rflts [rsimp_SEQ (rsimp (rder x r1)) (rsimp r2), rsimp (rder x r2)]) {})" |
|
825 apply(case_tac "rsimp r1 = RONE") |
|
826 apply(simp) |
|
827 apply(subst basic_rsimp_SEQ_property1) |
|
828 apply (simp add: idem_after_simp1) |
|
829 apply(case_tac "rsimp r1 = RZERO") |
|
830 using basic_regex_property1 apply blast |
|
831 apply(case_tac "rsimp r2 = RZERO") |
|
832 apply (simp add: basic_rsimp_SEQ_property3) |
|
833 apply(subst idiot2) |
|
834 apply simp+ |
|
835 apply(subgoal_tac "rnullable (rsimp r1)") |
|
836 apply simp |
|
837 using rsimp_idem apply presburger |
|
838 using der_simp_nullability by presburger |
|
839 |
|
840 |
|
841 |
|
842 lemma inside_simp_removal: |
1114 lemma inside_simp_removal: |
843 shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)" |
1115 shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)" |
844 apply(induct r) |
1116 apply(induct r) |
845 apply simp+ |
1117 apply simp+ |
846 apply(case_tac "rnullable r1") |
1118 apply(case_tac "rnullable r1") |
850 apply simp |
1122 apply simp |
851 apply (smt (verit, del_insts) idiot2 basic_rsimp_SEQ_property3 der_simp_nullability rder.simps(1) rder.simps(5) rnullable.simps(2) rsimp.simps(1) rsimp_SEQ.simps(1) rsimp_idem) |
1123 apply (smt (verit, del_insts) idiot2 basic_rsimp_SEQ_property3 der_simp_nullability rder.simps(1) rder.simps(5) rnullable.simps(2) rsimp.simps(1) rsimp_SEQ.simps(1) rsimp_idem) |
852 apply(subgoal_tac "rder x (RALTS xa) h\<leadsto>* rder x (rsimp (RALTS xa))") |
1124 apply(subgoal_tac "rder x (RALTS xa) h\<leadsto>* rder x (rsimp (RALTS xa))") |
853 using hrewrites_simpeq apply presburger |
1125 using hrewrites_simpeq apply presburger |
854 using interleave_star1 simp_hrewrites apply presburger |
1126 using interleave_star1 simp_hrewrites apply presburger |
855 by simp |
1127 by simp_all |
856 |
1128 |
857 |
1129 |
858 |
1130 |
859 |
1131 |
860 lemma rders_simp_same_simpders: |
1132 lemma rders_simp_same_simpders: |
885 lemma rders_simp_nonempty_simped: |
1157 lemma rders_simp_nonempty_simped: |
886 shows "xs \<noteq> [] \<Longrightarrow> rsimp \<circ> (\<lambda>r. rders_simp r xs) = (\<lambda>r. rders_simp r xs)" |
1158 shows "xs \<noteq> [] \<Longrightarrow> rsimp \<circ> (\<lambda>r. rders_simp r xs) = (\<lambda>r. rders_simp r xs)" |
887 using rders_simp_same_simpders rsimp_idem by auto |
1159 using rders_simp_same_simpders rsimp_idem by auto |
888 |
1160 |
889 lemma repeated_altssimp: |
1161 lemma repeated_altssimp: |
890 shows "\<forall>r \<in> set rs. rsimp r = r \<Longrightarrow> |
1162 shows "\<forall>r \<in> set rs. rsimp r = r \<Longrightarrow> rsimp (rsimp_ALTs (rdistinct (rflts rs) {})) = |
891 rsimp (rsimp_ALTs (rdistinct (rflts rs) {})) = |
|
892 rsimp_ALTs (rdistinct (rflts rs) {})" |
1163 rsimp_ALTs (rdistinct (rflts rs) {})" |
893 by (metis map_idI rsimp.simps(2) rsimp_idem) |
1164 by (metis map_idI rsimp.simps(2) rsimp_idem) |
894 |
1165 |
895 |
1166 |
896 |
1167 |
897 lemma alts_closed_form: |
1168 lemma alts_closed_form: |
898 shows "rsimp (rders_simp (RALTS rs) s) = |
1169 shows "rsimp (rders_simp (RALTS rs) s) = rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))" |
899 rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))" |
|
900 apply(induct s rule: rev_induct) |
1170 apply(induct s rule: rev_induct) |
901 apply simp |
1171 apply simp |
902 apply simp |
1172 apply simp |
903 apply(subst rders_simp_append) |
1173 apply(subst rders_simp_append) |
904 apply(subgoal_tac " rsimp (rders_simp (rders_simp (RALTS rs) xs) [x]) = |
1174 apply(subgoal_tac " rsimp (rders_simp (rders_simp (RALTS rs) xs) [x]) = |
979 shows "created_by_seq r \<Longrightarrow> created_by_seq (rder c r)" |
1249 shows "created_by_seq r \<Longrightarrow> created_by_seq (rder c r)" |
980 apply(induct r) |
1250 apply(induct r) |
981 apply simp+ |
1251 apply simp+ |
982 |
1252 |
983 using created_by_seq.cases apply blast |
1253 using created_by_seq.cases apply blast |
984 |
1254 apply(auto) |
985 apply (meson created_by_seq.cases rrexp.distinct(19) rrexp.distinct(21)) |
1255 apply (meson created_by_seq.cases rrexp.distinct(23) rrexp.distinct(25)) |
986 apply (metis created_by_seq.simps rder.simps(5)) |
1256 using created_by_seq.simps apply blast |
987 apply (smt (verit, ccfv_threshold) created_by_seq.simps list.set_intros(1) list.simps(8) list.simps(9) rder.simps(4) rrexp.distinct(25) rrexp.inject(3)) |
1257 apply (meson created_by_seq.simps) |
988 using created_by_seq.intros(1) by force |
1258 using created_by_seq.intros(1) apply blast |
1259 apply (metis (no_types, lifting) created_by_seq.simps k0a list.set_intros(1) list.simps(8) list.simps(9) rrexp.distinct(31)) |
|
1260 apply (simp add: created_by_seq.intros(1)) |
|
1261 using created_by_seq.simps apply blast |
|
1262 by (simp add: created_by_seq.intros(1)) |
|
989 |
1263 |
990 lemma createdbyseq_left_creatable: |
1264 lemma createdbyseq_left_creatable: |
991 shows "created_by_seq (RALT r1 r2) \<Longrightarrow> created_by_seq r1" |
1265 shows "created_by_seq (RALT r1 r2) \<Longrightarrow> created_by_seq r1" |
992 using created_by_seq.cases by blast |
1266 using created_by_seq.cases by blast |
993 |
1267 |
1028 apply(induction r rule: created_by_seq.induct) |
1302 apply(induction r rule: created_by_seq.induct) |
1029 apply simp |
1303 apply simp |
1030 by fastforce |
1304 by fastforce |
1031 |
1305 |
1032 |
1306 |
1033 fun vsuf :: "char list \<Rightarrow> rrexp \<Rightarrow> char list list" where |
|
1034 "vsuf [] _ = []" |
|
1035 |"vsuf (c#cs) r1 = (if (rnullable r1) then (vsuf cs (rder c r1)) @ [c # cs] |
|
1036 else (vsuf cs (rder c r1)) |
|
1037 ) " |
|
1038 |
|
1039 |
|
1040 |
|
1041 |
|
1042 |
|
1043 lemma vsuf_prop1: |
1307 lemma vsuf_prop1: |
1044 shows "vsuf (xs @ [x]) r = (if (rnullable (rders r xs)) |
1308 shows "vsuf (xs @ [x]) r = (if (rnullable (rders r xs)) |
1045 then [x] # (map (\<lambda>s. s @ [x]) (vsuf xs r) ) |
1309 then [x] # (map (\<lambda>s. s @ [x]) (vsuf xs r) ) |
1046 else (map (\<lambda>s. s @ [x]) (vsuf xs r)) ) |
1310 else (map (\<lambda>s. s @ [x]) (vsuf xs r)) ) |
1047 " |
1311 " |
1069 \<Longrightarrow> map (rder x \<circ> rders r2) (vsuf xs r1) = map (rders r2) (vsuf (xs @ [x]) r1)" |
1333 \<Longrightarrow> map (rder x \<circ> rders r2) (vsuf xs r1) = map (rders r2) (vsuf (xs @ [x]) r1)" |
1070 apply(subst vsuf_prop1) |
1334 apply(subst vsuf_prop1) |
1071 apply simp |
1335 apply simp |
1072 by (simp add: rders_append) |
1336 by (simp add: rders_append) |
1073 |
1337 |
1074 thm sfau_idem_der |
1338 |
1075 |
|
1076 lemma oneCharvsuf: |
|
1077 shows "breakHead [rder x (RSEQ r1 r2)] = RSEQ (rder x r1) r2 # map (rders r2) (vsuf [x] r1)" |
|
1078 by simp |
|
1079 |
|
1080 |
|
1081 lemma vsuf_compose2: |
|
1082 shows "(map (rders r2) (vsuf [x] (rders r1 xs))) @ map (rder x) (map (rders r2) (vsuf xs r1)) = |
|
1083 map (rders r2) (vsuf (xs @ [x]) r1)" |
|
1084 proof(induct xs arbitrary: r1) |
|
1085 case Nil |
|
1086 then show ?case |
|
1087 by simp |
|
1088 next |
|
1089 case (Cons a xs) |
|
1090 have "rnullable (rders r1 xs) \<longrightarrow> map (rders r2) (vsuf [x] (rders r1 (a # xs))) @ map (rder x) (map (rders r2) (vsuf (a # xs) r1)) = |
|
1091 map (rders r2) (vsuf ((a # xs) @ [x]) r1)" |
|
1092 proof |
|
1093 assume nullableCond: "rnullable (rders r1 xs)" |
|
1094 have "rnullable r1 \<longrightarrow> rder x (rders (rder a r2) xs) = rders (rder a r2) (xs @ [x])" |
|
1095 by (simp add: rders_append) |
|
1096 show " map (rders r2) (vsuf [x] (rders r1 (a # xs))) @ map (rder x) (map (rders r2) (vsuf (a # xs) r1)) = |
|
1097 map (rders r2) (vsuf ((a # xs) @ [x]) r1)" |
|
1098 using \<open>rnullable r1 \<longrightarrow> rder x (rders (rder a r2) xs) = rders (rder a r2) (xs @ [x])\<close> local.Cons by auto |
|
1099 qed |
|
1100 then have "\<not> rnullable (rders r1 xs) \<longrightarrow> map (rders r2) (vsuf [x] (rders r1 (a # xs))) @ map (rder x) (map (rders r2) (vsuf (a # xs) r1)) = |
|
1101 map (rders r2) (vsuf ((a # xs) @ [x]) r1)" |
|
1102 apply simp |
|
1103 by (smt (verit, ccfv_threshold) append_Cons append_Nil list.map_comp list.simps(8) list.simps(9) local.Cons rders.simps(1) rders.simps(2) rders_append vsuf.simps(1) vsuf.simps(2)) |
|
1104 then show ?case |
|
1105 using \<open>rnullable (rders r1 xs) \<longrightarrow> map (rders r2) (vsuf [x] (rders r1 (a # xs))) @ map (rder x) (map (rders r2) (vsuf (a # xs) r1)) = map (rders r2) (vsuf ((a # xs) @ [x]) r1)\<close> by blast |
|
1106 qed |
|
1107 |
1339 |
1108 |
1340 |
1109 lemma seq_sfau0: |
1341 lemma seq_sfau0: |
1110 shows "sflat_aux (rders (RSEQ r1 r2) s) = (RSEQ (rders r1 s) r2) # |
1342 shows "sflat_aux (rders (RSEQ r1 r2) s) = (RSEQ (rders r1 s) r2) # |
1111 (map (rders r2) (vsuf s r1)) " |
1343 (map (rders r2) (vsuf s r1)) " |
1112 proof(induct s rule: rev_induct) |
1344 apply(induct s rule: rev_induct) |
1113 case Nil |
1345 apply simp |
1114 then show ?case |
1346 apply(subst rders_append)+ |
1115 by simp |
1347 apply(subgoal_tac "created_by_seq (rders (RSEQ r1 r2) xs)") |
1116 next |
1348 prefer 2 |
1117 case (snoc x xs) |
1349 using recursively_derseq1 apply blast |
1118 then have LHS1:"sflat_aux (rders (RSEQ r1 r2) (xs @ [x])) = sflat_aux (rder x (rders (RSEQ r1 r2) xs)) " |
1350 apply simp |
1119 by (simp add: rders_append) |
1351 apply(subst sfau_idem_der) |
1120 then have LHS1A: "... = breakHead (map (rder x) (sflat_aux (rders (RSEQ r1 r2) xs)))" |
1352 |
1121 using recursively_derseq sfau_idem_der by auto |
1353 apply blast |
1122 then have LHS1B: "... = breakHead (map (rder x) (RSEQ (rders r1 xs) r2 # map (rders r2) (vsuf xs r1)))" |
1354 apply(case_tac "rnullable (rders r1 xs)") |
1123 using snoc by auto |
1355 apply simp |
1124 then have LHS1C: "... = breakHead (rder x (RSEQ (rders r1 xs) r2) # map (rder x) (map (rders r2) (vsuf xs r1)))" |
1356 apply(subst vsuf_prop1) |
1125 by simp |
1357 apply simp |
1126 then have LHS1D: "... = breakHead [rder x (RSEQ (rders r1 xs) r2)] @ map (rder x) (map (rders r2) (vsuf xs r1))" |
1358 apply (simp add: rders_append) |
1127 by simp |
1359 apply simp |
1128 then have LHS1E: "... = RSEQ (rder x (rders r1 xs)) r2 # (map (rders r2) (vsuf [x] (rders r1 xs))) @ map (rder x) (map (rders r2) (vsuf xs r1))" |
1360 using vsuf_compose1 by blast |
1129 by force |
1361 |
1130 then have LHS1F: "... = RSEQ (rder x (rders r1 xs)) r2 # (map (rders r2) (vsuf (xs @ [x]) r1))" |
1362 |
1131 using vsuf_compose2 by blast |
1363 |
1132 then have LHS1G: "... = RSEQ (rders r1 (xs @ [x])) r2 # (map (rders r2) (vsuf (xs @ [x]) r1))" |
1364 |
1133 using rders.simps(1) rders.simps(2) rders_append by presburger |
1365 |
1134 then show ?case |
1366 |
1135 using LHS1 LHS1A LHS1C LHS1D LHS1E LHS1F snoc by presburger |
1367 |
1136 qed |
1368 |
1137 |
1369 |
1370 thm sflat.elims |
|
1138 |
1371 |
1139 |
1372 |
1140 |
1373 |
1141 |
1374 |
1142 |
1375 |
1223 |
1456 |
1224 |
1457 |
1225 lemma seq_closed_form_variant: |
1458 lemma seq_closed_form_variant: |
1226 assumes "s \<noteq> []" |
1459 assumes "s \<noteq> []" |
1227 shows "rders_simp (RSEQ r1 r2) s = |
1460 shows "rders_simp (RSEQ r1 r2) s = |
1228 rsimp (RALTS (RSEQ (rders_simp r1 s) r2 # |
1461 rsimp (RALTS (RSEQ (rders_simp r1 s) r2 # (map (rders_simp r2) (vsuf s r1))))" |
1229 (map (rders_simp r2) (vsuf s r1))))" |
|
1230 using assms q seq_closed_form by force |
1462 using assms q seq_closed_form by force |
1231 |
1463 |
1232 |
1464 |
1233 fun hflat_aux :: "rrexp \<Rightarrow> rrexp list" where |
1465 fun hflat_aux :: "rrexp \<Rightarrow> rrexp list" where |
1234 "hflat_aux (RALT r1 r2) = hflat_aux r1 @ hflat_aux r2" |
1466 "hflat_aux (RALT r1 r2) = hflat_aux r1 @ hflat_aux r2" |
1241 |
1473 |
1242 inductive created_by_star :: "rrexp \<Rightarrow> bool" where |
1474 inductive created_by_star :: "rrexp \<Rightarrow> bool" where |
1243 "created_by_star (RSEQ ra (RSTAR rb))" |
1475 "created_by_star (RSEQ ra (RSTAR rb))" |
1244 | "\<lbrakk>created_by_star r1; created_by_star r2\<rbrakk> \<Longrightarrow> created_by_star (RALT r1 r2)" |
1476 | "\<lbrakk>created_by_star r1; created_by_star r2\<rbrakk> \<Longrightarrow> created_by_star (RALT r1 r2)" |
1245 |
1477 |
1246 |
1478 fun hElem :: "rrexp \<Rightarrow> rrexp list" where |
1247 |
1479 "hElem (RALT r1 r2) = (hElem r1 ) @ (hElem r2)" |
1248 fun star_update :: "char \<Rightarrow> rrexp \<Rightarrow> char list list \<Rightarrow> char list list" where |
1480 | "hElem r = [r]" |
1249 "star_update c r [] = []" |
|
1250 |"star_update c r (s # Ss) = (if (rnullable (rders r s)) |
|
1251 then (s@[c]) # [c] # (star_update c r Ss) |
|
1252 else (s@[c]) # (star_update c r Ss) )" |
|
1253 |
|
1254 |
|
1255 fun star_updates :: "char list \<Rightarrow> rrexp \<Rightarrow> char list list \<Rightarrow> char list list" |
|
1256 where |
|
1257 "star_updates [] r Ss = Ss" |
|
1258 | "star_updates (c # cs) r Ss = star_updates cs r (star_update c r Ss)" |
|
1259 |
|
1260 |
1481 |
1261 |
1482 |
1262 lemma cbs_ders_cbs: |
1483 lemma cbs_ders_cbs: |
1263 shows "created_by_star r \<Longrightarrow> created_by_star (rder c r)" |
1484 shows "created_by_star r \<Longrightarrow> created_by_star (rder c r)" |
1264 apply(induct r rule: created_by_star.induct) |
1485 apply(induct r rule: created_by_star.induct) |
1275 apply simp |
1496 apply simp |
1276 using cbs_ders_cbs by auto |
1497 using cbs_ders_cbs by auto |
1277 |
1498 |
1278 |
1499 |
1279 |
1500 |
1280 |
|
1281 lemma hfau_pushin: |
1501 lemma hfau_pushin: |
1282 shows "created_by_star r \<Longrightarrow> hflat_aux (rder c r) = concat (map hflat_aux (map (rder c) (hflat_aux r)))" |
1502 shows "created_by_star r \<Longrightarrow> hflat_aux (rder c r) = concat (map hElem (map (rder c) (hflat_aux r)))" |
1283 proof(induct r rule: created_by_star.induct) |
1503 apply(induct r rule: created_by_star.induct) |
1284 case (1 ra rb) |
1504 apply simp |
1285 then show ?case by simp |
1505 apply(subgoal_tac "created_by_star (rder c r1)") |
1286 next |
1506 prefer 2 |
1287 case (2 r1 r2) |
1507 apply(subgoal_tac "created_by_star (rder c r2)") |
1288 then have "created_by_star (rder c r1)" |
1508 using cbs_ders_cbs apply blast |
1289 using cbs_ders_cbs by blast |
1509 using cbs_ders_cbs apply auto[1] |
1290 then have "created_by_star (rder c r2)" |
|
1291 using "2.hyps"(3) cbs_ders_cbs by auto |
|
1292 then show ?case |
|
1293 by (simp add: "2.hyps"(2) "2.hyps"(4)) |
|
1294 qed |
|
1295 |
|
1296 (*AALTS [a\x . b.c, b\x .c, c \x]*) |
|
1297 (*AALTS [a\x . b.c, AALTS [b\x .c, c\x]]*) |
|
1298 |
|
1299 lemma stupdates_append: shows |
|
1300 "star_updates (s @ [c]) r Ss = star_update c r (star_updates s r Ss)" |
|
1301 apply(induct s arbitrary: Ss) |
|
1302 apply simp |
|
1303 apply simp |
1510 apply simp |
1304 done |
1511 done |
1305 |
1512 |
1306 |
|
1307 |
|
1308 |
|
1309 |
|
1310 lemma stupdate_induct1: |
1513 lemma stupdate_induct1: |
1311 shows " concat (map (hflat_aux \<circ> (rder x \<circ> (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)))) Ss) = |
1514 shows " concat (map (hElem \<circ> (rder x \<circ> (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)))) Ss) = |
1312 map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_update x r0 Ss)" |
1515 map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_update x r0 Ss)" |
1313 apply(induct Ss) |
1516 apply(induct Ss) |
1314 apply simp+ |
1517 apply simp+ |
1315 by (simp add: rders_append) |
1518 by (simp add: rders_append) |
1316 |
1519 |
1317 |
1520 |
1318 |
1521 |
1319 lemma stupdates_join_general: |
1522 lemma stupdates_join_general: |
1320 shows "concat |
1523 shows "concat (map hElem (map (rder x) (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates xs r0 Ss)))) = |
1321 (map hflat_aux (map (rder x) |
1524 map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates (xs @ [x]) r0 Ss)" |
1322 (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates xs r0 Ss))) |
|
1323 ) = |
|
1324 map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates (xs @ [x]) r0 Ss)" |
|
1325 apply(induct xs arbitrary: Ss) |
1525 apply(induct xs arbitrary: Ss) |
1326 apply (simp) |
1526 apply (simp) |
1327 prefer 2 |
1527 prefer 2 |
1328 apply auto[1] |
1528 apply auto[1] |
1329 using stupdate_induct1 by blast |
1529 using stupdate_induct1 by blast |
1339 apply(subgoal_tac "created_by_star (rders (RSEQ (rder c r0) (RSTAR r0)) xs)") |
1539 apply(subgoal_tac "created_by_star (rders (RSEQ (rder c r0) (RSTAR r0)) xs)") |
1340 prefer 2 |
1540 prefer 2 |
1341 apply (simp add: star_ders_cbs) |
1541 apply (simp add: star_ders_cbs) |
1342 apply(subst hfau_pushin) |
1542 apply(subst hfau_pushin) |
1343 apply simp |
1543 apply simp |
1344 apply(subgoal_tac "concat (map hflat_aux (map (rder x) (hflat_aux (rders (RSEQ (rder c r0) (RSTAR r0)) xs)))) = |
1544 apply(subgoal_tac "concat (map hElem (map (rder x) (hflat_aux (rders (RSEQ (rder c r0) (RSTAR r0)) xs)))) = |
1345 concat (map hflat_aux (map (rder x) ( map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates xs r0 [[c]])))) ") |
1545 concat (map hElem (map (rder x) ( map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_updates xs r0 [[c]])))) ") |
1346 apply(simp only:) |
1546 apply(simp only:) |
1347 prefer 2 |
1547 prefer 2 |
1348 apply presburger |
1548 apply presburger |
1349 apply(subst stupdates_append[symmetric]) |
1549 apply(subst stupdates_append[symmetric]) |
1350 using stupdates_join_general by blast |
1550 using stupdates_join_general by blast |
1551 |
|
1552 |
|
1351 |
1553 |
1352 lemma starders_hfau_also1: |
1554 lemma starders_hfau_also1: |
1353 shows "hflat_aux (rders (RSTAR r) (c # xs)) = map (\<lambda>s1. RSEQ (rders r s1) (RSTAR r)) (star_updates xs r [[c]])" |
1555 shows "hflat_aux (rders (RSTAR r) (c # xs)) = map (\<lambda>s1. RSEQ (rders r s1) (RSTAR r)) (star_updates xs r [[c]])" |
1354 using star_hfau_induct by force |
1556 using star_hfau_induct by force |
1355 |
1557 |
1364 apply (metis append.right_neutral append_Cons append_eq_append_conv2 grewrites.simps hflat_aux.simps(7) same_append_eq) |
1566 apply (metis append.right_neutral append_Cons append_eq_append_conv2 grewrites.simps hflat_aux.simps(7) same_append_eq) |
1365 apply(case_tac lista) |
1567 apply(case_tac lista) |
1366 apply simp |
1568 apply simp |
1367 apply (metis (no_types, lifting) append_Cons append_eq_append_conv2 gmany_steps_later greal_trans grewrite.intros(2) grewrites_append self_append_conv) |
1569 apply (metis (no_types, lifting) append_Cons append_eq_append_conv2 gmany_steps_later greal_trans grewrite.intros(2) grewrites_append self_append_conv) |
1368 apply simp |
1570 apply simp |
1369 by simp |
1571 by simp_all |
1370 |
1572 |
1371 |
1573 |
1372 |
1574 |
1373 |
1575 |
1374 lemma cbs_hfau_rsimpeq1: |
1576 lemma cbs_hfau_rsimpeq1: |
1378 by (metis append.right_neutral greal_trans grewrites_cons hflat_aux_grewrites) |
1580 by (metis append.right_neutral greal_trans grewrites_cons hflat_aux_grewrites) |
1379 |
1581 |
1380 |
1582 |
1381 lemma hfau_rsimpeq2: |
1583 lemma hfau_rsimpeq2: |
1382 shows "created_by_star r \<Longrightarrow> rsimp r = rsimp ( (RALTS (hflat_aux r)))" |
1584 shows "created_by_star r \<Longrightarrow> rsimp r = rsimp ( (RALTS (hflat_aux r)))" |
1383 apply(induct rule: created_by_star.induct) |
1585 apply(induct r) |
1384 apply simp |
1586 apply simp+ |
1385 apply (metis rsimp.simps(6) rsimp_seq_equal1) |
1587 |
1386 using cbs_hfau_rsimpeq1 hflat_aux.simps(1) by presburger |
1588 apply (metis rsimp_seq_equal1) |
1589 prefer 2 |
|
1590 apply simp |
|
1591 apply(case_tac x) |
|
1592 apply simp |
|
1593 apply(case_tac "list") |
|
1594 apply simp |
|
1595 |
|
1596 apply (metis idem_after_simp1) |
|
1597 apply(case_tac "lista") |
|
1598 prefer 2 |
|
1599 apply (metis hflat_aux.simps(8) idem_after_simp1 list.simps(8) list.simps(9) rsimp.simps(2)) |
|
1600 apply(subgoal_tac "rsimp (RALT a aa) = rsimp (RALTS (hflat_aux (RALT a aa)))") |
|
1601 apply simp |
|
1602 apply(subgoal_tac "rsimp (RALT a aa) = rsimp (RALTS (hflat_aux a @ hflat_aux aa))") |
|
1603 using hflat_aux.simps(1) apply presburger |
|
1604 apply simp |
|
1605 using cbs_hfau_rsimpeq1 apply(fastforce) |
|
1606 by simp |
|
1607 |
|
1387 |
1608 |
1388 lemma star_closed_form1: |
1609 lemma star_closed_form1: |
1389 shows "rsimp (rders (RSTAR r0) (c#s)) = |
1610 shows "rsimp (rders (RSTAR r0) (c#s)) = |
1390 rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))" |
1611 rsimp ( ( RALTS ( (map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) )))" |
1391 using hfau_rsimpeq2 rder.simps(6) rders.simps(2) star_ders_cbs starders_hfau_also1 by presburger |
1612 using hfau_rsimpeq2 rder.simps(6) rders.simps(2) star_ders_cbs starders_hfau_also1 by presburger |
1425 apply(subgoal_tac " map (\<lambda>s1. (RSEQ (rsimp (rders r0 s1)) (RSTAR r0)) ) Ss scf\<leadsto>* |
1646 apply(subgoal_tac " map (\<lambda>s1. (RSEQ (rsimp (rders r0 s1)) (RSTAR r0)) ) Ss scf\<leadsto>* |
1426 map (\<lambda>s1. rsimp (RSEQ (rders r0 s1) (RSTAR r0)) ) Ss ") |
1647 map (\<lambda>s1. rsimp (RSEQ (rders r0 s1) (RSTAR r0)) ) Ss ") |
1427 using hrewrites_simpeq srewritescf_alt1 apply fastforce |
1648 using hrewrites_simpeq srewritescf_alt1 apply fastforce |
1428 using star_closed_form6_hrewrites by blast |
1649 using star_closed_form6_hrewrites by blast |
1429 |
1650 |
1651 |
|
1652 |
|
1653 |
|
1430 lemma stupdate_nonempty: |
1654 lemma stupdate_nonempty: |
1431 shows "\<forall>s \<in> set Ss. s \<noteq> [] \<Longrightarrow> \<forall>s \<in> set (star_update c r Ss). s \<noteq> []" |
1655 shows "\<forall>s \<in> set Ss. s \<noteq> [] \<Longrightarrow> \<forall>s \<in> set (star_update c r Ss). s \<noteq> []" |
1432 apply(induct Ss) |
1656 apply(induct Ss) |
1433 apply simp |
1657 apply simp |
1434 apply(case_tac "rnullable (rders r a)") |
1658 apply(case_tac "rnullable (rders r a)") |
1435 apply simp+ |
1659 apply simp+ |
1436 done |
1660 done |
1452 |
1676 |
1453 |
1677 |
1454 lemma star_closed_form: |
1678 lemma star_closed_form: |
1455 shows "rders_simp (RSTAR r0) (c#s) = |
1679 shows "rders_simp (RSTAR r0) (c#s) = |
1456 rsimp ( RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) ))" |
1680 rsimp ( RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) (star_updates s r0 [[c]]) ) ))" |
1457 apply(induct s) |
1681 apply(case_tac s) |
1458 apply simp |
1682 apply simp |
1459 apply (metis idem_after_simp1 rsimp.simps(1) rsimp.simps(6) rsimp_idem) |
1683 apply (metis idem_after_simp1 rsimp.simps(1) rsimp.simps(6) rsimp_idem) |
1460 using star_closed_form4 star_closed_form5 star_closed_form6 star_closed_form8 by presburger |
1684 using star_closed_form4 star_closed_form5 star_closed_form6 star_closed_form8 by presburger |
1461 |
1685 |
1462 |
1686 |
1463 unused_thms |
1687 |
1464 |
1688 |
1689 fun nupdate :: "char \<Rightarrow> rrexp \<Rightarrow> (string * nat) option list \<Rightarrow> (string * nat) option list" where |
|
1690 "nupdate c r [] = []" |
|
1691 | "nupdate c r (Some (s, Suc n) # Ss) = (if (rnullable (rders r s)) |
|
1692 then Some (s@[c], Suc n) # Some ([c], n) # (nupdate c r Ss) |
|
1693 else Some ((s@[c]), Suc n) # (nupdate c r Ss) |
|
1694 )" |
|
1695 | "nupdate c r (Some (s, 0) # Ss) = (if (rnullable (rders r s)) |
|
1696 then Some (s@[c], 0) # None # (nupdate c r Ss) |
|
1697 else Some ((s@[c]), 0) # (nupdate c r Ss) |
|
1698 ) " |
|
1699 | "nupdate c r (None # Ss) = (None # nupdate c r Ss)" |
|
1700 |
|
1701 |
|
1702 fun nupdates :: "char list \<Rightarrow> rrexp \<Rightarrow> (string * nat) option list \<Rightarrow> (string * nat) option list" |
|
1703 where |
|
1704 "nupdates [] r Ss = Ss" |
|
1705 | "nupdates (c # cs) r Ss = nupdates cs r (nupdate c r Ss)" |
|
1706 |
|
1707 fun ntset :: "rrexp \<Rightarrow> nat \<Rightarrow> string \<Rightarrow> (string * nat) option list" where |
|
1708 "ntset r (Suc n) (c # cs) = nupdates cs r [Some ([c], n)]" |
|
1709 | "ntset r 0 _ = [None]" |
|
1710 | "ntset r _ [] = []" |
|
1711 |
|
1712 inductive created_by_ntimes :: "rrexp \<Rightarrow> bool" where |
|
1713 "created_by_ntimes RZERO" |
|
1714 | "created_by_ntimes (RSEQ ra (RNTIMES rb n))" |
|
1715 | "\<lbrakk>created_by_ntimes r1; created_by_ntimes r2\<rbrakk> \<Longrightarrow> created_by_ntimes (RALT r1 r2)" |
|
1716 | "\<lbrakk>created_by_ntimes r \<rbrakk> \<Longrightarrow> created_by_ntimes (RALT r RZERO)" |
|
1717 |
|
1718 fun highest_power_aux :: "(string * nat) option list \<Rightarrow> nat \<Rightarrow> nat" where |
|
1719 "highest_power_aux [] n = n" |
|
1720 | "highest_power_aux (None # rs) n = highest_power_aux rs n" |
|
1721 | "highest_power_aux (Some (s, n) # rs) m = highest_power_aux rs (max n m)" |
|
1722 |
|
1723 fun hpower :: "(string * nat) option list \<Rightarrow> nat" where |
|
1724 "hpower rs = highest_power_aux rs 0" |
|
1725 |
|
1726 |
|
1727 lemma nupdate_mono: |
|
1728 shows " (highest_power_aux (nupdate c r optlist) m) \<le> (highest_power_aux optlist m)" |
|
1729 apply(induct optlist arbitrary: m) |
|
1730 apply simp |
|
1731 apply(case_tac a) |
|
1732 apply simp |
|
1733 apply(case_tac aa) |
|
1734 apply(case_tac b) |
|
1735 apply simp+ |
|
1736 done |
|
1737 |
|
1738 lemma nupdate_mono1: |
|
1739 shows "hpower (nupdate c r optlist) \<le> hpower optlist" |
|
1740 by (simp add: nupdate_mono) |
|
1741 |
|
1742 |
|
1743 |
|
1744 lemma cbn_ders_cbn: |
|
1745 shows "created_by_ntimes r \<Longrightarrow> created_by_ntimes (rder c r)" |
|
1746 apply(induct r rule: created_by_ntimes.induct) |
|
1747 apply simp |
|
1748 |
|
1749 using created_by_ntimes.intros(1) created_by_ntimes.intros(2) created_by_ntimes.intros(3) apply presburger |
|
1750 |
|
1751 apply (metis created_by_ntimes.simps rder.simps(5) rder.simps(7)) |
|
1752 using created_by_star.intros(1) created_by_star.intros(2) apply auto[1] |
|
1753 using created_by_ntimes.intros(1) created_by_ntimes.intros(3) apply auto[1] |
|
1754 by (metis (mono_tags, lifting) created_by_ntimes.simps list.simps(8) list.simps(9) rder.simps(1) rder.simps(4)) |
|
1755 |
|
1756 lemma ntimes_ders_cbn: |
|
1757 shows "created_by_ntimes (rders (RSEQ r' (RNTIMES r n)) s)" |
|
1758 apply(induct s rule: rev_induct) |
|
1759 apply simp |
|
1760 apply (simp add: created_by_ntimes.intros(2)) |
|
1761 apply(subst rders_append) |
|
1762 using cbn_ders_cbn by auto |
|
1763 |
|
1764 lemma always0: |
|
1765 shows "rders RZERO s = RZERO" |
|
1766 apply(induct s) |
|
1767 by simp+ |
|
1768 |
|
1769 lemma ntimes_ders_cbn1: |
|
1770 shows "created_by_ntimes (rders (RNTIMES r n) (c#s))" |
|
1771 apply(case_tac n) |
|
1772 apply simp |
|
1773 using always0 created_by_ntimes.intros(1) apply auto[1] |
|
1774 by (simp add: ntimes_ders_cbn) |
|
1775 |
|
1776 |
|
1777 lemma ntimes_hfau_pushin: |
|
1778 shows "created_by_ntimes r \<Longrightarrow> hflat_aux (rder c r) = concat (map hflat_aux (map (rder c) (hflat_aux r)))" |
|
1779 apply(induct r rule: created_by_ntimes.induct) |
|
1780 apply simp+ |
|
1781 done |
|
1782 |
|
1783 |
|
1784 abbreviation |
|
1785 "opterm r SN \<equiv> case SN of |
|
1786 Some (s, n) \<Rightarrow> RSEQ (rders r s) (RNTIMES r n) |
|
1787 | None \<Rightarrow> RZERO |
|
1788 |
|
1789 |
|
1790 " |
|
1791 |
|
1792 fun nonempty_string :: "(string * nat) option \<Rightarrow> bool" where |
|
1793 "nonempty_string None = True" |
|
1794 | "nonempty_string (Some ([], n)) = False" |
|
1795 | "nonempty_string (Some (c#s, n)) = True" |
|
1796 |
|
1797 |
|
1798 lemma nupdate_nonempty: |
|
1799 shows "\<lbrakk>\<forall>opt \<in> set Ss. nonempty_string opt \<rbrakk> \<Longrightarrow> \<forall>opt \<in> set (nupdate c r Ss). nonempty_string opt" |
|
1800 apply(induct c r Ss rule: nupdate.induct) |
|
1801 apply(auto) |
|
1802 apply (metis Nil_is_append_conv neq_Nil_conv nonempty_string.simps(3)) |
|
1803 by (metis Nil_is_append_conv neq_Nil_conv nonempty_string.simps(3)) |
|
1804 |
|
1805 |
|
1806 |
|
1807 lemma nupdates_nonempty: |
|
1808 shows "\<lbrakk>\<forall>opt \<in> set Ss. nonempty_string opt \<rbrakk> \<Longrightarrow> \<forall>opt \<in> set (nupdates s r Ss). nonempty_string opt" |
|
1809 apply(induct s arbitrary: Ss) |
|
1810 apply simp |
|
1811 apply simp |
|
1812 using nupdate_nonempty by presburger |
|
1813 |
|
1814 lemma nullability1: shows "rnullable (rders r s) = rnullable (rders_simp r s)" |
|
1815 by (metis der_simp_nullability rders.simps(1) rders_simp.simps(1) rders_simp_same_simpders) |
|
1816 |
|
1817 lemma nupdate_induct1: |
|
1818 shows |
|
1819 "concat (map (hflat_aux \<circ> (rder c \<circ> (opterm r))) sl ) = |
|
1820 map (opterm r) (nupdate c r sl)" |
|
1821 apply(induct sl) |
|
1822 apply simp |
|
1823 apply(simp add: rders_append) |
|
1824 apply(case_tac "a") |
|
1825 apply simp+ |
|
1826 apply(case_tac "aa") |
|
1827 apply(case_tac "b") |
|
1828 apply(case_tac "rnullable (rders r ab)") |
|
1829 apply(subgoal_tac "rnullable (rders_simp r ab)") |
|
1830 apply simp |
|
1831 using rders.simps(1) rders.simps(2) rders_append apply presburger |
|
1832 using nullability1 apply blast |
|
1833 apply simp |
|
1834 using rders.simps(1) rders.simps(2) rders_append apply presburger |
|
1835 apply simp |
|
1836 using rders.simps(1) rders.simps(2) rders_append by presburger |
|
1837 |
|
1838 |
|
1839 lemma nupdates_join_general: |
|
1840 shows "concat (map hflat_aux (map (rder x) (map (opterm r) (nupdates xs r Ss)) )) = |
|
1841 map (opterm r) (nupdates (xs @ [x]) r Ss)" |
|
1842 apply(induct xs arbitrary: Ss) |
|
1843 apply (simp) |
|
1844 prefer 2 |
|
1845 apply auto[1] |
|
1846 using nupdate_induct1 by blast |
|
1847 |
|
1848 |
|
1849 lemma nupdates_join_general1: |
|
1850 shows "concat (map (hflat_aux \<circ> (rder x) \<circ> (opterm r)) (nupdates xs r Ss)) = |
|
1851 map (opterm r) (nupdates (xs @ [x]) r Ss)" |
|
1852 by (metis list.map_comp nupdates_join_general) |
|
1853 |
|
1854 lemma nupdates_append: shows |
|
1855 "nupdates (s @ [c]) r Ss = nupdate c r (nupdates s r Ss)" |
|
1856 apply(induct s arbitrary: Ss) |
|
1857 apply simp |
|
1858 apply simp |
|
1859 done |
|
1860 |
|
1861 lemma nupdates_mono: |
|
1862 shows "highest_power_aux (nupdates s r optlist) m \<le> highest_power_aux optlist m" |
|
1863 apply(induct s rule: rev_induct) |
|
1864 apply simp |
|
1865 apply(subst nupdates_append) |
|
1866 by (meson le_trans nupdate_mono) |
|
1867 |
|
1868 lemma nupdates_mono1: |
|
1869 shows "hpower (nupdates s r optlist) \<le> hpower optlist" |
|
1870 by (simp add: nupdates_mono) |
|
1871 |
|
1872 |
|
1873 (*"\<forall>r \<in> set (nupdates s r [Some ([c], n)]). r = None \<or>( \<exists>s' m. r = Some (s', m) \<and> m \<le> n)"*) |
|
1874 lemma nupdates_mono2: |
|
1875 shows "hpower (nupdates s r [Some ([c], n)]) \<le> n" |
|
1876 by (metis highest_power_aux.simps(1) highest_power_aux.simps(3) hpower.simps max_nat.right_neutral nupdates_mono1) |
|
1877 |
|
1878 lemma hpow_arg_mono: |
|
1879 shows "m \<ge> n \<Longrightarrow> highest_power_aux rs m \<ge> highest_power_aux rs n" |
|
1880 apply(induct rs arbitrary: m n) |
|
1881 apply simp |
|
1882 apply(case_tac a) |
|
1883 apply simp |
|
1884 apply(case_tac aa) |
|
1885 apply simp |
|
1886 done |
|
1887 |
|
1888 |
|
1889 lemma hpow_increase: |
|
1890 shows "highest_power_aux (a # rs') m \<ge> highest_power_aux rs' m" |
|
1891 apply(case_tac a) |
|
1892 apply simp |
|
1893 apply simp |
|
1894 apply(case_tac aa) |
|
1895 apply(case_tac b) |
|
1896 apply simp+ |
|
1897 apply(case_tac "Suc nat > m") |
|
1898 using hpow_arg_mono max.cobounded2 apply blast |
|
1899 using hpow_arg_mono max.cobounded2 by blast |
|
1900 |
|
1901 lemma hpow_append: |
|
1902 shows "highest_power_aux (rsa @ rsb) m = highest_power_aux rsb (highest_power_aux rsa m)" |
|
1903 apply (induct rsa arbitrary: rsb m) |
|
1904 apply simp |
|
1905 apply simp |
|
1906 apply(case_tac a) |
|
1907 apply simp |
|
1908 apply(case_tac aa) |
|
1909 apply simp |
|
1910 done |
|
1911 |
|
1912 lemma hpow_aux_mono: |
|
1913 shows "highest_power_aux (rsa @ rsb) m \<ge> highest_power_aux rsb m" |
|
1914 apply(induct rsa arbitrary: rsb rule: rev_induct) |
|
1915 apply simp |
|
1916 apply simp |
|
1917 using hpow_increase order.trans by blast |
|
1918 |
|
1919 |
|
1920 |
|
1921 |
|
1922 lemma hpow_mono: |
|
1923 shows "hpower (rsa @ rsb) \<le> n \<Longrightarrow> hpower rsb \<le> n" |
|
1924 apply(induct rsb arbitrary: rsa) |
|
1925 apply simp |
|
1926 apply(subgoal_tac "hpower rsb \<le> n") |
|
1927 apply simp |
|
1928 apply (metis dual_order.trans hpow_aux_mono) |
|
1929 by (metis hpow_append hpow_increase hpower.simps nat_le_iff_add trans_le_add1) |
|
1930 |
|
1931 |
|
1932 lemma hpower_rs_elems_aux: |
|
1933 shows "highest_power_aux rs k \<le> n \<Longrightarrow> \<forall>r\<in>set rs. r = None \<or> (\<exists>s' m. r = Some (s', m) \<and> m \<le> n)" |
|
1934 apply(induct rs k arbitrary: n rule: highest_power_aux.induct) |
|
1935 apply(auto) |
|
1936 by (metis dual_order.trans highest_power_aux.simps(1) hpow_append hpow_aux_mono linorder_le_cases max.absorb1 max.absorb2) |
|
1937 |
|
1938 |
|
1939 lemma hpower_rs_elems: |
|
1940 shows "hpower rs \<le> n \<Longrightarrow> \<forall>r \<in> set rs. r = None \<or>( \<exists>s' m. r = Some (s', m) \<and> m \<le> n)" |
|
1941 by (simp add: hpower_rs_elems_aux) |
|
1942 |
|
1943 lemma nupdates_elems_leqn: |
|
1944 shows "\<forall>r \<in> set (nupdates s r [Some ([c], n)]). r = None \<or>( \<exists>s' m. r = Some (s', m) \<and> m \<le> n)" |
|
1945 by (meson hpower_rs_elems nupdates_mono2) |
|
1946 |
|
1947 lemma ntimes_hfau_induct: |
|
1948 shows "hflat_aux (rders (RSEQ (rder c r) (RNTIMES r n)) s) = |
|
1949 map (opterm r) (nupdates s r [Some ([c], n)])" |
|
1950 apply(induct s rule: rev_induct) |
|
1951 apply simp |
|
1952 apply(subst rders_append)+ |
|
1953 apply simp |
|
1954 apply(subst nupdates_append) |
|
1955 apply(subgoal_tac "created_by_ntimes (rders (RSEQ (rder c r) (RNTIMES r n)) xs)") |
|
1956 prefer 2 |
|
1957 apply (simp add: ntimes_ders_cbn) |
|
1958 apply(subst ntimes_hfau_pushin) |
|
1959 apply simp |
|
1960 apply(subgoal_tac "concat (map hflat_aux (map (rder x) (hflat_aux (rders (RSEQ (rder c r) (RNTIMES r n)) xs)))) = |
|
1961 concat (map hflat_aux (map (rder x) ( map (opterm r) (nupdates xs r [Some ([c], n)])))) ") |
|
1962 apply(simp only:) |
|
1963 prefer 2 |
|
1964 apply presburger |
|
1965 apply(subst nupdates_append[symmetric]) |
|
1966 using nupdates_join_general by blast |
|
1967 |
|
1968 |
|
1969 (*nupdates s r [Some ([c], n)]*) |
|
1970 lemma ntimes_ders_hfau_also1: |
|
1971 shows "hflat_aux (rders (RNTIMES r (Suc n)) (c # xs)) = map (opterm r) (nupdates xs r [Some ([c], n)])" |
|
1972 using ntimes_hfau_induct by force |
|
1973 |
|
1974 |
|
1975 |
|
1976 lemma hfau_rsimpeq2_ntimes: |
|
1977 shows "created_by_ntimes r \<Longrightarrow> rsimp r = rsimp ( (RALTS (hflat_aux r)))" |
|
1978 apply(induct r) |
|
1979 apply simp+ |
|
1980 |
|
1981 apply (metis rsimp_seq_equal1) |
|
1982 prefer 2 |
|
1983 apply simp |
|
1984 apply(case_tac x) |
|
1985 apply simp |
|
1986 apply(case_tac "list") |
|
1987 apply simp |
|
1988 |
|
1989 apply (metis idem_after_simp1) |
|
1990 apply(case_tac "lista") |
|
1991 prefer 2 |
|
1992 apply (metis hflat_aux.simps(8) idem_after_simp1 list.simps(8) list.simps(9) rsimp.simps(2)) |
|
1993 apply(subgoal_tac "rsimp (RALT a aa) = rsimp (RALTS (hflat_aux (RALT a aa)))") |
|
1994 apply simp |
|
1995 apply(subgoal_tac "rsimp (RALT a aa) = rsimp (RALTS (hflat_aux a @ hflat_aux aa))") |
|
1996 using hflat_aux.simps(1) apply presburger |
|
1997 apply simp |
|
1998 using cbs_hfau_rsimpeq1 apply(fastforce) |
|
1999 by simp |
|
2000 |
|
2001 |
|
2002 lemma ntimes_closed_form1: |
|
2003 shows "rsimp (rders (RNTIMES r (Suc n)) (c#s)) = |
|
2004 rsimp ( ( RALTS ( map (opterm r) (nupdates s r [Some ([c], n)]) )))" |
|
2005 apply(subgoal_tac "created_by_ntimes (rders (RNTIMES r (Suc n)) (c#s))") |
|
2006 apply(subst hfau_rsimpeq2_ntimes) |
|
2007 apply linarith |
|
2008 using ntimes_ders_hfau_also1 apply auto[1] |
|
2009 using ntimes_ders_cbn1 by blast |
|
2010 |
|
2011 |
|
2012 lemma ntimes_closed_form2: |
|
2013 shows "rsimp (rders_simp (RNTIMES r (Suc n)) (c#s) ) = |
|
2014 rsimp ( ( RALTS ( (map (opterm r ) (nupdates s r [Some ([c], n)]) ) )))" |
|
2015 by (metis list.distinct(1) ntimes_closed_form1 rders_simp_same_simpders rsimp_idem) |
|
2016 |
|
2017 |
|
2018 lemma ntimes_closed_form3: |
|
2019 shows "rsimp (rders_simp (RNTIMES r n) (c#s)) = (rders_simp (RNTIMES r n) (c#s))" |
|
2020 by (metis list.distinct(1) rders_simp_same_simpders rsimp_idem) |
|
2021 |
|
2022 |
|
2023 lemma ntimes_closed_form4: |
|
2024 shows " (rders_simp (RNTIMES r (Suc n)) (c#s)) = |
|
2025 rsimp ( ( RALTS ( (map (opterm r ) (nupdates s r [Some ([c], n)]) ) )))" |
|
2026 using ntimes_closed_form2 ntimes_closed_form3 |
|
2027 by metis |
|
2028 |
|
2029 |
|
2030 |
|
2031 |
|
2032 lemma ntimes_closed_form5: |
|
2033 shows " rsimp ( RALTS (map (\<lambda>s1. RSEQ (rders r0 s1) (RNTIMES r n) ) Ss)) = |
|
2034 rsimp ( RALTS (map (\<lambda>s1. rsimp (RSEQ (rders r0 s1) (RNTIMES r n)) ) Ss))" |
|
2035 by (smt (verit, ccfv_SIG) list.map_comp map_eq_conv o_apply simp_flatten_aux0) |
|
2036 |
|
2037 |
|
2038 |
|
2039 lemma ntimes_closed_form6_hrewrites: |
|
2040 shows " |
|
2041 (map (\<lambda>s1. (RSEQ (rsimp (rders r0 s1)) (RNTIMES r0 n)) ) Ss ) |
|
2042 scf\<leadsto>* |
|
2043 (map (\<lambda>s1. rsimp (RSEQ (rders r0 s1) (RNTIMES r0 n)) ) Ss )" |
|
2044 apply(induct Ss) |
|
2045 apply simp |
|
2046 apply (simp add: ss1) |
|
2047 by (metis (no_types, lifting) list.simps(9) rsimp.simps(1) rsimp_idem simp_hrewrites ss2) |
|
2048 |
|
2049 |
|
2050 |
|
2051 lemma ntimes_closed_form6: |
|
2052 shows " rsimp ( ( RALTS ( (map (\<lambda>s1. rsimp (RSEQ (rders r0 s1) (RNTIMES r0 n)) ) Ss )))) = |
|
2053 rsimp ( ( RALTS ( (map (\<lambda>s1. (RSEQ (rsimp (rders r0 s1)) (RNTIMES r0 n)) ) Ss ))))" |
|
2054 apply(subgoal_tac " map (\<lambda>s1. (RSEQ (rsimp (rders r0 s1)) (RNTIMES r0 n)) ) Ss scf\<leadsto>* |
|
2055 map (\<lambda>s1. rsimp (RSEQ (rders r0 s1) (RNTIMES r0 n)) ) Ss ") |
|
2056 using hrewrites_simpeq srewritescf_alt1 apply fastforce |
|
2057 using ntimes_closed_form6_hrewrites by blast |
|
2058 |
|
2059 abbreviation |
|
2060 "optermsimp r SN \<equiv> case SN of |
|
2061 Some (s, n) \<Rightarrow> RSEQ (rders_simp r s) (RNTIMES r n) |
|
2062 | None \<Rightarrow> RZERO |
|
2063 |
|
2064 |
|
2065 " |
|
2066 |
|
2067 abbreviation |
|
2068 "optermOsimp r SN \<equiv> case SN of |
|
2069 Some (s, n) \<Rightarrow> rsimp (RSEQ (rders r s) (RNTIMES r n)) |
|
2070 | None \<Rightarrow> RZERO |
|
2071 |
|
2072 |
|
2073 " |
|
2074 |
|
2075 abbreviation |
|
2076 "optermosimp r SN \<equiv> case SN of |
|
2077 Some (s, n) \<Rightarrow> RSEQ (rsimp (rders r s)) (RNTIMES r n) |
|
2078 | None \<Rightarrow> RZERO |
|
2079 " |
|
2080 |
|
2081 lemma ntimes_closed_form51: |
|
2082 shows "rsimp (RALTS (map (opterm r) (nupdates s r [Some ([c], n)]))) = |
|
2083 rsimp (RALTS (map (rsimp \<circ> (opterm r)) (nupdates s r [Some ([c], n)])))" |
|
2084 by (metis map_map simp_flatten_aux0) |
|
2085 |
|
2086 |
|
2087 |
|
2088 lemma osimp_Osimp: |
|
2089 shows " nonempty_string sn \<Longrightarrow> optermosimp r sn = optermsimp r sn" |
|
2090 apply(induct rule: nonempty_string.induct) |
|
2091 apply force |
|
2092 apply auto[1] |
|
2093 apply simp |
|
2094 by (metis list.distinct(1) rders.simps(2) rders_simp.simps(2) rders_simp_same_simpders) |
|
2095 |
|
2096 |
|
2097 |
|
2098 lemma osimp_Osimp_list: |
|
2099 shows "\<forall>sn \<in> set snlist. nonempty_string sn \<Longrightarrow> map (optermosimp r) snlist = map (optermsimp r) snlist" |
|
2100 by (simp add: osimp_Osimp) |
|
2101 |
|
2102 |
|
2103 lemma ntimes_closed_form8: |
|
2104 shows |
|
2105 "rsimp (RALTS (map (optermosimp r) (nupdates s r [Some ([c], n)]))) = |
|
2106 rsimp (RALTS (map (optermsimp r) (nupdates s r [Some ([c], n)])))" |
|
2107 apply(subgoal_tac "\<forall>opt \<in> set (nupdates s r [Some ([c], n)]). nonempty_string opt") |
|
2108 using osimp_Osimp_list apply presburger |
|
2109 by (metis list.distinct(1) list.set_cases nonempty_string.simps(3) nupdates_nonempty set_ConsD) |
|
2110 |
|
2111 |
|
2112 |
|
2113 lemma ntimes_closed_form9aux: |
|
2114 shows "\<forall>snopt \<in> set (nupdates s r [Some ([c], n)]). nonempty_string snopt" |
|
2115 by (metis list.distinct(1) list.set_cases nonempty_string.simps(3) nupdates_nonempty set_ConsD) |
|
2116 |
|
2117 lemma ntimes_closed_form9aux1: |
|
2118 shows "\<forall>snopt \<in> set snlist. nonempty_string snopt \<Longrightarrow> |
|
2119 rsimp (RALTS (map (optermosimp r) snlist)) = |
|
2120 rsimp (RALTS (map (optermOsimp r) snlist))" |
|
2121 apply(induct snlist) |
|
2122 apply simp+ |
|
2123 apply(case_tac "a") |
|
2124 apply simp+ |
|
2125 by (smt (z3) case_prod_conv idem_after_simp1 map_eq_conv nonempty_string.elims(2) o_apply option.simps(4) option.simps(5) rsimp.simps(1) rsimp.simps(7) rsimp_idem) |
|
2126 |
|
2127 |
|
2128 |
|
2129 |
|
2130 lemma ntimes_closed_form9: |
|
2131 shows |
|
2132 "rsimp (RALTS (map (optermosimp r) (nupdates s r [Some ([c], n)]))) = |
|
2133 rsimp (RALTS (map (optermOsimp r) (nupdates s r [Some ([c], n)])))" |
|
2134 using ntimes_closed_form9aux ntimes_closed_form9aux1 by presburger |
|
2135 |
|
2136 |
|
2137 lemma ntimes_closed_form10rewrites_aux: |
|
2138 shows " map (rsimp \<circ> (opterm r)) optlist scf\<leadsto>* |
|
2139 map (optermOsimp r) optlist" |
|
2140 apply(induct optlist) |
|
2141 apply simp |
|
2142 apply (simp add: ss1) |
|
2143 apply simp |
|
2144 apply(case_tac a) |
|
2145 using ss2 apply fastforce |
|
2146 using ss2 by force |
|
2147 |
|
2148 |
|
2149 lemma ntimes_closed_form10rewrites: |
|
2150 shows " map (rsimp \<circ> (opterm r)) (nupdates s r [Some ([c], n)]) scf\<leadsto>* |
|
2151 map (optermOsimp r) (nupdates s r [Some ([c], n)])" |
|
2152 using ntimes_closed_form10rewrites_aux by blast |
|
2153 |
|
2154 lemma ntimes_closed_form10: |
|
2155 shows "rsimp (RALTS (map (rsimp \<circ> (opterm r)) (nupdates s r [Some ([c], n)]))) = |
|
2156 rsimp (RALTS (map (optermOsimp r) (nupdates s r [Some ([c], n)])))" |
|
2157 by (smt (verit, best) case_prod_conv hpower_rs_elems map_eq_conv nupdates_mono2 o_apply option.case(2) option.simps(4) rsimp.simps(3)) |
|
2158 |
|
2159 |
|
2160 lemma rders_simp_cons: |
|
2161 shows "rders_simp r (c # s) = rders_simp (rsimp (rder c r)) s" |
|
2162 by simp |
|
2163 |
|
2164 lemma rder_ntimes: |
|
2165 shows "rder c (RNTIMES r (Suc n)) = RSEQ (rder c r) (RNTIMES r n)" |
|
2166 by simp |
|
2167 |
|
2168 |
|
2169 lemma ntimes_closed_form: |
|
2170 shows "rders_simp (RNTIMES r0 (Suc n)) (c#s) = |
|
2171 rsimp ( RALTS ( (map (optermsimp r0 ) (nupdates s r0 [Some ([c], n)]) ) ))" |
|
2172 apply (subst rders_simp_cons) |
|
2173 apply(subst rder_ntimes) |
|
2174 using ntimes_closed_form10 ntimes_closed_form4 ntimes_closed_form51 ntimes_closed_form8 ntimes_closed_form9 by force |
|
2175 |
|
2176 |
|
2177 |
|
2178 |
|
2179 |
|
2180 |
|
2181 (* |
|
2182 lemma ntimes_closed_form: |
|
2183 assumes "s \<noteq> []" |
|
2184 shows "rders_simp (RNTIMES r (Suc n)) s = |
|
2185 rsimp ( RALTS ( map |
|
2186 (\<lambda> optSN. case optSN of |
|
2187 Some (s, n) \<Rightarrow> RSEQ (rders_simp r s) (RNTIMES r n) |
|
2188 | None \<Rightarrow> RZERO |
|
2189 ) |
|
2190 (ntset r n s) |
|
2191 ) |
|
2192 )" |
|
2193 |
|
2194 *) |
|
1465 end |
2195 end |