# HG changeset patch
# User huffman
# Date 1159817405 -7200
# Node ID 65ba80cae6df8e1c7854f644643ef96a063b68a8
# Parent  863b187780bb2f9d922fbdd56d7a52861cbceb68
add axclass banach for complete normed vector spaces

diff -r 863b187780bb -r 65ba80cae6df src/HOL/Hyperreal/SEQ.thy
--- a/src/HOL/Hyperreal/SEQ.thy	Mon Oct 02 19:57:02 2006 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy	Mon Oct 02 21:30:05 2006 +0200
@@ -840,6 +840,9 @@
 
 subsubsection {* Cauchy Sequences are Convergent *}
 
+axclass banach \<subseteq> real_normed_vector
+  Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X"
+
 text{*Equivalence of Cauchy criterion and convergence:
   We will prove this using our NS formulation which provides a
   much easier proof than using the standard definition. We do not
@@ -860,10 +863,12 @@
 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)
+lemma real_NSCauchy_NSconvergent:
+  fixes X :: "nat \<Rightarrow> real"
+  shows "NSCauchy X \<Longrightarrow> NSconvergent X"
+apply (simp add: NSconvergent_def NSLIMSEQ_def)
 apply (frule NSCauchy_NSBseq)
-apply (auto intro: approx_trans2 simp add: NSBseq_def NSCauchy_def)
+apply (simp add: NSBseq_def NSCauchy_def)
 apply (drule HNatInfinite_whn [THEN [2] bspec])
 apply (drule HNatInfinite_whn [THEN [2] bspec])
 apply (auto dest!: st_part_Ex simp add: SReal_iff)
@@ -871,8 +876,32 @@
 done
 
 text{*Standard proof for free*}
-lemma Cauchy_convergent_iff: "Cauchy X = convergent (X::nat=>real)"
-by (simp add: NSCauchy_Cauchy_iff [symmetric] convergent_NSconvergent_iff NSCauchy_NSconvergent_iff)
+lemma real_Cauchy_convergent:
+  fixes X :: "nat \<Rightarrow> real"
+  shows "Cauchy X \<Longrightarrow> convergent X"
+apply (drule Cauchy_NSCauchy [THEN real_NSCauchy_NSconvergent])
+apply (erule convergent_NSconvergent_iff [THEN iffD2])
+done
+
+instance real :: banach
+by intro_classes (rule real_Cauchy_convergent)
+
+lemma NSCauchy_NSconvergent:
+  fixes X :: "nat \<Rightarrow> 'a::banach"
+  shows "NSCauchy X \<Longrightarrow> NSconvergent X"
+apply (drule NSCauchy_Cauchy [THEN Cauchy_convergent])
+apply (erule convergent_NSconvergent_iff [THEN iffD1])
+done
+
+lemma NSCauchy_NSconvergent_iff:
+  fixes X :: "nat \<Rightarrow> 'a::banach"
+  shows "NSCauchy X = NSconvergent X"
+by (fast intro: NSCauchy_NSconvergent NSconvergent_NSCauchy)
+
+lemma Cauchy_convergent_iff:
+  fixes X :: "nat \<Rightarrow> 'a::banach"
+  shows "Cauchy X = convergent X"
+by (fast intro: Cauchy_convergent convergent_Cauchy)
 
 
 subsection {* More Properties of Sequences *}