# HG changeset patch
# User Chengsong
# Date 1644430861 0
# Node ID 5dcecc92608e1535a8289c102ada7d17a14edd25
# Parent  ec08181c1f42cdfaeca931df53ffbec22d4584ba
5ct

diff -r ec08181c1f42 -r 5dcecc92608e thys2/SizeBound5CT.thy
--- a/thys2/SizeBound5CT.thy	Wed Feb 09 00:30:04 2022 +0000
+++ b/thys2/SizeBound5CT.thy	Wed Feb 09 18:21:01 2022 +0000
@@ -1,6 +1,6 @@
 
 theory SizeBound5CT
-  imports "Lexer" "PDerivs"
+  imports "Lexer" "PDerivs" 
 begin
 
 section \<open>Bit-Encodings\<close>
@@ -1893,11 +1893,43 @@
    apply simp
   apply simp
   sorry
+(*
+fun rexp_encode :: "rrexp \<Rightarrow> nat"
+  where
+"rexp_encode RZERO = 0"
+|"rexp_encode RONE = 1"
+|"rexp_encode (RCHAR c) = 2"
+|"rexp_encode (RSEQ r1 r2) = ( 2 ^ (rexp_encode r1)) "
+*)
+lemma finite_chars:
+  shows " \<exists>N. ( (\<forall>r \<in> (set rs). \<exists>c. r = RCHAR c) \<and> (distinct rs) \<longrightarrow> length rs < N)"
+  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)"
+
+
+fun rexp_enum :: "nat \<Rightarrow> rrexp list"
+  where 
+"rexp_enum 0 = []"
+|"rexp_enum 1 =  RZERO # (RONE # (map RCHAR (all_chars 255)))"
+
+lemma finite_sized_rexp_forms_finite_set:
+  shows " \<exists>SN. ( \<forall>r.( rsize r < N \<longrightarrow> r \<in> SN)) \<and> (finite SN)"
+  apply(induct N)
+   apply simp
+   apply auto
+ (*\<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*)
+ (* \<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*)
+  sorry
 
 
 lemma finite_size_finite_regx:
-  shows "\<forall>N. \<exists>l. (\<forall>r \<in> (set rs). rsize r < N) \<and> (distinct rs) \<Longrightarrow> (length rs) < l "
-  sorry
+  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)
 
 
 (*below  probably needs proved concurrently*)
@@ -1978,11 +2010,10 @@
 lemma star_seqs_produce_star_seqs:
   shows "rsimp (rsimp_ALTs (map (rder x \<circ> (\<lambda>s1. rsimp_SEQ (rders_simp r s1) (RSTAR r))) Ss))
        = rsimp (rsimp_ALTs (map ( (\<lambda>s1. rder x (rsimp_SEQ (rders_simp r s1) (RSTAR r)))) Ss))"
-  sledgehammer
   by (meson comp_apply)
 
 lemma der_seqstar_res:
-  shows "rder x "
+  shows "rder x (RSEQ r1 r2) = RSEQ r3 r4"
 
 
 lemma linearity_of_list_of_star_or_starseqs:
@@ -1993,7 +2024,7 @@
    apply simp
    apply (metis list.simps(8) rsimp_ALTs.simps(1))
 
-  sledgehammer
+
   sorry
 
 lemma starder_is_a_list_of_stars_or_starseqs: