557 "bsimp_ASEQ _ AZERO _ = AZERO" |
560 "bsimp_ASEQ _ AZERO _ = AZERO" |
558 | "bsimp_ASEQ _ _ AZERO = AZERO" |
561 | "bsimp_ASEQ _ _ AZERO = AZERO" |
559 | "bsimp_ASEQ bs1 (AONE bs2) r2 = fuse (bs1 @ bs2) r2" |
562 | "bsimp_ASEQ bs1 (AONE bs2) r2 = fuse (bs1 @ bs2) r2" |
560 | "bsimp_ASEQ bs1 r1 r2 = ASEQ bs1 r1 r2" |
563 | "bsimp_ASEQ bs1 r1 r2 = ASEQ bs1 r1 r2" |
561 |
564 |
|
565 lemma bsimp_ASEQ0[simp]: |
|
566 shows "bsimp_ASEQ bs r1 AZERO = AZERO" |
|
567 by (case_tac r1)(simp_all) |
|
568 |
|
569 lemma bsimp_ASEQ1: |
|
570 assumes "r1 \<noteq> AZERO" "r2 \<noteq> AZERO" "\<nexists>bs. r1 = AONE bs" |
|
571 shows "bsimp_ASEQ bs r1 r2 = ASEQ bs r1 r2" |
|
572 using assms |
|
573 apply(induct bs r1 r2 rule: bsimp_ASEQ.induct) |
|
574 apply(auto) |
|
575 done |
|
576 |
|
577 lemma bsimp_ASEQ2[simp]: |
|
578 shows "bsimp_ASEQ bs1 (AONE bs2) r2 = fuse (bs1 @ bs2) r2" |
|
579 by (case_tac r2) (simp_all) |
|
580 |
562 |
581 |
563 fun bsimp_AALTs :: "bit list \<Rightarrow> arexp list \<Rightarrow> arexp" |
582 fun bsimp_AALTs :: "bit list \<Rightarrow> arexp list \<Rightarrow> arexp" |
564 where |
583 where |
565 "bsimp_AALTs _ [] = AZERO" |
584 "bsimp_AALTs _ [] = AZERO" |
566 | "bsimp_AALTs bs1 [r] = fuse bs1 r" |
585 | "bsimp_AALTs bs1 [r] = fuse bs1 r" |
945 |
939 |
946 lemma srewrites6: |
940 lemma srewrites6: |
947 assumes "r1 \<leadsto>* r2" |
941 assumes "r1 \<leadsto>* r2" |
948 shows "[r1] s\<leadsto>* [r2]" |
942 shows "[r1] s\<leadsto>* [r2]" |
949 using assms |
943 using assms |
950 |
|
951 apply(induct r1 r2 rule: rrewrites.induct) |
944 apply(induct r1 r2 rule: rrewrites.induct) |
952 apply(auto) |
945 apply(auto) |
953 by (meson srewrites.simps srewrites_trans ss3) |
946 by (meson srewrites.simps srewrites_trans ss3) |
954 |
947 |
955 lemma srewrites7: |
948 lemma srewrites7: |
956 assumes "rs3 s\<leadsto>* rs4" "r1 \<leadsto>* r2" |
949 assumes "rs3 s\<leadsto>* rs4" "r1 \<leadsto>* r2" |
957 shows "(r1 # rs3) s\<leadsto>* (r2 # rs4)" |
950 shows "(r1 # rs3) s\<leadsto>* (r2 # rs4)" |
958 using assms |
951 using assms |
959 by (smt (verit, best) append_Cons append_Nil srewrites1 srewrites3 srewrites6 srewrites_trans) |
952 by (smt (verit, best) append_Cons append_Nil srewrites1 srewrites3 srewrites6 srewrites_trans) |
960 |
953 |
|
954 lemma ss6_stronger_aux: |
|
955 shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ distinctBy rs2 erase (set (map erase rs1)))" |
|
956 apply(induct rs2 arbitrary: rs1) |
|
957 apply(auto) |
|
958 apply (smt (verit, best) append.assoc append.right_neutral append_Cons append_Nil split_list srewrite2(2) srewrites_trans ss6) |
|
959 apply(drule_tac x="rs1 @ [a]" in meta_spec) |
|
960 apply(simp) |
|
961 done |
|
962 |
|
963 lemma ss6_stronger: |
|
964 shows "rs1 s\<leadsto>* distinctBy rs1 erase {}" |
|
965 using ss6_stronger_aux[of "[]" _] by auto |
|
966 |
|
967 |
|
968 lemma rewrite_preserves_fuse: |
|
969 shows "r2 \<leadsto> r3 \<Longrightarrow> fuse bs r2 \<leadsto> fuse bs r3" |
|
970 and "rs2 s\<leadsto> rs3 \<Longrightarrow> map (fuse bs) rs2 s\<leadsto>* map (fuse bs) rs3" |
|
971 proof(induct rule: rrewrite_srewrite.inducts) |
|
972 case (bs3 bs1 bs2 r) |
|
973 then show ?case |
|
974 by (metis fuse.simps(5) fuse_append rrewrite_srewrite.bs3) |
|
975 next |
|
976 case (bs7 bs r) |
|
977 then show ?case |
|
978 by (metis fuse.simps(4) fuse_append rrewrite_srewrite.bs7) |
|
979 next |
|
980 case (ss2 rs1 rs2 r) |
|
981 then show ?case |
|
982 using srewrites7 by force |
|
983 next |
|
984 case (ss3 r1 r2 rs) |
|
985 then show ?case by (simp add: r_in_rstar srewrites7) |
|
986 next |
|
987 case (ss5 bs1 rs1 rsb) |
|
988 then show ?case |
|
989 apply(simp) |
|
990 by (metis (mono_tags, lifting) comp_def fuse_append map_eq_conv rrewrite_srewrite.ss5 srewrites.simps) |
|
991 next |
|
992 case (ss6 a1 a2 rsa rsb rsc) |
|
993 then show ?case |
|
994 apply(simp only: map_append) |
|
995 by (smt (verit, ccfv_threshold) erase_fuse list.simps(8) list.simps(9) rrewrite_srewrite.ss6 srewrites.simps) |
|
996 qed (auto intro: rrewrite_srewrite.intros) |
|
997 |
|
998 |
|
999 lemma rewrites_fuse: |
|
1000 assumes "r1 \<leadsto>* r2" |
|
1001 shows "fuse bs r1 \<leadsto>* fuse bs r2" |
|
1002 using assms |
|
1003 apply(induction r1 r2 arbitrary: bs rule: rrewrites.induct) |
|
1004 apply(auto intro: rewrite_preserves_fuse rrewrites_trans) |
|
1005 done |
961 |
1006 |
962 |
1007 |
963 lemma star_seq: |
1008 lemma star_seq: |
964 assumes "r1 \<leadsto>* r2" |
1009 assumes "r1 \<leadsto>* r2" |
965 shows "ASEQ bs r1 r3 \<leadsto>* ASEQ bs r2 r3" |
1010 shows "ASEQ bs r1 r3 \<leadsto>* ASEQ bs r2 r3" |
979 lemma continuous_rewrite: |
1024 lemma continuous_rewrite: |
980 assumes "r1 \<leadsto>* AZERO" |
1025 assumes "r1 \<leadsto>* AZERO" |
981 shows "ASEQ bs1 r1 r2 \<leadsto>* AZERO" |
1026 shows "ASEQ bs1 r1 r2 \<leadsto>* AZERO" |
982 using assms bs1 star_seq by blast |
1027 using assms bs1 star_seq by blast |
983 |
1028 |
|
1029 (* |
|
1030 lemma continuous_rewrite2: |
|
1031 assumes "r1 \<leadsto>* AONE bs" |
|
1032 shows "ASEQ bs1 r1 r2 \<leadsto>* (fuse (bs1 @ bs) r2)" |
|
1033 using assms by (meson bs3 rrewrites.simps star_seq) |
|
1034 *) |
984 |
1035 |
985 lemma bsimp_aalts_simpcases: |
1036 lemma bsimp_aalts_simpcases: |
986 shows "AONE bs \<leadsto>* bsimp (AONE bs)" |
1037 shows "AONE bs \<leadsto>* bsimp (AONE bs)" |
987 and "AZERO \<leadsto>* bsimp AZERO" |
1038 and "AZERO \<leadsto>* bsimp AZERO" |
988 and "ACHAR bs c \<leadsto>* bsimp (ACHAR bs c)" |
1039 and "ACHAR bs c \<leadsto>* bsimp (ACHAR bs c)" |
989 by (simp_all) |
1040 by (simp_all) |
990 |
1041 |
|
1042 lemma bsimp_AALTs_rewrites: |
|
1043 shows "AALTs bs1 rs \<leadsto>* bsimp_AALTs bs1 rs" |
|
1044 by (smt (verit) bs6 bs7 bsimp_AALTs.elims rrewrites.simps) |
991 |
1045 |
992 lemma trivialbsimp_srewrites: |
1046 lemma trivialbsimp_srewrites: |
993 "\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x \<rbrakk> \<Longrightarrow> rs s\<leadsto>* (map f rs)" |
1047 "\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x \<rbrakk> \<Longrightarrow> rs s\<leadsto>* (map f rs)" |
994 apply(induction rs) |
1048 apply(induction rs) |
995 apply simp |
1049 apply simp |
996 apply(simp) |
1050 apply(simp) |
997 using srewrites7 by auto |
1051 using srewrites7 by auto |
998 |
1052 |
999 lemma alts_simpalts: |
1053 |
1000 "(\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimp x) \<Longrightarrow> |
|
1001 AALTs bs1 rs \<leadsto>* AALTs bs1 (map bsimp rs)" |
|
1002 apply(induct rs) |
|
1003 apply(auto)[1] |
|
1004 using trivialbsimp_srewrites apply auto[1] |
|
1005 by (simp add: contextrewrites0 srewrites7) |
|
1006 |
|
1007 |
|
1008 lemma bsimp_AALTs_rewrites: |
|
1009 shows "AALTs bs1 rs \<leadsto>* bsimp_AALTs bs1 rs" |
|
1010 by (smt (verit) bs6 bs7 bsimp_AALTs.elims rrewrites.simps) |
|
1011 |
1054 |
1012 lemma fltsfrewrites: "rs s\<leadsto>* (flts rs)" |
1055 lemma fltsfrewrites: "rs s\<leadsto>* (flts rs)" |
1013 |
1056 apply(induction rs rule: flts.induct) |
1014 apply(induction rs) |
1057 apply(auto intro: rrewrite_srewrite.intros) |
1015 apply simp |
1058 apply (meson srewrites.simps srewrites1 ss5) |
1016 apply(case_tac a) |
|
1017 apply(auto) |
|
1018 using ss4 apply blast |
|
1019 using srewrites7 apply force |
|
1020 using rs1 srewrites7 apply presburger |
1059 using rs1 srewrites7 apply presburger |
1021 using srewrites7 apply force |
1060 using srewrites7 apply force |
1022 apply (meson srewrites.simps srewrites1 ss5) |
1061 apply (simp add: srewrites7) |
1023 by (simp add: srewrites7) |
1062 by (simp add: srewrites7) |
1024 |
1063 |
1025 |
|
1026 lemma flts_rewrites: "AALTs bs1 rs \<leadsto>* AALTs bs1 (flts rs)" |
|
1027 by (simp add: contextrewrites0 fltsfrewrites) |
|
1028 |
|
1029 |
|
1030 (* delete*) |
|
1031 lemma threelistsappend: "rsa@a#rsb = (rsa@[a])@rsb" |
|
1032 apply auto |
|
1033 done |
|
1034 |
|
1035 lemma somewhereInside: "r \<in> set rs \<Longrightarrow> \<exists>rs1 rs2. rs = rs1@[r]@rs2" |
|
1036 using split_list by fastforce |
|
1037 |
|
1038 lemma somewhereMapInside: "f r \<in> f ` set rs \<Longrightarrow> \<exists>rs1 rs2 a. rs = rs1@[a]@rs2 \<and> f a = f r" |
|
1039 apply auto |
|
1040 by (metis split_list) |
|
1041 |
|
1042 lemma alts_dBrewrites_withFront: |
|
1043 "AALTs bs (rsa @ rs) \<leadsto>* AALTs bs (rsa @ distinctBy rs erase (erase ` set rsa))" |
|
1044 |
|
1045 apply(induction rs arbitrary: rsa) |
|
1046 apply simp |
|
1047 |
|
1048 apply(drule_tac x = "rsa@[a]" in meta_spec) |
|
1049 |
|
1050 apply(subst threelistsappend) |
|
1051 apply(rule rrewrites_trans) |
|
1052 apply simp |
|
1053 |
|
1054 apply(case_tac "a \<in> set rsa") |
|
1055 apply simp |
|
1056 apply(drule somewhereInside) |
|
1057 apply(erule exE)+ |
|
1058 apply simp |
|
1059 using bs10 ss6 apply auto[1] |
|
1060 |
|
1061 apply(subgoal_tac "erase ` set (rsa @ [a]) = insert (erase a) (erase ` set rsa)") |
|
1062 prefer 2 |
|
1063 |
|
1064 apply auto[1] |
|
1065 apply(case_tac "erase a \<in> erase `set rsa") |
|
1066 |
|
1067 apply simp |
|
1068 apply(subgoal_tac "AALTs bs (rsa @ a # distinctBy rs erase (insert (erase a) (erase ` set rsa))) \<leadsto> |
|
1069 AALTs bs (rsa @ distinctBy rs erase (insert (erase a) (erase ` set rsa)))") |
|
1070 apply force |
|
1071 apply (smt (verit, ccfv_threshold) append.assoc append.left_neutral append_Cons append_Nil bs10 imageE insertCI insert_image somewhereMapInside ss6) |
|
1072 by simp |
|
1073 |
|
1074 |
|
1075 |
|
1076 lemma alts_dBrewrites: |
|
1077 shows "AALTs bs rs \<leadsto>* AALTs bs (distinctBy rs erase {})" |
|
1078 |
|
1079 apply(induction rs) |
|
1080 apply simp |
|
1081 apply simp |
|
1082 using alts_dBrewrites_withFront |
|
1083 by (metis append_Nil dB_single_step empty_set image_empty) |
|
1084 |
|
1085 lemma bsimp_rewrite: |
|
1086 shows "r \<leadsto>* bsimp r" |
|
1087 proof (induction r rule: bsimp.induct) |
|
1088 case (1 bs1 r1 r2) |
|
1089 then show "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" |
|
1090 apply(simp) |
|
1091 apply(case_tac "bsimp r1 = AZERO") |
|
1092 apply simp |
|
1093 using continuous_rewrite apply blast |
|
1094 apply(case_tac "\<exists>bs. bsimp r1 = AONE bs") |
|
1095 apply(erule exE) |
|
1096 apply simp |
|
1097 apply(subst bsimp_ASEQ2) |
|
1098 apply (meson rrewrites_trans rrewrite_srewrite.intros(3) rrewrites.intros(2) star_seq star_seq2) |
|
1099 apply (smt (verit, best) bsimp_ASEQ0 bsimp_ASEQ1 rrewrites_trans rrewrite_srewrite.intros(2) rs2 star_seq star_seq2) |
|
1100 done |
|
1101 next |
|
1102 case (2 bs1 rs) |
|
1103 then show "AALTs bs1 rs \<leadsto>* bsimp (AALTs bs1 rs)" |
|
1104 by (metis alts_dBrewrites alts_simpalts bsimp.simps(2) bsimp_AALTs_rewrites flts_rewrites rrewrites_trans) |
|
1105 next |
|
1106 case "3_1" |
|
1107 then show "AZERO \<leadsto>* bsimp AZERO" |
|
1108 by simp |
|
1109 next |
|
1110 case ("3_2" v) |
|
1111 then show "AONE v \<leadsto>* bsimp (AONE v)" |
|
1112 by simp |
|
1113 next |
|
1114 case ("3_3" v va) |
|
1115 then show "ACHAR v va \<leadsto>* bsimp (ACHAR v va)" |
|
1116 by simp |
|
1117 next |
|
1118 case ("3_4" v va) |
|
1119 then show "ASTAR v va \<leadsto>* bsimp (ASTAR v va)" |
|
1120 by simp |
|
1121 qed |
|
1122 |
1064 |
1123 lemma bnullable1: |
1065 lemma bnullable1: |
1124 shows "r1 \<leadsto> r2 \<Longrightarrow> (bnullable r1 \<Longrightarrow> bnullable r2)" |
1066 shows "r1 \<leadsto> r2 \<Longrightarrow> (bnullable r1 \<Longrightarrow> bnullable r2)" |
1125 and "rs1 s\<leadsto> rs2 \<Longrightarrow> ((\<exists>x \<in> set rs1. bnullable x) \<Longrightarrow> \<exists>x\<in>set rs2. bnullable x)" |
1067 and "rs1 s\<leadsto> rs2 \<Longrightarrow> ((\<exists>x \<in> set rs1. bnullable x) \<Longrightarrow> \<exists>x\<in>set rs2. bnullable x)" |
1126 apply(induct rule: rrewrite_srewrite.inducts) |
1068 apply(induct rule: rrewrite_srewrite.inducts) |
1238 have a4: "bnullable r2" using a1 a2 by (simp add: rewritesnullable) |
1180 have a4: "bnullable r2" using a1 a2 by (simp add: rewritesnullable) |
1239 then have "bmkeps r2 = bmkeps r3" using rewrite_bmkeps a3 a4 by simp |
1181 then have "bmkeps r2 = bmkeps r3" using rewrite_bmkeps a3 a4 by simp |
1240 then show "bmkeps r1 = bmkeps r3" using IH by simp |
1182 then show "bmkeps r1 = bmkeps r3" using IH by simp |
1241 qed |
1183 qed |
1242 |
1184 |
|
1185 |
|
1186 lemma rewrites_to_bsimp: |
|
1187 shows "r \<leadsto>* bsimp r" |
|
1188 proof (induction r rule: bsimp.induct) |
|
1189 case (1 bs1 r1 r2) |
|
1190 have IH1: "r1 \<leadsto>* bsimp r1" by fact |
|
1191 have IH2: "r2 \<leadsto>* bsimp r2" by fact |
|
1192 { assume as: "bsimp r1 = AZERO \<or> bsimp r2 = AZERO" |
|
1193 with IH1 IH2 have "r1 \<leadsto>* AZERO \<or> r2 \<leadsto>* AZERO" by auto |
|
1194 then have "ASEQ bs1 r1 r2 \<leadsto>* AZERO" |
|
1195 by (metis bs2 continuous_rewrite rrewrites.simps star_seq2) |
|
1196 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" using as by auto |
|
1197 } |
|
1198 moreover |
|
1199 { assume "\<exists>bs. bsimp r1 = AONE bs" |
|
1200 then obtain bs where as: "bsimp r1 = AONE bs" by blast |
|
1201 with IH1 have "r1 \<leadsto>* AONE bs" by simp |
|
1202 then have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) r2" using bs3 star_seq by blast |
|
1203 with IH2 have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) (bsimp r2)" |
|
1204 using rewrites_fuse by (meson rrewrites_trans) |
|
1205 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 (AONE bs) r2)" by simp |
|
1206 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" by (simp add: as) |
|
1207 } |
|
1208 moreover |
|
1209 { assume as1: "bsimp r1 \<noteq> AZERO" "bsimp r2 \<noteq> AZERO" and as2: "(\<nexists>bs. bsimp r1 = AONE bs)" |
|
1210 then have "bsimp_ASEQ bs1 (bsimp r1) (bsimp r2) = ASEQ bs1 (bsimp r1) (bsimp r2)" |
|
1211 by (simp add: bsimp_ASEQ1) |
|
1212 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp_ASEQ bs1 (bsimp r1) (bsimp r2)" using as1 as2 IH1 IH2 |
|
1213 by (metis rrewrites_trans star_seq star_seq2) |
|
1214 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" by simp |
|
1215 } |
|
1216 ultimately show "ASEQ bs1 r1 r2 \<leadsto>* bsimp (ASEQ bs1 r1 r2)" by blast |
|
1217 next |
|
1218 case (2 bs1 rs) |
|
1219 have IH: "\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimp x" by fact |
|
1220 then have "rs s\<leadsto>* (map bsimp rs)" by (simp add: trivialbsimp_srewrites) |
|
1221 also have "... s\<leadsto>* flts (map bsimp rs)" by (simp add: fltsfrewrites) |
|
1222 also have "... s\<leadsto>* distinctBy (flts (map bsimp rs)) erase {}" by (simp add: ss6_stronger) |
|
1223 finally have "AALTs bs1 rs \<leadsto>* AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {})" |
|
1224 using contextrewrites0 by blast |
|
1225 also have "... \<leadsto>* bsimp_AALTs bs1 (distinctBy (flts (map bsimp rs)) erase {})" |
|
1226 by (simp add: bsimp_AALTs_rewrites) |
|
1227 finally show "AALTs bs1 rs \<leadsto>* bsimp (AALTs bs1 rs)" by simp |
|
1228 next |
|
1229 case "3_1" |
|
1230 then show "AZERO \<leadsto>* bsimp AZERO" by simp |
|
1231 next |
|
1232 case ("3_2" v) |
|
1233 then show "AONE v \<leadsto>* bsimp (AONE v)" by simp |
|
1234 next |
|
1235 case ("3_3" v va) |
|
1236 then show "ACHAR v va \<leadsto>* bsimp (ACHAR v va)" by simp |
|
1237 next |
|
1238 case ("3_4" v va) |
|
1239 then show "ASTAR v va \<leadsto>* bsimp (ASTAR v va)" by simp |
|
1240 qed |
|
1241 |
|
1242 |
|
1243 |
1243 lemma to_zero_in_alt: |
1244 lemma to_zero_in_alt: |
1244 shows "AALT bs (ASEQ [] AZERO r) r2 \<leadsto> AALT bs AZERO r2" |
1245 shows "AALT bs (ASEQ [] AZERO r) r2 \<leadsto> AALT bs AZERO r2" |
1245 by (simp add: bs1 bs10 ss3) |
1246 by (simp add: bs1 bs10 ss3) |
1246 |
1247 |
1247 |
1248 |
1248 lemma rewrite_fuse2: |
|
1249 shows "r2 \<leadsto> r3 \<Longrightarrow> True" |
|
1250 and "rs2 s\<leadsto> rs3 \<Longrightarrow> (\<And>bs. map (fuse bs) rs2 s\<leadsto>* map (fuse bs) rs3)" |
|
1251 proof(induct rule: rrewrite_srewrite.inducts) |
|
1252 case ss1 |
|
1253 then show ?case |
|
1254 by simp |
|
1255 next |
|
1256 case (ss2 rs1 rs2 r) |
|
1257 then show ?case |
|
1258 using srewrites7 by force |
|
1259 next |
|
1260 case (ss3 r1 r2 rs) |
|
1261 then show ?case |
|
1262 by (simp add: r_in_rstar rewrite_fuse srewrites7) |
|
1263 next |
|
1264 case (ss4 rs) |
|
1265 then show ?case |
|
1266 by (metis fuse.simps(1) list.simps(9) rrewrite_srewrite.ss4 srewrites.simps) |
|
1267 next |
|
1268 case (ss5 bs1 rs1 rsb) |
|
1269 then show ?case |
|
1270 apply(simp) |
|
1271 by (metis (mono_tags, lifting) comp_def fuse_append map_eq_conv rrewrite_srewrite.ss5 srewrites.simps) |
|
1272 next |
|
1273 case (ss6 a1 a2 rsa rsb rsc) |
|
1274 then show ?case |
|
1275 apply(simp only: map_append) |
|
1276 by (smt (verit, ccfv_threshold) erase_fuse list.simps(8) list.simps(9) rrewrite_srewrite.ss6 srewrites.simps) |
|
1277 qed (auto) |
|
1278 |
|
1279 |
|
1280 lemma rewrites_fuse: |
|
1281 assumes "r1 \<leadsto>* r2" |
|
1282 shows "fuse bs r1 \<leadsto>* fuse bs r2" |
|
1283 using assms |
|
1284 apply(induction r1 r2 arbitrary: bs rule: rrewrites.induct) |
|
1285 apply(auto intro: rewrite_fuse rrewrites_trans) |
|
1286 done |
|
1287 |
1249 |
1288 lemma bder_fuse_list: |
1250 lemma bder_fuse_list: |
1289 shows "map (bder c \<circ> fuse bs1) rs1 = map (fuse bs1 \<circ> bder c) rs1" |
1251 shows "map (bder c \<circ> fuse bs1) rs1 = map (fuse bs1 \<circ> bder c) rs1" |
1290 apply(induction rs1) |
1252 apply(induction rs1) |
1291 apply(simp_all add: bder_fuse) |
1253 apply(simp_all add: bder_fuse) |
1292 done |
1254 done |
1293 |
1255 |
1294 |
1256 |
1295 lemma rewrite_after_der: |
1257 lemma rewrite_preserves_bder: |
1296 shows "r1 \<leadsto> r2 \<Longrightarrow> (bder c r1) \<leadsto>* (bder c r2)" |
1258 shows "r1 \<leadsto> r2 \<Longrightarrow> (bder c r1) \<leadsto>* (bder c r2)" |
1297 and "rs1 s\<leadsto> rs2 \<Longrightarrow> map (bder c) rs1 s\<leadsto>* map (bder c) rs2" |
1259 and "rs1 s\<leadsto> rs2 \<Longrightarrow> map (bder c) rs1 s\<leadsto>* map (bder c) rs2" |
1298 proof(induction rule: rrewrite_srewrite.inducts) |
1260 proof(induction rule: rrewrite_srewrite.inducts) |
1299 case (bs1 bs r2) |
1261 case (bs1 bs r2) |
1300 then show ?case |
1262 then show ?case |
1381 next |
1344 next |
1382 case (snoc x xs) |
1345 case (snoc x xs) |
1383 have IH: "\<And>r. bders r xs \<leadsto>* bders_simp r xs" by fact |
1346 have IH: "\<And>r. bders r xs \<leadsto>* bders_simp r xs" by fact |
1384 have "bders r (xs @ [x]) = bders (bders r xs) [x]" by (simp add: bders_append) |
1347 have "bders r (xs @ [x]) = bders (bders r xs) [x]" by (simp add: bders_append) |
1385 also have "... \<leadsto>* bders (bders_simp r xs) [x]" using IH |
1348 also have "... \<leadsto>* bders (bders_simp r xs) [x]" using IH |
1386 by (simp add: rewrites_after_der) |
1349 by (simp add: rewrites_preserves_bder) |
1387 also have "... \<leadsto>* bders_simp (bders_simp r xs) [x]" using IH |
1350 also have "... \<leadsto>* bders_simp (bders_simp r xs) [x]" using IH |
1388 by (simp add: bsimp_rewrite) |
1351 by (simp add: rewrites_to_bsimp) |
1389 finally show "bders r (xs @ [x]) \<leadsto>* bders_simp r (xs @ [x])" |
1352 finally show "bders r (xs @ [x]) \<leadsto>* bders_simp r (xs @ [x])" |
1390 by (simp add: bders_simp_append) |
1353 by (simp add: bders_simp_append) |
1391 qed |
1354 qed |
1392 |
1355 |
1393 |
1356 lemma main_aux: |
1394 |
|
1395 |
|
1396 |
|
1397 lemma quasi_main: |
|
1398 assumes "bnullable (bders r s)" |
1357 assumes "bnullable (bders r s)" |
1399 shows "bmkeps (bders r s) = bmkeps (bders_simp r s)" |
1358 shows "bmkeps (bders r s) = bmkeps (bders_simp r s)" |
1400 proof - |
1359 proof - |
1401 have "bders r s \<leadsto>* bders_simp r s" by (rule central) |
1360 have "bders r s \<leadsto>* bders_simp r s" by (rule central) |
1402 then |
1361 then |