# HG changeset patch
# User huffman
# Date 1244422794 25200
# Node ID 5400beeddb555d96a4d52a30c6bf643e76f87f7f
# Parent  f7310185481d429c21e44d19009c3344fccd640a
replace 'topo' with 'open'; add extra type constraint for 'open'

diff -r f7310185481d -r 5400beeddb55 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Sun Jun 07 15:18:52 2009 -0700
+++ b/src/HOL/Complex.thy	Sun Jun 07 17:59:54 2009 -0700
@@ -281,8 +281,8 @@
 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}"
+definition open_complex_def [code del]:
+  "open (S :: complex set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
 
 lemmas cmod_def = complex_norm_def
 
@@ -290,7 +290,7 @@
   by (simp add: complex_norm_def)
 
 instance proof
-  fix r :: real and x y :: complex
+  fix r :: real and x y :: complex and S :: "complex set"
   show "0 \<le> norm x"
     by (induct x) simp
   show "(norm x = 0) = (x = 0)"
@@ -308,8 +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)
+  show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+    by (rule open_complex_def)
 qed
 
 end
diff -r f7310185481d -r 5400beeddb55 src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Sun Jun 07 15:18:52 2009 -0700
+++ b/src/HOL/Library/Euclidean_Space.thy	Sun Jun 07 17:59:54 2009 -0700
@@ -506,8 +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}"
+definition open_vector_def:
+  "open (S :: ('a ^ 'b) set) \<longleftrightarrow>
+    (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
 
 instance proof
   fix x y :: "'a ^ 'b"
@@ -522,8 +523,9 @@
     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)
+  fix S :: "('a ^ 'b) set"
+  show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+    by (rule open_vector_def)
 qed
 
 end
diff -r f7310185481d -r 5400beeddb55 src/HOL/Library/Inner_Product.thy
--- a/src/HOL/Library/Inner_Product.thy	Sun Jun 07 15:18:52 2009 -0700
+++ b/src/HOL/Library/Inner_Product.thy	Sun Jun 07 17:59:54 2009 -0700
@@ -10,7 +10,13 @@
 
 subsection {* Real inner product spaces *}
 
-text {* Temporarily relax constraints for @{term dist} and @{term norm}. *}
+text {*
+  Temporarily relax type constraints for @{term "open"},
+  @{term dist}, and @{term norm}.
+*}
+
+setup {* Sign.add_const_constraint
+  (@{const_name "open"}, SOME @{typ "'a::open set \<Rightarrow> bool"}) *}
 
 setup {* Sign.add_const_constraint
   (@{const_name dist}, SOME @{typ "'a::dist \<Rightarrow> 'a \<Rightarrow> real"}) *}
@@ -18,7 +24,7 @@
 setup {* Sign.add_const_constraint
   (@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"}) *}
 
-class real_inner = real_vector + sgn_div_norm + dist_norm + topo_dist +
+class real_inner = real_vector + sgn_div_norm + dist_norm + open_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"
@@ -124,7 +130,13 @@
 
 end
 
-text {* Re-enable constraints for @{term dist} and @{term norm}. *}
+text {*
+  Re-enable constraints for @{term "open"},
+  @{term dist}, and @{term norm}.
+*}
+
+setup {* Sign.add_const_constraint
+  (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"}) *}
 
 setup {* Sign.add_const_constraint
   (@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"}) *}
diff -r f7310185481d -r 5400beeddb55 src/HOL/Library/Product_Vector.thy
--- a/src/HOL/Library/Product_Vector.thy	Sun Jun 07 15:18:52 2009 -0700
+++ b/src/HOL/Library/Product_Vector.thy	Sun Jun 07 17:59:54 2009 -0700
@@ -45,29 +45,29 @@
   "*" :: (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}"
+definition open_prod_def:
+  "open (S :: ('a \<times> 'b) set) \<longleftrightarrow>
+    (\<forall>x\<in>S. \<exists>A B. open A \<and> open B \<and> 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)
+  show "open (UNIV :: ('a \<times> 'b) set)"
+    unfolding open_prod_def by auto
 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
+  assume "open S" "open T" thus "open (S \<inter> T)"
+    unfolding open_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 (rule_tac x="Sa \<inter> Ta" in exI)
+    apply (rule_tac x="Sb \<inter> Tb" in exI)
+    apply (simp add: open_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
+  fix K :: "('a \<times> 'b) set set"
+  assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
+    unfolding open_prod_def by fast
 qed
 
 end
@@ -104,9 +104,10 @@
   (* 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)
+  fix S :: "('a \<times> 'b) set"
+  show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+    unfolding open_prod_def open_dist
+    apply safe
     apply (drule (1) bspec)
     apply clarify
     apply (drule (1) bspec)+
@@ -121,18 +122,19 @@
     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 (rule_tac x="{y. dist y a < r}" in exI)
+    apply (rule_tac x="{y. dist y b < s}" in exI)
+    apply (rule conjI)
     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 (rule conjI)
     apply clarify
     apply (rule_tac x="s - dist x b" in exI, rule conjI, simp)
     apply clarify
@@ -163,13 +165,13 @@
   assumes "(f ---> a) net"
   shows "((\<lambda>x. fst (f x)) ---> fst a) net"
 proof (rule topological_tendstoI)
-  fix S assume "S \<in> topo" "fst a \<in> S"
-  then have "fst -` S \<in> topo" "a \<in> fst -` S"
-    unfolding topo_prod_def
+  fix S assume "open S" "fst a \<in> S"
+  then have "open (fst -` S)" "a \<in> fst -` S"
+    unfolding open_prod_def
     apply simp_all
     apply clarify
-    apply (erule rev_bexI, simp)
-    apply (rule rev_bexI [OF topo_UNIV])
+    apply (rule exI, erule conjI)
+    apply (rule exI, rule conjI [OF open_UNIV])
     apply auto
     done
   with assms have "eventually (\<lambda>x. f x \<in> fst -` S) net"
@@ -182,13 +184,13 @@
   assumes "(f ---> a) net"
   shows "((\<lambda>x. snd (f x)) ---> snd a) net"
 proof (rule topological_tendstoI)
-  fix S assume "S \<in> topo" "snd a \<in> S"
-  then have "snd -` S \<in> topo" "a \<in> snd -` S"
-    unfolding topo_prod_def
+  fix S assume "open S" "snd a \<in> S"
+  then have "open (snd -` S)" "a \<in> snd -` S"
+    unfolding open_prod_def
     apply simp_all
     apply clarify
-    apply (rule rev_bexI [OF topo_UNIV])
-    apply (erule rev_bexI)
+    apply (rule exI, rule conjI [OF open_UNIV])
+    apply (rule exI, erule conjI)
     apply auto
     done
   with assms have "eventually (\<lambda>x. f x \<in> snd -` S) net"
@@ -201,15 +203,15 @@
   assumes "(f ---> a) net" and "(g ---> b) net"
   shows "((\<lambda>x. (f x, g x)) ---> (a, b)) net"
 proof (rule topological_tendstoI)
-  fix S assume "S \<in> topo" "(a, b) \<in> S"
-  then obtain A B where "A \<in> topo" "B \<in> topo" "a \<in> A" "b \<in> B" "A \<times> B \<subseteq> S"
-    unfolding topo_prod_def by auto
+  fix S assume "open S" "(a, b) \<in> S"
+  then obtain A B where "open A" "open B" "a \<in> A" "b \<in> B" "A \<times> B \<subseteq> S"
+    unfolding open_prod_def by auto
   have "eventually (\<lambda>x. f x \<in> A) net"
-    using `(f ---> a) net` `A \<in> topo` `a \<in> A`
+    using `(f ---> a) net` `open A` `a \<in> A`
     by (rule topological_tendstoD)
   moreover
   have "eventually (\<lambda>x. g x \<in> B) net"
-    using `(g ---> b) net` `B \<in> topo` `b \<in> B`
+    using `(g ---> b) net` `open B` `b \<in> B`
     by (rule topological_tendstoD)
   ultimately
   show "eventually (\<lambda>x. (f x, g x) \<in> S) net"
diff -r f7310185481d -r 5400beeddb55 src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Sun Jun 07 15:18:52 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Sun Jun 07 17:59:54 2009 -0700
@@ -255,11 +255,6 @@
 
 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+
@@ -274,7 +269,7 @@
   using dist_triangle_alt[where z=x]
   apply (clarsimp simp add: diff_less_iff)
   apply atomize
-  apply (erule_tac x="x'" in allE)
+  apply (erule_tac x="y" in allE)
   apply (erule_tac x="xa" in allE)
   by arith
 
@@ -1004,7 +999,7 @@
   thus "\<not> a islimpt S"
     unfolding trivial_limit_def
     unfolding Rep_net_within Rep_net_at
-    unfolding islimpt_def open_def [symmetric]
+    unfolding islimpt_def
     apply (clarsimp simp add: expand_set_eq)
     apply (rename_tac T, rule_tac x=T in exI)
     apply (clarsimp, drule_tac x=y in spec, simp)
@@ -1014,7 +1009,7 @@
   thus "trivial_limit (at a within S)"
     unfolding trivial_limit_def
     unfolding Rep_net_within Rep_net_at
-    unfolding islimpt_def open_def [symmetric]
+    unfolding islimpt_def
     apply (clarsimp simp add: image_image)
     apply (rule_tac x=T in image_eqI)
     apply (auto simp add: expand_set_eq)
@@ -1164,7 +1159,8 @@
   shows "(f ---> l) (net within (S \<union> T))"
   using assms unfolding tendsto_def Limits.eventually_within
   apply clarify
-  apply (drule (1) bspec)+
+  apply (drule spec, drule (1) mp, drule (1) mp)
+  apply (drule spec, drule (1) mp, drule (1) mp)
   apply (auto elim: eventually_elim2)
   done
 
@@ -1177,7 +1173,7 @@
 
 lemma Lim_at_within: "(f ---> l) net ==> (f ---> l)(net within S)"
   unfolding tendsto_def Limits.eventually_within
-  apply (clarify, drule (1) bspec)
+  apply (clarify, drule spec, drule (1) mp, drule (1) mp)
   by (auto elim!: eventually_elim1)
 
 lemma Lim_within_open:
@@ -1192,13 +1188,13 @@
     hence "eventually (\<lambda>x. x \<in> S \<longrightarrow> dist (f x) l < e) (at a)"
       unfolding Limits.eventually_within .
     then obtain T where "open T" "a \<in> T" "\<forall>x\<in>T. x \<noteq> a \<longrightarrow> x \<in> S \<longrightarrow> dist (f x) l < e"
-      unfolding eventually_at_topological open_def by fast
+      unfolding eventually_at_topological by fast
     hence "open (T \<inter> S)" "a \<in> T \<inter> S" "\<forall>x\<in>(T \<inter> S). x \<noteq> a \<longrightarrow> dist (f x) l < e"
       using assms by auto
     hence "\<exists>T. open T \<and> a \<in> T \<and> (\<forall>x\<in>T. x \<noteq> a \<longrightarrow> dist (f x) l < e)"
       by fast
     hence "eventually (\<lambda>x. dist (f x) l < e) (at a)"
-      unfolding eventually_at_topological open_def Bex_def .
+      unfolding eventually_at_topological .
   }
   thus ?rhs by (rule tendstoI)
 next
@@ -1778,6 +1774,7 @@
 unfolding Collect_neg_eq [symmetric] not_le
 apply (clarsimp simp add: open_dist, rename_tac y)
 apply (rule_tac x="dist x y - e" in exI, clarsimp)
+apply (rename_tac x')
 apply (cut_tac x=x and y=x' and z=y in dist_triangle)
 apply simp
 done
diff -r f7310185481d -r 5400beeddb55 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Sun Jun 07 15:18:52 2009 -0700
+++ b/src/HOL/Limits.thy	Sun Jun 07 17:59:54 2009 -0700
@@ -114,7 +114,7 @@
 
 definition
   at :: "'a::topological_space \<Rightarrow> 'a net" where
-  [code del]: "at a = Abs_net ((\<lambda>S. S - {a}) ` {S\<in>topo. a \<in> S})"
+  [code del]: "at a = Abs_net ((\<lambda>S. S - {a}) ` {S. open S \<and> a \<in> S})"
 
 lemma Rep_net_sequentially:
   "Rep_net sequentially = range (\<lambda>n. {n..})"
@@ -136,13 +136,13 @@
 done
 
 lemma Rep_net_at:
-  "Rep_net (at a) = ((\<lambda>S. S - {a}) ` {S\<in>topo. a \<in> S})"
+  "Rep_net (at a) = ((\<lambda>S. S - {a}) ` {S. open S \<and> a \<in> S})"
 unfolding at_def
 apply (rule Abs_net_inverse')
 apply (rule image_nonempty)
-apply (rule_tac x="UNIV" in exI, simp add: topo_UNIV)
+apply (rule_tac x="UNIV" in exI, simp)
 apply (clarsimp, rename_tac S T)
-apply (rule_tac x="S \<inter> T" in exI, auto simp add: topo_Int)
+apply (rule_tac x="S \<inter> T" in exI, auto simp add: open_Int)
 done
 
 lemma eventually_sequentially:
@@ -154,16 +154,16 @@
 unfolding eventually_def Rep_net_within by auto
 
 lemma eventually_at_topological:
-  "eventually P (at a) \<longleftrightarrow> (\<exists>S\<in>topo. a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
+  "eventually P (at a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
 unfolding eventually_def Rep_net_at by auto
 
 lemma eventually_at:
   fixes a :: "'a::metric_space"
   shows "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
-unfolding eventually_at_topological topo_dist
+unfolding eventually_at_topological open_dist
 apply safe
 apply fast
-apply (rule_tac x="{x. dist x a < d}" in bexI, simp)
+apply (rule_tac x="{x. dist x a < d}" in exI, simp)
 apply clarsimp
 apply (rule_tac x="d - dist x a" in exI, clarsimp)
 apply (simp only: less_diff_eq)
@@ -356,22 +356,22 @@
   tendsto :: "('a \<Rightarrow> 'b::topological_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool"
     (infixr "--->" 55)
 where [code del]:
-  "(f ---> l) net \<longleftrightarrow> (\<forall>S\<in>topo. l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
+  "(f ---> l) net \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
 
 lemma topological_tendstoI:
-  "(\<And>S. S \<in> topo \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net)
+  "(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net)
     \<Longrightarrow> (f ---> l) net"
   unfolding tendsto_def by auto
 
 lemma topological_tendstoD:
-  "(f ---> l) net \<Longrightarrow> S \<in> topo \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net"
+  "(f ---> l) net \<Longrightarrow> open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net"
   unfolding tendsto_def by auto
 
 lemma tendstoI:
   assumes "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net"
   shows "(f ---> l) net"
 apply (rule topological_tendstoI)
-apply (simp add: topo_dist)
+apply (simp add: open_dist)
 apply (drule (1) bspec, clarify)
 apply (drule assms)
 apply (erule eventually_elim1, simp)
@@ -380,7 +380,7 @@
 lemma tendstoD:
   "(f ---> l) net \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net"
 apply (drule_tac S="{x. dist x l < e}" in topological_tendstoD)
-apply (clarsimp simp add: topo_dist)
+apply (clarsimp simp add: open_dist)
 apply (rule_tac x="e - dist x l" in exI, clarsimp)
 apply (simp only: less_diff_eq)
 apply (erule le_less_trans [OF dist_triangle])
diff -r f7310185481d -r 5400beeddb55 src/HOL/RealVector.thy
--- a/src/HOL/RealVector.thy	Sun Jun 07 15:18:52 2009 -0700
+++ b/src/HOL/RealVector.thy	Sun Jun 07 17:59:54 2009 -0700
@@ -418,39 +418,19 @@
 
 subsection {* Topological spaces *}
 
-class topo =
-  fixes topo :: "'a set set"
-
-text {*
-  The syntactic class uses @{term topo} instead of @{text "open"}
-  so that @{text "open"} and @{text closed} will have the same type.
-  Maybe we could use extra type constraints instead, like with
-  @{text dist} and @{text norm}?
-*}
+class "open" =
+  fixes "open" :: "'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"
+class topological_space = "open" +
+  assumes open_UNIV [simp, intro]: "open UNIV"
+  assumes open_Int [intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<inter> T)"
+  assumes open_Union [intro]: "\<forall>S\<in>K. open S \<Longrightarrow> open (\<Union> K)"
 begin
 
 definition
-  "open" :: "'a set \<Rightarrow> bool" where
-  "open S \<longleftrightarrow> S \<in> topo"
-
-definition
   closed :: "'a set \<Rightarrow> bool" where
   "closed S \<longleftrightarrow> open (- S)"
 
-lemma open_UNIV [intro, simp]:  "open UNIV"
-  unfolding open_def by (rule topo_UNIV)
-
-lemma open_Int [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)"
-  unfolding open_def subset_eq [symmetric] by (rule topo_Union)
-
 lemma open_empty [intro, simp]: "open {}"
   using open_Union [of "{}"] by simp
 
@@ -516,10 +496,10 @@
 class dist =
   fixes dist :: "'a \<Rightarrow> 'a \<Rightarrow> real"
 
-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 open_dist = "open" + dist +
+  assumes open_dist: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
 
-class metric_space = topo_dist +
+class metric_space = open_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
@@ -554,20 +534,20 @@
 proof
   have "\<exists>e::real. 0 < e"
     by (fast intro: zero_less_one)
-  then show "UNIV \<in> topo"
-    unfolding topo_dist by simp
+  then show "open UNIV"
+    unfolding open_dist by simp
 next
-  fix A B assume "A \<in> topo" "B \<in> topo"
-  then show "A \<inter> B \<in> topo"
-    unfolding topo_dist
+  fix S T assume "open S" "open T"
+  then show "open (S \<inter> T)"
+    unfolding open_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
+  fix K assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
+    unfolding open_dist by fast
 qed
 
 end
@@ -584,7 +564,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 + topo_dist +
+class real_normed_vector = real_vector + sgn_div_norm + dist_norm + open_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"
@@ -621,14 +601,14 @@
 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}"
+definition open_real_def [code del]:
+  "open (S :: real set) \<longleftrightarrow> (\<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 (rule open_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)
@@ -819,6 +799,11 @@
 
 subsection {* Extra type constraints *}
 
+text {* Only allow @{term "open"} in class @{text topological_space}. *}
+
+setup {* Sign.add_const_constraint
+  (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"}) *}
+
 text {* Only allow @{term dist} in class @{text metric_space}. *}
 
 setup {* Sign.add_const_constraint