Theory Polytope

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
        show "S ∩ S' face_of S" "S ∩ S' face_of S'" if "S ∈ 𝒰 ∪ ?𝒯 ∧ S' ∈ 𝒰 ∪ ?𝒯" for S S'
          using that by auto
      qed
      show "∃F ⊆ 𝒰 ∪ ?𝒯. C = ⋃F" if "C ∈ ℳ" for C
      proof (cases "C ∈ 𝒮")
        case True
        then show ?thesis
          by (meson UnCI fin𝒰 subsetD subsetI)
      next
        case False
        then have "C ∈ 𝒩"
          by (simp add: 𝒩_def 𝒮_def affℳ less_le that)
        let ?z = "SOME z. z ∈ rel_interior C"
        have z: "?z ∈ rel_interior C"
          using ‹C ∈ 𝒩› in_rel_interior by blast
        let ?F = "⋃K ∈ 𝒰 ∩ Pow (rel_frontier C). {convex hull (insert ?z K)}"
        have "?F ⊆ ?𝒯"
          using ‹C ∈ 𝒩› by blast
        moreover have "C ⊆ ⋃?F"
        proof
          fix x
          assume "x ∈ C"
          have "convex C"
            using ‹C ∈ 𝒩› convex𝒩 by blast
          have "bounded C"
            using ‹C ∈ 𝒩› by (simp add: polyℳ polytope_imp_bounded that)
          have "polytope C"
            using ‹C ∈ 𝒩› poly𝒩 by auto
          have "¬ (?z = x ∧ C = {?z})"
            using ‹C ∈ 𝒩› aff_dim_sing [of ?z] ‹¬ n ≤ 1› by (force simp: 𝒩_def)
          then obtain y where y: "y ∈ rel_frontier C" and xzy: "x ∈ closed_segment ?z y"
            and sub: "open_segment ?z y ⊆ rel_interior C"
            by (blast intro: segment_to_rel_frontier [OF ‹convex C› ‹bounded C› z ‹x ∈ C›])
          then obtain F where "y ∈ F" "F face_of C" "F ≠ C"
            by (auto simp: rel_frontier_of_polyhedron_alt [OF polytope_imp_polyhedron [OF ‹polytope C›]])
          then obtain 𝒢 where "finite 𝒢" "𝒢 ⊆ 𝒰" "F = ⋃𝒢"
            by (metis (mono_tags, lifting) 𝒮_def ‹C ∈ ℳ› ‹convex C› affℳ faceℳ face_of_aff_dim_lt fin𝒰 le_less_trans mem_Collect_eq not_less)
          then obtain K where "y ∈ K" "K ∈ 𝒢"
            using ‹y ∈ F› by blast
          moreover have x: "x ∈ convex hull {?z,y}"
            using segment_convex_hull xzy by auto
          moreover have "convex hull {?z,y} ⊆ convex hull insert ?z K"
            by (metis (full_types) ‹y ∈ K› hull_mono empty_subsetI insertCI insert_subset)
          moreover have "K ∈ 𝒰"
            using ‹K ∈ 𝒢› ‹𝒢 ⊆ 𝒰› by blast
          moreover have "K ⊆ rel_frontier C"
            using ‹F = ⋃𝒢› ‹F ≠ C› ‹F face_of C› ‹K ∈ 𝒢› face_of_subset_rel_frontier by fastforce
          ultimately show "x ∈ ⋃?F"
            by force
        qed
        moreover
        have "convex hull insert (SOME z. z ∈ rel_interior C) K ⊆ C"
          if "K ∈ 𝒰" "K ⊆ rel_frontier C" for K
        proof (rule hull_minimal)
          show "insert (SOME z. z ∈ rel_interior C) K ⊆ C"
            using that ‹C ∈ 𝒩› in_rel_interior rel_interior_subset
            by (force simp: closure_eq rel_frontier_def closed𝒩)
          show "convex C"
            by (simp add: ‹C ∈ 𝒩› convex𝒩)
        qed
        then have "⋃?F ⊆ C"
          by auto
        ultimately show ?thesis
          by blast
      qed

      have "(∃C. C ∈ ℳ ∧ L ⊆ C) ∧ aff_dim L ≤ int n"  if "L ∈ 𝒰 ∪ ?𝒯" for L
        using that
      proof
        assume "L ∈ 𝒰"
        then show ?thesis
          using C𝒰 𝒮_def "*" by fastforce
      next
        assume "L ∈ ?𝒯"
        then obtain C K where "C ∈ 𝒩"
          and L: "L = convex hull insert (SOME z. z ∈ rel_interior C) K"
          and K: "K ∈ 𝒰" "K ⊆ rel_frontier C"
          by auto
        then have "convex hull C = C"
          by (meson convex𝒩 convex_hull_eq)
        then have "convex C"
          by (metis (no_types) convex_convex_hull)
        have "rel_frontier C ⊆ C"
          by (metis DiffE closed𝒩 ‹C ∈ 𝒩› closure_closed rel_frontier_def subsetI)
        have "K ⊆ C"
          using K ‹rel_frontier C ⊆ C› by blast
        have "C ∈ ℳ"
          using 𝒩_def ‹C ∈ 𝒩› by auto
        moreover have "L ⊆ C"
          using K L ‹C ∈ 𝒩›
          by (metis ‹K ⊆ C› ‹convex hull C = C› contra_subsetD hull_mono in_rel_interior insert_subset rel_interior_subset)
        ultimately show ?thesis
          using ‹rel_frontier C ⊆ C› ‹L ⊆ C› affℳ aff_dim_subset ‹C ∈ ℳ› dual_order.trans by blast
      qed
      then show "∃C. C ∈ ℳ ∧ L ⊆ C" "aff_dim L ≤ int n" if "L ∈ 𝒰 ∪ ?𝒯" for L
        using that by auto
    qed
    then show ?thesis
      apply (rule ex_forward, safe)
        apply (meson Union_iff subsetCE, fastforce)
      by (meson infinite_super simplicial_complex_def)
  qed
qed


lemma simplicial_subdivision_of_cell_complex_lowdim:
  assumes "finite ℳ"
      and poly: "⋀C. C ∈ ℳ ⟹ polytope C"
      and face: "⋀C1 C2. ⟦C1 ∈ ℳ; C2 ∈ ℳ⟧ ⟹ C1 ∩ C2 face_of C1 ∧ C1 ∩ C2 face_of C2"
      and aff: "⋀C. C ∈ ℳ ⟹ aff_dim C ≤ d"
  obtains 𝒯 where "simplicial_complex 𝒯" "⋀K. K ∈ 𝒯 ⟹ aff_dim K ≤ d"
                  "⋃𝒯 = ⋃ℳ"
                  "⋀C. C ∈ ℳ ⟹ ∃F. finite F ∧ F ⊆ 𝒯 ∧ C = ⋃F"
                  "⋀K. K ∈ 𝒯 ⟹ ∃C. C ∈ ℳ ∧ K ⊆ C"
proof (cases "d ≥ 0")
  case True
  then obtain n where n: "d = of_nat n"
    using zero_le_imp_eq_int by blast
  have "∃𝒯. simplicial_complex 𝒯 ∧
            (∀K∈𝒯. aff_dim K ≤ int n) ∧
            ⋃𝒯 = ⋃(⋃C∈ℳ. {F. F face_of C}) ∧
            (∀C∈⋃C∈ℳ. {F. F face_of C}.
                ∃F. finite F ∧ F ⊆ 𝒯 ∧ C = ⋃F) ∧
            (∀K∈𝒯. ∃C. C ∈ (⋃C∈ℳ. {F. F face_of C}) ∧ K ⊆ C)"
  proof (rule simplicial_subdivision_aux)
    show "finite (⋃C∈ℳ. {F. F face_of C})"
      using ‹finite ℳ› poly polyhedron_eq_finite_faces polytope_imp_polyhedron by fastforce
    show "polytope F" if "F ∈ (⋃C∈ℳ. {F. F face_of C})" for F
      using poly that face_of_polytope_polytope by blast
    show "aff_dim F ≤ int n" if "F ∈ (⋃C∈ℳ. {F. F face_of C})" for F
      using that
      by clarify (metis n aff_dim_subset aff face_of_imp_subset order_trans)
    show "F ∈ (⋃C∈ℳ. {F. F face_of C})"
      if "G ∈ (⋃C∈ℳ. {F. F face_of C})" and "F face_of G" for F G
      using that face_of_trans by blast
  next
    show "F1 ∩ F2 face_of F1 ∧ F1 ∩ F2 face_of F2"
      if "F1 ∈ (⋃C∈ℳ. {F. F face_of C})" and "F2 ∈ (⋃C∈ℳ. {F. F face_of C})" for F1 F2
      using that
      by safe (meson face face_of_Int_subface)+
  qed
  moreover
  have "⋃(⋃C∈ℳ. {F. F face_of C}) = ⋃ℳ"
    using face_of_imp_subset face by blast
  ultimately show ?thesis
    apply clarify
    apply (rule that, assumption+)
       using n apply blast
      apply (simp_all add: poly face_of_refl polytope_imp_convex)
    using face_of_imp_subset by fastforce
next
  case False
  then have m1: "⋀C. C ∈ ℳ ⟹ aff_dim C = -1"
    by (metis aff aff_dim_empty_eq aff_dim_negative_iff dual_order.trans not_less)
  then have faceℳ: "⋀F S. ⟦S ∈ ℳ; F face_of S⟧ ⟹ F ∈ ℳ"
    by (metis aff_dim_empty face_of_empty)
  show ?thesis
  proof
    have "⋀S. S ∈ ℳ ⟹ ∃n. n simplex S"
      by (metis (no_types) m1 aff_dim_empty simplex_minus_1)
    then show "simplicial_complex ℳ"
      by (auto simp: simplicial_complex_def ‹finite ℳ› face intro: faceℳ)
    show "aff_dim K ≤ d" if "K ∈ ℳ" for K
      by (simp add: that aff)
    show "∃F. finite F ∧ F ⊆ ℳ ∧ C = ⋃F" if "C ∈ ℳ" for C
      using ‹C ∈ ℳ› equals0I by auto
    show "∃C. C ∈ ℳ ∧ K ⊆ C" if "K ∈ ℳ" for K
      using ‹K ∈ ℳ› by blast
  qed auto
qed

proposition simplicial_subdivision_of_cell_complex:
  assumes "finite ℳ"
      and poly: "⋀C. C ∈ ℳ ⟹ polytope C"
      and face: "⋀C1 C2. ⟦C1 ∈ ℳ; C2 ∈ ℳ⟧ ⟹ C1 ∩ C2 face_of C1 ∧ C1 ∩ C2 face_of C2"
  obtains 𝒯 where "simplicial_complex 𝒯"
                  "⋃𝒯 = ⋃ℳ"
                  "⋀C. C ∈ ℳ ⟹ ∃F. finite F ∧ F ⊆ 𝒯 ∧ C = ⋃F"
                  "⋀K. K ∈ 𝒯 ⟹ ∃C. C ∈ ℳ ∧ K ⊆ C"
  by (blast intro: simplicial_subdivision_of_cell_complex_lowdim [OF assms aff_dim_le_DIM])

corollary fine_simplicial_subdivision_of_cell_complex:
  assumes "0 < e" "finite ℳ"
      and poly: "⋀C. C ∈ ℳ ⟹ polytope C"
      and face: "⋀C1 C2. ⟦C1 ∈ ℳ; C2 ∈ ℳ⟧ ⟹ C1 ∩ C2 face_of C1 ∧ C1 ∩ C2 face_of C2"
  obtains 𝒯 where "simplicial_complex 𝒯"
                  "⋀K. K ∈ 𝒯 ⟹ diameter K < e"
                  "⋃𝒯 = ⋃ℳ"
                  "⋀C. C ∈ ℳ ⟹ ∃F. finite F ∧ F ⊆ 𝒯 ∧ C = ⋃F"
                  "⋀K. K ∈ 𝒯 ⟹ ∃C. C ∈ ℳ ∧ K ⊆ C"
proof -
  obtain 𝒩 where 𝒩: "finite 𝒩" "⋃𝒩 = ⋃ℳ" 
              and diapoly: "⋀X. X ∈ 𝒩 ⟹ diameter X < e" "⋀X. X ∈ 𝒩 ⟹ polytope X"
               and      "⋀X Y. ⟦X ∈ 𝒩; Y ∈ 𝒩⟧ ⟹ X ∩ Y face_of X ∧ X ∩ Y face_of Y"
               and 𝒩covers: "⋀C x. C ∈ ℳ ∧ x ∈ C ⟹ ∃D. D ∈ 𝒩 ∧ x ∈ D ∧ D ⊆ C"
               and 𝒩covered: "⋀C. C ∈ 𝒩 ⟹ ∃D. D ∈ ℳ ∧ C ⊆ D"
    by (blast intro: cell_complex_subdivision_exists [OF ‹0 < e› ‹finite ℳ› poly aff_dim_le_DIM face])
  then obtain 𝒯 where 𝒯: "simplicial_complex 𝒯" "⋃𝒯 = ⋃𝒩"
                   and 𝒯covers: "⋀C. C ∈ 𝒩 ⟹ ∃F. finite F ∧ F ⊆ 𝒯 ∧ C = ⋃F"
                   and 𝒯covered: "⋀K. K ∈ 𝒯 ⟹ ∃C. C ∈ 𝒩 ∧ K ⊆ C"
    using simplicial_subdivision_of_cell_complex [OF ‹finite 𝒩›] by metis
  show ?thesis
  proof
    show "simplicial_complex 𝒯"
      by (rule 𝒯)
    show "diameter K < e" if "K ∈ 𝒯" for K
      by (metis le_less_trans diapoly 𝒯covered diameter_subset polytope_imp_bounded that)
    show "⋃𝒯 = ⋃ℳ"
      by (simp add: 𝒩(2) ‹⋃𝒯 = ⋃𝒩›)
    show "∃F. finite F ∧ F ⊆ 𝒯 ∧ C = ⋃F" if "C ∈ ℳ" for C
    proof -
      { fix x
        assume "x ∈ C"
        then obtain D where "D ∈ 𝒯" "x ∈ D" "D ⊆ C"
          using 𝒩covers ‹C ∈ ℳ› 𝒯covers by force
        then have "∃X∈𝒯 ∩ Pow C. x ∈ X"
          using ‹D ∈ 𝒯› ‹D ⊆ C› ‹x ∈ D› by blast
      }
      moreover
      have "finite (𝒯 ∩ Pow C)"
        using ‹simplicial_complex 𝒯› simplicial_complex_def by auto
      ultimately show ?thesis
        by (rule_tac x="(𝒯 ∩ Pow C)" in exI) auto
    qed
    show "∃C. C ∈ ℳ ∧ K ⊆ C" if "K ∈ 𝒯" for K
      by (meson 𝒩covered 𝒯covered order_trans that)
  qed
qed

subsection‹Some results on cell division with full-dimensional cells only›

lemma convex_Union_fulldim_cells:
  assumes "finite 𝒮" and clo: "⋀C. C ∈ 𝒮 ⟹ closed C" and con: "⋀C. C ∈ 𝒮 ⟹ convex C"
      and eq: "⋃𝒮 = U"and  "convex U"
 shows "⋃{C ∈ 𝒮. aff_dim C = aff_dim U} = U"  (is "?lhs = U")
proof -
  have "closed U"
    using ‹finite 𝒮› clo eq by blast
  have "?lhs ⊆ U"
    using eq by blast
  moreover have "U ⊆ ?lhs"
  proof (cases "∀C ∈ 𝒮. aff_dim C = aff_dim U")
    case True
    then show ?thesis
      using eq by blast
  next
    case False
    have "closed ?lhs"
      by (simp add: ‹finite 𝒮› clo closed_Union)
    moreover have "U ⊆ closure ?lhs"
    proof -
      have "U ⊆ closure(⋂{U - C |C. C ∈ 𝒮 ∧ aff_dim C < aff_dim U})"
      proof (rule Baire [OF ‹closed U›])
        show "countable {U - C |C. C ∈ 𝒮 ∧ aff_dim C < aff_dim U}"
          using ‹finite 𝒮› uncountable_infinite by fastforce
        have "⋀C. C ∈ 𝒮 ⟹ openin (subtopology euclidean U) (U-C)"
          by (metis Sup_upper clo closed_limpt closedin_limpt eq openin_diff openin_subtopology_self)
        then show "openin (subtopology euclidean U) T ∧ U ⊆ closure T"
          if "T ∈ {U - C |C. C ∈ 𝒮 ∧ aff_dim C < aff_dim U}" for T
          using that dense_complement_convex_closed ‹closed U› ‹convex U› by auto
      qed
      also have "... ⊆ closure ?lhs"
      proof -
        obtain C where "C ∈ 𝒮" "aff_dim C < aff_dim U"
          by (metis False Sup_upper aff_dim_subset eq eq_iff not_le)
        have "∃X. X ∈ 𝒮 ∧ aff_dim X = aff_dim U ∧ x ∈ X"
          if "⋀V. (∃C. V = U - C ∧ C ∈ 𝒮 ∧ aff_dim C < aff_dim U) ⟹ x ∈ V" for x
        proof -
          have "x ∈ U ∧ x ∈ ⋃𝒮"
            using ‹C ∈ 𝒮› ‹aff_dim C < aff_dim U› eq that by blast
          then show ?thesis
            by (metis Diff_iff Sup_upper Union_iff aff_dim_subset dual_order.order_iff_strict eq that)
        qed
        then show ?thesis
          by (auto intro!: closure_mono)
      qed
      finally show ?thesis .
    qed
    ultimately show ?thesis
      using closure_subset_eq by blast
  qed
  ultimately show ?thesis by blast
qed

proposition fine_triangular_subdivision_of_cell_complex:
  assumes "0 < e" "finite ℳ"
      and poly: "⋀C. C ∈ ℳ ⟹ polytope C"
      and aff: "⋀C. C ∈ ℳ ⟹ aff_dim C = d"
      and face: "⋀C1 C2. ⟦C1 ∈ ℳ; C2 ∈ ℳ⟧ ⟹ C1 ∩ C2 face_of C1 ∧ C1 ∩ C2 face_of C2"
  obtains 𝒯 where "triangulation 𝒯" "⋀k. k ∈ 𝒯 ⟹ diameter k < e"
                 "⋀k. k ∈ 𝒯 ⟹ aff_dim k = d" "⋃𝒯 = ⋃ℳ"
                 "⋀C. C ∈ ℳ ⟹ ∃f. finite f ∧ f ⊆ 𝒯 ∧ C = ⋃f"
                 "⋀k. k ∈ 𝒯 ⟹ ∃C. C ∈ ℳ ∧ k ⊆ C"
proof -
  obtain 𝒯 where "simplicial_complex 𝒯"
             and dia𝒯: "⋀K. K ∈ 𝒯 ⟹ diameter K < e"
             and "⋃𝒯 = ⋃ℳ"
             and inℳ: "⋀C. C ∈ ℳ ⟹ ∃F. finite F ∧ F ⊆ 𝒯 ∧ C = ⋃F"
             and in𝒯: "⋀K. K ∈ 𝒯 ⟹ ∃C. C ∈ ℳ ∧ K ⊆ C"
    by (blast intro: fine_simplicial_subdivision_of_cell_complex [OF ‹e > 0› ‹finite ℳ› poly face])
  let ?𝒯 = "{K ∈ 𝒯. aff_dim K = d}"
  show thesis
  proof
    show "triangulation ?𝒯"
      using ‹simplicial_complex 𝒯› by (auto simp: triangulation_def simplicial_complex_def)
    show "diameter L < e" if "L ∈ {K ∈ 𝒯. aff_dim K = d}" for L
      using that by (auto simp: dia𝒯)
    show "aff_dim L = d" if "L ∈ {K ∈ 𝒯. aff_dim K = d}" for L
      using that by auto
    show "∃F. finite F ∧ F ⊆ {K ∈ 𝒯. aff_dim K = d} ∧ C = ⋃F" if "C ∈ ℳ" for C
    proof -
      obtain F where "finite F" "F ⊆ 𝒯" "C = ⋃F"
        using inℳ [OF ‹C ∈ ℳ›] by auto
      show ?thesis
      proof (intro exI conjI)
        show "finite {K ∈ F. aff_dim K = d}"
          by (simp add: ‹finite F›)
        show "{K ∈ F. aff_dim K = d} ⊆ {K ∈ 𝒯. aff_dim K = d}"
          using ‹F ⊆ 𝒯› by blast
        have "d = aff_dim C"
          by (simp add: aff that)
        moreover have "⋀K. K ∈ F ⟹ closed K ∧ convex K"
          using ‹simplicial_complex 𝒯› ‹F ⊆ 𝒯›
          unfolding simplicial_complex_def by (metis subsetCE ‹F ⊆ 𝒯› closed_simplex convex_simplex)
        moreover have "convex (⋃F)"
          using ‹C = ⋃F› poly polytope_imp_convex that by blast
        ultimately show "C = ⋃{K ∈ F. aff_dim K = d}"
          by (simp add: convex_Union_fulldim_cells ‹C = ⋃F› ‹finite F›)
      qed
    qed
    then show "⋃{K ∈ 𝒯. aff_dim K = d} = ⋃ℳ"
      by auto (meson in𝒯 subsetCE)
    show "∃C. C ∈ ℳ ∧ L ⊆ C"
      if "L ∈ {K ∈ 𝒯. aff_dim K = d}" for L
      using that by (auto simp: in𝒯)
  qed
qed

end