diff -r 0a94fd47b792 -r 7fb1e3dd5ae6 thys2/ClosedFormsBounds.thy
--- a/thys2/ClosedFormsBounds.thy	Thu Mar 10 15:53:46 2022 +0000
+++ b/thys2/ClosedFormsBounds.thy	Fri Mar 11 21:25:08 2022 +0000
@@ -32,13 +32,25 @@
   sorry
 
 
+lemma star_lambda_ders:
+  shows " \<forall>s. rsize (rders_simp r0 s) \<le> N \<Longrightarrow>
+    \<forall>r\<in>set (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) (star_updates s r0 [[c]])).
+       rsize r \<le> Suc (N + rsize (RSTAR r0))"
+  sorry
+
+
 lemma star_control_bounded:
   shows "\<forall>s. rsize (rders_simp r0 s) \<le> N \<Longrightarrow>        
       (sum_list (map rsize (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0))
          (star_updates s r0 [[c]]) ) {})  ) ) \<le> 
 (card (sizeNregex (Suc (N + rsize (RSTAR r0))))) * (Suc (N + rsize (RSTAR r0)))
 "
-  sorry
+  apply(subgoal_tac "\<forall>r \<in> set (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0))
+         (star_updates s r0 [[c]]) ). (rsize r ) \<le> Suc (N + rsize (RSTAR r0))")
+   prefer 2
+  using star_lambda_ders apply blast
+  using distinct_list_rexp_up_to_certain_size_bouded_by_set_enumerating_up_to_that_size by blast
+
 
 lemma star_control_variant:
   assumes "\<forall>s. rsize (rders_simp r0 s) \<le> N"
@@ -78,7 +90,49 @@
   apply auto[1]
   using star_control_variant by blast
 
+lemma alts_simp_ineq_unfold:
+  shows "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct (rflts (map rsimp rs)) {})))"
+  using rsimp_aalts_smaller by auto
 
+lemma flts_has_no_zero:
+  shows "rdistinct (rflts rs) rset = rdistinct (rflts rs) (insert RZERO rset)"
+  sorry
+
+lemma flts_vs_nflts:
+  shows "\<forall>r \<in> noalts_set. \<forall>xs. r \<noteq> RALTS xs
+ \<and> (\<forall>a \<in> alts_set. \<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set)  
+\<Longrightarrow> Suc (sum_list (map rsize (rdistinct ( rflts rs) (noalts_set \<union> corr_set)  )))
+         \<le> Suc (sum_list (map rsize (rdistinct rs (noalts_set \<union> alts_set) )))"
+  apply(induct rs arbitrary: noalts_set)
+   apply simp
+
+  sorry
+
+
+lemma without_flts_ineq:
+  shows " Suc (sum_list (map rsize (rdistinct (rflts rs) {}) )) \<le> 
+         Suc (sum_list (map rsize (rdistinct (    rs  ) {}  )))"
+  by (metis empty_iff flts_vs_nflts sup_bot_left)
+
+
+lemma distinct_simp_ineq:
+  shows "Suc (sum_list (map rsize (rdistinct (map rsimp rs) {})))
+    \<le> Suc (sum_list (map rsize (rdistinct rs {})))"
+  sorry
+
+
+lemma alts_simp_control:
+  shows "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct rs {})))"
+proof -
+  have "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct (rflts (map rsimp rs)) {})))"
+    
+    using alts_simp_ineq_unfold by auto
+  then have "\<dots> \<le> Suc (sum_list (map rsize (rdistinct (map rsimp rs) {})))"
+    using without_flts_ineq by blast
+
+  show "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct rs {})))"
+    by (meson \<open>Suc (sum_list (map rsize (rdistinct (rflts (map rsimp rs)) {}))) \<le> Suc (sum_list (map rsize (rdistinct (map rsimp rs) {})))\<close> \<open>rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct (rflts (map rsimp rs)) {})))\<close> distinct_simp_ineq order_trans)
+qed
 
 
 
@@ -86,8 +140,7 @@
 lemma seq_list_estimate_control: shows 
 " rsize (rsimp (RALTS (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1))))
            \<le> Suc (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {})))"
-  
-  sorry
+  by(metis alts_simp_control)
 
 lemma rdistinct_equality1:
   shows "a \<notin> ss \<Longrightarrow> rdistinct (a  # rs) ss = a # rdistinct rs (insert a ss) "
@@ -115,7 +168,10 @@
 
 lemma larger_acc_smaller_distinct_res:
   shows " (sum_list (map rsize (rdistinct rs ss))) \<ge> (sum_list (map rsize (rdistinct rs (insert a ss))))"
-  sorry
+  apply(subgoal_tac "ss \<subseteq> (insert a ss)")
+   apply(rule larger_acc_smaller_distinct_res0)
+   apply simp
+  by (simp add: subset_insertI)
 
 lemma size_list_triangle1:
   shows  "sum_list (map rsize (a # (rdistinct as ss))) \<ge> rsize a + sum_list (map rsize (rdistinct as (insert a ss)))"