merged
authorhuffman
Wed, 03 Jun 2009 12:24:09 -0700
changeset 31422 b8bdef62bfa6
parent 31421 1501fc26f11b (diff)
parent 31412 f2e6b6526092 (current diff)
child 31423 79e707bb0d6b
child 31438 a1c4c1500abe
merged
--- a/src/HOL/Complex.thy	Wed Jun 03 15:48:54 2009 +0200
+++ b/src/HOL/Complex.thy	Wed Jun 03 12:24:09 2009 -0700
@@ -268,26 +268,28 @@
 instantiation complex :: real_normed_field
 begin
 
-definition
-  complex_norm_def: "norm z = sqrt ((Re z)\<twosuperior> + (Im z)\<twosuperior>)"
+definition complex_norm_def:
+  "norm z = sqrt ((Re z)\<twosuperior> + (Im z)\<twosuperior>)"
 
 abbreviation
   cmod :: "complex \<Rightarrow> real" where
   "cmod \<equiv> norm"
 
-definition
-  complex_sgn_def: "sgn x = x /\<^sub>R cmod x"
+definition complex_sgn_def:
+  "sgn x = x /\<^sub>R cmod x"
 
-definition
-  dist_complex_def: "dist x y = cmod (x - y)"
+definition dist_complex_def:
+  "dist x y = cmod (x - y)"
+
+definition topo_complex_def [code del]:
+  "topo = {S::complex set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
 
 lemmas cmod_def = complex_norm_def
 
 lemma complex_norm [simp]: "cmod (Complex x y) = sqrt (x\<twosuperior> + y\<twosuperior>)"
   by (simp add: complex_norm_def)
 
-instance
-proof
+instance proof
   fix r :: real and x y :: complex
   show "0 \<le> norm x"
     by (induct x) simp
@@ -306,6 +308,8 @@
     by (rule complex_sgn_def)
   show "dist x y = cmod (x - y)"
     by (rule dist_complex_def)
+  show "topo = {S::complex set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
+    by (rule topo_complex_def)
 qed
 
 end
--- a/src/HOL/Library/Convex_Euclidean_Space.thy	Wed Jun 03 15:48:54 2009 +0200
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy	Wed Jun 03 12:24:09 2009 -0700
@@ -602,8 +602,8 @@
     have "\<exists>x\<ge>0. x \<le> 1 \<and> (1 - x) *s x1 + x *s x2 \<notin> e1 \<and> (1 - x) *s x1 + x *s x2 \<notin> e2"
       apply(rule connected_real_lemma) apply (simp add: `x1\<in>e1` `x2\<in>e2` dist_commute)+
       using * apply(simp add: dist_norm)
-      using as(1,2)[unfolded open_def] apply simp
-      using as(1,2)[unfolded open_def] apply simp
+      using as(1,2)[unfolded open_dist] apply simp
+      using as(1,2)[unfolded open_dist] apply simp
       using assms[unfolded convex_alt, THEN bspec[where x=x1], THEN bspec[where x=x2]] using x1 x2
       using as(3) by auto
     then obtain x where "x\<ge>0" "x\<le>1" "(1 - x) *s x1 + x *s x2 \<notin> e1"  "(1 - x) *s x1 + x *s x2 \<notin> e2" by auto
--- a/src/HOL/Library/Euclidean_Space.thy	Wed Jun 03 15:48:54 2009 +0200
+++ b/src/HOL/Library/Euclidean_Space.thy	Wed Jun 03 12:24:09 2009 -0700
@@ -506,6 +506,9 @@
 definition dist_vector_def:
   "dist (x::'a^'b) (y::'a^'b) = setL2 (\<lambda>i. dist (x$i) (y$i)) UNIV"
 
+definition topo_vector_def:
+  "topo = {S::('a ^ 'b) set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
+
 instance proof
   fix x y :: "'a ^ 'b"
   show "dist x y = 0 \<longleftrightarrow> x = y"
@@ -518,6 +521,9 @@
     apply (rule order_trans [OF _ setL2_triangle_ineq])
     apply (simp add: setL2_mono dist_triangle2)
     done
+next
+  show "topo = {S::('a ^ 'b) set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
+    by (rule topo_vector_def)
 qed
 
 end
--- a/src/HOL/Library/Inner_Product.thy	Wed Jun 03 15:48:54 2009 +0200
+++ b/src/HOL/Library/Inner_Product.thy	Wed Jun 03 12:24:09 2009 -0700
@@ -10,7 +10,7 @@
 
 subsection {* Real inner product spaces *}
 
-class real_inner = real_vector + sgn_div_norm + dist_norm +
+class real_inner = real_vector + sgn_div_norm + dist_norm + topo_dist +
   fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
   assumes inner_commute: "inner x y = inner y x"
   and inner_left_distrib: "inner (x + y) z = inner x z + inner y z"
--- a/src/HOL/Library/Product_Vector.thy	Wed Jun 03 15:48:54 2009 +0200
+++ b/src/HOL/Library/Product_Vector.thy	Wed Jun 03 12:24:09 2009 -0700
@@ -39,6 +39,39 @@
 
 end
 
+subsection {* Product is a topological space *}
+
+instantiation
+  "*" :: (topological_space, topological_space) topological_space
+begin
+
+definition topo_prod_def:
+  "topo = {S. \<forall>x\<in>S. \<exists>A\<in>topo. \<exists>B\<in>topo. x \<in> A \<times> B \<and> A \<times> B \<subseteq> S}"
+
+instance proof
+  show "(UNIV :: ('a \<times> 'b) set) \<in> topo"
+    unfolding topo_prod_def by (auto intro: topo_UNIV)
+next
+  fix S T :: "('a \<times> 'b) set"
+  assume "S \<in> topo" "T \<in> topo" thus "S \<inter> T \<in> topo"
+    unfolding topo_prod_def
+    apply clarify
+    apply (drule (1) bspec)+
+    apply (clarify, rename_tac Sa Ta Sb Tb)
+    apply (rule_tac x="Sa \<inter> Ta" in rev_bexI)
+    apply (simp add: topo_Int)
+    apply (rule_tac x="Sb \<inter> Tb" in rev_bexI)
+    apply (simp add: topo_Int)
+    apply fast
+    done
+next
+  fix T :: "('a \<times> 'b) set set"
+  assume "T \<subseteq> topo" thus "\<Union>T \<in> topo"
+    unfolding topo_prod_def Bex_def by fast
+qed
+
+end
+
 subsection {* Product is a metric space *}
 
 instantiation
@@ -67,6 +100,53 @@
     apply (rule power_mono [OF dist_triangle2 [of _ _ "snd z"] zero_le_dist])
     apply (simp only: real_sum_squared_expand)
     done
+next
+  (* FIXME: long proof! *)
+  (* Maybe it would be easier to define topological spaces *)
+  (* in terms of neighborhoods instead of open sets? *)
+  show "topo = {S::('a \<times> 'b) set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
+    unfolding topo_prod_def topo_dist
+    apply (safe, rename_tac S a b)
+    apply (drule (1) bspec)
+    apply clarify
+    apply (drule (1) bspec)+
+    apply (clarify, rename_tac r s)
+    apply (rule_tac x="min r s" in exI, simp)
+    apply (clarify, rename_tac c d)
+    apply (erule subsetD)
+    apply (simp add: dist_Pair_Pair)
+    apply (rule conjI)
+    apply (drule spec, erule mp)
+    apply (erule le_less_trans [OF real_sqrt_sum_squares_ge1])
+    apply (drule spec, erule mp)
+    apply (erule le_less_trans [OF real_sqrt_sum_squares_ge2])
+
+    apply (rename_tac S a b)
+    apply (drule (1) bspec)
+    apply clarify
+    apply (subgoal_tac "\<exists>r>0. \<exists>s>0. e = sqrt (r\<twosuperior> + s\<twosuperior>)")
+    apply clarify
+    apply (rule_tac x="{y. dist y a < r}" in rev_bexI)
+    apply clarify
+    apply (rule_tac x="r - dist x a" in exI, rule conjI, simp)
+    apply clarify
+    apply (rule le_less_trans [OF dist_triangle])
+    apply (erule less_le_trans [OF add_strict_right_mono], simp)
+    apply (rule_tac x="{y. dist y b < s}" in rev_bexI)
+    apply clarify
+    apply (rule_tac x="s - dist x b" in exI, rule conjI, simp)
+    apply clarify
+    apply (rule le_less_trans [OF dist_triangle])
+    apply (erule less_le_trans [OF add_strict_right_mono], simp)
+    apply (rule conjI)
+    apply simp
+    apply (clarify, rename_tac c d)
+    apply (drule spec, erule mp)
+    apply (simp add: dist_Pair_Pair add_strict_mono power_strict_mono)
+    apply (rule_tac x="e / sqrt 2" in exI, simp add: divide_pos_pos)
+    apply (rule_tac x="e / sqrt 2" in exI, simp add: divide_pos_pos)
+    apply (simp add: power_divide)
+    done
 qed
 
 end
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Wed Jun 03 15:48:54 2009 +0200
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Wed Jun 03 12:24:09 2009 -0700
@@ -194,35 +194,30 @@
   by (simp add: subtopology_superset)
 
 subsection{* The universal Euclidean versions are what we use most of the time *}
+
 definition
-  "open" :: "'a::metric_space set \<Rightarrow> bool" where
-  "open S \<longleftrightarrow> (\<forall>x \<in> S. \<exists>e >0. \<forall>x'. dist x' x < e \<longrightarrow> x' \<in> S)"
-definition "closed S \<longleftrightarrow> open(UNIV - S)"
-definition "euclidean = topology open"
-
-lemma open_empty[intro,simp]: "open {}" by (simp add: open_def)
+  "open" :: "'a::topological_space set \<Rightarrow> bool" where
+  "open S \<longleftrightarrow> S \<in> topo"
+
+definition
+  closed :: "'a::topological_space set \<Rightarrow> bool" where
+  "closed S \<longleftrightarrow> open(UNIV - S)"
+
+definition
+  euclidean :: "'a::topological_space topology" where
+  "euclidean = topology open"
+
 lemma open_UNIV[intro,simp]:  "open UNIV"
-  by (simp add: open_def, rule exI[where x="1"], auto)
-
-lemma open_inter[intro]: assumes S: "open S" and T: "open T"
-  shows "open (S \<inter> T)"
-proof-
-  note thS = S[unfolded open_def, rule_format]
-  note thT = T[unfolded open_def, rule_format]
-  {fix x assume x: "x \<in> S\<inter>T"
-    hence xS: "x \<in> S" and xT: "x \<in> T" by simp_all
-    from thS[OF xS] obtain eS where eS: "eS > 0" "\<forall>x'. dist x' x < eS \<longrightarrow> x' \<in> S" by blast
-    from thT[OF xT] obtain eT where eT: "eT > 0" "\<forall>x'. dist x' x < eT \<longrightarrow> x' \<in> T" by blast
-    from real_lbound_gt_zero[OF eS(1) eT(1)] obtain e where e: "e > 0" "e < eS" "e < eT" by blast
-    { fix x' assume d: "dist x' x < e"
-      hence dS: "dist x' x < eS" and dT: "dist x' x < eT" using e by arith+
-      from eS(2)[rule_format, OF dS] eT(2)[rule_format, OF dT] have "x' \<in> S\<inter>T" by blast}
-    hence "\<exists>e >0. \<forall>x'. dist x' x < e \<longrightarrow> x' \<in> (S\<inter>T)" using e by blast}
-  then show ?thesis unfolding open_def by blast
-qed
+  unfolding open_def by (rule topo_UNIV)
+
+lemma open_inter[intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<inter> T)"
+  unfolding open_def by (rule topo_Int)
 
 lemma open_Union[intro]: "(\<forall>S\<in>K. open S) \<Longrightarrow> open (\<Union> K)"
-  by (simp add: open_def) metis
+  unfolding open_def subset_eq [symmetric] by (rule topo_Union)
+
+lemma open_empty[intro,simp]: "open {}"
+  using open_Union [of "{}"] by simp
 
 lemma open_openin: "open S \<longleftrightarrow> openin euclidean S"
   unfolding euclidean_def
@@ -242,7 +237,9 @@
 lemma closed_closedin: "closed S \<longleftrightarrow> closedin euclidean S"
   by (simp add: closed_def closedin_def topspace_euclidean open_openin)
 
-lemma open_Un[intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S\<union>T)"
+lemma open_Un[intro]:
+  fixes S T :: "'a::topological_space set"
+  shows "open S \<Longrightarrow> open T \<Longrightarrow> open (S\<union>T)"
   by (auto simp add: open_openin)
 
 lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)"
@@ -320,6 +317,11 @@
 
 subsection{* Topological properties of open balls *}
 
+lemma open_dist:
+  fixes S :: "'a::metric_space set"
+  shows "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>x'. dist x' x < e \<longrightarrow> x' \<in> S)"
+  unfolding open_def topo_dist by simp
+
 lemma diff_less_iff: "(a::real) - b > 0 \<longleftrightarrow> a > b"
   "(a::real) - b < 0 \<longleftrightarrow> a < b"
   "a - b < c \<longleftrightarrow> a < c +b" "a - b > c \<longleftrightarrow> a > c +b" by arith+
@@ -327,7 +329,7 @@
   "a - b \<le> c \<longleftrightarrow> a \<le> c +b" "a - b \<ge> c \<longleftrightarrow> a \<ge> c +b"  by arith+
 
 lemma open_ball[intro, simp]: "open (ball x e)"
-  unfolding open_def ball_def Collect_def Ball_def mem_def
+  unfolding open_dist ball_def Collect_def Ball_def mem_def
   unfolding dist_commute
   apply clarify
   apply (rule_tac x="e - dist xa x" in exI)
@@ -340,7 +342,7 @@
 
 lemma centre_in_ball[simp]: "x \<in> ball x e \<longleftrightarrow> e > 0" by (metis mem_ball dist_self)
 lemma open_contains_ball: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. ball x e \<subseteq> S)"
-  unfolding open_def subset_eq mem_ball Ball_def dist_commute ..
+  unfolding open_dist subset_eq mem_ball Ball_def dist_commute ..
 
 lemma open_contains_ball_eq: "open S \<Longrightarrow> \<forall>x. x\<in>S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)"
   by (metis open_contains_ball subset_eq centre_in_ball)
@@ -382,11 +384,13 @@
 lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> closedin (subtopology euclidean T) S"
   by (auto simp add: closedin_closed)
 
-lemma openin_euclidean_subtopology_iff: "openin (subtopology euclidean U) S
+lemma openin_euclidean_subtopology_iff:
+  fixes S U :: "'a::metric_space set"
+  shows "openin (subtopology euclidean U) S
   \<longleftrightarrow> S \<subseteq> U \<and> (\<forall>x\<in>S. \<exists>e>0. \<forall>x'\<in>U. dist x' x < e \<longrightarrow> x'\<in> S)" (is "?lhs \<longleftrightarrow> ?rhs")
 proof-
   {assume ?lhs hence ?rhs unfolding openin_subtopology open_openin[symmetric]
-      by (simp add: open_def) blast}
+      by (simp add: open_dist) blast}
   moreover
   {assume SU: "S \<subseteq> U" and H: "\<And>x. x \<in> S \<Longrightarrow> \<exists>e>0. \<forall>x'\<in>U. dist x' x < e \<longrightarrow> x' \<in> S"
     from H obtain d where d: "\<And>x . x\<in> S \<Longrightarrow> d x > 0 \<and> (\<forall>x' \<in> U. dist x' x < d x \<longrightarrow> x' \<in> S)"
@@ -441,7 +445,7 @@
                  e1 \<inter> e2 = {} \<and>
                  ~(e1 = {}) \<and>
                  ~(e2 = {}))"
-unfolding connected_def openin_open by blast
+unfolding connected_def openin_open by (safe, blast+)
 
 lemma exists_diff: "(\<exists>S. P(UNIV - S)) \<longleftrightarrow> (\<exists>S. P S)" (is "?lhs \<longleftrightarrow> ?rhs")
 proof-
@@ -480,31 +484,61 @@
 
 subsection{* Hausdorff and other separation properties *}
 
-lemma hausdorff:
-  assumes xy: "x \<noteq> y"
-  shows "\<exists>U V. open U \<and> open V \<and> x\<in> U \<and> y \<in> V \<and> (U \<inter> V = {})" (is "\<exists>U V. ?P U V")
-proof-
+axclass t0_space \<subseteq> topological_space
+  t0_space:
+    "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U)"
+
+axclass t1_space \<subseteq> topological_space
+  t1_space:
+    "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<notin> U \<and> x \<notin> V \<and> y \<in> V"
+
+instance t1_space \<subseteq> t0_space
+by default (fast dest: t1_space)
+
+text {* T2 spaces are also known as Hausdorff spaces. *}
+
+axclass t2_space \<subseteq> topological_space
+  hausdorff:
+    "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
+
+instance t2_space \<subseteq> t1_space
+by default (fast dest: hausdorff)
+
+instance metric_space \<subseteq> t2_space
+proof
+  fix x y :: "'a::metric_space"
+  assume xy: "x \<noteq> y"
   let ?U = "ball x (dist x y / 2)"
   let ?V = "ball y (dist x y / 2)"
   have th0: "\<And>d x y z. (d x z :: real) <= d x y + d y z \<Longrightarrow> d y z = d z y
                ==> ~(d x y * 2 < d x z \<and> d z y * 2 < d x z)" by arith
-  have "?P ?U ?V" using dist_pos_lt[OF xy] th0[of dist,OF dist_triangle dist_commute]
-    by (auto simp add: expand_set_eq less_divide_eq_number_of1)
-  then show ?thesis by blast
-qed
-
-lemma separation_t2: "x \<noteq> y \<longleftrightarrow> (\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {})"
+  have "open ?U \<and> open ?V \<and> x \<in> ?U \<and> y \<in> ?V \<and> ?U \<inter> ?V = {}"
+    using dist_pos_lt[OF xy] th0[of dist,OF dist_triangle dist_commute]
+    by (auto simp add: expand_set_eq)
+  then show "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
+    by blast
+qed
+
+lemma separation_t2:
+  fixes x y :: "'a::t2_space"
+  shows "x \<noteq> y \<longleftrightarrow> (\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {})"
   using hausdorff[of x y] by blast
 
-lemma separation_t1: "x \<noteq> y \<longleftrightarrow> (\<exists>U V. open U \<and> open V \<and> x \<in>U \<and> y\<notin> U \<and> x\<notin>V \<and> y\<in>V)"
-  using separation_t2[of x y] by blast
-
-lemma separation_t0: "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> ~(x\<in>U \<longleftrightarrow> y\<in>U))" by(metis separation_t1)
+lemma separation_t1:
+  fixes x y :: "'a::t1_space"
+  shows "x \<noteq> y \<longleftrightarrow> (\<exists>U V. open U \<and> open V \<and> x \<in>U \<and> y\<notin> U \<and> x\<notin>V \<and> y\<in>V)"
+  using t1_space[of x y] by blast
+
+lemma separation_t0:
+  fixes x y :: "'a::t0_space"
+  shows "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> ~(x\<in>U \<longleftrightarrow> y\<in>U))"
+  using t0_space[of x y] by blast
 
 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????*)
@@ -513,23 +547,29 @@
   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)
   apply auto
   apply(rule_tac x=y in bexI)
   apply (auto simp add: dist_commute)
-  apply (simp add: open_def, drule (1) bspec)
+  apply (simp add: open_dist, drule (1) bspec)
   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:
@@ -544,7 +584,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"
@@ -576,7 +616,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-
@@ -616,7 +656,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)
 
@@ -624,13 +666,14 @@
   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:
+  fixes S :: "'a::metric_space set"
   assumes e: "0 < e" and d: "\<forall>x \<in> S. \<forall>y \<in> S. dist y x < e \<longrightarrow> y = x"
   shows "closed S"
 proof-
@@ -644,7 +687,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 *}
@@ -652,7 +695,7 @@
 
 lemma interior_eq: "interior S = S \<longleftrightarrow> open S"
   apply (simp add: expand_set_eq interior_def)
-  apply (subst (2) open_subopen) by blast
+  apply (subst (2) open_subopen) by (safe, blast+)
 
 lemma interior_open: "open S ==> (interior S = S)" by (metis interior_eq)
 
@@ -701,7 +744,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
@@ -861,7 +903,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"
@@ -869,7 +914,7 @@
     { fix e::real
       assume "e > 0"
       from as `open S` obtain e' where "e' > 0" and e':"\<forall>x'. dist x' x < e' \<longrightarrow> x' \<in> S"
-	unfolding open_def
+	unfolding open_dist
 	by auto
       let ?e = "min e e'"
       from `e>0` `e'>0` have "?e > 0"
@@ -913,7 +958,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
@@ -1202,7 +1249,7 @@
   assume ?lhs
   { fix e::real assume "e>0"
     obtain d  where d:  "d >0" "\<forall>x\<in>S. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e" using `?lhs` `e>0` unfolding Lim_within by auto
-    obtain d' where d': "d'>0" "\<forall>x. dist x a < d' \<longrightarrow> x \<in> S" using assms  unfolding open_def by auto
+    obtain d' where d': "d'>0" "\<forall>x. dist x a < d' \<longrightarrow> x \<in> S" using assms  unfolding open_dist by auto
     from d d' have "\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e" by (rule_tac x= "min d d'" in exI)auto
   }
   thus ?rhs unfolding Lim_at by auto
@@ -1620,7 +1667,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)
@@ -1628,7 +1674,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)"
@@ -1642,7 +1687,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])
@@ -1652,7 +1696,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)"
@@ -1663,7 +1706,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)"
@@ -1673,8 +1715,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-
@@ -1715,15 +1755,21 @@
 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)
 
-lemma closed_approachable: "closed S ==> (\<forall>e>0. \<exists>y\<in>S. dist y x < e) \<longleftrightarrow> x \<in> S"
+lemma closed_approachable:
+  fixes S :: "'a::metric_space set"
+  shows "closed S ==> (\<forall>e>0. \<exists>y\<in>S. dist y x < e) \<longleftrightarrow> x \<in> S"
   by (metis closure_closed closure_approachable)
 
 text{* Some other lemmas about sequences. *}
@@ -1758,7 +1804,7 @@
 lemma closed_cball: "closed (cball x e)"
 unfolding cball_def closed_def Compl_eq_Diff_UNIV [symmetric]
 unfolding Collect_neg_eq [symmetric] not_le
-apply (clarsimp simp add: open_def, rename_tac y)
+apply (clarsimp simp add: open_dist, rename_tac y)
 apply (rule_tac x="dist x y - e" in exI, clarsimp)
 apply (cut_tac x=x and y=x' and z=y in dist_triangle)
 apply simp
@@ -1876,7 +1922,7 @@
   case True note cs = this
   have "ball x e \<subseteq> cball x e" using ball_subset_cball by auto moreover
   { fix S y assume as: "S \<subseteq> cball x e" "open S" "y\<in>S"
-    then obtain d where "d>0" and d:"\<forall>x'. dist x' y < d \<longrightarrow> x' \<in> S" unfolding open_def by blast
+    then obtain d where "d>0" and d:"\<forall>x'. dist x' y < d \<longrightarrow> x' \<in> S" unfolding open_dist by blast
 
     then obtain xa where xa:"dist y xa = d / 2" using vector_choose_dist[of "d/2" y] by auto
     hence xa_y:"xa \<noteq> y" using dist_nz[of y xa] using `d>0` by auto
@@ -2506,7 +2552,7 @@
 
   obtain b where "l\<in>b" "b\<in>t" using assms(2) and l by auto
   then obtain e where "e>0" and e:"\<forall>z. dist z l < e \<longrightarrow> z\<in>b"
-    using assms(3)[THEN bspec[where x=b]] unfolding open_def by auto
+    using assms(3)[THEN bspec[where x=b]] unfolding open_dist by auto
 
   then obtain N1 where N1:"\<forall>n\<ge>N1. dist ((f \<circ> r) n) l < e / 2"
     using lr[unfolded Lim_sequentially, THEN spec[where x="e/2"]] by auto
@@ -2672,6 +2718,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-
@@ -2797,8 +2844,10 @@
   unfolding compact_def o_def
   by (auto simp add: tendsto_const)
 
-lemma closed_sing [simp]: shows "closed {a}"
-  apply (clarsimp simp add: closed_def open_def)
+lemma closed_sing [simp]:
+  fixes a :: "'a::metric_space"
+  shows "closed {a}"
+  apply (clarsimp simp add: closed_def open_dist)
   apply (rule ccontr)
   apply (drule_tac x="dist x a" in spec)
   apply (simp add: dist_nz dist_commute)
@@ -2829,7 +2878,9 @@
   using frontier_subset_closed compact_eq_bounded_closed
   by blast
 
-lemma open_delete: "open s ==> open(s - {x})"
+lemma open_delete:
+  fixes s :: "'a::metric_space set"
+  shows "open s ==> open(s - {x})"
   using open_diff[of s "{x}"] closed_sing
   by blast
 
@@ -3443,7 +3494,7 @@
   { fix t assume as: "open t" "f x \<in> t"
     then obtain e where "e>0" and e:"ball (f x) e \<subseteq> t" unfolding open_contains_ball by auto
 
-    obtain d where "d>0" and d:"\<forall>y. 0 < dist y x \<and> dist y x < d \<longrightarrow> dist (f y) (f x) < e" using `e>0` using `?lhs`[unfolded continuous_at Lim_at open_def] by auto
+    obtain d where "d>0" and d:"\<forall>y. 0 < dist y x \<and> dist y x < d \<longrightarrow> dist (f y) (f x) < e" using `e>0` using `?lhs`[unfolded continuous_at Lim_at open_dist] by auto
 
     have "open (ball x d)" using open_ball by auto
     moreover have "x \<in> ball x d" unfolding centre_in_ball using `d>0` by simp
@@ -3672,7 +3723,7 @@
   shows "open((\<lambda>x. c *s x) ` s)"
 proof-
   { fix x assume "x \<in> s"
-    then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> s" using assms(2)[unfolded open_def, THEN bspec[where x=x]] by auto
+    then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> s" using assms(2)[unfolded open_dist, THEN bspec[where x=x]] by auto
     have "e * abs c > 0" using assms(1)[unfolded zero_less_abs_iff[THEN sym]] using real_mult_order[OF `e>0`] by auto
     moreover
     { fix y assume "dist y (c *s x) < e * \<bar>c\<bar>"
@@ -3681,7 +3732,7 @@
 	  assms(1)[unfolded zero_less_abs_iff[THEN sym]] by (simp del:zero_less_abs_iff)
       hence "y \<in> op *s c ` s" using rev_image_eqI[of "(1 / c) *s y" s y "op *s c"]  e[THEN spec[where x="(1 / c) *s y"]]  assms(1) unfolding dist_norm vector_smult_assoc by auto  }
     ultimately have "\<exists>e>0. \<forall>x'. dist x' (c *s x) < e \<longrightarrow> x' \<in> op *s c ` s" apply(rule_tac x="e * abs c" in exI) by auto  }
-  thus ?thesis unfolding open_def by auto
+  thus ?thesis unfolding open_dist by auto
 qed
 
 lemma open_negations:
@@ -3906,7 +3957,7 @@
   fixes s :: "real set" shows
  "open(vec1 ` s) \<longleftrightarrow>
         (\<forall>x \<in> s. \<exists>e>0. \<forall>x'. abs(x' - x) < e --> x' \<in> s)" (is "?lhs = ?rhs")
-  unfolding open_def apply simp unfolding forall_vec1 dist_vec1 vec1_in_image_vec1 by simp
+  unfolding open_dist apply simp unfolding forall_vec1 dist_vec1 vec1_in_image_vec1 by simp
 
 lemma islimpt_approachable_vec1:
   fixes s :: "real set" shows
@@ -4666,7 +4717,7 @@
       hence "a < x' \<and> x' < b" unfolding vector_less_def by auto  }
     ultimately have "\<exists>e>0. \<forall>x'. dist x' x < e \<longrightarrow> x' \<in> {a<..<b}" by (auto, rule_tac x="?d" in exI, simp)
   }
-  thus ?thesis unfolding open_def using open_interval_lemma by auto
+  thus ?thesis unfolding open_dist using open_interval_lemma by auto
 qed
 
 lemma closed_interval: fixes a :: "real^'n::finite" shows "closed {a .. b}"
@@ -4695,7 +4746,7 @@
 next
   { fix x assume "\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> {a..b}"
     then obtain s where s:"open s" "x \<in> s" "s \<subseteq> {a..b}" by auto
-    then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> {a..b}" unfolding open_def and subset_eq by auto
+    then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> {a..b}" unfolding open_dist and subset_eq by auto
     { fix i
       have "dist (x - (e / 2) *s basis i) x < e"
 	   "dist (x + (e / 2) *s basis i) x < e"
--- a/src/HOL/RealVector.thy	Wed Jun 03 15:48:54 2009 +0200
+++ b/src/HOL/RealVector.thy	Wed Jun 03 12:24:09 2009 -0700
@@ -416,12 +416,26 @@
   by (rule Reals_cases) auto
 
 
+subsection {* Topological spaces *}
+
+class topo =
+  fixes topo :: "'a set set"
+
+class topological_space = topo +
+  assumes topo_UNIV: "UNIV \<in> topo"
+  assumes topo_Int: "A \<in> topo \<Longrightarrow> B \<in> topo \<Longrightarrow> A \<inter> B \<in> topo"
+  assumes topo_Union: "T \<subseteq> topo \<Longrightarrow> \<Union>T \<in> topo"
+
+
 subsection {* Metric spaces *}
 
 class dist =
   fixes dist :: "'a \<Rightarrow> 'a \<Rightarrow> real"
 
-class metric_space = dist +
+class topo_dist = topo + dist +
+  assumes topo_dist: "topo = {S. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
+
+class metric_space = topo_dist +
   assumes dist_eq_0_iff [simp]: "dist x y = 0 \<longleftrightarrow> x = y"
   assumes dist_triangle2: "dist x y \<le> dist x z + dist y z"
 begin
@@ -452,6 +466,26 @@
 lemma dist_triangle: "dist x z \<le> dist x y + dist y z"
 using dist_triangle2 [of x z y] by (simp add: dist_commute)
 
+subclass topological_space
+proof
+  have "\<exists>e::real. 0 < e"
+    by (fast intro: zero_less_one)
+  then show "UNIV \<in> topo"
+    unfolding topo_dist by simp
+next
+  fix A B assume "A \<in> topo" "B \<in> topo"
+  then show "A \<inter> B \<in> topo"
+    unfolding topo_dist
+    apply clarify
+    apply (drule (1) bspec)+
+    apply (clarify, rename_tac r s)
+    apply (rule_tac x="min r s" in exI, simp)
+    done
+next
+  fix T assume "T \<subseteq> topo" thus "\<Union>T \<in> topo"
+    unfolding topo_dist by fast
+qed
+
 end
 
 
@@ -466,7 +500,7 @@
 class dist_norm = dist + norm + minus +
   assumes dist_norm: "dist x y = norm (x - y)"
 
-class real_normed_vector = real_vector + sgn_div_norm + dist_norm +
+class real_normed_vector = real_vector + sgn_div_norm + dist_norm + topo_dist +
   assumes norm_ge_zero [simp]: "0 \<le> norm x"
   and norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = 0"
   and norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y"
@@ -497,16 +531,20 @@
 instantiation real :: real_normed_field
 begin
 
-definition
-  real_norm_def [simp]: "norm r = \<bar>r\<bar>"
+definition real_norm_def [simp]:
+  "norm r = \<bar>r\<bar>"
 
-definition
-  dist_real_def: "dist x y = \<bar>x - y\<bar>"
+definition dist_real_def:
+  "dist x y = \<bar>x - y\<bar>"
+
+definition topo_real_def [code del]:
+  "topo = {S::real set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
 
 instance
 apply (intro_classes, unfold real_norm_def real_scaleR_def)
 apply (rule dist_real_def)
 apply (simp add: real_sgn_def)
+apply (rule topo_real_def)
 apply (rule abs_ge_zero)
 apply (rule abs_eq_0)
 apply (rule abs_triangle_ineq)