author paulson Thu, 27 Aug 2020 12:14:46 +0100 changeset 72219 0f38c96a0a74 parent 72211 a6cbf8ce979e child 72220 bb29e4eb938d
tidying up some theorem statements
 src/HOL/Computational_Algebra/Polynomial.thy file | annotate | diff | comparison | revisions src/HOL/Deriv.thy file | annotate | diff | comparison | revisions src/HOL/Limits.thy file | annotate | diff | comparison | revisions src/HOL/Series.thy file | annotate | diff | comparison | revisions src/HOL/Transcendental.thy file | annotate | diff | comparison | revisions
--- 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
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]:
assumes "a = b"
and "x = y"
and "S = T"
@@ -2192,13 +2187,6 @@
unfolding tendsto_def eventually_at_topological
using assms by simp

-  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)
+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
+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)
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"