Theory HOL-Analysis.Polytope

section ‹Faces, Extreme Points, Polytopes, Polyhedra etc›

text‹Ported from HOL Light by L C Paulson›

theory Polytope
imports Cartesian_Euclidean_Space Path_Connected
begin

subsection ‹Faces of a (usually convex) set›

definitiontag important› 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)"
    by (simp add: face_of_def)
  show ?thesis
    by (force simp: image_comp o_def dest: * [where a = "-a"] intro: *)
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 faces_of_linear_image:
   "linear f; inj f  {T. T face_of (f ` S)} = (image f) ` {T. T face_of S}"
  by (smt (verit) Collect_cong face_of_def face_of_linear_image setcompr_eq_image subset_imageE)

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

proposition 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
      by (meson greaterThanLessThan_iff in_segment(2))
    define u where "u  min (1/2) (e / norm (x - y))"
    have in01: "u  {0<..<1}"
      using y  x e > 0 by (simp add: u_def)
    have "norm (u *R y - u *R x)  e"
      using e > 0
      by (simp add: u_def norm_minus_commute min_mult_distrib_right flip: scaleR_diff_right)
    then have "dist y ((1 - u) *R y + u *R x)  e"
      by (simp add: dist_norm algebra_simps)
    then show False
      using zne [OF in01 e [THEN subsetD]] by (simp add: y  T hull_inc mem_affine x)
  qed
  show ?thesis
  proof (rule subset_antisym)
    show "T  affine hull T  S"
      using assms by (simp add: hull_subset face_of_imp_subset)
    show "affine hull T  S  T"
      using "*" convex T rel_interior_eq_empty by fastforce
  qed
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
    using "*" open_segment_commute by (fastforce simp add: face_of_def assms)
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: field_split_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)
      apply (rule_tac x="e / (e + norm (b - c))" in image_eqI)
      using False nbc 0 < e by (auto simp: algebra_simps)
    then have "d  T  c  T"
      by (meson b  T c  u d  u assms face_ofD subset_iff)
    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"
  using assms
  unfolding disjoint_iff_not_equal
  by (metis IntI empty_iff face_of_imp_subset mem_rel_interior_ball subset_antisym 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 = {}"
  using assms face_of_disjoint_rel_interior interior_subset_rel_interior by fastforce

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 subset_iff)

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"
    by (metis aff_dim_empty assms convex_rel_frontier_aff_dim face_of_imp_convex 
        face_of_subset_rel_frontier order_less_irrefl)
  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"
proof (rule subset_of_face_of [OF T U  S])
  show "T  rel_interior U  {}"
    using face_of_imp_eq_affine_Int [OF convex S T] rel_interior_subset dis U  S disjnt_def 
    by fastforce
qed

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 (meson antisym assms disjnt_def equalityD2 face_of_def 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] field_split_simps)
  then show ?thesis
    using affine S xy by (auto simp: affine_alt)
qed

proposition face_of_conic:
  assumes "conic S" "f face_of S"
  shows "conic f"
  unfolding conic_def
proof (intro strip)
  fix x and c::real
  assume "x  f" and "0  c"
  have f: "a b x. a  S; b  S; x  f; x  open_segment a b  a  f  b  f"
    using f face_of S face_ofD by blast
  show "c *R x  f"
  proof (cases "x=0  c=1")
    case True
    then show ?thesis
      using x  f by auto
  next
    case False
    with 0  c obtain d e where de: "0  d" "0  e" "d < 1" "1 < e" "d < e" "(d = c  e = c)"
      apply (simp add: neq_iff)
      by (metis gt_ex less_eq_real_def order_less_le_trans zero_less_one)
    then obtain [simp]: "c *R x  S" "e *R x  S" x  S
      using x  f assms conic_mul face_of_imp_subset by blast
    have "x  open_segment (d *R x) (e *R x)" if "c *R x  f"
      using de False that
      apply (simp add: in_segment)
      apply (rule_tac x="(1 - d) / (e - d)" in exI)
      apply (simp add: field_simps)
      by (smt (verit, del_insts) add_divide_distrib divide_self scaleR_collapse)
    then show ?thesis
      using conic S f [of "d *R x" "e *R x" x] de x  f
      by (force simp: conic_def in_segment)
  qed
qed

proposition 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: "(iS. a i *R i) = x"
                 and b: "i. i  S  0  b i" and bsum: "sum b S = 1" and beqy: "(iS. 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: "(iS. 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  "sum a T = 1"
        using assms by (metis sum.mono_neutral_cong_right a0 asum)
      moreover have "(xT. a x *R x) = x"
        using a0 assms by (auto simp: cge0 a aeqx [symmetric] sum.mono_neutral_right)
      ultimately show ?thesis
        using a assms(2) by (auto simp add: convex_hull_finite finite T )
    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 "sum c (S - T) = 1"
          by (simp add: S sum_diff sumc1)
        moreover 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 "(iS-T. c i *R i) = w"
          by (simp add: weq_sumsum)
        ultimately have "w  convex hull (S - T)"
          using cge0 by (auto simp add: convex_hull_finite fin)
        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 "x. x  T  0  inverse (1 - k) * c x"
          by (metis T  S cge0 inverse_nonnegative_iff_nonnegative mult_nonneg_nonneg subsetD sum_nonneg sumcf)
        moreover have "(xT. inverse (1 - k) * c x) = 1"
          by (metis False eq_iff_diff_eq_0 mult.commute right_inverse sum_distrib_left sumcf)
        ultimately have "(iT. c i *R i) /R (1 - k)  convex hull T"
          apply (simp add: convex_hull_finite fin)
          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 simp flip: sum_distrib_left k_def)
          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:
  assumes "finite S" "a  affine hull S" and T: "T face_of convex hull S"
  shows "T face_of convex hull insert a S"
proof -
  have "convex hull S face_of convex hull insert a S"
    by (simp add: assms face_of_convex_hulls insert_Diff_if subset_insertI)
  then show ?thesis
    using T face_of_trans by blast
qed

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"
        by (metis diff_add_cancel inverse_eq_divide midpoint_def midpoint_in_open_segment 
            scaleR_2 scaleR_half_double)
      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


proposition 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  λn. ((λr. insert (c r) r)^^n) {c{}}"
  note d_def [simp]
  have dSuc: "n. d (Suc n) = insert (c (d n)) (d n)"
    by simp
  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 by fastforce
qed

lemma faces_of_translation:
   "{F. F face_of (+) a ` S} = (image ((+) a)) ` {F. F face_of S}"
proof -
  have "F. F face_of (+) a ` S  G. G face_of S  F = (+) a ` G"
    by (metis face_of_imp_subset face_of_translation_eq subset_imageE)
  then show ?thesis
    by (auto simp: image_iff)
qed

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 linear_fst linear_snd)
    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 linear_fst linear_snd rel_interior_convex_linear_image [symmetric])
    have "C = fst ` C × snd ` C"
    proof (rule face_of_eq [OF C])
      show "fst ` C × snd ` C face_of S × S'"
        by (simp add: face_of_Times rel_interior_Times conv fst snd)
      show "rel_interior C  rel_interior (fst ` C × snd ` C)  {}"
        using False rel_interior_eq_empty convex C cc
        by (auto simp: face_of_Times rel_interior_Times conv fst)
    qed
    with fst snd show ?thesis by metis
  qed
qed (use face_of_Times in auto)

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 face_of {x. a  x = b}" if "F  {x. a  x  b}"
    proof -
      have "F face_of rel_frontier {x. a  x  b}"
      proof (rule face_of_subset [OF L])
        show "F  rel_frontier {x. a  x  b}"
          by (simp add: L face_of_subset_rel_frontier that)
      qed (force simp: rel_frontier_def closed_halfspace_le)
      then show ?thesis
        using False 
        by (simp add: frontier_halfspace_le rel_frontier_nonempty_interior [OF ine])
    qed
    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›

definitiontag important› 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"
proof -
  have "S  {x. 0  x  1}  {} = S  {x. 0  x = 1}"
    by force
  then show ?thesis
    using exposed_face_of_def by blast
qed

lemma exposed_face_of_refl_eq [simp]: "S exposed_face_of S  convex S"
proof
  assume S: "convex S"
  have "S  {x. 0  x  0}  S = S  {x. 0  x = 0}"
    by auto
  with S show "S exposed_face_of S"
    using exposed_face_of_def face_of_refl_eq by blast
qed (simp add: exposed_face_of_def face_of_refl_eq)

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}))"
     (is "?lhs = ?rhs")
proof
  show "?lhs  ?rhs"
    by (smt (verit) Collect_cong exposed_face_of_def hyperplane_eq_empty inf.absorb_iff1
                    inf_bot_right inner_zero_left)
  show "?rhs  ?lhs"
    using exposed_face_of_def face_of_imp_convex by fastforce
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)
  have "S  {x. (a + a')  x  b + b'}  T  U = S  {x. (a + a')  x = b + b'}"
    using S s' by (fastforce simp: ss inner_left_distrib teq ueq)
  then show ?thesis
    using exposed_face_of_def tu by auto
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
      by (induction Q rule: finite_induct; use exposed_face_of_Int in fastforce)
    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"
    proof (rule exposed_face_of_Int_supporting_hyperplane_le [OF convex S])
      show "x. x  S  u  x  u  a0"
        by (metis p z add_le_cancel_right inner_right_distrib lez [OF _ b0  T])
    qed
    have tef: "T  {x. u  x = u  b0} exposed_face_of T"
    proof (rule exposed_face_of_Int_supporting_hyperplane_le [OF convex T])
      show "x. x  T  u  x  u  b0"
        by (metis p z add.commute add_le_cancel_right inner_right_distrib lez [OF a0  S])
    qed
    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}"
    proof -
      have "x y. z = u  (x + y); x  S; y  T
            u  x = u  a0  u  y = u  b0"
        by (smt (verit, best) z p a0  S b0  T inner_right_distrib lez)
      then show ?thesis
        using feq by blast
    qed
    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

proposition 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'}"
        by (rule *) (use le eq Ssub in 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›

definitiontag important› 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"
  by (metis disjoint_iff face_of_disjoint_rel_interior face_of_singleton insertI1)

lemma extreme_point_not_in_interior:
  fixes S :: "'a::{real_normed_vector, perfect_space} set"
  assumes "x extreme_point_of S" shows "x  interior S"
  using assms extreme_point_not_in_REL_INTERIOR interior_subset_rel_interior by fastforce

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"
  using hull_minimal [of S "(convex hull S) - {x}" convex]
  using hull_subset [of S convex]
  by (force simp add: extreme_point_of_stillconvex)

proposition 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_points_of_translation_subtract:
   "{x. x extreme_point_of (image (λx. x - a) S)} =
    (λx. x - a) ` {x. x extreme_point_of S}"
  using extreme_points_of_translation [of "- a" S]
  by simp

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"
  by (metis convex_singleton face_of_Int_supporting_hyperplane_le_strong face_of_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"
  using extreme_point_of_Int_supporting_hyperplane_le [of S "-a" "-b" c]
  by simp

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"
  unfolding exposed_face_of_def
  by (force simp: face_of_singleton extreme_point_of_Int_supporting_hyperplane_le)

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:
  assumes "finite S" "a  convex hull S"
  shows "a extreme_point_of (convex hull (insert a S))"
proof (cases "a  S")
  case False
  then show ?thesis
   using face_of_convex_hulls [of "insert a S" "{a}"] assms
   by (auto simp: face_of_singleton hull_same)
qed (use assms  in simp add: hull_inc)

lemma extreme_point_of_conic:
  assumes "conic S" and x: "x extreme_point_of S"
  shows "x = 0"
proof -
  have "{x} face_of S"
    by (simp add: face_of_singleton x)
  then have "conic{x}"
    using assms(1) face_of_conic by blast
  then show ?thesis
    by (force simp: conic_def)
qed

subsection‹Facets›

definitiontag important› 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
      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
      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› (*FIXME too small subsection, rearrange? *)

definitiontag important› 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›

proposition 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
    show False
      by (metis dist_0_norm dist_decreases_open_segment noax nobx not_le x)
  qed
  then show ?thesis
    by (meson x  S extreme_point_of_def that)
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"
    by (simp add: closed S assms closure_minimal extreme_point_of_def hull_minimal)
  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 less.prems 
    show ?thesis
      by (metis subsetD convex_convex_hull convex_rel_interior_closure 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"
      using face_of_Int_supporting_hyperplane_ge le_ay convex S 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 face 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_subtract cong: image_cong_simp)
    have 2: "convex ((+) (- a) ` S)"
      by (simp add: convex S compact_translation_subtract)
    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_subtract translation_assoc cong: image_cong_simp)
    qed
next
  show "convex hull {x. x extreme_point_of S}  S"
    using convex S extreme_point_of_stillconvex subset_hull by fastforce
qed


subsection‹Applying it to convex hulls of explicitly indicated finite sets›

corollary 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"
  by (simp add: extreme_point_of_convex_hull_affine_independent)

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'"
proof
  show "{x. x extreme_point_of T}  S"
    using T extreme_point_of_convex_hull extreme_point_of_face by blast
  show "T = convex hull {x. x extreme_point_of T}"
    by (metis Krein_Milman_Minkowski assms compact_convex_hull convex_convex_hull 
        face_of_imp_compact face_of_imp_convex)
qed


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: field_split_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"
        by (simp add: FeqT True hull_inc hull_minimal)
    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 -
        have xah: "x  affine hull S"
          using F convex_hull_subset_affine_hull face_of_imp_subset x  F by blast
        have ah: "b  affine hull S" "c  affine hull S" 
          using b c convex_hull_subset_affine_hull by blast+
        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"
          by (rule face_of_convex_hull_aux) (use b c xah ah that in auto simp: algebra_simps)
        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  ub ub  1 v < 1 uxx x  F by force
        next
          case False
          show ?thesis
          proof (cases "ub = 0")
            case True
            then show ?thesis
              using equx 0  uc uc  1 0 < v uxx x  F by force
          next
            case False
            then have "0 < ub" "0 < uc"
              using uc  0 0  ub 0  uc by auto
            then have "(1 - v) * ub > 0" "v * uc > 0"
              by (simp_all add: 0 < uc 0 < v v < 1)
            then have "ux  0"
              using equx 0 < v by auto
            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: field_split_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: field_split_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) = {}"
    by (intro disjoint_affine_hull [OF assms C  S], auto)
  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"
    by (smt (verit) c  S aff_dim_affine_independent aff_independent_finite assms card_Diff_subset 
        card_mono of_nat_diff of_nat_eq_1_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 "aff_dim (S - {u}) = aff_dim S - 1"
    using assms u  S
    unfolding affine_dependent_def
    by (metis add_diff_cancel_right' aff_dim_insert insert_Diff [of u S])
  then have "aff_dim (convex hull (S - {u})) = aff_dim (convex hull S) - 1"
    by (simp add: aff_dim_convex_hull)
  then show ?lhs
    by (metis Diff_subset T  {} assms face_of_convex_hull_affine_independent facet_of_def u)
qed

lemma facet_of_convex_hull_affine_independent_alt:
  fixes S :: "'a::euclidean_space set"
  assumes "¬ affine_dependent S"
  shows "(T facet_of (convex hull S)  2  card S  (u. u  S  T = convex hull (S - {u})))"
        (is "?lhs = ?rhs")
proof
  assume L: ?lhs 
  then obtain x where
    "x  S" and x: "T = convex hull (S - {x})" and "finite S"
    using assms facet_of_convex_hull_affine_independent aff_independent_finite by blast
  moreover have "Suc (Suc 0)  card S"
    using L  x x  S finite S
    by (metis Suc_leI assms card.remove convex_hull_eq_empty card_gt_0_iff facet_of_convex_hull_affine_independent finite_Diff not_less_eq_eq)
  ultimately show ?rhs
    by auto
next
  assume ?rhs then show ?lhs
    using assms
    by (auto simp: facet_of_convex_hull_affine_independent Set.subset_singleton_iff)
qed

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


proposition 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"
  proof (rule hull_mono)
    show "{x. x extreme_point_of S}  frontier S"
      using closure_subset
      by (auto simp: frontier_def extreme_point_not_in_interior extreme_point_of_def)
  qed
  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›

definitiontag important› polytope where
 "polytope S  v. finite v  S = convex hull v"

lemma polytope_translation_eq: "polytope ((+) a ` S)  polytope S"
  unfolding polytope_def
  by (metis (no_types, opaque_lifting) add.left_inverse convex_hull_translation finite_imageI image_add_0 translation_assoc)

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)

proposition 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›

definitiontag important› 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 (clarsimp simp add: polyhedron_def)
  subgoal for F G
    by (rule_tac x="F  G" in exI, auto)
  done

lemma polyhedron_UNIV [iff]: "polyhedron UNIV"
  using polyhedron_def by 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 -
  define i::'a where "(i  SOME i. i  Basis)"
  have "a. a  0  (b. {x. i  x  -1} = {x. a  x  b})"
    by (rule_tac x="i" in exI) (force simp: i_def SOME_Basis nonzero_Basis)
  moreover have "a b. a  0  {x. -i  x  - 1} = {x. a  x  b}"
    by (metis Basis_zero SOME_Basis i_def neg_0_equal_iff_equal)
  ultimately show ?thesis
    unfolding polyhedron_def
    by (rule_tac x="{{x. i  x  -1}, {x. -i  x  -1}}" in exI) force
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_finite_intersection_hyperplanes hull_same polyhedron_Inter polyhedron_hyperplane)

lemma polyhedron_imp_closed:
  fixes S :: "'a :: euclidean_space set"
  shows "polyhedron S  closed S"
  by (metis closed_Inter closed_halfspace_le polyhedron_def)

lemma polyhedron_imp_convex:
  fixes S :: "'a :: euclidean_space set"
  shows "polyhedron S  convex S"
  by (metis convex_Inter convex_halfspace_le polyhedron_def)

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›

proposition 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}))"
  by (metis hull_subset inf.absorb_iff2 polyhedron_Int polyhedron_affine_hull polyhedron_def)

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 field_split_simps norm_minus_commute)
    finally have lte: "norm (ξ *R x - ξ *R z) < e" .
    have ξ_aff: "ξ *R z + (1 - ξ) *R x  affine hull S"
      by (simp add: x  S hull_inc mem_affine zaff)
    have "ξ *R z + (1 - ξ) *R x  S"
      using ins [OF _ ξ_aff] by (simp add: algebra_simps lte)
    then obtain l where l: "0 < l" "l < 1" and ls: "(l *R z + (1 - l) *R x)  S"
      using e > 0 z  x  
      by (rule_tac l = ξ in that) (auto simp: ξ_def)
    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. hF. y  interior h; y  affine hull S  y  S"
      by (metis IntI Inter_iff subsetD interior_subset seq)
    show ?thesis
      apply (simp add: rel_interior x  S)
      apply (rule_tac x="hF. 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 affine_hull_eq_empty inf.absorb_iff1 inf_assoc inf_bot_left 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
    let ?F = "(λh. {x. a h  x  b h}) ` {h  F. ¬ affine hull S  h}"
    show ?thesis
    proof (intro exI conjI)
      show "finite ?F"
        using finite F by force
      show "S = affine hull S   ?F"
        by (subst seq) (auto simp: ab INT_extend_simps)
    qed (use ab in blast)
  qed
next
  assume ?rhs then show ?lhs
    by (metis polyhedron_Int_affine)
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: "S  affine hull S  F'" if "F'  F" for F'
    using * [OF that] by (metis IntE aff inf.strict_order_iff that)
  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'))"
  by (metis polyhedron_Int_affine polyhedron_Int_affine_parallel_minimal)

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"
    unfolding polyhedron_Int_affine by (metis finite F faceq seq)
  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. hF. 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. hF  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 field_split_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"
      proof (rule mult_left_mono)
        show "a i  z  b i"
          by (metis DiffI Inter_iff empty_iff faceq insertE mem_Collect_eq that zint)
      qed (use 0 < l in auto)
      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)
    let ?F = "{x. a h  x = b h}"
    have faceS: "S  ?F face_of S"
    proof (rule face_of_Int_supporting_hyperplane_le)
      show "x. x  S  a h  x  b h"
        using faceq seq that by fastforce
    qed fact
    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 ne: "S  ?F  {}" by blast
    moreover have "affine hull (S  ?F) = (affine hull S)  ?F"
    proof
      show "affine hull (S  ?F)  affine hull S  ?F"
      proof -
        have "affine hull (S  ?F)  affine hull S"
          by (simp add: hull_mono)
        then show ?thesis
          by (simp add: affine_hyperplane subset_hull)
      qed
    next
      show "affine hull S  ?F  affine hull (S  ?F)"
      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
          let ?body = "(λj. if 0 < a j  y - a j  w
              then (b j - a j  w) / (a j  y - a j  w) else 1) ` (F - {h})"
          define inff where "inff = Inf ?body"
          from finite F have "finite ?body"
            by blast
          moreover from h' have "?body  {}"
            by blast
          moreover have "j > 0" if "j  ?body" for j
          proof -
            from that obtain x where "x  F" and "x  h" and *: "j =
              (if 0 < a x  y - a x  w
                then (b x - a x  w) / (a x  y - a x  w) else 1)"
              by blast
            with awlt [of x] have "a x  w < b x"
              by simp
            with * show ?thesis
              by simp
          qed
          ultimately have "0 < inff"
            by (simp_all add: finite_less_Inf_iff inff_def)
          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)"
              unfolding inff_def
              using finite F by (auto intro: cInf_le_finite simp add: that split: if_split_asm)
            then show ?thesis
              using 0 < inff awlt [OF that] mult_strict_left_mono
              by (fastforce simp add: field_split_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"
          using yaff w  affine hull S affine_affine_hull affine_alt by blast
        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 have "aff_dim (affine hull (S  ?F)) = aff_dim S - 1"
      using b h < a h  z zaff by (force simp: aff_dim_affine_Int_hyperplane)
    then show ?thesis
      by (simp add: ne faceS facet_of_def)
  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. hF. 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}"
    proof (rule subset_of_face_of [of _ S])
      show "S  {x. a i  x = b i} face_of S"
        by (simp add: "*" i  F facet_of_imp_face_of)
      show "C  S"
        by (simp add: C face_of S face_of_imp_subset)
      show "S  {x. a i  x = b i}  rel_interior C  {}"
        using a i  x = b i x  S x by blast
    qed
    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)
      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"
    by (metis finite F faceq polyhedron_Int polyhedron_Inter polyhedron_affine_hull polyhedron_halfspace_le 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
    using faceq seq face_of_Int_supporting_hyperplane_le 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. hF. 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
  proof
    show "C  S  {x. a i  x = b i}"
      using subset_of_face_of [OF face C  S] a i  x = b i x  rel_interior C x  S by blast
  qed fact
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"
    by (metis finite F faceq polyhedron_Int polyhedron_Inter polyhedron_affine_hull polyhedron_halfspace_le seq)
  then have "convex S"
    by (simp add: polyhedron_imp_convex)
  then have *: "(S  ?ab h) face_of S" if "h  F" for h
    using faceq seq face_of_Int_supporting_hyperplane_le 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. hF. 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"
      by (metis "*" Collect_cong IntI C  S empty_iff subset_of_face_of that z)
  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"
      using that z  S by (intro hull_mono) 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"
    using assms
    by (metis face_of_polyhedron_subset_explicit [OF finite F seq faceq psub] le_inf_iff)
  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::'a set. 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}"
    by (rule red) (metis seq bsub)
  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
    using z zinrel
    by (intro face_of_eq [OF C fac]) (force simp: **)
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}"
     using i  F ab by (subst seq) 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 "{G. G facet_of S  F  G} exposed_face_of S"
      by (metis (no_types, lifting) mem_Collect_eq exposed_face_of_Inter)
    then show ?thesis
      using False F face_of S assms face_of_polyhedron by fastforce
  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 (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"
  assumes "polyhedron S" shows "finite {v. v extreme_point_of S}"
proof -
  have "finite {v. {v} face_of S}"
    using assms by (intro finite_subset [OF _ finite_vimageI [OF finite_polyhedron_faces]], auto)
  then show ?thesis
    by (simp add: face_of_singleton)
qed

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. hF. 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 2 that x  F show ?thesis
        by blast
      qed
  qed
  moreover have "hF. 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}"
proof
  show "rel_frontier S   {F. F face_of S  F  S}"
    by (force simp: rel_frontier_of_polyhedron facet_of_def assms)
qed (use face_of_subset_rel_frontier in 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 blast+
    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)
      have oS: "openin (top_of_set (closed_segment c p)) (closed_segment c p  rel_interior S)"
        by (force simp: openin_rel_interior openin_Int intro: openin_subtopology_Int_subset [OF _ ccp])
      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 (drule mp [OF _ oS])
        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"
          using F_def x  S sex sns by blast
        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
    let ?S' = "affine hull S  {{x. a h  x  b h} |h. h  F}"
    have "S  ?S'"
      using ab by (auto simp: hull_subset)
    moreover have "?S'  S"
      using * by blast
    ultimately have "S = ?S'" ..
    moreover have "polyhedron ?S'"
      by (force intro: polyhedron_affine_hull polyhedron_halfspace_le simp: finite F)
    ultimately show ?thesis
      by auto
  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 [simp]: "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)
  { fix P
    have "x. P x  x  (`) h ` {f. P (h ` f)}" 
      using bij_is_surj [OF bij h]
      by (metis image_eqI mem_Collect_eq subset_imageE top_greatest)
    then have "{f. P f} = (image h) ` {f. P (h ` f)}"
      by force
  } 
  then have "finite {F. F face_of h ` S} =finite {F. F face_of S}"
    using linear h 
    by (simp add: finite_image_iff injim flip: face_of_linear_image [of h _ S])
  then show ?thesis
    using linear h 
    by (simp add: polyhedron_eq_finite_faces closed_injective_linear_image_eq)
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›

proposition 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 R: ?rhs 
  then have "finite {v. v extreme_point_of S}"
    by (simp add: finite_polyhedron_extreme_points)
  moreover have "S = convex hull {v. v extreme_point_of S}"
    using R by (simp add: Krein_Milman_Minkowski compact_eq_bounded_closed polyhedron_imp_closed polyhedron_imp_convex)
  ultimately show ?lhs
    unfolding polytope_def by blast
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) = (aS. 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 "int (card T)  aff_dim S + 1"  "finite T" "T  S""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 "yS. x  convex hull (S - {y})"
        using True affine_independent_iff_card [of S]
        by (metis (no_types, opaque_lifting) Diff_eq_empty_iff Diff_insert0 a  T T  S x  convex hull T hull_mono insert_Diff_single subsetCE)
    } note * = this
    have 1: "convex hull S  ( aS. convex hull (S - {a}))"
      by (subst caratheodory_aff_dim) (blast dest: *)
    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])
      using "1" "2" by auto
next
  case False
  then have "frontier (convex hull S) = closure (convex hull S) - interior (convex hull S)"
    by (simp add: rel_boundary_of_convex_hull frontier_def)
  also have " = (convex hull S) - rel_interior(convex hull S)"
    by (metis False 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_remove 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"
      using a>0 by (simp add: distrib_right floor_divide_lower)
    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"
      using a>0 by (simp add: distrib_right floor_divide_lower)
    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"
      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  𝒢. 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"
                   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"
      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. xC. 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"
  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"
                "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 "C  {x  . - B / (e / 2 / real DIM('a))  x  x  B / (e / 2 / real DIM('a))}"
    using 0 < e by (auto simp: field_split_simps C_def)
  then have "finite C"
    using finite_int_segment finite_subset by blast
  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"
              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 by auto
  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 blast+
          have "norm (x - y)  (bBasis. ¦(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[of X x y] X  ℱ' that unfolding I_def by auto
            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 termn  -1

definitiontag important› 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, opaque_lifting) 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}"
  using affine_independent_1 simplex_convex_hull by fastforce

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})"
  by (metis aff_dim_eq_0 aff_dim_simplex simplex_sing)

lemma one_simplex_segment: "a  b  1 simplex closed_segment a b"
  unfolding simplex_def
  by (rule_tac x="{a,b}" in exI) (auto simp: segment_convex_hull)

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›

definitiontag important› 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)"

definitiontag important› triangulation where
 "triangulation 𝒯 
        finite 𝒯 
        (T  𝒯. n. n simplex T) 
        (T T'. T  𝒯  T'  𝒯  (T  T') face_of T)"


subsection‹Refining a cell complex to a simplicial complex›

proposition 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 "(xT. closed_segment z x)  (xU. closed_segment z x)
           (if T  U = {} then {z} else ((closed_segment z) ` (T  U)))" (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
            by (meson between_antisym between_mem_segment between_trans_2 ends_in_segment(2))
          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"
    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"
    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 using True
      by (rule_tac x="" in exI) (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)"
      "C1 C2. C1  𝒮; C2  𝒮   C1  C2 face_of C1"
      using less.prems by (auto simp: 𝒮_def)
    moreover have §: "C F. C  𝒮; F face_of C  F  𝒮"
      using less.prems unfolding 𝒮_def 
      by (metis (no_types, lifting) mem_Collect_eq aff_dim_subset face_of_imp_subset less_le not_le)
    ultimately 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"
      using less.IH [of "n-1" 𝒮] False 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"
      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 (simp add: inf_commute)
        moreover have "L  C  C"
          using C  𝒩 L  𝒮
          by (metis (mono_tags, lifting) 𝒩_def 𝒮_def intfaceℳ mem_Collect_eq not_le order_refl §)
        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: "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"
                  by (simp add: F = convex hull J hull_mono hull_subset subset_insert_iff)
                moreover have "?F  F"
                  by (metis True F = convex hull J hull_insert insert_Diff set_eq_subset)
                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 J K = convex hull I face𝒰 subset_insert K  𝒰)
              then show "F  𝒰  ?𝒯"
                by blast
            qed
          qed
          ultimately show ?thesis
            using that by auto
        qed
        have §: "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"
          proof (rule Int_convex_hull_insert_rel_exterior [OF convex C K  C z])
            show "disjnt X (rel_interior C)"
              using DC by (meson X  D disjnt_def disjnt_subset1)
          qed
          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: XY(1) K  𝒰 faceI𝒰 inf_commute)
          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
            by (simp add: XY(1) Y K  𝒰 eq faceI𝒰)
        qed

        show "S  S' face_of S"
          if "S  𝒰  ?𝒯  S'  𝒰  ?𝒯" for S S'
          using that
        proof (elim conjE UnE)
          fix X Y
          assume "X  𝒰" and "Y  𝒰"
          then show "X  Y face_of X"
            by (simp add: faceI𝒰)
        next
          fix X Y
          assume XY: "X  𝒰" "Y  ?𝒯"
          then show "X  Y face_of X" "Y  X face_of Y"
            using § [OF XY] by (auto simp: Int_commute)
        next
          fix X Y
          assume XY: "X  ?𝒯" "Y  ?𝒯"
          show "X  Y face_of X"
          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
              have "convex hull insert (SOME z. z  rel_interior C) (K  L) face_of
                    convex hull insert (SOME z. z  rel_interior C) K"
                by (metis IntI C  𝒩 K  𝒰 K  rel_frontier C L  𝒰 ahK_C_disjoint empty_iff faceI𝒰 face_of_polytope_insert2 simpl𝒰 simplex_imp_polytope z)
              then show ?thesis
                using True X Y K  rel_frontier C L  rel_frontier C convex C convex K convex L convex_hull_insert_Int_eq z by force
            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 Int_commute 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 K  C convex C in_mono insert_subsetI rel_interior_subset subset_hull z)
              have "disjnt (convex hull insert (SOME z. z  rel_interior C) K) (rel_interior D)"
                using zKC CD by (force simp: disjnt_def)
              then have eq: "convex hull (insert ?z K)  convex hull (insert ?w L) =
                             convex hull (insert ?z K)  convex hull L"
                by (rule Int_convex_hull_insert_rel_exterior [OF convex D L  D w])
              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"
                    by (metis inf_commute C   D   ¬ C face_of D intfaceℳ)
                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 convex K aff_independent_finite face_of_convex_hull_insert_eq face_of_refl hull_insert 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 (metis K  𝒰 L  𝒰 chKL ch_id faceI𝒰 inf_commute)
              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 convex L aff_independent_finite 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
      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"
      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}) 
            (CC. {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
    fix F1 F2
    assume "F1  (C. {F. F face_of C})" and "F2  (C. {F. F face_of C})"
    then obtain C1 C2 where "C1  " "C2  " and F: "F1 face_of C1" "F2 face_of C2"
      by auto
    show "F1  F2 face_of F1"
      using face_of_Int_subface [OF _ _ F]
      by (metis C1   C2   face inf_commute)
  qed
  moreover
  have "(C. {F. F face_of C}) = "
    using face_of_imp_subset face by blast
  ultimately show ?thesis
    using face_of_imp_subset n
    by (fastforce intro!: that simp add: poly face_of_refl polytope_imp_convex)
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"
  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"
  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"
               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 (top_of_set U) (U-C)"
          by (metis Sup_upper clo closed_limpt closedin_limpt eq openin_diff openin_subtopology_self)
        then show "openin (top_of_set 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)
        then 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
          by (metis Diff_iff Sup_upper UnionE aff_dim_subset eq order_less_le that)
        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"
  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
section ‹Finitely generated cone is polyhedral, and hence closed›

proposition polyhedron_convex_cone_hull:
  fixes S :: "'a::euclidean_space set"
  assumes "finite S"
  shows "polyhedron(convex_cone hull S)"
proof (cases "S = {}")
  case True
  then show ?thesis
    by (simp add: affine_imp_polyhedron)
next
  case False
  then have "polyhedron(convex hull (insert 0 S))"
    by (simp add: assms polyhedron_convex_hull)
  then obtain F a b where "finite F" 
         and F: "convex hull (insert 0 S) =  F" 
         and ab: "h. h  F  a h  0  h = {x. a h  x  b h}"
    unfolding polyhedron_def by metis
  then have "F  {}"
    by (metis bounded_convex_hull finite_imp_bounded Inf_empty assms finite_insert not_bounded_UNIV)
  show ?thesis
    unfolding polyhedron_def
  proof (intro exI conjI)
    show "convex_cone hull S =  {h  F. b h = 0}" (is "?lhs = ?rhs")
    proof
      show "?lhs  ?rhs"
      proof (rule hull_minimal)
        show "S   {h  F. b h = 0}"
          by (smt (verit, best) F InterE InterI hull_subset insert_subset mem_Collect_eq subset_eq)
        have "S. S  F; b S = 0  convex_cone S"
          by (metis ab convex_cone_halfspace_le)
        then show "convex_cone ( {h  F. b h = 0})"
          by (force intro: convex_cone_Inter)
      qed
      have "x  convex_cone hull S"
        if x: "h. h  F; b h = 0  x  h" for x
      proof -
        have "t. 0 < t  (t *R x)  h" if "h  F" for h
        proof (cases "b h = 0")
          case True
          then show ?thesis
            by (metis x linordered_field_no_ub mult_1 scaleR_one that zero_less_mult_iff)
        next
          case False
          then have "b h > 0"
            by (smt (verit, del_insts) F InterE ab hull_subset inner_zero_right insert_subset mem_Collect_eq that)
          then have "0  interior {x. a h  x  b h}"
            by (simp add: ab that)
          then have "0  interior h"
            using ab that by auto
          then obtain ε where "0 < ε" and ε: "ball 0 ε  h"
            using mem_interior by blast
          show ?thesis
          proof (cases "x=0")
            case True
            then show ?thesis
              using ε 0 < ε by auto
          next
            case False
            with ε 0 < ε show ?thesis
              by (rule_tac x="ε / (2 * norm x)" in exI) (auto simp: divide_simps)
          qed
        qed
        then obtain t where t: "h. h  F  0 < t h  (t h *R x)  h" 
          by metis
        then have "Inf (t ` F) *R x /R Inf (t ` F) = x"
          by (smt (verit) F  {} finite F divideR_right finite_imageI finite_less_Inf_iff image_iff image_is_empty)
        moreover have "Inf (t ` F) *R x /R Inf (t ` F)  convex_cone hull S"
        proof (rule conicD [OF conic_convex_cone_hull])
          have "Inf (t ` F) *R x   F"
          proof clarify
            fix h
            assume  "h  F"
            have eq: "Inf (t ` F) *R x = (1 - Inf(t ` F) / t h) *R 0 + (Inf(t ` F) / t h) *R t h *R x"
              using h  F t by force
            show "Inf (t ` F) *R x  h"
              unfolding eq
            proof (rule convexD_alt)
              have "h = {x. a h  x  b h}"
                by (simp add: h  F ab)
              then show "convex h"
                by (metis convex_halfspace_le)
              show "0  h"
                by (metis F InterE h  F hull_subset insertCI subsetD)
              show "t h *R x  h"
                by (simp add: h  F t)
              show "0  Inf (t ` F) / t h"
                by (metis F  {} h  F cINF_greatest divide_nonneg_pos less_eq_real_def t)
              show "Inf (t ` F) / t h  1"
                by (simp add: finite F h  F cInf_le_finite t)
            qed
          qed
          moreover have "convex hull (insert 0 S)  convex_cone hull S"
            by (simp add: convex_cone_hull_contains_0 convex_convex_cone_hull hull_minimal hull_subset)
          ultimately show "Inf (t ` F) *R x  convex_cone hull S"
            using F by blast
          show "0  inverse (Inf (t ` F))"
            using t by (simp add: F  {} finite F finite_less_Inf_iff less_eq_real_def)
        qed
        ultimately show ?thesis
          by auto
      qed
      then show "?rhs  ?lhs"
        by auto
    qed
    show "h{h  F. b h = 0}. a b. a  0  h = {x. a  x  b}"
      using ab by blast
  qed (auto simp: finite F)
qed


lemma closed_convex_cone_hull:
  fixes S :: "'a::euclidean_space set"
  shows "finite S  closed(convex_cone hull S)"
  by (simp add: polyhedron_convex_cone_hull polyhedron_imp_closed)

lemma polyhedron_convex_cone_hull_polytope:
  fixes S :: "'a::euclidean_space set"
  shows "polytope S  polyhedron(convex_cone hull S)"
  by (metis convex_cone_hull_separate hull_hull polyhedron_convex_cone_hull polytope_def)

lemma polyhedron_conic_hull_polytope:
  fixes S :: "'a::euclidean_space set"
  shows "polytope S  polyhedron(conic hull S)"
  by (metis conic_hull_eq_empty convex_cone_hull_separate_nonempty hull_hull polyhedron_convex_cone_hull_polytope polyhedron_empty polytope_def)

lemma closed_conic_hull_strong:
  fixes S :: "'a::euclidean_space set"
  shows "0  rel_interior S  polytope S  compact S  ~(0  S)  closed(conic hull S)"
  using closed_conic_hull polyhedron_conic_hull_polytope polyhedron_imp_closed by blast

end