author hoelzl Mon Mar 14 14:37:33 2011 +0100 (2011-03-14) changeset 41969 1cf3e4107a2a parent 41966 d65835c381dd child 41970 47d6e13d1710
moved t2_spaces to HOL image
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.5  text{* Hence more metric properties. *}
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.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.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.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.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.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.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.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.102 +instance t2_space \<subseteq> t1_space
5.103 +proof qed (fast dest: hausdorff)
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.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.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.130  end