1480 r' \<leadsto>* bsimp bsimp r |
1480 r' \<leadsto>* bsimp bsimp r |
1481 size bsimp r > size r' \<ge> size bsimp bsimp r*) |
1481 size bsimp r > size r' \<ge> size bsimp bsimp r*) |
1482 |
1482 |
1483 fun orderedSufAux :: "nat \<Rightarrow> char list \<Rightarrow> char list list" |
1483 fun orderedSufAux :: "nat \<Rightarrow> char list \<Rightarrow> char list list" |
1484 where |
1484 where |
1485 "orderedSufAux (Suc 0) ss = Nil" |
1485 "orderedSufAux (Suc i) ss = (drop i ss) # (orderedSufAux i ss)" |
1486 |"orderedSufAux (Suc i) ss = (drop i ss) # (orderedSufAux i ss)" |
|
1487 |"orderedSufAux 0 ss = Nil" |
1486 |"orderedSufAux 0 ss = Nil" |
1488 |
1487 |
1489 fun |
1488 fun |
1490 orderedSuf :: "char list \<Rightarrow> char list list" |
1489 orderedSuf :: "char list \<Rightarrow> char list list" |
1491 where |
1490 where |
1492 "orderedSuf s = orderedSufAux (length s) s" |
1491 "orderedSuf s = orderedSufAux (length s) s" |
1493 |
1492 |
|
1493 fun orderedPrefAux :: "nat \<Rightarrow> char list \<Rightarrow> char list list" |
|
1494 where |
|
1495 "orderedPrefAux (Suc i) ss = (take i ss) # (orderedPrefAux i ss)" |
|
1496 |"orderedPrefAux 0 ss = Nil" |
|
1497 |
|
1498 |
|
1499 fun orderedPref :: "char list \<Rightarrow> char list list" |
|
1500 where |
|
1501 "orderedPref s = orderedPrefAux (length s) s" |
|
1502 |
|
1503 lemma shape_of_pref_1list: |
|
1504 shows "orderedPref [c] = [[]]" |
|
1505 apply auto |
|
1506 done |
|
1507 |
|
1508 lemma shape_of_suf_1list: |
|
1509 shows "orderedSuf [c] = [[c]]" |
|
1510 by auto |
|
1511 |
1494 lemma shape_of_suf_2list: |
1512 lemma shape_of_suf_2list: |
1495 shows "orderedSuf [c1, c2] = [[c2]]" |
1513 shows "orderedSuf [c2, c3] = [[c3], [c2,c3]]" |
1496 apply auto |
1514 by auto |
1497 done |
1515 |
|
1516 lemma shape_of_prf_2list: |
|
1517 shows "orderedPref [c1, c2] = [[c1], []]" |
|
1518 by auto |
1498 |
1519 |
1499 |
1520 |
1500 lemma shape_of_suf_3list: |
1521 lemma shape_of_suf_3list: |
1501 shows "orderedSuf [c1, c2, c3] = [[c3], [c2, c3]]" |
1522 shows "orderedSuf [c1, c2, c3] = [[c3], [c2, c3], [c1, c2, c3]]" |
1502 apply auto |
1523 by auto |
1503 done |
1524 |
|
1525 lemma throwing_elem_around: |
|
1526 shows "orderedSuf (s1 @ [a] @ s) = (orderedSuf s) @ (map (\<lambda>s11. s11 @ s) (orderedSuf ( s1 @ [a]) ))" |
|
1527 and "orderedSuf (s1 @ [a] @ s) = (orderedSuf ([a] @ s) @ (map (\<lambda>s11. s11 @ ([a] @ s))) (orderedSuf s1) )" |
|
1528 sorry |
|
1529 |
|
1530 |
|
1531 lemma suf_cons: |
|
1532 shows "orderedSuf (s1 @ s) = (orderedSuf s) @ (map (\<lambda>s11. s11 @ s) (orderedSuf s1))" |
|
1533 apply(induct s arbitrary: s1) |
|
1534 apply simp |
|
1535 apply(subgoal_tac "s1 @ a # s = (s1 @ [a]) @ s") |
|
1536 prefer 2 |
|
1537 apply simp |
|
1538 apply(subgoal_tac "orderedSuf (s1 @ a # s) = orderedSuf ((s1 @ [a]) @ s)") |
|
1539 prefer 2 |
|
1540 apply presburger |
|
1541 apply(drule_tac x="s1 @ [a]" in meta_spec) |
|
1542 sorry |
|
1543 |
|
1544 |
|
1545 |
|
1546 lemma shape_of_prf_3list: |
|
1547 shows "orderedPref [c1, c2, c3] = [[c1, c2], [c1], []]" |
|
1548 by auto |
|
1549 |
|
1550 fun zip_concat :: "char list list \<Rightarrow> char list list \<Rightarrow> char list list" |
|
1551 where |
|
1552 "zip_concat (s1#ss1) (s2#ss2) = (s1@s2) # (zip_concat ss1 ss2)" |
|
1553 | "zip_concat [] [] = []" |
|
1554 | "zip_concat [] (s2#ss2) = s2 # (zip_concat [] ss2)" |
|
1555 | "zip_concat (s1#ss1) [] = s1 # (zip_concat ss1 [])" |
|
1556 |
|
1557 |
|
1558 |
|
1559 lemma compliment_pref_suf: |
|
1560 shows "zip_concat (orderedPref s) (orderedSuf s) = replicate (length s) s " |
|
1561 apply(induct s) |
|
1562 apply auto[1] |
|
1563 sorry |
|
1564 |
1504 |
1565 |
1505 |
1566 |
1506 |
1567 |
1507 datatype rrexp = |
1568 datatype rrexp = |
1508 RZERO |
1569 RZERO |
1600 rders_simp :: "rrexp \<Rightarrow> string \<Rightarrow> rrexp" |
1661 rders_simp :: "rrexp \<Rightarrow> string \<Rightarrow> rrexp" |
1601 where |
1662 where |
1602 "rders_simp r [] = r" |
1663 "rders_simp r [] = r" |
1603 | "rders_simp r (c#s) = rders_simp (rsimp (rder c r)) s" |
1664 | "rders_simp r (c#s) = rders_simp (rsimp (rder c r)) s" |
1604 |
1665 |
|
1666 fun rsize :: "rrexp \<Rightarrow> nat" where |
|
1667 "rsize RZERO = 1" |
|
1668 | "rsize (RONE) = 1" |
|
1669 | "rsize (RCHAR c) = 1" |
|
1670 | "rsize (RALTS rs) = Suc (sum_list (map rsize rs))" |
|
1671 | "rsize (RSEQ r1 r2) = Suc (rsize r1 + rsize r2)" |
|
1672 | "rsize (RSTAR r) = Suc (rsize r)" |
|
1673 |
1605 |
1674 |
1606 lemma rerase_bsimp: |
1675 lemma rerase_bsimp: |
1607 shows "rerase (bsimp r) = rsimp (rerase r)" |
1676 shows "rerase (bsimp r) = rsimp (rerase r)" |
1608 apply(induct r) |
1677 apply(induct r) |
1609 apply auto |
1678 apply auto |
1610 |
1679 |
1611 |
1680 |
1612 sorry |
1681 sorry |
|
1682 |
1613 |
1683 |
1614 lemma rerase_bder: |
1684 lemma rerase_bder: |
1615 shows "rerase (bder c r) = rder c (rerase r)" |
1685 shows "rerase (bder c r) = rder c (rerase r)" |
1616 apply(induct r) |
1686 apply(induct r) |
1617 apply auto |
1687 apply auto |
1618 sorry |
1688 sorry |
1619 |
1689 (* |
1620 lemma rders_shape: |
1690 lemma rders_shape: |
1621 shows "rders_simp (RSEQ r1 r2) s = |
1691 shows "s \<noteq> [] \<Longrightarrow> rders_simp (RSEQ r1 r2) s = |
1622 rsimp (RALTS ((RSEQ (rders r1 s) r2) # |
1692 rsimp (RALTS ((RSEQ (rders r1 s) r2) # |
1623 (map (rders r2) (orderedSuf s))) )" |
1693 (map (rders r2) (orderedSuf s))) )" |
|
1694 apply(induct s arbitrary: r1 r2 rule: rev_induct) |
|
1695 apply simp |
|
1696 apply simp |
|
1697 |
1624 sorry |
1698 sorry |
|
1699 *) |
|
1700 |
|
1701 lemma ders_simp_comm_onechar: |
|
1702 shows " rerase (bders_simp r [c]) = rerase (bsimp (bders r [c]))" |
|
1703 and " rders_simp (RSEQ r1 r2) [c] = |
|
1704 rsimp (RALTS ((RSEQ (rders r1 [c]) r2) # |
|
1705 (map (rders r2) (orderedSuf [c]))) )" |
|
1706 apply simp |
|
1707 apply(simp add: rders.simps) |
|
1708 apply(case_tac "rsimp (rder c r1) = RZERO") |
|
1709 apply simp |
|
1710 apply auto |
|
1711 sledgehammer |
|
1712 oops |
|
1713 |
|
1714 fun rders_cond_list :: "rrexp \<Rightarrow> bool list \<Rightarrow> char list list \<Rightarrow> rrexp list" |
|
1715 where |
|
1716 "rders_cond_list r2 (True # bs) (s # strs) = (rders r2 s) # (rders_cond_list r2 bs strs)" |
|
1717 | "rders_cond_list r2 (False # bs) (s # strs) = rders_cond_list r2 bs strs" |
|
1718 | "rders_cond_list r2 [] s = []" |
|
1719 | "rders_cond_list r2 bs [] = []" |
|
1720 |
|
1721 fun nullable_bools :: "rrexp \<Rightarrow> char list list \<Rightarrow> bool list" |
|
1722 where |
|
1723 "nullable_bools r (s#strs) = (rnullable (rders r s)) # (nullable_bools r strs) " |
|
1724 |"nullable_bools r [] = []" |
1625 |
1725 |
1626 |
1726 |
1627 lemma ders_simp_commute: |
1727 lemma ders_simp_commute: |
1628 shows "rerase (bsimp (bders_simp r s)) = rerase (bsimp (bders r s))" |
1728 shows "\<lbrakk>s \<noteq>[] \<rbrakk> \<Longrightarrow> rerase (bders_simp r s) = rerase (bsimp (bders r s))" |
1629 apply(induct s arbitrary: r rule: rev_induct) |
1729 and "\<lbrakk>s \<noteq> []\<rbrakk> \<Longrightarrow> rders_simp (RSEQ r1 r2) s = |
1630 apply simp |
1730 rsimp (RALTS ((RSEQ (rders r1 s) r2) # |
1631 apply (simp add: bders_simp_append bders_append ) |
1731 (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s))) )" |
1632 apply (simp add: rerase_bsimp) |
1732 apply(induct s arbitrary: r r1 r2 rule: rev_induct) |
1633 apply (simp add: rerase_bder) |
1733 apply simp |
1634 apply (simp add: rders_shape) |
1734 apply simp |
1635 sledgehammer |
1735 apply(case_tac "xs = []") |
1636 oops |
1736 |
1637 |
1737 apply (simp add: bders_simp_append ) |
|
1738 apply(subgoal_tac "rerase (bsimp (bder x (bders_simp r xs))) = (rsimp (rerase (bder x (bders_simp r xs)))) ") |
|
1739 prefer 2 |
|
1740 apply (simp add: rerase_bsimp) |
|
1741 apply(subgoal_tac "(rsimp (rerase (bder x (bders_simp r xs)))) = (rsimp (rder x (rerase (bders_simp r xs))))") |
|
1742 |
|
1743 apply(subgoal_tac "xs \<noteq> [] \<Longrightarrow> rsimp (rder x (rerase (bders_simp r xs))) = rsimp (rder x (rerase (bsimp (bders r xs))))") |
|
1744 prefer 2 |
|
1745 apply presburger |
|
1746 sorry |
|
1747 |
|
1748 lemma finite_size_finite_regx: |
|
1749 shows "\<forall>N. \<exists>l. (\<forall>r \<in> (set rs). rsize r < N) \<and> (distinct rs) \<Longrightarrow> (length rs) < l " |
|
1750 sorry |
|
1751 |
|
1752 |
|
1753 (*below probably needs proved concurrently*) |
|
1754 |
|
1755 lemma finite_r1r2_ders_list: |
|
1756 shows "\<forall>r1 r2. \<exists>l. |
|
1757 (length (rdistinct (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s)) {})) < l " |
|
1758 sorry |
|
1759 |
|
1760 lemma finite_seq: |
|
1761 shows "(\<forall>s. rsize (rders_simp r1 s) < N1 \<and> rsize (rders_simp r2 s) < N2) |
|
1762 \<Longrightarrow> \<exists>N3.\<forall>s.(rsize (rders_simp (RSEQ r1 r2) s)) < N3" |
|
1763 sorry |
|
1764 |
|
1765 |
|
1766 lemma finite_size_ders: |
|
1767 shows "\<forall>r. \<exists>Nr. \<forall>s. rsize (rders_simp r s) < Nr" |
|
1768 sorry |
1638 |
1769 |
1639 |
1770 |
1640 unused_thms |
1771 unused_thms |
1641 lemma seq_ders_shape: |
1772 lemma seq_ders_shape: |
1642 shows "E" |
1773 shows "E" |