lots of new results about topology, affine dimension etc
authorpaulson <lp15@cam.ac.uk>
Thu Sep 15 15:48:37 2016 +0100 (2016-09-15)
changeset 63881b746b19197bd
parent 63880 729accd056ad
child 63883 41b5d9f3778a
lots of new results about topology, affine dimension etc
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/Linear_Algebra.thy
src/HOL/Analysis/Path_Connected.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
src/HOL/Library/Continuum_Not_Denumerable.thy
     1.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Sep 15 14:33:55 2016 +0100
     1.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Sep 15 15:48:37 2016 +0100
     1.3 @@ -665,6 +665,7 @@
     1.4  lemma affine_hull_empty[simp]: "affine hull {} = {}"
     1.5    by (rule hull_unique) auto
     1.6  
     1.7 +(*could delete: it simply rewrites setsum expressions, but it's used twice*)
     1.8  lemma affine_hull_finite_step:
     1.9    fixes y :: "'a::real_vector"
    1.10    shows
    1.11 @@ -2808,6 +2809,16 @@
    1.12    shows "aff_dim {a} = 0"
    1.13    using aff_dim_affine_independent[of "{a}"] affine_independent_1 by auto
    1.14  
    1.15 +lemma aff_dim_2 [simp]: "aff_dim {a,b} = (if a = b then 0 else 1)"
    1.16 +proof (clarsimp)
    1.17 +  assume "a \<noteq> b"
    1.18 +  then have "aff_dim{a,b} = card{a,b} - 1"
    1.19 +    using affine_independent_2 [of a b] aff_dim_affine_independent by fastforce
    1.20 +  also have "... = 1"
    1.21 +    using \<open>a \<noteq> b\<close> by simp
    1.22 +  finally show "aff_dim {a, b} = 1" .
    1.23 +qed
    1.24 +
    1.25  lemma aff_dim_inner_basis_exists:
    1.26    fixes V :: "('n::euclidean_space) set"
    1.27    shows "\<exists>B. B \<subseteq> V \<and> affine hull B = affine hull V \<and>
    1.28 @@ -3079,6 +3090,26 @@
    1.29    ultimately show ?thesis by auto
    1.30  qed
    1.31  
    1.32 +lemma aff_dim_eq_0:
    1.33 +  fixes S :: "'a::euclidean_space set"
    1.34 +  shows "aff_dim S = 0 \<longleftrightarrow> (\<exists>a. S = {a})"
    1.35 +proof (cases "S = {}")
    1.36 +  case True
    1.37 +  then show ?thesis
    1.38 +    by auto
    1.39 +next
    1.40 +  case False
    1.41 +  then obtain a where "a \<in> S" by auto
    1.42 +  show ?thesis
    1.43 +  proof safe
    1.44 +    assume 0: "aff_dim S = 0"
    1.45 +    have "~ {a,b} \<subseteq> S" if "b \<noteq> a" for b
    1.46 +      by (metis "0" aff_dim_2 aff_dim_subset not_one_le_zero that)
    1.47 +    then show "\<exists>a. S = {a}"
    1.48 +      using \<open>a \<in> S\<close> by blast
    1.49 +  qed auto
    1.50 +qed
    1.51 +
    1.52  lemma affine_hull_UNIV:
    1.53    fixes S :: "'n::euclidean_space set"
    1.54    assumes "aff_dim S = int(DIM('n))"
    1.55 @@ -3194,6 +3225,7 @@
    1.56    shows "interior S \<noteq> {} \<Longrightarrow> aff_dim S = DIM('a)"
    1.57  by (metis low_dim_interior)
    1.58  
    1.59 +
    1.60  subsection \<open>Caratheodory's theorem.\<close>
    1.61  
    1.62  lemma convex_hull_caratheodory_aff_dim:
    1.63 @@ -4657,6 +4689,49 @@
    1.64    shows "continuous_on t (closest_point s)"
    1.65    by (metis continuous_at_imp_continuous_on continuous_at_closest_point[OF assms])
    1.66  
    1.67 +proposition closest_point_in_rel_interior:
    1.68 +  assumes "closed S" "S \<noteq> {}" and x: "x \<in> affine hull S"
    1.69 +    shows "closest_point S x \<in> rel_interior S \<longleftrightarrow> x \<in> rel_interior S"
    1.70 +proof (cases "x \<in> S")
    1.71 +  case True
    1.72 +  then show ?thesis
    1.73 +    by (simp add: closest_point_self)
    1.74 +next
    1.75 +  case False
    1.76 +  then have "False" if asm: "closest_point S x \<in> rel_interior S"
    1.77 +  proof -
    1.78 +    obtain e where "e > 0" and clox: "closest_point S x \<in> S"
    1.79 +               and e: "cball (closest_point S x) e \<inter> affine hull S \<subseteq> S"
    1.80 +      using asm mem_rel_interior_cball by blast
    1.81 +    then have clo_notx: "closest_point S x \<noteq> x"
    1.82 +      using \<open>x \<notin> S\<close> by auto
    1.83 +    define y where "y \<equiv> closest_point S x -
    1.84 +                        (min 1 (e / norm(closest_point S x - x))) *\<^sub>R (closest_point S x - x)"
    1.85 +    have "x - y = (1 - min 1 (e / norm (closest_point S x - x))) *\<^sub>R (x - closest_point S x)"
    1.86 +      by (simp add: y_def algebra_simps)
    1.87 +    then have "norm (x - y) = abs ((1 - min 1 (e / norm (closest_point S x - x)))) * norm(x - closest_point S x)"
    1.88 +      by simp
    1.89 +    also have "... < norm(x - closest_point S x)"
    1.90 +      using clo_notx \<open>e > 0\<close>
    1.91 +      by (auto simp: mult_less_cancel_right2 divide_simps)
    1.92 +    finally have no_less: "norm (x - y) < norm (x - closest_point S x)" .
    1.93 +    have "y \<in> affine hull S"
    1.94 +      unfolding y_def
    1.95 +      by (meson affine_affine_hull clox hull_subset mem_affine_3_minus2 subsetD x)
    1.96 +    moreover have "dist (closest_point S x) y \<le> e"
    1.97 +      using \<open>e > 0\<close> by (auto simp: y_def min_mult_distrib_right)
    1.98 +    ultimately have "y \<in> S"
    1.99 +      using subsetD [OF e] by simp
   1.100 +    then have "dist x (closest_point S x) \<le> dist x y"
   1.101 +      by (simp add: closest_point_le \<open>closed S\<close>)
   1.102 +    with no_less show False
   1.103 +      by (simp add: dist_norm)
   1.104 +  qed
   1.105 +  moreover have "x \<notin> rel_interior S"
   1.106 +    using rel_interior_subset False by blast
   1.107 +  ultimately show ?thesis by blast
   1.108 +qed
   1.109 +
   1.110  
   1.111  subsubsection \<open>Various point-to-set separating/supporting hyperplane theorems.\<close>
   1.112  
   1.113 @@ -6198,14 +6273,7 @@
   1.114      "d + x \<in> open_segment (d + a) (d + b) \<longleftrightarrow> x \<in> open_segment a b"
   1.115    by (simp add: open_segment_def)
   1.116  
   1.117 -definition "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)"
   1.118 -
   1.119 -definition "starlike s \<longleftrightarrow> (\<exists>a\<in>s. \<forall>x\<in>s. closed_segment a x \<subseteq> s)"
   1.120 -
   1.121 -lemma starlike_UNIV [simp]: "starlike UNIV"
   1.122 -  by (simp add: starlike_def)
   1.123 -
   1.124 -lemma midpoint_refl: "midpoint x x = x"
   1.125 +lemma midpoint_idem [simp]: "midpoint x x = x"
   1.126    unfolding midpoint_def
   1.127    unfolding scaleR_right_distrib
   1.128    unfolding scaleR_left_distrib[symmetric]
   1.129 @@ -6265,19 +6333,33 @@
   1.130    "midpoint a b = b \<longleftrightarrow> a = b"
   1.131    unfolding midpoint_eq_iff by auto
   1.132  
   1.133 +lemma midpoint_plus_self [simp]: "midpoint a b + midpoint a b = a + b"
   1.134 +  using midpoint_eq_iff by metis
   1.135 +
   1.136 +lemma midpoint_linear_image:
   1.137 +   "linear f \<Longrightarrow> midpoint(f a)(f b) = f(midpoint a b)"
   1.138 +by (simp add: linear_iff midpoint_def)
   1.139 +
   1.140 +subsection\<open>Starlike sets\<close>
   1.141 +
   1.142 +definition "starlike S \<longleftrightarrow> (\<exists>a\<in>S. \<forall>x\<in>S. closed_segment a x \<subseteq> S)"
   1.143 +
   1.144 +lemma starlike_UNIV [simp]: "starlike UNIV"
   1.145 +  by (simp add: starlike_def)
   1.146 +
   1.147  lemma convex_contains_segment:
   1.148 -  "convex s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. closed_segment a b \<subseteq> s)"
   1.149 +  "convex S \<longleftrightarrow> (\<forall>a\<in>S. \<forall>b\<in>S. closed_segment a b \<subseteq> S)"
   1.150    unfolding convex_alt closed_segment_def by auto
   1.151  
   1.152 -lemma closed_segment_subset: "\<lbrakk>x \<in> s; y \<in> s; convex s\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> s"
   1.153 +lemma closed_segment_subset: "\<lbrakk>x \<in> S; y \<in> S; convex S\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> S"
   1.154    by (simp add: convex_contains_segment)
   1.155  
   1.156  lemma closed_segment_subset_convex_hull:
   1.157 -    "\<lbrakk>x \<in> convex hull s; y \<in> convex hull s\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> convex hull s"
   1.158 +    "\<lbrakk>x \<in> convex hull S; y \<in> convex hull S\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> convex hull S"
   1.159    using convex_contains_segment by blast
   1.160  
   1.161  lemma convex_imp_starlike:
   1.162 -  "convex s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> starlike s"
   1.163 +  "convex S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> starlike S"
   1.164    unfolding convex_contains_segment starlike_def by auto
   1.165  
   1.166  lemma segment_convex_hull:
   1.167 @@ -6862,6 +6944,8 @@
   1.168  
   1.169  subsection\<open>Betweenness\<close>
   1.170  
   1.171 +definition "between = (\<lambda>(a,b) x. x \<in> closed_segment a b)"
   1.172 +
   1.173  lemma between_mem_segment: "between (a,b) x \<longleftrightarrow> x \<in> closed_segment a b"
   1.174    unfolding between_def by auto
   1.175  
   1.176 @@ -6945,6 +7029,35 @@
   1.177    "between (a,b) x \<longleftrightarrow> x \<in> convex hull {a,b}"
   1.178    unfolding between_mem_segment segment_convex_hull ..
   1.179  
   1.180 +lemma between_triv_iff [simp]: "between (a,a) b \<longleftrightarrow> a=b"
   1.181 +  by (auto simp: between_def)
   1.182 +
   1.183 +lemma between_triv1 [simp]: "between (a,b) a"
   1.184 +  by (auto simp: between_def)
   1.185 +
   1.186 +lemma between_triv2 [simp]: "between (a,b) b"
   1.187 +  by (auto simp: between_def)
   1.188 +
   1.189 +lemma between_commute:
   1.190 +   "between (a,b) = between (b,a)"
   1.191 +by (auto simp: between_def closed_segment_commute)
   1.192 +
   1.193 +lemma between_antisym:
   1.194 +  fixes a :: "'a :: euclidean_space"
   1.195 +  shows "\<lbrakk>between (b,c) a; between (a,c) b\<rbrakk> \<Longrightarrow> a = b"
   1.196 +by (auto simp: between dist_commute)
   1.197 +
   1.198 +lemma between_trans:
   1.199 +    fixes a :: "'a :: euclidean_space"
   1.200 +    shows "\<lbrakk>between (b,c) a; between (a,c) d\<rbrakk> \<Longrightarrow> between (b,c) d"
   1.201 +  using dist_triangle2 [of b c d] dist_triangle3 [of b d a]
   1.202 +  by (auto simp: between dist_commute)
   1.203 +
   1.204 +lemma between_norm:
   1.205 +    fixes a :: "'a :: euclidean_space"
   1.206 +    shows "between (a,b) x \<longleftrightarrow> norm(x - a) *\<^sub>R (b - x) = norm(b - x) *\<^sub>R (x - a)"
   1.207 +  by (auto simp: between dist_triangle_eq norm_minus_commute algebra_simps)
   1.208 +
   1.209  
   1.210  subsection \<open>Shrinking towards the interior of a convex set\<close>
   1.211  
   1.212 @@ -7950,16 +8063,17 @@
   1.213    shows "affine hull S = UNIV \<Longrightarrow> rel_frontier S = frontier S"
   1.214  by (simp add: frontier_def rel_frontier_def rel_interior_interior)
   1.215  
   1.216 +lemma closest_point_in_rel_frontier:
   1.217 +   "\<lbrakk>closed S; S \<noteq> {}; x \<in> affine hull S - rel_interior S\<rbrakk>
   1.218 +   \<Longrightarrow> closest_point S x \<in> rel_frontier S"
   1.219 +  by (simp add: closest_point_in_rel_interior closest_point_in_set rel_frontier_def)
   1.220 +
   1.221  lemma closed_rel_frontier [iff]:
   1.222    fixes S :: "'n::euclidean_space set"
   1.223    shows "closed (rel_frontier S)"
   1.224  proof -
   1.225    have *: "closedin (subtopology euclidean (affine hull S)) (closure S - rel_interior S)"
   1.226 -    apply (rule closedin_diff[of "subtopology euclidean (affine hull S)""closure S" "rel_interior S"])
   1.227 -    using closed_closedin_trans[of "affine hull S" "closure S"] closed_affine_hull[of S]
   1.228 -      closure_affine_hull[of S] openin_rel_interior[of S]
   1.229 -    apply auto
   1.230 -    done
   1.231 +    by (simp add: closed_subset closedin_diff closure_affine_hull openin_rel_interior)
   1.232    show ?thesis
   1.233      apply (rule closedin_closed_trans[of "affine hull S" "rel_frontier S"])
   1.234      unfolding rel_frontier_def
   1.235 @@ -8055,7 +8169,6 @@
   1.236      using less_le by auto
   1.237  qed
   1.238  
   1.239 -
   1.240  lemma convex_rel_interior_if:
   1.241    fixes S ::  "'n::euclidean_space set"
   1.242    assumes "convex S"
   1.243 @@ -10291,9 +10404,83 @@
   1.244  lemma collinear_3: "NO_MATCH 0 x \<Longrightarrow> collinear {x,y,z} \<longleftrightarrow> collinear {0, x-y, z-y}"
   1.245    by (auto simp add: collinear_def)
   1.246  
   1.247 -
   1.248 -thm affine_hull_nonempty
   1.249 -corollary affine_hull_eq_empty [simp]: "affine hull S = {} \<longleftrightarrow> S = {}"
   1.250 +lemma collinear_3_expand:
   1.251 +   "collinear{a,b,c} \<longleftrightarrow> a = c \<or> (\<exists>u. b = u *\<^sub>R a + (1 - u) *\<^sub>R c)"
   1.252 +proof -
   1.253 +  have "collinear{a,b,c} = collinear{a,c,b}"
   1.254 +    by (simp add: insert_commute)
   1.255 +  also have "... = collinear {0, a - c, b - c}"
   1.256 +    by (simp add: collinear_3)
   1.257 +  also have "... \<longleftrightarrow> (a = c \<or> b = c \<or> (\<exists>ca. b - c = ca *\<^sub>R (a - c)))"
   1.258 +    by (simp add: collinear_lemma)
   1.259 +  also have "... \<longleftrightarrow> a = c \<or> (\<exists>u. b = u *\<^sub>R a + (1 - u) *\<^sub>R c)"
   1.260 +    by (cases "a = c \<or> b = c") (auto simp: algebra_simps)
   1.261 +  finally show ?thesis .
   1.262 +qed
   1.263 +
   1.264 +lemma collinear_midpoint: "collinear{a,midpoint a b,b}"
   1.265 +  apply (auto simp: collinear_3 collinear_lemma)
   1.266 +  apply (drule_tac x="-1" in spec)
   1.267 +  apply (simp add: algebra_simps)
   1.268 +  done
   1.269 +
   1.270 +lemma midpoint_collinear:
   1.271 +  fixes a b c :: "'a::real_normed_vector"
   1.272 +  assumes "a \<noteq> c"
   1.273 +    shows "b = midpoint a c \<longleftrightarrow> collinear{a,b,c} \<and> dist a b = dist b c"
   1.274 +proof -
   1.275 +  have *: "a - (u *\<^sub>R a + (1 - u) *\<^sub>R c) = (1 - u) *\<^sub>R (a - c)"
   1.276 +          "u *\<^sub>R a + (1 - u) *\<^sub>R c - c = u *\<^sub>R (a - c)"
   1.277 +          "\<bar>1 - u\<bar> = \<bar>u\<bar> \<longleftrightarrow> u = 1/2" for u::real
   1.278 +    by (auto simp: algebra_simps)
   1.279 +  have "b = midpoint a c \<Longrightarrow> collinear{a,b,c} "
   1.280 +    using collinear_midpoint by blast
   1.281 +  moreover have "collinear{a,b,c} \<Longrightarrow> b = midpoint a c \<longleftrightarrow> dist a b = dist b c"
   1.282 +    apply (auto simp: collinear_3_expand assms dist_midpoint)
   1.283 +    apply (simp add: dist_norm * assms midpoint_def del: divide_const_simps)
   1.284 +    apply (simp add: algebra_simps)
   1.285 +    done
   1.286 +  ultimately show ?thesis by blast
   1.287 +qed
   1.288 +
   1.289 +lemma collinear_triples:
   1.290 +  assumes "a \<noteq> b"
   1.291 +    shows "collinear(insert a (insert b S)) \<longleftrightarrow> (\<forall>x \<in> S. collinear{a,b,x})"
   1.292 +          (is "?lhs = ?rhs")
   1.293 +proof safe
   1.294 +  fix x
   1.295 +  assume ?lhs and "x \<in> S"
   1.296 +  then show "collinear {a, b, x}"
   1.297 +    using collinear_subset by force
   1.298 +next
   1.299 +  assume ?rhs
   1.300 +  then have "\<forall>x \<in> S. collinear{a,x,b}"
   1.301 +    by (simp add: insert_commute)
   1.302 +  then have *: "\<exists>u. x = u *\<^sub>R a + (1 - u) *\<^sub>R b" if "x \<in> (insert a (insert b S))" for x
   1.303 +    using that assms collinear_3_expand by fastforce+
   1.304 +  show ?lhs
   1.305 +    unfolding collinear_def
   1.306 +    apply (rule_tac x="b-a" in exI)
   1.307 +    apply (clarify dest!: *)
   1.308 +    by (metis (no_types, hide_lams) add.commute diff_add_cancel diff_diff_eq2 real_vector.scale_right_diff_distrib scaleR_left.diff)
   1.309 +qed
   1.310 +
   1.311 +lemma collinear_4_3:
   1.312 +  assumes "a \<noteq> b"
   1.313 +    shows "collinear {a,b,c,d} \<longleftrightarrow> collinear{a,b,c} \<and> collinear{a,b,d}"
   1.314 +  using collinear_triples [OF assms, of "{c,d}"] by (force simp:)
   1.315 +
   1.316 +lemma collinear_3_trans:
   1.317 +  assumes "collinear{a,b,c}" "collinear{b,c,d}" "b \<noteq> c"
   1.318 +    shows "collinear{a,b,d}"
   1.319 +proof -
   1.320 +  have "collinear{b,c,a,d}"
   1.321 +    by (metis (full_types) assms collinear_4_3 insert_commute)
   1.322 +  then show ?thesis
   1.323 +    by (simp add: collinear_subset)
   1.324 +qed
   1.325 +
   1.326 +lemma affine_hull_eq_empty [simp]: "affine hull S = {} \<longleftrightarrow> S = {}"
   1.327    using affine_hull_nonempty by blast
   1.328  
   1.329  lemma affine_hull_2_alt:
   1.330 @@ -11527,7 +11714,8 @@
   1.331  using supporting_hyperplane_rel_boundary [of "closure S" x]
   1.332  by (metis assms convex_closure convex_rel_interior_closure)
   1.333  
   1.334 -subsection\<open> Some results on decomposing convex hulls, e.g. simplicial subdivision\<close>
   1.335 +
   1.336 +subsection\<open> Some results on decomposing convex hulls: intersections, simplicial subdivision\<close>
   1.337  
   1.338  lemma
   1.339    fixes s :: "'a::euclidean_space set"
   1.340 @@ -11618,6 +11806,163 @@
   1.341      by auto
   1.342  qed
   1.343  
   1.344 +proposition in_convex_hull_exchange_unique:
   1.345 +  fixes S :: "'a::euclidean_space set"
   1.346 +  assumes naff: "~ affine_dependent S" and a: "a \<in> convex hull S"
   1.347 +      and S: "T \<subseteq> S" "T' \<subseteq> S"
   1.348 +      and x:  "x \<in> convex hull (insert a T)"
   1.349 +      and x': "x \<in> convex hull (insert a T')"
   1.350 +    shows "x \<in> convex hull (insert a (T \<inter> T'))"
   1.351 +proof (cases "a \<in> S")
   1.352 +  case True
   1.353 +  then have "\<not> affine_dependent (insert a T \<union> insert a T')"
   1.354 +    using affine_dependent_subset assms by auto
   1.355 +  then have "x \<in> convex hull (insert a T \<inter> insert a T')"
   1.356 +    by (metis IntI convex_hull_Int x x')
   1.357 +  then show ?thesis
   1.358 +    by simp
   1.359 +next
   1.360 +  case False
   1.361 +  then have anot: "a \<notin> T" "a \<notin> T'"
   1.362 +    using assms by auto
   1.363 +  have [simp]: "finite S"
   1.364 +    by (simp add: aff_independent_finite assms)
   1.365 +  then obtain b where b0: "\<And>s. s \<in> S \<Longrightarrow> 0 \<le> b s"
   1.366 +                  and b1: "setsum b S = 1" and aeq: "a = (\<Sum>s\<in>S. b s *\<^sub>R s)"
   1.367 +    using a by (auto simp: convex_hull_finite)
   1.368 +  have fin [simp]: "finite T" "finite T'"
   1.369 +    using assms infinite_super \<open>finite S\<close> by blast+
   1.370 +  then obtain c c' where c0: "\<And>t. t \<in> insert a T \<Longrightarrow> 0 \<le> c t"
   1.371 +                     and c1: "setsum c (insert a T) = 1"
   1.372 +                     and xeq: "x = (\<Sum>t \<in> insert a T. c t *\<^sub>R t)"
   1.373 +                     and c'0: "\<And>t. t \<in> insert a T' \<Longrightarrow> 0 \<le> c' t"
   1.374 +                     and c'1: "setsum c' (insert a T') = 1"
   1.375 +                     and x'eq: "x = (\<Sum>t \<in> insert a T'. c' t *\<^sub>R t)"
   1.376 +    using x x' by (auto simp: convex_hull_finite)
   1.377 +  with fin anot
   1.378 +  have sumTT': "setsum c T = 1 - c a" "setsum c' T' = 1 - c' a"
   1.379 +   and wsumT: "(\<Sum>t \<in> T. c t *\<^sub>R t) = x - c a *\<^sub>R a"
   1.380 +    by simp_all
   1.381 +  have wsumT': "(\<Sum>t \<in> T'. c' t *\<^sub>R t) = x - c' a *\<^sub>R a"
   1.382 +    using x'eq fin anot by simp
   1.383 +  define cc  where "cc \<equiv> \<lambda>x. if x \<in> T then c x else 0"
   1.384 +  define cc' where "cc' \<equiv> \<lambda>x. if x \<in> T' then c' x else 0"
   1.385 +  define dd  where "dd \<equiv> \<lambda>x. cc x - cc' x + (c a - c' a) * b x"
   1.386 +  have sumSS': "setsum cc S = 1 - c a" "setsum cc' S = 1 - c' a"
   1.387 +    unfolding cc_def cc'_def  using S
   1.388 +    by (simp_all add: Int_absorb1 Int_absorb2 setsum_subtractf setsum.inter_restrict [symmetric] sumTT')
   1.389 +  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"
   1.390 +    unfolding cc_def cc'_def  using S
   1.391 +    by (simp_all add: Int_absorb1 Int_absorb2 if_smult setsum.inter_restrict [symmetric] wsumT wsumT' cong: if_cong)
   1.392 +  have sum_dd0: "setsum dd S = 0"
   1.393 +    unfolding dd_def  using S
   1.394 +    by (simp add: sumSS' comm_monoid_add_class.setsum.distrib setsum_subtractf
   1.395 +                  algebra_simps setsum_left_distrib [symmetric] b1)
   1.396 +  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
   1.397 +    by (simp add: pth_5 real_vector.scale_setsum_right mult.commute)
   1.398 +  then have *: "(\<Sum>v\<in>S. (b v * x) *\<^sub>R v) = x *\<^sub>R a" for x
   1.399 +    using aeq by blast
   1.400 +  have "(\<Sum>v \<in> S. dd v *\<^sub>R v) = 0"
   1.401 +    unfolding dd_def using S
   1.402 +    by (simp add: * wsumSS setsum.distrib setsum_subtractf algebra_simps)
   1.403 +  then have dd0: "dd v = 0" if "v \<in> S" for v
   1.404 +    using naff that \<open>finite S\<close> sum_dd0 unfolding affine_dependent_explicit
   1.405 +    apply (simp only: not_ex)
   1.406 +    apply (drule_tac x=S in spec)
   1.407 +    apply (drule_tac x=dd in spec, simp)
   1.408 +    done
   1.409 +  consider "c' a \<le> c a" | "c a \<le> c' a" by linarith
   1.410 +  then show ?thesis
   1.411 +  proof cases
   1.412 +    case 1
   1.413 +    then have "setsum cc S \<le> setsum cc' S"
   1.414 +      by (simp add: sumSS')
   1.415 +    then have le: "cc x \<le> cc' x" if "x \<in> S" for x
   1.416 +      using dd0 [OF that] 1 b0 mult_left_mono that
   1.417 +      by (fastforce simp add: dd_def algebra_simps)
   1.418 +    have cc0: "cc x = 0" if "x \<in> S" "x \<notin> T \<inter> T'" for x
   1.419 +      using le [OF \<open>x \<in> S\<close>] that c0
   1.420 +      by (force simp: cc_def cc'_def split: if_split_asm)
   1.421 +    show ?thesis
   1.422 +    proof (simp add: convex_hull_finite, intro exI conjI)
   1.423 +      show "\<forall>x\<in>T \<inter> T'. 0 \<le> (cc(a := c a)) x"
   1.424 +        by (simp add: c0 cc_def)
   1.425 +      show "0 \<le> (cc(a := c a)) a"
   1.426 +        by (simp add: c0)
   1.427 +      have "setsum (cc(a := c a)) (insert a (T \<inter> T')) = c a + setsum (cc(a := c a)) (T \<inter> T')"
   1.428 +        by (simp add: anot)
   1.429 +      also have "... = c a + setsum (cc(a := c a)) S"
   1.430 +        apply simp
   1.431 +        apply (rule setsum.mono_neutral_left)
   1.432 +        using \<open>T \<subseteq> S\<close> apply (auto simp: \<open>a \<notin> S\<close> cc0)
   1.433 +        done
   1.434 +      also have "... = c a + (1 - c a)"
   1.435 +        by (metis \<open>a \<notin> S\<close> fun_upd_other setsum.cong sumSS')
   1.436 +      finally show "setsum (cc(a := c a)) (insert a (T \<inter> T')) = 1"
   1.437 +        by simp
   1.438 +      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)"
   1.439 +        by (simp add: anot)
   1.440 +      also have "... = c a *\<^sub>R a + (\<Sum>x \<in> S. (cc(a := c a)) x *\<^sub>R x)"
   1.441 +        apply simp
   1.442 +        apply (rule setsum.mono_neutral_left)
   1.443 +        using \<open>T \<subseteq> S\<close> apply (auto simp: \<open>a \<notin> S\<close> cc0)
   1.444 +        done
   1.445 +      also have "... = c a *\<^sub>R a + x - c a *\<^sub>R a"
   1.446 +        by (simp add: wsumSS \<open>a \<notin> S\<close> if_smult setsum_delta_notmem)
   1.447 +      finally show "(\<Sum>x\<in>insert a (T \<inter> T'). (cc(a := c a)) x *\<^sub>R x) = x"
   1.448 +        by simp
   1.449 +    qed
   1.450 +  next
   1.451 +    case 2
   1.452 +    then have "setsum cc' S \<le> setsum cc S"
   1.453 +      by (simp add: sumSS')
   1.454 +    then have le: "cc' x \<le> cc x" if "x \<in> S" for x
   1.455 +      using dd0 [OF that] 2 b0 mult_left_mono that
   1.456 +      by (fastforce simp add: dd_def algebra_simps)
   1.457 +    have cc0: "cc' x = 0" if "x \<in> S" "x \<notin> T \<inter> T'" for x
   1.458 +      using le [OF \<open>x \<in> S\<close>] that c'0
   1.459 +      by (force simp: cc_def cc'_def split: if_split_asm)
   1.460 +    show ?thesis
   1.461 +    proof (simp add: convex_hull_finite, intro exI conjI)
   1.462 +      show "\<forall>x\<in>T \<inter> T'. 0 \<le> (cc'(a := c' a)) x"
   1.463 +        by (simp add: c'0 cc'_def)
   1.464 +      show "0 \<le> (cc'(a := c' a)) a"
   1.465 +        by (simp add: c'0)
   1.466 +      have "setsum (cc'(a := c' a)) (insert a (T \<inter> T')) = c' a + setsum (cc'(a := c' a)) (T \<inter> T')"
   1.467 +        by (simp add: anot)
   1.468 +      also have "... = c' a + setsum (cc'(a := c' a)) S"
   1.469 +        apply simp
   1.470 +        apply (rule setsum.mono_neutral_left)
   1.471 +        using \<open>T \<subseteq> S\<close> apply (auto simp: \<open>a \<notin> S\<close> cc0)
   1.472 +        done
   1.473 +      also have "... = c' a + (1 - c' a)"
   1.474 +        by (metis \<open>a \<notin> S\<close> fun_upd_other setsum.cong sumSS')
   1.475 +      finally show "setsum (cc'(a := c' a)) (insert a (T \<inter> T')) = 1"
   1.476 +        by simp
   1.477 +      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)"
   1.478 +        by (simp add: anot)
   1.479 +      also have "... = c' a *\<^sub>R a + (\<Sum>x \<in> S. (cc'(a := c' a)) x *\<^sub>R x)"
   1.480 +        apply simp
   1.481 +        apply (rule setsum.mono_neutral_left)
   1.482 +        using \<open>T \<subseteq> S\<close> apply (auto simp: \<open>a \<notin> S\<close> cc0)
   1.483 +        done
   1.484 +      also have "... = c a *\<^sub>R a + x - c a *\<^sub>R a"
   1.485 +        by (simp add: wsumSS \<open>a \<notin> S\<close> if_smult setsum_delta_notmem)
   1.486 +      finally show "(\<Sum>x\<in>insert a (T \<inter> T'). (cc'(a := c' a)) x *\<^sub>R x) = x"
   1.487 +        by simp
   1.488 +    qed
   1.489 +  qed
   1.490 +qed
   1.491 +
   1.492 +corollary convex_hull_exchange_Int:
   1.493 +  fixes a  :: "'a::euclidean_space"
   1.494 +  assumes "~ affine_dependent S" "a \<in> convex hull S" "T \<subseteq> S" "T' \<subseteq> S"
   1.495 +  shows "(convex hull (insert a T)) \<inter> (convex hull (insert a T')) =
   1.496 +         convex hull (insert a (T \<inter> T'))"
   1.497 +apply (rule subset_antisym)
   1.498 +  using in_convex_hull_exchange_unique assms apply blast
   1.499 +  by (metis hull_mono inf_le1 inf_le2 insert_inter_insert le_inf_iff)
   1.500 +
   1.501  lemma affine_hull_finite_intersection_hyperplanes:
   1.502    fixes s :: "'a::euclidean_space set"
   1.503    obtains f where
     2.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Thu Sep 15 14:33:55 2016 +0100
     2.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Sep 15 15:48:37 2016 +0100
     2.3 @@ -3125,6 +3125,9 @@
     2.4  definition collinear :: "'a::real_vector set \<Rightarrow> bool"
     2.5    where "collinear S \<longleftrightarrow> (\<exists>u. \<forall>x \<in> S. \<forall> y \<in> S. \<exists>c. x - y = c *\<^sub>R u)"
     2.6  
     2.7 +lemma collinear_subset: "\<lbrakk>collinear T; S \<subseteq> T\<rbrakk> \<Longrightarrow> collinear S"
     2.8 +  by (meson collinear_def subsetCE)
     2.9 +
    2.10  lemma collinear_empty [iff]: "collinear {}"
    2.11    by (simp add: collinear_def)
    2.12  
     3.1 --- a/src/HOL/Analysis/Path_Connected.thy	Thu Sep 15 14:33:55 2016 +0100
     3.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Thu Sep 15 15:48:37 2016 +0100
     3.3 @@ -1214,6 +1214,17 @@
     3.4  lemma of_real_linepath: "of_real (linepath a b x) = linepath (of_real a) (of_real b) x"
     3.5    by (metis linepath_of_real mult.right_neutral of_real_def real_scaleR_def)
     3.6  
     3.7 +lemma inj_on_linepath:
     3.8 +  assumes "a \<noteq> b" shows "inj_on (linepath a b) {0..1}"
     3.9 +proof (clarsimp simp: inj_on_def linepath_def)
    3.10 +  fix x y
    3.11 +  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"
    3.12 +  then have "x *\<^sub>R (a - b) = y *\<^sub>R (a - b)"
    3.13 +    by (auto simp: algebra_simps)
    3.14 +  then show "x=y"
    3.15 +    using assms by auto
    3.16 +qed
    3.17 +
    3.18  
    3.19  subsection\<open>Segments via convex hulls\<close>
    3.20  
     4.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Sep 15 14:33:55 2016 +0100
     4.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Sep 15 15:48:37 2016 +0100
     4.3 @@ -763,10 +763,6 @@
     4.4  lemma closedin_closed_Int: "closed S \<Longrightarrow> closedin (subtopology euclidean U) (U \<inter> S)"
     4.5    by (metis closedin_closed)
     4.6  
     4.7 -lemma closed_closedin_trans:
     4.8 -  "closed S \<Longrightarrow> closed T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> closedin (subtopology euclidean S) T"
     4.9 -  by (metis closedin_closed inf.absorb2)
    4.10 -
    4.11  lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> closedin (subtopology euclidean T) S"
    4.12    by (auto simp add: closedin_closed)
    4.13  
    4.14 @@ -930,6 +926,11 @@
    4.15    shows "x \<in> sphere 0 e \<longleftrightarrow> norm x = e"
    4.16    by (simp add: dist_norm)
    4.17  
    4.18 +lemma sphere_empty [simp]:
    4.19 +  fixes a :: "'a::metric_space"
    4.20 +  shows "r < 0 \<Longrightarrow> sphere a r = {}"
    4.21 +by auto
    4.22 +
    4.23  lemma centre_in_ball [simp]: "x \<in> ball x e \<longleftrightarrow> 0 < e"
    4.24    by simp
    4.25  
    4.26 @@ -7312,6 +7313,13 @@
    4.27  definition diameter :: "'a::metric_space set \<Rightarrow> real" where
    4.28    "diameter S = (if S = {} then 0 else SUP (x,y):S\<times>S. dist x y)"
    4.29  
    4.30 +lemma diameter_le:
    4.31 +  assumes "S \<noteq> {} \<or> 0 \<le> d"
    4.32 +      and no: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> norm(x - y) \<le> d"
    4.33 +    shows "diameter S \<le> d"
    4.34 +using assms
    4.35 +  by (auto simp: dist_norm diameter_def intro: cSUP_least)
    4.36 +
    4.37  lemma diameter_bounded_bound:
    4.38    fixes s :: "'a :: metric_space set"
    4.39    assumes s: "bounded s" "x \<in> s" "y \<in> s"
    4.40 @@ -8058,7 +8066,10 @@
    4.41      unfolding mem_box by auto
    4.42  qed
    4.43  
    4.44 -lemma closure_box:
    4.45 +lemma closure_cbox [simp]: "closure (cbox a b) = cbox a b"
    4.46 +  by (simp add: closed_cbox)
    4.47 +
    4.48 +lemma closure_box [simp]:
    4.49    fixes a :: "'a::euclidean_space"
    4.50     assumes "box a b \<noteq> {}"
    4.51    shows "closure (box a b) = cbox a b"
     5.1 --- a/src/HOL/Library/Continuum_Not_Denumerable.thy	Thu Sep 15 14:33:55 2016 +0100
     5.2 +++ b/src/HOL/Library/Continuum_Not_Denumerable.thy	Thu Sep 15 15:48:37 2016 +0100
     5.3 @@ -167,6 +167,11 @@
     5.4      by auto
     5.5  qed
     5.6  
     5.7 +lemma uncountable_closed_interval: "uncountable {a..b} \<longleftrightarrow> a < b" for a b :: real
     5.8 +  apply (rule iffI)
     5.9 +   apply (metis atLeastAtMost_singleton atLeastatMost_empty countable_finite finite.emptyI finite_insert linorder_neqE_linordered_idom)
    5.10 +  using real_interval_avoid_countable_set by fastforce
    5.11 +
    5.12  lemma open_minus_countable:
    5.13    fixes S A :: "real set"
    5.14    assumes "countable A" "S \<noteq> {}" "open S"