# HG changeset patch
# User hoelzl
# Date 1363945303 -3600
# Node ID 2990382dc066359c85edd0976c6bba264f199ebf
# Parent  0c0efde246d1a32e0d0d3554cdb4980e29d95d9b
clean up lemma_nest_unique and renamed to nested_sequence_unique

diff -r 0c0efde246d1 -r 2990382dc066 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Deriv.thy	Fri Mar 22 10:41:43 2013 +0100
@@ -425,80 +425,27 @@
 
 subsection {* Nested Intervals and Bisection *}
 
-text{*Lemmas about nested intervals and proof by bisection (cf.Harrison).
-     All considerably tidied by lcp.*}
-
-lemma lemma_f_mono_add [rule_format (no_asm)]: "(\<forall>n. (f::nat=>real) n \<le> f (Suc n)) --> f m \<le> f(m + no)"
-apply (induct "no")
-apply (auto intro: order_trans)
-done
-
-lemma f_inc_g_dec_Beq_f: "[| \<forall>n. f(n) \<le> f(Suc n);
-         \<forall>n. g(Suc n) \<le> g(n);
-         \<forall>n. f(n) \<le> g(n) |]
-      ==> Bseq (f :: nat \<Rightarrow> real)"
-apply (rule_tac k = "f 0" and K = "g 0" in BseqI2, rule allI)
-apply (rule conjI)
-apply (induct_tac "n")
-apply (auto intro: order_trans)
-apply (rule_tac y = "g n" in order_trans)
-apply (induct_tac [2] "n")
-apply (auto intro: order_trans)
-done
-
-lemma f_inc_g_dec_Beq_g: "[| \<forall>n. f(n) \<le> f(Suc n);
-         \<forall>n. g(Suc n) \<le> g(n);
-         \<forall>n. f(n) \<le> g(n) |]
-      ==> Bseq (g :: nat \<Rightarrow> real)"
-apply (subst Bseq_minus_iff [symmetric])
-apply (rule_tac g = "%x. - (f x)" in f_inc_g_dec_Beq_f)
-apply auto
-done
-
-lemma f_inc_imp_le_lim:
-  fixes f :: "nat \<Rightarrow> real"
-  shows "\<lbrakk>\<forall>n. f n \<le> f (Suc n); convergent f\<rbrakk> \<Longrightarrow> f n \<le> lim f"
-  by (rule incseq_le, simp add: incseq_SucI, simp add: convergent_LIMSEQ_iff)
+lemma nested_sequence_unique:
+  assumes "\<forall>n. f n \<le> f (Suc n)" "\<forall>n. g (Suc n) \<le> g n" "\<forall>n. f n \<le> g n" "(\<lambda>n. f n - g n) ----> 0"
+  shows "\<exists>l::real. ((\<forall>n. f n \<le> l) \<and> f ----> l) \<and> ((\<forall>n. l \<le> g n) \<and> g ----> l)"
+proof -
+  have "incseq f" unfolding incseq_Suc_iff by fact
+  have "decseq g" unfolding decseq_Suc_iff by fact
 
-lemma lim_uminus:
-  fixes g :: "nat \<Rightarrow> 'a::real_normed_vector"
-  shows "convergent g ==> lim (%x. - g x) = - (lim g)"
-apply (rule tendsto_minus [THEN limI])
-apply (simp add: convergent_LIMSEQ_iff)
-done
-
-lemma g_dec_imp_lim_le:
-  fixes g :: "nat \<Rightarrow> real"
-  shows "\<lbrakk>\<forall>n. g (Suc n) \<le> g(n); convergent g\<rbrakk> \<Longrightarrow> lim g \<le> g n"
-  by (rule decseq_le, simp add: decseq_SucI, simp add: convergent_LIMSEQ_iff)
-
-lemma lemma_nest: "[| \<forall>n. f(n) \<le> f(Suc n);
-         \<forall>n. g(Suc n) \<le> g(n);
-         \<forall>n. f(n) \<le> g(n) |]
-      ==> \<exists>l m :: real. l \<le> m &  ((\<forall>n. f(n) \<le> l) & f ----> l) &
-                            ((\<forall>n. m \<le> g(n)) & g ----> m)"
-apply (subgoal_tac "monoseq f & monoseq g")
-prefer 2 apply (force simp add: LIMSEQ_iff monoseq_Suc)
-apply (subgoal_tac "Bseq f & Bseq g")
-prefer 2 apply (blast intro: f_inc_g_dec_Beq_f f_inc_g_dec_Beq_g)
-apply (auto dest!: Bseq_monoseq_convergent simp add: convergent_LIMSEQ_iff)
-apply (rule_tac x = "lim f" in exI)
-apply (rule_tac x = "lim g" in exI)
-apply (auto intro: LIMSEQ_le)
-apply (auto simp add: f_inc_imp_le_lim g_dec_imp_lim_le convergent_LIMSEQ_iff)
-done
-
-lemma lemma_nest_unique: "[| \<forall>n. f(n) \<le> f(Suc n);
-         \<forall>n. g(Suc n) \<le> g(n);
-         \<forall>n. f(n) \<le> g(n);
-         (%n. f(n) - g(n)) ----> 0 |]
-      ==> \<exists>l::real. ((\<forall>n. f(n) \<le> l) & f ----> l) &
-                ((\<forall>n. l \<le> g(n)) & g ----> l)"
-apply (drule lemma_nest, auto)
-apply (subgoal_tac "l = m")
-apply (drule_tac [2] f = f in tendsto_diff)
-apply (auto intro: LIMSEQ_unique)
-done
+  { fix n
+    from `decseq g` have "g n \<le> g 0" by (rule decseqD) simp
+    with `\<forall>n. f n \<le> g n`[THEN spec, of n] have "f n \<le> g 0" by auto }
+  then obtain u where "f ----> u" "\<forall>i. f i \<le> u"
+    using incseq_convergent[OF `incseq f`] by auto
+  moreover
+  { fix n
+    from `incseq f` have "f 0 \<le> f n" by (rule incseqD) simp
+    with `\<forall>n. f n \<le> g n`[THEN spec, of n] have "f 0 \<le> g n" by simp }
+  then obtain l where "g ----> l" "\<forall>i. l \<le> g i"
+    using decseq_convergent[OF `decseq g`] by auto
+  moreover note LIMSEQ_unique[OF assms(4) tendsto_diff[OF `f ----> u` `g ----> l`]]
+  ultimately show ?thesis by auto
+qed
 
 lemma Bolzano[consumes 1, case_names trans local]:
   fixes P :: "real \<Rightarrow> real \<Rightarrow> bool"
@@ -516,7 +463,7 @@
   { fix n have "l n \<le> u n" by (induct n) auto } note this[simp]
 
   have "\<exists>x. ((\<forall>n. l n \<le> x) \<and> l ----> x) \<and> ((\<forall>n. x \<le> u n) \<and> u ----> x)"
-  proof (safe intro!: lemma_nest_unique)
+  proof (safe intro!: nested_sequence_unique)
     fix n show "l n \<le> l (Suc n)" "u (Suc n) \<le> u n" by (induct n) auto
   next
     { fix n have "l n - u n = (a - b) / 2^n" by (induct n) (auto simp: field_simps) }
diff -r 0c0efde246d1 -r 2990382dc066 src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/SEQ.thy	Fri Mar 22 10:41:43 2013 +0100
@@ -301,6 +301,43 @@
   shows "\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e"
 by (simp add: Cauchy_iff)
 
+lemma Bseq_eq_bounded: "range f \<subseteq> {a .. b::real} \<Longrightarrow> Bseq f"
+  apply (simp add: subset_eq)
+  apply (rule BseqI'[where K="max (norm a) (norm b)"])
+  apply (erule_tac x=n in allE)
+  apply auto
+  done
+
+lemma incseq_bounded: "incseq X \<Longrightarrow> \<forall>i. X i \<le> (B::real) \<Longrightarrow> Bseq X"
+  by (intro Bseq_eq_bounded[of X "X 0" B]) (auto simp: incseq_def)
+
+lemma decseq_bounded: "decseq X \<Longrightarrow> \<forall>i. (B::real) \<le> X i \<Longrightarrow> Bseq X"
+  by (intro Bseq_eq_bounded[of X B "X 0"]) (auto simp: decseq_def)
+
+lemma incseq_convergent:
+  fixes X :: "nat \<Rightarrow> real"
+  assumes "incseq X" and "\<forall>i. X i \<le> B"
+  obtains L where "X ----> L" "\<forall>i. X i \<le> L"
+proof atomize_elim
+  from incseq_bounded[OF assms] `incseq X` Bseq_monoseq_convergent[of X]
+  obtain L where "X ----> L"
+    by (auto simp: convergent_def monoseq_def incseq_def)
+  with `incseq X` show "\<exists>L. X ----> L \<and> (\<forall>i. X i \<le> L)"
+    by (auto intro!: exI[of _ L] incseq_le)
+qed
+
+lemma decseq_convergent:
+  fixes X :: "nat \<Rightarrow> real"
+  assumes "decseq X" and "\<forall>i. B \<le> X i"
+  obtains L where "X ----> L" "\<forall>i. L \<le> X i"
+proof atomize_elim
+  from decseq_bounded[OF assms] `decseq X` Bseq_monoseq_convergent[of X]
+  obtain L where "X ----> L"
+    by (auto simp: convergent_def monoseq_def decseq_def)
+  with `decseq X` show "\<exists>L. X ----> L \<and> (\<forall>i. L \<le> X i)"
+    by (auto intro!: exI[of _ L] decseq_le)
+qed
+
 subsubsection {* Cauchy Sequences are Bounded *}
 
 text{*A Cauchy sequence is bounded -- this is the standard
diff -r 0c0efde246d1 -r 2990382dc066 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Series.thy	Fri Mar 22 10:41:43 2013 +0100
@@ -373,16 +373,13 @@
   have "convergent (\<lambda>n. setsum f {0..<n})"
     proof (rule Bseq_mono_convergent)
       show "Bseq (\<lambda>n. setsum f {0..<n})"
-        by (rule f_inc_g_dec_Beq_f [of "(\<lambda>n. setsum f {0..<n})" "\<lambda>n. x"])
-           (auto simp add: le pos)
+        by (intro BseqI'[of _ x]) (auto simp add: setsum_nonneg pos intro: le)
     next
       show "\<forall>m n. m \<le> n \<longrightarrow> setsum f {0..<m} \<le> setsum f {0..<n}"
         by (auto intro: setsum_mono2 pos)
     qed
-  then obtain L where "(%n. setsum f {0..<n}) ----> L"
-    by (blast dest: convergentD)
   thus ?thesis
-    by (force simp add: summable_def sums_def)
+    by (force simp add: summable_def sums_def convergent_def)
 qed
 
 lemma series_pos_le:
diff -r 0c0efde246d1 -r 2990382dc066 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Transcendental.thy	Fri Mar 22 10:41:43 2013 +0100
@@ -207,7 +207,7 @@
     thus "\<exists> N. \<forall> n \<ge> N. norm (- a (2 * n) - 0) < r" by auto
   qed
   ultimately
-  show ?thesis by (rule lemma_nest_unique)
+  show ?thesis by (rule nested_sequence_unique)
 qed
 
 lemma summable_Leibniz': fixes a :: "nat \<Rightarrow> real"