--- a/src/HOL/Complex.thy Wed Jun 03 08:46:13 2009 -0700
+++ b/src/HOL/Complex.thy Wed Jun 03 09:58:11 2009 -0700
@@ -281,8 +281,8 @@
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)"
+definition topo_complex_def:
+ "topo = {S::complex set. \<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 and S :: "complex set"
+ fix r :: real and x y :: complex
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 "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
- by (rule open_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)
qed
end
--- a/src/HOL/Library/Euclidean_Space.thy Wed Jun 03 08:46:13 2009 -0700
+++ b/src/HOL/Library/Euclidean_Space.thy Wed Jun 03 09:58:11 2009 -0700
@@ -506,8 +506,8 @@
definition dist_vector_def:
"dist (x::'a^'b) (y::'a^'b) = setL2 (\<lambda>i. dist (x$i) (y$i)) UNIV"
-definition open_vector_def:
- "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y::'a ^ 'b. dist y x < e \<longrightarrow> y \<in> S)"
+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}"
instance proof
fix x y :: "'a ^ 'b"
@@ -522,9 +522,8 @@
apply (simp add: setL2_mono dist_triangle2)
done
next
- fix S :: "('a ^ 'b) set"
- show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
- by (rule open_vector_def)
+ 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)
qed
end
--- a/src/HOL/Library/Inner_Product.thy Wed Jun 03 08:46:13 2009 -0700
+++ b/src/HOL/Library/Inner_Product.thy Wed Jun 03 09:58:11 2009 -0700
@@ -10,7 +10,7 @@
subsection {* Real inner product spaces *}
-class real_inner = real_vector + sgn_div_norm + dist_norm + open_dist +
+class real_inner = real_vector + sgn_div_norm + dist_norm + topo_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"
--- a/src/HOL/Library/Product_Vector.thy Wed Jun 03 08:46:13 2009 -0700
+++ b/src/HOL/Library/Product_Vector.thy Wed Jun 03 09:58:11 2009 -0700
@@ -45,28 +45,29 @@
"*" :: (topological_space, topological_space) topological_space
begin
-definition open_prod_def:
- "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)"
+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}"
instance proof
- show "open (UNIV :: ('a \<times> 'b) set)"
- unfolding open_prod_def by (fast intro: open_UNIV)
+ show "(UNIV :: ('a \<times> 'b) set) \<in> topo"
+ unfolding topo_prod_def by (auto intro: topo_UNIV)
next
fix S T :: "('a \<times> 'b) set"
- assume "open S" "open T" thus "open (S \<inter> T)"
- unfolding open_prod_def
+ assume "S \<in> topo" "T \<in> topo" thus "S \<inter> T \<in> topo"
+ unfolding topo_prod_def
apply clarify
apply (drule (1) bspec)+
apply (clarify, rename_tac Sa Ta Sb Tb)
- apply (rule_tac x="Sa \<inter> Ta" in exI)
- apply (rule_tac x="Sb \<inter> Tb" in exI)
- apply (simp add: open_Int)
+ 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 fast
done
next
fix T :: "('a \<times> 'b) set set"
- assume "\<forall>A\<in>T. open A" thus "open (\<Union>T)"
- unfolding open_prod_def by fast
+ assume "T \<subseteq> topo" thus "\<Union>T \<in> topo"
+ unfolding topo_prod_def Bex_def by fast
qed
end
@@ -103,10 +104,9 @@
(* FIXME: long proof! *)
(* Maybe it would be easier to define topological spaces *)
(* in terms of neighborhoods instead of open sets? *)
- fix S :: "('a \<times> 'b) set"
- show "open S = (\<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
+ 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)
apply (drule (1) bspec)
apply clarify
apply (drule (1) bspec)+
@@ -121,19 +121,18 @@
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 exI)
- apply (rule_tac x="{y. dist y b < s}" in exI)
- apply (rule conjI)
+ apply (rule_tac x="{y. dist y a < r}" in rev_bexI)
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 conjI)
+ apply (rule_tac x="{y. dist y b < s}" in rev_bexI)
apply clarify
apply (rule_tac x="s - dist x b" in exI, rule conjI, simp)
apply clarify
--- a/src/HOL/RealVector.thy Wed Jun 03 08:46:13 2009 -0700
+++ b/src/HOL/RealVector.thy Wed Jun 03 09:58:11 2009 -0700
@@ -418,13 +418,13 @@
subsection {* Topological spaces *}
-class "open" =
- fixes "open" :: "'a set \<Rightarrow> bool"
+class topo =
+ fixes topo :: "'a set set"
-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)"
+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"
subsection {* Metric spaces *}
@@ -432,10 +432,10 @@
class dist =
fixes dist :: "'a \<Rightarrow> 'a \<Rightarrow> real"
-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 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 metric_space = open_dist +
+class metric_space = topo_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
@@ -470,21 +470,20 @@
proof
have "\<exists>e::real. 0 < e"
by (fast intro: zero_less_one)
- then show "open UNIV"
- unfolding open_dist by simp
+ then show "UNIV \<in> topo"
+ unfolding topo_dist by simp
next
- fix A B assume "open A" "open B"
- then show "open (A \<inter> B)"
- unfolding open_dist
+ fix A B assume "A \<in> topo" "B \<in> topo"
+ then show "A \<inter> B \<in> topo"
+ unfolding topo_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
+ fix T assume "T \<subseteq> topo" thus "\<Union>T \<in> topo"
+ unfolding topo_dist by fast
qed
end
@@ -501,7 +500,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 + open_dist +
+class real_normed_vector = real_vector + sgn_div_norm + dist_norm + topo_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"
@@ -538,14 +537,14 @@
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)"
+definition topo_real_def:
+ "topo = {S::real set. \<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)