# HG changeset patch
# User huffman
# Date 1315160207 25200
# Node ID a8990b5d736535a5ca9f19fe66a7699f3cb56f05
# Parent  1e490e891c88273d925c02917f4a45eba8a0276d
simplify proof of Bseq_mono_convergent

diff -r 1e490e891c88 -r a8990b5d7365 src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Sun Sep 04 10:29:38 2011 -0700
+++ b/src/HOL/SEQ.thy	Sun Sep 04 11:16:47 2011 -0700
@@ -658,7 +658,6 @@
   "!!(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*}
 
@@ -669,15 +668,8 @@
 
 subsubsection{*A Bounded and Monotonic Sequence Converges*}
 
-lemma lemma_converg1:
-     "!!(X::nat=>real). [| \<forall>m. \<forall> n \<ge> m. X m \<le> X n;
-                  isLub (UNIV::real set) {x. \<exists>n. X n = x} (X ma)
-               |] ==> \<forall>n \<ge> ma. X n = X ma"
-apply safe
-apply (drule_tac y = "X n" in isLubD2)
-apply (blast dest: order_antisym)+
-done
-
+(* TODO: delete *)
+(* FIXME: one use in NSA/HSEQ.thy *)
 lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----> L)"
 unfolding tendsto_def eventually_sequentially
 apply (rule_tac x = "X m" in exI, safe)
@@ -685,50 +677,45 @@
 apply (drule spec, erule impE, auto)
 done
 
-lemma lemma_converg2:
-   "!!(X::nat=>real).
-    [| \<forall>m. X m ~= U;  isLub UNIV {x. \<exists>n. X n = x} U |] ==> \<forall>m. X m < U"
-apply safe
-apply (drule_tac y = "X m" in isLubD2)
-apply (auto dest!: order_le_imp_less_or_eq)
-done
-
-lemma lemma_converg3: "!!(X ::nat=>real). \<forall>m. X m \<le> U ==> isUb UNIV {x. \<exists>n. X n = x} U"
-by (rule setleI [THEN isUbI], auto)
+text {* A monotone sequence converges to its least upper bound. *}
 
-text{* FIXME: @{term "U - T < U"} is redundant *}
-lemma lemma_converg4: "!!(X::nat=> real).
-               [| \<forall>m. X m ~= U;
-                  isLub UNIV {x. \<exists>n. X n = x} U;
-                  0 < T;
-                  U + - T < U
-               |] ==> \<exists>m. U + -T < X m & X m < U"
-apply (drule lemma_converg2, assumption)
-apply (rule ccontr, simp)
-apply (simp add: linorder_not_less)
-apply (drule lemma_converg3)
-apply (drule isLub_le_isUb, assumption)
-apply (auto dest: order_less_le_trans)
-done
+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
 
 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)"
-apply (simp add: convergent_def)
-apply (frule Bseq_isLub, safe)
-apply (case_tac "\<exists>m. X m = U", auto)
-apply (blast dest: lemma_converg1 Bmonoseq_LIMSEQ)
-(* second case *)
-apply (rule_tac x = U in exI)
-apply (subst LIMSEQ_iff, safe)
-apply (frule lemma_converg2, assumption)
-apply (drule lemma_converg4, auto)
-apply (rule_tac x = m in exI, safe)
-apply (subgoal_tac "X m \<le> X n")
- prefer 2 apply blast
-apply (drule_tac x=n and P="%m. X m < U" in spec, arith)
-done
+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
 
 lemma Bseq_minus_iff: "Bseq (%n. -(X n)) = Bseq X"
 by (simp add: Bseq_def)