# HG changeset patch
# User huffman
# Date 1244040296 25200
# Node ID 729d90a531e4b6e67e995c253886eeadc2348829
# Parent  9f2ca03ae7b7425c27ae7586c085861c20c95c7e
introduce class topological_space as a superclass of metric_space

diff -r 9f2ca03ae7b7 -r 729d90a531e4 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Wed Jun 03 07:12:57 2009 -0700
+++ b/src/HOL/Complex.thy	Wed Jun 03 07:44:56 2009 -0700
@@ -268,27 +268,29 @@
 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 open_complex_def:
+  "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y::complex. 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
-  fix r :: real and x y :: complex
+instance proof
+  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)"
@@ -306,6 +308,8 @@
     by (rule complex_sgn_def)
   show "dist x y = cmod (x - y)"
     by (rule dist_complex_def)
+  show "open S = (\<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 9f2ca03ae7b7 -r 729d90a531e4 src/HOL/RealVector.thy
--- a/src/HOL/RealVector.thy	Wed Jun 03 07:12:57 2009 -0700
+++ b/src/HOL/RealVector.thy	Wed Jun 03 07:44:56 2009 -0700
@@ -416,12 +416,26 @@
   by (rule Reals_cases) auto
 
 
+subsection {* Topological spaces *}
+
+class "open" =
+  fixes "open" :: "'a set \<Rightarrow> bool"
+
+class topological_space = "open" +
+  assumes open_UNIV: "open UNIV"
+  assumes open_Int: "open A \<Longrightarrow> open B \<Longrightarrow> open (A \<inter> B)"
+  assumes open_Union: "\<forall>A\<in>T. open A \<Longrightarrow> open (\<Union>T)"
+
+
 subsection {* Metric spaces *}
 
 class dist =
   fixes dist :: "'a \<Rightarrow> 'a \<Rightarrow> real"
 
-class metric_space = dist +
+class open_dist = "open" + dist +
+  assumes open_dist: "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+
+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
@@ -452,6 +466,27 @@
 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 "open UNIV"
+    unfolding open_dist by simp
+next
+  fix A B assume "open A" "open B"
+  then show "open (A \<inter> B)"
+    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 "\<forall>A\<in>T. open A"
+  then show "open (\<Union>T)"
+    unfolding open_dist by fast
+qed
+
 end
 
 
@@ -466,7 +501,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 + 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"
@@ -497,15 +532,19 @@
 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 open_real_def:
+  "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y::real. 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 abs_ge_zero)
 apply (rule abs_eq_0)