1327 |
1327 |
1328 lemma hrewrites_seq_contexts: |
1328 lemma hrewrites_seq_contexts: |
1329 shows "\<lbrakk>r1 \<leadsto>* r2; r3 \<leadsto>* r4\<rbrakk> \<Longrightarrow> RSEQ r1 r3 \<leadsto>* RSEQ r2 r4" |
1329 shows "\<lbrakk>r1 \<leadsto>* r2; r3 \<leadsto>* r4\<rbrakk> \<Longrightarrow> RSEQ r1 r3 \<leadsto>* RSEQ r2 r4" |
1330 by (meson hreal_trans hrewrites_seq_context hrewrites_seq_context2) |
1330 by (meson hreal_trans hrewrites_seq_context hrewrites_seq_context2) |
1331 |
1331 |
|
1332 lemma hrewrite_simpeq: |
|
1333 shows "r1 \<leadsto> r2 \<Longrightarrow> rsimp r1 = rsimp r2" |
|
1334 apply(induct rule: hrewrite.induct) |
|
1335 apply simp+ |
|
1336 apply (simp add: basic_rsimp_SEQ_property3) |
|
1337 apply (simp add: basic_rsimp_SEQ_property1) |
|
1338 using rsimp.simps(1) apply presburger |
|
1339 apply simp+ |
|
1340 using flts_middle0 apply force |
|
1341 using simp_flatten3 apply presburger |
|
1342 apply simp+ |
|
1343 apply (simp add: idem_after_simp1) |
|
1344 using grewrite.intros(4) grewrite_equal_rsimp by presburger |
|
1345 |
1332 lemma hrewrites_simpeq: |
1346 lemma hrewrites_simpeq: |
1333 shows "r1 \<leadsto>* r2 \<Longrightarrow> rsimp r1 = rsimp r2" |
1347 shows "r1 \<leadsto>* r2 \<Longrightarrow> rsimp r1 = rsimp r2" |
1334 sorry |
1348 apply(induct rule: hrewrites.induct) |
1335 |
1349 apply simp |
1336 lemma distinct_grewrites_subgoal1: |
1350 apply(subgoal_tac "rsimp r2 = rsimp r3") |
1337 shows " \<And>rs1 rs2 rs3 a list. |
1351 apply auto[1] |
1338 \<lbrakk>rs1 \<leadsto>g* [a]; RALTS rs1 \<leadsto>* a; [a] \<leadsto>g rs3; rs2 = [a]; list = []\<rbrakk> \<Longrightarrow> RALTS rs1 \<leadsto>* rsimp_ALTs rs3" |
1352 using hrewrite_simpeq by presburger |
1339 (* apply (smt (z3) append.left_neutral append.right_neutral append_Cons grewrite.simps grewrite_singleton hrewrite.intros(10) hrewrite.intros(9) hrewrites.simps list.inject r_finite1 rsimp_ALTs.elims rsimp_ALTs.simps(2) rsimp_alts_equal)*) |
1353 |
1340 sorry |
|
1341 |
1354 |
1342 lemma grewrite_ralts: |
1355 lemma grewrite_ralts: |
1343 shows "rs \<leadsto>g rs' \<Longrightarrow> RALTS rs \<leadsto>* RALTS rs'" |
1356 shows "rs \<leadsto>g rs' \<Longrightarrow> RALTS rs \<leadsto>* RALTS rs'" |
1344 by (smt (verit) grewrite_cases_middle hr_in_rstar hrewrite.intros(11) hrewrite.intros(7) hrewrite.intros(8)) |
1357 by (smt (verit) grewrite_cases_middle hr_in_rstar hrewrite.intros(11) hrewrite.intros(7) hrewrite.intros(8)) |
1345 |
|
1346 |
|
1347 |
|
1348 |
1358 |
1349 lemma grewrites_ralts: |
1359 lemma grewrites_ralts: |
1350 shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs \<leadsto>* RALTS rs'" |
1360 shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs \<leadsto>* RALTS rs'" |
1351 apply(induct rs rs' rule: grewrites.induct) |
1361 apply(induct rule: grewrites.induct) |
1352 apply simp |
1362 apply simp |
1353 using grewrite_ralts hreal_trans by blast |
1363 using grewrite_ralts hreal_trans by blast |
|
1364 |
|
1365 |
|
1366 lemma distinct_grewrites_subgoal1: |
|
1367 shows " |
|
1368 \<lbrakk>rs1 \<leadsto>g* [a]; RALTS rs1 \<leadsto>* a; [a] \<leadsto>g rs3\<rbrakk> \<Longrightarrow> RALTS rs1 \<leadsto>* rsimp_ALTs rs3" |
|
1369 apply(subgoal_tac "RALTS rs1 \<leadsto>* RALTS rs3") |
|
1370 apply (metis hrewrite.intros(10) hrewrite.intros(9) rs2 rsimp_ALTs.cases rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3)) |
|
1371 apply(subgoal_tac "rs1 \<leadsto>g* rs3") |
|
1372 using grewrites_ralts apply blast |
|
1373 using grewrites.intros(2) by presburger |
|
1374 |
|
1375 |
|
1376 |
|
1377 |
1354 |
1378 |
1355 |
1379 |
1356 lemma grewrites_ralts_rsimpalts: |
1380 lemma grewrites_ralts_rsimpalts: |
1357 shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs \<leadsto>* rsimp_ALTs rs' " |
1381 shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs \<leadsto>* rsimp_ALTs rs' " |
1358 apply(induct rs rs' rule: grewrites.induct) |
1382 apply(induct rs rs' rule: grewrites.induct) |
1475 |
1499 |
1476 |
1500 |
1477 |
1501 |
1478 lemma rnullable_hrewrite: |
1502 lemma rnullable_hrewrite: |
1479 shows "r1 \<leadsto> r2 \<Longrightarrow> rnullable r1 = rnullable r2" |
1503 shows "r1 \<leadsto> r2 \<Longrightarrow> rnullable r1 = rnullable r2" |
1480 sorry |
1504 apply(induct rule: hrewrite.induct) |
|
1505 apply simp+ |
|
1506 apply blast |
|
1507 apply simp+ |
|
1508 done |
1481 |
1509 |
1482 |
1510 |
1483 lemma interleave1: |
1511 lemma interleave1: |
1484 shows "r \<leadsto> r' \<Longrightarrow> rder c r \<leadsto>* rder c r'" |
1512 shows "r \<leadsto> r' \<Longrightarrow> rder c r \<leadsto>* rder c r'" |
1485 apply(induct r r' rule: hrewrite.induct) |
1513 apply(induct r r' rule: hrewrite.induct) |
1486 |
|
1487 |
|
1488 apply (simp add: hr_in_rstar hrewrite.intros(1)) |
1514 apply (simp add: hr_in_rstar hrewrite.intros(1)) |
1489 apply (metis (no_types, lifting) basic_rsimp_SEQ_property3 list.simps(8) list.simps(9) rder.simps(1) rder.simps(5) rdistinct.simps(1) rflts.simps(1) rflts.simps(2) rsimp.simps(1) rsimp.simps(2) rsimp.simps(3) rsimp_ALTs.simps(1) simp_hrewrites) |
1515 apply (metis (no_types, lifting) basic_rsimp_SEQ_property3 list.simps(8) list.simps(9) rder.simps(1) rder.simps(5) rdistinct.simps(1) rflts.simps(1) rflts.simps(2) rsimp.simps(1) rsimp.simps(2) rsimp.simps(3) rsimp_ALTs.simps(1) simp_hrewrites) |
1490 apply simp |
1516 apply simp |
1491 apply(subst interleave_aux1) |
1517 apply(subst interleave_aux1) |
1492 apply simp |
1518 apply simp |
1493 apply(case_tac "rnullable r1") |
1519 apply(case_tac "rnullable r1") |
1494 |
1520 apply simp |
1495 sorry |
1521 |
1496 |
1522 apply (simp add: hrewrites_seq_context rnullable_hrewrite srewritescf_alt1 ss1 ss2) |
1497 |
1523 |
|
1524 apply (simp add: hrewrites_seq_context rnullable_hrewrite) |
|
1525 apply(case_tac "rnullable r1") |
|
1526 apply simp |
|
1527 |
|
1528 using hr_in_rstar hrewrites_seq_context2 srewritescf_alt1 ss1 ss2 apply presburger |
|
1529 apply simp |
|
1530 using hr_in_rstar hrewrites_seq_context2 apply blast |
|
1531 apply simp |
|
1532 |
|
1533 using hrewrites_alts apply auto[1] |
|
1534 apply simp |
|
1535 using grewrite.intros(1) grewrite_append grewrite_ralts apply auto[1] |
|
1536 apply simp |
|
1537 apply (simp add: grewrite.intros(2) grewrite_append grewrite_ralts) |
|
1538 apply (simp add: hr_in_rstar hrewrite.intros(9)) |
|
1539 apply (simp add: hr_in_rstar hrewrite.intros(10)) |
|
1540 apply simp |
|
1541 using hrewrite.intros(11) by auto |
|
1542 |
|
1543 lemma interleave_star1: |
|
1544 shows "r \<leadsto>* r' \<Longrightarrow> rder c r \<leadsto>* rder c r'" |
|
1545 apply(induct rule : hrewrites.induct) |
|
1546 apply simp |
|
1547 by (meson hreal_trans interleave1) |
|
1548 |
1498 |
1549 |
1499 |
1550 |
1500 lemma inside_simp_removal: |
1551 lemma inside_simp_removal: |
1501 shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)" |
1552 shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)" |
1502 apply(induct r) |
1553 apply(induct r) |
1505 apply simp |
1556 apply simp |
1506 |
1557 |
1507 using inside_simp_seq_nullable apply blast |
1558 using inside_simp_seq_nullable apply blast |
1508 apply simp |
1559 apply simp |
1509 apply (smt (verit, del_insts) basic_rsimp_SEQ_property2 basic_rsimp_SEQ_property3 der_simp_nullability rder.simps(1) rder.simps(5) rnullable.simps(2) rsimp.simps(1) rsimp_SEQ.simps(1) rsimp_idem) |
1560 apply (smt (verit, del_insts) basic_rsimp_SEQ_property2 basic_rsimp_SEQ_property3 der_simp_nullability rder.simps(1) rder.simps(5) rnullable.simps(2) rsimp.simps(1) rsimp_SEQ.simps(1) rsimp_idem) |
1510 |
1561 apply(subgoal_tac "rder x (RALTS xa) \<leadsto>* rder x (rsimp (RALTS xa))") |
1511 |
1562 using hrewrites_simpeq apply presburger |
1512 sorry |
1563 using interleave_star1 simp_hrewrites apply presburger |
|
1564 by simp |
|
1565 |
1513 |
1566 |
1514 |
1567 |
1515 |
1568 |
1516 lemma rders_simp_same_simpders: |
1569 lemma rders_simp_same_simpders: |
1517 shows "s \<noteq> [] \<Longrightarrow> rders_simp r s = rsimp (rders r s)" |
1570 shows "s \<noteq> [] \<Longrightarrow> rders_simp r s = rsimp (rders r s)" |
2089 |
2142 |
2090 lemma cbs_hfau_rsimpeq1: |
2143 lemma cbs_hfau_rsimpeq1: |
2091 shows "rsimp (RALT a b) = rsimp (RALTS ((hflat_aux a) @ (hflat_aux b)))" |
2144 shows "rsimp (RALT a b) = rsimp (RALTS ((hflat_aux a) @ (hflat_aux b)))" |
2092 apply(subgoal_tac "[a, b] \<leadsto>g* hflat_aux a @ hflat_aux b") |
2145 apply(subgoal_tac "[a, b] \<leadsto>g* hflat_aux a @ hflat_aux b") |
2093 using grewrites_equal_rsimp apply presburger |
2146 using grewrites_equal_rsimp apply presburger |
2094 sorry |
2147 by (metis append.right_neutral greal_trans grewrites_cons hflat_aux_grewrites) |
2095 |
2148 |
2096 |
2149 |
2097 lemma hfau_rsimpeq2: |
2150 lemma hfau_rsimpeq2: |
2098 shows "created_by_star r \<Longrightarrow> rsimp r = rsimp ( (RALTS (hflat_aux r)))" |
2151 shows "created_by_star r \<Longrightarrow> rsimp r = rsimp ( (RALTS (hflat_aux r)))" |
2099 apply(induct r) |
2152 apply(induct r) |