881 | "r \<leadsto> r' \<Longrightarrow> (AALTs bs (rs1 @ [r] @ rs2)) \<leadsto> (AALTs bs (rs1 @ [r'] @ rs2))" |
881 | "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)*) |
882 (*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)" |
883 | "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)" |
884 | "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*) |
885 (*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" |
886 (***| "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 |
887 (*opposite direction also allowed, which means bits are free to be moved around |
888 as long as they are on the right path*) |
888 as long as they are on the right path*) |
889 | "AALTs (bs@bs1) rs \<leadsto> AALTs bs (map (fuse bs1) rs)" |
889 | "AALTs (bs@bs1) rs \<leadsto> AALTs bs (map (fuse bs1) rs)" |
890 | "AALTs bs [] \<leadsto> AZERO" |
890 | "AALTs bs [] \<leadsto> AZERO" |
891 | "AALTs bs [r] \<leadsto> fuse bs r" |
891 | "AALTs bs [r] \<leadsto> fuse bs r" |
1000 |
1000 |
1001 lemma bsimp_AALTsrewrites: "AALTs bs1 rs \<leadsto>* bsimp_AALTs bs1 rs" |
1001 lemma bsimp_AALTsrewrites: "AALTs bs1 rs \<leadsto>* bsimp_AALTs bs1 rs" |
1002 apply(induction rs) |
1002 apply(induction rs) |
1003 apply simp |
1003 apply simp |
1004 apply(rule r_in_rstar) |
1004 apply(rule r_in_rstar) |
1005 apply(simp add: rrewrite.intros(11)) |
1005 apply (simp add: rrewrite.intros(10)) |
1006 apply(case_tac "rs = Nil") |
1006 apply(case_tac "rs = Nil") |
1007 apply(simp) |
1007 apply(simp) |
1008 using rrewrite.intros(12) apply auto[1] |
1008 using rrewrite.intros(12) apply auto[1] |
|
1009 using r_in_rstar rrewrite.intros(11) apply presburger |
1009 apply(subgoal_tac "length (a#rs) > 1") |
1010 apply(subgoal_tac "length (a#rs) > 1") |
1010 apply(simp add: bsimp_AALTs_qq) |
1011 apply(simp add: bsimp_AALTs_qq) |
1011 apply(simp) |
1012 apply(simp) |
1012 done |
1013 done |
1013 |
1014 |
1141 (set rs1 \<union> set rs2)))) \<leadsto> AALTs bs (rs1@ a # rs2 @ distinctBy rs erase |
1142 (set rs1 \<union> set rs2)))) \<leadsto> AALTs bs (rs1@ a # rs2 @ distinctBy rs erase |
1142 (insert (erase a) |
1143 (insert (erase a) |
1143 (erase ` |
1144 (erase ` |
1144 (set rs1 \<union> set rs2)))) ") |
1145 (set rs1 \<union> set rs2)))) ") |
1145 prefer 2 |
1146 prefer 2 |
1146 using rrewrite.intros(13) apply force |
1147 using rrewrite.intros(12) apply force |
1147 using r_in_rstar apply force |
1148 using r_in_rstar apply force |
1148 apply(subgoal_tac "erase ` set (rsa @ [a]) = insert (erase a) (erase ` set rsa)") |
1149 apply(subgoal_tac "erase ` set (rsa @ [a]) = insert (erase a) (erase ` set rsa)") |
1149 prefer 2 |
1150 prefer 2 |
1150 |
1151 |
1151 apply auto[1] |
1152 apply auto[1] |
1153 |
1154 |
1154 apply simp |
1155 apply simp |
1155 apply(subgoal_tac "AALTs bs (rsa @ a # distinctBy rs erase (insert (erase a) (erase ` set rsa))) \<leadsto> |
1156 apply(subgoal_tac "AALTs bs (rsa @ a # distinctBy rs erase (insert (erase a) (erase ` set rsa))) \<leadsto> |
1156 AALTs bs (rsa @ distinctBy rs erase (insert (erase a) (erase ` set rsa)))") |
1157 AALTs bs (rsa @ distinctBy rs erase (insert (erase a) (erase ` set rsa)))") |
1157 apply force |
1158 apply force |
1158 apply (smt (verit, ccfv_threshold) append_Cons append_assoc append_self_conv2 r_in_rstar rrewrite.intros(13) same_append_eq somewhereMapInside) |
1159 apply (smt (verit, ccfv_threshold) append_Cons append_assoc append_self_conv2 r_in_rstar rrewrite.intros(12) same_append_eq somewhereMapInside) |
1159 by force |
1160 by force |
1160 |
1161 |
1161 |
1162 |
1162 |
1163 |
1163 lemma alts_dBrewrites: "AALTs bs rs \<leadsto>* AALTs bs (distinctBy rs erase {})" |
1164 lemma alts_dBrewrites: "AALTs bs rs \<leadsto>* AALTs bs (distinctBy rs erase {})" |
1321 |
1322 |
1322 thm qq1 |
1323 thm qq1 |
1323 apply(subgoal_tac "bmkeps (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs rsb) ") |
1324 apply(subgoal_tac "bmkeps (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs rsb) ") |
1324 prefer 2 |
1325 prefer 2 |
1325 |
1326 |
1326 apply (metis append_Cons append_Nil bnullable.simps(1) bnullable_segment rewrite_nullable rrewrite.intros(11) third_segment_bmkeps) |
1327 apply (metis append_Cons append_Nil bnullable.simps(1) bnullable_segment rewrite_nullable rrewrite.intros(10) third_segment_bmkeps) |
1327 |
1328 by (metis bnullable.simps(4) rewrite_non_nullable_strong rrewrite.intros(9) third_segment_bmkeps) |
1328 by (metis bnullable.simps(4) rewrite_non_nullable rrewrite.intros(10) third_segment_bmkeps) |
1329 |
1329 |
1330 |
1330 |
1331 |
1331 |
1332 lemma rewrite_bmkeps: "\<lbrakk> r1 \<leadsto> r2; bnullable r1\<rbrakk> \<Longrightarrow> bmkeps r1 = bmkeps r2" |
1332 lemma rewrite_bmkeps: "\<lbrakk> r1 \<leadsto> r2; (bnullable r1)\<rbrakk> \<Longrightarrow> bmkeps r1 = bmkeps r2" |
|
1333 |
1333 |
1334 apply(frule rewrite_nullable) |
1334 apply(frule rewrite_nullable) |
1335 apply simp |
1335 apply simp |
1336 apply(induction r1 r2 rule: rrewrite.induct) |
1336 apply(induction r1 r2 rule: rrewrite.induct) |
1337 apply simp |
1337 apply simp |
1352 |
1352 |
1353 apply blast |
1353 apply blast |
1354 apply (simp add: flts_append qs3) |
1354 apply (simp add: flts_append qs3) |
1355 |
1355 |
1356 apply (meson rewrite_bmkepsalt) |
1356 apply (meson rewrite_bmkepsalt) |
1357 |
1357 using q3a apply force |
1358 using bnullable.simps(4) q3a apply blast |
|
1359 |
1358 |
1360 apply (simp add: q3a) |
1359 apply (simp add: q3a) |
1361 |
|
1362 using bnullable.simps(1) apply blast |
|
1363 |
|
1364 apply (simp add: b2) |
1360 apply (simp add: b2) |
1365 |
1361 apply(simp del: append.simps) |
1366 by (smt (z3) Un_iff bnullable_correctness erase.simps(5) qq1 qq2 bnullable.simps(4) set_append) |
1362 apply(case_tac "bnullable a1") |
|
1363 apply (metis append.assoc in_set_conv_decomp qq1) |
|
1364 apply(case_tac "\<exists>r \<in> set rsa. bnullable r") |
|
1365 using qq1 apply presburger |
|
1366 apply(case_tac "\<exists>r \<in> set rsb. bnullable r") |
|
1367 apply (metis UnCI append.assoc qq1 set_append) |
|
1368 apply(case_tac "bnullable a2") |
|
1369 apply (metis bnullable_correctness) |
|
1370 apply(subst qq2) |
|
1371 apply blast |
|
1372 apply(auto)[1] |
|
1373 apply(subst qq2) |
|
1374 apply (metis empty_iff list.set(1) set_ConsD) |
|
1375 apply(auto)[1] |
|
1376 apply(subst qq2) |
|
1377 apply(auto)[2] |
|
1378 apply(subst qq2) |
|
1379 apply(auto)[2] |
|
1380 apply(subst qq2) |
|
1381 apply(auto)[2] |
|
1382 apply(subst qq2) |
|
1383 apply(auto)[2] |
|
1384 apply(subst qq2) |
|
1385 apply(auto)[2] |
|
1386 apply(simp) |
|
1387 done |
1367 |
1388 |
1368 lemma rewrites_bmkeps: |
1389 lemma rewrites_bmkeps: |
1369 assumes "r1 \<leadsto>* r2" "bnullable r1" |
1390 assumes "r1 \<leadsto>* r2" "bnullable r1" |
1370 shows "bmkeps r1 = bmkeps r2" |
1391 shows "bmkeps r1 = bmkeps r2" |
1371 using assms |
1392 using assms |
1420 |
1441 |
1421 using rrewrite.intros(8) apply auto[1] |
1442 using rrewrite.intros(8) apply auto[1] |
1422 |
1443 |
1423 apply (metis append_assoc r_in_rstar rrewrite.intros(9)) |
1444 apply (metis append_assoc r_in_rstar rrewrite.intros(9)) |
1424 |
1445 |
1425 apply (metis append_assoc r_in_rstar rrewrite.intros(10)) |
1446 apply (metis r_in_rstar rrewrite.intros(10)) |
1426 |
1447 apply (metis fuse_append r_in_rstar rrewrite.intros(11)) |
1427 apply (simp add: r_in_rstar rrewrite.intros(11)) |
1448 using rrewrite.intros(12) by auto |
1428 |
|
1429 apply (metis fuse_append r_in_rstar rrewrite.intros(12)) |
|
1430 |
|
1431 using rrewrite.intros(13) by auto |
|
1432 |
|
1433 |
1449 |
1434 |
1450 |
1435 lemma rewrites_fuse: |
1451 lemma rewrites_fuse: |
1436 assumes "r2 \<leadsto>* r2'" |
1452 assumes "r2 \<leadsto>* r2'" |
1437 shows "fuse bs1 r2 \<leadsto>* fuse bs1 r2'" |
1453 shows "fuse bs1 r2 \<leadsto>* fuse bs1 r2'" |
1460 shows " erase a1 = erase a2 \<Longrightarrow> |
1476 shows " erase a1 = erase a2 \<Longrightarrow> |
1461 bder c (AALTs bs (rsa @ [a1] @ rsb @ [a2] @ rsc)) \<leadsto>* |
1477 bder c (AALTs bs (rsa @ [a1] @ rsb @ [a2] @ rsc)) \<leadsto>* |
1462 bder c (AALTs bs (rsa @ [a1] @ rsb @ rsc))" |
1478 bder c (AALTs bs (rsa @ [a1] @ rsb @ rsc))" |
1463 apply(simp) |
1479 apply(simp) |
1464 |
1480 |
1465 using rrewrite.intros(13) by auto |
1481 using rrewrite.intros(12) by auto |
1466 |
1482 |
1467 lemma rewrite_after_der: "r1 \<leadsto> r2 \<Longrightarrow> (bder c r1) \<leadsto>* (bder c r2)" |
1483 lemma rewrite_after_der: "r1 \<leadsto> r2 \<Longrightarrow> (bder c r1) \<leadsto>* (bder c r2)" |
1468 apply(induction r1 r2 arbitrary: c rule: rrewrite.induct) |
1484 apply(induction r1 r2 arbitrary: c rule: rrewrite.induct) |
1469 |
1485 |
1470 apply (simp add: r_in_rstar rrewrite.intros(1)) |
1486 apply (simp add: r_in_rstar rrewrite.intros(1)) |
1471 apply simp |
1487 apply simp |
1472 |
1488 |
1473 apply (meson contextrewrites1 r_in_rstar rrewrite.intros(11) rrewrite.intros(2) rrewrite0away rs2) |
1489 apply (meson contextrewrites1 r_in_rstar rrewrite.intros(10) rrewrite.intros(2) rrewrite0away rs2) |
1474 apply(simp) |
1490 apply(simp) |
1475 apply(rule many_steps_later) |
1491 apply(rule many_steps_later) |
1476 apply(rule to_zero_in_alt) |
1492 apply(rule to_zero_in_alt) |
1477 apply(rule many_steps_later) |
1493 apply(rule many_steps_later) |
1478 apply(rule alt_remove0_front) |
1494 apply(rule alt_remove0_front) |
1479 apply(rule many_steps_later) |
1495 apply(rule many_steps_later) |
1480 apply(rule rrewrite.intros(12)) |
1496 apply(rule rrewrite.intros(11)) |
1481 using bder_fuse fuse_append rs1 apply presburger |
1497 using bder_fuse fuse_append rs1 apply presburger |
1482 apply(case_tac "bnullable r1") |
1498 apply(case_tac "bnullable r1") |
1483 prefer 2 |
1499 prefer 2 |
1484 apply(subgoal_tac "\<not>bnullable r2") |
1500 apply(subgoal_tac "\<not>bnullable r2") |
1485 prefer 2 |
1501 prefer 2 |
1511 using rrewrite.intros(7) apply force |
1527 using rrewrite.intros(7) apply force |
1512 |
1528 |
1513 using rewrite_der_altmiddle apply auto[1] |
1529 using rewrite_der_altmiddle apply auto[1] |
1514 |
1530 |
1515 apply (metis bder.simps(4) bder_fuse_list map_map r_in_rstar rrewrite.intros(9)) |
1531 apply (metis bder.simps(4) bder_fuse_list map_map r_in_rstar rrewrite.intros(9)) |
1516 |
1532 apply (simp add: r_in_rstar rrewrite.intros(10)) |
1517 apply (metis List.map.compositionality bder.simps(4) bder_fuse_list r_in_rstar rrewrite.intros(10)) |
1533 |
1518 |
1534 apply (simp add: r_in_rstar rrewrite.intros(10)) |
1519 apply (simp add: r_in_rstar rrewrite.intros(11)) |
1535 using bder_fuse r_in_rstar rrewrite.intros(11) apply presburger |
1520 |
|
1521 apply (metis bder.simps(4) bder_bsimp_AALTs bsimp_AALTs.simps(2) bsimp_AALTsrewrites) |
|
1522 |
1536 |
1523 |
1537 |
1524 using lock_step_der_removal by auto |
1538 using lock_step_der_removal by auto |
1525 |
1539 |
1526 |
1540 |