introduce class topological_space as a superclass of metric_space
authorhuffman
Wed Jun 03 07:44:56 2009 -0700 (2009-06-03)
changeset 31413729d90a531e4
parent 31408 9f2ca03ae7b7
child 31414 8514775606e0
introduce class topological_space as a superclass of metric_space
src/HOL/Complex.thy
src/HOL/RealVector.thy
     1.1 --- a/src/HOL/Complex.thy	Wed Jun 03 07:12:57 2009 -0700
     1.2 +++ b/src/HOL/Complex.thy	Wed Jun 03 07:44:56 2009 -0700
     1.3 @@ -268,27 +268,29 @@
     1.4  instantiation complex :: real_normed_field
     1.5  begin
     1.6  
     1.7 -definition
     1.8 -  complex_norm_def: "norm z = sqrt ((Re z)\<twosuperior> + (Im z)\<twosuperior>)"
     1.9 +definition complex_norm_def:
    1.10 +  "norm z = sqrt ((Re z)\<twosuperior> + (Im z)\<twosuperior>)"
    1.11  
    1.12  abbreviation
    1.13    cmod :: "complex \<Rightarrow> real" where
    1.14    "cmod \<equiv> norm"
    1.15  
    1.16 -definition
    1.17 -  complex_sgn_def: "sgn x = x /\<^sub>R cmod x"
    1.18 +definition complex_sgn_def:
    1.19 +  "sgn x = x /\<^sub>R cmod x"
    1.20  
    1.21 -definition
    1.22 -  dist_complex_def: "dist x y = cmod (x - y)"
    1.23 +definition dist_complex_def:
    1.24 +  "dist x y = cmod (x - y)"
    1.25 +
    1.26 +definition open_complex_def:
    1.27 +  "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y::complex. dist y x < e \<longrightarrow> y \<in> S)"
    1.28  
    1.29  lemmas cmod_def = complex_norm_def
    1.30  
    1.31  lemma complex_norm [simp]: "cmod (Complex x y) = sqrt (x\<twosuperior> + y\<twosuperior>)"
    1.32    by (simp add: complex_norm_def)
    1.33  
    1.34 -instance
    1.35 -proof
    1.36 -  fix r :: real and x y :: complex
    1.37 +instance proof
    1.38 +  fix r :: real and x y :: complex and S :: "complex set"
    1.39    show "0 \<le> norm x"
    1.40      by (induct x) simp
    1.41    show "(norm x = 0) = (x = 0)"
    1.42 @@ -306,6 +308,8 @@
    1.43      by (rule complex_sgn_def)
    1.44    show "dist x y = cmod (x - y)"
    1.45      by (rule dist_complex_def)
    1.46 +  show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    1.47 +    by (rule open_complex_def)
    1.48  qed
    1.49  
    1.50  end
     2.1 --- a/src/HOL/RealVector.thy	Wed Jun 03 07:12:57 2009 -0700
     2.2 +++ b/src/HOL/RealVector.thy	Wed Jun 03 07:44:56 2009 -0700
     2.3 @@ -416,12 +416,26 @@
     2.4    by (rule Reals_cases) auto
     2.5  
     2.6  
     2.7 +subsection {* Topological spaces *}
     2.8 +
     2.9 +class "open" =
    2.10 +  fixes "open" :: "'a set \<Rightarrow> bool"
    2.11 +
    2.12 +class topological_space = "open" +
    2.13 +  assumes open_UNIV: "open UNIV"
    2.14 +  assumes open_Int: "open A \<Longrightarrow> open B \<Longrightarrow> open (A \<inter> B)"
    2.15 +  assumes open_Union: "\<forall>A\<in>T. open A \<Longrightarrow> open (\<Union>T)"
    2.16 +
    2.17 +
    2.18  subsection {* Metric spaces *}
    2.19  
    2.20  class dist =
    2.21    fixes dist :: "'a \<Rightarrow> 'a \<Rightarrow> real"
    2.22  
    2.23 -class metric_space = dist +
    2.24 +class open_dist = "open" + dist +
    2.25 +  assumes open_dist: "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    2.26 +
    2.27 +class metric_space = open_dist +
    2.28    assumes dist_eq_0_iff [simp]: "dist x y = 0 \<longleftrightarrow> x = y"
    2.29    assumes dist_triangle2: "dist x y \<le> dist x z + dist y z"
    2.30  begin
    2.31 @@ -452,6 +466,27 @@
    2.32  lemma dist_triangle: "dist x z \<le> dist x y + dist y z"
    2.33  using dist_triangle2 [of x z y] by (simp add: dist_commute)
    2.34  
    2.35 +subclass topological_space
    2.36 +proof
    2.37 +  have "\<exists>e::real. 0 < e"
    2.38 +    by (fast intro: zero_less_one)
    2.39 +  then show "open UNIV"
    2.40 +    unfolding open_dist by simp
    2.41 +next
    2.42 +  fix A B assume "open A" "open B"
    2.43 +  then show "open (A \<inter> B)"
    2.44 +    unfolding open_dist
    2.45 +    apply clarify
    2.46 +    apply (drule (1) bspec)+
    2.47 +    apply (clarify, rename_tac r s)
    2.48 +    apply (rule_tac x="min r s" in exI, simp)
    2.49 +    done
    2.50 +next
    2.51 +  fix T assume "\<forall>A\<in>T. open A"
    2.52 +  then show "open (\<Union>T)"
    2.53 +    unfolding open_dist by fast
    2.54 +qed
    2.55 +
    2.56  end
    2.57  
    2.58  
    2.59 @@ -466,7 +501,7 @@
    2.60  class dist_norm = dist + norm + minus +
    2.61    assumes dist_norm: "dist x y = norm (x - y)"
    2.62  
    2.63 -class real_normed_vector = real_vector + sgn_div_norm + dist_norm +
    2.64 +class real_normed_vector = real_vector + sgn_div_norm + dist_norm + open_dist +
    2.65    assumes norm_ge_zero [simp]: "0 \<le> norm x"
    2.66    and norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = 0"
    2.67    and norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y"
    2.68 @@ -497,15 +532,19 @@
    2.69  instantiation real :: real_normed_field
    2.70  begin
    2.71  
    2.72 -definition
    2.73 -  real_norm_def [simp]: "norm r = \<bar>r\<bar>"
    2.74 +definition real_norm_def [simp]:
    2.75 +  "norm r = \<bar>r\<bar>"
    2.76  
    2.77 -definition
    2.78 -  dist_real_def: "dist x y = \<bar>x - y\<bar>"
    2.79 +definition dist_real_def:
    2.80 +  "dist x y = \<bar>x - y\<bar>"
    2.81 +
    2.82 +definition open_real_def:
    2.83 +  "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y::real. dist y x < e \<longrightarrow> y \<in> S)"
    2.84  
    2.85  instance
    2.86  apply (intro_classes, unfold real_norm_def real_scaleR_def)
    2.87  apply (rule dist_real_def)
    2.88 +apply (rule open_real_def)
    2.89  apply (simp add: real_sgn_def)
    2.90  apply (rule abs_ge_zero)
    2.91  apply (rule abs_eq_0)