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