# HG changeset patch
# User hoelzl
# Date 1300109853 -3600
# Node ID 1cf3e4107a2a9e7972c66c9cbdee77bd3564acf4
# Parent  d65835c381dd9c4f848519606b2d25e87f3ab8c5
moved t2_spaces to HOL image

diff -r d65835c381dd -r 1cf3e4107a2a src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Mar 14 12:34:12 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Mar 14 14:37:33 2011 +0100
@@ -326,42 +326,6 @@
 
 text{* Hence more metric properties. *}
 
-lemma dist_triangle_alt:
-  fixes x y z :: "'a::metric_space"
-  shows "dist y z <= dist x y + dist x z"
-by (rule dist_triangle3)
-
-lemma dist_pos_lt:
-  fixes x y :: "'a::metric_space"
-  shows "x \<noteq> y ==> 0 < dist x y"
-by (simp add: zero_less_dist_iff)
-
-lemma dist_nz:
-  fixes x y :: "'a::metric_space"
-  shows "x \<noteq> y \<longleftrightarrow> 0 < dist x y"
-by (simp add: zero_less_dist_iff)
-
-lemma dist_triangle_le:
-  fixes x y z :: "'a::metric_space"
-  shows "dist x z + dist y z <= e \<Longrightarrow> dist x y <= e"
-by (rule order_trans [OF dist_triangle2])
-
-lemma dist_triangle_lt:
-  fixes x y z :: "'a::metric_space"
-  shows "dist x z + dist y z < e ==> dist x y < e"
-by (rule le_less_trans [OF dist_triangle2])
-
-lemma dist_triangle_half_l:
-  fixes x1 x2 y :: "'a::metric_space"
-  shows "dist x1 y < e / 2 \<Longrightarrow> dist x2 y < e / 2 \<Longrightarrow> dist x1 x2 < e"
-by (rule dist_triangle_lt [where z=y], simp)
-
-lemma dist_triangle_half_r:
-  fixes x1 x2 y :: "'a::metric_space"
-  shows "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 \<Longrightarrow> dist x1 x2 < e"
-by (rule dist_triangle_half_l, simp_all add: dist_commute)
-
-
 lemma norm_triangle_half_r:
   shows "norm (y - x1) < e / 2 \<Longrightarrow> norm (y - x2) < e / 2 \<Longrightarrow> norm (x1 - x2) < e"
   using dist_triangle_half_r unfolding dist_norm[THEN sym] by auto
diff -r d65835c381dd -r 1cf3e4107a2a src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Mar 14 12:34:12 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Mar 14 14:37:33 2011 +0100
@@ -1,4 +1,3 @@
-
 header {* Kurzweil-Henstock Gauge Integration in many dimensions. *}
 (*  Author:                     John Harrison
     Translation from HOL light: Robert Himmelmann, TU Muenchen *)
@@ -3780,7 +3779,7 @@
   shows "f x = y"
 proof- have "{x \<in> s. f x \<in> {y}} = {} \<or> {x \<in> s. f x \<in> {y}} = s"
     apply(rule assms(1)[unfolded connected_clopen,rule_format]) apply rule defer
-    apply(rule continuous_closed_in_preimage[OF assms(4) closed_sing])
+    apply(rule continuous_closed_in_preimage[OF assms(4) closed_singleton])
     apply(rule open_openin_trans[OF assms(2)]) unfolding open_contains_ball
   proof safe fix x assume "x\<in>s" 
     from assms(2)[unfolded open_contains_ball,rule_format,OF this] guess e .. note e=conjunctD2[OF this]
diff -r d65835c381dd -r 1cf3e4107a2a src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Mar 14 12:34:12 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Mar 14 14:37:33 2011 +0100
@@ -424,80 +424,6 @@
 lemma connected_empty[simp, intro]: "connected {}"
   by (simp add: connected_def)
 
-subsection{* Hausdorff and other separation properties *}
-
-class t0_space = topological_space +
-  assumes t0_space: "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U)"
-
-class t1_space = topological_space +
-  assumes t1_space: "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> x \<in> U \<and> y \<notin> U"
-
-instance t1_space \<subseteq> t0_space
-proof qed (fast dest: t1_space)
-
-lemma separation_t1:
-  fixes x y :: "'a::t1_space"
-  shows "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U)"
-  using t1_space[of x y] by blast
-
-lemma closed_sing:
-  fixes a :: "'a::t1_space"
-  shows "closed {a}"
-proof -
-  let ?T = "\<Union>{S. open S \<and> a \<notin> S}"
-  have "open ?T" by (simp add: open_Union)
-  also have "?T = - {a}"
-    by (simp add: set_eq_iff separation_t1, auto)
-  finally show "closed {a}" unfolding closed_def .
-qed
-
-lemma closed_insert [simp]:
-  fixes a :: "'a::t1_space"
-  assumes "closed S" shows "closed (insert a S)"
-proof -
-  from closed_sing assms
-  have "closed ({a} \<union> S)" by (rule closed_Un)
-  thus "closed (insert a S)" by simp
-qed
-
-lemma finite_imp_closed:
-  fixes S :: "'a::t1_space set"
-  shows "finite S \<Longrightarrow> closed S"
-by (induct set: finite, simp_all)
-
-text {* T2 spaces are also known as Hausdorff spaces. *}
-
-class t2_space = topological_space +
-  assumes 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
-proof qed (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 "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: set_eq_iff)
-  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_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
diff -r d65835c381dd -r 1cf3e4107a2a src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Mon Mar 14 12:34:12 2011 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Mon Mar 14 14:37:33 2011 +0100
@@ -57,7 +57,7 @@
   shows "f -` {x} \<inter> space M \<in> sets M"
 proof (cases "x \<in> f ` space M")
   case True then obtain y where "x = f y" by auto
-  from closed_sing[of "f y"]
+  from closed_singleton[of "f y"]
   have "{f y} \<in> sets borel" by (rule borel_closed)
   with assms show ?thesis
     unfolding in_borel_measurable_borel `x = f y` by auto
@@ -81,7 +81,7 @@
   shows "A \<in> sets borel \<Longrightarrow> insert x A \<in> sets borel"
   proof (rule borel.insert_in_sets)
     show "{x} \<in> sets borel"
-      using closed_sing[of x] by (rule borel_closed)
+      using closed_singleton[of x] by (rule borel_closed)
   qed simp
 
 lemma (in sigma_algebra) borel_measurable_const[simp, intro]:
diff -r d65835c381dd -r 1cf3e4107a2a src/HOL/RealVector.thy
--- a/src/HOL/RealVector.thy	Mon Mar 14 12:34:12 2011 +0100
+++ b/src/HOL/RealVector.thy	Mon Mar 14 14:37:33 2011 +0100
@@ -534,6 +534,34 @@
 lemma dist_triangle3: "dist x y \<le> dist a x + dist a y"
 using dist_triangle2 [of x y a] by (simp add: dist_commute)
 
+lemma dist_triangle_alt:
+  shows "dist y z <= dist x y + dist x z"
+by (rule dist_triangle3)
+
+lemma dist_pos_lt:
+  shows "x \<noteq> y ==> 0 < dist x y"
+by (simp add: zero_less_dist_iff)
+
+lemma dist_nz:
+  shows "x \<noteq> y \<longleftrightarrow> 0 < dist x y"
+by (simp add: zero_less_dist_iff)
+
+lemma dist_triangle_le:
+  shows "dist x z + dist y z <= e \<Longrightarrow> dist x y <= e"
+by (rule order_trans [OF dist_triangle2])
+
+lemma dist_triangle_lt:
+  shows "dist x z + dist y z < e ==> dist x y < e"
+by (rule le_less_trans [OF dist_triangle2])
+
+lemma dist_triangle_half_l:
+  shows "dist x1 y < e / 2 \<Longrightarrow> dist x2 y < e / 2 \<Longrightarrow> dist x1 x2 < e"
+by (rule dist_triangle_lt [where z=y], simp)
+
+lemma dist_triangle_half_r:
+  shows "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 \<Longrightarrow> dist x1 x2 < e"
+by (rule dist_triangle_half_l, simp_all add: dist_commute)
+
 subclass topological_space
 proof
   have "\<exists>e::real. 0 < e"
@@ -554,6 +582,13 @@
     unfolding open_dist by fast
 qed
 
+lemma (in metric_space) open_ball: "open {y. dist x y < d}"
+proof (unfold open_dist, intro ballI)
+  fix y assume *: "y \<in> {y. dist x y < d}"
+  then show "\<exists>e>0. \<forall>z. dist z y < e \<longrightarrow> z \<in> {y. dist x y < d}"
+    by (auto intro!: exI[of _ "d - dist x y"] simp: field_simps dist_triangle_lt)
+qed
+
 end
 
 
@@ -1060,4 +1095,78 @@
 interpretation of_real: bounded_linear "\<lambda>r. of_real r"
 unfolding of_real_def by (rule scaleR.bounded_linear_left)
 
+subsection{* Hausdorff and other separation properties *}
+
+class t0_space = topological_space +
+  assumes t0_space: "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U)"
+
+class t1_space = topological_space +
+  assumes t1_space: "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> x \<in> U \<and> y \<notin> U"
+
+instance t1_space \<subseteq> t0_space
+proof qed (fast dest: t1_space)
+
+lemma separation_t1:
+  fixes x y :: "'a::t1_space"
+  shows "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U)"
+  using t1_space[of x y] by blast
+
+lemma closed_singleton:
+  fixes a :: "'a::t1_space"
+  shows "closed {a}"
+proof -
+  let ?T = "\<Union>{S. open S \<and> a \<notin> S}"
+  have "open ?T" by (simp add: open_Union)
+  also have "?T = - {a}"
+    by (simp add: set_eq_iff separation_t1, auto)
+  finally show "closed {a}" unfolding closed_def .
+qed
+
+lemma closed_insert [simp]:
+  fixes a :: "'a::t1_space"
+  assumes "closed S" shows "closed (insert a S)"
+proof -
+  from closed_singleton assms
+  have "closed ({a} \<union> S)" by (rule closed_Un)
+  thus "closed (insert a S)" by simp
+qed
+
+lemma finite_imp_closed:
+  fixes S :: "'a::t1_space set"
+  shows "finite S \<Longrightarrow> closed S"
+by (induct set: finite, simp_all)
+
+text {* T2 spaces are also known as Hausdorff spaces. *}
+
+class t2_space = topological_space +
+  assumes 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
+proof qed (fast dest: hausdorff)
+
+instance metric_space \<subseteq> t2_space
+proof
+  fix x y :: "'a::metric_space"
+  assume xy: "x \<noteq> y"
+  let ?U = "{y'. dist x y' < dist x y / 2}"
+  let ?V = "{x'. dist y x' < dist x y / 2}"
+  have th0: "\<And>d x y z. (d x z :: real) \<le> d x y + d y z \<Longrightarrow> d y z = d z y
+               \<Longrightarrow> \<not>(d x y * 2 < d x z \<and> d z y * 2 < d x z)" by arith
+  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]
+    using open_ball[of _ "dist x y / 2"] by auto
+  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_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
+
 end