src/HOL/Analysis/Polytope.thy
author Manuel Eberl <eberlm@in.tum.de>
Mon Mar 12 20:52:53 2018 +0100 (17 months ago)
changeset 67829 2a6ef5ba4822
parent 67613 ce654b0e6d69
child 67831 07f5588f2735
permissions -rw-r--r--
Changes to complete distributive lattices due to Viorel Preoteasa
     1 section \<open>Faces, Extreme Points, Polytopes, Polyhedra etc.\<close>
     2 
     3 text\<open>Ported from HOL Light by L C Paulson\<close>
     4 
     5 theory Polytope
     6 imports Cartesian_Euclidean_Space
     7 begin
     8 
     9 subsection \<open>Faces of a (usually convex) set\<close>
    10 
    11 definition face_of :: "['a::real_vector set, 'a set] \<Rightarrow> bool" (infixr "(face'_of)" 50)
    12   where
    13   "T face_of S \<longleftrightarrow>
    14         T \<subseteq> S \<and> convex T \<and>
    15         (\<forall>a \<in> S. \<forall>b \<in> S. \<forall>x \<in> T. x \<in> open_segment a b \<longrightarrow> a \<in> T \<and> b \<in> T)"
    16 
    17 lemma face_ofD: "\<lbrakk>T face_of S; x \<in> open_segment a b; a \<in> S; b \<in> S; x \<in> T\<rbrakk> \<Longrightarrow> a \<in> T \<and> b \<in> T"
    18   unfolding face_of_def by blast
    19 
    20 lemma face_of_translation_eq [simp]:
    21     "((+) a ` T face_of (+) a ` S) \<longleftrightarrow> T face_of S"
    22 proof -
    23   have *: "\<And>a T S. T face_of S \<Longrightarrow> ((+) a ` T face_of (+) a ` S)"
    24     apply (simp add: face_of_def Ball_def, clarify)
    25     apply (drule open_segment_translation_eq [THEN iffD1])
    26     using inj_image_mem_iff inj_add_left apply metis
    27     done
    28   show ?thesis
    29     apply (rule iffI)
    30     apply (force simp: image_comp o_def dest: * [where a = "-a"])
    31     apply (blast intro: *)
    32     done
    33 qed
    34 
    35 lemma face_of_linear_image:
    36   assumes "linear f" "inj f"
    37     shows "(f ` c face_of f ` S) \<longleftrightarrow> c face_of S"
    38 by (simp add: face_of_def inj_image_subset_iff inj_image_mem_iff open_segment_linear_image assms)
    39 
    40 lemma face_of_refl: "convex S \<Longrightarrow> S face_of S"
    41   by (auto simp: face_of_def)
    42 
    43 lemma face_of_refl_eq: "S face_of S \<longleftrightarrow> convex S"
    44   by (auto simp: face_of_def)
    45 
    46 lemma empty_face_of [iff]: "{} face_of S"
    47   by (simp add: face_of_def)
    48 
    49 lemma face_of_empty [simp]: "S face_of {} \<longleftrightarrow> S = {}"
    50   by (meson empty_face_of face_of_def subset_empty)
    51 
    52 lemma face_of_trans [trans]: "\<lbrakk>S face_of T; T face_of u\<rbrakk> \<Longrightarrow> S face_of u"
    53   unfolding face_of_def by (safe; blast)
    54 
    55 lemma face_of_face: "T face_of S \<Longrightarrow> (f face_of T \<longleftrightarrow> f face_of S \<and> f \<subseteq> T)"
    56   unfolding face_of_def by (safe; blast)
    57 
    58 lemma face_of_subset: "\<lbrakk>F face_of S; F \<subseteq> T; T \<subseteq> S\<rbrakk> \<Longrightarrow> F face_of T"
    59   unfolding face_of_def by (safe; blast)
    60 
    61 lemma face_of_slice: "\<lbrakk>F face_of S; convex T\<rbrakk> \<Longrightarrow> (F \<inter> T) face_of (S \<inter> T)"
    62   unfolding face_of_def by (blast intro: convex_Int)
    63 
    64 lemma face_of_Int: "\<lbrakk>t1 face_of S; t2 face_of S\<rbrakk> \<Longrightarrow> (t1 \<inter> t2) face_of S"
    65   unfolding face_of_def by (blast intro: convex_Int)
    66 
    67 lemma face_of_Inter: "\<lbrakk>A \<noteq> {}; \<And>T. T \<in> A \<Longrightarrow> T face_of S\<rbrakk> \<Longrightarrow> (\<Inter> A) face_of S"
    68   unfolding face_of_def by (blast intro: convex_Inter)
    69 
    70 lemma face_of_Int_Int: "\<lbrakk>F face_of T; F' face_of t'\<rbrakk> \<Longrightarrow> (F \<inter> F') face_of (T \<inter> t')"
    71   unfolding face_of_def by (blast intro: convex_Int)
    72 
    73 lemma face_of_imp_subset: "T face_of S \<Longrightarrow> T \<subseteq> S"
    74   unfolding face_of_def by blast
    75 
    76 lemma face_of_imp_eq_affine_Int:
    77   fixes S :: "'a::euclidean_space set"
    78   assumes S: "convex S"  and T: "T face_of S"
    79   shows "T = (affine hull T) \<inter> S"
    80 proof -
    81   have "convex T" using T by (simp add: face_of_def)
    82   have *: False if x: "x \<in> affine hull T" and "x \<in> S" "x \<notin> T" and y: "y \<in> rel_interior T" for x y
    83   proof -
    84     obtain e where "e>0" and e: "cball y e \<inter> affine hull T \<subseteq> T"
    85       using y by (auto simp: rel_interior_cball)
    86     have "y \<noteq> x" "y \<in> S" "y \<in> T"
    87       using face_of_imp_subset rel_interior_subset T that by blast+
    88     then have zne: "\<And>u. \<lbrakk>u \<in> {0<..<1}; (1 - u) *\<^sub>R y + u *\<^sub>R x \<in> T\<rbrakk> \<Longrightarrow>  False"
    89       using \<open>x \<in> S\<close> \<open>x \<notin> T\<close> \<open>T face_of S\<close> unfolding face_of_def
    90       apply clarify
    91       apply (drule_tac x=x in bspec, assumption)
    92       apply (drule_tac x=y in bspec, assumption)
    93       apply (subst (asm) open_segment_commute)
    94       apply (force simp: open_segment_image_interval image_def)
    95       done
    96     have in01: "min (1/2) (e / norm (x - y)) \<in> {0<..<1}"
    97       using \<open>y \<noteq> x\<close> \<open>e > 0\<close> by simp
    98     show ?thesis
    99       apply (rule zne [OF in01])
   100       apply (rule e [THEN subsetD])
   101       apply (rule IntI)
   102         using \<open>y \<noteq> x\<close> \<open>e > 0\<close>
   103         apply (simp add: cball_def dist_norm algebra_simps)
   104         apply (simp add: Real_Vector_Spaces.scaleR_diff_right [symmetric] norm_minus_commute min_mult_distrib_right)
   105       apply (rule mem_affine [OF affine_affine_hull _ x])
   106       using \<open>y \<in> T\<close>  apply (auto simp: hull_inc)
   107       done
   108   qed
   109   show ?thesis
   110     apply (rule subset_antisym)
   111     using assms apply (simp add: hull_subset face_of_imp_subset)
   112     apply (cases "T={}", simp)
   113     apply (force simp: rel_interior_eq_empty [symmetric] \<open>convex T\<close> intro: *)
   114     done
   115 qed
   116 
   117 lemma face_of_imp_closed:
   118      fixes S :: "'a::euclidean_space set"
   119      assumes "convex S" "closed S" "T face_of S" shows "closed T"
   120   by (metis affine_affine_hull affine_closed closed_Int face_of_imp_eq_affine_Int assms)
   121 
   122 lemma face_of_Int_supporting_hyperplane_le_strong:
   123     assumes "convex(S \<inter> {x. a \<bullet> x = b})" and aleb: "\<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b"
   124       shows "(S \<inter> {x. a \<bullet> x = b}) face_of S"
   125 proof -
   126   have *: "a \<bullet> u = a \<bullet> x" if "x \<in> open_segment u v" "u \<in> S" "v \<in> S" and b: "b = a \<bullet> x"
   127           for u v x
   128   proof (rule antisym)
   129     show "a \<bullet> u \<le> a \<bullet> x"
   130       using aleb \<open>u \<in> S\<close> \<open>b = a \<bullet> x\<close> by blast
   131   next
   132     obtain \<xi> where "b = a \<bullet> ((1 - \<xi>) *\<^sub>R u + \<xi> *\<^sub>R v)" "0 < \<xi>" "\<xi> < 1"
   133       using \<open>b = a \<bullet> x\<close> \<open>x \<in> open_segment u v\<close> in_segment
   134       by (auto simp: open_segment_image_interval split: if_split_asm)
   135     then have "b + \<xi> * (a \<bullet> u) \<le> a \<bullet> u + \<xi> * b"
   136       using aleb [OF \<open>v \<in> S\<close>] by (simp add: algebra_simps)
   137     then have "(1 - \<xi>) * b \<le> (1 - \<xi>) * (a \<bullet> u)"
   138       by (simp add: algebra_simps)
   139     then have "b \<le> a \<bullet> u"
   140       using \<open>\<xi> < 1\<close> by auto
   141     with b show "a \<bullet> x \<le> a \<bullet> u" by simp
   142   qed
   143   show ?thesis
   144     apply (simp add: face_of_def assms)
   145     using "*" open_segment_commute by blast
   146 qed
   147 
   148 lemma face_of_Int_supporting_hyperplane_ge_strong:
   149    "\<lbrakk>convex(S \<inter> {x. a \<bullet> x = b}); \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b\<rbrakk>
   150     \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) face_of S"
   151   using face_of_Int_supporting_hyperplane_le_strong [of S "-a" "-b"] by simp
   152 
   153 lemma face_of_Int_supporting_hyperplane_le:
   154     "\<lbrakk>convex S; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b\<rbrakk> \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) face_of S"
   155   by (simp add: convex_Int convex_hyperplane face_of_Int_supporting_hyperplane_le_strong)
   156 
   157 lemma face_of_Int_supporting_hyperplane_ge:
   158     "\<lbrakk>convex S; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b\<rbrakk> \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) face_of S"
   159   by (simp add: convex_Int convex_hyperplane face_of_Int_supporting_hyperplane_ge_strong)
   160 
   161 lemma face_of_imp_convex: "T face_of S \<Longrightarrow> convex T"
   162   using face_of_def by blast
   163 
   164 lemma face_of_imp_compact:
   165     fixes S :: "'a::euclidean_space set"
   166     shows "\<lbrakk>convex S; compact S; T face_of S\<rbrakk> \<Longrightarrow> compact T"
   167   by (meson bounded_subset compact_eq_bounded_closed face_of_imp_closed face_of_imp_subset)
   168 
   169 lemma face_of_Int_subface:
   170      "\<lbrakk>A \<inter> B face_of A; A \<inter> B face_of B; C face_of A; D face_of B\<rbrakk>
   171       \<Longrightarrow> (C \<inter> D) face_of C \<and> (C \<inter> D) face_of D"
   172   by (meson face_of_Int_Int face_of_face inf_le1 inf_le2)
   173 
   174 lemma subset_of_face_of:
   175     fixes S :: "'a::real_normed_vector set"
   176     assumes "T face_of S" "u \<subseteq> S" "T \<inter> (rel_interior u) \<noteq> {}"
   177       shows "u \<subseteq> T"
   178 proof
   179   fix c
   180   assume "c \<in> u"
   181   obtain b where "b \<in> T" "b \<in> rel_interior u" using assms by auto
   182   then obtain e where "e>0" "b \<in> u" and e: "cball b e \<inter> affine hull u \<subseteq> u"
   183     by (auto simp: rel_interior_cball)
   184   show "c \<in> T"
   185   proof (cases "b=c")
   186     case True with \<open>b \<in> T\<close> show ?thesis by blast
   187   next
   188     case False
   189     define d where "d = b + (e / norm(b - c)) *\<^sub>R (b - c)"
   190     have "d \<in> cball b e \<inter> affine hull u"
   191       using \<open>e > 0\<close> \<open>b \<in> u\<close> \<open>c \<in> u\<close>
   192       by (simp add: d_def dist_norm hull_inc mem_affine_3_minus False)
   193     with e have "d \<in> u" by blast
   194     have nbc: "norm (b - c) + e > 0" using \<open>e > 0\<close>
   195       by (metis add.commute le_less_trans less_add_same_cancel2 norm_ge_zero)
   196     then have [simp]: "d \<noteq> c" using False scaleR_cancel_left [of "1 + (e / norm (b - c))" b c]
   197       by (simp add: algebra_simps d_def) (simp add: divide_simps)
   198     have [simp]: "((e - e * e / (e + norm (b - c))) / norm (b - c)) = (e / (e + norm (b - c)))"
   199       using False nbc
   200       apply (simp add: algebra_simps divide_simps)
   201       by (metis mult_eq_0_iff norm_eq_zero norm_imp_pos_and_ge norm_pths(2) real_scaleR_def scaleR_left.add zero_less_norm_iff)
   202     have "b \<in> open_segment d c"
   203       apply (simp add: open_segment_image_interval)
   204       apply (simp add: d_def algebra_simps image_def)
   205       apply (rule_tac x="e / (e + norm (b - c))" in bexI)
   206       using False nbc \<open>0 < e\<close>
   207       apply (auto simp: algebra_simps)
   208       done
   209     then have "d \<in> T \<and> c \<in> T"
   210       apply (rule face_ofD [OF \<open>T face_of S\<close>])
   211       using \<open>d \<in> u\<close>  \<open>c \<in> u\<close> \<open>u \<subseteq> S\<close>  \<open>b \<in> T\<close>  apply auto
   212       done
   213     then show ?thesis ..
   214   qed
   215 qed
   216 
   217 lemma face_of_eq:
   218     fixes S :: "'a::real_normed_vector set"
   219     assumes "T face_of S" "u face_of S" "(rel_interior T) \<inter> (rel_interior u) \<noteq> {}"
   220       shows "T = u"
   221   apply (rule subset_antisym)
   222   apply (metis assms disjoint_iff_not_equal face_of_imp_subset rel_interior_subset subsetCE subset_of_face_of)
   223   by (metis assms disjoint_iff_not_equal face_of_imp_subset rel_interior_subset subset_iff subset_of_face_of)
   224 
   225 lemma face_of_disjoint_rel_interior:
   226       fixes S :: "'a::real_normed_vector set"
   227       assumes "T face_of S" "T \<noteq> S"
   228         shows "T \<inter> rel_interior S = {}"
   229   by (meson assms subset_of_face_of face_of_imp_subset order_refl subset_antisym)
   230 
   231 lemma face_of_disjoint_interior:
   232       fixes S :: "'a::real_normed_vector set"
   233       assumes "T face_of S" "T \<noteq> S"
   234         shows "T \<inter> interior S = {}"
   235 proof -
   236   have "T \<inter> interior S \<subseteq> rel_interior S"
   237     by (meson inf_sup_ord(2) interior_subset_rel_interior order.trans)
   238   thus ?thesis
   239     by (metis (no_types) Int_greatest assms face_of_disjoint_rel_interior inf_sup_ord(1) subset_empty)
   240 qed
   241 
   242 lemma face_of_subset_rel_boundary:
   243   fixes S :: "'a::real_normed_vector set"
   244   assumes "T face_of S" "T \<noteq> S"
   245     shows "T \<subseteq> (S - rel_interior S)"
   246 by (meson DiffI assms disjoint_iff_not_equal face_of_disjoint_rel_interior face_of_imp_subset rev_subsetD subsetI)
   247 
   248 lemma face_of_subset_rel_frontier:
   249     fixes S :: "'a::real_normed_vector set"
   250     assumes "T face_of S" "T \<noteq> S"
   251       shows "T \<subseteq> rel_frontier S"
   252   using assms closure_subset face_of_disjoint_rel_interior face_of_imp_subset rel_frontier_def by fastforce
   253 
   254 lemma face_of_aff_dim_lt:
   255   fixes S :: "'a::euclidean_space set"
   256   assumes "convex S" "T face_of S" "T \<noteq> S"
   257     shows "aff_dim T < aff_dim S"
   258 proof -
   259   have "aff_dim T \<le> aff_dim S"
   260     by (simp add: face_of_imp_subset aff_dim_subset assms)
   261   moreover have "aff_dim T \<noteq> aff_dim S"
   262   proof (cases "T = {}")
   263     case True then show ?thesis
   264       by (metis aff_dim_empty \<open>T \<noteq> S\<close>)
   265   next case False then show ?thesis
   266     by (metis Set.set_insert assms convex_rel_frontier_aff_dim dual_order.irrefl face_of_imp_convex face_of_subset_rel_frontier insert_not_empty subsetI)
   267   qed
   268   ultimately show ?thesis
   269     by simp
   270 qed
   271 
   272 lemma subset_of_face_of_affine_hull:
   273     fixes S :: "'a::euclidean_space set"
   274   assumes T: "T face_of S" and "convex S" "U \<subseteq> S" and dis: "~disjnt (affine hull T) (rel_interior U)"
   275   shows "U \<subseteq> T"
   276   apply (rule subset_of_face_of [OF T \<open>U \<subseteq> S\<close>])
   277   using face_of_imp_eq_affine_Int [OF \<open>convex S\<close> T]
   278   using rel_interior_subset [of U] dis
   279   using \<open>U \<subseteq> S\<close> disjnt_def by fastforce
   280 
   281 lemma affine_hull_face_of_disjoint_rel_interior:
   282     fixes S :: "'a::euclidean_space set"
   283   assumes "convex S" "F face_of S" "F \<noteq> S"
   284   shows "affine hull F \<inter> rel_interior S = {}"
   285   by (metis assms disjnt_def face_of_imp_subset order_refl subset_antisym subset_of_face_of_affine_hull)
   286 
   287 lemma affine_diff_divide:
   288     assumes "affine S" "k \<noteq> 0" "k \<noteq> 1" and xy: "x \<in> S" "y /\<^sub>R (1 - k) \<in> S"
   289       shows "(x - y) /\<^sub>R k \<in> S"
   290 proof -
   291   have "inverse(k) *\<^sub>R (x - y) = (1 - inverse k) *\<^sub>R inverse(1 - k) *\<^sub>R y + inverse(k) *\<^sub>R x"
   292     using assms
   293     by (simp add: algebra_simps) (simp add: scaleR_left_distrib [symmetric] divide_simps)
   294   then show ?thesis
   295     using \<open>affine S\<close> xy by (auto simp: affine_alt)
   296 qed
   297 
   298 lemma face_of_convex_hulls:
   299       assumes S: "finite S" "T \<subseteq> S" and disj: "affine hull T \<inter> convex hull (S - T) = {}"
   300       shows  "(convex hull T) face_of (convex hull S)"
   301 proof -
   302   have fin: "finite T" "finite (S - T)" using assms
   303     by (auto simp: finite_subset)
   304   have *: "x \<in> convex hull T"
   305           if x: "x \<in> convex hull S" and y: "y \<in> convex hull S" and w: "w \<in> convex hull T" "w \<in> open_segment x y"
   306           for x y w
   307   proof -
   308     have waff: "w \<in> affine hull T"
   309       using convex_hull_subset_affine_hull w by blast
   310     obtain a b where a: "\<And>i. i \<in> S \<Longrightarrow> 0 \<le> a i" and asum: "sum a S = 1" and aeqx: "(\<Sum>i\<in>S. a i *\<^sub>R i) = x"
   311                  and b: "\<And>i. i \<in> S \<Longrightarrow> 0 \<le> b i" and bsum: "sum b S = 1" and beqy: "(\<Sum>i\<in>S. b i *\<^sub>R i) = y"
   312       using x y by (auto simp: assms convex_hull_finite)
   313     obtain u where "(1 - u) *\<^sub>R x + u *\<^sub>R y \<in> convex hull T" "x \<noteq> y" and weq: "w = (1 - u) *\<^sub>R x + u *\<^sub>R y"
   314                and u01: "0 < u" "u < 1"
   315       using w by (auto simp: open_segment_image_interval split: if_split_asm)
   316     define c where "c i = (1 - u) * a i + u * b i" for i
   317     have cge0: "\<And>i. i \<in> S \<Longrightarrow> 0 \<le> c i"
   318       using a b u01 by (simp add: c_def)
   319     have sumc1: "sum c S = 1"
   320       by (simp add: c_def sum.distrib sum_distrib_left [symmetric] asum bsum)
   321     have sumci_xy: "(\<Sum>i\<in>S. c i *\<^sub>R i) = (1 - u) *\<^sub>R x + u *\<^sub>R y"
   322       apply (simp add: c_def sum.distrib scaleR_left_distrib)
   323       by (simp only: scaleR_scaleR [symmetric] Real_Vector_Spaces.scaleR_right.sum [symmetric] aeqx beqy)
   324     show ?thesis
   325     proof (cases "sum c (S - T) = 0")
   326       case True
   327       have ci0: "\<And>i. i \<in> (S - T) \<Longrightarrow> c i = 0"
   328         using True cge0 fin(2) sum_nonneg_eq_0_iff by auto
   329       have a0: "a i = 0" if "i \<in> (S - T)" for i
   330         using ci0 [OF that] u01 a [of i] b [of i] that
   331         by (simp add: c_def Groups.ordered_comm_monoid_add_class.add_nonneg_eq_0_iff)
   332       have [simp]: "sum a T = 1"
   333         using assms by (metis sum.mono_neutral_cong_right a0 asum)
   334       show ?thesis
   335         apply (simp add: convex_hull_finite \<open>finite T\<close>)
   336         apply (rule_tac x=a in exI)
   337         using a0 assms
   338         apply (auto simp: cge0 a aeqx [symmetric] sum.mono_neutral_right)
   339         done
   340     next
   341       case False
   342       define k where "k = sum c (S - T)"
   343       have "k > 0" using False
   344         unfolding k_def by (metis DiffD1 antisym_conv cge0 sum_nonneg not_less)
   345       have weq_sumsum: "w = sum (\<lambda>x. c x *\<^sub>R x) T + sum (\<lambda>x. c x *\<^sub>R x) (S - T)"
   346         by (metis (no_types) add.commute S(1) S(2) sum.subset_diff sumci_xy weq)
   347       show ?thesis
   348       proof (cases "k = 1")
   349         case True
   350         then have "sum c T = 0"
   351           by (simp add: S k_def sum_diff sumc1)
   352         then have [simp]: "sum c (S - T) = 1"
   353           by (simp add: S sum_diff sumc1)
   354         have ci0: "\<And>i. i \<in> T \<Longrightarrow> c i = 0"
   355           by (meson \<open>finite T\<close> \<open>sum c T = 0\<close> \<open>T \<subseteq> S\<close> cge0 sum_nonneg_eq_0_iff subsetCE)
   356         then have [simp]: "(\<Sum>i\<in>S-T. c i *\<^sub>R i) = w"
   357           by (simp add: weq_sumsum)
   358         have "w \<in> convex hull (S - T)"
   359           apply (simp add: convex_hull_finite fin)
   360           apply (rule_tac x=c in exI)
   361           apply (auto simp: cge0 weq True k_def)
   362           done
   363         then show ?thesis
   364           using disj waff by blast
   365       next
   366         case False
   367         then have sumcf: "sum c T = 1 - k"
   368           by (simp add: S k_def sum_diff sumc1)
   369         have "(\<Sum>i\<in>T. c i *\<^sub>R i) /\<^sub>R (1 - k) \<in> convex hull T"
   370           apply (simp add: convex_hull_finite fin)
   371           apply (rule_tac x="\<lambda>i. inverse (1-k) * c i" in exI)
   372           apply auto
   373           apply (metis sumcf cge0 inverse_nonnegative_iff_nonnegative mult_nonneg_nonneg S(2) sum_nonneg subsetCE)
   374           apply (metis False mult.commute right_inverse right_minus_eq sum_distrib_left sumcf)
   375           by (metis (mono_tags, lifting) scaleR_right.sum scaleR_scaleR sum.cong)
   376         with \<open>0 < k\<close>  have "inverse(k) *\<^sub>R (w - sum (\<lambda>i. c i *\<^sub>R i) T) \<in> affine hull T"
   377           by (simp add: affine_diff_divide [OF affine_affine_hull] False waff convex_hull_subset_affine_hull [THEN subsetD])
   378         moreover have "inverse(k) *\<^sub>R (w - sum (\<lambda>x. c x *\<^sub>R x) T) \<in> convex hull (S - T)"
   379           apply (simp add: weq_sumsum convex_hull_finite fin)
   380           apply (rule_tac x="\<lambda>i. inverse k * c i" in exI)
   381           using \<open>k > 0\<close> cge0
   382           apply (auto simp: scaleR_right.sum sum_distrib_left [symmetric] k_def [symmetric])
   383           done
   384         ultimately show ?thesis
   385           using disj by blast
   386       qed
   387     qed
   388   qed
   389   have [simp]: "convex hull T \<subseteq> convex hull S"
   390     by (simp add: \<open>T \<subseteq> S\<close> hull_mono)
   391   show ?thesis
   392     using open_segment_commute by (auto simp: face_of_def intro: *)
   393 qed
   394 
   395 proposition face_of_convex_hull_insert:
   396    "\<lbrakk>finite S; a \<notin> affine hull S; T face_of convex hull S\<rbrakk> \<Longrightarrow> T face_of convex hull insert a S"
   397   apply (rule face_of_trans, blast)
   398   apply (rule face_of_convex_hulls; force simp: insert_Diff_if)
   399   done
   400 
   401 proposition face_of_affine_trivial:
   402     assumes "affine S" "T face_of S"
   403     shows "T = {} \<or> T = S"
   404 proof (rule ccontr, clarsimp)
   405   assume "T \<noteq> {}" "T \<noteq> S"
   406   then obtain a where "a \<in> T" by auto
   407   then have "a \<in> S"
   408     using \<open>T face_of S\<close> face_of_imp_subset by blast
   409   have "S \<subseteq> T"
   410   proof
   411     fix b  assume "b \<in> S"
   412     show "b \<in> T"
   413     proof (cases "a = b")
   414       case True with \<open>a \<in> T\<close> show ?thesis by auto
   415     next
   416       case False
   417       then have "a \<in> open_segment (2 *\<^sub>R a - b) b"
   418         apply (auto simp: open_segment_def closed_segment_def)
   419         apply (rule_tac x="1/2" in exI)
   420         apply (simp add: algebra_simps)
   421         by (simp add: scaleR_2)
   422       moreover have "2 *\<^sub>R a - b \<in> S"
   423         by (rule mem_affine [OF \<open>affine S\<close> \<open>a \<in> S\<close> \<open>b \<in> S\<close>, of 2 "-1", simplified])
   424       moreover note \<open>b \<in> S\<close> \<open>a \<in> T\<close>
   425       ultimately show ?thesis
   426         by (rule face_ofD [OF \<open>T face_of S\<close>, THEN conjunct2])
   427     qed
   428   qed
   429   then show False
   430     using \<open>T \<noteq> S\<close> \<open>T face_of S\<close> face_of_imp_subset by blast
   431 qed
   432 
   433 
   434 lemma face_of_affine_eq:
   435    "affine S \<Longrightarrow> (T face_of S \<longleftrightarrow> T = {} \<or> T = S)"
   436 using affine_imp_convex face_of_affine_trivial face_of_refl by auto
   437 
   438 
   439 lemma Inter_faces_finite_altbound:
   440     fixes T :: "'a::euclidean_space set set"
   441     assumes cfaI: "\<And>c. c \<in> T \<Longrightarrow> c face_of S"
   442     shows "\<exists>F'. finite F' \<and> F' \<subseteq> T \<and> card F' \<le> DIM('a) + 2 \<and> \<Inter>F' = \<Inter>T"
   443 proof (cases "\<forall>F'. finite F' \<and> F' \<subseteq> T \<and> card F' \<le> DIM('a) + 2 \<longrightarrow> (\<exists>c. c \<in> T \<and> c \<inter> (\<Inter>F') \<subset> (\<Inter>F'))")
   444   case True
   445   then obtain c where c:
   446        "\<And>F'. \<lbrakk>finite F'; F' \<subseteq> T; card F' \<le> DIM('a) + 2\<rbrakk> \<Longrightarrow> c F' \<in> T \<and> c F' \<inter> (\<Inter>F') \<subset> (\<Inter>F')"
   447     by metis
   448   define d where "d = rec_nat {c{}} (\<lambda>n r. insert (c r) r)"
   449   have [simp]: "d 0 = {c {}}"
   450     by (simp add: d_def)
   451   have dSuc [simp]: "\<And>n. d (Suc n) = insert (c (d n)) (d n)"
   452     by (simp add: d_def)
   453   have dn_notempty: "d n \<noteq> {}" for n
   454     by (induction n) auto
   455   have dn_le_Suc: "d n \<subseteq> T \<and> finite(d n) \<and> card(d n) \<le> Suc n" if "n \<le> DIM('a) + 2" for n
   456   using that
   457   proof (induction n)
   458     case 0
   459     then show ?case by (simp add: c)
   460   next
   461     case (Suc n)
   462     then show ?case by (auto simp: c card_insert_if)
   463   qed
   464   have aff_dim_le: "aff_dim(\<Inter>(d n)) \<le> DIM('a) - int n" if "n \<le> DIM('a) + 2" for n
   465   using that
   466   proof (induction n)
   467     case 0
   468     then show ?case
   469       by (simp add: aff_dim_le_DIM)
   470   next
   471     case (Suc n)
   472     have fs: "\<Inter>d (Suc n) face_of S"
   473       by (meson Suc.prems cfaI dn_le_Suc dn_notempty face_of_Inter subsetCE)
   474     have condn: "convex (\<Inter>d n)"
   475       using Suc.prems nat_le_linear not_less_eq_eq
   476       by (blast intro: face_of_imp_convex cfaI convex_Inter dest: dn_le_Suc)
   477     have fdn: "\<Inter>d (Suc n) face_of \<Inter>d n"
   478       by (metis (no_types, lifting) Inter_anti_mono Suc.prems dSuc cfaI dn_le_Suc dn_notempty face_of_Inter face_of_imp_subset face_of_subset subset_iff subset_insertI)
   479     have ne: "\<Inter>d (Suc n) \<noteq> \<Inter>d n"
   480       by (metis (no_types, lifting) Suc.prems Suc_leD c complete_lattice_class.Inf_insert dSuc dn_le_Suc less_irrefl order.trans)
   481     have *: "\<And>m::int. \<And>d. \<And>d'::int. d < d' \<and> d' \<le> m - n \<Longrightarrow> d \<le> m - of_nat(n+1)"
   482       by arith
   483     have "aff_dim (\<Inter>d (Suc n)) < aff_dim (\<Inter>d n)"
   484       by (rule face_of_aff_dim_lt [OF condn fdn ne])
   485     moreover have "aff_dim (\<Inter>d n) \<le> int (DIM('a)) - int n"
   486       using Suc by auto
   487     ultimately
   488     have "aff_dim (\<Inter>d (Suc n)) \<le> int (DIM('a)) - (n+1)" by arith
   489     then show ?case by linarith
   490   qed
   491   have "aff_dim (\<Inter>d (DIM('a) + 2)) \<le> -2"
   492       using aff_dim_le [OF order_refl] by simp
   493   with aff_dim_geq [of "\<Inter>d (DIM('a) + 2)"] show ?thesis
   494     using order.trans by fastforce
   495 next
   496   case False
   497   then show ?thesis
   498     apply simp
   499     apply (erule ex_forward)
   500     by blast
   501 qed
   502 
   503 lemma faces_of_translation:
   504    "{F. F face_of image (\<lambda>x. a + x) S} = image (image (\<lambda>x. a + x)) {F. F face_of S}"
   505 apply (rule subset_antisym, clarify)
   506 apply (auto simp: image_iff)
   507 apply (metis face_of_imp_subset face_of_translation_eq subset_imageE)
   508 done
   509 
   510 proposition face_of_Times:
   511   assumes "F face_of S" and "F' face_of S'"
   512     shows "(F \<times> F') face_of (S \<times> S')"
   513 proof -
   514   have "F \<times> F' \<subseteq> S \<times> S'"
   515     using assms [unfolded face_of_def] by blast
   516   moreover
   517   have "convex (F \<times> F')"
   518     using assms [unfolded face_of_def] by (blast intro: convex_Times)
   519   moreover
   520     have "a \<in> F \<and> a' \<in> F' \<and> b \<in> F \<and> b' \<in> F'"
   521        if "a \<in> S" "b \<in> S" "a' \<in> S'" "b' \<in> S'" "x \<in> F \<times> F'" "x \<in> open_segment (a,a') (b,b')"
   522        for a b a' b' x
   523   proof (cases "b=a \<or> b'=a'")
   524     case True with that show ?thesis
   525       using assms
   526       by (force simp: in_segment dest: face_ofD)
   527   next
   528     case False with assms [unfolded face_of_def] that show ?thesis
   529       by (blast dest!: open_segment_PairD)
   530   qed
   531   ultimately show ?thesis
   532     unfolding face_of_def by blast
   533 qed
   534 
   535 corollary face_of_Times_decomp:
   536     fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
   537     shows "c face_of (S \<times> S') \<longleftrightarrow> (\<exists>F F'. F face_of S \<and> F' face_of S' \<and> c = F \<times> F')"
   538      (is "?lhs = ?rhs")
   539 proof
   540   assume c: ?lhs
   541   show ?rhs
   542   proof (cases "c = {}")
   543     case True then show ?thesis by auto
   544   next
   545     case False
   546     have 1: "fst ` c \<subseteq> S" "snd ` c \<subseteq> S'"
   547       using c face_of_imp_subset by fastforce+
   548     have "convex c"
   549       using c by (metis face_of_imp_convex)
   550     have conv: "convex (fst ` c)" "convex (snd ` c)"
   551       by (simp_all add: \<open>convex c\<close> convex_linear_image fst_linear snd_linear)
   552     have fstab: "a \<in> fst ` c \<and> b \<in> fst ` c"
   553             if "a \<in> S" "b \<in> S" "x \<in> open_segment a b" "(x,x') \<in> c" for a b x x'
   554     proof -
   555       have *: "(x,x') \<in> open_segment (a,x') (b,x')"
   556         using that by (auto simp: in_segment)
   557       show ?thesis
   558         using face_ofD [OF c *] that face_of_imp_subset [OF c] by force
   559     qed
   560     have fst: "fst ` c face_of S"
   561       by (force simp: face_of_def 1 conv fstab)
   562     have sndab: "a' \<in> snd ` c \<and> b' \<in> snd ` c"
   563             if "a' \<in> S'" "b' \<in> S'" "x' \<in> open_segment a' b'" "(x,x') \<in> c" for a' b' x x'
   564     proof -
   565       have *: "(x,x') \<in> open_segment (x,a') (x,b')"
   566         using that by (auto simp: in_segment)
   567       show ?thesis
   568         using face_ofD [OF c *] that face_of_imp_subset [OF c] by force
   569     qed
   570     have snd: "snd ` c face_of S'"
   571       by (force simp: face_of_def 1 conv sndab)
   572     have cc: "rel_interior c \<subseteq> rel_interior (fst ` c) \<times> rel_interior (snd ` c)"
   573       by (force simp: face_of_Times rel_interior_Times conv fst snd \<open>convex c\<close> fst_linear snd_linear rel_interior_convex_linear_image [symmetric])
   574     have "c = fst ` c \<times> snd ` c"
   575       apply (rule face_of_eq [OF c])
   576       apply (simp_all add: face_of_Times rel_interior_Times conv fst snd)
   577       using False rel_interior_eq_empty \<open>convex c\<close> cc
   578       apply blast
   579       done
   580     with fst snd show ?thesis by metis
   581   qed
   582 next
   583   assume ?rhs with face_of_Times show ?lhs by auto
   584 qed
   585 
   586 lemma face_of_Times_eq:
   587     fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
   588     shows "(F \<times> F') face_of (S \<times> S') \<longleftrightarrow>
   589            F = {} \<or> F' = {} \<or> F face_of S \<and> F' face_of S'"
   590 by (auto simp: face_of_Times_decomp times_eq_iff)
   591 
   592 lemma hyperplane_face_of_halfspace_le: "{x. a \<bullet> x = b} face_of {x. a \<bullet> x \<le> b}"
   593 proof -
   594   have "{x. a \<bullet> x \<le> b} \<inter> {x. a \<bullet> x = b} = {x. a \<bullet> x = b}"
   595     by auto
   596   with face_of_Int_supporting_hyperplane_le [OF convex_halfspace_le [of a b], of a b]
   597   show ?thesis by auto
   598 qed
   599 
   600 lemma hyperplane_face_of_halfspace_ge: "{x. a \<bullet> x = b} face_of {x. a \<bullet> x \<ge> b}"
   601 proof -
   602   have "{x. a \<bullet> x \<ge> b} \<inter> {x. a \<bullet> x = b} = {x. a \<bullet> x = b}"
   603     by auto
   604   with face_of_Int_supporting_hyperplane_ge [OF convex_halfspace_ge [of b a], of b a]
   605   show ?thesis by auto
   606 qed
   607 
   608 lemma face_of_halfspace_le:
   609   fixes a :: "'n::euclidean_space"
   610   shows "F face_of {x. a \<bullet> x \<le> b} \<longleftrightarrow>
   611          F = {} \<or> F = {x. a \<bullet> x = b} \<or> F = {x. a \<bullet> x \<le> b}"
   612      (is "?lhs = ?rhs")
   613 proof (cases "a = 0")
   614   case True then show ?thesis
   615     using face_of_affine_eq affine_UNIV by auto
   616 next
   617   case False
   618   then have ine: "interior {x. a \<bullet> x \<le> b} \<noteq> {}"
   619     using halfspace_eq_empty_lt interior_halfspace_le by blast
   620   show ?thesis
   621   proof
   622     assume L: ?lhs
   623     have "F \<noteq> {x. a \<bullet> x \<le> b} \<Longrightarrow> F face_of {x. a \<bullet> x = b}"
   624       using False
   625       apply (simp add: frontier_halfspace_le [symmetric] rel_frontier_nonempty_interior [OF ine, symmetric])
   626       apply (rule face_of_subset [OF L])
   627       apply (simp add: face_of_subset_rel_frontier [OF L])
   628       apply (force simp: rel_frontier_def closed_halfspace_le)
   629       done
   630     with L show ?rhs
   631       using affine_hyperplane face_of_affine_eq by blast
   632   next
   633     assume ?rhs
   634     then show ?lhs
   635       by (metis convex_halfspace_le empty_face_of face_of_refl hyperplane_face_of_halfspace_le)
   636   qed
   637 qed
   638 
   639 lemma face_of_halfspace_ge:
   640   fixes a :: "'n::euclidean_space"
   641   shows "F face_of {x. a \<bullet> x \<ge> b} \<longleftrightarrow>
   642          F = {} \<or> F = {x. a \<bullet> x = b} \<or> F = {x. a \<bullet> x \<ge> b}"
   643 using face_of_halfspace_le [of F "-a" "-b"] by simp
   644 
   645 subsection\<open>Exposed faces\<close>
   646 
   647 text\<open>That is, faces that are intersection with supporting hyperplane\<close>
   648 
   649 definition exposed_face_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"
   650                                (infixr "(exposed'_face'_of)" 50)
   651   where "T exposed_face_of S \<longleftrightarrow>
   652          T face_of S \<and> (\<exists>a b. S \<subseteq> {x. a \<bullet> x \<le> b} \<and> T = S \<inter> {x. a \<bullet> x = b})"
   653 
   654 lemma empty_exposed_face_of [iff]: "{} exposed_face_of S"
   655   apply (simp add: exposed_face_of_def)
   656   apply (rule_tac x=0 in exI)
   657   apply (rule_tac x=1 in exI, force)
   658   done
   659 
   660 lemma exposed_face_of_refl_eq [simp]: "S exposed_face_of S \<longleftrightarrow> convex S"
   661   apply (simp add: exposed_face_of_def face_of_refl_eq, auto)
   662   apply (rule_tac x=0 in exI)+
   663   apply force
   664   done
   665 
   666 lemma exposed_face_of_refl: "convex S \<Longrightarrow> S exposed_face_of S"
   667   by simp
   668 
   669 lemma exposed_face_of:
   670     "T exposed_face_of S \<longleftrightarrow>
   671      T face_of S \<and>
   672      (T = {} \<or> T = S \<or>
   673       (\<exists>a b. a \<noteq> 0 \<and> S \<subseteq> {x. a \<bullet> x \<le> b} \<and> T = S \<inter> {x. a \<bullet> x = b}))"
   674 proof (cases "T = {}")
   675   case True then show ?thesis
   676     by simp
   677 next
   678   case False
   679   show ?thesis
   680   proof (cases "T = S")
   681     case True then show ?thesis
   682       by (simp add: face_of_refl_eq)
   683   next
   684     case False
   685     with \<open>T \<noteq> {}\<close> show ?thesis
   686       apply (auto simp: exposed_face_of_def)
   687       apply (metis inner_zero_left)
   688       done
   689   qed
   690 qed
   691 
   692 lemma exposed_face_of_Int_supporting_hyperplane_le:
   693    "\<lbrakk>convex S; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b\<rbrakk> \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) exposed_face_of S"
   694 by (force simp: exposed_face_of_def face_of_Int_supporting_hyperplane_le)
   695 
   696 lemma exposed_face_of_Int_supporting_hyperplane_ge:
   697    "\<lbrakk>convex S; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b\<rbrakk> \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) exposed_face_of S"
   698 using exposed_face_of_Int_supporting_hyperplane_le [of S "-a" "-b"] by simp
   699 
   700 proposition exposed_face_of_Int:
   701   assumes "T exposed_face_of S"
   702       and "u exposed_face_of S"
   703     shows "(T \<inter> u) exposed_face_of S"
   704 proof -
   705   obtain a b where T: "S \<inter> {x. a \<bullet> x = b} face_of S"
   706                and S: "S \<subseteq> {x. a \<bullet> x \<le> b}"
   707                and teq: "T = S \<inter> {x. a \<bullet> x = b}"
   708     using assms by (auto simp: exposed_face_of_def)
   709   obtain a' b' where u: "S \<inter> {x. a' \<bullet> x = b'} face_of S"
   710                  and s': "S \<subseteq> {x. a' \<bullet> x \<le> b'}"
   711                  and ueq: "u = S \<inter> {x. a' \<bullet> x = b'}"
   712     using assms by (auto simp: exposed_face_of_def)
   713   have tu: "T \<inter> u face_of S"
   714     using T teq u ueq by (simp add: face_of_Int)
   715   have ss: "S \<subseteq> {x. (a + a') \<bullet> x \<le> b + b'}"
   716     using S s' by (force simp: inner_left_distrib)
   717   show ?thesis
   718     apply (simp add: exposed_face_of_def tu)
   719     apply (rule_tac x="a+a'" in exI)
   720     apply (rule_tac x="b+b'" in exI)
   721     using S s'
   722     apply (fastforce simp: ss inner_left_distrib teq ueq)
   723     done
   724 qed
   725 
   726 proposition exposed_face_of_Inter:
   727     fixes P :: "'a::euclidean_space set set"
   728   assumes "P \<noteq> {}"
   729       and "\<And>T. T \<in> P \<Longrightarrow> T exposed_face_of S"
   730     shows "\<Inter>P exposed_face_of S"
   731 proof -
   732   obtain Q where "finite Q" and QsubP: "Q \<subseteq> P" "card Q \<le> DIM('a) + 2" and IntQ: "\<Inter>Q = \<Inter>P"
   733     using Inter_faces_finite_altbound [of P S] assms [unfolded exposed_face_of]
   734     by force
   735   show ?thesis
   736   proof (cases "Q = {}")
   737     case True then show ?thesis
   738       sledgehammer
   739       by (metis IntQ Inter_UNIV_conv(2) assms(1) assms(2) ex_in_conv)
   740 (*
   741       by (metis Inf_empty Inf_lower IntQ assms ex_in_conv subset_antisym top_greatest)
   742 *)
   743   next
   744     case False
   745     have "Q \<subseteq> {T. T exposed_face_of S}"
   746       using QsubP assms by blast
   747     moreover have "Q \<subseteq> {T. T exposed_face_of S} \<Longrightarrow> \<Inter>Q exposed_face_of S"
   748       using \<open>finite Q\<close> False
   749       apply (induction Q rule: finite_induct)
   750       using exposed_face_of_Int apply fastforce+
   751       done
   752     ultimately show ?thesis
   753       by (simp add: IntQ)
   754   qed
   755 qed
   756 
   757 proposition exposed_face_of_sums:
   758   assumes "convex S" and "convex T"
   759       and "F exposed_face_of {x + y | x y. x \<in> S \<and> y \<in> T}"
   760           (is "F exposed_face_of ?ST")
   761   obtains k l
   762     where "k exposed_face_of S" "l exposed_face_of T"
   763           "F = {x + y | x y. x \<in> k \<and> y \<in> l}"
   764 proof (cases "F = {}")
   765   case True then show ?thesis
   766     using that by blast
   767 next
   768   case False
   769   show ?thesis
   770   proof (cases "F = ?ST")
   771     case True then show ?thesis
   772       using assms exposed_face_of_refl_eq that by blast
   773   next
   774     case False
   775     obtain p where "p \<in> F" using \<open>F \<noteq> {}\<close> by blast
   776     moreover
   777     obtain u z where T: "?ST \<inter> {x. u \<bullet> x = z} face_of ?ST"
   778                  and S: "?ST \<subseteq> {x. u \<bullet> x \<le> z}"
   779                  and feq: "F = ?ST \<inter> {x. u \<bullet> x = z}"
   780       using assms by (auto simp: exposed_face_of_def)
   781     ultimately obtain a0 b0
   782             where p: "p = a0 + b0" and "a0 \<in> S" "b0 \<in> T" and z: "u \<bullet> p = z"
   783       by auto
   784     have lez: "u \<bullet> (x + y) \<le> z" if "x \<in> S" "y \<in> T" for x y
   785       using S that by auto
   786     have sef: "S \<inter> {x. u \<bullet> x = u \<bullet> a0} exposed_face_of S"
   787       apply (rule exposed_face_of_Int_supporting_hyperplane_le [OF \<open>convex S\<close>])
   788       apply (metis p z add_le_cancel_right inner_right_distrib lez [OF _ \<open>b0 \<in> T\<close>])
   789       done
   790     have tef: "T \<inter> {x. u \<bullet> x = u \<bullet> b0} exposed_face_of T"
   791       apply (rule exposed_face_of_Int_supporting_hyperplane_le [OF \<open>convex T\<close>])
   792       apply (metis p z add.commute add_le_cancel_right inner_right_distrib lez [OF \<open>a0 \<in> S\<close>])
   793       done
   794     have "{x + y |x y. x \<in> S \<and> u \<bullet> x = u \<bullet> a0 \<and> y \<in> T \<and> u \<bullet> y = u \<bullet> b0} \<subseteq> F"
   795       by (auto simp: feq) (metis inner_right_distrib p z)
   796     moreover have "F \<subseteq> {x + y |x y. x \<in> S \<and> u \<bullet> x = u \<bullet> a0 \<and> y \<in> T \<and> u \<bullet> y = u \<bullet> b0}"
   797       apply (auto simp: feq)
   798       apply (rename_tac x y)
   799       apply (rule_tac x=x in exI)
   800       apply (rule_tac x=y in exI, simp)
   801       using z p \<open>a0 \<in> S\<close> \<open>b0 \<in> T\<close>
   802       apply clarify
   803       apply (simp add: inner_right_distrib)
   804       apply (metis add_le_cancel_right antisym lez [unfolded inner_right_distrib] add.commute)
   805       done
   806     ultimately have "F = {x + y |x y. x \<in> S \<inter> {x. u \<bullet> x = u \<bullet> a0} \<and> y \<in> T \<inter> {x. u \<bullet> x = u \<bullet> b0}}"
   807       by blast
   808     then show ?thesis
   809       by (rule that [OF sef tef])
   810   qed
   811 qed
   812 
   813 lemma exposed_face_of_parallel:
   814    "T exposed_face_of S \<longleftrightarrow>
   815          T face_of S \<and>
   816          (\<exists>a b. S \<subseteq> {x. a \<bullet> x \<le> b} \<and> T = S \<inter> {x. a \<bullet> x = b} \<and>
   817                 (T \<noteq> {} \<longrightarrow> T \<noteq> S \<longrightarrow> a \<noteq> 0) \<and>
   818                 (T \<noteq> S \<longrightarrow> (\<forall>w \<in> affine hull S. (w + a) \<in> affine hull S)))"
   819   (is "?lhs = ?rhs")
   820 proof
   821   assume ?lhs then show ?rhs
   822   proof (clarsimp simp: exposed_face_of_def)
   823     fix a b
   824     assume faceS: "S \<inter> {x. a \<bullet> x = b} face_of S" and Ssub: "S \<subseteq> {x. a \<bullet> x \<le> b}" 
   825     show "\<exists>c d. S \<subseteq> {x. c \<bullet> x \<le> d} \<and>
   826                 S \<inter> {x. a \<bullet> x = b} = S \<inter> {x. c \<bullet> x = d} \<and>
   827                 (S \<inter> {x. a \<bullet> x = b} \<noteq> {} \<longrightarrow> S \<inter> {x. a \<bullet> x = b} \<noteq> S \<longrightarrow> c \<noteq> 0) \<and>
   828                 (S \<inter> {x. a \<bullet> x = b} \<noteq> S \<longrightarrow> (\<forall>w \<in> affine hull S. w + c \<in> affine hull S))"
   829     proof (cases "affine hull S \<inter> {x. -a \<bullet> x \<le> -b} = {} \<or> affine hull S \<subseteq> {x. - a \<bullet> x \<le> - b}")
   830       case True
   831       then show ?thesis
   832       proof
   833         assume "affine hull S \<inter> {x. - a \<bullet> x \<le> - b} = {}"
   834        then show ?thesis
   835          apply (rule_tac x="0" in exI)
   836          apply (rule_tac x="1" in exI)
   837          using hull_subset by fastforce
   838     next
   839       assume "affine hull S \<subseteq> {x. - a \<bullet> x \<le> - b}"
   840       then show ?thesis
   841          apply (rule_tac x="0" in exI)
   842          apply (rule_tac x="0" in exI)
   843         using Ssub hull_subset by fastforce
   844     qed
   845   next
   846     case False
   847     then obtain a' b' where "a' \<noteq> 0" 
   848       and le: "affine hull S \<inter> {x. a' \<bullet> x \<le> b'} = affine hull S \<inter> {x. - a \<bullet> x \<le> - b}" 
   849       and eq: "affine hull S \<inter> {x. a' \<bullet> x = b'} = affine hull S \<inter> {x. - a \<bullet> x = - b}" 
   850       and mem: "\<And>w. w \<in> affine hull S \<Longrightarrow> w + a' \<in> affine hull S"
   851       using affine_parallel_slice affine_affine_hull by metis 
   852     show ?thesis
   853     proof (intro conjI impI allI ballI exI)
   854       have *: "S \<subseteq> - (affine hull S \<inter> {x. P x}) \<union> affine hull S \<inter> {x. Q x} \<Longrightarrow> S \<subseteq> {x. ~P x \<or> Q x}" 
   855         for P Q 
   856         using hull_subset by fastforce  
   857       have "S \<subseteq> {x. ~ (a' \<bullet> x \<le> b') \<or> a' \<bullet> x = b'}"
   858         apply (rule *)
   859         apply (simp only: le eq)
   860         using Ssub by auto
   861       then show "S \<subseteq> {x. - a' \<bullet> x \<le> - b'}"
   862         by auto 
   863       show "S \<inter> {x. a \<bullet> x = b} = S \<inter> {x. - a' \<bullet> x = - b'}"
   864         using eq hull_subset [of S affine] by force
   865       show "\<lbrakk>S \<inter> {x. a \<bullet> x = b} \<noteq> {}; S \<inter> {x. a \<bullet> x = b} \<noteq> S\<rbrakk> \<Longrightarrow> - a' \<noteq> 0"
   866         using \<open>a' \<noteq> 0\<close> by auto
   867       show "w + - a' \<in> affine hull S"
   868         if "S \<inter> {x. a \<bullet> x = b} \<noteq> S" "w \<in> affine hull S" for w
   869       proof -
   870         have "w + 1 *\<^sub>R (w - (w + a')) \<in> affine hull S"
   871           using affine_affine_hull mem mem_affine_3_minus that(2) by blast
   872         then show ?thesis  by simp
   873       qed
   874     qed
   875   qed
   876 qed
   877 next
   878   assume ?rhs then show ?lhs
   879     unfolding exposed_face_of_def by blast
   880 qed
   881 
   882 subsection\<open>Extreme points of a set: its singleton faces\<close>
   883 
   884 definition extreme_point_of :: "['a::real_vector, 'a set] \<Rightarrow> bool"
   885                                (infixr "(extreme'_point'_of)" 50)
   886   where "x extreme_point_of S \<longleftrightarrow>
   887          x \<in> S \<and> (\<forall>a \<in> S. \<forall>b \<in> S. x \<notin> open_segment a b)"
   888 
   889 lemma extreme_point_of_stillconvex:
   890    "convex S \<Longrightarrow> (x extreme_point_of S \<longleftrightarrow> x \<in> S \<and> convex(S - {x}))"
   891   by (fastforce simp add: convex_contains_segment extreme_point_of_def open_segment_def)
   892 
   893 lemma face_of_singleton:
   894    "{x} face_of S \<longleftrightarrow> x extreme_point_of S"
   895 by (fastforce simp add: extreme_point_of_def face_of_def)
   896 
   897 lemma extreme_point_not_in_REL_INTERIOR:
   898     fixes S :: "'a::real_normed_vector set"
   899     shows "\<lbrakk>x extreme_point_of S; S \<noteq> {x}\<rbrakk> \<Longrightarrow> x \<notin> rel_interior S"
   900 apply (simp add: face_of_singleton [symmetric])
   901 apply (blast dest: face_of_disjoint_rel_interior)
   902 done
   903 
   904 lemma extreme_point_not_in_interior:
   905     fixes S :: "'a::{real_normed_vector, perfect_space} set"
   906     shows "x extreme_point_of S \<Longrightarrow> x \<notin> interior S"
   907 apply (case_tac "S = {x}")
   908 apply (simp add: empty_interior_finite)
   909 by (meson contra_subsetD extreme_point_not_in_REL_INTERIOR interior_subset_rel_interior)
   910 
   911 lemma extreme_point_of_face:
   912      "F face_of S \<Longrightarrow> v extreme_point_of F \<longleftrightarrow> v extreme_point_of S \<and> v \<in> F"
   913   by (meson empty_subsetI face_of_face face_of_singleton insert_subset)
   914 
   915 lemma extreme_point_of_convex_hull:
   916    "x extreme_point_of (convex hull S) \<Longrightarrow> x \<in> S"
   917 apply (simp add: extreme_point_of_stillconvex)
   918 using hull_minimal [of S "(convex hull S) - {x}" convex]
   919 using hull_subset [of S convex]
   920 apply blast
   921 done
   922 
   923 lemma extreme_points_of_convex_hull:
   924    "{x. x extreme_point_of (convex hull S)} \<subseteq> S"
   925 using extreme_point_of_convex_hull by auto
   926 
   927 lemma extreme_point_of_empty [simp]: "~ (x extreme_point_of {})"
   928   by (simp add: extreme_point_of_def)
   929 
   930 lemma extreme_point_of_singleton [iff]: "x extreme_point_of {a} \<longleftrightarrow> x = a"
   931   using extreme_point_of_stillconvex by auto
   932 
   933 lemma extreme_point_of_translation_eq:
   934    "(a + x) extreme_point_of (image (\<lambda>x. a + x) S) \<longleftrightarrow> x extreme_point_of S"
   935 by (auto simp: extreme_point_of_def)
   936 
   937 lemma extreme_points_of_translation:
   938    "{x. x extreme_point_of (image (\<lambda>x. a + x) S)} =
   939     (\<lambda>x. a + x) ` {x. x extreme_point_of S}"
   940 using extreme_point_of_translation_eq
   941 by auto (metis (no_types, lifting) image_iff mem_Collect_eq minus_add_cancel)
   942 
   943 lemma extreme_point_of_Int:
   944    "\<lbrakk>x extreme_point_of S; x extreme_point_of T\<rbrakk> \<Longrightarrow> x extreme_point_of (S \<inter> T)"
   945 by (simp add: extreme_point_of_def)
   946 
   947 lemma extreme_point_of_Int_supporting_hyperplane_le:
   948    "\<lbrakk>S \<inter> {x. a \<bullet> x = b} = {c}; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b\<rbrakk> \<Longrightarrow> c extreme_point_of S"
   949 apply (simp add: face_of_singleton [symmetric])
   950 by (metis face_of_Int_supporting_hyperplane_le_strong convex_singleton)
   951 
   952 lemma extreme_point_of_Int_supporting_hyperplane_ge:
   953    "\<lbrakk>S \<inter> {x. a \<bullet> x = b} = {c}; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b\<rbrakk> \<Longrightarrow> c extreme_point_of S"
   954 apply (simp add: face_of_singleton [symmetric])
   955 by (metis face_of_Int_supporting_hyperplane_ge_strong convex_singleton)
   956 
   957 lemma exposed_point_of_Int_supporting_hyperplane_le:
   958    "\<lbrakk>S \<inter> {x. a \<bullet> x = b} = {c}; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b\<rbrakk> \<Longrightarrow> {c} exposed_face_of S"
   959 apply (simp add: exposed_face_of_def face_of_singleton)
   960 apply (force simp: extreme_point_of_Int_supporting_hyperplane_le)
   961 done
   962 
   963 lemma exposed_point_of_Int_supporting_hyperplane_ge:
   964     "\<lbrakk>S \<inter> {x. a \<bullet> x = b} = {c}; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b\<rbrakk> \<Longrightarrow> {c} exposed_face_of S"
   965 using exposed_point_of_Int_supporting_hyperplane_le [of S "-a" "-b" c]
   966 by simp
   967 
   968 lemma extreme_point_of_convex_hull_insert:
   969    "\<lbrakk>finite S; a \<notin> convex hull S\<rbrakk> \<Longrightarrow> a extreme_point_of (convex hull (insert a S))"
   970 apply (case_tac "a \<in> S")
   971 apply (simp add: hull_inc)
   972 using face_of_convex_hulls [of "insert a S" "{a}"]
   973 apply (auto simp: face_of_singleton hull_same)
   974 done
   975 
   976 subsection\<open>Facets\<close>
   977 
   978 definition facet_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"
   979                     (infixr "(facet'_of)" 50)
   980   where "F facet_of S \<longleftrightarrow> F face_of S \<and> F \<noteq> {} \<and> aff_dim F = aff_dim S - 1"
   981 
   982 lemma facet_of_empty [simp]: "~ S facet_of {}"
   983   by (simp add: facet_of_def)
   984 
   985 lemma facet_of_irrefl [simp]: "~ S facet_of S "
   986   by (simp add: facet_of_def)
   987 
   988 lemma facet_of_imp_face_of: "F facet_of S \<Longrightarrow> F face_of S"
   989   by (simp add: facet_of_def)
   990 
   991 lemma facet_of_imp_subset: "F facet_of S \<Longrightarrow> F \<subseteq> S"
   992   by (simp add: face_of_imp_subset facet_of_def)
   993 
   994 lemma hyperplane_facet_of_halfspace_le:
   995    "a \<noteq> 0 \<Longrightarrow> {x. a \<bullet> x = b} facet_of {x. a \<bullet> x \<le> b}"
   996 unfolding facet_of_def hyperplane_eq_empty
   997 by (auto simp: hyperplane_face_of_halfspace_ge hyperplane_face_of_halfspace_le
   998            DIM_positive Suc_leI of_nat_diff aff_dim_halfspace_le)
   999 
  1000 lemma hyperplane_facet_of_halfspace_ge:
  1001     "a \<noteq> 0 \<Longrightarrow> {x. a \<bullet> x = b} facet_of {x. a \<bullet> x \<ge> b}"
  1002 unfolding facet_of_def hyperplane_eq_empty
  1003 by (auto simp: hyperplane_face_of_halfspace_le hyperplane_face_of_halfspace_ge
  1004            DIM_positive Suc_leI of_nat_diff aff_dim_halfspace_ge)
  1005 
  1006 lemma facet_of_halfspace_le:
  1007     "F facet_of {x. a \<bullet> x \<le> b} \<longleftrightarrow> a \<noteq> 0 \<and> F = {x. a \<bullet> x = b}"
  1008     (is "?lhs = ?rhs")
  1009 proof
  1010   assume c: ?lhs
  1011   with c facet_of_irrefl show ?rhs
  1012     by (force simp: aff_dim_halfspace_le facet_of_def face_of_halfspace_le cong: conj_cong split: if_split_asm)
  1013 next
  1014   assume ?rhs then show ?lhs
  1015     by (simp add: hyperplane_facet_of_halfspace_le)
  1016 qed
  1017 
  1018 lemma facet_of_halfspace_ge:
  1019     "F facet_of {x. a \<bullet> x \<ge> b} \<longleftrightarrow> a \<noteq> 0 \<and> F = {x. a \<bullet> x = b}"
  1020 using facet_of_halfspace_le [of F "-a" "-b"] by simp
  1021 
  1022 subsection \<open>Edges: faces of affine dimension 1\<close>
  1023 
  1024 definition edge_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"  (infixr "(edge'_of)" 50)
  1025   where "e edge_of S \<longleftrightarrow> e face_of S \<and> aff_dim e = 1"
  1026 
  1027 lemma edge_of_imp_subset:
  1028    "S edge_of T \<Longrightarrow> S \<subseteq> T"
  1029 by (simp add: edge_of_def face_of_imp_subset)
  1030 
  1031 subsection\<open>Existence of extreme points\<close>
  1032 
  1033 lemma different_norm_3_collinear_points:
  1034   fixes a :: "'a::euclidean_space"
  1035   assumes "x \<in> open_segment a b" "norm(a) = norm(b)" "norm(x) = norm(b)"
  1036   shows False
  1037 proof -
  1038   obtain u where "norm ((1 - u) *\<^sub>R a + u *\<^sub>R b) = norm b"
  1039              and "a \<noteq> b"
  1040              and u01: "0 < u" "u < 1"
  1041     using assms by (auto simp: open_segment_image_interval if_splits)
  1042   then have "(1 - u) *\<^sub>R a \<bullet> (1 - u) *\<^sub>R a + ((1 - u) * 2) *\<^sub>R a \<bullet> u *\<^sub>R b =
  1043              (1 - u * u) *\<^sub>R (a \<bullet> a)"
  1044     using assms by (simp add: norm_eq algebra_simps inner_commute)
  1045   then have "(1 - u) *\<^sub>R ((1 - u) *\<^sub>R a \<bullet> a + (2 * u) *\<^sub>R  a \<bullet> b) =
  1046              (1 - u) *\<^sub>R ((1 + u) *\<^sub>R (a \<bullet> a))"
  1047     by (simp add: algebra_simps)
  1048   then have "(1 - u) *\<^sub>R (a \<bullet> a) + (2 * u) *\<^sub>R (a \<bullet> b) = (1 + u) *\<^sub>R (a \<bullet> a)"
  1049     using u01 by auto
  1050   then have "a \<bullet> b = a \<bullet> a"
  1051     using u01 by (simp add: algebra_simps)
  1052   then have "a = b"
  1053     using \<open>norm(a) = norm(b)\<close> norm_eq vector_eq by fastforce
  1054   then show ?thesis
  1055     using \<open>a \<noteq> b\<close> by force
  1056 qed
  1057 
  1058 proposition extreme_point_exists_convex:
  1059   fixes S :: "'a::euclidean_space set"
  1060   assumes "compact S" "convex S" "S \<noteq> {}"
  1061   obtains x where "x extreme_point_of S"
  1062 proof -
  1063   obtain x where "x \<in> S" and xsup: "\<And>y. y \<in> S \<Longrightarrow> norm y \<le> norm x"
  1064     using distance_attains_sup [of S 0] assms by auto
  1065   have False if "a \<in> S" "b \<in> S" and x: "x \<in> open_segment a b" for a b
  1066   proof -
  1067     have noax: "norm a \<le> norm x" and nobx: "norm b \<le> norm x" using xsup that by auto
  1068     have "a \<noteq> b"
  1069       using empty_iff open_segment_idem x by auto
  1070     have *: "(1 - u) * na + u * nb < norm x" if "na < norm x"  "nb \<le> norm x" "0 < u" "u < 1" for na nb u
  1071     proof -
  1072       have "(1 - u) * na + u * nb < (1 - u) * norm x + u * nb"
  1073         by (simp add: that)
  1074       also have "... \<le> (1 - u) * norm x + u * norm x"
  1075         by (simp add: that)
  1076       finally have "(1 - u) * na + u * nb < (1 - u) * norm x + u * norm x" .
  1077       then show ?thesis
  1078       using scaleR_collapse [symmetric, of "norm x" u] by auto
  1079     qed
  1080     have "norm x < norm x" if "norm a < norm x"
  1081       using x
  1082       apply (clarsimp simp only: open_segment_image_interval \<open>a \<noteq> b\<close> if_False)
  1083       apply (rule norm_triangle_lt)
  1084       apply (simp add: norm_mult)
  1085       using * [of "norm a" "norm b"] nobx that
  1086         apply blast
  1087       done
  1088     moreover have "norm x < norm x" if "norm b < norm x"
  1089       using x
  1090       apply (clarsimp simp only: open_segment_image_interval \<open>a \<noteq> b\<close> if_False)
  1091       apply (rule norm_triangle_lt)
  1092       apply (simp add: norm_mult)
  1093       using * [of "norm b" "norm a" "1-u" for u] noax that
  1094         apply (simp add: add.commute)
  1095       done
  1096     ultimately have "~ (norm a < norm x) \<and> ~ (norm b < norm x)"
  1097       by auto
  1098     then show ?thesis
  1099       using different_norm_3_collinear_points noax nobx that(3) by fastforce
  1100   qed
  1101   then show ?thesis
  1102     apply (rule_tac x=x in that)
  1103     apply (force simp: extreme_point_of_def \<open>x \<in> S\<close>)
  1104     done
  1105 qed
  1106 
  1107 subsection\<open>Krein-Milman, the weaker form\<close>
  1108 
  1109 proposition Krein_Milman:
  1110   fixes S :: "'a::euclidean_space set"
  1111   assumes "compact S" "convex S"
  1112     shows "S = closure(convex hull {x. x extreme_point_of S})"
  1113 proof (cases "S = {}")
  1114   case True then show ?thesis   by simp
  1115 next
  1116   case False
  1117   have "closed S"
  1118     by (simp add: \<open>compact S\<close> compact_imp_closed)
  1119   have "closure (convex hull {x. x extreme_point_of S}) \<subseteq> S"
  1120     apply (rule closure_minimal [OF hull_minimal \<open>closed S\<close>])
  1121     using assms
  1122     apply (auto simp: extreme_point_of_def)
  1123     done
  1124   moreover have "u \<in> closure (convex hull {x. x extreme_point_of S})"
  1125                 if "u \<in> S" for u
  1126   proof (rule ccontr)
  1127     assume unot: "u \<notin> closure(convex hull {x. x extreme_point_of S})"
  1128     then obtain a b where "a \<bullet> u < b"
  1129           and ab: "\<And>x. x \<in> closure(convex hull {x. x extreme_point_of S}) \<Longrightarrow> b < a \<bullet> x"
  1130       using separating_hyperplane_closed_point [of "closure(convex hull {x. x extreme_point_of S})"]
  1131       by blast
  1132     have "continuous_on S ((\<bullet>) a)"
  1133       by (rule continuous_intros)+
  1134     then obtain m where "m \<in> S" and m: "\<And>y. y \<in> S \<Longrightarrow> a \<bullet> m \<le> a \<bullet> y"
  1135       using continuous_attains_inf [of S "\<lambda>x. a \<bullet> x"] \<open>compact S\<close> \<open>u \<in> S\<close>
  1136       by auto
  1137     define T where "T = S \<inter> {x. a \<bullet> x = a \<bullet> m}"
  1138     have "m \<in> T"
  1139       by (simp add: T_def \<open>m \<in> S\<close>)
  1140     moreover have "compact T"
  1141       by (simp add: T_def compact_Int_closed [OF \<open>compact S\<close> closed_hyperplane])
  1142     moreover have "convex T"
  1143       by (simp add: T_def convex_Int [OF \<open>convex S\<close> convex_hyperplane])
  1144     ultimately obtain v where v: "v extreme_point_of T"
  1145       using extreme_point_exists_convex [of T] by auto
  1146     then have "{v} face_of T"
  1147       by (simp add: face_of_singleton)
  1148     also have "T face_of S"
  1149       by (simp add: T_def m face_of_Int_supporting_hyperplane_ge [OF \<open>convex S\<close>])
  1150     finally have "v extreme_point_of S"
  1151       by (simp add: face_of_singleton)
  1152     then have "b < a \<bullet> v"
  1153       using closure_subset by (simp add: closure_hull hull_inc ab)
  1154     then show False
  1155       using \<open>a \<bullet> u < b\<close> \<open>{v} face_of T\<close> face_of_imp_subset m T_def that by fastforce
  1156   qed
  1157   ultimately show ?thesis
  1158     by blast
  1159 qed
  1160 
  1161 text\<open>Now the sharper form.\<close>
  1162 
  1163 lemma Krein_Milman_Minkowski_aux:
  1164   fixes S :: "'a::euclidean_space set"
  1165   assumes n: "dim S = n" and S: "compact S" "convex S" "0 \<in> S"
  1166     shows "0 \<in> convex hull {x. x extreme_point_of S}"
  1167 using n S
  1168 proof (induction n arbitrary: S rule: less_induct)
  1169   case (less n S) show ?case
  1170   proof (cases "0 \<in> rel_interior S")
  1171     case True with Krein_Milman show ?thesis
  1172       by (metis subsetD convex_convex_hull convex_rel_interior_closure less.prems(2) less.prems(3) rel_interior_subset)
  1173   next
  1174     case False
  1175     have "rel_interior S \<noteq> {}"
  1176       by (simp add: rel_interior_convex_nonempty_aux less)
  1177     then obtain c where c: "c \<in> rel_interior S" by blast
  1178     obtain a where "a \<noteq> 0"
  1179               and le_ay: "\<And>y. y \<in> S \<Longrightarrow> a \<bullet> 0 \<le> a \<bullet> y"
  1180               and less_ay: "\<And>y. y \<in> rel_interior S \<Longrightarrow> a \<bullet> 0 < a \<bullet> y"
  1181       by (blast intro: supporting_hyperplane_rel_boundary intro!: less False)
  1182     have face: "S \<inter> {x. a \<bullet> x = 0} face_of S"
  1183       apply (rule face_of_Int_supporting_hyperplane_ge [OF \<open>convex S\<close>])
  1184       using le_ay by auto
  1185     then have co: "compact (S \<inter> {x. a \<bullet> x = 0})" "convex (S \<inter> {x. a \<bullet> x = 0})"
  1186       using less.prems by (blast intro: face_of_imp_compact face_of_imp_convex)+
  1187     have "a \<bullet> y = 0" if "y \<in> span (S \<inter> {x. a \<bullet> x = 0})" for y
  1188     proof -
  1189       have "y \<in> span {x. a \<bullet> x = 0}"
  1190         by (metis inf.cobounded2 span_mono subsetCE that)
  1191       then show ?thesis
  1192         by (blast intro: span_induct [OF _ subspace_hyperplane])
  1193     qed
  1194     then have "dim (S \<inter> {x. a \<bullet> x = 0}) < n"
  1195       by (metis (no_types) less_ay c subsetD dim_eq_span inf.strict_order_iff
  1196            inf_le1 \<open>dim S = n\<close> not_le rel_interior_subset span_0 span_clauses(1))
  1197     then have "0 \<in> convex hull {x. x extreme_point_of (S \<inter> {x. a \<bullet> x = 0})}"
  1198       by (rule less.IH) (auto simp: co less.prems)
  1199     then show ?thesis
  1200       by (metis (mono_tags, lifting) Collect_mono_iff \<open>S \<inter> {x. a \<bullet> x = 0} face_of S\<close> extreme_point_of_face hull_mono subset_iff)
  1201   qed
  1202 qed
  1203 
  1204 
  1205 theorem Krein_Milman_Minkowski:
  1206   fixes S :: "'a::euclidean_space set"
  1207   assumes "compact S" "convex S"
  1208     shows "S = convex hull {x. x extreme_point_of S}"
  1209 proof
  1210   show "S \<subseteq> convex hull {x. x extreme_point_of S}"
  1211   proof
  1212     fix a assume [simp]: "a \<in> S"
  1213     have 1: "compact ((+) (- a) ` S)"
  1214       by (simp add: \<open>compact S\<close> compact_translation)
  1215     have 2: "convex ((+) (- a) ` S)"
  1216       by (simp add: \<open>convex S\<close> convex_translation)
  1217     show a_invex: "a \<in> convex hull {x. x extreme_point_of S}"
  1218       using Krein_Milman_Minkowski_aux [OF refl 1 2]
  1219             convex_hull_translation [of "-a"]
  1220       by (auto simp: extreme_points_of_translation translation_assoc)
  1221     qed
  1222 next
  1223   show "convex hull {x. x extreme_point_of S} \<subseteq> S"
  1224   proof -
  1225     have "{a. a extreme_point_of S} \<subseteq> S"
  1226       using extreme_point_of_def by blast
  1227     then show ?thesis
  1228       by (simp add: \<open>convex S\<close> hull_minimal)
  1229   qed
  1230 qed
  1231 
  1232 
  1233 subsection\<open>Applying it to convex hulls of explicitly indicated finite sets\<close>
  1234 
  1235 lemma Krein_Milman_polytope:
  1236   fixes S :: "'a::euclidean_space set"
  1237   shows
  1238    "finite S
  1239        \<Longrightarrow> convex hull S =
  1240            convex hull {x. x extreme_point_of (convex hull S)}"
  1241 by (simp add: Krein_Milman_Minkowski finite_imp_compact_convex_hull)
  1242 
  1243 lemma extreme_points_of_convex_hull_eq:
  1244   fixes S :: "'a::euclidean_space set"
  1245   shows
  1246    "\<lbrakk>compact S; \<And>T. T \<subset> S \<Longrightarrow> convex hull T \<noteq> convex hull S\<rbrakk>
  1247         \<Longrightarrow> {x. x extreme_point_of (convex hull S)} = S"
  1248 by (metis (full_types) Krein_Milman_Minkowski compact_convex_hull convex_convex_hull extreme_points_of_convex_hull psubsetI)
  1249 
  1250 
  1251 lemma extreme_point_of_convex_hull_eq:
  1252   fixes S :: "'a::euclidean_space set"
  1253   shows
  1254    "\<lbrakk>compact S; \<And>T. T \<subset> S \<Longrightarrow> convex hull T \<noteq> convex hull S\<rbrakk>
  1255     \<Longrightarrow> (x extreme_point_of (convex hull S) \<longleftrightarrow> x \<in> S)"
  1256 using extreme_points_of_convex_hull_eq by auto
  1257 
  1258 lemma extreme_point_of_convex_hull_convex_independent:
  1259   fixes S :: "'a::euclidean_space set"
  1260   assumes "compact S" and S: "\<And>a. a \<in> S \<Longrightarrow> a \<notin> convex hull (S - {a})"
  1261   shows "(x extreme_point_of (convex hull S) \<longleftrightarrow> x \<in> S)"
  1262 proof -
  1263   have "convex hull T \<noteq> convex hull S" if "T \<subset> S" for T
  1264   proof -
  1265     obtain a where  "T \<subseteq> S" "a \<in> S" "a \<notin> T" using \<open>T \<subset> S\<close> by blast
  1266     then show ?thesis
  1267       by (metis (full_types) Diff_eq_empty_iff Diff_insert0 S hull_mono hull_subset insert_Diff_single subsetCE)
  1268   qed
  1269   then show ?thesis
  1270     by (rule extreme_point_of_convex_hull_eq [OF \<open>compact S\<close>])
  1271 qed
  1272 
  1273 lemma extreme_point_of_convex_hull_affine_independent:
  1274   fixes S :: "'a::euclidean_space set"
  1275   shows
  1276    "~ affine_dependent S
  1277          \<Longrightarrow> (x extreme_point_of (convex hull S) \<longleftrightarrow> x \<in> S)"
  1278 by (metis aff_independent_finite affine_dependent_def affine_hull_convex_hull extreme_point_of_convex_hull_convex_independent finite_imp_compact hull_inc)
  1279 
  1280 text\<open>Elementary proofs exist, not requiring Euclidean spaces and all this development\<close>
  1281 lemma extreme_point_of_convex_hull_2:
  1282   fixes x :: "'a::euclidean_space"
  1283   shows "x extreme_point_of (convex hull {a,b}) \<longleftrightarrow> x = a \<or> x = b"
  1284 proof -
  1285   have "x extreme_point_of (convex hull {a,b}) \<longleftrightarrow> x \<in> {a,b}"
  1286     by (intro extreme_point_of_convex_hull_affine_independent affine_independent_2)
  1287   then show ?thesis
  1288     by simp
  1289 qed
  1290 
  1291 lemma extreme_point_of_segment:
  1292   fixes x :: "'a::euclidean_space"
  1293   shows
  1294    "x extreme_point_of closed_segment a b \<longleftrightarrow> x = a \<or> x = b"
  1295 by (simp add: extreme_point_of_convex_hull_2 segment_convex_hull)
  1296 
  1297 lemma face_of_convex_hull_subset:
  1298   fixes S :: "'a::euclidean_space set"
  1299   assumes "compact S" and T: "T face_of (convex hull S)"
  1300   obtains s' where "s' \<subseteq> S" "T = convex hull s'"
  1301 apply (rule_tac s' = "{x. x extreme_point_of T}" in that)
  1302 using T extreme_point_of_convex_hull extreme_point_of_face apply blast
  1303 by (metis (no_types) Krein_Milman_Minkowski assms compact_convex_hull convex_convex_hull face_of_imp_compact face_of_imp_convex)
  1304 
  1305 
  1306 lemma face_of_convex_hull_aux:
  1307   assumes eq: "x *\<^sub>R p = u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c"
  1308     and x: "u + v + w = x" "x \<noteq> 0" and S: "affine S" "a \<in> S" "b \<in> S" "c \<in> S"
  1309   shows "p \<in> S"
  1310 proof -
  1311   have "p = (u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c) /\<^sub>R x"
  1312     by (metis \<open>x \<noteq> 0\<close> eq mult.commute right_inverse scaleR_one scaleR_scaleR)
  1313   moreover have "affine hull {a,b,c} \<subseteq> S"
  1314     by (simp add: S hull_minimal)
  1315   moreover have "(u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c) /\<^sub>R x \<in> affine hull {a,b,c}"
  1316     apply (simp add: affine_hull_3)
  1317     apply (rule_tac x="u/x" in exI)
  1318     apply (rule_tac x="v/x" in exI)
  1319     apply (rule_tac x="w/x" in exI)
  1320     using x apply (auto simp: algebra_simps divide_simps)
  1321     done
  1322   ultimately show ?thesis by force
  1323 qed
  1324 
  1325 proposition face_of_convex_hull_insert_eq:
  1326   fixes a :: "'a :: euclidean_space"
  1327   assumes "finite S" and a: "a \<notin> affine hull S"
  1328   shows "(F face_of (convex hull (insert a S)) \<longleftrightarrow>
  1329           F face_of (convex hull S) \<or>
  1330           (\<exists>F'. F' face_of (convex hull S) \<and> F = convex hull (insert a F')))"
  1331          (is "F face_of ?CAS \<longleftrightarrow> _")
  1332 proof safe
  1333   assume F: "F face_of ?CAS"
  1334     and *: "\<nexists>F'. F' face_of convex hull S \<and> F = convex hull insert a F'"
  1335   obtain T where T: "T \<subseteq> insert a S" and FeqT: "F = convex hull T"
  1336     by (metis F \<open>finite S\<close> compact_insert finite_imp_compact face_of_convex_hull_subset)
  1337   show "F face_of convex hull S"
  1338   proof (cases "a \<in> T")
  1339     case True
  1340     have "F = convex hull insert a (convex hull T \<inter> convex hull S)"
  1341     proof
  1342       have "T \<subseteq> insert a (convex hull T \<inter> convex hull S)"
  1343         using T hull_subset by fastforce
  1344       then show "F \<subseteq> convex hull insert a (convex hull T \<inter> convex hull S)"
  1345         by (simp add: FeqT hull_mono)
  1346       show "convex hull insert a (convex hull T \<inter> convex hull S) \<subseteq> F"
  1347         apply (rule hull_minimal)
  1348         using True by (auto simp: \<open>F = convex hull T\<close> hull_inc)
  1349     qed
  1350     moreover have "convex hull T \<inter> convex hull S face_of convex hull S"
  1351       by (metis F FeqT convex_convex_hull face_of_slice hull_mono inf.absorb_iff2 subset_insertI)
  1352     ultimately show ?thesis
  1353       using * by force
  1354   next
  1355     case False
  1356     then show ?thesis
  1357       by (metis FeqT F T face_of_subset hull_mono subset_insert subset_insertI)
  1358   qed
  1359 next
  1360   assume "F face_of convex hull S"
  1361   show "F face_of ?CAS"
  1362     by (simp add: \<open>F face_of convex hull S\<close> a face_of_convex_hull_insert \<open>finite S\<close>)
  1363 next
  1364   fix F
  1365   assume F: "F face_of convex hull S"
  1366   show "convex hull insert a F face_of ?CAS"
  1367   proof (cases "S = {}")
  1368     case True
  1369     then show ?thesis
  1370       using F face_of_affine_eq by auto
  1371   next
  1372     case False
  1373     have anotc: "a \<notin> convex hull S"
  1374       by (metis (no_types) a affine_hull_convex_hull hull_inc)
  1375     show ?thesis
  1376     proof (cases "F = {}")
  1377       case True show ?thesis
  1378         using anotc by (simp add: \<open>F = {}\<close> \<open>finite S\<close> extreme_point_of_convex_hull_insert face_of_singleton)
  1379     next
  1380       case False
  1381       have "convex hull insert a F \<subseteq> ?CAS"
  1382         by (simp add: F a \<open>finite S\<close> convex_hull_subset face_of_convex_hull_insert face_of_imp_subset hull_inc)
  1383       moreover
  1384       have "(\<exists>y v. (1 - ub) *\<^sub>R a + ub *\<^sub>R b = (1 - v) *\<^sub>R a + v *\<^sub>R y \<and>
  1385                    0 \<le> v \<and> v \<le> 1 \<and> y \<in> F) \<and>
  1386             (\<exists>x u. (1 - uc) *\<^sub>R a + uc *\<^sub>R c = (1 - u) *\<^sub>R a + u *\<^sub>R x \<and>
  1387                    0 \<le> u \<and> u \<le> 1 \<and> x \<in> F)"
  1388         if *: "(1 - ux) *\<^sub>R a + ux *\<^sub>R x
  1389                \<in> open_segment ((1 - ub) *\<^sub>R a + ub *\<^sub>R b) ((1 - uc) *\<^sub>R a + uc *\<^sub>R c)"
  1390           and "0 \<le> ub" "ub \<le> 1" "0 \<le> uc" "uc \<le> 1" "0 \<le> ux" "ux \<le> 1"
  1391           and b: "b \<in> convex hull S" and c: "c \<in> convex hull S" and "x \<in> F"
  1392         for b c ub uc ux x
  1393       proof -
  1394         obtain v where ne: "(1 - ub) *\<^sub>R a + ub *\<^sub>R b \<noteq> (1 - uc) *\<^sub>R a + uc *\<^sub>R c"
  1395           and eq: "(1 - ux) *\<^sub>R a + ux *\<^sub>R x =
  1396                     (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)"
  1397           and "0 < v" "v < 1"
  1398           using * by (auto simp: in_segment)
  1399         then have 0: "((1 - ux) - ((1 - v) * (1 - ub) + v * (1 - uc))) *\<^sub>R a +
  1400                       (ux *\<^sub>R x - (((1 - v) * ub) *\<^sub>R b + (v * uc) *\<^sub>R c)) = 0"
  1401           by (auto simp: algebra_simps)
  1402         then have "((1 - ux) - ((1 - v) * (1 - ub) + v * (1 - uc))) *\<^sub>R a =
  1403                    ((1 - v) * ub) *\<^sub>R b + (v * uc) *\<^sub>R c + (-ux) *\<^sub>R x"
  1404           by (auto simp: algebra_simps)
  1405         then have "a \<in> affine hull S" if "1 - ux - ((1 - v) * (1 - ub) + v * (1 - uc)) \<noteq> 0"
  1406           apply (rule face_of_convex_hull_aux)
  1407           using b c that apply (auto simp: algebra_simps)
  1408           using F convex_hull_subset_affine_hull face_of_imp_subset \<open>x \<in> F\<close> apply blast+
  1409           done
  1410         then have "1 - ux - ((1 - v) * (1 - ub) + v * (1 - uc)) = 0"
  1411           using a by blast
  1412         with 0 have equx: "(1 - v) * ub + v * uc = ux"
  1413           and uxx: "ux *\<^sub>R x = (((1 - v) * ub) *\<^sub>R b + (v * uc) *\<^sub>R c)"
  1414           by auto (auto simp: algebra_simps)
  1415         show ?thesis
  1416         proof (cases "uc = 0")
  1417           case True
  1418           then show ?thesis
  1419             using equx 0 \<open>0 \<le> ub\<close> \<open>ub \<le> 1\<close> \<open>v < 1\<close> \<open>x \<in> F\<close>
  1420             apply (auto simp: algebra_simps)
  1421              apply (rule_tac x=x in exI, simp)
  1422              apply (rule_tac x=ub in exI, auto)
  1423              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)
  1424             using \<open>x \<in> F\<close> \<open>uc \<le> 1\<close> apply blast
  1425             done
  1426         next
  1427           case False
  1428           show ?thesis
  1429           proof (cases "ub = 0")
  1430             case True
  1431             then show ?thesis
  1432               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)
  1433           next
  1434             case False
  1435             then have "0 < ub" "0 < uc"
  1436               using \<open>uc \<noteq> 0\<close> \<open>0 \<le> ub\<close> \<open>0 \<le> uc\<close> by auto
  1437             then have "ux \<noteq> 0"
  1438               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)
  1439             have "b \<in> F \<and> c \<in> F"
  1440             proof (cases "b = c")
  1441               case True
  1442               then show ?thesis
  1443                 by (metis \<open>ux \<noteq> 0\<close> equx real_vector.scale_cancel_left scaleR_add_left uxx \<open>x \<in> F\<close>)
  1444             next
  1445               case False
  1446               have "x = (((1 - v) * ub) *\<^sub>R b + (v * uc) *\<^sub>R c) /\<^sub>R ux"
  1447                 by (metis \<open>ux \<noteq> 0\<close> uxx mult.commute right_inverse scaleR_one scaleR_scaleR)
  1448               also have "... = (1 - v * uc / ux) *\<^sub>R b + (v * uc / ux) *\<^sub>R c"
  1449                 using \<open>ux \<noteq> 0\<close> equx apply (auto simp: algebra_simps divide_simps)
  1450                 by (metis add.commute add_diff_eq add_divide_distrib diff_add_cancel scaleR_add_left)
  1451               finally have "x = (1 - v * uc / ux) *\<^sub>R b + (v * uc / ux) *\<^sub>R c" .
  1452               then have "x \<in> open_segment b c"
  1453                 apply (simp add: in_segment \<open>b \<noteq> c\<close>)
  1454                 apply (rule_tac x="(v * uc) / ux" in exI)
  1455                 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
  1456                 apply (force simp: algebra_simps divide_simps)
  1457                 done
  1458               then show ?thesis
  1459                 by (rule face_ofD [OF F _ b c \<open>x \<in> F\<close>])
  1460             qed
  1461             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
  1462           qed
  1463         qed
  1464       qed
  1465       moreover have "convex hull F = F"
  1466         by (meson F convex_hull_eq face_of_imp_convex)
  1467       ultimately show ?thesis
  1468         unfolding face_of_def by (fastforce simp: convex_hull_insert_alt \<open>S \<noteq> {}\<close> \<open>F \<noteq> {}\<close>)
  1469     qed
  1470   qed
  1471 qed
  1472 
  1473 lemma face_of_convex_hull_insert2:
  1474   fixes a :: "'a :: euclidean_space"
  1475   assumes S: "finite S" and a: "a \<notin> affine hull S" and F: "F face_of convex hull S"
  1476   shows "convex hull (insert a F) face_of convex hull (insert a S)"
  1477   by (metis F face_of_convex_hull_insert_eq [OF S a])
  1478 
  1479 proposition face_of_convex_hull_affine_independent:
  1480   fixes S :: "'a::euclidean_space set"
  1481   assumes "~ affine_dependent S"
  1482     shows "(T face_of (convex hull S) \<longleftrightarrow> (\<exists>c. c \<subseteq> S \<and> T = convex hull c))"
  1483           (is "?lhs = ?rhs")
  1484 proof
  1485   assume ?lhs
  1486   then show ?rhs
  1487     by (meson \<open>T face_of convex hull S\<close> aff_independent_finite assms face_of_convex_hull_subset finite_imp_compact)
  1488 next
  1489   assume ?rhs
  1490   then obtain c where "c \<subseteq> S" and T: "T = convex hull c"
  1491     by blast
  1492   have "affine hull c \<inter> affine hull (S - c) = {}"
  1493     apply (rule disjoint_affine_hull [OF assms \<open>c \<subseteq> S\<close>], auto)
  1494     done
  1495   then have "affine hull c \<inter> convex hull (S - c) = {}"
  1496     using convex_hull_subset_affine_hull by fastforce
  1497   then show ?lhs
  1498     by (metis face_of_convex_hulls \<open>c \<subseteq> S\<close> aff_independent_finite assms T)
  1499 qed
  1500 
  1501 lemma facet_of_convex_hull_affine_independent:
  1502   fixes S :: "'a::euclidean_space set"
  1503   assumes "~ affine_dependent S"
  1504     shows "T facet_of (convex hull S) \<longleftrightarrow>
  1505            T \<noteq> {} \<and> (\<exists>u. u \<in> S \<and> T = convex hull (S - {u}))"
  1506           (is "?lhs = ?rhs")
  1507 proof
  1508   assume ?lhs
  1509   then have "T face_of (convex hull S)" "T \<noteq> {}"
  1510         and afft: "aff_dim T = aff_dim (convex hull S) - 1"
  1511     by (auto simp: facet_of_def)
  1512   then obtain c where "c \<subseteq> S" and c: "T = convex hull c"
  1513     by (auto simp: face_of_convex_hull_affine_independent [OF assms])
  1514   then have affs: "aff_dim S = aff_dim c + 1"
  1515     by (metis aff_dim_convex_hull afft eq_diff_eq)
  1516   have "~ affine_dependent c"
  1517     using \<open>c \<subseteq> S\<close> affine_dependent_subset assms by blast
  1518   with affs have "card (S - c) = 1"
  1519     apply (simp add: aff_dim_affine_independent [symmetric] aff_dim_convex_hull)
  1520     by (metis aff_dim_affine_independent aff_independent_finite One_nat_def \<open>c \<subseteq> S\<close> add.commute
  1521                 add_diff_cancel_right' assms card_Diff_subset card_mono of_nat_1 of_nat_diff of_nat_eq_iff)
  1522   then obtain u where u: "u \<in> S - c"
  1523     by (metis DiffI \<open>c \<subseteq> S\<close> aff_independent_finite assms cancel_comm_monoid_add_class.diff_cancel
  1524                 card_Diff_subset subsetI subset_antisym zero_neq_one)
  1525   then have u: "S = insert u c"
  1526     by (metis Diff_subset \<open>c \<subseteq> S\<close> \<open>card (S - c) = 1\<close> card_1_singletonE double_diff insert_Diff insert_subset singletonD)
  1527   have "T = convex hull (c - {u})"
  1528     by (metis Diff_empty Diff_insert0 \<open>T facet_of convex hull S\<close> c facet_of_irrefl insert_absorb u)
  1529   with \<open>T \<noteq> {}\<close> show ?rhs
  1530     using c u by auto
  1531 next
  1532   assume ?rhs
  1533   then obtain u where "T \<noteq> {}" "u \<in> S" and u: "T = convex hull (S - {u})"
  1534     by (force simp: facet_of_def)
  1535   then have "\<not> S \<subseteq> {u}"
  1536     using \<open>T \<noteq> {}\<close> u by auto
  1537   have [simp]: "aff_dim (convex hull (S - {u})) = aff_dim (convex hull S) - 1"
  1538     using assms \<open>u \<in> S\<close>
  1539     apply (simp add: aff_dim_convex_hull affine_dependent_def)
  1540     apply (drule bspec, assumption)
  1541     by (metis add_diff_cancel_right' aff_dim_insert insert_Diff [of u S])
  1542   show ?lhs
  1543     apply (subst u)
  1544     apply (simp add: \<open>\<not> S \<subseteq> {u}\<close> facet_of_def face_of_convex_hull_affine_independent [OF assms], blast)
  1545     done
  1546 qed
  1547 
  1548 lemma facet_of_convex_hull_affine_independent_alt:
  1549   fixes S :: "'a::euclidean_space set"
  1550   shows
  1551    "~affine_dependent S
  1552         \<Longrightarrow> (T facet_of (convex hull S) \<longleftrightarrow>
  1553              2 \<le> card S \<and> (\<exists>u. u \<in> S \<and> T = convex hull (S - {u})))"
  1554 apply (simp add: facet_of_convex_hull_affine_independent)
  1555 apply (auto simp: Set.subset_singleton_iff)
  1556 apply (metis Diff_cancel Int_empty_right Int_insert_right_if1  aff_independent_finite card_eq_0_iff card_insert_if card_mono card_subset_eq convex_hull_eq_empty eq_iff equals0D finite_insert finite_subset inf.absorb_iff2 insert_absorb insert_not_empty  not_less_eq_eq numeral_2_eq_2)
  1557 done
  1558 
  1559 lemma segment_face_of:
  1560   assumes "(closed_segment a b) face_of S"
  1561   shows "a extreme_point_of S" "b extreme_point_of S"
  1562 proof -
  1563   have as: "{a} face_of S"
  1564     by (metis (no_types) assms convex_hull_singleton empty_iff extreme_point_of_convex_hull_insert face_of_face face_of_singleton finite.emptyI finite.insertI insert_absorb insert_iff segment_convex_hull)
  1565   moreover have "{b} face_of S"
  1566   proof -
  1567     have "b \<in> convex hull {a} \<or> b extreme_point_of convex hull {b, a}"
  1568       by (meson extreme_point_of_convex_hull_insert finite.emptyI finite.insertI)
  1569     moreover have "closed_segment a b = convex hull {b, a}"
  1570       using closed_segment_commute segment_convex_hull by blast
  1571     ultimately show ?thesis
  1572       by (metis as assms face_of_face convex_hull_singleton empty_iff face_of_singleton insertE)
  1573     qed
  1574   ultimately show "a extreme_point_of S" "b extreme_point_of S"
  1575     using face_of_singleton by blast+
  1576 qed
  1577 
  1578 
  1579 lemma Krein_Milman_frontier:
  1580   fixes S :: "'a::euclidean_space set"
  1581   assumes "convex S" "compact S"
  1582     shows "S = convex hull (frontier S)"
  1583           (is "?lhs = ?rhs")
  1584 proof
  1585   have "?lhs \<subseteq> convex hull {x. x extreme_point_of S}"
  1586     using Krein_Milman_Minkowski assms by blast
  1587   also have "... \<subseteq> ?rhs"
  1588     apply (rule hull_mono)
  1589     apply (auto simp: frontier_def extreme_point_not_in_interior)
  1590     using closure_subset apply (force simp: extreme_point_of_def)
  1591     done
  1592   finally show "?lhs \<subseteq> ?rhs" .
  1593 next
  1594   have "?rhs \<subseteq> convex hull S"
  1595     by (metis Diff_subset \<open>compact S\<close> closure_closed compact_eq_bounded_closed frontier_def hull_mono)
  1596   also have "... \<subseteq> ?lhs"
  1597     by (simp add: \<open>convex S\<close> hull_same)
  1598   finally show "?rhs \<subseteq> ?lhs" .
  1599 qed
  1600 
  1601 subsection\<open>Polytopes\<close>
  1602 
  1603 definition polytope where
  1604  "polytope S \<equiv> \<exists>v. finite v \<and> S = convex hull v"
  1605 
  1606 lemma polytope_translation_eq: "polytope (image (\<lambda>x. a + x) S) \<longleftrightarrow> polytope S"
  1607 apply (simp add: polytope_def, safe)
  1608 apply (metis convex_hull_translation finite_imageI translation_galois)
  1609 by (metis convex_hull_translation finite_imageI)
  1610 
  1611 lemma polytope_linear_image: "\<lbrakk>linear f; polytope p\<rbrakk> \<Longrightarrow> polytope(image f p)"
  1612   unfolding polytope_def using convex_hull_linear_image by blast
  1613 
  1614 lemma polytope_empty: "polytope {}"
  1615   using convex_hull_empty polytope_def by blast
  1616 
  1617 lemma polytope_convex_hull: "finite S \<Longrightarrow> polytope(convex hull S)"
  1618   using polytope_def by auto
  1619 
  1620 lemma polytope_Times: "\<lbrakk>polytope S; polytope T\<rbrakk> \<Longrightarrow> polytope(S \<times> T)"
  1621   unfolding polytope_def
  1622   by (metis finite_cartesian_product convex_hull_Times)
  1623 
  1624 lemma face_of_polytope_polytope:
  1625   fixes S :: "'a::euclidean_space set"
  1626   shows "\<lbrakk>polytope S; F face_of S\<rbrakk> \<Longrightarrow> polytope F"
  1627 unfolding polytope_def
  1628 by (meson face_of_convex_hull_subset finite_imp_compact finite_subset)
  1629 
  1630 lemma finite_polytope_faces:
  1631   fixes S :: "'a::euclidean_space set"
  1632   assumes "polytope S"
  1633   shows "finite {F. F face_of S}"
  1634 proof -
  1635   obtain v where "finite v" "S = convex hull v"
  1636     using assms polytope_def by auto
  1637   have "finite ((hull) convex ` {T. T \<subseteq> v})"
  1638     by (simp add: \<open>finite v\<close>)
  1639   moreover have "{F. F face_of S} \<subseteq> ((hull) convex ` {T. T \<subseteq> v})"
  1640     by (metis (no_types, lifting) \<open>finite v\<close> \<open>S = convex hull v\<close> face_of_convex_hull_subset finite_imp_compact image_eqI mem_Collect_eq subsetI)
  1641   ultimately show ?thesis
  1642     by (blast intro: finite_subset)
  1643 qed
  1644 
  1645 lemma finite_polytope_facets:
  1646   assumes "polytope S"
  1647   shows "finite {T. T facet_of S}"
  1648 by (simp add: assms facet_of_def finite_polytope_faces)
  1649 
  1650 lemma polytope_scaling:
  1651   assumes "polytope S"  shows "polytope (image (\<lambda>x. c *\<^sub>R x) S)"
  1652 by (simp add: assms polytope_linear_image)
  1653 
  1654 lemma polytope_imp_compact:
  1655   fixes S :: "'a::real_normed_vector set"
  1656   shows "polytope S \<Longrightarrow> compact S"
  1657 by (metis finite_imp_compact_convex_hull polytope_def)
  1658 
  1659 lemma polytope_imp_convex: "polytope S \<Longrightarrow> convex S"
  1660   by (metis convex_convex_hull polytope_def)
  1661 
  1662 lemma polytope_imp_closed:
  1663   fixes S :: "'a::real_normed_vector set"
  1664   shows "polytope S \<Longrightarrow> closed S"
  1665 by (simp add: compact_imp_closed polytope_imp_compact)
  1666 
  1667 lemma polytope_imp_bounded:
  1668   fixes S :: "'a::real_normed_vector set"
  1669   shows "polytope S \<Longrightarrow> bounded S"
  1670 by (simp add: compact_imp_bounded polytope_imp_compact)
  1671 
  1672 lemma polytope_interval: "polytope(cbox a b)"
  1673   unfolding polytope_def by (meson closed_interval_as_convex_hull)
  1674 
  1675 lemma polytope_sing: "polytope {a}"
  1676   using polytope_def by force
  1677 
  1678 lemma face_of_polytope_insert:
  1679      "\<lbrakk>polytope S; a \<notin> affine hull S; F face_of S\<rbrakk> \<Longrightarrow> F face_of convex hull (insert a S)"
  1680   by (metis (no_types, lifting) affine_hull_convex_hull face_of_convex_hull_insert hull_insert polytope_def)
  1681 
  1682 lemma face_of_polytope_insert2:
  1683   fixes a :: "'a :: euclidean_space"
  1684   assumes "polytope S" "a \<notin> affine hull S" "F face_of S"
  1685   shows "convex hull (insert a F) face_of convex hull (insert a S)"
  1686 proof -
  1687   obtain V where "finite V" "S = convex hull V"
  1688     using assms by (auto simp: polytope_def)
  1689   then have "convex hull (insert a F) face_of convex hull (insert a V)"
  1690     using affine_hull_convex_hull assms face_of_convex_hull_insert2 by blast
  1691   then show ?thesis
  1692     by (metis \<open>S = convex hull V\<close> hull_insert)
  1693 qed
  1694 
  1695 
  1696 subsection\<open>Polyhedra\<close>
  1697 
  1698 definition polyhedron where
  1699  "polyhedron S \<equiv>
  1700         \<exists>F. finite F \<and>
  1701             S = \<Inter> F \<and>
  1702             (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b})"
  1703 
  1704 lemma polyhedron_Int [intro,simp]:
  1705    "\<lbrakk>polyhedron S; polyhedron T\<rbrakk> \<Longrightarrow> polyhedron (S \<inter> T)"
  1706   apply (simp add: polyhedron_def, clarify)
  1707   apply (rename_tac F G)
  1708   apply (rule_tac x="F \<union> G" in exI, auto)
  1709   done
  1710 
  1711 lemma polyhedron_UNIV [iff]: "polyhedron UNIV"
  1712   unfolding polyhedron_def
  1713   by (rule_tac x="{}" in exI) auto
  1714 
  1715 lemma polyhedron_Inter [intro,simp]:
  1716    "\<lbrakk>finite F; \<And>S. S \<in> F \<Longrightarrow> polyhedron S\<rbrakk> \<Longrightarrow> polyhedron(\<Inter>F)"
  1717 by (induction F rule: finite_induct) auto
  1718 
  1719 
  1720 lemma polyhedron_empty [iff]: "polyhedron ({} :: 'a :: euclidean_space set)"
  1721 proof -
  1722   have "\<exists>a. a \<noteq> 0 \<and>
  1723              (\<exists>b. {x. (SOME i. i \<in> Basis) \<bullet> x \<le> - 1} = {x. a \<bullet> x \<le> b})"
  1724     by (rule_tac x="(SOME i. i \<in> Basis)" in exI) (force simp: SOME_Basis nonzero_Basis)
  1725   moreover have "\<exists>a b. a \<noteq> 0 \<and>
  1726                        {x. - (SOME i. i \<in> Basis) \<bullet> x \<le> - 1} = {x. a \<bullet> x \<le> b}"
  1727       apply (rule_tac x="-(SOME i. i \<in> Basis)" in exI)
  1728       apply (rule_tac x="-1" in exI)
  1729       apply (simp add: SOME_Basis nonzero_Basis)
  1730       done
  1731   ultimately show ?thesis
  1732     unfolding polyhedron_def
  1733     apply (rule_tac x="{{x. (SOME i. i \<in> Basis) \<bullet> x \<le> -1},
  1734                         {x. -(SOME i. i \<in> Basis) \<bullet> x \<le> -1}}" in exI)
  1735     apply force
  1736     done
  1737 qed
  1738 
  1739 lemma polyhedron_halfspace_le:
  1740   fixes a :: "'a :: euclidean_space"
  1741   shows "polyhedron {x. a \<bullet> x \<le> b}"
  1742 proof (cases "a = 0")
  1743   case True then show ?thesis by auto
  1744 next
  1745   case False
  1746   then show ?thesis
  1747     unfolding polyhedron_def
  1748     by (rule_tac x="{{x. a \<bullet> x \<le> b}}" in exI) auto
  1749 qed
  1750 
  1751 lemma polyhedron_halfspace_ge:
  1752   fixes a :: "'a :: euclidean_space"
  1753   shows "polyhedron {x. a \<bullet> x \<ge> b}"
  1754 using polyhedron_halfspace_le [of "-a" "-b"] by simp
  1755 
  1756 lemma polyhedron_hyperplane:
  1757   fixes a :: "'a :: euclidean_space"
  1758   shows "polyhedron {x. a \<bullet> x = b}"
  1759 proof -
  1760   have "{x. a \<bullet> x = b} = {x. a \<bullet> x \<le> b} \<inter> {x. a \<bullet> x \<ge> b}"
  1761     by force
  1762   then show ?thesis
  1763     by (simp add: polyhedron_halfspace_ge polyhedron_halfspace_le)
  1764 qed
  1765 
  1766 lemma affine_imp_polyhedron:
  1767   fixes S :: "'a :: euclidean_space set"
  1768   shows "affine S \<Longrightarrow> polyhedron S"
  1769 by (metis affine_hull_eq polyhedron_Inter polyhedron_hyperplane affine_hull_finite_intersection_hyperplanes [of S])
  1770 
  1771 lemma polyhedron_imp_closed:
  1772   fixes S :: "'a :: euclidean_space set"
  1773   shows "polyhedron S \<Longrightarrow> closed S"
  1774 apply (simp add: polyhedron_def)
  1775 using closed_halfspace_le by fastforce
  1776 
  1777 lemma polyhedron_imp_convex:
  1778   fixes S :: "'a :: euclidean_space set"
  1779   shows "polyhedron S \<Longrightarrow> convex S"
  1780 apply (simp add: polyhedron_def)
  1781 using convex_Inter convex_halfspace_le by fastforce
  1782 
  1783 lemma polyhedron_affine_hull:
  1784   fixes S :: "'a :: euclidean_space set"
  1785   shows "polyhedron(affine hull S)"
  1786 by (simp add: affine_imp_polyhedron)
  1787 
  1788 
  1789 subsection\<open>Canonical polyhedron representation making facial structure explicit\<close>
  1790 
  1791 lemma polyhedron_Int_affine:
  1792   fixes S :: "'a :: euclidean_space set"
  1793   shows "polyhedron S \<longleftrightarrow>
  1794            (\<exists>F. finite F \<and> S = (affine hull S) \<inter> \<Inter>F \<and>
  1795                 (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}))"
  1796         (is "?lhs = ?rhs")
  1797 proof
  1798   assume ?lhs then show ?rhs
  1799     apply (simp add: polyhedron_def)
  1800     apply (erule ex_forward)
  1801     using hull_subset apply force
  1802     done
  1803 next
  1804   assume ?rhs then show ?lhs
  1805     apply clarify
  1806     apply (erule ssubst)
  1807     apply (force intro: polyhedron_affine_hull polyhedron_halfspace_le)
  1808     done
  1809 qed
  1810 
  1811 proposition rel_interior_polyhedron_explicit:
  1812   assumes "finite F"
  1813       and seq: "S = affine hull S \<inter> \<Inter>F"
  1814       and faceq: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
  1815       and psub: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> affine hull S \<inter> \<Inter>F'"
  1816     shows "rel_interior S = {x \<in> S. \<forall>h \<in> F. a h \<bullet> x < b h}"
  1817 proof -
  1818   have rels: "\<And>x. x \<in> rel_interior S \<Longrightarrow> x \<in> S"
  1819     by (meson IntE mem_rel_interior)
  1820   moreover have "a i \<bullet> x < b i" if x: "x \<in> rel_interior S" and "i \<in> F" for x i
  1821   proof -
  1822     have fif: "F - {i} \<subset> F"
  1823       using \<open>i \<in> F\<close> Diff_insert_absorb Diff_subset set_insert psubsetI by blast
  1824     then have "S \<subset> affine hull S \<inter> \<Inter>(F - {i})"
  1825       by (rule psub)
  1826     then obtain z where ssub: "S \<subseteq> \<Inter>(F - {i})" and zint: "z \<in> \<Inter>(F - {i})"
  1827                     and "z \<notin> S" and zaff: "z \<in> affine hull S"
  1828       by auto
  1829     have "z \<noteq> x"
  1830       using \<open>z \<notin> S\<close> rels x by blast
  1831     have "z \<notin> affine hull S \<inter> \<Inter>F"
  1832       using \<open>z \<notin> S\<close> seq by auto
  1833     then have aiz: "a i \<bullet> z > b i"
  1834       using faceq zint zaff by fastforce
  1835     obtain e where "e > 0" "x \<in> S" and e: "ball x e \<inter> affine hull S \<subseteq> S"
  1836       using x by (auto simp: mem_rel_interior_ball)
  1837     then have ins: "\<And>y. \<lbrakk>norm (x - y) < e; y \<in> affine hull S\<rbrakk> \<Longrightarrow> y \<in> S"
  1838       by (metis IntI subsetD dist_norm mem_ball)
  1839     define \<xi> where "\<xi> = min (1/2) (e / 2 / norm(z - x))"
  1840     have "norm (\<xi> *\<^sub>R x - \<xi> *\<^sub>R z) = norm (\<xi> *\<^sub>R (x - z))"
  1841       by (simp add: \<xi>_def algebra_simps norm_mult)
  1842     also have "... = \<xi> * norm (x - z)"
  1843       using \<open>e > 0\<close> by (simp add: \<xi>_def)
  1844     also have "... < e"
  1845       using \<open>z \<noteq> x\<close> \<open>e > 0\<close> by (simp add: \<xi>_def min_def divide_simps norm_minus_commute)
  1846     finally have lte: "norm (\<xi> *\<^sub>R x - \<xi> *\<^sub>R z) < e" .
  1847     have \<xi>_aff: "\<xi> *\<^sub>R z + (1 - \<xi>) *\<^sub>R x \<in> affine hull S"
  1848       by (metis \<open>x \<in> S\<close> add.commute affine_affine_hull diff_add_cancel hull_inc mem_affine zaff)
  1849     have "\<xi> *\<^sub>R z + (1 - \<xi>) *\<^sub>R x \<in> S"
  1850       apply (rule ins [OF _ \<xi>_aff])
  1851       apply (simp add: algebra_simps lte)
  1852       done
  1853     then obtain l where l: "0 < l" "l < 1" and ls: "(l *\<^sub>R z + (1 - l) *\<^sub>R x) \<in> S"
  1854       apply (rule_tac l = \<xi> in that)
  1855       using \<open>e > 0\<close> \<open>z \<noteq> x\<close>  apply (auto simp: \<xi>_def)
  1856       done
  1857     then have i: "l *\<^sub>R z + (1 - l) *\<^sub>R x \<in> i"
  1858       using seq \<open>i \<in> F\<close> by auto
  1859     have "b i * l + (a i \<bullet> x) * (1 - l) < a i \<bullet> (l *\<^sub>R z + (1 - l) *\<^sub>R x)"
  1860       using l by (simp add: algebra_simps aiz)
  1861     also have "\<dots> \<le> b i" using i l
  1862       using faceq mem_Collect_eq \<open>i \<in> F\<close> by blast
  1863     finally have "(a i \<bullet> x) * (1 - l) < b i * (1 - l)"
  1864       by (simp add: algebra_simps)
  1865     with l show ?thesis
  1866       by simp
  1867   qed
  1868   moreover have "x \<in> rel_interior S"
  1869            if "x \<in> S" and less: "\<And>h. h \<in> F \<Longrightarrow> a h \<bullet> x < b h" for x
  1870   proof -
  1871     have 1: "\<And>h. h \<in> F \<Longrightarrow> x \<in> interior h"
  1872       by (metis interior_halfspace_le mem_Collect_eq less faceq)
  1873     have 2: "\<And>y. \<lbrakk>\<forall>h\<in>F. y \<in> interior h; y \<in> affine hull S\<rbrakk> \<Longrightarrow> y \<in> S"
  1874       by (metis IntI Inter_iff contra_subsetD interior_subset seq)
  1875     show ?thesis
  1876       apply (simp add: rel_interior \<open>x \<in> S\<close>)
  1877       apply (rule_tac x="\<Inter>h\<in>F. interior h" in exI)
  1878       apply (auto simp: \<open>finite F\<close> open_INT 1 2)
  1879       done
  1880   qed
  1881   ultimately show ?thesis by blast
  1882 qed
  1883 
  1884 
  1885 lemma polyhedron_Int_affine_parallel:
  1886   fixes S :: "'a :: euclidean_space set"
  1887   shows "polyhedron S \<longleftrightarrow>
  1888          (\<exists>F. finite F \<and>
  1889               S = (affine hull S) \<inter> (\<Inter>F) \<and>
  1890               (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b} \<and>
  1891                              (\<forall>x \<in> affine hull S. (x + a) \<in> affine hull S)))"
  1892     (is "?lhs = ?rhs")
  1893 proof
  1894   assume ?lhs
  1895   then obtain F where "finite F" and seq: "S = (affine hull S) \<inter> \<Inter>F"
  1896                   and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
  1897     by (fastforce simp add: polyhedron_Int_affine)
  1898   then obtain a b where ab: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
  1899     by metis
  1900   show ?rhs
  1901   proof -
  1902     have "\<exists>a' b'. a' \<noteq> 0 \<and>
  1903                   affine hull S \<inter> {x. a' \<bullet> x \<le> b'} = affine hull S \<inter> h \<and>
  1904                   (\<forall>w \<in> affine hull S. (w + a') \<in> affine hull S)"
  1905         if "h \<in> F" "~(affine hull S \<subseteq> h)" for h
  1906     proof -
  1907       have "a h \<noteq> 0" and "h = {x. a h \<bullet> x \<le> b h}" "h \<inter> \<Inter>F = \<Inter>F"
  1908         using \<open>h \<in> F\<close> ab by auto
  1909       then have "(affine hull S) \<inter> {x. a h \<bullet> x \<le> b h} \<noteq> {}"
  1910         by (metis (no_types) affine_hull_eq_empty inf.absorb_iff2 inf_assoc inf_bot_right inf_commute seq that(2))
  1911       moreover have "~ (affine hull S \<subseteq> {x. a h \<bullet> x \<le> b h})"
  1912         using \<open>h = {x. a h \<bullet> x \<le> b h}\<close> that(2) by blast
  1913       ultimately show ?thesis
  1914         using affine_parallel_slice [of "affine hull S"]
  1915         by (metis \<open>h = {x. a h \<bullet> x \<le> b h}\<close> affine_affine_hull)
  1916     qed
  1917     then obtain a b
  1918          where ab: "\<And>h. \<lbrakk>h \<in> F; ~ (affine hull S \<subseteq> h)\<rbrakk>
  1919              \<Longrightarrow> a h \<noteq> 0 \<and>
  1920                   affine hull S \<inter> {x. a h \<bullet> x \<le> b h} = affine hull S \<inter> h \<and>
  1921                   (\<forall>w \<in> affine hull S. (w + a h) \<in> affine hull S)"
  1922       by metis
  1923     have seq2: "S = affine hull S \<inter> (\<Inter>h\<in>{h \<in> F. \<not> affine hull S \<subseteq> h}. {x. a h \<bullet> x \<le> b h})"
  1924       by (subst seq) (auto simp: ab INT_extend_simps)
  1925     show ?thesis
  1926       apply (rule_tac x="(\<lambda>h. {x. a h \<bullet> x \<le> b h}) ` {h. h \<in> F \<and> ~(affine hull S \<subseteq> h)}" in exI)
  1927       apply (intro conjI seq2)
  1928         using \<open>finite F\<close> apply force
  1929        using ab apply blast
  1930        done
  1931   qed
  1932 next
  1933   assume ?rhs then show ?lhs
  1934     apply (simp add: polyhedron_Int_affine)
  1935     by metis
  1936 qed
  1937 
  1938 
  1939 proposition polyhedron_Int_affine_parallel_minimal:
  1940   fixes S :: "'a :: euclidean_space set"
  1941   shows "polyhedron S \<longleftrightarrow>
  1942          (\<exists>F. finite F \<and>
  1943               S = (affine hull S) \<inter> (\<Inter>F) \<and>
  1944               (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b} \<and>
  1945                              (\<forall>x \<in> affine hull S. (x + a) \<in> affine hull S)) \<and>
  1946               (\<forall>F'. F' \<subset> F \<longrightarrow> S \<subset> (affine hull S) \<inter> (\<Inter>F')))"
  1947     (is "?lhs = ?rhs")
  1948 proof
  1949   assume ?lhs
  1950   then obtain f0
  1951            where f0: "finite f0"
  1952                  "S = (affine hull S) \<inter> (\<Inter>f0)"
  1953                    (is "?P f0")
  1954                  "\<forall>h \<in> f0. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b} \<and>
  1955                              (\<forall>x \<in> affine hull S. (x + a) \<in> affine hull S)"
  1956                    (is "?Q f0")
  1957     by (force simp: polyhedron_Int_affine_parallel)
  1958   define n where "n = (LEAST n. \<exists>F. card F = n \<and> finite F \<and> ?P F \<and> ?Q F)"
  1959   have nf: "\<exists>F. card F = n \<and> finite F \<and> ?P F \<and> ?Q F"
  1960     apply (simp add: n_def)
  1961     apply (rule LeastI [where k = "card f0"])
  1962     using f0 apply auto
  1963     done
  1964   then obtain F where F: "card F = n" "finite F" and seq: "?P F" and aff: "?Q F"
  1965     by blast
  1966   then have "~ (finite g \<and> ?P g \<and> ?Q g)" if "card g < n" for g
  1967     using that by (auto simp: n_def dest!: not_less_Least)
  1968   then have *: "~ (?P g \<and> ?Q g)" if "g \<subset> F" for g
  1969     using that \<open>finite F\<close> psubset_card_mono \<open>card F = n\<close>
  1970     by (metis finite_Int inf.strict_order_iff)
  1971   have 1: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subseteq> affine hull S \<inter> \<Inter>F'"
  1972     by (subst seq) blast
  1973   have 2: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<noteq> affine hull S \<inter> \<Inter>F'"
  1974     apply (frule *)
  1975     by (metis aff subsetCE subset_iff_psubset_eq)
  1976   show ?rhs
  1977     by (metis \<open>finite F\<close> seq aff psubsetI 1 2)
  1978 next
  1979   assume ?rhs then show ?lhs
  1980     by (auto simp: polyhedron_Int_affine_parallel)
  1981 qed
  1982 
  1983 
  1984 lemma polyhedron_Int_affine_minimal:
  1985   fixes S :: "'a :: euclidean_space set"
  1986   shows "polyhedron S \<longleftrightarrow>
  1987          (\<exists>F. finite F \<and> S = (affine hull S) \<inter> \<Inter>F \<and>
  1988               (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}) \<and>
  1989               (\<forall>F'. F' \<subset> F \<longrightarrow> S \<subset> (affine hull S) \<inter> \<Inter>F'))"
  1990 apply (rule iffI)
  1991  apply (force simp: polyhedron_Int_affine_parallel_minimal elim!: ex_forward)
  1992 apply (auto simp: polyhedron_Int_affine elim!: ex_forward)
  1993 done
  1994 
  1995 proposition facet_of_polyhedron_explicit:
  1996   assumes "finite F"
  1997       and seq: "S = affine hull S \<inter> \<Inter>F"
  1998       and faceq: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
  1999       and psub: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> affine hull S \<inter> \<Inter>F'"
  2000     shows "c facet_of S \<longleftrightarrow> (\<exists>h. h \<in> F \<and> c = S \<inter> {x. a h \<bullet> x = b h})"
  2001 proof (cases "S = {}")
  2002   case True with psub show ?thesis by force
  2003 next
  2004   case False
  2005   have "polyhedron S"
  2006     apply (simp add: polyhedron_Int_affine)
  2007     apply (rule_tac x=F in exI)
  2008     using assms  apply force
  2009     done
  2010   then have "convex S"
  2011     by (rule polyhedron_imp_convex)
  2012   with False rel_interior_eq_empty have "rel_interior S \<noteq> {}" by blast
  2013   then obtain x where "x \<in> rel_interior S" by auto
  2014   then obtain T where "open T" "x \<in> T" "x \<in> S" "T \<inter> affine hull S \<subseteq> S"
  2015     by (force simp: mem_rel_interior)
  2016   then have xaff: "x \<in> affine hull S" and xint: "x \<in> \<Inter>F"
  2017     using seq hull_inc by auto
  2018   have "rel_interior S = {x \<in> S. \<forall>h\<in>F. a h \<bullet> x < b h}"
  2019     by (rule rel_interior_polyhedron_explicit [OF \<open>finite F\<close> seq faceq psub])
  2020   with \<open>x \<in> rel_interior S\<close>
  2021   have [simp]: "\<And>h. h\<in>F \<Longrightarrow> a h \<bullet> x < b h" by blast
  2022   have *: "(S \<inter> {x. a h \<bullet> x = b h}) facet_of S" if "h \<in> F" for h
  2023   proof -
  2024     have "S \<subset> affine hull S \<inter> \<Inter>(F - {h})"
  2025       using psub that by (metis Diff_disjoint Diff_subset insert_disjoint(2) psubsetI)
  2026     then obtain z where zaff: "z \<in> affine hull S" and zint: "z \<in> \<Inter>(F - {h})" and "z \<notin> S"
  2027       by force
  2028     then have "z \<noteq> x" "z \<notin> h" using seq \<open>x \<in> S\<close> by auto
  2029     have "x \<in> h" using that xint by auto
  2030     then have able: "a h \<bullet> x \<le> b h"
  2031       using faceq that by blast
  2032     also have "... < a h \<bullet> z" using \<open>z \<notin> h\<close> faceq [OF that] xint by auto
  2033     finally have xltz: "a h \<bullet> x < a h \<bullet> z" .
  2034     define l where "l = (b h - a h \<bullet> x) / (a h \<bullet> z - a h \<bullet> x)"
  2035     define w where "w = (1 - l) *\<^sub>R x + l *\<^sub>R z"
  2036     have "0 < l" "l < 1"
  2037       using able xltz \<open>b h < a h \<bullet> z\<close> \<open>h \<in> F\<close>
  2038       by (auto simp: l_def divide_simps)
  2039     have awlt: "a i \<bullet> w < b i" if "i \<in> F" "i \<noteq> h" for i
  2040     proof -
  2041       have "(1 - l) * (a i \<bullet> x) < (1 - l) * b i"
  2042         by (simp add: \<open>l < 1\<close> \<open>i \<in> F\<close>)
  2043       moreover have "l * (a i \<bullet> z) \<le> l * b i"
  2044         apply (rule mult_left_mono)
  2045         apply (metis Diff_insert_absorb Inter_iff Set.set_insert \<open>h \<in> F\<close> faceq insertE mem_Collect_eq that zint)
  2046         using \<open>0 < l\<close>
  2047         apply simp
  2048         done
  2049       ultimately show ?thesis by (simp add: w_def algebra_simps)
  2050     qed
  2051     have weq: "a h \<bullet> w = b h"
  2052       using xltz unfolding w_def l_def
  2053       by (simp add: algebra_simps) (simp add: field_simps)
  2054     have "w \<in> affine hull S"
  2055       by (simp add: w_def mem_affine xaff zaff)
  2056     moreover have "w \<in> \<Inter>F"
  2057       using \<open>a h \<bullet> w = b h\<close> awlt faceq less_eq_real_def by blast
  2058     ultimately have "w \<in> S"
  2059       using seq by blast
  2060     with weq have "S \<inter> {x. a h \<bullet> x = b h} \<noteq> {}" by blast
  2061     moreover have "S \<inter> {x. a h \<bullet> x = b h} face_of S"
  2062       apply (rule face_of_Int_supporting_hyperplane_le)
  2063       apply (rule \<open>convex S\<close>)
  2064       apply (subst (asm) seq)
  2065       using faceq that apply fastforce
  2066       done
  2067     moreover have "affine hull (S \<inter> {x. a h \<bullet> x = b h}) =
  2068                    (affine hull S) \<inter> {x. a h \<bullet> x = b h}"
  2069     proof
  2070       show "affine hull (S \<inter> {x. a h \<bullet> x = b h}) \<subseteq> affine hull S \<inter> {x. a h \<bullet> x = b h}"
  2071         apply (intro Int_greatest hull_mono Int_lower1)
  2072         apply (metis affine_hull_eq affine_hyperplane hull_mono inf_le2)
  2073         done
  2074     next
  2075       show "affine hull S \<inter> {x. a h \<bullet> x = b h} \<subseteq> affine hull (S \<inter> {x. a h \<bullet> x = b h})"
  2076       proof
  2077         fix y
  2078         assume yaff: "y \<in> affine hull S \<inter> {y. a h \<bullet> y = b h}"
  2079         obtain T where "0 < T"
  2080                  and T: "\<And>j. \<lbrakk>j \<in> F; j \<noteq> h\<rbrakk> \<Longrightarrow> T * (a j \<bullet> y - a j \<bullet> w) \<le> b j - a j \<bullet> w"
  2081         proof (cases "F - {h} = {}")
  2082           case True then show ?thesis
  2083             by (rule_tac T=1 in that) auto
  2084         next
  2085           case False
  2086           then obtain h' where h': "h' \<in> F - {h}" by auto
  2087           define inff where "inff =
  2088             (INF j:F - {h}.
  2089               if 0 < a j \<bullet> y - a j \<bullet> w
  2090               then (b j - a j \<bullet> w) / (a j \<bullet> y - a j \<bullet> w)
  2091               else 1)"
  2092           have "0 < inff"
  2093             apply (simp add: inff_def)
  2094             apply (rule finite_imp_less_Inf)
  2095               using \<open>finite F\<close> apply blast
  2096              using h' apply blast
  2097             apply simp
  2098             using awlt apply (force simp: divide_simps)
  2099             done
  2100           moreover have "inff * (a j \<bullet> y - a j \<bullet> w) \<le> b j - a j \<bullet> w"
  2101                         if "j \<in> F" "j \<noteq> h" for j
  2102           proof (cases "a j \<bullet> w < a j \<bullet> y")
  2103             case True
  2104             then have "inff \<le> (b j - a j \<bullet> w) / (a j \<bullet> y - a j \<bullet> w)"
  2105               apply (simp add: inff_def)
  2106               apply (rule cInf_le_finite)
  2107               using \<open>finite F\<close> apply blast
  2108               apply (simp add: that split: if_split_asm)
  2109               done
  2110             then show ?thesis
  2111               using \<open>0 < inff\<close> awlt [OF that] mult_strict_left_mono
  2112               by (fastforce simp add: algebra_simps divide_simps split: if_split_asm)
  2113           next
  2114             case False
  2115             with \<open>0 < inff\<close> have "inff * (a j \<bullet> y - a j \<bullet> w) \<le> 0"
  2116               by (simp add: mult_le_0_iff)
  2117             also have "... < b j - a j \<bullet> w"
  2118               by (simp add: awlt that)
  2119             finally show ?thesis by simp
  2120           qed
  2121           ultimately show ?thesis
  2122             by (blast intro: that)
  2123         qed
  2124         define c where "c = (1 - T) *\<^sub>R w + T *\<^sub>R y"
  2125         have "(1 - T) *\<^sub>R w + T *\<^sub>R y \<in> j" if "j \<in> F" for j
  2126         proof (cases "j = h")
  2127           case True
  2128           have "(1 - T) *\<^sub>R w + T *\<^sub>R y \<in> {x. a h \<bullet> x \<le> b h}"
  2129             using weq yaff by (auto simp: algebra_simps)
  2130           with True faceq [OF that] show ?thesis by metis
  2131         next
  2132           case False
  2133           with T that have "(1 - T) *\<^sub>R w + T *\<^sub>R y \<in> {x. a j \<bullet> x \<le> b j}"
  2134             by (simp add: algebra_simps)
  2135           with faceq [OF that] show ?thesis by simp
  2136         qed
  2137         moreover have "(1 - T) *\<^sub>R w + T *\<^sub>R y \<in> affine hull S"
  2138           apply (rule affine_affine_hull [simplified affine_alt, rule_format])
  2139           apply (simp add: \<open>w \<in> affine hull S\<close>)
  2140           using yaff apply blast
  2141           done
  2142         ultimately have "c \<in> S"
  2143           using seq by (force simp: c_def)
  2144         moreover have "a h \<bullet> c = b h"
  2145           using yaff by (force simp: c_def algebra_simps weq)
  2146         ultimately have caff: "c \<in> affine hull (S \<inter> {y. a h \<bullet> y = b h})"
  2147           by (simp add: hull_inc)
  2148         have waff: "w \<in> affine hull (S \<inter> {y. a h \<bullet> y = b h})"
  2149           using \<open>w \<in> S\<close> weq by (blast intro: hull_inc)
  2150         have yeq: "y = (1 - inverse T) *\<^sub>R w + c /\<^sub>R T"
  2151           using \<open>0 < T\<close> by (simp add: c_def algebra_simps)
  2152         show "y \<in> affine hull (S \<inter> {y. a h \<bullet> y = b h})"
  2153           by (metis yeq affine_affine_hull [simplified affine_alt, rule_format, OF waff caff])
  2154       qed
  2155     qed
  2156     ultimately show ?thesis
  2157       apply (simp add: facet_of_def)
  2158       apply (subst aff_dim_affine_hull [symmetric])
  2159       using  \<open>b h < a h \<bullet> z\<close> zaff
  2160       apply (force simp: aff_dim_affine_Int_hyperplane)
  2161       done
  2162   qed
  2163   show ?thesis
  2164   proof
  2165     show "\<exists>h. h \<in> F \<and> c = S \<inter> {x. a h \<bullet> x = b h} \<Longrightarrow> c facet_of S"
  2166       using * by blast
  2167   next
  2168     assume "c facet_of S"
  2169     then have "c face_of S" "convex c" "c \<noteq> {}" and affc: "aff_dim c = aff_dim S - 1"
  2170       by (auto simp: facet_of_def face_of_imp_convex)
  2171     then obtain x where x: "x \<in> rel_interior c"
  2172       by (force simp: rel_interior_eq_empty)
  2173     then have "x \<in> c"
  2174       by (meson subsetD rel_interior_subset)
  2175     then have "x \<in> S"
  2176       using \<open>c facet_of S\<close> facet_of_imp_subset by blast
  2177     have rels: "rel_interior S = {x \<in> S. \<forall>h\<in>F. a h \<bullet> x < b h}"
  2178       by (rule rel_interior_polyhedron_explicit [OF assms])
  2179     have "c \<noteq> S"
  2180       using \<open>c facet_of S\<close> facet_of_irrefl by blast
  2181     then have "x \<notin> rel_interior S"
  2182       by (metis IntI empty_iff \<open>x \<in> c\<close> \<open>c \<noteq> S\<close> \<open>c face_of S\<close> face_of_disjoint_rel_interior)
  2183     with rels \<open>x \<in> S\<close> obtain i where "i \<in> F" and i: "a i \<bullet> x \<ge> b i"
  2184       by force
  2185     have "x \<in> {u. a i \<bullet> u \<le> b i}"
  2186       by (metis IntD2 InterE \<open>i \<in> F\<close> \<open>x \<in> S\<close> faceq seq)
  2187     then have "a i \<bullet> x \<le> b i" by simp
  2188     then have "a i \<bullet> x = b i" using i by auto
  2189     have "c \<subseteq> S \<inter> {x. a i \<bullet> x = b i}"
  2190       apply (rule subset_of_face_of [of _ S])
  2191         apply (simp add: "*" \<open>i \<in> F\<close> facet_of_imp_face_of)
  2192        apply (simp add: \<open>c face_of S\<close> face_of_imp_subset)
  2193       using \<open>a i \<bullet> x = b i\<close> \<open>x \<in> S\<close> x by blast
  2194     then have cface: "c face_of (S \<inter> {x. a i \<bullet> x = b i})"
  2195       by (meson \<open>c face_of S\<close> face_of_subset inf_le1)
  2196     have con: "convex (S \<inter> {x. a i \<bullet> x = b i})"
  2197       by (simp add: \<open>convex S\<close> convex_Int convex_hyperplane)
  2198     show "\<exists>h. h \<in> F \<and> c = S \<inter> {x. a h \<bullet> x = b h}"
  2199       apply (rule_tac x=i in exI)
  2200       apply (simp add: \<open>i \<in> F\<close>)
  2201       by (metis (no_types) * \<open>i \<in> F\<close> affc facet_of_def less_irrefl face_of_aff_dim_lt [OF con cface])
  2202   qed
  2203 qed
  2204 
  2205 
  2206 lemma face_of_polyhedron_subset_explicit:
  2207   fixes S :: "'a :: euclidean_space set"
  2208   assumes "finite F"
  2209       and seq: "S = affine hull S \<inter> \<Inter>F"
  2210       and faceq: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
  2211       and psub: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> affine hull S \<inter> \<Inter>F'"
  2212       and c: "c face_of S" and "c \<noteq> {}" "c \<noteq> S"
  2213    obtains h where "h \<in> F" "c \<subseteq> S \<inter> {x. a h \<bullet> x = b h}"
  2214 proof -
  2215   have "c \<subseteq> S" using \<open>c face_of S\<close>
  2216     by (simp add: face_of_imp_subset)
  2217   have "polyhedron S"
  2218     apply (simp add: polyhedron_Int_affine)
  2219     by (metis \<open>finite F\<close> faceq seq)
  2220   then have "convex S"
  2221     by (simp add: polyhedron_imp_convex)
  2222   then have *: "(S \<inter> {x. a h \<bullet> x = b h}) face_of S" if "h \<in> F" for h
  2223     apply (rule face_of_Int_supporting_hyperplane_le)
  2224     using faceq seq that by fastforce
  2225   have "rel_interior c \<noteq> {}"
  2226     using c \<open>c \<noteq> {}\<close> face_of_imp_convex rel_interior_eq_empty by blast
  2227   then obtain x where "x \<in> rel_interior c" by auto
  2228   have rels: "rel_interior S = {x \<in> S. \<forall>h\<in>F. a h \<bullet> x < b h}"
  2229     by (rule rel_interior_polyhedron_explicit [OF \<open>finite F\<close> seq faceq psub])
  2230   then have xnot: "x \<notin> rel_interior S"
  2231     by (metis IntI \<open>x \<in> rel_interior c\<close> c \<open>c \<noteq> S\<close> contra_subsetD empty_iff face_of_disjoint_rel_interior rel_interior_subset)
  2232   then have "x \<in> S"
  2233     using \<open>c \<subseteq> S\<close> \<open>x \<in> rel_interior c\<close> rel_interior_subset by auto
  2234   then have xint: "x \<in> \<Inter>F"
  2235     using seq by blast
  2236   have "F \<noteq> {}" using assms
  2237     by (metis affine_Int affine_Inter affine_affine_hull ex_in_conv face_of_affine_trivial)
  2238   then obtain i where "i \<in> F" "~ (a i \<bullet> x < b i)"
  2239     using \<open>x \<in> S\<close> rels xnot by auto
  2240   with xint have "a i \<bullet> x = b i"
  2241     by (metis eq_iff mem_Collect_eq not_le Inter_iff faceq)
  2242   have face: "S \<inter> {x. a i \<bullet> x = b i} face_of S"
  2243     by (simp add: "*" \<open>i \<in> F\<close>)
  2244   show ?thesis
  2245     apply (rule_tac h = i in that)
  2246      apply (rule \<open>i \<in> F\<close>)
  2247     apply (rule subset_of_face_of [OF face \<open>c \<subseteq> S\<close>])
  2248     using \<open>a i \<bullet> x = b i\<close> \<open>x \<in> rel_interior c\<close> \<open>x \<in> S\<close> apply blast
  2249     done
  2250 qed
  2251 
  2252 text\<open>Initial part of proof duplicates that above\<close>
  2253 proposition face_of_polyhedron_explicit:
  2254   fixes S :: "'a :: euclidean_space set"
  2255   assumes "finite F"
  2256       and seq: "S = affine hull S \<inter> \<Inter>F"
  2257       and faceq: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
  2258       and psub: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> affine hull S \<inter> \<Inter>F'"
  2259       and c: "c face_of S" and "c \<noteq> {}" "c \<noteq> S"
  2260     shows "c = \<Inter>{S \<inter> {x. a h \<bullet> x = b h} | h. h \<in> F \<and> c \<subseteq> S \<inter> {x. a h \<bullet> x = b h}}"
  2261 proof -
  2262   let ?ab = "\<lambda>h. {x. a h \<bullet> x = b h}"
  2263   have "c \<subseteq> S" using \<open>c face_of S\<close>
  2264     by (simp add: face_of_imp_subset)
  2265   have "polyhedron S"
  2266     apply (simp add: polyhedron_Int_affine)
  2267     by (metis \<open>finite F\<close> faceq seq)
  2268   then have "convex S"
  2269     by (simp add: polyhedron_imp_convex)
  2270   then have *: "(S \<inter> ?ab h) face_of S" if "h \<in> F" for h
  2271     apply (rule face_of_Int_supporting_hyperplane_le)
  2272     using faceq seq that by fastforce
  2273   have "rel_interior c \<noteq> {}"
  2274     using c \<open>c \<noteq> {}\<close> face_of_imp_convex rel_interior_eq_empty by blast
  2275   then obtain z where z: "z \<in> rel_interior c" by auto
  2276   have rels: "rel_interior S = {z \<in> S. \<forall>h\<in>F. a h \<bullet> z < b h}"
  2277     by (rule rel_interior_polyhedron_explicit [OF \<open>finite F\<close> seq faceq psub])
  2278   then have xnot: "z \<notin> rel_interior S"
  2279     by (metis IntI \<open>z \<in> rel_interior c\<close> c \<open>c \<noteq> S\<close> contra_subsetD empty_iff face_of_disjoint_rel_interior rel_interior_subset)
  2280   then have "z \<in> S"
  2281     using \<open>c \<subseteq> S\<close> \<open>z \<in> rel_interior c\<close> rel_interior_subset by auto
  2282   with seq have xint: "z \<in> \<Inter>F" by blast
  2283   have "open (\<Inter>h\<in>{h \<in> F. a h \<bullet> z < b h}. {w. a h \<bullet> w < b h})"
  2284     by (auto simp: \<open>finite F\<close> open_halfspace_lt open_INT)
  2285   then obtain e where "0 < e"
  2286                  "ball z e \<subseteq> (\<Inter>h\<in>{h \<in> F. a h \<bullet> z < b h}. {w. a h \<bullet> w < b h})"
  2287     by (auto intro: openE [of _ z])
  2288   then have e: "\<And>h. \<lbrakk>h \<in> F; a h \<bullet> z < b h\<rbrakk> \<Longrightarrow> ball z e \<subseteq> {w. a h \<bullet> w < b h}"
  2289     by blast
  2290   have "c \<subseteq> (S \<inter> ?ab h) \<longleftrightarrow> z \<in> S \<inter> ?ab h" if "h \<in> F" for h
  2291   proof
  2292     show "z \<in> S \<inter> ?ab h \<Longrightarrow> c \<subseteq> S \<inter> ?ab h"
  2293       apply (rule subset_of_face_of [of _ S])
  2294       using that \<open>c \<subseteq> S\<close> \<open>z \<in> rel_interior c\<close>
  2295       using facet_of_polyhedron_explicit [OF \<open>finite F\<close> seq faceq psub]
  2296             unfolding facet_of_def
  2297       apply auto
  2298       done
  2299   next
  2300     show "c \<subseteq> S \<inter> ?ab h \<Longrightarrow> z \<in> S \<inter> ?ab h"
  2301       using \<open>z \<in> rel_interior c\<close> rel_interior_subset by force
  2302   qed
  2303   then have **: "{S \<inter> ?ab h | h. h \<in> F \<and> c \<subseteq> S \<and> c \<subseteq> ?ab h} =
  2304                  {S \<inter> ?ab h |h. h \<in> F \<and> z \<in> S \<inter> ?ab h}"
  2305     by blast
  2306   have bsub: "ball z e \<inter> affine hull \<Inter>{S \<inter> ?ab h |h. h \<in> F \<and> a h \<bullet> z = b h}
  2307              \<subseteq> affine hull S \<inter> \<Inter>F \<inter> \<Inter>{?ab h |h. h \<in> F \<and> a h \<bullet> z = b h}"
  2308             if "i \<in> F" and i: "a i \<bullet> z = b i" for i
  2309   proof -
  2310     have sub: "ball z e \<inter> \<Inter>{?ab h |h. h \<in> F \<and> a h \<bullet> z = b h} \<subseteq> j"
  2311              if "j \<in> F" for j
  2312     proof -
  2313       have "a j \<bullet> z \<le> b j" using faceq that xint by auto
  2314       then consider "a j \<bullet> z < b j" | "a j \<bullet> z = b j" by linarith
  2315       then have "\<exists>G. G \<in> {?ab h |h. h \<in> F \<and> a h \<bullet> z = b h} \<and> ball z e \<inter> G \<subseteq> j"
  2316       proof cases
  2317         assume "a j \<bullet> z < b j"
  2318         then have "ball z e \<inter> {x. a i \<bullet> x = b i} \<subseteq> j"
  2319           using e [OF \<open>j \<in> F\<close>] faceq that
  2320           by (fastforce simp: ball_def)
  2321         then show ?thesis
  2322           by (rule_tac x="{x. a i \<bullet> x = b i}" in exI) (force simp: \<open>i \<in> F\<close> i)
  2323       next
  2324         assume eq: "a j \<bullet> z = b j"
  2325         with faceq that show ?thesis
  2326           by (rule_tac x="{x. a j \<bullet> x = b j}" in exI) (fastforce simp add: \<open>j \<in> F\<close>)
  2327       qed
  2328       then show ?thesis  by blast
  2329     qed
  2330     have 1: "affine hull \<Inter>{S \<inter> ?ab h |h. h \<in> F \<and> a h \<bullet> z = b h} \<subseteq> affine hull S"
  2331       apply (rule hull_mono)
  2332       using that \<open>z \<in> S\<close> by auto
  2333     have 2: "affine hull \<Inter>{S \<inter> ?ab h |h. h \<in> F \<and> a h \<bullet> z = b h}
  2334           \<subseteq> \<Inter>{?ab h |h. h \<in> F \<and> a h \<bullet> z = b h}"
  2335       by (rule hull_minimal) (auto intro: affine_hyperplane)
  2336     have 3: "ball z e \<inter> \<Inter>{?ab h |h. h \<in> F \<and> a h \<bullet> z = b h} \<subseteq> \<Inter>F"
  2337       by (iprover intro: sub Inter_greatest)
  2338     have *: "\<lbrakk>A \<subseteq> (B :: 'a set); A \<subseteq> C; E \<inter> C \<subseteq> D\<rbrakk> \<Longrightarrow> E \<inter> A \<subseteq> (B \<inter> D) \<inter> C"
  2339              for A B C D E  by blast
  2340     show ?thesis by (intro * 1 2 3)
  2341   qed
  2342   have "\<exists>h. h \<in> F \<and> c \<subseteq> ?ab h"
  2343     apply (rule face_of_polyhedron_subset_explicit [OF \<open>finite F\<close> seq faceq psub])
  2344     using assms by auto
  2345   then have fac: "\<Inter>{S \<inter> ?ab h |h. h \<in> F \<and> c \<subseteq> S \<inter> ?ab h} face_of S"
  2346     using * by (force simp: \<open>c \<subseteq> S\<close> intro: face_of_Inter)
  2347   have red:
  2348      "(\<And>a. P a \<Longrightarrow> T \<subseteq> S \<inter> \<Inter>{F x |x. P x}) \<Longrightarrow> T \<subseteq> \<Inter>{S \<inter> F x |x. P x}"
  2349      for P T F   by blast
  2350   have "ball z e \<inter> affine hull \<Inter>{S \<inter> ?ab h |h. h \<in> F \<and> a h \<bullet> z = b h}
  2351         \<subseteq> \<Inter>{S \<inter> ?ab h |h. h \<in> F \<and> a h \<bullet> z = b h}"
  2352     apply (rule red)
  2353     apply (metis seq bsub)
  2354     done
  2355   with \<open>0 < e\<close> have zinrel: "z \<in> rel_interior
  2356                     (\<Inter>{S \<inter> ?ab h |h. h \<in> F \<and> z \<in> S \<and> a h \<bullet> z = b h})"
  2357     by (auto simp: mem_rel_interior_ball \<open>z \<in> S\<close>)
  2358   show ?thesis
  2359     apply (rule face_of_eq [OF c fac])
  2360     using z zinrel apply (force simp: **)
  2361     done
  2362 qed
  2363 
  2364 
  2365 subsection\<open>More general corollaries from the explicit representation\<close>
  2366 
  2367 corollary facet_of_polyhedron:
  2368   assumes "polyhedron S" and "c facet_of S"
  2369   obtains a b where "a \<noteq> 0" "S \<subseteq> {x. a \<bullet> x \<le> b}" "c = S \<inter> {x. a \<bullet> x = b}"
  2370 proof -
  2371   obtain F where "finite F" and seq: "S = affine hull S \<inter> \<Inter>F"
  2372              and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
  2373              and min: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> (affine hull S) \<inter> \<Inter>F'"
  2374     using assms by (simp add: polyhedron_Int_affine_minimal) meson
  2375   then obtain a b where ab: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
  2376     by metis
  2377   obtain i where "i \<in> F" and c: "c = S \<inter> {x. a i \<bullet> x = b i}"
  2378     using facet_of_polyhedron_explicit [OF \<open>finite F\<close> seq ab min] assms
  2379     by force
  2380   moreover have ssub: "S \<subseteq> {x. a i \<bullet> x \<le> b i}"
  2381      apply (subst seq)
  2382      using \<open>i \<in> F\<close> ab by auto
  2383   ultimately show ?thesis
  2384     by (rule_tac a = "a i" and b = "b i" in that) (simp_all add: ab)
  2385 qed
  2386 
  2387 corollary face_of_polyhedron:
  2388   assumes "polyhedron S" and "c face_of S" and "c \<noteq> {}" and "c \<noteq> S"
  2389     shows "c = \<Inter>{F. F facet_of S \<and> c \<subseteq> F}"
  2390 proof -
  2391   obtain F where "finite F" and seq: "S = affine hull S \<inter> \<Inter>F"
  2392              and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
  2393              and min: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> (affine hull S) \<inter> \<Inter>F'"
  2394     using assms by (simp add: polyhedron_Int_affine_minimal) meson
  2395   then obtain a b where ab: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
  2396     by metis
  2397   show ?thesis
  2398     apply (subst face_of_polyhedron_explicit [OF \<open>finite F\<close> seq ab min])
  2399     apply (auto simp: assms facet_of_polyhedron_explicit [OF \<open>finite F\<close> seq ab min] cong: Collect_cong)
  2400     done
  2401 qed
  2402 
  2403 lemma face_of_polyhedron_subset_facet:
  2404   assumes "polyhedron S" and "c face_of S" and "c \<noteq> {}" and "c \<noteq> S"
  2405   obtains F where "F facet_of S" "c \<subseteq> F"
  2406 using face_of_polyhedron assms
  2407 by (metis (no_types, lifting) Inf_greatest antisym_conv face_of_imp_subset mem_Collect_eq)
  2408 
  2409 
  2410 lemma exposed_face_of_polyhedron:
  2411   assumes "polyhedron S"
  2412     shows "F exposed_face_of S \<longleftrightarrow> F face_of S"
  2413 proof
  2414   show "F exposed_face_of S \<Longrightarrow> F face_of S"
  2415     by (simp add: exposed_face_of_def)
  2416 next
  2417   assume "F face_of S"
  2418   show "F exposed_face_of S"
  2419   proof (cases "F = {} \<or> F = S")
  2420     case True then show ?thesis
  2421       using \<open>F face_of S\<close> exposed_face_of by blast
  2422   next
  2423     case False
  2424     then have "{g. g facet_of S \<and> F \<subseteq> g} \<noteq> {}"
  2425       by (metis Collect_empty_eq_bot \<open>F face_of S\<close> assms empty_def face_of_polyhedron_subset_facet)
  2426     moreover have "\<And>T. \<lbrakk>T facet_of S; F \<subseteq> T\<rbrakk> \<Longrightarrow> T exposed_face_of S"
  2427       by (metis assms exposed_face_of facet_of_imp_face_of facet_of_polyhedron)
  2428     ultimately have "\<Inter>{fa.
  2429        fa facet_of S \<and> F \<subseteq> fa} exposed_face_of S"
  2430       by (metis (no_types, lifting) mem_Collect_eq exposed_face_of_Inter)
  2431     then show ?thesis
  2432       using False
  2433       apply (subst face_of_polyhedron [OF assms \<open>F face_of S\<close>], auto)
  2434       done
  2435   qed
  2436 qed
  2437 
  2438 lemma face_of_polyhedron_polyhedron:
  2439   fixes S :: "'a :: euclidean_space set"
  2440   assumes "polyhedron S" "c face_of S" shows "polyhedron c"
  2441 by (metis assms face_of_imp_eq_affine_Int polyhedron_Int polyhedron_affine_hull polyhedron_imp_convex)
  2442 
  2443 lemma finite_polyhedron_faces:
  2444   fixes S :: "'a :: euclidean_space set"
  2445   assumes "polyhedron S"
  2446     shows "finite {F. F face_of S}"
  2447 proof -
  2448   obtain F where "finite F" and seq: "S = affine hull S \<inter> \<Inter>F"
  2449              and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
  2450              and min:   "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> (affine hull S) \<inter> \<Inter>F'"
  2451     using assms by (simp add: polyhedron_Int_affine_minimal) meson
  2452   then obtain a b where ab: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
  2453     by metis
  2454   have "finite {\<Inter>{S \<inter> {x. a h \<bullet> x = b h} |h. h \<in> F'}| F'. F' \<in> Pow F}"
  2455     by (simp add: \<open>finite F\<close>)
  2456   moreover have "{F. F face_of S} - {{}, S} \<subseteq> {\<Inter>{S \<inter> {x. a h \<bullet> x = b h} |h. h \<in> F'}| F'. F' \<in> Pow F}"
  2457     apply clarify
  2458     apply (rename_tac c)
  2459     apply (drule face_of_polyhedron_explicit [OF \<open>finite F\<close> seq ab min, simplified], simp_all)
  2460     apply (erule ssubst)
  2461     apply (rule_tac x="{h \<in> F. c \<subseteq> S \<inter> {x. a h \<bullet> x = b h}}" in exI, auto)
  2462     done
  2463   ultimately show ?thesis
  2464     by (meson finite.emptyI finite.insertI finite_Diff2 finite_subset)
  2465 qed
  2466 
  2467 lemma finite_polyhedron_exposed_faces:
  2468    "polyhedron S \<Longrightarrow> finite {F. F exposed_face_of S}"
  2469 using exposed_face_of_polyhedron finite_polyhedron_faces by fastforce
  2470 
  2471 lemma finite_polyhedron_extreme_points:
  2472   fixes S :: "'a :: euclidean_space set"
  2473   shows "polyhedron S \<Longrightarrow> finite {v. v extreme_point_of S}"
  2474 apply (simp add: face_of_singleton [symmetric])
  2475 apply (rule finite_subset [OF _ finite_vimageI [OF finite_polyhedron_faces]], auto)
  2476 done
  2477 
  2478 lemma finite_polyhedron_facets:
  2479   fixes S :: "'a :: euclidean_space set"
  2480   shows "polyhedron S \<Longrightarrow> finite {F. F facet_of S}"
  2481 unfolding facet_of_def
  2482 by (blast intro: finite_subset [OF _ finite_polyhedron_faces])
  2483 
  2484 
  2485 proposition rel_interior_of_polyhedron:
  2486   fixes S :: "'a :: euclidean_space set"
  2487   assumes "polyhedron S"
  2488     shows "rel_interior S = S - \<Union>{F. F facet_of S}"
  2489 proof -
  2490   obtain F where "finite F" and seq: "S = affine hull S \<inter> \<Inter>F"
  2491              and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
  2492              and min: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> (affine hull S) \<inter> \<Inter>F'"
  2493     using assms by (simp add: polyhedron_Int_affine_minimal) meson
  2494   then obtain a b where ab: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
  2495     by metis
  2496   have facet: "(c facet_of S) \<longleftrightarrow> (\<exists>h. h \<in> F \<and> c = S \<inter> {x. a h \<bullet> x = b h})" for c
  2497     by (rule facet_of_polyhedron_explicit [OF \<open>finite F\<close> seq ab min])
  2498   have rel: "rel_interior S = {x \<in> S. \<forall>h\<in>F. a h \<bullet> x < b h}"
  2499     by (rule rel_interior_polyhedron_explicit [OF \<open>finite F\<close> seq ab min])
  2500   have "a h \<bullet> x < b h" if "x \<in> S" "h \<in> F" and xnot: "x \<notin> \<Union>{F. F facet_of S}" for x h
  2501   proof -
  2502     have "x \<in> \<Inter>F" using seq that by force
  2503     with \<open>h \<in> F\<close> ab have "a h \<bullet> x \<le> b h" by auto
  2504     then consider "a h \<bullet> x < b h" | "a h \<bullet> x = b h" by linarith
  2505     then show ?thesis
  2506     proof cases
  2507       case 1 then show ?thesis .
  2508     next
  2509       case 2
  2510       have "Collect ((\<in>) x) \<notin> Collect ((\<in>) (\<Union>{A. A facet_of S}))"
  2511         using xnot by fastforce
  2512       then have "F \<notin> Collect ((\<in>) h)"
  2513         using 2 \<open>x \<in> S\<close> facet by blast
  2514       with \<open>h \<in> F\<close> have "\<Inter>F \<subseteq> S \<inter> {x. a h \<bullet> x = b h}" by blast
  2515       with 2 that \<open>x \<in> \<Inter>F\<close> show ?thesis
  2516         apply simp
  2517         apply (drule_tac x="\<Inter>F" in spec)
  2518         apply (simp add: facet)
  2519         apply (drule_tac x=h in spec)
  2520         using seq by auto
  2521       qed
  2522   qed
  2523   moreover have "\<exists>h\<in>F. a h \<bullet> x \<ge> b h" if "x \<in> \<Union>{F. F facet_of S}" for x
  2524     using that by (force simp: facet)
  2525   ultimately show ?thesis
  2526     by (force simp: rel)
  2527 qed
  2528 
  2529 lemma rel_boundary_of_polyhedron:
  2530   fixes S :: "'a :: euclidean_space set"
  2531   assumes "polyhedron S"
  2532     shows "S - rel_interior S = \<Union> {F. F facet_of S}"
  2533 using facet_of_imp_subset by (fastforce simp add: rel_interior_of_polyhedron assms)
  2534 
  2535 lemma rel_frontier_of_polyhedron:
  2536   fixes S :: "'a :: euclidean_space set"
  2537   assumes "polyhedron S"
  2538     shows "rel_frontier S = \<Union> {F. F facet_of S}"
  2539 by (simp add: assms rel_frontier_def polyhedron_imp_closed rel_boundary_of_polyhedron)
  2540 
  2541 lemma rel_frontier_of_polyhedron_alt:
  2542   fixes S :: "'a :: euclidean_space set"
  2543   assumes "polyhedron S"
  2544     shows "rel_frontier S = \<Union> {F. F face_of S \<and> (F \<noteq> S)}"
  2545 apply (rule subset_antisym)
  2546   apply (force simp: rel_frontier_of_polyhedron facet_of_def assms)
  2547 using face_of_subset_rel_frontier by fastforce
  2548 
  2549 
  2550 text\<open>A characterization of polyhedra as having finitely many faces\<close>
  2551 
  2552 proposition polyhedron_eq_finite_exposed_faces:
  2553   fixes S :: "'a :: euclidean_space set"
  2554   shows "polyhedron S \<longleftrightarrow> closed S \<and> convex S \<and> finite {F. F exposed_face_of S}"
  2555          (is "?lhs = ?rhs")
  2556 proof
  2557   assume ?lhs
  2558   then show ?rhs
  2559     by (auto simp: polyhedron_imp_closed polyhedron_imp_convex finite_polyhedron_exposed_faces)
  2560 next
  2561   assume ?rhs
  2562   then have "closed S" "convex S" and fin: "finite {F. F exposed_face_of S}" by auto
  2563   show ?lhs
  2564   proof (cases "S = {}")
  2565     case True then show ?thesis by auto
  2566   next
  2567     case False
  2568     define F where "F = {h. h exposed_face_of S \<and> h \<noteq> {} \<and> h \<noteq> S}"
  2569     have "finite F" by (simp add: fin F_def)
  2570     have hface: "h face_of S"
  2571       and "\<exists>a b. a \<noteq> 0 \<and> S \<subseteq> {x. a \<bullet> x \<le> b} \<and> h = S \<inter> {x. a \<bullet> x = b}"
  2572       if "h \<in> F" for h
  2573       using exposed_face_of F_def that by simp_all auto
  2574     then obtain a b where ab:
  2575       "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> S \<subseteq> {x. a h \<bullet> x \<le> b h} \<and> h = S \<inter> {x. a h \<bullet> x = b h}"
  2576       by metis
  2577     have *: "False"
  2578       if paff: "p \<in> affine hull S" and "p \<notin> S"
  2579       and pint: "p \<in> \<Inter>{{x. a h \<bullet> x \<le> b h} |h. h \<in> F}" for p
  2580     proof -
  2581       have "rel_interior S \<noteq> {}"
  2582         by (simp add: \<open>S \<noteq> {}\<close> \<open>convex S\<close> rel_interior_eq_empty)
  2583       then obtain c where c: "c \<in> rel_interior S" by auto
  2584       with rel_interior_subset have "c \<in> S"  by blast
  2585       have ccp: "closed_segment c p \<subseteq> affine hull S"
  2586         by (meson affine_affine_hull affine_imp_convex c closed_segment_subset hull_subset paff rel_interior_subset subsetCE)
  2587       obtain x where xcl: "x \<in> closed_segment c p" and "x \<in> S" and xnot: "x \<notin> rel_interior S"
  2588         using connected_openin [of "closed_segment c p"]
  2589         apply simp
  2590         apply (drule_tac x="closed_segment c p \<inter> rel_interior S" in spec)
  2591         apply (erule impE)
  2592          apply (force simp: openin_rel_interior openin_Int intro: openin_subtopology_Int_subset [OF _ ccp])
  2593         apply (drule_tac x="closed_segment c p \<inter> (- S)" in spec)
  2594         using rel_interior_subset \<open>closed S\<close> c \<open>p \<notin> S\<close> apply blast
  2595         done
  2596       then obtain \<mu> where "0 \<le> \<mu>" "\<mu> \<le> 1" and xeq: "x = (1 - \<mu>) *\<^sub>R c + \<mu> *\<^sub>R p"
  2597         by (auto simp: in_segment)
  2598       show False
  2599       proof (cases "\<mu>=0 \<or> \<mu>=1")
  2600         case True with xeq c xnot \<open>x \<in> S\<close> \<open>p \<notin> S\<close>
  2601         show False by auto
  2602       next
  2603         case False
  2604         then have xos: "x \<in> open_segment c p"
  2605           using \<open>x \<in> S\<close> c open_segment_def that(2) xcl xnot by auto
  2606         have xclo: "x \<in> closure S"
  2607           using \<open>x \<in> S\<close> closure_subset by blast
  2608         obtain d where "d \<noteq> 0"
  2609               and dle: "\<And>y. y \<in> closure S \<Longrightarrow> d \<bullet> x \<le> d \<bullet> y"
  2610               and dless: "\<And>y. y \<in> rel_interior S \<Longrightarrow> d \<bullet> x < d \<bullet> y"
  2611           by (metis supporting_hyperplane_relative_frontier [OF \<open>convex S\<close> xclo xnot])
  2612         have sex: "S \<inter> {y. d \<bullet> y = d \<bullet> x} exposed_face_of S"
  2613           by (simp add: \<open>closed S\<close> dle exposed_face_of_Int_supporting_hyperplane_ge [OF \<open>convex S\<close>])
  2614         have sne: "S \<inter> {y. d \<bullet> y = d \<bullet> x} \<noteq> {}"
  2615           using \<open>x \<in> S\<close> by blast
  2616         have sns: "S \<inter> {y. d \<bullet> y = d \<bullet> x} \<noteq> S"
  2617           by (metis (mono_tags) Int_Collect c subsetD dless not_le order_refl rel_interior_subset)
  2618         obtain h where "h \<in> F" "x \<in> h"
  2619           apply (rule_tac h="S \<inter> {y. d \<bullet> y = d \<bullet> x}" in that)
  2620           apply (simp_all add: F_def sex sne sns \<open>x \<in> S\<close>)
  2621           done
  2622         have abface: "{y. a h \<bullet> y = b h} face_of {y. a h \<bullet> y \<le> b h}"
  2623           using hyperplane_face_of_halfspace_le by blast
  2624         then have "c \<in> h"
  2625           using face_ofD [OF abface xos] \<open>c \<in> S\<close> \<open>h \<in> F\<close> ab pint \<open>x \<in> h\<close> by blast
  2626         with c have "h \<inter> rel_interior S \<noteq> {}" by blast
  2627         then show False
  2628           using \<open>h \<in> F\<close> F_def face_of_disjoint_rel_interior hface by auto
  2629       qed
  2630     qed
  2631     have "S \<subseteq> affine hull S \<inter> \<Inter>{{x. a h \<bullet> x \<le> b h} |h. h \<in> F}"
  2632       using ab by (auto simp: hull_subset)
  2633     moreover have "affine hull S \<inter> \<Inter>{{x. a h \<bullet> x \<le> b h} |h. h \<in> F} \<subseteq> S"
  2634       using * by blast
  2635     ultimately have "S = affine hull S \<inter> \<Inter> {{x. a h \<bullet> x \<le> b h} |h. h \<in> F}" ..
  2636     then show ?thesis
  2637       apply (rule ssubst)
  2638       apply (force intro: polyhedron_affine_hull polyhedron_halfspace_le simp: \<open>finite F\<close>)
  2639       done
  2640   qed
  2641 qed
  2642 
  2643 corollary polyhedron_eq_finite_faces:
  2644   fixes S :: "'a :: euclidean_space set"
  2645   shows "polyhedron S \<longleftrightarrow> closed S \<and> convex S \<and> finite {F. F face_of S}"
  2646          (is "?lhs = ?rhs")
  2647 proof
  2648   assume ?lhs
  2649   then show ?rhs
  2650     by (simp add: finite_polyhedron_faces polyhedron_imp_closed polyhedron_imp_convex)
  2651 next
  2652   assume ?rhs
  2653   then show ?lhs
  2654     by (force simp: polyhedron_eq_finite_exposed_faces exposed_face_of intro: finite_subset)
  2655 qed
  2656 
  2657 lemma polyhedron_linear_image_eq:
  2658   fixes h :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
  2659   assumes "linear h" "bij h"
  2660     shows "polyhedron (h ` S) \<longleftrightarrow> polyhedron S"
  2661 proof -
  2662   have *: "{f. P f} = (image h) ` {f. P (h ` f)}" for P
  2663     apply safe
  2664     apply (rule_tac x="inv h ` x" in image_eqI)
  2665     apply (auto simp: \<open>bij h\<close> bij_is_surj image_f_inv_f)
  2666     done
  2667   have "inj h" using bij_is_inj assms by blast
  2668   then have injim: "inj_on ((`) h) A" for A
  2669     by (simp add: inj_on_def inj_image_eq_iff)
  2670   show ?thesis
  2671     using \<open>linear h\<close> \<open>inj h\<close>
  2672     apply (simp add: polyhedron_eq_finite_faces closed_injective_linear_image_eq)
  2673     apply (simp add: * face_of_linear_image [of h _ S, symmetric] finite_image_iff injim)
  2674     done
  2675 qed
  2676 
  2677 lemma polyhedron_negations:
  2678   fixes S :: "'a :: euclidean_space set"
  2679   shows   "polyhedron S \<Longrightarrow> polyhedron(image uminus S)"
  2680 by (auto simp: polyhedron_linear_image_eq linear_uminus bij_uminus)
  2681 
  2682 subsection\<open>Relation between polytopes and polyhedra\<close>
  2683 
  2684 lemma polytope_eq_bounded_polyhedron:
  2685   fixes S :: "'a :: euclidean_space set"
  2686   shows "polytope S \<longleftrightarrow> polyhedron S \<and> bounded S"
  2687          (is "?lhs = ?rhs")
  2688 proof
  2689   assume ?lhs
  2690   then show ?rhs
  2691     by (simp add: finite_polytope_faces polyhedron_eq_finite_faces
  2692                   polytope_imp_closed polytope_imp_convex polytope_imp_bounded)
  2693 next
  2694   assume ?rhs then show ?lhs
  2695     unfolding polytope_def
  2696     apply (rule_tac x="{v. v extreme_point_of S}" in exI)
  2697     apply (simp add: finite_polyhedron_extreme_points Krein_Milman_Minkowski compact_eq_bounded_closed polyhedron_imp_closed polyhedron_imp_convex)
  2698     done
  2699 qed
  2700 
  2701 lemma polytope_Int:
  2702   fixes S :: "'a :: euclidean_space set"
  2703   shows "\<lbrakk>polytope S; polytope T\<rbrakk> \<Longrightarrow> polytope(S \<inter> T)"
  2704 by (simp add: polytope_eq_bounded_polyhedron bounded_Int)
  2705 
  2706 
  2707 lemma polytope_Int_polyhedron:
  2708   fixes S :: "'a :: euclidean_space set"
  2709   shows "\<lbrakk>polytope S; polyhedron T\<rbrakk> \<Longrightarrow> polytope(S \<inter> T)"
  2710 by (simp add: bounded_Int polytope_eq_bounded_polyhedron)
  2711 
  2712 lemma polyhedron_Int_polytope:
  2713   fixes S :: "'a :: euclidean_space set"
  2714   shows "\<lbrakk>polyhedron S; polytope T\<rbrakk> \<Longrightarrow> polytope(S \<inter> T)"
  2715 by (simp add: bounded_Int polytope_eq_bounded_polyhedron)
  2716 
  2717 lemma polytope_imp_polyhedron:
  2718   fixes S :: "'a :: euclidean_space set"
  2719   shows "polytope S \<Longrightarrow> polyhedron S"
  2720 by (simp add: polytope_eq_bounded_polyhedron)
  2721 
  2722 lemma polytope_facet_exists:
  2723   fixes p :: "'a :: euclidean_space set"
  2724   assumes "polytope p" "0 < aff_dim p"
  2725   obtains F where "F facet_of p"
  2726 proof (cases "p = {}")
  2727   case True with assms show ?thesis by auto
  2728 next
  2729   case False
  2730   then obtain v where "v extreme_point_of p"
  2731     using extreme_point_exists_convex
  2732     by (blast intro: \<open>polytope p\<close> polytope_imp_compact polytope_imp_convex)
  2733   then
  2734   show ?thesis
  2735     by (metis face_of_polyhedron_subset_facet polytope_imp_polyhedron aff_dim_sing
  2736        all_not_in_conv assms face_of_singleton less_irrefl singletonI that)
  2737 qed
  2738 
  2739 lemma polyhedron_interval [iff]: "polyhedron(cbox a b)"
  2740 by (metis polytope_imp_polyhedron polytope_interval)
  2741 
  2742 lemma polyhedron_convex_hull:
  2743   fixes S :: "'a :: euclidean_space set"
  2744   shows "finite S \<Longrightarrow> polyhedron(convex hull S)"
  2745 by (simp add: polytope_convex_hull polytope_imp_polyhedron)
  2746 
  2747 
  2748 subsection\<open>Relative and absolute frontier of a polytope\<close>
  2749 
  2750 lemma rel_boundary_of_convex_hull:
  2751     fixes S :: "'a::euclidean_space set"
  2752     assumes "~ affine_dependent S"
  2753       shows "(convex hull S) - rel_interior(convex hull S) = (\<Union>a\<in>S. convex hull (S - {a}))"
  2754 proof -
  2755   have "finite S" by (metis assms aff_independent_finite)
  2756   then consider "card S = 0" | "card S = 1" | "2 \<le> card S" by arith
  2757   then show ?thesis
  2758   proof cases
  2759     case 1 then have "S = {}" by (simp add: \<open>finite S\<close>)
  2760     then show ?thesis by simp
  2761   next
  2762     case 2 show ?thesis
  2763       by (auto intro: card_1_singletonE [OF \<open>card S = 1\<close>])
  2764   next
  2765     case 3
  2766     with assms show ?thesis
  2767       by (auto simp: polyhedron_convex_hull rel_boundary_of_polyhedron facet_of_convex_hull_affine_independent_alt \<open>finite S\<close>)
  2768   qed
  2769 qed
  2770 
  2771 proposition frontier_of_convex_hull:
  2772     fixes S :: "'a::euclidean_space set"
  2773     assumes "card S = Suc (DIM('a))"
  2774       shows "frontier(convex hull S) = \<Union> {convex hull (S - {a}) | a. a \<in> S}"
  2775 proof (cases "affine_dependent S")
  2776   case True
  2777     have [iff]: "finite S"
  2778       using assms using card_infinite by force
  2779     then have ccs: "closed (convex hull S)"
  2780       by (simp add: compact_imp_closed finite_imp_compact_convex_hull)
  2781     { fix x T
  2782       assume "finite T" "T \<subseteq> S" "int (card T) \<le> aff_dim S + 1" "x \<in> convex hull T"
  2783       then have "S \<noteq> T"
  2784         using True \<open>finite S\<close> aff_dim_le_card affine_independent_iff_card by fastforce
  2785       then obtain a where "a \<in> S" "a \<notin> T"
  2786         using \<open>T \<subseteq> S\<close> by blast
  2787       then have "x \<in> (\<Union>a\<in>S. convex hull (S - {a}))"
  2788         using True affine_independent_iff_card [of S]
  2789         apply simp
  2790         apply (metis (no_types, hide_lams) Diff_eq_empty_iff Diff_insert0 \<open>a \<notin> T\<close> \<open>T \<subseteq> S\<close> \<open>x \<in> convex hull T\<close>  hull_mono insert_Diff_single   subsetCE)
  2791         done
  2792     } note * = this
  2793     have 1: "convex hull S \<subseteq> (\<Union> a\<in>S. convex hull (S - {a}))"
  2794       apply (subst caratheodory_aff_dim)
  2795       apply (blast intro: *)
  2796       done
  2797     have 2: "\<Union>((\<lambda>a. convex hull (S - {a})) ` S) \<subseteq> convex hull S"
  2798       by (rule Union_least) (metis (no_types, lifting)  Diff_subset hull_mono imageE)
  2799     show ?thesis using True
  2800       apply (simp add: segment_convex_hull frontier_def)
  2801       using interior_convex_hull_eq_empty [OF assms]
  2802       apply (simp add: closure_closed [OF ccs])
  2803       apply (rule subset_antisym)
  2804       using 1 apply blast
  2805       using 2 apply blast
  2806       done
  2807 next
  2808   case False
  2809   then have "frontier (convex hull S) = (convex hull S) - rel_interior(convex hull S)"
  2810     apply (simp add: rel_boundary_of_convex_hull [symmetric] frontier_def)
  2811     by (metis aff_independent_finite assms closure_convex_hull finite_imp_compact_convex_hull hull_hull interior_convex_hull_eq_empty rel_interior_nonempty_interior)
  2812   also have "... = \<Union>{convex hull (S - {a}) |a. a \<in> S}"
  2813   proof -
  2814     have "convex hull S - rel_interior (convex hull S) = rel_frontier (convex hull S)"
  2815       by (simp add: False aff_independent_finite polyhedron_convex_hull rel_boundary_of_polyhedron rel_frontier_of_polyhedron)
  2816     then show ?thesis
  2817       by (simp add: False rel_frontier_convex_hull_cases)
  2818   qed
  2819   finally show ?thesis .
  2820 qed
  2821 
  2822 subsection\<open>Special case of a triangle\<close>
  2823 
  2824 proposition frontier_of_triangle:
  2825     fixes a :: "'a::euclidean_space"
  2826     assumes "DIM('a) = 2"
  2827     shows "frontier(convex hull {a,b,c}) = closed_segment a b \<union> closed_segment b c \<union> closed_segment c a"
  2828           (is "?lhs = ?rhs")
  2829 proof (cases "b = a \<or> c = a \<or> c = b")
  2830   case True then show ?thesis
  2831     by (auto simp: assms segment_convex_hull frontier_def empty_interior_convex_hull insert_commute card_insert_le_m1 hull_inc insert_absorb)
  2832 next
  2833   case False then have [simp]: "card {a, b, c} = Suc (DIM('a))"
  2834     by (simp add: card_insert Set.insert_Diff_if assms)
  2835   show ?thesis
  2836   proof
  2837     show "?lhs \<subseteq> ?rhs"
  2838       using False
  2839       by (force simp: segment_convex_hull frontier_of_convex_hull insert_Diff_if insert_commute split: if_split_asm)
  2840     show "?rhs \<subseteq> ?lhs"
  2841       using False
  2842       apply (simp add: frontier_of_convex_hull segment_convex_hull)
  2843       apply (intro conjI subsetI)
  2844         apply (rule_tac X="convex hull {a,b}" in UnionI; force simp: Set.insert_Diff_if)
  2845        apply (rule_tac X="convex hull {b,c}" in UnionI; force)
  2846       apply (rule_tac X="convex hull {a,c}" in UnionI; force simp: insert_commute Set.insert_Diff_if)
  2847       done
  2848   qed
  2849 qed
  2850 
  2851 corollary inside_of_triangle:
  2852     fixes a :: "'a::euclidean_space"
  2853     assumes "DIM('a) = 2"
  2854     shows "inside (closed_segment a b \<union> closed_segment b c \<union> closed_segment c a) = interior(convex hull {a,b,c})"
  2855 by (metis assms frontier_of_triangle bounded_empty bounded_insert convex_convex_hull inside_frontier_eq_interior bounded_convex_hull)
  2856 
  2857 corollary interior_of_triangle:
  2858     fixes a :: "'a::euclidean_space"
  2859     assumes "DIM('a) = 2"
  2860     shows "interior(convex hull {a,b,c}) =
  2861            convex hull {a,b,c} - (closed_segment a b \<union> closed_segment b c \<union> closed_segment c a)"
  2862   using interior_subset
  2863   by (force simp: frontier_of_triangle [OF assms, symmetric] frontier_def Diff_Diff_Int)
  2864 
  2865 subsection\<open>Subdividing a cell complex\<close>
  2866 
  2867 lemma subdivide_interval:
  2868   fixes x::real
  2869   assumes "a < \<bar>x - y\<bar>" "0 < a"
  2870   obtains n where "n \<in> \<int>" "x < n * a \<and> n * a < y \<or> y <  n * a \<and> n * a < x"
  2871 proof -
  2872   consider "a + x < y" | "a + y < x"
  2873     using assms by linarith
  2874   then show ?thesis
  2875   proof cases
  2876     case 1
  2877     let ?n = "of_int (floor (x/a)) + 1"
  2878     have x: "x < ?n * a"
  2879       by (meson \<open>0 < a\<close> divide_less_eq floor_eq_iff)
  2880     have "?n * a \<le> a + x"
  2881       apply (simp add: algebra_simps)
  2882       by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_div_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
  2883     also have "... < y"
  2884       by (rule 1)
  2885     finally have "?n * a < y" .
  2886     with x show ?thesis
  2887       using Ints_1 Ints_add Ints_of_int that by blast
  2888   next
  2889     case 2
  2890     let ?n = "of_int (floor (y/a)) + 1"
  2891     have y: "y < ?n * a"
  2892       by (meson \<open>0 < a\<close> divide_less_eq floor_eq_iff)
  2893     have "?n * a \<le> a + y"
  2894       apply (simp add: algebra_simps)
  2895       by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_div_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
  2896     also have "... < x"
  2897       by (rule 2)
  2898     finally have "?n * a < x" .
  2899     then show ?thesis
  2900       using Ints_1 Ints_add Ints_of_int that y by blast
  2901   qed
  2902 qed
  2903 
  2904 lemma cell_subdivision_lemma:
  2905   assumes "finite \<F>"
  2906       and "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
  2907       and "\<And>X. X \<in> \<F> \<Longrightarrow> aff_dim X \<le> d"
  2908       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"
  2909       and "finite I"
  2910     shows "\<exists>\<G>. \<Union>\<G> = \<Union>\<F> \<and>
  2911                  finite \<G> \<and>
  2912                  (\<forall>C \<in> \<G>. \<exists>D. D \<in> \<F> \<and> C \<subseteq> D) \<and>
  2913                  (\<forall>C \<in> \<F>. \<forall>x \<in> C. \<exists>D. D \<in> \<G> \<and> x \<in> D \<and> D \<subseteq> C) \<and>
  2914                  (\<forall>X \<in> \<G>. polytope X) \<and>
  2915                  (\<forall>X \<in> \<G>. aff_dim X \<le> d) \<and>
  2916                  (\<forall>X \<in> \<G>. \<forall>Y \<in> \<G>. X \<inter> Y face_of X \<and> X \<inter> Y face_of Y) \<and>
  2917                  (\<forall>X \<in> \<G>. \<forall>x \<in> X. \<forall>y \<in> X. \<forall>a b.
  2918                           (a,b) \<in> I \<longrightarrow> a \<bullet> x \<le> b \<and> a \<bullet> y \<le> b \<or>
  2919                                         a \<bullet> x \<ge> b \<and> a \<bullet> y \<ge> b)"
  2920   using \<open>finite I\<close>
  2921 proof induction
  2922   case empty
  2923   then show ?case
  2924     by (rule_tac x="\<F>" in exI) (auto simp: assms)
  2925 next
  2926   case (insert ab I)
  2927   then obtain \<G> where eq: "\<Union>\<G> = \<Union>\<F>" and "finite \<G>"
  2928                    and sub1: "\<And>C. C \<in> \<G> \<Longrightarrow> \<exists>D. D \<in> \<F> \<and> C \<subseteq> D"
  2929                    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"
  2930                    and poly: "\<And>X. X \<in> \<G> \<Longrightarrow> polytope X"
  2931                    and aff: "\<And>X. X \<in> \<G> \<Longrightarrow> aff_dim X \<le> d"
  2932                    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"
  2933                    and I: "\<And>X x y a b.  \<lbrakk>X \<in> \<G>; x \<in> X; y \<in> X; (a,b) \<in> I\<rbrakk> \<Longrightarrow>
  2934                                     a \<bullet> x \<le> b \<and> a \<bullet> y \<le> b \<or> a \<bullet> x \<ge> b \<and> a \<bullet> y \<ge> b"
  2935     by (auto simp: that)
  2936   obtain a b where "ab = (a,b)"
  2937     by fastforce
  2938   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>"
  2939   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
  2940     by blast
  2941   show ?case
  2942   proof (intro conjI exI)
  2943     show "\<Union>?\<G> = \<Union>\<F>"
  2944       by (force simp: eq [symmetric])
  2945     show "finite ?\<G>"
  2946       using \<open>finite \<G>\<close> by force
  2947     show "\<forall>X \<in> ?\<G>. polytope X"
  2948       by (force simp: poly polytope_Int_polyhedron polyhedron_halfspace_le polyhedron_halfspace_ge)
  2949     show "\<forall>X \<in> ?\<G>. aff_dim X \<le> d"
  2950       by (auto; metis order_trans aff aff_dim_subset inf_le1)
  2951     show "\<forall>X \<in> ?\<G>. \<forall>x \<in> X. \<forall>y \<in> X. \<forall>a b.
  2952                           (a,b) \<in> insert ab I \<longrightarrow> a \<bullet> x \<le> b \<and> a \<bullet> y \<le> b \<or>
  2953                                                   a \<bullet> x \<ge> b \<and> a \<bullet> y \<ge> b"
  2954       using \<open>ab = (a, b)\<close> I by fastforce
  2955     show "\<forall>X \<in> ?\<G>. \<forall>Y \<in> ?\<G>. X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
  2956       by (auto simp: eqInt halfspace_Int_eq face_of_Int_Int face face_of_halfspace_le face_of_halfspace_ge)
  2957     show "\<forall>C \<in> ?\<G>. \<exists>D. D \<in> \<F> \<and> C \<subseteq> D"
  2958       using sub1 by force
  2959     show "\<forall>C\<in>\<F>. \<forall>x\<in>C. \<exists>D. D \<in> ?\<G> \<and> x \<in> D \<and> D \<subseteq> C"
  2960     proof (intro ballI)
  2961       fix C z
  2962       assume "C \<in> \<F>" "z \<in> C"
  2963       with sub2 obtain D where D: "D \<in> \<G>" "z \<in> D" "D \<subseteq> C" by blast
  2964       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>
  2965             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"
  2966         using linorder_class.linear [of "a \<bullet> z" b] D by blast
  2967       then show "\<exists>D. D \<in> ?\<G> \<and> z \<in> D \<and> D \<subseteq> C"
  2968         by blast
  2969     qed
  2970   qed
  2971 qed
  2972 
  2973 
  2974 proposition cell_complex_subdivision_exists:
  2975   fixes \<F> :: "'a::euclidean_space set set"
  2976   assumes "0 < e" "finite \<F>"
  2977       and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
  2978       and aff: "\<And>X. X \<in> \<F> \<Longrightarrow> aff_dim X \<le> d"
  2979       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"
  2980   obtains "\<F>'" where "finite \<F>'" "\<Union>\<F>' = \<Union>\<F>" "\<And>X. X \<in> \<F>' \<Longrightarrow> diameter X < e"
  2981                 "\<And>X. X \<in> \<F>' \<Longrightarrow> polytope X" "\<And>X. X \<in> \<F>' \<Longrightarrow> aff_dim X \<le> d"
  2982                 "\<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"
  2983                 "\<And>C. C \<in> \<F>' \<Longrightarrow> \<exists>D. D \<in> \<F> \<and> C \<subseteq> D"
  2984                 "\<And>C x. C \<in> \<F> \<and> x \<in> C \<Longrightarrow> \<exists>D. D \<in> \<F>' \<and> x \<in> D \<and> D \<subseteq> C"
  2985 proof -
  2986   have "bounded(\<Union>\<F>)"
  2987     by (simp add: \<open>finite \<F>\<close> poly bounded_Union polytope_imp_bounded)
  2988   then obtain B where "B > 0" and B: "\<And>x. x \<in> \<Union>\<F> \<Longrightarrow> norm x < B"
  2989     by (meson bounded_pos_less)
  2990   define C where "C \<equiv> {z \<in> \<int>. \<bar>z * e / 2 / real DIM('a)\<bar> \<le> B}"
  2991   define I where "I \<equiv> \<Union>i \<in> Basis. \<Union>j \<in> C. { (i::'a, j * e / 2 / DIM('a)) }"
  2992   have "finite C"
  2993     using finite_int_segment [of "-B / (e / 2 / DIM('a))" "B / (e / 2 / DIM('a))"]
  2994     apply (simp add: C_def)
  2995     apply (erule rev_finite_subset)
  2996     using \<open>0 < e\<close>
  2997     apply (auto simp: divide_simps)
  2998     done
  2999   then have "finite I"
  3000     by (simp add: I_def)
  3001   obtain \<F>' where eq: "\<Union>\<F>' = \<Union>\<F>" and "finite \<F>'"
  3002               and poly: "\<And>X. X \<in> \<F>' \<Longrightarrow> polytope X"
  3003               and aff: "\<And>X. X \<in> \<F>' \<Longrightarrow> aff_dim X \<le> d"
  3004               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"
  3005               and I: "\<And>X x y a b.  \<lbrakk>X \<in> \<F>'; x \<in> X; y \<in> X; (a,b) \<in> I\<rbrakk> \<Longrightarrow>
  3006                                      a \<bullet> x \<le> b \<and> a \<bullet> y \<le> b \<or> a \<bullet> x \<ge> b \<and> a \<bullet> y \<ge> b"
  3007               and sub1: "\<And>C. C \<in> \<F>' \<Longrightarrow> \<exists>D. D \<in> \<F> \<and> C \<subseteq> D"
  3008               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"
  3009     apply (rule exE [OF cell_subdivision_lemma])
  3010     using assms \<open>finite I\<close> apply auto
  3011     done
  3012   show ?thesis
  3013   proof (rule_tac \<F>'="\<F>'" in that)
  3014     show "diameter X < e" if "X \<in> \<F>'" for X
  3015     proof -
  3016       have "diameter X \<le> e/2"
  3017       proof (rule diameter_le)
  3018         show "norm (x - y) \<le> e / 2" if "x \<in> X" "y \<in> X" for x y
  3019         proof -
  3020           have "norm x < B" "norm y < B"
  3021             using B \<open>X \<in> \<F>'\<close> eq that by fastforce+
  3022           have "norm (x - y) \<le> (\<Sum>b\<in>Basis. \<bar>(x-y) \<bullet> b\<bar>)"
  3023             by (rule norm_le_l1)
  3024           also have "... \<le> of_nat (DIM('a)) * (e / 2 / DIM('a))"
  3025           proof (rule sum_bounded_above)
  3026             fix i::'a
  3027             assume "i \<in> Basis"
  3028             then have I': "\<And>z b. \<lbrakk>z \<in> C; b = z * e / (2 * real DIM('a))\<rbrakk> \<Longrightarrow> i \<bullet> x \<le> b \<and> i \<bullet> y \<le> b \<or> i \<bullet> x \<ge> b \<and> i \<bullet> y \<ge> b"
  3029               using I \<open>X \<in> \<F>'\<close> that
  3030               by (fastforce simp: I_def)
  3031             show "\<bar>(x - y) \<bullet> i\<bar> \<le> e / 2 / real DIM('a)"
  3032             proof (rule ccontr)
  3033               assume "\<not> \<bar>(x - y) \<bullet> i\<bar> \<le> e / 2 / real DIM('a)"
  3034               then have xyi: "\<bar>i \<bullet> x - i \<bullet> y\<bar> > e / 2 / real DIM('a)"
  3035                 by (simp add: inner_commute inner_diff_right)
  3036               obtain n where "n \<in> \<int>" and n: "i \<bullet> x < n * (e / 2 / real DIM('a)) \<and> n * (e / 2 / real DIM('a)) < i \<bullet> y \<or> i \<bullet> y < n * (e / 2 / real DIM('a)) \<and> n * (e / 2 / real DIM('a)) < i \<bullet> x"
  3037                 using subdivide_interval [OF xyi] DIM_positive \<open>0 < e\<close>
  3038                 by (auto simp: zero_less_divide_iff)
  3039               have "\<bar>i \<bullet> x\<bar> < B"
  3040                 by (metis \<open>i \<in> Basis\<close> \<open>norm x < B\<close> inner_commute norm_bound_Basis_lt)
  3041               have "\<bar>i \<bullet> y\<bar> < B"
  3042                 by (metis \<open>i \<in> Basis\<close> \<open>norm y < B\<close> inner_commute norm_bound_Basis_lt)
  3043               have *: "\<bar>n * e\<bar> \<le> B * (2 * real DIM('a))"
  3044                       if "\<bar>ix\<bar> < B" "\<bar>iy\<bar> < B"
  3045                          and ix: "ix * (2 * real DIM('a)) < n * e"
  3046                          and iy: "n * e < iy * (2 * real DIM('a))" for ix iy
  3047               proof (rule abs_leI)
  3048                 have "iy * (2 * real DIM('a)) \<le> B * (2 * real DIM('a))"
  3049                   by (rule mult_right_mono) (use \<open>\<bar>iy\<bar> < B\<close> in linarith)+
  3050                 then show "n * e \<le> B * (2 * real DIM('a))"
  3051                   using iy by linarith
  3052               next
  3053                 have "- ix * (2 * real DIM('a)) \<le> B * (2 * real DIM('a))"
  3054                   by (rule mult_right_mono) (use \<open>\<bar>ix\<bar> < B\<close> in linarith)+
  3055                 then show "- (n * e) \<le> B * (2 * real DIM('a))"
  3056                   using ix by linarith
  3057               qed
  3058               have "n \<in> C"
  3059                 using \<open>n \<in> \<int>\<close> n  by (auto simp: C_def divide_simps intro: * \<open>\<bar>i \<bullet> x\<bar> < B\<close> \<open>\<bar>i \<bullet> y\<bar> < B\<close>)
  3060               show False
  3061                 using  I' [OF \<open>n \<in> C\<close> refl] n  by auto
  3062             qed
  3063           qed
  3064           also have "... = e / 2"
  3065             by simp
  3066           finally show ?thesis .
  3067         qed
  3068       qed (use \<open>0 < e\<close> in force)
  3069       also have "... < e"
  3070         by (simp add: \<open>0 < e\<close>)
  3071       finally show ?thesis .
  3072     qed
  3073   qed (auto simp: eq poly aff face sub1 sub2 \<open>finite \<F>'\<close>)
  3074 qed
  3075 
  3076 
  3077 subsection\<open>Simplexes\<close>
  3078 
  3079 text\<open>The notion of n-simplex for integer @{term"n \<ge> -1"}\<close>
  3080 definition simplex :: "int \<Rightarrow> 'a::euclidean_space set \<Rightarrow> bool" (infix "simplex" 50)
  3081   where "n simplex S \<equiv> \<exists>C. ~(affine_dependent C) \<and> int(card C) = n + 1 \<and> S = convex hull C"
  3082 
  3083 lemma simplex:
  3084     "n simplex S \<longleftrightarrow> (\<exists>C. finite C \<and>
  3085                        ~(affine_dependent C) \<and>
  3086                        int(card C) = n + 1 \<and>
  3087                        S = convex hull C)"
  3088   by (auto simp add: simplex_def intro: aff_independent_finite)
  3089 
  3090 lemma simplex_convex_hull:
  3091    "~affine_dependent C \<and> int(card C) = n + 1 \<Longrightarrow> n simplex (convex hull C)"
  3092   by (auto simp add: simplex_def)
  3093 
  3094 lemma convex_simplex: "n simplex S \<Longrightarrow> convex S"
  3095   by (metis convex_convex_hull simplex_def)
  3096 
  3097 lemma compact_simplex: "n simplex S \<Longrightarrow> compact S"
  3098   unfolding simplex
  3099   using finite_imp_compact_convex_hull by blast
  3100 
  3101 lemma closed_simplex: "n simplex S \<Longrightarrow> closed S"
  3102   by (simp add: compact_imp_closed compact_simplex)
  3103 
  3104 lemma simplex_imp_polytope:
  3105    "n simplex S \<Longrightarrow> polytope S"
  3106   unfolding simplex_def polytope_def
  3107   using aff_independent_finite by blast
  3108 
  3109 lemma simplex_imp_polyhedron:
  3110    "n simplex S \<Longrightarrow> polyhedron S"
  3111   by (simp add: polytope_imp_polyhedron simplex_imp_polytope)
  3112 
  3113 lemma simplex_dim_ge: "n simplex S \<Longrightarrow> -1 \<le> n"
  3114   by (metis (no_types, hide_lams) aff_dim_geq affine_independent_iff_card diff_add_cancel diff_diff_eq2 simplex_def)
  3115 
  3116 lemma simplex_empty [simp]: "n simplex {} \<longleftrightarrow> n = -1"
  3117 proof
  3118   assume "n simplex {}"
  3119   then show "n = -1"
  3120     unfolding simplex by (metis card_empty convex_hull_eq_empty diff_0 diff_eq_eq of_nat_0)
  3121 next
  3122   assume "n = -1" then show "n simplex {}"
  3123     by (fastforce simp: simplex)
  3124 qed
  3125 
  3126 lemma simplex_minus_1 [simp]: "-1 simplex S \<longleftrightarrow> S = {}"
  3127   by (metis simplex cancel_comm_monoid_add_class.diff_cancel card_0_eq diff_minus_eq_add of_nat_eq_0_iff simplex_empty)
  3128 
  3129 
  3130 lemma aff_dim_simplex:
  3131    "n simplex S \<Longrightarrow> aff_dim S = n"
  3132   by (metis simplex add.commute add_diff_cancel_left' aff_dim_convex_hull affine_independent_iff_card)
  3133 
  3134 lemma zero_simplex_sing: "0 simplex {a}"
  3135   apply (simp add: simplex_def)
  3136   by (metis affine_independent_1 card_empty card_insert_disjoint convex_hull_singleton empty_iff finite.emptyI)
  3137 
  3138 lemma simplex_sing [simp]: "n simplex {a} \<longleftrightarrow> n = 0"
  3139   using aff_dim_simplex aff_dim_sing zero_simplex_sing by blast
  3140 
  3141 lemma simplex_zero: "0 simplex S \<longleftrightarrow> (\<exists>a. S = {a})"
  3142 apply (auto simp: )
  3143   using aff_dim_eq_0 aff_dim_simplex by blast
  3144 
  3145 lemma one_simplex_segment: "a \<noteq> b \<Longrightarrow> 1 simplex closed_segment a b"
  3146   apply (simp add: simplex_def)
  3147   apply (rule_tac x="{a,b}" in exI)
  3148   apply (auto simp: segment_convex_hull)
  3149   done
  3150 
  3151 lemma simplex_segment_cases:
  3152    "(if a = b then 0 else 1) simplex closed_segment a b"
  3153   by (auto simp: one_simplex_segment)
  3154 
  3155 lemma simplex_segment:
  3156    "\<exists>n. n simplex closed_segment a b"
  3157   using simplex_segment_cases by metis
  3158 
  3159 lemma polytope_lowdim_imp_simplex:
  3160   assumes "polytope P" "aff_dim P \<le> 1"
  3161   obtains n where "n simplex P"
  3162 proof (cases "P = {}")
  3163   case True
  3164   then show ?thesis
  3165     by (simp add: that)
  3166 next
  3167   case False
  3168   then show ?thesis
  3169     by (metis assms compact_convex_collinear_segment collinear_aff_dim polytope_imp_compact polytope_imp_convex simplex_segment_cases that)
  3170 qed
  3171 
  3172 lemma simplex_insert_dimplus1:
  3173   fixes n::int
  3174   assumes "n simplex S" and a: "a \<notin> affine hull S"
  3175   shows "(n+1) simplex (convex hull (insert a S))"
  3176 proof -
  3177   obtain C where C: "finite C" "~(affine_dependent C)" "int(card C) = n+1" and S: "S = convex hull C"
  3178     using assms unfolding simplex by force
  3179   show ?thesis
  3180     unfolding simplex
  3181   proof (intro exI conjI)
  3182       have "aff_dim S = n"
  3183         using aff_dim_simplex assms(1) by blast
  3184       moreover have "a \<notin> affine hull C"
  3185         using S a affine_hull_convex_hull by blast
  3186       moreover have "a \<notin> C"
  3187           using S a hull_inc by fastforce
  3188       ultimately show "\<not> affine_dependent (insert a C)"
  3189         by (simp add: C S aff_dim_convex_hull aff_dim_insert affine_independent_iff_card)
  3190   next
  3191     have "a \<notin> C"
  3192       using S a hull_inc by fastforce
  3193     then show "int (card (insert a C)) = n + 1 + 1"
  3194       by (simp add: C)
  3195   next
  3196     show "convex hull insert a S = convex hull (insert a C)"
  3197       by (simp add: S convex_hull_insert_segments)
  3198   qed (use C in auto)
  3199 qed
  3200 
  3201 subsection\<open>Simplicial complexes and triangulations\<close>
  3202 
  3203 definition simplicial_complex where
  3204  "simplicial_complex \<C> \<equiv>
  3205         finite \<C> \<and>
  3206         (\<forall>S \<in> \<C>. \<exists>n. n simplex S) \<and>
  3207         (\<forall>F S. S \<in> \<C> \<and> F face_of S \<longrightarrow> F \<in> \<C>) \<and>
  3208         (\<forall>S S'. S \<in> \<C> \<and> S' \<in> \<C>
  3209                 \<longrightarrow> (S \<inter> S') face_of S \<and> (S \<inter> S') face_of S')"
  3210 
  3211 definition triangulation where
  3212  "triangulation \<T> \<equiv>
  3213         finite \<T> \<and>
  3214         (\<forall>T \<in> \<T>. \<exists>n. n simplex T) \<and>
  3215         (\<forall>T T'. T \<in> \<T> \<and> T' \<in> \<T>
  3216                 \<longrightarrow> (T \<inter> T') face_of T \<and> (T \<inter> T') face_of T')"
  3217 
  3218 
  3219 subsection\<open>Refining a cell complex to a simplicial complex\<close>
  3220 
  3221 lemma convex_hull_insert_Int_eq:
  3222   fixes z :: "'a :: euclidean_space"
  3223   assumes z: "z \<in> rel_interior S"
  3224       and T: "T \<subseteq> rel_frontier S"
  3225       and U: "U \<subseteq> rel_frontier S"
  3226       and "convex S" "convex T" "convex U"
  3227   shows "convex hull (insert z T) \<inter> convex hull (insert z U) = convex hull (insert z (T \<inter> U))"
  3228     (is "?lhs = ?rhs")
  3229 proof
  3230   show "?lhs \<subseteq> ?rhs"
  3231   proof (cases "T={} \<or> U={}")
  3232     case True then show ?thesis by auto
  3233   next
  3234     case False
  3235     then have "T \<noteq> {}" "U \<noteq> {}" by auto
  3236     have TU: "convex (T \<inter> U)"
  3237       by (simp add: \<open>convex T\<close> \<open>convex U\<close> convex_Int)
  3238     have "(\<Union>x\<in>T. closed_segment z x) \<inter> (\<Union>x\<in>U. closed_segment z x)
  3239           \<subseteq> (if T \<inter> U = {} then {z} else UNION (T \<inter> U) (closed_segment z))" (is "_ \<subseteq> ?IF")
  3240     proof clarify
  3241       fix x t u
  3242       assume xt: "x \<in> closed_segment z t"
  3243         and xu: "x \<in> closed_segment z u"
  3244         and "t \<in> T" "u \<in> U"
  3245       then have ne: "t \<noteq> z" "u \<noteq> z"
  3246         using T U z unfolding rel_frontier_def by blast+
  3247       show "x \<in> ?IF"
  3248       proof (cases "x = z")
  3249         case True then show ?thesis by auto
  3250       next
  3251         case False
  3252         have t: "t \<in> closure S"
  3253           using T \<open>t \<in> T\<close> rel_frontier_def by auto
  3254         have u: "u \<in> closure S"
  3255           using U \<open>u \<in> U\<close> rel_frontier_def by auto
  3256         show ?thesis
  3257         proof (cases "t = u")
  3258           case True
  3259           then show ?thesis
  3260             using \<open>t \<in> T\<close> \<open>u \<in> U\<close> xt by auto
  3261         next
  3262           case False
  3263           have tnot: "t \<notin> closed_segment u z"
  3264           proof -
  3265             have "t \<in> closure S - rel_interior S"
  3266               using T \<open>t \<in> T\<close> rel_frontier_def by blast
  3267             then have "t \<notin> open_segment z u"
  3268               by (meson DiffD2 rel_interior_closure_convex_segment [OF \<open>convex S\<close> z u] subsetD)
  3269             then show ?thesis
  3270               by (simp add: \<open>t \<noteq> u\<close> \<open>t \<noteq> z\<close> open_segment_commute open_segment_def)
  3271           qed
  3272           moreover have "u \<notin> closed_segment z t"
  3273             using rel_interior_closure_convex_segment [OF \<open>convex S\<close> z t] \<open>u \<in> U\<close> \<open>u \<noteq> z\<close>
  3274               U [unfolded rel_frontier_def] tnot
  3275             by (auto simp: closed_segment_eq_open)
  3276           ultimately
  3277           have "~(between (t,u) z | between (u,z) t | between (z,t) u)" if "x \<noteq> z"
  3278             using that xt xu
  3279             apply (simp add: between_mem_segment [symmetric])
  3280             by (metis between_commute between_trans_2 between_antisym)
  3281           then have "~ collinear {t, z, u}" if "x \<noteq> z"
  3282             by (auto simp: that collinear_between_cases between_commute)
  3283           moreover have "collinear {t, z, x}"
  3284             by (metis closed_segment_commute collinear_2 collinear_closed_segment collinear_triples ends_in_segment(1) insert_absorb insert_absorb2 xt)
  3285           moreover have "collinear {z, x, u}"
  3286             by (metis closed_segment_commute collinear_2 collinear_closed_segment collinear_triples ends_in_segment(1) insert_absorb insert_absorb2 xu)
  3287           ultimately have False
  3288             using collinear_3_trans [of t z x u] \<open>x \<noteq> z\<close> by blast
  3289           then show ?thesis by metis
  3290         qed
  3291       qed
  3292     qed
  3293     then show ?thesis
  3294       using False \<open>convex T\<close> \<open>convex U\<close> TU
  3295       by (simp add: convex_hull_insert_segments hull_same split: if_split_asm)
  3296   qed
  3297   show "?rhs \<subseteq> ?lhs"
  3298     by (metis inf_greatest hull_mono inf.cobounded1 inf.cobounded2 insert_mono)
  3299 qed
  3300 
  3301 lemma simplicial_subdivision_aux:
  3302   assumes "finite \<M>"
  3303       and "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
  3304       and "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C \<le> of_nat n"
  3305       and "\<And>C F. \<lbrakk>C \<in> \<M>; F face_of C\<rbrakk> \<Longrightarrow> F \<in> \<M>"
  3306       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"
  3307     shows "\<exists>\<T>. simplicial_complex \<T> \<and>
  3308                 (\<forall>K \<in> \<T>. aff_dim K \<le> of_nat n) \<and>
  3309                 \<Union>\<T> = \<Union>\<M> \<and>
  3310                 (\<forall>C \<in> \<M>. \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F) \<and>
  3311                 (\<forall>K \<in> \<T>. \<exists>C. C \<in> \<M> \<and> K \<subseteq> C)"
  3312   using assms
  3313 proof (induction n arbitrary: \<M> rule: less_induct)
  3314   case (less n)
  3315   then have poly\<M>: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
  3316       and aff\<M>:    "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C \<le> of_nat n"
  3317       and face\<M>:   "\<And>C F. \<lbrakk>C \<in> \<M>; F face_of C\<rbrakk> \<Longrightarrow> F \<in> \<M>"
  3318       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"
  3319     by metis+
  3320   show ?case
  3321   proof (cases "n \<le> 1")
  3322     case True
  3323     have "\<And>s. \<lbrakk>n \<le> 1; s \<in> \<M>\<rbrakk> \<Longrightarrow> \<exists>m. m simplex s"
  3324       using poly\<M> aff\<M> by (force intro: polytope_lowdim_imp_simplex)
  3325     then show ?thesis
  3326       unfolding simplicial_complex_def
  3327       apply (rule_tac x="\<M>" in exI)
  3328       using True by (auto simp: less.prems)
  3329   next
  3330     case False
  3331     define \<S> where "\<S> \<equiv> {C \<in> \<M>. aff_dim C < n}"
  3332     have "finite \<S>" "\<And>C. C \<in> \<S> \<Longrightarrow> polytope C" "\<And>C. C \<in> \<S> \<Longrightarrow> aff_dim C \<le> int (n - 1)"
  3333          "\<And>C F. \<lbrakk>C \<in> \<S>; F face_of C\<rbrakk> \<Longrightarrow> F \<in> \<S>"
  3334          "\<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"
  3335       using less.prems
  3336       apply (auto simp: \<S>_def)
  3337       by (metis aff_dim_subset face_of_imp_subset less_le not_le)
  3338     with less.IH [of "n-1" \<S>] False
  3339     obtain \<U> where "simplicial_complex \<U>"
  3340            and aff_dim\<U>: "\<And>K. K \<in> \<U> \<Longrightarrow> aff_dim K \<le> int (n - 1)"
  3341            and        "\<Union>\<U> = \<Union>\<S>"
  3342            and fin\<U>:  "\<And>C. C \<in> \<S> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<U> \<and> C = \<Union>F"
  3343            and C\<U>:    "\<And>K. K \<in> \<U> \<Longrightarrow> \<exists>C. C \<in> \<S> \<and> K \<subseteq> C"
  3344       by auto
  3345     then have "finite \<U>"
  3346          and simpl\<U>: "\<And>S. S \<in> \<U> \<Longrightarrow> \<exists>n. n simplex S"
  3347          and face\<U>:  "\<And>F S. \<lbrakk>S \<in> \<U>; F face_of S\<rbrakk> \<Longrightarrow> F \<in> \<U>"
  3348          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'"
  3349       by (auto simp: simplicial_complex_def)
  3350     define \<N> where "\<N> \<equiv> {C \<in> \<M>. aff_dim C = n}"
  3351     have "finite \<N>"
  3352       by (simp add: \<N>_def less.prems(1))
  3353     have poly\<N>: "\<And>C. C \<in> \<N> \<Longrightarrow> polytope C"
  3354       and convex\<N>: "\<And>C. C \<in> \<N> \<Longrightarrow> convex C"
  3355       and closed\<N>: "\<And>C. C \<in> \<N> \<Longrightarrow> closed C"
  3356       by (auto simp: \<N>_def poly\<M> polytope_imp_convex polytope_imp_closed)
  3357     have in_rel_interior: "(SOME z. z \<in> rel_interior C) \<in> rel_interior C" if "C \<in> \<N>" for C
  3358         using that poly\<M> polytope_imp_convex rel_interior_aff_dim some_in_eq by (fastforce simp: \<N>_def)
  3359     have *: "\<exists>T. ~affine_dependent T \<and> card T \<le> n \<and> aff_dim K < n \<and> K = convex hull T"
  3360       if "K \<in> \<U>" for K
  3361     proof -
  3362       obtain r where r: "r simplex K"
  3363         using \<open>K \<in> \<U>\<close> simpl\<U> by blast
  3364       have "r = aff_dim K"
  3365         using \<open>r simplex K\<close> aff_dim_simplex by blast
  3366       with r
  3367       show ?thesis
  3368         unfolding simplex_def
  3369         using False \<open>\<And>K. K \<in> \<U> \<Longrightarrow> aff_dim K \<le> int (n - 1)\<close> that by fastforce
  3370     qed
  3371     have ahK_C_disjoint: "affine hull K \<inter> rel_interior C = {}"
  3372       if "C \<in> \<N>" "K \<in> \<U>" "K \<subseteq> rel_frontier C" for C K
  3373     proof -
  3374       have "convex C" "closed C"
  3375         by (auto simp: convex\<N> closed\<N> \<open>C \<in> \<N>\<close>)
  3376       obtain F where F: "F face_of C" and "F \<noteq> C" "K \<subseteq> F"
  3377       proof -
  3378         obtain L where "L \<in> \<S>" "K \<subseteq> L"
  3379           using \<open>K \<in> \<U>\<close> C\<U> by blast
  3380         have "K \<le> rel_frontier C"
  3381           by (simp add: \<open>K \<subseteq> rel_frontier C\<close>)
  3382         also have "... \<le> C"
  3383           by (simp add: \<open>closed C\<close> rel_frontier_def subset_iff)
  3384         finally have "K \<subseteq> C" .
  3385         have "L \<inter> C face_of C"
  3386           using \<N>_def \<S>_def \<open>C \<in> \<N>\<close> \<open>L \<in> \<S>\<close> intface\<M> by auto
  3387         moreover have "L \<inter> C \<noteq> C"
  3388           using \<open>C \<in> \<N>\<close> \<open>L \<in> \<S>\<close>
  3389           apply (clarsimp simp: \<N>_def \<S>_def)
  3390           by (metis aff_dim_subset inf_le1 not_le)
  3391         moreover have "K \<subseteq> L \<inter> C"
  3392           using \<open>C \<in> \<N>\<close> \<open>L \<in> \<S>\<close> \<open>K \<subseteq> C\<close> \<open>K \<subseteq> L\<close>
  3393           by (auto simp: \<N>_def \<S>_def)
  3394         ultimately show ?thesis using that by metis
  3395       qed
  3396       have "affine hull F \<inter> rel_interior C = {}"
  3397         by (rule affine_hull_face_of_disjoint_rel_interior [OF \<open>convex C\<close> F \<open>F \<noteq> C\<close>])
  3398       with hull_mono [OF \<open>K \<subseteq> F\<close>]
  3399       show "affine hull K \<inter> rel_interior C = {}"
  3400         by fastforce
  3401     qed
  3402     let ?\<T> = "(\<Union>C \<in> \<N>. \<Union>K \<in> \<U> \<inter> Pow (rel_frontier C).
  3403                      {convex hull (insert (SOME z. z \<in> rel_interior C) K)})"
  3404     have "\<exists>\<T>. simplicial_complex \<T> \<and>
  3405               (\<forall>K \<in> \<T>. aff_dim K \<le> of_nat n) \<and>
  3406               (\<forall>C \<in> \<M>. \<exists>F. F \<subseteq> \<T> \<and> C = \<Union>F) \<and>
  3407               (\<forall>K \<in> \<T>. \<exists>C. C \<in> \<M> \<and> K \<subseteq> C)"
  3408     proof (rule exI, intro conjI ballI)
  3409       show "simplicial_complex (\<U> \<union> ?\<T>)"
  3410         unfolding simplicial_complex_def
  3411       proof (intro conjI impI ballI allI)
  3412         show "finite (\<U> \<union> ?\<T>)"
  3413           using \<open>finite \<U>\<close> \<open>finite \<N>\<close> by simp
  3414         show "\<exists>n. n simplex S" if "S \<in> \<U> \<union> ?\<T>" for S
  3415           using that ahK_C_disjoint in_rel_interior simpl\<U> simplex_insert_dimplus1 by fastforce
  3416         show "F \<in> \<U> \<union> ?\<T>" if S: "S \<in> \<U> \<union> ?\<T> \<and> F face_of S" for F S
  3417         proof -
  3418           have "F \<in> \<U>" if "S \<in> \<U>"
  3419             using S face\<U> that by blast
  3420           moreover have "F \<in> \<U> \<union> ?\<T>"
  3421             if "F face_of S" "C \<in> \<N>" "K \<in> \<U>" and "K \<subseteq> rel_frontier C"
  3422               and S: "S = convex hull insert (SOME z. z \<in> rel_interior C) K" for C K
  3423           proof -
  3424             let ?z = "SOME z. z \<in> rel_interior C"
  3425             have "?z \<in> rel_interior C"
  3426               by (simp add: in_rel_interior \<open>C \<in> \<N>\<close>)
  3427             moreover
  3428             obtain I where "\<not> affine_dependent I" "card I \<le> n" "aff_dim K < int n" "K = convex hull I"
  3429               using * [OF \<open>K \<in> \<U>\<close>] by auto
  3430             ultimately have "?z \<notin> affine hull I"
  3431               using ahK_C_disjoint affine_hull_convex_hull that by blast
  3432             have "compact I" "finite I"
  3433               by (auto simp: \<open>\<not> affine_dependent I\<close> aff_independent_finite finite_imp_compact)
  3434             moreover have "F face_of convex hull insert ?z I"
  3435               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)
  3436             ultimately obtain J where "J \<subseteq> insert ?z I" "F = convex hull J"
  3437               using face_of_convex_hull_subset [of "insert ?z I" F] by auto
  3438             show ?thesis
  3439             proof (cases "?z \<in> J")
  3440               case True
  3441               have "F \<in> (\<Union>K\<in>\<U> \<inter> Pow (rel_frontier C). {convex hull insert ?z K})"
  3442               proof
  3443                 have "convex hull (J - {?z}) face_of K"
  3444                   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)
  3445                 then have "convex hull (J - {?z}) \<in> \<U>"
  3446                   by (rule face\<U> [OF \<open>K \<in> \<U>\<close>])
  3447                 moreover
  3448                 have "\<And>x. x \<in> convex hull (J - {?z}) \<Longrightarrow> x \<in> rel_frontier C"
  3449                   by (metis True \<open>J \<subseteq> insert ?z I\<close> \<open>K = convex hull I\<close> subsetD hull_mono subset_insert_iff that(4))
  3450                 ultimately show "convex hull (J - {?z}) \<in> \<U> \<inter> Pow (rel_frontier C)" by auto
  3451                 let ?F = "convex hull insert ?z (convex hull (J - {?z}))"
  3452                 have "F \<subseteq> ?F"
  3453                   apply (clarsimp simp: \<open>F = convex hull J\<close>)
  3454                   by (metis True subsetD hull_mono hull_subset subset_insert_iff)
  3455                 moreover have "?F \<subseteq> F"
  3456                   apply (clarsimp simp: \<open>F = convex hull J\<close>)
  3457                   by (metis (no_types, lifting) True convex_hull_eq_empty convex_hull_insert_segments hull_hull insert_Diff)
  3458                 ultimately
  3459                 show "F \<in> {?F}" by auto
  3460               qed
  3461               with \<open>C\<in>\<N>\<close> show ?thesis by auto
  3462             next
  3463               case False
  3464               then have "F \<in> \<U>"
  3465                 using face_of_convex_hull_affine_independent [OF \<open>\<not> affine_dependent I\<close>]
  3466                 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>)
  3467               then show "F \<in> \<U> \<union> ?\<T>"
  3468                 by blast
  3469             qed
  3470           qed
  3471           ultimately show ?thesis
  3472             using that by auto
  3473         qed
  3474         have "(S \<inter> S' face_of S) \<and> (S \<inter> S' face_of S')"
  3475           if "S \<in> \<U> \<union> ?\<T>" "S' \<in> \<U> \<union> ?\<T>" for S S'
  3476         proof -
  3477           have symmy: "\<lbrakk>\<And>X Y. R X Y \<Longrightarrow> R Y X;
  3478                         \<And>X Y. \<lbrakk>X \<in> \<U>; Y \<in> \<U>\<rbrakk> \<Longrightarrow> R X Y;
  3479                         \<And>X Y. \<lbrakk>X \<in> \<U>; Y \<in> ?\<T>\<rbrakk> \<Longrightarrow> R X Y;
  3480                         \<And>X Y. \<lbrakk>X \<in> ?\<T>; Y \<in> ?\<T>\<rbrakk> \<Longrightarrow> R X Y\<rbrakk> \<Longrightarrow> R S S'" for R
  3481             using that by (metis (no_types, lifting) Un_iff)
  3482           show ?thesis
  3483           proof (rule symmy)
  3484             show "Y \<inter> X face_of Y \<and> Y \<inter> X face_of X"
  3485               if "X \<inter> Y face_of X \<and> X \<inter> Y face_of Y" for X Y :: "'a set"
  3486               by (simp add: inf_commute that)
  3487           next
  3488             show "X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
  3489               if "X \<in> \<U>" and "Y \<in> \<U>" for X Y
  3490               by (simp add: faceI\<U> that)
  3491           next
  3492             show "X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
  3493               if XY: "X \<in> \<U>" "Y \<in> ?\<T>" for X Y
  3494             proof -
  3495               obtain C K
  3496                 where "C \<in> \<N>" "K \<in> \<U>" "K \<subseteq> rel_frontier C"
  3497                 and Y: "Y = convex hull insert (SOME z. z \<in> rel_interior C) K"
  3498                 using XY by blast
  3499               have "convex C"
  3500                 by (simp add: \<open>C \<in> \<N>\<close> convex\<N>)
  3501               have "K \<subseteq> C"
  3502                 by (metis DiffE \<open>C \<in> \<N>\<close> \<open>K \<subseteq> rel_frontier C\<close> closed\<N> closure_closed rel_frontier_def subset_iff)
  3503               let ?z = "(SOME z. z \<in> rel_interior C)"
  3504               have z: "?z \<in> rel_interior C"
  3505                 using \<open>C \<in> \<N>\<close> in_rel_interior by blast
  3506               obtain D where "D \<in> \<S>" "X \<subseteq> D"
  3507                 using C\<U> \<open>X \<in> \<U>\<close> by blast
  3508               have "D \<inter> rel_interior C = (C \<inter> D) \<inter> rel_interior C"
  3509                 using rel_interior_subset by blast
  3510               also have "(C \<inter> D) \<inter> rel_interior C = {}"
  3511               proof (rule face_of_disjoint_rel_interior)
  3512                 show "C \<inter> D face_of C"
  3513                   using \<N>_def \<S>_def \<open>C \<in> \<N>\<close> \<open>D \<in> \<S>\<close> intface\<M> by blast
  3514                 show "C \<inter> D \<noteq> C"
  3515                   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)
  3516               qed
  3517               finally have DC: "D \<inter> rel_interior C = {}" .
  3518               have eq: "X \<inter> convex hull (insert ?z K) = X \<inter> convex hull K"
  3519                 apply (rule Int_convex_hull_insert_rel_exterior [OF \<open>convex C\<close> \<open>K \<subseteq> C\<close> z])
  3520                 using DC by (meson \<open>X \<subseteq> D\<close> disjnt_def disjnt_subset1)
  3521               obtain I where I: "\<not> affine_dependent I"
  3522                          and Keq: "K = convex hull I" and [simp]: "convex hull K = K"
  3523                 using "*" \<open>K \<in> \<U>\<close> by force
  3524               then have "?z \<notin> affine hull I"
  3525                 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
  3526               have "X \<inter> K face_of K"
  3527                 by (simp add: \<open>K \<in> \<U>\<close> faceI\<U> \<open>X \<in> \<U>\<close>)
  3528               also have "... face_of convex hull insert ?z K"
  3529                 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)
  3530               finally have "X \<inter> K face_of convex hull insert ?z K" .
  3531               then show ?thesis
  3532                 using "*" \<open>K \<in> \<U>\<close> faceI\<U> that(1) by (fastforce simp add: Y eq)
  3533             qed
  3534           next
  3535             show "X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
  3536               if XY: "X \<in> ?\<T>" "Y \<in> ?\<T>" for X Y
  3537             proof -
  3538               obtain C K D L
  3539                 where "C \<in> \<N>" "K \<in> \<U>" "K \<subseteq> rel_frontier C"
  3540                 and X: "X = convex hull insert (SOME z. z \<in> rel_interior C) K"
  3541                 and "D \<in> \<N>" "L \<in> \<U>" "L \<subseteq> rel_frontier D"
  3542                 and Y: "Y = convex hull insert (SOME z. z \<in> rel_interior D) L"
  3543                 using XY by blast
  3544               let ?z = "(SOME z. z \<in> rel_interior C)"
  3545               have z: "?z \<in> rel_interior C"
  3546                 using \<open>C \<in> \<N>\<close> in_rel_interior by blast
  3547               have "convex C"
  3548                 by (simp add: \<open>C \<in> \<N>\<close> convex\<N>)
  3549               have "convex K"
  3550                 using "*" \<open>K \<in> \<U>\<close> by blast
  3551               have "convex L"
  3552                 by (meson \<open>L \<in> \<U>\<close> convex_simplex simpl\<U>)
  3553               show ?thesis
  3554               proof (cases "D=C")
  3555                 case True
  3556                 then have "L \<subseteq> rel_frontier C"
  3557                   using \<open>L \<subseteq> rel_frontier D\<close> by auto
  3558                 show ?thesis
  3559                   apply (simp add: X Y True)
  3560                   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>)
  3561                   using face_of_polytope_insert2
  3562                   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)
  3563               next
  3564                 case False
  3565                 have "convex D"
  3566                   by (simp add: \<open>D \<in> \<N>\<close> convex\<N>)
  3567                 have "K \<subseteq> C"
  3568                   by (metis DiffE \<open>C \<in> \<N>\<close> \<open>K \<subseteq> rel_frontier C\<close> closed\<N> closure_closed rel_frontier_def subset_eq)
  3569                 have "L \<subseteq> D"
  3570                   by (metis DiffE \<open>D \<in> \<N>\<close> \<open>L \<subseteq> rel_frontier D\<close> closed\<N> closure_closed rel_frontier_def subset_eq)
  3571                 let ?w = "(SOME w. w \<in> rel_interior D)"
  3572                 have w: "?w \<in> rel_interior D"
  3573                   using \<open>D \<in> \<N>\<close> in_rel_interior by blast
  3574                 have "C \<inter> rel_interior D = (D \<inter> C) \<inter> rel_interior D"
  3575                   using rel_interior_subset by blast
  3576                 also have "(D \<inter> C) \<inter> rel_interior D = {}"
  3577                 proof (rule face_of_disjoint_rel_interior)
  3578                   show "D \<inter> C face_of D"
  3579                     using \<N>_def \<open>C \<in> \<N>\<close> \<open>D \<in> \<N>\<close> intface\<M> by blast
  3580                   have "D \<in> \<M> \<and> aff_dim D = int n"
  3581                     using \<N>_def \<open>D \<in> \<N>\<close> by blast
  3582                   moreover have "C \<in> \<M> \<and> aff_dim C = int n"
  3583                     using \<N>_def \<open>C \<in> \<N>\<close> by blast
  3584                   ultimately show "D \<inter> C \<noteq> D"
  3585                     by (metis False face_of_aff_dim_lt inf.idem inf_le1 intface\<M> not_le poly\<M> polytope_imp_convex)
  3586                 qed
  3587                 finally have CD: "C \<inter> (rel_interior D) = {}" .
  3588                 have zKC: "(convex hull insert ?z K) \<subseteq> C"
  3589                   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)
  3590                 have eq: "convex hull (insert ?z K) \<inter> convex hull (insert ?w L) =
  3591                           convex hull (insert ?z K) \<inter> convex hull L"
  3592                   apply (rule Int_convex_hull_insert_rel_exterior [OF \<open>convex D\<close> \<open>L \<subseteq> D\<close> w])
  3593                   using zKC CD apply (force simp: disjnt_def)
  3594                   done
  3595                 have ch_id: "convex hull K = K" "convex hull L = L"
  3596                   using "*" \<open>K \<in> \<U>\<close> \<open>L \<in> \<U>\<close> hull_same by auto
  3597                 have "convex C"
  3598                   by (simp add: \<open>C \<in> \<N>\<close> convex\<N>)
  3599                 have "convex hull (insert ?z K) \<inter> L = L \<inter> convex hull (insert ?z K)"
  3600                   by blast
  3601                 also have "... = convex hull K \<inter> L"
  3602                 proof (subst Int_convex_hull_insert_rel_exterior [OF \<open>convex C\<close> \<open>K \<subseteq> C\<close> z])
  3603                   have "(C \<inter> D) \<inter> rel_interior C = {}"
  3604                   proof (rule face_of_disjoint_rel_interior)
  3605                     show "C \<inter> D face_of C"
  3606                       using \<N>_def \<open>C \<in> \<N>\<close> \<open>D \<in> \<N>\<close> intface\<M> by blast
  3607                     have "D \<in> \<M>" "aff_dim D = int n"
  3608                       using \<N>_def \<open>D \<in> \<N>\<close> by fastforce+
  3609                     moreover have "C \<in> \<M>" "aff_dim C = int n"
  3610                       using \<N>_def \<open>C \<in> \<N>\<close> by fastforce+
  3611                     ultimately have "aff_dim D + - 1 * aff_dim C \<le> 0"
  3612                       by fastforce
  3613                     then have "\<not> C face_of D"
  3614                       using False \<open>convex D\<close> face_of_aff_dim_lt by fastforce
  3615                     show "C \<inter> D \<noteq> C"
  3616                       using \<open>C \<in> \<M>\<close> \<open>D \<in> \<M>\<close> \<open>\<not> C face_of D\<close> intface\<M> by fastforce
  3617                   qed
  3618                   then have "D \<inter> rel_interior C = {}"
  3619                     by (metis inf.absorb_iff2 inf_assoc inf_sup_aci(1) rel_interior_subset)
  3620                   then show "disjnt L (rel_interior C)"
  3621                     by (meson \<open>L \<subseteq> D\<close> disjnt_def disjnt_subset1)
  3622                 next
  3623                   show "L \<inter> convex hull K = convex hull K \<inter> L"
  3624                     by force
  3625                 qed
  3626                 finally have chKL: "convex hull (insert ?z K) \<inter> L = convex hull K \<inter> L" .
  3627                 have "convex hull insert ?z K \<inter> convex hull L face_of K"
  3628                   by (simp add: \<open>K \<in> \<U>\<close> \<open>L \<in> \<U>\<close> ch_id chKL faceI\<U>)
  3629                 also have "... face_of convex hull insert ?z K"
  3630                 proof -
  3631                   obtain I where I: "\<not> affine_dependent I" "K = convex hull I"
  3632                     using * [OF \<open>K \<in> \<U>\<close>] by auto
  3633                   then have "\<And>a. a \<notin> rel_interior C \<or> a \<notin> affine hull I"
  3634                     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
  3635                   then show ?thesis
  3636                     by (metis I affine_independent_insert face_of_convex_hull_affine_independent hull_insert subset_insertI z)
  3637                 qed
  3638                 finally have 1: "convex hull insert ?z K \<inter> convex hull L face_of convex hull insert ?z K" .
  3639                 have "convex hull insert ?z K \<inter> convex hull L face_of L"
  3640                   by (simp add: \<open>K \<in> \<U>\<close> \<open>L \<in> \<U>\<close> ch_id chKL faceI\<U>)
  3641                 also have "... face_of convex hull insert ?w L"
  3642                 proof -
  3643                   obtain I where I: "\<not> affine_dependent I" "L = convex hull I"
  3644                     using * [OF \<open>L \<in> \<U>\<close>] by auto
  3645                   then have "\<And>a. a \<notin> rel_interior D \<or> a \<notin> affine hull I"
  3646                     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
  3647                   then show ?thesis
  3648                     by (metis I aff_independent_finite convex_convex_hull face_of_convex_hull_insert face_of_refl hull_insert w)
  3649                 qed
  3650                 finally have 2: "convex hull insert ?z K \<inter> convex hull L face_of convex hull insert ?w L" .
  3651                 show ?thesis
  3652                   by (simp add: X Y eq 1 2)
  3653               qed
  3654             qed
  3655           qed
  3656         qed
  3657         then
  3658         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'
  3659           using that by auto
  3660       qed
  3661       show "\<exists>F \<subseteq> \<U> \<union> ?\<T>. C = \<Union>F" if "C \<in> \<M>" for C
  3662       proof (cases "C \<in> \<S>")
  3663         case True
  3664         then show ?thesis
  3665           by (meson UnCI fin\<U> subsetD subsetI)
  3666       next
  3667         case False
  3668         then have "C \<in> \<N>"
  3669           by (simp add: \<N>_def \<S>_def aff\<M> less_le that)
  3670         let ?z = "SOME z. z \<in> rel_interior C"
  3671         have z: "?z \<in> rel_interior C"
  3672           using \<open>C \<in> \<N>\<close> in_rel_interior by blast
  3673         let ?F = "\<Union>K \<in> \<U> \<inter> Pow (rel_frontier C). {convex hull (insert ?z K)}"
  3674         have "?F \<subseteq> ?\<T>"
  3675           using \<open>C \<in> \<N>\<close> by blast
  3676         moreover have "C \<subseteq> \<Union>?F"
  3677         proof
  3678           fix x
  3679           assume "x \<in> C"
  3680           have "convex C"
  3681             using \<open>C \<in> \<N>\<close> convex\<N> by blast
  3682           have "bounded C"
  3683             using \<open>C \<in> \<N>\<close> by (simp add: poly\<M> polytope_imp_bounded that)
  3684           have "polytope C"
  3685             using \<open>C \<in> \<N>\<close> poly\<N> by auto
  3686           have "\<not> (?z = x \<and> C = {?z})"
  3687             using \<open>C \<in> \<N>\<close> aff_dim_sing [of ?z] \<open>\<not> n \<le> 1\<close> by (force simp: \<N>_def)
  3688           then obtain y where y: "y \<in> rel_frontier C" and xzy: "x \<in> closed_segment ?z y"
  3689             and sub: "open_segment ?z y \<subseteq> rel_interior C"
  3690             by (blast intro: segment_to_rel_frontier [OF \<open>convex C\<close> \<open>bounded C\<close> z \<open>x \<in> C\<close>])
  3691           then obtain F where "y \<in> F" "F face_of C" "F \<noteq> C"
  3692             by (auto simp: rel_frontier_of_polyhedron_alt [OF polytope_imp_polyhedron [OF \<open>polytope C\<close>]])
  3693           then obtain \<G> where "finite \<G>" "\<G> \<subseteq> \<U>" "F = \<Union>\<G>"
  3694             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)
  3695           then obtain K where "y \<in> K" "K \<in> \<G>"
  3696             using \<open>y \<in> F\<close> by blast
  3697           moreover have x: "x \<in> convex hull {?z,y}"
  3698             using segment_convex_hull xzy by auto
  3699           moreover have "convex hull {?z,y} \<subseteq> convex hull insert ?z K"
  3700             by (metis (full_types) \<open>y \<in> K\<close> hull_mono empty_subsetI insertCI insert_subset)
  3701           moreover have "K \<in> \<U>"
  3702             using \<open>K \<in> \<G>\<close> \<open>\<G> \<subseteq> \<U>\<close> by blast
  3703           moreover have "K \<subseteq> rel_frontier C"
  3704             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
  3705           ultimately show "x \<in> \<Union>?F"
  3706             by force
  3707         qed
  3708         moreover
  3709         have "convex hull insert (SOME z. z \<in> rel_interior C) K \<subseteq> C"
  3710           if "K \<in> \<U>" "K \<subseteq> rel_frontier C" for K
  3711         proof (rule hull_minimal)
  3712           show "insert (SOME z. z \<in> rel_interior C) K \<subseteq> C"
  3713             using that \<open>C \<in> \<N>\<close> in_rel_interior rel_interior_subset
  3714             by (force simp: closure_eq rel_frontier_def closed\<N>)
  3715           show "convex C"
  3716             by (simp add: \<open>C \<in> \<N>\<close> convex\<N>)
  3717         qed
  3718         then have "\<Union>?F \<subseteq> C"
  3719           by auto
  3720         ultimately show ?thesis
  3721           by blast
  3722       qed
  3723 
  3724       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
  3725         using that
  3726       proof
  3727         assume "L \<in> \<U>"
  3728         then show ?thesis
  3729           using C\<U> \<S>_def "*" by fastforce
  3730       next
  3731         assume "L \<in> ?\<T>"
  3732         then obtain C K where "C \<in> \<N>"
  3733           and L: "L = convex hull insert (SOME z. z \<in> rel_interior C) K"
  3734           and K: "K \<in> \<U>" "K \<subseteq> rel_frontier C"
  3735           by auto
  3736         then have "convex hull C = C"
  3737           by (meson convex\<N> convex_hull_eq)
  3738         then have "convex C"
  3739           by (metis (no_types) convex_convex_hull)
  3740         have "rel_frontier C \<subseteq> C"
  3741           by (metis DiffE closed\<N> \<open>C \<in> \<N>\<close> closure_closed rel_frontier_def subsetI)
  3742         have "K \<subseteq> C"
  3743           using K \<open>rel_frontier C \<subseteq> C\<close> by blast
  3744         have "C \<in> \<M>"
  3745           using \<N>_def \<open>C \<in> \<N>\<close> by auto
  3746         moreover have "L \<subseteq> C"
  3747           using K L \<open>C \<in> \<N>\<close>
  3748           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)
  3749         ultimately show ?thesis
  3750           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
  3751       qed
  3752       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
  3753         using that by auto
  3754     qed
  3755     then show ?thesis
  3756       apply (rule ex_forward, safe)
  3757         apply (meson Union_iff subsetCE, fastforce)
  3758       by (meson infinite_super simplicial_complex_def)
  3759   qed
  3760 qed
  3761 
  3762 
  3763 lemma simplicial_subdivision_of_cell_complex_lowdim:
  3764   assumes "finite \<M>"
  3765       and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
  3766       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"
  3767       and aff: "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C \<le> d"
  3768   obtains \<T> where "simplicial_complex \<T>" "\<And>K. K \<in> \<T> \<Longrightarrow> aff_dim K \<le> d"
  3769                   "\<Union>\<T> = \<Union>\<M>"
  3770                   "\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F"
  3771                   "\<And>K. K \<in> \<T> \<Longrightarrow> \<exists>C. C \<in> \<M> \<and> K \<subseteq> C"
  3772 proof (cases "d \<ge> 0")
  3773   case True
  3774   then obtain n where n: "d = of_nat n"
  3775     using zero_le_imp_eq_int by blast
  3776   have "\<exists>\<T>. simplicial_complex \<T> \<and>
  3777             (\<forall>K\<in>\<T>. aff_dim K \<le> int n) \<and>
  3778             \<Union>\<T> = \<Union>(\<Union>C\<in>\<M>. {F. F face_of C}) \<and>
  3779             (\<forall>C\<in>\<Union>C\<in>\<M>. {F. F face_of C}.
  3780                 \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F) \<and>
  3781             (\<forall>K\<in>\<T>. \<exists>C. C \<in> (\<Union>C\<in>\<M>. {F. F face_of C}) \<and> K \<subseteq> C)"
  3782   proof (rule simplicial_subdivision_aux)
  3783     show "finite (\<Union>C\<in>\<M>. {F. F face_of C})"
  3784       using \<open>finite \<M>\<close> poly polyhedron_eq_finite_faces polytope_imp_polyhedron by fastforce
  3785     show "polytope F" if "F \<in> (\<Union>C\<in>\<M>. {F. F face_of C})" for F
  3786       using poly that face_of_polytope_polytope by blast
  3787     show "aff_dim F \<le> int n" if "F \<in> (\<Union>C\<in>\<M>. {F. F face_of C})" for F
  3788       using that
  3789       by clarify (metis n aff_dim_subset aff face_of_imp_subset order_trans)
  3790     show "F \<in> (\<Union>C\<in>\<M>. {F. F face_of C})"
  3791       if "G \<in> (\<Union>C\<in>\<M>. {F. F face_of C})" and "F face_of G" for F G
  3792       using that face_of_trans by blast
  3793   next
  3794     show "F1 \<inter> F2 face_of F1 \<and> F1 \<inter> F2 face_of F2"
  3795       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
  3796       using that
  3797       by safe (meson face face_of_Int_subface)+
  3798   qed
  3799   moreover
  3800   have "\<Union>(\<Union>C\<in>\<M>. {F. F face_of C}) = \<Union>\<M>"
  3801     using face_of_imp_subset face by blast
  3802   ultimately show ?thesis
  3803     apply clarify
  3804     apply (rule that, assumption+)
  3805        using n apply blast
  3806       apply (simp_all add: poly face_of_refl polytope_imp_convex)
  3807     using face_of_imp_subset by fastforce
  3808 next
  3809   case False
  3810   then have m1: "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C = -1"
  3811     by (metis aff aff_dim_empty_eq aff_dim_negative_iff dual_order.trans not_less)
  3812   then have face\<M>: "\<And>F S. \<lbrakk>S \<in> \<M>; F face_of S\<rbrakk> \<Longrightarrow> F \<in> \<M>"
  3813     by (metis aff_dim_empty face_of_empty)
  3814   show ?thesis
  3815   proof
  3816     have "\<And>S. S \<in> \<M> \<Longrightarrow> \<exists>n. n simplex S"
  3817       by (metis (no_types) m1 aff_dim_empty simplex_minus_1)
  3818     then show "simplicial_complex \<M>"
  3819       by (auto simp: simplicial_complex_def \<open>finite \<M>\<close> face intro: face\<M>)
  3820     show "aff_dim K \<le> d" if "K \<in> \<M>" for K
  3821       by (simp add: that aff)
  3822     show "\<exists>F. finite F \<and> F \<subseteq> \<M> \<and> C = \<Union>F" if "C \<in> \<M>" for C
  3823       using \<open>C \<in> \<M>\<close> equals0I by auto
  3824     show "\<exists>C. C \<in> \<M> \<and> K \<subseteq> C" if "K \<in> \<M>" for K
  3825       using \<open>K \<in> \<M>\<close> by blast
  3826   qed auto
  3827 qed
  3828 
  3829 proposition simplicial_subdivision_of_cell_complex:
  3830   assumes "finite \<M>"
  3831       and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
  3832       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"
  3833   obtains \<T> where "simplicial_complex \<T>"
  3834                   "\<Union>\<T> = \<Union>\<M>"
  3835                   "\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F"
  3836                   "\<And>K. K \<in> \<T> \<Longrightarrow> \<exists>C. C \<in> \<M> \<and> K \<subseteq> C"
  3837   by (blast intro: simplicial_subdivision_of_cell_complex_lowdim [OF assms aff_dim_le_DIM])
  3838 
  3839 corollary fine_simplicial_subdivision_of_cell_complex:
  3840   assumes "0 < e" "finite \<M>"
  3841       and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
  3842       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"
  3843   obtains \<T> where "simplicial_complex \<T>"
  3844                   "\<And>K. K \<in> \<T> \<Longrightarrow> diameter K < e"
  3845                   "\<Union>\<T> = \<Union>\<M>"
  3846                   "\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F"
  3847                   "\<And>K. K \<in> \<T> \<Longrightarrow> \<exists>C. C \<in> \<M> \<and> K \<subseteq> C"
  3848 proof -
  3849   obtain \<N> where \<N>: "finite \<N>" "\<Union>\<N> = \<Union>\<M>" 
  3850               and diapoly: "\<And>X. X \<in> \<N> \<Longrightarrow> diameter X < e" "\<And>X. X \<in> \<N> \<Longrightarrow> polytope X"
  3851                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"
  3852                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"
  3853                and \<N>covered: "\<And>C. C \<in> \<N> \<Longrightarrow> \<exists>D. D \<in> \<M> \<and> C \<subseteq> D"
  3854     by (blast intro: cell_complex_subdivision_exists [OF \<open>0 < e\<close> \<open>finite \<M>\<close> poly aff_dim_le_DIM face])
  3855   then obtain \<T> where \<T>: "simplicial_complex \<T>" "\<Union>\<T> = \<Union>\<N>"
  3856                    and \<T>covers: "\<And>C. C \<in> \<N> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F"
  3857                    and \<T>covered: "\<And>K. K \<in> \<T> \<Longrightarrow> \<exists>C. C \<in> \<N> \<and> K \<subseteq> C"
  3858     using simplicial_subdivision_of_cell_complex [OF \<open>finite \<N>\<close>] by metis
  3859   show ?thesis
  3860   proof
  3861     show "simplicial_complex \<T>"
  3862       by (rule \<T>)
  3863     show "diameter K < e" if "K \<in> \<T>" for K
  3864       by (metis le_less_trans diapoly \<T>covered diameter_subset polytope_imp_bounded that)
  3865     show "\<Union>\<T> = \<Union>\<M>"
  3866       by (simp add: \<N>(2) \<open>\<Union>\<T> = \<Union>\<N>\<close>)
  3867     show "\<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F" if "C \<in> \<M>" for C
  3868     proof -
  3869       { fix x
  3870         assume "x \<in> C"
  3871         then obtain D where "D \<in> \<T>" "x \<in> D" "D \<subseteq> C"
  3872           using \<N>covers \<open>C \<in> \<M>\<close> \<T>covers by force
  3873         then have "\<exists>X\<in>\<T> \<inter> Pow C. x \<in> X"
  3874           using \<open>D \<in> \<T>\<close> \<open>D \<subseteq> C\<close> \<open>x \<in> D\<close> by blast
  3875       }
  3876       moreover
  3877       have "finite (\<T> \<inter> Pow C)"
  3878         using \<open>simplicial_complex \<T>\<close> simplicial_complex_def by auto
  3879       ultimately show ?thesis
  3880         by (rule_tac x="(\<T> \<inter> Pow C)" in exI) auto
  3881     qed
  3882     show "\<exists>C. C \<in> \<M> \<and> K \<subseteq> C" if "K \<in> \<T>" for K
  3883       by (meson \<N>covered \<T>covered order_trans that)
  3884   qed
  3885 qed
  3886 
  3887 subsection\<open>Some results on cell division with full-dimensional cells only\<close>
  3888 
  3889 lemma convex_Union_fulldim_cells:
  3890   assumes "finite \<S>" and clo: "\<And>C. C \<in> \<S> \<Longrightarrow> closed C" and con: "\<And>C. C \<in> \<S> \<Longrightarrow> convex C"
  3891       and eq: "\<Union>\<S> = U"and  "convex U"
  3892  shows "\<Union>{C \<in> \<S>. aff_dim C = aff_dim U} = U"  (is "?lhs = U")
  3893 proof -
  3894   have "closed U"
  3895     using \<open>finite \<S>\<close> clo eq by blast
  3896   have "?lhs \<subseteq> U"
  3897     using eq by blast
  3898   moreover have "U \<subseteq> ?lhs"
  3899   proof (cases "\<forall>C \<in> \<S>. aff_dim C = aff_dim U")
  3900     case True
  3901     then show ?thesis
  3902       using eq by blast
  3903   next
  3904     case False
  3905     have "closed ?lhs"
  3906       by (simp add: \<open>finite \<S>\<close> clo closed_Union)
  3907     moreover have "U \<subseteq> closure ?lhs"
  3908     proof -
  3909       have "U \<subseteq> closure(\<Inter>{U - C |C. C \<in> \<S> \<and> aff_dim C < aff_dim U})"
  3910       proof (rule Baire [OF \<open>closed U\<close>])
  3911         show "countable {U - C |C. C \<in> \<S> \<and> aff_dim C < aff_dim U}"
  3912           using \<open>finite \<S>\<close> uncountable_infinite by fastforce
  3913         have "\<And>C. C \<in> \<S> \<Longrightarrow> openin (subtopology euclidean U) (U-C)"
  3914           by (metis Sup_upper clo closed_limpt closedin_limpt eq openin_diff openin_subtopology_self)
  3915         then show "openin (subtopology euclidean U) T \<and> U \<subseteq> closure T"
  3916           if "T \<in> {U - C |C. C \<in> \<S> \<and> aff_dim C < aff_dim U}" for T
  3917           using that dense_complement_convex_closed \<open>closed U\<close> \<open>convex U\<close> by auto
  3918       qed
  3919       also have "... \<subseteq> closure ?lhs"
  3920       proof -
  3921         obtain C where "C \<in> \<S>" "aff_dim C < aff_dim U"
  3922           by (metis False Sup_upper aff_dim_subset eq eq_iff not_le)
  3923         have "\<exists>X. X \<in> \<S> \<and> aff_dim X = aff_dim U \<and> x \<in> X"
  3924           if "\<And>V. (\<exists>C. V = U - C \<and> C \<in> \<S> \<and> aff_dim C < aff_dim U) \<Longrightarrow> x \<in> V" for x
  3925         proof -
  3926           have "x \<in> U \<and> x \<in> \<Union>\<S>"
  3927             using \<open>C \<in> \<S>\<close> \<open>aff_dim C < aff_dim U\<close> eq that by blast
  3928           then show ?thesis
  3929             by (metis Diff_iff Sup_upper Union_iff aff_dim_subset dual_order.order_iff_strict eq that)
  3930         qed
  3931         then show ?thesis
  3932           by (auto intro!: closure_mono)
  3933       qed
  3934       finally show ?thesis .
  3935     qed
  3936     ultimately show ?thesis
  3937       using closure_subset_eq by blast
  3938   qed
  3939   ultimately show ?thesis by blast
  3940 qed
  3941 
  3942 proposition fine_triangular_subdivision_of_cell_complex:
  3943   assumes "0 < e" "finite \<M>"
  3944       and poly: "\<And>C. C \<in> \<M> \<Longrightarrow> polytope C"
  3945       and aff: "\<And>C. C \<in> \<M> \<Longrightarrow> aff_dim C = d"
  3946       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"
  3947   obtains \<T> where "triangulation \<T>" "\<And>k. k \<in> \<T> \<Longrightarrow> diameter k < e"
  3948                  "\<And>k. k \<in> \<T> \<Longrightarrow> aff_dim k = d" "\<Union>\<T> = \<Union>\<M>"
  3949                  "\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>f. finite f \<and> f \<subseteq> \<T> \<and> C = \<Union>f"
  3950                  "\<And>k. k \<in> \<T> \<Longrightarrow> \<exists>C. C \<in> \<M> \<and> k \<subseteq> C"
  3951 proof -
  3952   obtain \<T> where "simplicial_complex \<T>"
  3953              and dia\<T>: "\<And>K. K \<in> \<T> \<Longrightarrow> diameter K < e"
  3954              and "\<Union>\<T> = \<Union>\<M>"
  3955              and in\<M>: "\<And>C. C \<in> \<M> \<Longrightarrow> \<exists>F. finite F \<and> F \<subseteq> \<T> \<and> C = \<Union>F"
  3956              and in\<T>: "\<And>K. K \<in> \<T> \<Longrightarrow> \<exists>C. C \<in> \<M> \<and> K \<subseteq> C"
  3957     by (blast intro: fine_simplicial_subdivision_of_cell_complex [OF \<open>e > 0\<close> \<open>finite \<M>\<close> poly face])
  3958   let ?\<T> = "{K \<in> \<T>. aff_dim K = d}"
  3959   show thesis
  3960   proof
  3961     show "triangulation ?\<T>"
  3962       using \<open>simplicial_complex \<T>\<close> by (auto simp: triangulation_def simplicial_complex_def)
  3963     show "diameter L < e" if "L \<in> {K \<in> \<T>. aff_dim K = d}" for L
  3964       using that by (auto simp: dia\<T>)
  3965     show "aff_dim L = d" if "L \<in> {K \<in> \<T>. aff_dim K = d}" for L
  3966       using that by auto
  3967     show "\<exists>F. finite F \<and> F \<subseteq> {K \<in> \<T>. aff_dim K = d} \<and> C = \<Union>F" if "C \<in> \<M>" for C
  3968     proof -
  3969       obtain F where "finite F" "F \<subseteq> \<T>" "C = \<Union>F"
  3970         using in\<M> [OF \<open>C \<in> \<M>\<close>] by auto
  3971       show ?thesis
  3972       proof (intro exI conjI)
  3973         show "finite {K \<in> F. aff_dim K = d}"
  3974           by (simp add: \<open>finite F\<close>)
  3975         show "{K \<in> F. aff_dim K = d} \<subseteq> {K \<in> \<T>. aff_dim K = d}"
  3976           using \<open>F \<subseteq> \<T>\<close> by blast
  3977         have "d = aff_dim C"
  3978           by (simp add: aff that)
  3979         moreover have "\<And>K. K \<in> F \<Longrightarrow> closed K \<and> convex K"
  3980           using \<open>simplicial_complex \<T>\<close> \<open>F \<subseteq> \<T>\<close>
  3981           unfolding simplicial_complex_def by (metis subsetCE \<open>F \<subseteq> \<T>\<close> closed_simplex convex_simplex)
  3982         moreover have "convex (\<Union>F)"
  3983           using \<open>C = \<Union>F\<close> poly polytope_imp_convex that by blast
  3984         ultimately show "C = \<Union>{K \<in> F. aff_dim K = d}"
  3985           by (simp add: convex_Union_fulldim_cells \<open>C = \<Union>F\<close> \<open>finite F\<close>)
  3986       qed
  3987     qed
  3988     then show "\<Union>{K \<in> \<T>. aff_dim K = d} = \<Union>\<M>"
  3989       by auto (meson in\<T> subsetCE)
  3990     show "\<exists>C. C \<in> \<M> \<and> L \<subseteq> C"
  3991       if "L \<in> {K \<in> \<T>. aff_dim K = d}" for L
  3992       using that by (auto simp: in\<T>)
  3993   qed
  3994 qed
  3995 
  3996 end