new material: Colinearity, convex sets, polytopes
authorpaulson <lp15@cam.ac.uk>
Wed Jul 19 16:41:26 2017 +0100 (22 months ago)
changeset 66287005a30862ed0
parent 66286 1c977b13414f
child 66288 e5995950b98a
new material: Colinearity, convex sets, polytopes
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/Homeomorphism.thy
src/HOL/Analysis/Linear_Algebra.thy
src/HOL/Analysis/Polytope.thy
     1.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Jul 18 11:35:32 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Wed Jul 19 16:41:26 2017 +0100
     1.3 @@ -2704,6 +2704,13 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +lemma convex_hull_insert_alt:
     1.8 +   "convex hull (insert a S) =
     1.9 +      (if S = {} then {a}
    1.10 +      else {(1 - u) *\<^sub>R a + u *\<^sub>R x |x u. 0 \<le> u \<and> u \<le> 1 \<and> x \<in> convex hull S})"
    1.11 +  apply (auto simp: convex_hull_insert)
    1.12 +  using diff_eq_eq apply fastforce
    1.13 +  by (metis add.group_left_neutral add_le_imp_le_diff diff_add_cancel)
    1.14  
    1.15  subsubsection \<open>Explicit expression for convex hull\<close>
    1.16  
    1.17 @@ -3271,13 +3278,13 @@
    1.18  
    1.19  subsection \<open>Some Properties of Affine Dependent Sets\<close>
    1.20  
    1.21 -lemma affine_independent_0: "\<not> affine_dependent {}"
    1.22 +lemma affine_independent_0 [simp]: "\<not> affine_dependent {}"
    1.23    by (simp add: affine_dependent_def)
    1.24  
    1.25 -lemma affine_independent_1: "\<not> affine_dependent {a}"
    1.26 +lemma affine_independent_1 [simp]: "\<not> affine_dependent {a}"
    1.27    by (simp add: affine_dependent_def)
    1.28  
    1.29 -lemma affine_independent_2: "\<not> affine_dependent {a,b}"
    1.30 +lemma affine_independent_2 [simp]: "\<not> affine_dependent {a,b}"
    1.31    by (simp add: affine_dependent_def insert_Diff_if hull_same)
    1.32  
    1.33  lemma affine_hull_translation: "affine hull ((\<lambda>x. a + x) `  S) = (\<lambda>x. a + x) ` (affine hull S)"
    1.34 @@ -7806,6 +7813,7 @@
    1.35      by (metis image_comp convex_translation)
    1.36  qed
    1.37  
    1.38 +
    1.39  lemmas convex_segment = convex_closed_segment convex_open_segment
    1.40  
    1.41  lemma connected_segment [iff]:
    1.42 @@ -7836,6 +7844,36 @@
    1.43      by (auto intro: rel_interior_closure_convex_shrink)
    1.44  qed
    1.45  
    1.46 +lemma convex_hull_insert_segments:
    1.47 +   "convex hull (insert a S) =
    1.48 +    (if S = {} then {a} else  \<Union>x \<in> convex hull S. closed_segment a x)"
    1.49 +  by (force simp add: convex_hull_insert_alt in_segment)
    1.50 +
    1.51 +lemma Int_convex_hull_insert_rel_exterior:
    1.52 +  fixes z :: "'a::euclidean_space"
    1.53 +  assumes "convex C" "T \<subseteq> C" and z: "z \<in> rel_interior C" and dis: "disjnt S (rel_interior C)"
    1.54 +  shows "S \<inter> (convex hull (insert z T)) = S \<inter> (convex hull T)" (is "?lhs = ?rhs")
    1.55 +proof
    1.56 +  have "T = {} \<Longrightarrow> z \<notin> S"
    1.57 +    using dis z by (auto simp add: disjnt_def)
    1.58 +  then show "?lhs \<subseteq> ?rhs"
    1.59 +  proof (clarsimp simp add: convex_hull_insert_segments)
    1.60 +    fix x y
    1.61 +    assume "x \<in> S" and y: "y \<in> convex hull T" and "x \<in> closed_segment z y"
    1.62 +    have "y \<in> closure C"
    1.63 +      by (metis y \<open>convex C\<close> \<open>T \<subseteq> C\<close> closure_subset contra_subsetD convex_hull_eq hull_mono)
    1.64 +    moreover have "x \<notin> rel_interior C"
    1.65 +      by (meson \<open>x \<in> S\<close> dis disjnt_iff)
    1.66 +    moreover have "x \<in> open_segment z y \<union> {z, y}"
    1.67 +      using \<open>x \<in> closed_segment z y\<close> closed_segment_eq_open by blast
    1.68 +    ultimately show "x \<in> convex hull T"
    1.69 +      using rel_interior_closure_convex_segment [OF \<open>convex C\<close> z]
    1.70 +      using y z by blast
    1.71 +  qed
    1.72 +  show "?rhs \<subseteq> ?lhs"
    1.73 +    by (meson hull_mono inf_mono subset_insertI subset_refl)
    1.74 +qed
    1.75 +
    1.76  subsection\<open>More results about segments\<close>
    1.77  
    1.78  lemma dist_half_times2:
    1.79 @@ -8210,6 +8248,24 @@
    1.80    shows "between (X, B) Y \<longleftrightarrow> between (A, Y) X"
    1.81  using assms by (auto simp add: between)
    1.82  
    1.83 +lemma between_translation [simp]: "between (a + y,a + z) (a + x) \<longleftrightarrow> between (y,z) x"
    1.84 +  by (auto simp: between_def)
    1.85 +
    1.86 +lemma between_trans_2:
    1.87 +  fixes a :: "'a :: euclidean_space"
    1.88 +  shows "\<lbrakk>between (b,c) a; between (a,b) d\<rbrakk> \<Longrightarrow> between (c,d) a"
    1.89 +  by (metis between_commute between_swap between_trans)
    1.90 +
    1.91 +lemma between_scaleR_lift [simp]:
    1.92 +  fixes v :: "'a::euclidean_space"
    1.93 +  shows "between (a *\<^sub>R v, b *\<^sub>R v) (c *\<^sub>R v) \<longleftrightarrow> v = 0 \<or> between (a, b) c"
    1.94 +  by (simp add: between dist_norm scaleR_left_diff_distrib [symmetric] distrib_right [symmetric])
    1.95 +
    1.96 +lemma between_1:
    1.97 +  fixes x::real
    1.98 +  shows "between (a,b) x \<longleftrightarrow> (a \<le> x \<and> x \<le> b) \<or> (b \<le> x \<and> x \<le> a)"
    1.99 +  by (auto simp: between_mem_segment closed_segment_eq_real_ivl)
   1.100 +
   1.101  
   1.102  subsection \<open>Shrinking towards the interior of a convex set\<close>
   1.103  
   1.104 @@ -11527,6 +11583,24 @@
   1.105    by (metis convex_hull_subset_affine_hull segment_convex_hull dual_order.trans
   1.106      convex_hull_subset_affine_hull Diff_subset collinear_affine_hull)
   1.107  
   1.108 +lemma collinear_between_cases:
   1.109 +  fixes c :: "'a::euclidean_space"
   1.110 +  shows "collinear {a,b,c} \<longleftrightarrow> between (b,c) a \<or> between (c,a) b \<or> between (a,b) c"
   1.111 +         (is "?lhs = ?rhs")
   1.112 +proof
   1.113 +  assume ?lhs
   1.114 +  then obtain u v where uv: "\<And>x. x \<in> {a, b, c} \<Longrightarrow> \<exists>c. x = u + c *\<^sub>R v"
   1.115 +    by (auto simp: collinear_alt)
   1.116 +  show ?rhs
   1.117 +    using uv [of a] uv [of b] uv [of c] by (auto simp: between_1)
   1.118 +next
   1.119 +  assume ?rhs
   1.120 +  then show ?lhs
   1.121 +    unfolding between_mem_convex_hull
   1.122 +    by (metis (no_types, hide_lams) collinear_closed_segment collinear_subset hull_redundant hull_subset insert_commute segment_convex_hull)
   1.123 +qed
   1.124 +
   1.125 +
   1.126  lemma subset_continuous_image_segment_1:
   1.127    fixes f :: "'a::euclidean_space \<Rightarrow> real"
   1.128    assumes "continuous_on (closed_segment a b) f"
   1.129 @@ -12401,6 +12475,145 @@
   1.130      by (simp add: continuous_on_closed * closedin_imp_subset)
   1.131  qed
   1.132  
   1.133 +subsection\<open>Trivial fact: convexity equals connectedness for collinear sets\<close>
   1.134 +
   1.135 +lemma convex_connected_collinear:
   1.136 +  fixes S :: "'a::euclidean_space set"
   1.137 +  assumes "collinear S"
   1.138 +    shows "convex S \<longleftrightarrow> connected S"
   1.139 +proof
   1.140 +  assume "convex S"
   1.141 +  then show "connected S"
   1.142 +    using convex_connected by blast
   1.143 +next
   1.144 +  assume S: "connected S"
   1.145 +  show "convex S"
   1.146 +  proof (cases "S = {}")
   1.147 +    case True
   1.148 +    then show ?thesis by simp
   1.149 +  next
   1.150 +    case False
   1.151 +    then obtain a where "a \<in> S" by auto
   1.152 +    have "collinear (affine hull S)"
   1.153 +      by (simp add: assms collinear_affine_hull_collinear)
   1.154 +    then obtain z where "z \<noteq> 0" "\<And>x. x \<in> affine hull S \<Longrightarrow> \<exists>c. x - a = c *\<^sub>R z"
   1.155 +      by (meson \<open>a \<in> S\<close> collinear hull_inc)
   1.156 +    then obtain f where f: "\<And>x. x \<in> affine hull S \<Longrightarrow> x - a = f x *\<^sub>R z"
   1.157 +      by metis
   1.158 +    then have inj_f: "inj_on f (affine hull S)"
   1.159 +      by (metis diff_add_cancel inj_onI)
   1.160 +    have diff: "x - y = (f x - f y) *\<^sub>R z" if x: "x \<in> affine hull S" and y: "y \<in> affine hull S" for x y
   1.161 +    proof -
   1.162 +      have "f x *\<^sub>R z = x - a"
   1.163 +        by (simp add: f hull_inc x)
   1.164 +      moreover have "f y *\<^sub>R z = y - a"
   1.165 +        by (simp add: f hull_inc y)
   1.166 +      ultimately show ?thesis
   1.167 +        by (simp add: scaleR_left.diff)
   1.168 +    qed
   1.169 +    have cont_f: "continuous_on (affine hull S) f"
   1.170 +      apply (clarsimp simp: dist_norm continuous_on_iff diff)
   1.171 +      by (metis \<open>z \<noteq> 0\<close> mult.commute mult_less_cancel_left_pos norm_minus_commute real_norm_def zero_less_mult_iff zero_less_norm_iff)
   1.172 +    then have conn_fS: "connected (f ` S)"
   1.173 +      by (meson S connected_continuous_image continuous_on_subset hull_subset)
   1.174 +    show ?thesis
   1.175 +    proof (clarsimp simp: convex_contains_segment)
   1.176 +      fix x y z
   1.177 +      assume "x \<in> S" "y \<in> S" "z \<in> closed_segment x y"
   1.178 +      have False if "z \<notin> S"
   1.179 +      proof -
   1.180 +        have "f ` (closed_segment x y) = closed_segment (f x) (f y)"
   1.181 +          apply (rule continuous_injective_image_segment_1)
   1.182 +          apply (meson \<open>x \<in> S\<close> \<open>y \<in> S\<close> convex_affine_hull convex_contains_segment hull_inc continuous_on_subset [OF cont_f])
   1.183 +          by (meson \<open>x \<in> S\<close> \<open>y \<in> S\<close> convex_affine_hull convex_contains_segment hull_inc inj_on_subset [OF inj_f])
   1.184 +        then have fz: "f z \<in> closed_segment (f x) (f y)"
   1.185 +          using \<open>z \<in> closed_segment x y\<close> by blast
   1.186 +        have "z \<in> affine hull S"
   1.187 +          by (meson \<open>x \<in> S\<close> \<open>y \<in> S\<close> \<open>z \<in> closed_segment x y\<close> convex_affine_hull convex_contains_segment hull_inc subset_eq)
   1.188 +        then have fz_notin: "f z \<notin> f ` S"
   1.189 +          using hull_subset inj_f inj_onD that by fastforce
   1.190 +        moreover have "{..<f z} \<inter> f ` S \<noteq> {}" "{f z<..} \<inter> f ` S \<noteq> {}"
   1.191 +        proof -
   1.192 +          have "{..<f z} \<inter> f ` {x,y} \<noteq> {}"  "{f z<..} \<inter> f ` {x,y} \<noteq> {}"
   1.193 +            using fz fz_notin \<open>x \<in> S\<close> \<open>y \<in> S\<close>
   1.194 +             apply (auto simp: closed_segment_eq_real_ivl split: if_split_asm)
   1.195 +             apply (metis image_eqI less_eq_real_def)+
   1.196 +            done
   1.197 +          then show "{..<f z} \<inter> f ` S \<noteq> {}" "{f z<..} \<inter> f ` S \<noteq> {}"
   1.198 +            using \<open>x \<in> S\<close> \<open>y \<in> S\<close> by blast+
   1.199 +        qed
   1.200 +        ultimately show False
   1.201 +          using connectedD [OF conn_fS, of "{..<f z}" "{f z<..}"] by force
   1.202 +      qed
   1.203 +      then show "z \<in> S" by meson
   1.204 +    qed
   1.205 +  qed
   1.206 +qed
   1.207 +
   1.208 +lemma compact_convex_collinear_segment_alt:
   1.209 +  fixes S :: "'a::euclidean_space set"
   1.210 +  assumes "S \<noteq> {}" "compact S" "connected S" "collinear S"
   1.211 +  obtains a b where "S = closed_segment a b"
   1.212 +proof -
   1.213 +  obtain \<xi> where "\<xi> \<in> S" using \<open>S \<noteq> {}\<close> by auto
   1.214 +  have "collinear (affine hull S)"
   1.215 +    by (simp add: assms collinear_affine_hull_collinear)
   1.216 +  then obtain z where "z \<noteq> 0" "\<And>x. x \<in> affine hull S \<Longrightarrow> \<exists>c. x - \<xi> = c *\<^sub>R z"
   1.217 +    by (meson \<open>\<xi> \<in> S\<close> collinear hull_inc)
   1.218 +  then obtain f where f: "\<And>x. x \<in> affine hull S \<Longrightarrow> x - \<xi> = f x *\<^sub>R z"
   1.219 +    by metis
   1.220 +  let ?g = "\<lambda>r. r *\<^sub>R z + \<xi>"
   1.221 +  have gf: "?g (f x) = x" if "x \<in> affine hull S" for x
   1.222 +    by (metis diff_add_cancel f that)
   1.223 +  then have inj_f: "inj_on f (affine hull S)"
   1.224 +    by (metis inj_onI)
   1.225 +  have diff: "x - y = (f x - f y) *\<^sub>R z" if x: "x \<in> affine hull S" and y: "y \<in> affine hull S" for x y
   1.226 +  proof -
   1.227 +    have "f x *\<^sub>R z = x - \<xi>"
   1.228 +      by (simp add: f hull_inc x)
   1.229 +    moreover have "f y *\<^sub>R z = y - \<xi>"
   1.230 +      by (simp add: f hull_inc y)
   1.231 +    ultimately show ?thesis
   1.232 +      by (simp add: scaleR_left.diff)
   1.233 +  qed
   1.234 +  have cont_f: "continuous_on (affine hull S) f"
   1.235 +    apply (clarsimp simp: dist_norm continuous_on_iff diff)
   1.236 +    by (metis \<open>z \<noteq> 0\<close> mult.commute mult_less_cancel_left_pos norm_minus_commute real_norm_def zero_less_mult_iff zero_less_norm_iff)
   1.237 +  then have "connected (f ` S)"
   1.238 +    by (meson \<open>connected S\<close> connected_continuous_image continuous_on_subset hull_subset)
   1.239 +  moreover have "compact (f ` S)"
   1.240 +    by (meson \<open>compact S\<close> compact_continuous_image_eq cont_f hull_subset inj_f)
   1.241 +  ultimately obtain x y where "f ` S = {x..y}"
   1.242 +    by (meson connected_compact_interval_1)
   1.243 +  then have fS_eq: "f ` S = closed_segment x y"
   1.244 +    using \<open>S \<noteq> {}\<close> closed_segment_eq_real_ivl by auto
   1.245 +  obtain a b where "a \<in> S" "f a = x" "b \<in> S" "f b = y"
   1.246 +    by (metis (full_types) ends_in_segment fS_eq imageE)
   1.247 +  have "f ` (closed_segment a b) = closed_segment (f a) (f b)"
   1.248 +    apply (rule continuous_injective_image_segment_1)
   1.249 +     apply (meson \<open>a \<in> S\<close> \<open>b \<in> S\<close> convex_affine_hull convex_contains_segment hull_inc continuous_on_subset [OF cont_f])
   1.250 +    by (meson \<open>a \<in> S\<close> \<open>b \<in> S\<close> convex_affine_hull convex_contains_segment hull_inc inj_on_subset [OF inj_f])
   1.251 +  then have "f ` (closed_segment a b) = f ` S"
   1.252 +    by (simp add: \<open>f a = x\<close> \<open>f b = y\<close> fS_eq)
   1.253 +  then have "?g ` f ` (closed_segment a b) = ?g ` f ` S"
   1.254 +    by simp
   1.255 +  moreover have "(\<lambda>x. f x *\<^sub>R z + \<xi>) ` closed_segment a b = closed_segment a b"
   1.256 +    apply safe
   1.257 +     apply (metis (mono_tags, hide_lams) \<open>a \<in> S\<close> \<open>b \<in> S\<close> convex_affine_hull convex_contains_segment gf hull_inc subsetCE)
   1.258 +    by (metis (mono_tags, lifting) \<open>a \<in> S\<close> \<open>b \<in> S\<close> convex_affine_hull convex_contains_segment gf hull_subset image_iff subsetCE)
   1.259 +  ultimately have "closed_segment a b = S"
   1.260 +    using gf by (simp add: image_comp o_def hull_inc cong: image_cong)
   1.261 +  then show ?thesis
   1.262 +    using that by blast
   1.263 +qed
   1.264 +
   1.265 +lemma compact_convex_collinear_segment:
   1.266 +  fixes S :: "'a::euclidean_space set"
   1.267 +  assumes "S \<noteq> {}" "compact S" "convex S" "collinear S"
   1.268 +  obtains a b where "S = closed_segment a b"
   1.269 +  using assms convex_connected_collinear compact_convex_collinear_segment_alt by blast
   1.270 +
   1.271 +
   1.272  lemma proper_map_from_compact:
   1.273    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   1.274    assumes contf: "continuous_on S f" and imf: "f ` S \<subseteq> T" and "compact S"
     2.1 --- a/src/HOL/Analysis/Homeomorphism.thy	Tue Jul 18 11:35:32 2017 +0200
     2.2 +++ b/src/HOL/Analysis/Homeomorphism.thy	Wed Jul 19 16:41:26 2017 +0100
     2.3 @@ -157,6 +157,65 @@
     2.4      by (simp add: \<open>interior S = rel_interior S\<close> frontier_def rel_frontier_def that)
     2.5  qed
     2.6  
     2.7 +
     2.8 +lemma segment_to_rel_frontier_aux:
     2.9 +  fixes x :: "'a::euclidean_space"
    2.10 +  assumes "convex S" "bounded S" and x: "x \<in> rel_interior S" and y: "y \<in> S" and xy: "x \<noteq> y"
    2.11 +  obtains z where "z \<in> rel_frontier S" "y \<in> closed_segment x z"
    2.12 +                   "open_segment x z \<subseteq> rel_interior S"
    2.13 +proof -
    2.14 +  have "x + (y - x) \<in> affine hull S"
    2.15 +    using hull_inc [OF y] by auto
    2.16 +  then obtain d where "0 < d" and df: "(x + d *\<^sub>R (y-x)) \<in> rel_frontier S"
    2.17 +                  and di: "\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (x + e *\<^sub>R (y-x)) \<in> rel_interior S"
    2.18 +    by (rule ray_to_rel_frontier [OF \<open>bounded S\<close> x]) (use xy in auto)
    2.19 +  show ?thesis
    2.20 +  proof
    2.21 +    show "x + d *\<^sub>R (y - x) \<in> rel_frontier S"
    2.22 +      by (simp add: df)
    2.23 +  next
    2.24 +    have "open_segment x y \<subseteq> rel_interior S"
    2.25 +      using rel_interior_closure_convex_segment [OF \<open>convex S\<close> x] closure_subset y by blast
    2.26 +    moreover have "x + d *\<^sub>R (y - x) \<in> open_segment x y" if "d < 1"
    2.27 +      using xy
    2.28 +      apply (auto simp: in_segment)
    2.29 +      apply (rule_tac x="d" in exI)
    2.30 +      using \<open>0 < d\<close> that apply (auto simp: divide_simps algebra_simps)
    2.31 +      done
    2.32 +    ultimately have "1 \<le> d"
    2.33 +      using df rel_frontier_def by fastforce
    2.34 +    moreover have "x = (1 / d) *\<^sub>R x + ((d - 1) / d) *\<^sub>R x"
    2.35 +      by (metis \<open>0 < d\<close> add.commute add_divide_distrib diff_add_cancel divide_self_if less_irrefl scaleR_add_left scaleR_one)
    2.36 +    ultimately show "y \<in> closed_segment x (x + d *\<^sub>R (y - x))"
    2.37 +      apply (auto simp: in_segment)
    2.38 +      apply (rule_tac x="1/d" in exI)
    2.39 +      apply (auto simp: divide_simps algebra_simps)
    2.40 +      done
    2.41 +  next
    2.42 +    show "open_segment x (x + d *\<^sub>R (y - x)) \<subseteq> rel_interior S"
    2.43 +      apply (rule rel_interior_closure_convex_segment [OF \<open>convex S\<close> x])
    2.44 +      using df rel_frontier_def by auto
    2.45 +  qed
    2.46 +qed
    2.47 +
    2.48 +lemma segment_to_rel_frontier:
    2.49 +  fixes x :: "'a::euclidean_space"
    2.50 +  assumes S: "convex S" "bounded S" and x: "x \<in> rel_interior S"
    2.51 +      and y: "y \<in> S" and xy: "~(x = y \<and> S = {x})"
    2.52 +  obtains z where "z \<in> rel_frontier S" "y \<in> closed_segment x z"
    2.53 +                  "open_segment x z \<subseteq> rel_interior S"
    2.54 +proof (cases "x=y")
    2.55 +  case True
    2.56 +  with xy have "S \<noteq> {x}"
    2.57 +    by blast
    2.58 +  with True show ?thesis
    2.59 +    by (metis Set.set_insert all_not_in_conv ends_in_segment(1) insert_iff segment_to_rel_frontier_aux[OF S x] that y)
    2.60 +next
    2.61 +  case False
    2.62 +  then show ?thesis
    2.63 +    using segment_to_rel_frontier_aux [OF S x y] that by blast
    2.64 +qed
    2.65 +
    2.66  proposition rel_frontier_not_sing:
    2.67    fixes a :: "'a::euclidean_space"
    2.68    assumes "bounded S"
     3.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Tue Jul 18 11:35:32 2017 +0200
     3.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Wed Jul 19 16:41:26 2017 +0100
     3.3 @@ -3140,6 +3140,44 @@
     3.4  definition collinear :: "'a::real_vector set \<Rightarrow> bool"
     3.5    where "collinear S \<longleftrightarrow> (\<exists>u. \<forall>x \<in> S. \<forall> y \<in> S. \<exists>c. x - y = c *\<^sub>R u)"
     3.6  
     3.7 +lemma collinear_alt:
     3.8 +     "collinear S \<longleftrightarrow> (\<exists>u v. \<forall>x \<in> S. \<exists>c. x = u + c *\<^sub>R v)" (is "?lhs = ?rhs")
     3.9 +proof
    3.10 +  assume ?lhs
    3.11 +  then show ?rhs
    3.12 +    unfolding collinear_def by (metis Groups.add_ac(2) diff_add_cancel)
    3.13 +next
    3.14 +  assume ?rhs
    3.15 +  then obtain u v where *: "\<And>x. x \<in> S \<Longrightarrow> \<exists>c. x = u + c *\<^sub>R v"
    3.16 +    by (auto simp: )
    3.17 +  have "\<exists>c. x - y = c *\<^sub>R v" if "x \<in> S" "y \<in> S" for x y
    3.18 +        by (metis *[OF \<open>x \<in> S\<close>] *[OF \<open>y \<in> S\<close>] scaleR_left.diff add_diff_cancel_left)
    3.19 +  then show ?lhs
    3.20 +    using collinear_def by blast
    3.21 +qed
    3.22 +
    3.23 +lemma collinear:
    3.24 +  fixes S :: "'a::{perfect_space,real_vector} set"
    3.25 +  shows "collinear S \<longleftrightarrow> (\<exists>u. u \<noteq> 0 \<and> (\<forall>x \<in> S. \<forall> y \<in> S. \<exists>c. x - y = c *\<^sub>R u))"
    3.26 +proof -
    3.27 +  have "\<exists>v. v \<noteq> 0 \<and> (\<forall>x\<in>S. \<forall>y\<in>S. \<exists>c. x - y = c *\<^sub>R v)"
    3.28 +    if "\<forall>x\<in>S. \<forall>y\<in>S. \<exists>c. x - y = c *\<^sub>R u" "u=0" for u
    3.29 +  proof -
    3.30 +    have "\<forall>x\<in>S. \<forall>y\<in>S. x = y"
    3.31 +      using that by auto
    3.32 +    moreover
    3.33 +    obtain v::'a where "v \<noteq> 0"
    3.34 +      using UNIV_not_singleton [of 0] by auto
    3.35 +    ultimately have "\<forall>x\<in>S. \<forall>y\<in>S. \<exists>c. x - y = c *\<^sub>R v"
    3.36 +      by auto
    3.37 +    then show ?thesis
    3.38 +      using \<open>v \<noteq> 0\<close> by blast
    3.39 +  qed
    3.40 +  then show ?thesis
    3.41 +    apply (clarsimp simp: collinear_def)
    3.42 +    by (metis real_vector.scale_zero_right vector_fraction_eq_iff)
    3.43 +qed
    3.44 +
    3.45  lemma collinear_subset: "\<lbrakk>collinear T; S \<subseteq> T\<rbrakk> \<Longrightarrow> collinear S"
    3.46    by (meson collinear_def subsetCE)
    3.47  
     4.1 --- a/src/HOL/Analysis/Polytope.thy	Tue Jul 18 11:35:32 2017 +0200
     4.2 +++ b/src/HOL/Analysis/Polytope.thy	Wed Jul 19 16:41:26 2017 +0100
     4.3 @@ -74,9 +74,9 @@
     4.4    unfolding face_of_def by blast
     4.5  
     4.6  lemma face_of_imp_eq_affine_Int:
     4.7 -     fixes S :: "'a::euclidean_space set"
     4.8 -     assumes S: "convex S" "closed S" and T: "T face_of S"
     4.9 -     shows "T = (affine hull T) \<inter> S"
    4.10 +  fixes S :: "'a::euclidean_space set"
    4.11 +  assumes S: "convex S"  and T: "T face_of S"
    4.12 +  shows "T = (affine hull T) \<inter> S"
    4.13  proof -
    4.14    have "convex T" using T by (simp add: face_of_def)
    4.15    have *: False if x: "x \<in> affine hull T" and "x \<in> S" "x \<notin> T" and y: "y \<in> rel_interior T" for x y
    4.16 @@ -269,6 +269,20 @@
    4.17      by simp
    4.18  qed
    4.19  
    4.20 +lemma subset_of_face_of_affine_hull:
    4.21 +    fixes S :: "'a::euclidean_space set"
    4.22 +  assumes T: "T face_of S" and "convex S" "U \<subseteq> S" and dis: "~disjnt (affine hull T) (rel_interior U)"
    4.23 +  shows "U \<subseteq> T"
    4.24 +  apply (rule subset_of_face_of [OF T \<open>U \<subseteq> S\<close>])
    4.25 +  using face_of_imp_eq_affine_Int [OF \<open>convex S\<close> T]
    4.26 +  using rel_interior_subset [of U] dis
    4.27 +  using \<open>U \<subseteq> S\<close> disjnt_def by fastforce
    4.28 +
    4.29 +lemma affine_hull_face_of_disjoint_rel_interior:
    4.30 +    fixes S :: "'a::euclidean_space set"
    4.31 +  assumes "convex S" "F face_of S" "F \<noteq> S"
    4.32 +  shows "affine hull F \<inter> rel_interior S = {}"
    4.33 +  by (metis assms disjnt_def face_of_imp_subset order_refl subset_antisym subset_of_face_of_affine_hull)
    4.34  
    4.35  lemma affine_diff_divide:
    4.36      assumes "affine S" "k \<noteq> 0" "k \<noteq> 1" and xy: "x \<in> S" "y /\<^sub>R (1 - k) \<in> S"
    4.37 @@ -2160,9 +2174,8 @@
    4.38  
    4.39  lemma face_of_polyhedron_polyhedron:
    4.40    fixes S :: "'a :: euclidean_space set"
    4.41 -  assumes "polyhedron S" "c face_of S"
    4.42 -    shows "polyhedron c"
    4.43 -by (metis assms face_of_imp_eq_affine_Int polyhedron_Int polyhedron_affine_hull polyhedron_imp_closed polyhedron_imp_convex)
    4.44 +  assumes "polyhedron S" "c face_of S" shows "polyhedron c"
    4.45 +by (metis assms face_of_imp_eq_affine_Int polyhedron_Int polyhedron_affine_hull polyhedron_imp_convex)
    4.46  
    4.47  lemma finite_polyhedron_faces:
    4.48    fixes S :: "'a :: euclidean_space set"
    4.49 @@ -2778,4 +2791,130 @@
    4.50    qed (auto simp: eq poly aff face \<open>finite \<F>'\<close>)
    4.51  qed
    4.52  
    4.53 +
    4.54 +subsection\<open>Simplicial complexes and triangulations\<close>
    4.55 +
    4.56 +subsubsection\<open>The notion of n-simplex for integer @{term"n \<ge> -1"}\<close>
    4.57 +
    4.58 +definition simplex :: "int \<Rightarrow> 'a::euclidean_space set \<Rightarrow> bool" (infix "simplex" 50)
    4.59 +  where "n simplex S \<equiv> \<exists>C. ~(affine_dependent C) \<and> int(card C) = n + 1 \<and> S = convex hull C"
    4.60 +
    4.61 +lemma simplex:
    4.62 +    "n simplex S \<longleftrightarrow> (\<exists>C. finite C \<and>
    4.63 +                       ~(affine_dependent C) \<and>
    4.64 +                       int(card C) = n + 1 \<and>
    4.65 +                       S = convex hull C)"
    4.66 +  by (auto simp add: simplex_def intro: aff_independent_finite)
    4.67 +
    4.68 +lemma simplex_convex_hull:
    4.69 +   "~affine_dependent C \<and> int(card C) = n + 1 \<Longrightarrow> n simplex (convex hull C)"
    4.70 +  by (auto simp add: simplex_def)
    4.71 +
    4.72 +lemma convex_simplex: "n simplex S \<Longrightarrow> convex S"
    4.73 +  by (metis convex_convex_hull simplex_def)
    4.74 +
    4.75 +lemma compact_simplex: "n simplex S \<Longrightarrow> compact S"
    4.76 +  unfolding simplex
    4.77 +  using finite_imp_compact_convex_hull by blast
    4.78 +
    4.79 +lemma closed_simplex: "n simplex S \<Longrightarrow> closed S"
    4.80 +  by (simp add: compact_imp_closed compact_simplex)
    4.81 +
    4.82 +lemma simplex_imp_polytope:
    4.83 +   "n simplex S \<Longrightarrow> polytope S"
    4.84 +  unfolding simplex_def polytope_def
    4.85 +  using aff_independent_finite by blast
    4.86 +
    4.87 +lemma simplex_imp_polyhedron:
    4.88 +   "n simplex S \<Longrightarrow> polyhedron S"
    4.89 +  by (simp add: polytope_imp_polyhedron simplex_imp_polytope)
    4.90 +
    4.91 +lemma simplex_dim_ge: "n simplex S \<Longrightarrow> -1 \<le> n"
    4.92 +  by (metis (no_types, hide_lams) aff_dim_geq affine_independent_iff_card diff_add_cancel diff_diff_eq2 simplex_def)
    4.93 +
    4.94 +lemma simplex_empty [simp]: "n simplex {} \<longleftrightarrow> n = -1"
    4.95 +proof
    4.96 +  assume "n simplex {}"
    4.97 +  then show "n = -1"
    4.98 +    unfolding simplex by (metis card_empty convex_hull_eq_empty diff_0 diff_eq_eq of_nat_0)
    4.99 +next
   4.100 +  assume "n = -1" then show "n simplex {}"
   4.101 +    by (fastforce simp: simplex)
   4.102 +qed
   4.103 +
   4.104 +lemma simplex_minus_1 [simp]: "-1 simplex S \<longleftrightarrow> S = {}"
   4.105 +  by (metis simplex cancel_comm_monoid_add_class.diff_cancel card_0_eq diff_minus_eq_add of_nat_eq_0_iff simplex_empty)
   4.106 +
   4.107 +
   4.108 +lemma aff_dim_simplex:
   4.109 +   "n simplex S \<Longrightarrow> aff_dim S = n"
   4.110 +  by (metis simplex add.commute add_diff_cancel_left' aff_dim_convex_hull affine_independent_iff_card)
   4.111 +
   4.112 +lemma zero_simplex_sing: "0 simplex {a}"
   4.113 +  apply (simp add: simplex_def)
   4.114 +  by (metis affine_independent_1 card_empty card_insert_disjoint convex_hull_singleton empty_iff finite.emptyI)
   4.115 +
   4.116 +lemma simplex_sing [simp]: "n simplex {a} \<longleftrightarrow> n = 0"
   4.117 +  using aff_dim_simplex aff_dim_sing zero_simplex_sing by blast
   4.118 +
   4.119 +lemma simplex_zero: "0 simplex S \<longleftrightarrow> (\<exists>a. S = {a})"
   4.120 +apply (auto simp: )
   4.121 +  using aff_dim_eq_0 aff_dim_simplex by blast
   4.122 +
   4.123 +lemma one_simplex_segment: "a \<noteq> b \<Longrightarrow> 1 simplex closed_segment a b"
   4.124 +  apply (simp add: simplex_def)
   4.125 +  apply (rule_tac x="{a,b}" in exI)
   4.126 +  apply (auto simp: segment_convex_hull)
   4.127 +  done
   4.128 +
   4.129 +lemma simplex_segment_cases:
   4.130 +   "(if a = b then 0 else 1) simplex closed_segment a b"
   4.131 +  by (auto simp: one_simplex_segment)
   4.132 +
   4.133 +lemma simplex_segment:
   4.134 +   "\<exists>n. n simplex closed_segment a b"
   4.135 +  using simplex_segment_cases by metis
   4.136 +
   4.137 +lemma polytope_lowdim_imp_simplex:
   4.138 +  assumes "polytope P" "aff_dim P \<le> 1"
   4.139 +  obtains n where "n simplex P"
   4.140 +proof (cases "P = {}")
   4.141 +  case True
   4.142 +  then show ?thesis
   4.143 +    by (simp add: that)
   4.144 +next
   4.145 +  case False
   4.146 +  then show ?thesis
   4.147 +    by (metis assms compact_convex_collinear_segment collinear_aff_dim polytope_imp_compact polytope_imp_convex simplex_segment_cases that)
   4.148 +qed
   4.149 +
   4.150 +lemma simplex_insert_dimplus1:
   4.151 +  fixes n::int
   4.152 +  assumes "n simplex S" and a: "a \<notin> affine hull S"
   4.153 +  shows "(n+1) simplex (convex hull (insert a S))"
   4.154 +proof -
   4.155 +  obtain C where C: "finite C" "~(affine_dependent C)" "int(card C) = n+1" and S: "S = convex hull C"
   4.156 +    using assms unfolding simplex by force
   4.157 +  show ?thesis
   4.158 +    unfolding simplex
   4.159 +  proof (intro exI conjI)
   4.160 +      have "aff_dim S = n"
   4.161 +        using aff_dim_simplex assms(1) by blast
   4.162 +      moreover have "a \<notin> affine hull C"
   4.163 +        using S a affine_hull_convex_hull by blast
   4.164 +      moreover have "a \<notin> C"
   4.165 +          using S a hull_inc by fastforce
   4.166 +      ultimately show "\<not> affine_dependent (insert a C)"
   4.167 +        by (simp add: C S aff_dim_convex_hull aff_dim_insert affine_independent_iff_card)
   4.168 +  next
   4.169 +    have "a \<notin> C"
   4.170 +      using S a hull_inc by fastforce
   4.171 +    then show "int (card (insert a C)) = n + 1 + 1"
   4.172 +      by (simp add: C)
   4.173 +  next
   4.174 +    show "convex hull insert a S = convex hull (insert a C)"
   4.175 +      by (simp add: S convex_hull_insert_segments)
   4.176 +  qed (use C in auto)
   4.177 +qed
   4.178 +
   4.179  end