--- 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 \<open>0 < j\<close> have "k > 0" "2 * k < 2 ^ n"
using Suc.prems(2) k by auto
with k \<open>0 < n\<close> 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 \<open>0 < k\<close>
- 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)
--- 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 (\<lambda>n. x \<le> X n) sequentially"
unfolding filterlim_at_top_ge[where c=x] by auto
then show "(\<lambda>n. indicator {..X n} x *\<^sub>R f x) \<longlonglongrightarrow> 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) \<le> norm (f x)"
by (auto split: split_indicator)
--- 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 (\<lambda>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 "(\<lambda>n. ?f n x) \<longlonglongrightarrow> ?fR x"
by (rule tendsto_eventually)
qed (auto simp: nonneg incseq_def le_fun_def split: split_indicator)
--- 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 \<le> 1/2")
case True
show ?thesis
- using \<open>j \<noteq> 0 \<close> \<open>j < n\<close> True
+ using \<open>j \<noteq> 0\<close> \<open>j < n\<close> 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 \<open>j < n\<close> by (simp add: algebra_simps diff_divide_distrib of_nat_diff)
+
show ?thesis
- unfolding seq
- using \<open>j < n\<close> 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) \<le> pi / real n"
+ by (smt (verit) divide_nonneg_nonneg of_nat_0_le_iff pi_ge_zero)
+ qed (use \<open>j < n\<close> False in \<open>auto simp: divide_simps\<close>)
qed
with sin_less show ?thesis by force
qed
--- 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 \<open>p > 0\<close>
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: "\<And>m t. m < p \<Longrightarrow> a \<le> t \<Longrightarrow> t \<le> b \<Longrightarrow>
(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 = "\<lambda>t. \<Sum>i<p. (- 1) ^ i *\<^sub>R Dg i t *\<^sub>R Df (p - Suc i) t"
from sum_prod_derivatives_has_vector_derivative[of _ Dg _ _ _ Df,
OF \<open>p > 0\<close> g0 Dg f0 Df]
--- 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 \<bullet> x = 0}"
by (auto simp: affine_hyperplane)
show "aff_dim {x. i \<bullet> 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 \<bullet> x = 0} f g"
by (force simp: homeomorphic_def)
--- 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 = "\<lambda>i. \<lfloor>b * \<theta> i\<rfloor> - \<lfloor>a * \<theta> i\<rfloor>"
show ?thesis
proof
+ show "int (b - a) \<le> int (N ^ n)"
+ using \<open>b \<le> N ^ n\<close> by auto
+ next
fix i
assume "i<n"
have "frac (b * \<theta> i) - frac (a * \<theta> i) = ?k * \<theta> i - ?h i"
using \<open>a < b\<close> by (simp add: frac_def left_diff_distrib' of_nat_diff)
then show "\<bar>of_int ?k * \<theta> i - ?h i\<bar> < 1/N"
by (metis "*" \<open>i < n\<close> of_int_of_nat_eq)
- qed (use \<open>a < b\<close> \<open>b \<le> N^n\<close> in auto)
+ qed (use \<open>a < b\<close> in auto)
qed
--- 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 "\<dots> \<le> ?\<mu> (\<lambda>y. f x \<le> g x)"
- using mono by (intro emeasure_mono_AE) auto
+ using mono by (force intro: emeasure_mono_AE)
finally have "\<not> \<not> f x \<le> g x"
by (intro notI) auto
then show ?thesis
--- 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 \<bullet> x = 0} \<longleftrightarrow> DIM('a) = 1"
proof
assume "bounded {x. a \<bullet> x = 0}"
- then have "aff_dim {x. a \<bullet> x = 0} \<le> 0"
+ then have 0: "aff_dim {x. a \<bullet> x = 0} \<le> 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 \<bullet> x = 0}"
--- 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 \<open>e>0\<close> 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 "... \<le> e * (\<Sum>i\<le>j-2. xf i t)"
--- 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 \<open>Combinatorial definition\<close>
-definition binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat" (infixl "choose" 65)
+definition binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat" (infix "choose" 64)
where "n choose k = card {K\<in>Pow {0..<n}. card K = k}"
-lemma binomial_mono:
+lemma binomial_right_mono:
assumes "m \<le> n" shows "m choose k \<le> n choose k"
proof -
have "{K. K \<subseteq> {0..<m} \<and> card K = k} \<subseteq> {K. K \<subseteq> {0..<n} \<and> card K = k}"
@@ -1219,7 +1219,7 @@
by (rule card_image) auto
also have "\<dots> = (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 + \<dots> =
+ also have "(length xs + length (y # ys) choose length xs) + \<dots> =
(length (x # xs) + length (y # ys)) choose length (x # xs)" by simp
finally show ?case .
qed auto
@@ -1243,6 +1243,7 @@
qed
subsection \<open>Inclusion-exclusion principle\<close>
+
text \<open>Ported from HOL Light by lcp\<close>
lemma Inter_over_Union:
--- 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 = (\<Sum>i=0..nat (n - dfg). f $$ (df + int i) * g $$ (n - df - int i))"
- by simp
+ by (simp del: of_nat_diff)
moreover have
"(\<Sum>i=0..nat (n - dfg). f $$ (df + int i) * g $$ (n - df - int i)) =
(\<Sum>i=0..n - dfg. f $$ (df + i) * g $$ (n - df - i))"
--- 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 \<open>j < n\<close> j b by auto
+ using \<open>j < n\<close> 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 \<noteq> 0"
@@ -5732,7 +5731,7 @@
have h: "?b \<noteq> of_nat j" if "j < n" for j
proof -
have "c \<noteq> - 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
--- 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 \<Longrightarrow> eventually Q F \<Longrightarrow> frequently (\<lambda>x. P x \<and> Q x) F"
using frequently_cong [of Q F P "\<lambda>x. P x \<and> Q x"] by meson
-lemma eventually_frequently_const_simps:
+lemma eventually_frequently_const_simps [simp]:
"(\<exists>\<^sub>Fx in F. P x \<and> C) \<longleftrightarrow> (\<exists>\<^sub>Fx in F. P x) \<and> C"
"(\<exists>\<^sub>Fx in F. C \<and> P x) \<longleftrightarrow> C \<and> (\<exists>\<^sub>Fx in F. P x)"
"(\<forall>\<^sub>Fx in F. P x \<or> C) \<longleftrightarrow> (\<forall>\<^sub>Fx in F. P x) \<or> C"
--- 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 \<open>Basis for universal domain\<close>
@@ -54,7 +54,7 @@
lemma eq_prod_encode_pairI:
"\<lbrakk>fst (prod_decode x) = a; snd (prod_decode x) = b\<rbrakk> \<Longrightarrow> x = prod_encode (a, b)"
-by (erule subst, erule subst, simp)
+ by auto
lemma node_cases:
assumes 1: "x = 0 \<Longrightarrow> 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: "\<And>x. P x \<Longrightarrow> 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 "\<And>i a S b. \<lbrakk>finite S; P (node i a S); b \<in> S; ubasis_le a b\<rbrakk> \<Longrightarrow> 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:
--- 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
--- 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 \<open>Handy results about @{term Max} and @{term Min} by Chelsea Edmonds\<close>
+lemma obtains_Max:
+ assumes "finite A" and "A \<noteq> {}"
+ obtains x where "x \<in> A" and "Max A = x"
+ using assms Max_in by blast
+
+lemma obtains_MAX:
+ assumes "finite A" and "A \<noteq> {}"
+ obtains x where "x \<in> 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 \<noteq> {}"
+ obtains x where "x \<in> A" and "Min A = x"
+ using assms Min_in by blast
+
+lemma obtains_MIN:
+ assumes "finite A" and "A \<noteq> {}"
+ obtains x where "x \<in> 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" "\<forall>a\<in>A. \<exists>b\<in>B. a \<le> b" "\<forall>b\<in>B. \<exists>a\<in>A. b \<le> a"
shows "Max A = Max B"
--- 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 (\<lambda>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]
--- 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]:
\<open>of_nat (m - n) = of_nat m - of_nat n\<close> if \<open>n \<le> m\<close>
proof -
from that obtain q where \<open>m = n + q\<close>
--- 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 "\<dots> = n"
using \<open>2 < n\<close> by (simp add: x_def)
finally have "real (n - 1) * (real n / 2 * (x n)\<^sup>2) \<le> real (n - 1) * 1"
- by simp
+ using that by auto
then have "(x n)\<^sup>2 \<le> 2 / real n"
using \<open>2 < n\<close> unfolding mult_le_cancel_left by (simp add: field_simps)
from real_sqrt_le_mono[OF this] show ?thesis
--- 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 \<open>0 \<le> fst res\<close> yk(1) by simp
- moreover have "snd res = int (y - k2 * q)"
- using \<open>0 \<le> snd res\<close> 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 \<le> y" "k2 * q \<le> 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 \<open>fst res = int (y - k1 * p)\<close> assms(1) assms(2) cong_def mod_pos_pos_trivial nat_int of_nat_mod)
- apply (metis \<open>snd res = int (y - k2 * q)\<close> 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"
--- 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) (\<lambda>t. \<theta> * sinc (t * \<theta>))"
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 \<notin> 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 *)
--- 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 (\<lambda>(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 \<Longrightarrow> Random.pick (map (Pair 1) xs) (natural_of_nat l) = nth xs l"
--- 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 (\<lambda>x. ?h x = g x - c * ln (b x) -
eval (C - const_expansion c * L) x * b x powr e) at_top"
(is "eventually (\<lambda>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)
- (\<lambda>x. g x - c * ln (b x)) (b # basis)" using assms unfolding scale_ms_def
+ (\<lambda>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)
--- 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 \<le> n choose k"
+proof -
+ from assms have "1 \<le> n" by simp
+ define k' where "k' = (if n div 2 \<le> k then k else n - k)"
+ from assms have 1: "k' \<le> n - 1" and 2: "n div 2 \<le> k'" by (auto simp: k'_def)
+ from assms(2) have "k \<le> n" by simp
+ have "n choose k = n choose k'" by (simp add: k'_def binomial_symmetric[OF \<open>k \<le> n\<close>])
+ have "n = n choose 1" by (simp only: choose_one)
+ also from \<open>1 \<le> n\<close> have "\<dots> = n choose (n - 1)" by (rule binomial_symmetric)
+ also from 1 2 have "\<dots> \<le> n choose k'" by (rule binomial_antimono) simp
+ also have "\<dots> = n choose k" by (simp add: k'_def binomial_symmetric[OF \<open>k \<le> n\<close>])
+ finally show ?thesis .
+qed
+
subsection \<open>Properties of Power Series\<close>
@@ -3061,8 +3077,9 @@
shows "((\<lambda>x. f x powr g x) \<longlongrightarrow> a powr b) F"
unfolding powr_def
proof (rule filterlim_If)
- from f show "((\<lambda>x. 0) \<longlongrightarrow> (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 "((\<lambda>x. 0) \<longlongrightarrow> (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 "((\<lambda>x. exp (g x * ln (f x))) \<longlongrightarrow> (if a = 0 then 0 else exp (b * ln a)))
(inf F (principal {x. f x \<noteq> 0}))"
by (auto intro!: tendsto_intros intro: tendsto_mono inf_le1)
--- 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
"\<dots> = ((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
"\<dots> = (real (2::nat))^(m - 1) / (real (2::nat))^m"
by (simp add: tmdef)