# HG changeset patch # User paulson # Date 1715002773 -3600 # Node ID 200107cdd3ace94795120c67770f74402ab1903e # Parent 32d2b96affc790d08316860e4d86f8c4b75f814e Some new simprules – and patches for proofs diff -r 32d2b96affc7 -r 200107cdd3ac src/HOL/Analysis/Arcwise_Connected.thy --- a/src/HOL/Analysis/Arcwise_Connected.thy Sun May 05 15:31:08 2024 +0100 +++ b/src/HOL/Analysis/Arcwise_Connected.thy Mon May 06 14:39:33 2024 +0100 @@ -1103,13 +1103,15 @@ with Suc.prems show ?thesis by auto next case True - show ?thesis proof (cases "even j") + show ?thesis + proof (cases "even j") case True then obtain k where k: "j = 2*k" by (metis evenE) with \0 < j\ have "k > 0" "2 * k < 2 ^ n" using Suc.prems(2) k by auto with k \0 < n\ Suc.IH [of k] show ?thesis - by (simp add: m1_to_3 a41 b43 del: power_Suc) (auto simp: of_nat_diff) + apply (simp add: m1_to_3 a41 b43 del: power_Suc of_nat_diff) + by simp next case False then obtain k where k: "j = 2*k + 1" by (metis oddE) @@ -1145,7 +1147,7 @@ by auto then show ?thesis using Suc.IH [of k] k \0 < k\ - by (simp add: less2n add.commute [of 1] m1_to_3 a41 b43 del: power_Suc) (auto simp: of_nat_diff) + by (simp add: less2n add.commute [of 1] m1_to_3 a41 b43 del: power_Suc of_nat_diff) auto next case False then obtain k where k: "j = 2*k + 1" by (metis oddE) diff -r 32d2b96affc7 -r 200107cdd3ac src/HOL/Analysis/Bochner_Integration.thy --- a/src/HOL/Analysis/Bochner_Integration.thy Sun May 05 15:31:08 2024 +0100 +++ b/src/HOL/Analysis/Bochner_Integration.thy Mon May 06 14:39:33 2024 +0100 @@ -2795,7 +2795,7 @@ have "eventually (\n. x \ X n) sequentially" unfolding filterlim_at_top_ge[where c=x] by auto then show "(\n. indicator {..X n} x *\<^sub>R f x) \ f x" - by (intro tendsto_eventually) (auto split: split_indicator elim!: eventually_mono) + by (intro tendsto_eventually) (auto simp: frequently_def split: split_indicator) qed fix n show "AE x in M. norm (indicator {..X n} x *\<^sub>R f x) \ norm (f x)" by (auto split: split_indicator) diff -r 32d2b96affc7 -r 200107cdd3ac src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Sun May 05 15:31:08 2024 +0100 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Mon May 06 14:39:33 2024 +0100 @@ -3945,7 +3945,7 @@ obtain n where "x - a < real n" using reals_Archimedean2[of "x - a"] .. then have "eventually (\n. ?f n x = ?fR x) sequentially" - by (auto intro!: eventually_sequentiallyI[where c=n] split: split_indicator) + by (auto simp: frequently_def intro!: eventually_sequentiallyI[where c=n] split: split_indicator) then show "(\n. ?f n x) \ ?fR x" by (rule tendsto_eventually) qed (auto simp: nonneg incseq_def le_fun_def split: split_indicator) diff -r 32d2b96affc7 -r 200107cdd3ac src/HOL/Analysis/Further_Topology.thy --- a/src/HOL/Analysis/Further_Topology.thy Sun May 05 15:31:08 2024 +0100 +++ b/src/HOL/Analysis/Further_Topology.thy Mon May 06 14:39:33 2024 +0100 @@ -3310,16 +3310,19 @@ proof (cases "j / n \ 1/2") case True show ?thesis - using \j \ 0 \ \j < n\ True + using \j \ 0\ \j < n\ True by (intro sin_monotone_2pi_le) (auto simp: field_simps intro: order_trans [of _ 0]) next case False then have seq: "sin(pi * j / n) = sin(pi * (n - j) / n)" using \j < n\ by (simp add: algebra_simps diff_divide_distrib of_nat_diff) + show ?thesis - unfolding seq - using \j < n\ False - by (intro sin_monotone_2pi_le) (auto simp: field_simps intro: order_trans [of _ 0]) + unfolding seq + proof (intro sin_monotone_2pi_le) + show "- (pi / 2) \ pi / real n" + by (smt (verit) divide_nonneg_nonneg of_nat_0_le_iff pi_ge_zero) + qed (use \j < n\ False in \auto simp: divide_simps\) qed with sin_less show ?thesis by force qed diff -r 32d2b96affc7 -r 200107cdd3ac src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sun May 05 15:31:08 2024 +0100 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Mon May 06 14:39:33 2024 +0100 @@ -2915,18 +2915,13 @@ have g0: "Dg 0 = g" using \p > 0\ by (auto simp add: Dg_def field_split_simps g_def split: if_split_asm) - { - fix m - assume "p > Suc m" - hence "p - Suc m = Suc (p - Suc (Suc m))" - by auto - hence "real (p - Suc m) * fact (p - Suc (Suc m)) = fact (p - Suc m)" - by auto - } note fact_eq = this + have fact_eq: "real (p - Suc m) * fact (p - Suc (Suc m)) = fact (p - Suc m)" + if "p > Suc m" for m + by (metis Suc_diff_Suc fact_Suc that) have Dg: "\m t. m < p \ a \ t \ t \ b \ (Dg m has_vector_derivative Dg (Suc m) t) (at t within {a..b})" - unfolding Dg_def - by (auto intro!: derivative_eq_intros simp: has_vector_derivative_def fact_eq field_split_simps) + unfolding Dg_def has_vector_derivative_def + by (auto intro!: derivative_eq_intros simp: fact_eq divide_simps simp del: of_nat_diff) let ?sum = "\t. \iR Dg i t *\<^sub>R Df (p - Suc i) t" from sum_prod_derivatives_has_vector_derivative[of _ Dg _ _ _ Df, OF \p > 0\ g0 Dg f0 Df] diff -r 32d2b96affc7 -r 200107cdd3ac src/HOL/Analysis/Homeomorphism.thy --- a/src/HOL/Analysis/Homeomorphism.thy Sun May 05 15:31:08 2024 +0100 +++ b/src/HOL/Analysis/Homeomorphism.thy Mon May 06 14:39:33 2024 +0100 @@ -716,7 +716,7 @@ show "affine {x. i \ x = 0}" by (auto simp: affine_hyperplane) show "aff_dim {x. i \ x = 0} + 1 = int DIM('n)" - using i by clarsimp (metis DIM_positive Suc_pred add.commute of_nat_Suc) + using i by force qed (use i in auto) then obtain f g where fg: "homeomorphism (sphere 0 1 - {i}) {x. i \ x = 0} f g" by (force simp: homeomorphic_def) diff -r 32d2b96affc7 -r 200107cdd3ac src/HOL/Analysis/Kronecker_Approximation_Theorem.thy --- a/src/HOL/Analysis/Kronecker_Approximation_Theorem.thy Sun May 05 15:31:08 2024 +0100 +++ b/src/HOL/Analysis/Kronecker_Approximation_Theorem.thy Mon May 06 14:39:33 2024 +0100 @@ -75,13 +75,16 @@ let ?h = "\i. \b * \ i\ - \a * \ i\" show ?thesis proof + show "int (b - a) \ int (N ^ n)" + using \b \ N ^ n\ by auto + next fix i assume "i i) - frac (a * \ i) = ?k * \ i - ?h i" using \a < b\ by (simp add: frac_def left_diff_distrib' of_nat_diff) then show "\of_int ?k * \ i - ?h i\ < 1/N" by (metis "*" \i < n\ of_int_of_nat_eq) - qed (use \a < b\ \b \ N^n\ in auto) + qed (use \a < b\ in auto) qed diff -r 32d2b96affc7 -r 200107cdd3ac src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy --- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Sun May 05 15:31:08 2024 +0100 +++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Mon May 06 14:39:33 2024 +0100 @@ -713,7 +713,7 @@ then have "0 < ?M" by (simp add: less_le) also have "\ \ ?\ (\y. f x \ g x)" - using mono by (intro emeasure_mono_AE) auto + using mono by (force intro: emeasure_mono_AE) finally have "\ \ f x \ g x" by (intro notI) auto then show ?thesis diff -r 32d2b96affc7 -r 200107cdd3ac src/HOL/Analysis/Starlike.thy --- a/src/HOL/Analysis/Starlike.thy Sun May 05 15:31:08 2024 +0100 +++ b/src/HOL/Analysis/Starlike.thy Mon May 06 14:39:33 2024 +0100 @@ -4863,10 +4863,12 @@ shows "bounded {x. a \ x = 0} \ DIM('a) = 1" proof assume "bounded {x. a \ x = 0}" - then have "aff_dim {x. a \ x = 0} \ 0" + then have 0: "aff_dim {x. a \ x = 0} \ 0" by (simp add: affine_bounded_eq_lowdim affine_hyperplane) - with assms show "DIM('a) = 1" - by (simp add: le_Suc_eq) + with assms 0 + have "int DIM('a) = 1" + using order_neq_le_trans by fastforce + then show "DIM('a) = 1" by auto next assume "DIM('a) = 1" then show "bounded {x. a \ x = 0}" diff -r 32d2b96affc7 -r 200107cdd3ac src/HOL/Analysis/Weierstrass_Theorems.thy --- a/src/HOL/Analysis/Weierstrass_Theorems.thy Sun May 05 15:31:08 2024 +0100 +++ b/src/HOL/Analysis/Weierstrass_Theorems.thy Mon May 06 14:39:33 2024 +0100 @@ -656,7 +656,12 @@ then have "(j - 4/3)*e < (j-1)*e - e^2" using e by (auto simp: of_nat_diff algebra_simps power2_eq_square) also have "... < (j-1)*e - ((j - 1)/n) * e^2" - using e True jn by (simp add: power2_eq_square field_simps) + proof - + have "(j - 1) / n < 1" + using j1 jn by fastforce + with \e>0\ show ?thesis + by (smt (verit, best) mult_less_cancel_right2 zero_less_power) + qed also have "... = e * (j-1) * (1 - e/n)" by (simp add: power2_eq_square field_simps) also have "... \ e * (\i\j-2. xf i t)" diff -r 32d2b96affc7 -r 200107cdd3ac src/HOL/Binomial.thy --- a/src/HOL/Binomial.thy Sun May 05 15:31:08 2024 +0100 +++ b/src/HOL/Binomial.thy Mon May 06 14:39:33 2024 +0100 @@ -18,10 +18,10 @@ text \Combinatorial definition\ -definition binomial :: "nat \ nat \ nat" (infixl "choose" 65) +definition binomial :: "nat \ nat \ nat" (infix "choose" 64) where "n choose k = card {K\Pow {0.. n" shows "m choose k \ n choose k" proof - have "{K. K \ {0.. card K = k} \ {K. K \ {0.. card K = k}" @@ -1219,7 +1219,7 @@ by (rule card_image) auto also have "\ = (length (x # xs) + length ys) choose length (x # xs)" using "3.prems" by (intro "3.IH") auto - also have "length xs + length (y # ys) choose length xs + \ = + also have "(length xs + length (y # ys) choose length xs) + \ = (length (x # xs) + length (y # ys)) choose length (x # xs)" by simp finally show ?case . qed auto @@ -1243,6 +1243,7 @@ qed subsection \Inclusion-exclusion principle\ + text \Ported from HOL Light by lcp\ lemma Inter_over_Union: diff -r 32d2b96affc7 -r 200107cdd3ac src/HOL/Computational_Algebra/Formal_Laurent_Series.thy --- a/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy Sun May 05 15:31:08 2024 +0100 +++ b/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy Mon May 06 14:39:33 2024 +0100 @@ -1057,7 +1057,7 @@ by (auto simp: dfg_def) ultimately have "(f * g) $$ n = (\i=0..nat (n - dfg). f $$ (df + int i) * g $$ (n - df - int i))" - by simp + by (simp del: of_nat_diff) moreover have "(\i=0..nat (n - dfg). f $$ (df + int i) * g $$ (n - df - int i)) = (\i=0..n - dfg. f $$ (df + i) * g $$ (n - df - i))" diff -r 32d2b96affc7 -r 200107cdd3ac src/HOL/Computational_Algebra/Formal_Power_Series.thy --- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Sun May 05 15:31:08 2024 +0100 +++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Mon May 06 14:39:33 2024 +0100 @@ -5625,10 +5625,9 @@ unfolding pochhammer_eq_0_iff by blast from j have "b = of_nat n - of_nat j - of_nat 1" by (simp add: algebra_simps) - then have "b = of_nat (n - j - 1)" - using j kn by (simp add: of_nat_diff) then show False - using \j < n\ j b by auto + using \j < n\ j b + by (metis bn0 c mult_cancel_right2 pochhammer_minus) qed from nz kn [simplified] have nz': "pochhammer (1 + b - of_nat n) k \ 0" @@ -5732,7 +5731,7 @@ have h: "?b \ of_nat j" if "j < n" for j proof - have "c \ - of_nat (n - j - 1)" - using c that by auto + using c that by (auto simp: dest!: bspec [where x = "n-j-1"]) with that show ?thesis by (auto simp add: algebra_simps of_nat_diff) qed diff -r 32d2b96affc7 -r 200107cdd3ac src/HOL/Filter.thy --- a/src/HOL/Filter.thy Sun May 05 15:31:08 2024 +0100 +++ b/src/HOL/Filter.thy Mon May 06 14:39:33 2024 +0100 @@ -233,7 +233,7 @@ "frequently P F \ eventually Q F \ frequently (\x. P x \ Q x) F" using frequently_cong [of Q F P "\x. P x \ Q x"] by meson -lemma eventually_frequently_const_simps: +lemma eventually_frequently_const_simps [simp]: "(\\<^sub>Fx in F. P x \ C) \ (\\<^sub>Fx in F. P x) \ C" "(\\<^sub>Fx in F. C \ P x) \ C \ (\\<^sub>Fx in F. P x)" "(\\<^sub>Fx in F. P x \ C) \ (\\<^sub>Fx in F. P x) \ C" diff -r 32d2b96affc7 -r 200107cdd3ac src/HOL/HOLCF/Universal.thy --- a/src/HOL/HOLCF/Universal.thy Sun May 05 15:31:08 2024 +0100 +++ b/src/HOL/HOLCF/Universal.thy Mon May 06 14:39:33 2024 +0100 @@ -8,7 +8,7 @@ imports Bifinite Completion "HOL-Library.Nat_Bijection" begin -no_notation binomial (infixl "choose" 65) +no_notation binomial (infix "choose" 64) subsection \Basis for universal domain\ @@ -54,7 +54,7 @@ lemma eq_prod_encode_pairI: "\fst (prod_decode x) = a; snd (prod_decode x) = b\ \ x = prod_encode (a, b)" -by (erule subst, erule subst, simp) + by auto lemma node_cases: assumes 1: "x = 0 \ P" @@ -144,24 +144,14 @@ lemma ubasis_until_less: "ubasis_le (ubasis_until P x) x" apply (induct x rule: node_induct) apply (simp add: ubasis_le_refl) -apply (simp add: ubasis_le_refl) -apply (rule impI) -apply (erule ubasis_le_trans) -apply (erule ubasis_le_lower) -done + by (metis ubasis_le.simps ubasis_until.simps(2)) lemma ubasis_until_chain: assumes PQ: "\x. P x \ Q x" shows "ubasis_le (ubasis_until P x) (ubasis_until Q x)" apply (induct x rule: node_induct) apply (simp add: ubasis_le_refl) -apply (simp add: ubasis_le_refl) -apply (simp add: PQ) -apply clarify -apply (rule ubasis_le_trans) -apply (rule ubasis_until_less) -apply (erule ubasis_le_lower) -done + by (metis assms ubasis_until.simps(2) ubasis_until_less) lemma ubasis_until_mono: assumes "\i a S b. \finite S; P (node i a S); b \ S; ubasis_le a b\ \ P b" @@ -172,17 +162,10 @@ case (ubasis_le_trans a b c) thus ?case by - (rule ubasis_le.ubasis_le_trans) next case (ubasis_le_lower S a i) thus ?case - apply (clarsimp simp add: ubasis_le_refl) - apply (rule ubasis_le_trans [OF ubasis_until_less]) - apply (erule ubasis_le.ubasis_le_lower) - done + by (metis ubasis_le.simps ubasis_until.simps(2) ubasis_until_less) next case (ubasis_le_upper S b a i) thus ?case - apply clarsimp - apply (subst ubasis_until_same) - apply (erule (3) assms) - apply (erule (2) ubasis_le.ubasis_le_upper) - done + by (metis assms ubasis_le.simps ubasis_until.simps(2) ubasis_until_same) qed lemma finite_range_ubasis_until: diff -r 32d2b96affc7 -r 200107cdd3ac src/HOL/Homology/Homology_Groups.thy --- a/src/HOL/Homology/Homology_Groups.thy Sun May 05 15:31:08 2024 +0100 +++ b/src/HOL/Homology/Homology_Groups.thy Mon May 06 14:39:33 2024 +0100 @@ -770,11 +770,11 @@ using a chain_boundary_chain_map singular_relcycle by blast have contf: "continuous_map (subtopology X S) (subtopology Y T) f" using assms - by (auto simp: continuous_map_in_subtopology topspace_subtopology - continuous_map_from_subtopology) + by (auto simp: continuous_map_in_subtopology continuous_map_from_subtopology) show ?thesis unfolding q using assms p1 a - by (simp add: cbm ceq contf hom_boundary_chain_boundary hom_induced_chain_map p1_eq sb sr) + by (simp add: cbm ceq contf hom_boundary_chain_boundary hom_induced_chain_map p1_eq sb sr + del: of_nat_diff) next case False with assms show ?thesis diff -r 32d2b96affc7 -r 200107cdd3ac src/HOL/Lattices_Big.thy --- a/src/HOL/Lattices_Big.thy Sun May 05 15:31:08 2024 +0100 +++ b/src/HOL/Lattices_Big.thy Mon May 06 14:39:33 2024 +0100 @@ -655,6 +655,29 @@ end +text \Handy results about @{term Max} and @{term Min} by Chelsea Edmonds\ +lemma obtains_Max: + assumes "finite A" and "A \ {}" + obtains x where "x \ A" and "Max A = x" + using assms Max_in by blast + +lemma obtains_MAX: + assumes "finite A" and "A \ {}" + obtains x where "x \ A" and "Max (f ` A) = f x" + using obtains_Max + by (metis (mono_tags, opaque_lifting) assms(1) assms(2) empty_is_image finite_imageI image_iff) + +lemma obtains_Min: + assumes "finite A" and "A \ {}" + obtains x where "x \ A" and "Min A = x" + using assms Min_in by blast + +lemma obtains_MIN: + assumes "finite A" and "A \ {}" + obtains x where "x \ A" and "Min (f ` A) = f x" + using obtains_Min assms empty_is_image finite_imageI image_iff + by (metis (mono_tags, opaque_lifting)) + lemma Max_eq_if: assumes "finite A" "finite B" "\a\A. \b\B. a \ b" "\b\B. \a\A. b \ a" shows "Max A = Max B" diff -r 32d2b96affc7 -r 200107cdd3ac src/HOL/Library/Landau_Symbols.thy --- a/src/HOL/Library/Landau_Symbols.thy Sun May 05 15:31:08 2024 +0100 +++ b/src/HOL/Library/Landau_Symbols.thy Mon May 06 14:39:33 2024 +0100 @@ -1447,9 +1447,8 @@ lemma landau_symbol_if_at_top_eq [simp]: assumes "landau_symbol L L' Lr" shows "L at_top (\x::'a::linordered_semidom. if x = a then f x else g x) = L at_top (g)" -apply (rule landau_symbol.cong[OF assms]) -using less_add_one[of a] apply (auto intro: eventually_mono eventually_ge_at_top[of "a + 1"]) -done + apply (rule landau_symbol.cong[OF assms]) + by (auto simp add: frequently_def eventually_at_top_linorder dest!: spec [where x= "a + 1"]) lemmas landau_symbols_if_at_top_eq [simp] = landau_symbols[THEN landau_symbol_if_at_top_eq] diff -r 32d2b96affc7 -r 200107cdd3ac src/HOL/Nat.thy --- a/src/HOL/Nat.thy Sun May 05 15:31:08 2024 +0100 +++ b/src/HOL/Nat.thy Mon May 06 14:39:33 2024 +0100 @@ -1752,7 +1752,7 @@ context semiring_1_cancel begin -lemma of_nat_diff: +lemma of_nat_diff [simp]: \of_nat (m - n) = of_nat m - of_nat n\ if \n \ m\ proof - from that obtain q where \m = n + q\ diff -r 32d2b96affc7 -r 200107cdd3ac src/HOL/NthRoot.thy --- a/src/HOL/NthRoot.thy Sun May 05 15:31:08 2024 +0100 +++ b/src/HOL/NthRoot.thy Mon May 06 14:39:33 2024 +0100 @@ -745,7 +745,7 @@ also have "\ = n" using \2 < n\ by (simp add: x_def) finally have "real (n - 1) * (real n / 2 * (x n)\<^sup>2) \ real (n - 1) * 1" - by simp + using that by auto then have "(x n)\<^sup>2 \ 2 / real n" using \2 < n\ unfolding mult_le_cancel_left by (simp add: field_simps) from real_sqrt_le_mono[OF this] show ?thesis diff -r 32d2b96affc7 -r 200107cdd3ac src/HOL/Number_Theory/Quadratic_Reciprocity.thy --- a/src/HOL/Number_Theory/Quadratic_Reciprocity.thy Sun May 05 15:31:08 2024 +0100 +++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy Mon May 06 14:39:33 2024 +0100 @@ -185,24 +185,14 @@ proof - obtain y k1 k2 where yk: "y = nat (fst res) + k1 * p" "y = nat (snd res) + k2 * q" using chinese_remainder[of p q] pq_coprime p_ge_0 q_ge_0 by fastforce - have "fst res = int (y - k1 * p)" - using \0 \ fst res\ yk(1) by simp - moreover have "snd res = int (y - k2 * q)" - using \0 \ snd res\ yk(2) by simp - ultimately have res: "res = (int (y - k1 * p), int (y - k2 * q))" - by (simp add: prod_eq_iff) - have y: "k1 * p \ y" "k2 * q \ y" - using yk by simp_all - from y have *: "[y = nat (fst res)] (mod p)" "[y = nat (snd res)] (mod q)" - by (auto simp add: res cong_le_nat intro: exI [of _ k1] exI [of _ k2]) - from * have "(y mod (int p * int q)) mod int p = fst res" "(y mod (int p * int q)) mod int q = snd res" - using y apply (auto simp add: res of_nat_mult [symmetric] of_nat_mod [symmetric] mod_mod_cancel simp del: of_nat_mult) - apply (metis \fst res = int (y - k1 * p)\ assms(1) assms(2) cong_def mod_pos_pos_trivial nat_int of_nat_mod) - apply (metis \snd res = int (y - k2 * q)\ assms(3) assms(4) cong_def mod_pos_pos_trivial nat_int of_nat_mod) - done - then obtain x where "P_1 res x" + have "(y mod (int p * int q)) mod int p = fst res" + using assms by (simp add: mod_mod_cancel yk(1)) + moreover have "(y mod (int p * int q)) mod int q = snd res" + using assms by (simp add: mod_mod_cancel yk(2)) + ultimately obtain x where "P_1 res x" unfolding P_1_def - using Divides.pos_mod_bound Divides.pos_mod_sign pq_ge_0 by fastforce + using Divides.pos_mod_bound Divides.pos_mod_sign pq_ge_0 + by (metis atLeastAtMost_iff zle_diff1_eq) moreover have "a = b" if "P_1 res a" "P_1 res b" for a b proof - from that have "int p * int q dvd a - b" diff -r 32d2b96affc7 -r 200107cdd3ac src/HOL/Probability/Sinc_Integral.thy --- a/src/HOL/Probability/Sinc_Integral.thy Sun May 05 15:31:08 2024 +0100 +++ b/src/HOL/Probability/Sinc_Integral.thy Mon May 06 14:39:33 2024 +0100 @@ -182,9 +182,10 @@ have *: "interval_lebesgue_integrable lborel (ereal 0) (ereal T) (\t. \ * sinc (t * \))" by (intro interval_lebesgue_integrable_mult_right interval_integrable_isCont continuous_within_compose3 [OF isCont_sinc]) auto - show ?thesis - by (rule interval_lebesgue_integrable_cong_AE[THEN iffD1, OF _ _ _ *]) - (insert AE_lborel_singleton[of 0], auto) + have "0 \ einterval (min (ereal 0) (ereal T)) (max (ereal 0) (ereal T))" + by (smt (verit, best) einterval_iff max_def min_def_raw order_less_le) + then show ?thesis + by (intro interval_lebesgue_integrable_cong_AE[THEN iffD1, OF _ _ _ *]) auto qed (* TODO: need a better version of FTC2 *) diff -r 32d2b96affc7 -r 200107cdd3ac src/HOL/Random.thy --- a/src/HOL/Random.thy Sun May 05 15:31:08 2024 +0100 +++ b/src/HOL/Random.thy Mon May 06 14:39:33 2024 +0100 @@ -84,7 +84,9 @@ lemma pick_drop_zero: "pick (filter (\(k, _). k > 0) xs) = pick xs" - by (induct xs) (auto simp add: fun_eq_iff less_natural_def minus_natural_def) + apply (induct xs) + apply (auto simp: fun_eq_iff less_natural.rep_eq split: prod.split) + by (metis diff_zero of_nat_0 of_nat_of_natural) lemma pick_same: "l < length xs \ Random.pick (map (Pair 1) xs) (natural_of_nat l) = nth xs l" diff -r 32d2b96affc7 -r 200107cdd3ac src/HOL/Real_Asymp/Multiseries_Expansion.thy --- a/src/HOL/Real_Asymp/Multiseries_Expansion.thy Sun May 05 15:31:08 2024 +0100 +++ b/src/HOL/Real_Asymp/Multiseries_Expansion.thy Mon May 06 14:39:33 2024 +0100 @@ -4219,14 +4219,17 @@ hence "eventually (\x. ?h x = g x - c * ln (b x) - eval (C - const_expansion c * L) x * b x powr e) at_top" (is "eventually (\x. _ = ?h x) _") using assms(2) - by (auto simp: expands_to.simps scale_ms_def elim: eventually_elim2) - ultimately have **: "is_expansion_aux xs ?h (b # basis)" by (rule is_expansion_aux_cong) + apply (simp add: expands_to.simps scale_ms_def) + by (smt (verit) eventually_cong) + ultimately have **: "is_expansion_aux xs ?h (b # basis)" + by (rule is_expansion_aux_cong) from assms(1,4) have "ms_exp_gt 0 (ms_aux_hd_exp xs)" "is_expansion C basis" by (auto simp: expands_to.simps elim!: is_expansion_aux_MSLCons) moreover from assms(1) have "length basis = expansion_level TYPE('a)" by (auto simp: expands_to.simps dest: is_expansion_aux_expansion_level) ultimately have "is_expansion_aux (MSLCons (C - scale_ms c L, e) xs) - (\x. g x - c * ln (b x)) (b # basis)" using assms unfolding scale_ms_def + (\x. g x - c * ln (b x)) (b # basis)" + using assms unfolding scale_ms_def by (intro is_expansion_aux.intros is_expansion_minus is_expansion_mult is_expansion_const * **) (simp_all add: basis_wf_Cons expands_to.simps) with assms(1) show ?thesis by (auto simp: expands_to.simps) diff -r 32d2b96affc7 -r 200107cdd3ac src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Sun May 05 15:31:08 2024 +0100 +++ b/src/HOL/Transcendental.thy Mon May 06 14:39:33 2024 +0100 @@ -211,6 +211,22 @@ with assms show ?thesis by (simp add: field_simps) qed +lemma upper_le_binomial: + assumes "0 < k" and "k < n" + shows "n \ n choose k" +proof - + from assms have "1 \ n" by simp + define k' where "k' = (if n div 2 \ k then k else n - k)" + from assms have 1: "k' \ n - 1" and 2: "n div 2 \ k'" by (auto simp: k'_def) + from assms(2) have "k \ n" by simp + have "n choose k = n choose k'" by (simp add: k'_def binomial_symmetric[OF \k \ n\]) + have "n = n choose 1" by (simp only: choose_one) + also from \1 \ n\ have "\ = n choose (n - 1)" by (rule binomial_symmetric) + also from 1 2 have "\ \ n choose k'" by (rule binomial_antimono) simp + also have "\ = n choose k" by (simp add: k'_def binomial_symmetric[OF \k \ n\]) + finally show ?thesis . +qed + subsection \Properties of Power Series\ @@ -3061,8 +3077,9 @@ shows "((\x. f x powr g x) \ a powr b) F" unfolding powr_def proof (rule filterlim_If) - from f show "((\x. 0) \ (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x = 0}))" - by simp (auto simp: filterlim_iff eventually_inf_principal elim: eventually_mono dest: t1_space_nhds) + show "((\x. 0) \ (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x = 0}))" + using tendsto_imp_eventually_ne [OF f] a + by (simp add: filterlim_iff eventually_inf_principal frequently_def) from f g a show "((\x. exp (g x * ln (f x))) \ (if a = 0 then 0 else exp (b * ln a))) (inf F (principal {x. f x \ 0}))" by (auto intro!: tendsto_intros intro: tendsto_mono inf_le1) diff -r 32d2b96affc7 -r 200107cdd3ac src/HOL/ex/HarmonicSeries.thy --- a/src/HOL/ex/HarmonicSeries.thy Sun May 05 15:31:08 2024 +0100 +++ b/src/HOL/ex/HarmonicSeries.thy Mon May 06 14:39:33 2024 +0100 @@ -103,7 +103,7 @@ by (simp add: tmdef) also from mgt0 have "\ = ((1/(real tm)) * real ((2::nat)^(m - 1)))" - by (auto simp: tmdef dest: two_pow_sub) + using tmdef two_pow_sub by presburger also have "\ = (real (2::nat))^(m - 1) / (real (2::nat))^m" by (simp add: tmdef)