# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1464014004 -3600
# Node ID 27afe7af737945931f9f387a72cc803b540f468e
# Parent  932cf444f2fe6d661d3cae3b5d7dfd342f2c88ca
Lots of new material for multivariate analysis

diff -r 932cf444f2fe -r 27afe7af7379 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Sat May 21 07:08:59 2016 +0200
+++ b/src/HOL/Complex.thy	Mon May 23 15:33:24 2016 +0100
@@ -799,9 +799,15 @@
 lemma exp_pi_i [simp]: "exp(of_real pi * ii) = -1"
   by (metis cis_conv_exp cis_pi mult.commute)
 
+lemma exp_pi_i' [simp]: "exp(ii * of_real pi) = -1"
+  using cis_conv_exp cis_pi by auto
+
 lemma exp_two_pi_i [simp]: "exp(2 * of_real pi * ii) = 1"
   by (simp add: exp_eq_polar complex_eq_iff)
 
+lemma exp_two_pi_i' [simp]: "exp (\<i> * (of_real pi * 2)) = 1"
+  by (metis exp_two_pi_i mult.commute)
+
 subsubsection \<open>Complex argument\<close>
 
 definition arg :: "complex \<Rightarrow> real" where
diff -r 932cf444f2fe -r 27afe7af7379 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sat May 21 07:08:59 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon May 23 15:33:24 2016 +0100
@@ -1,9 +1,8 @@
 (*  Title:      HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
-    Author:     Robert Himmelmann, TU Muenchen
-    Author:     Bogdan Grechuk, University of Edinburgh
+    Authors: Robert Himmelmann, TU Muenchen; Bogdan Grechuk, University of Edinburgh; LCP
 *)
 
-section \<open>Convex sets, functions and related things.\<close>
+section \<open>Convex sets, functions and related things\<close>
 
 theory Convex_Euclidean_Space
 imports
@@ -70,7 +69,7 @@
   also have "\<dots> \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y \<in> S. f (x - y) = 0 \<longrightarrow> x - y = 0)"
     by (simp add: linear_sub[OF lf])
   also have "\<dots> \<longleftrightarrow> (\<forall>x \<in> S. f x = 0 \<longrightarrow> x = 0)"
-    using \<open>subspace S\<close> subspace_def[of S] subspace_sub[of S] by auto
+    using \<open>subspace S\<close> subspace_def[of S] subspace_diff[of S] by auto
   finally show ?thesis .
 qed
 
@@ -426,6 +425,12 @@
 lemma affine_Int[intro]: "affine s \<Longrightarrow> affine t \<Longrightarrow> affine (s \<inter> t)"
   unfolding affine_def by auto
 
+lemma affine_scaling: "affine s \<Longrightarrow> affine (image (\<lambda>x. c *\<^sub>R x) s)"
+  apply (clarsimp simp add: affine_def)
+  apply (rule_tac x="u *\<^sub>R x + v *\<^sub>R y" in image_eqI)
+  apply (auto simp: algebra_simps)
+  done
+
 lemma affine_affine_hull [simp]: "affine(affine hull s)"
   unfolding hull_def
   using affine_Inter[of "{t. affine t \<and> s \<subseteq> t}"] by auto
@@ -2915,11 +2920,16 @@
 
 lemma aff_dim_subspace:
   fixes S :: "'n::euclidean_space set"
-  assumes "S \<noteq> {}"
-    and "subspace S"
+  assumes "subspace S"
   shows "aff_dim S = int (dim S)"
-  using aff_dim_affine[of S S] assms subspace_imp_affine[of S] affine_parallel_reflex[of S]
-  by auto
+proof (cases "S={}")
+  case True with assms show ?thesis
+    by (simp add: subspace_affine)
+next
+  case False
+  with aff_dim_affine[of S S] assms subspace_imp_affine[of S] affine_parallel_reflex[of S] subspace_affine
+  show ?thesis by auto
+qed
 
 lemma aff_dim_zero:
   fixes S :: "'n::euclidean_space set"
@@ -2964,6 +2974,41 @@
   then show ?thesis by auto
 qed
 
+lemma affine_independent_card_dim_diffs:
+  fixes S :: "'a :: euclidean_space set"
+  assumes "~ affine_dependent S" "a \<in> S"
+    shows "card S = dim {x - a|x. x \<in> S} + 1"
+proof -
+  have 1: "{b - a|b. b \<in> (S - {a})} \<subseteq> {x - a|x. x \<in> S}" by auto
+  have 2: "x - a \<in> span {b - a |b. b \<in> S - {a}}" if "x \<in> S" for x
+  proof (cases "x = a")
+    case True then show ?thesis by simp
+  next
+    case False then show ?thesis
+      using assms by (blast intro: span_superset that)
+  qed
+  have "\<not> affine_dependent (insert a S)"
+    by (simp add: assms insert_absorb)
+  then have 3: "independent {b - a |b. b \<in> S - {a}}"
+      using dependent_imp_affine_dependent by fastforce
+  have "{b - a |b. b \<in> S - {a}} = (\<lambda>b. b-a) ` (S - {a})"
+    by blast
+  then have "card {b - a |b. b \<in> S - {a}} = card ((\<lambda>b. b-a) ` (S - {a}))"
+    by simp
+  also have "... = card (S - {a})"
+    by (metis (no_types, lifting) card_image diff_add_cancel inj_onI)
+  also have "... = card S - 1"
+    by (simp add: aff_independent_finite assms)
+  finally have 4: "card {b - a |b. b \<in> S - {a}} = card S - 1" .
+  have "finite S"
+    by (meson assms aff_independent_finite)
+  with \<open>a \<in> S\<close> have "card S \<noteq> 0" by auto
+  moreover have "dim {x - a |x. x \<in> S} = card S - 1"
+    using 2 by (blast intro: dim_unique [OF 1 _ 3 4])
+  ultimately show ?thesis
+    by auto
+qed
+
 lemma independent_card_le_aff_dim:
   fixes B :: "'n::euclidean_space set"
   assumes "B \<subseteq> V"
@@ -3361,11 +3406,11 @@
 lemma affine_hull_sing [simp]: "affine hull {a :: 'n::euclidean_space} = {a}"
   by (metis affine_hull_eq affine_sing)
 
-lemma rel_interior_sing [simp]: "rel_interior {a :: 'n::euclidean_space} = {a}"
-  unfolding rel_interior_ball affine_hull_sing
-  apply auto
-  apply (rule_tac x = "1 :: real" in exI)
-  apply simp
+lemma rel_interior_sing [simp]:
+    fixes a :: "'n::euclidean_space"  shows "rel_interior {a} = {a}"
+  apply (auto simp: rel_interior_ball)
+  apply (rule_tac x=1 in exI)
+  apply force
   done
 
 lemma subset_rel_interior:
@@ -3671,7 +3716,7 @@
   ultimately show ?thesis by auto
 qed
 
-lemma closure_aff_dim:
+lemma closure_aff_dim [simp]:
   fixes S :: "'n::euclidean_space set"
   shows "aff_dim (closure S) = aff_dim S"
 proof -
@@ -3911,7 +3956,7 @@
       moreover have "f x - f xy = f (x - xy)"
         using assms linear_sub[of f x xy] linear_conv_bounded_linear[of f] by auto
       moreover have *: "x - xy \<in> span S"
-        using subspace_sub[of "span S" x xy] subspace_span \<open>x \<in> S\<close> xy
+        using subspace_diff[of "span S" x xy] subspace_span \<open>x \<in> S\<close> xy
           affine_hull_subset_span[of S] span_inc
         by auto
       moreover from * have "e1 * norm (x - xy) \<le> norm (f (x - xy))"
@@ -6570,6 +6615,17 @@
     "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> open_segment (f a) (f b) = f ` (open_segment a b)"
   by (force simp: open_segment_def closed_segment_linear_image inj_on_def)
 
+lemma closed_segment_translation:
+    "closed_segment (c + a) (c + b) = image (\<lambda>x. c + x) (closed_segment a b)"
+apply safe
+apply (rule_tac x="x-c" in image_eqI)
+apply (auto simp: in_segment algebra_simps)
+done
+
+lemma open_segment_translation:
+    "open_segment (c + a) (c + b) = image (\<lambda>x. c + x) (open_segment a b)"
+by (simp add: open_segment_def closed_segment_translation translation_diff)
+
 lemma open_segment_PairD:
     "(x, x') \<in> open_segment (a, a') (b, b')
      \<Longrightarrow> (x \<in> open_segment a b \<or> a = b) \<and> (x' \<in> open_segment a' b' \<or> a' = b')"
@@ -6782,6 +6838,118 @@
   fixes u::real shows "closed_segment u v = (\<lambda>x. (v - u) * x + u) ` {0..1}"
   by (simp add: add.commute [of u] image_affinity_atLeastAtMost [where c=u] closed_segment_eq_real_ivl)
 
+lemma dist_in_closed_segment:
+  fixes a :: "'a :: euclidean_space"
+  assumes "x \<in> closed_segment a b"
+    shows "dist x a \<le> dist a b \<and> dist x b \<le> dist a b"
+proof (intro conjI)
+  obtain u where u: "0 \<le> u" "u \<le> 1" and x: "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
+    using assms by (force simp: in_segment algebra_simps)
+  have "dist x a = u * dist a b"
+    apply (simp add: dist_norm algebra_simps x)
+    by (metis \<open>0 \<le> u\<close> abs_of_nonneg norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib)
+  also have "...  \<le> dist a b"
+    by (simp add: mult_left_le_one_le u)
+  finally show "dist x a \<le> dist a b" .
+  have "dist x b = norm ((1-u) *\<^sub>R a - (1-u) *\<^sub>R b)"
+    by (simp add: dist_norm algebra_simps x)
+  also have "... = (1-u) * dist a b"
+  proof -
+    have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)"
+      using \<open>u \<le> 1\<close> by force
+    then show ?thesis
+      by (simp add: dist_norm real_vector.scale_right_diff_distrib)
+  qed
+  also have "... \<le> dist a b"
+    by (simp add: mult_left_le_one_le u)
+  finally show "dist x b \<le> dist a b" .
+qed
+
+lemma dist_in_open_segment:
+  fixes a :: "'a :: euclidean_space"
+  assumes "x \<in> open_segment a b"
+    shows "dist x a < dist a b \<and> dist x b < dist a b"
+proof (intro conjI)
+  obtain u where u: "0 < u" "u < 1" and x: "x = (1 - u) *\<^sub>R a + u *\<^sub>R b"
+    using assms by (force simp: in_segment algebra_simps)
+  have "dist x a = u * dist a b"
+    apply (simp add: dist_norm algebra_simps x)
+    by (metis abs_of_nonneg less_eq_real_def norm_minus_commute norm_scaleR real_vector.scale_right_diff_distrib \<open>0 < u\<close>)
+  also have *: "...  < dist a b"
+    by (metis (no_types) assms dist_eq_0_iff dist_not_less_zero in_segment(2) linorder_neqE_linordered_idom mult.left_neutral real_mult_less_iff1 \<open>u < 1\<close>)
+  finally show "dist x a < dist a b" .
+  have ab_ne0: "dist a b \<noteq> 0"
+    using * by fastforce
+  have "dist x b = norm ((1-u) *\<^sub>R a - (1-u) *\<^sub>R b)"
+    by (simp add: dist_norm algebra_simps x)
+  also have "... = (1-u) * dist a b"
+  proof -
+    have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)"
+      using \<open>u < 1\<close> by force
+    then show ?thesis
+      by (simp add: dist_norm real_vector.scale_right_diff_distrib)
+  qed
+  also have "... < dist a b"
+    using ab_ne0 \<open>0 < u\<close> by simp
+  finally show "dist x b < dist a b" .
+qed
+
+lemma dist_decreases_open_segment_0:
+  fixes x :: "'a :: euclidean_space"
+  assumes "x \<in> open_segment 0 b"
+    shows "dist c x < dist c 0 \<or> dist c x < dist c b"
+proof (rule ccontr, clarsimp simp: not_less)
+  obtain u where u: "0 \<noteq> b" "0 < u" "u < 1" and x: "x = u *\<^sub>R b"
+    using assms by (auto simp: in_segment)
+  have xb: "x \<bullet> b < b \<bullet> b"
+    using u x by auto
+  assume "norm c \<le> dist c x"
+  then have "c \<bullet> c \<le> (c - x) \<bullet> (c - x)"
+    by (simp add: dist_norm norm_le)
+  moreover have "0 < x \<bullet> b"
+    using u x by auto
+  ultimately have less: "c \<bullet> b < x \<bullet> b"
+    by (simp add: x algebra_simps inner_commute u)
+  assume "dist c b \<le> dist c x"
+  then have "(c - b) \<bullet> (c - b) \<le> (c - x) \<bullet> (c - x)"
+    by (simp add: dist_norm norm_le)
+  then have "(b \<bullet> b) * (1 - u*u) \<le> 2 * (b \<bullet> c) * (1-u)"
+    by (simp add: x algebra_simps inner_commute)
+  then have "(1+u) * (b \<bullet> b) * (1-u) \<le> 2 * (b \<bullet> c) * (1-u)"
+    by (simp add: algebra_simps)
+  then have "(1+u) * (b \<bullet> b) \<le> 2 * (b \<bullet> c)"
+    using \<open>u < 1\<close> by auto
+  with xb have "c \<bullet> b \<ge> x \<bullet> b"
+    by (auto simp: x algebra_simps inner_commute)
+  with less show False by auto
+qed
+
+proposition dist_decreases_open_segment:
+  fixes a :: "'a :: euclidean_space"
+  assumes "x \<in> open_segment a b"
+    shows "dist c x < dist c a \<or> dist c x < dist c b"
+proof -
+  have *: "x - a \<in> open_segment 0 (b - a)" using assms
+    by (metis diff_self open_segment_translation_eq uminus_add_conv_diff)
+  show ?thesis
+    using dist_decreases_open_segment_0 [OF *, of "c-a"] assms
+    by (simp add: dist_norm)
+qed
+
+lemma dist_decreases_closed_segment:
+  fixes a :: "'a :: euclidean_space"
+  assumes "x \<in> closed_segment a b"
+    shows "dist c x \<le> dist c a \<or> dist c x \<le> dist c b"
+apply (cases "x \<in> open_segment a b")
+ using dist_decreases_open_segment less_eq_real_def apply blast
+by (metis DiffI assms empty_iff insertE open_segment_def order_refl)
+
+lemma convex_intermediate_ball:
+  fixes a :: "'a :: euclidean_space"
+  shows "\<lbrakk>ball a r \<subseteq> T; T \<subseteq> cball a r\<rbrakk> \<Longrightarrow> convex T"
+apply (simp add: convex_contains_open_segment, clarify)
+by (metis (no_types, hide_lams) less_le_trans mem_ball mem_cball subsetCE dist_decreases_open_segment)
+
 subsubsection\<open>More lemmas, especially for working with the underlying formula\<close>
 
 lemma segment_eq_compose:
@@ -8157,6 +8325,28 @@
 
 definition "rel_frontier S = closure S - rel_interior S"
 
+lemma rel_frontier_empty [simp]: "rel_frontier {} = {}"
+  by (simp add: rel_frontier_def)
+
+lemma rel_frontier_sing [simp]:
+    fixes a :: "'n::euclidean_space"
+    shows "rel_frontier {a} = {}"
+  by (simp add: rel_frontier_def)
+
+lemma rel_frontier_cball [simp]:
+    fixes a :: "'n::euclidean_space"
+    shows "rel_frontier(cball a r) = (if r = 0 then {} else sphere a r)"
+proof (cases rule: linorder_cases [of r 0])
+  case less then show ?thesis
+    by (force simp: sphere_def)
+next
+  case equal then show ?thesis by simp
+next
+  case greater then show ?thesis
+    apply simp
+    by (metis centre_in_ball empty_iff frontier_cball frontier_def interior_cball interior_rel_interior_gen rel_frontier_def)
+qed
+
 lemma closed_affine_hull:
   fixes S :: "'n::euclidean_space set"
   shows "closed (affine hull S)"
@@ -8190,6 +8380,43 @@
     done
 qed
 
+lemma closed_rel_boundary:
+  fixes S :: "'n::euclidean_space set"
+  shows "closed S \<Longrightarrow> closed(S - rel_interior S)"
+by (metis closed_rel_frontier closure_closed rel_frontier_def)
+
+lemma compact_rel_boundary:
+  fixes S :: "'n::euclidean_space set"
+  shows "compact S \<Longrightarrow> compact(S - rel_interior S)"
+by (metis bounded_diff closed_rel_boundary closure_eq compact_closure compact_imp_closed)
+
+lemma bounded_rel_frontier:
+  fixes S :: "'n::euclidean_space set"
+  shows "bounded S \<Longrightarrow> bounded(rel_frontier S)"
+by (simp add: bounded_closure bounded_diff rel_frontier_def)
+
+lemma compact_rel_frontier_bounded:
+  fixes S :: "'n::euclidean_space set"
+  shows "bounded S \<Longrightarrow> compact(rel_frontier S)"
+using bounded_rel_frontier closed_rel_frontier compact_eq_bounded_closed by blast
+
+lemma compact_rel_frontier:
+  fixes S :: "'n::euclidean_space set"
+  shows "compact S \<Longrightarrow> compact(rel_frontier S)"
+by (meson compact_eq_bounded_closed compact_rel_frontier_bounded)
+
+lemma convex_same_rel_interior_closure:
+  fixes S :: "'n::euclidean_space set"
+  shows "\<lbrakk>convex S; convex T\<rbrakk>
+         \<Longrightarrow> rel_interior S = rel_interior T \<longleftrightarrow> closure S = closure T"
+by (simp add: closure_eq_rel_interior_eq)
+
+lemma convex_same_rel_interior_closure_straddle:
+  fixes S :: "'n::euclidean_space set"
+  shows "\<lbrakk>convex S; convex T\<rbrakk>
+         \<Longrightarrow> rel_interior S = rel_interior T \<longleftrightarrow>
+             rel_interior S \<subseteq> T \<and> T \<subseteq> closure S"
+by (simp add: closure_eq_between convex_same_rel_interior_closure)
 
 lemma convex_rel_frontier_aff_dim:
   fixes S1 S2 :: "'n::euclidean_space set"
@@ -10701,6 +10928,16 @@
   shows "setdist s {x} = 0 \<longleftrightarrow> s = {} \<or> x \<in> closure s"
 by (auto simp: setdist_eq_0_bounded)
 
+lemma setdist_neq_0_sing_1:
+    fixes s :: "'a::euclidean_space set"
+    shows "\<lbrakk>setdist {x} s = a; a \<noteq> 0\<rbrakk> \<Longrightarrow> s \<noteq> {} \<and> x \<notin> closure s"
+by auto
+
+lemma setdist_neq_0_sing_2:
+  fixes s :: "'a::euclidean_space set"
+    shows "\<lbrakk>setdist s {x} = a; a \<noteq> 0\<rbrakk> \<Longrightarrow> s \<noteq> {} \<and> x \<notin> closure s"
+by auto
+
 lemma setdist_sing_in_set:
   fixes s :: "'a::euclidean_space set"
   shows "x \<in> s \<Longrightarrow> setdist {x} s = 0"
@@ -12046,6 +12283,42 @@
     done
 qed
 
+proposition orthonormal_basis_subspace:
+  fixes S :: "'a :: euclidean_space set"
+  assumes "subspace S"
+  obtains B where "B \<subseteq> S" "pairwise orthogonal B"
+              and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
+              and "independent B" "card B = dim S" "span B = S"
+proof -
+  obtain B where "0 \<notin> B" "B \<subseteq> S"
+             and orth: "pairwise orthogonal B"
+             and "independent B" "card B = dim S" "span B = S"
+    by (blast intro: orthogonal_basis_subspace [OF assms])
+  have 1: "(\<lambda>x. x /\<^sub>R norm x) ` B \<subseteq> S"
+    using \<open>span B = S\<close> span_clauses(1) span_mul by fastforce
+  have 2: "pairwise orthogonal ((\<lambda>x. x /\<^sub>R norm x) ` B)"
+    using orth by (force simp: pairwise_def orthogonal_clauses)
+  have 3: "\<And>x. x \<in> (\<lambda>x. x /\<^sub>R norm x) ` B \<Longrightarrow> norm x = 1"
+    by (metis (no_types, lifting) \<open>0 \<notin> B\<close> image_iff norm_sgn sgn_div_norm)
+  have 4: "independent ((\<lambda>x. x /\<^sub>R norm x) ` B)"
+    by (metis "2" "3" norm_zero pairwise_orthogonal_independent zero_neq_one)
+  have "inj_on (\<lambda>x. x /\<^sub>R norm x) B"
+  proof
+    fix x y
+    assume "x \<in> B" "y \<in> B" "x /\<^sub>R norm x = y /\<^sub>R norm y"
+    moreover have "\<And>i. i \<in> B \<Longrightarrow> norm (i /\<^sub>R norm i) = 1"
+      using 3 by blast
+    ultimately show "x = y"
+      by (metis norm_eq_1 orth orthogonal_clauses(7) orthogonal_commute orthogonal_def pairwise_def zero_neq_one)
+  qed
+  then have 5: "card ((\<lambda>x. x /\<^sub>R norm x) ` B) = dim S"
+    by (metis \<open>card B = dim S\<close> card_image)
+  have 6: "span ((\<lambda>x. x /\<^sub>R norm x) ` B) = S"
+    by (metis "1" "4" "5" assms card_eq_dim independent_finite span_subspace)
+  show ?thesis
+    by (rule that [OF 1 2 3 4 5 6])
+qed
+
 proposition orthogonal_subspace_decomp_exists:
   fixes S :: "'a :: euclidean_space set"
   obtains y z where "y \<in> span S" "\<And>w. w \<in> span S \<Longrightarrow> orthogonal z w" "x = y + z"
@@ -12078,6 +12351,7 @@
   with assms show ?thesis by auto
 qed
 
+subsection\<open>Parallel slices, etc.\<close>
 
 text\<open> If we take a slice out of a set, we can do it perpendicularly,
   with the normal vector to the slice parallel to the affine hull.\<close>
@@ -12139,4 +12413,167 @@
   qed
 qed
 
+lemma diffs_affine_hull_span:
+  assumes "a \<in> S"
+    shows "{x - a |x. x \<in> affine hull S} = span {x - a |x. x \<in> S}"
+proof -
+  have *: "((\<lambda>x. x - a) ` (S - {a})) = {x. x + a \<in> S} - {0}"
+    by (auto simp: algebra_simps)
+  show ?thesis
+    apply (simp add: affine_hull_span2 [OF assms] *)
+    apply (auto simp: algebra_simps)
+    done
+qed
+
+lemma aff_dim_dim_affine_diffs:
+  fixes S :: "'a :: euclidean_space set"
+  assumes "affine S" "a \<in> S"
+    shows "aff_dim S = dim {x - a |x. x \<in> S}"
+proof -
+  obtain B where aff: "affine hull B = affine hull S"
+             and ind: "\<not> affine_dependent B"
+             and card: "of_nat (card B) = aff_dim S + 1"
+    using aff_dim_basis_exists by blast
+  then have "B \<noteq> {}" using assms
+    by (metis affine_hull_eq_empty ex_in_conv)
+  then obtain c where "c \<in> B" by auto
+  then have "c \<in> S"
+    by (metis aff affine_hull_eq \<open>affine S\<close> hull_inc)
+  have xy: "x - c = y - a \<longleftrightarrow> y = x + 1 *\<^sub>R (a - c)" for x y c and a::'a
+    by (auto simp: algebra_simps)
+  have *: "{x - c |x. x \<in> S} = {x - a |x. x \<in> S}"
+    apply safe
+    apply (simp_all only: xy)
+    using mem_affine_3_minus [OF \<open>affine S\<close>] \<open>a \<in> S\<close> \<open>c \<in> S\<close> apply blast+
+    done
+  have affS: "affine hull S = S"
+    by (simp add: \<open>affine S\<close>)
+  have "aff_dim S = of_nat (card B) - 1"
+    using card by simp
+  also have "... = dim {x - c |x. x \<in> B}"
+    by (simp add: affine_independent_card_dim_diffs [OF ind \<open>c \<in> B\<close>])
+  also have "... = dim {x - c | x. x \<in> affine hull B}"
+     by (simp add: diffs_affine_hull_span \<open>c \<in> B\<close>)
+  also have "... = dim {x - a |x. x \<in> S}"
+     by (simp add: affS aff *)
+   finally show ?thesis .
+qed
+
+lemma aff_dim_linear_image_le:
+  assumes "linear f"
+    shows "aff_dim(f ` S) \<le> aff_dim S"
+proof -
+  have "aff_dim (f ` T) \<le> aff_dim T" if "affine T" for T
+  proof (cases "T = {}")
+    case True then show ?thesis by (simp add: aff_dim_geq)
+  next
+    case False
+    then obtain a where "a \<in> T" by auto
+    have 1: "((\<lambda>x. x - f a) ` f ` T) = {x - f a |x. x \<in> f ` T}"
+      by auto
+    have 2: "{x - f a| x. x \<in> f ` T} = f ` {x - a| x. x \<in> T}"
+      by (force simp: linear_sub [OF assms])
+    have "aff_dim (f ` T) = int (dim {x - f a |x. x \<in> f ` T})"
+      by (simp add: \<open>a \<in> T\<close> hull_inc aff_dim_eq_dim [of "f a"] 1)
+    also have "... = int (dim (f ` {x - a| x. x \<in> T}))"
+      by (force simp: linear_sub [OF assms] 2)
+    also have "... \<le> int (dim {x - a| x. x \<in> T})"
+      by (simp add: dim_image_le [OF assms])
+    also have "... \<le> aff_dim T"
+      by (simp add: aff_dim_dim_affine_diffs [symmetric] \<open>a \<in> T\<close> \<open>affine T\<close>)
+    finally show ?thesis .
+  qed
+  then
+  have "aff_dim (f ` (affine hull S)) \<le> aff_dim (affine hull S)"
+    using affine_affine_hull [of S] by blast
+  then show ?thesis
+    using affine_hull_linear_image assms linear_conv_bounded_linear by fastforce
+qed
+
+lemma aff_dim_injective_linear_image [simp]:
+  assumes "linear f" "inj f"
+    shows "aff_dim (f ` S) = aff_dim S"
+proof (rule antisym)
+  show "aff_dim (f ` S) \<le> aff_dim S"
+    by (simp add: aff_dim_linear_image_le assms(1))
+next
+  obtain g where "linear g" "g \<circ> f = id"
+    using linear_injective_left_inverse assms by blast
+  then have "aff_dim S \<le> aff_dim(g ` f ` S)"
+    by (simp add: image_comp)
+  also have "... \<le> aff_dim (f ` S)"
+    by (simp add: \<open>linear g\<close> aff_dim_linear_image_le)
+  finally show "aff_dim S \<le> aff_dim (f ` S)" .
+qed
+
+text\<open>Choosing a subspace of a given dimension\<close>
+proposition choose_subspace_of_subspace:
+  fixes S :: "'n::euclidean_space set"
+  assumes "n \<le> dim S"
+  obtains T where "subspace T" "T \<subseteq> span S" "dim T = n"
+proof -
+  have "\<exists>T. subspace T \<and> T \<subseteq> span S \<and> dim T = n"
+  using assms
+  proof (induction n)
+    case 0 then show ?case by force
+  next
+    case (Suc n)
+    then obtain T where "subspace T" "T \<subseteq> span S" "dim T = n"
+      by force
+    then show ?case
+    proof (cases "span S \<subseteq> span T")
+      case True
+      have "dim S = dim T"
+        apply (rule span_eq_dim [OF subset_antisym [OF True]])
+        by (simp add: \<open>T \<subseteq> span S\<close> span_minimal subspace_span)
+      then show ?thesis
+        using Suc.prems \<open>dim T = n\<close> by linarith
+    next
+      case False
+      then obtain y where y: "y \<in> S" "y \<notin> T"
+        by (meson span_mono subsetI)
+      then have "span (insert y T) \<subseteq> span S"
+        by (metis (no_types) \<open>T \<subseteq> span S\<close> subsetD insert_subset span_inc span_mono span_span)
+      with \<open>dim T = n\<close>  \<open>subspace T\<close> span_induct y show ?thesis
+        apply (rule_tac x="span(insert y T)" in exI)
+        apply (auto simp: subspace_span dim_insert)
+        done
+    qed
+  qed
+  with that show ?thesis by blast
+qed
+
+lemma choose_affine_subset:
+  assumes "affine S" "-1 \<le> d" and dle: "d \<le> aff_dim S"
+  obtains T where "affine T" "T \<subseteq> S" "aff_dim T = d"
+proof (cases "d = -1 \<or> S={}")
+  case True with assms show ?thesis
+    by (metis aff_dim_empty affine_empty bot.extremum that eq_iff)
+next
+  case False
+  with assms obtain a where "a \<in> S" "0 \<le> d" by auto
+  with assms have ss: "subspace (op + (- a) ` S)"
+    by (simp add: affine_diffs_subspace)
+  have "nat d \<le> dim (op + (- a) ` S)"
+    by (metis aff_dim_subspace aff_dim_translation_eq dle nat_int nat_mono ss)
+  then obtain T where "subspace T" and Tsb: "T \<subseteq> span (op + (- a) ` S)"
+                  and Tdim: "dim T = nat d"
+    using choose_subspace_of_subspace [of "nat d" "op + (- a) ` S"] by blast
+  then have "affine T"
+    using subspace_affine by blast
+  then have "affine (op + a ` T)"
+    by (metis affine_hull_eq affine_hull_translation)
+  moreover have "op + a ` T \<subseteq> S"
+  proof -
+    have "T \<subseteq> op + (- a) ` S"
+      by (metis (no_types) span_eq Tsb ss)
+    then show "op + a ` T \<subseteq> S"
+      using add_ac by auto
+  qed
+  moreover have "aff_dim (op + a ` T) = d"
+    by (simp add: aff_dim_subspace Tdim \<open>0 \<le> d\<close> \<open>subspace T\<close> aff_dim_translation_eq)
+  ultimately show ?thesis
+    by (rule that)
+qed
+
 end
diff -r 932cf444f2fe -r 27afe7af7379 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sat May 21 07:08:59 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon May 23 15:33:24 2016 +0100
@@ -110,6 +110,18 @@
 lemma DIM_ge_Suc0 [iff]: "Suc 0 \<le> card Basis"
   by (meson DIM_positive Suc_leI)
 
+
+lemma setsum_inner_Basis_scaleR [simp]:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_vector"
+  assumes "b \<in> Basis" shows "(\<Sum>i\<in>Basis. (inner i b) *\<^sub>R f i) = f b"
+  by (simp add: comm_monoid_add_class.setsum.remove [OF finite_Basis assms]
+         assms inner_not_same_Basis comm_monoid_add_class.setsum.neutral)
+
+lemma setsum_inner_Basis_eq [simp]:
+  assumes "b \<in> Basis" shows "(\<Sum>i\<in>Basis. (inner i b) * f i) = f b"
+  by (simp add: comm_monoid_add_class.setsum.remove [OF finite_Basis assms]
+         assms inner_not_same_Basis comm_monoid_add_class.setsum.neutral)
+
 subsection \<open>Subclass relationships\<close>
 
 instance euclidean_space \<subseteq> perfect_space
diff -r 932cf444f2fe -r 27afe7af7379 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sat May 21 07:08:59 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Mon May 23 15:33:24 2016 +0100
@@ -223,7 +223,7 @@
 lemma subspace_neg: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> - x \<in> S"
   by (metis scaleR_minus1_left subspace_mul)
 
-lemma subspace_sub: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x - y \<in> S"
+lemma subspace_diff: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x - y \<in> S"
   using subspace_add [of S x "- y"] by (simp add: subspace_neg)
 
 lemma (in real_vector) subspace_setsum:
@@ -434,7 +434,7 @@
   by (metis subspace_neg subspace_span)
 
 lemma span_sub: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x - y \<in> span S"
-  by (metis subspace_span subspace_sub)
+  by (metis subspace_span subspace_diff)
 
 lemma (in real_vector) span_setsum: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> span S) \<Longrightarrow> setsum f A \<in> span S"
   by (rule subspace_setsum [OF subspace_span])
@@ -1524,6 +1524,46 @@
 lemma orthogonal_commute: "orthogonal x y \<longleftrightarrow> orthogonal y x"
   by (simp add: orthogonal_def inner_commute)
 
+lemma orthogonal_scaleR [simp]: "c \<noteq> 0 \<Longrightarrow> orthogonal (c *\<^sub>R x) = orthogonal x"
+  by (rule ext) (simp add: orthogonal_def)
+
+lemma pairwise_ortho_scaleR:
+    "pairwise (\<lambda>i j. orthogonal (f i) (g j)) B
+    \<Longrightarrow> pairwise (\<lambda>i j. orthogonal (a i *\<^sub>R f i) (a j *\<^sub>R g j)) B"
+  by (auto simp: pairwise_def orthogonal_clauses)
+
+lemma orthogonal_rvsum:
+    "\<lbrakk>finite s; \<And>y. y \<in> s \<Longrightarrow> orthogonal x (f y)\<rbrakk> \<Longrightarrow> orthogonal x (setsum f s)"
+  by (induction s rule: finite_induct) (auto simp: orthogonal_clauses)
+
+lemma orthogonal_lvsum:
+    "\<lbrakk>finite s; \<And>x. x \<in> s \<Longrightarrow> orthogonal (f x) y\<rbrakk> \<Longrightarrow> orthogonal (setsum f s) y"
+  by (induction s rule: finite_induct) (auto simp: orthogonal_clauses)
+
+lemma norm_add_Pythagorean:
+  assumes "orthogonal a b"
+    shows "norm(a + b) ^ 2 = norm a ^ 2 + norm b ^ 2"
+proof -
+  from assms have "(a - (0 - b)) \<bullet> (a - (0 - b)) = a \<bullet> a - (0 - b \<bullet> b)"
+    by (simp add: algebra_simps orthogonal_def inner_commute)
+  then show ?thesis
+    by (simp add: power2_norm_eq_inner)
+qed
+
+lemma norm_setsum_Pythagorean:
+  assumes "finite I" "pairwise (\<lambda>i j. orthogonal (f i) (f j)) I"
+    shows "(norm (setsum f I))\<^sup>2 = (\<Sum>i\<in>I. (norm (f i))\<^sup>2)"
+using assms
+proof (induction I rule: finite_induct)
+  case empty then show ?case by simp
+next
+  case (insert x I)
+  then have "orthogonal (f x) (setsum f I)"
+    by (metis pairwise_insert orthogonal_rvsum)
+  with insert show ?case
+    by (simp add: pairwise_insert norm_add_Pythagorean)
+qed
+
 
 subsection \<open>Bilinear functions.\<close>
 
diff -r 932cf444f2fe -r 27afe7af7379 src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Sat May 21 07:08:59 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon May 23 15:33:24 2016 +0100
@@ -2109,6 +2109,79 @@
     by (auto simp: closure_def)
 qed
 
+lemma connected_disjoint_Union_open_pick:
+  assumes "pairwise disjnt B"
+          "\<And>S. S \<in> A \<Longrightarrow> connected S \<and> S \<noteq> {}"
+          "\<And>S. S \<in> B \<Longrightarrow> open S"
+          "\<Union>A \<subseteq> \<Union>B"
+          "S \<in> A"
+  obtains T where "T \<in> B" "S \<subseteq> T" "S \<inter> \<Union>(B - {T}) = {}"
+proof -
+  have "S \<subseteq> \<Union>B" "connected S" "S \<noteq> {}"
+    using assms \<open>S \<in> A\<close> by blast+
+  then obtain T where "T \<in> B" "S \<inter> T \<noteq> {}"
+    by (metis Sup_inf_eq_bot_iff inf.absorb_iff2 inf_commute)
+  have 1: "open T" by (simp add: \<open>T \<in> B\<close> assms)
+  have 2: "open (\<Union>(B-{T}))" using assms by blast
+  have 3: "S \<subseteq> T \<union> \<Union>(B - {T})" using \<open>S \<subseteq> \<Union>B\<close> by blast
+  have "T \<inter> \<Union>(B - {T}) = {}" using \<open>T \<in> B\<close> \<open>pairwise disjnt B\<close>
+    by (auto simp: pairwise_def disjnt_def)
+  then have 4: "T \<inter> \<Union>(B - {T}) \<inter> S = {}" by auto
+  from connectedD [OF \<open>connected S\<close> 1 2 3 4]
+  have "S \<inter> \<Union>(B-{T}) = {}"
+    by (auto simp: Int_commute \<open>S \<inter> T \<noteq> {}\<close>)
+  with \<open>T \<in> B\<close> have "S \<subseteq> T"
+    using "3" by auto
+  show ?thesis
+    using \<open>S \<inter> \<Union>(B - {T}) = {}\<close> \<open>S \<subseteq> T\<close> \<open>T \<in> B\<close> that by auto
+qed
+
+lemma connected_disjoint_Union_open_subset:
+  assumes A: "pairwise disjnt A" and B: "pairwise disjnt B"
+      and SA: "\<And>S. S \<in> A \<Longrightarrow> open S \<and> connected S \<and> S \<noteq> {}"
+      and SB: "\<And>S. S \<in> B \<Longrightarrow> open S \<and> connected S \<and> S \<noteq> {}"
+      and eq [simp]: "\<Union>A = \<Union>B"
+    shows "A \<subseteq> B"
+proof
+  fix S
+  assume "S \<in> A"
+  obtain T where "T \<in> B" "S \<subseteq> T" "S \<inter> \<Union>(B - {T}) = {}"
+      apply (rule connected_disjoint_Union_open_pick [OF B, of A])
+      using SA SB \<open>S \<in> A\<close> by auto
+  moreover obtain S' where "S' \<in> A" "T \<subseteq> S'" "T \<inter> \<Union>(A - {S'}) = {}"
+      apply (rule connected_disjoint_Union_open_pick [OF A, of B])
+      using SA SB \<open>T \<in> B\<close> by auto
+  ultimately have "S' = S"
+    by (metis A Int_subset_iff SA \<open>S \<in> A\<close> disjnt_def inf.orderE pairwise_def)
+  with \<open>T \<subseteq> S'\<close> have "T \<subseteq> S" by simp
+  with \<open>S \<subseteq> T\<close> have "S = T" by blast
+  with \<open>T \<in> B\<close> show "S \<in> B" by simp
+qed
+
+lemma connected_disjoint_Union_open_unique:
+  assumes A: "pairwise disjnt A" and B: "pairwise disjnt B"
+      and SA: "\<And>S. S \<in> A \<Longrightarrow> open S \<and> connected S \<and> S \<noteq> {}"
+      and SB: "\<And>S. S \<in> B \<Longrightarrow> open S \<and> connected S \<and> S \<noteq> {}"
+      and eq [simp]: "\<Union>A = \<Union>B"
+    shows "A = B"
+by (rule subset_antisym; metis connected_disjoint_Union_open_subset assms)
+
+proposition components_open_unique:
+ fixes S :: "'a::real_normed_vector set"
+  assumes "pairwise disjnt A" "\<Union>A = S"
+          "\<And>X. X \<in> A \<Longrightarrow> open X \<and> connected X \<and> X \<noteq> {}"
+    shows "components S = A"
+proof -
+  have "open S" using assms by blast
+  show ?thesis
+    apply (rule connected_disjoint_Union_open_unique)
+    apply (simp add: components_eq disjnt_def pairwise_def)
+    using \<open>open S\<close>
+    apply (simp_all add: assms open_components in_components_connected in_components_nonempty)
+    done
+qed
+
+
 subsection\<open>Existence of unbounded components\<close>
 
 lemma cobounded_unbounded_component:
@@ -3742,14 +3815,13 @@
 lemma homotopic_paths_linear:
   fixes g h :: "real \<Rightarrow> 'a::real_normed_vector"
   assumes "path g" "path h" "pathstart h = pathstart g" "pathfinish h = pathfinish g"
-          "\<And>t x. t \<in> {0..1} \<Longrightarrow> closed_segment (g t) (h t) \<subseteq> s"
+          "\<And>t. t \<in> {0..1} \<Longrightarrow> closed_segment (g t) (h t) \<subseteq> s"
     shows "homotopic_paths s g h"
   using assms
   unfolding path_def
   apply (simp add: closed_segment_def pathstart_def pathfinish_def homotopic_paths_def homotopic_with_def)
-  apply (rule_tac x="\<lambda>y. ((1 - (fst y)) *\<^sub>R g(snd y) + (fst y) *\<^sub>R h(snd y))" in exI)
-  apply (intro conjI subsetI continuous_intros)
-  apply (fastforce intro: continuous_intros continuous_on_compose2 [where g=g] continuous_on_compose2 [where g=h])+
+  apply (rule_tac x="\<lambda>y. ((1 - (fst y)) *\<^sub>R (g o snd) y + (fst y) *\<^sub>R (h o snd) y)" in exI)
+  apply (intro conjI subsetI continuous_intros; force)
   done
 
 lemma homotopic_loops_linear:
@@ -5052,6 +5124,346 @@
 apply (force simp: convex_Int convex_imp_path_connected)
 done
 
+subsection\<open>Components, continuity, openin, closedin\<close>
+
+lemma continuous_openin_preimage_eq:
+   "continuous_on S f \<longleftrightarrow>
+    (\<forall>t. open t \<longrightarrow> openin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> t})"
+apply (auto simp: continuous_openin_preimage)
+apply (fastforce simp add: continuous_on_open openin_open)
+done
+
+lemma continuous_closedin_preimage_eq:
+   "continuous_on S f \<longleftrightarrow>
+    (\<forall>t. closed t \<longrightarrow> closedin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> t})"
+apply safe
+apply (simp add: continuous_closedin_preimage)
+apply (fastforce simp add: continuous_on_closed closedin_closed)
+done
+
+lemma continuous_on_components_gen:
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
+  assumes "\<And>c. c \<in> components S \<Longrightarrow>
+              openin (subtopology euclidean S) c \<and> continuous_on c f"
+    shows "continuous_on S f"
+proof (clarsimp simp: continuous_openin_preimage_eq)
+  fix t :: "'b set"
+  assume "open t"
+  have "{x. x \<in> S \<and> f x \<in> t} = \<Union>{{x. x \<in> c \<and> f x \<in> t} |c. c \<in> components S}"
+    apply auto
+    apply (metis (lifting) components_iff connected_component_refl_eq mem_Collect_eq)
+    using Union_components by blast
+  then show "openin (subtopology euclidean S) {x \<in> S. f x \<in> t}"
+    using \<open>open t\<close> assms
+    by (fastforce intro: openin_trans continuous_openin_preimage)
+qed
+
+lemma continuous_on_components:
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
+  assumes "locally connected S "
+          "\<And>c. c \<in> components S \<Longrightarrow> continuous_on c f"
+    shows "continuous_on S f"
+apply (rule continuous_on_components_gen)
+apply (auto simp: assms intro: openin_components_locally_connected)
+done
+
+lemma continuous_on_components_eq:
+    "locally connected S
+     \<Longrightarrow> (continuous_on S f \<longleftrightarrow> (\<forall>c \<in> components S. continuous_on c f))"
+by (meson continuous_on_components continuous_on_subset in_components_subset)
+
+lemma continuous_on_components_open:
+ fixes S :: "'a::real_normed_vector set"
+  assumes "open S "
+          "\<And>c. c \<in> components S \<Longrightarrow> continuous_on c f"
+    shows "continuous_on S f"
+using continuous_on_components open_imp_locally_connected assms by blast
+
+lemma continuous_on_components_open_eq:
+  fixes S :: "'a::real_normed_vector set"
+  shows "open S \<Longrightarrow> (continuous_on S f \<longleftrightarrow> (\<forall>c \<in> components S. continuous_on c f))"
+using continuous_on_subset in_components_subset
+by (blast intro: continuous_on_components_open)
+
+lemma closedin_union_complement_components:
+  assumes u: "locally connected u"
+      and S: "closedin (subtopology euclidean u) S"
+      and cuS: "c \<subseteq> components(u - S)"
+    shows "closedin (subtopology euclidean u) (S \<union> \<Union>c)"
+proof -
+  have di: "(\<And>S t. S \<in> c \<and> t \<in> c' \<Longrightarrow> disjnt S t) \<Longrightarrow> disjnt (\<Union> c) (\<Union> c')" for c'
+    by (simp add: disjnt_def) blast
+  have "S \<subseteq> u"
+    using S closedin_imp_subset by blast
+  moreover have "u - S = \<Union>c \<union> \<Union>(components (u - S) - c)"
+    by (metis Diff_partition Topology_Euclidean_Space.Union_components Union_Un_distrib assms(3))
+  moreover have "disjnt (\<Union>c) (\<Union>(components (u - S) - c))"
+    apply (rule di)
+    by (metis DiffD1 DiffD2 assms(3) components_nonoverlap disjnt_def subsetCE)
+  ultimately have eq: "S \<union> \<Union>c = u - (\<Union>(components(u - S) - c))"
+    by (auto simp: disjnt_def)
+  have *: "openin (subtopology euclidean u) (\<Union>(components (u - S) - c))"
+    apply (rule openin_Union)
+    apply (rule openin_trans [of "u - S"])
+    apply (simp add: u S locally_diff_closed openin_components_locally_connected)
+    apply (simp add: openin_diff S)
+    done
+  have "openin (subtopology euclidean u) (u - (u - \<Union>(components (u - S) - c)))"
+    apply (rule openin_diff, simp)
+    apply (metis closedin_diff closedin_topspace topspace_euclidean_subtopology *)
+    done
+  then show ?thesis
+    by (force simp: eq closedin_def)
+qed
+
+lemma closed_union_complement_components:
+  fixes S :: "'a::real_normed_vector set"
+  assumes S: "closed S" and c: "c \<subseteq> components(- S)"
+    shows "closed(S \<union> \<Union> c)"
+proof -
+  have "closedin (subtopology euclidean UNIV) (S \<union> \<Union>c)"
+    apply (rule closedin_union_complement_components [OF locally_connected_UNIV])
+    using S apply (simp add: closed_closedin)
+    using c apply (simp add: Compl_eq_Diff_UNIV)
+    done
+  then show ?thesis
+    by (simp add: closed_closedin)
+qed
+
+lemma closedin_Un_complement_component:
+  fixes S :: "'a::real_normed_vector set"
+  assumes u: "locally connected u"
+      and S: "closedin (subtopology euclidean u) S"
+      and c: " c \<in> components(u - S)"
+    shows "closedin (subtopology euclidean u) (S \<union> c)"
+proof -
+  have "closedin (subtopology euclidean u) (S \<union> \<Union>{c})"
+    using c by (blast intro: closedin_union_complement_components [OF u S])
+  then show ?thesis
+    by simp
+qed
+
+lemma closed_Un_complement_component:
+  fixes S :: "'a::real_normed_vector set"
+  assumes S: "closed S" and c: " c \<in> components(-S)"
+    shows "closed (S \<union> c)"
+by (metis Compl_eq_Diff_UNIV S c closed_closedin closedin_Un_complement_component locally_connected_UNIV subtopology_UNIV)
+
+
+subsection\<open>Existence of isometry between subspaces of same dimension\<close>
+
+thm subspace_isomorphism
+lemma isometry_subset_subspace:
+  fixes S :: "'a::euclidean_space set"
+    and T :: "'b::euclidean_space set"
+  assumes S: "subspace S"
+      and T: "subspace T"
+      and d: "dim S \<le> dim T"
+  obtains f where "linear f" "f ` S \<subseteq> T" "\<And>x. x \<in> S \<Longrightarrow> norm(f x) = norm x"
+proof -
+  obtain B where "B \<subseteq> S" and Borth: "pairwise orthogonal B"
+             and B1: "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
+             and "independent B" "finite B" "card B = dim S" "span B = S"
+    by (metis orthonormal_basis_subspace [OF S] independent_finite)
+  obtain C where "C \<subseteq> T" and Corth: "pairwise orthogonal C"
+             and C1:"\<And>x. x \<in> C \<Longrightarrow> norm x = 1"
+             and "independent C" "finite C" "card C = dim T" "span C = T"
+    by (metis orthonormal_basis_subspace [OF T] independent_finite)
+  obtain fb where "fb ` B \<subseteq> C" "inj_on fb B"
+    by (metis \<open>card B = dim S\<close> \<open>card C = dim T\<close> \<open>finite B\<close> \<open>finite C\<close> card_le_inj d)
+  then have pairwise_orth_fb: "pairwise (\<lambda>v j. orthogonal (fb v) (fb j)) B"
+    using Corth
+    apply (auto simp: pairwise_def orthogonal_clauses)
+    by (meson subsetD image_eqI inj_on_def)
+  obtain f where "linear f" and ffb: "\<And>x. x \<in> B \<Longrightarrow> f x = fb x"
+    using linear_independent_extend \<open>independent B\<close> by fastforce
+  have "f ` S \<subseteq> T"
+    by (metis ffb \<open>fb ` B \<subseteq> C\<close> \<open>linear f\<close> \<open>span B = S\<close> \<open>span C = T\<close> image_cong span_linear_image span_mono)
+  have [simp]: "\<And>x. x \<in> B \<Longrightarrow> norm (fb x) = norm x"
+    using B1 C1 \<open>fb ` B \<subseteq> C\<close> by auto
+  have "norm (f x) = norm x" if "x \<in> S" for x
+  proof -
+    obtain a where x: "x = (\<Sum>v \<in> B. a v *\<^sub>R v)"
+      using \<open>finite B\<close> \<open>span B = S\<close> \<open>x \<in> S\<close> span_finite by fastforce
+    have "f x = (\<Sum>v \<in> B. f (a v *\<^sub>R v))"
+      using linear_setsum [OF \<open>linear f\<close>] x by auto
+    also have "... = (\<Sum>v \<in> B. a v *\<^sub>R f v)"
+      using \<open>linear f\<close> by (simp add: linear_setsum linear.scaleR)
+    also have "... = (\<Sum>v \<in> B. a v *\<^sub>R fb v)"
+      by (simp add: ffb cong: setsum.cong)
+    finally have "norm (f x)^2 = norm (\<Sum>v\<in>B. a v *\<^sub>R fb v)^2" by simp
+    also have "... = (\<Sum>v\<in>B. norm ((a v *\<^sub>R fb v))^2)"
+      apply (rule norm_setsum_Pythagorean [OF \<open>finite B\<close>])
+      apply (rule pairwise_ortho_scaleR [OF pairwise_orth_fb])
+      done
+    also have "... = norm x ^2"
+      by (simp add: x pairwise_ortho_scaleR Borth norm_setsum_Pythagorean [OF \<open>finite B\<close>])
+    finally show ?thesis
+      by (simp add: norm_eq_sqrt_inner)
+  qed
+  then show ?thesis
+    by (rule that [OF \<open>linear f\<close> \<open>f ` S \<subseteq> T\<close>])
+qed
+
+proposition isometries_subspaces:
+  fixes S :: "'a::euclidean_space set"
+    and T :: "'b::euclidean_space set"
+  assumes S: "subspace S"
+      and T: "subspace T"
+      and d: "dim S = dim T"
+  obtains f g where "linear f" "linear g" "f ` S = T" "g ` T = S"
+                    "\<And>x. x \<in> S \<Longrightarrow> norm(f x) = norm x"
+                    "\<And>x. x \<in> T \<Longrightarrow> norm(g x) = norm x"
+                    "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
+                    "\<And>x. x \<in> T \<Longrightarrow> f(g x) = x"
+proof -
+  obtain B where "B \<subseteq> S" and Borth: "pairwise orthogonal B"
+             and B1: "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
+             and "independent B" "finite B" "card B = dim S" "span B = S"
+    by (metis orthonormal_basis_subspace [OF S] independent_finite)
+  obtain C where "C \<subseteq> T" and Corth: "pairwise orthogonal C"
+             and C1:"\<And>x. x \<in> C \<Longrightarrow> norm x = 1"
+             and "independent C" "finite C" "card C = dim T" "span C = T"
+    by (metis orthonormal_basis_subspace [OF T] independent_finite)
+  obtain fb where "bij_betw fb B C"
+    by (metis \<open>finite B\<close> \<open>finite C\<close> bij_betw_iff_card \<open>card B = dim S\<close> \<open>card C = dim T\<close> d)
+  then have pairwise_orth_fb: "pairwise (\<lambda>v j. orthogonal (fb v) (fb j)) B"
+    using Corth
+    apply (auto simp: pairwise_def orthogonal_clauses bij_betw_def)
+    by (meson subsetD image_eqI inj_on_def)
+  obtain f where "linear f" and ffb: "\<And>x. x \<in> B \<Longrightarrow> f x = fb x"
+    using linear_independent_extend \<open>independent B\<close> by fastforce
+  define gb where "gb \<equiv> inv_into B fb"
+  then have pairwise_orth_gb: "pairwise (\<lambda>v j. orthogonal (gb v) (gb j)) C"
+    using Borth
+    apply (auto simp: pairwise_def orthogonal_clauses bij_betw_def)
+    by (metis \<open>bij_betw fb B C\<close> bij_betw_imp_surj_on bij_betw_inv_into_right inv_into_into)
+  obtain g where "linear g" and ggb: "\<And>x. x \<in> C \<Longrightarrow> g x = gb x"
+    using linear_independent_extend \<open>independent C\<close> by fastforce
+  have "f ` S \<subseteq> T"
+    by (metis \<open>bij_betw fb B C\<close> bij_betw_imp_surj_on eq_iff ffb  \<open>linear f\<close> \<open>span B = S\<close> \<open>span C = T\<close> image_cong span_linear_image)
+  have [simp]: "\<And>x. x \<in> B \<Longrightarrow> norm (fb x) = norm x"
+    using B1 C1 \<open>bij_betw fb B C\<close> bij_betw_imp_surj_on by fastforce
+  have f [simp]: "norm (f x) = norm x" "g (f x) = x" if "x \<in> S" for x
+  proof -
+    obtain a where x: "x = (\<Sum>v \<in> B. a v *\<^sub>R v)"
+      using \<open>finite B\<close> \<open>span B = S\<close> \<open>x \<in> S\<close> span_finite by fastforce
+    have "f x = (\<Sum>v \<in> B. f (a v *\<^sub>R v))"
+      using linear_setsum [OF \<open>linear f\<close>] x by auto
+    also have "... = (\<Sum>v \<in> B. a v *\<^sub>R f v)"
+      using \<open>linear f\<close> by (simp add: linear_setsum linear.scaleR)
+    also have "... = (\<Sum>v \<in> B. a v *\<^sub>R fb v)"
+      by (simp add: ffb cong: setsum.cong)
+    finally have *: "f x = (\<Sum>v\<in>B. a v *\<^sub>R fb v)" .
+    then have "(norm (f x))\<^sup>2 = (norm (\<Sum>v\<in>B. a v *\<^sub>R fb v))\<^sup>2" by simp
+    also have "... = (\<Sum>v\<in>B. norm ((a v *\<^sub>R fb v))^2)"
+      apply (rule norm_setsum_Pythagorean [OF \<open>finite B\<close>])
+      apply (rule pairwise_ortho_scaleR [OF pairwise_orth_fb])
+      done
+    also have "... = (norm x)\<^sup>2"
+      by (simp add: x pairwise_ortho_scaleR Borth norm_setsum_Pythagorean [OF \<open>finite B\<close>])
+    finally show "norm (f x) = norm x"
+      by (simp add: norm_eq_sqrt_inner)
+    have "g (f x) = g (\<Sum>v\<in>B. a v *\<^sub>R fb v)" by (simp add: *)
+    also have "... = (\<Sum>v\<in>B. g (a v *\<^sub>R fb v))"
+      using \<open>linear g\<close> by (simp add: linear_setsum linear.scaleR)
+    also have "... = (\<Sum>v\<in>B. a v *\<^sub>R g (fb v))"
+      by (simp add: \<open>linear g\<close> linear.scaleR)
+    also have "... = (\<Sum>v\<in>B. a v *\<^sub>R v)"
+      apply (rule setsum.cong [OF refl])
+      using \<open>bij_betw fb B C\<close> gb_def bij_betwE bij_betw_inv_into_left gb_def ggb by fastforce
+    also have "... = x"
+      using x by blast
+    finally show "g (f x) = x" .
+  qed
+  have [simp]: "\<And>x. x \<in> C \<Longrightarrow> norm (gb x) = norm x"
+    by (metis B1 C1 \<open>bij_betw fb B C\<close> bij_betw_imp_surj_on gb_def inv_into_into)
+  have g [simp]: "f (g x) = x" if "x \<in> T" for x
+  proof -
+    obtain a where x: "x = (\<Sum>v \<in> C. a v *\<^sub>R v)"
+      using \<open>finite C\<close> \<open>span C = T\<close> \<open>x \<in> T\<close> span_finite by fastforce
+    have "g x = (\<Sum>v \<in> C. g (a v *\<^sub>R v))"
+      using linear_setsum [OF \<open>linear g\<close>] x by auto
+    also have "... = (\<Sum>v \<in> C. a v *\<^sub>R g v)"
+      using \<open>linear g\<close> by (simp add: linear_setsum linear.scaleR)
+    also have "... = (\<Sum>v \<in> C. a v *\<^sub>R gb v)"
+      by (simp add: ggb cong: setsum.cong)
+    finally have "f (g x) = f (\<Sum>v\<in>C. a v *\<^sub>R gb v)" by simp
+    also have "... = (\<Sum>v\<in>C. f (a v *\<^sub>R gb v))"
+      using \<open>linear f\<close> by (simp add: linear_setsum linear.scaleR)
+    also have "... = (\<Sum>v\<in>C. a v *\<^sub>R f (gb v))"
+      by (simp add: \<open>linear f\<close> linear.scaleR)
+    also have "... = (\<Sum>v\<in>C. a v *\<^sub>R v)"
+      using \<open>bij_betw fb B C\<close>
+      by (simp add: bij_betw_def gb_def bij_betw_inv_into_right ffb inv_into_into)
+    also have "... = x"
+      using x by blast
+    finally show "f (g x) = x" .
+  qed
+  have gim: "g ` T = S"
+    by (metis (no_types, lifting) \<open>f ` S \<subseteq> T\<close> \<open>linear g\<close> \<open>span B = S\<close> \<open>span C = T\<close> d dim_eq_span dim_image_le f(2) image_subset_iff span_linear_image span_span subsetI)
+  have fim: "f ` S = T"
+    using \<open>g ` T = S\<close> image_iff by fastforce
+  have [simp]: "norm (g x) = norm x" if "x \<in> T" for x
+    using fim that by auto
+  show ?thesis
+    apply (rule that [OF \<open>linear f\<close> \<open>linear g\<close>])
+    apply (simp_all add: fim gim)
+    done
+qed
+
+(*REPLACE*)
+lemma isometry_subspaces:
+  fixes S :: "'a::euclidean_space set"
+    and T :: "'b::euclidean_space set"
+  assumes S: "subspace S"
+      and T: "subspace T"
+      and d: "dim S = dim T"
+  obtains f where "linear f" "f ` S = T" "\<And>x. x \<in> S \<Longrightarrow> norm(f x) = norm x"
+using isometries_subspaces [OF assms]
+by metis
+
+lemma homeomorphic_subspaces:
+  fixes S :: "'a::euclidean_space set"
+    and T :: "'b::euclidean_space set"
+  assumes S: "subspace S"
+      and T: "subspace T"
+      and d: "dim S = dim T"
+    shows "S homeomorphic T"
+proof -
+  obtain f g where "linear f" "linear g" "f ` S = T" "g ` T = S"
+                   "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x" "\<And>x. x \<in> T \<Longrightarrow> f(g x) = x"
+    by (blast intro: isometries_subspaces [OF assms])
+  then show ?thesis
+    apply (simp add: homeomorphic_def homeomorphism_def)
+    apply (rule_tac x=f in exI)
+    apply (rule_tac x=g in exI)
+    apply (auto simp: linear_continuous_on linear_conv_bounded_linear)
+    done
+qed
+
+lemma homeomorphic_affine_sets:
+  assumes "affine S" "affine T" "aff_dim S = aff_dim T"
+    shows "S homeomorphic T"
+proof (cases "S = {} \<or> T = {}")
+  case True  with assms aff_dim_empty homeomorphic_empty show ?thesis
+    by metis
+next
+  case False
+  then obtain a b where ab: "a \<in> S" "b \<in> T" by auto
+  then have ss: "subspace (op + (- a) ` S)" "subspace (op + (- b) ` T)"
+    using affine_diffs_subspace assms by blast+
+  have dd: "dim (op + (- a) ` S) = dim (op + (- b) ` T)"
+    using assms ab  by (simp add: aff_dim_eq_dim  [OF hull_inc] image_def)
+  have "S homeomorphic (op + (- a) ` S)"
+    by (simp add: homeomorphic_translation)
+  also have "... homeomorphic (op + (- b) ` T)"
+    by (rule homeomorphic_subspaces [OF ss dd])
+  also have "... homeomorphic T"
+    using homeomorphic_sym homeomorphic_translation by auto
+  finally show ?thesis .
+qed
+
 subsection\<open>Retracts, in a general sense, preserve (co)homotopic triviality)\<close>
 
 locale Retracts =
diff -r 932cf444f2fe -r 27afe7af7379 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat May 21 07:08:59 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon May 23 15:33:24 2016 +0100
@@ -861,6 +861,11 @@
   shows "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e"
   by (simp add: dist_norm)
 
+lemma mem_sphere_0 [simp]:
+  fixes x :: "'a::real_normed_vector"
+  shows "x \<in> sphere 0 e \<longleftrightarrow> norm x = e"
+  by (simp add: dist_norm)
+
 lemma centre_in_ball [simp]: "x \<in> ball x e \<longleftrightarrow> 0 < e"
   by simp
 
@@ -986,6 +991,22 @@
 abbreviation One :: "'a::euclidean_space"
   where "One \<equiv> \<Sum>Basis"
 
+lemma One_non_0: assumes "One = (0::'a::euclidean_space)" shows False
+proof -
+  have "dependent (Basis :: 'a set)"
+    apply (simp add: dependent_finite)
+    apply (rule_tac x="\<lambda>i. 1" in exI)
+    using SOME_Basis apply (auto simp: assms)
+    done
+  with independent_Basis show False by force
+qed
+
+corollary One_neq_0[iff]: "One \<noteq> 0"
+  by (metis One_non_0)
+
+corollary Zero_neq_One[iff]: "0 \<noteq> One"
+  by (metis One_non_0)
+
 definition (in euclidean_space) eucl_less (infix "<e" 50)
   where "eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)"
 
@@ -5788,7 +5809,7 @@
   unfolding continuous_on_closed_invariant closedin_closed Int_def vimage_def Int_commute
   by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong)
 
-text \<open>Half-global and completely global cases.\<close>
+subsection \<open>Half-global and completely global cases.\<close>
 
 lemma continuous_openin_preimage:
   assumes "continuous_on s f"  "open t"
@@ -5874,7 +5895,7 @@
   with \<open>x = f y\<close> show "x \<in> f ` interior s" ..
 qed
 
-text \<open>Equality of continuous functions on closure and related results.\<close>
+subsection \<open>Equality of continuous functions on closure and related results.\<close>
 
 lemma continuous_closedin_preimage_constant:
   fixes f :: "_ \<Rightarrow> 'b::t1_space"
@@ -7238,6 +7259,11 @@
   shows "(\<lambda>x. a + x) ` (s - t) = ((\<lambda>x. a + x) ` s) - ((\<lambda>x. a + x) ` t)"
   by auto
 
+lemma translation_Int:
+  fixes a :: "'a::ab_group_add"
+  shows "(\<lambda>x. a + x) ` (s \<inter> t) = ((\<lambda>x. a + x) ` s) \<inter> ((\<lambda>x. a + x) ` t)"
+  by auto
+
 lemma closure_translation:
   fixes a :: "'a::real_normed_vector"
   shows "closure ((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (closure s)"
@@ -7261,6 +7287,30 @@
   unfolding frontier_def translation_diff interior_translation closure_translation
   by auto
 
+lemma sphere_translation:
+  fixes a :: "'n::euclidean_space"
+  shows "sphere (a+c) r = op+a ` sphere c r"
+apply safe
+apply (rule_tac x="x-a" in image_eqI)
+apply (auto simp: dist_norm algebra_simps)
+done
+
+lemma cball_translation:
+  fixes a :: "'n::euclidean_space"
+  shows "cball (a+c) r = op+a ` cball c r"
+apply safe
+apply (rule_tac x="x-a" in image_eqI)
+apply (auto simp: dist_norm algebra_simps)
+done
+
+lemma ball_translation:
+  fixes a :: "'n::euclidean_space"
+  shows "ball (a+c) r = op+a ` ball c r"
+apply safe
+apply (rule_tac x="x-a" in image_eqI)
+apply (auto simp: dist_norm algebra_simps)
+done
+
 
 subsection \<open>Separation between points and sets\<close>
 
@@ -8211,6 +8261,37 @@
   apply auto
   done
 
+lemma homeomorphicI [intro?]:
+   "\<lbrakk>f ` S = T; g ` T = S;
+     continuous_on S f; continuous_on T g;
+     \<And>x. x \<in> S \<Longrightarrow> g(f(x)) = x;
+     \<And>y. y \<in> T \<Longrightarrow> f(g(y)) = y\<rbrakk> \<Longrightarrow> S homeomorphic T"
+unfolding homeomorphic_def homeomorphism_def by metis
+
+lemma homeomorphism_of_subsets:
+   "\<lbrakk>homeomorphism S T f g; S' \<subseteq> S; T'' \<subseteq> T; f ` S' = T'\<rbrakk>
+    \<Longrightarrow> homeomorphism S' T' f g"
+apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
+by (metis contra_subsetD imageI)
+
+lemma homeomorphism_apply1: "\<lbrakk>homeomorphism S T f g; x \<in> S\<rbrakk> \<Longrightarrow> g(f x) = x"
+  by (simp add: homeomorphism_def)
+
+lemma homeomorphism_apply2: "\<lbrakk>homeomorphism S T f g; x \<in> T\<rbrakk> \<Longrightarrow> f(g x) = x"
+  by (simp add: homeomorphism_def)
+
+lemma homeomorphism_image1: "homeomorphism S T f g \<Longrightarrow> f ` S = T"
+  by (simp add: homeomorphism_def)
+
+lemma homeomorphism_image2: "homeomorphism S T f g \<Longrightarrow> g ` T = S"
+  by (simp add: homeomorphism_def)
+
+lemma homeomorphism_cont1: "homeomorphism S T f g \<Longrightarrow> continuous_on S f"
+  by (simp add: homeomorphism_def)
+
+lemma homeomorphism_cont2: "homeomorphism S T f g \<Longrightarrow> continuous_on T g"
+  by (simp add: homeomorphism_def)
+
 text \<open>Relatively weak hypotheses if a set is compact.\<close>
 
 lemma homeomorphism_compact:
@@ -8332,7 +8413,109 @@
     done
 qed
 
-text\<open>"Isometry" (up to constant bounds) of injective linear map etc.\<close>
+subsection\<open>Inverse function property for open/closed maps\<close>
+
+lemma continuous_on_inverse_open_map:
+  assumes contf: "continuous_on S f"
+      and imf: "f ` S = T"
+      and injf: "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
+      and oo: "\<And>U. openin (subtopology euclidean S) U
+                    \<Longrightarrow> openin (subtopology euclidean T) (f ` U)"
+    shows "continuous_on T g"
+proof -
+  have gTS: "g ` T = S"
+    using imf injf by force
+  have fU: "U \<subseteq> S \<Longrightarrow> (f ` U) = {x \<in> T. g x \<in> U}" for U
+    using imf injf by force
+  show ?thesis
+    apply (simp add: continuous_on_open [of T g] gTS)
+    apply (metis openin_imp_subset fU oo)
+    done
+qed
+
+lemma continuous_on_inverse_closed_map:
+  assumes contf: "continuous_on S f"
+      and imf: "f ` S = T"
+      and injf: "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
+      and oo: "\<And>U. closedin (subtopology euclidean S) U
+                    \<Longrightarrow> closedin (subtopology euclidean T) (f ` U)"
+    shows "continuous_on T g"
+proof -
+  have gTS: "g ` T = S"
+    using imf injf by force
+  have fU: "U \<subseteq> S \<Longrightarrow> (f ` U) = {x \<in> T. g x \<in> U}" for U
+    using imf injf by force
+  show ?thesis
+    apply (simp add: continuous_on_closed [of T g] gTS)
+    apply (metis closedin_imp_subset fU oo)
+    done
+qed
+
+lemma homeomorphism_injective_open_map:
+  assumes contf: "continuous_on S f"
+      and imf: "f ` S = T"
+      and injf: "inj_on f S"
+      and oo: "\<And>U. openin (subtopology euclidean S) U
+                    \<Longrightarrow> openin (subtopology euclidean T) (f ` U)"
+  obtains g where "homeomorphism S T f g"
+proof -
+  have "continuous_on T (inv_into S f)"
+    by (metis contf continuous_on_inverse_open_map imf injf inv_into_f_f oo)
+  then show ?thesis
+    apply (rule_tac g = "inv_into S f" in that)
+    using imf injf contf apply (auto simp: homeomorphism_def)
+    done
+qed
+
+lemma homeomorphism_injective_closed_map:
+  assumes contf: "continuous_on S f"
+      and imf: "f ` S = T"
+      and injf: "inj_on f S"
+      and oo: "\<And>U. closedin (subtopology euclidean S) U
+                    \<Longrightarrow> closedin (subtopology euclidean T) (f ` U)"
+  obtains g where "homeomorphism S T f g"
+proof -
+  have "continuous_on T (inv_into S f)"
+    by (metis contf continuous_on_inverse_closed_map imf injf inv_into_f_f oo)
+  then show ?thesis
+    apply (rule_tac g = "inv_into S f" in that)
+    using imf injf contf apply (auto simp: homeomorphism_def)
+    done
+qed
+
+lemma homeomorphism_imp_open_map:
+  assumes hom: "homeomorphism S T f g"
+      and oo: "openin (subtopology euclidean S) U"
+    shows "openin (subtopology euclidean T) (f ` U)"
+proof -
+  have [simp]: "f ` U = {y. y \<in> T \<and> g y \<in> U}"
+    using assms openin_subset
+    by (fastforce simp: homeomorphism_def rev_image_eqI)
+  have "continuous_on T g"
+    using hom homeomorphism_def by blast
+  moreover have "g ` T = S"
+    by (metis hom homeomorphism_def)
+  ultimately show ?thesis
+    by (simp add: continuous_on_open oo)
+qed
+
+lemma homeomorphism_imp_closed_map:
+  assumes hom: "homeomorphism S T f g"
+      and oo: "closedin (subtopology euclidean S) U"
+    shows "closedin (subtopology euclidean T) (f ` U)"
+proof -
+  have [simp]: "f ` U = {y. y \<in> T \<and> g y \<in> U}"
+    using assms closedin_subset
+    by (fastforce simp: homeomorphism_def rev_image_eqI)
+  have "continuous_on T g"
+    using hom homeomorphism_def by blast
+  moreover have "g ` T = S"
+    by (metis hom homeomorphism_def)
+  ultimately show ?thesis
+    by (simp add: continuous_on_closed oo)
+qed
+
+subsection\<open>"Isometry" (up to constant bounds) of injective linear map etc.\<close>
 
 lemma cauchy_isometric:
   assumes e: "e > 0"
@@ -8354,7 +8537,7 @@
       fix n
       assume "n\<ge>N"
       have "e * norm (x n - x N) \<le> norm (f (x n - x N))"
-        using subspace_sub[OF s, of "x n" "x N"]
+        using subspace_diff[OF s, of "x n" "x N"]
         using xs[THEN spec[where x=N]] and xs[THEN spec[where x=n]]
         using normf[THEN bspec[where x="x n - x N"]]
         by auto
diff -r 932cf444f2fe -r 27afe7af7379 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Sat May 21 07:08:59 2016 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Mon May 23 15:33:24 2016 +0100
@@ -236,6 +236,18 @@
   apply (simp_all add: algebra_simps)
   done
 
+lemma vector_add_divide_simps :
+  fixes v :: "'a :: real_vector"
+  shows "v + (b / z) *\<^sub>R w = (if z = 0 then v else (z *\<^sub>R v + b *\<^sub>R w) /\<^sub>R z)"
+        "a *\<^sub>R v + (b / z) *\<^sub>R w = (if z = 0 then a *\<^sub>R v else ((a * z) *\<^sub>R v + b *\<^sub>R w) /\<^sub>R z)"
+        "(a / z) *\<^sub>R v + w = (if z = 0 then w else (a *\<^sub>R v + z *\<^sub>R w) /\<^sub>R z)"
+        "(a / z) *\<^sub>R v + b *\<^sub>R w = (if z = 0 then b *\<^sub>R w else (a *\<^sub>R v + (b * z) *\<^sub>R w) /\<^sub>R z)"
+        "v - (b / z) *\<^sub>R w = (if z = 0 then v else (z *\<^sub>R v - b *\<^sub>R w) /\<^sub>R z)"
+        "a *\<^sub>R v - (b / z) *\<^sub>R w = (if z = 0 then a *\<^sub>R v else ((a * z) *\<^sub>R v - b *\<^sub>R w) /\<^sub>R z)"
+        "(a / z) *\<^sub>R v - w = (if z = 0 then -w else (a *\<^sub>R v - z *\<^sub>R w) /\<^sub>R z)"
+        "(a / z) *\<^sub>R v - b *\<^sub>R w = (if z = 0 then -b *\<^sub>R w else (a *\<^sub>R v - (b * z) *\<^sub>R w) /\<^sub>R z)"
+by (simp_all add: divide_inverse_commute scaleR_add_right real_vector.scale_right_diff_distrib)
+
 lemma real_vector_affinity_eq:
   fixes x :: "'a :: real_vector"
   assumes m0: "m \<noteq> 0"
@@ -769,6 +781,21 @@
     by (rule norm_minus_cancel)
   thus ?thesis by simp
 qed
+  
+lemma dist_add_cancel [simp]:
+  fixes a :: "'a::real_normed_vector"
+  shows "dist (a + b) (a + c) = dist b c"
+by (simp add: dist_norm)
+
+lemma dist_add_cancel2 [simp]:
+  fixes a :: "'a::real_normed_vector"
+  shows "dist (b + a) (c + a) = dist b c"
+by (simp add: dist_norm)
+
+lemma dist_scaleR [simp]:
+  fixes a :: "'a::real_normed_vector"
+  shows "dist (x *\<^sub>R a) (y *\<^sub>R a) = abs (x-y) * norm a"
+by (metis dist_norm norm_scaleR scaleR_left.diff)
 
 lemma norm_uminus_minus: "norm (-x - y :: 'a :: real_normed_vector) = norm (x + y)"
   by (subst (2) norm_minus_cancel[symmetric], subst minus_add_distrib) simp
diff -r 932cf444f2fe -r 27afe7af7379 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sat May 21 07:08:59 2016 +0200
+++ b/src/HOL/Set.thy	Mon May 23 15:33:24 2016 +0100
@@ -1934,6 +1934,14 @@
 lemma pairwise_singleton [simp]: "pairwise P {A}"
   by (simp add: pairwise_def)
 
+lemma pairwise_insert:
+   "pairwise r (insert x s) \<longleftrightarrow> (\<forall>y. y \<in> s \<and> y \<noteq> x \<longrightarrow> r x y \<and> r y x) \<and> pairwise r s"
+by (force simp: pairwise_def)
+
+lemma pairwise_image:
+   "pairwise r (f ` s) \<longleftrightarrow> pairwise (\<lambda>x y. (f x \<noteq> f y) \<longrightarrow> r (f x) (f y)) s"
+by (force simp: pairwise_def)
+
 lemma Int_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> False) \<Longrightarrow> A \<inter> B = {}"
   by blast
 
diff -r 932cf444f2fe -r 27afe7af7379 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Sat May 21 07:08:59 2016 +0200
+++ b/src/HOL/Set_Interval.thy	Mon May 23 15:33:24 2016 +0100
@@ -1168,19 +1168,18 @@
 by (rule finite_same_card_bij) auto
 
 lemma bij_betw_iff_card:
-  assumes FIN: "finite A" and FIN': "finite B"
-  shows BIJ: "(\<exists>f. bij_betw f A B) \<longleftrightarrow> (card A = card B)"
-using assms
-proof(auto simp add: bij_betw_same_card)
-  assume *: "card A = card B"
-  obtain f where "bij_betw f A {0 ..< card A}"
-  using FIN ex_bij_betw_finite_nat by blast
+  assumes "finite A" "finite B"
+  shows "(\<exists>f. bij_betw f A B) \<longleftrightarrow> (card A = card B)"
+proof
+  assume "card A = card B"
+  moreover obtain f where "bij_betw f A {0 ..< card A}"
+    using assms ex_bij_betw_finite_nat by blast
   moreover obtain g where "bij_betw g {0 ..< card B} B"
-  using FIN' ex_bij_betw_nat_finite by blast
+    using assms ex_bij_betw_nat_finite by blast
   ultimately have "bij_betw (g o f) A B"
-  using * by (auto simp add: bij_betw_trans)
+    by (auto simp: bij_betw_trans)
   thus "(\<exists>f. bij_betw f A B)" by blast
-qed
+qed (auto simp: bij_betw_same_card)
 
 lemma inj_on_iff_card_le:
   assumes FIN: "finite A" and FIN': "finite B"