1721 fun nullable_bools :: "rrexp \<Rightarrow> char list list \<Rightarrow> bool list" |
1724 fun nullable_bools :: "rrexp \<Rightarrow> char list list \<Rightarrow> bool list" |
1722 where |
1725 where |
1723 "nullable_bools r (s#strs) = (rnullable (rders r s)) # (nullable_bools r strs) " |
1726 "nullable_bools r (s#strs) = (rnullable (rders r s)) # (nullable_bools r strs) " |
1724 |"nullable_bools r [] = []" |
1727 |"nullable_bools r [] = []" |
1725 |
1728 |
|
1729 thm rsimp_SEQ.simps |
|
1730 |
|
1731 lemma idiot: |
|
1732 shows "rsimp_SEQ RONE r = r" |
|
1733 apply(case_tac r) |
|
1734 apply simp_all |
|
1735 done |
|
1736 |
|
1737 lemma no_dup_after_simp: |
|
1738 shows "RALTS rs = rsimp r \<Longrightarrow> distinct rs" |
|
1739 sorry |
|
1740 |
|
1741 lemma no_further_dB_after_simp: |
|
1742 shows "RALTS rs = rsimp r \<Longrightarrow> rdistinct rs {} = rs" |
|
1743 sorry |
|
1744 |
|
1745 lemma longlist_withstands_rsimp_alts: |
|
1746 shows "length rs \<ge> 2 \<Longrightarrow> rsimp_ALTs rs = RALTS rs" |
|
1747 sorry |
|
1748 |
|
1749 lemma no_alt_short_list_after_simp: |
|
1750 shows "RALTS rs = rsimp r \<Longrightarrow> rsimp_ALTs rs = RALTS rs" |
|
1751 sorry |
|
1752 |
|
1753 lemma idiot2: |
|
1754 shows " \<lbrakk>r1 \<noteq> RZERO; r1 \<noteq> RONE;r2 \<noteq> RZERO\<rbrakk> |
|
1755 \<Longrightarrow> rsimp_SEQ r1 r2 = RSEQ r1 r2" |
|
1756 apply(case_tac r1) |
|
1757 apply(case_tac r2) |
|
1758 apply simp_all |
|
1759 apply(case_tac r2) |
|
1760 apply simp_all |
|
1761 apply(case_tac r2) |
|
1762 apply simp_all |
|
1763 apply(case_tac r2) |
|
1764 apply simp_all |
|
1765 apply(case_tac r2) |
|
1766 apply simp_all |
|
1767 done |
|
1768 |
|
1769 lemma rsimp_aalts_another: |
|
1770 shows "\<forall>r \<in> (set (map rsimp ((RSEQ (rders r1 s) r2) # |
|
1771 (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s)) )) ). (rsize r) < N " |
|
1772 sorry |
|
1773 |
|
1774 |
|
1775 |
|
1776 lemma shape_derssimpseq_onechar: |
|
1777 shows " rerase (bders_simp r [c]) = rerase (bsimp (bders r [c]))" |
|
1778 and "rders_simp (RSEQ r1 r2) [c] = |
|
1779 rsimp (RALTS ((RSEQ (rders r1 [c]) r2) # |
|
1780 (rders_cond_list r2 (nullable_bools r1 (orderedPref [c])) (orderedSuf [c]))) )" |
|
1781 apply simp |
|
1782 apply(simp add: rders.simps) |
|
1783 apply(case_tac "rsimp (rder c r1) = RZERO") |
|
1784 apply auto |
|
1785 apply(case_tac "rsimp (rder c r1) = RONE") |
|
1786 apply auto |
|
1787 apply(subgoal_tac "rsimp_SEQ RONE (rsimp r2) = rsimp r2") |
|
1788 prefer 2 |
|
1789 using idiot |
|
1790 apply simp |
|
1791 apply(subgoal_tac "rsimp_SEQ RONE (rsimp r2) = rsimp_ALTs (rdistinct (rflts [rsimp r2]) {})") |
|
1792 prefer 2 |
|
1793 apply auto |
|
1794 apply(case_tac "rsimp r2") |
|
1795 apply auto |
|
1796 apply(subgoal_tac "rdistinct x5 {} = x5") |
|
1797 prefer 2 |
|
1798 using no_further_dB_after_simp |
|
1799 apply metis |
|
1800 apply(subgoal_tac "rsimp_ALTs (rdistinct x5 {}) = rsimp_ALTs x5") |
|
1801 prefer 2 |
|
1802 apply fastforce |
|
1803 apply auto |
|
1804 apply (metis no_alt_short_list_after_simp) |
|
1805 apply (case_tac "rsimp r2 = RZERO") |
|
1806 apply(subgoal_tac "rsimp_SEQ (rsimp (rder c r1)) (rsimp r2) = RZERO") |
|
1807 prefer 2 |
|
1808 apply(case_tac "rsimp ( rder c r1)") |
|
1809 apply auto |
|
1810 apply(subgoal_tac "rsimp_SEQ (rsimp (rder c r1)) (rsimp r2) = RSEQ (rsimp (rder c r1)) (rsimp r2)") |
|
1811 prefer 2 |
|
1812 apply auto |
|
1813 apply(metis idiot2) |
|
1814 done |
|
1815 |
|
1816 lemma rders__onechar: |
|
1817 shows " (rders_simp r [c]) = (rsimp (rders r [c]))" |
|
1818 by simp |
|
1819 |
|
1820 lemma rders_append: |
|
1821 "rders c (s1 @ s2) = rders (rders c s1) s2" |
|
1822 apply(induct s1 arbitrary: c s2) |
|
1823 apply(simp_all) |
|
1824 done |
|
1825 |
|
1826 lemma rders_simp_append: |
|
1827 "rders_simp c (s1 @ s2) = rders_simp (rders_simp c s1) s2" |
|
1828 apply(induct s1 arbitrary: c s2) |
|
1829 apply(simp_all) |
|
1830 done |
|
1831 |
|
1832 lemma inside_simp_removal: |
|
1833 shows " rsimp (rder x (rsimp r)) = rsimp (rder x r)" |
1726 |
1834 |
|
1835 sorry |
|
1836 |
|
1837 lemma set_related_list: |
|
1838 shows "distinct rs \<Longrightarrow> length rs = card (set rs)" |
|
1839 by (simp add: distinct_card) |
|
1840 (*this section deals with the property of distinctBy: creates a list without duplicates*) |
|
1841 lemma rdistinct_never_added_twice: |
|
1842 shows "rdistinct (a # rs) {a} = rdistinct rs {a}" |
|
1843 by force |
|
1844 |
|
1845 |
|
1846 lemma rdistinct_does_the_job: |
|
1847 shows "distinct (rdistinct rs s)" |
|
1848 apply(induct rs arbitrary: s) |
|
1849 apply simp |
|
1850 apply simp |
|
1851 sorry |
|
1852 |
|
1853 |
|
1854 |
|
1855 |
|
1856 (*this section deals with the property of distinctBy: creates a list without duplicates*) |
|
1857 |
|
1858 lemma rders_simp_same_simpders: |
|
1859 shows "s \<noteq> [] \<Longrightarrow> rders_simp r s = rsimp (rders r s)" |
|
1860 apply(induct s rule: rev_induct) |
|
1861 apply simp |
|
1862 apply(case_tac "xs = []") |
|
1863 apply simp |
|
1864 apply(simp add: rders_append rders_simp_append) |
|
1865 using inside_simp_removal by blast |
|
1866 |
1727 lemma shape_derssimp_seq: |
1867 lemma shape_derssimp_seq: |
1728 shows "\<lbrakk>s \<noteq>[] \<rbrakk> \<Longrightarrow> rerase (bders_simp r s) = rerase (bsimp (bders r s))" |
1868 shows "\<lbrakk>s \<noteq>[] \<rbrakk> \<Longrightarrow> (rders_simp r s) = (rsimp (rders r s))" |
1729 and "\<lbrakk>s \<noteq> []\<rbrakk> \<Longrightarrow> rders_simp (RSEQ r1 r2) s = |
1869 and "\<lbrakk>s \<noteq> []\<rbrakk> \<Longrightarrow> rders_simp (RSEQ r1 r2) s = |
1730 rsimp (RALTS ((RSEQ (rders r1 s) r2) # |
1870 rsimp (RALTS ((RSEQ (rders r1 s) r2) # |
1731 (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s))) )" |
1871 (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s))) )" |
1732 apply(induct s arbitrary: r r1 r2 rule: rev_induct) |
1872 apply(induct s arbitrary: r r1 r2 rule: rev_induct) |
1733 apply simp |
1873 apply simp |
1740 apply (simp add: rerase_bsimp) |
1880 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))))") |
1881 apply(subgoal_tac "(rsimp (rerase (bder x (bders_simp r xs)))) = (rsimp (rder x (rerase (bders_simp r xs))))") |
1742 |
1882 |
1743 apply(subgoal_tac "xs \<noteq> [] \<Longrightarrow> rsimp (rder x (rerase (bders_simp r xs))) = rsimp (rder x (rerase (bsimp (bders r xs))))") |
1883 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 |
1884 prefer 2 |
1745 apply presburger |
1885 apply presburger |
1746 sorry |
1886 apply(case_tac "xs = []") |
|
1887 sorry |
|
1888 |
1747 |
1889 |
1748 lemma shape_derssimp_alts: |
1890 lemma shape_derssimp_alts: |
1749 shows "rders_simp (RALTS rs) s = rsimp (RALTS (map (\<lambda>r. rders r s) rs))" |
1891 shows "s \<noteq> [] \<Longrightarrow> rders_simp (RALTS rs) s = rsimp (RALTS (map (\<lambda>r. rders r s) rs))" |
|
1892 apply(case_tac "s") |
|
1893 apply simp |
|
1894 apply simp |
|
1895 sorry |
1750 |
1896 |
1751 |
1897 |
1752 lemma finite_size_finite_regx: |
1898 lemma finite_size_finite_regx: |
1753 shows "\<forall>N. \<exists>l. (\<forall>r \<in> (set rs). rsize r < N) \<and> (distinct rs) \<Longrightarrow> (length rs) < l " |
1899 shows "\<forall>N. \<exists>l. (\<forall>r \<in> (set rs). rsize r < N) \<and> (distinct rs) \<Longrightarrow> (length rs) < l " |
1754 sorry |
1900 sorry |
1755 |
1901 |
1756 |
1902 |
1757 (*below probably needs proved concurrently*) |
1903 (*below probably needs proved concurrently*) |
1758 |
1904 |
1759 lemma finite_r1r2_ders_list: |
1905 lemma finite_r1r2_ders_list: |
1760 shows "\<forall>r1 r2. \<exists>l. |
1906 shows "(\<forall>s. rsize (rders_simp r1 s) < N1 \<and> rsize (rders_simp r2 s) < N2) |
1761 (length (rdistinct (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s)) {})) < l " |
1907 \<Longrightarrow> \<exists>l. \<forall>s. |
1762 sorry |
1908 (length (rdistinct (map rsimp (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s))) {}) ) < l " |
|
1909 sorry |
|
1910 |
|
1911 (* |
|
1912 \<lbrakk>s \<noteq> []\<rbrakk> \<Longrightarrow> rders_simp (RSEQ r1 r2) s = |
|
1913 rsimp (RALTS ((RSEQ (rders r1 s) r2) # |
|
1914 (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s))) ) |
|
1915 *) |
|
1916 |
|
1917 lemma finite_width_alt: |
|
1918 shows "(\<forall>s. rsize (rders_simp r1 s) < N1 \<and> rsize (rders_simp r2 s) < N2) |
|
1919 \<Longrightarrow> \<exists>N3. \<forall>s. rsize (rsimp (RALTS ((RSEQ (rders r1 s) r2) # |
|
1920 (rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s))) )) < N3" |
|
1921 |
|
1922 sorry |
|
1923 |
|
1924 |
|
1925 lemma empty_diff: |
|
1926 shows "s = [] \<Longrightarrow> |
|
1927 (rsize (rders_simp (RSEQ r1 r2) s)) \<le> |
|
1928 (max |
|
1929 (rsize (rsimp (RALTS (RSEQ (rders r1 s) r2 # rders_cond_list r2 (nullable_bools r1 (orderedPref s)) (orderedSuf s))))) |
|
1930 (Suc (rsize r1 + rsize r2)) ) " |
|
1931 apply simp |
|
1932 done |
1763 |
1933 |
1764 lemma finite_seq: |
1934 lemma finite_seq: |
1765 shows "(\<forall>s. rsize (rders_simp r1 s) < N1 \<and> rsize (rders_simp r2 s) < N2) |
1935 shows "(\<forall>s. rsize (rders_simp r1 s) < N1 \<and> rsize (rders_simp r2 s) < N2) |
1766 \<Longrightarrow> \<exists>N3.\<forall>s.(rsize (rders_simp (RSEQ r1 r2) s)) < N3" |
1936 \<Longrightarrow> \<exists>N3.\<forall>s.(rsize (rders_simp (RSEQ r1 r2) s)) < N3" |
1767 sorry |
1937 apply(frule finite_width_alt) |
|
1938 apply(erule exE) |
|
1939 apply(rule_tac x = "max (N3+2) (Suc (Suc (rsize r1) + (rsize r2)))" in exI) |
|
1940 apply(rule allI) |
|
1941 apply(case_tac "s = []") |
|
1942 prefer 2 |
|
1943 apply (simp add: less_SucI shape_derssimp_seq(2)) |
|
1944 apply (meson less_SucI less_max_iff_disj) |
|
1945 apply simp |
|
1946 done |
|
1947 |
|
1948 |
|
1949 (*For star related error bound*) |
|
1950 |
|
1951 lemma star_is_a_singleton_list_derc: |
|
1952 shows " \<exists>Ss. rders_simp (RSTAR r) [c] = rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss)" |
|
1953 apply simp |
|
1954 apply(rule_tac x = "[[c]]" in exI) |
|
1955 apply auto |
|
1956 done |
|
1957 |
|
1958 lemma rder_rsimp_ALTs_commute: |
|
1959 shows " (rder x (rsimp_ALTs rs)) = rsimp_ALTs (map (rder x) rs)" |
|
1960 apply(induct rs) |
|
1961 apply simp |
|
1962 apply(case_tac rs) |
|
1963 apply simp |
|
1964 apply auto |
|
1965 done |
|
1966 |
|
1967 lemma double_nested_ALTs_under_rsimp: |
|
1968 shows "rsimp (rsimp_ALTs ((RALTS rs1) # rs)) = rsimp (RALTS (rs1 @ rs))" |
|
1969 apply(case_tac rs1) |
|
1970 apply simp |
|
1971 |
|
1972 apply (metis list.simps(8) list.simps(9) neq_Nil_conv rdistinct.simps(1) rflts.simps(1) rflts.simps(2) rsimp.simps(2) rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3)) |
|
1973 apply(case_tac rs) |
|
1974 apply simp |
|
1975 apply auto |
|
1976 sorry |
|
1977 |
|
1978 lemma star_seqs_produce_star_seqs: |
|
1979 shows "rsimp (rsimp_ALTs (map (rder x \<circ> (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss)) |
|
1980 = rsimp (rsimp_ALTs (map ( (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r)))) Ss))" |
|
1981 sledgehammer |
|
1982 by (meson comp_apply) |
|
1983 |
|
1984 lemma der_seqstar_res: |
|
1985 shows "rder x " |
|
1986 |
|
1987 |
|
1988 lemma linearity_of_list_of_star_or_starseqs: |
|
1989 shows "\<exists>Ssa. rsimp (rder x (rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss))) = |
|
1990 rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ssa)" |
|
1991 apply(simp add: rder_rsimp_ALTs_commute) |
|
1992 apply(induct Ss) |
|
1993 apply simp |
|
1994 apply (metis list.simps(8) rsimp_ALTs.simps(1)) |
|
1995 |
|
1996 sledgehammer |
|
1997 sorry |
|
1998 |
|
1999 lemma starder_is_a_list_of_stars_or_starseqs: |
|
2000 shows "s \<noteq> [] \<Longrightarrow> \<exists>Ss. rders_simp (RSTAR r) s = rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ss)" |
|
2001 apply(induct s rule: rev_induct) |
|
2002 apply simp |
|
2003 apply(case_tac "xs = []") |
|
2004 using star_is_a_singleton_list_derc |
|
2005 apply(simp) |
|
2006 apply auto |
|
2007 apply(simp add: rders_simp_append) |
|
2008 using linearity_of_list_of_star_or_starseqs by blast |
1768 |
2009 |
1769 |
2010 |
1770 lemma finite_star: |
2011 lemma finite_star: |
1771 shows "(\<forall>s. rsize (rders_simp r0 s) < N0 ) |
2012 shows "(\<forall>s. rsize (rders_simp r0 s) < N0 ) |
1772 \<Longrightarrow> \<exists>N3. \<forall>s.(rsize (rders_simp (RSTAR r0) s)) < N3" |
2013 \<Longrightarrow> \<exists>N3. \<forall>s.(rsize (rders_simp (RSTAR r0) s)) < N3" |
|
2014 |
1773 sorry |
2015 sorry |
1774 |
2016 |
1775 |
2017 |
1776 lemma rderssimp_zero: |
2018 lemma rderssimp_zero: |
1777 shows"rders_simp RZERO s = RZERO" |
2019 shows"rders_simp RZERO s = RZERO" |