diff -r afd8eff20402 -r 579caa608a15 thys2/SizeBound5CT.thy
--- a/thys2/SizeBound5CT.thy	Wed Feb 09 18:21:15 2022 +0000
+++ b/thys2/SizeBound5CT.thy	Fri Feb 11 17:28:33 2022 +0000
@@ -1906,16 +1906,15 @@
   apply(rule_tac x = "Suc 256" in exI)
   sorry
 
-fun all_chars :: "nat \<Rightarrow> char list"
-  where
-"all_chars 0 = [CHR 0x00]"
-|"all_chars (Suc i) = (char_of (Suc i)) # (all_chars i)"
-
+definition all_chars :: "int \<Rightarrow> char list"
+  where "all_chars n = map char_of [0..n]"
 
 fun rexp_enum :: "nat \<Rightarrow> rrexp list"
   where 
 "rexp_enum 0 = []"
-|"rexp_enum 1 =  RZERO # (RONE # (map RCHAR (all_chars 255)))"
+|"rexp_enum (Suc 0) =  RALTS [] # RZERO # (RONE # (map RCHAR (all_chars 255)))"
+|"rexp_enum (Suc n) = [(RSEQ r1 r2). r1 \<in> set (rexp_enum i) \<and> r2 \<in> set (rexp_enum j) \<and> i + j = n]"
+
 
 lemma finite_sized_rexp_forms_finite_set:
   shows " \<exists>SN. ( \<forall>r.( rsize r < N \<longrightarrow> r \<in> SN)) \<and> (finite SN)"
@@ -1929,8 +1928,7 @@
 
 lemma finite_size_finite_regx:
   shows " \<exists>l. \<forall>rs. ((\<forall>r \<in> (set rs). rsize r < N) \<and> (distinct rs) \<longrightarrow> (length rs) < l) "
-  apply(frule finite_sized_rexp_forms_finite_set)
-
+  sorry
 
 (*below  probably needs proved concurrently*)