clean up lemma_nest_unique and renamed to nested_sequence_unique
authorhoelzl
Fri Mar 22 10:41:43 2013 +0100 (2013-03-22)
changeset 514772990382dc066
parent 51476 0c0efde246d1
child 51478 270b21f3ae0a
clean up lemma_nest_unique and renamed to nested_sequence_unique
src/HOL/Deriv.thy
src/HOL/SEQ.thy
src/HOL/Series.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Deriv.thy	Fri Mar 22 10:41:43 2013 +0100
     1.2 +++ b/src/HOL/Deriv.thy	Fri Mar 22 10:41:43 2013 +0100
     1.3 @@ -425,80 +425,27 @@
     1.4  
     1.5  subsection {* Nested Intervals and Bisection *}
     1.6  
     1.7 -text{*Lemmas about nested intervals and proof by bisection (cf.Harrison).
     1.8 -     All considerably tidied by lcp.*}
     1.9 -
    1.10 -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)"
    1.11 -apply (induct "no")
    1.12 -apply (auto intro: order_trans)
    1.13 -done
    1.14 -
    1.15 -lemma f_inc_g_dec_Beq_f: "[| \<forall>n. f(n) \<le> f(Suc n);
    1.16 -         \<forall>n. g(Suc n) \<le> g(n);
    1.17 -         \<forall>n. f(n) \<le> g(n) |]
    1.18 -      ==> Bseq (f :: nat \<Rightarrow> real)"
    1.19 -apply (rule_tac k = "f 0" and K = "g 0" in BseqI2, rule allI)
    1.20 -apply (rule conjI)
    1.21 -apply (induct_tac "n")
    1.22 -apply (auto intro: order_trans)
    1.23 -apply (rule_tac y = "g n" in order_trans)
    1.24 -apply (induct_tac [2] "n")
    1.25 -apply (auto intro: order_trans)
    1.26 -done
    1.27 -
    1.28 -lemma f_inc_g_dec_Beq_g: "[| \<forall>n. f(n) \<le> f(Suc n);
    1.29 -         \<forall>n. g(Suc n) \<le> g(n);
    1.30 -         \<forall>n. f(n) \<le> g(n) |]
    1.31 -      ==> Bseq (g :: nat \<Rightarrow> real)"
    1.32 -apply (subst Bseq_minus_iff [symmetric])
    1.33 -apply (rule_tac g = "%x. - (f x)" in f_inc_g_dec_Beq_f)
    1.34 -apply auto
    1.35 -done
    1.36 -
    1.37 -lemma f_inc_imp_le_lim:
    1.38 -  fixes f :: "nat \<Rightarrow> real"
    1.39 -  shows "\<lbrakk>\<forall>n. f n \<le> f (Suc n); convergent f\<rbrakk> \<Longrightarrow> f n \<le> lim f"
    1.40 -  by (rule incseq_le, simp add: incseq_SucI, simp add: convergent_LIMSEQ_iff)
    1.41 +lemma nested_sequence_unique:
    1.42 +  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"
    1.43 +  shows "\<exists>l::real. ((\<forall>n. f n \<le> l) \<and> f ----> l) \<and> ((\<forall>n. l \<le> g n) \<and> g ----> l)"
    1.44 +proof -
    1.45 +  have "incseq f" unfolding incseq_Suc_iff by fact
    1.46 +  have "decseq g" unfolding decseq_Suc_iff by fact
    1.47  
    1.48 -lemma lim_uminus:
    1.49 -  fixes g :: "nat \<Rightarrow> 'a::real_normed_vector"
    1.50 -  shows "convergent g ==> lim (%x. - g x) = - (lim g)"
    1.51 -apply (rule tendsto_minus [THEN limI])
    1.52 -apply (simp add: convergent_LIMSEQ_iff)
    1.53 -done
    1.54 -
    1.55 -lemma g_dec_imp_lim_le:
    1.56 -  fixes g :: "nat \<Rightarrow> real"
    1.57 -  shows "\<lbrakk>\<forall>n. g (Suc n) \<le> g(n); convergent g\<rbrakk> \<Longrightarrow> lim g \<le> g n"
    1.58 -  by (rule decseq_le, simp add: decseq_SucI, simp add: convergent_LIMSEQ_iff)
    1.59 -
    1.60 -lemma lemma_nest: "[| \<forall>n. f(n) \<le> f(Suc n);
    1.61 -         \<forall>n. g(Suc n) \<le> g(n);
    1.62 -         \<forall>n. f(n) \<le> g(n) |]
    1.63 -      ==> \<exists>l m :: real. l \<le> m &  ((\<forall>n. f(n) \<le> l) & f ----> l) &
    1.64 -                            ((\<forall>n. m \<le> g(n)) & g ----> m)"
    1.65 -apply (subgoal_tac "monoseq f & monoseq g")
    1.66 -prefer 2 apply (force simp add: LIMSEQ_iff monoseq_Suc)
    1.67 -apply (subgoal_tac "Bseq f & Bseq g")
    1.68 -prefer 2 apply (blast intro: f_inc_g_dec_Beq_f f_inc_g_dec_Beq_g)
    1.69 -apply (auto dest!: Bseq_monoseq_convergent simp add: convergent_LIMSEQ_iff)
    1.70 -apply (rule_tac x = "lim f" in exI)
    1.71 -apply (rule_tac x = "lim g" in exI)
    1.72 -apply (auto intro: LIMSEQ_le)
    1.73 -apply (auto simp add: f_inc_imp_le_lim g_dec_imp_lim_le convergent_LIMSEQ_iff)
    1.74 -done
    1.75 -
    1.76 -lemma lemma_nest_unique: "[| \<forall>n. f(n) \<le> f(Suc n);
    1.77 -         \<forall>n. g(Suc n) \<le> g(n);
    1.78 -         \<forall>n. f(n) \<le> g(n);
    1.79 -         (%n. f(n) - g(n)) ----> 0 |]
    1.80 -      ==> \<exists>l::real. ((\<forall>n. f(n) \<le> l) & f ----> l) &
    1.81 -                ((\<forall>n. l \<le> g(n)) & g ----> l)"
    1.82 -apply (drule lemma_nest, auto)
    1.83 -apply (subgoal_tac "l = m")
    1.84 -apply (drule_tac [2] f = f in tendsto_diff)
    1.85 -apply (auto intro: LIMSEQ_unique)
    1.86 -done
    1.87 +  { fix n
    1.88 +    from `decseq g` have "g n \<le> g 0" by (rule decseqD) simp
    1.89 +    with `\<forall>n. f n \<le> g n`[THEN spec, of n] have "f n \<le> g 0" by auto }
    1.90 +  then obtain u where "f ----> u" "\<forall>i. f i \<le> u"
    1.91 +    using incseq_convergent[OF `incseq f`] by auto
    1.92 +  moreover
    1.93 +  { fix n
    1.94 +    from `incseq f` have "f 0 \<le> f n" by (rule incseqD) simp
    1.95 +    with `\<forall>n. f n \<le> g n`[THEN spec, of n] have "f 0 \<le> g n" by simp }
    1.96 +  then obtain l where "g ----> l" "\<forall>i. l \<le> g i"
    1.97 +    using decseq_convergent[OF `decseq g`] by auto
    1.98 +  moreover note LIMSEQ_unique[OF assms(4) tendsto_diff[OF `f ----> u` `g ----> l`]]
    1.99 +  ultimately show ?thesis by auto
   1.100 +qed
   1.101  
   1.102  lemma Bolzano[consumes 1, case_names trans local]:
   1.103    fixes P :: "real \<Rightarrow> real \<Rightarrow> bool"
   1.104 @@ -516,7 +463,7 @@
   1.105    { fix n have "l n \<le> u n" by (induct n) auto } note this[simp]
   1.106  
   1.107    have "\<exists>x. ((\<forall>n. l n \<le> x) \<and> l ----> x) \<and> ((\<forall>n. x \<le> u n) \<and> u ----> x)"
   1.108 -  proof (safe intro!: lemma_nest_unique)
   1.109 +  proof (safe intro!: nested_sequence_unique)
   1.110      fix n show "l n \<le> l (Suc n)" "u (Suc n) \<le> u n" by (induct n) auto
   1.111    next
   1.112      { fix n have "l n - u n = (a - b) / 2^n" by (induct n) (auto simp: field_simps) }
     2.1 --- a/src/HOL/SEQ.thy	Fri Mar 22 10:41:43 2013 +0100
     2.2 +++ b/src/HOL/SEQ.thy	Fri Mar 22 10:41:43 2013 +0100
     2.3 @@ -301,6 +301,43 @@
     2.4    shows "\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e"
     2.5  by (simp add: Cauchy_iff)
     2.6  
     2.7 +lemma Bseq_eq_bounded: "range f \<subseteq> {a .. b::real} \<Longrightarrow> Bseq f"
     2.8 +  apply (simp add: subset_eq)
     2.9 +  apply (rule BseqI'[where K="max (norm a) (norm b)"])
    2.10 +  apply (erule_tac x=n in allE)
    2.11 +  apply auto
    2.12 +  done
    2.13 +
    2.14 +lemma incseq_bounded: "incseq X \<Longrightarrow> \<forall>i. X i \<le> (B::real) \<Longrightarrow> Bseq X"
    2.15 +  by (intro Bseq_eq_bounded[of X "X 0" B]) (auto simp: incseq_def)
    2.16 +
    2.17 +lemma decseq_bounded: "decseq X \<Longrightarrow> \<forall>i. (B::real) \<le> X i \<Longrightarrow> Bseq X"
    2.18 +  by (intro Bseq_eq_bounded[of X B "X 0"]) (auto simp: decseq_def)
    2.19 +
    2.20 +lemma incseq_convergent:
    2.21 +  fixes X :: "nat \<Rightarrow> real"
    2.22 +  assumes "incseq X" and "\<forall>i. X i \<le> B"
    2.23 +  obtains L where "X ----> L" "\<forall>i. X i \<le> L"
    2.24 +proof atomize_elim
    2.25 +  from incseq_bounded[OF assms] `incseq X` Bseq_monoseq_convergent[of X]
    2.26 +  obtain L where "X ----> L"
    2.27 +    by (auto simp: convergent_def monoseq_def incseq_def)
    2.28 +  with `incseq X` show "\<exists>L. X ----> L \<and> (\<forall>i. X i \<le> L)"
    2.29 +    by (auto intro!: exI[of _ L] incseq_le)
    2.30 +qed
    2.31 +
    2.32 +lemma decseq_convergent:
    2.33 +  fixes X :: "nat \<Rightarrow> real"
    2.34 +  assumes "decseq X" and "\<forall>i. B \<le> X i"
    2.35 +  obtains L where "X ----> L" "\<forall>i. L \<le> X i"
    2.36 +proof atomize_elim
    2.37 +  from decseq_bounded[OF assms] `decseq X` Bseq_monoseq_convergent[of X]
    2.38 +  obtain L where "X ----> L"
    2.39 +    by (auto simp: convergent_def monoseq_def decseq_def)
    2.40 +  with `decseq X` show "\<exists>L. X ----> L \<and> (\<forall>i. L \<le> X i)"
    2.41 +    by (auto intro!: exI[of _ L] decseq_le)
    2.42 +qed
    2.43 +
    2.44  subsubsection {* Cauchy Sequences are Bounded *}
    2.45  
    2.46  text{*A Cauchy sequence is bounded -- this is the standard
     3.1 --- a/src/HOL/Series.thy	Fri Mar 22 10:41:43 2013 +0100
     3.2 +++ b/src/HOL/Series.thy	Fri Mar 22 10:41:43 2013 +0100
     3.3 @@ -373,16 +373,13 @@
     3.4    have "convergent (\<lambda>n. setsum f {0..<n})"
     3.5      proof (rule Bseq_mono_convergent)
     3.6        show "Bseq (\<lambda>n. setsum f {0..<n})"
     3.7 -        by (rule f_inc_g_dec_Beq_f [of "(\<lambda>n. setsum f {0..<n})" "\<lambda>n. x"])
     3.8 -           (auto simp add: le pos)
     3.9 +        by (intro BseqI'[of _ x]) (auto simp add: setsum_nonneg pos intro: le)
    3.10      next
    3.11        show "\<forall>m n. m \<le> n \<longrightarrow> setsum f {0..<m} \<le> setsum f {0..<n}"
    3.12          by (auto intro: setsum_mono2 pos)
    3.13      qed
    3.14 -  then obtain L where "(%n. setsum f {0..<n}) ----> L"
    3.15 -    by (blast dest: convergentD)
    3.16    thus ?thesis
    3.17 -    by (force simp add: summable_def sums_def)
    3.18 +    by (force simp add: summable_def sums_def convergent_def)
    3.19  qed
    3.20  
    3.21  lemma series_pos_le:
     4.1 --- a/src/HOL/Transcendental.thy	Fri Mar 22 10:41:43 2013 +0100
     4.2 +++ b/src/HOL/Transcendental.thy	Fri Mar 22 10:41:43 2013 +0100
     4.3 @@ -207,7 +207,7 @@
     4.4      thus "\<exists> N. \<forall> n \<ge> N. norm (- a (2 * n) - 0) < r" by auto
     4.5    qed
     4.6    ultimately
     4.7 -  show ?thesis by (rule lemma_nest_unique)
     4.8 +  show ?thesis by (rule nested_sequence_unique)
     4.9  qed
    4.10  
    4.11  lemma summable_Leibniz': fixes a :: "nat \<Rightarrow> real"