(* ========================================================================= *) (* Formalization of Jim Lawrence's proof of Euler's relation. *) (* ========================================================================= *) needs "Multivariate/polytope.ml";; needs "Library/binomial.ml";; needs "100/inclusion_exclusion.ml";; needs "100/combinations.ml";; prioritize_real();; (* ------------------------------------------------------------------------- *) (* Interpret which "side" of a hyperplane a point is on. *) (* ------------------------------------------------------------------------- *) let hyperplane_side = new_definition `hyperplane_side (a,b) (x:real^N) = real_sgn (a dot x - b)`;; (* ------------------------------------------------------------------------- *) (* Equivalence relation imposed by a hyperplane arrangement. *) (* ------------------------------------------------------------------------- *) let hyperplane_equiv = new_definition `hyperplane_equiv A x y <=> !h. h IN A ==> hyperplane_side h x = hyperplane_side h y`;; let HYPERPLANE_EQUIV_REFL = prove (`!A x. hyperplane_equiv A x x`, REWRITE_TAC[hyperplane_equiv]);; let HYPERPLANE_EQUIV_SYM = prove (`!A x y. hyperplane_equiv A x y <=> hyperplane_equiv A y x`, REWRITE_TAC[hyperplane_equiv; EQ_SYM_EQ]);; let HYPERPLANE_EQUIV_TRANS = prove (`!A x y z. hyperplane_equiv A x y /\ hyperplane_equiv A y z ==> hyperplane_equiv A x z`, REWRITE_TAC[hyperplane_equiv] THEN MESON_TAC[]);; let HYPERPLANE_EQUIV_UNION = prove (`!A B x y. hyperplane_equiv (A UNION B) x y <=> hyperplane_equiv A x y /\ hyperplane_equiv B x y`, REWRITE_TAC[hyperplane_equiv; IN_UNION] THEN MESON_TAC[]);; (* ------------------------------------------------------------------------- *) (* Cells of a hyperplane arrangement. *) (* ------------------------------------------------------------------------- *) let hyperplane_cell = new_definition `hyperplane_cell A c <=> ?x. c = hyperplane_equiv A x`;; let HYPERPLANE_CELL = prove (`hyperplane_cell A c <=> ?x. c = {y | hyperplane_equiv A x y}`, REWRITE_TAC[EXTENSION; hyperplane_cell; IN_ELIM_THM; IN] THEN MESON_TAC[]);; let NOT_HYPERPLANE_CELL_EMPTY = prove (`!A. ~(hyperplane_cell A {})`, REWRITE_TAC[hyperplane_cell; EXTENSION; NOT_IN_EMPTY] THEN MESON_TAC[HYPERPLANE_EQUIV_REFL; IN]);; let NONEMPTY_HYPERPLANE_CELL = prove (`!A c. hyperplane_cell A c ==> ~(c = {})`, MESON_TAC[NOT_HYPERPLANE_CELL_EMPTY]);; let UNIONS_HYPERPLANE_CELLS = prove (`!A. UNIONS {c | hyperplane_cell A c} = (:real^N)`, REWRITE_TAC[EXTENSION; IN_UNIONS; IN_UNIV; IN_ELIM_THM] THEN REWRITE_TAC[hyperplane_cell] THEN MESON_TAC[HYPERPLANE_EQUIV_REFL; IN]);; let DISJOINT_HYPERPLANE_CELLS = prove (`!A c1 c2. hyperplane_cell A c1 /\ hyperplane_cell A c2 /\ ~(c1 = c2) ==> DISJOINT c1 c2`, REWRITE_TAC[hyperplane_cell] THEN REPEAT STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o check (is_neg o concl)) THEN ASM_REWRITE_TAC[IN_DISJOINT; IN; EXTENSION] THEN ASM_MESON_TAC[HYPERPLANE_EQUIV_TRANS; HYPERPLANE_EQUIV_SYM]);; let DISJOINT_HYPERPLANE_CELLS_EQ = prove (`!A c1 c2. hyperplane_cell A c1 /\ hyperplane_cell A c2 ==> (DISJOINT c1 c2 <=> ~(c1 = c2))`, MESON_TAC[NONEMPTY_HYPERPLANE_CELL; DISJOINT_HYPERPLANE_CELLS; SET_RULE `DISJOINT s s <=> s = {}`]);; let HYPERPLANE_CELL_EMPTY = prove (`hyperplane_cell {} c <=> c = (:real^N)`, REWRITE_TAC[HYPERPLANE_CELL; NOT_IN_EMPTY; hyperplane_equiv] THEN SET_TAC[]);; let HYPERPLANE_CELL_SING_CASES = prove (`!a b c:real^N->bool. hyperplane_cell {(a,b)} c ==> c = {x | a dot x = b} \/ c = {x | a dot x < b} \/ c = {x | a dot x > b}`, REWRITE_TAC[HYPERPLANE_CELL; hyperplane_equiv] THEN REWRITE_TAC[FORALL_UNWIND_THM2; IN_SING; hyperplane_side] THEN REPEAT GEN_TAC THEN DISCH_THEN(X_CHOOSE_THEN `y:real^N` MP_TAC) THEN GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV) [EQ_SYM_EQ] THEN REPEAT_TCL DISJ_CASES_THEN SUBST1_TAC (SPEC `(a:real^N) dot y - b` REAL_SGN_CASES) THEN ASM_REWRITE_TAC[REAL_SGN_EQ] THEN SIMP_TAC[REAL_SUB_0; REAL_SUB_LT; real_gt; REAL_ARITH `x - y < &0 <=> x < y`]);; let HYPERPLANE_CELL_SING = prove (`!a b c. hyperplane_cell {(a,b)} c <=> if a = vec 0 then c = (:real^N) else c = {x | a dot x = b} \/ c = {x | a dot x < b} \/ c = {x | a dot x > b}`, REPEAT GEN_TAC THEN COND_CASES_TAC THENL [REWRITE_TAC[hyperplane_cell; hyperplane_equiv; EXTENSION; IN_UNIV] THEN REWRITE_TAC[IN] THEN REWRITE_TAC[hyperplane_equiv] THEN ASM_SIMP_TAC[IN_SING; FORALL_UNWIND_THM2] THEN REWRITE_TAC[hyperplane_side; DOT_LZERO]; EQ_TAC THEN REWRITE_TAC[HYPERPLANE_CELL_SING_CASES] THEN STRIP_TAC THEN ASM_REWRITE_TAC[hyperplane_cell; EXTENSION; IN_ELIM_THM] THEN REWRITE_TAC[IN] THEN REWRITE_TAC[hyperplane_equiv] THEN ASM_SIMP_TAC[IN_SING; FORALL_UNWIND_THM2] THEN REWRITE_TAC[hyperplane_side] THEN ONCE_REWRITE_TAC[REAL_ARITH `a dot x = b <=> a dot x - b = &0`; REAL_ARITH `a > b <=> a - b > &0`; REAL_ARITH `a < b <=> a - b < &0`] THEN ONCE_REWRITE_TAC[GSYM REAL_SGN_EQ] THEN REWRITE_TAC[REAL_SUB_0] THEN MATCH_MP_TAC(MESON[] `(?x. f x = a) ==> (?x. !y. f y = a <=> f x = f y)`) THEN REWRITE_TAC[REAL_SGN_EQ] THENL [EXISTS_TAC `b / (a dot a) % a:real^N`; EXISTS_TAC `(b - &1) / (a dot a) % a:real^N`; EXISTS_TAC `(b + &1) / (a dot a) % a:real^N`] THEN ASM_SIMP_TAC[DOT_RMUL; REAL_DIV_RMUL; DOT_EQ_0] THEN REAL_ARITH_TAC]);; let HYPERPLANE_CELL_UNION = prove (`!A B c:real^N->bool. hyperplane_cell (A UNION B) c <=> ~(c = {}) /\ ?c1 c2. hyperplane_cell A c1 /\ hyperplane_cell B c2 /\ c = c1 INTER c2`, REPEAT GEN_TAC THEN ASM_CASES_TAC `c:real^N->bool = {}` THENL [ASM_MESON_TAC[NONEMPTY_HYPERPLANE_CELL]; ASM_REWRITE_TAC[]] THEN REWRITE_TAC[HYPERPLANE_CELL; HYPERPLANE_EQUIV_UNION] THEN REWRITE_TAC[SET_RULE `{x | P x /\ Q x} = {x | P x} INTER {x | Q x}`] THEN REWRITE_TAC[MESON[] `(?c1 c2. (?x. c1 = f x) /\ (?y. c2 = g y) /\ P c1 c2) <=> (?x y. P (f x) (g y))`] THEN EQ_TAC THENL [MESON_TAC[]; REWRITE_TAC[LEFT_IMP_EXISTS_THM]] THEN MAP_EVERY X_GEN_TAC [`a:real^N`; `b:real^N`] THEN DISCH_THEN SUBST_ALL_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `x:real^N` THEN REWRITE_TAC[EXTENSION; IN_INTER; IN_ELIM_THM] THEN MESON_TAC[HYPERPLANE_EQUIV_TRANS; HYPERPLANE_EQUIV_SYM]);; let FINITE_HYPERPLANE_CELLS = prove (`!A. FINITE A ==> FINITE {c:real^N->bool | hyperplane_cell A c}`, MATCH_MP_TAC FINITE_INDUCT_STRONG THEN REWRITE_TAC[HYPERPLANE_CELL_EMPTY; SING_GSPEC; FINITE_SING] THEN REWRITE_TAC[FORALL_PAIR_THM] THEN MAP_EVERY X_GEN_TAC [`a:real^N`; `b:real`; `A:(real^N#real)->bool`] THEN STRIP_TAC THEN ONCE_REWRITE_TAC[SET_RULE `a INSERT s = {a} UNION s`] THEN REWRITE_TAC[HYPERPLANE_CELL_UNION] THEN MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `{ c1 INTER c2:real^N->bool | c1 IN {c | hyperplane_cell A c} /\ c2 IN {c | hyperplane_cell {(a,b)} c}}` THEN CONJ_TAC THENL [MATCH_MP_TAC FINITE_PRODUCT_DEPENDENT THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `{{x:real^N | a dot x = b},{x | a dot x < b},{x | a dot x > b}}` THEN REWRITE_TAC[SUBSET; IN_SING; HYPERPLANE_CELL_SING_CASES; IN_ELIM_THM; IN_INSERT; NOT_IN_EMPTY; FINITE_INSERT; FINITE_EMPTY]; REWRITE_TAC[IN_ELIM_THM; SUBSET] THEN MESON_TAC[INTER_COMM]]);; let FINITE_RESTRICT_HYPERPLANE_CELLS = prove (`!P A. FINITE A ==> FINITE {c:real^N->bool | hyperplane_cell A c /\ P c}`, REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `{c:real^N->bool | hyperplane_cell A c}` THEN ASM_SIMP_TAC[FINITE_HYPERPLANE_CELLS] THEN SET_TAC[]);; let FINITE_SET_OF_HYPERPLANE_CELLS = prove (`!A C. FINITE A /\ (!c:real^N->bool. c IN C ==> hyperplane_cell A c) ==> FINITE C`, REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `{c:real^N->bool | hyperplane_cell A c}` THEN ASM_SIMP_TAC[FINITE_HYPERPLANE_CELLS] THEN ASM SET_TAC[]);; let PAIRWISE_DISJOINT_HYPERPLANE_CELLS = prove (`!A C. (!c. c IN C ==> hyperplane_cell A c) ==> pairwise DISJOINT C`, REWRITE_TAC[pairwise] THEN MESON_TAC[DISJOINT_HYPERPLANE_CELLS]);; let HYPERPLANE_CELL_INTER_OPEN_AFFINE = prove (`!A c:real^N->bool. FINITE A /\ hyperplane_cell A c ==> ?s t. open s /\ affine t /\ c = s INTER t`, REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN CONJ_TAC THENL [REWRITE_TAC[HYPERPLANE_CELL_EMPTY] THEN REPEAT STRIP_TAC THEN REPEAT(EXISTS_TAC `(:real^N)`) THEN ASM_REWRITE_TAC[AFFINE_UNIV; OPEN_UNIV; INTER_UNIV]; ALL_TAC] THEN REWRITE_TAC[FORALL_PAIR_THM] THEN MAP_EVERY X_GEN_TAC [`a:real^N`; `b:real`; `A:real^N#real->bool`] THEN STRIP_TAC THEN ONCE_REWRITE_TAC[SET_RULE `a INSERT s = {a} UNION s`] THEN REWRITE_TAC[HYPERPLANE_CELL_UNION] THEN X_GEN_TAC `c':real^N->bool` THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC [`c1:real^N->bool`; `c:real^N->bool`] THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC)) THEN FIRST_X_ASSUM(MP_TAC o SPEC `c:real^N->bool`) THEN ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC [`s:real^N->bool`; `t:real^N->bool`] THEN STRIP_TAC THEN REWRITE_TAC[HYPERPLANE_CELL_SING] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN REPEAT(FIRST_X_ASSUM SUBST_ALL_TAC) THENL [MAP_EVERY EXISTS_TAC [`s:real^N->bool`; `t:real^N->bool`] THEN ASM_REWRITE_TAC[INTER_UNIV]; MAP_EVERY EXISTS_TAC [`s:real^N->bool`; `{x:real^N | a dot x = b} INTER t`] THEN ASM_REWRITE_TAC[INTER_ACI] THEN MATCH_MP_TAC AFFINE_INTER THEN ASM_REWRITE_TAC[AFFINE_HYPERPLANE]; MAP_EVERY EXISTS_TAC [`{x:real^N | a dot x < b} INTER s`; `t:real^N->bool`] THEN ASM_REWRITE_TAC[INTER_ACI] THEN MATCH_MP_TAC OPEN_INTER THEN ASM_REWRITE_TAC[OPEN_HALFSPACE_LT]; MAP_EVERY EXISTS_TAC [`{x:real^N | a dot x > b} INTER s`; `t:real^N->bool`] THEN ASM_REWRITE_TAC[INTER_ACI] THEN MATCH_MP_TAC OPEN_INTER THEN ASM_REWRITE_TAC[OPEN_HALFSPACE_GT]]);; let HYPERPLANE_CELL_RELATIVELY_OPEN = prove (`!A c:real^N->bool. FINITE A /\ hyperplane_cell A c ==> open_in (subtopology euclidean (affine hull c)) c`, REPEAT GEN_TAC THEN DISCH_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP HYPERPLANE_CELL_INTER_OPEN_AFFINE) THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC [`s:real^N->bool`; `t:real^N->bool`] THEN STRIP_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN ASM_CASES_TAC `s INTER t:real^N->bool = {}` THEN ASM_REWRITE_TAC[OPEN_IN_EMPTY] THEN SUBGOAL_THEN `affine hull (s INTER t:real^N->bool) = t` SUBST1_TAC THENL [MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `affine hull t:real^N->bool` THEN ASM_REWRITE_TAC[AFFINE_HULL_EQ] THEN MATCH_MP_TAC(ONCE_REWRITE_RULE[INTER_COMM] AFFINE_HULL_CONVEX_INTER_OPEN) THEN ASM_SIMP_TAC[AFFINE_IMP_CONVEX]; ONCE_REWRITE_TAC[INTER_COMM] THEN ASM_SIMP_TAC[OPEN_IN_OPEN_INTER]]);; let HYPERPLANE_CELL_RELATIVE_INTERIOR = prove (`!A c:real^N->bool. FINITE A /\ hyperplane_cell A c ==> relative_interior c = c`, MESON_TAC[RELATIVE_INTERIOR_OPEN_IN; HYPERPLANE_CELL_RELATIVELY_OPEN]);; let HYPERPLANE_CELL_CONVEX = prove (`!A c:real^N->bool. hyperplane_cell A c ==> convex c`, REPEAT GEN_TAC THEN REWRITE_TAC[HYPERPLANE_CELL] THEN DISCH_THEN(X_CHOOSE_THEN `c:real^N` SUBST1_TAC) THEN REWRITE_TAC[hyperplane_equiv] THEN ONCE_REWRITE_TAC[SET_RULE `f x = f y <=> y IN {y | f x = f y}`] THEN REWRITE_TAC[GSYM INTERS_IMAGE] THEN MATCH_MP_TAC CONVEX_INTERS THEN REWRITE_TAC[FORALL_IN_IMAGE] THEN REWRITE_TAC[FORALL_PAIR_THM] THEN MAP_EVERY X_GEN_TAC [`a:real^N`; `b:real`] THEN DISCH_TAC THEN CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN REWRITE_TAC[hyperplane_side] THEN REPEAT_TCL DISJ_CASES_THEN SUBST1_TAC (SPEC `(a:real^N) dot c - b` REAL_SGN_CASES) THEN ASM_REWRITE_TAC[REAL_SGN_EQ] THEN SIMP_TAC[REAL_SUB_0; REAL_ARITH `a - b > &0 <=> a > b`; REAL_ARITH `a - b < &0 <=> a < b`] THEN REWRITE_TAC[CONVEX_HALFSPACE_LT; CONVEX_HALFSPACE_GT; CONVEX_HYPERPLANE]);; let HYPERPLANE_CELL_INTERS = prove (`!A C. (!c:real^N->bool. c IN C ==> hyperplane_cell A c) /\ ~(C = {}) /\ ~(INTERS C = {}) ==> hyperplane_cell A (INTERS C)`, REPEAT GEN_TAC THEN REWRITE_TAC[HYPERPLANE_CELL; GSYM MEMBER_NOT_EMPTY] THEN REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `z:real^N` THEN REWRITE_TAC[IN_INTERS] THEN DISCH_TAC THEN GEN_REWRITE_TAC I [EXTENSION] THEN REWRITE_TAC[IN_INTERS; IN_ELIM_THM] THEN X_GEN_TAC `x:real^N` THEN EQ_TAC THEN DISCH_TAC THENL [FIRST_X_ASSUM(X_CHOOSE_TAC `c:real^N->bool`); X_GEN_TAC `c:real^N->bool` THEN DISCH_TAC] THEN REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `c:real^N->bool`)) THEN ASM_REWRITE_TAC[] THEN REPEAT DISCH_TAC THEN FIRST_X_ASSUM(CHOOSE_THEN SUBST_ALL_TAC) THEN RULE_ASSUM_TAC(REWRITE_RULE[IN_ELIM_THM]) THEN SIMP_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[HYPERPLANE_EQUIV_SYM; HYPERPLANE_EQUIV_TRANS]);; let HYPERPLANE_CELL_INTER = prove (`!A s t:real^N->bool. hyperplane_cell A s /\ hyperplane_cell A t /\ ~(s INTER t = {}) ==> hyperplane_cell A (s INTER t)`, REWRITE_TAC[GSYM INTERS_2] THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC HYPERPLANE_CELL_INTERS THEN ASM_REWRITE_TAC[FORALL_IN_INSERT; NOT_IN_EMPTY; NOT_INSERT_EMPTY]);; (* ------------------------------------------------------------------------- *) (* A cell complex is considered to be a union of such cells. *) (* ------------------------------------------------------------------------- *) let hyperplane_cellcomplex = new_definition `hyperplane_cellcomplex A s <=> ?t. (!c. c IN t ==> hyperplane_cell A c) /\ s = UNIONS t`;; let HYPERPLANE_CELLCOMPLEX_EMPTY = prove (`!A:real^N#real->bool. hyperplane_cellcomplex A {}`, GEN_TAC THEN REWRITE_TAC[hyperplane_cellcomplex] THEN EXISTS_TAC `{}:(real^N->bool)->bool` THEN REWRITE_TAC[NOT_IN_EMPTY; UNIONS_0]);; let HYPERPLANE_CELL_CELLCOMPLEX = prove (`!A c:real^N->bool. hyperplane_cell A c ==> hyperplane_cellcomplex A c`, REPEAT STRIP_TAC THEN REWRITE_TAC[hyperplane_cellcomplex] THEN EXISTS_TAC `{c:real^N->bool}` THEN ASM_SIMP_TAC[IN_SING; UNIONS_1]);; let HYPERPLANE_CELLCOMPLEX_UNIONS = prove (`!A C. (!s:real^N->bool. s IN C ==> hyperplane_cellcomplex A s) ==> hyperplane_cellcomplex A (UNIONS C)`, REPEAT GEN_TAC THEN REWRITE_TAC[hyperplane_cellcomplex] THEN GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [RIGHT_IMP_EXISTS_THM] THEN REWRITE_TAC[SKOLEM_THM; LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `f:(real^N->bool)->(real^N->bool)->bool` THEN DISCH_TAC THEN EXISTS_TAC `UNIONS (IMAGE (f:(real^N->bool)->(real^N->bool)->bool) C)` THEN REWRITE_TAC[FORALL_IN_UNIONS; IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN REWRITE_TAC[FORALL_IN_IMAGE] THEN CONJ_TAC THENL [ASM_MESON_TAC[]; REWRITE_TAC[UNIONS_IMAGE]] THEN GEN_REWRITE_TAC I [EXTENSION] THEN REWRITE_TAC[IN_UNIONS; IN_ELIM_THM] THEN ASM SET_TAC[]);; let HYPERPLANE_CELLCOMPLEX_UNION = prove (`!A s t. hyperplane_cellcomplex A s /\ hyperplane_cellcomplex A t ==> hyperplane_cellcomplex A (s UNION t)`, REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM UNIONS_2] THEN MATCH_MP_TAC HYPERPLANE_CELLCOMPLEX_UNIONS THEN ASM_REWRITE_TAC[FORALL_IN_INSERT; NOT_IN_EMPTY]);; let HYPERPLANE_CELLCOMPLEX_UNIV = prove (`!A. hyperplane_cellcomplex A (:real^N)`, REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM UNIONS_HYPERPLANE_CELLS] THEN MATCH_MP_TAC HYPERPLANE_CELLCOMPLEX_UNIONS THEN REWRITE_TAC[IN_ELIM_THM; HYPERPLANE_CELL_CELLCOMPLEX]);; let HYPERPLANE_CELLCOMPLEX_INTERS = prove (`!A C. (!s:real^N->bool. s IN C ==> hyperplane_cellcomplex A s) ==> hyperplane_cellcomplex A (INTERS C)`, let lemma = prove (`UNIONS s = UNIONS {t | t IN s /\ ~(t = {})}`, REWRITE_TAC[UNIONS_GSPEC] THEN GEN_REWRITE_TAC I [EXTENSION] THEN REWRITE_TAC[IN_UNIONS; IN_ELIM_THM] THEN MESON_TAC[NOT_IN_EMPTY]) in REPEAT GEN_TAC THEN ASM_CASES_TAC `C:(real^N->bool)->bool = {}` THEN ASM_REWRITE_TAC[INTERS_0; HYPERPLANE_CELLCOMPLEX_UNIV] THEN GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [hyperplane_cellcomplex] THEN REWRITE_TAC[RIGHT_IMP_EXISTS_THM; SKOLEM_THM; LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `f:(real^N->bool)->(real^N->bool)->bool` THEN DISCH_TAC THEN SUBGOAL_THEN `C = {UNIONS((f:(real^N->bool)->(real^N->bool)->bool) s) | s IN C}` SUBST1_TAC THENL [GEN_REWRITE_TAC I [EXTENSION] THEN REWRITE_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[]; ALL_TAC] THEN REWRITE_TAC[INTERS_OVER_UNIONS] THEN ONCE_REWRITE_TAC[lemma] THEN MATCH_MP_TAC HYPERPLANE_CELLCOMPLEX_UNIONS THEN REWRITE_TAC[FORALL_IN_GSPEC; IMP_CONJ] THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC HYPERPLANE_CELL_CELLCOMPLEX THEN MATCH_MP_TAC HYPERPLANE_CELL_INTERS THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN CONJ_TAC THENL [ASM_MESON_TAC[]; ASM SET_TAC[]]);; let HYPERPLANE_CELLCOMPLEX_INTER = prove (`!A s t. hyperplane_cellcomplex A s /\ hyperplane_cellcomplex A t ==> hyperplane_cellcomplex A (s INTER t)`, REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM INTERS_2] THEN MATCH_MP_TAC HYPERPLANE_CELLCOMPLEX_INTERS THEN ASM_REWRITE_TAC[FORALL_IN_INSERT; NOT_IN_EMPTY]);; let HYPERPLANE_CELLCOMPLEX_COMPL = prove (`!A s. hyperplane_cellcomplex A s ==> hyperplane_cellcomplex A ((:real^N) DIFF s)`, REPEAT GEN_TAC THEN GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [hyperplane_cellcomplex] THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `C:(real^N->bool)->bool` THEN STRIP_TAC THEN ASM_REWRITE_TAC[UNIONS_INTERS; SET_RULE `UNIV DIFF (UNIV DIFF s) = s`] THEN MATCH_MP_TAC HYPERPLANE_CELLCOMPLEX_INTERS THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN X_GEN_TAC `c:real^N->bool` THEN DISCH_TAC THEN SUBGOAL_THEN `(:real^N) DIFF c = UNIONS {c' | hyperplane_cell A c' /\ ~(c' = c)}` SUBST1_TAC THENL [SUBST1_TAC(SYM(ISPEC `A:real^N#real->bool` UNIONS_HYPERPLANE_CELLS)) THEN GEN_REWRITE_TAC I [EXTENSION] THEN REWRITE_TAC[IN_DIFF; UNIONS_GSPEC; IN_ELIM_THM] THEN X_GEN_TAC `x:real^N` THEN REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN X_GEN_TAC `c':real^N->bool` THEN REWRITE_TAC[] THEN MP_TAC(ISPECL [`A:real^N#real->bool`; `c:real^N->bool`; `c':real^N->bool`] DISJOINT_HYPERPLANE_CELLS_EQ) THEN ASM_SIMP_TAC[] THEN SET_TAC[]; MATCH_MP_TAC HYPERPLANE_CELLCOMPLEX_UNIONS THEN ASM_SIMP_TAC[HYPERPLANE_CELL_CELLCOMPLEX; IN_ELIM_THM]]);; let HYPERPLANE_CELLCOMPLEX_DIFF = prove (`!A s t. hyperplane_cellcomplex A s /\ hyperplane_cellcomplex A t ==> hyperplane_cellcomplex A (s DIFF t)`, ONCE_REWRITE_TAC[SET_RULE `s DIFF t = s INTER (UNIV DIFF t)`] THEN SIMP_TAC[HYPERPLANE_CELLCOMPLEX_COMPL; HYPERPLANE_CELLCOMPLEX_INTER]);; let HYPERPLANE_CELLCOMPLEX_MONO = prove (`!A B s:real^N->bool. hyperplane_cellcomplex A s /\ A SUBSET B ==> hyperplane_cellcomplex B s`, REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [hyperplane_cellcomplex]) THEN DISCH_THEN(X_CHOOSE_THEN `C:(real^N->bool)->bool` STRIP_ASSUME_TAC) THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN MATCH_MP_TAC HYPERPLANE_CELLCOMPLEX_UNIONS THEN X_GEN_TAC `c:real^N->bool` THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `c:real^N->bool`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN SUBGOAL_THEN `B:(real^N#real)->bool = A UNION (B DIFF A)` SUBST1_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN REWRITE_TAC[hyperplane_cellcomplex; HYPERPLANE_CELL_UNION] THEN EXISTS_TAC `{c' INTER c:real^N->bool |c'| hyperplane_cell (B DIFF A) c' /\ ~(c' INTER c = {})}` THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN CONJ_TAC THENL [X_GEN_TAC `c':real^N->bool` THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MAP_EVERY EXISTS_TAC [`c:real^N->bool`; `c':real^N->bool`] THEN ASM_REWRITE_TAC[INTER_COMM]; GEN_REWRITE_TAC I [EXTENSION] THEN REWRITE_TAC[UNIONS_GSPEC; IN_ELIM_THM; IN_INTER] THEN X_GEN_TAC `x:real^N` THEN EQ_TAC THENL [DISCH_TAC; MESON_TAC[]] THEN MP_TAC(ISPEC `B DIFF A:(real^N#real)->bool` UNIONS_HYPERPLANE_CELLS) THEN GEN_REWRITE_TAC LAND_CONV [EXTENSION] THEN REWRITE_TAC[IN_UNIONS; IN_ELIM_THM; IN_UNIV] THEN ASM SET_TAC[]]);; let FINITE_HYPERPLANE_CELLCOMPLEXES = prove (`!A. FINITE A ==> FINITE {c:real^N->bool | hyperplane_cellcomplex A c}`, REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `IMAGE UNIONS {t | t SUBSET {c:real^N->bool | hyperplane_cell A c}}` THEN ASM_SIMP_TAC[FINITE_IMAGE; FINITE_POWERSET; FINITE_HYPERPLANE_CELLS] THEN REWRITE_TAC[SUBSET; IN_IMAGE; IN_ELIM_THM; hyperplane_cellcomplex] THEN MESON_TAC[]);; let FINITE_RESTRICT_HYPERPLANE_CELLCOMPLEXES = prove (`!P A. FINITE A ==> FINITE {c:real^N->bool | hyperplane_cellcomplex A c /\ P c}`, REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `{c:real^N->bool | hyperplane_cellcomplex A c}` THEN ASM_SIMP_TAC[FINITE_HYPERPLANE_CELLCOMPLEXES] THEN SET_TAC[]);; let FINITE_SET_OF_HYPERPLANE_CELLS = prove (`!A C. FINITE A /\ (!c:real^N->bool. c IN C ==> hyperplane_cellcomplex A c) ==> FINITE C`, REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `{c:real^N->bool | hyperplane_cellcomplex A c}` THEN ASM_SIMP_TAC[FINITE_HYPERPLANE_CELLCOMPLEXES] THEN ASM SET_TAC[]);; let CELL_SUBSET_CELLCOMPLEX = prove (`!A s c:real^N->bool. hyperplane_cell A c /\ hyperplane_cellcomplex A s ==> (c SUBSET s <=> ~(DISJOINT c s))`, REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [hyperplane_cellcomplex]) THEN DISCH_THEN(X_CHOOSE_THEN `C:(real^N->bool)->bool` STRIP_ASSUME_TAC) THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN EQ_TAC THENL [ASM_CASES_TAC `c:real^N->bool = {}` THENL [ASM_MESON_TAC[NONEMPTY_HYPERPLANE_CELL]; ASM SET_TAC[]]; REWRITE_TAC[DISJOINT; INTER_UNIONS; GSYM MEMBER_NOT_EMPTY] THEN REWRITE_TAC[UNIONS_GSPEC; IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC [`x:real^N`; `c':real^N->bool`] THEN REWRITE_TAC[IN_INTER] THEN STRIP_TAC THEN MP_TAC(ISPECL [`A:(real^N#real)->bool`; `c:real^N->bool`; `c':real^N->bool`] DISJOINT_HYPERPLANE_CELLS_EQ) THEN ASM_SIMP_TAC[] THEN ASM_CASES_TAC `c':real^N->bool = c` THENL [DISCH_THEN(K ALL_TAC); ASM SET_TAC[]] THEN MATCH_MP_TAC(SET_RULE `c IN C ==> c SUBSET UNIONS C`) THEN ASM_MESON_TAC[]]);; (* ------------------------------------------------------------------------- *) (* Euler characteristic. *) (* ------------------------------------------------------------------------- *) let euler_characteristic = new_definition `euler_characteristic A (s:real^N->bool) = sum {c | hyperplane_cell A c /\ c SUBSET s} (\c. (-- &1) pow (num_of_int(aff_dim c)))`;; let EULER_CHARACTERISTIC_EMPTY = prove (`euler_characteristic A {} = &0`, REWRITE_TAC[euler_characteristic; SUBSET_EMPTY] THEN MATCH_MP_TAC SUM_EQ_0 THEN MATCH_MP_TAC(MESON[] `~(?x. x IN s) ==> (!x. x IN s ==> P x)`) THEN REWRITE_TAC[IN_ELIM_THM] THEN MESON_TAC[NONEMPTY_HYPERPLANE_CELL]);; let EULER_CHARACTERISTIC_CELL_UNIONS = prove (`!A C. (!c:real^N->bool. c IN C ==> hyperplane_cell A c) ==> euler_characteristic A (UNIONS C) = sum C (\c. (-- &1) pow (num_of_int(aff_dim c)))`, REPEAT STRIP_TAC THEN REWRITE_TAC[euler_characteristic] THEN MATCH_MP_TAC(MESON[] `s = t ==> sum s f = sum t f`) THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN X_GEN_TAC `c:real^N->bool` THEN EQ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN SUBGOAL_THEN `~(c:real^N->bool = {})` MP_TAC THENL [ASM_MESON_TAC[NONEMPTY_HYPERPLANE_CELL]; ALL_TAC] THEN REWRITE_TAC[MEMBER_NOT_EMPTY; SUBSET; IN_UNIONS] THEN REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN `c':real^N->bool` STRIP_ASSUME_TAC) THEN SUBGOAL_THEN `~(DISJOINT (c:real^N->bool) c')` MP_TAC THENL [ASM SET_TAC[]; ASM_MESON_TAC[DISJOINT_HYPERPLANE_CELLS_EQ]]);; let EULER_CHARACTERISTIC_CELL = prove (`!A c. hyperplane_cell A c ==> euler_characteristic A c = (-- &1) pow (num_of_int(aff_dim c))`, REPEAT STRIP_TAC THEN GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM UNIONS_1] THEN ASM_SIMP_TAC[EULER_CHARACTERISTIC_CELL_UNIONS; IN_SING; SUM_SING]);; let EULER_CHARACTERISTIC_CELLCOMPLEX_UNION = prove (`!A s t:real^N->bool. FINITE A /\ hyperplane_cellcomplex A s /\ hyperplane_cellcomplex A t /\ DISJOINT s t ==> euler_characteristic A (s UNION t) = euler_characteristic A s + euler_characteristic A t`, REPEAT STRIP_TAC THEN REWRITE_TAC[euler_characteristic] THEN CONV_TAC SYM_CONV THEN MATCH_MP_TAC SUM_UNION_EQ THEN ASM_SIMP_TAC[FINITE_RESTRICT_HYPERPLANE_CELLS] THEN REWRITE_TAC[EXTENSION; IN_INTER; IN_ELIM_THM; NOT_IN_EMPTY; IN_UNION] THEN CONJ_TAC THEN X_GEN_TAC `c:real^N->bool` THENL [ASM_CASES_TAC `c:real^N->bool = {}` THENL [ASM_MESON_TAC[NONEMPTY_HYPERPLANE_CELL]; ASM SET_TAC[]]; ASM_CASES_TAC `hyperplane_cell A (c:real^N->bool)` THEN ASM_REWRITE_TAC[] THEN MP_TAC(ISPEC `A:(real^N#real)->bool` CELL_SUBSET_CELLCOMPLEX) THEN ASM_SIMP_TAC[HYPERPLANE_CELLCOMPLEX_UNION] THEN SET_TAC[]]);; let EULER_CHARACTERISTIC_CELLCOMPLEX_UNIONS = prove (`!A C. FINITE A /\ (!c:real^N->bool. c IN C ==> hyperplane_cellcomplex A c) /\ pairwise DISJOINT C ==> euler_characteristic A (UNIONS C) = sum C (\c. euler_characteristic A c)`, REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN ASM_CASES_TAC `FINITE(C:(real^N->bool)->bool)` THENL [UNDISCH_TAC `FINITE(C:(real^N->bool)->bool)`; ASM_MESON_TAC[FINITE_SET_OF_HYPERPLANE_CELLS]] THEN SPEC_TAC(`C:(real^N->bool)->bool`,`C:(real^N->bool)->bool`) THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN SIMP_TAC[EULER_CHARACTERISTIC_EMPTY; SUM_CLAUSES; UNIONS_0] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[UNIONS_INSERT] THEN W(MP_TAC o PART_MATCH (lhs o rand) EULER_CHARACTERISTIC_CELLCOMPLEX_UNION o lhs o snd) THEN ANTS_TAC THENL [ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL [ASM SET_TAC[]; MATCH_MP_TAC HYPERPLANE_CELLCOMPLEX_UNIONS THEN ASM SET_TAC[]; FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [pairwise]) THEN REWRITE_TAC[DISJOINT; INTER_UNIONS; IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_INSERT; EMPTY_UNIONS; FORALL_IN_GSPEC] THEN ASM_MESON_TAC[INTER_COMM]]; DISCH_THEN SUBST1_TAC THEN AP_TERM_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [pairwise]) THEN ASM_REWRITE_TAC[pairwise] THEN ASM SET_TAC[]]);; let EULER_CHARACTERISTIC = prove (`!A s:real^N->bool. FINITE A ==> euler_characteristic A s = sum (0..dimindex(:N)) (\d. (-- &1) pow d * &(CARD {c | hyperplane_cell A c /\ c SUBSET s /\ aff_dim c = &d}))`, REPEAT STRIP_TAC THEN REWRITE_TAC[euler_characteristic] THEN MP_TAC(ISPECL [`\c:real^N->bool. aff_dim c`; `\c:real^N->bool. (-- &1) pow (num_of_int(aff_dim c))`; `{c:real^N->bool | hyperplane_cell A c /\ c SUBSET s}`; `IMAGE int_of_num (0..dimindex(:N))`] SUM_GROUP) THEN SIMP_TAC[SUM_IMAGE; INT_OF_NUM_EQ; o_DEF; NUM_OF_INT_OF_NUM] THEN ANTS_TAC THENL [ASM_SIMP_TAC[FINITE_RESTRICT_HYPERPLANE_CELLS] THEN GEN_REWRITE_TAC I [SUBSET] THEN REWRITE_TAC[FORALL_IN_IMAGE; IN_ELIM_THM] THEN X_GEN_TAC `c:real^N->bool` THEN STRIP_TAC THEN REWRITE_TAC[IN_IMAGE; IN_NUMSEG; LE_0] THEN REWRITE_TAC[GSYM INT_OF_NUM_LE; INT_EXISTS_POS] THEN EXISTS_TAC `aff_dim(c:real^N->bool)` THEN REWRITE_TAC[AFF_DIM_LE_UNIV; AFF_DIM_POS_LE] THEN ASM_MESON_TAC[NONEMPTY_HYPERPLANE_CELL]; DISCH_THEN(SUBST1_TAC o SYM) THEN REWRITE_TAC[IN_ELIM_THM; GSYM CONJ_ASSOC] THEN ASM_SIMP_TAC[SUM_CONST; FINITE_RESTRICT_HYPERPLANE_CELLS] THEN REWRITE_TAC[REAL_MUL_AC]]);; (* ------------------------------------------------------------------------- *) (* Show that the characteristic is invariant w.r.t. hyperplane arrangement. *) (* ------------------------------------------------------------------------- *) let HYPERPLANE_CELLS_DISTINCT_LEMMA = prove (`!a b. {x | a dot x = b} INTER {x | a dot x < b} = {} /\ {x | a dot x = b} INTER {x | a dot x > b} = {} /\ {x | a dot x < b} INTER {x | a dot x = b} = {} /\ {x | a dot x < b} INTER {x | a dot x > b} = {} /\ {x | a dot x > b} INTER {x | a dot x = b} = {} /\ {x | a dot x > b} INTER {x | a dot x < b} = {}`, REWRITE_TAC[EXTENSION; IN_INTER; IN_ELIM_THM; NOT_IN_EMPTY] THEN REAL_ARITH_TAC);; let EULER_CHARACTERSTIC_LEMMA = prove (`!A h s:real^N->bool. FINITE A /\ hyperplane_cellcomplex A s ==> euler_characteristic (h INSERT A) s = euler_characteristic A s`, REWRITE_TAC[FORALL_PAIR_THM] THEN MAP_EVERY X_GEN_TAC [`A:(real^N#real)->bool`; `a:real^N`; `b:real`; `s:real^N->bool`] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN REWRITE_TAC[hyperplane_cellcomplex] THEN DISCH_THEN(X_CHOOSE_THEN `C:(real^N->bool)->bool` STRIP_ASSUME_TAC) THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN SUBGOAL_THEN `!c:real^N->bool. c IN C ==> hyperplane_cellcomplex A c /\ hyperplane_cellcomplex ((a,b) INSERT A) c` ASSUME_TAC THENL [REPEAT STRIP_TAC THEN ASM_SIMP_TAC[HYPERPLANE_CELL_CELLCOMPLEX] THEN MATCH_MP_TAC HYPERPLANE_CELLCOMPLEX_MONO THEN EXISTS_TAC `A:(real^N#real)->bool` THEN ASM_SIMP_TAC[HYPERPLANE_CELL_CELLCOMPLEX] THEN SET_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `pairwise DISJOINT (C:(real^N->bool)->bool)` ASSUME_TAC THENL [ASM_MESON_TAC[PAIRWISE_DISJOINT_HYPERPLANE_CELLS]; ALL_TAC] THEN ASM_SIMP_TAC[EULER_CHARACTERISTIC_CELLCOMPLEX_UNIONS; FINITE_INSERT] THEN MATCH_MP_TAC SUM_EQ THEN X_GEN_TAC `c:real^N->bool` THEN DISCH_TAC THEN ASM_CASES_TAC `hyperplane_cell ((a,b) INSERT A) (c:real^N->bool)` THEN ASM_SIMP_TAC[EULER_CHARACTERISTIC_CELL] THEN SUBGOAL_THEN `~(a:real^N = vec 0)` ASSUME_TAC THENL [FIRST_X_ASSUM(MP_TAC o check (is_neg o concl)) THEN SIMP_TAC[CONTRAPOS_THM] THEN DISCH_THEN(K ALL_TAC) THEN ONCE_REWRITE_TAC[SET_RULE `x INSERT s = {x} UNION s`] THEN REWRITE_TAC[HYPERPLANE_CELL_UNION] THEN REWRITE_TAC[HYPERPLANE_CELL_SING; RIGHT_EXISTS_AND_THM; UNWIND_THM2] THEN CONJ_TAC THENL [ASM_MESON_TAC[NONEMPTY_HYPERPLANE_CELL]; ALL_TAC] THEN ONCE_REWRITE_TAC[CONJ_SYM] THEN REWRITE_TAC[INTER_UNIV; UNWIND_THM1] THEN ASM_SIMP_TAC[]; ALL_TAC] THEN REWRITE_TAC[euler_characteristic] THEN ONCE_REWRITE_TAC[SET_RULE `x INSERT s = {x} UNION s`] THEN REWRITE_TAC[HYPERPLANE_CELL_UNION] THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `sum {c' INTER c |c'| hyperplane_cell {(a,b)} c' /\ ~(c' INTER c = {})} (\c:real^N->bool. (-- &1) pow (num_of_int(aff_dim c)))` THEN CONJ_TAC THENL [MATCH_MP_TAC(MESON[] `s = t ==> sum s f = sum t f`) THEN GEN_REWRITE_TAC I [EXTENSION] THEN REWRITE_TAC[IN_ELIM_THM] THEN X_GEN_TAC `c':real^N->bool` THEN EQ_TAC THENL [DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `c1:real^N->bool` THEN DISCH_THEN(X_CHOOSE_THEN `c2:real^N->bool` STRIP_ASSUME_TAC) THEN SUBGOAL_THEN `~(DISJOINT c2 (c:real^N->bool))` ASSUME_TAC THENL [ASM SET_TAC[]; ASM_MESON_TAC[DISJOINT_HYPERPLANE_CELLS_EQ]]; DISCH_THEN(X_CHOOSE_THEN `c1:real^N->bool` STRIP_ASSUME_TAC) THEN ASM_REWRITE_TAC[INTER_SUBSET] THEN MAP_EVERY EXISTS_TAC [`c1:real^N->bool`; `c:real^N->bool`] THEN ASM_SIMP_TAC[]]; ALL_TAC] THEN ASM_REWRITE_TAC[HYPERPLANE_CELL_SING] THEN SUBGOAL_THEN `~(c:real^N->bool = {})` ASSUME_TAC THENL [ASM_MESON_TAC[NONEMPTY_HYPERPLANE_CELL]; ALL_TAC] THEN MAP_EVERY (fun t -> ASM_CASES_TAC t THENL [MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `sum {c} (\c:real^N->bool. (-- &1) pow num_of_int (aff_dim c))` THEN CONJ_TAC THENL [ALL_TAC; SIMP_TAC[SUM_SING]] THEN MATCH_MP_TAC(MESON[] `s = t ==> sum s f = sum t f`) THEN GEN_REWRITE_TAC I [EXTENSION] THEN X_GEN_TAC `c':real^N->bool` THEN REWRITE_TAC[IN_SING; IN_ELIM_THM] THEN REWRITE_TAC[TAUT `(a \/ b) /\ c <=> a /\ c \/ b /\ c`] THEN REWRITE_TAC[EXISTS_OR_THM; UNWIND_THM2; GSYM CONJ_ASSOC] THEN EQ_TAC THEN STRIP_TAC THEN FIRST_X_ASSUM SUBST1_TAC THEN MP_TAC(ISPECL [`a:real^N`; `b:real`] HYPERPLANE_CELLS_DISTINCT_LEMMA) THEN ASM SET_TAC[]; ALL_TAC]) [`c SUBSET {x:real^N | a dot x < b}`; `c SUBSET {x:real^N | a dot x > b}`; `c SUBSET {x:real^N | a dot x = b}`] THEN SUBGOAL_THEN `~(c INTER {x:real^N | a dot x = b} = {})` ASSUME_TAC THENL [SUBGOAL_THEN `?u v:real^N. u IN c /\ ~(a dot u < b) /\ v IN c /\ ~(a dot v > b)` MP_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN REWRITE_TAC[real_gt; REAL_NOT_LT; GSYM MEMBER_NOT_EMPTY] THEN REWRITE_TAC[IN_INTER; IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC [`u:real^N`; `v:real^N`] THEN SIMP_TAC[REAL_LE_LT] THEN ASM_CASES_TAC `(a:real^N) dot u = b` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN ASM_CASES_TAC `(a:real^N) dot v = b` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN EXISTS_TAC `v + (b - a dot v) / (a dot u - a dot v) % (u - v):real^N` THEN SUBGOAL_THEN `(a:real^N) dot v < a dot u` ASSUME_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN ASM_SIMP_TAC[DOT_RADD; DOT_RMUL; DOT_RSUB; REAL_DIV_RMUL; REAL_SUB_LT; REAL_LT_IMP_NZ; REAL_SUB_ADD2] THEN REWRITE_TAC[VECTOR_ARITH `v + a % (u - v):real^N = (&1 - a) % v + a % u`] THEN MATCH_MP_TAC IN_CONVEX_SET THEN ASM_SIMP_TAC[REAL_LE_RDIV_EQ; REAL_LE_LDIV_EQ; REAL_SUB_LT] THEN CONJ_TAC THENL [ALL_TAC; ASM_REAL_ARITH_TAC] THEN ASM_MESON_TAC[HYPERPLANE_CELL_CONVEX]; ALL_TAC] THEN SUBGOAL_THEN `~(c INTER {x:real^N | a dot x < b} = {}) /\ ~(c INTER {x:real^N | a dot x > b} = {})` STRIP_ASSUME_TAC THENL [SUBGOAL_THEN `?u v:real^N. u IN c /\ a dot u = b /\ v IN c /\ ~(a dot v = b) /\ ~(u = v)` STRIP_ASSUME_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `open_in (subtopology euclidean (affine hull c)) (c:real^N->bool)` MP_TAC THENL [ASM_MESON_TAC[HYPERPLANE_CELL_RELATIVELY_OPEN]; ALL_TAC] THEN REWRITE_TAC[open_in] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o SPEC `u:real^N`)) THEN ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `e:real` THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o SPEC `u - e / &2 / norm(v - u) % (v - u):real^N`)) THEN ANTS_TAC THENL [REWRITE_TAC[NORM_ARITH `dist(u - a:real^N,u) = norm a`] THEN REWRITE_TAC[VECTOR_ARITH `x - a % (y - z):real^N = x + a % (z - y)`] THEN REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NUM; REAL_ABS_NORM] THEN ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN ASM_REWRITE_TAC[REAL_ARITH `abs e / &2 < e <=> &0 < e`] THEN MATCH_MP_TAC IN_AFFINE_ADD_MUL_DIFF THEN ASM_SIMP_TAC[AFFINE_AFFINE_HULL; HULL_INC]; DISCH_TAC] THEN REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER; IN_ELIM_THM] THEN SUBGOAL_THEN `(a:real^N) dot v < b \/ a dot v > b` STRIP_ASSUME_TAC THENL [ASM_REAL_ARITH_TAC; CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN EXISTS_TAC `u - e / &2 / norm(v - u) % (v - u):real^N` THEN ASM_REWRITE_TAC[DOT_RSUB; DOT_RMUL] THEN REWRITE_TAC[REAL_ARITH `b - x * y > b <=> &0 < x * --y`] THEN MATCH_MP_TAC REAL_LT_MUL THEN ASM_SIMP_TAC[REAL_LT_DIV; REAL_HALF; NORM_POS_LT; VECTOR_SUB_EQ] THEN ASM_REAL_ARITH_TAC; CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[]]] THEN EXISTS_TAC `u - e / &2 / norm(v - u) % (v - u):real^N` THEN ASM_REWRITE_TAC[DOT_RSUB; DOT_RMUL] THEN REWRITE_TAC[REAL_ARITH `b - x * y > b <=> &0 < x * --y`; REAL_ARITH `b - x < b <=> &0 < x`] THEN MATCH_MP_TAC REAL_LT_MUL THEN ASM_SIMP_TAC[REAL_LT_DIV; REAL_HALF; NORM_POS_LT; VECTOR_SUB_EQ] THEN ASM_REAL_ARITH_TAC; ALL_TAC] THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `sum {{x | a dot x = b} INTER c, {x | a dot x > b} INTER c, {x | a dot x < b} INTER c} (\c:real^N->bool. (-- &1) pow (num_of_int(aff_dim c)))` THEN CONJ_TAC THENL [MATCH_MP_TAC(MESON[] `s = t ==> sum s f = sum t f`) THEN GEN_REWRITE_TAC I [EXTENSION] THEN REWRITE_TAC[IN_ELIM_THM] THEN X_GEN_TAC `c':real^N->bool` THEN REWRITE_TAC[TAUT `(a \/ b) /\ c <=> a /\ c \/ b /\ c`] THEN REWRITE_TAC[EXISTS_OR_THM; UNWIND_THM2; GSYM CONJ_ASSOC] THEN ONCE_REWRITE_TAC[INTER_COMM] THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN CONV_TAC TAUT; ALL_TAC] THEN SIMP_TAC[SUM_CLAUSES; FINITE_INSERT; FINITE_EMPTY; IN_INSERT; NOT_IN_EMPTY] THEN ONCE_REWRITE_TAC[INTER_COMM] THEN ASM_SIMP_TAC[HYPERPLANE_CELLS_DISTINCT_LEMMA; REAL_ADD_RID; SET_RULE `s INTER t = {} /\ ~(c INTER s = {}) ==> ~(c INTER s = c INTER t)`] THEN SUBGOAL_THEN `aff_dim (c INTER {x:real^N | a dot x < b}) = aff_dim c /\ aff_dim (c INTER {x:real^N | a dot x > b}) = aff_dim c` (CONJUNCTS_THEN SUBST1_TAC) THENL [ONCE_REWRITE_TAC[GSYM AFF_DIM_AFFINE_HULL] THEN CONJ_TAC THEN AP_TERM_TAC THEN MATCH_MP_TAC AFFINE_HULL_CONVEX_INTER_OPEN THEN ASM_REWRITE_TAC[OPEN_HALFSPACE_LT; OPEN_HALFSPACE_GT] THEN ASM_MESON_TAC[HYPERPLANE_CELL_CONVEX]; ALL_TAC] THEN SUBGOAL_THEN `aff_dim c = aff_dim(c INTER {x:real^N | a dot x = b}) + &1` SUBST1_TAC THENL [MP_TAC(ISPECL [`A:real^N#real->bool`; `c:real^N->bool`] HYPERPLANE_CELL_INTER_OPEN_AFFINE) THEN ASM_SIMP_TAC[LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC [`s:real^N->bool`; `t:real^N->bool`] THEN STRIP_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN ONCE_REWRITE_TAC[GSYM AFF_DIM_AFFINE_HULL] THEN SUBGOAL_THEN `affine hull (s INTER t) = affine hull t /\ affine hull ((s INTER t) INTER {x:real^N | a dot x = b}) = affine hull (t INTER {x:real^N | a dot x = b})` (CONJUNCTS_THEN SUBST1_TAC) THENL [REWRITE_TAC[INTER_ASSOC] THEN CONJ_TAC THEN GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [INTER_COMM] THEN MATCH_MP_TAC AFFINE_HULL_CONVEX_INTER_OPEN THEN ASM_SIMP_TAC[CONVEX_INTER; CONVEX_HYPERPLANE; AFFINE_IMP_CONVEX] THEN ASM SET_TAC[]; REWRITE_TAC[AFF_DIM_AFFINE_HULL] THEN ASM_SIMP_TAC[AFF_DIM_AFFINE_INTER_HYPERPLANE] THEN REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[INT_SUB_ADD]) THEN ASM SET_TAC[]]; SUBGOAL_THEN `&0 <= aff_dim (c INTER {x:real^N | a dot x = b})` MP_TAC THENL [REWRITE_TAC[AFF_DIM_POS_LE] THEN ASM SET_TAC[]; ALL_TAC] THEN SPEC_TAC(`aff_dim (c INTER {x:real^N | a dot x = b})`,`i:int`) THEN REWRITE_TAC[GSYM INT_FORALL_POS] THEN REWRITE_TAC[NUM_OF_INT_OF_NUM; INT_OF_NUM_ADD] THEN REWRITE_TAC[REAL_POW_ADD] THEN REAL_ARITH_TAC]);; let EULER_CHARACTERSTIC_INVARIANT = prove (`!A B h s:real^N->bool. FINITE A /\ FINITE B /\ hyperplane_cellcomplex A s /\ hyperplane_cellcomplex B s ==> euler_characteristic A s = euler_characteristic B s`, SUBGOAL_THEN `!A s:real^N->bool. FINITE A /\ hyperplane_cellcomplex A s ==> !B. FINITE B ==> euler_characteristic (A UNION B) s = euler_characteristic A s` ASSUME_TAC THENL [REPEAT GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN ASM_REWRITE_TAC[UNION_EMPTY] THEN MAP_EVERY X_GEN_TAC [`h:real^N#real`; `B:real^N#real->bool`] THEN DISCH_THEN(CONJUNCTS_THEN2 (SUBST1_TAC o SYM) STRIP_ASSUME_TAC) THEN REWRITE_TAC[SET_RULE `s UNION (x INSERT t) = x INSERT (s UNION t)`] THEN MATCH_MP_TAC EULER_CHARACTERSTIC_LEMMA THEN ASM_REWRITE_TAC[FINITE_UNION] THEN MATCH_MP_TAC HYPERPLANE_CELLCOMPLEX_MONO THEN EXISTS_TAC `A:real^N#real->bool` THEN ASM_REWRITE_TAC[] THEN SET_TAC[]; RULE_ASSUM_TAC(REWRITE_RULE[RIGHT_IMP_FORALL_THM; IMP_IMP]) THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `euler_characteristic (A UNION B) (s:real^N->bool)` THEN ASM_MESON_TAC[UNION_COMM]]);; let EULER_CHARACTERISTIC_INCLUSION_EXCLUSION = prove (`!A s:(real^N->bool)->bool. FINITE A /\ FINITE s /\ (!k. k IN s ==> hyperplane_cellcomplex A k) ==> euler_characteristic A (UNIONS s) = sum {t | t SUBSET s /\ ~(t = {})} (\t. (-- &1) pow (CARD t + 1) * euler_characteristic A (INTERS t))`, REPEAT STRIP_TAC THEN MP_TAC(ISPECL [`hyperplane_cellcomplex A :(real^N->bool)->bool`; `euler_characteristic A :(real^N->bool)->real`; `s:(real^N->bool)->bool`] INCLUSION_EXCLUSION_REAL_RESTRICTED) THEN ASM_SIMP_TAC[EULER_CHARACTERISTIC_CELLCOMPLEX_UNION] THEN SIMP_TAC[HYPERPLANE_CELLCOMPLEX_EMPTY; HYPERPLANE_CELLCOMPLEX_INTER; HYPERPLANE_CELLCOMPLEX_UNION; HYPERPLANE_CELLCOMPLEX_DIFF]);; (* ------------------------------------------------------------------------- *) (* Euler-type relation for full-dimensional proper polyhedral cones. *) (* ------------------------------------------------------------------------- *) let EULER_POLYHEDRAL_CONE = prove (`!s. polyhedron s /\ conic s /\ ~(interior s = {}) /\ ~(s = (:real^N)) ==> sum (0..dimindex(:N)) (\d. (-- &1) pow d * &(CARD {f | f face_of s /\ aff_dim f = &d })) = &0`, REPEAT STRIP_TAC THEN SUBGOAL_THEN `affine hull s = (:real^N)` ASSUME_TAC THENL [MATCH_MP_TAC(SET_RULE `!s. s = UNIV /\ s SUBSET t ==> t = UNIV`) THEN EXISTS_TAC `affine hull (interior s:real^N->bool)` THEN SIMP_TAC[INTERIOR_SUBSET; HULL_MONO] THEN MATCH_MP_TAC AFFINE_HULL_OPEN THEN ASM_REWRITE_TAC[OPEN_INTERIOR]; ALL_TAC] THEN FIRST_ASSUM (MP_TAC o GEN_REWRITE_RULE I [POLYHEDRON_INTER_AFFINE_MINIMAL]) THEN ASM_REWRITE_TAC[INTER_UNIV; LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `H:(real^N->bool)->bool` THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN DISCH_THEN(CONJUNCTS_THEN2 (ASSUME_TAC o SYM) STRIP_ASSUME_TAC) THEN SUBGOAL_THEN `(vec 0:real^N) IN s` ASSUME_TAC THENL [ASM_SIMP_TAC[CONIC_CONTAINS_0] THEN ASM_MESON_TAC[SUBSET_EMPTY; INTERIOR_SUBSET]; ALL_TAC] THEN SUBGOAL_THEN `!h:real^N->bool. h IN H ==> ?a. ~(a = vec 0) /\ h = {x | a dot x <= &0}` MP_TAC THENL [GEN_TAC THEN DISCH_TAC THEN FIRST_ASSUM(MP_TAC o SPEC `h:real^N->bool`) THEN ANTS_TAC THENL [ASM_REWRITE_TAC[]; MATCH_MP_TAC MONO_EXISTS] THEN X_GEN_TAC `a:real^N` THEN DISCH_THEN(X_CHOOSE_THEN `b:real` STRIP_ASSUME_TAC) THEN SUBGOAL_THEN `b = &0` SUBST_ALL_TAC THENL [ALL_TAC; ASM_REWRITE_TAC[]] THEN MATCH_MP_TAC(REAL_ARITH `&0 <= b /\ ~(&0 < b) ==> b = &0`) THEN CONJ_TAC THENL [SUBGOAL_THEN `(vec 0:real^N) IN INTERS H` MP_TAC THENL [ASM SET_TAC[]; REWRITE_TAC[IN_INTERS]] THEN DISCH_THEN(MP_TAC o SPEC `h:real^N->bool`) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[IN_ELIM_THM; DOT_RZERO]; DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `H DELETE (h:real^N->bool)`) THEN ANTS_TAC THENL [ASM SET_TAC[]; REWRITE_TAC[PSUBSET_ALT]] THEN DISCH_THEN(X_CHOOSE_THEN `x:real^N` STRIP_ASSUME_TAC o CONJUNCT2) THEN SUBGOAL_THEN `?e. &0 < e /\ e < &1 /\ (e % x:real^N) IN h` STRIP_ASSUME_TAC THENL [EXISTS_TAC `min (&1 / &2) (b / ((a:real^N) dot x))` THEN ASM_REWRITE_TAC[IN_ELIM_THM; DOT_RMUL] THEN SUBGOAL_THEN `&0 < (a:real^N) dot x` ASSUME_TAC THENL [MATCH_MP_TAC REAL_LT_TRANS THEN EXISTS_TAC `b:real` THEN ASM_REWRITE_TAC[] THEN UNDISCH_TAC `~((x:real^N) IN s)` THEN EXPAND_TAC "s" THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[REAL_NOT_LT] THEN DISCH_TAC THEN SUBGOAL_THEN `H:(real^N->bool)->bool = h INSERT (H DELETE h)` SUBST1_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN REWRITE_TAC[INTERS_INSERT; IN_INTER] THEN ASM_REWRITE_TAC[IN_ELIM_THM]; ASM_SIMP_TAC[REAL_LT_MIN; REAL_LT_DIV; REAL_MIN_LT] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN ASM_SIMP_TAC[GSYM REAL_LE_RDIV_EQ] THEN REAL_ARITH_TAC]; UNDISCH_TAC `~((x:real^N) IN s)` THEN REWRITE_TAC[] THEN SUBGOAL_THEN `x:real^N = inv e % e % x` SUBST1_TAC THENL [ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; REAL_LT_IMP_NZ; VECTOR_MUL_LID]; ALL_TAC] THEN RULE_ASSUM_TAC(REWRITE_RULE[conic]) THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[REAL_LT_IMP_LE; REAL_LE_INV_EQ] THEN EXPAND_TAC "s" THEN SUBGOAL_THEN `H:(real^N->bool)->bool = h INSERT (H DELETE h)` SUBST1_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN REWRITE_TAC[INTERS_INSERT; IN_INTER] THEN CONJ_TAC THENL [ASM_REWRITE_TAC[]; ALL_TAC] THEN UNDISCH_TAC `(x:real^N) IN INTERS (H DELETE h)` THEN REWRITE_TAC[IN_INTERS] THEN MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `k:real^N->bool` THEN REWRITE_TAC[IN_DELETE] THEN DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN ANTS_TAC THENL [ASM_REWRITE_TAC[]; ALL_TAC] THEN FIRST_X_ASSUM(MP_TAC o SPEC `k:real^N->bool`) THEN ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC [`a':real^N`; `b':real`] THEN STRIP_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN MATCH_MP_TAC(REAL_ARITH `(&0 <= x ==> y <= x) /\ (&0 <= --x ==> &0 <= --y) /\ &0 <= b ==> x <= b ==> y <= b`) THEN REWRITE_TAC[DOT_RMUL; GSYM REAL_MUL_RNEG] THEN REWRITE_TAC[REAL_ARITH `e * x <= x <=> &0 <= x * (&1 - e)`] THEN ASM_SIMP_TAC[REAL_LE_MUL; REAL_LT_IMP_LE; REAL_SUB_LE] THEN SUBGOAL_THEN `(vec 0:real^N) IN INTERS H` MP_TAC THENL [ASM SET_TAC[]; REWRITE_TAC[IN_INTERS]] THEN DISCH_THEN(MP_TAC o SPEC `k:real^N->bool`) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[IN_ELIM_THM; DOT_RZERO]]]; FIRST_X_ASSUM(K ALL_TAC o SPEC `h:real^N->bool`)] THEN GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [RIGHT_IMP_EXISTS_THM] THEN REWRITE_TAC[SKOLEM_THM; LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `fa:(real^N->bool)->real^N` THEN GEN_REWRITE_TAC (LAND_CONV o BINDER_CONV o funpow 2 RAND_CONV) [EQ_SYM_EQ] THEN DISCH_TAC THEN ABBREV_TAC `A = IMAGE (\h. (fa:(real^N->bool)->real^N) h,&0) H` THEN SUBGOAL_THEN `FINITE(A:real^N#real->bool)` ASSUME_TAC THENL [EXPAND_TAC "A" THEN MATCH_MP_TAC FINITE_IMAGE THEN ASM_SIMP_TAC[]; ALL_TAC] THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `euler_characteristic A (s:real^N->bool)` THEN CONJ_TAC THENL [ASM_SIMP_TAC[EULER_CHARACTERISTIC] THEN MATCH_MP_TAC SUM_EQ_NUMSEG THEN X_GEN_TAC `d:num` THEN STRIP_TAC THEN REWRITE_TAC[] THEN AP_TERM_TAC THEN AP_TERM_TAC THEN MATCH_MP_TAC BIJECTIONS_CARD_EQ THEN ASM_SIMP_TAC[FINITE_RESTRICT_HYPERPLANE_CELLS] THEN EXISTS_TAC `relative_interior:(real^N->bool)->(real^N->bool)` THEN EXISTS_TAC `closure:(real^N->bool)->(real^N->bool)` THEN REWRITE_TAC[IN_ELIM_THM] THEN CONJ_TAC THENL [X_GEN_TAC `f:real^N->bool` THEN STRIP_TAC THEN SUBGOAL_THEN `closure(relative_interior f):real^N->bool = f` ASSUME_TAC THENL [MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `closure f:real^N->bool` THEN CONJ_TAC THENL [MATCH_MP_TAC CONVEX_CLOSURE_RELATIVE_INTERIOR THEN ASM_MESON_TAC[FACE_OF_IMP_CONVEX]; REWRITE_TAC[CLOSURE_EQ] THEN MATCH_MP_TAC FACE_OF_IMP_CLOSED THEN ASM_MESON_TAC[POLYHEDRON_IMP_CLOSED; POLYHEDRON_IMP_CONVEX]]; ALL_TAC] THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [ALL_TAC; ONCE_REWRITE_TAC[GSYM AFF_DIM_AFFINE_HULL] THEN ONCE_REWRITE_TAC[GSYM AFFINE_HULL_CLOSURE] THEN ASM_REWRITE_TAC[AFF_DIM_AFFINE_HULL] THEN ASM_MESON_TAC[RELATIVE_INTERIOR_SUBSET; SUBSET_TRANS; FACE_OF_IMP_SUBSET]] THEN SUBGOAL_THEN `~(f:real^N->bool = {})` ASSUME_TAC THENL [ASM_REWRITE_TAC[GSYM AFF_DIM_POS_LE; INT_POS]; ALL_TAC] THEN SUBGOAL_THEN `?J. J SUBSET H /\ f = INTERS {{x:real^N | fa h dot x <= &0} | h IN H} INTER INTERS {{x | fa(h:real^N->bool) dot x = &0} | h IN J}` ASSUME_TAC THENL [ASM_CASES_TAC `f:real^N->bool = s` THENL [EXISTS_TAC `{}:(real^N->bool)->bool` THEN REWRITE_TAC[EMPTY_SUBSET; NOT_IN_EMPTY; INTERS_0; INTER_UNIV; SET_RULE `{f x | x | F} = {}`] THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[SYM(ASSUME `INTERS H = (s:real^N->bool)`)] THEN AP_TERM_TAC THEN MATCH_MP_TAC(SET_RULE `(!x. x IN s ==> f x = x) ==> s = {f x | x IN s}`) THEN ASM_SIMP_TAC[]; ALL_TAC] THEN EXISTS_TAC `{h:real^N->bool | h IN H /\ f SUBSET s INTER {x:real^N | fa h dot x = &0}}` THEN CONJ_TAC THENL [SET_TAC[]; ALL_TAC] THEN MP_TAC(ISPECL [`s:real^N->bool`; `H:(real^N->bool)->bool`; `fa:(real^N->bool)->real^N`; `\h:real^N->bool. &0`] FACE_OF_POLYHEDRON_EXPLICIT) THEN ASM_SIMP_TAC[INTER_UNIV] THEN DISCH_THEN(MP_TAC o SPEC `f:real^N->bool`) THEN ASM_REWRITE_TAC[] THEN SUBGOAL_THEN `INTERS {{x:real^N | fa(h:real^N->bool) dot x <= &0} | h IN H} = s` ASSUME_TAC THENL [EXPAND_TAC "s" THEN AP_TERM_TAC THEN MATCH_MP_TAC(SET_RULE `(!x. x IN s ==> f x = x) ==> {f x | x IN s} = s`) THEN ASM_SIMP_TAC[]; ALL_TAC] THEN ASM_CASES_TAC `{h:real^N->bool | h IN H /\ f SUBSET s INTER {x:real^N | fa h dot x = &0}} = {}` THENL [ONCE_REWRITE_TAC[SIMPLE_IMAGE_GEN] THEN ASM_REWRITE_TAC[IMAGE_CLAUSES; INTERS_0] THEN FIRST_ASSUM(MP_TAC o MATCH_MP FACE_OF_IMP_SUBSET) THEN ASM SET_TAC[]; ALL_TAC] THEN DISCH_THEN(fun th -> GEN_REWRITE_TAC LAND_CONV [th]) THEN ASM_REWRITE_TAC[] THEN GEN_REWRITE_TAC I [EXTENSION] THEN X_GEN_TAC `y:real^N` THEN REWRITE_TAC[IN_INTER; IN_INTERS] THEN REWRITE_TAC[FORALL_IN_GSPEC; IN_INTER] THEN ASM_CASES_TAC `(y:real^N) IN s` THEN ASM_REWRITE_TAC[] THEN ASM SET_TAC[]; ALL_TAC] THEN ABBREV_TAC `H' = IMAGE (\h:real^N->bool. {x:real^N | --(fa h) dot x <= &0}) H` THEN SUBGOAL_THEN `?J. FINITE J /\ J SUBSET (H UNION H') /\ f:real^N->bool = affine hull f INTER INTERS J` MP_TAC THENL [FIRST_X_ASSUM(X_CHOOSE_THEN `J:(real^N->bool)->bool` STRIP_ASSUME_TAC) THEN EXISTS_TAC `H UNION IMAGE (\h:real^N->bool. {x:real^N | --(fa h) dot x <= &0}) J` THEN REPEAT CONJ_TAC THENL [ASM_REWRITE_TAC[FINITE_UNION] THEN MATCH_MP_TAC FINITE_IMAGE THEN ASM_MESON_TAC[FINITE_SUBSET]; EXPAND_TAC "H'" THEN ASM SET_TAC[]; MATCH_MP_TAC(SET_RULE `s SUBSET f /\ s = t ==> s = f INTER t`) THEN REWRITE_TAC[HULL_SUBSET] THEN FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [th]) THEN REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN REWRITE_TAC[INTERS_UNION] THEN MATCH_MP_TAC(SET_RULE `s = s' /\ (!x. x IN s ==> (x IN t <=> x IN t')) ==> s INTER t = s' INTER t'`) THEN CONJ_TAC THENL [AP_TERM_TAC THEN MATCH_MP_TAC(SET_RULE `(!x. x IN s ==> f x = x) ==> {f x | x IN s} = s`) THEN ASM_SIMP_TAC[]; ALL_TAC] THEN X_GEN_TAC `y:real^N` THEN REWRITE_TAC[IN_INTERS] THEN REWRITE_TAC[FORALL_IN_IMAGE; FORALL_IN_GSPEC] THEN REWRITE_TAC[IN_ELIM_THM; DOT_LNEG] THEN REWRITE_TAC[REAL_ARITH `--x <= &0 <=> &0 <= x`] THEN ASM SET_TAC[]]; ALL_TAC] THEN GEN_REWRITE_TAC LAND_CONV [MESON[HAS_SIZE] `(?f. FINITE f /\ P f) <=> (?n f. f HAS_SIZE n /\ P f)`] THEN GEN_REWRITE_TAC LAND_CONV [num_WOP] THEN DISCH_THEN(X_CHOOSE_THEN `nn:num` (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN DISCH_THEN(X_CHOOSE_THEN `J:(real^N->bool)->bool` STRIP_ASSUME_TAC) THEN SUBGOAL_THEN `!J'. J' PSUBSET J ==> (f:real^N->bool) PSUBSET (affine hull f INTER INTERS J')` ASSUME_TAC THENL [REPEAT STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `CARD(J':(real^N->bool)->bool)`) THEN ANTS_TAC THENL [ASM_MESON_TAC[CARD_PSUBSET; HAS_SIZE]; ALL_TAC] THEN REWRITE_TAC[NOT_EXISTS_THM; HAS_SIZE] THEN DISCH_THEN(MP_TAC o SPEC `J':(real^N->bool)->bool`) THEN MATCH_MP_TAC(TAUT `a /\ b /\ (~c ==> d) ==> ~(a /\ b /\ c) ==> d`) THEN CONJ_TAC THENL [ASM_MESON_TAC[PSUBSET; FINITE_SUBSET; HAS_SIZE]; ALL_TAC] THEN CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN MATCH_MP_TAC(SET_RULE `s SUBSET t ==> ~(s = t) ==> s PSUBSET t`) THEN FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [th]) THEN ASM SET_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `!h:real^N->bool. h IN J ==> ?a. {x | a dot x <= &0} = h /\ (h IN H /\ a = fa h \/ ?h'. h' IN H /\ a = --(fa h'))` MP_TAC THENL [X_GEN_TAC `h:real^N->bool` THEN DISCH_TAC THEN SUBGOAL_THEN `(h:real^N->bool) IN (H UNION H')` MP_TAC THENL [ASM SET_TAC[]; EXPAND_TAC "H'"] THEN UNDISCH_THEN `(h:real^N->bool) IN J` (K ALL_TAC) THEN SPEC_TAC(`h:real^N->bool`,`h:real^N->bool`) THEN REWRITE_TAC[IN_UNION; TAUT `(a \/ b ==> c) <=> (a ==> c) /\ (b ==> c)`; FORALL_AND_THM; FORALL_IN_IMAGE] THEN CONJ_TAC THEN X_GEN_TAC `h:real^N->bool` THEN DISCH_TAC THENL [EXISTS_TAC `(fa:(real^N->bool)->real^N) h` THEN ASM_SIMP_TAC[]; EXISTS_TAC `--((fa:(real^N->bool)->real^N) h)` THEN REWRITE_TAC[] THEN DISJ2_TAC THEN ASM_MESON_TAC[]]; ALL_TAC] THEN GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [RIGHT_IMP_EXISTS_THM] THEN REWRITE_TAC[SKOLEM_THM; LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `ga:(real^N->bool)->real^N` THEN DISCH_TAC THEN MP_TAC(ISPECL [`f:real^N->bool`; `J:(real^N->bool)->bool`; `ga:(real^N->bool)->real^N`; `\h:real^N->bool. &0`] RELATIVE_INTERIOR_POLYHEDRON_EXPLICIT) THEN ASM_REWRITE_TAC[] THEN ANTS_TAC THENL [REPEAT CONJ_TAC THENL [ASM_MESON_TAC[HAS_SIZE]; ASM_MESON_TAC[]; ASM_SIMP_TAC[] THEN ASM_MESON_TAC[VECTOR_NEG_EQ_0; SUBSET]]; DISCH_TAC THEN ASM_REWRITE_TAC[]] THEN SUBGOAL_THEN `!h:real^N->bool. h IN J ==> h IN H /\ ga h:real^N = fa h` ASSUME_TAC THENL [SUBGOAL_THEN `~(relative_interior f:real^N->bool = {})` MP_TAC THENL [ASM_MESON_TAC[RELATIVE_INTERIOR_EQ_EMPTY; FACE_OF_IMP_CONVEX]; REWRITE_TAC[GSYM MEMBER_NOT_EMPTY]] THEN DISCH_THEN(X_CHOOSE_TAC `z:real^N`) THEN SUBGOAL_THEN `(z:real^N) IN f /\ z IN s` STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[SUBSET; FACE_OF_IMP_SUBSET; RELATIVE_INTERIOR_SUBSET]; ALL_TAC] THEN X_GEN_TAC `h:real^N->bool` THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `h:real^N->bool`) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN DISCH_THEN(DISJ_CASES_THEN MP_TAC) THEN REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN `h':real^N->bool` STRIP_ASSUME_TAC) THEN UNDISCH_TAC `(z:real^N) IN relative_interior f` THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN DISCH_THEN(MP_TAC o SPEC `h:real^N->bool`) THEN ASM_REWRITE_TAC[DOT_LNEG] THEN UNDISCH_TAC `(z:real^N) IN s` THEN EXPAND_TAC "s" THEN REWRITE_TAC[IN_INTERS] THEN DISCH_THEN(MP_TAC o SPEC `h':real^N->bool`) THEN ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM(MP_TAC o SPEC `h':real^N->bool`) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(fun th -> GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [SYM(CONJUNCT2 th)]) THEN REWRITE_TAC[IN_ELIM_THM] THEN REAL_ARITH_TAC; ALL_TAC] THEN FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [SYM th] THEN MP_TAC(SYM th)) THEN FIRST_X_ASSUM(X_CHOOSE_THEN `K:(real^N->bool)->bool` MP_TAC) THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN DISCH_THEN(fun th -> ASSUME_TAC(SYM th) THEN GEN_REWRITE_TAC (LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV) [th]) THEN REWRITE_TAC[IN_INTER; IN_INTERS; FORALL_IN_GSPEC; GSYM CONJ_ASSOC] THEN REWRITE_TAC[IN_ELIM_THM] THEN DISCH_TAC THEN SUBGOAL_THEN `~(relative_interior f:real^N->bool = {})` ASSUME_TAC THENL [ASM_MESON_TAC[RELATIVE_INTERIOR_EQ_EMPTY; FACE_OF_IMP_CONVEX]; ALL_TAC] THEN SUBGOAL_THEN `DISJOINT (J:(real^N->bool)->bool) K` ASSUME_TAC THENL [UNDISCH_TAC `~(relative_interior f:real^N->bool = {})` THEN FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o LAND_CONV) [SYM th]) THEN REWRITE_TAC[IN_DISJOINT; GSYM MEMBER_NOT_EMPTY; IN_ELIM_THM] THEN ASM_MESON_TAC[REAL_LT_REFL]; ALL_TAC] THEN SUBGOAL_THEN `relative_interior f = INTERS {(if (h:real^N->bool) IN J then {x | fa h dot x < &0} else if h IN K then {x:real^N | fa h dot x = &0} else if relative_interior f SUBSET {x | fa h dot x = &0} then {x | fa h dot x = &0} else {x | fa h dot x < &0}) | h IN H}` ASSUME_TAC THENL [MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL [ALL_TAC; FIRST_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [SYM th]) THEN GEN_REWRITE_TAC I [SUBSET] THEN REWRITE_TAC[IN_INTERS; FORALL_IN_GSPEC; AND_FORALL_THM] THEN X_GEN_TAC `x:real^N` THEN REWRITE_TAC[IN_ELIM_THM] THEN MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `h:real^N->bool` THEN ASM_CASES_TAC `(h:real^N->bool) IN H` THENL [ALL_TAC; DISCH_THEN(K ALL_TAC) THEN ASM SET_TAC[]] THEN ASM_REWRITE_TAC[] THEN ASM_CASES_TAC `(h:real^N->bool) IN J` THEN ASM_SIMP_TAC[IN_ELIM_THM; REAL_LT_IMP_LE] THENL [ASM SET_TAC[]; ALL_TAC] THEN ASM_CASES_TAC `(h:real^N->bool) IN K` THEN ASM_SIMP_TAC[IN_ELIM_THM; REAL_LE_REFL] THEN COND_CASES_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN REAL_ARITH_TAC] THEN GEN_REWRITE_TAC I [SUBSET] THEN X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN REWRITE_TAC[IN_INTERS; FORALL_IN_GSPEC] THEN X_GEN_TAC `h:real^N->bool` THEN DISCH_TAC THEN REPEAT(COND_CASES_TAC THENL [ASM SET_TAC[]; ALL_TAC]) THEN REWRITE_TAC[IN_ELIM_THM; REAL_LT_LE] THEN CONJ_TAC THENL [ASM SET_TAC[]; DISCH_TAC] THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [SET_RULE `~(s SUBSET t) <=> ?y. y IN s /\ ~(y IN t)`]) THEN REWRITE_TAC[IN_ELIM_THM; NOT_EXISTS_THM] THEN X_GEN_TAC `y:real^N` THEN STRIP_TAC THEN FIRST_X_ASSUM(DISJ_CASES_TAC o MATCH_MP (REAL_ARITH `~(x:real = &0) ==> ~(x <= &0) \/ x < &0`)) THENL [ASM SET_TAC[]; ALL_TAC] THEN MP_TAC(ASSUME `(x:real^N) IN relative_interior f`) THEN REWRITE_TAC[IN_RELATIVE_INTERIOR_CBALL] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN REWRITE_TAC[NOT_EXISTS_THM] THEN X_GEN_TAC `e:real` THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN REWRITE_TAC[SUBSET; IN_INTER; IN_CBALL] THEN SUBGOAL_THEN `~(y:real^N = x)` ASSUME_TAC THENL [ASM_MESON_TAC[REAL_LT_REFL]; ALL_TAC] THEN DISCH_THEN(MP_TAC o SPEC `x + e / norm(y - x) % (x - y):real^N`) THEN SUBGOAL_THEN `(x:real^N) IN affine hull f /\ y IN affine hull f` STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[RELATIVE_INTERIOR_SUBSET; SUBSET; HULL_SUBSET]; ASM_SIMP_TAC[IN_AFFINE_ADD_MUL_DIFF; AFFINE_AFFINE_HULL]] THEN REWRITE_TAC[NORM_ARITH `dist(x:real^N,x + r) = norm r`] THEN REWRITE_TAC[NOT_IMP] THEN CONJ_TAC THENL [ASM_SIMP_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM; NORM_SUB; REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN ASM_REAL_ARITH_TAC; DISCH_TAC] THEN SUBGOAL_THEN `(x + e / norm(y - x) % (x - y):real^N) IN s` MP_TAC THENL [ASM_MESON_TAC[SUBSET; FACE_OF_IMP_SUBSET]; ALL_TAC] THEN EXPAND_TAC "s" THEN REWRITE_TAC[IN_INTERS] THEN DISCH_THEN(MP_TAC o SPEC `h:real^N->bool`) THEN ASM_REWRITE_TAC[] THEN FIRST_ASSUM(fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [SYM(CONJUNCT2(MATCH_MP th (ASSUME `(h:real^N->bool) IN H`)))]) THEN ASM_REWRITE_TAC[IN_ELIM_THM; DOT_RADD; REAL_ADD_LID; DOT_RMUL] THEN ASM_REWRITE_TAC[DOT_RSUB; REAL_SUB_LZERO; REAL_NOT_LE] THEN MATCH_MP_TAC REAL_LT_MUL THEN ASM_SIMP_TAC[REAL_LT_DIV; NORM_POS_LT; VECTOR_SUB_EQ] THEN ASM_REAL_ARITH_TAC; ALL_TAC] THEN UNDISCH_TAC `~(relative_interior f:real^N->bool = {})` THEN REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; hyperplane_cell] THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `z:real^N` THEN GEN_REWRITE_TAC RAND_CONV [EXTENSION] THEN ONCE_ASM_REWRITE_TAC[] THEN EXPAND_TAC "A" THEN REWRITE_TAC[IN_INTERS; FORALL_IN_GSPEC] THEN DISCH_THEN(fun th -> X_GEN_TAC `x:real^N` THEN MP_TAC th) THEN GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [IN] THEN REWRITE_TAC[hyperplane_equiv; FORALL_IN_IMAGE] THEN MATCH_MP_TAC(MESON[] `(!h. P h ==> (Q h <=> R h)) ==> (!h. P h) ==> ((!h. Q h) <=> (!h. R h))`) THEN X_GEN_TAC `h:real^N->bool` THEN ASM_CASES_TAC `(h:real^N->bool) IN H` THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[hyperplane_side; REAL_SUB_RZERO] THEN REPEAT(COND_CASES_TAC THEN SIMP_TAC[IN_ELIM_THM] THENL [MESON_TAC[REAL_SGN_EQ]; ALL_TAC]) THEN MESON_TAC[REAL_SGN_EQ]; X_GEN_TAC `c:real^N->bool` THEN STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM AFF_DIM_AFFINE_HULL] THEN REWRITE_TAC[AFFINE_HULL_CLOSURE] THEN ASM_REWRITE_TAC[AFF_DIM_AFFINE_HULL] THEN CONJ_TAC THENL [ALL_TAC; MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `relative_interior c:real^N->bool` THEN CONJ_TAC THENL [MATCH_MP_TAC CONVEX_RELATIVE_INTERIOR_CLOSURE THEN ASM_MESON_TAC[HYPERPLANE_CELL_CONVEX]; ASM_MESON_TAC[HYPERPLANE_CELL_RELATIVE_INTERIOR]]] THEN SUBGOAL_THEN `?J. J SUBSET H /\ c = INTERS {{x | (fa(h:real^N->bool)) dot x < &0} | h IN J} INTER INTERS {{x:real^N | (fa h) dot x = &0} | h IN (H DIFF J)}` MP_TAC THENL [FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [HYPERPLANE_CELL]) THEN EXPAND_TAC "A" THEN REWRITE_TAC[hyperplane_equiv; FORALL_IN_IMAGE] THEN DISCH_THEN(X_CHOOSE_THEN `z:real^N` MP_TAC) THEN REWRITE_TAC[hyperplane_side; REAL_SUB_RZERO] THEN GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV) [EQ_SYM_EQ] THEN DISCH_THEN(ASSUME_TAC o SYM) THEN EXISTS_TAC `{h:real^N->bool | h IN H /\ real_sgn(fa h dot (z:real^N)) = -- &1}` THEN REWRITE_TAC[SET_RULE `{x | x IN s /\ P x} SUBSET s`] THEN REWRITE_TAC[GSYM INTERS_UNION] THEN EXPAND_TAC "c" THEN GEN_REWRITE_TAC I [EXTENSION] THEN X_GEN_TAC `y:real^N` THEN REWRITE_TAC[IN_ELIM_THM; IN_INTERS] THEN REWRITE_TAC[IN_UNION] THEN REWRITE_TAC[TAUT `(a \/ b ==> c) <=> (a ==> c) /\ (b ==> c)`; FORALL_AND_THM] THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN REWRITE_TAC[IN_DIFF; IN_ELIM_THM] THEN REWRITE_TAC[TAUT `a /\ ~(a /\ b) <=> a /\ ~b`] THEN REWRITE_TAC[AND_FORALL_THM] THEN AP_TERM_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `h:real^N->bool` THEN ASM_CASES_TAC `(h:real^N->bool) IN H` THEN ASM_REWRITE_TAC[] THEN REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC (SPEC `(fa:(real^N->bool)->real^N) h dot z` REAL_SGN_CASES) THEN ASM_REWRITE_TAC[] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[REAL_SGN_EQ] THEN SUBGOAL_THEN `?x:real^N. x IN c /\ x IN s` MP_TAC THENL [ASM_MESON_TAC[MEMBER_NOT_EMPTY; SUBSET; NONEMPTY_HYPERPLANE_CELL]; MATCH_MP_TAC(TAUT `~p ==> p ==> q`)] THEN MAP_EVERY EXPAND_TAC ["s"; "c"] THEN REWRITE_TAC[IN_INTERS; IN_ELIM_THM; NOT_EXISTS_THM] THEN X_GEN_TAC `x:real^N` THEN REWRITE_TAC[AND_FORALL_THM] THEN DISCH_THEN(MP_TAC o SPEC `h:real^N->bool`) THEN ASM_REWRITE_TAC[REAL_SGN_EQ] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN FIRST_X_ASSUM(MP_TAC o SPEC `h:real^N->bool`) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(SUBST1_TAC o SYM o CONJUNCT2) THEN REWRITE_TAC[IN_ELIM_THM] THEN ASM_REAL_ARITH_TAC; DISCH_THEN(STRIP_ASSUME_TAC o GSYM)] THEN EXPAND_TAC "c" THEN W(MP_TAC o PART_MATCH (lhand o rand) CLOSURE_INTER_CONVEX o lhand o snd) THEN ANTS_TAC THENL [SIMP_TAC[CONVEX_INTERS; FORALL_IN_GSPEC; CONVEX_HALFSPACE_LT; CONVEX_HYPERPLANE] THEN W(MP_TAC o PART_MATCH (lhand o rand) RELATIVE_INTERIOR_OPEN o lhand o lhand o rand o snd) THEN ANTS_TAC THENL [MATCH_MP_TAC OPEN_INTERS THEN ONCE_REWRITE_TAC[SIMPLE_IMAGE] THEN REWRITE_TAC[FORALL_IN_IMAGE; OPEN_HALFSPACE_LT] THEN MATCH_MP_TAC FINITE_IMAGE THEN ASM_MESON_TAC[FINITE_SUBSET]; DISCH_THEN SUBST1_TAC] THEN W(MP_TAC o PART_MATCH (lhand o rand) RELATIVE_INTERIOR_OPEN_IN o rand o lhand o rand o snd) THEN ANTS_TAC THENL [MATCH_MP_TAC(MESON[OPEN_IN_SUBTOPOLOGY_REFL] `s SUBSET topspace tp /\ t = s ==> open_in (subtopology tp t) s`) THEN REWRITE_TAC[SUBSET_UNIV; TOPSPACE_EUCLIDEAN] THEN REWRITE_TAC[AFFINE_HULL_EQ] THEN SIMP_TAC[AFFINE_INTERS; AFFINE_HYPERPLANE; FORALL_IN_GSPEC]; DISCH_THEN SUBST1_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[NONEMPTY_HYPERPLANE_CELL]]; ALL_TAC] THEN DISCH_THEN SUBST1_TAC THEN SIMP_TAC[CLOSURE_INTERS_CONVEX_OPEN; FORALL_IN_GSPEC; CONVEX_HALFSPACE_LT; OPEN_HALFSPACE_LT] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[EMPTY_FACE_OF; INTER_EMPTY] THEN SUBGOAL_THEN `IMAGE closure {{x | fa h dot x < &0} | h IN J} = {{x | (fa:(real^N->bool)->real^N) h dot x <= &0} | h IN J}` SUBST1_TAC THENL [ONCE_REWRITE_TAC[SIMPLE_IMAGE] THEN REWRITE_TAC[GSYM IMAGE_o; o_DEF] THEN MATCH_MP_TAC(SET_RULE `(!x. x IN s ==> f x = g x) ==> IMAGE f s = IMAGE g s`) THEN GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[] THEN MATCH_MP_TAC CLOSURE_HALFSPACE_LT THEN ASM SET_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `closure (INTERS {{x | fa h dot x = &0} | h IN H DIFF J}) = INTERS {{x | (fa:(real^N->bool)->real^N) h dot x = &0} | h IN H DIFF J}` SUBST1_TAC THENL [REWRITE_TAC[CLOSURE_EQ] THEN SIMP_TAC[CLOSED_INTERS; FORALL_IN_GSPEC; CLOSED_HYPERPLANE]; ALL_TAC] THEN ASM_CASES_TAC `J:(real^N->bool)->bool = H` THENL [ASM_REWRITE_TAC[DIFF_EQ_EMPTY; INTER_UNIV; NOT_IN_EMPTY; SET_RULE `{f x | x | F} = {}`; INTERS_0] THEN FIRST_ASSUM(MP_TAC o MATCH_MP FACE_OF_REFL o MATCH_MP POLYHEDRON_IMP_CONVEX) THEN MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN AP_TERM_TAC THEN EXPAND_TAC "s" THEN AP_TERM_TAC THEN MATCH_MP_TAC(SET_RULE `(!x. x IN s ==> f x = x) ==> s = {f x | x IN s}`) THEN ASM_SIMP_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `INTERS {{x | fa(h:real^N->bool) dot x <= &0} | h IN J} INTER INTERS {{x:real^N | fa h dot x = &0} | h IN H DIFF J} = INTERS {s INTER {x | fa h dot x = &0} | h IN H DIFF J}` SUBST1_TAC THENL [ONCE_REWRITE_TAC[SIMPLE_IMAGE] THEN REWRITE_TAC[INTERS_IMAGE] THEN GEN_REWRITE_TAC I [EXTENSION] THEN X_GEN_TAC `y:real^N` THEN REWRITE_TAC[IN_INTER; IN_ELIM_THM] THEN ASM_CASES_TAC `(y:real^N) IN s` THEN ASM_REWRITE_TAC[] THENL [MATCH_MP_TAC(TAUT `a ==> (a /\ b <=> b)`) THEN UNDISCH_TAC `(y:real^N) IN s` THEN EXPAND_TAC "s" THEN REWRITE_TAC[IN_INTERS] THEN MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `h:real^N->bool` THEN DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN FIRST_X_ASSUM(MP_TAC o SPEC `h:real^N->bool`) THEN ANTS_TAC THENL [ASM SET_TAC[]; SET_TAC[]]; UNDISCH_TAC `~((y:real^N) IN s)` THEN MATCH_MP_TAC (TAUT `~q /\ (p ==> r) ==> ~r ==> (p <=> q)`) THEN CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN EXPAND_TAC "s" THEN REWRITE_TAC[IN_INTERS; AND_FORALL_THM] THEN MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `h:real^N->bool` THEN DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN FIRST_X_ASSUM(MP_TAC o SPEC `h:real^N->bool`) THEN ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN DISCH_THEN(fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM(CONJUNCT2 th)]) THEN ASM_REWRITE_TAC[IN_DIFF; IN_ELIM_THM] THEN ASM_CASES_TAC `(h:real^N->bool) IN J` THEN ASM_SIMP_TAC[REAL_LE_REFL]]; ALL_TAC] THEN MATCH_MP_TAC FACE_OF_INTERS THEN CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN X_GEN_TAC `h:real^N->bool` THEN REWRITE_TAC[IN_DIFF] THEN STRIP_TAC THEN MATCH_MP_TAC FACE_OF_INTER_SUPPORTING_HYPERPLANE_LE THEN ASM_SIMP_TAC[POLYHEDRON_IMP_CONVEX] THEN X_GEN_TAC `y:real^N` THEN EXPAND_TAC "s" THEN REWRITE_TAC[IN_INTERS] THEN DISCH_THEN(MP_TAC o SPEC `h:real^N->bool`) THEN ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM(MP_TAC o SPEC `h:real^N->bool`) THEN ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN DISCH_THEN(fun th -> GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM(CONJUNCT2 th)]) THEN REWRITE_TAC[IN_ELIM_THM]]; ALL_TAC] THEN SUBGOAL_THEN `!h. h IN H ==> hyperplane_cellcomplex A ((:real^N) DIFF h)` ASSUME_TAC THENL [GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC HYPERPLANE_CELLCOMPLEX_MONO THEN EXISTS_TAC `{((fa:(real^N->bool)->real^N) h,&0)}` THEN CONJ_TAC THENL [MATCH_MP_TAC HYPERPLANE_CELL_CELLCOMPLEX THEN ASM_SIMP_TAC[HYPERPLANE_CELL_SING] THEN REPEAT DISJ2_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `h:real^N->bool`) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [SYM(CONJUNCT2 th)]) THEN REWRITE_TAC[EXTENSION; IN_DIFF; IN_ELIM_THM; IN_UNIV] THEN REAL_ARITH_TAC; EXPAND_TAC "A" THEN REWRITE_TAC[IN_IMAGE; SUBSET; FORALL_UNWIND_THM2; IN_SING] THEN ASM_MESON_TAC[]]; ALL_TAC] THEN SUBGOAL_THEN `!h:real^N->bool. h IN H ==> hyperplane_cellcomplex A h` ASSUME_TAC THENL [ASM_MESON_TAC[HYPERPLANE_CELLCOMPLEX_COMPL; SET_RULE `UNIV DIFF (UNIV DIFF s) = s`]; ALL_TAC] THEN SUBGOAL_THEN `hyperplane_cellcomplex A (s:real^N->bool)` ASSUME_TAC THENL [EXPAND_TAC "s" THEN MATCH_MP_TAC HYPERPLANE_CELLCOMPLEX_INTERS THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN MP_TAC(ISPECL [`A:real^N#real->bool`; `INTERS H:real^N->bool`; `(:real^N) DIFF INTERS H`] EULER_CHARACTERISTIC_CELLCOMPLEX_UNION) THEN REWRITE_TAC[SET_RULE `DISJOINT s (UNIV DIFF s)`] THEN ANTS_TAC THENL [ASM_SIMP_TAC[HYPERPLANE_CELLCOMPLEX_DIFF; HYPERPLANE_CELLCOMPLEX_UNIV]; REWRITE_TAC[SET_RULE `s UNION (UNIV DIFF s) = UNIV`]] THEN REWRITE_TAC[DIFF_INTERS] THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(REAL_ARITH `x = (--(&1)) pow (dimindex(:N)) /\ y = (--(&1)) pow (dimindex(:N)) ==> x = s + y ==> s = &0`) THEN CONJ_TAC THENL [MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `euler_characteristic {} (:real^N)` THEN CONJ_TAC THENL [MATCH_MP_TAC EULER_CHARACTERSTIC_INVARIANT THEN ASM_REWRITE_TAC[FINITE_EMPTY] THEN CONJ_TAC THENL [MATCH_MP_TAC HYPERPLANE_CELLCOMPLEX_MONO THEN EXISTS_TAC `{}:real^N#real->bool` THEN REWRITE_TAC[EMPTY_SUBSET]; ALL_TAC] THEN MATCH_MP_TAC HYPERPLANE_CELL_CELLCOMPLEX THEN REWRITE_TAC[HYPERPLANE_CELL_EMPTY]; SIMP_TAC[EULER_CHARACTERISTIC_CELL; HYPERPLANE_CELL_EMPTY] THEN REWRITE_TAC[AFF_DIM_UNIV; NUM_OF_INT_OF_NUM]]; ALL_TAC] THEN W(MP_TAC o PART_MATCH (lhs o rand) EULER_CHARACTERISTIC_INCLUSION_EXCLUSION o lhand o snd) THEN ANTS_TAC THENL [ASM_REWRITE_TAC[FORALL_IN_GSPEC] THEN ONCE_REWRITE_TAC[SIMPLE_IMAGE] THEN ASM_SIMP_TAC[FINITE_IMAGE]; DISCH_THEN SUBST1_TAC] THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `sum {t | t SUBSET {(:real^N) DIFF t | t IN H} /\ ~(t = {})} (\t. -- &1 pow (CARD t + 1) * (--(&1)) pow (dimindex(:N)))` THEN CONJ_TAC THENL [MATCH_MP_TAC SUM_EQ THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN REWRITE_TAC[SIMPLE_IMAGE; IMP_CONJ; FORALL_SUBSET_IMAGE] THEN X_GEN_TAC `J:(real^N->bool)->bool` THEN DISCH_TAC THEN REWRITE_TAC[IMAGE_EQ_EMPTY] THEN DISCH_TAC THEN AP_TERM_TAC THEN ABBREV_TAC `B = IMAGE (\h:real^N->bool. fa h:real^N,&0) J` THEN SUBGOAL_THEN `(B:real^N#real->bool) SUBSET A` ASSUME_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `INTERS (IMAGE (\t. (:real^N) DIFF t) H) = IMAGE (--) (interior s)` ASSUME_TAC THENL [MP_TAC(ISPECL [`s:real^N->bool`; `H:(real^N->bool)->bool`; `fa:(real^N->bool)->real^N`; `\h:real^N->bool. &0`] RELATIVE_INTERIOR_POLYHEDRON_EXPLICIT) THEN ASM_SIMP_TAC[INTER_UNIV] THEN ASM_SIMP_TAC[RELATIVE_INTERIOR_INTERIOR] THEN DISCH_THEN(K ALL_TAC) THEN CONV_TAC SYM_CONV THEN MATCH_MP_TAC SURJECTIVE_IMAGE_EQ THEN REWRITE_TAC[VECTOR_ARITH `--x:real^N = y <=> x = --y`; EXISTS_REFL] THEN X_GEN_TAC `x:real^N` THEN REWRITE_TAC[IN_INTERS; IN_ELIM_THM] THEN REWRITE_TAC[FORALL_IN_IMAGE; IN_DIFF; IN_UNIV] THEN MATCH_MP_TAC(TAUT `(c ==> b) /\ (a <=> c) ==> (a <=> b /\ c)`) THEN CONJ_TAC THENL [EXPAND_TAC "s" THEN REWRITE_TAC[IN_INTERS] THEN MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `h:real^N->bool` THEN ASM_CASES_TAC `(h:real^N->bool) IN H` THEN ASM_REWRITE_TAC[] THEN ASM SET_TAC[REAL_LT_IMP_LE]; MATCH_MP_TAC(MESON[] `(!h. P h ==> (Q h <=> R h)) ==> ((!h. P h ==> Q h) <=> (!h. P h ==> R h))`) THEN X_GEN_TAC `h:real^N->bool` THEN DISCH_TAC THEN FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [SYM(CONJUNCT2(MATCH_MP th (ASSUME `(h:real^N->bool) IN H`)))]) THEN REWRITE_TAC[IN_ELIM_THM; DOT_RNEG] THEN REAL_ARITH_TAC]; ALL_TAC] THEN SUBGOAL_THEN `hyperplane_cell B (INTERS (IMAGE (\t. (:real^N) DIFF t) J))` ASSUME_TAC THENL [SUBGOAL_THEN `~(INTERS (IMAGE (\t. (:real^N) DIFF t) J) = {})` MP_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN REWRITE_TAC[hyperplane_cell; GSYM MEMBER_NOT_EMPTY; IN_INTERS] THEN REWRITE_TAC[FORALL_IN_IMAGE] THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `z:real^N` THEN REWRITE_TAC[IN_UNIV; IN_DIFF] THEN GEN_REWRITE_TAC RAND_CONV [EXTENSION] THEN DISCH_THEN(fun th -> X_GEN_TAC `x:real^N` THEN MP_TAC th) THEN REWRITE_TAC[IN_INTERS; FORALL_IN_IMAGE; IN_DIFF; IN_UNIV] THEN GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [IN] THEN REWRITE_TAC[hyperplane_equiv] THEN EXPAND_TAC "B" THEN REWRITE_TAC[FORALL_IN_IMAGE; hyperplane_side] THEN MATCH_MP_TAC(MESON[] `(!h. P h ==> (Q h <=> R h)) ==> (!h. P h) ==> ((!h. Q h) <=> (!h. R h))`) THEN X_GEN_TAC `h:real^N->bool` THEN ASM_CASES_TAC `(h:real^N->bool) IN J` THEN ASM_REWRITE_TAC[] THEN SUBGOAL_THEN `(h:real^N->bool) IN H` ASSUME_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN FIRST_X_ASSUM(MP_TAC o CONJUNCT2 o C MATCH_MP (ASSUME `(h:real^N->bool) IN H`)) THEN DISCH_THEN(fun th -> GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o ONCE_DEPTH_CONV) [SYM th] THEN GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [SYM th]) THEN REWRITE_TAC[IN_ELIM_THM; REAL_SUB_RZERO; REAL_NOT_LE] THEN MESON_TAC[REAL_SGN_EQ; real_gt]; ALL_TAC] THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `euler_characteristic B (INTERS (IMAGE (\t. (:real^N) DIFF t) J))` THEN CONJ_TAC THENL [MATCH_MP_TAC EULER_CHARACTERSTIC_INVARIANT THEN ASM_SIMP_TAC[HYPERPLANE_CELL_CELLCOMPLEX] THEN CONJ_TAC THENL [ASM_MESON_TAC[FINITE_SUBSET]; ALL_TAC] THEN MATCH_MP_TAC HYPERPLANE_CELLCOMPLEX_MONO THEN EXISTS_TAC `B:real^N#real->bool` THEN ASM_SIMP_TAC[HYPERPLANE_CELL_CELLCOMPLEX]; ALL_TAC] THEN ASM_SIMP_TAC[EULER_CHARACTERISTIC_CELL] THEN AP_TERM_TAC THEN MATCH_MP_TAC(MESON[NUM_OF_INT_OF_NUM] `i = &n ==> num_of_int i = n`) THEN REWRITE_TAC[AFF_DIM_EQ_FULL] THEN MATCH_MP_TAC(SET_RULE `!t. t SUBSET s /\ t = UNIV ==> s = UNIV`) THEN EXISTS_TAC `affine hull (INTERS (IMAGE (\t. (:real^N) DIFF t) H))` THEN CONJ_TAC THENL [MATCH_MP_TAC HULL_MONO THEN ASM SET_TAC[]; ALL_TAC] THEN MATCH_MP_TAC AFFINE_HULL_OPEN THEN ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[IMAGE_EQ_EMPTY; OPEN_NEGATIONS; OPEN_INTERIOR]; ALL_TAC] THEN REWRITE_TAC[SUM_RMUL] THEN MATCH_MP_TAC(REAL_RING `s = &1 ==> s * t = t`) THEN MP_TAC(ISPECL [`\t:(real^N->bool)->bool. CARD t`; `\t:(real^N->bool)->bool. (-- &1) pow (CARD t + 1)`; `{t | t SUBSET {(:real^N) DIFF t | t IN H} /\ ~(t = {})}`; `1..CARD(H:(real^N->bool)->bool)`] SUM_GROUP) THEN ANTS_TAC THENL [CONJ_TAC THENL [MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `{t | t SUBSET {(:real^N) DIFF t | t IN H}}` THEN CONJ_TAC THENL [ALL_TAC; SET_TAC[]] THEN MATCH_MP_TAC FINITE_POWERSET THEN REWRITE_TAC[SIMPLE_IMAGE] THEN ASM_SIMP_TAC[FINITE_IMAGE]; GEN_REWRITE_TAC I [SUBSET] THEN REWRITE_TAC[FORALL_IN_IMAGE] THEN REWRITE_TAC[FORALL_IN_GSPEC; IN_NUMSEG] THEN REWRITE_TAC[SIMPLE_IMAGE; FORALL_SUBSET_IMAGE; IMP_CONJ] THEN X_GEN_TAC `J:(real^N->bool)->bool` THEN DISCH_TAC THEN REWRITE_TAC[IMAGE_EQ_EMPTY] THEN DISCH_TAC THEN SUBGOAL_THEN `FINITE(J:(real^N->bool)->bool)` ASSUME_TAC THENL [ASM_MESON_TAC[FINITE_SUBSET]; ALL_TAC] THEN ASM_SIMP_TAC[CARD_EQ_0; FINITE_IMAGE; ARITH_RULE `1 <= n <=> ~(n = 0)`; IMAGE_EQ_EMPTY] THEN MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `CARD(J:(real^N->bool)->bool)` THEN ASM_SIMP_TAC[CARD_SUBSET; CARD_IMAGE_LE]]; REWRITE_TAC[] THEN DISCH_THEN(SUBST1_TAC o SYM)] THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `sum (1..CARD(H:(real^N->bool)->bool)) (\n. -- &1 pow (n + 1) * &(binom(CARD H,n)))` THEN CONJ_TAC THENL [MATCH_MP_TAC SUM_EQ THEN X_GEN_TAC `n:num` THEN REWRITE_TAC[IN_NUMSEG] THEN DISCH_TAC THEN SIMP_TAC[IN_ELIM_THM] THEN W(MP_TAC o PART_MATCH (lhs o rand) SUM_CONST o lhand o snd) THEN ANTS_TAC THENL [MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `{t | t SUBSET {(:real^N) DIFF t | t IN H}}` THEN CONJ_TAC THENL [ALL_TAC; SET_TAC[]] THEN MATCH_MP_TAC FINITE_POWERSET THEN REWRITE_TAC[SIMPLE_IMAGE] THEN ASM_SIMP_TAC[FINITE_IMAGE]; DISCH_THEN SUBST1_TAC] THEN GEN_REWRITE_TAC LAND_CONV [REAL_MUL_SYM] THEN AP_TERM_TAC THEN AP_TERM_TAC THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `CARD {t | t SUBSET {(:real^N) DIFF t | t IN H} /\ t HAS_SIZE n}` THEN CONJ_TAC THENL [AP_TERM_TAC THEN GEN_REWRITE_TAC I [EXTENSION] THEN X_GEN_TAC `t:(real^N->bool)->bool` THEN REWRITE_TAC[IN_ELIM_THM] THEN ASM_CASES_TAC `t:(real^N->bool)->bool = {}` THEN ASM_REWRITE_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_EMPTY] THENL [ASM_ARITH_TAC; ALL_TAC] THEN MATCH_MP_TAC(TAUT `(p ==> r) ==> (p /\ q <=> p /\ r /\ q)`) THEN SPEC_TAC(`t:(real^N->bool)->bool`,`u:(real^N->bool)->bool`) THEN REWRITE_TAC[SIMPLE_IMAGE; FORALL_SUBSET_IMAGE] THEN ASM_MESON_TAC[FINITE_IMAGE; FINITE_SUBSET]; ALL_TAC] THEN MP_TAC(ISPECL [`CARD(H:(real^N->bool)->bool)`; `n:num`; `{(:real^N) DIFF t | t IN H}`] NUMBER_OF_COMBINATIONS) THEN ANTS_TAC THENL [ALL_TAC; SIMP_TAC[HAS_SIZE]] THEN REWRITE_TAC[SIMPLE_IMAGE] THEN MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN ASM_REWRITE_TAC[GSYM FINITE_HAS_SIZE] THEN SET_TAC[]; ALL_TAC] THEN MP_TAC(ISPECL [`CARD(H:(real^N->bool)->bool)`; `--(&1)`; `&1`] REAL_BINOMIAL_THEOREM) THEN REWRITE_TAC[REAL_POW_ONE; REAL_MUL_RID; REAL_ADD_LINV] THEN SIMP_TAC[SUM_CLAUSES_LEFT; REAL_POW_ADD; REAL_POW_ONE; LE_0] THEN REWRITE_TAC[REAL_ARITH `(x * --(&1) pow 1) * y = --(y * x)`] THEN REWRITE_TAC[real_pow; SUM_NEG; ADD_CLAUSES; REAL_MUL_RID] THEN REWRITE_TAC[binom] THEN MATCH_MP_TAC(REAL_ARITH `x = &0 ==> x = &1 + y ==> --y = &1`) THEN REWRITE_TAC[REAL_POW_ZERO] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN UNDISCH_TAC `CARD(H:(real^N->bool)->bool) = 0` THEN ASM_SIMP_TAC[CARD_EQ_0] THEN DISCH_THEN SUBST_ALL_TAC THEN ASM SET_TAC[]);; (* ------------------------------------------------------------------------- *) (* Euler-Poincare relation for special (n-1)-dimensional polytope. *) (* ------------------------------------------------------------------------- *) let EULER_POINCARE_LEMMA = prove (`!p:real^N->bool. 2 <= dimindex(:N) /\ polytope p /\ affine hull p = {x | x$1 = &1} ==> sum (0..dimindex(:N)-1) (\d. (-- &1) pow d * &(CARD {f | f face_of p /\ aff_dim f = &d })) = &1`, REPEAT STRIP_TAC THEN MP_TAC(ISPECL [`basis 1:real^N`; `&1`] AFF_DIM_HYPERPLANE) THEN SIMP_TAC[BASIS_NONZERO; DOT_BASIS; DIMINDEX_GE_1; LE_REFL] THEN FIRST_ASSUM(SUBST1_TAC o SYM) THEN REWRITE_TAC[AFF_DIM_AFFINE_HULL] THEN ASM_CASES_TAC `p:real^N->bool = {}` THENL [ASM_REWRITE_TAC[AFF_DIM_EMPTY] THEN REWRITE_TAC[INT_ARITH `--(&1):int = x - &1 <=> x = &0`] THEN SIMP_TAC[INT_OF_NUM_EQ; LE_1; DIMINDEX_GE_1]; DISCH_TAC] THEN ABBREV_TAC `s:real^N->bool = conic hull p` THEN MP_TAC(ISPEC `s:real^N->bool` EULER_POLYHEDRAL_CONE) THEN SUBGOAL_THEN `!f. f SUBSET {x:real^N | x$1 = &1} ==> (conic hull f) INTER {x:real^N | x$1 = &1} = f` ASSUME_TAC THENL [GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC SUBSET_ANTISYM THEN ASM_SIMP_TAC[HULL_SUBSET; SUBSET_INTER] THEN REWRITE_TAC[SUBSET; CONIC_HULL_EXPLICIT; IN_INTER; IMP_CONJ] THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN MAP_EVERY X_GEN_TAC [`c:real`; `x:real^N`] THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [SUBSET]) THEN DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN ASM_SIMP_TAC[VECTOR_MUL_COMPONENT; REAL_MUL_RID; VECTOR_MUL_LID]; ALL_TAC] THEN SUBGOAL_THEN `polyhedron(s:real^N->bool)` ASSUME_TAC THENL [EXPAND_TAC "s" THEN FIRST_X_ASSUM(X_CHOOSE_THEN `k:real^N->bool` MP_TAC o GEN_REWRITE_RULE I [polytope]) THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN DISCH_THEN(fun th -> SUBST1_TAC th THEN ASSUME_TAC th) THEN MP_TAC(ISPEC `k:real^N->bool` CONVEX_CONE_HULL_SEPARATE_NONEMPTY) THEN ANTS_TAC THENL [ASM_MESON_TAC[CONVEX_HULL_EQ_EMPTY]; ALL_TAC] THEN DISCH_THEN(SUBST1_TAC o SYM) THEN MATCH_MP_TAC POLYHEDRON_CONVEX_CONE_HULL THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN FIRST_ASSUM(ASSUME_TAC o MATCH_MP POLYHEDRON_IMP_CONVEX) THEN SUBGOAL_THEN `conic(s:real^N->bool)` ASSUME_TAC THENL [ASM_MESON_TAC[CONIC_CONIC_HULL]; ALL_TAC] THEN SUBGOAL_THEN `~(s = (:real^N))` ASSUME_TAC THENL [DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `p:real^N->bool`) THEN ANTS_TAC THENL [ASM_MESON_TAC[HULL_SUBSET]; ALL_TAC] THEN ASM_REWRITE_TAC[INTER_UNIV] THEN DISCH_THEN(ASSUME_TAC o SYM) THEN UNDISCH_TAC `polytope(p:real^N->bool)` THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o MATCH_MP POLYTOPE_IMP_BOUNDED) THEN REWRITE_TAC[BOUNDED_POS; NOT_EXISTS_THM] THEN X_GEN_TAC `B:real` THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN DISCH_THEN(MP_TAC o SPEC `(lambda i. if i = 1 then &1 else B + &1):real^N`) THEN SIMP_TAC[LAMBDA_BETA; DIMINDEX_GE_1; LE_REFL; IN_ELIM_THM] THEN REWRITE_TAC[REAL_NOT_LE] THEN MP_TAC(ISPECL [`(lambda i. if i = 1 then &1 else B + &1):real^N`; `2`] COMPONENT_LE_NORM) THEN ASM_SIMP_TAC[ARITH; LAMBDA_BETA; DIMINDEX_GE_1; LE_REFL] THEN REAL_ARITH_TAC; ALL_TAC] THEN SUBGOAL_THEN `~(s:real^N->bool = {})` ASSUME_TAC THENL [ASM_MESON_TAC[CONIC_HULL_EQ_EMPTY]; ALL_TAC] THEN MP_TAC(ISPEC `s:real^N->bool` CONIC_CONTAINS_0) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN SUBGOAL_THEN `~(interior(s:real^N->bool) = {})` ASSUME_TAC THENL [DISCH_TAC THEN MP_TAC(ISPEC `s:real^N->bool` EMPTY_INTERIOR_SUBSET_HYPERPLANE) THEN ASM_REWRITE_TAC[NOT_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC [`a:real^N`; `b:real`] THEN STRIP_TAC THEN SUBGOAL_THEN `s SUBSET {x:real^N | x$1 = &1}` MP_TAC THENL [FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE `s SUBSET h' ==> h SUBSET h' /\ ~(h PSUBSET h') ==> s SUBSET h`)) THEN CONJ_TAC THENL [FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [SYM th]) THEN MATCH_MP_TAC HULL_MINIMAL THEN REWRITE_TAC[AFFINE_HYPERPLANE] THEN MATCH_MP_TAC SUBSET_TRANS THEN EXISTS_TAC `s:real^N->bool` THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[HULL_SUBSET]; DISCH_TAC THEN MP_TAC(ISPECL [`a:real^N`; `b:real`] AFF_DIM_HYPERPLANE) THEN MP_TAC(ISPECL [`basis 1:real^N`; `&1`] AFF_DIM_HYPERPLANE) THEN ASM_SIMP_TAC[BASIS_NONZERO; DOT_BASIS; DIMINDEX_GE_1; LE_REFL] THEN MATCH_MP_TAC(INT_ARITH `a:int < b ==> a = n ==> ~(b = n)`) THEN MATCH_MP_TAC AFF_DIM_PSUBSET THEN FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE `s PSUBSET t ==> s' = s /\ t' = t ==> s' PSUBSET t'`)) THEN REWRITE_TAC[AFFINE_HULL_EQ; AFFINE_HYPERPLANE] THEN MP_TAC(ISPECL [`basis 1:real^N`; `&1`] AFFINE_HYPERPLANE) THEN SIMP_TAC[BASIS_NONZERO; DOT_BASIS; DIMINDEX_GE_1; LE_REFL]]; REWRITE_TAC[SUBSET; NOT_FORALL_THM; NOT_IMP] THEN EXISTS_TAC `vec 0:real^N` THEN ASM_REWRITE_TAC[IN_ELIM_THM; VEC_COMPONENT] THEN REAL_ARITH_TAC]; ALL_TAC] THEN ASM_REWRITE_TAC[] THEN SUBGOAL_THEN `!x:real^N. x IN s /\ ~(x = vec 0) ==> &0 < x$1` ASSUME_TAC THENL [EXPAND_TAC "s" THEN REWRITE_TAC[CONIC_HULL_EXPLICIT; IMP_CONJ] THEN REWRITE_TAC[FORALL_IN_GSPEC; VECTOR_MUL_EQ_0; DE_MORGAN_THM] THEN MAP_EVERY X_GEN_TAC [`c:real`; `x:real^N`] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[VECTOR_MUL_COMPONENT] THEN MATCH_MP_TAC REAL_LT_MUL THEN CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC] THEN SUBGOAL_THEN `(x:real^N) IN affine hull p` MP_TAC THENL [ASM_MESON_TAC[HULL_SUBSET; SUBSET]; ASM_REWRITE_TAC[]] THEN SIMP_TAC[IN_ELIM_THM; REAL_LT_01]; ALL_TAC] THEN SUBGOAL_THEN `!x:real^N. x IN s ==> &0 <= x$1` ASSUME_TAC THENL [X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN ASM_CASES_TAC `x:real^N = vec 0` THEN ASM_SIMP_TAC[VEC_COMPONENT; REAL_POS; REAL_LT_IMP_LE]; ALL_TAC] THEN W(MP_TAC o PART_MATCH (lhs o rand) SUM_CLAUSES_LEFT o lhand o lhand o snd) THEN REWRITE_TAC[LE_0] THEN DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[AFF_DIM_EQ_0; real_pow; REAL_MUL_LID] THEN SUBGOAL_THEN `{f | f face_of s /\ (?a:real^N. f = {a})} = {{vec 0}}` (fun th -> REWRITE_TAC[th]) THENL [GEN_REWRITE_TAC I [EXTENSION] THEN REWRITE_TAC[IN_ELIM_THM; IN_SING] THEN X_GEN_TAC `f:real^N->bool` THEN EQ_TAC THENL [DISCH_THEN(CONJUNCTS_THEN2 MP_TAC (X_CHOOSE_TAC `a:real^N`)) THEN ASM_REWRITE_TAC[FACE_OF_SING] THEN ASM_MESON_TAC[EXTREME_POINT_OF_CONIC]; DISCH_THEN SUBST1_TAC THEN CONJ_TAC THENL [ALL_TAC; MESON_TAC[]] THEN ASM_REWRITE_TAC[FACE_OF_SING; extreme_point_of; IN_SEGMENT] THEN MAP_EVERY X_GEN_TAC [`a:real^N`; `b:real^N`] THEN STRIP_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN REWRITE_TAC[NOT_EXISTS_THM] THEN X_GEN_TAC `u:real` THEN REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN REWRITE_TAC[CART_EQ] THEN DISCH_THEN(MP_TAC o SPEC `1`) THEN REWRITE_TAC[LE_REFL; DIMINDEX_GE_1; VEC_COMPONENT] THEN REWRITE_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT] THEN SUBGOAL_THEN `&0 < (a:real^N)$1 \/ &0 < (b:real^N)$1` DISJ_CASES_TAC THENL [ASM_MESON_TAC[]; MATCH_MP_TAC(REAL_ARITH `&0 < a /\ &0 <= b ==> ~(&0 = a + b)`); MATCH_MP_TAC(REAL_ARITH `&0 < b /\ &0 <= a ==> ~(&0 = a + b)`)] THEN ASM_SIMP_TAC[REAL_LE_MUL; REAL_LT_IMP_LE; REAL_LT_MUL; REAL_SUB_LT]]; ALL_TAC] THEN SIMP_TAC[CARD_CLAUSES; FINITE_EMPTY; NOT_IN_EMPTY; GSYM REAL_OF_NUM_SUC] THEN MATCH_MP_TAC(REAL_ARITH `s = --t ==> (&0 + &1) + s = &0 ==> t = &1`) THEN SUBGOAL_THEN `dimindex(:N) = (dimindex(:N)-1)+1` (fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th]) THENL [ASM_ARITH_TAC; ALL_TAC] THEN REWRITE_TAC[SUM_OFFSET; GSYM SUM_NEG] THEN MATCH_MP_TAC SUM_EQ_NUMSEG THEN X_GEN_TAC `d:num` THEN STRIP_TAC THEN REWRITE_TAC[REAL_POW_ADD; REAL_POW_1; REAL_MUL_RNEG; REAL_MUL_LNEG] THEN AP_TERM_TAC THEN REWRITE_TAC[REAL_MUL_RID] THEN AP_TERM_TAC THEN AP_TERM_TAC THEN MATCH_MP_TAC BIJECTIONS_CARD_EQ THEN EXISTS_TAC `\f:real^N->bool. f INTER {x | x$1 = &1}` THEN EXISTS_TAC `\f:real^N->bool. conic hull f` THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN CONJ_TAC THENL [DISJ1_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `{f:real^N->bool | f face_of s}` THEN ASM_SIMP_TAC[FINITE_POLYHEDRON_FACES] THEN SET_TAC[]; REWRITE_TAC[IN_ELIM_THM; GSYM INT_OF_NUM_ADD]] THEN SUBGOAL_THEN `!f:real^N->bool. f face_of p ==> conic hull f INTER {x | x$1 = &1} = f` ASSUME_TAC THENL [GEN_TAC THEN DISCH_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN MATCH_MP_TAC SUBSET_TRANS THEN EXISTS_TAC `affine hull p:real^N->bool` THEN CONJ_TAC THENL [ASM_MESON_TAC[FACE_OF_IMP_SUBSET; HULL_SUBSET; SUBSET_TRANS]; ASM_REWRITE_TAC[SUBSET_REFL]]; ASM_SIMP_TAC[]] THEN SUBGOAL_THEN `!f:real^N->bool. f face_of s ==> f INTER {x | x$1 = &1} face_of p` ASSUME_TAC THENL [REPEAT STRIP_TAC THEN SUBGOAL_THEN `p = conic hull p INTER {x:real^N | x$1 = &1}` SUBST1_TAC THENL [ASM_MESON_TAC[FACE_OF_REFL; POLYTOPE_IMP_CONVEX]; ALL_TAC] THEN MATCH_MP_TAC FACE_OF_SLICE THEN ASM_REWRITE_TAC[CONVEX_STANDARD_HYPERPLANE]; ASM_SIMP_TAC[]] THEN SUBGOAL_THEN `!f. f face_of s /\ &0 < aff_dim f ==> conic hull (f INTER {x:real^N | x$1 = &1}) = f` ASSUME_TAC THENL [REPEAT STRIP_TAC THEN MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL [REWRITE_TAC[SUBSET; CONIC_HULL_EXPLICIT; FORALL_IN_GSPEC] THEN REWRITE_TAC[IN_INTER; IN_ELIM_THM] THEN ASM_MESON_TAC[FACE_OF_CONIC; conic]; REWRITE_TAC[SUBSET; CONIC_HULL_EXPLICIT] THEN X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN REWRITE_TAC[IN_ELIM_THM; IN_INTER] THEN ASM_CASES_TAC `x:real^N = vec 0` THENL [SUBGOAL_THEN `?y:real^N. y IN f /\ ~(y = vec 0)` STRIP_ASSUME_TAC THENL [MATCH_MP_TAC(SET_RULE `a IN s /\ ~(s = {a}) ==> ?y. y IN s /\ ~(y = a)`) THEN ASM_MESON_TAC[AFF_DIM_EQ_0; INT_LT_REFL]; SUBGOAL_THEN `&0 < (y:real^N)$1` ASSUME_TAC THENL [ASM_MESON_TAC[FACE_OF_IMP_SUBSET; SUBSET]; ALL_TAC] THEN EXISTS_TAC `&0` THEN ASM_REWRITE_TAC[REAL_POS; VECTOR_MUL_LZERO] THEN EXISTS_TAC `inv(y$1) % y:real^N` THEN ASM_SIMP_TAC[VECTOR_MUL_COMPONENT; REAL_MUL_LINV; REAL_LT_IMP_NZ] THEN ASM_MESON_TAC[FACE_OF_CONIC; conic; REAL_LE_INV_EQ; REAL_LT_IMP_LE]]; SUBGOAL_THEN `&0 < (x:real^N)$1` ASSUME_TAC THENL [ASM_MESON_TAC[FACE_OF_IMP_SUBSET; SUBSET]; ALL_TAC] THEN EXISTS_TAC `(x:real^N)$1` THEN EXISTS_TAC `inv(x$1) % x:real^N` THEN ASM_SIMP_TAC[VECTOR_MUL_COMPONENT; REAL_MUL_LINV; REAL_LT_IMP_LE; REAL_LT_IMP_NZ; VECTOR_MUL_ASSOC; REAL_MUL_RINV; VECTOR_MUL_LID] THEN ASM_MESON_TAC[FACE_OF_CONIC; conic; REAL_LE_INV_EQ; REAL_LT_IMP_LE]]]; ASM_SIMP_TAC[INT_ARITH `&0:int < &d + &1`]] THEN SUBGOAL_THEN `!f:real^N->bool. f face_of p ==> (conic hull f) face_of s` ASSUME_TAC THENL [REPEAT STRIP_TAC THEN ASM_CASES_TAC `f:real^N->bool = {}` THEN ASM_REWRITE_TAC[CONIC_HULL_EMPTY; EMPTY_FACE_OF] THEN REWRITE_TAC[face_of] THEN REPEAT CONJ_TAC THENL [EXPAND_TAC "s" THEN MATCH_MP_TAC HULL_MONO THEN ASM_MESON_TAC[FACE_OF_IMP_SUBSET]; ASM_MESON_TAC[CONVEX_CONIC_HULL; FACE_OF_IMP_CONVEX]; ALL_TAC] THEN EXPAND_TAC "s" THEN REWRITE_TAC[CONIC_HULL_EXPLICIT; IMP_CONJ] THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM; FORALL_IN_GSPEC] THEN MAP_EVERY X_GEN_TAC [`ca:real`; `a:real^N`] THEN STRIP_TAC THEN MAP_EVERY X_GEN_TAC [`cb:real`; `b:real^N`] THEN STRIP_TAC THEN MAP_EVERY X_GEN_TAC [`cx:real`; `x:real^N`] THEN STRIP_TAC THEN ASM_CASES_TAC `cx % x:real^N = vec 0` THENL [ASM_REWRITE_TAC[IN_SEGMENT] THEN MATCH_MP_TAC(TAUT `(a ==> ~b) ==> a /\ b ==> c`) THEN DISCH_TAC THEN DISCH_THEN(X_CHOOSE_THEN `u:real` MP_TAC) THEN REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN REWRITE_TAC[CART_EQ] THEN DISCH_THEN(MP_TAC o SPEC `1`) THEN REWRITE_TAC[LE_REFL; DIMINDEX_GE_1; VEC_COMPONENT] THEN REWRITE_TAC[VECTOR_ADD_COMPONENT] THEN ONCE_REWRITE_TAC[VECTOR_MUL_COMPONENT] THEN SUBGOAL_THEN `&0 < (ca % a:real^N)$1 \/ &0 < (cb % b:real^N)$1` DISJ_CASES_TAC THENL [SUBGOAL_THEN `(ca % a:real^N) IN s /\ (cb % b:real^N) IN s` (fun th -> ASM_MESON_TAC[th]) THEN ASM_MESON_TAC[conic; HULL_SUBSET; SUBSET]; MATCH_MP_TAC(REAL_ARITH `&0 < a /\ &0 <= b ==> ~(&0 = a + b)`); MATCH_MP_TAC(REAL_ARITH `&0 < b /\ &0 <= a ==> ~(&0 = a + b)`)] THEN ASM_SIMP_TAC[REAL_LE_MUL; REAL_LT_IMP_LE; REAL_LT_MUL; REAL_SUB_LT] THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_SIMP_TAC[REAL_LT_IMP_LE; REAL_SUB_LT] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[conic; HULL_SUBSET; SUBSET]; ALL_TAC] THEN UNDISCH_TAC `~(cx % x:real^N = vec 0)` THEN REWRITE_TAC[VECTOR_MUL_EQ_0; DE_MORGAN_THM] THEN STRIP_TAC THEN ASM_CASES_TAC `x:real^N = a` THENL [REWRITE_TAC[IN_SEGMENT] THEN DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC (X_CHOOSE_THEN `u:real` MP_TAC)) THEN REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN ASM_REWRITE_TAC[VECTOR_MUL_ASSOC; VECTOR_ARITH `x % a:real^N = y % a + z % b <=> (x - y) % a = z % b`] THEN DISCH_THEN(fun th -> MP_TAC th THEN MP_TAC th) THEN GEN_REWRITE_TAC LAND_CONV [CART_EQ] THEN DISCH_THEN(MP_TAC o SPEC `1`) THEN REWRITE_TAC[LE_REFL; DIMINDEX_GE_1; VECTOR_MUL_COMPONENT] THEN SUBGOAL_THEN `(a:real^N) IN affine hull p /\ b IN affine hull p` MP_TAC THENL [ASM_MESON_TAC[FACE_OF_IMP_SUBSET; HULL_SUBSET; SUBSET]; ALL_TAC] THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN DISCH_THEN(CONJUNCTS_THEN SUBST1_TAC) THEN REWRITE_TAC[REAL_MUL_RID] THEN DISCH_THEN SUBST1_TAC THEN ASM_SIMP_TAC[VECTOR_MUL_LCANCEL; REAL_ENTIRE; REAL_LT_IMP_NZ] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THENL [CONJ_TAC THENL [MAP_EVERY EXISTS_TAC [`ca:real`; `a:real^N`] THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]; MAP_EVERY EXISTS_TAC [`&0`; `x:real^N`] THEN ASM_REWRITE_TAC[VECTOR_MUL_LZERO; REAL_LE_REFL]]; CONJ_TAC THENL [EXISTS_TAC `ca:real`; EXISTS_TAC `cb:real`] THEN EXISTS_TAC `x:real^N` THEN ASM_REWRITE_TAC[]]; ALL_TAC] THEN ASM_CASES_TAC `x:real^N = b` THENL [REWRITE_TAC[IN_SEGMENT] THEN DISCH_THEN (CONJUNCTS_THEN2 ASSUME_TAC (X_CHOOSE_THEN `u:real` MP_TAC)) THEN REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN ASM_REWRITE_TAC[VECTOR_MUL_ASSOC; VECTOR_ARITH `x % b:real^N = y % a + z % b <=> (x - z) % b = y % a`] THEN DISCH_THEN(fun th -> MP_TAC th THEN MP_TAC th) THEN GEN_REWRITE_TAC LAND_CONV [CART_EQ] THEN DISCH_THEN(MP_TAC o SPEC `1`) THEN REWRITE_TAC[LE_REFL; DIMINDEX_GE_1; VECTOR_MUL_COMPONENT] THEN SUBGOAL_THEN `(a:real^N) IN affine hull p /\ b IN affine hull p` MP_TAC THENL [ASM_MESON_TAC[FACE_OF_IMP_SUBSET; HULL_SUBSET; SUBSET]; ALL_TAC] THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN DISCH_THEN(CONJUNCTS_THEN SUBST1_TAC) THEN REWRITE_TAC[REAL_MUL_RID] THEN DISCH_THEN SUBST1_TAC THEN ASM_SIMP_TAC[VECTOR_MUL_LCANCEL; REAL_ENTIRE; REAL_LT_IMP_NE; REAL_SUB_0] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THENL [CONJ_TAC THENL [MAP_EVERY EXISTS_TAC [`&0`; `x:real^N`] THEN ASM_REWRITE_TAC[VECTOR_MUL_LZERO; REAL_LE_REFL]; MAP_EVERY EXISTS_TAC [`cb:real`; `b:real^N`] THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]]; CONJ_TAC THENL [EXISTS_TAC `ca:real`; EXISTS_TAC `cb:real`] THEN EXISTS_TAC `x:real^N` THEN ASM_REWRITE_TAC[]]; ALL_TAC] THEN DISCH_TAC THEN SUBGOAL_THEN `(x:real^N) IN segment(a,b)` ASSUME_TAC THENL [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [IN_OPEN_SEGMENT]) THEN ASM_REWRITE_TAC[IN_OPEN_SEGMENT] THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN REWRITE_TAC[IN_SEGMENT] THEN DISCH_THEN(X_CHOOSE_THEN `u:real` MP_TAC) THEN REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN DISCH_THEN(fun th -> MP_TAC th THEN MP_TAC th) THEN GEN_REWRITE_TAC LAND_CONV [CART_EQ] THEN DISCH_THEN(MP_TAC o SPEC `1`) THEN REWRITE_TAC[LE_REFL; DIMINDEX_GE_1; VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT] THEN SUBGOAL_THEN `(x:real^N) IN affine hull p /\ a IN affine hull p /\ b IN affine hull p` MP_TAC THENL [ASM_MESON_TAC[FACE_OF_IMP_SUBSET; HULL_SUBSET; SUBSET]; ALL_TAC] THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN SUBST1_TAC) THEN REWRITE_TAC[REAL_MUL_RID] THEN DISCH_THEN(ASSUME_TAC o SYM) THEN DISCH_THEN(MP_TAC o AP_TERM `(%) (inv cx) :real^N->real^N`) THEN ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN DISCH_THEN(K ALL_TAC) THEN EXISTS_TAC `inv(cx) * u * cb` THEN REWRITE_TAC[REAL_ARITH `inv(cx) * x:real = x / cx`] THEN ASM_SIMP_TAC[REAL_LE_RDIV_EQ; REAL_LE_LDIV_EQ; REAL_LT_LE] THEN REPEAT CONJ_TAC THENL [REWRITE_TAC[REAL_MUL_LZERO] THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REAL_ARITH_TAC; FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH `a + b = cx ==> &0 <= a ==> b <= &1 * cx`)) THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REAL_ARITH_TAC; REWRITE_TAC[VECTOR_MUL_ASSOC; VECTOR_ADD_LDISTRIB] THEN BINOP_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN MAP_EVERY UNDISCH_TAC [`(&1 - u) * ca + u * cb = cx`; `~(cx = &0)`] THEN CONV_TAC REAL_FIELD]; FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [face_of]) THEN REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN DISCH_THEN(MP_TAC o SPECL [`a:real^N`; `b:real^N`; `x:real^N`]) THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[]]; ASM_SIMP_TAC[]] THEN SUBGOAL_THEN `!f:real^N->bool. f face_of p /\ ~(f = {}) ==> aff_dim(conic hull f) = aff_dim f + &1` (LABEL_TAC "*") THENL [ALL_TAC; CONJ_TAC THEN X_GEN_TAC `f:real^N->bool` THEN STRIP_TAC THENL [REMOVE_THEN "*" (MP_TAC o SPEC `f INTER {x:real^N | x$1 = &1}`) THEN ASM_SIMP_TAC[INT_ARITH `&0:int < &d + &1`; INT_EQ_ADD_RCANCEL] THEN ANTS_TAC THENL [ALL_TAC; SIMP_TAC[]] THEN SUBGOAL_THEN `?y:real^N. y IN f /\ ~(y = vec 0)` STRIP_ASSUME_TAC THENL [MATCH_MP_TAC(SET_RULE `a IN s /\ ~(s = {a}) ==> ?y. y IN s /\ ~(y = a)`) THEN CONJ_TAC THENL [MP_TAC(ISPECL [`s:real^N->bool`; `f:real^N->bool`] FACE_OF_CONIC) THEN ASM_SIMP_TAC[CONIC_CONTAINS_0] THEN REPEAT DISCH_TAC; DISCH_TAC] THEN UNDISCH_TAC `aff_dim(f:real^N->bool) = &d + &1` THEN ASM_REWRITE_TAC[AFF_DIM_SING; AFF_DIM_EMPTY] THEN INT_ARITH_TAC; REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER; IN_ELIM_THM] THEN SUBGOAL_THEN `&0 < (y:real^N)$1` ASSUME_TAC THENL [ASM_MESON_TAC[FACE_OF_IMP_SUBSET; SUBSET]; ALL_TAC] THEN EXISTS_TAC `inv(y$1) % y:real^N` THEN ASM_SIMP_TAC[VECTOR_MUL_COMPONENT; REAL_MUL_LINV; REAL_LT_IMP_NZ] THEN MP_TAC(ISPECL [`s:real^N->bool`; `f:real^N->bool`] FACE_OF_CONIC) THEN ASM_SIMP_TAC[CONIC_CONTAINS_0] THEN REWRITE_TAC[conic] THEN DISCH_THEN MATCH_MP_TAC THEN ASM_SIMP_TAC[REAL_LE_INV_EQ; REAL_LT_IMP_LE]]; REMOVE_THEN "*" (MP_TAC o SPEC `f:real^N->bool`) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN MATCH_MP_TAC THEN DISCH_TAC THEN UNDISCH_TAC `aff_dim(f:real^N->bool) = &d` THEN ASM_REWRITE_TAC[AFF_DIM_EMPTY] THEN INT_ARITH_TAC]] THEN X_GEN_TAC `f:real^N->bool` THEN STRIP_TAC THEN MATCH_MP_TAC(INT_ARITH `f < a /\ a <= f + &1 ==> a:int = f + &1`) THEN CONJ_TAC THENL [MATCH_MP_TAC AFF_DIM_PSUBSET THEN SIMP_TAC[PSUBSET; HULL_MONO; HULL_SUBSET] THEN REWRITE_TAC[EXTENSION; NOT_FORALL_THM] THEN EXISTS_TAC `vec 0:real^N` THEN MATCH_MP_TAC(TAUT `~p /\ q ==> ~(p <=> q)`) THEN CONJ_TAC THENL [MATCH_MP_TAC(SET_RULE `!t. ~(x IN t) /\ s SUBSET t ==> ~(x IN s)`) THEN EXISTS_TAC `affine hull p:real^N->bool` THEN CONJ_TAC THENL [ASM_REWRITE_TAC[IN_ELIM_THM; VEC_COMPONENT] THEN REAL_ARITH_TAC; MATCH_MP_TAC HULL_MONO THEN ASM_MESON_TAC[FACE_OF_IMP_SUBSET]]; MATCH_MP_TAC(SET_RULE `x IN s /\ s SUBSET P hull s ==> x IN P hull s`) THEN ASM_SIMP_TAC[CONIC_CONTAINS_0; HULL_SUBSET; CONIC_CONIC_HULL] THEN ASM_REWRITE_TAC[CONIC_HULL_EQ_EMPTY]]; MATCH_MP_TAC INT_LE_TRANS THEN EXISTS_TAC `aff_dim((vec 0:real^N) INSERT (affine hull f))` THEN CONJ_TAC THENL [ALL_TAC; REWRITE_TAC[AFF_DIM_INSERT; AFF_DIM_AFFINE_HULL] THEN INT_ARITH_TAC] THEN ONCE_REWRITE_TAC[GSYM AFF_DIM_AFFINE_HULL] THEN MATCH_MP_TAC AFF_DIM_SUBSET THEN MATCH_MP_TAC HULL_MINIMAL THEN REWRITE_TAC[AFFINE_AFFINE_HULL; SUBSET; CONIC_HULL_EXPLICIT] THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN MAP_EVERY X_GEN_TAC [`c:real`; `x:real^N`] THEN STRIP_TAC THEN ONCE_REWRITE_TAC[VECTOR_ARITH `c % x:real^N = vec 0 + c % (x - vec 0)`] THEN MATCH_MP_TAC IN_AFFINE_ADD_MUL_DIFF THEN ASM_SIMP_TAC[AFFINE_AFFINE_HULL; HULL_INC; IN_INSERT]]);; let EULER_POINCARE_SPECIAL = prove (`!p:real^N->bool. 2 <= dimindex(:N) /\ polytope p /\ affine hull p = {x | x$1 = &0} ==> sum (0..dimindex(:N)-1) (\d. (-- &1) pow d * &(CARD {f | f face_of p /\ aff_dim f = &d })) = &1`, REPEAT STRIP_TAC THEN MP_TAC(ISPEC `IMAGE (\x:real^N. basis 1 + x) p` EULER_POINCARE_LEMMA) THEN ASM_REWRITE_TAC[POLYTOPE_TRANSLATION_EQ; AFFINE_HULL_TRANSLATION] THEN ANTS_TAC THENL [MATCH_MP_TAC SURJECTIVE_IMAGE_EQ THEN REWRITE_TAC[EXISTS_REFL; VECTOR_ARITH `a + x:real^N = y <=> x = y - a`] THEN SIMP_TAC[IN_ELIM_THM; VECTOR_ADD_COMPONENT; BASIS_COMPONENT; DIMINDEX_GE_1; LE_REFL] THEN REAL_ARITH_TAC; REWRITE_TAC[SET_RULE `{f | f face_of s /\ P f} = {f | f IN {f | f face_of s} /\ P f}`] THEN REWRITE_TAC[FACES_OF_TRANSLATION] THEN REWRITE_TAC[SET_RULE `{y | y IN IMAGE f s /\ P y} = {f x |x| x IN s /\ P(f x)}`] THEN REWRITE_TAC[AFF_DIM_TRANSLATION_EQ; IN_ELIM_THM] THEN DISCH_THEN(fun th -> GEN_REWRITE_TAC RAND_CONV [SYM th]) THEN MATCH_MP_TAC SUM_EQ_NUMSEG THEN X_GEN_TAC `d:num` THEN STRIP_TAC THEN REWRITE_TAC[] THEN AP_TERM_TAC THEN AP_TERM_TAC THEN GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [SIMPLE_IMAGE_GEN] THEN CONV_TAC SYM_CONV THEN MATCH_MP_TAC CARD_IMAGE_INJ THEN CONJ_TAC THENL [REWRITE_TAC[] THEN MATCH_MP_TAC(MESON[] `(!x y. Q x y ==> x = y) ==> (!x y. P x /\ P y /\ Q x y ==> x = y)`) THEN REWRITE_TAC[INJECTIVE_IMAGE] THEN VECTOR_ARITH_TAC; MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `{f:real^N->bool | f face_of p}` THEN ASM_SIMP_TAC[FINITE_POLYTOPE_FACES] THEN SET_TAC[]]]);; (* ------------------------------------------------------------------------- *) (* Now Euler-Poincare for a general full-dimensional polytope. *) (* ------------------------------------------------------------------------- *) let EULER_POINCARE_FULL = prove (`!p:real^N->bool. polytope p /\ aff_dim p = &(dimindex(:N)) ==> sum (0..dimindex(:N)) (\d. (-- &1) pow d * &(CARD {f | f face_of p /\ aff_dim f = &d })) = &1`, REPEAT STRIP_TAC THEN ABBREV_TAC `f:real^N->real^(N,1)finite_sum = \x. lambda i. if i = 1 then &0 else x$(i-1)` THEN ABBREV_TAC `s = IMAGE (f:real^N->real^(N,1)finite_sum) p` THEN MP_TAC(ISPEC `s:real^(N,1)finite_sum->bool` EULER_POINCARE_SPECIAL) THEN REWRITE_TAC[DIMINDEX_FINITE_SUM; DIMINDEX_1; ADD_SUB] THEN REWRITE_TAC[DIMINDEX_GE_1; ARITH_RULE `2 <= n + 1 <=> 1 <= n`] THEN SUBGOAL_THEN `linear(f:real^N->real^(N,1)finite_sum)` ASSUME_TAC THENL [EXPAND_TAC "f" THEN REWRITE_TAC[linear] THEN SIMP_TAC[CART_EQ; VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT; LAMBDA_BETA] THEN REAL_ARITH_TAC; ALL_TAC] THEN EXPAND_TAC "s" THEN ASM_SIMP_TAC[POLYTOPE_LINEAR_IMAGE; AFFINE_HULL_LINEAR_IMAGE] THEN RULE_ASSUM_TAC(REWRITE_RULE[AFF_DIM_EQ_FULL]) THEN ASM_REWRITE_TAC[] THEN ANTS_TAC THENL [REWRITE_TAC[EXTENSION; IN_IMAGE; IN_ELIM_THM; IN_UNIV] THEN X_GEN_TAC `y:real^(N,1)finite_sum` THEN EQ_TAC THENL [DISCH_THEN(X_CHOOSE_THEN `x:real^N` SUBST1_TAC) THEN EXPAND_TAC "f" THEN SIMP_TAC[LAMBDA_BETA; LE_REFL; DIMINDEX_GE_1]; DISCH_TAC THEN EXISTS_TAC `(lambda i. (y:real^(N,1)finite_sum)$(i+1)):real^N` THEN EXPAND_TAC "f" THEN REWRITE_TAC[CART_EQ; DIMINDEX_FINITE_SUM; DIMINDEX_1] THEN X_GEN_TAC `i:num` THEN STRIP_TAC THEN ASM_SIMP_TAC[CART_EQ; LAMBDA_BETA; DIMINDEX_FINITE_SUM; DIMINDEX_1; DIMINDEX_GE_1; ARITH_RULE `1 <= i /\ ~(i = 1) ==> 1 <= i - 1`; ARITH_RULE `1 <= n /\ i <= n + 1 ==> i - 1 <= n`] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN AP_TERM_TAC THEN ASM_ARITH_TAC]; DISCH_THEN(fun th -> GEN_REWRITE_TAC RAND_CONV [SYM th]) THEN MATCH_MP_TAC SUM_EQ_NUMSEG THEN X_GEN_TAC `d:num` THEN STRIP_TAC THEN REWRITE_TAC[] THEN AP_TERM_TAC THEN AP_TERM_TAC THEN SUBGOAL_THEN `!x y. (f:real^N->real^(N,1)finite_sum) x = f y <=> x = y` ASSUME_TAC THENL [EXPAND_TAC "f" THEN ASM_SIMP_TAC[CART_EQ; LAMBDA_BETA; DIMINDEX_FINITE_SUM; DIMINDEX_1; DIMINDEX_GE_1; ARITH_RULE `1 <= i /\ ~(i = 1) ==> 1 <= i - 1`; ARITH_RULE `1 <= n /\ i <= n + 1 ==> i - 1 <= n`] THEN REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN X_GEN_TAC `i:num` THENL [REPEAT STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `i + 1`) THEN ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN REWRITE_TAC[ADD_SUB] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC; STRIP_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC]; ALL_TAC] THEN EXPAND_TAC "s" THEN MP_TAC(ISPECL [`f:real^N->real^(N,1)finite_sum`; `p:real^N->bool`] FACES_OF_LINEAR_IMAGE) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN REWRITE_TAC[SET_RULE `{f | f face_of s /\ P f} = {f | f IN {f | f face_of s} /\ P f}`] THEN ASM_REWRITE_TAC[SET_RULE `{y | y IN IMAGE f s /\ P y} = {f x |x| x IN s /\ P(f x)}`] THEN ASM_SIMP_TAC[AFF_DIM_INJECTIVE_LINEAR_IMAGE] THEN REWRITE_TAC[IN_ELIM_THM] THEN GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [SIMPLE_IMAGE_GEN] THEN CONV_TAC SYM_CONV THEN MATCH_MP_TAC CARD_IMAGE_INJ THEN CONJ_TAC THENL [REWRITE_TAC[] THEN MATCH_MP_TAC(MESON[] `(!x y. Q x y ==> x = y) ==> (!x y. P x /\ P y /\ Q x y ==> x = y)`) THEN ASM_REWRITE_TAC[INJECTIVE_IMAGE]; MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `{f:real^N->bool | f face_of p}` THEN ASM_SIMP_TAC[FINITE_POLYTOPE_FACES] THEN SET_TAC[]]]);; (* ------------------------------------------------------------------------- *) (* In particular the Euler relation in 3D. *) (* ------------------------------------------------------------------------- *) let EULER_RELATION = prove (`!p:real^3->bool. polytope p /\ aff_dim p = &3 ==> (CARD {v | v face_of p /\ aff_dim(v) = &0} + CARD {f | f face_of p /\ aff_dim(f) = &2}) - CARD {e | e face_of p /\ aff_dim(e) = &1} = 2`, REPEAT STRIP_TAC THEN MP_TAC(ISPEC `p:real^3->bool` EULER_POINCARE_FULL) THEN ASM_REWRITE_TAC[DIMINDEX_3] THEN REWRITE_TAC[TOP_DEPTH_CONV num_CONV `3`; SUM_CLAUSES_NUMSEG] THEN CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[REAL_MUL_LID; REAL_MUL_LNEG] THEN SUBGOAL_THEN `{f:real^3->bool | f face_of p /\ aff_dim f = &3} = {p}` (fun th -> SIMP_TAC[th; NOT_IN_EMPTY; FINITE_EMPTY; CARD_CLAUSES]) THENL [MATCH_MP_TAC(SET_RULE `P a /\ (!x. P x ==> x = a) ==> {x | P x} = {a}`) THEN ASM_SIMP_TAC[FACE_OF_REFL; POLYTOPE_IMP_CONVEX] THEN X_GEN_TAC `f:real^3->bool` THEN STRIP_TAC THEN MP_TAC(ISPECL [`f:real^3->bool`; `p:real^3->bool`] FACE_OF_AFF_DIM_LT) THEN ASM_SIMP_TAC[POLYTOPE_IMP_CONVEX; INT_LT_REFL]; REWRITE_TAC[GSYM REAL_OF_NUM_SUC; REAL_ADD_LID] THEN REWRITE_TAC[REAL_ARITH `((x + --y) + z) + -- &1:real = &1 <=> x + z = y + &2`] THEN REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_EQ] THEN DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[ADD_SUB2]]);;