764 "nonnested (AALTs bs2 []) = True" |
764 "nonnested (AALTs bs2 []) = True" |
765 | "nonnested (AALTs bs2 ((AALTs bs1 rs1) # rs2)) = False" |
765 | "nonnested (AALTs bs2 ((AALTs bs1 rs1) # rs2)) = False" |
766 | "nonnested (AALTs bs2 (r # rs2)) = nonnested (AALTs bs2 rs2)" |
766 | "nonnested (AALTs bs2 (r # rs2)) = nonnested (AALTs bs2 rs2)" |
767 | "nonnested r = True" |
767 | "nonnested r = True" |
768 |
768 |
769 |
769 lemma flts_append: |
770 lemma k0: |
770 shows "flts (xs1 @ xs2) = flts xs1 @ flts xs2" |
771 shows "flts (r # rs1) = flts [r] @ flts rs1" |
771 by (induct xs1 arbitrary: xs2 rule: flts.induct)(auto) |
772 apply(induct r arbitrary: rs1) |
|
773 apply(auto) |
|
774 done |
|
775 |
|
776 lemma k00: |
|
777 shows "flts (rs1 @ rs2) = flts rs1 @ flts rs2" |
|
778 apply(induct rs1 arbitrary: rs2) |
|
779 apply(auto) |
|
780 by (metis append.assoc k0) |
|
781 |
772 |
782 lemma k0a: |
773 lemma k0a: |
783 shows "flts [AALTs bs rs] = map (fuse bs) rs" |
774 shows "flts [AALTs bs rs] = map (fuse bs) rs" |
784 apply(simp) |
775 apply(simp) |
785 done |
776 done |
786 |
|
787 |
|
788 |
|
789 |
|
790 |
|
791 |
|
792 |
777 |
793 |
778 |
794 lemma bsimp_AALTs_qq: |
779 lemma bsimp_AALTs_qq: |
795 assumes "1 < length rs" |
780 assumes "1 < length rs" |
796 shows "bsimp_AALTs bs rs = AALTs bs rs" |
781 shows "bsimp_AALTs bs rs = AALTs bs rs" |
938 apply(induct a arbitrary: bs c) |
913 apply(induct a arbitrary: bs c) |
939 apply(simp_all) |
914 apply(simp_all) |
940 done |
915 done |
941 |
916 |
942 |
917 |
943 fun flts2 :: "char \<Rightarrow> arexp list \<Rightarrow> arexp list" |
|
944 where |
|
945 "flts2 _ [] = []" |
|
946 | "flts2 c (AZERO # rs) = flts2 c rs" |
|
947 | "flts2 c (AONE _ # rs) = flts2 c rs" |
|
948 | "flts2 c (ACHAR bs d # rs) = (if c = d then (ACHAR bs d # flts2 c rs) else flts2 c rs)" |
|
949 | "flts2 c ((AALTs bs rs1) # rs) = (map (fuse bs) rs1) @ flts2 c rs" |
|
950 | "flts2 c (ASEQ bs r1 r2 # rs) = (if (bnullable(r1) \<and> r2 = AZERO) then |
|
951 flts2 c rs |
|
952 else ASEQ bs r1 r2 # flts2 c rs)" |
|
953 | "flts2 c (r1 # rs) = r1 # flts2 c rs" |
|
954 |
|
955 |
|
956 |
|
957 |
|
958 |
|
959 |
|
960 |
|
961 |
|
962 |
|
963 |
|
964 |
|
965 |
|
966 |
|
967 lemma WQ1: |
|
968 assumes "s \<in> L (der c r)" |
|
969 shows "s \<in> der c r \<rightarrow> mkeps (ders s (der c r))" |
|
970 using assms |
|
971 oops |
|
972 |
|
973 |
|
974 |
|
975 lemma bder_bsimp_AALTs: |
918 lemma bder_bsimp_AALTs: |
976 shows "bder c (bsimp_AALTs bs rs) = bsimp_AALTs bs (map (bder c) rs)" |
919 shows "bder c (bsimp_AALTs bs rs) = bsimp_AALTs bs (map (bder c) rs)" |
977 apply(induct bs rs rule: bsimp_AALTs.induct) |
920 apply(induct bs rs rule: bsimp_AALTs.induct) |
978 apply(simp) |
921 apply(simp) |
979 apply(simp) |
922 apply(simp) |
980 apply (simp add: bder_fuse) |
923 apply (simp add: bder_fuse) |
981 apply(simp) |
924 apply(simp) |
982 done |
925 done |
983 |
|
984 |
|
985 |
|
986 lemma |
|
987 assumes "asize (bsimp a) = asize a" "a = AALTs bs [AALTs bs2 [], AZERO, AONE bs3]" |
|
988 shows "bsimp a = a" |
|
989 using assms |
|
990 apply(simp) |
|
991 oops |
|
992 |
|
993 |
|
994 |
|
995 |
|
996 |
|
997 |
926 |
998 |
927 |
999 |
928 |
1000 inductive rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99) |
929 inductive rrewrite:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99) |
1001 where |
930 where |
1034 |
963 |
1035 |
964 |
1036 lemma r_in_rstar : "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2" |
965 lemma r_in_rstar : "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2" |
1037 using rrewrites.intros(1) rrewrites.intros(2) by blast |
966 using rrewrites.intros(1) rrewrites.intros(2) by blast |
1038 |
967 |
1039 lemma real_trans: |
968 lemma real_trans [trans]: |
1040 assumes a1: "r1 \<leadsto>* r2" and a2: "r2 \<leadsto>* r3" |
969 assumes a1: "r1 \<leadsto>* r2" and a2: "r2 \<leadsto>* r3" |
1041 shows "r1 \<leadsto>* r3" |
970 shows "r1 \<leadsto>* r3" |
1042 using a2 a1 |
971 using a2 a1 |
1043 apply(induct r2 r3 arbitrary: r1 rule: rrewrites.induct) |
972 apply(induct r2 r3 arbitrary: r1 rule: rrewrites.induct) |
1044 apply(auto) |
973 apply(auto) |
1219 |
1148 |
1220 apply (meson nonazero.elims(3)) |
1149 apply (meson nonazero.elims(3)) |
1221 apply(subgoal_tac "(a#rs) f\<leadsto>* (a#flts rs)") |
1150 apply(subgoal_tac "(a#rs) f\<leadsto>* (a#flts rs)") |
1222 apply (metis append_Nil frewritesaalts) |
1151 apply (metis append_Nil frewritesaalts) |
1223 apply (meson fltsfrewrites fs4 nonalt.elims(3) nonazero.elims(3)) |
1152 apply (meson fltsfrewrites fs4 nonalt.elims(3) nonazero.elims(3)) |
1224 by (metis append_Cons append_Nil fltsfrewrites frewritesaalts k00 k0a) |
1153 by (metis append_Cons append_Nil fltsfrewrites frewritesaalts flts_append k0a) |
1225 |
1154 |
1226 lemma alts_simpalts: "\<And>bs1 rs. (\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimp x) \<Longrightarrow> |
1155 lemma alts_simpalts: "\<And>bs1 rs. (\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimp x) \<Longrightarrow> |
1227 AALTs bs1 rs \<leadsto>* AALTs bs1 (map bsimp rs)" |
1156 AALTs bs1 rs \<leadsto>* AALTs bs1 (map bsimp rs)" |
1228 apply(subgoal_tac " rs s\<leadsto>* (map bsimp rs)") |
1157 apply(subgoal_tac " rs s\<leadsto>* (map bsimp rs)") |
1229 prefer 2 |
1158 prefer 2 |
1343 using fltsrewrites apply auto[1] |
1272 using fltsrewrites apply auto[1] |
1344 |
1273 |
1345 using alts_simpalts by force |
1274 using alts_simpalts by force |
1346 |
1275 |
1347 |
1276 |
1348 lemma rewritenullable: "\<lbrakk>r1 \<leadsto> r2; bnullable r1 \<rbrakk> \<Longrightarrow> bnullable r2" |
|
1349 apply(induction r1 r2 rule: rrewrite.induct) |
|
1350 apply(simp)+ |
|
1351 apply (metis bnullable_correctness erase_fuse) |
|
1352 apply simp |
|
1353 apply simp |
|
1354 apply auto[1] |
|
1355 apply auto[1] |
|
1356 apply auto[4] |
|
1357 apply (metis UnCI bnullable_correctness erase_fuse imageI) |
|
1358 apply (metis bnullable_correctness erase_fuse) |
|
1359 apply (metis bnullable_correctness erase_fuse) |
|
1360 |
|
1361 apply (metis bnullable_correctness erase.simps(5) erase_fuse) |
|
1362 |
|
1363 |
|
1364 by (smt (z3) Un_iff bnullable_correctness insert_iff list.set(2) qq3 set_append) |
|
1365 |
|
1366 lemma rewrite_non_nullable: "\<lbrakk>r1 \<leadsto> r2; \<not>bnullable r1 \<rbrakk> \<Longrightarrow> \<not>bnullable r2" |
1277 lemma rewrite_non_nullable: "\<lbrakk>r1 \<leadsto> r2; \<not>bnullable r1 \<rbrakk> \<Longrightarrow> \<not>bnullable r2" |
1367 apply(induction r1 r2 rule: rrewrite.induct) |
1278 apply(induction r1 r2 rule: rrewrite.induct) |
1368 apply auto |
1279 apply auto |
1369 apply (metis bnullable_correctness erase_fuse)+ |
1280 apply (metis bnullable_correctness erase_fuse)+ |
1370 done |
1281 done |
1371 |
1282 |
1372 |
1283 lemma rewrite_non_nullable_strong: |
1373 lemma rewritesnullable: "\<lbrakk> r1 \<leadsto>* r2; bnullable r1 \<rbrakk> \<Longrightarrow> bnullable r2" |
1284 assumes "r1 \<leadsto> r2" |
|
1285 shows "bnullable r1 = bnullable r2" |
|
1286 using assms |
|
1287 apply(induction r1 r2 rule: rrewrite.induct) |
|
1288 apply(auto) |
|
1289 apply(metis bnullable_correctness erase_fuse)+ |
|
1290 apply(metis UnCI bnullable_correctness erase_fuse imageI) |
|
1291 apply(metis bnullable_correctness erase_fuse)+ |
|
1292 done |
|
1293 |
|
1294 lemma rewrite_nullable: |
|
1295 assumes "r1 \<leadsto> r2" "bnullable r1" |
|
1296 shows "bnullable r2" |
|
1297 using assms rewrite_non_nullable_strong |
|
1298 by auto |
|
1299 |
|
1300 lemma rewritesnullable: |
|
1301 assumes "r1 \<leadsto>* r2" "bnullable r1" |
|
1302 shows "bnullable r2" |
|
1303 using assms |
1374 apply(induction r1 r2 rule: rrewrites.induct) |
1304 apply(induction r1 r2 rule: rrewrites.induct) |
1375 apply simp |
|
1376 apply(rule rewritenullable) |
|
1377 apply simp |
|
1378 apply simp |
1305 apply simp |
1379 done |
1306 using rewrite_non_nullable_strong by blast |
1380 |
1307 |
1381 lemma nonbnullable_lists_concat: " \<lbrakk> \<not> (\<exists>r0\<in>set rs1. bnullable r0); \<not> bnullable r; \<not> (\<exists>r0\<in>set rs2. bnullable r0)\<rbrakk> \<Longrightarrow> |
1308 lemma nonbnullable_lists_concat: " \<lbrakk> \<not> (\<exists>r0\<in>set rs1. bnullable r0); \<not> bnullable r; \<not> (\<exists>r0\<in>set rs2. bnullable r0)\<rbrakk> \<Longrightarrow> |
1382 \<not>(\<exists>r0 \<in> (set (rs1@[r]@rs2)). bnullable r0 ) " |
1309 \<not>(\<exists>r0 \<in> (set (rs1@[r]@rs2)). bnullable r0 ) " |
1383 apply simp |
1310 apply simp |
1384 apply blast |
1311 apply blast |
1410 |
1337 |
1411 lemma bnullablewhichbmkeps: "\<lbrakk>bnullable (AALTs bs (rs1@[r]@rs2)); \<not> bnullable (AALTs bs rs1); bnullable r \<rbrakk> |
1338 lemma bnullablewhichbmkeps: "\<lbrakk>bnullable (AALTs bs (rs1@[r]@rs2)); \<not> bnullable (AALTs bs rs1); bnullable r \<rbrakk> |
1412 \<Longrightarrow> bmkeps (AALTs bs (rs1@[r]@rs2)) = bs @ (bmkeps r)" |
1339 \<Longrightarrow> bmkeps (AALTs bs (rs1@[r]@rs2)) = bs @ (bmkeps r)" |
1413 using qq2 bnullable_Hdbmkeps_Hd by force |
1340 using qq2 bnullable_Hdbmkeps_Hd by force |
1414 |
1341 |
1415 lemma rrewrite_nbnullable: "\<lbrakk> r1 \<leadsto> r2 ; \<not> bnullable r1 \<rbrakk> \<Longrightarrow> \<not>bnullable r2" |
|
1416 apply(induction rule: rrewrite.induct) |
|
1417 apply auto[1] |
|
1418 apply auto[1] |
|
1419 apply auto[1] |
|
1420 apply (metis bnullable_correctness erase_fuse) |
|
1421 apply auto[1] |
|
1422 apply auto[1] |
|
1423 apply auto[1] |
|
1424 apply auto[1] |
|
1425 apply auto[1] |
|
1426 apply (metis bnullable_correctness erase_fuse) |
|
1427 apply auto[1] |
|
1428 apply (metis bnullable_correctness erase_fuse) |
|
1429 apply auto[1] |
|
1430 apply (metis bnullable_correctness erase_fuse) |
|
1431 apply auto[1] |
|
1432 apply auto[1] |
|
1433 |
|
1434 apply (metis bnullable_correctness erase_fuse) |
|
1435 |
|
1436 by (meson rewrite_non_nullable rrewrite.intros(13)) |
|
1437 |
|
1438 |
|
1439 |
1342 |
1440 |
1343 |
1441 lemma spillbmkepslistr: "bnullable (AALTs bs1 rs1) |
1344 lemma spillbmkepslistr: "bnullable (AALTs bs1 rs1) |
1442 \<Longrightarrow> bmkeps (AALTs bs (AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs ( map (fuse bs1) rs1 @ rsb))" |
1345 \<Longrightarrow> bmkeps (AALTs bs (AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs ( map (fuse bs1) rs1 @ rsb))" |
1443 apply(subst bnullable_Hdbmkeps_Hd) |
1346 apply(subst bnullable_Hdbmkeps_Hd) |
1446 by (metis bmkeps.simps(3) k0a list.set_intros(1) qq1 qq4 qs3) |
1349 by (metis bmkeps.simps(3) k0a list.set_intros(1) qq1 qq4 qs3) |
1447 |
1350 |
1448 lemma third_segment_bnullable: "\<lbrakk>bnullable (AALTs bs (rs1@rs2@rs3)); \<not>bnullable (AALTs bs rs1); \<not>bnullable (AALTs bs rs2)\<rbrakk> \<Longrightarrow> |
1351 lemma third_segment_bnullable: "\<lbrakk>bnullable (AALTs bs (rs1@rs2@rs3)); \<not>bnullable (AALTs bs rs1); \<not>bnullable (AALTs bs rs2)\<rbrakk> \<Longrightarrow> |
1449 bnullable (AALTs bs rs3)" |
1352 bnullable (AALTs bs rs3)" |
1450 |
1353 |
1451 by (metis append.left_neutral append_Cons bnullable.simps(1) bnullable_segment rrewrite.intros(7) rrewrite_nbnullable) |
1354 by (metis append.left_neutral append_Cons bnullable.simps(1) bnullable_segment rrewrite.intros(7) rewrite_non_nullable) |
1452 |
1355 |
1453 |
1356 |
1454 lemma third_segment_bmkeps: "\<lbrakk>bnullable (AALTs bs (rs1@rs2@rs3)); \<not>bnullable (AALTs bs rs1); \<not>bnullable (AALTs bs rs2)\<rbrakk> \<Longrightarrow> |
1357 lemma third_segment_bmkeps: "\<lbrakk>bnullable (AALTs bs (rs1@rs2@rs3)); \<not>bnullable (AALTs bs rs1); \<not>bnullable (AALTs bs rs2)\<rbrakk> \<Longrightarrow> |
1455 bmkeps (AALTs bs (rs1@rs2@rs3) ) = bmkeps (AALTs bs rs3)" |
1358 bmkeps (AALTs bs (rs1@rs2@rs3) ) = bmkeps (AALTs bs rs3)" |
1456 apply(subgoal_tac "bnullable (AALTs bs rs3)") |
1359 apply(subgoal_tac "bnullable (AALTs bs rs3)") |
1475 |
1378 |
1476 |
1379 |
1477 using r2 apply blast |
1380 using r2 apply blast |
1478 |
1381 |
1479 apply (metis list.set_intros(1)) |
1382 apply (metis list.set_intros(1)) |
1480 apply (smt (verit, ccfv_threshold) append_eq_append_conv2 list.set_intros(1) qq2 qq3 rewritenullable rrewrite.intros(8) self_append_conv2 spillbmkepslistr) |
1383 apply (smt (verit, ccfv_threshold) append_eq_append_conv2 list.set_intros(1) qq2 qq3 rewrite_nullable rrewrite.intros(8) self_append_conv2 spillbmkepslistr) |
1481 |
1384 |
1482 |
1385 |
1483 thm qq1 |
1386 thm qq1 |
1484 apply(subgoal_tac "bmkeps (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs rsb) ") |
1387 apply(subgoal_tac "bmkeps (AALTs bs (rsa @ AALTs bs1 rs1 # rsb)) = bmkeps (AALTs bs rsb) ") |
1485 prefer 2 |
1388 prefer 2 |
1486 |
1389 |
1487 apply (metis append_Cons append_Nil bnullable.simps(1) bnullable_segment rewritenullable rrewrite.intros(11) third_segment_bmkeps) |
1390 apply (metis append_Cons append_Nil bnullable.simps(1) bnullable_segment rewrite_nullable rrewrite.intros(11) third_segment_bmkeps) |
1488 |
1391 |
1489 by (metis bnullable.simps(4) rewrite_non_nullable rrewrite.intros(10) third_segment_bmkeps) |
1392 by (metis bnullable.simps(4) rewrite_non_nullable rrewrite.intros(10) third_segment_bmkeps) |
1490 |
1393 |
1491 |
1394 |
1492 |
1395 |
1493 lemma rewrite_bmkeps: "\<lbrakk> r1 \<leadsto> r2; (bnullable r1)\<rbrakk> \<Longrightarrow> bmkeps r1 = bmkeps r2" |
1396 lemma rewrite_bmkeps: "\<lbrakk> r1 \<leadsto> r2; (bnullable r1)\<rbrakk> \<Longrightarrow> bmkeps r1 = bmkeps r2" |
1494 |
1397 |
1495 apply(frule rewritenullable) |
1398 apply(frule rewrite_nullable) |
1496 apply simp |
1399 apply simp |
1497 apply(induction r1 r2 rule: rrewrite.induct) |
1400 apply(induction r1 r2 rule: rrewrite.induct) |
1498 apply simp |
1401 apply simp |
1499 using bnullable.simps(1) bnullable.simps(5) apply blast |
1402 using bnullable.simps(1) bnullable.simps(5) apply blast |
1500 apply (simp add: b2) |
1403 apply (simp add: b2) |
1502 apply simp |
1405 apply simp |
1503 apply(frule bnullable_segment) |
1406 apply(frule bnullable_segment) |
1504 apply(case_tac "bnullable (AALTs bs rs1)") |
1407 apply(case_tac "bnullable (AALTs bs rs1)") |
1505 using qq1 apply force |
1408 using qq1 apply force |
1506 apply(case_tac "bnullable r") |
1409 apply(case_tac "bnullable r") |
1507 using bnullablewhichbmkeps rewritenullable apply presburger |
1410 using bnullablewhichbmkeps rewrite_nullable apply presburger |
1508 apply(subgoal_tac "bnullable (AALTs bs rs2)") |
1411 apply(subgoal_tac "bnullable (AALTs bs rs2)") |
1509 apply(subgoal_tac "\<not> bnullable r'") |
1412 apply(subgoal_tac "\<not> bnullable r'") |
1510 apply (simp add: qq2 r1) |
1413 apply (simp add: qq2 r1) |
1511 |
1414 |
1512 using rrewrite_nbnullable apply blast |
1415 using rewrite_non_nullable apply blast |
1513 |
1416 |
1514 apply blast |
1417 apply blast |
1515 apply (simp add: flts_append qs3) |
1418 apply (simp add: flts_append qs3) |
1516 |
1419 |
1517 apply (meson rewrite_bmkepsalt) |
1420 apply (meson rewrite_bmkepsalt) |
1524 |
1427 |
1525 apply (simp add: b2) |
1428 apply (simp add: b2) |
1526 |
1429 |
1527 by (smt (z3) Un_iff bnullable_correctness erase.simps(5) qq1 qq2 qq3 set_append) |
1430 by (smt (z3) Un_iff bnullable_correctness erase.simps(5) qq1 qq2 qq3 set_append) |
1528 |
1431 |
1529 |
1432 lemma rewrites_bmkeps: |
1530 |
1433 assumes "r1 \<leadsto>* r2" "bnullable r1" |
1531 lemma rewrites_bmkeps: "\<lbrakk> (r1 \<leadsto>* r2); (bnullable r1)\<rbrakk> \<Longrightarrow> bmkeps r1 = bmkeps r2" |
1434 shows "bmkeps r1 = bmkeps r2" |
1532 apply(induction r1 r2 rule: rrewrites.induct) |
1435 using assms |
1533 apply simp |
1436 proof(induction r1 r2 rule: rrewrites.induct) |
1534 apply(subgoal_tac "bnullable r2") |
1437 case (rs1 r) |
1535 prefer 2 |
1438 then show "bmkeps r = bmkeps r" by simp |
1536 apply(metis rewritesnullable) |
1439 next |
1537 apply(subgoal_tac "bmkeps r1 = bmkeps r2") |
1440 case (rs2 r1 r2 r3) |
1538 prefer 2 |
1441 then have IH: "bmkeps r1 = bmkeps r2" by simp |
1539 apply fastforce |
1442 have a1: "bnullable r1" by fact |
1540 using rewrite_bmkeps by presburger |
1443 have a2: "r1 \<leadsto>* r2" by fact |
1541 |
1444 have a3: "r2 \<leadsto> r3" by fact |
1542 |
1445 have a4: "bnullable r2" using a1 a2 by (simp add: rewritesnullable) |
1543 thm rrewrite.intros(12) |
1446 then have "bmkeps r2 = bmkeps r3" using rewrite_bmkeps a3 a4 by simp |
|
1447 then show "bmkeps r1 = bmkeps r3" using IH by simp |
|
1448 qed |
|
1449 |
1544 lemma alts_rewrite_front: "r \<leadsto> r' \<Longrightarrow> AALTs bs (r # rs) \<leadsto> AALTs bs (r' # rs)" |
1450 lemma alts_rewrite_front: "r \<leadsto> r' \<Longrightarrow> AALTs bs (r # rs) \<leadsto> AALTs bs (r' # rs)" |
1545 by (metis append_Cons append_Nil rrewrite.intros(6)) |
1451 by (metis append_Cons append_Nil rrewrite.intros(6)) |
1546 |
1452 |
1547 lemma alt_rewrite_front: "r \<leadsto> r' \<Longrightarrow> AALT bs r r2 \<leadsto> AALT bs r' r2" |
1453 lemma alt_rewrite_front: "r \<leadsto> r' \<Longrightarrow> AALT bs r r2 \<leadsto> AALT bs r' r2" |
1548 using alts_rewrite_front by blast |
1454 using alts_rewrite_front by blast |
1646 apply simp+ |
1552 apply simp+ |
1647 apply(subgoal_tac "bmkeps r1 = bmkeps r2") |
1553 apply(subgoal_tac "bmkeps r1 = bmkeps r2") |
1648 prefer 2 |
1554 prefer 2 |
1649 using rewrite_bmkeps apply auto[1] |
1555 using rewrite_bmkeps apply auto[1] |
1650 using contextrewrites1 star_seq apply auto[1] |
1556 using contextrewrites1 star_seq apply auto[1] |
1651 using rewritenullable apply auto[1] |
1557 using rewrite_nullable apply auto[1] |
1652 apply(case_tac "bnullable r1") |
1558 apply(case_tac "bnullable r1") |
1653 apply simp |
1559 apply simp |
1654 apply(subgoal_tac "ASEQ [] (bder c r1) r3 \<leadsto> ASEQ [] (bder c r1) r4") |
1560 apply(subgoal_tac "ASEQ [] (bder c r1) r3 \<leadsto> ASEQ [] (bder c r1) r4") |
1655 prefer 2 |
1561 prefer 2 |
1656 using rrewrite.intros(5) apply blast |
1562 using rrewrite.intros(5) apply blast |
1678 |
1584 |
1679 using lock_step_der_removal by auto |
1585 using lock_step_der_removal by auto |
1680 |
1586 |
1681 |
1587 |
1682 |
1588 |
1683 lemma rewrites_after_der: " r1 \<leadsto>* r2 \<Longrightarrow> (bder c r1) \<leadsto>* (bder c r2)" |
1589 lemma rewrites_after_der: |
1684 apply(induction r1 r2 rule: rrewrites.induct) |
1590 assumes "r1 \<leadsto>* r2" |
1685 apply(rule rs1) |
1591 shows "bder c r1 \<leadsto>* bder c r2" |
1686 by (meson real_trans rewrite_after_der) |
1592 using assms |
1687 |
1593 apply(induction r1 r2 rule: rrewrites.induct) |
1688 |
1594 apply(simp_all add: rewrite_after_der real_trans) |
1689 |
1595 done |
1690 |
1596 |
1691 lemma central: " (bders r s) \<leadsto>* (bders_simp r s)" |
1597 lemma central: |
1692 apply(induct s arbitrary: r rule: rev_induct) |
1598 shows "bders r s \<leadsto>* bders_simp r s" |
1693 |
1599 proof(induct s arbitrary: r rule: rev_induct) |
1694 apply simp |
1600 case Nil |
1695 apply(subst bders_append) |
1601 then show "bders r [] \<leadsto>* bders_simp r []" by simp |
1696 apply(subst bders_simp_append) |
1602 next |
1697 by (metis bders.simps(1) bders.simps(2) bders_simp.simps(1) bders_simp.simps(2) bsimp_rewrite real_trans rewrites_after_der) |
1603 case (snoc x xs) |
1698 |
1604 have IH: "\<And>r. bders r xs \<leadsto>* bders_simp r xs" by fact |
1699 |
1605 have "bders r (xs @ [x]) = bders (bders r xs) [x]" by (simp add: bders_append) |
1700 |
1606 also have "... \<leadsto>* bders (bders_simp r xs) [x]" using IH |
1701 thm arexp.induct |
1607 by (simp add: rewrites_after_der) |
1702 |
1608 also have "... \<leadsto>* bders_simp (bders_simp r xs) [x]" using IH |
1703 lemma quasi_main: "bnullable (bders r s) \<Longrightarrow> bmkeps (bders r s) = bmkeps (bders_simp r s)" |
1609 by (simp add: bsimp_rewrite) |
1704 using central rewrites_bmkeps by blast |
1610 finally show "bders r (xs @ [x]) \<leadsto>* bders_simp r (xs @ [x])" |
1705 |
1611 by (simp add: bders_simp_append) |
1706 theorem main_main: "blexer r s = blexer_simp r s" |
1612 qed |
|
1613 |
|
1614 |
|
1615 lemma quasi_main: |
|
1616 assumes "bnullable (bders r s)" |
|
1617 shows "bmkeps (bders r s) = bmkeps (bders_simp r s)" |
|
1618 using assms central rewrites_bmkeps by blast |
|
1619 |
|
1620 theorem main_main: |
|
1621 shows "blexer r s = blexer_simp r s" |
1707 by (simp add: b4 blexer_def blexer_simp_def quasi_main) |
1622 by (simp add: b4 blexer_def blexer_simp_def quasi_main) |
1708 |
1623 |
1709 |
1624 |
1710 theorem blexersimp_correctness: "blexer_simp r s= lexer r s" |
1625 theorem blexersimp_correctness: |
|
1626 shows "lexer r s = blexer_simp r s" |
1711 using blexer_correctness main_main by auto |
1627 using blexer_correctness main_main by auto |
1712 |
1628 |
1713 |
1629 |
1714 unused_thms |
1630 unused_thms |
1715 |
1631 |