# HG changeset patch
# User huffman
# Date 1243982279 25200
# Node ID 97a2a3d4088ebab4ff4b566967d0def9a0b25c99
# Parent  1d0478b16613412c6a65a3bf8fc401c714ffc9dd
generalize type of 'at' to metric_space

diff -r 1d0478b16613 -r 97a2a3d4088e src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Tue Jun 02 15:13:22 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Tue Jun 02 15:37:59 2009 -0700
@@ -1011,7 +1011,7 @@
 subsection{* Common nets and The "within" modifier for nets. *}
 
 definition
-  at :: "'a::perfect_space \<Rightarrow> 'a net" where
+  at :: "'a::metric_space \<Rightarrow> 'a net" where
   "at a = Abs_net ((\<lambda>r. {x. 0 < dist x a \<and> dist x a < r}) ` {r. 0 < r})"
 
 definition
@@ -1088,7 +1088,7 @@
   "trivial_limit net \<longleftrightarrow> {} \<in> Rep_net net"
 
 lemma trivial_limit_within:
-  fixes a :: "'a::perfect_space"
+  fixes a :: "'a::metric_space"
   shows "trivial_limit (at a within S) \<longleftrightarrow> \<not> a islimpt S"
 proof
   assume "trivial_limit (at a within S)"
@@ -1112,12 +1112,18 @@
     done
 qed
 
-lemma trivial_limit_at: "\<not> trivial_limit (at a)"
+lemma trivial_limit_at_iff: "trivial_limit (at a) \<longleftrightarrow> \<not> a islimpt UNIV"
   using trivial_limit_within [of a UNIV]
   by (simp add: within_UNIV)
 
+lemma trivial_limit_at:
+  fixes a :: "'a::perfect_space"
+  shows "\<not> trivial_limit (at a)"
+  by (simp add: trivial_limit_at_iff)
+
 lemma trivial_limit_at_infinity:
   "\<not> trivial_limit (at_infinity :: ('a::{real_normed_vector,zero_neq_one}) net)"
+  (* FIXME: find a more appropriate type class *)
   unfolding trivial_limit_def Rep_net_at_infinity
   apply (clarsimp simp add: expand_set_eq)
   apply (drule_tac x="scaleR r (sgn 1)" in spec)
@@ -1636,7 +1642,7 @@
 apply (subst within_UNIV[symmetric]) by (simp add: Lim_within_id)
 
 lemma Lim_at_zero:
-  fixes a :: "'a::{real_normed_vector, perfect_space}"
+  fixes a :: "'a::real_normed_vector"
   shows "(f ---> l) (at a) \<longleftrightarrow> ((\<lambda>x. f(a + x)) ---> l) (at 0)" (is "?lhs = ?rhs")
 proof
   assume "?lhs"
@@ -1696,7 +1702,9 @@
 apply simp
 done
 
-lemma netlimit_at: "netlimit (at a) = a"
+lemma netlimit_at:
+  fixes a :: "'a::perfect_space"
+  shows "netlimit (at a) = a"
   apply (subst within_UNIV[symmetric])
   using netlimit_within[of a UNIV]
   by (simp add: trivial_limit_at within_UNIV)
@@ -3069,7 +3077,9 @@
   using continuous_within [of x UNIV f] by (simp add: within_UNIV)
 
 lemma continuous_at_within:
+  fixes x :: "'a::perfect_space"
   assumes "continuous (at x) f"  shows "continuous (at x within s) f"
+  (* FIXME: generalize *)
 proof(cases "x islimpt s")
   case True show ?thesis using assms unfolding continuous_def and netlimit_at
     using Lim_at_within[of f "f x" x s]