Mercurial Mercurial > hg > lexing / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys2/SizeBound6CT.thy
changeset 441 426a93160f4a
parent 439 a5376206fd52
child 442 09a57446696a
equal deleted inserted replaced
440:0856fbf8bda7 441:426a93160f4a 
   114   sorry
 
   114   sorry
 
   115 
   115 
   116 
   116 
   117 *)
 
   117 *)
 
   118 
   118 
   119 datatype cchar = 
       
   120 Achar
 
       
   121 |Bchar
 
       
   122 |Cchar
 
       
   123 |Dchar
 
       
   124 
   119 
   125 datatype rrexp = 
   120 datatype rrexp = 
   126   RZERO
 
   121   RZERO
 
   127 | RONE 
   122 | RONE 
   128 | RCHAR cchar
 
   123 | RCHAR char
 
   129 | RSEQ rrexp rrexp
 
   124 | RSEQ rrexp rrexp
 
   130 | RALTS "rrexp list"
 
   125 | RALTS "rrexp list"
 
   131 | RSTAR rrexp
 
   126 | RSTAR rrexp
 
   132 
   127 
   133 abbreviation
 
   128 abbreviation
 
   143 | "rnullable (RCHAR   c) = False"
 
   138 | "rnullable (RCHAR   c) = False"
 
   144 | "rnullable (RALTS   rs) = (\<exists>r \<in> set rs. rnullable r)"
 
   139 | "rnullable (RALTS   rs) = (\<exists>r \<in> set rs. rnullable r)"
 
   145 | "rnullable (RSEQ  r1 r2) = (rnullable r1 \<and> rnullable r2)"
 
   140 | "rnullable (RSEQ  r1 r2) = (rnullable r1 \<and> rnullable r2)"
 
   146 | "rnullable (RSTAR   r) = True"
 
   141 | "rnullable (RSTAR   r) = True"
 
   147 
   142 
   148 fun convert_cchar_char :: "cchar \<Rightarrow> char"
 
       
   149   where
 
       
   150 "convert_cchar_char Achar = (CHR 0x41) "
 
       
   151 | "convert_cchar_char Bchar = (CHR 0x42) "
 
       
   152 | "convert_cchar_char Cchar = (CHR 0x43) "
 
       
   153 | "convert_cchar_char Dchar = (CHR 0x44) "
 
       
   154 
   143 
   155 fun
 
   144 fun
 
   156  rder :: "char \<Rightarrow> rrexp \<Rightarrow> rrexp"
 
   145  rder :: "char \<Rightarrow> rrexp \<Rightarrow> rrexp"
 
   157 where
 
   146 where
 
   158   "rder c (RZERO) = RZERO"
 
   147   "rder c (RZERO) = RZERO"
 
   159 | "rder c (RONE) = RZERO"
 
   148 | "rder c (RONE) = RZERO"
 
   160 | "rder c (RCHAR d) = (if c = (convert_cchar_char d) then RONE else RZERO)"
 
   149 | "rder c (RCHAR d) = (if c = d then RONE else RZERO)"
 
   161 | "rder c (RALTS rs) = RALTS (map (rder c) rs)"
 
   150 | "rder c (RALTS rs) = RALTS (map (rder c) rs)"
 
   162 | "rder c (RSEQ r1 r2) = 
   151 | "rder c (RSEQ r1 r2) = 
   163      (if rnullable r1
 
   152      (if rnullable r1
 
   164       then RALT   (RSEQ (rder c r1) r2) (rder c r2)
 
   153       then RALT   (RSEQ (rder c r1) r2) (rder c r2)
 
   165       else RSEQ   (rder c r1) r2)"
 
   154       else RSEQ   (rder c r1) r2)"
 
   877 "rexp_enum 0 = []"
 
   866 "rexp_enum 0 = []"
 
   878 |"rexp_enum (Suc 0) =  RALTS [] # RZERO # (RONE # (map RCHAR (all_chars 255)))"
 
   867 |"rexp_enum (Suc 0) =  RALTS [] # RZERO # (RONE # (map RCHAR (all_chars 255)))"
 
   879 |"rexp_enum (Suc n) = [(RSEQ r1 r2). r1 \<in> set (rexp_enum i) \<and> r2 \<in> set (rexp_enum j) \<and> i + j = n]"
 
   868 |"rexp_enum (Suc n) = [(RSEQ r1 r2). r1 \<in> set (rexp_enum i) \<and> r2 \<in> set (rexp_enum j) \<and> i + j = n]"
 
   880 
   869 
   881 *)
 
   870 *)
 
       
   871 definition SEQ_set where
 
       
   872   "SEQ_set A n \<equiv> {RSEQ r1 r2 | r1 r2. r1 \<in> A \<and> r2 \<in> A \<and> rsize r1 + rsize r2 \<le> n}"
 
       
   873 
       
   874 definition ALT_set where
 
       
   875 "ALT_set A n \<equiv> {RALTS rs | rs. set rs \<subseteq> A \<and> sum_list (map rsize rs) \<le> n}"
 
       
   876 
   882 context notes rev_conj_cong[fundef_cong] begin
 
   877 context notes rev_conj_cong[fundef_cong] begin
 
   883 function (sequential) rexp_enum :: "nat \<Rightarrow> rrexp set"
 
   878 function (sequential) rexp_enum :: "nat \<Rightarrow> rrexp set"
 
   884   where 
   879   where 
   885 "rexp_enum 0 = {}"
 
   880 "rexp_enum 0 = {}"
 
   886 |"rexp_enum (Suc 0) =  {RALTS []} \<union> {RZERO} \<union> {RONE} \<union> { (RCHAR c) |c. c \<in>{Achar, Bchar, Cchar, Dchar} }"
 
   881 |"rexp_enum (Suc 0) =  {RALTS []} \<union> {RZERO} \<union> {RONE} \<union> { (RCHAR c) |c::char. True }"
 
   887 |"rexp_enum (Suc n) = {(RSEQ r1 r2)|r1 r2 i j. r1 \<in>  (rexp_enum i) \<and> r2 \<in>  (rexp_enum j) \<and> i + j = n} \<union>
 
   882 |"rexp_enum (Suc n) = {(RSEQ r1 r2)|r1 r2 i j. r1 \<in>  (rexp_enum i) \<and> r2 \<in>  (rexp_enum j) \<and> i + j = n} \<union>
 
   888 {(RALTS (a # rs)) | a rs i j. a \<in> (rexp_enum i) \<and> (RALTS rs) \<in> (rexp_enum j) \<and> i + j = Suc n \<and> i \<le> n \<and> j \<le> n} \<union>
 
   883 {(RALTS (a # rs)) | a rs i j. a \<in> (rexp_enum i) \<and> (RALTS rs) \<in> (rexp_enum j) \<and> i + j = Suc n \<and> i \<le> n \<and> j \<le> n} \<union>
 
   889 {RSTAR r0 | r0. r0 \<in> (rexp_enum n)} \<union>
 
   884 {RSTAR r0 | r0. r0 \<in> (rexp_enum n)} \<union>
 
   890 (rexp_enum n)"
 
   885 (rexp_enum n)"
 
   891   by pat_completeness auto
 
   886   by pat_completeness auto
 
   902 
   897 
   903 lemma rexp_enum_mono:
 
   898 lemma rexp_enum_mono:
 
   904   shows "n \<le> m \<Longrightarrow> (rexp_enum n) \<subseteq> (rexp_enum m)"
 
   899   shows "n \<le> m \<Longrightarrow> (rexp_enum n) \<subseteq> (rexp_enum m)"
 
   905   by (simp add: lift_Suc_mono_le rexp_enum_inclusion)
 
   900   by (simp add: lift_Suc_mono_le rexp_enum_inclusion)
 
   906 
   901 
       
   902 lemma zero_in_Suc0:
 
       
   903   shows "RZERO \<in> rexp_enum (Suc 0)"
 
       
   904 and "RZERO \<in> rexp_enum 1"
 
       
   905   apply simp
 
       
   906   by simp
 
       
   907 
       
   908 lemma one_in_Suc0:
 
       
   909   shows "RONE \<in> rexp_enum (Suc 0)"
 
       
   910 and "RONE \<in> rexp_enum 1"
 
       
   911    apply simp
 
       
   912   by simp
 
       
   913 
       
   914 lemma char_in_Suc0:
 
       
   915   shows "RCHAR c \<in> rexp_enum (Suc 0)"
 
       
   916   apply simp
 
       
   917   done
 
       
   918 
       
   919 
       
   920 lemma char_in1:
 
       
   921   shows "RCHAR c \<in> rexp_enum 1"
 
       
   922   using One_nat_def char_in_Suc0 by presburger
 
       
   923 
       
   924 lemma alts_nil_in_Suc0:
 
       
   925   shows "RALTS [] \<in> rexp_enum (Suc 0)"
 
       
   926   and "RALTS [] \<in> rexp_enum 1"
 
       
   927   apply simp
 
       
   928   by simp
 
       
   929 
       
   930 
       
   931 lemma zero_in_positive:
 
       
   932   shows "RZERO \<in> rexp_enum (Suc N)"
 
       
   933   by (metis le_add1 plus_1_eq_Suc rexp_enum_mono subsetD zero_in_Suc0(2))
 
       
   934 
       
   935 lemma one_in_positive:
 
       
   936   shows "RONE \<in> rexp_enum (Suc N)"
 
       
   937   by (metis le_add1 plus_1_eq_Suc rexp_enum_mono subsetD one_in_Suc0(2))
 
       
   938 
       
   939 lemma alts_in_positive:
 
       
   940   shows "RALTS [] \<in> rexp_enum (Suc N)"
 
       
   941   by (metis One_nat_def alts_nil_in_Suc0(1) le_add_same_cancel1 less_Suc_eq_le plus_1_eq_Suc rexp_enum_mono subsetD zero_less_Suc)
 
       
   942 
       
   943 lemma char_in_positive:
 
       
   944   shows "RCHAR c \<in> rexp_enum (Suc N)"
 
       
   945   apply(cases c)
 
       
   946      apply (metis Suc_eq_plus1 char_in1 le_add2 rexp_enum_mono subsetD)+
 
       
   947   done
 
       
   948 
   907 lemma enum_inductive_cases:
 
   949 lemma enum_inductive_cases:
 
   908   shows "rsize (RSEQ r1 r2) = Suc n \<Longrightarrow> \<exists>i j. rsize r1 = i \<and> rsize r2 = j\<and> i + j = n"
 
   950   shows "rsize (RSEQ r1 r2) = Suc n \<Longrightarrow> \<exists>i j. rsize r1 = i \<and> rsize r2 = j\<and> i + j = n"
 
   909   by (metis Suc_inject rsize.simps(5))
 
   951   by (metis Suc_inject rsize.simps(5))
 
   910 thm rsize.simps(5)
 
   952 
   911 
   953 
   912 lemma enumeration_finite:
 
   954 lemma enumeration_finite:
 
   913   shows "\<exists>Nn. card (rexp_enum n) < Nn"
 
   955   shows "\<exists>Nn. card (rexp_enum n) < Nn"
 
   914   apply(simp add:no_top_class.gt_ex)
 
   956   apply(simp add:no_top_class.gt_ex)
 
   915   done
 
   957   done
 
       
   958 
       
   959 
       
   960 lemma s1:
 
       
   961 "{r::rexp . size r = 0} = ({ZERO, ONE} \<union> {CH c| c. True})"
 
       
   962 apply(auto)
 
       
   963 apply(case_tac x)
 
       
   964 apply(simp_all)
 
       
   965 done
 
       
   966 
       
   967 
       
   968 
       
   969 
       
   970 lemma enum_Suc0:
 
       
   971   shows " rexp_enum (Suc 0) = {RZERO} \<union> {RONE} \<union> {RCHAR c | c. True} \<union> {RALTS []}"
 
       
   972   by auto
 
       
   973 
       
   974 lemma enumeration_chars_finite:
 
       
   975   shows "finite {RCHAR c |c. True}"
 
       
   976   apply(subgoal_tac "finite (RCHAR ` (UNIV::char set))")
 
       
   977   prefer 2
 
       
   978   using finite_code apply blast
 
       
   979   by (simp add: full_SetCompr_eq)
 
       
   980 
       
   981 lemma enum_Suc0_finite:
 
       
   982   shows "finite (rexp_enum (Suc 0))"
 
       
   983   apply(subgoal_tac "finite ( {RZERO} \<union> {RONE} \<union> {RCHAR c | c. True} \<union> {RALTS []})")
 
       
   984   using enum_Suc0 apply presburger
 
       
   985   using enumeration_chars_finite by blast
 
       
   986 
       
   987 lemma enum_1_finite:
 
       
   988   shows "finite (rexp_enum 1)"
 
       
   989   using enum_Suc0_finite by force
 
       
   990 
       
   991 lemma enum_stars_finite:
 
       
   992   shows " finite (rexp_enum n) \<Longrightarrow> finite {RSTAR r0 | r0. r0 \<in> (rexp_enum n)}"
 
       
   993   apply(induct n)
 
       
   994    apply simp
 
       
   995   apply simp
 
       
   996   done
 
       
   997 
       
   998 definition RSEQ_set
 
       
   999   where
 
       
  1000   "RSEQ_set A B \<equiv> (\<lambda>(r1, r2) . (RSEQ r1 r2 )) ` (A \<times> B)"
 
       
  1001 
       
  1002 
       
  1003 lemma enum_seq_finite:
 
       
  1004   shows "(\<forall>k. k < n \<longrightarrow> finite (rexp_enum k)) \<Longrightarrow> finite  
       
  1005 {(RSEQ r1 r2)|r1 r2 i j. r1 \<in>  (rexp_enum i) \<and> r2 \<in>  (rexp_enum j) \<and> i + j = n}"
 
       
  1006   apply(induct n)
 
       
  1007    apply simp
 
       
  1008   apply(subgoal_tac "{(RSEQ r1 r2)|r1 r2 i j. r1 \<in>  (rexp_enum i) \<and> r2 \<in>  (rexp_enum j) \<and> i + j = Suc n}
 
       
  1009 \<subseteq> RSEQ_set (rexp_enum n) (rexp_enum n)")
 
       
  1010    apply(subgoal_tac "finite ( RSEQ_set (rexp_enum n) (rexp_enum n))")
 
       
  1011   using rev_finite_subset
 
       
  1012     apply fastforce
 
       
  1013 
       
  1014   sorry
 
       
  1015 
       
  1016 
       
  1017 
       
  1018 lemma enum_induct_finite:
 
       
  1019   shows " finite ( {(RSEQ r1 r2)|r1 r2 i j. r1 \<in>  (rexp_enum i) \<and> r2 \<in>  (rexp_enum j) \<and> i + j = n} \<union>
 
       
  1020 {(RALTS (a # rs)) | a rs i j. a \<in> (rexp_enum i) \<and> (RALTS rs) \<in> (rexp_enum j) \<and> i + j = Suc n \<and> i \<le> n \<and> j \<le> n} \<union>
 
       
  1021 {RSTAR r0 | r0. r0 \<in> (rexp_enum n)} \<union>
 
       
  1022 (rexp_enum n))"
 
       
  1023   apply(induct n)
 
       
  1024   apply simp
 
       
  1025   sorry
 
       
  1026 
       
  1027 lemma enumeration_finite2:
 
       
  1028   shows "finite (rexp_enum n)"
 
       
  1029   apply(cases n)
 
       
  1030   apply auto[1]
 
       
  1031   apply(case_tac nat)
 
       
  1032   using enum_Suc0_finite apply blast
 
       
  1033   apply(subgoal_tac "rexp_enum ( Suc n) =  {(RSEQ r1 r2)|r1 r2 i j. r1 \<in>  (rexp_enum i) \<and> r2 \<in>  (rexp_enum j) \<and> i + j = n} \<union>
 
       
  1034 {(RALTS (a # rs)) | a rs i j. a \<in> (rexp_enum i) \<and> (RALTS rs) \<in> (rexp_enum j) \<and> i + j = Suc n \<and> i \<le> n \<and> j \<le> n} \<union>
 
       
  1035 {RSTAR r0 | r0. r0 \<in> (rexp_enum n)} \<union>
 
       
  1036 (rexp_enum n)")
 
       
  1037   prefer 2
 
       
  1038   using rexp_enum.simps(3) apply presburger
 
       
  1039   using enum_induct_finite by auto
 
       
  1040 
   916 
  1041 
   917 lemma size1_rexps:
 
  1042 lemma size1_rexps:
 
   918   shows "RCHAR x \<in> rexp_enum 1"
 
  1043   shows "RCHAR x \<in> rexp_enum 1"
 
   919   apply(cases x)
 
  1044   apply(cases x)
 
   920      apply auto
 
  1045      apply auto
 
   976   apply(subgoal_tac "r \<in> {uu.
 
  1101   apply(subgoal_tac "r \<in> {uu.
 
   977       \<exists>a rs i j. uu = RALTS (a # rs) \<and> a \<in> rexp_enum i \<and> RALTS rs \<in> rexp_enum j \<and> i + j = Suc N \<and> i \<le> N \<and> j \<le> N}")
 
  1102       \<exists>a rs i j. uu = RALTS (a # rs) \<and> a \<in> rexp_enum i \<and> RALTS rs \<in> rexp_enum j \<and> i + j = Suc N \<and> i \<le> N \<and> j \<le> N}")
 
   978    apply auto[1]
 
  1103    apply auto[1]
 
   979   apply(subgoal_tac "RALTS (a # list) \<in>  {uu.
 
  1104   apply(subgoal_tac "RALTS (a # list) \<in>  {uu.
 
   980       \<exists>a rs i j. uu = RALTS (a # rs) \<and> a \<in> rexp_enum i \<and> RALTS rs \<in> rexp_enum j \<and> i + j = Suc N \<and> i \<le> N \<and> j \<le> N}")
 
  1105       \<exists>a rs i j. uu = RALTS (a # rs) \<and> a \<in> rexp_enum i \<and> RALTS rs \<in> rexp_enum j \<and> i + j = Suc N \<and> i \<le> N \<and> j \<le> N}")
 
   981 
       
   982   
       
   983    apply fastforce
 
  1106    apply fastforce
 
   984   apply(subgoal_tac "a \<in> rexp_enum i")
 
  1107   apply(subgoal_tac "a \<in> rexp_enum i")
 
   985   prefer 2
 
  1108   prefer 2
 
   986   
       
   987    apply linarith
 
  1109    apply linarith
 
   988   by blast
 
  1110   by blast
 
       
  1111 
       
  1112 thm rsize.elims
 
   989 
  1113 
   990 lemma rexp_enum_covers:
 
  1114 lemma rexp_enum_covers:
 
   991   shows " rsize r \<le> N \<Longrightarrow> r \<in> rexp_enum N \<and> r \<in> rexp_enum (rsize r)"
 
  1115   shows " rsize r \<le> N \<Longrightarrow> r \<in> rexp_enum N \<and> r \<in> rexp_enum (rsize r)"
 
   992   apply(induct N arbitrary : r)
 
  1116   apply(induct N arbitrary : r)
 
   993    apply simp
 
  1117    apply simp
 
  1014          apply (meson def_enum_alts rexp_size_induct)
 
  1138          apply (meson def_enum_alts rexp_size_induct)
 
  1015         apply(subgoal_tac "rsize (RALTS list) \<le> N")
 
  1139         apply(subgoal_tac "rsize (RALTS list) \<le> N")
 
  1016          apply(subgoal_tac "RALTS list \<in> rexp_enum N")
 
  1140          apply(subgoal_tac "RALTS list \<in> rexp_enum N")
 
  1017   prefer 2
 
  1141   prefer 2
 
  1018           apply presburger
 
  1142           apply presburger
 
  1019   
  1143   using def_enum_alts rexp_size_induct apply presburger
 
  1020   sorry
 
  1144   using rexp_size_induct apply presburger
 
  1021 
  1145   using rexp_size_induct apply presburger  
  1022 
  1146   using rexp_size_induct apply presburger
 
  1023 lemma finite_size_finite_regx:
 
  1147       apply(subgoal_tac "r \<in> rexp_enum 1")
 
  1024   shows " \<exists>l. \<forall>rs. ((\<forall>r \<in> (set rs). rsize r < N) \<and> (distinct rs) \<longrightarrow> (length rs) < l) "
 
  1148   apply (metis rsize.simps(1))
 
  1025 
  1149   apply(subgoal_tac "rsize r = Suc 0")
 
  1026   sorry
 
  1150   prefer 2
 
       
  1151   using rsize.simps(1) apply presburger
 
       
  1152       apply(subgoal_tac "r \<in> rexp_enum (Suc 0)")
 
       
  1153        apply force
 
       
  1154   using zero_in_Suc0 apply blast
 
       
  1155   apply simp
 
       
  1156   
       
  1157   using one_in_positive apply auto[1]
 
       
  1158   
       
  1159   apply (metis char_in_positive)
 
       
  1160    apply(subgoal_tac "rsize x41 \<le> N")
 
       
  1161     apply(subgoal_tac "rsize x42 \<le> N")
 
       
  1162   prefer 2
 
       
  1163      apply auto[1]
 
       
  1164   prefer 2
 
       
  1165   using enum_inductive_cases nat_le_iff_add apply blast
 
       
  1166    apply(subgoal_tac "x41 \<in> rexp_enum (rsize x41)")
 
       
  1167     prefer 2
 
       
  1168     apply blast
 
       
  1169    apply(subgoal_tac "x42 \<in> rexp_enum (rsize x42)")
 
       
  1170   prefer 2
 
       
  1171   apply blast
 
       
  1172    apply(subgoal_tac "rsize x42 + rsize x41 = N")
 
       
  1173   prefer 2
 
       
  1174   using add.commute enum_inductive_cases apply blast
 
       
  1175   apply(subgoal_tac "rexp_enum (Suc N) =  {(RSEQ r1 r2)|r1 r2 i j. r1 \<in>  (rexp_enum i) \<and> r2 \<in>  (rexp_enum j) \<and> i + j = N} \<union>
 
       
  1176 {(RALTS (a # rs)) | a rs i j. a \<in> (rexp_enum i) \<and> (RALTS rs) \<in> (rexp_enum j) \<and> i + j = Suc  N \<and> i \<le> N \<and> j \<le> N} \<union>
 
       
  1177 {RSTAR r0 | r0. r0 \<in> (rexp_enum N)} \<union>
 
       
  1178 (rexp_enum N)")
 
       
  1179     apply (smt (verit, del_insts) UnCI mem_Collect_eq old.nat.inject rsize.simps(5))
 
       
  1180    apply (smt (verit, ccfv_threshold) One_nat_def nle_le not_less_eq_eq rexp_enum_case3 size_geq1)
 
       
  1181   apply(subgoal_tac "x6 \<in> rexp_enum N")
 
       
  1182   prefer 2
 
       
  1183 
       
  1184    apply force
 
       
  1185   apply(subgoal_tac "N \<ge> Suc 0")
 
       
  1186   prefer 2
 
       
  1187   apply (metis less_Suc_eq_le non_zero_size rsize.simps(6))
 
       
  1188   apply(subgoal_tac "rexp_enum (Suc N) =  {(RSEQ r1 r2)|r1 r2 i j. r1 \<in>  (rexp_enum i) \<and> r2 \<in>  (rexp_enum j) \<and> i + j = N} \<union>
 
       
  1189 {(RALTS (a # rs)) | a rs i j. a \<in> (rexp_enum i) \<and> (RALTS rs) \<in> (rexp_enum j) \<and> i + j = Suc  N \<and> i \<le> N \<and> j \<le> N} \<union>
 
       
  1190 {RSTAR r0 | r0. r0 \<in> (rexp_enum N)} \<union>
 
       
  1191 (rexp_enum N)")
 
       
  1192   prefer 2
 
       
  1193   using rexp_enum_case3 apply presburger
 
       
  1194   by (metis (mono_tags, lifting) Un_iff mem_Collect_eq)
 
       
  1195 
       
  1196 
       
  1197 
       
  1198 
       
  1199 
       
  1200 definition
 
       
  1201   "sizeNregex N \<equiv> {r. rsize r \<le> N}"
 
       
  1202 
       
  1203 
       
  1204 
       
  1205 lemma sizeNregex_covered:
 
       
  1206   shows "sizeNregex N \<subseteq> rexp_enum N"
 
       
  1207   using rexp_enum_covers sizeNregex_def by auto
 
       
  1208 
       
  1209 lemma finiteness_of_sizeN_regex:
 
       
  1210   shows "finite (sizeNregex N)"
 
       
  1211   by (meson enumeration_finite2 rev_finite_subset sizeNregex_covered)
 
       
  1212 
       
  1213 
  1027 
  1214 
  1028 (*below  probably needs proved concurrently*)
 
  1215 (*below  probably needs proved concurrently*)
 
  1029 
  1216 
  1030 lemma finite_r1r2_ders_list:
 
  1217 lemma finite_r1r2_ders_list:
 
  1031   shows "(\<forall>s. rsize (rders_simp r1 s) < N1 \<and> rsize (rders_simp r2 s) < N2)
 
  1218   shows "(\<forall>s. rsize (rders_simp r1 s) < N1 \<and> rsize (rders_simp r2 s) < N2)
lexing