# HG changeset patch
# User hoelzl
# Date 1354555152 -3600
# Node ID 4b6dc5077e98868379aafcbc8db45567fe105f75
# Parent  d0b12171118efcbb48ecd7b6d4afc985e400699d
use filterlim in Lim and SEQ; tuned proofs

diff -r d0b12171118e -r 4b6dc5077e98 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Mon Dec 03 18:19:11 2012 +0100
+++ b/src/HOL/Deriv.thy	Mon Dec 03 18:19:12 2012 +0100
@@ -76,7 +76,7 @@
 lemma DERIV_mult_lemma:
   fixes a b c d :: "'a::real_field"
   shows "(a * b - c * d) / h = a * ((b - d) / h) + ((a - c) / h) * d"
-by (simp add: diff_minus add_divide_distrib [symmetric] ring_distribs)
+  by (simp add: field_simps diff_divide_distrib)
 
 lemma DERIV_mult':
   assumes f: "DERIV f x :> D"
@@ -97,15 +97,12 @@
 qed
 
 lemma DERIV_mult:
-     "[| DERIV f x :> Da; DERIV g x :> Db |]
-      ==> DERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))"
-by (drule (1) DERIV_mult', simp only: mult_commute add_commute)
+    "DERIV f x :> Da \<Longrightarrow> DERIV g x :> Db \<Longrightarrow> DERIV (\<lambda>x. f x * g x) x :> Da * g x + Db * f x"
+  by (drule (1) DERIV_mult', simp only: mult_commute add_commute)
 
 lemma DERIV_unique:
-      "[| DERIV f x :> D; DERIV f x :> E |] ==> D = E"
-apply (simp add: deriv_def)
-apply (blast intro: LIM_unique)
-done
+    "DERIV f x :> D \<Longrightarrow> DERIV f x :> E \<Longrightarrow> D = E"
+  unfolding deriv_def by (rule LIM_unique) 
 
 text{*Differentiation of finite sum*}
 
diff -r d0b12171118e -r 4b6dc5077e98 src/HOL/Lim.thy
--- a/src/HOL/Lim.thy	Mon Dec 03 18:19:11 2012 +0100
+++ b/src/HOL/Lim.thy	Mon Dec 03 18:19:12 2012 +0100
@@ -323,36 +323,6 @@
   isCont_diff isCont_mult isCont_inverse isCont_divide isCont_scaleR
   isCont_of_real isCont_power isCont_sgn isCont_setsum
 
-lemma LIM_less_bound: fixes f :: "real \<Rightarrow> real" assumes "b < x"
-  and all_le: "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and isCont: "isCont f x"
-  shows "0 \<le> f x"
-proof (rule ccontr)
-  assume "\<not> 0 \<le> f x" hence "f x < 0" by auto
-  hence "0 < - f x / 2" by auto
-  from isCont[unfolded isCont_def, THEN LIM_D, OF this]
-  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
-
-  let ?x = "x - min (s / 2) ((x - b) / 2)"
-  have "?x < x" and "\<bar> ?x - x \<bar> < s"
-    using `b < x` and `0 < s` by auto
-  have "b < ?x"
-  proof (cases "s < x - b")
-    case True thus ?thesis using `0 < s` by auto
-  next
-    case False hence "s / 2 \<ge> (x - b) / 2" by auto
-    hence "?x = (x + b) / 2" by (simp add: field_simps min_max.inf_absorb2)
-    thus ?thesis using `b < x` by auto
-  qed
-  hence "0 \<le> f ?x" using all_le `?x < x` by auto
-  moreover have "\<bar>f ?x - f x\<bar> < - f x / 2"
-    using s_D[OF _ `\<bar> ?x - x \<bar> < s`] `?x < x` by auto
-  hence "f ?x - f x < - f x / 2" by auto
-  hence "f ?x < f x / 2" by auto
-  hence "f ?x < 0" using `f x < 0` by auto
-  thus False using `0 \<le> f ?x` by auto
-qed
-
-
 subsection {* Uniform Continuity *}
 
 lemma isUCont_isCont: "isUCont f ==> isCont f x"
@@ -442,4 +412,15 @@
    (X -- a --> (L::'b::topological_space))"
   using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..
 
+lemma LIM_less_bound: 
+  fixes f :: "real \<Rightarrow> real"
+  assumes ev: "b < x" "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and "isCont f x"
+  shows "0 \<le> f x"
+proof (rule tendsto_le_const)
+  show "(f ---> f x) (at_left x)"
+    using `isCont f x` by (simp add: filterlim_at_split isCont_def)
+  show "eventually (\<lambda>x. 0 \<le> f x) (at_left x)"
+    using ev by (auto simp: eventually_within_less dist_real_def intro!: exI[of _ "x - b"])
+qed simp
+
 end
diff -r d0b12171118e -r 4b6dc5077e98 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Mon Dec 03 18:19:11 2012 +0100
+++ b/src/HOL/Limits.thy	Mon Dec 03 18:19:12 2012 +0100
@@ -463,6 +463,22 @@
 lemma at_neq_bot [simp]: "at (a::'a::perfect_space) \<noteq> bot"
   by (simp add: at_eq_bot_iff not_open_singleton)
 
+lemma trivial_limit_at_left_real [simp]: (* maybe generalize type *)
+  "\<not> trivial_limit (at_left (x::real))"
+  unfolding trivial_limit_def eventually_within_le
+  apply clarsimp
+  apply (rule_tac x="x - d/2" in bexI)
+  apply (auto simp: dist_real_def)
+  done
+
+lemma trivial_limit_at_right_real [simp]: (* maybe generalize type *)
+  "\<not> trivial_limit (at_right (x::real))"
+  unfolding trivial_limit_def eventually_within_le
+  apply clarsimp
+  apply (rule_tac x="x + d/2" in bexI)
+  apply (auto simp: dist_real_def)
+  done
+
 lemma eventually_at_infinity:
   "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. b \<le> norm x \<longrightarrow> P x)"
 unfolding at_infinity_def
@@ -713,6 +729,9 @@
   "filterlim f F F1 \<Longrightarrow> filterlim f F F2 \<Longrightarrow> filterlim f F (sup F1 F2)"
   unfolding filterlim_def filtermap_sup by auto
 
+lemma filterlim_Suc: "filterlim Suc sequentially sequentially"
+  by (simp add: filterlim_iff eventually_sequentially) (metis le_Suc_eq)
+
 abbreviation (in topological_space)
   tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "--->" 55) where
   "(f ---> l) F \<equiv> filterlim f (nhds l) F"
@@ -1027,6 +1046,30 @@
     by (simp add: tendsto_const)
 qed
 
+lemma tendsto_le_const:
+  fixes f :: "_ \<Rightarrow> real" 
+  assumes F: "\<not> trivial_limit F"
+  assumes x: "(f ---> x) F" and a: "eventually (\<lambda>x. a \<le> f x) F"
+  shows "a \<le> x"
+proof (rule ccontr)
+  assume "\<not> a \<le> x"
+  with x have "eventually (\<lambda>x. f x < a) F"
+    by (auto simp add: tendsto_def elim!: allE[of _ "{..< a}"])
+  with a have "eventually (\<lambda>x. False) F"
+    by eventually_elim auto
+  with F show False
+    by (simp add: eventually_False)
+qed
+
+lemma tendsto_le:
+  fixes f g :: "_ \<Rightarrow> real" 
+  assumes F: "\<not> trivial_limit F"
+  assumes x: "(f ---> x) F" and y: "(g ---> y) F"
+  assumes ev: "eventually (\<lambda>x. g x \<le> f x) F"
+  shows "y \<le> x"
+  using tendsto_le_const[OF F tendsto_diff[OF x y], of 0] ev
+  by (simp add: sign_simps)
+
 subsubsection {* Inverse and division *}
 
 lemma (in bounded_bilinear) Zfun_prod_Bfun:
@@ -1382,6 +1425,44 @@
     by eventually_elim simp
 qed
 
+lemma tendsto_divide_0:
+  fixes f :: "_ \<Rightarrow> 'a\<Colon>{real_normed_div_algebra, division_ring_inverse_zero}"
+  assumes f: "(f ---> c) F"
+  assumes g: "LIM x F. g x :> at_infinity"
+  shows "((\<lambda>x. f x / g x) ---> 0) F"
+  using tendsto_mult[OF f filterlim_compose[OF tendsto_inverse_0 g]] by (simp add: divide_inverse)
+
+lemma linear_plus_1_le_power:
+  fixes x :: real
+  assumes x: "0 \<le> x"
+  shows "real n * x + 1 \<le> (x + 1) ^ n"
+proof (induct n)
+  case (Suc n)
+  have "real (Suc n) * x + 1 \<le> (x + 1) * (real n * x + 1)"
+    by (simp add: field_simps real_of_nat_Suc mult_nonneg_nonneg x)
+  also have "\<dots> \<le> (x + 1)^Suc n"
+    using Suc x by (simp add: mult_left_mono)
+  finally show ?case .
+qed simp
+
+lemma filterlim_realpow_sequentially_gt1:
+  fixes x :: "'a :: real_normed_div_algebra"
+  assumes x[arith]: "1 < norm x"
+  shows "LIM n sequentially. x ^ n :> at_infinity"
+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)
+  also have "\<dots> \<le> real N * (norm x - 1) + 1" by simp
+  also have "\<dots> \<le> (norm x - 1 + 1) ^ N" by (rule linear_plus_1_le_power) simp
+  also have "\<dots> = norm x ^ N" by simp
+  finally have "\<forall>n\<ge>N. y \<le> norm x ^ n"
+    by (metis order_less_le_trans power_increasing order_less_imp_le x)
+  then show "eventually (\<lambda>n. y \<le> norm (x ^ n)) sequentially"
+    unfolding eventually_sequentially
+    by (auto simp: norm_power)
+qed simp
+
 subsection {* Relate @{const at}, @{const at_left} and @{const at_right} *}
 
 text {*
diff -r d0b12171118e -r 4b6dc5077e98 src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Mon Dec 03 18:19:11 2012 +0100
+++ b/src/HOL/SEQ.thy	Mon Dec 03 18:19:12 2012 +0100
@@ -171,6 +171,9 @@
   thus ?case by arith
 qed
 
+lemma filterlim_subseq: "subseq f \<Longrightarrow> filterlim f sequentially sequentially"
+  unfolding filterlim_iff eventually_sequentially by (metis le_trans seq_suble)
+
 lemma subseq_o: "subseq r \<Longrightarrow> subseq s \<Longrightarrow> subseq (r \<circ> s)"
   unfolding subseq_def by simp
 
@@ -357,36 +360,23 @@
 
 lemma increasing_LIMSEQ:
   fixes f :: "nat \<Rightarrow> real"
-  assumes inc: "!!n. f n \<le> f (Suc n)"
-      and bdd: "!!n. f n \<le> l"
-      and en: "!!e. 0 < e \<Longrightarrow> \<exists>n. l \<le> f n + e"
+  assumes inc: "\<And>n. f n \<le> f (Suc n)"
+      and bdd: "\<And>n. f n \<le> l"
+      and en: "\<And>e. 0 < e \<Longrightarrow> \<exists>n. l \<le> f n + e"
   shows "f ----> l"
-proof (auto simp add: LIMSEQ_def)
-  fix e :: real
-  assume e: "0 < e"
-  then obtain N where "l \<le> f N + e/2"
-    by (metis half_gt_zero e en that)
-  hence N: "l < f N + e" using e
-    by simp
-  { fix k
-    have [simp]: "!!n. \<bar>f n - l\<bar> = l - f n"
-      by (simp add: bdd) 
-    have "\<bar>f (N+k) - l\<bar> < e"
-    proof (induct k)
-      case 0 show ?case using N
-        by simp   
-    next
-      case (Suc k) thus ?case using N inc [of "N+k"]
-        by simp
-    qed 
-  } note 1 = this
-  { fix n
-    have "N \<le> n \<Longrightarrow> \<bar>f n - l\<bar> < e" using 1 [of "n-N"]
-      by simp 
-  } note [intro] = this
-  show " \<exists>no. \<forall>n\<ge>no. dist (f n) l < e"
-    by (auto simp add: dist_real_def) 
-  qed
+  unfolding LIMSEQ_def
+proof safe
+  fix r :: real assume "0 < r"
+  with bdd en[of "r / 2"] obtain n where n: "dist (f n) l \<le> r / 2"
+    by (auto simp add: field_simps dist_real_def)
+  { fix N assume "n \<le> N"
+    then have "dist (f N) l \<le> dist (f n) l"
+      using incseq_SucI[of f] inc bdd by (auto dest!: incseqD simp: dist_real_def)
+    then have "dist (f N) l < r"
+      using `0 < r` n by simp }
+  with `0 < r` show "\<exists>no. \<forall>n\<ge>no. dist (f n) l < r"
+    by (auto simp add: LIMSEQ_def field_simps intro!: exI[of _ n])
+qed
 
 lemma Bseq_inverse_lemma:
   fixes x :: "'a::real_normed_div_algebra"
@@ -414,24 +404,16 @@
 
 lemma LIMSEQ_inverse_zero:
   "\<forall>r::real. \<exists>N. \<forall>n\<ge>N. r < X n \<Longrightarrow> (\<lambda>n. inverse (X n)) ----> 0"
-apply (rule LIMSEQ_I)
-apply (drule_tac x="inverse r" in spec, safe)
-apply (rule_tac x="N" in exI, safe)
-apply (drule_tac x="n" in spec, safe)
-apply (frule positive_imp_inverse_positive)
-apply (frule (1) less_imp_inverse_less)
-apply (subgoal_tac "0 < X n", simp)
-apply (erule (1) order_less_trans)
-done
+  apply (rule filterlim_compose[OF tendsto_inverse_0])
+  apply (simp add: filterlim_at_infinity[OF order_refl] eventually_sequentially)
+  apply (metis abs_le_D1 linorder_le_cases linorder_not_le)
+  done
 
 text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*}
 
 lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0"
-apply (rule LIMSEQ_inverse_zero, safe)
-apply (cut_tac x = r in reals_Archimedean2)
-apply (safe, rule_tac x = n in exI)
-apply (auto simp add: real_of_nat_Suc)
-done
+  by (metis filterlim_compose tendsto_inverse_0 filterlim_mono order_refl filterlim_Suc
+            filterlim_compose[OF filterlim_real_sequentially] at_top_le_at_infinity)
 
 text{*The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to
 infinity is now easily proved*}
@@ -442,41 +424,25 @@
 
 lemma LIMSEQ_inverse_real_of_nat_add_minus:
      "(%n. r + -inverse(real(Suc n))) ----> r"
-  using tendsto_add [OF tendsto_const
-    tendsto_minus [OF LIMSEQ_inverse_real_of_nat]] by auto
+  using tendsto_add [OF tendsto_const tendsto_minus [OF LIMSEQ_inverse_real_of_nat]]
+  by auto
 
 lemma LIMSEQ_inverse_real_of_nat_add_minus_mult:
      "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r"
-  using tendsto_mult [OF tendsto_const
-    LIMSEQ_inverse_real_of_nat_add_minus [of 1]]
+  using tendsto_mult [OF tendsto_const LIMSEQ_inverse_real_of_nat_add_minus [of 1]]
   by auto
 
 lemma LIMSEQ_le_const:
   "\<lbrakk>X ----> (x::real); \<exists>N. \<forall>n\<ge>N. a \<le> X n\<rbrakk> \<Longrightarrow> a \<le> x"
-apply (rule ccontr, simp only: linorder_not_le)
-apply (drule_tac r="a - x" in LIMSEQ_D, simp)
-apply clarsimp
-apply (drule_tac x="max N no" in spec, drule mp, rule le_maxI1)
-apply (drule_tac x="max N no" in spec, drule mp, rule le_maxI2)
-apply simp
-done
+  using tendsto_le_const[of sequentially X x a] by (simp add: eventually_sequentially)
+
+lemma LIMSEQ_le:
+  "\<lbrakk>X ----> x; Y ----> y; \<exists>N. \<forall>n\<ge>N. X n \<le> Y n\<rbrakk> \<Longrightarrow> x \<le> (y::real)"
+  using tendsto_le[of sequentially Y y X x] by (simp add: eventually_sequentially)
 
 lemma LIMSEQ_le_const2:
   "\<lbrakk>X ----> (x::real); \<exists>N. \<forall>n\<ge>N. X n \<le> a\<rbrakk> \<Longrightarrow> x \<le> a"
-apply (subgoal_tac "- a \<le> - x", simp)
-apply (rule LIMSEQ_le_const)
-apply (erule tendsto_minus)
-apply simp
-done
-
-lemma LIMSEQ_le:
-  "\<lbrakk>X ----> x; Y ----> y; \<exists>N. \<forall>n\<ge>N. X n \<le> Y n\<rbrakk> \<Longrightarrow> x \<le> (y::real)"
-apply (subgoal_tac "0 \<le> y - x", simp)
-apply (rule LIMSEQ_le_const)
-apply (erule (1) tendsto_diff)
-apply (simp add: le_diff_eq)
-done
-
+  by (rule LIMSEQ_le[of X x "\<lambda>n. a"]) (auto simp: tendsto_const)
 
 subsection {* Convergence *}
 
@@ -531,88 +497,17 @@
 apply (drule tendsto_minus, auto)
 done
 
-lemma lim_le:
-  fixes x :: real
-  assumes f: "convergent f" and fn_le: "!!n. f n \<le> x"
-  shows "lim f \<le> x"
-proof (rule classical)
-  assume "\<not> lim f \<le> x"
-  hence 0: "0 < lim f - x" by arith
-  have 1: "f----> lim f"
-    by (metis convergent_LIMSEQ_iff f) 
-  thus ?thesis
-    proof (simp add: LIMSEQ_iff)
-      assume "\<forall>r>0. \<exists>no. \<forall>n\<ge>no. \<bar>f n - lim f\<bar> < r"
-      hence "\<exists>no. \<forall>n\<ge>no. \<bar>f n - lim f\<bar> < lim f - x"
-        by (metis 0)
-      from this obtain no where "\<forall>n\<ge>no. \<bar>f n - lim f\<bar> < lim f - x"
-        by blast
-      thus "lim f \<le> x"
-        by (metis 1 LIMSEQ_le_const2 fn_le)
-    qed
-qed
+lemma lim_le: "convergent f \<Longrightarrow> (\<And>n. f n \<le> (x::real)) \<Longrightarrow> lim f \<le> x"
+  using LIMSEQ_le_const2[of f "lim f" x] by (simp add: convergent_LIMSEQ_iff)
 
 lemma monoseq_le:
-  fixes a :: "nat \<Rightarrow> real"
-  assumes "monoseq a" and "a ----> x"
-  shows "((\<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))"
-proof -
-  { fix x n fix a :: "nat \<Rightarrow> real"
-    assume "a ----> x" and "\<forall> m. \<forall> n \<ge> m. a m \<le> a n"
-    hence monotone: "\<And> m n. m \<le> n \<Longrightarrow> a m \<le> a n" by auto
-    have "a n \<le> x"
-    proof (rule ccontr)
-      assume "\<not> a n \<le> x" hence "x < a n" by auto
-      hence "0 < a n - x" by auto
-      from `a ----> x`[THEN LIMSEQ_D, OF this]
-      obtain no where "\<And>n'. no \<le> n' \<Longrightarrow> norm (a n' - x) < a n - x" by blast
-      hence "norm (a (max no n) - x) < a n - x" by auto
-      moreover
-      { fix n' have "n \<le> n' \<Longrightarrow> x < a n'" using monotone[where m=n and n=n'] and `x < a n` by auto }
-      hence "x < a (max no n)" by auto
-      ultimately
-      have "a (max no n) < a n" by auto
-      with monotone[where m=n and n="max no n"]
-      show False by (auto simp:max_def split:split_if_asm)
-    qed
-  } note top_down = this
-  { fix x n m fix a :: "nat \<Rightarrow> real"
-    assume "a ----> x" and "monoseq a" and "a m < x"
-    have "a n \<le> x \<and> (\<forall> m. \<forall> n \<ge> m. a m \<le> a n)"
-    proof (cases "\<forall> m. \<forall> n \<ge> m. a m \<le> a n")
-      case True with top_down and `a ----> x` show ?thesis by auto
-    next
-      case False with `monoseq a`[unfolded monoseq_def] have "\<forall> m. \<forall> n \<ge> m. - a m \<le> - a n" by auto
-      hence "- a m \<le> - x" using top_down[OF tendsto_minus[OF `a ----> x`]] by blast
-      hence False using `a m < x` by auto
-      thus ?thesis ..
-    qed
-  } note when_decided = this
-
-  show ?thesis
-  proof (cases "\<exists> m. a m \<noteq> x")
-    case True then obtain m where "a m \<noteq> x" by auto
-    show ?thesis
-    proof (cases "a m < x")
-      case True with when_decided[OF `a ----> x` `monoseq a`, where m2=m]
-      show ?thesis by blast
-    next
-      case False hence "- a m < - x" using `a m \<noteq> x` by auto
-      with when_decided[OF tendsto_minus[OF `a ----> x`] monoseq_minus[OF `monoseq a`], where m2=m]
-      show ?thesis by auto
-    qed
-  qed auto
-qed
+  "monoseq a \<Longrightarrow> a ----> (x::real) \<Longrightarrow>
+    ((\<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))"
+  by (metis LIMSEQ_le_const LIMSEQ_le_const2 decseq_def incseq_def monoseq_iff)
 
 lemma LIMSEQ_subseq_LIMSEQ:
   "\<lbrakk> X ----> L; subseq f \<rbrakk> \<Longrightarrow> (X o f) ----> L"
-apply (rule topological_tendstoI)
-apply (drule (2) topological_tendstoD)
-apply (simp only: eventually_sequentially)
-apply (clarify, rule_tac x=N in exI, clarsimp)
-apply (blast intro: seq_suble le_trans dest!: spec) 
-done
+  unfolding comp_def by (rule filterlim_compose[of X, OF _ filterlim_subseq])
 
 lemma convergent_subseq_convergent:
   "\<lbrakk>convergent X; subseq f\<rbrakk> \<Longrightarrow> convergent (X o f)"
@@ -630,27 +525,16 @@
 by (auto simp add: Bseq_def)
 
 lemma lemma_NBseq_def:
-     "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) =
-      (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
-proof auto
+  "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
+proof safe
   fix K :: real
   from reals_Archimedean2 obtain n :: nat where "K < real n" ..
   then have "K \<le> real (Suc n)" by auto
-  assume "\<forall>m. norm (X m) \<le> K"
-  have "\<forall>m. norm (X m) \<le> real (Suc n)"
-  proof
-    fix m :: 'a
-    from `\<forall>m. norm (X m) \<le> K` have "norm (X m) \<le> K" ..
-    with `K \<le> real (Suc n)` show "norm (X m) \<le> real (Suc n)" by auto
-  qed
+  moreover assume "\<forall>m. norm (X m) \<le> K"
+  ultimately have "\<forall>m. norm (X m) \<le> real (Suc n)"
+    by (blast intro: order_trans)
   then show "\<exists>N. \<forall>n. norm (X n) \<le> real (Suc N)" ..
-next
-  fix N :: nat
-  have "real (Suc N) > 0" by (simp add: real_of_nat_Suc)
-  moreover assume "\<forall>n. norm (X n) \<le> real (Suc N)"
-  ultimately show "\<exists>K>0. \<forall>n. norm (X n) \<le> K" by blast
-qed
-
+qed (force simp add: real_of_nat_Suc)
 
 text{* alternative definition for Bseq *}
 lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
@@ -672,6 +556,39 @@
 lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
 by (simp add: Bseq_def lemma_NBseq_def2)
 
+subsubsection{*A Few More Equivalence Theorems for Boundedness*}
+
+text{*alternative formulation for boundedness*}
+lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. norm (X(n) + -x) \<le> k)"
+apply (unfold Bseq_def, safe)
+apply (rule_tac [2] x = "k + norm x" in exI)
+apply (rule_tac x = K in exI, simp)
+apply (rule exI [where x = 0], auto)
+apply (erule order_less_le_trans, simp)
+apply (drule_tac x=n in spec, fold diff_minus)
+apply (drule order_trans [OF norm_triangle_ineq2])
+apply simp
+done
+
+text{*alternative formulation for boundedness*}
+lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. norm(X(n) + -X(N)) \<le> k)"
+apply safe
+apply (simp add: Bseq_def, safe)
+apply (rule_tac x = "K + norm (X N)" in exI)
+apply auto
+apply (erule order_less_le_trans, simp)
+apply (rule_tac x = N in exI, safe)
+apply (drule_tac x = n in spec)
+apply (rule order_trans [OF norm_triangle_ineq], simp)
+apply (auto simp add: Bseq_iff2)
+done
+
+lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> (K::real)) ==> Bseq f"
+apply (simp add: Bseq_def)
+apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI, auto)
+apply (drule_tac x = n in spec, arith)
+done
+
 subsubsection{*Upper Bounds and Lubs of Bounded Sequences*}
 
 lemma Bseq_isUb:
@@ -725,115 +642,43 @@
 text{*A standard proof of the theorem for monotone increasing sequence*}
 
 lemma Bseq_mono_convergent:
-     "[| Bseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> convergent (X::nat=>real)"
-proof -
-  assume "Bseq X"
-  then obtain u where u: "isLub UNIV {x. \<exists>n. X n = x} u"
-    using Bseq_isLub by fast
-  assume "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
-  with u have "X ----> u"
-    by (rule isLub_mono_imp_LIMSEQ)
-  thus "convergent X"
-    by (rule convergentI)
-qed
+   "Bseq X \<Longrightarrow> \<forall>m. \<forall>n \<ge> m. X m \<le> X n \<Longrightarrow> convergent (X::nat=>real)"
+  by (metis Bseq_isLub isLub_mono_imp_LIMSEQ convergentI)
 
 lemma Bseq_minus_iff: "Bseq (%n. -(X n)) = Bseq X"
-by (simp add: Bseq_def)
+  by (simp add: Bseq_def)
 
 text{*Main monotonicity theorem*}
-lemma Bseq_monoseq_convergent: "[| Bseq X; monoseq X |] ==> convergent (X::nat\<Rightarrow>real)"
-apply (simp add: monoseq_def, safe)
-apply (rule_tac [2] convergent_minus_iff [THEN ssubst])
-apply (drule_tac [2] Bseq_minus_iff [THEN ssubst])
-apply (auto intro!: Bseq_mono_convergent)
-done
+
+lemma Bseq_monoseq_convergent: "Bseq X \<Longrightarrow> monoseq X \<Longrightarrow> convergent (X::nat\<Rightarrow>real)"
+  by (metis monoseq_iff incseq_def decseq_eq_incseq convergent_minus_iff Bseq_minus_iff
+            Bseq_mono_convergent)
 
 subsubsection{*Increasing and Decreasing Series*}
 
-lemma incseq_le:
-  fixes X :: "nat \<Rightarrow> real"
-  assumes inc: "incseq X" and lim: "X ----> L" shows "X n \<le> L"
-  using monoseq_le [OF incseq_imp_monoseq [OF inc] lim]
-proof
-  assume "(\<forall>n. X n \<le> L) \<and> (\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n)"
-  thus ?thesis by simp
-next
-  assume "(\<forall>n. L \<le> X n) \<and> (\<forall>m n. m \<le> n \<longrightarrow> X n \<le> X m)"
-  hence const: "(!!m n. m \<le> n \<Longrightarrow> X n = X m)" using inc
-    by (auto simp add: incseq_def intro: order_antisym)
-  have X: "!!n. X n = X 0"
-    by (blast intro: const [of 0]) 
-  have "X = (\<lambda>n. X 0)"
-    by (blast intro: X)
-  hence "L = X 0" using tendsto_const [of "X 0" sequentially]
-    by (auto intro: LIMSEQ_unique lim)
-  thus ?thesis
-    by (blast intro: eq_refl X)
-qed
-
-lemma decseq_le:
-  fixes X :: "nat \<Rightarrow> real" assumes dec: "decseq X" and lim: "X ----> L" shows "L \<le> X n"
-proof -
-  have inc: "incseq (\<lambda>n. - X n)" using dec
-    by (simp add: decseq_eq_incseq)
-  have "- X n \<le> - L" 
-    by (blast intro: incseq_le [OF inc] tendsto_minus lim) 
-  thus ?thesis
-    by simp
-qed
+lemma incseq_le: "incseq X \<Longrightarrow> X ----> L \<Longrightarrow> X n \<le> (L::real)"
+  by (metis incseq_def LIMSEQ_le_const)
 
-subsubsection{*A Few More Equivalence Theorems for Boundedness*}
-
-text{*alternative formulation for boundedness*}
-lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. norm (X(n) + -x) \<le> k)"
-apply (unfold Bseq_def, safe)
-apply (rule_tac [2] x = "k + norm x" in exI)
-apply (rule_tac x = K in exI, simp)
-apply (rule exI [where x = 0], auto)
-apply (erule order_less_le_trans, simp)
-apply (drule_tac x=n in spec, fold diff_minus)
-apply (drule order_trans [OF norm_triangle_ineq2])
-apply simp
-done
-
-text{*alternative formulation for boundedness*}
-lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. norm(X(n) + -X(N)) \<le> k)"
-apply safe
-apply (simp add: Bseq_def, safe)
-apply (rule_tac x = "K + norm (X N)" in exI)
-apply auto
-apply (erule order_less_le_trans, simp)
-apply (rule_tac x = N in exI, safe)
-apply (drule_tac x = n in spec)
-apply (rule order_trans [OF norm_triangle_ineq], simp)
-apply (auto simp add: Bseq_iff2)
-done
-
-lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> (K::real)) ==> Bseq f"
-apply (simp add: Bseq_def)
-apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI, auto)
-apply (drule_tac x = n in spec, arith)
-done
-
+lemma decseq_le: "decseq X \<Longrightarrow> X ----> L \<Longrightarrow> (L::real) \<le> X n"
+  by (metis decseq_def LIMSEQ_le_const2)
 
 subsection {* Cauchy Sequences *}
 
 lemma metric_CauchyI:
   "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
-by (simp add: Cauchy_def)
+  by (simp add: Cauchy_def)
 
 lemma metric_CauchyD:
-  "\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e"
-by (simp add: Cauchy_def)
+  "Cauchy X \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e"
+  by (simp add: Cauchy_def)
 
 lemma Cauchy_iff:
   fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
   shows "Cauchy X \<longleftrightarrow> (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e)"
-unfolding Cauchy_def dist_norm ..
+  unfolding Cauchy_def dist_norm ..
 
 lemma Cauchy_iff2:
-     "Cauchy X =
-      (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m - X n\<bar> < inverse(real (Suc j))))"
+  "Cauchy X = (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m - X n\<bar> < inverse(real (Suc j))))"
 apply (simp add: Cauchy_iff, auto)
 apply (drule reals_Archimedean, safe)
 apply (drule_tac x = n in spec, auto)
@@ -934,24 +779,17 @@
 lemma isUb_UNIV_I: "(\<And>y. y \<in> S \<Longrightarrow> y \<le> u) \<Longrightarrow> isUb UNIV S u"
 by (simp add: isUbI setleI)
 
-locale real_Cauchy =
+lemma real_Cauchy_convergent:
   fixes X :: "nat \<Rightarrow> real"
   assumes X: "Cauchy X"
-  fixes S :: "real set"
-  defines S_def: "S \<equiv> {x::real. \<exists>N. \<forall>n\<ge>N. x < X n}"
-
-lemma real_CauchyI:
-  assumes "Cauchy X"
-  shows "real_Cauchy X"
-  proof qed (fact assms)
+  shows "convergent X"
+proof -
+  def S \<equiv> "{x::real. \<exists>N. \<forall>n\<ge>N. x < X n}"
+  then have mem_S: "\<And>N x. \<forall>n\<ge>N. x < X n \<Longrightarrow> x \<in> S" by auto
 
-lemma (in real_Cauchy) mem_S: "\<forall>n\<ge>N. x < X n \<Longrightarrow> x \<in> S"
-by (unfold S_def, auto)
-
-lemma (in real_Cauchy) bound_isUb:
-  assumes N: "\<forall>n\<ge>N. X n < x"
-  shows "isUb UNIV S x"
-proof (rule isUb_UNIV_I)
+  { fix N x assume N: "\<forall>n\<ge>N. X n < x"
+  have "isUb UNIV S x"
+  proof (rule isUb_UNIV_I)
   fix y::real assume "y \<in> S"
   hence "\<exists>M. \<forall>n\<ge>M. y < X n"
     by (simp add: S_def)
@@ -960,10 +798,11 @@
   also have "\<dots> < x" using N by simp
   finally show "y \<le> x"
     by (rule order_less_imp_le)
-qed
+  qed }
+  note bound_isUb = this 
 
-lemma (in real_Cauchy) isLub_ex: "\<exists>u. isLub UNIV S u"
-proof (rule reals_complete)
+  have "\<exists>u. isLub UNIV S u"
+  proof (rule reals_complete)
   obtain N where "\<forall>m\<ge>N. \<forall>n\<ge>N. norm (X m - X n) < 1"
     using CauchyD [OF X zero_less_one] by auto
   hence N: "\<forall>n\<ge>N. norm (X n - X N) < 1" by simp
@@ -980,12 +819,10 @@
     thus "isUb UNIV S (X N + 1)"
       by (rule bound_isUb)
   qed
-qed
-
-lemma (in real_Cauchy) isLub_imp_LIMSEQ:
-  assumes x: "isLub UNIV S x"
-  shows "X ----> x"
-proof (rule LIMSEQ_I)
+  qed
+  then obtain x where x: "isLub UNIV S x" ..
+  have "X ----> x"
+  proof (rule LIMSEQ_I)
   fix r::real assume "0 < r"
   hence r: "0 < r/2" by simp
   obtain N where "\<forall>n\<ge>N. \<forall>m\<ge>N. norm (X n - X m) < r/2"
@@ -1009,26 +846,12 @@
     thus "norm (X n - x) < r" using 1 2
       by (simp add: abs_diff_less_iff)
   qed
+  qed
+  then show ?thesis unfolding convergent_def by auto
 qed
 
-lemma (in real_Cauchy) LIMSEQ_ex: "\<exists>x. X ----> x"
-proof -
-  obtain x where "isLub UNIV S x"
-    using isLub_ex by fast
-  hence "X ----> x"
-    by (rule isLub_imp_LIMSEQ)
-  thus ?thesis ..
-qed
-
-lemma real_Cauchy_convergent:
-  fixes X :: "nat \<Rightarrow> real"
-  shows "Cauchy X \<Longrightarrow> convergent X"
-unfolding convergent_def
-by (rule real_Cauchy.LIMSEQ_ex)
- (rule real_CauchyI)
-
 instance real :: banach
-by intro_classes (rule real_Cauchy_convergent)
+  by intro_classes (rule real_Cauchy_convergent)
 
 
 subsection {* Power Sequences *}
@@ -1053,53 +876,12 @@
   "[| 0 \<le> (x::real); x \<le> 1 |] ==> convergent (%n. x ^ n)"
 by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow)
 
-lemma LIMSEQ_inverse_realpow_zero_lemma:
-  fixes x :: real
-  assumes x: "0 \<le> x"
-  shows "real n * x + 1 \<le> (x + 1) ^ n"
-apply (induct n)
-apply simp
-apply simp
-apply (rule order_trans)
-prefer 2
-apply (erule mult_left_mono)
-apply (rule add_increasing [OF x], simp)
-apply (simp add: real_of_nat_Suc)
-apply (simp add: ring_distribs)
-apply (simp add: mult_nonneg_nonneg x)
-done
-
-lemma LIMSEQ_inverse_realpow_zero:
-  "1 < (x::real) \<Longrightarrow> (\<lambda>n. inverse (x ^ n)) ----> 0"
-proof (rule LIMSEQ_inverse_zero [rule_format])
-  fix y :: real
-  assume x: "1 < x"
-  hence "0 < x - 1" by simp
-  hence "\<forall>y. \<exists>N::nat. y < real N * (x - 1)"
-    by (rule reals_Archimedean3)
-  hence "\<exists>N::nat. y < real N * (x - 1)" ..
-  then obtain N::nat where "y < real N * (x - 1)" ..
-  also have "\<dots> \<le> real N * (x - 1) + 1" by simp
-  also have "\<dots> \<le> (x - 1 + 1) ^ N"
-    by (rule LIMSEQ_inverse_realpow_zero_lemma, cut_tac x, simp)
-  also have "\<dots> = x ^ N" by simp
-  finally have "y < x ^ N" .
-  hence "\<forall>n\<ge>N. y < x ^ n"
-    apply clarify
-    apply (erule order_less_le_trans)
-    apply (erule power_increasing)
-    apply (rule order_less_imp_le [OF x])
-    done
-  thus "\<exists>N. \<forall>n\<ge>N. y < x ^ n" ..
-qed
+lemma LIMSEQ_inverse_realpow_zero: "1 < (x::real) \<Longrightarrow> (\<lambda>n. inverse (x ^ n)) ----> 0"
+  by (rule filterlim_compose[OF tendsto_inverse_0 filterlim_realpow_sequentially_gt1]) simp
 
 lemma LIMSEQ_realpow_zero:
   "\<lbrakk>0 \<le> (x::real); x < 1\<rbrakk> \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
-proof (cases)
-  assume "x = 0"
-  hence "(\<lambda>n. x ^ Suc n) ----> 0" by (simp add: tendsto_const)
-  thus ?thesis by (rule LIMSEQ_imp_Suc)
-next
+proof cases
   assume "0 \<le> x" and "x \<noteq> 0"
   hence x0: "0 < x" by simp
   assume x1: "x < 1"
@@ -1108,7 +890,7 @@
   hence "(\<lambda>n. inverse (inverse x ^ n)) ----> 0"
     by (rule LIMSEQ_inverse_realpow_zero)
   thus ?thesis by (simp add: power_inverse)
-qed
+qed (rule LIMSEQ_imp_Suc, simp add: tendsto_const)
 
 lemma LIMSEQ_power_zero:
   fixes x :: "'a::{real_normed_algebra_1}"
@@ -1118,22 +900,15 @@
 apply (simp add: power_abs norm_power_ineq)
 done
 
-lemma LIMSEQ_divide_realpow_zero:
-  "1 < (x::real) ==> (%n. a / (x ^ n)) ----> 0"
-using tendsto_mult [OF tendsto_const [of a]
-  LIMSEQ_realpow_zero [of "inverse x"]]
-apply (auto simp add: divide_inverse power_inverse)
-apply (simp add: inverse_eq_divide pos_divide_less_eq)
-done
+lemma LIMSEQ_divide_realpow_zero: "1 < x \<Longrightarrow> (\<lambda>n. a / (x ^ n) :: real) ----> 0"
+  by (rule tendsto_divide_0 [OF tendsto_const filterlim_realpow_sequentially_gt1]) simp
 
 text{*Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}*}
 
-lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < (1::real) ==> (%n. \<bar>c\<bar> ^ n) ----> 0"
-by (rule LIMSEQ_realpow_zero [OF abs_ge_zero])
+lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. \<bar>c\<bar> ^ n :: real) ----> 0"
+  by (rule LIMSEQ_realpow_zero [OF abs_ge_zero])
 
-lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < (1::real) ==> (%n. c ^ n) ----> 0"
-apply (rule tendsto_rabs_zero_cancel)
-apply (auto intro: LIMSEQ_rabs_realpow_zero simp add: power_abs)
-done
+lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. c ^ n :: real) ----> 0"
+  by (rule LIMSEQ_power_zero) simp
 
 end
diff -r d0b12171118e -r 4b6dc5077e98 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Mon Dec 03 18:19:11 2012 +0100
+++ b/src/HOL/Series.thy	Mon Dec 03 18:19:12 2012 +0100
@@ -650,6 +650,7 @@
 lemma rabs_ratiotest_lemma: "[| c \<le> 0; abs x \<le> c * abs y |] ==> x = (0::real)"
 by (erule norm_ratiotest_lemma, simp)
 
+(* TODO: MOVE *)
 lemma le_Suc_ex: "(k::nat) \<le> l ==> (\<exists>n. l = k + n)"
 apply (drule le_imp_less_or_eq)
 apply (auto dest: less_imp_Suc_add)