polytopes: simplical subdivisions, etc.
authorpaulson <lp15@cam.ac.uk>
Thu Jul 27 15:22:35 2017 +0100 (24 months ago)
changeset 66297d425bdf419f5
parent 66296 33a47f2d9edc
child 66298 5ff9fe3fee66
polytopes: simplical subdivisions, etc.
src/HOL/Analysis/Linear_Algebra.thy
src/HOL/Analysis/Polytope.thy
src/HOL/Analysis/Starlike.thy
     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Wed Jul 26 16:07:45 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Jul 27 15:22:35 2017 +0100
     1.3 @@ -79,20 +79,27 @@
     1.4  lemma hull_inc: "x \<in> S \<Longrightarrow> x \<in> P hull S"
     1.5    by (metis hull_subset subset_eq)
     1.6  
     1.7 -lemma hull_union_subset: "(S hull s) \<union> (S hull t) \<subseteq> (S hull (s \<union> t))"
     1.8 +lemma hull_Un_subset: "(S hull s) \<union> (S hull t) \<subseteq> (S hull (s \<union> t))"
     1.9    unfolding Un_subset_iff by (metis hull_mono Un_upper1 Un_upper2)
    1.10  
    1.11 -lemma hull_union:
    1.12 +lemma hull_Un:
    1.13    assumes T: "\<And>T. Ball T S \<Longrightarrow> S (\<Inter>T)"
    1.14    shows "S hull (s \<union> t) = S hull (S hull s \<union> S hull t)"
    1.15 -  apply rule
    1.16 -  apply (rule hull_mono)
    1.17 -  unfolding Un_subset_iff
    1.18 -  apply (metis hull_subset Un_upper1 Un_upper2 subset_trans)
    1.19 -  apply (rule hull_minimal)
    1.20 -  apply (metis hull_union_subset)
    1.21 -  apply (metis hull_in T)
    1.22 -  done
    1.23 +  apply (rule equalityI)
    1.24 +  apply (meson hull_mono hull_subset sup.mono)
    1.25 +  by (metis hull_Un_subset hull_hull hull_mono)
    1.26 +
    1.27 +lemma hull_Un_left: "P hull (S \<union> T) = P hull (P hull S \<union> T)"
    1.28 +  apply (rule equalityI)
    1.29 +   apply (simp add: Un_commute hull_mono hull_subset sup.coboundedI2)
    1.30 +  by (metis Un_subset_iff hull_hull hull_mono hull_subset)
    1.31 +
    1.32 +lemma hull_Un_right: "P hull (S \<union> T) = P hull (S \<union> P hull T)"
    1.33 +  by (metis hull_Un_left sup.commute)
    1.34 +
    1.35 +lemma hull_insert:
    1.36 +   "P hull (insert a S) = P hull (insert a (P hull S))"
    1.37 +  by (metis hull_Un_right insert_is_Un)
    1.38  
    1.39  lemma hull_redundant_eq: "a \<in> (S hull s) \<longleftrightarrow> S hull (insert a s) = S hull s"
    1.40    unfolding hull_def by blast
     2.1 --- a/src/HOL/Analysis/Polytope.thy	Wed Jul 26 16:07:45 2017 +0100
     2.2 +++ b/src/HOL/Analysis/Polytope.thy	Thu Jul 27 15:22:35 2017 +0100
     2.3 @@ -1230,6 +1230,179 @@
     2.4  by (metis (no_types) Krein_Milman_Minkowski assms compact_convex_hull convex_convex_hull face_of_imp_compact face_of_imp_convex)
     2.5  
     2.6  
     2.7 +lemma face_of_convex_hull_aux:
     2.8 +  assumes eq: "x *\<^sub>R p = u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c"
     2.9 +    and x: "u + v + w = x" "x \<noteq> 0" and S: "affine S" "a \<in> S" "b \<in> S" "c \<in> S"
    2.10 +  shows "p \<in> S"
    2.11 +proof -
    2.12 +  have "p = (u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c) /\<^sub>R x"
    2.13 +    by (metis \<open>x \<noteq> 0\<close> eq mult.commute right_inverse scaleR_one scaleR_scaleR)
    2.14 +  moreover have "affine hull {a,b,c} \<subseteq> S"
    2.15 +    by (simp add: S hull_minimal)
    2.16 +  moreover have "(u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c) /\<^sub>R x \<in> affine hull {a,b,c}"
    2.17 +    apply (simp add: affine_hull_3)
    2.18 +    apply (rule_tac x="u/x" in exI)
    2.19 +    apply (rule_tac x="v/x" in exI)
    2.20 +    apply (rule_tac x="w/x" in exI)
    2.21 +    using x apply (auto simp: algebra_simps divide_simps)
    2.22 +    done
    2.23 +  ultimately show ?thesis by force
    2.24 +qed
    2.25 +
    2.26 +proposition face_of_convex_hull_insert_eq:
    2.27 +  fixes a :: "'a :: euclidean_space"
    2.28 +  assumes "finite S" and a: "a \<notin> affine hull S"
    2.29 +  shows "(F face_of (convex hull (insert a S)) \<longleftrightarrow>
    2.30 +          F face_of (convex hull S) \<or>
    2.31 +          (\<exists>F'. F' face_of (convex hull S) \<and> F = convex hull (insert a F')))"
    2.32 +         (is "F face_of ?CAS \<longleftrightarrow> _")
    2.33 +proof safe
    2.34 +  assume F: "F face_of ?CAS"
    2.35 +    and *: "\<nexists>F'. F' face_of convex hull S \<and> F = convex hull insert a F'"
    2.36 +  obtain T where T: "T \<subseteq> insert a S" and FeqT: "F = convex hull T"
    2.37 +    by (metis F \<open>finite S\<close> compact_insert finite_imp_compact face_of_convex_hull_subset)
    2.38 +  show "F face_of convex hull S"
    2.39 +  proof (cases "a \<in> T")
    2.40 +    case True
    2.41 +    have "F = convex hull insert a (convex hull T \<inter> convex hull S)"
    2.42 +    proof
    2.43 +      have "T \<subseteq> insert a (convex hull T \<inter> convex hull S)"
    2.44 +        using T hull_subset by fastforce
    2.45 +      then show "F \<subseteq> convex hull insert a (convex hull T \<inter> convex hull S)"
    2.46 +        by (simp add: FeqT hull_mono)
    2.47 +      show "convex hull insert a (convex hull T \<inter> convex hull S) \<subseteq> F"
    2.48 +        apply (rule hull_minimal)
    2.49 +        using True by (auto simp: \<open>F = convex hull T\<close> hull_inc)
    2.50 +    qed
    2.51 +    moreover have "convex hull T \<inter> convex hull S face_of convex hull S"
    2.52 +      by (metis F FeqT convex_convex_hull face_of_slice hull_mono inf.absorb_iff2 subset_insertI)
    2.53 +    ultimately show ?thesis
    2.54 +      using * by force
    2.55 +  next
    2.56 +    case False
    2.57 +    then show ?thesis
    2.58 +      by (metis FeqT F T face_of_subset hull_mono subset_insert subset_insertI)
    2.59 +  qed
    2.60 +next
    2.61 +  assume "F face_of convex hull S"
    2.62 +  show "F face_of ?CAS"
    2.63 +    by (simp add: \<open>F face_of convex hull S\<close> a face_of_convex_hull_insert \<open>finite S\<close>)
    2.64 +next
    2.65 +  fix F
    2.66 +  assume F: "F face_of convex hull S"
    2.67 +  show "convex hull insert a F face_of ?CAS"
    2.68 +  proof (cases "S = {}")
    2.69 +    case True
    2.70 +    then show ?thesis
    2.71 +      using F face_of_affine_eq by auto
    2.72 +  next
    2.73 +    case False
    2.74 +    have anotc: "a \<notin> convex hull S"
    2.75 +      by (metis (no_types) a affine_hull_convex_hull hull_inc)
    2.76 +    show ?thesis
    2.77 +    proof (cases "F = {}")
    2.78 +      case True show ?thesis
    2.79 +        using anotc by (simp add: \<open>F = {}\<close> \<open>finite S\<close> extreme_point_of_convex_hull_insert face_of_singleton)
    2.80 +    next
    2.81 +      case False
    2.82 +      have "convex hull insert a F \<subseteq> ?CAS"
    2.83 +        by (simp add: F a \<open>finite S\<close> convex_hull_subset face_of_convex_hull_insert face_of_imp_subset hull_inc)
    2.84 +      moreover
    2.85 +      have "(\<exists>y v. (1 - ub) *\<^sub>R a + ub *\<^sub>R b = (1 - v) *\<^sub>R a + v *\<^sub>R y \<and>
    2.86 +                   0 \<le> v \<and> v \<le> 1 \<and> y \<in> F) \<and>
    2.87 +            (\<exists>x u. (1 - uc) *\<^sub>R a + uc *\<^sub>R c = (1 - u) *\<^sub>R a + u *\<^sub>R x \<and>
    2.88 +                   0 \<le> u \<and> u \<le> 1 \<and> x \<in> F)"
    2.89 +        if *: "(1 - ux) *\<^sub>R a + ux *\<^sub>R x
    2.90 +               \<in> open_segment ((1 - ub) *\<^sub>R a + ub *\<^sub>R b) ((1 - uc) *\<^sub>R a + uc *\<^sub>R c)"
    2.91 +          and "0 \<le> ub" "ub \<le> 1" "0 \<le> uc" "uc \<le> 1" "0 \<le> ux" "ux \<le> 1"
    2.92 +          and b: "b \<in> convex hull S" and c: "c \<in> convex hull S" and "x \<in> F"
    2.93 +        for b c ub uc ux x
    2.94 +      proof -
    2.95 +        obtain v where ne: "(1 - ub) *\<^sub>R a + ub *\<^sub>R b \<noteq> (1 - uc) *\<^sub>R a + uc *\<^sub>R c"
    2.96 +          and eq: "(1 - ux) *\<^sub>R a + ux *\<^sub>R x =
    2.97 +                    (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)"
    2.98 +          and "0 < v" "v < 1"
    2.99 +          using * by (auto simp: in_segment)
   2.100 +        then have 0: "((1 - ux) - ((1 - v) * (1 - ub) + v * (1 - uc))) *\<^sub>R a +
   2.101 +                      (ux *\<^sub>R x - (((1 - v) * ub) *\<^sub>R b + (v * uc) *\<^sub>R c)) = 0"
   2.102 +          by (auto simp: algebra_simps)
   2.103 +        then have "((1 - ux) - ((1 - v) * (1 - ub) + v * (1 - uc))) *\<^sub>R a =
   2.104 +                   ((1 - v) * ub) *\<^sub>R b + (v * uc) *\<^sub>R c + (-ux) *\<^sub>R x"
   2.105 +          by (auto simp: algebra_simps)
   2.106 +        then have "a \<in> affine hull S" if "1 - ux - ((1 - v) * (1 - ub) + v * (1 - uc)) \<noteq> 0"
   2.107 +          apply (rule face_of_convex_hull_aux)
   2.108 +          using b c that apply (auto simp: algebra_simps)
   2.109 +          using F convex_hull_subset_affine_hull face_of_imp_subset \<open>x \<in> F\<close> apply blast+
   2.110 +          done
   2.111 +        then have "1 - ux - ((1 - v) * (1 - ub) + v * (1 - uc)) = 0"
   2.112 +          using a by blast
   2.113 +        with 0 have equx: "(1 - v) * ub + v * uc = ux"
   2.114 +          and uxx: "ux *\<^sub>R x = (((1 - v) * ub) *\<^sub>R b + (v * uc) *\<^sub>R c)"
   2.115 +          by auto (auto simp: algebra_simps)
   2.116 +        show ?thesis
   2.117 +        proof (cases "uc = 0")
   2.118 +          case True
   2.119 +          then show ?thesis
   2.120 +            using equx 0 \<open>0 \<le> ub\<close> \<open>ub \<le> 1\<close> \<open>v < 1\<close> \<open>x \<in> F\<close>
   2.121 +            apply (auto simp: algebra_simps)
   2.122 +             apply (rule_tac x=x in exI, simp)
   2.123 +             apply (rule_tac x=ub in exI, auto)
   2.124 +             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)
   2.125 +            using \<open>x \<in> F\<close> \<open>uc \<le> 1\<close> apply blast
   2.126 +            done
   2.127 +        next
   2.128 +          case False
   2.129 +          show ?thesis
   2.130 +          proof (cases "ub = 0")
   2.131 +            case True
   2.132 +            then show ?thesis
   2.133 +              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)
   2.134 +          next
   2.135 +            case False
   2.136 +            then have "0 < ub" "0 < uc"
   2.137 +              using \<open>uc \<noteq> 0\<close> \<open>0 \<le> ub\<close> \<open>0 \<le> uc\<close> by auto
   2.138 +            then have "ux \<noteq> 0"
   2.139 +              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)
   2.140 +            have "b \<in> F \<and> c \<in> F"
   2.141 +            proof (cases "b = c")
   2.142 +              case True
   2.143 +              then show ?thesis
   2.144 +                by (metis \<open>ux \<noteq> 0\<close> equx real_vector.scale_cancel_left scaleR_add_left uxx \<open>x \<in> F\<close>)
   2.145 +            next
   2.146 +              case False
   2.147 +              have "x = (((1 - v) * ub) *\<^sub>R b + (v * uc) *\<^sub>R c) /\<^sub>R ux"
   2.148 +                by (metis \<open>ux \<noteq> 0\<close> uxx mult.commute right_inverse scaleR_one scaleR_scaleR)
   2.149 +              also have "... = (1 - v * uc / ux) *\<^sub>R b + (v * uc / ux) *\<^sub>R c"
   2.150 +                using \<open>ux \<noteq> 0\<close> equx apply (auto simp: algebra_simps divide_simps)
   2.151 +                by (metis add.commute add_diff_eq add_divide_distrib diff_add_cancel scaleR_add_left)
   2.152 +              finally have "x = (1 - v * uc / ux) *\<^sub>R b + (v * uc / ux) *\<^sub>R c" .
   2.153 +              then have "x \<in> open_segment b c"
   2.154 +                apply (simp add: in_segment \<open>b \<noteq> c\<close>)
   2.155 +                apply (rule_tac x="(v * uc) / ux" in exI)
   2.156 +                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
   2.157 +                apply (force simp: algebra_simps divide_simps)
   2.158 +                done
   2.159 +              then show ?thesis
   2.160 +                by (rule face_ofD [OF F _ b c \<open>x \<in> F\<close>])
   2.161 +            qed
   2.162 +            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
   2.163 +          qed
   2.164 +        qed
   2.165 +      qed
   2.166 +      moreover have "convex hull F = F"
   2.167 +        by (meson F convex_hull_eq face_of_imp_convex)
   2.168 +      ultimately show ?thesis
   2.169 +        unfolding face_of_def by (fastforce simp: convex_hull_insert_alt \<open>S \<noteq> {}\<close> \<open>F \<noteq> {}\<close>)
   2.170 +    qed
   2.171 +  qed
   2.172 +qed
   2.173 +
   2.174 +lemma face_of_convex_hull_insert2:
   2.175 +  fixes a :: "'a :: euclidean_space"
   2.176 +  assumes S: "finite S" and a: "a \<notin> affine hull S" and F: "F face_of convex hull S"
   2.177 +  shows "convex hull (insert a F) face_of convex hull (insert a S)"
   2.178 +  by (metis F face_of_convex_hull_insert_eq [OF S a])
   2.179 +
   2.180  proposition face_of_convex_hull_affine_independent:
   2.181    fixes S :: "'a::euclidean_space set"
   2.182    assumes "~ affine_dependent S"
   2.183 @@ -1429,6 +1602,23 @@
   2.184  lemma polytope_sing: "polytope {a}"
   2.185    using polytope_def by force
   2.186  
   2.187 +lemma face_of_polytope_insert:
   2.188 +     "\<lbrakk>polytope S; a \<notin> affine hull S; F face_of S\<rbrakk> \<Longrightarrow> F face_of convex hull (insert a S)"
   2.189 +  by (metis (no_types, lifting) affine_hull_convex_hull face_of_convex_hull_insert hull_insert polytope_def)
   2.190 +
   2.191 +lemma face_of_polytope_insert2:
   2.192 +  fixes a :: "'a :: euclidean_space"
   2.193 +  assumes "polytope S" "a \<notin> affine hull S" "F face_of S"
   2.194 +  shows "convex hull (insert a F) face_of convex hull (insert a S)"
   2.195 +proof -
   2.196 +  obtain V where "finite V" "S = convex hull V"
   2.197 +    using assms by (auto simp: polytope_def)
   2.198 +  then have "convex hull (insert a F) face_of convex hull (insert a V)"
   2.199 +    using affine_hull_convex_hull assms face_of_convex_hull_insert2 by blast
   2.200 +  then show ?thesis
   2.201 +    by (metis \<open>S = convex hull V\<close> hull_insert)
   2.202 +qed
   2.203 +
   2.204  
   2.205  subsection\<open>Polyhedra\<close>
   2.206  
   2.207 @@ -2638,38 +2828,41 @@
   2.208    qed
   2.209  qed
   2.210  
   2.211 -
   2.212  lemma cell_subdivision_lemma:
   2.213    assumes "finite \<F>"
   2.214        and "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
   2.215        and "\<And>X. X \<in> \<F> \<Longrightarrow> aff_dim X \<le> d"
   2.216        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"
   2.217        and "finite I"
   2.218 -    shows "\<exists>\<F>'. \<Union>\<F>' = \<Union>\<F> \<and>
   2.219 -                 finite \<F>' \<and>
   2.220 -                 (\<forall>X \<in> \<F>'. polytope X) \<and>
   2.221 -                 (\<forall>X \<in> \<F>'. aff_dim X \<le> d) \<and>
   2.222 -                 (\<forall>X \<in> \<F>'. \<forall>Y \<in> \<F>'. X \<inter> Y face_of X \<and> X \<inter> Y face_of Y) \<and>
   2.223 -                 (\<forall>X \<in> \<F>'. \<forall>x \<in> X. \<forall>y \<in> X. \<forall>a b.
   2.224 +    shows "\<exists>\<G>. \<Union>\<G> = \<Union>\<F> \<and>
   2.225 +                 finite \<G> \<and>
   2.226 +                 (\<forall>C \<in> \<G>. \<exists>D. D \<in> \<F> \<and> C \<subseteq> D) \<and>
   2.227 +                 (\<forall>C \<in> \<F>. \<forall>x \<in> C. \<exists>D. D \<in> \<G> \<and> x \<in> D \<and> D \<subseteq> C) \<and>
   2.228 +                 (\<forall>X \<in> \<G>. polytope X) \<and>
   2.229 +                 (\<forall>X \<in> \<G>. aff_dim X \<le> d) \<and>
   2.230 +                 (\<forall>X \<in> \<G>. \<forall>Y \<in> \<G>. X \<inter> Y face_of X \<and> X \<inter> Y face_of Y) \<and>
   2.231 +                 (\<forall>X \<in> \<G>. \<forall>x \<in> X. \<forall>y \<in> X. \<forall>a b.
   2.232                            (a,b) \<in> I \<longrightarrow> a \<bullet> x \<le> b \<and> a \<bullet> y \<le> b \<or>
   2.233                                          a \<bullet> x \<ge> b \<and> a \<bullet> y \<ge> b)"
   2.234    using \<open>finite I\<close>
   2.235  proof induction
   2.236    case empty
   2.237    then show ?case
   2.238 -    by (rule_tac x="\<F>" in exI) (simp add: assms)
   2.239 +    by (rule_tac x="\<F>" in exI) (auto simp: assms)
   2.240  next
   2.241    case (insert ab I)
   2.242 -  then obtain \<F>' where eq: "\<Union>\<F>' = \<Union>\<F>" and "finite \<F>'"
   2.243 -                   and poly: "\<And>X. X \<in> \<F>' \<Longrightarrow> polytope X"
   2.244 -                   and aff: "\<And>X. X \<in> \<F>' \<Longrightarrow> aff_dim X \<le> d"
   2.245 -                   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"
   2.246 -                   and I: "\<And>X x y a b.  \<lbrakk>X \<in> \<F>'; x \<in> X; y \<in> X; (a,b) \<in> I\<rbrakk> \<Longrightarrow>
   2.247 +  then obtain \<G> where eq: "\<Union>\<G> = \<Union>\<F>" and "finite \<G>"
   2.248 +                   and sub1: "\<And>C. C \<in> \<G> \<Longrightarrow> \<exists>D. D \<in> \<F> \<and> C \<subseteq> D"
   2.249 +                   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"
   2.250 +                   and poly: "\<And>X. X \<in> \<G> \<Longrightarrow> polytope X"
   2.251 +                   and aff: "\<And>X. X \<in> \<G> \<Longrightarrow> aff_dim X \<le> d"
   2.252 +                   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"
   2.253 +                   and I: "\<And>X x y a b.  \<lbrakk>X \<in> \<G>; x \<in> X; y \<in> X; (a,b) \<in> I\<rbrakk> \<Longrightarrow>
   2.254                                      a \<bullet> x \<le> b \<and> a \<bullet> y \<le> b \<or> a \<bullet> x \<ge> b \<and> a \<bullet> y \<ge> b"
   2.255      by (auto simp: that)
   2.256    obtain a b where "ab = (a,b)"
   2.257      by fastforce
   2.258 -  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>'"
   2.259 +  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>"
   2.260    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
   2.261      by blast
   2.262    show ?case
   2.263 @@ -2677,7 +2870,7 @@
   2.264      show "\<Union>?\<G> = \<Union>\<F>"
   2.265        by (force simp: eq [symmetric])
   2.266      show "finite ?\<G>"
   2.267 -      using \<open>finite \<F>'\<close> by force
   2.268 +      using \<open>finite \<G>\<close> by force
   2.269      show "\<forall>X \<in> ?\<G>. polytope X"
   2.270        by (force simp: poly polytope_Int_polyhedron polyhedron_halfspace_le polyhedron_halfspace_ge)
   2.271      show "\<forall>X \<in> ?\<G>. aff_dim X \<le> d"
   2.272 @@ -2688,6 +2881,19 @@
   2.273        using \<open>ab = (a, b)\<close> I by fastforce
   2.274      show "\<forall>X \<in> ?\<G>. \<forall>Y \<in> ?\<G>. X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
   2.275        by (auto simp: eqInt halfspace_Int_eq face_of_Int_Int face face_of_halfspace_le face_of_halfspace_ge)
   2.276 +    show "\<forall>C \<in> ?\<G>. \<exists>D. D \<in> \<F> \<and> C \<subseteq> D"
   2.277 +      using sub1 by force
   2.278 +    show "\<forall>C\<in>\<F>. \<forall>x\<in>C. \<exists>D. D \<in> ?\<G> \<and> x \<in> D \<and> D \<subseteq> C"
   2.279 +    proof (intro ballI)
   2.280 +      fix C z
   2.281 +      assume "C \<in> \<F>" "z \<in> C"
   2.282 +      with sub2 obtain D where D: "D \<in> \<G>" "z \<in> D" "D \<subseteq> C" by blast
   2.283 +      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>
   2.284 +            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"
   2.285 +        using linorder_class.linear [of "a \<bullet> z" b] D by blast
   2.286 +      then show "\<exists>D. D \<in> ?\<G> \<and> z \<in> D \<and> D \<subseteq> C"
   2.287 +        by blast
   2.288 +    qed
   2.289    qed
   2.290  qed
   2.291  
   2.292 @@ -2701,6 +2907,8 @@
   2.293    obtains "\<F>'" where "finite \<F>'" "\<Union>\<F>' = \<Union>\<F>" "\<And>X. X \<in> \<F>' \<Longrightarrow> diameter X < e"
   2.294                  "\<And>X. X \<in> \<F>' \<Longrightarrow> polytope X" "\<And>X. X \<in> \<F>' \<Longrightarrow> aff_dim X \<le> d"
   2.295                  "\<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"
   2.296 +                "\<And>C. C \<in> \<F>' \<Longrightarrow> \<exists>D. D \<in> \<F> \<and> C \<subseteq> D"
   2.297 +                "\<And>C x. C \<in> \<F> \<and> x \<in> C \<Longrightarrow> \<exists>D. D \<in> \<F>' \<and> x \<in> D \<and> D \<subseteq> C"
   2.298  proof -
   2.299    have "bounded(\<Union>\<F>)"
   2.300      by (simp add: \<open>finite \<F>\<close> poly bounded_Union polytope_imp_bounded)
   2.301 @@ -2723,9 +2931,10 @@
   2.302                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"
   2.303                and I: "\<And>X x y a b.  \<lbrakk>X \<in> \<F>'; x \<in> X; y \<in> X; (a,b) \<in> I\<rbrakk> \<Longrightarrow>
   2.304                                       a \<bullet> x \<le> b \<and> a \<bullet> y \<le> b \<or> a \<bullet> x \<ge> b \<and> a \<bullet> y \<ge> b"
   2.305 +              and sub1: "\<And>C. C \<in> \<F>' \<Longrightarrow> \<exists>D. D \<in> \<F> \<and> C \<subseteq> D"
   2.306 +              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"
   2.307      apply (rule exE [OF cell_subdivision_lemma])
   2.308 -         apply (rule assms \<open>finite I\<close> | assumption)+
   2.309 -    apply (auto intro: that)
   2.310 +    using assms \<open>finite I\<close> apply auto
   2.311      done
   2.312    show ?thesis
   2.313    proof (rule_tac \<F>'="\<F>'" in that)
   2.314 @@ -2788,14 +2997,13 @@
   2.315          by (simp add: \<open>0 < e\<close>)
   2.316        finally show ?thesis .
   2.317      qed
   2.318 -  qed (auto simp: eq poly aff face \<open>finite \<F>'\<close>)
   2.319 +  qed (auto simp: eq poly aff face sub1 sub2 \<open>finite \<F>'\<close>)
   2.320  qed
   2.321  
   2.322  
   2.323 -subsection\<open>Simplicial complexes and triangulations\<close>
   2.324 +subsection\<open>Simplexes\<close>
   2.325  
   2.326 -subsubsection\<open>The notion of n-simplex for integer @{term"n \<ge> -1"}\<close>
   2.327 -
   2.328 +text\<open>The notion of n-simplex for integer @{term"n \<ge> -1"}\<close>
   2.329  definition simplex :: "int \<Rightarrow> 'a::euclidean_space set \<Rightarrow> bool" (infix "simplex" 50)
   2.330    where "n simplex S \<equiv> \<exists>C. ~(affine_dependent C) \<and> int(card C) = n + 1 \<and> S = convex hull C"
   2.331  
   2.332 @@ -2917,4 +3125,690 @@
   2.333    qed (use C in auto)
   2.334  qed
   2.335  
   2.336 +subsection\<open>Simplicial complexes and triangulations\<close>
   2.337 +
   2.338 +definition simplicial_complex where
   2.339 + "simplicial_complex \<C> \<equiv>
   2.340 +        finite \<C> \<and>
   2.341 +        (\<forall>S \<in> \<C>. \<exists>n. n simplex S) \<and>
   2.342 +        (\<forall>F S. S \<in> \<C> \<and> F face_of S \<longrightarrow> F \<in> \<C>) \<and>
   2.343 +        (!S S'. S \<in> \<C> \<and> S' \<in> \<C>
   2.344 +                \<longrightarrow> (S \<inter> S') face_of S \<and> (S \<inter> S') face_of S')"
   2.345 +
   2.346 +definition triangulation where
   2.347 + "triangulation \<T> \<equiv>
   2.348 +        finite \<T> \<and>
   2.349 +        (\<forall>T \<in> \<T>. \<exists>n. n simplex T) \<and>
   2.350 +        (\<forall>T T'. T \<in> \<T> \<and> T' \<in> \<T>
   2.351 +                \<longrightarrow> (T \<inter> T') face_of T \<and> (T \<inter> T') face_of T')"
   2.352 +
   2.353 +
   2.354 +subsection\<open>Refining a cell complex to a simplicial complex\<close>
   2.355 +
   2.356 +lemma convex_hull_insert_Int_eq:
   2.357 +  fixes z :: "'a :: euclidean_space"
   2.358 +  assumes z: "z \<in> rel_interior S"
   2.359 +      and T: "T \<subseteq> rel_frontier S"
   2.360 +      and U: "U \<subseteq> rel_frontier S"
   2.361 +      and "convex S" "convex T" "convex U"
   2.362 +  shows "convex hull (insert z T) \<inter> convex hull (insert z U) = convex hull (insert z (T \<inter> U))"
   2.363 +    (is "?lhs = ?rhs")
   2.364 +proof
   2.365 +  show "?lhs \<subseteq> ?rhs"
   2.366 +  proof (cases "T={} \<or> U={}")
   2.367 +    case True then show ?thesis by auto
   2.368 +  next
   2.369 +    case False
   2.370 +    then have "T \<noteq> {}" "U \<noteq> {}" by auto
   2.371 +    have TU: "convex (T \<inter> U)"
   2.372 +      by (simp add: \<open>convex T\<close> \<open>convex U\<close> convex_Int)
   2.373 +    have "(\<Union>x\<in>T. closed_segment z x) \<inter> (\<Union>x\<in>U. closed_segment z x)
   2.374 +          \<subseteq> (if T \<inter> U = {} then {z} else UNION (T \<inter> U) (closed_segment z))" (is "_ \<subseteq> ?IF")
   2.375 +    proof clarify
   2.376 +      fix x t u
   2.377 +      assume xt: "x \<in> closed_segment z t"
   2.378 +        and xu: "x \<in> closed_segment z u"
   2.379 +        and "t \<in> T" "u \<in> U"
   2.380 +      then have ne: "t \<noteq> z" "u \<noteq> z"
   2.381 +        using T U z unfolding rel_frontier_def by blast+
   2.382 +      show "x \<in> ?IF"
   2.383 +      proof (cases "x = z")
   2.384 +        case True then show ?thesis by auto
   2.385 +      next
   2.386 +        case False
   2.387 +        have t: "t \<in> closure S"
   2.388 +          using T \<open>t \<in> T\<close> rel_frontier_def by auto
   2.389 +        have u: "u \<in> closure S"
   2.390 +          using U \<open>u \<in> U\<close> rel_frontier_def by auto
   2.391 +        show ?thesis
   2.392 +        proof (cases "t = u")
   2.393 +          case True
   2.394 +          then show ?thesis
   2.395 +            using \<open>t \<in> T\<close> \<open>u \<in> U\<close> xt by auto
   2.396 +        next
   2.397 +          case False
   2.398 +          have tnot: "t \<notin> closed_segment u z"
   2.399 +          proof -
   2.400 +            have "t \<in> closure S - rel_interior S"
   2.401 +              using T \<open>t \<in> T\<close> rel_frontier_def by blast
   2.402 +            then have "t \<notin> open_segment z u"
   2.403 +              by (meson DiffD2 rel_interior_closure_convex_segment [OF \<open>convex S\<close> z u] subsetD)
   2.404 +            then show ?thesis
   2.405 +              by (simp add: \<open>t \<noteq> u\<close> \<open>t \<noteq> z\<close> open_segment_commute open_segment_def)
   2.406 +          qed
   2.407 +          moreover have "u \<notin> closed_segment z t"
   2.408 +            using rel_interior_closure_convex_segment [OF \<open>convex S\<close> z t] \<open>u \<in> U\<close> \<open>u \<noteq> z\<close>
   2.409 +              U [unfolded rel_frontier_def] tnot
   2.410 +            by (auto simp: closed_segment_eq_open)
   2.411 +          ultimately
   2.412 +          have "~(between (t,u) z | between (u,z) t | between (z,t) u)" if "x \<noteq> z"
   2.413 +            using that xt xu
   2.414 +            apply (simp add: between_mem_segment [symmetric])
   2.415 +            by (metis between_commute between_trans_2 between_antisym)
   2.416 +          then have "~ collinear {t, z, u}" if "x \<noteq> z"
   2.417 +            by (auto simp: that collinear_between_cases between_commute)
   2.418 +          moreover have "collinear {t, z, x}"
   2.419 +            by (metis closed_segment_commute collinear_2 collinear_closed_segment collinear_triples ends_in_segment(1) insert_absorb insert_absorb2 xt)
   2.420 +          moreover have "collinear {z, x, u}"
   2.421 +            by (metis closed_segment_commute collinear_2 collinear_closed_segment collinear_triples ends_in_segment(1) insert_absorb insert_absorb2 xu)
   2.422 +          ultimately have False
   2.423 +            using collinear_3_trans [of t z x u] \<open>x \<noteq> z\<close> by blast
   2.424 +          then show ?thesis by metis
   2.425 +        qed
   2.426 +      qed
   2.427 +    qed
   2.428 +    then show ?thesis
   2.429 +      using False \<open>convex T\<close> \<open>convex U\<close> TU
   2.430 +      by (simp add: convex_hull_insert_segments hull_same split: if_split_asm)
   2.431 +  qed
   2.432 +  show "?rhs \<subseteq> ?lhs"
   2.433 +    by (metis inf_greatest hull_mono inf.cobounded1 inf.cobounded2 insert_mono)
   2.434 +qed
   2.435 +
   2.436 +lemma simplicial_subdivision_aux:
   2.437 +  assumes "finite \<M>"
   2.438 +      and "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
   2.439 +      and "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C \<le> of_nat n"
   2.440 +      and "\<And>C F. \<lbrakk>C \<in> \<M>; F face_of C\<rbrakk> \<Longrightarrow> F \<in> \<M>"
   2.441 +      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"
   2.442 +    shows "\<exists>\<T>. simplicial_complex \<T> \<and>
   2.443 +                (\<forall>K \<in> \<T>. aff_dim K \<le> of_nat n) \<and>
   2.444 +                \<Union>\<T> = \<Union>\<M> \<and>
   2.445 +                (\<forall>C \<in> \<M>. \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F) \<and>
   2.446 +                (\<forall>K \<in> \<T>. \<exists>C. C \<in> \<M> \<and> K \<subseteq> C)"
   2.447 +  using assms
   2.448 +proof (induction n arbitrary: \<M> rule: less_induct)
   2.449 +  case (less n)
   2.450 +  then have poly\<M>: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
   2.451 +      and aff\<M>:    "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C \<le> of_nat n"
   2.452 +      and face\<M>:   "\<And>C F. \<lbrakk>C \<in> \<M>; F face_of C\<rbrakk> \<Longrightarrow> F \<in> \<M>"
   2.453 +      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"
   2.454 +    by metis+
   2.455 +  show ?case
   2.456 +  proof (cases "n \<le> 1")
   2.457 +    case True
   2.458 +    have "\<And>s. \<lbrakk>n \<le> 1; s \<in> \<M>\<rbrakk> \<Longrightarrow> \<exists>m. m simplex s"
   2.459 +      using poly\<M> aff\<M> by (force intro: polytope_lowdim_imp_simplex)
   2.460 +    then show ?thesis
   2.461 +      unfolding simplicial_complex_def
   2.462 +      apply (rule_tac x="\<M>" in exI)
   2.463 +      using True by (auto simp: less.prems)
   2.464 +  next
   2.465 +    case False
   2.466 +    define \<S> where "\<S> \<equiv> {C \<in> \<M>. aff_dim C < n}"
   2.467 +    have "finite \<S>" "\<And>C. C \<in> \<S> \<Longrightarrow> polytope C" "\<And>C. C \<in> \<S> \<Longrightarrow> aff_dim C \<le> int (n - 1)"
   2.468 +         "\<And>C F. \<lbrakk>C \<in> \<S>; F face_of C\<rbrakk> \<Longrightarrow> F \<in> \<S>"
   2.469 +         "\<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"
   2.470 +      using less.prems
   2.471 +      apply (auto simp: \<S>_def)
   2.472 +      by (metis aff_dim_subset face_of_imp_subset less_le not_le)
   2.473 +    with less.IH [of "n-1" \<S>] False
   2.474 +    obtain \<U> where "simplicial_complex \<U>"
   2.475 +           and aff_dim\<U>: "\<And>K. K \<in> \<U> \<Longrightarrow> aff_dim K \<le> int (n - 1)"
   2.476 +           and        "\<Union>\<U> = \<Union>\<S>"
   2.477 +           and fin\<U>:  "\<And>C. C \<in> \<S> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<U> \<and> C = \<Union>F"
   2.478 +           and C\<U>:    "\<And>K. K \<in> \<U> \<Longrightarrow> \<exists>C. C \<in> \<S> \<and> K \<subseteq> C"
   2.479 +      by auto
   2.480 +    then have "finite \<U>"
   2.481 +         and simpl\<U>: "\<And>S. S \<in> \<U> \<Longrightarrow> \<exists>n. n simplex S"
   2.482 +         and face\<U>:  "\<And>F S. \<lbrakk>S \<in> \<U>; F face_of S\<rbrakk> \<Longrightarrow> F \<in> \<U>"
   2.483 +         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'"
   2.484 +      by (auto simp: simplicial_complex_def)
   2.485 +    define \<N> where "\<N> \<equiv> {C \<in> \<M>. aff_dim C = n}"
   2.486 +    have "finite \<N>"
   2.487 +      by (simp add: \<N>_def less.prems(1))
   2.488 +    have poly\<N>: "\<And>C. C \<in> \<N> \<Longrightarrow> polytope C"
   2.489 +      and convex\<N>: "\<And>C. C \<in> \<N> \<Longrightarrow> convex C"
   2.490 +      and closed\<N>: "\<And>C. C \<in> \<N> \<Longrightarrow> closed C"
   2.491 +      by (auto simp: \<N>_def poly\<M> polytope_imp_convex polytope_imp_closed)
   2.492 +    have in_rel_interior: "(@z. z \<in> rel_interior C) \<in> rel_interior C" if "C \<in> \<N>" for C
   2.493 +        using that poly\<M> polytope_imp_convex rel_interior_aff_dim some_in_eq by (fastforce simp: \<N>_def)
   2.494 +    have *: "\<exists>T. ~affine_dependent T \<and> card T \<le> n \<and> aff_dim K < n \<and> K = convex hull T"
   2.495 +      if "K \<in> \<U>" for K
   2.496 +    proof -
   2.497 +      obtain r where r: "r simplex K"
   2.498 +        using \<open>K \<in> \<U>\<close> simpl\<U> by blast
   2.499 +      have "r = aff_dim K"
   2.500 +        using \<open>r simplex K\<close> aff_dim_simplex by blast
   2.501 +      with r
   2.502 +      show ?thesis
   2.503 +        unfolding simplex_def
   2.504 +        using False \<open>\<And>K. K \<in> \<U> \<Longrightarrow> aff_dim K \<le> int (n - 1)\<close> that by fastforce
   2.505 +    qed
   2.506 +    have ahK_C_disjoint: "affine hull K \<inter> rel_interior C = {}"
   2.507 +      if "C \<in> \<N>" "K \<in> \<U>" "K \<subseteq> rel_frontier C" for C K
   2.508 +    proof -
   2.509 +      have "convex C" "closed C"
   2.510 +        by (auto simp: convex\<N> closed\<N> \<open>C \<in> \<N>\<close>)
   2.511 +      obtain F where F: "F face_of C" and "F \<noteq> C" "K \<subseteq> F"
   2.512 +      proof -
   2.513 +        obtain L where "L \<in> \<S>" "K \<subseteq> L"
   2.514 +          using \<open>K \<in> \<U>\<close> C\<U> by blast
   2.515 +        have "K \<le> rel_frontier C"
   2.516 +          by (simp add: \<open>K \<subseteq> rel_frontier C\<close>)
   2.517 +        also have "... \<le> C"
   2.518 +          by (simp add: \<open>closed C\<close> rel_frontier_def subset_iff)
   2.519 +        finally have "K \<subseteq> C" .
   2.520 +        have "L \<inter> C face_of C"
   2.521 +          using \<N>_def \<S>_def \<open>C \<in> \<N>\<close> \<open>L \<in> \<S>\<close> intface\<M> by auto
   2.522 +        moreover have "L \<inter> C \<noteq> C"
   2.523 +          using \<open>C \<in> \<N>\<close> \<open>L \<in> \<S>\<close>
   2.524 +          apply (clarsimp simp: \<N>_def \<S>_def)
   2.525 +          by (metis aff_dim_subset inf_le1 not_le)
   2.526 +        moreover have "K \<subseteq> L \<inter> C"
   2.527 +          using \<open>C \<in> \<N>\<close> \<open>L \<in> \<S>\<close> \<open>K \<subseteq> C\<close> \<open>K \<subseteq> L\<close>
   2.528 +          by (auto simp: \<N>_def \<S>_def)
   2.529 +        ultimately show ?thesis using that by metis
   2.530 +      qed
   2.531 +      have "affine hull F \<inter> rel_interior C = {}"
   2.532 +        by (rule affine_hull_face_of_disjoint_rel_interior [OF \<open>convex C\<close> F \<open>F \<noteq> C\<close>])
   2.533 +      with hull_mono [OF \<open>K \<subseteq> F\<close>]
   2.534 +      show "affine hull K \<inter> rel_interior C = {}"
   2.535 +        by fastforce
   2.536 +    qed
   2.537 +    let ?\<T> = "(\<Union>C \<in> \<N>. \<Union>K \<in> \<U> \<inter> Pow (rel_frontier C).
   2.538 +                     {convex hull (insert (@z. z \<in> rel_interior C) K)})"
   2.539 +    have "\<exists>\<T>. simplicial_complex \<T> \<and>
   2.540 +              (\<forall>K \<in> \<T>. aff_dim K \<le> of_nat n) \<and>
   2.541 +              (\<forall>C \<in> \<M>. \<exists>F. F \<subseteq> \<T> \<and> C = \<Union>F) \<and>
   2.542 +              (\<forall>K \<in> \<T>. \<exists>C. C \<in> \<M> \<and> K \<subseteq> C)"
   2.543 +    proof (rule exI, intro conjI ballI)
   2.544 +      show "simplicial_complex (\<U> \<union> ?\<T>)"
   2.545 +        unfolding simplicial_complex_def
   2.546 +      proof (intro conjI impI ballI allI)
   2.547 +        show "finite (\<U> \<union> ?\<T>)"
   2.548 +          using \<open>finite \<U>\<close> \<open>finite \<N>\<close> by simp
   2.549 +        show "\<exists>n. n simplex S" if "S \<in> \<U> \<union> ?\<T>" for S
   2.550 +          using that ahK_C_disjoint in_rel_interior simpl\<U> simplex_insert_dimplus1 by fastforce
   2.551 +        show "F \<in> \<U> \<union> ?\<T>" if S: "S \<in> \<U> \<union> ?\<T> \<and> F face_of S" for F S
   2.552 +        proof -
   2.553 +          have "F \<in> \<U>" if "S \<in> \<U>"
   2.554 +            using S face\<U> that by blast
   2.555 +          moreover have "F \<in> \<U> \<union> ?\<T>"
   2.556 +            if "F face_of S" "C \<in> \<N>" "K \<in> \<U>" and "K \<subseteq> rel_frontier C"
   2.557 +              and S: "S = convex hull insert (@z. z \<in> rel_interior C) K" for C K
   2.558 +          proof -
   2.559 +            let ?z = "@z. z \<in> rel_interior C"
   2.560 +            have "?z \<in> rel_interior C"
   2.561 +              by (simp add: in_rel_interior \<open>C \<in> \<N>\<close>)
   2.562 +            moreover
   2.563 +            obtain I where "\<not> affine_dependent I" "card I \<le> n" "aff_dim K < int n" "K = convex hull I"
   2.564 +              using * [OF \<open>K \<in> \<U>\<close>] by auto
   2.565 +            ultimately have "?z \<notin> affine hull I"
   2.566 +              using ahK_C_disjoint affine_hull_convex_hull that by blast
   2.567 +            have "compact I" "finite I"
   2.568 +              by (auto simp: \<open>\<not> affine_dependent I\<close> aff_independent_finite finite_imp_compact)
   2.569 +            moreover have "F face_of convex hull insert ?z I"
   2.570 +              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)
   2.571 +            ultimately obtain J where "J \<subseteq> insert ?z I" "F = convex hull J"
   2.572 +              using face_of_convex_hull_subset [of "insert ?z I" F] by auto
   2.573 +            show ?thesis
   2.574 +            proof (cases "?z \<in> J")
   2.575 +              case True
   2.576 +              have "F \<in> (\<Union>K\<in>\<U> \<inter> Pow (rel_frontier C). {convex hull insert ?z K})"
   2.577 +              proof
   2.578 +                have "convex hull (J - {?z}) face_of K"
   2.579 +                  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)
   2.580 +                then have "convex hull (J - {?z}) \<in> \<U>"
   2.581 +                  by (rule face\<U> [OF \<open>K \<in> \<U>\<close>])
   2.582 +                moreover
   2.583 +                have "\<And>x. x \<in> convex hull (J - {?z}) \<Longrightarrow> x \<in> rel_frontier C"
   2.584 +                  by (metis True \<open>J \<subseteq> insert ?z I\<close> \<open>K = convex hull I\<close> subsetD hull_mono subset_insert_iff that(4))
   2.585 +                ultimately show "convex hull (J - {?z}) \<in> \<U> \<inter> Pow (rel_frontier C)" by auto
   2.586 +                let ?F = "convex hull insert ?z (convex hull (J - {?z}))"
   2.587 +                have "F \<subseteq> ?F"
   2.588 +                  apply (clarsimp simp: \<open>F = convex hull J\<close>)
   2.589 +                  by (metis True subsetD hull_mono hull_subset subset_insert_iff)
   2.590 +                moreover have "?F \<subseteq> F"
   2.591 +                  apply (clarsimp simp: \<open>F = convex hull J\<close>)
   2.592 +                  by (metis (no_types, lifting) True convex_hull_eq_empty convex_hull_insert_segments hull_hull insert_Diff)
   2.593 +                ultimately
   2.594 +                show "F \<in> {?F}" by auto
   2.595 +              qed
   2.596 +              with \<open>C\<in>\<N>\<close> show ?thesis by auto
   2.597 +            next
   2.598 +              case False
   2.599 +              then have "F \<in> \<U>"
   2.600 +                using face_of_convex_hull_affine_independent [OF \<open>\<not> affine_dependent I\<close>]
   2.601 +                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>)
   2.602 +              then show "F \<in> \<U> \<union> ?\<T>"
   2.603 +                by blast
   2.604 +            qed
   2.605 +          qed
   2.606 +          ultimately show ?thesis
   2.607 +            using that by auto
   2.608 +        qed
   2.609 +        have "(S \<inter> S' face_of S) \<and> (S \<inter> S' face_of S')"
   2.610 +          if "S \<in> \<U> \<union> ?\<T>" "S' \<in> \<U> \<union> ?\<T>" for S S'
   2.611 +        proof -
   2.612 +          have symmy: "\<lbrakk>\<And>X Y. R X Y \<Longrightarrow> R Y X;
   2.613 +                        \<And>X Y. \<lbrakk>X \<in> \<U>; Y \<in> \<U>\<rbrakk> \<Longrightarrow> R X Y;
   2.614 +                        \<And>X Y. \<lbrakk>X \<in> \<U>; Y \<in> ?\<T>\<rbrakk> \<Longrightarrow> R X Y;
   2.615 +                        \<And>X Y. \<lbrakk>X \<in> ?\<T>; Y \<in> ?\<T>\<rbrakk> \<Longrightarrow> R X Y\<rbrakk> \<Longrightarrow> R S S'" for R
   2.616 +            using that by (metis (no_types, lifting) Un_iff)
   2.617 +          show ?thesis
   2.618 +          proof (rule symmy)
   2.619 +            show "Y \<inter> X face_of Y \<and> Y \<inter> X face_of X"
   2.620 +              if "X \<inter> Y face_of X \<and> X \<inter> Y face_of Y" for X Y :: "'a set"
   2.621 +              by (simp add: inf_commute that)
   2.622 +          next
   2.623 +            show "X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
   2.624 +              if "X \<in> \<U>" and "Y \<in> \<U>" for X Y
   2.625 +              by (simp add: faceI\<U> that)
   2.626 +          next
   2.627 +            show "X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
   2.628 +              if XY: "X \<in> \<U>" "Y \<in> ?\<T>" for X Y
   2.629 +            proof -
   2.630 +              obtain C K
   2.631 +                where "C \<in> \<N>" "K \<in> \<U>" "K \<subseteq> rel_frontier C"
   2.632 +                and Y: "Y = convex hull insert (@z. z \<in> rel_interior C) K"
   2.633 +                using XY by blast
   2.634 +              have "convex C"
   2.635 +                by (simp add: \<open>C \<in> \<N>\<close> convex\<N>)
   2.636 +              have "K \<subseteq> C"
   2.637 +                by (metis DiffE \<open>C \<in> \<N>\<close> \<open>K \<subseteq> rel_frontier C\<close> closed\<N> closure_closed rel_frontier_def subset_iff)
   2.638 +              let ?z = "(@z. z \<in> rel_interior C)"
   2.639 +              have z: "?z \<in> rel_interior C"
   2.640 +                using \<open>C \<in> \<N>\<close> in_rel_interior by blast
   2.641 +              obtain D where "D \<in> \<S>" "X \<subseteq> D"
   2.642 +                using C\<U> \<open>X \<in> \<U>\<close> by blast
   2.643 +              have "D \<inter> rel_interior C = (C \<inter> D) \<inter> rel_interior C"
   2.644 +                using rel_interior_subset by blast
   2.645 +              also have "(C \<inter> D) \<inter> rel_interior C = {}"
   2.646 +              proof (rule face_of_disjoint_rel_interior)
   2.647 +                show "C \<inter> D face_of C"
   2.648 +                  using \<N>_def \<S>_def \<open>C \<in> \<N>\<close> \<open>D \<in> \<S>\<close> intface\<M> by blast
   2.649 +                show "C \<inter> D \<noteq> C"
   2.650 +                  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)
   2.651 +              qed
   2.652 +              finally have DC: "D \<inter> rel_interior C = {}" .
   2.653 +              have eq: "X \<inter> convex hull (insert ?z K) = X \<inter> convex hull K"
   2.654 +                apply (rule Int_convex_hull_insert_rel_exterior [OF \<open>convex C\<close> \<open>K \<subseteq> C\<close> z])
   2.655 +                using DC by (meson \<open>X \<subseteq> D\<close> disjnt_def disjnt_subset1)
   2.656 +              obtain I where I: "\<not> affine_dependent I"
   2.657 +                         and Keq: "K = convex hull I" and [simp]: "convex hull K = K"
   2.658 +                using "*" \<open>K \<in> \<U>\<close> by force
   2.659 +              then have "?z \<notin> affine hull I"
   2.660 +                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
   2.661 +              have "X \<inter> K face_of K"
   2.662 +                by (simp add: \<open>K \<in> \<U>\<close> faceI\<U> \<open>X \<in> \<U>\<close>)
   2.663 +              also have "... face_of convex hull insert ?z K"
   2.664 +                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)
   2.665 +              finally have "X \<inter> K face_of convex hull insert ?z K" .
   2.666 +              then show ?thesis
   2.667 +                using "*" \<open>K \<in> \<U>\<close> faceI\<U> that(1) by (fastforce simp add: Y eq)
   2.668 +            qed
   2.669 +          next
   2.670 +            show "X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
   2.671 +              if XY: "X \<in> ?\<T>" "Y \<in> ?\<T>" for X Y
   2.672 +            proof -
   2.673 +              obtain C K D L
   2.674 +                where "C \<in> \<N>" "K \<in> \<U>" "K \<subseteq> rel_frontier C"
   2.675 +                and X: "X = convex hull insert (@z. z \<in> rel_interior C) K"
   2.676 +                and "D \<in> \<N>" "L \<in> \<U>" "L \<subseteq> rel_frontier D"
   2.677 +                and Y: "Y = convex hull insert (@z. z \<in> rel_interior D) L"
   2.678 +                using XY by blast
   2.679 +              let ?z = "(@z. z \<in> rel_interior C)"
   2.680 +              have z: "?z \<in> rel_interior C"
   2.681 +                using \<open>C \<in> \<N>\<close> in_rel_interior by blast
   2.682 +              have "convex C"
   2.683 +                by (simp add: \<open>C \<in> \<N>\<close> convex\<N>)
   2.684 +              have "convex K"
   2.685 +                using "*" \<open>K \<in> \<U>\<close> by blast
   2.686 +              have "convex L"
   2.687 +                by (meson \<open>L \<in> \<U>\<close> convex_simplex simpl\<U>)
   2.688 +              show ?thesis
   2.689 +              proof (cases "D=C")
   2.690 +                case True
   2.691 +                then have "L \<subseteq> rel_frontier C"
   2.692 +                  using \<open>L \<subseteq> rel_frontier D\<close> by auto
   2.693 +                show ?thesis
   2.694 +                  apply (simp add: X Y True)
   2.695 +                  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>)
   2.696 +                  using face_of_polytope_insert2
   2.697 +                  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)
   2.698 +              next
   2.699 +                case False
   2.700 +                have "convex D"
   2.701 +                  by (simp add: \<open>D \<in> \<N>\<close> convex\<N>)
   2.702 +                have "K \<subseteq> C"
   2.703 +                  by (metis DiffE \<open>C \<in> \<N>\<close> \<open>K \<subseteq> rel_frontier C\<close> closed\<N> closure_closed rel_frontier_def subset_eq)
   2.704 +                have "L \<subseteq> D"
   2.705 +                  by (metis DiffE \<open>D \<in> \<N>\<close> \<open>L \<subseteq> rel_frontier D\<close> closed\<N> closure_closed rel_frontier_def subset_eq)
   2.706 +                let ?w = "(@w. w \<in> rel_interior D)"
   2.707 +                have w: "?w \<in> rel_interior D"
   2.708 +                  using \<open>D \<in> \<N>\<close> in_rel_interior by blast
   2.709 +                have "C \<inter> rel_interior D = (D \<inter> C) \<inter> rel_interior D"
   2.710 +                  using rel_interior_subset by blast
   2.711 +                also have "(D \<inter> C) \<inter> rel_interior D = {}"
   2.712 +                proof (rule face_of_disjoint_rel_interior)
   2.713 +                  show "D \<inter> C face_of D"
   2.714 +                    using \<N>_def \<open>C \<in> \<N>\<close> \<open>D \<in> \<N>\<close> intface\<M> by blast
   2.715 +                  have "D \<in> \<M> \<and> aff_dim D = int n"
   2.716 +                    using \<N>_def \<open>D \<in> \<N>\<close> by blast
   2.717 +                  moreover have "C \<in> \<M> \<and> aff_dim C = int n"
   2.718 +                    using \<N>_def \<open>C \<in> \<N>\<close> by blast
   2.719 +                  ultimately show "D \<inter> C \<noteq> D"
   2.720 +                    by (metis False face_of_aff_dim_lt inf.idem inf_le1 intface\<M> not_le poly\<M> polytope_imp_convex)
   2.721 +                qed
   2.722 +                finally have CD: "C \<inter> (rel_interior D) = {}" .
   2.723 +                have zKC: "(convex hull insert ?z K) \<subseteq> C"
   2.724 +                  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)
   2.725 +                have eq: "convex hull (insert ?z K) \<inter> convex hull (insert ?w L) =
   2.726 +                          convex hull (insert ?z K) \<inter> convex hull L"
   2.727 +                  apply (rule Int_convex_hull_insert_rel_exterior [OF \<open>convex D\<close> \<open>L \<subseteq> D\<close> w])
   2.728 +                  using zKC CD apply (force simp: disjnt_def)
   2.729 +                  done
   2.730 +                have ch_id: "convex hull K = K" "convex hull L = L"
   2.731 +                  using "*" \<open>K \<in> \<U>\<close> \<open>L \<in> \<U>\<close> hull_same by auto
   2.732 +                have "convex C"
   2.733 +                  by (simp add: \<open>C \<in> \<N>\<close> convex\<N>)
   2.734 +                have "convex hull (insert ?z K) \<inter> L = L \<inter> convex hull (insert ?z K)"
   2.735 +                  by blast
   2.736 +                also have "... = convex hull K \<inter> L"
   2.737 +                proof (subst Int_convex_hull_insert_rel_exterior [OF \<open>convex C\<close> \<open>K \<subseteq> C\<close> z])
   2.738 +                  have "(C \<inter> D) \<inter> rel_interior C = {}"
   2.739 +                  proof (rule face_of_disjoint_rel_interior)
   2.740 +                    show "C \<inter> D face_of C"
   2.741 +                      using \<N>_def \<open>C \<in> \<N>\<close> \<open>D \<in> \<N>\<close> intface\<M> by blast
   2.742 +                    have "D \<in> \<M>" "aff_dim D = int n"
   2.743 +                      using \<N>_def \<open>D \<in> \<N>\<close> by fastforce+
   2.744 +                    moreover have "C \<in> \<M>" "aff_dim C = int n"
   2.745 +                      using \<N>_def \<open>C \<in> \<N>\<close> by fastforce+
   2.746 +                    ultimately have "aff_dim D + - 1 * aff_dim C \<le> 0"
   2.747 +                      by fastforce
   2.748 +                    then have "\<not> C face_of D"
   2.749 +                      using False \<open>convex D\<close> face_of_aff_dim_lt by fastforce
   2.750 +                    show "C \<inter> D \<noteq> C"
   2.751 +                      using \<open>C \<in> \<M>\<close> \<open>D \<in> \<M>\<close> \<open>\<not> C face_of D\<close> intface\<M> by fastforce
   2.752 +                  qed
   2.753 +                  then have "D \<inter> rel_interior C = {}"
   2.754 +                    by (metis inf.absorb_iff2 inf_assoc inf_sup_aci(1) rel_interior_subset)
   2.755 +                  then show "disjnt L (rel_interior C)"
   2.756 +                    by (meson \<open>L \<subseteq> D\<close> disjnt_def disjnt_subset1)
   2.757 +                next
   2.758 +                  show "L \<inter> convex hull K = convex hull K \<inter> L"
   2.759 +                    by force
   2.760 +                qed
   2.761 +                finally have chKL: "convex hull (insert ?z K) \<inter> L = convex hull K \<inter> L" .
   2.762 +                have "convex hull insert ?z K \<inter> convex hull L face_of K"
   2.763 +                  by (simp add: \<open>K \<in> \<U>\<close> \<open>L \<in> \<U>\<close> ch_id chKL faceI\<U>)
   2.764 +                also have "... face_of convex hull insert ?z K"
   2.765 +                proof -
   2.766 +                  obtain I where I: "\<not> affine_dependent I" "K = convex hull I"
   2.767 +                    using * [OF \<open>K \<in> \<U>\<close>] by auto
   2.768 +                  then have "\<And>a. a \<notin> rel_interior C \<or> a \<notin> affine hull I"
   2.769 +                    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
   2.770 +                  then show ?thesis
   2.771 +                    by (metis I affine_independent_insert face_of_convex_hull_affine_independent hull_insert subset_insertI z)
   2.772 +                qed
   2.773 +                finally have 1: "convex hull insert ?z K \<inter> convex hull L face_of convex hull insert ?z K" .
   2.774 +                have "convex hull insert ?z K \<inter> convex hull L face_of L"
   2.775 +                  by (simp add: \<open>K \<in> \<U>\<close> \<open>L \<in> \<U>\<close> ch_id chKL faceI\<U>)
   2.776 +                also have "... face_of convex hull insert ?w L"
   2.777 +                proof -
   2.778 +                  obtain I where I: "\<not> affine_dependent I" "L = convex hull I"
   2.779 +                    using * [OF \<open>L \<in> \<U>\<close>] by auto
   2.780 +                  then have "\<And>a. a \<notin> rel_interior D \<or> a \<notin> affine hull I"
   2.781 +                    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
   2.782 +                  then show ?thesis
   2.783 +                    by (metis I aff_independent_finite convex_convex_hull face_of_convex_hull_insert face_of_refl hull_insert w)
   2.784 +                qed
   2.785 +                finally have 2: "convex hull insert ?z K \<inter> convex hull L face_of convex hull insert ?w L" .
   2.786 +                show ?thesis
   2.787 +                  by (simp add: X Y eq 1 2)
   2.788 +              qed
   2.789 +            qed
   2.790 +          qed
   2.791 +        qed
   2.792 +        then
   2.793 +        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'
   2.794 +          using that by auto
   2.795 +      qed
   2.796 +      show "\<exists>F \<subseteq> \<U> \<union> ?\<T>. C = \<Union>F" if "C \<in> \<M>" for C
   2.797 +      proof (cases "C \<in> \<S>")
   2.798 +        case True
   2.799 +        then show ?thesis
   2.800 +          by (meson UnCI fin\<U> subsetD subsetI)
   2.801 +      next
   2.802 +        case False
   2.803 +        then have "C \<in> \<N>"
   2.804 +          by (simp add: \<N>_def \<S>_def aff\<M> less_le that)
   2.805 +        let ?z = "@z. z \<in> rel_interior C"
   2.806 +        have z: "?z \<in> rel_interior C"
   2.807 +          using \<open>C \<in> \<N>\<close> in_rel_interior by blast
   2.808 +        let ?F = "\<Union>K \<in> \<U> \<inter> Pow (rel_frontier C). {convex hull (insert ?z K)}"
   2.809 +        have "?F \<subseteq> ?\<T>"
   2.810 +          using \<open>C \<in> \<N>\<close> by blast
   2.811 +        moreover have "C \<subseteq> \<Union>?F"
   2.812 +        proof
   2.813 +          fix x
   2.814 +          assume "x \<in> C"
   2.815 +          have "convex C"
   2.816 +            using \<open>C \<in> \<N>\<close> convex\<N> by blast
   2.817 +          have "bounded C"
   2.818 +            using \<open>C \<in> \<N>\<close> by (simp add: poly\<M> polytope_imp_bounded that)
   2.819 +          have "polytope C"
   2.820 +            using \<open>C \<in> \<N>\<close> poly\<N> by auto
   2.821 +          have "\<not> (?z = x \<and> C = {?z})"
   2.822 +            using \<open>C \<in> \<N>\<close> aff_dim_sing [of ?z] \<open>\<not> n \<le> 1\<close> by (force simp: \<N>_def)
   2.823 +          then obtain y where y: "y \<in> rel_frontier C" and xzy: "x \<in> closed_segment ?z y"
   2.824 +            and sub: "open_segment ?z y \<subseteq> rel_interior C"
   2.825 +            by (blast intro: segment_to_rel_frontier [OF \<open>convex C\<close> \<open>bounded C\<close> z \<open>x \<in> C\<close>])
   2.826 +          then obtain F where "y \<in> F" "F face_of C" "F \<noteq> C"
   2.827 +            by (auto simp: rel_frontier_of_polyhedron_alt [OF polytope_imp_polyhedron [OF \<open>polytope C\<close>]])
   2.828 +          then obtain \<G> where "finite \<G>" "\<G> \<subseteq> \<U>" "F = \<Union>\<G>"
   2.829 +            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)
   2.830 +          then obtain K where "y \<in> K" "K \<in> \<G>"
   2.831 +            using \<open>y \<in> F\<close> by blast
   2.832 +          moreover have x: "x \<in> convex hull {?z,y}"
   2.833 +            using segment_convex_hull xzy by auto
   2.834 +          moreover have "convex hull {?z,y} \<subseteq> convex hull insert ?z K"
   2.835 +            by (metis (full_types) \<open>y \<in> K\<close> hull_mono empty_subsetI insertCI insert_subset)
   2.836 +          moreover have "K \<in> \<U>"
   2.837 +            using \<open>K \<in> \<G>\<close> \<open>\<G> \<subseteq> \<U>\<close> by blast
   2.838 +          moreover have "K \<subseteq> rel_frontier C"
   2.839 +            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
   2.840 +          ultimately show "x \<in> \<Union>?F"
   2.841 +            by force
   2.842 +        qed
   2.843 +        moreover
   2.844 +        have "convex hull insert (SOME z. z \<in> rel_interior C) K \<subseteq> C"
   2.845 +          if "K \<in> \<U>" "K \<subseteq> rel_frontier C" for K
   2.846 +        proof (rule hull_minimal)
   2.847 +          show "insert (SOME z. z \<in> rel_interior C) K \<subseteq> C"
   2.848 +            using that \<open>C \<in> \<N>\<close> in_rel_interior rel_interior_subset
   2.849 +            by (force simp: closure_eq rel_frontier_def closed\<N>)
   2.850 +          show "convex C"
   2.851 +            by (simp add: \<open>C \<in> \<N>\<close> convex\<N>)
   2.852 +        qed
   2.853 +        then have "\<Union>?F \<subseteq> C"
   2.854 +          by auto
   2.855 +        ultimately show ?thesis
   2.856 +          by blast
   2.857 +      qed
   2.858 +
   2.859 +      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
   2.860 +        using that
   2.861 +      proof
   2.862 +        assume "L \<in> \<U>"
   2.863 +        then show ?thesis
   2.864 +          using C\<U> \<S>_def "*" by fastforce
   2.865 +      next
   2.866 +        assume "L \<in> ?\<T>"
   2.867 +        then obtain C K where "C \<in> \<N>"
   2.868 +          and L: "L = convex hull insert (@z. z \<in> rel_interior C) K"
   2.869 +          and K: "K \<in> \<U>" "K \<subseteq> rel_frontier C"
   2.870 +          by auto
   2.871 +        then have "convex hull C = C"
   2.872 +          by (meson convex\<N> convex_hull_eq)
   2.873 +        then have "convex C"
   2.874 +          by (metis (no_types) convex_convex_hull)
   2.875 +        have "rel_frontier C \<subseteq> C"
   2.876 +          by (metis DiffE closed\<N> \<open>C \<in> \<N>\<close> closure_closed rel_frontier_def subsetI)
   2.877 +        have "K \<subseteq> C"
   2.878 +          using K \<open>rel_frontier C \<subseteq> C\<close> by blast
   2.879 +        have "C \<in> \<M>"
   2.880 +          using \<N>_def \<open>C \<in> \<N>\<close> by auto
   2.881 +        moreover have "L \<subseteq> C"
   2.882 +          using K L \<open>C \<in> \<N>\<close>
   2.883 +          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)
   2.884 +        ultimately show ?thesis
   2.885 +          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
   2.886 +      qed
   2.887 +      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
   2.888 +        using that by auto
   2.889 +    qed
   2.890 +    then show ?thesis
   2.891 +      apply (rule ex_forward, safe)
   2.892 +        apply (meson Union_iff subsetCE, fastforce)
   2.893 +      by (meson infinite_super simplicial_complex_def)
   2.894 +  qed
   2.895 +qed
   2.896 +
   2.897 +
   2.898 +lemma simplicial_subdivision_of_cell_complex_lowdim:
   2.899 +  assumes "finite \<M>"
   2.900 +      and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
   2.901 +      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"
   2.902 +      and aff: "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C \<le> d"
   2.903 +  obtains \<T> where "simplicial_complex \<T>" "\<And>K. K \<in> \<T> \<Longrightarrow> aff_dim K \<le> d"
   2.904 +                  "\<Union>\<T> = \<Union>\<M>"
   2.905 +                  "\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F"
   2.906 +                  "\<And>K. K \<in> \<T> \<Longrightarrow> \<exists>C. C \<in> \<M> \<and> K \<subseteq> C"
   2.907 +proof (cases "d \<ge> 0")
   2.908 +  case True
   2.909 +  then obtain n where n: "d = of_nat n"
   2.910 +    using zero_le_imp_eq_int by blast
   2.911 +  have "\<exists>\<T>. simplicial_complex \<T> \<and>
   2.912 +            (\<forall>K\<in>\<T>. aff_dim K \<le> int n) \<and>
   2.913 +            \<Union>\<T> = \<Union>(\<Union>C\<in>\<M>. {F. F face_of C}) \<and>
   2.914 +            (\<forall>C\<in>\<Union>C\<in>\<M>. {F. F face_of C}.
   2.915 +                \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F) \<and>
   2.916 +            (\<forall>K\<in>\<T>. \<exists>C. C \<in> (\<Union>C\<in>\<M>. {F. F face_of C}) \<and> K \<subseteq> C)"
   2.917 +  proof (rule simplicial_subdivision_aux)
   2.918 +    show "finite (\<Union>C\<in>\<M>. {F. F face_of C})"
   2.919 +      using \<open>finite \<M>\<close> poly polyhedron_eq_finite_faces polytope_imp_polyhedron by fastforce
   2.920 +    show "polytope F" if "F \<in> (\<Union>C\<in>\<M>. {F. F face_of C})" for F
   2.921 +      using poly that face_of_polytope_polytope by blast
   2.922 +    show "aff_dim F \<le> int n" if "F \<in> (\<Union>C\<in>\<M>. {F. F face_of C})" for F
   2.923 +      using that
   2.924 +      by clarify (metis n aff_dim_subset aff face_of_imp_subset order_trans)
   2.925 +    show "F \<in> (\<Union>C\<in>\<M>. {F. F face_of C})"
   2.926 +      if "G \<in> (\<Union>C\<in>\<M>. {F. F face_of C})" and "F face_of G" for F G
   2.927 +      using that face_of_trans by blast
   2.928 +  next
   2.929 +    show "F1 \<inter> F2 face_of F1 \<and> F1 \<inter> F2 face_of F2"
   2.930 +      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
   2.931 +      using that
   2.932 +      by safe (meson face face_of_Int_subface)+
   2.933 +  qed
   2.934 +  moreover
   2.935 +  have "\<Union>(\<Union>C\<in>\<M>. {F. F face_of C}) = \<Union>\<M>"
   2.936 +    using face_of_imp_subset face by blast
   2.937 +  ultimately show ?thesis
   2.938 +    apply clarify
   2.939 +    apply (rule that, assumption+)
   2.940 +       using n apply blast
   2.941 +      apply (simp_all add: poly face_of_refl polytope_imp_convex)
   2.942 +    using face_of_imp_subset by fastforce
   2.943 +next
   2.944 +  case False
   2.945 +  then have m1: "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C = -1"
   2.946 +    by (metis aff aff_dim_empty_eq aff_dim_negative_iff dual_order.trans not_less)
   2.947 +  then have face\<M>: "\<And>F S. \<lbrakk>S \<in> \<M>; F face_of S\<rbrakk> \<Longrightarrow> F \<in> \<M>"
   2.948 +    by (metis aff_dim_empty face_of_empty)
   2.949 +  show ?thesis
   2.950 +  proof
   2.951 +    have "\<And>S. S \<in> \<M> \<Longrightarrow> \<exists>n. n simplex S"
   2.952 +      by (metis (no_types) m1 aff_dim_empty simplex_minus_1)
   2.953 +    then show "simplicial_complex \<M>"
   2.954 +      by (auto simp: simplicial_complex_def \<open>finite \<M>\<close> face intro: face\<M>)
   2.955 +    show "aff_dim K \<le> d" if "K \<in> \<M>" for K
   2.956 +      by (simp add: that aff)
   2.957 +    show "\<exists>F. finite F \<and> F \<subseteq> \<M> \<and> C = \<Union>F" if "C \<in> \<M>" for C
   2.958 +      using \<open>C \<in> \<M>\<close> equals0I by auto
   2.959 +    show "\<exists>C. C \<in> \<M> \<and> K \<subseteq> C" if "K \<in> \<M>" for K
   2.960 +      using \<open>K \<in> \<M>\<close> by blast
   2.961 +  qed auto
   2.962 +qed
   2.963 +
   2.964 +proposition simplicial_subdivision_of_cell_complex:
   2.965 +  assumes "finite \<M>"
   2.966 +      and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
   2.967 +      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"
   2.968 +  obtains \<T> where "simplicial_complex \<T>"
   2.969 +                  "\<Union>\<T> = \<Union>\<M>"
   2.970 +                  "\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F"
   2.971 +                  "\<And>K. K \<in> \<T> \<Longrightarrow> \<exists>C. C \<in> \<M> \<and> K \<subseteq> C"
   2.972 +  by (blast intro: simplicial_subdivision_of_cell_complex_lowdim [OF assms aff_dim_le_DIM])
   2.973 +
   2.974 +corollary fine_simplicial_subdivision_of_cell_complex:
   2.975 +  assumes "0 < e" "finite \<M>"
   2.976 +      and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
   2.977 +      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"
   2.978 +  obtains \<T> where "simplicial_complex \<T>"
   2.979 +                  "\<And>K. K \<in> \<T> \<Longrightarrow> diameter K < e"
   2.980 +                  "\<Union>\<T> = \<Union>\<M>"
   2.981 +                  "\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F"
   2.982 +                  "\<And>K. K \<in> \<T> \<Longrightarrow> \<exists>C. C \<in> \<M> \<and> K \<subseteq> C"
   2.983 +proof -
   2.984 +  obtain \<N> where \<N>: "finite \<N>" "\<Union>\<N> = \<Union>\<M>" 
   2.985 +              and diapoly: "\<And>X. X \<in> \<N> \<Longrightarrow> diameter X < e" "\<And>X. X \<in> \<N> \<Longrightarrow> polytope X"
   2.986 +               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"
   2.987 +               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"
   2.988 +               and \<N>covered: "\<And>C. C \<in> \<N> \<Longrightarrow> \<exists>D. D \<in> \<M> \<and> C \<subseteq> D"
   2.989 +    by (blast intro: cell_complex_subdivision_exists [OF \<open>0 < e\<close> \<open>finite \<M>\<close> poly aff_dim_le_DIM face])
   2.990 +  then obtain \<T> where \<T>: "simplicial_complex \<T>" "\<Union>\<T> = \<Union>\<N>"
   2.991 +                   and \<T>covers: "\<And>C. C \<in> \<N> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F"
   2.992 +                   and \<T>covered: "\<And>K. K \<in> \<T> \<Longrightarrow> \<exists>C. C \<in> \<N> \<and> K \<subseteq> C"
   2.993 +    using simplicial_subdivision_of_cell_complex [OF \<open>finite \<N>\<close>] by metis
   2.994 +  show ?thesis
   2.995 +  proof
   2.996 +    show "simplicial_complex \<T>"
   2.997 +      by (rule \<T>)
   2.998 +    show "diameter K < e" if "K \<in> \<T>" for K
   2.999 +      by (metis le_less_trans diapoly \<T>covered diameter_subset polytope_imp_bounded that)
  2.1000 +    show "\<Union>\<T> = \<Union>\<M>"
  2.1001 +      by (simp add: \<N>(2) \<open>\<Union>\<T> = \<Union>\<N>\<close>)
  2.1002 +    show "\<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F" if "C \<in> \<M>" for C
  2.1003 +    proof -
  2.1004 +      { fix x
  2.1005 +        assume "x \<in> C"
  2.1006 +        then obtain D where "D \<in> \<T>" "x \<in> D" "D \<subseteq> C"
  2.1007 +          using \<N>covers \<open>C \<in> \<M>\<close> \<T>covers by force
  2.1008 +        then have "\<exists>X\<in>\<T> \<inter> Pow C. x \<in> X"
  2.1009 +          using \<open>D \<in> \<T>\<close> \<open>D \<subseteq> C\<close> \<open>x \<in> D\<close> by blast
  2.1010 +      }
  2.1011 +      moreover
  2.1012 +      have "finite (\<T> \<inter> Pow C)"
  2.1013 +        using \<open>simplicial_complex \<T>\<close> simplicial_complex_def by auto
  2.1014 +      ultimately show ?thesis
  2.1015 +        by (rule_tac x="(\<T> \<inter> Pow C)" in exI) auto
  2.1016 +    qed
  2.1017 +    show "\<exists>C. C \<in> \<M> \<and> K \<subseteq> C" if "K \<in> \<T>" for K
  2.1018 +      by (meson \<N>covered \<T>covered order_trans that)
  2.1019 +  qed
  2.1020 +qed
  2.1021 +
  2.1022  end
     3.1 --- a/src/HOL/Analysis/Starlike.thy	Wed Jul 26 16:07:45 2017 +0100
     3.2 +++ b/src/HOL/Analysis/Starlike.thy	Thu Jul 27 15:22:35 2017 +0100
     3.3 @@ -5837,11 +5837,41 @@
     3.4    show ?thesis using S
     3.5      apply (simp add: hull_redundant cong: aff_dim_affine_hull2)
     3.6      apply (simp add: affine_hull_insert_span_gen hull_inc)
     3.7 -    apply (simp add: insert_commute [of a] hull_inc aff_dim_eq_dim [of x] dim_insert span_0)
     3.8 +    apply (simp add: insert_commute [of a] hull_inc aff_dim_eq_dim [of x] dim_insert)
     3.9      apply (metis (no_types, lifting) add_minus_cancel image_iff uminus_add_conv_diff)
    3.10      done
    3.11  qed
    3.12  
    3.13 +lemma affine_dependent_choose:
    3.14 +  fixes a :: "'a :: euclidean_space"
    3.15 +  assumes "~(affine_dependent S)"
    3.16 +  shows "affine_dependent(insert a S) \<longleftrightarrow> a \<notin> S \<and> a \<in> affine hull S"
    3.17 +        (is "?lhs = ?rhs")
    3.18 +proof safe
    3.19 +  assume "affine_dependent (insert a S)" and "a \<in> S"
    3.20 +  then show "False"
    3.21 +    using \<open>a \<in> S\<close> assms insert_absorb by fastforce
    3.22 +next
    3.23 +  assume lhs: "affine_dependent (insert a S)"
    3.24 +  then have "a \<notin> S"
    3.25 +    by (metis (no_types) assms insert_absorb)
    3.26 +  moreover have "finite S"
    3.27 +    using affine_independent_iff_card assms by blast
    3.28 +  moreover have "aff_dim (insert a S) \<noteq> int (card S)"
    3.29 +    using \<open>finite S\<close> affine_independent_iff_card \<open>a \<notin> S\<close> lhs by fastforce
    3.30 +  ultimately show "a \<in> affine hull S"
    3.31 +    by (metis aff_dim_affine_independent aff_dim_insert assms)
    3.32 +next
    3.33 +  assume "a \<notin> S" and "a \<in> affine hull S"
    3.34 +  show "affine_dependent (insert a S)"
    3.35 +    by (simp add: \<open>a \<in> affine hull S\<close> \<open>a \<notin> S\<close> affine_dependent_def)
    3.36 +qed
    3.37 +
    3.38 +lemma affine_independent_insert:
    3.39 +  fixes a :: "'a :: euclidean_space"
    3.40 +  shows "\<lbrakk>~(affine_dependent S); a \<notin> affine hull S\<rbrakk> \<Longrightarrow> ~(affine_dependent(insert a S))"
    3.41 +  by (simp add: affine_dependent_choose)
    3.42 +
    3.43  lemma subspace_bounded_eq_trivial:
    3.44    fixes S :: "'a::real_normed_vector set"
    3.45    assumes "subspace S"