--- a/thys2/ClosedFormsBounds.thy	Sun Mar 20 23:32:08 2022 +0000
+++ b/thys2/ClosedFormsBounds.thy	Sun Mar 20 23:32:45 2022 +0000
@@ -704,44 +704,33 @@
   apply auto[1]
   using star_control_variant by blast
 
-
-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)) {})))"
-  by(metis alts_simp_control)
-
-lemma map_ders_is_list_of_ders:
-  shows  "\<forall>s. rsize (rders_simp r2 s) \<le> N2 \<Longrightarrow>
-\<forall>r \<in> set (rdistinct (map (rders_simp r2) Ss) {}). rsize r \<le> N2"
-  apply(rule same_regex_property_after_distinct)
-  by simp
-
 lemma seq_estimate_bounded: 
-  assumes "\<forall>s. rsize (rders_simp r1 s) \<le> N1" and "\<forall>s. rsize (rders_simp r2 s) \<le> N2"
+  assumes "\<forall>s. rsize (rders_simp r1 s) \<le> N1" 
+      and "\<forall>s. rsize (rders_simp r2 s) \<le> N2"
   shows
-"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)))"
-  apply(subgoal_tac " (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {}))) \<le>
-  (Suc (N1 + (rsize r2)) + (N2 * card (sizeNregex N2)))")
-   apply force
-  apply(subgoal_tac " (sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {}))) \<le>
-                      (rsize (RSEQ (rders_simp r1 s) r2)) + (sum_list (map rsize (rdistinct (map (rders_simp r2) (vsuf s r1)) {})) )")
-  prefer 2
-  using triangle_inequality_distinct apply blast
-  apply(subgoal_tac " sum_list (map rsize (rdistinct (map (rders_simp r2) (vsuf s r1)) {})) \<le> N2 * card (sizeNregex N2) ")
-   apply(subgoal_tac "rsize (RSEQ (rders_simp r1 s) r2) \<le> Suc (N1 + rsize r2)")
-    apply linarith
-   apply (simp add: assms(1))
-  apply(subgoal_tac "\<forall>r \<in> set (rdistinct (map (rders_simp r2) (vsuf s r1)) {}). rsize r \<le> N2")
-  apply (metis (no_types, opaque_lifting) assms(2) distinct_list_rexp_up_to_certain_size_bouded_by_set_enumerating_up_to_that_size ex_map_conv mult.commute)
-  using assms(2) map_ders_is_list_of_ders by blast
+    "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)))"
+proof -
+  have a: "sum_list (map rsize (rdistinct (map (rders_simp r2) (vsuf s r1)) {})) \<le> N2 * card (sizeNregex N2)"
+    by (metis assms(2) distinct_list_rexp_up_to_certain_size_bouded_by_set_enumerating_up_to_that_size ex_map_conv mult.commute)
 
+  have "sum_list (map rsize (rdistinct (RSEQ (rders_simp r1 s) r2 # map (rders_simp r2) (vsuf s r1)) {})) \<le>
+          rsize (RSEQ (rders_simp r1 s) r2) + sum_list (map rsize (rdistinct (map (rders_simp r2) (vsuf s r1)) {}))"
+    using triangle_inequality_distinct by blast    
+  also have "... \<le> rsize (RSEQ (rders_simp r1 s) r2) + N2 * card (sizeNregex N2)"
+    by (simp add: a)
+  also have "... \<le> Suc (N1 + (rsize r2) + N2 * card (sizeNregex N2))"
+    by (simp add: assms(1))
+  finally show ?thesis
+    by force
+qed    
 
 
 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))"
+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)
@@ -754,7 +743,6 @@
   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)
@@ -762,8 +750,6 @@
     by auto 
 qed
 
-thm seq_closed_form_bounded2 
-
 
 lemma rders_simp_bounded: 
   shows "\<exists>N. \<forall>s. rsize (rders_simp r s) \<le> N"
@@ -786,18 +772,4 @@
 unused_thms
 
 
-
-
-
-
-
-
-
-
-
-
-(*Obsolete materials*)
-
-
-
 end