# HG changeset patch
# User huffman
# Date 1159064188 -7200
# Node ID 53cbea20e4d91d56c92d6eb58b80e9354ff35203
# Parent  136b206327a4b3135a3779c015a72769dbb4aeb2
add lemma convergent_Cauchy

diff -r 136b206327a4 -r 53cbea20e4d9 src/HOL/Hyperreal/SEQ.thy
--- a/src/HOL/Hyperreal/SEQ.thy	Sun Sep 24 04:00:46 2006 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy	Sun Sep 24 04:16:28 2006 +0200
@@ -925,6 +925,16 @@
   instantiations for his 'espsilon-delta' proof(s) in this case
   since the NS formulations do not involve existential quantifiers.*}
 
+lemma NSconvergent_NSCauchy: "NSconvergent X \<Longrightarrow> NSCauchy X"
+apply (simp add: NSconvergent_def NSLIMSEQ_def NSCauchy_def, safe)
+apply (auto intro: approx_trans2)
+done
+
+lemma convergent_Cauchy: "convergent X \<Longrightarrow> Cauchy X"
+apply (rule NSconvergent_NSCauchy [THEN NSCauchy_Cauchy])
+apply (simp add: convergent_NSconvergent_iff)
+done
+
 lemma NSCauchy_NSconvergent_iff: "NSCauchy X = NSconvergent (X::nat=>real)"
 apply (simp add: NSconvergent_def NSLIMSEQ_def, safe)
 apply (frule NSCauchy_NSBseq)