--- a/src/HOL/Computational_Algebra/Polynomial.thy Wed Aug 26 15:59:21 2020 +0100
+++ b/src/HOL/Computational_Algebra/Polynomial.thy Thu Aug 27 12:14:46 2020 +0100
@@ -2613,7 +2613,7 @@
lemma poly_IVT_pos: "a < b \<Longrightarrow> poly p a < 0 \<Longrightarrow> 0 < poly p b \<Longrightarrow> \<exists>x. a < x \<and> x < b \<and> poly p x = 0"
for a b :: real
- using IVT_objl [of "poly p" a 0 b] by (auto simp add: order_le_less)
+ using IVT [of "poly p" a 0 b] by (auto simp add: order_le_less)
lemma poly_IVT_neg: "a < b \<Longrightarrow> 0 < poly p a \<Longrightarrow> poly p b < 0 \<Longrightarrow> \<exists>x. a < x \<and> x < b \<and> poly p x = 0"
for a b :: real
--- a/src/HOL/Deriv.thy Wed Aug 26 15:59:21 2020 +0100
+++ b/src/HOL/Deriv.thy Thu Aug 27 12:14:46 2020 +0100
@@ -141,7 +141,15 @@
lemma has_derivative_at_within:
"(f has_derivative f') (at x within s) \<longleftrightarrow>
(bounded_linear f' \<and> ((\<lambda>y. ((f y - f x) - f' (y - x)) /\<^sub>R norm (y - x)) \<longlongrightarrow> 0) (at x within s))"
- by (cases "at x within s = bot") (simp_all add: has_derivative_def Lim_ident_at)
+proof (cases "at x within s = bot")
+ case True
+ then show ?thesis
+ by (metis (no_types, lifting) has_derivative_within tendsto_bot)
+next
+ case False
+ then show ?thesis
+ by (simp add: Lim_ident_at has_derivative_def)
+qed
lemma has_derivative_iff_norm:
"(f has_derivative f') (at x within s) \<longleftrightarrow>
--- a/src/HOL/Limits.thy Wed Aug 26 15:59:21 2020 +0100
+++ b/src/HOL/Limits.thy Thu Aug 27 12:14:46 2020 +0100
@@ -116,9 +116,6 @@
lemma BseqI': "(\<And>n. norm (X n) \<le> K) \<Longrightarrow> Bseq X"
by (intro BfunI) (auto simp: eventually_sequentially)
-lemma BseqI2': "\<forall>n\<ge>N. norm (X n) \<le> K \<Longrightarrow> Bseq X"
- by (intro BfunI) (auto simp: eventually_sequentially)
-
lemma Bseq_def: "Bseq X \<longleftrightarrow> (\<exists>K>0. \<forall>n. norm (X n) \<le> K)"
unfolding Bfun_def eventually_sequentially
proof safe
@@ -343,7 +340,7 @@
subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Polynomal function extremal theorem, from HOL Light\<close>
-lemma polyfun_extremal_lemma: (*COMPLEX_POLYFUN_EXTREMAL_LEMMA in HOL Light*)
+lemma polyfun_extremal_lemma:
fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
assumes "0 < e"
shows "\<exists>M. \<forall>z. M \<le> norm(z) \<longrightarrow> norm (\<Sum>i\<le>n. c(i) * z^i) \<le> e * norm(z) ^ (Suc n)"
@@ -386,14 +383,13 @@
proof (induction n)
case 0
then show ?case
- using k by simp
+ using k by simp
next
case (Suc m)
- let ?even = ?case
- show ?even
+ show ?case
proof (cases "c (Suc m) = 0")
case True
- then show ?even using Suc k
+ then show ?thesis using Suc k
by auto (metis antisym_conv less_eq_Suc_le not_le)
next
case False
@@ -424,7 +420,7 @@
apply (simp add: field_simps norm_mult norm_power)
done
qed
- then show ?even
+ then show ?thesis
by (simp add: eventually_at_infinity)
qed
qed
@@ -1526,10 +1522,12 @@
lemma at_bot_mirror :
shows "(at_bot::('a::{ordered_ab_group_add,linorder} filter)) = filtermap uminus at_top"
- apply (rule filtermap_fun_inverse[of uminus, symmetric])
- subgoal unfolding filterlim_at_top filterlim_at_bot eventually_at_bot_linorder using le_minus_iff by auto
- subgoal unfolding filterlim_at_bot eventually_at_top_linorder using minus_le_iff by auto
- by auto
+proof (rule filtermap_fun_inverse[symmetric])
+ show "filterlim uminus at_top (at_bot::'a filter)"
+ using eventually_at_bot_linorder filterlim_at_top le_minus_iff by force
+ show "filterlim uminus (at_bot::'a filter) at_top"
+ by (simp add: filterlim_at_bot minus_le_iff)
+qed auto
lemma at_top_mirror :
shows "(at_top::('a::{ordered_ab_group_add,linorder} filter)) = filtermap uminus at_bot"
@@ -1992,9 +1990,8 @@
proof (intro filterlim_at_infinity[THEN iffD2] allI impI)
fix y :: real
assume "0 < y"
- have "0 < norm x - 1" by simp
- then obtain N :: nat where "y < real N * (norm x - 1)"
- by (blast dest: reals_Archimedean3)
+ obtain N :: nat where "y < real N * (norm x - 1)"
+ by (meson diff_gt_0_iff_gt reals_Archimedean3 x)
also have "\<dots> \<le> real N * (norm x - 1) + 1"
by simp
also have "\<dots> \<le> (norm x - 1 + 1) ^ N"
@@ -2181,9 +2178,7 @@
text \<open>A congruence rule allowing us to transform limits assuming not at point.\<close>
-(* FIXME: Only one congruence rule for tendsto can be used at a time! *)
-
-lemma Lim_cong_within(*[cong add]*):
+lemma Lim_cong_within [cong]:
assumes "a = b"
and "x = y"
and "S = T"
@@ -2192,13 +2187,6 @@
unfolding tendsto_def eventually_at_topological
using assms by simp
-lemma Lim_cong_at(*[cong add]*):
- assumes "a = b" "x = y"
- and "\<And>x. x \<noteq> a \<Longrightarrow> f x = g x"
- shows "((\<lambda>x. f x) \<longlongrightarrow> x) (at a) \<longleftrightarrow> ((g \<longlongrightarrow> y) (at a))"
- unfolding tendsto_def eventually_at_topological
- using assms by simp
-
text \<open>An unbounded sequence's inverse tends to 0.\<close>
lemma LIMSEQ_inverse_zero:
assumes "\<And>r::real. \<exists>N. \<forall>n\<ge>N. r < X n"
@@ -2963,19 +2951,6 @@
\<exists>M. (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M) \<and> (\<forall>N. N < M \<longrightarrow> (\<exists>x. a \<le> x \<and> x \<le> b \<and> N < f x))"
using isCont_eq_Ub[of a b f] by auto
-(*HOL style here: object-level formulations*)
-lemma IVT_objl:
- "(f a \<le> y \<and> y \<le> f b \<and> a \<le> b \<and> (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x)) \<longrightarrow>
- (\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y)"
- for a y :: real
- by (blast intro: IVT)
-
-lemma IVT2_objl:
- "(f b \<le> y \<and> y \<le> f a \<and> a \<le> b \<and> (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x)) \<longrightarrow>
- (\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y)"
- for b y :: real
- by (blast intro: IVT2)
-
lemma isCont_Lb_Ub:
fixes f :: "real \<Rightarrow> real"
assumes "a \<le> b" "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x"
--- a/src/HOL/Series.thy Wed Aug 26 15:59:21 2020 +0100
+++ b/src/HOL/Series.thy Thu Aug 27 12:14:46 2020 +0100
@@ -200,7 +200,7 @@
subsection \<open>Infinite summability on ordered, topological monoids\<close>
-lemma sums_le: "\<forall>n. f n \<le> g n \<Longrightarrow> f sums s \<Longrightarrow> g sums t \<Longrightarrow> s \<le> t"
+lemma sums_le: "(\<And>n. f n \<le> g n) \<Longrightarrow> f sums s \<Longrightarrow> g sums t \<Longrightarrow> s \<le> t"
for f g :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add,linorder_topology}"
by (rule LIMSEQ_le) (auto intro: sum_mono simp: sums_def)
@@ -208,24 +208,26 @@
fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add,linorder_topology}"
begin
-lemma suminf_le: "\<forall>n. f n \<le> g n \<Longrightarrow> summable f \<Longrightarrow> summable g \<Longrightarrow> suminf f \<le> suminf g"
- by (auto dest: sums_summable intro: sums_le)
+lemma suminf_le: "(\<And>n. f n \<le> g n) \<Longrightarrow> summable f \<Longrightarrow> summable g \<Longrightarrow> suminf f \<le> suminf g"
+ using sums_le by blast
lemma sum_le_suminf:
- shows "summable f \<Longrightarrow> finite I \<Longrightarrow> \<forall>m\<in>- I. 0 \<le> f m \<Longrightarrow> sum f I \<le> suminf f"
+ shows "summable f \<Longrightarrow> finite I \<Longrightarrow> (\<And>n. n \<in>- I \<Longrightarrow> 0 \<le> f n) \<Longrightarrow> sum f I \<le> suminf f"
by (rule sums_le[OF _ sums_If_finite_set summable_sums]) auto
-lemma suminf_nonneg: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 \<le> suminf f"
+lemma suminf_nonneg: "summable f \<Longrightarrow> (\<And>n. 0 \<le> f n) \<Longrightarrow> 0 \<le> suminf f"
using sum_le_suminf by force
lemma suminf_le_const: "summable f \<Longrightarrow> (\<And>n. sum f {..<n} \<le> x) \<Longrightarrow> suminf f \<le> x"
by (metis LIMSEQ_le_const2 summable_LIMSEQ)
-lemma suminf_eq_zero_iff: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> suminf f = 0 \<longleftrightarrow> (\<forall>n. f n = 0)"
+lemma suminf_eq_zero_iff:
+ assumes "summable f" and pos: "\<And>n. 0 \<le> f n"
+ shows "suminf f = 0 \<longleftrightarrow> (\<forall>n. f n = 0)"
proof
- assume "summable f" "suminf f = 0" and pos: "\<forall>n. 0 \<le> f n"
+ assume "suminf f = 0"
then have f: "(\<lambda>n. \<Sum>i<n. f i) \<longlonglongrightarrow> 0"
- using summable_LIMSEQ[of f] by simp
+ using summable_LIMSEQ[of f] assms by simp
then have "\<And>i. (\<Sum>n\<in>{i}. f n) \<le> 0"
proof (rule LIMSEQ_le_const)
show "\<exists>N. \<forall>n\<ge>N. (\<Sum>n\<in>{i}. f n) \<le> sum f {..<n}" for i
@@ -235,11 +237,11 @@
by (auto intro!: antisym)
qed (metis suminf_zero fun_eq_iff)
-lemma suminf_pos_iff: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
+lemma suminf_pos_iff: "summable f \<Longrightarrow> (\<And>n. 0 \<le> f n) \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
using sum_le_suminf[of "{}"] suminf_eq_zero_iff by (simp add: less_le)
lemma suminf_pos2:
- assumes "summable f" "\<forall>n. 0 \<le> f n" "0 < f i"
+ assumes "summable f" "\<And>n. 0 \<le> f n" "0 < f i"
shows "0 < suminf f"
proof -
have "0 < (\<Sum>n<Suc i. f n)"
@@ -249,7 +251,7 @@
finally show ?thesis .
qed
-lemma suminf_pos: "summable f \<Longrightarrow> \<forall>n. 0 < f n \<Longrightarrow> 0 < suminf f"
+lemma suminf_pos: "summable f \<Longrightarrow> (\<And>n. 0 < f n) \<Longrightarrow> 0 < suminf f"
by (intro suminf_pos2[where i=0]) (auto intro: less_imp_le)
end
@@ -259,13 +261,13 @@
begin
lemma sum_less_suminf2:
- "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 \<le> f m \<Longrightarrow> n \<le> i \<Longrightarrow> 0 < f i \<Longrightarrow> sum f {..<n} < suminf f"
+ "summable f \<Longrightarrow> (\<And>m. m\<ge>n \<Longrightarrow> 0 \<le> f m) \<Longrightarrow> n \<le> i \<Longrightarrow> 0 < f i \<Longrightarrow> sum f {..<n} < suminf f"
using sum_le_suminf[of f "{..< Suc i}"]
and add_strict_increasing[of "f i" "sum f {..<n}" "sum f {..<i}"]
and sum_mono2[of "{..<i}" "{..<n}" f]
by (auto simp: less_imp_le ac_simps)
-lemma sum_less_suminf: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 < f m \<Longrightarrow> sum f {..<n} < suminf f"
+lemma sum_less_suminf: "summable f \<Longrightarrow> (\<And>m. m\<ge>n \<Longrightarrow> 0 < f m) \<Longrightarrow> sum f {..<n} < suminf f"
using sum_less_suminf2[of n n] by (simp add: less_imp_le)
end
@@ -460,11 +462,15 @@
by (auto simp: norm_minus_commute suminf_minus_initial_segment[OF \<open>summable f\<close>])
qed
-lemma summable_LIMSEQ_zero: "summable f \<Longrightarrow> f \<longlonglongrightarrow> 0"
- apply (drule summable_iff_convergent [THEN iffD1])
- apply (drule convergent_Cauchy)
- apply (simp only: Cauchy_iff LIMSEQ_iff)
- by (metis add.commute add_diff_cancel_right' diff_zero le_SucI sum.lessThan_Suc)
+lemma summable_LIMSEQ_zero:
+ assumes "summable f" shows "f \<longlonglongrightarrow> 0"
+proof -
+ have "Cauchy (\<lambda>n. sum f {..<n})"
+ using LIMSEQ_imp_Cauchy assms summable_LIMSEQ by blast
+ then show ?thesis
+ unfolding Cauchy_iff LIMSEQ_iff
+ by (metis add.commute add_diff_cancel_right' diff_zero le_SucI sum.lessThan_Suc)
+qed
lemma summable_imp_convergent: "summable f \<Longrightarrow> convergent f"
by (force dest!: summable_LIMSEQ_zero simp: convergent_def)
@@ -1286,7 +1292,6 @@
from eventually_conj[OF this bound] obtain x0 where x0:
"\<And>x. x \<ge> x0 \<Longrightarrow> \<bar>g x\<bar> < \<epsilon>" "\<And>a b. x0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> norm (sum f {a<..b}) \<le> g a"
unfolding eventually_at_top_linorder by auto
-
show ?case
proof (intro exI[of _ x0] allI impI)
fix m n assume mn: "x0 \<le> m" "m < n"
--- a/src/HOL/Transcendental.thy Wed Aug 26 15:59:21 2020 +0100
+++ b/src/HOL/Transcendental.thy Thu Aug 27 12:14:46 2020 +0100
@@ -743,7 +743,7 @@
then have "norm (suminf (g h)) \<le> (\<Sum>n. norm (g h n))"
by (rule summable_norm)
also from 1 3 2 have "(\<Sum>n. norm (g h n)) \<le> (\<Sum>n. f n * norm h)"
- by (rule suminf_le)
+ by (simp add: suminf_le)
also from f have "(\<Sum>n. f n * norm h) = suminf f * norm h"
by (rule suminf_mult2 [symmetric])
finally show "norm (suminf (g h)) \<le> suminf f * norm h" .
@@ -1003,7 +1003,7 @@
have *: "((\<lambda>x. if x = 0 then a 0 else f x) \<longlongrightarrow> a 0) (at 0)"
by (rule powser_limit_0 [OF s]) (auto simp: powser_sums_zero sm)
show ?thesis
- by (simp add: * LIM_equal [where g = "(\<lambda>x. if x = 0 then a 0 else f x)"])
+ using "*" by auto
qed
@@ -1574,10 +1574,7 @@
have "1 + x \<le> (\<Sum>n<2. inverse (fact n) * x^n)"
by (auto simp: numeral_2_eq_2)
also have "\<dots> \<le> (\<Sum>n. inverse (fact n) * x^n)"
- proof (rule sum_le_suminf [OF summable_exp])
- show "\<forall>m\<in>- {..<2}. 0 \<le> inverse (fact m) * x ^ m"
- using \<open>0 < x\<close> by (auto simp add: zero_le_mult_iff)
- qed auto
+ using \<open>0 < x\<close> by (auto simp add: zero_le_mult_iff intro: sum_le_suminf [OF summable_exp])
finally show "1 + x \<le> exp x"
by (simp add: exp_def)
qed auto
@@ -3643,9 +3640,7 @@
have sums: "?f sums sin x"
by (rule sin_paired [THEN sums_group]) simp
show "0 < sin x"
- unfolding sums_unique [OF sums]
- using sums_summable [OF sums] pos
- by (rule suminf_pos)
+ unfolding sums_unique [OF sums] using sums_summable [OF sums] pos by (simp add: suminf_pos)
qed
lemma cos_double_less_one: "0 < x \<Longrightarrow> x < 2 \<Longrightarrow> cos (2 * x) < 1"