1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 08 11:47:41 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 08 14:44:20 2011 -0700
     1.3 @@ -464,11 +464,10 @@
     1.4    by metis 
     1.5  
     1.6  class perfect_space =
     1.7 -  (* FIXME: perfect_space should inherit from topological_space *)
     1.8 -  assumes islimpt_UNIV [simp, intro]: "(x::'a::metric_space) islimpt UNIV"
     1.9 +  assumes islimpt_UNIV [simp, intro]: "(x::'a::topological_space) islimpt UNIV"
    1.10  
    1.11  lemma perfect_choose_dist:
    1.12 -  fixes x :: "'a::perfect_space"
    1.13 +  fixes x :: "'a::{perfect_space, metric_space}"
    1.14    shows "0 < r \<Longrightarrow> \<exists>a. a \<noteq> x \<and> dist a x < r"
    1.15  using islimpt_UNIV [of x]
    1.16  by (simp add: islimpt_approachable)
    1.17 @@ -599,22 +598,12 @@
    1.18  lemma interior_limit_point [intro]:
    1.19    fixes x :: "'a::perfect_space"
    1.20    assumes x: "x \<in> interior S" shows "x islimpt S"
    1.21 -proof-
    1.22 -  from x obtain e where e: "e>0" "\<forall>x'. dist x x' < e \<longrightarrow> x' \<in> S"
    1.23 -    unfolding mem_interior subset_eq Ball_def mem_ball by blast
    1.24 -  {
    1.25 -    fix d::real assume d: "d>0"
    1.26 -    let ?m = "min d e"
    1.27 -    have mde2: "0 < ?m" using e(1) d(1) by simp
    1.28 -    from perfect_choose_dist [OF mde2, of x]
    1.29 -    obtain y where "y \<noteq> x" and "dist y x < ?m" by blast
    1.30 -    then have "dist y x < e" "dist y x < d" by simp_all
    1.31 -    from `dist y x < e` e(2) have "y \<in> S" by (simp add: dist_commute)
    1.32 -    have "\<exists>x'\<in>S. x'\<noteq> x \<and> dist x' x < d"
    1.33 -      using `y \<in> S` `y \<noteq> x` `dist y x < d` by fast
    1.34 -  }
    1.35 -  then show ?thesis unfolding islimpt_approachable by blast
    1.36 -qed
    1.37 +  using x islimpt_UNIV [of x]
    1.38 +  unfolding interior_def islimpt_def
    1.39 +  apply (clarsimp, rename_tac T T')
    1.40 +  apply (drule_tac x="T \<inter> T'" in spec)
    1.41 +  apply (auto simp add: open_Int)
    1.42 +  done
    1.43  
    1.44  lemma interior_closed_Un_empty_interior:
    1.45    assumes cS: "closed S" and iT: "interior T = {}"
    1.46 @@ -954,12 +943,13 @@
    1.47    by (simp add: trivial_limit_at_iff)
    1.48  
    1.49  lemma trivial_limit_at_infinity:
    1.50 -  "\<not> trivial_limit (at_infinity :: ('a::{real_normed_vector,zero_neq_one}) net)"
    1.51 -  (* FIXME: find a more appropriate type class *)
    1.52 +  "\<not> trivial_limit (at_infinity :: ('a::{real_normed_vector,perfect_space}) net)"
    1.53    unfolding trivial_limit_def eventually_at_infinity
    1.54    apply clarsimp
    1.55 -  apply (rule_tac x="scaleR b (sgn 1)" in exI)
    1.56 -  apply (simp add: norm_sgn)
    1.57 +  apply (subgoal_tac "\<exists>x::'a. x \<noteq> 0", clarify)
    1.58 +   apply (rule_tac x="scaleR (b / norm x) x" in exI, simp)
    1.59 +  apply (cut_tac islimpt_UNIV [of "0::'a", unfolded islimpt_def])
    1.60 +  apply (drule_tac x=UNIV in spec, simp)
    1.61    done
    1.62  
    1.63  text {* Some property holds "sufficiently close" to the limit point. *}
    1.64 @@ -1513,7 +1503,7 @@
    1.65  done
    1.66  
    1.67  lemma netlimit_at:
    1.68 -  fixes a :: "'a::perfect_space"
    1.69 +  fixes a :: "'a::{perfect_space,t2_space}"
    1.70    shows "netlimit (at a) = a"
    1.71    apply (subst within_UNIV[symmetric])
    1.72    using netlimit_within[of a UNIV]
    1.73 @@ -1911,7 +1901,7 @@
    1.74  lemma cball_empty: "e < 0 ==> cball x e = {}" by (simp add: cball_eq_empty)
    1.75  
    1.76  lemma cball_eq_sing:
    1.77 -  fixes x :: "'a::perfect_space"
    1.78 +  fixes x :: "'a::{metric_space,perfect_space}"
    1.79    shows "(cball x e = {x}) \<longleftrightarrow> e = 0"
    1.80  proof (rule linorder_cases)
    1.81    assume e: "0 < e"
    1.82 @@ -1959,7 +1949,7 @@
    1.83    by (simp add: at_within_interior)
    1.84  
    1.85  lemma netlimit_within_interior:
    1.86 -  fixes x :: "'a::perfect_space"
    1.87 +  fixes x :: "'a::{t2_space,perfect_space}"
    1.88    assumes "x \<in> interior S"
    1.89    shows "netlimit (at x within S) = x"
    1.90  using assms by (simp add: at_within_interior netlimit_at)