# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1476802553 -3600
# Node ID d85d887227457b048c4211df41c9aa73ee2698c9
# Parent  f3b905b2eee23cf28da3892204f444f378b071a7
more from moretop.ml

diff -r f3b905b2eee2 -r d85d88722745 src/HOL/Analysis/Bochner_Integration.thy
--- a/src/HOL/Analysis/Bochner_Integration.thy	Tue Oct 18 12:01:54 2016 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy	Tue Oct 18 15:55:53 2016 +0100
@@ -1157,7 +1157,7 @@
   let ?s = "\<lambda>n. simple_bochner_integral M (s n)"
 
   have "\<exists>x. ?s \<longlonglongrightarrow> x"
-    unfolding convergent_eq_cauchy
+    unfolding convergent_eq_Cauchy
   proof (rule metric_CauchyI)
     fix e :: real assume "0 < e"
     then have "0 < ennreal (e / 2)" by auto
diff -r f3b905b2eee2 -r d85d88722745 src/HOL/Analysis/Borel_Space.thy
--- a/src/HOL/Analysis/Borel_Space.thy	Tue Oct 18 12:01:54 2016 +0200
+++ b/src/HOL/Analysis/Borel_Space.thy	Tue Oct 18 15:55:53 2016 +0100
@@ -1797,13 +1797,13 @@
 proof -
   define u' where "u' x = lim (\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0)" for x
   then have *: "\<And>x. lim (\<lambda>i. f i x) = (if Cauchy (\<lambda>i. f i x) then u' x else (THE x. False))"
-    by (auto simp: lim_def convergent_eq_cauchy[symmetric])
+    by (auto simp: lim_def convergent_eq_Cauchy[symmetric])
   have "u' \<in> borel_measurable M"
   proof (rule borel_measurable_LIMSEQ_metric)
     fix x
     have "convergent (\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0)"
       by (cases "Cauchy (\<lambda>i. f i x)")
-         (auto simp add: convergent_eq_cauchy[symmetric] convergent_def)
+         (auto simp add: convergent_eq_Cauchy[symmetric] convergent_def)
     then show "(\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0) \<longlonglongrightarrow> u' x"
       unfolding u'_def
       by (rule convergent_LIMSEQ_iff[THEN iffD1])
diff -r f3b905b2eee2 -r d85d88722745 src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Oct 18 12:01:54 2016 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Oct 18 15:55:53 2016 +0100
@@ -236,6 +236,23 @@
   finally show ?thesis .
 qed
 
+lemma exp_plus_2pin [simp]: "exp (z + \<i> * (of_int n * (of_real pi * 2))) = exp z"
+  by (simp add: exp_eq)
+
+lemma inj_on_exp_pi:
+  fixes z::complex shows "inj_on exp (ball z pi)"
+proof (clarsimp simp: inj_on_def exp_eq)
+  fix y n
+  assume "dist z (y + 2 * of_int n * of_real pi * \<i>) < pi"
+         "dist z y < pi"
+  then have "dist y (y + 2 * of_int n * of_real pi * \<i>) < pi+pi"
+    using dist_commute_lessI dist_triangle_less_add by blast
+  then have "norm (2 * of_int n * of_real pi * \<i>) < 2*pi"
+    by (simp add: dist_norm)
+  then show "n = 0"
+    by (auto simp: norm_mult)
+qed
+
 lemma sin_cos_eq_iff: "sin y = sin x \<and> cos y = cos x \<longleftrightarrow> (\<exists>n::int. y = x + 2 * n * pi)"
 proof -
   { assume "sin y = sin x" "cos y = cos x"
diff -r f3b905b2eee2 -r d85d88722745 src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Oct 18 12:01:54 2016 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Oct 18 15:55:53 2016 +0100
@@ -4378,6 +4378,15 @@
 definition "rel_interior S =
   {x. \<exists>T. openin (subtopology euclidean (affine hull S)) T \<and> x \<in> T \<and> T \<subseteq> S}"
 
+lemma rel_interior_mono:
+   "\<lbrakk>S \<subseteq> T; affine hull S = affine hull T\<rbrakk>
+   \<Longrightarrow> (rel_interior S) \<subseteq> (rel_interior T)"
+  by (auto simp: rel_interior_def)
+
+lemma rel_interior_maximal:
+   "\<lbrakk>T \<subseteq> S; openin(subtopology euclidean (affine hull S)) T\<rbrakk> \<Longrightarrow> T \<subseteq> (rel_interior S)"
+  by (auto simp: rel_interior_def)
+
 lemma rel_interior:
   "rel_interior S = {x \<in> S. \<exists>T. open T \<and> x \<in> T \<and> T \<inter> affine hull S \<subseteq> S}"
   unfolding rel_interior_def[of S] openin_open[of "affine hull S"]
diff -r f3b905b2eee2 -r d85d88722745 src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Tue Oct 18 12:01:54 2016 +0200
+++ b/src/HOL/Analysis/Derivative.thy	Tue Oct 18 15:55:53 2016 +0100
@@ -1922,7 +1922,7 @@
     using assms(1,2,3) by (rule has_derivative_sequence_lipschitz)
   have "\<exists>g. \<forall>x\<in>s. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially"
     apply (rule bchoice)
-    unfolding convergent_eq_cauchy
+    unfolding convergent_eq_Cauchy
   proof
     fix x
     assume "x \<in> s"
diff -r f3b905b2eee2 -r d85d88722745 src/HOL/Analysis/FurtherTopology.thy
--- a/src/HOL/Analysis/FurtherTopology.thy	Tue Oct 18 12:01:54 2016 +0200
+++ b/src/HOL/Analysis/FurtherTopology.thy	Tue Oct 18 15:55:53 2016 +0100
@@ -3,7 +3,7 @@
 text\<open>Ported from HOL Light (moretop.ml) by L C Paulson\<close>
 
 theory "FurtherTopology"
-  imports Equivalence_Lebesgue_Henstock_Integration Weierstrass_Theorems Polytope
+  imports Equivalence_Lebesgue_Henstock_Integration Weierstrass_Theorems Polytope Complex_Transcendental
 
 begin
 
@@ -2352,4 +2352,747 @@
   using invariance_of_domain_homeomorphism [OF assms]
   by (meson homeomorphic_def)
 
+lemma continuous_image_subset_interior:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "continuous_on S f" "inj_on f S" "DIM('b) \<le> DIM('a)"
+  shows "f ` (interior S) \<subseteq> interior(f ` S)"
+  apply (rule interior_maximal)
+   apply (simp add: image_mono interior_subset)
+  apply (rule invariance_of_domain_gen)
+  using assms
+     apply (auto simp: subset_inj_on interior_subset continuous_on_subset)
+  done
+
+lemma homeomorphic_interiors_same_dimension:
+  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+  assumes "S homeomorphic T" and dimeq: "DIM('a) = DIM('b)"
+  shows "(interior S) homeomorphic (interior T)"
+  using assms [unfolded homeomorphic_minimal]
+  unfolding homeomorphic_def
+proof (clarify elim!: ex_forward)
+  fix f g
+  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"
+     and contf: "continuous_on S f" and contg: "continuous_on T g"
+  then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T"
+    by (auto simp: inj_on_def intro: rev_image_eqI) metis+
+  have fim: "f ` interior S \<subseteq> interior T"
+    using continuous_image_subset_interior [OF contf \<open>inj_on f S\<close>] dimeq fST by simp
+  have gim: "g ` interior T \<subseteq> interior S"
+    using continuous_image_subset_interior [OF contg \<open>inj_on g T\<close>] dimeq gTS by simp
+  show "homeomorphism (interior S) (interior T) f g"
+    unfolding homeomorphism_def
+  proof (intro conjI ballI)
+    show "\<And>x. x \<in> interior S \<Longrightarrow> g (f x) = x"
+      by (meson \<open>\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x\<close> subsetD interior_subset)
+    have "interior T \<subseteq> f ` interior S"
+    proof
+      fix x assume "x \<in> interior T"
+      then have "g x \<in> interior S"
+        using gim by blast
+      then show "x \<in> f ` interior S"
+        by (metis T \<open>x \<in> interior T\<close> image_iff interior_subset subsetCE)
+    qed
+    then show "f ` interior S = interior T"
+      using fim by blast
+    show "continuous_on (interior S) f"
+      by (metis interior_subset continuous_on_subset contf)
+    show "\<And>y. y \<in> interior T \<Longrightarrow> f (g y) = y"
+      by (meson T subsetD interior_subset)
+    have "interior S \<subseteq> g ` interior T"
+    proof
+      fix x assume "x \<in> interior S"
+      then have "f x \<in> interior T"
+        using fim by blast
+      then show "x \<in> g ` interior T"
+        by (metis S \<open>x \<in> interior S\<close> image_iff interior_subset subsetCE)
+    qed
+    then show "g ` interior T = interior S"
+      using gim by blast
+    show "continuous_on (interior T) g"
+      by (metis interior_subset continuous_on_subset contg)
+  qed
+qed
+
+lemma homeomorphic_open_imp_same_dimension:
+  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+  assumes "S homeomorphic T" "open S" "S \<noteq> {}" "open T" "T \<noteq> {}"
+  shows "DIM('a) = DIM('b)"
+    using assms
+    apply (simp add: homeomorphic_minimal)
+    apply (rule order_antisym; metis inj_onI invariance_of_dimension)
+    done
+
+lemma homeomorphic_interiors:
+  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+  assumes "S homeomorphic T" "interior S = {} \<longleftrightarrow> interior T = {}"
+    shows "(interior S) homeomorphic (interior T)"
+proof (cases "interior T = {}")
+  case True
+  with assms show ?thesis by auto
+next
+  case False
+  then have "DIM('a) = DIM('b)"
+    using assms
+    apply (simp add: homeomorphic_minimal)
+    apply (rule order_antisym; metis continuous_on_subset inj_onI inj_on_subset interior_subset invariance_of_dimension open_interior)
+    done
+  then show ?thesis
+    by (rule homeomorphic_interiors_same_dimension [OF \<open>S homeomorphic T\<close>])
+qed
+
+lemma homeomorphic_frontiers_same_dimension:
+  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+  assumes "S homeomorphic T" "closed S" "closed T" and dimeq: "DIM('a) = DIM('b)"
+  shows "(frontier S) homeomorphic (frontier T)"
+  using assms [unfolded homeomorphic_minimal]
+  unfolding homeomorphic_def
+proof (clarify elim!: ex_forward)
+  fix f g
+  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"
+     and contf: "continuous_on S f" and contg: "continuous_on T g"
+  then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T"
+    by (auto simp: inj_on_def intro: rev_image_eqI) metis+
+  have "g ` interior T \<subseteq> interior S"
+    using continuous_image_subset_interior [OF contg \<open>inj_on g T\<close>] dimeq gTS by simp
+  then have fim: "f ` frontier S \<subseteq> frontier T"
+    apply (simp add: frontier_def)
+    using continuous_image_subset_interior assms(2) assms(3) S by auto
+  have "f ` interior S \<subseteq> interior T"
+    using continuous_image_subset_interior [OF contf \<open>inj_on f S\<close>] dimeq fST by simp
+  then have gim: "g ` frontier T \<subseteq> frontier S"
+    apply (simp add: frontier_def)
+    using continuous_image_subset_interior T assms(2) assms(3) by auto
+  show "homeomorphism (frontier S) (frontier T) f g"
+    unfolding homeomorphism_def
+  proof (intro conjI ballI)
+    show gf: "\<And>x. x \<in> frontier S \<Longrightarrow> g (f x) = x"
+      by (simp add: S assms(2) frontier_def)
+    show fg: "\<And>y. y \<in> frontier T \<Longrightarrow> f (g y) = y"
+      by (simp add: T assms(3) frontier_def)
+    have "frontier T \<subseteq> f ` frontier S"
+    proof
+      fix x assume "x \<in> frontier T"
+      then have "g x \<in> frontier S"
+        using gim by blast
+      then show "x \<in> f ` frontier S"
+        by (metis fg \<open>x \<in> frontier T\<close> imageI)
+    qed
+    then show "f ` frontier S = frontier T"
+      using fim by blast
+    show "continuous_on (frontier S) f"
+      by (metis Diff_subset assms(2) closure_eq contf continuous_on_subset frontier_def)
+    have "frontier S \<subseteq> g ` frontier T"
+    proof
+      fix x assume "x \<in> frontier S"
+      then have "f x \<in> frontier T"
+        using fim by blast
+      then show "x \<in> g ` frontier T"
+        by (metis gf \<open>x \<in> frontier S\<close> imageI)
+    qed
+    then show "g ` frontier T = frontier S"
+      using gim by blast
+    show "continuous_on (frontier T) g"
+      by (metis Diff_subset assms(3) closure_closed contg continuous_on_subset frontier_def)
+  qed
+qed
+
+lemma homeomorphic_frontiers:
+  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+  assumes "S homeomorphic T" "closed S" "closed T"
+          "interior S = {} \<longleftrightarrow> interior T = {}"
+    shows "(frontier S) homeomorphic (frontier T)"
+proof (cases "interior T = {}")
+  case True
+  then show ?thesis
+    by (metis Diff_empty assms closure_eq frontier_def)
+next
+  case False
+  show ?thesis
+    apply (rule homeomorphic_frontiers_same_dimension)
+       apply (simp_all add: assms)
+    using False assms homeomorphic_interiors homeomorphic_open_imp_same_dimension by blast
+qed
+
+lemma continuous_image_subset_rel_interior:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \<subseteq> T"
+      and TS: "aff_dim T \<le> aff_dim S"
+  shows "f ` (rel_interior S) \<subseteq> rel_interior(f ` S)"
+proof (rule rel_interior_maximal)
+  show "f ` rel_interior S \<subseteq> f ` S"
+    by(simp add: image_mono rel_interior_subset)
+  show "openin (subtopology euclidean (affine hull f ` S)) (f ` rel_interior S)"
+  proof (rule invariance_of_domain_affine_sets)
+    show "openin (subtopology euclidean (affine hull S)) (rel_interior S)"
+      by (simp add: openin_rel_interior)
+    show "aff_dim (affine hull f ` S) \<le> aff_dim (affine hull S)"
+      by (metis aff_dim_affine_hull aff_dim_subset fim TS order_trans)
+    show "f ` rel_interior S \<subseteq> affine hull f ` S"
+      by (meson \<open>f ` rel_interior S \<subseteq> f ` S\<close> hull_subset order_trans)
+    show "continuous_on (rel_interior S) f"
+      using contf continuous_on_subset rel_interior_subset by blast
+    show "inj_on f (rel_interior S)"
+      using inj_on_subset injf rel_interior_subset by blast
+  qed auto
+qed
+
+lemma homeomorphic_rel_interiors_same_dimension:
+  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+  assumes "S homeomorphic T" and aff: "aff_dim S = aff_dim T"
+  shows "(rel_interior S) homeomorphic (rel_interior T)"
+  using assms [unfolded homeomorphic_minimal]
+  unfolding homeomorphic_def
+proof (clarify elim!: ex_forward)
+  fix f g
+  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"
+     and contf: "continuous_on S f" and contg: "continuous_on T g"
+  then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T"
+    by (auto simp: inj_on_def intro: rev_image_eqI) metis+
+  have fim: "f ` rel_interior S \<subseteq> rel_interior T"
+    by (metis \<open>inj_on f S\<close> aff contf continuous_image_subset_rel_interior fST order_refl)
+  have gim: "g ` rel_interior T \<subseteq> rel_interior S"
+    by (metis \<open>inj_on g T\<close> aff contg continuous_image_subset_rel_interior gTS order_refl)
+  show "homeomorphism (rel_interior S) (rel_interior T) f g"
+    unfolding homeomorphism_def
+  proof (intro conjI ballI)
+    show gf: "\<And>x. x \<in> rel_interior S \<Longrightarrow> g (f x) = x"
+      using S rel_interior_subset by blast
+    show fg: "\<And>y. y \<in> rel_interior T \<Longrightarrow> f (g y) = y"
+      using T mem_rel_interior_ball by blast
+    have "rel_interior T \<subseteq> f ` rel_interior S"
+    proof
+      fix x assume "x \<in> rel_interior T"
+      then have "g x \<in> rel_interior S"
+        using gim by blast
+      then show "x \<in> f ` rel_interior S"
+        by (metis fg \<open>x \<in> rel_interior T\<close> imageI)
+    qed
+    moreover have "f ` rel_interior S \<subseteq> rel_interior T"
+      by (metis \<open>inj_on f S\<close> aff contf continuous_image_subset_rel_interior fST order_refl)
+    ultimately show "f ` rel_interior S = rel_interior T"
+      by blast
+    show "continuous_on (rel_interior S) f"
+      using contf continuous_on_subset rel_interior_subset by blast
+    have "rel_interior S \<subseteq> g ` rel_interior T"
+    proof
+      fix x assume "x \<in> rel_interior S"
+      then have "f x \<in> rel_interior T"
+        using fim by blast
+      then show "x \<in> g ` rel_interior T"
+        by (metis gf \<open>x \<in> rel_interior S\<close> imageI)
+    qed
+    then show "g ` rel_interior T = rel_interior S"
+      using gim by blast
+    show "continuous_on (rel_interior T) g"
+      using contg continuous_on_subset rel_interior_subset by blast
+  qed
+qed
+
+lemma homeomorphic_rel_interiors:
+  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+  assumes "S homeomorphic T" "rel_interior S = {} \<longleftrightarrow> rel_interior T = {}"
+    shows "(rel_interior S) homeomorphic (rel_interior T)"
+proof (cases "rel_interior T = {}")
+  case True
+  with assms show ?thesis by auto
+next
+  case False
+  obtain f g
+    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"
+      and contf: "continuous_on S f" and contg: "continuous_on T g"
+    using  assms [unfolded homeomorphic_minimal] by auto
+  have "aff_dim (affine hull S) \<le> aff_dim (affine hull T)"
+    apply (rule invariance_of_dimension_affine_sets [of _ "rel_interior S" _ f])
+          apply (simp_all add: openin_rel_interior False assms)
+    using contf continuous_on_subset rel_interior_subset apply blast
+      apply (meson S hull_subset image_subsetI rel_interior_subset rev_subsetD)
+    apply (metis S inj_on_inverseI inj_on_subset rel_interior_subset)
+    done
+  moreover have "aff_dim (affine hull T) \<le> aff_dim (affine hull S)"
+    apply (rule invariance_of_dimension_affine_sets [of _ "rel_interior T" _ g])
+          apply (simp_all add: openin_rel_interior False assms)
+    using contg continuous_on_subset rel_interior_subset apply blast
+      apply (meson T hull_subset image_subsetI rel_interior_subset rev_subsetD)
+    apply (metis T inj_on_inverseI inj_on_subset rel_interior_subset)
+    done
+  ultimately have "aff_dim S = aff_dim T" by force
+  then show ?thesis
+    by (rule homeomorphic_rel_interiors_same_dimension [OF \<open>S homeomorphic T\<close>])
+qed
+
+
+lemma homeomorphic_rel_boundaries_same_dimension:
+  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+  assumes "S homeomorphic T" and aff: "aff_dim S = aff_dim T"
+  shows "(S - rel_interior S) homeomorphic (T - rel_interior T)"
+  using assms [unfolded homeomorphic_minimal]
+  unfolding homeomorphic_def
+proof (clarify elim!: ex_forward)
+  fix f g
+  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"
+     and contf: "continuous_on S f" and contg: "continuous_on T g"
+  then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T"
+    by (auto simp: inj_on_def intro: rev_image_eqI) metis+
+  have fim: "f ` rel_interior S \<subseteq> rel_interior T"
+    by (metis \<open>inj_on f S\<close> aff contf continuous_image_subset_rel_interior fST order_refl)
+  have gim: "g ` rel_interior T \<subseteq> rel_interior S"
+    by (metis \<open>inj_on g T\<close> aff contg continuous_image_subset_rel_interior gTS order_refl)
+  show "homeomorphism (S - rel_interior S) (T - rel_interior T) f g"
+    unfolding homeomorphism_def
+  proof (intro conjI ballI)
+    show gf: "\<And>x. x \<in> S - rel_interior S \<Longrightarrow> g (f x) = x"
+      using S rel_interior_subset by blast
+    show fg: "\<And>y. y \<in> T - rel_interior T \<Longrightarrow> f (g y) = y"
+      using T mem_rel_interior_ball by blast
+    show "f ` (S - rel_interior S) = T - rel_interior T"
+      using S fST fim gim by auto
+    show "continuous_on (S - rel_interior S) f"
+      using contf continuous_on_subset rel_interior_subset by blast
+    show "g ` (T - rel_interior T) = S - rel_interior S"
+      using T gTS gim fim by auto
+    show "continuous_on (T - rel_interior T) g"
+      using contg continuous_on_subset rel_interior_subset by blast
+  qed
+qed
+
+lemma homeomorphic_rel_boundaries:
+  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+  assumes "S homeomorphic T" "rel_interior S = {} \<longleftrightarrow> rel_interior T = {}"
+    shows "(S - rel_interior S) homeomorphic (T - rel_interior T)"
+proof (cases "rel_interior T = {}")
+  case True
+  with assms show ?thesis by auto
+next
+  case False
+  obtain f g
+    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"
+      and contf: "continuous_on S f" and contg: "continuous_on T g"
+    using  assms [unfolded homeomorphic_minimal] by auto
+  have "aff_dim (affine hull S) \<le> aff_dim (affine hull T)"
+    apply (rule invariance_of_dimension_affine_sets [of _ "rel_interior S" _ f])
+          apply (simp_all add: openin_rel_interior False assms)
+    using contf continuous_on_subset rel_interior_subset apply blast
+      apply (meson S hull_subset image_subsetI rel_interior_subset rev_subsetD)
+    apply (metis S inj_on_inverseI inj_on_subset rel_interior_subset)
+    done
+  moreover have "aff_dim (affine hull T) \<le> aff_dim (affine hull S)"
+    apply (rule invariance_of_dimension_affine_sets [of _ "rel_interior T" _ g])
+          apply (simp_all add: openin_rel_interior False assms)
+    using contg continuous_on_subset rel_interior_subset apply blast
+      apply (meson T hull_subset image_subsetI rel_interior_subset rev_subsetD)
+    apply (metis T inj_on_inverseI inj_on_subset rel_interior_subset)
+    done
+  ultimately have "aff_dim S = aff_dim T" by force
+  then show ?thesis
+    by (rule homeomorphic_rel_boundaries_same_dimension [OF \<open>S homeomorphic T\<close>])
+qed
+
+proposition uniformly_continuous_homeomorphism_UNIV_trivial:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
+  assumes contf: "uniformly_continuous_on S f" and hom: "homeomorphism S UNIV f g"
+  shows "S = UNIV"
+proof (cases "S = {}")
+  case True
+  then show ?thesis
+    by (metis UNIV_I hom empty_iff homeomorphism_def image_eqI)
+next
+  case False
+  have "inj g"
+    by (metis UNIV_I hom homeomorphism_apply2 injI)
+  then have "open (g ` UNIV)"
+    by (blast intro: invariance_of_domain hom homeomorphism_cont2)
+  then have "open S"
+    using hom homeomorphism_image2 by blast
+  moreover have "complete S"
+    unfolding complete_def
+  proof clarify
+    fix \<sigma>
+    assume \<sigma>: "\<forall>n. \<sigma> n \<in> S" and "Cauchy \<sigma>"
+    have "Cauchy (f o \<sigma>)"
+      using uniformly_continuous_imp_Cauchy_continuous \<open>Cauchy \<sigma>\<close> \<sigma> contf by blast
+    then obtain l where "(f \<circ> \<sigma>) \<longlonglongrightarrow> l"
+      by (auto simp: convergent_eq_Cauchy [symmetric])
+    show "\<exists>l\<in>S. \<sigma> \<longlonglongrightarrow> l"
+    proof
+      show "g l \<in> S"
+        using hom homeomorphism_image2 by blast
+      have "(g \<circ> (f \<circ> \<sigma>)) \<longlonglongrightarrow> g l"
+        by (meson UNIV_I \<open>(f \<circ> \<sigma>) \<longlonglongrightarrow> l\<close> continuous_on_sequentially hom homeomorphism_cont2)
+      then show "\<sigma> \<longlonglongrightarrow> g l"
+      proof -
+        have "\<forall>n. \<sigma> n = (g \<circ> (f \<circ> \<sigma>)) n"
+          by (metis (no_types) \<sigma> comp_eq_dest_lhs hom homeomorphism_apply1)
+        then show ?thesis
+          by (metis (no_types) LIMSEQ_iff \<open>(g \<circ> (f \<circ> \<sigma>)) \<longlonglongrightarrow> g l\<close>)
+      qed
+    qed
+  qed
+  then have "closed S"
+    by (simp add: complete_eq_closed)
+  ultimately show ?thesis
+    using clopen [of S] False  by simp
+qed
+
+subsection\<open>The power, squaring and exponential functions as covering maps\<close>
+
+proposition covering_space_power_punctured_plane:
+  assumes "0 < n"
+    shows "covering_space (- {0}) (\<lambda>z::complex. z^n) (- {0})"
+proof -
+  consider "n = 1" | "2 \<le> n" using assms by linarith
+  then obtain e where "0 < e"
+                and e: "\<And>w z. cmod(w - z) < e * cmod z \<Longrightarrow> (w^n = z^n \<longleftrightarrow> w = z)"
+  proof cases
+    assume "n = 1" then show ?thesis
+      by (rule_tac e=1 in that) auto
+  next
+    assume "2 \<le> n"
+    have eq_if_pow_eq:
+         "w = z" if lt: "cmod (w - z) < 2 * sin (pi / real n) * cmod z"
+                 and eq: "w^n = z^n" for w z
+    proof (cases "z = 0")
+      case True with eq assms show ?thesis by (auto simp: power_0_left)
+    next
+      case False
+      then have "z \<noteq> 0" by auto
+      have "(w/z)^n = 1"
+        by (metis False divide_self_if eq power_divide power_one)
+      then obtain j where j: "w / z = exp (2 * of_real pi * \<i> * j / n)" and "j < n"
+        using Suc_leI assms \<open>2 \<le> n\<close> complex_roots_unity [THEN eqset_imp_iff, of n "w/z"]
+        by force
+      have "cmod (w/z - 1) < 2 * sin (pi / real n)"
+        using lt assms \<open>z \<noteq> 0\<close> by (simp add: divide_simps norm_divide)
+      then have "cmod (exp (\<i> * of_real (2 * pi * j / n)) - 1) < 2 * sin (pi / real n)"
+        by (simp add: j field_simps)
+      then have "2 * \<bar>sin((2 * pi * j / n) / 2)\<bar> < 2 * sin (pi / real n)"
+        by (simp only: dist_exp_ii_1)
+      then have sin_less: "sin((pi * j / n)) < sin (pi / real n)"
+        by (simp add: field_simps)
+      then have "w / z = 1"
+      proof (cases "j = 0")
+        case True then show ?thesis by (auto simp: j)
+      next
+        case False
+        then have "sin (pi / real n) \<le> sin((pi * j / n))"
+        proof (cases "j / n \<le> 1/2")
+          case True
+          show ?thesis
+            apply (rule sin_monotone_2pi_le)
+            using \<open>j \<noteq> 0 \<close> \<open>j < n\<close> True
+            apply (auto simp: field_simps intro: order_trans [of _ 0])
+            done
+        next
+          case False
+          then have seq: "sin(pi * j / n) = sin(pi * (n - j) / n)"
+            using \<open>j < n\<close> by (simp add: algebra_simps diff_divide_distrib of_nat_diff)
+          show ?thesis
+            apply (simp only: seq)
+            apply (rule sin_monotone_2pi_le)
+            using \<open>j < n\<close> False
+            apply (auto simp: field_simps intro: order_trans [of _ 0])
+            done
+        qed
+        with sin_less show ?thesis by force
+      qed
+      then show ?thesis by simp
+    qed
+    show ?thesis
+      apply (rule_tac e = "2 * sin(pi / n)" in that)
+       apply (force simp: \<open>2 \<le> n\<close> sin_pi_divide_n_gt_0)
+      apply (meson eq_if_pow_eq)
+      done
+  qed
+  have zn1: "continuous_on (- {0}) (\<lambda>z::complex. z^n)"
+    by (rule continuous_intros)+
+  have zn2: "(\<lambda>z::complex. z^n) ` (- {0}) = - {0}"
+    using assms by (auto simp: image_def elim: exists_complex_root_nonzero [where n = n])
+  have zn3: "\<exists>T. z^n \<in> T \<and> open T \<and> 0 \<notin> T \<and>
+               (\<exists>v. \<Union>v = {x. x \<noteq> 0 \<and> x^n \<in> T} \<and>
+                    (\<forall>u\<in>v. open u \<and> 0 \<notin> u) \<and>
+                    pairwise disjnt v \<and>
+                    (\<forall>u\<in>v. Ex (homeomorphism u T (\<lambda>z. z^n))))"
+           if "z \<noteq> 0" for z::complex
+  proof -
+    def d \<equiv> "min (1/2) (e/4) * norm z"
+    have "0 < d"
+      by (simp add: d_def \<open>0 < e\<close> \<open>z \<noteq> 0\<close>)
+    have iff_x_eq_y: "x^n = y^n \<longleftrightarrow> x = y"
+         if eq: "w^n = z^n" and x: "x \<in> ball w d" and y: "y \<in> ball w d" for w x y
+    proof -
+      have [simp]: "norm z = norm w" using that
+        by (simp add: assms power_eq_imp_eq_norm)
+      show ?thesis
+      proof (cases "w = 0")
+        case True with \<open>z \<noteq> 0\<close> assms eq
+        show ?thesis by (auto simp: power_0_left)
+      next
+        case False
+        have "cmod (x - y) < 2*d"
+          using x y
+          by (simp add: dist_norm [symmetric]) (metis dist_commute mult_2 dist_triangle_less_add)
+        also have "... \<le> 2 * e / 4 * norm w"
+          using \<open>e > 0\<close> by (simp add: d_def min_mult_distrib_right)
+        also have "... = e * (cmod w / 2)"
+          by simp
+        also have "... \<le> e * cmod y"
+          apply (rule mult_left_mono)
+          using \<open>e > 0\<close> y
+           apply (simp_all add: dist_norm d_def min_mult_distrib_right del: divide_const_simps)
+          apply (metis dist_0_norm dist_complex_def dist_triangle_half_l linorder_not_less order_less_irrefl)
+          done
+        finally have "cmod (x - y) < e * cmod y" .
+        then show ?thesis by (rule e)
+      qed
+    qed
+    then have inj: "inj_on (\<lambda>w. w^n) (ball z d)"
+      by (simp add: inj_on_def)
+    have cont: "continuous_on (ball z d) (\<lambda>w. w ^ n)"
+      by (intro continuous_intros)
+    have noncon: "\<not> (\<lambda>w::complex. w^n) constant_on UNIV"
+      by (metis UNIV_I assms constant_on_def power_one zero_neq_one zero_power)
+    have open_imball: "open ((\<lambda>w. w^n) ` ball z d)"
+      by (rule invariance_of_domain [OF cont open_ball inj])
+    have im_eq: "(\<lambda>w. w^n) ` ball z' d = (\<lambda>w. w^n) ` ball z d"
+                if z': "z'^n = z^n" for z'
+    proof -
+      have nz': "norm z' = norm z" using that assms power_eq_imp_eq_norm by blast
+      have "(w \<in> (\<lambda>w. w^n) ` ball z' d) = (w \<in> (\<lambda>w. w^n) ` ball z d)" for w
+      proof (cases "w=0")
+        case True with assms show ?thesis
+          by (simp add: image_def ball_def nz')
+      next
+        case False
+        have "z' \<noteq> 0" using \<open>z \<noteq> 0\<close> nz' by force
+        have [simp]: "(z*x / z')^n = x^n" if "x \<noteq> 0" for x
+          using z' that by (simp add: field_simps \<open>z \<noteq> 0\<close>)
+        have [simp]: "cmod (z - z * x / z') = cmod (z' - x)" if "x \<noteq> 0" for x
+        proof -
+          have "cmod (z - z * x / z') = cmod z * cmod (1 - x / z')"
+            by (metis (no_types) ab_semigroup_mult_class.mult_ac(1) complex_divide_def mult.right_neutral norm_mult right_diff_distrib')
+          also have "... = cmod z' * cmod (1 - x / z')"
+            by (simp add: nz')
+          also have "... = cmod (z' - x)"
+            by (simp add: \<open>z' \<noteq> 0\<close> diff_divide_eq_iff norm_divide)
+          finally show ?thesis .
+        qed
+        have [simp]: "(z'*x / z)^n = x^n" if "x \<noteq> 0" for x
+          using z' that by (simp add: field_simps \<open>z \<noteq> 0\<close>)
+        have [simp]: "cmod (z' - z' * x / z) = cmod (z - x)" if "x \<noteq> 0" for x
+        proof -
+          have "cmod (z * (1 - x * inverse z)) = cmod (z - x)"
+            by (metis \<open>z \<noteq> 0\<close> diff_divide_distrib divide_complex_def divide_self_if nonzero_eq_divide_eq semiring_normalization_rules(7))
+          then show ?thesis
+            by (metis (no_types) mult.assoc complex_divide_def mult.right_neutral norm_mult nz' right_diff_distrib')
+        qed
+        show ?thesis
+          unfolding image_def ball_def
+          apply safe
+          apply simp_all
+          apply (rule_tac x="z/z' * x" in exI)
+          using assms False apply (simp add: dist_norm)
+          apply (rule_tac x="z'/z * x" in exI)
+          using assms False apply (simp add: dist_norm)
+          done
+      qed
+      then show ?thesis by blast
+    qed
+    have ex_ball: "\<exists>B. (\<exists>z'. B = ball z' d \<and> z'^n = z^n) \<and> x \<in> B"
+                  if "x \<noteq> 0" and eq: "x^n = w^n" and dzw: "dist z w < d" for x w
+    proof -
+      have "w \<noteq> 0" by (metis assms power_eq_0_iff that(1) that(2))
+      have [simp]: "cmod x = cmod w"
+        using assms power_eq_imp_eq_norm eq by blast
+      have [simp]: "cmod (x * z / w - x) = cmod (z - w)"
+      proof -
+        have "cmod (x * z / w - x) = cmod x * cmod (z / w - 1)"
+          by (metis (no_types) mult.right_neutral norm_mult right_diff_distrib' times_divide_eq_right)
+        also have "... = cmod w * cmod (z / w - 1)"
+          by simp
+        also have "... = cmod (z - w)"
+          by (simp add: \<open>w \<noteq> 0\<close> divide_diff_eq_iff nonzero_norm_divide)
+        finally show ?thesis .
+      qed
+      show ?thesis
+        apply (rule_tac x="ball (z / w * x) d" in exI)
+        using \<open>d > 0\<close> that
+        apply (simp add: ball_eq_ball_iff)
+        apply (simp add: \<open>z \<noteq> 0\<close> \<open>w \<noteq> 0\<close> field_simps)
+        apply (simp add: dist_norm)
+        done
+    qed
+    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}"
+      apply (rule equalityI)
+       prefer 2 apply (force simp: ex_ball, clarsimp)
+      apply (subst im_eq [symmetric], assumption)
+      using assms
+      apply (force simp: dist_norm d_def min_mult_distrib_right dest: power_eq_imp_eq_norm)
+      done
+    have ball2: "pairwise disjnt {ball z' d |z'. z'^n = z^n}"
+    proof (clarsimp simp add: pairwise_def disjnt_iff)
+      fix \<xi> \<zeta> x
+      assume "\<xi>^n = z^n" "\<zeta>^n = z^n" "ball \<xi> d \<noteq> ball \<zeta> d"
+         and "dist \<xi> x < d" "dist \<zeta> x < d"
+      then have "dist \<xi> \<zeta> < d+d"
+        using dist_triangle_less_add by blast
+      then have "cmod (\<xi> - \<zeta>) < 2*d"
+        by (simp add: dist_norm)
+      also have "... \<le> e * cmod z"
+        using mult_right_mono \<open>0 < e\<close> that by (auto simp: d_def)
+      finally have "cmod (\<xi> - \<zeta>) < e * cmod z" .
+      with e have "\<xi> = \<zeta>"
+        by (metis \<open>\<xi>^n = z^n\<close> \<open>\<zeta>^n = z^n\<close> assms power_eq_imp_eq_norm)
+      then show "False"
+        using \<open>ball \<xi> d \<noteq> ball \<zeta> d\<close> by blast
+    qed
+    have ball3: "Ex (homeomorphism (ball z' d) ((\<lambda>w. w^n) ` ball z d) (\<lambda>z. z^n))"
+            if zeq: "z'^n = z^n" for z'
+    proof -
+      have inj: "inj_on (\<lambda>z. z ^ n) (ball z' d)"
+        by (meson iff_x_eq_y inj_onI zeq)
+      show ?thesis
+        apply (rule invariance_of_domain_homeomorphism [of "ball z' d" "\<lambda>z. z^n"])
+          apply (rule open_ball continuous_intros order_refl inj)+
+        apply (force simp: im_eq [OF zeq])
+        done
+    qed
+    show ?thesis
+      apply (rule_tac x = "(\<lambda>w. w^n) ` (ball z d)" in exI)
+      apply (intro conjI open_imball)
+        using \<open>d > 0\<close> apply simp
+       using \<open>z \<noteq> 0\<close> assms apply (force simp: d_def)
+      apply (rule_tac x="{ ball z' d |z'. z'^n = z^n}" in exI)
+      apply (intro conjI ball1 ball2)
+       apply (force simp: assms d_def power_eq_imp_eq_norm that, clarify)
+      by (metis ball3)
+  qed
+  show ?thesis
+    using assms
+    apply (simp add: covering_space_def zn1 zn2)
+    apply (subst zn2 [symmetric])
+    apply (simp add: openin_open_eq open_Compl)
+    apply (blast intro: zn3)
+    done
+qed
+
+corollary covering_space_square_punctured_plane:
+  "covering_space (- {0}) (\<lambda>z::complex. z^2) (- {0})"
+  by (simp add: covering_space_power_punctured_plane)
+
+
+
+proposition covering_space_exp_punctured_plane:
+  "covering_space UNIV (\<lambda>z::complex. exp z) (- {0})"
+proof (simp add: covering_space_def, intro conjI ballI)
+  show "continuous_on UNIV (\<lambda>z::complex. exp z)"
+    by (rule continuous_on_exp [OF continuous_on_id])
+  show "range exp = - {0::complex}"
+    by auto (metis exp_Ln range_eqI)
+  show "\<exists>T. z \<in> T \<and> openin (subtopology euclidean (- {0})) T \<and>
+             (\<exists>v. \<Union>v = {z. exp z \<in> T} \<and> (\<forall>u\<in>v. open u) \<and> disjoint v \<and>
+                  (\<forall>u\<in>v. \<exists>q. homeomorphism u T exp q))"
+        if "z \<in> - {0::complex}" for z
+  proof -
+    have "z \<noteq> 0"
+      using that by auto
+    have inj_exp: "inj_on exp (ball (Ln z) 1)"
+      apply (rule inj_on_subset [OF inj_on_exp_pi [of "Ln z"]])
+      using pi_ge_two by (simp add: ball_subset_ball_iff)
+    define \<V> where "\<V> \<equiv> range (\<lambda>n. (\<lambda>x. x + of_real (2 * of_int n * pi) * ii) ` (ball(Ln z) 1))"
+    show ?thesis
+    proof (intro exI conjI)
+      show "z \<in> exp ` (ball(Ln z) 1)"
+        by (metis \<open>z \<noteq> 0\<close> centre_in_ball exp_Ln rev_image_eqI zero_less_one)
+      have "open (- {0::complex})"
+        by blast
+      moreover have "inj_on exp (ball (Ln z) 1)"
+        apply (rule inj_on_subset [OF inj_on_exp_pi [of "Ln z"]])
+        using pi_ge_two by (simp add: ball_subset_ball_iff)
+      ultimately show "openin (subtopology euclidean (- {0})) (exp ` ball (Ln z) 1)"
+        by (auto simp: openin_open_eq invariance_of_domain continuous_on_exp [OF continuous_on_id])
+      show "\<Union>\<V> = {w. exp w \<in> exp ` ball (Ln z) 1}"
+        by (auto simp: \<V>_def Complex_Transcendental.exp_eq image_iff)
+      show "\<forall>V\<in>\<V>. open V"
+        by (auto simp: \<V>_def inj_on_def continuous_intros invariance_of_domain)
+      have xy: "2 \<le> cmod (2 * of_int x * of_real pi * \<i> - 2 * of_int y * of_real pi * \<i>)"
+               if "x < y" for x y
+      proof -
+        have "1 \<le> abs (x - y)"
+          using that by linarith
+        then have "1 \<le> cmod (of_int x - of_int y) * 1"
+          by (metis mult.right_neutral norm_of_int of_int_1_le_iff of_int_abs of_int_diff)
+        also have "... \<le> cmod (of_int x - of_int y) * of_real pi"
+          apply (rule mult_left_mono)
+          using pi_ge_two by auto
+        also have "... \<le> cmod ((of_int x - of_int y) * of_real pi * \<i>)"
+          by (simp add: norm_mult)
+        also have "... \<le> cmod (of_int x * of_real pi * \<i> - of_int y * of_real pi * \<i>)"
+          by (simp add: algebra_simps)
+        finally have "1 \<le> cmod (of_int x * of_real pi * \<i> - of_int y * of_real pi * \<i>)" .
+        then have "2 * 1 \<le> cmod (2 * (of_int x * of_real pi * \<i> - of_int y * of_real pi * \<i>))"
+          by (metis mult_le_cancel_left_pos norm_mult_numeral1 zero_less_numeral)
+        then show ?thesis
+          by (simp add: algebra_simps)
+      qed
+      show "disjoint \<V>"
+        apply (clarsimp simp add: \<V>_def pairwise_def disjnt_def add.commute [of _ "x*y" for x y]
+                        image_add_ball ball_eq_ball_iff)
+        apply (rule disjoint_ballI)
+        apply (auto simp: dist_norm neq_iff)
+        by (metis norm_minus_commute xy)+
+      show "\<forall>u\<in>\<V>. \<exists>q. homeomorphism u (exp ` ball (Ln z) 1) exp q"
+      proof
+        fix u
+        assume "u \<in> \<V>"
+        then obtain n where n: "u = (\<lambda>x. x + of_real (2 * of_int n * pi) * ii) ` (ball(Ln z) 1)"
+          by (auto simp: \<V>_def)
+        have "compact (cball (Ln z) 1)"
+          by simp
+        moreover have "continuous_on (cball (Ln z) 1) exp"
+          by (rule continuous_on_exp [OF continuous_on_id])
+        moreover have "inj_on exp (cball (Ln z) 1)"
+          apply (rule inj_on_subset [OF inj_on_exp_pi [of "Ln z"]])
+          using pi_ge_two by (simp add: cball_subset_ball_iff)
+        ultimately obtain \<gamma> where hom: "homeomorphism (cball (Ln z) 1) (exp ` cball (Ln z) 1) exp \<gamma>"
+          using homeomorphism_compact  by blast
+        have eq1: "exp ` u = exp ` ball (Ln z) 1"
+          unfolding n
+          apply (auto simp: algebra_simps)
+          apply (rename_tac w)
+          apply (rule_tac x = "w + \<i> * (of_int n * (of_real pi * 2))" in image_eqI)
+          apply (auto simp: image_iff)
+          done
+        have \<gamma>exp: "\<gamma> (exp x) + 2 * of_int n * of_real pi * \<i> = x" if "x \<in> u" for x
+        proof -
+          have "exp x = exp (x - 2 * of_int n * of_real pi * \<i>)"
+            by (simp add: exp_eq)
+          then have "\<gamma> (exp x) = \<gamma> (exp (x - 2 * of_int n * of_real pi * \<i>))"
+            by simp
+          also have "... = x - 2 * of_int n * of_real pi * \<i>"
+            apply (rule homeomorphism_apply1 [OF hom])
+            using \<open>x \<in> u\<close> by (auto simp: n)
+          finally show ?thesis
+            by simp
+        qed
+        have exp2n: "exp (\<gamma> (exp x) + 2 * of_int n * complex_of_real pi * \<i>) = exp x"
+                if "dist (Ln z) x < 1" for x
+          using that by (auto simp: exp_eq homeomorphism_apply1 [OF hom])
+        have cont: "continuous_on (exp ` ball (Ln z) 1) (\<lambda>x. \<gamma> x + 2 * of_int n * complex_of_real pi * \<i>)"
+          apply (intro continuous_intros)
+          apply (rule continuous_on_subset [OF homeomorphism_cont2 [OF hom]])
+          apply (force simp:)
+          done
+        show "\<exists>q. homeomorphism u (exp ` ball (Ln z) 1) exp q"
+          apply (rule_tac x="(\<lambda>x. x + of_real(2 * n * pi) * ii) \<circ> \<gamma>" in exI)
+          unfolding homeomorphism_def
+          apply (intro conjI ballI eq1 continuous_on_exp [OF continuous_on_id])
+             apply (auto simp: \<gamma>exp exp2n cont n)
+           apply (simp add:  homeomorphism_apply1 [OF hom])
+          apply (simp add: image_comp [symmetric])
+          using hom homeomorphism_apply1  apply (force simp: image_iff)
+          done
+      qed
+    qed
+  qed
+qed
+
 end
diff -r f3b905b2eee2 -r d85d88722745 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Oct 18 12:01:54 2016 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Oct 18 15:55:53 2016 +0100
@@ -960,7 +960,7 @@
         using dp p(1) mn d(2) by auto
     qed
   qed
-  then guess y unfolding convergent_eq_cauchy[symmetric] .. note y=this[THEN LIMSEQ_D]
+  then guess y unfolding convergent_eq_Cauchy[symmetric] .. note y=this[THEN LIMSEQ_D]
   show ?l
     unfolding integrable_on_def has_integral
   proof (rule_tac x=y in exI, clarify)
@@ -1798,7 +1798,7 @@
     qed
   qed
   then obtain s where s: "i \<longlonglongrightarrow> s"
-    using convergent_eq_cauchy[symmetric] by blast
+    using convergent_eq_Cauchy[symmetric] by blast
   show ?thesis
     unfolding integrable_on_def has_integral
   proof (rule_tac x=s in exI, clarify)
@@ -5437,7 +5437,7 @@
       apply auto
       done
   qed
-  from this[unfolded convergent_eq_cauchy[symmetric]] guess i ..
+  from this[unfolded convergent_eq_Cauchy[symmetric]] guess i ..
   note i = this[THEN LIMSEQ_D]
 
   show ?l unfolding integrable_on_def has_integral_alt'[of f]
diff -r f3b905b2eee2 -r d85d88722745 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Oct 18 12:01:54 2016 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Oct 18 15:55:53 2016 +0100
@@ -1034,6 +1034,14 @@
   shows "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e"
   by (simp add: dist_norm)
 
+lemma disjoint_ballI:
+  shows "dist x y \<ge> r+s \<Longrightarrow> ball x r \<inter> ball y s = {}"
+  using dist_triangle_less_add not_le by fastforce
+
+lemma disjoint_cballI:
+  shows "dist x y > r+s \<Longrightarrow> cball x r \<inter> cball y s = {}"
+  by (metis add_mono disjoint_iff_not_equal dist_triangle2 dual_order.trans leD mem_cball)
+
 lemma mem_sphere_0 [simp]:
   fixes x :: "'a::real_normed_vector"
   shows "x \<in> sphere 0 e \<longleftrightarrow> norm x = e"
@@ -5435,62 +5443,62 @@
 qed
 
 lemma complete_imp_closed:
-  fixes s :: "'a::metric_space set"
-  assumes "complete s"
-  shows "closed s"
+  fixes S :: "'a::metric_space set"
+  assumes "complete S"
+  shows "closed S"
 proof (unfold closed_sequential_limits, clarify)
-  fix f x assume "\<forall>n. f n \<in> s" and "f \<longlonglongrightarrow> x"
+  fix f x assume "\<forall>n. f n \<in> S" and "f \<longlonglongrightarrow> x"
   from \<open>f \<longlonglongrightarrow> x\<close> have "Cauchy f"
     by (rule LIMSEQ_imp_Cauchy)
-  with \<open>complete s\<close> and \<open>\<forall>n. f n \<in> s\<close> obtain l where "l \<in> s" and "f \<longlonglongrightarrow> l"
+  with \<open>complete S\<close> and \<open>\<forall>n. f n \<in> S\<close> obtain l where "l \<in> S" and "f \<longlonglongrightarrow> l"
     by (rule completeE)
   from \<open>f \<longlonglongrightarrow> x\<close> and \<open>f \<longlonglongrightarrow> l\<close> have "x = l"
     by (rule LIMSEQ_unique)
-  with \<open>l \<in> s\<close> show "x \<in> s"
+  with \<open>l \<in> S\<close> show "x \<in> S"
     by simp
 qed
 
 lemma complete_Int_closed:
-  fixes s :: "'a::metric_space set"
-  assumes "complete s" and "closed t"
-  shows "complete (s \<inter> t)"
+  fixes S :: "'a::metric_space set"
+  assumes "complete S" and "closed t"
+  shows "complete (S \<inter> t)"
 proof (rule completeI)
-  fix f assume "\<forall>n. f n \<in> s \<inter> t" and "Cauchy f"
-  then have "\<forall>n. f n \<in> s" and "\<forall>n. f n \<in> t"
+  fix f assume "\<forall>n. f n \<in> S \<inter> t" and "Cauchy f"
+  then have "\<forall>n. f n \<in> S" and "\<forall>n. f n \<in> t"
     by simp_all
-  from \<open>complete s\<close> obtain l where "l \<in> s" and "f \<longlonglongrightarrow> l"
-    using \<open>\<forall>n. f n \<in> s\<close> and \<open>Cauchy f\<close> by (rule completeE)
+  from \<open>complete S\<close> obtain l where "l \<in> S" and "f \<longlonglongrightarrow> l"
+    using \<open>\<forall>n. f n \<in> S\<close> and \<open>Cauchy f\<close> by (rule completeE)
   from \<open>closed t\<close> and \<open>\<forall>n. f n \<in> t\<close> and \<open>f \<longlonglongrightarrow> l\<close> have "l \<in> t"
     by (rule closed_sequentially)
-  with \<open>l \<in> s\<close> and \<open>f \<longlonglongrightarrow> l\<close> show "\<exists>l\<in>s \<inter> t. f \<longlonglongrightarrow> l"
+  with \<open>l \<in> S\<close> and \<open>f \<longlonglongrightarrow> l\<close> show "\<exists>l\<in>S \<inter> t. f \<longlonglongrightarrow> l"
     by fast
 qed
 
 lemma complete_closed_subset:
-  fixes s :: "'a::metric_space set"
-  assumes "closed s" and "s \<subseteq> t" and "complete t"
-  shows "complete s"
-  using assms complete_Int_closed [of t s] by (simp add: Int_absorb1)
+  fixes S :: "'a::metric_space set"
+  assumes "closed S" and "S \<subseteq> t" and "complete t"
+  shows "complete S"
+  using assms complete_Int_closed [of t S] by (simp add: Int_absorb1)
 
 lemma complete_eq_closed:
-  fixes s :: "('a::complete_space) set"
-  shows "complete s \<longleftrightarrow> closed s"
+  fixes S :: "('a::complete_space) set"
+  shows "complete S \<longleftrightarrow> closed S"
 proof
-  assume "closed s" then show "complete s"
+  assume "closed S" then show "complete S"
     using subset_UNIV complete_UNIV by (rule complete_closed_subset)
 next
-  assume "complete s" then show "closed s"
+  assume "complete S" then show "closed S"
     by (rule complete_imp_closed)
 qed
 
-lemma convergent_eq_cauchy:
-  fixes s :: "nat \<Rightarrow> 'a::complete_space"
-  shows "(\<exists>l. (s \<longlongrightarrow> l) sequentially) \<longleftrightarrow> Cauchy s"
+lemma convergent_eq_Cauchy:
+  fixes S :: "nat \<Rightarrow> 'a::complete_space"
+  shows "(\<exists>l. (S \<longlongrightarrow> l) sequentially) \<longleftrightarrow> Cauchy S"
   unfolding Cauchy_convergent_iff convergent_def ..
 
 lemma convergent_imp_bounded:
-  fixes s :: "nat \<Rightarrow> 'a::metric_space"
-  shows "(s \<longlongrightarrow> l) sequentially \<Longrightarrow> bounded (range s)"
+  fixes S :: "nat \<Rightarrow> 'a::metric_space"
+  shows "(S \<longlongrightarrow> l) sequentially \<Longrightarrow> bounded (range S)"
   by (intro cauchy_imp_bounded LIMSEQ_imp_Cauchy)
 
 lemma compact_cball[simp]:
@@ -5500,15 +5508,15 @@
   by blast
 
 lemma compact_frontier_bounded[intro]:
-  fixes s :: "'a::heine_borel set"
-  shows "bounded s \<Longrightarrow> compact (frontier s)"
+  fixes S :: "'a::heine_borel set"
+  shows "bounded S \<Longrightarrow> compact (frontier S)"
   unfolding frontier_def
   using compact_eq_bounded_closed
   by blast
 
 lemma compact_frontier[intro]:
-  fixes s :: "'a::heine_borel set"
-  shows "compact s \<Longrightarrow> compact (frontier s)"
+  fixes S :: "'a::heine_borel set"
+  shows "compact S \<Longrightarrow> compact (frontier S)"
   using compact_eq_bounded_closed compact_frontier_bounded
   by blast
 
@@ -5528,8 +5536,8 @@
 by (simp add: compact_imp_closed)
 
 lemma frontier_subset_compact:
-  fixes s :: "'a::heine_borel set"
-  shows "compact s \<Longrightarrow> frontier s \<subseteq> s"
+  fixes S :: "'a::heine_borel set"
+  shows "compact S \<Longrightarrow> frontier S \<subseteq> S"
   using frontier_subset_closed compact_eq_bounded_closed
   by blast
 
@@ -5723,7 +5731,7 @@
     apply auto
     done
   then obtain l where l: "\<forall>x. P x \<longrightarrow> ((\<lambda>n. s n x) \<longlongrightarrow> l x) sequentially"
-    unfolding convergent_eq_cauchy[symmetric]
+    unfolding convergent_eq_Cauchy[symmetric]
     using choice[of "\<lambda>x l. P x \<longrightarrow> ((\<lambda>n. s n x) \<longlongrightarrow> l) sequentially"]
     by auto
   {
@@ -6081,6 +6089,11 @@
     unfolding uniformly_continuous_on_def by blast
 qed
 
+lemma continuous_closed_imp_Cauchy_continuous:
+  fixes S :: "('a::complete_space) set"
+  shows "\<lbrakk>continuous_on S f; closed S; Cauchy \<sigma>; \<And>n. (\<sigma> n) \<in> S\<rbrakk> \<Longrightarrow> Cauchy(f o \<sigma>)"
+  apply (simp add: complete_eq_closed [symmetric] continuous_on_sequentially)
+  by (meson LIMSEQ_imp_Cauchy complete_def)
 
 text\<open>The usual transformation theorems.\<close>
 
@@ -6630,7 +6643,7 @@
 
   from uniformly_continuous_on_Cauchy[OF uc LIMSEQ_imp_Cauchy, OF xs]
   obtain l where l: "(\<lambda>n. f (xs n)) \<longlonglongrightarrow> l"
-    by atomize_elim (simp only: convergent_eq_cauchy)
+    by atomize_elim (simp only: convergent_eq_Cauchy)
 
   have "(f \<longlongrightarrow> l) (at x within X)"
   proof (safe intro!: Lim_within_LIMSEQ)
@@ -6641,7 +6654,7 @@
 
     from uniformly_continuous_on_Cauchy[OF uc LIMSEQ_imp_Cauchy, OF \<open>xs' \<longlonglongrightarrow> x\<close> \<open>xs' _ \<in> X\<close>]
     obtain l' where l': "(\<lambda>n. f (xs' n)) \<longlonglongrightarrow> l'"
-      by atomize_elim (simp only: convergent_eq_cauchy)
+      by atomize_elim (simp only: convergent_eq_Cauchy)
 
     show "(\<lambda>n. f (xs' n)) \<longlonglongrightarrow> l"
     proof (rule tendstoI)
diff -r f3b905b2eee2 -r d85d88722745 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Tue Oct 18 12:01:54 2016 +0200
+++ b/src/HOL/Limits.thy	Tue Oct 18 15:55:53 2016 +0100
@@ -2340,6 +2340,11 @@
 
 lemma isUCont_Cauchy: "isUCont f \<Longrightarrow> Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
   by (rule uniformly_continuous_on_Cauchy[where S=UNIV and f=f]) simp_all
+  
+lemma uniformly_continuous_imp_Cauchy_continuous:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+  shows "\<lbrakk>uniformly_continuous_on S f; Cauchy \<sigma>; \<And>n. (\<sigma> n) \<in> S\<rbrakk> \<Longrightarrow> Cauchy(f o \<sigma>)"
+  by (simp add: uniformly_continuous_on_def Cauchy_def) meson
 
 lemma (in bounded_linear) isUCont: "isUCont f"
   unfolding isUCont_def dist_norm
diff -r f3b905b2eee2 -r d85d88722745 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Tue Oct 18 12:01:54 2016 +0200
+++ b/src/HOL/Orderings.thy	Tue Oct 18 15:55:53 2016 +0100
@@ -1437,6 +1437,17 @@
 apply (erule Least_le)
 done
 
+lemma exists_least_iff: "(\<exists>n. P n) \<longleftrightarrow> (\<exists>n. P n \<and> (\<forall>m < n. \<not> P m))" (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+  assume ?rhs thus ?lhs by blast
+next
+  assume H: ?lhs then obtain n where n: "P n" by blast
+  let ?x = "Least P"
+  { fix m assume m: "m < ?x"
+    from not_less_Least[OF m] have "\<not> P m" . }
+  with LeastI_ex[OF H] show ?rhs by blast
+qed
+
 end