1891 shows "s \<noteq> [] \<Longrightarrow> 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") |
1892 apply(case_tac "s") |
1893 apply simp |
1893 apply simp |
1894 apply simp |
1894 apply simp |
1895 sorry |
1895 sorry |
|
1896 (* |
|
1897 fun rexp_encode :: "rrexp \<Rightarrow> nat" |
|
1898 where |
|
1899 "rexp_encode RZERO = 0" |
|
1900 |"rexp_encode RONE = 1" |
|
1901 |"rexp_encode (RCHAR c) = 2" |
|
1902 |"rexp_encode (RSEQ r1 r2) = ( 2 ^ (rexp_encode r1)) " |
|
1903 *) |
|
1904 lemma finite_chars: |
|
1905 shows " \<exists>N. ( (\<forall>r \<in> (set rs). \<exists>c. r = RCHAR c) \<and> (distinct rs) \<longrightarrow> length rs < N)" |
|
1906 apply(rule_tac x = "Suc 256" in exI) |
|
1907 sorry |
|
1908 |
|
1909 fun all_chars :: "nat \<Rightarrow> char list" |
|
1910 where |
|
1911 "all_chars 0 = [CHR 0x00]" |
|
1912 |"all_chars (Suc i) = (char_of (Suc i)) # (all_chars i)" |
|
1913 |
|
1914 |
|
1915 fun rexp_enum :: "nat \<Rightarrow> rrexp list" |
|
1916 where |
|
1917 "rexp_enum 0 = []" |
|
1918 |"rexp_enum 1 = RZERO # (RONE # (map RCHAR (all_chars 255)))" |
|
1919 |
|
1920 lemma finite_sized_rexp_forms_finite_set: |
|
1921 shows " \<exists>SN. ( \<forall>r.( rsize r < N \<longrightarrow> r \<in> SN)) \<and> (finite SN)" |
|
1922 apply(induct N) |
|
1923 apply simp |
|
1924 apply auto |
|
1925 (*\<lbrakk>\<forall>r. rsize r < N \<longrightarrow> r \<in> SN; finite SN\<rbrakk> \<Longrightarrow> \<exists>SN. (\<forall>r. rsize r < Suc N \<longrightarrow> r \<in> SN) \<and> finite SN*) |
|
1926 (* \<And>N. \<exists>SN. (\<forall>r. rsize r < N \<longrightarrow> r \<in> SN) \<and> finite SN \<Longrightarrow> \<exists>SN. (\<forall>r. rsize r < Suc N \<longrightarrow> r \<in> SN) \<and> finite SN*) |
|
1927 sorry |
1896 |
1928 |
1897 |
1929 |
1898 lemma finite_size_finite_regx: |
1930 lemma finite_size_finite_regx: |
1899 shows "\<forall>N. \<exists>l. (\<forall>r \<in> (set rs). rsize r < N) \<and> (distinct rs) \<Longrightarrow> (length rs) < l " |
1931 shows " \<exists>l. \<forall>rs. ((\<forall>r \<in> (set rs). rsize r < N) \<and> (distinct rs) \<longrightarrow> (length rs) < l) " |
1900 sorry |
1932 apply(frule finite_sized_rexp_forms_finite_set) |
1901 |
1933 |
1902 |
1934 |
1903 (*below probably needs proved concurrently*) |
1935 (*below probably needs proved concurrently*) |
1904 |
1936 |
1905 lemma finite_r1r2_ders_list: |
1937 lemma finite_r1r2_ders_list: |
1976 sorry |
2008 sorry |
1977 |
2009 |
1978 lemma star_seqs_produce_star_seqs: |
2010 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)) |
2011 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))" |
2012 = rsimp (rsimp_ALTs (map ( (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r)))) Ss))" |
1981 sledgehammer |
|
1982 by (meson comp_apply) |
2013 by (meson comp_apply) |
1983 |
2014 |
1984 lemma der_seqstar_res: |
2015 lemma der_seqstar_res: |
1985 shows "rder x " |
2016 shows "rder x (RSEQ r1 r2) = RSEQ r3 r4" |
1986 |
2017 |
1987 |
2018 |
1988 lemma linearity_of_list_of_star_or_starseqs: |
2019 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))) = |
2020 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)" |
2021 rsimp_ALTs (map (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r)) Ssa)" |
1991 apply(simp add: rder_rsimp_ALTs_commute) |
2022 apply(simp add: rder_rsimp_ALTs_commute) |
1992 apply(induct Ss) |
2023 apply(induct Ss) |
1993 apply simp |
2024 apply simp |
1994 apply (metis list.simps(8) rsimp_ALTs.simps(1)) |
2025 apply (metis list.simps(8) rsimp_ALTs.simps(1)) |
1995 |
2026 |
1996 sledgehammer |
2027 |
1997 sorry |
2028 sorry |
1998 |
2029 |
1999 lemma starder_is_a_list_of_stars_or_starseqs: |
2030 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)" |
2031 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) |
2032 apply(induct s rule: rev_induct) |