--- 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) }
--- 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
--- 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:
--- 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"