# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1473950917 -3600
# Node ID b746b19197bd8db9c3ec2c6f719ac9854606d2a9
# Parent  729accd056ad9800b40c74d8e53dd95e3568166d
lots of new results about topology, affine dimension etc

diff -r 729accd056ad -r b746b19197bd src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Sep 15 14:33:55 2016 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Sep 15 15:48:37 2016 +0100
@@ -665,6 +665,7 @@
 lemma affine_hull_empty[simp]: "affine hull {} = {}"
   by (rule hull_unique) auto
 
+(*could delete: it simply rewrites setsum expressions, but it's used twice*)
 lemma affine_hull_finite_step:
   fixes y :: "'a::real_vector"
   shows
@@ -2808,6 +2809,16 @@
   shows "aff_dim {a} = 0"
   using aff_dim_affine_independent[of "{a}"] affine_independent_1 by auto
 
+lemma aff_dim_2 [simp]: "aff_dim {a,b} = (if a = b then 0 else 1)"
+proof (clarsimp)
+  assume "a \<noteq> b"
+  then have "aff_dim{a,b} = card{a,b} - 1"
+    using affine_independent_2 [of a b] aff_dim_affine_independent by fastforce
+  also have "... = 1"
+    using \<open>a \<noteq> b\<close> by simp
+  finally show "aff_dim {a, b} = 1" .
+qed
+
 lemma aff_dim_inner_basis_exists:
   fixes V :: "('n::euclidean_space) set"
   shows "\<exists>B. B \<subseteq> V \<and> affine hull B = affine hull V \<and>
@@ -3079,6 +3090,26 @@
   ultimately show ?thesis by auto
 qed
 
+lemma aff_dim_eq_0:
+  fixes S :: "'a::euclidean_space set"
+  shows "aff_dim S = 0 \<longleftrightarrow> (\<exists>a. S = {a})"
+proof (cases "S = {}")
+  case True
+  then show ?thesis
+    by auto
+next
+  case False
+  then obtain a where "a \<in> S" by auto
+  show ?thesis
+  proof safe
+    assume 0: "aff_dim S = 0"
+    have "~ {a,b} \<subseteq> S" if "b \<noteq> a" for b
+      by (metis "0" aff_dim_2 aff_dim_subset not_one_le_zero that)
+    then show "\<exists>a. S = {a}"
+      using \<open>a \<in> S\<close> by blast
+  qed auto
+qed
+
 lemma affine_hull_UNIV:
   fixes S :: "'n::euclidean_space set"
   assumes "aff_dim S = int(DIM('n))"
@@ -3194,6 +3225,7 @@
   shows "interior S \<noteq> {} \<Longrightarrow> aff_dim S = DIM('a)"
 by (metis low_dim_interior)
 
+
 subsection \<open>Caratheodory's theorem.\<close>
 
 lemma convex_hull_caratheodory_aff_dim:
@@ -4657,6 +4689,49 @@
   shows "continuous_on t (closest_point s)"
   by (metis continuous_at_imp_continuous_on continuous_at_closest_point[OF assms])
 
+proposition closest_point_in_rel_interior:
+  assumes "closed S" "S \<noteq> {}" and x: "x \<in> affine hull S"
+    shows "closest_point S x \<in> rel_interior S \<longleftrightarrow> x \<in> rel_interior S"
+proof (cases "x \<in> S")
+  case True
+  then show ?thesis
+    by (simp add: closest_point_self)
+next
+  case False
+  then have "False" if asm: "closest_point S x \<in> rel_interior S"
+  proof -
+    obtain e where "e > 0" and clox: "closest_point S x \<in> S"
+               and e: "cball (closest_point S x) e \<inter> affine hull S \<subseteq> S"
+      using asm mem_rel_interior_cball by blast
+    then have clo_notx: "closest_point S x \<noteq> x"
+      using \<open>x \<notin> S\<close> by auto
+    define y where "y \<equiv> closest_point S x -
+                        (min 1 (e / norm(closest_point S x - x))) *\<^sub>R (closest_point S x - x)"
+    have "x - y = (1 - min 1 (e / norm (closest_point S x - x))) *\<^sub>R (x - closest_point S x)"
+      by (simp add: y_def algebra_simps)
+    then have "norm (x - y) = abs ((1 - min 1 (e / norm (closest_point S x - x)))) * norm(x - closest_point S x)"
+      by simp
+    also have "... < norm(x - closest_point S x)"
+      using clo_notx \<open>e > 0\<close>
+      by (auto simp: mult_less_cancel_right2 divide_simps)
+    finally have no_less: "norm (x - y) < norm (x - closest_point S x)" .
+    have "y \<in> affine hull S"
+      unfolding y_def
+      by (meson affine_affine_hull clox hull_subset mem_affine_3_minus2 subsetD x)
+    moreover have "dist (closest_point S x) y \<le> e"
+      using \<open>e > 0\<close> by (auto simp: y_def min_mult_distrib_right)
+    ultimately have "y \<in> S"
+      using subsetD [OF e] by simp
+    then have "dist x (closest_point S x) \<le> dist x y"
+      by (simp add: closest_point_le \<open>closed S\<close>)
+    with no_less show False
+      by (simp add: dist_norm)
+  qed
+  moreover have "x \<notin> rel_interior S"
+    using rel_interior_subset False by blast
+  ultimately show ?thesis by blast
+qed
+
 
 subsubsection \<open>Various point-to-set separating/supporting hyperplane theorems.\<close>
 
@@ -6198,14 +6273,7 @@
     "d + x \<in> open_segment (d + a) (d + b) \<longleftrightarrow> x \<in> open_segment a b"
   by (simp add: open_segment_def)
 
-definition "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)"
-
-definition "starlike s \<longleftrightarrow> (\<exists>a\<in>s. \<forall>x\<in>s. closed_segment a x \<subseteq> s)"
-
-lemma starlike_UNIV [simp]: "starlike UNIV"
-  by (simp add: starlike_def)
-
-lemma midpoint_refl: "midpoint x x = x"
+lemma midpoint_idem [simp]: "midpoint x x = x"
   unfolding midpoint_def
   unfolding scaleR_right_distrib
   unfolding scaleR_left_distrib[symmetric]
@@ -6265,19 +6333,33 @@
   "midpoint a b = b \<longleftrightarrow> a = b"
   unfolding midpoint_eq_iff by auto
 
+lemma midpoint_plus_self [simp]: "midpoint a b + midpoint a b = a + b"
+  using midpoint_eq_iff by metis
+
+lemma midpoint_linear_image:
+   "linear f \<Longrightarrow> midpoint(f a)(f b) = f(midpoint a b)"
+by (simp add: linear_iff midpoint_def)
+
+subsection\<open>Starlike sets\<close>
+
+definition "starlike S \<longleftrightarrow> (\<exists>a\<in>S. \<forall>x\<in>S. closed_segment a x \<subseteq> S)"
+
+lemma starlike_UNIV [simp]: "starlike UNIV"
+  by (simp add: starlike_def)
+
 lemma convex_contains_segment:
-  "convex s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. closed_segment a b \<subseteq> s)"
+  "convex S \<longleftrightarrow> (\<forall>a\<in>S. \<forall>b\<in>S. closed_segment a b \<subseteq> S)"
   unfolding convex_alt closed_segment_def by auto
 
-lemma closed_segment_subset: "\<lbrakk>x \<in> s; y \<in> s; convex s\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> s"
+lemma closed_segment_subset: "\<lbrakk>x \<in> S; y \<in> S; convex S\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> S"
   by (simp add: convex_contains_segment)
 
 lemma closed_segment_subset_convex_hull:
-    "\<lbrakk>x \<in> convex hull s; y \<in> convex hull s\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> convex hull s"
+    "\<lbrakk>x \<in> convex hull S; y \<in> convex hull S\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> convex hull S"
   using convex_contains_segment by blast
 
 lemma convex_imp_starlike:
-  "convex s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> starlike s"
+  "convex S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> starlike S"
   unfolding convex_contains_segment starlike_def by auto
 
 lemma segment_convex_hull:
@@ -6862,6 +6944,8 @@
 
 subsection\<open>Betweenness\<close>
 
+definition "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)"
+
 lemma between_mem_segment: "between (a,b) x \<longleftrightarrow> x \<in> closed_segment a b"
   unfolding between_def by auto
 
@@ -6945,6 +7029,35 @@
   "between (a,b) x \<longleftrightarrow> x \<in> convex hull {a,b}"
   unfolding between_mem_segment segment_convex_hull ..
 
+lemma between_triv_iff [simp]: "between (a,a) b \<longleftrightarrow> a=b"
+  by (auto simp: between_def)
+
+lemma between_triv1 [simp]: "between (a,b) a"
+  by (auto simp: between_def)
+
+lemma between_triv2 [simp]: "between (a,b) b"
+  by (auto simp: between_def)
+
+lemma between_commute:
+   "between (a,b) = between (b,a)"
+by (auto simp: between_def closed_segment_commute)
+
+lemma between_antisym:
+  fixes a :: "'a :: euclidean_space"
+  shows "\<lbrakk>between (b,c) a; between (a,c) b\<rbrakk> \<Longrightarrow> a = b"
+by (auto simp: between dist_commute)
+
+lemma between_trans:
+    fixes a :: "'a :: euclidean_space"
+    shows "\<lbrakk>between (b,c) a; between (a,c) d\<rbrakk> \<Longrightarrow> between (b,c) d"
+  using dist_triangle2 [of b c d] dist_triangle3 [of b d a]
+  by (auto simp: between dist_commute)
+
+lemma between_norm:
+    fixes a :: "'a :: euclidean_space"
+    shows "between (a,b) x \<longleftrightarrow> norm(x - a) *\<^sub>R (b - x) = norm(b - x) *\<^sub>R (x - a)"
+  by (auto simp: between dist_triangle_eq norm_minus_commute algebra_simps)
+
 
 subsection \<open>Shrinking towards the interior of a convex set\<close>
 
@@ -7950,16 +8063,17 @@
   shows "affine hull S = UNIV \<Longrightarrow> rel_frontier S = frontier S"
 by (simp add: frontier_def rel_frontier_def rel_interior_interior)
 
+lemma closest_point_in_rel_frontier:
+   "\<lbrakk>closed S; S \<noteq> {}; x \<in> affine hull S - rel_interior S\<rbrakk>
+   \<Longrightarrow> closest_point S x \<in> rel_frontier S"
+  by (simp add: closest_point_in_rel_interior closest_point_in_set rel_frontier_def)
+
 lemma closed_rel_frontier [iff]:
   fixes S :: "'n::euclidean_space set"
   shows "closed (rel_frontier S)"
 proof -
   have *: "closedin (subtopology euclidean (affine hull S)) (closure S - rel_interior S)"
-    apply (rule closedin_diff[of "subtopology euclidean (affine hull S)""closure S" "rel_interior S"])
-    using closed_closedin_trans[of "affine hull S" "closure S"] closed_affine_hull[of S]
-      closure_affine_hull[of S] openin_rel_interior[of S]
-    apply auto
-    done
+    by (simp add: closed_subset closedin_diff closure_affine_hull openin_rel_interior)
   show ?thesis
     apply (rule closedin_closed_trans[of "affine hull S" "rel_frontier S"])
     unfolding rel_frontier_def
@@ -8055,7 +8169,6 @@
     using less_le by auto
 qed
 
-
 lemma convex_rel_interior_if:
   fixes S ::  "'n::euclidean_space set"
   assumes "convex S"
@@ -10291,9 +10404,83 @@
 lemma collinear_3: "NO_MATCH 0 x \<Longrightarrow> collinear {x,y,z} \<longleftrightarrow> collinear {0, x-y, z-y}"
   by (auto simp add: collinear_def)
 
-
-thm affine_hull_nonempty
-corollary affine_hull_eq_empty [simp]: "affine hull S = {} \<longleftrightarrow> S = {}"
+lemma collinear_3_expand:
+   "collinear{a,b,c} \<longleftrightarrow> a = c \<or> (\<exists>u. b = u *\<^sub>R a + (1 - u) *\<^sub>R c)"
+proof -
+  have "collinear{a,b,c} = collinear{a,c,b}"
+    by (simp add: insert_commute)
+  also have "... = collinear {0, a - c, b - c}"
+    by (simp add: collinear_3)
+  also have "... \<longleftrightarrow> (a = c \<or> b = c \<or> (\<exists>ca. b - c = ca *\<^sub>R (a - c)))"
+    by (simp add: collinear_lemma)
+  also have "... \<longleftrightarrow> a = c \<or> (\<exists>u. b = u *\<^sub>R a + (1 - u) *\<^sub>R c)"
+    by (cases "a = c \<or> b = c") (auto simp: algebra_simps)
+  finally show ?thesis .
+qed
+
+lemma collinear_midpoint: "collinear{a,midpoint a b,b}"
+  apply (auto simp: collinear_3 collinear_lemma)
+  apply (drule_tac x="-1" in spec)
+  apply (simp add: algebra_simps)
+  done
+
+lemma midpoint_collinear:
+  fixes a b c :: "'a::real_normed_vector"
+  assumes "a \<noteq> c"
+    shows "b = midpoint a c \<longleftrightarrow> collinear{a,b,c} \<and> dist a b = dist b c"
+proof -
+  have *: "a - (u *\<^sub>R a + (1 - u) *\<^sub>R c) = (1 - u) *\<^sub>R (a - c)"
+          "u *\<^sub>R a + (1 - u) *\<^sub>R c - c = u *\<^sub>R (a - c)"
+          "\<bar>1 - u\<bar> = \<bar>u\<bar> \<longleftrightarrow> u = 1/2" for u::real
+    by (auto simp: algebra_simps)
+  have "b = midpoint a c \<Longrightarrow> collinear{a,b,c} "
+    using collinear_midpoint by blast
+  moreover have "collinear{a,b,c} \<Longrightarrow> b = midpoint a c \<longleftrightarrow> dist a b = dist b c"
+    apply (auto simp: collinear_3_expand assms dist_midpoint)
+    apply (simp add: dist_norm * assms midpoint_def del: divide_const_simps)
+    apply (simp add: algebra_simps)
+    done
+  ultimately show ?thesis by blast
+qed
+
+lemma collinear_triples:
+  assumes "a \<noteq> b"
+    shows "collinear(insert a (insert b S)) \<longleftrightarrow> (\<forall>x \<in> S. collinear{a,b,x})"
+          (is "?lhs = ?rhs")
+proof safe
+  fix x
+  assume ?lhs and "x \<in> S"
+  then show "collinear {a, b, x}"
+    using collinear_subset by force
+next
+  assume ?rhs
+  then have "\<forall>x \<in> S. collinear{a,x,b}"
+    by (simp add: insert_commute)
+  then have *: "\<exists>u. x = u *\<^sub>R a + (1 - u) *\<^sub>R b" if "x \<in> (insert a (insert b S))" for x
+    using that assms collinear_3_expand by fastforce+
+  show ?lhs
+    unfolding collinear_def
+    apply (rule_tac x="b-a" in exI)
+    apply (clarify dest!: *)
+    by (metis (no_types, hide_lams) add.commute diff_add_cancel diff_diff_eq2 real_vector.scale_right_diff_distrib scaleR_left.diff)
+qed
+
+lemma collinear_4_3:
+  assumes "a \<noteq> b"
+    shows "collinear {a,b,c,d} \<longleftrightarrow> collinear{a,b,c} \<and> collinear{a,b,d}"
+  using collinear_triples [OF assms, of "{c,d}"] by (force simp:)
+
+lemma collinear_3_trans:
+  assumes "collinear{a,b,c}" "collinear{b,c,d}" "b \<noteq> c"
+    shows "collinear{a,b,d}"
+proof -
+  have "collinear{b,c,a,d}"
+    by (metis (full_types) assms collinear_4_3 insert_commute)
+  then show ?thesis
+    by (simp add: collinear_subset)
+qed
+
+lemma affine_hull_eq_empty [simp]: "affine hull S = {} \<longleftrightarrow> S = {}"
   using affine_hull_nonempty by blast
 
 lemma affine_hull_2_alt:
@@ -11527,7 +11714,8 @@
 using supporting_hyperplane_rel_boundary [of "closure S" x]
 by (metis assms convex_closure convex_rel_interior_closure)
 
-subsection\<open> Some results on decomposing convex hulls, e.g. simplicial subdivision\<close>
+
+subsection\<open> Some results on decomposing convex hulls: intersections, simplicial subdivision\<close>
 
 lemma
   fixes s :: "'a::euclidean_space set"
@@ -11618,6 +11806,163 @@
     by auto
 qed
 
+proposition in_convex_hull_exchange_unique:
+  fixes S :: "'a::euclidean_space set"
+  assumes naff: "~ affine_dependent S" and a: "a \<in> convex hull S"
+      and S: "T \<subseteq> S" "T' \<subseteq> S"
+      and x:  "x \<in> convex hull (insert a T)"
+      and x': "x \<in> convex hull (insert a T')"
+    shows "x \<in> convex hull (insert a (T \<inter> T'))"
+proof (cases "a \<in> S")
+  case True
+  then have "\<not> affine_dependent (insert a T \<union> insert a T')"
+    using affine_dependent_subset assms by auto
+  then have "x \<in> convex hull (insert a T \<inter> insert a T')"
+    by (metis IntI convex_hull_Int x x')
+  then show ?thesis
+    by simp
+next
+  case False
+  then have anot: "a \<notin> T" "a \<notin> T'"
+    using assms by auto
+  have [simp]: "finite S"
+    by (simp add: aff_independent_finite assms)
+  then obtain b where b0: "\<And>s. s \<in> S \<Longrightarrow> 0 \<le> b s"
+                  and b1: "setsum b S = 1" and aeq: "a = (\<Sum>s\<in>S. b s *\<^sub>R s)"
+    using a by (auto simp: convex_hull_finite)
+  have fin [simp]: "finite T" "finite T'"
+    using assms infinite_super \<open>finite S\<close> by blast+
+  then obtain c c' where c0: "\<And>t. t \<in> insert a T \<Longrightarrow> 0 \<le> c t"
+                     and c1: "setsum c (insert a T) = 1"
+                     and xeq: "x = (\<Sum>t \<in> insert a T. c t *\<^sub>R t)"
+                     and c'0: "\<And>t. t \<in> insert a T' \<Longrightarrow> 0 \<le> c' t"
+                     and c'1: "setsum c' (insert a T') = 1"
+                     and x'eq: "x = (\<Sum>t \<in> insert a T'. c' t *\<^sub>R t)"
+    using x x' by (auto simp: convex_hull_finite)
+  with fin anot
+  have sumTT': "setsum c T = 1 - c a" "setsum c' T' = 1 - c' a"
+   and wsumT: "(\<Sum>t \<in> T. c t *\<^sub>R t) = x - c a *\<^sub>R a"
+    by simp_all
+  have wsumT': "(\<Sum>t \<in> T'. c' t *\<^sub>R t) = x - c' a *\<^sub>R a"
+    using x'eq fin anot by simp
+  define cc  where "cc \<equiv> \<lambda>x. if x \<in> T then c x else 0"
+  define cc' where "cc' \<equiv> \<lambda>x. if x \<in> T' then c' x else 0"
+  define dd  where "dd \<equiv> \<lambda>x. cc x - cc' x + (c a - c' a) * b x"
+  have sumSS': "setsum cc S = 1 - c a" "setsum cc' S = 1 - c' a"
+    unfolding cc_def cc'_def  using S
+    by (simp_all add: Int_absorb1 Int_absorb2 setsum_subtractf setsum.inter_restrict [symmetric] sumTT')
+  have wsumSS: "(\<Sum>t \<in> S. cc t *\<^sub>R t) = x - c a *\<^sub>R a" "(\<Sum>t \<in> S. cc' t *\<^sub>R t) = x - c' a *\<^sub>R a"
+    unfolding cc_def cc'_def  using S
+    by (simp_all add: Int_absorb1 Int_absorb2 if_smult setsum.inter_restrict [symmetric] wsumT wsumT' cong: if_cong)
+  have sum_dd0: "setsum dd S = 0"
+    unfolding dd_def  using S
+    by (simp add: sumSS' comm_monoid_add_class.setsum.distrib setsum_subtractf
+                  algebra_simps setsum_left_distrib [symmetric] b1)
+  have "(\<Sum>v\<in>S. (b v * x) *\<^sub>R v) = x *\<^sub>R (\<Sum>v\<in>S. b v *\<^sub>R v)" for x
+    by (simp add: pth_5 real_vector.scale_setsum_right mult.commute)
+  then have *: "(\<Sum>v\<in>S. (b v * x) *\<^sub>R v) = x *\<^sub>R a" for x
+    using aeq by blast
+  have "(\<Sum>v \<in> S. dd v *\<^sub>R v) = 0"
+    unfolding dd_def using S
+    by (simp add: * wsumSS setsum.distrib setsum_subtractf algebra_simps)
+  then have dd0: "dd v = 0" if "v \<in> S" for v
+    using naff that \<open>finite S\<close> sum_dd0 unfolding affine_dependent_explicit
+    apply (simp only: not_ex)
+    apply (drule_tac x=S in spec)
+    apply (drule_tac x=dd in spec, simp)
+    done
+  consider "c' a \<le> c a" | "c a \<le> c' a" by linarith
+  then show ?thesis
+  proof cases
+    case 1
+    then have "setsum cc S \<le> setsum cc' S"
+      by (simp add: sumSS')
+    then have le: "cc x \<le> cc' x" if "x \<in> S" for x
+      using dd0 [OF that] 1 b0 mult_left_mono that
+      by (fastforce simp add: dd_def algebra_simps)
+    have cc0: "cc x = 0" if "x \<in> S" "x \<notin> T \<inter> T'" for x
+      using le [OF \<open>x \<in> S\<close>] that c0
+      by (force simp: cc_def cc'_def split: if_split_asm)
+    show ?thesis
+    proof (simp add: convex_hull_finite, intro exI conjI)
+      show "\<forall>x\<in>T \<inter> T'. 0 \<le> (cc(a := c a)) x"
+        by (simp add: c0 cc_def)
+      show "0 \<le> (cc(a := c a)) a"
+        by (simp add: c0)
+      have "setsum (cc(a := c a)) (insert a (T \<inter> T')) = c a + setsum (cc(a := c a)) (T \<inter> T')"
+        by (simp add: anot)
+      also have "... = c a + setsum (cc(a := c a)) S"
+        apply simp
+        apply (rule setsum.mono_neutral_left)
+        using \<open>T \<subseteq> S\<close> apply (auto simp: \<open>a \<notin> S\<close> cc0)
+        done
+      also have "... = c a + (1 - c a)"
+        by (metis \<open>a \<notin> S\<close> fun_upd_other setsum.cong sumSS')
+      finally show "setsum (cc(a := c a)) (insert a (T \<inter> T')) = 1"
+        by simp
+      have "(\<Sum>x\<in>insert a (T \<inter> T'). (cc(a := c a)) x *\<^sub>R x) = c a *\<^sub>R a + (\<Sum>x \<in> T \<inter> T'. (cc(a := c a)) x *\<^sub>R x)"
+        by (simp add: anot)
+      also have "... = c a *\<^sub>R a + (\<Sum>x \<in> S. (cc(a := c a)) x *\<^sub>R x)"
+        apply simp
+        apply (rule setsum.mono_neutral_left)
+        using \<open>T \<subseteq> S\<close> apply (auto simp: \<open>a \<notin> S\<close> cc0)
+        done
+      also have "... = c a *\<^sub>R a + x - c a *\<^sub>R a"
+        by (simp add: wsumSS \<open>a \<notin> S\<close> if_smult setsum_delta_notmem)
+      finally show "(\<Sum>x\<in>insert a (T \<inter> T'). (cc(a := c a)) x *\<^sub>R x) = x"
+        by simp
+    qed
+  next
+    case 2
+    then have "setsum cc' S \<le> setsum cc S"
+      by (simp add: sumSS')
+    then have le: "cc' x \<le> cc x" if "x \<in> S" for x
+      using dd0 [OF that] 2 b0 mult_left_mono that
+      by (fastforce simp add: dd_def algebra_simps)
+    have cc0: "cc' x = 0" if "x \<in> S" "x \<notin> T \<inter> T'" for x
+      using le [OF \<open>x \<in> S\<close>] that c'0
+      by (force simp: cc_def cc'_def split: if_split_asm)
+    show ?thesis
+    proof (simp add: convex_hull_finite, intro exI conjI)
+      show "\<forall>x\<in>T \<inter> T'. 0 \<le> (cc'(a := c' a)) x"
+        by (simp add: c'0 cc'_def)
+      show "0 \<le> (cc'(a := c' a)) a"
+        by (simp add: c'0)
+      have "setsum (cc'(a := c' a)) (insert a (T \<inter> T')) = c' a + setsum (cc'(a := c' a)) (T \<inter> T')"
+        by (simp add: anot)
+      also have "... = c' a + setsum (cc'(a := c' a)) S"
+        apply simp
+        apply (rule setsum.mono_neutral_left)
+        using \<open>T \<subseteq> S\<close> apply (auto simp: \<open>a \<notin> S\<close> cc0)
+        done
+      also have "... = c' a + (1 - c' a)"
+        by (metis \<open>a \<notin> S\<close> fun_upd_other setsum.cong sumSS')
+      finally show "setsum (cc'(a := c' a)) (insert a (T \<inter> T')) = 1"
+        by simp
+      have "(\<Sum>x\<in>insert a (T \<inter> T'). (cc'(a := c' a)) x *\<^sub>R x) = c' a *\<^sub>R a + (\<Sum>x \<in> T \<inter> T'. (cc'(a := c' a)) x *\<^sub>R x)"
+        by (simp add: anot)
+      also have "... = c' a *\<^sub>R a + (\<Sum>x \<in> S. (cc'(a := c' a)) x *\<^sub>R x)"
+        apply simp
+        apply (rule setsum.mono_neutral_left)
+        using \<open>T \<subseteq> S\<close> apply (auto simp: \<open>a \<notin> S\<close> cc0)
+        done
+      also have "... = c a *\<^sub>R a + x - c a *\<^sub>R a"
+        by (simp add: wsumSS \<open>a \<notin> S\<close> if_smult setsum_delta_notmem)
+      finally show "(\<Sum>x\<in>insert a (T \<inter> T'). (cc'(a := c' a)) x *\<^sub>R x) = x"
+        by simp
+    qed
+  qed
+qed
+
+corollary convex_hull_exchange_Int:
+  fixes a  :: "'a::euclidean_space"
+  assumes "~ affine_dependent S" "a \<in> convex hull S" "T \<subseteq> S" "T' \<subseteq> S"
+  shows "(convex hull (insert a T)) \<inter> (convex hull (insert a T')) =
+         convex hull (insert a (T \<inter> T'))"
+apply (rule subset_antisym)
+  using in_convex_hull_exchange_unique assms apply blast
+  by (metis hull_mono inf_le1 inf_le2 insert_inter_insert le_inf_iff)
+
 lemma affine_hull_finite_intersection_hyperplanes:
   fixes s :: "'a::euclidean_space set"
   obtains f where
diff -r 729accd056ad -r b746b19197bd src/HOL/Analysis/Linear_Algebra.thy
--- a/src/HOL/Analysis/Linear_Algebra.thy	Thu Sep 15 14:33:55 2016 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Sep 15 15:48:37 2016 +0100
@@ -3125,6 +3125,9 @@
 definition collinear :: "'a::real_vector set \<Rightarrow> bool"
   where "collinear S \<longleftrightarrow> (\<exists>u. \<forall>x \<in> S. \<forall> y \<in> S. \<exists>c. x - y = c *\<^sub>R u)"
 
+lemma collinear_subset: "\<lbrakk>collinear T; S \<subseteq> T\<rbrakk> \<Longrightarrow> collinear S"
+  by (meson collinear_def subsetCE)
+
 lemma collinear_empty [iff]: "collinear {}"
   by (simp add: collinear_def)
 
diff -r 729accd056ad -r b746b19197bd src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Thu Sep 15 14:33:55 2016 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Thu Sep 15 15:48:37 2016 +0100
@@ -1214,6 +1214,17 @@
 lemma of_real_linepath: "of_real (linepath a b x) = linepath (of_real a) (of_real b) x"
   by (metis linepath_of_real mult.right_neutral of_real_def real_scaleR_def)
 
+lemma inj_on_linepath:
+  assumes "a \<noteq> b" shows "inj_on (linepath a b) {0..1}"
+proof (clarsimp simp: inj_on_def linepath_def)
+  fix x y
+  assume "(1 - x) *\<^sub>R a + x *\<^sub>R b = (1 - y) *\<^sub>R a + y *\<^sub>R b" "0 \<le> x" "x \<le> 1" "0 \<le> y" "y \<le> 1"
+  then have "x *\<^sub>R (a - b) = y *\<^sub>R (a - b)"
+    by (auto simp: algebra_simps)
+  then show "x=y"
+    using assms by auto
+qed
+
 
 subsection\<open>Segments via convex hulls\<close>
 
diff -r 729accd056ad -r b746b19197bd src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Sep 15 14:33:55 2016 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Sep 15 15:48:37 2016 +0100
@@ -763,10 +763,6 @@
 lemma closedin_closed_Int: "closed S \<Longrightarrow> closedin (subtopology euclidean U) (U \<inter> S)"
   by (metis closedin_closed)
 
-lemma closed_closedin_trans:
-  "closed S \<Longrightarrow> closed T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> closedin (subtopology euclidean S) T"
-  by (metis closedin_closed inf.absorb2)
-
 lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> closedin (subtopology euclidean T) S"
   by (auto simp add: closedin_closed)
 
@@ -930,6 +926,11 @@
   shows "x \<in> sphere 0 e \<longleftrightarrow> norm x = e"
   by (simp add: dist_norm)
 
+lemma sphere_empty [simp]:
+  fixes a :: "'a::metric_space"
+  shows "r < 0 \<Longrightarrow> sphere a r = {}"
+by auto
+
 lemma centre_in_ball [simp]: "x \<in> ball x e \<longleftrightarrow> 0 < e"
   by simp
 
@@ -7312,6 +7313,13 @@
 definition diameter :: "'a::metric_space set \<Rightarrow> real" where
   "diameter S = (if S = {} then 0 else SUP (x,y):S\<times>S. dist x y)"
 
+lemma diameter_le:
+  assumes "S \<noteq> {} \<or> 0 \<le> d"
+      and no: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> norm(x - y) \<le> d"
+    shows "diameter S \<le> d"
+using assms
+  by (auto simp: dist_norm diameter_def intro: cSUP_least)
+
 lemma diameter_bounded_bound:
   fixes s :: "'a :: metric_space set"
   assumes s: "bounded s" "x \<in> s" "y \<in> s"
@@ -8058,7 +8066,10 @@
     unfolding mem_box by auto
 qed
 
-lemma closure_box:
+lemma closure_cbox [simp]: "closure (cbox a b) = cbox a b"
+  by (simp add: closed_cbox)
+
+lemma closure_box [simp]:
   fixes a :: "'a::euclidean_space"
    assumes "box a b \<noteq> {}"
   shows "closure (box a b) = cbox a b"
diff -r 729accd056ad -r b746b19197bd src/HOL/Library/Continuum_Not_Denumerable.thy
--- a/src/HOL/Library/Continuum_Not_Denumerable.thy	Thu Sep 15 14:33:55 2016 +0100
+++ b/src/HOL/Library/Continuum_Not_Denumerable.thy	Thu Sep 15 15:48:37 2016 +0100
@@ -167,6 +167,11 @@
     by auto
 qed
 
+lemma uncountable_closed_interval: "uncountable {a..b} \<longleftrightarrow> a < b" for a b :: real
+  apply (rule iffI)
+   apply (metis atLeastAtMost_singleton atLeastatMost_empty countable_finite finite.emptyI finite_insert linorder_neqE_linordered_idom)
+  using real_interval_avoid_countable_set by fastforce
+
 lemma open_minus_countable:
   fixes S A :: "real set"
   assumes "countable A" "S \<noteq> {}" "open S"