--- a/src/HOL/Complex.thy Wed Jun 03 15:48:54 2009 +0200
+++ b/src/HOL/Complex.thy Wed Jun 03 12:24:09 2009 -0700
@@ -268,26 +268,28 @@
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 topo_complex_def [code del]:
+ "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
lemma complex_norm [simp]: "cmod (Complex x y) = sqrt (x\<twosuperior> + y\<twosuperior>)"
by (simp add: complex_norm_def)
-instance
-proof
+instance proof
fix r :: real and x y :: complex
show "0 \<le> norm x"
by (induct x) simp
@@ -306,6 +308,8 @@
by (rule complex_sgn_def)
show "dist x y = cmod (x - y)"
by (rule dist_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/Convex_Euclidean_Space.thy Wed Jun 03 15:48:54 2009 +0200
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy Wed Jun 03 12:24:09 2009 -0700
@@ -602,8 +602,8 @@
have "\<exists>x\<ge>0. x \<le> 1 \<and> (1 - x) *s x1 + x *s x2 \<notin> e1 \<and> (1 - x) *s x1 + x *s x2 \<notin> e2"
apply(rule connected_real_lemma) apply (simp add: `x1\<in>e1` `x2\<in>e2` dist_commute)+
using * apply(simp add: dist_norm)
- using as(1,2)[unfolded open_def] apply simp
- using as(1,2)[unfolded open_def] apply simp
+ using as(1,2)[unfolded open_dist] apply simp
+ using as(1,2)[unfolded open_dist] apply simp
using assms[unfolded convex_alt, THEN bspec[where x=x1], THEN bspec[where x=x2]] using x1 x2
using as(3) by auto
then obtain x where "x\<ge>0" "x\<le>1" "(1 - x) *s x1 + x *s x2 \<notin> e1" "(1 - x) *s x1 + x *s x2 \<notin> e2" by auto
--- a/src/HOL/Library/Euclidean_Space.thy Wed Jun 03 15:48:54 2009 +0200
+++ b/src/HOL/Library/Euclidean_Space.thy Wed Jun 03 12:24:09 2009 -0700
@@ -506,6 +506,9 @@
definition dist_vector_def:
"dist (x::'a^'b) (y::'a^'b) = setL2 (\<lambda>i. dist (x$i) (y$i)) UNIV"
+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"
show "dist x y = 0 \<longleftrightarrow> x = y"
@@ -518,6 +521,9 @@
apply (rule order_trans [OF _ setL2_triangle_ineq])
apply (simp add: setL2_mono dist_triangle2)
done
+next
+ 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 15:48:54 2009 +0200
+++ b/src/HOL/Library/Inner_Product.thy Wed Jun 03 12:24:09 2009 -0700
@@ -10,7 +10,7 @@
subsection {* Real inner product spaces *}
-class real_inner = real_vector + sgn_div_norm + dist_norm +
+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 15:48:54 2009 +0200
+++ b/src/HOL/Library/Product_Vector.thy Wed Jun 03 12:24:09 2009 -0700
@@ -39,6 +39,39 @@
end
+subsection {* Product is a topological space *}
+
+instantiation
+ "*" :: (topological_space, topological_space) topological_space
+begin
+
+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 "(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 "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 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 "T \<subseteq> topo" thus "\<Union>T \<in> topo"
+ unfolding topo_prod_def Bex_def by fast
+qed
+
+end
+
subsection {* Product is a metric space *}
instantiation
@@ -67,6 +100,53 @@
apply (rule power_mono [OF dist_triangle2 [of _ _ "snd z"] zero_le_dist])
apply (simp only: real_sum_squared_expand)
done
+next
+ (* FIXME: long proof! *)
+ (* Maybe it would be easier to define topological spaces *)
+ (* in terms of neighborhoods instead of open sets? *)
+ 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)+
+ apply (clarify, rename_tac r s)
+ apply (rule_tac x="min r s" in exI, simp)
+ apply (clarify, rename_tac c d)
+ apply (erule subsetD)
+ apply (simp add: dist_Pair_Pair)
+ apply (rule conjI)
+ apply (drule spec, erule mp)
+ apply (erule le_less_trans [OF real_sqrt_sum_squares_ge1])
+ 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 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_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
+ apply (rule le_less_trans [OF dist_triangle])
+ apply (erule less_le_trans [OF add_strict_right_mono], simp)
+ apply (rule conjI)
+ apply simp
+ apply (clarify, rename_tac c d)
+ apply (drule spec, erule mp)
+ apply (simp add: dist_Pair_Pair add_strict_mono power_strict_mono)
+ apply (rule_tac x="e / sqrt 2" in exI, simp add: divide_pos_pos)
+ apply (rule_tac x="e / sqrt 2" in exI, simp add: divide_pos_pos)
+ apply (simp add: power_divide)
+ done
qed
end
--- a/src/HOL/Library/Topology_Euclidean_Space.thy Wed Jun 03 15:48:54 2009 +0200
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy Wed Jun 03 12:24:09 2009 -0700
@@ -194,35 +194,30 @@
by (simp add: subtopology_superset)
subsection{* The universal Euclidean versions are what we use most of the time *}
+
definition
- "open" :: "'a::metric_space set \<Rightarrow> bool" where
- "open S \<longleftrightarrow> (\<forall>x \<in> S. \<exists>e >0. \<forall>x'. dist x' x < e \<longrightarrow> x' \<in> S)"
-definition "closed S \<longleftrightarrow> open(UNIV - S)"
-definition "euclidean = topology open"
-
-lemma open_empty[intro,simp]: "open {}" by (simp add: open_def)
+ "open" :: "'a::topological_space set \<Rightarrow> bool" where
+ "open S \<longleftrightarrow> S \<in> topo"
+
+definition
+ closed :: "'a::topological_space set \<Rightarrow> bool" where
+ "closed S \<longleftrightarrow> open(UNIV - S)"
+
+definition
+ euclidean :: "'a::topological_space topology" where
+ "euclidean = topology open"
+
lemma open_UNIV[intro,simp]: "open UNIV"
- by (simp add: open_def, rule exI[where x="1"], auto)
-
-lemma open_inter[intro]: assumes S: "open S" and T: "open T"
- shows "open (S \<inter> T)"
-proof-
- note thS = S[unfolded open_def, rule_format]
- note thT = T[unfolded open_def, rule_format]
- {fix x assume x: "x \<in> S\<inter>T"
- hence xS: "x \<in> S" and xT: "x \<in> T" by simp_all
- from thS[OF xS] obtain eS where eS: "eS > 0" "\<forall>x'. dist x' x < eS \<longrightarrow> x' \<in> S" by blast
- from thT[OF xT] obtain eT where eT: "eT > 0" "\<forall>x'. dist x' x < eT \<longrightarrow> x' \<in> T" by blast
- from real_lbound_gt_zero[OF eS(1) eT(1)] obtain e where e: "e > 0" "e < eS" "e < eT" by blast
- { fix x' assume d: "dist x' x < e"
- hence dS: "dist x' x < eS" and dT: "dist x' x < eT" using e by arith+
- from eS(2)[rule_format, OF dS] eT(2)[rule_format, OF dT] have "x' \<in> S\<inter>T" by blast}
- hence "\<exists>e >0. \<forall>x'. dist x' x < e \<longrightarrow> x' \<in> (S\<inter>T)" using e by blast}
- then show ?thesis unfolding open_def by blast
-qed
+ unfolding open_def by (rule topo_UNIV)
+
+lemma open_inter[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)"
- by (simp add: open_def) metis
+ unfolding open_def subset_eq [symmetric] by (rule topo_Union)
+
+lemma open_empty[intro,simp]: "open {}"
+ using open_Union [of "{}"] by simp
lemma open_openin: "open S \<longleftrightarrow> openin euclidean S"
unfolding euclidean_def
@@ -242,7 +237,9 @@
lemma closed_closedin: "closed S \<longleftrightarrow> closedin euclidean S"
by (simp add: closed_def closedin_def topspace_euclidean open_openin)
-lemma open_Un[intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S\<union>T)"
+lemma open_Un[intro]:
+ fixes S T :: "'a::topological_space set"
+ shows "open S \<Longrightarrow> open T \<Longrightarrow> open (S\<union>T)"
by (auto simp add: open_openin)
lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)"
@@ -320,6 +317,11 @@
subsection{* Topological properties of open balls *}
+lemma open_dist:
+ fixes S :: "'a::metric_space set"
+ shows "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>x'. dist x' x < e \<longrightarrow> x' \<in> S)"
+ unfolding open_def topo_dist by simp
+
lemma diff_less_iff: "(a::real) - b > 0 \<longleftrightarrow> a > b"
"(a::real) - b < 0 \<longleftrightarrow> a < b"
"a - b < c \<longleftrightarrow> a < c +b" "a - b > c \<longleftrightarrow> a > c +b" by arith+
@@ -327,7 +329,7 @@
"a - b \<le> c \<longleftrightarrow> a \<le> c +b" "a - b \<ge> c \<longleftrightarrow> a \<ge> c +b" by arith+
lemma open_ball[intro, simp]: "open (ball x e)"
- unfolding open_def ball_def Collect_def Ball_def mem_def
+ unfolding open_dist ball_def Collect_def Ball_def mem_def
unfolding dist_commute
apply clarify
apply (rule_tac x="e - dist xa x" in exI)
@@ -340,7 +342,7 @@
lemma centre_in_ball[simp]: "x \<in> ball x e \<longleftrightarrow> e > 0" by (metis mem_ball dist_self)
lemma open_contains_ball: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. ball x e \<subseteq> S)"
- unfolding open_def subset_eq mem_ball Ball_def dist_commute ..
+ unfolding open_dist subset_eq mem_ball Ball_def dist_commute ..
lemma open_contains_ball_eq: "open S \<Longrightarrow> \<forall>x. x\<in>S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)"
by (metis open_contains_ball subset_eq centre_in_ball)
@@ -382,11 +384,13 @@
lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> closedin (subtopology euclidean T) S"
by (auto simp add: closedin_closed)
-lemma openin_euclidean_subtopology_iff: "openin (subtopology euclidean U) S
+lemma openin_euclidean_subtopology_iff:
+ fixes S U :: "'a::metric_space set"
+ shows "openin (subtopology euclidean U) S
\<longleftrightarrow> S \<subseteq> U \<and> (\<forall>x\<in>S. \<exists>e>0. \<forall>x'\<in>U. dist x' x < e \<longrightarrow> x'\<in> S)" (is "?lhs \<longleftrightarrow> ?rhs")
proof-
{assume ?lhs hence ?rhs unfolding openin_subtopology open_openin[symmetric]
- by (simp add: open_def) blast}
+ by (simp add: open_dist) blast}
moreover
{assume SU: "S \<subseteq> U" and H: "\<And>x. x \<in> S \<Longrightarrow> \<exists>e>0. \<forall>x'\<in>U. dist x' x < e \<longrightarrow> x' \<in> S"
from H obtain d where d: "\<And>x . x\<in> S \<Longrightarrow> d x > 0 \<and> (\<forall>x' \<in> U. dist x' x < d x \<longrightarrow> x' \<in> S)"
@@ -441,7 +445,7 @@
e1 \<inter> e2 = {} \<and>
~(e1 = {}) \<and>
~(e2 = {}))"
-unfolding connected_def openin_open by blast
+unfolding connected_def openin_open by (safe, blast+)
lemma exists_diff: "(\<exists>S. P(UNIV - S)) \<longleftrightarrow> (\<exists>S. P S)" (is "?lhs \<longleftrightarrow> ?rhs")
proof-
@@ -480,31 +484,61 @@
subsection{* Hausdorff and other separation properties *}
-lemma hausdorff:
- assumes xy: "x \<noteq> y"
- shows "\<exists>U V. open U \<and> open V \<and> x\<in> U \<and> y \<in> V \<and> (U \<inter> V = {})" (is "\<exists>U V. ?P U V")
-proof-
+axclass t0_space \<subseteq> topological_space
+ t0_space:
+ "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U)"
+
+axclass t1_space \<subseteq> topological_space
+ t1_space:
+ "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<notin> U \<and> x \<notin> V \<and> y \<in> V"
+
+instance t1_space \<subseteq> t0_space
+by default (fast dest: t1_space)
+
+text {* T2 spaces are also known as Hausdorff spaces. *}
+
+axclass t2_space \<subseteq> topological_space
+ hausdorff:
+ "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
+
+instance t2_space \<subseteq> t1_space
+by default (fast dest: hausdorff)
+
+instance metric_space \<subseteq> t2_space
+proof
+ fix x y :: "'a::metric_space"
+ assume xy: "x \<noteq> y"
let ?U = "ball x (dist x y / 2)"
let ?V = "ball y (dist x y / 2)"
have th0: "\<And>d x y z. (d x z :: real) <= d x y + d y z \<Longrightarrow> d y z = d z y
==> ~(d x y * 2 < d x z \<and> d z y * 2 < d x z)" by arith
- have "?P ?U ?V" using dist_pos_lt[OF xy] th0[of dist,OF dist_triangle dist_commute]
- by (auto simp add: expand_set_eq less_divide_eq_number_of1)
- then show ?thesis by blast
-qed
-
-lemma separation_t2: "x \<noteq> y \<longleftrightarrow> (\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {})"
+ have "open ?U \<and> open ?V \<and> x \<in> ?U \<and> y \<in> ?V \<and> ?U \<inter> ?V = {}"
+ using dist_pos_lt[OF xy] th0[of dist,OF dist_triangle dist_commute]
+ by (auto simp add: expand_set_eq)
+ then show "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
+ by blast
+qed
+
+lemma separation_t2:
+ fixes x y :: "'a::t2_space"
+ shows "x \<noteq> y \<longleftrightarrow> (\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {})"
using hausdorff[of x y] by blast
-lemma separation_t1: "x \<noteq> y \<longleftrightarrow> (\<exists>U V. open U \<and> open V \<and> x \<in>U \<and> y\<notin> U \<and> x\<notin>V \<and> y\<in>V)"
- using separation_t2[of x y] by blast
-
-lemma separation_t0: "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> ~(x\<in>U \<longleftrightarrow> y\<in>U))" by(metis separation_t1)
+lemma separation_t1:
+ fixes x y :: "'a::t1_space"
+ shows "x \<noteq> y \<longleftrightarrow> (\<exists>U V. open U \<and> open V \<and> x \<in>U \<and> y\<notin> U \<and> x\<notin>V \<and> y\<in>V)"
+ using t1_space[of x y] by blast
+
+lemma separation_t0:
+ fixes x y :: "'a::t0_space"
+ shows "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> ~(x\<in>U \<longleftrightarrow> y\<in>U))"
+ using t0_space[of x y] by blast
subsection{* Limit points *}
definition
- islimpt:: "'a::metric_space \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "islimpt" 60) where
+ islimpt:: "'a::topological_space \<Rightarrow> 'a set \<Rightarrow> bool"
+ (infixr "islimpt" 60) where
"x islimpt S \<longleftrightarrow> (\<forall>T. x\<in>T \<longrightarrow> open T \<longrightarrow> (\<exists>y\<in>S. y\<in>T \<and> y\<noteq>x))"
(* FIXME: Sure this form is OK????*)
@@ -513,23 +547,29 @@
using assms unfolding islimpt_def by auto
lemma islimpt_subset: "x islimpt S \<Longrightarrow> S \<subseteq> T ==> x islimpt T" by (auto simp add: islimpt_def)
-lemma islimpt_approachable: "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e)"
+
+lemma islimpt_approachable:
+ fixes x :: "'a::metric_space"
+ shows "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e)"
unfolding islimpt_def
apply auto
apply(erule_tac x="ball x e" in allE)
apply auto
apply(rule_tac x=y in bexI)
apply (auto simp add: dist_commute)
- apply (simp add: open_def, drule (1) bspec)
+ apply (simp add: open_dist, drule (1) bspec)
apply (clarify, drule spec, drule (1) mp, auto)
done
-lemma islimpt_approachable_le: "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in> S. x' \<noteq> x \<and> dist x' x <= e)"
+lemma islimpt_approachable_le:
+ fixes x :: "'a::metric_space"
+ shows "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in> S. x' \<noteq> x \<and> dist x' x <= e)"
unfolding islimpt_approachable
using approachable_lt_le[where f="\<lambda>x'. dist x' x" and P="\<lambda>x'. \<not> (x'\<in>S \<and> x'\<noteq>x)"]
by metis (* FIXME: VERY slow! *)
axclass perfect_space \<subseteq> metric_space
+ (* FIXME: perfect_space should inherit from topological_space *)
islimpt_UNIV [simp, intro]: "x islimpt UNIV"
lemma perfect_choose_dist:
@@ -544,7 +584,7 @@
apply (clarify, rule_tac x="x + e/2" in bexI)
apply (auto simp add: dist_norm)
done
-
+
instance "^" :: (perfect_space, finite) perfect_space
proof
fix x :: "'a ^ 'b"
@@ -576,7 +616,7 @@
by (metis DiffE DiffI UNIV_I insertCI insert_absorb mem_def)
lemma islimpt_EMPTY[simp]: "\<not> x islimpt {}"
- unfolding islimpt_approachable apply auto by ferrack
+ unfolding islimpt_def by auto
lemma closed_positive_orthant: "closed {x::real^'n::finite. \<forall>i. 0 \<le>x$i}"
proof-
@@ -616,7 +656,9 @@
ultimately show ?case by blast
qed
-lemma islimpt_finite: assumes fS: "finite S" shows "\<not> a islimpt S"
+lemma islimpt_finite:
+ fixes S :: "'a::metric_space set"
+ assumes fS: "finite S" shows "\<not> a islimpt S"
unfolding islimpt_approachable
using finite_set_avoid[OF fS, of a] by (metis dist_commute not_le)
@@ -624,13 +666,14 @@
apply (rule iffI)
defer
apply (metis Un_upper1 Un_upper2 islimpt_subset)
- unfolding islimpt_approachable
- apply auto
- apply (erule_tac x="min e ea" in allE)
- apply auto
+ unfolding islimpt_def
+ apply (rule ccontr, clarsimp, rename_tac A B)
+ apply (drule_tac x="A \<inter> B" in spec)
+ apply (auto simp add: open_inter)
done
lemma discrete_imp_closed:
+ fixes S :: "'a::metric_space set"
assumes e: "0 < e" and d: "\<forall>x \<in> S. \<forall>y \<in> S. dist y x < e \<longrightarrow> y = x"
shows "closed S"
proof-
@@ -644,7 +687,7 @@
by (intro dist_triangle_lt [where z=x], simp)
from d[rule_format, OF y(1) z(1) th] y z
have False by (auto simp add: dist_commute)}
- then show ?thesis by (metis islimpt_approachable closed_limpt)
+ then show ?thesis by (metis islimpt_approachable closed_limpt [where 'a='a])
qed
subsection{* Interior of a Set *}
@@ -652,7 +695,7 @@
lemma interior_eq: "interior S = S \<longleftrightarrow> open S"
apply (simp add: expand_set_eq interior_def)
- apply (subst (2) open_subopen) by blast
+ apply (subst (2) open_subopen) by (safe, blast+)
lemma interior_open: "open S ==> (interior S = S)" by (metis interior_eq)
@@ -701,7 +744,6 @@
qed
lemma interior_closed_Un_empty_interior:
- fixes S T :: "'a::metric_space set"
assumes cS: "closed S" and iT: "interior T = {}"
shows "interior(S \<union> T) = interior S"
proof
@@ -861,7 +903,10 @@
unfolding closure_interior
by auto
-lemma open_inter_closure_subset: "open S \<Longrightarrow> (S \<inter> (closure T)) \<subseteq> closure(S \<inter> T)"
+lemma open_inter_closure_subset:
+ fixes S :: "'a::metric_space set"
+ (* FIXME: generalize to topological_space *)
+ shows "open S \<Longrightarrow> (S \<inter> (closure T)) \<subseteq> closure(S \<inter> T)"
proof
fix x
assume as: "open S" "x \<in> S \<inter> closure T"
@@ -869,7 +914,7 @@
{ fix e::real
assume "e > 0"
from as `open S` obtain e' where "e' > 0" and e':"\<forall>x'. dist x' x < e' \<longrightarrow> x' \<in> S"
- unfolding open_def
+ unfolding open_dist
by auto
let ?e = "min e e'"
from `e>0` `e'>0` have "?e > 0"
@@ -913,7 +958,9 @@
lemma frontier_closures: "frontier S = (closure S) \<inter> (closure(UNIV - S))"
by (auto simp add: frontier_def interior_closure)
-lemma frontier_straddle: "a \<in> frontier S \<longleftrightarrow> (\<forall>e>0. (\<exists>x\<in>S. dist a x < e) \<and> (\<exists>x. x \<notin> S \<and> dist a x < e))" (is "?lhs \<longleftrightarrow> ?rhs")
+lemma frontier_straddle:
+ fixes a :: "'a::metric_space"
+ shows "a \<in> frontier S \<longleftrightarrow> (\<forall>e>0. (\<exists>x\<in>S. dist a x < e) \<and> (\<exists>x. x \<notin> S \<and> dist a x < e))" (is "?lhs \<longleftrightarrow> ?rhs")
proof
assume "?lhs"
{ fix e::real
@@ -1202,7 +1249,7 @@
assume ?lhs
{ fix e::real assume "e>0"
obtain d where d: "d >0" "\<forall>x\<in>S. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e" using `?lhs` `e>0` unfolding Lim_within by auto
- obtain d' where d': "d'>0" "\<forall>x. dist x a < d' \<longrightarrow> x \<in> S" using assms unfolding open_def by auto
+ obtain d' where d': "d'>0" "\<forall>x. dist x a < d' \<longrightarrow> x \<in> S" using assms unfolding open_dist by auto
from d d' have "\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e" by (rule_tac x= "min d d'" in exI)auto
}
thus ?rhs unfolding Lim_at by auto
@@ -1620,7 +1667,6 @@
qed
lemma Lim_transform_eventually:
- fixes f g :: "'a::type \<Rightarrow> 'b::metric_space"
shows "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net ==> (g ---> l) net"
unfolding tendsto_def
apply (clarify, drule spec, drule (1) mp)
@@ -1628,7 +1674,6 @@
done
lemma Lim_transform_within:
- fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space"
assumes "0 < d" "(\<forall>x'\<in>S. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x')"
"(f ---> l) (at x within S)"
shows "(g ---> l) (at x within S)"
@@ -1642,7 +1687,6 @@
done
lemma Lim_transform_at:
- fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space"
shows "0 < d \<Longrightarrow> (\<forall>x'. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x') \<Longrightarrow>
(f ---> l) (at x) ==> (g ---> l) (at x)"
apply (subst within_UNIV[symmetric])
@@ -1652,7 +1696,6 @@
text{* Common case assuming being away from some crucial point like 0. *}
lemma Lim_transform_away_within:
- fixes f:: "'a::metric_space \<Rightarrow> 'b::metric_space"
assumes "a\<noteq>b" "\<forall>x\<in> S. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
and "(f ---> l) (at a within S)"
shows "(g ---> l) (at a within S)"
@@ -1663,7 +1706,6 @@
qed
lemma Lim_transform_away_at:
- fixes f:: "'a::metric_space \<Rightarrow> 'b::metric_space"
assumes ab: "a\<noteq>b" and fg: "\<forall>x. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
and fl: "(f ---> l) (at a)"
shows "(g ---> l) (at a)"
@@ -1673,8 +1715,6 @@
text{* Alternatively, within an open set. *}
lemma Lim_transform_within_open:
- fixes f:: "'a::metric_space \<Rightarrow> 'b::metric_space"
- (* FIXME: generalize to metric_space *)
assumes "open S" "a \<in> S" "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> f x = g x" "(f ---> l) (at a)"
shows "(g ---> l) (at a)"
proof-
@@ -1715,15 +1755,21 @@
qed
lemma closed_sequential_limits:
- "closed S \<longleftrightarrow> (\<forall>x l. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially \<longrightarrow> l \<in> S)"
+ fixes S :: "'a::metric_space set"
+ shows "closed S \<longleftrightarrow> (\<forall>x l. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially \<longrightarrow> l \<in> S)"
unfolding closed_limpt
- by (metis closure_sequential closure_closed closed_limpt islimpt_sequential mem_delete)
-
-lemma closure_approachable: "x \<in> closure S \<longleftrightarrow> (\<forall>e>0. \<exists>y\<in>S. dist y x < e)"
+ using closure_sequential [where 'a='a] closure_closed [where 'a='a] closed_limpt [where 'a='a] islimpt_sequential [where 'a='a] mem_delete [where 'a='a]
+ by metis
+
+lemma closure_approachable:
+ fixes S :: "'a::metric_space set"
+ shows "x \<in> closure S \<longleftrightarrow> (\<forall>e>0. \<exists>y\<in>S. dist y x < e)"
apply (auto simp add: closure_def islimpt_approachable)
by (metis dist_self)
-lemma closed_approachable: "closed S ==> (\<forall>e>0. \<exists>y\<in>S. dist y x < e) \<longleftrightarrow> x \<in> S"
+lemma closed_approachable:
+ fixes S :: "'a::metric_space set"
+ shows "closed S ==> (\<forall>e>0. \<exists>y\<in>S. dist y x < e) \<longleftrightarrow> x \<in> S"
by (metis closure_closed closure_approachable)
text{* Some other lemmas about sequences. *}
@@ -1758,7 +1804,7 @@
lemma closed_cball: "closed (cball x e)"
unfolding cball_def closed_def Compl_eq_Diff_UNIV [symmetric]
unfolding Collect_neg_eq [symmetric] not_le
-apply (clarsimp simp add: open_def, rename_tac y)
+apply (clarsimp simp add: open_dist, rename_tac y)
apply (rule_tac x="dist x y - e" in exI, clarsimp)
apply (cut_tac x=x and y=x' and z=y in dist_triangle)
apply simp
@@ -1876,7 +1922,7 @@
case True note cs = this
have "ball x e \<subseteq> cball x e" using ball_subset_cball by auto moreover
{ fix S y assume as: "S \<subseteq> cball x e" "open S" "y\<in>S"
- then obtain d where "d>0" and d:"\<forall>x'. dist x' y < d \<longrightarrow> x' \<in> S" unfolding open_def by blast
+ then obtain d where "d>0" and d:"\<forall>x'. dist x' y < d \<longrightarrow> x' \<in> S" unfolding open_dist by blast
then obtain xa where xa:"dist y xa = d / 2" using vector_choose_dist[of "d/2" y] by auto
hence xa_y:"xa \<noteq> y" using dist_nz[of y xa] using `d>0` by auto
@@ -2506,7 +2552,7 @@
obtain b where "l\<in>b" "b\<in>t" using assms(2) and l by auto
then obtain e where "e>0" and e:"\<forall>z. dist z l < e \<longrightarrow> z\<in>b"
- using assms(3)[THEN bspec[where x=b]] unfolding open_def by auto
+ using assms(3)[THEN bspec[where x=b]] unfolding open_dist by auto
then obtain N1 where N1:"\<forall>n\<ge>N1. dist ((f \<circ> r) n) l < e / 2"
using lr[unfolded Lim_sequentially, THEN spec[where x="e/2"]] by auto
@@ -2672,6 +2718,7 @@
qed
lemma bolzano_weierstrass_imp_closed:
+ fixes s :: "'a::metric_space set" (* TODO: can this be generalized? *)
assumes "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t)"
shows "closed s"
proof-
@@ -2797,8 +2844,10 @@
unfolding compact_def o_def
by (auto simp add: tendsto_const)
-lemma closed_sing [simp]: shows "closed {a}"
- apply (clarsimp simp add: closed_def open_def)
+lemma closed_sing [simp]:
+ fixes a :: "'a::metric_space"
+ shows "closed {a}"
+ apply (clarsimp simp add: closed_def open_dist)
apply (rule ccontr)
apply (drule_tac x="dist x a" in spec)
apply (simp add: dist_nz dist_commute)
@@ -2829,7 +2878,9 @@
using frontier_subset_closed compact_eq_bounded_closed
by blast
-lemma open_delete: "open s ==> open(s - {x})"
+lemma open_delete:
+ fixes s :: "'a::metric_space set"
+ shows "open s ==> open(s - {x})"
using open_diff[of s "{x}"] closed_sing
by blast
@@ -3443,7 +3494,7 @@
{ fix t assume as: "open t" "f x \<in> t"
then obtain e where "e>0" and e:"ball (f x) e \<subseteq> t" unfolding open_contains_ball by auto
- obtain d where "d>0" and d:"\<forall>y. 0 < dist y x \<and> dist y x < d \<longrightarrow> dist (f y) (f x) < e" using `e>0` using `?lhs`[unfolded continuous_at Lim_at open_def] by auto
+ obtain d where "d>0" and d:"\<forall>y. 0 < dist y x \<and> dist y x < d \<longrightarrow> dist (f y) (f x) < e" using `e>0` using `?lhs`[unfolded continuous_at Lim_at open_dist] by auto
have "open (ball x d)" using open_ball by auto
moreover have "x \<in> ball x d" unfolding centre_in_ball using `d>0` by simp
@@ -3672,7 +3723,7 @@
shows "open((\<lambda>x. c *s x) ` s)"
proof-
{ fix x assume "x \<in> s"
- then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> s" using assms(2)[unfolded open_def, THEN bspec[where x=x]] by auto
+ then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> s" using assms(2)[unfolded open_dist, THEN bspec[where x=x]] by auto
have "e * abs c > 0" using assms(1)[unfolded zero_less_abs_iff[THEN sym]] using real_mult_order[OF `e>0`] by auto
moreover
{ fix y assume "dist y (c *s x) < e * \<bar>c\<bar>"
@@ -3681,7 +3732,7 @@
assms(1)[unfolded zero_less_abs_iff[THEN sym]] by (simp del:zero_less_abs_iff)
hence "y \<in> op *s c ` s" using rev_image_eqI[of "(1 / c) *s y" s y "op *s c"] e[THEN spec[where x="(1 / c) *s y"]] assms(1) unfolding dist_norm vector_smult_assoc by auto }
ultimately have "\<exists>e>0. \<forall>x'. dist x' (c *s x) < e \<longrightarrow> x' \<in> op *s c ` s" apply(rule_tac x="e * abs c" in exI) by auto }
- thus ?thesis unfolding open_def by auto
+ thus ?thesis unfolding open_dist by auto
qed
lemma open_negations:
@@ -3906,7 +3957,7 @@
fixes s :: "real set" shows
"open(vec1 ` s) \<longleftrightarrow>
(\<forall>x \<in> s. \<exists>e>0. \<forall>x'. abs(x' - x) < e --> x' \<in> s)" (is "?lhs = ?rhs")
- unfolding open_def apply simp unfolding forall_vec1 dist_vec1 vec1_in_image_vec1 by simp
+ unfolding open_dist apply simp unfolding forall_vec1 dist_vec1 vec1_in_image_vec1 by simp
lemma islimpt_approachable_vec1:
fixes s :: "real set" shows
@@ -4666,7 +4717,7 @@
hence "a < x' \<and> x' < b" unfolding vector_less_def by auto }
ultimately have "\<exists>e>0. \<forall>x'. dist x' x < e \<longrightarrow> x' \<in> {a<..<b}" by (auto, rule_tac x="?d" in exI, simp)
}
- thus ?thesis unfolding open_def using open_interval_lemma by auto
+ thus ?thesis unfolding open_dist using open_interval_lemma by auto
qed
lemma closed_interval: fixes a :: "real^'n::finite" shows "closed {a .. b}"
@@ -4695,7 +4746,7 @@
next
{ fix x assume "\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> {a..b}"
then obtain s where s:"open s" "x \<in> s" "s \<subseteq> {a..b}" by auto
- then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> {a..b}" unfolding open_def and subset_eq by auto
+ then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> {a..b}" unfolding open_dist and subset_eq by auto
{ fix i
have "dist (x - (e / 2) *s basis i) x < e"
"dist (x + (e / 2) *s basis i) x < e"
--- a/src/HOL/RealVector.thy Wed Jun 03 15:48:54 2009 +0200
+++ b/src/HOL/RealVector.thy Wed Jun 03 12:24:09 2009 -0700
@@ -416,12 +416,26 @@
by (rule Reals_cases) auto
+subsection {* Topological spaces *}
+
+class topo =
+ fixes topo :: "'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"
+
+
subsection {* Metric spaces *}
class dist =
fixes dist :: "'a \<Rightarrow> 'a \<Rightarrow> real"
-class metric_space = dist +
+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 = 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
@@ -452,6 +466,26 @@
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 "UNIV \<in> topo"
+ unfolding topo_dist by simp
+next
+ 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 "T \<subseteq> topo" thus "\<Union>T \<in> topo"
+ unfolding topo_dist by fast
+qed
+
end
@@ -466,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 +
+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"
@@ -497,16 +531,20 @@
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 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}"
instance
apply (intro_classes, unfold real_norm_def real_scaleR_def)
apply (rule dist_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)