# HG changeset patch
# User huffman
# Date 1244009165 25200
# Node ID 0baaad47cef21aca392d94e6e48269fff69aa2db
# Parent  e37967787a4feaf76c88b3c32a28aef4f808b282
class complete_space

diff -r e37967787a4f -r 0baaad47cef2 src/HOL/SEQ.thy
--- 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 *}