204 | "bder c (AALTs bs rs) = AALTs bs (map (bder c) rs)" |
204 | "bder c (AALTs bs rs) = AALTs bs (map (bder c) rs)" |
205 | "bder c (ASEQ bs r1 r2) = |
205 | "bder c (ASEQ bs r1 r2) = |
206 (if bnullable r1 |
206 (if bnullable r1 |
207 then AALT bs (ASEQ [] (bder c r1) r2) (fuse (bmkeps r1) (bder c r2)) |
207 then AALT bs (ASEQ [] (bder c r1) r2) (fuse (bmkeps r1) (bder c r2)) |
208 else ASEQ bs (bder c r1) r2)" |
208 else ASEQ bs (bder c r1) r2)" |
209 | "bder c (ASTAR bs r) = ASEQ bs (fuse [Z] (bder c r)) (ASTAR [] r)" |
209 | "bder c (ASTAR bs r) = ASEQ (bs @ [Z]) (bder c r) (ASTAR [] r)" |
210 |
210 |
211 |
211 |
212 fun |
212 fun |
213 bders :: "arexp \<Rightarrow> string \<Rightarrow> arexp" |
213 bders :: "arexp \<Rightarrow> string \<Rightarrow> arexp" |
214 where |
214 where |
564 (*| ss1: "[] s\<leadsto> []"*) |
564 (*| ss1: "[] s\<leadsto> []"*) |
565 | ss2: "rs1 s\<leadsto> rs2 \<Longrightarrow> (r # rs1) s\<leadsto> (r # rs2)" |
565 | ss2: "rs1 s\<leadsto> rs2 \<Longrightarrow> (r # rs1) s\<leadsto> (r # rs2)" |
566 | ss3: "r1 \<leadsto> r2 \<Longrightarrow> (r1 # rs) s\<leadsto> (r2 # rs)" |
566 | ss3: "r1 \<leadsto> r2 \<Longrightarrow> (r1 # rs) s\<leadsto> (r2 # rs)" |
567 | ss4: "(AZERO # rs) s\<leadsto> rs" |
567 | ss4: "(AZERO # rs) s\<leadsto> rs" |
568 | ss5: "(AALTs bs1 rs1 # rsb) s\<leadsto> ((map (fuse bs1) rs1) @ rsb)" |
568 | ss5: "(AALTs bs1 rs1 # rsb) s\<leadsto> ((map (fuse bs1) rs1) @ rsb)" |
569 | ss6: "erase a1 = erase a2 \<Longrightarrow> (rsa@[a1]@rsb@[a2]@rsc) s\<leadsto> (rsa@[a1]@rsb@rsc)" |
569 | ss6: "L(erase a2) \<subseteq> L(erase a1) \<Longrightarrow> (rsa@[a1]@rsb@[a2]@rsc) s\<leadsto> (rsa@[a1]@rsb@rsc)" |
570 |
570 (*| extra: "bnullable r1 \<Longrightarrow> ASEQ bs0 (ASEQ bs1 r1 r2) r3 \<leadsto> |
|
571 ASEQ (bs0 @ bs1) r1 (ASEQ [] r2 r3)" |
|
572 *) |
571 |
573 |
572 inductive |
574 inductive |
573 rrewrites:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100) |
575 rrewrites:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100) |
574 where |
576 where |
575 rs1[intro, simp]:"r \<leadsto>* r" |
577 rs1[intro, simp]:"r \<leadsto>* r" |
582 | sss2[intro]: "\<lbrakk>rs1 s\<leadsto> rs2; rs2 s\<leadsto>* rs3\<rbrakk> \<Longrightarrow> rs1 s\<leadsto>* rs3" |
584 | sss2[intro]: "\<lbrakk>rs1 s\<leadsto> rs2; rs2 s\<leadsto>* rs3\<rbrakk> \<Longrightarrow> rs1 s\<leadsto>* rs3" |
583 |
585 |
584 |
586 |
585 lemma r_in_rstar: |
587 lemma r_in_rstar: |
586 shows "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2" |
588 shows "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2" |
|
589 using rrewrites.intros(1) rrewrites.intros(2) by blast |
|
590 |
|
591 lemma rs_in_rstar: |
|
592 shows "r1 s\<leadsto> r2 \<Longrightarrow> r1 s\<leadsto>* r2" |
587 using rrewrites.intros(1) rrewrites.intros(2) by blast |
593 using rrewrites.intros(1) rrewrites.intros(2) by blast |
588 |
594 |
589 lemma rrewrites_trans[trans]: |
595 lemma rrewrites_trans[trans]: |
590 assumes a1: "r1 \<leadsto>* r2" and a2: "r2 \<leadsto>* r3" |
596 assumes a1: "r1 \<leadsto>* r2" and a2: "r2 \<leadsto>* r3" |
591 shows "r1 \<leadsto>* r3" |
597 shows "r1 \<leadsto>* r3" |
672 |
678 |
673 lemma ss6_stronger_aux: |
679 lemma ss6_stronger_aux: |
674 shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ distinctBy rs2 erase (set (map erase rs1)))" |
680 shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ distinctBy rs2 erase (set (map erase rs1)))" |
675 apply(induct rs2 arbitrary: rs1) |
681 apply(induct rs2 arbitrary: rs1) |
676 apply(auto) |
682 apply(auto) |
677 apply (smt (verit, best) append.assoc append.right_neutral append_Cons append_Nil split_list srewrite2(2) srewrites_trans ss6) |
683 prefer 2 |
678 apply(drule_tac x="rs1 @ [a]" in meta_spec) |
684 apply(drule_tac x="rs1 @ [a]" in meta_spec) |
679 apply(simp) |
685 apply(simp) |
680 done |
686 apply(drule_tac x="rs1" in meta_spec) |
|
687 apply(subgoal_tac "(rs1 @ a # rs2) s\<leadsto>* (rs1 @ rs2)") |
|
688 using srewrites_trans apply blast |
|
689 apply(subgoal_tac "\<exists>rs1a rs1b. rs1 = rs1a @ [x] @ rs1b") |
|
690 prefer 2 |
|
691 apply (simp add: split_list) |
|
692 apply(erule exE)+ |
|
693 apply(simp) |
|
694 using ss6[simplified] |
|
695 using rs_in_rstar by force |
681 |
696 |
682 lemma ss6_stronger: |
697 lemma ss6_stronger: |
683 shows "rs1 s\<leadsto>* distinctBy rs1 erase {}" |
698 shows "rs1 s\<leadsto>* distinctBy rs1 erase {}" |
684 using ss6_stronger_aux[of "[]" _] by auto |
699 using ss6_stronger_aux[of "[]" _] by auto |
685 |
700 |
708 also have "... s\<leadsto> ((map (fuse (bs @ bs1)) rs1) @ (map (fuse bs) rsb))" |
723 also have "... s\<leadsto> ((map (fuse (bs @ bs1)) rs1) @ (map (fuse bs) rsb))" |
709 by (simp add: rrewrite_srewrite.ss5) |
724 by (simp add: rrewrite_srewrite.ss5) |
710 finally show "map (fuse bs) (AALTs bs1 rs1 # rsb) s\<leadsto> map (fuse bs) (map (fuse bs1) rs1 @ rsb)" |
725 finally show "map (fuse bs) (AALTs bs1 rs1 # rsb) s\<leadsto> map (fuse bs) (map (fuse bs1) rs1 @ rsb)" |
711 by (simp add: comp_def fuse_append) |
726 by (simp add: comp_def fuse_append) |
712 next |
727 next |
713 case (ss6 a1 a2 rsa rsb rsc) |
728 case (ss6 a2 a1 rsa rsb rsc) |
|
729 have "L (erase a2) \<subseteq> L (erase a1)" by fact |
714 then show "map (fuse bs) (rsa @ [a1] @ rsb @ [a2] @ rsc) s\<leadsto> map (fuse bs) (rsa @ [a1] @ rsb @ rsc)" |
730 then show "map (fuse bs) (rsa @ [a1] @ rsb @ [a2] @ rsc) s\<leadsto> map (fuse bs) (rsa @ [a1] @ rsb @ rsc)" |
715 apply(simp) |
731 apply(simp) |
716 apply(rule rrewrite_srewrite.ss6[simplified]) |
732 apply(rule rrewrite_srewrite.ss6[simplified]) |
717 apply(simp add: erase_fuse) |
733 apply(simp add: erase_fuse) |
718 done |
734 done |
|
735 (*next |
|
736 case (extra bs0 bs1 r1 r2 r3) |
|
737 then show ?case |
|
738 by (metis append_assoc fuse.simps(5) rrewrite_srewrite.extra)*) |
719 qed (auto intro: rrewrite_srewrite.intros) |
739 qed (auto intro: rrewrite_srewrite.intros) |
720 |
740 |
721 lemma rewrites_fuse: |
741 lemma rewrites_fuse: |
722 assumes "r1 \<leadsto>* r2" |
742 assumes "r1 \<leadsto>* r2" |
723 shows "fuse bs r1 \<leadsto>* fuse bs r2" |
743 shows "fuse bs r1 \<leadsto>* fuse bs r2" |
785 lemma bnullable0: |
805 lemma bnullable0: |
786 shows "r1 \<leadsto> r2 \<Longrightarrow> bnullable r1 = bnullable r2" |
806 shows "r1 \<leadsto> r2 \<Longrightarrow> bnullable r1 = bnullable r2" |
787 and "rs1 s\<leadsto> rs2 \<Longrightarrow> bnullables rs1 = bnullables rs2" |
807 and "rs1 s\<leadsto> rs2 \<Longrightarrow> bnullables rs1 = bnullables rs2" |
788 apply(induct rule: rrewrite_srewrite.inducts) |
808 apply(induct rule: rrewrite_srewrite.inducts) |
789 apply(auto simp add: bnullable_fuse) |
809 apply(auto simp add: bnullable_fuse) |
790 apply (meson UnCI bnullable_fuse imageI) |
810 apply (meson UnCI bnullable_fuse imageI) |
791 by (metis bnullable_correctness) |
811 |
|
812 using bnullable_correctness nullable_correctness by blast |
792 |
813 |
793 |
814 |
794 lemma rewrites_bnullable_eq: |
815 lemma rewrites_bnullable_eq: |
795 assumes "r1 \<leadsto>* r2" |
816 assumes "r1 \<leadsto>* r2" |
796 shows "bnullable r1 = bnullable r2" |
817 shows "bnullable r1 = bnullable r2" |
822 case (ss5 bs1 rs1 rsb) |
843 case (ss5 bs1 rs1 rsb) |
823 have "bnullables (AALTs bs1 rs1 # rsb)" by fact |
844 have "bnullables (AALTs bs1 rs1 # rsb)" by fact |
824 then show "bmkepss (AALTs bs1 rs1 # rsb) = bmkepss (map (fuse bs1) rs1 @ rsb)" |
845 then show "bmkepss (AALTs bs1 rs1 # rsb) = bmkepss (map (fuse bs1) rs1 @ rsb)" |
825 by (simp add: bmkepss1 bmkepss2 bmkepss_fuse bnullable_fuse) |
846 by (simp add: bmkepss1 bmkepss2 bmkepss_fuse bnullable_fuse) |
826 next |
847 next |
827 case (ss6 a1 a2 rsa rsb rsc) |
848 case (ss6 a2 a1 rsa rsb rsc) |
828 have as1: "erase a1 = erase a2" by fact |
849 have as1: "L(erase a2) \<subseteq> L(erase a1)" by fact |
829 have as3: "bnullables (rsa @ [a1] @ rsb @ [a2] @ rsc)" by fact |
850 have as3: "bnullables (rsa @ [a1] @ rsb @ [a2] @ rsc)" by fact |
830 show "bmkepss (rsa @ [a1] @ rsb @ [a2] @ rsc) = bmkepss (rsa @ [a1] @ rsb @ rsc)" using as1 as3 |
851 show "bmkepss (rsa @ [a1] @ rsb @ [a2] @ rsc) = bmkepss (rsa @ [a1] @ rsb @ rsc)" using as1 as3 |
831 by (smt (verit, best) append_Cons bmkeps.simps(3) bmkepss.simps(2) bmkepss1 bmkepss2 bnullable_correctness) |
852 by (smt (verit, ccfv_SIG) append_Cons bmkepss.simps(2) bmkepss1 bmkepss2 bnullable_correctness nullable_correctness subset_eq) |
|
853 (*next |
|
854 case (extra bs0 bs1 r1 bs2 r2 bs4 bs3) |
|
855 then show ?case |
|
856 apply(subst bmkeps.simps) |
|
857 apply(subst bmkeps.simps) |
|
858 apply(subst bmkeps.simps) |
|
859 apply(subst bmkeps.simps) |
|
860 apply(subst bmkeps.simps) |
|
861 apply(subst bmkeps.simps) |
|
862 apply(simp) |
|
863 done*) |
832 qed (auto) |
864 qed (auto) |
833 |
865 |
834 lemma rewrites_bmkeps: |
866 lemma rewrites_bmkeps: |
835 assumes "r1 \<leadsto>* r2" "bnullable r1" |
867 assumes "r1 \<leadsto>* r2" "bnullable r1" |
836 shows "bmkeps r1 = bmkeps r2" |
868 shows "bmkeps r1 = bmkeps r2" |
906 shows "map (bder c \<circ> fuse bs1) rs1 = map (fuse bs1 \<circ> bder c) rs1" |
938 shows "map (bder c \<circ> fuse bs1) rs1 = map (fuse bs1 \<circ> bder c) rs1" |
907 apply(induction rs1) |
939 apply(induction rs1) |
908 apply(simp_all add: bder_fuse) |
940 apply(simp_all add: bder_fuse) |
909 done |
941 done |
910 |
942 |
|
943 lemma map_single: |
|
944 shows "map f [x] = [f x]" |
|
945 by simp |
|
946 |
|
947 |
911 lemma rewrite_preserves_bder: |
948 lemma rewrite_preserves_bder: |
912 shows "r1 \<leadsto> r2 \<Longrightarrow> bder c r1 \<leadsto>* bder c r2" |
949 shows "r1 \<leadsto> r2 \<Longrightarrow> bder c r1 \<leadsto>* bder c r2" |
913 and "rs1 s\<leadsto> rs2 \<Longrightarrow> map (bder c) rs1 s\<leadsto>* map (bder c) rs2" |
950 and "rs1 s\<leadsto> rs2 \<Longrightarrow> map (bder c) rs1 s\<leadsto>* map (bder c) rs2" |
914 proof(induction rule: rrewrite_srewrite.inducts) |
951 proof(induction rule: rrewrite_srewrite.inducts) |
915 case (bs1 bs r2) |
952 case (bs1 bs r2) |
975 case (ss5 bs1 rs1 rsb) |
1012 case (ss5 bs1 rs1 rsb) |
976 show "map (bder c) (AALTs bs1 rs1 # rsb) s\<leadsto>* map (bder c) (map (fuse bs1) rs1 @ rsb)" |
1013 show "map (bder c) (AALTs bs1 rs1 # rsb) s\<leadsto>* map (bder c) (map (fuse bs1) rs1 @ rsb)" |
977 apply(simp) |
1014 apply(simp) |
978 using bder_fuse_list map_map rrewrite_srewrite.ss5 srewrites.simps by blast |
1015 using bder_fuse_list map_map rrewrite_srewrite.ss5 srewrites.simps by blast |
979 next |
1016 next |
980 case (ss6 a1 a2 bs rsa rsb) |
1017 case (ss6 a2 a1 bs rsa rsb) |
981 have as: "erase a1 = erase a2" by fact |
1018 have as: "L(erase a2) \<subseteq> L(erase a1)" by fact |
982 show "map (bder c) (bs @ [a1] @ rsa @ [a2] @ rsb) s\<leadsto>* map (bder c) (bs @ [a1] @ rsa @ rsb)" |
1019 show "map (bder c) (bs @ [a1] @ rsa @ [a2] @ rsb) s\<leadsto>* map (bder c) (bs @ [a1] @ rsa @ rsb)" |
983 apply(simp only: map_append) |
1020 apply(simp only: map_append) |
984 by (smt (verit, best) erase_bder list.simps(8) list.simps(9) as rrewrite_srewrite.ss6 srewrites.simps) |
1021 apply(simp only: map_single) |
|
1022 apply(rule rs_in_rstar) |
|
1023 thm rrewrite_srewrite.intros |
|
1024 apply(rule rrewrite_srewrite.ss6) |
|
1025 using as |
|
1026 apply(auto simp add: der_correctness Der_def) |
|
1027 done |
|
1028 (*next |
|
1029 case (extra bs0 bs1 r1 r2 r3) |
|
1030 then show ?case |
|
1031 apply(auto simp add: comp_def) |
|
1032 |
|
1033 defer |
|
1034 using r_in_rstar rrewrite_srewrite.extra apply presburger |
|
1035 prefer 2 |
|
1036 using r_in_rstar rrewrite_srewrite.extra apply presburger |
|
1037 prefer 2 |
|
1038 sorry*) |
985 qed |
1039 qed |
|
1040 |
|
1041 |
986 |
1042 |
987 lemma rewrites_preserves_bder: |
1043 lemma rewrites_preserves_bder: |
988 assumes "r1 \<leadsto>* r2" |
1044 assumes "r1 \<leadsto>* r2" |
989 shows "bder c r1 \<leadsto>* bder c r2" |
1045 shows "bder c r1 \<leadsto>* bder c r2" |
990 using assms |
1046 using assms |
991 apply(induction r1 r2 rule: rrewrites.induct) |
1047 apply(induction r1 r2 rule: rrewrites.induct) |
992 apply(simp_all add: rewrite_preserves_bder rrewrites_trans) |
1048 apply(simp_all add: rewrite_preserves_bder rrewrites_trans) |
993 done |
1049 done |
994 |
1050 |
995 |
1051 |
996 lemma central: |
1052 lemma central: |
997 shows "bders r s \<leadsto>* bders_simp r s" |
1053 shows "bders r s \<leadsto>* bders_simp r s" |
998 proof(induct s arbitrary: r rule: rev_induct) |
1054 proof(induct s arbitrary: r rule: rev_induct) |
1032 using blexer_correctness main_blexer_simp by simp |
1088 using blexer_correctness main_blexer_simp by simp |
1033 |
1089 |
1034 |
1090 |
1035 (* some tests *) |
1091 (* some tests *) |
1036 |
1092 |
|
1093 definition |
|
1094 bders_simp_Set :: "string set \<Rightarrow> arexp \<Rightarrow> arexp set" |
|
1095 where |
|
1096 "bders_simp_Set A r \<equiv> bders_simp r ` A" |
|
1097 |
|
1098 lemma pders_Set_union: |
|
1099 shows "bders_simp_Set (A \<union> B) r = (bders_simp_Set A r \<union> bders_simp_Set B r)" |
|
1100 apply (simp add: bders_simp_Set_def) |
|
1101 by (simp add: image_Un) |
|
1102 |
|
1103 lemma pders_Set_subset: |
|
1104 shows "A \<subseteq> B \<Longrightarrow> bders_simp_Set A r \<subseteq> bders_simp_Set B r" |
|
1105 apply (auto simp add: bders_simp_Set_def) |
|
1106 done |
|
1107 |
|
1108 |
|
1109 lemma AZERO_r: |
|
1110 "bders_simp AZERO s = AZERO" |
|
1111 apply(induct s) |
|
1112 apply(auto) |
|
1113 done |
|
1114 |
|
1115 lemma bders_simp_Set_ZERO [simp]: |
|
1116 shows "bders_simp_Set UNIV1 AZERO \<subseteq> {AZERO}" |
|
1117 unfolding UNIV1_def bders_simp_Set_def |
|
1118 apply(auto) |
|
1119 using AZERO_r by blast |
|
1120 |
|
1121 lemma AONE_r: |
|
1122 shows "bders_simp (AONE bs) s = AZERO \<or> bders_simp (AONE bs) s = AONE bs" |
|
1123 apply(induct s) |
|
1124 apply(auto) |
|
1125 using AZERO_r apply blast |
|
1126 using AZERO_r by blast |
|
1127 |
|
1128 lemma bders_simp_Set_ONE [simp]: |
|
1129 shows "bders_simp_Set UNIV1 (AONE bs) \<subseteq> {AZERO, AONE bs}" |
|
1130 unfolding UNIV1_def bders_simp_Set_def |
|
1131 apply(auto split: if_splits) |
|
1132 using AONE_r by blast |
|
1133 |
|
1134 lemma ACHAR_r: |
|
1135 shows "bders_simp (ACHAR bs c) s = AZERO \<or> |
|
1136 bders_simp (ACHAR bs c) s = AONE bs \<or> |
|
1137 bders_simp (ACHAR bs c) s = ACHAR bs c" |
|
1138 apply(induct s) |
|
1139 apply(auto) |
|
1140 using AONE_r apply blast |
|
1141 using AZERO_r apply force |
|
1142 using AONE_r apply blast |
|
1143 using AZERO_r apply blast |
|
1144 using AONE_r apply blast |
|
1145 using AZERO_r by blast |
|
1146 |
|
1147 lemma bders_simp_Set_CHAR [simp]: |
|
1148 shows "bders_simp_Set UNIV1 (ACHAR bs c) \<subseteq> {AZERO, AONE bs, ACHAR bs c}" |
|
1149 unfolding UNIV1_def bders_simp_Set_def |
|
1150 apply(auto) |
|
1151 using ACHAR_r by blast |
|
1152 |
|
1153 lemma bders_simp_Set_ALT [simp]: |
|
1154 shows "bders_simp_Set UNIV1 (AALT bs r1 r2) = bders_simp_Set UNIV1 r1 \<union> bders_simp_Set UNIV1 r2" |
|
1155 unfolding UNIV1_def bders_simp_Set_def |
|
1156 apply(auto) |
|
1157 oops |
|
1158 |
|
1159 |
|
1160 |
|
1161 |
|
1162 (* |
1037 lemma asize_fuse: |
1163 lemma asize_fuse: |
1038 shows "asize (fuse bs r) = asize r" |
1164 shows "asize (fuse bs r) = asize r" |
1039 apply(induct r arbitrary: bs) |
1165 apply(induct r arbitrary: bs) |
1040 apply(auto) |
1166 apply(auto) |
1041 done |
1167 done |
1370 apply(rule order_trans) |
1496 apply(rule order_trans) |
1371 apply(rule pders_SEQs) |
1497 apply(rule pders_SEQs) |
1372 using finite_pder apply blast |
1498 using finite_pder apply blast |
1373 oops |
1499 oops |
1374 |
1500 |
1375 |
1501 *) |
1376 |
1502 |
1377 |
1503 |
1378 (* below is the idempotency of bsimp *) |
1504 (* below is the idempotency of bsimp *) |
|
1505 |
|
1506 (* |
1379 |
1507 |
1380 lemma bsimp_ASEQ_fuse: |
1508 lemma bsimp_ASEQ_fuse: |
1381 shows "fuse bs1 (bsimp_ASEQ bs2 r1 r2) = bsimp_ASEQ (bs1 @ bs2) r1 r2" |
1509 shows "fuse bs1 (bsimp_ASEQ bs2 r1 r2) = bsimp_ASEQ (bs1 @ bs2) r1 r2" |
1382 apply(induct r1 r2 arbitrary: bs1 bs2 rule: bsimp_ASEQ.induct) |
1510 apply(induct r1 r2 arbitrary: bs1 bs2 rule: bsimp_ASEQ.induct) |
1383 apply(auto) |
1511 apply(auto) |
1464 apply(erule rrewrite.cases) |
1592 apply(erule rrewrite.cases) |
1465 apply simp |
1593 apply simp |
1466 apply auto |
1594 apply auto |
1467 |
1595 |
1468 oops |
1596 oops |
|
1597 *) |
|
1598 |
1469 |
1599 |
1470 (* |
1600 (* |
1471 AALTs [] [AZERO, AALTs(bs1, [a, b]) ] |
1601 AALTs [] [AZERO, AALTs(bs1, [a, b]) ] |
1472 rewrite seq 1: \<leadsto> AALTs [] [ AALTs(bs1, [a, b]) ] \<leadsto> |
1602 rewrite seq 1: \<leadsto> AALTs [] [ AALTs(bs1, [a, b]) ] \<leadsto> |
1473 fuse [] (AALTs bs1, [a, b]) |
1603 fuse [] (AALTs bs1, [a, b]) |
1474 rewrite seq 2: \<leadsto> AALTs [] [AZERO, (fuse bs1 a), (fuse bs1 b)]) ] |
1604 rewrite seq 2: \<leadsto> AALTs [] [AZERO, (fuse bs1 a), (fuse bs1 b)]) ] |
1475 |
1605 |
1476 *) |
1606 *) |
1477 |
1607 |
1478 lemma normal_bsimp: |
|
1479 shows "\<nexists>r'. bsimp r \<leadsto> r'" |
|
1480 oops |
|
1481 |
1608 |
1482 (*r' size bsimp r > size r' |
1609 (*r' size bsimp r > size r' |
1483 r' \<leadsto>* bsimp bsimp r |
1610 r' \<leadsto>* bsimp bsimp r |
1484 size bsimp r > size r' \<ge> size bsimp bsimp r*) |
1611 size bsimp r > size r' \<ge> size bsimp bsimp r*) |
1485 |
1612 |
1486 export_code blexer_simp blexer lexer bders bders_simp in Scala module_name VerifiedLexers |
|
1487 |
|
1488 |
1613 |
1489 unused_thms |
1614 unused_thms |
1490 |
1615 |
1491 |
1616 (* |
1492 inductive aggressive:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>? _" [99, 99] 99) |
1617 inductive aggressive:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>? _" [99, 99] 99) |
1493 where |
1618 where |
1494 "ASEQ bs (AALTs bs1 rs) r \<leadsto>? AALTs (bs@bs1) (map (\<lambda>r'. ASEQ [] r' r) rs) " |
1619 "ASEQ bs (AALTs bs1 rs) r \<leadsto>? AALTs (bs@bs1) (map (\<lambda>r'. ASEQ [] r' r) rs) " |
1495 |
1620 *) |
1496 |
1621 |
1497 |
1622 |
1498 end |
1623 end |