# HG changeset patch # User huffman # Date 1176250746 -7200 # Node ID 73771f4548611f92902d6e1ed6c34797ba609676 # Parent 0e5ac9503d7e3313911466066494bb0ad0d8db26 new standard proof of convergent = Cauchy diff -r 0e5ac9503d7e -r 73771f454861 src/HOL/Hyperreal/SEQ.thy --- a/src/HOL/Hyperreal/SEQ.thy Tue Apr 10 22:02:43 2007 +0200 +++ b/src/HOL/Hyperreal/SEQ.thy Wed Apr 11 02:19:06 2007 +0200 @@ -1326,10 +1326,31 @@ apply (auto intro: approx_trans2) done +theorem LIMSEQ_imp_Cauchy: + assumes X: "X ----> a" shows "Cauchy X" +proof (rule CauchyI) + fix e::real assume "0 < e" + hence "0 < e/2" by simp + with X have "\N. \n\N. norm (X n - a) < e/2" by (rule LIMSEQ_D) + then obtain N where N: "\n\N. norm (X n - a) < e/2" .. + show "\N. \m\N. \n\N. norm (X m - X n) < e" + proof (intro exI allI impI) + fix m assume "N \ m" + hence m: "norm (X m - a) < e/2" using N by fast + fix n assume "N \ n" + hence n: "norm (X n - a) < e/2" using N by fast + have "norm (X m - X n) = norm ((X m - a) - (X n - a))" by simp + also have "\ \ norm (X m - a) + norm (X n - a)" + by (rule norm_triangle_ineq4) + also from m n have "\ < e/2 + e/2" by (rule add_strict_mono) + also have "e/2 + e/2 = e" by simp + finally show "norm (X m - X n) < e" . + qed +qed + lemma convergent_Cauchy: "convergent X \ Cauchy X" -apply (rule NSconvergent_NSCauchy [THEN NSCauchy_Cauchy]) -apply (simp add: convergent_NSconvergent_iff) -done +unfolding convergent_def +by (erule exE, erule LIMSEQ_imp_Cauchy) lemma real_NSCauchy_NSconvergent: fixes X :: "nat \ real" @@ -1343,13 +1364,113 @@ apply (blast intro: approx_trans3) done -text{*Standard proof for free*} +text {* +Proof that Cauchy sequences converge based on the one from +http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html +*} + +text {* + If sequence @{term "X"} is Cauchy, then its limit is the lub of + @{term "{r::real. \N. \n\N. r < X n}"} +*} + +lemma isUb_UNIV_I: "(\y. y \ S \ y \ u) \ isUb UNIV S u" +by (simp add: isUbI setleI) + +lemma real_abs_diff_less_iff: + "(\x - a\ < (r::real)) = (a - r < x \ x < a + r)" +by auto + +locale (open) real_Cauchy = + fixes X :: "nat \ real" + assumes X: "Cauchy X" + fixes S :: "real set" + defines S_def: "S \ {x::real. \N. \n\N. x < X n}" + +lemma (in real_Cauchy) mem_S: "\n\N. x < X n \ x \ S" +by (unfold S_def, auto) + +lemma (in real_Cauchy) bound_isUb: + assumes N: "\n\N. X n < x" + shows "isUb UNIV S x" +proof (rule isUb_UNIV_I) + fix y::real assume "y \ S" + hence "\M. \n\M. y < X n" + by (simp add: S_def) + then obtain M where "\n\M. y < X n" .. + hence "y < X (max M N)" by simp + also have "\ < x" using N by simp + finally show "y \ x" + by (rule order_less_imp_le) +qed + +lemma (in real_Cauchy) isLub_ex: "\u. isLub UNIV S u" +proof (rule reals_complete) + obtain N where "\m\N. \n\N. norm (X m - X n) < 1" + using CauchyD [OF X zero_less_one] by fast + hence N: "\n\N. norm (X n - X N) < 1" by simp + show "\x. x \ S" + proof + from N have "\n\N. X N - 1 < X n" + by (simp add: real_abs_diff_less_iff) + thus "X N - 1 \ S" by (rule mem_S) + qed + show "\u. isUb UNIV S u" + proof + from N have "\n\N. X n < X N + 1" + by (simp add: real_abs_diff_less_iff) + thus "isUb UNIV S (X N + 1)" + by (rule bound_isUb) + qed +qed + +lemma (in real_Cauchy) isLub_imp_LIMSEQ: + assumes x: "isLub UNIV S x" + shows "X ----> x" +proof (rule LIMSEQ_I) + fix r::real assume "0 < r" + hence r: "0 < r/2" by simp + obtain N where "\n\N. \m\N. norm (X n - X m) < r/2" + using CauchyD [OF X r] by fast + hence "\n\N. norm (X n - X N) < r/2" by simp + hence N: "\n\N. X N - r/2 < X n \ X n < X N + r/2" + by (simp only: real_norm_def real_abs_diff_less_iff) + + from N have "\n\N. X N - r/2 < X n" by fast + hence "X N - r/2 \ S" by (rule mem_S) + hence "X N - r/2 \ x" using x isLub_isUb isUbD by fast + hence 1: "X N + r/2 \ x + r" by simp + + from N have "\n\N. X n < X N + r/2" by fast + hence "isUb UNIV S (X N + r/2)" by (rule bound_isUb) + hence "x \ X N + r/2" using x isLub_le_isUb by fast + hence 2: "x - r \ X N - r/2" by simp + + show "\N. \n\N. norm (X n - x) < r" + proof (intro exI allI impI) + fix n assume n: "N \ n" + from N n have 3: "X n < X N + r/2" by simp + from N n have 4: "X N - r/2 < X n" by simp + show "norm (X n - x) < r" + using order_less_le_trans [OF 3 1] + order_le_less_trans [OF 2 4] + by (simp add: real_abs_diff_less_iff) + qed +qed + +lemma (in real_Cauchy) LIMSEQ_ex: "\x. X ----> x" +proof - + obtain x where "isLub UNIV S x" + using isLub_ex by fast + hence "X ----> x" + by (rule isLub_imp_LIMSEQ) + thus ?thesis .. +qed + lemma real_Cauchy_convergent: fixes X :: "nat \ real" shows "Cauchy X \ convergent X" -apply (drule Cauchy_NSCauchy [THEN real_NSCauchy_NSconvergent]) -apply (erule convergent_NSconvergent_iff [THEN iffD2]) -done +unfolding convergent_def by (rule real_Cauchy.LIMSEQ_ex) instance real :: banach by intro_classes (rule real_Cauchy_convergent)