--- a/src/HOL/SEQ.thy Tue Jun 02 22:35:56 2009 -0700
+++ b/src/HOL/SEQ.thy Tue Jun 02 23:06:05 2009 -0700
@@ -1034,9 +1034,11 @@
subsubsection {* Cauchy Sequences are Convergent *}
-axclass banach \<subseteq> real_normed_vector
+axclass complete_space \<subseteq> metric_space
Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X"
+axclass banach \<subseteq> real_normed_vector, complete_space
+
theorem LIMSEQ_imp_Cauchy:
assumes X: "X ----> a" shows "Cauchy X"
proof (rule metric_CauchyI)
@@ -1061,6 +1063,16 @@
unfolding convergent_def
by (erule exE, erule LIMSEQ_imp_Cauchy)
+lemma Cauchy_convergent_iff:
+ fixes X :: "nat \<Rightarrow> 'a::complete_space"
+ shows "Cauchy X = convergent X"
+by (fast intro: Cauchy_convergent convergent_Cauchy)
+
+lemma convergent_subseq_convergent:
+ fixes X :: "nat \<Rightarrow> 'a::complete_space"
+ shows "\<lbrakk> convergent X; subseq f \<rbrakk> \<Longrightarrow> convergent (X o f)"
+ by (simp add: Cauchy_subseq_Cauchy Cauchy_convergent_iff [symmetric])
+
text {*
Proof that Cauchy sequences converge based on the one from
http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html
@@ -1174,16 +1186,6 @@
instance real :: banach
by intro_classes (rule real_Cauchy_convergent)
-lemma Cauchy_convergent_iff:
- fixes X :: "nat \<Rightarrow> 'a::banach"
- shows "Cauchy X = convergent X"
-by (fast intro: Cauchy_convergent convergent_Cauchy)
-
-lemma convergent_subseq_convergent:
- fixes X :: "nat \<Rightarrow> 'a::banach"
- shows "\<lbrakk> convergent X; subseq f \<rbrakk> \<Longrightarrow> convergent (X o f)"
- by (simp add: Cauchy_subseq_Cauchy Cauchy_convergent_iff [symmetric])
-
subsection {* Power Sequences *}