# HG changeset patch
# User Chengsong
# Date 1644283526 0
# Node ID fb23e3fd12e55242bf5ad0f07916995a646b271c
# Parent  d9e1df9ae58f12f8ff230a02d4bcd2e694a33fbe
prf

diff -r d9e1df9ae58f -r fb23e3fd12e5 thys2/SizeBound5CT.thy
--- a/thys2/SizeBound5CT.thy	Tue Feb 08 00:38:27 2022 +0000
+++ b/thys2/SizeBound5CT.thy	Tue Feb 08 01:25:26 2022 +0000
@@ -1724,7 +1724,7 @@
 |"nullable_bools r [] = []"
 
   
-lemma ders_simp_commute:
+lemma shape_derssimp_seq:
   shows "\<lbrakk>s \<noteq>[] \<rbrakk> \<Longrightarrow> rerase  (bders_simp r s) = rerase (bsimp (bders r s))"
 and "\<lbrakk>s \<noteq> []\<rbrakk> \<Longrightarrow> rders_simp (RSEQ r1 r2) s = 
          rsimp (RALTS  ((RSEQ (rders r1 s) r2) #
@@ -1745,6 +1745,10 @@
   apply presburger
   sorry
 
+lemma shape_derssimp_alts:
+  shows "rders_simp (RALTS rs) s = rsimp (RALTS (map (\<lambda>r. rders r s) rs))"
+
+
 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
@@ -1763,8 +1767,45 @@
   sorry
 
 
+lemma finite_star:
+  shows "(\<forall>s. rsize (rders_simp r0 s) < N0 )
+           \<Longrightarrow> \<exists>N3. \<forall>s.(rsize (rders_simp (RSTAR r0) s)) < N3"
+  sorry
+
+
+lemma rderssimp_zero:
+  shows"rders_simp RZERO s = RZERO"
+  apply(induction s)
+  apply simp
+  by simp
+
+lemma rderssimp_one:
+  shows"rders_simp RONE (a # s) = RZERO"
+  apply(induction s)
+  apply simp
+  by simp
+
+lemma rderssimp_char:
+  shows "rders_simp (RCHAR c) s = RONE \<or> rders_simp (RCHAR c) s = RZERO \<or> rders_simp (RCHAR c) s = (RCHAR c)"
+  apply auto
+  by (metis rder.simps(2) rder.simps(3) rders_simp.elims rders_simp.simps(2) rderssimp_one rsimp.simps(4))
+
 lemma finite_size_ders:
-  shows "\<forall>r. \<exists>Nr. \<forall>s. rsize (rders_simp r s) < Nr"
+  shows " \<exists>Nr. \<forall>s. rsize (rders_simp r s) < Nr"
+  apply(induct r rule: rrexp.induct)
+       apply auto
+  apply(rule_tac x = "2" in exI)
+  using rderssimp_zero rsize.simps(1) apply presburger
+      apply(rule_tac x = "2" in exI)
+      apply (metis Suc_1 lessI rders_simp.elims rderssimp_one rsize.simps(1) rsize.simps(2))
+     apply(rule_tac x = "2" in meta_spec)
+     apply (metis lessI rderssimp_char rsize.simps(1) rsize.simps(2) rsize.simps(3))
+  
+  using finite_seq apply blast
+   prefer 2
+
+   apply (simp add: finite_star)
+sledgehammer
   sorry