
diff -r 0497408a3598 -r 94604a5fd271 thys3/src/ClosedFormsBounds.thy
--- a/thys3/src/ClosedFormsBounds.thy	Wed Jul 13 08:35:09 2022 +0100
+++ b/thys3/src/ClosedFormsBounds.thy	Wed Jul 13 08:35:45 2022 +0100
@@ -141,7 +141,7 @@
              apply(simp only:)
   apply(subgoal_tac "rsizes (rdistinct rs (insert RZERO (insert RONE noalts_set \<union> alts_set)))
                    \<le>  rsizes (RONE # rdistinct rs (insert RZERO (insert RONE noalts_set \<union> alts_set)))")
-  apply (smt (verit, best) dual_order.trans insert_iff rrexp.distinct(15))
+  apply (smt (verit, ccfv_threshold) dual_order.trans insertE rrexp.distinct(17))
   apply (metis (no_types, opaque_lifting)  le_add_same_cancel2 list.simps(9) sum_list.Cons zero_le)
             apply fastforce
            apply fastforce
@@ -151,8 +151,8 @@
   using rflts.simps(4) apply presburger
       apply simp
       apply(subgoal_tac "insert RONE (noalts_set \<union> corr_set) = (insert RONE noalts_set) \<union> corr_set")
-  apply(simp only:)
-  apply (metis Un_insert_left insertE rrexp.distinct(15))
+        apply(simp only:)
+  apply (metis Un_insert_left insertE rrexp.distinct(17))
       apply fastforce
      apply(case_tac "a \<in> noalts_set")
       apply simp
@@ -174,14 +174,14 @@
   apply(subgoal_tac "(insert a (noalts_set \<union> alts_set)) = (insert a noalts_set) \<union> alts_set")
         apply(simp only:)
         apply(subgoal_tac "noalts_set \<union> corr_set = (insert a noalts_set) \<union> corr_set")
-  apply(simp only:)
-  apply (metis insertE rrexp.distinct(21))
+          apply(simp only:)
+  apply (metis insertE nonalt.simps(1) nonalt.simps(4))
         apply blast
   
   apply fastforce
   apply force
-     apply simp
-     apply (metis Un_insert_left insert_iff rrexp.distinct(21))
+      apply simp
+  apply (metis Un_insert_left insertE nonalt.simps(1) nonalt.simps(4))
     apply(case_tac "a \<in> noalts_set")
      apply simp
   apply(subgoal_tac "a \<notin> alts_set")
@@ -204,14 +204,13 @@
         apply(subgoal_tac "noalts_set \<union> corr_set = (insert a noalts_set) \<union> corr_set")
   apply(simp only:)
 
-
-  apply (metis insertE rrexp.distinct(25))
+         apply (metis insertE rrexp.distinct(31))
   apply blast
   apply fastforce
   apply force
      apply simp
   
-    apply (metis Un_insert_left insertE rrexp.distinct(25))
+    apply (metis Un_insert_left insertE rrexp.distinct(31))
 
   using Suc_le_mono flts_size_reduction_alts apply presburger
      apply(case_tac "a \<in> noalts_set")
@@ -234,16 +233,42 @@
   apply(subgoal_tac "(insert a (noalts_set \<union> alts_set)) = (insert a noalts_set) \<union> alts_set")
         apply(simp only:)
         apply(subgoal_tac "noalts_set \<union> corr_set = (insert a noalts_set) \<union> corr_set")
-  apply(simp only:)
-  apply (metis insertE rrexp.distinct(29))
+       apply(simp only:)
+  apply (metis insertE rrexp.distinct(37))
 
         apply blast
   
   apply fastforce
   apply force
      apply simp
-  apply (metis Un_insert_left insert_iff rrexp.distinct(29))
-  done
+   apply (metis Un_insert_left insert_iff rrexp.distinct(37))
+  apply(case_tac "a \<in> noalts_set")
+      apply simp
+  apply(subgoal_tac "a \<notin> alts_set")
+     prefer 2
+      apply blast
+  apply(case_tac "a \<in> corr_set")
+      apply(subgoal_tac "noalts_set \<union> corr_set = insert a ( noalts_set  \<union> corr_set)")
+  prefer 2
+  apply fastforce
+   apply(simp only:)
+   apply(subgoal_tac "rsizes (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set))) \<le>
+               rsizes (rdistinct (a # rs) (insert RZERO (noalts_set \<union> alts_set)))")
+
+       apply(subgoal_tac "rsizes (rdistinct (rflts (a # rs)) ((insert a noalts_set) \<union> corr_set)) \<le>
+          rsizes (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \<union> alts_set)))")
+  apply fastforce
+       apply simp
+  apply(subgoal_tac "(insert a (noalts_set \<union> alts_set)) = (insert a noalts_set) \<union> alts_set")
+        apply(simp only:)
+        apply(subgoal_tac "noalts_set \<union> corr_set = (insert a noalts_set) \<union> corr_set")
+       apply(simp only:)
+  apply (metis insertE nonalt.simps(1) nonalt.simps(7))
+  apply blast
+  apply blast
+  apply force
+  apply(auto)
+  by (metis Un_insert_left insert_iff rrexp.distinct(39))
 
 
 lemma flts_vs_nflts:
@@ -379,6 +404,220 @@
 qed
 
 
+thm ntimes_closed_form
+
+thm rsize.simps
+
+lemma nupdates_snoc:
+  shows " (nupdates (xs @ [x]) r optlist) = nupdate x r (nupdates xs r optlist)"
+  by (simp add: nupdates_append)
+
+lemma nupdate_elems:
+  shows "\<forall>opt \<in> set (nupdate c r optlist). opt = None \<or> (\<exists>s n. opt = Some (s, n))"
+  using nonempty_string.cases by auto
+
+lemma nupdates_elems:
+  shows "\<forall>opt \<in> set (nupdates s r optlist). opt = None \<or> (\<exists>s n. opt = Some (s, n))"
+  by (meson nonempty_string.cases)
+
+
+lemma opterm_optlist_result_shape:
+  shows "\<forall>r' \<in> set (map (optermsimp r) optlist). r' = RZERO \<or> (\<exists>s m. r' = RSEQ (rders_simp r s) (RNTIMES r m))"
+  apply(induct optlist)
+   apply simp
+  apply(case_tac a)
+  apply simp+
+  by fastforce
+
+
+lemma opterm_optlist_result_shape2:
+  shows "\<And>optlist. \<forall>r' \<in> set (map (optermsimp r) optlist). r' = RZERO \<or> (\<exists>s m. r' = RSEQ (rders_simp r s) (RNTIMES r m))"  
+  using opterm_optlist_result_shape by presburger
+
+
+lemma nupdate_n_leq_n:
+  shows "\<forall>r \<in> set (nupdate c' r [Some ([c], n)]). r = None \<or>( \<exists>s' m. r = Some (s', m) \<and> m \<le> n)"
+  apply(case_tac n)
+   apply simp
+  apply simp
+  done
+(*
+lemma nupdate_induct_leqn:
+  shows "\<lbrakk>\<forall>opt \<in> set optlist. opt = None \<or> (\<exists>s' m. opt = Some(s', m) \<and> m \<le> n) \<rbrakk> \<Longrightarrow> 
+       \<forall>opt \<in> set (nupdate c' r optlist). opt = None \<or> (\<exists>s' m. opt = Some (s', m) \<and> m \<le> n)"
+  apply (case_tac optlist)
+   apply simp
+  apply(case_tac a)
+   apply simp
+  sledgehammer
+*)
+
+
+lemma nupdates_n_leq_n:
+  shows "\<forall>r \<in> set (nupdates s r [Some ([c], n)]). r = None \<or>( \<exists>s' m. r = Some (s', m) \<and> m \<le> n)"
+  apply(induct s rule: rev_induct)
+   apply simp
+  apply(subst nupdates_append)
+  by (metis nupdates_elems_leqn nupdates_snoc)
+  
+
+
+lemma ntimes_closed_form_list_elem_shape:
+  shows "\<forall>r' \<in> set (map (optermsimp r) (nupdates s r [Some ([c], n)])). 
+r' = RZERO \<or> (\<exists>s' m. r' = RSEQ (rders_simp r s') (RNTIMES r m) \<and> m \<le> n)"
+  apply(insert opterm_optlist_result_shape2)
+  apply(case_tac s)
+   apply(auto)
+  apply (metis rders_simp_one_char)
+  by (metis case_prod_conv nupdates.simps(2) nupdates_n_leq_n option.simps(4) option.simps(5))
+
+
+lemma ntimes_trivial1:
+  shows "rsize RZERO \<le> N + rsize (RNTIMES r n)"
+  by simp
+
+
+lemma ntimes_trivial20:
+  shows "m \<le> n \<Longrightarrow> rsize (RNTIMES r m) \<le> rsize (RNTIMES r n)"
+  by simp
+
+
+lemma ntimes_trivial2:
+  assumes "\<forall>s. rsize (rders_simp r s) \<le> N"
+  shows "    r' = RSEQ (rders_simp r s1) (RNTIMES r m) \<and> m \<le> n
+       \<Longrightarrow> rsize r' \<le> Suc (N + rsize (RNTIMES r n))"
+  apply simp
+  by (simp add: add_mono_thms_linordered_semiring(1) assms)
+
+lemma ntimes_closed_form_list_elem_bounded:
+  assumes "\<forall>s. rsize (rders_simp r s) \<le> N"
+  shows "\<forall>r' \<in>  set  (map (optermsimp r) (nupdates s r [Some ([c], n)])). rsize r' \<le> Suc (N + rsize (RNTIMES r n))"
+  apply(rule ballI)
+  apply(subgoal_tac  "r' = RZERO \<or> (\<exists>s' m. r' = RSEQ (rders_simp r s') (RNTIMES r m) \<and> m \<le> n)")
+  prefer 2
+  using ntimes_closed_form_list_elem_shape apply blast
+  apply(case_tac "r' = RZERO")
+  using le_SucI ntimes_trivial1 apply presburger
+  apply(subgoal_tac "\<exists>s1 m. r' = RSEQ (rders_simp r s1) (RNTIMES r m) \<and> m \<le> n")
+  apply(erule exE)+
+  using assms ntimes_trivial2 apply presburger
+  by blast
+
+
+lemma P_holds_after_distinct:
+  assumes "\<forall>r \<in> set rs. P r"
+  shows "\<forall>r \<in> set (rdistinct rs rset). P r"
+  by (simp add: assms rdistinct_set_equality1)
+
+lemma ntimes_control_bounded:
+  assumes "\<forall>s. rsize (rders_simp r s) \<le> N"
+  shows "rsizes (rdistinct (map (optermsimp r) (nupdates s r [Some ([c], n)])) {}) 
+     \<le> (card (sizeNregex (Suc (N + rsize (RNTIMES r n))))) * (Suc (N + rsize (RNTIMES r n)))"
+  apply(subgoal_tac "\<forall>r' \<in> set (rdistinct (map (optermsimp r) (nupdates s r [Some ([c], n)])) {}).
+          rsize r' \<le> Suc (N + rsize (RNTIMES r n))")
+   apply (meson distinct_list_rexp_upto rdistinct_same_set)
+  apply(subgoal_tac "\<forall>r' \<in> set (map (optermsimp r) (nupdates s r [Some ([c], n)])). rsize r' \<le> Suc (N + rsize (RNTIMES r n))")
+   apply (simp add: rdistinct_set_equality)
+  by (metis assms nat_le_linear not_less_eq_eq ntimes_closed_form_list_elem_bounded)
+
+
+
+lemma ntimes_closed_form_bounded0:
+  assumes "\<forall>s. rsize (rders_simp r s) \<le> N"
+  shows " (rders_simp (RNTIMES r 0) s)  = RZERO \<or> (rders_simp (RNTIMES r 0) s)  = RNTIMES r 0
+           "
+  apply(induct s)
+   apply simp
+  by (metis always0 list.simps(3) rder.simps(7) rders.simps(2) rders_simp_same_simpders rsimp.simps(3))
+
+lemma ntimes_closed_form_bounded1:
+  assumes "\<forall>s. rsize (rders_simp r s) \<le> N"
+  shows " rsize (rders_simp (RNTIMES r 0) s) \<le> max (rsize  RZERO) (rsize (RNTIMES r 0))"
+  
+  by (metis assms max.cobounded1 max.cobounded2 ntimes_closed_form_bounded0)
+
+lemma self_smaller_than_bound:
+  shows "\<forall>s. rsize (rders_simp r s) \<le> N \<Longrightarrow> rsize r \<le> N"
+  apply(drule_tac x = "[]" in spec)
+  apply simp
+  done
+
+lemma ntimes_closed_form_bounded_nil_aux:
+  shows "max (rsize  RZERO) (rsize (RNTIMES r 0)) = 1 + rsize r"
+  by auto
+
+lemma ntimes_closed_form_bounded_nil:
+  assumes "\<forall>s. rsize (rders_simp r s) \<le> N"
+  shows " rsize (rders_simp (RNTIMES r 0) s) \<le> 1 + rsize r"
+  using assms ntimes_closed_form_bounded1 by auto
+
+lemma ntimes_ineq1:
+  shows "(rsize (RNTIMES r n)) \<ge> 1 + rsize r"
+  by simp
+
+lemma ntimes_ineq2:
+  shows "1 + rsize r \<le>  
+max ((Suc (card (sizeNregex (Suc (N + rsize (RNTIMES r n))))) * (Suc (N + rsize (RNTIMES r n))))) (rsize (RNTIMES r n))"
+  by (meson le_max_iff_disj ntimes_ineq1)
+
+lemma ntimes_closed_form_bounded:
+  assumes "\<forall>s. rsize (rders_simp r s) \<le> N"
+  shows "rsize (rders_simp (RNTIMES r (Suc n)) s) \<le> 
+           max ((Suc (card (sizeNregex (Suc (N + rsize (RNTIMES r n))))) * (Suc (N + rsize (RNTIMES r n))))) (rsize (RNTIMES r n))"
+proof(cases s)
+  case Nil
+  then show "rsize (rders_simp (RNTIMES r (Suc n)) s)
+    \<le> max (Suc (card (sizeNregex (Suc (N + rsize (RNTIMES r n))))) * Suc (N + rsize (RNTIMES r n))) (rsize (RNTIMES r n))" 
+    by simp
+next
+  case (Cons a list)
+
+  then have "rsize (rders_simp (RNTIMES r (Suc n)) s) = 
+             rsize (rsimp (RALTS ((map (optermsimp r)    (nupdates list r [Some ([a], n)])))))"
+    using ntimes_closed_form by fastforce
+  also have "... \<le> Suc (rsizes (rdistinct ((map (optermsimp r) (nupdates list r [Some ([a], n)]))) {}))"
+    using alts_simp_control by blast 
+  also have "... \<le> Suc (card (sizeNregex (Suc (N + rsize (RNTIMES r n))))) * (Suc (N + rsize (RNTIMES r n)))" 
+    using ntimes_control_bounded[OF assms]
+    by (metis add_mono le_add1 mult_Suc plus_1_eq_Suc)
+  also have "... \<le> max (Suc (card (sizeNregex (Suc (N + rsize (RNTIMES r n))))) * Suc (N + rsize (RNTIMES r n))) (rsize (RNTIMES r n))"
+    by simp    
+  finally show ?thesis by simp  
+qed
+
+
+lemma ntimes_closed_form_boundedA:
+  assumes "\<forall>s. rsize (rders_simp r s) \<le> N"
+  shows "\<exists>N'. \<forall>s. rsize (rders_simp (RNTIMES r n) s) \<le> N'"
+  apply(case_tac n)
+  using assms ntimes_closed_form_bounded_nil apply blast
+  using assms ntimes_closed_form_bounded by blast
+
+
+lemma star_closed_form_nonempty_bounded:
+  assumes "\<forall>s. rsize (rders_simp r s) \<le> N" and "s \<noteq> []"
+  shows "rsize (rders_simp (RSTAR r) s) \<le> 
+            ((Suc (card (sizeNregex (Suc (N + rsize (RSTAR r))))) * (Suc (N + rsize (RSTAR r))))) "
+proof(cases s)
+  case Nil
+  then show ?thesis 
+    using local.Nil by fastforce
+next
+  case (Cons a list)
+  then have "rsize (rders_simp (RSTAR r) s) = 
+    rsize (rsimp (RALTS ((map (\<lambda>s1. RSEQ (rders_simp r s1) (RSTAR r)) (star_updates list r [[a]])))))"
+    using star_closed_form by fastforce
+  also have "... \<le> Suc (rsizes (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r s1) (RSTAR r)) (star_updates list r [[a]])) {}))"
+    using alts_simp_control by blast 
+  also have "... \<le> Suc (card (sizeNregex (Suc (N + rsize (RSTAR r))))) * (Suc (N + rsize (RSTAR r)))" 
+    by (smt (z3) add_mono_thms_linordered_semiring(1) assms(1) le_add1 map_eq_conv mult_Suc plus_1_eq_Suc star_control_bounded)
+  also have "... \<le> max (Suc (card (sizeNregex (Suc (N + rsize (RSTAR r))))) * Suc (N + rsize (RSTAR r))) (rsize (RSTAR r))"
+    by simp    
+  finally show ?thesis by simp  
+qed
+
+
+
 lemma seq_estimate_bounded: 
   assumes "\<forall>s. rsize (rders_simp r1 s) \<le> N1" 
       and "\<forall>s. rsize (rders_simp r2 s) \<le> N2"
@@ -425,7 +664,6 @@
     by auto 
 qed
 
-
 lemma rders_simp_bounded: 
   shows "\<exists>N. \<forall>s. rsize (rders_simp r s) \<le> N"
   apply(induct r)
@@ -440,9 +678,12 @@
   apply(assumption)
   apply(assumption)
   apply (metis alts_closed_form_bounded size_list_estimation')
-  using star_closed_form_bounded by blast
+  using star_closed_form_bounded apply blast
+  using ntimes_closed_form_boundedA by blast
+  
+  
+unused_thms
+export_code rders_simp rsimp rder in Scala module_name Example
 
 
-unused_thms
-
 end




