src/HOL/SEQ.thy
changeset 44206 5e4a1664106e
parent 44205 18da2a87421c
child 44208 1d2bf1f240ac
     1.1 --- a/src/HOL/SEQ.thy	Sun Aug 14 10:25:43 2011 -0700
     1.2 +++ b/src/HOL/SEQ.thy	Sun Aug 14 10:47:47 2011 -0700
     1.3 @@ -183,8 +183,8 @@
     1.4  
     1.5  subsection {* Defintions of limits *}
     1.6  
     1.7 -abbreviation
     1.8 -  LIMSEQ :: "[nat \<Rightarrow> 'a::topological_space, 'a] \<Rightarrow> bool"
     1.9 +abbreviation (in topological_space)
    1.10 +  LIMSEQ :: "[nat \<Rightarrow> 'a, 'a] \<Rightarrow> bool"
    1.11      ("((_)/ ----> (_))" [60, 60] 60) where
    1.12    "X ----> L \<equiv> (X ---> L) sequentially"
    1.13  
    1.14 @@ -193,9 +193,7 @@
    1.15      --{*Standard definition of limit using choice operator*}
    1.16    "lim X = (THE L. X ----> L)"
    1.17  
    1.18 -definition
    1.19 -  convergent :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where
    1.20 -    --{*Standard definition of convergence*}
    1.21 +definition (in topological_space) convergent :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
    1.22    "convergent X = (\<exists>L. X ----> L)"
    1.23  
    1.24  definition
    1.25 @@ -203,9 +201,7 @@
    1.26      --{*Standard definition for bounded sequence*}
    1.27    "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
    1.28  
    1.29 -definition
    1.30 -  Cauchy :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where
    1.31 -    --{*Standard definition of the Cauchy condition*}
    1.32 +definition (in metric_space) Cauchy :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
    1.33    "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)"
    1.34  
    1.35  
    1.36 @@ -977,7 +973,7 @@
    1.37  
    1.38  subsubsection {* Cauchy Sequences are Convergent *}
    1.39  
    1.40 -class complete_space =
    1.41 +class complete_space = metric_space +
    1.42    assumes Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X"
    1.43  
    1.44  class banach = real_normed_vector + complete_space