--- a/thys2/ClosedFormsBounds.thy Fri Mar 11 23:32:44 2022 +0000
+++ b/thys2/ClosedFormsBounds.thy Sat Mar 12 14:04:57 2022 +0000
@@ -3,92 +3,44 @@
imports "GeneralRegexBound" "ClosedForms"
begin
+lemma alts_ders_lambda_shape_ders:
+ shows "\<forall>r \<in> set (map (\<lambda>r. rders_simp r ( s)) rs ). \<exists>r1 \<in> set rs. r = rders_simp r1 s"
+ by (simp add: image_iff)
+
+
+
+lemma rlist_bound:
+ shows "\<forall>r \<in> set rs. rsize r \<le> N \<Longrightarrow> sum_list (map rsize rs) \<le> N * (length rs)"
+ apply(induct rs)
+ apply simp
+ by simp
lemma alts_closed_form_bounded: shows
"\<forall>r \<in> set rs. \<forall>s. rsize(rders_simp r s ) \<le> N \<Longrightarrow>
-rsize (rders_simp (RALTS rs ) s) \<le> max (Suc ( N * (card (sizeNregex N)))) (rsize (RALTS rs) )"
+rsize (rders_simp (RALTS rs ) s) \<le> max (Suc ( N * (length rs))) (rsize (RALTS rs) )"
apply(induct s)
apply simp
- apply(insert alts_closed_form_variant)
-
-
- sorry
-
-
-
-lemma star_closed_form_bounded_by_rdistinct_list_estimate:
- shows "rsize (rsimp ( RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) )
- (star_updates s r0 [[c]]) ) ))) \<le>
- Suc (sum_list (map rsize (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) )
- (star_updates s r0 [[c]]) ) {}) ) )"
-
- sorry
-
-lemma distinct_list_rexp_up_to_certain_size_bouded_by_set_enumerating_up_to_that_size:
- shows "\<forall>r\<in> set rs. (rsize r ) \<le> N \<Longrightarrow> sum_list (map rsize (rdistinct rs {})) \<le>
- (card (sizeNregex N))* N"
-
- 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)))
-"
- 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))")
+ apply(subst alts_closed_form_variant)
+ apply force
+ apply(subgoal_tac "rsize (rsimp (RALTS (map (\<lambda>r. rders_simp r (a # s)) rs))) \<le> rsize ( (RALTS (map (\<lambda>r. rders_simp r (a # s)) rs)))")
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"
- shows"Suc
- (sum_list (map rsize (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0))
- (star_updates list r0 [[a]])) {})))
-\<le> (Suc (card (sizeNregex (Suc (N + rsize (RSTAR r0))))) * Suc (N + rsize (RSTAR r0))) "
- apply(subgoal_tac "(sum_list (map rsize (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0))
- (star_updates list r0 [[a]])) {})))
-\<le> ( (card (sizeNregex (Suc (N + rsize (RSTAR r0))))) * Suc (N + rsize (RSTAR r0))) ")
+ using rsimp_mono apply presburger
+ apply(subgoal_tac "rsize (RALTS (map (\<lambda>r. rders_simp r (a # s)) rs)) =
+ Suc (sum_list (map rsize (map (\<lambda>r. rders_simp r (a # s)) rs)))")
prefer 2
- using assms star_control_bounded apply presburger
- by simp
-
-
+ using rsize.simps(4) apply blast
+ apply(subgoal_tac "sum_list (map rsize (map (\<lambda>r. rders_simp r (a # s)) rs )) \<le> N * (length rs) ")
+ apply linarith
+ apply(subgoal_tac "\<forall>r \<in> set (map (\<lambda>r. rders_simp r (a # s)) rs ). rsize r \<le> N")
+ prefer 2
+ apply(subgoal_tac "\<forall>r \<in> set (map (\<lambda>r. rders_simp r (a # s)) rs ). \<exists>r1 \<in> set rs. r = rders_simp r1 (a # s)")
+ prefer 2
+ using alts_ders_lambda_shape_ders apply presburger
+ apply metis
+ apply(frule rlist_bound)
+ by fastforce
-lemma star_closed_form_bounded:
- shows "\<forall>s. rsize (rders_simp r0 s) \<le> N \<Longrightarrow>
- rsize (rders_simp (RSTAR r0) s) \<le>
-max ( (Suc (card (sizeNregex (Suc (N + rsize (RSTAR r0))))) * (Suc (N + rsize (RSTAR r0))))) (rsize (RSTAR r0))"
- apply(case_tac s)
- apply simp
- apply(subgoal_tac " rsize (rders_simp (RSTAR r0) (a # list)) =
-rsize (rsimp ( RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) (star_updates list r0 [[a]]) ) )))")
- prefer 2
- using star_closed_form apply presburger
- apply(subgoal_tac "rsize (rsimp (
- RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) (star_updates list r0 [[a]]) ) )))
-\<le> Suc (sum_list (map rsize (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) )
- (star_updates list r0 [[a]]) ) {}) ) )")
- prefer 2
- using star_closed_form_bounded_by_rdistinct_list_estimate apply presburger
- apply(subgoal_tac "Suc (sum_list
- (map rsize
- (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) (star_updates list r0 [[a]])) {})))
-\<le> (Suc (card (sizeNregex (Suc (N + rsize (RSTAR r0))))) * Suc (N + rsize (RSTAR r0))) ")
- 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)) {})))"
@@ -96,8 +48,15 @@
lemma flts_has_no_zero:
shows "rdistinct (rflts rs) rset = rdistinct (rflts rs) (insert RZERO rset)"
+
sorry
+lemma not_mentioned_elem_distinct:
+ shows "r \<noteq> a \<Longrightarrow> (r \<in> set (rdistinct rs {})) = (r \<in> set (rdistinct rs {a}))"
+ 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)
@@ -108,6 +67,12 @@
sorry
+lemma distinct_simp_ineq_general:
+ shows "rsimp ` no_simp = has_simp \<Longrightarrow>Suc (sum_list (map rsize (rdistinct (map rsimp rs) has_simp)))
+ \<le> Suc (sum_list (map rsize (rdistinct rs no_simp)))"
+
+ sorry
+
lemma without_flts_ineq:
shows " Suc (sum_list (map rsize (rdistinct (rflts rs) {}) )) \<le>
@@ -115,10 +80,6 @@
by (metis empty_iff flts_vs_nflts sup_bot_left)
-lemma distinct_simp_ineq_general:
- shows "rsimp ` no_simp = has_simp \<Longrightarrow>Suc (sum_list (map rsize (rdistinct (map rsimp rs) has_simp)))
- \<le> Suc (sum_list (map rsize (rdistinct rs no_simp)))"
- sorry
lemma distinct_simp_ineq:
@@ -145,12 +106,6 @@
-
-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 rdistinct_equality1:
shows "a \<notin> ss \<Longrightarrow> rdistinct (a # rs) ss = a # rdistinct rs (insert a ss) "
by auto
@@ -211,6 +166,149 @@
apply(rule same_regex_property_after_map)
by simp
+
+
+lemma Sum_cons:
+ shows "distinct (a # as) \<Longrightarrow> \<Sum> (set ((a::nat) # as)) = a + \<Sum> (set as)"
+ by simp
+
+
+lemma distinct_list_sizeNregex_bounded:
+ shows "distinct rs \<and> (\<forall> r \<in> (set rs). rsize r \<le> N) \<Longrightarrow> sum_list (map rsize rs) \<le> N * length rs"
+ apply(induct rs)
+ apply simp
+ by simp
+
+
+lemma distinct_list_size_len_bounded:
+ shows "distinct rs \<and> (\<forall>r \<in> set rs. rsize r \<le> N) \<and> length rs \<le> lrs \<Longrightarrow> sum_list (map rsize rs) \<le> lrs * N "
+ by (metis distinct_list_sizeNregex_bounded dual_order.trans mult.commute mult_le_mono1)
+
+
+
+lemma rdistinct_same_set:
+ shows "(r \<in> set rs) = (r \<in> set (rdistinct rs {}))"
+ apply(induct rs)
+ apply simp
+ apply(case_tac "a \<in> set rs")
+ apply(case_tac "r = a")
+ apply (simp)
+ apply (simp add: not_mentioned_elem_distinct)
+ using not_mentioned_elem_distinct by fastforce
+
+
+
+lemma distinct_list_rexp_up_to_certain_size_bouded_by_set_enumerating_up_to_that_size:
+ shows "\<forall>r\<in> set rs. (rsize r ) \<le> N \<Longrightarrow> sum_list (map rsize (rdistinct rs {})) \<le>
+ (card (sizeNregex N))* N"
+ apply(subgoal_tac "distinct (rdistinct rs {})")
+ prefer 2
+ using rdistinct_does_the_job apply blast
+ apply(subgoal_tac "length (rdistinct rs {}) \<le> card (sizeNregex N)")
+ apply(rule distinct_list_size_len_bounded)
+ apply(rule conjI)+
+ apply simp
+ apply(rule conjI)
+ apply (meson rdistinct_same_set)
+ apply blast
+ apply(subgoal_tac "\<forall>r \<in> set (rdistinct rs {}). rsize r \<le> N")
+ prefer 2
+ apply (meson rdistinct_same_set)
+ apply(subgoal_tac "length (rdistinct rs {}) = card (set (rdistinct rs {}))")
+ prefer 2
+ using set_related_list apply blast
+ apply(simp only:)
+ by (metis card_mono finite_size_n mem_Collect_eq sizeNregex_def subset_code(1))
+
+
+
+
+
+
+lemma star_closed_form_bounded_by_rdistinct_list_estimate:
+ shows "rsize (rsimp ( RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) )
+ (star_updates s r0 [[c]]) ) ))) \<le>
+ Suc (sum_list (map rsize (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) )
+ (star_updates s r0 [[c]]) ) {}) ) )"
+ by (metis alts_simp_control )
+
+
+
+
+lemma star_lambda_form:
+ shows "\<forall> r \<in> set (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) ls).
+ \<exists>s2. r = RSEQ (rders_simp r0 s2) (RSTAR r0) "
+ by (meson ex_map_conv)
+
+
+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))"
+ apply(insert star_lambda_form)
+ apply(simp)
+ done
+
+
+
+
+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)))
+"
+ 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"
+ shows"Suc
+ (sum_list (map rsize (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0))
+ (star_updates list r0 [[a]])) {})))
+\<le> (Suc (card (sizeNregex (Suc (N + rsize (RSTAR r0))))) * Suc (N + rsize (RSTAR r0))) "
+ apply(subgoal_tac "(sum_list (map rsize (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0))
+ (star_updates list r0 [[a]])) {})))
+\<le> ( (card (sizeNregex (Suc (N + rsize (RSTAR r0))))) * Suc (N + rsize (RSTAR r0))) ")
+ prefer 2
+ using assms star_control_bounded apply presburger
+ by simp
+
+
+
+lemma star_closed_form_bounded:
+ shows "\<forall>s. rsize (rders_simp r0 s) \<le> N \<Longrightarrow>
+ rsize (rders_simp (RSTAR r0) s) \<le>
+max ( (Suc (card (sizeNregex (Suc (N + rsize (RSTAR r0))))) * (Suc (N + rsize (RSTAR r0))))) (rsize (RSTAR r0))"
+ apply(case_tac s)
+ apply simp
+ apply(subgoal_tac " rsize (rders_simp (RSTAR r0) (a # list)) =
+rsize (rsimp ( RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) (star_updates list r0 [[a]]) ) )))")
+ prefer 2
+ using star_closed_form apply presburger
+ apply(subgoal_tac "rsize (rsimp (
+ RALTS ( (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) (star_updates list r0 [[a]]) ) )))
+\<le> Suc (sum_list (map rsize (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0) )
+ (star_updates list r0 [[a]]) ) {}) ) )")
+ prefer 2
+ using star_closed_form_bounded_by_rdistinct_list_estimate apply presburger
+ apply(subgoal_tac "Suc (sum_list
+ (map rsize
+ (rdistinct (map (\<lambda>s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) (star_updates list r0 [[a]])) {})))
+\<le> (Suc (card (sizeNregex (Suc (N + rsize (RSTAR r0))))) * Suc (N + rsize (RSTAR r0))) ")
+ 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"