100/polyhedron.ml

   1 (* ========================================================================= *)
   2 (* Formalization of Jim Lawrence's proof of Euler's relation.                *)
   3 (* ========================================================================= *)
   4
   5 needs "Multivariate/polytope.ml";;
   6 needs "Library/binomial.ml";;
   7 needs "100/inclusion_exclusion.ml";;
   8 needs "100/combinations.ml";;
   9
  10 prioritize_real();;
  11
  12 (* ------------------------------------------------------------------------- *)
  13 (* Interpret which "side" of a hyperplane a point is on.                     *)
  14 (* ------------------------------------------------------------------------- *)
  15
  16 let hyperplane_side = new_definition
  17  `hyperplane_side (a,b) (x:real^N) = real_sgn (a dot x - b)`;;
  18
  19 (* ------------------------------------------------------------------------- *)
  20 (* Equivalence relation imposed by a hyperplane arrangement.                 *)
  21 (* ------------------------------------------------------------------------- *)
  22
  23 let hyperplane_equiv = new_definition
  24  `hyperplane_equiv A x y <=>
  25         !h. h IN A ==> hyperplane_side h x = hyperplane_side h y`;;
  26
  27 let HYPERPLANE_EQUIV_REFL = prove
  28  (`!A x. hyperplane_equiv A x x`,
  29   REWRITE_TAC[hyperplane_equiv]);;
  30
  31 let HYPERPLANE_EQUIV_SYM = prove
  32  (`!A x y. hyperplane_equiv A x y <=> hyperplane_equiv A y x`,
  33   REWRITE_TAC[hyperplane_equiv; EQ_SYM_EQ]);;
  34
  35 let HYPERPLANE_EQUIV_TRANS = prove
  36  (`!A x y z.
  37         hyperplane_equiv A x y /\ hyperplane_equiv A y z
  38         ==> hyperplane_equiv A x z`,
  39   REWRITE_TAC[hyperplane_equiv] THEN MESON_TAC[]);;
  40
  41 let HYPERPLANE_EQUIV_UNION = prove
  42  (`!A B x y. hyperplane_equiv (A UNION B) x y <=>
  43                 hyperplane_equiv A x y /\ hyperplane_equiv B x y`,
  44   REWRITE_TAC[hyperplane_equiv; IN_UNION] THEN MESON_TAC[]);;
  45
  46 (* ------------------------------------------------------------------------- *)
  47 (* Cells of a hyperplane arrangement.                                        *)
  48 (* ------------------------------------------------------------------------- *)
  49
  50 let hyperplane_cell = new_definition
  51  `hyperplane_cell A c <=> ?x. c = hyperplane_equiv A x`;;
  52
  53 let HYPERPLANE_CELL = prove
  54  (`hyperplane_cell A c <=> ?x. c = {y | hyperplane_equiv A x y}`,
  55   REWRITE_TAC[EXTENSION; hyperplane_cell; IN_ELIM_THM; IN] THEN
  56   MESON_TAC[]);;
  57
  58 let NOT_HYPERPLANE_CELL_EMPTY = prove
  59  (`!A. ~(hyperplane_cell A {})`,
  60   REWRITE_TAC[hyperplane_cell; EXTENSION; NOT_IN_EMPTY] THEN
  61   MESON_TAC[HYPERPLANE_EQUIV_REFL; IN]);;
  62
  63 let NONEMPTY_HYPERPLANE_CELL = prove
  64  (`!A c. hyperplane_cell A c ==> ~(c = {})`,
  65   MESON_TAC[NOT_HYPERPLANE_CELL_EMPTY]);;
  66
  67 let UNIONS_HYPERPLANE_CELLS = prove
  68  (`!A. UNIONS {c | hyperplane_cell A c} = (:real^N)`,
  69   REWRITE_TAC[EXTENSION; IN_UNIONS; IN_UNIV; IN_ELIM_THM] THEN
  70   REWRITE_TAC[hyperplane_cell] THEN MESON_TAC[HYPERPLANE_EQUIV_REFL; IN]);;
  71
  72 let DISJOINT_HYPERPLANE_CELLS = prove
  73  (`!A c1 c2. hyperplane_cell A c1 /\ hyperplane_cell A c2 /\ ~(c1 = c2)
  74              ==> DISJOINT c1 c2`,
  75   REWRITE_TAC[hyperplane_cell] THEN REPEAT STRIP_TAC THEN
  76   FIRST_X_ASSUM(MP_TAC o check (is_neg o concl)) THEN
  77   ASM_REWRITE_TAC[IN_DISJOINT; IN; EXTENSION] THEN
  78   ASM_MESON_TAC[HYPERPLANE_EQUIV_TRANS; HYPERPLANE_EQUIV_SYM]);;
  79
  80 let DISJOINT_HYPERPLANE_CELLS_EQ = prove
  81  (`!A c1 c2. hyperplane_cell A c1 /\ hyperplane_cell A c2
  82              ==> (DISJOINT c1 c2 <=> ~(c1 = c2))`,
  83   MESON_TAC[NONEMPTY_HYPERPLANE_CELL; DISJOINT_HYPERPLANE_CELLS;
  84             SET_RULE `DISJOINT s s <=> s = {}`]);;
  85
  86 let HYPERPLANE_CELL_EMPTY = prove
  87  (`hyperplane_cell {} c <=> c = (:real^N)`,
  88   REWRITE_TAC[HYPERPLANE_CELL; NOT_IN_EMPTY; hyperplane_equiv] THEN
  89   SET_TAC[]);;
  90
  91 let HYPERPLANE_CELL_SING_CASES = prove
  92  (`!a b c:real^N->bool.
  93         hyperplane_cell {(a,b)} c
  94         ==>  c = {x | a dot x = b} \/
  95              c = {x | a dot x < b} \/
  96              c = {x | a dot x > b}`,
  97   REWRITE_TAC[HYPERPLANE_CELL; hyperplane_equiv] THEN
  98   REWRITE_TAC[FORALL_UNWIND_THM2; IN_SING; hyperplane_side] THEN
  99   REPEAT GEN_TAC THEN DISCH_THEN(X_CHOOSE_THEN `y:real^N` MP_TAC) THEN
 100   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV) [EQ_SYM_EQ] THEN
 101   REPEAT_TCL DISJ_CASES_THEN SUBST1_TAC
 102    (SPEC `(a:real^N) dot y - b` REAL_SGN_CASES) THEN
 103   ASM_REWRITE_TAC[REAL_SGN_EQ] THEN
 104   SIMP_TAC[REAL_SUB_0; REAL_SUB_LT; real_gt;
 105            REAL_ARITH `x - y < &0 <=> x < y`]);;
 106
 107 let HYPERPLANE_CELL_SING = prove
 108  (`!a b c.
 109         hyperplane_cell {(a,b)} c <=>
 110         if a = vec 0 then c = (:real^N)
 111         else c = {x | a dot x = b} \/
 112              c = {x | a dot x < b} \/
 113              c = {x | a dot x > b}`,
 114   REPEAT GEN_TAC THEN COND_CASES_TAC THENL
 115    [REWRITE_TAC[hyperplane_cell; hyperplane_equiv; EXTENSION; IN_UNIV] THEN
 116     REWRITE_TAC[IN] THEN REWRITE_TAC[hyperplane_equiv] THEN
 117     ASM_SIMP_TAC[IN_SING; FORALL_UNWIND_THM2] THEN
 118     REWRITE_TAC[hyperplane_side; DOT_LZERO];
 119     EQ_TAC THEN REWRITE_TAC[HYPERPLANE_CELL_SING_CASES] THEN STRIP_TAC THEN
 120     ASM_REWRITE_TAC[hyperplane_cell; EXTENSION; IN_ELIM_THM] THEN
 121     REWRITE_TAC[IN] THEN REWRITE_TAC[hyperplane_equiv] THEN
 122     ASM_SIMP_TAC[IN_SING; FORALL_UNWIND_THM2] THEN
 123     REWRITE_TAC[hyperplane_side] THEN
 124     ONCE_REWRITE_TAC[REAL_ARITH `a dot x = b <=> a dot x - b = &0`;
 125                      REAL_ARITH `a > b <=> a - b > &0`;
 126                      REAL_ARITH `a < b <=> a - b < &0`] THEN
 127     ONCE_REWRITE_TAC[GSYM REAL_SGN_EQ] THEN REWRITE_TAC[REAL_SUB_0] THEN
 128     MATCH_MP_TAC(MESON[]
 129      `(?x. f x = a) ==> (?x. !y. f y = a <=> f x = f y)`) THEN
 130     REWRITE_TAC[REAL_SGN_EQ] THENL
 131      [EXISTS_TAC `b / (a dot a) % a:real^N`;
 132       EXISTS_TAC `(b - &1) / (a dot a) % a:real^N`;
 133       EXISTS_TAC `(b + &1) / (a dot a) % a:real^N`] THEN
 134     ASM_SIMP_TAC[DOT_RMUL; REAL_DIV_RMUL; DOT_EQ_0] THEN REAL_ARITH_TAC]);;
 135
 136 let HYPERPLANE_CELL_UNION = prove
 137  (`!A B c:real^N->bool.
 138         hyperplane_cell (A UNION B) c <=>
 139         ~(c = {}) /\
 140         ?c1 c2. hyperplane_cell A c1 /\
 141                 hyperplane_cell B c2 /\
 142                 c = c1 INTER c2`,
 143   REPEAT GEN_TAC THEN ASM_CASES_TAC `c:real^N->bool = {}` THENL
 144    [ASM_MESON_TAC[NONEMPTY_HYPERPLANE_CELL]; ASM_REWRITE_TAC[]] THEN
 145   REWRITE_TAC[HYPERPLANE_CELL; HYPERPLANE_EQUIV_UNION] THEN
 146   REWRITE_TAC[SET_RULE `{x | P x /\ Q x} = {x | P x} INTER {x | Q x}`] THEN
 147   REWRITE_TAC[MESON[]
 148    `(?c1 c2. (?x. c1 = f x) /\ (?y. c2 = g y) /\ P c1 c2) <=>
 149     (?x y. P (f x) (g y))`] THEN
 150   EQ_TAC THENL [MESON_TAC[]; REWRITE_TAC[LEFT_IMP_EXISTS_THM]] THEN
 151   MAP_EVERY X_GEN_TAC [`a:real^N`; `b:real^N`] THEN
 152   DISCH_THEN SUBST_ALL_TAC THEN POP_ASSUM MP_TAC THEN
 153   REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN MATCH_MP_TAC MONO_EXISTS THEN
 154   X_GEN_TAC `x:real^N` THEN REWRITE_TAC[EXTENSION; IN_INTER; IN_ELIM_THM] THEN
 155   MESON_TAC[HYPERPLANE_EQUIV_TRANS; HYPERPLANE_EQUIV_SYM]);;
 156
 157 let FINITE_HYPERPLANE_CELLS = prove
 158  (`!A. FINITE A ==> FINITE {c:real^N->bool | hyperplane_cell A c}`,
 159   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 160   REWRITE_TAC[HYPERPLANE_CELL_EMPTY; SING_GSPEC; FINITE_SING] THEN
 161   REWRITE_TAC[FORALL_PAIR_THM] THEN
 162   MAP_EVERY X_GEN_TAC [`a:real^N`; `b:real`; `A:(real^N#real)->bool`] THEN
 163   STRIP_TAC THEN ONCE_REWRITE_TAC[SET_RULE `a INSERT s = {a} UNION s`] THEN
 164   REWRITE_TAC[HYPERPLANE_CELL_UNION] THEN MATCH_MP_TAC FINITE_SUBSET THEN
 165   EXISTS_TAC `{ c1 INTER c2:real^N->bool |
 166                 c1 IN {c | hyperplane_cell A c} /\
 167                 c2 IN {c | hyperplane_cell {(a,b)} c}}` THEN
 168   CONJ_TAC THENL
 169    [MATCH_MP_TAC FINITE_PRODUCT_DEPENDENT THEN
 170     ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN
 171     MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC
 172      `{{x:real^N | a dot x = b},{x | a dot x < b},{x | a dot x > b}}` THEN
 173     REWRITE_TAC[SUBSET; IN_SING; HYPERPLANE_CELL_SING_CASES; IN_ELIM_THM;
 174                 IN_INSERT; NOT_IN_EMPTY; FINITE_INSERT; FINITE_EMPTY];
 175     REWRITE_TAC[IN_ELIM_THM; SUBSET] THEN MESON_TAC[INTER_COMM]]);;
 176
 177 let FINITE_RESTRICT_HYPERPLANE_CELLS = prove
 178  (`!P A. FINITE A ==> FINITE {c:real^N->bool | hyperplane_cell A c /\ P c}`,
 179   REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN
 180   EXISTS_TAC `{c:real^N->bool | hyperplane_cell A c}` THEN
 181   ASM_SIMP_TAC[FINITE_HYPERPLANE_CELLS] THEN SET_TAC[]);;
 182
 183 let FINITE_SET_OF_HYPERPLANE_CELLS = prove
 184  (`!A C. FINITE A /\ (!c:real^N->bool. c IN C ==> hyperplane_cell A c)
 185          ==> FINITE C`,
 186   REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN
 187   EXISTS_TAC `{c:real^N->bool | hyperplane_cell A c}` THEN
 188   ASM_SIMP_TAC[FINITE_HYPERPLANE_CELLS] THEN ASM SET_TAC[]);;
 189
 190 let PAIRWISE_DISJOINT_HYPERPLANE_CELLS = prove
 191  (`!A C. (!c. c IN C ==> hyperplane_cell A c)
 192          ==> pairwise DISJOINT C`,
 193   REWRITE_TAC[pairwise] THEN MESON_TAC[DISJOINT_HYPERPLANE_CELLS]);;
 194
 195 let HYPERPLANE_CELL_INTER_OPEN_AFFINE = prove
 196  (`!A c:real^N->bool.
 197         FINITE A /\ hyperplane_cell A c
 198         ==> ?s t. open s /\ affine t /\ c = s INTER t`,
 199   REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
 200   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN CONJ_TAC THENL
 201    [REWRITE_TAC[HYPERPLANE_CELL_EMPTY] THEN REPEAT STRIP_TAC THEN
 202     REPEAT(EXISTS_TAC `(:real^N)`) THEN
 203     ASM_REWRITE_TAC[AFFINE_UNIV; OPEN_UNIV; INTER_UNIV];
 204     ALL_TAC] THEN
 205   REWRITE_TAC[FORALL_PAIR_THM] THEN
 206   MAP_EVERY X_GEN_TAC [`a:real^N`; `b:real`; `A:real^N#real->bool`] THEN
 207   STRIP_TAC THEN ONCE_REWRITE_TAC[SET_RULE `a INSERT s = {a} UNION s`] THEN
 208   REWRITE_TAC[HYPERPLANE_CELL_UNION] THEN X_GEN_TAC `c':real^N->bool` THEN
 209   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 210   REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 211   MAP_EVERY X_GEN_TAC [`c1:real^N->bool`; `c:real^N->bool`] THEN
 212   DISCH_THEN(CONJUNCTS_THEN2 MP_TAC
 213    (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC)) THEN
 214   FIRST_X_ASSUM(MP_TAC o SPEC `c:real^N->bool`) THEN
 215   ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 216   MAP_EVERY X_GEN_TAC [`s:real^N->bool`; `t:real^N->bool`] THEN
 217   STRIP_TAC THEN REWRITE_TAC[HYPERPLANE_CELL_SING] THEN
 218   COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
 219   REPEAT(FIRST_X_ASSUM SUBST_ALL_TAC) THENL
 220    [MAP_EVERY EXISTS_TAC [`s:real^N->bool`; `t:real^N->bool`] THEN
 221     ASM_REWRITE_TAC[INTER_UNIV];
 222     MAP_EVERY EXISTS_TAC
 223      [`s:real^N->bool`; `{x:real^N | a dot x = b} INTER t`] THEN
 224     ASM_REWRITE_TAC[INTER_ACI] THEN MATCH_MP_TAC AFFINE_INTER THEN
 225     ASM_REWRITE_TAC[AFFINE_HYPERPLANE];
 226     MAP_EVERY EXISTS_TAC
 227      [`{x:real^N | a dot x < b} INTER s`; `t:real^N->bool`] THEN
 228     ASM_REWRITE_TAC[INTER_ACI] THEN MATCH_MP_TAC OPEN_INTER THEN
 229     ASM_REWRITE_TAC[OPEN_HALFSPACE_LT];
 230     MAP_EVERY EXISTS_TAC
 231      [`{x:real^N | a dot x > b} INTER s`; `t:real^N->bool`] THEN
 232     ASM_REWRITE_TAC[INTER_ACI] THEN MATCH_MP_TAC OPEN_INTER THEN
 233     ASM_REWRITE_TAC[OPEN_HALFSPACE_GT]]);;
 234
 235 let HYPERPLANE_CELL_RELATIVELY_OPEN = prove
 236  (`!A c:real^N->bool.
 237         FINITE A /\ hyperplane_cell A c
 238         ==> open_in (subtopology euclidean (affine hull c)) c`,
 239   REPEAT GEN_TAC THEN DISCH_TAC THEN
 240   FIRST_ASSUM(MP_TAC o MATCH_MP HYPERPLANE_CELL_INTER_OPEN_AFFINE) THEN
 241   REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 242   MAP_EVERY X_GEN_TAC [`s:real^N->bool`; `t:real^N->bool`] THEN
 243   STRIP_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN
 244   ASM_CASES_TAC `s INTER t:real^N->bool = {}` THEN
 245   ASM_REWRITE_TAC[OPEN_IN_EMPTY] THEN
 246   SUBGOAL_THEN `affine hull (s INTER t:real^N->bool) = t`
 247   SUBST1_TAC THENL
 248    [MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `affine hull t:real^N->bool` THEN
 249     ASM_REWRITE_TAC[AFFINE_HULL_EQ] THEN
 250     MATCH_MP_TAC(ONCE_REWRITE_RULE[INTER_COMM]
 251       AFFINE_HULL_CONVEX_INTER_OPEN) THEN
 252     ASM_SIMP_TAC[AFFINE_IMP_CONVEX];
 253     ONCE_REWRITE_TAC[INTER_COMM] THEN ASM_SIMP_TAC[OPEN_IN_OPEN_INTER]]);;
 254
 255 let HYPERPLANE_CELL_RELATIVE_INTERIOR = prove
 256  (`!A c:real^N->bool.
 257         FINITE A /\ hyperplane_cell A c
 258         ==> relative_interior c = c`,
 259   MESON_TAC[RELATIVE_INTERIOR_OPEN_IN; HYPERPLANE_CELL_RELATIVELY_OPEN]);;
 260
 261 let HYPERPLANE_CELL_CONVEX = prove
 262  (`!A c:real^N->bool. hyperplane_cell A c ==> convex c`,
 263   REPEAT GEN_TAC THEN REWRITE_TAC[HYPERPLANE_CELL] THEN
 264   DISCH_THEN(X_CHOOSE_THEN `c:real^N` SUBST1_TAC) THEN
 265   REWRITE_TAC[hyperplane_equiv] THEN
 266   ONCE_REWRITE_TAC[SET_RULE `f x = f y <=> y IN {y | f x = f y}`] THEN
 267   REWRITE_TAC[GSYM INTERS_IMAGE] THEN MATCH_MP_TAC CONVEX_INTERS THEN
 268   REWRITE_TAC[FORALL_IN_IMAGE] THEN REWRITE_TAC[FORALL_PAIR_THM] THEN
 269   MAP_EVERY X_GEN_TAC [`a:real^N`; `b:real`] THEN DISCH_TAC THEN
 270   CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN REWRITE_TAC[hyperplane_side] THEN
 271   REPEAT_TCL DISJ_CASES_THEN SUBST1_TAC
 272    (SPEC `(a:real^N) dot c - b` REAL_SGN_CASES) THEN
 273   ASM_REWRITE_TAC[REAL_SGN_EQ] THEN
 274   SIMP_TAC[REAL_SUB_0; REAL_ARITH `a - b > &0 <=> a > b`;
 275            REAL_ARITH `a - b < &0 <=> a < b`] THEN
 276   REWRITE_TAC[CONVEX_HALFSPACE_LT; CONVEX_HALFSPACE_GT;
 277               CONVEX_HYPERPLANE]);;
 278
 279 let HYPERPLANE_CELL_INTERS = prove
 280  (`!A C. (!c:real^N->bool. c IN C ==> hyperplane_cell A c) /\
 281          ~(C = {}) /\ ~(INTERS C = {})
 282          ==> hyperplane_cell A (INTERS C)`,
 283   REPEAT GEN_TAC THEN REWRITE_TAC[HYPERPLANE_CELL; GSYM MEMBER_NOT_EMPTY] THEN
 284   REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
 285   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `z:real^N` THEN
 286   REWRITE_TAC[IN_INTERS] THEN DISCH_TAC THEN
 287   GEN_REWRITE_TAC I [EXTENSION] THEN
 288   REWRITE_TAC[IN_INTERS; IN_ELIM_THM] THEN
 289   X_GEN_TAC `x:real^N` THEN EQ_TAC THEN DISCH_TAC THENL
 290    [FIRST_X_ASSUM(X_CHOOSE_TAC `c:real^N->bool`);
 291     X_GEN_TAC `c:real^N->bool` THEN DISCH_TAC] THEN
 292   REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `c:real^N->bool`)) THEN
 293   ASM_REWRITE_TAC[] THEN REPEAT DISCH_TAC THEN
 294   FIRST_X_ASSUM(CHOOSE_THEN SUBST_ALL_TAC) THEN
 295   RULE_ASSUM_TAC(REWRITE_RULE[IN_ELIM_THM]) THEN SIMP_TAC[IN_ELIM_THM] THEN
 296   ASM_MESON_TAC[HYPERPLANE_EQUIV_SYM; HYPERPLANE_EQUIV_TRANS]);;
 297
 298 let HYPERPLANE_CELL_INTER = prove
 299  (`!A s t:real^N->bool.
 300         hyperplane_cell A s /\ hyperplane_cell A t /\ ~(s INTER t = {})
 301         ==> hyperplane_cell A (s INTER t)`,
 302   REWRITE_TAC[GSYM INTERS_2] THEN REPEAT STRIP_TAC THEN
 303   MATCH_MP_TAC HYPERPLANE_CELL_INTERS THEN
 304   ASM_REWRITE_TAC[FORALL_IN_INSERT; NOT_IN_EMPTY; NOT_INSERT_EMPTY]);;
 305
 306 (* ------------------------------------------------------------------------- *)
 307 (* A cell complex is considered to be a union of such cells.                 *)
 308 (* ------------------------------------------------------------------------- *)
 309
 310 let hyperplane_cellcomplex = new_definition
 311  `hyperplane_cellcomplex A s <=>
 312         ?t. (!c. c IN t ==> hyperplane_cell A c) /\
 313             s = UNIONS t`;;
 314
 315 let HYPERPLANE_CELLCOMPLEX_EMPTY = prove
 316  (`!A:real^N#real->bool. hyperplane_cellcomplex A {}`,
 317   GEN_TAC THEN REWRITE_TAC[hyperplane_cellcomplex] THEN
 318   EXISTS_TAC `{}:(real^N->bool)->bool` THEN
 319   REWRITE_TAC[NOT_IN_EMPTY; UNIONS_0]);;
 320
 321 let HYPERPLANE_CELL_CELLCOMPLEX = prove
 322  (`!A c:real^N->bool. hyperplane_cell A c ==> hyperplane_cellcomplex A c`,
 323   REPEAT STRIP_TAC THEN REWRITE_TAC[hyperplane_cellcomplex] THEN
 324   EXISTS_TAC `{c:real^N->bool}` THEN
 325   ASM_SIMP_TAC[IN_SING; UNIONS_1]);;
 326
 327 let HYPERPLANE_CELLCOMPLEX_UNIONS = prove
 328  (`!A C. (!s:real^N->bool. s IN C ==> hyperplane_cellcomplex A s)
 329          ==> hyperplane_cellcomplex A (UNIONS C)`,
 330   REPEAT GEN_TAC THEN REWRITE_TAC[hyperplane_cellcomplex] THEN
 331   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [RIGHT_IMP_EXISTS_THM] THEN
 332   REWRITE_TAC[SKOLEM_THM; LEFT_IMP_EXISTS_THM] THEN
 333   X_GEN_TAC `f:(real^N->bool)->(real^N->bool)->bool` THEN DISCH_TAC THEN
 334   EXISTS_TAC `UNIONS (IMAGE (f:(real^N->bool)->(real^N->bool)->bool) C)` THEN
 335   REWRITE_TAC[FORALL_IN_UNIONS; IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
 336   REWRITE_TAC[FORALL_IN_IMAGE] THEN
 337   CONJ_TAC THENL [ASM_MESON_TAC[]; REWRITE_TAC[UNIONS_IMAGE]] THEN
 338   GEN_REWRITE_TAC I [EXTENSION] THEN REWRITE_TAC[IN_UNIONS; IN_ELIM_THM] THEN
 339   ASM SET_TAC[]);;
 340
 341 let HYPERPLANE_CELLCOMPLEX_UNION = prove
 342  (`!A s t.
 343         hyperplane_cellcomplex A s /\ hyperplane_cellcomplex A t
 344         ==> hyperplane_cellcomplex A (s UNION t)`,
 345   REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM UNIONS_2] THEN
 346   MATCH_MP_TAC HYPERPLANE_CELLCOMPLEX_UNIONS THEN
 347   ASM_REWRITE_TAC[FORALL_IN_INSERT; NOT_IN_EMPTY]);;
 348
 349 let HYPERPLANE_CELLCOMPLEX_UNIV = prove
 350  (`!A. hyperplane_cellcomplex A (:real^N)`,
 351   REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM UNIONS_HYPERPLANE_CELLS] THEN
 352   MATCH_MP_TAC HYPERPLANE_CELLCOMPLEX_UNIONS THEN
 353   REWRITE_TAC[IN_ELIM_THM; HYPERPLANE_CELL_CELLCOMPLEX]);;
 354
 355 let HYPERPLANE_CELLCOMPLEX_INTERS = prove
 356  (`!A C. (!s:real^N->bool. s IN C ==> hyperplane_cellcomplex A s)
 357          ==> hyperplane_cellcomplex A (INTERS C)`,
 358   let lemma = prove
 359    (`UNIONS s = UNIONS {t | t IN s /\ ~(t = {})}`,
 360     REWRITE_TAC[UNIONS_GSPEC] THEN GEN_REWRITE_TAC I [EXTENSION] THEN
 361     REWRITE_TAC[IN_UNIONS; IN_ELIM_THM] THEN MESON_TAC[NOT_IN_EMPTY]) in
 362   REPEAT GEN_TAC THEN ASM_CASES_TAC `C:(real^N->bool)->bool = {}` THEN
 363   ASM_REWRITE_TAC[INTERS_0; HYPERPLANE_CELLCOMPLEX_UNIV] THEN
 364   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [hyperplane_cellcomplex] THEN
 365   REWRITE_TAC[RIGHT_IMP_EXISTS_THM; SKOLEM_THM; LEFT_IMP_EXISTS_THM] THEN
 366   X_GEN_TAC `f:(real^N->bool)->(real^N->bool)->bool` THEN
 367   DISCH_TAC THEN SUBGOAL_THEN
 368    `C = {UNIONS((f:(real^N->bool)->(real^N->bool)->bool) s) | s IN C}`
 369   SUBST1_TAC THENL
 370    [GEN_REWRITE_TAC I [EXTENSION] THEN REWRITE_TAC[IN_ELIM_THM] THEN
 371     ASM_MESON_TAC[];
 372     ALL_TAC] THEN
 373   REWRITE_TAC[INTERS_OVER_UNIONS] THEN ONCE_REWRITE_TAC[lemma] THEN
 374   MATCH_MP_TAC HYPERPLANE_CELLCOMPLEX_UNIONS THEN
 375   REWRITE_TAC[FORALL_IN_GSPEC; IMP_CONJ] THEN REPEAT STRIP_TAC THEN
 376   MATCH_MP_TAC HYPERPLANE_CELL_CELLCOMPLEX THEN
 377   MATCH_MP_TAC HYPERPLANE_CELL_INTERS THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN
 378   CONJ_TAC THENL [ASM_MESON_TAC[]; ASM SET_TAC[]]);;
 379
 380 let HYPERPLANE_CELLCOMPLEX_INTER = prove
 381  (`!A s t.
 382         hyperplane_cellcomplex A s /\ hyperplane_cellcomplex A t
 383         ==> hyperplane_cellcomplex A (s INTER t)`,
 384   REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM INTERS_2] THEN
 385   MATCH_MP_TAC HYPERPLANE_CELLCOMPLEX_INTERS THEN
 386   ASM_REWRITE_TAC[FORALL_IN_INSERT; NOT_IN_EMPTY]);;
 387
 388 let HYPERPLANE_CELLCOMPLEX_COMPL = prove
 389  (`!A s. hyperplane_cellcomplex A s
 390          ==> hyperplane_cellcomplex A ((:real^N) DIFF s)`,
 391   REPEAT GEN_TAC THEN
 392   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [hyperplane_cellcomplex] THEN
 393   REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 394   X_GEN_TAC `C:(real^N->bool)->bool` THEN STRIP_TAC THEN
 395   ASM_REWRITE_TAC[UNIONS_INTERS; SET_RULE `UNIV DIFF (UNIV DIFF s) = s`] THEN
 396   MATCH_MP_TAC HYPERPLANE_CELLCOMPLEX_INTERS THEN
 397   REWRITE_TAC[FORALL_IN_GSPEC] THEN
 398   X_GEN_TAC `c:real^N->bool` THEN DISCH_TAC THEN
 399   SUBGOAL_THEN
 400    `(:real^N) DIFF c = UNIONS {c' | hyperplane_cell A c' /\ ~(c' = c)}`
 401   SUBST1_TAC THENL
 402    [SUBST1_TAC(SYM(ISPEC `A:real^N#real->bool` UNIONS_HYPERPLANE_CELLS)) THEN
 403     GEN_REWRITE_TAC I [EXTENSION] THEN
 404     REWRITE_TAC[IN_DIFF; UNIONS_GSPEC; IN_ELIM_THM] THEN
 405     X_GEN_TAC `x:real^N` THEN REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
 406     AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN
 407     X_GEN_TAC `c':real^N->bool` THEN REWRITE_TAC[] THEN
 408     MP_TAC(ISPECL [`A:real^N#real->bool`; `c:real^N->bool`; `c':real^N->bool`]
 409         DISJOINT_HYPERPLANE_CELLS_EQ) THEN
 410     ASM_SIMP_TAC[] THEN SET_TAC[];
 411     MATCH_MP_TAC HYPERPLANE_CELLCOMPLEX_UNIONS THEN
 412     ASM_SIMP_TAC[HYPERPLANE_CELL_CELLCOMPLEX; IN_ELIM_THM]]);;
 413
 414 let HYPERPLANE_CELLCOMPLEX_DIFF = prove
 415  (`!A s t.
 416         hyperplane_cellcomplex A s /\ hyperplane_cellcomplex A t
 417         ==> hyperplane_cellcomplex A (s DIFF t)`,
 418   ONCE_REWRITE_TAC[SET_RULE `s DIFF t = s INTER (UNIV DIFF t)`] THEN
 419   SIMP_TAC[HYPERPLANE_CELLCOMPLEX_COMPL; HYPERPLANE_CELLCOMPLEX_INTER]);;
 420
 421 let HYPERPLANE_CELLCOMPLEX_MONO = prove
 422  (`!A B s:real^N->bool.
 423         hyperplane_cellcomplex A s /\ A SUBSET B
 424         ==> hyperplane_cellcomplex B s`,
 425   REPEAT STRIP_TAC THEN
 426   FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [hyperplane_cellcomplex]) THEN
 427   DISCH_THEN(X_CHOOSE_THEN `C:(real^N->bool)->bool` STRIP_ASSUME_TAC) THEN
 428   FIRST_X_ASSUM SUBST_ALL_TAC THEN
 429   MATCH_MP_TAC HYPERPLANE_CELLCOMPLEX_UNIONS THEN
 430   X_GEN_TAC `c:real^N->bool` THEN DISCH_TAC THEN
 431   FIRST_X_ASSUM(MP_TAC o SPEC `c:real^N->bool`) THEN
 432   ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 433   SUBGOAL_THEN `B:(real^N#real)->bool = A UNION (B DIFF A)` SUBST1_TAC THENL
 434    [ASM SET_TAC[]; ALL_TAC] THEN
 435   REWRITE_TAC[hyperplane_cellcomplex; HYPERPLANE_CELL_UNION] THEN
 436   EXISTS_TAC `{c' INTER c:real^N->bool |c'| hyperplane_cell (B DIFF A) c' /\
 437                                             ~(c' INTER c = {})}` THEN
 438   REWRITE_TAC[FORALL_IN_GSPEC] THEN CONJ_TAC THENL
 439    [X_GEN_TAC `c':real^N->bool` THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 440     MAP_EVERY EXISTS_TAC [`c:real^N->bool`; `c':real^N->bool`] THEN
 441     ASM_REWRITE_TAC[INTER_COMM];
 442     GEN_REWRITE_TAC I [EXTENSION] THEN
 443     REWRITE_TAC[UNIONS_GSPEC; IN_ELIM_THM; IN_INTER] THEN
 444     X_GEN_TAC `x:real^N` THEN EQ_TAC THENL [DISCH_TAC; MESON_TAC[]] THEN
 445     MP_TAC(ISPEC `B DIFF A:(real^N#real)->bool` UNIONS_HYPERPLANE_CELLS) THEN
 446     GEN_REWRITE_TAC LAND_CONV [EXTENSION] THEN
 447     REWRITE_TAC[IN_UNIONS; IN_ELIM_THM; IN_UNIV] THEN ASM SET_TAC[]]);;
 448
 449 let FINITE_HYPERPLANE_CELLCOMPLEXES = prove
 450  (`!A. FINITE A ==> FINITE {c:real^N->bool | hyperplane_cellcomplex A c}`,
 451   REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC
 452    `IMAGE UNIONS {t | t SUBSET {c:real^N->bool | hyperplane_cell A c}}` THEN
 453   ASM_SIMP_TAC[FINITE_IMAGE; FINITE_POWERSET; FINITE_HYPERPLANE_CELLS] THEN
 454   REWRITE_TAC[SUBSET; IN_IMAGE; IN_ELIM_THM; hyperplane_cellcomplex] THEN
 455   MESON_TAC[]);;
 456
 457 let FINITE_RESTRICT_HYPERPLANE_CELLCOMPLEXES = prove
 458  (`!P A. FINITE A
 459          ==> FINITE {c:real^N->bool | hyperplane_cellcomplex A c /\ P c}`,
 460   REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN
 461   EXISTS_TAC `{c:real^N->bool | hyperplane_cellcomplex A c}` THEN
 462   ASM_SIMP_TAC[FINITE_HYPERPLANE_CELLCOMPLEXES] THEN SET_TAC[]);;
 463
 464 let FINITE_SET_OF_HYPERPLANE_CELLS = prove
 465  (`!A C. FINITE A /\ (!c:real^N->bool. c IN C ==> hyperplane_cellcomplex A c)
 466          ==> FINITE C`,
 467   REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN
 468   EXISTS_TAC `{c:real^N->bool | hyperplane_cellcomplex A c}` THEN
 469   ASM_SIMP_TAC[FINITE_HYPERPLANE_CELLCOMPLEXES] THEN ASM SET_TAC[]);;
 470
 471 let CELL_SUBSET_CELLCOMPLEX = prove
 472  (`!A s c:real^N->bool.
 473         hyperplane_cell A c /\ hyperplane_cellcomplex A s
 474         ==> (c SUBSET s <=> ~(DISJOINT c s))`,
 475   REPEAT STRIP_TAC THEN
 476   FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [hyperplane_cellcomplex]) THEN
 477   DISCH_THEN(X_CHOOSE_THEN `C:(real^N->bool)->bool` STRIP_ASSUME_TAC) THEN
 478   FIRST_X_ASSUM SUBST_ALL_TAC THEN EQ_TAC THENL
 479    [ASM_CASES_TAC `c:real^N->bool = {}` THENL
 480      [ASM_MESON_TAC[NONEMPTY_HYPERPLANE_CELL]; ASM SET_TAC[]];
 481     REWRITE_TAC[DISJOINT; INTER_UNIONS; GSYM MEMBER_NOT_EMPTY] THEN
 482     REWRITE_TAC[UNIONS_GSPEC; IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN
 483     MAP_EVERY X_GEN_TAC [`x:real^N`; `c':real^N->bool`] THEN
 484     REWRITE_TAC[IN_INTER] THEN STRIP_TAC THEN
 485     MP_TAC(ISPECL [`A:(real^N#real)->bool`; `c:real^N->bool`;
 486       `c':real^N->bool`] DISJOINT_HYPERPLANE_CELLS_EQ) THEN
 487     ASM_SIMP_TAC[] THEN
 488     ASM_CASES_TAC `c':real^N->bool = c` THENL
 489      [DISCH_THEN(K ALL_TAC); ASM SET_TAC[]] THEN
 490     MATCH_MP_TAC(SET_RULE `c IN C ==> c SUBSET UNIONS C`) THEN
 491     ASM_MESON_TAC[]]);;
 492
 493 (* ------------------------------------------------------------------------- *)
 494 (* Euler characteristic.                                                     *)
 495 (* ------------------------------------------------------------------------- *)
 496
 497 let euler_characteristic = new_definition
 498  `euler_characteristic A (s:real^N->bool) =
 499         sum {c | hyperplane_cell A c /\ c SUBSET s}
 500             (\c. (-- &1) pow (num_of_int(aff_dim c)))`;;
 501
 502 let EULER_CHARACTERISTIC_EMPTY = prove
 503  (`euler_characteristic A {} = &0`,
 504   REWRITE_TAC[euler_characteristic; SUBSET_EMPTY] THEN
 505   MATCH_MP_TAC SUM_EQ_0 THEN
 506   MATCH_MP_TAC(MESON[] `~(?x. x IN s) ==> (!x. x IN s ==> P x)`) THEN
 507   REWRITE_TAC[IN_ELIM_THM] THEN MESON_TAC[NONEMPTY_HYPERPLANE_CELL]);;
 508
 509 let EULER_CHARACTERISTIC_CELL_UNIONS = prove
 510  (`!A C. (!c:real^N->bool. c IN C ==> hyperplane_cell A c)
 511          ==> euler_characteristic A (UNIONS C) =
 512              sum C (\c. (-- &1) pow (num_of_int(aff_dim c)))`,
 513   REPEAT STRIP_TAC THEN REWRITE_TAC[euler_characteristic] THEN
 514   MATCH_MP_TAC(MESON[] `s = t ==> sum s f = sum t f`) THEN
 515   REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN X_GEN_TAC `c:real^N->bool` THEN
 516   EQ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
 517   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 518   SUBGOAL_THEN `~(c:real^N->bool = {})` MP_TAC THENL
 519    [ASM_MESON_TAC[NONEMPTY_HYPERPLANE_CELL]; ALL_TAC] THEN
 520   REWRITE_TAC[MEMBER_NOT_EMPTY; SUBSET; IN_UNIONS] THEN
 521   REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; LEFT_IMP_EXISTS_THM] THEN
 522   X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
 523   DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN
 524   DISCH_THEN(X_CHOOSE_THEN `c':real^N->bool` STRIP_ASSUME_TAC) THEN
 525   SUBGOAL_THEN `~(DISJOINT (c:real^N->bool) c')` MP_TAC THENL
 526    [ASM SET_TAC[]; ASM_MESON_TAC[DISJOINT_HYPERPLANE_CELLS_EQ]]);;
 527
 528 let EULER_CHARACTERISTIC_CELL = prove
 529  (`!A c. hyperplane_cell A c
 530          ==> euler_characteristic A c =  (-- &1) pow (num_of_int(aff_dim c))`,
 531   REPEAT STRIP_TAC THEN
 532   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM UNIONS_1] THEN
 533   ASM_SIMP_TAC[EULER_CHARACTERISTIC_CELL_UNIONS; IN_SING; SUM_SING]);;
 534
 535 let EULER_CHARACTERISTIC_CELLCOMPLEX_UNION = prove
 536  (`!A s t:real^N->bool.
 537         FINITE A /\
 538         hyperplane_cellcomplex A s /\
 539         hyperplane_cellcomplex A t /\
 540         DISJOINT s t
 541         ==> euler_characteristic A (s UNION t) =
 542             euler_characteristic A s + euler_characteristic A t`,
 543   REPEAT STRIP_TAC THEN REWRITE_TAC[euler_characteristic] THEN
 544   CONV_TAC SYM_CONV THEN MATCH_MP_TAC SUM_UNION_EQ THEN
 545   ASM_SIMP_TAC[FINITE_RESTRICT_HYPERPLANE_CELLS] THEN
 546   REWRITE_TAC[EXTENSION; IN_INTER; IN_ELIM_THM; NOT_IN_EMPTY; IN_UNION] THEN
 547   CONJ_TAC THEN X_GEN_TAC `c:real^N->bool` THENL
 548    [ASM_CASES_TAC `c:real^N->bool = {}` THENL
 549      [ASM_MESON_TAC[NONEMPTY_HYPERPLANE_CELL]; ASM SET_TAC[]];
 550     ASM_CASES_TAC `hyperplane_cell A (c:real^N->bool)` THEN
 551     ASM_REWRITE_TAC[] THEN
 552     MP_TAC(ISPEC `A:(real^N#real)->bool` CELL_SUBSET_CELLCOMPLEX) THEN
 553     ASM_SIMP_TAC[HYPERPLANE_CELLCOMPLEX_UNION] THEN SET_TAC[]]);;
 554
 555 let EULER_CHARACTERISTIC_CELLCOMPLEX_UNIONS = prove
 556  (`!A C. FINITE A /\
 557          (!c:real^N->bool. c IN C ==> hyperplane_cellcomplex A c) /\
 558          pairwise DISJOINT C
 559          ==> euler_characteristic A (UNIONS C) =
 560              sum C (\c. euler_characteristic A c)`,
 561   REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 562   ASM_CASES_TAC `FINITE(C:(real^N->bool)->bool)` THENL
 563    [UNDISCH_TAC `FINITE(C:(real^N->bool)->bool)`;
 564     ASM_MESON_TAC[FINITE_SET_OF_HYPERPLANE_CELLS]] THEN
 565   SPEC_TAC(`C:(real^N->bool)->bool`,`C:(real^N->bool)->bool`) THEN
 566   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 567   SIMP_TAC[EULER_CHARACTERISTIC_EMPTY; SUM_CLAUSES; UNIONS_0] THEN
 568   REPEAT STRIP_TAC THEN REWRITE_TAC[UNIONS_INSERT] THEN
 569   W(MP_TAC o PART_MATCH (lhs o rand) EULER_CHARACTERISTIC_CELLCOMPLEX_UNION o
 570         lhs o snd) THEN
 571   ANTS_TAC THENL
 572    [ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL
 573      [ASM SET_TAC[];
 574       MATCH_MP_TAC HYPERPLANE_CELLCOMPLEX_UNIONS THEN ASM SET_TAC[];
 575       FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [pairwise]) THEN
 576       REWRITE_TAC[DISJOINT; INTER_UNIONS; IMP_CONJ; RIGHT_FORALL_IMP_THM;
 577                   FORALL_IN_INSERT; EMPTY_UNIONS; FORALL_IN_GSPEC] THEN
 578       ASM_MESON_TAC[INTER_COMM]];
 579     DISCH_THEN SUBST1_TAC THEN AP_TERM_TAC THEN
 580     FIRST_X_ASSUM MATCH_MP_TAC THEN
 581     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [pairwise]) THEN
 582     ASM_REWRITE_TAC[pairwise] THEN ASM SET_TAC[]]);;
 583
 584 let EULER_CHARACTERISTIC = prove
 585  (`!A s:real^N->bool.
 586         FINITE A
 587         ==> euler_characteristic A s =
 588             sum (0..dimindex(:N))
 589                 (\d. (-- &1) pow d *
 590                      &(CARD {c | hyperplane_cell A c /\ c SUBSET s /\
 591                                  aff_dim c = &d}))`,
 592   REPEAT STRIP_TAC THEN REWRITE_TAC[euler_characteristic] THEN
 593   MP_TAC(ISPECL [`\c:real^N->bool. aff_dim c`;
 594                  `\c:real^N->bool. (-- &1) pow (num_of_int(aff_dim c))`;
 595                  `{c:real^N->bool | hyperplane_cell A c /\ c SUBSET s}`;
 596                  `IMAGE int_of_num (0..dimindex(:N))`]
 597                 SUM_GROUP) THEN
 598   SIMP_TAC[SUM_IMAGE; INT_OF_NUM_EQ; o_DEF; NUM_OF_INT_OF_NUM] THEN
 599   ANTS_TAC THENL
 600    [ASM_SIMP_TAC[FINITE_RESTRICT_HYPERPLANE_CELLS] THEN
 601     GEN_REWRITE_TAC I [SUBSET] THEN
 602     REWRITE_TAC[FORALL_IN_IMAGE; IN_ELIM_THM] THEN
 603     X_GEN_TAC `c:real^N->bool` THEN STRIP_TAC THEN
 604     REWRITE_TAC[IN_IMAGE; IN_NUMSEG; LE_0] THEN
 605     REWRITE_TAC[GSYM INT_OF_NUM_LE; INT_EXISTS_POS] THEN
 606     EXISTS_TAC `aff_dim(c:real^N->bool)` THEN
 607     REWRITE_TAC[AFF_DIM_LE_UNIV; AFF_DIM_POS_LE] THEN
 608     ASM_MESON_TAC[NONEMPTY_HYPERPLANE_CELL];
 609     DISCH_THEN(SUBST1_TAC o SYM) THEN
 610     REWRITE_TAC[IN_ELIM_THM; GSYM CONJ_ASSOC] THEN
 611     ASM_SIMP_TAC[SUM_CONST; FINITE_RESTRICT_HYPERPLANE_CELLS] THEN
 612     REWRITE_TAC[REAL_MUL_AC]]);;
 613
 614 (* ------------------------------------------------------------------------- *)
 615 (* Show that the characteristic is invariant w.r.t. hyperplane arrangement.  *)
 616 (* ------------------------------------------------------------------------- *)
 617
 618 let HYPERPLANE_CELLS_DISTINCT_LEMMA = prove
 619  (`!a b. {x | a dot x = b} INTER {x | a dot x < b} = {} /\
 620          {x | a dot x = b} INTER {x | a dot x > b} = {} /\
 621          {x | a dot x < b} INTER {x | a dot x = b} = {} /\
 622          {x | a dot x < b} INTER {x | a dot x > b} = {} /\
 623          {x | a dot x > b} INTER {x | a dot x = b} = {} /\
 624          {x | a dot x > b} INTER {x | a dot x < b} = {}`,
 625   REWRITE_TAC[EXTENSION; IN_INTER; IN_ELIM_THM; NOT_IN_EMPTY] THEN
 626   REAL_ARITH_TAC);;
 627
 628 let EULER_CHARACTERSTIC_LEMMA = prove
 629  (`!A h s:real^N->bool.
 630         FINITE A /\ hyperplane_cellcomplex A s
 631         ==> euler_characteristic (h INSERT A) s = euler_characteristic A s`,
 632   REWRITE_TAC[FORALL_PAIR_THM] THEN MAP_EVERY X_GEN_TAC
 633    [`A:(real^N#real)->bool`; `a:real^N`; `b:real`; `s:real^N->bool`] THEN
 634   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 635   REWRITE_TAC[hyperplane_cellcomplex] THEN
 636   DISCH_THEN(X_CHOOSE_THEN `C:(real^N->bool)->bool` STRIP_ASSUME_TAC) THEN
 637   FIRST_X_ASSUM SUBST_ALL_TAC THEN
 638   SUBGOAL_THEN
 639    `!c:real^N->bool. c IN C ==> hyperplane_cellcomplex A c /\
 640                                 hyperplane_cellcomplex ((a,b) INSERT A) c`
 641   ASSUME_TAC THENL
 642    [REPEAT STRIP_TAC THEN ASM_SIMP_TAC[HYPERPLANE_CELL_CELLCOMPLEX] THEN
 643     MATCH_MP_TAC HYPERPLANE_CELLCOMPLEX_MONO THEN
 644     EXISTS_TAC `A:(real^N#real)->bool` THEN
 645     ASM_SIMP_TAC[HYPERPLANE_CELL_CELLCOMPLEX] THEN SET_TAC[];
 646     ALL_TAC] THEN
 647   SUBGOAL_THEN `pairwise DISJOINT (C:(real^N->bool)->bool)` ASSUME_TAC THENL
 648    [ASM_MESON_TAC[PAIRWISE_DISJOINT_HYPERPLANE_CELLS]; ALL_TAC] THEN
 649   ASM_SIMP_TAC[EULER_CHARACTERISTIC_CELLCOMPLEX_UNIONS; FINITE_INSERT] THEN
 650   MATCH_MP_TAC SUM_EQ THEN X_GEN_TAC `c:real^N->bool` THEN DISCH_TAC THEN
 651   ASM_CASES_TAC `hyperplane_cell ((a,b) INSERT A) (c:real^N->bool)` THEN
 652   ASM_SIMP_TAC[EULER_CHARACTERISTIC_CELL] THEN
 653   SUBGOAL_THEN `~(a:real^N = vec 0)` ASSUME_TAC THENL
 654    [FIRST_X_ASSUM(MP_TAC o check (is_neg o concl)) THEN
 655     SIMP_TAC[CONTRAPOS_THM] THEN DISCH_THEN(K ALL_TAC) THEN
 656     ONCE_REWRITE_TAC[SET_RULE `x INSERT s = {x} UNION s`] THEN
 657     REWRITE_TAC[HYPERPLANE_CELL_UNION] THEN
 658     REWRITE_TAC[HYPERPLANE_CELL_SING; RIGHT_EXISTS_AND_THM; UNWIND_THM2] THEN
 659     CONJ_TAC THENL [ASM_MESON_TAC[NONEMPTY_HYPERPLANE_CELL]; ALL_TAC] THEN
 660     ONCE_REWRITE_TAC[CONJ_SYM] THEN REWRITE_TAC[INTER_UNIV; UNWIND_THM1] THEN
 661     ASM_SIMP_TAC[];
 662     ALL_TAC] THEN
 663   REWRITE_TAC[euler_characteristic] THEN
 664   ONCE_REWRITE_TAC[SET_RULE `x INSERT s = {x} UNION s`] THEN
 665   REWRITE_TAC[HYPERPLANE_CELL_UNION] THEN MATCH_MP_TAC EQ_TRANS THEN
 666   EXISTS_TAC
 667    `sum {c' INTER c |c'| hyperplane_cell {(a,b)} c' /\ ~(c' INTER c = {})}
 668         (\c:real^N->bool. (-- &1) pow (num_of_int(aff_dim c)))` THEN
 669   CONJ_TAC THENL
 670    [MATCH_MP_TAC(MESON[] `s = t ==> sum s f = sum t f`) THEN
 671     GEN_REWRITE_TAC I [EXTENSION] THEN REWRITE_TAC[IN_ELIM_THM] THEN
 672     X_GEN_TAC `c':real^N->bool` THEN EQ_TAC THENL
 673      [DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
 674       DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 675       MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `c1:real^N->bool` THEN
 676       DISCH_THEN(X_CHOOSE_THEN `c2:real^N->bool` STRIP_ASSUME_TAC) THEN
 677       SUBGOAL_THEN `~(DISJOINT c2 (c:real^N->bool))` ASSUME_TAC THENL
 678        [ASM SET_TAC[]; ASM_MESON_TAC[DISJOINT_HYPERPLANE_CELLS_EQ]];
 679       DISCH_THEN(X_CHOOSE_THEN `c1:real^N->bool` STRIP_ASSUME_TAC) THEN
 680       ASM_REWRITE_TAC[INTER_SUBSET] THEN
 681       MAP_EVERY EXISTS_TAC [`c1:real^N->bool`; `c:real^N->bool`] THEN
 682       ASM_SIMP_TAC[]];
 683     ALL_TAC] THEN
 684   ASM_REWRITE_TAC[HYPERPLANE_CELL_SING] THEN
 685   SUBGOAL_THEN `~(c:real^N->bool = {})` ASSUME_TAC THENL
 686    [ASM_MESON_TAC[NONEMPTY_HYPERPLANE_CELL]; ALL_TAC] THEN
 687   MAP_EVERY (fun t ->
 688    ASM_CASES_TAC t THENL
 689     [MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC
 690       `sum {c} (\c:real^N->bool. (-- &1) pow num_of_int (aff_dim c))` THEN
 691      CONJ_TAC THENL [ALL_TAC; SIMP_TAC[SUM_SING]] THEN
 692      MATCH_MP_TAC(MESON[] `s = t ==> sum s f = sum t f`) THEN
 693      GEN_REWRITE_TAC I [EXTENSION] THEN X_GEN_TAC `c':real^N->bool` THEN
 694      REWRITE_TAC[IN_SING; IN_ELIM_THM] THEN
 695      REWRITE_TAC[TAUT `(a \/ b) /\ c <=> a /\ c \/ b /\ c`] THEN
 696      REWRITE_TAC[EXISTS_OR_THM; UNWIND_THM2; GSYM CONJ_ASSOC] THEN
 697      EQ_TAC THEN STRIP_TAC THEN FIRST_X_ASSUM SUBST1_TAC THEN
 698      MP_TAC(ISPECL [`a:real^N`; `b:real`] HYPERPLANE_CELLS_DISTINCT_LEMMA) THEN
 699      ASM SET_TAC[];
 700      ALL_TAC])
 701    [`c SUBSET {x:real^N | a dot x < b}`;
 702     `c SUBSET {x:real^N | a dot x > b}`;
 703     `c SUBSET {x:real^N | a dot x = b}`] THEN
 704   SUBGOAL_THEN `~(c INTER {x:real^N | a dot x = b} = {})` ASSUME_TAC THENL
 705    [SUBGOAL_THEN
 706      `?u v:real^N. u IN c /\ ~(a dot u < b) /\ v IN c /\ ~(a dot v > b)`
 707     MP_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
 708     REWRITE_TAC[real_gt; REAL_NOT_LT; GSYM MEMBER_NOT_EMPTY] THEN
 709     REWRITE_TAC[IN_INTER; IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN
 710     MAP_EVERY X_GEN_TAC [`u:real^N`; `v:real^N`] THEN SIMP_TAC[REAL_LE_LT] THEN
 711     ASM_CASES_TAC `(a:real^N) dot u = b` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 712     ASM_CASES_TAC `(a:real^N) dot v = b` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 713     ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
 714     EXISTS_TAC `v + (b - a dot v) / (a dot u - a dot v) % (u - v):real^N` THEN
 715     SUBGOAL_THEN `(a:real^N) dot v < a dot u` ASSUME_TAC THENL
 716      [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
 717     ASM_SIMP_TAC[DOT_RADD; DOT_RMUL; DOT_RSUB; REAL_DIV_RMUL; REAL_SUB_LT;
 718                  REAL_LT_IMP_NZ; REAL_SUB_ADD2] THEN
 719     REWRITE_TAC[VECTOR_ARITH
 720      `v + a % (u - v):real^N = (&1 - a) % v + a % u`] THEN
 721     MATCH_MP_TAC IN_CONVEX_SET THEN
 722     ASM_SIMP_TAC[REAL_LE_RDIV_EQ; REAL_LE_LDIV_EQ; REAL_SUB_LT] THEN
 723     CONJ_TAC THENL [ALL_TAC; ASM_REAL_ARITH_TAC] THEN
 724     ASM_MESON_TAC[HYPERPLANE_CELL_CONVEX];
 725     ALL_TAC] THEN
 726   SUBGOAL_THEN `~(c INTER {x:real^N | a dot x < b} = {}) /\
 727                 ~(c INTER {x:real^N | a dot x > b} = {})`
 728   STRIP_ASSUME_TAC THENL
 729    [SUBGOAL_THEN
 730      `?u v:real^N.
 731          u IN c /\ a dot u = b /\ v IN c /\ ~(a dot v = b) /\ ~(u = v)`
 732     STRIP_ASSUME_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
 733     SUBGOAL_THEN
 734      `open_in (subtopology euclidean (affine hull c)) (c:real^N->bool)`
 735     MP_TAC THENL [ASM_MESON_TAC[HYPERPLANE_CELL_RELATIVELY_OPEN]; ALL_TAC] THEN
 736     REWRITE_TAC[open_in] THEN
 737     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o SPEC `u:real^N`)) THEN
 738     ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `e:real` THEN
 739     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC
 740      (MP_TAC o SPEC `u - e / &2 / norm(v - u) % (v - u):real^N`)) THEN
 741     ANTS_TAC THENL
 742      [REWRITE_TAC[NORM_ARITH `dist(u - a:real^N,u) = norm a`] THEN
 743       REWRITE_TAC[VECTOR_ARITH `x - a % (y - z):real^N = x + a % (z - y)`] THEN
 744       REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NUM; REAL_ABS_NORM] THEN
 745       ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN
 746       ASM_REWRITE_TAC[REAL_ARITH `abs e / &2 < e <=> &0 < e`] THEN
 747       MATCH_MP_TAC IN_AFFINE_ADD_MUL_DIFF THEN
 748       ASM_SIMP_TAC[AFFINE_AFFINE_HULL; HULL_INC];
 749       DISCH_TAC] THEN
 750     REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER; IN_ELIM_THM] THEN
 751     SUBGOAL_THEN `(a:real^N) dot v < b \/ a dot v > b` STRIP_ASSUME_TAC THENL
 752      [ASM_REAL_ARITH_TAC;
 753       CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 754       EXISTS_TAC `u - e / &2 / norm(v - u) % (v - u):real^N` THEN
 755       ASM_REWRITE_TAC[DOT_RSUB; DOT_RMUL] THEN
 756       REWRITE_TAC[REAL_ARITH `b - x * y > b <=> &0 < x * --y`] THEN
 757       MATCH_MP_TAC REAL_LT_MUL THEN
 758       ASM_SIMP_TAC[REAL_LT_DIV; REAL_HALF; NORM_POS_LT; VECTOR_SUB_EQ] THEN
 759       ASM_REAL_ARITH_TAC;
 760       CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[]]] THEN
 761     EXISTS_TAC `u - e / &2 / norm(v - u) % (v - u):real^N` THEN
 762     ASM_REWRITE_TAC[DOT_RSUB; DOT_RMUL] THEN
 763     REWRITE_TAC[REAL_ARITH `b - x * y > b <=> &0 < x * --y`;
 764                 REAL_ARITH `b - x < b <=> &0 < x`] THEN
 765     MATCH_MP_TAC REAL_LT_MUL THEN
 766     ASM_SIMP_TAC[REAL_LT_DIV; REAL_HALF; NORM_POS_LT; VECTOR_SUB_EQ] THEN
 767     ASM_REAL_ARITH_TAC;
 768     ALL_TAC] THEN
 769   MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC
 770    `sum {{x | a dot x = b} INTER c,
 771          {x | a dot x > b} INTER c,
 772          {x | a dot x < b} INTER c}
 773         (\c:real^N->bool. (-- &1) pow (num_of_int(aff_dim c)))` THEN
 774   CONJ_TAC THENL
 775    [MATCH_MP_TAC(MESON[] `s = t ==> sum s f = sum t f`) THEN
 776     GEN_REWRITE_TAC I [EXTENSION] THEN REWRITE_TAC[IN_ELIM_THM] THEN
 777     X_GEN_TAC `c':real^N->bool` THEN
 778     REWRITE_TAC[TAUT `(a \/ b) /\ c <=> a /\ c \/ b /\ c`] THEN
 779     REWRITE_TAC[EXISTS_OR_THM; UNWIND_THM2; GSYM CONJ_ASSOC] THEN
 780     ONCE_REWRITE_TAC[INTER_COMM] THEN ASM_REWRITE_TAC[] THEN
 781     REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN CONV_TAC TAUT;
 782     ALL_TAC] THEN
 783   SIMP_TAC[SUM_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
 784            IN_INSERT; NOT_IN_EMPTY] THEN
 785   ONCE_REWRITE_TAC[INTER_COMM] THEN
 786   ASM_SIMP_TAC[HYPERPLANE_CELLS_DISTINCT_LEMMA; REAL_ADD_RID; SET_RULE
 787    `s INTER t = {} /\ ~(c INTER s = {}) ==> ~(c INTER s = c INTER t)`] THEN
 788   SUBGOAL_THEN
 789    `aff_dim (c INTER {x:real^N | a dot x < b}) = aff_dim c /\
 790     aff_dim (c INTER {x:real^N | a dot x > b}) = aff_dim c`
 791    (CONJUNCTS_THEN SUBST1_TAC)
 792   THENL
 793    [ONCE_REWRITE_TAC[GSYM AFF_DIM_AFFINE_HULL] THEN CONJ_TAC THEN
 794     AP_TERM_TAC THEN MATCH_MP_TAC AFFINE_HULL_CONVEX_INTER_OPEN THEN
 795     ASM_REWRITE_TAC[OPEN_HALFSPACE_LT; OPEN_HALFSPACE_GT] THEN
 796     ASM_MESON_TAC[HYPERPLANE_CELL_CONVEX];
 797     ALL_TAC] THEN
 798   SUBGOAL_THEN
 799    `aff_dim c = aff_dim(c INTER {x:real^N | a dot x = b}) + &1`
 800   SUBST1_TAC THENL
 801    [MP_TAC(ISPECL [`A:real^N#real->bool`; `c:real^N->bool`]
 802         HYPERPLANE_CELL_INTER_OPEN_AFFINE) THEN
 803     ASM_SIMP_TAC[LEFT_IMP_EXISTS_THM] THEN
 804     MAP_EVERY X_GEN_TAC [`s:real^N->bool`; `t:real^N->bool`] THEN
 805     STRIP_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN
 806     ONCE_REWRITE_TAC[GSYM AFF_DIM_AFFINE_HULL] THEN
 807     SUBGOAL_THEN
 808      `affine hull (s INTER t) = affine hull t /\
 809       affine hull ((s INTER t) INTER {x:real^N | a dot x = b}) =
 810       affine hull (t INTER {x:real^N | a dot x = b})`
 811      (CONJUNCTS_THEN SUBST1_TAC)
 812     THENL
 813      [REWRITE_TAC[INTER_ASSOC] THEN CONJ_TAC THEN
 814       GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [INTER_COMM] THEN
 815       MATCH_MP_TAC AFFINE_HULL_CONVEX_INTER_OPEN THEN
 816       ASM_SIMP_TAC[CONVEX_INTER; CONVEX_HYPERPLANE; AFFINE_IMP_CONVEX] THEN
 817       ASM SET_TAC[];
 818       REWRITE_TAC[AFF_DIM_AFFINE_HULL] THEN
 819       ASM_SIMP_TAC[AFF_DIM_AFFINE_INTER_HYPERPLANE] THEN
 820       REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[INT_SUB_ADD]) THEN
 821       ASM SET_TAC[]];
 822     SUBGOAL_THEN `&0 <= aff_dim (c INTER {x:real^N | a dot x = b})` MP_TAC
 823     THENL [REWRITE_TAC[AFF_DIM_POS_LE] THEN ASM SET_TAC[]; ALL_TAC] THEN
 824     SPEC_TAC(`aff_dim (c INTER {x:real^N | a dot x = b})`,`i:int`) THEN
 825     REWRITE_TAC[GSYM INT_FORALL_POS] THEN
 826     REWRITE_TAC[NUM_OF_INT_OF_NUM; INT_OF_NUM_ADD] THEN
 827     REWRITE_TAC[REAL_POW_ADD] THEN REAL_ARITH_TAC]);;
 828
 829 let EULER_CHARACTERSTIC_INVARIANT = prove
 830  (`!A B h s:real^N->bool.
 831         FINITE A /\ FINITE B /\
 832         hyperplane_cellcomplex A s /\ hyperplane_cellcomplex B s
 833         ==> euler_characteristic A s = euler_characteristic B s`,
 834   SUBGOAL_THEN
 835    `!A s:real^N->bool.
 836         FINITE A /\ hyperplane_cellcomplex A s
 837         ==> !B. FINITE B
 838                 ==> euler_characteristic (A UNION B) s =
 839                     euler_characteristic A s`
 840   ASSUME_TAC THENL
 841    [REPEAT GEN_TAC THEN STRIP_TAC THEN
 842     MATCH_MP_TAC FINITE_INDUCT_STRONG THEN ASM_REWRITE_TAC[UNION_EMPTY] THEN
 843     MAP_EVERY X_GEN_TAC [`h:real^N#real`; `B:real^N#real->bool`] THEN
 844     DISCH_THEN(CONJUNCTS_THEN2 (SUBST1_TAC o SYM) STRIP_ASSUME_TAC) THEN
 845     REWRITE_TAC[SET_RULE `s UNION (x INSERT t) = x INSERT (s UNION t)`] THEN
 846     MATCH_MP_TAC EULER_CHARACTERSTIC_LEMMA THEN
 847     ASM_REWRITE_TAC[FINITE_UNION] THEN
 848     MATCH_MP_TAC HYPERPLANE_CELLCOMPLEX_MONO THEN
 849     EXISTS_TAC `A:real^N#real->bool` THEN ASM_REWRITE_TAC[] THEN SET_TAC[];
 850     RULE_ASSUM_TAC(REWRITE_RULE[RIGHT_IMP_FORALL_THM; IMP_IMP]) THEN
 851     REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
 852     EXISTS_TAC `euler_characteristic (A UNION B) (s:real^N->bool)` THEN
 853     ASM_MESON_TAC[UNION_COMM]]);;
 854
 855 let EULER_CHARACTERISTIC_INCLUSION_EXCLUSION = prove
 856  (`!A s:(real^N->bool)->bool.
 857         FINITE A /\ FINITE s /\ (!k. k IN s ==> hyperplane_cellcomplex A k)
 858         ==> euler_characteristic A (UNIONS s) =
 859             sum {t | t SUBSET s /\ ~(t = {})}
 860                 (\t. (-- &1) pow (CARD t + 1) *
 861                      euler_characteristic A (INTERS t))`,
 862   REPEAT STRIP_TAC THEN
 863   MP_TAC(ISPECL
 864    [`hyperplane_cellcomplex A :(real^N->bool)->bool`;
 865     `euler_characteristic A :(real^N->bool)->real`;
 866     `s:(real^N->bool)->bool`]
 867         INCLUSION_EXCLUSION_REAL_RESTRICTED) THEN
 868   ASM_SIMP_TAC[EULER_CHARACTERISTIC_CELLCOMPLEX_UNION] THEN
 869   SIMP_TAC[HYPERPLANE_CELLCOMPLEX_EMPTY; HYPERPLANE_CELLCOMPLEX_INTER;
 870            HYPERPLANE_CELLCOMPLEX_UNION; HYPERPLANE_CELLCOMPLEX_DIFF]);;
 871
 872 (* ------------------------------------------------------------------------- *)
 873 (* Euler-type relation for full-dimensional proper polyhedral cones.         *)
 874 (* ------------------------------------------------------------------------- *)
 875
 876 let EULER_POLYHEDRAL_CONE = prove
 877  (`!s. polyhedron s /\ conic s /\ ~(interior s = {}) /\ ~(s = (:real^N))
 878        ==> sum (0..dimindex(:N))
 879                (\d. (-- &1) pow d *
 880                     &(CARD {f | f face_of s /\ aff_dim f = &d })) = &0`,
 881   REPEAT STRIP_TAC THEN
 882   SUBGOAL_THEN `affine hull s = (:real^N)` ASSUME_TAC THENL
 883    [MATCH_MP_TAC(SET_RULE `!s. s = UNIV /\ s SUBSET t ==> t = UNIV`) THEN
 884     EXISTS_TAC `affine hull (interior s:real^N->bool)` THEN
 885     SIMP_TAC[INTERIOR_SUBSET; HULL_MONO] THEN
 886     MATCH_MP_TAC AFFINE_HULL_OPEN THEN ASM_REWRITE_TAC[OPEN_INTERIOR];
 887     ALL_TAC] THEN
 888   FIRST_ASSUM
 889    (MP_TAC o GEN_REWRITE_RULE I [POLYHEDRON_INTER_AFFINE_MINIMAL]) THEN
 890   ASM_REWRITE_TAC[INTER_UNIV; LEFT_IMP_EXISTS_THM] THEN
 891   X_GEN_TAC `H:(real^N->bool)->bool` THEN
 892   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 893   DISCH_THEN(CONJUNCTS_THEN2 (ASSUME_TAC o SYM) STRIP_ASSUME_TAC) THEN
 894   SUBGOAL_THEN `(vec 0:real^N) IN s` ASSUME_TAC THENL
 895    [ASM_SIMP_TAC[CONIC_CONTAINS_0] THEN
 896     ASM_MESON_TAC[SUBSET_EMPTY; INTERIOR_SUBSET];
 897     ALL_TAC] THEN
 898   SUBGOAL_THEN
 899    `!h:real^N->bool. h IN H ==> ?a. ~(a = vec 0) /\ h = {x | a dot x <= &0}`
 900   MP_TAC THENL
 901    [GEN_TAC THEN DISCH_TAC THEN
 902     FIRST_ASSUM(MP_TAC o SPEC `h:real^N->bool`) THEN
 903     ANTS_TAC THENL [ASM_REWRITE_TAC[]; MATCH_MP_TAC MONO_EXISTS]  THEN
 904     X_GEN_TAC `a:real^N` THEN
 905     DISCH_THEN(X_CHOOSE_THEN `b:real` STRIP_ASSUME_TAC) THEN
 906     SUBGOAL_THEN `b = &0` SUBST_ALL_TAC THENL [ALL_TAC; ASM_REWRITE_TAC[]] THEN
 907     MATCH_MP_TAC(REAL_ARITH `&0 <= b /\ ~(&0 < b) ==> b = &0`) THEN
 908     CONJ_TAC THENL
 909      [SUBGOAL_THEN `(vec 0:real^N) IN INTERS H` MP_TAC THENL
 910        [ASM SET_TAC[]; REWRITE_TAC[IN_INTERS]] THEN
 911       DISCH_THEN(MP_TAC o SPEC `h:real^N->bool`) THEN ASM_REWRITE_TAC[] THEN
 912       REWRITE_TAC[IN_ELIM_THM; DOT_RZERO];
 913       DISCH_TAC THEN
 914       FIRST_X_ASSUM(MP_TAC o SPEC `H DELETE (h:real^N->bool)`) THEN
 915       ANTS_TAC THENL [ASM SET_TAC[]; REWRITE_TAC[PSUBSET_ALT]] THEN
 916       DISCH_THEN(X_CHOOSE_THEN `x:real^N` STRIP_ASSUME_TAC o CONJUNCT2) THEN
 917       SUBGOAL_THEN `?e. &0 < e /\ e < &1 /\
 918                         (e % x:real^N) IN h` STRIP_ASSUME_TAC THENL
 919        [EXISTS_TAC `min (&1 / &2) (b / ((a:real^N) dot x))` THEN
 920         ASM_REWRITE_TAC[IN_ELIM_THM; DOT_RMUL] THEN
 921         SUBGOAL_THEN `&0 < (a:real^N) dot x` ASSUME_TAC THENL
 922          [MATCH_MP_TAC REAL_LT_TRANS THEN EXISTS_TAC `b:real` THEN
 923           ASM_REWRITE_TAC[] THEN
 924           UNDISCH_TAC `~((x:real^N) IN s)` THEN EXPAND_TAC "s" THEN
 925           ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
 926           REWRITE_TAC[REAL_NOT_LT] THEN DISCH_TAC THEN
 927           SUBGOAL_THEN `H:(real^N->bool)->bool = h INSERT (H DELETE h)`
 928           SUBST1_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
 929           REWRITE_TAC[INTERS_INSERT; IN_INTER] THEN
 930           ASM_REWRITE_TAC[IN_ELIM_THM];
 931           ASM_SIMP_TAC[REAL_LT_MIN; REAL_LT_DIV; REAL_MIN_LT] THEN
 932           CONV_TAC REAL_RAT_REDUCE_CONV THEN
 933           ASM_SIMP_TAC[GSYM REAL_LE_RDIV_EQ] THEN REAL_ARITH_TAC];
 934         UNDISCH_TAC `~((x:real^N) IN s)` THEN REWRITE_TAC[] THEN
 935         SUBGOAL_THEN `x:real^N = inv e % e % x` SUBST1_TAC THENL
 936          [ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; REAL_LT_IMP_NZ;
 937                        VECTOR_MUL_LID];
 938           ALL_TAC] THEN
 939         RULE_ASSUM_TAC(REWRITE_RULE[conic]) THEN
 940         FIRST_ASSUM MATCH_MP_TAC THEN
 941         ASM_SIMP_TAC[REAL_LT_IMP_LE; REAL_LE_INV_EQ] THEN
 942         EXPAND_TAC "s" THEN
 943         SUBGOAL_THEN `H:(real^N->bool)->bool = h INSERT (H DELETE h)`
 944         SUBST1_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
 945         REWRITE_TAC[INTERS_INSERT; IN_INTER] THEN
 946         CONJ_TAC THENL [ASM_REWRITE_TAC[]; ALL_TAC] THEN
 947         UNDISCH_TAC `(x:real^N) IN INTERS (H DELETE h)` THEN
 948         REWRITE_TAC[IN_INTERS] THEN MATCH_MP_TAC MONO_FORALL THEN
 949         X_GEN_TAC `k:real^N->bool` THEN REWRITE_TAC[IN_DELETE] THEN
 950         DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
 951         ANTS_TAC THENL [ASM_REWRITE_TAC[]; ALL_TAC] THEN
 952         FIRST_X_ASSUM(MP_TAC o SPEC `k:real^N->bool`) THEN
 953         ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 954         MAP_EVERY X_GEN_TAC [`a':real^N`; `b':real`] THEN
 955         STRIP_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN
 956         MATCH_MP_TAC(REAL_ARITH
 957          `(&0 <= x ==> y <= x) /\ (&0 <= --x ==> &0 <= --y) /\ &0 <= b
 958           ==> x <= b ==> y <= b`) THEN
 959         REWRITE_TAC[DOT_RMUL; GSYM REAL_MUL_RNEG] THEN
 960         REWRITE_TAC[REAL_ARITH `e * x <= x <=> &0 <= x * (&1 - e)`] THEN
 961         ASM_SIMP_TAC[REAL_LE_MUL; REAL_LT_IMP_LE; REAL_SUB_LE] THEN
 962         SUBGOAL_THEN `(vec 0:real^N) IN INTERS H` MP_TAC THENL
 963          [ASM SET_TAC[]; REWRITE_TAC[IN_INTERS]] THEN
 964         DISCH_THEN(MP_TAC o SPEC `k:real^N->bool`) THEN ASM_REWRITE_TAC[] THEN
 965         REWRITE_TAC[IN_ELIM_THM; DOT_RZERO]]];
 966     FIRST_X_ASSUM(K ALL_TAC o SPEC `h:real^N->bool`)] THEN
 967   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [RIGHT_IMP_EXISTS_THM] THEN
 968   REWRITE_TAC[SKOLEM_THM; LEFT_IMP_EXISTS_THM] THEN
 969   X_GEN_TAC `fa:(real^N->bool)->real^N` THEN
 970   GEN_REWRITE_TAC (LAND_CONV o BINDER_CONV o funpow 2 RAND_CONV)
 971    [EQ_SYM_EQ] THEN
 972   DISCH_TAC THEN ABBREV_TAC
 973    `A = IMAGE (\h. (fa:(real^N->bool)->real^N) h,&0) H` THEN
 974   SUBGOAL_THEN `FINITE(A:real^N#real->bool)` ASSUME_TAC THENL
 975    [EXPAND_TAC "A" THEN MATCH_MP_TAC FINITE_IMAGE THEN ASM_SIMP_TAC[];
 976     ALL_TAC] THEN
 977   MATCH_MP_TAC EQ_TRANS THEN
 978   EXISTS_TAC `euler_characteristic A (s:real^N->bool)` THEN CONJ_TAC THENL
 979    [ASM_SIMP_TAC[EULER_CHARACTERISTIC] THEN MATCH_MP_TAC SUM_EQ_NUMSEG THEN
 980     X_GEN_TAC `d:num` THEN STRIP_TAC THEN REWRITE_TAC[] THEN
 981     AP_TERM_TAC THEN AP_TERM_TAC THEN MATCH_MP_TAC BIJECTIONS_CARD_EQ THEN
 982     ASM_SIMP_TAC[FINITE_RESTRICT_HYPERPLANE_CELLS] THEN
 983     EXISTS_TAC `relative_interior:(real^N->bool)->(real^N->bool)` THEN
 984     EXISTS_TAC `closure:(real^N->bool)->(real^N->bool)` THEN
 985     REWRITE_TAC[IN_ELIM_THM] THEN CONJ_TAC THENL
 986      [X_GEN_TAC `f:real^N->bool` THEN STRIP_TAC THEN
 987       SUBGOAL_THEN `closure(relative_interior f):real^N->bool = f`
 988       ASSUME_TAC THENL
 989        [MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `closure f:real^N->bool` THEN
 990         CONJ_TAC THENL
 991          [MATCH_MP_TAC CONVEX_CLOSURE_RELATIVE_INTERIOR THEN
 992           ASM_MESON_TAC[FACE_OF_IMP_CONVEX];
 993           REWRITE_TAC[CLOSURE_EQ] THEN MATCH_MP_TAC FACE_OF_IMP_CLOSED THEN
 994           ASM_MESON_TAC[POLYHEDRON_IMP_CLOSED; POLYHEDRON_IMP_CONVEX]];
 995         ALL_TAC] THEN
 996       ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
 997        [ALL_TAC;
 998         ONCE_REWRITE_TAC[GSYM AFF_DIM_AFFINE_HULL] THEN
 999         ONCE_REWRITE_TAC[GSYM AFFINE_HULL_CLOSURE] THEN
1000         ASM_REWRITE_TAC[AFF_DIM_AFFINE_HULL] THEN
1001         ASM_MESON_TAC[RELATIVE_INTERIOR_SUBSET; SUBSET_TRANS;
1002                       FACE_OF_IMP_SUBSET]] THEN
1003       SUBGOAL_THEN `~(f:real^N->bool = {})` ASSUME_TAC THENL
1004        [ASM_REWRITE_TAC[GSYM AFF_DIM_POS_LE; INT_POS]; ALL_TAC] THEN
1005       SUBGOAL_THEN
1006        `?J. J SUBSET H /\
1007             f = INTERS {{x:real^N | fa h dot x <= &0} | h IN H} INTER
1008                 INTERS {{x | fa(h:real^N->bool) dot x = &0} | h IN J}`
1009       ASSUME_TAC THENL
1010        [ASM_CASES_TAC `f:real^N->bool = s` THENL
1011          [EXISTS_TAC `{}:(real^N->bool)->bool` THEN
1012           REWRITE_TAC[EMPTY_SUBSET; NOT_IN_EMPTY; INTERS_0; INTER_UNIV;
1013                       SET_RULE `{f x | x | F} = {}`] THEN
1014           ASM_REWRITE_TAC[] THEN
1015           REWRITE_TAC[SYM(ASSUME `INTERS H = (s:real^N->bool)`)] THEN
1016           AP_TERM_TAC THEN MATCH_MP_TAC(SET_RULE
1017            `(!x. x IN s ==> f x = x) ==> s = {f x | x IN s}`) THEN
1018           ASM_SIMP_TAC[];
1019           ALL_TAC] THEN
1020         EXISTS_TAC
1021         `{h:real^N->bool | h IN H /\
1022                      f SUBSET s INTER {x:real^N | fa h dot x = &0}}` THEN
1023         CONJ_TAC THENL [SET_TAC[]; ALL_TAC] THEN
1024         MP_TAC(ISPECL [`s:real^N->bool`; `H:(real^N->bool)->bool`;
1025                        `fa:(real^N->bool)->real^N`;
1026                        `\h:real^N->bool. &0`]
1027           FACE_OF_POLYHEDRON_EXPLICIT) THEN
1028         ASM_SIMP_TAC[INTER_UNIV] THEN
1029         DISCH_THEN(MP_TAC o SPEC `f:real^N->bool`) THEN ASM_REWRITE_TAC[] THEN
1030         SUBGOAL_THEN
1031          `INTERS {{x:real^N | fa(h:real^N->bool) dot x <= &0} | h IN H} = s`
1032         ASSUME_TAC THENL
1033          [EXPAND_TAC "s" THEN AP_TERM_TAC THEN MATCH_MP_TAC(SET_RULE
1034            `(!x. x IN s ==> f x = x) ==> {f x | x IN s} = s`) THEN
1035           ASM_SIMP_TAC[];
1036          ALL_TAC] THEN
1037         ASM_CASES_TAC `{h:real^N->bool | h IN H /\
1038                            f SUBSET s INTER {x:real^N | fa h dot x = &0}} =
1039                        {}`
1040         THENL
1041          [ONCE_REWRITE_TAC[SIMPLE_IMAGE_GEN] THEN
1042           ASM_REWRITE_TAC[IMAGE_CLAUSES; INTERS_0] THEN
1043           FIRST_ASSUM(MP_TAC o MATCH_MP FACE_OF_IMP_SUBSET) THEN
1044           ASM SET_TAC[];
1045           ALL_TAC] THEN
1046         DISCH_THEN(fun th -> GEN_REWRITE_TAC LAND_CONV [th]) THEN
1047         ASM_REWRITE_TAC[] THEN GEN_REWRITE_TAC I [EXTENSION] THEN
1048         X_GEN_TAC `y:real^N` THEN REWRITE_TAC[IN_INTER; IN_INTERS] THEN
1049         REWRITE_TAC[FORALL_IN_GSPEC; IN_INTER] THEN
1050         ASM_CASES_TAC `(y:real^N) IN s` THEN ASM_REWRITE_TAC[] THEN
1051         ASM SET_TAC[];
1052         ALL_TAC] THEN
1053       ABBREV_TAC
1054        `H' = IMAGE (\h:real^N->bool. {x:real^N | --(fa h) dot x <= &0}) H` THEN
1055       SUBGOAL_THEN
1056        `?J. FINITE J /\
1057             J SUBSET (H UNION H') /\
1058             f:real^N->bool = affine hull f INTER INTERS J`
1059       MP_TAC THENL
1060        [FIRST_X_ASSUM(X_CHOOSE_THEN `J:(real^N->bool)->bool`
1061           STRIP_ASSUME_TAC) THEN
1062         EXISTS_TAC
1063          `H UNION IMAGE (\h:real^N->bool.
1064              {x:real^N | --(fa h) dot x <= &0}) J` THEN
1065         REPEAT CONJ_TAC THENL
1066          [ASM_REWRITE_TAC[FINITE_UNION] THEN MATCH_MP_TAC FINITE_IMAGE THEN
1067           ASM_MESON_TAC[FINITE_SUBSET];
1068           EXPAND_TAC "H'" THEN ASM SET_TAC[];
1069           MATCH_MP_TAC(SET_RULE `s SUBSET f /\ s = t ==> s = f INTER t`) THEN
1070           REWRITE_TAC[HULL_SUBSET] THEN
1071           FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [th]) THEN
1072           REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN
1073           REWRITE_TAC[INTERS_UNION] THEN MATCH_MP_TAC(SET_RULE
1074            `s = s' /\ (!x. x IN s ==> (x IN t <=> x IN t'))
1075             ==> s INTER t = s' INTER t'`) THEN
1076           CONJ_TAC THENL
1077            [AP_TERM_TAC THEN MATCH_MP_TAC(SET_RULE
1078              `(!x. x IN s ==> f x = x) ==> {f x | x IN s} = s`) THEN
1079             ASM_SIMP_TAC[];
1080             ALL_TAC] THEN
1081           X_GEN_TAC `y:real^N` THEN REWRITE_TAC[IN_INTERS] THEN
1082           REWRITE_TAC[FORALL_IN_IMAGE; FORALL_IN_GSPEC] THEN
1083           REWRITE_TAC[IN_ELIM_THM; DOT_LNEG] THEN
1084           REWRITE_TAC[REAL_ARITH `--x <= &0 <=> &0 <= x`] THEN
1085           ASM SET_TAC[]];
1086         ALL_TAC] THEN
1087       GEN_REWRITE_TAC LAND_CONV
1088          [MESON[HAS_SIZE]
1089            `(?f. FINITE f /\ P f) <=> (?n f. f HAS_SIZE n /\ P f)`] THEN
1090       GEN_REWRITE_TAC LAND_CONV [num_WOP] THEN
1091       DISCH_THEN(X_CHOOSE_THEN `nn:num`
1092         (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
1093       DISCH_THEN(X_CHOOSE_THEN `J:(real^N->bool)->bool` STRIP_ASSUME_TAC) THEN
1094       SUBGOAL_THEN
1095        `!J'. J' PSUBSET J
1096              ==> (f:real^N->bool) PSUBSET (affine hull f INTER INTERS J')`
1097       ASSUME_TAC THENL
1098        [REPEAT STRIP_TAC THEN
1099         FIRST_X_ASSUM(MP_TAC o SPEC `CARD(J':(real^N->bool)->bool)`) THEN
1100         ANTS_TAC THENL [ASM_MESON_TAC[CARD_PSUBSET; HAS_SIZE]; ALL_TAC] THEN
1101         REWRITE_TAC[NOT_EXISTS_THM; HAS_SIZE] THEN
1102         DISCH_THEN(MP_TAC o SPEC `J':(real^N->bool)->bool`) THEN
1103         MATCH_MP_TAC(TAUT `a /\ b /\ (~c ==> d) ==> ~(a /\ b /\ c) ==> d`) THEN
1104         CONJ_TAC THENL
1105          [ASM_MESON_TAC[PSUBSET; FINITE_SUBSET; HAS_SIZE]; ALL_TAC] THEN
1106         CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
1107         MATCH_MP_TAC(SET_RULE
1108          `s SUBSET t ==> ~(s = t) ==> s PSUBSET t`) THEN
1109         FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [th]) THEN
1110         ASM SET_TAC[];
1111         ALL_TAC] THEN
1112       SUBGOAL_THEN
1113        `!h:real^N->bool. h IN J
1114           ==> ?a. {x | a dot x <= &0} = h /\
1115                   (h IN H /\ a = fa h \/ ?h'. h' IN H /\ a = --(fa h'))`
1116       MP_TAC THENL
1117        [X_GEN_TAC `h:real^N->bool` THEN DISCH_TAC THEN
1118         SUBGOAL_THEN `(h:real^N->bool) IN (H UNION H')` MP_TAC THENL
1119          [ASM SET_TAC[]; EXPAND_TAC "H'"] THEN
1120         UNDISCH_THEN `(h:real^N->bool) IN J` (K ALL_TAC) THEN
1121         SPEC_TAC(`h:real^N->bool`,`h:real^N->bool`) THEN
1122         REWRITE_TAC[IN_UNION; TAUT `(a \/ b ==> c) <=> (a ==> c) /\ (b ==> c)`;
1123                     FORALL_AND_THM; FORALL_IN_IMAGE] THEN
1124         CONJ_TAC THEN X_GEN_TAC `h:real^N->bool` THEN DISCH_TAC THENL
1125          [EXISTS_TAC `(fa:(real^N->bool)->real^N) h` THEN
1126           ASM_SIMP_TAC[];
1127           EXISTS_TAC `--((fa:(real^N->bool)->real^N) h)` THEN
1128           REWRITE_TAC[] THEN DISJ2_TAC THEN ASM_MESON_TAC[]];
1129         ALL_TAC] THEN
1130       GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [RIGHT_IMP_EXISTS_THM] THEN
1131       REWRITE_TAC[SKOLEM_THM; LEFT_IMP_EXISTS_THM] THEN
1132       X_GEN_TAC `ga:(real^N->bool)->real^N` THEN DISCH_TAC THEN
1133       MP_TAC(ISPECL
1134        [`f:real^N->bool`; `J:(real^N->bool)->bool`;
1135         `ga:(real^N->bool)->real^N`; `\h:real^N->bool. &0`]
1136        RELATIVE_INTERIOR_POLYHEDRON_EXPLICIT) THEN
1137       ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
1138        [REPEAT CONJ_TAC THENL
1139          [ASM_MESON_TAC[HAS_SIZE];
1140           ASM_MESON_TAC[];
1141           ASM_SIMP_TAC[] THEN ASM_MESON_TAC[VECTOR_NEG_EQ_0; SUBSET]];
1142         DISCH_TAC THEN ASM_REWRITE_TAC[]] THEN
1143       SUBGOAL_THEN
1144        `!h:real^N->bool. h IN J ==> h IN H /\ ga h:real^N = fa h`
1145       ASSUME_TAC THENL
1146        [SUBGOAL_THEN `~(relative_interior f:real^N->bool = {})` MP_TAC THENL
1147          [ASM_MESON_TAC[RELATIVE_INTERIOR_EQ_EMPTY; FACE_OF_IMP_CONVEX];
1148           REWRITE_TAC[GSYM MEMBER_NOT_EMPTY]] THEN
1149         DISCH_THEN(X_CHOOSE_TAC `z:real^N`) THEN
1150         SUBGOAL_THEN `(z:real^N) IN f /\ z IN s` STRIP_ASSUME_TAC THENL
1151          [ASM_MESON_TAC[SUBSET; FACE_OF_IMP_SUBSET; RELATIVE_INTERIOR_SUBSET];
1152           ALL_TAC] THEN
1153         X_GEN_TAC `h:real^N->bool` THEN DISCH_TAC THEN
1154         FIRST_X_ASSUM(MP_TAC o SPEC `h:real^N->bool`) THEN
1155         ASM_REWRITE_TAC[] THEN
1156         DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1157         DISCH_THEN(DISJ_CASES_THEN MP_TAC) THEN REWRITE_TAC[] THEN
1158         DISCH_THEN(X_CHOOSE_THEN `h':real^N->bool` STRIP_ASSUME_TAC) THEN
1159         UNDISCH_TAC `(z:real^N) IN relative_interior f` THEN
1160         ASM_REWRITE_TAC[IN_ELIM_THM] THEN
1161         DISCH_THEN(MP_TAC o SPEC `h:real^N->bool`) THEN
1162         ASM_REWRITE_TAC[DOT_LNEG] THEN
1163         UNDISCH_TAC `(z:real^N) IN s` THEN EXPAND_TAC "s" THEN
1164         REWRITE_TAC[IN_INTERS] THEN
1165         DISCH_THEN(MP_TAC o SPEC `h':real^N->bool`) THEN ASM_REWRITE_TAC[] THEN
1166         FIRST_X_ASSUM(MP_TAC o SPEC `h':real^N->bool`) THEN
1167         ASM_REWRITE_TAC[] THEN DISCH_THEN(fun th ->
1168           GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [SYM(CONJUNCT2 th)]) THEN
1169         REWRITE_TAC[IN_ELIM_THM] THEN REAL_ARITH_TAC;
1170         ALL_TAC] THEN
1171       FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [SYM th] THEN
1172         MP_TAC(SYM th)) THEN
1173       FIRST_X_ASSUM(X_CHOOSE_THEN `K:(real^N->bool)->bool` MP_TAC) THEN
1174       DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1175       DISCH_THEN(fun th -> ASSUME_TAC(SYM th) THEN
1176         GEN_REWRITE_TAC (LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV) [th]) THEN
1177       REWRITE_TAC[IN_INTER; IN_INTERS; FORALL_IN_GSPEC; GSYM CONJ_ASSOC] THEN
1178       REWRITE_TAC[IN_ELIM_THM] THEN DISCH_TAC THEN
1179       SUBGOAL_THEN `~(relative_interior f:real^N->bool = {})` ASSUME_TAC THENL
1180        [ASM_MESON_TAC[RELATIVE_INTERIOR_EQ_EMPTY; FACE_OF_IMP_CONVEX];
1181         ALL_TAC] THEN
1182       SUBGOAL_THEN `DISJOINT (J:(real^N->bool)->bool) K` ASSUME_TAC THENL
1183        [UNDISCH_TAC `~(relative_interior f:real^N->bool = {})` THEN
1184         FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC
1185          (LAND_CONV o RAND_CONV o LAND_CONV) [SYM th]) THEN
1186         REWRITE_TAC[IN_DISJOINT; GSYM MEMBER_NOT_EMPTY; IN_ELIM_THM] THEN
1187         ASM_MESON_TAC[REAL_LT_REFL];
1188         ALL_TAC] THEN
1189       SUBGOAL_THEN
1190        `relative_interior f =
1191           INTERS {(if (h:real^N->bool) IN J then {x | fa h dot x < &0}
1192                    else if h IN K then {x:real^N | fa h dot x = &0}
1193                    else if relative_interior f SUBSET {x | fa h dot x = &0}
1194                    then {x | fa h dot x = &0}
1195                    else {x | fa h dot x < &0}) | h IN H}`
1196       ASSUME_TAC THENL
1197        [MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL
1198          [ALL_TAC;
1199           FIRST_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [SYM th]) THEN
1200           GEN_REWRITE_TAC I [SUBSET] THEN
1201           REWRITE_TAC[IN_INTERS; FORALL_IN_GSPEC; AND_FORALL_THM] THEN
1202           X_GEN_TAC `x:real^N` THEN REWRITE_TAC[IN_ELIM_THM] THEN
1203           MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `h:real^N->bool` THEN
1204           ASM_CASES_TAC `(h:real^N->bool) IN H` THENL
1205            [ALL_TAC; DISCH_THEN(K ALL_TAC) THEN ASM SET_TAC[]] THEN
1206           ASM_REWRITE_TAC[] THEN
1207           ASM_CASES_TAC `(h:real^N->bool) IN J` THEN
1208           ASM_SIMP_TAC[IN_ELIM_THM; REAL_LT_IMP_LE] THENL
1209            [ASM SET_TAC[]; ALL_TAC] THEN
1210           ASM_CASES_TAC `(h:real^N->bool) IN K` THEN
1211           ASM_SIMP_TAC[IN_ELIM_THM; REAL_LE_REFL] THEN
1212           COND_CASES_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN
1213           REAL_ARITH_TAC] THEN
1214         GEN_REWRITE_TAC I [SUBSET] THEN X_GEN_TAC `x:real^N` THEN
1215         DISCH_TAC THEN REWRITE_TAC[IN_INTERS; FORALL_IN_GSPEC] THEN
1216         X_GEN_TAC `h:real^N->bool` THEN DISCH_TAC THEN
1217         REPEAT(COND_CASES_TAC THENL [ASM SET_TAC[]; ALL_TAC]) THEN
1218         REWRITE_TAC[IN_ELIM_THM; REAL_LT_LE] THEN
1219         CONJ_TAC THENL [ASM SET_TAC[]; DISCH_TAC] THEN
1220         FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I
1221          [SET_RULE `~(s SUBSET t) <=> ?y. y IN s /\ ~(y IN t)`]) THEN
1222         REWRITE_TAC[IN_ELIM_THM; NOT_EXISTS_THM] THEN
1223         X_GEN_TAC `y:real^N` THEN STRIP_TAC THEN
1224         FIRST_X_ASSUM(DISJ_CASES_TAC o MATCH_MP (REAL_ARITH
1225          `~(x:real = &0) ==> ~(x <= &0) \/ x < &0`))
1226         THENL [ASM SET_TAC[]; ALL_TAC] THEN
1227         MP_TAC(ASSUME `(x:real^N) IN relative_interior f`) THEN
1228         REWRITE_TAC[IN_RELATIVE_INTERIOR_CBALL] THEN
1229         DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1230         REWRITE_TAC[NOT_EXISTS_THM] THEN X_GEN_TAC `e:real` THEN
1231         DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1232         REWRITE_TAC[SUBSET; IN_INTER; IN_CBALL] THEN
1233         SUBGOAL_THEN `~(y:real^N = x)` ASSUME_TAC THENL
1234          [ASM_MESON_TAC[REAL_LT_REFL]; ALL_TAC] THEN
1235         DISCH_THEN(MP_TAC o SPEC `x + e / norm(y - x) % (x - y):real^N`) THEN
1236         SUBGOAL_THEN
1237          `(x:real^N) IN affine hull f /\ y IN affine hull f`
1238         STRIP_ASSUME_TAC THENL
1239          [ASM_MESON_TAC[RELATIVE_INTERIOR_SUBSET; SUBSET; HULL_SUBSET];
1240           ASM_SIMP_TAC[IN_AFFINE_ADD_MUL_DIFF; AFFINE_AFFINE_HULL]] THEN
1241         REWRITE_TAC[NORM_ARITH `dist(x:real^N,x + r) = norm r`] THEN
1242         REWRITE_TAC[NOT_IMP] THEN CONJ_TAC THENL
1243          [ASM_SIMP_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM; NORM_SUB;
1244                        REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN
1245           ASM_REAL_ARITH_TAC;
1246           DISCH_TAC] THEN
1247         SUBGOAL_THEN `(x + e / norm(y - x) % (x - y):real^N) IN s` MP_TAC THENL
1248          [ASM_MESON_TAC[SUBSET; FACE_OF_IMP_SUBSET]; ALL_TAC] THEN
1249         EXPAND_TAC "s" THEN REWRITE_TAC[IN_INTERS] THEN
1250         DISCH_THEN(MP_TAC o SPEC `h:real^N->bool`) THEN
1251         ASM_REWRITE_TAC[] THEN
1252         FIRST_ASSUM(fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV)
1253          [SYM(CONJUNCT2(MATCH_MP th (ASSUME `(h:real^N->bool) IN H`)))]) THEN
1254         ASM_REWRITE_TAC[IN_ELIM_THM; DOT_RADD; REAL_ADD_LID; DOT_RMUL] THEN
1255         ASM_REWRITE_TAC[DOT_RSUB; REAL_SUB_LZERO; REAL_NOT_LE] THEN
1256         MATCH_MP_TAC REAL_LT_MUL THEN
1257         ASM_SIMP_TAC[REAL_LT_DIV; NORM_POS_LT; VECTOR_SUB_EQ] THEN
1258         ASM_REAL_ARITH_TAC;
1259         ALL_TAC] THEN
1260       UNDISCH_TAC `~(relative_interior f:real^N->bool = {})` THEN
1261       REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; hyperplane_cell] THEN
1262       MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `z:real^N` THEN
1263       GEN_REWRITE_TAC RAND_CONV [EXTENSION] THEN
1264       ONCE_ASM_REWRITE_TAC[] THEN EXPAND_TAC "A" THEN
1265       REWRITE_TAC[IN_INTERS; FORALL_IN_GSPEC] THEN
1266       DISCH_THEN(fun th -> X_GEN_TAC `x:real^N` THEN MP_TAC th) THEN
1267       GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [IN] THEN
1268       REWRITE_TAC[hyperplane_equiv; FORALL_IN_IMAGE] THEN
1269       MATCH_MP_TAC(MESON[]
1270        `(!h. P h ==> (Q h <=> R h))
1271         ==> (!h. P h) ==> ((!h. Q h) <=> (!h. R h))`) THEN
1272       X_GEN_TAC `h:real^N->bool` THEN
1273       ASM_CASES_TAC `(h:real^N->bool) IN H` THEN ASM_REWRITE_TAC[] THEN
1274       REWRITE_TAC[hyperplane_side; REAL_SUB_RZERO] THEN
1275       REPEAT(COND_CASES_TAC THEN
1276         SIMP_TAC[IN_ELIM_THM] THENL [MESON_TAC[REAL_SGN_EQ]; ALL_TAC]) THEN
1277       MESON_TAC[REAL_SGN_EQ];
1278       X_GEN_TAC `c:real^N->bool` THEN STRIP_TAC THEN
1279       ONCE_REWRITE_TAC[GSYM AFF_DIM_AFFINE_HULL] THEN
1280       REWRITE_TAC[AFFINE_HULL_CLOSURE] THEN
1281       ASM_REWRITE_TAC[AFF_DIM_AFFINE_HULL] THEN CONJ_TAC THENL
1282        [ALL_TAC;
1283         MATCH_MP_TAC EQ_TRANS THEN
1284         EXISTS_TAC `relative_interior c:real^N->bool` THEN CONJ_TAC THENL
1285          [MATCH_MP_TAC CONVEX_RELATIVE_INTERIOR_CLOSURE THEN
1286           ASM_MESON_TAC[HYPERPLANE_CELL_CONVEX];
1287           ASM_MESON_TAC[HYPERPLANE_CELL_RELATIVE_INTERIOR]]] THEN
1288       SUBGOAL_THEN
1289        `?J. J SUBSET H /\
1290             c = INTERS {{x | (fa(h:real^N->bool)) dot x < &0} | h IN J} INTER
1291                 INTERS {{x:real^N | (fa h) dot x = &0} | h IN (H DIFF J)}`
1292       MP_TAC THENL
1293        [FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [HYPERPLANE_CELL]) THEN
1294         EXPAND_TAC "A" THEN REWRITE_TAC[hyperplane_equiv; FORALL_IN_IMAGE] THEN
1295         DISCH_THEN(X_CHOOSE_THEN `z:real^N` MP_TAC) THEN
1296         REWRITE_TAC[hyperplane_side; REAL_SUB_RZERO] THEN
1297         GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)
1298          [EQ_SYM_EQ] THEN
1299         DISCH_THEN(ASSUME_TAC o SYM) THEN EXISTS_TAC
1300          `{h:real^N->bool | h IN H /\
1301                             real_sgn(fa h dot (z:real^N)) = -- &1}` THEN
1302         REWRITE_TAC[SET_RULE `{x | x IN s /\ P x} SUBSET s`] THEN
1303         REWRITE_TAC[GSYM INTERS_UNION] THEN EXPAND_TAC "c" THEN
1304         GEN_REWRITE_TAC I [EXTENSION] THEN X_GEN_TAC `y:real^N` THEN
1305         REWRITE_TAC[IN_ELIM_THM; IN_INTERS] THEN REWRITE_TAC[IN_UNION] THEN
1306         REWRITE_TAC[TAUT `(a \/ b ==> c) <=> (a ==> c) /\ (b ==> c)`;
1307                     FORALL_AND_THM] THEN
1308         REWRITE_TAC[FORALL_IN_GSPEC] THEN
1309         REWRITE_TAC[IN_DIFF; IN_ELIM_THM] THEN
1310         REWRITE_TAC[TAUT `a /\ ~(a /\ b) <=> a /\ ~b`] THEN
1311         REWRITE_TAC[AND_FORALL_THM] THEN AP_TERM_TAC THEN
1312         REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `h:real^N->bool` THEN
1313         ASM_CASES_TAC `(h:real^N->bool) IN H` THEN ASM_REWRITE_TAC[] THEN
1314         REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
1315          (SPEC `(fa:(real^N->bool)->real^N) h dot z` REAL_SGN_CASES) THEN
1316         ASM_REWRITE_TAC[] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
1317         REWRITE_TAC[REAL_SGN_EQ] THEN
1318         SUBGOAL_THEN `?x:real^N. x IN c /\ x IN s` MP_TAC THENL
1319          [ASM_MESON_TAC[MEMBER_NOT_EMPTY; SUBSET; NONEMPTY_HYPERPLANE_CELL];
1320           MATCH_MP_TAC(TAUT `~p ==> p ==> q`)] THEN
1321         MAP_EVERY EXPAND_TAC ["s"; "c"] THEN
1322         REWRITE_TAC[IN_INTERS; IN_ELIM_THM; NOT_EXISTS_THM] THEN
1323         X_GEN_TAC `x:real^N` THEN REWRITE_TAC[AND_FORALL_THM] THEN
1324         DISCH_THEN(MP_TAC o SPEC `h:real^N->bool`) THEN
1325         ASM_REWRITE_TAC[REAL_SGN_EQ] THEN
1326         DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1327         FIRST_X_ASSUM(MP_TAC o SPEC `h:real^N->bool`) THEN
1328         ASM_REWRITE_TAC[] THEN
1329         DISCH_THEN(SUBST1_TAC o SYM o CONJUNCT2) THEN
1330         REWRITE_TAC[IN_ELIM_THM] THEN ASM_REAL_ARITH_TAC;
1331         DISCH_THEN(STRIP_ASSUME_TAC o GSYM)] THEN
1332       EXPAND_TAC "c" THEN
1333       W(MP_TAC o PART_MATCH (lhand o rand) CLOSURE_INTER_CONVEX o
1334         lhand o snd) THEN
1335       ANTS_TAC THENL
1336        [SIMP_TAC[CONVEX_INTERS; FORALL_IN_GSPEC; CONVEX_HALFSPACE_LT;
1337                  CONVEX_HYPERPLANE] THEN
1338         W(MP_TAC o PART_MATCH (lhand o rand) RELATIVE_INTERIOR_OPEN o
1339           lhand o lhand o rand o snd) THEN
1340         ANTS_TAC THENL
1341          [MATCH_MP_TAC OPEN_INTERS THEN
1342           ONCE_REWRITE_TAC[SIMPLE_IMAGE] THEN
1343           REWRITE_TAC[FORALL_IN_IMAGE; OPEN_HALFSPACE_LT] THEN
1344           MATCH_MP_TAC FINITE_IMAGE THEN ASM_MESON_TAC[FINITE_SUBSET];
1345           DISCH_THEN SUBST1_TAC] THEN
1346         W(MP_TAC o PART_MATCH (lhand o rand) RELATIVE_INTERIOR_OPEN_IN o
1347           rand o lhand o rand o snd) THEN
1348         ANTS_TAC THENL
1349          [MATCH_MP_TAC(MESON[OPEN_IN_SUBTOPOLOGY_REFL]
1350            `s SUBSET topspace tp /\ t = s
1351             ==> open_in (subtopology tp t) s`) THEN
1352           REWRITE_TAC[SUBSET_UNIV; TOPSPACE_EUCLIDEAN] THEN
1353           REWRITE_TAC[AFFINE_HULL_EQ] THEN
1354           SIMP_TAC[AFFINE_INTERS; AFFINE_HYPERPLANE; FORALL_IN_GSPEC];
1355           DISCH_THEN SUBST1_TAC THEN ASM_REWRITE_TAC[] THEN
1356           ASM_MESON_TAC[NONEMPTY_HYPERPLANE_CELL]];
1357         ALL_TAC] THEN
1358       DISCH_THEN SUBST1_TAC THEN
1359       SIMP_TAC[CLOSURE_INTERS_CONVEX_OPEN; FORALL_IN_GSPEC;
1360                CONVEX_HALFSPACE_LT; OPEN_HALFSPACE_LT] THEN
1361       COND_CASES_TAC THEN ASM_REWRITE_TAC[EMPTY_FACE_OF; INTER_EMPTY] THEN
1362       SUBGOAL_THEN
1363        `IMAGE closure {{x | fa h dot x < &0} | h IN J} =
1364         {{x | (fa:(real^N->bool)->real^N) h dot x <= &0} | h IN J}`
1365       SUBST1_TAC THENL
1366        [ONCE_REWRITE_TAC[SIMPLE_IMAGE] THEN
1367         REWRITE_TAC[GSYM IMAGE_o; o_DEF] THEN
1368         MATCH_MP_TAC(SET_RULE
1369          `(!x. x IN s ==> f x = g x) ==> IMAGE f s = IMAGE g s`) THEN
1370         GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[] THEN
1371         MATCH_MP_TAC CLOSURE_HALFSPACE_LT THEN ASM SET_TAC[];
1372         ALL_TAC] THEN
1373       SUBGOAL_THEN
1374       `closure (INTERS {{x | fa h dot x = &0} | h IN H DIFF J}) =
1375        INTERS {{x | (fa:(real^N->bool)->real^N) h dot x = &0} | h IN H DIFF J}`
1376       SUBST1_TAC THENL
1377        [REWRITE_TAC[CLOSURE_EQ] THEN
1378         SIMP_TAC[CLOSED_INTERS; FORALL_IN_GSPEC; CLOSED_HYPERPLANE];
1379         ALL_TAC] THEN
1380       ASM_CASES_TAC `J:(real^N->bool)->bool = H` THENL
1381        [ASM_REWRITE_TAC[DIFF_EQ_EMPTY; INTER_UNIV; NOT_IN_EMPTY;
1382                         SET_RULE `{f x | x | F} = {}`; INTERS_0] THEN
1383         FIRST_ASSUM(MP_TAC o MATCH_MP FACE_OF_REFL o
1384          MATCH_MP POLYHEDRON_IMP_CONVEX) THEN
1385         MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN AP_TERM_TAC THEN
1386         EXPAND_TAC "s" THEN AP_TERM_TAC THEN
1387         MATCH_MP_TAC(SET_RULE
1388          `(!x. x IN s ==> f x = x) ==> s = {f x | x IN s}`) THEN
1389         ASM_SIMP_TAC[];
1390         ALL_TAC] THEN
1391       SUBGOAL_THEN
1392        `INTERS {{x | fa(h:real^N->bool) dot x <= &0} | h IN J} INTER
1393         INTERS {{x:real^N | fa h dot x = &0} | h IN H DIFF J} =
1394         INTERS {s INTER {x | fa h dot x = &0} | h IN H DIFF J}`
1395       SUBST1_TAC THENL
1396        [ONCE_REWRITE_TAC[SIMPLE_IMAGE] THEN REWRITE_TAC[INTERS_IMAGE] THEN
1397         GEN_REWRITE_TAC I [EXTENSION] THEN X_GEN_TAC `y:real^N` THEN
1398         REWRITE_TAC[IN_INTER; IN_ELIM_THM] THEN
1399         ASM_CASES_TAC `(y:real^N) IN s` THEN ASM_REWRITE_TAC[] THENL
1400          [MATCH_MP_TAC(TAUT `a ==> (a /\ b <=> b)`) THEN
1401           UNDISCH_TAC `(y:real^N) IN s` THEN EXPAND_TAC "s" THEN
1402           REWRITE_TAC[IN_INTERS] THEN MATCH_MP_TAC MONO_FORALL THEN
1403           X_GEN_TAC `h:real^N->bool` THEN
1404           DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
1405           ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
1406           FIRST_X_ASSUM(MP_TAC o SPEC `h:real^N->bool`) THEN
1407           ANTS_TAC THENL [ASM SET_TAC[]; SET_TAC[]];
1408           UNDISCH_TAC `~((y:real^N) IN s)` THEN MATCH_MP_TAC
1409            (TAUT `~q /\ (p ==> r) ==> ~r ==> (p <=> q)`) THEN
1410           CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
1411           EXPAND_TAC "s" THEN REWRITE_TAC[IN_INTERS; AND_FORALL_THM] THEN
1412           MATCH_MP_TAC MONO_FORALL THEN
1413           X_GEN_TAC `h:real^N->bool` THEN
1414           DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
1415           FIRST_X_ASSUM(MP_TAC o SPEC `h:real^N->bool`) THEN
1416           ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
1417           DISCH_THEN(fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV)
1418            [GSYM(CONJUNCT2 th)]) THEN
1419           ASM_REWRITE_TAC[IN_DIFF; IN_ELIM_THM] THEN
1420           ASM_CASES_TAC `(h:real^N->bool) IN J` THEN
1421           ASM_SIMP_TAC[REAL_LE_REFL]];
1422         ALL_TAC] THEN
1423       MATCH_MP_TAC FACE_OF_INTERS THEN
1424       CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
1425       REWRITE_TAC[FORALL_IN_GSPEC] THEN
1426       X_GEN_TAC `h:real^N->bool` THEN REWRITE_TAC[IN_DIFF] THEN STRIP_TAC THEN
1427       MATCH_MP_TAC FACE_OF_INTER_SUPPORTING_HYPERPLANE_LE THEN
1428       ASM_SIMP_TAC[POLYHEDRON_IMP_CONVEX] THEN X_GEN_TAC `y:real^N` THEN
1429       EXPAND_TAC "s" THEN REWRITE_TAC[IN_INTERS] THEN
1430       DISCH_THEN(MP_TAC o SPEC `h:real^N->bool`) THEN ASM_REWRITE_TAC[] THEN
1431       FIRST_X_ASSUM(MP_TAC o SPEC `h:real^N->bool`) THEN
1432       ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
1433       DISCH_THEN(fun th -> GEN_REWRITE_TAC (LAND_CONV o RAND_CONV)
1434         [GSYM(CONJUNCT2 th)]) THEN
1435       REWRITE_TAC[IN_ELIM_THM]];
1436     ALL_TAC] THEN
1437   SUBGOAL_THEN
1438    `!h. h IN H ==> hyperplane_cellcomplex A ((:real^N) DIFF h)`
1439   ASSUME_TAC THENL
1440    [GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC HYPERPLANE_CELLCOMPLEX_MONO THEN
1441     EXISTS_TAC `{((fa:(real^N->bool)->real^N) h,&0)}` THEN CONJ_TAC THENL
1442      [MATCH_MP_TAC HYPERPLANE_CELL_CELLCOMPLEX THEN
1443       ASM_SIMP_TAC[HYPERPLANE_CELL_SING] THEN REPEAT DISJ2_TAC THEN
1444       FIRST_X_ASSUM(MP_TAC o SPEC `h:real^N->bool`) THEN
1445       ASM_REWRITE_TAC[] THEN DISCH_THEN(fun th ->
1446         GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [SYM(CONJUNCT2 th)]) THEN
1447       REWRITE_TAC[EXTENSION; IN_DIFF; IN_ELIM_THM; IN_UNIV] THEN
1448       REAL_ARITH_TAC;
1449       EXPAND_TAC "A" THEN
1450       REWRITE_TAC[IN_IMAGE; SUBSET; FORALL_UNWIND_THM2; IN_SING] THEN
1451       ASM_MESON_TAC[]];
1452     ALL_TAC] THEN
1453   SUBGOAL_THEN
1454    `!h:real^N->bool. h IN H ==> hyperplane_cellcomplex A h`
1455   ASSUME_TAC THENL
1456    [ASM_MESON_TAC[HYPERPLANE_CELLCOMPLEX_COMPL;
1457                   SET_RULE `UNIV DIFF (UNIV DIFF s) = s`];
1458     ALL_TAC] THEN
1459   SUBGOAL_THEN `hyperplane_cellcomplex A (s:real^N->bool)` ASSUME_TAC THENL
1460    [EXPAND_TAC "s" THEN MATCH_MP_TAC HYPERPLANE_CELLCOMPLEX_INTERS THEN
1461     ASM_REWRITE_TAC[];
1462     ALL_TAC] THEN
1463   MP_TAC(ISPECL [`A:real^N#real->bool`;
1464                  `INTERS H:real^N->bool`;
1465                  `(:real^N) DIFF INTERS H`]
1466         EULER_CHARACTERISTIC_CELLCOMPLEX_UNION) THEN
1467   REWRITE_TAC[SET_RULE `DISJOINT s (UNIV DIFF s)`] THEN ANTS_TAC THENL
1468    [ASM_SIMP_TAC[HYPERPLANE_CELLCOMPLEX_DIFF; HYPERPLANE_CELLCOMPLEX_UNIV];
1469     REWRITE_TAC[SET_RULE `s UNION (UNIV DIFF s) = UNIV`]] THEN
1470   REWRITE_TAC[DIFF_INTERS] THEN ASM_REWRITE_TAC[] THEN
1471   MATCH_MP_TAC(REAL_ARITH
1472    `x = (--(&1)) pow (dimindex(:N)) /\
1473     y = (--(&1)) pow (dimindex(:N))
1474     ==> x = s + y ==> s = &0`) THEN
1475   CONJ_TAC THENL
1476    [MATCH_MP_TAC EQ_TRANS THEN
1477     EXISTS_TAC `euler_characteristic {} (:real^N)` THEN CONJ_TAC THENL
1478      [MATCH_MP_TAC EULER_CHARACTERSTIC_INVARIANT THEN
1479       ASM_REWRITE_TAC[FINITE_EMPTY] THEN CONJ_TAC THENL
1480        [MATCH_MP_TAC HYPERPLANE_CELLCOMPLEX_MONO THEN
1481         EXISTS_TAC `{}:real^N#real->bool` THEN REWRITE_TAC[EMPTY_SUBSET];
1482         ALL_TAC] THEN
1483       MATCH_MP_TAC HYPERPLANE_CELL_CELLCOMPLEX THEN
1484       REWRITE_TAC[HYPERPLANE_CELL_EMPTY];
1485       SIMP_TAC[EULER_CHARACTERISTIC_CELL; HYPERPLANE_CELL_EMPTY] THEN
1486       REWRITE_TAC[AFF_DIM_UNIV; NUM_OF_INT_OF_NUM]];
1487     ALL_TAC] THEN
1488   W(MP_TAC o PART_MATCH (lhs o rand) EULER_CHARACTERISTIC_INCLUSION_EXCLUSION o
1489     lhand o snd) THEN
1490   ANTS_TAC THENL
1491    [ASM_REWRITE_TAC[FORALL_IN_GSPEC] THEN ONCE_REWRITE_TAC[SIMPLE_IMAGE] THEN
1492     ASM_SIMP_TAC[FINITE_IMAGE];
1493     DISCH_THEN SUBST1_TAC] THEN
1494   MATCH_MP_TAC EQ_TRANS THEN
1495   EXISTS_TAC `sum {t | t SUBSET {(:real^N) DIFF t | t IN H} /\ ~(t = {})}
1496              (\t. -- &1 pow (CARD t + 1) * (--(&1)) pow (dimindex(:N)))` THEN
1497   CONJ_TAC THENL
1498    [MATCH_MP_TAC SUM_EQ THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN
1499     REWRITE_TAC[SIMPLE_IMAGE; IMP_CONJ; FORALL_SUBSET_IMAGE] THEN
1500     X_GEN_TAC `J:(real^N->bool)->bool` THEN DISCH_TAC THEN
1501     REWRITE_TAC[IMAGE_EQ_EMPTY] THEN DISCH_TAC THEN AP_TERM_TAC THEN
1502     ABBREV_TAC `B = IMAGE (\h:real^N->bool. fa h:real^N,&0) J` THEN
1503     SUBGOAL_THEN `(B:real^N#real->bool) SUBSET A` ASSUME_TAC THENL
1504      [ASM SET_TAC[]; ALL_TAC] THEN
1505     SUBGOAL_THEN
1506      `INTERS (IMAGE (\t. (:real^N) DIFF t) H) =
1507       IMAGE (--) (interior s)`
1508     ASSUME_TAC THENL
1509      [MP_TAC(ISPECL [`s:real^N->bool`; `H:(real^N->bool)->bool`;
1510                      `fa:(real^N->bool)->real^N`;
1511                      `\h:real^N->bool. &0`]
1512                 RELATIVE_INTERIOR_POLYHEDRON_EXPLICIT) THEN
1513       ASM_SIMP_TAC[INTER_UNIV] THEN
1514       ASM_SIMP_TAC[RELATIVE_INTERIOR_INTERIOR] THEN
1515       DISCH_THEN(K ALL_TAC) THEN
1516       CONV_TAC SYM_CONV THEN MATCH_MP_TAC SURJECTIVE_IMAGE_EQ THEN
1517       REWRITE_TAC[VECTOR_ARITH `--x:real^N = y <=> x = --y`; EXISTS_REFL] THEN
1518       X_GEN_TAC `x:real^N` THEN REWRITE_TAC[IN_INTERS; IN_ELIM_THM] THEN
1519       REWRITE_TAC[FORALL_IN_IMAGE; IN_DIFF; IN_UNIV] THEN
1520       MATCH_MP_TAC(TAUT `(c ==> b) /\ (a <=> c) ==> (a <=> b /\ c)`) THEN
1521       CONJ_TAC THENL
1522        [EXPAND_TAC "s" THEN REWRITE_TAC[IN_INTERS] THEN
1523         MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `h:real^N->bool` THEN
1524         ASM_CASES_TAC `(h:real^N->bool) IN H` THEN ASM_REWRITE_TAC[] THEN
1525         ASM SET_TAC[REAL_LT_IMP_LE];
1526         MATCH_MP_TAC(MESON[]
1527          `(!h. P h ==> (Q h <=> R h))
1528           ==> ((!h. P h ==> Q h) <=> (!h. P h ==> R h))`) THEN
1529         X_GEN_TAC `h:real^N->bool` THEN DISCH_TAC THEN
1530         FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
1531          [SYM(CONJUNCT2(MATCH_MP th (ASSUME `(h:real^N->bool) IN H`)))]) THEN
1532         REWRITE_TAC[IN_ELIM_THM; DOT_RNEG] THEN REAL_ARITH_TAC];
1533       ALL_TAC] THEN
1534     SUBGOAL_THEN
1535      `hyperplane_cell B (INTERS (IMAGE (\t. (:real^N) DIFF t) J))`
1536     ASSUME_TAC THENL
1537      [SUBGOAL_THEN
1538        `~(INTERS (IMAGE (\t. (:real^N) DIFF t) J) = {})`
1539       MP_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
1540       REWRITE_TAC[hyperplane_cell; GSYM MEMBER_NOT_EMPTY; IN_INTERS] THEN
1541       REWRITE_TAC[FORALL_IN_IMAGE] THEN
1542       MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `z:real^N` THEN
1543       REWRITE_TAC[IN_UNIV; IN_DIFF] THEN
1544       GEN_REWRITE_TAC RAND_CONV [EXTENSION] THEN
1545       DISCH_THEN(fun th -> X_GEN_TAC `x:real^N` THEN MP_TAC th) THEN
1546       REWRITE_TAC[IN_INTERS; FORALL_IN_IMAGE; IN_DIFF; IN_UNIV] THEN
1547       GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [IN] THEN
1548       REWRITE_TAC[hyperplane_equiv] THEN EXPAND_TAC "B" THEN
1549       REWRITE_TAC[FORALL_IN_IMAGE; hyperplane_side] THEN
1550       MATCH_MP_TAC(MESON[]
1551        `(!h. P h ==> (Q h <=> R h))
1552         ==> (!h. P h) ==> ((!h. Q h) <=> (!h. R h))`) THEN
1553       X_GEN_TAC `h:real^N->bool` THEN
1554       ASM_CASES_TAC `(h:real^N->bool) IN J` THEN ASM_REWRITE_TAC[] THEN
1555       SUBGOAL_THEN `(h:real^N->bool) IN H` ASSUME_TAC THENL
1556        [ASM SET_TAC[]; ALL_TAC] THEN
1557       FIRST_X_ASSUM(MP_TAC o CONJUNCT2 o C MATCH_MP (ASSUME
1558        `(h:real^N->bool) IN H`)) THEN
1559       DISCH_THEN(fun th ->
1560         GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o ONCE_DEPTH_CONV) [SYM th] THEN
1561         GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [SYM th]) THEN
1562       REWRITE_TAC[IN_ELIM_THM; REAL_SUB_RZERO; REAL_NOT_LE] THEN
1563       MESON_TAC[REAL_SGN_EQ; real_gt];
1564       ALL_TAC] THEN
1565     MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC
1566      `euler_characteristic B (INTERS (IMAGE (\t. (:real^N) DIFF t) J))` THEN
1567     CONJ_TAC THENL
1568      [MATCH_MP_TAC EULER_CHARACTERSTIC_INVARIANT THEN
1569       ASM_SIMP_TAC[HYPERPLANE_CELL_CELLCOMPLEX] THEN
1570       CONJ_TAC THENL [ASM_MESON_TAC[FINITE_SUBSET]; ALL_TAC] THEN
1571       MATCH_MP_TAC HYPERPLANE_CELLCOMPLEX_MONO THEN
1572       EXISTS_TAC `B:real^N#real->bool` THEN
1573       ASM_SIMP_TAC[HYPERPLANE_CELL_CELLCOMPLEX];
1574       ALL_TAC] THEN
1575     ASM_SIMP_TAC[EULER_CHARACTERISTIC_CELL] THEN AP_TERM_TAC THEN
1576     MATCH_MP_TAC(MESON[NUM_OF_INT_OF_NUM] `i = &n ==> num_of_int i = n`) THEN
1577     REWRITE_TAC[AFF_DIM_EQ_FULL] THEN
1578     MATCH_MP_TAC(SET_RULE `!t. t SUBSET s /\ t = UNIV ==> s = UNIV`) THEN
1579     EXISTS_TAC `affine hull (INTERS (IMAGE (\t. (:real^N) DIFF t) H))` THEN
1580     CONJ_TAC THENL [MATCH_MP_TAC HULL_MONO THEN ASM SET_TAC[]; ALL_TAC] THEN
1581     MATCH_MP_TAC AFFINE_HULL_OPEN THEN ASM_REWRITE_TAC[] THEN
1582     ASM_SIMP_TAC[IMAGE_EQ_EMPTY; OPEN_NEGATIONS; OPEN_INTERIOR];
1583     ALL_TAC] THEN
1584   REWRITE_TAC[SUM_RMUL] THEN
1585   MATCH_MP_TAC(REAL_RING `s = &1 ==> s * t = t`) THEN
1586   MP_TAC(ISPECL [`\t:(real^N->bool)->bool. CARD t`;
1587                  `\t:(real^N->bool)->bool. (-- &1) pow (CARD t + 1)`;
1588                  `{t |  t SUBSET
1589                      {(:real^N) DIFF t | t IN H} /\ ~(t = {})}`;
1590                  `1..CARD(H:(real^N->bool)->bool)`]
1591         SUM_GROUP) THEN
1592   ANTS_TAC THENL
1593    [CONJ_TAC THENL
1594      [MATCH_MP_TAC FINITE_SUBSET THEN
1595       EXISTS_TAC `{t |  t SUBSET {(:real^N) DIFF t | t IN H}}` THEN
1596       CONJ_TAC THENL [ALL_TAC; SET_TAC[]] THEN
1597       MATCH_MP_TAC FINITE_POWERSET THEN REWRITE_TAC[SIMPLE_IMAGE] THEN
1598       ASM_SIMP_TAC[FINITE_IMAGE];
1599       GEN_REWRITE_TAC I [SUBSET] THEN REWRITE_TAC[FORALL_IN_IMAGE] THEN
1600       REWRITE_TAC[FORALL_IN_GSPEC; IN_NUMSEG] THEN
1601       REWRITE_TAC[SIMPLE_IMAGE; FORALL_SUBSET_IMAGE; IMP_CONJ] THEN
1602       X_GEN_TAC `J:(real^N->bool)->bool` THEN DISCH_TAC THEN
1603       REWRITE_TAC[IMAGE_EQ_EMPTY] THEN DISCH_TAC THEN
1604       SUBGOAL_THEN `FINITE(J:(real^N->bool)->bool)` ASSUME_TAC THENL
1605        [ASM_MESON_TAC[FINITE_SUBSET]; ALL_TAC] THEN
1606       ASM_SIMP_TAC[CARD_EQ_0; FINITE_IMAGE; ARITH_RULE `1 <= n <=> ~(n = 0)`;
1607                    IMAGE_EQ_EMPTY] THEN
1608       MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `CARD(J:(real^N->bool)->bool)` THEN
1609       ASM_SIMP_TAC[CARD_SUBSET; CARD_IMAGE_LE]];
1610     REWRITE_TAC[] THEN DISCH_THEN(SUBST1_TAC o SYM)] THEN
1611   MATCH_MP_TAC EQ_TRANS THEN
1612   EXISTS_TAC
1613    `sum (1..CARD(H:(real^N->bool)->bool))
1614         (\n. -- &1 pow (n + 1) * &(binom(CARD H,n)))` THEN
1615   CONJ_TAC THENL
1616    [MATCH_MP_TAC SUM_EQ THEN X_GEN_TAC `n:num` THEN
1617     REWRITE_TAC[IN_NUMSEG] THEN DISCH_TAC THEN
1618     SIMP_TAC[IN_ELIM_THM] THEN
1619     W(MP_TAC o PART_MATCH (lhs o rand) SUM_CONST o lhand o snd) THEN
1620     ANTS_TAC THENL
1621      [MATCH_MP_TAC FINITE_SUBSET THEN
1622       EXISTS_TAC `{t |  t SUBSET {(:real^N) DIFF t | t IN H}}` THEN
1623       CONJ_TAC THENL [ALL_TAC; SET_TAC[]] THEN
1624       MATCH_MP_TAC FINITE_POWERSET THEN REWRITE_TAC[SIMPLE_IMAGE] THEN
1625       ASM_SIMP_TAC[FINITE_IMAGE];
1626       DISCH_THEN SUBST1_TAC] THEN
1627     GEN_REWRITE_TAC LAND_CONV [REAL_MUL_SYM] THEN AP_TERM_TAC THEN
1628     AP_TERM_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
1629     EXISTS_TAC `CARD {t | t SUBSET {(:real^N) DIFF t | t IN H} /\
1630                           t HAS_SIZE n}` THEN
1631     CONJ_TAC THENL
1632      [AP_TERM_TAC THEN GEN_REWRITE_TAC I [EXTENSION] THEN
1633       X_GEN_TAC `t:(real^N->bool)->bool` THEN
1634       REWRITE_TAC[IN_ELIM_THM] THEN
1635       ASM_CASES_TAC `t:(real^N->bool)->bool = {}` THEN
1636       ASM_REWRITE_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_EMPTY] THENL
1637        [ASM_ARITH_TAC; ALL_TAC] THEN
1638       MATCH_MP_TAC(TAUT `(p ==> r) ==> (p /\ q <=> p /\ r /\ q)`) THEN
1639       SPEC_TAC(`t:(real^N->bool)->bool`,`u:(real^N->bool)->bool`) THEN
1640       REWRITE_TAC[SIMPLE_IMAGE; FORALL_SUBSET_IMAGE] THEN
1641       ASM_MESON_TAC[FINITE_IMAGE; FINITE_SUBSET];
1642       ALL_TAC] THEN
1643     MP_TAC(ISPECL [`CARD(H:(real^N->bool)->bool)`;
1644                    `n:num`; `{(:real^N) DIFF t | t IN H}`]
1645         NUMBER_OF_COMBINATIONS) THEN
1646     ANTS_TAC THENL [ALL_TAC; SIMP_TAC[HAS_SIZE]] THEN
1647     REWRITE_TAC[SIMPLE_IMAGE] THEN MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN
1648     ASM_REWRITE_TAC[GSYM FINITE_HAS_SIZE] THEN SET_TAC[];
1649     ALL_TAC] THEN
1650   MP_TAC(ISPECL [`CARD(H:(real^N->bool)->bool)`; `--(&1)`; `&1`]
1651         REAL_BINOMIAL_THEOREM) THEN
1652   REWRITE_TAC[REAL_POW_ONE; REAL_MUL_RID; REAL_ADD_LINV] THEN
1653   SIMP_TAC[SUM_CLAUSES_LEFT; REAL_POW_ADD; REAL_POW_ONE; LE_0] THEN
1654   REWRITE_TAC[REAL_ARITH `(x * --(&1) pow 1) * y = --(y * x)`] THEN
1655   REWRITE_TAC[real_pow; SUM_NEG; ADD_CLAUSES; REAL_MUL_RID] THEN
1656   REWRITE_TAC[binom] THEN MATCH_MP_TAC(REAL_ARITH
1657    `x = &0 ==> x = &1 + y ==> --y = &1`) THEN
1658   REWRITE_TAC[REAL_POW_ZERO] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
1659   UNDISCH_TAC `CARD(H:(real^N->bool)->bool) = 0` THEN
1660   ASM_SIMP_TAC[CARD_EQ_0] THEN DISCH_THEN SUBST_ALL_TAC THEN ASM SET_TAC[]);;
1661
1662 (* ------------------------------------------------------------------------- *)
1663 (* Euler-Poincare relation for special (n-1)-dimensional polytope.           *)
1664 (* ------------------------------------------------------------------------- *)
1665
1666 let EULER_POINCARE_LEMMA = prove
1667  (`!p:real^N->bool.
1668         2 <= dimindex(:N) /\ polytope p /\ affine hull p = {x | x$1 = &1}
1669         ==> sum (0..dimindex(:N)-1)
1670                (\d. (-- &1) pow d *
1671                     &(CARD {f | f face_of p /\ aff_dim f = &d })) = &1`,
1672   REPEAT STRIP_TAC THEN
1673   MP_TAC(ISPECL [`basis 1:real^N`; `&1`] AFF_DIM_HYPERPLANE) THEN
1674   SIMP_TAC[BASIS_NONZERO; DOT_BASIS; DIMINDEX_GE_1; LE_REFL] THEN
1675   FIRST_ASSUM(SUBST1_TAC o SYM) THEN REWRITE_TAC[AFF_DIM_AFFINE_HULL] THEN
1676   ASM_CASES_TAC `p:real^N->bool = {}` THENL
1677    [ASM_REWRITE_TAC[AFF_DIM_EMPTY] THEN
1678     REWRITE_TAC[INT_ARITH `--(&1):int = x - &1 <=> x = &0`] THEN
1679     SIMP_TAC[INT_OF_NUM_EQ; LE_1; DIMINDEX_GE_1];
1680     DISCH_TAC] THEN
1681   ABBREV_TAC `s:real^N->bool = conic hull p` THEN
1682   MP_TAC(ISPEC `s:real^N->bool` EULER_POLYHEDRAL_CONE) THEN
1683   SUBGOAL_THEN
1684    `!f. f SUBSET {x:real^N | x$1 = &1}
1685         ==> (conic hull f) INTER {x:real^N | x$1 = &1} = f`
1686   ASSUME_TAC THENL
1687    [GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC SUBSET_ANTISYM THEN
1688     ASM_SIMP_TAC[HULL_SUBSET; SUBSET_INTER] THEN
1689     REWRITE_TAC[SUBSET; CONIC_HULL_EXPLICIT; IN_INTER; IMP_CONJ] THEN
1690     REWRITE_TAC[FORALL_IN_GSPEC] THEN
1691     MAP_EVERY X_GEN_TAC [`c:real`; `x:real^N`] THEN DISCH_TAC THEN
1692     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [SUBSET]) THEN
1693     DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN
1694     ASM_SIMP_TAC[VECTOR_MUL_COMPONENT; REAL_MUL_RID; VECTOR_MUL_LID];
1695     ALL_TAC] THEN
1696   SUBGOAL_THEN `polyhedron(s:real^N->bool)` ASSUME_TAC THENL
1697    [EXPAND_TAC "s" THEN
1698     FIRST_X_ASSUM(X_CHOOSE_THEN `k:real^N->bool` MP_TAC o
1699       GEN_REWRITE_RULE I [polytope]) THEN
1700     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1701     DISCH_THEN(fun th -> SUBST1_TAC th THEN ASSUME_TAC th) THEN
1702     MP_TAC(ISPEC `k:real^N->bool` CONVEX_CONE_HULL_SEPARATE_NONEMPTY) THEN
1703     ANTS_TAC THENL [ASM_MESON_TAC[CONVEX_HULL_EQ_EMPTY]; ALL_TAC] THEN
1704     DISCH_THEN(SUBST1_TAC o SYM) THEN
1705     MATCH_MP_TAC POLYHEDRON_CONVEX_CONE_HULL THEN ASM_REWRITE_TAC[];
1706     ALL_TAC] THEN
1707   FIRST_ASSUM(ASSUME_TAC o MATCH_MP POLYHEDRON_IMP_CONVEX) THEN
1708   SUBGOAL_THEN `conic(s:real^N->bool)` ASSUME_TAC THENL
1709    [ASM_MESON_TAC[CONIC_CONIC_HULL]; ALL_TAC] THEN
1710   SUBGOAL_THEN `~(s = (:real^N))` ASSUME_TAC THENL
1711    [DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `p:real^N->bool`) THEN
1712     ANTS_TAC THENL [ASM_MESON_TAC[HULL_SUBSET]; ALL_TAC] THEN
1713     ASM_REWRITE_TAC[INTER_UNIV] THEN DISCH_THEN(ASSUME_TAC o SYM) THEN
1714     UNDISCH_TAC `polytope(p:real^N->bool)` THEN ASM_REWRITE_TAC[] THEN
1715     DISCH_THEN(MP_TAC o MATCH_MP POLYTOPE_IMP_BOUNDED) THEN
1716     REWRITE_TAC[BOUNDED_POS; NOT_EXISTS_THM] THEN X_GEN_TAC `B:real` THEN
1717     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1718     DISCH_THEN(MP_TAC o SPEC
1719      `(lambda i. if i = 1 then &1 else B + &1):real^N`) THEN
1720     SIMP_TAC[LAMBDA_BETA; DIMINDEX_GE_1; LE_REFL; IN_ELIM_THM] THEN
1721     REWRITE_TAC[REAL_NOT_LE] THEN
1722     MP_TAC(ISPECL
1723     [`(lambda i. if i = 1 then &1 else B + &1):real^N`; `2`]
1724       COMPONENT_LE_NORM) THEN
1725     ASM_SIMP_TAC[ARITH; LAMBDA_BETA; DIMINDEX_GE_1; LE_REFL] THEN
1726     REAL_ARITH_TAC;
1727     ALL_TAC] THEN
1728   SUBGOAL_THEN `~(s:real^N->bool = {})` ASSUME_TAC THENL
1729    [ASM_MESON_TAC[CONIC_HULL_EQ_EMPTY]; ALL_TAC] THEN
1730   MP_TAC(ISPEC `s:real^N->bool` CONIC_CONTAINS_0) THEN
1731   ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1732   SUBGOAL_THEN `~(interior(s:real^N->bool) = {})` ASSUME_TAC THENL
1733    [DISCH_TAC THEN MP_TAC(ISPEC `s:real^N->bool`
1734      EMPTY_INTERIOR_SUBSET_HYPERPLANE) THEN
1735     ASM_REWRITE_TAC[NOT_EXISTS_THM] THEN
1736     MAP_EVERY X_GEN_TAC [`a:real^N`; `b:real`] THEN STRIP_TAC THEN
1737     SUBGOAL_THEN `s SUBSET {x:real^N | x$1 = &1}` MP_TAC THENL
1738      [FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
1739        `s SUBSET h' ==> h SUBSET h' /\ ~(h PSUBSET h') ==> s SUBSET h`)) THEN
1740       CONJ_TAC THENL
1741        [FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [SYM th]) THEN
1742         MATCH_MP_TAC HULL_MINIMAL THEN REWRITE_TAC[AFFINE_HYPERPLANE] THEN
1743         MATCH_MP_TAC SUBSET_TRANS THEN EXISTS_TAC `s:real^N->bool` THEN
1744         ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[HULL_SUBSET];
1745         DISCH_TAC THEN
1746         MP_TAC(ISPECL [`a:real^N`; `b:real`] AFF_DIM_HYPERPLANE) THEN
1747         MP_TAC(ISPECL [`basis 1:real^N`; `&1`] AFF_DIM_HYPERPLANE) THEN
1748         ASM_SIMP_TAC[BASIS_NONZERO; DOT_BASIS; DIMINDEX_GE_1; LE_REFL] THEN
1749         MATCH_MP_TAC(INT_ARITH `a:int < b ==> a = n ==> ~(b = n)`) THEN
1750         MATCH_MP_TAC AFF_DIM_PSUBSET THEN FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP
1751          (SET_RULE `s PSUBSET t ==> s' = s /\ t' = t ==> s' PSUBSET t'`)) THEN
1752         REWRITE_TAC[AFFINE_HULL_EQ; AFFINE_HYPERPLANE] THEN
1753         MP_TAC(ISPECL [`basis 1:real^N`; `&1`] AFFINE_HYPERPLANE) THEN
1754         SIMP_TAC[BASIS_NONZERO; DOT_BASIS; DIMINDEX_GE_1; LE_REFL]];
1755       REWRITE_TAC[SUBSET; NOT_FORALL_THM; NOT_IMP] THEN
1756       EXISTS_TAC `vec 0:real^N` THEN
1757       ASM_REWRITE_TAC[IN_ELIM_THM; VEC_COMPONENT] THEN REAL_ARITH_TAC];
1758     ALL_TAC] THEN
1759   ASM_REWRITE_TAC[] THEN
1760   SUBGOAL_THEN `!x:real^N. x IN s /\ ~(x = vec 0) ==> &0 < x$1`
1761   ASSUME_TAC THENL
1762    [EXPAND_TAC "s" THEN REWRITE_TAC[CONIC_HULL_EXPLICIT; IMP_CONJ] THEN
1763     REWRITE_TAC[FORALL_IN_GSPEC; VECTOR_MUL_EQ_0; DE_MORGAN_THM] THEN
1764     MAP_EVERY X_GEN_TAC [`c:real`; `x:real^N`] THEN REPEAT STRIP_TAC THEN
1765     REWRITE_TAC[VECTOR_MUL_COMPONENT] THEN MATCH_MP_TAC REAL_LT_MUL THEN
1766     CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
1767     SUBGOAL_THEN `(x:real^N) IN affine hull p` MP_TAC THENL
1768      [ASM_MESON_TAC[HULL_SUBSET; SUBSET]; ASM_REWRITE_TAC[]] THEN
1769     SIMP_TAC[IN_ELIM_THM; REAL_LT_01];
1770     ALL_TAC] THEN
1771   SUBGOAL_THEN `!x:real^N. x IN s ==> &0 <= x$1` ASSUME_TAC THENL
1772    [X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
1773     ASM_CASES_TAC `x:real^N = vec 0` THEN
1774     ASM_SIMP_TAC[VEC_COMPONENT; REAL_POS; REAL_LT_IMP_LE];
1775     ALL_TAC] THEN
1776   W(MP_TAC o PART_MATCH (lhs o rand) SUM_CLAUSES_LEFT o
1777     lhand o lhand o snd) THEN
1778   REWRITE_TAC[LE_0] THEN DISCH_THEN SUBST1_TAC THEN
1779   REWRITE_TAC[AFF_DIM_EQ_0; real_pow; REAL_MUL_LID] THEN
1780   SUBGOAL_THEN `{f | f face_of s /\ (?a:real^N. f = {a})} = {{vec 0}}`
1781    (fun th -> REWRITE_TAC[th])
1782   THENL
1783    [GEN_REWRITE_TAC I [EXTENSION] THEN REWRITE_TAC[IN_ELIM_THM; IN_SING] THEN
1784     X_GEN_TAC `f:real^N->bool` THEN EQ_TAC THENL
1785      [DISCH_THEN(CONJUNCTS_THEN2 MP_TAC (X_CHOOSE_TAC `a:real^N`)) THEN
1786       ASM_REWRITE_TAC[FACE_OF_SING] THEN
1787       ASM_MESON_TAC[EXTREME_POINT_OF_CONIC];
1788       DISCH_THEN SUBST1_TAC THEN CONJ_TAC THENL [ALL_TAC; MESON_TAC[]] THEN
1789       ASM_REWRITE_TAC[FACE_OF_SING; extreme_point_of; IN_SEGMENT] THEN
1790       MAP_EVERY X_GEN_TAC [`a:real^N`; `b:real^N`] THEN STRIP_TAC THEN
1791       DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1792       REWRITE_TAC[NOT_EXISTS_THM] THEN X_GEN_TAC `u:real` THEN
1793       REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
1794       REWRITE_TAC[CART_EQ] THEN DISCH_THEN(MP_TAC o SPEC `1`) THEN
1795       REWRITE_TAC[LE_REFL; DIMINDEX_GE_1; VEC_COMPONENT] THEN
1796       REWRITE_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT] THEN
1797       SUBGOAL_THEN `&0 < (a:real^N)$1 \/ &0 < (b:real^N)$1` DISJ_CASES_TAC THENL
1798        [ASM_MESON_TAC[];
1799         MATCH_MP_TAC(REAL_ARITH `&0 < a /\ &0 <= b ==> ~(&0 = a + b)`);
1800         MATCH_MP_TAC(REAL_ARITH `&0 < b /\ &0 <= a ==> ~(&0 = a + b)`)] THEN
1801       ASM_SIMP_TAC[REAL_LE_MUL; REAL_LT_IMP_LE; REAL_LT_MUL; REAL_SUB_LT]];
1802     ALL_TAC] THEN
1803   SIMP_TAC[CARD_CLAUSES; FINITE_EMPTY; NOT_IN_EMPTY; GSYM REAL_OF_NUM_SUC] THEN
1804   MATCH_MP_TAC(REAL_ARITH `s = --t ==> (&0 + &1) + s = &0 ==> t = &1`) THEN
1805   SUBGOAL_THEN `dimindex(:N) = (dimindex(:N)-1)+1`
1806    (fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th])
1807   THENL [ASM_ARITH_TAC; ALL_TAC] THEN
1808   REWRITE_TAC[SUM_OFFSET; GSYM SUM_NEG] THEN
1809   MATCH_MP_TAC SUM_EQ_NUMSEG THEN X_GEN_TAC `d:num` THEN STRIP_TAC THEN
1810   REWRITE_TAC[REAL_POW_ADD; REAL_POW_1; REAL_MUL_RNEG; REAL_MUL_LNEG] THEN
1811   AP_TERM_TAC THEN REWRITE_TAC[REAL_MUL_RID] THEN AP_TERM_TAC THEN
1812   AP_TERM_TAC THEN MATCH_MP_TAC BIJECTIONS_CARD_EQ THEN
1813   EXISTS_TAC `\f:real^N->bool. f INTER {x | x$1 = &1}` THEN
1814   EXISTS_TAC `\f:real^N->bool. conic hull f` THEN
1815   REWRITE_TAC[FORALL_IN_GSPEC] THEN CONJ_TAC THENL
1816    [DISJ1_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN
1817     EXISTS_TAC `{f:real^N->bool | f face_of s}` THEN
1818     ASM_SIMP_TAC[FINITE_POLYHEDRON_FACES] THEN SET_TAC[];
1819     REWRITE_TAC[IN_ELIM_THM; GSYM INT_OF_NUM_ADD]] THEN
1820   SUBGOAL_THEN
1821    `!f:real^N->bool. f face_of p ==> conic hull f INTER {x | x$1 = &1} = f`
1822   ASSUME_TAC THENL
1823    [GEN_TAC THEN DISCH_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
1824     MATCH_MP_TAC SUBSET_TRANS THEN
1825     EXISTS_TAC `affine hull p:real^N->bool` THEN CONJ_TAC THENL
1826      [ASM_MESON_TAC[FACE_OF_IMP_SUBSET; HULL_SUBSET; SUBSET_TRANS];
1827       ASM_REWRITE_TAC[SUBSET_REFL]];
1828     ASM_SIMP_TAC[]] THEN
1829   SUBGOAL_THEN
1830    `!f:real^N->bool. f face_of s ==> f INTER {x | x$1 = &1} face_of p`
1831   ASSUME_TAC THENL
1832    [REPEAT STRIP_TAC THEN
1833     SUBGOAL_THEN `p = conic hull p INTER {x:real^N | x$1 = &1}` SUBST1_TAC
1834     THENL [ASM_MESON_TAC[FACE_OF_REFL; POLYTOPE_IMP_CONVEX]; ALL_TAC] THEN
1835     MATCH_MP_TAC FACE_OF_SLICE THEN
1836     ASM_REWRITE_TAC[CONVEX_STANDARD_HYPERPLANE];
1837     ASM_SIMP_TAC[]] THEN
1838   SUBGOAL_THEN
1839    `!f. f face_of s  /\ &0 < aff_dim f
1840         ==> conic hull (f INTER {x:real^N | x$1 = &1}) = f`
1841   ASSUME_TAC THENL
1842    [REPEAT STRIP_TAC THEN MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL
1843      [REWRITE_TAC[SUBSET; CONIC_HULL_EXPLICIT; FORALL_IN_GSPEC] THEN
1844       REWRITE_TAC[IN_INTER; IN_ELIM_THM] THEN
1845       ASM_MESON_TAC[FACE_OF_CONIC; conic];
1846       REWRITE_TAC[SUBSET; CONIC_HULL_EXPLICIT] THEN X_GEN_TAC `x:real^N` THEN
1847       DISCH_TAC THEN REWRITE_TAC[IN_ELIM_THM; IN_INTER] THEN
1848       ASM_CASES_TAC `x:real^N = vec 0` THENL
1849        [SUBGOAL_THEN `?y:real^N. y IN f /\ ~(y = vec 0)` STRIP_ASSUME_TAC THENL
1850          [MATCH_MP_TAC(SET_RULE
1851            `a IN s /\ ~(s = {a}) ==> ?y. y IN s /\ ~(y = a)`) THEN
1852           ASM_MESON_TAC[AFF_DIM_EQ_0; INT_LT_REFL];
1853           SUBGOAL_THEN `&0 < (y:real^N)$1` ASSUME_TAC THENL
1854            [ASM_MESON_TAC[FACE_OF_IMP_SUBSET; SUBSET]; ALL_TAC] THEN
1855           EXISTS_TAC `&0` THEN ASM_REWRITE_TAC[REAL_POS; VECTOR_MUL_LZERO] THEN
1856           EXISTS_TAC `inv(y$1) % y:real^N` THEN
1857           ASM_SIMP_TAC[VECTOR_MUL_COMPONENT; REAL_MUL_LINV;
1858                        REAL_LT_IMP_NZ] THEN
1859           ASM_MESON_TAC[FACE_OF_CONIC; conic; REAL_LE_INV_EQ; REAL_LT_IMP_LE]];
1860         SUBGOAL_THEN `&0 < (x:real^N)$1` ASSUME_TAC THENL
1861          [ASM_MESON_TAC[FACE_OF_IMP_SUBSET; SUBSET]; ALL_TAC] THEN
1862         EXISTS_TAC `(x:real^N)$1` THEN EXISTS_TAC `inv(x$1) % x:real^N` THEN
1863         ASM_SIMP_TAC[VECTOR_MUL_COMPONENT; REAL_MUL_LINV; REAL_LT_IMP_LE;
1864           REAL_LT_IMP_NZ; VECTOR_MUL_ASSOC; REAL_MUL_RINV; VECTOR_MUL_LID] THEN
1865         ASM_MESON_TAC[FACE_OF_CONIC; conic; REAL_LE_INV_EQ; REAL_LT_IMP_LE]]];
1866     ASM_SIMP_TAC[INT_ARITH `&0:int < &d + &1`]] THEN
1867   SUBGOAL_THEN
1868    `!f:real^N->bool. f face_of p ==> (conic hull f) face_of s`
1869   ASSUME_TAC THENL
1870    [REPEAT STRIP_TAC THEN ASM_CASES_TAC `f:real^N->bool = {}` THEN
1871     ASM_REWRITE_TAC[CONIC_HULL_EMPTY; EMPTY_FACE_OF] THEN
1872     REWRITE_TAC[face_of] THEN REPEAT CONJ_TAC THENL
1873      [EXPAND_TAC "s" THEN MATCH_MP_TAC HULL_MONO THEN
1874       ASM_MESON_TAC[FACE_OF_IMP_SUBSET];
1875       ASM_MESON_TAC[CONVEX_CONIC_HULL; FACE_OF_IMP_CONVEX];
1876       ALL_TAC] THEN
1877     EXPAND_TAC "s" THEN REWRITE_TAC[CONIC_HULL_EXPLICIT; IMP_CONJ] THEN
1878     REWRITE_TAC[RIGHT_FORALL_IMP_THM; FORALL_IN_GSPEC] THEN
1879     MAP_EVERY X_GEN_TAC [`ca:real`; `a:real^N`] THEN STRIP_TAC THEN
1880     MAP_EVERY X_GEN_TAC [`cb:real`; `b:real^N`] THEN STRIP_TAC THEN
1881     MAP_EVERY X_GEN_TAC [`cx:real`; `x:real^N`] THEN STRIP_TAC THEN
1882     ASM_CASES_TAC `cx % x:real^N = vec 0` THENL
1883      [ASM_REWRITE_TAC[IN_SEGMENT] THEN
1884       MATCH_MP_TAC(TAUT `(a ==> ~b) ==> a /\ b ==> c`) THEN
1885       DISCH_TAC THEN DISCH_THEN(X_CHOOSE_THEN `u:real` MP_TAC) THEN
1886       REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
1887       REWRITE_TAC[CART_EQ] THEN DISCH_THEN(MP_TAC o SPEC `1`) THEN
1888       REWRITE_TAC[LE_REFL; DIMINDEX_GE_1; VEC_COMPONENT] THEN
1889       REWRITE_TAC[VECTOR_ADD_COMPONENT] THEN
1890       ONCE_REWRITE_TAC[VECTOR_MUL_COMPONENT] THEN
1891       SUBGOAL_THEN `&0 < (ca % a:real^N)$1 \/ &0 < (cb % b:real^N)$1`
1892       DISJ_CASES_TAC THENL
1893        [SUBGOAL_THEN `(ca % a:real^N) IN s /\ (cb % b:real^N) IN s`
1894           (fun th -> ASM_MESON_TAC[th]) THEN
1895         ASM_MESON_TAC[conic; HULL_SUBSET; SUBSET];
1896         MATCH_MP_TAC(REAL_ARITH `&0 < a /\ &0 <= b ==> ~(&0 = a + b)`);
1897         MATCH_MP_TAC(REAL_ARITH `&0 < b /\ &0 <= a ==> ~(&0 = a + b)`)] THEN
1898       ASM_SIMP_TAC[REAL_LE_MUL; REAL_LT_IMP_LE; REAL_LT_MUL; REAL_SUB_LT] THEN
1899       MATCH_MP_TAC REAL_LE_MUL THEN
1900       ASM_SIMP_TAC[REAL_LT_IMP_LE; REAL_SUB_LT] THEN
1901       FIRST_X_ASSUM MATCH_MP_TAC THEN
1902       ASM_MESON_TAC[conic; HULL_SUBSET; SUBSET];
1903       ALL_TAC] THEN
1904     UNDISCH_TAC `~(cx % x:real^N = vec 0)` THEN
1905     REWRITE_TAC[VECTOR_MUL_EQ_0; DE_MORGAN_THM] THEN STRIP_TAC THEN
1906     ASM_CASES_TAC `x:real^N = a` THENL
1907      [REWRITE_TAC[IN_SEGMENT] THEN DISCH_THEN
1908        (CONJUNCTS_THEN2 ASSUME_TAC (X_CHOOSE_THEN `u:real` MP_TAC)) THEN
1909       REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
1910       ASM_REWRITE_TAC[VECTOR_MUL_ASSOC; VECTOR_ARITH
1911        `x % a:real^N = y % a + z % b <=> (x - y) % a = z % b`] THEN
1912       DISCH_THEN(fun th -> MP_TAC th THEN MP_TAC th) THEN
1913       GEN_REWRITE_TAC LAND_CONV [CART_EQ] THEN
1914       DISCH_THEN(MP_TAC o SPEC `1`) THEN
1915       REWRITE_TAC[LE_REFL; DIMINDEX_GE_1; VECTOR_MUL_COMPONENT] THEN
1916       SUBGOAL_THEN `(a:real^N) IN affine hull p /\ b IN affine hull p`
1917       MP_TAC THENL
1918        [ASM_MESON_TAC[FACE_OF_IMP_SUBSET; HULL_SUBSET; SUBSET]; ALL_TAC] THEN
1919       ASM_REWRITE_TAC[IN_ELIM_THM] THEN
1920       DISCH_THEN(CONJUNCTS_THEN SUBST1_TAC) THEN
1921       REWRITE_TAC[REAL_MUL_RID] THEN DISCH_THEN SUBST1_TAC THEN
1922       ASM_SIMP_TAC[VECTOR_MUL_LCANCEL; REAL_ENTIRE; REAL_LT_IMP_NZ] THEN
1923       STRIP_TAC THEN ASM_REWRITE_TAC[] THENL
1924        [CONJ_TAC THENL
1925          [MAP_EVERY EXISTS_TAC [`ca:real`; `a:real^N`] THEN
1926           ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[];
1927           MAP_EVERY EXISTS_TAC [`&0`; `x:real^N`] THEN
1928           ASM_REWRITE_TAC[VECTOR_MUL_LZERO; REAL_LE_REFL]];
1929         CONJ_TAC THENL [EXISTS_TAC `ca:real`; EXISTS_TAC `cb:real`] THEN
1930         EXISTS_TAC `x:real^N` THEN ASM_REWRITE_TAC[]];
1931       ALL_TAC] THEN
1932     ASM_CASES_TAC `x:real^N = b` THENL
1933      [REWRITE_TAC[IN_SEGMENT] THEN DISCH_THEN
1934        (CONJUNCTS_THEN2 ASSUME_TAC (X_CHOOSE_THEN `u:real` MP_TAC)) THEN
1935       REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
1936       ASM_REWRITE_TAC[VECTOR_MUL_ASSOC; VECTOR_ARITH
1937        `x % b:real^N = y % a + z % b <=> (x - z) % b = y % a`] THEN
1938       DISCH_THEN(fun th -> MP_TAC th THEN MP_TAC th) THEN
1939       GEN_REWRITE_TAC LAND_CONV [CART_EQ] THEN
1940       DISCH_THEN(MP_TAC o SPEC `1`) THEN
1941       REWRITE_TAC[LE_REFL; DIMINDEX_GE_1; VECTOR_MUL_COMPONENT] THEN
1942       SUBGOAL_THEN `(a:real^N) IN affine hull p /\ b IN affine hull p`
1943       MP_TAC THENL
1944        [ASM_MESON_TAC[FACE_OF_IMP_SUBSET; HULL_SUBSET; SUBSET]; ALL_TAC] THEN
1945       ASM_REWRITE_TAC[IN_ELIM_THM] THEN
1946       DISCH_THEN(CONJUNCTS_THEN SUBST1_TAC) THEN
1947       REWRITE_TAC[REAL_MUL_RID] THEN DISCH_THEN SUBST1_TAC THEN
1948       ASM_SIMP_TAC[VECTOR_MUL_LCANCEL; REAL_ENTIRE;
1949                    REAL_LT_IMP_NE; REAL_SUB_0] THEN
1950       STRIP_TAC THEN ASM_REWRITE_TAC[] THENL
1951        [CONJ_TAC THENL
1952          [MAP_EVERY EXISTS_TAC [`&0`; `x:real^N`] THEN
1953           ASM_REWRITE_TAC[VECTOR_MUL_LZERO; REAL_LE_REFL];
1954           MAP_EVERY EXISTS_TAC [`cb:real`; `b:real^N`] THEN
1955           ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]];
1956         CONJ_TAC THENL [EXISTS_TAC `ca:real`; EXISTS_TAC `cb:real`] THEN
1957         EXISTS_TAC `x:real^N` THEN ASM_REWRITE_TAC[]];
1958       ALL_TAC] THEN
1959     DISCH_TAC THEN
1960     SUBGOAL_THEN `(x:real^N) IN segment(a,b)` ASSUME_TAC THENL
1961      [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [IN_OPEN_SEGMENT]) THEN
1962       ASM_REWRITE_TAC[IN_OPEN_SEGMENT] THEN
1963       DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN
1964       REWRITE_TAC[IN_SEGMENT] THEN
1965       DISCH_THEN(X_CHOOSE_THEN `u:real` MP_TAC) THEN
1966       REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
1967       DISCH_THEN(fun th -> MP_TAC th THEN MP_TAC th) THEN
1968       GEN_REWRITE_TAC LAND_CONV [CART_EQ] THEN
1969       DISCH_THEN(MP_TAC o SPEC `1`) THEN
1970       REWRITE_TAC[LE_REFL; DIMINDEX_GE_1; VECTOR_ADD_COMPONENT;
1971                   VECTOR_MUL_COMPONENT] THEN
1972       SUBGOAL_THEN `(x:real^N) IN affine hull p /\
1973                     a IN affine hull p /\ b IN affine hull p`
1974       MP_TAC THENL
1975        [ASM_MESON_TAC[FACE_OF_IMP_SUBSET; HULL_SUBSET; SUBSET]; ALL_TAC] THEN
1976       ASM_REWRITE_TAC[IN_ELIM_THM] THEN
1977       DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN SUBST1_TAC) THEN
1978       REWRITE_TAC[REAL_MUL_RID] THEN DISCH_THEN(ASSUME_TAC o SYM) THEN
1979       DISCH_THEN(MP_TAC o AP_TERM `(%) (inv cx) :real^N->real^N`) THEN
1980       ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
1981       DISCH_THEN(K ALL_TAC) THEN EXISTS_TAC `inv(cx) * u * cb` THEN
1982       REWRITE_TAC[REAL_ARITH `inv(cx) * x:real = x / cx`] THEN
1983       ASM_SIMP_TAC[REAL_LE_RDIV_EQ; REAL_LE_LDIV_EQ; REAL_LT_LE] THEN
1984       REPEAT CONJ_TAC THENL
1985        [REWRITE_TAC[REAL_MUL_LZERO] THEN MATCH_MP_TAC REAL_LE_MUL THEN
1986         ASM_REAL_ARITH_TAC;
1987         FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
1988          `a + b = cx ==> &0 <= a ==> b <= &1 * cx`)) THEN
1989         MATCH_MP_TAC REAL_LE_MUL THEN ASM_REAL_ARITH_TAC;
1990         REWRITE_TAC[VECTOR_MUL_ASSOC; VECTOR_ADD_LDISTRIB] THEN
1991         BINOP_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
1992         MAP_EVERY UNDISCH_TAC
1993          [`(&1 - u) * ca + u * cb = cx`; `~(cx = &0)`] THEN
1994         CONV_TAC REAL_FIELD];
1995       FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [face_of]) THEN
1996       REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
1997       DISCH_THEN(MP_TAC o SPECL [`a:real^N`; `b:real^N`; `x:real^N`]) THEN
1998       ASM_REWRITE_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[]];
1999     ASM_SIMP_TAC[]] THEN
2000   SUBGOAL_THEN
2001    `!f:real^N->bool. f face_of p /\ ~(f = {})
2002                      ==> aff_dim(conic hull f) = aff_dim f + &1`
2003   (LABEL_TAC "*") THENL
2004    [ALL_TAC;
2005     CONJ_TAC THEN X_GEN_TAC `f:real^N->bool` THEN STRIP_TAC THENL
2006      [REMOVE_THEN "*" (MP_TAC o SPEC `f INTER {x:real^N | x$1 = &1}`) THEN
2007       ASM_SIMP_TAC[INT_ARITH `&0:int < &d + &1`; INT_EQ_ADD_RCANCEL] THEN
2008       ANTS_TAC THENL [ALL_TAC; SIMP_TAC[]] THEN
2009       SUBGOAL_THEN `?y:real^N. y IN f /\ ~(y = vec 0)` STRIP_ASSUME_TAC THENL
2010        [MATCH_MP_TAC(SET_RULE
2011          `a IN s /\ ~(s = {a}) ==> ?y. y IN s /\ ~(y = a)`) THEN
2012         CONJ_TAC THENL
2013          [MP_TAC(ISPECL [`s:real^N->bool`; `f:real^N->bool`]
2014             FACE_OF_CONIC) THEN
2015           ASM_SIMP_TAC[CONIC_CONTAINS_0] THEN REPEAT DISCH_TAC;
2016           DISCH_TAC] THEN
2017         UNDISCH_TAC `aff_dim(f:real^N->bool) = &d + &1` THEN
2018         ASM_REWRITE_TAC[AFF_DIM_SING; AFF_DIM_EMPTY] THEN INT_ARITH_TAC;
2019         REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER; IN_ELIM_THM] THEN
2020         SUBGOAL_THEN `&0 < (y:real^N)$1` ASSUME_TAC THENL
2021          [ASM_MESON_TAC[FACE_OF_IMP_SUBSET; SUBSET]; ALL_TAC] THEN
2022         EXISTS_TAC `inv(y$1) % y:real^N` THEN
2023         ASM_SIMP_TAC[VECTOR_MUL_COMPONENT; REAL_MUL_LINV;
2024                      REAL_LT_IMP_NZ] THEN
2025         MP_TAC(ISPECL [`s:real^N->bool`; `f:real^N->bool`]
2026           FACE_OF_CONIC) THEN
2027         ASM_SIMP_TAC[CONIC_CONTAINS_0] THEN
2028         REWRITE_TAC[conic] THEN DISCH_THEN MATCH_MP_TAC THEN
2029         ASM_SIMP_TAC[REAL_LE_INV_EQ; REAL_LT_IMP_LE]];
2030       REMOVE_THEN "*" (MP_TAC o SPEC `f:real^N->bool`) THEN
2031       ASM_REWRITE_TAC[] THEN DISCH_THEN MATCH_MP_TAC THEN
2032       DISCH_TAC THEN UNDISCH_TAC `aff_dim(f:real^N->bool) = &d` THEN
2033       ASM_REWRITE_TAC[AFF_DIM_EMPTY] THEN INT_ARITH_TAC]] THEN
2034   X_GEN_TAC `f:real^N->bool` THEN STRIP_TAC THEN
2035   MATCH_MP_TAC(INT_ARITH `f < a /\ a <= f + &1 ==> a:int = f + &1`) THEN
2036   CONJ_TAC THENL
2037    [MATCH_MP_TAC AFF_DIM_PSUBSET THEN
2038     SIMP_TAC[PSUBSET; HULL_MONO; HULL_SUBSET] THEN
2039     REWRITE_TAC[EXTENSION; NOT_FORALL_THM] THEN EXISTS_TAC `vec 0:real^N` THEN
2040     MATCH_MP_TAC(TAUT `~p /\ q ==> ~(p <=> q)`) THEN CONJ_TAC THENL
2041      [MATCH_MP_TAC(SET_RULE `!t. ~(x IN t) /\ s SUBSET t ==> ~(x IN s)`) THEN
2042       EXISTS_TAC `affine hull p:real^N->bool` THEN CONJ_TAC THENL
2043        [ASM_REWRITE_TAC[IN_ELIM_THM; VEC_COMPONENT] THEN REAL_ARITH_TAC;
2044         MATCH_MP_TAC HULL_MONO THEN ASM_MESON_TAC[FACE_OF_IMP_SUBSET]];
2045       MATCH_MP_TAC(SET_RULE
2046        `x IN s /\ s SUBSET P hull s ==> x IN P hull s`) THEN
2047       ASM_SIMP_TAC[CONIC_CONTAINS_0; HULL_SUBSET; CONIC_CONIC_HULL] THEN
2048       ASM_REWRITE_TAC[CONIC_HULL_EQ_EMPTY]];
2049     MATCH_MP_TAC INT_LE_TRANS THEN
2050     EXISTS_TAC `aff_dim((vec 0:real^N) INSERT (affine hull f))` THEN
2051     CONJ_TAC THENL
2052      [ALL_TAC;
2053       REWRITE_TAC[AFF_DIM_INSERT; AFF_DIM_AFFINE_HULL] THEN INT_ARITH_TAC] THEN
2054     ONCE_REWRITE_TAC[GSYM AFF_DIM_AFFINE_HULL] THEN
2055     MATCH_MP_TAC AFF_DIM_SUBSET THEN MATCH_MP_TAC HULL_MINIMAL THEN
2056     REWRITE_TAC[AFFINE_AFFINE_HULL; SUBSET; CONIC_HULL_EXPLICIT] THEN
2057     REWRITE_TAC[FORALL_IN_GSPEC] THEN
2058     MAP_EVERY X_GEN_TAC [`c:real`; `x:real^N`] THEN STRIP_TAC THEN
2059     ONCE_REWRITE_TAC[VECTOR_ARITH
2060      `c % x:real^N = vec 0 + c % (x - vec 0)`] THEN
2061     MATCH_MP_TAC IN_AFFINE_ADD_MUL_DIFF THEN
2062     ASM_SIMP_TAC[AFFINE_AFFINE_HULL; HULL_INC; IN_INSERT]]);;
2063
2064 let EULER_POINCARE_SPECIAL = prove
2065  (`!p:real^N->bool.
2066         2 <= dimindex(:N) /\ polytope p /\ affine hull p = {x | x$1 = &0}
2067         ==> sum (0..dimindex(:N)-1)
2068                (\d. (-- &1) pow d *
2069                     &(CARD {f | f face_of p /\ aff_dim f = &d })) = &1`,
2070   REPEAT STRIP_TAC THEN
2071   MP_TAC(ISPEC `IMAGE (\x:real^N. basis 1 + x) p` EULER_POINCARE_LEMMA) THEN
2072   ASM_REWRITE_TAC[POLYTOPE_TRANSLATION_EQ; AFFINE_HULL_TRANSLATION] THEN
2073   ANTS_TAC THENL
2074    [MATCH_MP_TAC SURJECTIVE_IMAGE_EQ THEN
2075     REWRITE_TAC[EXISTS_REFL; VECTOR_ARITH
2076      `a + x:real^N = y <=> x = y - a`] THEN
2077     SIMP_TAC[IN_ELIM_THM; VECTOR_ADD_COMPONENT; BASIS_COMPONENT;
2078              DIMINDEX_GE_1; LE_REFL] THEN REAL_ARITH_TAC;
2079     REWRITE_TAC[SET_RULE `{f | f face_of s /\ P f} =
2080                           {f | f IN {f | f face_of s} /\ P f}`] THEN
2081     REWRITE_TAC[FACES_OF_TRANSLATION] THEN
2082     REWRITE_TAC[SET_RULE `{y | y IN IMAGE f s /\ P y} =
2083                           {f x |x| x IN s /\ P(f x)}`] THEN
2084     REWRITE_TAC[AFF_DIM_TRANSLATION_EQ; IN_ELIM_THM] THEN
2085     DISCH_THEN(fun th -> GEN_REWRITE_TAC RAND_CONV [SYM th]) THEN
2086     MATCH_MP_TAC SUM_EQ_NUMSEG THEN X_GEN_TAC `d:num` THEN STRIP_TAC THEN
2087     REWRITE_TAC[] THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
2088     GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [SIMPLE_IMAGE_GEN] THEN
2089     CONV_TAC SYM_CONV THEN MATCH_MP_TAC CARD_IMAGE_INJ THEN CONJ_TAC THENL
2090      [REWRITE_TAC[] THEN MATCH_MP_TAC(MESON[]
2091        `(!x y. Q x y ==> x = y)
2092         ==> (!x y. P x /\ P y /\ Q x y ==> x = y)`) THEN
2093       REWRITE_TAC[INJECTIVE_IMAGE] THEN VECTOR_ARITH_TAC;
2094       MATCH_MP_TAC FINITE_SUBSET THEN
2095       EXISTS_TAC `{f:real^N->bool | f face_of p}` THEN
2096       ASM_SIMP_TAC[FINITE_POLYTOPE_FACES] THEN SET_TAC[]]]);;
2097
2098 (* ------------------------------------------------------------------------- *)
2099 (* Now Euler-Poincare for a general full-dimensional polytope.               *)
2100 (* ------------------------------------------------------------------------- *)
2101
2102 let EULER_POINCARE_FULL = prove
2103  (`!p:real^N->bool.
2104         polytope p /\ aff_dim p = &(dimindex(:N))
2105         ==> sum (0..dimindex(:N))
2106                 (\d. (-- &1) pow d *
2107                      &(CARD {f | f face_of p /\ aff_dim f = &d })) = &1`,
2108   REPEAT STRIP_TAC THEN ABBREV_TAC
2109    `f:real^N->real^(N,1)finite_sum =
2110           \x. lambda i. if i = 1 then &0 else x$(i-1)` THEN
2111   ABBREV_TAC `s = IMAGE (f:real^N->real^(N,1)finite_sum) p` THEN
2112   MP_TAC(ISPEC `s:real^(N,1)finite_sum->bool` EULER_POINCARE_SPECIAL) THEN
2113   REWRITE_TAC[DIMINDEX_FINITE_SUM; DIMINDEX_1; ADD_SUB] THEN
2114   REWRITE_TAC[DIMINDEX_GE_1; ARITH_RULE `2 <= n + 1 <=> 1 <= n`] THEN
2115   SUBGOAL_THEN `linear(f:real^N->real^(N,1)finite_sum)` ASSUME_TAC THENL
2116    [EXPAND_TAC "f" THEN REWRITE_TAC[linear] THEN
2117     SIMP_TAC[CART_EQ; VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT;
2118              LAMBDA_BETA] THEN
2119     REAL_ARITH_TAC;
2120     ALL_TAC] THEN
2121   EXPAND_TAC "s" THEN
2122   ASM_SIMP_TAC[POLYTOPE_LINEAR_IMAGE; AFFINE_HULL_LINEAR_IMAGE] THEN
2123   RULE_ASSUM_TAC(REWRITE_RULE[AFF_DIM_EQ_FULL]) THEN
2124   ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
2125    [REWRITE_TAC[EXTENSION; IN_IMAGE; IN_ELIM_THM; IN_UNIV] THEN
2126     X_GEN_TAC `y:real^(N,1)finite_sum` THEN EQ_TAC THENL
2127      [DISCH_THEN(X_CHOOSE_THEN `x:real^N` SUBST1_TAC) THEN
2128       EXPAND_TAC "f" THEN SIMP_TAC[LAMBDA_BETA; LE_REFL; DIMINDEX_GE_1];
2129       DISCH_TAC THEN
2130       EXISTS_TAC `(lambda i. (y:real^(N,1)finite_sum)$(i+1)):real^N` THEN
2131       EXPAND_TAC "f" THEN
2132       REWRITE_TAC[CART_EQ; DIMINDEX_FINITE_SUM; DIMINDEX_1] THEN
2133       X_GEN_TAC `i:num` THEN STRIP_TAC THEN
2134       ASM_SIMP_TAC[CART_EQ; LAMBDA_BETA; DIMINDEX_FINITE_SUM; DIMINDEX_1;
2135        DIMINDEX_GE_1; ARITH_RULE `1 <= i /\ ~(i = 1) ==> 1 <= i - 1`;
2136        ARITH_RULE `1 <= n /\ i <= n + 1 ==> i - 1 <= n`] THEN
2137       COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN AP_TERM_TAC THEN
2138       ASM_ARITH_TAC];
2139     DISCH_THEN(fun th -> GEN_REWRITE_TAC RAND_CONV [SYM th]) THEN
2140     MATCH_MP_TAC SUM_EQ_NUMSEG THEN X_GEN_TAC `d:num` THEN STRIP_TAC THEN
2141     REWRITE_TAC[] THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
2142     SUBGOAL_THEN `!x y. (f:real^N->real^(N,1)finite_sum) x = f y <=> x = y`
2143     ASSUME_TAC THENL
2144      [EXPAND_TAC "f" THEN
2145       ASM_SIMP_TAC[CART_EQ; LAMBDA_BETA; DIMINDEX_FINITE_SUM; DIMINDEX_1;
2146         DIMINDEX_GE_1; ARITH_RULE `1 <= i /\ ~(i = 1) ==> 1 <= i - 1`;
2147         ARITH_RULE `1 <= n /\ i <= n + 1 ==> i - 1 <= n`] THEN
2148       REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN X_GEN_TAC `i:num` THENL
2149        [REPEAT STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `i + 1`) THEN
2150         ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
2151         REWRITE_TAC[ADD_SUB] THEN
2152         COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC;
2153         STRIP_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
2154         FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC];
2155       ALL_TAC] THEN
2156     EXPAND_TAC "s" THEN
2157     MP_TAC(ISPECL [`f:real^N->real^(N,1)finite_sum`; `p:real^N->bool`]
2158         FACES_OF_LINEAR_IMAGE) THEN
2159     ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
2160     REWRITE_TAC[SET_RULE `{f | f face_of s /\ P f} =
2161                           {f | f IN {f | f face_of s} /\ P f}`] THEN
2162     ASM_REWRITE_TAC[SET_RULE `{y | y IN IMAGE f s /\ P y} =
2163                               {f x |x| x IN s /\ P(f x)}`] THEN
2164     ASM_SIMP_TAC[AFF_DIM_INJECTIVE_LINEAR_IMAGE] THEN
2165     REWRITE_TAC[IN_ELIM_THM] THEN
2166     GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [SIMPLE_IMAGE_GEN] THEN
2167     CONV_TAC SYM_CONV THEN MATCH_MP_TAC CARD_IMAGE_INJ THEN CONJ_TAC THENL
2168      [REWRITE_TAC[] THEN MATCH_MP_TAC(MESON[]
2169        `(!x y. Q x y ==> x = y)
2170         ==> (!x y. P x /\ P y /\ Q x y ==> x = y)`) THEN
2171       ASM_REWRITE_TAC[INJECTIVE_IMAGE];
2172       MATCH_MP_TAC FINITE_SUBSET THEN
2173       EXISTS_TAC `{f:real^N->bool | f face_of p}` THEN
2174       ASM_SIMP_TAC[FINITE_POLYTOPE_FACES] THEN SET_TAC[]]]);;
2175
2176 (* ------------------------------------------------------------------------- *)
2177 (* In particular the Euler relation in 3D.                                   *)
2178 (* ------------------------------------------------------------------------- *)
2179
2180 let EULER_RELATION = prove
2181  (`!p:real^3->bool.
2182         polytope p /\ aff_dim p = &3
2183         ==> (CARD {v | v face_of p /\ aff_dim(v) = &0} +
2184              CARD {f | f face_of p /\ aff_dim(f) = &2}) -
2185             CARD {e | e face_of p /\ aff_dim(e) = &1} = 2`,
2186   REPEAT STRIP_TAC THEN
2187   MP_TAC(ISPEC `p:real^3->bool` EULER_POINCARE_FULL) THEN
2188   ASM_REWRITE_TAC[DIMINDEX_3] THEN
2189   REWRITE_TAC[TOP_DEPTH_CONV num_CONV `3`; SUM_CLAUSES_NUMSEG] THEN
2190   CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
2191   REWRITE_TAC[REAL_MUL_LID; REAL_MUL_LNEG] THEN
2192   SUBGOAL_THEN `{f:real^3->bool | f face_of p /\ aff_dim f = &3} = {p}`
2193    (fun th -> SIMP_TAC[th; NOT_IN_EMPTY; FINITE_EMPTY; CARD_CLAUSES])
2194   THENL
2195    [MATCH_MP_TAC(SET_RULE
2196      `P a /\ (!x. P x ==> x = a) ==> {x | P x} = {a}`) THEN
2197     ASM_SIMP_TAC[FACE_OF_REFL; POLYTOPE_IMP_CONVEX] THEN
2198     X_GEN_TAC `f:real^3->bool` THEN STRIP_TAC THEN
2199     MP_TAC(ISPECL [`f:real^3->bool`; `p:real^3->bool`]
2200         FACE_OF_AFF_DIM_LT) THEN
2201     ASM_SIMP_TAC[POLYTOPE_IMP_CONVEX; INT_LT_REFL];
2202     REWRITE_TAC[GSYM REAL_OF_NUM_SUC; REAL_ADD_LID] THEN
2203     REWRITE_TAC[REAL_ARITH `((x + --y) + z) + -- &1:real = &1 <=>
2204                             x + z = y + &2`] THEN
2205     REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_EQ] THEN
2206     DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[ADD_SUB2]]);;