1.1 --- a/src/HOL/SEQ.thy	Sun Sep 04 10:29:38 2011 -0700
     1.2 +++ b/src/HOL/SEQ.thy	Sun Sep 04 11:16:47 2011 -0700
     1.3 @@ -658,7 +658,6 @@
     1.4    "!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
     1.5  by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff)
     1.6  
     1.7 -
     1.8  text{* Use completeness of reals (supremum property)
     1.9     to show that any bounded sequence has a least upper bound*}
    1.10  
    1.11 @@ -669,15 +668,8 @@
    1.12  
    1.13  subsubsection{*A Bounded and Monotonic Sequence Converges*}
    1.14  
    1.15 -lemma lemma_converg1:
    1.16 -     "!!(X::nat=>real). [| \<forall>m. \<forall> n \<ge> m. X m \<le> X n;
    1.17 -                  isLub (UNIV::real set) {x. \<exists>n. X n = x} (X ma)
    1.18 -               |] ==> \<forall>n \<ge> ma. X n = X ma"
    1.19 -apply safe
    1.20 -apply (drule_tac y = "X n" in isLubD2)
    1.21 -apply (blast dest: order_antisym)+
    1.22 -done
    1.23 -
    1.24 +(* TODO: delete *)
    1.25 +(* FIXME: one use in NSA/HSEQ.thy *)
    1.26  lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----> L)"
    1.27  unfolding tendsto_def eventually_sequentially
    1.28  apply (rule_tac x = "X m" in exI, safe)
    1.29 @@ -685,50 +677,45 @@
    1.30  apply (drule spec, erule impE, auto)
    1.31  done
    1.32  
    1.33 -lemma lemma_converg2:
    1.34 -   "!!(X::nat=>real).
    1.35 -    [| \<forall>m. X m ~= U;  isLub UNIV {x. \<exists>n. X n = x} U |] ==> \<forall>m. X m < U"
    1.36 -apply safe
    1.37 -apply (drule_tac y = "X m" in isLubD2)
    1.38 -apply (auto dest!: order_le_imp_less_or_eq)
    1.39 -done
    1.40 +text {* A monotone sequence converges to its least upper bound. *}
    1.41  
    1.42 -lemma lemma_converg3: "!!(X ::nat=>real). \<forall>m. X m \<le> U ==> isUb UNIV {x. \<exists>n. X n = x} U"
    1.43 -by (rule setleI [THEN isUbI], auto)
    1.44 -
    1.45 -text{* FIXME: @{term "U - T < U"} is redundant *}
    1.46 -lemma lemma_converg4: "!!(X::nat=> real).
    1.47 -               [| \<forall>m. X m ~= U;
    1.48 -                  isLub UNIV {x. \<exists>n. X n = x} U;
    1.49 -                  0 < T;
    1.50 -                  U + - T < U
    1.51 -               |] ==> \<exists>m. U + -T < X m & X m < U"
    1.52 -apply (drule lemma_converg2, assumption)
    1.53 -apply (rule ccontr, simp)
    1.54 -apply (simp add: linorder_not_less)
    1.55 -apply (drule lemma_converg3)
    1.56 -apply (drule isLub_le_isUb, assumption)
    1.57 -apply (auto dest: order_less_le_trans)
    1.58 -done
    1.59 +lemma isLub_mono_imp_LIMSEQ:
    1.60 +  fixes X :: "nat \<Rightarrow> real"
    1.61 +  assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use 'range X' *)
    1.62 +  assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
    1.63 +  shows "X ----> u"
    1.64 +proof (rule LIMSEQ_I)
    1.65 +  have 1: "\<forall>n. X n \<le> u"
    1.66 +    using isLubD2 [OF u] by auto
    1.67 +  have "\<forall>y. (\<forall>n. X n \<le> y) \<longrightarrow> u \<le> y"
    1.68 +    using isLub_le_isUb [OF u] by (auto simp add: isUb_def setle_def)
    1.69 +  hence 2: "\<forall>y<u. \<exists>n. y < X n"
    1.70 +    by (metis not_le)
    1.71 +  fix r :: real assume "0 < r"
    1.72 +  hence "u - r < u" by simp
    1.73 +  hence "\<exists>m. u - r < X m" using 2 by simp
    1.74 +  then obtain m where "u - r < X m" ..
    1.75 +  with X have "\<forall>n\<ge>m. u - r < X n"
    1.76 +    by (fast intro: less_le_trans)
    1.77 +  hence "\<exists>m. \<forall>n\<ge>m. u - r < X n" ..
    1.78 +  thus "\<exists>m. \<forall>n\<ge>m. norm (X n - u) < r"
    1.79 +    using 1 by (simp add: diff_less_eq add_commute)
    1.80 +qed
    1.81  
    1.82  text{*A standard proof of the theorem for monotone increasing sequence*}
    1.83  
    1.84  lemma Bseq_mono_convergent:
    1.85       "[| Bseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> convergent (X::nat=>real)"
    1.86 -apply (simp add: convergent_def)
    1.87 -apply (frule Bseq_isLub, safe)
    1.88 -apply (case_tac "\<exists>m. X m = U", auto)
    1.89 -apply (blast dest: lemma_converg1 Bmonoseq_LIMSEQ)
    1.90 -(* second case *)
    1.91 -apply (rule_tac x = U in exI)
    1.92 -apply (subst LIMSEQ_iff, safe)
    1.93 -apply (frule lemma_converg2, assumption)
    1.94 -apply (drule lemma_converg4, auto)
    1.95 -apply (rule_tac x = m in exI, safe)
    1.96 -apply (subgoal_tac "X m \<le> X n")
    1.97 - prefer 2 apply blast
    1.98 -apply (drule_tac x=n and P="%m. X m < U" in spec, arith)
    1.99 -done
   1.100 +proof -
   1.101 +  assume "Bseq X"
   1.102 +  then obtain u where u: "isLub UNIV {x. \<exists>n. X n = x} u"
   1.103 +    using Bseq_isLub by fast
   1.104 +  assume "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
   1.105 +  with u have "X ----> u"
   1.106 +    by (rule isLub_mono_imp_LIMSEQ)
   1.107 +  thus "convergent X"
   1.108 +    by (rule convergentI)
   1.109 +qed
   1.110  
   1.111  lemma Bseq_minus_iff: "Bseq (%n. -(X n)) = Bseq X"
   1.112  by (simp add: Bseq_def)