locale-ize some constant definitions, so complete_space can inherit from metric_space
authorhuffman
Sun Aug 14 10:47:47 2011 -0700 (2011-08-14)
changeset 442065e4a1664106e
parent 44205 18da2a87421c
child 44207 ea99698c2070
locale-ize some constant definitions, so complete_space can inherit from metric_space
src/HOL/Limits.thy
src/HOL/SEQ.thy
     1.1 --- a/src/HOL/Limits.thy	Sun Aug 14 10:25:43 2011 -0700
     1.2 +++ b/src/HOL/Limits.thy	Sun Aug 14 10:47:47 2011 -0700
     1.3 @@ -283,10 +283,10 @@
     1.4  definition within :: "'a filter \<Rightarrow> 'a set \<Rightarrow> 'a filter" (infixr "within" 70)
     1.5    where "F within S = Abs_filter (\<lambda>P. eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) F)"
     1.6  
     1.7 -definition nhds :: "'a::topological_space \<Rightarrow> 'a filter"
     1.8 +definition (in topological_space) nhds :: "'a \<Rightarrow> 'a filter"
     1.9    where "nhds a = Abs_filter (\<lambda>P. \<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
    1.10  
    1.11 -definition at :: "'a::topological_space \<Rightarrow> 'a filter"
    1.12 +definition (in topological_space) at :: "'a \<Rightarrow> 'a filter"
    1.13    where "at a = nhds a within - {a}"
    1.14  
    1.15  lemma eventually_within:
    1.16 @@ -517,8 +517,8 @@
    1.17  
    1.18  subsection {* Limits *}
    1.19  
    1.20 -definition tendsto :: "('a \<Rightarrow> 'b::topological_space) \<Rightarrow> 'b \<Rightarrow> 'a filter \<Rightarrow> bool"
    1.21 -    (infixr "--->" 55) where
    1.22 +definition (in topological_space)
    1.23 +  tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "--->" 55) where
    1.24    "(f ---> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)"
    1.25  
    1.26  ML {*
     2.1 --- a/src/HOL/SEQ.thy	Sun Aug 14 10:25:43 2011 -0700
     2.2 +++ b/src/HOL/SEQ.thy	Sun Aug 14 10:47:47 2011 -0700
     2.3 @@ -183,8 +183,8 @@
     2.4  
     2.5  subsection {* Defintions of limits *}
     2.6  
     2.7 -abbreviation
     2.8 -  LIMSEQ :: "[nat \<Rightarrow> 'a::topological_space, 'a] \<Rightarrow> bool"
     2.9 +abbreviation (in topological_space)
    2.10 +  LIMSEQ :: "[nat \<Rightarrow> 'a, 'a] \<Rightarrow> bool"
    2.11      ("((_)/ ----> (_))" [60, 60] 60) where
    2.12    "X ----> L \<equiv> (X ---> L) sequentially"
    2.13  
    2.14 @@ -193,9 +193,7 @@
    2.15      --{*Standard definition of limit using choice operator*}
    2.16    "lim X = (THE L. X ----> L)"
    2.17  
    2.18 -definition
    2.19 -  convergent :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where
    2.20 -    --{*Standard definition of convergence*}
    2.21 +definition (in topological_space) convergent :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
    2.22    "convergent X = (\<exists>L. X ----> L)"
    2.23  
    2.24  definition
    2.25 @@ -203,9 +201,7 @@
    2.26      --{*Standard definition for bounded sequence*}
    2.27    "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
    2.28  
    2.29 -definition
    2.30 -  Cauchy :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where
    2.31 -    --{*Standard definition of the Cauchy condition*}
    2.32 +definition (in metric_space) Cauchy :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
    2.33    "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)"
    2.34  
    2.35  
    2.36 @@ -977,7 +973,7 @@
    2.37  
    2.38  subsubsection {* Cauchy Sequences are Convergent *}
    2.39  
    2.40 -class complete_space =
    2.41 +class complete_space = metric_space +
    2.42    assumes Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X"
    2.43  
    2.44  class banach = real_normed_vector + complete_space