diff -r cf7a5c863831 -r 6c13f76c070b thys3/ClosedFormsBounds.thy --- a/thys3/ClosedFormsBounds.thy Wed Feb 15 11:52:22 2023 +0000 +++ b/thys3/ClosedFormsBounds.thy Thu Feb 16 23:23:22 2023 +0000 @@ -2,8 +2,6 @@ theory ClosedFormsBounds 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) @@ -16,12 +14,6 @@ apply simp by simp -lemma distinct_list_size_len_bounded: - assumes "\r \ set rs. rsize r \ N" "length rs \ lrs" - shows "rsizes rs \ lrs * N " - using assms - by (metis rlist_bound dual_order.trans mult.commute mult_le_mono1) - lemma alts_closed_form_bounded: assumes "\r \ set rs. \s. rsize (rders_simp r s) \ N" shows "rsize (rders_simp (RALTS rs) s) \ max (Suc (N * (length rs))) (rsize (RALTS rs))" @@ -149,7 +141,7 @@ apply(simp only:) apply(subgoal_tac "rsizes (rdistinct rs (insert RZERO (insert RONE noalts_set \ alts_set))) \ rsizes (RONE # rdistinct rs (insert RZERO (insert RONE noalts_set \ 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 @@ -159,8 +151,8 @@ using rflts.simps(4) apply presburger apply simp apply(subgoal_tac "insert RONE (noalts_set \ corr_set) = (insert RONE noalts_set) \ 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 \ noalts_set") apply simp @@ -182,14 +174,14 @@ apply(subgoal_tac "(insert a (noalts_set \ alts_set)) = (insert a noalts_set) \ alts_set") apply(simp only:) apply(subgoal_tac "noalts_set \ corr_set = (insert a noalts_set) \ 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 \ noalts_set") apply simp apply(subgoal_tac "a \ alts_set") @@ -212,14 +204,13 @@ apply(subgoal_tac "noalts_set \ corr_set = (insert a noalts_set) \ 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 \ noalts_set") @@ -242,16 +233,42 @@ apply(subgoal_tac "(insert a (noalts_set \ alts_set)) = (insert a noalts_set) \ alts_set") apply(simp only:) apply(subgoal_tac "noalts_set \ corr_set = (insert a noalts_set) \ 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 \ noalts_set") + apply simp + apply(subgoal_tac "a \ alts_set") + prefer 2 + apply blast + apply(case_tac "a \ corr_set") + apply(subgoal_tac "noalts_set \ corr_set = insert a ( noalts_set \ corr_set)") + prefer 2 + apply fastforce + apply(simp only:) + apply(subgoal_tac "rsizes (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \ alts_set))) \ + rsizes (rdistinct (a # rs) (insert RZERO (noalts_set \ alts_set)))") + + apply(subgoal_tac "rsizes (rdistinct (rflts (a # rs)) ((insert a noalts_set) \ corr_set)) \ + rsizes (rdistinct (a # rs) (insert RZERO ((insert a noalts_set) \ alts_set)))") + apply fastforce + apply simp + apply(subgoal_tac "(insert a (noalts_set \ alts_set)) = (insert a noalts_set) \ alts_set") + apply(simp only:) + apply(subgoal_tac "noalts_set \ corr_set = (insert a noalts_set) \ 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: @@ -318,6 +335,11 @@ by (simp add: larger_acc_smaller_distinct_res) +lemma distinct_list_size_len_bounded: + assumes "\r \ set rs. rsize r \ N" "length rs \ lrs" + shows "rsizes rs \ lrs * N " + using assms + by (metis rlist_bound dual_order.trans mult.commute mult_le_mono1) @@ -382,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 "\opt \ set (nupdate c r optlist). opt = None \ (\s n. opt = Some (s, n))" + using nonempty_string.cases by auto + +lemma nupdates_elems: + shows "\opt \ set (nupdates s r optlist). opt = None \ (\s n. opt = Some (s, n))" + by (meson nonempty_string.cases) + + +lemma opterm_optlist_result_shape: + shows "\r' \ set (map (optermsimp r) optlist). r' = RZERO \ (\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 "\optlist. \r' \ set (map (optermsimp r) optlist). r' = RZERO \ (\s m. r' = RSEQ (rders_simp r s) (RNTIMES r m))" + using opterm_optlist_result_shape by presburger + + +lemma nupdate_n_leq_n: + shows "\r \ set (nupdate c' r [Some ([c], n)]). r = None \( \s' m. r = Some (s', m) \ m \ n)" + apply(case_tac n) + apply simp + apply simp + done +(* +lemma nupdate_induct_leqn: + shows "\\opt \ set optlist. opt = None \ (\s' m. opt = Some(s', m) \ m \ n) \ \ + \opt \ set (nupdate c' r optlist). opt = None \ (\s' m. opt = Some (s', m) \ m \ n)" + apply (case_tac optlist) + apply simp + apply(case_tac a) + apply simp + sledgehammer +*) + + +lemma nupdates_n_leq_n: + shows "\r \ set (nupdates s r [Some ([c], n)]). r = None \( \s' m. r = Some (s', m) \ m \ 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 "\r' \ set (map (optermsimp r) (nupdates s r [Some ([c], n)])). +r' = RZERO \ (\s' m. r' = RSEQ (rders_simp r s') (RNTIMES r m) \ m \ 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 \ N + rsize (RNTIMES r n)" + by simp + + +lemma ntimes_trivial20: + shows "m \ n \ rsize (RNTIMES r m) \ rsize (RNTIMES r n)" + by simp + + +lemma ntimes_trivial2: + assumes "\s. rsize (rders_simp r s) \ N" + shows " r' = RSEQ (rders_simp r s1) (RNTIMES r m) \ m \ n + \ rsize r' \ 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 "\s. rsize (rders_simp r s) \ N" + shows "\r' \ set (map (optermsimp r) (nupdates s r [Some ([c], n)])). rsize r' \ Suc (N + rsize (RNTIMES r n))" + apply(rule ballI) + apply(subgoal_tac "r' = RZERO \ (\s' m. r' = RSEQ (rders_simp r s') (RNTIMES r m) \ m \ 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 "\s1 m. r' = RSEQ (rders_simp r s1) (RNTIMES r m) \ m \ n") + apply(erule exE)+ + using assms ntimes_trivial2 apply presburger + by blast + + +lemma P_holds_after_distinct: + assumes "\r \ set rs. P r" + shows "\r \ set (rdistinct rs rset). P r" + by (simp add: assms rdistinct_set_equality1) + +lemma ntimes_control_bounded: + assumes "\s. rsize (rders_simp r s) \ N" + shows "rsizes (rdistinct (map (optermsimp r) (nupdates s r [Some ([c], n)])) {}) + \ (card (sizeNregex (Suc (N + rsize (RNTIMES r n))))) * (Suc (N + rsize (RNTIMES r n)))" + apply(subgoal_tac "\r' \ set (rdistinct (map (optermsimp r) (nupdates s r [Some ([c], n)])) {}). + rsize r' \ Suc (N + rsize (RNTIMES r n))") + apply (meson distinct_list_rexp_upto rdistinct_same_set) + apply(subgoal_tac "\r' \ set (map (optermsimp r) (nupdates s r [Some ([c], n)])). rsize r' \ 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 "\s. rsize (rders_simp r s) \ N" + shows " (rders_simp (RNTIMES r 0) s) = RZERO \ (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 "\s. rsize (rders_simp r s) \ N" + shows " rsize (rders_simp (RNTIMES r 0) s) \ max (rsize RZERO) (rsize (RNTIMES r 0))" + + by (metis assms max.cobounded1 max.cobounded2 ntimes_closed_form_bounded0) + +lemma self_smaller_than_bound: + shows "\s. rsize (rders_simp r s) \ N \ rsize r \ 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 "\s. rsize (rders_simp r s) \ N" + shows " rsize (rders_simp (RNTIMES r 0) s) \ 1 + rsize r" + using assms ntimes_closed_form_bounded1 by auto + +lemma ntimes_ineq1: + shows "(rsize (RNTIMES r n)) \ 1 + rsize r" + by simp + +lemma ntimes_ineq2: + shows "1 + rsize r \ +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 "\s. rsize (rders_simp r s) \ N" + shows "rsize (rders_simp (RNTIMES r (Suc n)) s) \ + 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) + \ 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 "... \ Suc (rsizes (rdistinct ((map (optermsimp r) (nupdates list r [Some ([a], n)]))) {}))" + using alts_simp_control by blast + also have "... \ 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 "... \ 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 "\s. rsize (rders_simp r s) \ N" + shows "\N'. \s. rsize (rders_simp (RNTIMES r n) s) \ 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 "\s. rsize (rders_simp r s) \ N" and "s \ []" + shows "rsize (rders_simp (RSTAR r) s) \ + ((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 (\s1. RSEQ (rders_simp r s1) (RSTAR r)) (star_updates list r [[a]])))))" + using star_closed_form by fastforce + also have "... \ Suc (rsizes (rdistinct (map (\s1. RSEQ (rders_simp r s1) (RSTAR r)) (star_updates list r [[a]])) {}))" + using alts_simp_control by blast + also have "... \ 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 "... \ 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 "\s. rsize (rders_simp r1 s) \ N1" and "\s. rsize (rders_simp r2 s) \ N2" @@ -428,7 +664,6 @@ by auto qed - lemma rders_simp_bounded: shows "\N. \s. rsize (rders_simp r s) \ N" apply(induct r) @@ -443,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