author paulson Thu Jul 27 15:22:35 2017 +0100 (24 months ago) changeset 66297 d425bdf419f5 parent 66296 33a47f2d9edc child 66298 5ff9fe3fee66
polytopes: simplical subdivisions, etc.
 src/HOL/Analysis/Linear_Algebra.thy file | annotate | diff | revisions src/HOL/Analysis/Polytope.thy file | annotate | diff | revisions src/HOL/Analysis/Starlike.thy file | annotate | diff | revisions
```     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.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.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"
```