1630 inductive softrewrite :: "rrexp \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>o _" [100, 100] 100) where |
1634 inductive softrewrite :: "rrexp \<Rightarrow> rrexp list \<Rightarrow> bool" ("_ \<leadsto>o _" [100, 100] 100) where |
1631 "RALTS rs \<leadsto>o rs" |
1635 "RALTS rs \<leadsto>o rs" |
1632 | "r1 \<leadsto>o rs1 \<Longrightarrow> (RALT r1 r2) \<leadsto>o (rs1 @ [r2])" |
1636 | "r1 \<leadsto>o rs1 \<Longrightarrow> (RALT r1 r2) \<leadsto>o (rs1 @ [r2])" |
1633 |
1637 |
1634 |
1638 |
1635 fun sflat :: "rrexp \<Rightarrow> rrexp list " where |
1639 fun sflat_aux :: "rrexp \<Rightarrow> rrexp list " where |
1636 "sflat (RALTS (r # rs)) = sflat r @ rs" |
1640 "sflat_aux (RALTS (r # rs)) = sflat_aux r @ rs" |
1637 | "sflat (RALTS []) = []" |
1641 | "sflat_aux (RALTS []) = []" |
1638 | "sflat r = [r]" |
1642 | "sflat_aux r = [r]" |
1639 |
1643 |
1640 lemma softrewrite_flat: |
1644 |
1641 shows "r \<leadsto>o sflat r" |
1645 fun sflat :: "rrexp \<Rightarrow> rrexp" where |
1642 oops |
1646 "sflat (RALTS (r # [])) = r" |
1643 |
1647 | "sflat (RALTS (r # rs)) = RALTS (sflat_aux r @ rs)" |
1644 lemma sflat_der: |
1648 | "sflat r = r" |
1645 shows "sflat r1 = sflat r2 \<Longrightarrow> sflat (rder c r1) = sflat (rder c r2)" |
1649 |
1646 apply(case_tac r1 ) |
1650 inductive created_by_seq:: "rrexp \<Rightarrow> bool" where |
1647 |
1651 "created_by_seq (RSEQ r1 r2) " |
|
1652 | "created_by_seq r1 \<Longrightarrow> created_by_seq (RALT r1 r2)" |
|
1653 |
|
1654 (*Why \<and> rnullable case would be provable.....?*) |
|
1655 lemma seq_der_shape: |
|
1656 shows "\<forall>r1 r2. \<exists>r3 r4. (rder c (RSEQ r1 r2) = RSEQ r3 r4 \<or> rder c (RSEQ r1 r2) = RALT r3 r4)" |
|
1657 by (meson rder.simps(5)) |
|
1658 |
|
1659 lemma alt_der_shape: |
|
1660 shows "\<forall>rs. \<exists> rs'. (rder c (RALTS rs)) = RALTS (map (rder c) rs)" |
|
1661 by force |
|
1662 |
|
1663 lemma seq_ders_shape1: |
|
1664 shows "\<forall>r1 r2. \<exists>r3 r4. (rders (RSEQ r1 r2) s) = RSEQ r3 r4 \<or> (rders (RSEQ r1 r2) s) = RALT r3 r4" |
|
1665 apply(induct s rule: rev_induct) |
|
1666 apply auto[1] |
|
1667 apply(rule allI)+ |
|
1668 apply(subst rders_append)+ |
|
1669 apply(subgoal_tac " \<exists>r3 r4. rders (RSEQ r1 r2) xs = RSEQ r3 r4 \<or> rders (RSEQ r1 r2) xs = RALT r3 r4 ") |
|
1670 apply(erule exE)+ |
|
1671 apply(erule disjE) |
|
1672 apply simp+ |
|
1673 done |
|
1674 |
|
1675 |
|
1676 lemma seq_ders_shape2: |
|
1677 shows "rders (RSEQ r1 r2) s = RALTS (ra # rb # rs) \<Longrightarrow> rs = []" |
|
1678 using seq_ders_shape1 |
|
1679 by (metis list.inject rrexp.distinct(25) rrexp.inject(3)) |
|
1680 |
|
1681 lemma created_by_seq_der: |
|
1682 shows "created_by_seq r \<Longrightarrow> created_by_seq (rder c r)" |
|
1683 apply(induct r) |
|
1684 apply simp+ |
|
1685 |
|
1686 using created_by_seq.cases apply blast |
|
1687 |
|
1688 apply (meson created_by_seq.cases rrexp.distinct(19) rrexp.distinct(21)) |
|
1689 apply (metis created_by_seq.simps rder.simps(5)) |
|
1690 apply (smt (verit, ccfv_threshold) created_by_seq.simps list.set_intros(1) list.simps(8) list.simps(9) rder.simps(4) rrexp.distinct(25) rrexp.inject(3)) |
|
1691 using created_by_seq.intros(1) by force |
|
1692 |
|
1693 lemma createdbyseq_left_creatable: |
|
1694 shows "created_by_seq (RALT r1 r2) \<Longrightarrow> created_by_seq r1" |
|
1695 using created_by_seq.cases by blast |
|
1696 |
|
1697 |
|
1698 |
|
1699 lemma recursively_derseq: |
|
1700 shows " created_by_seq (rders (RSEQ r1 r2) s)" |
|
1701 apply(induct s rule: rev_induct) |
|
1702 apply simp |
|
1703 using created_by_seq.intros(1) apply force |
|
1704 apply(subgoal_tac "created_by_seq (rders (RSEQ r1 r2) (xs @ [x]))") |
|
1705 apply blast |
|
1706 apply(subst rders_append) |
|
1707 apply(subgoal_tac "\<exists>r3 r4. rders (RSEQ r1 r2) xs = RSEQ r3 r4 \<or> |
|
1708 rders (RSEQ r1 r2) xs = RALT r3 r4") |
|
1709 prefer 2 |
|
1710 using seq_ders_shape1 apply presburger |
|
1711 apply(erule exE)+ |
|
1712 apply(erule disjE) |
|
1713 apply(subgoal_tac "created_by_seq (rders (RSEQ r3 r4) [x])") |
|
1714 apply presburger |
|
1715 apply simp |
|
1716 using created_by_seq.intros(1) created_by_seq.intros(2) apply presburger |
|
1717 apply simp |
|
1718 apply(subgoal_tac "created_by_seq r3") |
|
1719 prefer 2 |
|
1720 using createdbyseq_left_creatable apply blast |
|
1721 using created_by_seq.intros(2) created_by_seq_der by blast |
|
1722 |
|
1723 |
|
1724 lemma recursively_derseq1: |
|
1725 shows "r = rders (RSEQ r1 r2) s \<Longrightarrow> created_by_seq r" |
|
1726 using recursively_derseq by blast |
|
1727 |
|
1728 lemma recursively_derseq2: |
|
1729 shows "r = rders (RSEQ r1 r2) s \<Longrightarrow> \<exists>r1 r2. r = RSEQ r1 r2 \<or> (r = RALT r1 r2 \<and> created_by_seq r1) " |
|
1730 by (meson created_by_seq.cases recursively_derseq) |
|
1731 |
|
1732 lemma recursively_derseq3: |
|
1733 shows "created_by_seq r \<Longrightarrow> \<exists>r1 r2. r = RSEQ r1 r2 \<or> (r = RALT r1 r2 \<and> created_by_seq r1) " |
|
1734 by (meson created_by_seq.cases recursively_derseq) |
|
1735 |
|
1736 lemma createdbyseq_prop1: |
|
1737 shows "created_by_seq (RALTS xs) \<Longrightarrow> \<exists> ra rb. xs = [ra, rb]" |
|
1738 by (metis created_by_seq.cases rrexp.inject(3) rrexp.simps(30)) |
|
1739 |
|
1740 |
|
1741 lemma sfau_head: |
|
1742 shows " created_by_seq r \<Longrightarrow> \<exists>ra rb rs. sflat_aux r = RSEQ ra rb # rs" |
|
1743 apply(induction r rule: created_by_seq.induct) |
|
1744 apply simp |
|
1745 by fastforce |
|
1746 |
|
1747 |
|
1748 |
|
1749 |
|
1750 lemma sfaux_eq10: |
|
1751 shows "created_by_seq r3 \<Longrightarrow> |
|
1752 rs \<noteq> [] \<Longrightarrow> sflat (RALTS ((map (rder c) (sflat_aux r3)) @ (map (rder c) rs))) = |
|
1753 RALTS (sflat_aux (rder c r3) @ (map (rder c ) rs) )" |
|
1754 apply(induction r3 arbitrary: rs rule: created_by_seq.induct) |
|
1755 apply simp |
|
1756 apply(case_tac "rnullable r1") |
|
1757 apply simp |
|
1758 |
|
1759 apply (metis append_Cons list.exhaust map_is_Nil_conv self_append_conv2 sflat.simps(2) sflat_aux.simps(1) sflat_aux.simps(6)) |
|
1760 apply simp |
|
1761 |
|
1762 apply (metis Nil_is_map_conv append_Cons append_Nil list.exhaust sflat.simps(2) sflat_aux.simps(6)) |
|
1763 apply simp |
|
1764 by force |
|
1765 |
|
1766 lemma sfaux_keeps_tail: |
|
1767 shows "created_by_seq r3 \<Longrightarrow> |
|
1768 sflat_aux (RALTS (map (rder c) (sflat_aux r3) @ xs )) = |
|
1769 sflat_aux (RALTS (map (rder c) (sflat_aux r3))) @ xs " |
|
1770 using sfau_head by fastforce |
|
1771 |
|
1772 |
|
1773 |
|
1774 |
|
1775 lemma sfaux_eq00: |
|
1776 shows "created_by_seq r3 \<Longrightarrow> |
|
1777 sflat_aux (RALTS ((map (rder c) (sflat_aux r3)) @ (map (rder c) rs))) = |
|
1778 (sflat_aux (rder c r3) @ (map (rder c ) rs) )" |
|
1779 apply(induct rs rule: rev_induct) |
|
1780 apply simp |
|
1781 apply (smt (verit, del_insts) append_Cons created_by_seq.simps list.distinct(1) list.simps(9) map_append rder.simps(4) rrexp.inject(3) self_append_conv self_append_conv2 sfau_head sfaux_eq10 sflat_aux.simps(1) sflat_aux.simps(6)) |
|
1782 apply simp |
|
1783 apply(subst sfaux_keeps_tail) |
|
1784 apply simp |
|
1785 apply(subst (asm) sfaux_keeps_tail) |
|
1786 apply simp+ |
|
1787 done |
|
1788 |
|
1789 |
|
1790 lemma sfaux_eq1: |
|
1791 shows "created_by_seq r3 \<Longrightarrow> sflat (RALTS ((map (rder c) (sflat_aux r3)) @ [rder c r4])) = RALTS (sflat_aux (rder c r3) @ [rder c r4] )" |
|
1792 by (metis (no_types, lifting) list.distinct(1) list.simps(9) map_append map_concat_cons self_append_conv sfaux_eq10) |
|
1793 |
|
1794 lemma sflat_seq_induct: |
|
1795 shows "sflat (rder c (sflat (rders (RSEQ r1 r2) s) )) = sflat (rders (RSEQ r1 r2) (s @ [c]))" |
|
1796 apply(subst rders_append) |
|
1797 apply(case_tac "rders (RSEQ r1 r2) s ") |
|
1798 prefer 6 |
|
1799 apply simp+ |
|
1800 apply(subgoal_tac "\<exists>r3 r4. x5 = [r3, r4]") |
|
1801 apply(erule exE)+ |
|
1802 apply(subgoal_tac "sflat (rder c (sflat (RALT r3 r4))) = sflat (RALTS (map (rder c) [r3, r4]))") |
|
1803 apply meson |
|
1804 apply simp |
|
1805 |
|
1806 apply (metis createdbyseq_left_creatable recursively_derseq sfaux_eq1) |
|
1807 by (metis created_by_seq.simps recursively_derseq rrexp.distinct(25) rrexp.inject(3)) |
1648 |
1808 |
1649 |
1809 |
1650 |
1810 |
1651 lemma seq_sflat0: |
1811 lemma seq_sflat0: |
1652 shows "sflat (rders (RSEQ r1 r2) s) = sflat (RALTS ( (RSEQ (rders r1 s) r2) # |
1812 shows "sflat (rders (RSEQ r1 r2) s) = sflat (RALTS ( (RSEQ (rders r1 s) r2) # |
1653 (map (rders r2) (vsuf s r1))) )" |
1813 (map (rders r2) (vsuf s r1))) )" |
1654 apply(induct s rule: rev_induct) |
1814 apply(induct s rule: rev_induct) |
1655 apply simp |
1815 apply simp |
1656 apply(subst rders_append) |
1816 apply(subst rders_append)+ |
|
1817 |
1657 sorry |
1818 sorry |
1658 |
1819 |
1659 lemma seq_sflat1: |
1820 lemma vsuf_prop1: |
1660 shows "sflat ( RALTS ( (RSEQ (rders r1 (s @ [c])) r2) # |
1821 shows "vsuf (xs @ [x]) r = (if (rnullable (rders r xs)) |
1661 (map (rders r2) (vsuf (s @ [c]) r1)) |
1822 then [x] # (map (\<lambda>s. s @ [x]) (vsuf xs r) ) |
1662 ) ) = sflat (rders (RSEQ r1 r2) (s @ [c]))" |
1823 else (map (\<lambda>s. s @ [x]) (vsuf xs r)) ) |
1663 sorry |
1824 " |
1664 |
1825 apply(induct xs arbitrary: r) |
1665 |
1826 apply simp |
1666 lemma seq_sflat: |
1827 apply(case_tac "rnullable r") |
1667 shows "sflat ( RALTS ( (RSEQ (rders r1 (s @ [c])) r2) # |
1828 apply simp |
1668 (map (rders r2) (vsuf (s @ [c]) r1)) |
1829 apply simp |
1669 ) ) = sflat ( rder x (RALTS ( (RSEQ (rders r1 s) r2) # |
1830 done |
1670 (map (rders r2) (vsuf s r1)) |
1831 |
1671 )) )" |
1832 fun breakHead :: "rrexp list \<Rightarrow> rrexp list" where |
1672 sorry |
1833 "breakHead [] = [] " |
1673 |
1834 | "breakHead (RALT r1 r2 # rs) = r1 # r2 # rs" |
1674 lemma sflat_elemnum: |
1835 | "breakHead (r # rs) = r # rs" |
1675 shows "sflat (RALTS [a1, a2, a3]) = [a1, a2, a3]" |
1836 |
1676 sorry |
1837 |
1677 |
1838 lemma sfau_idem_der: |
1678 lemma sflat_emptyalts: |
1839 shows "created_by_seq r \<Longrightarrow> sflat_aux (rder c r) = breakHead (map (rder c) (sflat_aux r))" |
1679 shows "sflat (RALTS xs) = [] \<Longrightarrow> xs = []" |
1840 apply(induct rule: created_by_seq.induct) |
1680 using sflat.elims by auto |
1841 apply simp+ |
1681 |
1842 using sfau_head by fastforce |
1682 lemma ralt_sflat_gte2: |
1843 |
1683 shows "\<exists>ra rb rsc. sflat (RALT r1 r2) = ra # rb # rsc" |
1844 lemma vsuf_compose1: |
1684 apply(case_tac r1) |
1845 shows " \<not> rnullable (rders r1 xs) |
1685 apply simp+ |
1846 \<Longrightarrow> map (rder x \<circ> rders r2) (vsuf xs r1) = map (rders r2) (vsuf (xs @ [x]) r1)" |
1686 |
1847 apply(subst vsuf_prop1) |
1687 oops |
1848 apply simp |
1688 |
1849 by (simp add: rders_append) |
1689 lemma sflat_singleton: |
1850 |
1690 shows "sflat (RALTS xs) = [a] \<Longrightarrow> xs = [a]" |
1851 |
1691 apply(case_tac xs) |
1852 |
1692 apply simp |
1853 |
1693 apply(case_tac list) |
1854 lemma seq_sfau0: |
1694 apply simp |
1855 shows "sflat_aux (rders (RSEQ r1 r2) s) = (RSEQ (rders r1 s) r2) # |
1695 apply simp |
1856 (map (rders r2) (vsuf s r1)) " |
1696 oops |
1857 apply(induct s rule: rev_induct) |
|
1858 apply simp |
|
1859 apply(subst rders_append)+ |
|
1860 apply(subgoal_tac "created_by_seq (rders (RSEQ r1 r2) xs)") |
|
1861 prefer 2 |
|
1862 using recursively_derseq1 apply blast |
|
1863 apply simp |
|
1864 apply(subst sfau_idem_der) |
|
1865 |
|
1866 apply blast |
|
1867 apply(case_tac "rnullable (rders r1 xs)") |
|
1868 apply simp |
|
1869 apply(subst vsuf_prop1) |
|
1870 apply simp |
|
1871 apply (simp add: rders_append) |
|
1872 apply simp |
|
1873 using vsuf_compose1 by blast |
|
1874 |
|
1875 |
|
1876 |
|
1877 |
|
1878 |
|
1879 |
|
1880 |
|
1881 |
1697 |
1882 |
1698 thm sflat.elims |
1883 thm sflat.elims |
1699 |
1884 |
1700 |
1885 |
1701 lemma sflat_ralts: |
|
1702 shows "sflat (RALTS xs) = sflat (RALTS xs') |
|
1703 \<Longrightarrow> rsimp (RALTS xs) = rsimp (RALTS xs')" |
|
1704 apply(induct xs) |
|
1705 |
|
1706 apply(case_tac xs) |
|
1707 apply simp |
|
1708 apply (metis list.simps(8) rdistinct.simps(1) rflts.simps(1) rsimp_ALTs.simps(1) sflat_emptyalts) |
|
1709 apply(case_tac list) |
|
1710 apply simp |
|
1711 apply |
|
1712 sledgehammer |
|
1713 |
|
1714 |
1886 |
1715 |
1887 |
1716 |
1888 |
1717 lemma sflat_rsimpeq: |
1889 lemma sflat_rsimpeq: |
1718 shows "sflat r1 = sflat r2 \<Longrightarrow> rsimp r1 = rsimp r2" |
1890 shows "sflat_aux r1 = sflat_aux r2 \<Longrightarrow> rsimp r1 = rsimp r2" |
1719 apply(cases r1 ) |
1891 apply(cases r1 ) |
1720 apply(cases r2) |
1892 apply(cases r2) |
1721 apply simp+ |
1893 apply simp+ |
1722 apply(case_tac x5) |
1894 apply(case_tac x5) |
1723 apply simp |
1895 apply simp |
1724 apply(case_tac list) |
1896 apply(case_tac list) |
1725 apply simp |
1897 apply simp |
1726 apply(case_tac lista) |
1898 |
1727 apply simp |
|
1728 |
1899 |
1729 |
1900 |
1730 sorry |
1901 sorry |
1731 |
1902 |
1732 |
1903 |
1733 |
1904 |
1734 lemma seq_closed_form_general: |
1905 lemma seq_closed_form_general: |
1735 shows "rsimp (rders (RSEQ r1 r2) s) = |
1906 shows "rsimp (rders (RSEQ r1 r2) s) = |
1736 rsimp ( (RALTS ( (RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1))))))" |
1907 rsimp ( (RALTS ( (RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1))))))" |
1737 apply(subgoal_tac "sflat (rders (RSEQ r1 r2) s) = sflat (RALTS ( (RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1)))))") |
1908 apply(case_tac "s \<noteq> []") |
|
1909 apply(subgoal_tac "sflat_aux (rders (RSEQ r1 r2) s) = sflat_aux (RALTS ( (RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1)))))") |
1738 using sflat_rsimpeq apply blast |
1910 using sflat_rsimpeq apply blast |
1739 by (simp add: seq_sflat0) |
1911 using seq_sfau0 apply blast |
1740 |
1912 apply simp |
|
1913 by (metis idem_after_simp1 rsimp.simps(1)) |
|
1914 |
|
1915 |
1741 lemma seq_closed_form_aux1: |
1916 lemma seq_closed_form_aux1: |
1742 shows "rsimp ( (RALTS ( (RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1)))))) = |
1917 shows "rsimp ( (RALTS ( (RSEQ (rders r1 s) r2 # (map (rders r2) (vsuf s r1)))))) = |
1743 rsimp ( (RALTS ( (RSEQ (rders_simp r1 s) r2 # (map (rders r2) (vsuf s r1))))))" |
1918 rsimp ( (RALTS ( (RSEQ (rders_simp r1 s) r2 # (map (rders r2) (vsuf s r1))))))" |
1744 by (smt (verit, best) list.simps(9) rders.simps(1) rders_simp.simps(1) rders_simp_same_simpders rsimp.simps(1) rsimp.simps(2) rsimp_idem) |
1919 by (smt (verit, best) list.simps(9) rders.simps(1) rders_simp.simps(1) rders_simp_same_simpders rsimp.simps(1) rsimp.simps(2) rsimp_idem) |
1745 |
1920 |