369 shows "r1 \<leadsto> r2 \<Longrightarrow> bnullable r1 = bnullable r2" |
371 shows "r1 \<leadsto> r2 \<Longrightarrow> bnullable r1 = bnullable r2" |
370 and "rs1 s\<leadsto> rs2 \<Longrightarrow> bnullables rs1 = bnullables rs2" |
372 and "rs1 s\<leadsto> rs2 \<Longrightarrow> bnullables rs1 = bnullables rs2" |
371 apply(induct rule: rrewrite_srewrite.inducts) |
373 apply(induct rule: rrewrite_srewrite.inducts) |
372 apply(auto simp add: bnullable_fuse) |
374 apply(auto simp add: bnullable_fuse) |
373 apply (meson UnCI bnullable_fuse imageI) |
375 apply (meson UnCI bnullable_fuse imageI) |
374 using bnullable_correctness nullable_correctness by blast |
376 using bnullable_correctness nullable_correctness by blast |
|
377 |
|
378 |
375 |
379 |
376 |
380 |
377 lemma rewritesnullable: |
381 lemma rewritesnullable: |
378 assumes "r1 \<leadsto>* r2" |
382 assumes "r1 \<leadsto>* r2" |
379 shows "bnullable r1 = bnullable r2" |
383 shows "bnullable r1 = bnullable r2" |
567 assumes "r1 \<leadsto>* r2" |
571 assumes "r1 \<leadsto>* r2" |
568 shows "bder c r1 \<leadsto>* bder c r2" |
572 shows "bder c r1 \<leadsto>* bder c r2" |
569 using assms |
573 using assms |
570 apply(induction r1 r2 rule: rrewrites.induct) |
574 apply(induction r1 r2 rule: rrewrites.induct) |
571 apply(simp_all add: rewrite_preserves_bder rrewrites_trans) |
575 apply(simp_all add: rewrite_preserves_bder rrewrites_trans) |
572 done |
576 done |
573 |
|
574 |
|
575 |
|
576 lemma central: |
|
577 shows "bders r s \<leadsto>* bders_simp r s" |
|
578 proof(induct s arbitrary: r rule: rev_induct) |
|
579 case Nil |
|
580 then show "bders r [] \<leadsto>* bders_simp r []" by simp |
|
581 next |
|
582 case (snoc x xs) |
|
583 have IH: "\<And>r. bders r xs \<leadsto>* bders_simp r xs" by fact |
|
584 have "bders r (xs @ [x]) = bders (bders r xs) [x]" by (simp add: bders_append) |
|
585 also have "... \<leadsto>* bders (bders_simp r xs) [x]" using IH |
|
586 by (simp add: rewrites_preserves_bder) |
|
587 also have "... \<leadsto>* bders_simp (bders_simp r xs) [x]" using IH |
|
588 by (simp add: rewrites_to_bsimp) |
|
589 finally show "bders r (xs @ [x]) \<leadsto>* bders_simp r (xs @ [x])" |
|
590 by (simp add: bders_simp_append) |
|
591 qed |
|
592 |
|
593 lemma main_aux: |
|
594 assumes "bnullable (bders r s)" |
|
595 shows "bmkeps (bders r s) = bmkeps (bders_simp r s)" |
|
596 proof - |
|
597 have "bders r s \<leadsto>* bders_simp r s" by (rule central) |
|
598 then |
|
599 show "bmkeps (bders r s) = bmkeps (bders_simp r s)" using assms |
|
600 by (rule rewrites_bmkeps) |
|
601 qed |
|
602 |
|
603 |
|
604 |
|
605 |
|
606 theorem main_blexer_simp: |
|
607 shows "blexer r s = blexer_simp r s" |
|
608 unfolding blexer_def blexer_simp_def |
|
609 by (metis central main_aux rewritesnullable) |
|
610 |
|
611 theorem blexersimp_correctness: |
|
612 shows "lexer r s = blexer_simp r s" |
|
613 using blexer_correctness main_blexer_simp by simp |
|
614 |
|
615 |
577 |
616 |
578 |
617 |
579 |
618 |
580 |
619 fun ABIncludedByC :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('c \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool" where |
581 fun ABIncludedByC :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('c \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool" where |
676 definition blexerStrong where |
638 definition blexerStrong where |
677 "blexerStrong r s \<equiv> if bnullable (bdersStrong6 (intern r) s) then |
639 "blexerStrong r s \<equiv> if bnullable (bdersStrong6 (intern r) s) then |
678 decode (bmkeps (bdersStrong6 (intern r) s)) r else None" |
640 decode (bmkeps (bdersStrong6 (intern r) s)) r else None" |
679 |
641 |
680 |
642 |
681 (* |
643 lemma bders_simp_appendStrong : |
682 lemma rewrite_preserves_bder: |
644 shows "bdersStrong6 r (s1 @ s2) = bdersStrong6 (bdersStrong6 r s1) s2" |
683 shows "r1 \<leadsto> r2 \<Longrightarrow> (bder c r1) \<leadsto>* (bder c r2)" |
645 apply(induct s1 arbitrary: s2 rule: rev_induct) |
684 and "rs1 s\<leadsto> rs2 \<Longrightarrow> map (bder c) rs1 s\<leadsto>* map (bder c) rs2" |
646 apply simp |
685 proof(induction rule: rrewrite_srewrite.inducts) |
647 apply auto |
686 case (bs1 bs r2) |
648 done |
687 then show ?case |
649 |
688 by (simp add: continuous_rewrite) |
650 |
689 next |
|
690 case (bs2 bs r1) |
|
691 then show ?case |
|
692 apply(auto) |
|
693 apply (meson bs6 contextrewrites0 rrewrite_srewrite.bs2 rs2 ss3 ss4 sss1 sss2) |
|
694 by (simp add: r_in_rstar rrewrite_srewrite.bs2) |
|
695 next |
|
696 case (bs3 bs1 bs2 r) |
|
697 then show ?case |
|
698 apply(simp) |
|
699 |
|
700 by (metis (no_types, lifting) bder_fuse bs10 bs7 fuse_append rrewrites.simps ss4 to_zero_in_alt) |
|
701 next |
|
702 case (bs4 r1 r2 bs r3) |
|
703 have as: "r1 \<leadsto> r2" by fact |
|
704 have IH: "bder c r1 \<leadsto>* bder c r2" by fact |
|
705 from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r2 r3)" |
|
706 by (metis bder.simps(5) bnullable0(1) contextrewrites1 rewrite_bmkeps_aux(1) star_seq) |
|
707 next |
|
708 case (bs5 r3 r4 bs r1) |
|
709 have as: "r3 \<leadsto> r4" by fact |
|
710 have IH: "bder c r3 \<leadsto>* bder c r4" by fact |
|
711 from as IH show "bder c (ASEQ bs r1 r3) \<leadsto>* bder c (ASEQ bs r1 r4)" |
|
712 apply(simp) |
|
713 apply(auto) |
|
714 using contextrewrites0 r_in_rstar rewrites_fuse srewrites6 srewrites7 star_seq2 apply presburger |
|
715 using star_seq2 by blast |
|
716 next |
|
717 case (bs6 bs) |
|
718 then show ?case |
|
719 using rrewrite_srewrite.bs6 by force |
|
720 next |
|
721 case (bs7 bs r) |
|
722 then show ?case |
|
723 by (simp add: bder_fuse r_in_rstar rrewrite_srewrite.bs7) |
|
724 next |
|
725 case (bs10 rs1 rs2 bs) |
|
726 then show ?case |
|
727 using contextrewrites0 by force |
|
728 next |
|
729 case ss1 |
|
730 then show ?case by simp |
|
731 next |
|
732 case (ss2 rs1 rs2 r) |
|
733 then show ?case |
|
734 by (simp add: srewrites7) |
|
735 next |
|
736 case (ss3 r1 r2 rs) |
|
737 then show ?case |
|
738 by (simp add: srewrites7) |
|
739 next |
|
740 case (ss4 rs) |
|
741 then show ?case |
|
742 using rrewrite_srewrite.ss4 by fastforce |
|
743 next |
|
744 case (ss5 bs1 rs1 rsb) |
|
745 then show ?case |
|
746 apply(simp) |
|
747 using bder_fuse_list map_map rrewrite_srewrite.ss5 srewrites.simps by blast |
|
748 next |
|
749 case (ss6 a1 a2 bs rsa rsb) |
|
750 then show ?case |
|
751 apply(simp only: map_append map1) |
|
752 apply(rule srewrites_trans) |
|
753 apply(rule rs_in_rstar) |
|
754 apply(rule_tac rrewrite_srewrite.ss6) |
|
755 using Der_def der_correctness apply auto[1] |
|
756 by blast |
|
757 qed |
|
758 *) |
|
759 |
651 |
760 |
652 |
761 lemma rewrites_to_bsimpStrong: |
653 lemma rewrites_to_bsimpStrong: |
762 shows "r \<leadsto>* bsimpStrong6 r" |
654 shows "r \<leadsto>* bsimpStrong6 r" |
763 proof (induction r rule: bsimpStrong6.induct) |
655 proof (induction r rule: bsimpStrong6.induct) |
800 also have "... \<leadsto>* bsimp_AALTs bs1 (distinctWith (flts (map bsimpStrong6 rs)) eq1 {})" |
692 also have "... \<leadsto>* bsimp_AALTs bs1 (distinctWith (flts (map bsimpStrong6 rs)) eq1 {})" |
801 by (simp add: bsimp_AALTs_rewrites) |
693 by (simp add: bsimp_AALTs_rewrites) |
802 finally show "AALTs bs1 rs \<leadsto>* bsimpStrong6 (AALTs bs1 rs)" sorry |
694 finally show "AALTs bs1 rs \<leadsto>* bsimpStrong6 (AALTs bs1 rs)" sorry |
803 qed (simp_all) |
695 qed (simp_all) |
804 |
696 |
805 lemma bders_simp_appendStrong : |
697 |
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 |
698 |
812 |
699 |
813 lemma centralStrong: |
700 lemma centralStrong: |
814 shows "bders r s \<leadsto>* bdersStrong6 r s" |
701 shows "bders r s \<leadsto>* bdersStrong6 r s" |
815 proof(induct s arbitrary: r rule: rev_induct) |
702 proof(induct s arbitrary: r rule: rev_induct) |
829 |
716 |
830 lemma mainStrong: |
717 lemma mainStrong: |
831 assumes "bnullable (bders r s)" |
718 assumes "bnullable (bders r s)" |
832 shows "bmkeps (bders r s) = bmkeps (bdersStrong6 r s)" |
719 shows "bmkeps (bders r s) = bmkeps (bdersStrong6 r s)" |
833 proof - |
720 proof - |
834 have "bders_simp r s \<leadsto>* bdersStrong6 r s" sorry |
721 have "bders r s \<leadsto>* bdersStrong6 r s" |
|
722 using centralStrong by force |
835 then |
723 then |
836 show "bmkeps (bders r s) = bmkeps (bdersStrong6 r s)" |
724 show "bmkeps (bders r s) = bmkeps (bdersStrong6 r s)" |
837 |
725 using assms rewrites_bmkeps by blast |
838 sorry |
|
839 qed |
726 qed |
840 |
727 |
841 |
728 |
842 |
729 |
843 |
730 |
844 theorem blexerStrong_correct : |
731 theorem blexerStrong_correct : |
845 shows "blexerStrong r s = blexer_simp r s" |
732 shows "blexerStrong r s = blexer r s" |
846 |
733 unfolding blexerStrong_def blexer_def |
847 sorry |
734 by (metis centralStrong mainStrong rewritesnullable) |
848 |
735 |
849 |
736 |
850 |
737 |
851 end |
738 end |