570 apply(induction r1 r2 rule: rrewrites.induct) |
570 apply(induction r1 r2 rule: rrewrites.induct) |
571 apply(simp_all add: rewrite_preserves_bder rrewrites_trans) |
571 apply(simp_all add: rewrite_preserves_bder rrewrites_trans) |
572 done |
572 done |
573 |
573 |
574 |
574 |
|
575 |
575 lemma central: |
576 lemma central: |
576 shows "bders r s \<leadsto>* bders_simp r s" |
577 shows "bders r s \<leadsto>* bders_simp r s" |
577 proof(induct s arbitrary: r rule: rev_induct) |
578 proof(induct s arbitrary: r rule: rev_induct) |
578 case Nil |
579 case Nil |
579 then show "bders r [] \<leadsto>* bders_simp r []" by simp |
580 then show "bders r [] \<leadsto>* bders_simp r []" by simp |
755 by blast |
756 by blast |
756 qed |
757 qed |
757 *) |
758 *) |
758 |
759 |
759 |
760 |
|
761 lemma rewrites_to_bsimpStrong: |
|
762 shows "r \<leadsto>* bsimpStrong6 r" |
|
763 proof (induction r rule: bsimpStrong6.induct) |
|
764 case (1 bs1 r1 r2) |
|
765 have IH1: "r1 \<leadsto>* bsimpStrong6 r1" by fact |
|
766 have IH2: "r2 \<leadsto>* bsimpStrong6 r2" by fact |
|
767 { assume as: "bsimpStrong6 r1 = AZERO \<or> bsimpStrong6 r2 = AZERO" |
|
768 with IH1 IH2 have "r1 \<leadsto>* AZERO \<or> r2 \<leadsto>* AZERO" by auto |
|
769 then have "ASEQ bs1 r1 r2 \<leadsto>* AZERO" |
|
770 by (metis bs2 continuous_rewrite rrewrites.simps star_seq2) |
|
771 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" using as by auto |
|
772 } |
|
773 moreover |
|
774 { assume "\<exists>bs. bsimpStrong6 r1 = AONE bs" |
|
775 then obtain bs where as: "bsimpStrong6 r1 = AONE bs" by blast |
|
776 with IH1 have "r1 \<leadsto>* AONE bs" by simp |
|
777 then have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) r2" using bs3 star_seq by blast |
|
778 with IH2 have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) (bsimpStrong6 r2)" |
|
779 using rewrites_fuse by (meson rrewrites_trans) |
|
780 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 (AONE bs) r2)" by simp |
|
781 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" by (simp add: as) |
|
782 } |
|
783 moreover |
|
784 { assume as1: "bsimpStrong6 r1 \<noteq> AZERO" "bsimpStrong6 r2 \<noteq> AZERO" and as2: "(\<nexists>bs. bsimpStrong6 r1 = AONE bs)" |
|
785 then have "bsimp_ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2) = ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2)" |
|
786 by (simp add: bsimp_ASEQ1) |
|
787 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp_ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2)" using as1 as2 IH1 IH2 |
|
788 by (metis rrewrites_trans star_seq star_seq2) |
|
789 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" by simp |
|
790 } |
|
791 ultimately show "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" sorry |
|
792 next |
|
793 case (2 bs1 rs) |
|
794 have IH: "\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimpStrong6 x" by fact |
|
795 then have "rs s\<leadsto>* (map bsimpStrong6 rs)" by (simp add: trivialbsimp_srewrites) |
|
796 also have "... s\<leadsto>* flts (map bsimpStrong6 rs)" by (simp add: fltsfrewrites) |
|
797 also have "... s\<leadsto>* distinctWith (flts (map bsimpStrong6 rs)) eq1 {}" by (simp add: ss6_stronger) |
|
798 finally have "AALTs bs1 rs \<leadsto>* AALTs bs1 (distinctWith (flts (map bsimpStrong6 rs)) eq1 {})" |
|
799 using contextrewrites0 by auto |
|
800 also have "... \<leadsto>* bsimp_AALTs bs1 (distinctWith (flts (map bsimpStrong6 rs)) eq1 {})" |
|
801 by (simp add: bsimp_AALTs_rewrites) |
|
802 finally show "AALTs bs1 rs \<leadsto>* bsimpStrong6 (AALTs bs1 rs)" sorry |
|
803 qed (simp_all) |
|
804 |
|
805 lemma bders_simp_appendStrong : |
|
806 shows "bdersStrong6 r (s1 @ s2) = bdersStrong6 (bdersStrong6 r s1) s2" |
|
807 apply(induct s1 arbitrary: s2 rule: rev_induct) |
|
808 apply simp |
|
809 apply auto |
|
810 done |
|
811 |
760 |
812 |
761 lemma centralStrong: |
813 lemma centralStrong: |
762 shows "bders r s \<leadsto>* bdersStrong6 r s" |
814 shows "bders r s \<leadsto>* bdersStrong6 r s" |
763 proof(induct s arbitrary: r rule: rev_induct) |
815 proof(induct s arbitrary: r rule: rev_induct) |
764 case Nil |
816 case Nil |
768 have IH: "\<And>r. bders r xs \<leadsto>* bdersStrong6 r xs" by fact |
820 have IH: "\<And>r. bders r xs \<leadsto>* bdersStrong6 r xs" by fact |
769 have "bders r (xs @ [x]) = bders (bders r xs) [x]" by (simp add: bders_append) |
821 have "bders r (xs @ [x]) = bders (bders r xs) [x]" by (simp add: bders_append) |
770 also have "... \<leadsto>* bders (bdersStrong6 r xs) [x]" using IH |
822 also have "... \<leadsto>* bders (bdersStrong6 r xs) [x]" using IH |
771 by (simp add: rewrites_preserves_bder) |
823 by (simp add: rewrites_preserves_bder) |
772 also have "... \<leadsto>* bdersStrong6 (bdersStrong6 r xs) [x]" using IH |
824 also have "... \<leadsto>* bdersStrong6 (bdersStrong6 r xs) [x]" using IH |
773 by (simp add: rewrites_to_bsimp) |
825 by (simp add: rewrites_to_bsimpStrong) |
774 finally show "bders r (xs @ [x]) \<leadsto>* bders_simp r (xs @ [x])" |
826 finally show "bders r (xs @ [x]) \<leadsto>* bdersStrong6 r (xs @ [x])" |
775 by (simp add: bders_simp_append) |
827 by (simp add: bders_simp_appendStrong) |
776 qed |
828 qed |
777 |
829 |
778 lemma mainStrong: |
830 lemma mainStrong: |
779 assumes "bnullable (bders r s)" |
831 assumes "bnullable (bders r s)" |
780 shows "bmkeps (bders r s) = bmkeps (bdersStrong6 r s)" |
832 shows "bmkeps (bders r s) = bmkeps (bdersStrong6 r s)" |