60 shows "bder c (fuse bs a) = fuse bs (bder c a)" |
60 shows "bder c (fuse bs a) = fuse bs (bder c a)" |
61 apply(induct a arbitrary: bs c) |
61 apply(induct a arbitrary: bs c) |
62 apply(simp_all) |
62 apply(simp_all) |
63 done |
63 done |
64 |
64 |
|
65 |
|
66 |
|
67 |
|
68 fun ABIncludedByC :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('c \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool" where |
|
69 "ABIncludedByC a b c f subseteqPred = subseteqPred (f a b) c" |
|
70 |
|
71 fun furtherSEQ :: "rexp \<Rightarrow> rexp \<Rightarrow> rexp list" and |
|
72 turnIntoTerms :: "rexp \<Rightarrow> rexp list " |
|
73 where |
|
74 "furtherSEQ ONE r2 = turnIntoTerms r2 " |
|
75 | "furtherSEQ r11 r2 = [SEQ r11 r2]" |
|
76 | "turnIntoTerms (SEQ ONE r2) = turnIntoTerms r2" |
|
77 | "turnIntoTerms (SEQ r1 r2) = concat (map (\<lambda>r11. furtherSEQ r11 r2) (turnIntoTerms r1))" |
|
78 | "turnIntoTerms r = [r]" |
|
79 |
|
80 fun regConcat :: "rexp \<Rightarrow> rexp list \<Rightarrow> rexp" where |
|
81 "regConcat acc [] = acc" |
|
82 | "regConcat ONE (r # rs1) = regConcat r rs1" |
|
83 | "regConcat acc (r # rs1) = regConcat (SEQ acc r) rs1" |
|
84 |
|
85 fun attachCtx :: "arexp \<Rightarrow> rexp list \<Rightarrow> rexp set" where |
|
86 "attachCtx r ctx = set (turnIntoTerms (regConcat (erase r) ctx))" |
|
87 |
|
88 |
|
89 |
|
90 fun rs1_subseteq_rs2 :: "rexp set \<Rightarrow> rexp set \<Rightarrow> bool" where |
|
91 "rs1_subseteq_rs2 rs1 rs2 = (rs1 \<subseteq> rs2)" |
|
92 |
|
93 fun notZero :: "arexp \<Rightarrow> bool" where |
|
94 "notZero AZERO = True" |
|
95 | "notZero _ = False" |
|
96 |
|
97 fun prune6 :: "rexp set \<Rightarrow> arexp \<Rightarrow> rexp list \<Rightarrow> arexp" where |
|
98 "prune6 acc a ctx = (if (ABIncludedByC a ctx acc attachCtx rs1_subseteq_rs2) then AZERO else |
|
99 (case a of (ASEQ bs r1 r2) \<Rightarrow> bsimp_ASEQ bs (prune6 acc r1 (erase r2 # ctx)) r2 |
|
100 | AALTs bs rs0 \<Rightarrow> bsimp_AALTs bs (filter notZero (map (\<lambda>r.(prune6 acc r ctx)) rs0))) )" |
|
101 |
|
102 |
|
103 |
|
104 fun dB6 :: "arexp list \<Rightarrow> rexp set \<Rightarrow> arexp list" where |
|
105 "dB6 [] acc = []" |
|
106 | "dB6 (a # as) acc = (if (erase a \<in> acc) then (dB6 as acc) |
|
107 else (let pruned = prune6 acc a [] in |
|
108 (case pruned of |
|
109 AZERO \<Rightarrow> dB6 as acc |
|
110 |xPrime \<Rightarrow> xPrime # (dB6 as ( (set (turnIntoTerms (erase pruned))) \<union> acc) ) ) )) " |
|
111 |
|
112 |
|
113 fun bsimpStrong6 :: "arexp \<Rightarrow> arexp" |
|
114 where |
|
115 "bsimpStrong6 (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2)" |
|
116 | "bsimpStrong6 (AALTs bs1 rs) = bsimp_AALTs bs1 (dB6 (flts (map bsimpStrong6 rs)) {}) " |
|
117 | "bsimpStrong6 r = r" |
|
118 |
|
119 |
|
120 fun |
|
121 bdersStrong6 :: "arexp \<Rightarrow> string \<Rightarrow> arexp" |
|
122 where |
|
123 "bdersStrong6 r [] = r" |
|
124 | "bdersStrong6 r (c # s) = bdersStrong6 (bsimpStrong6 (bder c r)) s" |
|
125 |
|
126 definition blexerStrong where |
|
127 "blexerStrong r s \<equiv> if bnullable (bdersStrong6 (intern r) s) then |
|
128 decode (bmkeps (bdersStrong6 (intern r) s)) r else None" |
65 |
129 |
66 |
130 |
67 |
131 |
68 inductive |
132 inductive |
69 rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99) |
133 rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99) |
369 using a3 bnullable0(1) rewrite_bmkeps_aux(1) by blast |
433 using a3 bnullable0(1) rewrite_bmkeps_aux(1) by blast |
370 then show "bmkeps r1 = bmkeps r3" using IH by simp |
434 then show "bmkeps r1 = bmkeps r3" using IH by simp |
371 qed |
435 qed |
372 |
436 |
373 |
437 |
374 lemma rewrites_to_bsimp: |
|
375 shows "r \<leadsto>* bsimp r" |
|
376 proof (induction r rule: bsimp.induct) |
|
377 case (1 bs1 r1 r2) |
|
378 have IH1: "r1 \<leadsto>* bsimp r1" by fact |
|
379 have IH2: "r2 \<leadsto>* bsimp r2" by fact |
|
380 { assume as: "bsimp r1 = AZERO \<or> bsimp r2 = AZERO" |
|
381 with IH1 IH2 have "r1 \<leadsto>* AZERO \<or> r2 \<leadsto>* AZERO" by auto |
|
382 then have "ASEQ bs1 r1 r2 \<leadsto>* AZERO" |
|
383 by (metis bs2 continuous_rewrite rrewrites.simps star_seq2) |
|
384 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" using as by auto |
|
385 } |
|
386 moreover |
|
387 { assume "\<exists>bs. bsimp r1 = AONE bs" |
|
388 then obtain bs where as: "bsimp r1 = AONE bs" by blast |
|
389 with IH1 have "r1 \<leadsto>* AONE bs" by simp |
|
390 then have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) r2" using bs3 star_seq by blast |
|
391 with IH2 have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) (bsimp r2)" |
|
392 using rewrites_fuse by (meson rrewrites_trans) |
|
393 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 (AONE bs) r2)" by simp |
|
394 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" by (simp add: as) |
|
395 } |
|
396 moreover |
|
397 { assume as1: "bsimp r1 \<noteq> AZERO" "bsimp r2 \<noteq> AZERO" and as2: "(\<nexists>bs. bsimp r1 = AONE bs)" |
|
398 then have "bsimp_ASEQ bs1 (bsimp r1) (bsimp r2) = ASEQ bs1 (bsimp r1) (bsimp r2)" |
|
399 by (simp add: bsimp_ASEQ1) |
|
400 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)" using as1 as2 IH1 IH2 |
|
401 by (metis rrewrites_trans star_seq star_seq2) |
|
402 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" by simp |
|
403 } |
|
404 ultimately show "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" by blast |
|
405 next |
|
406 case (2 bs1 rs) |
|
407 have IH: "\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimp x" by fact |
|
408 then have "rs s\<leadsto>* (map bsimp rs)" by (simp add: trivialbsimp_srewrites) |
|
409 also have "... s\<leadsto>* flts (map bsimp rs)" by (simp add: fltsfrewrites) |
|
410 also have "... s\<leadsto>* distinctWith (flts (map bsimp rs)) eq1 {}" by (simp add: ss6_stronger) |
|
411 finally have "AALTs bs1 rs \<leadsto>* AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {})" |
|
412 using contextrewrites0 by auto |
|
413 also have "... \<leadsto>* bsimp_AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {})" |
|
414 by (simp add: bsimp_AALTs_rewrites) |
|
415 finally show "AALTs bs1 rs \<leadsto>* bsimp (AALTs bs1 rs)" by simp |
|
416 qed (simp_all) |
|
417 |
|
418 |
438 |
419 lemma to_zero_in_alt: |
439 lemma to_zero_in_alt: |
420 shows "AALT bs (ASEQ [] AZERO r) r2 \<leadsto> AALT bs AZERO r2" |
440 shows "AALT bs (ASEQ [] AZERO r) r2 \<leadsto> AALT bs AZERO r2" |
421 by (simp add: bs1 bs10 ss3) |
441 by (simp add: bs1 bs10 ss3) |
422 |
442 |
515 using assms |
535 using assms |
516 apply(induction r1 r2 rule: rrewrites.induct) |
536 apply(induction r1 r2 rule: rrewrites.induct) |
517 apply(simp_all add: rewrite_preserves_bder rrewrites_trans) |
537 apply(simp_all add: rewrite_preserves_bder rrewrites_trans) |
518 done |
538 done |
519 |
539 |
520 |
|
521 |
|
522 |
|
523 fun ABIncludedByC :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('c \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool" where |
|
524 "ABIncludedByC a b c f subseteqPred = subseteqPred (f a b) c" |
|
525 |
|
526 fun furtherSEQ :: "rexp \<Rightarrow> rexp \<Rightarrow> rexp list" and |
|
527 turnIntoTerms :: "rexp \<Rightarrow> rexp list " |
|
528 where |
|
529 "furtherSEQ ONE r2 = turnIntoTerms r2 " |
|
530 | "furtherSEQ r11 r2 = [SEQ r11 r2]" |
|
531 | "turnIntoTerms (SEQ ONE r2) = turnIntoTerms r2" |
|
532 | "turnIntoTerms (SEQ r1 r2) = concat (map (\<lambda>r11. furtherSEQ r11 r2) (turnIntoTerms r1))" |
|
533 | "turnIntoTerms r = [r]" |
|
534 |
|
535 fun regConcat :: "rexp \<Rightarrow> rexp list \<Rightarrow> rexp" where |
|
536 "regConcat acc [] = acc" |
|
537 | "regConcat ONE (r # rs1) = regConcat r rs1" |
|
538 | "regConcat acc (r # rs1) = regConcat (SEQ acc r) rs1" |
|
539 |
|
540 fun attachCtx :: "arexp \<Rightarrow> rexp list \<Rightarrow> rexp set" where |
|
541 "attachCtx r ctx = set (turnIntoTerms (regConcat (erase r) ctx))" |
|
542 |
|
543 |
|
544 |
|
545 fun rs1_subseteq_rs2 :: "rexp set \<Rightarrow> rexp set \<Rightarrow> bool" where |
|
546 "rs1_subseteq_rs2 rs1 rs2 = (rs1 \<subseteq> rs2)" |
|
547 |
|
548 fun notZero :: "arexp \<Rightarrow> bool" where |
|
549 "notZero AZERO = True" |
|
550 | "notZero _ = False" |
|
551 |
|
552 fun prune6 :: "rexp set \<Rightarrow> arexp \<Rightarrow> rexp list \<Rightarrow> arexp" where |
|
553 "prune6 acc a ctx = (if (ABIncludedByC a ctx acc attachCtx rs1_subseteq_rs2) then AZERO else |
|
554 (case a of (ASEQ bs r1 r2) \<Rightarrow> bsimp_ASEQ bs (prune6 acc r1 (erase r2 # ctx)) r2 |
|
555 | AALTs bs rs0 \<Rightarrow> bsimp_AALTs bs (filter notZero (map (\<lambda>r.(prune6 acc r ctx)) rs0))) )" |
|
556 |
|
557 |
|
558 fun dB6 :: "arexp list \<Rightarrow> rexp set \<Rightarrow> arexp list" where |
|
559 "dB6 [] acc = []" |
|
560 | "dB6 (a # as) acc = (if (erase a \<in> acc) then (dB6 as acc) |
|
561 else (let pruned = prune6 acc a [] in |
|
562 (case pruned of |
|
563 AZERO \<Rightarrow> dB6 as acc |
|
564 |xPrime \<Rightarrow> xPrime # (dB6 as ( (set (turnIntoTerms (erase pruned))) \<union> acc) ) ) )) " |
|
565 |
|
566 |
|
567 fun bsimpStrong6 :: "arexp \<Rightarrow> arexp" |
|
568 where |
|
569 "bsimpStrong6 (ASEQ bs1 r1 r2) = bsimp_ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2)" |
|
570 | "bsimpStrong6 (AALTs bs1 rs) = bsimp_AALTs bs1 (dB6 (flts (map bsimpStrong6 rs)) {}) " |
|
571 | "bsimpStrong6 r = r" |
|
572 |
|
573 |
|
574 fun |
|
575 bdersStrong6 :: "arexp \<Rightarrow> string \<Rightarrow> arexp" |
|
576 where |
|
577 "bdersStrong6 r [] = r" |
|
578 | "bdersStrong6 r (c # s) = bdersStrong6 (bsimpStrong6 (bder c r)) s" |
|
579 |
|
580 definition blexerStrong where |
|
581 "blexerStrong r s \<equiv> if bnullable (bdersStrong6 (intern r) s) then |
|
582 decode (bmkeps (bdersStrong6 (intern r) s)) r else None" |
|
583 |
540 |
584 |
541 |
585 lemma bders_simp_appendStrong : |
542 lemma bders_simp_appendStrong : |
586 shows "bdersStrong6 r (s1 @ s2) = bdersStrong6 (bdersStrong6 r s1) s2" |
543 shows "bdersStrong6 r (s1 @ s2) = bdersStrong6 (bdersStrong6 r s1) s2" |
587 apply(induct s1 arbitrary: s2 rule: rev_induct) |
544 apply(induct s1 arbitrary: s2 rule: rev_induct) |