author paulson Thu Sep 15 15:48:37 2016 +0100 (2016-09-15) changeset 63881 b746b19197bd parent 63880 729accd056ad child 63883 41b5d9f3778a
lots of new results about topology, affine dimension etc
```     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.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.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.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.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.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.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"
```