Theory of polyhedra: faces, extreme points, polytopes, and the Krein–Milman
authorpaulson <lp15@cam.ac.uk>
Tue May 10 14:04:44 2016 +0100 (2016-05-10 ago)
changeset 63078e49dc94eb624
parent 63077 844725394a37
child 63079 e9ad90ce926c
Theory of polyhedra: faces, extreme points, polytopes, and the Krein–Milman
Minkowski theorem
NEWS
src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy
src/HOL/Multivariate_Analysis/Polytope.thy
src/HOL/ROOT
     1.1 --- a/NEWS	Tue May 10 11:56:23 2016 +0100
     1.2 +++ b/NEWS	Tue May 10 14:04:44 2016 +0100
     1.3 @@ -158,7 +158,10 @@
     1.4  INCOMPATIBILITY.
     1.5  
     1.6  * More complex analysis including Cauchy's inequality, Liouville theorem,
     1.7 -open mapping theorem, maximum modulus principle, Schwarz Lemma.
     1.8 +open mapping theorem, maximum modulus principle, Residue theorem, Schwarz Lemma.
     1.9 +
    1.10 +* Theory of polyhedra: faces, extreme points, polytopes, and the Krein–Milman
    1.11 +Minkowski theorem.
    1.12  
    1.13  * "Gcd (f ` A)" and "Lcm (f ` A)" are printed with optional
    1.14  comprehension-like syntax analogously to "Inf (f ` A)" and "Sup (f ` A)".
     2.1 --- a/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy	Tue May 10 11:56:23 2016 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy	Tue May 10 14:04:44 2016 +0100
     2.3 @@ -6,6 +6,7 @@
     2.4    Ordered_Euclidean_Space
     2.5    Bounded_Continuous_Function
     2.6    Weierstrass
     2.7 +  Polytope
     2.8    Conformal_Mappings
     2.9    Generalised_Binomial_Theorem
    2.10    Gamma
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Multivariate_Analysis/Polytope.thy	Tue May 10 14:04:44 2016 +0100
     3.3 @@ -0,0 +1,2613 @@
     3.4 +section \<open>Faces, Extreme Points, Polytopes, Polyhedra etc.\<close>
     3.5 +
     3.6 +text\<open>Ported from HOL Light by L C Paulson\<close>
     3.7 +
     3.8 +theory Polytope
     3.9 +imports Cartesian_Euclidean_Space
    3.10 +begin
    3.11 +
    3.12 +subsection \<open>Faces of a (usually convex) set\<close>
    3.13 +
    3.14 +definition face_of :: "['a::real_vector set, 'a set] \<Rightarrow> bool" (infixr "(face'_of)" 50)
    3.15 +  where
    3.16 +  "T face_of S \<longleftrightarrow>
    3.17 +        T \<subseteq> S \<and> convex T \<and>
    3.18 +        (\<forall>a \<in> S. \<forall>b \<in> S. \<forall>x \<in> T. x \<in> open_segment a b \<longrightarrow> a \<in> T \<and> b \<in> T)"
    3.19 +
    3.20 +lemma face_ofD: "\<lbrakk>T face_of S; x \<in> open_segment a b; a \<in> S; b \<in> S; x \<in> T\<rbrakk> \<Longrightarrow> a \<in> T \<and> b \<in> T"
    3.21 +  unfolding face_of_def by blast
    3.22 +
    3.23 +lemma face_of_translation_eq [simp]:
    3.24 +    "(op + a ` T face_of op + a ` S) \<longleftrightarrow> T face_of S"
    3.25 +proof -
    3.26 +  have *: "\<And>a T S. T face_of S \<Longrightarrow> (op + a ` T face_of op + a ` S)"
    3.27 +    apply (simp add: face_of_def Ball_def, clarify)
    3.28 +    apply (drule open_segment_translation_eq [THEN iffD1])
    3.29 +    using inj_image_mem_iff inj_add_left apply metis
    3.30 +    done
    3.31 +  show ?thesis
    3.32 +    apply (rule iffI)
    3.33 +    apply (force simp: image_comp o_def dest: * [where a = "-a"])
    3.34 +    apply (blast intro: *)
    3.35 +    done
    3.36 +qed
    3.37 +
    3.38 +lemma face_of_linear_image:
    3.39 +  assumes "linear f" "inj f"
    3.40 +    shows "(f ` c face_of f ` S) \<longleftrightarrow> c face_of S"
    3.41 +by (simp add: face_of_def inj_image_subset_iff inj_image_mem_iff open_segment_linear_image assms)
    3.42 +
    3.43 +lemma face_of_refl: "convex S \<Longrightarrow> S face_of S"
    3.44 +  by (auto simp: face_of_def)
    3.45 +
    3.46 +lemma face_of_refl_eq: "S face_of S \<longleftrightarrow> convex S"
    3.47 +  by (auto simp: face_of_def)
    3.48 +
    3.49 +lemma empty_face_of [iff]: "{} face_of S"
    3.50 +  by (simp add: face_of_def)
    3.51 +
    3.52 +lemma face_of_empty [simp]: "S face_of {} \<longleftrightarrow> S = {}"
    3.53 +  by (meson empty_face_of face_of_def subset_empty)
    3.54 +
    3.55 +lemma face_of_trans [trans]: "\<lbrakk>S face_of T; T face_of u\<rbrakk> \<Longrightarrow> S face_of u"
    3.56 +  unfolding face_of_def by (safe; blast)
    3.57 +
    3.58 +lemma face_of_face: "T face_of S \<Longrightarrow> (f face_of T \<longleftrightarrow> f face_of S \<and> f \<subseteq> T)"
    3.59 +  unfolding face_of_def by (safe; blast)
    3.60 +
    3.61 +lemma face_of_subset: "\<lbrakk>F face_of S; F \<subseteq> T; T \<subseteq> S\<rbrakk> \<Longrightarrow> F face_of T"
    3.62 +  unfolding face_of_def by (safe; blast)
    3.63 +
    3.64 +lemma face_of_slice: "\<lbrakk>F face_of S; convex T\<rbrakk> \<Longrightarrow> (F \<inter> T) face_of (S \<inter> T)"
    3.65 +  unfolding face_of_def by (blast intro: convex_Int)
    3.66 +
    3.67 +lemma face_of_Int: "\<lbrakk>t1 face_of S; t2 face_of S\<rbrakk> \<Longrightarrow> (t1 \<inter> t2) face_of S"
    3.68 +  unfolding face_of_def by (blast intro: convex_Int)
    3.69 +
    3.70 +lemma face_of_Inter: "\<lbrakk>A \<noteq> {}; \<And>T. T \<in> A \<Longrightarrow> T face_of S\<rbrakk> \<Longrightarrow> (\<Inter> A) face_of S"
    3.71 +  unfolding face_of_def by (blast intro: convex_Inter)
    3.72 +
    3.73 +lemma face_of_Int_Int: "\<lbrakk>F face_of T; F' face_of t'\<rbrakk> \<Longrightarrow> (F \<inter> F') face_of (T \<inter> t')"
    3.74 +  unfolding face_of_def by (blast intro: convex_Int)
    3.75 +
    3.76 +lemma face_of_imp_subset: "T face_of S \<Longrightarrow> T \<subseteq> S"
    3.77 +  unfolding face_of_def by blast
    3.78 +
    3.79 +lemma face_of_imp_eq_affine_Int:
    3.80 +     fixes S :: "'a::euclidean_space set"
    3.81 +     assumes S: "convex S" "closed S" and T: "T face_of S"
    3.82 +     shows "T = (affine hull T) \<inter> S"
    3.83 +proof -
    3.84 +  have "convex T" using T by (simp add: face_of_def)
    3.85 +  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
    3.86 +  proof -
    3.87 +    obtain e where "e>0" and e: "cball y e \<inter> affine hull T \<subseteq> T"
    3.88 +      using y by (auto simp: rel_interior_cball)
    3.89 +    have "y \<noteq> x" "y \<in> S" "y \<in> T"
    3.90 +      using face_of_imp_subset rel_interior_subset T that by blast+
    3.91 +    then have zne: "\<And>u. \<lbrakk>u \<in> {0<..<1}; (1 - u) *\<^sub>R y + u *\<^sub>R x \<in> T\<rbrakk> \<Longrightarrow>  False"
    3.92 +      using \<open>x \<in> S\<close> \<open>x \<notin> T\<close> \<open>T face_of S\<close> unfolding face_of_def
    3.93 +      apply clarify
    3.94 +      apply (drule_tac x=x in bspec, assumption)
    3.95 +      apply (drule_tac x=y in bspec, assumption)
    3.96 +      apply (subst (asm) open_segment_commute)
    3.97 +      apply (force simp: open_segment_image_interval image_def)
    3.98 +      done
    3.99 +    have in01: "min (1/2) (e / norm (x - y)) \<in> {0<..<1}"
   3.100 +      using \<open>y \<noteq> x\<close> \<open>e > 0\<close> by simp
   3.101 +    show ?thesis
   3.102 +      apply (rule zne [OF in01])
   3.103 +      apply (rule e [THEN subsetD])
   3.104 +      apply (rule IntI)
   3.105 +        using `y \<noteq> x` \<open>e > 0\<close>
   3.106 +        apply (simp add: cball_def dist_norm algebra_simps)
   3.107 +        apply (simp add: Real_Vector_Spaces.scaleR_diff_right [symmetric] norm_minus_commute min_mult_distrib_right)
   3.108 +      apply (rule mem_affine [OF affine_affine_hull _ x])
   3.109 +      using \<open>y \<in> T\<close>  apply (auto simp: hull_inc)
   3.110 +      done
   3.111 +  qed
   3.112 +  show ?thesis
   3.113 +    apply (rule subset_antisym)
   3.114 +    using assms apply (simp add: hull_subset face_of_imp_subset)
   3.115 +    apply (cases "T={}", simp)
   3.116 +    apply (force simp: rel_interior_eq_empty [symmetric] \<open>convex T\<close> intro: *)
   3.117 +    done
   3.118 +qed
   3.119 +
   3.120 +lemma face_of_imp_closed:
   3.121 +     fixes S :: "'a::euclidean_space set"
   3.122 +     assumes "convex S" "closed S" "T face_of S" shows "closed T"
   3.123 +  by (metis affine_affine_hull affine_closed closed_Int face_of_imp_eq_affine_Int assms)
   3.124 +
   3.125 +lemma face_of_Int_supporting_hyperplane_le_strong:
   3.126 +    assumes "convex(S \<inter> {x. a \<bullet> x = b})" and aleb: "\<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b"
   3.127 +      shows "(S \<inter> {x. a \<bullet> x = b}) face_of S"
   3.128 +proof -
   3.129 +  have *: "a \<bullet> u = a \<bullet> x" if "x \<in> open_segment u v" "u \<in> S" "v \<in> S" and b: "b = a \<bullet> x"
   3.130 +          for u v x
   3.131 +  proof (rule antisym)
   3.132 +    show "a \<bullet> u \<le> a \<bullet> x"
   3.133 +      using aleb \<open>u \<in> S\<close> \<open>b = a \<bullet> x\<close> by blast
   3.134 +  next
   3.135 +    obtain \<xi> where "b = a \<bullet> ((1 - \<xi>) *\<^sub>R u + \<xi> *\<^sub>R v)" "0 < \<xi>" "\<xi> < 1"
   3.136 +      using \<open>b = a \<bullet> x\<close> \<open>x \<in> open_segment u v\<close> in_segment
   3.137 +      by (auto simp: open_segment_image_interval split: if_split_asm)
   3.138 +    then have "b + \<xi> * (a \<bullet> u) \<le> a \<bullet> u + \<xi> * b"
   3.139 +      using aleb [OF \<open>v \<in> S\<close>] by (simp add: algebra_simps)
   3.140 +    then have "(1 - \<xi>) * b \<le> (1 - \<xi>) * (a \<bullet> u)"
   3.141 +      by (simp add: algebra_simps)
   3.142 +    then have "b \<le> a \<bullet> u"
   3.143 +      using \<open>\<xi> < 1\<close> by auto
   3.144 +    with b show "a \<bullet> x \<le> a \<bullet> u" by simp
   3.145 +  qed
   3.146 +  show ?thesis
   3.147 +    apply (simp add: face_of_def assms)
   3.148 +    using "*" open_segment_commute by blast
   3.149 +qed
   3.150 +
   3.151 +lemma face_of_Int_supporting_hyperplane_ge_strong:
   3.152 +   "\<lbrakk>convex(S \<inter> {x. a \<bullet> x = b}); \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b\<rbrakk>
   3.153 +    \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) face_of S"
   3.154 +  using face_of_Int_supporting_hyperplane_le_strong [of S "-a" "-b"] by simp
   3.155 +
   3.156 +lemma face_of_Int_supporting_hyperplane_le:
   3.157 +    "\<lbrakk>convex S; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b\<rbrakk> \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) face_of S"
   3.158 +  by (simp add: convex_Int convex_hyperplane face_of_Int_supporting_hyperplane_le_strong)
   3.159 +
   3.160 +lemma face_of_Int_supporting_hyperplane_ge:
   3.161 +    "\<lbrakk>convex S; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b\<rbrakk> \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) face_of S"
   3.162 +  by (simp add: convex_Int convex_hyperplane face_of_Int_supporting_hyperplane_ge_strong)
   3.163 +
   3.164 +lemma face_of_imp_convex: "T face_of S \<Longrightarrow> convex T"
   3.165 +  using face_of_def by blast
   3.166 +
   3.167 +lemma face_of_imp_compact:
   3.168 +    fixes S :: "'a::euclidean_space set"
   3.169 +    shows "\<lbrakk>convex S; compact S; T face_of S\<rbrakk> \<Longrightarrow> compact T"
   3.170 +  by (meson bounded_subset compact_eq_bounded_closed face_of_imp_closed face_of_imp_subset)
   3.171 +
   3.172 +lemma face_of_Int_subface:
   3.173 +     "c1 \<inter> c2 face_of c1 \<and> c1 \<inter> c2 face_of c2 \<and> d1 face_of c1 \<and> d2 face_of c2
   3.174 +      \<Longrightarrow> (d1 \<inter> d2) face_of d1 \<and> (d1 \<inter> d2) face_of d2"
   3.175 +  by (meson face_of_Int_Int face_of_face inf_le1 inf_le2)
   3.176 +
   3.177 +lemma subset_of_face_of:
   3.178 +    fixes S :: "'a::real_normed_vector set"
   3.179 +    assumes "T face_of S" "u \<subseteq> S" "T \<inter> (rel_interior u) \<noteq> {}"
   3.180 +      shows "u \<subseteq> T"
   3.181 +proof
   3.182 +  fix c
   3.183 +  assume "c \<in> u"
   3.184 +  obtain b where "b \<in> T" "b \<in> rel_interior u" using assms by auto
   3.185 +  then obtain e where "e>0" "b \<in> u" and e: "cball b e \<inter> affine hull u \<subseteq> u"
   3.186 +    by (auto simp: rel_interior_cball)
   3.187 +  show "c \<in> T"
   3.188 +  proof (cases "b=c")
   3.189 +    case True with \<open>b \<in> T\<close> show ?thesis by blast
   3.190 +  next
   3.191 +    case False
   3.192 +    def d \<equiv> "b + (e / norm(b - c)) *\<^sub>R (b - c)"
   3.193 +    have "d \<in> cball b e \<inter> affine hull u"
   3.194 +      using \<open>e > 0\<close> \<open>b \<in> u\<close> \<open>c \<in> u\<close>
   3.195 +      by (simp add: d_def dist_norm hull_inc mem_affine_3_minus False)
   3.196 +    with e have "d \<in> u" by blast
   3.197 +    have nbc: "norm (b - c) + e > 0" using \<open>e > 0\<close>
   3.198 +      by (metis add.commute le_less_trans less_add_same_cancel2 norm_ge_zero)
   3.199 +    then have [simp]: "d \<noteq> c" using False scaleR_cancel_left [of "1 + (e / norm (b - c))" b c]
   3.200 +      by (simp add: algebra_simps d_def) (simp add: divide_simps)
   3.201 +    have [simp]: "((e - e * e / (e + norm (b - c))) / norm (b - c)) = (e / (e + norm (b - c)))"
   3.202 +      using False nbc
   3.203 +      apply (simp add: algebra_simps divide_simps)
   3.204 +      by (metis mult_eq_0_iff norm_eq_zero norm_imp_pos_and_ge norm_pths(2) real_scaleR_def scaleR_left.add zero_less_norm_iff)
   3.205 +    have "b \<in> open_segment d c"
   3.206 +      apply (simp add: open_segment_image_interval)
   3.207 +      apply (simp add: d_def algebra_simps image_def)
   3.208 +      apply (rule_tac x="e / (e + norm (b - c))" in bexI)
   3.209 +      using False nbc \<open>0 < e\<close>
   3.210 +      apply (auto simp: algebra_simps)
   3.211 +      done
   3.212 +    then have "d \<in> T \<and> c \<in> T"
   3.213 +      apply (rule face_ofD [OF \<open>T face_of S\<close>])
   3.214 +      using `d \<in> u`  `c \<in> u` \<open>u \<subseteq> S\<close>  \<open>b \<in> T\<close>  apply auto
   3.215 +      done
   3.216 +    then show ?thesis ..
   3.217 +  qed
   3.218 +qed
   3.219 +
   3.220 +lemma face_of_eq:
   3.221 +    fixes S :: "'a::real_normed_vector set"
   3.222 +    assumes "T face_of S" "u face_of S" "(rel_interior T) \<inter> (rel_interior u) \<noteq> {}"
   3.223 +      shows "T = u"
   3.224 +  apply (rule subset_antisym)
   3.225 +  apply (metis assms disjoint_iff_not_equal face_of_imp_subset rel_interior_subset subsetCE subset_of_face_of)
   3.226 +  by (metis assms disjoint_iff_not_equal face_of_imp_subset rel_interior_subset subset_iff subset_of_face_of)
   3.227 +
   3.228 +lemma face_of_disjoint_rel_interior:
   3.229 +      fixes S :: "'a::real_normed_vector set"
   3.230 +      assumes "T face_of S" "T \<noteq> S"
   3.231 +        shows "T \<inter> rel_interior S = {}"
   3.232 +  by (meson assms subset_of_face_of face_of_imp_subset order_refl subset_antisym)
   3.233 +
   3.234 +lemma face_of_disjoint_interior:
   3.235 +      fixes S :: "'a::real_normed_vector set"
   3.236 +      assumes "T face_of S" "T \<noteq> S"
   3.237 +        shows "T \<inter> interior S = {}"
   3.238 +proof -
   3.239 +  have "T \<inter> interior S \<subseteq> rel_interior S"
   3.240 +    by (meson inf_sup_ord(2) interior_subset_rel_interior order.trans)
   3.241 +  thus ?thesis
   3.242 +    by (metis (no_types) Int_greatest assms face_of_disjoint_rel_interior inf_sup_ord(1) subset_empty)
   3.243 +qed
   3.244 +
   3.245 +lemma face_of_subset_rel_boundary:
   3.246 +  fixes S :: "'a::real_normed_vector set"
   3.247 +  assumes "T face_of S" "T \<noteq> S"
   3.248 +    shows "T \<subseteq> (S - rel_interior S)"
   3.249 +by (meson DiffI assms disjoint_iff_not_equal face_of_disjoint_rel_interior face_of_imp_subset rev_subsetD subsetI)
   3.250 +
   3.251 +lemma face_of_subset_rel_frontier:
   3.252 +    fixes S :: "'a::real_normed_vector set"
   3.253 +    assumes "T face_of S" "T \<noteq> S"
   3.254 +      shows "T \<subseteq> rel_frontier S"
   3.255 +  using assms closure_subset face_of_disjoint_rel_interior face_of_imp_subset rel_frontier_def by fastforce
   3.256 +
   3.257 +lemma face_of_aff_dim_lt:
   3.258 +  fixes S :: "'a::euclidean_space set"
   3.259 +  assumes "convex S" "T face_of S" "T \<noteq> S"
   3.260 +    shows "aff_dim T < aff_dim S"
   3.261 +proof -
   3.262 +  have "aff_dim T \<le> aff_dim S"
   3.263 +    by (simp add: face_of_imp_subset aff_dim_subset assms)
   3.264 +  moreover have "aff_dim T \<noteq> aff_dim S"
   3.265 +  proof (cases "T = {}")
   3.266 +    case True then show ?thesis
   3.267 +      by (metis aff_dim_empty \<open>T \<noteq> S\<close>)
   3.268 +  next case False then show ?thesis
   3.269 +    by (metis Set.set_insert assms convex_rel_frontier_aff_dim dual_order.irrefl face_of_imp_convex face_of_subset_rel_frontier insert_not_empty subsetI)
   3.270 +  qed
   3.271 +  ultimately show ?thesis
   3.272 +    by simp
   3.273 +qed
   3.274 +
   3.275 +
   3.276 +lemma affine_diff_divide:
   3.277 +    assumes "affine S" "k \<noteq> 0" "k \<noteq> 1" and xy: "x \<in> S" "y /\<^sub>R (1 - k) \<in> S"
   3.278 +      shows "(x - y) /\<^sub>R k \<in> S"
   3.279 +proof -
   3.280 +  have "inverse(k) *\<^sub>R (x - y) = (1 - inverse k) *\<^sub>R inverse(1 - k) *\<^sub>R y + inverse(k) *\<^sub>R x"
   3.281 +    using assms
   3.282 +    by (simp add: algebra_simps) (simp add: scaleR_left_distrib [symmetric] divide_simps)
   3.283 +  then show ?thesis
   3.284 +    using \<open>affine S\<close> xy by (auto simp: affine_alt)
   3.285 +qed
   3.286 +
   3.287 +lemma face_of_convex_hulls:
   3.288 +      assumes S: "finite S" "T \<subseteq> S" and disj: "affine hull T \<inter> convex hull (S - T) = {}"
   3.289 +      shows  "(convex hull T) face_of (convex hull S)"
   3.290 +proof -
   3.291 +  have fin: "finite T" "finite (S - T)" using assms
   3.292 +    by (auto simp: finite_subset)
   3.293 +  have *: "x \<in> convex hull T"
   3.294 +          if x: "x \<in> convex hull S" and y: "y \<in> convex hull S" and w: "w \<in> convex hull T" "w \<in> open_segment x y"
   3.295 +          for x y w
   3.296 +  proof -
   3.297 +    have waff: "w \<in> affine hull T"
   3.298 +      using convex_hull_subset_affine_hull w by blast
   3.299 +    obtain a b where a: "\<And>i. i \<in> S \<Longrightarrow> 0 \<le> a i" and asum: "setsum a S = 1" and aeqx: "(\<Sum>i\<in>S. a i *\<^sub>R i) = x"
   3.300 +                 and b: "\<And>i. i \<in> S \<Longrightarrow> 0 \<le> b i" and bsum: "setsum b S = 1" and beqy: "(\<Sum>i\<in>S. b i *\<^sub>R i) = y"
   3.301 +      using x y by (auto simp: assms convex_hull_finite)
   3.302 +    obtain u where "(1 - u) *\<^sub>R x + u *\<^sub>R y \<in> convex hull T" "x \<noteq> y" and weq: "w = (1 - u) *\<^sub>R x + u *\<^sub>R y"
   3.303 +               and u01: "0 < u" "u < 1"
   3.304 +      using w by (auto simp: open_segment_image_interval split: if_split_asm)
   3.305 +    def c \<equiv> "\<lambda>i. (1 - u) * a i + u * b i"
   3.306 +    have cge0: "\<And>i. i \<in> S \<Longrightarrow> 0 \<le> c i"
   3.307 +      using a b u01 by (simp add: c_def)
   3.308 +    have sumc1: "setsum c S = 1"
   3.309 +      by (simp add: c_def setsum.distrib setsum_right_distrib [symmetric] asum bsum)
   3.310 +    have sumci_xy: "(\<Sum>i\<in>S. c i *\<^sub>R i) = (1 - u) *\<^sub>R x + u *\<^sub>R y"
   3.311 +      apply (simp add: c_def setsum.distrib scaleR_left_distrib)
   3.312 +      by (simp only: scaleR_scaleR [symmetric] Real_Vector_Spaces.scaleR_right.setsum [symmetric] aeqx beqy)
   3.313 +    show ?thesis
   3.314 +    proof (cases "setsum c (S - T) = 0")
   3.315 +      case True
   3.316 +      have ci0: "\<And>i. i \<in> (S - T) \<Longrightarrow> c i = 0"
   3.317 +        using True cge0 by (simp add: \<open>finite S\<close> setsum_nonneg_eq_0_iff)
   3.318 +      have a0: "a i = 0" if "i \<in> (S - T)" for i
   3.319 +        using ci0 [OF that] u01 a [of i] b [of i] that
   3.320 +        by (simp add: c_def Groups.ordered_comm_monoid_add_class.add_nonneg_eq_0_iff)
   3.321 +      have [simp]: "setsum a T = 1"
   3.322 +        using assms by (metis setsum.mono_neutral_cong_right a0 asum)
   3.323 +      show ?thesis
   3.324 +        apply (simp add: convex_hull_finite \<open>finite T\<close>)
   3.325 +        apply (rule_tac x=a in exI)
   3.326 +        using a0 assms
   3.327 +        apply (auto simp: cge0 a aeqx [symmetric] setsum.mono_neutral_right)
   3.328 +        done
   3.329 +    next
   3.330 +      case False
   3.331 +      def k \<equiv> "setsum c (S - T)"
   3.332 +      have "k > 0" using False
   3.333 +        unfolding k_def by (metis DiffD1 antisym_conv cge0 setsum_nonneg not_less)
   3.334 +      have weq_sumsum: "w = setsum (\<lambda>x. c x *\<^sub>R x) T + setsum (\<lambda>x. c x *\<^sub>R x) (S - T)"
   3.335 +        by (metis (no_types) add.commute S(1) S(2) setsum.subset_diff sumci_xy weq)
   3.336 +      show ?thesis
   3.337 +      proof (cases "k = 1")
   3.338 +        case True
   3.339 +        then have "setsum c T = 0"
   3.340 +          by (simp add: S k_def setsum_diff sumc1)
   3.341 +        then have [simp]: "setsum c (S - T) = 1"
   3.342 +          by (simp add: S setsum_diff sumc1)
   3.343 +        have ci0: "\<And>i. i \<in> T \<Longrightarrow> c i = 0"
   3.344 +          by (meson `finite T` `setsum c T = 0` \<open>T \<subseteq> S\<close> cge0 setsum_nonneg_eq_0_iff subsetCE)
   3.345 +        then have [simp]: "(\<Sum>i\<in>S-T. c i *\<^sub>R i) = w"
   3.346 +          by (simp add: weq_sumsum)
   3.347 +        have "w \<in> convex hull (S - T)"
   3.348 +          apply (simp add: convex_hull_finite fin)
   3.349 +          apply (rule_tac x=c in exI)
   3.350 +          apply (auto simp: cge0 weq True k_def)
   3.351 +          done
   3.352 +        then show ?thesis
   3.353 +          using disj waff by blast
   3.354 +      next
   3.355 +        case False
   3.356 +        then have sumcf: "setsum c T = 1 - k"
   3.357 +          by (simp add: S k_def setsum_diff sumc1)
   3.358 +        have "(\<Sum>i\<in>T. c i *\<^sub>R i) /\<^sub>R (1 - k) \<in> convex hull T"
   3.359 +          apply (simp add: convex_hull_finite fin)
   3.360 +          apply (rule_tac x="\<lambda>i. inverse (1-k) * c i" in exI)
   3.361 +          apply auto
   3.362 +          apply (metis sumcf cge0 inverse_nonnegative_iff_nonnegative mult_nonneg_nonneg S(2) setsum_nonneg subsetCE)
   3.363 +          apply (metis False mult.commute right_inverse right_minus_eq setsum_right_distrib sumcf)
   3.364 +          by (metis (mono_tags, lifting) scaleR_right.setsum scaleR_scaleR setsum.cong)
   3.365 +        with `0 < k`  have "inverse(k) *\<^sub>R (w - setsum (\<lambda>i. c i *\<^sub>R i) T) \<in> affine hull T"
   3.366 +          by (simp add: affine_diff_divide [OF affine_affine_hull] False waff convex_hull_subset_affine_hull [THEN subsetD])
   3.367 +        moreover have "inverse(k) *\<^sub>R (w - setsum (\<lambda>x. c x *\<^sub>R x) T) \<in> convex hull (S - T)"
   3.368 +          apply (simp add: weq_sumsum convex_hull_finite fin)
   3.369 +          apply (rule_tac x="\<lambda>i. inverse k * c i" in exI)
   3.370 +          using \<open>k > 0\<close> cge0
   3.371 +          apply (auto simp: scaleR_right.setsum setsum_right_distrib [symmetric] k_def [symmetric])
   3.372 +          done
   3.373 +        ultimately show ?thesis
   3.374 +          using disj by blast
   3.375 +      qed
   3.376 +    qed
   3.377 +  qed
   3.378 +  have [simp]: "convex hull T \<subseteq> convex hull S"
   3.379 +    by (simp add: \<open>T \<subseteq> S\<close> hull_mono)
   3.380 +  show ?thesis
   3.381 +    using open_segment_commute by (auto simp: face_of_def intro: *)
   3.382 +qed
   3.383 +
   3.384 +proposition face_of_convex_hull_insert:
   3.385 +   "\<lbrakk>finite S; a \<notin> affine hull S; T face_of convex hull S\<rbrakk> \<Longrightarrow> T face_of convex hull insert a S"
   3.386 +  apply (rule face_of_trans, blast)
   3.387 +  apply (rule face_of_convex_hulls; force simp: insert_Diff_if)
   3.388 +  done
   3.389 +
   3.390 +proposition face_of_affine_trivial:
   3.391 +    assumes "affine S" "T face_of S"
   3.392 +    shows "T = {} \<or> T = S"
   3.393 +proof (rule ccontr, clarsimp)
   3.394 +  assume "T \<noteq> {}" "T \<noteq> S"
   3.395 +  then obtain a where "a \<in> T" by auto
   3.396 +  then have "a \<in> S"
   3.397 +    using \<open>T face_of S\<close> face_of_imp_subset by blast
   3.398 +  have "S \<subseteq> T"
   3.399 +  proof
   3.400 +    fix b  assume "b \<in> S"
   3.401 +    show "b \<in> T"
   3.402 +    proof (cases "a = b")
   3.403 +      case True with \<open>a \<in> T\<close> show ?thesis by auto
   3.404 +    next
   3.405 +      case False
   3.406 +      then have "a \<in> open_segment (2 *\<^sub>R a - b) b"
   3.407 +        apply (auto simp: open_segment_def closed_segment_def)
   3.408 +        apply (rule_tac x="1/2" in exI)
   3.409 +        apply (simp add: algebra_simps)
   3.410 +        by (simp add: scaleR_2)
   3.411 +      moreover have "2 *\<^sub>R a - b \<in> S"
   3.412 +        by (rule mem_affine [OF \<open>affine S\<close> \<open>a \<in> S\<close> \<open>b \<in> S\<close>, of 2 "-1", simplified])
   3.413 +      moreover note \<open>b \<in> S\<close> \<open>a \<in> T\<close>
   3.414 +      ultimately show ?thesis
   3.415 +        by (rule face_ofD [OF \<open>T face_of S\<close>, THEN conjunct2])
   3.416 +    qed
   3.417 +  qed
   3.418 +  then show False
   3.419 +    using `T \<noteq> S` \<open>T face_of S\<close> face_of_imp_subset by blast
   3.420 +qed
   3.421 +
   3.422 +
   3.423 +lemma face_of_affine_eq:
   3.424 +   "affine S \<Longrightarrow> (T face_of S \<longleftrightarrow> T = {} \<or> T = S)"
   3.425 +using affine_imp_convex face_of_affine_trivial face_of_refl by auto
   3.426 +
   3.427 +
   3.428 +lemma Inter_faces_finite_altbound:
   3.429 +    fixes T :: "'a::euclidean_space set set"
   3.430 +    assumes cfaI: "\<And>c. c \<in> T \<Longrightarrow> c face_of S"
   3.431 +    shows "\<exists>F'. finite F' \<and> F' \<subseteq> T \<and> card F' \<le> DIM('a) + 2 \<and> \<Inter>F' = \<Inter>T"
   3.432 +proof (cases "\<forall>F'. finite F' \<and> F' \<subseteq> T \<and> card F' \<le> DIM('a) + 2 \<longrightarrow> (\<exists>c. c \<in> T \<and> c \<inter> (\<Inter>F') \<subset> (\<Inter>F'))")
   3.433 +  case True
   3.434 +  then obtain c where c:
   3.435 +       "\<And>F'. \<lbrakk>finite F'; F' \<subseteq> T; card F' \<le> DIM('a) + 2\<rbrakk> \<Longrightarrow> c F' \<in> T \<and> c F' \<inter> (\<Inter>F') \<subset> (\<Inter>F')"
   3.436 +    by metis
   3.437 +  def d \<equiv> "rec_nat {c{}} (\<lambda>n r. insert (c r) r)"
   3.438 +  have [simp]: "d 0 = {c {}}"
   3.439 +    by (simp add: d_def)
   3.440 +  have dSuc [simp]: "\<And>n. d (Suc n) = insert (c (d n)) (d n)"
   3.441 +    by (simp add: d_def)
   3.442 +  have dn_notempty: "d n \<noteq> {}" for n
   3.443 +    by (induction n) auto
   3.444 +  have dn_le_Suc: "d n \<subseteq> T \<and> finite(d n) \<and> card(d n) \<le> Suc n" if "n \<le> DIM('a) + 2" for n
   3.445 +  using that
   3.446 +  proof (induction n)
   3.447 +    case 0
   3.448 +    then show ?case by (simp add: c)
   3.449 +  next
   3.450 +    case (Suc n)
   3.451 +    then show ?case by (auto simp: c card_insert_if)
   3.452 +  qed
   3.453 +  have aff_dim_le: "aff_dim(\<Inter>(d n)) \<le> DIM('a) - int n" if "n \<le> DIM('a) + 2" for n
   3.454 +  using that
   3.455 +  proof (induction n)
   3.456 +    case 0
   3.457 +    then show ?case
   3.458 +      by (simp add: aff_dim_le_DIM)
   3.459 +  next
   3.460 +    case (Suc n)
   3.461 +    have fs: "\<Inter>d (Suc n) face_of S"
   3.462 +      by (meson Suc.prems cfaI dn_le_Suc dn_notempty face_of_Inter subsetCE)
   3.463 +    have condn: "convex (\<Inter>d n)"
   3.464 +      using Suc.prems nat_le_linear not_less_eq_eq
   3.465 +      by (blast intro: face_of_imp_convex cfaI convex_Inter dest: dn_le_Suc)
   3.466 +    have fdn: "\<Inter>d (Suc n) face_of \<Inter>d n"
   3.467 +      by (metis (no_types, lifting) Inter_anti_mono Suc.prems dSuc cfaI dn_le_Suc dn_notempty face_of_Inter face_of_imp_subset face_of_subset subset_iff subset_insertI)
   3.468 +    have ne: "\<Inter>d (Suc n) \<noteq> \<Inter>d n"
   3.469 +      by (metis (no_types, lifting) Suc.prems Suc_leD c complete_lattice_class.Inf_insert dSuc dn_le_Suc less_irrefl order.trans)
   3.470 +    have *: "\<And>m::int. \<And>d. \<And>d'::int. d < d' \<and> d' \<le> m - n \<Longrightarrow> d \<le> m - of_nat(n+1)"
   3.471 +      by arith
   3.472 +    have "aff_dim (\<Inter>d (Suc n)) < aff_dim (\<Inter>d n)"
   3.473 +      by (rule face_of_aff_dim_lt [OF condn fdn ne])
   3.474 +    moreover have "aff_dim (\<Inter>d n) \<le> int (DIM('a)) - int n"
   3.475 +      using Suc by auto
   3.476 +    ultimately
   3.477 +    have "aff_dim (\<Inter>d (Suc n)) \<le> int (DIM('a)) - (n+1)" by arith
   3.478 +    then show ?case by linarith
   3.479 +  qed
   3.480 +  have "aff_dim (\<Inter>d (DIM('a) + 2)) \<le> -2"
   3.481 +      using aff_dim_le [OF order_refl] by simp
   3.482 +  with aff_dim_geq [of "\<Inter>d (DIM('a) + 2)"] show ?thesis
   3.483 +    using order.trans by fastforce
   3.484 +next
   3.485 +  case False
   3.486 +  then show ?thesis
   3.487 +    apply simp
   3.488 +    apply (erule ex_forward)
   3.489 +    by blast
   3.490 +qed
   3.491 +
   3.492 +lemma faces_of_translation:
   3.493 +   "{F. F face_of image (\<lambda>x. a + x) S} = image (image (\<lambda>x. a + x)) {F. F face_of S}"
   3.494 +apply (rule subset_antisym, clarify)
   3.495 +apply (auto simp: image_iff)
   3.496 +apply (metis face_of_imp_subset face_of_translation_eq subset_imageE)
   3.497 +done
   3.498 +
   3.499 +proposition face_of_Times:
   3.500 +  assumes "F face_of S" and "F' face_of S'"
   3.501 +    shows "(F \<times> F') face_of (S \<times> S')"
   3.502 +proof -
   3.503 +  have "F \<times> F' \<subseteq> S \<times> S'"
   3.504 +    using assms [unfolded face_of_def] by blast
   3.505 +  moreover
   3.506 +  have "convex (F \<times> F')"
   3.507 +    using assms [unfolded face_of_def] by (blast intro: convex_Times)
   3.508 +  moreover
   3.509 +    have "a \<in> F \<and> a' \<in> F' \<and> b \<in> F \<and> b' \<in> F'"
   3.510 +       if "a \<in> S" "b \<in> S" "a' \<in> S'" "b' \<in> S'" "x \<in> F \<times> F'" "x \<in> open_segment (a,a') (b,b')"
   3.511 +       for a b a' b' x
   3.512 +  proof (cases "b=a \<or> b'=a'")
   3.513 +    case True with that show ?thesis
   3.514 +      using assms
   3.515 +      by (force simp: in_segment dest: face_ofD)
   3.516 +  next
   3.517 +    case False with assms [unfolded face_of_def] that show ?thesis
   3.518 +      by (blast dest!: open_segment_PairD)
   3.519 +  qed
   3.520 +  ultimately show ?thesis
   3.521 +    unfolding face_of_def by blast
   3.522 +qed
   3.523 +
   3.524 +corollary face_of_Times_decomp:
   3.525 +    fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
   3.526 +    shows "c face_of (S \<times> S') \<longleftrightarrow> (\<exists>F F'. F face_of S \<and> F' face_of S' \<and> c = F \<times> F')"
   3.527 +     (is "?lhs = ?rhs")
   3.528 +proof
   3.529 +  assume c: ?lhs
   3.530 +  show ?rhs
   3.531 +  proof (cases "c = {}")
   3.532 +    case True then show ?thesis by auto
   3.533 +  next
   3.534 +    case False
   3.535 +    have 1: "fst ` c \<subseteq> S" "snd ` c \<subseteq> S'"
   3.536 +      using c face_of_imp_subset by fastforce+
   3.537 +    have "convex c"
   3.538 +      using c by (metis face_of_imp_convex)
   3.539 +    have conv: "convex (fst ` c)" "convex (snd ` c)"
   3.540 +      by (simp_all add: \<open>convex c\<close> convex_linear_image fst_linear snd_linear)
   3.541 +    have fstab: "a \<in> fst ` c \<and> b \<in> fst ` c"
   3.542 +            if "a \<in> S" "b \<in> S" "x \<in> open_segment a b" "(x,x') \<in> c" for a b x x'
   3.543 +    proof -
   3.544 +      have *: "(x,x') \<in> open_segment (a,x') (b,x')"
   3.545 +        using that by (auto simp: in_segment)
   3.546 +      show ?thesis
   3.547 +        using face_ofD [OF c *] that face_of_imp_subset [OF c] by force
   3.548 +    qed
   3.549 +    have fst: "fst ` c face_of S"
   3.550 +      by (force simp: face_of_def 1 conv fstab)
   3.551 +    have sndab: "a' \<in> snd ` c \<and> b' \<in> snd ` c"
   3.552 +            if "a' \<in> S'" "b' \<in> S'" "x' \<in> open_segment a' b'" "(x,x') \<in> c" for a' b' x x'
   3.553 +    proof -
   3.554 +      have *: "(x,x') \<in> open_segment (x,a') (x,b')"
   3.555 +        using that by (auto simp: in_segment)
   3.556 +      show ?thesis
   3.557 +        using face_ofD [OF c *] that face_of_imp_subset [OF c] by force
   3.558 +    qed
   3.559 +    have snd: "snd ` c face_of S'"
   3.560 +      by (force simp: face_of_def 1 conv sndab)
   3.561 +    have cc: "rel_interior c \<subseteq> rel_interior (fst ` c) \<times> rel_interior (snd ` c)"
   3.562 +      by (force simp: face_of_Times rel_interior_Times conv fst snd \<open>convex c\<close> fst_linear snd_linear rel_interior_convex_linear_image [symmetric])
   3.563 +    have "c = fst ` c \<times> snd ` c"
   3.564 +      apply (rule face_of_eq [OF c])
   3.565 +      apply (simp_all add: face_of_Times rel_interior_Times conv fst snd)
   3.566 +      using False rel_interior_eq_empty \<open>convex c\<close> cc
   3.567 +      apply blast
   3.568 +      done
   3.569 +    with fst snd show ?thesis by metis
   3.570 +  qed
   3.571 +next
   3.572 +  assume ?rhs with face_of_Times show ?lhs by auto
   3.573 +qed
   3.574 +
   3.575 +lemma face_of_Times_eq:
   3.576 +    fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
   3.577 +    shows "(F \<times> F') face_of (S \<times> S') \<longleftrightarrow>
   3.578 +           F = {} \<or> F' = {} \<or> F face_of S \<and> F' face_of S'"
   3.579 +by (auto simp: face_of_Times_decomp times_eq_iff)
   3.580 +
   3.581 +lemma hyperplane_face_of_halfspace_le: "{x. a \<bullet> x = b} face_of {x. a \<bullet> x \<le> b}"
   3.582 +proof -
   3.583 +  have "{x. a \<bullet> x \<le> b} \<inter> {x. a \<bullet> x = b} = {x. a \<bullet> x = b}"
   3.584 +    by auto
   3.585 +  with face_of_Int_supporting_hyperplane_le [OF convex_halfspace_le [of a b], of a b]
   3.586 +  show ?thesis by auto
   3.587 +qed
   3.588 +
   3.589 +lemma hyperplane_face_of_halfspace_ge: "{x. a \<bullet> x = b} face_of {x. a \<bullet> x \<ge> b}"
   3.590 +proof -
   3.591 +  have "{x. a \<bullet> x \<ge> b} \<inter> {x. a \<bullet> x = b} = {x. a \<bullet> x = b}"
   3.592 +    by auto
   3.593 +  with face_of_Int_supporting_hyperplane_ge [OF convex_halfspace_ge [of b a], of b a]
   3.594 +  show ?thesis by auto
   3.595 +qed
   3.596 +
   3.597 +lemma face_of_halfspace_le:
   3.598 +  fixes a :: "'n::euclidean_space"
   3.599 +  shows "F face_of {x. a \<bullet> x \<le> b} \<longleftrightarrow>
   3.600 +         F = {} \<or> F = {x. a \<bullet> x = b} \<or> F = {x. a \<bullet> x \<le> b}"
   3.601 +     (is "?lhs = ?rhs")
   3.602 +proof (cases "a = 0")
   3.603 +  case True then show ?thesis
   3.604 +    using face_of_affine_eq affine_UNIV by auto
   3.605 +next
   3.606 +  case False
   3.607 +  then have ine: "interior {x. a \<bullet> x \<le> b} \<noteq> {}"
   3.608 +    using halfspace_eq_empty_lt interior_halfspace_le by blast
   3.609 +  show ?thesis
   3.610 +  proof
   3.611 +    assume L: ?lhs
   3.612 +    have "F \<noteq> {x. a \<bullet> x \<le> b} \<Longrightarrow> F face_of {x. a \<bullet> x = b}"
   3.613 +      using False
   3.614 +      apply (simp add: frontier_halfspace_le [symmetric] rel_frontier_nonempty_interior [OF ine, symmetric])
   3.615 +      apply (rule face_of_subset [OF L])
   3.616 +      apply (simp add: face_of_subset_rel_frontier [OF L])
   3.617 +      apply (force simp: rel_frontier_def closed_halfspace_le)
   3.618 +      done
   3.619 +    with L show ?rhs
   3.620 +      using affine_hyperplane face_of_affine_eq by blast
   3.621 +  next
   3.622 +    assume ?rhs
   3.623 +    then show ?lhs
   3.624 +      by (metis convex_halfspace_le empty_face_of face_of_refl hyperplane_face_of_halfspace_le)
   3.625 +  qed
   3.626 +qed
   3.627 +
   3.628 +lemma face_of_halfspace_ge:
   3.629 +  fixes a :: "'n::euclidean_space"
   3.630 +  shows "F face_of {x. a \<bullet> x \<ge> b} \<longleftrightarrow>
   3.631 +         F = {} \<or> F = {x. a \<bullet> x = b} \<or> F = {x. a \<bullet> x \<ge> b}"
   3.632 +using face_of_halfspace_le [of F "-a" "-b"] by simp
   3.633 +
   3.634 +subsection\<open>Exposed faces\<close>
   3.635 +
   3.636 +text\<open>That is, faces that are intersection with supporting hyperplane\<close>
   3.637 +
   3.638 +definition exposed_face_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"
   3.639 +                               (infixr "(exposed'_face'_of)" 50)
   3.640 +  where "T exposed_face_of S \<longleftrightarrow>
   3.641 +         T face_of S \<and> (\<exists>a b. S \<subseteq> {x. a \<bullet> x \<le> b} \<and> T = S \<inter> {x. a \<bullet> x = b})"
   3.642 +
   3.643 +lemma empty_exposed_face_of [iff]: "{} exposed_face_of S"
   3.644 +  apply (simp add: exposed_face_of_def)
   3.645 +  apply (rule_tac x=0 in exI)
   3.646 +  apply (rule_tac x=1 in exI, force)
   3.647 +  done
   3.648 +
   3.649 +lemma exposed_face_of_refl_eq [simp]: "S exposed_face_of S \<longleftrightarrow> convex S"
   3.650 +  apply (simp add: exposed_face_of_def face_of_refl_eq, auto)
   3.651 +  apply (rule_tac x=0 in exI)+
   3.652 +  apply force
   3.653 +  done
   3.654 +
   3.655 +lemma exposed_face_of_refl: "convex S \<Longrightarrow> S exposed_face_of S"
   3.656 +  by simp
   3.657 +
   3.658 +lemma exposed_face_of:
   3.659 +    "T exposed_face_of S \<longleftrightarrow>
   3.660 +     T face_of S \<and>
   3.661 +     (T = {} \<or> T = S \<or>
   3.662 +      (\<exists>a b. a \<noteq> 0 \<and> S \<subseteq> {x. a \<bullet> x \<le> b} \<and> T = S \<inter> {x. a \<bullet> x = b}))"
   3.663 +proof (cases "T = {}")
   3.664 +  case True then show ?thesis
   3.665 +    by simp
   3.666 +next
   3.667 +  case False
   3.668 +  show ?thesis
   3.669 +  proof (cases "T = S")
   3.670 +    case True then show ?thesis
   3.671 +      by (simp add: face_of_refl_eq)
   3.672 +  next
   3.673 +    case False
   3.674 +    with \<open>T \<noteq> {}\<close> show ?thesis
   3.675 +      apply (auto simp: exposed_face_of_def)
   3.676 +      apply (metis inner_zero_left)
   3.677 +      done
   3.678 +  qed
   3.679 +qed
   3.680 +
   3.681 +lemma exposed_face_of_Int_supporting_hyperplane_le:
   3.682 +   "\<lbrakk>convex S; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b\<rbrakk> \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) exposed_face_of S"
   3.683 +by (force simp: exposed_face_of_def face_of_Int_supporting_hyperplane_le)
   3.684 +
   3.685 +lemma exposed_face_of_Int_supporting_hyperplane_ge:
   3.686 +   "\<lbrakk>convex S; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b\<rbrakk> \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) exposed_face_of S"
   3.687 +using exposed_face_of_Int_supporting_hyperplane_le [of S "-a" "-b"] by simp
   3.688 +
   3.689 +proposition exposed_face_of_Int:
   3.690 +  assumes "T exposed_face_of S"
   3.691 +      and "u exposed_face_of S"
   3.692 +    shows "(T \<inter> u) exposed_face_of S"
   3.693 +proof -
   3.694 +  obtain a b where T: "S \<inter> {x. a \<bullet> x = b} face_of S"
   3.695 +               and S: "S \<subseteq> {x. a \<bullet> x \<le> b}"
   3.696 +               and teq: "T = S \<inter> {x. a \<bullet> x = b}"
   3.697 +    using assms by (auto simp: exposed_face_of_def)
   3.698 +  obtain a' b' where u: "S \<inter> {x. a' \<bullet> x = b'} face_of S"
   3.699 +                 and s': "S \<subseteq> {x. a' \<bullet> x \<le> b'}"
   3.700 +                 and ueq: "u = S \<inter> {x. a' \<bullet> x = b'}"
   3.701 +    using assms by (auto simp: exposed_face_of_def)
   3.702 +  have tu: "T \<inter> u face_of S"
   3.703 +    using T teq u ueq by (simp add: face_of_Int)
   3.704 +  have ss: "S \<subseteq> {x. (a + a') \<bullet> x \<le> b + b'}"
   3.705 +    using S s' by (force simp: inner_left_distrib)
   3.706 +  show ?thesis
   3.707 +    apply (simp add: exposed_face_of_def tu)
   3.708 +    apply (rule_tac x="a+a'" in exI)
   3.709 +    apply (rule_tac x="b+b'" in exI)
   3.710 +    using S s'
   3.711 +    apply (fastforce simp: ss inner_left_distrib teq ueq)
   3.712 +    done
   3.713 +qed
   3.714 +
   3.715 +proposition exposed_face_of_Inter:
   3.716 +    fixes P :: "'a::euclidean_space set set"
   3.717 +  assumes "P \<noteq> {}"
   3.718 +      and "\<And>T. T \<in> P \<Longrightarrow> T exposed_face_of S"
   3.719 +    shows "\<Inter>P exposed_face_of S"
   3.720 +proof -
   3.721 +  obtain Q where "finite Q" and QsubP: "Q \<subseteq> P" "card Q \<le> DIM('a) + 2" and IntQ: "\<Inter>Q = \<Inter>P"
   3.722 +    using Inter_faces_finite_altbound [of P S] assms [unfolded exposed_face_of]
   3.723 +    by force
   3.724 +  show ?thesis
   3.725 +  proof (cases "Q = {}")
   3.726 +    case True then show ?thesis
   3.727 +      by (metis Inf_empty Inf_lower IntQ assms ex_in_conv subset_antisym top_greatest)
   3.728 +  next
   3.729 +    case False
   3.730 +    have "Q \<subseteq> {T. T exposed_face_of S}"
   3.731 +      using QsubP assms by blast
   3.732 +    moreover have "Q \<subseteq> {T. T exposed_face_of S} \<Longrightarrow> \<Inter>Q exposed_face_of S"
   3.733 +      using \<open>finite Q\<close> False
   3.734 +      apply (induction Q rule: finite_induct)
   3.735 +      using exposed_face_of_Int apply fastforce+
   3.736 +      done
   3.737 +    ultimately show ?thesis
   3.738 +      by (simp add: IntQ)
   3.739 +  qed
   3.740 +qed
   3.741 +
   3.742 +proposition exposed_face_of_sums:
   3.743 +  assumes "convex S" and "convex T"
   3.744 +      and "F exposed_face_of {x + y | x y. x \<in> S \<and> y \<in> T}"
   3.745 +          (is "F exposed_face_of ?ST")
   3.746 +  obtains k l
   3.747 +    where "k exposed_face_of S" "l exposed_face_of T"
   3.748 +          "F = {x + y | x y. x \<in> k \<and> y \<in> l}"
   3.749 +proof (cases "F = {}")
   3.750 +  case True then show ?thesis
   3.751 +    using that by blast
   3.752 +next
   3.753 +  case False
   3.754 +  show ?thesis
   3.755 +  proof (cases "F = ?ST")
   3.756 +    case True then show ?thesis
   3.757 +      using assms exposed_face_of_refl_eq that by blast
   3.758 +  next
   3.759 +    case False
   3.760 +    obtain p where "p \<in> F" using \<open>F \<noteq> {}\<close> by blast
   3.761 +    moreover
   3.762 +    obtain u z where T: "?ST \<inter> {x. u \<bullet> x = z} face_of ?ST"
   3.763 +                 and S: "?ST \<subseteq> {x. u \<bullet> x \<le> z}"
   3.764 +                 and feq: "F = ?ST \<inter> {x. u \<bullet> x = z}"
   3.765 +      using assms by (auto simp: exposed_face_of_def)
   3.766 +    ultimately obtain a0 b0
   3.767 +            where p: "p = a0 + b0" and "a0 \<in> S" "b0 \<in> T" and z: "u \<bullet> p = z"
   3.768 +      by auto
   3.769 +    have lez: "u \<bullet> (x + y) \<le> z" if "x \<in> S" "y \<in> T" for x y
   3.770 +      using S that by auto
   3.771 +    have sef: "S \<inter> {x. u \<bullet> x = u \<bullet> a0} exposed_face_of S"
   3.772 +      apply (rule exposed_face_of_Int_supporting_hyperplane_le [OF \<open>convex S\<close>])
   3.773 +      apply (metis p z add_le_cancel_right inner_right_distrib lez [OF _ \<open>b0 \<in> T\<close>])
   3.774 +      done
   3.775 +    have tef: "T \<inter> {x. u \<bullet> x = u \<bullet> b0} exposed_face_of T"
   3.776 +      apply (rule exposed_face_of_Int_supporting_hyperplane_le [OF \<open>convex T\<close>])
   3.777 +      apply (metis p z add.commute add_le_cancel_right inner_right_distrib lez [OF \<open>a0 \<in> S\<close>])
   3.778 +      done
   3.779 +    have "{x + y |x y. x \<in> S \<and> u \<bullet> x = u \<bullet> a0 \<and> y \<in> T \<and> u \<bullet> y = u \<bullet> b0} \<subseteq> F"
   3.780 +      by (auto simp: feq) (metis inner_right_distrib p z)
   3.781 +    moreover have "F \<subseteq> {x + y |x y. x \<in> S \<and> u \<bullet> x = u \<bullet> a0 \<and> y \<in> T \<and> u \<bullet> y = u \<bullet> b0}"
   3.782 +      apply (auto simp: feq)
   3.783 +      apply (rename_tac x y)
   3.784 +      apply (rule_tac x=x in exI)
   3.785 +      apply (rule_tac x=y in exI, simp)
   3.786 +      using z p \<open>a0 \<in> S\<close> \<open>b0 \<in> T\<close>
   3.787 +      apply clarify
   3.788 +      apply (simp add: inner_right_distrib)
   3.789 +      apply (metis add_le_cancel_right antisym lez [unfolded inner_right_distrib] add.commute)
   3.790 +      done
   3.791 +    ultimately have "F = {x + y |x y. x \<in> S \<inter> {x. u \<bullet> x = u \<bullet> a0} \<and> y \<in> T \<inter> {x. u \<bullet> x = u \<bullet> b0}}"
   3.792 +      by blast
   3.793 +    then show ?thesis
   3.794 +      by (rule that [OF sef tef])
   3.795 +  qed
   3.796 +qed
   3.797 +
   3.798 +subsection\<open>Extreme points of a set: its singleton faces\<close>
   3.799 +
   3.800 +definition extreme_point_of :: "['a::real_vector, 'a set] \<Rightarrow> bool"
   3.801 +                               (infixr "(extreme'_point'_of)" 50)
   3.802 +  where "x extreme_point_of S \<longleftrightarrow>
   3.803 +         x \<in> S \<and> (\<forall>a \<in> S. \<forall>b \<in> S. x \<notin> open_segment a b)"
   3.804 +
   3.805 +lemma extreme_point_of_stillconvex:
   3.806 +   "convex S \<Longrightarrow> (x extreme_point_of S \<longleftrightarrow> x \<in> S \<and> convex(S - {x}))"
   3.807 +  by (fastforce simp add: convex_contains_segment extreme_point_of_def open_segment_def)
   3.808 +
   3.809 +lemma face_of_singleton:
   3.810 +   "{x} face_of S \<longleftrightarrow> x extreme_point_of S"
   3.811 +by (fastforce simp add: extreme_point_of_def face_of_def)
   3.812 +
   3.813 +lemma extreme_point_not_in_REL_INTERIOR:
   3.814 +    fixes S :: "'a::real_normed_vector set"
   3.815 +    shows "\<lbrakk>x extreme_point_of S; S \<noteq> {x}\<rbrakk> \<Longrightarrow> x \<notin> rel_interior S"
   3.816 +apply (simp add: face_of_singleton [symmetric])
   3.817 +apply (blast dest: face_of_disjoint_rel_interior)
   3.818 +done
   3.819 +
   3.820 +lemma extreme_point_not_in_interior:
   3.821 +    fixes S :: "'a::{real_normed_vector, perfect_space} set"
   3.822 +    shows "x extreme_point_of S \<Longrightarrow> x \<notin> interior S"
   3.823 +apply (case_tac "S = {x}")
   3.824 +apply (simp add: empty_interior_finite)
   3.825 +by (meson contra_subsetD extreme_point_not_in_REL_INTERIOR interior_subset_rel_interior)
   3.826 +
   3.827 +lemma extreme_point_of_face:
   3.828 +     "F face_of S \<Longrightarrow> v extreme_point_of F \<longleftrightarrow> v extreme_point_of S \<and> v \<in> F"
   3.829 +  by (meson empty_subsetI face_of_face face_of_singleton insert_subset)
   3.830 +
   3.831 +lemma extreme_point_of_convex_hull:
   3.832 +   "x extreme_point_of (convex hull S) \<Longrightarrow> x \<in> S"
   3.833 +apply (simp add: extreme_point_of_stillconvex)
   3.834 +using hull_minimal [of S "(convex hull S) - {x}" convex]
   3.835 +using hull_subset [of S convex]
   3.836 +apply blast
   3.837 +done
   3.838 +
   3.839 +lemma extreme_points_of_convex_hull:
   3.840 +   "{x. x extreme_point_of (convex hull S)} \<subseteq> S"
   3.841 +using extreme_point_of_convex_hull by auto
   3.842 +
   3.843 +lemma extreme_point_of_empty [simp]: "~ (x extreme_point_of {})"
   3.844 +  by (simp add: extreme_point_of_def)
   3.845 +
   3.846 +lemma extreme_point_of_singleton [iff]: "x extreme_point_of {a} \<longleftrightarrow> x = a"
   3.847 +  using extreme_point_of_stillconvex by auto
   3.848 +
   3.849 +lemma extreme_point_of_translation_eq:
   3.850 +   "(a + x) extreme_point_of (image (\<lambda>x. a + x) S) \<longleftrightarrow> x extreme_point_of S"
   3.851 +by (auto simp: extreme_point_of_def)
   3.852 +
   3.853 +lemma extreme_points_of_translation:
   3.854 +   "{x. x extreme_point_of (image (\<lambda>x. a + x) S)} =
   3.855 +    (\<lambda>x. a + x) ` {x. x extreme_point_of S}"
   3.856 +using extreme_point_of_translation_eq
   3.857 +by auto (metis (no_types, lifting) image_iff mem_Collect_eq minus_add_cancel)
   3.858 +
   3.859 +lemma extreme_point_of_Int:
   3.860 +   "\<lbrakk>x extreme_point_of S; x extreme_point_of T\<rbrakk> \<Longrightarrow> x extreme_point_of (S \<inter> T)"
   3.861 +by (simp add: extreme_point_of_def)
   3.862 +
   3.863 +lemma extreme_point_of_Int_supporting_hyperplane_le:
   3.864 +   "\<lbrakk>S \<inter> {x. a \<bullet> x = b} = {c}; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b\<rbrakk> \<Longrightarrow> c extreme_point_of S"
   3.865 +apply (simp add: face_of_singleton [symmetric])
   3.866 +by (metis face_of_Int_supporting_hyperplane_le_strong convex_singleton)
   3.867 +
   3.868 +lemma extreme_point_of_Int_supporting_hyperplane_ge:
   3.869 +   "\<lbrakk>S \<inter> {x. a \<bullet> x = b} = {c}; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b\<rbrakk> \<Longrightarrow> c extreme_point_of S"
   3.870 +apply (simp add: face_of_singleton [symmetric])
   3.871 +by (metis face_of_Int_supporting_hyperplane_ge_strong convex_singleton)
   3.872 +
   3.873 +lemma exposed_point_of_Int_supporting_hyperplane_le:
   3.874 +   "\<lbrakk>S \<inter> {x. a \<bullet> x = b} = {c}; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b\<rbrakk> \<Longrightarrow> {c} exposed_face_of S"
   3.875 +apply (simp add: exposed_face_of_def face_of_singleton)
   3.876 +apply (force simp: extreme_point_of_Int_supporting_hyperplane_le)
   3.877 +done
   3.878 +
   3.879 +lemma exposed_point_of_Int_supporting_hyperplane_ge:
   3.880 +    "\<lbrakk>S \<inter> {x. a \<bullet> x = b} = {c}; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b\<rbrakk> \<Longrightarrow> {c} exposed_face_of S"
   3.881 +using exposed_point_of_Int_supporting_hyperplane_le [of S "-a" "-b" c]
   3.882 +by simp
   3.883 +
   3.884 +lemma extreme_point_of_convex_hull_insert:
   3.885 +   "\<lbrakk>finite S; a \<notin> convex hull S\<rbrakk> \<Longrightarrow> a extreme_point_of (convex hull (insert a S))"
   3.886 +apply (case_tac "a \<in> S")
   3.887 +apply (simp add: hull_inc)
   3.888 +using face_of_convex_hulls [of "insert a S" "{a}"]
   3.889 +apply (auto simp: face_of_singleton hull_same)
   3.890 +done
   3.891 +
   3.892 +subsection\<open>Facets\<close>
   3.893 +
   3.894 +definition facet_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"
   3.895 +                    (infixr "(facet'_of)" 50)
   3.896 +  where "F facet_of S \<longleftrightarrow> F face_of S \<and> F \<noteq> {} \<and> aff_dim F = aff_dim S - 1"
   3.897 +
   3.898 +lemma facet_of_empty [simp]: "~ S facet_of {}"
   3.899 +  by (simp add: facet_of_def)
   3.900 +
   3.901 +lemma facet_of_irrefl [simp]: "~ S facet_of S "
   3.902 +  by (simp add: facet_of_def)
   3.903 +
   3.904 +lemma facet_of_imp_face_of: "F facet_of S \<Longrightarrow> F face_of S"
   3.905 +  by (simp add: facet_of_def)
   3.906 +
   3.907 +lemma facet_of_imp_subset: "F facet_of S \<Longrightarrow> F \<subseteq> S"
   3.908 +  by (simp add: face_of_imp_subset facet_of_def)
   3.909 +
   3.910 +lemma hyperplane_facet_of_halfspace_le:
   3.911 +   "a \<noteq> 0 \<Longrightarrow> {x. a \<bullet> x = b} facet_of {x. a \<bullet> x \<le> b}"
   3.912 +unfolding facet_of_def hyperplane_eq_empty
   3.913 +by (auto simp: hyperplane_face_of_halfspace_ge hyperplane_face_of_halfspace_le
   3.914 +           DIM_positive Suc_leI of_nat_diff aff_dim_halfspace_le)
   3.915 +
   3.916 +lemma hyperplane_facet_of_halfspace_ge:
   3.917 +    "a \<noteq> 0 \<Longrightarrow> {x. a \<bullet> x = b} facet_of {x. a \<bullet> x \<ge> b}"
   3.918 +unfolding facet_of_def hyperplane_eq_empty
   3.919 +by (auto simp: hyperplane_face_of_halfspace_le hyperplane_face_of_halfspace_ge
   3.920 +           DIM_positive Suc_leI of_nat_diff aff_dim_halfspace_ge)
   3.921 +
   3.922 +lemma facet_of_halfspace_le:
   3.923 +    "F facet_of {x. a \<bullet> x \<le> b} \<longleftrightarrow> a \<noteq> 0 \<and> F = {x. a \<bullet> x = b}"
   3.924 +    (is "?lhs = ?rhs")
   3.925 +proof
   3.926 +  assume c: ?lhs
   3.927 +  with c facet_of_irrefl show ?rhs
   3.928 +    by (force simp: aff_dim_halfspace_le facet_of_def face_of_halfspace_le cong: conj_cong split: if_split_asm)
   3.929 +next
   3.930 +  assume ?rhs then show ?lhs
   3.931 +    by (simp add: hyperplane_facet_of_halfspace_le)
   3.932 +qed
   3.933 +
   3.934 +lemma facet_of_halfspace_ge:
   3.935 +    "F facet_of {x. a \<bullet> x \<ge> b} \<longleftrightarrow> a \<noteq> 0 \<and> F = {x. a \<bullet> x = b}"
   3.936 +using facet_of_halfspace_le [of F "-a" "-b"] by simp
   3.937 +
   3.938 +subsection \<open>Edges: faces of affine dimension 1\<close>
   3.939 +
   3.940 +definition edge_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"  (infixr "(edge'_of)" 50)
   3.941 +  where "e edge_of S \<longleftrightarrow> e face_of S \<and> aff_dim e = 1"
   3.942 +
   3.943 +lemma edge_of_imp_subset:
   3.944 +   "S edge_of T \<Longrightarrow> S \<subseteq> T"
   3.945 +by (simp add: edge_of_def face_of_imp_subset)
   3.946 +
   3.947 +subsection\<open>Existence of extreme points\<close>
   3.948 +
   3.949 +lemma different_norm_3_collinear_points:
   3.950 +  fixes a :: "'a::euclidean_space"
   3.951 +  assumes "x \<in> open_segment a b" "norm(a) = norm(b)" "norm(x) = norm(b)"
   3.952 +  shows False
   3.953 +proof -
   3.954 +  obtain u where "norm ((1 - u) *\<^sub>R a + u *\<^sub>R b) = norm b"
   3.955 +             and "a \<noteq> b"
   3.956 +             and u01: "0 < u" "u < 1"
   3.957 +    using assms by (auto simp: open_segment_image_interval if_splits)
   3.958 +  then have "(1 - u) *\<^sub>R a \<bullet> (1 - u) *\<^sub>R a + ((1 - u) * 2) *\<^sub>R a \<bullet> u *\<^sub>R b =
   3.959 +             (1 - u * u) *\<^sub>R (a \<bullet> a)"
   3.960 +    using assms by (simp add: norm_eq algebra_simps inner_commute)
   3.961 +  then have "(1 - u) *\<^sub>R ((1 - u) *\<^sub>R a \<bullet> a + (2 * u) *\<^sub>R  a \<bullet> b) =
   3.962 +             (1 - u) *\<^sub>R ((1 + u) *\<^sub>R (a \<bullet> a))"
   3.963 +    by (simp add: algebra_simps)
   3.964 +  then have "(1 - u) *\<^sub>R (a \<bullet> a) + (2 * u) *\<^sub>R (a \<bullet> b) = (1 + u) *\<^sub>R (a \<bullet> a)"
   3.965 +    using u01 by auto
   3.966 +  then have "a \<bullet> b = a \<bullet> a"
   3.967 +    using u01 by (simp add: algebra_simps)
   3.968 +  then have "a = b"
   3.969 +    using \<open>norm(a) = norm(b)\<close> norm_eq vector_eq by fastforce
   3.970 +  then show ?thesis
   3.971 +    using \<open>a \<noteq> b\<close> by force
   3.972 +qed
   3.973 +
   3.974 +proposition extreme_point_exists_convex:
   3.975 +  fixes S :: "'a::euclidean_space set"
   3.976 +  assumes "compact S" "convex S" "S \<noteq> {}"
   3.977 +  obtains x where "x extreme_point_of S"
   3.978 +proof -
   3.979 +  obtain x where "x \<in> S" and xsup: "\<And>y. y \<in> S \<Longrightarrow> norm y \<le> norm x"
   3.980 +    using distance_attains_sup [of S 0] assms by auto
   3.981 +  have False if "a \<in> S" "b \<in> S" and x: "x \<in> open_segment a b" for a b
   3.982 +  proof -
   3.983 +    have noax: "norm a \<le> norm x" and nobx: "norm b \<le> norm x" using xsup that by auto
   3.984 +    have "a \<noteq> b"
   3.985 +      using empty_iff open_segment_idem x by auto
   3.986 +    have *: "(1 - u) * na + u * nb < norm x" if "na < norm x"  "nb \<le> norm x" "0 < u" "u < 1" for na nb u
   3.987 +    proof -
   3.988 +      have "(1 - u) * na + u * nb < (1 - u) * norm x + u * nb"
   3.989 +        by (simp add: that)
   3.990 +      also have "... \<le> (1 - u) * norm x + u * norm x"
   3.991 +        by (simp add: that)
   3.992 +      finally have "(1 - u) * na + u * nb < (1 - u) * norm x + u * norm x" .
   3.993 +      then show ?thesis
   3.994 +      using scaleR_collapse [symmetric, of "norm x" u] by auto
   3.995 +    qed
   3.996 +    have "norm x < norm x" if "norm a < norm x"
   3.997 +      using x
   3.998 +      apply (clarsimp simp only: open_segment_image_interval \<open>a \<noteq> b\<close> if_False)
   3.999 +      apply (rule norm_triangle_lt)
  3.1000 +      apply (simp add: norm_mult)
  3.1001 +      using * [of "norm a" "norm b"] nobx that
  3.1002 +        apply blast
  3.1003 +      done
  3.1004 +    moreover have "norm x < norm x" if "norm b < norm x"
  3.1005 +      using x
  3.1006 +      apply (clarsimp simp only: open_segment_image_interval \<open>a \<noteq> b\<close> if_False)
  3.1007 +      apply (rule norm_triangle_lt)
  3.1008 +      apply (simp add: norm_mult)
  3.1009 +      using * [of "norm b" "norm a" "1-u" for u] noax that
  3.1010 +        apply (simp add: add.commute)
  3.1011 +      done
  3.1012 +    ultimately have "~ (norm a < norm x) \<and> ~ (norm b < norm x)"
  3.1013 +      by auto
  3.1014 +    then show ?thesis
  3.1015 +      using different_norm_3_collinear_points noax nobx that(3) by fastforce
  3.1016 +  qed
  3.1017 +  then show ?thesis
  3.1018 +    apply (rule_tac x=x in that)
  3.1019 +    apply (force simp: extreme_point_of_def \<open>x \<in> S\<close>)
  3.1020 +    done
  3.1021 +qed
  3.1022 +
  3.1023 +subsection\<open>Krein-Milman, the weaker form\<close>
  3.1024 +
  3.1025 +proposition Krein_Milman:
  3.1026 +  fixes S :: "'a::euclidean_space set"
  3.1027 +  assumes "compact S" "convex S"
  3.1028 +    shows "S = closure(convex hull {x. x extreme_point_of S})"
  3.1029 +proof (cases "S = {}")
  3.1030 +  case True then show ?thesis   by simp
  3.1031 +next
  3.1032 +  case False
  3.1033 +  have "closed S"
  3.1034 +    by (simp add: \<open>compact S\<close> compact_imp_closed)
  3.1035 +  have "closure (convex hull {x. x extreme_point_of S}) \<subseteq> S"
  3.1036 +    apply (rule closure_minimal [OF hull_minimal \<open>closed S\<close>])
  3.1037 +    using assms
  3.1038 +    apply (auto simp: extreme_point_of_def)
  3.1039 +    done
  3.1040 +  moreover have "u \<in> closure (convex hull {x. x extreme_point_of S})"
  3.1041 +                if "u \<in> S" for u
  3.1042 +  proof (rule ccontr)
  3.1043 +    assume unot: "u \<notin> closure(convex hull {x. x extreme_point_of S})"
  3.1044 +    then obtain a b where "a \<bullet> u < b"
  3.1045 +          and ab: "\<And>x. x \<in> closure(convex hull {x. x extreme_point_of S}) \<Longrightarrow> b < a \<bullet> x"
  3.1046 +      using separating_hyperplane_closed_point [of "closure(convex hull {x. x extreme_point_of S})"]
  3.1047 +      by blast
  3.1048 +    have "continuous_on S (op \<bullet> a)"
  3.1049 +      by (rule continuous_intros)+
  3.1050 +    then obtain m where "m \<in> S" and m: "\<And>y. y \<in> S \<Longrightarrow> a \<bullet> m \<le> a \<bullet> y"
  3.1051 +      using continuous_attains_inf [of S "\<lambda>x. a \<bullet> x"] \<open>compact S\<close> \<open>u \<in> S\<close>
  3.1052 +      by auto
  3.1053 +    def T \<equiv> "S \<inter> {x. a \<bullet> x = a \<bullet> m}"
  3.1054 +    have "m \<in> T"
  3.1055 +      by (simp add: T_def \<open>m \<in> S\<close>)
  3.1056 +    moreover have "compact T"
  3.1057 +      by (simp add: T_def compact_Int_closed [OF \<open>compact S\<close> closed_hyperplane])
  3.1058 +    moreover have "convex T"
  3.1059 +      by (simp add: T_def convex_Int [OF \<open>convex S\<close> convex_hyperplane])
  3.1060 +    ultimately obtain v where v: "v extreme_point_of T"
  3.1061 +      using extreme_point_exists_convex [of T] by auto
  3.1062 +    then have "{v} face_of T"
  3.1063 +      by (simp add: face_of_singleton)
  3.1064 +    also have "T face_of S"
  3.1065 +      by (simp add: T_def m face_of_Int_supporting_hyperplane_ge [OF \<open>convex S\<close>])
  3.1066 +    finally have "v extreme_point_of S"
  3.1067 +      by (simp add: face_of_singleton)
  3.1068 +    then have "b < a \<bullet> v"
  3.1069 +      using closure_subset by (simp add: closure_hull hull_inc ab)
  3.1070 +    then show False
  3.1071 +      using \<open>a \<bullet> u < b\<close> \<open>{v} face_of T\<close> face_of_imp_subset m T_def that by fastforce
  3.1072 +  qed
  3.1073 +  ultimately show ?thesis
  3.1074 +    by blast
  3.1075 +qed
  3.1076 +
  3.1077 +text\<open>Now the sharper form.\<close>
  3.1078 +
  3.1079 +lemma Krein_Milman_Minkowski_aux:
  3.1080 +  fixes S :: "'a::euclidean_space set"
  3.1081 +  assumes n: "dim S = n" and S: "compact S" "convex S" "0 \<in> S"
  3.1082 +    shows "0 \<in> convex hull {x. x extreme_point_of S}"
  3.1083 +using n S
  3.1084 +proof (induction n arbitrary: S rule: less_induct)
  3.1085 +  case (less n S) show ?case
  3.1086 +  proof (cases "0 \<in> rel_interior S")
  3.1087 +    case True with Krein_Milman show ?thesis
  3.1088 +      by (metis subsetD convex_convex_hull convex_rel_interior_closure less.prems(2) less.prems(3) rel_interior_subset)
  3.1089 +  next
  3.1090 +    case False
  3.1091 +    have "rel_interior S \<noteq> {}"
  3.1092 +      by (simp add: rel_interior_convex_nonempty_aux less)
  3.1093 +    then obtain c where c: "c \<in> rel_interior S" by blast
  3.1094 +    obtain a where "a \<noteq> 0"
  3.1095 +              and le_ay: "\<And>y. y \<in> S \<Longrightarrow> a \<bullet> 0 \<le> a \<bullet> y"
  3.1096 +              and less_ay: "\<And>y. y \<in> rel_interior S \<Longrightarrow> a \<bullet> 0 < a \<bullet> y"
  3.1097 +      by (blast intro: supporting_hyperplane_rel_boundary intro!: less False)
  3.1098 +    have face: "S \<inter> {x. a \<bullet> x = 0} face_of S"
  3.1099 +      apply (rule face_of_Int_supporting_hyperplane_ge [OF \<open>convex S\<close>])
  3.1100 +      using le_ay by auto
  3.1101 +    then have co: "compact (S \<inter> {x. a \<bullet> x = 0})" "convex (S \<inter> {x. a \<bullet> x = 0})"
  3.1102 +      using less.prems by (blast intro: face_of_imp_compact face_of_imp_convex)+
  3.1103 +    have "a \<bullet> y = 0" if "y \<in> span (S \<inter> {x. a \<bullet> x = 0})" for y
  3.1104 +    proof -
  3.1105 +      have "y \<in> span {x. a \<bullet> x = 0}"
  3.1106 +        by (metis inf.cobounded2 span_mono subsetCE that)
  3.1107 +      then have "y \<in> {x. a \<bullet> x = 0}"
  3.1108 +        by (rule span_induct [OF _ subspace_hyperplane])
  3.1109 +      then show ?thesis by simp
  3.1110 +    qed
  3.1111 +    then have "dim (S \<inter> {x. a \<bullet> x = 0}) < n"
  3.1112 +      by (metis (no_types) less_ay c subsetD dim_eq_span inf.strict_order_iff
  3.1113 +           inf_le1 \<open>dim S = n\<close> not_le rel_interior_subset span_0 span_clauses(1))
  3.1114 +    then have "0 \<in> convex hull {x. x extreme_point_of (S \<inter> {x. a \<bullet> x = 0})}"
  3.1115 +      by (rule less.IH) (auto simp: co less.prems)
  3.1116 +    then show ?thesis
  3.1117 +      by (metis (mono_tags, lifting) Collect_mono_iff \<open>S \<inter> {x. a \<bullet> x = 0} face_of S\<close> extreme_point_of_face hull_mono subset_iff)
  3.1118 +  qed
  3.1119 +qed
  3.1120 +
  3.1121 +
  3.1122 +theorem Krein_Milman_Minkowski:
  3.1123 +  fixes S :: "'a::euclidean_space set"
  3.1124 +  assumes "compact S" "convex S"
  3.1125 +    shows "S = convex hull {x. x extreme_point_of S}"
  3.1126 +proof
  3.1127 +  show "S \<subseteq> convex hull {x. x extreme_point_of S}"
  3.1128 +  proof
  3.1129 +    fix a assume [simp]: "a \<in> S"
  3.1130 +    have 1: "compact (op + (- a) ` S)"
  3.1131 +      by (simp add: \<open>compact S\<close> compact_translation)
  3.1132 +    have 2: "convex (op + (- a) ` S)"
  3.1133 +      by (simp add: \<open>convex S\<close> convex_translation)
  3.1134 +    show a_invex: "a \<in> convex hull {x. x extreme_point_of S}"
  3.1135 +      using Krein_Milman_Minkowski_aux [OF refl 1 2]
  3.1136 +            convex_hull_translation [of "-a"]
  3.1137 +      by (auto simp: extreme_points_of_translation translation_assoc)
  3.1138 +    qed
  3.1139 +next
  3.1140 +  show "convex hull {x. x extreme_point_of S} \<subseteq> S"
  3.1141 +  proof -
  3.1142 +    have "{a. a extreme_point_of S} \<subseteq> S"
  3.1143 +      using extreme_point_of_def by blast
  3.1144 +    then show ?thesis
  3.1145 +      by (simp add: \<open>convex S\<close> hull_minimal)
  3.1146 +  qed
  3.1147 +qed
  3.1148 +
  3.1149 +
  3.1150 +subsection\<open>Applying it to convex hulls of explicitly indicated finite sets\<close>
  3.1151 +
  3.1152 +lemma Krein_Milman_polytope:
  3.1153 +  fixes S :: "'a::euclidean_space set"
  3.1154 +  shows
  3.1155 +   "finite S
  3.1156 +       \<Longrightarrow> convex hull S =
  3.1157 +           convex hull {x. x extreme_point_of (convex hull S)}"
  3.1158 +by (simp add: Krein_Milman_Minkowski finite_imp_compact_convex_hull)
  3.1159 +
  3.1160 +lemma extreme_points_of_convex_hull_eq:
  3.1161 +  fixes S :: "'a::euclidean_space set"
  3.1162 +  shows
  3.1163 +   "\<lbrakk>compact S; \<And>T. T \<subset> S \<Longrightarrow> convex hull T \<noteq> convex hull S\<rbrakk>
  3.1164 +        \<Longrightarrow> {x. x extreme_point_of (convex hull S)} = S"
  3.1165 +by (metis (full_types) Krein_Milman_Minkowski compact_convex_hull convex_convex_hull extreme_points_of_convex_hull psubsetI)
  3.1166 +
  3.1167 +
  3.1168 +lemma extreme_point_of_convex_hull_eq:
  3.1169 +  fixes S :: "'a::euclidean_space set"
  3.1170 +  shows
  3.1171 +   "\<lbrakk>compact S; \<And>T. T \<subset> S \<Longrightarrow> convex hull T \<noteq> convex hull S\<rbrakk>
  3.1172 +    \<Longrightarrow> (x extreme_point_of (convex hull S) \<longleftrightarrow> x \<in> S)"
  3.1173 +using extreme_points_of_convex_hull_eq by auto
  3.1174 +
  3.1175 +lemma extreme_point_of_convex_hull_convex_independent:
  3.1176 +  fixes S :: "'a::euclidean_space set"
  3.1177 +  assumes "compact S" and S: "\<And>a. a \<in> S \<Longrightarrow> a \<notin> convex hull (S - {a})"
  3.1178 +  shows "(x extreme_point_of (convex hull S) \<longleftrightarrow> x \<in> S)"
  3.1179 +proof -
  3.1180 +  have "convex hull T \<noteq> convex hull S" if "T \<subset> S" for T
  3.1181 +  proof -
  3.1182 +    obtain a where  "T \<subseteq> S" "a \<in> S" "a \<notin> T" using \<open>T \<subset> S\<close> by blast
  3.1183 +    then show ?thesis
  3.1184 +      by (metis (full_types) Diff_eq_empty_iff Diff_insert0 S hull_mono hull_subset insert_Diff_single subsetCE)
  3.1185 +  qed
  3.1186 +  then show ?thesis
  3.1187 +    by (rule extreme_point_of_convex_hull_eq [OF \<open>compact S\<close>])
  3.1188 +qed
  3.1189 +
  3.1190 +lemma extreme_point_of_convex_hull_affine_independent:
  3.1191 +  fixes S :: "'a::euclidean_space set"
  3.1192 +  shows
  3.1193 +   "~ affine_dependent S
  3.1194 +         \<Longrightarrow> (x extreme_point_of (convex hull S) \<longleftrightarrow> x \<in> S)"
  3.1195 +by (metis aff_independent_finite affine_dependent_def affine_hull_convex_hull extreme_point_of_convex_hull_convex_independent finite_imp_compact hull_inc)
  3.1196 +
  3.1197 +text\<open>Elementary proofs exist, not requiring Euclidean spaces and all this development\<close>
  3.1198 +lemma extreme_point_of_convex_hull_2:
  3.1199 +  fixes x :: "'a::euclidean_space"
  3.1200 +  shows "x extreme_point_of (convex hull {a,b}) \<longleftrightarrow> x = a \<or> x = b"
  3.1201 +proof -
  3.1202 +  have "x extreme_point_of (convex hull {a,b}) \<longleftrightarrow> x \<in> {a,b}"
  3.1203 +    by (intro extreme_point_of_convex_hull_affine_independent affine_independent_2)
  3.1204 +  then show ?thesis
  3.1205 +    by simp
  3.1206 +qed
  3.1207 +
  3.1208 +lemma extreme_point_of_segment:
  3.1209 +  fixes x :: "'a::euclidean_space"
  3.1210 +  shows
  3.1211 +   "x extreme_point_of closed_segment a b \<longleftrightarrow> x = a \<or> x = b"
  3.1212 +by (simp add: extreme_point_of_convex_hull_2 segment_convex_hull)
  3.1213 +
  3.1214 +lemma face_of_convex_hull_subset:
  3.1215 +  fixes S :: "'a::euclidean_space set"
  3.1216 +  assumes "compact S" and T: "T face_of (convex hull S)"
  3.1217 +  obtains s' where "s' \<subseteq> S" "T = convex hull s'"
  3.1218 +apply (rule_tac s' = "{x. x extreme_point_of T}" in that)
  3.1219 +using T extreme_point_of_convex_hull extreme_point_of_face apply blast
  3.1220 +by (metis (no_types) Krein_Milman_Minkowski assms compact_convex_hull convex_convex_hull face_of_imp_compact face_of_imp_convex)
  3.1221 +
  3.1222 +
  3.1223 +proposition face_of_convex_hull_affine_independent:
  3.1224 +  fixes S :: "'a::euclidean_space set"
  3.1225 +  assumes "~ affine_dependent S"
  3.1226 +    shows "(T face_of (convex hull S) \<longleftrightarrow> (\<exists>c. c \<subseteq> S \<and> T = convex hull c))"
  3.1227 +          (is "?lhs = ?rhs")
  3.1228 +proof
  3.1229 +  assume ?lhs
  3.1230 +  then show ?rhs
  3.1231 +    by (meson \<open>T face_of convex hull S\<close> aff_independent_finite assms face_of_convex_hull_subset finite_imp_compact)
  3.1232 +next
  3.1233 +  assume ?rhs
  3.1234 +  then obtain c where "c \<subseteq> S" and T: "T = convex hull c"
  3.1235 +    by blast
  3.1236 +  have "affine hull c \<inter> affine hull (S - c) = {}"
  3.1237 +    apply (rule disjoint_affine_hull [OF assms \<open>c \<subseteq> S\<close>], auto)
  3.1238 +    done
  3.1239 +  then have "affine hull c \<inter> convex hull (S - c) = {}"
  3.1240 +    using convex_hull_subset_affine_hull by fastforce
  3.1241 +  then show ?lhs
  3.1242 +    by (metis face_of_convex_hulls \<open>c \<subseteq> S\<close> aff_independent_finite assms T)
  3.1243 +qed
  3.1244 +
  3.1245 +lemma facet_of_convex_hull_affine_independent:
  3.1246 +  fixes S :: "'a::euclidean_space set"
  3.1247 +  assumes "~ affine_dependent S"
  3.1248 +    shows "T facet_of (convex hull S) \<longleftrightarrow>
  3.1249 +           T \<noteq> {} \<and> (\<exists>u. u \<in> S \<and> T = convex hull (S - {u}))"
  3.1250 +          (is "?lhs = ?rhs")
  3.1251 +proof
  3.1252 +  assume ?lhs
  3.1253 +  then have "T face_of (convex hull S)" "T \<noteq> {}"
  3.1254 +        and afft: "aff_dim T = aff_dim (convex hull S) - 1"
  3.1255 +    by (auto simp: facet_of_def)
  3.1256 +  then obtain c where "c \<subseteq> S" and c: "T = convex hull c"
  3.1257 +    by (auto simp: face_of_convex_hull_affine_independent [OF assms])
  3.1258 +  then have affs: "aff_dim S = aff_dim c + 1"
  3.1259 +    by (metis aff_dim_convex_hull afft eq_diff_eq)
  3.1260 +  have "~ affine_dependent c"
  3.1261 +    using \<open>c \<subseteq> S\<close> affine_dependent_subset assms by blast
  3.1262 +  with affs have "card (S - c) = 1"
  3.1263 +    apply (simp add: aff_dim_affine_independent [symmetric] aff_dim_convex_hull)
  3.1264 +    by (metis aff_dim_affine_independent aff_independent_finite One_nat_def \<open>c \<subseteq> S\<close> add.commute
  3.1265 +                add_diff_cancel_right' assms card_Diff_subset card_mono of_nat_1 of_nat_diff of_nat_eq_iff)
  3.1266 +  then obtain u where u: "u \<in> S - c"
  3.1267 +    by (metis DiffI \<open>c \<subseteq> S\<close> aff_independent_finite assms cancel_comm_monoid_add_class.diff_cancel
  3.1268 +                card_Diff_subset subsetI subset_antisym zero_neq_one)
  3.1269 +  then have u: "S = insert u c"
  3.1270 +    by (metis Diff_subset \<open>c \<subseteq> S\<close> \<open>card (S - c) = 1\<close> card_1_singletonE double_diff insert_Diff insert_subset singletonD)
  3.1271 +  have "T = convex hull (c - {u})"
  3.1272 +    by (metis Diff_empty Diff_insert0 \<open>T facet_of convex hull S\<close> c facet_of_irrefl insert_absorb u)
  3.1273 +  with \<open>T \<noteq> {}\<close> show ?rhs
  3.1274 +    using c u by auto
  3.1275 +next
  3.1276 +  assume ?rhs
  3.1277 +  then obtain u where "T \<noteq> {}" "u \<in> S" and u: "T = convex hull (S - {u})"
  3.1278 +    by (force simp: facet_of_def)
  3.1279 +  then have "\<not> S \<subseteq> {u}"
  3.1280 +    using \<open>T \<noteq> {}\<close> u by auto
  3.1281 +  have [simp]: "aff_dim (convex hull (S - {u})) = aff_dim (convex hull S) - 1"
  3.1282 +    using assms \<open>u \<in> S\<close>
  3.1283 +    apply (simp add: aff_dim_convex_hull affine_dependent_def)
  3.1284 +    apply (drule bspec, assumption)
  3.1285 +    by (metis add_diff_cancel_right' aff_dim_insert insert_Diff [of u S])
  3.1286 +  show ?lhs
  3.1287 +    apply (subst u)
  3.1288 +    apply (simp add: \<open>\<not> S \<subseteq> {u}\<close> facet_of_def face_of_convex_hull_affine_independent [OF assms], blast)
  3.1289 +    done
  3.1290 +qed
  3.1291 +
  3.1292 +lemma facet_of_convex_hull_affine_independent_alt:
  3.1293 +  fixes S :: "'a::euclidean_space set"
  3.1294 +  shows
  3.1295 +   "~affine_dependent S
  3.1296 +        \<Longrightarrow> (T facet_of (convex hull S) \<longleftrightarrow>
  3.1297 +             2 \<le> card S \<and> (\<exists>u. u \<in> S \<and> T = convex hull (S - {u})))"
  3.1298 +apply (simp add: facet_of_convex_hull_affine_independent)
  3.1299 +apply (auto simp: Set.subset_singleton_iff)
  3.1300 +apply (metis Diff_cancel Int_empty_right Int_insert_right_if1  aff_independent_finite card_eq_0_iff card_insert_if card_mono card_subset_eq convex_hull_eq_empty eq_iff equals0D finite_insert finite_subset inf.absorb_iff2 insert_absorb insert_not_empty  not_less_eq_eq numeral_2_eq_2)
  3.1301 +done
  3.1302 +
  3.1303 +lemma segment_face_of:
  3.1304 +  assumes "(closed_segment a b) face_of S"
  3.1305 +  shows "a extreme_point_of S" "b extreme_point_of S"
  3.1306 +proof -
  3.1307 +  have as: "{a} face_of S"
  3.1308 +    by (metis (no_types) assms convex_hull_singleton empty_iff extreme_point_of_convex_hull_insert face_of_face face_of_singleton finite.emptyI finite.insertI insert_absorb insert_iff segment_convex_hull)
  3.1309 +  moreover have "{b} face_of S"
  3.1310 +  proof -
  3.1311 +    have "b \<in> convex hull {a} \<or> b extreme_point_of convex hull {b, a}"
  3.1312 +      by (meson extreme_point_of_convex_hull_insert finite.emptyI finite.insertI)
  3.1313 +    moreover have "closed_segment a b = convex hull {b, a}"
  3.1314 +      using closed_segment_commute segment_convex_hull by blast
  3.1315 +    ultimately show ?thesis
  3.1316 +      by (metis as assms face_of_face convex_hull_singleton empty_iff face_of_singleton insertE)
  3.1317 +    qed
  3.1318 +  ultimately show "a extreme_point_of S" "b extreme_point_of S"
  3.1319 +    using face_of_singleton by blast+
  3.1320 +qed
  3.1321 +
  3.1322 +
  3.1323 +lemma Krein_Milman_frontier:
  3.1324 +  fixes S :: "'a::euclidean_space set"
  3.1325 +  assumes "convex S" "compact S"
  3.1326 +    shows "S = convex hull (frontier S)"
  3.1327 +          (is "?lhs = ?rhs")
  3.1328 +proof
  3.1329 +  have "?lhs \<subseteq> convex hull {x. x extreme_point_of S}"
  3.1330 +    using Krein_Milman_Minkowski assms by blast
  3.1331 +  also have "... \<subseteq> ?rhs"
  3.1332 +    apply (rule hull_mono)
  3.1333 +    apply (auto simp: frontier_def extreme_point_not_in_interior)
  3.1334 +    using closure_subset apply (force simp: extreme_point_of_def)
  3.1335 +    done
  3.1336 +  finally show "?lhs \<subseteq> ?rhs" .
  3.1337 +next
  3.1338 +  have "?rhs \<subseteq> convex hull S"
  3.1339 +    by (metis Diff_subset \<open>compact S\<close> closure_closed compact_eq_bounded_closed frontier_def hull_mono)
  3.1340 +  also have "... \<subseteq> ?lhs"
  3.1341 +    by (simp add: \<open>convex S\<close> hull_same)
  3.1342 +  finally show "?rhs \<subseteq> ?lhs" .
  3.1343 +qed
  3.1344 +
  3.1345 +subsection\<open>Polytopes\<close>
  3.1346 +
  3.1347 +definition polytope where
  3.1348 + "polytope S \<equiv> \<exists>v. finite v \<and> S = convex hull v"
  3.1349 +
  3.1350 +lemma polytope_translation_eq: "polytope (image (\<lambda>x. a + x) S) \<longleftrightarrow> polytope S"
  3.1351 +apply (simp add: polytope_def, safe)
  3.1352 +apply (metis convex_hull_translation finite_imageI translation_galois)
  3.1353 +by (metis convex_hull_translation finite_imageI)
  3.1354 +
  3.1355 +lemma polytope_linear_image: "\<lbrakk>linear f; polytope p\<rbrakk> \<Longrightarrow> polytope(image f p)"
  3.1356 +  unfolding polytope_def using convex_hull_linear_image by blast
  3.1357 +
  3.1358 +lemma polytope_empty: "polytope {}"
  3.1359 +  using convex_hull_empty polytope_def by blast
  3.1360 +
  3.1361 +lemma polytope_convex_hull: "finite S \<Longrightarrow> polytope(convex hull S)"
  3.1362 +  using polytope_def by auto
  3.1363 +
  3.1364 +lemma polytope_Times: "\<lbrakk>polytope S; polytope T\<rbrakk> \<Longrightarrow> polytope(S \<times> T)"
  3.1365 +  unfolding polytope_def
  3.1366 +  by (metis finite_cartesian_product convex_hull_Times)
  3.1367 +
  3.1368 +lemma face_of_polytope_polytope:
  3.1369 +  fixes S :: "'a::euclidean_space set"
  3.1370 +  shows "\<lbrakk>polytope S; F face_of S\<rbrakk> \<Longrightarrow> polytope F"
  3.1371 +unfolding polytope_def
  3.1372 +by (meson face_of_convex_hull_subset finite_imp_compact finite_subset)
  3.1373 +
  3.1374 +lemma finite_polytope_faces:
  3.1375 +  fixes S :: "'a::euclidean_space set"
  3.1376 +  assumes "polytope S"
  3.1377 +  shows "finite {F. F face_of S}"
  3.1378 +proof -
  3.1379 +  obtain v where "finite v" "S = convex hull v"
  3.1380 +    using assms polytope_def by auto
  3.1381 +  have "finite (op hull convex ` {T. T \<subseteq> v})"
  3.1382 +    by (simp add: \<open>finite v\<close>)
  3.1383 +  moreover have "{F. F face_of S} \<subseteq> (op hull convex ` {T. T \<subseteq> v})"
  3.1384 +    by (metis (no_types, lifting) \<open>finite v\<close> \<open>S = convex hull v\<close> face_of_convex_hull_subset finite_imp_compact image_eqI mem_Collect_eq subsetI)
  3.1385 +  ultimately show ?thesis
  3.1386 +    by (blast intro: finite_subset)
  3.1387 +qed
  3.1388 +
  3.1389 +lemma finite_polytope_facets:
  3.1390 +  assumes "polytope S"
  3.1391 +  shows "finite {T. T facet_of S}"
  3.1392 +by (simp add: assms facet_of_def finite_polytope_faces)
  3.1393 +
  3.1394 +lemma polytope_scaling:
  3.1395 +  assumes "polytope S"  shows "polytope (image (\<lambda>x. c *\<^sub>R x) S)"
  3.1396 +by (simp add: assms polytope_linear_image)
  3.1397 +
  3.1398 +lemma polytope_imp_compact:
  3.1399 +  fixes S :: "'a::real_normed_vector set"
  3.1400 +  shows "polytope S \<Longrightarrow> compact S"
  3.1401 +by (metis finite_imp_compact_convex_hull polytope_def)
  3.1402 +
  3.1403 +lemma polytope_imp_convex: "polytope S \<Longrightarrow> convex S"
  3.1404 +  by (metis convex_convex_hull polytope_def)
  3.1405 +
  3.1406 +lemma polytope_imp_closed:
  3.1407 +  fixes S :: "'a::real_normed_vector set"
  3.1408 +  shows "polytope S \<Longrightarrow> closed S"
  3.1409 +by (simp add: compact_imp_closed polytope_imp_compact)
  3.1410 +
  3.1411 +lemma polytope_imp_bounded:
  3.1412 +  fixes S :: "'a::real_normed_vector set"
  3.1413 +  shows "polytope S \<Longrightarrow> bounded S"
  3.1414 +by (simp add: compact_imp_bounded polytope_imp_compact)
  3.1415 +
  3.1416 +lemma polytope_interval: "polytope(cbox a b)"
  3.1417 +  unfolding polytope_def by (meson closed_interval_as_convex_hull)
  3.1418 +
  3.1419 +lemma polytope_sing: "polytope {a}"
  3.1420 +  using polytope_def by force
  3.1421 +
  3.1422 +
  3.1423 +subsection\<open>Polyhedra\<close>
  3.1424 +
  3.1425 +definition polyhedron where
  3.1426 + "polyhedron S \<equiv>
  3.1427 +        \<exists>F. finite F \<and>
  3.1428 +            S = \<Inter> F \<and>
  3.1429 +            (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b})"
  3.1430 +
  3.1431 +lemma polyhedron_Int [intro,simp]:
  3.1432 +   "\<lbrakk>polyhedron S; polyhedron T\<rbrakk> \<Longrightarrow> polyhedron (S \<inter> T)"
  3.1433 +  apply (simp add: polyhedron_def, clarify)
  3.1434 +  apply (rename_tac F G)
  3.1435 +  apply (rule_tac x="F \<union> G" in exI, auto)
  3.1436 +  done
  3.1437 +
  3.1438 +lemma polyhedron_UNIV [iff]: "polyhedron UNIV"
  3.1439 +  unfolding polyhedron_def
  3.1440 +  by (rule_tac x="{}" in exI) auto
  3.1441 +
  3.1442 +lemma polyhedron_Inter [intro,simp]:
  3.1443 +   "\<lbrakk>finite F; \<And>S. S \<in> F \<Longrightarrow> polyhedron S\<rbrakk> \<Longrightarrow> polyhedron(\<Inter>F)"
  3.1444 +by (induction F rule: finite_induct) auto
  3.1445 +
  3.1446 +
  3.1447 +lemma polyhedron_empty [iff]: "polyhedron ({} :: 'a :: euclidean_space set)"
  3.1448 +proof -
  3.1449 +  have "\<exists>a. a \<noteq> 0 \<and>
  3.1450 +             (\<exists>b. {x. (SOME i. i \<in> Basis) \<bullet> x \<le> - 1} = {x. a \<bullet> x \<le> b})"
  3.1451 +    by (rule_tac x="(SOME i. i \<in> Basis)" in exI) (force simp: SOME_Basis nonzero_Basis)
  3.1452 +  moreover have "\<exists>a b. a \<noteq> 0 \<and>
  3.1453 +                       {x. - (SOME i. i \<in> Basis) \<bullet> x \<le> - 1} = {x. a \<bullet> x \<le> b}"
  3.1454 +      apply (rule_tac x="-(SOME i. i \<in> Basis)" in exI)
  3.1455 +      apply (rule_tac x="-1" in exI)
  3.1456 +      apply (simp add: SOME_Basis nonzero_Basis)
  3.1457 +      done
  3.1458 +  ultimately show ?thesis
  3.1459 +    unfolding polyhedron_def
  3.1460 +    apply (rule_tac x="{{x. (SOME i. i \<in> Basis) \<bullet> x \<le> -1},
  3.1461 +                        {x. -(SOME i. i \<in> Basis) \<bullet> x \<le> -1}}" in exI)
  3.1462 +    apply force
  3.1463 +    done
  3.1464 +qed
  3.1465 +
  3.1466 +lemma polyhedron_halfspace_le:
  3.1467 +  fixes a :: "'a :: euclidean_space"
  3.1468 +  shows "polyhedron {x. a \<bullet> x \<le> b}"
  3.1469 +proof (cases "a = 0")
  3.1470 +  case True then show ?thesis by auto
  3.1471 +next
  3.1472 +  case False
  3.1473 +  then show ?thesis
  3.1474 +    unfolding polyhedron_def
  3.1475 +    by (rule_tac x="{{x. a \<bullet> x \<le> b}}" in exI) auto
  3.1476 +qed
  3.1477 +
  3.1478 +lemma polyhedron_halfspace_ge:
  3.1479 +  fixes a :: "'a :: euclidean_space"
  3.1480 +  shows "polyhedron {x. a \<bullet> x \<ge> b}"
  3.1481 +using polyhedron_halfspace_le [of "-a" "-b"] by simp
  3.1482 +
  3.1483 +lemma polyhedron_hyperplane:
  3.1484 +  fixes a :: "'a :: euclidean_space"
  3.1485 +  shows "polyhedron {x. a \<bullet> x = b}"
  3.1486 +proof -
  3.1487 +  have "{x. a \<bullet> x = b} = {x. a \<bullet> x \<le> b} \<inter> {x. a \<bullet> x \<ge> b}"
  3.1488 +    by force
  3.1489 +  then show ?thesis
  3.1490 +    by (simp add: polyhedron_halfspace_ge polyhedron_halfspace_le)
  3.1491 +qed
  3.1492 +
  3.1493 +lemma affine_imp_polyhedron:
  3.1494 +  fixes S :: "'a :: euclidean_space set"
  3.1495 +  shows "affine S \<Longrightarrow> polyhedron S"
  3.1496 +by (metis affine_hull_eq polyhedron_Inter polyhedron_hyperplane affine_hull_finite_intersection_hyperplanes [of S])
  3.1497 +
  3.1498 +lemma polyhedron_imp_closed:
  3.1499 +  fixes S :: "'a :: euclidean_space set"
  3.1500 +  shows "polyhedron S \<Longrightarrow> closed S"
  3.1501 +apply (simp add: polyhedron_def)
  3.1502 +using closed_halfspace_le by fastforce
  3.1503 +
  3.1504 +lemma polyhedron_imp_convex:
  3.1505 +  fixes S :: "'a :: euclidean_space set"
  3.1506 +  shows "polyhedron S \<Longrightarrow> convex S"
  3.1507 +apply (simp add: polyhedron_def)
  3.1508 +using convex_Inter convex_halfspace_le by fastforce
  3.1509 +
  3.1510 +lemma polyhedron_affine_hull:
  3.1511 +  fixes S :: "'a :: euclidean_space set"
  3.1512 +  shows "polyhedron(affine hull S)"
  3.1513 +by (simp add: affine_imp_polyhedron)
  3.1514 +
  3.1515 +
  3.1516 +subsection\<open>Canonical polyhedron representation making facial structure explicit\<close>
  3.1517 +
  3.1518 +lemma polyhedron_Int_affine:
  3.1519 +  fixes S :: "'a :: euclidean_space set"
  3.1520 +  shows "polyhedron S \<longleftrightarrow>
  3.1521 +           (\<exists>F. finite F \<and> S = (affine hull S) \<inter> \<Inter>F \<and>
  3.1522 +                (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}))"
  3.1523 +        (is "?lhs = ?rhs")
  3.1524 +proof
  3.1525 +  assume ?lhs then show ?rhs
  3.1526 +    apply (simp add: polyhedron_def)
  3.1527 +    apply (erule ex_forward)
  3.1528 +    using hull_subset apply force
  3.1529 +    done
  3.1530 +next
  3.1531 +  assume ?rhs then show ?lhs
  3.1532 +    apply clarify
  3.1533 +    apply (erule ssubst)
  3.1534 +    apply (force intro: polyhedron_affine_hull polyhedron_halfspace_le)
  3.1535 +    done
  3.1536 +qed
  3.1537 +
  3.1538 +proposition rel_interior_polyhedron_explicit:
  3.1539 +  assumes "finite F"
  3.1540 +      and seq: "S = affine hull S \<inter> \<Inter>F"
  3.1541 +      and faceq: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
  3.1542 +      and psub: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> affine hull S \<inter> \<Inter>F'"
  3.1543 +    shows "rel_interior S = {x \<in> S. \<forall>h \<in> F. a h \<bullet> x < b h}"
  3.1544 +proof -
  3.1545 +  have rels: "\<And>x. x \<in> rel_interior S \<Longrightarrow> x \<in> S"
  3.1546 +    by (meson IntE mem_rel_interior)
  3.1547 +  moreover have "a i \<bullet> x < b i" if x: "x \<in> rel_interior S" and "i \<in> F" for x i
  3.1548 +  proof -
  3.1549 +    have fif: "F - {i} \<subset> F"
  3.1550 +      using \<open>i \<in> F\<close> Diff_insert_absorb Diff_subset set_insert psubsetI by blast
  3.1551 +    then have "S \<subset> affine hull S \<inter> \<Inter>(F - {i})"
  3.1552 +      by (rule psub)
  3.1553 +    then obtain z where ssub: "S \<subseteq> \<Inter>(F - {i})" and zint: "z \<in> \<Inter>(F - {i})"
  3.1554 +                    and "z \<notin> S" and zaff: "z \<in> affine hull S"
  3.1555 +      by auto
  3.1556 +    have "z \<noteq> x"
  3.1557 +      using \<open>z \<notin> S\<close> rels x by blast
  3.1558 +    have "z \<notin> affine hull S \<inter> \<Inter>F"
  3.1559 +      using \<open>z \<notin> S\<close> seq by auto
  3.1560 +    then have aiz: "a i \<bullet> z > b i"
  3.1561 +      using faceq zint zaff by fastforce
  3.1562 +    obtain e where "e > 0" "x \<in> S" and e: "ball x e \<inter> affine hull S \<subseteq> S"
  3.1563 +      using x by (auto simp: mem_rel_interior_ball)
  3.1564 +    then have ins: "\<And>y. \<lbrakk>norm (x - y) < e; y \<in> affine hull S\<rbrakk> \<Longrightarrow> y \<in> S"
  3.1565 +      by (metis IntI subsetD dist_norm mem_ball)
  3.1566 +    def \<xi> \<equiv> "min (1/2) (e / 2 / norm(z - x))"
  3.1567 +    have "norm (\<xi> *\<^sub>R x - \<xi> *\<^sub>R z) = norm (\<xi> *\<^sub>R (x - z))"
  3.1568 +      by (simp add: \<xi>_def algebra_simps norm_mult)
  3.1569 +    also have "... = \<xi> * norm (x - z)"
  3.1570 +      using \<open>e > 0\<close> by (simp add: \<xi>_def)
  3.1571 +    also have "... < e"
  3.1572 +      using \<open>z \<noteq> x\<close> \<open>e > 0\<close> by (simp add: \<xi>_def min_def divide_simps norm_minus_commute)
  3.1573 +    finally have lte: "norm (\<xi> *\<^sub>R x - \<xi> *\<^sub>R z) < e" .
  3.1574 +    have \<xi>_aff: "\<xi> *\<^sub>R z + (1 - \<xi>) *\<^sub>R x \<in> affine hull S"
  3.1575 +      by (metis \<open>x \<in> S\<close> add.commute affine_affine_hull diff_add_cancel hull_inc mem_affine zaff)
  3.1576 +    have "\<xi> *\<^sub>R z + (1 - \<xi>) *\<^sub>R x \<in> S"
  3.1577 +      apply (rule ins [OF _ \<xi>_aff])
  3.1578 +      apply (simp add: algebra_simps lte)
  3.1579 +      done
  3.1580 +    then obtain l where l: "0 < l" "l < 1" and ls: "(l *\<^sub>R z + (1 - l) *\<^sub>R x) \<in> S"
  3.1581 +      apply (rule_tac l = \<xi> in that)
  3.1582 +      using \<open>e > 0\<close> \<open>z \<noteq> x\<close>  apply (auto simp: \<xi>_def)
  3.1583 +      done
  3.1584 +    then have i: "l *\<^sub>R z + (1 - l) *\<^sub>R x \<in> i"
  3.1585 +      using seq \<open>i \<in> F\<close> by auto
  3.1586 +    have "b i * l + (a i \<bullet> x) * (1 - l) < a i \<bullet> (l *\<^sub>R z + (1 - l) *\<^sub>R x)"
  3.1587 +      using l by (simp add: algebra_simps aiz)
  3.1588 +    also have "\<dots> \<le> b i" using i l
  3.1589 +      using faceq mem_Collect_eq \<open>i \<in> F\<close> by blast
  3.1590 +    finally have "(a i \<bullet> x) * (1 - l) < b i * (1 - l)"
  3.1591 +      by (simp add: algebra_simps)
  3.1592 +    with l show ?thesis
  3.1593 +      by simp
  3.1594 +  qed
  3.1595 +  moreover have "x \<in> rel_interior S"
  3.1596 +           if "x \<in> S" and less: "\<And>h. h \<in> F \<Longrightarrow> a h \<bullet> x < b h" for x
  3.1597 +  proof -
  3.1598 +    have 1: "\<And>h. h \<in> F \<Longrightarrow> x \<in> interior h"
  3.1599 +      by (metis interior_halfspace_le mem_Collect_eq less faceq)
  3.1600 +    have 2: "\<And>y. \<lbrakk>\<forall>h\<in>F. y \<in> interior h; y \<in> affine hull S\<rbrakk> \<Longrightarrow> y \<in> S"
  3.1601 +      by (metis IntI Inter_iff contra_subsetD interior_subset seq)
  3.1602 +    show ?thesis
  3.1603 +      apply (simp add: rel_interior \<open>x \<in> S\<close>)
  3.1604 +      apply (rule_tac x="\<Inter>h\<in>F. interior h" in exI)
  3.1605 +      apply (auto simp: \<open>finite F\<close> open_INT 1 2)
  3.1606 +      done
  3.1607 +  qed
  3.1608 +  ultimately show ?thesis by blast
  3.1609 +qed
  3.1610 +
  3.1611 +
  3.1612 +lemma polyhedron_Int_affine_parallel:
  3.1613 +  fixes S :: "'a :: euclidean_space set"
  3.1614 +  shows "polyhedron S \<longleftrightarrow>
  3.1615 +         (\<exists>F. finite F \<and>
  3.1616 +              S = (affine hull S) \<inter> (\<Inter>F) \<and>
  3.1617 +              (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b} \<and>
  3.1618 +                             (\<forall>x \<in> affine hull S. (x + a) \<in> affine hull S)))"
  3.1619 +    (is "?lhs = ?rhs")
  3.1620 +proof
  3.1621 +  assume ?lhs
  3.1622 +  then obtain F where "finite F" and seq: "S = (affine hull S) \<inter> \<Inter>F"
  3.1623 +                  and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
  3.1624 +    by (fastforce simp add: polyhedron_Int_affine)
  3.1625 +  then obtain a b where ab: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
  3.1626 +    by metis
  3.1627 +  show ?rhs
  3.1628 +  proof -
  3.1629 +    have "\<exists>a' b'. a' \<noteq> 0 \<and>
  3.1630 +                  affine hull S \<inter> {x. a' \<bullet> x \<le> b'} = affine hull S \<inter> h \<and>
  3.1631 +                  (\<forall>w \<in> affine hull S. (w + a') \<in> affine hull S)"
  3.1632 +        if "h \<in> F" "~(affine hull S \<subseteq> h)" for h
  3.1633 +    proof -
  3.1634 +      have "a h \<noteq> 0" and "h = {x. a h \<bullet> x \<le> b h}" "h \<inter> \<Inter>F = \<Inter>F"
  3.1635 +        using \<open>h \<in> F\<close> ab by auto
  3.1636 +      then have "(affine hull S) \<inter> {x. a h \<bullet> x \<le> b h} \<noteq> {}"
  3.1637 +        by (metis (no_types) affine_hull_eq_empty inf.absorb_iff2 inf_assoc inf_bot_right inf_commute seq that(2))
  3.1638 +      moreover have "~ (affine hull S \<subseteq> {x. a h \<bullet> x \<le> b h})"
  3.1639 +        using \<open>h = {x. a h \<bullet> x \<le> b h}\<close> that(2) by blast
  3.1640 +      ultimately show ?thesis
  3.1641 +        using affine_parallel_slice [of "affine hull S"]
  3.1642 +        by (metis \<open>h = {x. a h \<bullet> x \<le> b h}\<close> affine_affine_hull)
  3.1643 +    qed
  3.1644 +    then obtain a b
  3.1645 +         where ab: "\<And>h. \<lbrakk>h \<in> F; ~ (affine hull S \<subseteq> h)\<rbrakk>
  3.1646 +             \<Longrightarrow> a h \<noteq> 0 \<and>
  3.1647 +                  affine hull S \<inter> {x. a h \<bullet> x \<le> b h} = affine hull S \<inter> h \<and>
  3.1648 +                  (\<forall>w \<in> affine hull S. (w + a h) \<in> affine hull S)"
  3.1649 +      by metis
  3.1650 +    have seq2: "S = affine hull S \<inter> (\<Inter>h\<in>{h \<in> F. \<not> affine hull S \<subseteq> h}. {x. a h \<bullet> x \<le> b h})"
  3.1651 +      by (subst seq) (auto simp: ab INT_extend_simps)
  3.1652 +    show ?thesis
  3.1653 +      apply (rule_tac x="(\<lambda>h. {x. a h \<bullet> x \<le> b h}) ` {h. h \<in> F \<and> ~(affine hull S \<subseteq> h)}" in exI)
  3.1654 +      apply (intro conjI seq2)
  3.1655 +        using \<open>finite F\<close> apply force
  3.1656 +       using ab apply blast
  3.1657 +       done
  3.1658 +  qed
  3.1659 +next
  3.1660 +  assume ?rhs then show ?lhs
  3.1661 +    apply (simp add: polyhedron_Int_affine)
  3.1662 +    by metis
  3.1663 +qed
  3.1664 +
  3.1665 +
  3.1666 +proposition polyhedron_Int_affine_parallel_minimal:
  3.1667 +  fixes S :: "'a :: euclidean_space set"
  3.1668 +  shows "polyhedron S \<longleftrightarrow>
  3.1669 +         (\<exists>F. finite F \<and>
  3.1670 +              S = (affine hull S) \<inter> (\<Inter>F) \<and>
  3.1671 +              (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b} \<and>
  3.1672 +                             (\<forall>x \<in> affine hull S. (x + a) \<in> affine hull S)) \<and>
  3.1673 +              (\<forall>F'. F' \<subset> F \<longrightarrow> S \<subset> (affine hull S) \<inter> (\<Inter>F')))"
  3.1674 +    (is "?lhs = ?rhs")
  3.1675 +proof
  3.1676 +  assume ?lhs
  3.1677 +  then obtain f0
  3.1678 +           where f0: "finite f0"
  3.1679 +                 "S = (affine hull S) \<inter> (\<Inter>f0)"
  3.1680 +                   (is "?P f0")
  3.1681 +                 "\<forall>h \<in> f0. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b} \<and>
  3.1682 +                             (\<forall>x \<in> affine hull S. (x + a) \<in> affine hull S)"
  3.1683 +                   (is "?Q f0")
  3.1684 +    by (force simp: polyhedron_Int_affine_parallel)
  3.1685 +  def n \<equiv> "LEAST n. \<exists>F. card F = n \<and> finite F \<and> ?P F \<and> ?Q F"
  3.1686 +  have nf: "\<exists>F. card F = n \<and> finite F \<and> ?P F \<and> ?Q F"
  3.1687 +    apply (simp add: n_def)
  3.1688 +    apply (rule LeastI [where k = "card f0"])
  3.1689 +    using f0 apply auto
  3.1690 +    done
  3.1691 +  then obtain F where F: "card F = n" "finite F" and seq: "?P F" and aff: "?Q F"
  3.1692 +    by blast
  3.1693 +  then have "~ (finite g \<and> ?P g \<and> ?Q g)" if "card g < n" for g
  3.1694 +    using that by (auto simp: n_def dest!: not_less_Least)
  3.1695 +  then have *: "~ (?P g \<and> ?Q g)" if "g \<subset> F" for g
  3.1696 +    using that \<open>finite F\<close> psubset_card_mono \<open>card F = n\<close>
  3.1697 +    by (metis finite_Int inf.strict_order_iff)
  3.1698 +  have 1: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subseteq> affine hull S \<inter> \<Inter>F'"
  3.1699 +    by (subst seq) blast
  3.1700 +  have 2: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<noteq> affine hull S \<inter> \<Inter>F'"
  3.1701 +    apply (frule *)
  3.1702 +    by (metis aff subsetCE subset_iff_psubset_eq)
  3.1703 +  show ?rhs
  3.1704 +    by (metis \<open>finite F\<close> seq aff psubsetI 1 2)
  3.1705 +next
  3.1706 +  assume ?rhs then show ?lhs
  3.1707 +    by (auto simp: polyhedron_Int_affine_parallel)
  3.1708 +qed
  3.1709 +
  3.1710 +
  3.1711 +lemma polyhedron_Int_affine_minimal:
  3.1712 +  fixes S :: "'a :: euclidean_space set"
  3.1713 +  shows "polyhedron S \<longleftrightarrow>
  3.1714 +         (\<exists>F. finite F \<and> S = (affine hull S) \<inter> \<Inter>F \<and>
  3.1715 +              (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}) \<and>
  3.1716 +              (\<forall>F'. F' \<subset> F \<longrightarrow> S \<subset> (affine hull S) \<inter> \<Inter>F'))"
  3.1717 +apply (rule iffI)
  3.1718 + apply (force simp: polyhedron_Int_affine_parallel_minimal elim!: ex_forward)
  3.1719 +apply (auto simp: polyhedron_Int_affine elim!: ex_forward)
  3.1720 +done
  3.1721 +
  3.1722 +proposition facet_of_polyhedron_explicit:
  3.1723 +  assumes "finite F"
  3.1724 +      and seq: "S = affine hull S \<inter> \<Inter>F"
  3.1725 +      and faceq: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
  3.1726 +      and psub: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> affine hull S \<inter> \<Inter>F'"
  3.1727 +    shows "c facet_of S \<longleftrightarrow> (\<exists>h. h \<in> F \<and> c = S \<inter> {x. a h \<bullet> x = b h})"
  3.1728 +proof (cases "S = {}")
  3.1729 +  case True with psub show ?thesis by force
  3.1730 +next
  3.1731 +  case False
  3.1732 +  have "polyhedron S"
  3.1733 +    apply (simp add: polyhedron_Int_affine)
  3.1734 +    apply (rule_tac x=F in exI)
  3.1735 +    using assms  apply force
  3.1736 +    done
  3.1737 +  then have "convex S"
  3.1738 +    by (rule polyhedron_imp_convex)
  3.1739 +  with False rel_interior_eq_empty have "rel_interior S \<noteq> {}" by blast
  3.1740 +  then obtain x where "x \<in> rel_interior S" by auto
  3.1741 +  then obtain T where "open T" "x \<in> T" "x \<in> S" "T \<inter> affine hull S \<subseteq> S"
  3.1742 +    by (force simp: mem_rel_interior)
  3.1743 +  then have xaff: "x \<in> affine hull S" and xint: "x \<in> \<Inter>F"
  3.1744 +    using seq hull_inc by auto
  3.1745 +  have "rel_interior S = {x \<in> S. \<forall>h\<in>F. a h \<bullet> x < b h}"
  3.1746 +    by (rule rel_interior_polyhedron_explicit [OF \<open>finite F\<close> seq faceq psub])
  3.1747 +  with \<open>x \<in> rel_interior S\<close>
  3.1748 +  have [simp]: "\<And>h. h\<in>F \<Longrightarrow> a h \<bullet> x < b h" by blast
  3.1749 +  have *: "(S \<inter> {x. a h \<bullet> x = b h}) facet_of S" if "h \<in> F" for h
  3.1750 +  proof -
  3.1751 +    have "S \<subset> affine hull S \<inter> \<Inter>(F - {h})"
  3.1752 +      using psub that by (metis Diff_disjoint Diff_subset insert_disjoint(2) psubsetI)
  3.1753 +    then obtain z where zaff: "z \<in> affine hull S" and zint: "z \<in> \<Inter>(F - {h})" and "z \<notin> S"
  3.1754 +      by force
  3.1755 +    then have "z \<noteq> x" "z \<notin> h" using seq \<open>x \<in> S\<close> by auto
  3.1756 +    have "x \<in> h" using that xint by auto
  3.1757 +    then have able: "a h \<bullet> x \<le> b h"
  3.1758 +      using faceq that by blast
  3.1759 +    also have "... < a h \<bullet> z" using \<open>z \<notin> h\<close> faceq [OF that] xint by auto
  3.1760 +    finally have xltz: "a h \<bullet> x < a h \<bullet> z" .
  3.1761 +    def l \<equiv> "(b h - a h \<bullet> x) / (a h \<bullet> z - a h \<bullet> x)"
  3.1762 +    def w \<equiv> "(1 - l) *\<^sub>R x + l *\<^sub>R z"
  3.1763 +    have "0 < l" "l < 1"
  3.1764 +      using able xltz \<open>b h < a h \<bullet> z\<close> \<open>h \<in> F\<close>
  3.1765 +      by (auto simp: l_def divide_simps)
  3.1766 +    have awlt: "a i \<bullet> w < b i" if "i \<in> F" "i \<noteq> h" for i
  3.1767 +    proof -
  3.1768 +      have "(1 - l) * (a i \<bullet> x) < (1 - l) * b i"
  3.1769 +        by (simp add: \<open>l < 1\<close> \<open>i \<in> F\<close>)
  3.1770 +      moreover have "l * (a i \<bullet> z) \<le> l * b i"
  3.1771 +        apply (rule mult_left_mono)
  3.1772 +        apply (metis Diff_insert_absorb Inter_iff Set.set_insert \<open>h \<in> F\<close> faceq insertE mem_Collect_eq that zint)
  3.1773 +        using \<open>0 < l\<close>
  3.1774 +        apply simp
  3.1775 +        done
  3.1776 +      ultimately show ?thesis by (simp add: w_def algebra_simps)
  3.1777 +    qed
  3.1778 +    have weq: "a h \<bullet> w = b h"
  3.1779 +      using xltz unfolding w_def l_def
  3.1780 +      by (simp add: algebra_simps) (simp add: field_simps)
  3.1781 +    have "w \<in> affine hull S"
  3.1782 +      by (simp add: w_def mem_affine xaff zaff)
  3.1783 +    moreover have "w \<in> \<Inter>F"
  3.1784 +      using \<open>a h \<bullet> w = b h\<close> awlt faceq less_eq_real_def by blast
  3.1785 +    ultimately have "w \<in> S"
  3.1786 +      using seq by blast
  3.1787 +    with weq have "S \<inter> {x. a h \<bullet> x = b h} \<noteq> {}" by blast
  3.1788 +    moreover have "S \<inter> {x. a h \<bullet> x = b h} face_of S"
  3.1789 +      apply (rule face_of_Int_supporting_hyperplane_le)
  3.1790 +      apply (rule \<open>convex S\<close>)
  3.1791 +      apply (subst (asm) seq)
  3.1792 +      using faceq that apply fastforce
  3.1793 +      done
  3.1794 +    moreover have "affine hull (S \<inter> {x. a h \<bullet> x = b h}) =
  3.1795 +                   (affine hull S) \<inter> {x. a h \<bullet> x = b h}"
  3.1796 +    proof
  3.1797 +      show "affine hull (S \<inter> {x. a h \<bullet> x = b h}) \<subseteq> affine hull S \<inter> {x. a h \<bullet> x = b h}"
  3.1798 +        apply (intro Int_greatest hull_mono Int_lower1)
  3.1799 +        apply (metis affine_hull_eq affine_hyperplane hull_mono inf_le2)
  3.1800 +        done
  3.1801 +    next
  3.1802 +      show "affine hull S \<inter> {x. a h \<bullet> x = b h} \<subseteq> affine hull (S \<inter> {x. a h \<bullet> x = b h})"
  3.1803 +      proof
  3.1804 +        fix y
  3.1805 +        assume yaff: "y \<in> affine hull S \<inter> {y. a h \<bullet> y = b h}"
  3.1806 +        obtain T where "0 < T"
  3.1807 +                 and T: "\<And>j. \<lbrakk>j \<in> F; j \<noteq> h\<rbrakk> \<Longrightarrow> T * (a j \<bullet> y - a j \<bullet> w) \<le> b j - a j \<bullet> w"
  3.1808 +        proof (cases "F - {h} = {}")
  3.1809 +          case True then show ?thesis
  3.1810 +            by (rule_tac T=1 in that) auto
  3.1811 +        next
  3.1812 +          case False
  3.1813 +          then obtain h' where h': "h' \<in> F - {h}" by auto
  3.1814 +          def inff \<equiv> "INF j:F - {h}. if 0 < a j \<bullet> y - a j \<bullet> w
  3.1815 +                                      then (b j - a j \<bullet> w) / (a j \<bullet> y - a j \<bullet> w)
  3.1816 +                                      else 1"
  3.1817 +          have "0 < inff"
  3.1818 +            apply (simp add: inff_def)
  3.1819 +            apply (rule finite_imp_less_Inf)
  3.1820 +              using \<open>finite F\<close> apply blast
  3.1821 +             using h' apply blast
  3.1822 +            apply simp
  3.1823 +            using awlt apply (force simp: divide_simps)
  3.1824 +            done
  3.1825 +          moreover have "inff * (a j \<bullet> y - a j \<bullet> w) \<le> b j - a j \<bullet> w"
  3.1826 +                        if "j \<in> F" "j \<noteq> h" for j
  3.1827 +          proof (cases "a j \<bullet> w < a j \<bullet> y")
  3.1828 +            case True
  3.1829 +            then have "inff \<le> (b j - a j \<bullet> w) / (a j \<bullet> y - a j \<bullet> w)"
  3.1830 +              apply (simp add: inff_def)
  3.1831 +              apply (rule cInf_le_finite)
  3.1832 +              using \<open>finite F\<close> apply blast
  3.1833 +              apply (simp add: that split: if_split_asm)
  3.1834 +              done
  3.1835 +            then show ?thesis
  3.1836 +              using \<open>0 < inff\<close> awlt [OF that] mult_strict_left_mono
  3.1837 +              by (fastforce simp add: algebra_simps divide_simps split: if_split_asm)
  3.1838 +          next
  3.1839 +            case False
  3.1840 +            with \<open>0 < inff\<close> have "inff * (a j \<bullet> y - a j \<bullet> w) \<le> 0"
  3.1841 +              by (simp add: mult_le_0_iff)
  3.1842 +            also have "... < b j - a j \<bullet> w"
  3.1843 +              by (simp add: awlt that)
  3.1844 +            finally show ?thesis by simp
  3.1845 +          qed
  3.1846 +          ultimately show ?thesis
  3.1847 +            by (blast intro: that)
  3.1848 +        qed
  3.1849 +        def c \<equiv> "(1 - T) *\<^sub>R w + T *\<^sub>R y"
  3.1850 +        have "(1 - T) *\<^sub>R w + T *\<^sub>R y \<in> j" if "j \<in> F" for j
  3.1851 +        proof (cases "j = h")
  3.1852 +          case True
  3.1853 +          have "(1 - T) *\<^sub>R w + T *\<^sub>R y \<in> {x. a h \<bullet> x \<le> b h}"
  3.1854 +            using weq yaff by (auto simp: algebra_simps)
  3.1855 +          with True faceq [OF that] show ?thesis by metis
  3.1856 +        next
  3.1857 +          case False
  3.1858 +          with T that have "(1 - T) *\<^sub>R w + T *\<^sub>R y \<in> {x. a j \<bullet> x \<le> b j}"
  3.1859 +            by (simp add: algebra_simps)
  3.1860 +          with faceq [OF that] show ?thesis by simp
  3.1861 +        qed
  3.1862 +        moreover have "(1 - T) *\<^sub>R w + T *\<^sub>R y \<in> affine hull S"
  3.1863 +          apply (rule affine_affine_hull [unfolded affine_alt, rule_format])
  3.1864 +          apply (simp add: \<open>w \<in> affine hull S\<close>)
  3.1865 +          using yaff apply blast
  3.1866 +          done
  3.1867 +        ultimately have "c \<in> S"
  3.1868 +          using seq by (force simp: c_def)
  3.1869 +        moreover have "a h \<bullet> c = b h"
  3.1870 +          using yaff by (force simp: c_def algebra_simps weq)
  3.1871 +        ultimately have caff: "c \<in> affine hull (S \<inter> {y. a h \<bullet> y = b h})"
  3.1872 +          by (simp add: hull_inc)
  3.1873 +        have waff: "w \<in> affine hull (S \<inter> {y. a h \<bullet> y = b h})"
  3.1874 +          using \<open>w \<in> S\<close> weq by (blast intro: hull_inc)
  3.1875 +        have yeq: "y = (1 - inverse T) *\<^sub>R w + c /\<^sub>R T"
  3.1876 +          using \<open>0 < T\<close> by (simp add: c_def algebra_simps)
  3.1877 +        show "y \<in> affine hull (S \<inter> {y. a h \<bullet> y = b h})"
  3.1878 +          by (metis yeq affine_affine_hull [unfolded affine_alt, rule_format, OF waff caff])
  3.1879 +      qed
  3.1880 +    qed
  3.1881 +    ultimately show ?thesis
  3.1882 +      apply (simp add: facet_of_def)
  3.1883 +      apply (subst aff_dim_affine_hull [symmetric])
  3.1884 +      using  \<open>b h < a h \<bullet> z\<close> zaff
  3.1885 +      apply (force simp: aff_dim_affine_Int_hyperplane)
  3.1886 +      done
  3.1887 +  qed
  3.1888 +  show ?thesis
  3.1889 +  proof
  3.1890 +    show "\<exists>h. h \<in> F \<and> c = S \<inter> {x. a h \<bullet> x = b h} \<Longrightarrow> c facet_of S"
  3.1891 +      using * by blast
  3.1892 +  next
  3.1893 +    assume "c facet_of S"
  3.1894 +    then have "c face_of S" "convex c" "c \<noteq> {}" and affc: "aff_dim c = aff_dim S - 1"
  3.1895 +      by (auto simp: facet_of_def face_of_imp_convex)
  3.1896 +    then obtain x where x: "x \<in> rel_interior c"
  3.1897 +      by (force simp: rel_interior_eq_empty)
  3.1898 +    then have "x \<in> c"
  3.1899 +      by (meson subsetD rel_interior_subset)
  3.1900 +    then have "x \<in> S"
  3.1901 +      using \<open>c facet_of S\<close> facet_of_imp_subset by blast
  3.1902 +    have rels: "rel_interior S = {x \<in> S. \<forall>h\<in>F. a h \<bullet> x < b h}"
  3.1903 +      by (rule rel_interior_polyhedron_explicit [OF assms])
  3.1904 +    have "c \<noteq> S"
  3.1905 +      using \<open>c facet_of S\<close> facet_of_irrefl by blast
  3.1906 +    then have "x \<notin> rel_interior S"
  3.1907 +      by (metis IntI empty_iff \<open>x \<in> c\<close> \<open>c \<noteq> S\<close> \<open>c face_of S\<close> face_of_disjoint_rel_interior)
  3.1908 +    with rels \<open>x \<in> S\<close> obtain i where "i \<in> F" and i: "a i \<bullet> x \<ge> b i"
  3.1909 +      by force
  3.1910 +    have "x \<in> {u. a i \<bullet> u \<le> b i}"
  3.1911 +      by (metis IntD2 InterE \<open>i \<in> F\<close> \<open>x \<in> S\<close> faceq seq)
  3.1912 +    then have "a i \<bullet> x \<le> b i" by simp
  3.1913 +    then have "a i \<bullet> x = b i" using i by auto
  3.1914 +    have "c \<subseteq> S \<inter> {x. a i \<bullet> x = b i}"
  3.1915 +      apply (rule subset_of_face_of [of _ S])
  3.1916 +        apply (simp add: "*" \<open>i \<in> F\<close> facet_of_imp_face_of)
  3.1917 +       apply (simp add: \<open>c face_of S\<close> face_of_imp_subset)
  3.1918 +      using \<open>a i \<bullet> x = b i\<close> \<open>x \<in> S\<close> x by blast
  3.1919 +    then have cface: "c face_of (S \<inter> {x. a i \<bullet> x = b i})"
  3.1920 +      by (meson \<open>c face_of S\<close> face_of_subset inf_le1)
  3.1921 +    have con: "convex (S \<inter> {x. a i \<bullet> x = b i})"
  3.1922 +      by (simp add: \<open>convex S\<close> convex_Int convex_hyperplane)
  3.1923 +    show "\<exists>h. h \<in> F \<and> c = S \<inter> {x. a h \<bullet> x = b h}"
  3.1924 +      apply (rule_tac x=i in exI)
  3.1925 +      apply (simp add: \<open>i \<in> F\<close>)
  3.1926 +      by (metis (no_types) * \<open>i \<in> F\<close> affc facet_of_def less_irrefl face_of_aff_dim_lt [OF con cface])
  3.1927 +  qed
  3.1928 +qed
  3.1929 +
  3.1930 +
  3.1931 +lemma face_of_polyhedron_subset_explicit:
  3.1932 +  fixes S :: "'a :: euclidean_space set"
  3.1933 +  assumes "finite F"
  3.1934 +      and seq: "S = affine hull S \<inter> \<Inter>F"
  3.1935 +      and faceq: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
  3.1936 +      and psub: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> affine hull S \<inter> \<Inter>F'"
  3.1937 +      and c: "c face_of S" and "c \<noteq> {}" "c \<noteq> S"
  3.1938 +   obtains h where "h \<in> F" "c \<subseteq> S \<inter> {x. a h \<bullet> x = b h}"
  3.1939 +proof -
  3.1940 +  have "c \<subseteq> S" using \<open>c face_of S\<close>
  3.1941 +    by (simp add: face_of_imp_subset)
  3.1942 +  have "polyhedron S"
  3.1943 +    apply (simp add: polyhedron_Int_affine)
  3.1944 +    by (metis \<open>finite F\<close> faceq seq)
  3.1945 +  then have "convex S"
  3.1946 +    by (simp add: polyhedron_imp_convex)
  3.1947 +  then have *: "(S \<inter> {x. a h \<bullet> x = b h}) face_of S" if "h \<in> F" for h
  3.1948 +    apply (rule face_of_Int_supporting_hyperplane_le)
  3.1949 +    using faceq seq that by fastforce
  3.1950 +  have "rel_interior c \<noteq> {}"
  3.1951 +    using c \<open>c \<noteq> {}\<close> face_of_imp_convex rel_interior_eq_empty by blast
  3.1952 +  then obtain x where "x \<in> rel_interior c" by auto
  3.1953 +  have rels: "rel_interior S = {x \<in> S. \<forall>h\<in>F. a h \<bullet> x < b h}"
  3.1954 +    by (rule rel_interior_polyhedron_explicit [OF \<open>finite F\<close> seq faceq psub])
  3.1955 +  then have xnot: "x \<notin> rel_interior S"
  3.1956 +    by (metis IntI \<open>x \<in> rel_interior c\<close> c \<open>c \<noteq> S\<close> contra_subsetD empty_iff face_of_disjoint_rel_interior rel_interior_subset)
  3.1957 +  then have "x \<in> S"
  3.1958 +    using \<open>c \<subseteq> S\<close> \<open>x \<in> rel_interior c\<close> rel_interior_subset by auto
  3.1959 +  then have xint: "x \<in> \<Inter>F"
  3.1960 +    using seq by blast
  3.1961 +  have "F \<noteq> {}" using assms
  3.1962 +    by (metis affine_Int affine_Inter affine_affine_hull ex_in_conv face_of_affine_trivial)
  3.1963 +  then obtain i where "i \<in> F" "~ (a i \<bullet> x < b i)"
  3.1964 +    using \<open>x \<in> S\<close> rels xnot by auto
  3.1965 +  with xint have "a i \<bullet> x = b i"
  3.1966 +    by (metis eq_iff mem_Collect_eq not_le Inter_iff faceq)
  3.1967 +  have face: "S \<inter> {x. a i \<bullet> x = b i} face_of S"
  3.1968 +    by (simp add: "*" \<open>i \<in> F\<close>)
  3.1969 +  show ?thesis
  3.1970 +    apply (rule_tac h = i in that)
  3.1971 +     apply (rule \<open>i \<in> F\<close>)
  3.1972 +    apply (rule subset_of_face_of [OF face \<open>c \<subseteq> S\<close>])
  3.1973 +    using \<open>a i \<bullet> x = b i\<close> \<open>x \<in> rel_interior c\<close> \<open>x \<in> S\<close> apply blast
  3.1974 +    done
  3.1975 +qed
  3.1976 +
  3.1977 +text\<open>Initial part of proof duplicates that above\<close>
  3.1978 +proposition face_of_polyhedron_explicit:
  3.1979 +  fixes S :: "'a :: euclidean_space set"
  3.1980 +  assumes "finite F"
  3.1981 +      and seq: "S = affine hull S \<inter> \<Inter>F"
  3.1982 +      and faceq: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
  3.1983 +      and psub: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> affine hull S \<inter> \<Inter>F'"
  3.1984 +      and c: "c face_of S" and "c \<noteq> {}" "c \<noteq> S"
  3.1985 +    shows "c = \<Inter>{S \<inter> {x. a h \<bullet> x = b h} | h. h \<in> F \<and> c \<subseteq> S \<inter> {x. a h \<bullet> x = b h}}"
  3.1986 +proof -
  3.1987 +  let ?ab = "\<lambda>h. {x. a h \<bullet> x = b h}"
  3.1988 +  have "c \<subseteq> S" using \<open>c face_of S\<close>
  3.1989 +    by (simp add: face_of_imp_subset)
  3.1990 +  have "polyhedron S"
  3.1991 +    apply (simp add: polyhedron_Int_affine)
  3.1992 +    by (metis \<open>finite F\<close> faceq seq)
  3.1993 +  then have "convex S"
  3.1994 +    by (simp add: polyhedron_imp_convex)
  3.1995 +  then have *: "(S \<inter> ?ab h) face_of S" if "h \<in> F" for h
  3.1996 +    apply (rule face_of_Int_supporting_hyperplane_le)
  3.1997 +    using faceq seq that by fastforce
  3.1998 +  have "rel_interior c \<noteq> {}"
  3.1999 +    using c \<open>c \<noteq> {}\<close> face_of_imp_convex rel_interior_eq_empty by blast
  3.2000 +  then obtain z where z: "z \<in> rel_interior c" by auto
  3.2001 +  have rels: "rel_interior S = {z \<in> S. \<forall>h\<in>F. a h \<bullet> z < b h}"
  3.2002 +    by (rule rel_interior_polyhedron_explicit [OF \<open>finite F\<close> seq faceq psub])
  3.2003 +  then have xnot: "z \<notin> rel_interior S"
  3.2004 +    by (metis IntI \<open>z \<in> rel_interior c\<close> c \<open>c \<noteq> S\<close> contra_subsetD empty_iff face_of_disjoint_rel_interior rel_interior_subset)
  3.2005 +  then have "z \<in> S"
  3.2006 +    using \<open>c \<subseteq> S\<close> \<open>z \<in> rel_interior c\<close> rel_interior_subset by auto
  3.2007 +  with seq have xint: "z \<in> \<Inter>F" by blast
  3.2008 +  have "open (\<Inter>h\<in>{h \<in> F. a h \<bullet> z < b h}. {w. a h \<bullet> w < b h})"
  3.2009 +    by (auto simp: \<open>finite F\<close> open_halfspace_lt open_INT)
  3.2010 +  then obtain e where "0 < e"
  3.2011 +                 "ball z e \<subseteq> (\<Inter>h\<in>{h \<in> F. a h \<bullet> z < b h}. {w. a h \<bullet> w < b h})"
  3.2012 +    by (auto intro: openE [of _ z])
  3.2013 +  then have e: "\<And>h. \<lbrakk>h \<in> F; a h \<bullet> z < b h\<rbrakk> \<Longrightarrow> ball z e \<subseteq> {w. a h \<bullet> w < b h}"
  3.2014 +    by blast
  3.2015 +  have "c \<subseteq> (S \<inter> ?ab h) \<longleftrightarrow> z \<in> S \<inter> ?ab h" if "h \<in> F" for h
  3.2016 +  proof
  3.2017 +    show "z \<in> S \<inter> ?ab h \<Longrightarrow> c \<subseteq> S \<inter> ?ab h"
  3.2018 +      apply (rule subset_of_face_of [of _ S])
  3.2019 +      using that \<open>c \<subseteq> S\<close> \<open>z \<in> rel_interior c\<close>
  3.2020 +      using facet_of_polyhedron_explicit [OF \<open>finite F\<close> seq faceq psub]
  3.2021 +            unfolding facet_of_def
  3.2022 +      apply auto
  3.2023 +      done
  3.2024 +  next
  3.2025 +    show "c \<subseteq> S \<inter> ?ab h \<Longrightarrow> z \<in> S \<inter> ?ab h"
  3.2026 +      using \<open>z \<in> rel_interior c\<close> rel_interior_subset by force
  3.2027 +  qed
  3.2028 +  then have **: "{S \<inter> ?ab h | h. h \<in> F \<and> c \<subseteq> S \<and> c \<subseteq> ?ab h} =
  3.2029 +                 {S \<inter> ?ab h |h. h \<in> F \<and> z \<in> S \<inter> ?ab h}"
  3.2030 +    by blast
  3.2031 +  have bsub: "ball z e \<inter> affine hull \<Inter>{S \<inter> ?ab h |h. h \<in> F \<and> a h \<bullet> z = b h}
  3.2032 +             \<subseteq> affine hull S \<inter> \<Inter>F \<inter> \<Inter>{?ab h |h. h \<in> F \<and> a h \<bullet> z = b h}"
  3.2033 +            if "i \<in> F" and i: "a i \<bullet> z = b i" for i
  3.2034 +  proof -
  3.2035 +    have sub: "ball z e \<inter> \<Inter>{?ab h |h. h \<in> F \<and> a h \<bullet> z = b h} \<subseteq> j"
  3.2036 +             if "j \<in> F" for j
  3.2037 +    proof -
  3.2038 +      have "a j \<bullet> z \<le> b j" using faceq that xint by auto
  3.2039 +      then consider "a j \<bullet> z < b j" | "a j \<bullet> z = b j" by linarith
  3.2040 +      then have "\<exists>G. G \<in> {?ab h |h. h \<in> F \<and> a h \<bullet> z = b h} \<and> ball z e \<inter> G \<subseteq> j"
  3.2041 +      proof cases
  3.2042 +        assume "a j \<bullet> z < b j"
  3.2043 +        then have "ball z e \<inter> {x. a i \<bullet> x = b i} \<subseteq> j"
  3.2044 +          using e [OF \<open>j \<in> F\<close>] faceq that
  3.2045 +          by (fastforce simp: ball_def)
  3.2046 +        then show ?thesis
  3.2047 +          by (rule_tac x="{x. a i \<bullet> x = b i}" in exI) (force simp: \<open>i \<in> F\<close> i)
  3.2048 +      next
  3.2049 +        assume eq: "a j \<bullet> z = b j"
  3.2050 +        with faceq that show ?thesis
  3.2051 +          by (rule_tac x="{x. a j \<bullet> x = b j}" in exI) (fastforce simp add: \<open>j \<in> F\<close>)
  3.2052 +      qed
  3.2053 +      then show ?thesis  by blast
  3.2054 +    qed
  3.2055 +    have 1: "affine hull \<Inter>{S \<inter> ?ab h |h. h \<in> F \<and> a h \<bullet> z = b h} \<subseteq> affine hull S"
  3.2056 +      apply (rule hull_mono)
  3.2057 +      using that \<open>z \<in> S\<close> by auto
  3.2058 +    have 2: "affine hull \<Inter>{S \<inter> ?ab h |h. h \<in> F \<and> a h \<bullet> z = b h}
  3.2059 +          \<subseteq> \<Inter>{?ab h |h. h \<in> F \<and> a h \<bullet> z = b h}"
  3.2060 +      by (rule hull_minimal) (auto intro: affine_hyperplane)
  3.2061 +    have 3: "ball z e \<inter> \<Inter>{?ab h |h. h \<in> F \<and> a h \<bullet> z = b h} \<subseteq> \<Inter>F"
  3.2062 +      by (iprover intro: sub Inter_greatest)
  3.2063 +    have *: "\<lbrakk>A \<subseteq> (B :: 'a set); A \<subseteq> C; E \<inter> C \<subseteq> D\<rbrakk> \<Longrightarrow> E \<inter> A \<subseteq> (B \<inter> D) \<inter> C"
  3.2064 +             for A B C D E  by blast
  3.2065 +    show ?thesis by (intro * 1 2 3)
  3.2066 +  qed
  3.2067 +  have "\<exists>h. h \<in> F \<and> c \<subseteq> ?ab h"
  3.2068 +    apply (rule face_of_polyhedron_subset_explicit [OF \<open>finite F\<close> seq faceq psub])
  3.2069 +    using assms by auto
  3.2070 +  then have fac: "\<Inter>{S \<inter> ?ab h |h. h \<in> F \<and> c \<subseteq> S \<inter> ?ab h} face_of S"
  3.2071 +    using * by (force simp: \<open>c \<subseteq> S\<close> intro: face_of_Inter)
  3.2072 +  have red:
  3.2073 +     "(\<And>a. P a \<Longrightarrow> T \<subseteq> S \<inter> \<Inter>{F x |x. P x}) \<Longrightarrow> T \<subseteq> \<Inter>{S \<inter> F x |x. P x}"
  3.2074 +     for P T F   by blast
  3.2075 +  have "ball z e \<inter> affine hull \<Inter>{S \<inter> ?ab h |h. h \<in> F \<and> a h \<bullet> z = b h}
  3.2076 +        \<subseteq> \<Inter>{S \<inter> ?ab h |h. h \<in> F \<and> a h \<bullet> z = b h}"
  3.2077 +    apply (rule red)
  3.2078 +    apply (metis seq bsub)
  3.2079 +    done
  3.2080 +  with \<open>0 < e\<close> have zinrel: "z \<in> rel_interior
  3.2081 +                    (\<Inter>{S \<inter> ?ab h |h. h \<in> F \<and> z \<in> S \<and> a h \<bullet> z = b h})"
  3.2082 +    by (auto simp: mem_rel_interior_ball \<open>z \<in> S\<close>)
  3.2083 +  show ?thesis
  3.2084 +    apply (rule face_of_eq [OF c fac])
  3.2085 +    using z zinrel apply (force simp: **)
  3.2086 +    done
  3.2087 +qed
  3.2088 +
  3.2089 +
  3.2090 +subsection\<open>More general corollaries from the explicit representation\<close>
  3.2091 +
  3.2092 +corollary facet_of_polyhedron:
  3.2093 +  assumes "polyhedron S" and "c facet_of S"
  3.2094 +  obtains a b where "a \<noteq> 0" "S \<subseteq> {x. a \<bullet> x \<le> b}" "c = S \<inter> {x. a \<bullet> x = b}"
  3.2095 +proof -
  3.2096 +  obtain F where "finite F" and seq: "S = affine hull S \<inter> \<Inter>F"
  3.2097 +             and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
  3.2098 +             and min: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> (affine hull S) \<inter> \<Inter>F'"
  3.2099 +    using assms by (simp add: polyhedron_Int_affine_minimal) meson
  3.2100 +  then obtain a b where ab: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
  3.2101 +    by metis
  3.2102 +  obtain i where "i \<in> F" and c: "c = S \<inter> {x. a i \<bullet> x = b i}"
  3.2103 +    using facet_of_polyhedron_explicit [OF \<open>finite F\<close> seq ab min] assms
  3.2104 +    by force
  3.2105 +  moreover have ssub: "S \<subseteq> {x. a i \<bullet> x \<le> b i}"
  3.2106 +     apply (subst seq)
  3.2107 +     using \<open>i \<in> F\<close> ab by auto
  3.2108 +  ultimately show ?thesis
  3.2109 +    by (rule_tac a = "a i" and b = "b i" in that) (simp_all add: ab)
  3.2110 +qed
  3.2111 +
  3.2112 +corollary face_of_polyhedron:
  3.2113 +  assumes "polyhedron S" and "c face_of S" and "c \<noteq> {}" and "c \<noteq> S"
  3.2114 +    shows "c = \<Inter>{F. F facet_of S \<and> c \<subseteq> F}"
  3.2115 +proof -
  3.2116 +  obtain F where "finite F" and seq: "S = affine hull S \<inter> \<Inter>F"
  3.2117 +             and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
  3.2118 +             and min: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> (affine hull S) \<inter> \<Inter>F'"
  3.2119 +    using assms by (simp add: polyhedron_Int_affine_minimal) meson
  3.2120 +  then obtain a b where ab: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
  3.2121 +    by metis
  3.2122 +  show ?thesis
  3.2123 +    apply (subst face_of_polyhedron_explicit [OF \<open>finite F\<close> seq ab min])
  3.2124 +    apply (auto simp: assms facet_of_polyhedron_explicit [OF \<open>finite F\<close> seq ab min] cong: Collect_cong)
  3.2125 +    done
  3.2126 +qed
  3.2127 +
  3.2128 +lemma face_of_polyhedron_subset_facet:
  3.2129 +  assumes "polyhedron S" and "c face_of S" and "c \<noteq> {}" and "c \<noteq> S"
  3.2130 +  obtains F where "F facet_of S" "c \<subseteq> F"
  3.2131 +using face_of_polyhedron assms
  3.2132 +by (metis (no_types, lifting) Inf_greatest antisym_conv face_of_imp_subset mem_Collect_eq)
  3.2133 +
  3.2134 +
  3.2135 +lemma exposed_face_of_polyhedron:
  3.2136 +  assumes "polyhedron S"
  3.2137 +    shows "F exposed_face_of S \<longleftrightarrow> F face_of S"
  3.2138 +proof
  3.2139 +  show "F exposed_face_of S \<Longrightarrow> F face_of S"
  3.2140 +    by (simp add: exposed_face_of_def)
  3.2141 +next
  3.2142 +  assume "F face_of S"
  3.2143 +  show "F exposed_face_of S"
  3.2144 +  proof (cases "F = {} \<or> F = S")
  3.2145 +    case True then show ?thesis
  3.2146 +      using \<open>F face_of S\<close> exposed_face_of by blast
  3.2147 +  next
  3.2148 +    case False
  3.2149 +    then have "{g. g facet_of S \<and> F \<subseteq> g} \<noteq> {}"
  3.2150 +      by (metis Collect_empty_eq_bot \<open>F face_of S\<close> assms empty_def face_of_polyhedron_subset_facet)
  3.2151 +    moreover have "\<And>T. \<lbrakk>T facet_of S; F \<subseteq> T\<rbrakk> \<Longrightarrow> T exposed_face_of S"
  3.2152 +      by (metis assms exposed_face_of facet_of_imp_face_of facet_of_polyhedron)
  3.2153 +    ultimately have "\<Inter>{fa.
  3.2154 +       fa facet_of S \<and> F \<subseteq> fa} exposed_face_of S"
  3.2155 +      by (metis (no_types, lifting) mem_Collect_eq exposed_face_of_Inter)
  3.2156 +    then show ?thesis
  3.2157 +      using False
  3.2158 +      apply (subst face_of_polyhedron [OF assms \<open>F face_of S\<close>], auto)
  3.2159 +      done
  3.2160 +  qed
  3.2161 +qed
  3.2162 +
  3.2163 +lemma face_of_polyhedron_polyhedron:
  3.2164 +  fixes S :: "'a :: euclidean_space set"
  3.2165 +  assumes "polyhedron S" "c face_of S"
  3.2166 +    shows "polyhedron c"
  3.2167 +proof -
  3.2168 +  obtain F where "finite F" and seq: "S = affine hull S \<inter> \<Inter>F"
  3.2169 +             and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
  3.2170 +             and min:   "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> (affine hull S) \<inter> \<Inter>F'"
  3.2171 +    using assms by (simp add: polyhedron_Int_affine_minimal) meson
  3.2172 +  then obtain a b where ab: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
  3.2173 +    by metis
  3.2174 +  show ?thesis
  3.2175 +  proof (cases "c = {} \<or> c = S")
  3.2176 +    case True with assms show ?thesis
  3.2177 +      by auto
  3.2178 +  next
  3.2179 +    case False
  3.2180 +    let ?ab = "\<lambda>h. {x. a h \<bullet> x = b h}"
  3.2181 +    have "{S \<inter> ?ab h |h. h \<in> F \<and> c \<subseteq> S \<inter> ?ab h} \<subseteq> {S \<inter> ?ab h |h. h \<in> F}"
  3.2182 +      by blast
  3.2183 +    then have fin: "finite ({S \<inter> ?ab h |h. h \<in> F \<and> c \<subseteq> S \<inter> ?ab h})"
  3.2184 +      by (rule finite_subset) (simp add: \<open>finite F\<close>)
  3.2185 +    then have "polyhedron (\<Inter>{S \<inter> ?ab h |h. h \<in> F \<and> c \<subseteq> S \<inter> ?ab h})"
  3.2186 +      by (auto simp: \<open>polyhedron S\<close> polyhedron_hyperplane)
  3.2187 +    with False show ?thesis
  3.2188 +      using face_of_polyhedron_explicit [OF \<open>finite F\<close> seq ab min] assms
  3.2189 +      by auto
  3.2190 +  qed
  3.2191 +qed
  3.2192 +
  3.2193 +
  3.2194 +lemma finite_polyhedron_faces:
  3.2195 +  fixes S :: "'a :: euclidean_space set"
  3.2196 +  assumes "polyhedron S"
  3.2197 +    shows "finite {F. F face_of S}"
  3.2198 +proof -
  3.2199 +  obtain F where "finite F" and seq: "S = affine hull S \<inter> \<Inter>F"
  3.2200 +             and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
  3.2201 +             and min:   "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> (affine hull S) \<inter> \<Inter>F'"
  3.2202 +    using assms by (simp add: polyhedron_Int_affine_minimal) meson
  3.2203 +  then obtain a b where ab: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
  3.2204 +    by metis
  3.2205 +  have "finite {\<Inter>{S \<inter> {x. a h \<bullet> x = b h} |h. h \<in> F'}| F'. F' \<in> Pow F}"
  3.2206 +    by (simp add: \<open>finite F\<close>)
  3.2207 +  moreover have "{F. F face_of S} - {{}, S} \<subseteq> {\<Inter>{S \<inter> {x. a h \<bullet> x = b h} |h. h \<in> F'}| F'. F' \<in> Pow F}"
  3.2208 +    apply clarify
  3.2209 +    apply (rename_tac c)
  3.2210 +    apply (drule face_of_polyhedron_explicit [OF \<open>finite F\<close> seq ab min, simplified], simp_all)
  3.2211 +    apply (erule ssubst)
  3.2212 +    apply (rule_tac x="{h \<in> F. c \<subseteq> S \<inter> {x. a h \<bullet> x = b h}}" in exI, auto)
  3.2213 +    done
  3.2214 +  ultimately show ?thesis
  3.2215 +    by (meson finite.emptyI finite.insertI finite_Diff2 finite_subset)
  3.2216 +qed
  3.2217 +
  3.2218 +lemma finite_polyhedron_exposed_faces:
  3.2219 +   "polyhedron S \<Longrightarrow> finite {F. F exposed_face_of S}"
  3.2220 +using exposed_face_of_polyhedron finite_polyhedron_faces by fastforce
  3.2221 +
  3.2222 +lemma finite_polyhedron_extreme_points:
  3.2223 +  fixes S :: "'a :: euclidean_space set"
  3.2224 +  shows "polyhedron S \<Longrightarrow> finite {v. v extreme_point_of S}"
  3.2225 +apply (simp add: face_of_singleton [symmetric])
  3.2226 +apply (rule finite_subset [OF _ finite_vimageI [OF finite_polyhedron_faces]], auto)
  3.2227 +done
  3.2228 +
  3.2229 +lemma finite_polyhedron_facets:
  3.2230 +  fixes S :: "'a :: euclidean_space set"
  3.2231 +  shows "polyhedron S \<Longrightarrow> finite {F. F facet_of S}"
  3.2232 +unfolding facet_of_def
  3.2233 +by (blast intro: finite_subset [OF _ finite_polyhedron_faces])
  3.2234 +
  3.2235 +
  3.2236 +proposition rel_interior_of_polyhedron:
  3.2237 +  fixes S :: "'a :: euclidean_space set"
  3.2238 +  assumes "polyhedron S"
  3.2239 +    shows "rel_interior S = S - \<Union>{F. F facet_of S}"
  3.2240 +proof -
  3.2241 +  obtain F where "finite F" and seq: "S = affine hull S \<inter> \<Inter>F"
  3.2242 +             and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
  3.2243 +             and min: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> (affine hull S) \<inter> \<Inter>F'"
  3.2244 +    using assms by (simp add: polyhedron_Int_affine_minimal) meson
  3.2245 +  then obtain a b where ab: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
  3.2246 +    by metis
  3.2247 +  have facet: "(c facet_of S) \<longleftrightarrow> (\<exists>h. h \<in> F \<and> c = S \<inter> {x. a h \<bullet> x = b h})" for c
  3.2248 +    by (rule facet_of_polyhedron_explicit [OF \<open>finite F\<close> seq ab min])
  3.2249 +  have rel: "rel_interior S = {x \<in> S. \<forall>h\<in>F. a h \<bullet> x < b h}"
  3.2250 +    by (rule rel_interior_polyhedron_explicit [OF \<open>finite F\<close> seq ab min])
  3.2251 +  have "a h \<bullet> x < b h" if "x \<in> S" "h \<in> F" and xnot: "x \<notin> \<Union>{F. F facet_of S}" for x h
  3.2252 +  proof -
  3.2253 +    have "x \<in> \<Inter>F" using seq that by force
  3.2254 +    with \<open>h \<in> F\<close> ab have "a h \<bullet> x \<le> b h" by auto
  3.2255 +    then consider "a h \<bullet> x < b h" | "a h \<bullet> x = b h" by linarith
  3.2256 +    then show ?thesis
  3.2257 +    proof cases
  3.2258 +      case 1 then show ?thesis .
  3.2259 +    next
  3.2260 +      case 2
  3.2261 +      have "Collect (op \<in> x) \<notin> Collect (op \<in> (\<Union>{A. A facet_of S}))"
  3.2262 +        using xnot by fastforce
  3.2263 +      then have "F \<notin> Collect (op \<in> h)"
  3.2264 +        using 2 \<open>x \<in> S\<close> facet by blast
  3.2265 +      with \<open>h \<in> F\<close> have "\<Inter>F \<subseteq> S \<inter> {x. a h \<bullet> x = b h}" by blast
  3.2266 +      with 2 that \<open>x \<in> \<Inter>F\<close> show ?thesis
  3.2267 +        apply simp
  3.2268 +        apply (drule_tac x="\<Inter>F" in spec)
  3.2269 +        apply (simp add: facet)
  3.2270 +        apply (drule_tac x=h in spec)
  3.2271 +        using seq by auto
  3.2272 +      qed
  3.2273 +  qed
  3.2274 +  moreover have "\<exists>h\<in>F. a h \<bullet> x \<ge> b h" if "x \<in> \<Union>{F. F facet_of S}" for x
  3.2275 +    using that by (force simp: facet)
  3.2276 +  ultimately show ?thesis
  3.2277 +    by (force simp: rel)
  3.2278 +qed
  3.2279 +
  3.2280 +lemma rel_boundary_of_polyhedron:
  3.2281 +  fixes S :: "'a :: euclidean_space set"
  3.2282 +  assumes "polyhedron S"
  3.2283 +    shows "S - rel_interior S = \<Union> {F. F facet_of S}"
  3.2284 +using facet_of_imp_subset by (fastforce simp add: rel_interior_of_polyhedron assms)
  3.2285 +
  3.2286 +lemma rel_frontier_of_polyhedron:
  3.2287 +  fixes S :: "'a :: euclidean_space set"
  3.2288 +  assumes "polyhedron S"
  3.2289 +    shows "rel_frontier S = \<Union> {F. F facet_of S}"
  3.2290 +by (simp add: assms rel_frontier_def polyhedron_imp_closed rel_boundary_of_polyhedron)
  3.2291 +
  3.2292 +lemma rel_frontier_of_polyhedron_alt:
  3.2293 +  fixes S :: "'a :: euclidean_space set"
  3.2294 +  assumes "polyhedron S"
  3.2295 +    shows "rel_frontier S = \<Union> {F. F face_of S \<and> (F \<noteq> S)}"
  3.2296 +apply (rule subset_antisym)
  3.2297 +  apply (force simp: rel_frontier_of_polyhedron facet_of_def assms)
  3.2298 +using face_of_subset_rel_frontier by fastforce
  3.2299 +
  3.2300 +
  3.2301 +text\<open>A characterization of polyhedra as having finitely many faces\<close>
  3.2302 +
  3.2303 +proposition polyhedron_eq_finite_exposed_faces:
  3.2304 +  fixes S :: "'a :: euclidean_space set"
  3.2305 +  shows "polyhedron S \<longleftrightarrow> closed S \<and> convex S \<and> finite {F. F exposed_face_of S}"
  3.2306 +         (is "?lhs = ?rhs")
  3.2307 +proof
  3.2308 +  assume ?lhs
  3.2309 +  then show ?rhs
  3.2310 +    by (auto simp: polyhedron_imp_closed polyhedron_imp_convex finite_polyhedron_exposed_faces)
  3.2311 +next
  3.2312 +  assume ?rhs
  3.2313 +  then have "closed S" "convex S" and fin: "finite {F. F exposed_face_of S}" by auto
  3.2314 +  show ?lhs
  3.2315 +  proof (cases "S = {}")
  3.2316 +    case True then show ?thesis by auto
  3.2317 +  next
  3.2318 +    case False
  3.2319 +    def F \<equiv> "{h. h exposed_face_of S \<and> h \<noteq> {} \<and> h \<noteq> S}"
  3.2320 +    have "finite F" by (simp add: fin F_def)
  3.2321 +    have hface: "h face_of S"
  3.2322 +                and "\<exists>a b. a \<noteq> 0 \<and> S \<subseteq> {x. a \<bullet> x \<le> b} \<and> h = S \<inter> {x. a \<bullet> x = b}"
  3.2323 +         if "h \<in> F" for h
  3.2324 +      using exposed_face_of F_def that by simp_all auto
  3.2325 +    then obtain a b where ab:
  3.2326 +      "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> S \<subseteq> {x. a h \<bullet> x \<le> b h} \<and> h = S \<inter> {x. a h \<bullet> x = b h}"
  3.2327 +      by metis
  3.2328 +    have *: "False"
  3.2329 +      if paff: "p \<in> affine hull S" and "p \<notin> S" and
  3.2330 +         pint: "p \<in> \<Inter>{{x. a h \<bullet> x \<le> b h} |h. h \<in> F}" for p
  3.2331 +    proof -
  3.2332 +      have "rel_interior S \<noteq> {}"
  3.2333 +        by (simp add: \<open>S \<noteq> {}\<close> \<open>convex S\<close> rel_interior_eq_empty)
  3.2334 +      then obtain c where c: "c \<in> rel_interior S" by auto
  3.2335 +      with rel_interior_subset have "c \<in> S"  by blast
  3.2336 +      have ccp: "closed_segment c p \<subseteq> affine hull S"
  3.2337 +        by (meson affine_affine_hull affine_imp_convex c closed_segment_subset hull_subset paff rel_interior_subset subsetCE)
  3.2338 +      obtain x where xcl: "x \<in> closed_segment c p" and "x \<in> S" and xnot: "x \<notin> rel_interior S"
  3.2339 +        using connected_openin [of "closed_segment c p"]
  3.2340 +        apply simp
  3.2341 +        apply (drule_tac x="closed_segment c p \<inter> rel_interior S" in spec)
  3.2342 +        apply (erule impE)
  3.2343 +         apply (force simp: openin_rel_interior openin_Int intro: openin_subtopology_Int_subset [OF _ ccp])
  3.2344 +        apply (drule_tac x="closed_segment c p \<inter> (- S)" in spec)
  3.2345 +        using rel_interior_subset \<open>closed S\<close> c \<open>p \<notin> S\<close> apply blast
  3.2346 +        done
  3.2347 +      then obtain \<mu> where "0 \<le> \<mu>" "\<mu> \<le> 1" and xeq: "x = (1 - \<mu>) *\<^sub>R c + \<mu> *\<^sub>R p"
  3.2348 +        by (auto simp: in_segment)
  3.2349 +      show False
  3.2350 +      proof (cases "\<mu>=0 \<or> \<mu>=1")
  3.2351 +        case True with xeq c xnot \<open>x \<in> S\<close> \<open>p \<notin> S\<close>
  3.2352 +        show False by auto
  3.2353 +      next
  3.2354 +        case False
  3.2355 +        then have xos: "x \<in> open_segment c p"
  3.2356 +          using \<open>x \<in> S\<close> c open_segment_def that(2) xcl xnot by auto
  3.2357 +        have xclo: "x \<in> closure S"
  3.2358 +          using \<open>x \<in> S\<close> closure_subset by blast
  3.2359 +        obtain d where "d \<noteq> 0"
  3.2360 +              and dle: "\<And>y. y \<in> closure S \<Longrightarrow> d \<bullet> x \<le> d \<bullet> y"
  3.2361 +              and dless: "\<And>y. y \<in> rel_interior S \<Longrightarrow> d \<bullet> x < d \<bullet> y"
  3.2362 +          by (metis supporting_hyperplane_relative_frontier [OF \<open>convex S\<close> xclo xnot])
  3.2363 +        have sex: "S \<inter> {y. d \<bullet> y = d \<bullet> x} exposed_face_of S"
  3.2364 +          by (simp add: \<open>closed S\<close> dle exposed_face_of_Int_supporting_hyperplane_ge [OF \<open>convex S\<close>])
  3.2365 +        have sne: "S \<inter> {y. d \<bullet> y = d \<bullet> x} \<noteq> {}"
  3.2366 +          using \<open>x \<in> S\<close> by blast
  3.2367 +        have sns: "S \<inter> {y. d \<bullet> y = d \<bullet> x} \<noteq> S"
  3.2368 +          by (metis (mono_tags) Int_Collect c subsetD dless not_le order_refl rel_interior_subset)
  3.2369 +        obtain h where "h \<in> F" "x \<in> h"
  3.2370 +          apply (rule_tac h="S \<inter> {y. d \<bullet> y = d \<bullet> x}" in that)
  3.2371 +          apply (simp_all add: F_def sex sne sns \<open>x \<in> S\<close>)
  3.2372 +          done
  3.2373 +        have abface: "{y. a h \<bullet> y = b h} face_of {y. a h \<bullet> y \<le> b h}"
  3.2374 +          using hyperplane_face_of_halfspace_le by blast
  3.2375 +        then have "c \<in> h"
  3.2376 +          using face_ofD [OF abface xos] \<open>c \<in> S\<close> \<open>h \<in> F\<close> ab pint \<open>x \<in> h\<close> by blast
  3.2377 +        with c have "h \<inter> rel_interior S \<noteq> {}" by blast
  3.2378 +        then show False
  3.2379 +          using \<open>h \<in> F\<close> F_def face_of_disjoint_rel_interior hface by auto
  3.2380 +      qed
  3.2381 +    qed
  3.2382 +    have "S \<subseteq> affine hull S \<inter> \<Inter>{{x. a h \<bullet> x \<le> b h} |h. h \<in> F}"
  3.2383 +      using ab by (auto simp: hull_subset)
  3.2384 +    moreover have "affine hull S \<inter> \<Inter>{{x. a h \<bullet> x \<le> b h} |h. h \<in> F} \<subseteq> S"
  3.2385 +      using * by blast
  3.2386 +    ultimately have "S = affine hull S \<inter> \<Inter> {{x. a h \<bullet> x \<le> b h} |h. h \<in> F}" ..
  3.2387 +    then show ?thesis
  3.2388 +      apply (rule ssubst)
  3.2389 +      apply (force intro: polyhedron_affine_hull polyhedron_halfspace_le simp: \<open>finite F\<close>)
  3.2390 +      done
  3.2391 +  qed
  3.2392 +qed
  3.2393 +
  3.2394 +corollary polyhedron_eq_finite_faces:
  3.2395 +  fixes S :: "'a :: euclidean_space set"
  3.2396 +  shows "polyhedron S \<longleftrightarrow> closed S \<and> convex S \<and> finite {F. F face_of S}"
  3.2397 +         (is "?lhs = ?rhs")
  3.2398 +proof
  3.2399 +  assume ?lhs
  3.2400 +  then show ?rhs
  3.2401 +    by (simp add: finite_polyhedron_faces polyhedron_imp_closed polyhedron_imp_convex)
  3.2402 +next
  3.2403 +  assume ?rhs
  3.2404 +  then show ?lhs
  3.2405 +    by (force simp: polyhedron_eq_finite_exposed_faces exposed_face_of intro: finite_subset)
  3.2406 +qed
  3.2407 +
  3.2408 +lemma polyhedron_linear_image_eq:
  3.2409 +  fixes h :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
  3.2410 +  assumes "linear h" "bij h"
  3.2411 +    shows "polyhedron (h ` S) \<longleftrightarrow> polyhedron S"
  3.2412 +proof -
  3.2413 +  have *: "{f. P f} = (image h) ` {f. P (h ` f)}" for P
  3.2414 +    apply safe
  3.2415 +    apply (rule_tac x="inv h ` x" in image_eqI)
  3.2416 +    apply (auto simp: \<open>bij h\<close> bij_is_surj image_surj_f_inv_f)
  3.2417 +    done
  3.2418 +  have "inj h" using bij_is_inj assms by blast
  3.2419 +  then have injim: "inj_on (op ` h) A" for A
  3.2420 +    by (simp add: inj_on_def inj_image_eq_iff)
  3.2421 +  show ?thesis
  3.2422 +    using \<open>linear h\<close> \<open>inj h\<close>
  3.2423 +    apply (simp add: polyhedron_eq_finite_faces closed_injective_linear_image_eq)
  3.2424 +    apply (simp add: * face_of_linear_image [of h _ S, symmetric] finite_image_iff injim)
  3.2425 +    done
  3.2426 +qed
  3.2427 +
  3.2428 +lemma polyhedron_negations:
  3.2429 +  fixes S :: "'a :: euclidean_space set"
  3.2430 +  shows   "polyhedron S \<Longrightarrow> polyhedron(image uminus S)"
  3.2431 +by (auto simp: polyhedron_linear_image_eq linear_uminus bij_uminus)
  3.2432 +
  3.2433 +subsection\<open>Relation between polytopes and polyhedra\<close>
  3.2434 +
  3.2435 +lemma polytope_eq_bounded_polyhedron:
  3.2436 +  fixes S :: "'a :: euclidean_space set"
  3.2437 +  shows "polytope S \<longleftrightarrow> polyhedron S \<and> bounded S"
  3.2438 +         (is "?lhs = ?rhs")
  3.2439 +proof
  3.2440 +  assume ?lhs
  3.2441 +  then show ?rhs
  3.2442 +    by (simp add: finite_polytope_faces polyhedron_eq_finite_faces
  3.2443 +                  polytope_imp_closed polytope_imp_convex polytope_imp_bounded)
  3.2444 +next
  3.2445 +  assume ?rhs then show ?lhs
  3.2446 +    unfolding polytope_def
  3.2447 +    apply (rule_tac x="{v. v extreme_point_of S}" in exI)
  3.2448 +    apply (simp add: finite_polyhedron_extreme_points Krein_Milman_Minkowski compact_eq_bounded_closed polyhedron_imp_closed polyhedron_imp_convex)
  3.2449 +    done
  3.2450 +qed
  3.2451 +
  3.2452 +lemma polytope_Int:
  3.2453 +  fixes S :: "'a :: euclidean_space set"
  3.2454 +  shows "\<lbrakk>polytope S; polytope T\<rbrakk> \<Longrightarrow> polytope(S \<inter> T)"
  3.2455 +by (simp add: polytope_eq_bounded_polyhedron bounded_Int)
  3.2456 +
  3.2457 +
  3.2458 +lemma polytope_Int_polyhedron:
  3.2459 +  fixes S :: "'a :: euclidean_space set"
  3.2460 +  shows "\<lbrakk>polytope S; polyhedron T\<rbrakk> \<Longrightarrow> polytope(S \<inter> T)"
  3.2461 +by (simp add: bounded_Int polytope_eq_bounded_polyhedron)
  3.2462 +
  3.2463 +lemma polyhedron_Int_polytope:
  3.2464 +  fixes S :: "'a :: euclidean_space set"
  3.2465 +  shows "\<lbrakk>polyhedron S; polytope T\<rbrakk> \<Longrightarrow> polytope(S \<inter> T)"
  3.2466 +by (simp add: bounded_Int polytope_eq_bounded_polyhedron)
  3.2467 +
  3.2468 +lemma polytope_imp_polyhedron:
  3.2469 +  fixes S :: "'a :: euclidean_space set"
  3.2470 +  shows "polytope S \<Longrightarrow> polyhedron S"
  3.2471 +by (simp add: polytope_eq_bounded_polyhedron)
  3.2472 +
  3.2473 +lemma polytope_facet_exists:
  3.2474 +  fixes p :: "'a :: euclidean_space set"
  3.2475 +  assumes "polytope p" "0 < aff_dim p"
  3.2476 +  obtains F where "F facet_of p"
  3.2477 +proof (cases "p = {}")
  3.2478 +  case True with assms show ?thesis by auto
  3.2479 +next
  3.2480 +  case False
  3.2481 +  then obtain v where "v extreme_point_of p"
  3.2482 +    using extreme_point_exists_convex
  3.2483 +    by (blast intro: \<open>polytope p\<close> polytope_imp_compact polytope_imp_convex)
  3.2484 +  then
  3.2485 +  show ?thesis
  3.2486 +    by (metis face_of_polyhedron_subset_facet polytope_imp_polyhedron aff_dim_sing
  3.2487 +       all_not_in_conv assms face_of_singleton less_irrefl singletonI that)
  3.2488 +qed
  3.2489 +
  3.2490 +lemma polyhedron_interval [iff]: "polyhedron(cbox a b)"
  3.2491 +by (metis polytope_imp_polyhedron polytope_interval)
  3.2492 +
  3.2493 +lemma polyhedron_convex_hull:
  3.2494 +  fixes S :: "'a :: euclidean_space set"
  3.2495 +  shows "finite S \<Longrightarrow> polyhedron(convex hull S)"
  3.2496 +by (simp add: polytope_convex_hull polytope_imp_polyhedron)
  3.2497 +
  3.2498 +
  3.2499 +subsection\<open>Relative and absolute frontier of a polytope\<close>
  3.2500 +
  3.2501 +lemma rel_boundary_of_convex_hull:
  3.2502 +    fixes S :: "'a::euclidean_space set"
  3.2503 +    assumes "~ affine_dependent S"
  3.2504 +      shows "(convex hull S) - rel_interior(convex hull S) = (\<Union>a\<in>S. convex hull (S - {a}))"
  3.2505 +proof -
  3.2506 +  have "finite S" by (metis assms aff_independent_finite)
  3.2507 +  then consider "card S = 0" | "card S = 1" | "2 \<le> card S" by arith
  3.2508 +  then show ?thesis
  3.2509 +  proof cases
  3.2510 +    case 1 then have "S = {}" by (simp add: `finite S`)
  3.2511 +    then show ?thesis by simp
  3.2512 +  next
  3.2513 +    case 2 show ?thesis
  3.2514 +      by (auto intro: card_1_singletonE [OF `card S = 1`])
  3.2515 +  next
  3.2516 +    case 3
  3.2517 +    with assms show ?thesis
  3.2518 +      by (auto simp: polyhedron_convex_hull rel_boundary_of_polyhedron facet_of_convex_hull_affine_independent_alt \<open>finite S\<close>)
  3.2519 +  qed
  3.2520 +qed
  3.2521 +
  3.2522 +proposition frontier_of_convex_hull:
  3.2523 +    fixes S :: "'a::euclidean_space set"
  3.2524 +    assumes "card S = Suc (DIM('a))"
  3.2525 +      shows "frontier(convex hull S) = \<Union> {convex hull (S - {a}) | a. a \<in> S}"
  3.2526 +proof (cases "affine_dependent S")
  3.2527 +  case True
  3.2528 +    have [iff]: "finite S"
  3.2529 +      using assms using card_infinite by force
  3.2530 +    then have ccs: "closed (convex hull S)"
  3.2531 +      by (simp add: compact_imp_closed finite_imp_compact_convex_hull)
  3.2532 +    { fix x T
  3.2533 +      assume "finite T" "T \<subseteq> S" "int (card T) \<le> aff_dim S + 1" "x \<in> convex hull T"
  3.2534 +      then have "S \<noteq> T"
  3.2535 +        using True \<open>finite S\<close> aff_dim_le_card affine_independent_iff_card by fastforce
  3.2536 +      then obtain a where "a \<in> S" "a \<notin> T"
  3.2537 +        using \<open>T \<subseteq> S\<close> by blast
  3.2538 +      then have "x \<in> (\<Union>a\<in>S. convex hull (S - {a}))"
  3.2539 +        using True affine_independent_iff_card [of S]
  3.2540 +        apply simp
  3.2541 +        apply (metis (no_types, hide_lams) Diff_eq_empty_iff Diff_insert0 `a \<notin> T` `T \<subseteq> S` `x \<in> convex hull T`  hull_mono insert_Diff_single   subsetCE)
  3.2542 +        done
  3.2543 +    } note * = this
  3.2544 +    have 1: "convex hull S \<subseteq> (\<Union> a\<in>S. convex hull (S - {a}))"
  3.2545 +      apply (subst caratheodory_aff_dim)
  3.2546 +      apply (blast intro: *)
  3.2547 +      done
  3.2548 +    have 2: "\<Union>((\<lambda>a. convex hull (S - {a})) ` S) \<subseteq> convex hull S"
  3.2549 +      by (rule Union_least) (metis (no_types, lifting)  Diff_subset hull_mono imageE)
  3.2550 +    show ?thesis using True
  3.2551 +      apply (simp add: segment_convex_hull frontier_def)
  3.2552 +      using interior_convex_hull_eq_empty [OF assms]
  3.2553 +      apply (simp add: closure_closed [OF ccs])
  3.2554 +      apply (rule subset_antisym)
  3.2555 +      using 1 apply blast
  3.2556 +      using 2 apply blast
  3.2557 +      done
  3.2558 +next
  3.2559 +  case False
  3.2560 +  then have "frontier (convex hull S) = (convex hull S) - rel_interior(convex hull S)"
  3.2561 +    apply (simp add: rel_boundary_of_convex_hull [symmetric] frontier_def)
  3.2562 +    by (metis aff_independent_finite assms closure_convex_hull finite_imp_compact_convex_hull hull_hull interior_convex_hull_eq_empty rel_interior_nonempty_interior)
  3.2563 +  also have "... = \<Union>{convex hull (S - {a}) |a. a \<in> S}"
  3.2564 +  proof -
  3.2565 +    have "convex hull S - rel_interior (convex hull S) = rel_frontier (convex hull S)"
  3.2566 +      by (simp add: False aff_independent_finite polyhedron_convex_hull rel_boundary_of_polyhedron rel_frontier_of_polyhedron)
  3.2567 +    then show ?thesis
  3.2568 +      by (simp add: False rel_frontier_convex_hull_cases)
  3.2569 +  qed
  3.2570 +  finally show ?thesis .
  3.2571 +qed
  3.2572 +
  3.2573 +subsection\<open>Special case of a triangle\<close>
  3.2574 +
  3.2575 +proposition frontier_of_triangle:
  3.2576 +    fixes a :: "'a::euclidean_space"
  3.2577 +    assumes "DIM('a) = 2"
  3.2578 +    shows "frontier(convex hull {a,b,c}) = closed_segment a b \<union> closed_segment b c \<union> closed_segment c a"
  3.2579 +          (is "?lhs = ?rhs")
  3.2580 +proof (cases "b = a \<or> c = a \<or> c = b")
  3.2581 +  case True then show ?thesis
  3.2582 +    by (auto simp: assms segment_convex_hull frontier_def empty_interior_convex_hull insert_commute card_insert_le_m1 hull_inc insert_absorb)
  3.2583 +next
  3.2584 +  case False then have [simp]: "card {a, b, c} = Suc (DIM('a))"
  3.2585 +    by (simp add: card_insert Set.insert_Diff_if assms)
  3.2586 +  show ?thesis
  3.2587 +  proof
  3.2588 +    show "?lhs \<subseteq> ?rhs"
  3.2589 +      using False
  3.2590 +      by (force simp: segment_convex_hull frontier_of_convex_hull insert_Diff_if insert_commute split: if_split_asm)
  3.2591 +    show "?rhs \<subseteq> ?lhs"
  3.2592 +      using False
  3.2593 +      apply (simp add: frontier_of_convex_hull segment_convex_hull)
  3.2594 +      apply (intro conjI subsetI)
  3.2595 +        apply (rule_tac X="convex hull {a,b}" in UnionI; force simp: Set.insert_Diff_if)
  3.2596 +       apply (rule_tac X="convex hull {b,c}" in UnionI; force)
  3.2597 +      apply (rule_tac X="convex hull {a,c}" in UnionI; force simp: insert_commute Set.insert_Diff_if)
  3.2598 +      done
  3.2599 +  qed
  3.2600 +qed
  3.2601 +
  3.2602 +corollary inside_of_triangle:
  3.2603 +    fixes a :: "'a::euclidean_space"
  3.2604 +    assumes "DIM('a) = 2"
  3.2605 +    shows "inside (closed_segment a b \<union> closed_segment b c \<union> closed_segment c a) = interior(convex hull {a,b,c})"
  3.2606 +by (metis assms frontier_of_triangle bounded_empty bounded_insert convex_convex_hull inside_frontier_eq_interior bounded_convex_hull)
  3.2607 +
  3.2608 +corollary interior_of_triangle:
  3.2609 +    fixes a :: "'a::euclidean_space"
  3.2610 +    assumes "DIM('a) = 2"
  3.2611 +    shows "interior(convex hull {a,b,c}) =
  3.2612 +           convex hull {a,b,c} - (closed_segment a b \<union> closed_segment b c \<union> closed_segment c a)"
  3.2613 +  using interior_subset
  3.2614 +  by (force simp: frontier_of_triangle [OF assms, symmetric] frontier_def Diff_Diff_Int)
  3.2615 +
  3.2616 +end
     4.1 --- a/src/HOL/ROOT	Tue May 10 11:56:23 2016 +0100
     4.2 +++ b/src/HOL/ROOT	Tue May 10 14:04:44 2016 +0100
     4.3 @@ -720,6 +720,7 @@
     4.4      Multivariate_Analysis
     4.5      Determinants
     4.6      PolyRoots
     4.7 +    Polytope
     4.8      Complex_Analysis_Basics
     4.9      Complex_Transcendental
    4.10      Cauchy_Integral_Thm