lots of new theorems about differentiable_on, retracts, ANRs, etc.

--- a/src/HOL/Complete_Lattices.thy	Tue Jul 12 22:54:37 2016 +0200
+++ b/src/HOL/Complete_Lattices.thy	Wed Jul 13 17:14:17 2016 +0100
@@ -1128,6 +1128,8 @@
 lemma Union_mono: "A \<subseteq> B \<Longrightarrow> \<Union>A \<subseteq> \<Union>B"
   by (fact Sup_subset_mono)
 
+lemma Union_subsetI: "(\<And>x. x \<in> A \<Longrightarrow> \<exists>y. y \<in> B \<and> x \<subseteq> y) \<Longrightarrow> \<Union>A \<subseteq> \<Union>B"
+  by blast
 
 subsubsection \<open>Unions of families\<close>
 

--- a/src/HOL/Deriv.thy	Tue Jul 12 22:54:37 2016 +0200
+++ b/src/HOL/Deriv.thy	Wed Jul 13 17:14:17 2016 +0100
@@ -82,6 +82,9 @@
 lemma has_derivative_ident[derivative_intros, simp]: "((\<lambda>x. x) has_derivative (\<lambda>x. x)) F"
   by (simp add: has_derivative_def)
 
+lemma has_derivative_id [derivative_intros, simp]: "(id has_derivative id) (at a)"
+  by (metis eq_id_iff has_derivative_ident)
+
 lemma has_derivative_const[derivative_intros, simp]: "((\<lambda>x. c) has_derivative (\<lambda>x. 0)) F"
   by (simp add: has_derivative_def)
 

--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Tue Jul 12 22:54:37 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Wed Jul 13 17:14:17 2016 +0100
@@ -2170,7 +2170,7 @@
     shows  "\<lbrakk> locally compact s; t retract_of s\<rbrakk> \<Longrightarrow> locally compact t"
   by (metis locally_compact_closedin closedin_retract)
 
-lemma retract_of_times:
+lemma retract_of_Times:
    "\<lbrakk>s retract_of s'; t retract_of t'\<rbrakk> \<Longrightarrow> (s \<times> t) retract_of (s' \<times> t')"
 apply (simp add: retract_of_def retraction_def Sigma_mono, clarify)
 apply (rename_tac f g)
@@ -2188,6 +2188,18 @@
 apply (rule conjI continuous_intros | erule continuous_on_subset | force simp: image_subset_iff)+
 done
 
+lemma retract_of_locally_connected:
+  assumes "locally connected T" "S retract_of T"
+    shows "locally connected S"
+  using assms
+  by (auto simp: retract_of_def retraction intro!: retraction_imp_quotient_map elim!: locally_connected_quotient_image)
+
+lemma retract_of_locally_path_connected:
+  assumes "locally path_connected T" "S retract_of T"
+    shows "locally path_connected S"
+  using assms
+  by (auto simp: retract_of_def retraction intro!: retraction_imp_quotient_map elim!: locally_path_connected_quotient_image)
+
 subsection\<open>Borsuk-style characterization of separation\<close>
 
 lemma continuous_on_Borsuk_map:
@@ -3352,4 +3364,251 @@
   shows "\<lbrakk>closed S; closed T; ANR S; ANR T; ANR (S \<inter> T)\<rbrakk> \<Longrightarrow> ANR (S \<union> T)"
 by (simp add: ANR_closed_Un_local closedin_def diff_eq open_Compl openin_open_Int)
 
+lemma ANR_openin:
+  fixes S :: "'a::euclidean_space set"
+  assumes "ANR T" and opeTS: "openin (subtopology euclidean T) S"
+  shows "ANR S"
+proof (clarsimp simp only: ANR_eq_absolute_neighbourhood_extensor)
+  fix f :: "'a \<times> real \<Rightarrow> 'a" and U C
+  assume contf: "continuous_on C f" and fim: "f ` C \<subseteq> S"
+     and cloUC: "closedin (subtopology euclidean U) C"
+  have "f ` C \<subseteq> T"
+    using fim opeTS openin_imp_subset by blast
+  obtain W g where "C \<subseteq> W"
+               and UW: "openin (subtopology euclidean U) W"
+               and contg: "continuous_on W g"
+               and gim: "g ` W \<subseteq> T"
+               and geq: "\<And>x. x \<in> C \<Longrightarrow> g x = f x"
+    apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR T\<close> contf \<open>f ` C \<subseteq> T\<close> cloUC])
+    using fim by auto
+  show "\<exists>V g. C \<subseteq> V \<and> openin (subtopology euclidean U) V \<and> continuous_on V g \<and> g ` V \<subseteq> S \<and> (\<forall>x\<in>C. g x = f x)"
+  proof (intro exI conjI)
+    show "C \<subseteq> {x \<in> W. g x \<in> S}"
+      using \<open>C \<subseteq> W\<close> fim geq by blast
+    show "openin (subtopology euclidean U) {x \<in> W. g x \<in> S}"
+      by (metis (mono_tags, lifting) UW contg continuous_openin_preimage gim opeTS openin_trans)
+    show "continuous_on {x \<in> W. g x \<in> S} g"
+      by (blast intro: continuous_on_subset [OF contg])
+    show "g ` {x \<in> W. g x \<in> S} \<subseteq> S"
+      using gim by blast
+    show "\<forall>x\<in>C. g x = f x"
+      using geq by blast
+  qed
+qed
+
+lemma ENR_openin:
+    fixes S :: "'a::euclidean_space set"
+    assumes "ENR T" and opeTS: "openin (subtopology euclidean T) S"
+    shows "ENR S"
+  using assms apply (simp add: ENR_ANR)
+  using ANR_openin locally_open_subset by blast
+
+lemma ANR_neighborhood_retract:
+    fixes S :: "'a::euclidean_space set"
+    assumes "ANR U" "S retract_of T" "openin (subtopology euclidean U) T"
+    shows "ANR S"
+  using ANR_openin ANR_retract_of_ANR assms by blast
+
+lemma ENR_neighborhood_retract:
+    fixes S :: "'a::euclidean_space set"
+    assumes "ENR U" "S retract_of T" "openin (subtopology euclidean U) T"
+    shows "ENR S"
+  using ENR_openin ENR_retract_of_ENR assms by blast
+
+lemma ANR_rel_interior:
+  fixes S :: "'a::euclidean_space set"
+  shows "ANR S \<Longrightarrow> ANR(rel_interior S)"
+   by (blast intro: ANR_openin openin_set_rel_interior)
+
+lemma ANR_delete:
+  fixes S :: "'a::euclidean_space set"
+  shows "ANR S \<Longrightarrow> ANR(S - {a})"
+   by (blast intro: ANR_openin openin_delete openin_subtopology_self)
+
+lemma ENR_rel_interior:
+  fixes S :: "'a::euclidean_space set"
+  shows "ENR S \<Longrightarrow> ENR(rel_interior S)"
+   by (blast intro: ENR_openin openin_set_rel_interior)
+
+lemma ENR_delete:
+  fixes S :: "'a::euclidean_space set"
+  shows "ENR S \<Longrightarrow> ENR(S - {a})"
+   by (blast intro: ENR_openin openin_delete openin_subtopology_self)
+
+lemma open_imp_ENR: "open S \<Longrightarrow> ENR S"
+    using ENR_def by blast
+
+lemma open_imp_ANR:
+    fixes S :: "'a::euclidean_space set"
+    shows "open S \<Longrightarrow> ANR S"
+  by (simp add: ENR_imp_ANR open_imp_ENR)
+
+lemma ANR_ball [iff]:
+    fixes a :: "'a::euclidean_space"
+    shows "ANR(ball a r)"
+  by (simp add: convex_imp_ANR)
+
+lemma ENR_ball [iff]: "ENR(ball a r)"
+  by (simp add: open_imp_ENR)
+
+lemma AR_ball [simp]:
+    fixes a :: "'a::euclidean_space"
+    shows "AR(ball a r) \<longleftrightarrow> 0 < r"
+  by (auto simp: AR_ANR convex_imp_contractible)
+
+lemma ANR_cball [iff]:
+    fixes a :: "'a::euclidean_space"
+    shows "ANR(cball a r)"
+  by (simp add: convex_imp_ANR)
+
+lemma ENR_cball:
+    fixes a :: "'a::euclidean_space"
+    shows "ENR(cball a r)"
+  using ENR_convex_closed by blast
+
+lemma AR_cball [simp]:
+    fixes a :: "'a::euclidean_space"
+    shows "AR(cball a r) \<longleftrightarrow> 0 \<le> r"
+  by (auto simp: AR_ANR convex_imp_contractible)
+
+lemma ANR_box [iff]:
+    fixes a :: "'a::euclidean_space"
+    shows "ANR(cbox a b)" "ANR(box a b)"
+  by (auto simp: convex_imp_ANR open_imp_ANR)
+
+lemma ENR_box [iff]:
+    fixes a :: "'a::euclidean_space"
+    shows "ENR(cbox a b)" "ENR(box a b)"
+apply (simp add: ENR_convex_closed closed_cbox)
+by (simp add: open_box open_imp_ENR)
+
+lemma AR_box [simp]:
+    "AR(cbox a b) \<longleftrightarrow> cbox a b \<noteq> {}" "AR(box a b) \<longleftrightarrow> box a b \<noteq> {}"
+  by (auto simp: AR_ANR convex_imp_contractible)
+
+lemma ANR_interior:
+     fixes S :: "'a::euclidean_space set"
+     shows "ANR(interior S)"
+  by (simp add: open_imp_ANR)
+
+lemma ENR_interior:
+     fixes S :: "'a::euclidean_space set"
+     shows "ENR(interior S)"
+  by (simp add: open_imp_ENR)
+
+lemma AR_imp_contractible:
+    fixes S :: "'a::euclidean_space set"
+    shows "AR S \<Longrightarrow> contractible S"
+  by (simp add: AR_ANR)
+
+lemma ENR_imp_locally_compact:
+    fixes S :: "'a::euclidean_space set"
+    shows "ENR S \<Longrightarrow> locally compact S"
+  by (simp add: ENR_ANR)
+
+lemma ANR_imp_locally_path_connected:
+  fixes S :: "'a::euclidean_space set"
+  assumes "ANR S"
+    shows "locally path_connected S"
+proof -
+  obtain U and T :: "('a \<times> real) set"
+     where "convex U" "U \<noteq> {}"
+       and UT: "closedin (subtopology euclidean U) T"
+       and "S homeomorphic T"
+    apply (rule homeomorphic_closedin_convex [of S])
+    using aff_dim_le_DIM [of S] apply auto
+    done
+  have "locally path_connected T"
+    by (meson ANR_imp_absolute_neighbourhood_retract \<open>S homeomorphic T\<close> \<open>closedin (subtopology euclidean U) T\<close> \<open>convex U\<close> assms convex_imp_locally_path_connected locally_open_subset retract_of_locally_path_connected)
+  then have S: "locally path_connected S"
+      if "openin (subtopology euclidean U) V" "T retract_of V" "U \<noteq> {}" for V
+    using \<open>S homeomorphic T\<close> homeomorphic_locally homeomorphic_path_connectedness by blast
+  show ?thesis
+    using assms
+    apply (clarsimp simp: ANR_def)
+    apply (drule_tac x=U in spec)
+    apply (drule_tac x=T in spec)
+    using \<open>S homeomorphic T\<close> \<open>U \<noteq> {}\<close> UT  apply (blast intro: S)
+    done
+qed
+
+lemma ANR_imp_locally_connected:
+  fixes S :: "'a::euclidean_space set"
+  assumes "ANR S"
+    shows "locally connected S"
+using locally_path_connected_imp_locally_connected ANR_imp_locally_path_connected assms by auto
+
+lemma AR_imp_locally_path_connected:
+  fixes S :: "'a::euclidean_space set"
+  assumes "AR S"
+    shows "locally path_connected S"
+by (simp add: ANR_imp_locally_path_connected AR_imp_ANR assms)
+
+lemma AR_imp_locally_connected:
+  fixes S :: "'a::euclidean_space set"
+  assumes "AR S"
+    shows "locally connected S"
+using ANR_imp_locally_connected AR_ANR assms by blast
+
+lemma ENR_imp_locally_path_connected:
+  fixes S :: "'a::euclidean_space set"
+  assumes "ENR S"
+    shows "locally path_connected S"
+by (simp add: ANR_imp_locally_path_connected ENR_imp_ANR assms)
+
+lemma ENR_imp_locally_connected:
+  fixes S :: "'a::euclidean_space set"
+  assumes "ENR S"
+    shows "locally connected S"
+using ANR_imp_locally_connected ENR_ANR assms by blast
+
+lemma ANR_Times:
+  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+  assumes "ANR S" "ANR T" shows "ANR(S \<times> T)"
+proof (clarsimp simp only: ANR_eq_absolute_neighbourhood_extensor)
+  fix f :: " ('a \<times> 'b) \<times> real \<Rightarrow> 'a \<times> 'b" and U C
+  assume "continuous_on C f" and fim: "f ` C \<subseteq> S \<times> T"
+     and cloUC: "closedin (subtopology euclidean U) C"
+  have contf1: "continuous_on C (fst \<circ> f)"
+    by (simp add: \<open>continuous_on C f\<close> continuous_on_fst)
+  obtain W1 g where "C \<subseteq> W1"
+               and UW1: "openin (subtopology euclidean U) W1"
+               and contg: "continuous_on W1 g"
+               and gim: "g ` W1 \<subseteq> S"
+               and geq: "\<And>x. x \<in> C \<Longrightarrow> g x = (fst \<circ> f) x"
+    apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR S\<close> contf1 _ cloUC])
+    using fim apply auto
+    done
+  have contf2: "continuous_on C (snd \<circ> f)"
+    by (simp add: \<open>continuous_on C f\<close> continuous_on_snd)
+  obtain W2 h where "C \<subseteq> W2"
+               and UW2: "openin (subtopology euclidean U) W2"
+               and conth: "continuous_on W2 h"
+               and him: "h ` W2 \<subseteq> T"
+               and heq: "\<And>x. x \<in> C \<Longrightarrow> h x = (snd \<circ> f) x"
+    apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR T\<close> contf2 _ cloUC])
+    using fim apply auto
+    done
+  show "\<exists>V g. C \<subseteq> V \<and>
+               openin (subtopology euclidean U) V \<and>
+               continuous_on V g \<and> g ` V \<subseteq> S \<times> T \<and> (\<forall>x\<in>C. g x = f x)"
+  proof (intro exI conjI)
+    show "C \<subseteq> W1 \<inter> W2"
+      by (simp add: \<open>C \<subseteq> W1\<close> \<open>C \<subseteq> W2\<close>)
+    show "openin (subtopology euclidean U) (W1 \<inter> W2)"
+      by (simp add: UW1 UW2 openin_Int)
+    show  "continuous_on (W1 \<inter> W2) (\<lambda>x. (g x, h x))"
+      by (metis (no_types) contg conth continuous_on_Pair continuous_on_subset inf_commute inf_le1)
+    show  "(\<lambda>x. (g x, h x)) ` (W1 \<inter> W2) \<subseteq> S \<times> T"
+      using gim him by blast
+    show  "(\<forall>x\<in>C. (g x, h x) = f x)"
+      using geq heq by auto
+  qed
+qed
+
+lemma AR_Times:
+  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+  assumes "AR S" "AR T" shows "AR(S \<times> T)"
+using assms by (simp add: AR_ANR ANR_Times contractible_Times)
+
 end

--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Jul 12 22:54:37 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Jul 13 17:14:17 2016 +0100
@@ -62,7 +62,7 @@
   also have "\<dots> \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y \<in> S. f x - f y = 0 \<longrightarrow> x - y = 0)"
     by simp
   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])
+    by (simp add: linear_diff[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_diff[of S] by auto
   finally show ?thesis .
@@ -218,7 +218,7 @@
     from B(3) x y have x': "x \<in> span B" and y': "y \<in> span B"
       by blast+
     from gxy have th0: "g (x - y) = 0"
-      by (simp add: linear_sub[OF g(1)])
+      by (simp add: linear_diff[OF g(1)])
     have th1: "x - y \<in> span B" using x' y'
       by (metis span_sub)
     have "x = y" using g0[OF th1 th0] by simp
@@ -1104,6 +1104,9 @@
 lemma cone_Inter[intro]: "\<forall>s\<in>f. cone s \<Longrightarrow> cone (\<Inter>f)"
   unfolding cone_def by auto
 
+lemma subspace_imp_cone: "subspace S \<Longrightarrow> cone S"
+  by (simp add: cone_def subspace_mul)
+
 
 subsubsection \<open>Conic hull\<close>
 
@@ -2969,6 +2972,11 @@
   then show ?thesis by auto
 qed
 
+lemma aff_dim_negative_iff [simp]:
+  fixes S :: "'n::euclidean_space set"
+  shows "aff_dim S < 0 \<longleftrightarrow>S = {}"
+by (metis aff_dim_empty aff_dim_geq diff_0 eq_iff zle_diff1_eq)
+
 lemma affine_independent_card_dim_diffs:
   fixes S :: "'a :: euclidean_space set"
   assumes "~ affine_dependent S" "a \<in> S"
@@ -3667,6 +3675,10 @@
   apply blast
   done
 
+lemma openin_set_rel_interior:
+   "openin (subtopology euclidean S) (rel_interior S)"
+by (rule openin_subset_trans [OF openin_rel_interior rel_interior_subset hull_subset])
+
 lemma affine_rel_open:
   fixes S :: "'n::euclidean_space set"
   assumes "affine S"
@@ -3814,6 +3826,40 @@
    "openin(subtopology euclidean (affine hull s)) s \<Longrightarrow> rel_interior s = s"
 by (simp add: rel_interior_eq)
 
+lemma rel_interior_affine:
+  fixes S :: "'n::euclidean_space set"
+  shows  "affine S \<Longrightarrow> rel_interior S = S"
+using affine_rel_open rel_open_def by auto
+
+lemma rel_interior_eq_closure:
+  fixes S :: "'n::euclidean_space set"
+  shows "rel_interior S = closure S \<longleftrightarrow> affine S"
+proof (cases "S = {}")
+  case True
+ then show ?thesis
+    by auto
+next
+  case False show ?thesis
+  proof
+    assume eq: "rel_interior S = closure S"
+    have "S = {} \<or> S = affine hull S"
+      apply (rule connected_clopen [THEN iffD1, rule_format])
+       apply (simp add: affine_imp_convex convex_connected)
+      apply (rule conjI)
+       apply (metis eq closure_subset openin_rel_interior rel_interior_subset subset_antisym)
+      apply (metis closed_subset closure_subset_eq eq hull_subset rel_interior_subset)
+      done
+    with False have "affine hull S = S"
+      by auto
+    then show "affine S"
+      by (metis affine_hull_eq)
+  next
+    assume "affine S"
+    then show "rel_interior S = closure S"
+      by (simp add: rel_interior_affine affine_closed)
+  qed
+qed
+
 
 subsubsection\<open>Relative interior preserves under linear transformations\<close>
 
@@ -3905,7 +3951,7 @@
       from y have "norm (x-y) \<le> e1 * e2"
         using cball_def[of x e] dist_norm[of x y] e_def by auto
       moreover have "f x - f y = f (x - y)"
-        using assms linear_sub[of f x y] linear_conv_bounded_linear[of f] by auto
+        using assms linear_diff[of f x y] linear_conv_bounded_linear[of f] by auto
       moreover have "e1 * norm (f (x-y)) \<le> norm (x - y)"
         using e1 by auto
       ultimately have "e1 * norm ((f x)-(f y)) \<le> e1 * e2"
@@ -3949,7 +3995,7 @@
       with y have "norm (f x - f xy) \<le> e1 * e2"
         using cball_def[of "f x" e] dist_norm[of "f x" y] e_def by auto
       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
+        using assms linear_diff[of f x xy] linear_conv_bounded_linear[of f] by auto
       moreover have *: "x - xy \<in> span S"
         using subspace_diff[of "span S" x xy] subspace_span \<open>x \<in> S\<close> xy
           affine_hull_subset_span[of S] span_inc
@@ -7854,6 +7900,13 @@
 lemma rel_frontier_empty [simp]: "rel_frontier {} = {}"
   by (simp add: rel_frontier_def)
 
+lemma rel_frontier_eq_empty:
+    fixes S :: "'n::euclidean_space set"
+    shows "rel_frontier S = {} \<longleftrightarrow> affine S"
+  apply (simp add: rel_frontier_def)
+  apply (simp add: rel_interior_eq_closure [symmetric])
+  using rel_interior_subset_closure by blast
+  
 lemma rel_frontier_sing [simp]:
     fixes a :: "'n::euclidean_space"
     shows "rel_frontier {a} = {}"
@@ -7873,7 +7926,12 @@
     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:
+lemma rel_frontier_translation:
+  fixes a :: "'a::euclidean_space"
+  shows "rel_frontier((\<lambda>x. a + x) ` S) = (\<lambda>x. a + x) ` (rel_frontier S)"
+by (simp add: rel_frontier_def translation_diff rel_interior_translation closure_translation)
+
+lemma closed_affine_hull [iff]:
   fixes S :: "'n::euclidean_space set"
   shows "closed (affine hull S)"
   by (metis affine_affine_hull affine_closed)
@@ -7888,7 +7946,7 @@
   shows "affine hull S = UNIV \<Longrightarrow> rel_frontier S = frontier S"
 by (simp add: frontier_def rel_frontier_def rel_interior_interior)
 
-lemma closed_rel_frontier:
+lemma closed_rel_frontier [iff]:
   fixes S :: "'n::euclidean_space set"
   shows "closed (rel_frontier S)"
 proof -
@@ -10999,6 +11057,9 @@
 lemma subspace_hyperplane: "subspace {x. a \<bullet> x = 0}"
   by (simp add: subspace_def inner_right_distrib)
 
+lemma subspace_hyperplane2: "subspace {x. x \<bullet> a = 0}"
+  by (simp add: inner_commute inner_right_distrib subspace_def)
+
 lemma special_hyperplane_span:
   fixes S :: "'n::euclidean_space set"
   assumes "k \<in> Basis"
@@ -11990,7 +12051,7 @@
 lemma orthogonal_to_span:
   assumes a: "a \<in> span S" and x: "\<And>y. y \<in> S \<Longrightarrow> orthogonal x y"
     shows "orthogonal x a"
-apply (rule CollectD, rule span_induct [OF a subspace_orthogonal_to_vector])
+apply (rule span_induct [OF a subspace_orthogonal_to_vector])
 apply (simp add: x)
 done
 
@@ -12068,7 +12129,7 @@
   show ?thesis
     apply (rule_tac U=U in that)
      apply (simp add: \<open>pairwise orthogonal (S \<union> U)\<close>)
-    by (metis \<open>span (S \<union> U) = span (S \<union> B)\<close> \<open>span B = span T\<close> span_union)
+    by (metis \<open>span (S \<union> U) = span (S \<union> B)\<close> \<open>span B = span T\<close> span_Un)
 qed
 
 corollary orthogonal_extension_strong:
@@ -12083,7 +12144,7 @@
     apply (rule_tac U = "U - (insert 0 S)" in that)
       apply blast
      apply (force simp: pairwise_def)
-    apply (metis (no_types, lifting) Un_Diff_cancel span_insert_0 span_union)
+    apply (metis (no_types, lifting) Un_Diff_cancel span_insert_0 span_Un)
   done
 qed
 
@@ -12306,11 +12367,11 @@
     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])
+      by (force simp: linear_diff [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)
+      by (force simp: linear_diff [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"
@@ -12368,10 +12429,10 @@
         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
+      with \<open>dim T = n\<close>  \<open>subspace T\<close> y show ?thesis
         apply (rule_tac x="span(insert y T)" in exI)
-        apply (auto simp: subspace_span dim_insert)
-        done
+        apply (auto simp: dim_insert)
+        using span_eq by blast
     qed
   qed
   with that show ?thesis by blast

--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Jul 12 22:54:37 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Jul 13 17:14:17 2016 +0100
@@ -220,6 +220,71 @@
    using assms has_derivative_transform_within unfolding differentiable_def
    by blast
 
+lemma differentiable_on_ident [simp, derivative_intros]: "(\<lambda>x. x) differentiable_on S"
+  by (simp add: differentiable_at_imp_differentiable_on)
+
+lemma differentiable_on_id [simp, derivative_intros]: "id differentiable_on S"
+  by (simp add: id_def)
+
+lemma differentiable_on_compose:
+   "\<lbrakk>g differentiable_on S; f differentiable_on (g ` S)\<rbrakk> \<Longrightarrow> (\<lambda>x. f (g x)) differentiable_on S"
+by (simp add: differentiable_in_compose differentiable_on_def)
+
+lemma bounded_linear_imp_differentiable_on: "bounded_linear f \<Longrightarrow> f differentiable_on S"
+  by (simp add: differentiable_on_def bounded_linear_imp_differentiable)
+
+lemma linear_imp_differentiable_on:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
+  shows "linear f \<Longrightarrow> f differentiable_on S"
+by (simp add: differentiable_on_def linear_imp_differentiable)
+
+lemma differentiable_on_minus [simp, derivative_intros]:
+   "f differentiable_on S \<Longrightarrow> (\<lambda>z. -(f z)) differentiable_on S"
+by (simp add: differentiable_on_def)
+
+lemma differentiable_on_add [simp, derivative_intros]:
+   "\<lbrakk>f differentiable_on S; g differentiable_on S\<rbrakk> \<Longrightarrow> (\<lambda>z. f z + g z) differentiable_on S"
+by (simp add: differentiable_on_def)
+
+lemma differentiable_on_diff [simp, derivative_intros]:
+   "\<lbrakk>f differentiable_on S; g differentiable_on S\<rbrakk> \<Longrightarrow> (\<lambda>z. f z - g z) differentiable_on S"
+by (simp add: differentiable_on_def)
+
+lemma differentiable_on_inverse [simp, derivative_intros]:
+  fixes f :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
+  shows "f differentiable_on S \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> f x \<noteq> 0) \<Longrightarrow> (\<lambda>x. inverse (f x)) differentiable_on S"
+by (simp add: differentiable_on_def)
+
+lemma differentiable_on_scaleR [derivative_intros, simp]:
+   "\<lbrakk>f differentiable_on S; g differentiable_on S\<rbrakk> \<Longrightarrow> (\<lambda>x. f x *\<^sub>R g x) differentiable_on S"
+  unfolding differentiable_on_def
+  by (blast intro: differentiable_scaleR)
+
+lemma has_derivative_sqnorm_at [derivative_intros, simp]:
+   "((\<lambda>x. (norm x)\<^sup>2) has_derivative (\<lambda>x. 2 *\<^sub>R (a \<bullet> x))) (at a)"
+using has_derivative_bilinear_at [of id id a id id "op  \<bullet>"]
+by (auto simp: inner_commute dot_square_norm bounded_bilinear_inner)
+
+lemma differentiable_sqnorm_at [derivative_intros, simp]:
+  fixes a :: "'a :: {real_normed_vector,real_inner}"
+  shows "(\<lambda>x. (norm x)\<^sup>2) differentiable (at a)"
+by (force simp add: differentiable_def intro: has_derivative_sqnorm_at)
+
+lemma differentiable_on_sqnorm [derivative_intros, simp]:
+  fixes S :: "'a :: {real_normed_vector,real_inner} set"
+  shows "(\<lambda>x. (norm x)\<^sup>2) differentiable_on S"
+by (simp add: differentiable_at_imp_differentiable_on)
+
+lemma differentiable_norm_at [derivative_intros, simp]:
+  fixes a :: "'a :: {real_normed_vector,real_inner}"
+  shows "a \<noteq> 0 \<Longrightarrow> norm differentiable (at a)"
+using differentiableI has_derivative_norm by blast
+
+lemma differentiable_on_norm [derivative_intros, simp]:
+  fixes S :: "'a :: {real_normed_vector,real_inner} set"
+  shows "0 \<notin> S \<Longrightarrow> norm differentiable_on S"
+by (metis differentiable_at_imp_differentiable_on differentiable_norm_at)
+
 
 subsection \<open>Frechet derivative and Jacobian matrix\<close>
 
@@ -1075,7 +1140,7 @@
      using assms by (auto simp: fun_diff_def)
   from differentiable_bound_segment[OF assms(1) g B] \<open>x0 \<in> S\<close>
   show ?thesis
-    by (simp add: g_def field_simps linear_sub[OF has_derivative_linear[OF f']])
+    by (simp add: g_def field_simps linear_diff[OF has_derivative_linear[OF f']])
 qed
 
 text \<open>In particular.\<close>
@@ -1288,7 +1353,7 @@
     and "g (f x) = x"
     and "open t"
     and "f x \<in> t"
-    and "\<forall>y\<in>t. f (g y) = y"
+    and "\<forall>y\<in>t. f (g y) = y"    
   shows "(g has_derivative g') (at (f x))"
   apply (rule has_derivative_inverse_basic)
   using assms

--- a/src/HOL/Multivariate_Analysis/Determinants.thy	Tue Jul 12 22:54:37 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Wed Jul 13 17:14:17 2016 +0100
@@ -1081,7 +1081,7 @@
   unfolding orthogonal_transformation
   apply (rule iffI)
   apply clarify
-  apply (clarsimp simp add: linear_0 linear_sub[symmetric] dist_norm)
+  apply (clarsimp simp add: linear_0 linear_diff[symmetric] dist_norm)
   apply (rule conjI)
   apply (rule isometry_linear)
   apply simp

--- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Jul 12 22:54:37 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Jul 13 17:14:17 2016 +0100
@@ -1254,7 +1254,7 @@
         next
           assume as': "k  = cbox a b"
           show ?thesis
-            using as' k' q(5) x' by blast 
+            using as' k' q(5) x' by blast
         next
           assume as': "k' = cbox a b"
           show ?thesis
@@ -1739,7 +1739,7 @@
   unfolding integrable_on_def integral_def by (metis (mono_tags, lifting) someI_ex)
 
 lemma not_integrable_integral: "~ f integrable_on i \<Longrightarrow> integral i f = 0"
-  unfolding integrable_on_def integral_def by blast 
+  unfolding integrable_on_def integral_def by blast
 
 lemma has_integral_integrable[intro]: "(f has_integral i) s \<Longrightarrow> f integrable_on s"
   unfolding integrable_on_def by auto
@@ -2559,7 +2559,7 @@
   "(f has_integral k) s \<Longrightarrow> (g has_integral l) s \<Longrightarrow>
     ((\<lambda>x. f x - g x) has_integral (k - l)) s"
   using has_integral_add[OF _ has_integral_neg, of f k s g l]
-  by (auto simp: algebra_simps) 
+  by (auto simp: algebra_simps)
 
 lemma integral_0 [simp]:
   "integral s (\<lambda>x::'n::euclidean_space. 0::'m::real_normed_vector) = 0"
@@ -5370,7 +5370,7 @@
   shows "negligible s"
   using assms by (induct s) auto
 
-lemma negligible_unions[intro]:
+lemma negligible_Union[intro]:
   assumes "finite s"
     and "\<forall>t\<in>s. negligible t"
   shows "negligible(\<Union>s)"
@@ -5456,7 +5456,7 @@
   then show ?thesis
     apply -
     apply (rule negligible_subset[of ?A])
-    apply (rule negligible_unions[OF finite_imageI])
+    apply (rule negligible_Union[OF finite_imageI])
     apply auto
     done
 qed
@@ -8979,7 +8979,7 @@
   assumes "negligible (A \<inter> B)" "f integrable_on A" "f integrable_on B"
   shows   "f integrable_on (A \<union> B)"
 proof -
-  from assms obtain y z where "(f has_integral y) A" "(f has_integral z) B" 
+  from assms obtain y z where "(f has_integral y) A" "(f has_integral z) B"
      by (auto simp: integrable_on_def)
   from has_integral_union[OF this assms(1)] show ?thesis by (auto simp: integrable_on_def)
 qed
@@ -8999,7 +8999,7 @@
 proof -
   note * = has_integral_restrict_univ[symmetric, of f]
   have **: "negligible (\<Union>((\<lambda>(a,b). a \<inter> b) ` {(a,b). a \<in> t \<and> b \<in> {y. y \<in> t \<and> a \<noteq> y}}))"
-    apply (rule negligible_unions)
+    apply (rule negligible_Union)
     apply (rule finite_imageI)
     apply (rule finite_subset[of _ "t \<times> t"])
     defer
@@ -12254,7 +12254,7 @@
   assumes cont [continuous_intros]: "continuous_on {a..b} f" "continuous_on {a..b} g"
   assumes deriv: "\<And>x. x\<in>{a<..<b} - s \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
                  "\<And>x. x\<in>{a<..<b} - s \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
-  assumes int: "((\<lambda>x. prod (f x) (g' x)) has_integral 
+  assumes int: "((\<lambda>x. prod (f x) (g' x)) has_integral
                   (prod (f b) (g b) - prod (f a) (g a) - y)) {a..b}"
   shows   "((\<lambda>x. prod (f' x) (g x)) has_integral y) {a..b}"
 proof -
@@ -12720,7 +12720,7 @@
 
 subsection \<open>Definite integrals for exponential and power function\<close>
 
-lemma has_integral_exp_minus_to_infinity: 
+lemma has_integral_exp_minus_to_infinity:
   assumes a: "a > 0"
   shows   "((\<lambda>x::real. exp (-a*x)) has_integral exp (-a*c)/a) {c..}"
 proof -
@@ -12728,7 +12728,7 @@
 
   {
     fix k :: nat assume k: "of_nat k \<ge> c"
-    from k a 
+    from k a
       have "((\<lambda>x. exp (-a*x)) has_integral (-exp (-a*real k)/a - (-exp (-a*c)/a))) {c..real k}"
       by (intro fundamental_theorem_of_calculus)
          (auto intro!: derivative_eq_intros
@@ -12738,7 +12738,7 @@
   } note has_integral_f = this
 
   have [simp]: "f k = (\<lambda>_. 0)" if "of_nat k < c" for k using that by (auto simp: fun_eq_iff f_def)
-  have integral_f: "integral {c..} (f k) = 
+  have integral_f: "integral {c..} (f k) =
                       (if real k \<ge> c then exp (-a*c)/a - exp (-a*real k)/a else 0)"
     for k using integral_unique[OF has_integral_f[of k]] by simp
 
@@ -12769,8 +12769,8 @@
       case False
       hence "abs (integral {c..} (f k)) = abs (exp (- (a * c)) / a - exp (- (a * real k)) / a)"
         by (simp add: integral_f)
-      also have "abs (exp (- (a * c)) / a - exp (- (a * real k)) / a) = 
-                   exp (- (a * c)) / a - exp (- (a * real k)) / a" 
+      also have "abs (exp (- (a * c)) / a - exp (- (a * real k)) / a) =
+                   exp (- (a * c)) / a - exp (- (a * real k)) / a"
         using False a by (intro abs_of_nonneg) (simp_all add: field_simps)
       also have "\<dots> \<le> exp (- a * c) / a" using a by simp
       finally show ?thesis .
@@ -12784,7 +12784,7 @@
   hence "eventually (\<lambda>k. exp (-a*c)/a - exp (-a * of_nat k)/a = integral {c..} (f k)) sequentially"
     by eventually_elim (simp add: integral_f)
   moreover have "(\<lambda>k. exp (-a*c)/a - exp (-a * of_nat k)/a) \<longlonglongrightarrow> exp (-a*c)/a - 0/a"
-    by (intro tendsto_intros filterlim_compose[OF exp_at_bot] 
+    by (intro tendsto_intros filterlim_compose[OF exp_at_bot]
           filterlim_tendsto_neg_mult_at_bot[OF tendsto_const] filterlim_real_sequentially)+
        (insert a, simp_all)
   ultimately have "(\<lambda>k. integral {c..} (f k)) \<longlonglongrightarrow> exp (-a*c)/a - 0/a"
@@ -12804,9 +12804,9 @@
 proof (cases "c = 0")
   case False
   define f where "f = (\<lambda>k x. if x \<in> {inverse (of_nat (Suc k))..c} then x powr a else 0)"
-  define F where "F = (\<lambda>k. if inverse (of_nat (Suc k)) \<le> c then 
+  define F where "F = (\<lambda>k. if inverse (of_nat (Suc k)) \<le> c then
                              c powr (a+1)/(a+1) - inverse (real (Suc k)) powr (a+1)/(a+1) else 0)"
-  
+
   {
     fix k :: nat
     have "(f k has_integral F k) {0..c}"
@@ -12818,10 +12818,10 @@
         also note x
         finally have "x > 0" .
       } note x = this
-      hence "((\<lambda>x. x powr a) has_integral c powr (a + 1) / (a + 1) - 
-               inverse (real (Suc k)) powr (a + 1) / (a + 1)) {inverse (real (Suc k))..c}" 
+      hence "((\<lambda>x. x powr a) has_integral c powr (a + 1) / (a + 1) -
+               inverse (real (Suc k)) powr (a + 1) / (a + 1)) {inverse (real (Suc k))..c}"
         using True a by (intro fundamental_theorem_of_calculus)
-           (auto intro!: derivative_eq_intros continuous_on_powr' continuous_on_const 
+           (auto intro!: derivative_eq_intros continuous_on_powr' continuous_on_const
              continuous_on_id simp: has_field_derivative_iff_has_vector_derivative [symmetric])
       with True show ?thesis unfolding f_def F_def by (subst has_integral_restrict) simp_all
     next
@@ -12830,9 +12830,9 @@
     qed
   } note has_integral_f = this
   have integral_f: "integral {0..c} (f k) = F k" for k
-    using has_integral_f[of k] by (rule integral_unique) 
-  
-  have A: "(\<lambda>x. x powr a) integrable_on {0..c} \<and> 
+    using has_integral_f[of k] by (rule integral_unique)
+
+  have A: "(\<lambda>x. x powr a) integrable_on {0..c} \<and>
            (\<lambda>k. integral {0..c} (f k)) \<longlonglongrightarrow> integral {0..c} (\<lambda>x. x powr a)"
   proof (intro monotone_convergence_increasing ballI allI)
     fix k from has_integral_f[of k] show "f k integrable_on {0..c}"
@@ -12863,7 +12863,7 @@
       fix k
       from a have "F k \<le> c powr (a + 1) / (a + 1)"
         by (auto simp add: F_def divide_simps)
-      also from a have "F k \<ge> 0" 
+      also from a have "F k \<ge> 0"
         by (auto simp: F_def divide_simps simp del: of_nat_Suc intro!: powr_mono2)
       hence "F k = abs (F k)" by simp
       finally have "abs (F k) \<le>  c powr (a + 1) / (a + 1)" .

--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Jul 12 22:54:37 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Jul 13 17:14:17 2016 +0100
@@ -146,7 +146,7 @@
 lemma linear_add: "linear f \<Longrightarrow> f (x + y) = f x + f y"
   by (metis linear_iff)
 
-lemma linear_sub: "linear f \<Longrightarrow> f (x - y) = f x - f y"
+lemma linear_diff: "linear f \<Longrightarrow> f (x - y) = f x - f y"
   using linear_add [of f x "- y"] by (simp add: linear_neg)
 
 lemma linear_setsum:
@@ -177,7 +177,7 @@
   also have "\<dots> \<longleftrightarrow> (\<forall> x y. f x - f y = 0 \<longrightarrow> x - y = 0)"
     by simp
   also have "\<dots> \<longleftrightarrow> (\<forall> x y. f (x - y) = 0 \<longrightarrow> x - y = 0)"
-    by (simp add: linear_sub[OF lin])
+    by (simp add: linear_diff[OF lin])
   also have "\<dots> \<longleftrightarrow> (\<forall> x. f x = 0 \<longrightarrow> x = 0)"
     by auto
   finally show ?thesis .
@@ -258,7 +258,7 @@
 lemma (in real_vector) span_mono: "A \<subseteq> B \<Longrightarrow> span A \<subseteq> span B"
   by (metis span_def hull_mono)
 
-lemma (in real_vector) subspace_span: "subspace (span S)"
+lemma (in real_vector) subspace_span [iff]: "subspace (span S)"
   unfolding span_def
   apply (rule hull_in)
   apply (simp only: subspace_def Inter_iff Int_iff subset_eq)
@@ -284,15 +284,15 @@
 
 lemma (in real_vector) span_induct:
   assumes x: "x \<in> span S"
-    and P: "subspace P"
-    and SP: "\<And>x. x \<in> S \<Longrightarrow> x \<in> P"
-  shows "x \<in> P"
+    and P: "subspace (Collect P)"
+    and SP: "\<And>x. x \<in> S \<Longrightarrow> P x"
+  shows "P x"
 proof -
-  from SP have SP': "S \<subseteq> P"
+  from SP have SP': "S \<subseteq> Collect P"
     by (simp add: subset_eq)
   from x hull_minimal[where S=subspace, OF SP' P, unfolded span_def[symmetric]]
-  show "x \<in> P"
-    by (metis subset_eq)
+  show ?thesis
+    using subset_eq by force
 qed
 
 lemma span_empty[simp]: "span {} = {0}"
@@ -385,7 +385,7 @@
           apply assumption
           apply simp
           done }
-      ultimately show "subspace (span_induct_alt_help S)"
+      ultimately show "subspace {a. a \<in> span_induct_alt_help S}"
         unfolding subspace_def Ball_def by blast
     qed
   }
@@ -501,7 +501,7 @@
   shows "f ` V \<subseteq> span (f ` B)"
   unfolding span_linear_image[OF lf] by (metis VB image_mono)
 
-lemma span_union: "span (A \<union> B) = (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
+lemma span_Un: "span (A \<union> B) = (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
 proof (rule span_unique)
   show "A \<union> B \<subseteq> (\<lambda>(a, b). a + b) ` (span A \<times> span B)"
     by safe (force intro: span_clauses)+
@@ -522,7 +522,7 @@
 lemma span_insert: "span (insert a S) = {x. \<exists>k. (x - k *\<^sub>R a) \<in> span S}"
 proof -
   have "span ({a} \<union> S) = {x. \<exists>k. (x - k *\<^sub>R a) \<in> span S}"
-    unfolding span_union span_singleton
+    unfolding span_Un span_singleton
     apply safe
     apply (rule_tac x=k in exI, simp)
     apply (erule rev_image_eqI [OF SigmaI [OF rangeI]])
@@ -2059,6 +2059,23 @@
     by (simp only: ac_simps)
 qed
 
+lemma bounded_linear_imp_has_derivative:
+     "bounded_linear f \<Longrightarrow> (f has_derivative f) net"
+  by (simp add: has_derivative_def bounded_linear.linear linear_diff)
+
+lemma linear_imp_has_derivative:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
+  shows "linear f \<Longrightarrow> (f has_derivative f) net"
+by (simp add: has_derivative_def linear_conv_bounded_linear linear_diff)
+
+lemma bounded_linear_imp_differentiable: "bounded_linear f \<Longrightarrow> f differentiable net"
+  using bounded_linear_imp_has_derivative differentiable_def by blast
+
+lemma linear_imp_differentiable:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
+  shows "linear f \<Longrightarrow> f differentiable net"
+by (metis linear_imp_has_derivative differentiable_def)
+
 
 subsection \<open>We continue.\<close>
 
@@ -2507,7 +2524,7 @@
     apply blast
     done
   then have "f x - k*\<^sub>R f a \<in> span (f ` b)"
-    by (simp add: linear_sub[OF lf] linear_cmul[OF lf])
+    by (simp add: linear_diff[OF lf] linear_cmul[OF lf])
   then have th: "-k *\<^sub>R f a \<in> span (f ` b)"
     using "2.prems"(5) by simp
   have xsb: "x \<in> span b"
@@ -2572,7 +2589,7 @@
     from B(3) x y have x': "x \<in> span B" and y': "y \<in> span B"
       by blast+
     from gxy have th0: "g (x - y) = 0"
-      by (simp add: linear_sub[OF g(1)])
+      by (simp add: linear_diff[OF g(1)])
     have th1: "x - y \<in> span B"
       using x' y' by (metis span_sub)
     have "x = y"

--- a/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy	Tue Jul 12 22:54:37 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy	Wed Jul 13 17:14:17 2016 +0100
@@ -293,5 +293,15 @@
 
 end
 
+lemma ANR_interval [iff]:
+    fixes a :: "'a::ordered_euclidean_space"
+    shows "ANR{a..b}"
+by (simp add: interval_cbox)
+
+lemma ENR_interval [iff]:
+    fixes a :: "'a::ordered_euclidean_space"
+    shows "ENR{a..b}"
+  by (auto simp: interval_cbox)
+
 end
 

--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Tue Jul 12 22:54:37 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Wed Jul 13 17:14:17 2016 +0100
@@ -4411,7 +4411,7 @@
 using contractible_imp_simply_connected convex_imp_contractible is_interval_convex_1 
       is_interval_simply_connected_1 by auto
 
-lemma contractible_times:
+lemma contractible_Times:
   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   assumes S: "contractible S" and T: "contractible T"
   shows "contractible (S \<times> T)"
@@ -5098,7 +5098,7 @@
           \<longrightarrow> (\<exists>u. openin (subtopology euclidean S) u \<and> path_connected u \<and> x \<in> u \<and> u \<subseteq> v))"
 by (metis locally_path_connected_1 locally_path_connected_2 locally_path_connected_3)
 
-proposition locally_path_connected_open_path_connected_component:
+proposition locally_path_connected_open_path_component:
   "locally path_connected S \<longleftrightarrow>
    (\<forall>t x. openin (subtopology euclidean S) t \<and> x \<in> t
           \<longrightarrow> openin (subtopology euclidean S) (path_component_set t x))"
@@ -5185,7 +5185,7 @@
       done
   qed
   show ?lhs
-    apply (clarsimp simp add: locally_path_connected_open_path_connected_component)
+    apply (clarsimp simp add: locally_path_connected_open_path_component)
     apply (subst openin_subopen)
     apply (blast intro: *)
     done
@@ -5259,6 +5259,190 @@
 apply (force simp: convex_Int convex_imp_path_connected)
 done
 
+subsection\<open>Relations between components and path components\<close>
+
+lemma path_component_eq_connected_component:
+  assumes "locally path_connected S"
+    shows "(path_component S x = connected_component S x)"
+proof (cases "x \<in> S")
+  case True
+  have "openin (subtopology euclidean (connected_component_set S x)) (path_component_set S x)"
+    apply (rule openin_subset_trans [of S])
+    apply (intro conjI openin_path_component_locally_path_connected [OF assms])
+    using path_component_subset_connected_component   apply (auto simp: connected_component_subset)
+    done
+  moreover have "closedin (subtopology euclidean (connected_component_set S x)) (path_component_set S x)"
+    apply (rule closedin_subset_trans [of S])
+    apply (intro conjI closedin_path_component_locally_path_connected [OF assms])
+    using path_component_subset_connected_component   apply (auto simp: connected_component_subset)
+    done
+  ultimately have *: "path_component_set S x = connected_component_set S x"
+    by (metis connected_connected_component connected_clopen True path_component_eq_empty)
+  then show ?thesis
+    by blast
+next
+  case False then show ?thesis
+    by (metis Collect_empty_eq_bot connected_component_eq_empty path_component_eq_empty)
+qed
+
+lemma path_component_eq_connected_component_set:
+     "locally path_connected S \<Longrightarrow> (path_component_set S x = connected_component_set S x)"
+by (simp add: path_component_eq_connected_component)
+
+lemma locally_path_connected_path_component:
+     "locally path_connected S \<Longrightarrow> locally path_connected (path_component_set S x)"
+using locally_path_connected_connected_component path_component_eq_connected_component by fastforce
+
+lemma open_path_connected_component:
+  fixes S :: "'a :: real_normed_vector set"
+  shows "open S \<Longrightarrow> path_component S x = connected_component S x"
+by (simp add: path_component_eq_connected_component open_imp_locally_path_connected)
+
+lemma open_path_connected_component_set:
+  fixes S :: "'a :: real_normed_vector set"
+  shows "open S \<Longrightarrow> path_component_set S x = connected_component_set S x"
+by (simp add: open_path_connected_component)
+
+proposition locally_connected_quotient_image:
+  assumes lcS: "locally connected S"
+      and oo: "\<And>T. T \<subseteq> f ` S
+                \<Longrightarrow> openin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> T} \<longleftrightarrow>
+                    openin (subtopology euclidean (f ` S)) T"
+    shows "locally connected (f ` S)"
+proof (clarsimp simp: locally_connected_open_component)
+  fix U C
+  assume opefSU: "openin (subtopology euclidean (f ` S)) U" and "C \<in> components U"
+  then have "C \<subseteq> U" "U \<subseteq> f ` S"
+    by (meson in_components_subset openin_imp_subset)+
+  then have "openin (subtopology euclidean (f ` S)) C \<longleftrightarrow>
+             openin (subtopology euclidean S) {x \<in> S. f x \<in> C}"
+    by (auto simp: oo)
+  moreover have "openin (subtopology euclidean S) {x \<in> S. f x \<in> C}"
+  proof (subst openin_subopen, clarify)
+    fix x
+    assume "x \<in> S" "f x \<in> C"
+    show "\<exists>T. openin (subtopology euclidean S) T \<and> x \<in> T \<and> T \<subseteq> {x \<in> S. f x \<in> C}"
+    proof (intro conjI exI)
+      show "openin (subtopology euclidean S) (connected_component_set {w \<in> S. f w \<in> U} x)"
+      proof (rule ccontr)
+        assume **: "\<not> openin (subtopology euclidean S) (connected_component_set {a \<in> S. f a \<in> U} x)"
+        then have "x \<notin> {a \<in> S. f a \<in> U}"
+          using \<open>U \<subseteq> f ` S\<close> opefSU lcS locally_connected_2 oo by blast
+        with ** show False
+          by (metis (no_types) connected_component_eq_empty empty_iff openin_subopen)
+      qed
+    next
+      show "x \<in> connected_component_set {w \<in> S. f w \<in> U} x"
+        using \<open>C \<subseteq> U\<close> \<open>f x \<in> C\<close> \<open>x \<in> S\<close> by auto
+    next
+      have contf: "continuous_on S f"
+        by (simp add: continuous_on_open oo openin_imp_subset)
+      then have "continuous_on (connected_component_set {w \<in> S. f w \<in> U} x) f"
+        apply (rule continuous_on_subset)
+        using connected_component_subset apply blast
+        done
+      then have "connected (f ` connected_component_set {w \<in> S. f w \<in> U} x)"
+        by (rule connected_continuous_image [OF _ connected_connected_component])
+      moreover have "f ` connected_component_set {w \<in> S. f w \<in> U} x \<subseteq> U"
+        using connected_component_in by blast
+      moreover have "C \<inter> f ` connected_component_set {w \<in> S. f w \<in> U} x \<noteq> {}"
+        using \<open>C \<subseteq> U\<close> \<open>f x \<in> C\<close> \<open>x \<in> S\<close> by fastforce
+      ultimately have fC: "f ` (connected_component_set {w \<in> S. f w \<in> U} x) \<subseteq> C"
+        by (rule components_maximal [OF \<open>C \<in> components U\<close>])
+      have cUC: "connected_component_set {a \<in> S. f a \<in> U} x \<subseteq> {a \<in> S. f a \<in> C}"
+        using connected_component_subset fC by blast
+      have "connected_component_set {w \<in> S. f w \<in> U} x \<subseteq> connected_component_set {w \<in> S. f w \<in> C} x"
+      proof -
+        { assume "x \<in> connected_component_set {a \<in> S. f a \<in> U} x"
+          then have ?thesis
+            by (simp add: cUC connected_component_maximal) }
+        then show ?thesis
+          using connected_component_eq_empty by auto
+      qed
+      also have "... \<subseteq> {w \<in> S. f w \<in> C}"
+        by (rule connected_component_subset)
+      finally show "connected_component_set {w \<in> S. f w \<in> U} x \<subseteq> {x \<in> S. f x \<in> C}" .
+    qed
+  qed
+  ultimately show "openin (subtopology euclidean (f ` S)) C"
+    by metis
+qed
+
+text\<open>The proof resembles that above but is not identical!\<close>
+proposition locally_path_connected_quotient_image:
+  assumes lcS: "locally path_connected S"
+      and oo: "\<And>T. T \<subseteq> f ` S
+                \<Longrightarrow> openin (subtopology euclidean S) {x. x \<in> S \<and> f x \<in> T} \<longleftrightarrow>
+                    openin (subtopology euclidean (f ` S)) T"
+    shows "locally path_connected (f ` S)"
+proof (clarsimp simp: locally_path_connected_open_path_component)
+  fix U y
+  assume opefSU: "openin (subtopology euclidean (f ` S)) U" and "y \<in> U"
+  then have "path_component_set U y \<subseteq> U" "U \<subseteq> f ` S"
+    by (meson path_component_subset openin_imp_subset)+
+  then have "openin (subtopology euclidean (f ` S)) (path_component_set U y) \<longleftrightarrow>
+             openin (subtopology euclidean S) {x \<in> S. f x \<in> path_component_set U y}"
+  proof -
+    have "path_component_set U y \<subseteq> f ` S"
+      using \<open>U \<subseteq> f ` S\<close> \<open>path_component_set U y \<subseteq> U\<close> by blast
+    then show ?thesis
+      using oo by blast
+  qed
+  moreover have "openin (subtopology euclidean S) {x \<in> S. f x \<in> path_component_set U y}"
+  proof (subst openin_subopen, clarify)
+    fix x
+    assume "x \<in> S" and Uyfx: "path_component U y (f x)"
+    then have "f x \<in> U"
+      using path_component_mem by blast
+    show "\<exists>T. openin (subtopology euclidean S) T \<and> x \<in> T \<and> T \<subseteq> {x \<in> S. f x \<in> path_component_set U y}"
+    proof (intro conjI exI)
+      show "openin (subtopology euclidean S) (path_component_set {w \<in> S. f w \<in> U} x)"
+      proof (rule ccontr)
+        assume **: "\<not> openin (subtopology euclidean S) (path_component_set {a \<in> S. f a \<in> U} x)"
+        then have "x \<notin> {a \<in> S. f a \<in> U}"
+          by (metis (no_types, lifting) \<open>U \<subseteq> f ` S\<close> opefSU lcS oo locally_path_connected_open_path_component)
+        then show False
+          using ** \<open>path_component_set U y \<subseteq> U\<close>  \<open>x \<in> S\<close> \<open>path_component U y (f x)\<close> by blast
+      qed
+    next
+      show "x \<in> path_component_set {w \<in> S. f w \<in> U} x"
+        by (metis (no_types, lifting) \<open>x \<in> S\<close> IntD2 Int_Collect \<open>path_component U y (f x)\<close> path_component_mem(2) path_component_refl)
+    next
+      have contf: "continuous_on S f"
+        by (simp add: continuous_on_open oo openin_imp_subset)
+      then have "continuous_on (path_component_set {w \<in> S. f w \<in> U} x) f"
+        apply (rule continuous_on_subset)
+        using path_component_subset apply blast
+        done
+      then have "path_connected (f ` path_component_set {w \<in> S. f w \<in> U} x)"
+        by (simp add: path_connected_continuous_image path_connected_path_component)
+      moreover have "f ` path_component_set {w \<in> S. f w \<in> U} x \<subseteq> U"
+        using path_component_mem by fastforce
+      moreover have "f x \<in> f ` path_component_set {w \<in> S. f w \<in> U} x"
+        by (force simp: \<open>x \<in> S\<close> \<open>f x \<in> U\<close> path_component_refl_eq)
+      ultimately have "f ` (path_component_set {w \<in> S. f w \<in> U} x) \<subseteq> path_component_set U (f x)"
+        by (meson path_component_maximal)
+       also have  "... \<subseteq> path_component_set U y"
+        by (simp add: Uyfx path_component_maximal path_component_subset path_component_sym path_connected_path_component)
+      finally have fC: "f ` (path_component_set {w \<in> S. f w \<in> U} x) \<subseteq> path_component_set U y" .
+      have cUC: "path_component_set {a \<in> S. f a \<in> U} x \<subseteq> {a \<in> S. f a \<in> path_component_set U y}"
+        using path_component_subset fC by blast
+      have "path_component_set {w \<in> S. f w \<in> U} x \<subseteq> path_component_set {w \<in> S. f w \<in> path_component_set U y} x"
+      proof -
+        have "\<And>a. path_component_set (path_component_set {a \<in> S. f a \<in> U} x) a \<subseteq> path_component_set {a \<in> S. f a \<in> path_component_set U y} a"
+          using cUC path_component_mono by blast
+        then show ?thesis
+          using path_component_path_component by blast
+      qed
+      also have "... \<subseteq> {w \<in> S. f w \<in> path_component_set U y}"
+        by (rule path_component_subset)
+      finally show "path_component_set {w \<in> S. f w \<in> U} x \<subseteq> {x \<in> S. f x \<in> path_component_set U y}" .
+    qed
+  qed
+  ultimately show "openin (subtopology euclidean (f ` S)) (path_component_set U y)"
+    by metis
+qed
+
 subsection\<open>Components, continuity, openin, closedin\<close>
 
 lemma continuous_openin_preimage_eq:

--- a/src/HOL/Multivariate_Analysis/Polytope.thy	Tue Jul 12 22:54:37 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Polytope.thy	Wed Jul 13 17:14:17 2016 +0100
@@ -167,8 +167,8 @@
   by (meson bounded_subset compact_eq_bounded_closed face_of_imp_closed face_of_imp_subset)
 
 lemma face_of_Int_subface:
-     "c1 \<inter> c2 face_of c1 \<and> c1 \<inter> c2 face_of c2 \<and> d1 face_of c1 \<and> d2 face_of c2
-      \<Longrightarrow> (d1 \<inter> d2) face_of d1 \<and> (d1 \<inter> d2) face_of d2"
+     "\<lbrakk>A \<inter> B face_of A; A \<inter> B face_of B; C face_of A; D face_of B\<rbrakk>
+      \<Longrightarrow> (C \<inter> D) face_of C \<and> (C \<inter> D) face_of D"
   by (meson face_of_Int_Int face_of_face inf_le1 inf_le2)
 
 lemma subset_of_face_of:
@@ -1101,9 +1101,8 @@
     proof -
       have "y \<in> span {x. a \<bullet> x = 0}"
         by (metis inf.cobounded2 span_mono subsetCE that)
-      then have "y \<in> {x. a \<bullet> x = 0}"
-        by (rule span_induct [OF _ subspace_hyperplane])
-      then show ?thesis by simp
+      then show ?thesis
+        by (blast intro: span_induct [OF _ subspace_hyperplane])
     qed
     then have "dim (S \<inter> {x. a \<bullet> x = 0}) < n"
       by (metis (no_types) less_ay c subsetD dim_eq_span inf.strict_order_iff

--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Jul 12 22:54:37 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Jul 13 17:14:17 2016 +0100
@@ -1012,6 +1012,9 @@
 lemma cball_trivial [simp]: "cball x 0 = {x}"
   by (simp add: cball_def)
 
+lemma sphere_trivial [simp]: "sphere x 0 = {x}"
+  by (simp add: sphere_def)
+
 lemma mem_ball_0 [simp]:
   fixes x :: "'a::real_normed_vector"
   shows "x \<in> ball 0 e \<longleftrightarrow> norm x < e"
@@ -2107,6 +2110,11 @@
     \<Longrightarrow> closedin (subtopology euclidean T) S"
 by (meson closedin_limpt subset_iff)
 
+lemma openin_subset_trans:
+    "\<lbrakk>openin (subtopology euclidean U) S; S \<subseteq> T; T \<subseteq> U\<rbrakk>
+     \<Longrightarrow> openin (subtopology euclidean T) S"
+  by (auto simp: openin_open)
+
 lemma closedin_Times:
    "\<lbrakk>closedin (subtopology euclidean S) S'; closedin (subtopology euclidean T) T'\<rbrakk>
     \<Longrightarrow> closedin (subtopology euclidean (S \<times> T)) (S' \<times> T')"
@@ -2324,6 +2332,14 @@
 lemma components_iff: "s \<in> components u \<longleftrightarrow> (\<exists>x. x \<in> u \<and> s = connected_component_set u x)"
   by (auto simp: components_def)
 
+lemma componentsI: "x \<in> u \<Longrightarrow> connected_component_set u x \<in> components u"
+  by (auto simp: components_def)
+
+lemma componentsE:
+  assumes "s \<in> components u"
+  obtains x where "x \<in> u" "s = connected_component_set u x"
+  using assms by (auto simp: components_def)
+
 lemma Union_components [simp]: "\<Union>(components u) = u"
   apply (rule subset_antisym)
   using Union_connected_component components_def apply fastforce

--- a/src/HOL/Real_Vector_Spaces.thy	Tue Jul 12 22:54:37 2016 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Wed Jul 13 17:14:17 2016 +0100
@@ -1439,7 +1439,8 @@
   show ?thesis by (auto intro: order_less_imp_le)
 qed
 
-lemma linear: "linear f" ..
+lemma linear: "linear f" 
+  by (fact local.linear_axioms)
 
 end