src/HOL/Analysis/Polytope.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (3 weeks ago)
changeset 69981 3dced198b9ec
parent 69922 4a9167f377b0
child 70136 f03a01a18c6e
permissions -rw-r--r--
more strict AFP properties;
nipkow@67968
     1
section \<open>Faces, Extreme Points, Polytopes, Polyhedra etc\<close>
lp15@63078
     2
lp15@63078
     3
text\<open>Ported from HOL Light by L C Paulson\<close>
lp15@63078
     4
lp15@63078
     5
theory Polytope
lp15@63078
     6
imports Cartesian_Euclidean_Space
lp15@63078
     7
begin
lp15@63078
     8
immler@69683
     9
subsection \<open>Faces of a (usually convex) set\<close>
ak2110@68833
    10
ak2110@68833
    11
definition%important face_of :: "['a::real_vector set, 'a set] \<Rightarrow> bool" (infixr "(face'_of)" 50)
lp15@63078
    12
  where
lp15@63078
    13
  "T face_of S \<longleftrightarrow>
lp15@63078
    14
        T \<subseteq> S \<and> convex T \<and>
lp15@63078
    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)"
lp15@63078
    16
ak2110@69730
    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"
lp15@63078
    18
  unfolding face_of_def by blast
lp15@63078
    19
ak2110@69730
    20
lemma face_of_translation_eq [simp]:
nipkow@67399
    21
    "((+) a ` T face_of (+) a ` S) \<longleftrightarrow> T face_of S"
lp15@63078
    22
proof -
nipkow@67399
    23
  have *: "\<And>a T S. T face_of S \<Longrightarrow> ((+) a ` T face_of (+) a ` S)"
lp15@63078
    24
    apply (simp add: face_of_def Ball_def, clarify)
lp15@63078
    25
    apply (drule open_segment_translation_eq [THEN iffD1])
lp15@63078
    26
    using inj_image_mem_iff inj_add_left apply metis
lp15@63078
    27
    done
lp15@63078
    28
  show ?thesis
lp15@63078
    29
    apply (rule iffI)
lp15@63078
    30
    apply (force simp: image_comp o_def dest: * [where a = "-a"])
lp15@63078
    31
    apply (blast intro: *)
lp15@63078
    32
    done
lp15@63078
    33
qed
lp15@63078
    34
ak2110@69730
    35
lemma face_of_linear_image:
lp15@63078
    36
  assumes "linear f" "inj f"
lp15@63078
    37
    shows "(f ` c face_of f ` S) \<longleftrightarrow> c face_of S"
lp15@63078
    38
by (simp add: face_of_def inj_image_subset_iff inj_image_mem_iff open_segment_linear_image assms)
lp15@63078
    39
ak2110@69730
    40
lemma face_of_refl: "convex S \<Longrightarrow> S face_of S"
lp15@63078
    41
  by (auto simp: face_of_def)
lp15@63078
    42
ak2110@69730
    43
lemma face_of_refl_eq: "S face_of S \<longleftrightarrow> convex S"
lp15@63078
    44
  by (auto simp: face_of_def)
lp15@63078
    45
ak2110@69730
    46
lemma empty_face_of [iff]: "{} face_of S"
lp15@63078
    47
  by (simp add: face_of_def)
lp15@63078
    48
ak2110@69730
    49
lemma face_of_empty [simp]: "S face_of {} \<longleftrightarrow> S = {}"
lp15@63078
    50
  by (meson empty_face_of face_of_def subset_empty)
lp15@63078
    51
ak2110@69730
    52
lemma face_of_trans [trans]: "\<lbrakk>S face_of T; T face_of u\<rbrakk> \<Longrightarrow> S face_of u"
lp15@63078
    53
  unfolding face_of_def by (safe; blast)
lp15@63078
    54
ak2110@69730
    55
lemma face_of_face: "T face_of S \<Longrightarrow> (f face_of T \<longleftrightarrow> f face_of S \<and> f \<subseteq> T)"
lp15@63078
    56
  unfolding face_of_def by (safe; blast)
lp15@63078
    57
ak2110@69730
    58
lemma face_of_subset: "\<lbrakk>F face_of S; F \<subseteq> T; T \<subseteq> S\<rbrakk> \<Longrightarrow> F face_of T"
lp15@63078
    59
  unfolding face_of_def by (safe; blast)
lp15@63078
    60
ak2110@69730
    61
lemma face_of_slice: "\<lbrakk>F face_of S; convex T\<rbrakk> \<Longrightarrow> (F \<inter> T) face_of (S \<inter> T)"
lp15@63078
    62
  unfolding face_of_def by (blast intro: convex_Int)
lp15@63078
    63
ak2110@69730
    64
lemma face_of_Int: "\<lbrakk>t1 face_of S; t2 face_of S\<rbrakk> \<Longrightarrow> (t1 \<inter> t2) face_of S"
lp15@63078
    65
  unfolding face_of_def by (blast intro: convex_Int)
lp15@63078
    66
ak2110@69730
    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"
lp15@63078
    68
  unfolding face_of_def by (blast intro: convex_Inter)
lp15@63078
    69
ak2110@69730
    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')"
lp15@63078
    71
  unfolding face_of_def by (blast intro: convex_Int)
lp15@63078
    72
ak2110@69730
    73
lemma face_of_imp_subset: "T face_of S \<Longrightarrow> T \<subseteq> S"
lp15@63078
    74
  unfolding face_of_def by blast
lp15@63078
    75
ak2110@69730
    76
proposition face_of_imp_eq_affine_Int:
lp15@66287
    77
  fixes S :: "'a::euclidean_space set"
lp15@66287
    78
  assumes S: "convex S"  and T: "T face_of S"
lp15@66287
    79
  shows "T = (affine hull T) \<inter> S"
ak2110@69730
    80
proof -
lp15@63078
    81
  have "convex T" using T by (simp add: face_of_def)
lp15@63078
    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
lp15@63078
    83
  proof -
lp15@63078
    84
    obtain e where "e>0" and e: "cball y e \<inter> affine hull T \<subseteq> T"
lp15@63078
    85
      using y by (auto simp: rel_interior_cball)
lp15@63078
    86
    have "y \<noteq> x" "y \<in> S" "y \<in> T"
lp15@63078
    87
      using face_of_imp_subset rel_interior_subset T that by blast+
lp15@63078
    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"
lp15@63078
    89
      using \<open>x \<in> S\<close> \<open>x \<notin> T\<close> \<open>T face_of S\<close> unfolding face_of_def
lp15@63078
    90
      apply clarify
lp15@63078
    91
      apply (drule_tac x=x in bspec, assumption)
lp15@63078
    92
      apply (drule_tac x=y in bspec, assumption)
lp15@63078
    93
      apply (subst (asm) open_segment_commute)
lp15@63078
    94
      apply (force simp: open_segment_image_interval image_def)
lp15@63078
    95
      done
lp15@63078
    96
    have in01: "min (1/2) (e / norm (x - y)) \<in> {0<..<1}"
lp15@63078
    97
      using \<open>y \<noteq> x\<close> \<open>e > 0\<close> by simp
lp15@63078
    98
    show ?thesis
lp15@63078
    99
      apply (rule zne [OF in01])
lp15@63078
   100
      apply (rule e [THEN subsetD])
lp15@63078
   101
      apply (rule IntI)
wenzelm@63145
   102
        using \<open>y \<noteq> x\<close> \<open>e > 0\<close>
lp15@63078
   103
        apply (simp add: cball_def dist_norm algebra_simps)
lp15@63078
   104
        apply (simp add: Real_Vector_Spaces.scaleR_diff_right [symmetric] norm_minus_commute min_mult_distrib_right)
lp15@63078
   105
      apply (rule mem_affine [OF affine_affine_hull _ x])
lp15@63078
   106
      using \<open>y \<in> T\<close>  apply (auto simp: hull_inc)
lp15@63078
   107
      done
lp15@63078
   108
  qed
lp15@63078
   109
  show ?thesis
lp15@63078
   110
    apply (rule subset_antisym)
lp15@63078
   111
    using assms apply (simp add: hull_subset face_of_imp_subset)
lp15@63078
   112
    apply (cases "T={}", simp)
lp15@63078
   113
    apply (force simp: rel_interior_eq_empty [symmetric] \<open>convex T\<close> intro: *)
lp15@63078
   114
    done
lp15@63078
   115
qed
lp15@63078
   116
ak2110@69730
   117
lemma face_of_imp_closed:
lp15@63078
   118
     fixes S :: "'a::euclidean_space set"
lp15@63078
   119
     assumes "convex S" "closed S" "T face_of S" shows "closed T"
lp15@63078
   120
  by (metis affine_affine_hull affine_closed closed_Int face_of_imp_eq_affine_Int assms)
lp15@63078
   121
ak2110@69730
   122
lemma face_of_Int_supporting_hyperplane_le_strong:
lp15@63078
   123
    assumes "convex(S \<inter> {x. a \<bullet> x = b})" and aleb: "\<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b"
lp15@63078
   124
      shows "(S \<inter> {x. a \<bullet> x = b}) face_of S"
ak2110@69730
   125
proof -
lp15@63078
   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"
lp15@63078
   127
          for u v x
lp15@63078
   128
  proof (rule antisym)
lp15@63078
   129
    show "a \<bullet> u \<le> a \<bullet> x"
lp15@63078
   130
      using aleb \<open>u \<in> S\<close> \<open>b = a \<bullet> x\<close> by blast
lp15@63078
   131
  next
lp15@63078
   132
    obtain \<xi> where "b = a \<bullet> ((1 - \<xi>) *\<^sub>R u + \<xi> *\<^sub>R v)" "0 < \<xi>" "\<xi> < 1"
lp15@63078
   133
      using \<open>b = a \<bullet> x\<close> \<open>x \<in> open_segment u v\<close> in_segment
lp15@63078
   134
      by (auto simp: open_segment_image_interval split: if_split_asm)
lp15@63078
   135
    then have "b + \<xi> * (a \<bullet> u) \<le> a \<bullet> u + \<xi> * b"
lp15@63078
   136
      using aleb [OF \<open>v \<in> S\<close>] by (simp add: algebra_simps)
lp15@63078
   137
    then have "(1 - \<xi>) * b \<le> (1 - \<xi>) * (a \<bullet> u)"
lp15@63078
   138
      by (simp add: algebra_simps)
lp15@63078
   139
    then have "b \<le> a \<bullet> u"
lp15@63078
   140
      using \<open>\<xi> < 1\<close> by auto
lp15@63078
   141
    with b show "a \<bullet> x \<le> a \<bullet> u" by simp
lp15@63078
   142
  qed
lp15@63078
   143
  show ?thesis
lp15@63078
   144
    apply (simp add: face_of_def assms)
lp15@63078
   145
    using "*" open_segment_commute by blast
lp15@63078
   146
qed
lp15@63078
   147
ak2110@69730
   148
lemma face_of_Int_supporting_hyperplane_ge_strong:
lp15@63078
   149
   "\<lbrakk>convex(S \<inter> {x. a \<bullet> x = b}); \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<ge> b\<rbrakk>
lp15@63078
   150
    \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) face_of S"
lp15@63078
   151
  using face_of_Int_supporting_hyperplane_le_strong [of S "-a" "-b"] by simp
lp15@63078
   152
ak2110@69730
   153
lemma face_of_Int_supporting_hyperplane_le:
lp15@63078
   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"
lp15@63078
   155
  by (simp add: convex_Int convex_hyperplane face_of_Int_supporting_hyperplane_le_strong)
lp15@63078
   156
ak2110@69730
   157
lemma face_of_Int_supporting_hyperplane_ge:
lp15@63078
   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"
lp15@63078
   159
  by (simp add: convex_Int convex_hyperplane face_of_Int_supporting_hyperplane_ge_strong)
lp15@63078
   160
ak2110@69730
   161
lemma face_of_imp_convex: "T face_of S \<Longrightarrow> convex T"
lp15@63078
   162
  using face_of_def by blast
lp15@63078
   163
ak2110@69730
   164
lemma face_of_imp_compact:
lp15@63078
   165
    fixes S :: "'a::euclidean_space set"
lp15@63078
   166
    shows "\<lbrakk>convex S; compact S; T face_of S\<rbrakk> \<Longrightarrow> compact T"
lp15@63078
   167
  by (meson bounded_subset compact_eq_bounded_closed face_of_imp_closed face_of_imp_subset)
lp15@63078
   168
ak2110@69730
   169
lemma face_of_Int_subface:
lp15@63469
   170
     "\<lbrakk>A \<inter> B face_of A; A \<inter> B face_of B; C face_of A; D face_of B\<rbrakk>
lp15@63469
   171
      \<Longrightarrow> (C \<inter> D) face_of C \<and> (C \<inter> D) face_of D"
lp15@63078
   172
  by (meson face_of_Int_Int face_of_face inf_le1 inf_le2)
lp15@63078
   173
ak2110@69730
   174
lemma subset_of_face_of:
lp15@63078
   175
    fixes S :: "'a::real_normed_vector set"
lp15@63078
   176
    assumes "T face_of S" "u \<subseteq> S" "T \<inter> (rel_interior u) \<noteq> {}"
lp15@63078
   177
      shows "u \<subseteq> T"
lp15@63078
   178
proof
lp15@63078
   179
  fix c
lp15@63078
   180
  assume "c \<in> u"
lp15@63078
   181
  obtain b where "b \<in> T" "b \<in> rel_interior u" using assms by auto
lp15@63078
   182
  then obtain e where "e>0" "b \<in> u" and e: "cball b e \<inter> affine hull u \<subseteq> u"
lp15@63078
   183
    by (auto simp: rel_interior_cball)
lp15@63078
   184
  show "c \<in> T"
lp15@63078
   185
  proof (cases "b=c")
lp15@63078
   186
    case True with \<open>b \<in> T\<close> show ?thesis by blast
lp15@63078
   187
  next
lp15@63078
   188
    case False
wenzelm@63148
   189
    define d where "d = b + (e / norm(b - c)) *\<^sub>R (b - c)"
lp15@63078
   190
    have "d \<in> cball b e \<inter> affine hull u"
lp15@63078
   191
      using \<open>e > 0\<close> \<open>b \<in> u\<close> \<open>c \<in> u\<close>
lp15@63078
   192
      by (simp add: d_def dist_norm hull_inc mem_affine_3_minus False)
lp15@63078
   193
    with e have "d \<in> u" by blast
lp15@63078
   194
    have nbc: "norm (b - c) + e > 0" using \<open>e > 0\<close>
lp15@63078
   195
      by (metis add.commute le_less_trans less_add_same_cancel2 norm_ge_zero)
lp15@63078
   196
    then have [simp]: "d \<noteq> c" using False scaleR_cancel_left [of "1 + (e / norm (b - c))" b c]
lp15@63078
   197
      by (simp add: algebra_simps d_def) (simp add: divide_simps)
lp15@63078
   198
    have [simp]: "((e - e * e / (e + norm (b - c))) / norm (b - c)) = (e / (e + norm (b - c)))"
lp15@63078
   199
      using False nbc
immler@68072
   200
      by (simp add: divide_simps) (simp add: algebra_simps)
lp15@63078
   201
    have "b \<in> open_segment d c"
lp15@63078
   202
      apply (simp add: open_segment_image_interval)
lp15@63078
   203
      apply (simp add: d_def algebra_simps image_def)
lp15@63078
   204
      apply (rule_tac x="e / (e + norm (b - c))" in bexI)
lp15@63078
   205
      using False nbc \<open>0 < e\<close>
lp15@63078
   206
      apply (auto simp: algebra_simps)
lp15@63078
   207
      done
lp15@63078
   208
    then have "d \<in> T \<and> c \<in> T"
lp15@63078
   209
      apply (rule face_ofD [OF \<open>T face_of S\<close>])
wenzelm@63145
   210
      using \<open>d \<in> u\<close>  \<open>c \<in> u\<close> \<open>u \<subseteq> S\<close>  \<open>b \<in> T\<close>  apply auto
lp15@63078
   211
      done
lp15@63078
   212
    then show ?thesis ..
lp15@63078
   213
  qed
lp15@63078
   214
qed
lp15@63078
   215
ak2110@69730
   216
lemma face_of_eq:
lp15@63078
   217
    fixes S :: "'a::real_normed_vector set"
lp15@63078
   218
    assumes "T face_of S" "u face_of S" "(rel_interior T) \<inter> (rel_interior u) \<noteq> {}"
lp15@63078
   219
      shows "T = u"
lp15@63078
   220
  apply (rule subset_antisym)
lp15@63078
   221
  apply (metis assms disjoint_iff_not_equal face_of_imp_subset rel_interior_subset subsetCE subset_of_face_of)
lp15@63078
   222
  by (metis assms disjoint_iff_not_equal face_of_imp_subset rel_interior_subset subset_iff subset_of_face_of)
lp15@63078
   223
ak2110@69730
   224
lemma face_of_disjoint_rel_interior:
lp15@63078
   225
      fixes S :: "'a::real_normed_vector set"
lp15@63078
   226
      assumes "T face_of S" "T \<noteq> S"
lp15@63078
   227
        shows "T \<inter> rel_interior S = {}"
lp15@63078
   228
  by (meson assms subset_of_face_of face_of_imp_subset order_refl subset_antisym)
lp15@63078
   229
ak2110@69730
   230
lemma face_of_disjoint_interior:
lp15@63078
   231
      fixes S :: "'a::real_normed_vector set"
lp15@63078
   232
      assumes "T face_of S" "T \<noteq> S"
lp15@63078
   233
        shows "T \<inter> interior S = {}"
lp15@63078
   234
proof -
lp15@63078
   235
  have "T \<inter> interior S \<subseteq> rel_interior S"
lp15@63078
   236
    by (meson inf_sup_ord(2) interior_subset_rel_interior order.trans)
lp15@63078
   237
  thus ?thesis
lp15@63078
   238
    by (metis (no_types) Int_greatest assms face_of_disjoint_rel_interior inf_sup_ord(1) subset_empty)
lp15@63078
   239
qed
lp15@63078
   240
ak2110@69730
   241
lemma face_of_subset_rel_boundary:
lp15@63078
   242
  fixes S :: "'a::real_normed_vector set"
lp15@63078
   243
  assumes "T face_of S" "T \<noteq> S"
lp15@63078
   244
    shows "T \<subseteq> (S - rel_interior S)"
lp15@63078
   245
by (meson DiffI assms disjoint_iff_not_equal face_of_disjoint_rel_interior face_of_imp_subset rev_subsetD subsetI)
lp15@63078
   246
ak2110@69730
   247
lemma face_of_subset_rel_frontier:
lp15@63078
   248
    fixes S :: "'a::real_normed_vector set"
lp15@63078
   249
    assumes "T face_of S" "T \<noteq> S"
lp15@63078
   250
      shows "T \<subseteq> rel_frontier S"
lp15@63078
   251
  using assms closure_subset face_of_disjoint_rel_interior face_of_imp_subset rel_frontier_def by fastforce
lp15@63078
   252
ak2110@69730
   253
lemma face_of_aff_dim_lt:
lp15@63078
   254
  fixes S :: "'a::euclidean_space set"
lp15@63078
   255
  assumes "convex S" "T face_of S" "T \<noteq> S"
lp15@63078
   256
    shows "aff_dim T < aff_dim S"
lp15@63078
   257
proof -
lp15@63078
   258
  have "aff_dim T \<le> aff_dim S"
lp15@63078
   259
    by (simp add: face_of_imp_subset aff_dim_subset assms)
lp15@63078
   260
  moreover have "aff_dim T \<noteq> aff_dim S"
lp15@63078
   261
  proof (cases "T = {}")
lp15@63078
   262
    case True then show ?thesis
lp15@63078
   263
      by (metis aff_dim_empty \<open>T \<noteq> S\<close>)
lp15@63078
   264
  next case False then show ?thesis
lp15@63078
   265
    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)
lp15@63078
   266
  qed
lp15@63078
   267
  ultimately show ?thesis
lp15@63078
   268
    by simp
lp15@63078
   269
qed
lp15@63078
   270
ak2110@69730
   271
lemma subset_of_face_of_affine_hull:
lp15@66287
   272
    fixes S :: "'a::euclidean_space set"
nipkow@69508
   273
  assumes T: "T face_of S" and "convex S" "U \<subseteq> S" and dis: "\<not> disjnt (affine hull T) (rel_interior U)"
lp15@66287
   274
  shows "U \<subseteq> T"
lp15@66287
   275
  apply (rule subset_of_face_of [OF T \<open>U \<subseteq> S\<close>])
lp15@66287
   276
  using face_of_imp_eq_affine_Int [OF \<open>convex S\<close> T]
lp15@66287
   277
  using rel_interior_subset [of U] dis
lp15@66287
   278
  using \<open>U \<subseteq> S\<close> disjnt_def by fastforce
lp15@66287
   279
ak2110@69730
   280
lemma affine_hull_face_of_disjoint_rel_interior:
lp15@66287
   281
    fixes S :: "'a::euclidean_space set"
lp15@66287
   282
  assumes "convex S" "F face_of S" "F \<noteq> S"
lp15@66287
   283
  shows "affine hull F \<inter> rel_interior S = {}"
lp15@66287
   284
  by (metis assms disjnt_def face_of_imp_subset order_refl subset_antisym subset_of_face_of_affine_hull)
lp15@63078
   285
ak2110@69730
   286
lemma affine_diff_divide:
lp15@63078
   287
    assumes "affine S" "k \<noteq> 0" "k \<noteq> 1" and xy: "x \<in> S" "y /\<^sub>R (1 - k) \<in> S"
lp15@63078
   288
      shows "(x - y) /\<^sub>R k \<in> S"
lp15@63078
   289
proof -
lp15@63078
   290
  have "inverse(k) *\<^sub>R (x - y) = (1 - inverse k) *\<^sub>R inverse(1 - k) *\<^sub>R y + inverse(k) *\<^sub>R x"
lp15@63078
   291
    using assms
lp15@63078
   292
    by (simp add: algebra_simps) (simp add: scaleR_left_distrib [symmetric] divide_simps)
lp15@63078
   293
  then show ?thesis
lp15@63078
   294
    using \<open>affine S\<close> xy by (auto simp: affine_alt)
lp15@63078
   295
qed
lp15@63078
   296
ak2110@69730
   297
proposition face_of_convex_hulls:
lp15@63078
   298
      assumes S: "finite S" "T \<subseteq> S" and disj: "affine hull T \<inter> convex hull (S - T) = {}"
lp15@63078
   299
      shows  "(convex hull T) face_of (convex hull S)"
ak2110@69730
   300
proof -
lp15@63078
   301
  have fin: "finite T" "finite (S - T)" using assms
lp15@63078
   302
    by (auto simp: finite_subset)
lp15@63078
   303
  have *: "x \<in> convex hull T"
lp15@63078
   304
          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"
lp15@63078
   305
          for x y w
lp15@63078
   306
  proof -
lp15@63078
   307
    have waff: "w \<in> affine hull T"
lp15@63078
   308
      using convex_hull_subset_affine_hull w by blast
nipkow@64267
   309
    obtain a b where a: "\<And>i. i \<in> S \<Longrightarrow> 0 \<le> a i" and asum: "sum a S = 1" and aeqx: "(\<Sum>i\<in>S. a i *\<^sub>R i) = x"
nipkow@64267
   310
                 and b: "\<And>i. i \<in> S \<Longrightarrow> 0 \<le> b i" and bsum: "sum b S = 1" and beqy: "(\<Sum>i\<in>S. b i *\<^sub>R i) = y"
lp15@63078
   311
      using x y by (auto simp: assms convex_hull_finite)
lp15@63078
   312
    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"
lp15@63078
   313
               and u01: "0 < u" "u < 1"
lp15@63078
   314
      using w by (auto simp: open_segment_image_interval split: if_split_asm)
wenzelm@63148
   315
    define c where "c i = (1 - u) * a i + u * b i" for i
lp15@63078
   316
    have cge0: "\<And>i. i \<in> S \<Longrightarrow> 0 \<le> c i"
lp15@63078
   317
      using a b u01 by (simp add: c_def)
nipkow@64267
   318
    have sumc1: "sum c S = 1"
nipkow@64267
   319
      by (simp add: c_def sum.distrib sum_distrib_left [symmetric] asum bsum)
lp15@63078
   320
    have sumci_xy: "(\<Sum>i\<in>S. c i *\<^sub>R i) = (1 - u) *\<^sub>R x + u *\<^sub>R y"
nipkow@64267
   321
      apply (simp add: c_def sum.distrib scaleR_left_distrib)
nipkow@64267
   322
      by (simp only: scaleR_scaleR [symmetric] Real_Vector_Spaces.scaleR_right.sum [symmetric] aeqx beqy)
lp15@63078
   323
    show ?thesis
nipkow@64267
   324
    proof (cases "sum c (S - T) = 0")
lp15@63078
   325
      case True
lp15@63078
   326
      have ci0: "\<And>i. i \<in> (S - T) \<Longrightarrow> c i = 0"
lp15@65680
   327
        using True cge0 fin(2) sum_nonneg_eq_0_iff by auto
lp15@63078
   328
      have a0: "a i = 0" if "i \<in> (S - T)" for i
lp15@63078
   329
        using ci0 [OF that] u01 a [of i] b [of i] that
lp15@63078
   330
        by (simp add: c_def Groups.ordered_comm_monoid_add_class.add_nonneg_eq_0_iff)
nipkow@64267
   331
      have [simp]: "sum a T = 1"
nipkow@64267
   332
        using assms by (metis sum.mono_neutral_cong_right a0 asum)
lp15@63078
   333
      show ?thesis
lp15@63078
   334
        apply (simp add: convex_hull_finite \<open>finite T\<close>)
lp15@63078
   335
        apply (rule_tac x=a in exI)
lp15@63078
   336
        using a0 assms
nipkow@64267
   337
        apply (auto simp: cge0 a aeqx [symmetric] sum.mono_neutral_right)
lp15@63078
   338
        done
lp15@63078
   339
    next
lp15@63078
   340
      case False
nipkow@64267
   341
      define k where "k = sum c (S - T)"
lp15@63078
   342
      have "k > 0" using False
nipkow@64267
   343
        unfolding k_def by (metis DiffD1 antisym_conv cge0 sum_nonneg not_less)
nipkow@64267
   344
      have weq_sumsum: "w = sum (\<lambda>x. c x *\<^sub>R x) T + sum (\<lambda>x. c x *\<^sub>R x) (S - T)"
nipkow@64267
   345
        by (metis (no_types) add.commute S(1) S(2) sum.subset_diff sumci_xy weq)
lp15@63078
   346
      show ?thesis
lp15@63078
   347
      proof (cases "k = 1")
lp15@63078
   348
        case True
nipkow@64267
   349
        then have "sum c T = 0"
nipkow@64267
   350
          by (simp add: S k_def sum_diff sumc1)
nipkow@64267
   351
        then have [simp]: "sum c (S - T) = 1"
nipkow@64267
   352
          by (simp add: S sum_diff sumc1)
lp15@63078
   353
        have ci0: "\<And>i. i \<in> T \<Longrightarrow> c i = 0"
nipkow@64267
   354
          by (meson \<open>finite T\<close> \<open>sum c T = 0\<close> \<open>T \<subseteq> S\<close> cge0 sum_nonneg_eq_0_iff subsetCE)
lp15@63078
   355
        then have [simp]: "(\<Sum>i\<in>S-T. c i *\<^sub>R i) = w"
lp15@63078
   356
          by (simp add: weq_sumsum)
lp15@63078
   357
        have "w \<in> convex hull (S - T)"
lp15@63078
   358
          apply (simp add: convex_hull_finite fin)
lp15@63078
   359
          apply (rule_tac x=c in exI)
lp15@63078
   360
          apply (auto simp: cge0 weq True k_def)
lp15@63078
   361
          done
lp15@63078
   362
        then show ?thesis
lp15@63078
   363
          using disj waff by blast
lp15@63078
   364
      next
lp15@63078
   365
        case False
nipkow@64267
   366
        then have sumcf: "sum c T = 1 - k"
nipkow@64267
   367
          by (simp add: S k_def sum_diff sumc1)
lp15@63078
   368
        have "(\<Sum>i\<in>T. c i *\<^sub>R i) /\<^sub>R (1 - k) \<in> convex hull T"
lp15@63078
   369
          apply (simp add: convex_hull_finite fin)
lp15@63078
   370
          apply (rule_tac x="\<lambda>i. inverse (1-k) * c i" in exI)
lp15@63078
   371
          apply auto
nipkow@64267
   372
          apply (metis sumcf cge0 inverse_nonnegative_iff_nonnegative mult_nonneg_nonneg S(2) sum_nonneg subsetCE)
nipkow@64267
   373
          apply (metis False mult.commute right_inverse right_minus_eq sum_distrib_left sumcf)
nipkow@64267
   374
          by (metis (mono_tags, lifting) scaleR_right.sum scaleR_scaleR sum.cong)
nipkow@64267
   375
        with \<open>0 < k\<close>  have "inverse(k) *\<^sub>R (w - sum (\<lambda>i. c i *\<^sub>R i) T) \<in> affine hull T"
lp15@63078
   376
          by (simp add: affine_diff_divide [OF affine_affine_hull] False waff convex_hull_subset_affine_hull [THEN subsetD])
nipkow@64267
   377
        moreover have "inverse(k) *\<^sub>R (w - sum (\<lambda>x. c x *\<^sub>R x) T) \<in> convex hull (S - T)"
lp15@63078
   378
          apply (simp add: weq_sumsum convex_hull_finite fin)
lp15@63078
   379
          apply (rule_tac x="\<lambda>i. inverse k * c i" in exI)
lp15@63078
   380
          using \<open>k > 0\<close> cge0
nipkow@64267
   381
          apply (auto simp: scaleR_right.sum sum_distrib_left [symmetric] k_def [symmetric])
lp15@63078
   382
          done
lp15@63078
   383
        ultimately show ?thesis
lp15@63078
   384
          using disj by blast
lp15@63078
   385
      qed
lp15@63078
   386
    qed
lp15@63078
   387
  qed
lp15@63078
   388
  have [simp]: "convex hull T \<subseteq> convex hull S"
lp15@63078
   389
    by (simp add: \<open>T \<subseteq> S\<close> hull_mono)
lp15@63078
   390
  show ?thesis
lp15@63078
   391
    using open_segment_commute by (auto simp: face_of_def intro: *)
lp15@63078
   392
qed
lp15@63078
   393
ak2110@69730
   394
proposition face_of_convex_hull_insert:
lp15@63078
   395
   "\<lbrakk>finite S; a \<notin> affine hull S; T face_of convex hull S\<rbrakk> \<Longrightarrow> T face_of convex hull insert a S"
lp15@63078
   396
  apply (rule face_of_trans, blast)
lp15@63078
   397
  apply (rule face_of_convex_hulls; force simp: insert_Diff_if)
lp15@63078
   398
  done
lp15@63078
   399
ak2110@69730
   400
proposition face_of_affine_trivial:
lp15@63078
   401
    assumes "affine S" "T face_of S"
lp15@63078
   402
    shows "T = {} \<or> T = S"
ak2110@69730
   403
proof (rule ccontr, clarsimp)
lp15@63078
   404
  assume "T \<noteq> {}" "T \<noteq> S"
lp15@63078
   405
  then obtain a where "a \<in> T" by auto
lp15@63078
   406
  then have "a \<in> S"
lp15@63078
   407
    using \<open>T face_of S\<close> face_of_imp_subset by blast
lp15@63078
   408
  have "S \<subseteq> T"
lp15@63078
   409
  proof
lp15@63078
   410
    fix b  assume "b \<in> S"
lp15@63078
   411
    show "b \<in> T"
lp15@63078
   412
    proof (cases "a = b")
lp15@63078
   413
      case True with \<open>a \<in> T\<close> show ?thesis by auto
lp15@63078
   414
    next
lp15@63078
   415
      case False
lp15@63078
   416
      then have "a \<in> open_segment (2 *\<^sub>R a - b) b"
lp15@63078
   417
        apply (auto simp: open_segment_def closed_segment_def)
lp15@63078
   418
        apply (rule_tac x="1/2" in exI)
lp15@63078
   419
        apply (simp add: algebra_simps)
lp15@63078
   420
        by (simp add: scaleR_2)
lp15@63078
   421
      moreover have "2 *\<^sub>R a - b \<in> S"
lp15@63078
   422
        by (rule mem_affine [OF \<open>affine S\<close> \<open>a \<in> S\<close> \<open>b \<in> S\<close>, of 2 "-1", simplified])
lp15@63078
   423
      moreover note \<open>b \<in> S\<close> \<open>a \<in> T\<close>
lp15@63078
   424
      ultimately show ?thesis
lp15@63078
   425
        by (rule face_ofD [OF \<open>T face_of S\<close>, THEN conjunct2])
lp15@63078
   426
    qed
lp15@63078
   427
  qed
lp15@63078
   428
  then show False
wenzelm@63145
   429
    using \<open>T \<noteq> S\<close> \<open>T face_of S\<close> face_of_imp_subset by blast
lp15@63078
   430
qed
lp15@63078
   431
lp15@63078
   432
ak2110@69730
   433
lemma face_of_affine_eq:
lp15@63078
   434
   "affine S \<Longrightarrow> (T face_of S \<longleftrightarrow> T = {} \<or> T = S)"
lp15@63078
   435
using affine_imp_convex face_of_affine_trivial face_of_refl by auto
lp15@63078
   436
lp15@63078
   437
ak2110@69730
   438
proposition Inter_faces_finite_altbound:
lp15@63078
   439
    fixes T :: "'a::euclidean_space set set"
lp15@63078
   440
    assumes cfaI: "\<And>c. c \<in> T \<Longrightarrow> c face_of S"
lp15@63078
   441
    shows "\<exists>F'. finite F' \<and> F' \<subseteq> T \<and> card F' \<le> DIM('a) + 2 \<and> \<Inter>F' = \<Inter>T"
ak2110@69730
   442
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'))")
lp15@63078
   443
  case True
lp15@63078
   444
  then obtain c where c:
lp15@63078
   445
       "\<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')"
lp15@63078
   446
    by metis
wenzelm@63148
   447
  define d where "d = rec_nat {c{}} (\<lambda>n r. insert (c r) r)"
lp15@63078
   448
  have [simp]: "d 0 = {c {}}"
lp15@63078
   449
    by (simp add: d_def)
lp15@63078
   450
  have dSuc [simp]: "\<And>n. d (Suc n) = insert (c (d n)) (d n)"
lp15@63078
   451
    by (simp add: d_def)
lp15@63078
   452
  have dn_notempty: "d n \<noteq> {}" for n
lp15@63078
   453
    by (induction n) auto
lp15@63078
   454
  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
lp15@63078
   455
  using that
lp15@63078
   456
  proof (induction n)
lp15@63078
   457
    case 0
lp15@63078
   458
    then show ?case by (simp add: c)
lp15@63078
   459
  next
lp15@63078
   460
    case (Suc n)
lp15@63078
   461
    then show ?case by (auto simp: c card_insert_if)
lp15@63078
   462
  qed
lp15@63078
   463
  have aff_dim_le: "aff_dim(\<Inter>(d n)) \<le> DIM('a) - int n" if "n \<le> DIM('a) + 2" for n
lp15@63078
   464
  using that
lp15@63078
   465
  proof (induction n)
lp15@63078
   466
    case 0
lp15@63078
   467
    then show ?case
lp15@63078
   468
      by (simp add: aff_dim_le_DIM)
lp15@63078
   469
  next
lp15@63078
   470
    case (Suc n)
nipkow@69745
   471
    have fs: "\<Inter>(d (Suc n)) face_of S"
lp15@63078
   472
      by (meson Suc.prems cfaI dn_le_Suc dn_notempty face_of_Inter subsetCE)
nipkow@69745
   473
    have condn: "convex (\<Inter>(d n))"
lp15@63078
   474
      using Suc.prems nat_le_linear not_less_eq_eq
lp15@63078
   475
      by (blast intro: face_of_imp_convex cfaI convex_Inter dest: dn_le_Suc)
nipkow@69745
   476
    have fdn: "\<Inter>(d (Suc n)) face_of \<Inter>(d n)"
lp15@63078
   477
      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)
nipkow@69745
   478
    have ne: "\<Inter>(d (Suc n)) \<noteq> \<Inter>(d n)"
lp15@63078
   479
      by (metis (no_types, lifting) Suc.prems Suc_leD c complete_lattice_class.Inf_insert dSuc dn_le_Suc less_irrefl order.trans)
lp15@63078
   480
    have *: "\<And>m::int. \<And>d. \<And>d'::int. d < d' \<and> d' \<le> m - n \<Longrightarrow> d \<le> m - of_nat(n+1)"
lp15@63078
   481
      by arith
nipkow@69745
   482
    have "aff_dim (\<Inter>(d (Suc n))) < aff_dim (\<Inter>(d n))"
lp15@63078
   483
      by (rule face_of_aff_dim_lt [OF condn fdn ne])
nipkow@69745
   484
    moreover have "aff_dim (\<Inter>(d n)) \<le> int (DIM('a)) - int n"
lp15@63078
   485
      using Suc by auto
lp15@63078
   486
    ultimately
nipkow@69745
   487
    have "aff_dim (\<Inter>(d (Suc n))) \<le> int (DIM('a)) - (n+1)" by arith
lp15@63078
   488
    then show ?case by linarith
lp15@63078
   489
  qed
nipkow@69745
   490
  have "aff_dim (\<Inter>(d (DIM('a) + 2))) \<le> -2"
lp15@63078
   491
      using aff_dim_le [OF order_refl] by simp
nipkow@69745
   492
  with aff_dim_geq [of "\<Inter>(d (DIM('a) + 2))"] show ?thesis
lp15@63078
   493
    using order.trans by fastforce
lp15@63078
   494
next
lp15@63078
   495
  case False
lp15@63078
   496
  then show ?thesis
lp15@63078
   497
    apply simp
lp15@63078
   498
    apply (erule ex_forward)
lp15@63078
   499
    by blast
lp15@63078
   500
qed
lp15@63078
   501
ak2110@69730
   502
lemma faces_of_translation:
lp15@63078
   503
   "{F. F face_of image (\<lambda>x. a + x) S} = image (image (\<lambda>x. a + x)) {F. F face_of S}"
lp15@63078
   504
apply (rule subset_antisym, clarify)
lp15@63078
   505
apply (auto simp: image_iff)
lp15@63078
   506
apply (metis face_of_imp_subset face_of_translation_eq subset_imageE)
lp15@63078
   507
done
lp15@63078
   508
ak2110@69730
   509
proposition face_of_Times:
lp15@63078
   510
  assumes "F face_of S" and "F' face_of S'"
lp15@63078
   511
    shows "(F \<times> F') face_of (S \<times> S')"
ak2110@69730
   512
proof -
lp15@63078
   513
  have "F \<times> F' \<subseteq> S \<times> S'"
lp15@63078
   514
    using assms [unfolded face_of_def] by blast
lp15@63078
   515
  moreover
lp15@63078
   516
  have "convex (F \<times> F')"
lp15@63078
   517
    using assms [unfolded face_of_def] by (blast intro: convex_Times)
lp15@63078
   518
  moreover
lp15@63078
   519
    have "a \<in> F \<and> a' \<in> F' \<and> b \<in> F \<and> b' \<in> F'"
lp15@63078
   520
       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')"
lp15@63078
   521
       for a b a' b' x
lp15@63078
   522
  proof (cases "b=a \<or> b'=a'")
lp15@63078
   523
    case True with that show ?thesis
lp15@63078
   524
      using assms
lp15@63078
   525
      by (force simp: in_segment dest: face_ofD)
lp15@63078
   526
  next
lp15@63078
   527
    case False with assms [unfolded face_of_def] that show ?thesis
lp15@63078
   528
      by (blast dest!: open_segment_PairD)
lp15@63078
   529
  qed
lp15@63078
   530
  ultimately show ?thesis
lp15@63078
   531
    unfolding face_of_def by blast
lp15@63078
   532
qed
lp15@63078
   533
ak2110@69730
   534
corollary face_of_Times_decomp:
lp15@63078
   535
    fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
lp15@63078
   536
    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')"
lp15@63078
   537
     (is "?lhs = ?rhs")
ak2110@69730
   538
proof
lp15@63078
   539
  assume c: ?lhs
lp15@63078
   540
  show ?rhs
lp15@63078
   541
  proof (cases "c = {}")
lp15@63078
   542
    case True then show ?thesis by auto
lp15@63078
   543
  next
lp15@63078
   544
    case False
lp15@63078
   545
    have 1: "fst ` c \<subseteq> S" "snd ` c \<subseteq> S'"
lp15@63078
   546
      using c face_of_imp_subset by fastforce+
lp15@63078
   547
    have "convex c"
lp15@63078
   548
      using c by (metis face_of_imp_convex)
lp15@63078
   549
    have conv: "convex (fst ` c)" "convex (snd ` c)"
lp15@63078
   550
      by (simp_all add: \<open>convex c\<close> convex_linear_image fst_linear snd_linear)
lp15@63078
   551
    have fstab: "a \<in> fst ` c \<and> b \<in> fst ` c"
lp15@63078
   552
            if "a \<in> S" "b \<in> S" "x \<in> open_segment a b" "(x,x') \<in> c" for a b x x'
lp15@63078
   553
    proof -
lp15@63078
   554
      have *: "(x,x') \<in> open_segment (a,x') (b,x')"
lp15@63078
   555
        using that by (auto simp: in_segment)
lp15@63078
   556
      show ?thesis
lp15@63078
   557
        using face_ofD [OF c *] that face_of_imp_subset [OF c] by force
lp15@63078
   558
    qed
lp15@63078
   559
    have fst: "fst ` c face_of S"
lp15@63078
   560
      by (force simp: face_of_def 1 conv fstab)
lp15@63078
   561
    have sndab: "a' \<in> snd ` c \<and> b' \<in> snd ` c"
lp15@63078
   562
            if "a' \<in> S'" "b' \<in> S'" "x' \<in> open_segment a' b'" "(x,x') \<in> c" for a' b' x x'
lp15@63078
   563
    proof -
lp15@63078
   564
      have *: "(x,x') \<in> open_segment (x,a') (x,b')"
lp15@63078
   565
        using that by (auto simp: in_segment)
lp15@63078
   566
      show ?thesis
lp15@63078
   567
        using face_ofD [OF c *] that face_of_imp_subset [OF c] by force
lp15@63078
   568
    qed
lp15@63078
   569
    have snd: "snd ` c face_of S'"
lp15@63078
   570
      by (force simp: face_of_def 1 conv sndab)
lp15@63078
   571
    have cc: "rel_interior c \<subseteq> rel_interior (fst ` c) \<times> rel_interior (snd ` c)"
lp15@63078
   572
      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])
lp15@63078
   573
    have "c = fst ` c \<times> snd ` c"
lp15@63078
   574
      apply (rule face_of_eq [OF c])
lp15@63078
   575
      apply (simp_all add: face_of_Times rel_interior_Times conv fst snd)
lp15@63078
   576
      using False rel_interior_eq_empty \<open>convex c\<close> cc
lp15@63078
   577
      apply blast
lp15@63078
   578
      done
lp15@63078
   579
    with fst snd show ?thesis by metis
lp15@63078
   580
  qed
lp15@63078
   581
next
lp15@63078
   582
  assume ?rhs with face_of_Times show ?lhs by auto
lp15@63078
   583
qed
lp15@63078
   584
ak2110@69730
   585
lemma face_of_Times_eq:
lp15@63078
   586
    fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
lp15@63078
   587
    shows "(F \<times> F') face_of (S \<times> S') \<longleftrightarrow>
lp15@63078
   588
           F = {} \<or> F' = {} \<or> F face_of S \<and> F' face_of S'"
lp15@63078
   589
by (auto simp: face_of_Times_decomp times_eq_iff)
lp15@63078
   590
ak2110@69730
   591
lemma hyperplane_face_of_halfspace_le: "{x. a \<bullet> x = b} face_of {x. a \<bullet> x \<le> b}"
lp15@63078
   592
proof -
lp15@63078
   593
  have "{x. a \<bullet> x \<le> b} \<inter> {x. a \<bullet> x = b} = {x. a \<bullet> x = b}"
lp15@63078
   594
    by auto
lp15@63078
   595
  with face_of_Int_supporting_hyperplane_le [OF convex_halfspace_le [of a b], of a b]
lp15@63078
   596
  show ?thesis by auto
lp15@63078
   597
qed
lp15@63078
   598
ak2110@69730
   599
lemma hyperplane_face_of_halfspace_ge: "{x. a \<bullet> x = b} face_of {x. a \<bullet> x \<ge> b}"
lp15@63078
   600
proof -
lp15@63078
   601
  have "{x. a \<bullet> x \<ge> b} \<inter> {x. a \<bullet> x = b} = {x. a \<bullet> x = b}"
lp15@63078
   602
    by auto
lp15@63078
   603
  with face_of_Int_supporting_hyperplane_ge [OF convex_halfspace_ge [of b a], of b a]
lp15@63078
   604
  show ?thesis by auto
lp15@63078
   605
qed
lp15@63078
   606
ak2110@69730
   607
lemma face_of_halfspace_le:
lp15@63078
   608
  fixes a :: "'n::euclidean_space"
lp15@63078
   609
  shows "F face_of {x. a \<bullet> x \<le> b} \<longleftrightarrow>
lp15@63078
   610
         F = {} \<or> F = {x. a \<bullet> x = b} \<or> F = {x. a \<bullet> x \<le> b}"
lp15@63078
   611
     (is "?lhs = ?rhs")
ak2110@69730
   612
proof (cases "a = 0")
lp15@63078
   613
  case True then show ?thesis
lp15@63078
   614
    using face_of_affine_eq affine_UNIV by auto
lp15@63078
   615
next
lp15@63078
   616
  case False
lp15@63078
   617
  then have ine: "interior {x. a \<bullet> x \<le> b} \<noteq> {}"
lp15@63078
   618
    using halfspace_eq_empty_lt interior_halfspace_le by blast
lp15@63078
   619
  show ?thesis
lp15@63078
   620
  proof
lp15@63078
   621
    assume L: ?lhs
lp15@63078
   622
    have "F \<noteq> {x. a \<bullet> x \<le> b} \<Longrightarrow> F face_of {x. a \<bullet> x = b}"
lp15@63078
   623
      using False
lp15@63078
   624
      apply (simp add: frontier_halfspace_le [symmetric] rel_frontier_nonempty_interior [OF ine, symmetric])
lp15@63078
   625
      apply (rule face_of_subset [OF L])
lp15@63078
   626
      apply (simp add: face_of_subset_rel_frontier [OF L])
lp15@63078
   627
      apply (force simp: rel_frontier_def closed_halfspace_le)
lp15@63078
   628
      done
lp15@63078
   629
    with L show ?rhs
lp15@63078
   630
      using affine_hyperplane face_of_affine_eq by blast
lp15@63078
   631
  next
lp15@63078
   632
    assume ?rhs
lp15@63078
   633
    then show ?lhs
lp15@63078
   634
      by (metis convex_halfspace_le empty_face_of face_of_refl hyperplane_face_of_halfspace_le)
lp15@63078
   635
  qed
lp15@63078
   636
qed
lp15@63078
   637
ak2110@69730
   638
lemma face_of_halfspace_ge:
lp15@63078
   639
  fixes a :: "'n::euclidean_space"
lp15@63078
   640
  shows "F face_of {x. a \<bullet> x \<ge> b} \<longleftrightarrow>
lp15@63078
   641
         F = {} \<or> F = {x. a \<bullet> x = b} \<or> F = {x. a \<bullet> x \<ge> b}"
lp15@63078
   642
using face_of_halfspace_le [of F "-a" "-b"] by simp
lp15@63078
   643
immler@69683
   644
subsection\<open>Exposed faces\<close>
lp15@63078
   645
lp15@63078
   646
text\<open>That is, faces that are intersection with supporting hyperplane\<close>
lp15@63078
   647
ak2110@68833
   648
definition%important exposed_face_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"
lp15@63078
   649
                               (infixr "(exposed'_face'_of)" 50)
lp15@63078
   650
  where "T exposed_face_of S \<longleftrightarrow>
lp15@63078
   651
         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})"
lp15@63078
   652
ak2110@69730
   653
lemma empty_exposed_face_of [iff]: "{} exposed_face_of S"
lp15@63078
   654
  apply (simp add: exposed_face_of_def)
lp15@63078
   655
  apply (rule_tac x=0 in exI)
lp15@63078
   656
  apply (rule_tac x=1 in exI, force)
lp15@63078
   657
  done
lp15@63078
   658
ak2110@69730
   659
lemma exposed_face_of_refl_eq [simp]: "S exposed_face_of S \<longleftrightarrow> convex S"
lp15@63078
   660
  apply (simp add: exposed_face_of_def face_of_refl_eq, auto)
lp15@63078
   661
  apply (rule_tac x=0 in exI)+
lp15@63078
   662
  apply force
lp15@63078
   663
  done
lp15@63078
   664
ak2110@69730
   665
lemma exposed_face_of_refl: "convex S \<Longrightarrow> S exposed_face_of S"
lp15@63078
   666
  by simp
lp15@63078
   667
ak2110@69730
   668
lemma exposed_face_of:
lp15@63078
   669
    "T exposed_face_of S \<longleftrightarrow>
lp15@63078
   670
     T face_of S \<and>
lp15@63078
   671
     (T = {} \<or> T = S \<or>
lp15@63078
   672
      (\<exists>a b. a \<noteq> 0 \<and> S \<subseteq> {x. a \<bullet> x \<le> b} \<and> T = S \<inter> {x. a \<bullet> x = b}))"
lp15@63078
   673
proof (cases "T = {}")
lp15@63078
   674
  case True then show ?thesis
lp15@63078
   675
    by simp
lp15@63078
   676
next
lp15@63078
   677
  case False
lp15@63078
   678
  show ?thesis
lp15@63078
   679
  proof (cases "T = S")
lp15@63078
   680
    case True then show ?thesis
lp15@63078
   681
      by (simp add: face_of_refl_eq)
lp15@63078
   682
  next
lp15@63078
   683
    case False
lp15@63078
   684
    with \<open>T \<noteq> {}\<close> show ?thesis
lp15@63078
   685
      apply (auto simp: exposed_face_of_def)
lp15@63078
   686
      apply (metis inner_zero_left)
lp15@63078
   687
      done
lp15@63078
   688
  qed
lp15@63078
   689
qed
lp15@63078
   690
ak2110@69730
   691
lemma exposed_face_of_Int_supporting_hyperplane_le:
lp15@63078
   692
   "\<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"
lp15@63078
   693
by (force simp: exposed_face_of_def face_of_Int_supporting_hyperplane_le)
lp15@63078
   694
ak2110@69730
   695
lemma exposed_face_of_Int_supporting_hyperplane_ge:
lp15@63078
   696
   "\<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"
lp15@63078
   697
using exposed_face_of_Int_supporting_hyperplane_le [of S "-a" "-b"] by simp
lp15@63078
   698
ak2110@69730
   699
proposition exposed_face_of_Int:
lp15@63078
   700
  assumes "T exposed_face_of S"
lp15@63078
   701
      and "u exposed_face_of S"
lp15@63078
   702
    shows "(T \<inter> u) exposed_face_of S"
ak2110@69730
   703
proof -
lp15@63078
   704
  obtain a b where T: "S \<inter> {x. a \<bullet> x = b} face_of S"
lp15@63078
   705
               and S: "S \<subseteq> {x. a \<bullet> x \<le> b}"
lp15@63078
   706
               and teq: "T = S \<inter> {x. a \<bullet> x = b}"
lp15@63078
   707
    using assms by (auto simp: exposed_face_of_def)
lp15@63078
   708
  obtain a' b' where u: "S \<inter> {x. a' \<bullet> x = b'} face_of S"
lp15@63078
   709
                 and s': "S \<subseteq> {x. a' \<bullet> x \<le> b'}"
lp15@63078
   710
                 and ueq: "u = S \<inter> {x. a' \<bullet> x = b'}"
lp15@63078
   711
    using assms by (auto simp: exposed_face_of_def)
lp15@63078
   712
  have tu: "T \<inter> u face_of S"
lp15@63078
   713
    using T teq u ueq by (simp add: face_of_Int)
lp15@63078
   714
  have ss: "S \<subseteq> {x. (a + a') \<bullet> x \<le> b + b'}"
lp15@63078
   715
    using S s' by (force simp: inner_left_distrib)
lp15@63078
   716
  show ?thesis
lp15@63078
   717
    apply (simp add: exposed_face_of_def tu)
lp15@63078
   718
    apply (rule_tac x="a+a'" in exI)
lp15@63078
   719
    apply (rule_tac x="b+b'" in exI)
lp15@63078
   720
    using S s'
lp15@63078
   721
    apply (fastforce simp: ss inner_left_distrib teq ueq)
lp15@63078
   722
    done
lp15@63078
   723
qed
lp15@63078
   724
ak2110@69730
   725
proposition exposed_face_of_Inter:
lp15@63078
   726
    fixes P :: "'a::euclidean_space set set"
lp15@63078
   727
  assumes "P \<noteq> {}"
lp15@63078
   728
      and "\<And>T. T \<in> P \<Longrightarrow> T exposed_face_of S"
lp15@63078
   729
    shows "\<Inter>P exposed_face_of S"
ak2110@69730
   730
proof -
lp15@63078
   731
  obtain Q where "finite Q" and QsubP: "Q \<subseteq> P" "card Q \<le> DIM('a) + 2" and IntQ: "\<Inter>Q = \<Inter>P"
lp15@63078
   732
    using Inter_faces_finite_altbound [of P S] assms [unfolded exposed_face_of]
lp15@63078
   733
    by force
lp15@63078
   734
  show ?thesis
lp15@63078
   735
  proof (cases "Q = {}")
lp15@63078
   736
    case True then show ?thesis
eberlm@67829
   737
      by (metis IntQ Inter_UNIV_conv(2) assms(1) assms(2) ex_in_conv)
lp15@63078
   738
  next
lp15@63078
   739
    case False
lp15@63078
   740
    have "Q \<subseteq> {T. T exposed_face_of S}"
lp15@63078
   741
      using QsubP assms by blast
lp15@63078
   742
    moreover have "Q \<subseteq> {T. T exposed_face_of S} \<Longrightarrow> \<Inter>Q exposed_face_of S"
lp15@63078
   743
      using \<open>finite Q\<close> False
lp15@63078
   744
      apply (induction Q rule: finite_induct)
lp15@63078
   745
      using exposed_face_of_Int apply fastforce+
lp15@63078
   746
      done
lp15@63078
   747
    ultimately show ?thesis
lp15@63078
   748
      by (simp add: IntQ)
lp15@63078
   749
  qed
lp15@63078
   750
qed
lp15@63078
   751
ak2110@69730
   752
proposition exposed_face_of_sums:
lp15@63078
   753
  assumes "convex S" and "convex T"
lp15@63078
   754
      and "F exposed_face_of {x + y | x y. x \<in> S \<and> y \<in> T}"
lp15@63078
   755
          (is "F exposed_face_of ?ST")
lp15@63078
   756
  obtains k l
lp15@63078
   757
    where "k exposed_face_of S" "l exposed_face_of T"
lp15@63078
   758
          "F = {x + y | x y. x \<in> k \<and> y \<in> l}"
ak2110@69730
   759
proof (cases "F = {}")
lp15@63078
   760
  case True then show ?thesis
lp15@63078
   761
    using that by blast
lp15@63078
   762
next
lp15@63078
   763
  case False
lp15@63078
   764
  show ?thesis
lp15@63078
   765
  proof (cases "F = ?ST")
lp15@63078
   766
    case True then show ?thesis
lp15@63078
   767
      using assms exposed_face_of_refl_eq that by blast
lp15@63078
   768
  next
lp15@63078
   769
    case False
lp15@63078
   770
    obtain p where "p \<in> F" using \<open>F \<noteq> {}\<close> by blast
lp15@63078
   771
    moreover
lp15@63078
   772
    obtain u z where T: "?ST \<inter> {x. u \<bullet> x = z} face_of ?ST"
lp15@63078
   773
                 and S: "?ST \<subseteq> {x. u \<bullet> x \<le> z}"
lp15@63078
   774
                 and feq: "F = ?ST \<inter> {x. u \<bullet> x = z}"
lp15@63078
   775
      using assms by (auto simp: exposed_face_of_def)
lp15@63078
   776
    ultimately obtain a0 b0
lp15@63078
   777
            where p: "p = a0 + b0" and "a0 \<in> S" "b0 \<in> T" and z: "u \<bullet> p = z"
lp15@63078
   778
      by auto
lp15@63078
   779
    have lez: "u \<bullet> (x + y) \<le> z" if "x \<in> S" "y \<in> T" for x y
lp15@63078
   780
      using S that by auto
lp15@63078
   781
    have sef: "S \<inter> {x. u \<bullet> x = u \<bullet> a0} exposed_face_of S"
lp15@63078
   782
      apply (rule exposed_face_of_Int_supporting_hyperplane_le [OF \<open>convex S\<close>])
lp15@63078
   783
      apply (metis p z add_le_cancel_right inner_right_distrib lez [OF _ \<open>b0 \<in> T\<close>])
lp15@63078
   784
      done
lp15@63078
   785
    have tef: "T \<inter> {x. u \<bullet> x = u \<bullet> b0} exposed_face_of T"
lp15@63078
   786
      apply (rule exposed_face_of_Int_supporting_hyperplane_le [OF \<open>convex T\<close>])
lp15@63078
   787
      apply (metis p z add.commute add_le_cancel_right inner_right_distrib lez [OF \<open>a0 \<in> S\<close>])
lp15@63078
   788
      done
lp15@63078
   789
    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"
lp15@63078
   790
      by (auto simp: feq) (metis inner_right_distrib p z)
lp15@63078
   791
    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}"
lp15@63078
   792
      apply (auto simp: feq)
lp15@63078
   793
      apply (rename_tac x y)
lp15@63078
   794
      apply (rule_tac x=x in exI)
lp15@63078
   795
      apply (rule_tac x=y in exI, simp)
lp15@63078
   796
      using z p \<open>a0 \<in> S\<close> \<open>b0 \<in> T\<close>
lp15@63078
   797
      apply clarify
lp15@63078
   798
      apply (simp add: inner_right_distrib)
lp15@63078
   799
      apply (metis add_le_cancel_right antisym lez [unfolded inner_right_distrib] add.commute)
lp15@63078
   800
      done
lp15@63078
   801
    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}}"
lp15@63078
   802
      by blast
lp15@63078
   803
    then show ?thesis
lp15@63078
   804
      by (rule that [OF sef tef])
lp15@63078
   805
  qed
lp15@63078
   806
qed
lp15@63078
   807
ak2110@69730
   808
proposition exposed_face_of_parallel:
lp15@66652
   809
   "T exposed_face_of S \<longleftrightarrow>
lp15@66652
   810
         T face_of S \<and>
lp15@66652
   811
         (\<exists>a b. S \<subseteq> {x. a \<bullet> x \<le> b} \<and> T = S \<inter> {x. a \<bullet> x = b} \<and>
lp15@66652
   812
                (T \<noteq> {} \<longrightarrow> T \<noteq> S \<longrightarrow> a \<noteq> 0) \<and>
lp15@66652
   813
                (T \<noteq> S \<longrightarrow> (\<forall>w \<in> affine hull S. (w + a) \<in> affine hull S)))"
lp15@66652
   814
  (is "?lhs = ?rhs")
ak2110@69730
   815
proof
lp15@66652
   816
  assume ?lhs then show ?rhs
lp15@66652
   817
  proof (clarsimp simp: exposed_face_of_def)
lp15@66652
   818
    fix a b
lp15@66652
   819
    assume faceS: "S \<inter> {x. a \<bullet> x = b} face_of S" and Ssub: "S \<subseteq> {x. a \<bullet> x \<le> b}" 
lp15@66652
   820
    show "\<exists>c d. S \<subseteq> {x. c \<bullet> x \<le> d} \<and>
lp15@66652
   821
                S \<inter> {x. a \<bullet> x = b} = S \<inter> {x. c \<bullet> x = d} \<and>
lp15@66652
   822
                (S \<inter> {x. a \<bullet> x = b} \<noteq> {} \<longrightarrow> S \<inter> {x. a \<bullet> x = b} \<noteq> S \<longrightarrow> c \<noteq> 0) \<and>
lp15@66652
   823
                (S \<inter> {x. a \<bullet> x = b} \<noteq> S \<longrightarrow> (\<forall>w \<in> affine hull S. w + c \<in> affine hull S))"
lp15@66652
   824
    proof (cases "affine hull S \<inter> {x. -a \<bullet> x \<le> -b} = {} \<or> affine hull S \<subseteq> {x. - a \<bullet> x \<le> - b}")
lp15@66652
   825
      case True
lp15@66652
   826
      then show ?thesis
lp15@66652
   827
      proof
lp15@66652
   828
        assume "affine hull S \<inter> {x. - a \<bullet> x \<le> - b} = {}"
lp15@66652
   829
       then show ?thesis
lp15@66652
   830
         apply (rule_tac x="0" in exI)
lp15@66652
   831
         apply (rule_tac x="1" in exI)
lp15@66652
   832
         using hull_subset by fastforce
lp15@66652
   833
    next
lp15@66652
   834
      assume "affine hull S \<subseteq> {x. - a \<bullet> x \<le> - b}"
lp15@66652
   835
      then show ?thesis
lp15@66652
   836
         apply (rule_tac x="0" in exI)
lp15@66652
   837
         apply (rule_tac x="0" in exI)
lp15@66652
   838
        using Ssub hull_subset by fastforce
lp15@66652
   839
    qed
lp15@66652
   840
  next
lp15@66652
   841
    case False
lp15@66652
   842
    then obtain a' b' where "a' \<noteq> 0" 
lp15@66652
   843
      and le: "affine hull S \<inter> {x. a' \<bullet> x \<le> b'} = affine hull S \<inter> {x. - a \<bullet> x \<le> - b}" 
lp15@66652
   844
      and eq: "affine hull S \<inter> {x. a' \<bullet> x = b'} = affine hull S \<inter> {x. - a \<bullet> x = - b}" 
lp15@66652
   845
      and mem: "\<And>w. w \<in> affine hull S \<Longrightarrow> w + a' \<in> affine hull S"
lp15@66652
   846
      using affine_parallel_slice affine_affine_hull by metis 
lp15@66652
   847
    show ?thesis
lp15@66652
   848
    proof (intro conjI impI allI ballI exI)
nipkow@69508
   849
      have *: "S \<subseteq> - (affine hull S \<inter> {x. P x}) \<union> affine hull S \<inter> {x. Q x} \<Longrightarrow> S \<subseteq> {x. \<not> P x \<or> Q x}" 
lp15@66652
   850
        for P Q 
lp15@66652
   851
        using hull_subset by fastforce  
nipkow@69508
   852
      have "S \<subseteq> {x. \<not> (a' \<bullet> x \<le> b') \<or> a' \<bullet> x = b'}"
lp15@66652
   853
        apply (rule *)
lp15@66652
   854
        apply (simp only: le eq)
lp15@66652
   855
        using Ssub by auto
lp15@66652
   856
      then show "S \<subseteq> {x. - a' \<bullet> x \<le> - b'}"
lp15@66652
   857
        by auto 
lp15@66652
   858
      show "S \<inter> {x. a \<bullet> x = b} = S \<inter> {x. - a' \<bullet> x = - b'}"
lp15@66652
   859
        using eq hull_subset [of S affine] by force
lp15@66652
   860
      show "\<lbrakk>S \<inter> {x. a \<bullet> x = b} \<noteq> {}; S \<inter> {x. a \<bullet> x = b} \<noteq> S\<rbrakk> \<Longrightarrow> - a' \<noteq> 0"
lp15@66652
   861
        using \<open>a' \<noteq> 0\<close> by auto
lp15@66652
   862
      show "w + - a' \<in> affine hull S"
lp15@66652
   863
        if "S \<inter> {x. a \<bullet> x = b} \<noteq> S" "w \<in> affine hull S" for w
lp15@66652
   864
      proof -
lp15@66652
   865
        have "w + 1 *\<^sub>R (w - (w + a')) \<in> affine hull S"
lp15@66652
   866
          using affine_affine_hull mem mem_affine_3_minus that(2) by blast
lp15@66652
   867
        then show ?thesis  by simp
lp15@66652
   868
      qed
lp15@66652
   869
    qed
lp15@66652
   870
  qed
lp15@66652
   871
qed
lp15@66652
   872
next
lp15@66652
   873
  assume ?rhs then show ?lhs
lp15@66652
   874
    unfolding exposed_face_of_def by blast
lp15@66652
   875
qed
lp15@66652
   876
immler@69683
   877
subsection\<open>Extreme points of a set: its singleton faces\<close>
ak2110@68833
   878
ak2110@68833
   879
definition%important extreme_point_of :: "['a::real_vector, 'a set] \<Rightarrow> bool"
lp15@63078
   880
                               (infixr "(extreme'_point'_of)" 50)
lp15@63078
   881
  where "x extreme_point_of S \<longleftrightarrow>
lp15@63078
   882
         x \<in> S \<and> (\<forall>a \<in> S. \<forall>b \<in> S. x \<notin> open_segment a b)"
lp15@63078
   883
ak2110@69730
   884
lemma extreme_point_of_stillconvex:
lp15@63078
   885
   "convex S \<Longrightarrow> (x extreme_point_of S \<longleftrightarrow> x \<in> S \<and> convex(S - {x}))"
lp15@63078
   886
  by (fastforce simp add: convex_contains_segment extreme_point_of_def open_segment_def)
lp15@63078
   887
ak2110@69730
   888
lemma face_of_singleton:
lp15@63078
   889
   "{x} face_of S \<longleftrightarrow> x extreme_point_of S"
lp15@63078
   890
by (fastforce simp add: extreme_point_of_def face_of_def)
lp15@63078
   891
ak2110@69730
   892
lemma extreme_point_not_in_REL_INTERIOR:
lp15@63078
   893
    fixes S :: "'a::real_normed_vector set"
lp15@63078
   894
    shows "\<lbrakk>x extreme_point_of S; S \<noteq> {x}\<rbrakk> \<Longrightarrow> x \<notin> rel_interior S"
lp15@63078
   895
apply (simp add: face_of_singleton [symmetric])
lp15@63078
   896
apply (blast dest: face_of_disjoint_rel_interior)
lp15@63078
   897
done
lp15@63078
   898
ak2110@69730
   899
lemma extreme_point_not_in_interior:
lp15@63078
   900
    fixes S :: "'a::{real_normed_vector, perfect_space} set"
lp15@63078
   901
    shows "x extreme_point_of S \<Longrightarrow> x \<notin> interior S"
lp15@63078
   902
apply (case_tac "S = {x}")
lp15@63078
   903
apply (simp add: empty_interior_finite)
lp15@63078
   904
by (meson contra_subsetD extreme_point_not_in_REL_INTERIOR interior_subset_rel_interior)
lp15@63078
   905
ak2110@69730
   906
lemma extreme_point_of_face:
lp15@63078
   907
     "F face_of S \<Longrightarrow> v extreme_point_of F \<longleftrightarrow> v extreme_point_of S \<and> v \<in> F"
lp15@63078
   908
  by (meson empty_subsetI face_of_face face_of_singleton insert_subset)
lp15@63078
   909
ak2110@69730
   910
lemma extreme_point_of_convex_hull:
lp15@63078
   911
   "x extreme_point_of (convex hull S) \<Longrightarrow> x \<in> S"
lp15@63078
   912
apply (simp add: extreme_point_of_stillconvex)
lp15@63078
   913
using hull_minimal [of S "(convex hull S) - {x}" convex]
lp15@63078
   914
using hull_subset [of S convex]
lp15@63078
   915
apply blast
lp15@63078
   916
done
lp15@63078
   917
ak2110@69730
   918
proposition extreme_points_of_convex_hull:
lp15@63078
   919
   "{x. x extreme_point_of (convex hull S)} \<subseteq> S"
ak2110@69730
   920
  using extreme_point_of_convex_hull by auto
ak2110@69730
   921
ak2110@69730
   922
lemma extreme_point_of_empty [simp]: "\<not> (x extreme_point_of {})"
lp15@63078
   923
  by (simp add: extreme_point_of_def)
lp15@63078
   924
ak2110@69730
   925
lemma extreme_point_of_singleton [iff]: "x extreme_point_of {a} \<longleftrightarrow> x = a"
lp15@63078
   926
  using extreme_point_of_stillconvex by auto
lp15@63078
   927
ak2110@69730
   928
lemma extreme_point_of_translation_eq:
lp15@63078
   929
   "(a + x) extreme_point_of (image (\<lambda>x. a + x) S) \<longleftrightarrow> x extreme_point_of S"
lp15@63078
   930
by (auto simp: extreme_point_of_def)
lp15@63078
   931
ak2110@69730
   932
lemma extreme_points_of_translation:
lp15@63078
   933
   "{x. x extreme_point_of (image (\<lambda>x. a + x) S)} =
lp15@63078
   934
    (\<lambda>x. a + x) ` {x. x extreme_point_of S}"
ak2110@69730
   935
  using extreme_point_of_translation_eq
ak2110@69730
   936
  by auto (metis (no_types, lifting) image_iff mem_Collect_eq minus_add_cancel)
ak2110@69730
   937
ak2110@69730
   938
lemma extreme_points_of_translation_subtract:
haftmann@69661
   939
   "{x. x extreme_point_of (image (\<lambda>x. x - a) S)} =
haftmann@69661
   940
    (\<lambda>x. x - a) ` {x. x extreme_point_of S}"
ak2110@69730
   941
  using extreme_points_of_translation [of "- a" S]
ak2110@69730
   942
  by simp
ak2110@69730
   943
ak2110@69730
   944
lemma extreme_point_of_Int:
lp15@63078
   945
   "\<lbrakk>x extreme_point_of S; x extreme_point_of T\<rbrakk> \<Longrightarrow> x extreme_point_of (S \<inter> T)"
lp15@63078
   946
by (simp add: extreme_point_of_def)
lp15@63078
   947
ak2110@69730
   948
lemma extreme_point_of_Int_supporting_hyperplane_le:
lp15@63078
   949
   "\<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"
lp15@63078
   950
apply (simp add: face_of_singleton [symmetric])
lp15@63078
   951
by (metis face_of_Int_supporting_hyperplane_le_strong convex_singleton)
lp15@63078
   952
ak2110@69730
   953
lemma extreme_point_of_Int_supporting_hyperplane_ge:
lp15@63078
   954
   "\<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"
lp15@63078
   955
apply (simp add: face_of_singleton [symmetric])
lp15@63078
   956
by (metis face_of_Int_supporting_hyperplane_ge_strong convex_singleton)
lp15@63078
   957
ak2110@69730
   958
lemma exposed_point_of_Int_supporting_hyperplane_le:
lp15@63078
   959
   "\<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"
lp15@63078
   960
apply (simp add: exposed_face_of_def face_of_singleton)
lp15@63078
   961
apply (force simp: extreme_point_of_Int_supporting_hyperplane_le)
lp15@63078
   962
done
lp15@63078
   963
ak2110@69730
   964
lemma exposed_point_of_Int_supporting_hyperplane_ge:
lp15@63078
   965
    "\<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"
lp15@63078
   966
using exposed_point_of_Int_supporting_hyperplane_le [of S "-a" "-b" c]
lp15@63078
   967
by simp
lp15@63078
   968
ak2110@69730
   969
lemma extreme_point_of_convex_hull_insert:
lp15@63078
   970
   "\<lbrakk>finite S; a \<notin> convex hull S\<rbrakk> \<Longrightarrow> a extreme_point_of (convex hull (insert a S))"
lp15@63078
   971
apply (case_tac "a \<in> S")
lp15@63078
   972
apply (simp add: hull_inc)
lp15@63078
   973
using face_of_convex_hulls [of "insert a S" "{a}"]
lp15@63078
   974
apply (auto simp: face_of_singleton hull_same)
lp15@63078
   975
done
lp15@63078
   976
immler@69683
   977
subsection\<open>Facets\<close>
ak2110@68833
   978
ak2110@68833
   979
definition%important facet_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"
lp15@63078
   980
                    (infixr "(facet'_of)" 50)
lp15@63078
   981
  where "F facet_of S \<longleftrightarrow> F face_of S \<and> F \<noteq> {} \<and> aff_dim F = aff_dim S - 1"
lp15@63078
   982
ak2110@69730
   983
lemma facet_of_empty [simp]: "\<not> S facet_of {}"
lp15@63078
   984
  by (simp add: facet_of_def)
lp15@63078
   985
ak2110@69730
   986
lemma facet_of_irrefl [simp]: "\<not> S facet_of S "
lp15@63078
   987
  by (simp add: facet_of_def)
lp15@63078
   988
ak2110@69730
   989
lemma facet_of_imp_face_of: "F facet_of S \<Longrightarrow> F face_of S"
lp15@63078
   990
  by (simp add: facet_of_def)
lp15@63078
   991
ak2110@69730
   992
lemma facet_of_imp_subset: "F facet_of S \<Longrightarrow> F \<subseteq> S"
lp15@63078
   993
  by (simp add: face_of_imp_subset facet_of_def)
lp15@63078
   994
ak2110@69730
   995
lemma hyperplane_facet_of_halfspace_le:
lp15@63078
   996
   "a \<noteq> 0 \<Longrightarrow> {x. a \<bullet> x = b} facet_of {x. a \<bullet> x \<le> b}"
lp15@63078
   997
unfolding facet_of_def hyperplane_eq_empty
lp15@63078
   998
by (auto simp: hyperplane_face_of_halfspace_ge hyperplane_face_of_halfspace_le
lp15@63078
   999
           DIM_positive Suc_leI of_nat_diff aff_dim_halfspace_le)
lp15@63078
  1000
ak2110@69730
  1001
lemma hyperplane_facet_of_halfspace_ge:
lp15@63078
  1002
    "a \<noteq> 0 \<Longrightarrow> {x. a \<bullet> x = b} facet_of {x. a \<bullet> x \<ge> b}"
lp15@63078
  1003
unfolding facet_of_def hyperplane_eq_empty
lp15@63078
  1004
by (auto simp: hyperplane_face_of_halfspace_le hyperplane_face_of_halfspace_ge
lp15@63078
  1005
           DIM_positive Suc_leI of_nat_diff aff_dim_halfspace_ge)
lp15@63078
  1006
ak2110@69730
  1007
lemma facet_of_halfspace_le:
lp15@63078
  1008
    "F facet_of {x. a \<bullet> x \<le> b} \<longleftrightarrow> a \<noteq> 0 \<and> F = {x. a \<bullet> x = b}"
lp15@63078
  1009
    (is "?lhs = ?rhs")
ak2110@69730
  1010
proof
lp15@63078
  1011
  assume c: ?lhs
lp15@63078
  1012
  with c facet_of_irrefl show ?rhs
lp15@63078
  1013
    by (force simp: aff_dim_halfspace_le facet_of_def face_of_halfspace_le cong: conj_cong split: if_split_asm)
lp15@63078
  1014
next
lp15@63078
  1015
  assume ?rhs then show ?lhs
lp15@63078
  1016
    by (simp add: hyperplane_facet_of_halfspace_le)
lp15@63078
  1017
qed
lp15@63078
  1018
ak2110@69730
  1019
lemma facet_of_halfspace_ge:
lp15@63078
  1020
    "F facet_of {x. a \<bullet> x \<ge> b} \<longleftrightarrow> a \<noteq> 0 \<and> F = {x. a \<bullet> x = b}"
lp15@63078
  1021
using facet_of_halfspace_le [of F "-a" "-b"] by simp
lp15@63078
  1022
ak2110@69730
  1023
subsection \<open>Edges: faces of affine dimension 1\<close> (*FIXME too small subsection, rearrange? *)
ak2110@68833
  1024
ak2110@68833
  1025
definition%important edge_of :: "['a::euclidean_space set, 'a set] \<Rightarrow> bool"  (infixr "(edge'_of)" 50)
lp15@63078
  1026
  where "e edge_of S \<longleftrightarrow> e face_of S \<and> aff_dim e = 1"
lp15@63078
  1027
ak2110@69730
  1028
lemma edge_of_imp_subset:
lp15@63078
  1029
   "S edge_of T \<Longrightarrow> S \<subseteq> T"
lp15@63078
  1030
by (simp add: edge_of_def face_of_imp_subset)
lp15@63078
  1031
immler@69683
  1032
subsection\<open>Existence of extreme points\<close>
ak2110@68833
  1033
ak2110@69730
  1034
proposition different_norm_3_collinear_points:
lp15@63078
  1035
  fixes a :: "'a::euclidean_space"
lp15@63078
  1036
  assumes "x \<in> open_segment a b" "norm(a) = norm(b)" "norm(x) = norm(b)"
lp15@63078
  1037
  shows False
ak2110@69730
  1038
proof -
lp15@63078
  1039
  obtain u where "norm ((1 - u) *\<^sub>R a + u *\<^sub>R b) = norm b"
lp15@63078
  1040
             and "a \<noteq> b"
lp15@63078
  1041
             and u01: "0 < u" "u < 1"
lp15@63078
  1042
    using assms by (auto simp: open_segment_image_interval if_splits)
lp15@63078
  1043
  then have "(1 - u) *\<^sub>R a \<bullet> (1 - u) *\<^sub>R a + ((1 - u) * 2) *\<^sub>R a \<bullet> u *\<^sub>R b =
lp15@63078
  1044
             (1 - u * u) *\<^sub>R (a \<bullet> a)"
lp15@63078
  1045
    using assms by (simp add: norm_eq algebra_simps inner_commute)
lp15@63078
  1046
  then have "(1 - u) *\<^sub>R ((1 - u) *\<^sub>R a \<bullet> a + (2 * u) *\<^sub>R  a \<bullet> b) =
lp15@63078
  1047
             (1 - u) *\<^sub>R ((1 + u) *\<^sub>R (a \<bullet> a))"
lp15@63078
  1048
    by (simp add: algebra_simps)
lp15@63078
  1049
  then have "(1 - u) *\<^sub>R (a \<bullet> a) + (2 * u) *\<^sub>R (a \<bullet> b) = (1 + u) *\<^sub>R (a \<bullet> a)"
lp15@63078
  1050
    using u01 by auto
lp15@63078
  1051
  then have "a \<bullet> b = a \<bullet> a"
lp15@63078
  1052
    using u01 by (simp add: algebra_simps)
lp15@63078
  1053
  then have "a = b"
lp15@63078
  1054
    using \<open>norm(a) = norm(b)\<close> norm_eq vector_eq by fastforce
lp15@63078
  1055
  then show ?thesis
lp15@63078
  1056
    using \<open>a \<noteq> b\<close> by force
lp15@63078
  1057
qed
lp15@63078
  1058
ak2110@69730
  1059
proposition extreme_point_exists_convex:
lp15@63078
  1060
  fixes S :: "'a::euclidean_space set"
lp15@63078
  1061
  assumes "compact S" "convex S" "S \<noteq> {}"
lp15@63078
  1062
  obtains x where "x extreme_point_of S"
ak2110@69730
  1063
proof -
lp15@63078
  1064
  obtain x where "x \<in> S" and xsup: "\<And>y. y \<in> S \<Longrightarrow> norm y \<le> norm x"
lp15@63078
  1065
    using distance_attains_sup [of S 0] assms by auto
lp15@63078
  1066
  have False if "a \<in> S" "b \<in> S" and x: "x \<in> open_segment a b" for a b
lp15@63078
  1067
  proof -
lp15@63078
  1068
    have noax: "norm a \<le> norm x" and nobx: "norm b \<le> norm x" using xsup that by auto
lp15@63078
  1069
    have "a \<noteq> b"
lp15@63078
  1070
      using empty_iff open_segment_idem x by auto
lp15@63078
  1071
    have *: "(1 - u) * na + u * nb < norm x" if "na < norm x"  "nb \<le> norm x" "0 < u" "u < 1" for na nb u
lp15@63078
  1072
    proof -
lp15@63078
  1073
      have "(1 - u) * na + u * nb < (1 - u) * norm x + u * nb"
lp15@63078
  1074
        by (simp add: that)
lp15@63078
  1075
      also have "... \<le> (1 - u) * norm x + u * norm x"
lp15@63078
  1076
        by (simp add: that)
lp15@63078
  1077
      finally have "(1 - u) * na + u * nb < (1 - u) * norm x + u * norm x" .
lp15@63078
  1078
      then show ?thesis
lp15@63078
  1079
      using scaleR_collapse [symmetric, of "norm x" u] by auto
lp15@63078
  1080
    qed
lp15@63078
  1081
    have "norm x < norm x" if "norm a < norm x"
lp15@63078
  1082
      using x
lp15@63078
  1083
      apply (clarsimp simp only: open_segment_image_interval \<open>a \<noteq> b\<close> if_False)
lp15@63078
  1084
      apply (rule norm_triangle_lt)
lp15@63078
  1085
      apply (simp add: norm_mult)
lp15@63078
  1086
      using * [of "norm a" "norm b"] nobx that
lp15@63078
  1087
        apply blast
lp15@63078
  1088
      done
lp15@63078
  1089
    moreover have "norm x < norm x" if "norm b < norm x"
lp15@63078
  1090
      using x
lp15@63078
  1091
      apply (clarsimp simp only: open_segment_image_interval \<open>a \<noteq> b\<close> if_False)
lp15@63078
  1092
      apply (rule norm_triangle_lt)
lp15@63078
  1093
      apply (simp add: norm_mult)
lp15@63078
  1094
      using * [of "norm b" "norm a" "1-u" for u] noax that
lp15@63078
  1095
        apply (simp add: add.commute)
lp15@63078
  1096
      done
nipkow@69508
  1097
    ultimately have "\<not> (norm a < norm x) \<and> \<not> (norm b < norm x)"
lp15@63078
  1098
      by auto
lp15@63078
  1099
    then show ?thesis
lp15@63078
  1100
      using different_norm_3_collinear_points noax nobx that(3) by fastforce
lp15@63078
  1101
  qed
lp15@63078
  1102
  then show ?thesis
lp15@63078
  1103
    apply (rule_tac x=x in that)
lp15@63078
  1104
    apply (force simp: extreme_point_of_def \<open>x \<in> S\<close>)
lp15@63078
  1105
    done
lp15@63078
  1106
qed
lp15@63078
  1107
immler@69683
  1108
subsection\<open>Krein-Milman, the weaker form\<close>
ak2110@68833
  1109
ak2110@69730
  1110
proposition Krein_Milman:
lp15@63078
  1111
  fixes S :: "'a::euclidean_space set"
lp15@63078
  1112
  assumes "compact S" "convex S"
lp15@63078
  1113
    shows "S = closure(convex hull {x. x extreme_point_of S})"
ak2110@69730
  1114
proof (cases "S = {}")
lp15@63078
  1115
  case True then show ?thesis   by simp
lp15@63078
  1116
next
lp15@63078
  1117
  case False
lp15@63078
  1118
  have "closed S"
lp15@63078
  1119
    by (simp add: \<open>compact S\<close> compact_imp_closed)
lp15@63078
  1120
  have "closure (convex hull {x. x extreme_point_of S}) \<subseteq> S"
lp15@63078
  1121
    apply (rule closure_minimal [OF hull_minimal \<open>closed S\<close>])
lp15@63078
  1122
    using assms
lp15@63078
  1123
    apply (auto simp: extreme_point_of_def)
lp15@63078
  1124
    done
lp15@63078
  1125
  moreover have "u \<in> closure (convex hull {x. x extreme_point_of S})"
lp15@63078
  1126
                if "u \<in> S" for u
lp15@63078
  1127
  proof (rule ccontr)
lp15@63078
  1128
    assume unot: "u \<notin> closure(convex hull {x. x extreme_point_of S})"
lp15@63078
  1129
    then obtain a b where "a \<bullet> u < b"
lp15@63078
  1130
          and ab: "\<And>x. x \<in> closure(convex hull {x. x extreme_point_of S}) \<Longrightarrow> b < a \<bullet> x"
lp15@63078
  1131
      using separating_hyperplane_closed_point [of "closure(convex hull {x. x extreme_point_of S})"]
lp15@63078
  1132
      by blast
nipkow@67399
  1133
    have "continuous_on S ((\<bullet>) a)"
lp15@63078
  1134
      by (rule continuous_intros)+
lp15@63078
  1135
    then obtain m where "m \<in> S" and m: "\<And>y. y \<in> S \<Longrightarrow> a \<bullet> m \<le> a \<bullet> y"
lp15@63078
  1136
      using continuous_attains_inf [of S "\<lambda>x. a \<bullet> x"] \<open>compact S\<close> \<open>u \<in> S\<close>
lp15@63078
  1137
      by auto
wenzelm@63148
  1138
    define T where "T = S \<inter> {x. a \<bullet> x = a \<bullet> m}"
lp15@63078
  1139
    have "m \<in> T"
lp15@63078
  1140
      by (simp add: T_def \<open>m \<in> S\<close>)
lp15@63078
  1141
    moreover have "compact T"
lp15@63078
  1142
      by (simp add: T_def compact_Int_closed [OF \<open>compact S\<close> closed_hyperplane])
lp15@63078
  1143
    moreover have "convex T"
lp15@63078
  1144
      by (simp add: T_def convex_Int [OF \<open>convex S\<close> convex_hyperplane])
lp15@63078
  1145
    ultimately obtain v where v: "v extreme_point_of T"
lp15@63078
  1146
      using extreme_point_exists_convex [of T] by auto
lp15@63078
  1147
    then have "{v} face_of T"
lp15@63078
  1148
      by (simp add: face_of_singleton)
lp15@63078
  1149
    also have "T face_of S"
lp15@63078
  1150
      by (simp add: T_def m face_of_Int_supporting_hyperplane_ge [OF \<open>convex S\<close>])
lp15@63078
  1151
    finally have "v extreme_point_of S"
lp15@63078
  1152
      by (simp add: face_of_singleton)
lp15@63078
  1153
    then have "b < a \<bullet> v"
lp15@63078
  1154
      using closure_subset by (simp add: closure_hull hull_inc ab)
lp15@63078
  1155
    then show False
lp15@63078
  1156
      using \<open>a \<bullet> u < b\<close> \<open>{v} face_of T\<close> face_of_imp_subset m T_def that by fastforce
lp15@63078
  1157
  qed
lp15@63078
  1158
  ultimately show ?thesis
lp15@63078
  1159
    by blast
lp15@63078
  1160
qed
lp15@63078
  1161
lp15@63078
  1162
text\<open>Now the sharper form.\<close>
lp15@63078
  1163
ak2110@69730
  1164
lemma Krein_Milman_Minkowski_aux:
lp15@63078
  1165
  fixes S :: "'a::euclidean_space set"
lp15@63078
  1166
  assumes n: "dim S = n" and S: "compact S" "convex S" "0 \<in> S"
lp15@63078
  1167
    shows "0 \<in> convex hull {x. x extreme_point_of S}"
lp15@63078
  1168
using n S
ak2110@69730
  1169
proof (induction n arbitrary: S rule: less_induct)
lp15@63078
  1170
  case (less n S) show ?case
lp15@63078
  1171
  proof (cases "0 \<in> rel_interior S")
lp15@63078
  1172
    case True with Krein_Milman show ?thesis
lp15@63078
  1173
      by (metis subsetD convex_convex_hull convex_rel_interior_closure less.prems(2) less.prems(3) rel_interior_subset)
lp15@63078
  1174
  next
lp15@63078
  1175
    case False
lp15@63078
  1176
    have "rel_interior S \<noteq> {}"
lp15@63078
  1177
      by (simp add: rel_interior_convex_nonempty_aux less)
lp15@63078
  1178
    then obtain c where c: "c \<in> rel_interior S" by blast
lp15@63078
  1179
    obtain a where "a \<noteq> 0"
lp15@63078
  1180
              and le_ay: "\<And>y. y \<in> S \<Longrightarrow> a \<bullet> 0 \<le> a \<bullet> y"
lp15@63078
  1181
              and less_ay: "\<And>y. y \<in> rel_interior S \<Longrightarrow> a \<bullet> 0 < a \<bullet> y"
lp15@63078
  1182
      by (blast intro: supporting_hyperplane_rel_boundary intro!: less False)
lp15@63078
  1183
    have face: "S \<inter> {x. a \<bullet> x = 0} face_of S"
lp15@63078
  1184
      apply (rule face_of_Int_supporting_hyperplane_ge [OF \<open>convex S\<close>])
lp15@63078
  1185
      using le_ay by auto
lp15@63078
  1186
    then have co: "compact (S \<inter> {x. a \<bullet> x = 0})" "convex (S \<inter> {x. a \<bullet> x = 0})"
lp15@63078
  1187
      using less.prems by (blast intro: face_of_imp_compact face_of_imp_convex)+
lp15@63078
  1188
    have "a \<bullet> y = 0" if "y \<in> span (S \<inter> {x. a \<bullet> x = 0})" for y
lp15@63078
  1189
    proof -
lp15@63078
  1190
      have "y \<in> span {x. a \<bullet> x = 0}"
lp15@63078
  1191
        by (metis inf.cobounded2 span_mono subsetCE that)
lp15@63469
  1192
      then show ?thesis
lp15@63469
  1193
        by (blast intro: span_induct [OF _ subspace_hyperplane])
lp15@63078
  1194
    qed
lp15@63078
  1195
    then have "dim (S \<inter> {x. a \<bullet> x = 0}) < n"
lp15@63078
  1196
      by (metis (no_types) less_ay c subsetD dim_eq_span inf.strict_order_iff
immler@68074
  1197
           inf_le1 \<open>dim S = n\<close> not_le rel_interior_subset span_0 span_base)
lp15@63078
  1198
    then have "0 \<in> convex hull {x. x extreme_point_of (S \<inter> {x. a \<bullet> x = 0})}"
lp15@63078
  1199
      by (rule less.IH) (auto simp: co less.prems)
lp15@63078
  1200
    then show ?thesis
lp15@63078
  1201
      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)
lp15@63078
  1202
  qed
lp15@63078
  1203
qed
lp15@63078
  1204
lp15@63078
  1205
ak2110@69730
  1206
theorem Krein_Milman_Minkowski:
lp15@63078
  1207
  fixes S :: "'a::euclidean_space set"
lp15@63078
  1208
  assumes "compact S" "convex S"
lp15@63078
  1209
    shows "S = convex hull {x. x extreme_point_of S}"
ak2110@69730
  1210
proof
lp15@63078
  1211
  show "S \<subseteq> convex hull {x. x extreme_point_of S}"
lp15@63078
  1212
  proof
lp15@63078
  1213
    fix a assume [simp]: "a \<in> S"
nipkow@67399
  1214
    have 1: "compact ((+) (- a) ` S)"
haftmann@69661
  1215
      by (simp add: \<open>compact S\<close> compact_translation_subtract cong: image_cong_simp)
nipkow@67399
  1216
    have 2: "convex ((+) (- a) ` S)"
haftmann@69661
  1217
      by (simp add: \<open>convex S\<close> compact_translation_subtract)
lp15@63078
  1218
    show a_invex: "a \<in> convex hull {x. x extreme_point_of S}"
lp15@63078
  1219
      using Krein_Milman_Minkowski_aux [OF refl 1 2]
lp15@63078
  1220
            convex_hull_translation [of "-a"]
haftmann@69661
  1221
      by (auto simp: extreme_points_of_translation_subtract translation_assoc cong: image_cong_simp)
lp15@63078
  1222
    qed
lp15@63078
  1223
next
lp15@63078
  1224
  show "convex hull {x. x extreme_point_of S} \<subseteq> S"
lp15@63078
  1225
  proof -
lp15@63078
  1226
    have "{a. a extreme_point_of S} \<subseteq> S"
lp15@63078
  1227
      using extreme_point_of_def by blast
lp15@63078
  1228
    then show ?thesis
lp15@63078
  1229
      by (simp add: \<open>convex S\<close> hull_minimal)
lp15@63078
  1230
  qed
lp15@63078
  1231
qed
lp15@63078
  1232
lp15@63078
  1233
immler@69683
  1234
subsection\<open>Applying it to convex hulls of explicitly indicated finite sets\<close>
ak2110@68833
  1235
ak2110@69730
  1236
corollary Krein_Milman_polytope:
lp15@63078
  1237
  fixes S :: "'a::euclidean_space set"
lp15@63078
  1238
  shows
lp15@63078
  1239
   "finite S
lp15@63078
  1240
       \<Longrightarrow> convex hull S =
lp15@63078
  1241
           convex hull {x. x extreme_point_of (convex hull S)}"
ak2110@69730
  1242
  by (simp add: Krein_Milman_Minkowski finite_imp_compact_convex_hull)
ak2110@69730
  1243
ak2110@69730
  1244
lemma extreme_points_of_convex_hull_eq:
lp15@63078
  1245
  fixes S :: "'a::euclidean_space set"
lp15@63078
  1246
  shows
lp15@63078
  1247
   "\<lbrakk>compact S; \<And>T. T \<subset> S \<Longrightarrow> convex hull T \<noteq> convex hull S\<rbrakk>
lp15@63078
  1248
        \<Longrightarrow> {x. x extreme_point_of (convex hull S)} = S"
lp15@63078
  1249
by (metis (full_types) Krein_Milman_Minkowski compact_convex_hull convex_convex_hull extreme_points_of_convex_hull psubsetI)
lp15@63078
  1250
lp15@63078
  1251
ak2110@69730
  1252
lemma extreme_point_of_convex_hull_eq:
lp15@63078
  1253
  fixes S :: "'a::euclidean_space set"
lp15@63078
  1254
  shows
lp15@63078
  1255
   "\<lbrakk>compact S; \<And>T. T \<subset> S \<Longrightarrow> convex hull T \<noteq> convex hull S\<rbrakk>
lp15@63078
  1256
    \<Longrightarrow> (x extreme_point_of (convex hull S) \<longleftrightarrow> x \<in> S)"
lp15@63078
  1257
using extreme_points_of_convex_hull_eq by auto
lp15@63078
  1258
ak2110@69730
  1259
lemma extreme_point_of_convex_hull_convex_independent:
lp15@63078
  1260
  fixes S :: "'a::euclidean_space set"
lp15@63078
  1261
  assumes "compact S" and S: "\<And>a. a \<in> S \<Longrightarrow> a \<notin> convex hull (S - {a})"
lp15@63078
  1262
  shows "(x extreme_point_of (convex hull S) \<longleftrightarrow> x \<in> S)"
ak2110@69730
  1263
proof -
lp15@63078
  1264
  have "convex hull T \<noteq> convex hull S" if "T \<subset> S" for T
lp15@63078
  1265
  proof -
lp15@63078
  1266
    obtain a where  "T \<subseteq> S" "a \<in> S" "a \<notin> T" using \<open>T \<subset> S\<close> by blast
lp15@63078
  1267
    then show ?thesis
lp15@63078
  1268
      by (metis (full_types) Diff_eq_empty_iff Diff_insert0 S hull_mono hull_subset insert_Diff_single subsetCE)
lp15@63078
  1269
  qed
lp15@63078
  1270
  then show ?thesis
lp15@63078
  1271
    by (rule extreme_point_of_convex_hull_eq [OF \<open>compact S\<close>])
lp15@63078
  1272
qed
lp15@63078
  1273
ak2110@69730
  1274
lemma extreme_point_of_convex_hull_affine_independent:
lp15@63078
  1275
  fixes S :: "'a::euclidean_space set"
lp15@63078
  1276
  shows
nipkow@69508
  1277
   "\<not> affine_dependent S
lp15@63078
  1278
         \<Longrightarrow> (x extreme_point_of (convex hull S) \<longleftrightarrow> x \<in> S)"
lp15@63078
  1279
by (metis aff_independent_finite affine_dependent_def affine_hull_convex_hull extreme_point_of_convex_hull_convex_independent finite_imp_compact hull_inc)
lp15@63078
  1280
lp15@63078
  1281
text\<open>Elementary proofs exist, not requiring Euclidean spaces and all this development\<close>
ak2110@69730
  1282
lemma extreme_point_of_convex_hull_2:
lp15@63078
  1283
  fixes x :: "'a::euclidean_space"
lp15@63078
  1284
  shows "x extreme_point_of (convex hull {a,b}) \<longleftrightarrow> x = a \<or> x = b"
lp15@63078
  1285
proof -
lp15@63078
  1286
  have "x extreme_point_of (convex hull {a,b}) \<longleftrightarrow> x \<in> {a,b}"
lp15@63078
  1287
    by (intro extreme_point_of_convex_hull_affine_independent affine_independent_2)
lp15@63078
  1288
  then show ?thesis
lp15@63078
  1289
    by simp
lp15@63078
  1290
qed
lp15@63078
  1291
ak2110@69730
  1292
lemma extreme_point_of_segment:
lp15@63078
  1293
  fixes x :: "'a::euclidean_space"
lp15@63078
  1294
  shows
lp15@63078
  1295
   "x extreme_point_of closed_segment a b \<longleftrightarrow> x = a \<or> x = b"
lp15@63078
  1296
by (simp add: extreme_point_of_convex_hull_2 segment_convex_hull)
lp15@63078
  1297
ak2110@69730
  1298
lemma face_of_convex_hull_subset:
lp15@63078
  1299
  fixes S :: "'a::euclidean_space set"
lp15@63078
  1300
  assumes "compact S" and T: "T face_of (convex hull S)"
lp15@63078
  1301
  obtains s' where "s' \<subseteq> S" "T = convex hull s'"
lp15@63078
  1302
apply (rule_tac s' = "{x. x extreme_point_of T}" in that)
lp15@63078
  1303
using T extreme_point_of_convex_hull extreme_point_of_face apply blast
lp15@63078
  1304
by (metis (no_types) Krein_Milman_Minkowski assms compact_convex_hull convex_convex_hull face_of_imp_compact face_of_imp_convex)
lp15@63078
  1305
lp15@63078
  1306
ak2110@69730
  1307
lemma face_of_convex_hull_aux:
lp15@66297
  1308
  assumes eq: "x *\<^sub>R p = u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c"
lp15@66297
  1309
    and x: "u + v + w = x" "x \<noteq> 0" and S: "affine S" "a \<in> S" "b \<in> S" "c \<in> S"
lp15@66297
  1310
  shows "p \<in> S"
ak2110@69730
  1311
proof -
lp15@66297
  1312
  have "p = (u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c) /\<^sub>R x"
lp15@66297
  1313
    by (metis \<open>x \<noteq> 0\<close> eq mult.commute right_inverse scaleR_one scaleR_scaleR)
lp15@66297
  1314
  moreover have "affine hull {a,b,c} \<subseteq> S"
lp15@66297
  1315
    by (simp add: S hull_minimal)
lp15@66297
  1316
  moreover have "(u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c) /\<^sub>R x \<in> affine hull {a,b,c}"
lp15@66297
  1317
    apply (simp add: affine_hull_3)
lp15@66297
  1318
    apply (rule_tac x="u/x" in exI)
lp15@66297
  1319
    apply (rule_tac x="v/x" in exI)
lp15@66297
  1320
    apply (rule_tac x="w/x" in exI)
lp15@66297
  1321
    using x apply (auto simp: algebra_simps divide_simps)
lp15@66297
  1322
    done
lp15@66297
  1323
  ultimately show ?thesis by force
lp15@66297
  1324
qed
lp15@66297
  1325
ak2110@69730
  1326
proposition face_of_convex_hull_insert_eq:
lp15@66297
  1327
  fixes a :: "'a :: euclidean_space"
lp15@66297
  1328
  assumes "finite S" and a: "a \<notin> affine hull S"
lp15@66297
  1329
  shows "(F face_of (convex hull (insert a S)) \<longleftrightarrow>
lp15@66297
  1330
          F face_of (convex hull S) \<or>
lp15@66297
  1331
          (\<exists>F'. F' face_of (convex hull S) \<and> F = convex hull (insert a F')))"
lp15@66297
  1332
         (is "F face_of ?CAS \<longleftrightarrow> _")
ak2110@69730
  1333
proof safe
lp15@66297
  1334
  assume F: "F face_of ?CAS"
lp15@66297
  1335
    and *: "\<nexists>F'. F' face_of convex hull S \<and> F = convex hull insert a F'"
lp15@66297
  1336
  obtain T where T: "T \<subseteq> insert a S" and FeqT: "F = convex hull T"
lp15@66297
  1337
    by (metis F \<open>finite S\<close> compact_insert finite_imp_compact face_of_convex_hull_subset)
lp15@66297
  1338
  show "F face_of convex hull S"
lp15@66297
  1339
  proof (cases "a \<in> T")
lp15@66297
  1340
    case True
lp15@66297
  1341
    have "F = convex hull insert a (convex hull T \<inter> convex hull S)"
lp15@66297
  1342
    proof
lp15@66297
  1343
      have "T \<subseteq> insert a (convex hull T \<inter> convex hull S)"
lp15@66297
  1344
        using T hull_subset by fastforce
lp15@66297
  1345
      then show "F \<subseteq> convex hull insert a (convex hull T \<inter> convex hull S)"
lp15@66297
  1346
        by (simp add: FeqT hull_mono)
lp15@66297
  1347
      show "convex hull insert a (convex hull T \<inter> convex hull S) \<subseteq> F"
lp15@66297
  1348
        apply (rule hull_minimal)
lp15@66297
  1349
        using True by (auto simp: \<open>F = convex hull T\<close> hull_inc)
lp15@66297
  1350
    qed
lp15@66297
  1351
    moreover have "convex hull T \<inter> convex hull S face_of convex hull S"
lp15@66297
  1352
      by (metis F FeqT convex_convex_hull face_of_slice hull_mono inf.absorb_iff2 subset_insertI)
lp15@66297
  1353
    ultimately show ?thesis
lp15@66297
  1354
      using * by force
lp15@66297
  1355
  next
lp15@66297
  1356
    case False
lp15@66297
  1357
    then show ?thesis
lp15@66297
  1358
      by (metis FeqT F T face_of_subset hull_mono subset_insert subset_insertI)
lp15@66297
  1359
  qed
lp15@66297
  1360
next
lp15@66297
  1361
  assume "F face_of convex hull S"
lp15@66297
  1362
  show "F face_of ?CAS"
lp15@66297
  1363
    by (simp add: \<open>F face_of convex hull S\<close> a face_of_convex_hull_insert \<open>finite S\<close>)
lp15@66297
  1364
next
lp15@66297
  1365
  fix F
lp15@66297
  1366
  assume F: "F face_of convex hull S"
lp15@66297
  1367
  show "convex hull insert a F face_of ?CAS"
lp15@66297
  1368
  proof (cases "S = {}")
lp15@66297
  1369
    case True
lp15@66297
  1370
    then show ?thesis
lp15@66297
  1371
      using F face_of_affine_eq by auto
lp15@66297
  1372
  next
lp15@66297
  1373
    case False
lp15@66297
  1374
    have anotc: "a \<notin> convex hull S"
lp15@66297
  1375
      by (metis (no_types) a affine_hull_convex_hull hull_inc)
lp15@66297
  1376
    show ?thesis
lp15@66297
  1377
    proof (cases "F = {}")
lp15@66297
  1378
      case True show ?thesis
lp15@66297
  1379
        using anotc by (simp add: \<open>F = {}\<close> \<open>finite S\<close> extreme_point_of_convex_hull_insert face_of_singleton)
lp15@66297
  1380
    next
lp15@66297
  1381
      case False
lp15@66297
  1382
      have "convex hull insert a F \<subseteq> ?CAS"
lp15@66297
  1383
        by (simp add: F a \<open>finite S\<close> convex_hull_subset face_of_convex_hull_insert face_of_imp_subset hull_inc)
lp15@66297
  1384
      moreover
lp15@66297
  1385
      have "(\<exists>y v. (1 - ub) *\<^sub>R a + ub *\<^sub>R b = (1 - v) *\<^sub>R a + v *\<^sub>R y \<and>
lp15@66297
  1386
                   0 \<le> v \<and> v \<le> 1 \<and> y \<in> F) \<and>
lp15@66297
  1387
            (\<exists>x u. (1 - uc) *\<^sub>R a + uc *\<^sub>R c = (1 - u) *\<^sub>R a + u *\<^sub>R x \<and>
lp15@66297
  1388
                   0 \<le> u \<and> u \<le> 1 \<and> x \<in> F)"
lp15@66297
  1389
        if *: "(1 - ux) *\<^sub>R a + ux *\<^sub>R x
lp15@66297
  1390
               \<in> open_segment ((1 - ub) *\<^sub>R a + ub *\<^sub>R b) ((1 - uc) *\<^sub>R a + uc *\<^sub>R c)"
lp15@66297
  1391
          and "0 \<le> ub" "ub \<le> 1" "0 \<le> uc" "uc \<le> 1" "0 \<le> ux" "ux \<le> 1"
lp15@66297
  1392
          and b: "b \<in> convex hull S" and c: "c \<in> convex hull S" and "x \<in> F"
lp15@66297
  1393
        for b c ub uc ux x
lp15@66297
  1394
      proof -
lp15@66297
  1395
        obtain v where ne: "(1 - ub) *\<^sub>R a + ub *\<^sub>R b \<noteq> (1 - uc) *\<^sub>R a + uc *\<^sub>R c"
lp15@66297
  1396
          and eq: "(1 - ux) *\<^sub>R a + ux *\<^sub>R x =
lp15@66297
  1397
                    (1 - v) *\<^sub>R ((1 - ub) *\<^sub>R a + ub *\<^sub>R b) + v *\<^sub>R ((1 - uc) *\<^sub>R a + uc *\<^sub>R c)"
lp15@66297
  1398
          and "0 < v" "v < 1"
lp15@66297
  1399
          using * by (auto simp: in_segment)
lp15@66297
  1400
        then have 0: "((1 - ux) - ((1 - v) * (1 - ub) + v * (1 - uc))) *\<^sub>R a +
lp15@66297
  1401
                      (ux *\<^sub>R x - (((1 - v) * ub) *\<^sub>R b + (v * uc) *\<^sub>R c)) = 0"
lp15@66297
  1402
          by (auto simp: algebra_simps)
lp15@66297
  1403
        then have "((1 - ux) - ((1 - v) * (1 - ub) + v * (1 - uc))) *\<^sub>R a =
lp15@66297
  1404
                   ((1 - v) * ub) *\<^sub>R b + (v * uc) *\<^sub>R c + (-ux) *\<^sub>R x"
lp15@66297
  1405
          by (auto simp: algebra_simps)
lp15@66297
  1406
        then have "a \<in> affine hull S" if "1 - ux - ((1 - v) * (1 - ub) + v * (1 - uc)) \<noteq> 0"
lp15@66297
  1407
          apply (rule face_of_convex_hull_aux)
lp15@66297
  1408
          using b c that apply (auto simp: algebra_simps)
lp15@66297
  1409
          using F convex_hull_subset_affine_hull face_of_imp_subset \<open>x \<in> F\<close> apply blast+
lp15@66297
  1410
          done
lp15@66297
  1411
        then have "1 - ux - ((1 - v) * (1 - ub) + v * (1 - uc)) = 0"
lp15@66297
  1412
          using a by blast
lp15@66297
  1413
        with 0 have equx: "(1 - v) * ub + v * uc = ux"
lp15@66297
  1414
          and uxx: "ux *\<^sub>R x = (((1 - v) * ub) *\<^sub>R b + (v * uc) *\<^sub>R c)"
lp15@66297
  1415
          by auto (auto simp: algebra_simps)
lp15@66297
  1416
        show ?thesis
lp15@66297
  1417
        proof (cases "uc = 0")
lp15@66297
  1418
          case True
lp15@66297
  1419
          then show ?thesis
lp15@66297
  1420
            using equx 0 \<open>0 \<le> ub\<close> \<open>ub \<le> 1\<close> \<open>v < 1\<close> \<open>x \<in> F\<close>
lp15@66297
  1421
            apply (auto simp: algebra_simps)
lp15@66297
  1422
             apply (rule_tac x=x in exI, simp)
lp15@66297
  1423
             apply (rule_tac x=ub in exI, auto)
lp15@66297
  1424
             apply (metis add.left_neutral diff_eq_eq less_irrefl mult.commute mult_cancel_right1 real_vector.scale_cancel_left real_vector.scale_left_diff_distrib)
lp15@66297
  1425
            using \<open>x \<in> F\<close> \<open>uc \<le> 1\<close> apply blast
lp15@66297
  1426
            done
lp15@66297
  1427
        next
lp15@66297
  1428
          case False
lp15@66297
  1429
          show ?thesis
lp15@66297
  1430
          proof (cases "ub = 0")
lp15@66297
  1431
            case True
lp15@66297
  1432
            then show ?thesis
lp15@66297
  1433
              using equx 0 \<open>0 \<le> uc\<close> \<open>uc \<le> 1\<close> \<open>0 < v\<close> \<open>x \<in> F\<close> \<open>uc \<noteq> 0\<close> by (force simp: algebra_simps)
lp15@66297
  1434
          next
lp15@66297
  1435
            case False
lp15@66297
  1436
            then have "0 < ub" "0 < uc"
lp15@66297
  1437
              using \<open>uc \<noteq> 0\<close> \<open>0 \<le> ub\<close> \<open>0 \<le> uc\<close> by auto
lp15@66297
  1438
            then have "ux \<noteq> 0"
lp15@66297
  1439
              by (metis \<open>0 < v\<close> \<open>v < 1\<close> diff_ge_0_iff_ge dual_order.strict_implies_order equx leD le_add_same_cancel2 zero_le_mult_iff zero_less_mult_iff)
lp15@66297
  1440
            have "b \<in> F \<and> c \<in> F"
lp15@66297
  1441
            proof (cases "b = c")
lp15@66297
  1442
              case True
lp15@66297
  1443
              then show ?thesis
lp15@66297
  1444
                by (metis \<open>ux \<noteq> 0\<close> equx real_vector.scale_cancel_left scaleR_add_left uxx \<open>x \<in> F\<close>)
lp15@66297
  1445
            next
lp15@66297
  1446
              case False
lp15@66297
  1447
              have "x = (((1 - v) * ub) *\<^sub>R b + (v * uc) *\<^sub>R c) /\<^sub>R ux"
lp15@66297
  1448
                by (metis \<open>ux \<noteq> 0\<close> uxx mult.commute right_inverse scaleR_one scaleR_scaleR)
lp15@66297
  1449
              also have "... = (1 - v * uc / ux) *\<^sub>R b + (v * uc / ux) *\<^sub>R c"
lp15@66297
  1450
                using \<open>ux \<noteq> 0\<close> equx apply (auto simp: algebra_simps divide_simps)
lp15@66297
  1451
                by (metis add.commute add_diff_eq add_divide_distrib diff_add_cancel scaleR_add_left)
lp15@66297
  1452
              finally have "x = (1 - v * uc / ux) *\<^sub>R b + (v * uc / ux) *\<^sub>R c" .
lp15@66297
  1453
              then have "x \<in> open_segment b c"
lp15@66297
  1454
                apply (simp add: in_segment \<open>b \<noteq> c\<close>)
lp15@66297
  1455
                apply (rule_tac x="(v * uc) / ux" in exI)
lp15@66297
  1456
                using \<open>0 \<le> ux\<close> \<open>ux \<noteq> 0\<close> \<open>0 < uc\<close> \<open>0 < v\<close> \<open>0 < ub\<close> \<open>v < 1\<close> equx
lp15@66297
  1457
                apply (force simp: algebra_simps divide_simps)
lp15@66297
  1458
                done
lp15@66297
  1459
              then show ?thesis
lp15@66297
  1460
                by (rule face_ofD [OF F _ b c \<open>x \<in> F\<close>])
lp15@66297
  1461
            qed
lp15@66297
  1462
            with \<open>0 \<le> ub\<close> \<open>ub \<le> 1\<close> \<open>0 \<le> uc\<close> \<open>uc \<le> 1\<close> show ?thesis by blast
lp15@66297
  1463
          qed
lp15@66297
  1464
        qed
lp15@66297
  1465
      qed
lp15@66297
  1466
      moreover have "convex hull F = F"
lp15@66297
  1467
        by (meson F convex_hull_eq face_of_imp_convex)
lp15@66297
  1468
      ultimately show ?thesis
lp15@66297
  1469
        unfolding face_of_def by (fastforce simp: convex_hull_insert_alt \<open>S \<noteq> {}\<close> \<open>F \<noteq> {}\<close>)
lp15@66297
  1470
    qed
lp15@66297
  1471
  qed
lp15@66297
  1472
qed
lp15@66297
  1473
ak2110@69730
  1474
lemma face_of_convex_hull_insert2:
lp15@66297
  1475
  fixes a :: "'a :: euclidean_space"
lp15@66297
  1476
  assumes S: "finite S" and a: "a \<notin> affine hull S" and F: "F face_of convex hull S"
lp15@66297
  1477
  shows "convex hull (insert a F) face_of convex hull (insert a S)"
lp15@66297
  1478
  by (metis F face_of_convex_hull_insert_eq [OF S a])
lp15@66297
  1479
ak2110@69730
  1480
proposition face_of_convex_hull_affine_independent:
lp15@63078
  1481
  fixes S :: "'a::euclidean_space set"
nipkow@69508
  1482
  assumes "\<not> affine_dependent S"
lp15@63078
  1483
    shows "(T face_of (convex hull S) \<longleftrightarrow> (\<exists>c. c \<subseteq> S \<and> T = convex hull c))"
lp15@63078
  1484
          (is "?lhs = ?rhs")
ak2110@69730
  1485
proof
lp15@63078
  1486
  assume ?lhs
lp15@63078
  1487
  then show ?rhs
lp15@63078
  1488
    by (meson \<open>T face_of convex hull S\<close> aff_independent_finite assms face_of_convex_hull_subset finite_imp_compact)
lp15@63078
  1489
next
lp15@63078
  1490
  assume ?rhs
lp15@63078
  1491
  then obtain c where "c \<subseteq> S" and T: "T = convex hull c"
lp15@63078
  1492
    by blast
lp15@63078
  1493
  have "affine hull c \<inter> affine hull (S - c) = {}"
lp15@63078
  1494
    apply (rule disjoint_affine_hull [OF assms \<open>c \<subseteq> S\<close>], auto)
lp15@63078
  1495
    done
lp15@63078
  1496
  then have "affine hull c \<inter> convex hull (S - c) = {}"
lp15@63078
  1497
    using convex_hull_subset_affine_hull by fastforce
lp15@63078
  1498
  then show ?lhs
lp15@63078
  1499
    by (metis face_of_convex_hulls \<open>c \<subseteq> S\<close> aff_independent_finite assms T)
lp15@63078
  1500
qed
lp15@63078
  1501
ak2110@69730
  1502
lemma facet_of_convex_hull_affine_independent:
lp15@63078
  1503
  fixes S :: "'a::euclidean_space set"
nipkow@69508
  1504
  assumes "\<not> affine_dependent S"
lp15@63078
  1505
    shows "T facet_of (convex hull S) \<longleftrightarrow>
lp15@63078
  1506
           T \<noteq> {} \<and> (\<exists>u. u \<in> S \<and> T = convex hull (S - {u}))"
lp15@63078
  1507
          (is "?lhs = ?rhs")
lp15@63078
  1508
proof
lp15@63078
  1509
  assume ?lhs
lp15@63078
  1510
  then have "T face_of (convex hull S)" "T \<noteq> {}"
lp15@63078
  1511
        and afft: "aff_dim T = aff_dim (convex hull S) - 1"
lp15@63078
  1512
    by (auto simp: facet_of_def)
lp15@63078
  1513
  then obtain c where "c \<subseteq> S" and c: "T = convex hull c"
lp15@63078
  1514
    by (auto simp: face_of_convex_hull_affine_independent [OF assms])
lp15@63078
  1515
  then have affs: "aff_dim S = aff_dim c + 1"
lp15@63078
  1516
    by (metis aff_dim_convex_hull afft eq_diff_eq)
nipkow@69508
  1517
  have "\<not> affine_dependent c"
lp15@63078
  1518
    using \<open>c \<subseteq> S\<close> affine_dependent_subset assms by blast
lp15@63078
  1519
  with affs have "card (S - c) = 1"
lp15@63078
  1520
    apply (simp add: aff_dim_affine_independent [symmetric] aff_dim_convex_hull)
lp15@63078
  1521
    by (metis aff_dim_affine_independent aff_independent_finite One_nat_def \<open>c \<subseteq> S\<close> add.commute
lp15@63078
  1522
                add_diff_cancel_right' assms card_Diff_subset card_mono of_nat_1 of_nat_diff of_nat_eq_iff)
lp15@63078
  1523
  then obtain u where u: "u \<in> S - c"
lp15@63078
  1524
    by (metis DiffI \<open>c \<subseteq> S\<close> aff_independent_finite assms cancel_comm_monoid_add_class.diff_cancel
lp15@63078
  1525
                card_Diff_subset subsetI subset_antisym zero_neq_one)
lp15@63078
  1526
  then have u: "S = insert u c"
lp15@63078
  1527
    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)
lp15@63078
  1528
  have "T = convex hull (c - {u})"
lp15@63078
  1529
    by (metis Diff_empty Diff_insert0 \<open>T facet_of convex hull S\<close> c facet_of_irrefl insert_absorb u)
lp15@63078
  1530
  with \<open>T \<noteq> {}\<close> show ?rhs
lp15@63078
  1531
    using c u by auto
lp15@63078
  1532
next
lp15@63078
  1533
  assume ?rhs
lp15@63078
  1534
  then obtain u where "T \<noteq> {}" "u \<in> S" and u: "T = convex hull (S - {u})"
lp15@63078
  1535
    by (force simp: facet_of_def)
lp15@63078
  1536
  then have "\<not> S \<subseteq> {u}"
lp15@63078
  1537
    using \<open>T \<noteq> {}\<close> u by auto
lp15@63078
  1538
  have [simp]: "aff_dim (convex hull (S - {u})) = aff_dim (convex hull S) - 1"
lp15@63078
  1539
    using assms \<open>u \<in> S\<close>
lp15@63078
  1540
    apply (simp add: aff_dim_convex_hull affine_dependent_def)
lp15@63078
  1541
    apply (drule bspec, assumption)
lp15@63078
  1542
    by (metis add_diff_cancel_right' aff_dim_insert insert_Diff [of u S])
lp15@63078
  1543
  show ?lhs
lp15@63078
  1544
    apply (subst u)
lp15@63078
  1545
    apply (simp add: \<open>\<not> S \<subseteq> {u}\<close> facet_of_def face_of_convex_hull_affine_independent [OF assms], blast)
lp15@63078
  1546
    done
lp15@63078
  1547
qed
lp15@63078
  1548
ak2110@69730
  1549
lemma facet_of_convex_hull_affine_independent_alt:
lp15@63078
  1550
  fixes S :: "'a::euclidean_space set"
lp15@63078
  1551
  shows
nipkow@69508
  1552
   "\<not>affine_dependent S
lp15@63078
  1553
        \<Longrightarrow> (T facet_of (convex hull S) \<longleftrightarrow>
lp15@63078
  1554
             2 \<le> card S \<and> (\<exists>u. u \<in> S \<and> T = convex hull (S - {u})))"
lp15@63078
  1555
apply (simp add: facet_of_convex_hull_affine_independent)
lp15@63078
  1556
apply (auto simp: Set.subset_singleton_iff)
lp15@63078
  1557
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)
lp15@63078
  1558
done
lp15@63078
  1559
ak2110@69730
  1560
lemma segment_face_of:
lp15@63078
  1561
  assumes "(closed_segment a b) face_of S"
lp15@63078
  1562
  shows "a extreme_point_of S" "b extreme_point_of S"
lp15@63078
  1563
proof -
lp15@63078
  1564
  have as: "{a} face_of S"
lp15@63078
  1565
    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)
lp15@63078
  1566
  moreover have "{b} face_of S"
lp15@63078
  1567
  proof -
lp15@63078
  1568
    have "b \<in> convex hull {a} \<or> b extreme_point_of convex hull {b, a}"
lp15@63078
  1569
      by (meson extreme_point_of_convex_hull_insert finite.emptyI finite.insertI)
lp15@63078
  1570
    moreover have "closed_segment a b = convex hull {b, a}"
lp15@63078
  1571
      using closed_segment_commute segment_convex_hull by blast
lp15@63078
  1572
    ultimately show ?thesis
lp15@63078
  1573
      by (metis as assms face_of_face convex_hull_singleton empty_iff face_of_singleton insertE)
lp15@63078
  1574
    qed
lp15@63078
  1575
  ultimately show "a extreme_point_of S" "b extreme_point_of S"
lp15@63078
  1576
    using face_of_singleton by blast+
lp15@63078
  1577
qed
lp15@63078
  1578
lp15@63078
  1579
ak2110@69730
  1580
proposition Krein_Milman_frontier:
lp15@63078
  1581
  fixes S :: "'a::euclidean_space set"
lp15@63078
  1582
  assumes "convex S" "compact S"
lp15@63078
  1583
    shows "S = convex hull (frontier S)"
lp15@63078
  1584
          (is "?lhs = ?rhs")
ak2110@69730
  1585
proof
lp15@63078
  1586
  have "?lhs \<subseteq> convex hull {x. x extreme_point_of S}"
lp15@63078
  1587
    using Krein_Milman_Minkowski assms by blast
lp15@63078
  1588
  also have "... \<subseteq> ?rhs"
lp15@63078
  1589
    apply (rule hull_mono)
lp15@63078
  1590
    apply (auto simp: frontier_def extreme_point_not_in_interior)
lp15@63078
  1591
    using closure_subset apply (force simp: extreme_point_of_def)
lp15@63078
  1592
    done
lp15@63078
  1593
  finally show "?lhs \<subseteq> ?rhs" .
lp15@63078
  1594
next
lp15@63078
  1595
  have "?rhs \<subseteq> convex hull S"
lp15@63078
  1596
    by (metis Diff_subset \<open>compact S\<close> closure_closed compact_eq_bounded_closed frontier_def hull_mono)
lp15@63078
  1597
  also have "... \<subseteq> ?lhs"
lp15@63078
  1598
    by (simp add: \<open>convex S\<close> hull_same)
lp15@63078
  1599
  finally show "?rhs \<subseteq> ?lhs" .
lp15@63078
  1600
qed
lp15@63078
  1601
immler@69683
  1602
subsection\<open>Polytopes\<close>
ak2110@68833
  1603
ak2110@68833
  1604
definition%important polytope where
lp15@63078
  1605
 "polytope S \<equiv> \<exists>v. finite v \<and> S = convex hull v"
lp15@63078
  1606
ak2110@69730
  1607
lemma polytope_translation_eq: "polytope (image (\<lambda>x. a + x) S) \<longleftrightarrow> polytope S"
lp15@63078
  1608
apply (simp add: polytope_def, safe)
lp15@63078
  1609
apply (metis convex_hull_translation finite_imageI translation_galois)
lp15@63078
  1610
by (metis convex_hull_translation finite_imageI)
lp15@63078
  1611
ak2110@69730
  1612
lemma polytope_linear_image: "\<lbrakk>linear f; polytope p\<rbrakk> \<Longrightarrow> polytope(image f p)"
lp15@63078
  1613
  unfolding polytope_def using convex_hull_linear_image by blast
lp15@63078
  1614
ak2110@69730
  1615
lemma polytope_empty: "polytope {}"
lp15@63078
  1616
  using convex_hull_empty polytope_def by blast
lp15@63078
  1617
ak2110@69730
  1618
lemma polytope_convex_hull: "finite S \<Longrightarrow> polytope(convex hull S)"
lp15@63078
  1619
  using polytope_def by auto
lp15@63078
  1620
ak2110@69730
  1621
lemma polytope_Times: "\<lbrakk>polytope S; polytope T\<rbrakk> \<Longrightarrow> polytope(S \<times> T)"
lp15@63078
  1622
  unfolding polytope_def
lp15@63078
  1623
  by (metis finite_cartesian_product convex_hull_Times)
lp15@63078
  1624
ak2110@69730
  1625
lemma face_of_polytope_polytope:
lp15@63078
  1626
  fixes S :: "'a::euclidean_space set"
lp15@63078
  1627
  shows "\<lbrakk>polytope S; F face_of S\<rbrakk> \<Longrightarrow> polytope F"
lp15@63078
  1628
unfolding polytope_def
lp15@63078
  1629
by (meson face_of_convex_hull_subset finite_imp_compact finite_subset)
lp15@63078
  1630
ak2110@69730
  1631
lemma finite_polytope_faces:
lp15@63078
  1632
  fixes S :: "'a::euclidean_space set"
lp15@63078
  1633
  assumes "polytope S"
lp15@63078
  1634
  shows "finite {F. F face_of S}"
lp15@63078
  1635
proof -
lp15@63078
  1636
  obtain v where "finite v" "S = convex hull v"
lp15@63078
  1637
    using assms polytope_def by auto
nipkow@67399
  1638
  have "finite ((hull) convex ` {T. T \<subseteq> v})"
lp15@63078
  1639
    by (simp add: \<open>finite v\<close>)
nipkow@67399
  1640
  moreover have "{F. F face_of S} \<subseteq> ((hull) convex ` {T. T \<subseteq> v})"
lp15@63078
  1641
    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)
lp15@63078
  1642
  ultimately show ?thesis
lp15@63078
  1643
    by (blast intro: finite_subset)
lp15@63078
  1644
qed
lp15@63078
  1645
ak2110@69730
  1646
lemma finite_polytope_facets:
lp15@63078
  1647
  assumes "polytope S"
lp15@63078
  1648
  shows "finite {T. T facet_of S}"
lp15@63078
  1649
by (simp add: assms facet_of_def finite_polytope_faces)
lp15@63078
  1650
ak2110@69730
  1651
lemma polytope_scaling:
lp15@63078
  1652
  assumes "polytope S"  shows "polytope (image (\<lambda>x. c *\<^sub>R x) S)"
lp15@63078
  1653
by (simp add: assms polytope_linear_image)
lp15@63078
  1654
ak2110@69730
  1655
lemma polytope_imp_compact:
lp15@63078
  1656
  fixes S :: "'a::real_normed_vector set"
lp15@63078
  1657
  shows "polytope S \<Longrightarrow> compact S"
lp15@63078
  1658
by (metis finite_imp_compact_convex_hull polytope_def)
lp15@63078
  1659
ak2110@69730
  1660
lemma polytope_imp_convex: "polytope S \<Longrightarrow> convex S"
lp15@63078
  1661
  by (metis convex_convex_hull polytope_def)
lp15@63078
  1662
ak2110@69730
  1663
lemma polytope_imp_closed:
lp15@63078
  1664
  fixes S :: "'a::real_normed_vector set"
lp15@63078
  1665
  shows "polytope S \<Longrightarrow> closed S"
lp15@63078
  1666
by (simp add: compact_imp_closed polytope_imp_compact)
lp15@63078
  1667
ak2110@69730
  1668
lemma polytope_imp_bounded:
lp15@63078
  1669
  fixes S :: "'a::real_normed_vector set"
lp15@63078
  1670
  shows "polytope S \<Longrightarrow> bounded S"
lp15@63078
  1671
by (simp add: compact_imp_bounded polytope_imp_compact)
lp15@63078
  1672
ak2110@69730
  1673
lemma polytope_interval: "polytope(cbox a b)"
lp15@63078
  1674
  unfolding polytope_def by (meson closed_interval_as_convex_hull)
lp15@63078
  1675
ak2110@69730
  1676
lemma polytope_sing: "polytope {a}"
lp15@63078
  1677
  using polytope_def by force
lp15@63078
  1678
ak2110@69730
  1679
lemma face_of_polytope_insert:
lp15@66297
  1680
     "\<lbrakk>polytope S; a \<notin> affine hull S; F face_of S\<rbrakk> \<Longrightarrow> F face_of convex hull (insert a S)"
lp15@66297
  1681
  by (metis (no_types, lifting) affine_hull_convex_hull face_of_convex_hull_insert hull_insert polytope_def)
lp15@66297
  1682
ak2110@69730
  1683
proposition face_of_polytope_insert2:
lp15@66297
  1684
  fixes a :: "'a :: euclidean_space"
lp15@66297
  1685
  assumes "polytope S" "a \<notin> affine hull S" "F face_of S"
lp15@66297
  1686
  shows "convex hull (insert a F) face_of convex hull (insert a S)"
ak2110@69730
  1687
proof -
lp15@66297
  1688
  obtain V where "finite V" "S = convex hull V"
lp15@66297
  1689
    using assms by (auto simp: polytope_def)
lp15@66297
  1690
  then have "convex hull (insert a F) face_of convex hull (insert a V)"
lp15@66297
  1691
    using affine_hull_convex_hull assms face_of_convex_hull_insert2 by blast
lp15@66297
  1692
  then show ?thesis
lp15@66297
  1693
    by (metis \<open>S = convex hull V\<close> hull_insert)
lp15@66297
  1694
qed
lp15@66297
  1695
lp15@63078
  1696
immler@69683
  1697
subsection\<open>Polyhedra\<close>
ak2110@68833
  1698
ak2110@68833
  1699
definition%important polyhedron where
lp15@63078
  1700
 "polyhedron S \<equiv>
lp15@63078
  1701
        \<exists>F. finite F \<and>
lp15@63078
  1702
            S = \<Inter> F \<and>
lp15@63078
  1703
            (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b})"
lp15@63078
  1704
ak2110@69730
  1705
lemma polyhedron_Int [intro,simp]:
lp15@63078
  1706
   "\<lbrakk>polyhedron S; polyhedron T\<rbrakk> \<Longrightarrow> polyhedron (S \<inter> T)"
lp15@63078
  1707
  apply (simp add: polyhedron_def, clarify)
lp15@63078
  1708
  apply (rename_tac F G)
lp15@63078
  1709
  apply (rule_tac x="F \<union> G" in exI, auto)
lp15@63078
  1710
  done
lp15@63078
  1711
ak2110@69730
  1712
lemma polyhedron_UNIV [iff]: "polyhedron UNIV"
lp15@63078
  1713
  unfolding polyhedron_def
lp15@63078
  1714
  by (rule_tac x="{}" in exI) auto
lp15@63078
  1715
ak2110@69730
  1716
lemma polyhedron_Inter [intro,simp]:
lp15@63078
  1717
   "\<lbrakk>finite F; \<And>S. S \<in> F \<Longrightarrow> polyhedron S\<rbrakk> \<Longrightarrow> polyhedron(\<Inter>F)"
lp15@63078
  1718
by (induction F rule: finite_induct) auto
lp15@63078
  1719
lp15@63078
  1720
ak2110@69730
  1721
lemma polyhedron_empty [iff]: "polyhedron ({} :: 'a :: euclidean_space set)"
lp15@63078
  1722
proof -
lp15@63078
  1723
  have "\<exists>a. a \<noteq> 0 \<and>
lp15@63078
  1724
             (\<exists>b. {x. (SOME i. i \<in> Basis) \<bullet> x \<le> - 1} = {x. a \<bullet> x \<le> b})"
lp15@63078
  1725
    by (rule_tac x="(SOME i. i \<in> Basis)" in exI) (force simp: SOME_Basis nonzero_Basis)
lp15@63078
  1726
  moreover have "\<exists>a b. a \<noteq> 0 \<and>
lp15@63078
  1727
                       {x. - (SOME i. i \<in> Basis) \<bullet> x \<le> - 1} = {x. a \<bullet> x \<le> b}"
lp15@63078
  1728
      apply (rule_tac x="-(SOME i. i \<in> Basis)" in exI)
lp15@63078
  1729
      apply (rule_tac x="-1" in exI)
lp15@63078
  1730
      apply (simp add: SOME_Basis nonzero_Basis)
lp15@63078
  1731
      done
lp15@63078
  1732
  ultimately show ?thesis
lp15@63078
  1733
    unfolding polyhedron_def
lp15@63078
  1734
    apply (rule_tac x="{{x. (SOME i. i \<in> Basis) \<bullet> x \<le> -1},
lp15@63078
  1735
                        {x. -(SOME i. i \<in> Basis) \<bullet> x \<le> -1}}" in exI)
lp15@63078
  1736
    apply force
lp15@63078
  1737
    done
lp15@63078
  1738
qed
lp15@63078
  1739
ak2110@69730
  1740
lemma polyhedron_halfspace_le:
lp15@63078
  1741
  fixes a :: "'a :: euclidean_space"
lp15@63078
  1742
  shows "polyhedron {x. a \<bullet> x \<le> b}"
lp15@63078
  1743
proof (cases "a = 0")
lp15@63078
  1744
  case True then show ?thesis by auto
lp15@63078
  1745
next
lp15@63078
  1746
  case False
lp15@63078
  1747
  then show ?thesis
lp15@63078
  1748
    unfolding polyhedron_def
lp15@63078
  1749
    by (rule_tac x="{{x. a \<bullet> x \<le> b}}" in exI) auto
lp15@63078
  1750
qed
lp15@63078
  1751
ak2110@69730
  1752
lemma polyhedron_halfspace_ge:
lp15@63078
  1753
  fixes a :: "'a :: euclidean_space"
lp15@63078
  1754
  shows "polyhedron {x. a \<bullet> x \<ge> b}"
lp15@63078
  1755
using polyhedron_halfspace_le [of "-a" "-b"] by simp
lp15@63078
  1756
ak2110@69730
  1757
lemma polyhedron_hyperplane:
lp15@63078
  1758
  fixes a :: "'a :: euclidean_space"
lp15@63078
  1759
  shows "polyhedron {x. a \<bullet> x = b}"
ak2110@69730
  1760
proof -
lp15@63078
  1761
  have "{x. a \<bullet> x = b} = {x. a \<bullet> x \<le> b} \<inter> {x. a \<bullet> x \<ge> b}"
lp15@63078
  1762
    by force
lp15@63078
  1763
  then show ?thesis
lp15@63078
  1764
    by (simp add: polyhedron_halfspace_ge polyhedron_halfspace_le)
lp15@63078
  1765
qed
lp15@63078
  1766
ak2110@69730
  1767
lemma affine_imp_polyhedron:
lp15@63078
  1768
  fixes S :: "'a :: euclidean_space set"
lp15@63078
  1769
  shows "affine S \<Longrightarrow> polyhedron S"
lp15@63078
  1770
by (metis affine_hull_eq polyhedron_Inter polyhedron_hyperplane affine_hull_finite_intersection_hyperplanes [of S])
lp15@63078
  1771
ak2110@69730
  1772
lemma polyhedron_imp_closed:
lp15@63078
  1773
  fixes S :: "'a :: euclidean_space set"
lp15@63078
  1774
  shows "polyhedron S \<Longrightarrow> closed S"
lp15@63078
  1775
apply (simp add: polyhedron_def)
lp15@63078
  1776
using closed_halfspace_le by fastforce
lp15@63078
  1777
ak2110@69730
  1778
lemma polyhedron_imp_convex:
lp15@63078
  1779
  fixes S :: "'a :: euclidean_space set"
lp15@63078
  1780
  shows "polyhedron S \<Longrightarrow> convex S"
lp15@63078
  1781
apply (simp add: polyhedron_def)
lp15@63078
  1782
using convex_Inter convex_halfspace_le by fastforce
lp15@63078
  1783
ak2110@69730
  1784
lemma polyhedron_affine_hull:
lp15@63078
  1785
  fixes S :: "'a :: euclidean_space set"
lp15@63078
  1786
  shows "polyhedron(affine hull S)"
lp15@63078
  1787
by (simp add: affine_imp_polyhedron)
lp15@63078
  1788
lp15@63078
  1789
immler@69683
  1790
subsection\<open>Canonical polyhedron representation making facial structure explicit\<close>
ak2110@68833
  1791
ak2110@69730
  1792
proposition polyhedron_Int_affine:
lp15@63078
  1793
  fixes S :: "'a :: euclidean_space set"
lp15@63078
  1794
  shows "polyhedron S \<longleftrightarrow>
lp15@63078
  1795
           (\<exists>F. finite F \<and> S = (affine hull S) \<inter> \<Inter>F \<and>
lp15@63078
  1796
                (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}))"
lp15@63078
  1797
        (is "?lhs = ?rhs")
ak2110@69730
  1798
proof
lp15@63078
  1799
  assume ?lhs then show ?rhs
lp15@63078
  1800
    apply (simp add: polyhedron_def)
lp15@63078
  1801
    apply (erule ex_forward)
lp15@63078
  1802
    using hull_subset apply force
lp15@63078
  1803
    done
lp15@63078
  1804
next
lp15@63078
  1805
  assume ?rhs then show ?lhs
lp15@63078
  1806
    apply clarify
lp15@63078
  1807
    apply (erule ssubst)
lp15@63078
  1808
    apply (force intro: polyhedron_affine_hull polyhedron_halfspace_le)
lp15@63078
  1809
    done
lp15@63078
  1810
qed
lp15@63078
  1811
ak2110@69730
  1812
proposition rel_interior_polyhedron_explicit:
lp15@63078
  1813
  assumes "finite F"
lp15@63078
  1814
      and seq: "S = affine hull S \<inter> \<Inter>F"
lp15@63078
  1815
      and faceq: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
lp15@63078
  1816
      and psub: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> affine hull S \<inter> \<Inter>F'"
lp15@63078
  1817
    shows "rel_interior S = {x \<in> S. \<forall>h \<in> F. a h \<bullet> x < b h}"
ak2110@69730
  1818
proof -
lp15@63078
  1819
  have rels: "\<And>x. x \<in> rel_interior S \<Longrightarrow> x \<in> S"
lp15@63078
  1820
    by (meson IntE mem_rel_interior)
lp15@63078
  1821
  moreover have "a i \<bullet> x < b i" if x: "x \<in> rel_interior S" and "i \<in> F" for x i
lp15@63078
  1822
  proof -
lp15@63078
  1823
    have fif: "F - {i} \<subset> F"
lp15@63078
  1824
      using \<open>i \<in> F\<close> Diff_insert_absorb Diff_subset set_insert psubsetI by blast
lp15@63078
  1825
    then have "S \<subset> affine hull S \<inter> \<Inter>(F - {i})"
lp15@63078
  1826
      by (rule psub)
lp15@63078
  1827
    then obtain z where ssub: "S \<subseteq> \<Inter>(F - {i})" and zint: "z \<in> \<Inter>(F - {i})"
lp15@63078
  1828
                    and "z \<notin> S" and zaff: "z \<in> affine hull S"
lp15@63078
  1829
      by auto
lp15@63078
  1830
    have "z \<noteq> x"
lp15@63078
  1831
      using \<open>z \<notin> S\<close> rels x by blast
lp15@63078
  1832
    have "z \<notin> affine hull S \<inter> \<Inter>F"
lp15@63078
  1833
      using \<open>z \<notin> S\<close> seq by auto
lp15@63078
  1834
    then have aiz: "a i \<bullet> z > b i"
lp15@63078
  1835
      using faceq zint zaff by fastforce
lp15@63078
  1836
    obtain e where "e > 0" "x \<in> S" and e: "ball x e \<inter> affine hull S \<subseteq> S"
lp15@63078
  1837
      using x by (auto simp: mem_rel_interior_ball)
lp15@63078
  1838
    then have ins: "\<And>y. \<lbrakk>norm (x - y) < e; y \<in> affine hull S\<rbrakk> \<Longrightarrow> y \<in> S"
lp15@63078
  1839
      by (metis IntI subsetD dist_norm mem_ball)
wenzelm@63148
  1840
    define \<xi> where "\<xi> = min (1/2) (e / 2 / norm(z - x))"
lp15@63078
  1841
    have "norm (\<xi> *\<^sub>R x - \<xi> *\<^sub>R z) = norm (\<xi> *\<^sub>R (x - z))"
lp15@63078
  1842
      by (simp add: \<xi>_def algebra_simps norm_mult)
lp15@63078
  1843
    also have "... = \<xi> * norm (x - z)"
lp15@63078
  1844
      using \<open>e > 0\<close> by (simp add: \<xi>_def)
lp15@63078
  1845
    also have "... < e"
lp15@63078
  1846
      using \<open>z \<noteq> x\<close> \<open>e > 0\<close> by (simp add: \<xi>_def min_def divide_simps norm_minus_commute)
lp15@63078
  1847
    finally have lte: "norm (\<xi> *\<^sub>R x - \<xi> *\<^sub>R z) < e" .
lp15@63078
  1848
    have \<xi>_aff: "\<xi> *\<^sub>R z + (1 - \<xi>) *\<^sub>R x \<in> affine hull S"
lp15@63078
  1849
      by (metis \<open>x \<in> S\<close> add.commute affine_affine_hull diff_add_cancel hull_inc mem_affine zaff)
lp15@63078
  1850
    have "\<xi> *\<^sub>R z + (1 - \<xi>) *\<^sub>R x \<in> S"
lp15@63078
  1851
      apply (rule ins [OF _ \<xi>_aff])
lp15@63078
  1852
      apply (simp add: algebra_simps lte)
lp15@63078
  1853
      done
lp15@63078
  1854
    then obtain l where l: "0 < l" "l < 1" and ls: "(l *\<^sub>R z + (1 - l) *\<^sub>R x) \<in> S"
lp15@63078
  1855
      apply (rule_tac l = \<xi> in that)
lp15@63078
  1856
      using \<open>e > 0\<close> \<open>z \<noteq> x\<close>  apply (auto simp: \<xi>_def)
lp15@63078
  1857
      done
lp15@63078
  1858
    then have i: "l *\<^sub>R z + (1 - l) *\<^sub>R x \<in> i"
lp15@63078
  1859
      using seq \<open>i \<in> F\<close> by auto
lp15@63078
  1860
    have "b i * l + (a i \<bullet> x) * (1 - l) < a i \<bullet> (l *\<^sub>R z + (1 - l) *\<^sub>R x)"
lp15@63078
  1861
      using l by (simp add: algebra_simps aiz)
lp15@63078
  1862
    also have "\<dots> \<le> b i" using i l
lp15@63078
  1863
      using faceq mem_Collect_eq \<open>i \<in> F\<close> by blast
lp15@63078
  1864
    finally have "(a i \<bullet> x) * (1 - l) < b i * (1 - l)"
lp15@63078
  1865
      by (simp add: algebra_simps)
lp15@63078
  1866
    with l show ?thesis
lp15@63078
  1867
      by simp
lp15@63078
  1868
  qed
lp15@63078
  1869
  moreover have "x \<in> rel_interior S"
lp15@63078
  1870
           if "x \<in> S" and less: "\<And>h. h \<in> F \<Longrightarrow> a h \<bullet> x < b h" for x
lp15@63078
  1871
  proof -
lp15@63078
  1872
    have 1: "\<And>h. h \<in> F \<Longrightarrow> x \<in> interior h"
lp15@63078
  1873
      by (metis interior_halfspace_le mem_Collect_eq less faceq)
lp15@63078
  1874
    have 2: "\<And>y. \<lbrakk>\<forall>h\<in>F. y \<in> interior h; y \<in> affine hull S\<rbrakk> \<Longrightarrow> y \<in> S"
lp15@63078
  1875
      by (metis IntI Inter_iff contra_subsetD interior_subset seq)
lp15@63078
  1876
    show ?thesis
lp15@63078
  1877
      apply (simp add: rel_interior \<open>x \<in> S\<close>)
lp15@63078
  1878
      apply (rule_tac x="\<Inter>h\<in>F. interior h" in exI)
lp15@63078
  1879
      apply (auto simp: \<open>finite F\<close> open_INT 1 2)
lp15@63078
  1880
      done
lp15@63078
  1881
  qed
lp15@63078
  1882
  ultimately show ?thesis by blast
lp15@63078
  1883
qed
lp15@63078
  1884
lp15@63078
  1885
ak2110@69730
  1886
lemma polyhedron_Int_affine_parallel:
lp15@63078
  1887
  fixes S :: "'a :: euclidean_space set"
lp15@63078
  1888
  shows "polyhedron S \<longleftrightarrow>
lp15@63078
  1889
         (\<exists>F. finite F \<and>
lp15@63078
  1890
              S = (affine hull S) \<inter> (\<Inter>F) \<and>
lp15@63078
  1891
              (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b} \<and>
lp15@63078
  1892
                             (\<forall>x \<in> affine hull S. (x + a) \<in> affine hull S)))"
lp15@63078
  1893
    (is "?lhs = ?rhs")
ak2110@69730
  1894
proof
lp15@63078
  1895
  assume ?lhs
lp15@63078
  1896
  then obtain F where "finite F" and seq: "S = (affine hull S) \<inter> \<Inter>F"
lp15@63078
  1897
                  and faces: "\<And>h. h \<in> F \<Longrightarrow> \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}"
lp15@63078
  1898
    by (fastforce simp add: polyhedron_Int_affine)
lp15@63078
  1899
  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}"
lp15@63078
  1900
    by metis
lp15@63078
  1901
  show ?rhs
lp15@63078
  1902
  proof -
lp15@63078
  1903
    have "\<exists>a' b'. a' \<noteq> 0 \<and>
lp15@63078
  1904
                  affine hull S \<inter> {x. a' \<bullet> x \<le> b'} = affine hull S \<inter> h \<and>
lp15@63078
  1905
                  (\<forall>w \<in> affine hull S. (w + a') \<in> affine hull S)"
nipkow@69508
  1906
        if "h \<in> F" "\<not>(affine hull S \<subseteq> h)" for h
lp15@63078
  1907
    proof -
lp15@63078
  1908
      have "a h \<noteq> 0" and "h = {x. a h \<bullet> x \<le> b h}" "h \<inter> \<Inter>F = \<Inter>F"
lp15@63078
  1909
        using \<open>h \<in> F\<close> ab by auto
lp15@63078
  1910
      then have "(affine hull S) \<inter> {x. a h \<bullet> x \<le> b h} \<noteq> {}"
lp15@63078
  1911
        by (metis (no_types) affine_hull_eq_empty inf.absorb_iff2 inf_assoc inf_bot_right inf_commute seq that(2))
nipkow@69508
  1912
      moreover have "\<not> (affine hull S \<subseteq> {x. a h \<bullet> x \<le> b h})"
lp15@63078
  1913
        using \<open>h = {x. a h \<bullet> x \<le> b h}\<close> that(2) by blast
lp15@63078
  1914
      ultimately show ?thesis
lp15@63078
  1915
        using affine_parallel_slice [of "affine hull S"]
lp15@63078
  1916
        by (metis \<open>h = {x. a h \<bullet> x \<le> b h}\<close> affine_affine_hull)
lp15@63078
  1917
    qed
lp15@63078
  1918
    then obtain a b
nipkow@69508
  1919
         where ab: "\<And>h. \<lbrakk>h \<in> F; \<not> (affine hull S \<subseteq> h)\<rbrakk>
lp15@63078
  1920
             \<Longrightarrow> a h \<noteq> 0 \<and>
lp15@63078
  1921
                  affine hull S \<inter> {x. a h \<bullet> x \<le> b h} = affine hull S \<inter> h \<and>
lp15@63078
  1922
                  (\<forall>w \<in> affine hull S. (w + a h) \<in> affine hull S)"
lp15@63078
  1923
      by metis
lp15@63078
  1924
    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})"
lp15@63078
  1925
      by (subst seq) (auto simp: ab INT_extend_simps)
lp15@63078
  1926
    show ?thesis
nipkow@69508
  1927
      apply (rule_tac x="(\<lambda>h. {x. a h \<bullet> x \<le> b h}) ` {h. h \<in> F \<and> \<not>(affine hull S \<subseteq> h)}" in exI)
lp15@63078
  1928
      apply (intro conjI seq2)
lp15@63078
  1929
        using \<open>finite F\<close> apply force
lp15@63078
  1930
       using ab apply blast
lp15@63078
  1931
       done
lp15@63078
  1932
  qed
lp15@63078
  1933
next
lp15@63078
  1934
  assume ?rhs then show ?lhs
lp15@63078
  1935
    apply (simp add: polyhedron_Int_affine)
lp15@63078
  1936
    by metis
lp15@63078
  1937
qed
lp15@63078
  1938
lp15@63078
  1939
ak2110@69730
  1940
proposition polyhedron_Int_affine_parallel_minimal:
lp15@63078
  1941
  fixes S :: "'a :: euclidean_space set"
lp15@63078
  1942
  shows "polyhedron S \<longleftrightarrow>
lp15@63078
  1943
         (\<exists>F. finite F \<and>
lp15@63078
  1944
              S = (affine hull S) \<inter> (\<Inter>F) \<and>
lp15@63078
  1945
              (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b} \<and>
lp15@63078
  1946
                             (\<forall>x \<in> affine hull S. (x + a) \<in> affine hull S)) \<and>
lp15@63078
  1947
              (\<forall>F'. F' \<subset> F \<longrightarrow> S \<subset> (affine hull S) \<inter> (\<Inter>F')))"
lp15@63078
  1948
    (is "?lhs = ?rhs")
ak2110@69730
  1949
proof
lp15@63078
  1950
  assume ?lhs
lp15@63078
  1951
  then obtain f0
lp15@63078
  1952
           where f0: "finite f0"
lp15@63078
  1953
                 "S = (affine hull S) \<inter> (\<Inter>f0)"
lp15@63078
  1954
                   (is "?P f0")
lp15@63078
  1955
                 "\<forall>h \<in> f0. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b} \<and>
lp15@63078
  1956
                             (\<forall>x \<in> affine hull S. (x + a) \<in> affine hull S)"
lp15@63078
  1957
                   (is "?Q f0")
lp15@63078
  1958
    by (force simp: polyhedron_Int_affine_parallel)
wenzelm@63148
  1959
  define n where "n = (LEAST n. \<exists>F. card F = n \<and> finite F \<and> ?P F \<and> ?Q F)"
lp15@63078
  1960
  have nf: "\<exists>F. card F = n \<and> finite F \<and> ?P F \<and> ?Q F"
lp15@63078
  1961
    apply (simp add: n_def)
lp15@63078
  1962
    apply (rule LeastI [where k = "card f0"])
lp15@63078
  1963
    using f0 apply auto
lp15@63078
  1964
    done
lp15@63078
  1965
  then obtain F where F: "card F = n" "finite F" and seq: "?P F" and aff: "?Q F"
lp15@63078
  1966
    by blast
nipkow@69508
  1967
  then have "\<not> (finite g \<and> ?P g \<and> ?Q g)" if "card g < n" for g
lp15@63078
  1968
    using that by (auto simp: n_def dest!: not_less_Least)
nipkow@69508
  1969
  then have *: "\<not> (?P g \<and> ?Q g)" if "g \<subset> F" for g
lp15@63078
  1970
    using that \<open>finite F\<close> psubset_card_mono \<open>card F = n\<close>
lp15@63078
  1971
    by (metis finite_Int inf.strict_order_iff)
lp15@63078
  1972
  have 1: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subseteq> affine hull S \<inter> \<Inter>F'"
lp15@63078
  1973
    by (subst seq) blast
lp15@63078
  1974
  have 2: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<noteq> affine hull S \<inter> \<Inter>F'"
lp15@63078
  1975
    apply (frule *)
lp15@63078
  1976
    by (metis aff subsetCE subset_iff_psubset_eq)
lp15@63078
  1977
  show ?rhs
lp15@63078
  1978
    by (metis \<open>finite F\<close> seq aff psubsetI 1 2)
lp15@63078
  1979
next
lp15@63078
  1980
  assume ?rhs then show ?lhs
lp15@63078
  1981
    by (auto simp: polyhedron_Int_affine_parallel)
lp15@63078
  1982
qed
lp15@63078
  1983
lp15@63078
  1984
ak2110@69730
  1985
lemma polyhedron_Int_affine_minimal:
lp15@63078
  1986
  fixes S :: "'a :: euclidean_space set"
lp15@63078
  1987
  shows "polyhedron S \<longleftrightarrow>
lp15@63078
  1988
         (\<exists>F. finite F \<and> S = (affine hull S) \<inter> \<Inter>F \<and>
lp15@63078
  1989
              (\<forall>h \<in> F. \<exists>a b. a \<noteq> 0 \<and> h = {x. a \<bullet> x \<le> b}) \<and>
lp15@63078
  1990
              (\<forall>F'. F' \<subset> F \<longrightarrow> S \<subset> (affine hull S) \<inter> \<Inter>F'))"
lp15@63078
  1991
apply (rule iffI)
lp15@63078
  1992
 apply (force simp: polyhedron_Int_affine_parallel_minimal elim!: ex_forward)
lp15@63078
  1993
apply (auto simp: polyhedron_Int_affine elim!: ex_forward)
lp15@63078
  1994
done
lp15@63078
  1995
ak2110@69730
  1996
proposition facet_of_polyhedron_explicit:
lp15@63078
  1997
  assumes "finite F"
lp15@63078
  1998
      and seq: "S = affine hull S \<inter> \<Inter>F"
lp15@63078
  1999
      and faceq: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
lp15@63078
  2000
      and psub: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> affine hull S \<inter> \<Inter>F'"
lp15@63078
  2001
    shows "c facet_of S \<longleftrightarrow> (\<exists>h. h \<in> F \<and> c = S \<inter> {x. a h \<bullet> x = b h})"
ak2110@69730
  2002
proof (cases "S = {}")
lp15@63078
  2003
  case True with psub show ?thesis by force
lp15@63078
  2004
next
lp15@63078
  2005
  case False
lp15@63078
  2006
  have "polyhedron S"
lp15@63078
  2007
    apply (simp add: polyhedron_Int_affine)
lp15@63078
  2008
    apply (rule_tac x=F in exI)
lp15@63078
  2009
    using assms  apply force
lp15@63078
  2010
    done
lp15@63078
  2011
  then have "convex S"
lp15@63078
  2012
    by (rule polyhedron_imp_convex)
lp15@63078
  2013
  with False rel_interior_eq_empty have "rel_interior S \<noteq> {}" by blast
lp15@63078
  2014
  then obtain x where "x \<in> rel_interior S" by auto
lp15@63078
  2015
  then obtain T where "open T" "x \<in> T" "x \<in> S" "T \<inter> affine hull S \<subseteq> S"
lp15@63078
  2016
    by (force simp: mem_rel_interior)
lp15@63078
  2017
  then have xaff: "x \<in> affine hull S" and xint: "x \<in> \<Inter>F"
lp15@63078
  2018
    using seq hull_inc by auto
lp15@63078
  2019
  have "rel_interior S = {x \<in> S. \<forall>h\<in>F. a h \<bullet> x < b h}"
lp15@63078
  2020
    by (rule rel_interior_polyhedron_explicit [OF \<open>finite F\<close> seq faceq psub])
lp15@63078
  2021
  with \<open>x \<in> rel_interior S\<close>
lp15@63078
  2022
  have [simp]: "\<And>h. h\<in>F \<Longrightarrow> a h \<bullet> x < b h" by blast
lp15@63078
  2023
  have *: "(S \<inter> {x. a h \<bullet> x = b h}) facet_of S" if "h \<in> F" for h
lp15@63078
  2024
  proof -
lp15@63078
  2025
    have "S \<subset> affine hull S \<inter> \<Inter>(F - {h})"
lp15@63078
  2026
      using psub that by (metis Diff_disjoint Diff_subset insert_disjoint(2) psubsetI)
lp15@63078
  2027
    then obtain z where zaff: "z \<in> affine hull S" and zint: "z \<in> \<Inter>(F - {h})" and "z \<notin> S"
lp15@63078
  2028
      by force
lp15@63078
  2029
    then have "z \<noteq> x" "z \<notin> h" using seq \<open>x \<in> S\<close> by auto
lp15@63078
  2030
    have "x \<in> h" using that xint by auto
lp15@63078
  2031
    then have able: "a h \<bullet> x \<le> b h"
lp15@63078
  2032
      using faceq that by blast
lp15@63078
  2033
    also have "... < a h \<bullet> z" using \<open>z \<notin> h\<close> faceq [OF that] xint by auto
lp15@63078
  2034
    finally have xltz: "a h \<bullet> x < a h \<bullet> z" .
wenzelm@63148
  2035
    define l where "l = (b h - a h \<bullet> x) / (a h \<bullet> z - a h \<bullet> x)"
wenzelm@63148
  2036
    define w where "w = (1 - l) *\<^sub>R x + l *\<^sub>R z"
lp15@63078
  2037
    have "0 < l" "l < 1"
lp15@63078
  2038
      using able xltz \<open>b h < a h \<bullet> z\<close> \<open>h \<in> F\<close>
lp15@63078
  2039
      by (auto simp: l_def divide_simps)
lp15@63078
  2040
    have awlt: "a i \<bullet> w < b i" if "i \<in> F" "i \<noteq> h" for i
lp15@63078
  2041
    proof -
lp15@63078
  2042
      have "(1 - l) * (a i \<bullet> x) < (1 - l) * b i"
lp15@63078
  2043
        by (simp add: \<open>l < 1\<close> \<open>i \<in> F\<close>)
lp15@63078
  2044
      moreover have "l * (a i \<bullet> z) \<le> l * b i"
lp15@63078
  2045
        apply (rule mult_left_mono)
lp15@63078
  2046
        apply (metis Diff_insert_absorb Inter_iff Set.set_insert \<open>h \<in> F\<close> faceq insertE mem_Collect_eq that zint)
lp15@63078
  2047
        using \<open>0 < l\<close>
lp15@63078
  2048
        apply simp
lp15@63078
  2049
        done
lp15@63078
  2050
      ultimately show ?thesis by (simp add: w_def algebra_simps)
lp15@63078
  2051
    qed
lp15@63078
  2052
    have weq: "a h \<bullet> w = b h"
lp15@63078
  2053
      using xltz unfolding w_def l_def
lp15@63078
  2054
      by (simp add: algebra_simps) (simp add: field_simps)
lp15@63078
  2055
    have "w \<in> affine hull S"
lp15@63078
  2056
      by (simp add: w_def mem_affine xaff zaff)
lp15@63078
  2057
    moreover have "w \<in> \<Inter>F"
lp15@63078
  2058
      using \<open>a h \<bullet> w = b h\<close> awlt faceq less_eq_real_def by blast
lp15@63078
  2059
    ultimately have "w \<in> S"
lp15@63078
  2060
      using seq by blast
lp15@63078
  2061
    with weq have "S \<inter> {x. a h \<bullet> x = b h} \<noteq> {}" by blast
lp15@63078
  2062
    moreover have "S \<inter> {x. a h \<bullet> x = b h} face_of S"
lp15@63078
  2063
      apply (rule face_of_Int_supporting_hyperplane_le)
lp15@63078
  2064
      apply (rule \<open>convex S\<close>)
lp15@63078
  2065
      apply (subst (asm) seq)
lp15@63078
  2066
      using faceq that apply fastforce
lp15@63078
  2067
      done
lp15@63078
  2068
    moreover have "affine hull (S \<inter> {x. a h \<bullet> x = b h}) =
lp15@63078
  2069
                   (affine hull S) \<inter> {x. a h \<bullet> x = b h}"
lp15@63078
  2070
    proof
lp15@63078
  2071
      show "affine hull (S \<inter> {x. a h \<bullet> x = b h}) \<subseteq> affine hull S \<inter> {x. a h \<bullet> x = b h}"
lp15@63078
  2072
        apply (intro Int_greatest hull_mono Int_lower1)
lp15@63078
  2073
        apply (metis affine_hull_eq affine_hyperplane hull_mono inf_le2)
lp15@63078
  2074
        done
lp15@63078
  2075
    next
lp15@63078
  2076
      show "affine hull S \<inter> {x. a h \<bullet> x = b h} \<subseteq> affine hull (S \<inter> {x. a h \<bullet> x = b h})"
lp15@63078
  2077
      proof
lp15@63078
  2078
        fix y
lp15@63078
  2079
        assume yaff: "y \<in> affine hull S \<inter> {y. a h \<bullet> y = b h}"
lp15@63078
  2080
        obtain T where "0 < T"
lp15@63078
  2081
                 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"
lp15@63078
  2082
        proof (cases "F - {h} = {}")
lp15@63078
  2083
          case True then show ?thesis
lp15@63078
  2084
            by (rule_tac T=1 in that) auto
lp15@63078
  2085
        next
lp15@63078
  2086
          case False
lp15@63078
  2087
          then obtain h' where h': "h' \<in> F - {h}" by auto
haftmann@69661
  2088
          let ?body = "(\<lambda>j. if 0 < a j \<bullet> y - a j \<bullet> w
wenzelm@63148
  2089
              then (b j - a j \<bullet> w) / (a j \<bullet> y - a j \<bullet> w)
haftmann@69661
  2090
              else 1) ` (F - {h})"
haftmann@69661
  2091
          define inff where "inff = Inf ?body"
haftmann@69661
  2092
          from \<open>finite F\<close> have "finite ?body"
haftmann@69661
  2093
            by blast
haftmann@69661
  2094
          moreover from h' have "?body \<noteq> {}"
haftmann@69661
  2095
            by blast
haftmann@69661
  2096
          moreover have "j > 0" if "j \<in> ?body" for j
haftmann@69661
  2097
          proof -
haftmann@69661
  2098
            from that obtain x where "x \<in> F" and "x \<noteq> h" and *: "j =
haftmann@69661
  2099
              (if 0 < a x \<bullet> y - a x \<bullet> w
haftmann@69661
  2100
                then (b x - a x \<bullet> w) / (a x \<bullet> y - a x \<bullet> w) else 1)"
haftmann@69661
  2101
              by blast
haftmann@69661
  2102
            with awlt [of x] have "a x \<bullet> w < b x"
haftmann@69661
  2103
              by simp
haftmann@69661
  2104
            with * show ?thesis
haftmann@69661
  2105
              by simp
haftmann@69661
  2106
          qed
haftmann@69661
  2107
          ultimately have "0 < inff"
haftmann@69661
  2108
            by (simp_all add: finite_less_Inf_iff inff_def)
lp15@63078
  2109
          moreover have "inff * (a j \<bullet> y - a j \<bullet> w) \<le> b j - a j \<bullet> w"
lp15@63078
  2110
                        if "j \<in> F" "j \<noteq> h" for j
lp15@63078
  2111
          proof (cases "a j \<bullet> w < a j \<bullet> y")
lp15@63078
  2112
            case True
lp15@63078
  2113
            then have "inff \<le> (b j - a j \<bullet> w) / (a j \<bullet> y - a j \<bullet> w)"
lp15@63078
  2114
              apply (simp add: inff_def)
lp15@63078
  2115
              apply (rule cInf_le_finite)
lp15@63078
  2116
              using \<open>finite F\<close> apply blast
lp15@63078
  2117
              apply (simp add: that split: if_split_asm)
lp15@63078
  2118
              done
lp15@63078
  2119
            then show ?thesis
lp15@63078
  2120
              using \<open>0 < inff\<close> awlt [OF that] mult_strict_left_mono
lp15@63078
  2121
              by (fastforce simp add: algebra_simps divide_simps split: if_split_asm)
lp15@63078
  2122
          next
lp15@63078
  2123
            case False
lp15@63078
  2124
            with \<open>0 < inff\<close> have "inff * (a j \<bullet> y - a j \<bullet> w) \<le> 0"
lp15@63078
  2125
              by (simp add: mult_le_0_iff)
lp15@63078
  2126
            also have "... < b j - a j \<bullet> w"
lp15@63078
  2127
              by (simp add: awlt that)
lp15@63078
  2128
            finally show ?thesis by simp
lp15@63078
  2129
          qed
lp15@63078
  2130
          ultimately show ?thesis
lp15@63078
  2131
            by (blast intro: that)
lp15@63078
  2132
        qed
wenzelm@63148
  2133
        define c where "c = (1 - T) *\<^sub>R w + T *\<^sub>R y"
lp15@63078
  2134
        have "(1 - T) *\<^sub>R w + T *\<^sub>R y \<in> j" if "j \<in> F" for j
lp15@63078
  2135
        proof (cases "j = h")
lp15@63078
  2136
          case True
lp15@63078
  2137
          have "(1 - T) *\<^sub>R w + T *\<^sub>R y \<in> {x. a h \<bullet> x \<le> b h}"
lp15@63078
  2138
            using weq yaff by (auto simp: algebra_simps)
lp15@63078
  2139
          with True faceq [OF that] show ?thesis by metis
lp15@63078
  2140
        next
lp15@63078
  2141
          case False
lp15@63078
  2142
          with T that have "(1 - T) *\<^sub>R w + T *\<^sub>R y \<in> {x. a j \<bullet> x \<le> b j}"
lp15@63078
  2143
            by (simp add: algebra_simps)
lp15@63078
  2144
          with faceq [OF that] show ?thesis by simp
lp15@63078
  2145
        qed
lp15@63078
  2146
        moreover have "(1 - T) *\<^sub>R w + T *\<^sub>R y \<in> affine hull S"
wenzelm@63170
  2147
          apply (rule affine_affine_hull [simplified affine_alt, rule_format])
lp15@63078
  2148
          apply (simp add: \<open>w \<in> affine hull S\<close>)
lp15@63078
  2149
          using yaff apply blast
lp15@63078
  2150
          done
lp15@63078
  2151
        ultimately have "c \<in> S"
lp15@63078
  2152
          using seq by (force simp: c_def)
lp15@63078
  2153
        moreover have "a h \<bullet> c = b h"
lp15@63078
  2154
          using yaff by (force simp: c_def algebra_simps weq)
lp15@63078
  2155
        ultimately have caff: "c \<in> affine hull (S \<inter> {y. a h \<bullet> y = b h})"
lp15@63078
  2156
          by (simp add: hull_inc)
lp15@63078
  2157
        have waff: "w \<in> affine hull (S \<inter> {y. a h \<bullet> y = b h})"
lp15@63078
  2158
          using \<open>w \<in> S\<close> weq by (blast intro: hull_inc)
lp15@63078
  2159
        have yeq: "y = (1 - inverse T) *\<^sub>R w + c /\<^sub>R T"
lp15@63078
  2160
          using \<open>0 < T\<close> by (simp add: c_def algebra_simps)
lp15@63078
  2161
        show "y \<in> affine hull (S \<inter> {y. a h \<bullet> y = b h})"
wenzelm@63170
  2162
          by (metis yeq affine_affine_hull [simplified affine_alt, rule_format, OF waff caff])
lp15@63078
  2163
      qed
lp15@63078
  2164
    qed
lp15@63078
  2165
    ultimately show ?thesis
lp15@63078
  2166
      apply (simp add: facet_of_def)
lp15@63078
  2167
      apply (subst aff_dim_affine_hull [symmetric])
lp15@63078
  2168
      using  \<open>b h < a h \<bullet> z\<close> zaff
lp15@63078
  2169
      apply (force simp: aff_dim_affine_Int_hyperplane)
lp15@63078
  2170
      done
lp15@63078
  2171
  qed
lp15@63078
  2172
  show ?thesis
lp15@63078
  2173
  proof
lp15@63078
  2174
    show "\<exists>h. h \<in> F \<and> c = S \<inter> {x. a h \<bullet> x = b h} \<Longrightarrow> c facet_of S"
lp15@63078
  2175
      using * by blast
lp15@63078
  2176
  next
lp15@63078
  2177
    assume "c facet_of S"
lp15@63078
  2178
    then have "c face_of S" "convex c" "c \<noteq> {}" and affc: "aff_dim c = aff_dim S - 1"
lp15@63078
  2179
      by (auto simp: facet_of_def face_of_imp_convex)
lp15@63078
  2180
    then obtain x where x: "x \<in> rel_interior c"
lp15@63078
  2181
      by (force simp: rel_interior_eq_empty)
lp15@63078
  2182
    then have "x \<in> c"
lp15@63078
  2183
      by (meson subsetD rel_interior_subset)
lp15@63078
  2184
    then have "x \<in> S"
lp15@63078
  2185
      using \<open>c facet_of S\<close> facet_of_imp_subset by blast
lp15@63078
  2186
    have rels: "rel_interior S = {x \<in> S. \<forall>h\<in>F. a h \<bullet> x < b h}"
lp15@63078
  2187
      by (rule rel_interior_polyhedron_explicit [OF assms])
lp15@63078
  2188
    have "c \<noteq> S"
lp15@63078
  2189
      using \<open>c facet_of S\<close> facet_of_irrefl by blast
lp15@63078
  2190
    then have "x \<notin> rel_interior S"
lp15@63078
  2191
      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)
lp15@63078
  2192
    with rels \<open>x \<in> S\<close> obtain i where "i \<in> F" and i: "a i \<bullet> x \<ge> b i"
lp15@63078
  2193
      by force
lp15@63078
  2194
    have "x \<in> {u. a i \<bullet> u \<le> b i}"
lp15@63078
  2195
      by (metis IntD2 InterE \<open>i \<in> F\<close> \<open>x \<in> S\<close> faceq seq)
lp15@63078
  2196
    then have "a i \<bullet> x \<le> b i" by simp
lp15@63078
  2197
    then have "a i \<bullet> x = b i" using i by auto
lp15@63078
  2198
    have "c \<subseteq> S \<inter> {x. a i \<bullet> x = b i}"
lp15@63078
  2199
      apply (rule subset_of_face_of [of _ S])
lp15@63078
  2200
        apply (simp add: "*" \<open>i \<in> F\<close> facet_of_imp_face_of)
lp15@63078
  2201
       apply (simp add: \<open>c face_of S\<close> face_of_imp_subset)
lp15@63078
  2202
      using \<open>a i \<bullet> x = b i\<close> \<open>x \<in> S\<close> x by blast
lp15@63078
  2203
    then have cface: "c face_of (S \<inter> {x. a i \<bullet> x = b i})"
lp15@63078
  2204
      by (meson \<open>c face_of S\<close> face_of_subset inf_le1)
lp15@63078
  2205
    have con: "convex (S \<inter> {x. a i \<bullet> x = b i})"
lp15@63078
  2206
      by (simp add: \<open>convex S\<close> convex_Int convex_hyperplane)
lp15@63078
  2207
    show "\<exists>h. h \<in> F \<and> c = S \<inter> {x. a h \<bullet> x = b h}"
lp15@63078
  2208
      apply (rule_tac x=i in exI)
lp15@63078
  2209
      apply (simp add: \<open>i \<in> F\<close>)
lp15@63078
  2210
      by (metis (no_types) * \<open>i \<in> F\<close> affc facet_of_def less_irrefl face_of_aff_dim_lt [OF con cface])
lp15@63078
  2211
  qed
lp15@63078
  2212
qed
lp15@63078
  2213
lp15@63078
  2214
ak2110@69730
  2215
lemma face_of_polyhedron_subset_explicit:
lp15@63078
  2216
  fixes S :: "'a :: euclidean_space set"
lp15@63078
  2217
  assumes "finite F"
lp15@63078
  2218
      and seq: "S = affine hull S \<inter> \<Inter>F"
lp15@63078
  2219
      and faceq: "\<And>h. h \<in> F \<Longrightarrow> a h \<noteq> 0 \<and> h = {x. a h \<bullet> x \<le> b h}"
lp15@63078
  2220
      and psub: "\<And>F'. F' \<subset> F \<Longrightarrow> S \<subset> affine hull S \<inter> \<Inter>F'"
lp15@63078
  2221
      and c: "c face_of S" and "c \<noteq> {}" "c \<noteq> S"