857 shows "bder c (fuse bs a) = fuse bs (bder c a)" |
857 shows "bder c (fuse bs a) = fuse bs (bder c a)" |
858 apply(induct a arbitrary: bs c) |
858 apply(induct a arbitrary: bs c) |
859 apply(simp_all) |
859 apply(simp_all) |
860 done |
860 done |
861 |
861 |
862 |
|
863 lemma bder_bsimp_AALTs: |
|
864 shows "bder c (bsimp_AALTs bs rs) = bsimp_AALTs bs (map (bder c) rs)" |
|
865 apply(induct bs rs rule: bsimp_AALTs.induct) |
|
866 apply(simp) |
|
867 apply(simp) |
|
868 apply (simp add: bder_fuse) |
|
869 apply(simp) |
|
870 done |
|
871 |
|
872 |
|
873 |
|
874 inductive rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99) |
862 inductive rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99) |
875 where |
863 where |
876 "ASEQ bs AZERO r2 \<leadsto> AZERO" |
864 "ASEQ bs AZERO r2 \<leadsto> AZERO" |
877 | "ASEQ bs r1 AZERO \<leadsto> AZERO" |
865 | "ASEQ bs r1 AZERO \<leadsto> AZERO" |
878 | "ASEQ bs (AONE bs1) r \<leadsto> fuse (bs@bs1) r" |
866 | "ASEQ bs (AONE bs1) r \<leadsto> fuse (bs@bs1) r" |
879 | "r1 \<leadsto> r2 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r2 r3" |
867 | "r1 \<leadsto> r2 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r2 r3" |
880 | "r3 \<leadsto> r4 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r1 r4" |
868 | "r3 \<leadsto> r4 \<Longrightarrow> ASEQ bs r1 r3 \<leadsto> ASEQ bs r1 r4" |
881 | "r \<leadsto> r' \<Longrightarrow> (AALTs bs (rs1 @ [r] @ rs2)) \<leadsto> (AALTs bs (rs1 @ [r'] @ rs2))" |
869 | "r \<leadsto> r' \<Longrightarrow> (AALTs bs (rs1 @ [r] @ rs2)) \<leadsto> (AALTs bs (rs1 @ [r'] @ rs2))" |
882 (*context rule for eliminating 0, alts--corresponds to the recursive call flts r::rs = r::(flts rs)*) |
870 (*context rule for eliminating 0, alts--corresponds to the recursive call flts r::rs = r::(flts rs)*) |
883 | "AALTs bs (rsa@AZERO # rsb) \<leadsto> AALTs bs (rsa@rsb)" |
871 | "AALTs bs (rsa@ [AZERO] @ rsb) \<leadsto> AALTs bs (rsa @ rsb)" |
884 | "AALTs bs (rsa@(AALTs bs1 rs1)# rsb) \<leadsto> AALTs bs (rsa@(map (fuse bs1) rs1)@rsb)" |
872 | "AALTs bs (rsa@ [AALTs bs1 rs1] @ rsb) \<leadsto> AALTs bs (rsa@(map (fuse bs1) rs1)@rsb)" |
885 (*the below rule for extracting common prefixes between a list of rexp's bitcodes*) |
873 (*the below rule for extracting common prefixes between a list of rexp's bitcodes*) |
886 (***| "AALTs bs (map (fuse bs1) rs) \<leadsto> AALTs (bs@bs1) rs"******) |
874 (***| "AALTs bs (map (fuse bs1) rs) \<leadsto> AALTs (bs@bs1) rs"******) |
887 (*opposite direction also allowed, which means bits are free to be moved around |
875 (*opposite direction also allowed, which means bits are free to be moved around |
888 as long as they are on the right path*) |
876 as long as they are on the right path*) |
889 | "AALTs (bs@bs1) rs \<leadsto> AALTs bs (map (fuse bs1) rs)" |
877 | "AALTs (bs@bs1) rs \<leadsto> AALTs bs (map (fuse bs1) rs)" |
1051 |
1039 |
1052 by (meson fs4 nonalt.elims(3) nonazero.elims(3)) |
1040 by (meson fs4 nonalt.elims(3) nonazero.elims(3)) |
1053 |
1041 |
1054 |
1042 |
1055 lemma rrewrite0away: "AALTs bs (AZERO # rsb) \<leadsto> AALTs bs rsb" |
1043 lemma rrewrite0away: "AALTs bs (AZERO # rsb) \<leadsto> AALTs bs rsb" |
1056 by (metis append_Nil rrewrite.intros(7)) |
1044 by (metis append_Cons append_Nil rrewrite.intros(7)) |
1057 |
1045 |
1058 |
1046 |
1059 lemma frewritesaalts:"rs f\<leadsto>* rs' \<Longrightarrow> (AALTs bs (rs1@rs)) \<leadsto>* (AALTs bs (rs1@rs'))" |
1047 lemma frewritesaalts:"rs f\<leadsto>* rs' \<Longrightarrow> (AALTs bs (rs1@rs)) \<leadsto>* (AALTs bs (rs1@rs'))" |
1060 apply(induct rs rs' arbitrary: bs rs1 rule:frewrites.induct) |
1048 apply(induct rs rs' arbitrary: bs rs1 rule:frewrites.induct) |
1061 apply(rule rs1) |
1049 apply(rule rs1) |
1062 apply(drule_tac x = "bs" in meta_spec) |
1050 apply(drule_tac x = "bs" in meta_spec) |
1063 apply(drule_tac x = "rs1 @ [AZERO]" in meta_spec) |
1051 apply(drule_tac x = "rs1 @ [AZERO]" in meta_spec) |
1064 apply(rule real_trans) |
1052 apply(rule real_trans) |
1065 apply simp |
1053 apply simp |
1066 using r_in_rstar rrewrite.intros(7) apply presburger |
1054 using rrewrite.intros(7) apply auto[1] |
1067 apply(drule_tac x = "bsa" in meta_spec) |
1055 apply(drule_tac x = "bsa" in meta_spec) |
1068 apply(drule_tac x = "rs1a @ [AALTs bs rs1]" in meta_spec) |
1056 apply(drule_tac x = "rs1a @ [AALTs bs rs1]" in meta_spec) |
1069 apply(rule real_trans) |
1057 apply(rule real_trans) |
1070 apply simp |
1058 apply simp |
1071 using r_in_rstar rrewrite.intros(8) apply presburger |
1059 using r_in_rstar rrewrite.intros(8) apply auto[1] |
1072 apply(drule_tac x = "bs" in meta_spec) |
1060 apply(drule_tac x = "bs" in meta_spec) |
1073 apply(drule_tac x = "rs1@[r]" in meta_spec) |
1061 apply(drule_tac x = "rs1@[r]" in meta_spec) |
1074 apply(rule real_trans) |
1062 apply(rule real_trans) |
1075 apply simp |
1063 apply simp |
1076 apply auto |
1064 apply auto |
1315 |
1301 |
1316 |
1302 |
1317 using r2 apply blast |
1303 using r2 apply blast |
1318 |
1304 |
1319 apply (metis list.set_intros(1)) |
1305 apply (metis list.set_intros(1)) |
1320 apply (smt (verit, ccfv_threshold) append_eq_append_conv2 list.set_intros(1) qq2 bnullable.simps(4) rewrite_nullable rrewrite.intros(8) self_append_conv2 spillbmkepslistr) |
1306 apply (metis append_Nil bnullable.simps(1) rewrite_non_nullable_strong rrewrite.intros(10) spillbmkepslistr third_segment_bmkeps) |
1321 |
|
1322 |
|
1323 thm qq1 |
|
1324 apply(subgoal_tac "bmkeps (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs rsb) ") |
1307 apply(subgoal_tac "bmkeps (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs rsb) ") |
1325 prefer 2 |
1308 prefer 2 |
1326 |
1309 |
1327 apply (metis append_Cons append_Nil bnullable.simps(1) bnullable_segment rewrite_nullable rrewrite.intros(10) third_segment_bmkeps) |
1310 apply (metis append_Cons append_Nil bnullable.simps(1) bnullable_segment rewrite_nullable rrewrite.intros(10) third_segment_bmkeps) |
1328 by (metis bnullable.simps(4) rewrite_non_nullable_strong rrewrite.intros(9) third_segment_bmkeps) |
1311 by (metis bnullable.simps(4) rewrite_non_nullable_strong rrewrite.intros(9) third_segment_bmkeps) |
1350 |
1333 |
1351 using rewrite_non_nullable apply blast |
1334 using rewrite_non_nullable apply blast |
1352 |
1335 |
1353 apply blast |
1336 apply blast |
1354 apply (simp add: flts_append qs3) |
1337 apply (simp add: flts_append qs3) |
1355 |
1338 apply (simp add: rewrite_bmkepsalt) |
1356 apply (meson rewrite_bmkepsalt) |
|
1357 using q3a apply force |
1339 using q3a apply force |
1358 |
1340 |
1359 apply (simp add: q3a) |
1341 apply (simp add: q3a) |
1360 apply (simp add: b2) |
1342 apply (simp add: b2) |
1361 apply(simp del: append.simps) |
1343 apply(simp del: append.simps) |
1435 |
1417 |
1436 using r_in_rstar star_seq2 apply blast |
1418 using r_in_rstar star_seq2 apply blast |
1437 |
1419 |
1438 using contextrewrites2 r_in_rstar apply auto[1] |
1420 using contextrewrites2 r_in_rstar apply auto[1] |
1439 |
1421 |
1440 apply (simp add: r_in_rstar rrewrite.intros(7)) |
|
1441 |
|
1442 using rrewrite.intros(8) apply auto[1] |
1422 using rrewrite.intros(8) apply auto[1] |
1443 |
1423 using rrewrite.intros(7) apply auto[1] |
1444 apply (metis append_assoc r_in_rstar rrewrite.intros(9)) |
1424 using rrewrite.intros(8) apply force |
1445 |
1425 apply (metis append_assoc r_in_rstar rrewrite.intros(9)) |
1446 apply (metis r_in_rstar rrewrite.intros(10)) |
1426 apply (simp add: r_in_rstar rrewrite.intros(10)) |
1447 apply (metis fuse_append r_in_rstar rrewrite.intros(11)) |
1427 apply (metis fuse_append r_in_rstar rrewrite.intros(11)) |
1448 using rrewrite.intros(12) by auto |
1428 using rrewrite.intros(12) by auto |
1449 |
1429 |
1450 |
1430 |
1451 lemma rewrites_fuse: |
1431 lemma rewrites_fuse: |
1463 done |
1443 done |
1464 |
1444 |
1465 |
1445 |
1466 lemma rewrite_der_altmiddle: "bder c (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) \<leadsto>* bder c (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))" |
1446 lemma rewrite_der_altmiddle: "bder c (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) \<leadsto>* bder c (AALTs bs (rsa @ map (fuse bs1) rs1 @ rsb))" |
1467 apply simp |
1447 apply simp |
1468 apply(simp add: bder_fuse_list) |
1448 apply(simp add: bder_fuse_list del: append.simps) |
1469 apply(rule many_steps_later) |
1449 by (metis append.assoc map_map r_in_rstar rrewrite.intros(8) threelistsappend) |
1470 apply(subst rrewrite.intros(8)) |
|
1471 apply simp |
|
1472 |
|
1473 by fastforce |
|
1474 |
1450 |
1475 lemma lock_step_der_removal: |
1451 lemma lock_step_der_removal: |
1476 shows " erase a1 = erase a2 \<Longrightarrow> |
1452 shows " erase a1 = erase a2 \<Longrightarrow> |
1477 bder c (AALTs bs (rsa @ [a1] @ rsb @ [a2] @ rsc)) \<leadsto>* |
1453 bder c (AALTs bs (rsa @ [a1] @ rsb @ [a2] @ rsc)) \<leadsto>* |
1478 bder c (AALTs bs (rsa @ [a1] @ rsb @ rsc))" |
1454 bder c (AALTs bs (rsa @ [a1] @ rsb @ rsc))" |