# HG changeset patch # User huffman # Date 1313347452 25200 # Node ID ea99698c207042e9f516e18042bed0d29bfd76d4 # Parent 5e4a1664106e118902f09abea078662b3169f41f locale-ize some definitions, so perfect_space and heine_borel can inherit from the proper superclasses diff -r 5e4a1664106e -r ea99698c2070 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sun Aug 14 10:47:47 2011 -0700 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sun Aug 14 11:44:12 2011 -0700 @@ -432,9 +432,8 @@ subsection{* Limit points *} -definition - islimpt:: "'a::topological_space \ 'a set \ bool" - (infixr "islimpt" 60) where +definition (in topological_space) + islimpt:: "'a \ 'a set \ bool" (infixr "islimpt" 60) where "x islimpt S \ (\T. x\T \ open T \ (\y\S. y\T \ y\x))" lemma islimptI: @@ -469,8 +468,8 @@ using approachable_lt_le[where f="\x'. dist x' x" and P="\x'. \ (x'\S \ x'\x)"] by metis -class perfect_space = - assumes islimpt_UNIV [simp, intro]: "(x::'a::topological_space) islimpt UNIV" +class perfect_space = topological_space + + assumes islimpt_UNIV [simp, intro]: "x islimpt UNIV" lemma perfect_choose_dist: fixes x :: "'a::{perfect_space, metric_space}" @@ -1881,8 +1880,8 @@ subsection{* Boundedness. *} (* FIXME: This has to be unified with BSEQ!! *) -definition - bounded :: "'a::metric_space set \ bool" where +definition (in metric_space) + bounded :: "'a set \ bool" where "bounded S \ (\x e. \y\S. dist x y \ e)" lemma bounded_any_center: "bounded S \ (\e. \y\S. dist a y \ e)" @@ -2110,7 +2109,7 @@ Heine-Borel property if every closed and bounded subset is compact. *} -class heine_borel = +class heine_borel = metric_space + assumes bounded_imp_convergent_subsequence: "bounded s \ \n. f n \ s \ \l r. subseq r \ ((f \ r) ---> l) sequentially"