1 (* ========================================================================= *)
2 (* Formalization of Jim Lawrence's proof of Euler's relation. *)
3 (* ========================================================================= *)
5 needs "Multivariate/polytope.ml";;
6 needs "Library/binomial.ml";;
7 needs "100/inclusion_exclusion.ml";;
8 needs "100/combinations.ml";;
12 (* ------------------------------------------------------------------------- *)
13 (* Interpret which "side" of a hyperplane a point is on. *)
14 (* ------------------------------------------------------------------------- *)
16 let hyperplane_side = new_definition
17 `hyperplane_side (a,b) (x:real^N) = real_sgn (a dot x - b)`;;
19 (* ------------------------------------------------------------------------- *)
20 (* Equivalence relation imposed by a hyperplane arrangement. *)
21 (* ------------------------------------------------------------------------- *)
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`;;
27 let HYPERPLANE_EQUIV_REFL = prove
28 (`!A x. hyperplane_equiv A x x`,
29 REWRITE_TAC[hyperplane_equiv]);;
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]);;
35 let HYPERPLANE_EQUIV_TRANS = prove
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[]);;
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[]);;
46 (* ------------------------------------------------------------------------- *)
47 (* Cells of a hyperplane arrangement. *)
48 (* ------------------------------------------------------------------------- *)
50 let hyperplane_cell = new_definition
51 `hyperplane_cell A c <=> ?x. c = hyperplane_equiv A x`;;
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
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]);;
63 let NONEMPTY_HYPERPLANE_CELL = prove
64 (`!A c. hyperplane_cell A c ==> ~(c = {})`,
65 MESON_TAC[NOT_HYPERPLANE_CELL_EMPTY]);;
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]);;
72 let DISJOINT_HYPERPLANE_CELLS = prove
73 (`!A c1 c2. hyperplane_cell A c1 /\ hyperplane_cell A c2 /\ ~(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]);;
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 = {}`]);;
86 let HYPERPLANE_CELL_EMPTY = prove
87 (`hyperplane_cell {} c <=> c = (:real^N)`,
88 REWRITE_TAC[HYPERPLANE_CELL; NOT_IN_EMPTY; hyperplane_equiv] THEN
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`]);;
107 let HYPERPLANE_CELL_SING = prove
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
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]);;
136 let HYPERPLANE_CELL_UNION = prove
137 (`!A B c:real^N->bool.
138 hyperplane_cell (A UNION B) c <=>
140 ?c1 c2. hyperplane_cell A c1 /\
141 hyperplane_cell B 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
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]);;
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
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]]);;
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[]);;
183 let FINITE_SET_OF_HYPERPLANE_CELLS = prove
184 (`!A C. FINITE A /\ (!c:real^N->bool. c IN C ==> hyperplane_cell A 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[]);;
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]);;
195 let HYPERPLANE_CELL_INTER_OPEN_AFFINE = prove
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];
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];
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];
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];
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]]);;
235 let HYPERPLANE_CELL_RELATIVELY_OPEN = prove
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`
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]]);;
255 let HYPERPLANE_CELL_RELATIVE_INTERIOR = prove
257 FINITE A /\ hyperplane_cell A c
258 ==> relative_interior c = c`,
259 MESON_TAC[RELATIVE_INTERIOR_OPEN_IN; HYPERPLANE_CELL_RELATIVELY_OPEN]);;
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]);;
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]);;
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]);;
306 (* ------------------------------------------------------------------------- *)
307 (* A cell complex is considered to be a union of such cells. *)
308 (* ------------------------------------------------------------------------- *)
310 let hyperplane_cellcomplex = new_definition
311 `hyperplane_cellcomplex A s <=>
312 ?t. (!c. c IN t ==> hyperplane_cell A c) /\
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]);;
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]);;
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
341 let HYPERPLANE_CELLCOMPLEX_UNION = prove
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]);;
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]);;
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)`,
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}`
370 [GEN_REWRITE_TAC I [EXTENSION] THEN REWRITE_TAC[IN_ELIM_THM] 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[]]);;
380 let HYPERPLANE_CELLCOMPLEX_INTER = prove
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]);;
388 let HYPERPLANE_CELLCOMPLEX_COMPL = prove
389 (`!A s. hyperplane_cellcomplex A s
390 ==> hyperplane_cellcomplex A ((:real^N) DIFF s)`,
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
400 `(:real^N) DIFF c = UNIONS {c' | hyperplane_cell A c' /\ ~(c' = c)}`
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]]);;
414 let HYPERPLANE_CELLCOMPLEX_DIFF = prove
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]);;
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[]]);;
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
457 let FINITE_RESTRICT_HYPERPLANE_CELLCOMPLEXES = prove
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[]);;
464 let FINITE_SET_OF_HYPERPLANE_CELLS = prove
465 (`!A C. FINITE A /\ (!c:real^N->bool. c IN C ==> hyperplane_cellcomplex A 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[]);;
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
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
493 (* ------------------------------------------------------------------------- *)
494 (* Euler characteristic. *)
495 (* ------------------------------------------------------------------------- *)
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)))`;;
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]);;
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]]);;
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]);;
535 let EULER_CHARACTERISTIC_CELLCOMPLEX_UNION = prove
536 (`!A s t:real^N->bool.
538 hyperplane_cellcomplex A s /\
539 hyperplane_cellcomplex A 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[]]);;
555 let EULER_CHARACTERISTIC_CELLCOMPLEX_UNIONS = prove
557 (!c:real^N->bool. c IN C ==> hyperplane_cellcomplex A 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
572 [ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL
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[]]);;
584 let EULER_CHARACTERISTIC = prove
587 ==> euler_characteristic A s =
588 sum (0..dimindex(:N))
590 &(CARD {c | hyperplane_cell A c /\ c SUBSET s /\
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))`]
598 SIMP_TAC[SUM_IMAGE; INT_OF_NUM_EQ; o_DEF; NUM_OF_INT_OF_NUM] THEN
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]]);;
614 (* ------------------------------------------------------------------------- *)
615 (* Show that the characteristic is invariant w.r.t. hyperplane arrangement. *)
616 (* ------------------------------------------------------------------------- *)
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
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
639 `!c:real^N->bool. c IN C ==> hyperplane_cellcomplex A c /\
640 hyperplane_cellcomplex ((a,b) INSERT A) c`
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[];
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
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
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
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
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
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
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
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];
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
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
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
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];
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
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
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
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
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;
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
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)
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];
799 `aff_dim c = aff_dim(c INTER {x:real^N | a dot x = b}) + &1`
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
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)
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
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
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]);;
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`,
836 FINITE A /\ hyperplane_cellcomplex A s
838 ==> euler_characteristic (A UNION B) s =
839 euler_characteristic A s`
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]]);;
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
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]);;
872 (* ------------------------------------------------------------------------- *)
873 (* Euler-type relation for full-dimensional proper polyhedral cones. *)
874 (* ------------------------------------------------------------------------- *)
876 let EULER_POLYHEDRAL_CONE = prove
877 (`!s. polyhedron s /\ conic s /\ ~(interior s = {}) /\ ~(s = (:real^N))
878 ==> sum (0..dimindex(:N))
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];
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];
899 `!h:real^N->bool. h IN H ==> ?a. ~(a = vec 0) /\ h = {x | a dot x <= &0}`
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
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];
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;
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
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)
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[];
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`
989 [MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `closure f:real^N->bool` THEN
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]];
996 ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
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
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}`
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
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
1031 `INTERS {{x:real^N | fa(h:real^N->bool) dot x <= &0} | h IN H} = s`
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
1037 ASM_CASES_TAC `{h:real^N->bool | h IN H /\
1038 f SUBSET s INTER {x:real^N | fa h dot x = &0}} =
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
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
1054 `H' = IMAGE (\h:real^N->bool. {x:real^N | --(fa h) dot x <= &0}) H` THEN
1057 J SUBSET (H UNION H') /\
1058 f:real^N->bool = affine hull f INTER INTERS J`
1060 [FIRST_X_ASSUM(X_CHOOSE_THEN `J:(real^N->bool)->bool`
1061 STRIP_ASSUME_TAC) THEN
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
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
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
1087 GEN_REWRITE_TAC LAND_CONV
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
1096 ==> (f:real^N->bool) PSUBSET (affine hull f INTER INTERS J')`
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
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
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'))`
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
1127 EXISTS_TAC `--((fa:(real^N->bool)->real^N) h)` THEN
1128 REWRITE_TAC[] THEN DISJ2_TAC THEN ASM_MESON_TAC[]];
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
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];
1141 ASM_SIMP_TAC[] THEN ASM_MESON_TAC[VECTOR_NEG_EQ_0; SUBSET]];
1142 DISCH_TAC THEN ASM_REWRITE_TAC[]] THEN
1144 `!h:real^N->bool. h IN J ==> h IN H /\ ga h:real^N = fa h`
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];
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;
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];
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];
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}`
1197 [MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL
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
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
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
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
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
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)}`
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)
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
1333 W(MP_TAC o PART_MATCH (lhand o rand) CLOSURE_INTER_CONVEX o
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
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
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]];
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
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}`
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[];
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}`
1377 [REWRITE_TAC[CLOSURE_EQ] THEN
1378 SIMP_TAC[CLOSED_INTERS; FORALL_IN_GSPEC; CLOSED_HYPERPLANE];
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
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}`
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]];
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]];
1438 `!h. h IN H ==> hyperplane_cellcomplex A ((:real^N) DIFF h)`
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
1450 REWRITE_TAC[IN_IMAGE; SUBSET; FORALL_UNWIND_THM2; IN_SING] THEN
1454 `!h:real^N->bool. h IN H ==> hyperplane_cellcomplex A h`
1456 [ASM_MESON_TAC[HYPERPLANE_CELLCOMPLEX_COMPL;
1457 SET_RULE `UNIV DIFF (UNIV DIFF s) = s`];
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
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
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];
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]];
1488 W(MP_TAC o PART_MATCH (lhs o rand) EULER_CHARACTERISTIC_INCLUSION_EXCLUSION o
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
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
1506 `INTERS (IMAGE (\t. (:real^N) DIFF t) H) =
1507 IMAGE (--) (interior s)`
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
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];
1535 `hyperplane_cell B (INTERS (IMAGE (\t. (:real^N) DIFF t) J))`
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];
1565 MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC
1566 `euler_characteristic B (INTERS (IMAGE (\t. (:real^N) DIFF t) J))` THEN
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];
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];
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)`;
1589 {(:real^N) DIFF t | t IN H} /\ ~(t = {})}`;
1590 `1..CARD(H:(real^N->bool)->bool)`]
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
1613 `sum (1..CARD(H:(real^N->bool)->bool))
1614 (\n. -- &1 pow (n + 1) * &(binom(CARD H,n)))` THEN
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
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} /\
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];
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[];
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[]);;
1662 (* ------------------------------------------------------------------------- *)
1663 (* Euler-Poincare relation for special (n-1)-dimensional polytope. *)
1664 (* ------------------------------------------------------------------------- *)
1666 let EULER_POINCARE_LEMMA = prove
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];
1681 ABBREV_TAC `s:real^N->bool = conic hull p` THEN
1682 MP_TAC(ISPEC `s:real^N->bool` EULER_POLYHEDRAL_CONE) THEN
1684 `!f. f SUBSET {x:real^N | x$1 = &1}
1685 ==> (conic hull f) INTER {x:real^N | x$1 = &1} = f`
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];
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[];
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
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
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
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];
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];
1759 ASM_REWRITE_TAC[] THEN
1760 SUBGOAL_THEN `!x:real^N. x IN s /\ ~(x = vec 0) ==> &0 < x$1`
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];
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];
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])
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
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]];
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
1821 `!f:real^N->bool. f face_of p ==> conic hull f INTER {x | x$1 = &1} = f`
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
1830 `!f:real^N->bool. f face_of s ==> f INTER {x | x$1 = &1} face_of p`
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
1839 `!f. f face_of s /\ &0 < aff_dim f
1840 ==> conic hull (f INTER {x:real^N | x$1 = &1}) = f`
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
1868 `!f:real^N->bool. f face_of p ==> (conic hull f) face_of s`
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];
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];
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`
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
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[]];
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`
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
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[]];
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`
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
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
2001 `!f:real^N->bool. f face_of p /\ ~(f = {})
2002 ==> aff_dim(conic hull f) = aff_dim f + &1`
2003 (LABEL_TAC "*") THENL
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
2013 [MP_TAC(ISPECL [`s:real^N->bool`; `f:real^N->bool`]
2015 ASM_SIMP_TAC[CONIC_CONTAINS_0] THEN REPEAT DISCH_TAC;
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`]
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
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
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]]);;
2064 let EULER_POINCARE_SPECIAL = prove
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
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[]]]);;
2098 (* ------------------------------------------------------------------------- *)
2099 (* Now Euler-Poincare for a general full-dimensional polytope. *)
2100 (* ------------------------------------------------------------------------- *)
2102 let EULER_POINCARE_FULL = prove
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;
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];
2130 EXISTS_TAC `(lambda i. (y:real^(N,1)finite_sum)$(i+1)):real^N` 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
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`
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];
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[]]]);;
2176 (* ------------------------------------------------------------------------- *)
2177 (* In particular the Euler relation in 3D. *)
2178 (* ------------------------------------------------------------------------- *)
2180 let EULER_RELATION = prove
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])
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]]);;