--- a/thys2/ClosedFormsBounds.thy	Tue Mar 15 16:37:41 2022 +0000
+++ b/thys2/ClosedFormsBounds.thy	Sat Mar 19 09:53:48 2022 +0000
@@ -493,7 +493,7 @@
     by (metis empty_iff flts_vs_nflts sup_bot_left)
   also have "... \<le>  Suc (sum_list (map rsize (rdistinct rs {})))" 
     by (simp add: larger_acc_smaller_distinct_res0)
-  finally show ?thesis sledgehammer
+  finally show ?thesis
     by blast
 qed
 
@@ -515,13 +515,11 @@
   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 alts_simp_ineq_unfold by auto
+   moreover 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)
+  ultimately show "rsize (rsimp (RALTS rs)) \<le> Suc (sum_list (map rsize (rdistinct rs {})))"
+    by (meson distinct_simp_ineq order.trans)
 qed
 
 
@@ -739,37 +737,47 @@
   using assms(2) map_ders_is_list_of_ders by blast
 
 
-lemma seq_closed_form_bounded: shows
-"\<lbrakk>\<forall>s. rsize (rders_simp r1 s) \<le> N1 ; \<forall>s. rsize (rders_simp r2 s) \<le> N2\<rbrakk> \<Longrightarrow>
-rsize (rders_simp (RSEQ r1 r2) s) \<le> 
-max (Suc (Suc (N1 + (rsize r2)) + (N2 * card (sizeNregex N2)))) (rsize (RSEQ r1 r2)) "
-  apply(case_tac s)
-  apply simp
-  apply(subgoal_tac " (rders_simp (RSEQ r1 r2) s) = 
-rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) # (map (rders_simp r2) (vsuf s r1))))")
-  prefer 2
-  using seq_closed_form_variant apply blast
-  apply(subgoal_tac "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)) {})))")
-  apply(subgoal_tac "Suc (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {})))
-\<le> Suc (Suc (N1 + (rsize r2)) + (N2 * card (sizeNregex N2)))")
-  prefer 2
-  using seq_estimate_bounded apply blast
-   apply(subgoal_tac "rsize (rders_simp (RSEQ r1 r2) s) \<le> Suc (Suc (N1 + rsize r2) + N2 * card (sizeNregex N2))")
-  using le_max_iff_disj apply blast
-   apply auto[1]
-  using seq_list_estimate_control by presburger
+
+lemma seq_closed_form_bounded2: 
+  assumes "\<forall>s. rsize (rders_simp r1 s) \<le> N1"
+  and     "\<forall>s. rsize (rders_simp r2 s) \<le> N2"
+  shows "rsize (rders_simp (RSEQ r1 r2) s) \<le> max (Suc (Suc (N1 + (rsize r2)) + (N2 * card (sizeNregex N2)))) (rsize (RSEQ r1 r2))"
+proof(cases s)
+  case Nil
+  then show "rsize (rders_simp (RSEQ r1 r2) s)
+     \<le> max (Suc (Suc (N1 + rsize r2) + N2 * card (sizeNregex N2))) (rsize (RSEQ r1 r2))" 
+    by simp
+next
+  case (Cons a list)
+  then have "rsize (rders_simp (RSEQ r1 r2) s) = 
+    rsize (rsimp (RALTS ((RSEQ (rders_simp r1 s) r2) # (map (rders_simp r2) (vsuf s r1)))))" 
+  using seq_closed_form_variant by (metis list.discI) 
+  also have "... \<le> Suc (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {})))"
+    using alts_simp_control by blast
+    (*or using seq_list_estimate_control by blast*)   
+  also have "... \<le> Suc (Suc (N1 + (rsize r2)) + (N2 * card (sizeNregex N2)))"
+  using assms seq_estimate_bounded by blast
+  ultimately show "rsize (rders_simp (RSEQ r1 r2) s)
+       \<le> max (Suc (Suc (N1 + rsize r2) + N2 * card (sizeNregex N2))) (rsize (RSEQ r1 r2))"
+    by auto 
+qed
+
+thm seq_closed_form_bounded2 
 
 
-lemma rders_simp_bounded: shows
-"\<exists>N. \<forall>s. rsize (rders_simp r s) \<le> N"
+lemma rders_simp_bounded: 
+  shows "\<exists>N. \<forall>s. rsize (rders_simp r s) \<le> N"
   apply(induct r)
-       apply(rule_tac x = "Suc 0 " in exI)
+  apply(rule_tac x = "Suc 0 " in exI)
   using three_easy_cases0 apply force
   using three_easy_cases1 apply blast
   using three_easy_casesC apply blast
-  using seq_closed_form_bounded apply blast
+  apply(erule exE)+
+  apply(rule exI)
+  apply(rule allI)
+  apply(rule seq_closed_form_bounded2)
+  apply(assumption)
+  apply(assumption)
   apply (metis alts_closed_form_bounded size_list_estimation')
   using star_closed_form_bounded by blast