src/HOL/Analysis/Polytope.thy
author paulson <lp15@cam.ac.uk>
Fri Sep 30 14:05:51 2016 +0100 (2016-09-30)
changeset 63967 2aa42596edc3
parent 63918 6bf55e6e0b75
child 64240 eabf80376aab
permissions -rw-r--r--
new material on paths, etc. Also rationalisation
     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     "(op + a ` T face_of op + a ` S) \<longleftrightarrow> T face_of S"
    22 proof -
    23   have *: "\<And>a T S. T face_of S \<Longrightarrow> (op + a ` T face_of op + 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" "closed 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 
   273 lemma affine_diff_divide:
   274     assumes "affine S" "k \<noteq> 0" "k \<noteq> 1" and xy: "x \<in> S" "y /\<^sub>R (1 - k) \<in> S"
   275       shows "(x - y) /\<^sub>R k \<in> S"
   276 proof -
   277   have "inverse(k) *\<^sub>R (x - y) = (1 - inverse k) *\<^sub>R inverse(1 - k) *\<^sub>R y + inverse(k) *\<^sub>R x"
   278     using assms
   279     by (simp add: algebra_simps) (simp add: scaleR_left_distrib [symmetric] divide_simps)
   280   then show ?thesis
   281     using \<open>affine S\<close> xy by (auto simp: affine_alt)
   282 qed
   283 
   284 lemma face_of_convex_hulls:
   285       assumes S: "finite S" "T \<subseteq> S" and disj: "affine hull T \<inter> convex hull (S - T) = {}"
   286       shows  "(convex hull T) face_of (convex hull S)"
   287 proof -
   288   have fin: "finite T" "finite (S - T)" using assms
   289     by (auto simp: finite_subset)
   290   have *: "x \<in> convex hull T"
   291           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"
   292           for x y w
   293   proof -
   294     have waff: "w \<in> affine hull T"
   295       using convex_hull_subset_affine_hull w by blast
   296     obtain a b where a: "\<And>i. i \<in> S \<Longrightarrow> 0 \<le> a i" and asum: "setsum a S = 1" and aeqx: "(\<Sum>i\<in>S. a i *\<^sub>R i) = x"
   297                  and b: "\<And>i. i \<in> S \<Longrightarrow> 0 \<le> b i" and bsum: "setsum b S = 1" and beqy: "(\<Sum>i\<in>S. b i *\<^sub>R i) = y"
   298       using x y by (auto simp: assms convex_hull_finite)
   299     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"
   300                and u01: "0 < u" "u < 1"
   301       using w by (auto simp: open_segment_image_interval split: if_split_asm)
   302     define c where "c i = (1 - u) * a i + u * b i" for i
   303     have cge0: "\<And>i. i \<in> S \<Longrightarrow> 0 \<le> c i"
   304       using a b u01 by (simp add: c_def)
   305     have sumc1: "setsum c S = 1"
   306       by (simp add: c_def setsum.distrib setsum_distrib_left [symmetric] asum bsum)
   307     have sumci_xy: "(\<Sum>i\<in>S. c i *\<^sub>R i) = (1 - u) *\<^sub>R x + u *\<^sub>R y"
   308       apply (simp add: c_def setsum.distrib scaleR_left_distrib)
   309       by (simp only: scaleR_scaleR [symmetric] Real_Vector_Spaces.scaleR_right.setsum [symmetric] aeqx beqy)
   310     show ?thesis
   311     proof (cases "setsum c (S - T) = 0")
   312       case True
   313       have ci0: "\<And>i. i \<in> (S - T) \<Longrightarrow> c i = 0"
   314         using True cge0 by (simp add: \<open>finite S\<close> setsum_nonneg_eq_0_iff)
   315       have a0: "a i = 0" if "i \<in> (S - T)" for i
   316         using ci0 [OF that] u01 a [of i] b [of i] that
   317         by (simp add: c_def Groups.ordered_comm_monoid_add_class.add_nonneg_eq_0_iff)
   318       have [simp]: "setsum a T = 1"
   319         using assms by (metis setsum.mono_neutral_cong_right a0 asum)
   320       show ?thesis
   321         apply (simp add: convex_hull_finite \<open>finite T\<close>)
   322         apply (rule_tac x=a in exI)
   323         using a0 assms
   324         apply (auto simp: cge0 a aeqx [symmetric] setsum.mono_neutral_right)
   325         done
   326     next
   327       case False
   328       define k where "k = setsum c (S - T)"
   329       have "k > 0" using False
   330         unfolding k_def by (metis DiffD1 antisym_conv cge0 setsum_nonneg not_less)
   331       have weq_sumsum: "w = setsum (\<lambda>x. c x *\<^sub>R x) T + setsum (\<lambda>x. c x *\<^sub>R x) (S - T)"
   332         by (metis (no_types) add.commute S(1) S(2) setsum.subset_diff sumci_xy weq)
   333       show ?thesis
   334       proof (cases "k = 1")
   335         case True
   336         then have "setsum c T = 0"
   337           by (simp add: S k_def setsum_diff sumc1)
   338         then have [simp]: "setsum c (S - T) = 1"
   339           by (simp add: S setsum_diff sumc1)
   340         have ci0: "\<And>i. i \<in> T \<Longrightarrow> c i = 0"
   341           by (meson \<open>finite T\<close> \<open>setsum c T = 0\<close> \<open>T \<subseteq> S\<close> cge0 setsum_nonneg_eq_0_iff subsetCE)
   342         then have [simp]: "(\<Sum>i\<in>S-T. c i *\<^sub>R i) = w"
   343           by (simp add: weq_sumsum)
   344         have "w \<in> convex hull (S - T)"
   345           apply (simp add: convex_hull_finite fin)
   346           apply (rule_tac x=c in exI)
   347           apply (auto simp: cge0 weq True k_def)
   348           done
   349         then show ?thesis
   350           using disj waff by blast
   351       next
   352         case False
   353         then have sumcf: "setsum c T = 1 - k"
   354           by (simp add: S k_def setsum_diff sumc1)
   355         have "(\<Sum>i\<in>T. c i *\<^sub>R i) /\<^sub>R (1 - k) \<in> convex hull T"
   356           apply (simp add: convex_hull_finite fin)
   357           apply (rule_tac x="\<lambda>i. inverse (1-k) * c i" in exI)
   358           apply auto
   359           apply (metis sumcf cge0 inverse_nonnegative_iff_nonnegative mult_nonneg_nonneg S(2) setsum_nonneg subsetCE)
   360           apply (metis False mult.commute right_inverse right_minus_eq setsum_distrib_left sumcf)
   361           by (metis (mono_tags, lifting) scaleR_right.setsum scaleR_scaleR setsum.cong)
   362         with \<open>0 < k\<close>  have "inverse(k) *\<^sub>R (w - setsum (\<lambda>i. c i *\<^sub>R i) T) \<in> affine hull T"
   363           by (simp add: affine_diff_divide [OF affine_affine_hull] False waff convex_hull_subset_affine_hull [THEN subsetD])
   364         moreover have "inverse(k) *\<^sub>R (w - setsum (\<lambda>x. c x *\<^sub>R x) T) \<in> convex hull (S - T)"
   365           apply (simp add: weq_sumsum convex_hull_finite fin)
   366           apply (rule_tac x="\<lambda>i. inverse k * c i" in exI)
   367           using \<open>k > 0\<close> cge0
   368           apply (auto simp: scaleR_right.setsum setsum_distrib_left [symmetric] k_def [symmetric])
   369           done
   370         ultimately show ?thesis
   371           using disj by blast
   372       qed
   373     qed
   374   qed
   375   have [simp]: "convex hull T \<subseteq> convex hull S"
   376     by (simp add: \<open>T \<subseteq> S\<close> hull_mono)
   377   show ?thesis
   378     using open_segment_commute by (auto simp: face_of_def intro: *)
   379 qed
   380 
   381 proposition face_of_convex_hull_insert:
   382    "\<lbrakk>finite S; a \<notin> affine hull S; T face_of convex hull S\<rbrakk> \<Longrightarrow> T face_of convex hull insert a S"
   383   apply (rule face_of_trans, blast)
   384   apply (rule face_of_convex_hulls; force simp: insert_Diff_if)
   385   done
   386 
   387 proposition face_of_affine_trivial:
   388     assumes "affine S" "T face_of S"
   389     shows "T = {} \<or> T = S"
   390 proof (rule ccontr, clarsimp)
   391   assume "T \<noteq> {}" "T \<noteq> S"
   392   then obtain a where "a \<in> T" by auto
   393   then have "a \<in> S"
   394     using \<open>T face_of S\<close> face_of_imp_subset by blast
   395   have "S \<subseteq> T"
   396   proof
   397     fix b  assume "b \<in> S"
   398     show "b \<in> T"
   399     proof (cases "a = b")
   400       case True with \<open>a \<in> T\<close> show ?thesis by auto
   401     next
   402       case False
   403       then have "a \<in> open_segment (2 *\<^sub>R a - b) b"
   404         apply (auto simp: open_segment_def closed_segment_def)
   405         apply (rule_tac x="1/2" in exI)
   406         apply (simp add: algebra_simps)
   407         by (simp add: scaleR_2)
   408       moreover have "2 *\<^sub>R a - b \<in> S"
   409         by (rule mem_affine [OF \<open>affine S\<close> \<open>a \<in> S\<close> \<open>b \<in> S\<close>, of 2 "-1", simplified])
   410       moreover note \<open>b \<in> S\<close> \<open>a \<in> T\<close>
   411       ultimately show ?thesis
   412         by (rule face_ofD [OF \<open>T face_of S\<close>, THEN conjunct2])
   413     qed
   414   qed
   415   then show False
   416     using \<open>T \<noteq> S\<close> \<open>T face_of S\<close> face_of_imp_subset by blast
   417 qed
   418 
   419 
   420 lemma face_of_affine_eq:
   421    "affine S \<Longrightarrow> (T face_of S \<longleftrightarrow> T = {} \<or> T = S)"
   422 using affine_imp_convex face_of_affine_trivial face_of_refl by auto
   423 
   424 
   425 lemma Inter_faces_finite_altbound:
   426     fixes T :: "'a::euclidean_space set set"
   427     assumes cfaI: "\<And>c. c \<in> T \<Longrightarrow> c face_of S"
   428     shows "\<exists>F'. finite F' \<and> F' \<subseteq> T \<and> card F' \<le> DIM('a) + 2 \<and> \<Inter>F' = \<Inter>T"
   429 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'))")
   430   case True
   431   then obtain c where c:
   432        "\<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')"
   433     by metis
   434   define d where "d = rec_nat {c{}} (\<lambda>n r. insert (c r) r)"
   435   have [simp]: "d 0 = {c {}}"
   436     by (simp add: d_def)
   437   have dSuc [simp]: "\<And>n. d (Suc n) = insert (c (d n)) (d n)"
   438     by (simp add: d_def)
   439   have dn_notempty: "d n \<noteq> {}" for n
   440     by (induction n) auto
   441   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
   442   using that
   443   proof (induction n)
   444     case 0
   445     then show ?case by (simp add: c)
   446   next
   447     case (Suc n)
   448     then show ?case by (auto simp: c card_insert_if)
   449   qed
   450   have aff_dim_le: "aff_dim(\<Inter>(d n)) \<le> DIM('a) - int n" if "n \<le> DIM('a) + 2" for n
   451   using that
   452   proof (induction n)
   453     case 0
   454     then show ?case
   455       by (simp add: aff_dim_le_DIM)
   456   next
   457     case (Suc n)
   458     have fs: "\<Inter>d (Suc n) face_of S"
   459       by (meson Suc.prems cfaI dn_le_Suc dn_notempty face_of_Inter subsetCE)
   460     have condn: "convex (\<Inter>d n)"
   461       using Suc.prems nat_le_linear not_less_eq_eq
   462       by (blast intro: face_of_imp_convex cfaI convex_Inter dest: dn_le_Suc)
   463     have fdn: "\<Inter>d (Suc n) face_of \<Inter>d n"
   464       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)
   465     have ne: "\<Inter>d (Suc n) \<noteq> \<Inter>d n"
   466       by (metis (no_types, lifting) Suc.prems Suc_leD c complete_lattice_class.Inf_insert dSuc dn_le_Suc less_irrefl order.trans)
   467     have *: "\<And>m::int. \<And>d. \<And>d'::int. d < d' \<and> d' \<le> m - n \<Longrightarrow> d \<le> m - of_nat(n+1)"
   468       by arith
   469     have "aff_dim (\<Inter>d (Suc n)) < aff_dim (\<Inter>d n)"
   470       by (rule face_of_aff_dim_lt [OF condn fdn ne])
   471     moreover have "aff_dim (\<Inter>d n) \<le> int (DIM('a)) - int n"
   472       using Suc by auto
   473     ultimately
   474     have "aff_dim (\<Inter>d (Suc n)) \<le> int (DIM('a)) - (n+1)" by arith
   475     then show ?case by linarith
   476   qed
   477   have "aff_dim (\<Inter>d (DIM('a) + 2)) \<le> -2"
   478       using aff_dim_le [OF order_refl] by simp
   479   with aff_dim_geq [of "\<Inter>d (DIM('a) + 2)"] show ?thesis
   480     using order.trans by fastforce
   481 next
   482   case False
   483   then show ?thesis
   484     apply simp
   485     apply (erule ex_forward)
   486     by blast
   487 qed
   488 
   489 lemma faces_of_translation:
   490    "{F. F face_of image (\<lambda>x. a + x) S} = image (image (\<lambda>x. a + x)) {F. F face_of S}"
   491 apply (rule subset_antisym, clarify)
   492 apply (auto simp: image_iff)
   493 apply (metis face_of_imp_subset face_of_translation_eq subset_imageE)
   494 done
   495 
   496 proposition face_of_Times:
   497   assumes "F face_of S" and "F' face_of S'"
   498     shows "(F \<times> F') face_of (S \<times> S')"
   499 proof -
   500   have "F \<times> F' \<subseteq> S \<times> S'"
   501     using assms [unfolded face_of_def] by blast
   502   moreover
   503   have "convex (F \<times> F')"
   504     using assms [unfolded face_of_def] by (blast intro: convex_Times)
   505   moreover
   506     have "a \<in> F \<and> a' \<in> F' \<and> b \<in> F \<and> b' \<in> F'"
   507        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')"
   508        for a b a' b' x
   509   proof (cases "b=a \<or> b'=a'")
   510     case True with that show ?thesis
   511       using assms
   512       by (force simp: in_segment dest: face_ofD)
   513   next
   514     case False with assms [unfolded face_of_def] that show ?thesis
   515       by (blast dest!: open_segment_PairD)
   516   qed
   517   ultimately show ?thesis
   518     unfolding face_of_def by blast
   519 qed
   520 
   521 corollary face_of_Times_decomp:
   522     fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
   523     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')"
   524      (is "?lhs = ?rhs")
   525 proof
   526   assume c: ?lhs
   527   show ?rhs
   528   proof (cases "c = {}")
   529     case True then show ?thesis by auto
   530   next
   531     case False
   532     have 1: "fst ` c \<subseteq> S" "snd ` c \<subseteq> S'"
   533       using c face_of_imp_subset by fastforce+
   534     have "convex c"
   535       using c by (metis face_of_imp_convex)
   536     have conv: "convex (fst ` c)" "convex (snd ` c)"
   537       by (simp_all add: \<open>convex c\<close> convex_linear_image fst_linear snd_linear)
   538     have fstab: "a \<in> fst ` c \<and> b \<in> fst ` c"
   539             if "a \<in> S" "b \<in> S" "x \<in> open_segment a b" "(x,x') \<in> c" for a b x x'
   540     proof -
   541       have *: "(x,x') \<in> open_segment (a,x') (b,x')"
   542         using that by (auto simp: in_segment)
   543       show ?thesis
   544         using face_ofD [OF c *] that face_of_imp_subset [OF c] by force
   545     qed
   546     have fst: "fst ` c face_of S"
   547       by (force simp: face_of_def 1 conv fstab)
   548     have sndab: "a' \<in> snd ` c \<and> b' \<in> snd ` c"
   549             if "a' \<in> S'" "b' \<in> S'" "x' \<in> open_segment a' b'" "(x,x') \<in> c" for a' b' x x'
   550     proof -
   551       have *: "(x,x') \<in> open_segment (x,a') (x,b')"
   552         using that by (auto simp: in_segment)
   553       show ?thesis
   554         using face_ofD [OF c *] that face_of_imp_subset [OF c] by force
   555     qed
   556     have snd: "snd ` c face_of S'"
   557       by (force simp: face_of_def 1 conv sndab)
   558     have cc: "rel_interior c \<subseteq> rel_interior (fst ` c) \<times> rel_interior (snd ` c)"
   559       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])
   560     have "c = fst ` c \<times> snd ` c"
   561       apply (rule face_of_eq [OF c])
   562       apply (simp_all add: face_of_Times rel_interior_Times conv fst snd)
   563       using False rel_interior_eq_empty \<open>convex c\<close> cc
   564       apply blast
   565       done
   566     with fst snd show ?thesis by metis
   567   qed
   568 next
   569   assume ?rhs with face_of_Times show ?lhs by auto
   570 qed
   571 
   572 lemma face_of_Times_eq:
   573     fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
   574     shows "(F \<times> F') face_of (S \<times> S') \<longleftrightarrow>
   575            F = {} \<or> F' = {} \<or> F face_of S \<and> F' face_of S'"
   576 by (auto simp: face_of_Times_decomp times_eq_iff)
   577 
   578 lemma hyperplane_face_of_halfspace_le: "{x. a \<bullet> x = b} face_of {x. a \<bullet> x \<le> b}"
   579 proof -
   580   have "{x. a \<bullet> x \<le> b} \<inter> {x. a \<bullet> x = b} = {x. a \<bullet> x = b}"
   581     by auto
   582   with face_of_Int_supporting_hyperplane_le [OF convex_halfspace_le [of a b], of a b]
   583   show ?thesis by auto
   584 qed
   585 
   586 lemma hyperplane_face_of_halfspace_ge: "{x. a \<bullet> x = b} face_of {x. a \<bullet> x \<ge> b}"
   587 proof -
   588   have "{x. a \<bullet> x \<ge> b} \<inter> {x. a \<bullet> x = b} = {x. a \<bullet> x = b}"
   589     by auto
   590   with face_of_Int_supporting_hyperplane_ge [OF convex_halfspace_ge [of b a], of b a]
   591   show ?thesis by auto
   592 qed
   593 
   594 lemma face_of_halfspace_le:
   595   fixes a :: "'n::euclidean_space"
   596   shows "F face_of {x. a \<bullet> x \<le> b} \<longleftrightarrow>
   597          F = {} \<or> F = {x. a \<bullet> x = b} \<or> F = {x. a \<bullet> x \<le> b}"
   598      (is "?lhs = ?rhs")
   599 proof (cases "a = 0")
   600   case True then show ?thesis
   601     using face_of_affine_eq affine_UNIV by auto
   602 next
   603   case False
   604   then have ine: "interior {x. a \<bullet> x \<le> b} \<noteq> {}"
   605     using halfspace_eq_empty_lt interior_halfspace_le by blast
   606   show ?thesis
   607   proof
   608     assume L: ?lhs
   609     have "F \<noteq> {x. a \<bullet> x \<le> b} \<Longrightarrow> F face_of {x. a \<bullet> x = b}"
   610       using False
   611       apply (simp add: frontier_halfspace_le [symmetric] rel_frontier_nonempty_interior [OF ine, symmetric])
   612       apply (rule face_of_subset [OF L])
   613       apply (simp add: face_of_subset_rel_frontier [OF L])
   614       apply (force simp: rel_frontier_def closed_halfspace_le)
   615       done
   616     with L show ?rhs
   617       using affine_hyperplane face_of_affine_eq by blast
   618   next
   619     assume ?rhs
   620     then show ?lhs
   621       by (metis convex_halfspace_le empty_face_of face_of_refl hyperplane_face_of_halfspace_le)
   622   qed
   623 qed
   624 
   625 lemma face_of_halfspace_ge:
   626   fixes a :: "'n::euclidean_space"
   627   shows "F face_of {x. a \<bullet> x \<ge> b} \<longleftrightarrow>
   628          F = {} \<or> F = {x. a \<bullet> x = b} \<or> F = {x. a \<bullet> x \<ge> b}"
   629 using face_of_halfspace_le [of F "-a" "-b"] by simp
   630 
   631 subsection\<open>Exposed faces\<close>
   632 
   633 text\<open>That is, faces that are intersection with supporting hyperplane\<close>
   634 
   635 definition exposed_face_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"
   636                                (infixr "(exposed'_face'_of)" 50)
   637   where "T exposed_face_of S \<longleftrightarrow>
   638          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})"
   639 
   640 lemma empty_exposed_face_of [iff]: "{} exposed_face_of S"
   641   apply (simp add: exposed_face_of_def)
   642   apply (rule_tac x=0 in exI)
   643   apply (rule_tac x=1 in exI, force)
   644   done
   645 
   646 lemma exposed_face_of_refl_eq [simp]: "S exposed_face_of S \<longleftrightarrow> convex S"
   647   apply (simp add: exposed_face_of_def face_of_refl_eq, auto)
   648   apply (rule_tac x=0 in exI)+
   649   apply force
   650   done
   651 
   652 lemma exposed_face_of_refl: "convex S \<Longrightarrow> S exposed_face_of S"
   653   by simp
   654 
   655 lemma exposed_face_of:
   656     "T exposed_face_of S \<longleftrightarrow>
   657      T face_of S \<and>
   658      (T = {} \<or> T = S \<or>
   659       (\<exists>a b. a \<noteq> 0 \<and> S \<subseteq> {x. a \<bullet> x \<le> b} \<and> T = S \<inter> {x. a \<bullet> x = b}))"
   660 proof (cases "T = {}")
   661   case True then show ?thesis
   662     by simp
   663 next
   664   case False
   665   show ?thesis
   666   proof (cases "T = S")
   667     case True then show ?thesis
   668       by (simp add: face_of_refl_eq)
   669   next
   670     case False
   671     with \<open>T \<noteq> {}\<close> show ?thesis
   672       apply (auto simp: exposed_face_of_def)
   673       apply (metis inner_zero_left)
   674       done
   675   qed
   676 qed
   677 
   678 lemma exposed_face_of_Int_supporting_hyperplane_le:
   679    "\<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"
   680 by (force simp: exposed_face_of_def face_of_Int_supporting_hyperplane_le)
   681 
   682 lemma exposed_face_of_Int_supporting_hyperplane_ge:
   683    "\<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"
   684 using exposed_face_of_Int_supporting_hyperplane_le [of S "-a" "-b"] by simp
   685 
   686 proposition exposed_face_of_Int:
   687   assumes "T exposed_face_of S"
   688       and "u exposed_face_of S"
   689     shows "(T \<inter> u) exposed_face_of S"
   690 proof -
   691   obtain a b where T: "S \<inter> {x. a \<bullet> x = b} face_of S"
   692                and S: "S \<subseteq> {x. a \<bullet> x \<le> b}"
   693                and teq: "T = S \<inter> {x. a \<bullet> x = b}"
   694     using assms by (auto simp: exposed_face_of_def)
   695   obtain a' b' where u: "S \<inter> {x. a' \<bullet> x = b'} face_of S"
   696                  and s': "S \<subseteq> {x. a' \<bullet> x \<le> b'}"
   697                  and ueq: "u = S \<inter> {x. a' \<bullet> x = b'}"
   698     using assms by (auto simp: exposed_face_of_def)
   699   have tu: "T \<inter> u face_of S"
   700     using T teq u ueq by (simp add: face_of_Int)
   701   have ss: "S \<subseteq> {x. (a + a') \<bullet> x \<le> b + b'}"
   702     using S s' by (force simp: inner_left_distrib)
   703   show ?thesis
   704     apply (simp add: exposed_face_of_def tu)
   705     apply (rule_tac x="a+a'" in exI)
   706     apply (rule_tac x="b+b'" in exI)
   707     using S s'
   708     apply (fastforce simp: ss inner_left_distrib teq ueq)
   709     done
   710 qed
   711 
   712 proposition exposed_face_of_Inter:
   713     fixes P :: "'a::euclidean_space set set"
   714   assumes "P \<noteq> {}"
   715       and "\<And>T. T \<in> P \<Longrightarrow> T exposed_face_of S"
   716     shows "\<Inter>P exposed_face_of S"
   717 proof -
   718   obtain Q where "finite Q" and QsubP: "Q \<subseteq> P" "card Q \<le> DIM('a) + 2" and IntQ: "\<Inter>Q = \<Inter>P"
   719     using Inter_faces_finite_altbound [of P S] assms [unfolded exposed_face_of]
   720     by force
   721   show ?thesis
   722   proof (cases "Q = {}")
   723     case True then show ?thesis
   724       by (metis Inf_empty Inf_lower IntQ assms ex_in_conv subset_antisym top_greatest)
   725   next
   726     case False
   727     have "Q \<subseteq> {T. T exposed_face_of S}"
   728       using QsubP assms by blast
   729     moreover have "Q \<subseteq> {T. T exposed_face_of S} \<Longrightarrow> \<Inter>Q exposed_face_of S"
   730       using \<open>finite Q\<close> False
   731       apply (induction Q rule: finite_induct)
   732       using exposed_face_of_Int apply fastforce+
   733       done
   734     ultimately show ?thesis
   735       by (simp add: IntQ)
   736   qed
   737 qed
   738 
   739 proposition exposed_face_of_sums:
   740   assumes "convex S" and "convex T"
   741       and "F exposed_face_of {x + y | x y. x \<in> S \<and> y \<in> T}"
   742           (is "F exposed_face_of ?ST")
   743   obtains k l
   744     where "k exposed_face_of S" "l exposed_face_of T"
   745           "F = {x + y | x y. x \<in> k \<and> y \<in> l}"
   746 proof (cases "F = {}")
   747   case True then show ?thesis
   748     using that by blast
   749 next
   750   case False
   751   show ?thesis
   752   proof (cases "F = ?ST")
   753     case True then show ?thesis
   754       using assms exposed_face_of_refl_eq that by blast
   755   next
   756     case False
   757     obtain p where "p \<in> F" using \<open>F \<noteq> {}\<close> by blast
   758     moreover
   759     obtain u z where T: "?ST \<inter> {x. u \<bullet> x = z} face_of ?ST"
   760                  and S: "?ST \<subseteq> {x. u \<bullet> x \<le> z}"
   761                  and feq: "F = ?ST \<inter> {x. u \<bullet> x = z}"
   762       using assms by (auto simp: exposed_face_of_def)
   763     ultimately obtain a0 b0
   764             where p: "p = a0 + b0" and "a0 \<in> S" "b0 \<in> T" and z: "u \<bullet> p = z"
   765       by auto
   766     have lez: "u \<bullet> (x + y) \<le> z" if "x \<in> S" "y \<in> T" for x y
   767       using S that by auto
   768     have sef: "S \<inter> {x. u \<bullet> x = u \<bullet> a0} exposed_face_of S"
   769       apply (rule exposed_face_of_Int_supporting_hyperplane_le [OF \<open>convex S\<close>])
   770       apply (metis p z add_le_cancel_right inner_right_distrib lez [OF _ \<open>b0 \<in> T\<close>])
   771       done
   772     have tef: "T \<inter> {x. u \<bullet> x = u \<bullet> b0} exposed_face_of T"
   773       apply (rule exposed_face_of_Int_supporting_hyperplane_le [OF \<open>convex T\<close>])
   774       apply (metis p z add.commute add_le_cancel_right inner_right_distrib lez [OF \<open>a0 \<in> S\<close>])
   775       done
   776     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"
   777       by (auto simp: feq) (metis inner_right_distrib p z)
   778     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}"
   779       apply (auto simp: feq)
   780       apply (rename_tac x y)
   781       apply (rule_tac x=x in exI)
   782       apply (rule_tac x=y in exI, simp)
   783       using z p \<open>a0 \<in> S\<close> \<open>b0 \<in> T\<close>
   784       apply clarify
   785       apply (simp add: inner_right_distrib)
   786       apply (metis add_le_cancel_right antisym lez [unfolded inner_right_distrib] add.commute)
   787       done
   788     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}}"
   789       by blast
   790     then show ?thesis
   791       by (rule that [OF sef tef])
   792   qed
   793 qed
   794 
   795 subsection\<open>Extreme points of a set: its singleton faces\<close>
   796 
   797 definition extreme_point_of :: "['a::real_vector, 'a set] \<Rightarrow> bool"
   798                                (infixr "(extreme'_point'_of)" 50)
   799   where "x extreme_point_of S \<longleftrightarrow>
   800          x \<in> S \<and> (\<forall>a \<in> S. \<forall>b \<in> S. x \<notin> open_segment a b)"
   801 
   802 lemma extreme_point_of_stillconvex:
   803    "convex S \<Longrightarrow> (x extreme_point_of S \<longleftrightarrow> x \<in> S \<and> convex(S - {x}))"
   804   by (fastforce simp add: convex_contains_segment extreme_point_of_def open_segment_def)
   805 
   806 lemma face_of_singleton:
   807    "{x} face_of S \<longleftrightarrow> x extreme_point_of S"
   808 by (fastforce simp add: extreme_point_of_def face_of_def)
   809 
   810 lemma extreme_point_not_in_REL_INTERIOR:
   811     fixes S :: "'a::real_normed_vector set"
   812     shows "\<lbrakk>x extreme_point_of S; S \<noteq> {x}\<rbrakk> \<Longrightarrow> x \<notin> rel_interior S"
   813 apply (simp add: face_of_singleton [symmetric])
   814 apply (blast dest: face_of_disjoint_rel_interior)
   815 done
   816 
   817 lemma extreme_point_not_in_interior:
   818     fixes S :: "'a::{real_normed_vector, perfect_space} set"
   819     shows "x extreme_point_of S \<Longrightarrow> x \<notin> interior S"
   820 apply (case_tac "S = {x}")
   821 apply (simp add: empty_interior_finite)
   822 by (meson contra_subsetD extreme_point_not_in_REL_INTERIOR interior_subset_rel_interior)
   823 
   824 lemma extreme_point_of_face:
   825      "F face_of S \<Longrightarrow> v extreme_point_of F \<longleftrightarrow> v extreme_point_of S \<and> v \<in> F"
   826   by (meson empty_subsetI face_of_face face_of_singleton insert_subset)
   827 
   828 lemma extreme_point_of_convex_hull:
   829    "x extreme_point_of (convex hull S) \<Longrightarrow> x \<in> S"
   830 apply (simp add: extreme_point_of_stillconvex)
   831 using hull_minimal [of S "(convex hull S) - {x}" convex]
   832 using hull_subset [of S convex]
   833 apply blast
   834 done
   835 
   836 lemma extreme_points_of_convex_hull:
   837    "{x. x extreme_point_of (convex hull S)} \<subseteq> S"
   838 using extreme_point_of_convex_hull by auto
   839 
   840 lemma extreme_point_of_empty [simp]: "~ (x extreme_point_of {})"
   841   by (simp add: extreme_point_of_def)
   842 
   843 lemma extreme_point_of_singleton [iff]: "x extreme_point_of {a} \<longleftrightarrow> x = a"
   844   using extreme_point_of_stillconvex by auto
   845 
   846 lemma extreme_point_of_translation_eq:
   847    "(a + x) extreme_point_of (image (\<lambda>x. a + x) S) \<longleftrightarrow> x extreme_point_of S"
   848 by (auto simp: extreme_point_of_def)
   849 
   850 lemma extreme_points_of_translation:
   851    "{x. x extreme_point_of (image (\<lambda>x. a + x) S)} =
   852     (\<lambda>x. a + x) ` {x. x extreme_point_of S}"
   853 using extreme_point_of_translation_eq
   854 by auto (metis (no_types, lifting) image_iff mem_Collect_eq minus_add_cancel)
   855 
   856 lemma extreme_point_of_Int:
   857    "\<lbrakk>x extreme_point_of S; x extreme_point_of T\<rbrakk> \<Longrightarrow> x extreme_point_of (S \<inter> T)"
   858 by (simp add: extreme_point_of_def)
   859 
   860 lemma extreme_point_of_Int_supporting_hyperplane_le:
   861    "\<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"
   862 apply (simp add: face_of_singleton [symmetric])
   863 by (metis face_of_Int_supporting_hyperplane_le_strong convex_singleton)
   864 
   865 lemma extreme_point_of_Int_supporting_hyperplane_ge:
   866    "\<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"
   867 apply (simp add: face_of_singleton [symmetric])
   868 by (metis face_of_Int_supporting_hyperplane_ge_strong convex_singleton)
   869 
   870 lemma exposed_point_of_Int_supporting_hyperplane_le:
   871    "\<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"
   872 apply (simp add: exposed_face_of_def face_of_singleton)
   873 apply (force simp: extreme_point_of_Int_supporting_hyperplane_le)
   874 done
   875 
   876 lemma exposed_point_of_Int_supporting_hyperplane_ge:
   877     "\<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"
   878 using exposed_point_of_Int_supporting_hyperplane_le [of S "-a" "-b" c]
   879 by simp
   880 
   881 lemma extreme_point_of_convex_hull_insert:
   882    "\<lbrakk>finite S; a \<notin> convex hull S\<rbrakk> \<Longrightarrow> a extreme_point_of (convex hull (insert a S))"
   883 apply (case_tac "a \<in> S")
   884 apply (simp add: hull_inc)
   885 using face_of_convex_hulls [of "insert a S" "{a}"]
   886 apply (auto simp: face_of_singleton hull_same)
   887 done
   888 
   889 subsection\<open>Facets\<close>
   890 
   891 definition facet_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"
   892                     (infixr "(facet'_of)" 50)
   893   where "F facet_of S \<longleftrightarrow> F face_of S \<and> F \<noteq> {} \<and> aff_dim F = aff_dim S - 1"
   894 
   895 lemma facet_of_empty [simp]: "~ S facet_of {}"
   896   by (simp add: facet_of_def)
   897 
   898 lemma facet_of_irrefl [simp]: "~ S facet_of S "
   899   by (simp add: facet_of_def)
   900 
   901 lemma facet_of_imp_face_of: "F facet_of S \<Longrightarrow> F face_of S"
   902   by (simp add: facet_of_def)
   903 
   904 lemma facet_of_imp_subset: "F facet_of S \<Longrightarrow> F \<subseteq> S"
   905   by (simp add: face_of_imp_subset facet_of_def)
   906 
   907 lemma hyperplane_facet_of_halfspace_le:
   908    "a \<noteq> 0 \<Longrightarrow> {x. a \<bullet> x = b} facet_of {x. a \<bullet> x \<le> b}"
   909 unfolding facet_of_def hyperplane_eq_empty
   910 by (auto simp: hyperplane_face_of_halfspace_ge hyperplane_face_of_halfspace_le
   911            DIM_positive Suc_leI of_nat_diff aff_dim_halfspace_le)
   912 
   913 lemma hyperplane_facet_of_halfspace_ge:
   914     "a \<noteq> 0 \<Longrightarrow> {x. a \<bullet> x = b} facet_of {x. a \<bullet> x \<ge> b}"
   915 unfolding facet_of_def hyperplane_eq_empty
   916 by (auto simp: hyperplane_face_of_halfspace_le hyperplane_face_of_halfspace_ge
   917            DIM_positive Suc_leI of_nat_diff aff_dim_halfspace_ge)
   918 
   919 lemma facet_of_halfspace_le:
   920     "F facet_of {x. a \<bullet> x \<le> b} \<longleftrightarrow> a \<noteq> 0 \<and> F = {x. a \<bullet> x = b}"
   921     (is "?lhs = ?rhs")
   922 proof
   923   assume c: ?lhs
   924   with c facet_of_irrefl show ?rhs
   925     by (force simp: aff_dim_halfspace_le facet_of_def face_of_halfspace_le cong: conj_cong split: if_split_asm)
   926 next
   927   assume ?rhs then show ?lhs
   928     by (simp add: hyperplane_facet_of_halfspace_le)
   929 qed
   930 
   931 lemma facet_of_halfspace_ge:
   932     "F facet_of {x. a \<bullet> x \<ge> b} \<longleftrightarrow> a \<noteq> 0 \<and> F = {x. a \<bullet> x = b}"
   933 using facet_of_halfspace_le [of F "-a" "-b"] by simp
   934 
   935 subsection \<open>Edges: faces of affine dimension 1\<close>
   936 
   937 definition edge_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"  (infixr "(edge'_of)" 50)
   938   where "e edge_of S \<longleftrightarrow> e face_of S \<and> aff_dim e = 1"
   939 
   940 lemma edge_of_imp_subset:
   941    "S edge_of T \<Longrightarrow> S \<subseteq> T"
   942 by (simp add: edge_of_def face_of_imp_subset)
   943 
   944 subsection\<open>Existence of extreme points\<close>
   945 
   946 lemma different_norm_3_collinear_points:
   947   fixes a :: "'a::euclidean_space"
   948   assumes "x \<in> open_segment a b" "norm(a) = norm(b)" "norm(x) = norm(b)"
   949   shows False
   950 proof -
   951   obtain u where "norm ((1 - u) *\<^sub>R a + u *\<^sub>R b) = norm b"
   952              and "a \<noteq> b"
   953              and u01: "0 < u" "u < 1"
   954     using assms by (auto simp: open_segment_image_interval if_splits)
   955   then have "(1 - u) *\<^sub>R a \<bullet> (1 - u) *\<^sub>R a + ((1 - u) * 2) *\<^sub>R a \<bullet> u *\<^sub>R b =
   956              (1 - u * u) *\<^sub>R (a \<bullet> a)"
   957     using assms by (simp add: norm_eq algebra_simps inner_commute)
   958   then have "(1 - u) *\<^sub>R ((1 - u) *\<^sub>R a \<bullet> a + (2 * u) *\<^sub>R  a \<bullet> b) =
   959              (1 - u) *\<^sub>R ((1 + u) *\<^sub>R (a \<bullet> a))"
   960     by (simp add: algebra_simps)
   961   then have "(1 - u) *\<^sub>R (a \<bullet> a) + (2 * u) *\<^sub>R (a \<bullet> b) = (1 + u) *\<^sub>R (a \<bullet> a)"
   962     using u01 by auto
   963   then have "a \<bullet> b = a \<bullet> a"
   964     using u01 by (simp add: algebra_simps)
   965   then have "a = b"
   966     using \<open>norm(a) = norm(b)\<close> norm_eq vector_eq by fastforce
   967   then show ?thesis
   968     using \<open>a \<noteq> b\<close> by force
   969 qed
   970 
   971 proposition extreme_point_exists_convex:
   972   fixes S :: "'a::euclidean_space set"
   973   assumes "compact S" "convex S" "S \<noteq> {}"
   974   obtains x where "x extreme_point_of S"
   975 proof -
   976   obtain x where "x \<in> S" and xsup: "\<And>y. y \<in> S \<Longrightarrow> norm y \<le> norm x"
   977     using distance_attains_sup [of S 0] assms by auto
   978   have False if "a \<in> S" "b \<in> S" and x: "x \<in> open_segment a b" for a b
   979   proof -
   980     have noax: "norm a \<le> norm x" and nobx: "norm b \<le> norm x" using xsup that by auto
   981     have "a \<noteq> b"
   982       using empty_iff open_segment_idem x by auto
   983     have *: "(1 - u) * na + u * nb < norm x" if "na < norm x"  "nb \<le> norm x" "0 < u" "u < 1" for na nb u
   984     proof -
   985       have "(1 - u) * na + u * nb < (1 - u) * norm x + u * nb"
   986         by (simp add: that)
   987       also have "... \<le> (1 - u) * norm x + u * norm x"
   988         by (simp add: that)
   989       finally have "(1 - u) * na + u * nb < (1 - u) * norm x + u * norm x" .
   990       then show ?thesis
   991       using scaleR_collapse [symmetric, of "norm x" u] by auto
   992     qed
   993     have "norm x < norm x" if "norm a < norm x"
   994       using x
   995       apply (clarsimp simp only: open_segment_image_interval \<open>a \<noteq> b\<close> if_False)
   996       apply (rule norm_triangle_lt)
   997       apply (simp add: norm_mult)
   998       using * [of "norm a" "norm b"] nobx that
   999         apply blast
  1000       done
  1001     moreover have "norm x < norm x" if "norm b < norm x"
  1002       using x
  1003       apply (clarsimp simp only: open_segment_image_interval \<open>a \<noteq> b\<close> if_False)
  1004       apply (rule norm_triangle_lt)
  1005       apply (simp add: norm_mult)
  1006       using * [of "norm b" "norm a" "1-u" for u] noax that
  1007         apply (simp add: add.commute)
  1008       done
  1009     ultimately have "~ (norm a < norm x) \<and> ~ (norm b < norm x)"
  1010       by auto
  1011     then show ?thesis
  1012       using different_norm_3_collinear_points noax nobx that(3) by fastforce
  1013   qed
  1014   then show ?thesis
  1015     apply (rule_tac x=x in that)
  1016     apply (force simp: extreme_point_of_def \<open>x \<in> S\<close>)
  1017     done
  1018 qed
  1019 
  1020 subsection\<open>Krein-Milman, the weaker form\<close>
  1021 
  1022 proposition Krein_Milman:
  1023   fixes S :: "'a::euclidean_space set"
  1024   assumes "compact S" "convex S"
  1025     shows "S = closure(convex hull {x. x extreme_point_of S})"
  1026 proof (cases "S = {}")
  1027   case True then show ?thesis   by simp
  1028 next
  1029   case False
  1030   have "closed S"
  1031     by (simp add: \<open>compact S\<close> compact_imp_closed)
  1032   have "closure (convex hull {x. x extreme_point_of S}) \<subseteq> S"
  1033     apply (rule closure_minimal [OF hull_minimal \<open>closed S\<close>])
  1034     using assms
  1035     apply (auto simp: extreme_point_of_def)
  1036     done
  1037   moreover have "u \<in> closure (convex hull {x. x extreme_point_of S})"
  1038                 if "u \<in> S" for u
  1039   proof (rule ccontr)
  1040     assume unot: "u \<notin> closure(convex hull {x. x extreme_point_of S})"
  1041     then obtain a b where "a \<bullet> u < b"
  1042           and ab: "\<And>x. x \<in> closure(convex hull {x. x extreme_point_of S}) \<Longrightarrow> b < a \<bullet> x"
  1043       using separating_hyperplane_closed_point [of "closure(convex hull {x. x extreme_point_of S})"]
  1044       by blast
  1045     have "continuous_on S (op \<bullet> a)"
  1046       by (rule continuous_intros)+
  1047     then obtain m where "m \<in> S" and m: "\<And>y. y \<in> S \<Longrightarrow> a \<bullet> m \<le> a \<bullet> y"
  1048       using continuous_attains_inf [of S "\<lambda>x. a \<bullet> x"] \<open>compact S\<close> \<open>u \<in> S\<close>
  1049       by auto
  1050     define T where "T = S \<inter> {x. a \<bullet> x = a \<bullet> m}"
  1051     have "m \<in> T"
  1052       by (simp add: T_def \<open>m \<in> S\<close>)
  1053     moreover have "compact T"
  1054       by (simp add: T_def compact_Int_closed [OF \<open>compact S\<close> closed_hyperplane])
  1055     moreover have "convex T"
  1056       by (simp add: T_def convex_Int [OF \<open>convex S\<close> convex_hyperplane])
  1057     ultimately obtain v where v: "v extreme_point_of T"
  1058       using extreme_point_exists_convex [of T] by auto
  1059     then have "{v} face_of T"
  1060       by (simp add: face_of_singleton)
  1061     also have "T face_of S"
  1062       by (simp add: T_def m face_of_Int_supporting_hyperplane_ge [OF \<open>convex S\<close>])
  1063     finally have "v extreme_point_of S"
  1064       by (simp add: face_of_singleton)
  1065     then have "b < a \<bullet> v"
  1066       using closure_subset by (simp add: closure_hull hull_inc ab)
  1067     then show False
  1068       using \<open>a \<bullet> u < b\<close> \<open>{v} face_of T\<close> face_of_imp_subset m T_def that by fastforce
  1069   qed
  1070   ultimately show ?thesis
  1071     by blast
  1072 qed
  1073 
  1074 text\<open>Now the sharper form.\<close>
  1075 
  1076 lemma Krein_Milman_Minkowski_aux:
  1077   fixes S :: "'a::euclidean_space set"
  1078   assumes n: "dim S = n" and S: "compact S" "convex S" "0 \<in> S"
  1079     shows "0 \<in> convex hull {x. x extreme_point_of S}"
  1080 using n S
  1081 proof (induction n arbitrary: S rule: less_induct)
  1082   case (less n S) show ?case
  1083   proof (cases "0 \<in> rel_interior S")
  1084     case True with Krein_Milman show ?thesis
  1085       by (metis subsetD convex_convex_hull convex_rel_interior_closure less.prems(2) less.prems(3) rel_interior_subset)
  1086   next
  1087     case False
  1088     have "rel_interior S \<noteq> {}"
  1089       by (simp add: rel_interior_convex_nonempty_aux less)
  1090     then obtain c where c: "c \<in> rel_interior S" by blast
  1091     obtain a where "a \<noteq> 0"
  1092               and le_ay: "\<And>y. y \<in> S \<Longrightarrow> a \<bullet> 0 \<le> a \<bullet> y"
  1093               and less_ay: "\<And>y. y \<in> rel_interior S \<Longrightarrow> a \<bullet> 0 < a \<bullet> y"
  1094       by (blast intro: supporting_hyperplane_rel_boundary intro!: less False)
  1095     have face: "S \<inter> {x. a \<bullet> x = 0} face_of S"
  1096       apply (rule face_of_Int_supporting_hyperplane_ge [OF \<open>convex S\<close>])
  1097       using le_ay by auto
  1098     then have co: "compact (S \<inter> {x. a \<bullet> x = 0})" "convex (S \<inter> {x. a \<bullet> x = 0})"
  1099       using less.prems by (blast intro: face_of_imp_compact face_of_imp_convex)+
  1100     have "a \<bullet> y = 0" if "y \<in> span (S \<inter> {x. a \<bullet> x = 0})" for y
  1101     proof -
  1102       have "y \<in> span {x. a \<bullet> x = 0}"
  1103         by (metis inf.cobounded2 span_mono subsetCE that)
  1104       then show ?thesis
  1105         by (blast intro: span_induct [OF _ subspace_hyperplane])
  1106     qed
  1107     then have "dim (S \<inter> {x. a \<bullet> x = 0}) < n"
  1108       by (metis (no_types) less_ay c subsetD dim_eq_span inf.strict_order_iff
  1109            inf_le1 \<open>dim S = n\<close> not_le rel_interior_subset span_0 span_clauses(1))
  1110     then have "0 \<in> convex hull {x. x extreme_point_of (S \<inter> {x. a \<bullet> x = 0})}"
  1111       by (rule less.IH) (auto simp: co less.prems)
  1112     then show ?thesis
  1113       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)
  1114   qed
  1115 qed
  1116 
  1117 
  1118 theorem Krein_Milman_Minkowski:
  1119   fixes S :: "'a::euclidean_space set"
  1120   assumes "compact S" "convex S"
  1121     shows "S = convex hull {x. x extreme_point_of S}"
  1122 proof
  1123   show "S \<subseteq> convex hull {x. x extreme_point_of S}"
  1124   proof
  1125     fix a assume [simp]: "a \<in> S"
  1126     have 1: "compact (op + (- a) ` S)"
  1127       by (simp add: \<open>compact S\<close> compact_translation)
  1128     have 2: "convex (op + (- a) ` S)"
  1129       by (simp add: \<open>convex S\<close> convex_translation)
  1130     show a_invex: "a \<in> convex hull {x. x extreme_point_of S}"
  1131       using Krein_Milman_Minkowski_aux [OF refl 1 2]
  1132             convex_hull_translation [of "-a"]
  1133       by (auto simp: extreme_points_of_translation translation_assoc)
  1134     qed
  1135 next
  1136   show "convex hull {x. x extreme_point_of S} \<subseteq> S"
  1137   proof -
  1138     have "{a. a extreme_point_of S} \<subseteq> S"
  1139       using extreme_point_of_def by blast
  1140     then show ?thesis
  1141       by (simp add: \<open>convex S\<close> hull_minimal)
  1142   qed
  1143 qed
  1144 
  1145 
  1146 subsection\<open>Applying it to convex hulls of explicitly indicated finite sets\<close>
  1147 
  1148 lemma Krein_Milman_polytope:
  1149   fixes S :: "'a::euclidean_space set"
  1150   shows
  1151    "finite S
  1152        \<Longrightarrow> convex hull S =
  1153            convex hull {x. x extreme_point_of (convex hull S)}"
  1154 by (simp add: Krein_Milman_Minkowski finite_imp_compact_convex_hull)
  1155 
  1156 lemma extreme_points_of_convex_hull_eq:
  1157   fixes S :: "'a::euclidean_space set"
  1158   shows
  1159    "\<lbrakk>compact S; \<And>T. T \<subset> S \<Longrightarrow> convex hull T \<noteq> convex hull S\<rbrakk>
  1160         \<Longrightarrow> {x. x extreme_point_of (convex hull S)} = S"
  1161 by (metis (full_types) Krein_Milman_Minkowski compact_convex_hull convex_convex_hull extreme_points_of_convex_hull psubsetI)
  1162 
  1163 
  1164 lemma extreme_point_of_convex_hull_eq:
  1165   fixes S :: "'a::euclidean_space set"
  1166   shows
  1167    "\<lbrakk>compact S; \<And>T. T \<subset> S \<Longrightarrow> convex hull T \<noteq> convex hull S\<rbrakk>
  1168     \<Longrightarrow> (x extreme_point_of (convex hull S) \<longleftrightarrow> x \<in> S)"
  1169 using extreme_points_of_convex_hull_eq by auto
  1170 
  1171 lemma extreme_point_of_convex_hull_convex_independent:
  1172   fixes S :: "'a::euclidean_space set"
  1173   assumes "compact S" and S: "\<And>a. a \<in> S \<Longrightarrow> a \<notin> convex hull (S - {a})"
  1174   shows "(x extreme_point_of (convex hull S) \<longleftrightarrow> x \<in> S)"
  1175 proof -
  1176   have "convex hull T \<noteq> convex hull S" if "T \<subset> S" for T
  1177   proof -
  1178     obtain a where  "T \<subseteq> S" "a \<in> S" "a \<notin> T" using \<open>T \<subset> S\<close> by blast
  1179     then show ?thesis
  1180       by (metis (full_types) Diff_eq_empty_iff Diff_insert0 S hull_mono hull_subset insert_Diff_single subsetCE)
  1181   qed
  1182   then show ?thesis
  1183     by (rule extreme_point_of_convex_hull_eq [OF \<open>compact S\<close>])
  1184 qed
  1185 
  1186 lemma extreme_point_of_convex_hull_affine_independent:
  1187   fixes S :: "'a::euclidean_space set"
  1188   shows
  1189    "~ affine_dependent S
  1190          \<Longrightarrow> (x extreme_point_of (convex hull S) \<longleftrightarrow> x \<in> S)"
  1191 by (metis aff_independent_finite affine_dependent_def affine_hull_convex_hull extreme_point_of_convex_hull_convex_independent finite_imp_compact hull_inc)
  1192 
  1193 text\<open>Elementary proofs exist, not requiring Euclidean spaces and all this development\<close>
  1194 lemma extreme_point_of_convex_hull_2:
  1195   fixes x :: "'a::euclidean_space"
  1196   shows "x extreme_point_of (convex hull {a,b}) \<longleftrightarrow> x = a \<or> x = b"
  1197 proof -
  1198   have "x extreme_point_of (convex hull {a,b}) \<longleftrightarrow> x \<in> {a,b}"
  1199     by (intro extreme_point_of_convex_hull_affine_independent affine_independent_2)
  1200   then show ?thesis
  1201     by simp
  1202 qed
  1203 
  1204 lemma extreme_point_of_segment:
  1205   fixes x :: "'a::euclidean_space"
  1206   shows
  1207    "x extreme_point_of closed_segment a b \<longleftrightarrow> x = a \<or> x = b"
  1208 by (simp add: extreme_point_of_convex_hull_2 segment_convex_hull)
  1209 
  1210 lemma face_of_convex_hull_subset:
  1211   fixes S :: "'a::euclidean_space set"
  1212   assumes "compact S" and T: "T face_of (convex hull S)"
  1213   obtains s' where "s' \<subseteq> S" "T = convex hull s'"
  1214 apply (rule_tac s' = "{x. x extreme_point_of T}" in that)
  1215 using T extreme_point_of_convex_hull extreme_point_of_face apply blast
  1216 by (metis (no_types) Krein_Milman_Minkowski assms compact_convex_hull convex_convex_hull face_of_imp_compact face_of_imp_convex)
  1217 
  1218 
  1219 proposition face_of_convex_hull_affine_independent:
  1220   fixes S :: "'a::euclidean_space set"
  1221   assumes "~ affine_dependent S"
  1222     shows "(T face_of (convex hull S) \<longleftrightarrow> (\<exists>c. c \<subseteq> S \<and> T = convex hull c))"
  1223           (is "?lhs = ?rhs")
  1224 proof
  1225   assume ?lhs
  1226   then show ?rhs
  1227     by (meson \<open>T face_of convex hull S\<close> aff_independent_finite assms face_of_convex_hull_subset finite_imp_compact)
  1228 next
  1229   assume ?rhs
  1230   then obtain c where "c \<subseteq> S" and T: "T = convex hull c"
  1231     by blast
  1232   have "affine hull c \<inter> affine hull (S - c) = {}"
  1233     apply (rule disjoint_affine_hull [OF assms \<open>c \<subseteq> S\<close>], auto)
  1234     done
  1235   then have "affine hull c \<inter> convex hull (S - c) = {}"
  1236     using convex_hull_subset_affine_hull by fastforce
  1237   then show ?lhs
  1238     by (metis face_of_convex_hulls \<open>c \<subseteq> S\<close> aff_independent_finite assms T)
  1239 qed
  1240 
  1241 lemma facet_of_convex_hull_affine_independent:
  1242   fixes S :: "'a::euclidean_space set"
  1243   assumes "~ affine_dependent S"
  1244     shows "T facet_of (convex hull S) \<longleftrightarrow>
  1245            T \<noteq> {} \<and> (\<exists>u. u \<in> S \<and> T = convex hull (S - {u}))"
  1246           (is "?lhs = ?rhs")
  1247 proof
  1248   assume ?lhs
  1249   then have "T face_of (convex hull S)" "T \<noteq> {}"
  1250         and afft: "aff_dim T = aff_dim (convex hull S) - 1"
  1251     by (auto simp: facet_of_def)
  1252   then obtain c where "c \<subseteq> S" and c: "T = convex hull c"
  1253     by (auto simp: face_of_convex_hull_affine_independent [OF assms])
  1254   then have affs: "aff_dim S = aff_dim c + 1"
  1255     by (metis aff_dim_convex_hull afft eq_diff_eq)
  1256   have "~ affine_dependent c"
  1257     using \<open>c \<subseteq> S\<close> affine_dependent_subset assms by blast
  1258   with affs have "card (S - c) = 1"
  1259     apply (simp add: aff_dim_affine_independent [symmetric] aff_dim_convex_hull)
  1260     by (metis aff_dim_affine_independent aff_independent_finite One_nat_def \<open>c \<subseteq> S\<close> add.commute
  1261                 add_diff_cancel_right' assms card_Diff_subset card_mono of_nat_1 of_nat_diff of_nat_eq_iff)
  1262   then obtain u where u: "u \<in> S - c"
  1263     by (metis DiffI \<open>c \<subseteq> S\<close> aff_independent_finite assms cancel_comm_monoid_add_class.diff_cancel
  1264                 card_Diff_subset subsetI subset_antisym zero_neq_one)
  1265   then have u: "S = insert u c"
  1266     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)
  1267   have "T = convex hull (c - {u})"
  1268     by (metis Diff_empty Diff_insert0 \<open>T facet_of convex hull S\<close> c facet_of_irrefl insert_absorb u)
  1269   with \<open>T \<noteq> {}\<close> show ?rhs
  1270     using c u by auto
  1271 next
  1272   assume ?rhs
  1273   then obtain u where "T \<noteq> {}" "u \<in> S" and u: "T = convex hull (S - {u})"
  1274     by (force simp: facet_of_def)
  1275   then have "\<not> S \<subseteq> {u}"
  1276     using \<open>T \<noteq> {}\<close> u by auto
  1277   have [simp]: "aff_dim (convex hull (S - {u})) = aff_dim (convex hull S) - 1"
  1278     using assms \<open>u \<in> S\<close>
  1279     apply (simp add: aff_dim_convex_hull affine_dependent_def)
  1280     apply (drule bspec, assumption)
  1281     by (metis add_diff_cancel_right' aff_dim_insert insert_Diff [of u S])
  1282   show ?lhs
  1283     apply (subst u)
  1284     apply (simp add: \<open>\<not> S \<subseteq> {u}\<close> facet_of_def face_of_convex_hull_affine_independent [OF assms], blast)
  1285     done
  1286 qed
  1287 
  1288 lemma facet_of_convex_hull_affine_independent_alt:
  1289   fixes S :: "'a::euclidean_space set"
  1290   shows
  1291    "~affine_dependent S
  1292         \<Longrightarrow> (T facet_of (convex hull S) \<longleftrightarrow>
  1293              2 \<le> card S \<and> (\<exists>u. u \<in> S \<and> T = convex hull (S - {u})))"
  1294 apply (simp add: facet_of_convex_hull_affine_independent)
  1295 apply (auto simp: Set.subset_singleton_iff)
  1296 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)
  1297 done
  1298 
  1299 lemma segment_face_of:
  1300   assumes "(closed_segment a b) face_of S"
  1301   shows "a extreme_point_of S" "b extreme_point_of S"
  1302 proof -
  1303   have as: "{a} face_of S"
  1304     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)
  1305   moreover have "{b} face_of S"
  1306   proof -
  1307     have "b \<in> convex hull {a} \<or> b extreme_point_of convex hull {b, a}"
  1308       by (meson extreme_point_of_convex_hull_insert finite.emptyI finite.insertI)
  1309     moreover have "closed_segment a b = convex hull {b, a}"
  1310       using closed_segment_commute segment_convex_hull by blast
  1311     ultimately show ?thesis
  1312       by (metis as assms face_of_face convex_hull_singleton empty_iff face_of_singleton insertE)
  1313     qed
  1314   ultimately show "a extreme_point_of S" "b extreme_point_of S"
  1315     using face_of_singleton by blast+
  1316 qed
  1317 
  1318 
  1319 lemma Krein_Milman_frontier:
  1320   fixes S :: "'a::euclidean_space set"
  1321   assumes "convex S" "compact S"
  1322     shows "S = convex hull (frontier S)"
  1323           (is "?lhs = ?rhs")
  1324 proof
  1325   have "?lhs \<subseteq> convex hull {x. x extreme_point_of S}"
  1326     using Krein_Milman_Minkowski assms by blast
  1327   also have "... \<subseteq> ?rhs"
  1328     apply (rule hull_mono)
  1329     apply (auto simp: frontier_def extreme_point_not_in_interior)
  1330     using closure_subset apply (force simp: extreme_point_of_def)
  1331     done
  1332   finally show "?lhs \<subseteq> ?rhs" .
  1333 next
  1334   have "?rhs \<subseteq> convex hull S"
  1335     by (metis Diff_subset \<open>compact S\<close> closure_closed compact_eq_bounded_closed frontier_def hull_mono)
  1336   also have "... \<subseteq> ?lhs"
  1337     by (simp add: \<open>convex S\<close> hull_same)
  1338   finally show "?rhs \<subseteq> ?lhs" .
  1339 qed
  1340 
  1341 subsection\<open>Polytopes\<close>
  1342 
  1343 definition polytope where
  1344  "polytope S \<equiv> \<exists>v. finite v \<and> S = convex hull v"
  1345 
  1346 lemma polytope_translation_eq: "polytope (image (\<lambda>x. a + x) S) \<longleftrightarrow> polytope S"
  1347 apply (simp add: polytope_def, safe)
  1348 apply (metis convex_hull_translation finite_imageI translation_galois)
  1349 by (metis convex_hull_translation finite_imageI)
  1350 
  1351 lemma polytope_linear_image: "\<lbrakk>linear f; polytope p\<rbrakk> \<Longrightarrow> polytope(image f p)"
  1352   unfolding polytope_def using convex_hull_linear_image by blast
  1353 
  1354 lemma polytope_empty: "polytope {}"
  1355   using convex_hull_empty polytope_def by blast
  1356 
  1357 lemma polytope_convex_hull: "finite S \<Longrightarrow> polytope(convex hull S)"
  1358   using polytope_def by auto
  1359 
  1360 lemma polytope_Times: "\<lbrakk>polytope S; polytope T\<rbrakk> \<Longrightarrow> polytope(S \<times> T)"
  1361   unfolding polytope_def
  1362   by (metis finite_cartesian_product convex_hull_Times)
  1363 
  1364 lemma face_of_polytope_polytope:
  1365   fixes S :: "'a::euclidean_space set"
  1366   shows "\<lbrakk>polytope S; F face_of S\<rbrakk> \<Longrightarrow> polytope F"
  1367 unfolding polytope_def
  1368 by (meson face_of_convex_hull_subset finite_imp_compact finite_subset)
  1369 
  1370 lemma finite_polytope_faces:
  1371   fixes S :: "'a::euclidean_space set"
  1372   assumes "polytope S"
  1373   shows "finite {F. F face_of S}"
  1374 proof -
  1375   obtain v where "finite v" "S = convex hull v"
  1376     using assms polytope_def by auto
  1377   have "finite (op hull convex ` {T. T \<subseteq> v})"
  1378     by (simp add: \<open>finite v\<close>)
  1379   moreover have "{F. F face_of S} \<subseteq> (op hull convex ` {T. T \<subseteq> v})"
  1380     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)
  1381   ultimately show ?thesis
  1382     by (blast intro: finite_subset)
  1383 qed
  1384 
  1385 lemma finite_polytope_facets:
  1386   assumes "polytope S"
  1387   shows "finite {T. T facet_of S}"
  1388 by (simp add: assms facet_of_def finite_polytope_faces)
  1389 
  1390 lemma polytope_scaling:
  1391   assumes "polytope S"  shows "polytope (image (\<lambda>x. c *\<^sub>R x) S)"
  1392 by (simp add: assms polytope_linear_image)
  1393 
  1394 lemma polytope_imp_compact:
  1395   fixes S :: "'a::real_normed_vector set"
  1396   shows "polytope S \<Longrightarrow> compact S"
  1397 by (metis finite_imp_compact_convex_hull polytope_def)
  1398 
  1399 lemma polytope_imp_convex: "polytope S \<Longrightarrow> convex S"
  1400   by (metis convex_convex_hull polytope_def)
  1401 
  1402 lemma polytope_imp_closed:
  1403   fixes S :: "'a::real_normed_vector set"
  1404   shows "polytope S \<Longrightarrow> closed S"
  1405 by (simp add: compact_imp_closed polytope_imp_compact)
  1406 
  1407 lemma polytope_imp_bounded:
  1408   fixes S :: "'a::real_normed_vector set"
  1409   shows "polytope S \<Longrightarrow> bounded S"
  1410 by (simp add: compact_imp_bounded polytope_imp_compact)
  1411 
  1412 lemma polytope_interval: "polytope(cbox a b)"
  1413   unfolding polytope_def by (meson closed_interval_as_convex_hull)
  1414 
  1415 lemma polytope_sing: "polytope {a}"
  1416   using polytope_def by force
  1417 
  1418 
  1419 subsection\<open>Polyhedra\<close>
  1420 
  1421 definition polyhedron where
  1422  "polyhedron S \<equiv>
  1423         \<exists>F. finite F \<and>
  1424             S = \<Inter> F \<and>
  1425             (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b})"
  1426 
  1427 lemma polyhedron_Int [intro,simp]:
  1428    "\<lbrakk>polyhedron S; polyhedron T\<rbrakk> \<Longrightarrow> polyhedron (S \<inter> T)"
  1429   apply (simp add: polyhedron_def, clarify)
  1430   apply (rename_tac F G)
  1431   apply (rule_tac x="F \<union> G" in exI, auto)
  1432   done
  1433 
  1434 lemma polyhedron_UNIV [iff]: "polyhedron UNIV"
  1435   unfolding polyhedron_def
  1436   by (rule_tac x="{}" in exI) auto
  1437 
  1438 lemma polyhedron_Inter [intro,simp]:
  1439    "\<lbrakk>finite F; \<And>S. S \<in> F \<Longrightarrow> polyhedron S\<rbrakk> \<Longrightarrow> polyhedron(\<Inter>F)"
  1440 by (induction F rule: finite_induct) auto
  1441 
  1442 
  1443 lemma polyhedron_empty [iff]: "polyhedron ({} :: 'a :: euclidean_space set)"
  1444 proof -
  1445   have "\<exists>a. a \<noteq> 0 \<and>
  1446              (\<exists>b. {x. (SOME i. i \<in> Basis) \<bullet> x \<le> - 1} = {x. a \<bullet> x \<le> b})"
  1447     by (rule_tac x="(SOME i. i \<in> Basis)" in exI) (force simp: SOME_Basis nonzero_Basis)
  1448   moreover have "\<exists>a b. a \<noteq> 0 \<and>
  1449                        {x. - (SOME i. i \<in> Basis) \<bullet> x \<le> - 1} = {x. a \<bullet> x \<le> b}"
  1450       apply (rule_tac x="-(SOME i. i \<in> Basis)" in exI)
  1451       apply (rule_tac x="-1" in exI)
  1452       apply (simp add: SOME_Basis nonzero_Basis)
  1453       done
  1454   ultimately show ?thesis
  1455     unfolding polyhedron_def
  1456     apply (rule_tac x="{{x. (SOME i. i \<in> Basis) \<bullet> x \<le> -1},
  1457                         {x. -(SOME i. i \<in> Basis) \<bullet> x \<le> -1}}" in exI)
  1458     apply force
  1459     done
  1460 qed
  1461 
  1462 lemma polyhedron_halfspace_le:
  1463   fixes a :: "'a :: euclidean_space"
  1464   shows "polyhedron {x. a \<bullet> x \<le> b}"
  1465 proof (cases "a = 0")
  1466   case True then show ?thesis by auto
  1467 next
  1468   case False
  1469   then show ?thesis
  1470     unfolding polyhedron_def
  1471     by (rule_tac x="{{x. a \<bullet> x \<le> b}}" in exI) auto
  1472 qed
  1473 
  1474 lemma polyhedron_halfspace_ge:
  1475   fixes a :: "'a :: euclidean_space"
  1476   shows "polyhedron {x. a \<bullet> x \<ge> b}"
  1477 using polyhedron_halfspace_le [of "-a" "-b"] by simp
  1478 
  1479 lemma polyhedron_hyperplane:
  1480   fixes a :: "'a :: euclidean_space"
  1481   shows "polyhedron {x. a \<bullet> x = b}"
  1482 proof -
  1483   have "{x. a \<bullet> x = b} = {x. a \<bullet> x \<le> b} \<inter> {x. a \<bullet> x \<ge> b}"
  1484     by force
  1485   then show ?thesis
  1486     by (simp add: polyhedron_halfspace_ge polyhedron_halfspace_le)
  1487 qed
  1488 
  1489 lemma affine_imp_polyhedron:
  1490   fixes S :: "'a :: euclidean_space set"
  1491   shows "affine S \<Longrightarrow> polyhedron S"
  1492 by (metis affine_hull_eq polyhedron_Inter polyhedron_hyperplane affine_hull_finite_intersection_hyperplanes [of S])
  1493 
  1494 lemma polyhedron_imp_closed:
  1495   fixes S :: "'a :: euclidean_space set"
  1496   shows "polyhedron S \<Longrightarrow> closed S"
  1497 apply (simp add: polyhedron_def)
  1498 using closed_halfspace_le by fastforce
  1499 
  1500 lemma polyhedron_imp_convex:
  1501   fixes S :: "'a :: euclidean_space set"
  1502   shows "polyhedron S \<Longrightarrow> convex S"
  1503 apply (simp add: polyhedron_def)
  1504 using convex_Inter convex_halfspace_le by fastforce
  1505 
  1506 lemma polyhedron_affine_hull:
  1507   fixes S :: "'a :: euclidean_space set"
  1508   shows "polyhedron(affine hull S)"
  1509 by (simp add: affine_imp_polyhedron)
  1510 
  1511 
  1512 subsection\<open>Canonical polyhedron representation making facial structure explicit\<close>
  1513 
  1514 lemma polyhedron_Int_affine:
  1515   fixes S :: "'a :: euclidean_space set"
  1516   shows "polyhedron S \<longleftrightarrow>
  1517            (\<exists>F. finite F \<and> S = (affine hull S) \<inter> \<Inter>F \<and>
  1518                 (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}))"
  1519         (is "?lhs = ?rhs")
  1520 proof
  1521   assume ?lhs then show ?rhs
  1522     apply (simp add: polyhedron_def)
  1523     apply (erule ex_forward)
  1524     using hull_subset apply force
  1525     done
  1526 next
  1527   assume ?rhs then show ?lhs
  1528     apply clarify
  1529     apply (erule ssubst)
  1530     apply (force intro: polyhedron_affine_hull polyhedron_halfspace_le)
  1531     done
  1532 qed
  1533 
  1534 proposition rel_interior_polyhedron_explicit:
  1535   assumes "finite F"
  1536       and seq: "S = affine hull S \<inter> \<Inter>F"
  1537       and faceq: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
  1538       and psub: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> affine hull S \<inter> \<Inter>F'"
  1539     shows "rel_interior S = {x \<in> S. \<forall>h \<in> F. a h \<bullet> x < b h}"
  1540 proof -
  1541   have rels: "\<And>x. x \<in> rel_interior S \<Longrightarrow> x \<in> S"
  1542     by (meson IntE mem_rel_interior)
  1543   moreover have "a i \<bullet> x < b i" if x: "x \<in> rel_interior S" and "i \<in> F" for x i
  1544   proof -
  1545     have fif: "F - {i} \<subset> F"
  1546       using \<open>i \<in> F\<close> Diff_insert_absorb Diff_subset set_insert psubsetI by blast
  1547     then have "S \<subset> affine hull S \<inter> \<Inter>(F - {i})"
  1548       by (rule psub)
  1549     then obtain z where ssub: "S \<subseteq> \<Inter>(F - {i})" and zint: "z \<in> \<Inter>(F - {i})"
  1550                     and "z \<notin> S" and zaff: "z \<in> affine hull S"
  1551       by auto
  1552     have "z \<noteq> x"
  1553       using \<open>z \<notin> S\<close> rels x by blast
  1554     have "z \<notin> affine hull S \<inter> \<Inter>F"
  1555       using \<open>z \<notin> S\<close> seq by auto
  1556     then have aiz: "a i \<bullet> z > b i"
  1557       using faceq zint zaff by fastforce
  1558     obtain e where "e > 0" "x \<in> S" and e: "ball x e \<inter> affine hull S \<subseteq> S"
  1559       using x by (auto simp: mem_rel_interior_ball)
  1560     then have ins: "\<And>y. \<lbrakk>norm (x - y) < e; y \<in> affine hull S\<rbrakk> \<Longrightarrow> y \<in> S"
  1561       by (metis IntI subsetD dist_norm mem_ball)
  1562     define \<xi> where "\<xi> = min (1/2) (e / 2 / norm(z - x))"
  1563     have "norm (\<xi> *\<^sub>R x - \<xi> *\<^sub>R z) = norm (\<xi> *\<^sub>R (x - z))"
  1564       by (simp add: \<xi>_def algebra_simps norm_mult)
  1565     also have "... = \<xi> * norm (x - z)"
  1566       using \<open>e > 0\<close> by (simp add: \<xi>_def)
  1567     also have "... < e"
  1568       using \<open>z \<noteq> x\<close> \<open>e > 0\<close> by (simp add: \<xi>_def min_def divide_simps norm_minus_commute)
  1569     finally have lte: "norm (\<xi> *\<^sub>R x - \<xi> *\<^sub>R z) < e" .
  1570     have \<xi>_aff: "\<xi> *\<^sub>R z + (1 - \<xi>) *\<^sub>R x \<in> affine hull S"
  1571       by (metis \<open>x \<in> S\<close> add.commute affine_affine_hull diff_add_cancel hull_inc mem_affine zaff)
  1572     have "\<xi> *\<^sub>R z + (1 - \<xi>) *\<^sub>R x \<in> S"
  1573       apply (rule ins [OF _ \<xi>_aff])
  1574       apply (simp add: algebra_simps lte)
  1575       done
  1576     then obtain l where l: "0 < l" "l < 1" and ls: "(l *\<^sub>R z + (1 - l) *\<^sub>R x) \<in> S"
  1577       apply (rule_tac l = \<xi> in that)
  1578       using \<open>e > 0\<close> \<open>z \<noteq> x\<close>  apply (auto simp: \<xi>_def)
  1579       done
  1580     then have i: "l *\<^sub>R z + (1 - l) *\<^sub>R x \<in> i"
  1581       using seq \<open>i \<in> F\<close> by auto
  1582     have "b i * l + (a i \<bullet> x) * (1 - l) < a i \<bullet> (l *\<^sub>R z + (1 - l) *\<^sub>R x)"
  1583       using l by (simp add: algebra_simps aiz)
  1584     also have "\<dots> \<le> b i" using i l
  1585       using faceq mem_Collect_eq \<open>i \<in> F\<close> by blast
  1586     finally have "(a i \<bullet> x) * (1 - l) < b i * (1 - l)"
  1587       by (simp add: algebra_simps)
  1588     with l show ?thesis
  1589       by simp
  1590   qed
  1591   moreover have "x \<in> rel_interior S"
  1592            if "x \<in> S" and less: "\<And>h. h \<in> F \<Longrightarrow> a h \<bullet> x < b h" for x
  1593   proof -
  1594     have 1: "\<And>h. h \<in> F \<Longrightarrow> x \<in> interior h"
  1595       by (metis interior_halfspace_le mem_Collect_eq less faceq)
  1596     have 2: "\<And>y. \<lbrakk>\<forall>h\<in>F. y \<in> interior h; y \<in> affine hull S\<rbrakk> \<Longrightarrow> y \<in> S"
  1597       by (metis IntI Inter_iff contra_subsetD interior_subset seq)
  1598     show ?thesis
  1599       apply (simp add: rel_interior \<open>x \<in> S\<close>)
  1600       apply (rule_tac x="\<Inter>h\<in>F. interior h" in exI)
  1601       apply (auto simp: \<open>finite F\<close> open_INT 1 2)
  1602       done
  1603   qed
  1604   ultimately show ?thesis by blast
  1605 qed
  1606 
  1607 
  1608 lemma polyhedron_Int_affine_parallel:
  1609   fixes S :: "'a :: euclidean_space set"
  1610   shows "polyhedron S \<longleftrightarrow>
  1611          (\<exists>F. finite F \<and>
  1612               S = (affine hull S) \<inter> (\<Inter>F) \<and>
  1613               (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b} \<and>
  1614                              (\<forall>x \<in> affine hull S. (x + a) \<in> affine hull S)))"
  1615     (is "?lhs = ?rhs")
  1616 proof
  1617   assume ?lhs
  1618   then obtain F where "finite F" and seq: "S = (affine hull S) \<inter> \<Inter>F"
  1619                   and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
  1620     by (fastforce simp add: polyhedron_Int_affine)
  1621   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}"
  1622     by metis
  1623   show ?rhs
  1624   proof -
  1625     have "\<exists>a' b'. a' \<noteq> 0 \<and>
  1626                   affine hull S \<inter> {x. a' \<bullet> x \<le> b'} = affine hull S \<inter> h \<and>
  1627                   (\<forall>w \<in> affine hull S. (w + a') \<in> affine hull S)"
  1628         if "h \<in> F" "~(affine hull S \<subseteq> h)" for h
  1629     proof -
  1630       have "a h \<noteq> 0" and "h = {x. a h \<bullet> x \<le> b h}" "h \<inter> \<Inter>F = \<Inter>F"
  1631         using \<open>h \<in> F\<close> ab by auto
  1632       then have "(affine hull S) \<inter> {x. a h \<bullet> x \<le> b h} \<noteq> {}"
  1633         by (metis (no_types) affine_hull_eq_empty inf.absorb_iff2 inf_assoc inf_bot_right inf_commute seq that(2))
  1634       moreover have "~ (affine hull S \<subseteq> {x. a h \<bullet> x \<le> b h})"
  1635         using \<open>h = {x. a h \<bullet> x \<le> b h}\<close> that(2) by blast
  1636       ultimately show ?thesis
  1637         using affine_parallel_slice [of "affine hull S"]
  1638         by (metis \<open>h = {x. a h \<bullet> x \<le> b h}\<close> affine_affine_hull)
  1639     qed
  1640     then obtain a b
  1641          where ab: "\<And>h. \<lbrakk>h \<in> F; ~ (affine hull S \<subseteq> h)\<rbrakk>
  1642              \<Longrightarrow> a h \<noteq> 0 \<and>
  1643                   affine hull S \<inter> {x. a h \<bullet> x \<le> b h} = affine hull S \<inter> h \<and>
  1644                   (\<forall>w \<in> affine hull S. (w + a h) \<in> affine hull S)"
  1645       by metis
  1646     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})"
  1647       by (subst seq) (auto simp: ab INT_extend_simps)
  1648     show ?thesis
  1649       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)
  1650       apply (intro conjI seq2)
  1651         using \<open>finite F\<close> apply force
  1652        using ab apply blast
  1653        done
  1654   qed
  1655 next
  1656   assume ?rhs then show ?lhs
  1657     apply (simp add: polyhedron_Int_affine)
  1658     by metis
  1659 qed
  1660 
  1661 
  1662 proposition polyhedron_Int_affine_parallel_minimal:
  1663   fixes S :: "'a :: euclidean_space set"
  1664   shows "polyhedron S \<longleftrightarrow>
  1665          (\<exists>F. finite F \<and>
  1666               S = (affine hull S) \<inter> (\<Inter>F) \<and>
  1667               (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b} \<and>
  1668                              (\<forall>x \<in> affine hull S. (x + a) \<in> affine hull S)) \<and>
  1669               (\<forall>F'. F' \<subset> F \<longrightarrow> S \<subset> (affine hull S) \<inter> (\<Inter>F')))"
  1670     (is "?lhs = ?rhs")
  1671 proof
  1672   assume ?lhs
  1673   then obtain f0
  1674            where f0: "finite f0"
  1675                  "S = (affine hull S) \<inter> (\<Inter>f0)"
  1676                    (is "?P f0")
  1677                  "\<forall>h \<in> f0. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b} \<and>
  1678                              (\<forall>x \<in> affine hull S. (x + a) \<in> affine hull S)"
  1679                    (is "?Q f0")
  1680     by (force simp: polyhedron_Int_affine_parallel)
  1681   define n where "n = (LEAST n. \<exists>F. card F = n \<and> finite F \<and> ?P F \<and> ?Q F)"
  1682   have nf: "\<exists>F. card F = n \<and> finite F \<and> ?P F \<and> ?Q F"
  1683     apply (simp add: n_def)
  1684     apply (rule LeastI [where k = "card f0"])
  1685     using f0 apply auto
  1686     done
  1687   then obtain F where F: "card F = n" "finite F" and seq: "?P F" and aff: "?Q F"
  1688     by blast
  1689   then have "~ (finite g \<and> ?P g \<and> ?Q g)" if "card g < n" for g
  1690     using that by (auto simp: n_def dest!: not_less_Least)
  1691   then have *: "~ (?P g \<and> ?Q g)" if "g \<subset> F" for g
  1692     using that \<open>finite F\<close> psubset_card_mono \<open>card F = n\<close>
  1693     by (metis finite_Int inf.strict_order_iff)
  1694   have 1: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subseteq> affine hull S \<inter> \<Inter>F'"
  1695     by (subst seq) blast
  1696   have 2: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<noteq> affine hull S \<inter> \<Inter>F'"
  1697     apply (frule *)
  1698     by (metis aff subsetCE subset_iff_psubset_eq)
  1699   show ?rhs
  1700     by (metis \<open>finite F\<close> seq aff psubsetI 1 2)
  1701 next
  1702   assume ?rhs then show ?lhs
  1703     by (auto simp: polyhedron_Int_affine_parallel)
  1704 qed
  1705 
  1706 
  1707 lemma polyhedron_Int_affine_minimal:
  1708   fixes S :: "'a :: euclidean_space set"
  1709   shows "polyhedron S \<longleftrightarrow>
  1710          (\<exists>F. finite F \<and> S = (affine hull S) \<inter> \<Inter>F \<and>
  1711               (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}) \<and>
  1712               (\<forall>F'. F' \<subset> F \<longrightarrow> S \<subset> (affine hull S) \<inter> \<Inter>F'))"
  1713 apply (rule iffI)
  1714  apply (force simp: polyhedron_Int_affine_parallel_minimal elim!: ex_forward)
  1715 apply (auto simp: polyhedron_Int_affine elim!: ex_forward)
  1716 done
  1717 
  1718 proposition facet_of_polyhedron_explicit:
  1719   assumes "finite F"
  1720       and seq: "S = affine hull S \<inter> \<Inter>F"
  1721       and faceq: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
  1722       and psub: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> affine hull S \<inter> \<Inter>F'"
  1723     shows "c facet_of S \<longleftrightarrow> (\<exists>h. h \<in> F \<and> c = S \<inter> {x. a h \<bullet> x = b h})"
  1724 proof (cases "S = {}")
  1725   case True with psub show ?thesis by force
  1726 next
  1727   case False
  1728   have "polyhedron S"
  1729     apply (simp add: polyhedron_Int_affine)
  1730     apply (rule_tac x=F in exI)
  1731     using assms  apply force
  1732     done
  1733   then have "convex S"
  1734     by (rule polyhedron_imp_convex)
  1735   with False rel_interior_eq_empty have "rel_interior S \<noteq> {}" by blast
  1736   then obtain x where "x \<in> rel_interior S" by auto
  1737   then obtain T where "open T" "x \<in> T" "x \<in> S" "T \<inter> affine hull S \<subseteq> S"
  1738     by (force simp: mem_rel_interior)
  1739   then have xaff: "x \<in> affine hull S" and xint: "x \<in> \<Inter>F"
  1740     using seq hull_inc by auto
  1741   have "rel_interior S = {x \<in> S. \<forall>h\<in>F. a h \<bullet> x < b h}"
  1742     by (rule rel_interior_polyhedron_explicit [OF \<open>finite F\<close> seq faceq psub])
  1743   with \<open>x \<in> rel_interior S\<close>
  1744   have [simp]: "\<And>h. h\<in>F \<Longrightarrow> a h \<bullet> x < b h" by blast
  1745   have *: "(S \<inter> {x. a h \<bullet> x = b h}) facet_of S" if "h \<in> F" for h
  1746   proof -
  1747     have "S \<subset> affine hull S \<inter> \<Inter>(F - {h})"
  1748       using psub that by (metis Diff_disjoint Diff_subset insert_disjoint(2) psubsetI)
  1749     then obtain z where zaff: "z \<in> affine hull S" and zint: "z \<in> \<Inter>(F - {h})" and "z \<notin> S"
  1750       by force
  1751     then have "z \<noteq> x" "z \<notin> h" using seq \<open>x \<in> S\<close> by auto
  1752     have "x \<in> h" using that xint by auto
  1753     then have able: "a h \<bullet> x \<le> b h"
  1754       using faceq that by blast
  1755     also have "... < a h \<bullet> z" using \<open>z \<notin> h\<close> faceq [OF that] xint by auto
  1756     finally have xltz: "a h \<bullet> x < a h \<bullet> z" .
  1757     define l where "l = (b h - a h \<bullet> x) / (a h \<bullet> z - a h \<bullet> x)"
  1758     define w where "w = (1 - l) *\<^sub>R x + l *\<^sub>R z"
  1759     have "0 < l" "l < 1"
  1760       using able xltz \<open>b h < a h \<bullet> z\<close> \<open>h \<in> F\<close>
  1761       by (auto simp: l_def divide_simps)
  1762     have awlt: "a i \<bullet> w < b i" if "i \<in> F" "i \<noteq> h" for i
  1763     proof -
  1764       have "(1 - l) * (a i \<bullet> x) < (1 - l) * b i"
  1765         by (simp add: \<open>l < 1\<close> \<open>i \<in> F\<close>)
  1766       moreover have "l * (a i \<bullet> z) \<le> l * b i"
  1767         apply (rule mult_left_mono)
  1768         apply (metis Diff_insert_absorb Inter_iff Set.set_insert \<open>h \<in> F\<close> faceq insertE mem_Collect_eq that zint)
  1769         using \<open>0 < l\<close>
  1770         apply simp
  1771         done
  1772       ultimately show ?thesis by (simp add: w_def algebra_simps)
  1773     qed
  1774     have weq: "a h \<bullet> w = b h"
  1775       using xltz unfolding w_def l_def
  1776       by (simp add: algebra_simps) (simp add: field_simps)
  1777     have "w \<in> affine hull S"
  1778       by (simp add: w_def mem_affine xaff zaff)
  1779     moreover have "w \<in> \<Inter>F"
  1780       using \<open>a h \<bullet> w = b h\<close> awlt faceq less_eq_real_def by blast
  1781     ultimately have "w \<in> S"
  1782       using seq by blast
  1783     with weq have "S \<inter> {x. a h \<bullet> x = b h} \<noteq> {}" by blast
  1784     moreover have "S \<inter> {x. a h \<bullet> x = b h} face_of S"
  1785       apply (rule face_of_Int_supporting_hyperplane_le)
  1786       apply (rule \<open>convex S\<close>)
  1787       apply (subst (asm) seq)
  1788       using faceq that apply fastforce
  1789       done
  1790     moreover have "affine hull (S \<inter> {x. a h \<bullet> x = b h}) =
  1791                    (affine hull S) \<inter> {x. a h \<bullet> x = b h}"
  1792     proof
  1793       show "affine hull (S \<inter> {x. a h \<bullet> x = b h}) \<subseteq> affine hull S \<inter> {x. a h \<bullet> x = b h}"
  1794         apply (intro Int_greatest hull_mono Int_lower1)
  1795         apply (metis affine_hull_eq affine_hyperplane hull_mono inf_le2)
  1796         done
  1797     next
  1798       show "affine hull S \<inter> {x. a h \<bullet> x = b h} \<subseteq> affine hull (S \<inter> {x. a h \<bullet> x = b h})"
  1799       proof
  1800         fix y
  1801         assume yaff: "y \<in> affine hull S \<inter> {y. a h \<bullet> y = b h}"
  1802         obtain T where "0 < T"
  1803                  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"
  1804         proof (cases "F - {h} = {}")
  1805           case True then show ?thesis
  1806             by (rule_tac T=1 in that) auto
  1807         next
  1808           case False
  1809           then obtain h' where h': "h' \<in> F - {h}" by auto
  1810           define inff where "inff =
  1811             (INF j:F - {h}.
  1812               if 0 < a j \<bullet> y - a j \<bullet> w
  1813               then (b j - a j \<bullet> w) / (a j \<bullet> y - a j \<bullet> w)
  1814               else 1)"
  1815           have "0 < inff"
  1816             apply (simp add: inff_def)
  1817             apply (rule finite_imp_less_Inf)
  1818               using \<open>finite F\<close> apply blast
  1819              using h' apply blast
  1820             apply simp
  1821             using awlt apply (force simp: divide_simps)
  1822             done
  1823           moreover have "inff * (a j \<bullet> y - a j \<bullet> w) \<le> b j - a j \<bullet> w"
  1824                         if "j \<in> F" "j \<noteq> h" for j
  1825           proof (cases "a j \<bullet> w < a j \<bullet> y")
  1826             case True
  1827             then have "inff \<le> (b j - a j \<bullet> w) / (a j \<bullet> y - a j \<bullet> w)"
  1828               apply (simp add: inff_def)
  1829               apply (rule cInf_le_finite)
  1830               using \<open>finite F\<close> apply blast
  1831               apply (simp add: that split: if_split_asm)
  1832               done
  1833             then show ?thesis
  1834               using \<open>0 < inff\<close> awlt [OF that] mult_strict_left_mono
  1835               by (fastforce simp add: algebra_simps divide_simps split: if_split_asm)
  1836           next
  1837             case False
  1838             with \<open>0 < inff\<close> have "inff * (a j \<bullet> y - a j \<bullet> w) \<le> 0"
  1839               by (simp add: mult_le_0_iff)
  1840             also have "... < b j - a j \<bullet> w"
  1841               by (simp add: awlt that)
  1842             finally show ?thesis by simp
  1843           qed
  1844           ultimately show ?thesis
  1845             by (blast intro: that)
  1846         qed
  1847         define c where "c = (1 - T) *\<^sub>R w + T *\<^sub>R y"
  1848         have "(1 - T) *\<^sub>R w + T *\<^sub>R y \<in> j" if "j \<in> F" for j
  1849         proof (cases "j = h")
  1850           case True
  1851           have "(1 - T) *\<^sub>R w + T *\<^sub>R y \<in> {x. a h \<bullet> x \<le> b h}"
  1852             using weq yaff by (auto simp: algebra_simps)
  1853           with True faceq [OF that] show ?thesis by metis
  1854         next
  1855           case False
  1856           with T that have "(1 - T) *\<^sub>R w + T *\<^sub>R y \<in> {x. a j \<bullet> x \<le> b j}"
  1857             by (simp add: algebra_simps)
  1858           with faceq [OF that] show ?thesis by simp
  1859         qed
  1860         moreover have "(1 - T) *\<^sub>R w + T *\<^sub>R y \<in> affine hull S"
  1861           apply (rule affine_affine_hull [simplified affine_alt, rule_format])
  1862           apply (simp add: \<open>w \<in> affine hull S\<close>)
  1863           using yaff apply blast
  1864           done
  1865         ultimately have "c \<in> S"
  1866           using seq by (force simp: c_def)
  1867         moreover have "a h \<bullet> c = b h"
  1868           using yaff by (force simp: c_def algebra_simps weq)
  1869         ultimately have caff: "c \<in> affine hull (S \<inter> {y. a h \<bullet> y = b h})"
  1870           by (simp add: hull_inc)
  1871         have waff: "w \<in> affine hull (S \<inter> {y. a h \<bullet> y = b h})"
  1872           using \<open>w \<in> S\<close> weq by (blast intro: hull_inc)
  1873         have yeq: "y = (1 - inverse T) *\<^sub>R w + c /\<^sub>R T"
  1874           using \<open>0 < T\<close> by (simp add: c_def algebra_simps)
  1875         show "y \<in> affine hull (S \<inter> {y. a h \<bullet> y = b h})"
  1876           by (metis yeq affine_affine_hull [simplified affine_alt, rule_format, OF waff caff])
  1877       qed
  1878     qed
  1879     ultimately show ?thesis
  1880       apply (simp add: facet_of_def)
  1881       apply (subst aff_dim_affine_hull [symmetric])
  1882       using  \<open>b h < a h \<bullet> z\<close> zaff
  1883       apply (force simp: aff_dim_affine_Int_hyperplane)
  1884       done
  1885   qed
  1886   show ?thesis
  1887   proof
  1888     show "\<exists>h. h \<in> F \<and> c = S \<inter> {x. a h \<bullet> x = b h} \<Longrightarrow> c facet_of S"
  1889       using * by blast
  1890   next
  1891     assume "c facet_of S"
  1892     then have "c face_of S" "convex c" "c \<noteq> {}" and affc: "aff_dim c = aff_dim S - 1"
  1893       by (auto simp: facet_of_def face_of_imp_convex)
  1894     then obtain x where x: "x \<in> rel_interior c"
  1895       by (force simp: rel_interior_eq_empty)
  1896     then have "x \<in> c"
  1897       by (meson subsetD rel_interior_subset)
  1898     then have "x \<in> S"
  1899       using \<open>c facet_of S\<close> facet_of_imp_subset by blast
  1900     have rels: "rel_interior S = {x \<in> S. \<forall>h\<in>F. a h \<bullet> x < b h}"
  1901       by (rule rel_interior_polyhedron_explicit [OF assms])
  1902     have "c \<noteq> S"
  1903       using \<open>c facet_of S\<close> facet_of_irrefl by blast
  1904     then have "x \<notin> rel_interior S"
  1905       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)
  1906     with rels \<open>x \<in> S\<close> obtain i where "i \<in> F" and i: "a i \<bullet> x \<ge> b i"
  1907       by force
  1908     have "x \<in> {u. a i \<bullet> u \<le> b i}"
  1909       by (metis IntD2 InterE \<open>i \<in> F\<close> \<open>x \<in> S\<close> faceq seq)
  1910     then have "a i \<bullet> x \<le> b i" by simp
  1911     then have "a i \<bullet> x = b i" using i by auto
  1912     have "c \<subseteq> S \<inter> {x. a i \<bullet> x = b i}"
  1913       apply (rule subset_of_face_of [of _ S])
  1914         apply (simp add: "*" \<open>i \<in> F\<close> facet_of_imp_face_of)
  1915        apply (simp add: \<open>c face_of S\<close> face_of_imp_subset)
  1916       using \<open>a i \<bullet> x = b i\<close> \<open>x \<in> S\<close> x by blast
  1917     then have cface: "c face_of (S \<inter> {x. a i \<bullet> x = b i})"
  1918       by (meson \<open>c face_of S\<close> face_of_subset inf_le1)
  1919     have con: "convex (S \<inter> {x. a i \<bullet> x = b i})"
  1920       by (simp add: \<open>convex S\<close> convex_Int convex_hyperplane)
  1921     show "\<exists>h. h \<in> F \<and> c = S \<inter> {x. a h \<bullet> x = b h}"
  1922       apply (rule_tac x=i in exI)
  1923       apply (simp add: \<open>i \<in> F\<close>)
  1924       by (metis (no_types) * \<open>i \<in> F\<close> affc facet_of_def less_irrefl face_of_aff_dim_lt [OF con cface])
  1925   qed
  1926 qed
  1927 
  1928 
  1929 lemma face_of_polyhedron_subset_explicit:
  1930   fixes S :: "'a :: euclidean_space set"
  1931   assumes "finite F"
  1932       and seq: "S = affine hull S \<inter> \<Inter>F"
  1933       and faceq: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
  1934       and psub: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> affine hull S \<inter> \<Inter>F'"
  1935       and c: "c face_of S" and "c \<noteq> {}" "c \<noteq> S"
  1936    obtains h where "h \<in> F" "c \<subseteq> S \<inter> {x. a h \<bullet> x = b h}"
  1937 proof -
  1938   have "c \<subseteq> S" using \<open>c face_of S\<close>
  1939     by (simp add: face_of_imp_subset)
  1940   have "polyhedron S"
  1941     apply (simp add: polyhedron_Int_affine)
  1942     by (metis \<open>finite F\<close> faceq seq)
  1943   then have "convex S"
  1944     by (simp add: polyhedron_imp_convex)
  1945   then have *: "(S \<inter> {x. a h \<bullet> x = b h}) face_of S" if "h \<in> F" for h
  1946     apply (rule face_of_Int_supporting_hyperplane_le)
  1947     using faceq seq that by fastforce
  1948   have "rel_interior c \<noteq> {}"
  1949     using c \<open>c \<noteq> {}\<close> face_of_imp_convex rel_interior_eq_empty by blast
  1950   then obtain x where "x \<in> rel_interior c" by auto
  1951   have rels: "rel_interior S = {x \<in> S. \<forall>h\<in>F. a h \<bullet> x < b h}"
  1952     by (rule rel_interior_polyhedron_explicit [OF \<open>finite F\<close> seq faceq psub])
  1953   then have xnot: "x \<notin> rel_interior S"
  1954     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)
  1955   then have "x \<in> S"
  1956     using \<open>c \<subseteq> S\<close> \<open>x \<in> rel_interior c\<close> rel_interior_subset by auto
  1957   then have xint: "x \<in> \<Inter>F"
  1958     using seq by blast
  1959   have "F \<noteq> {}" using assms
  1960     by (metis affine_Int affine_Inter affine_affine_hull ex_in_conv face_of_affine_trivial)
  1961   then obtain i where "i \<in> F" "~ (a i \<bullet> x < b i)"
  1962     using \<open>x \<in> S\<close> rels xnot by auto
  1963   with xint have "a i \<bullet> x = b i"
  1964     by (metis eq_iff mem_Collect_eq not_le Inter_iff faceq)
  1965   have face: "S \<inter> {x. a i \<bullet> x = b i} face_of S"
  1966     by (simp add: "*" \<open>i \<in> F\<close>)
  1967   show ?thesis
  1968     apply (rule_tac h = i in that)
  1969      apply (rule \<open>i \<in> F\<close>)
  1970     apply (rule subset_of_face_of [OF face \<open>c \<subseteq> S\<close>])
  1971     using \<open>a i \<bullet> x = b i\<close> \<open>x \<in> rel_interior c\<close> \<open>x \<in> S\<close> apply blast
  1972     done
  1973 qed
  1974 
  1975 text\<open>Initial part of proof duplicates that above\<close>
  1976 proposition face_of_polyhedron_explicit:
  1977   fixes S :: "'a :: euclidean_space set"
  1978   assumes "finite F"
  1979       and seq: "S = affine hull S \<inter> \<Inter>F"
  1980       and faceq: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
  1981       and psub: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> affine hull S \<inter> \<Inter>F'"
  1982       and c: "c face_of S" and "c \<noteq> {}" "c \<noteq> S"
  1983     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}}"
  1984 proof -
  1985   let ?ab = "\<lambda>h. {x. a h \<bullet> x = b h}"
  1986   have "c \<subseteq> S" using \<open>c face_of S\<close>
  1987     by (simp add: face_of_imp_subset)
  1988   have "polyhedron S"
  1989     apply (simp add: polyhedron_Int_affine)
  1990     by (metis \<open>finite F\<close> faceq seq)
  1991   then have "convex S"
  1992     by (simp add: polyhedron_imp_convex)
  1993   then have *: "(S \<inter> ?ab h) face_of S" if "h \<in> F" for h
  1994     apply (rule face_of_Int_supporting_hyperplane_le)
  1995     using faceq seq that by fastforce
  1996   have "rel_interior c \<noteq> {}"
  1997     using c \<open>c \<noteq> {}\<close> face_of_imp_convex rel_interior_eq_empty by blast
  1998   then obtain z where z: "z \<in> rel_interior c" by auto
  1999   have rels: "rel_interior S = {z \<in> S. \<forall>h\<in>F. a h \<bullet> z < b h}"
  2000     by (rule rel_interior_polyhedron_explicit [OF \<open>finite F\<close> seq faceq psub])
  2001   then have xnot: "z \<notin> rel_interior S"
  2002     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)
  2003   then have "z \<in> S"
  2004     using \<open>c \<subseteq> S\<close> \<open>z \<in> rel_interior c\<close> rel_interior_subset by auto
  2005   with seq have xint: "z \<in> \<Inter>F" by blast
  2006   have "open (\<Inter>h\<in>{h \<in> F. a h \<bullet> z < b h}. {w. a h \<bullet> w < b h})"
  2007     by (auto simp: \<open>finite F\<close> open_halfspace_lt open_INT)
  2008   then obtain e where "0 < e"
  2009                  "ball z e \<subseteq> (\<Inter>h\<in>{h \<in> F. a h \<bullet> z < b h}. {w. a h \<bullet> w < b h})"
  2010     by (auto intro: openE [of _ z])
  2011   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}"
  2012     by blast
  2013   have "c \<subseteq> (S \<inter> ?ab h) \<longleftrightarrow> z \<in> S \<inter> ?ab h" if "h \<in> F" for h
  2014   proof
  2015     show "z \<in> S \<inter> ?ab h \<Longrightarrow> c \<subseteq> S \<inter> ?ab h"
  2016       apply (rule subset_of_face_of [of _ S])
  2017       using that \<open>c \<subseteq> S\<close> \<open>z \<in> rel_interior c\<close>
  2018       using facet_of_polyhedron_explicit [OF \<open>finite F\<close> seq faceq psub]
  2019             unfolding facet_of_def
  2020       apply auto
  2021       done
  2022   next
  2023     show "c \<subseteq> S \<inter> ?ab h \<Longrightarrow> z \<in> S \<inter> ?ab h"
  2024       using \<open>z \<in> rel_interior c\<close> rel_interior_subset by force
  2025   qed
  2026   then have **: "{S \<inter> ?ab h | h. h \<in> F \<and> c \<subseteq> S \<and> c \<subseteq> ?ab h} =
  2027                  {S \<inter> ?ab h |h. h \<in> F \<and> z \<in> S \<inter> ?ab h}"
  2028     by blast
  2029   have bsub: "ball z e \<inter> affine hull \<Inter>{S \<inter> ?ab h |h. h \<in> F \<and> a h \<bullet> z = b h}
  2030              \<subseteq> affine hull S \<inter> \<Inter>F \<inter> \<Inter>{?ab h |h. h \<in> F \<and> a h \<bullet> z = b h}"
  2031             if "i \<in> F" and i: "a i \<bullet> z = b i" for i
  2032   proof -
  2033     have sub: "ball z e \<inter> \<Inter>{?ab h |h. h \<in> F \<and> a h \<bullet> z = b h} \<subseteq> j"
  2034              if "j \<in> F" for j
  2035     proof -
  2036       have "a j \<bullet> z \<le> b j" using faceq that xint by auto
  2037       then consider "a j \<bullet> z < b j" | "a j \<bullet> z = b j" by linarith
  2038       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"
  2039       proof cases
  2040         assume "a j \<bullet> z < b j"
  2041         then have "ball z e \<inter> {x. a i \<bullet> x = b i} \<subseteq> j"
  2042           using e [OF \<open>j \<in> F\<close>] faceq that
  2043           by (fastforce simp: ball_def)
  2044         then show ?thesis
  2045           by (rule_tac x="{x. a i \<bullet> x = b i}" in exI) (force simp: \<open>i \<in> F\<close> i)
  2046       next
  2047         assume eq: "a j \<bullet> z = b j"
  2048         with faceq that show ?thesis
  2049           by (rule_tac x="{x. a j \<bullet> x = b j}" in exI) (fastforce simp add: \<open>j \<in> F\<close>)
  2050       qed
  2051       then show ?thesis  by blast
  2052     qed
  2053     have 1: "affine hull \<Inter>{S \<inter> ?ab h |h. h \<in> F \<and> a h \<bullet> z = b h} \<subseteq> affine hull S"
  2054       apply (rule hull_mono)
  2055       using that \<open>z \<in> S\<close> by auto
  2056     have 2: "affine hull \<Inter>{S \<inter> ?ab h |h. h \<in> F \<and> a h \<bullet> z = b h}
  2057           \<subseteq> \<Inter>{?ab h |h. h \<in> F \<and> a h \<bullet> z = b h}"
  2058       by (rule hull_minimal) (auto intro: affine_hyperplane)
  2059     have 3: "ball z e \<inter> \<Inter>{?ab h |h. h \<in> F \<and> a h \<bullet> z = b h} \<subseteq> \<Inter>F"
  2060       by (iprover intro: sub Inter_greatest)
  2061     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"
  2062              for A B C D E  by blast
  2063     show ?thesis by (intro * 1 2 3)
  2064   qed
  2065   have "\<exists>h. h \<in> F \<and> c \<subseteq> ?ab h"
  2066     apply (rule face_of_polyhedron_subset_explicit [OF \<open>finite F\<close> seq faceq psub])
  2067     using assms by auto
  2068   then have fac: "\<Inter>{S \<inter> ?ab h |h. h \<in> F \<and> c \<subseteq> S \<inter> ?ab h} face_of S"
  2069     using * by (force simp: \<open>c \<subseteq> S\<close> intro: face_of_Inter)
  2070   have red:
  2071      "(\<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}"
  2072      for P T F   by blast
  2073   have "ball z e \<inter> affine hull \<Inter>{S \<inter> ?ab h |h. h \<in> F \<and> a h \<bullet> z = b h}
  2074         \<subseteq> \<Inter>{S \<inter> ?ab h |h. h \<in> F \<and> a h \<bullet> z = b h}"
  2075     apply (rule red)
  2076     apply (metis seq bsub)
  2077     done
  2078   with \<open>0 < e\<close> have zinrel: "z \<in> rel_interior
  2079                     (\<Inter>{S \<inter> ?ab h |h. h \<in> F \<and> z \<in> S \<and> a h \<bullet> z = b h})"
  2080     by (auto simp: mem_rel_interior_ball \<open>z \<in> S\<close>)
  2081   show ?thesis
  2082     apply (rule face_of_eq [OF c fac])
  2083     using z zinrel apply (force simp: **)
  2084     done
  2085 qed
  2086 
  2087 
  2088 subsection\<open>More general corollaries from the explicit representation\<close>
  2089 
  2090 corollary facet_of_polyhedron:
  2091   assumes "polyhedron S" and "c facet_of S"
  2092   obtains a b where "a \<noteq> 0" "S \<subseteq> {x. a \<bullet> x \<le> b}" "c = S \<inter> {x. a \<bullet> x = b}"
  2093 proof -
  2094   obtain F where "finite F" and seq: "S = affine hull S \<inter> \<Inter>F"
  2095              and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
  2096              and min: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> (affine hull S) \<inter> \<Inter>F'"
  2097     using assms by (simp add: polyhedron_Int_affine_minimal) meson
  2098   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}"
  2099     by metis
  2100   obtain i where "i \<in> F" and c: "c = S \<inter> {x. a i \<bullet> x = b i}"
  2101     using facet_of_polyhedron_explicit [OF \<open>finite F\<close> seq ab min] assms
  2102     by force
  2103   moreover have ssub: "S \<subseteq> {x. a i \<bullet> x \<le> b i}"
  2104      apply (subst seq)
  2105      using \<open>i \<in> F\<close> ab by auto
  2106   ultimately show ?thesis
  2107     by (rule_tac a = "a i" and b = "b i" in that) (simp_all add: ab)
  2108 qed
  2109 
  2110 corollary face_of_polyhedron:
  2111   assumes "polyhedron S" and "c face_of S" and "c \<noteq> {}" and "c \<noteq> S"
  2112     shows "c = \<Inter>{F. F facet_of S \<and> c \<subseteq> F}"
  2113 proof -
  2114   obtain F where "finite F" and seq: "S = affine hull S \<inter> \<Inter>F"
  2115              and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
  2116              and min: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> (affine hull S) \<inter> \<Inter>F'"
  2117     using assms by (simp add: polyhedron_Int_affine_minimal) meson
  2118   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}"
  2119     by metis
  2120   show ?thesis
  2121     apply (subst face_of_polyhedron_explicit [OF \<open>finite F\<close> seq ab min])
  2122     apply (auto simp: assms facet_of_polyhedron_explicit [OF \<open>finite F\<close> seq ab min] cong: Collect_cong)
  2123     done
  2124 qed
  2125 
  2126 lemma face_of_polyhedron_subset_facet:
  2127   assumes "polyhedron S" and "c face_of S" and "c \<noteq> {}" and "c \<noteq> S"
  2128   obtains F where "F facet_of S" "c \<subseteq> F"
  2129 using face_of_polyhedron assms
  2130 by (metis (no_types, lifting) Inf_greatest antisym_conv face_of_imp_subset mem_Collect_eq)
  2131 
  2132 
  2133 lemma exposed_face_of_polyhedron:
  2134   assumes "polyhedron S"
  2135     shows "F exposed_face_of S \<longleftrightarrow> F face_of S"
  2136 proof
  2137   show "F exposed_face_of S \<Longrightarrow> F face_of S"
  2138     by (simp add: exposed_face_of_def)
  2139 next
  2140   assume "F face_of S"
  2141   show "F exposed_face_of S"
  2142   proof (cases "F = {} \<or> F = S")
  2143     case True then show ?thesis
  2144       using \<open>F face_of S\<close> exposed_face_of by blast
  2145   next
  2146     case False
  2147     then have "{g. g facet_of S \<and> F \<subseteq> g} \<noteq> {}"
  2148       by (metis Collect_empty_eq_bot \<open>F face_of S\<close> assms empty_def face_of_polyhedron_subset_facet)
  2149     moreover have "\<And>T. \<lbrakk>T facet_of S; F \<subseteq> T\<rbrakk> \<Longrightarrow> T exposed_face_of S"
  2150       by (metis assms exposed_face_of facet_of_imp_face_of facet_of_polyhedron)
  2151     ultimately have "\<Inter>{fa.
  2152        fa facet_of S \<and> F \<subseteq> fa} exposed_face_of S"
  2153       by (metis (no_types, lifting) mem_Collect_eq exposed_face_of_Inter)
  2154     then show ?thesis
  2155       using False
  2156       apply (subst face_of_polyhedron [OF assms \<open>F face_of S\<close>], auto)
  2157       done
  2158   qed
  2159 qed
  2160 
  2161 lemma face_of_polyhedron_polyhedron:
  2162   fixes S :: "'a :: euclidean_space set"
  2163   assumes "polyhedron S" "c face_of S"
  2164     shows "polyhedron c"
  2165 by (metis assms face_of_imp_eq_affine_Int polyhedron_Int polyhedron_affine_hull polyhedron_imp_closed polyhedron_imp_convex)
  2166 
  2167 lemma finite_polyhedron_faces:
  2168   fixes S :: "'a :: euclidean_space set"
  2169   assumes "polyhedron S"
  2170     shows "finite {F. F face_of S}"
  2171 proof -
  2172   obtain F where "finite F" and seq: "S = affine hull S \<inter> \<Inter>F"
  2173              and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
  2174              and min:   "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> (affine hull S) \<inter> \<Inter>F'"
  2175     using assms by (simp add: polyhedron_Int_affine_minimal) meson
  2176   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}"
  2177     by metis
  2178   have "finite {\<Inter>{S \<inter> {x. a h \<bullet> x = b h} |h. h \<in> F'}| F'. F' \<in> Pow F}"
  2179     by (simp add: \<open>finite F\<close>)
  2180   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}"
  2181     apply clarify
  2182     apply (rename_tac c)
  2183     apply (drule face_of_polyhedron_explicit [OF \<open>finite F\<close> seq ab min, simplified], simp_all)
  2184     apply (erule ssubst)
  2185     apply (rule_tac x="{h \<in> F. c \<subseteq> S \<inter> {x. a h \<bullet> x = b h}}" in exI, auto)
  2186     done
  2187   ultimately show ?thesis
  2188     by (meson finite.emptyI finite.insertI finite_Diff2 finite_subset)
  2189 qed
  2190 
  2191 lemma finite_polyhedron_exposed_faces:
  2192    "polyhedron S \<Longrightarrow> finite {F. F exposed_face_of S}"
  2193 using exposed_face_of_polyhedron finite_polyhedron_faces by fastforce
  2194 
  2195 lemma finite_polyhedron_extreme_points:
  2196   fixes S :: "'a :: euclidean_space set"
  2197   shows "polyhedron S \<Longrightarrow> finite {v. v extreme_point_of S}"
  2198 apply (simp add: face_of_singleton [symmetric])
  2199 apply (rule finite_subset [OF _ finite_vimageI [OF finite_polyhedron_faces]], auto)
  2200 done
  2201 
  2202 lemma finite_polyhedron_facets:
  2203   fixes S :: "'a :: euclidean_space set"
  2204   shows "polyhedron S \<Longrightarrow> finite {F. F facet_of S}"
  2205 unfolding facet_of_def
  2206 by (blast intro: finite_subset [OF _ finite_polyhedron_faces])
  2207 
  2208 
  2209 proposition rel_interior_of_polyhedron:
  2210   fixes S :: "'a :: euclidean_space set"
  2211   assumes "polyhedron S"
  2212     shows "rel_interior S = S - \<Union>{F. F facet_of S}"
  2213 proof -
  2214   obtain F where "finite F" and seq: "S = affine hull S \<inter> \<Inter>F"
  2215              and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
  2216              and min: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> (affine hull S) \<inter> \<Inter>F'"
  2217     using assms by (simp add: polyhedron_Int_affine_minimal) meson
  2218   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}"
  2219     by metis
  2220   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
  2221     by (rule facet_of_polyhedron_explicit [OF \<open>finite F\<close> seq ab min])
  2222   have rel: "rel_interior S = {x \<in> S. \<forall>h\<in>F. a h \<bullet> x < b h}"
  2223     by (rule rel_interior_polyhedron_explicit [OF \<open>finite F\<close> seq ab min])
  2224   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
  2225   proof -
  2226     have "x \<in> \<Inter>F" using seq that by force
  2227     with \<open>h \<in> F\<close> ab have "a h \<bullet> x \<le> b h" by auto
  2228     then consider "a h \<bullet> x < b h" | "a h \<bullet> x = b h" by linarith
  2229     then show ?thesis
  2230     proof cases
  2231       case 1 then show ?thesis .
  2232     next
  2233       case 2
  2234       have "Collect (op \<in> x) \<notin> Collect (op \<in> (\<Union>{A. A facet_of S}))"
  2235         using xnot by fastforce
  2236       then have "F \<notin> Collect (op \<in> h)"
  2237         using 2 \<open>x \<in> S\<close> facet by blast
  2238       with \<open>h \<in> F\<close> have "\<Inter>F \<subseteq> S \<inter> {x. a h \<bullet> x = b h}" by blast
  2239       with 2 that \<open>x \<in> \<Inter>F\<close> show ?thesis
  2240         apply simp
  2241         apply (drule_tac x="\<Inter>F" in spec)
  2242         apply (simp add: facet)
  2243         apply (drule_tac x=h in spec)
  2244         using seq by auto
  2245       qed
  2246   qed
  2247   moreover have "\<exists>h\<in>F. a h \<bullet> x \<ge> b h" if "x \<in> \<Union>{F. F facet_of S}" for x
  2248     using that by (force simp: facet)
  2249   ultimately show ?thesis
  2250     by (force simp: rel)
  2251 qed
  2252 
  2253 lemma rel_boundary_of_polyhedron:
  2254   fixes S :: "'a :: euclidean_space set"
  2255   assumes "polyhedron S"
  2256     shows "S - rel_interior S = \<Union> {F. F facet_of S}"
  2257 using facet_of_imp_subset by (fastforce simp add: rel_interior_of_polyhedron assms)
  2258 
  2259 lemma rel_frontier_of_polyhedron:
  2260   fixes S :: "'a :: euclidean_space set"
  2261   assumes "polyhedron S"
  2262     shows "rel_frontier S = \<Union> {F. F facet_of S}"
  2263 by (simp add: assms rel_frontier_def polyhedron_imp_closed rel_boundary_of_polyhedron)
  2264 
  2265 lemma rel_frontier_of_polyhedron_alt:
  2266   fixes S :: "'a :: euclidean_space set"
  2267   assumes "polyhedron S"
  2268     shows "rel_frontier S = \<Union> {F. F face_of S \<and> (F \<noteq> S)}"
  2269 apply (rule subset_antisym)
  2270   apply (force simp: rel_frontier_of_polyhedron facet_of_def assms)
  2271 using face_of_subset_rel_frontier by fastforce
  2272 
  2273 
  2274 text\<open>A characterization of polyhedra as having finitely many faces\<close>
  2275 
  2276 proposition polyhedron_eq_finite_exposed_faces:
  2277   fixes S :: "'a :: euclidean_space set"
  2278   shows "polyhedron S \<longleftrightarrow> closed S \<and> convex S \<and> finite {F. F exposed_face_of S}"
  2279          (is "?lhs = ?rhs")
  2280 proof
  2281   assume ?lhs
  2282   then show ?rhs
  2283     by (auto simp: polyhedron_imp_closed polyhedron_imp_convex finite_polyhedron_exposed_faces)
  2284 next
  2285   assume ?rhs
  2286   then have "closed S" "convex S" and fin: "finite {F. F exposed_face_of S}" by auto
  2287   show ?lhs
  2288   proof (cases "S = {}")
  2289     case True then show ?thesis by auto
  2290   next
  2291     case False
  2292     define F where "F = {h. h exposed_face_of S \<and> h \<noteq> {} \<and> h \<noteq> S}"
  2293     have "finite F" by (simp add: fin F_def)
  2294     have hface: "h face_of S"
  2295       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}"
  2296       if "h \<in> F" for h
  2297       using exposed_face_of F_def that by simp_all auto
  2298     then obtain a b where ab:
  2299       "\<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}"
  2300       by metis
  2301     have *: "False"
  2302       if paff: "p \<in> affine hull S" and "p \<notin> S"
  2303       and pint: "p \<in> \<Inter>{{x. a h \<bullet> x \<le> b h} |h. h \<in> F}" for p
  2304     proof -
  2305       have "rel_interior S \<noteq> {}"
  2306         by (simp add: \<open>S \<noteq> {}\<close> \<open>convex S\<close> rel_interior_eq_empty)
  2307       then obtain c where c: "c \<in> rel_interior S" by auto
  2308       with rel_interior_subset have "c \<in> S"  by blast
  2309       have ccp: "closed_segment c p \<subseteq> affine hull S"
  2310         by (meson affine_affine_hull affine_imp_convex c closed_segment_subset hull_subset paff rel_interior_subset subsetCE)
  2311       obtain x where xcl: "x \<in> closed_segment c p" and "x \<in> S" and xnot: "x \<notin> rel_interior S"
  2312         using connected_openin [of "closed_segment c p"]
  2313         apply simp
  2314         apply (drule_tac x="closed_segment c p \<inter> rel_interior S" in spec)
  2315         apply (erule impE)
  2316          apply (force simp: openin_rel_interior openin_Int intro: openin_subtopology_Int_subset [OF _ ccp])
  2317         apply (drule_tac x="closed_segment c p \<inter> (- S)" in spec)
  2318         using rel_interior_subset \<open>closed S\<close> c \<open>p \<notin> S\<close> apply blast
  2319         done
  2320       then obtain \<mu> where "0 \<le> \<mu>" "\<mu> \<le> 1" and xeq: "x = (1 - \<mu>) *\<^sub>R c + \<mu> *\<^sub>R p"
  2321         by (auto simp: in_segment)
  2322       show False
  2323       proof (cases "\<mu>=0 \<or> \<mu>=1")
  2324         case True with xeq c xnot \<open>x \<in> S\<close> \<open>p \<notin> S\<close>
  2325         show False by auto
  2326       next
  2327         case False
  2328         then have xos: "x \<in> open_segment c p"
  2329           using \<open>x \<in> S\<close> c open_segment_def that(2) xcl xnot by auto
  2330         have xclo: "x \<in> closure S"
  2331           using \<open>x \<in> S\<close> closure_subset by blast
  2332         obtain d where "d \<noteq> 0"
  2333               and dle: "\<And>y. y \<in> closure S \<Longrightarrow> d \<bullet> x \<le> d \<bullet> y"
  2334               and dless: "\<And>y. y \<in> rel_interior S \<Longrightarrow> d \<bullet> x < d \<bullet> y"
  2335           by (metis supporting_hyperplane_relative_frontier [OF \<open>convex S\<close> xclo xnot])
  2336         have sex: "S \<inter> {y. d \<bullet> y = d \<bullet> x} exposed_face_of S"
  2337           by (simp add: \<open>closed S\<close> dle exposed_face_of_Int_supporting_hyperplane_ge [OF \<open>convex S\<close>])
  2338         have sne: "S \<inter> {y. d \<bullet> y = d \<bullet> x} \<noteq> {}"
  2339           using \<open>x \<in> S\<close> by blast
  2340         have sns: "S \<inter> {y. d \<bullet> y = d \<bullet> x} \<noteq> S"
  2341           by (metis (mono_tags) Int_Collect c subsetD dless not_le order_refl rel_interior_subset)
  2342         obtain h where "h \<in> F" "x \<in> h"
  2343           apply (rule_tac h="S \<inter> {y. d \<bullet> y = d \<bullet> x}" in that)
  2344           apply (simp_all add: F_def sex sne sns \<open>x \<in> S\<close>)
  2345           done
  2346         have abface: "{y. a h \<bullet> y = b h} face_of {y. a h \<bullet> y \<le> b h}"
  2347           using hyperplane_face_of_halfspace_le by blast
  2348         then have "c \<in> h"
  2349           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
  2350         with c have "h \<inter> rel_interior S \<noteq> {}" by blast
  2351         then show False
  2352           using \<open>h \<in> F\<close> F_def face_of_disjoint_rel_interior hface by auto
  2353       qed
  2354     qed
  2355     have "S \<subseteq> affine hull S \<inter> \<Inter>{{x. a h \<bullet> x \<le> b h} |h. h \<in> F}"
  2356       using ab by (auto simp: hull_subset)
  2357     moreover have "affine hull S \<inter> \<Inter>{{x. a h \<bullet> x \<le> b h} |h. h \<in> F} \<subseteq> S"
  2358       using * by blast
  2359     ultimately have "S = affine hull S \<inter> \<Inter> {{x. a h \<bullet> x \<le> b h} |h. h \<in> F}" ..
  2360     then show ?thesis
  2361       apply (rule ssubst)
  2362       apply (force intro: polyhedron_affine_hull polyhedron_halfspace_le simp: \<open>finite F\<close>)
  2363       done
  2364   qed
  2365 qed
  2366 
  2367 corollary polyhedron_eq_finite_faces:
  2368   fixes S :: "'a :: euclidean_space set"
  2369   shows "polyhedron S \<longleftrightarrow> closed S \<and> convex S \<and> finite {F. F face_of S}"
  2370          (is "?lhs = ?rhs")
  2371 proof
  2372   assume ?lhs
  2373   then show ?rhs
  2374     by (simp add: finite_polyhedron_faces polyhedron_imp_closed polyhedron_imp_convex)
  2375 next
  2376   assume ?rhs
  2377   then show ?lhs
  2378     by (force simp: polyhedron_eq_finite_exposed_faces exposed_face_of intro: finite_subset)
  2379 qed
  2380 
  2381 lemma polyhedron_linear_image_eq:
  2382   fixes h :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
  2383   assumes "linear h" "bij h"
  2384     shows "polyhedron (h ` S) \<longleftrightarrow> polyhedron S"
  2385 proof -
  2386   have *: "{f. P f} = (image h) ` {f. P (h ` f)}" for P
  2387     apply safe
  2388     apply (rule_tac x="inv h ` x" in image_eqI)
  2389     apply (auto simp: \<open>bij h\<close> bij_is_surj image_f_inv_f)
  2390     done
  2391   have "inj h" using bij_is_inj assms by blast
  2392   then have injim: "inj_on (op ` h) A" for A
  2393     by (simp add: inj_on_def inj_image_eq_iff)
  2394   show ?thesis
  2395     using \<open>linear h\<close> \<open>inj h\<close>
  2396     apply (simp add: polyhedron_eq_finite_faces closed_injective_linear_image_eq)
  2397     apply (simp add: * face_of_linear_image [of h _ S, symmetric] finite_image_iff injim)
  2398     done
  2399 qed
  2400 
  2401 lemma polyhedron_negations:
  2402   fixes S :: "'a :: euclidean_space set"
  2403   shows   "polyhedron S \<Longrightarrow> polyhedron(image uminus S)"
  2404 by (auto simp: polyhedron_linear_image_eq linear_uminus bij_uminus)
  2405 
  2406 subsection\<open>Relation between polytopes and polyhedra\<close>
  2407 
  2408 lemma polytope_eq_bounded_polyhedron:
  2409   fixes S :: "'a :: euclidean_space set"
  2410   shows "polytope S \<longleftrightarrow> polyhedron S \<and> bounded S"
  2411          (is "?lhs = ?rhs")
  2412 proof
  2413   assume ?lhs
  2414   then show ?rhs
  2415     by (simp add: finite_polytope_faces polyhedron_eq_finite_faces
  2416                   polytope_imp_closed polytope_imp_convex polytope_imp_bounded)
  2417 next
  2418   assume ?rhs then show ?lhs
  2419     unfolding polytope_def
  2420     apply (rule_tac x="{v. v extreme_point_of S}" in exI)
  2421     apply (simp add: finite_polyhedron_extreme_points Krein_Milman_Minkowski compact_eq_bounded_closed polyhedron_imp_closed polyhedron_imp_convex)
  2422     done
  2423 qed
  2424 
  2425 lemma polytope_Int:
  2426   fixes S :: "'a :: euclidean_space set"
  2427   shows "\<lbrakk>polytope S; polytope T\<rbrakk> \<Longrightarrow> polytope(S \<inter> T)"
  2428 by (simp add: polytope_eq_bounded_polyhedron bounded_Int)
  2429 
  2430 
  2431 lemma polytope_Int_polyhedron:
  2432   fixes S :: "'a :: euclidean_space set"
  2433   shows "\<lbrakk>polytope S; polyhedron T\<rbrakk> \<Longrightarrow> polytope(S \<inter> T)"
  2434 by (simp add: bounded_Int polytope_eq_bounded_polyhedron)
  2435 
  2436 lemma polyhedron_Int_polytope:
  2437   fixes S :: "'a :: euclidean_space set"
  2438   shows "\<lbrakk>polyhedron S; polytope T\<rbrakk> \<Longrightarrow> polytope(S \<inter> T)"
  2439 by (simp add: bounded_Int polytope_eq_bounded_polyhedron)
  2440 
  2441 lemma polytope_imp_polyhedron:
  2442   fixes S :: "'a :: euclidean_space set"
  2443   shows "polytope S \<Longrightarrow> polyhedron S"
  2444 by (simp add: polytope_eq_bounded_polyhedron)
  2445 
  2446 lemma polytope_facet_exists:
  2447   fixes p :: "'a :: euclidean_space set"
  2448   assumes "polytope p" "0 < aff_dim p"
  2449   obtains F where "F facet_of p"
  2450 proof (cases "p = {}")
  2451   case True with assms show ?thesis by auto
  2452 next
  2453   case False
  2454   then obtain v where "v extreme_point_of p"
  2455     using extreme_point_exists_convex
  2456     by (blast intro: \<open>polytope p\<close> polytope_imp_compact polytope_imp_convex)
  2457   then
  2458   show ?thesis
  2459     by (metis face_of_polyhedron_subset_facet polytope_imp_polyhedron aff_dim_sing
  2460        all_not_in_conv assms face_of_singleton less_irrefl singletonI that)
  2461 qed
  2462 
  2463 lemma polyhedron_interval [iff]: "polyhedron(cbox a b)"
  2464 by (metis polytope_imp_polyhedron polytope_interval)
  2465 
  2466 lemma polyhedron_convex_hull:
  2467   fixes S :: "'a :: euclidean_space set"
  2468   shows "finite S \<Longrightarrow> polyhedron(convex hull S)"
  2469 by (simp add: polytope_convex_hull polytope_imp_polyhedron)
  2470 
  2471 
  2472 subsection\<open>Relative and absolute frontier of a polytope\<close>
  2473 
  2474 lemma rel_boundary_of_convex_hull:
  2475     fixes S :: "'a::euclidean_space set"
  2476     assumes "~ affine_dependent S"
  2477       shows "(convex hull S) - rel_interior(convex hull S) = (\<Union>a\<in>S. convex hull (S - {a}))"
  2478 proof -
  2479   have "finite S" by (metis assms aff_independent_finite)
  2480   then consider "card S = 0" | "card S = 1" | "2 \<le> card S" by arith
  2481   then show ?thesis
  2482   proof cases
  2483     case 1 then have "S = {}" by (simp add: \<open>finite S\<close>)
  2484     then show ?thesis by simp
  2485   next
  2486     case 2 show ?thesis
  2487       by (auto intro: card_1_singletonE [OF \<open>card S = 1\<close>])
  2488   next
  2489     case 3
  2490     with assms show ?thesis
  2491       by (auto simp: polyhedron_convex_hull rel_boundary_of_polyhedron facet_of_convex_hull_affine_independent_alt \<open>finite S\<close>)
  2492   qed
  2493 qed
  2494 
  2495 proposition frontier_of_convex_hull:
  2496     fixes S :: "'a::euclidean_space set"
  2497     assumes "card S = Suc (DIM('a))"
  2498       shows "frontier(convex hull S) = \<Union> {convex hull (S - {a}) | a. a \<in> S}"
  2499 proof (cases "affine_dependent S")
  2500   case True
  2501     have [iff]: "finite S"
  2502       using assms using card_infinite by force
  2503     then have ccs: "closed (convex hull S)"
  2504       by (simp add: compact_imp_closed finite_imp_compact_convex_hull)
  2505     { fix x T
  2506       assume "finite T" "T \<subseteq> S" "int (card T) \<le> aff_dim S + 1" "x \<in> convex hull T"
  2507       then have "S \<noteq> T"
  2508         using True \<open>finite S\<close> aff_dim_le_card affine_independent_iff_card by fastforce
  2509       then obtain a where "a \<in> S" "a \<notin> T"
  2510         using \<open>T \<subseteq> S\<close> by blast
  2511       then have "x \<in> (\<Union>a\<in>S. convex hull (S - {a}))"
  2512         using True affine_independent_iff_card [of S]
  2513         apply simp
  2514         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)
  2515         done
  2516     } note * = this
  2517     have 1: "convex hull S \<subseteq> (\<Union> a\<in>S. convex hull (S - {a}))"
  2518       apply (subst caratheodory_aff_dim)
  2519       apply (blast intro: *)
  2520       done
  2521     have 2: "\<Union>((\<lambda>a. convex hull (S - {a})) ` S) \<subseteq> convex hull S"
  2522       by (rule Union_least) (metis (no_types, lifting)  Diff_subset hull_mono imageE)
  2523     show ?thesis using True
  2524       apply (simp add: segment_convex_hull frontier_def)
  2525       using interior_convex_hull_eq_empty [OF assms]
  2526       apply (simp add: closure_closed [OF ccs])
  2527       apply (rule subset_antisym)
  2528       using 1 apply blast
  2529       using 2 apply blast
  2530       done
  2531 next
  2532   case False
  2533   then have "frontier (convex hull S) = (convex hull S) - rel_interior(convex hull S)"
  2534     apply (simp add: rel_boundary_of_convex_hull [symmetric] frontier_def)
  2535     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)
  2536   also have "... = \<Union>{convex hull (S - {a}) |a. a \<in> S}"
  2537   proof -
  2538     have "convex hull S - rel_interior (convex hull S) = rel_frontier (convex hull S)"
  2539       by (simp add: False aff_independent_finite polyhedron_convex_hull rel_boundary_of_polyhedron rel_frontier_of_polyhedron)
  2540     then show ?thesis
  2541       by (simp add: False rel_frontier_convex_hull_cases)
  2542   qed
  2543   finally show ?thesis .
  2544 qed
  2545 
  2546 subsection\<open>Special case of a triangle\<close>
  2547 
  2548 proposition frontier_of_triangle:
  2549     fixes a :: "'a::euclidean_space"
  2550     assumes "DIM('a) = 2"
  2551     shows "frontier(convex hull {a,b,c}) = closed_segment a b \<union> closed_segment b c \<union> closed_segment c a"
  2552           (is "?lhs = ?rhs")
  2553 proof (cases "b = a \<or> c = a \<or> c = b")
  2554   case True then show ?thesis
  2555     by (auto simp: assms segment_convex_hull frontier_def empty_interior_convex_hull insert_commute card_insert_le_m1 hull_inc insert_absorb)
  2556 next
  2557   case False then have [simp]: "card {a, b, c} = Suc (DIM('a))"
  2558     by (simp add: card_insert Set.insert_Diff_if assms)
  2559   show ?thesis
  2560   proof
  2561     show "?lhs \<subseteq> ?rhs"
  2562       using False
  2563       by (force simp: segment_convex_hull frontier_of_convex_hull insert_Diff_if insert_commute split: if_split_asm)
  2564     show "?rhs \<subseteq> ?lhs"
  2565       using False
  2566       apply (simp add: frontier_of_convex_hull segment_convex_hull)
  2567       apply (intro conjI subsetI)
  2568         apply (rule_tac X="convex hull {a,b}" in UnionI; force simp: Set.insert_Diff_if)
  2569        apply (rule_tac X="convex hull {b,c}" in UnionI; force)
  2570       apply (rule_tac X="convex hull {a,c}" in UnionI; force simp: insert_commute Set.insert_Diff_if)
  2571       done
  2572   qed
  2573 qed
  2574 
  2575 corollary inside_of_triangle:
  2576     fixes a :: "'a::euclidean_space"
  2577     assumes "DIM('a) = 2"
  2578     shows "inside (closed_segment a b \<union> closed_segment b c \<union> closed_segment c a) = interior(convex hull {a,b,c})"
  2579 by (metis assms frontier_of_triangle bounded_empty bounded_insert convex_convex_hull inside_frontier_eq_interior bounded_convex_hull)
  2580 
  2581 corollary interior_of_triangle:
  2582     fixes a :: "'a::euclidean_space"
  2583     assumes "DIM('a) = 2"
  2584     shows "interior(convex hull {a,b,c}) =
  2585            convex hull {a,b,c} - (closed_segment a b \<union> closed_segment b c \<union> closed_segment c a)"
  2586   using interior_subset
  2587   by (force simp: frontier_of_triangle [OF assms, symmetric] frontier_def Diff_Diff_Int)
  2588 
  2589 subsection\<open>Subdividing a cell complex\<close>
  2590 
  2591 lemma subdivide_interval:
  2592   fixes x::real
  2593   assumes "a < \<bar>x - y\<bar>" "0 < a"
  2594   obtains n where "n \<in> \<int>" "x < n * a \<and> n * a < y \<or> y <  n * a \<and> n * a < x"
  2595 proof -
  2596   consider "a + x < y" | "a + y < x"
  2597     using assms by linarith
  2598   then show ?thesis
  2599   proof cases
  2600     case 1
  2601     let ?n = "of_int (floor (x/a)) + 1"
  2602     have x: "x < ?n * a"
  2603       by (meson \<open>0 < a\<close> divide_less_eq floor_unique_iff)
  2604     have "?n * a \<le> a + x"
  2605       apply (simp add: algebra_simps)
  2606       by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_divide_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
  2607     also have "... < y"
  2608       by (rule 1)
  2609     finally have "?n * a < y" .
  2610     with x show ?thesis
  2611       using Ints_1 Ints_add Ints_of_int that by blast
  2612   next
  2613     case 2
  2614     let ?n = "of_int (floor (y/a)) + 1"
  2615     have y: "y < ?n * a"
  2616       by (meson \<open>0 < a\<close> divide_less_eq floor_unique_iff)
  2617     have "?n * a \<le> a + y"
  2618       apply (simp add: algebra_simps)
  2619       by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_divide_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
  2620     also have "... < x"
  2621       by (rule 2)
  2622     finally have "?n * a < x" .
  2623     then show ?thesis
  2624       using Ints_1 Ints_add Ints_of_int that y by blast
  2625   qed
  2626 qed
  2627 
  2628 
  2629 lemma cell_subdivision_lemma:
  2630   assumes "finite \<F>"
  2631       and "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
  2632       and "\<And>X. X \<in> \<F> \<Longrightarrow> aff_dim X \<le> d"
  2633       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"
  2634       and "finite I"
  2635     shows "\<exists>\<F>'. \<Union>\<F>' = \<Union>\<F> \<and>
  2636                  finite \<F>' \<and>
  2637                  (\<forall>X \<in> \<F>'. polytope X) \<and>
  2638                  (\<forall>X \<in> \<F>'. aff_dim X \<le> d) \<and>
  2639                  (\<forall>X \<in> \<F>'. \<forall>Y \<in> \<F>'. X \<inter> Y face_of X \<and> X \<inter> Y face_of Y) \<and>
  2640                  (\<forall>X \<in> \<F>'. \<forall>x \<in> X. \<forall>y \<in> X. \<forall>a b.
  2641                           (a,b) \<in> I \<longrightarrow> a \<bullet> x \<le> b \<and> a \<bullet> y \<le> b \<or>
  2642                                         a \<bullet> x \<ge> b \<and> a \<bullet> y \<ge> b)"
  2643   using \<open>finite I\<close>
  2644 proof induction
  2645   case empty
  2646   then show ?case
  2647     by (rule_tac x="\<F>" in exI) (simp add: assms)
  2648 next
  2649   case (insert ab I)
  2650   then obtain \<F>' where eq: "\<Union>\<F>' = \<Union>\<F>" and "finite \<F>'"
  2651                    and poly: "\<And>X. X \<in> \<F>' \<Longrightarrow> polytope X"
  2652                    and aff: "\<And>X. X \<in> \<F>' \<Longrightarrow> aff_dim X \<le> d"
  2653                    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"
  2654                    and I: "\<And>X x y a b.  \<lbrakk>X \<in> \<F>'; x \<in> X; y \<in> X; (a,b) \<in> I\<rbrakk> \<Longrightarrow>
  2655                                     a \<bullet> x \<le> b \<and> a \<bullet> y \<le> b \<or> a \<bullet> x \<ge> b \<and> a \<bullet> y \<ge> b"
  2656     by (auto simp: that)
  2657   obtain a b where "ab = (a,b)"
  2658     by fastforce
  2659   let ?\<G> = "(\<lambda>X. X \<inter> {x. a \<bullet> x \<le> b}) ` \<F>' \<union> (\<lambda>X. X \<inter> {x. a \<bullet> x \<ge> b}) ` \<F>'"
  2660   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
  2661     by blast
  2662   show ?case
  2663   proof (intro conjI exI)
  2664     show "\<Union>?\<G> = \<Union>\<F>"
  2665       by (force simp: eq [symmetric])
  2666     show "finite ?\<G>"
  2667       using \<open>finite \<F>'\<close> by force
  2668     show "\<forall>X \<in> ?\<G>. polytope X"
  2669       by (force simp: poly polytope_Int_polyhedron polyhedron_halfspace_le polyhedron_halfspace_ge)
  2670     show "\<forall>X \<in> ?\<G>. aff_dim X \<le> d"
  2671       by (auto; metis order_trans aff aff_dim_subset inf_le1)
  2672     show "\<forall>X \<in> ?\<G>. \<forall>x \<in> X. \<forall>y \<in> X. \<forall>a b.
  2673                           (a,b) \<in> insert ab I \<longrightarrow> a \<bullet> x \<le> b \<and> a \<bullet> y \<le> b \<or>
  2674                                                   a \<bullet> x \<ge> b \<and> a \<bullet> y \<ge> b"
  2675       using \<open>ab = (a, b)\<close> I by fastforce
  2676     show "\<forall>X \<in> ?\<G>. \<forall>Y \<in> ?\<G>. X \<inter> Y face_of X \<and> X \<inter> Y face_of Y"
  2677       by (auto simp: eqInt halfspace_Int_eq face_of_Int_Int face face_of_halfspace_le face_of_halfspace_ge)
  2678   qed
  2679 qed
  2680 
  2681 
  2682 proposition cell_complex_subdivision_exists:
  2683   fixes \<F> :: "'a::euclidean_space set set"
  2684   assumes "0 < e" "finite \<F>"
  2685       and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X"
  2686       and aff: "\<And>X. X \<in> \<F> \<Longrightarrow> aff_dim X \<le> d"
  2687       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"
  2688   obtains "\<F>'" where "finite \<F>'" "\<Union>\<F>' = \<Union>\<F>" "\<And>X. X \<in> \<F>' \<Longrightarrow> diameter X < e"
  2689                 "\<And>X. X \<in> \<F>' \<Longrightarrow> polytope X" "\<And>X. X \<in> \<F>' \<Longrightarrow> aff_dim X \<le> d"
  2690                 "\<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"
  2691 proof -
  2692   have "bounded(\<Union>\<F>)"
  2693     by (simp add: \<open>finite \<F>\<close> poly bounded_Union polytope_imp_bounded)
  2694   then obtain B where "B > 0" and B: "\<And>x. x \<in> \<Union>\<F> \<Longrightarrow> norm x < B"
  2695     by (meson bounded_pos_less)
  2696   define C where "C \<equiv> {z \<in> \<int>. \<bar>z * e / 2 / real DIM('a)\<bar> \<le> B}"
  2697   define I where "I \<equiv> \<Union>i \<in> Basis. \<Union>j \<in> C. { (i::'a, j * e / 2 / DIM('a)) }"
  2698   have "finite C"
  2699     using finite_int_segment [of "-B / (e / 2 / DIM('a))" "B / (e / 2 / DIM('a))"]
  2700     apply (simp add: C_def)
  2701     apply (erule rev_finite_subset)
  2702     using \<open>0 < e\<close>
  2703     apply (auto simp: divide_simps)
  2704     done
  2705   then have "finite I"
  2706     by (simp add: I_def)
  2707   obtain \<F>' where eq: "\<Union>\<F>' = \<Union>\<F>" and "finite \<F>'"
  2708               and poly: "\<And>X. X \<in> \<F>' \<Longrightarrow> polytope X"
  2709               and aff: "\<And>X. X \<in> \<F>' \<Longrightarrow> aff_dim X \<le> d"
  2710               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"
  2711               and I: "\<And>X x y a b.  \<lbrakk>X \<in> \<F>'; x \<in> X; y \<in> X; (a,b) \<in> I\<rbrakk> \<Longrightarrow>
  2712                                      a \<bullet> x \<le> b \<and> a \<bullet> y \<le> b \<or> a \<bullet> x \<ge> b \<and> a \<bullet> y \<ge> b"
  2713     apply (rule exE [OF cell_subdivision_lemma])
  2714          apply (rule assms \<open>finite I\<close> | assumption)+
  2715     apply (auto intro: that)
  2716     done
  2717   show ?thesis
  2718   proof (rule_tac \<F>'="\<F>'" in that)
  2719     show "diameter X < e" if "X \<in> \<F>'" for X
  2720     proof -
  2721       have "diameter X \<le> e/2"
  2722       proof (rule diameter_le)
  2723         show "norm (x - y) \<le> e / 2" if "x \<in> X" "y \<in> X" for x y
  2724         proof -
  2725           have "norm x < B" "norm y < B"
  2726             using B \<open>X \<in> \<F>'\<close> eq that by fastforce+
  2727           have "norm (x - y) \<le> (\<Sum>b\<in>Basis. \<bar>(x-y) \<bullet> b\<bar>)"
  2728             by (rule norm_le_l1)
  2729           also have "... \<le> of_nat (DIM('a)) * (e / 2 / DIM('a))"
  2730           proof (rule setsum_bounded_above)
  2731             fix i::'a
  2732             assume "i \<in> Basis"
  2733             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"
  2734               using I \<open>X \<in> \<F>'\<close> that
  2735               by (fastforce simp: I_def)
  2736             show "\<bar>(x - y) \<bullet> i\<bar> \<le> e / 2 / real DIM('a)"
  2737             proof (rule ccontr)
  2738               assume "\<not> \<bar>(x - y) \<bullet> i\<bar> \<le> e / 2 / real DIM('a)"
  2739               then have xyi: "\<bar>i \<bullet> x - i \<bullet> y\<bar> > e / 2 / real DIM('a)"
  2740                 by (simp add: inner_commute inner_diff_right)
  2741               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"
  2742                 using subdivide_interval [OF xyi] DIM_positive \<open>0 < e\<close>
  2743                 by (auto simp: zero_less_divide_iff)
  2744               have "\<bar>i \<bullet> x\<bar> < B"
  2745                 by (metis \<open>i \<in> Basis\<close> \<open>norm x < B\<close> inner_commute norm_bound_Basis_lt)
  2746               have "\<bar>i \<bullet> y\<bar> < B"
  2747                 by (metis \<open>i \<in> Basis\<close> \<open>norm y < B\<close> inner_commute norm_bound_Basis_lt)
  2748               have *: "\<bar>n * e\<bar> \<le> B * (2 * real DIM('a))"
  2749                       if "\<bar>ix\<bar> < B" "\<bar>iy\<bar> < B"
  2750                          and ix: "ix * (2 * real DIM('a)) < n * e"
  2751                          and iy: "n * e < iy * (2 * real DIM('a))" for ix iy
  2752               proof (rule abs_leI)
  2753                 have "iy * (2 * real DIM('a)) \<le> B * (2 * real DIM('a))"
  2754                   by (rule mult_right_mono) (use \<open>\<bar>iy\<bar> < B\<close> in linarith)+
  2755                 then show "n * e \<le> B * (2 * real DIM('a))"
  2756                   using iy by linarith
  2757               next
  2758                 have "- ix * (2 * real DIM('a)) \<le> B * (2 * real DIM('a))"
  2759                   by (rule mult_right_mono) (use \<open>\<bar>ix\<bar> < B\<close> in linarith)+
  2760                 then show "- (n * e) \<le> B * (2 * real DIM('a))"
  2761                   using ix by linarith
  2762               qed
  2763               have "n \<in> C"
  2764                 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>)
  2765               show False
  2766                 using  I' [OF \<open>n \<in> C\<close> refl] n  by auto
  2767             qed
  2768           qed
  2769           also have "... = e / 2"
  2770             by simp
  2771           finally show ?thesis .
  2772         qed
  2773       qed (use \<open>0 < e\<close> in force)
  2774       also have "... < e"
  2775         by (simp add: \<open>0 < e\<close>)
  2776       finally show ?thesis .
  2777     qed
  2778   qed (auto simp: eq poly aff face  \<open>finite \<F>'\<close>)
  2779 qed
  2780 
  2781 end