# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1501165355 -3600
# Node ID d425bdf419f5d86687ea3815398d70431cc2676e
# Parent  33a47f2d9edc8984d6feb80e3af1c1f825468e66
polytopes: simplical subdivisions, etc.

diff -r 33a47f2d9edc -r d425bdf419f5 src/HOL/Analysis/Linear_Algebra.thy
--- a/src/HOL/Analysis/Linear_Algebra.thy	Wed Jul 26 16:07:45 2017 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Jul 27 15:22:35 2017 +0100
@@ -79,20 +79,27 @@
 lemma hull_inc: "x \<in> S \<Longrightarrow> x \<in> P hull S"
   by (metis hull_subset subset_eq)
 
-lemma hull_union_subset: "(S hull s) \<union> (S hull t) \<subseteq> (S hull (s \<union> t))"
+lemma hull_Un_subset: "(S hull s) \<union> (S hull t) \<subseteq> (S hull (s \<union> t))"
   unfolding Un_subset_iff by (metis hull_mono Un_upper1 Un_upper2)
 
-lemma hull_union:
+lemma hull_Un:
   assumes T: "\<And>T. Ball T S \<Longrightarrow> S (\<Inter>T)"
   shows "S hull (s \<union> t) = S hull (S hull s \<union> S hull t)"
-  apply rule
-  apply (rule hull_mono)
-  unfolding Un_subset_iff
-  apply (metis hull_subset Un_upper1 Un_upper2 subset_trans)
-  apply (rule hull_minimal)
-  apply (metis hull_union_subset)
-  apply (metis hull_in T)
-  done
+  apply (rule equalityI)
+  apply (meson hull_mono hull_subset sup.mono)
+  by (metis hull_Un_subset hull_hull hull_mono)
+
+lemma hull_Un_left: "P hull (S \<union> T) = P hull (P hull S \<union> T)"
+  apply (rule equalityI)
+   apply (simp add: Un_commute hull_mono hull_subset sup.coboundedI2)
+  by (metis Un_subset_iff hull_hull hull_mono hull_subset)
+
+lemma hull_Un_right: "P hull (S \<union> T) = P hull (S \<union> P hull T)"
+  by (metis hull_Un_left sup.commute)
+
+lemma hull_insert:
+   "P hull (insert a S) = P hull (insert a (P hull S))"
+  by (metis hull_Un_right insert_is_Un)
 
 lemma hull_redundant_eq: "a \<in> (S hull s) \<longleftrightarrow> S hull (insert a s) = S hull s"
   unfolding hull_def by blast
diff -r 33a47f2d9edc -r d425bdf419f5 src/HOL/Analysis/Polytope.thy
--- a/src/HOL/Analysis/Polytope.thy	Wed Jul 26 16:07:45 2017 +0100
+++ b/src/HOL/Analysis/Polytope.thy	Thu Jul 27 15:22:35 2017 +0100
@@ -1230,6 +1230,179 @@
 by (metis (no_types) Krein_Milman_Minkowski assms compact_convex_hull convex_convex_hull face_of_imp_compact face_of_imp_convex)
 
 
+lemma face_of_convex_hull_aux:
+  assumes eq: "x *\<^sub>R p = u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c"
+    and x: "u + v + w = x" "x \<noteq> 0" and S: "affine S" "a \<in> S" "b \<in> S" "c \<in> S"
+  shows "p \<in> S"
+proof -
+  have "p = (u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c) /\<^sub>R x"
+    by (metis \<open>x \<noteq> 0\<close> eq mult.commute right_inverse scaleR_one scaleR_scaleR)
+  moreover have "affine hull {a,b,c} \<subseteq> S"
+    by (simp add: S hull_minimal)
+  moreover have "(u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c) /\<^sub>R x \<in> affine hull {a,b,c}"
+    apply (simp add: affine_hull_3)
+    apply (rule_tac x="u/x" in exI)
+    apply (rule_tac x="v/x" in exI)
+    apply (rule_tac x="w/x" in exI)
+    using x apply (auto simp: algebra_simps divide_simps)
+    done
+  ultimately show ?thesis by force
+qed
+
+proposition face_of_convex_hull_insert_eq:
+  fixes a :: "'a :: euclidean_space"
+  assumes "finite S" and a: "a \<notin> affine hull S"
+  shows "(F face_of (convex hull (insert a S)) \<longleftrightarrow>
+          F face_of (convex hull S) \<or>
+          (\<exists>F'. F' face_of (convex hull S) \<and> F = convex hull (insert a F')))"
+         (is "F face_of ?CAS \<longleftrightarrow> _")
+proof safe
+  assume F: "F face_of ?CAS"
+    and *: "\<nexists>F'. F' face_of convex hull S \<and> F = convex hull insert a F'"
+  obtain T where T: "T \<subseteq> insert a S" and FeqT: "F = convex hull T"
+    by (metis F \<open>finite S\<close> compact_insert finite_imp_compact face_of_convex_hull_subset)
+  show "F face_of convex hull S"
+  proof (cases "a \<in> T")
+    case True
+    have "F = convex hull insert a (convex hull T \<inter> convex hull S)"
+    proof
+      have "T \<subseteq> insert a (convex hull T \<inter> convex hull S)"
+        using T hull_subset by fastforce
+      then show "F \<subseteq> convex hull insert a (convex hull T \<inter> convex hull S)"
+        by (simp add: FeqT hull_mono)
+      show "convex hull insert a (convex hull T \<inter> convex hull S) \<subseteq> F"
+        apply (rule hull_minimal)
+        using True by (auto simp: \<open>F = convex hull T\<close> hull_inc)
+    qed
+    moreover have "convex hull T \<inter> 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: \<open>F face_of convex hull S\<close> a face_of_convex_hull_insert \<open>finite S\<close>)
+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 \<notin> 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: \<open>F = {}\<close> \<open>finite S\<close> extreme_point_of_convex_hull_insert face_of_singleton)
+    next
+      case False
+      have "convex hull insert a F \<subseteq> ?CAS"
+        by (simp add: F a \<open>finite S\<close> convex_hull_subset face_of_convex_hull_insert face_of_imp_subset hull_inc)
+      moreover
+      have "(\<exists>y v. (1 - ub) *\<^sub>R a + ub *\<^sub>R b = (1 - v) *\<^sub>R a + v *\<^sub>R y \<and>
+                   0 \<le> v \<and> v \<le> 1 \<and> y \<in> F) \<and>
+            (\<exists>x u. (1 - uc) *\<^sub>R a + uc *\<^sub>R c = (1 - u) *\<^sub>R a + u *\<^sub>R x \<and>
+                   0 \<le> u \<and> u \<le> 1 \<and> x \<in> F)"
+        if *: "(1 - ux) *\<^sub>R a + ux *\<^sub>R x
+               \<in> open_segment ((1 - ub) *\<^sub>R a + ub *\<^sub>R b) ((1 - uc) *\<^sub>R a + uc *\<^sub>R c)"
+          and "0 \<le> ub" "ub \<le> 1" "0 \<le> uc" "uc \<le> 1" "0 \<le> ux" "ux \<le> 1"
+          and b: "b \<in> convex hull S" and c: "c \<in> convex hull S" and "x \<in> F"
+        for b c ub uc ux x
+      proof -
+        obtain v where ne: "(1 - ub) *\<^sub>R a + ub *\<^sub>R b \<noteq> (1 - uc) *\<^sub>R a + uc *\<^sub>R c"
+          and eq: "(1 - ux) *\<^sub>R a + ux *\<^sub>R x =
+                    (1 - v) *\<^sub>R ((1 - ub) *\<^sub>R a + ub *\<^sub>R b) + v *\<^sub>R ((1 - uc) *\<^sub>R a + uc *\<^sub>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))) *\<^sub>R a +
+                      (ux *\<^sub>R x - (((1 - v) * ub) *\<^sub>R b + (v * uc) *\<^sub>R c)) = 0"
+          by (auto simp: algebra_simps)
+        then have "((1 - ux) - ((1 - v) * (1 - ub) + v * (1 - uc))) *\<^sub>R a =
+                   ((1 - v) * ub) *\<^sub>R b + (v * uc) *\<^sub>R c + (-ux) *\<^sub>R x"
+          by (auto simp: algebra_simps)
+        then have "a \<in> affine hull S" if "1 - ux - ((1 - v) * (1 - ub) + v * (1 - uc)) \<noteq> 0"
+          apply (rule face_of_convex_hull_aux)
+          using b c that apply (auto simp: algebra_simps)
+          using F convex_hull_subset_affine_hull face_of_imp_subset \<open>x \<in> F\<close> apply blast+
+          done
+        then have "1 - ux - ((1 - v) * (1 - ub) + v * (1 - uc)) = 0"
+          using a by blast
+        with 0 have equx: "(1 - v) * ub + v * uc = ux"
+          and uxx: "ux *\<^sub>R x = (((1 - v) * ub) *\<^sub>R b + (v * uc) *\<^sub>R c)"
+          by auto (auto simp: algebra_simps)
+        show ?thesis
+        proof (cases "uc = 0")
+          case True
+          then show ?thesis
+            using equx 0 \<open>0 \<le> ub\<close> \<open>ub \<le> 1\<close> \<open>v < 1\<close> \<open>x \<in> F\<close>
+            apply (auto simp: algebra_simps)
+             apply (rule_tac x=x in exI, simp)
+             apply (rule_tac x=ub in exI, auto)
+             apply (metis add.left_neutral diff_eq_eq less_irrefl mult.commute mult_cancel_right1 real_vector.scale_cancel_left real_vector.scale_left_diff_distrib)
+            using \<open>x \<in> F\<close> \<open>uc \<le> 1\<close> apply blast
+            done
+        next
+          case False
+          show ?thesis
+          proof (cases "ub = 0")
+            case True
+            then show ?thesis
+              using equx 0 \<open>0 \<le> uc\<close> \<open>uc \<le> 1\<close> \<open>0 < v\<close> \<open>x \<in> F\<close> \<open>uc \<noteq> 0\<close> by (force simp: algebra_simps)
+          next
+            case False
+            then have "0 < ub" "0 < uc"
+              using \<open>uc \<noteq> 0\<close> \<open>0 \<le> ub\<close> \<open>0 \<le> uc\<close> by auto
+            then have "ux \<noteq> 0"
+              by (metis \<open>0 < v\<close> \<open>v < 1\<close> diff_ge_0_iff_ge dual_order.strict_implies_order equx leD le_add_same_cancel2 zero_le_mult_iff zero_less_mult_iff)
+            have "b \<in> F \<and> c \<in> F"
+            proof (cases "b = c")
+              case True
+              then show ?thesis
+                by (metis \<open>ux \<noteq> 0\<close> equx real_vector.scale_cancel_left scaleR_add_left uxx \<open>x \<in> F\<close>)
+            next
+              case False
+              have "x = (((1 - v) * ub) *\<^sub>R b + (v * uc) *\<^sub>R c) /\<^sub>R ux"
+                by (metis \<open>ux \<noteq> 0\<close> uxx mult.commute right_inverse scaleR_one scaleR_scaleR)
+              also have "... = (1 - v * uc / ux) *\<^sub>R b + (v * uc / ux) *\<^sub>R c"
+                using \<open>ux \<noteq> 0\<close> equx apply (auto simp: algebra_simps divide_simps)
+                by (metis add.commute add_diff_eq add_divide_distrib diff_add_cancel scaleR_add_left)
+              finally have "x = (1 - v * uc / ux) *\<^sub>R b + (v * uc / ux) *\<^sub>R c" .
+              then have "x \<in> open_segment b c"
+                apply (simp add: in_segment \<open>b \<noteq> c\<close>)
+                apply (rule_tac x="(v * uc) / ux" in exI)
+                using \<open>0 \<le> ux\<close> \<open>ux \<noteq> 0\<close> \<open>0 < uc\<close> \<open>0 < v\<close> \<open>0 < ub\<close> \<open>v < 1\<close> equx
+                apply (force simp: algebra_simps divide_simps)
+                done
+              then show ?thesis
+                by (rule face_ofD [OF F _ b c \<open>x \<in> F\<close>])
+            qed
+            with \<open>0 \<le> ub\<close> \<open>ub \<le> 1\<close> \<open>0 \<le> uc\<close> \<open>uc \<le> 1\<close> 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 \<open>S \<noteq> {}\<close> \<open>F \<noteq> {}\<close>)
+    qed
+  qed
+qed
+
+lemma face_of_convex_hull_insert2:
+  fixes a :: "'a :: euclidean_space"
+  assumes S: "finite S" and a: "a \<notin> 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"
@@ -1429,6 +1602,23 @@
 lemma polytope_sing: "polytope {a}"
   using polytope_def by force
 
+lemma face_of_polytope_insert:
+     "\<lbrakk>polytope S; a \<notin> affine hull S; F face_of S\<rbrakk> \<Longrightarrow> F face_of convex hull (insert a S)"
+  by (metis (no_types, lifting) affine_hull_convex_hull face_of_convex_hull_insert hull_insert polytope_def)
+
+lemma face_of_polytope_insert2:
+  fixes a :: "'a :: euclidean_space"
+  assumes "polytope S" "a \<notin> 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 \<open>S = convex hull V\<close> hull_insert)
+qed
+
 
 subsection\<open>Polyhedra\<close>
 
@@ -2638,38 +2828,41 @@
   qed
 qed
 
-
 lemma cell_subdivision_lemma:
   assumes "finite \<F>"
       and "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
       and "\<And>X. X \<in> \<F> \<Longrightarrow> aff_dim X \<le> d"
       and "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> (X \<inter> Y) face_of X \<and> (X \<inter> Y) face_of Y"
       and "finite I"
-    shows "\<exists>\<F>'. \<Union>\<F>' = \<Union>\<F> \<and>
-                 finite \<F>' \<and>
-                 (\<forall>X \<in> \<F>'. polytope X) \<and>
-                 (\<forall>X \<in> \<F>'. aff_dim X \<le> d) \<and>
-                 (\<forall>X \<in> \<F>'. \<forall>Y \<in> \<F>'. X \<inter> Y face_of X \<and> X \<inter> Y face_of Y) \<and>
-                 (\<forall>X \<in> \<F>'. \<forall>x \<in> X. \<forall>y \<in> X. \<forall>a b.
+    shows "\<exists>\<G>. \<Union>\<G> = \<Union>\<F> \<and>
+                 finite \<G> \<and>
+                 (\<forall>C \<in> \<G>. \<exists>D. D \<in> \<F> \<and> C \<subseteq> D) \<and>
+                 (\<forall>C \<in> \<F>. \<forall>x \<in> C. \<exists>D. D \<in> \<G> \<and> x \<in> D \<and> D \<subseteq> C) \<and>
+                 (\<forall>X \<in> \<G>. polytope X) \<and>
+                 (\<forall>X \<in> \<G>. aff_dim X \<le> d) \<and>
+                 (\<forall>X \<in> \<G>. \<forall>Y \<in> \<G>. X \<inter> Y face_of X \<and> X \<inter> Y face_of Y) \<and>
+                 (\<forall>X \<in> \<G>. \<forall>x \<in> X. \<forall>y \<in> X. \<forall>a b.
                           (a,b) \<in> I \<longrightarrow> a \<bullet> x \<le> b \<and> a \<bullet> y \<le> b \<or>
                                         a \<bullet> x \<ge> b \<and> a \<bullet> y \<ge> b)"
   using \<open>finite I\<close>
 proof induction
   case empty
   then show ?case
-    by (rule_tac x="\<F>" in exI) (simp add: assms)
+    by (rule_tac x="\<F>" in exI) (auto simp: assms)
 next
   case (insert ab I)
-  then obtain \<F>' where eq: "\<Union>\<F>' = \<Union>\<F>" and "finite \<F>'"
-                   and poly: "\<And>X. X \<in> \<F>' \<Longrightarrow> polytope X"
-                   and aff: "\<And>X. X \<in> \<F>' \<Longrightarrow> aff_dim X \<le> d"
-                   and face: "\<And>X Y. \<lbrakk>X \<in> \<F>'; Y \<in> \<F>'\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
-                   and I: "\<And>X x y a b.  \<lbrakk>X \<in> \<F>'; x \<in> X; y \<in> X; (a,b) \<in> I\<rbrakk> \<Longrightarrow>
+  then obtain \<G> where eq: "\<Union>\<G> = \<Union>\<F>" and "finite \<G>"
+                   and sub1: "\<And>C. C \<in> \<G> \<Longrightarrow> \<exists>D. D \<in> \<F> \<and> C \<subseteq> D"
+                   and sub2: "\<And>C x. C \<in> \<F> \<and> x \<in> C \<Longrightarrow> \<exists>D. D \<in> \<G> \<and> x \<in> D \<and> D \<subseteq> C"
+                   and poly: "\<And>X. X \<in> \<G> \<Longrightarrow> polytope X"
+                   and aff: "\<And>X. X \<in> \<G> \<Longrightarrow> aff_dim X \<le> d"
+                   and face: "\<And>X Y. \<lbrakk>X \<in> \<G>; Y \<in> \<G>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
+                   and I: "\<And>X x y a b.  \<lbrakk>X \<in> \<G>; x \<in> X; y \<in> X; (a,b) \<in> I\<rbrakk> \<Longrightarrow>
                                     a \<bullet> x \<le> b \<and> a \<bullet> y \<le> b \<or> a \<bullet> x \<ge> b \<and> a \<bullet> y \<ge> b"
     by (auto simp: that)
   obtain a b where "ab = (a,b)"
     by fastforce
-  let ?\<G> = "(\<lambda>X. X \<inter> {x. a \<bullet> x \<le> b}) ` \<F>' \<union> (\<lambda>X. X \<inter> {x. a \<bullet> x \<ge> b}) ` \<F>'"
+  let ?\<G> = "(\<lambda>X. X \<inter> {x. a \<bullet> x \<le> b}) ` \<G> \<union> (\<lambda>X. X \<inter> {x. a \<bullet> x \<ge> b}) ` \<G>"
   have eqInt: "(S \<inter> Collect P) \<inter> (T \<inter> Collect Q) = (S \<inter> T) \<inter> (Collect P \<inter> Collect Q)" for S T::"'a set" and P Q
     by blast
   show ?case
@@ -2677,7 +2870,7 @@
     show "\<Union>?\<G> = \<Union>\<F>"
       by (force simp: eq [symmetric])
     show "finite ?\<G>"
-      using \<open>finite \<F>'\<close> by force
+      using \<open>finite \<G>\<close> by force
     show "\<forall>X \<in> ?\<G>. polytope X"
       by (force simp: poly polytope_Int_polyhedron polyhedron_halfspace_le polyhedron_halfspace_ge)
     show "\<forall>X \<in> ?\<G>. aff_dim X \<le> d"
@@ -2688,6 +2881,19 @@
       using \<open>ab = (a, b)\<close> I by fastforce
     show "\<forall>X \<in> ?\<G>. \<forall>Y \<in> ?\<G>. X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
       by (auto simp: eqInt halfspace_Int_eq face_of_Int_Int face face_of_halfspace_le face_of_halfspace_ge)
+    show "\<forall>C \<in> ?\<G>. \<exists>D. D \<in> \<F> \<and> C \<subseteq> D"
+      using sub1 by force
+    show "\<forall>C\<in>\<F>. \<forall>x\<in>C. \<exists>D. D \<in> ?\<G> \<and> x \<in> D \<and> D \<subseteq> C"
+    proof (intro ballI)
+      fix C z
+      assume "C \<in> \<F>" "z \<in> C"
+      with sub2 obtain D where D: "D \<in> \<G>" "z \<in> D" "D \<subseteq> C" by blast
+      have "D \<in> \<G> \<and> z \<in> D \<inter> {x. a \<bullet> x \<le> b} \<and> D \<inter> {x. a \<bullet> x \<le> b} \<subseteq> C \<or>
+            D \<in> \<G> \<and> z \<in> D \<inter> {x. a \<bullet> x \<ge> b} \<and> D \<inter> {x. a \<bullet> x \<ge> b} \<subseteq> C"
+        using linorder_class.linear [of "a \<bullet> z" b] D by blast
+      then show "\<exists>D. D \<in> ?\<G> \<and> z \<in> D \<and> D \<subseteq> C"
+        by blast
+    qed
   qed
 qed
 
@@ -2701,6 +2907,8 @@
   obtains "\<F>'" where "finite \<F>'" "\<Union>\<F>' = \<Union>\<F>" "\<And>X. X \<in> \<F>' \<Longrightarrow> diameter X < e"
                 "\<And>X. X \<in> \<F>' \<Longrightarrow> polytope X" "\<And>X. X \<in> \<F>' \<Longrightarrow> aff_dim X \<le> d"
                 "\<And>X Y. \<lbrakk>X \<in> \<F>'; Y \<in> \<F>'\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
+                "\<And>C. C \<in> \<F>' \<Longrightarrow> \<exists>D. D \<in> \<F> \<and> C \<subseteq> D"
+                "\<And>C x. C \<in> \<F> \<and> x \<in> C \<Longrightarrow> \<exists>D. D \<in> \<F>' \<and> x \<in> D \<and> D \<subseteq> C"
 proof -
   have "bounded(\<Union>\<F>)"
     by (simp add: \<open>finite \<F>\<close> poly bounded_Union polytope_imp_bounded)
@@ -2723,9 +2931,10 @@
               and face: "\<And>X Y. \<lbrakk>X \<in> \<F>'; Y \<in> \<F>'\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
               and I: "\<And>X x y a b.  \<lbrakk>X \<in> \<F>'; x \<in> X; y \<in> X; (a,b) \<in> I\<rbrakk> \<Longrightarrow>
                                      a \<bullet> x \<le> b \<and> a \<bullet> y \<le> b \<or> a \<bullet> x \<ge> b \<and> a \<bullet> y \<ge> b"
+              and sub1: "\<And>C. C \<in> \<F>' \<Longrightarrow> \<exists>D. D \<in> \<F> \<and> C \<subseteq> D"
+              and sub2: "\<And>C x. C \<in> \<F> \<and> x \<in> C \<Longrightarrow> \<exists>D. D \<in> \<F>' \<and> x \<in> D \<and> D \<subseteq> C"
     apply (rule exE [OF cell_subdivision_lemma])
-         apply (rule assms \<open>finite I\<close> | assumption)+
-    apply (auto intro: that)
+    using assms \<open>finite I\<close> apply auto
     done
   show ?thesis
   proof (rule_tac \<F>'="\<F>'" in that)
@@ -2788,14 +2997,13 @@
         by (simp add: \<open>0 < e\<close>)
       finally show ?thesis .
     qed
-  qed (auto simp: eq poly aff face \<open>finite \<F>'\<close>)
+  qed (auto simp: eq poly aff face sub1 sub2 \<open>finite \<F>'\<close>)
 qed
 
 
-subsection\<open>Simplicial complexes and triangulations\<close>
+subsection\<open>Simplexes\<close>
 
-subsubsection\<open>The notion of n-simplex for integer @{term"n \<ge> -1"}\<close>
-
+text\<open>The notion of n-simplex for integer @{term"n \<ge> -1"}\<close>
 definition simplex :: "int \<Rightarrow> 'a::euclidean_space set \<Rightarrow> bool" (infix "simplex" 50)
   where "n simplex S \<equiv> \<exists>C. ~(affine_dependent C) \<and> int(card C) = n + 1 \<and> S = convex hull C"
 
@@ -2917,4 +3125,690 @@
   qed (use C in auto)
 qed
 
+subsection\<open>Simplicial complexes and triangulations\<close>
+
+definition simplicial_complex where
+ "simplicial_complex \<C> \<equiv>
+        finite \<C> \<and>
+        (\<forall>S \<in> \<C>. \<exists>n. n simplex S) \<and>
+        (\<forall>F S. S \<in> \<C> \<and> F face_of S \<longrightarrow> F \<in> \<C>) \<and>
+        (!S S'. S \<in> \<C> \<and> S' \<in> \<C>
+                \<longrightarrow> (S \<inter> S') face_of S \<and> (S \<inter> S') face_of S')"
+
+definition triangulation where
+ "triangulation \<T> \<equiv>
+        finite \<T> \<and>
+        (\<forall>T \<in> \<T>. \<exists>n. n simplex T) \<and>
+        (\<forall>T T'. T \<in> \<T> \<and> T' \<in> \<T>
+                \<longrightarrow> (T \<inter> T') face_of T \<and> (T \<inter> T') face_of T')"
+
+
+subsection\<open>Refining a cell complex to a simplicial complex\<close>
+
+lemma convex_hull_insert_Int_eq:
+  fixes z :: "'a :: euclidean_space"
+  assumes z: "z \<in> rel_interior S"
+      and T: "T \<subseteq> rel_frontier S"
+      and U: "U \<subseteq> rel_frontier S"
+      and "convex S" "convex T" "convex U"
+  shows "convex hull (insert z T) \<inter> convex hull (insert z U) = convex hull (insert z (T \<inter> U))"
+    (is "?lhs = ?rhs")
+proof
+  show "?lhs \<subseteq> ?rhs"
+  proof (cases "T={} \<or> U={}")
+    case True then show ?thesis by auto
+  next
+    case False
+    then have "T \<noteq> {}" "U \<noteq> {}" by auto
+    have TU: "convex (T \<inter> U)"
+      by (simp add: \<open>convex T\<close> \<open>convex U\<close> convex_Int)
+    have "(\<Union>x\<in>T. closed_segment z x) \<inter> (\<Union>x\<in>U. closed_segment z x)
+          \<subseteq> (if T \<inter> U = {} then {z} else UNION (T \<inter> U) (closed_segment z))" (is "_ \<subseteq> ?IF")
+    proof clarify
+      fix x t u
+      assume xt: "x \<in> closed_segment z t"
+        and xu: "x \<in> closed_segment z u"
+        and "t \<in> T" "u \<in> U"
+      then have ne: "t \<noteq> z" "u \<noteq> z"
+        using T U z unfolding rel_frontier_def by blast+
+      show "x \<in> ?IF"
+      proof (cases "x = z")
+        case True then show ?thesis by auto
+      next
+        case False
+        have t: "t \<in> closure S"
+          using T \<open>t \<in> T\<close> rel_frontier_def by auto
+        have u: "u \<in> closure S"
+          using U \<open>u \<in> U\<close> rel_frontier_def by auto
+        show ?thesis
+        proof (cases "t = u")
+          case True
+          then show ?thesis
+            using \<open>t \<in> T\<close> \<open>u \<in> U\<close> xt by auto
+        next
+          case False
+          have tnot: "t \<notin> closed_segment u z"
+          proof -
+            have "t \<in> closure S - rel_interior S"
+              using T \<open>t \<in> T\<close> rel_frontier_def by blast
+            then have "t \<notin> open_segment z u"
+              by (meson DiffD2 rel_interior_closure_convex_segment [OF \<open>convex S\<close> z u] subsetD)
+            then show ?thesis
+              by (simp add: \<open>t \<noteq> u\<close> \<open>t \<noteq> z\<close> open_segment_commute open_segment_def)
+          qed
+          moreover have "u \<notin> closed_segment z t"
+            using rel_interior_closure_convex_segment [OF \<open>convex S\<close> z t] \<open>u \<in> U\<close> \<open>u \<noteq> z\<close>
+              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 \<noteq> z"
+            using that xt xu
+            apply (simp add: between_mem_segment [symmetric])
+            by (metis between_commute between_trans_2 between_antisym)
+          then have "~ collinear {t, z, u}" if "x \<noteq> 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] \<open>x \<noteq> z\<close> by blast
+          then show ?thesis by metis
+        qed
+      qed
+    qed
+    then show ?thesis
+      using False \<open>convex T\<close> \<open>convex U\<close> TU
+      by (simp add: convex_hull_insert_segments hull_same split: if_split_asm)
+  qed
+  show "?rhs \<subseteq> ?lhs"
+    by (metis inf_greatest hull_mono inf.cobounded1 inf.cobounded2 insert_mono)
+qed
+
+lemma simplicial_subdivision_aux:
+  assumes "finite \<M>"
+      and "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
+      and "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C \<le> of_nat n"
+      and "\<And>C F. \<lbrakk>C \<in> \<M>; F face_of C\<rbrakk> \<Longrightarrow> F \<in> \<M>"
+      and "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1 \<and> C1 \<inter> C2 face_of C2"
+    shows "\<exists>\<T>. simplicial_complex \<T> \<and>
+                (\<forall>K \<in> \<T>. aff_dim K \<le> of_nat n) \<and>
+                \<Union>\<T> = \<Union>\<M> \<and>
+                (\<forall>C \<in> \<M>. \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F) \<and>
+                (\<forall>K \<in> \<T>. \<exists>C. C \<in> \<M> \<and> K \<subseteq> C)"
+  using assms
+proof (induction n arbitrary: \<M> rule: less_induct)
+  case (less n)
+  then have poly\<M>: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
+      and aff\<M>:    "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C \<le> of_nat n"
+      and face\<M>:   "\<And>C F. \<lbrakk>C \<in> \<M>; F face_of C\<rbrakk> \<Longrightarrow> F \<in> \<M>"
+      and intface\<M>: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1 \<and> C1 \<inter> C2 face_of C2"
+    by metis+
+  show ?case
+  proof (cases "n \<le> 1")
+    case True
+    have "\<And>s. \<lbrakk>n \<le> 1; s \<in> \<M>\<rbrakk> \<Longrightarrow> \<exists>m. m simplex s"
+      using poly\<M> aff\<M> by (force intro: polytope_lowdim_imp_simplex)
+    then show ?thesis
+      unfolding simplicial_complex_def
+      apply (rule_tac x="\<M>" in exI)
+      using True by (auto simp: less.prems)
+  next
+    case False
+    define \<S> where "\<S> \<equiv> {C \<in> \<M>. aff_dim C < n}"
+    have "finite \<S>" "\<And>C. C \<in> \<S> \<Longrightarrow> polytope C" "\<And>C. C \<in> \<S> \<Longrightarrow> aff_dim C \<le> int (n - 1)"
+         "\<And>C F. \<lbrakk>C \<in> \<S>; F face_of C\<rbrakk> \<Longrightarrow> F \<in> \<S>"
+         "\<And>C1 C2. \<lbrakk>C1 \<in> \<S>; C2 \<in> \<S>\<rbrakk>  \<Longrightarrow> C1 \<inter> C2 face_of C1 \<and> C1 \<inter> C2 face_of C2"
+      using less.prems
+      apply (auto simp: \<S>_def)
+      by (metis aff_dim_subset face_of_imp_subset less_le not_le)
+    with less.IH [of "n-1" \<S>] False
+    obtain \<U> where "simplicial_complex \<U>"
+           and aff_dim\<U>: "\<And>K. K \<in> \<U> \<Longrightarrow> aff_dim K \<le> int (n - 1)"
+           and        "\<Union>\<U> = \<Union>\<S>"
+           and fin\<U>:  "\<And>C. C \<in> \<S> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<U> \<and> C = \<Union>F"
+           and C\<U>:    "\<And>K. K \<in> \<U> \<Longrightarrow> \<exists>C. C \<in> \<S> \<and> K \<subseteq> C"
+      by auto
+    then have "finite \<U>"
+         and simpl\<U>: "\<And>S. S \<in> \<U> \<Longrightarrow> \<exists>n. n simplex S"
+         and face\<U>:  "\<And>F S. \<lbrakk>S \<in> \<U>; F face_of S\<rbrakk> \<Longrightarrow> F \<in> \<U>"
+         and faceI\<U>: "\<And>S S'. \<lbrakk>S \<in> \<U>; S' \<in> \<U>\<rbrakk> \<Longrightarrow> (S \<inter> S') face_of S \<and> (S \<inter> S') face_of S'"
+      by (auto simp: simplicial_complex_def)
+    define \<N> where "\<N> \<equiv> {C \<in> \<M>. aff_dim C = n}"
+    have "finite \<N>"
+      by (simp add: \<N>_def less.prems(1))
+    have poly\<N>: "\<And>C. C \<in> \<N> \<Longrightarrow> polytope C"
+      and convex\<N>: "\<And>C. C \<in> \<N> \<Longrightarrow> convex C"
+      and closed\<N>: "\<And>C. C \<in> \<N> \<Longrightarrow> closed C"
+      by (auto simp: \<N>_def poly\<M> polytope_imp_convex polytope_imp_closed)
+    have in_rel_interior: "(@z. z \<in> rel_interior C) \<in> rel_interior C" if "C \<in> \<N>" for C
+        using that poly\<M> polytope_imp_convex rel_interior_aff_dim some_in_eq by (fastforce simp: \<N>_def)
+    have *: "\<exists>T. ~affine_dependent T \<and> card T \<le> n \<and> aff_dim K < n \<and> K = convex hull T"
+      if "K \<in> \<U>" for K
+    proof -
+      obtain r where r: "r simplex K"
+        using \<open>K \<in> \<U>\<close> simpl\<U> by blast
+      have "r = aff_dim K"
+        using \<open>r simplex K\<close> aff_dim_simplex by blast
+      with r
+      show ?thesis
+        unfolding simplex_def
+        using False \<open>\<And>K. K \<in> \<U> \<Longrightarrow> aff_dim K \<le> int (n - 1)\<close> that by fastforce
+    qed
+    have ahK_C_disjoint: "affine hull K \<inter> rel_interior C = {}"
+      if "C \<in> \<N>" "K \<in> \<U>" "K \<subseteq> rel_frontier C" for C K
+    proof -
+      have "convex C" "closed C"
+        by (auto simp: convex\<N> closed\<N> \<open>C \<in> \<N>\<close>)
+      obtain F where F: "F face_of C" and "F \<noteq> C" "K \<subseteq> F"
+      proof -
+        obtain L where "L \<in> \<S>" "K \<subseteq> L"
+          using \<open>K \<in> \<U>\<close> C\<U> by blast
+        have "K \<le> rel_frontier C"
+          by (simp add: \<open>K \<subseteq> rel_frontier C\<close>)
+        also have "... \<le> C"
+          by (simp add: \<open>closed C\<close> rel_frontier_def subset_iff)
+        finally have "K \<subseteq> C" .
+        have "L \<inter> C face_of C"
+          using \<N>_def \<S>_def \<open>C \<in> \<N>\<close> \<open>L \<in> \<S>\<close> intface\<M> by auto
+        moreover have "L \<inter> C \<noteq> C"
+          using \<open>C \<in> \<N>\<close> \<open>L \<in> \<S>\<close>
+          apply (clarsimp simp: \<N>_def \<S>_def)
+          by (metis aff_dim_subset inf_le1 not_le)
+        moreover have "K \<subseteq> L \<inter> C"
+          using \<open>C \<in> \<N>\<close> \<open>L \<in> \<S>\<close> \<open>K \<subseteq> C\<close> \<open>K \<subseteq> L\<close>
+          by (auto simp: \<N>_def \<S>_def)
+        ultimately show ?thesis using that by metis
+      qed
+      have "affine hull F \<inter> rel_interior C = {}"
+        by (rule affine_hull_face_of_disjoint_rel_interior [OF \<open>convex C\<close> F \<open>F \<noteq> C\<close>])
+      with hull_mono [OF \<open>K \<subseteq> F\<close>]
+      show "affine hull K \<inter> rel_interior C = {}"
+        by fastforce
+    qed
+    let ?\<T> = "(\<Union>C \<in> \<N>. \<Union>K \<in> \<U> \<inter> Pow (rel_frontier C).
+                     {convex hull (insert (@z. z \<in> rel_interior C) K)})"
+    have "\<exists>\<T>. simplicial_complex \<T> \<and>
+              (\<forall>K \<in> \<T>. aff_dim K \<le> of_nat n) \<and>
+              (\<forall>C \<in> \<M>. \<exists>F. F \<subseteq> \<T> \<and> C = \<Union>F) \<and>
+              (\<forall>K \<in> \<T>. \<exists>C. C \<in> \<M> \<and> K \<subseteq> C)"
+    proof (rule exI, intro conjI ballI)
+      show "simplicial_complex (\<U> \<union> ?\<T>)"
+        unfolding simplicial_complex_def
+      proof (intro conjI impI ballI allI)
+        show "finite (\<U> \<union> ?\<T>)"
+          using \<open>finite \<U>\<close> \<open>finite \<N>\<close> by simp
+        show "\<exists>n. n simplex S" if "S \<in> \<U> \<union> ?\<T>" for S
+          using that ahK_C_disjoint in_rel_interior simpl\<U> simplex_insert_dimplus1 by fastforce
+        show "F \<in> \<U> \<union> ?\<T>" if S: "S \<in> \<U> \<union> ?\<T> \<and> F face_of S" for F S
+        proof -
+          have "F \<in> \<U>" if "S \<in> \<U>"
+            using S face\<U> that by blast
+          moreover have "F \<in> \<U> \<union> ?\<T>"
+            if "F face_of S" "C \<in> \<N>" "K \<in> \<U>" and "K \<subseteq> rel_frontier C"
+              and S: "S = convex hull insert (@z. z \<in> rel_interior C) K" for C K
+          proof -
+            let ?z = "@z. z \<in> rel_interior C"
+            have "?z \<in> rel_interior C"
+              by (simp add: in_rel_interior \<open>C \<in> \<N>\<close>)
+            moreover
+            obtain I where "\<not> affine_dependent I" "card I \<le> n" "aff_dim K < int n" "K = convex hull I"
+              using * [OF \<open>K \<in> \<U>\<close>] by auto
+            ultimately have "?z \<notin> affine hull I"
+              using ahK_C_disjoint affine_hull_convex_hull that by blast
+            have "compact I" "finite I"
+              by (auto simp: \<open>\<not> affine_dependent I\<close> aff_independent_finite finite_imp_compact)
+            moreover have "F face_of convex hull insert ?z I"
+              by (metis S \<open>F face_of S\<close> \<open>K = convex hull I\<close> convex_hull_eq_empty convex_hull_insert_segments hull_hull)
+            ultimately obtain J where "J \<subseteq> 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 \<in> J")
+              case True
+              have "F \<in> (\<Union>K\<in>\<U> \<inter> Pow (rel_frontier C). {convex hull insert ?z K})"
+              proof
+                have "convex hull (J - {?z}) face_of K"
+                  by (metis True \<open>J \<subseteq> insert ?z I\<close> \<open>K = convex hull I\<close> \<open>\<not> affine_dependent I\<close> face_of_convex_hull_affine_independent subset_insert_iff)
+                then have "convex hull (J - {?z}) \<in> \<U>"
+                  by (rule face\<U> [OF \<open>K \<in> \<U>\<close>])
+                moreover
+                have "\<And>x. x \<in> convex hull (J - {?z}) \<Longrightarrow> x \<in> rel_frontier C"
+                  by (metis True \<open>J \<subseteq> insert ?z I\<close> \<open>K = convex hull I\<close> subsetD hull_mono subset_insert_iff that(4))
+                ultimately show "convex hull (J - {?z}) \<in> \<U> \<inter> Pow (rel_frontier C)" by auto
+                let ?F = "convex hull insert ?z (convex hull (J - {?z}))"
+                have "F \<subseteq> ?F"
+                  apply (clarsimp simp: \<open>F = convex hull J\<close>)
+                  by (metis True subsetD hull_mono hull_subset subset_insert_iff)
+                moreover have "?F \<subseteq> F"
+                  apply (clarsimp simp: \<open>F = convex hull J\<close>)
+                  by (metis (no_types, lifting) True convex_hull_eq_empty convex_hull_insert_segments hull_hull insert_Diff)
+                ultimately
+                show "F \<in> {?F}" by auto
+              qed
+              with \<open>C\<in>\<N>\<close> show ?thesis by auto
+            next
+              case False
+              then have "F \<in> \<U>"
+                using face_of_convex_hull_affine_independent [OF \<open>\<not> affine_dependent I\<close>]
+                by (metis Int_absorb2 Int_insert_right_if0 \<open>F = convex hull J\<close> \<open>J \<subseteq> insert ?z I\<close> \<open>K = convex hull I\<close> face\<U> inf_le2 \<open>K \<in> \<U>\<close>)
+              then show "F \<in> \<U> \<union> ?\<T>"
+                by blast
+            qed
+          qed
+          ultimately show ?thesis
+            using that by auto
+        qed
+        have "(S \<inter> S' face_of S) \<and> (S \<inter> S' face_of S')"
+          if "S \<in> \<U> \<union> ?\<T>" "S' \<in> \<U> \<union> ?\<T>" for S S'
+        proof -
+          have symmy: "\<lbrakk>\<And>X Y. R X Y \<Longrightarrow> R Y X;
+                        \<And>X Y. \<lbrakk>X \<in> \<U>; Y \<in> \<U>\<rbrakk> \<Longrightarrow> R X Y;
+                        \<And>X Y. \<lbrakk>X \<in> \<U>; Y \<in> ?\<T>\<rbrakk> \<Longrightarrow> R X Y;
+                        \<And>X Y. \<lbrakk>X \<in> ?\<T>; Y \<in> ?\<T>\<rbrakk> \<Longrightarrow> R X Y\<rbrakk> \<Longrightarrow> R S S'" for R
+            using that by (metis (no_types, lifting) Un_iff)
+          show ?thesis
+          proof (rule symmy)
+            show "Y \<inter> X face_of Y \<and> Y \<inter> X face_of X"
+              if "X \<inter> Y face_of X \<and> X \<inter> Y face_of Y" for X Y :: "'a set"
+              by (simp add: inf_commute that)
+          next
+            show "X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
+              if "X \<in> \<U>" and "Y \<in> \<U>" for X Y
+              by (simp add: faceI\<U> that)
+          next
+            show "X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
+              if XY: "X \<in> \<U>" "Y \<in> ?\<T>" for X Y
+            proof -
+              obtain C K
+                where "C \<in> \<N>" "K \<in> \<U>" "K \<subseteq> rel_frontier C"
+                and Y: "Y = convex hull insert (@z. z \<in> rel_interior C) K"
+                using XY by blast
+              have "convex C"
+                by (simp add: \<open>C \<in> \<N>\<close> convex\<N>)
+              have "K \<subseteq> C"
+                by (metis DiffE \<open>C \<in> \<N>\<close> \<open>K \<subseteq> rel_frontier C\<close> closed\<N> closure_closed rel_frontier_def subset_iff)
+              let ?z = "(@z. z \<in> rel_interior C)"
+              have z: "?z \<in> rel_interior C"
+                using \<open>C \<in> \<N>\<close> in_rel_interior by blast
+              obtain D where "D \<in> \<S>" "X \<subseteq> D"
+                using C\<U> \<open>X \<in> \<U>\<close> by blast
+              have "D \<inter> rel_interior C = (C \<inter> D) \<inter> rel_interior C"
+                using rel_interior_subset by blast
+              also have "(C \<inter> D) \<inter> rel_interior C = {}"
+              proof (rule face_of_disjoint_rel_interior)
+                show "C \<inter> D face_of C"
+                  using \<N>_def \<S>_def \<open>C \<in> \<N>\<close> \<open>D \<in> \<S>\<close> intface\<M> by blast
+                show "C \<inter> D \<noteq> C"
+                  by (metis (mono_tags, lifting) Int_lower2 \<N>_def \<S>_def \<open>C \<in> \<N>\<close> \<open>D \<in> \<S>\<close> aff_dim_subset mem_Collect_eq not_le)
+              qed
+              finally have DC: "D \<inter> rel_interior C = {}" .
+              have eq: "X \<inter> convex hull (insert ?z K) = X \<inter> convex hull K"
+                apply (rule Int_convex_hull_insert_rel_exterior [OF \<open>convex C\<close> \<open>K \<subseteq> C\<close> z])
+                using DC by (meson \<open>X \<subseteq> D\<close> disjnt_def disjnt_subset1)
+              obtain I where I: "\<not> affine_dependent I"
+                         and Keq: "K = convex hull I" and [simp]: "convex hull K = K"
+                using "*" \<open>K \<in> \<U>\<close> by force
+              then have "?z \<notin> affine hull I"
+                using ahK_C_disjoint \<open>C \<in> \<N>\<close> \<open>K \<in> \<U>\<close> \<open>K \<subseteq> rel_frontier C\<close> affine_hull_convex_hull z by blast
+              have "X \<inter> K face_of K"
+                by (simp add: \<open>K \<in> \<U>\<close> faceI\<U> \<open>X \<in> \<U>\<close>)
+              also have "... face_of convex hull insert ?z K"
+                by (metis I Keq \<open>?z \<notin> affine hull I\<close> aff_independent_finite convex_convex_hull face_of_convex_hull_insert face_of_refl hull_insert)
+              finally have "X \<inter> K face_of convex hull insert ?z K" .
+              then show ?thesis
+                using "*" \<open>K \<in> \<U>\<close> faceI\<U> that(1) by (fastforce simp add: Y eq)
+            qed
+          next
+            show "X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
+              if XY: "X \<in> ?\<T>" "Y \<in> ?\<T>" for X Y
+            proof -
+              obtain C K D L
+                where "C \<in> \<N>" "K \<in> \<U>" "K \<subseteq> rel_frontier C"
+                and X: "X = convex hull insert (@z. z \<in> rel_interior C) K"
+                and "D \<in> \<N>" "L \<in> \<U>" "L \<subseteq> rel_frontier D"
+                and Y: "Y = convex hull insert (@z. z \<in> rel_interior D) L"
+                using XY by blast
+              let ?z = "(@z. z \<in> rel_interior C)"
+              have z: "?z \<in> rel_interior C"
+                using \<open>C \<in> \<N>\<close> in_rel_interior by blast
+              have "convex C"
+                by (simp add: \<open>C \<in> \<N>\<close> convex\<N>)
+              have "convex K"
+                using "*" \<open>K \<in> \<U>\<close> by blast
+              have "convex L"
+                by (meson \<open>L \<in> \<U>\<close> convex_simplex simpl\<U>)
+              show ?thesis
+              proof (cases "D=C")
+                case True
+                then have "L \<subseteq> rel_frontier C"
+                  using \<open>L \<subseteq> rel_frontier D\<close> by auto
+                show ?thesis
+                  apply (simp add: X Y True)
+                  apply (simp add: convex_hull_insert_Int_eq [OF z] \<open>K \<subseteq> rel_frontier C\<close> \<open>L \<subseteq> rel_frontier C\<close> \<open>convex C\<close> \<open>convex K\<close> \<open>convex L\<close>)
+                  using face_of_polytope_insert2
+                  by (metis "*" IntI \<open>C \<in> \<N>\<close> \<open>K \<in> \<U>\<close> \<open>L \<in> \<U>\<close>\<open>K \<subseteq> rel_frontier C\<close> \<open>L \<subseteq> rel_frontier C\<close> aff_independent_finite ahK_C_disjoint empty_iff faceI\<U> polytope_convex_hull z)
+              next
+                case False
+                have "convex D"
+                  by (simp add: \<open>D \<in> \<N>\<close> convex\<N>)
+                have "K \<subseteq> C"
+                  by (metis DiffE \<open>C \<in> \<N>\<close> \<open>K \<subseteq> rel_frontier C\<close> closed\<N> closure_closed rel_frontier_def subset_eq)
+                have "L \<subseteq> D"
+                  by (metis DiffE \<open>D \<in> \<N>\<close> \<open>L \<subseteq> rel_frontier D\<close> closed\<N> closure_closed rel_frontier_def subset_eq)
+                let ?w = "(@w. w \<in> rel_interior D)"
+                have w: "?w \<in> rel_interior D"
+                  using \<open>D \<in> \<N>\<close> in_rel_interior by blast
+                have "C \<inter> rel_interior D = (D \<inter> C) \<inter> rel_interior D"
+                  using rel_interior_subset by blast
+                also have "(D \<inter> C) \<inter> rel_interior D = {}"
+                proof (rule face_of_disjoint_rel_interior)
+                  show "D \<inter> C face_of D"
+                    using \<N>_def \<open>C \<in> \<N>\<close> \<open>D \<in> \<N>\<close> intface\<M> by blast
+                  have "D \<in> \<M> \<and> aff_dim D = int n"
+                    using \<N>_def \<open>D \<in> \<N>\<close> by blast
+                  moreover have "C \<in> \<M> \<and> aff_dim C = int n"
+                    using \<N>_def \<open>C \<in> \<N>\<close> by blast
+                  ultimately show "D \<inter> C \<noteq> D"
+                    by (metis False face_of_aff_dim_lt inf.idem inf_le1 intface\<M> not_le poly\<M> polytope_imp_convex)
+                qed
+                finally have CD: "C \<inter> (rel_interior D) = {}" .
+                have zKC: "(convex hull insert ?z K) \<subseteq> C"
+                  by (metis DiffE \<open>C \<in> \<N>\<close> \<open>K \<subseteq> rel_frontier C\<close> closed\<N> closure_closed convex\<N> hull_minimal insert_subset rel_frontier_def rel_interior_subset subset_iff z)
+                have eq: "convex hull (insert ?z K) \<inter> convex hull (insert ?w L) =
+                          convex hull (insert ?z K) \<inter> convex hull L"
+                  apply (rule Int_convex_hull_insert_rel_exterior [OF \<open>convex D\<close> \<open>L \<subseteq> D\<close> w])
+                  using zKC CD apply (force simp: disjnt_def)
+                  done
+                have ch_id: "convex hull K = K" "convex hull L = L"
+                  using "*" \<open>K \<in> \<U>\<close> \<open>L \<in> \<U>\<close> hull_same by auto
+                have "convex C"
+                  by (simp add: \<open>C \<in> \<N>\<close> convex\<N>)
+                have "convex hull (insert ?z K) \<inter> L = L \<inter> convex hull (insert ?z K)"
+                  by blast
+                also have "... = convex hull K \<inter> L"
+                proof (subst Int_convex_hull_insert_rel_exterior [OF \<open>convex C\<close> \<open>K \<subseteq> C\<close> z])
+                  have "(C \<inter> D) \<inter> rel_interior C = {}"
+                  proof (rule face_of_disjoint_rel_interior)
+                    show "C \<inter> D face_of C"
+                      using \<N>_def \<open>C \<in> \<N>\<close> \<open>D \<in> \<N>\<close> intface\<M> by blast
+                    have "D \<in> \<M>" "aff_dim D = int n"
+                      using \<N>_def \<open>D \<in> \<N>\<close> by fastforce+
+                    moreover have "C \<in> \<M>" "aff_dim C = int n"
+                      using \<N>_def \<open>C \<in> \<N>\<close> by fastforce+
+                    ultimately have "aff_dim D + - 1 * aff_dim C \<le> 0"
+                      by fastforce
+                    then have "\<not> C face_of D"
+                      using False \<open>convex D\<close> face_of_aff_dim_lt by fastforce
+                    show "C \<inter> D \<noteq> C"
+                      using \<open>C \<in> \<M>\<close> \<open>D \<in> \<M>\<close> \<open>\<not> C face_of D\<close> intface\<M> by fastforce
+                  qed
+                  then have "D \<inter> 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 \<open>L \<subseteq> D\<close> disjnt_def disjnt_subset1)
+                next
+                  show "L \<inter> convex hull K = convex hull K \<inter> L"
+                    by force
+                qed
+                finally have chKL: "convex hull (insert ?z K) \<inter> L = convex hull K \<inter> L" .
+                have "convex hull insert ?z K \<inter> convex hull L face_of K"
+                  by (simp add: \<open>K \<in> \<U>\<close> \<open>L \<in> \<U>\<close> ch_id chKL faceI\<U>)
+                also have "... face_of convex hull insert ?z K"
+                proof -
+                  obtain I where I: "\<not> affine_dependent I" "K = convex hull I"
+                    using * [OF \<open>K \<in> \<U>\<close>] by auto
+                  then have "\<And>a. a \<notin> rel_interior C \<or> a \<notin> affine hull I"
+                    using ahK_C_disjoint \<open>C \<in> \<N>\<close> \<open>K \<in> \<U>\<close> \<open>K \<subseteq> rel_frontier C\<close> affine_hull_convex_hull by blast
+                  then show ?thesis
+                    by (metis I affine_independent_insert face_of_convex_hull_affine_independent hull_insert subset_insertI z)
+                qed
+                finally have 1: "convex hull insert ?z K \<inter> convex hull L face_of convex hull insert ?z K" .
+                have "convex hull insert ?z K \<inter> convex hull L face_of L"
+                  by (simp add: \<open>K \<in> \<U>\<close> \<open>L \<in> \<U>\<close> ch_id chKL faceI\<U>)
+                also have "... face_of convex hull insert ?w L"
+                proof -
+                  obtain I where I: "\<not> affine_dependent I" "L = convex hull I"
+                    using * [OF \<open>L \<in> \<U>\<close>] by auto
+                  then have "\<And>a. a \<notin> rel_interior D \<or> a \<notin> affine hull I"
+                    using \<open>D \<in> \<N>\<close> \<open>L \<in> \<U>\<close> \<open>L \<subseteq> rel_frontier D\<close> affine_hull_convex_hull ahK_C_disjoint by blast
+                  then show ?thesis
+                    by (metis I aff_independent_finite convex_convex_hull face_of_convex_hull_insert face_of_refl hull_insert w)
+                qed
+                finally have 2: "convex hull insert ?z K \<inter> convex hull L face_of convex hull insert ?w L" .
+                show ?thesis
+                  by (simp add: X Y eq 1 2)
+              qed
+            qed
+          qed
+        qed
+        then
+        show "S \<inter> S' face_of S" "S \<inter> S' face_of S'" if "S \<in> \<U> \<union> ?\<T> \<and> S' \<in> \<U> \<union> ?\<T>" for S S'
+          using that by auto
+      qed
+      show "\<exists>F \<subseteq> \<U> \<union> ?\<T>. C = \<Union>F" if "C \<in> \<M>" for C
+      proof (cases "C \<in> \<S>")
+        case True
+        then show ?thesis
+          by (meson UnCI fin\<U> subsetD subsetI)
+      next
+        case False
+        then have "C \<in> \<N>"
+          by (simp add: \<N>_def \<S>_def aff\<M> less_le that)
+        let ?z = "@z. z \<in> rel_interior C"
+        have z: "?z \<in> rel_interior C"
+          using \<open>C \<in> \<N>\<close> in_rel_interior by blast
+        let ?F = "\<Union>K \<in> \<U> \<inter> Pow (rel_frontier C). {convex hull (insert ?z K)}"
+        have "?F \<subseteq> ?\<T>"
+          using \<open>C \<in> \<N>\<close> by blast
+        moreover have "C \<subseteq> \<Union>?F"
+        proof
+          fix x
+          assume "x \<in> C"
+          have "convex C"
+            using \<open>C \<in> \<N>\<close> convex\<N> by blast
+          have "bounded C"
+            using \<open>C \<in> \<N>\<close> by (simp add: poly\<M> polytope_imp_bounded that)
+          have "polytope C"
+            using \<open>C \<in> \<N>\<close> poly\<N> by auto
+          have "\<not> (?z = x \<and> C = {?z})"
+            using \<open>C \<in> \<N>\<close> aff_dim_sing [of ?z] \<open>\<not> n \<le> 1\<close> by (force simp: \<N>_def)
+          then obtain y where y: "y \<in> rel_frontier C" and xzy: "x \<in> closed_segment ?z y"
+            and sub: "open_segment ?z y \<subseteq> rel_interior C"
+            by (blast intro: segment_to_rel_frontier [OF \<open>convex C\<close> \<open>bounded C\<close> z \<open>x \<in> C\<close>])
+          then obtain F where "y \<in> F" "F face_of C" "F \<noteq> C"
+            by (auto simp: rel_frontier_of_polyhedron_alt [OF polytope_imp_polyhedron [OF \<open>polytope C\<close>]])
+          then obtain \<G> where "finite \<G>" "\<G> \<subseteq> \<U>" "F = \<Union>\<G>"
+            by (metis (mono_tags, lifting) \<S>_def \<open>C \<in> \<M>\<close> \<open>convex C\<close> aff\<M> face\<M> face_of_aff_dim_lt fin\<U> le_less_trans mem_Collect_eq not_less)
+          then obtain K where "y \<in> K" "K \<in> \<G>"
+            using \<open>y \<in> F\<close> by blast
+          moreover have x: "x \<in> convex hull {?z,y}"
+            using segment_convex_hull xzy by auto
+          moreover have "convex hull {?z,y} \<subseteq> convex hull insert ?z K"
+            by (metis (full_types) \<open>y \<in> K\<close> hull_mono empty_subsetI insertCI insert_subset)
+          moreover have "K \<in> \<U>"
+            using \<open>K \<in> \<G>\<close> \<open>\<G> \<subseteq> \<U>\<close> by blast
+          moreover have "K \<subseteq> rel_frontier C"
+            using \<open>F = \<Union>\<G>\<close> \<open>F \<noteq> C\<close> \<open>F face_of C\<close> \<open>K \<in> \<G>\<close> face_of_subset_rel_frontier by fastforce
+          ultimately show "x \<in> \<Union>?F"
+            by force
+        qed
+        moreover
+        have "convex hull insert (SOME z. z \<in> rel_interior C) K \<subseteq> C"
+          if "K \<in> \<U>" "K \<subseteq> rel_frontier C" for K
+        proof (rule hull_minimal)
+          show "insert (SOME z. z \<in> rel_interior C) K \<subseteq> C"
+            using that \<open>C \<in> \<N>\<close> in_rel_interior rel_interior_subset
+            by (force simp: closure_eq rel_frontier_def closed\<N>)
+          show "convex C"
+            by (simp add: \<open>C \<in> \<N>\<close> convex\<N>)
+        qed
+        then have "\<Union>?F \<subseteq> C"
+          by auto
+        ultimately show ?thesis
+          by blast
+      qed
+
+      have "(\<exists>C. C \<in> \<M> \<and> L \<subseteq> C) \<and> aff_dim L \<le> int n"  if "L \<in> \<U> \<union> ?\<T>" for L
+        using that
+      proof
+        assume "L \<in> \<U>"
+        then show ?thesis
+          using C\<U> \<S>_def "*" by fastforce
+      next
+        assume "L \<in> ?\<T>"
+        then obtain C K where "C \<in> \<N>"
+          and L: "L = convex hull insert (@z. z \<in> rel_interior C) K"
+          and K: "K \<in> \<U>" "K \<subseteq> rel_frontier C"
+          by auto
+        then have "convex hull C = C"
+          by (meson convex\<N> convex_hull_eq)
+        then have "convex C"
+          by (metis (no_types) convex_convex_hull)
+        have "rel_frontier C \<subseteq> C"
+          by (metis DiffE closed\<N> \<open>C \<in> \<N>\<close> closure_closed rel_frontier_def subsetI)
+        have "K \<subseteq> C"
+          using K \<open>rel_frontier C \<subseteq> C\<close> by blast
+        have "C \<in> \<M>"
+          using \<N>_def \<open>C \<in> \<N>\<close> by auto
+        moreover have "L \<subseteq> C"
+          using K L \<open>C \<in> \<N>\<close>
+          by (metis \<open>K \<subseteq> C\<close> \<open>convex hull C = C\<close> contra_subsetD hull_mono in_rel_interior insert_subset rel_interior_subset)
+        ultimately show ?thesis
+          using \<open>rel_frontier C \<subseteq> C\<close> \<open>L \<subseteq> C\<close> aff\<M> aff_dim_subset \<open>C \<in> \<M>\<close> dual_order.trans by blast
+      qed
+      then show "\<exists>C. C \<in> \<M> \<and> L \<subseteq> C" "aff_dim L \<le> int n" if "L \<in> \<U> \<union> ?\<T>" 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 \<M>"
+      and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
+      and face: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1 \<and> C1 \<inter> C2 face_of C2"
+      and aff: "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C \<le> d"
+  obtains \<T> where "simplicial_complex \<T>" "\<And>K. K \<in> \<T> \<Longrightarrow> aff_dim K \<le> d"
+                  "\<Union>\<T> = \<Union>\<M>"
+                  "\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F"
+                  "\<And>K. K \<in> \<T> \<Longrightarrow> \<exists>C. C \<in> \<M> \<and> K \<subseteq> C"
+proof (cases "d \<ge> 0")
+  case True
+  then obtain n where n: "d = of_nat n"
+    using zero_le_imp_eq_int by blast
+  have "\<exists>\<T>. simplicial_complex \<T> \<and>
+            (\<forall>K\<in>\<T>. aff_dim K \<le> int n) \<and>
+            \<Union>\<T> = \<Union>(\<Union>C\<in>\<M>. {F. F face_of C}) \<and>
+            (\<forall>C\<in>\<Union>C\<in>\<M>. {F. F face_of C}.
+                \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F) \<and>
+            (\<forall>K\<in>\<T>. \<exists>C. C \<in> (\<Union>C\<in>\<M>. {F. F face_of C}) \<and> K \<subseteq> C)"
+  proof (rule simplicial_subdivision_aux)
+    show "finite (\<Union>C\<in>\<M>. {F. F face_of C})"
+      using \<open>finite \<M>\<close> poly polyhedron_eq_finite_faces polytope_imp_polyhedron by fastforce
+    show "polytope F" if "F \<in> (\<Union>C\<in>\<M>. {F. F face_of C})" for F
+      using poly that face_of_polytope_polytope by blast
+    show "aff_dim F \<le> int n" if "F \<in> (\<Union>C\<in>\<M>. {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 \<in> (\<Union>C\<in>\<M>. {F. F face_of C})"
+      if "G \<in> (\<Union>C\<in>\<M>. {F. F face_of C})" and "F face_of G" for F G
+      using that face_of_trans by blast
+  next
+    show "F1 \<inter> F2 face_of F1 \<and> F1 \<inter> F2 face_of F2"
+      if "F1 \<in> (\<Union>C\<in>\<M>. {F. F face_of C})" and "F2 \<in> (\<Union>C\<in>\<M>. {F. F face_of C})" for F1 F2
+      using that
+      by safe (meson face face_of_Int_subface)+
+  qed
+  moreover
+  have "\<Union>(\<Union>C\<in>\<M>. {F. F face_of C}) = \<Union>\<M>"
+    using face_of_imp_subset face by blast
+  ultimately show ?thesis
+    apply clarify
+    apply (rule that, assumption+)
+       using n apply blast
+      apply (simp_all add: poly face_of_refl polytope_imp_convex)
+    using face_of_imp_subset by fastforce
+next
+  case False
+  then have m1: "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C = -1"
+    by (metis aff aff_dim_empty_eq aff_dim_negative_iff dual_order.trans not_less)
+  then have face\<M>: "\<And>F S. \<lbrakk>S \<in> \<M>; F face_of S\<rbrakk> \<Longrightarrow> F \<in> \<M>"
+    by (metis aff_dim_empty face_of_empty)
+  show ?thesis
+  proof
+    have "\<And>S. S \<in> \<M> \<Longrightarrow> \<exists>n. n simplex S"
+      by (metis (no_types) m1 aff_dim_empty simplex_minus_1)
+    then show "simplicial_complex \<M>"
+      by (auto simp: simplicial_complex_def \<open>finite \<M>\<close> face intro: face\<M>)
+    show "aff_dim K \<le> d" if "K \<in> \<M>" for K
+      by (simp add: that aff)
+    show "\<exists>F. finite F \<and> F \<subseteq> \<M> \<and> C = \<Union>F" if "C \<in> \<M>" for C
+      using \<open>C \<in> \<M>\<close> equals0I by auto
+    show "\<exists>C. C \<in> \<M> \<and> K \<subseteq> C" if "K \<in> \<M>" for K
+      using \<open>K \<in> \<M>\<close> by blast
+  qed auto
+qed
+
+proposition simplicial_subdivision_of_cell_complex:
+  assumes "finite \<M>"
+      and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
+      and face: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1 \<and> C1 \<inter> C2 face_of C2"
+  obtains \<T> where "simplicial_complex \<T>"
+                  "\<Union>\<T> = \<Union>\<M>"
+                  "\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F"
+                  "\<And>K. K \<in> \<T> \<Longrightarrow> \<exists>C. C \<in> \<M> \<and> K \<subseteq> 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 \<M>"
+      and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
+      and face: "\<And>C1 C2. \<lbrakk>C1 \<in> \<M>; C2 \<in> \<M>\<rbrakk> \<Longrightarrow> C1 \<inter> C2 face_of C1 \<and> C1 \<inter> C2 face_of C2"
+  obtains \<T> where "simplicial_complex \<T>"
+                  "\<And>K. K \<in> \<T> \<Longrightarrow> diameter K < e"
+                  "\<Union>\<T> = \<Union>\<M>"
+                  "\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F"
+                  "\<And>K. K \<in> \<T> \<Longrightarrow> \<exists>C. C \<in> \<M> \<and> K \<subseteq> C"
+proof -
+  obtain \<N> where \<N>: "finite \<N>" "\<Union>\<N> = \<Union>\<M>" 
+              and diapoly: "\<And>X. X \<in> \<N> \<Longrightarrow> diameter X < e" "\<And>X. X \<in> \<N> \<Longrightarrow> polytope X"
+               and      "\<And>X Y. \<lbrakk>X \<in> \<N>; Y \<in> \<N>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
+               and \<N>covers: "\<And>C x. C \<in> \<M> \<and> x \<in> C \<Longrightarrow> \<exists>D. D \<in> \<N> \<and> x \<in> D \<and> D \<subseteq> C"
+               and \<N>covered: "\<And>C. C \<in> \<N> \<Longrightarrow> \<exists>D. D \<in> \<M> \<and> C \<subseteq> D"
+    by (blast intro: cell_complex_subdivision_exists [OF \<open>0 < e\<close> \<open>finite \<M>\<close> poly aff_dim_le_DIM face])
+  then obtain \<T> where \<T>: "simplicial_complex \<T>" "\<Union>\<T> = \<Union>\<N>"
+                   and \<T>covers: "\<And>C. C \<in> \<N> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F"
+                   and \<T>covered: "\<And>K. K \<in> \<T> \<Longrightarrow> \<exists>C. C \<in> \<N> \<and> K \<subseteq> C"
+    using simplicial_subdivision_of_cell_complex [OF \<open>finite \<N>\<close>] by metis
+  show ?thesis
+  proof
+    show "simplicial_complex \<T>"
+      by (rule \<T>)
+    show "diameter K < e" if "K \<in> \<T>" for K
+      by (metis le_less_trans diapoly \<T>covered diameter_subset polytope_imp_bounded that)
+    show "\<Union>\<T> = \<Union>\<M>"
+      by (simp add: \<N>(2) \<open>\<Union>\<T> = \<Union>\<N>\<close>)
+    show "\<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F" if "C \<in> \<M>" for C
+    proof -
+      { fix x
+        assume "x \<in> C"
+        then obtain D where "D \<in> \<T>" "x \<in> D" "D \<subseteq> C"
+          using \<N>covers \<open>C \<in> \<M>\<close> \<T>covers by force
+        then have "\<exists>X\<in>\<T> \<inter> Pow C. x \<in> X"
+          using \<open>D \<in> \<T>\<close> \<open>D \<subseteq> C\<close> \<open>x \<in> D\<close> by blast
+      }
+      moreover
+      have "finite (\<T> \<inter> Pow C)"
+        using \<open>simplicial_complex \<T>\<close> simplicial_complex_def by auto
+      ultimately show ?thesis
+        by (rule_tac x="(\<T> \<inter> Pow C)" in exI) auto
+    qed
+    show "\<exists>C. C \<in> \<M> \<and> K \<subseteq> C" if "K \<in> \<T>" for K
+      by (meson \<N>covered \<T>covered order_trans that)
+  qed
+qed
+
 end
diff -r 33a47f2d9edc -r d425bdf419f5 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Wed Jul 26 16:07:45 2017 +0100
+++ b/src/HOL/Analysis/Starlike.thy	Thu Jul 27 15:22:35 2017 +0100
@@ -5837,11 +5837,41 @@
   show ?thesis using S
     apply (simp add: hull_redundant cong: aff_dim_affine_hull2)
     apply (simp add: affine_hull_insert_span_gen hull_inc)
-    apply (simp add: insert_commute [of a] hull_inc aff_dim_eq_dim [of x] dim_insert span_0)
+    apply (simp add: insert_commute [of a] hull_inc aff_dim_eq_dim [of x] dim_insert)
     apply (metis (no_types, lifting) add_minus_cancel image_iff uminus_add_conv_diff)
     done
 qed
 
+lemma affine_dependent_choose:
+  fixes a :: "'a :: euclidean_space"
+  assumes "~(affine_dependent S)"
+  shows "affine_dependent(insert a S) \<longleftrightarrow> a \<notin> S \<and> a \<in> affine hull S"
+        (is "?lhs = ?rhs")
+proof safe
+  assume "affine_dependent (insert a S)" and "a \<in> S"
+  then show "False"
+    using \<open>a \<in> S\<close> assms insert_absorb by fastforce
+next
+  assume lhs: "affine_dependent (insert a S)"
+  then have "a \<notin> S"
+    by (metis (no_types) assms insert_absorb)
+  moreover have "finite S"
+    using affine_independent_iff_card assms by blast
+  moreover have "aff_dim (insert a S) \<noteq> int (card S)"
+    using \<open>finite S\<close> affine_independent_iff_card \<open>a \<notin> S\<close> lhs by fastforce
+  ultimately show "a \<in> affine hull S"
+    by (metis aff_dim_affine_independent aff_dim_insert assms)
+next
+  assume "a \<notin> S" and "a \<in> affine hull S"
+  show "affine_dependent (insert a S)"
+    by (simp add: \<open>a \<in> affine hull S\<close> \<open>a \<notin> S\<close> affine_dependent_def)
+qed
+
+lemma affine_independent_insert:
+  fixes a :: "'a :: euclidean_space"
+  shows "\<lbrakk>~(affine_dependent S); a \<notin> affine hull S\<rbrakk> \<Longrightarrow> ~(affine_dependent(insert a S))"
+  by (simp add: affine_dependent_choose)
+
 lemma subspace_bounded_eq_trivial:
   fixes S :: "'a::real_normed_vector set"
   assumes "subspace S"