648 "prune6 acc a ctx = (if (ABIncludedByC a ctx acc attachCtx rs1_subseteq_rs2) then AZERO else |
648 "prune6 acc a ctx = (if (ABIncludedByC a ctx acc attachCtx rs1_subseteq_rs2) then AZERO else |
649 (case a of (ASEQ bs r1 r2) \<Rightarrow> bsimp_ASEQ bs (prune6 acc r1 (erase r2 # ctx)) r2 |
649 (case a of (ASEQ bs r1 r2) \<Rightarrow> bsimp_ASEQ bs (prune6 acc r1 (erase r2 # ctx)) r2 |
650 | AALTs bs rs0 \<Rightarrow> bsimp_AALTs bs (filter notZero (map (\<lambda>r.(prune6 acc r ctx)) rs0))) )" |
650 | AALTs bs rs0 \<Rightarrow> bsimp_AALTs bs (filter notZero (map (\<lambda>r.(prune6 acc r ctx)) rs0))) )" |
651 |
651 |
652 |
652 |
653 |
|
654 (* |
|
655 def prune6(acc: Set[Rexp], r: ARexp, ctx: List[Rexp] = Nil) : ARexp = { |
|
656 if (ABIncludedByC(a = r, b = ctx, c = acc, |
|
657 f = attachCtx, subseteqPred = rs1_subseteq_rs2)) |
|
658 { |
|
659 AZERO |
|
660 } |
|
661 else{ |
|
662 r match { |
|
663 case ASEQ(bs, r1, r2) => (prune6(acc, r1, erase(r2) :: ctx)) match{ |
|
664 case AZERO => |
|
665 AZERO |
|
666 case AONE(bs1) => //when r1 becomes 1, chances to further prune r2 |
|
667 prune6(acc, fuse(bs1, r2), ctx) |
|
668 case r1p => |
|
669 ASEQ(bs, r1p, r2) |
|
670 } |
|
671 case AALTS(bs, rs0) => |
|
672 rs0.map(r => prune6(acc, r, ctx)).filter(_ != AZERO) match { |
|
673 case Nil => |
|
674 AZERO |
|
675 case r :: Nil => |
|
676 fuse(bs, r) |
|
677 case rs0p => |
|
678 AALTS(bs, rs0p) |
|
679 } |
|
680 case r => r |
|
681 } |
|
682 } |
|
683 } |
|
684 |
|
685 |
|
686 *) |
|
687 |
|
688 fun dB6 :: "arexp list \<Rightarrow> rexp set \<Rightarrow> arexp list" where |
653 fun dB6 :: "arexp list \<Rightarrow> rexp set \<Rightarrow> arexp list" where |
689 "dB6 [] acc = []" |
654 "dB6 [] acc = []" |
690 | "dB6 (a # as) acc = (if (erase a \<in> acc) then (dB6 as acc) |
655 | "dB6 (a # as) acc = (if (erase a \<in> acc) then (dB6 as acc) |
691 else (let pruned = prune6 acc a [] in |
656 else (let pruned = prune6 acc a [] in |
692 (case pruned of |
657 (case pruned of |
710 definition blexerStrong where |
675 definition blexerStrong where |
711 "blexerStrong r s \<equiv> if bnullable (bdersStrong6 (intern r) s) then |
676 "blexerStrong r s \<equiv> if bnullable (bdersStrong6 (intern r) s) then |
712 decode (bmkeps (bdersStrong6 (intern r) s)) r else None" |
677 decode (bmkeps (bdersStrong6 (intern r) s)) r else None" |
713 |
678 |
714 |
679 |
|
680 (* |
|
681 lemma rewrite_preserves_bder: |
|
682 shows "r1 \<leadsto> r2 \<Longrightarrow> (bder c r1) \<leadsto>* (bder c r2)" |
|
683 and "rs1 s\<leadsto> rs2 \<Longrightarrow> map (bder c) rs1 s\<leadsto>* map (bder c) rs2" |
|
684 proof(induction rule: rrewrite_srewrite.inducts) |
|
685 case (bs1 bs r2) |
|
686 then show ?case |
|
687 by (simp add: continuous_rewrite) |
|
688 next |
|
689 case (bs2 bs r1) |
|
690 then show ?case |
|
691 apply(auto) |
|
692 apply (meson bs6 contextrewrites0 rrewrite_srewrite.bs2 rs2 ss3 ss4 sss1 sss2) |
|
693 by (simp add: r_in_rstar rrewrite_srewrite.bs2) |
|
694 next |
|
695 case (bs3 bs1 bs2 r) |
|
696 then show ?case |
|
697 apply(simp) |
|
698 |
|
699 by (metis (no_types, lifting) bder_fuse bs10 bs7 fuse_append rrewrites.simps ss4 to_zero_in_alt) |
|
700 next |
|
701 case (bs4 r1 r2 bs r3) |
|
702 have as: "r1 \<leadsto> r2" by fact |
|
703 have IH: "bder c r1 \<leadsto>* bder c r2" by fact |
|
704 from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r2 r3)" |
|
705 by (metis bder.simps(5) bnullable0(1) contextrewrites1 rewrite_bmkeps_aux(1) star_seq) |
|
706 next |
|
707 case (bs5 r3 r4 bs r1) |
|
708 have as: "r3 \<leadsto> r4" by fact |
|
709 have IH: "bder c r3 \<leadsto>* bder c r4" by fact |
|
710 from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r1 r4)" |
|
711 apply(simp) |
|
712 apply(auto) |
|
713 using contextrewrites0 r_in_rstar rewrites_fuse srewrites6 srewrites7 star_seq2 apply presburger |
|
714 using star_seq2 by blast |
|
715 next |
|
716 case (bs6 bs) |
|
717 then show ?case |
|
718 using rrewrite_srewrite.bs6 by force |
|
719 next |
|
720 case (bs7 bs r) |
|
721 then show ?case |
|
722 by (simp add: bder_fuse r_in_rstar rrewrite_srewrite.bs7) |
|
723 next |
|
724 case (bs10 rs1 rs2 bs) |
|
725 then show ?case |
|
726 using contextrewrites0 by force |
|
727 next |
|
728 case ss1 |
|
729 then show ?case by simp |
|
730 next |
|
731 case (ss2 rs1 rs2 r) |
|
732 then show ?case |
|
733 by (simp add: srewrites7) |
|
734 next |
|
735 case (ss3 r1 r2 rs) |
|
736 then show ?case |
|
737 by (simp add: srewrites7) |
|
738 next |
|
739 case (ss4 rs) |
|
740 then show ?case |
|
741 using rrewrite_srewrite.ss4 by fastforce |
|
742 next |
|
743 case (ss5 bs1 rs1 rsb) |
|
744 then show ?case |
|
745 apply(simp) |
|
746 using bder_fuse_list map_map rrewrite_srewrite.ss5 srewrites.simps by blast |
|
747 next |
|
748 case (ss6 a1 a2 bs rsa rsb) |
|
749 then show ?case |
|
750 apply(simp only: map_append map1) |
|
751 apply(rule srewrites_trans) |
|
752 apply(rule rs_in_rstar) |
|
753 apply(rule_tac rrewrite_srewrite.ss6) |
|
754 using Der_def der_correctness apply auto[1] |
|
755 by blast |
|
756 qed |
|
757 *) |
|
758 |
|
759 |
|
760 |
715 lemma centralStrong: |
761 lemma centralStrong: |
716 shows "bders_simp r s \<leadsto>* bdersStrong6 r s" |
762 shows "bders r s \<leadsto>* bdersStrong6 r s" |
717 proof(induct s arbitrary: r rule: rev_induct) |
763 proof(induct s arbitrary: r rule: rev_induct) |
718 case Nil |
764 case Nil |
719 then show "bders_simp r [] \<leadsto>* bdersStrong6 r []" by simp |
765 then show "bders r [] \<leadsto>* bdersStrong6 r []" by simp |
720 next |
766 next |
721 case (snoc x xs) |
767 case (snoc x xs) |
722 have IH: "\<And>r. bders_simp r xs \<leadsto>* bdersStrong6 r xs" by fact |
768 have IH: "\<And>r. bders r xs \<leadsto>* bdersStrong6 r xs" by fact |
723 have "bders_simp r (xs @ [x]) = bders_simp (bders_simp r xs) [x]" by (simp add: bders_simp_append) |
769 have "bders r (xs @ [x]) = bders (bders r xs) [x]" by (simp add: bders_append) |
724 also have "... \<leadsto>* bders_simp (bdersStrong6 r xs) [x]" using IH |
770 also have "... \<leadsto>* bders (bdersStrong6 r xs) [x]" using IH |
725 by (simp add: rewrites_preserves_bder) |
771 by (simp add: rewrites_preserves_bder) |
726 also have "... \<leadsto>* bders_simp (bders_simp r xs) [x]" using IH |
772 also have "... \<leadsto>* bdersStrong6 (bdersStrong6 r xs) [x]" using IH |
727 by (simp add: rewrites_to_bsimp) |
773 by (simp add: rewrites_to_bsimp) |
728 finally show "bders r (xs @ [x]) \<leadsto>* bders_simp r (xs @ [x])" |
774 finally show "bders r (xs @ [x]) \<leadsto>* bders_simp r (xs @ [x])" |
729 by (simp add: bders_simp_append) |
775 by (simp add: bders_simp_append) |
730 qed |
776 qed |
731 |
777 |
732 lemma mainStrong: |
778 lemma mainStrong: |
733 assumes "bnullable (bders r s)" |
779 assumes "bnullable (bders r s)" |
734 shows "bmkeps (bders_simp r s) = bmkeps (bdersStrong6 r s)" |
780 shows "bmkeps (bders r s) = bmkeps (bdersStrong6 r s)" |
735 proof - |
781 proof - |
736 have "bders_simp r s \<leadsto>* bdersStrong6 r s" sorry |
782 have "bders_simp r s \<leadsto>* bdersStrong6 r s" sorry |
737 then |
783 then |
738 show "bmkeps (bders_simp r s) = bmkeps (bdersStrong6 r s)" |
784 show "bmkeps (bders r s) = bmkeps (bdersStrong6 r s)" |
739 |
785 |
740 sorry |
786 sorry |
741 qed |
787 qed |
742 |
788 |
743 |
789 |