# HG changeset patch # User Chengsong # Date 1647093897 0 # Node ID 09d7cd8e5ef8c7261f54348b179d2f36f56a518a # Parent 3bc0f0069d06313d0b027ed0ec948dbf76e8b2fd more diff -r 3bc0f0069d06 -r 09d7cd8e5ef8 thys2/ClosedFormsBounds.thy --- 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 "\r \ set (map (\r. rders_simp r ( s)) rs ). \r1 \ set rs. r = rders_simp r1 s" + by (simp add: image_iff) + + + +lemma rlist_bound: + shows "\r \ set rs. rsize r \ N \ sum_list (map rsize rs) \ N * (length rs)" + apply(induct rs) + apply simp + by simp lemma alts_closed_form_bounded: shows "\r \ set rs. \s. rsize(rders_simp r s ) \ N \ -rsize (rders_simp (RALTS rs ) s) \ max (Suc ( N * (card (sizeNregex N)))) (rsize (RALTS rs) )" +rsize (rders_simp (RALTS rs ) s) \ 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 (\s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) - (star_updates s r0 [[c]]) ) ))) \ - Suc (sum_list (map rsize (rdistinct (map (\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 "\r\ set rs. (rsize r ) \ N \ sum_list (map rsize (rdistinct rs {})) \ - (card (sizeNregex N))* N" - - sorry - - -lemma star_lambda_ders: - shows " \s. rsize (rders_simp r0 s) \ N \ - \r\set (map (\s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) (star_updates s r0 [[c]])). - rsize r \ Suc (N + rsize (RSTAR r0))" - sorry - - -lemma star_control_bounded: - shows "\s. rsize (rders_simp r0 s) \ N \ - (sum_list (map rsize (rdistinct (map (\s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) - (star_updates s r0 [[c]]) ) {}) ) ) \ -(card (sizeNregex (Suc (N + rsize (RSTAR r0))))) * (Suc (N + rsize (RSTAR r0))) -" - apply(subgoal_tac "\r \ set (map (\s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) - (star_updates s r0 [[c]]) ). (rsize r ) \ Suc (N + rsize (RSTAR r0))") + apply(subst alts_closed_form_variant) + apply force + apply(subgoal_tac "rsize (rsimp (RALTS (map (\r. rders_simp r (a # s)) rs))) \ rsize ( (RALTS (map (\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 "\s. rsize (rders_simp r0 s) \ N" - shows"Suc - (sum_list (map rsize (rdistinct (map (\s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) - (star_updates list r0 [[a]])) {}))) -\ (Suc (card (sizeNregex (Suc (N + rsize (RSTAR r0))))) * Suc (N + rsize (RSTAR r0))) " - apply(subgoal_tac "(sum_list (map rsize (rdistinct (map (\s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) - (star_updates list r0 [[a]])) {}))) -\ ( (card (sizeNregex (Suc (N + rsize (RSTAR r0))))) * Suc (N + rsize (RSTAR r0))) ") + using rsimp_mono apply presburger + apply(subgoal_tac "rsize (RALTS (map (\r. rders_simp r (a # s)) rs)) = + Suc (sum_list (map rsize (map (\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 (\r. rders_simp r (a # s)) rs )) \ N * (length rs) ") + apply linarith + apply(subgoal_tac "\r \ set (map (\r. rders_simp r (a # s)) rs ). rsize r \ N") + prefer 2 + apply(subgoal_tac "\r \ set (map (\r. rders_simp r (a # s)) rs ). \r1 \ 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 "\s. rsize (rders_simp r0 s) \ N \ - rsize (rders_simp (RSTAR r0) s) \ -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 (\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 (\s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) (star_updates list r0 [[a]]) ) ))) -\ Suc (sum_list (map rsize (rdistinct (map (\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 (\s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) (star_updates list r0 [[a]])) {}))) -\ (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)) \ 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 \ a \ (r \ set (rdistinct rs {})) = (r \ set (rdistinct rs {a}))" + sorry + + + lemma flts_vs_nflts: shows "\r \ noalts_set. \xs. r \ RALTS xs \ (\a \ alts_set. \xs. a = RALTS xs \ set xs \ corr_set) @@ -108,6 +67,12 @@ sorry +lemma distinct_simp_ineq_general: + shows "rsimp ` no_simp = has_simp \Suc (sum_list (map rsize (rdistinct (map rsimp rs) has_simp))) + \ Suc (sum_list (map rsize (rdistinct rs no_simp)))" + + sorry + lemma without_flts_ineq: shows " Suc (sum_list (map rsize (rdistinct (rflts rs) {}) )) \ @@ -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 \Suc (sum_list (map rsize (rdistinct (map rsimp rs) has_simp))) - \ 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)))) - \ 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 \ ss \ 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) \ \ (set ((a::nat) # as)) = a + \ (set as)" + by simp + + +lemma distinct_list_sizeNregex_bounded: + shows "distinct rs \ (\ r \ (set rs). rsize r \ N) \ sum_list (map rsize rs) \ N * length rs" + apply(induct rs) + apply simp + by simp + + +lemma distinct_list_size_len_bounded: + shows "distinct rs \ (\r \ set rs. rsize r \ N) \ length rs \ lrs \ sum_list (map rsize rs) \ lrs * N " + by (metis distinct_list_sizeNregex_bounded dual_order.trans mult.commute mult_le_mono1) + + + +lemma rdistinct_same_set: + shows "(r \ set rs) = (r \ set (rdistinct rs {}))" + apply(induct rs) + apply simp + apply(case_tac "a \ 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 "\r\ set rs. (rsize r ) \ N \ sum_list (map rsize (rdistinct rs {})) \ + (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 {}) \ 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 "\r \ set (rdistinct rs {}). rsize r \ 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 (\s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) + (star_updates s r0 [[c]]) ) ))) \ + Suc (sum_list (map rsize (rdistinct (map (\s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) + (star_updates s r0 [[c]]) ) {}) ) )" + by (metis alts_simp_control ) + + + + +lemma star_lambda_form: + shows "\ r \ set (map (\s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) ls). + \s2. r = RSEQ (rders_simp r0 s2) (RSTAR r0) " + by (meson ex_map_conv) + + +lemma star_lambda_ders: + shows " \s. rsize (rders_simp r0 s) \ N \ + \r\set (map (\s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) (star_updates s r0 [[c]])). + rsize r \ Suc (N + rsize (RSTAR r0))" + apply(insert star_lambda_form) + apply(simp) + done + + + + +lemma star_control_bounded: + shows "\s. rsize (rders_simp r0 s) \ N \ + (sum_list (map rsize (rdistinct (map (\s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) + (star_updates s r0 [[c]]) ) {}) ) ) \ +(card (sizeNregex (Suc (N + rsize (RSTAR r0))))) * (Suc (N + rsize (RSTAR r0))) +" + apply(subgoal_tac "\r \ set (map (\s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) + (star_updates s r0 [[c]]) ). (rsize r ) \ 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 "\s. rsize (rders_simp r0 s) \ N" + shows"Suc + (sum_list (map rsize (rdistinct (map (\s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) + (star_updates list r0 [[a]])) {}))) +\ (Suc (card (sizeNregex (Suc (N + rsize (RSTAR r0))))) * Suc (N + rsize (RSTAR r0))) " + apply(subgoal_tac "(sum_list (map rsize (rdistinct (map (\s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) + (star_updates list r0 [[a]])) {}))) +\ ( (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 "\s. rsize (rders_simp r0 s) \ N \ + rsize (rders_simp (RSTAR r0) s) \ +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 (\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 (\s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) (star_updates list r0 [[a]]) ) ))) +\ Suc (sum_list (map rsize (rdistinct (map (\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 (\s1. RSEQ (rders_simp r0 s1) (RSTAR r0)) (star_updates list r0 [[a]])) {}))) +\ (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)))) + \ 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 "\s. rsize (rders_simp r2 s) \ N2 \ \r \ set (rdistinct (map (rders_simp r2) Ss) {}). rsize r \ N2"