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 442 09a57446696a
parent 441 426a93160f4a
equal deleted inserted replaced
441:426a93160f4a 442:09a57446696a 
   866 "rexp_enum 0 = []"
 
   866 "rexp_enum 0 = []"
 
   867 |"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)))"
 
   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]"
 
   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]"
 
   869 
   869 
   870 *)
 
   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 
       
   877 context notes rev_conj_cong[fundef_cong] begin
 
       
   878 function (sequential) rexp_enum :: "nat \<Rightarrow> rrexp set"
 
       
   879   where 
       
   880 "rexp_enum 0 = {}"
 
       
   881 |"rexp_enum (Suc 0) =  {RALTS []} \<union> {RZERO} \<union> {RONE} \<union> { (RCHAR c) |c::char. True }"
 
       
   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>
 
       
   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>
 
       
   884 {RSTAR r0 | r0. r0 \<in> (rexp_enum n)} \<union>
 
       
   885 (rexp_enum n)"
 
       
   886   by pat_completeness auto
 
       
   887 termination
 
       
   888   by (relation "measure size") auto
 
       
   889 end
 
       
   890 
       
   891 lemma rexp_enum_inclusion:
 
       
   892   shows "(rexp_enum n) \<subseteq> (rexp_enum (Suc n))"
 
       
   893   apply(induct n)
 
       
   894    apply auto[1]
 
       
   895   apply(simp)
 
       
   896   done
 
       
   897 
       
   898 lemma rexp_enum_mono:
 
       
   899   shows "n \<le> m \<Longrightarrow> (rexp_enum n) \<subseteq> (rexp_enum m)"
 
       
   900   by (simp add: lift_Suc_mono_le rexp_enum_inclusion)
 
       
   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 
       
   949 lemma enum_inductive_cases:
 
       
   950   shows "rsize (RSEQ r1 r2) = Suc n \<Longrightarrow> \<exists>i j. rsize r1 = i \<and> rsize r2 = j\<and> i + j = n"
 
       
   951   by (metis Suc_inject rsize.simps(5))
 
       
   952 
       
   953 
       
   954 lemma enumeration_finite:
 
       
   955   shows "\<exists>Nn. card (rexp_enum n) < Nn"
 
       
   956   apply(simp add:no_top_class.gt_ex)
 
       
   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 
       
  1041 
       
  1042 lemma size1_rexps:
 
       
  1043   shows "RCHAR x \<in> rexp_enum 1"
 
       
  1044   apply(cases x)
 
       
  1045      apply auto
 
       
  1046   done
 
       
  1047 
   871 
  1048 lemma non_zero_size:
 
   872 lemma non_zero_size:
 
  1049   shows "rsize r \<ge> Suc 0"
 
   873   shows "rsize r \<ge> Suc 0"
 
  1050   apply(induct r)
 
   874   apply(induct r)
 
  1051   apply auto done
 
   875   apply auto done
 
  1068   prefer 2
 
   892   prefer 2
 
  1069   using size_geq1 apply blast
 
   893   using size_geq1 apply blast
 
  1070   apply simp
 
   894   apply simp
 
  1071   done
 
   895   done
 
  1072 
   896 
  1073 lemma rexp_enum_case3:
 
   897 definition SEQ_set where
 
  1074   shows "N \<ge> Suc 0 \<Longrightarrow> 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>
 
   898   "SEQ_set A n \<equiv> {RSEQ r1 r2 | r1 r2. r1 \<in> A \<and> r2 \<in> A \<and> rsize r1 + rsize r2 \<le> n}"
 
  1075 {(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>
 
   899 
  1076 {RSTAR r0 | r0. r0 \<in> (rexp_enum N)} \<union>
 
   900 definition SEQ_set_cartesian where
 
  1077 (rexp_enum N)"
 
   901 "SEQ_set_cartesian A n  = {RSEQ r1 r2 | r1 r2. r1 \<in> A \<and> r2 \<in> A}"
 
  1078   apply(case_tac N)
 
   902 
  1079    apply simp
 
   903 definition ALT_set where
 
  1080   apply auto
 
   904 "ALT_set A n \<equiv> {RALTS rs | rs. set rs \<subseteq> A \<and> sum_list (map rsize rs) \<le> n}"
 
  1081   done
 
       
  1082 
       
  1083 
       
  1084 
       
  1085 lemma def_enum_alts:
 
       
  1086   shows "\<lbrakk> r = RALTS x5; x5 = a # list;
 
       
  1087         rsize a = i \<and> rsize (RALTS list) = j \<and> i + j = Suc N \<and> a \<in> (rexp_enum i) \<and> (RALTS list) \<in> (rexp_enum j) \<rbrakk>
 
       
  1088        \<Longrightarrow> r \<in> rexp_enum (Suc N)"
 
       
  1089   apply(subgoal_tac "N \<ge> 1")
 
       
  1090   prefer 2
 
       
  1091   apply (metis One_nat_def add_is_1 less_Suc0 linorder_le_less_linear non_zero_size)
 
       
  1092   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>
 
       
  1093 {(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>
 
       
  1094 {RSTAR r0 | r0. r0 \<in> (rexp_enum N)} \<union>
 
       
  1095 (rexp_enum N)")
 
       
  1096   prefer 2
 
       
  1097   using One_nat_def rexp_enum_case3 apply presburger
 
       
  1098   apply(subgoal_tac "i \<le> N \<and> j \<le> N")
 
       
  1099   prefer 2
 
       
  1100   using non_zero_size apply auto[1]
 
       
  1101   apply(subgoal_tac "r \<in> {uu.
 
       
  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}")
 
       
  1103    apply auto[1]
 
       
  1104   apply(subgoal_tac "RALTS (a # list) \<in>  {uu.
 
       
  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}")
 
       
  1106    apply fastforce
 
       
  1107   apply(subgoal_tac "a \<in> rexp_enum i")
 
       
  1108   prefer 2
 
       
  1109    apply linarith
 
       
  1110   by blast
 
       
  1111 
       
  1112 thm rsize.elims
 
       
  1113 
       
  1114 lemma rexp_enum_covers:
 
       
  1115   shows " rsize r \<le> N \<Longrightarrow> r \<in> rexp_enum N \<and> r \<in> rexp_enum (rsize r)"
 
       
  1116   apply(induct N arbitrary : r)
 
       
  1117    apply simp
 
       
  1118   
       
  1119   using rsize.elims apply auto[1]
 
       
  1120   apply(case_tac "rsize r \<le> N")
 
       
  1121   using enumeration_finite
 
       
  1122   
       
  1123    apply (meson in_mono rexp_enum_inclusion)
 
       
  1124   apply(subgoal_tac "rsize r = Suc N")
 
       
  1125   prefer 2
 
       
  1126   using le_Suc_eq apply blast
 
       
  1127 
       
  1128   apply(case_tac r)
 
       
  1129        prefer 5
 
       
  1130        apply(case_tac x5)
 
       
  1131         apply(subgoal_tac "rsize r =1")
 
       
  1132   prefer 2
 
       
  1133   using hand_made_def_rlist_size rlist_size.simps(2) rsize.simps(4) apply presburger
 
       
  1134         apply simp
 
       
  1135   apply(subgoal_tac "a \<in> rexp_enum (rsize a)")
 
       
  1136   apply(subgoal_tac "RALTS list \<in> rexp_enum (rsize (RALTS list))")
 
       
  1137   
       
  1138          apply (meson def_enum_alts rexp_size_induct)
 
       
  1139         apply(subgoal_tac "rsize (RALTS list) \<le> N")
 
       
  1140          apply(subgoal_tac "RALTS list \<in> rexp_enum N")
 
       
  1141   prefer 2
 
       
  1142           apply presburger
 
       
  1143   using def_enum_alts rexp_size_induct apply presburger
 
       
  1144   using rexp_size_induct apply presburger
 
       
  1145   using rexp_size_induct apply presburger  
       
  1146   using rexp_size_induct apply presburger
 
       
  1147       apply(subgoal_tac "r \<in> rexp_enum 1")
 
       
  1148   apply (metis rsize.simps(1))
 
       
  1149   apply(subgoal_tac "rsize r = Suc 0")
 
       
  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 
   905 
  1199 
   906 
  1200 definition
 
   907 definition
 
  1201   "sizeNregex N \<equiv> {r. rsize r \<le> N}"
 
   908   "sizeNregex N \<equiv> {r. rsize r \<le> N}"
 
  1202 
   909 
  1203 
   910 lemma sizenregex_induct:
 
  1204 
   911   shows "sizeNregex (Suc n) = sizeNregex n \<union> {RZERO, RONE, RALTS []} \<union> {RCHAR c| c. True} \<union>
 
  1205 lemma sizeNregex_covered:
 
   912 SEQ_set ( sizeNregex n) n \<union> ALT_set (sizeNregex n) n \<union> (RSTAR ` (sizeNregex n))"
 
  1206   shows "sizeNregex N \<subseteq> rexp_enum N"
 
   913   sorry
 
  1207   using rexp_enum_covers sizeNregex_def by auto
 
   914 
  1208 
   915 
  1209 lemma finiteness_of_sizeN_regex:
 
   916 lemma chars_finite:
 
  1210   shows "finite (sizeNregex N)"
 
   917   shows "finite (RCHAR ` (UNIV::(char set)))"
 
  1211   by (meson enumeration_finite2 rev_finite_subset sizeNregex_covered)
 
   918   apply(simp)
 
  1212 
   919   done
 
  1213 
   920 
       
   921 thm full_SetCompr_eq 
       
   922 
       
   923 lemma size1finite:
 
       
   924   shows "finite (sizeNregex (Suc 0))"
 
       
   925   apply(subst sizenregex_induct)
 
       
   926   apply(subst finite_Un)+
 
       
   927   apply(subgoal_tac "sizeNregex 0 = {}")
 
       
   928   apply(rule conjI)+
 
       
   929   apply (metis Collect_empty_eq finite.emptyI non_zero_size not_less_eq_eq sizeNregex_def)
 
       
   930       apply simp
 
       
   931       apply (simp add: full_SetCompr_eq)
 
       
   932   apply (simp add: SEQ_set_def)
 
       
   933     apply (simp add: ALT_set_def)  
       
   934    apply(simp add: full_SetCompr_eq)
 
       
   935   using non_zero_size not_less_eq_eq sizeNregex_def by fastforce
 
       
   936 
       
   937 lemma seq_included_in_cart:
 
       
   938   shows "SEQ_set A n \<subseteq> SEQ_set_cartesian A n"
 
       
   939   sledgehammer
 
       
   940 
       
   941 lemma finite_seq:
 
       
   942   shows " finite (sizeNregex n) \<Longrightarrow> finite (SEQ_set (sizeNregex n) n)"
 
       
   943   apply(rule finite_subset)
 
       
   944   sorry
 
       
   945 
       
   946 
       
   947 lemma finite_size_n:
 
       
   948   shows "finite (sizeNregex n)"
 
       
   949   apply(induct n)
 
       
   950   apply (metis Collect_empty_eq finite.emptyI non_zero_size not_less_eq_eq sizeNregex_def)
 
       
   951   apply(subst sizenregex_induct)
 
       
   952   apply(subst finite_Un)+
 
       
   953   apply(rule conjI)+
 
       
   954        apply simp
 
       
   955       apply simp
 
       
   956      apply (simp add: full_SetCompr_eq)
 
       
   957 
       
   958   sorry
 
  1214 
   959 
  1215 (*below  probably needs proved concurrently*)
 
   960 (*below  probably needs proved concurrently*)
 
  1216 
   961 
  1217 lemma finite_r1r2_ders_list:
 
   962 lemma finite_r1r2_ders_list:
 
  1218   shows "(\<forall>s. rsize (rders_simp r1 s) < N1 \<and> rsize (rders_simp r2 s) < N2)
 
   963   shows "(\<forall>s. rsize (rders_simp r1 s) < N1 \<and> rsize (rders_simp r2 s) < N2)
lexing