more from moretop.ml
authorpaulson <lp15@cam.ac.uk>
Tue Oct 18 15:55:53 2016 +0100 (2016-10-18)
changeset 64287d85d88722745
parent 64284 f3b905b2eee2
child 64288 4750673a96da
more from moretop.ml
src/HOL/Analysis/Bochner_Integration.thy
src/HOL/Analysis/Borel_Space.thy
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/Derivative.thy
src/HOL/Analysis/FurtherTopology.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
src/HOL/Limits.thy
src/HOL/Orderings.thy
     1.1 --- a/src/HOL/Analysis/Bochner_Integration.thy	Tue Oct 18 12:01:54 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Bochner_Integration.thy	Tue Oct 18 15:55:53 2016 +0100
     1.3 @@ -1157,7 +1157,7 @@
     1.4    let ?s = "\<lambda>n. simple_bochner_integral M (s n)"
     1.5  
     1.6    have "\<exists>x. ?s \<longlonglongrightarrow> x"
     1.7 -    unfolding convergent_eq_cauchy
     1.8 +    unfolding convergent_eq_Cauchy
     1.9    proof (rule metric_CauchyI)
    1.10      fix e :: real assume "0 < e"
    1.11      then have "0 < ennreal (e / 2)" by auto
     2.1 --- a/src/HOL/Analysis/Borel_Space.thy	Tue Oct 18 12:01:54 2016 +0200
     2.2 +++ b/src/HOL/Analysis/Borel_Space.thy	Tue Oct 18 15:55:53 2016 +0100
     2.3 @@ -1797,13 +1797,13 @@
     2.4  proof -
     2.5    define u' where "u' x = lim (\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0)" for x
     2.6    then have *: "\<And>x. lim (\<lambda>i. f i x) = (if Cauchy (\<lambda>i. f i x) then u' x else (THE x. False))"
     2.7 -    by (auto simp: lim_def convergent_eq_cauchy[symmetric])
     2.8 +    by (auto simp: lim_def convergent_eq_Cauchy[symmetric])
     2.9    have "u' \<in> borel_measurable M"
    2.10    proof (rule borel_measurable_LIMSEQ_metric)
    2.11      fix x
    2.12      have "convergent (\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0)"
    2.13        by (cases "Cauchy (\<lambda>i. f i x)")
    2.14 -         (auto simp add: convergent_eq_cauchy[symmetric] convergent_def)
    2.15 +         (auto simp add: convergent_eq_Cauchy[symmetric] convergent_def)
    2.16      then show "(\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0) \<longlonglongrightarrow> u' x"
    2.17        unfolding u'_def
    2.18        by (rule convergent_LIMSEQ_iff[THEN iffD1])
     3.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Oct 18 12:01:54 2016 +0200
     3.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Oct 18 15:55:53 2016 +0100
     3.3 @@ -236,6 +236,23 @@
     3.4    finally show ?thesis .
     3.5  qed
     3.6  
     3.7 +lemma exp_plus_2pin [simp]: "exp (z + \<i> * (of_int n * (of_real pi * 2))) = exp z"
     3.8 +  by (simp add: exp_eq)
     3.9 +
    3.10 +lemma inj_on_exp_pi:
    3.11 +  fixes z::complex shows "inj_on exp (ball z pi)"
    3.12 +proof (clarsimp simp: inj_on_def exp_eq)
    3.13 +  fix y n
    3.14 +  assume "dist z (y + 2 * of_int n * of_real pi * \<i>) < pi"
    3.15 +         "dist z y < pi"
    3.16 +  then have "dist y (y + 2 * of_int n * of_real pi * \<i>) < pi+pi"
    3.17 +    using dist_commute_lessI dist_triangle_less_add by blast
    3.18 +  then have "norm (2 * of_int n * of_real pi * \<i>) < 2*pi"
    3.19 +    by (simp add: dist_norm)
    3.20 +  then show "n = 0"
    3.21 +    by (auto simp: norm_mult)
    3.22 +qed
    3.23 +
    3.24  lemma sin_cos_eq_iff: "sin y = sin x \<and> cos y = cos x \<longleftrightarrow> (\<exists>n::int. y = x + 2 * n * pi)"
    3.25  proof -
    3.26    { assume "sin y = sin x" "cos y = cos x"
     4.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Oct 18 12:01:54 2016 +0200
     4.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Oct 18 15:55:53 2016 +0100
     4.3 @@ -4378,6 +4378,15 @@
     4.4  definition "rel_interior S =
     4.5    {x. \<exists>T. openin (subtopology euclidean (affine hull S)) T \<and> x \<in> T \<and> T \<subseteq> S}"
     4.6  
     4.7 +lemma rel_interior_mono:
     4.8 +   "\<lbrakk>S \<subseteq> T; affine hull S = affine hull T\<rbrakk>
     4.9 +   \<Longrightarrow> (rel_interior S) \<subseteq> (rel_interior T)"
    4.10 +  by (auto simp: rel_interior_def)
    4.11 +
    4.12 +lemma rel_interior_maximal:
    4.13 +   "\<lbrakk>T \<subseteq> S; openin(subtopology euclidean (affine hull S)) T\<rbrakk> \<Longrightarrow> T \<subseteq> (rel_interior S)"
    4.14 +  by (auto simp: rel_interior_def)
    4.15 +
    4.16  lemma rel_interior:
    4.17    "rel_interior S = {x \<in> S. \<exists>T. open T \<and> x \<in> T \<and> T \<inter> affine hull S \<subseteq> S}"
    4.18    unfolding rel_interior_def[of S] openin_open[of "affine hull S"]
     5.1 --- a/src/HOL/Analysis/Derivative.thy	Tue Oct 18 12:01:54 2016 +0200
     5.2 +++ b/src/HOL/Analysis/Derivative.thy	Tue Oct 18 15:55:53 2016 +0100
     5.3 @@ -1922,7 +1922,7 @@
     5.4      using assms(1,2,3) by (rule has_derivative_sequence_lipschitz)
     5.5    have "\<exists>g. \<forall>x\<in>s. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially"
     5.6      apply (rule bchoice)
     5.7 -    unfolding convergent_eq_cauchy
     5.8 +    unfolding convergent_eq_Cauchy
     5.9    proof
    5.10      fix x
    5.11      assume "x \<in> s"
     6.1 --- a/src/HOL/Analysis/FurtherTopology.thy	Tue Oct 18 12:01:54 2016 +0200
     6.2 +++ b/src/HOL/Analysis/FurtherTopology.thy	Tue Oct 18 15:55:53 2016 +0100
     6.3 @@ -3,7 +3,7 @@
     6.4  text\<open>Ported from HOL Light (moretop.ml) by L C Paulson\<close>
     6.5  
     6.6  theory "FurtherTopology"
     6.7 -  imports Equivalence_Lebesgue_Henstock_Integration Weierstrass_Theorems Polytope
     6.8 +  imports Equivalence_Lebesgue_Henstock_Integration Weierstrass_Theorems Polytope Complex_Transcendental
     6.9  
    6.10  begin
    6.11  
    6.12 @@ -2352,4 +2352,747 @@
    6.13    using invariance_of_domain_homeomorphism [OF assms]
    6.14    by (meson homeomorphic_def)
    6.15  
    6.16 +lemma continuous_image_subset_interior:
    6.17 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
    6.18 +  assumes "continuous_on S f" "inj_on f S" "DIM('b) \<le> DIM('a)"
    6.19 +  shows "f ` (interior S) \<subseteq> interior(f ` S)"
    6.20 +  apply (rule interior_maximal)
    6.21 +   apply (simp add: image_mono interior_subset)
    6.22 +  apply (rule invariance_of_domain_gen)
    6.23 +  using assms
    6.24 +     apply (auto simp: subset_inj_on interior_subset continuous_on_subset)
    6.25 +  done
    6.26 +
    6.27 +lemma homeomorphic_interiors_same_dimension:
    6.28 +  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
    6.29 +  assumes "S homeomorphic T" and dimeq: "DIM('a) = DIM('b)"
    6.30 +  shows "(interior S) homeomorphic (interior T)"
    6.31 +  using assms [unfolded homeomorphic_minimal]
    6.32 +  unfolding homeomorphic_def
    6.33 +proof (clarify elim!: ex_forward)
    6.34 +  fix f g
    6.35 +  assume S: "\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x" and T: "\<forall>y\<in>T. g y \<in> S \<and> f (g y) = y"
    6.36 +     and contf: "continuous_on S f" and contg: "continuous_on T g"
    6.37 +  then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T"
    6.38 +    by (auto simp: inj_on_def intro: rev_image_eqI) metis+
    6.39 +  have fim: "f ` interior S \<subseteq> interior T"
    6.40 +    using continuous_image_subset_interior [OF contf \<open>inj_on f S\<close>] dimeq fST by simp
    6.41 +  have gim: "g ` interior T \<subseteq> interior S"
    6.42 +    using continuous_image_subset_interior [OF contg \<open>inj_on g T\<close>] dimeq gTS by simp
    6.43 +  show "homeomorphism (interior S) (interior T) f g"
    6.44 +    unfolding homeomorphism_def
    6.45 +  proof (intro conjI ballI)
    6.46 +    show "\<And>x. x \<in> interior S \<Longrightarrow> g (f x) = x"
    6.47 +      by (meson \<open>\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x\<close> subsetD interior_subset)
    6.48 +    have "interior T \<subseteq> f ` interior S"
    6.49 +    proof
    6.50 +      fix x assume "x \<in> interior T"
    6.51 +      then have "g x \<in> interior S"
    6.52 +        using gim by blast
    6.53 +      then show "x \<in> f ` interior S"
    6.54 +        by (metis T \<open>x \<in> interior T\<close> image_iff interior_subset subsetCE)
    6.55 +    qed
    6.56 +    then show "f ` interior S = interior T"
    6.57 +      using fim by blast
    6.58 +    show "continuous_on (interior S) f"
    6.59 +      by (metis interior_subset continuous_on_subset contf)
    6.60 +    show "\<And>y. y \<in> interior T \<Longrightarrow> f (g y) = y"
    6.61 +      by (meson T subsetD interior_subset)
    6.62 +    have "interior S \<subseteq> g ` interior T"
    6.63 +    proof
    6.64 +      fix x assume "x \<in> interior S"
    6.65 +      then have "f x \<in> interior T"
    6.66 +        using fim by blast
    6.67 +      then show "x \<in> g ` interior T"
    6.68 +        by (metis S \<open>x \<in> interior S\<close> image_iff interior_subset subsetCE)
    6.69 +    qed
    6.70 +    then show "g ` interior T = interior S"
    6.71 +      using gim by blast
    6.72 +    show "continuous_on (interior T) g"
    6.73 +      by (metis interior_subset continuous_on_subset contg)
    6.74 +  qed
    6.75 +qed
    6.76 +
    6.77 +lemma homeomorphic_open_imp_same_dimension:
    6.78 +  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
    6.79 +  assumes "S homeomorphic T" "open S" "S \<noteq> {}" "open T" "T \<noteq> {}"
    6.80 +  shows "DIM('a) = DIM('b)"
    6.81 +    using assms
    6.82 +    apply (simp add: homeomorphic_minimal)
    6.83 +    apply (rule order_antisym; metis inj_onI invariance_of_dimension)
    6.84 +    done
    6.85 +
    6.86 +lemma homeomorphic_interiors:
    6.87 +  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
    6.88 +  assumes "S homeomorphic T" "interior S = {} \<longleftrightarrow> interior T = {}"
    6.89 +    shows "(interior S) homeomorphic (interior T)"
    6.90 +proof (cases "interior T = {}")
    6.91 +  case True
    6.92 +  with assms show ?thesis by auto
    6.93 +next
    6.94 +  case False
    6.95 +  then have "DIM('a) = DIM('b)"
    6.96 +    using assms
    6.97 +    apply (simp add: homeomorphic_minimal)
    6.98 +    apply (rule order_antisym; metis continuous_on_subset inj_onI inj_on_subset interior_subset invariance_of_dimension open_interior)
    6.99 +    done
   6.100 +  then show ?thesis
   6.101 +    by (rule homeomorphic_interiors_same_dimension [OF \<open>S homeomorphic T\<close>])
   6.102 +qed
   6.103 +
   6.104 +lemma homeomorphic_frontiers_same_dimension:
   6.105 +  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   6.106 +  assumes "S homeomorphic T" "closed S" "closed T" and dimeq: "DIM('a) = DIM('b)"
   6.107 +  shows "(frontier S) homeomorphic (frontier T)"
   6.108 +  using assms [unfolded homeomorphic_minimal]
   6.109 +  unfolding homeomorphic_def
   6.110 +proof (clarify elim!: ex_forward)
   6.111 +  fix f g
   6.112 +  assume S: "\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x" and T: "\<forall>y\<in>T. g y \<in> S \<and> f (g y) = y"
   6.113 +     and contf: "continuous_on S f" and contg: "continuous_on T g"
   6.114 +  then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T"
   6.115 +    by (auto simp: inj_on_def intro: rev_image_eqI) metis+
   6.116 +  have "g ` interior T \<subseteq> interior S"
   6.117 +    using continuous_image_subset_interior [OF contg \<open>inj_on g T\<close>] dimeq gTS by simp
   6.118 +  then have fim: "f ` frontier S \<subseteq> frontier T"
   6.119 +    apply (simp add: frontier_def)
   6.120 +    using continuous_image_subset_interior assms(2) assms(3) S by auto
   6.121 +  have "f ` interior S \<subseteq> interior T"
   6.122 +    using continuous_image_subset_interior [OF contf \<open>inj_on f S\<close>] dimeq fST by simp
   6.123 +  then have gim: "g ` frontier T \<subseteq> frontier S"
   6.124 +    apply (simp add: frontier_def)
   6.125 +    using continuous_image_subset_interior T assms(2) assms(3) by auto
   6.126 +  show "homeomorphism (frontier S) (frontier T) f g"
   6.127 +    unfolding homeomorphism_def
   6.128 +  proof (intro conjI ballI)
   6.129 +    show gf: "\<And>x. x \<in> frontier S \<Longrightarrow> g (f x) = x"
   6.130 +      by (simp add: S assms(2) frontier_def)
   6.131 +    show fg: "\<And>y. y \<in> frontier T \<Longrightarrow> f (g y) = y"
   6.132 +      by (simp add: T assms(3) frontier_def)
   6.133 +    have "frontier T \<subseteq> f ` frontier S"
   6.134 +    proof
   6.135 +      fix x assume "x \<in> frontier T"
   6.136 +      then have "g x \<in> frontier S"
   6.137 +        using gim by blast
   6.138 +      then show "x \<in> f ` frontier S"
   6.139 +        by (metis fg \<open>x \<in> frontier T\<close> imageI)
   6.140 +    qed
   6.141 +    then show "f ` frontier S = frontier T"
   6.142 +      using fim by blast
   6.143 +    show "continuous_on (frontier S) f"
   6.144 +      by (metis Diff_subset assms(2) closure_eq contf continuous_on_subset frontier_def)
   6.145 +    have "frontier S \<subseteq> g ` frontier T"
   6.146 +    proof
   6.147 +      fix x assume "x \<in> frontier S"
   6.148 +      then have "f x \<in> frontier T"
   6.149 +        using fim by blast
   6.150 +      then show "x \<in> g ` frontier T"
   6.151 +        by (metis gf \<open>x \<in> frontier S\<close> imageI)
   6.152 +    qed
   6.153 +    then show "g ` frontier T = frontier S"
   6.154 +      using gim by blast
   6.155 +    show "continuous_on (frontier T) g"
   6.156 +      by (metis Diff_subset assms(3) closure_closed contg continuous_on_subset frontier_def)
   6.157 +  qed
   6.158 +qed
   6.159 +
   6.160 +lemma homeomorphic_frontiers:
   6.161 +  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   6.162 +  assumes "S homeomorphic T" "closed S" "closed T"
   6.163 +          "interior S = {} \<longleftrightarrow> interior T = {}"
   6.164 +    shows "(frontier S) homeomorphic (frontier T)"
   6.165 +proof (cases "interior T = {}")
   6.166 +  case True
   6.167 +  then show ?thesis
   6.168 +    by (metis Diff_empty assms closure_eq frontier_def)
   6.169 +next
   6.170 +  case False
   6.171 +  show ?thesis
   6.172 +    apply (rule homeomorphic_frontiers_same_dimension)
   6.173 +       apply (simp_all add: assms)
   6.174 +    using False assms homeomorphic_interiors homeomorphic_open_imp_same_dimension by blast
   6.175 +qed
   6.176 +
   6.177 +lemma continuous_image_subset_rel_interior:
   6.178 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   6.179 +  assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \<subseteq> T"
   6.180 +      and TS: "aff_dim T \<le> aff_dim S"
   6.181 +  shows "f ` (rel_interior S) \<subseteq> rel_interior(f ` S)"
   6.182 +proof (rule rel_interior_maximal)
   6.183 +  show "f ` rel_interior S \<subseteq> f ` S"
   6.184 +    by(simp add: image_mono rel_interior_subset)
   6.185 +  show "openin (subtopology euclidean (affine hull f ` S)) (f ` rel_interior S)"
   6.186 +  proof (rule invariance_of_domain_affine_sets)
   6.187 +    show "openin (subtopology euclidean (affine hull S)) (rel_interior S)"
   6.188 +      by (simp add: openin_rel_interior)
   6.189 +    show "aff_dim (affine hull f ` S) \<le> aff_dim (affine hull S)"
   6.190 +      by (metis aff_dim_affine_hull aff_dim_subset fim TS order_trans)
   6.191 +    show "f ` rel_interior S \<subseteq> affine hull f ` S"
   6.192 +      by (meson \<open>f ` rel_interior S \<subseteq> f ` S\<close> hull_subset order_trans)
   6.193 +    show "continuous_on (rel_interior S) f"
   6.194 +      using contf continuous_on_subset rel_interior_subset by blast
   6.195 +    show "inj_on f (rel_interior S)"
   6.196 +      using inj_on_subset injf rel_interior_subset by blast
   6.197 +  qed auto
   6.198 +qed
   6.199 +
   6.200 +lemma homeomorphic_rel_interiors_same_dimension:
   6.201 +  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   6.202 +  assumes "S homeomorphic T" and aff: "aff_dim S = aff_dim T"
   6.203 +  shows "(rel_interior S) homeomorphic (rel_interior T)"
   6.204 +  using assms [unfolded homeomorphic_minimal]
   6.205 +  unfolding homeomorphic_def
   6.206 +proof (clarify elim!: ex_forward)
   6.207 +  fix f g
   6.208 +  assume S: "\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x" and T: "\<forall>y\<in>T. g y \<in> S \<and> f (g y) = y"
   6.209 +     and contf: "continuous_on S f" and contg: "continuous_on T g"
   6.210 +  then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T"
   6.211 +    by (auto simp: inj_on_def intro: rev_image_eqI) metis+
   6.212 +  have fim: "f ` rel_interior S \<subseteq> rel_interior T"
   6.213 +    by (metis \<open>inj_on f S\<close> aff contf continuous_image_subset_rel_interior fST order_refl)
   6.214 +  have gim: "g ` rel_interior T \<subseteq> rel_interior S"
   6.215 +    by (metis \<open>inj_on g T\<close> aff contg continuous_image_subset_rel_interior gTS order_refl)
   6.216 +  show "homeomorphism (rel_interior S) (rel_interior T) f g"
   6.217 +    unfolding homeomorphism_def
   6.218 +  proof (intro conjI ballI)
   6.219 +    show gf: "\<And>x. x \<in> rel_interior S \<Longrightarrow> g (f x) = x"
   6.220 +      using S rel_interior_subset by blast
   6.221 +    show fg: "\<And>y. y \<in> rel_interior T \<Longrightarrow> f (g y) = y"
   6.222 +      using T mem_rel_interior_ball by blast
   6.223 +    have "rel_interior T \<subseteq> f ` rel_interior S"
   6.224 +    proof
   6.225 +      fix x assume "x \<in> rel_interior T"
   6.226 +      then have "g x \<in> rel_interior S"
   6.227 +        using gim by blast
   6.228 +      then show "x \<in> f ` rel_interior S"
   6.229 +        by (metis fg \<open>x \<in> rel_interior T\<close> imageI)
   6.230 +    qed
   6.231 +    moreover have "f ` rel_interior S \<subseteq> rel_interior T"
   6.232 +      by (metis \<open>inj_on f S\<close> aff contf continuous_image_subset_rel_interior fST order_refl)
   6.233 +    ultimately show "f ` rel_interior S = rel_interior T"
   6.234 +      by blast
   6.235 +    show "continuous_on (rel_interior S) f"
   6.236 +      using contf continuous_on_subset rel_interior_subset by blast
   6.237 +    have "rel_interior S \<subseteq> g ` rel_interior T"
   6.238 +    proof
   6.239 +      fix x assume "x \<in> rel_interior S"
   6.240 +      then have "f x \<in> rel_interior T"
   6.241 +        using fim by blast
   6.242 +      then show "x \<in> g ` rel_interior T"
   6.243 +        by (metis gf \<open>x \<in> rel_interior S\<close> imageI)
   6.244 +    qed
   6.245 +    then show "g ` rel_interior T = rel_interior S"
   6.246 +      using gim by blast
   6.247 +    show "continuous_on (rel_interior T) g"
   6.248 +      using contg continuous_on_subset rel_interior_subset by blast
   6.249 +  qed
   6.250 +qed
   6.251 +
   6.252 +lemma homeomorphic_rel_interiors:
   6.253 +  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   6.254 +  assumes "S homeomorphic T" "rel_interior S = {} \<longleftrightarrow> rel_interior T = {}"
   6.255 +    shows "(rel_interior S) homeomorphic (rel_interior T)"
   6.256 +proof (cases "rel_interior T = {}")
   6.257 +  case True
   6.258 +  with assms show ?thesis by auto
   6.259 +next
   6.260 +  case False
   6.261 +  obtain f g
   6.262 +    where S: "\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x" and T: "\<forall>y\<in>T. g y \<in> S \<and> f (g y) = y"
   6.263 +      and contf: "continuous_on S f" and contg: "continuous_on T g"
   6.264 +    using  assms [unfolded homeomorphic_minimal] by auto
   6.265 +  have "aff_dim (affine hull S) \<le> aff_dim (affine hull T)"
   6.266 +    apply (rule invariance_of_dimension_affine_sets [of _ "rel_interior S" _ f])
   6.267 +          apply (simp_all add: openin_rel_interior False assms)
   6.268 +    using contf continuous_on_subset rel_interior_subset apply blast
   6.269 +      apply (meson S hull_subset image_subsetI rel_interior_subset rev_subsetD)
   6.270 +    apply (metis S inj_on_inverseI inj_on_subset rel_interior_subset)
   6.271 +    done
   6.272 +  moreover have "aff_dim (affine hull T) \<le> aff_dim (affine hull S)"
   6.273 +    apply (rule invariance_of_dimension_affine_sets [of _ "rel_interior T" _ g])
   6.274 +          apply (simp_all add: openin_rel_interior False assms)
   6.275 +    using contg continuous_on_subset rel_interior_subset apply blast
   6.276 +      apply (meson T hull_subset image_subsetI rel_interior_subset rev_subsetD)
   6.277 +    apply (metis T inj_on_inverseI inj_on_subset rel_interior_subset)
   6.278 +    done
   6.279 +  ultimately have "aff_dim S = aff_dim T" by force
   6.280 +  then show ?thesis
   6.281 +    by (rule homeomorphic_rel_interiors_same_dimension [OF \<open>S homeomorphic T\<close>])
   6.282 +qed
   6.283 +
   6.284 +
   6.285 +lemma homeomorphic_rel_boundaries_same_dimension:
   6.286 +  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   6.287 +  assumes "S homeomorphic T" and aff: "aff_dim S = aff_dim T"
   6.288 +  shows "(S - rel_interior S) homeomorphic (T - rel_interior T)"
   6.289 +  using assms [unfolded homeomorphic_minimal]
   6.290 +  unfolding homeomorphic_def
   6.291 +proof (clarify elim!: ex_forward)
   6.292 +  fix f g
   6.293 +  assume S: "\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x" and T: "\<forall>y\<in>T. g y \<in> S \<and> f (g y) = y"
   6.294 +     and contf: "continuous_on S f" and contg: "continuous_on T g"
   6.295 +  then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T"
   6.296 +    by (auto simp: inj_on_def intro: rev_image_eqI) metis+
   6.297 +  have fim: "f ` rel_interior S \<subseteq> rel_interior T"
   6.298 +    by (metis \<open>inj_on f S\<close> aff contf continuous_image_subset_rel_interior fST order_refl)
   6.299 +  have gim: "g ` rel_interior T \<subseteq> rel_interior S"
   6.300 +    by (metis \<open>inj_on g T\<close> aff contg continuous_image_subset_rel_interior gTS order_refl)
   6.301 +  show "homeomorphism (S - rel_interior S) (T - rel_interior T) f g"
   6.302 +    unfolding homeomorphism_def
   6.303 +  proof (intro conjI ballI)
   6.304 +    show gf: "\<And>x. x \<in> S - rel_interior S \<Longrightarrow> g (f x) = x"
   6.305 +      using S rel_interior_subset by blast
   6.306 +    show fg: "\<And>y. y \<in> T - rel_interior T \<Longrightarrow> f (g y) = y"
   6.307 +      using T mem_rel_interior_ball by blast
   6.308 +    show "f ` (S - rel_interior S) = T - rel_interior T"
   6.309 +      using S fST fim gim by auto
   6.310 +    show "continuous_on (S - rel_interior S) f"
   6.311 +      using contf continuous_on_subset rel_interior_subset by blast
   6.312 +    show "g ` (T - rel_interior T) = S - rel_interior S"
   6.313 +      using T gTS gim fim by auto
   6.314 +    show "continuous_on (T - rel_interior T) g"
   6.315 +      using contg continuous_on_subset rel_interior_subset by blast
   6.316 +  qed
   6.317 +qed
   6.318 +
   6.319 +lemma homeomorphic_rel_boundaries:
   6.320 +  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   6.321 +  assumes "S homeomorphic T" "rel_interior S = {} \<longleftrightarrow> rel_interior T = {}"
   6.322 +    shows "(S - rel_interior S) homeomorphic (T - rel_interior T)"
   6.323 +proof (cases "rel_interior T = {}")
   6.324 +  case True
   6.325 +  with assms show ?thesis by auto
   6.326 +next
   6.327 +  case False
   6.328 +  obtain f g
   6.329 +    where S: "\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x" and T: "\<forall>y\<in>T. g y \<in> S \<and> f (g y) = y"
   6.330 +      and contf: "continuous_on S f" and contg: "continuous_on T g"
   6.331 +    using  assms [unfolded homeomorphic_minimal] by auto
   6.332 +  have "aff_dim (affine hull S) \<le> aff_dim (affine hull T)"
   6.333 +    apply (rule invariance_of_dimension_affine_sets [of _ "rel_interior S" _ f])
   6.334 +          apply (simp_all add: openin_rel_interior False assms)
   6.335 +    using contf continuous_on_subset rel_interior_subset apply blast
   6.336 +      apply (meson S hull_subset image_subsetI rel_interior_subset rev_subsetD)
   6.337 +    apply (metis S inj_on_inverseI inj_on_subset rel_interior_subset)
   6.338 +    done
   6.339 +  moreover have "aff_dim (affine hull T) \<le> aff_dim (affine hull S)"
   6.340 +    apply (rule invariance_of_dimension_affine_sets [of _ "rel_interior T" _ g])
   6.341 +          apply (simp_all add: openin_rel_interior False assms)
   6.342 +    using contg continuous_on_subset rel_interior_subset apply blast
   6.343 +      apply (meson T hull_subset image_subsetI rel_interior_subset rev_subsetD)
   6.344 +    apply (metis T inj_on_inverseI inj_on_subset rel_interior_subset)
   6.345 +    done
   6.346 +  ultimately have "aff_dim S = aff_dim T" by force
   6.347 +  then show ?thesis
   6.348 +    by (rule homeomorphic_rel_boundaries_same_dimension [OF \<open>S homeomorphic T\<close>])
   6.349 +qed
   6.350 +
   6.351 +proposition uniformly_continuous_homeomorphism_UNIV_trivial:
   6.352 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
   6.353 +  assumes contf: "uniformly_continuous_on S f" and hom: "homeomorphism S UNIV f g"
   6.354 +  shows "S = UNIV"
   6.355 +proof (cases "S = {}")
   6.356 +  case True
   6.357 +  then show ?thesis
   6.358 +    by (metis UNIV_I hom empty_iff homeomorphism_def image_eqI)
   6.359 +next
   6.360 +  case False
   6.361 +  have "inj g"
   6.362 +    by (metis UNIV_I hom homeomorphism_apply2 injI)
   6.363 +  then have "open (g ` UNIV)"
   6.364 +    by (blast intro: invariance_of_domain hom homeomorphism_cont2)
   6.365 +  then have "open S"
   6.366 +    using hom homeomorphism_image2 by blast
   6.367 +  moreover have "complete S"
   6.368 +    unfolding complete_def
   6.369 +  proof clarify
   6.370 +    fix \<sigma>
   6.371 +    assume \<sigma>: "\<forall>n. \<sigma> n \<in> S" and "Cauchy \<sigma>"
   6.372 +    have "Cauchy (f o \<sigma>)"
   6.373 +      using uniformly_continuous_imp_Cauchy_continuous \<open>Cauchy \<sigma>\<close> \<sigma> contf by blast
   6.374 +    then obtain l where "(f \<circ> \<sigma>) \<longlonglongrightarrow> l"
   6.375 +      by (auto simp: convergent_eq_Cauchy [symmetric])
   6.376 +    show "\<exists>l\<in>S. \<sigma> \<longlonglongrightarrow> l"
   6.377 +    proof
   6.378 +      show "g l \<in> S"
   6.379 +        using hom homeomorphism_image2 by blast
   6.380 +      have "(g \<circ> (f \<circ> \<sigma>)) \<longlonglongrightarrow> g l"
   6.381 +        by (meson UNIV_I \<open>(f \<circ> \<sigma>) \<longlonglongrightarrow> l\<close> continuous_on_sequentially hom homeomorphism_cont2)
   6.382 +      then show "\<sigma> \<longlonglongrightarrow> g l"
   6.383 +      proof -
   6.384 +        have "\<forall>n. \<sigma> n = (g \<circ> (f \<circ> \<sigma>)) n"
   6.385 +          by (metis (no_types) \<sigma> comp_eq_dest_lhs hom homeomorphism_apply1)
   6.386 +        then show ?thesis
   6.387 +          by (metis (no_types) LIMSEQ_iff \<open>(g \<circ> (f \<circ> \<sigma>)) \<longlonglongrightarrow> g l\<close>)
   6.388 +      qed
   6.389 +    qed
   6.390 +  qed
   6.391 +  then have "closed S"
   6.392 +    by (simp add: complete_eq_closed)
   6.393 +  ultimately show ?thesis
   6.394 +    using clopen [of S] False  by simp
   6.395 +qed
   6.396 +
   6.397 +subsection\<open>The power, squaring and exponential functions as covering maps\<close>
   6.398 +
   6.399 +proposition covering_space_power_punctured_plane:
   6.400 +  assumes "0 < n"
   6.401 +    shows "covering_space (- {0}) (\<lambda>z::complex. z^n) (- {0})"
   6.402 +proof -
   6.403 +  consider "n = 1" | "2 \<le> n" using assms by linarith
   6.404 +  then obtain e where "0 < e"
   6.405 +                and e: "\<And>w z. cmod(w - z) < e * cmod z \<Longrightarrow> (w^n = z^n \<longleftrightarrow> w = z)"
   6.406 +  proof cases
   6.407 +    assume "n = 1" then show ?thesis
   6.408 +      by (rule_tac e=1 in that) auto
   6.409 +  next
   6.410 +    assume "2 \<le> n"
   6.411 +    have eq_if_pow_eq:
   6.412 +         "w = z" if lt: "cmod (w - z) < 2 * sin (pi / real n) * cmod z"
   6.413 +                 and eq: "w^n = z^n" for w z
   6.414 +    proof (cases "z = 0")
   6.415 +      case True with eq assms show ?thesis by (auto simp: power_0_left)
   6.416 +    next
   6.417 +      case False
   6.418 +      then have "z \<noteq> 0" by auto
   6.419 +      have "(w/z)^n = 1"
   6.420 +        by (metis False divide_self_if eq power_divide power_one)
   6.421 +      then obtain j where j: "w / z = exp (2 * of_real pi * \<i> * j / n)" and "j < n"
   6.422 +        using Suc_leI assms \<open>2 \<le> n\<close> complex_roots_unity [THEN eqset_imp_iff, of n "w/z"]
   6.423 +        by force
   6.424 +      have "cmod (w/z - 1) < 2 * sin (pi / real n)"
   6.425 +        using lt assms \<open>z \<noteq> 0\<close> by (simp add: divide_simps norm_divide)
   6.426 +      then have "cmod (exp (\<i> * of_real (2 * pi * j / n)) - 1) < 2 * sin (pi / real n)"
   6.427 +        by (simp add: j field_simps)
   6.428 +      then have "2 * \<bar>sin((2 * pi * j / n) / 2)\<bar> < 2 * sin (pi / real n)"
   6.429 +        by (simp only: dist_exp_ii_1)
   6.430 +      then have sin_less: "sin((pi * j / n)) < sin (pi / real n)"
   6.431 +        by (simp add: field_simps)
   6.432 +      then have "w / z = 1"
   6.433 +      proof (cases "j = 0")
   6.434 +        case True then show ?thesis by (auto simp: j)
   6.435 +      next
   6.436 +        case False
   6.437 +        then have "sin (pi / real n) \<le> sin((pi * j / n))"
   6.438 +        proof (cases "j / n \<le> 1/2")
   6.439 +          case True
   6.440 +          show ?thesis
   6.441 +            apply (rule sin_monotone_2pi_le)
   6.442 +            using \<open>j \<noteq> 0 \<close> \<open>j < n\<close> True
   6.443 +            apply (auto simp: field_simps intro: order_trans [of _ 0])
   6.444 +            done
   6.445 +        next
   6.446 +          case False
   6.447 +          then have seq: "sin(pi * j / n) = sin(pi * (n - j) / n)"
   6.448 +            using \<open>j < n\<close> by (simp add: algebra_simps diff_divide_distrib of_nat_diff)
   6.449 +          show ?thesis
   6.450 +            apply (simp only: seq)
   6.451 +            apply (rule sin_monotone_2pi_le)
   6.452 +            using \<open>j < n\<close> False
   6.453 +            apply (auto simp: field_simps intro: order_trans [of _ 0])
   6.454 +            done
   6.455 +        qed
   6.456 +        with sin_less show ?thesis by force
   6.457 +      qed
   6.458 +      then show ?thesis by simp
   6.459 +    qed
   6.460 +    show ?thesis
   6.461 +      apply (rule_tac e = "2 * sin(pi / n)" in that)
   6.462 +       apply (force simp: \<open>2 \<le> n\<close> sin_pi_divide_n_gt_0)
   6.463 +      apply (meson eq_if_pow_eq)
   6.464 +      done
   6.465 +  qed
   6.466 +  have zn1: "continuous_on (- {0}) (\<lambda>z::complex. z^n)"
   6.467 +    by (rule continuous_intros)+
   6.468 +  have zn2: "(\<lambda>z::complex. z^n) ` (- {0}) = - {0}"
   6.469 +    using assms by (auto simp: image_def elim: exists_complex_root_nonzero [where n = n])
   6.470 +  have zn3: "\<exists>T. z^n \<in> T \<and> open T \<and> 0 \<notin> T \<and>
   6.471 +               (\<exists>v. \<Union>v = {x. x \<noteq> 0 \<and> x^n \<in> T} \<and>
   6.472 +                    (\<forall>u\<in>v. open u \<and> 0 \<notin> u) \<and>
   6.473 +                    pairwise disjnt v \<and>
   6.474 +                    (\<forall>u\<in>v. Ex (homeomorphism u T (\<lambda>z. z^n))))"
   6.475 +           if "z \<noteq> 0" for z::complex
   6.476 +  proof -
   6.477 +    def d \<equiv> "min (1/2) (e/4) * norm z"
   6.478 +    have "0 < d"
   6.479 +      by (simp add: d_def \<open>0 < e\<close> \<open>z \<noteq> 0\<close>)
   6.480 +    have iff_x_eq_y: "x^n = y^n \<longleftrightarrow> x = y"
   6.481 +         if eq: "w^n = z^n" and x: "x \<in> ball w d" and y: "y \<in> ball w d" for w x y
   6.482 +    proof -
   6.483 +      have [simp]: "norm z = norm w" using that
   6.484 +        by (simp add: assms power_eq_imp_eq_norm)
   6.485 +      show ?thesis
   6.486 +      proof (cases "w = 0")
   6.487 +        case True with \<open>z \<noteq> 0\<close> assms eq
   6.488 +        show ?thesis by (auto simp: power_0_left)
   6.489 +      next
   6.490 +        case False
   6.491 +        have "cmod (x - y) < 2*d"
   6.492 +          using x y
   6.493 +          by (simp add: dist_norm [symmetric]) (metis dist_commute mult_2 dist_triangle_less_add)
   6.494 +        also have "... \<le> 2 * e / 4 * norm w"
   6.495 +          using \<open>e > 0\<close> by (simp add: d_def min_mult_distrib_right)
   6.496 +        also have "... = e * (cmod w / 2)"
   6.497 +          by simp
   6.498 +        also have "... \<le> e * cmod y"
   6.499 +          apply (rule mult_left_mono)
   6.500 +          using \<open>e > 0\<close> y
   6.501 +           apply (simp_all add: dist_norm d_def min_mult_distrib_right del: divide_const_simps)
   6.502 +          apply (metis dist_0_norm dist_complex_def dist_triangle_half_l linorder_not_less order_less_irrefl)
   6.503 +          done
   6.504 +        finally have "cmod (x - y) < e * cmod y" .
   6.505 +        then show ?thesis by (rule e)
   6.506 +      qed
   6.507 +    qed
   6.508 +    then have inj: "inj_on (\<lambda>w. w^n) (ball z d)"
   6.509 +      by (simp add: inj_on_def)
   6.510 +    have cont: "continuous_on (ball z d) (\<lambda>w. w ^ n)"
   6.511 +      by (intro continuous_intros)
   6.512 +    have noncon: "\<not> (\<lambda>w::complex. w^n) constant_on UNIV"
   6.513 +      by (metis UNIV_I assms constant_on_def power_one zero_neq_one zero_power)
   6.514 +    have open_imball: "open ((\<lambda>w. w^n) ` ball z d)"
   6.515 +      by (rule invariance_of_domain [OF cont open_ball inj])
   6.516 +    have im_eq: "(\<lambda>w. w^n) ` ball z' d = (\<lambda>w. w^n) ` ball z d"
   6.517 +                if z': "z'^n = z^n" for z'
   6.518 +    proof -
   6.519 +      have nz': "norm z' = norm z" using that assms power_eq_imp_eq_norm by blast
   6.520 +      have "(w \<in> (\<lambda>w. w^n) ` ball z' d) = (w \<in> (\<lambda>w. w^n) ` ball z d)" for w
   6.521 +      proof (cases "w=0")
   6.522 +        case True with assms show ?thesis
   6.523 +          by (simp add: image_def ball_def nz')
   6.524 +      next
   6.525 +        case False
   6.526 +        have "z' \<noteq> 0" using \<open>z \<noteq> 0\<close> nz' by force
   6.527 +        have [simp]: "(z*x / z')^n = x^n" if "x \<noteq> 0" for x
   6.528 +          using z' that by (simp add: field_simps \<open>z \<noteq> 0\<close>)
   6.529 +        have [simp]: "cmod (z - z * x / z') = cmod (z' - x)" if "x \<noteq> 0" for x
   6.530 +        proof -
   6.531 +          have "cmod (z - z * x / z') = cmod z * cmod (1 - x / z')"
   6.532 +            by (metis (no_types) ab_semigroup_mult_class.mult_ac(1) complex_divide_def mult.right_neutral norm_mult right_diff_distrib')
   6.533 +          also have "... = cmod z' * cmod (1 - x / z')"
   6.534 +            by (simp add: nz')
   6.535 +          also have "... = cmod (z' - x)"
   6.536 +            by (simp add: \<open>z' \<noteq> 0\<close> diff_divide_eq_iff norm_divide)
   6.537 +          finally show ?thesis .
   6.538 +        qed
   6.539 +        have [simp]: "(z'*x / z)^n = x^n" if "x \<noteq> 0" for x
   6.540 +          using z' that by (simp add: field_simps \<open>z \<noteq> 0\<close>)
   6.541 +        have [simp]: "cmod (z' - z' * x / z) = cmod (z - x)" if "x \<noteq> 0" for x
   6.542 +        proof -
   6.543 +          have "cmod (z * (1 - x * inverse z)) = cmod (z - x)"
   6.544 +            by (metis \<open>z \<noteq> 0\<close> diff_divide_distrib divide_complex_def divide_self_if nonzero_eq_divide_eq semiring_normalization_rules(7))
   6.545 +          then show ?thesis
   6.546 +            by (metis (no_types) mult.assoc complex_divide_def mult.right_neutral norm_mult nz' right_diff_distrib')
   6.547 +        qed
   6.548 +        show ?thesis
   6.549 +          unfolding image_def ball_def
   6.550 +          apply safe
   6.551 +          apply simp_all
   6.552 +          apply (rule_tac x="z/z' * x" in exI)
   6.553 +          using assms False apply (simp add: dist_norm)
   6.554 +          apply (rule_tac x="z'/z * x" in exI)
   6.555 +          using assms False apply (simp add: dist_norm)
   6.556 +          done
   6.557 +      qed
   6.558 +      then show ?thesis by blast
   6.559 +    qed
   6.560 +    have ex_ball: "\<exists>B. (\<exists>z'. B = ball z' d \<and> z'^n = z^n) \<and> x \<in> B"
   6.561 +                  if "x \<noteq> 0" and eq: "x^n = w^n" and dzw: "dist z w < d" for x w
   6.562 +    proof -
   6.563 +      have "w \<noteq> 0" by (metis assms power_eq_0_iff that(1) that(2))
   6.564 +      have [simp]: "cmod x = cmod w"
   6.565 +        using assms power_eq_imp_eq_norm eq by blast
   6.566 +      have [simp]: "cmod (x * z / w - x) = cmod (z - w)"
   6.567 +      proof -
   6.568 +        have "cmod (x * z / w - x) = cmod x * cmod (z / w - 1)"
   6.569 +          by (metis (no_types) mult.right_neutral norm_mult right_diff_distrib' times_divide_eq_right)
   6.570 +        also have "... = cmod w * cmod (z / w - 1)"
   6.571 +          by simp
   6.572 +        also have "... = cmod (z - w)"
   6.573 +          by (simp add: \<open>w \<noteq> 0\<close> divide_diff_eq_iff nonzero_norm_divide)
   6.574 +        finally show ?thesis .
   6.575 +      qed
   6.576 +      show ?thesis
   6.577 +        apply (rule_tac x="ball (z / w * x) d" in exI)
   6.578 +        using \<open>d > 0\<close> that
   6.579 +        apply (simp add: ball_eq_ball_iff)
   6.580 +        apply (simp add: \<open>z \<noteq> 0\<close> \<open>w \<noteq> 0\<close> field_simps)
   6.581 +        apply (simp add: dist_norm)
   6.582 +        done
   6.583 +    qed
   6.584 +    have ball1: "\<Union>{ball z' d |z'. z'^n = z^n} = {x. x \<noteq> 0 \<and> x^n \<in> (\<lambda>w. w^n) ` ball z d}"
   6.585 +      apply (rule equalityI)
   6.586 +       prefer 2 apply (force simp: ex_ball, clarsimp)
   6.587 +      apply (subst im_eq [symmetric], assumption)
   6.588 +      using assms
   6.589 +      apply (force simp: dist_norm d_def min_mult_distrib_right dest: power_eq_imp_eq_norm)
   6.590 +      done
   6.591 +    have ball2: "pairwise disjnt {ball z' d |z'. z'^n = z^n}"
   6.592 +    proof (clarsimp simp add: pairwise_def disjnt_iff)
   6.593 +      fix \<xi> \<zeta> x
   6.594 +      assume "\<xi>^n = z^n" "\<zeta>^n = z^n" "ball \<xi> d \<noteq> ball \<zeta> d"
   6.595 +         and "dist \<xi> x < d" "dist \<zeta> x < d"
   6.596 +      then have "dist \<xi> \<zeta> < d+d"
   6.597 +        using dist_triangle_less_add by blast
   6.598 +      then have "cmod (\<xi> - \<zeta>) < 2*d"
   6.599 +        by (simp add: dist_norm)
   6.600 +      also have "... \<le> e * cmod z"
   6.601 +        using mult_right_mono \<open>0 < e\<close> that by (auto simp: d_def)
   6.602 +      finally have "cmod (\<xi> - \<zeta>) < e * cmod z" .
   6.603 +      with e have "\<xi> = \<zeta>"
   6.604 +        by (metis \<open>\<xi>^n = z^n\<close> \<open>\<zeta>^n = z^n\<close> assms power_eq_imp_eq_norm)
   6.605 +      then show "False"
   6.606 +        using \<open>ball \<xi> d \<noteq> ball \<zeta> d\<close> by blast
   6.607 +    qed
   6.608 +    have ball3: "Ex (homeomorphism (ball z' d) ((\<lambda>w. w^n) ` ball z d) (\<lambda>z. z^n))"
   6.609 +            if zeq: "z'^n = z^n" for z'
   6.610 +    proof -
   6.611 +      have inj: "inj_on (\<lambda>z. z ^ n) (ball z' d)"
   6.612 +        by (meson iff_x_eq_y inj_onI zeq)
   6.613 +      show ?thesis
   6.614 +        apply (rule invariance_of_domain_homeomorphism [of "ball z' d" "\<lambda>z. z^n"])
   6.615 +          apply (rule open_ball continuous_intros order_refl inj)+
   6.616 +        apply (force simp: im_eq [OF zeq])
   6.617 +        done
   6.618 +    qed
   6.619 +    show ?thesis
   6.620 +      apply (rule_tac x = "(\<lambda>w. w^n) ` (ball z d)" in exI)
   6.621 +      apply (intro conjI open_imball)
   6.622 +        using \<open>d > 0\<close> apply simp
   6.623 +       using \<open>z \<noteq> 0\<close> assms apply (force simp: d_def)
   6.624 +      apply (rule_tac x="{ ball z' d |z'. z'^n = z^n}" in exI)
   6.625 +      apply (intro conjI ball1 ball2)
   6.626 +       apply (force simp: assms d_def power_eq_imp_eq_norm that, clarify)
   6.627 +      by (metis ball3)
   6.628 +  qed
   6.629 +  show ?thesis
   6.630 +    using assms
   6.631 +    apply (simp add: covering_space_def zn1 zn2)
   6.632 +    apply (subst zn2 [symmetric])
   6.633 +    apply (simp add: openin_open_eq open_Compl)
   6.634 +    apply (blast intro: zn3)
   6.635 +    done
   6.636 +qed
   6.637 +
   6.638 +corollary covering_space_square_punctured_plane:
   6.639 +  "covering_space (- {0}) (\<lambda>z::complex. z^2) (- {0})"
   6.640 +  by (simp add: covering_space_power_punctured_plane)
   6.641 +
   6.642 +
   6.643 +
   6.644 +proposition covering_space_exp_punctured_plane:
   6.645 +  "covering_space UNIV (\<lambda>z::complex. exp z) (- {0})"
   6.646 +proof (simp add: covering_space_def, intro conjI ballI)
   6.647 +  show "continuous_on UNIV (\<lambda>z::complex. exp z)"
   6.648 +    by (rule continuous_on_exp [OF continuous_on_id])
   6.649 +  show "range exp = - {0::complex}"
   6.650 +    by auto (metis exp_Ln range_eqI)
   6.651 +  show "\<exists>T. z \<in> T \<and> openin (subtopology euclidean (- {0})) T \<and>
   6.652 +             (\<exists>v. \<Union>v = {z. exp z \<in> T} \<and> (\<forall>u\<in>v. open u) \<and> disjoint v \<and>
   6.653 +                  (\<forall>u\<in>v. \<exists>q. homeomorphism u T exp q))"
   6.654 +        if "z \<in> - {0::complex}" for z
   6.655 +  proof -
   6.656 +    have "z \<noteq> 0"
   6.657 +      using that by auto
   6.658 +    have inj_exp: "inj_on exp (ball (Ln z) 1)"
   6.659 +      apply (rule inj_on_subset [OF inj_on_exp_pi [of "Ln z"]])
   6.660 +      using pi_ge_two by (simp add: ball_subset_ball_iff)
   6.661 +    define \<V> where "\<V> \<equiv> range (\<lambda>n. (\<lambda>x. x + of_real (2 * of_int n * pi) * ii) ` (ball(Ln z) 1))"
   6.662 +    show ?thesis
   6.663 +    proof (intro exI conjI)
   6.664 +      show "z \<in> exp ` (ball(Ln z) 1)"
   6.665 +        by (metis \<open>z \<noteq> 0\<close> centre_in_ball exp_Ln rev_image_eqI zero_less_one)
   6.666 +      have "open (- {0::complex})"
   6.667 +        by blast
   6.668 +      moreover have "inj_on exp (ball (Ln z) 1)"
   6.669 +        apply (rule inj_on_subset [OF inj_on_exp_pi [of "Ln z"]])
   6.670 +        using pi_ge_two by (simp add: ball_subset_ball_iff)
   6.671 +      ultimately show "openin (subtopology euclidean (- {0})) (exp ` ball (Ln z) 1)"
   6.672 +        by (auto simp: openin_open_eq invariance_of_domain continuous_on_exp [OF continuous_on_id])
   6.673 +      show "\<Union>\<V> = {w. exp w \<in> exp ` ball (Ln z) 1}"
   6.674 +        by (auto simp: \<V>_def Complex_Transcendental.exp_eq image_iff)
   6.675 +      show "\<forall>V\<in>\<V>. open V"
   6.676 +        by (auto simp: \<V>_def inj_on_def continuous_intros invariance_of_domain)
   6.677 +      have xy: "2 \<le> cmod (2 * of_int x * of_real pi * \<i> - 2 * of_int y * of_real pi * \<i>)"
   6.678 +               if "x < y" for x y
   6.679 +      proof -
   6.680 +        have "1 \<le> abs (x - y)"
   6.681 +          using that by linarith
   6.682 +        then have "1 \<le> cmod (of_int x - of_int y) * 1"
   6.683 +          by (metis mult.right_neutral norm_of_int of_int_1_le_iff of_int_abs of_int_diff)
   6.684 +        also have "... \<le> cmod (of_int x - of_int y) * of_real pi"
   6.685 +          apply (rule mult_left_mono)
   6.686 +          using pi_ge_two by auto
   6.687 +        also have "... \<le> cmod ((of_int x - of_int y) * of_real pi * \<i>)"
   6.688 +          by (simp add: norm_mult)
   6.689 +        also have "... \<le> cmod (of_int x * of_real pi * \<i> - of_int y * of_real pi * \<i>)"
   6.690 +          by (simp add: algebra_simps)
   6.691 +        finally have "1 \<le> cmod (of_int x * of_real pi * \<i> - of_int y * of_real pi * \<i>)" .
   6.692 +        then have "2 * 1 \<le> cmod (2 * (of_int x * of_real pi * \<i> - of_int y * of_real pi * \<i>))"
   6.693 +          by (metis mult_le_cancel_left_pos norm_mult_numeral1 zero_less_numeral)
   6.694 +        then show ?thesis
   6.695 +          by (simp add: algebra_simps)
   6.696 +      qed
   6.697 +      show "disjoint \<V>"
   6.698 +        apply (clarsimp simp add: \<V>_def pairwise_def disjnt_def add.commute [of _ "x*y" for x y]
   6.699 +                        image_add_ball ball_eq_ball_iff)
   6.700 +        apply (rule disjoint_ballI)
   6.701 +        apply (auto simp: dist_norm neq_iff)
   6.702 +        by (metis norm_minus_commute xy)+
   6.703 +      show "\<forall>u\<in>\<V>. \<exists>q. homeomorphism u (exp ` ball (Ln z) 1) exp q"
   6.704 +      proof
   6.705 +        fix u
   6.706 +        assume "u \<in> \<V>"
   6.707 +        then obtain n where n: "u = (\<lambda>x. x + of_real (2 * of_int n * pi) * ii) ` (ball(Ln z) 1)"
   6.708 +          by (auto simp: \<V>_def)
   6.709 +        have "compact (cball (Ln z) 1)"
   6.710 +          by simp
   6.711 +        moreover have "continuous_on (cball (Ln z) 1) exp"
   6.712 +          by (rule continuous_on_exp [OF continuous_on_id])
   6.713 +        moreover have "inj_on exp (cball (Ln z) 1)"
   6.714 +          apply (rule inj_on_subset [OF inj_on_exp_pi [of "Ln z"]])
   6.715 +          using pi_ge_two by (simp add: cball_subset_ball_iff)
   6.716 +        ultimately obtain \<gamma> where hom: "homeomorphism (cball (Ln z) 1) (exp ` cball (Ln z) 1) exp \<gamma>"
   6.717 +          using homeomorphism_compact  by blast
   6.718 +        have eq1: "exp ` u = exp ` ball (Ln z) 1"
   6.719 +          unfolding n
   6.720 +          apply (auto simp: algebra_simps)
   6.721 +          apply (rename_tac w)
   6.722 +          apply (rule_tac x = "w + \<i> * (of_int n * (of_real pi * 2))" in image_eqI)
   6.723 +          apply (auto simp: image_iff)
   6.724 +          done
   6.725 +        have \<gamma>exp: "\<gamma> (exp x) + 2 * of_int n * of_real pi * \<i> = x" if "x \<in> u" for x
   6.726 +        proof -
   6.727 +          have "exp x = exp (x - 2 * of_int n * of_real pi * \<i>)"
   6.728 +            by (simp add: exp_eq)
   6.729 +          then have "\<gamma> (exp x) = \<gamma> (exp (x - 2 * of_int n * of_real pi * \<i>))"
   6.730 +            by simp
   6.731 +          also have "... = x - 2 * of_int n * of_real pi * \<i>"
   6.732 +            apply (rule homeomorphism_apply1 [OF hom])
   6.733 +            using \<open>x \<in> u\<close> by (auto simp: n)
   6.734 +          finally show ?thesis
   6.735 +            by simp
   6.736 +        qed
   6.737 +        have exp2n: "exp (\<gamma> (exp x) + 2 * of_int n * complex_of_real pi * \<i>) = exp x"
   6.738 +                if "dist (Ln z) x < 1" for x
   6.739 +          using that by (auto simp: exp_eq homeomorphism_apply1 [OF hom])
   6.740 +        have cont: "continuous_on (exp ` ball (Ln z) 1) (\<lambda>x. \<gamma> x + 2 * of_int n * complex_of_real pi * \<i>)"
   6.741 +          apply (intro continuous_intros)
   6.742 +          apply (rule continuous_on_subset [OF homeomorphism_cont2 [OF hom]])
   6.743 +          apply (force simp:)
   6.744 +          done
   6.745 +        show "\<exists>q. homeomorphism u (exp ` ball (Ln z) 1) exp q"
   6.746 +          apply (rule_tac x="(\<lambda>x. x + of_real(2 * n * pi) * ii) \<circ> \<gamma>" in exI)
   6.747 +          unfolding homeomorphism_def
   6.748 +          apply (intro conjI ballI eq1 continuous_on_exp [OF continuous_on_id])
   6.749 +             apply (auto simp: \<gamma>exp exp2n cont n)
   6.750 +           apply (simp add:  homeomorphism_apply1 [OF hom])
   6.751 +          apply (simp add: image_comp [symmetric])
   6.752 +          using hom homeomorphism_apply1  apply (force simp: image_iff)
   6.753 +          done
   6.754 +      qed
   6.755 +    qed
   6.756 +  qed
   6.757 +qed
   6.758 +
   6.759  end
     7.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Oct 18 12:01:54 2016 +0200
     7.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Oct 18 15:55:53 2016 +0100
     7.3 @@ -960,7 +960,7 @@
     7.4          using dp p(1) mn d(2) by auto
     7.5      qed
     7.6    qed
     7.7 -  then guess y unfolding convergent_eq_cauchy[symmetric] .. note y=this[THEN LIMSEQ_D]
     7.8 +  then guess y unfolding convergent_eq_Cauchy[symmetric] .. note y=this[THEN LIMSEQ_D]
     7.9    show ?l
    7.10      unfolding integrable_on_def has_integral
    7.11    proof (rule_tac x=y in exI, clarify)
    7.12 @@ -1798,7 +1798,7 @@
    7.13      qed
    7.14    qed
    7.15    then obtain s where s: "i \<longlonglongrightarrow> s"
    7.16 -    using convergent_eq_cauchy[symmetric] by blast
    7.17 +    using convergent_eq_Cauchy[symmetric] by blast
    7.18    show ?thesis
    7.19      unfolding integrable_on_def has_integral
    7.20    proof (rule_tac x=s in exI, clarify)
    7.21 @@ -5437,7 +5437,7 @@
    7.22        apply auto
    7.23        done
    7.24    qed
    7.25 -  from this[unfolded convergent_eq_cauchy[symmetric]] guess i ..
    7.26 +  from this[unfolded convergent_eq_Cauchy[symmetric]] guess i ..
    7.27    note i = this[THEN LIMSEQ_D]
    7.28  
    7.29    show ?l unfolding integrable_on_def has_integral_alt'[of f]
     8.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Oct 18 12:01:54 2016 +0200
     8.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Oct 18 15:55:53 2016 +0100
     8.3 @@ -1034,6 +1034,14 @@
     8.4    shows "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e"
     8.5    by (simp add: dist_norm)
     8.6  
     8.7 +lemma disjoint_ballI:
     8.8 +  shows "dist x y \<ge> r+s \<Longrightarrow> ball x r \<inter> ball y s = {}"
     8.9 +  using dist_triangle_less_add not_le by fastforce
    8.10 +
    8.11 +lemma disjoint_cballI:
    8.12 +  shows "dist x y > r+s \<Longrightarrow> cball x r \<inter> cball y s = {}"
    8.13 +  by (metis add_mono disjoint_iff_not_equal dist_triangle2 dual_order.trans leD mem_cball)
    8.14 +
    8.15  lemma mem_sphere_0 [simp]:
    8.16    fixes x :: "'a::real_normed_vector"
    8.17    shows "x \<in> sphere 0 e \<longleftrightarrow> norm x = e"
    8.18 @@ -5435,62 +5443,62 @@
    8.19  qed
    8.20  
    8.21  lemma complete_imp_closed:
    8.22 -  fixes s :: "'a::metric_space set"
    8.23 -  assumes "complete s"
    8.24 -  shows "closed s"
    8.25 +  fixes S :: "'a::metric_space set"
    8.26 +  assumes "complete S"
    8.27 +  shows "closed S"
    8.28  proof (unfold closed_sequential_limits, clarify)
    8.29 -  fix f x assume "\<forall>n. f n \<in> s" and "f \<longlonglongrightarrow> x"
    8.30 +  fix f x assume "\<forall>n. f n \<in> S" and "f \<longlonglongrightarrow> x"
    8.31    from \<open>f \<longlonglongrightarrow> x\<close> have "Cauchy f"
    8.32      by (rule LIMSEQ_imp_Cauchy)
    8.33 -  with \<open>complete s\<close> and \<open>\<forall>n. f n \<in> s\<close> obtain l where "l \<in> s" and "f \<longlonglongrightarrow> l"
    8.34 +  with \<open>complete S\<close> and \<open>\<forall>n. f n \<in> S\<close> obtain l where "l \<in> S" and "f \<longlonglongrightarrow> l"
    8.35      by (rule completeE)
    8.36    from \<open>f \<longlonglongrightarrow> x\<close> and \<open>f \<longlonglongrightarrow> l\<close> have "x = l"
    8.37      by (rule LIMSEQ_unique)
    8.38 -  with \<open>l \<in> s\<close> show "x \<in> s"
    8.39 +  with \<open>l \<in> S\<close> show "x \<in> S"
    8.40      by simp
    8.41  qed
    8.42  
    8.43  lemma complete_Int_closed:
    8.44 -  fixes s :: "'a::metric_space set"
    8.45 -  assumes "complete s" and "closed t"
    8.46 -  shows "complete (s \<inter> t)"
    8.47 +  fixes S :: "'a::metric_space set"
    8.48 +  assumes "complete S" and "closed t"
    8.49 +  shows "complete (S \<inter> t)"
    8.50  proof (rule completeI)
    8.51 -  fix f assume "\<forall>n. f n \<in> s \<inter> t" and "Cauchy f"
    8.52 -  then have "\<forall>n. f n \<in> s" and "\<forall>n. f n \<in> t"
    8.53 +  fix f assume "\<forall>n. f n \<in> S \<inter> t" and "Cauchy f"
    8.54 +  then have "\<forall>n. f n \<in> S" and "\<forall>n. f n \<in> t"
    8.55      by simp_all
    8.56 -  from \<open>complete s\<close> obtain l where "l \<in> s" and "f \<longlonglongrightarrow> l"
    8.57 -    using \<open>\<forall>n. f n \<in> s\<close> and \<open>Cauchy f\<close> by (rule completeE)
    8.58 +  from \<open>complete S\<close> obtain l where "l \<in> S" and "f \<longlonglongrightarrow> l"
    8.59 +    using \<open>\<forall>n. f n \<in> S\<close> and \<open>Cauchy f\<close> by (rule completeE)
    8.60    from \<open>closed t\<close> and \<open>\<forall>n. f n \<in> t\<close> and \<open>f \<longlonglongrightarrow> l\<close> have "l \<in> t"
    8.61      by (rule closed_sequentially)
    8.62 -  with \<open>l \<in> s\<close> and \<open>f \<longlonglongrightarrow> l\<close> show "\<exists>l\<in>s \<inter> t. f \<longlonglongrightarrow> l"
    8.63 +  with \<open>l \<in> S\<close> and \<open>f \<longlonglongrightarrow> l\<close> show "\<exists>l\<in>S \<inter> t. f \<longlonglongrightarrow> l"
    8.64      by fast
    8.65  qed
    8.66  
    8.67  lemma complete_closed_subset:
    8.68 -  fixes s :: "'a::metric_space set"
    8.69 -  assumes "closed s" and "s \<subseteq> t" and "complete t"
    8.70 -  shows "complete s"
    8.71 -  using assms complete_Int_closed [of t s] by (simp add: Int_absorb1)
    8.72 +  fixes S :: "'a::metric_space set"
    8.73 +  assumes "closed S" and "S \<subseteq> t" and "complete t"
    8.74 +  shows "complete S"
    8.75 +  using assms complete_Int_closed [of t S] by (simp add: Int_absorb1)
    8.76  
    8.77  lemma complete_eq_closed:
    8.78 -  fixes s :: "('a::complete_space) set"
    8.79 -  shows "complete s \<longleftrightarrow> closed s"
    8.80 +  fixes S :: "('a::complete_space) set"
    8.81 +  shows "complete S \<longleftrightarrow> closed S"
    8.82  proof
    8.83 -  assume "closed s" then show "complete s"
    8.84 +  assume "closed S" then show "complete S"
    8.85      using subset_UNIV complete_UNIV by (rule complete_closed_subset)
    8.86  next
    8.87 -  assume "complete s" then show "closed s"
    8.88 +  assume "complete S" then show "closed S"
    8.89      by (rule complete_imp_closed)
    8.90  qed
    8.91  
    8.92 -lemma convergent_eq_cauchy:
    8.93 -  fixes s :: "nat \<Rightarrow> 'a::complete_space"
    8.94 -  shows "(\<exists>l. (s \<longlongrightarrow> l) sequentially) \<longleftrightarrow> Cauchy s"
    8.95 +lemma convergent_eq_Cauchy:
    8.96 +  fixes S :: "nat \<Rightarrow> 'a::complete_space"
    8.97 +  shows "(\<exists>l. (S \<longlongrightarrow> l) sequentially) \<longleftrightarrow> Cauchy S"
    8.98    unfolding Cauchy_convergent_iff convergent_def ..
    8.99  
   8.100  lemma convergent_imp_bounded:
   8.101 -  fixes s :: "nat \<Rightarrow> 'a::metric_space"
   8.102 -  shows "(s \<longlongrightarrow> l) sequentially \<Longrightarrow> bounded (range s)"
   8.103 +  fixes S :: "nat \<Rightarrow> 'a::metric_space"
   8.104 +  shows "(S \<longlongrightarrow> l) sequentially \<Longrightarrow> bounded (range S)"
   8.105    by (intro cauchy_imp_bounded LIMSEQ_imp_Cauchy)
   8.106  
   8.107  lemma compact_cball[simp]:
   8.108 @@ -5500,15 +5508,15 @@
   8.109    by blast
   8.110  
   8.111  lemma compact_frontier_bounded[intro]:
   8.112 -  fixes s :: "'a::heine_borel set"
   8.113 -  shows "bounded s \<Longrightarrow> compact (frontier s)"
   8.114 +  fixes S :: "'a::heine_borel set"
   8.115 +  shows "bounded S \<Longrightarrow> compact (frontier S)"
   8.116    unfolding frontier_def
   8.117    using compact_eq_bounded_closed
   8.118    by blast
   8.119  
   8.120  lemma compact_frontier[intro]:
   8.121 -  fixes s :: "'a::heine_borel set"
   8.122 -  shows "compact s \<Longrightarrow> compact (frontier s)"
   8.123 +  fixes S :: "'a::heine_borel set"
   8.124 +  shows "compact S \<Longrightarrow> compact (frontier S)"
   8.125    using compact_eq_bounded_closed compact_frontier_bounded
   8.126    by blast
   8.127  
   8.128 @@ -5528,8 +5536,8 @@
   8.129  by (simp add: compact_imp_closed)
   8.130  
   8.131  lemma frontier_subset_compact:
   8.132 -  fixes s :: "'a::heine_borel set"
   8.133 -  shows "compact s \<Longrightarrow> frontier s \<subseteq> s"
   8.134 +  fixes S :: "'a::heine_borel set"
   8.135 +  shows "compact S \<Longrightarrow> frontier S \<subseteq> S"
   8.136    using frontier_subset_closed compact_eq_bounded_closed
   8.137    by blast
   8.138  
   8.139 @@ -5723,7 +5731,7 @@
   8.140      apply auto
   8.141      done
   8.142    then obtain l where l: "\<forall>x. P x \<longrightarrow> ((\<lambda>n. s n x) \<longlongrightarrow> l x) sequentially"
   8.143 -    unfolding convergent_eq_cauchy[symmetric]
   8.144 +    unfolding convergent_eq_Cauchy[symmetric]
   8.145      using choice[of "\<lambda>x l. P x \<longrightarrow> ((\<lambda>n. s n x) \<longlongrightarrow> l) sequentially"]
   8.146      by auto
   8.147    {
   8.148 @@ -6081,6 +6089,11 @@
   8.149      unfolding uniformly_continuous_on_def by blast
   8.150  qed
   8.151  
   8.152 +lemma continuous_closed_imp_Cauchy_continuous:
   8.153 +  fixes S :: "('a::complete_space) set"
   8.154 +  shows "\<lbrakk>continuous_on S f; closed S; Cauchy \<sigma>; \<And>n. (\<sigma> n) \<in> S\<rbrakk> \<Longrightarrow> Cauchy(f o \<sigma>)"
   8.155 +  apply (simp add: complete_eq_closed [symmetric] continuous_on_sequentially)
   8.156 +  by (meson LIMSEQ_imp_Cauchy complete_def)
   8.157  
   8.158  text\<open>The usual transformation theorems.\<close>
   8.159  
   8.160 @@ -6630,7 +6643,7 @@
   8.161  
   8.162    from uniformly_continuous_on_Cauchy[OF uc LIMSEQ_imp_Cauchy, OF xs]
   8.163    obtain l where l: "(\<lambda>n. f (xs n)) \<longlonglongrightarrow> l"
   8.164 -    by atomize_elim (simp only: convergent_eq_cauchy)
   8.165 +    by atomize_elim (simp only: convergent_eq_Cauchy)
   8.166  
   8.167    have "(f \<longlongrightarrow> l) (at x within X)"
   8.168    proof (safe intro!: Lim_within_LIMSEQ)
   8.169 @@ -6641,7 +6654,7 @@
   8.170  
   8.171      from uniformly_continuous_on_Cauchy[OF uc LIMSEQ_imp_Cauchy, OF \<open>xs' \<longlonglongrightarrow> x\<close> \<open>xs' _ \<in> X\<close>]
   8.172      obtain l' where l': "(\<lambda>n. f (xs' n)) \<longlonglongrightarrow> l'"
   8.173 -      by atomize_elim (simp only: convergent_eq_cauchy)
   8.174 +      by atomize_elim (simp only: convergent_eq_Cauchy)
   8.175  
   8.176      show "(\<lambda>n. f (xs' n)) \<longlonglongrightarrow> l"
   8.177      proof (rule tendstoI)
     9.1 --- a/src/HOL/Limits.thy	Tue Oct 18 12:01:54 2016 +0200
     9.2 +++ b/src/HOL/Limits.thy	Tue Oct 18 15:55:53 2016 +0100
     9.3 @@ -2340,6 +2340,11 @@
     9.4  
     9.5  lemma isUCont_Cauchy: "isUCont f \<Longrightarrow> Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
     9.6    by (rule uniformly_continuous_on_Cauchy[where S=UNIV and f=f]) simp_all
     9.7 +  
     9.8 +lemma uniformly_continuous_imp_Cauchy_continuous:
     9.9 +  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
    9.10 +  shows "\<lbrakk>uniformly_continuous_on S f; Cauchy \<sigma>; \<And>n. (\<sigma> n) \<in> S\<rbrakk> \<Longrightarrow> Cauchy(f o \<sigma>)"
    9.11 +  by (simp add: uniformly_continuous_on_def Cauchy_def) meson
    9.12  
    9.13  lemma (in bounded_linear) isUCont: "isUCont f"
    9.14    unfolding isUCont_def dist_norm
    10.1 --- a/src/HOL/Orderings.thy	Tue Oct 18 12:01:54 2016 +0200
    10.2 +++ b/src/HOL/Orderings.thy	Tue Oct 18 15:55:53 2016 +0100
    10.3 @@ -1437,6 +1437,17 @@
    10.4  apply (erule Least_le)
    10.5  done
    10.6  
    10.7 +lemma exists_least_iff: "(\<exists>n. P n) \<longleftrightarrow> (\<exists>n. P n \<and> (\<forall>m < n. \<not> P m))" (is "?lhs \<longleftrightarrow> ?rhs")
    10.8 +proof
    10.9 +  assume ?rhs thus ?lhs by blast
   10.10 +next
   10.11 +  assume H: ?lhs then obtain n where n: "P n" by blast
   10.12 +  let ?x = "Least P"
   10.13 +  { fix m assume m: "m < ?x"
   10.14 +    from not_less_Least[OF m] have "\<not> P m" . }
   10.15 +  with LeastI_ex[OF H] show ?rhs by blast
   10.16 +qed
   10.17 +
   10.18  end
   10.19  
   10.20