moved t2_spaces to HOL image
authorhoelzl
Mon Mar 14 14:37:33 2011 +0100 (2011-03-14)
changeset 419691cf3e4107a2a
parent 41966 d65835c381dd
child 41970 47d6e13d1710
moved t2_spaces to HOL image
src/HOL/Multivariate_Analysis/Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/RealVector.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Mar 14 12:34:12 2011 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Mar 14 14:37:33 2011 +0100
     1.3 @@ -326,42 +326,6 @@
     1.4  
     1.5  text{* Hence more metric properties. *}
     1.6  
     1.7 -lemma dist_triangle_alt:
     1.8 -  fixes x y z :: "'a::metric_space"
     1.9 -  shows "dist y z <= dist x y + dist x z"
    1.10 -by (rule dist_triangle3)
    1.11 -
    1.12 -lemma dist_pos_lt:
    1.13 -  fixes x y :: "'a::metric_space"
    1.14 -  shows "x \<noteq> y ==> 0 < dist x y"
    1.15 -by (simp add: zero_less_dist_iff)
    1.16 -
    1.17 -lemma dist_nz:
    1.18 -  fixes x y :: "'a::metric_space"
    1.19 -  shows "x \<noteq> y \<longleftrightarrow> 0 < dist x y"
    1.20 -by (simp add: zero_less_dist_iff)
    1.21 -
    1.22 -lemma dist_triangle_le:
    1.23 -  fixes x y z :: "'a::metric_space"
    1.24 -  shows "dist x z + dist y z <= e \<Longrightarrow> dist x y <= e"
    1.25 -by (rule order_trans [OF dist_triangle2])
    1.26 -
    1.27 -lemma dist_triangle_lt:
    1.28 -  fixes x y z :: "'a::metric_space"
    1.29 -  shows "dist x z + dist y z < e ==> dist x y < e"
    1.30 -by (rule le_less_trans [OF dist_triangle2])
    1.31 -
    1.32 -lemma dist_triangle_half_l:
    1.33 -  fixes x1 x2 y :: "'a::metric_space"
    1.34 -  shows "dist x1 y < e / 2 \<Longrightarrow> dist x2 y < e / 2 \<Longrightarrow> dist x1 x2 < e"
    1.35 -by (rule dist_triangle_lt [where z=y], simp)
    1.36 -
    1.37 -lemma dist_triangle_half_r:
    1.38 -  fixes x1 x2 y :: "'a::metric_space"
    1.39 -  shows "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 \<Longrightarrow> dist x1 x2 < e"
    1.40 -by (rule dist_triangle_half_l, simp_all add: dist_commute)
    1.41 -
    1.42 -
    1.43  lemma norm_triangle_half_r:
    1.44    shows "norm (y - x1) < e / 2 \<Longrightarrow> norm (y - x2) < e / 2 \<Longrightarrow> norm (x1 - x2) < e"
    1.45    using dist_triangle_half_r unfolding dist_norm[THEN sym] by auto
     2.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Mar 14 12:34:12 2011 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Mar 14 14:37:33 2011 +0100
     2.3 @@ -1,4 +1,3 @@
     2.4 -
     2.5  header {* Kurzweil-Henstock Gauge Integration in many dimensions. *}
     2.6  (*  Author:                     John Harrison
     2.7      Translation from HOL light: Robert Himmelmann, TU Muenchen *)
     2.8 @@ -3780,7 +3779,7 @@
     2.9    shows "f x = y"
    2.10  proof- have "{x \<in> s. f x \<in> {y}} = {} \<or> {x \<in> s. f x \<in> {y}} = s"
    2.11      apply(rule assms(1)[unfolded connected_clopen,rule_format]) apply rule defer
    2.12 -    apply(rule continuous_closed_in_preimage[OF assms(4) closed_sing])
    2.13 +    apply(rule continuous_closed_in_preimage[OF assms(4) closed_singleton])
    2.14      apply(rule open_openin_trans[OF assms(2)]) unfolding open_contains_ball
    2.15    proof safe fix x assume "x\<in>s" 
    2.16      from assms(2)[unfolded open_contains_ball,rule_format,OF this] guess e .. note e=conjunctD2[OF this]
     3.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Mar 14 12:34:12 2011 +0100
     3.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Mar 14 14:37:33 2011 +0100
     3.3 @@ -424,80 +424,6 @@
     3.4  lemma connected_empty[simp, intro]: "connected {}"
     3.5    by (simp add: connected_def)
     3.6  
     3.7 -subsection{* Hausdorff and other separation properties *}
     3.8 -
     3.9 -class t0_space = topological_space +
    3.10 -  assumes t0_space: "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U)"
    3.11 -
    3.12 -class t1_space = topological_space +
    3.13 -  assumes t1_space: "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> x \<in> U \<and> y \<notin> U"
    3.14 -
    3.15 -instance t1_space \<subseteq> t0_space
    3.16 -proof qed (fast dest: t1_space)
    3.17 -
    3.18 -lemma separation_t1:
    3.19 -  fixes x y :: "'a::t1_space"
    3.20 -  shows "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U)"
    3.21 -  using t1_space[of x y] by blast
    3.22 -
    3.23 -lemma closed_sing:
    3.24 -  fixes a :: "'a::t1_space"
    3.25 -  shows "closed {a}"
    3.26 -proof -
    3.27 -  let ?T = "\<Union>{S. open S \<and> a \<notin> S}"
    3.28 -  have "open ?T" by (simp add: open_Union)
    3.29 -  also have "?T = - {a}"
    3.30 -    by (simp add: set_eq_iff separation_t1, auto)
    3.31 -  finally show "closed {a}" unfolding closed_def .
    3.32 -qed
    3.33 -
    3.34 -lemma closed_insert [simp]:
    3.35 -  fixes a :: "'a::t1_space"
    3.36 -  assumes "closed S" shows "closed (insert a S)"
    3.37 -proof -
    3.38 -  from closed_sing assms
    3.39 -  have "closed ({a} \<union> S)" by (rule closed_Un)
    3.40 -  thus "closed (insert a S)" by simp
    3.41 -qed
    3.42 -
    3.43 -lemma finite_imp_closed:
    3.44 -  fixes S :: "'a::t1_space set"
    3.45 -  shows "finite S \<Longrightarrow> closed S"
    3.46 -by (induct set: finite, simp_all)
    3.47 -
    3.48 -text {* T2 spaces are also known as Hausdorff spaces. *}
    3.49 -
    3.50 -class t2_space = topological_space +
    3.51 -  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 = {}"
    3.52 -
    3.53 -instance t2_space \<subseteq> t1_space
    3.54 -proof qed (fast dest: hausdorff)
    3.55 -
    3.56 -instance metric_space \<subseteq> t2_space
    3.57 -proof
    3.58 -  fix x y :: "'a::metric_space"
    3.59 -  assume xy: "x \<noteq> y"
    3.60 -  let ?U = "ball x (dist x y / 2)"
    3.61 -  let ?V = "ball y (dist x y / 2)"
    3.62 -  have th0: "\<And>d x y z. (d x z :: real) <= d x y + d y z \<Longrightarrow> d y z = d z y
    3.63 -               ==> ~(d x y * 2 < d x z \<and> d z y * 2 < d x z)" by arith
    3.64 -  have "open ?U \<and> open ?V \<and> x \<in> ?U \<and> y \<in> ?V \<and> ?U \<inter> ?V = {}"
    3.65 -    using dist_pos_lt[OF xy] th0[of dist,OF dist_triangle dist_commute]
    3.66 -    by (auto simp add: set_eq_iff)
    3.67 -  then show "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
    3.68 -    by blast
    3.69 -qed
    3.70 -
    3.71 -lemma separation_t2:
    3.72 -  fixes x y :: "'a::t2_space"
    3.73 -  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 = {})"
    3.74 -  using hausdorff[of x y] by blast
    3.75 -
    3.76 -lemma separation_t0:
    3.77 -  fixes x y :: "'a::t0_space"
    3.78 -  shows "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> ~(x\<in>U \<longleftrightarrow> y\<in>U))"
    3.79 -  using t0_space[of x y] by blast
    3.80 -
    3.81  subsection{* Limit points *}
    3.82  
    3.83  definition
     4.1 --- a/src/HOL/Probability/Borel_Space.thy	Mon Mar 14 12:34:12 2011 +0100
     4.2 +++ b/src/HOL/Probability/Borel_Space.thy	Mon Mar 14 14:37:33 2011 +0100
     4.3 @@ -57,7 +57,7 @@
     4.4    shows "f -` {x} \<inter> space M \<in> sets M"
     4.5  proof (cases "x \<in> f ` space M")
     4.6    case True then obtain y where "x = f y" by auto
     4.7 -  from closed_sing[of "f y"]
     4.8 +  from closed_singleton[of "f y"]
     4.9    have "{f y} \<in> sets borel" by (rule borel_closed)
    4.10    with assms show ?thesis
    4.11      unfolding in_borel_measurable_borel `x = f y` by auto
    4.12 @@ -81,7 +81,7 @@
    4.13    shows "A \<in> sets borel \<Longrightarrow> insert x A \<in> sets borel"
    4.14    proof (rule borel.insert_in_sets)
    4.15      show "{x} \<in> sets borel"
    4.16 -      using closed_sing[of x] by (rule borel_closed)
    4.17 +      using closed_singleton[of x] by (rule borel_closed)
    4.18    qed simp
    4.19  
    4.20  lemma (in sigma_algebra) borel_measurable_const[simp, intro]:
     5.1 --- a/src/HOL/RealVector.thy	Mon Mar 14 12:34:12 2011 +0100
     5.2 +++ b/src/HOL/RealVector.thy	Mon Mar 14 14:37:33 2011 +0100
     5.3 @@ -534,6 +534,34 @@
     5.4  lemma dist_triangle3: "dist x y \<le> dist a x + dist a y"
     5.5  using dist_triangle2 [of x y a] by (simp add: dist_commute)
     5.6  
     5.7 +lemma dist_triangle_alt:
     5.8 +  shows "dist y z <= dist x y + dist x z"
     5.9 +by (rule dist_triangle3)
    5.10 +
    5.11 +lemma dist_pos_lt:
    5.12 +  shows "x \<noteq> y ==> 0 < dist x y"
    5.13 +by (simp add: zero_less_dist_iff)
    5.14 +
    5.15 +lemma dist_nz:
    5.16 +  shows "x \<noteq> y \<longleftrightarrow> 0 < dist x y"
    5.17 +by (simp add: zero_less_dist_iff)
    5.18 +
    5.19 +lemma dist_triangle_le:
    5.20 +  shows "dist x z + dist y z <= e \<Longrightarrow> dist x y <= e"
    5.21 +by (rule order_trans [OF dist_triangle2])
    5.22 +
    5.23 +lemma dist_triangle_lt:
    5.24 +  shows "dist x z + dist y z < e ==> dist x y < e"
    5.25 +by (rule le_less_trans [OF dist_triangle2])
    5.26 +
    5.27 +lemma dist_triangle_half_l:
    5.28 +  shows "dist x1 y < e / 2 \<Longrightarrow> dist x2 y < e / 2 \<Longrightarrow> dist x1 x2 < e"
    5.29 +by (rule dist_triangle_lt [where z=y], simp)
    5.30 +
    5.31 +lemma dist_triangle_half_r:
    5.32 +  shows "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 \<Longrightarrow> dist x1 x2 < e"
    5.33 +by (rule dist_triangle_half_l, simp_all add: dist_commute)
    5.34 +
    5.35  subclass topological_space
    5.36  proof
    5.37    have "\<exists>e::real. 0 < e"
    5.38 @@ -554,6 +582,13 @@
    5.39      unfolding open_dist by fast
    5.40  qed
    5.41  
    5.42 +lemma (in metric_space) open_ball: "open {y. dist x y < d}"
    5.43 +proof (unfold open_dist, intro ballI)
    5.44 +  fix y assume *: "y \<in> {y. dist x y < d}"
    5.45 +  then show "\<exists>e>0. \<forall>z. dist z y < e \<longrightarrow> z \<in> {y. dist x y < d}"
    5.46 +    by (auto intro!: exI[of _ "d - dist x y"] simp: field_simps dist_triangle_lt)
    5.47 +qed
    5.48 +
    5.49  end
    5.50  
    5.51  
    5.52 @@ -1060,4 +1095,78 @@
    5.53  interpretation of_real: bounded_linear "\<lambda>r. of_real r"
    5.54  unfolding of_real_def by (rule scaleR.bounded_linear_left)
    5.55  
    5.56 +subsection{* Hausdorff and other separation properties *}
    5.57 +
    5.58 +class t0_space = topological_space +
    5.59 +  assumes t0_space: "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U)"
    5.60 +
    5.61 +class t1_space = topological_space +
    5.62 +  assumes t1_space: "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> x \<in> U \<and> y \<notin> U"
    5.63 +
    5.64 +instance t1_space \<subseteq> t0_space
    5.65 +proof qed (fast dest: t1_space)
    5.66 +
    5.67 +lemma separation_t1:
    5.68 +  fixes x y :: "'a::t1_space"
    5.69 +  shows "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U)"
    5.70 +  using t1_space[of x y] by blast
    5.71 +
    5.72 +lemma closed_singleton:
    5.73 +  fixes a :: "'a::t1_space"
    5.74 +  shows "closed {a}"
    5.75 +proof -
    5.76 +  let ?T = "\<Union>{S. open S \<and> a \<notin> S}"
    5.77 +  have "open ?T" by (simp add: open_Union)
    5.78 +  also have "?T = - {a}"
    5.79 +    by (simp add: set_eq_iff separation_t1, auto)
    5.80 +  finally show "closed {a}" unfolding closed_def .
    5.81 +qed
    5.82 +
    5.83 +lemma closed_insert [simp]:
    5.84 +  fixes a :: "'a::t1_space"
    5.85 +  assumes "closed S" shows "closed (insert a S)"
    5.86 +proof -
    5.87 +  from closed_singleton assms
    5.88 +  have "closed ({a} \<union> S)" by (rule closed_Un)
    5.89 +  thus "closed (insert a S)" by simp
    5.90 +qed
    5.91 +
    5.92 +lemma finite_imp_closed:
    5.93 +  fixes S :: "'a::t1_space set"
    5.94 +  shows "finite S \<Longrightarrow> closed S"
    5.95 +by (induct set: finite, simp_all)
    5.96 +
    5.97 +text {* T2 spaces are also known as Hausdorff spaces. *}
    5.98 +
    5.99 +class t2_space = topological_space +
   5.100 +  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 = {}"
   5.101 +
   5.102 +instance t2_space \<subseteq> t1_space
   5.103 +proof qed (fast dest: hausdorff)
   5.104 +
   5.105 +instance metric_space \<subseteq> t2_space
   5.106 +proof
   5.107 +  fix x y :: "'a::metric_space"
   5.108 +  assume xy: "x \<noteq> y"
   5.109 +  let ?U = "{y'. dist x y' < dist x y / 2}"
   5.110 +  let ?V = "{x'. dist y x' < dist x y / 2}"
   5.111 +  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
   5.112 +               \<Longrightarrow> \<not>(d x y * 2 < d x z \<and> d z y * 2 < d x z)" by arith
   5.113 +  have "open ?U \<and> open ?V \<and> x \<in> ?U \<and> y \<in> ?V \<and> ?U \<inter> ?V = {}"
   5.114 +    using dist_pos_lt[OF xy] th0[of dist, OF dist_triangle dist_commute]
   5.115 +    using open_ball[of _ "dist x y / 2"] by auto
   5.116 +  then show "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
   5.117 +    by blast
   5.118 +qed
   5.119 +
   5.120 +lemma separation_t2:
   5.121 +  fixes x y :: "'a::t2_space"
   5.122 +  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 = {})"
   5.123 +  using hausdorff[of x y] by blast
   5.124 +
   5.125 +lemma separation_t0:
   5.126 +  fixes x y :: "'a::t0_space"
   5.127 +  shows "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> ~(x\<in>U \<longleftrightarrow> y\<in>U))"
   5.128 +  using t0_space[of x y] by blast
   5.129 +
   5.130  end