# HG changeset patch
# User huffman
# Date 1244053369 25200
# Node ID 4c22ef11078b8c9f9167fa694fa637b5a1ee8c9f
# Parent  74fc28c5d68c37d9de5d07ca496dc35948821dc5
generalize type of islimpt

diff -r 74fc28c5d68c -r 4c22ef11078b src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Wed Jun 03 10:29:11 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Wed Jun 03 11:22:49 2009 -0700
@@ -515,7 +515,8 @@
 subsection{* Limit points *}
 
 definition
-  islimpt:: "'a::metric_space \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "islimpt" 60) where
+  islimpt:: "'a::topological_space \<Rightarrow> 'a set \<Rightarrow> bool"
+    (infixr "islimpt" 60) where
   "x islimpt S \<longleftrightarrow> (\<forall>T. x\<in>T \<longrightarrow> open T \<longrightarrow> (\<exists>y\<in>S. y\<in>T \<and> y\<noteq>x))"
 
   (* FIXME: Sure this form is OK????*)
@@ -524,7 +525,10 @@
   using assms unfolding islimpt_def by auto
 
 lemma islimpt_subset: "x islimpt S \<Longrightarrow> S \<subseteq> T ==> x islimpt T" by (auto simp add: islimpt_def)
-lemma islimpt_approachable: "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e)"
+
+lemma islimpt_approachable:
+  fixes x :: "'a::metric_space"
+  shows "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e)"
   unfolding islimpt_def
   apply auto
   apply(erule_tac x="ball x e" in allE)
@@ -535,12 +539,15 @@
   apply (clarify, drule spec, drule (1) mp, auto)
   done
 
-lemma islimpt_approachable_le: "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in> S. x' \<noteq> x \<and> dist x' x <= e)"
+lemma islimpt_approachable_le:
+  fixes x :: "'a::metric_space"
+  shows "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in> S. x' \<noteq> x \<and> dist x' x <= e)"
   unfolding islimpt_approachable
   using approachable_lt_le[where f="\<lambda>x'. dist x' x" and P="\<lambda>x'. \<not> (x'\<in>S \<and> x'\<noteq>x)"]
   by metis (* FIXME: VERY slow! *)
 
 axclass perfect_space \<subseteq> metric_space
+  (* FIXME: perfect_space should inherit from topological_space *)
   islimpt_UNIV [simp, intro]: "x islimpt UNIV"
 
 lemma perfect_choose_dist:
@@ -555,7 +562,7 @@
 apply (clarify, rule_tac x="x + e/2" in bexI)
 apply (auto simp add: dist_norm)
 done
-  
+
 instance "^" :: (perfect_space, finite) perfect_space
 proof
   fix x :: "'a ^ 'b"
@@ -587,7 +594,7 @@
   by (metis DiffE DiffI UNIV_I insertCI insert_absorb mem_def)
 
 lemma islimpt_EMPTY[simp]: "\<not> x islimpt {}"
-  unfolding islimpt_approachable apply auto by ferrack
+  unfolding islimpt_def by auto
 
 lemma closed_positive_orthant: "closed {x::real^'n::finite. \<forall>i. 0 \<le>x$i}"
 proof-
@@ -627,7 +634,9 @@
   ultimately show ?case by blast
 qed
 
-lemma islimpt_finite: assumes fS: "finite S" shows "\<not> a islimpt S"
+lemma islimpt_finite:
+  fixes S :: "'a::metric_space set"
+  assumes fS: "finite S" shows "\<not> a islimpt S"
   unfolding islimpt_approachable
   using finite_set_avoid[OF fS, of a] by (metis dist_commute  not_le)
 
@@ -635,10 +644,10 @@
   apply (rule iffI)
   defer
   apply (metis Un_upper1 Un_upper2 islimpt_subset)
-  unfolding islimpt_approachable
-  apply auto
-  apply (erule_tac x="min e ea" in allE)
-  apply auto
+  unfolding islimpt_def
+  apply (rule ccontr, clarsimp, rename_tac A B)
+  apply (drule_tac x="A \<inter> B" in spec)
+  apply (auto simp add: open_inter)
   done
 
 lemma discrete_imp_closed:
@@ -656,7 +665,7 @@
       by (intro dist_triangle_lt [where z=x], simp)
     from d[rule_format, OF y(1) z(1) th] y z
     have False by (auto simp add: dist_commute)}
-  then show ?thesis by (metis islimpt_approachable closed_limpt)
+  then show ?thesis by (metis islimpt_approachable closed_limpt [where 'a='a])
 qed
 
 subsection{* Interior of a Set *}
@@ -713,7 +722,6 @@
 qed
 
 lemma interior_closed_Un_empty_interior:
-  fixes S T :: "'a::metric_space set"
   assumes cS: "closed S" and iT: "interior T = {}"
   shows "interior(S \<union> T) = interior S"
 proof
@@ -873,7 +881,10 @@
   unfolding closure_interior
   by auto
 
-lemma open_inter_closure_subset: "open S \<Longrightarrow> (S \<inter> (closure T)) \<subseteq> closure(S \<inter> T)"
+lemma open_inter_closure_subset:
+  fixes S :: "'a::metric_space set"
+    (* FIXME: generalize to topological_space *)
+  shows "open S \<Longrightarrow> (S \<inter> (closure T)) \<subseteq> closure(S \<inter> T)"
 proof
   fix x
   assume as: "open S" "x \<in> S \<inter> closure T"
@@ -925,7 +936,9 @@
 lemma frontier_closures: "frontier S = (closure S) \<inter> (closure(UNIV - S))"
   by (auto simp add: frontier_def interior_closure)
 
-lemma frontier_straddle: "a \<in> frontier S \<longleftrightarrow> (\<forall>e>0. (\<exists>x\<in>S. dist a x < e) \<and> (\<exists>x. x \<notin> S \<and> dist a x < e))" (is "?lhs \<longleftrightarrow> ?rhs")
+lemma frontier_straddle:
+  fixes a :: "'a::metric_space"
+  shows "a \<in> frontier S \<longleftrightarrow> (\<forall>e>0. (\<exists>x\<in>S. dist a x < e) \<and> (\<exists>x. x \<notin> S \<and> dist a x < e))" (is "?lhs \<longleftrightarrow> ?rhs")
 proof
   assume "?lhs"
   { fix e::real
@@ -1632,7 +1645,6 @@
 qed
 
 lemma Lim_transform_eventually:
-  fixes f g :: "'a::type \<Rightarrow> 'b::metric_space"
   shows "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net ==> (g ---> l) net"
   unfolding tendsto_def
   apply (clarify, drule spec, drule (1) mp)
@@ -1640,7 +1652,6 @@
   done
 
 lemma Lim_transform_within:
-  fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space"
   assumes "0 < d" "(\<forall>x'\<in>S. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x')"
           "(f ---> l) (at x within S)"
   shows   "(g ---> l) (at x within S)"
@@ -1654,7 +1665,6 @@
   done
 
 lemma Lim_transform_at:
-  fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space"
   shows "0 < d \<Longrightarrow> (\<forall>x'. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x') \<Longrightarrow>
   (f ---> l) (at x) ==> (g ---> l) (at x)"
   apply (subst within_UNIV[symmetric])
@@ -1664,7 +1674,6 @@
 text{* Common case assuming being away from some crucial point like 0. *}
 
 lemma Lim_transform_away_within:
-  fixes f:: "'a::metric_space \<Rightarrow> 'b::metric_space"
   assumes "a\<noteq>b" "\<forall>x\<in> S. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
   and "(f ---> l) (at a within S)"
   shows "(g ---> l) (at a within S)"
@@ -1675,7 +1684,6 @@
 qed
 
 lemma Lim_transform_away_at:
-  fixes f:: "'a::metric_space \<Rightarrow> 'b::metric_space"
   assumes ab: "a\<noteq>b" and fg: "\<forall>x. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
   and fl: "(f ---> l) (at a)"
   shows "(g ---> l) (at a)"
@@ -1685,8 +1693,6 @@
 text{* Alternatively, within an open set. *}
 
 lemma Lim_transform_within_open:
-  fixes f:: "'a::metric_space \<Rightarrow> 'b::metric_space"
-    (* FIXME: generalize to metric_space *)
   assumes "open S"  "a \<in> S"  "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> f x = g x"  "(f ---> l) (at a)"
   shows "(g ---> l) (at a)"
 proof-
@@ -1727,11 +1733,15 @@
 qed
 
 lemma closed_sequential_limits:
- "closed S \<longleftrightarrow> (\<forall>x l. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially \<longrightarrow> l \<in> S)"
+  fixes S :: "'a::metric_space set"
+  shows "closed S \<longleftrightarrow> (\<forall>x l. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially \<longrightarrow> l \<in> S)"
   unfolding closed_limpt
-  by (metis closure_sequential closure_closed closed_limpt islimpt_sequential mem_delete)
-
-lemma closure_approachable: "x \<in> closure S \<longleftrightarrow> (\<forall>e>0. \<exists>y\<in>S. dist y x < e)"
+  using closure_sequential [where 'a='a] closure_closed [where 'a='a] closed_limpt [where 'a='a] islimpt_sequential [where 'a='a] mem_delete [where 'a='a]
+  by metis
+
+lemma closure_approachable:
+  fixes S :: "'a::metric_space set"
+  shows "x \<in> closure S \<longleftrightarrow> (\<forall>e>0. \<exists>y\<in>S. dist y x < e)"
   apply (auto simp add: closure_def islimpt_approachable)
   by (metis dist_self)
 
@@ -2686,6 +2696,7 @@
 qed
 
 lemma bolzano_weierstrass_imp_closed:
+  fixes s :: "'a::metric_space set" (* TODO: can this be generalized? *)
   assumes "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t)"
   shows "closed s"
 proof-