# HG changeset patch
# User wenzelm
# Date 1468574800 -7200
# Node ID 7f0e36eb73b4e956007e2c199353cc306eb55ee0
# Parent  d51a0a772094bf71ca220dec4648d08966055a21# Parent  b0f8845e349895e843530ce915e93a7c0911fefb
merged

diff -r b0f8845e3498 -r 7f0e36eb73b4 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Fri Jul 15 11:26:36 2016 +0200
+++ b/src/HOL/Library/Infinite_Set.thy	Fri Jul 15 11:26:40 2016 +0200
@@ -307,5 +307,36 @@
     unfolding bij_betw_def by (auto intro: enumerate_in_set)
 qed
 
+text\<open>A pair of weird and wonderful lemmas from HOL Light\<close>
+lemma finite_transitivity_chain:
+  assumes "finite A"
+      and R: "\<And>x. ~ R x x" "\<And>x y z. \<lbrakk>R x y; R y z\<rbrakk> \<Longrightarrow> R x z"
+      and A: "\<And>x. x \<in> A \<Longrightarrow> \<exists>y. y \<in> A \<and> R x y"
+  shows "A = {}"
+using \<open>finite A\<close> A
+proof (induction A)
+  case (insert a A)
+  with R show ?case
+    by (metis empty_iff insert_iff) 
+qed simp
+
+corollary Union_maximal_sets:
+  assumes "finite \<F>"
+    shows "\<Union>{T \<in> \<F>. \<forall>U\<in>\<F>. \<not> T \<subset> U} = \<Union>\<F>"
+    (is "?lhs = ?rhs")
+proof
+  show "?rhs \<subseteq> ?lhs"
+  proof (rule Union_subsetI)
+    fix S
+    assume "S \<in> \<F>"
+    have "{T \<in> \<F>. S \<subseteq> T} = {}" if "~ (\<exists>y. y \<in> {T \<in> \<F>. \<forall>U\<in>\<F>. \<not> T \<subset> U} \<and> S \<subseteq> y)"
+      apply (rule finite_transitivity_chain [of _ "\<lambda>T U. S \<subseteq> T \<and> T \<subset> U"])
+	 using assms that apply auto
+      by (blast intro: dual_order.trans psubset_imp_subset)
+    then show "\<exists>y. y \<in> {T \<in> \<F>. \<forall>U\<in>\<F>. \<not> T \<subset> U} \<and> S \<subseteq> y"
+      using \<open>S \<in> \<F>\<close> by blast
+  qed
+qed force
+
 end
 
diff -r b0f8845e3498 -r 7f0e36eb73b4 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Fri Jul 15 11:26:36 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Fri Jul 15 11:26:40 2016 +0200
@@ -2057,7 +2057,7 @@
 apply (auto simp: retraction_def intro: continuous_on_compose2)
 by blast
 
-lemma retract_of_trans:
+lemma retract_of_trans [trans]:
   assumes "s retract_of t" and "t retract_of u"
     shows "s retract_of u"
 using assms by (auto simp: retract_of_def intro: retraction_comp)
@@ -2200,6 +2200,227 @@
   using assms
   by (auto simp: retract_of_def retraction intro!: retraction_imp_quotient_map elim!: locally_path_connected_quotient_image)
 
+subsection\<open>Punctured affine hulls, etc.\<close>
+
+lemma continuous_on_compact_surface_projection_aux:
+  fixes S :: "'a::t2_space set"
+  assumes "compact S" "S \<subseteq> T" "image q T \<subseteq> S"
+      and contp: "continuous_on T p"
+      and "\<And>x. x \<in> S \<Longrightarrow> q x = x"
+      and [simp]: "\<And>x. x \<in> T \<Longrightarrow> q(p x) = q x"
+      and "\<And>x. x \<in> T \<Longrightarrow> p(q x) = p x"
+    shows "continuous_on T q"
+proof -
+  have *: "image p T = image p S"
+    using assms by auto (metis imageI subset_iff)
+  have contp': "continuous_on S p"
+    by (rule continuous_on_subset [OF contp \<open>S \<subseteq> T\<close>])
+  have "continuous_on T (q \<circ> p)"
+    apply (rule continuous_on_compose [OF contp])
+    apply (simp add: *)
+    apply (rule continuous_on_inv [OF contp' \<open>compact S\<close>])
+    using assms by auto
+  then show ?thesis
+    apply (rule continuous_on_eq [of _ "q o p"])
+    apply (simp add: o_def)
+    done
+qed
+
+lemma continuous_on_compact_surface_projection:
+  fixes S :: "'a::real_normed_vector set"
+  assumes "compact S"
+      and S: "S \<subseteq> V - {0}" and "cone V"
+      and iff: "\<And>x k. x \<in> V - {0} \<Longrightarrow> 0 < k \<and> (k *\<^sub>R x) \<in> S \<longleftrightarrow> d x = k"
+  shows "continuous_on (V - {0}) (\<lambda>x. d x *\<^sub>R x)"
+proof (rule continuous_on_compact_surface_projection_aux [OF \<open>compact S\<close> S])
+  show "(\<lambda>x. d x *\<^sub>R x) ` (V - {0}) \<subseteq> S"
+    using iff by auto
+  show "continuous_on (V - {0}) (\<lambda>x. inverse(norm x) *\<^sub>R x)"
+    by (intro continuous_intros) force
+  show "\<And>x. x \<in> S \<Longrightarrow> d x *\<^sub>R x = x"
+    by (metis S zero_less_one local.iff scaleR_one subset_eq)
+  show "d (x /\<^sub>R norm x) *\<^sub>R (x /\<^sub>R norm x) = d x *\<^sub>R x" if "x \<in> V - {0}" for x
+    using iff [of "inverse(norm x) *\<^sub>R x" "norm x * d x", symmetric] iff that \<open>cone V\<close>
+    by (simp add: field_simps cone_def zero_less_mult_iff)
+  show "d x *\<^sub>R x /\<^sub>R norm (d x *\<^sub>R x) = x /\<^sub>R norm x" if "x \<in> V - {0}" for x
+  proof -
+    have "0 < d x"
+      using local.iff that by blast
+    then show ?thesis
+      by simp
+  qed
+qed
+
+proposition rel_frontier_deformation_retract_of_punctured_convex:
+  fixes S :: "'a::euclidean_space set"
+  assumes "convex S" "convex T" "bounded S"
+      and arelS: "a \<in> rel_interior S"
+      and relS: "rel_frontier S \<subseteq> T"
+      and affS: "T \<subseteq> affine hull S"
+  obtains r where "homotopic_with (\<lambda>x. True) (T - {a}) (T - {a}) id r"
+                  "retraction (T - {a}) (rel_frontier S) r"
+proof -
+  have "\<exists>d. 0 < d \<and> (a + d *\<^sub>R l) \<in> rel_frontier S \<and>
+            (\<forall>e. 0 \<le> e \<and> e < d \<longrightarrow> (a + e *\<^sub>R l) \<in> rel_interior S)"
+       if "(a + l) \<in> affine hull S" "l \<noteq> 0" for l
+    apply (rule ray_to_rel_frontier [OF \<open>bounded S\<close> arelS])
+    apply (rule that)+
+    by metis
+  then obtain dd
+    where dd1: "\<And>l. \<lbrakk>(a + l) \<in> affine hull S; l \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < dd l \<and> (a + dd l *\<^sub>R l) \<in> rel_frontier S"
+      and dd2: "\<And>l e. \<lbrakk>(a + l) \<in> affine hull S; e < dd l; 0 \<le> e; l \<noteq> 0\<rbrakk>
+                      \<Longrightarrow> (a + e *\<^sub>R l) \<in> rel_interior S"
+    by metis+
+  have aaffS: "a \<in> affine hull S"
+    by (meson arelS subsetD hull_inc rel_interior_subset)
+  have "((\<lambda>z. z - a) ` (affine hull S - {a})) = ((\<lambda>z. z - a) ` (affine hull S)) - {0}"
+    by (auto simp: )
+  moreover have "continuous_on (((\<lambda>z. z - a) ` (affine hull S)) - {0}) (\<lambda>x. dd x *\<^sub>R x)"
+  proof (rule continuous_on_compact_surface_projection)
+    show "compact (rel_frontier ((\<lambda>z. z - a) ` S))"
+      by (simp add: \<open>bounded S\<close> bounded_translation_minus compact_rel_frontier_bounded)
+    have releq: "rel_frontier ((\<lambda>z. z - a) ` S) = (\<lambda>z. z - a) ` rel_frontier S"
+      using rel_frontier_translation [of "-a"] add.commute by simp
+    also have "... \<subseteq> (\<lambda>z. z - a) ` (affine hull S) - {0}"
+      using rel_frontier_affine_hull arelS rel_frontier_def by fastforce
+    finally show "rel_frontier ((\<lambda>z. z - a) ` S) \<subseteq> (\<lambda>z. z - a) ` (affine hull S) - {0}" .
+    show "cone ((\<lambda>z. z - a) ` (affine hull S))"
+      apply (rule subspace_imp_cone)
+      using aaffS
+      apply (simp add: subspace_affine image_comp o_def affine_translation_aux [of a])
+      done
+    show "(0 < k \<and> k *\<^sub>R x \<in> rel_frontier ((\<lambda>z. z - a) ` S)) \<longleftrightarrow> (dd x = k)"
+         if x: "x \<in> (\<lambda>z. z - a) ` (affine hull S) - {0}" for k x
+    proof
+      show "dd x = k \<Longrightarrow> 0 < k \<and> k *\<^sub>R x \<in> rel_frontier ((\<lambda>z. z - a) ` S)"
+      using dd1 [of x] that image_iff by (fastforce simp add: releq)
+    next
+      assume k: "0 < k \<and> k *\<^sub>R x \<in> rel_frontier ((\<lambda>z. z - a) ` S)"
+      have False if "dd x < k"
+      proof -
+        have "k \<noteq> 0" "a + k *\<^sub>R x \<in> closure S"
+          using k closure_translation [of "-a"]
+          by (auto simp: rel_frontier_def)
+        then have segsub: "open_segment a (a + k *\<^sub>R x) \<subseteq> rel_interior S"
+          by (metis rel_interior_closure_convex_segment [OF \<open>convex S\<close> arelS])
+        have "x \<noteq> 0" and xaffS: "a + x \<in> affine hull S"
+          using x by (auto simp: )
+        then have "0 < dd x" and inS: "a + dd x *\<^sub>R x \<in> rel_frontier S"
+          using dd1 by auto
+        moreover have "a + dd x *\<^sub>R x \<in> open_segment a (a + k *\<^sub>R x)"
+          using k \<open>x \<noteq> 0\<close> \<open>0 < dd x\<close>
+          apply (simp add: in_segment)
+          apply (rule_tac x = "dd x / k" in exI)
+          apply (simp add: field_simps that)
+          apply (simp add: vector_add_divide_simps algebra_simps)
+          apply (metis (no_types) \<open>k \<noteq> 0\<close> divide_inverse_commute inverse_eq_divide mult.left_commute right_inverse)
+          done
+        ultimately show ?thesis
+          using segsub by (auto simp add: rel_frontier_def)
+      qed
+      moreover have False if "k < dd x"
+        using x k that rel_frontier_def
+        by (fastforce simp: algebra_simps releq dest!: dd2)
+      ultimately show "dd x = k"
+        by fastforce
+    qed
+  qed
+  ultimately have *: "continuous_on ((\<lambda>z. z - a) ` (affine hull S - {a})) (\<lambda>x. dd x *\<^sub>R x)"
+    by auto
+  have "continuous_on (affine hull S - {a}) ((\<lambda>x. a + dd x *\<^sub>R x) \<circ> (\<lambda>z. z - a))"
+    by (intro * continuous_intros continuous_on_compose)
+  with affS have contdd: "continuous_on (T - {a}) ((\<lambda>x. a + dd x *\<^sub>R x) \<circ> (\<lambda>z. z - a))"
+    by (blast intro: continuous_on_subset elim: )
+  show ?thesis
+  proof
+    show "homotopic_with (\<lambda>x. True) (T - {a}) (T - {a}) id (\<lambda>x. a + dd (x - a) *\<^sub>R (x - a))"
+    proof (rule homotopic_with_linear)
+      show "continuous_on (T - {a}) id"
+        by (intro continuous_intros continuous_on_compose)
+      show "continuous_on (T - {a}) (\<lambda>x. a + dd (x - a) *\<^sub>R (x - a))"
+        using contdd by (simp add: o_def)
+      show "closed_segment (id x) (a + dd (x - a) *\<^sub>R (x - a)) \<subseteq> T - {a}"
+           if "x \<in> T - {a}" for x
+      proof (clarsimp simp: in_segment, intro conjI)
+        fix u::real assume u: "0 \<le> u" "u \<le> 1"
+        show "(1 - u) *\<^sub>R x + u *\<^sub>R (a + dd (x - a) *\<^sub>R (x - a)) \<in> T"
+          apply (rule convexD [OF \<open>convex T\<close>])
+          using that u apply (auto simp add: )
+          apply (metis add.commute affS dd1 diff_add_cancel eq_iff_diff_eq_0 relS subsetD)
+          done
+        have iff: "(1 - u) *\<^sub>R x + u *\<^sub>R (a + d *\<^sub>R (x - a)) = a \<longleftrightarrow>
+                  (1 - u + u * d) *\<^sub>R (x - a) = 0" for d
+          by (auto simp: algebra_simps)
+        have "x \<in> T" "x \<noteq> a" using that by auto
+        then have axa: "a + (x - a) \<in> affine hull S"
+           by (metis (no_types) add.commute affS diff_add_cancel set_rev_mp)
+        then have "\<not> dd (x - a) \<le> 0 \<and> a + dd (x - a) *\<^sub>R (x - a) \<in> rel_frontier S"
+          using \<open>x \<noteq> a\<close> dd1 by fastforce
+        with \<open>x \<noteq> a\<close> show "(1 - u) *\<^sub>R x + u *\<^sub>R (a + dd (x - a) *\<^sub>R (x - a)) \<noteq> a"
+          apply (auto simp: iff)
+          using less_eq_real_def mult_le_0_iff not_less u by fastforce
+      qed
+    qed
+    show "retraction (T - {a}) (rel_frontier S) (\<lambda>x. a + dd (x - a) *\<^sub>R (x - a))"
+    proof (simp add: retraction_def, intro conjI ballI)
+      show "rel_frontier S \<subseteq> T - {a}"
+        using arelS relS rel_frontier_def by fastforce
+      show "continuous_on (T - {a}) (\<lambda>x. a + dd (x - a) *\<^sub>R (x - a))"
+        using contdd by (simp add: o_def)
+      show "(\<lambda>x. a + dd (x - a) *\<^sub>R (x - a)) ` (T - {a}) \<subseteq> rel_frontier S"
+        apply (auto simp: rel_frontier_def)
+        apply (metis Diff_subset add.commute affS dd1 diff_add_cancel eq_iff_diff_eq_0 rel_frontier_def subset_iff)
+        by (metis DiffE add.commute affS dd1 diff_add_cancel eq_iff_diff_eq_0 rel_frontier_def rev_subsetD)
+      show "a + dd (x - a) *\<^sub>R (x - a) = x" if x: "x \<in> rel_frontier S" for x
+      proof -
+        have "x \<noteq> a"
+          using that arelS by (auto simp add: rel_frontier_def)
+        have False if "dd (x - a) < 1"
+        proof -
+          have "x \<in> closure S"
+            using x by (auto simp: rel_frontier_def)
+          then have segsub: "open_segment a x \<subseteq> rel_interior S"
+            by (metis rel_interior_closure_convex_segment [OF \<open>convex S\<close> arelS])
+          have  xaffS: "x \<in> affine hull S"
+            using affS relS x by auto
+          then have "0 < dd (x - a)" and inS: "a + dd (x - a) *\<^sub>R (x - a) \<in> rel_frontier S"
+            using dd1 by (auto simp add: \<open>x \<noteq> a\<close>)
+          moreover have "a + dd (x - a) *\<^sub>R (x - a) \<in> open_segment a x"
+            using  \<open>x \<noteq> a\<close> \<open>0 < dd (x - a)\<close>
+            apply (simp add: in_segment)
+            apply (rule_tac x = "dd (x - a)" in exI)
+            apply (simp add: algebra_simps that)
+            done
+          ultimately show ?thesis
+            using segsub by (auto simp add: rel_frontier_def)
+        qed
+        moreover have False if "1 < dd (x - a)"
+          using x that dd2 [of "x - a" 1] \<open>x \<noteq> a\<close> closure_affine_hull
+          by (auto simp: rel_frontier_def)
+        ultimately have "dd (x - a) = 1" --\<open>similar to another proof above\<close>
+          by fastforce
+        with that show ?thesis
+          by (simp add: rel_frontier_def)
+      qed
+    qed
+  qed
+qed
+
+corollary rel_frontier_retract_of_punctured_affine_hull:
+  fixes S :: "'a::euclidean_space set"
+  assumes "bounded S" "convex S" "a \<in> rel_interior S"
+    shows "rel_frontier S retract_of (affine hull S - {a})"
+apply (rule rel_frontier_deformation_retract_of_punctured_convex [of S "affine hull S" a])
+apply (auto simp add: affine_imp_convex rel_frontier_affine_hull retract_of_def assms)
+done
+
+corollary rel_boundary_retract_of_punctured_affine_hull:
+  fixes S :: "'a::euclidean_space set"
+  assumes "compact S" "convex S" "a \<in> rel_interior S"
+    shows "(S - rel_interior S) retract_of (affine hull S - {a})"
+by (metis assms closure_closed compact_eq_bounded_closed rel_frontier_def
+          rel_frontier_retract_of_punctured_affine_hull)
+
 subsection\<open>Borsuk-style characterization of separation\<close>
 
 lemma continuous_on_Borsuk_map:
@@ -3611,4 +3832,333 @@
   assumes "AR S" "AR T" shows "AR(S \<times> T)"
 using assms by (simp add: AR_ANR ANR_Times contractible_Times)
 
+
+lemma ENR_rel_frontier_convex:
+  fixes S :: "'a::euclidean_space set"
+  assumes "bounded S" "convex S"
+    shows "ENR(rel_frontier S)"
+proof (cases "S = {}")
+  case True then show ?thesis
+    by simp
+next
+  case False
+  with assms have "rel_interior S \<noteq> {}"
+    by (simp add: rel_interior_eq_empty)
+  then obtain a where a: "a \<in> rel_interior S"
+    by auto
+  have ahS: "affine hull S - {a} \<subseteq> {x. closest_point (affine hull S) x \<noteq> a}"
+    by (auto simp: closest_point_self)
+  have "rel_frontier S retract_of affine hull S - {a}"
+    by (simp add: assms a rel_frontier_retract_of_punctured_affine_hull)
+  also have "... retract_of {x. closest_point (affine hull S) x \<noteq> a}"
+    apply (simp add: retract_of_def retraction_def ahS)
+    apply (rule_tac x="closest_point (affine hull S)" in exI)
+    apply (auto simp add: False closest_point_self affine_imp_convex closest_point_in_set continuous_on_closest_point)
+    done
+  finally have "rel_frontier S retract_of {x. closest_point (affine hull S) x \<noteq> a}" .
+  moreover have "openin (subtopology euclidean UNIV) {x \<in> UNIV. closest_point (affine hull S) x \<in> - {a}}"
+    apply (rule continuous_openin_preimage_gen)
+    apply (auto simp add: False affine_imp_convex continuous_on_closest_point)
+    done
+  ultimately show ?thesis
+    apply (simp add: ENR_def)
+    apply (rule_tac x = "{x. x \<in> UNIV \<and>
+                             closest_point (affine hull S) x \<in> (- {a})}" in exI)
+    apply (simp add: open_openin)
+    done
+qed
+
+lemma ANR_rel_frontier_convex:
+                 fixes S :: "'a::euclidean_space set"
+  assumes "bounded S" "convex S"
+    shows "ANR(rel_frontier S)"
+by (simp add: ENR_imp_ANR ENR_rel_frontier_convex assms)
+
+(*UNUSED
+lemma ENR_Times:
+  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+  assumes "ENR S" "ENR T" shows "ENR(S \<times> T)"
+using assms apply (simp add: ENR_ANR ANR_Times)
+thm locally_compact_Times
+oops
+  SIMP_TAC[ENR_ANR; ANR_PCROSS; LOCALLY_COMPACT_PCROSS]);;
+*)
+
+subsection\<open>Borsuk homotopy extension theorem\<close>
+
+text\<open>It's only this late so we can use the concept of retraction,
+  saying that the domain sets or range set are ENRs.\<close>
+
+theorem Borsuk_homotopy_extension_homotopic:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes cloTS: "closedin (subtopology euclidean T) S"
+      and anr: "(ANR S \<and> ANR T) \<or> ANR U"
+      and contf: "continuous_on T f"
+      and "f ` T \<subseteq> U"
+      and "homotopic_with (\<lambda>x. True) S U f g"
+   obtains g' where "homotopic_with (\<lambda>x. True) T U f g'"
+                    "continuous_on T g'" "image g' T \<subseteq> U"
+                    "\<And>x. x \<in> S \<Longrightarrow> g' x = g x"
+proof -
+  have "S \<subseteq> T" using assms closedin_imp_subset by blast
+  obtain h where conth: "continuous_on ({0..1} \<times> S) h"
+             and him: "h ` ({0..1} \<times> S) \<subseteq> U"
+             and [simp]: "\<And>x. h(0, x) = f x" "\<And>x. h(1::real, x) = g x"
+       using assms by (auto simp: homotopic_with_def)
+  define h' where "h' \<equiv>  \<lambda>z. if snd z \<in> S then h z else (f o snd) z"
+  define B where "B \<equiv> {0::real} \<times> T \<union> {0..1} \<times> S"
+  have clo0T: "closedin (subtopology euclidean ({0..1} \<times> T)) ({0::real} \<times> T)"
+    by (simp add: closedin_subtopology_refl closedin_Times)
+  moreover have cloT1S: "closedin (subtopology euclidean ({0..1} \<times> T)) ({0..1} \<times> S)"
+    by (simp add: closedin_subtopology_refl closedin_Times assms)
+  ultimately have clo0TB:"closedin (subtopology euclidean ({0..1} \<times> T)) B"
+    by (auto simp: B_def)
+  have cloBS: "closedin (subtopology euclidean B) ({0..1} \<times> S)"
+    by (metis (no_types) Un_subset_iff B_def closedin_subset_trans [OF cloT1S] clo0TB closedin_imp_subset closedin_self)
+  moreover have cloBT: "closedin (subtopology euclidean B) ({0} \<times> T)"
+    using \<open>S \<subseteq> T\<close> closedin_subset_trans [OF clo0T]
+    by (metis B_def Un_upper1 clo0TB closedin_closed inf_le1)
+  moreover have "continuous_on ({0} \<times> T) (f \<circ> snd)"
+    apply (rule continuous_intros)+
+    apply (simp add: contf)
+    done
+  ultimately have conth': "continuous_on B h'"
+    apply (simp add: h'_def B_def Un_commute [of "{0} \<times> T"])
+    apply (auto intro!: continuous_on_cases_local conth)
+    done
+  have "image h' B \<subseteq> U"
+    using \<open>f ` T \<subseteq> U\<close> him by (auto simp: h'_def B_def)
+  obtain V k where "B \<subseteq> V" and opeTV: "openin (subtopology euclidean ({0..1} \<times> T)) V"
+               and contk: "continuous_on V k" and kim: "k ` V \<subseteq> U"
+               and keq: "\<And>x. x \<in> B \<Longrightarrow> k x = h' x"
+  using anr
+  proof
+    assume ST: "ANR S \<and> ANR T"
+    have eq: "({0} \<times> T \<inter> {0..1} \<times> S) = {0::real} \<times> S"
+      using \<open>S \<subseteq> T\<close> by auto
+    have "ANR B"
+      apply (simp add: B_def)
+      apply (rule ANR_closed_Un_local)
+          apply (metis cloBT B_def)
+         apply (metis Un_commute cloBS B_def)
+        apply (simp_all add: ANR_Times convex_imp_ANR ANR_singleton ST eq)
+      done
+    note Vk = that
+    have *: thesis if "openin (subtopology euclidean ({0..1::real} \<times> T)) V"
+                      "retraction V B r" for V r
+      using that
+      apply (clarsimp simp add: retraction_def)
+      apply (rule Vk [of V "h' o r"], assumption+)
+        apply (metis continuous_on_compose conth' continuous_on_subset) 
+      using \<open>h' ` B \<subseteq> U\<close> apply force+
+      done
+    show thesis
+        apply (rule ANR_imp_neighbourhood_retract [OF \<open>ANR B\<close> clo0TB])
+        apply (auto simp: ANR_Times ANR_singleton ST retract_of_def *)
+        done
+  next
+    assume "ANR U"
+    with ANR_imp_absolute_neighbourhood_extensor \<open>h' ` B \<subseteq> U\<close> clo0TB conth' that
+    show ?thesis by blast
+  qed
+  define S' where "S' \<equiv> {x. \<exists>u::real. u \<in> {0..1} \<and> (u, x::'a) \<in> {0..1} \<times> T - V}"
+  have "closedin (subtopology euclidean T) S'"
+    unfolding S'_def
+    apply (rule closedin_compact_projection, blast)
+    using closedin_self opeTV by blast
+  have S'_def: "S' = {x. \<exists>u::real.  (u, x::'a) \<in> {0..1} \<times> T - V}"
+    by (auto simp: S'_def)
+  have cloTS': "closedin (subtopology euclidean T) S'"
+    using S'_def \<open>closedin (subtopology euclidean T) S'\<close> by blast
+  have "S \<inter> S' = {}"
+    using S'_def B_def \<open>B \<subseteq> V\<close> by force
+  obtain a :: "'a \<Rightarrow> real" where conta: "continuous_on T a"
+      and "\<And>x. x \<in> T \<Longrightarrow> a x \<in> closed_segment 1 0"
+      and a1: "\<And>x. x \<in> S \<Longrightarrow> a x = 1"
+      and a0: "\<And>x. x \<in> S' \<Longrightarrow> a x = 0"
+    apply (rule Urysohn_local [OF cloTS cloTS' \<open>S \<inter> S' = {}\<close>, of 1 0], blast)
+    done
+  then have ain: "\<And>x. x \<in> T \<Longrightarrow> a x \<in> {0..1}"
+    using closed_segment_eq_real_ivl by auto
+  have inV: "(u * a t, t) \<in> V" if "t \<in> T" "0 \<le> u" "u \<le> 1" for t u
+  proof (rule ccontr)
+    assume "(u * a t, t) \<notin> V"
+    with ain [OF \<open>t \<in> T\<close>] have "a t = 0"
+      apply simp
+      apply (rule a0)
+      by (metis (no_types, lifting) Diff_iff S'_def SigmaI atLeastAtMost_iff mem_Collect_eq mult_le_one mult_nonneg_nonneg that)
+    show False
+      using B_def \<open>(u * a t, t) \<notin> V\<close> \<open>B \<subseteq> V\<close> \<open>a t = 0\<close> that by auto
+  qed
+  show ?thesis
+  proof
+    show hom: "homotopic_with (\<lambda>x. True) T U f (\<lambda>x. k (a x, x))"
+    proof (simp add: homotopic_with, intro exI conjI)
+      show "continuous_on ({0..1} \<times> T) (k \<circ> (\<lambda>z. (fst z *\<^sub>R (a \<circ> snd) z, snd z)))"
+        apply (intro continuous_on_compose continuous_intros)
+        apply (rule continuous_on_subset [OF conta], force)
+        apply (rule continuous_on_subset [OF contk])
+        apply (force intro: inV)
+        done
+      show "(k \<circ> (\<lambda>z. (fst z *\<^sub>R (a \<circ> snd) z, snd z))) ` ({0..1} \<times> T) \<subseteq> U"
+        using inV kim by auto
+      show "\<forall>x\<in>T. (k \<circ> (\<lambda>z. (fst z *\<^sub>R (a \<circ> snd) z, snd z))) (0, x) = f x"
+        by (simp add: B_def h'_def keq)
+      show "\<forall>x\<in>T. (k \<circ> (\<lambda>z. (fst z *\<^sub>R (a \<circ> snd) z, snd z))) (1, x) = k (a x, x)"
+        by auto
+    qed
+  show "continuous_on T (\<lambda>x. k (a x, x))"
+    using hom homotopic_with_imp_continuous by blast
+  show "(\<lambda>x. k (a x, x)) ` T \<subseteq> U"
+  proof clarify
+    fix t
+    assume "t \<in> T"
+    show "k (a t, t) \<in> U"
+      by (metis \<open>t \<in> T\<close> image_subset_iff inV kim not_one_le_zero linear mult_cancel_right1)
+  qed
+  show "\<And>x. x \<in> S \<Longrightarrow> k (a x, x) = g x"
+    by (simp add: B_def a1 h'_def keq)
+  qed
+qed
+
+
+corollary nullhomotopic_into_ANR_extension:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "closed S"
+      and contf: "continuous_on S f"
+      and "ANR T"
+      and fim: "f ` S \<subseteq> T"
+      and "S \<noteq> {}"
+   shows "(\<exists>c. homotopic_with (\<lambda>x. True) S T f (\<lambda>x. c)) \<longleftrightarrow>
+          (\<exists>g. continuous_on UNIV g \<and> range g \<subseteq> T \<and> (\<forall>x \<in> S. g x = f x))"
+       (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then obtain c where c: "homotopic_with (\<lambda>x. True) S T (\<lambda>x. c) f"
+    by (blast intro: homotopic_with_symD elim: )
+  have "closedin (subtopology euclidean UNIV) S"
+    using \<open>closed S\<close> closed_closedin by fastforce
+  then obtain g where "continuous_on UNIV g" "range g \<subseteq> T"
+                      "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+    apply (rule Borsuk_homotopy_extension_homotopic [OF _ _ continuous_on_const _ c, where T=UNIV])
+    using \<open>ANR T\<close> \<open>S \<noteq> {}\<close> c homotopic_with_imp_subset1 apply fastforce+
+    done
+  then show ?rhs by blast
+next
+  assume ?rhs
+  then obtain g where "continuous_on UNIV g" "range g \<subseteq> T" "\<And>x. x\<in>S \<Longrightarrow> g x = f x"
+    by blast
+  then obtain c where "homotopic_with (\<lambda>h. True) UNIV T g (\<lambda>x. c)"
+    using nullhomotopic_from_contractible [of UNIV g T] contractible_UNIV by blast
+  then show ?lhs
+    apply (rule_tac x="c" in exI)
+    apply (rule homotopic_with_eq [of _ _ _ g "\<lambda>x. c"])
+    apply (rule homotopic_with_subset_left)
+    apply (auto simp add: \<open>\<And>x. x \<in> S \<Longrightarrow> g x = f x\<close>)
+    done
+qed
+
+corollary nullhomotopic_into_rel_frontier_extension:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "closed S"
+      and contf: "continuous_on S f"
+      and "convex T" "bounded T"
+      and fim: "f ` S \<subseteq> rel_frontier T"
+      and "S \<noteq> {}"
+   shows "(\<exists>c. homotopic_with (\<lambda>x. True) S (rel_frontier T) f (\<lambda>x. c)) \<longleftrightarrow>
+          (\<exists>g. continuous_on UNIV g \<and> range g \<subseteq> rel_frontier T \<and> (\<forall>x \<in> S. g x = f x))"
+by (simp add: nullhomotopic_into_ANR_extension assms ANR_rel_frontier_convex)
+
+corollary nullhomotopic_into_sphere_extension:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b :: euclidean_space"
+  assumes "closed S" and contf: "continuous_on S f"
+      and "S \<noteq> {}" and fim: "f ` S \<subseteq> sphere a r"
+    shows "((\<exists>c. homotopic_with (\<lambda>x. True) S (sphere a r) f (\<lambda>x. c)) \<longleftrightarrow>
+           (\<exists>g. continuous_on UNIV g \<and> range g \<subseteq> sphere a r \<and> (\<forall>x \<in> S. g x = f x)))"
+           (is "?lhs = ?rhs")
+proof (cases "r = 0")
+  case True with fim show ?thesis
+    apply (auto simp: )
+    using fim continuous_on_const apply fastforce
+    by (metis contf contractible_sing nullhomotopic_into_contractible)
+next
+  case False
+  then have eq: "sphere a r = rel_frontier (cball a r)" by simp
+  show ?thesis
+    using fim unfolding eq
+    apply (rule nullhomotopic_into_rel_frontier_extension [OF \<open>closed S\<close> contf convex_cball bounded_cball])
+    apply (rule \<open>S \<noteq> {}\<close>)
+    done
+qed
+
+proposition Borsuk_map_essential_bounded_component:
+  fixes a :: "'a :: euclidean_space"
+  assumes "compact S" and "a \<notin> S"
+   shows "bounded (connected_component_set (- S) a) \<longleftrightarrow>
+          ~(\<exists>c. homotopic_with (\<lambda>x. True) S (sphere 0 1)
+                               (\<lambda>x. inverse(norm(x - a)) *\<^sub>R (x - a)) (\<lambda>x. c))"
+   (is "?lhs = ?rhs")
+proof (cases "S = {}")
+  case True then show ?thesis
+    by simp
+next
+  case False
+  have "closed S" "bounded S"
+    using \<open>compact S\<close> compact_eq_bounded_closed by auto
+  have s01: "(\<lambda>x. (x - a) /\<^sub>R norm (x - a)) ` S \<subseteq> sphere 0 1"
+    using \<open>a \<notin> S\<close>  by clarsimp (metis dist_eq_0_iff dist_norm mult.commute right_inverse)
+  have aincc: "a \<in> connected_component_set (- S) a"
+    by (simp add: \<open>a \<notin> S\<close>)
+  obtain r where "r>0" and r: "S \<subseteq> ball 0 r"
+    using bounded_subset_ballD \<open>bounded S\<close> by blast
+  have "~ ?rhs \<longleftrightarrow> ~ ?lhs"
+  proof
+    assume notr: "~ ?rhs"
+    have nog: "~ (\<exists>g. continuous_on (S \<union> connected_component_set (- S) a) g \<and>
+                   g ` (S \<union> connected_component_set (- S) a) \<subseteq> sphere 0 1 \<and>
+                   (\<forall>x\<in>S. g x = (x - a) /\<^sub>R norm (x - a)))"
+         if "bounded (connected_component_set (- S) a)"
+      apply (rule non_extensible_Borsuk_map [OF \<open>compact S\<close> componentsI _ aincc])
+      using  \<open>a \<notin> S\<close> that by auto
+    obtain g where "range g \<subseteq> sphere 0 1" "continuous_on UNIV g"
+                        "\<And>x. x \<in> S \<Longrightarrow> g x = (x - a) /\<^sub>R norm (x - a)"
+      using notr
+      by (auto simp add: nullhomotopic_into_sphere_extension
+                 [OF \<open>closed S\<close> continuous_on_Borsuk_map [OF \<open>a \<notin> S\<close>] False s01])
+    with \<open>a \<notin> S\<close> show  "~ ?lhs"
+      apply (clarsimp simp: Borsuk_map_into_sphere [of a S, symmetric] dest!: nog)
+      apply (drule_tac x="g" in spec)
+      using continuous_on_subset by fastforce 
+  next
+    assume "~ ?lhs"
+    then obtain b where b: "b \<in> connected_component_set (- S) a" and "r \<le> norm b"
+      using bounded_iff linear by blast
+    then have bnot: "b \<notin> ball 0 r"
+      by simp
+    have "homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. (x - a) /\<^sub>R norm (x - a))
+                                                   (\<lambda>x. (x - b) /\<^sub>R norm (x - b))"
+      apply (rule Borsuk_maps_homotopic_in_path_component)
+      using \<open>closed S\<close> b open_Compl open_path_connected_component apply fastforce
+      done
+    moreover
+    obtain c where "homotopic_with (\<lambda>x. True) (ball 0 r) (sphere 0 1)
+                                   (\<lambda>x. inverse (norm (x - b)) *\<^sub>R (x - b)) (\<lambda>x. c)"
+    proof (rule nullhomotopic_from_contractible)
+      show "contractible (ball (0::'a) r)"
+        by (metis convex_imp_contractible convex_ball)
+      show "continuous_on (ball 0 r) (\<lambda>x. inverse(norm (x - b)) *\<^sub>R (x - b))"
+        by (rule continuous_on_Borsuk_map [OF bnot])
+      show "(\<lambda>x. (x - b) /\<^sub>R norm (x - b)) ` ball 0 r \<subseteq> sphere 0 1"
+        using bnot Borsuk_map_into_sphere by blast
+    qed blast
+    ultimately have "homotopic_with (\<lambda>x. True) S (sphere 0 1)
+                         (\<lambda>x. (x - a) /\<^sub>R norm (x - a)) (\<lambda>x. c)"
+      by (meson homotopic_with_subset_left homotopic_with_trans r)
+    then show "~ ?rhs"
+      by blast
+  qed
+  then show ?thesis by blast
+qed
+
+
 end
diff -r b0f8845e3498 -r 7f0e36eb73b4 src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Fri Jul 15 11:26:36 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Fri Jul 15 11:26:40 2016 +0200
@@ -2551,8 +2551,8 @@
   then have "cos (Arcsin z) \<noteq> 0"
     by (metis diff_0_right power_zero_numeral sin_squared_eq)
   then show ?thesis
-    apply (rule has_complex_derivative_inverse_basic [OF DERIV_sin])
-    apply (auto intro: isCont_Arcsin open_ball [of z 1] assms)
+    apply (rule has_complex_derivative_inverse_basic [OF DERIV_sin _ _ open_ball [of z 1]])
+    apply (auto intro: isCont_Arcsin assms)
     done
 qed
 
@@ -2716,8 +2716,8 @@
   then have "- sin (Arccos z) \<noteq> 0"
     by (metis cos_squared_eq diff_0_right mult_zero_left neg_0_equal_iff_equal power2_eq_square)
   then have "(Arccos has_field_derivative inverse(- sin(Arccos z))) (at z)"
-    apply (rule has_complex_derivative_inverse_basic [OF DERIV_cos])
-    apply (auto intro: isCont_Arccos open_ball [of z 1] assms)
+    apply (rule has_complex_derivative_inverse_basic [OF DERIV_cos _ _ open_ball [of z 1]])
+    apply (auto intro: isCont_Arccos assms)
     done
   then show ?thesis
     by simp
diff -r b0f8845e3498 -r 7f0e36eb73b4 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Jul 15 11:26:36 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Jul 15 11:26:40 2016 +0200
@@ -7912,6 +7912,11 @@
     shows "rel_frontier {a} = {}"
   by (simp add: rel_frontier_def)
 
+lemma rel_frontier_affine_hull:
+  fixes S :: "'a::euclidean_space set"
+  shows "rel_frontier S \<subseteq> affine hull S"
+using closure_affine_hull rel_frontier_def by fastforce
+
 lemma rel_frontier_cball [simp]:
     fixes a :: "'n::euclidean_space"
     shows "rel_frontier(cball a r) = (if r = 0 then {} else sphere a r)"
@@ -12246,6 +12251,67 @@
   with assms show ?thesis by auto
 qed
 
+proposition dim_orthogonal_sum:
+  fixes A :: "'a::euclidean_space set"
+  assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
+    shows "dim(A \<union> B) = dim A + dim B"
+proof -
+  have 1: "\<And>x y. \<lbrakk>x \<in> span A; y \<in> B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
+    by (erule span_induct [OF _ subspace_hyperplane2]; simp add: assms)
+  have "\<And>x y. \<lbrakk>x \<in> span A; y \<in> span B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
+    apply (erule span_induct [OF _ subspace_hyperplane])
+    using 1 by (simp add: )
+  then have 0: "\<And>x y. \<lbrakk>x \<in> span A; y \<in> span B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
+    by simp
+  have "dim(A \<union> B) = dim (span (A \<union> B))"
+    by simp
+  also have "... = dim ((\<lambda>(a, b). a + b) ` (span A \<times> span B))"
+    by (simp add: span_Un)
+  also have "... = dim {x + y |x y. x \<in> span A \<and> y \<in> span B}"
+    by (auto intro!: arg_cong [where f=dim])
+  also have "... = dim {x + y |x y. x \<in> span A \<and> y \<in> span B} + dim(span A \<inter> span B)"
+    by (auto simp: dest: 0)
+  also have "... = dim (span A) + dim (span B)"
+    by (rule dim_sums_Int) auto
+  also have "... = dim A + dim B"
+    by simp
+  finally show ?thesis .
+qed
+
+lemma dim_subspace_orthogonal_to_vectors:
+  fixes A :: "'a::euclidean_space set"
+  assumes "subspace A" "subspace B" "A \<subseteq> B"
+    shows "dim {y \<in> B. \<forall>x \<in> A. orthogonal x y} + dim A = dim B"
+proof -
+  have "dim (span ({y \<in> B. \<forall>x\<in>A. orthogonal x y} \<union> A)) = dim (span B)"
+  proof (rule arg_cong [where f=dim, OF subset_antisym])
+    show "span ({y \<in> B. \<forall>x\<in>A. orthogonal x y} \<union> A) \<subseteq> span B"
+      by (simp add: \<open>A \<subseteq> B\<close> Collect_restrict span_mono)
+  next
+    have *: "x \<in> span ({y \<in> B. \<forall>x\<in>A. orthogonal x y} \<union> A)"
+         if "x \<in> B" for x
+    proof -
+      obtain y z where "x = y + z" "y \<in> span A" and orth: "\<And>w. w \<in> span A \<Longrightarrow> orthogonal z w"
+        using orthogonal_subspace_decomp_exists [of A x] that by auto
+      have "y \<in> span B"
+        by (metis span_eq \<open>y \<in> span A\<close> assms subset_iff)
+      then have "z \<in> {a \<in> B. \<forall>x. x \<in> A \<longrightarrow> orthogonal x a}"
+        by simp (metis (no_types) span_eq \<open>x = y + z\<close> \<open>subspace A\<close> \<open>subspace B\<close> orth orthogonal_commute span_add_eq that)
+      then have z: "z \<in> span {y \<in> B. \<forall>x\<in>A. orthogonal x y}"
+        by (meson span_inc subset_iff)
+      then show ?thesis
+        apply (simp add: span_Un image_def)
+        apply (rule bexI [OF _ z])
+        apply (simp add: \<open>x = y + z\<close> \<open>y \<in> span A\<close>)
+        done
+    qed
+    show "span B \<subseteq> span ({y \<in> B. \<forall>x\<in>A. orthogonal x y} \<union> A)"
+      by (rule span_minimal) (auto intro: * span_minimal elim: )
+  qed
+  then show ?thesis
+    by (metis (no_types, lifting) dim_orthogonal_sum dim_span mem_Collect_eq orthogonal_commute orthogonal_def)
+qed
+
 subsection\<open>Parallel slices, etc.\<close>
 
 text\<open> If we take a slice out of a set, we can do it perpendicularly,
diff -r b0f8845e3498 -r 7f0e36eb73b4 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Jul 15 11:26:36 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri Jul 15 11:26:40 2016 +0200
@@ -5328,12 +5328,12 @@
   shows "negligible (s - t)"
   using assms by auto
 
-lemma negligible_inter:
+lemma negligible_Int:
   assumes "negligible s \<or> negligible t"
   shows "negligible (s \<inter> t)"
   using assms by auto
 
-lemma negligible_union:
+lemma negligible_Un:
   assumes "negligible s"
     and "negligible t"
   shows "negligible (s \<union> t)"
@@ -5350,15 +5350,15 @@
     done
 qed
 
-lemma negligible_union_eq[simp]: "negligible (s \<union> t) \<longleftrightarrow> negligible s \<and> negligible t"
-  using negligible_union by auto
+lemma negligible_Un_eq[simp]: "negligible (s \<union> t) \<longleftrightarrow> negligible s \<and> negligible t"
+  using negligible_Un by auto
 
 lemma negligible_sing[intro]: "negligible {a::'a::euclidean_space}"
   using negligible_standard_hyperplane[OF SOME_Basis, of "a \<bullet> (SOME i. i \<in> Basis)"] by auto
 
 lemma negligible_insert[simp]: "negligible (insert a s) \<longleftrightarrow> negligible s"
   apply (subst insert_is_Un)
-  unfolding negligible_union_eq
+  unfolding negligible_Un_eq
   apply auto
   done
 
@@ -6803,7 +6803,6 @@
   apply auto
   done
 
-
 subsection \<open>even more special cases.\<close>
 
 lemma uminus_interval_vector[simp]:
@@ -8394,6 +8393,33 @@
   qed
 qed auto
 
+lemma negligible_translation:
+  assumes "negligible S"
+    shows "negligible (op + c ` S)"
+proof -
+  have inj: "inj (op + c)"
+    by simp
+  show ?thesis
+  using assms
+  proof (clarsimp simp: negligible_def)
+    fix a b
+    assume "\<forall>x y. (indicator S has_integral 0) (cbox x y)"
+    then have *: "(indicator S has_integral 0) (cbox (a-c) (b-c))"
+      by (meson Diff_iff assms has_integral_negligible indicator_simps(2))
+    have eq: "indicator (op + c ` S) = (\<lambda>x. indicator S (x - c))"
+      by (force simp add: indicator_def)
+    show "(indicator (op + c ` S) has_integral 0) (cbox a b)"
+      using has_integral_affinity [OF *, of 1 "-c"]
+            cbox_translation [of "c" "-c+a" "-c+b"]
+      by (simp add: eq add.commute)
+  qed
+qed
+
+lemma negligible_translation_rev:
+  assumes "negligible (op + c ` S)"
+    shows "negligible S"
+by (metis negligible_translation [OF assms, of "-c"] translation_galois)
+
 lemma has_integral_spike_set_eq:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   assumes "negligible ((s - t) \<union> (t - s))"
@@ -9065,7 +9091,7 @@
       unfolding obt interior_cbox
       apply -
       apply (rule negligible_subset[of "(cbox a b-box a b) \<union> (cbox c d-box c d)"])
-      apply (rule negligible_union negligible_frontier_interval)+
+      apply (rule negligible_Un negligible_frontier_interval)+
       apply auto
       done
   qed
diff -r b0f8845e3498 -r 7f0e36eb73b4 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Jul 15 11:26:36 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Jul 15 11:26:40 2016 +0200
@@ -819,7 +819,7 @@
   apply (auto simp add: istopology_def)
   done
 
-lemma topspace_euclidean: "topspace euclidean = UNIV"
+lemma topspace_euclidean [simp]: "topspace euclidean = UNIV"
   apply (simp add: topspace_def)
   apply (rule set_eqI)
   apply (auto simp add: open_openin[symmetric])