use filterlim in Lim and SEQ; tuned proofs
authorhoelzl
Mon Dec 03 18:19:12 2012 +0100 (2012-12-03)
changeset 503314b6dc5077e98
parent 50330 d0b12171118e
child 50332 2c7479865e07
use filterlim in Lim and SEQ; tuned proofs
src/HOL/Deriv.thy
src/HOL/Lim.thy
src/HOL/Limits.thy
src/HOL/SEQ.thy
src/HOL/Series.thy
     1.1 --- a/src/HOL/Deriv.thy	Mon Dec 03 18:19:11 2012 +0100
     1.2 +++ b/src/HOL/Deriv.thy	Mon Dec 03 18:19:12 2012 +0100
     1.3 @@ -76,7 +76,7 @@
     1.4  lemma DERIV_mult_lemma:
     1.5    fixes a b c d :: "'a::real_field"
     1.6    shows "(a * b - c * d) / h = a * ((b - d) / h) + ((a - c) / h) * d"
     1.7 -by (simp add: diff_minus add_divide_distrib [symmetric] ring_distribs)
     1.8 +  by (simp add: field_simps diff_divide_distrib)
     1.9  
    1.10  lemma DERIV_mult':
    1.11    assumes f: "DERIV f x :> D"
    1.12 @@ -97,15 +97,12 @@
    1.13  qed
    1.14  
    1.15  lemma DERIV_mult:
    1.16 -     "[| DERIV f x :> Da; DERIV g x :> Db |]
    1.17 -      ==> DERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))"
    1.18 -by (drule (1) DERIV_mult', simp only: mult_commute add_commute)
    1.19 +    "DERIV f x :> Da \<Longrightarrow> DERIV g x :> Db \<Longrightarrow> DERIV (\<lambda>x. f x * g x) x :> Da * g x + Db * f x"
    1.20 +  by (drule (1) DERIV_mult', simp only: mult_commute add_commute)
    1.21  
    1.22  lemma DERIV_unique:
    1.23 -      "[| DERIV f x :> D; DERIV f x :> E |] ==> D = E"
    1.24 -apply (simp add: deriv_def)
    1.25 -apply (blast intro: LIM_unique)
    1.26 -done
    1.27 +    "DERIV f x :> D \<Longrightarrow> DERIV f x :> E \<Longrightarrow> D = E"
    1.28 +  unfolding deriv_def by (rule LIM_unique) 
    1.29  
    1.30  text{*Differentiation of finite sum*}
    1.31  
     2.1 --- a/src/HOL/Lim.thy	Mon Dec 03 18:19:11 2012 +0100
     2.2 +++ b/src/HOL/Lim.thy	Mon Dec 03 18:19:12 2012 +0100
     2.3 @@ -323,36 +323,6 @@
     2.4    isCont_diff isCont_mult isCont_inverse isCont_divide isCont_scaleR
     2.5    isCont_of_real isCont_power isCont_sgn isCont_setsum
     2.6  
     2.7 -lemma LIM_less_bound: fixes f :: "real \<Rightarrow> real" assumes "b < x"
     2.8 -  and all_le: "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and isCont: "isCont f x"
     2.9 -  shows "0 \<le> f x"
    2.10 -proof (rule ccontr)
    2.11 -  assume "\<not> 0 \<le> f x" hence "f x < 0" by auto
    2.12 -  hence "0 < - f x / 2" by auto
    2.13 -  from isCont[unfolded isCont_def, THEN LIM_D, OF this]
    2.14 -  obtain s where "s > 0" and s_D: "\<And>x'. \<lbrakk> x' \<noteq> x ; \<bar> x' - x \<bar> < s \<rbrakk> \<Longrightarrow> \<bar> f x' - f x \<bar> < - f x / 2" by auto
    2.15 -
    2.16 -  let ?x = "x - min (s / 2) ((x - b) / 2)"
    2.17 -  have "?x < x" and "\<bar> ?x - x \<bar> < s"
    2.18 -    using `b < x` and `0 < s` by auto
    2.19 -  have "b < ?x"
    2.20 -  proof (cases "s < x - b")
    2.21 -    case True thus ?thesis using `0 < s` by auto
    2.22 -  next
    2.23 -    case False hence "s / 2 \<ge> (x - b) / 2" by auto
    2.24 -    hence "?x = (x + b) / 2" by (simp add: field_simps min_max.inf_absorb2)
    2.25 -    thus ?thesis using `b < x` by auto
    2.26 -  qed
    2.27 -  hence "0 \<le> f ?x" using all_le `?x < x` by auto
    2.28 -  moreover have "\<bar>f ?x - f x\<bar> < - f x / 2"
    2.29 -    using s_D[OF _ `\<bar> ?x - x \<bar> < s`] `?x < x` by auto
    2.30 -  hence "f ?x - f x < - f x / 2" by auto
    2.31 -  hence "f ?x < f x / 2" by auto
    2.32 -  hence "f ?x < 0" using `f x < 0` by auto
    2.33 -  thus False using `0 \<le> f ?x` by auto
    2.34 -qed
    2.35 -
    2.36 -
    2.37  subsection {* Uniform Continuity *}
    2.38  
    2.39  lemma isUCont_isCont: "isUCont f ==> isCont f x"
    2.40 @@ -442,4 +412,15 @@
    2.41     (X -- a --> (L::'b::topological_space))"
    2.42    using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..
    2.43  
    2.44 +lemma LIM_less_bound: 
    2.45 +  fixes f :: "real \<Rightarrow> real"
    2.46 +  assumes ev: "b < x" "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and "isCont f x"
    2.47 +  shows "0 \<le> f x"
    2.48 +proof (rule tendsto_le_const)
    2.49 +  show "(f ---> f x) (at_left x)"
    2.50 +    using `isCont f x` by (simp add: filterlim_at_split isCont_def)
    2.51 +  show "eventually (\<lambda>x. 0 \<le> f x) (at_left x)"
    2.52 +    using ev by (auto simp: eventually_within_less dist_real_def intro!: exI[of _ "x - b"])
    2.53 +qed simp
    2.54 +
    2.55  end
     3.1 --- a/src/HOL/Limits.thy	Mon Dec 03 18:19:11 2012 +0100
     3.2 +++ b/src/HOL/Limits.thy	Mon Dec 03 18:19:12 2012 +0100
     3.3 @@ -463,6 +463,22 @@
     3.4  lemma at_neq_bot [simp]: "at (a::'a::perfect_space) \<noteq> bot"
     3.5    by (simp add: at_eq_bot_iff not_open_singleton)
     3.6  
     3.7 +lemma trivial_limit_at_left_real [simp]: (* maybe generalize type *)
     3.8 +  "\<not> trivial_limit (at_left (x::real))"
     3.9 +  unfolding trivial_limit_def eventually_within_le
    3.10 +  apply clarsimp
    3.11 +  apply (rule_tac x="x - d/2" in bexI)
    3.12 +  apply (auto simp: dist_real_def)
    3.13 +  done
    3.14 +
    3.15 +lemma trivial_limit_at_right_real [simp]: (* maybe generalize type *)
    3.16 +  "\<not> trivial_limit (at_right (x::real))"
    3.17 +  unfolding trivial_limit_def eventually_within_le
    3.18 +  apply clarsimp
    3.19 +  apply (rule_tac x="x + d/2" in bexI)
    3.20 +  apply (auto simp: dist_real_def)
    3.21 +  done
    3.22 +
    3.23  lemma eventually_at_infinity:
    3.24    "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. b \<le> norm x \<longrightarrow> P x)"
    3.25  unfolding at_infinity_def
    3.26 @@ -713,6 +729,9 @@
    3.27    "filterlim f F F1 \<Longrightarrow> filterlim f F F2 \<Longrightarrow> filterlim f F (sup F1 F2)"
    3.28    unfolding filterlim_def filtermap_sup by auto
    3.29  
    3.30 +lemma filterlim_Suc: "filterlim Suc sequentially sequentially"
    3.31 +  by (simp add: filterlim_iff eventually_sequentially) (metis le_Suc_eq)
    3.32 +
    3.33  abbreviation (in topological_space)
    3.34    tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "--->" 55) where
    3.35    "(f ---> l) F \<equiv> filterlim f (nhds l) F"
    3.36 @@ -1027,6 +1046,30 @@
    3.37      by (simp add: tendsto_const)
    3.38  qed
    3.39  
    3.40 +lemma tendsto_le_const:
    3.41 +  fixes f :: "_ \<Rightarrow> real" 
    3.42 +  assumes F: "\<not> trivial_limit F"
    3.43 +  assumes x: "(f ---> x) F" and a: "eventually (\<lambda>x. a \<le> f x) F"
    3.44 +  shows "a \<le> x"
    3.45 +proof (rule ccontr)
    3.46 +  assume "\<not> a \<le> x"
    3.47 +  with x have "eventually (\<lambda>x. f x < a) F"
    3.48 +    by (auto simp add: tendsto_def elim!: allE[of _ "{..< a}"])
    3.49 +  with a have "eventually (\<lambda>x. False) F"
    3.50 +    by eventually_elim auto
    3.51 +  with F show False
    3.52 +    by (simp add: eventually_False)
    3.53 +qed
    3.54 +
    3.55 +lemma tendsto_le:
    3.56 +  fixes f g :: "_ \<Rightarrow> real" 
    3.57 +  assumes F: "\<not> trivial_limit F"
    3.58 +  assumes x: "(f ---> x) F" and y: "(g ---> y) F"
    3.59 +  assumes ev: "eventually (\<lambda>x. g x \<le> f x) F"
    3.60 +  shows "y \<le> x"
    3.61 +  using tendsto_le_const[OF F tendsto_diff[OF x y], of 0] ev
    3.62 +  by (simp add: sign_simps)
    3.63 +
    3.64  subsubsection {* Inverse and division *}
    3.65  
    3.66  lemma (in bounded_bilinear) Zfun_prod_Bfun:
    3.67 @@ -1382,6 +1425,44 @@
    3.68      by eventually_elim simp
    3.69  qed
    3.70  
    3.71 +lemma tendsto_divide_0:
    3.72 +  fixes f :: "_ \<Rightarrow> 'a\<Colon>{real_normed_div_algebra, division_ring_inverse_zero}"
    3.73 +  assumes f: "(f ---> c) F"
    3.74 +  assumes g: "LIM x F. g x :> at_infinity"
    3.75 +  shows "((\<lambda>x. f x / g x) ---> 0) F"
    3.76 +  using tendsto_mult[OF f filterlim_compose[OF tendsto_inverse_0 g]] by (simp add: divide_inverse)
    3.77 +
    3.78 +lemma linear_plus_1_le_power:
    3.79 +  fixes x :: real
    3.80 +  assumes x: "0 \<le> x"
    3.81 +  shows "real n * x + 1 \<le> (x + 1) ^ n"
    3.82 +proof (induct n)
    3.83 +  case (Suc n)
    3.84 +  have "real (Suc n) * x + 1 \<le> (x + 1) * (real n * x + 1)"
    3.85 +    by (simp add: field_simps real_of_nat_Suc mult_nonneg_nonneg x)
    3.86 +  also have "\<dots> \<le> (x + 1)^Suc n"
    3.87 +    using Suc x by (simp add: mult_left_mono)
    3.88 +  finally show ?case .
    3.89 +qed simp
    3.90 +
    3.91 +lemma filterlim_realpow_sequentially_gt1:
    3.92 +  fixes x :: "'a :: real_normed_div_algebra"
    3.93 +  assumes x[arith]: "1 < norm x"
    3.94 +  shows "LIM n sequentially. x ^ n :> at_infinity"
    3.95 +proof (intro filterlim_at_infinity[THEN iffD2] allI impI)
    3.96 +  fix y :: real assume "0 < y"
    3.97 +  have "0 < norm x - 1" by simp
    3.98 +  then obtain N::nat where "y < real N * (norm x - 1)" by (blast dest: reals_Archimedean3)
    3.99 +  also have "\<dots> \<le> real N * (norm x - 1) + 1" by simp
   3.100 +  also have "\<dots> \<le> (norm x - 1 + 1) ^ N" by (rule linear_plus_1_le_power) simp
   3.101 +  also have "\<dots> = norm x ^ N" by simp
   3.102 +  finally have "\<forall>n\<ge>N. y \<le> norm x ^ n"
   3.103 +    by (metis order_less_le_trans power_increasing order_less_imp_le x)
   3.104 +  then show "eventually (\<lambda>n. y \<le> norm (x ^ n)) sequentially"
   3.105 +    unfolding eventually_sequentially
   3.106 +    by (auto simp: norm_power)
   3.107 +qed simp
   3.108 +
   3.109  subsection {* Relate @{const at}, @{const at_left} and @{const at_right} *}
   3.110  
   3.111  text {*
     4.1 --- a/src/HOL/SEQ.thy	Mon Dec 03 18:19:11 2012 +0100
     4.2 +++ b/src/HOL/SEQ.thy	Mon Dec 03 18:19:12 2012 +0100
     4.3 @@ -171,6 +171,9 @@
     4.4    thus ?case by arith
     4.5  qed
     4.6  
     4.7 +lemma filterlim_subseq: "subseq f \<Longrightarrow> filterlim f sequentially sequentially"
     4.8 +  unfolding filterlim_iff eventually_sequentially by (metis le_trans seq_suble)
     4.9 +
    4.10  lemma subseq_o: "subseq r \<Longrightarrow> subseq s \<Longrightarrow> subseq (r \<circ> s)"
    4.11    unfolding subseq_def by simp
    4.12  
    4.13 @@ -357,36 +360,23 @@
    4.14  
    4.15  lemma increasing_LIMSEQ:
    4.16    fixes f :: "nat \<Rightarrow> real"
    4.17 -  assumes inc: "!!n. f n \<le> f (Suc n)"
    4.18 -      and bdd: "!!n. f n \<le> l"
    4.19 -      and en: "!!e. 0 < e \<Longrightarrow> \<exists>n. l \<le> f n + e"
    4.20 +  assumes inc: "\<And>n. f n \<le> f (Suc n)"
    4.21 +      and bdd: "\<And>n. f n \<le> l"
    4.22 +      and en: "\<And>e. 0 < e \<Longrightarrow> \<exists>n. l \<le> f n + e"
    4.23    shows "f ----> l"
    4.24 -proof (auto simp add: LIMSEQ_def)
    4.25 -  fix e :: real
    4.26 -  assume e: "0 < e"
    4.27 -  then obtain N where "l \<le> f N + e/2"
    4.28 -    by (metis half_gt_zero e en that)
    4.29 -  hence N: "l < f N + e" using e
    4.30 -    by simp
    4.31 -  { fix k
    4.32 -    have [simp]: "!!n. \<bar>f n - l\<bar> = l - f n"
    4.33 -      by (simp add: bdd) 
    4.34 -    have "\<bar>f (N+k) - l\<bar> < e"
    4.35 -    proof (induct k)
    4.36 -      case 0 show ?case using N
    4.37 -        by simp   
    4.38 -    next
    4.39 -      case (Suc k) thus ?case using N inc [of "N+k"]
    4.40 -        by simp
    4.41 -    qed 
    4.42 -  } note 1 = this
    4.43 -  { fix n
    4.44 -    have "N \<le> n \<Longrightarrow> \<bar>f n - l\<bar> < e" using 1 [of "n-N"]
    4.45 -      by simp 
    4.46 -  } note [intro] = this
    4.47 -  show " \<exists>no. \<forall>n\<ge>no. dist (f n) l < e"
    4.48 -    by (auto simp add: dist_real_def) 
    4.49 -  qed
    4.50 +  unfolding LIMSEQ_def
    4.51 +proof safe
    4.52 +  fix r :: real assume "0 < r"
    4.53 +  with bdd en[of "r / 2"] obtain n where n: "dist (f n) l \<le> r / 2"
    4.54 +    by (auto simp add: field_simps dist_real_def)
    4.55 +  { fix N assume "n \<le> N"
    4.56 +    then have "dist (f N) l \<le> dist (f n) l"
    4.57 +      using incseq_SucI[of f] inc bdd by (auto dest!: incseqD simp: dist_real_def)
    4.58 +    then have "dist (f N) l < r"
    4.59 +      using `0 < r` n by simp }
    4.60 +  with `0 < r` show "\<exists>no. \<forall>n\<ge>no. dist (f n) l < r"
    4.61 +    by (auto simp add: LIMSEQ_def field_simps intro!: exI[of _ n])
    4.62 +qed
    4.63  
    4.64  lemma Bseq_inverse_lemma:
    4.65    fixes x :: "'a::real_normed_div_algebra"
    4.66 @@ -414,24 +404,16 @@
    4.67  
    4.68  lemma LIMSEQ_inverse_zero:
    4.69    "\<forall>r::real. \<exists>N. \<forall>n\<ge>N. r < X n \<Longrightarrow> (\<lambda>n. inverse (X n)) ----> 0"
    4.70 -apply (rule LIMSEQ_I)
    4.71 -apply (drule_tac x="inverse r" in spec, safe)
    4.72 -apply (rule_tac x="N" in exI, safe)
    4.73 -apply (drule_tac x="n" in spec, safe)
    4.74 -apply (frule positive_imp_inverse_positive)
    4.75 -apply (frule (1) less_imp_inverse_less)
    4.76 -apply (subgoal_tac "0 < X n", simp)
    4.77 -apply (erule (1) order_less_trans)
    4.78 -done
    4.79 +  apply (rule filterlim_compose[OF tendsto_inverse_0])
    4.80 +  apply (simp add: filterlim_at_infinity[OF order_refl] eventually_sequentially)
    4.81 +  apply (metis abs_le_D1 linorder_le_cases linorder_not_le)
    4.82 +  done
    4.83  
    4.84  text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*}
    4.85  
    4.86  lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0"
    4.87 -apply (rule LIMSEQ_inverse_zero, safe)
    4.88 -apply (cut_tac x = r in reals_Archimedean2)
    4.89 -apply (safe, rule_tac x = n in exI)
    4.90 -apply (auto simp add: real_of_nat_Suc)
    4.91 -done
    4.92 +  by (metis filterlim_compose tendsto_inverse_0 filterlim_mono order_refl filterlim_Suc
    4.93 +            filterlim_compose[OF filterlim_real_sequentially] at_top_le_at_infinity)
    4.94  
    4.95  text{*The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to
    4.96  infinity is now easily proved*}
    4.97 @@ -442,41 +424,25 @@
    4.98  
    4.99  lemma LIMSEQ_inverse_real_of_nat_add_minus:
   4.100       "(%n. r + -inverse(real(Suc n))) ----> r"
   4.101 -  using tendsto_add [OF tendsto_const
   4.102 -    tendsto_minus [OF LIMSEQ_inverse_real_of_nat]] by auto
   4.103 +  using tendsto_add [OF tendsto_const tendsto_minus [OF LIMSEQ_inverse_real_of_nat]]
   4.104 +  by auto
   4.105  
   4.106  lemma LIMSEQ_inverse_real_of_nat_add_minus_mult:
   4.107       "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r"
   4.108 -  using tendsto_mult [OF tendsto_const
   4.109 -    LIMSEQ_inverse_real_of_nat_add_minus [of 1]]
   4.110 +  using tendsto_mult [OF tendsto_const LIMSEQ_inverse_real_of_nat_add_minus [of 1]]
   4.111    by auto
   4.112  
   4.113  lemma LIMSEQ_le_const:
   4.114    "\<lbrakk>X ----> (x::real); \<exists>N. \<forall>n\<ge>N. a \<le> X n\<rbrakk> \<Longrightarrow> a \<le> x"
   4.115 -apply (rule ccontr, simp only: linorder_not_le)
   4.116 -apply (drule_tac r="a - x" in LIMSEQ_D, simp)
   4.117 -apply clarsimp
   4.118 -apply (drule_tac x="max N no" in spec, drule mp, rule le_maxI1)
   4.119 -apply (drule_tac x="max N no" in spec, drule mp, rule le_maxI2)
   4.120 -apply simp
   4.121 -done
   4.122 +  using tendsto_le_const[of sequentially X x a] by (simp add: eventually_sequentially)
   4.123 +
   4.124 +lemma LIMSEQ_le:
   4.125 +  "\<lbrakk>X ----> x; Y ----> y; \<exists>N. \<forall>n\<ge>N. X n \<le> Y n\<rbrakk> \<Longrightarrow> x \<le> (y::real)"
   4.126 +  using tendsto_le[of sequentially Y y X x] by (simp add: eventually_sequentially)
   4.127  
   4.128  lemma LIMSEQ_le_const2:
   4.129    "\<lbrakk>X ----> (x::real); \<exists>N. \<forall>n\<ge>N. X n \<le> a\<rbrakk> \<Longrightarrow> x \<le> a"
   4.130 -apply (subgoal_tac "- a \<le> - x", simp)
   4.131 -apply (rule LIMSEQ_le_const)
   4.132 -apply (erule tendsto_minus)
   4.133 -apply simp
   4.134 -done
   4.135 -
   4.136 -lemma LIMSEQ_le:
   4.137 -  "\<lbrakk>X ----> x; Y ----> y; \<exists>N. \<forall>n\<ge>N. X n \<le> Y n\<rbrakk> \<Longrightarrow> x \<le> (y::real)"
   4.138 -apply (subgoal_tac "0 \<le> y - x", simp)
   4.139 -apply (rule LIMSEQ_le_const)
   4.140 -apply (erule (1) tendsto_diff)
   4.141 -apply (simp add: le_diff_eq)
   4.142 -done
   4.143 -
   4.144 +  by (rule LIMSEQ_le[of X x "\<lambda>n. a"]) (auto simp: tendsto_const)
   4.145  
   4.146  subsection {* Convergence *}
   4.147  
   4.148 @@ -531,88 +497,17 @@
   4.149  apply (drule tendsto_minus, auto)
   4.150  done
   4.151  
   4.152 -lemma lim_le:
   4.153 -  fixes x :: real
   4.154 -  assumes f: "convergent f" and fn_le: "!!n. f n \<le> x"
   4.155 -  shows "lim f \<le> x"
   4.156 -proof (rule classical)
   4.157 -  assume "\<not> lim f \<le> x"
   4.158 -  hence 0: "0 < lim f - x" by arith
   4.159 -  have 1: "f----> lim f"
   4.160 -    by (metis convergent_LIMSEQ_iff f) 
   4.161 -  thus ?thesis
   4.162 -    proof (simp add: LIMSEQ_iff)
   4.163 -      assume "\<forall>r>0. \<exists>no. \<forall>n\<ge>no. \<bar>f n - lim f\<bar> < r"
   4.164 -      hence "\<exists>no. \<forall>n\<ge>no. \<bar>f n - lim f\<bar> < lim f - x"
   4.165 -        by (metis 0)
   4.166 -      from this obtain no where "\<forall>n\<ge>no. \<bar>f n - lim f\<bar> < lim f - x"
   4.167 -        by blast
   4.168 -      thus "lim f \<le> x"
   4.169 -        by (metis 1 LIMSEQ_le_const2 fn_le)
   4.170 -    qed
   4.171 -qed
   4.172 +lemma lim_le: "convergent f \<Longrightarrow> (\<And>n. f n \<le> (x::real)) \<Longrightarrow> lim f \<le> x"
   4.173 +  using LIMSEQ_le_const2[of f "lim f" x] by (simp add: convergent_LIMSEQ_iff)
   4.174  
   4.175  lemma monoseq_le:
   4.176 -  fixes a :: "nat \<Rightarrow> real"
   4.177 -  assumes "monoseq a" and "a ----> x"
   4.178 -  shows "((\<forall> n. a n \<le> x) \<and> (\<forall>m. \<forall>n\<ge>m. a m \<le> a n)) \<or> 
   4.179 -         ((\<forall> n. x \<le> a n) \<and> (\<forall>m. \<forall>n\<ge>m. a n \<le> a m))"
   4.180 -proof -
   4.181 -  { fix x n fix a :: "nat \<Rightarrow> real"
   4.182 -    assume "a ----> x" and "\<forall> m. \<forall> n \<ge> m. a m \<le> a n"
   4.183 -    hence monotone: "\<And> m n. m \<le> n \<Longrightarrow> a m \<le> a n" by auto
   4.184 -    have "a n \<le> x"
   4.185 -    proof (rule ccontr)
   4.186 -      assume "\<not> a n \<le> x" hence "x < a n" by auto
   4.187 -      hence "0 < a n - x" by auto
   4.188 -      from `a ----> x`[THEN LIMSEQ_D, OF this]
   4.189 -      obtain no where "\<And>n'. no \<le> n' \<Longrightarrow> norm (a n' - x) < a n - x" by blast
   4.190 -      hence "norm (a (max no n) - x) < a n - x" by auto
   4.191 -      moreover
   4.192 -      { fix n' have "n \<le> n' \<Longrightarrow> x < a n'" using monotone[where m=n and n=n'] and `x < a n` by auto }
   4.193 -      hence "x < a (max no n)" by auto
   4.194 -      ultimately
   4.195 -      have "a (max no n) < a n" by auto
   4.196 -      with monotone[where m=n and n="max no n"]
   4.197 -      show False by (auto simp:max_def split:split_if_asm)
   4.198 -    qed
   4.199 -  } note top_down = this
   4.200 -  { fix x n m fix a :: "nat \<Rightarrow> real"
   4.201 -    assume "a ----> x" and "monoseq a" and "a m < x"
   4.202 -    have "a n \<le> x \<and> (\<forall> m. \<forall> n \<ge> m. a m \<le> a n)"
   4.203 -    proof (cases "\<forall> m. \<forall> n \<ge> m. a m \<le> a n")
   4.204 -      case True with top_down and `a ----> x` show ?thesis by auto
   4.205 -    next
   4.206 -      case False with `monoseq a`[unfolded monoseq_def] have "\<forall> m. \<forall> n \<ge> m. - a m \<le> - a n" by auto
   4.207 -      hence "- a m \<le> - x" using top_down[OF tendsto_minus[OF `a ----> x`]] by blast
   4.208 -      hence False using `a m < x` by auto
   4.209 -      thus ?thesis ..
   4.210 -    qed
   4.211 -  } note when_decided = this
   4.212 -
   4.213 -  show ?thesis
   4.214 -  proof (cases "\<exists> m. a m \<noteq> x")
   4.215 -    case True then obtain m where "a m \<noteq> x" by auto
   4.216 -    show ?thesis
   4.217 -    proof (cases "a m < x")
   4.218 -      case True with when_decided[OF `a ----> x` `monoseq a`, where m2=m]
   4.219 -      show ?thesis by blast
   4.220 -    next
   4.221 -      case False hence "- a m < - x" using `a m \<noteq> x` by auto
   4.222 -      with when_decided[OF tendsto_minus[OF `a ----> x`] monoseq_minus[OF `monoseq a`], where m2=m]
   4.223 -      show ?thesis by auto
   4.224 -    qed
   4.225 -  qed auto
   4.226 -qed
   4.227 +  "monoseq a \<Longrightarrow> a ----> (x::real) \<Longrightarrow>
   4.228 +    ((\<forall> n. a n \<le> x) \<and> (\<forall>m. \<forall>n\<ge>m. a m \<le> a n)) \<or> ((\<forall> n. x \<le> a n) \<and> (\<forall>m. \<forall>n\<ge>m. a n \<le> a m))"
   4.229 +  by (metis LIMSEQ_le_const LIMSEQ_le_const2 decseq_def incseq_def monoseq_iff)
   4.230  
   4.231  lemma LIMSEQ_subseq_LIMSEQ:
   4.232    "\<lbrakk> X ----> L; subseq f \<rbrakk> \<Longrightarrow> (X o f) ----> L"
   4.233 -apply (rule topological_tendstoI)
   4.234 -apply (drule (2) topological_tendstoD)
   4.235 -apply (simp only: eventually_sequentially)
   4.236 -apply (clarify, rule_tac x=N in exI, clarsimp)
   4.237 -apply (blast intro: seq_suble le_trans dest!: spec) 
   4.238 -done
   4.239 +  unfolding comp_def by (rule filterlim_compose[of X, OF _ filterlim_subseq])
   4.240  
   4.241  lemma convergent_subseq_convergent:
   4.242    "\<lbrakk>convergent X; subseq f\<rbrakk> \<Longrightarrow> convergent (X o f)"
   4.243 @@ -630,27 +525,16 @@
   4.244  by (auto simp add: Bseq_def)
   4.245  
   4.246  lemma lemma_NBseq_def:
   4.247 -     "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) =
   4.248 -      (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
   4.249 -proof auto
   4.250 +  "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
   4.251 +proof safe
   4.252    fix K :: real
   4.253    from reals_Archimedean2 obtain n :: nat where "K < real n" ..
   4.254    then have "K \<le> real (Suc n)" by auto
   4.255 -  assume "\<forall>m. norm (X m) \<le> K"
   4.256 -  have "\<forall>m. norm (X m) \<le> real (Suc n)"
   4.257 -  proof
   4.258 -    fix m :: 'a
   4.259 -    from `\<forall>m. norm (X m) \<le> K` have "norm (X m) \<le> K" ..
   4.260 -    with `K \<le> real (Suc n)` show "norm (X m) \<le> real (Suc n)" by auto
   4.261 -  qed
   4.262 +  moreover assume "\<forall>m. norm (X m) \<le> K"
   4.263 +  ultimately have "\<forall>m. norm (X m) \<le> real (Suc n)"
   4.264 +    by (blast intro: order_trans)
   4.265    then show "\<exists>N. \<forall>n. norm (X n) \<le> real (Suc N)" ..
   4.266 -next
   4.267 -  fix N :: nat
   4.268 -  have "real (Suc N) > 0" by (simp add: real_of_nat_Suc)
   4.269 -  moreover assume "\<forall>n. norm (X n) \<le> real (Suc N)"
   4.270 -  ultimately show "\<exists>K>0. \<forall>n. norm (X n) \<le> K" by blast
   4.271 -qed
   4.272 -
   4.273 +qed (force simp add: real_of_nat_Suc)
   4.274  
   4.275  text{* alternative definition for Bseq *}
   4.276  lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
   4.277 @@ -672,6 +556,39 @@
   4.278  lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
   4.279  by (simp add: Bseq_def lemma_NBseq_def2)
   4.280  
   4.281 +subsubsection{*A Few More Equivalence Theorems for Boundedness*}
   4.282 +
   4.283 +text{*alternative formulation for boundedness*}
   4.284 +lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. norm (X(n) + -x) \<le> k)"
   4.285 +apply (unfold Bseq_def, safe)
   4.286 +apply (rule_tac [2] x = "k + norm x" in exI)
   4.287 +apply (rule_tac x = K in exI, simp)
   4.288 +apply (rule exI [where x = 0], auto)
   4.289 +apply (erule order_less_le_trans, simp)
   4.290 +apply (drule_tac x=n in spec, fold diff_minus)
   4.291 +apply (drule order_trans [OF norm_triangle_ineq2])
   4.292 +apply simp
   4.293 +done
   4.294 +
   4.295 +text{*alternative formulation for boundedness*}
   4.296 +lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. norm(X(n) + -X(N)) \<le> k)"
   4.297 +apply safe
   4.298 +apply (simp add: Bseq_def, safe)
   4.299 +apply (rule_tac x = "K + norm (X N)" in exI)
   4.300 +apply auto
   4.301 +apply (erule order_less_le_trans, simp)
   4.302 +apply (rule_tac x = N in exI, safe)
   4.303 +apply (drule_tac x = n in spec)
   4.304 +apply (rule order_trans [OF norm_triangle_ineq], simp)
   4.305 +apply (auto simp add: Bseq_iff2)
   4.306 +done
   4.307 +
   4.308 +lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> (K::real)) ==> Bseq f"
   4.309 +apply (simp add: Bseq_def)
   4.310 +apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI, auto)
   4.311 +apply (drule_tac x = n in spec, arith)
   4.312 +done
   4.313 +
   4.314  subsubsection{*Upper Bounds and Lubs of Bounded Sequences*}
   4.315  
   4.316  lemma Bseq_isUb:
   4.317 @@ -725,115 +642,43 @@
   4.318  text{*A standard proof of the theorem for monotone increasing sequence*}
   4.319  
   4.320  lemma Bseq_mono_convergent:
   4.321 -     "[| Bseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> convergent (X::nat=>real)"
   4.322 -proof -
   4.323 -  assume "Bseq X"
   4.324 -  then obtain u where u: "isLub UNIV {x. \<exists>n. X n = x} u"
   4.325 -    using Bseq_isLub by fast
   4.326 -  assume "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
   4.327 -  with u have "X ----> u"
   4.328 -    by (rule isLub_mono_imp_LIMSEQ)
   4.329 -  thus "convergent X"
   4.330 -    by (rule convergentI)
   4.331 -qed
   4.332 +   "Bseq X \<Longrightarrow> \<forall>m. \<forall>n \<ge> m. X m \<le> X n \<Longrightarrow> convergent (X::nat=>real)"
   4.333 +  by (metis Bseq_isLub isLub_mono_imp_LIMSEQ convergentI)
   4.334  
   4.335  lemma Bseq_minus_iff: "Bseq (%n. -(X n)) = Bseq X"
   4.336 -by (simp add: Bseq_def)
   4.337 +  by (simp add: Bseq_def)
   4.338  
   4.339  text{*Main monotonicity theorem*}
   4.340 -lemma Bseq_monoseq_convergent: "[| Bseq X; monoseq X |] ==> convergent (X::nat\<Rightarrow>real)"
   4.341 -apply (simp add: monoseq_def, safe)
   4.342 -apply (rule_tac [2] convergent_minus_iff [THEN ssubst])
   4.343 -apply (drule_tac [2] Bseq_minus_iff [THEN ssubst])
   4.344 -apply (auto intro!: Bseq_mono_convergent)
   4.345 -done
   4.346 +
   4.347 +lemma Bseq_monoseq_convergent: "Bseq X \<Longrightarrow> monoseq X \<Longrightarrow> convergent (X::nat\<Rightarrow>real)"
   4.348 +  by (metis monoseq_iff incseq_def decseq_eq_incseq convergent_minus_iff Bseq_minus_iff
   4.349 +            Bseq_mono_convergent)
   4.350  
   4.351  subsubsection{*Increasing and Decreasing Series*}
   4.352  
   4.353 -lemma incseq_le:
   4.354 -  fixes X :: "nat \<Rightarrow> real"
   4.355 -  assumes inc: "incseq X" and lim: "X ----> L" shows "X n \<le> L"
   4.356 -  using monoseq_le [OF incseq_imp_monoseq [OF inc] lim]
   4.357 -proof
   4.358 -  assume "(\<forall>n. X n \<le> L) \<and> (\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n)"
   4.359 -  thus ?thesis by simp
   4.360 -next
   4.361 -  assume "(\<forall>n. L \<le> X n) \<and> (\<forall>m n. m \<le> n \<longrightarrow> X n \<le> X m)"
   4.362 -  hence const: "(!!m n. m \<le> n \<Longrightarrow> X n = X m)" using inc
   4.363 -    by (auto simp add: incseq_def intro: order_antisym)
   4.364 -  have X: "!!n. X n = X 0"
   4.365 -    by (blast intro: const [of 0]) 
   4.366 -  have "X = (\<lambda>n. X 0)"
   4.367 -    by (blast intro: X)
   4.368 -  hence "L = X 0" using tendsto_const [of "X 0" sequentially]
   4.369 -    by (auto intro: LIMSEQ_unique lim)
   4.370 -  thus ?thesis
   4.371 -    by (blast intro: eq_refl X)
   4.372 -qed
   4.373 -
   4.374 -lemma decseq_le:
   4.375 -  fixes X :: "nat \<Rightarrow> real" assumes dec: "decseq X" and lim: "X ----> L" shows "L \<le> X n"
   4.376 -proof -
   4.377 -  have inc: "incseq (\<lambda>n. - X n)" using dec
   4.378 -    by (simp add: decseq_eq_incseq)
   4.379 -  have "- X n \<le> - L" 
   4.380 -    by (blast intro: incseq_le [OF inc] tendsto_minus lim) 
   4.381 -  thus ?thesis
   4.382 -    by simp
   4.383 -qed
   4.384 +lemma incseq_le: "incseq X \<Longrightarrow> X ----> L \<Longrightarrow> X n \<le> (L::real)"
   4.385 +  by (metis incseq_def LIMSEQ_le_const)
   4.386  
   4.387 -subsubsection{*A Few More Equivalence Theorems for Boundedness*}
   4.388 -
   4.389 -text{*alternative formulation for boundedness*}
   4.390 -lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. norm (X(n) + -x) \<le> k)"
   4.391 -apply (unfold Bseq_def, safe)
   4.392 -apply (rule_tac [2] x = "k + norm x" in exI)
   4.393 -apply (rule_tac x = K in exI, simp)
   4.394 -apply (rule exI [where x = 0], auto)
   4.395 -apply (erule order_less_le_trans, simp)
   4.396 -apply (drule_tac x=n in spec, fold diff_minus)
   4.397 -apply (drule order_trans [OF norm_triangle_ineq2])
   4.398 -apply simp
   4.399 -done
   4.400 -
   4.401 -text{*alternative formulation for boundedness*}
   4.402 -lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. norm(X(n) + -X(N)) \<le> k)"
   4.403 -apply safe
   4.404 -apply (simp add: Bseq_def, safe)
   4.405 -apply (rule_tac x = "K + norm (X N)" in exI)
   4.406 -apply auto
   4.407 -apply (erule order_less_le_trans, simp)
   4.408 -apply (rule_tac x = N in exI, safe)
   4.409 -apply (drule_tac x = n in spec)
   4.410 -apply (rule order_trans [OF norm_triangle_ineq], simp)
   4.411 -apply (auto simp add: Bseq_iff2)
   4.412 -done
   4.413 -
   4.414 -lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> (K::real)) ==> Bseq f"
   4.415 -apply (simp add: Bseq_def)
   4.416 -apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI, auto)
   4.417 -apply (drule_tac x = n in spec, arith)
   4.418 -done
   4.419 -
   4.420 +lemma decseq_le: "decseq X \<Longrightarrow> X ----> L \<Longrightarrow> (L::real) \<le> X n"
   4.421 +  by (metis decseq_def LIMSEQ_le_const2)
   4.422  
   4.423  subsection {* Cauchy Sequences *}
   4.424  
   4.425  lemma metric_CauchyI:
   4.426    "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
   4.427 -by (simp add: Cauchy_def)
   4.428 +  by (simp add: Cauchy_def)
   4.429  
   4.430  lemma metric_CauchyD:
   4.431 -  "\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e"
   4.432 -by (simp add: Cauchy_def)
   4.433 +  "Cauchy X \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e"
   4.434 +  by (simp add: Cauchy_def)
   4.435  
   4.436  lemma Cauchy_iff:
   4.437    fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
   4.438    shows "Cauchy X \<longleftrightarrow> (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e)"
   4.439 -unfolding Cauchy_def dist_norm ..
   4.440 +  unfolding Cauchy_def dist_norm ..
   4.441  
   4.442  lemma Cauchy_iff2:
   4.443 -     "Cauchy X =
   4.444 -      (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m - X n\<bar> < inverse(real (Suc j))))"
   4.445 +  "Cauchy X = (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m - X n\<bar> < inverse(real (Suc j))))"
   4.446  apply (simp add: Cauchy_iff, auto)
   4.447  apply (drule reals_Archimedean, safe)
   4.448  apply (drule_tac x = n in spec, auto)
   4.449 @@ -934,24 +779,17 @@
   4.450  lemma isUb_UNIV_I: "(\<And>y. y \<in> S \<Longrightarrow> y \<le> u) \<Longrightarrow> isUb UNIV S u"
   4.451  by (simp add: isUbI setleI)
   4.452  
   4.453 -locale real_Cauchy =
   4.454 +lemma real_Cauchy_convergent:
   4.455    fixes X :: "nat \<Rightarrow> real"
   4.456    assumes X: "Cauchy X"
   4.457 -  fixes S :: "real set"
   4.458 -  defines S_def: "S \<equiv> {x::real. \<exists>N. \<forall>n\<ge>N. x < X n}"
   4.459 -
   4.460 -lemma real_CauchyI:
   4.461 -  assumes "Cauchy X"
   4.462 -  shows "real_Cauchy X"
   4.463 -  proof qed (fact assms)
   4.464 +  shows "convergent X"
   4.465 +proof -
   4.466 +  def S \<equiv> "{x::real. \<exists>N. \<forall>n\<ge>N. x < X n}"
   4.467 +  then have mem_S: "\<And>N x. \<forall>n\<ge>N. x < X n \<Longrightarrow> x \<in> S" by auto
   4.468  
   4.469 -lemma (in real_Cauchy) mem_S: "\<forall>n\<ge>N. x < X n \<Longrightarrow> x \<in> S"
   4.470 -by (unfold S_def, auto)
   4.471 -
   4.472 -lemma (in real_Cauchy) bound_isUb:
   4.473 -  assumes N: "\<forall>n\<ge>N. X n < x"
   4.474 -  shows "isUb UNIV S x"
   4.475 -proof (rule isUb_UNIV_I)
   4.476 +  { fix N x assume N: "\<forall>n\<ge>N. X n < x"
   4.477 +  have "isUb UNIV S x"
   4.478 +  proof (rule isUb_UNIV_I)
   4.479    fix y::real assume "y \<in> S"
   4.480    hence "\<exists>M. \<forall>n\<ge>M. y < X n"
   4.481      by (simp add: S_def)
   4.482 @@ -960,10 +798,11 @@
   4.483    also have "\<dots> < x" using N by simp
   4.484    finally show "y \<le> x"
   4.485      by (rule order_less_imp_le)
   4.486 -qed
   4.487 +  qed }
   4.488 +  note bound_isUb = this 
   4.489  
   4.490 -lemma (in real_Cauchy) isLub_ex: "\<exists>u. isLub UNIV S u"
   4.491 -proof (rule reals_complete)
   4.492 +  have "\<exists>u. isLub UNIV S u"
   4.493 +  proof (rule reals_complete)
   4.494    obtain N where "\<forall>m\<ge>N. \<forall>n\<ge>N. norm (X m - X n) < 1"
   4.495      using CauchyD [OF X zero_less_one] by auto
   4.496    hence N: "\<forall>n\<ge>N. norm (X n - X N) < 1" by simp
   4.497 @@ -980,12 +819,10 @@
   4.498      thus "isUb UNIV S (X N + 1)"
   4.499        by (rule bound_isUb)
   4.500    qed
   4.501 -qed
   4.502 -
   4.503 -lemma (in real_Cauchy) isLub_imp_LIMSEQ:
   4.504 -  assumes x: "isLub UNIV S x"
   4.505 -  shows "X ----> x"
   4.506 -proof (rule LIMSEQ_I)
   4.507 +  qed
   4.508 +  then obtain x where x: "isLub UNIV S x" ..
   4.509 +  have "X ----> x"
   4.510 +  proof (rule LIMSEQ_I)
   4.511    fix r::real assume "0 < r"
   4.512    hence r: "0 < r/2" by simp
   4.513    obtain N where "\<forall>n\<ge>N. \<forall>m\<ge>N. norm (X n - X m) < r/2"
   4.514 @@ -1009,26 +846,12 @@
   4.515      thus "norm (X n - x) < r" using 1 2
   4.516        by (simp add: abs_diff_less_iff)
   4.517    qed
   4.518 +  qed
   4.519 +  then show ?thesis unfolding convergent_def by auto
   4.520  qed
   4.521  
   4.522 -lemma (in real_Cauchy) LIMSEQ_ex: "\<exists>x. X ----> x"
   4.523 -proof -
   4.524 -  obtain x where "isLub UNIV S x"
   4.525 -    using isLub_ex by fast
   4.526 -  hence "X ----> x"
   4.527 -    by (rule isLub_imp_LIMSEQ)
   4.528 -  thus ?thesis ..
   4.529 -qed
   4.530 -
   4.531 -lemma real_Cauchy_convergent:
   4.532 -  fixes X :: "nat \<Rightarrow> real"
   4.533 -  shows "Cauchy X \<Longrightarrow> convergent X"
   4.534 -unfolding convergent_def
   4.535 -by (rule real_Cauchy.LIMSEQ_ex)
   4.536 - (rule real_CauchyI)
   4.537 -
   4.538  instance real :: banach
   4.539 -by intro_classes (rule real_Cauchy_convergent)
   4.540 +  by intro_classes (rule real_Cauchy_convergent)
   4.541  
   4.542  
   4.543  subsection {* Power Sequences *}
   4.544 @@ -1053,53 +876,12 @@
   4.545    "[| 0 \<le> (x::real); x \<le> 1 |] ==> convergent (%n. x ^ n)"
   4.546  by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow)
   4.547  
   4.548 -lemma LIMSEQ_inverse_realpow_zero_lemma:
   4.549 -  fixes x :: real
   4.550 -  assumes x: "0 \<le> x"
   4.551 -  shows "real n * x + 1 \<le> (x + 1) ^ n"
   4.552 -apply (induct n)
   4.553 -apply simp
   4.554 -apply simp
   4.555 -apply (rule order_trans)
   4.556 -prefer 2
   4.557 -apply (erule mult_left_mono)
   4.558 -apply (rule add_increasing [OF x], simp)
   4.559 -apply (simp add: real_of_nat_Suc)
   4.560 -apply (simp add: ring_distribs)
   4.561 -apply (simp add: mult_nonneg_nonneg x)
   4.562 -done
   4.563 -
   4.564 -lemma LIMSEQ_inverse_realpow_zero:
   4.565 -  "1 < (x::real) \<Longrightarrow> (\<lambda>n. inverse (x ^ n)) ----> 0"
   4.566 -proof (rule LIMSEQ_inverse_zero [rule_format])
   4.567 -  fix y :: real
   4.568 -  assume x: "1 < x"
   4.569 -  hence "0 < x - 1" by simp
   4.570 -  hence "\<forall>y. \<exists>N::nat. y < real N * (x - 1)"
   4.571 -    by (rule reals_Archimedean3)
   4.572 -  hence "\<exists>N::nat. y < real N * (x - 1)" ..
   4.573 -  then obtain N::nat where "y < real N * (x - 1)" ..
   4.574 -  also have "\<dots> \<le> real N * (x - 1) + 1" by simp
   4.575 -  also have "\<dots> \<le> (x - 1 + 1) ^ N"
   4.576 -    by (rule LIMSEQ_inverse_realpow_zero_lemma, cut_tac x, simp)
   4.577 -  also have "\<dots> = x ^ N" by simp
   4.578 -  finally have "y < x ^ N" .
   4.579 -  hence "\<forall>n\<ge>N. y < x ^ n"
   4.580 -    apply clarify
   4.581 -    apply (erule order_less_le_trans)
   4.582 -    apply (erule power_increasing)
   4.583 -    apply (rule order_less_imp_le [OF x])
   4.584 -    done
   4.585 -  thus "\<exists>N. \<forall>n\<ge>N. y < x ^ n" ..
   4.586 -qed
   4.587 +lemma LIMSEQ_inverse_realpow_zero: "1 < (x::real) \<Longrightarrow> (\<lambda>n. inverse (x ^ n)) ----> 0"
   4.588 +  by (rule filterlim_compose[OF tendsto_inverse_0 filterlim_realpow_sequentially_gt1]) simp
   4.589  
   4.590  lemma LIMSEQ_realpow_zero:
   4.591    "\<lbrakk>0 \<le> (x::real); x < 1\<rbrakk> \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
   4.592 -proof (cases)
   4.593 -  assume "x = 0"
   4.594 -  hence "(\<lambda>n. x ^ Suc n) ----> 0" by (simp add: tendsto_const)
   4.595 -  thus ?thesis by (rule LIMSEQ_imp_Suc)
   4.596 -next
   4.597 +proof cases
   4.598    assume "0 \<le> x" and "x \<noteq> 0"
   4.599    hence x0: "0 < x" by simp
   4.600    assume x1: "x < 1"
   4.601 @@ -1108,7 +890,7 @@
   4.602    hence "(\<lambda>n. inverse (inverse x ^ n)) ----> 0"
   4.603      by (rule LIMSEQ_inverse_realpow_zero)
   4.604    thus ?thesis by (simp add: power_inverse)
   4.605 -qed
   4.606 +qed (rule LIMSEQ_imp_Suc, simp add: tendsto_const)
   4.607  
   4.608  lemma LIMSEQ_power_zero:
   4.609    fixes x :: "'a::{real_normed_algebra_1}"
   4.610 @@ -1118,22 +900,15 @@
   4.611  apply (simp add: power_abs norm_power_ineq)
   4.612  done
   4.613  
   4.614 -lemma LIMSEQ_divide_realpow_zero:
   4.615 -  "1 < (x::real) ==> (%n. a / (x ^ n)) ----> 0"
   4.616 -using tendsto_mult [OF tendsto_const [of a]
   4.617 -  LIMSEQ_realpow_zero [of "inverse x"]]
   4.618 -apply (auto simp add: divide_inverse power_inverse)
   4.619 -apply (simp add: inverse_eq_divide pos_divide_less_eq)
   4.620 -done
   4.621 +lemma LIMSEQ_divide_realpow_zero: "1 < x \<Longrightarrow> (\<lambda>n. a / (x ^ n) :: real) ----> 0"
   4.622 +  by (rule tendsto_divide_0 [OF tendsto_const filterlim_realpow_sequentially_gt1]) simp
   4.623  
   4.624  text{*Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}*}
   4.625  
   4.626 -lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < (1::real) ==> (%n. \<bar>c\<bar> ^ n) ----> 0"
   4.627 -by (rule LIMSEQ_realpow_zero [OF abs_ge_zero])
   4.628 +lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. \<bar>c\<bar> ^ n :: real) ----> 0"
   4.629 +  by (rule LIMSEQ_realpow_zero [OF abs_ge_zero])
   4.630  
   4.631 -lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < (1::real) ==> (%n. c ^ n) ----> 0"
   4.632 -apply (rule tendsto_rabs_zero_cancel)
   4.633 -apply (auto intro: LIMSEQ_rabs_realpow_zero simp add: power_abs)
   4.634 -done
   4.635 +lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. c ^ n :: real) ----> 0"
   4.636 +  by (rule LIMSEQ_power_zero) simp
   4.637  
   4.638  end
     5.1 --- a/src/HOL/Series.thy	Mon Dec 03 18:19:11 2012 +0100
     5.2 +++ b/src/HOL/Series.thy	Mon Dec 03 18:19:12 2012 +0100
     5.3 @@ -650,6 +650,7 @@
     5.4  lemma rabs_ratiotest_lemma: "[| c \<le> 0; abs x \<le> c * abs y |] ==> x = (0::real)"
     5.5  by (erule norm_ratiotest_lemma, simp)
     5.6  
     5.7 +(* TODO: MOVE *)
     5.8  lemma le_Suc_ex: "(k::nat) \<le> l ==> (\<exists>n. l = k + n)"
     5.9  apply (drule le_imp_less_or_eq)
    5.10  apply (auto dest: less_imp_Suc_add)