# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1531319772 -3600
# Node ID 3cb44b0abc5c22582e8e5c32be1d4dc224acc338
# Parent  2fae3e01a2ecb7d3c504ca5290f56f1450cfcf07
more de-applying

diff -r 2fae3e01a2ec -r 3cb44b0abc5c src/HOL/Limits.thy
--- 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
 
 
diff -r 2fae3e01a2ec -r 3cb44b0abc5c src/HOL/Nonstandard_Analysis/HSEQ.thy
--- 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
diff -r 2fae3e01a2ec -r 3cb44b0abc5c src/HOL/Transcendental.thy
--- 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