Many new theorems, and more tidying
authorpaulson <lp15@cam.ac.uk>
Wed Jan 04 16:18:50 2017 +0000 (2017-01-04)
changeset 64773223b2ebdda79
parent 64770 1ddc262514b8
child 64774 8cac34b3dcd0
Many new theorems, and more tidying
src/HOL/Analysis/Cauchy_Integral_Theorem.thy
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/Euclidean_Space.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Homeomorphism.thy
src/HOL/Analysis/Linear_Algebra.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
src/HOL/Complex.thy
src/HOL/Number_Theory/Primes.thy
src/HOL/Set_Interval.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Jan 03 23:21:09 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Wed Jan 04 16:18:50 2017 +0000
     1.3 @@ -3271,165 +3271,6 @@
     1.4    by (force simp: L contour_integral_integral)
     1.5  qed
     1.6  
     1.7 -subsection\<open>Constancy of a function from a connected set into a finite, disconnected or discrete set\<close>
     1.8 -
     1.9 -text\<open>Still missing: versions for a set that is smaller than R, or countable.\<close>
    1.10 -
    1.11 -lemma continuous_disconnected_range_constant:
    1.12 -  assumes s: "connected s"
    1.13 -      and conf: "continuous_on s f"
    1.14 -      and fim: "f ` s \<subseteq> t"
    1.15 -      and cct: "\<And>y. y \<in> t \<Longrightarrow> connected_component_set t y = {y}"
    1.16 -    shows "\<exists>a. \<forall>x \<in> s. f x = a"
    1.17 -proof (cases "s = {}")
    1.18 -  case True then show ?thesis by force
    1.19 -next
    1.20 -  case False
    1.21 -  { fix x assume "x \<in> s"
    1.22 -    then have "f ` s \<subseteq> {f x}"
    1.23 -    by (metis connected_continuous_image conf connected_component_maximal fim image_subset_iff rev_image_eqI s cct)
    1.24 -  }
    1.25 -  with False show ?thesis
    1.26 -    by blast
    1.27 -qed
    1.28 -
    1.29 -lemma discrete_subset_disconnected:
    1.30 -  fixes s :: "'a::topological_space set"
    1.31 -  fixes t :: "'b::real_normed_vector set"
    1.32 -  assumes conf: "continuous_on s f"
    1.33 -      and no: "\<And>x. x \<in> s \<Longrightarrow> \<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)"
    1.34 -   shows "f ` s \<subseteq> {y. connected_component_set (f ` s) y = {y}}"
    1.35 -proof -
    1.36 -  { fix x assume x: "x \<in> s"
    1.37 -    then obtain e where "e>0" and ele: "\<And>y. \<lbrakk>y \<in> s; f y \<noteq> f x\<rbrakk> \<Longrightarrow> e \<le> norm (f y - f x)"
    1.38 -      using conf no [OF x] by auto
    1.39 -    then have e2: "0 \<le> e / 2"
    1.40 -      by simp
    1.41 -    have "f y = f x" if "y \<in> s" and ccs: "f y \<in> connected_component_set (f ` s) (f x)" for y
    1.42 -      apply (rule ccontr)
    1.43 -      using connected_closed [of "connected_component_set (f ` s) (f x)"] \<open>e>0\<close>
    1.44 -      apply (simp add: del: ex_simps)
    1.45 -      apply (drule spec [where x="cball (f x) (e / 2)"])
    1.46 -      apply (drule spec [where x="- ball(f x) e"])
    1.47 -      apply (auto simp: dist_norm open_closed [symmetric] simp del: le_divide_eq_numeral1 dest!: connected_component_in)
    1.48 -        apply (metis diff_self e2 ele norm_minus_commute norm_zero not_less)
    1.49 -       using centre_in_cball connected_component_refl_eq e2 x apply blast
    1.50 -      using ccs
    1.51 -      apply (force simp: cball_def dist_norm norm_minus_commute dest: ele [OF \<open>y \<in> s\<close>])
    1.52 -      done
    1.53 -    moreover have "connected_component_set (f ` s) (f x) \<subseteq> f ` s"
    1.54 -      by (auto simp: connected_component_in)
    1.55 -    ultimately have "connected_component_set (f ` s) (f x) = {f x}"
    1.56 -      by (auto simp: x)
    1.57 -  }
    1.58 -  with assms show ?thesis
    1.59 -    by blast
    1.60 -qed
    1.61 -
    1.62 -lemma finite_implies_discrete:
    1.63 -  fixes s :: "'a::topological_space set"
    1.64 -  assumes "finite (f ` s)"
    1.65 -  shows "(\<forall>x \<in> s. \<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x))"
    1.66 -proof -
    1.67 -  have "\<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)" if "x \<in> s" for x
    1.68 -  proof (cases "f ` s - {f x} = {}")
    1.69 -    case True
    1.70 -    with zero_less_numeral show ?thesis
    1.71 -      by (fastforce simp add: Set.image_subset_iff cong: conj_cong)
    1.72 -  next
    1.73 -    case False
    1.74 -    then obtain z where z: "z \<in> s" "f z \<noteq> f x"
    1.75 -      by blast
    1.76 -    have finn: "finite {norm (z - f x) |z. z \<in> f ` s - {f x}}"
    1.77 -      using assms by simp
    1.78 -    then have *: "0 < Inf{norm(z - f x) | z. z \<in> f ` s - {f x}}"
    1.79 -      apply (rule finite_imp_less_Inf)
    1.80 -      using z apply force+
    1.81 -      done
    1.82 -    show ?thesis
    1.83 -      by (force intro!: * cInf_le_finite [OF finn])
    1.84 -  qed
    1.85 -  with assms show ?thesis
    1.86 -    by blast
    1.87 -qed
    1.88 -
    1.89 -text\<open>This proof requires the existence of two separate values of the range type.\<close>
    1.90 -lemma finite_range_constant_imp_connected:
    1.91 -  assumes "\<And>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
    1.92 -              \<lbrakk>continuous_on s f; finite(f ` s)\<rbrakk> \<Longrightarrow> \<exists>a. \<forall>x \<in> s. f x = a"
    1.93 -    shows "connected s"
    1.94 -proof -
    1.95 -  { fix t u
    1.96 -    assume clt: "closedin (subtopology euclidean s) t"
    1.97 -       and clu: "closedin (subtopology euclidean s) u"
    1.98 -       and tue: "t \<inter> u = {}" and tus: "t \<union> u = s"
    1.99 -    have conif: "continuous_on s (\<lambda>x. if x \<in> t then 0 else 1)"
   1.100 -      apply (subst tus [symmetric])
   1.101 -      apply (rule continuous_on_cases_local)
   1.102 -      using clt clu tue
   1.103 -      apply (auto simp: tus continuous_on_const)
   1.104 -      done
   1.105 -    have fi: "finite ((\<lambda>x. if x \<in> t then 0 else 1) ` s)"
   1.106 -      by (rule finite_subset [of _ "{0,1}"]) auto
   1.107 -    have "t = {} \<or> u = {}"
   1.108 -      using assms [OF conif fi] tus [symmetric]
   1.109 -      by (auto simp: Ball_def) (metis IntI empty_iff one_neq_zero tue)
   1.110 -  }
   1.111 -  then show ?thesis
   1.112 -    by (simp add: connected_closedin_eq)
   1.113 -qed
   1.114 -
   1.115 -lemma continuous_disconnected_range_constant_eq:
   1.116 -      "(connected s \<longleftrightarrow>
   1.117 -           (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
   1.118 -            \<forall>t. continuous_on s f \<and> f ` s \<subseteq> t \<and> (\<forall>y \<in> t. connected_component_set t y = {y})
   1.119 -            \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> s. f x = a)))" (is ?thesis1)
   1.120 -  and continuous_discrete_range_constant_eq:
   1.121 -      "(connected s \<longleftrightarrow>
   1.122 -         (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
   1.123 -          continuous_on s f \<and>
   1.124 -          (\<forall>x \<in> s. \<exists>e. 0 < e \<and> (\<forall>y. y \<in> s \<and> (f y \<noteq> f x) \<longrightarrow> e \<le> norm(f y - f x)))
   1.125 -          \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> s. f x = a)))" (is ?thesis2)
   1.126 -  and continuous_finite_range_constant_eq:
   1.127 -      "(connected s \<longleftrightarrow>
   1.128 -         (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
   1.129 -          continuous_on s f \<and> finite (f ` s)
   1.130 -          \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> s. f x = a)))" (is ?thesis3)
   1.131 -proof -
   1.132 -  have *: "\<And>s t u v. \<lbrakk>s \<Longrightarrow> t; t \<Longrightarrow> u; u \<Longrightarrow> v; v \<Longrightarrow> s\<rbrakk>
   1.133 -    \<Longrightarrow> (s \<longleftrightarrow> t) \<and> (s \<longleftrightarrow> u) \<and> (s \<longleftrightarrow> v)"
   1.134 -    by blast
   1.135 -  have "?thesis1 \<and> ?thesis2 \<and> ?thesis3"
   1.136 -    apply (rule *)
   1.137 -    using continuous_disconnected_range_constant apply metis
   1.138 -    apply clarify
   1.139 -    apply (frule discrete_subset_disconnected; blast)
   1.140 -    apply (blast dest: finite_implies_discrete)
   1.141 -    apply (blast intro!: finite_range_constant_imp_connected)
   1.142 -    done
   1.143 -  then show ?thesis1 ?thesis2 ?thesis3
   1.144 -    by blast+
   1.145 -qed
   1.146 -
   1.147 -lemma continuous_discrete_range_constant:
   1.148 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1"
   1.149 -  assumes s: "connected s"
   1.150 -      and "continuous_on s f"
   1.151 -      and "\<And>x. x \<in> s \<Longrightarrow> \<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)"
   1.152 -    shows "\<exists>a. \<forall>x \<in> s. f x = a"
   1.153 -  using continuous_discrete_range_constant_eq [THEN iffD1, OF s] assms
   1.154 -  by blast
   1.155 -
   1.156 -lemma continuous_finite_range_constant:
   1.157 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1"
   1.158 -  assumes "connected s"
   1.159 -      and "continuous_on s f"
   1.160 -      and "finite (f ` s)"
   1.161 -    shows "\<exists>a. \<forall>x \<in> s. f x = a"
   1.162 -  using assms continuous_finite_range_constant_eq
   1.163 -  by blast
   1.164 -
   1.165 -
   1.166  text\<open>We can treat even non-rectifiable paths as having a "length" for bounds on analytic functions in open sets.\<close>
   1.167  
   1.168  subsection\<open>Winding Numbers\<close>
     2.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Jan 03 23:21:09 2017 +0100
     2.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Wed Jan 04 16:18:50 2017 +0000
     2.3 @@ -6,6 +6,7 @@
     2.4  imports
     2.5    Complex_Analysis_Basics
     2.6    Summation_Tests
     2.7 +   "~~/src/HOL/Library/Periodic_Fun"
     2.8  begin
     2.9  
    2.10  (* TODO: Figure out what to do with Möbius transformations *)
    2.11 @@ -400,6 +401,89 @@
    2.12    apply (simp add: real_sqrt_mult)
    2.13    done
    2.14  
    2.15 +
    2.16 +lemma complex_sin_eq:
    2.17 +  fixes w :: complex
    2.18 +  shows "sin w = sin z \<longleftrightarrow> (\<exists>n \<in> \<int>. w = z + of_real(2*n*pi) \<or> w = -z + of_real((2*n + 1)*pi))"
    2.19 +        (is "?lhs = ?rhs")
    2.20 +proof
    2.21 +  assume ?lhs
    2.22 +  then have "sin w - sin z = 0"
    2.23 +    by (auto simp: algebra_simps)
    2.24 +  then have "sin ((w - z) / 2)*cos ((w + z) / 2) = 0"
    2.25 +    by (auto simp: sin_diff_sin)
    2.26 +  then consider "sin ((w - z) / 2) = 0" | "cos ((w + z) / 2) = 0"
    2.27 +    using mult_eq_0_iff by blast
    2.28 +  then show ?rhs
    2.29 +  proof cases
    2.30 +    case 1
    2.31 +    then show ?thesis
    2.32 +      apply (auto simp: sin_eq_0 algebra_simps)
    2.33 +      by (metis Ints_of_int of_real_of_int_eq)
    2.34 +  next
    2.35 +    case 2
    2.36 +    then show ?thesis
    2.37 +      apply (auto simp: cos_eq_0 algebra_simps)
    2.38 +      by (metis Ints_of_int of_real_of_int_eq)
    2.39 +  qed
    2.40 +next
    2.41 +  assume ?rhs
    2.42 +  then obtain n::int where w: "w = z + of_real (2* of_int n*pi) \<or>
    2.43 +                               w = -z + of_real ((2* of_int n + 1)*pi)"
    2.44 +    using Ints_cases by blast
    2.45 +  then show ?lhs
    2.46 +    using Periodic_Fun.sin.plus_of_int [of z n]
    2.47 +    apply (auto simp: algebra_simps)
    2.48 +    by (metis (no_types, hide_lams) add_diff_cancel_left add_diff_cancel_left' add_minus_cancel
    2.49 +              mult.commute sin.plus_of_int sin_minus sin_plus_pi)
    2.50 +qed
    2.51 +
    2.52 +lemma complex_cos_eq:
    2.53 +  fixes w :: complex
    2.54 +  shows "cos w = cos z \<longleftrightarrow>
    2.55 +         (\<exists>n \<in> \<int>. w = z + of_real(2*n*pi) \<or> w = -z + of_real(2*n*pi))"
    2.56 +        (is "?lhs = ?rhs")
    2.57 +proof
    2.58 +  assume ?lhs
    2.59 +  then have "cos w - cos z = 0"
    2.60 +    by (auto simp: algebra_simps)
    2.61 +  then have "sin ((w + z) / 2) * sin ((z - w) / 2) = 0"
    2.62 +    by (auto simp: cos_diff_cos)
    2.63 +  then consider "sin ((w + z) / 2) = 0" | "sin ((z - w) / 2) = 0"
    2.64 +    using mult_eq_0_iff by blast
    2.65 +  then show ?rhs
    2.66 +  proof cases
    2.67 +    case 1
    2.68 +    then show ?thesis
    2.69 +      apply (auto simp: sin_eq_0 algebra_simps)
    2.70 +      by (metis Ints_of_int of_real_of_int_eq)
    2.71 +  next
    2.72 +    case 2
    2.73 +    then show ?thesis
    2.74 +      apply (auto simp: sin_eq_0 algebra_simps)
    2.75 +      by (metis Ints_of_int add_minus_cancel distrib_right mult_of_int_commute mult_zero_right of_int_0 of_int_add of_real_of_int_eq)
    2.76 +  qed
    2.77 +next
    2.78 +  assume ?rhs
    2.79 +  then obtain n::int where w: "w = z + of_real (2* of_int n*pi) \<or>
    2.80 +                               w = -z + of_real(2*n*pi)"
    2.81 +    using Ints_cases  by (metis of_int_mult of_int_numeral)
    2.82 +  then show ?lhs
    2.83 +    using Periodic_Fun.cos.plus_of_int [of z n]
    2.84 +    apply (auto simp: algebra_simps)
    2.85 +    by (metis cos.plus_of_int cos_minus minus_add_cancel mult.commute)
    2.86 +qed
    2.87 +
    2.88 +lemma sin_eq:
    2.89 +   "sin x = sin y \<longleftrightarrow> (\<exists>n \<in> \<int>. x = y + 2*n*pi \<or> x = -y + (2*n + 1)*pi)"
    2.90 +  using complex_sin_eq [of x y]
    2.91 +  by (simp only: sin_of_real Re_complex_of_real of_real_add [symmetric] of_real_minus [symmetric] of_real_mult [symmetric] of_real_eq_iff)
    2.92 +
    2.93 +lemma cos_eq:
    2.94 +   "cos x = cos y \<longleftrightarrow> (\<exists>n \<in> \<int>. x = y + 2*n*pi \<or> x = -y + 2*n*pi)"
    2.95 +  using complex_cos_eq [of x y]
    2.96 +  by (simp only: cos_of_real Re_complex_of_real of_real_add [symmetric] of_real_minus [symmetric] of_real_mult [symmetric] of_real_eq_iff)
    2.97 +
    2.98  lemma sinh_complex:
    2.99    fixes z :: complex
   2.100    shows "(exp z - inverse (exp z)) / 2 = -\<i> * sin(\<i> * z)"
   2.101 @@ -2837,6 +2921,19 @@
   2.102  lemma Re_Arccos_bound: "\<bar>Re(Arccos z)\<bar> \<le> pi"
   2.103    by (meson Re_Arccos_bounds abs_le_iff less_eq_real_def minus_less_iff)
   2.104  
   2.105 +lemma Im_Arccos_bound: "\<bar>Im (Arccos w)\<bar> \<le> cmod w"
   2.106 +proof -
   2.107 +  have "(Im (Arccos w))\<^sup>2 \<le> (cmod (cos (Arccos w)))\<^sup>2 - (cos (Re (Arccos w)))\<^sup>2"
   2.108 +    using norm_cos_squared [of "Arccos w"] real_le_abs_sinh [of "Im (Arccos w)"]
   2.109 +    apply (simp only: abs_le_square_iff)
   2.110 +    apply (simp add: divide_simps)
   2.111 +    done
   2.112 +  also have "... \<le> (cmod w)\<^sup>2"
   2.113 +    by (auto simp: cmod_power2)
   2.114 +  finally show ?thesis
   2.115 +    using abs_le_square_iff by force 
   2.116 +qed
   2.117 +  
   2.118  lemma Re_Arcsin_bounds: "-pi < Re(Arcsin z) & Re(Arcsin z) \<le> pi"
   2.119    unfolding Re_Arcsin
   2.120    by (blast intro!: mpi_less_Im_Ln Im_Ln_le_pi Arcsin_body_lemma)
   2.121 @@ -2844,6 +2941,21 @@
   2.122  lemma Re_Arcsin_bound: "\<bar>Re(Arcsin z)\<bar> \<le> pi"
   2.123    by (meson Re_Arcsin_bounds abs_le_iff less_eq_real_def minus_less_iff)
   2.124  
   2.125 +lemma norm_Arccos_bounded:
   2.126 +  fixes w :: complex
   2.127 +  shows "norm (Arccos w) \<le> pi + norm w"
   2.128 +proof -
   2.129 +  have Re: "(Re (Arccos w))\<^sup>2 \<le> pi\<^sup>2" "(Im (Arccos w))\<^sup>2 \<le> (cmod w)\<^sup>2"
   2.130 +    using Re_Arccos_bound [of w] Im_Arccos_bound [of w] abs_le_square_iff by force+
   2.131 +  have "Arccos w \<bullet> Arccos w \<le> pi\<^sup>2 + (cmod w)\<^sup>2"
   2.132 +    using Re by (simp add: dot_square_norm cmod_power2 [of "Arccos w"])
   2.133 +  then have "cmod (Arccos w) \<le> pi + cmod (cos (Arccos w))"
   2.134 +    apply (simp add: norm_le_square)
   2.135 +    by (metis dot_square_norm norm_ge_zero norm_le_square pi_ge_zero triangle_lemma)
   2.136 +  then show "cmod (Arccos w) \<le> pi + cmod w"
   2.137 +    by auto
   2.138 +qed
   2.139 +
   2.140  
   2.141  subsection\<open>Interrelations between Arcsin and Arccos\<close>
   2.142  
     3.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Jan 03 23:21:09 2017 +0100
     3.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Wed Jan 04 16:18:50 2017 +0000
     3.3 @@ -14,6 +14,20 @@
     3.4    "~~/src/HOL/Library/Set_Algebras"
     3.5  begin
     3.6  
     3.7 +lemma swap_continuous: (*move to Topological_Spaces?*)
     3.8 +  assumes "continuous_on (cbox (a,c) (b,d)) (\<lambda>(x,y). f x y)"
     3.9 +    shows "continuous_on (cbox (c,a) (d,b)) (\<lambda>(x, y). f y x)"
    3.10 +proof -
    3.11 +  have "(\<lambda>(x, y). f y x) = (\<lambda>(x, y). f x y) \<circ> prod.swap"
    3.12 +    by auto
    3.13 +  then show ?thesis
    3.14 +    apply (rule ssubst)
    3.15 +    apply (rule continuous_on_compose)
    3.16 +    apply (simp add: split_def)
    3.17 +    apply (rule continuous_intros | simp add: assms)+
    3.18 +    done
    3.19 +qed
    3.20 +
    3.21  lemma dim_image_eq:
    3.22    fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
    3.23    assumes lf: "linear f"
    3.24 @@ -4651,7 +4665,7 @@
    3.25    ultimately show ?thesis by auto
    3.26  qed
    3.27  
    3.28 -lemma interior_atLeastAtMost_real: "interior {a..b} = {a<..<b :: real}"
    3.29 +lemma interior_atLeastAtMost_real [simp]: "interior {a..b} = {a<..<b :: real}"
    3.30  proof-
    3.31    have "{a..b} = {a..} \<inter> {..b}" by auto
    3.32    also have "interior ... = {a<..} \<inter> {..<b}"
    3.33 @@ -4660,12 +4674,15 @@
    3.34    finally show ?thesis .
    3.35  qed
    3.36  
    3.37 -lemma frontier_real_Iic:
    3.38 +lemma interior_greaterThanLessThan_real [simp]: "interior {a<..<b} = {a<..<b :: real}"
    3.39 +  by (metis interior_atLeastAtMost_real interior_interior)
    3.40 +
    3.41 +lemma frontier_real_Iic [simp]:
    3.42    fixes a :: real
    3.43    shows "frontier {..a} = {a}"
    3.44    unfolding frontier_def by (auto simp add: interior_real_semiline')
    3.45  
    3.46 -lemma rel_interior_real_box:
    3.47 +lemma rel_interior_real_box [simp]:
    3.48    fixes a b :: real
    3.49    assumes "a < b"
    3.50    shows "rel_interior {a .. b} = {a <..< b}"
    3.51 @@ -4679,7 +4696,7 @@
    3.52      by (simp split: if_split_asm del: box_real add: box_real[symmetric] interior_cbox)
    3.53  qed
    3.54  
    3.55 -lemma rel_interior_real_semiline:
    3.56 +lemma rel_interior_real_semiline [simp]:
    3.57    fixes a :: real
    3.58    shows "rel_interior {a..} = {a<..}"
    3.59  proof -
    3.60 @@ -6596,7 +6613,7 @@
    3.61    apply rule
    3.62    apply rule
    3.63    apply (erule conjE)
    3.64 -  apply (rule ccontr)
    3.65 +  apply (rule ccontr)       
    3.66  proof -
    3.67    fix a b x
    3.68    assume as: "connected s" "a \<in> s" "b \<in> s" "a \<le> x" "x \<le> b" "x \<notin> s"
    3.69 @@ -6630,6 +6647,10 @@
    3.70    shows "is_interval s \<longleftrightarrow> convex s"
    3.71    by (metis is_interval_convex convex_connected is_interval_connected_1)
    3.72  
    3.73 +lemma connected_compact_interval_1:
    3.74 +     "connected S \<and> compact S \<longleftrightarrow> (\<exists>a b. S = {a..b::real})"
    3.75 +  by (auto simp: is_interval_connected_1 [symmetric] is_interval_compact)
    3.76 +
    3.77  lemma connected_convex_1:
    3.78    fixes s :: "real set"
    3.79    shows "connected s \<longleftrightarrow> convex s"
    3.80 @@ -7315,6 +7336,12 @@
    3.81      unfolding midpoint_def scaleR_2 [symmetric] by simp
    3.82  qed
    3.83  
    3.84 +lemma
    3.85 +  fixes a::real
    3.86 +  assumes "a \<le> b" shows ge_midpoint_1: "a \<le> midpoint a b"
    3.87 +                    and le_midpoint_1: "midpoint a b \<le> b"
    3.88 +  by (simp_all add: midpoint_def assms)
    3.89 +
    3.90  lemma dist_midpoint:
    3.91    fixes a b :: "'a::real_normed_vector" shows
    3.92    "dist a (midpoint a b) = (dist a b) / 2" (is ?t1)
    3.93 @@ -7535,7 +7562,7 @@
    3.94    proof -
    3.95      have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)"
    3.96        using \<open>u \<le> 1\<close> by force
    3.97 -    then show ?thesis
    3.98 +    then show ?thesis                     
    3.99        by (simp add: dist_norm real_vector.scale_right_diff_distrib)
   3.100    qed
   3.101    also have "... \<le> dist a b"
   3.102 @@ -7639,6 +7666,19 @@
   3.103    shows "a \<noteq> b \<Longrightarrow> a \<notin> closed_segment (midpoint a b) b"
   3.104  by (auto simp: dist_midpoint dest!: dist_in_closed_segment)
   3.105  
   3.106 +lemma segment_to_closest_point:
   3.107 +  fixes S :: "'a :: euclidean_space set"
   3.108 +  shows "\<lbrakk>closed S; S \<noteq> {}\<rbrakk> \<Longrightarrow> open_segment a (closest_point S a) \<inter> S = {}"
   3.109 +  apply (subst disjoint_iff_not_equal)
   3.110 +  apply (clarify dest!: dist_in_open_segment)
   3.111 +  by (metis closest_point_le dist_commute le_less_trans less_irrefl)
   3.112 +
   3.113 +lemma segment_to_point_exists:
   3.114 +  fixes S :: "'a :: euclidean_space set"
   3.115 +    assumes "closed S" "S \<noteq> {}"
   3.116 +    obtains b where "b \<in> S" "open_segment a b \<inter> S = {}"
   3.117 +  by (metis assms segment_to_closest_point closest_point_exists that)
   3.118 +
   3.119  subsubsection\<open>More lemmas, especially for working with the underlying formula\<close>
   3.120  
   3.121  lemma segment_eq_compose:
   3.122 @@ -8243,6 +8283,71 @@
   3.123    finally show "(1 - u) *\<^sub>R a + u *\<^sub>R b \<in> interior S" .
   3.124  qed
   3.125  
   3.126 +lemma closure_open_Int_superset:
   3.127 +  assumes "open S" "S \<subseteq> closure T"
   3.128 +  shows "closure(S \<inter> T) = closure S"
   3.129 +proof -
   3.130 +  have "closure S \<subseteq> closure(S \<inter> T)"
   3.131 +    by (metis assms closed_closure closure_minimal inf.orderE open_Int_closure_subset)
   3.132 +  then show ?thesis
   3.133 +    by (simp add: closure_mono dual_order.antisym)
   3.134 +qed
   3.135 +
   3.136 +lemma convex_closure_interior:
   3.137 +  fixes S :: "'a::euclidean_space set"
   3.138 +  assumes "convex S" and int: "interior S \<noteq> {}"
   3.139 +  shows "closure(interior S) = closure S"
   3.140 +proof -
   3.141 +  obtain a where a: "a \<in> interior S"
   3.142 +    using int by auto
   3.143 +  have "closure S \<subseteq> closure(interior S)"
   3.144 +  proof
   3.145 +    fix x
   3.146 +    assume x: "x \<in> closure S"
   3.147 +    show "x \<in> closure (interior S)"
   3.148 +    proof (cases "x=a")
   3.149 +      case True
   3.150 +      then show ?thesis
   3.151 +        using \<open>a \<in> interior S\<close> closure_subset by blast
   3.152 +    next
   3.153 +      case False
   3.154 +      show ?thesis
   3.155 +      proof (clarsimp simp add: closure_def islimpt_approachable)
   3.156 +        fix e::real
   3.157 +        assume xnotS: "x \<notin> interior S" and "0 < e"
   3.158 +        show "\<exists>x'\<in>interior S. x' \<noteq> x \<and> dist x' x < e"
   3.159 +        proof (intro bexI conjI)
   3.160 +          show "x - min (e/2 / norm (x - a)) 1 *\<^sub>R (x - a) \<noteq> x"
   3.161 +            using False \<open>0 < e\<close> by (auto simp: algebra_simps min_def)
   3.162 +          show "dist (x - min (e/2 / norm (x - a)) 1 *\<^sub>R (x - a)) x < e"
   3.163 +            using \<open>0 < e\<close> by (auto simp: dist_norm min_def)
   3.164 +          show "x - min (e/2 / norm (x - a)) 1 *\<^sub>R (x - a) \<in> interior S"
   3.165 +            apply (clarsimp simp add: min_def a)
   3.166 +            apply (rule mem_interior_closure_convex_shrink [OF \<open>convex S\<close> a x])
   3.167 +            using \<open>0 < e\<close> False apply (auto simp: divide_simps)
   3.168 +            done
   3.169 +        qed
   3.170 +      qed
   3.171 +    qed
   3.172 +  qed
   3.173 +  then show ?thesis
   3.174 +    by (simp add: closure_mono interior_subset subset_antisym)
   3.175 +qed
   3.176 +
   3.177 +lemma closure_convex_Int_superset:
   3.178 +  fixes S :: "'a::euclidean_space set"
   3.179 +  assumes "convex S" "interior S \<noteq> {}" "interior S \<subseteq> closure T"
   3.180 +  shows "closure(S \<inter> T) = closure S"
   3.181 +proof -
   3.182 +  have "closure S \<subseteq> closure(interior S)"
   3.183 +    by (simp add: convex_closure_interior assms)
   3.184 +  also have "... \<subseteq> closure (S \<inter> T)"
   3.185 +    using interior_subset [of S] assms
   3.186 +    by (metis (no_types, lifting) Int_assoc Int_lower2 closure_mono closure_open_Int_superset inf.orderE open_interior)
   3.187 +  finally show ?thesis
   3.188 +    by (simp add: closure_mono dual_order.antisym)
   3.189 +qed
   3.190 +
   3.191  
   3.192  subsection \<open>Some obvious but surprisingly hard simplex lemmas\<close>
   3.193  
   3.194 @@ -14406,4 +14511,78 @@
   3.195  using paracompact_closedin [of UNIV S \<C>] assms
   3.196  by (auto simp: open_openin [symmetric] closed_closedin [symmetric])
   3.197  
   3.198 +  
   3.199 +subsection\<open>Closed-graph characterization of continuity\<close>
   3.200 +
   3.201 +lemma continuous_closed_graph_gen:
   3.202 +  fixes T :: "'b::real_normed_vector set"
   3.203 +  assumes contf: "continuous_on S f" and fim: "f ` S \<subseteq> T"
   3.204 +    shows "closedin (subtopology euclidean (S \<times> T)) ((\<lambda>x. Pair x (f x)) ` S)"
   3.205 +proof -
   3.206 +  have eq: "((\<lambda>x. Pair x (f x)) ` S) = {z. z \<in> S \<times> T \<and> (f \<circ> fst)z - snd z \<in> {0}}"
   3.207 +    using fim by auto
   3.208 +  show ?thesis
   3.209 +    apply (subst eq)
   3.210 +    apply (intro continuous_intros continuous_closedin_preimage continuous_on_subset [OF contf])
   3.211 +    by auto
   3.212 +qed
   3.213 +
   3.214 +lemma continuous_closed_graph_eq:
   3.215 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   3.216 +  assumes "compact T" and fim: "f ` S \<subseteq> T"
   3.217 +  shows "continuous_on S f \<longleftrightarrow>
   3.218 +         closedin (subtopology euclidean (S \<times> T)) ((\<lambda>x. Pair x (f x)) ` S)"
   3.219 +         (is "?lhs = ?rhs")
   3.220 +proof -
   3.221 +  have "?lhs" if ?rhs
   3.222 +  proof (clarsimp simp add: continuous_on_closed_gen [OF fim])
   3.223 +    fix U
   3.224 +    assume U: "closedin (subtopology euclidean T) U"
   3.225 +    have eq: "{x. x \<in> S \<and> f x \<in> U} = fst ` (((\<lambda>x. Pair x (f x)) ` S) \<inter> (S \<times> U))"
   3.226 +      by (force simp: image_iff)
   3.227 +    show "closedin (subtopology euclidean S) {x \<in> S. f x \<in> U}"
   3.228 +      by (simp add: U closedin_Int closedin_Times closed_map_fst [OF \<open>compact T\<close>] that eq)
   3.229 +  qed
   3.230 +  with continuous_closed_graph_gen assms show ?thesis by blast
   3.231 +qed
   3.232 +
   3.233 +lemma continuous_closed_graph:
   3.234 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   3.235 +  assumes "closed S" and contf: "continuous_on S f"
   3.236 +  shows "closed ((\<lambda>x. Pair x (f x)) ` S)"
   3.237 +  apply (rule closedin_closed_trans)
   3.238 +   apply (rule continuous_closed_graph_gen [OF contf subset_UNIV])
   3.239 +  by (simp add: \<open>closed S\<close> closed_Times)
   3.240 +
   3.241 +lemma continuous_from_closed_graph:
   3.242 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   3.243 +  assumes "compact T" and fim: "f ` S \<subseteq> T" and clo: "closed ((\<lambda>x. Pair x (f x)) ` S)"
   3.244 +  shows "continuous_on S f"
   3.245 +    using fim clo
   3.246 +    by (auto intro: closed_subset simp: continuous_closed_graph_eq [OF \<open>compact T\<close> fim])
   3.247 +
   3.248 +lemma continuous_on_Un_local_open:
   3.249 +  assumes opS: "openin (subtopology euclidean (S \<union> T)) S"
   3.250 +      and opT: "openin (subtopology euclidean (S \<union> T)) T"
   3.251 +      and contf: "continuous_on S f" and contg: "continuous_on T f"
   3.252 +    shows "continuous_on (S \<union> T) f"
   3.253 +using pasting_lemma [of "{S,T}" "S \<union> T" "\<lambda>i. i" "\<lambda>i. f" f] contf contg opS opT by blast
   3.254 +
   3.255 +lemma continuous_on_cases_local_open:
   3.256 +  assumes opS: "openin (subtopology euclidean (S \<union> T)) S"
   3.257 +      and opT: "openin (subtopology euclidean (S \<union> T)) T"
   3.258 +      and contf: "continuous_on S f" and contg: "continuous_on T g"
   3.259 +      and fg: "\<And>x. x \<in> S \<and> ~P x \<or> x \<in> T \<and> P x \<Longrightarrow> f x = g x"
   3.260 +    shows "continuous_on (S \<union> T) (\<lambda>x. if P x then f x else g x)"
   3.261 +proof -
   3.262 +  have "\<And>x. x \<in> S \<Longrightarrow> (if P x then f x else g x) = f x"  "\<And>x. x \<in> T \<Longrightarrow> (if P x then f x else g x) = g x"
   3.263 +    by (simp_all add: fg)
   3.264 +  then have "continuous_on S (\<lambda>x. if P x then f x else g x)" "continuous_on T (\<lambda>x. if P x then f x else g x)"
   3.265 +    by (simp_all add: contf contg cong: continuous_on_cong)
   3.266 +  then show ?thesis
   3.267 +    by (rule continuous_on_Un_local_open [OF opS opT])
   3.268 +qed
   3.269 +
   3.270 +
   3.271 +  
   3.272  end
     4.1 --- a/src/HOL/Analysis/Euclidean_Space.thy	Tue Jan 03 23:21:09 2017 +0100
     4.2 +++ b/src/HOL/Analysis/Euclidean_Space.thy	Wed Jan 04 16:18:50 2017 +0000
     4.3 @@ -53,6 +53,9 @@
     4.4  lemma (in euclidean_space) SOME_Basis: "(SOME i. i \<in> Basis) \<in> Basis"
     4.5    by (metis ex_in_conv nonempty_Basis someI_ex)
     4.6  
     4.7 +lemma norm_some_Basis [simp]: "norm (SOME i. i \<in> Basis) = 1"
     4.8 +  by (simp add: SOME_Basis)
     4.9 +
    4.10  lemma (in euclidean_space) inner_sum_left_Basis[simp]:
    4.11      "b \<in> Basis \<Longrightarrow> inner (\<Sum>i\<in>Basis. f i *\<^sub>R i) b = f b"
    4.12    by (simp add: inner_sum_left inner_Basis if_distrib comm_monoid_add_class.sum.If_cases)
     5.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Jan 03 23:21:09 2017 +0100
     5.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Jan 04 16:18:50 2017 +0000
     5.3 @@ -10,21 +10,6 @@
     5.4  begin
     5.5  
     5.6  (* BEGIN MOVE *)
     5.7 -lemma swap_continuous:
     5.8 -  assumes "continuous_on (cbox (a,c) (b,d)) (\<lambda>(x,y). f x y)"
     5.9 -    shows "continuous_on (cbox (c,a) (d,b)) (\<lambda>(x, y). f y x)"
    5.10 -proof -
    5.11 -  have "(\<lambda>(x, y). f y x) = (\<lambda>(x, y). f x y) \<circ> prod.swap"
    5.12 -    by auto
    5.13 -  then show ?thesis
    5.14 -    apply (rule ssubst)
    5.15 -    apply (rule continuous_on_compose)
    5.16 -    apply (simp add: split_def)
    5.17 -    apply (rule continuous_intros | simp add: assms)+
    5.18 -    done
    5.19 -qed
    5.20 -
    5.21 -
    5.22  lemma norm_minus2: "norm (x1-x2, y1-y2) = norm (x2-x1, y2-y1)"
    5.23    by (simp add: norm_minus_eqI)
    5.24  
    5.25 @@ -44,10 +29,6 @@
    5.26  
    5.27  lemma Sigma_Int_Paircomp2: "(Sigma A B) \<inter> {(x, y). P y} = Sigma A (\<lambda>z. B z \<inter> {y. P y})"
    5.28    by blast
    5.29 -
    5.30 -lemma empty_as_interval: "{} = cbox One (0::'a::euclidean_space)"
    5.31 -  using nonempty_Basis
    5.32 -  by (fastforce simp add: set_eq_iff mem_box)
    5.33  (* END MOVE *)
    5.34  
    5.35  subsection \<open>Content (length, area, volume...) of an interval.\<close>
    5.36 @@ -6191,7 +6172,6 @@
    5.37        apply (rule le_less_trans[of _ "sum (\<lambda>x. k / (real (card r) + 1)) r"])
    5.38        unfolding sum_subtractf[symmetric]
    5.39        apply (rule sum_norm_le)
    5.40 -      apply rule
    5.41        apply (drule qq)
    5.42        defer
    5.43        unfolding divide_inverse sum_distrib_right[symmetric]
    5.44 @@ -6536,7 +6516,7 @@
    5.45              m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x))) < e / 2"
    5.46              apply (rule le_less_trans[of _ "sum (\<lambda>i. e / 2^(i+2)) {0..s}"])
    5.47              apply (rule sum_norm_le)
    5.48 -          proof
    5.49 +          proof -
    5.50              show "(\<Sum>i = 0..s. e / 2 ^ (i + 2)) < e / 2"
    5.51                unfolding power_add divide_inverse inverse_mult_distrib
    5.52                unfolding sum_distrib_left[symmetric] sum_distrib_right[symmetric]
     6.1 --- a/src/HOL/Analysis/Homeomorphism.thy	Tue Jan 03 23:21:09 2017 +0100
     6.2 +++ b/src/HOL/Analysis/Homeomorphism.thy	Wed Jan 04 16:18:50 2017 +0000
     6.3 @@ -1112,19 +1112,19 @@
     6.4  
     6.5  
     6.6  lemma homeomorphic_convex_compact_lemma:
     6.7 -  fixes s :: "'a::euclidean_space set"
     6.8 -  assumes "convex s"
     6.9 -    and "compact s"
    6.10 -    and "cball 0 1 \<subseteq> s"
    6.11 -  shows "s homeomorphic (cball (0::'a) 1)"
    6.12 +  fixes S :: "'a::euclidean_space set"
    6.13 +  assumes "convex S"
    6.14 +    and "compact S"
    6.15 +    and "cball 0 1 \<subseteq> S"
    6.16 +  shows "S homeomorphic (cball (0::'a) 1)"
    6.17  proof (rule starlike_compact_projective_special[OF assms(2-3)])
    6.18    fix x u
    6.19 -  assume "x \<in> s" and "0 \<le> u" and "u < (1::real)"
    6.20 +  assume "x \<in> S" and "0 \<le> u" and "u < (1::real)"
    6.21    have "open (ball (u *\<^sub>R x) (1 - u))"
    6.22      by (rule open_ball)
    6.23    moreover have "u *\<^sub>R x \<in> ball (u *\<^sub>R x) (1 - u)"
    6.24      unfolding centre_in_ball using \<open>u < 1\<close> by simp
    6.25 -  moreover have "ball (u *\<^sub>R x) (1 - u) \<subseteq> s"
    6.26 +  moreover have "ball (u *\<^sub>R x) (1 - u) \<subseteq> S"
    6.27    proof
    6.28      fix y
    6.29      assume "y \<in> ball (u *\<^sub>R x) (1 - u)"
    6.30 @@ -1132,32 +1132,32 @@
    6.31        unfolding mem_ball .
    6.32      with \<open>u < 1\<close> have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> cball 0 1"
    6.33        by (simp add: dist_norm inverse_eq_divide norm_minus_commute)
    6.34 -    with assms(3) have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> s" ..
    6.35 -    with assms(1) have "(1 - u) *\<^sub>R ((y - u *\<^sub>R x) /\<^sub>R (1 - u)) + u *\<^sub>R x \<in> s"
    6.36 -      using \<open>x \<in> s\<close> \<open>0 \<le> u\<close> \<open>u < 1\<close> [THEN less_imp_le] by (rule convexD_alt)
    6.37 -    then show "y \<in> s" using \<open>u < 1\<close>
    6.38 +    with assms(3) have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> S" ..
    6.39 +    with assms(1) have "(1 - u) *\<^sub>R ((y - u *\<^sub>R x) /\<^sub>R (1 - u)) + u *\<^sub>R x \<in> S"
    6.40 +      using \<open>x \<in> S\<close> \<open>0 \<le> u\<close> \<open>u < 1\<close> [THEN less_imp_le] by (rule convexD_alt)
    6.41 +    then show "y \<in> S" using \<open>u < 1\<close>
    6.42        by simp
    6.43    qed
    6.44 -  ultimately have "u *\<^sub>R x \<in> interior s" ..
    6.45 -  then show "u *\<^sub>R x \<in> s - frontier s"
    6.46 +  ultimately have "u *\<^sub>R x \<in> interior S" ..
    6.47 +  then show "u *\<^sub>R x \<in> S - frontier S"
    6.48      using frontier_def and interior_subset by auto
    6.49  qed
    6.50  
    6.51  proposition homeomorphic_convex_compact_cball:
    6.52    fixes e :: real
    6.53 -    and s :: "'a::euclidean_space set"
    6.54 -  assumes "convex s"
    6.55 -    and "compact s"
    6.56 -    and "interior s \<noteq> {}"
    6.57 +    and S :: "'a::euclidean_space set"
    6.58 +  assumes "convex S"
    6.59 +    and "compact S"
    6.60 +    and "interior S \<noteq> {}"
    6.61      and "e > 0"
    6.62 -  shows "s homeomorphic (cball (b::'a) e)"
    6.63 +  shows "S homeomorphic (cball (b::'a) e)"
    6.64  proof -
    6.65 -  obtain a where "a \<in> interior s"
    6.66 +  obtain a where "a \<in> interior S"
    6.67      using assms(3) by auto
    6.68 -  then obtain d where "d > 0" and d: "cball a d \<subseteq> s"
    6.69 +  then obtain d where "d > 0" and d: "cball a d \<subseteq> S"
    6.70      unfolding mem_interior_cball by auto
    6.71    let ?d = "inverse d" and ?n = "0::'a"
    6.72 -  have "cball ?n 1 \<subseteq> (\<lambda>x. inverse d *\<^sub>R (x - a)) ` s"
    6.73 +  have "cball ?n 1 \<subseteq> (\<lambda>x. inverse d *\<^sub>R (x - a)) ` S"
    6.74      apply rule
    6.75      apply (rule_tac x="d *\<^sub>R x + a" in image_eqI)
    6.76      defer
    6.77 @@ -1166,25 +1166,25 @@
    6.78      unfolding mem_cball dist_norm
    6.79      apply (auto simp add: mult_right_le_one_le)
    6.80      done
    6.81 -  then have "(\<lambda>x. inverse d *\<^sub>R (x - a)) ` s homeomorphic cball ?n 1"
    6.82 -    using homeomorphic_convex_compact_lemma[of "(\<lambda>x. ?d *\<^sub>R -a + ?d *\<^sub>R x) ` s",
    6.83 +  then have "(\<lambda>x. inverse d *\<^sub>R (x - a)) ` S homeomorphic cball ?n 1"
    6.84 +    using homeomorphic_convex_compact_lemma[of "(\<lambda>x. ?d *\<^sub>R -a + ?d *\<^sub>R x) ` S",
    6.85        OF convex_affinity compact_affinity]
    6.86      using assms(1,2)
    6.87      by (auto simp add: scaleR_right_diff_distrib)
    6.88    then show ?thesis
    6.89      apply (rule_tac homeomorphic_trans[OF _ homeomorphic_balls(2)[of 1 _ ?n]])
    6.90 -    apply (rule homeomorphic_trans[OF homeomorphic_affinity[of "?d" s "?d *\<^sub>R -a"]])
    6.91 +    apply (rule homeomorphic_trans[OF homeomorphic_affinity[of "?d" S "?d *\<^sub>R -a"]])
    6.92      using \<open>d>0\<close> \<open>e>0\<close>
    6.93      apply (auto simp add: scaleR_right_diff_distrib)
    6.94      done
    6.95  qed
    6.96  
    6.97  corollary homeomorphic_convex_compact:
    6.98 -  fixes s :: "'a::euclidean_space set"
    6.99 -    and t :: "'a set"
   6.100 -  assumes "convex s" "compact s" "interior s \<noteq> {}"
   6.101 -    and "convex t" "compact t" "interior t \<noteq> {}"
   6.102 -  shows "s homeomorphic t"
   6.103 +  fixes S :: "'a::euclidean_space set"
   6.104 +    and T :: "'a set"
   6.105 +  assumes "convex S" "compact S" "interior S \<noteq> {}"
   6.106 +    and "convex T" "compact T" "interior T \<noteq> {}"
   6.107 +  shows "S homeomorphic T"
   6.108    using assms
   6.109    by (meson zero_less_one homeomorphic_trans homeomorphic_convex_compact_cball homeomorphic_sym)
   6.110  
   6.111 @@ -1193,31 +1193,31 @@
   6.112  definition covering_space
   6.113             :: "'a::topological_space set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
   6.114    where
   6.115 -  "covering_space c p s \<equiv>
   6.116 -       continuous_on c p \<and> p ` c = s \<and>
   6.117 -       (\<forall>x \<in> s. \<exists>t. x \<in> t \<and> openin (subtopology euclidean s) t \<and>
   6.118 -                    (\<exists>v. \<Union>v = {x. x \<in> c \<and> p x \<in> t} \<and>
   6.119 +  "covering_space c p S \<equiv>
   6.120 +       continuous_on c p \<and> p ` c = S \<and>
   6.121 +       (\<forall>x \<in> S. \<exists>T. x \<in> T \<and> openin (subtopology euclidean S) T \<and>
   6.122 +                    (\<exists>v. \<Union>v = {x. x \<in> c \<and> p x \<in> T} \<and>
   6.123                          (\<forall>u \<in> v. openin (subtopology euclidean c) u) \<and>
   6.124                          pairwise disjnt v \<and>
   6.125 -                        (\<forall>u \<in> v. \<exists>q. homeomorphism u t p q)))"
   6.126 +                        (\<forall>u \<in> v. \<exists>q. homeomorphism u T p q)))"
   6.127  
   6.128 -lemma covering_space_imp_continuous: "covering_space c p s \<Longrightarrow> continuous_on c p"
   6.129 +lemma covering_space_imp_continuous: "covering_space c p S \<Longrightarrow> continuous_on c p"
   6.130    by (simp add: covering_space_def)
   6.131  
   6.132 -lemma covering_space_imp_surjective: "covering_space c p s \<Longrightarrow> p ` c = s"
   6.133 +lemma covering_space_imp_surjective: "covering_space c p S \<Longrightarrow> p ` c = S"
   6.134    by (simp add: covering_space_def)
   6.135  
   6.136 -lemma homeomorphism_imp_covering_space: "homeomorphism s t f g \<Longrightarrow> covering_space s f t"
   6.137 +lemma homeomorphism_imp_covering_space: "homeomorphism S T f g \<Longrightarrow> covering_space S f T"
   6.138    apply (simp add: homeomorphism_def covering_space_def, clarify)
   6.139 -  apply (rule_tac x=t in exI, simp)
   6.140 -  apply (rule_tac x="{s}" in exI, auto)
   6.141 +  apply (rule_tac x=T in exI, simp)
   6.142 +  apply (rule_tac x="{S}" in exI, auto)
   6.143    done
   6.144  
   6.145  lemma covering_space_local_homeomorphism:
   6.146 -  assumes "covering_space c p s" "x \<in> c"
   6.147 -  obtains t u q where "x \<in> t" "openin (subtopology euclidean c) t"
   6.148 -                      "p x \<in> u" "openin (subtopology euclidean s) u"
   6.149 -                      "homeomorphism t u p q"
   6.150 +  assumes "covering_space c p S" "x \<in> c"
   6.151 +  obtains T u q where "x \<in> T" "openin (subtopology euclidean c) T"
   6.152 +                      "p x \<in> u" "openin (subtopology euclidean S) u"
   6.153 +                      "homeomorphism T u p q"
   6.154  using assms
   6.155  apply (simp add: covering_space_def, clarify)
   6.156  apply (drule_tac x="p x" in bspec, force)
   6.157 @@ -1225,11 +1225,11 @@
   6.158  
   6.159  
   6.160  lemma covering_space_local_homeomorphism_alt:
   6.161 -  assumes p: "covering_space c p s" and "y \<in> s"
   6.162 -  obtains x t u q where "p x = y"
   6.163 -                        "x \<in> t" "openin (subtopology euclidean c) t"
   6.164 -                        "y \<in> u" "openin (subtopology euclidean s) u"
   6.165 -                          "homeomorphism t u p q"
   6.166 +  assumes p: "covering_space c p S" and "y \<in> S"
   6.167 +  obtains x T u q where "p x = y"
   6.168 +                        "x \<in> T" "openin (subtopology euclidean c) T"
   6.169 +                        "y \<in> u" "openin (subtopology euclidean S) u"
   6.170 +                          "homeomorphism T u p q"
   6.171  proof -
   6.172    obtain x where "p x = y" "x \<in> c"
   6.173      using assms covering_space_imp_surjective by blast
   6.174 @@ -1239,50 +1239,50 @@
   6.175  qed
   6.176  
   6.177  proposition covering_space_open_map:
   6.178 -  fixes s :: "'a :: metric_space set" and t :: "'b :: metric_space set"
   6.179 -  assumes p: "covering_space c p s" and t: "openin (subtopology euclidean c) t"
   6.180 -    shows "openin (subtopology euclidean s) (p ` t)"
   6.181 +  fixes S :: "'a :: metric_space set" and T :: "'b :: metric_space set"
   6.182 +  assumes p: "covering_space c p S" and T: "openin (subtopology euclidean c) T"
   6.183 +    shows "openin (subtopology euclidean S) (p ` T)"
   6.184  proof -
   6.185 -  have pce: "p ` c = s"
   6.186 +  have pce: "p ` c = S"
   6.187     and covs:
   6.188 -       "\<And>x. x \<in> s \<Longrightarrow>
   6.189 -            \<exists>X VS. x \<in> X \<and> openin (subtopology euclidean s) X \<and>
   6.190 +       "\<And>x. x \<in> S \<Longrightarrow>
   6.191 +            \<exists>X VS. x \<in> X \<and> openin (subtopology euclidean S) X \<and>
   6.192                    \<Union>VS = {x. x \<in> c \<and> p x \<in> X} \<and>
   6.193                    (\<forall>u \<in> VS. openin (subtopology euclidean c) u) \<and>
   6.194                    pairwise disjnt VS \<and>
   6.195                    (\<forall>u \<in> VS. \<exists>q. homeomorphism u X p q)"
   6.196      using p by (auto simp: covering_space_def)
   6.197 -  have "t \<subseteq> c"  by (metis openin_euclidean_subtopology_iff t)
   6.198 -  have "\<exists>T. openin (subtopology euclidean s) T \<and> y \<in> T \<and> T \<subseteq> p ` t"
   6.199 -          if "y \<in> p ` t" for y
   6.200 +  have "T \<subseteq> c"  by (metis openin_euclidean_subtopology_iff T)
   6.201 +  have "\<exists>X. openin (subtopology euclidean S) X \<and> y \<in> X \<and> X \<subseteq> p ` T"
   6.202 +          if "y \<in> p ` T" for y
   6.203    proof -
   6.204 -    have "y \<in> s" using \<open>t \<subseteq> c\<close> pce that by blast
   6.205 -    obtain U VS where "y \<in> U" and U: "openin (subtopology euclidean s) U"
   6.206 +    have "y \<in> S" using \<open>T \<subseteq> c\<close> pce that by blast
   6.207 +    obtain U VS where "y \<in> U" and U: "openin (subtopology euclidean S) U"
   6.208                    and VS: "\<Union>VS = {x. x \<in> c \<and> p x \<in> U}"
   6.209                    and openVS: "\<forall>V \<in> VS. openin (subtopology euclidean c) V"
   6.210                    and homVS: "\<And>V. V \<in> VS \<Longrightarrow> \<exists>q. homeomorphism V U p q"
   6.211 -      using covs [OF \<open>y \<in> s\<close>] by auto
   6.212 -    obtain x where "x \<in> c" "p x \<in> U" "x \<in> t" "p x = y"
   6.213 +      using covs [OF \<open>y \<in> S\<close>] by auto
   6.214 +    obtain x where "x \<in> c" "p x \<in> U" "x \<in> T" "p x = y"
   6.215        apply simp
   6.216 -      using t [unfolded openin_euclidean_subtopology_iff] \<open>y \<in> U\<close> \<open>y \<in> p ` t\<close> by blast
   6.217 +      using T [unfolded openin_euclidean_subtopology_iff] \<open>y \<in> U\<close> \<open>y \<in> p ` T\<close> by blast
   6.218      with VS obtain V where "x \<in> V" "V \<in> VS" by auto
   6.219      then obtain q where q: "homeomorphism V U p q" using homVS by blast
   6.220 -    then have ptV: "p ` (t \<inter> V) = U \<inter> {z. q z \<in> (t \<inter> V)}"
   6.221 +    then have ptV: "p ` (T \<inter> V) = U \<inter> {z. q z \<in> (T \<inter> V)}"
   6.222        using VS \<open>V \<in> VS\<close> by (auto simp: homeomorphism_def)
   6.223      have ocv: "openin (subtopology euclidean c) V"
   6.224        by (simp add: \<open>V \<in> VS\<close> openVS)
   6.225 -    have "openin (subtopology euclidean U) {z \<in> U. q z \<in> t \<inter> V}"
   6.226 +    have "openin (subtopology euclidean U) {z \<in> U. q z \<in> T \<inter> V}"
   6.227        apply (rule continuous_on_open [THEN iffD1, rule_format])
   6.228         using homeomorphism_def q apply blast
   6.229 -      using openin_subtopology_Int_subset [of c] q t unfolding homeomorphism_def
   6.230 +      using openin_subtopology_Int_subset [of c] q T unfolding homeomorphism_def
   6.231        by (metis inf.absorb_iff2 Int_commute ocv openin_euclidean_subtopology_iff)
   6.232 -    then have os: "openin (subtopology euclidean s) (U \<inter> {z. q z \<in> t \<inter> V})"
   6.233 +    then have os: "openin (subtopology euclidean S) (U \<inter> {z. q z \<in> T \<inter> V})"
   6.234        using openin_trans [of U] by (simp add: Collect_conj_eq U)
   6.235      show ?thesis
   6.236 -      apply (rule_tac x = "p ` (t \<inter> V)" in exI)
   6.237 +      apply (rule_tac x = "p ` (T \<inter> V)" in exI)
   6.238        apply (rule conjI)
   6.239        apply (simp only: ptV os)
   6.240 -      using \<open>p x = y\<close> \<open>x \<in> V\<close> \<open>x \<in> t\<close> apply blast
   6.241 +      using \<open>p x = y\<close> \<open>x \<in> V\<close> \<open>x \<in> T\<close> apply blast
   6.242        done
   6.243    qed
   6.244    with openin_subopen show ?thesis by blast
   6.245 @@ -1291,73 +1291,73 @@
   6.246  lemma covering_space_lift_unique_gen:
   6.247    fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
   6.248    fixes g1 :: "'a \<Rightarrow> 'c::real_normed_vector"
   6.249 -  assumes cov: "covering_space c p s"
   6.250 +  assumes cov: "covering_space c p S"
   6.251        and eq: "g1 a = g2 a"
   6.252 -      and f: "continuous_on t f"  "f ` t \<subseteq> s"
   6.253 -      and g1: "continuous_on t g1"  "g1 ` t \<subseteq> c"
   6.254 -      and fg1: "\<And>x. x \<in> t \<Longrightarrow> f x = p(g1 x)"
   6.255 -      and g2: "continuous_on t g2"  "g2 ` t \<subseteq> c"
   6.256 -      and fg2: "\<And>x. x \<in> t \<Longrightarrow> f x = p(g2 x)"
   6.257 -      and u_compt: "u \<in> components t" and "a \<in> u" "x \<in> u"
   6.258 +      and f: "continuous_on T f"  "f ` T \<subseteq> S"
   6.259 +      and g1: "continuous_on T g1"  "g1 ` T \<subseteq> c"
   6.260 +      and fg1: "\<And>x. x \<in> T \<Longrightarrow> f x = p(g1 x)"
   6.261 +      and g2: "continuous_on T g2"  "g2 ` T \<subseteq> c"
   6.262 +      and fg2: "\<And>x. x \<in> T \<Longrightarrow> f x = p(g2 x)"
   6.263 +      and u_compt: "U \<in> components T" and "a \<in> U" "x \<in> U"
   6.264      shows "g1 x = g2 x"
   6.265  proof -
   6.266 -  have "u \<subseteq> t" by (rule in_components_subset [OF u_compt])
   6.267 -  def G12 \<equiv> "{x \<in> u. g1 x - g2 x = 0}"
   6.268 -  have "connected u" by (rule in_components_connected [OF u_compt])
   6.269 -  have contu: "continuous_on u g1" "continuous_on u g2"
   6.270 -       using \<open>u \<subseteq> t\<close> continuous_on_subset g1 g2 by blast+
   6.271 -  have o12: "openin (subtopology euclidean u) G12"
   6.272 +  have "U \<subseteq> T" by (rule in_components_subset [OF u_compt])
   6.273 +  def G12 \<equiv> "{x \<in> U. g1 x - g2 x = 0}"
   6.274 +  have "connected U" by (rule in_components_connected [OF u_compt])
   6.275 +  have contu: "continuous_on U g1" "continuous_on U g2"
   6.276 +       using \<open>U \<subseteq> T\<close> continuous_on_subset g1 g2 by blast+
   6.277 +  have o12: "openin (subtopology euclidean U) G12"
   6.278    unfolding G12_def
   6.279    proof (subst openin_subopen, clarify)
   6.280      fix z
   6.281 -    assume z: "z \<in> u" "g1 z - g2 z = 0"
   6.282 +    assume z: "z \<in> U" "g1 z - g2 z = 0"
   6.283      obtain v w q where "g1 z \<in> v" and ocv: "openin (subtopology euclidean c) v"
   6.284 -                   and "p (g1 z) \<in> w" and osw: "openin (subtopology euclidean s) w"
   6.285 +                   and "p (g1 z) \<in> w" and osw: "openin (subtopology euclidean S) w"
   6.286                     and hom: "homeomorphism v w p q"
   6.287        apply (rule_tac x = "g1 z" in covering_space_local_homeomorphism [OF cov])
   6.288 -       using \<open>u \<subseteq> t\<close> \<open>z \<in> u\<close> g1(2) apply blast+
   6.289 +       using \<open>U \<subseteq> T\<close> \<open>z \<in> U\<close> g1(2) apply blast+
   6.290        done
   6.291      have "g2 z \<in> v" using \<open>g1 z \<in> v\<close> z by auto
   6.292 -    have gg: "{x \<in> u. g x \<in> v} = {x \<in> u. g x \<in> (v \<inter> g ` u)}" for g
   6.293 +    have gg: "{x \<in> U. g x \<in> v} = {x \<in> U. g x \<in> (v \<inter> g ` U)}" for g
   6.294        by auto
   6.295 -    have "openin (subtopology euclidean (g1 ` u)) (v \<inter> g1 ` u)"
   6.296 -      using ocv \<open>u \<subseteq> t\<close> g1 by (fastforce simp add: openin_open)
   6.297 -    then have 1: "openin (subtopology euclidean u) {x \<in> u. g1 x \<in> v}"
   6.298 +    have "openin (subtopology euclidean (g1 ` U)) (v \<inter> g1 ` U)"
   6.299 +      using ocv \<open>U \<subseteq> T\<close> g1 by (fastforce simp add: openin_open)
   6.300 +    then have 1: "openin (subtopology euclidean U) {x \<in> U. g1 x \<in> v}"
   6.301        unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format])
   6.302 -    have "openin (subtopology euclidean (g2 ` u)) (v \<inter> g2 ` u)"
   6.303 -      using ocv \<open>u \<subseteq> t\<close> g2 by (fastforce simp add: openin_open)
   6.304 -    then have 2: "openin (subtopology euclidean u) {x \<in> u. g2 x \<in> v}"
   6.305 +    have "openin (subtopology euclidean (g2 ` U)) (v \<inter> g2 ` U)"
   6.306 +      using ocv \<open>U \<subseteq> T\<close> g2 by (fastforce simp add: openin_open)
   6.307 +    then have 2: "openin (subtopology euclidean U) {x \<in> U. g2 x \<in> v}"
   6.308        unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format])
   6.309 -    show "\<exists>T. openin (subtopology euclidean u) T \<and>
   6.310 -              z \<in> T \<and> T \<subseteq> {z \<in> u. g1 z - g2 z = 0}"
   6.311 +    show "\<exists>T. openin (subtopology euclidean U) T \<and>
   6.312 +              z \<in> T \<and> T \<subseteq> {z \<in> U. g1 z - g2 z = 0}"
   6.313        using z
   6.314 -      apply (rule_tac x = "{x. x \<in> u \<and> g1 x \<in> v} \<inter> {x. x \<in> u \<and> g2 x \<in> v}" in exI)
   6.315 +      apply (rule_tac x = "{x. x \<in> U \<and> g1 x \<in> v} \<inter> {x. x \<in> U \<and> g2 x \<in> v}" in exI)
   6.316        apply (intro conjI)
   6.317        apply (rule openin_Int [OF 1 2])
   6.318        using \<open>g1 z \<in> v\<close>  \<open>g2 z \<in> v\<close>  apply (force simp:, clarify)
   6.319 -      apply (metis \<open>u \<subseteq> t\<close> subsetD eq_iff_diff_eq_0 fg1 fg2 hom homeomorphism_def)
   6.320 +      apply (metis \<open>U \<subseteq> T\<close> subsetD eq_iff_diff_eq_0 fg1 fg2 hom homeomorphism_def)
   6.321        done
   6.322    qed
   6.323 -  have c12: "closedin (subtopology euclidean u) G12"
   6.324 +  have c12: "closedin (subtopology euclidean U) G12"
   6.325      unfolding G12_def
   6.326      by (intro continuous_intros continuous_closedin_preimage_constant contu)
   6.327 -  have "G12 = {} \<or> G12 = u"
   6.328 -    by (intro connected_clopen [THEN iffD1, rule_format] \<open>connected u\<close> conjI o12 c12)
   6.329 -  with eq \<open>a \<in> u\<close> have "\<And>x. x \<in> u \<Longrightarrow> g1 x - g2 x = 0" by (auto simp: G12_def)
   6.330 +  have "G12 = {} \<or> G12 = U"
   6.331 +    by (intro connected_clopen [THEN iffD1, rule_format] \<open>connected U\<close> conjI o12 c12)
   6.332 +  with eq \<open>a \<in> U\<close> have "\<And>x. x \<in> U \<Longrightarrow> g1 x - g2 x = 0" by (auto simp: G12_def)
   6.333    then show ?thesis
   6.334 -    using \<open>x \<in> u\<close> by force
   6.335 +    using \<open>x \<in> U\<close> by force
   6.336  qed
   6.337  
   6.338  proposition covering_space_lift_unique:
   6.339    fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
   6.340    fixes g1 :: "'a \<Rightarrow> 'c::real_normed_vector"
   6.341 -  assumes "covering_space c p s"
   6.342 +  assumes "covering_space c p S"
   6.343            "g1 a = g2 a"
   6.344 -          "continuous_on t f"  "f ` t \<subseteq> s"
   6.345 -          "continuous_on t g1"  "g1 ` t \<subseteq> c"  "\<And>x. x \<in> t \<Longrightarrow> f x = p(g1 x)"
   6.346 -          "continuous_on t g2"  "g2 ` t \<subseteq> c"  "\<And>x. x \<in> t \<Longrightarrow> f x = p(g2 x)"
   6.347 -          "connected t"  "a \<in> t"   "x \<in> t"
   6.348 +          "continuous_on T f"  "f ` T \<subseteq> S"
   6.349 +          "continuous_on T g1"  "g1 ` T \<subseteq> c"  "\<And>x. x \<in> T \<Longrightarrow> f x = p(g1 x)"
   6.350 +          "continuous_on T g2"  "g2 ` T \<subseteq> c"  "\<And>x. x \<in> T \<Longrightarrow> f x = p(g2 x)"
   6.351 +          "connected T"  "a \<in> T"   "x \<in> T"
   6.352     shows "g1 x = g2 x"
   6.353 -using covering_space_lift_unique_gen [of c p s] in_components_self assms ex_in_conv by blast
   6.354 +using covering_space_lift_unique_gen [of c p S] in_components_self assms ex_in_conv by blast
   6.355  
   6.356  end
     7.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Tue Jan 03 23:21:09 2017 +0100
     7.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Wed Jan 04 16:18:50 2017 +0000
     7.3 @@ -1482,14 +1482,14 @@
     7.4  
     7.5  lemma sum_norm_le:
     7.6    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
     7.7 -  assumes fg: "\<forall>x \<in> S. norm (f x) \<le> g x"
     7.8 +  assumes fg: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> g x"
     7.9    shows "norm (sum f S) \<le> sum g S"
    7.10    by (rule order_trans [OF norm_sum sum_mono]) (simp add: fg)
    7.11  
    7.12  lemma sum_norm_bound:
    7.13    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
    7.14 -  assumes K: "\<forall>x \<in> S. norm (f x) \<le> K"
    7.15 -  shows "norm (sum f S) \<le> of_nat (card S) * K"
    7.16 +  assumes K: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> K"
    7.17 +  shows "norm (sum f S) \<le> of_nat (card S)*K"
    7.18    using sum_norm_le[OF K] sum_constant[symmetric]
    7.19    by simp
    7.20  
    7.21 @@ -1946,11 +1946,9 @@
    7.22      also have "\<dots> = norm (sum ?g Basis)"
    7.23        by (simp add: linear_sum [OF lf] linear_cmul [OF lf])
    7.24      finally have th0: "norm (f x) = norm (sum ?g Basis)" .
    7.25 -    have th: "\<forall>b\<in>Basis. norm (?g b) \<le> norm (f b) * norm x"
    7.26 -    proof
    7.27 -      fix i :: 'a
    7.28 -      assume i: "i \<in> Basis"
    7.29 -      from Basis_le_norm[OF i, of x]
    7.30 +    have th: "norm (?g i) \<le> norm (f i) * norm x" if "i \<in> Basis" for i
    7.31 +    proof -
    7.32 +      from Basis_le_norm[OF that, of x]
    7.33        show "norm (?g i) \<le> norm (f i) * norm x"
    7.34          unfolding norm_scaleR
    7.35          apply (subst mult.commute)
    7.36 @@ -2023,7 +2021,6 @@
    7.37    show "norm (h x y) \<le> (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. norm (h i j)) * norm x * norm y"
    7.38      apply (auto simp add: sum_distrib_right th sum.cartesian_product)
    7.39      apply (rule sum_norm_le)
    7.40 -    apply simp
    7.41      apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh]
    7.42        field_simps simp del: scaleR_scaleR)
    7.43      apply (rule mult_mono)
     8.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Jan 03 23:21:09 2017 +0100
     8.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Wed Jan 04 16:18:50 2017 +0000
     8.3 @@ -15,6 +15,23 @@
     8.4    Norm_Arith
     8.5  begin
     8.6  
     8.7 +(* FIXME: move to HOL/Real_Vector_Spaces.thy *)
     8.8 +
     8.9 +lemma scaleR_2:
    8.10 +  fixes x :: "'a::real_vector"
    8.11 +  shows "scaleR 2 x = x + x"
    8.12 +  unfolding one_add_one [symmetric] scaleR_left_distrib by simp
    8.13 +
    8.14 +lemma scaleR_half_double [simp]:
    8.15 +  fixes a :: "'a::real_normed_vector"
    8.16 +  shows "(1 / 2) *\<^sub>R (a + a) = a"
    8.17 +proof -
    8.18 +  have "\<And>r. r *\<^sub>R (a + a) = (r * 2) *\<^sub>R a"
    8.19 +    by (metis scaleR_2 scaleR_scaleR)
    8.20 +  then show ?thesis
    8.21 +    by simp
    8.22 +qed
    8.23 +
    8.24  
    8.25  (* FIXME: move elsewhere *)
    8.26  
    8.27 @@ -1675,6 +1692,9 @@
    8.28  lemma box01_nonempty [simp]: "box 0 One \<noteq> {}"
    8.29    by (simp add: box_ne_empty inner_Basis inner_sum_left) (simp add: sum.remove)
    8.30  
    8.31 +lemma empty_as_interval: "{} = cbox One (0::'a::euclidean_space)"
    8.32 +  using nonempty_Basis box01_nonempty box_eq_empty(1) box_ne_empty(1) by blast
    8.33 +
    8.34  
    8.35  subsection \<open>Connectedness\<close>
    8.36  
    8.37 @@ -4338,6 +4358,16 @@
    8.38    using l unfolding islimpt_eq_acc_point
    8.39    by (rule acc_point_range_imp_convergent_subsequence)
    8.40  
    8.41 +lemma islimpt_eq_infinite_ball: "x islimpt S \<longleftrightarrow> (\<forall>e>0. infinite(S \<inter> ball x e))"
    8.42 +  apply (simp add: islimpt_eq_acc_point, safe)
    8.43 +   apply (metis Int_commute open_ball centre_in_ball)
    8.44 +  by (metis open_contains_ball Int_mono finite_subset inf_commute subset_refl)
    8.45 +
    8.46 +lemma islimpt_eq_infinite_cball: "x islimpt S \<longleftrightarrow> (\<forall>e>0. infinite(S \<inter> cball x e))"
    8.47 +  apply (simp add: islimpt_eq_infinite_ball, safe)
    8.48 +   apply (meson Int_mono ball_subset_cball finite_subset order_refl)
    8.49 +  by (metis open_ball centre_in_ball finite_Int inf.absorb_iff2 inf_assoc open_contains_cball_eq)
    8.50 +
    8.51  lemma sequence_unique_limpt:
    8.52    fixes f :: "nat \<Rightarrow> 'a::t2_space"
    8.53    assumes "(f \<longlongrightarrow> l) sequentially"
    8.54 @@ -4475,6 +4505,7 @@
    8.55           \<Longrightarrow> openin (subtopology euclidean u) (s - {a})"
    8.56  by (metis Int_Diff open_delete openin_open)
    8.57  
    8.58 +
    8.59  text\<open>Compactness expressed with filters\<close>
    8.60  
    8.61  lemma closure_iff_nhds_not_empty:
    8.62 @@ -5032,6 +5063,7 @@
    8.63    "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> bounded s"
    8.64    using compact_imp_bounded unfolding compact_eq_bolzano_weierstrass .
    8.65  
    8.66 +
    8.67  subsection \<open>Metric spaces with the Heine-Borel property\<close>
    8.68  
    8.69  text \<open>
    8.70 @@ -5254,6 +5286,84 @@
    8.71    show "\<exists>l r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
    8.72      using l r by fast
    8.73  qed
    8.74 +  
    8.75 +subsubsection \<open>Intersecting chains of compact sets\<close>
    8.76 +
    8.77 +proposition bounded_closed_chain:
    8.78 +  fixes \<F> :: "'a::heine_borel set set"
    8.79 +  assumes "B \<in> \<F>" "bounded B" and \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> closed S" and "{} \<notin> \<F>"
    8.80 +      and chain: "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
    8.81 +    shows "\<Inter>\<F> \<noteq> {}"
    8.82 +proof -
    8.83 +  have "B \<inter> \<Inter>\<F> \<noteq> {}"
    8.84 +  proof (rule compact_imp_fip)
    8.85 +    show "compact B" "\<And>T. T \<in> \<F> \<Longrightarrow> closed T"
    8.86 +      by (simp_all add: assms compact_eq_bounded_closed)
    8.87 +    show "\<lbrakk>finite \<G>; \<G> \<subseteq> \<F>\<rbrakk> \<Longrightarrow> B \<inter> \<Inter>\<G> \<noteq> {}" for \<G>
    8.88 +    proof (induction \<G> rule: finite_induct)
    8.89 +      case empty
    8.90 +      with assms show ?case by force
    8.91 +    next
    8.92 +      case (insert U \<G>)
    8.93 +      then have "U \<in> \<F>" and ne: "B \<inter> \<Inter>\<G> \<noteq> {}" by auto
    8.94 +      then consider "B \<subseteq> U" | "U \<subseteq> B"
    8.95 +          using \<open>B \<in> \<F>\<close> chain by blast
    8.96 +        then show ?case
    8.97 +        proof cases
    8.98 +          case 1
    8.99 +          then show ?thesis
   8.100 +            using Int_left_commute ne by auto
   8.101 +        next
   8.102 +          case 2
   8.103 +          have "U \<noteq> {}"
   8.104 +            using \<open>U \<in> \<F>\<close> \<open>{} \<notin> \<F>\<close> by blast
   8.105 +          moreover
   8.106 +          have False if "\<And>x. x \<in> U \<Longrightarrow> \<exists>Y\<in>\<G>. x \<notin> Y"
   8.107 +          proof -
   8.108 +            have "\<And>x. x \<in> U \<Longrightarrow> \<exists>Y\<in>\<G>. Y \<subseteq> U"
   8.109 +              by (metis chain contra_subsetD insert.prems insert_subset that)
   8.110 +            then obtain Y where "Y \<in> \<G>" "Y \<subseteq> U"
   8.111 +              by (metis all_not_in_conv \<open>U \<noteq> {}\<close>)
   8.112 +            moreover obtain x where "x \<in> \<Inter>\<G>"
   8.113 +              by (metis Int_emptyI ne)
   8.114 +            ultimately show ?thesis
   8.115 +              by (metis Inf_lower subset_eq that)
   8.116 +          qed
   8.117 +          with 2 show ?thesis
   8.118 +            by blast
   8.119 +        qed
   8.120 +      qed
   8.121 +  qed
   8.122 +  then show ?thesis by blast
   8.123 +qed
   8.124 +
   8.125 +corollary compact_chain:
   8.126 +  fixes \<F> :: "'a::heine_borel set set"
   8.127 +  assumes "\<And>S. S \<in> \<F> \<Longrightarrow> compact S" "{} \<notin> \<F>"
   8.128 +          "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
   8.129 +    shows "\<Inter> \<F> \<noteq> {}"
   8.130 +proof (cases "\<F> = {}")
   8.131 +  case True
   8.132 +  then show ?thesis by auto
   8.133 +next
   8.134 +  case False
   8.135 +  show ?thesis
   8.136 +    by (metis False all_not_in_conv assms compact_imp_bounded compact_imp_closed bounded_closed_chain)
   8.137 +qed
   8.138 +
   8.139 +lemma compact_nest:
   8.140 +  fixes F :: "'a::linorder \<Rightarrow> 'b::heine_borel set"
   8.141 +  assumes F: "\<And>n. compact(F n)" "\<And>n. F n \<noteq> {}" and mono: "\<And>m n. m \<le> n \<Longrightarrow> F n \<subseteq> F m"
   8.142 +  shows "\<Inter>range F \<noteq> {}"
   8.143 +proof -
   8.144 +  have *: "\<And>S T. S \<in> range F \<and> T \<in> range F \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
   8.145 +    by (metis mono image_iff le_cases)
   8.146 +  show ?thesis
   8.147 +    apply (rule compact_chain [OF _ _ *])
   8.148 +    using F apply (blast intro: dest: *)+
   8.149 +    done
   8.150 +qed
   8.151 +
   8.152  
   8.153  subsubsection \<open>Completeness\<close>
   8.154  
   8.155 @@ -7446,7 +7556,7 @@
   8.156  qed
   8.157  
   8.158  
   8.159 -subsection \<open>Topological stuff lifted from and dropped to R\<close>
   8.160 +subsection \<open>Topological stuff about the set of Reals\<close>
   8.161  
   8.162  lemma open_real:
   8.163    fixes s :: "real set"
   8.164 @@ -7697,11 +7807,17 @@
   8.165      using continuous_attains_sup[of "s \<times> s" "\<lambda>x. dist (fst x) (snd x)"] by auto
   8.166  qed
   8.167  
   8.168 -text \<open>We can state this in terms of diameter of a set.\<close>
   8.169 +subsection \<open>The diameter of a set.\<close>
   8.170  
   8.171  definition diameter :: "'a::metric_space set \<Rightarrow> real" where
   8.172    "diameter S = (if S = {} then 0 else SUP (x,y):S\<times>S. dist x y)"
   8.173  
   8.174 +lemma diameter_empty [simp]: "diameter{} = 0"
   8.175 +  by (auto simp: diameter_def)
   8.176 +
   8.177 +lemma diameter_singleton [simp]: "diameter{x} = 0"
   8.178 +  by (auto simp: diameter_def)
   8.179 +
   8.180  lemma diameter_le:
   8.181    assumes "S \<noteq> {} \<or> 0 \<le> d"
   8.182        and no: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> norm(x - y) \<le> d"
   8.183 @@ -7772,7 +7888,180 @@
   8.184      by (metis b diameter_bounded_bound order_antisym xys)
   8.185  qed
   8.186  
   8.187 -text \<open>Related results with closure as the conclusion.\<close>
   8.188 +lemma diameter_ge_0:
   8.189 +  assumes "bounded S"  shows "0 \<le> diameter S"
   8.190 +  by (metis all_not_in_conv assms diameter_bounded_bound diameter_empty dist_self order_refl)
   8.191 +
   8.192 +lemma diameter_subset:
   8.193 +  assumes "S \<subseteq> T" "bounded T"
   8.194 +  shows "diameter S \<le> diameter T"
   8.195 +proof (cases "S = {} \<or> T = {}")
   8.196 +  case True
   8.197 +  with assms show ?thesis
   8.198 +    by (force simp: diameter_ge_0)
   8.199 +next
   8.200 +  case False
   8.201 +  then have "bdd_above ((\<lambda>x. case x of (x, xa) \<Rightarrow> dist x xa) ` (T \<times> T))"
   8.202 +    using \<open>bounded T\<close> diameter_bounded_bound by (force simp: bdd_above_def)
   8.203 +  with False \<open>S \<subseteq> T\<close> show ?thesis
   8.204 +    apply (simp add: diameter_def)
   8.205 +    apply (rule cSUP_subset_mono, auto)
   8.206 +    done
   8.207 +qed
   8.208 +
   8.209 +lemma diameter_closure:
   8.210 +  assumes "bounded S"
   8.211 +  shows "diameter(closure S) = diameter S"
   8.212 +proof (rule order_antisym)
   8.213 +  have "False" if "diameter S < diameter (closure S)"
   8.214 +  proof -
   8.215 +    define d where "d = diameter(closure S) - diameter(S)"
   8.216 +    have "d > 0"
   8.217 +      using that by (simp add: d_def)
   8.218 +    then have "diameter(closure(S)) - d / 2 < diameter(closure(S))"
   8.219 +      by simp
   8.220 +    have dd: "diameter (closure S) - d / 2 = (diameter(closure(S)) + diameter(S)) / 2"
   8.221 +      by (simp add: d_def divide_simps)
   8.222 +     have bocl: "bounded (closure S)"
   8.223 +      using assms by blast
   8.224 +    moreover have "0 \<le> diameter S"
   8.225 +      using assms diameter_ge_0 by blast
   8.226 +    ultimately obtain x y where "x \<in> closure S" "y \<in> closure S" and xy: "diameter(closure(S)) - d / 2 < dist x y"
   8.227 +      using diameter_bounded(2) [OF bocl, rule_format, of "diameter(closure(S)) - d / 2"] \<open>d > 0\<close> d_def by auto
   8.228 +    then obtain x' y' where x'y': "x' \<in> S" "dist x' x < d/4" "y' \<in> S" "dist y' y < d/4"
   8.229 +      using closure_approachable
   8.230 +      by (metis \<open>0 < d\<close> zero_less_divide_iff zero_less_numeral)
   8.231 +    then have "dist x' y' \<le> diameter S"
   8.232 +      using assms diameter_bounded_bound by blast
   8.233 +    with x'y' have "dist x y \<le> d / 4 + diameter S + d / 4"
   8.234 +      by (meson add_mono_thms_linordered_semiring(1) dist_triangle dist_triangle3 less_eq_real_def order_trans)
   8.235 +    then show ?thesis
   8.236 +      using xy d_def by linarith
   8.237 +  qed
   8.238 +  then show "diameter (closure S) \<le> diameter S"
   8.239 +    by fastforce
   8.240 +  next
   8.241 +    show "diameter S \<le> diameter (closure S)"
   8.242 +      by (simp add: assms bounded_closure closure_subset diameter_subset)
   8.243 +qed
   8.244 +
   8.245 +lemma diameter_cball [simp]:
   8.246 +  fixes a :: "'a::euclidean_space"
   8.247 +  shows "diameter(cball a r) = (if r < 0 then 0 else 2*r)"
   8.248 +proof -
   8.249 +  have "diameter(cball a r) = 2*r" if "r \<ge> 0"
   8.250 +  proof (rule order_antisym)
   8.251 +    show "diameter (cball a r) \<le> 2*r"
   8.252 +    proof (rule diameter_le)
   8.253 +      fix x y assume "x \<in> cball a r" "y \<in> cball a r"
   8.254 +      then have "norm (x - a) \<le> r" "norm (a - y) \<le> r"
   8.255 +        by (auto simp: dist_norm norm_minus_commute)
   8.256 +      then have "norm (x - y) \<le> r+r"
   8.257 +        using norm_diff_triangle_le by blast
   8.258 +      then show "norm (x - y) \<le> 2*r" by simp
   8.259 +    qed (simp add: that)
   8.260 +    have "2*r = dist (a + r *\<^sub>R (SOME i. i \<in> Basis)) (a - r *\<^sub>R (SOME i. i \<in> Basis))"
   8.261 +      apply (simp add: dist_norm)
   8.262 +      by (metis abs_of_nonneg mult.right_neutral norm_numeral norm_scaleR norm_some_Basis real_norm_def scaleR_2 that)
   8.263 +    also have "... \<le> diameter (cball a r)"
   8.264 +      apply (rule diameter_bounded_bound)
   8.265 +      using that by (auto simp: dist_norm)
   8.266 +    finally show "2*r \<le> diameter (cball a r)" .
   8.267 +  qed
   8.268 +  then show ?thesis by simp
   8.269 +qed
   8.270 +
   8.271 +lemma diameter_ball [simp]:
   8.272 +  fixes a :: "'a::euclidean_space"
   8.273 +  shows "diameter(ball a r) = (if r < 0 then 0 else 2*r)"
   8.274 +proof -
   8.275 +  have "diameter(ball a r) = 2*r" if "r > 0"
   8.276 +    by (metis bounded_ball diameter_closure closure_ball diameter_cball less_eq_real_def linorder_not_less that)
   8.277 +  then show ?thesis
   8.278 +    by (simp add: diameter_def)
   8.279 +qed
   8.280 +
   8.281 +lemma diameter_closed_interval [simp]: "diameter {a..b} = (if b < a then 0 else b-a)"
   8.282 +proof -
   8.283 +  have "{a .. b} = cball ((a+b)/2) ((b-a)/2)"
   8.284 +    by (auto simp: dist_norm abs_if divide_simps split: if_split_asm)
   8.285 +  then show ?thesis
   8.286 +    by simp
   8.287 +qed
   8.288 +
   8.289 +lemma diameter_open_interval [simp]: "diameter {a<..<b} = (if b < a then 0 else b-a)"
   8.290 +proof -
   8.291 +  have "{a <..< b} = ball ((a+b)/2) ((b-a)/2)"
   8.292 +    by (auto simp: dist_norm abs_if divide_simps split: if_split_asm)
   8.293 +  then show ?thesis
   8.294 +    by simp
   8.295 +qed
   8.296 +
   8.297 +proposition Lebesgue_number_lemma:
   8.298 +  assumes "compact S" "\<C> \<noteq> {}" "S \<subseteq> \<Union>\<C>" and ope: "\<And>B. B \<in> \<C> \<Longrightarrow> open B"
   8.299 +  obtains \<delta> where "0 < \<delta>" "\<And>T. \<lbrakk>T \<subseteq> S; diameter T < \<delta>\<rbrakk> \<Longrightarrow> \<exists>B \<in> \<C>. T \<subseteq> B"
   8.300 +proof (cases "S = {}")
   8.301 +  case True
   8.302 +  then show ?thesis
   8.303 +    by (metis \<open>\<C> \<noteq> {}\<close> zero_less_one empty_subsetI equals0I subset_trans that)
   8.304 +next
   8.305 +  case False
   8.306 +  { fix x assume "x \<in> S"
   8.307 +    then obtain C where C: "x \<in> C" "C \<in> \<C>"
   8.308 +      using \<open>S \<subseteq> \<Union>\<C>\<close> by blast
   8.309 +    then obtain r where r: "r>0" "ball x (2*r) \<subseteq> C"
   8.310 +      by (metis mult.commute mult_2_right not_le ope openE real_sum_of_halves zero_le_numeral zero_less_mult_iff)
   8.311 +    then have "\<exists>r C. r > 0 \<and> ball x (2*r) \<subseteq> C \<and> C \<in> \<C>"
   8.312 +      using C by blast
   8.313 +  }
   8.314 +  then obtain r where r: "\<And>x. x \<in> S \<Longrightarrow> r x > 0 \<and> (\<exists>C \<in> \<C>. ball x (2*r x) \<subseteq> C)"
   8.315 +    by metis
   8.316 +  then have "S \<subseteq> (\<Union>x \<in> S. ball x (r x))"
   8.317 +    by auto
   8.318 +  then obtain \<T> where "finite \<T>" "S \<subseteq> \<Union>\<T>" and \<T>: "\<T> \<subseteq> (\<lambda>x. ball x (r x)) ` S"
   8.319 +    by (rule compactE [OF \<open>compact S\<close>]) auto
   8.320 +  then obtain S0 where "S0 \<subseteq> S" "finite S0" and S0: "\<T> = (\<lambda>x. ball x (r x)) ` S0"
   8.321 +    by (meson finite_subset_image)
   8.322 +  then have "S0 \<noteq> {}"
   8.323 +    using False \<open>S \<subseteq> \<Union>\<T>\<close> by auto
   8.324 +  define \<delta> where "\<delta> = Inf (r ` S0)"
   8.325 +  have "\<delta> > 0"
   8.326 +    using \<open>finite S0\<close> \<open>S0 \<subseteq> S\<close> \<open>S0 \<noteq> {}\<close> r by (auto simp: \<delta>_def finite_less_Inf_iff)
   8.327 +  show ?thesis
   8.328 +  proof
   8.329 +    show "0 < \<delta>"
   8.330 +      by (simp add: \<open>0 < \<delta>\<close>)
   8.331 +    show "\<exists>B \<in> \<C>. T \<subseteq> B" if "T \<subseteq> S" and dia: "diameter T < \<delta>" for T
   8.332 +    proof (cases "T = {}")
   8.333 +      case True
   8.334 +      then show ?thesis
   8.335 +        using \<open>\<C> \<noteq> {}\<close> by blast
   8.336 +    next
   8.337 +      case False
   8.338 +      then obtain y where "y \<in> T" by blast
   8.339 +      then have "y \<in> S"
   8.340 +        using \<open>T \<subseteq> S\<close> by auto
   8.341 +      then obtain x where "x \<in> S0" and x: "y \<in> ball x (r x)"
   8.342 +        using \<open>S \<subseteq> \<Union>\<T>\<close> S0 that by blast
   8.343 +      have "ball y \<delta> \<subseteq> ball y (r x)"
   8.344 +        by (metis \<delta>_def \<open>S0 \<noteq> {}\<close> \<open>finite S0\<close> \<open>x \<in> S0\<close> empty_is_image finite_imageI finite_less_Inf_iff imageI less_irrefl not_le subset_ball)
   8.345 +      also have "... \<subseteq> ball x (2*r x)"
   8.346 +        by clarsimp (metis dist_commute dist_triangle_less_add mem_ball mult_2 x)
   8.347 +      finally obtain C where "C \<in> \<C>" "ball y \<delta> \<subseteq> C"
   8.348 +        by (meson r \<open>S0 \<subseteq> S\<close> \<open>x \<in> S0\<close> dual_order.trans subsetCE)
   8.349 +      have "bounded T"
   8.350 +        using \<open>compact S\<close> bounded_subset compact_imp_bounded \<open>T \<subseteq> S\<close> by blast
   8.351 +      then have "T \<subseteq> ball y \<delta>"
   8.352 +        using \<open>y \<in> T\<close> dia diameter_bounded_bound by fastforce
   8.353 +      then show ?thesis
   8.354 +        apply (rule_tac x=C in bexI)
   8.355 +        using \<open>ball y \<delta> \<subseteq> C\<close> \<open>C \<in> \<C>\<close> by auto
   8.356 +    qed
   8.357 +  qed
   8.358 +qed
   8.359 +
   8.360 +
   8.361 +subsection \<open>Compact sets and the closure operation.\<close>
   8.362  
   8.363  lemma closed_scaling:
   8.364    fixes s :: "'a::real_normed_vector set"
   8.365 @@ -8396,6 +8685,63 @@
   8.366    using bounded_closed_imp_seq_compact[of "cbox a b"] using bounded_cbox[of a b]
   8.367    by (auto simp: compact_eq_seq_compact_metric)
   8.368  
   8.369 +proposition is_interval_compact:
   8.370 +   "is_interval S \<and> compact S \<longleftrightarrow> (\<exists>a b. S = cbox a b)"   (is "?lhs = ?rhs")
   8.371 +proof (cases "S = {}")
   8.372 +  case True
   8.373 +  with empty_as_interval show ?thesis by auto
   8.374 +next
   8.375 +  case False
   8.376 +  show ?thesis
   8.377 +  proof
   8.378 +    assume L: ?lhs
   8.379 +    then have "is_interval S" "compact S" by auto
   8.380 +    define a where "a \<equiv> \<Sum>i\<in>Basis. (INF x:S. x \<bullet> i) *\<^sub>R i"
   8.381 +    define b where "b \<equiv> \<Sum>i\<in>Basis. (SUP x:S. x \<bullet> i) *\<^sub>R i"
   8.382 +    have 1: "\<And>x i. \<lbrakk>x \<in> S; i \<in> Basis\<rbrakk> \<Longrightarrow> (INF x:S. x \<bullet> i) \<le> x \<bullet> i"
   8.383 +      by (simp add: cInf_lower bounded_inner_imp_bdd_below compact_imp_bounded L)
   8.384 +    have 2: "\<And>x i. \<lbrakk>x \<in> S; i \<in> Basis\<rbrakk> \<Longrightarrow> x \<bullet> i \<le> (SUP x:S. x \<bullet> i)"
   8.385 +      by (simp add: cSup_upper bounded_inner_imp_bdd_above compact_imp_bounded L)
   8.386 +    have 3: "x \<in> S" if inf: "\<And>i. i \<in> Basis \<Longrightarrow> (INF x:S. x \<bullet> i) \<le> x \<bullet> i"
   8.387 +                   and sup: "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i \<le> (SUP x:S. x \<bullet> i)" for x
   8.388 +    proof (rule mem_box_componentwiseI [OF \<open>is_interval S\<close>])
   8.389 +      fix i::'a
   8.390 +      assume i: "i \<in> Basis"
   8.391 +      have cont: "continuous_on S (\<lambda>x. x \<bullet> i)"
   8.392 +        by (intro continuous_intros)
   8.393 +      obtain a where "a \<in> S" and a: "\<And>y. y\<in>S \<Longrightarrow> a \<bullet> i \<le> y \<bullet> i"
   8.394 +        using continuous_attains_inf [OF \<open>compact S\<close> False cont] by blast
   8.395 +      obtain b where "b \<in> S" and b: "\<And>y. y\<in>S \<Longrightarrow> y \<bullet> i \<le> b \<bullet> i"
   8.396 +        using continuous_attains_sup [OF \<open>compact S\<close> False cont] by blast
   8.397 +      have "a \<bullet> i \<le> (INF x:S. x \<bullet> i)"
   8.398 +        by (simp add: False a cINF_greatest)
   8.399 +      also have "\<dots> \<le> x \<bullet> i"
   8.400 +        by (simp add: i inf)
   8.401 +      finally have ai: "a \<bullet> i \<le> x \<bullet> i" .
   8.402 +      have "x \<bullet> i \<le> (SUP x:S. x \<bullet> i)"
   8.403 +        by (simp add: i sup)
   8.404 +      also have "(SUP x:S. x \<bullet> i) \<le> b \<bullet> i"
   8.405 +        by (simp add: False b cSUP_least)
   8.406 +      finally have bi: "x \<bullet> i \<le> b \<bullet> i" .
   8.407 +      show "x \<bullet> i \<in> (\<lambda>x. x \<bullet> i) ` S"
   8.408 +        apply (rule_tac x="\<Sum>j\<in>Basis. (if j = i then x \<bullet> i else a \<bullet> j) *\<^sub>R j" in image_eqI)
   8.409 +        apply (simp add: i)
   8.410 +        apply (rule mem_is_intervalI [OF \<open>is_interval S\<close> \<open>a \<in> S\<close> \<open>b \<in> S\<close>])
   8.411 +        using i ai bi apply force
   8.412 +        done
   8.413 +    qed
   8.414 +    have "S = cbox a b"
   8.415 +      by (auto simp: a_def b_def mem_box intro: 1 2 3)
   8.416 +    then show ?rhs
   8.417 +      by blast
   8.418 +  next
   8.419 +    assume R: ?rhs
   8.420 +    then show ?lhs
   8.421 +      using compact_cbox is_interval_cbox by blast
   8.422 +  qed
   8.423 +qed
   8.424 +
   8.425 +
   8.426  lemma box_midpoint:
   8.427    fixes a :: "'a::euclidean_space"
   8.428    assumes "box a b \<noteq> {}"
   8.429 @@ -9959,6 +10305,20 @@
   8.430                compact T \<and> T \<subseteq> S)"
   8.431  by (metis closedin_imp_subset closedin_compact closed_subset compact_imp_closed)
   8.432  
   8.433 +lemma continuous_imp_closed_map:
   8.434 +  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
   8.435 +  assumes "closedin (subtopology euclidean S) U"
   8.436 +          "continuous_on S f" "image f S = T" "compact S"
   8.437 +    shows "closedin (subtopology euclidean T) (image f U)"
   8.438 +  by (metis assms closedin_compact_eq compact_continuous_image continuous_on_subset subset_image_iff)
   8.439 +
   8.440 +lemma continuous_imp_quotient_map:
   8.441 +  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
   8.442 +  assumes "continuous_on S f" "image f S = T" "compact S" "U \<subseteq> T"
   8.443 +    shows "openin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> U} \<longleftrightarrow>
   8.444 +           openin (subtopology euclidean T) U"
   8.445 +  by (metis (no_types, lifting) Collect_cong assms closed_map_imp_quotient_map continuous_imp_closed_map)
   8.446 +
   8.447  subsection\<open> Finite intersection property\<close>
   8.448  
   8.449  text\<open>Also developed in HOL's toplogical spaces theory, but the Heine-Borel type class isn't available there.\<close>
   8.450 @@ -10305,6 +10665,166 @@
   8.451    qed
   8.452    from X0(1,2) this show ?thesis ..
   8.453  qed
   8.454 +  
   8.455 +  
   8.456 +subsection\<open>Constancy of a function from a connected set into a finite, disconnected or discrete set\<close>
   8.457 +
   8.458 +text\<open>Still missing: versions for a set that is smaller than R, or countable.\<close>
   8.459 +
   8.460 +lemma continuous_disconnected_range_constant:
   8.461 +  assumes s: "connected s"
   8.462 +      and conf: "continuous_on s f"
   8.463 +      and fim: "f ` s \<subseteq> t"
   8.464 +      and cct: "\<And>y. y \<in> t \<Longrightarrow> connected_component_set t y = {y}"
   8.465 +    shows "\<exists>a. \<forall>x \<in> s. f x = a"
   8.466 +proof (cases "s = {}")
   8.467 +  case True then show ?thesis by force
   8.468 +next
   8.469 +  case False
   8.470 +  { fix x assume "x \<in> s"
   8.471 +    then have "f ` s \<subseteq> {f x}"
   8.472 +    by (metis connected_continuous_image conf connected_component_maximal fim image_subset_iff rev_image_eqI s cct)
   8.473 +  }
   8.474 +  with False show ?thesis
   8.475 +    by blast
   8.476 +qed
   8.477 +
   8.478 +lemma discrete_subset_disconnected:
   8.479 +  fixes s :: "'a::topological_space set"
   8.480 +  fixes t :: "'b::real_normed_vector set"
   8.481 +  assumes conf: "continuous_on s f"
   8.482 +      and no: "\<And>x. x \<in> s \<Longrightarrow> \<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)"
   8.483 +   shows "f ` s \<subseteq> {y. connected_component_set (f ` s) y = {y}}"
   8.484 +proof -
   8.485 +  { fix x assume x: "x \<in> s"
   8.486 +    then obtain e where "e>0" and ele: "\<And>y. \<lbrakk>y \<in> s; f y \<noteq> f x\<rbrakk> \<Longrightarrow> e \<le> norm (f y - f x)"
   8.487 +      using conf no [OF x] by auto
   8.488 +    then have e2: "0 \<le> e / 2"
   8.489 +      by simp
   8.490 +    have "f y = f x" if "y \<in> s" and ccs: "f y \<in> connected_component_set (f ` s) (f x)" for y
   8.491 +      apply (rule ccontr)
   8.492 +      using connected_closed [of "connected_component_set (f ` s) (f x)"] \<open>e>0\<close>
   8.493 +      apply (simp add: del: ex_simps)
   8.494 +      apply (drule spec [where x="cball (f x) (e / 2)"])
   8.495 +      apply (drule spec [where x="- ball(f x) e"])
   8.496 +      apply (auto simp: dist_norm open_closed [symmetric] simp del: le_divide_eq_numeral1 dest!: connected_component_in)
   8.497 +        apply (metis diff_self e2 ele norm_minus_commute norm_zero not_less)
   8.498 +       using centre_in_cball connected_component_refl_eq e2 x apply blast
   8.499 +      using ccs
   8.500 +      apply (force simp: cball_def dist_norm norm_minus_commute dest: ele [OF \<open>y \<in> s\<close>])
   8.501 +      done
   8.502 +    moreover have "connected_component_set (f ` s) (f x) \<subseteq> f ` s"
   8.503 +      by (auto simp: connected_component_in)
   8.504 +    ultimately have "connected_component_set (f ` s) (f x) = {f x}"
   8.505 +      by (auto simp: x)
   8.506 +  }
   8.507 +  with assms show ?thesis
   8.508 +    by blast
   8.509 +qed
   8.510 +
   8.511 +lemma finite_implies_discrete:
   8.512 +  fixes s :: "'a::topological_space set"
   8.513 +  assumes "finite (f ` s)"
   8.514 +  shows "(\<forall>x \<in> s. \<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x))"
   8.515 +proof -
   8.516 +  have "\<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)" if "x \<in> s" for x
   8.517 +  proof (cases "f ` s - {f x} = {}")
   8.518 +    case True
   8.519 +    with zero_less_numeral show ?thesis
   8.520 +      by (fastforce simp add: Set.image_subset_iff cong: conj_cong)
   8.521 +  next
   8.522 +    case False
   8.523 +    then obtain z where z: "z \<in> s" "f z \<noteq> f x"
   8.524 +      by blast
   8.525 +    have finn: "finite {norm (z - f x) |z. z \<in> f ` s - {f x}}"
   8.526 +      using assms by simp
   8.527 +    then have *: "0 < Inf{norm(z - f x) | z. z \<in> f ` s - {f x}}"
   8.528 +      apply (rule finite_imp_less_Inf)
   8.529 +      using z apply force+
   8.530 +      done
   8.531 +    show ?thesis
   8.532 +      by (force intro!: * cInf_le_finite [OF finn])
   8.533 +  qed
   8.534 +  with assms show ?thesis
   8.535 +    by blast
   8.536 +qed
   8.537 +
   8.538 +text\<open>This proof requires the existence of two separate values of the range type.\<close>
   8.539 +lemma finite_range_constant_imp_connected:
   8.540 +  assumes "\<And>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
   8.541 +              \<lbrakk>continuous_on s f; finite(f ` s)\<rbrakk> \<Longrightarrow> \<exists>a. \<forall>x \<in> s. f x = a"
   8.542 +    shows "connected s"
   8.543 +proof -
   8.544 +  { fix t u
   8.545 +    assume clt: "closedin (subtopology euclidean s) t"
   8.546 +       and clu: "closedin (subtopology euclidean s) u"
   8.547 +       and tue: "t \<inter> u = {}" and tus: "t \<union> u = s"
   8.548 +    have conif: "continuous_on s (\<lambda>x. if x \<in> t then 0 else 1)"
   8.549 +      apply (subst tus [symmetric])
   8.550 +      apply (rule continuous_on_cases_local)
   8.551 +      using clt clu tue
   8.552 +      apply (auto simp: tus continuous_on_const)
   8.553 +      done
   8.554 +    have fi: "finite ((\<lambda>x. if x \<in> t then 0 else 1) ` s)"
   8.555 +      by (rule finite_subset [of _ "{0,1}"]) auto
   8.556 +    have "t = {} \<or> u = {}"
   8.557 +      using assms [OF conif fi] tus [symmetric]
   8.558 +      by (auto simp: Ball_def) (metis IntI empty_iff one_neq_zero tue)
   8.559 +  }
   8.560 +  then show ?thesis
   8.561 +    by (simp add: connected_closedin_eq)
   8.562 +qed
   8.563 +
   8.564 +lemma continuous_disconnected_range_constant_eq:
   8.565 +      "(connected s \<longleftrightarrow>
   8.566 +           (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
   8.567 +            \<forall>t. continuous_on s f \<and> f ` s \<subseteq> t \<and> (\<forall>y \<in> t. connected_component_set t y = {y})
   8.568 +            \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> s. f x = a)))" (is ?thesis1)
   8.569 +  and continuous_discrete_range_constant_eq:
   8.570 +      "(connected s \<longleftrightarrow>
   8.571 +         (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
   8.572 +          continuous_on s f \<and>
   8.573 +          (\<forall>x \<in> s. \<exists>e. 0 < e \<and> (\<forall>y. y \<in> s \<and> (f y \<noteq> f x) \<longrightarrow> e \<le> norm(f y - f x)))
   8.574 +          \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> s. f x = a)))" (is ?thesis2)
   8.575 +  and continuous_finite_range_constant_eq:
   8.576 +      "(connected s \<longleftrightarrow>
   8.577 +         (\<forall>f::'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1.
   8.578 +          continuous_on s f \<and> finite (f ` s)
   8.579 +          \<longrightarrow> (\<exists>a::'b. \<forall>x \<in> s. f x = a)))" (is ?thesis3)
   8.580 +proof -
   8.581 +  have *: "\<And>s t u v. \<lbrakk>s \<Longrightarrow> t; t \<Longrightarrow> u; u \<Longrightarrow> v; v \<Longrightarrow> s\<rbrakk>
   8.582 +    \<Longrightarrow> (s \<longleftrightarrow> t) \<and> (s \<longleftrightarrow> u) \<and> (s \<longleftrightarrow> v)"
   8.583 +    by blast
   8.584 +  have "?thesis1 \<and> ?thesis2 \<and> ?thesis3"
   8.585 +    apply (rule *)
   8.586 +    using continuous_disconnected_range_constant apply metis
   8.587 +    apply clarify
   8.588 +    apply (frule discrete_subset_disconnected; blast)
   8.589 +    apply (blast dest: finite_implies_discrete)
   8.590 +    apply (blast intro!: finite_range_constant_imp_connected)
   8.591 +    done
   8.592 +  then show ?thesis1 ?thesis2 ?thesis3
   8.593 +    by blast+
   8.594 +qed
   8.595 +
   8.596 +lemma continuous_discrete_range_constant:
   8.597 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1"
   8.598 +  assumes s: "connected s"
   8.599 +      and "continuous_on s f"
   8.600 +      and "\<And>x. x \<in> s \<Longrightarrow> \<exists>e>0. \<forall>y. y \<in> s \<and> f y \<noteq> f x \<longrightarrow> e \<le> norm (f y - f x)"
   8.601 +    shows "\<exists>a. \<forall>x \<in> s. f x = a"
   8.602 +  using continuous_discrete_range_constant_eq [THEN iffD1, OF s] assms
   8.603 +  by blast
   8.604 +
   8.605 +lemma continuous_finite_range_constant:
   8.606 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra_1"
   8.607 +  assumes "connected s"
   8.608 +      and "continuous_on s f"
   8.609 +      and "finite (f ` s)"
   8.610 +    shows "\<exists>a. \<forall>x \<in> s. f x = a"
   8.611 +  using assms continuous_finite_range_constant_eq
   8.612 +  by blast
   8.613 +
   8.614  
   8.615  no_notation
   8.616    eucl_less (infix "<e" 50)
     9.1 --- a/src/HOL/Complex.thy	Tue Jan 03 23:21:09 2017 +0100
     9.2 +++ b/src/HOL/Complex.thy	Wed Jan 04 16:18:50 2017 +0000
     9.3 @@ -437,6 +437,14 @@
     9.4    "continuous F f \<longleftrightarrow> continuous F (\<lambda>x. Re (f x)) \<and> continuous F (\<lambda>x. Im (f x))"
     9.5    by (simp only: continuous_def tendsto_complex_iff)
     9.6  
     9.7 +lemma continuous_on_of_real_o_iff [simp]:
     9.8 +     "continuous_on S (\<lambda>x. complex_of_real (g x)) = continuous_on S g"
     9.9 +  using continuous_on_Re continuous_on_of_real  by fastforce
    9.10 +
    9.11 +lemma continuous_on_of_real_id [simp]:
    9.12 +     "continuous_on S (of_real :: real \<Rightarrow> 'a::real_normed_algebra_1)"
    9.13 +  by (rule continuous_on_of_real [OF continuous_on_id])
    9.14 +
    9.15  lemma has_vector_derivative_complex_iff: "(f has_vector_derivative x) F \<longleftrightarrow>
    9.16      ((\<lambda>x. Re (f x)) has_field_derivative (Re x)) F \<and>
    9.17      ((\<lambda>x. Im (f x)) has_field_derivative (Im x)) F"
    10.1 --- a/src/HOL/Number_Theory/Primes.thy	Tue Jan 03 23:21:09 2017 +0100
    10.2 +++ b/src/HOL/Number_Theory/Primes.thy	Wed Jan 04 16:18:50 2017 +0000
    10.3 @@ -194,6 +194,64 @@
    10.4    using assms irreducible_altdef[of m]
    10.5    by (auto simp: prime_elem_iff_irreducible prime_def irreducible_altdef)
    10.6  
    10.7 +    
    10.8 +subsection\<open>Largest exponent of a prime factor\<close>
    10.9 +text\<open>Possibly duplicates other material, but avoid the complexities of multisets.\<close>
   10.10 +  
   10.11 +lemma prime_power_cancel_less:
   10.12 +  assumes "prime p" and eq: "m * (p ^ k) = m' * (p ^ k')" and less: "k < k'" and "\<not> p dvd m"
   10.13 +  shows False
   10.14 +proof -
   10.15 +  obtain l where l: "k' = k + l" and "l > 0"
   10.16 +    using less less_imp_add_positive by auto
   10.17 +  have "m = m * (p ^ k) div (p ^ k)"
   10.18 +    using \<open>prime p\<close> by simp
   10.19 +  also have "\<dots> = m' * (p ^ k') div (p ^ k)"
   10.20 +    using eq by simp
   10.21 +  also have "\<dots> = m' * (p ^ l) * (p ^ k) div (p ^ k)"
   10.22 +    by (simp add: l mult.commute mult.left_commute power_add)
   10.23 +  also have "... = m' * (p ^ l)"
   10.24 +    using \<open>prime p\<close> by simp
   10.25 +  finally have "p dvd m"
   10.26 +    using \<open>l > 0\<close> by simp
   10.27 +  with assms show False
   10.28 +    by simp
   10.29 +qed
   10.30 +
   10.31 +lemma prime_power_cancel:
   10.32 +  assumes "prime p" and eq: "m * (p ^ k) = m' * (p ^ k')" and "\<not> p dvd m" "\<not> p dvd m'"
   10.33 +  shows "k = k'"
   10.34 +  using prime_power_cancel_less [OF \<open>prime p\<close>] assms
   10.35 +  by (metis linorder_neqE_nat)
   10.36 +
   10.37 +lemma prime_power_cancel2:
   10.38 +  assumes "prime p" "m * (p ^ k) = m' * (p ^ k')" "\<not> p dvd m" "\<not> p dvd m'"
   10.39 +  obtains "m = m'" "k = k'"
   10.40 +  using prime_power_cancel [OF assms] assms by auto
   10.41 +
   10.42 +lemma prime_power_canonical:
   10.43 +  fixes m::nat
   10.44 +  assumes "prime p" "m > 0"
   10.45 +  shows "\<exists>k n. \<not> p dvd n \<and> m = n * p^k"
   10.46 +using \<open>m > 0\<close>
   10.47 +proof (induction m rule: less_induct)
   10.48 +  case (less m)
   10.49 +  show ?case
   10.50 +  proof (cases "p dvd m")
   10.51 +    case True
   10.52 +    then obtain m' where m': "m = p * m'"
   10.53 +      using dvdE by blast
   10.54 +    with \<open>prime p\<close> have "0 < m'" "m' < m"
   10.55 +      using less.prems prime_nat_iff by auto
   10.56 +    with m' less show ?thesis
   10.57 +      by (metis power_Suc mult.left_commute)
   10.58 +  next
   10.59 +    case False
   10.60 +    then show ?thesis
   10.61 +      by (metis mult.right_neutral power_0)
   10.62 +  qed
   10.63 +qed
   10.64 +
   10.65  
   10.66  subsubsection \<open>Make prime naively executable\<close>
   10.67  
    11.1 --- a/src/HOL/Set_Interval.thy	Tue Jan 03 23:21:09 2017 +0100
    11.2 +++ b/src/HOL/Set_Interval.thy	Wed Jan 04 16:18:50 2017 +0000
    11.3 @@ -1090,6 +1090,19 @@
    11.4       "!!f::nat=>nat. (!!n. n \<le> f n) ==> finite {n. f n \<le> u}"
    11.5  by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)
    11.6  
    11.7 +lemma bounded_Max_nat:
    11.8 +  fixes P :: "nat \<Rightarrow> bool"
    11.9 +  assumes x: "P x" and M: "\<And>x. P x \<Longrightarrow> x \<le> M"
   11.10 +  obtains m where "P m" "\<And>x. P x \<Longrightarrow> x \<le> m"
   11.11 +proof -
   11.12 +  have "finite {x. P x}"
   11.13 +    using M finite_nat_set_iff_bounded_le by auto
   11.14 +  then have "Max {x. P x} \<in> {x. P x}"
   11.15 +    using Max_in x by auto
   11.16 +  then show ?thesis
   11.17 +    by (simp add: \<open>finite {x. P x}\<close> that)
   11.18 +qed
   11.19 +
   11.20  
   11.21  text\<open>Any subset of an interval of natural numbers the size of the
   11.22  subset is exactly that interval.\<close>
    12.1 --- a/src/HOL/Topological_Spaces.thy	Tue Jan 03 23:21:09 2017 +0100
    12.2 +++ b/src/HOL/Topological_Spaces.thy	Wed Jan 04 16:18:50 2017 +0000
    12.3 @@ -1530,9 +1530,6 @@
    12.4  lemma tendsto_compose: "g \<midarrow>l\<rightarrow> g l \<Longrightarrow> (f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) \<longlongrightarrow> g l) F"
    12.5    unfolding tendsto_at_iff_tendsto_nhds by (rule filterlim_compose[of g])
    12.6  
    12.7 -lemma LIM_o: "g \<midarrow>l\<rightarrow> g l \<Longrightarrow> f \<midarrow>a\<rightarrow> l \<Longrightarrow> (g \<circ> f) \<midarrow>a\<rightarrow> g l"
    12.8 -  unfolding o_def by (rule tendsto_compose)
    12.9 -
   12.10  lemma tendsto_compose_eventually:
   12.11    "g \<midarrow>l\<rightarrow> m \<Longrightarrow> (f \<longlongrightarrow> l) F \<Longrightarrow> eventually (\<lambda>x. f x \<noteq> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) \<longlongrightarrow> m) F"
   12.12    by (rule filterlim_compose[of g _ "at l"]) (auto simp add: filterlim_at)