--- a/src/HOL/Limits.thy Wed Jul 11 09:47:09 2018 +0100
+++ b/src/HOL/Limits.thy Wed Jul 11 15:36:12 2018 +0100
@@ -23,24 +23,22 @@
corollary eventually_at_infinity_pos:
"eventually p at_infinity \<longleftrightarrow> (\<exists>b. 0 < b \<and> (\<forall>x. norm x \<ge> b \<longrightarrow> p x))"
- apply (simp add: eventually_at_infinity)
- apply auto
- apply (case_tac "b \<le> 0")
- using norm_ge_zero order_trans zero_less_one apply blast
- apply force
- done
+ unfolding eventually_at_infinity
+ by (meson le_less_trans norm_ge_zero not_le zero_less_one)
lemma at_infinity_eq_at_top_bot: "(at_infinity :: real filter) = sup at_top at_bot"
- apply (simp add: filter_eq_iff eventually_sup eventually_at_infinity
- eventually_at_top_linorder eventually_at_bot_linorder)
- apply safe
- apply (rule_tac x="b" in exI)
- apply simp
- apply (rule_tac x="- b" in exI)
- apply simp
- apply (rule_tac x="max (- Na) N" in exI)
- apply (auto simp: abs_real_def)
- done
+proof -
+ have 1: "\<lbrakk>\<forall>n\<ge>u. A n; \<forall>n\<le>v. A n\<rbrakk>
+ \<Longrightarrow> \<exists>b. \<forall>x. b \<le> \<bar>x\<bar> \<longrightarrow> A x" for A and u v::real
+ by (rule_tac x="max (- v) u" in exI) (auto simp: abs_real_def)
+ have 2: "\<forall>x. u \<le> \<bar>x\<bar> \<longrightarrow> A x \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. A n" for A and u::real
+ by (meson abs_less_iff le_cases less_le_not_le)
+ have 3: "\<forall>x. u \<le> \<bar>x\<bar> \<longrightarrow> A x \<Longrightarrow> \<exists>N. \<forall>n\<le>N. A n" for A and u::real
+ by (metis (full_types) abs_ge_self abs_minus_cancel le_minus_iff order_trans)
+ show ?thesis
+ by (auto simp add: filter_eq_iff eventually_sup eventually_at_infinity
+ eventually_at_top_linorder eventually_at_bot_linorder intro: 1 2 3)
+qed
lemma at_top_le_at_infinity: "at_top \<le> (at_infinity :: real filter)"
unfolding at_infinity_eq_at_top_bot by simp
@@ -103,19 +101,15 @@
obtains B where "0 < B" and "eventually (\<lambda>x. norm (f x) \<le> B) F"
using assms unfolding Bfun_def by blast
-lemma Cauchy_Bseq: "Cauchy X \<Longrightarrow> Bseq X"
- unfolding Cauchy_def Bfun_metric_def eventually_sequentially
- apply (erule_tac x=1 in allE)
- apply simp
- apply safe
- apply (rule_tac x="X M" in exI)
- apply (rule_tac x=1 in exI)
- apply (erule_tac x=M in allE)
- apply simp
- apply (rule_tac x=M in exI)
- apply (auto simp: dist_commute)
- done
-
+lemma Cauchy_Bseq:
+ assumes "Cauchy X" shows "Bseq X"
+proof -
+ have "\<exists>y K. 0 < K \<and> (\<exists>N. \<forall>n\<ge>N. dist (X n) y \<le> K)"
+ if "\<And>m n. \<lbrakk>m \<ge> M; n \<ge> M\<rbrakk> \<Longrightarrow> dist (X m) (X n) < 1" for M
+ by (meson order.order_iff_strict that zero_less_one)
+ with assms show ?thesis
+ by (force simp: Cauchy_def Bfun_metric_def eventually_sequentially)
+qed
subsubsection \<open>Bounded Sequences\<close>
@@ -202,15 +196,14 @@
by (simp add: Bseq_def) (simp add: lemma_NBseq_def)
lemma lemma_NBseq_def2: "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
- apply (subst lemma_NBseq_def)
- apply auto
- apply (rule_tac x = "Suc N" in exI)
- apply (rule_tac [2] x = N in exI)
- apply auto
- prefer 2 apply (blast intro: order_less_imp_le)
- apply (drule_tac x = n in spec)
- apply simp
- done
+proof -
+ have *: "\<And>N. \<forall>n. norm (X n) \<le> 1 + real N \<Longrightarrow>
+ \<exists>N. \<forall>n. norm (X n) < 1 + real N"
+ by (metis add.commute le_less_trans less_add_one of_nat_Suc)
+ then show ?thesis
+ unfolding lemma_NBseq_def
+ by (metis less_le_not_le not_less_iff_gr_or_eq of_nat_Suc)
+qed
text \<open>Yet another definition for Bseq.\<close>
lemma Bseq_iff1a: "Bseq X \<longleftrightarrow> (\<exists>N. \<forall>n. norm (X n) < real (Suc N))"
@@ -220,19 +213,8 @@
text \<open>Alternative formulation for boundedness.\<close>
lemma Bseq_iff2: "Bseq X \<longleftrightarrow> (\<exists>k > 0. \<exists>x. \<forall>n. norm (X n + - x) \<le> k)"
- apply (unfold Bseq_def)
- apply safe
- apply (rule_tac [2] x = "k + norm x" in exI)
- apply (rule_tac x = K in exI)
- apply simp
- apply (rule exI [where x = 0])
- apply auto
- apply (erule order_less_le_trans)
- apply simp
- apply (drule_tac x=n in spec)
- apply (drule order_trans [OF norm_triangle_ineq2])
- apply simp
- done
+ by (metis BseqE BseqI' add.commute add_cancel_right_left add_uminus_conv_diff norm_add_leD
+ norm_minus_cancel norm_minus_commute)
text \<open>Alternative formulation for boundedness.\<close>
lemma Bseq_iff3: "Bseq X \<longleftrightarrow> (\<exists>k>0. \<exists>N. \<forall>n. norm (X n + - X N) \<le> k)"
@@ -252,15 +234,6 @@
then show ?P by (auto simp add: Bseq_iff2)
qed
-lemma BseqI2: "\<forall>n. k \<le> f n \<and> f n \<le> K \<Longrightarrow> Bseq f"
- for k K :: real
- apply (simp add: Bseq_def)
- apply (rule_tac x = "(\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI)
- apply auto
- apply (drule_tac x = n in spec)
- apply arith
- done
-
subsubsection \<open>Upper Bounds and Lubs of Bounded Sequences\<close>
@@ -351,11 +324,13 @@
lemma Bseq_eq_bounded: "range f \<subseteq> {a..b} \<Longrightarrow> Bseq f"
for a b :: real
- apply (simp add: subset_eq)
- apply (rule BseqI'[where K="max (norm a) (norm b)"])
- apply (erule_tac x=n in allE)
- apply auto
- done
+proof (rule BseqI'[where K="max (norm a) (norm b)"])
+ fix n assume "range f \<subseteq> {a..b}"
+ then have "f n \<in> {a..b}"
+ by blast
+ then show "norm (f n) \<le> max (norm a) (norm b)"
+ by auto
+qed
lemma incseq_bounded: "incseq X \<Longrightarrow> \<forall>i. X i \<le> B \<Longrightarrow> Bseq X"
for B :: real
@@ -366,20 +341,6 @@
by (intro Bseq_eq_bounded[of X B "X 0"]) (auto simp: decseq_def)
-subsection \<open>Bounded Monotonic Sequences\<close>
-
-subsubsection \<open>A Bounded and Monotonic Sequence Converges\<close>
-
-(* TODO: delete *)
-(* FIXME: one use in NSA/HSEQ.thy *)
-lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n \<longrightarrow> X n = X m \<Longrightarrow> \<exists>L. X \<longlonglongrightarrow> L"
- apply (rule_tac x="X m" in exI)
- apply (rule filterlim_cong[THEN iffD2, OF refl refl _ tendsto_const])
- unfolding eventually_sequentially
- apply blast
- done
-
-
subsection \<open>Convergence to Zero\<close>
definition Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool"
@@ -2371,10 +2332,10 @@
text \<open>Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}.\<close>
-lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. \<bar>c\<bar> ^ n :: real) \<longlonglongrightarrow> 0"
+lemma LIMSEQ_abs_realpow_zero: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. \<bar>c\<bar> ^ n :: real) \<longlonglongrightarrow> 0"
by (rule LIMSEQ_realpow_zero [OF abs_ge_zero])
-lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. c ^ n :: real) \<longlonglongrightarrow> 0"
+lemma LIMSEQ_abs_realpow_zero2: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. c ^ n :: real) \<longlonglongrightarrow> 0"
by (rule LIMSEQ_power_zero) simp
--- a/src/HOL/Nonstandard_Analysis/HSEQ.thy Wed Jul 11 09:47:09 2018 +0100
+++ b/src/HOL/Nonstandard_Analysis/HSEQ.thy Wed Jul 11 15:36:12 2018 +0100
@@ -354,8 +354,9 @@
theorem and then use equivalence to "transfer" it into the
equivalent nonstandard form if needed!\<close>
-lemma Bmonoseq_NSLIMSEQ: "\<forall>n \<ge> m. X n = X m \<Longrightarrow> \<exists>L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
- by (auto dest!: Bmonoseq_LIMSEQ simp add: LIMSEQ_NSLIMSEQ_iff)
+lemma Bmonoseq_NSLIMSEQ: "\<forall>\<^sub>F k in sequentially. X k = X m \<Longrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S X m"
+ unfolding LIMSEQ_NSLIMSEQ_iff[symmetric]
+ by (simp add: eventually_mono eventually_nhds_x_imp_x filterlim_iff)
lemma NSBseq_mono_NSconvergent: "NSBseq X \<Longrightarrow> \<forall>m. \<forall>n \<ge> m. X m \<le> X n \<Longrightarrow> NSconvergent X"
for X :: "nat \<Rightarrow> real"
@@ -452,22 +453,22 @@
lemma NSconvergent_NSCauchy: "NSconvergent X \<Longrightarrow> NSCauchy X"
by (simp add: NSconvergent_def NSLIMSEQ_def NSCauchy_def) (auto intro: approx_trans2)
-lemma real_NSCauchy_NSconvergent: "NSCauchy X \<Longrightarrow> NSconvergent X"
- for X :: "nat \<Rightarrow> real"
- apply (simp add: NSconvergent_def NSLIMSEQ_def)
- apply (frule NSCauchy_NSBseq)
- apply (simp add: NSBseq_def NSCauchy_def)
- apply (drule HNatInfinite_whn [THEN [2] bspec])
- apply (drule HNatInfinite_whn [THEN [2] bspec])
- apply (auto dest!: st_part_Ex simp add: SReal_iff)
- apply (blast intro: approx_trans3)
- done
+lemma real_NSCauchy_NSconvergent:
+ fixes X :: "nat \<Rightarrow> real"
+ assumes "NSCauchy X" shows "NSconvergent X"
+ unfolding NSconvergent_def NSLIMSEQ_def
+proof -
+ have "( *f* X) whn \<in> HFinite"
+ by (simp add: NSBseqD2 NSCauchy_NSBseq assms)
+ moreover have "\<forall>N\<in>HNatInfinite. ( *f* X) whn \<approx> ( *f* X) N"
+ using HNatInfinite_whn NSCauchy_def assms by blast
+ ultimately show "\<exists>L. \<forall>N\<in>HNatInfinite. ( *f* X) N \<approx> hypreal_of_real L"
+ by (force dest!: st_part_Ex simp add: SReal_iff intro: approx_trans3)
+qed
lemma NSCauchy_NSconvergent: "NSCauchy X \<Longrightarrow> NSconvergent X"
for X :: "nat \<Rightarrow> 'a::banach"
- apply (drule NSCauchy_Cauchy [THEN Cauchy_convergent])
- apply (erule convergent_NSconvergent_iff [THEN iffD1])
- done
+ using Cauchy_convergent NSCauchy_Cauchy convergent_NSconvergent_iff by auto
lemma NSCauchy_NSconvergent_iff: "NSCauchy X = NSconvergent X"
for X :: "nat \<Rightarrow> 'a::banach"
@@ -481,42 +482,34 @@
also fact that bounded and monotonic sequence converges.\<close>
text \<open>We now use NS criterion to bring proof of theorem through.\<close>
-lemma NSLIMSEQ_realpow_zero: "0 \<le> x \<Longrightarrow> x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
- for x :: real
- apply (simp add: NSLIMSEQ_def)
- apply (auto dest!: convergent_realpow simp add: convergent_NSconvergent_iff)
- apply (frule NSconvergentD)
- apply (auto simp add: NSLIMSEQ_def NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfun_pow)
- apply (frule HNatInfinite_add_one)
- apply (drule bspec, assumption)
- apply (drule bspec, assumption)
- apply (drule_tac x = "N + 1" in bspec, assumption)
- apply (simp add: hyperpow_add)
- apply (drule approx_mult_subst_star_of, assumption)
- apply (drule approx_trans3, assumption)
- apply (auto simp del: star_of_mult simp add: star_of_mult [symmetric])
- done
+lemma NSLIMSEQ_realpow_zero:
+ fixes x :: real
+ assumes "0 \<le> x" "x < 1" shows "(\<lambda>n. x ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
+proof -
+ have "( *f* (^) x) N \<approx> 0"
+ if N: "N \<in> HNatInfinite" and x: "NSconvergent ((^) x)" for N
+ proof -
+ have "hypreal_of_real x pow N \<approx> hypreal_of_real x pow (N + 1)"
+ by (metis HNatInfinite_add N NSCauchy_NSconvergent_iff NSCauchy_def starfun_pow x)
+ moreover obtain L where L: "hypreal_of_real x pow N \<approx> hypreal_of_real L"
+ using NSconvergentD [OF x] N by (auto simp add: NSLIMSEQ_def starfun_pow)
+ ultimately have "hypreal_of_real x pow N \<approx> hypreal_of_real L * hypreal_of_real x"
+ by (simp add: approx_mult_subst_star_of hyperpow_add)
+ then have "hypreal_of_real L \<approx> hypreal_of_real L * hypreal_of_real x"
+ using L approx_trans3 by blast
+ then show ?thesis
+ by (metis L \<open>x < 1\<close> hyperpow_def less_irrefl mult.right_neutral mult_left_cancel star_of_approx_iff star_of_mult star_of_simps(9) starfun2_star_of)
+ qed
+ with assms show ?thesis
+ by (force dest!: convergent_realpow simp add: NSLIMSEQ_def convergent_NSconvergent_iff)
+qed
-lemma NSLIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. \<bar>c\<bar> ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
+lemma NSLIMSEQ_abs_realpow_zero: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. \<bar>c\<bar> ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
for c :: real
- by (simp add: LIMSEQ_rabs_realpow_zero LIMSEQ_NSLIMSEQ_iff [symmetric])
-
-lemma NSLIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. c ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
- for c :: real
- by (simp add: LIMSEQ_rabs_realpow_zero2 LIMSEQ_NSLIMSEQ_iff [symmetric])
+ by (simp add: LIMSEQ_abs_realpow_zero LIMSEQ_NSLIMSEQ_iff [symmetric])
-(***---------------------------------------------------------------
- Theorems proved by Harrison in HOL that we do not need
- in order to prove equivalence between Cauchy criterion
- and convergence:
- -- Show that every sequence contains a monotonic subsequence
-Goal "\<exists>f. subseq f & monoseq (%n. s (f n))"
- -- Show that a subsequence of a bounded sequence is bounded
-Goal "Bseq X ==> Bseq (%n. X (f n))";
- -- Show we can take subsequential terms arbitrarily far
- up a sequence
-Goal "subseq f ==> n \<le> f(n)";
-Goal "subseq f ==> \<exists>n. N1 \<le> n & N2 \<le> f(n)";
- ---------------------------------------------------------------***)
+lemma NSLIMSEQ_abs_realpow_zero2: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. c ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
+ for c :: real
+ by (simp add: LIMSEQ_abs_realpow_zero2 LIMSEQ_NSLIMSEQ_iff [symmetric])
end
--- a/src/HOL/Transcendental.thy Wed Jul 11 09:47:09 2018 +0100
+++ b/src/HOL/Transcendental.thy Wed Jul 11 15:36:12 2018 +0100
@@ -5697,16 +5697,9 @@
if x'_bounds: "x' \<in> {- 1 <..< 1}" for x' :: real
proof -
from that have "\<bar>x'\<bar> < 1" by auto
- then have *: "summable (\<lambda>n. (- 1) ^ n * x' ^ (2 * n))"
- by (rule summable_Integral)
- show ?thesis
- unfolding if_eq
- apply (rule sums_summable [where l="0 + (\<Sum>n. (-1)^n * x'^(2 * n))"])
- apply (rule sums_if)
- apply (rule sums_zero)
- apply (rule summable_sums)
- apply (rule *)
- done
+ then show ?thesis
+ using that sums_summable sums_if [OF sums_0 [of "\<lambda>x. 0"] summable_sums [OF summable_Integral]]
+ by (auto simp add: if_distrib [of "\<lambda>x. x * y" for y] cong: if_cong)
qed
qed auto
then show ?thesis