section ‹Faces, Extreme Points, Polytopes, Polyhedra etc› text‹Ported from HOL Light by L C Paulson› theory Polytope imports Cartesian_Euclidean_Space begin subsection ‹Faces of a (usually convex) set› definition face_of :: "['a::real_vector set, 'a set] ⇒ bool" (infixr "(face'_of)" 50) where "T face_of S ⟷ T ⊆ S ∧ convex T ∧ (∀a ∈ S. ∀b ∈ S. ∀x ∈ T. x ∈ open_segment a b ⟶ a ∈ T ∧ b ∈ T)" lemma face_ofD: "⟦T face_of S; x ∈ open_segment a b; a ∈ S; b ∈ S; x ∈ T⟧ ⟹ a ∈ T ∧ b ∈ T" unfolding face_of_def by blast lemma face_of_translation_eq [simp]: "((+) a ` T face_of (+) a ` S) ⟷ T face_of S" proof - have *: "⋀a T S. T face_of S ⟹ ((+) a ` T face_of (+) a ` S)" apply (simp add: face_of_def Ball_def, clarify) apply (drule open_segment_translation_eq [THEN iffD1]) using inj_image_mem_iff inj_add_left apply metis done show ?thesis apply (rule iffI) apply (force simp: image_comp o_def dest: * [where a = "-a"]) apply (blast intro: *) done qed lemma face_of_linear_image: assumes "linear f" "inj f" shows "(f ` c face_of f ` S) ⟷ c face_of S" by (simp add: face_of_def inj_image_subset_iff inj_image_mem_iff open_segment_linear_image assms) lemma face_of_refl: "convex S ⟹ S face_of S" by (auto simp: face_of_def) lemma face_of_refl_eq: "S face_of S ⟷ convex S" by (auto simp: face_of_def) lemma empty_face_of [iff]: "{} face_of S" by (simp add: face_of_def) lemma face_of_empty [simp]: "S face_of {} ⟷ S = {}" by (meson empty_face_of face_of_def subset_empty) lemma face_of_trans [trans]: "⟦S face_of T; T face_of u⟧ ⟹ S face_of u" unfolding face_of_def by (safe; blast) lemma face_of_face: "T face_of S ⟹ (f face_of T ⟷ f face_of S ∧ f ⊆ T)" unfolding face_of_def by (safe; blast) lemma face_of_subset: "⟦F face_of S; F ⊆ T; T ⊆ S⟧ ⟹ F face_of T" unfolding face_of_def by (safe; blast) lemma face_of_slice: "⟦F face_of S; convex T⟧ ⟹ (F ∩ T) face_of (S ∩ T)" unfolding face_of_def by (blast intro: convex_Int) lemma face_of_Int: "⟦t1 face_of S; t2 face_of S⟧ ⟹ (t1 ∩ t2) face_of S" unfolding face_of_def by (blast intro: convex_Int) lemma face_of_Inter: "⟦A ≠ {}; ⋀T. T ∈ A ⟹ T face_of S⟧ ⟹ (⋂ A) face_of S" unfolding face_of_def by (blast intro: convex_Inter) lemma face_of_Int_Int: "⟦F face_of T; F' face_of t'⟧ ⟹ (F ∩ F') face_of (T ∩ t')" unfolding face_of_def by (blast intro: convex_Int) lemma face_of_imp_subset: "T face_of S ⟹ T ⊆ S" unfolding face_of_def by blast lemma face_of_imp_eq_affine_Int: fixes S :: "'a::euclidean_space set" assumes S: "convex S" and T: "T face_of S" shows "T = (affine hull T) ∩ S" proof - have "convex T" using T by (simp add: face_of_def) have *: False if x: "x ∈ affine hull T" and "x ∈ S" "x ∉ T" and y: "y ∈ rel_interior T" for x y proof - obtain e where "e>0" and e: "cball y e ∩ affine hull T ⊆ T" using y by (auto simp: rel_interior_cball) have "y ≠ x" "y ∈ S" "y ∈ T" using face_of_imp_subset rel_interior_subset T that by blast+ then have zne: "⋀u. ⟦u ∈ {0<..<1}; (1 - u) *⇩_{R}y + u *⇩_{R}x ∈ T⟧ ⟹ False" using ‹x ∈ S› ‹x ∉ T› ‹T face_of S› unfolding face_of_def apply clarify apply (drule_tac x=x in bspec, assumption) apply (drule_tac x=y in bspec, assumption) apply (subst (asm) open_segment_commute) apply (force simp: open_segment_image_interval image_def) done have in01: "min (1/2) (e / norm (x - y)) ∈ {0<..<1}" using ‹y ≠ x› ‹e > 0› by simp show ?thesis apply (rule zne [OF in01]) apply (rule e [THEN subsetD]) apply (rule IntI) using ‹y ≠ x› ‹e > 0› apply (simp add: cball_def dist_norm algebra_simps) apply (simp add: Real_Vector_Spaces.scaleR_diff_right [symmetric] norm_minus_commute min_mult_distrib_right) apply (rule mem_affine [OF affine_affine_hull _ x]) using ‹y ∈ T› apply (auto simp: hull_inc) done qed show ?thesis apply (rule subset_antisym) using assms apply (simp add: hull_subset face_of_imp_subset) apply (cases "T={}", simp) apply (force simp: rel_interior_eq_empty [symmetric] ‹convex T› intro: *) done qed lemma face_of_imp_closed: fixes S :: "'a::euclidean_space set" assumes "convex S" "closed S" "T face_of S" shows "closed T" by (metis affine_affine_hull affine_closed closed_Int face_of_imp_eq_affine_Int assms) lemma face_of_Int_supporting_hyperplane_le_strong: assumes "convex(S ∩ {x. a ∙ x = b})" and aleb: "⋀x. x ∈ S ⟹ a ∙ x ≤ b" shows "(S ∩ {x. a ∙ x = b}) face_of S" proof - have *: "a ∙ u = a ∙ x" if "x ∈ open_segment u v" "u ∈ S" "v ∈ S" and b: "b = a ∙ x" for u v x proof (rule antisym) show "a ∙ u ≤ a ∙ x" using aleb ‹u ∈ S› ‹b = a ∙ x› by blast next obtain ξ where "b = a ∙ ((1 - ξ) *⇩_{R}u + ξ *⇩_{R}v)" "0 < ξ" "ξ < 1" using ‹b = a ∙ x› ‹x ∈ open_segment u v› in_segment by (auto simp: open_segment_image_interval split: if_split_asm) then have "b + ξ * (a ∙ u) ≤ a ∙ u + ξ * b" using aleb [OF ‹v ∈ S›] by (simp add: algebra_simps) then have "(1 - ξ) * b ≤ (1 - ξ) * (a ∙ u)" by (simp add: algebra_simps) then have "b ≤ a ∙ u" using ‹ξ < 1› by auto with b show "a ∙ x ≤ a ∙ u" by simp qed show ?thesis apply (simp add: face_of_def assms) using "*" open_segment_commute by blast qed lemma face_of_Int_supporting_hyperplane_ge_strong: "⟦convex(S ∩ {x. a ∙ x = b}); ⋀x. x ∈ S ⟹ a ∙ x ≥ b⟧ ⟹ (S ∩ {x. a ∙ x = b}) face_of S" using face_of_Int_supporting_hyperplane_le_strong [of S "-a" "-b"] by simp lemma face_of_Int_supporting_hyperplane_le: "⟦convex S; ⋀x. x ∈ S ⟹ a ∙ x ≤ b⟧ ⟹ (S ∩ {x. a ∙ x = b}) face_of S" by (simp add: convex_Int convex_hyperplane face_of_Int_supporting_hyperplane_le_strong) lemma face_of_Int_supporting_hyperplane_ge: "⟦convex S; ⋀x. x ∈ S ⟹ a ∙ x ≥ b⟧ ⟹ (S ∩ {x. a ∙ x = b}) face_of S" by (simp add: convex_Int convex_hyperplane face_of_Int_supporting_hyperplane_ge_strong) lemma face_of_imp_convex: "T face_of S ⟹ convex T" using face_of_def by blast lemma face_of_imp_compact: fixes S :: "'a::euclidean_space set" shows "⟦convex S; compact S; T face_of S⟧ ⟹ compact T" by (meson bounded_subset compact_eq_bounded_closed face_of_imp_closed face_of_imp_subset) lemma face_of_Int_subface: "⟦A ∩ B face_of A; A ∩ B face_of B; C face_of A; D face_of B⟧ ⟹ (C ∩ D) face_of C ∧ (C ∩ D) face_of D" by (meson face_of_Int_Int face_of_face inf_le1 inf_le2) lemma subset_of_face_of: fixes S :: "'a::real_normed_vector set" assumes "T face_of S" "u ⊆ S" "T ∩ (rel_interior u) ≠ {}" shows "u ⊆ T" proof fix c assume "c ∈ u" obtain b where "b ∈ T" "b ∈ rel_interior u" using assms by auto then obtain e where "e>0" "b ∈ u" and e: "cball b e ∩ affine hull u ⊆ u" by (auto simp: rel_interior_cball) show "c ∈ T" proof (cases "b=c") case True with ‹b ∈ T› show ?thesis by blast next case False define d where "d = b + (e / norm(b - c)) *⇩_{R}(b - c)" have "d ∈ cball b e ∩ affine hull u" using ‹e > 0› ‹b ∈ u› ‹c ∈ u› by (simp add: d_def dist_norm hull_inc mem_affine_3_minus False) with e have "d ∈ u" by blast have nbc: "norm (b - c) + e > 0" using ‹e > 0› by (metis add.commute le_less_trans less_add_same_cancel2 norm_ge_zero) then have [simp]: "d ≠ c" using False scaleR_cancel_left [of "1 + (e / norm (b - c))" b c] by (simp add: algebra_simps d_def) (simp add: divide_simps) have [simp]: "((e - e * e / (e + norm (b - c))) / norm (b - c)) = (e / (e + norm (b - c)))" using False nbc by (simp add: divide_simps) (simp add: algebra_simps) have "b ∈ open_segment d c" apply (simp add: open_segment_image_interval) apply (simp add: d_def algebra_simps image_def) apply (rule_tac x="e / (e + norm (b - c))" in bexI) using False nbc ‹0 < e› apply (auto simp: algebra_simps) done then have "d ∈ T ∧ c ∈ T" apply (rule face_ofD [OF ‹T face_of S›]) using ‹d ∈ u› ‹c ∈ u› ‹u ⊆ S› ‹b ∈ T› apply auto done then show ?thesis .. qed qed lemma face_of_eq: fixes S :: "'a::real_normed_vector set" assumes "T face_of S" "u face_of S" "(rel_interior T) ∩ (rel_interior u) ≠ {}" shows "T = u" apply (rule subset_antisym) apply (metis assms disjoint_iff_not_equal face_of_imp_subset rel_interior_subset subsetCE subset_of_face_of) by (metis assms disjoint_iff_not_equal face_of_imp_subset rel_interior_subset subset_iff subset_of_face_of) lemma face_of_disjoint_rel_interior: fixes S :: "'a::real_normed_vector set" assumes "T face_of S" "T ≠ S" shows "T ∩ rel_interior S = {}" by (meson assms subset_of_face_of face_of_imp_subset order_refl subset_antisym) lemma face_of_disjoint_interior: fixes S :: "'a::real_normed_vector set" assumes "T face_of S" "T ≠ S" shows "T ∩ interior S = {}" proof - have "T ∩ interior S ⊆ rel_interior S" by (meson inf_sup_ord(2) interior_subset_rel_interior order.trans) thus ?thesis by (metis (no_types) Int_greatest assms face_of_disjoint_rel_interior inf_sup_ord(1) subset_empty) qed lemma face_of_subset_rel_boundary: fixes S :: "'a::real_normed_vector set" assumes "T face_of S" "T ≠ S" shows "T ⊆ (S - rel_interior S)" by (meson DiffI assms disjoint_iff_not_equal face_of_disjoint_rel_interior face_of_imp_subset rev_subsetD subsetI) lemma face_of_subset_rel_frontier: fixes S :: "'a::real_normed_vector set" assumes "T face_of S" "T ≠ S" shows "T ⊆ rel_frontier S" using assms closure_subset face_of_disjoint_rel_interior face_of_imp_subset rel_frontier_def by fastforce lemma face_of_aff_dim_lt: fixes S :: "'a::euclidean_space set" assumes "convex S" "T face_of S" "T ≠ S" shows "aff_dim T < aff_dim S" proof - have "aff_dim T ≤ aff_dim S" by (simp add: face_of_imp_subset aff_dim_subset assms) moreover have "aff_dim T ≠ aff_dim S" proof (cases "T = {}") case True then show ?thesis by (metis aff_dim_empty ‹T ≠ S›) next case False then show ?thesis 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) qed ultimately show ?thesis by simp qed lemma subset_of_face_of_affine_hull: fixes S :: "'a::euclidean_space set" assumes T: "T face_of S" and "convex S" "U ⊆ S" and dis: "~disjnt (affine hull T) (rel_interior U)" shows "U ⊆ T" apply (rule subset_of_face_of [OF T ‹U ⊆ S›]) using face_of_imp_eq_affine_Int [OF ‹convex S› T] using rel_interior_subset [of U] dis using ‹U ⊆ S› disjnt_def by fastforce lemma affine_hull_face_of_disjoint_rel_interior: fixes S :: "'a::euclidean_space set" assumes "convex S" "F face_of S" "F ≠ S" shows "affine hull F ∩ rel_interior S = {}" by (metis assms disjnt_def face_of_imp_subset order_refl subset_antisym subset_of_face_of_affine_hull) lemma affine_diff_divide: assumes "affine S" "k ≠ 0" "k ≠ 1" and xy: "x ∈ S" "y /⇩_{R}(1 - k) ∈ S" shows "(x - y) /⇩_{R}k ∈ S" proof - have "inverse(k) *⇩_{R}(x - y) = (1 - inverse k) *⇩_{R}inverse(1 - k) *⇩_{R}y + inverse(k) *⇩_{R}x" using assms by (simp add: algebra_simps) (simp add: scaleR_left_distrib [symmetric] divide_simps) then show ?thesis using ‹affine S› xy by (auto simp: affine_alt) qed lemma face_of_convex_hulls: assumes S: "finite S" "T ⊆ S" and disj: "affine hull T ∩ convex hull (S - T) = {}" shows "(convex hull T) face_of (convex hull S)" proof - have fin: "finite T" "finite (S - T)" using assms by (auto simp: finite_subset) have *: "x ∈ convex hull T" if x: "x ∈ convex hull S" and y: "y ∈ convex hull S" and w: "w ∈ convex hull T" "w ∈ open_segment x y" for x y w proof - have waff: "w ∈ affine hull T" using convex_hull_subset_affine_hull w by blast obtain a b where a: "⋀i. i ∈ S ⟹ 0 ≤ a i" and asum: "sum a S = 1" and aeqx: "(∑i∈S. a i *⇩_{R}i) = x" and b: "⋀i. i ∈ S ⟹ 0 ≤ b i" and bsum: "sum b S = 1" and beqy: "(∑i∈S. b i *⇩_{R}i) = y" using x y by (auto simp: assms convex_hull_finite) obtain u where "(1 - u) *⇩_{R}x + u *⇩_{R}y ∈ convex hull T" "x ≠ y" and weq: "w = (1 - u) *⇩_{R}x + u *⇩_{R}y" and u01: "0 < u" "u < 1" using w by (auto simp: open_segment_image_interval split: if_split_asm) define c where "c i = (1 - u) * a i + u * b i" for i have cge0: "⋀i. i ∈ S ⟹ 0 ≤ c i" using a b u01 by (simp add: c_def) have sumc1: "sum c S = 1" by (simp add: c_def sum.distrib sum_distrib_left [symmetric] asum bsum) have sumci_xy: "(∑i∈S. c i *⇩_{R}i) = (1 - u) *⇩_{R}x + u *⇩_{R}y" apply (simp add: c_def sum.distrib scaleR_left_distrib) by (simp only: scaleR_scaleR [symmetric] Real_Vector_Spaces.scaleR_right.sum [symmetric] aeqx beqy) show ?thesis proof (cases "sum c (S - T) = 0") case True have ci0: "⋀i. i ∈ (S - T) ⟹ c i = 0" using True cge0 fin(2) sum_nonneg_eq_0_iff by auto have a0: "a i = 0" if "i ∈ (S - T)" for i using ci0 [OF that] u01 a [of i] b [of i] that by (simp add: c_def Groups.ordered_comm_monoid_add_class.add_nonneg_eq_0_iff) have [simp]: "sum a T = 1" using assms by (metis sum.mono_neutral_cong_right a0 asum) show ?thesis apply (simp add: convex_hull_finite ‹finite T›) apply (rule_tac x=a in exI) using a0 assms apply (auto simp: cge0 a aeqx [symmetric] sum.mono_neutral_right) done next case False define k where "k = sum c (S - T)" have "k > 0" using False unfolding k_def by (metis DiffD1 antisym_conv cge0 sum_nonneg not_less) have weq_sumsum: "w = sum (λx. c x *⇩_{R}x) T + sum (λx. c x *⇩_{R}x) (S - T)" by (metis (no_types) add.commute S(1) S(2) sum.subset_diff sumci_xy weq) show ?thesis proof (cases "k = 1") case True then have "sum c T = 0" by (simp add: S k_def sum_diff sumc1) then have [simp]: "sum c (S - T) = 1" by (simp add: S sum_diff sumc1) have ci0: "⋀i. i ∈ T ⟹ c i = 0" by (meson ‹finite T› ‹sum c T = 0› ‹T ⊆ S› cge0 sum_nonneg_eq_0_iff subsetCE) then have [simp]: "(∑i∈S-T. c i *⇩_{R}i) = w" by (simp add: weq_sumsum) have "w ∈ convex hull (S - T)" apply (simp add: convex_hull_finite fin) apply (rule_tac x=c in exI) apply (auto simp: cge0 weq True k_def) done then show ?thesis using disj waff by blast next case False then have sumcf: "sum c T = 1 - k" by (simp add: S k_def sum_diff sumc1) have "(∑i∈T. c i *⇩_{R}i) /⇩_{R}(1 - k) ∈ convex hull T" apply (simp add: convex_hull_finite fin) apply (rule_tac x="λi. inverse (1-k) * c i" in exI) apply auto apply (metis sumcf cge0 inverse_nonnegative_iff_nonnegative mult_nonneg_nonneg S(2) sum_nonneg subsetCE) apply (metis False mult.commute right_inverse right_minus_eq sum_distrib_left sumcf) by (metis (mono_tags, lifting) scaleR_right.sum scaleR_scaleR sum.cong) with ‹0 < k› have "inverse(k) *⇩_{R}(w - sum (λi. c i *⇩_{R}i) T) ∈ affine hull T" by (simp add: affine_diff_divide [OF affine_affine_hull] False waff convex_hull_subset_affine_hull [THEN subsetD]) moreover have "inverse(k) *⇩_{R}(w - sum (λx. c x *⇩_{R}x) T) ∈ convex hull (S - T)" apply (simp add: weq_sumsum convex_hull_finite fin) apply (rule_tac x="λi. inverse k * c i" in exI) using ‹k > 0› cge0 apply (auto simp: scaleR_right.sum sum_distrib_left [symmetric] k_def [symmetric]) done ultimately show ?thesis using disj by blast qed qed qed have [simp]: "convex hull T ⊆ convex hull S" by (simp add: ‹T ⊆ S› hull_mono) show ?thesis using open_segment_commute by (auto simp: face_of_def intro: *) qed proposition face_of_convex_hull_insert: "⟦finite S; a ∉ affine hull S; T face_of convex hull S⟧ ⟹ T face_of convex hull insert a S" apply (rule face_of_trans, blast) apply (rule face_of_convex_hulls; force simp: insert_Diff_if) done proposition face_of_affine_trivial: assumes "affine S" "T face_of S" shows "T = {} ∨ T = S" proof (rule ccontr, clarsimp) assume "T ≠ {}" "T ≠ S" then obtain a where "a ∈ T" by auto then have "a ∈ S" using ‹T face_of S› face_of_imp_subset by blast have "S ⊆ T" proof fix b assume "b ∈ S" show "b ∈ T" proof (cases "a = b") case True with ‹a ∈ T› show ?thesis by auto next case False then have "a ∈ open_segment (2 *⇩_{R}a - b) b" apply (auto simp: open_segment_def closed_segment_def) apply (rule_tac x="1/2" in exI) apply (simp add: algebra_simps) by (simp add: scaleR_2) moreover have "2 *⇩_{R}a - b ∈ S" by (rule mem_affine [OF ‹affine S› ‹a ∈ S› ‹b ∈ S›, of 2 "-1", simplified]) moreover note ‹b ∈ S› ‹a ∈ T› ultimately show ?thesis by (rule face_ofD [OF ‹T face_of S›, THEN conjunct2]) qed qed then show False using ‹T ≠ S› ‹T face_of S› face_of_imp_subset by blast qed lemma face_of_affine_eq: "affine S ⟹ (T face_of S ⟷ T = {} ∨ T = S)" using affine_imp_convex face_of_affine_trivial face_of_refl by auto lemma Inter_faces_finite_altbound: fixes T :: "'a::euclidean_space set set" assumes cfaI: "⋀c. c ∈ T ⟹ c face_of S" shows "∃F'. finite F' ∧ F' ⊆ T ∧ card F' ≤ DIM('a) + 2 ∧ ⋂F' = ⋂T" proof (cases "∀F'. finite F' ∧ F' ⊆ T ∧ card F' ≤ DIM('a) + 2 ⟶ (∃c. c ∈ T ∧ c ∩ (⋂F') ⊂ (⋂F'))") case True then obtain c where c: "⋀F'. ⟦finite F'; F' ⊆ T; card F' ≤ DIM('a) + 2⟧ ⟹ c F' ∈ T ∧ c F' ∩ (⋂F') ⊂ (⋂F')" by metis define d where "d = rec_nat {c{}} (λn r. insert (c r) r)" have [simp]: "d 0 = {c {}}" by (simp add: d_def) have dSuc [simp]: "⋀n. d (Suc n) = insert (c (d n)) (d n)" by (simp add: d_def) have dn_notempty: "d n ≠ {}" for n by (induction n) auto have dn_le_Suc: "d n ⊆ T ∧ finite(d n) ∧ card(d n) ≤ Suc n" if "n ≤ DIM('a) + 2" for n using that proof (induction n) case 0 then show ?case by (simp add: c) next case (Suc n) then show ?case by (auto simp: c card_insert_if) qed have aff_dim_le: "aff_dim(⋂(d n)) ≤ DIM('a) - int n" if "n ≤ DIM('a) + 2" for n using that proof (induction n) case 0 then show ?case by (simp add: aff_dim_le_DIM) next case (Suc n) have fs: "⋂d (Suc n) face_of S" by (meson Suc.prems cfaI dn_le_Suc dn_notempty face_of_Inter subsetCE) have condn: "convex (⋂d n)" using Suc.prems nat_le_linear not_less_eq_eq by (blast intro: face_of_imp_convex cfaI convex_Inter dest: dn_le_Suc) have fdn: "⋂d (Suc n) face_of ⋂d n" 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) have ne: "⋂d (Suc n) ≠ ⋂d n" by (metis (no_types, lifting) Suc.prems Suc_leD c complete_lattice_class.Inf_insert dSuc dn_le_Suc less_irrefl order.trans) have *: "⋀m::int. ⋀d. ⋀d'::int. d < d' ∧ d' ≤ m - n ⟹ d ≤ m - of_nat(n+1)" by arith have "aff_dim (⋂d (Suc n)) < aff_dim (⋂d n)" by (rule face_of_aff_dim_lt [OF condn fdn ne]) moreover have "aff_dim (⋂d n) ≤ int (DIM('a)) - int n" using Suc by auto ultimately have "aff_dim (⋂d (Suc n)) ≤ int (DIM('a)) - (n+1)" by arith then show ?case by linarith qed have "aff_dim (⋂d (DIM('a) + 2)) ≤ -2" using aff_dim_le [OF order_refl] by simp with aff_dim_geq [of "⋂d (DIM('a) + 2)"] show ?thesis using order.trans by fastforce next case False then show ?thesis apply simp apply (erule ex_forward) by blast qed lemma faces_of_translation: "{F. F face_of image (λx. a + x) S} = image (image (λx. a + x)) {F. F face_of S}" apply (rule subset_antisym, clarify) apply (auto simp: image_iff) apply (metis face_of_imp_subset face_of_translation_eq subset_imageE) done proposition face_of_Times: assumes "F face_of S" and "F' face_of S'" shows "(F × F') face_of (S × S')" proof - have "F × F' ⊆ S × S'" using assms [unfolded face_of_def] by blast moreover have "convex (F × F')" using assms [unfolded face_of_def] by (blast intro: convex_Times) moreover have "a ∈ F ∧ a' ∈ F' ∧ b ∈ F ∧ b' ∈ F'" if "a ∈ S" "b ∈ S" "a' ∈ S'" "b' ∈ S'" "x ∈ F × F'" "x ∈ open_segment (a,a') (b,b')" for a b a' b' x proof (cases "b=a ∨ b'=a'") case True with that show ?thesis using assms by (force simp: in_segment dest: face_ofD) next case False with assms [unfolded face_of_def] that show ?thesis by (blast dest!: open_segment_PairD) qed ultimately show ?thesis unfolding face_of_def by blast qed corollary face_of_Times_decomp: fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set" shows "c face_of (S × S') ⟷ (∃F F'. F face_of S ∧ F' face_of S' ∧ c = F × F')" (is "?lhs = ?rhs") proof assume c: ?lhs show ?rhs proof (cases "c = {}") case True then show ?thesis by auto next case False have 1: "fst ` c ⊆ S" "snd ` c ⊆ S'" using c face_of_imp_subset by fastforce+ have "convex c" using c by (metis face_of_imp_convex) have conv: "convex (fst ` c)" "convex (snd ` c)" by (simp_all add: ‹convex c› convex_linear_image fst_linear snd_linear) have fstab: "a ∈ fst ` c ∧ b ∈ fst ` c" if "a ∈ S" "b ∈ S" "x ∈ open_segment a b" "(x,x') ∈ c" for a b x x' proof - have *: "(x,x') ∈ open_segment (a,x') (b,x')" using that by (auto simp: in_segment) show ?thesis using face_ofD [OF c *] that face_of_imp_subset [OF c] by force qed have fst: "fst ` c face_of S" by (force simp: face_of_def 1 conv fstab) have sndab: "a' ∈ snd ` c ∧ b' ∈ snd ` c" if "a' ∈ S'" "b' ∈ S'" "x' ∈ open_segment a' b'" "(x,x') ∈ c" for a' b' x x' proof - have *: "(x,x') ∈ open_segment (x,a') (x,b')" using that by (auto simp: in_segment) show ?thesis using face_ofD [OF c *] that face_of_imp_subset [OF c] by force qed have snd: "snd ` c face_of S'" by (force simp: face_of_def 1 conv sndab) have cc: "rel_interior c ⊆ rel_interior (fst ` c) × rel_interior (snd ` c)" by (force simp: face_of_Times rel_interior_Times conv fst snd ‹convex c› fst_linear snd_linear rel_interior_convex_linear_image [symmetric]) have "c = fst ` c × snd ` c" apply (rule face_of_eq [OF c]) apply (simp_all add: face_of_Times rel_interior_Times conv fst snd) using False rel_interior_eq_empty ‹convex c› cc apply blast done with fst snd show ?thesis by metis qed next assume ?rhs with face_of_Times show ?lhs by auto qed lemma face_of_Times_eq: fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set" shows "(F × F') face_of (S × S') ⟷ F = {} ∨ F' = {} ∨ F face_of S ∧ F' face_of S'" by (auto simp: face_of_Times_decomp times_eq_iff) lemma hyperplane_face_of_halfspace_le: "{x. a ∙ x = b} face_of {x. a ∙ x ≤ b}" proof - have "{x. a ∙ x ≤ b} ∩ {x. a ∙ x = b} = {x. a ∙ x = b}" by auto with face_of_Int_supporting_hyperplane_le [OF convex_halfspace_le [of a b], of a b] show ?thesis by auto qed lemma hyperplane_face_of_halfspace_ge: "{x. a ∙ x = b} face_of {x. a ∙ x ≥ b}" proof - have "{x. a ∙ x ≥ b} ∩ {x. a ∙ x = b} = {x. a ∙ x = b}" by auto with face_of_Int_supporting_hyperplane_ge [OF convex_halfspace_ge [of b a], of b a] show ?thesis by auto qed lemma face_of_halfspace_le: fixes a :: "'n::euclidean_space" shows "F face_of {x. a ∙ x ≤ b} ⟷ F = {} ∨ F = {x. a ∙ x = b} ∨ F = {x. a ∙ x ≤ b}" (is "?lhs = ?rhs") proof (cases "a = 0") case True then show ?thesis using face_of_affine_eq affine_UNIV by auto next case False then have ine: "interior {x. a ∙ x ≤ b} ≠ {}" using halfspace_eq_empty_lt interior_halfspace_le by blast show ?thesis proof assume L: ?lhs have "F ≠ {x. a ∙ x ≤ b} ⟹ F face_of {x. a ∙ x = b}" using False apply (simp add: frontier_halfspace_le [symmetric] rel_frontier_nonempty_interior [OF ine, symmetric]) apply (rule face_of_subset [OF L]) apply (simp add: face_of_subset_rel_frontier [OF L]) apply (force simp: rel_frontier_def closed_halfspace_le) done with L show ?rhs using affine_hyperplane face_of_affine_eq by blast next assume ?rhs then show ?lhs by (metis convex_halfspace_le empty_face_of face_of_refl hyperplane_face_of_halfspace_le) qed qed lemma face_of_halfspace_ge: fixes a :: "'n::euclidean_space" shows "F face_of {x. a ∙ x ≥ b} ⟷ F = {} ∨ F = {x. a ∙ x = b} ∨ F = {x. a ∙ x ≥ b}" using face_of_halfspace_le [of F "-a" "-b"] by simp subsection‹Exposed faces› text‹That is, faces that are intersection with supporting hyperplane› definition exposed_face_of :: "['a::euclidean_space set, 'a set] ⇒ bool" (infixr "(exposed'_face'_of)" 50) where "T exposed_face_of S ⟷ T face_of S ∧ (∃a b. S ⊆ {x. a ∙ x ≤ b} ∧ T = S ∩ {x. a ∙ x = b})" lemma empty_exposed_face_of [iff]: "{} exposed_face_of S" apply (simp add: exposed_face_of_def) apply (rule_tac x=0 in exI) apply (rule_tac x=1 in exI, force) done lemma exposed_face_of_refl_eq [simp]: "S exposed_face_of S ⟷ convex S" apply (simp add: exposed_face_of_def face_of_refl_eq, auto) apply (rule_tac x=0 in exI)+ apply force done lemma exposed_face_of_refl: "convex S ⟹ S exposed_face_of S" by simp lemma exposed_face_of: "T exposed_face_of S ⟷ T face_of S ∧ (T = {} ∨ T = S ∨ (∃a b. a ≠ 0 ∧ S ⊆ {x. a ∙ x ≤ b} ∧ T = S ∩ {x. a ∙ x = b}))" proof (cases "T = {}") case True then show ?thesis by simp next case False show ?thesis proof (cases "T = S") case True then show ?thesis by (simp add: face_of_refl_eq) next case False with ‹T ≠ {}› show ?thesis apply (auto simp: exposed_face_of_def) apply (metis inner_zero_left) done qed qed lemma exposed_face_of_Int_supporting_hyperplane_le: "⟦convex S; ⋀x. x ∈ S ⟹ a ∙ x ≤ b⟧ ⟹ (S ∩ {x. a ∙ x = b}) exposed_face_of S" by (force simp: exposed_face_of_def face_of_Int_supporting_hyperplane_le) lemma exposed_face_of_Int_supporting_hyperplane_ge: "⟦convex S; ⋀x. x ∈ S ⟹ a ∙ x ≥ b⟧ ⟹ (S ∩ {x. a ∙ x = b}) exposed_face_of S" using exposed_face_of_Int_supporting_hyperplane_le [of S "-a" "-b"] by simp proposition exposed_face_of_Int: assumes "T exposed_face_of S" and "u exposed_face_of S" shows "(T ∩ u) exposed_face_of S" proof - obtain a b where T: "S ∩ {x. a ∙ x = b} face_of S" and S: "S ⊆ {x. a ∙ x ≤ b}" and teq: "T = S ∩ {x. a ∙ x = b}" using assms by (auto simp: exposed_face_of_def) obtain a' b' where u: "S ∩ {x. a' ∙ x = b'} face_of S" and s': "S ⊆ {x. a' ∙ x ≤ b'}" and ueq: "u = S ∩ {x. a' ∙ x = b'}" using assms by (auto simp: exposed_face_of_def) have tu: "T ∩ u face_of S" using T teq u ueq by (simp add: face_of_Int) have ss: "S ⊆ {x. (a + a') ∙ x ≤ b + b'}" using S s' by (force simp: inner_left_distrib) show ?thesis apply (simp add: exposed_face_of_def tu) apply (rule_tac x="a+a'" in exI) apply (rule_tac x="b+b'" in exI) using S s' apply (fastforce simp: ss inner_left_distrib teq ueq) done qed proposition exposed_face_of_Inter: fixes P :: "'a::euclidean_space set set" assumes "P ≠ {}" and "⋀T. T ∈ P ⟹ T exposed_face_of S" shows "⋂P exposed_face_of S" proof - obtain Q where "finite Q" and QsubP: "Q ⊆ P" "card Q ≤ DIM('a) + 2" and IntQ: "⋂Q = ⋂P" using Inter_faces_finite_altbound [of P S] assms [unfolded exposed_face_of] by force show ?thesis proof (cases "Q = {}") case True then show ?thesis by (metis IntQ Inter_UNIV_conv(2) assms(1) assms(2) ex_in_conv) next case False have "Q ⊆ {T. T exposed_face_of S}" using QsubP assms by blast moreover have "Q ⊆ {T. T exposed_face_of S} ⟹ ⋂Q exposed_face_of S" using ‹finite Q› False apply (induction Q rule: finite_induct) using exposed_face_of_Int apply fastforce+ done ultimately show ?thesis by (simp add: IntQ) qed qed proposition exposed_face_of_sums: assumes "convex S" and "convex T" and "F exposed_face_of {x + y | x y. x ∈ S ∧ y ∈ T}" (is "F exposed_face_of ?ST") obtains k l where "k exposed_face_of S" "l exposed_face_of T" "F = {x + y | x y. x ∈ k ∧ y ∈ l}" proof (cases "F = {}") case True then show ?thesis using that by blast next case False show ?thesis proof (cases "F = ?ST") case True then show ?thesis using assms exposed_face_of_refl_eq that by blast next case False obtain p where "p ∈ F" using ‹F ≠ {}› by blast moreover obtain u z where T: "?ST ∩ {x. u ∙ x = z} face_of ?ST" and S: "?ST ⊆ {x. u ∙ x ≤ z}" and feq: "F = ?ST ∩ {x. u ∙ x = z}" using assms by (auto simp: exposed_face_of_def) ultimately obtain a0 b0 where p: "p = a0 + b0" and "a0 ∈ S" "b0 ∈ T" and z: "u ∙ p = z" by auto have lez: "u ∙ (x + y) ≤ z" if "x ∈ S" "y ∈ T" for x y using S that by auto have sef: "S ∩ {x. u ∙ x = u ∙ a0} exposed_face_of S" apply (rule exposed_face_of_Int_supporting_hyperplane_le [OF ‹convex S›]) apply (metis p z add_le_cancel_right inner_right_distrib lez [OF _ ‹b0 ∈ T›]) done have tef: "T ∩ {x. u ∙ x = u ∙ b0} exposed_face_of T" apply (rule exposed_face_of_Int_supporting_hyperplane_le [OF ‹convex T›]) apply (metis p z add.commute add_le_cancel_right inner_right_distrib lez [OF ‹a0 ∈ S›]) done have "{x + y |x y. x ∈ S ∧ u ∙ x = u ∙ a0 ∧ y ∈ T ∧ u ∙ y = u ∙ b0} ⊆ F" by (auto simp: feq) (metis inner_right_distrib p z) moreover have "F ⊆ {x + y |x y. x ∈ S ∧ u ∙ x = u ∙ a0 ∧ y ∈ T ∧ u ∙ y = u ∙ b0}" apply (auto simp: feq) apply (rename_tac x y) apply (rule_tac x=x in exI) apply (rule_tac x=y in exI, simp) using z p ‹a0 ∈ S› ‹b0 ∈ T› apply clarify apply (simp add: inner_right_distrib) apply (metis add_le_cancel_right antisym lez [unfolded inner_right_distrib] add.commute) done ultimately have "F = {x + y |x y. x ∈ S ∩ {x. u ∙ x = u ∙ a0} ∧ y ∈ T ∩ {x. u ∙ x = u ∙ b0}}" by blast then show ?thesis by (rule that [OF sef tef]) qed qed lemma exposed_face_of_parallel: "T exposed_face_of S ⟷ T face_of S ∧ (∃a b. S ⊆ {x. a ∙ x ≤ b} ∧ T = S ∩ {x. a ∙ x = b} ∧ (T ≠ {} ⟶ T ≠ S ⟶ a ≠ 0) ∧ (T ≠ S ⟶ (∀w ∈ affine hull S. (w + a) ∈ affine hull S)))" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs proof (clarsimp simp: exposed_face_of_def) fix a b assume faceS: "S ∩ {x. a ∙ x = b} face_of S" and Ssub: "S ⊆ {x. a ∙ x ≤ b}" show "∃c d. S ⊆ {x. c ∙ x ≤ d} ∧ S ∩ {x. a ∙ x = b} = S ∩ {x. c ∙ x = d} ∧ (S ∩ {x. a ∙ x = b} ≠ {} ⟶ S ∩ {x. a ∙ x = b} ≠ S ⟶ c ≠ 0) ∧ (S ∩ {x. a ∙ x = b} ≠ S ⟶ (∀w ∈ affine hull S. w + c ∈ affine hull S))" proof (cases "affine hull S ∩ {x. -a ∙ x ≤ -b} = {} ∨ affine hull S ⊆ {x. - a ∙ x ≤ - b}") case True then show ?thesis proof assume "affine hull S ∩ {x. - a ∙ x ≤ - b} = {}" then show ?thesis apply (rule_tac x="0" in exI) apply (rule_tac x="1" in exI) using hull_subset by fastforce next assume "affine hull S ⊆ {x. - a ∙ x ≤ - b}" then show ?thesis apply (rule_tac x="0" in exI) apply (rule_tac x="0" in exI) using Ssub hull_subset by fastforce qed next case False then obtain a' b' where "a' ≠ 0" and le: "affine hull S ∩ {x. a' ∙ x ≤ b'} = affine hull S ∩ {x. - a ∙ x ≤ - b}" and eq: "affine hull S ∩ {x. a' ∙ x = b'} = affine hull S ∩ {x. - a ∙ x = - b}" and mem: "⋀w. w ∈ affine hull S ⟹ w + a' ∈ affine hull S" using affine_parallel_slice affine_affine_hull by metis show ?thesis proof (intro conjI impI allI ballI exI) have *: "S ⊆ - (affine hull S ∩ {x. P x}) ∪ affine hull S ∩ {x. Q x} ⟹ S ⊆ {x. ~P x ∨ Q x}" for P Q using hull_subset by fastforce have "S ⊆ {x. ~ (a' ∙ x ≤ b') ∨ a' ∙ x = b'}" apply (rule *) apply (simp only: le eq) using Ssub by auto then show "S ⊆ {x. - a' ∙ x ≤ - b'}" by auto show "S ∩ {x. a ∙ x = b} = S ∩ {x. - a' ∙ x = - b'}" using eq hull_subset [of S affine] by force show "⟦S ∩ {x. a ∙ x = b} ≠ {}; S ∩ {x. a ∙ x = b} ≠ S⟧ ⟹ - a' ≠ 0" using ‹a' ≠ 0› by auto show "w + - a' ∈ affine hull S" if "S ∩ {x. a ∙ x = b} ≠ S" "w ∈ affine hull S" for w proof - have "w + 1 *⇩_{R}(w - (w + a')) ∈ affine hull S" using affine_affine_hull mem mem_affine_3_minus that(2) by blast then show ?thesis by simp qed qed qed qed next assume ?rhs then show ?lhs unfolding exposed_face_of_def by blast qed subsection‹Extreme points of a set: its singleton faces› definition extreme_point_of :: "['a::real_vector, 'a set] ⇒ bool" (infixr "(extreme'_point'_of)" 50) where "x extreme_point_of S ⟷ x ∈ S ∧ (∀a ∈ S. ∀b ∈ S. x ∉ open_segment a b)" lemma extreme_point_of_stillconvex: "convex S ⟹ (x extreme_point_of S ⟷ x ∈ S ∧ convex(S - {x}))" by (fastforce simp add: convex_contains_segment extreme_point_of_def open_segment_def) lemma face_of_singleton: "{x} face_of S ⟷ x extreme_point_of S" by (fastforce simp add: extreme_point_of_def face_of_def) lemma extreme_point_not_in_REL_INTERIOR: fixes S :: "'a::real_normed_vector set" shows "⟦x extreme_point_of S; S ≠ {x}⟧ ⟹ x ∉ rel_interior S" apply (simp add: face_of_singleton [symmetric]) apply (blast dest: face_of_disjoint_rel_interior) done lemma extreme_point_not_in_interior: fixes S :: "'a::{real_normed_vector, perfect_space} set" shows "x extreme_point_of S ⟹ x ∉ interior S" apply (case_tac "S = {x}") apply (simp add: empty_interior_finite) by (meson contra_subsetD extreme_point_not_in_REL_INTERIOR interior_subset_rel_interior) lemma extreme_point_of_face: "F face_of S ⟹ v extreme_point_of F ⟷ v extreme_point_of S ∧ v ∈ F" by (meson empty_subsetI face_of_face face_of_singleton insert_subset) lemma extreme_point_of_convex_hull: "x extreme_point_of (convex hull S) ⟹ x ∈ S" apply (simp add: extreme_point_of_stillconvex) using hull_minimal [of S "(convex hull S) - {x}" convex] using hull_subset [of S convex] apply blast done lemma extreme_points_of_convex_hull: "{x. x extreme_point_of (convex hull S)} ⊆ S" using extreme_point_of_convex_hull by auto lemma extreme_point_of_empty [simp]: "~ (x extreme_point_of {})" by (simp add: extreme_point_of_def) lemma extreme_point_of_singleton [iff]: "x extreme_point_of {a} ⟷ x = a" using extreme_point_of_stillconvex by auto lemma extreme_point_of_translation_eq: "(a + x) extreme_point_of (image (λx. a + x) S) ⟷ x extreme_point_of S" by (auto simp: extreme_point_of_def) lemma extreme_points_of_translation: "{x. x extreme_point_of (image (λx. a + x) S)} = (λx. a + x) ` {x. x extreme_point_of S}" using extreme_point_of_translation_eq by auto (metis (no_types, lifting) image_iff mem_Collect_eq minus_add_cancel) lemma extreme_point_of_Int: "⟦x extreme_point_of S; x extreme_point_of T⟧ ⟹ x extreme_point_of (S ∩ T)" by (simp add: extreme_point_of_def) lemma extreme_point_of_Int_supporting_hyperplane_le: "⟦S ∩ {x. a ∙ x = b} = {c}; ⋀x. x ∈ S ⟹ a ∙ x ≤ b⟧ ⟹ c extreme_point_of S" apply (simp add: face_of_singleton [symmetric]) by (metis face_of_Int_supporting_hyperplane_le_strong convex_singleton) lemma extreme_point_of_Int_supporting_hyperplane_ge: "⟦S ∩ {x. a ∙ x = b} = {c}; ⋀x. x ∈ S ⟹ a ∙ x ≥ b⟧ ⟹ c extreme_point_of S" apply (simp add: face_of_singleton [symmetric]) by (metis face_of_Int_supporting_hyperplane_ge_strong convex_singleton) lemma exposed_point_of_Int_supporting_hyperplane_le: "⟦S ∩ {x. a ∙ x = b} = {c}; ⋀x. x ∈ S ⟹ a ∙ x ≤ b⟧ ⟹ {c} exposed_face_of S" apply (simp add: exposed_face_of_def face_of_singleton) apply (force simp: extreme_point_of_Int_supporting_hyperplane_le) done lemma exposed_point_of_Int_supporting_hyperplane_ge: "⟦S ∩ {x. a ∙ x = b} = {c}; ⋀x. x ∈ S ⟹ a ∙ x ≥ b⟧ ⟹ {c} exposed_face_of S" using exposed_point_of_Int_supporting_hyperplane_le [of S "-a" "-b" c] by simp lemma extreme_point_of_convex_hull_insert: "⟦finite S; a ∉ convex hull S⟧ ⟹ a extreme_point_of (convex hull (insert a S))" apply (case_tac "a ∈ S") apply (simp add: hull_inc) using face_of_convex_hulls [of "insert a S" "{a}"] apply (auto simp: face_of_singleton hull_same) done subsection‹Facets› definition facet_of :: "['a::euclidean_space set, 'a set] ⇒ bool" (infixr "(facet'_of)" 50) where "F facet_of S ⟷ F face_of S ∧ F ≠ {} ∧ aff_dim F = aff_dim S - 1" lemma facet_of_empty [simp]: "~ S facet_of {}" by (simp add: facet_of_def) lemma facet_of_irrefl [simp]: "~ S facet_of S " by (simp add: facet_of_def) lemma facet_of_imp_face_of: "F facet_of S ⟹ F face_of S" by (simp add: facet_of_def) lemma facet_of_imp_subset: "F facet_of S ⟹ F ⊆ S" by (simp add: face_of_imp_subset facet_of_def) lemma hyperplane_facet_of_halfspace_le: "a ≠ 0 ⟹ {x. a ∙ x = b} facet_of {x. a ∙ x ≤ b}" unfolding facet_of_def hyperplane_eq_empty by (auto simp: hyperplane_face_of_halfspace_ge hyperplane_face_of_halfspace_le DIM_positive Suc_leI of_nat_diff aff_dim_halfspace_le) lemma hyperplane_facet_of_halfspace_ge: "a ≠ 0 ⟹ {x. a ∙ x = b} facet_of {x. a ∙ x ≥ b}" unfolding facet_of_def hyperplane_eq_empty by (auto simp: hyperplane_face_of_halfspace_le hyperplane_face_of_halfspace_ge DIM_positive Suc_leI of_nat_diff aff_dim_halfspace_ge) lemma facet_of_halfspace_le: "F facet_of {x. a ∙ x ≤ b} ⟷ a ≠ 0 ∧ F = {x. a ∙ x = b}" (is "?lhs = ?rhs") proof assume c: ?lhs with c facet_of_irrefl show ?rhs by (force simp: aff_dim_halfspace_le facet_of_def face_of_halfspace_le cong: conj_cong split: if_split_asm) next assume ?rhs then show ?lhs by (simp add: hyperplane_facet_of_halfspace_le) qed lemma facet_of_halfspace_ge: "F facet_of {x. a ∙ x ≥ b} ⟷ a ≠ 0 ∧ F = {x. a ∙ x = b}" using facet_of_halfspace_le [of F "-a" "-b"] by simp subsection ‹Edges: faces of affine dimension 1› definition edge_of :: "['a::euclidean_space set, 'a set] ⇒ bool" (infixr "(edge'_of)" 50) where "e edge_of S ⟷ e face_of S ∧ aff_dim e = 1" lemma edge_of_imp_subset: "S edge_of T ⟹ S ⊆ T" by (simp add: edge_of_def face_of_imp_subset) subsection‹Existence of extreme points› lemma different_norm_3_collinear_points: fixes a :: "'a::euclidean_space" assumes "x ∈ open_segment a b" "norm(a) = norm(b)" "norm(x) = norm(b)" shows False proof - obtain u where "norm ((1 - u) *⇩_{R}a + u *⇩_{R}b) = norm b" and "a ≠ b" and u01: "0 < u" "u < 1" using assms by (auto simp: open_segment_image_interval if_splits) then have "(1 - u) *⇩_{R}a ∙ (1 - u) *⇩_{R}a + ((1 - u) * 2) *⇩_{R}a ∙ u *⇩_{R}b = (1 - u * u) *⇩_{R}(a ∙ a)" using assms by (simp add: norm_eq algebra_simps inner_commute) then have "(1 - u) *⇩_{R}((1 - u) *⇩_{R}a ∙ a + (2 * u) *⇩_{R}a ∙ b) = (1 - u) *⇩_{R}((1 + u) *⇩_{R}(a ∙ a))" by (simp add: algebra_simps) then have "(1 - u) *⇩_{R}(a ∙ a) + (2 * u) *⇩_{R}(a ∙ b) = (1 + u) *⇩_{R}(a ∙ a)" using u01 by auto then have "a ∙ b = a ∙ a" using u01 by (simp add: algebra_simps) then have "a = b" using ‹norm(a) = norm(b)› norm_eq vector_eq by fastforce then show ?thesis using ‹a ≠ b› by force qed proposition extreme_point_exists_convex: fixes S :: "'a::euclidean_space set" assumes "compact S" "convex S" "S ≠ {}" obtains x where "x extreme_point_of S" proof - obtain x where "x ∈ S" and xsup: "⋀y. y ∈ S ⟹ norm y ≤ norm x" using distance_attains_sup [of S 0] assms by auto have False if "a ∈ S" "b ∈ S" and x: "x ∈ open_segment a b" for a b proof - have noax: "norm a ≤ norm x" and nobx: "norm b ≤ norm x" using xsup that by auto have "a ≠ b" using empty_iff open_segment_idem x by auto have *: "(1 - u) * na + u * nb < norm x" if "na < norm x" "nb ≤ norm x" "0 < u" "u < 1" for na nb u proof - have "(1 - u) * na + u * nb < (1 - u) * norm x + u * nb" by (simp add: that) also have "... ≤ (1 - u) * norm x + u * norm x" by (simp add: that) finally have "(1 - u) * na + u * nb < (1 - u) * norm x + u * norm x" . then show ?thesis using scaleR_collapse [symmetric, of "norm x" u] by auto qed have "norm x < norm x" if "norm a < norm x" using x apply (clarsimp simp only: open_segment_image_interval ‹a ≠ b› if_False) apply (rule norm_triangle_lt) apply (simp add: norm_mult) using * [of "norm a" "norm b"] nobx that apply blast done moreover have "norm x < norm x" if "norm b < norm x" using x apply (clarsimp simp only: open_segment_image_interval ‹a ≠ b› if_False) apply (rule norm_triangle_lt) apply (simp add: norm_mult) using * [of "norm b" "norm a" "1-u" for u] noax that apply (simp add: add.commute) done ultimately have "~ (norm a < norm x) ∧ ~ (norm b < norm x)" by auto then show ?thesis using different_norm_3_collinear_points noax nobx that(3) by fastforce qed then show ?thesis apply (rule_tac x=x in that) apply (force simp: extreme_point_of_def ‹x ∈ S›) done qed subsection‹Krein-Milman, the weaker form› proposition Krein_Milman: fixes S :: "'a::euclidean_space set" assumes "compact S" "convex S" shows "S = closure(convex hull {x. x extreme_point_of S})" proof (cases "S = {}") case True then show ?thesis by simp next case False have "closed S" by (simp add: ‹compact S› compact_imp_closed) have "closure (convex hull {x. x extreme_point_of S}) ⊆ S" apply (rule closure_minimal [OF hull_minimal ‹closed S›]) using assms apply (auto simp: extreme_point_of_def) done moreover have "u ∈ closure (convex hull {x. x extreme_point_of S})" if "u ∈ S" for u proof (rule ccontr) assume unot: "u ∉ closure(convex hull {x. x extreme_point_of S})" then obtain a b where "a ∙ u < b" and ab: "⋀x. x ∈ closure(convex hull {x. x extreme_point_of S}) ⟹ b < a ∙ x" using separating_hyperplane_closed_point [of "closure(convex hull {x. x extreme_point_of S})"] by blast have "continuous_on S ((∙) a)" by (rule continuous_intros)+ then obtain m where "m ∈ S" and m: "⋀y. y ∈ S ⟹ a ∙ m ≤ a ∙ y" using continuous_attains_inf [of S "λx. a ∙ x"] ‹compact S› ‹u ∈ S› by auto define T where "T = S ∩ {x. a ∙ x = a ∙ m}" have "m ∈ T" by (simp add: T_def ‹m ∈ S›) moreover have "compact T" by (simp add: T_def compact_Int_closed [OF ‹compact S› closed_hyperplane]) moreover have "convex T" by (simp add: T_def convex_Int [OF ‹convex S› convex_hyperplane]) ultimately obtain v where v: "v extreme_point_of T" using extreme_point_exists_convex [of T] by auto then have "{v} face_of T" by (simp add: face_of_singleton) also have "T face_of S" by (simp add: T_def m face_of_Int_supporting_hyperplane_ge [OF ‹convex S›]) finally have "v extreme_point_of S" by (simp add: face_of_singleton) then have "b < a ∙ v" using closure_subset by (simp add: closure_hull hull_inc ab) then show False using ‹a ∙ u < b› ‹{v} face_of T› face_of_imp_subset m T_def that by fastforce qed ultimately show ?thesis by blast qed text‹Now the sharper form.› lemma Krein_Milman_Minkowski_aux: fixes S :: "'a::euclidean_space set" assumes n: "dim S = n" and S: "compact S" "convex S" "0 ∈ S" shows "0 ∈ convex hull {x. x extreme_point_of S}" using n S proof (induction n arbitrary: S rule: less_induct) case (less n S) show ?case proof (cases "0 ∈ rel_interior S") case True with Krein_Milman show ?thesis by (metis subsetD convex_convex_hull convex_rel_interior_closure less.prems(2) less.prems(3) rel_interior_subset) next case False have "rel_interior S ≠ {}" by (simp add: rel_interior_convex_nonempty_aux less) then obtain c where c: "c ∈ rel_interior S" by blast obtain a where "a ≠ 0" and le_ay: "⋀y. y ∈ S ⟹ a ∙ 0 ≤ a ∙ y" and less_ay: "⋀y. y ∈ rel_interior S ⟹ a ∙ 0 < a ∙ y" by (blast intro: supporting_hyperplane_rel_boundary intro!: less False) have face: "S ∩ {x. a ∙ x = 0} face_of S" apply (rule face_of_Int_supporting_hyperplane_ge [OF ‹convex S›]) using le_ay by auto then have co: "compact (S ∩ {x. a ∙ x = 0})" "convex (S ∩ {x. a ∙ x = 0})" using less.prems by (blast intro: face_of_imp_compact face_of_imp_convex)+ have "a ∙ y = 0" if "y ∈ span (S ∩ {x. a ∙ x = 0})" for y proof - have "y ∈ span {x. a ∙ x = 0}" by (metis inf.cobounded2 span_mono subsetCE that) then show ?thesis by (blast intro: span_induct [OF _ subspace_hyperplane]) qed then have "dim (S ∩ {x. a ∙ x = 0}) < n" by (metis (no_types) less_ay c subsetD dim_eq_span inf.strict_order_iff inf_le1 ‹dim S = n› not_le rel_interior_subset span_0 span_base) then have "0 ∈ convex hull {x. x extreme_point_of (S ∩ {x. a ∙ x = 0})}" by (rule less.IH) (auto simp: co less.prems) then show ?thesis by (metis (mono_tags, lifting) Collect_mono_iff ‹S ∩ {x. a ∙ x = 0} face_of S› extreme_point_of_face hull_mono subset_iff) qed qed theorem Krein_Milman_Minkowski: fixes S :: "'a::euclidean_space set" assumes "compact S" "convex S" shows "S = convex hull {x. x extreme_point_of S}" proof show "S ⊆ convex hull {x. x extreme_point_of S}" proof fix a assume [simp]: "a ∈ S" have 1: "compact ((+) (- a) ` S)" by (simp add: ‹compact S› compact_translation) have 2: "convex ((+) (- a) ` S)" by (simp add: ‹convex S› convex_translation) show a_invex: "a ∈ convex hull {x. x extreme_point_of S}" using Krein_Milman_Minkowski_aux [OF refl 1 2] convex_hull_translation [of "-a"] by (auto simp: extreme_points_of_translation translation_assoc) qed next show "convex hull {x. x extreme_point_of S} ⊆ S" proof - have "{a. a extreme_point_of S} ⊆ S" using extreme_point_of_def by blast then show ?thesis by (simp add: ‹convex S› hull_minimal) qed qed subsection‹Applying it to convex hulls of explicitly indicated finite sets› lemma Krein_Milman_polytope: fixes S :: "'a::euclidean_space set" shows "finite S ⟹ convex hull S = convex hull {x. x extreme_point_of (convex hull S)}" by (simp add: Krein_Milman_Minkowski finite_imp_compact_convex_hull) lemma extreme_points_of_convex_hull_eq: fixes S :: "'a::euclidean_space set" shows "⟦compact S; ⋀T. T ⊂ S ⟹ convex hull T ≠ convex hull S⟧ ⟹ {x. x extreme_point_of (convex hull S)} = S" by (metis (full_types) Krein_Milman_Minkowski compact_convex_hull convex_convex_hull extreme_points_of_convex_hull psubsetI) lemma extreme_point_of_convex_hull_eq: fixes S :: "'a::euclidean_space set" shows "⟦compact S; ⋀T. T ⊂ S ⟹ convex hull T ≠ convex hull S⟧ ⟹ (x extreme_point_of (convex hull S) ⟷ x ∈ S)" using extreme_points_of_convex_hull_eq by auto lemma extreme_point_of_convex_hull_convex_independent: fixes S :: "'a::euclidean_space set" assumes "compact S" and S: "⋀a. a ∈ S ⟹ a ∉ convex hull (S - {a})" shows "(x extreme_point_of (convex hull S) ⟷ x ∈ S)" proof - have "convex hull T ≠ convex hull S" if "T ⊂ S" for T proof - obtain a where "T ⊆ S" "a ∈ S" "a ∉ T" using ‹T ⊂ S› by blast then show ?thesis by (metis (full_types) Diff_eq_empty_iff Diff_insert0 S hull_mono hull_subset insert_Diff_single subsetCE) qed then show ?thesis by (rule extreme_point_of_convex_hull_eq [OF ‹compact S›]) qed lemma extreme_point_of_convex_hull_affine_independent: fixes S :: "'a::euclidean_space set" shows "~ affine_dependent S ⟹ (x extreme_point_of (convex hull S) ⟷ x ∈ S)" by (metis aff_independent_finite affine_dependent_def affine_hull_convex_hull extreme_point_of_convex_hull_convex_independent finite_imp_compact hull_inc) text‹Elementary proofs exist, not requiring Euclidean spaces and all this development› lemma extreme_point_of_convex_hull_2: fixes x :: "'a::euclidean_space" shows "x extreme_point_of (convex hull {a,b}) ⟷ x = a ∨ x = b" proof - have "x extreme_point_of (convex hull {a,b}) ⟷ x ∈ {a,b}" by (intro extreme_point_of_convex_hull_affine_independent affine_independent_2) then show ?thesis by simp qed lemma extreme_point_of_segment: fixes x :: "'a::euclidean_space" shows "x extreme_point_of closed_segment a b ⟷ x = a ∨ x = b" by (simp add: extreme_point_of_convex_hull_2 segment_convex_hull) lemma face_of_convex_hull_subset: fixes S :: "'a::euclidean_space set" assumes "compact S" and T: "T face_of (convex hull S)" obtains s' where "s' ⊆ S" "T = convex hull s'" apply (rule_tac s' = "{x. x extreme_point_of T}" in that) using T extreme_point_of_convex_hull extreme_point_of_face apply blast by (metis (no_types) Krein_Milman_Minkowski assms compact_convex_hull convex_convex_hull face_of_imp_compact face_of_imp_convex) lemma face_of_convex_hull_aux: assumes eq: "x *⇩_{R}p = u *⇩_{R}a + v *⇩_{R}b + w *⇩_{R}c" and x: "u + v + w = x" "x ≠ 0" and S: "affine S" "a ∈ S" "b ∈ S" "c ∈ S" shows "p ∈ S" proof - have "p = (u *⇩_{R}a + v *⇩_{R}b + w *⇩_{R}c) /⇩_{R}x" by (metis ‹x ≠ 0› eq mult.commute right_inverse scaleR_one scaleR_scaleR) moreover have "affine hull {a,b,c} ⊆ S" by (simp add: S hull_minimal) moreover have "(u *⇩_{R}a + v *⇩_{R}b + w *⇩_{R}c) /⇩_{R}x ∈ affine hull {a,b,c}" apply (simp add: affine_hull_3) apply (rule_tac x="u/x" in exI) apply (rule_tac x="v/x" in exI) apply (rule_tac x="w/x" in exI) using x apply (auto simp: algebra_simps divide_simps) done ultimately show ?thesis by force qed proposition face_of_convex_hull_insert_eq: fixes a :: "'a :: euclidean_space" assumes "finite S" and a: "a ∉ affine hull S" shows "(F face_of (convex hull (insert a S)) ⟷ F face_of (convex hull S) ∨ (∃F'. F' face_of (convex hull S) ∧ F = convex hull (insert a F')))" (is "F face_of ?CAS ⟷ _") proof safe assume F: "F face_of ?CAS" and *: "∄F'. F' face_of convex hull S ∧ F = convex hull insert a F'" obtain T where T: "T ⊆ insert a S" and FeqT: "F = convex hull T" by (metis F ‹finite S› compact_insert finite_imp_compact face_of_convex_hull_subset) show "F face_of convex hull S" proof (cases "a ∈ T") case True have "F = convex hull insert a (convex hull T ∩ convex hull S)" proof have "T ⊆ insert a (convex hull T ∩ convex hull S)" using T hull_subset by fastforce then show "F ⊆ convex hull insert a (convex hull T ∩ convex hull S)" by (simp add: FeqT hull_mono) show "convex hull insert a (convex hull T ∩ convex hull S) ⊆ F" apply (rule hull_minimal) using True by (auto simp: ‹F = convex hull T› hull_inc) qed moreover have "convex hull T ∩ convex hull S face_of convex hull S" by (metis F FeqT convex_convex_hull face_of_slice hull_mono inf.absorb_iff2 subset_insertI) ultimately show ?thesis using * by force next case False then show ?thesis by (metis FeqT F T face_of_subset hull_mono subset_insert subset_insertI) qed next assume "F face_of convex hull S" show "F face_of ?CAS" by (simp add: ‹F face_of convex hull S› a face_of_convex_hull_insert ‹finite S›) next fix F assume F: "F face_of convex hull S" show "convex hull insert a F face_of ?CAS" proof (cases "S = {}") case True then show ?thesis using F face_of_affine_eq by auto next case False have anotc: "a ∉ convex hull S" by (metis (no_types) a affine_hull_convex_hull hull_inc) show ?thesis proof (cases "F = {}") case True show ?thesis using anotc by (simp add: ‹F = {}› ‹finite S› extreme_point_of_convex_hull_insert face_of_singleton) next case False have "convex hull insert a F ⊆ ?CAS" by (simp add: F a ‹finite S› convex_hull_subset face_of_convex_hull_insert face_of_imp_subset hull_inc) moreover have "(∃y v. (1 - ub) *⇩_{R}a + ub *⇩_{R}b = (1 - v) *⇩_{R}a + v *⇩_{R}y ∧ 0 ≤ v ∧ v ≤ 1 ∧ y ∈ F) ∧ (∃x u. (1 - uc) *⇩_{R}a + uc *⇩_{R}c = (1 - u) *⇩_{R}a + u *⇩_{R}x ∧ 0 ≤ u ∧ u ≤ 1 ∧ x ∈ F)" if *: "(1 - ux) *⇩_{R}a + ux *⇩_{R}x ∈ open_segment ((1 - ub) *⇩_{R}a + ub *⇩_{R}b) ((1 - uc) *⇩_{R}a + uc *⇩_{R}c)" and "0 ≤ ub" "ub ≤ 1" "0 ≤ uc" "uc ≤ 1" "0 ≤ ux" "ux ≤ 1" and b: "b ∈ convex hull S" and c: "c ∈ convex hull S" and "x ∈ F" for b c ub uc ux x proof - obtain v where ne: "(1 - ub) *⇩_{R}a + ub *⇩_{R}b ≠ (1 - uc) *⇩_{R}a + uc *⇩_{R}c" and eq: "(1 - ux) *⇩_{R}a + ux *⇩_{R}x = (1 - v) *⇩_{R}((1 - ub) *⇩_{R}a + ub *⇩_{R}b) + v *⇩_{R}((1 - uc) *⇩_{R}a + uc *⇩_{R}c)" and "0 < v" "v < 1" using * by (auto simp: in_segment) then have 0: "((1 - ux) - ((1 - v) * (1 - ub) + v * (1 - uc))) *⇩_{R}a + (ux *⇩_{R}x - (((1 - v) * ub) *⇩_{R}b + (v * uc) *⇩_{R}c)) = 0" by (auto simp: algebra_simps) then have "((1 - ux) - ((1 - v) * (1 - ub) + v * (1 - uc))) *⇩_{R}a = ((1 - v) * ub) *⇩_{R}b + (v * uc) *⇩_{R}c + (-ux) *⇩_{R}x" by (auto simp: algebra_simps) then have "a ∈ affine hull S" if "1 - ux - ((1 - v) * (1 - ub) + v * (1 - uc)) ≠ 0" apply (rule face_of_convex_hull_aux) using b c that apply (auto simp: algebra_simps) using F convex_hull_subset_affine_hull face_of_imp_subset ‹x ∈ F› apply blast+ done then have "1 - ux - ((1 - v) * (1 - ub) + v * (1 - uc)) = 0" using a by blast with 0 have equx: "(1 - v) * ub + v * uc = ux" and uxx: "ux *⇩_{R}x = (((1 - v) * ub) *⇩_{R}b + (v * uc) *⇩_{R}c)" by auto (auto simp: algebra_simps) show ?thesis proof (cases "uc = 0") case True then show ?thesis using equx 0 ‹0 ≤ ub› ‹ub ≤ 1› ‹v < 1› ‹x ∈ F› apply (auto simp: algebra_simps) apply (rule_tac x=x in exI, simp) apply (rule_tac x=ub in exI, auto) apply (metis add.left_neutral diff_eq_eq less_irrefl mult.commute mult_cancel_right1 real_vector.scale_cancel_left real_vector.scale_left_diff_distrib) using ‹x ∈ F› ‹uc ≤ 1› apply blast done next case False show ?thesis proof (cases "ub = 0") case True then show ?thesis using equx 0 ‹0 ≤ uc› ‹uc ≤ 1› ‹0 < v› ‹x ∈ F› ‹uc ≠ 0› by (force simp: algebra_simps) next case False then have "0 < ub" "0 < uc" using ‹uc ≠ 0› ‹0 ≤ ub› ‹0 ≤ uc› by auto then have "ux ≠ 0" by (metis ‹0 < v› ‹v < 1› diff_ge_0_iff_ge dual_order.strict_implies_order equx leD le_add_same_cancel2 zero_le_mult_iff zero_less_mult_iff) have "b ∈ F ∧ c ∈ F" proof (cases "b = c") case True then show ?thesis by (metis ‹ux ≠ 0› equx real_vector.scale_cancel_left scaleR_add_left uxx ‹x ∈ F›) next case False have "x = (((1 - v) * ub) *⇩_{R}b + (v * uc) *⇩_{R}c) /⇩_{R}ux" by (metis ‹ux ≠ 0› uxx mult.commute right_inverse scaleR_one scaleR_scaleR) also have "... = (1 - v * uc / ux) *⇩_{R}b + (v * uc / ux) *⇩_{R}c" using ‹ux ≠ 0› equx apply (auto simp: algebra_simps divide_simps) by (metis add.commute add_diff_eq add_divide_distrib diff_add_cancel scaleR_add_left) finally have "x = (1 - v * uc / ux) *⇩_{R}b + (v * uc / ux) *⇩_{R}c" . then have "x ∈ open_segment b c" apply (simp add: in_segment ‹b ≠ c›) apply (rule_tac x="(v * uc) / ux" in exI) using ‹0 ≤ ux› ‹ux ≠ 0› ‹0 < uc› ‹0 < v› ‹0 < ub› ‹v < 1› equx apply (force simp: algebra_simps divide_simps) done then show ?thesis by (rule face_ofD [OF F _ b c ‹x ∈ F›]) qed with ‹0 ≤ ub› ‹ub ≤ 1› ‹0 ≤ uc› ‹uc ≤ 1› show ?thesis by blast qed qed qed moreover have "convex hull F = F" by (meson F convex_hull_eq face_of_imp_convex) ultimately show ?thesis unfolding face_of_def by (fastforce simp: convex_hull_insert_alt ‹S ≠ {}› ‹F ≠ {}›) qed qed qed lemma face_of_convex_hull_insert2: fixes a :: "'a :: euclidean_space" assumes S: "finite S" and a: "a ∉ affine hull S" and F: "F face_of convex hull S" shows "convex hull (insert a F) face_of convex hull (insert a S)" by (metis F face_of_convex_hull_insert_eq [OF S a]) proposition face_of_convex_hull_affine_independent: fixes S :: "'a::euclidean_space set" assumes "~ affine_dependent S" shows "(T face_of (convex hull S) ⟷ (∃c. c ⊆ S ∧ T = convex hull c))" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs by (meson ‹T face_of convex hull S› aff_independent_finite assms face_of_convex_hull_subset finite_imp_compact) next assume ?rhs then obtain c where "c ⊆ S" and T: "T = convex hull c" by blast have "affine hull c ∩ affine hull (S - c) = {}" apply (rule disjoint_affine_hull [OF assms ‹c ⊆ S›], auto) done then have "affine hull c ∩ convex hull (S - c) = {}" using convex_hull_subset_affine_hull by fastforce then show ?lhs by (metis face_of_convex_hulls ‹c ⊆ S› aff_independent_finite assms T) qed lemma facet_of_convex_hull_affine_independent: fixes S :: "'a::euclidean_space set" assumes "~ affine_dependent S" shows "T facet_of (convex hull S) ⟷ T ≠ {} ∧ (∃u. u ∈ S ∧ T = convex hull (S - {u}))" (is "?lhs = ?rhs") proof assume ?lhs then have "T face_of (convex hull S)" "T ≠ {}" and afft: "aff_dim T = aff_dim (convex hull S) - 1" by (auto simp: facet_of_def) then obtain c where "c ⊆ S" and c: "T = convex hull c" by (auto simp: face_of_convex_hull_affine_independent [OF assms]) then have affs: "aff_dim S = aff_dim c + 1" by (metis aff_dim_convex_hull afft eq_diff_eq) have "~ affine_dependent c" using ‹c ⊆ S› affine_dependent_subset assms by blast with affs have "card (S - c) = 1" apply (simp add: aff_dim_affine_independent [symmetric] aff_dim_convex_hull) by (metis aff_dim_affine_independent aff_independent_finite One_nat_def ‹c ⊆ S› add.commute add_diff_cancel_right' assms card_Diff_subset card_mono of_nat_1 of_nat_diff of_nat_eq_iff) then obtain u where u: "u ∈ S - c" by (metis DiffI ‹c ⊆ S› aff_independent_finite assms cancel_comm_monoid_add_class.diff_cancel card_Diff_subset subsetI subset_antisym zero_neq_one) then have u: "S = insert u c" by (metis Diff_subset ‹c ⊆ S› ‹card (S - c) = 1› card_1_singletonE double_diff insert_Diff insert_subset singletonD) have "T = convex hull (c - {u})" by (metis Diff_empty Diff_insert0 ‹T facet_of convex hull S› c facet_of_irrefl insert_absorb u) with ‹T ≠ {}› show ?rhs using c u by auto next assume ?rhs then obtain u where "T ≠ {}" "u ∈ S" and u: "T = convex hull (S - {u})" by (force simp: facet_of_def) then have "¬ S ⊆ {u}" using ‹T ≠ {}› u by auto have [simp]: "aff_dim (convex hull (S - {u})) = aff_dim (convex hull S) - 1" using assms ‹u ∈ S› apply (simp add: aff_dim_convex_hull affine_dependent_def) apply (drule bspec, assumption) by (metis add_diff_cancel_right' aff_dim_insert insert_Diff [of u S]) show ?lhs apply (subst u) apply (simp add: ‹¬ S ⊆ {u}› facet_of_def face_of_convex_hull_affine_independent [OF assms], blast) done qed lemma facet_of_convex_hull_affine_independent_alt: fixes S :: "'a::euclidean_space set" shows "~affine_dependent S ⟹ (T facet_of (convex hull S) ⟷ 2 ≤ card S ∧ (∃u. u ∈ S ∧ T = convex hull (S - {u})))" apply (simp add: facet_of_convex_hull_affine_independent) apply (auto simp: Set.subset_singleton_iff) 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) done lemma segment_face_of: assumes "(closed_segment a b) face_of S" shows "a extreme_point_of S" "b extreme_point_of S" proof - have as: "{a} face_of S" 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) moreover have "{b} face_of S" proof - have "b ∈ convex hull {a} ∨ b extreme_point_of convex hull {b, a}" by (meson extreme_point_of_convex_hull_insert finite.emptyI finite.insertI) moreover have "closed_segment a b = convex hull {b, a}" using closed_segment_commute segment_convex_hull by blast ultimately show ?thesis by (metis as assms face_of_face convex_hull_singleton empty_iff face_of_singleton insertE) qed ultimately show "a extreme_point_of S" "b extreme_point_of S" using face_of_singleton by blast+ qed lemma Krein_Milman_frontier: fixes S :: "'a::euclidean_space set" assumes "convex S" "compact S" shows "S = convex hull (frontier S)" (is "?lhs = ?rhs") proof have "?lhs ⊆ convex hull {x. x extreme_point_of S}" using Krein_Milman_Minkowski assms by blast also have "... ⊆ ?rhs" apply (rule hull_mono) apply (auto simp: frontier_def extreme_point_not_in_interior) using closure_subset apply (force simp: extreme_point_of_def) done finally show "?lhs ⊆ ?rhs" . next have "?rhs ⊆ convex hull S" by (metis Diff_subset ‹compact S› closure_closed compact_eq_bounded_closed frontier_def hull_mono) also have "... ⊆ ?lhs" by (simp add: ‹convex S› hull_same) finally show "?rhs ⊆ ?lhs" . qed subsection‹Polytopes› definition polytope where "polytope S ≡ ∃v. finite v ∧ S = convex hull v" lemma polytope_translation_eq: "polytope (image (λx. a + x) S) ⟷ polytope S" apply (simp add: polytope_def, safe) apply (metis convex_hull_translation finite_imageI translation_galois) by (metis convex_hull_translation finite_imageI) lemma polytope_linear_image: "⟦linear f; polytope p⟧ ⟹ polytope(image f p)" unfolding polytope_def using convex_hull_linear_image by blast lemma polytope_empty: "polytope {}" using convex_hull_empty polytope_def by blast lemma polytope_convex_hull: "finite S ⟹ polytope(convex hull S)" using polytope_def by auto lemma polytope_Times: "⟦polytope S; polytope T⟧ ⟹ polytope(S × T)" unfolding polytope_def by (metis finite_cartesian_product convex_hull_Times) lemma face_of_polytope_polytope: fixes S :: "'a::euclidean_space set" shows "⟦polytope S; F face_of S⟧ ⟹ polytope F" unfolding polytope_def by (meson face_of_convex_hull_subset finite_imp_compact finite_subset) lemma finite_polytope_faces: fixes S :: "'a::euclidean_space set" assumes "polytope S" shows "finite {F. F face_of S}" proof - obtain v where "finite v" "S = convex hull v" using assms polytope_def by auto have "finite ((hull) convex ` {T. T ⊆ v})" by (simp add: ‹finite v›) moreover have "{F. F face_of S} ⊆ ((hull) convex ` {T. T ⊆ v})" by (metis (no_types, lifting) ‹finite v› ‹S = convex hull v› face_of_convex_hull_subset finite_imp_compact image_eqI mem_Collect_eq subsetI) ultimately show ?thesis by (blast intro: finite_subset) qed lemma finite_polytope_facets: assumes "polytope S" shows "finite {T. T facet_of S}" by (simp add: assms facet_of_def finite_polytope_faces) lemma polytope_scaling: assumes "polytope S" shows "polytope (image (λx. c *⇩_{R}x) S)" by (simp add: assms polytope_linear_image) lemma polytope_imp_compact: fixes S :: "'a::real_normed_vector set" shows "polytope S ⟹ compact S" by (metis finite_imp_compact_convex_hull polytope_def) lemma polytope_imp_convex: "polytope S ⟹ convex S" by (metis convex_convex_hull polytope_def) lemma polytope_imp_closed: fixes S :: "'a::real_normed_vector set" shows "polytope S ⟹ closed S" by (simp add: compact_imp_closed polytope_imp_compact) lemma polytope_imp_bounded: fixes S :: "'a::real_normed_vector set" shows "polytope S ⟹ bounded S" by (simp add: compact_imp_bounded polytope_imp_compact) lemma polytope_interval: "polytope(cbox a b)" unfolding polytope_def by (meson closed_interval_as_convex_hull) lemma polytope_sing: "polytope {a}" using polytope_def by force lemma face_of_polytope_insert: "⟦polytope S; a ∉ affine hull S; F face_of S⟧ ⟹ F face_of convex hull (insert a S)" by (metis (no_types, lifting) affine_hull_convex_hull face_of_convex_hull_insert hull_insert polytope_def) lemma face_of_polytope_insert2: fixes a :: "'a :: euclidean_space" assumes "polytope S" "a ∉ affine hull S" "F face_of S" shows "convex hull (insert a F) face_of convex hull (insert a S)" proof - obtain V where "finite V" "S = convex hull V" using assms by (auto simp: polytope_def) then have "convex hull (insert a F) face_of convex hull (insert a V)" using affine_hull_convex_hull assms face_of_convex_hull_insert2 by blast then show ?thesis by (metis ‹S = convex hull V› hull_insert) qed subsection‹Polyhedra› definition polyhedron where "polyhedron S ≡ ∃F. finite F ∧ S = ⋂ F ∧ (∀h ∈ F. ∃a b. a ≠ 0 ∧ h = {x. a ∙ x ≤ b})" lemma polyhedron_Int [intro,simp]: "⟦polyhedron S; polyhedron T⟧ ⟹ polyhedron (S ∩ T)" apply (simp add: polyhedron_def, clarify) apply (rename_tac F G) apply (rule_tac x="F ∪ G" in exI, auto) done lemma polyhedron_UNIV [iff]: "polyhedron UNIV" unfolding polyhedron_def by (rule_tac x="{}" in exI) auto lemma polyhedron_Inter [intro,simp]: "⟦finite F; ⋀S. S ∈ F ⟹ polyhedron S⟧ ⟹ polyhedron(⋂F)" by (induction F rule: finite_induct) auto lemma polyhedron_empty [iff]: "polyhedron ({} :: 'a :: euclidean_space set)" proof - have "∃a. a ≠ 0 ∧ (∃b. {x. (SOME i. i ∈ Basis) ∙ x ≤ - 1} = {x. a ∙ x ≤ b})" by (rule_tac x="(SOME i. i ∈ Basis)" in exI) (force simp: SOME_Basis nonzero_Basis) moreover have "∃a b. a ≠ 0 ∧ {x. - (SOME i. i ∈ Basis) ∙ x ≤ - 1} = {x. a ∙ x ≤ b}" apply (rule_tac x="-(SOME i. i ∈ Basis)" in exI) apply (rule_tac x="-1" in exI) apply (simp add: SOME_Basis nonzero_Basis) done ultimately show ?thesis unfolding polyhedron_def apply (rule_tac x="{{x. (SOME i. i ∈ Basis) ∙ x ≤ -1}, {x. -(SOME i. i ∈ Basis) ∙ x ≤ -1}}" in exI) apply force done qed lemma polyhedron_halfspace_le: fixes a :: "'a :: euclidean_space" shows "polyhedron {x. a ∙ x ≤ b}" proof (cases "a = 0") case True then show ?thesis by auto next case False then show ?thesis unfolding polyhedron_def by (rule_tac x="{{x. a ∙ x ≤ b}}" in exI) auto qed lemma polyhedron_halfspace_ge: fixes a :: "'a :: euclidean_space" shows "polyhedron {x. a ∙ x ≥ b}" using polyhedron_halfspace_le [of "-a" "-b"] by simp lemma polyhedron_hyperplane: fixes a :: "'a :: euclidean_space" shows "polyhedron {x. a ∙ x = b}" proof - have "{x. a ∙ x = b} = {x. a ∙ x ≤ b} ∩ {x. a ∙ x ≥ b}" by force then show ?thesis by (simp add: polyhedron_halfspace_ge polyhedron_halfspace_le) qed lemma affine_imp_polyhedron: fixes S :: "'a :: euclidean_space set" shows "affine S ⟹ polyhedron S" by (metis affine_hull_eq polyhedron_Inter polyhedron_hyperplane affine_hull_finite_intersection_hyperplanes [of S]) lemma polyhedron_imp_closed: fixes S :: "'a :: euclidean_space set" shows "polyhedron S ⟹ closed S" apply (simp add: polyhedron_def) using closed_halfspace_le by fastforce lemma polyhedron_imp_convex: fixes S :: "'a :: euclidean_space set" shows "polyhedron S ⟹ convex S" apply (simp add: polyhedron_def) using convex_Inter convex_halfspace_le by fastforce lemma polyhedron_affine_hull: fixes S :: "'a :: euclidean_space set" shows "polyhedron(affine hull S)" by (simp add: affine_imp_polyhedron) subsection‹Canonical polyhedron representation making facial structure explicit› lemma polyhedron_Int_affine: fixes S :: "'a :: euclidean_space set" shows "polyhedron S ⟷ (∃F. finite F ∧ S = (affine hull S) ∩ ⋂F ∧ (∀h ∈ F. ∃a b. a ≠ 0 ∧ h = {x. a ∙ x ≤ b}))" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs apply (simp add: polyhedron_def) apply (erule ex_forward) using hull_subset apply force done next assume ?rhs then show ?lhs apply clarify apply (erule ssubst) apply (force intro: polyhedron_affine_hull polyhedron_halfspace_le) done qed proposition rel_interior_polyhedron_explicit: assumes "finite F" and seq: "S = affine hull S ∩ ⋂F" and faceq: "⋀h. h ∈ F ⟹ a h ≠ 0 ∧ h = {x. a h ∙ x ≤ b h}" and psub: "⋀F'. F' ⊂ F ⟹ S ⊂ affine hull S ∩ ⋂F'" shows "rel_interior S = {x ∈ S. ∀h ∈ F. a h ∙ x < b h}" proof - have rels: "⋀x. x ∈ rel_interior S ⟹ x ∈ S" by (meson IntE mem_rel_interior) moreover have "a i ∙ x < b i" if x: "x ∈ rel_interior S" and "i ∈ F" for x i proof - have fif: "F - {i} ⊂ F" using ‹i ∈ F› Diff_insert_absorb Diff_subset set_insert psubsetI by blast then have "S ⊂ affine hull S ∩ ⋂(F - {i})" by (rule psub) then obtain z where ssub: "S ⊆ ⋂(F - {i})" and zint: "z ∈ ⋂(F - {i})" and "z ∉ S" and zaff: "z ∈ affine hull S" by auto have "z ≠ x" using ‹z ∉ S› rels x by blast have "z ∉ affine hull S ∩ ⋂F" using ‹z ∉ S› seq by auto then have aiz: "a i ∙ z > b i" using faceq zint zaff by fastforce obtain e where "e > 0" "x ∈ S" and e: "ball x e ∩ affine hull S ⊆ S" using x by (auto simp: mem_rel_interior_ball) then have ins: "⋀y. ⟦norm (x - y) < e; y ∈ affine hull S⟧ ⟹ y ∈ S" by (metis IntI subsetD dist_norm mem_ball) define ξ where "ξ = min (1/2) (e / 2 / norm(z - x))" have "norm (ξ *⇩_{R}x - ξ *⇩_{R}z) = norm (ξ *⇩_{R}(x - z))" by (simp add: ξ_def algebra_simps norm_mult) also have "... = ξ * norm (x - z)" using ‹e > 0› by (simp add: ξ_def) also have "... < e" using ‹z ≠ x› ‹e > 0› by (simp add: ξ_def min_def divide_simps norm_minus_commute) finally have lte: "norm (ξ *⇩_{R}x - ξ *⇩_{R}z) < e" . have ξ_aff: "ξ *⇩_{R}z + (1 - ξ) *⇩_{R}x ∈ affine hull S" by (metis ‹x ∈ S› add.commute affine_affine_hull diff_add_cancel hull_inc mem_affine zaff) have "ξ *⇩_{R}z + (1 - ξ) *⇩_{R}x ∈ S" apply (rule ins [OF _ ξ_aff]) apply (simp add: algebra_simps lte) done then obtain l where l: "0 < l" "l < 1" and ls: "(l *⇩_{R}z + (1 - l) *⇩_{R}x) ∈ S" apply (rule_tac l = ξ in that) using ‹e > 0› ‹z ≠ x› apply (auto simp: ξ_def) done then have i: "l *⇩_{R}z + (1 - l) *⇩_{R}x ∈ i" using seq ‹i ∈ F› by auto have "b i * l + (a i ∙ x) * (1 - l) < a i ∙ (l *⇩_{R}z + (1 - l) *⇩_{R}x)" using l by (simp add: algebra_simps aiz) also have "… ≤ b i" using i l using faceq mem_Collect_eq ‹i ∈ F› by blast finally have "(a i ∙ x) * (1 - l) < b i * (1 - l)" by (simp add: algebra_simps) with l show ?thesis by simp qed moreover have "x ∈ rel_interior S" if "x ∈ S" and less: "⋀h. h ∈ F ⟹ a h ∙ x < b h" for x proof - have 1: "⋀h. h ∈ F ⟹ x ∈ interior h" by (metis interior_halfspace_le mem_Collect_eq less faceq) have 2: "⋀y. ⟦∀h∈F. y ∈ interior h; y ∈ affine hull S⟧ ⟹ y ∈ S" by (metis IntI Inter_iff contra_subsetD interior_subset seq) show ?thesis apply (simp add: rel_interior ‹x ∈ S›) apply (rule_tac x="⋂h∈F. interior h" in exI) apply (auto simp: ‹finite F› open_INT 1 2) done qed ultimately show ?thesis by blast qed lemma polyhedron_Int_affine_parallel: fixes S :: "'a :: euclidean_space set" shows "polyhedron S ⟷ (∃F. finite F ∧ S = (affine hull S) ∩ (⋂F) ∧ (∀h ∈ F. ∃a b. a ≠ 0 ∧ h = {x. a ∙ x ≤ b} ∧ (∀x ∈ affine hull S. (x + a) ∈ affine hull S)))" (is "?lhs = ?rhs") proof assume ?lhs then obtain F where "finite F" and seq: "S = (affine hull S) ∩ ⋂F" and faces: "⋀h. h ∈ F ⟹ ∃a b. a ≠ 0 ∧ h = {x. a ∙ x ≤ b}" by (fastforce simp add: polyhedron_Int_affine) then obtain a b where ab: "⋀h. h ∈ F ⟹ a h ≠ 0 ∧ h = {x. a h ∙ x ≤ b h}" by metis show ?rhs proof - have "∃a' b'. a' ≠ 0 ∧ affine hull S ∩ {x. a' ∙ x ≤ b'} = affine hull S ∩ h ∧ (∀w ∈ affine hull S. (w + a') ∈ affine hull S)" if "h ∈ F" "~(affine hull S ⊆ h)" for h proof - have "a h ≠ 0" and "h = {x. a h ∙ x ≤ b h}" "h ∩ ⋂F = ⋂F" using ‹h ∈ F› ab by auto then have "(affine hull S) ∩ {x. a h ∙ x ≤ b h} ≠ {}" by (metis (no_types) affine_hull_eq_empty inf.absorb_iff2 inf_assoc inf_bot_right inf_commute seq that(2)) moreover have "~ (affine hull S ⊆ {x. a h ∙ x ≤ b h})" using ‹h = {x. a h ∙ x ≤ b h}› that(2) by blast ultimately show ?thesis using affine_parallel_slice [of "affine hull S"] by (metis ‹h = {x. a h ∙ x ≤ b h}› affine_affine_hull) qed then obtain a b where ab: "⋀h. ⟦h ∈ F; ~ (affine hull S ⊆ h)⟧ ⟹ a h ≠ 0 ∧ affine hull S ∩ {x. a h ∙ x ≤ b h} = affine hull S ∩ h ∧ (∀w ∈ affine hull S. (w + a h) ∈ affine hull S)" by metis have seq2: "S = affine hull S ∩ (⋂h∈{h ∈ F. ¬ affine hull S ⊆ h}. {x. a h ∙ x ≤ b h})" by (subst seq) (auto simp: ab INT_extend_simps) show ?thesis apply (rule_tac x="(λh. {x. a h ∙ x ≤ b h}) ` {h. h ∈ F ∧ ~(affine hull S ⊆ h)}" in exI) apply (intro conjI seq2) using ‹finite F› apply force using ab apply blast done qed next assume ?rhs then show ?lhs apply (simp add: polyhedron_Int_affine) by metis qed proposition polyhedron_Int_affine_parallel_minimal: fixes S :: "'a :: euclidean_space set" shows "polyhedron S ⟷ (∃F. finite F ∧ S = (affine hull S) ∩ (⋂F) ∧ (∀h ∈ F. ∃a b. a ≠ 0 ∧ h = {x. a ∙ x ≤ b} ∧ (∀x ∈ affine hull S. (x + a) ∈ affine hull S)) ∧ (∀F'. F' ⊂ F ⟶ S ⊂ (affine hull S) ∩ (⋂F')))" (is "?lhs = ?rhs") proof assume ?lhs then obtain f0 where f0: "finite f0" "S = (affine hull S) ∩ (⋂f0)" (is "?P f0") "∀h ∈ f0. ∃a b. a ≠ 0 ∧ h = {x. a ∙ x ≤ b} ∧ (∀x ∈ affine hull S. (x + a) ∈ affine hull S)" (is "?Q f0") by (force simp: polyhedron_Int_affine_parallel) define n where "n = (LEAST n. ∃F. card F = n ∧ finite F ∧ ?P F ∧ ?Q F)" have nf: "∃F. card F = n ∧ finite F ∧ ?P F ∧ ?Q F" apply (simp add: n_def) apply (rule LeastI [where k = "card f0"]) using f0 apply auto done then obtain F where F: "card F = n" "finite F" and seq: "?P F" and aff: "?Q F" by blast then have "~ (finite g ∧ ?P g ∧ ?Q g)" if "card g < n" for g using that by (auto simp: n_def dest!: not_less_Least) then have *: "~ (?P g ∧ ?Q g)" if "g ⊂ F" for g using that ‹finite F› psubset_card_mono ‹card F = n› by (metis finite_Int inf.strict_order_iff) have 1: "⋀F'. F' ⊂ F ⟹ S ⊆ affine hull S ∩ ⋂F'" by (subst seq) blast have 2: "⋀F'. F' ⊂ F ⟹ S ≠ affine hull S ∩ ⋂F'" apply (frule *) by (metis aff subsetCE subset_iff_psubset_eq) show ?rhs by (metis ‹finite F› seq aff psubsetI 1 2) next assume ?rhs then show ?lhs by (auto simp: polyhedron_Int_affine_parallel) qed lemma polyhedron_Int_affine_minimal: fixes S :: "'a :: euclidean_space set" shows "polyhedron S ⟷ (∃F. finite F ∧ S = (affine hull S) ∩ ⋂F ∧ (∀h ∈ F. ∃a b. a ≠ 0 ∧ h = {x. a ∙ x ≤ b}) ∧ (∀F'. F' ⊂ F ⟶ S ⊂ (affine hull S) ∩ ⋂F'))" apply (rule iffI) apply (force simp: polyhedron_Int_affine_parallel_minimal elim!: ex_forward) apply (auto simp: polyhedron_Int_affine elim!: ex_forward) done proposition facet_of_polyhedron_explicit: assumes "finite F" and seq: "S = affine hull S ∩ ⋂F" and faceq: "⋀h. h ∈ F ⟹ a h ≠ 0 ∧ h = {x. a h ∙ x ≤ b h}" and psub: "⋀F'. F' ⊂ F ⟹ S ⊂ affine hull S ∩ ⋂F'" shows "c facet_of S ⟷ (∃h. h ∈ F ∧ c = S ∩ {x. a h ∙ x = b h})" proof (cases "S = {}") case True with psub show ?thesis by force next case False have "polyhedron S" apply (simp add: polyhedron_Int_affine) apply (rule_tac x=F in exI) using assms apply force done then have "convex S" by (rule polyhedron_imp_convex) with False rel_interior_eq_empty have "rel_interior S ≠ {}" by blast then obtain x where "x ∈ rel_interior S" by auto then obtain T where "open T" "x ∈ T" "x ∈ S" "T ∩ affine hull S ⊆ S" by (force simp: mem_rel_interior) then have xaff: "x ∈ affine hull S" and xint: "x ∈ ⋂F" using seq hull_inc by auto have "rel_interior S = {x ∈ S. ∀h∈F. a h ∙ x < b h}" by (rule rel_interior_polyhedron_explicit [OF ‹finite F› seq faceq psub]) with ‹x ∈ rel_interior S› have [simp]: "⋀h. h∈F ⟹ a h ∙ x < b h" by blast have *: "(S ∩ {x. a h ∙ x = b h}) facet_of S" if "h ∈ F" for h proof - have "S ⊂ affine hull S ∩ ⋂(F - {h})" using psub that by (metis Diff_disjoint Diff_subset insert_disjoint(2) psubsetI) then obtain z where zaff: "z ∈ affine hull S" and zint: "z ∈ ⋂(F - {h})" and "z ∉ S" by force then have "z ≠ x" "z ∉ h" using seq ‹x ∈ S› by auto have "x ∈ h" using that xint by auto then have able: "a h ∙ x ≤ b h" using faceq that by blast also have "... < a h ∙ z" using ‹z ∉ h› faceq [OF that] xint by auto finally have xltz: "a h ∙ x < a h ∙ z" . define l where "l = (b h - a h ∙ x) / (a h ∙ z - a h ∙ x)" define w where "w = (1 - l) *⇩_{R}x + l *⇩_{R}z" have "0 < l" "l < 1" using able xltz ‹b h < a h ∙ z› ‹h ∈ F› by (auto simp: l_def divide_simps) have awlt: "a i ∙ w < b i" if "i ∈ F" "i ≠ h" for i proof - have "(1 - l) * (a i ∙ x) < (1 - l) * b i" by (simp add: ‹l < 1› ‹i ∈ F›) moreover have "l * (a i ∙ z) ≤ l * b i" apply (rule mult_left_mono) apply (metis Diff_insert_absorb Inter_iff Set.set_insert ‹h ∈ F› faceq insertE mem_Collect_eq that zint) using ‹0 < l› apply simp done ultimately show ?thesis by (simp add: w_def algebra_simps) qed have weq: "a h ∙ w = b h" using xltz unfolding w_def l_def by (simp add: algebra_simps) (simp add: field_simps) have "w ∈ affine hull S" by (simp add: w_def mem_affine xaff zaff) moreover have "w ∈ ⋂F" using ‹a h ∙ w = b h› awlt faceq less_eq_real_def by blast ultimately have "w ∈ S" using seq by blast with weq have "S ∩ {x. a h ∙ x = b h} ≠ {}" by blast moreover have "S ∩ {x. a h ∙ x = b h} face_of S" apply (rule face_of_Int_supporting_hyperplane_le) apply (rule ‹convex S›) apply (subst (asm) seq) using faceq that apply fastforce done moreover have "affine hull (S ∩ {x. a h ∙ x = b h}) = (affine hull S) ∩ {x. a h ∙ x = b h}" proof show "affine hull (S ∩ {x. a h ∙ x = b h}) ⊆ affine hull S ∩ {x. a h ∙ x = b h}" apply (intro Int_greatest hull_mono Int_lower1) apply (metis affine_hull_eq affine_hyperplane hull_mono inf_le2) done next show "affine hull S ∩ {x. a h ∙ x = b h} ⊆ affine hull (S ∩ {x. a h ∙ x = b h})" proof fix y assume yaff: "y ∈ affine hull S ∩ {y. a h ∙ y = b h}" obtain T where "0 < T" and T: "⋀j. ⟦j ∈ F; j ≠ h⟧ ⟹ T * (a j ∙ y - a j ∙ w) ≤ b j - a j ∙ w" proof (cases "F - {h} = {}") case True then show ?thesis by (rule_tac T=1 in that) auto next case False then obtain h' where h': "h' ∈ F - {h}" by auto define inff where "inff = (INF j:F - {h}. if 0 < a j ∙ y - a j ∙ w then (b j - a j ∙ w) / (a j ∙ y - a j ∙ w) else 1)" have "0 < inff" apply (simp add: inff_def) apply (rule finite_imp_less_Inf) using ‹finite F› apply blast using h' apply blast apply simp using awlt apply (force simp: divide_simps) done moreover have "inff * (a j ∙ y - a j ∙ w) ≤ b j - a j ∙ w" if "j ∈ F" "j ≠ h" for j proof (cases "a j ∙ w < a j ∙ y") case True then have "inff ≤ (b j - a j ∙ w) / (a j ∙ y - a j ∙ w)" apply (simp add: inff_def) apply (rule cInf_le_finite) using ‹finite F› apply blast apply (simp add: that split: if_split_asm) done then show ?thesis using ‹0 < inff› awlt [OF that] mult_strict_left_mono by (fastforce simp add: algebra_simps divide_simps split: if_split_asm) next case False with ‹0 < inff› have "inff * (a j ∙ y - a j ∙ w) ≤ 0" by (simp add: mult_le_0_iff) also have "... < b j - a j ∙ w" by (simp add: awlt that) finally show ?thesis by simp qed ultimately show ?thesis by (blast intro: that) qed define c where "c = (1 - T) *⇩_{R}w + T *⇩_{R}y" have "(1 - T) *⇩_{R}w + T *⇩_{R}y ∈ j" if "j ∈ F" for j proof (cases "j = h") case True have "(1 - T) *⇩_{R}w + T *⇩_{R}y ∈ {x. a h ∙ x ≤ b h}" using weq yaff by (auto simp: algebra_simps) with True faceq [OF that] show ?thesis by metis next case False with T that have "(1 - T) *⇩_{R}w + T *⇩_{R}y ∈ {x. a j ∙ x ≤ b j}" by (simp add: algebra_simps) with faceq [OF that] show ?thesis by simp qed moreover have "(1 - T) *⇩_{R}w + T *⇩_{R}y ∈ affine hull S" apply (rule affine_affine_hull [simplified affine_alt, rule_format]) apply (simp add: ‹w ∈ affine hull S›) using yaff apply blast done ultimately have "c ∈ S" using seq by (force simp: c_def) moreover have "a h ∙ c = b h" using yaff by (force simp: c_def algebra_simps weq) ultimately have caff: "c ∈ affine hull (S ∩ {y. a h ∙ y = b h})" by (simp add: hull_inc) have waff: "w ∈ affine hull (S ∩ {y. a h ∙ y = b h})" using ‹w ∈ S› weq by (blast intro: hull_inc) have yeq: "y = (1 - inverse T) *⇩_{R}w + c /⇩_{R}T" using ‹0 < T› by (simp add: c_def algebra_simps) show "y ∈ affine hull (S ∩ {y. a h ∙ y = b h})" by (metis yeq affine_affine_hull [simplified affine_alt, rule_format, OF waff caff]) qed qed ultimately show ?thesis apply (simp add: facet_of_def) apply (subst aff_dim_affine_hull [symmetric]) using ‹b h < a h ∙ z› zaff apply (force simp: aff_dim_affine_Int_hyperplane) done qed show ?thesis proof show "∃h. h ∈ F ∧ c = S ∩ {x. a h ∙ x = b h} ⟹ c facet_of S" using * by blast next assume "c facet_of S" then have "c face_of S" "convex c" "c ≠ {}" and affc: "aff_dim c = aff_dim S - 1" by (auto simp: facet_of_def face_of_imp_convex) then obtain x where x: "x ∈ rel_interior c" by (force simp: rel_interior_eq_empty) then have "x ∈ c" by (meson subsetD rel_interior_subset) then have "x ∈ S" using ‹c facet_of S› facet_of_imp_subset by blast have rels: "rel_interior S = {x ∈ S. ∀h∈F. a h ∙ x < b h}" by (rule rel_interior_polyhedron_explicit [OF assms]) have "c ≠ S" using ‹c facet_of S› facet_of_irrefl by blast then have "x ∉ rel_interior S" by (metis IntI empty_iff ‹x ∈ c› ‹c ≠ S› ‹c face_of S› face_of_disjoint_rel_interior) with rels ‹x ∈ S› obtain i where "i ∈ F" and i: "a i ∙ x ≥ b i" by force have "x ∈ {u. a i ∙ u ≤ b i}" by (metis IntD2 InterE ‹i ∈ F› ‹x ∈ S› faceq seq) then have "a i ∙ x ≤ b i" by simp then have "a i ∙ x = b i" using i by auto have "c ⊆ S ∩ {x. a i ∙ x = b i}" apply (rule subset_of_face_of [of _ S]) apply (simp add: "*" ‹i ∈ F› facet_of_imp_face_of) apply (simp add: ‹c face_of S› face_of_imp_subset) using ‹a i ∙ x = b i› ‹x ∈ S› x by blast then have cface: "c face_of (S ∩ {x. a i ∙ x = b i})" by (meson ‹c face_of S› face_of_subset inf_le1) have con: "convex (S ∩ {x. a i ∙ x = b i})" by (simp add: ‹convex S› convex_Int convex_hyperplane) show "∃h. h ∈ F ∧ c = S ∩ {x. a h ∙ x = b h}" apply (rule_tac x=i in exI) apply (simp add: ‹i ∈ F›) by (metis (no_types) * ‹i ∈ F› affc facet_of_def less_irrefl face_of_aff_dim_lt [OF con cface]) qed qed lemma face_of_polyhedron_subset_explicit: fixes S :: "'a :: euclidean_space set" assumes "finite F" and seq: "S = affine hull S ∩ ⋂F" and faceq: "⋀h. h ∈ F ⟹ a h ≠ 0 ∧ h = {x. a h ∙ x ≤ b h}" and psub: "⋀F'. F' ⊂ F ⟹ S ⊂ affine hull S ∩ ⋂F'" and c: "c face_of S" and "c ≠ {}" "c ≠ S" obtains h where "h ∈ F" "c ⊆ S ∩ {x. a h ∙ x = b h}" proof - have "c ⊆ S" using ‹c face_of S› by (simp add: face_of_imp_subset) have "polyhedron S" apply (simp add: polyhedron_Int_affine) by (metis ‹finite F› faceq seq) then have "convex S" by (simp add: polyhedron_imp_convex) then have *: "(S ∩ {x. a h ∙ x = b h}) face_of S" if "h ∈ F" for h apply (rule face_of_Int_supporting_hyperplane_le) using faceq seq that by fastforce have "rel_interior c ≠ {}" using c ‹c ≠ {}› face_of_imp_convex rel_interior_eq_empty by blast then obtain x where "x ∈ rel_interior c" by auto have rels: "rel_interior S = {x ∈ S. ∀h∈F. a h ∙ x < b h}" by (rule rel_interior_polyhedron_explicit [OF ‹finite F› seq faceq psub]) then have xnot: "x ∉ rel_interior S" by (metis IntI ‹x ∈ rel_interior c› c ‹c ≠ S› contra_subsetD empty_iff face_of_disjoint_rel_interior rel_interior_subset) then have "x ∈ S" using ‹c ⊆ S› ‹x ∈ rel_interior c› rel_interior_subset by auto then have xint: "x ∈ ⋂F" using seq by blast have "F ≠ {}" using assms by (metis affine_Int affine_Inter affine_affine_hull ex_in_conv face_of_affine_trivial) then obtain i where "i ∈ F" "~ (a i ∙ x < b i)" using ‹x ∈ S› rels xnot by auto with xint have "a i ∙ x = b i" by (metis eq_iff mem_Collect_eq not_le Inter_iff faceq) have face: "S ∩ {x. a i ∙ x = b i} face_of S" by (simp add: "*" ‹i ∈ F›) show ?thesis apply (rule_tac h = i in that) apply (rule ‹i ∈ F›) apply (rule subset_of_face_of [OF face ‹c ⊆ S›]) using ‹a i ∙ x = b i› ‹x ∈ rel_interior c› ‹x ∈ S› apply blast done qed text‹Initial part of proof duplicates that above› proposition face_of_polyhedron_explicit: fixes S :: "'a :: euclidean_space set" assumes "finite F" and seq: "S = affine hull S ∩ ⋂F" and faceq: "⋀h. h ∈ F ⟹ a h ≠ 0 ∧ h = {x. a h ∙ x ≤ b h}" and psub: "⋀F'. F' ⊂ F ⟹ S ⊂ affine hull S ∩ ⋂F'" and c: "c face_of S" and "c ≠ {}" "c ≠ S" shows "c = ⋂{S ∩ {x. a h ∙ x = b h} | h. h ∈ F ∧ c ⊆ S ∩ {x. a h ∙ x = b h}}" proof - let ?ab = "λh. {x. a h ∙ x = b h}" have "c ⊆ S" using ‹c face_of S› by (simp add: face_of_imp_subset) have "polyhedron S" apply (simp add: polyhedron_Int_affine) by (metis ‹finite F› faceq seq) then have "convex S" by (simp add: polyhedron_imp_convex) then have *: "(S ∩ ?ab h) face_of S" if "h ∈ F" for h apply (rule face_of_Int_supporting_hyperplane_le) using faceq seq that by fastforce have "rel_interior c ≠ {}" using c ‹c ≠ {}› face_of_imp_convex rel_interior_eq_empty by blast then obtain z where z: "z ∈ rel_interior c" by auto have rels: "rel_interior S = {z ∈ S. ∀h∈F. a h ∙ z < b h}" by (rule rel_interior_polyhedron_explicit [OF ‹finite F› seq faceq psub]) then have xnot: "z ∉ rel_interior S" by (metis IntI ‹z ∈ rel_interior c› c ‹c ≠ S› contra_subsetD empty_iff face_of_disjoint_rel_interior rel_interior_subset) then have "z ∈ S" using ‹c ⊆ S› ‹z ∈ rel_interior c› rel_interior_subset by auto with seq have xint: "z ∈ ⋂F" by blast have "open (⋂h∈{h ∈ F. a h ∙ z < b h}. {w. a h ∙ w < b h})" by (auto simp: ‹finite F› open_halfspace_lt open_INT) then obtain e where "0 < e" "ball z e ⊆ (⋂h∈{h ∈ F. a h ∙ z < b h}. {w. a h ∙ w < b h})" by (auto intro: openE [of _ z]) then have e: "⋀h. ⟦h ∈ F; a h ∙ z < b h⟧ ⟹ ball z e ⊆ {w. a h ∙ w < b h}" by blast have "c ⊆ (S ∩ ?ab h) ⟷ z ∈ S ∩ ?ab h" if "h ∈ F" for h proof show "z ∈ S ∩ ?ab h ⟹ c ⊆ S ∩ ?ab h" apply (rule subset_of_face_of [of _ S]) using that ‹c ⊆ S› ‹z ∈ rel_interior c› using facet_of_polyhedron_explicit [OF ‹finite F› seq faceq psub] unfolding facet_of_def apply auto done next show "c ⊆ S ∩ ?ab h ⟹ z ∈ S ∩ ?ab h" using ‹z ∈ rel_interior c› rel_interior_subset by force qed then have **: "{S ∩ ?ab h | h. h ∈ F ∧ c ⊆ S ∧ c ⊆ ?ab h} = {S ∩ ?ab h |h. h ∈ F ∧ z ∈ S ∩ ?ab h}" by blast have bsub: "ball z e ∩ affine hull ⋂{S ∩ ?ab h |h. h ∈ F ∧ a h ∙ z = b h} ⊆ affine hull S ∩ ⋂F ∩ ⋂{?ab h |h. h ∈ F ∧ a h ∙ z = b h}" if "i ∈ F" and i: "a i ∙ z = b i" for i proof - have sub: "ball z e ∩ ⋂{?ab h |h. h ∈ F ∧ a h ∙ z = b h} ⊆ j" if "j ∈ F" for j proof - have "a j ∙ z ≤ b j" using faceq that xint by auto then consider "a j ∙ z < b j" | "a j ∙ z = b j" by linarith then have "∃G. G ∈ {?ab h |h. h ∈ F ∧ a h ∙ z = b h} ∧ ball z e ∩ G ⊆ j" proof cases assume "a j ∙ z < b j" then have "ball z e ∩ {x. a i ∙ x = b i} ⊆ j" using e [OF ‹j ∈ F›] faceq that by (fastforce simp: ball_def) then show ?thesis by (rule_tac x="{x. a i ∙ x = b i}" in exI) (force simp: ‹i ∈ F› i) next assume eq: "a j ∙ z = b j" with faceq that show ?thesis by (rule_tac x="{x. a j ∙ x = b j}" in exI) (fastforce simp add: ‹j ∈ F›) qed then show ?thesis by blast qed have 1: "affine hull ⋂{S ∩ ?ab h |h. h ∈ F ∧ a h ∙ z = b h} ⊆ affine hull S" apply (rule hull_mono) using that ‹z ∈ S› by auto have 2: "affine hull ⋂{S ∩ ?ab h |h. h ∈ F ∧ a h ∙ z = b h} ⊆ ⋂{?ab h |h. h ∈ F ∧ a h ∙ z = b h}" by (rule hull_minimal) (auto intro: affine_hyperplane) have 3: "ball z e ∩ ⋂{?ab h |h. h ∈ F ∧ a h ∙ z = b h} ⊆ ⋂F" by (iprover intro: sub Inter_greatest) have *: "⟦A ⊆ (B :: 'a set); A ⊆ C; E ∩ C ⊆ D⟧ ⟹ E ∩ A ⊆ (B ∩ D) ∩ C" for A B C D E by blast show ?thesis by (intro * 1 2 3) qed have "∃h. h ∈ F ∧ c ⊆ ?ab h" apply (rule face_of_polyhedron_subset_explicit [OF ‹finite F› seq faceq psub]) using assms by auto then have fac: "⋂{S ∩ ?ab h |h. h ∈ F ∧ c ⊆ S ∩ ?ab h} face_of S" using * by (force simp: ‹c ⊆ S› intro: face_of_Inter) have red: "(⋀a. P a ⟹ T ⊆ S ∩ ⋂{F x |x. P x}) ⟹ T ⊆ ⋂{S ∩ F x |x. P x}" for P T F by blast have "ball z e ∩ affine hull ⋂{S ∩ ?ab h |h. h ∈ F ∧ a h ∙ z = b h} ⊆ ⋂{S ∩ ?ab h |h. h ∈ F ∧ a h ∙ z = b h}" apply (rule red) apply (metis seq bsub) done with ‹0 < e› have zinrel: "z ∈ rel_interior (⋂{S ∩ ?ab h |h. h ∈ F ∧ z ∈ S ∧ a h ∙ z = b h})" by (auto simp: mem_rel_interior_ball ‹z ∈ S›) show ?thesis apply (rule face_of_eq [OF c fac]) using z zinrel apply (force simp: **) done qed subsection‹More general corollaries from the explicit representation› corollary facet_of_polyhedron: assumes "polyhedron S" and "c facet_of S" obtains a b where "a ≠ 0" "S ⊆ {x. a ∙ x ≤ b}" "c = S ∩ {x. a ∙ x = b}" proof - obtain F where "finite F" and seq: "S = affine hull S ∩ ⋂F" and faces: "⋀h. h ∈ F ⟹ ∃a b. a ≠ 0 ∧ h = {x. a ∙ x ≤ b}" and min: "⋀F'. F' ⊂ F ⟹ S ⊂ (affine hull S) ∩ ⋂F'" using assms by (simp add: polyhedron_Int_affine_minimal) meson then obtain a b where ab: "⋀h. h ∈ F ⟹ a h ≠ 0 ∧ h = {x. a h ∙ x ≤ b h}" by metis obtain i where "i ∈ F" and c: "c = S ∩ {x. a i ∙ x = b i}" using facet_of_polyhedron_explicit [OF ‹finite F› seq ab min] assms by force moreover have ssub: "S ⊆ {x. a i ∙ x ≤ b i}" apply (subst seq) using ‹i ∈ F› ab by auto ultimately show ?thesis by (rule_tac a = "a i" and b = "b i" in that) (simp_all add: ab) qed corollary face_of_polyhedron: assumes "polyhedron S" and "c face_of S" and "c ≠ {}" and "c ≠ S" shows "c = ⋂{F. F facet_of S ∧ c ⊆ F}" proof - obtain F where "finite F" and seq: "S = affine hull S ∩ ⋂F" and faces: "⋀h. h ∈ F ⟹ ∃a b. a ≠ 0 ∧ h = {x. a ∙ x ≤ b}" and min: "⋀F'. F' ⊂ F ⟹ S ⊂ (affine hull S) ∩ ⋂F'" using assms by (simp add: polyhedron_Int_affine_minimal) meson then obtain a b where ab: "⋀h. h ∈ F ⟹ a h ≠ 0 ∧ h = {x. a h ∙ x ≤ b h}" by metis show ?thesis apply (subst face_of_polyhedron_explicit [OF ‹finite F› seq ab min]) apply (auto simp: assms facet_of_polyhedron_explicit [OF ‹finite F› seq ab min] cong: Collect_cong) done qed lemma face_of_polyhedron_subset_facet: assumes "polyhedron S" and "c face_of S" and "c ≠ {}" and "c ≠ S" obtains F where "F facet_of S" "c ⊆ F" using face_of_polyhedron assms by (metis (no_types, lifting) Inf_greatest antisym_conv face_of_imp_subset mem_Collect_eq) lemma exposed_face_of_polyhedron: assumes "polyhedron S" shows "F exposed_face_of S ⟷ F face_of S" proof show "F exposed_face_of S ⟹ F face_of S" by (simp add: exposed_face_of_def) next assume "F face_of S" show "F exposed_face_of S" proof (cases "F = {} ∨ F = S") case True then show ?thesis using ‹F face_of S› exposed_face_of by blast next case False then have "{g. g facet_of S ∧ F ⊆ g} ≠ {}" by (metis Collect_empty_eq_bot ‹F face_of S› assms empty_def face_of_polyhedron_subset_facet) moreover have "⋀T. ⟦T facet_of S; F ⊆ T⟧ ⟹ T exposed_face_of S" by (metis assms exposed_face_of facet_of_imp_face_of facet_of_polyhedron) ultimately have "⋂{fa. fa facet_of S ∧ F ⊆ fa} exposed_face_of S" by (metis (no_types, lifting) mem_Collect_eq exposed_face_of_Inter) then show ?thesis using False apply (subst face_of_polyhedron [OF assms ‹F face_of S›], auto) done qed qed lemma face_of_polyhedron_polyhedron: fixes S :: "'a :: euclidean_space set" assumes "polyhedron S" "c face_of S" shows "polyhedron c" by (metis assms face_of_imp_eq_affine_Int polyhedron_Int polyhedron_affine_hull polyhedron_imp_convex) lemma finite_polyhedron_faces: fixes S :: "'a :: euclidean_space set" assumes "polyhedron S" shows "finite {F. F face_of S}" proof - obtain F where "finite F" and seq: "S = affine hull S ∩ ⋂F" and faces: "⋀h. h ∈ F ⟹ ∃a b. a ≠ 0 ∧ h = {x. a ∙ x ≤ b}" and min: "⋀F'. F' ⊂ F ⟹ S ⊂ (affine hull S) ∩ ⋂F'" using assms by (simp add: polyhedron_Int_affine_minimal) meson then obtain a b where ab: "⋀h. h ∈ F ⟹ a h ≠ 0 ∧ h = {x. a h ∙ x ≤ b h}" by metis have "finite {⋂{S ∩ {x. a h ∙ x = b h} |h. h ∈ F'}| F'. F' ∈ Pow F}" by (simp add: ‹finite F›) moreover have "{F. F face_of S} - {{}, S} ⊆ {⋂{S ∩ {x. a h ∙ x = b h} |h. h ∈ F'}| F'. F' ∈ Pow F}" apply clarify apply (rename_tac c) apply (drule face_of_polyhedron_explicit [OF ‹finite F› seq ab min, simplified], simp_all) apply (erule ssubst) apply (rule_tac x="{h ∈ F. c ⊆ S ∩ {x. a h ∙ x = b h}}" in exI, auto) done ultimately show ?thesis by (meson finite.emptyI finite.insertI finite_Diff2 finite_subset) qed lemma finite_polyhedron_exposed_faces: "polyhedron S ⟹ finite {F. F exposed_face_of S}" using exposed_face_of_polyhedron finite_polyhedron_faces by fastforce lemma finite_polyhedron_extreme_points: fixes S :: "'a :: euclidean_space set" shows "polyhedron S ⟹ finite {v. v extreme_point_of S}" apply (simp add: face_of_singleton [symmetric]) apply (rule finite_subset [OF _ finite_vimageI [OF finite_polyhedron_faces]], auto) done lemma finite_polyhedron_facets: fixes S :: "'a :: euclidean_space set" shows "polyhedron S ⟹ finite {F. F facet_of S}" unfolding facet_of_def by (blast intro: finite_subset [OF _ finite_polyhedron_faces]) proposition rel_interior_of_polyhedron: fixes S :: "'a :: euclidean_space set" assumes "polyhedron S" shows "rel_interior S = S - ⋃{F. F facet_of S}" proof - obtain F where "finite F" and seq: "S = affine hull S ∩ ⋂F" and faces: "⋀h. h ∈ F ⟹ ∃a b. a ≠ 0 ∧ h = {x. a ∙ x ≤ b}" and min: "⋀F'. F' ⊂ F ⟹ S ⊂ (affine hull S) ∩ ⋂F'" using assms by (simp add: polyhedron_Int_affine_minimal) meson then obtain a b where ab: "⋀h. h ∈ F ⟹ a h ≠ 0 ∧ h = {x. a h ∙ x ≤ b h}" by metis have facet: "(c facet_of S) ⟷ (∃h. h ∈ F ∧ c = S ∩ {x. a h ∙ x = b h})" for c by (rule facet_of_polyhedron_explicit [OF ‹finite F› seq ab min]) have rel: "rel_interior S = {x ∈ S. ∀h∈F. a h ∙ x < b h}" by (rule rel_interior_polyhedron_explicit [OF ‹finite F› seq ab min]) have "a h ∙ x < b h" if "x ∈ S" "h ∈ F" and xnot: "x ∉ ⋃{F. F facet_of S}" for x h proof - have "x ∈ ⋂F" using seq that by force with ‹h ∈ F› ab have "a h ∙ x ≤ b h" by auto then consider "a h ∙ x < b h" | "a h ∙ x = b h" by linarith then show ?thesis proof cases case 1 then show ?thesis . next case 2 have "Collect ((∈) x) ∉ Collect ((∈) (⋃{A. A facet_of S}))" using xnot by fastforce then have "F ∉ Collect ((∈) h)" using 2 ‹x ∈ S› facet by blast with ‹h ∈ F› have "⋂F ⊆ S ∩ {x. a h ∙ x = b h}" by blast with 2 that ‹x ∈ ⋂F› show ?thesis apply simp apply (drule_tac x="⋂F" in spec) apply (simp add: facet) apply (drule_tac x=h in spec) using seq by auto qed qed moreover have "∃h∈F. a h ∙ x ≥ b h" if "x ∈ ⋃{F. F facet_of S}" for x using that by (force simp: facet) ultimately show ?thesis by (force simp: rel) qed lemma rel_boundary_of_polyhedron: fixes S :: "'a :: euclidean_space set" assumes "polyhedron S" shows "S - rel_interior S = ⋃ {F. F facet_of S}" using facet_of_imp_subset by (fastforce simp add: rel_interior_of_polyhedron assms) lemma rel_frontier_of_polyhedron: fixes S :: "'a :: euclidean_space set" assumes "polyhedron S" shows "rel_frontier S = ⋃ {F. F facet_of S}" by (simp add: assms rel_frontier_def polyhedron_imp_closed rel_boundary_of_polyhedron) lemma rel_frontier_of_polyhedron_alt: fixes S :: "'a :: euclidean_space set" assumes "polyhedron S" shows "rel_frontier S = ⋃ {F. F face_of S ∧ (F ≠ S)}" apply (rule subset_antisym) apply (force simp: rel_frontier_of_polyhedron facet_of_def assms) using face_of_subset_rel_frontier by fastforce text‹A characterization of polyhedra as having finitely many faces› proposition polyhedron_eq_finite_exposed_faces: fixes S :: "'a :: euclidean_space set" shows "polyhedron S ⟷ closed S ∧ convex S ∧ finite {F. F exposed_face_of S}" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs by (auto simp: polyhedron_imp_closed polyhedron_imp_convex finite_polyhedron_exposed_faces) next assume ?rhs then have "closed S" "convex S" and fin: "finite {F. F exposed_face_of S}" by auto show ?lhs proof (cases "S = {}") case True then show ?thesis by auto next case False define F where "F = {h. h exposed_face_of S ∧ h ≠ {} ∧ h ≠ S}" have "finite F" by (simp add: fin F_def) have hface: "h face_of S" and "∃a b. a ≠ 0 ∧ S ⊆ {x. a ∙ x ≤ b} ∧ h = S ∩ {x. a ∙ x = b}" if "h ∈ F" for h using exposed_face_of F_def that by simp_all auto then obtain a b where ab: "⋀h. h ∈ F ⟹ a h ≠ 0 ∧ S ⊆ {x. a h ∙ x ≤ b h} ∧ h = S ∩ {x. a h ∙ x = b h}" by metis have *: "False" if paff: "p ∈ affine hull S" and "p ∉ S" and pint: "p ∈ ⋂{{x. a h ∙ x ≤ b h} |h. h ∈ F}" for p proof - have "rel_interior S ≠ {}" by (simp add: ‹S ≠ {}› ‹convex S› rel_interior_eq_empty) then obtain c where c: "c ∈ rel_interior S" by auto with rel_interior_subset have "c ∈ S" by blast have ccp: "closed_segment c p ⊆ affine hull S" by (meson affine_affine_hull affine_imp_convex c closed_segment_subset hull_subset paff rel_interior_subset subsetCE) obtain x where xcl: "x ∈ closed_segment c p" and "x ∈ S" and xnot: "x ∉ rel_interior S" using connected_openin [of "closed_segment c p"] apply simp apply (drule_tac x="closed_segment c p ∩ rel_interior S" in spec) apply (erule impE) apply (force simp: openin_rel_interior openin_Int intro: openin_subtopology_Int_subset [OF _ ccp]) apply (drule_tac x="closed_segment c p ∩ (- S)" in spec) using rel_interior_subset ‹closed S› c ‹p ∉ S› apply blast done then obtain μ where "0 ≤ μ" "μ ≤ 1" and xeq: "x = (1 - μ) *⇩_{R}c + μ *⇩_{R}p" by (auto simp: in_segment) show False proof (cases "μ=0 ∨ μ=1") case True with xeq c xnot ‹x ∈ S› ‹p ∉ S› show False by auto next case False then have xos: "x ∈ open_segment c p" using ‹x ∈ S› c open_segment_def that(2) xcl xnot by auto have xclo: "x ∈ closure S" using ‹x ∈ S› closure_subset by blast obtain d where "d ≠ 0" and dle: "⋀y. y ∈ closure S ⟹ d ∙ x ≤ d ∙ y" and dless: "⋀y. y ∈ rel_interior S ⟹ d ∙ x < d ∙ y" by (metis supporting_hyperplane_relative_frontier [OF ‹convex S› xclo xnot]) have sex: "S ∩ {y. d ∙ y = d ∙ x} exposed_face_of S" by (simp add: ‹closed S› dle exposed_face_of_Int_supporting_hyperplane_ge [OF ‹convex S›]) have sne: "S ∩ {y. d ∙ y = d ∙ x} ≠ {}" using ‹x ∈ S› by blast have sns: "S ∩ {y. d ∙ y = d ∙ x} ≠ S" by (metis (mono_tags) Int_Collect c subsetD dless not_le order_refl rel_interior_subset) obtain h where "h ∈ F" "x ∈ h" apply (rule_tac h="S ∩ {y. d ∙ y = d ∙ x}" in that) apply (simp_all add: F_def sex sne sns ‹x ∈ S›) done have abface: "{y. a h ∙ y = b h} face_of {y. a h ∙ y ≤ b h}" using hyperplane_face_of_halfspace_le by blast then have "c ∈ h" using face_ofD [OF abface xos] ‹c ∈ S› ‹h ∈ F› ab pint ‹x ∈ h› by blast with c have "h ∩ rel_interior S ≠ {}" by blast then show False using ‹h ∈ F› F_def face_of_disjoint_rel_interior hface by auto qed qed have "S ⊆ affine hull S ∩ ⋂{{x. a h ∙ x ≤ b h} |h. h ∈ F}" using ab by (auto simp: hull_subset) moreover have "affine hull S ∩ ⋂{{x. a h ∙ x ≤ b h} |h. h ∈ F} ⊆ S" using * by blast ultimately have "S = affine hull S ∩ ⋂ {{x. a h ∙ x ≤ b h} |h. h ∈ F}" .. then show ?thesis apply (rule ssubst) apply (force intro: polyhedron_affine_hull polyhedron_halfspace_le simp: ‹finite F›) done qed qed corollary polyhedron_eq_finite_faces: fixes S :: "'a :: euclidean_space set" shows "polyhedron S ⟷ closed S ∧ convex S ∧ finite {F. F face_of S}" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs by (simp add: finite_polyhedron_faces polyhedron_imp_closed polyhedron_imp_convex) next assume ?rhs then show ?lhs by (force simp: polyhedron_eq_finite_exposed_faces exposed_face_of intro: finite_subset) qed lemma polyhedron_linear_image_eq: fixes h :: "'a :: euclidean_space ⇒ 'b :: euclidean_space" assumes "linear h" "bij h" shows "polyhedron (h ` S) ⟷ polyhedron S" proof - have *: "{f. P f} = (image h) ` {f. P (h ` f)}" for P apply safe apply (rule_tac x="inv h ` x" in image_eqI) apply (auto simp: ‹bij h› bij_is_surj image_f_inv_f) done have "inj h" using bij_is_inj assms by blast then have injim: "inj_on ((`) h) A" for A by (simp add: inj_on_def inj_image_eq_iff) show ?thesis using ‹linear h› ‹inj h› apply (simp add: polyhedron_eq_finite_faces closed_injective_linear_image_eq) apply (simp add: * face_of_linear_image [of h _ S, symmetric] finite_image_iff injim) done qed lemma polyhedron_negations: fixes S :: "'a :: euclidean_space set" shows "polyhedron S ⟹ polyhedron(image uminus S)" by (subst polyhedron_linear_image_eq) (auto simp: bij_uminus intro!: linear_uminus) subsection‹Relation between polytopes and polyhedra› lemma polytope_eq_bounded_polyhedron: fixes S :: "'a :: euclidean_space set" shows "polytope S ⟷ polyhedron S ∧ bounded S" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs by (simp add: finite_polytope_faces polyhedron_eq_finite_faces polytope_imp_closed polytope_imp_convex polytope_imp_bounded) next assume ?rhs then show ?lhs unfolding polytope_def apply (rule_tac x="{v. v extreme_point_of S}" in exI) apply (simp add: finite_polyhedron_extreme_points Krein_Milman_Minkowski compact_eq_bounded_closed polyhedron_imp_closed polyhedron_imp_convex) done qed lemma polytope_Int: fixes S :: "'a :: euclidean_space set" shows "⟦polytope S; polytope T⟧ ⟹ polytope(S ∩ T)" by (simp add: polytope_eq_bounded_polyhedron bounded_Int) lemma polytope_Int_polyhedron: fixes S :: "'a :: euclidean_space set" shows "⟦polytope S; polyhedron T⟧ ⟹ polytope(S ∩ T)" by (simp add: bounded_Int polytope_eq_bounded_polyhedron) lemma polyhedron_Int_polytope: fixes S :: "'a :: euclidean_space set" shows "⟦polyhedron S; polytope T⟧ ⟹ polytope(S ∩ T)" by (simp add: bounded_Int polytope_eq_bounded_polyhedron) lemma polytope_imp_polyhedron: fixes S :: "'a :: euclidean_space set" shows "polytope S ⟹ polyhedron S" by (simp add: polytope_eq_bounded_polyhedron) lemma polytope_facet_exists: fixes p :: "'a :: euclidean_space set" assumes "polytope p" "0 < aff_dim p" obtains F where "F facet_of p" proof (cases "p = {}") case True with assms show ?thesis by auto next case False then obtain v where "v extreme_point_of p" using extreme_point_exists_convex by (blast intro: ‹polytope p› polytope_imp_compact polytope_imp_convex) then show ?thesis by (metis face_of_polyhedron_subset_facet polytope_imp_polyhedron aff_dim_sing all_not_in_conv assms face_of_singleton less_irrefl singletonI that) qed lemma polyhedron_interval [iff]: "polyhedron(cbox a b)" by (metis polytope_imp_polyhedron polytope_interval) lemma polyhedron_convex_hull: fixes S :: "'a :: euclidean_space set" shows "finite S ⟹ polyhedron(convex hull S)" by (simp add: polytope_convex_hull polytope_imp_polyhedron) subsection‹Relative and absolute frontier of a polytope› lemma rel_boundary_of_convex_hull: fixes S :: "'a::euclidean_space set" assumes "~ affine_dependent S" shows "(convex hull S) - rel_interior(convex hull S) = (⋃a∈S. convex hull (S - {a}))" proof - have "finite S" by (metis assms aff_independent_finite) then consider "card S = 0" | "card S = 1" | "2 ≤ card S" by arith then show ?thesis proof cases case 1 then have "S = {}" by (simp add: ‹finite S›) then show ?thesis by simp next case 2 show ?thesis by (auto intro: card_1_singletonE [OF ‹card S = 1›]) next case 3 with assms show ?thesis by (auto simp: polyhedron_convex_hull rel_boundary_of_polyhedron facet_of_convex_hull_affine_independent_alt ‹finite S›) qed qed proposition frontier_of_convex_hull: fixes S :: "'a::euclidean_space set" assumes "card S = Suc (DIM('a))" shows "frontier(convex hull S) = ⋃ {convex hull (S - {a}) | a. a ∈ S}" proof (cases "affine_dependent S") case True have [iff]: "finite S" using assms using card_infinite by force then have ccs: "closed (convex hull S)" by (simp add: compact_imp_closed finite_imp_compact_convex_hull) { fix x T assume "finite T" "T ⊆ S" "int (card T) ≤ aff_dim S + 1" "x ∈ convex hull T" then have "S ≠ T" using True ‹finite S› aff_dim_le_card affine_independent_iff_card by fastforce then obtain a where "a ∈ S" "a ∉ T" using ‹T ⊆ S› by blast then have "x ∈ (⋃a∈S. convex hull (S - {a}))" using True affine_independent_iff_card [of S] apply simp apply (metis (no_types, hide_lams) Diff_eq_empty_iff Diff_insert0 ‹a ∉ T› ‹T ⊆ S› ‹x ∈ convex hull T› hull_mono insert_Diff_single subsetCE) done } note * = this have 1: "convex hull S ⊆ (⋃ a∈S. convex hull (S - {a}))" apply (subst caratheodory_aff_dim) apply (blast intro: *) done have 2: "⋃((λa. convex hull (S - {a})) ` S) ⊆ convex hull S" by (rule Union_least) (metis (no_types, lifting) Diff_subset hull_mono imageE) show ?thesis using True apply (simp add: segment_convex_hull frontier_def) using interior_convex_hull_eq_empty [OF assms] apply (simp add: closure_closed [OF ccs]) apply (rule subset_antisym) using 1 apply blast using 2 apply blast done next case False then have "frontier (convex hull S) = (convex hull S) - rel_interior(convex hull S)" apply (simp add: rel_boundary_of_convex_hull [symmetric] frontier_def) 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) also have "... = ⋃{convex hull (S - {a}) |a. a ∈ S}" proof - have "convex hull S - rel_interior (convex hull S) = rel_frontier (convex hull S)" by (simp add: False aff_independent_finite polyhedron_convex_hull rel_boundary_of_polyhedron rel_frontier_of_polyhedron) then show ?thesis by (simp add: False rel_frontier_convex_hull_cases) qed finally show ?thesis . qed subsection‹Special case of a triangle› proposition frontier_of_triangle: fixes a :: "'a::euclidean_space" assumes "DIM('a) = 2" shows "frontier(convex hull {a,b,c}) = closed_segment a b ∪ closed_segment b c ∪ closed_segment c a" (is "?lhs = ?rhs") proof (cases "b = a ∨ c = a ∨ c = b") case True then show ?thesis by (auto simp: assms segment_convex_hull frontier_def empty_interior_convex_hull insert_commute card_insert_le_m1 hull_inc insert_absorb) next case False then have [simp]: "card {a, b, c} = Suc (DIM('a))" by (simp add: card_insert Set.insert_Diff_if assms) show ?thesis proof show "?lhs ⊆ ?rhs" using False by (force simp: segment_convex_hull frontier_of_convex_hull insert_Diff_if insert_commute split: if_split_asm) show "?rhs ⊆ ?lhs" using False apply (simp add: frontier_of_convex_hull segment_convex_hull) apply (intro conjI subsetI) apply (rule_tac X="convex hull {a,b}" in UnionI; force simp: Set.insert_Diff_if) apply (rule_tac X="convex hull {b,c}" in UnionI; force) apply (rule_tac X="convex hull {a,c}" in UnionI; force simp: insert_commute Set.insert_Diff_if) done qed qed corollary inside_of_triangle: fixes a :: "'a::euclidean_space" assumes "DIM('a) = 2" shows "inside (closed_segment a b ∪ closed_segment b c ∪ closed_segment c a) = interior(convex hull {a,b,c})" by (metis assms frontier_of_triangle bounded_empty bounded_insert convex_convex_hull inside_frontier_eq_interior bounded_convex_hull) corollary interior_of_triangle: fixes a :: "'a::euclidean_space" assumes "DIM('a) = 2" shows "interior(convex hull {a,b,c}) = convex hull {a,b,c} - (closed_segment a b ∪ closed_segment b c ∪ closed_segment c a)" using interior_subset by (force simp: frontier_of_triangle [OF assms, symmetric] frontier_def Diff_Diff_Int) subsection‹Subdividing a cell complex› lemma subdivide_interval: fixes x::real assumes "a < ¦x - y¦" "0 < a" obtains n where "n ∈ ℤ" "x < n * a ∧ n * a < y ∨ y < n * a ∧ n * a < x" proof - consider "a + x < y" | "a + y < x" using assms by linarith then show ?thesis proof cases case 1 let ?n = "of_int (floor (x/a)) + 1" have x: "x < ?n * a" by (meson ‹0 < a› divide_less_eq floor_eq_iff) have "?n * a ≤ a + x" apply (simp add: algebra_simps) by (metis ‹0 < a› floor_correct less_irrefl nonzero_mult_div_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right) also have "... < y" by (rule 1) finally have "?n * a < y" . with x show ?thesis using Ints_1 Ints_add Ints_of_int that by blast next case 2 let ?n = "of_int (floor (y/a)) + 1" have y: "y < ?n * a" by (meson ‹0 < a› divide_less_eq floor_eq_iff) have "?n * a ≤ a + y" apply (simp add: algebra_simps) by (metis ‹0 < a› floor_correct less_irrefl nonzero_mult_div_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right) also have "... < x" by (rule 2) finally have "?n * a < x" . then show ?thesis using Ints_1 Ints_add Ints_of_int that y by blast qed qed lemma cell_subdivision_lemma: assumes "finite ℱ" and "⋀X. X ∈ ℱ ⟹ polytope X" and "⋀X. X ∈ ℱ ⟹ aff_dim X ≤ d" and "⋀X Y. ⟦X ∈ ℱ; Y ∈ ℱ⟧ ⟹ (X ∩ Y) face_of X ∧ (X ∩ Y) face_of Y" and "finite I" shows "∃𝒢. ⋃𝒢 = ⋃ℱ ∧ finite 𝒢 ∧ (∀C ∈ 𝒢. ∃D. D ∈ ℱ ∧ C ⊆ D) ∧ (∀C ∈ ℱ. ∀x ∈ C. ∃D. D ∈ 𝒢 ∧ x ∈ D ∧ D ⊆ C) ∧ (∀X ∈ 𝒢. polytope X) ∧ (∀X ∈ 𝒢. aff_dim X ≤ d) ∧ (∀X ∈ 𝒢. ∀Y ∈ 𝒢. X ∩ Y face_of X ∧ X ∩ Y face_of Y) ∧ (∀X ∈ 𝒢. ∀x ∈ X. ∀y ∈ X. ∀a b. (a,b) ∈ I ⟶ a ∙ x ≤ b ∧ a ∙ y ≤ b ∨ a ∙ x ≥ b ∧ a ∙ y ≥ b)" using ‹finite I› proof induction case empty then show ?case by (rule_tac x="ℱ" in exI) (auto simp: assms) next case (insert ab I) then obtain 𝒢 where eq: "⋃𝒢 = ⋃ℱ" and "finite 𝒢" and sub1: "⋀C. C ∈ 𝒢 ⟹ ∃D. D ∈ ℱ ∧ C ⊆ D" and sub2: "⋀C x. C ∈ ℱ ∧ x ∈ C ⟹ ∃D. D ∈ 𝒢 ∧ x ∈ D ∧ D ⊆ C" and poly: "⋀X. X ∈ 𝒢 ⟹ polytope X" and aff: "⋀X. X ∈ 𝒢 ⟹ aff_dim X ≤ d" and face: "⋀X Y. ⟦X ∈ 𝒢; Y ∈ 𝒢⟧ ⟹ X ∩ Y face_of X ∧ X ∩ Y face_of Y" and I: "⋀X x y a b. ⟦X ∈ 𝒢; x ∈ X; y ∈ X; (a,b) ∈ I⟧ ⟹ a ∙ x ≤ b ∧ a ∙ y ≤ b ∨ a ∙ x ≥ b ∧ a ∙ y ≥ b" by (auto simp: that) obtain a b where "ab = (a,b)" by fastforce let ?𝒢 = "(λX. X ∩ {x. a ∙ x ≤ b}) ` 𝒢 ∪ (λX. X ∩ {x. a ∙ x ≥ b}) ` 𝒢" have eqInt: "(S ∩ Collect P) ∩ (T ∩ Collect Q) = (S ∩ T) ∩ (Collect P ∩ Collect Q)" for S T::"'a set" and P Q by blast show ?case proof (intro conjI exI) show "⋃?𝒢 = ⋃ℱ" by (force simp: eq [symmetric]) show "finite ?𝒢" using ‹finite 𝒢› by force show "∀X ∈ ?𝒢. polytope X" by (force simp: poly polytope_Int_polyhedron polyhedron_halfspace_le polyhedron_halfspace_ge) show "∀X ∈ ?𝒢. aff_dim X ≤ d" by (auto; metis order_trans aff aff_dim_subset inf_le1) show "∀X ∈ ?𝒢. ∀x ∈ X. ∀y ∈ X. ∀a b. (a,b) ∈ insert ab I ⟶ a ∙ x ≤ b ∧ a ∙ y ≤ b ∨ a ∙ x ≥ b ∧ a ∙ y ≥ b" using ‹ab = (a, b)› I by fastforce show "∀X ∈ ?𝒢. ∀Y ∈ ?𝒢. X ∩ Y face_of X ∧ X ∩ Y face_of Y" by (auto simp: eqInt halfspace_Int_eq face_of_Int_Int face face_of_halfspace_le face_of_halfspace_ge) show "∀C ∈ ?𝒢. ∃D. D ∈ ℱ ∧ C ⊆ D" using sub1 by force show "∀C∈ℱ. ∀x∈C. ∃D. D ∈ ?𝒢 ∧ x ∈ D ∧ D ⊆ C" proof (intro ballI) fix C z assume "C ∈ ℱ" "z ∈ C" with sub2 obtain D where D: "D ∈ 𝒢" "z ∈ D" "D ⊆ C" by blast have "D ∈ 𝒢 ∧ z ∈ D ∩ {x. a ∙ x ≤ b} ∧ D ∩ {x. a ∙ x ≤ b} ⊆ C ∨ D ∈ 𝒢 ∧ z ∈ D ∩ {x. a ∙ x ≥ b} ∧ D ∩ {x. a ∙ x ≥ b} ⊆ C" using linorder_class.linear [of "a ∙ z" b] D by blast then show "∃D. D ∈ ?𝒢 ∧ z ∈ D ∧ D ⊆ C" by blast qed qed qed proposition cell_complex_subdivision_exists: fixes ℱ :: "'a::euclidean_space set set" assumes "0 < e" "finite ℱ" and poly: "⋀X. X ∈ ℱ ⟹ polytope X" and aff: "⋀X. X ∈ ℱ ⟹ aff_dim X ≤ d" and face: "⋀X Y. ⟦X ∈ ℱ; Y ∈ ℱ⟧ ⟹ X ∩ Y face_of X ∧ X ∩ Y face_of Y" obtains "ℱ'" where "finite ℱ'" "⋃ℱ' = ⋃ℱ" "⋀X. X ∈ ℱ' ⟹ diameter X < e" "⋀X. X ∈ ℱ' ⟹ polytope X" "⋀X. X ∈ ℱ' ⟹ aff_dim X ≤ d" "⋀X Y. ⟦X ∈ ℱ'; Y ∈ ℱ'⟧ ⟹ X ∩ Y face_of X ∧ X ∩ Y face_of Y" "⋀C. C ∈ ℱ' ⟹ ∃D. D ∈ ℱ ∧ C ⊆ D" "⋀C x. C ∈ ℱ ∧ x ∈ C ⟹ ∃D. D ∈ ℱ' ∧ x ∈ D ∧ D ⊆ C" proof - have "bounded(⋃ℱ)" by (simp add: ‹finite ℱ› poly bounded_Union polytope_imp_bounded) then obtain B where "B > 0" and B: "⋀x. x ∈ ⋃ℱ ⟹ norm x < B" by (meson bounded_pos_less) define C where "C ≡ {z ∈ ℤ. ¦z * e / 2 / real DIM('a)¦ ≤ B}" define I where "I ≡ ⋃i ∈ Basis. ⋃j ∈ C. { (i::'a, j * e / 2 / DIM('a)) }" have "finite C" using finite_int_segment [of "-B / (e / 2 / DIM('a))" "B / (e / 2 / DIM('a))"] apply (simp add: C_def) apply (erule rev_finite_subset) using ‹0 < e› apply (auto simp: divide_simps) done then have "finite I" by (simp add: I_def) obtain ℱ' where eq: "⋃ℱ' = ⋃ℱ" and "finite ℱ'" and poly: "⋀X. X ∈ ℱ' ⟹ polytope X" and aff: "⋀X. X ∈ ℱ' ⟹ aff_dim X ≤ d" and face: "⋀X Y. ⟦X ∈ ℱ'; Y ∈ ℱ'⟧ ⟹ X ∩ Y face_of X ∧ X ∩ Y face_of Y" and I: "⋀X x y a b. ⟦X ∈ ℱ'; x ∈ X; y ∈ X; (a,b) ∈ I⟧ ⟹ a ∙ x ≤ b ∧ a ∙ y ≤ b ∨ a ∙ x ≥ b ∧ a ∙ y ≥ b" and sub1: "⋀C. C ∈ ℱ' ⟹ ∃D. D ∈ ℱ ∧ C ⊆ D" and sub2: "⋀C x. C ∈ ℱ ∧ x ∈ C ⟹ ∃D. D ∈ ℱ' ∧ x ∈ D ∧ D ⊆ C" apply (rule exE [OF cell_subdivision_lemma]) using assms ‹finite I› apply auto done show ?thesis proof (rule_tac ℱ'="ℱ'" in that) show "diameter X < e" if "X ∈ ℱ'" for X proof - have "diameter X ≤ e/2" proof (rule diameter_le) show "norm (x - y) ≤ e / 2" if "x ∈ X" "y ∈ X" for x y proof - have "norm x < B" "norm y < B" using B ‹X ∈ ℱ'› eq that by fastforce+ have "norm (x - y) ≤ (∑b∈Basis. ¦(x-y) ∙ b¦)" by (rule norm_le_l1) also have "... ≤ of_nat (DIM('a)) * (e / 2 / DIM('a))" proof (rule sum_bounded_above) fix i::'a assume "i ∈ Basis" then have I': "⋀z b. ⟦z ∈ C; b = z * e / (2 * real DIM('a))⟧ ⟹ i ∙ x ≤ b ∧ i ∙ y ≤ b ∨ i ∙ x ≥ b ∧ i ∙ y ≥ b" using I ‹X ∈ ℱ'› that by (fastforce simp: I_def) show "¦(x - y) ∙ i¦ ≤ e / 2 / real DIM('a)" proof (rule ccontr) assume "¬ ¦(x - y) ∙ i¦ ≤ e / 2 / real DIM('a)" then have xyi: "¦i ∙ x - i ∙ y¦ > e / 2 / real DIM('a)" by (simp add: inner_commute inner_diff_right) obtain n where "n ∈ ℤ" and n: "i ∙ x < n * (e / 2 / real DIM('a)) ∧ n * (e / 2 / real DIM('a)) < i ∙ y ∨ i ∙ y < n * (e / 2 / real DIM('a)) ∧ n * (e / 2 / real DIM('a)) < i ∙ x" using subdivide_interval [OF xyi] DIM_positive ‹0 < e› by (auto simp: zero_less_divide_iff) have "¦i ∙ x¦ < B" by (metis ‹i ∈ Basis› ‹norm x < B› inner_commute norm_bound_Basis_lt) have "¦i ∙ y¦ < B" by (metis ‹i ∈ Basis› ‹norm y < B› inner_commute norm_bound_Basis_lt) have *: "¦n * e¦ ≤ B * (2 * real DIM('a))" if "¦ix¦ < B" "¦iy¦ < B" and ix: "ix * (2 * real DIM('a)) < n * e" and iy: "n * e < iy * (2 * real DIM('a))" for ix iy proof (rule abs_leI) have "iy * (2 * real DIM('a)) ≤ B * (2 * real DIM('a))" by (rule mult_right_mono) (use ‹¦iy¦ < B› in linarith)+ then show "n * e ≤ B * (2 * real DIM('a))" using iy by linarith next have "- ix * (2 * real DIM('a)) ≤ B * (2 * real DIM('a))" by (rule mult_right_mono) (use ‹¦ix¦ < B› in linarith)+ then show "- (n * e) ≤ B * (2 * real DIM('a))" using ix by linarith qed have "n ∈ C" using ‹n ∈ ℤ› n by (auto simp: C_def divide_simps intro: * ‹¦i ∙ x¦ < B› ‹¦i ∙ y¦ < B›) show False using I' [OF ‹n ∈ C› refl] n by auto qed qed also have "... = e / 2" by simp finally show ?thesis . qed qed (use ‹0 < e› in force) also have "... < e" by (simp add: ‹0 < e›) finally show ?thesis . qed qed (auto simp: eq poly aff face sub1 sub2 ‹finite ℱ'›) qed subsection‹Simplexes› text‹The notion of n-simplex for integer @{term"n ≥ -1"}› definition simplex :: "int ⇒ 'a::euclidean_space set ⇒ bool" (infix "simplex" 50) where "n simplex S ≡ ∃C. ~(affine_dependent C) ∧ int(card C) = n + 1 ∧ S = convex hull C" lemma simplex: "n simplex S ⟷ (∃C. finite C ∧ ~(affine_dependent C) ∧ int(card C) = n + 1 ∧ S = convex hull C)" by (auto simp add: simplex_def intro: aff_independent_finite) lemma simplex_convex_hull: "~affine_dependent C ∧ int(card C) = n + 1 ⟹ n simplex (convex hull C)" by (auto simp add: simplex_def) lemma convex_simplex: "n simplex S ⟹ convex S" by (metis convex_convex_hull simplex_def) lemma compact_simplex: "n simplex S ⟹ compact S" unfolding simplex using finite_imp_compact_convex_hull by blast lemma closed_simplex: "n simplex S ⟹ closed S" by (simp add: compact_imp_closed compact_simplex) lemma simplex_imp_polytope: "n simplex S ⟹ polytope S" unfolding simplex_def polytope_def using aff_independent_finite by blast lemma simplex_imp_polyhedron: "n simplex S ⟹ polyhedron S" by (simp add: polytope_imp_polyhedron simplex_imp_polytope) lemma simplex_dim_ge: "n simplex S ⟹ -1 ≤ n" by (metis (no_types, hide_lams) aff_dim_geq affine_independent_iff_card diff_add_cancel diff_diff_eq2 simplex_def) lemma simplex_empty [simp]: "n simplex {} ⟷ n = -1" proof assume "n simplex {}" then show "n = -1" unfolding simplex by (metis card_empty convex_hull_eq_empty diff_0 diff_eq_eq of_nat_0) next assume "n = -1" then show "n simplex {}" by (fastforce simp: simplex) qed lemma simplex_minus_1 [simp]: "-1 simplex S ⟷ S = {}" by (metis simplex cancel_comm_monoid_add_class.diff_cancel card_0_eq diff_minus_eq_add of_nat_eq_0_iff simplex_empty) lemma aff_dim_simplex: "n simplex S ⟹ aff_dim S = n" by (metis simplex add.commute add_diff_cancel_left' aff_dim_convex_hull affine_independent_iff_card) lemma zero_simplex_sing: "0 simplex {a}" apply (simp add: simplex_def) by (metis affine_independent_1 card_empty card_insert_disjoint convex_hull_singleton empty_iff finite.emptyI) lemma simplex_sing [simp]: "n simplex {a} ⟷ n = 0" using aff_dim_simplex aff_dim_sing zero_simplex_sing by blast lemma simplex_zero: "0 simplex S ⟷ (∃a. S = {a})" apply (auto simp: ) using aff_dim_eq_0 aff_dim_simplex by blast lemma one_simplex_segment: "a ≠ b ⟹ 1 simplex closed_segment a b" apply (simp add: simplex_def) apply (rule_tac x="{a,b}" in exI) apply (auto simp: segment_convex_hull) done lemma simplex_segment_cases: "(if a = b then 0 else 1) simplex closed_segment a b" by (auto simp: one_simplex_segment) lemma simplex_segment: "∃n. n simplex closed_segment a b" using simplex_segment_cases by metis lemma polytope_lowdim_imp_simplex: assumes "polytope P" "aff_dim P ≤ 1" obtains n where "n simplex P" proof (cases "P = {}") case True then show ?thesis by (simp add: that) next case False then show ?thesis by (metis assms compact_convex_collinear_segment collinear_aff_dim polytope_imp_compact polytope_imp_convex simplex_segment_cases that) qed lemma simplex_insert_dimplus1: fixes n::int assumes "n simplex S" and a: "a ∉ affine hull S" shows "(n+1) simplex (convex hull (insert a S))" proof - obtain C where C: "finite C" "~(affine_dependent C)" "int(card C) = n+1" and S: "S = convex hull C" using assms unfolding simplex by force show ?thesis unfolding simplex proof (intro exI conjI) have "aff_dim S = n" using aff_dim_simplex assms(1) by blast moreover have "a ∉ affine hull C" using S a affine_hull_convex_hull by blast moreover have "a ∉ C" using S a hull_inc by fastforce ultimately show "¬ affine_dependent (insert a C)" by (simp add: C S aff_dim_convex_hull aff_dim_insert affine_independent_iff_card) next have "a ∉ C" using S a hull_inc by fastforce then show "int (card (insert a C)) = n + 1 + 1" by (simp add: C) next show "convex hull insert a S = convex hull (insert a C)" by (simp add: S convex_hull_insert_segments) qed (use C in auto) qed subsection‹Simplicial complexes and triangulations› definition simplicial_complex where "simplicial_complex 𝒞 ≡ finite 𝒞 ∧ (∀S ∈ 𝒞. ∃n. n simplex S) ∧ (∀F S. S ∈ 𝒞 ∧ F face_of S ⟶ F ∈ 𝒞) ∧ (∀S S'. S ∈ 𝒞 ∧ S' ∈ 𝒞 ⟶ (S ∩ S') face_of S ∧ (S ∩ S') face_of S')" definition triangulation where "triangulation 𝒯 ≡ finite 𝒯 ∧ (∀T ∈ 𝒯. ∃n. n simplex T) ∧ (∀T T'. T ∈ 𝒯 ∧ T' ∈ 𝒯 ⟶ (T ∩ T') face_of T ∧ (T ∩ T') face_of T')" subsection‹Refining a cell complex to a simplicial complex› lemma convex_hull_insert_Int_eq: fixes z :: "'a :: euclidean_space" assumes z: "z ∈ rel_interior S" and T: "T ⊆ rel_frontier S" and U: "U ⊆ rel_frontier S" and "convex S" "convex T" "convex U" shows "convex hull (insert z T) ∩ convex hull (insert z U) = convex hull (insert z (T ∩ U))" (is "?lhs = ?rhs") proof show "?lhs ⊆ ?rhs" proof (cases "T={} ∨ U={}") case True then show ?thesis by auto next case False then have "T ≠ {}" "U ≠ {}" by auto have TU: "convex (T ∩ U)" by (simp add: ‹convex T› ‹convex U› convex_Int) have "(⋃x∈T. closed_segment z x) ∩ (⋃x∈U. closed_segment z x) ⊆ (if T ∩ U = {} then {z} else UNION (T ∩ U) (closed_segment z))" (is "_ ⊆ ?IF") proof clarify fix x t u assume xt: "x ∈ closed_segment z t" and xu: "x ∈ closed_segment z u" and "t ∈ T" "u ∈ U" then have ne: "t ≠ z" "u ≠ z" using T U z unfolding rel_frontier_def by blast+ show "x ∈ ?IF" proof (cases "x = z") case True then show ?thesis by auto next case False have t: "t ∈ closure S" using T ‹t ∈ T› rel_frontier_def by auto have u: "u ∈ closure S" using U ‹u ∈ U› rel_frontier_def by auto show ?thesis proof (cases "t = u") case True then show ?thesis using ‹t ∈ T› ‹u ∈ U› xt by auto next case False have tnot: "t ∉ closed_segment u z" proof - have "t ∈ closure S - rel_interior S" using T ‹t ∈ T› rel_frontier_def by blast then have "t ∉ open_segment z u" by (meson DiffD2 rel_interior_closure_convex_segment [OF ‹convex S› z u] subsetD) then show ?thesis by (simp add: ‹t ≠ u› ‹t ≠ z› open_segment_commute open_segment_def) qed moreover have "u ∉ closed_segment z t" using rel_interior_closure_convex_segment [OF ‹convex S› z t] ‹u ∈ U› ‹u ≠ z› U [unfolded rel_frontier_def] tnot by (auto simp: closed_segment_eq_open) ultimately have "~(between (t,u) z | between (u,z) t | between (z,t) u)" if "x ≠ z" using that xt xu apply (simp add: between_mem_segment [symmetric]) by (metis between_commute between_trans_2 between_antisym) then have "~ collinear {t, z, u}" if "x ≠ z" by (auto simp: that collinear_between_cases between_commute) moreover have "collinear {t, z, x}" by (metis closed_segment_commute collinear_2 collinear_closed_segment collinear_triples ends_in_segment(1) insert_absorb insert_absorb2 xt) moreover have "collinear {z, x, u}" by (metis closed_segment_commute collinear_2 collinear_closed_segment collinear_triples ends_in_segment(1) insert_absorb insert_absorb2 xu) ultimately have False using collinear_3_trans [of t z x u] ‹x ≠ z› by blast then show ?thesis by metis qed qed qed then show ?thesis using False ‹convex T› ‹convex U› TU by (simp add: convex_hull_insert_segments hull_same split: if_split_asm) qed show "?rhs ⊆ ?lhs" by (metis inf_greatest hull_mono inf.cobounded1 inf.cobounded2 insert_mono) qed lemma simplicial_subdivision_aux: assumes "finite ℳ" and "⋀C. C ∈ ℳ ⟹ polytope C" and "⋀C. C ∈ ℳ ⟹ aff_dim C ≤ of_nat n" and "⋀C F. ⟦C ∈ ℳ; F face_of C⟧ ⟹ F ∈ ℳ" and "⋀C1 C2. ⟦C1 ∈ ℳ; C2 ∈ ℳ⟧ ⟹ C1 ∩ C2 face_of C1 ∧ C1 ∩ C2 face_of C2" shows "∃𝒯. simplicial_complex 𝒯 ∧ (∀K ∈ 𝒯. aff_dim K ≤ of_nat n) ∧ ⋃𝒯 = ⋃ℳ ∧ (∀C ∈ ℳ. ∃F. finite F ∧ F ⊆ 𝒯 ∧ C = ⋃F) ∧ (∀K ∈ 𝒯. ∃C. C ∈ ℳ ∧ K ⊆ C)" using assms proof (induction n arbitrary: ℳ rule: less_induct) case (less n) then have polyℳ: "⋀C. C ∈ ℳ ⟹ polytope C" and affℳ: "⋀C. C ∈ ℳ ⟹ aff_dim C ≤ of_nat n" and faceℳ: "⋀C F. ⟦C ∈ ℳ; F face_of C⟧ ⟹ F ∈ ℳ" and intfaceℳ: "⋀C1 C2. ⟦C1 ∈ ℳ; C2 ∈ ℳ⟧ ⟹ C1 ∩ C2 face_of C1 ∧ C1 ∩ C2 face_of C2" by metis+ show ?case proof (cases "n ≤ 1") case True have "⋀s. ⟦n ≤ 1; s ∈ ℳ⟧ ⟹ ∃m. m simplex s" using polyℳ affℳ by (force intro: polytope_lowdim_imp_simplex) then show ?thesis unfolding simplicial_complex_def apply (rule_tac x="ℳ" in exI) using True by (auto simp: less.prems) next case False define 𝒮 where "𝒮 ≡ {C ∈ ℳ. aff_dim C < n}" have "finite 𝒮" "⋀C. C ∈ 𝒮 ⟹ polytope C" "⋀C. C ∈ 𝒮 ⟹ aff_dim C ≤ int (n - 1)" "⋀C F. ⟦C ∈ 𝒮; F face_of C⟧ ⟹ F ∈ 𝒮" "⋀C1 C2. ⟦C1 ∈ 𝒮; C2 ∈ 𝒮⟧ ⟹ C1 ∩ C2 face_of C1 ∧ C1 ∩ C2 face_of C2" using less.prems apply (auto simp: 𝒮_def) by (metis aff_dim_subset face_of_imp_subset less_le not_le) with less.IH [of "n-1" 𝒮] False obtain 𝒰 where "simplicial_complex 𝒰" and aff_dim𝒰: "⋀K. K ∈ 𝒰 ⟹ aff_dim K ≤ int (n - 1)" and "⋃𝒰 = ⋃𝒮" and fin𝒰: "⋀C. C ∈ 𝒮 ⟹ ∃F. finite F ∧ F ⊆ 𝒰 ∧ C = ⋃F" and C𝒰: "⋀K. K ∈ 𝒰 ⟹ ∃C. C ∈ 𝒮 ∧ K ⊆ C" by auto then have "finite 𝒰" and simpl𝒰: "⋀S. S ∈ 𝒰 ⟹ ∃n. n simplex S" and face𝒰: "⋀F S. ⟦S ∈ 𝒰; F face_of S⟧ ⟹ F ∈ 𝒰" and faceI𝒰: "⋀S S'. ⟦S ∈ 𝒰; S' ∈ 𝒰⟧ ⟹ (S ∩ S') face_of S ∧ (S ∩ S') face_of S'" by (auto simp: simplicial_complex_def) define 𝒩 where "𝒩 ≡ {C ∈ ℳ. aff_dim C = n}" have "finite 𝒩" by (simp add: 𝒩_def less.prems(1)) have poly𝒩: "⋀C. C ∈ 𝒩 ⟹ polytope C" and convex𝒩: "⋀C. C ∈ 𝒩 ⟹ convex C" and closed𝒩: "⋀C. C ∈ 𝒩 ⟹ closed C" by (auto simp: 𝒩_def polyℳ polytope_imp_convex polytope_imp_closed) have in_rel_interior: "(SOME z. z ∈ rel_interior C) ∈ rel_interior C" if "C ∈ 𝒩" for C using that polyℳ polytope_imp_convex rel_interior_aff_dim some_in_eq by (fastforce simp: 𝒩_def) have *: "∃T. ~affine_dependent T ∧ card T ≤ n ∧ aff_dim K < n ∧ K = convex hull T" if "K ∈ 𝒰" for K proof - obtain r where r: "r simplex K" using ‹K ∈ 𝒰› simpl𝒰 by blast have "r = aff_dim K" using ‹r simplex K› aff_dim_simplex by blast with r show ?thesis unfolding simplex_def using False ‹⋀K. K ∈ 𝒰 ⟹ aff_dim K ≤ int (n - 1)› that by fastforce qed have ahK_C_disjoint: "affine hull K ∩ rel_interior C = {}" if "C ∈ 𝒩" "K ∈ 𝒰" "K ⊆ rel_frontier C" for C K proof - have "convex C" "closed C" by (auto simp: convex𝒩 closed𝒩 ‹C ∈ 𝒩›) obtain F where F: "F face_of C" and "F ≠ C" "K ⊆ F" proof - obtain L where "L ∈ 𝒮" "K ⊆ L" using ‹K ∈ 𝒰› C𝒰 by blast have "K ≤ rel_frontier C" by (simp add: ‹K ⊆ rel_frontier C›) also have "... ≤ C" by (simp add: ‹closed C› rel_frontier_def subset_iff) finally have "K ⊆ C" . have "L ∩ C face_of C" using 𝒩_def 𝒮_def ‹C ∈ 𝒩› ‹L ∈ 𝒮› intfaceℳ by auto moreover have "L ∩ C ≠ C" using ‹C ∈ 𝒩› ‹L ∈ 𝒮› apply (clarsimp simp: 𝒩_def 𝒮_def) by (metis aff_dim_subset inf_le1 not_le) moreover have "K ⊆ L ∩ C" using ‹C ∈ 𝒩› ‹L ∈ 𝒮› ‹K ⊆ C› ‹K ⊆ L› by (auto simp: 𝒩_def 𝒮_def) ultimately show ?thesis using that by metis qed have "affine hull F ∩ rel_interior C = {}" by (rule affine_hull_face_of_disjoint_rel_interior [OF ‹convex C› F ‹F ≠ C›]) with hull_mono [OF ‹K ⊆ F›] show "affine hull K ∩ rel_interior C = {}" by fastforce qed let ?𝒯 = "(⋃C ∈ 𝒩. ⋃K ∈ 𝒰 ∩ Pow (rel_frontier C). {convex hull (insert (SOME z. z ∈ rel_interior C) K)})" have "∃𝒯. simplicial_complex 𝒯 ∧ (∀K ∈ 𝒯. aff_dim K ≤ of_nat n) ∧ (∀C ∈ ℳ. ∃F. F ⊆ 𝒯 ∧ C = ⋃F) ∧ (∀K ∈ 𝒯. ∃C. C ∈ ℳ ∧ K ⊆ C)" proof (rule exI, intro conjI ballI) show "simplicial_complex (𝒰 ∪ ?𝒯)" unfolding simplicial_complex_def proof (intro conjI impI ballI allI) show "finite (𝒰 ∪ ?𝒯)" using ‹finite 𝒰› ‹finite 𝒩› by simp show "∃n. n simplex S" if "S ∈ 𝒰 ∪ ?𝒯" for S using that ahK_C_disjoint in_rel_interior simpl𝒰 simplex_insert_dimplus1 by fastforce show "F ∈ 𝒰 ∪ ?𝒯" if S: "S ∈ 𝒰 ∪ ?𝒯 ∧ F face_of S" for F S proof - have "F ∈ 𝒰" if "S ∈ 𝒰" using S face𝒰 that by blast moreover have "F ∈ 𝒰 ∪ ?𝒯" if "F face_of S" "C ∈ 𝒩" "K ∈ 𝒰" and "K ⊆ rel_frontier C" and S: "S = convex hull insert (SOME z. z ∈ rel_interior C) K" for C K proof - let ?z = "SOME z. z ∈ rel_interior C" have "?z ∈ rel_interior C" by (simp add: in_rel_interior ‹C ∈ 𝒩›) moreover obtain I where "¬ affine_dependent I" "card I ≤ n" "aff_dim K < int n" "K = convex hull I" using * [OF ‹K ∈ 𝒰›] by auto ultimately have "?z ∉ affine hull I" using ahK_C_disjoint affine_hull_convex_hull that by blast have "compact I" "finite I" by (auto simp: ‹¬ affine_dependent I› aff_independent_finite finite_imp_compact) moreover have "F face_of convex hull insert ?z I" by (metis S ‹F face_of S› ‹K = convex hull I› convex_hull_eq_empty convex_hull_insert_segments hull_hull) ultimately obtain J where "J ⊆ insert ?z I" "F = convex hull J" using face_of_convex_hull_subset [of "insert ?z I" F] by auto show ?thesis proof (cases "?z ∈ J") case True have "F ∈ (⋃K∈𝒰 ∩ Pow (rel_frontier C). {convex hull insert ?z K})" proof have "convex hull (J - {?z}) face_of K" by (metis True ‹J ⊆ insert ?z I› ‹K = convex hull I› ‹¬ affine_dependent I› face_of_convex_hull_affine_independent subset_insert_iff) then have "convex hull (J - {?z}) ∈ 𝒰" by (rule face𝒰 [OF ‹K ∈ 𝒰›]) moreover have "⋀x. x ∈ convex hull (J - {?z}) ⟹ x ∈ rel_frontier C" by (metis True ‹J ⊆ insert ?z I› ‹K = convex hull I› subsetD hull_mono subset_insert_iff that(4)) ultimately show "convex hull (J - {?z}) ∈ 𝒰 ∩ Pow (rel_frontier C)" by auto let ?F = "convex hull insert ?z (convex hull (J - {?z}))" have "F ⊆ ?F" apply (clarsimp simp: ‹F = convex hull J›) by (metis True subsetD hull_mono hull_subset subset_insert_iff) moreover have "?F ⊆ F" apply (clarsimp simp: ‹F = convex hull J›) by (metis (no_types, lifting) True convex_hull_eq_empty convex_hull_insert_segments hull_hull insert_Diff) ultimately show "F ∈ {?F}" by auto qed with ‹C∈𝒩› show ?thesis by auto next case False then have "F ∈ 𝒰" using face_of_convex_hull_affine_independent [OF ‹¬ affine_dependent I›] by (metis Int_absorb2 Int_insert_right_if0 ‹F = convex hull J› ‹J ⊆ insert ?z I› ‹K = convex hull I› face𝒰 inf_le2 ‹K ∈ 𝒰›) then show "F ∈ 𝒰 ∪ ?𝒯" by blast qed qed ultimately show ?thesis using that by auto qed have "(S ∩ S' face_of S) ∧ (S ∩ S' face_of S')" if "S ∈ 𝒰 ∪ ?𝒯" "S' ∈ 𝒰 ∪ ?𝒯" for S S' proof - have symmy: "⟦⋀X Y. R X Y ⟹ R Y X; ⋀X Y. ⟦X ∈ 𝒰; Y ∈ 𝒰⟧ ⟹ R X Y; ⋀X Y. ⟦X ∈ 𝒰; Y ∈ ?𝒯⟧ ⟹ R X Y; ⋀X Y. ⟦X ∈ ?𝒯; Y ∈ ?𝒯⟧ ⟹ R X Y⟧ ⟹ R S S'" for R using that by (metis (no_types, lifting) Un_iff) show ?thesis proof (rule symmy) show "Y ∩ X face_of Y ∧ Y ∩ X face_of X" if "X ∩ Y face_of X ∧ X ∩ Y face_of Y" for X Y :: "'a set" by (simp add: inf_commute that) next show "X ∩ Y face_of X ∧ X ∩ Y face_of Y" if "X ∈ 𝒰" and "Y ∈ 𝒰" for X Y by (simp add: faceI𝒰 that) next show "X ∩ Y face_of X ∧ X ∩ Y face_of Y" if XY: "X ∈ 𝒰" "Y ∈ ?𝒯" for X Y proof - obtain C K where "C ∈ 𝒩" "K ∈ 𝒰" "K ⊆ rel_frontier C" and Y: "Y = convex hull insert (SOME z. z ∈ rel_interior C) K" using XY by blast have "convex C" by (simp add: ‹C ∈ 𝒩› convex𝒩) have "K ⊆ C" by (metis DiffE ‹C ∈ 𝒩› ‹K ⊆ rel_frontier C› closed𝒩 closure_closed rel_frontier_def subset_iff) let ?z = "(SOME z. z ∈ rel_interior C)" have z: "?z ∈ rel_interior C" using ‹C ∈ 𝒩› in_rel_interior by blast obtain D where "D ∈ 𝒮" "X ⊆ D" using C𝒰 ‹X ∈ 𝒰› by blast have "D ∩ rel_interior C = (C ∩ D) ∩ rel_interior C" using rel_interior_subset by blast also have "(C ∩ D) ∩ rel_interior C = {}" proof (rule face_of_disjoint_rel_interior) show "C ∩ D face_of C" using 𝒩_def 𝒮_def ‹C ∈ 𝒩› ‹D ∈ 𝒮› intfaceℳ by blast show "C ∩ D ≠ C" by (metis (mono_tags, lifting) Int_lower2 𝒩_def 𝒮_def ‹C ∈ 𝒩› ‹D ∈ 𝒮› aff_dim_subset mem_Collect_eq not_le) qed finally have DC: "D ∩ rel_interior C = {}" . have eq: "X ∩ convex hull (insert ?z K) = X ∩ convex hull K" apply (rule Int_convex_hull_insert_rel_exterior [OF ‹convex C› ‹K ⊆ C› z]) using DC by (meson ‹X ⊆ D› disjnt_def disjnt_subset1) obtain I where I: "¬ affine_dependent I" and Keq: "K = convex hull I" and [simp]: "convex hull K = K" using "*" ‹K ∈ 𝒰› by force then have "?z ∉ affine hull I" using ahK_C_disjoint ‹C ∈ 𝒩› ‹K ∈ 𝒰› ‹K ⊆ rel_frontier C› affine_hull_convex_hull z by blast have "X ∩ K face_of K" by (simp add: ‹K ∈ 𝒰› faceI𝒰 ‹X ∈ 𝒰›) also have "... face_of convex hull insert ?z K" by (metis I Keq ‹?z ∉ affine hull I› aff_independent_finite convex_convex_hull face_of_convex_hull_insert face_of_refl hull_insert) finally have "X ∩ K face_of convex hull insert ?z K" . then show ?thesis using "*" ‹K ∈ 𝒰› faceI𝒰 that(1) by (fastforce simp add: Y eq) qed next show "X ∩ Y face_of X ∧ X ∩ Y face_of Y" if XY: "X ∈ ?𝒯" "Y ∈ ?𝒯" for X Y proof - obtain C K D L where "C ∈ 𝒩" "K ∈ 𝒰" "K ⊆ rel_frontier C" and X: "X = convex hull insert (SOME z. z ∈ rel_interior C) K" and "D ∈ 𝒩" "L ∈ 𝒰" "L ⊆ rel_frontier D" and Y: "Y = convex hull insert (SOME z. z ∈ rel_interior D) L" using XY by blast let ?z = "(SOME z. z ∈ rel_interior C)" have z: "?z ∈ rel_interior C" using ‹C ∈ 𝒩› in_rel_interior by blast have "convex C" by (simp add: ‹C ∈ 𝒩› convex𝒩) have "convex K" using "*" ‹K ∈ 𝒰› by blast have "convex L" by (meson ‹L ∈ 𝒰› convex_simplex simpl𝒰) show ?thesis proof (cases "D=C") case True then have "L ⊆ rel_frontier C" using ‹L ⊆ rel_frontier D› by auto show ?thesis apply (simp add: X Y True) apply (simp add: convex_hull_insert_Int_eq [OF z] ‹K ⊆ rel_frontier C› ‹L ⊆ rel_frontier C› ‹convex C› ‹convex K› ‹convex L›) using face_of_polytope_insert2 by (metis "*" IntI ‹C ∈ 𝒩› ‹K ∈ 𝒰› ‹L ∈ 𝒰›‹K ⊆ rel_frontier C› ‹L ⊆ rel_frontier C› aff_independent_finite ahK_C_disjoint empty_iff faceI𝒰 polytope_convex_hull z) next case False have "convex D" by (simp add: ‹D ∈ 𝒩› convex𝒩) have "K ⊆ C" by (metis DiffE ‹C ∈ 𝒩› ‹K ⊆ rel_frontier C› closed𝒩 closure_closed rel_frontier_def subset_eq) have "L ⊆ D" by (metis DiffE ‹D ∈ 𝒩› ‹L ⊆ rel_frontier D› closed𝒩 closure_closed rel_frontier_def subset_eq) let ?w = "(SOME w. w ∈ rel_interior D)" have w: "?w ∈ rel_interior D" using ‹D ∈ 𝒩› in_rel_interior by blast have "C ∩ rel_interior D = (D ∩ C) ∩ rel_interior D" using rel_interior_subset by blast also have "(D ∩ C) ∩ rel_interior D = {}" proof (rule face_of_disjoint_rel_interior) show "D ∩ C face_of D" using 𝒩_def ‹C ∈ 𝒩› ‹D ∈ 𝒩› intfaceℳ by blast have "D ∈ ℳ ∧ aff_dim D = int n" using 𝒩_def ‹D ∈ 𝒩› by blast moreover have "C ∈ ℳ ∧ aff_dim C = int n" using 𝒩_def ‹C ∈ 𝒩› by blast ultimately show "D ∩ C ≠ D" by (metis False face_of_aff_dim_lt inf.idem inf_le1 intfaceℳ not_le polyℳ polytope_imp_convex) qed finally have CD: "C ∩ (rel_interior D) = {}" . have zKC: "(convex hull insert ?z K) ⊆ C" by (metis DiffE ‹C ∈ 𝒩› ‹K ⊆ rel_frontier C› closed𝒩 closure_closed convex𝒩 hull_minimal insert_subset rel_frontier_def rel_interior_subset subset_iff z) have eq: "convex hull (insert ?z K) ∩ convex hull (insert ?w L) = convex hull (insert ?z K) ∩ convex hull L" apply (rule Int_convex_hull_insert_rel_exterior [OF ‹convex D› ‹L ⊆ D› w]) using zKC CD apply (force simp: disjnt_def) done have ch_id: "convex hull K = K" "convex hull L = L" using "*" ‹K ∈ 𝒰› ‹L ∈ 𝒰› hull_same by auto have "convex C" by (simp add: ‹C ∈ 𝒩› convex𝒩) have "convex hull (insert ?z K) ∩ L = L ∩ convex hull (insert ?z K)" by blast also have "... = convex hull K ∩ L" proof (subst Int_convex_hull_insert_rel_exterior [OF ‹convex C› ‹K ⊆ C› z]) have "(C ∩ D) ∩ rel_interior C = {}" proof (rule face_of_disjoint_rel_interior) show "C ∩ D face_of C" using 𝒩_def ‹C ∈ 𝒩› ‹D ∈ 𝒩› intfaceℳ by blast have "D ∈ ℳ" "aff_dim D = int n" using 𝒩_def ‹D ∈ 𝒩› by fastforce+ moreover have "C ∈ ℳ" "aff_dim C = int n" using 𝒩_def ‹C ∈ 𝒩› by fastforce+ ultimately have "aff_dim D + - 1 * aff_dim C ≤ 0" by fastforce then have "¬ C face_of D" using False ‹convex D› face_of_aff_dim_lt by fastforce show "C ∩ D ≠ C" using ‹C ∈ ℳ› ‹D ∈ ℳ› ‹¬ C face_of D› intfaceℳ by fastforce qed then have "D ∩ rel_interior C = {}" by (metis inf.absorb_iff2 inf_assoc inf_sup_aci(1) rel_interior_subset) then show "disjnt L (rel_interior C)" by (meson ‹L ⊆ D› disjnt_def disjnt_subset1) next show "L ∩ convex hull K = convex hull K ∩ L" by force qed finally have chKL: "convex hull (insert ?z K) ∩ L = convex hull K ∩ L" . have "convex hull insert ?z K ∩ convex hull L face_of K" by (simp add: ‹K ∈ 𝒰› ‹L ∈ 𝒰› ch_id chKL faceI𝒰) also have "... face_of convex hull insert ?z K" proof - obtain I where I: "¬ affine_dependent I" "K = convex hull I" using * [OF ‹K ∈ 𝒰›] by auto then have "⋀a. a ∉ rel_interior C ∨ a ∉ affine hull I" using ahK_C_disjoint ‹C ∈ 𝒩› ‹K ∈ 𝒰› ‹K ⊆ rel_frontier C› affine_hull_convex_hull by blast then show ?thesis by (metis I affine_independent_insert face_of_convex_hull_affine_independent hull_insert subset_insertI z) qed finally have 1: "convex hull insert ?z K ∩ convex hull L face_of convex hull insert ?z K" . have "convex hull insert ?z K ∩ convex hull L face_of L" by (simp add: ‹K ∈ 𝒰› ‹L ∈ 𝒰› ch_id chKL faceI𝒰) also have "... face_of convex hull insert ?w L" proof - obtain I where I: "¬ affine_dependent I" "L = convex hull I" using * [OF ‹L ∈ 𝒰›] by auto then have "⋀a. a ∉ rel_interior D ∨ a ∉ affine hull I" using ‹D ∈ 𝒩› ‹L ∈ 𝒰› ‹L ⊆ rel_frontier D› affine_hull_convex_hull ahK_C_disjoint by blast then show ?thesis by (metis I aff_independent_finite convex_convex_hull face_of_convex_hull_insert face_of_refl hull_insert w) qed finally have 2: "convex hull insert ?z K ∩ convex hull L face_of convex hull insert ?w L" . show ?thesis by (simp add: X Y eq 1 2) qed qed qed qed then