locale-ize some constant definitions, so complete_space can inherit from metric_space

--- a/src/HOL/Limits.thy	Sun Aug 14 10:25:43 2011 -0700
+++ b/src/HOL/Limits.thy	Sun Aug 14 10:47:47 2011 -0700
@@ -283,10 +283,10 @@
 definition within :: "'a filter \<Rightarrow> 'a set \<Rightarrow> 'a filter" (infixr "within" 70)
   where "F within S = Abs_filter (\<lambda>P. eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) F)"
 
-definition nhds :: "'a::topological_space \<Rightarrow> 'a filter"
+definition (in topological_space) nhds :: "'a \<Rightarrow> 'a filter"
   where "nhds a = Abs_filter (\<lambda>P. \<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
 
-definition at :: "'a::topological_space \<Rightarrow> 'a filter"
+definition (in topological_space) at :: "'a \<Rightarrow> 'a filter"
   where "at a = nhds a within - {a}"
 
 lemma eventually_within:
@@ -517,8 +517,8 @@
 
 subsection {* Limits *}
 
-definition tendsto :: "('a \<Rightarrow> 'b::topological_space) \<Rightarrow> 'b \<Rightarrow> 'a filter \<Rightarrow> bool"
-    (infixr "--->" 55) where
+definition (in topological_space)
+  tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "--->" 55) where
   "(f ---> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)"
 
 ML {*

--- a/src/HOL/SEQ.thy	Sun Aug 14 10:25:43 2011 -0700
+++ b/src/HOL/SEQ.thy	Sun Aug 14 10:47:47 2011 -0700
@@ -183,8 +183,8 @@
 
 subsection {* Defintions of limits *}
 
-abbreviation
-  LIMSEQ :: "[nat \<Rightarrow> 'a::topological_space, 'a] \<Rightarrow> bool"
+abbreviation (in topological_space)
+  LIMSEQ :: "[nat \<Rightarrow> 'a, 'a] \<Rightarrow> bool"
     ("((_)/ ----> (_))" [60, 60] 60) where
   "X ----> L \<equiv> (X ---> L) sequentially"
 
@@ -193,9 +193,7 @@
     --{*Standard definition of limit using choice operator*}
   "lim X = (THE L. X ----> L)"
 
-definition
-  convergent :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where
-    --{*Standard definition of convergence*}
+definition (in topological_space) convergent :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
   "convergent X = (\<exists>L. X ----> L)"
 
 definition
@@ -203,9 +201,7 @@
     --{*Standard definition for bounded sequence*}
   "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
 
-definition
-  Cauchy :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where
-    --{*Standard definition of the Cauchy condition*}
+definition (in metric_space) Cauchy :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
   "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)"
 
 
@@ -977,7 +973,7 @@
 
 subsubsection {* Cauchy Sequences are Convergent *}
 
-class complete_space =
+class complete_space = metric_space +
   assumes Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X"
 
 class banach = real_normed_vector + complete_space