replace class open with class topo
authorhuffman
Wed Jun 03 09:58:11 2009 -0700 (2009-06-03)
changeset 31417c12b25b7f015
parent 31416 f4c079225845
child 31418 9baa48bad81c
replace class open with class topo
src/HOL/Complex.thy
src/HOL/Library/Euclidean_Space.thy
src/HOL/Library/Inner_Product.thy
src/HOL/Library/Product_Vector.thy
src/HOL/RealVector.thy
     1.1 --- a/src/HOL/Complex.thy	Wed Jun 03 08:46:13 2009 -0700
     1.2 +++ b/src/HOL/Complex.thy	Wed Jun 03 09:58:11 2009 -0700
     1.3 @@ -281,8 +281,8 @@
     1.4  definition dist_complex_def:
     1.5    "dist x y = cmod (x - y)"
     1.6  
     1.7 -definition open_complex_def:
     1.8 -  "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y::complex. dist y x < e \<longrightarrow> y \<in> S)"
     1.9 +definition topo_complex_def:
    1.10 +  "topo = {S::complex set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
    1.11  
    1.12  lemmas cmod_def = complex_norm_def
    1.13  
    1.14 @@ -290,7 +290,7 @@
    1.15    by (simp add: complex_norm_def)
    1.16  
    1.17  instance proof
    1.18 -  fix r :: real and x y :: complex and S :: "complex set"
    1.19 +  fix r :: real and x y :: complex
    1.20    show "0 \<le> norm x"
    1.21      by (induct x) simp
    1.22    show "(norm x = 0) = (x = 0)"
    1.23 @@ -308,8 +308,8 @@
    1.24      by (rule complex_sgn_def)
    1.25    show "dist x y = cmod (x - y)"
    1.26      by (rule dist_complex_def)
    1.27 -  show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    1.28 -    by (rule open_complex_def)
    1.29 +  show "topo = {S::complex set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
    1.30 +    by (rule topo_complex_def)
    1.31  qed
    1.32  
    1.33  end
     2.1 --- a/src/HOL/Library/Euclidean_Space.thy	Wed Jun 03 08:46:13 2009 -0700
     2.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Wed Jun 03 09:58:11 2009 -0700
     2.3 @@ -506,8 +506,8 @@
     2.4  definition dist_vector_def:
     2.5    "dist (x::'a^'b) (y::'a^'b) = setL2 (\<lambda>i. dist (x$i) (y$i)) UNIV"
     2.6  
     2.7 -definition open_vector_def:
     2.8 -  "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y::'a ^ 'b. dist y x < e \<longrightarrow> y \<in> S)"
     2.9 +definition topo_vector_def:
    2.10 +  "topo = {S::('a ^ 'b) set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
    2.11  
    2.12  instance proof
    2.13    fix x y :: "'a ^ 'b"
    2.14 @@ -522,9 +522,8 @@
    2.15      apply (simp add: setL2_mono dist_triangle2)
    2.16      done
    2.17  next
    2.18 -  fix S :: "('a ^ 'b) set"
    2.19 -  show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    2.20 -    by (rule open_vector_def)
    2.21 +  show "topo = {S::('a ^ 'b) set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
    2.22 +    by (rule topo_vector_def)
    2.23  qed
    2.24  
    2.25  end
     3.1 --- a/src/HOL/Library/Inner_Product.thy	Wed Jun 03 08:46:13 2009 -0700
     3.2 +++ b/src/HOL/Library/Inner_Product.thy	Wed Jun 03 09:58:11 2009 -0700
     3.3 @@ -10,7 +10,7 @@
     3.4  
     3.5  subsection {* Real inner product spaces *}
     3.6  
     3.7 -class real_inner = real_vector + sgn_div_norm + dist_norm + open_dist +
     3.8 +class real_inner = real_vector + sgn_div_norm + dist_norm + topo_dist +
     3.9    fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
    3.10    assumes inner_commute: "inner x y = inner y x"
    3.11    and inner_left_distrib: "inner (x + y) z = inner x z + inner y z"
     4.1 --- a/src/HOL/Library/Product_Vector.thy	Wed Jun 03 08:46:13 2009 -0700
     4.2 +++ b/src/HOL/Library/Product_Vector.thy	Wed Jun 03 09:58:11 2009 -0700
     4.3 @@ -45,28 +45,29 @@
     4.4    "*" :: (topological_space, topological_space) topological_space
     4.5  begin
     4.6  
     4.7 -definition open_prod_def:
     4.8 -  "open S = (\<forall>x\<in>S. \<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S)"
     4.9 +definition topo_prod_def:
    4.10 +  "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}"
    4.11  
    4.12  instance proof
    4.13 -  show "open (UNIV :: ('a \<times> 'b) set)"
    4.14 -    unfolding open_prod_def by (fast intro: open_UNIV)
    4.15 +  show "(UNIV :: ('a \<times> 'b) set) \<in> topo"
    4.16 +    unfolding topo_prod_def by (auto intro: topo_UNIV)
    4.17  next
    4.18    fix S T :: "('a \<times> 'b) set"
    4.19 -  assume "open S" "open T" thus "open (S \<inter> T)"
    4.20 -    unfolding open_prod_def
    4.21 +  assume "S \<in> topo" "T \<in> topo" thus "S \<inter> T \<in> topo"
    4.22 +    unfolding topo_prod_def
    4.23      apply clarify
    4.24      apply (drule (1) bspec)+
    4.25      apply (clarify, rename_tac Sa Ta Sb Tb)
    4.26 -    apply (rule_tac x="Sa \<inter> Ta" in exI)
    4.27 -    apply (rule_tac x="Sb \<inter> Tb" in exI)
    4.28 -    apply (simp add: open_Int)
    4.29 +    apply (rule_tac x="Sa \<inter> Ta" in rev_bexI)
    4.30 +    apply (simp add: topo_Int)
    4.31 +    apply (rule_tac x="Sb \<inter> Tb" in rev_bexI)
    4.32 +    apply (simp add: topo_Int)
    4.33      apply fast
    4.34      done
    4.35  next
    4.36    fix T :: "('a \<times> 'b) set set"
    4.37 -  assume "\<forall>A\<in>T. open A" thus "open (\<Union>T)"
    4.38 -    unfolding open_prod_def by fast
    4.39 +  assume "T \<subseteq> topo" thus "\<Union>T \<in> topo"
    4.40 +    unfolding topo_prod_def Bex_def by fast
    4.41  qed
    4.42  
    4.43  end
    4.44 @@ -103,10 +104,9 @@
    4.45    (* FIXME: long proof! *)
    4.46    (* Maybe it would be easier to define topological spaces *)
    4.47    (* in terms of neighborhoods instead of open sets? *)
    4.48 -  fix S :: "('a \<times> 'b) set"
    4.49 -  show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    4.50 -    unfolding open_prod_def open_dist
    4.51 -    apply safe
    4.52 +  show "topo = {S::('a \<times> 'b) set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
    4.53 +    unfolding topo_prod_def topo_dist
    4.54 +    apply (safe, rename_tac S a b)
    4.55      apply (drule (1) bspec)
    4.56      apply clarify
    4.57      apply (drule (1) bspec)+
    4.58 @@ -121,19 +121,18 @@
    4.59      apply (drule spec, erule mp)
    4.60      apply (erule le_less_trans [OF real_sqrt_sum_squares_ge2])
    4.61  
    4.62 +    apply (rename_tac S a b)
    4.63      apply (drule (1) bspec)
    4.64      apply clarify
    4.65      apply (subgoal_tac "\<exists>r>0. \<exists>s>0. e = sqrt (r\<twosuperior> + s\<twosuperior>)")
    4.66      apply clarify
    4.67 -    apply (rule_tac x="{y. dist y a < r}" in exI)
    4.68 -    apply (rule_tac x="{y. dist y b < s}" in exI)
    4.69 -    apply (rule conjI)
    4.70 +    apply (rule_tac x="{y. dist y a < r}" in rev_bexI)
    4.71      apply clarify
    4.72      apply (rule_tac x="r - dist x a" in exI, rule conjI, simp)
    4.73      apply clarify
    4.74      apply (rule le_less_trans [OF dist_triangle])
    4.75      apply (erule less_le_trans [OF add_strict_right_mono], simp)
    4.76 -    apply (rule conjI)
    4.77 +    apply (rule_tac x="{y. dist y b < s}" in rev_bexI)
    4.78      apply clarify
    4.79      apply (rule_tac x="s - dist x b" in exI, rule conjI, simp)
    4.80      apply clarify
     5.1 --- a/src/HOL/RealVector.thy	Wed Jun 03 08:46:13 2009 -0700
     5.2 +++ b/src/HOL/RealVector.thy	Wed Jun 03 09:58:11 2009 -0700
     5.3 @@ -418,13 +418,13 @@
     5.4  
     5.5  subsection {* Topological spaces *}
     5.6  
     5.7 -class "open" =
     5.8 -  fixes "open" :: "'a set \<Rightarrow> bool"
     5.9 +class topo =
    5.10 +  fixes topo :: "'a set set"
    5.11  
    5.12 -class topological_space = "open" +
    5.13 -  assumes open_UNIV: "open UNIV"
    5.14 -  assumes open_Int: "open A \<Longrightarrow> open B \<Longrightarrow> open (A \<inter> B)"
    5.15 -  assumes open_Union: "\<forall>A\<in>T. open A \<Longrightarrow> open (\<Union>T)"
    5.16 +class topological_space = topo +
    5.17 +  assumes topo_UNIV: "UNIV \<in> topo"
    5.18 +  assumes topo_Int: "A \<in> topo \<Longrightarrow> B \<in> topo \<Longrightarrow> A \<inter> B \<in> topo"
    5.19 +  assumes topo_Union: "T \<subseteq> topo \<Longrightarrow> \<Union>T \<in> topo"
    5.20  
    5.21  
    5.22  subsection {* Metric spaces *}
    5.23 @@ -432,10 +432,10 @@
    5.24  class dist =
    5.25    fixes dist :: "'a \<Rightarrow> 'a \<Rightarrow> real"
    5.26  
    5.27 -class open_dist = "open" + dist +
    5.28 -  assumes open_dist: "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    5.29 +class topo_dist = topo + dist +
    5.30 +  assumes topo_dist: "topo = {S. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
    5.31  
    5.32 -class metric_space = open_dist +
    5.33 +class metric_space = topo_dist +
    5.34    assumes dist_eq_0_iff [simp]: "dist x y = 0 \<longleftrightarrow> x = y"
    5.35    assumes dist_triangle2: "dist x y \<le> dist x z + dist y z"
    5.36  begin
    5.37 @@ -470,21 +470,20 @@
    5.38  proof
    5.39    have "\<exists>e::real. 0 < e"
    5.40      by (fast intro: zero_less_one)
    5.41 -  then show "open UNIV"
    5.42 -    unfolding open_dist by simp
    5.43 +  then show "UNIV \<in> topo"
    5.44 +    unfolding topo_dist by simp
    5.45  next
    5.46 -  fix A B assume "open A" "open B"
    5.47 -  then show "open (A \<inter> B)"
    5.48 -    unfolding open_dist
    5.49 +  fix A B assume "A \<in> topo" "B \<in> topo"
    5.50 +  then show "A \<inter> B \<in> topo"
    5.51 +    unfolding topo_dist
    5.52      apply clarify
    5.53      apply (drule (1) bspec)+
    5.54      apply (clarify, rename_tac r s)
    5.55      apply (rule_tac x="min r s" in exI, simp)
    5.56      done
    5.57  next
    5.58 -  fix T assume "\<forall>A\<in>T. open A"
    5.59 -  then show "open (\<Union>T)"
    5.60 -    unfolding open_dist by fast
    5.61 +  fix T assume "T \<subseteq> topo" thus "\<Union>T \<in> topo"
    5.62 +    unfolding topo_dist by fast
    5.63  qed
    5.64  
    5.65  end
    5.66 @@ -501,7 +500,7 @@
    5.67  class dist_norm = dist + norm + minus +
    5.68    assumes dist_norm: "dist x y = norm (x - y)"
    5.69  
    5.70 -class real_normed_vector = real_vector + sgn_div_norm + dist_norm + open_dist +
    5.71 +class real_normed_vector = real_vector + sgn_div_norm + dist_norm + topo_dist +
    5.72    assumes norm_ge_zero [simp]: "0 \<le> norm x"
    5.73    and norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = 0"
    5.74    and norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y"
    5.75 @@ -538,14 +537,14 @@
    5.76  definition dist_real_def:
    5.77    "dist x y = \<bar>x - y\<bar>"
    5.78  
    5.79 -definition open_real_def:
    5.80 -  "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y::real. dist y x < e \<longrightarrow> y \<in> S)"
    5.81 +definition topo_real_def:
    5.82 +  "topo = {S::real set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
    5.83  
    5.84  instance
    5.85  apply (intro_classes, unfold real_norm_def real_scaleR_def)
    5.86  apply (rule dist_real_def)
    5.87 -apply (rule open_real_def)
    5.88  apply (simp add: real_sgn_def)
    5.89 +apply (rule topo_real_def)
    5.90  apply (rule abs_ge_zero)
    5.91  apply (rule abs_eq_0)
    5.92  apply (rule abs_triangle_ineq)