935 apply(auto simp add: bnullable_fuse) |
935 apply(auto simp add: bnullable_fuse) |
936 apply (meson UnCI bnullable_fuse imageI) |
936 apply (meson UnCI bnullable_fuse imageI) |
937 by (metis bnullable_correctness) |
937 by (metis bnullable_correctness) |
938 |
938 |
939 |
939 |
940 lemma rewritesnullable: |
940 lemma rewrites_bnullable_eq: |
941 assumes "r1 \<leadsto>* r2" |
941 assumes "r1 \<leadsto>* r2" |
942 shows "bnullable r1 = bnullable r2" |
942 shows "bnullable r1 = bnullable r2" |
943 using assms |
943 using assms |
944 apply(induction r1 r2 rule: rrewrites.induct) |
944 apply(induction r1 r2 rule: rrewrites.induct) |
945 apply simp |
945 apply simp |
946 using bnullable0(1) by auto |
946 using bnullable0(1) by auto |
947 |
947 |
948 lemma rewrite_bmkeps_aux: |
948 lemma rewrite_bmkeps_aux: |
949 shows "r1 \<leadsto> r2 \<Longrightarrow> (bnullable r1 \<and> bnullable r2 \<Longrightarrow> bmkeps r1 = bmkeps r2)" |
949 shows "r1 \<leadsto> r2 \<Longrightarrow> bnullable r1 \<Longrightarrow> bmkeps r1 = bmkeps r2" |
950 and "rs1 s\<leadsto> rs2 \<Longrightarrow> (bnullables rs1 \<and> bnullables rs2 \<Longrightarrow> bmkepss rs1 = bmkepss rs2)" |
950 and "rs1 s\<leadsto> rs2 \<Longrightarrow> bnullables rs1 \<Longrightarrow> bmkepss rs1 = bmkepss rs2" |
951 proof (induct rule: rrewrite_srewrite.inducts) |
951 proof (induct rule: rrewrite_srewrite.inducts) |
952 case (bs3 bs1 bs2 r) |
952 case (bs3 bs1 bs2 r) |
953 then show ?case by (simp add: bmkeps_fuse) |
953 have IH2: "bnullable (ASEQ bs1 (AONE bs2) r)" by fact |
|
954 then show "bmkeps (ASEQ bs1 (AONE bs2) r) = bmkeps (fuse (bs1 @ bs2) r)" |
|
955 by (simp add: bmkeps_fuse) |
954 next |
956 next |
955 case (bs7 bs r) |
957 case (bs7 bs r) |
956 then show ?case by (simp add: bmkeps_fuse) |
958 have IH2: "bnullable (AALTs bs [r])" by fact |
|
959 then show "bmkeps (AALTs bs [r]) = bmkeps (fuse bs r)" |
|
960 by (simp add: bmkeps_fuse) |
957 next |
961 next |
958 case (ss3 r1 r2 rs) |
962 case (ss3 r1 r2 rs) |
959 then show ?case |
963 have IH1: "bnullable r1 \<Longrightarrow> bmkeps r1 = bmkeps r2" by fact |
960 by (metis bmkepss.simps(2) bnullable0(1)) |
964 have as: "r1 \<leadsto> r2" by fact |
|
965 from IH1 as show "bmkepss (r1 # rs) = bmkepss (r2 # rs)" |
|
966 by (simp add: bnullable0) |
961 next |
967 next |
962 case (ss5 bs1 rs1 rsb) |
968 case (ss5 bs1 rs1 rsb) |
963 then show ?case |
969 have "bnullables (AALTs bs1 rs1 # rsb)" by fact |
|
970 then show "bmkepss (AALTs bs1 rs1 # rsb) = bmkepss (map (fuse bs1) rs1 @ rsb)" |
964 by (simp add: bmkepss1 bmkepss2 bmkepss_fuse bnullable_fuse) |
971 by (simp add: bmkepss1 bmkepss2 bmkepss_fuse bnullable_fuse) |
965 next |
972 next |
966 case (ss6 a1 a2 rsa rsb rsc) |
973 case (ss6 a1 a2 rsa rsb rsc) |
967 then show ?case |
974 have as1: "erase a1 = erase a2" by fact |
|
975 have as3: "bnullables (rsa @ [a1] @ rsb @ [a2] @ rsc)" by fact |
|
976 show "bmkepss (rsa @ [a1] @ rsb @ [a2] @ rsc) = bmkepss (rsa @ [a1] @ rsb @ rsc)" using as1 as3 |
968 by (smt (verit, best) append_Cons bmkeps.simps(3) bmkepss.simps(2) bmkepss1 bmkepss2 bnullable_correctness) |
977 by (smt (verit, best) append_Cons bmkeps.simps(3) bmkepss.simps(2) bmkepss1 bmkepss2 bnullable_correctness) |
969 qed (auto) |
978 qed (auto) |
970 |
979 |
971 lemma rewrites_bmkeps: |
980 lemma rewrites_bmkeps: |
972 assumes "r1 \<leadsto>* r2" "bnullable r1" |
981 assumes "r1 \<leadsto>* r2" "bnullable r1" |
979 case (rs2 r1 r2 r3) |
988 case (rs2 r1 r2 r3) |
980 then have IH: "bmkeps r1 = bmkeps r2" by simp |
989 then have IH: "bmkeps r1 = bmkeps r2" by simp |
981 have a1: "bnullable r1" by fact |
990 have a1: "bnullable r1" by fact |
982 have a2: "r1 \<leadsto>* r2" by fact |
991 have a2: "r1 \<leadsto>* r2" by fact |
983 have a3: "r2 \<leadsto> r3" by fact |
992 have a3: "r2 \<leadsto> r3" by fact |
984 have a4: "bnullable r2" using a1 a2 by (simp add: rewritesnullable) |
993 have a4: "bnullable r2" using a1 a2 by (simp add: rewrites_bnullable_eq) |
985 then have "bmkeps r2 = bmkeps r3" |
994 then have "bmkeps r2 = bmkeps r3" |
986 using a3 bnullable0(1) rewrite_bmkeps_aux(1) by blast |
995 using a3 bnullable0(1) rewrite_bmkeps_aux(1) by blast |
987 then show "bmkeps r1 = bmkeps r3" using IH by simp |
996 then show "bmkeps r1 = bmkeps r3" using IH by simp |
988 qed |
997 qed |
989 |
998 |
1045 apply(simp_all add: bder_fuse) |
1054 apply(simp_all add: bder_fuse) |
1046 done |
1055 done |
1047 |
1056 |
1048 |
1057 |
1049 lemma rewrite_preserves_bder: |
1058 lemma rewrite_preserves_bder: |
1050 shows "r1 \<leadsto> r2 \<Longrightarrow> (bder c r1) \<leadsto>* (bder c r2)" |
1059 shows "r1 \<leadsto> r2 \<Longrightarrow> bder c r1 \<leadsto>* bder c r2" |
1051 and "rs1 s\<leadsto> rs2 \<Longrightarrow> map (bder c) rs1 s\<leadsto>* map (bder c) rs2" |
1060 and "rs1 s\<leadsto> rs2 \<Longrightarrow> map (bder c) rs1 s\<leadsto>* map (bder c) rs2" |
1052 proof(induction rule: rrewrite_srewrite.inducts) |
1061 proof(induction rule: rrewrite_srewrite.inducts) |
1053 case (bs1 bs r2) |
1062 case (bs1 bs r2) |
1054 then show ?case |
1063 show "bder c (ASEQ bs AZERO r2) \<leadsto>* bder c AZERO" |
1055 by (simp add: continuous_rewrite) |
1064 by (simp add: continuous_rewrite) |
1056 next |
1065 next |
1057 case (bs2 bs r1) |
1066 case (bs2 bs r1) |
1058 then show ?case |
1067 show "bder c (ASEQ bs r1 AZERO) \<leadsto>* bder c AZERO" |
1059 apply(auto) |
1068 apply(auto) |
1060 apply (meson bs6 contextrewrites0 rrewrite_srewrite.bs2 rs2 ss3 ss4 sss1 sss2) |
1069 apply (meson bs6 contextrewrites0 rrewrite_srewrite.bs2 rs2 ss3 ss4 sss1 sss2) |
1061 by (simp add: r_in_rstar rrewrite_srewrite.bs2) |
1070 by (simp add: r_in_rstar rrewrite_srewrite.bs2) |
1062 next |
1071 next |
1063 case (bs3 bs1 bs2 r) |
1072 case (bs3 bs1 bs2 r) |
1064 then show ?case |
1073 show "bder c (ASEQ bs1 (AONE bs2) r) \<leadsto>* bder c (fuse (bs1 @ bs2) r)" |
1065 apply(simp) |
1074 apply(simp) |
1066 |
|
1067 by (metis (no_types, lifting) bder_fuse bs10 bs7 fuse_append rrewrites.simps ss4 to_zero_in_alt) |
1075 by (metis (no_types, lifting) bder_fuse bs10 bs7 fuse_append rrewrites.simps ss4 to_zero_in_alt) |
1068 next |
1076 next |
1069 case (bs4 r1 r2 bs r3) |
1077 case (bs4 r1 r2 bs r3) |
1070 have as: "r1 \<leadsto> r2" by fact |
1078 have as: "r1 \<leadsto> r2" by fact |
1071 have IH: "bder c r1 \<leadsto>* bder c r2" by fact |
1079 have IH: "bder c r1 \<leadsto>* bder c r2" by fact |
1080 apply(auto) |
1088 apply(auto) |
1081 using contextrewrites0 r_in_rstar rewrites_fuse srewrites6 srewrites7 star_seq2 apply presburger |
1089 using contextrewrites0 r_in_rstar rewrites_fuse srewrites6 srewrites7 star_seq2 apply presburger |
1082 using star_seq2 by blast |
1090 using star_seq2 by blast |
1083 next |
1091 next |
1084 case (bs6 bs) |
1092 case (bs6 bs) |
1085 then show ?case |
1093 show "bder c (AALTs bs []) \<leadsto>* bder c AZERO" |
1086 using rrewrite_srewrite.bs6 by force |
1094 using rrewrite_srewrite.bs6 by force |
1087 next |
1095 next |
1088 case (bs7 bs r) |
1096 case (bs7 bs r) |
1089 then show ?case |
1097 show "bder c (AALTs bs [r]) \<leadsto>* bder c (fuse bs r)" |
1090 by (simp add: bder_fuse r_in_rstar rrewrite_srewrite.bs7) |
1098 by (simp add: bder_fuse r_in_rstar rrewrite_srewrite.bs7) |
1091 next |
1099 next |
1092 case (bs10 rs1 rs2 bs) |
1100 case (bs10 rs1 rs2 bs) |
1093 then show ?case |
1101 have IH1: "map (bder c) rs1 s\<leadsto>* map (bder c) rs2" by fact |
|
1102 then show "bder c (AALTs bs rs1) \<leadsto>* bder c (AALTs bs rs2)" |
1094 using contextrewrites0 by force |
1103 using contextrewrites0 by force |
1095 next |
1104 next |
1096 case ss1 |
1105 case ss1 |
1097 then show ?case by simp |
1106 show "map (bder c) [] s\<leadsto>* map (bder c) []" by simp |
1098 next |
1107 next |
1099 case (ss2 rs1 rs2 r) |
1108 case (ss2 rs1 rs2 r) |
1100 then show ?case |
1109 have IH1: "map (bder c) rs1 s\<leadsto>* map (bder c) rs2" by fact |
|
1110 then show "map (bder c) (r # rs1) s\<leadsto>* map (bder c) (r # rs2)" |
1101 by (simp add: srewrites7) |
1111 by (simp add: srewrites7) |
1102 next |
1112 next |
1103 case (ss3 r1 r2 rs) |
1113 case (ss3 r1 r2 rs) |
1104 then show ?case |
1114 have IH: "bder c r1 \<leadsto>* bder c r2" by fact |
|
1115 then show "map (bder c) (r1 # rs) s\<leadsto>* map (bder c) (r2 # rs)" |
1105 by (simp add: srewrites7) |
1116 by (simp add: srewrites7) |
1106 next |
1117 next |
1107 case (ss4 rs) |
1118 case (ss4 rs) |
1108 then show ?case |
1119 show "map (bder c) (AZERO # rs) s\<leadsto>* map (bder c) rs" |
1109 using rrewrite_srewrite.ss4 by fastforce |
1120 using rrewrite_srewrite.ss4 by fastforce |
1110 next |
1121 next |
1111 case (ss5 bs1 rs1 rsb) |
1122 case (ss5 bs1 rs1 rsb) |
1112 then show ?case |
1123 show "map (bder c) (AALTs bs1 rs1 # rsb) s\<leadsto>* map (bder c) (map (fuse bs1) rs1 @ rsb)" |
1113 apply(simp) |
1124 apply(simp) |
1114 using bder_fuse_list map_map rrewrite_srewrite.ss5 srewrites.simps by blast |
1125 using bder_fuse_list map_map rrewrite_srewrite.ss5 srewrites.simps by blast |
1115 next |
1126 next |
1116 case (ss6 a1 a2 bs rsa rsb) |
1127 case (ss6 a1 a2 bs rsa rsb) |
1117 then show ?case |
1128 have as: "erase a1 = erase a2" by fact |
|
1129 show "map (bder c) (bs @ [a1] @ rsa @ [a2] @ rsb) s\<leadsto>* map (bder c) (bs @ [a1] @ rsa @ rsb)" |
1118 apply(simp only: map_append) |
1130 apply(simp only: map_append) |
1119 by (smt (verit, best) erase_bder list.simps(8) list.simps(9) local.ss6 rrewrite_srewrite.ss6 srewrites.simps) |
1131 by (smt (verit, best) erase_bder list.simps(8) list.simps(9) as rrewrite_srewrite.ss6 srewrites.simps) |
1120 qed |
1132 qed |
1121 |
1133 |
1122 lemma rewrites_preserves_bder: |
1134 lemma rewrites_preserves_bder: |
1123 assumes "r1 \<leadsto>* r2" |
1135 assumes "r1 \<leadsto>* r2" |
1124 shows "bder c r1 \<leadsto>* bder c r2" |
1136 shows "bder c r1 \<leadsto>* bder c r2" |