equal
deleted
inserted
replaced
1904 lemma finite_chars: |
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)" |
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) |
1906 apply(rule_tac x = "Suc 256" in exI) |
1907 sorry |
1907 sorry |
1908 |
1908 |
1909 fun all_chars :: "nat \<Rightarrow> char list" |
1909 definition all_chars :: "int \<Rightarrow> char list" |
1910 where |
1910 where "all_chars n = map char_of [0..n]" |
1911 "all_chars 0 = [CHR 0x00]" |
|
1912 |"all_chars (Suc i) = (char_of (Suc i)) # (all_chars i)" |
|
1913 |
|
1914 |
1911 |
1915 fun rexp_enum :: "nat \<Rightarrow> rrexp list" |
1912 fun rexp_enum :: "nat \<Rightarrow> rrexp list" |
1916 where |
1913 where |
1917 "rexp_enum 0 = []" |
1914 "rexp_enum 0 = []" |
1918 |"rexp_enum 1 = RZERO # (RONE # (map RCHAR (all_chars 255)))" |
1915 |"rexp_enum (Suc 0) = RALTS [] # RZERO # (RONE # (map RCHAR (all_chars 255)))" |
|
1916 |"rexp_enum (Suc n) = [(RSEQ r1 r2). r1 \<in> set (rexp_enum i) \<and> r2 \<in> set (rexp_enum j) \<and> i + j = n]" |
|
1917 |
1919 |
1918 |
1920 lemma finite_sized_rexp_forms_finite_set: |
1919 lemma finite_sized_rexp_forms_finite_set: |
1921 shows " \<exists>SN. ( \<forall>r.( rsize r < N \<longrightarrow> r \<in> SN)) \<and> (finite SN)" |
1920 shows " \<exists>SN. ( \<forall>r.( rsize r < N \<longrightarrow> r \<in> SN)) \<and> (finite SN)" |
1922 apply(induct N) |
1921 apply(induct N) |
1923 apply simp |
1922 apply simp |
1927 sorry |
1926 sorry |
1928 |
1927 |
1929 |
1928 |
1930 lemma finite_size_finite_regx: |
1929 lemma finite_size_finite_regx: |
1931 shows " \<exists>l. \<forall>rs. ((\<forall>r \<in> (set rs). rsize r < N) \<and> (distinct rs) \<longrightarrow> (length rs) < l) " |
1930 shows " \<exists>l. \<forall>rs. ((\<forall>r \<in> (set rs). rsize r < N) \<and> (distinct rs) \<longrightarrow> (length rs) < l) " |
1932 apply(frule finite_sized_rexp_forms_finite_set) |
1931 sorry |
1933 |
|
1934 |
1932 |
1935 (*below probably needs proved concurrently*) |
1933 (*below probably needs proved concurrently*) |
1936 |
1934 |
1937 lemma finite_r1r2_ders_list: |
1935 lemma finite_r1r2_ders_list: |
1938 shows "(\<forall>s. rsize (rders_simp r1 s) < N1 \<and> rsize (rders_simp r2 s) < N2) |
1936 shows "(\<forall>s. rsize (rders_simp r1 s) < N1 \<and> rsize (rders_simp r2 s) < N2) |