src/HOL/Limits.thy

--- a/src/HOL/Limits.thy	Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/Limits.thy	Tue Nov 05 09:45:02 2013 +0100
@@ -138,6 +138,18 @@
 lemma BseqI: "[| 0 < K; \<forall>n. norm (X n) \<le> K |] ==> Bseq X"
 by (auto simp add: Bseq_def)
 
+lemma Bseq_bdd_above: "Bseq (X::nat \<Rightarrow> real) \<Longrightarrow> bdd_above (range X)"
+proof (elim BseqE, intro bdd_aboveI2)
+  fix K n assume "0 < K" "\<forall>n. norm (X n) \<le> K" then show "X n \<le> K"
+    by (auto elim!: allE[of _ n])
+qed
+
+lemma Bseq_bdd_below: "Bseq (X::nat \<Rightarrow> real) \<Longrightarrow> bdd_below (range X)"
+proof (elim BseqE, intro bdd_belowI2)
+  fix K n assume "0 < K" "\<forall>n. norm (X n) \<le> K" then show "- K \<le> X n"
+    by (auto elim!: allE[of _ n])
+qed
+
 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 safe
@@ -210,18 +222,6 @@
 
 subsubsection{*Upper Bounds and Lubs of Bounded Sequences*}
 
-lemma Bseq_isUb:
-  "!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
-by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff)
-
-text{* Use completeness of reals (supremum property)
-   to show that any bounded sequence has a least upper bound*}
-
-lemma Bseq_isLub:
-  "!!(X::nat=>real). Bseq X ==>
-   \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U"
-by (blast intro: reals_complete Bseq_isUb)
-
 lemma Bseq_minus_iff: "Bseq (%n. -(X n) :: 'a :: real_normed_vector) = Bseq X"
   by (simp add: Bseq_def)
 
@@ -1358,40 +1358,29 @@
 
 text {* A monotone sequence converges to its least upper bound. *}
 
-lemma isLub_mono_imp_LIMSEQ:
-  fixes X :: "nat \<Rightarrow> real"
-  assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use 'range X' *)
-  assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
-  shows "X ----> u"
-proof (rule LIMSEQ_I)
-  have 1: "\<forall>n. X n \<le> u"
-    using isLubD2 [OF u] by auto
-  have "\<forall>y. (\<forall>n. X n \<le> y) \<longrightarrow> u \<le> y"
-    using isLub_le_isUb [OF u] by (auto simp add: isUb_def setle_def)
-  hence 2: "\<forall>y<u. \<exists>n. y < X n"
-    by (metis not_le)
-  fix r :: real assume "0 < r"
-  hence "u - r < u" by simp
-  hence "\<exists>m. u - r < X m" using 2 by simp
-  then obtain m where "u - r < X m" ..
-  with X have "\<forall>n\<ge>m. u - r < X n"
-    by (fast intro: less_le_trans)
-  hence "\<exists>m. \<forall>n\<ge>m. u - r < X n" ..
-  thus "\<exists>m. \<forall>n\<ge>m. norm (X n - u) < r"
-    using 1 by (simp add: diff_less_eq add_commute)
-qed
+lemma LIMSEQ_incseq_SUP:
+  fixes X :: "nat \<Rightarrow> 'a::{conditionally_complete_linorder, linorder_topology}"
+  assumes u: "bdd_above (range X)"
+  assumes X: "incseq X"
+  shows "X ----> (SUP i. X i)"
+  by (rule order_tendstoI)
+     (auto simp: eventually_sequentially u less_cSUP_iff intro: X[THEN incseqD] less_le_trans cSUP_lessD[OF u])
 
-text{*A standard proof of the theorem for monotone increasing sequence*}
-
-lemma Bseq_mono_convergent:
-   "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 LIMSEQ_decseq_INF:
+  fixes X :: "nat \<Rightarrow> 'a::{conditionally_complete_linorder, linorder_topology}"
+  assumes u: "bdd_below (range X)"
+  assumes X: "decseq X"
+  shows "X ----> (INF i. X i)"
+  by (rule order_tendstoI)
+     (auto simp: eventually_sequentially u cINF_less_iff intro: X[THEN decseqD] le_less_trans less_cINF_D[OF u])
 
 text{*Main monotonicity theorem*}
 
 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)
+  by (auto simp: monoseq_iff convergent_def intro: LIMSEQ_decseq_INF LIMSEQ_incseq_SUP dest: Bseq_bdd_above Bseq_bdd_below)
+
+lemma Bseq_mono_convergent: "Bseq X \<Longrightarrow> (\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n) \<Longrightarrow> convergent (X::nat\<Rightarrow>real)"
+  by (auto intro!: Bseq_monoseq_convergent incseq_imp_monoseq simp: incseq_def)
 
 lemma Cauchy_iff:
   fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"