1.1 --- a/src/HOL/Limits.thy	Tue Nov 05 09:45:00 2013 +0100
     1.2 +++ b/src/HOL/Limits.thy	Tue Nov 05 09:45:02 2013 +0100
     1.3 @@ -138,6 +138,18 @@
     1.4  lemma BseqI: "[| 0 < K; \<forall>n. norm (X n) \<le> K |] ==> Bseq X"
     1.5  by (auto simp add: Bseq_def)
     1.6  
     1.7 +lemma Bseq_bdd_above: "Bseq (X::nat \<Rightarrow> real) \<Longrightarrow> bdd_above (range X)"
     1.8 +proof (elim BseqE, intro bdd_aboveI2)
     1.9 +  fix K n assume "0 < K" "\<forall>n. norm (X n) \<le> K" then show "X n \<le> K"
    1.10 +    by (auto elim!: allE[of _ n])
    1.11 +qed
    1.12 +
    1.13 +lemma Bseq_bdd_below: "Bseq (X::nat \<Rightarrow> real) \<Longrightarrow> bdd_below (range X)"
    1.14 +proof (elim BseqE, intro bdd_belowI2)
    1.15 +  fix K n assume "0 < K" "\<forall>n. norm (X n) \<le> K" then show "- K \<le> X n"
    1.16 +    by (auto elim!: allE[of _ n])
    1.17 +qed
    1.18 +
    1.19  lemma lemma_NBseq_def:
    1.20    "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
    1.21  proof safe
    1.22 @@ -210,18 +222,6 @@
    1.23  
    1.24  subsubsection{*Upper Bounds and Lubs of Bounded Sequences*}
    1.25  
    1.26 -lemma Bseq_isUb:
    1.27 -  "!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
    1.28 -by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff)
    1.29 -
    1.30 -text{* Use completeness of reals (supremum property)
    1.31 -   to show that any bounded sequence has a least upper bound*}
    1.32 -
    1.33 -lemma Bseq_isLub:
    1.34 -  "!!(X::nat=>real). Bseq X ==>
    1.35 -   \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U"
    1.36 -by (blast intro: reals_complete Bseq_isUb)
    1.37 -
    1.38  lemma Bseq_minus_iff: "Bseq (%n. -(X n) :: 'a :: real_normed_vector) = Bseq X"
    1.39    by (simp add: Bseq_def)
    1.40  
    1.41 @@ -1358,40 +1358,29 @@
    1.42  
    1.43  text {* A monotone sequence converges to its least upper bound. *}
    1.44  
    1.45 -lemma isLub_mono_imp_LIMSEQ:
    1.46 -  fixes X :: "nat \<Rightarrow> real"
    1.47 -  assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use 'range X' *)
    1.48 -  assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
    1.49 -  shows "X ----> u"
    1.50 -proof (rule LIMSEQ_I)
    1.51 -  have 1: "\<forall>n. X n \<le> u"
    1.52 -    using isLubD2 [OF u] by auto
    1.53 -  have "\<forall>y. (\<forall>n. X n \<le> y) \<longrightarrow> u \<le> y"
    1.54 -    using isLub_le_isUb [OF u] by (auto simp add: isUb_def setle_def)
    1.55 -  hence 2: "\<forall>y<u. \<exists>n. y < X n"
    1.56 -    by (metis not_le)
    1.57 -  fix r :: real assume "0 < r"
    1.58 -  hence "u - r < u" by simp
    1.59 -  hence "\<exists>m. u - r < X m" using 2 by simp
    1.60 -  then obtain m where "u - r < X m" ..
    1.61 -  with X have "\<forall>n\<ge>m. u - r < X n"
    1.62 -    by (fast intro: less_le_trans)
    1.63 -  hence "\<exists>m. \<forall>n\<ge>m. u - r < X n" ..
    1.64 -  thus "\<exists>m. \<forall>n\<ge>m. norm (X n - u) < r"
    1.65 -    using 1 by (simp add: diff_less_eq add_commute)
    1.66 -qed
    1.67 +lemma LIMSEQ_incseq_SUP:
    1.68 +  fixes X :: "nat \<Rightarrow> 'a::{conditionally_complete_linorder, linorder_topology}"
    1.69 +  assumes u: "bdd_above (range X)"
    1.70 +  assumes X: "incseq X"
    1.71 +  shows "X ----> (SUP i. X i)"
    1.72 +  by (rule order_tendstoI)
    1.73 +     (auto simp: eventually_sequentially u less_cSUP_iff intro: X[THEN incseqD] less_le_trans cSUP_lessD[OF u])
    1.74  
    1.75 -text{*A standard proof of the theorem for monotone increasing sequence*}
    1.76 -
    1.77 -lemma Bseq_mono_convergent:
    1.78 -   "Bseq X \<Longrightarrow> \<forall>m. \<forall>n \<ge> m. X m \<le> X n \<Longrightarrow> convergent (X::nat=>real)"
    1.79 -  by (metis Bseq_isLub isLub_mono_imp_LIMSEQ convergentI)
    1.80 +lemma LIMSEQ_decseq_INF:
    1.81 +  fixes X :: "nat \<Rightarrow> 'a::{conditionally_complete_linorder, linorder_topology}"
    1.82 +  assumes u: "bdd_below (range X)"
    1.83 +  assumes X: "decseq X"
    1.84 +  shows "X ----> (INF i. X i)"
    1.85 +  by (rule order_tendstoI)
    1.86 +     (auto simp: eventually_sequentially u cINF_less_iff intro: X[THEN decseqD] le_less_trans less_cINF_D[OF u])
    1.87  
    1.88  text{*Main monotonicity theorem*}
    1.89  
    1.90  lemma Bseq_monoseq_convergent: "Bseq X \<Longrightarrow> monoseq X \<Longrightarrow> convergent (X::nat\<Rightarrow>real)"
    1.91 -  by (metis monoseq_iff incseq_def decseq_eq_incseq convergent_minus_iff Bseq_minus_iff
    1.92 -            Bseq_mono_convergent)
    1.93 +  by (auto simp: monoseq_iff convergent_def intro: LIMSEQ_decseq_INF LIMSEQ_incseq_SUP dest: Bseq_bdd_above Bseq_bdd_below)
    1.94 +
    1.95 +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)"
    1.96 +  by (auto intro!: Bseq_monoseq_convergent incseq_imp_monoseq simp: incseq_def)
    1.97  
    1.98  lemma Cauchy_iff:
    1.99    fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"