1181 using grewrites_simpalts by force |
1181 using grewrites_simpalts by force |
1182 |
1182 |
1183 |
1183 |
1184 lemma basic_regex_property1: |
1184 lemma basic_regex_property1: |
1185 shows "rnullable r \<Longrightarrow> rsimp r \<noteq> RZERO" |
1185 shows "rnullable r \<Longrightarrow> rsimp r \<noteq> RZERO" |
1186 sorry |
1186 apply(induct r rule: rsimp.induct) |
|
1187 apply(auto) |
|
1188 apply (metis idiot idiot2 rrexp.distinct(5)) |
|
1189 by (metis der_simp_nullability rnullable.simps(1) rnullable.simps(4) rsimp.simps(2)) |
1187 |
1190 |
1188 lemma basic_rsimp_SEQ_property1: |
1191 lemma basic_rsimp_SEQ_property1: |
1189 shows "rsimp_SEQ RONE r = r" |
1192 shows "rsimp_SEQ RONE r = r" |
1190 by (simp add: idiot) |
1193 by (simp add: idiot) |
1191 |
1194 |
1369 apply(case_tac rs3) |
1372 apply(case_tac rs3) |
1370 apply simp |
1373 apply simp |
1371 using grewrites_ralts hrewrite.intros(9) apply blast |
1374 using grewrites_ralts hrewrite.intros(9) apply blast |
1372 by (metis (no_types, opaque_lifting) grewrite_ralts hr_in_rstar hreal_trans hrewrite.intros(10) neq_Nil_conv rsimp_ALTs.simps(2) rsimp_ALTs.simps(3)) |
1375 by (metis (no_types, opaque_lifting) grewrite_ralts hr_in_rstar hreal_trans hrewrite.intros(10) neq_Nil_conv rsimp_ALTs.simps(2) rsimp_ALTs.simps(3)) |
1373 |
1376 |
1374 lemma hrewrites_list: |
1377 lemma hrewrites_alts: |
1375 shows "\<forall>r \<in> set rs. r \<leadsto>* f r \<Longrightarrow> rs \<leadsto>g* map f rs" |
1378 shows " r \<leadsto>* r' \<Longrightarrow> (RALTS (rs1 @ [r] @ rs2)) \<leadsto>* (RALTS (rs1 @ [r'] @ rs2))" |
1376 sorry |
1379 apply(induct r r' rule: hrewrites.induct) |
|
1380 apply simp |
|
1381 using hrewrite.intros(6) by blast |
|
1382 |
|
1383 inductive |
|
1384 srewritescf:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" (" _ scf\<leadsto>* _" [100, 100] 100) |
|
1385 where |
|
1386 ss1: "[] scf\<leadsto>* []" |
|
1387 | ss2: "\<lbrakk>r \<leadsto>* r'; rs scf\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (r#rs) scf\<leadsto>* (r'#rs')" |
|
1388 |
|
1389 |
|
1390 lemma hrewrites_alts_cons: |
|
1391 shows " RALTS rs \<leadsto>* RALTS rs' \<Longrightarrow> RALTS (r # rs) \<leadsto>* RALTS (r # rs')" |
|
1392 |
|
1393 |
|
1394 oops |
|
1395 |
|
1396 |
|
1397 lemma srewritescf_alt: "rs1 scf\<leadsto>* rs2 \<Longrightarrow> (RALTS (rs@rs1)) \<leadsto>* (RALTS (rs@rs2))" |
|
1398 |
|
1399 apply(induct rs1 rs2 arbitrary: rs rule: srewritescf.induct) |
|
1400 apply(rule rs1) |
|
1401 apply(drule_tac x = "rsa@[r']" in meta_spec) |
|
1402 apply simp |
|
1403 apply(rule hreal_trans) |
|
1404 prefer 2 |
|
1405 apply(assumption) |
|
1406 apply(drule hrewrites_alts) |
|
1407 by auto |
|
1408 |
|
1409 |
|
1410 corollary srewritescf_alt1: |
|
1411 assumes "rs1 scf\<leadsto>* rs2" |
|
1412 shows "RALTS rs1 \<leadsto>* RALTS rs2" |
|
1413 using assms |
|
1414 by (metis append_Nil srewritescf_alt) |
|
1415 |
|
1416 |
|
1417 |
|
1418 |
|
1419 lemma trivialrsimp_srewrites: |
|
1420 "\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x \<rbrakk> \<Longrightarrow> rs scf\<leadsto>* (map f rs)" |
|
1421 |
|
1422 apply(induction rs) |
|
1423 apply simp |
|
1424 apply(rule ss1) |
|
1425 by (metis insert_iff list.simps(15) list.simps(9) srewritescf.simps) |
|
1426 |
|
1427 lemma hrewrites_list: |
|
1428 shows |
|
1429 " (\<And>xa. xa \<in> set x \<Longrightarrow> xa \<leadsto>* rsimp xa) \<Longrightarrow> RALTS x \<leadsto>* RALTS (map rsimp x)" |
|
1430 apply(induct x) |
|
1431 apply(simp)+ |
|
1432 by (simp add: srewritescf_alt1 ss2 trivialrsimp_srewrites) |
|
1433 (* apply(subgoal_tac "RALTS x \<leadsto>* RALTS (map rsimp x)")*) |
|
1434 |
|
1435 |
|
1436 |
1377 |
1437 |
1378 |
1438 |
1379 lemma simp_hrewrites: |
1439 lemma simp_hrewrites: |
1380 shows "r1 \<leadsto>* rsimp r1" |
1440 shows "r1 \<leadsto>* rsimp r1" |
1381 apply(induct r1) |
1441 apply(induct r1) |
1399 apply simp |
1459 apply simp |
1400 apply(subgoal_tac "RALTS x \<leadsto>* RALTS (map rsimp x)") |
1460 apply(subgoal_tac "RALTS x \<leadsto>* RALTS (map rsimp x)") |
1401 apply(subgoal_tac "RALTS (map rsimp x) \<leadsto>* rsimp_ALTs (rdistinct (rflts (map rsimp x)) {}) ") |
1461 apply(subgoal_tac "RALTS (map rsimp x) \<leadsto>* rsimp_ALTs (rdistinct (rflts (map rsimp x)) {}) ") |
1402 using hreal_trans apply blast |
1462 using hreal_trans apply blast |
1403 apply (meson flts_gstar greal_trans grewrites_ralts_rsimpalts gstar_rdistinct) |
1463 apply (meson flts_gstar greal_trans grewrites_ralts_rsimpalts gstar_rdistinct) |
1404 sledgehammer |
1464 |
|
1465 apply (simp add: grewrites_ralts hrewrites_list) |
|
1466 by simp |
|
1467 |
|
1468 lemma interleave_aux1: |
|
1469 shows " RALT (RSEQ RZERO r1) r \<leadsto>* r" |
|
1470 apply(subgoal_tac "RSEQ RZERO r1 \<leadsto>* RZERO") |
|
1471 apply (metis append_eq_Cons_conv hr_in_rstar hrewrite.intros(10) hrewrite.intros(7) hrewrites.simps) |
|
1472 by (simp add: hr_in_rstar hrewrite.intros(1)) |
|
1473 |
|
1474 lemma rnullable_hrewrite: |
|
1475 shows "r1 \<leadsto> r2 \<Longrightarrow> rnullable r1 = rnullable r2" |
1405 sorry |
1476 sorry |
|
1477 |
|
1478 |
|
1479 lemma interleave1: |
|
1480 shows "r \<leadsto> r' \<Longrightarrow> rder c r \<leadsto>* rder c r'" |
|
1481 apply(induct r r' rule: hrewrite.induct) |
|
1482 |
|
1483 |
|
1484 apply (simp add: hr_in_rstar hrewrite.intros(1)) |
|
1485 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) |
|
1486 apply simp |
|
1487 apply(subst interleave_aux1) |
|
1488 apply simp |
|
1489 apply(case_tac "rnullable r1") |
|
1490 |
|
1491 sorry |
|
1492 |
|
1493 |
1406 |
1494 |
1407 |
1495 |
1408 lemma inside_simp_removal: |
1496 lemma inside_simp_removal: |
1409 shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)" |
1497 shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)" |
1410 apply(induct r) |
1498 apply(induct r) |
1456 by (metis map_idI rsimp.simps(2) rsimp_idem) |
1544 by (metis map_idI rsimp.simps(2) rsimp_idem) |
1457 |
1545 |
1458 |
1546 |
1459 lemma add0_isomorphic: |
1547 lemma add0_isomorphic: |
1460 shows "rsimp_ALTs (rdistinct (rflts [rsimp r, RZERO]) {}) = rsimp r" |
1548 shows "rsimp_ALTs (rdistinct (rflts [rsimp r, RZERO]) {}) = rsimp r" |
1461 sorry |
1549 by (metis append.left_neutral append_Cons flts_removes0 idem_after_simp1) |
1462 |
1550 |
1463 |
1551 |
1464 lemma distinct_append_simp: |
1552 |
1465 shows " rsimp (rsimp_ALTs rs1) = rsimp (rsimp_ALTs rs2) \<Longrightarrow> |
|
1466 rsimp (rsimp_ALTs (f a # rs1)) = |
|
1467 rsimp (rsimp_ALTs (f a # rs2))" |
|
1468 apply(case_tac rs1) |
|
1469 apply simp |
|
1470 apply(case_tac rs2) |
|
1471 apply simp |
|
1472 apply simp |
|
1473 prefer 2 |
|
1474 apply(case_tac list) |
|
1475 apply(case_tac rs2) |
|
1476 apply simp |
|
1477 using add0_isomorphic apply blast |
|
1478 apply simp |
|
1479 oops |
|
1480 |
1553 |
1481 lemma alts_closed_form: shows |
1554 lemma alts_closed_form: shows |
1482 "rsimp (rders_simp (RALTS rs) s) = |
1555 "rsimp (rders_simp (RALTS rs) s) = |
1483 rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))" |
1556 rsimp (RALTS (map (\<lambda>r. rders_simp r s) rs))" |
1484 apply(induct s rule: rev_induct) |
1557 apply(induct s rule: rev_induct) |
1558 "RALTS rs \<leadsto>o rs" |
1631 "RALTS rs \<leadsto>o rs" |
1559 | "r1 \<leadsto>o rs1 \<Longrightarrow> (RALT r1 r2) \<leadsto>o (rs1 @ [r2])" |
1632 | "r1 \<leadsto>o rs1 \<Longrightarrow> (RALT r1 r2) \<leadsto>o (rs1 @ [r2])" |
1560 |
1633 |
1561 |
1634 |
1562 fun sflat :: "rrexp \<Rightarrow> rrexp list " where |
1635 fun sflat :: "rrexp \<Rightarrow> rrexp list " where |
1563 "sflat (RALT r1 r2) = sflat r1 @ [r2]" |
1636 "sflat (RALTS (r # rs)) = sflat r @ rs" |
1564 | "sflat (RALTS rs) = rs" |
1637 | "sflat (RALTS []) = []" |
1565 | "sflat r = [r]" |
1638 | "sflat r = [r]" |
1566 |
1639 |
1567 lemma softrewrite_flat: |
1640 lemma softrewrite_flat: |
1568 shows "r \<leadsto>o sflat r" |
1641 shows "r \<leadsto>o sflat r" |
1569 |
1642 oops |
|
1643 |
|
1644 lemma sflat_der: |
|
1645 shows "sflat r1 = sflat r2 \<Longrightarrow> sflat (rder c r1) = sflat (rder c r2)" |
|
1646 apply(case_tac r1 ) |
|
1647 |
|
1648 |
|
1649 |
1570 |
1650 |
1571 lemma seq_sflat0: |
1651 lemma seq_sflat0: |
1572 shows "sflat (rders (RSEQ r1 r2) s) = sflat (RALTS ( (RSEQ (rders r1 s) r2) # |
1652 shows "sflat (rders (RSEQ r1 r2) s) = sflat (RALTS ( (RSEQ (rders r1 s) r2) # |
1573 (map (rders r2) (vsuf s r1))) )" |
1653 (map (rders r2) (vsuf s r1))) )" |
1574 |
1654 apply(induct s rule: rev_induct) |
|
1655 apply simp |
|
1656 apply(subst rders_append) |
1575 sorry |
1657 sorry |
1576 |
1658 |
1577 lemma seq_sflat1: |
1659 lemma seq_sflat1: |
1578 shows "sflat ( RALTS ( (RSEQ (rders r1 (s @ [c])) r2) # |
1660 shows "sflat ( RALTS ( (RSEQ (rders r1 (s @ [c])) r2) # |
1579 (map (rders r2) (vsuf (s @ [c]) r1)) |
1661 (map (rders r2) (vsuf (s @ [c]) r1)) |