(* ========================================================================= *)
(* Results connected with topological dimension. *)
(* *)
(* At the moment this is just Brouwer's fixpoint theorem. The proof is from *)
(* Kuhn: "some combinatorial lemmas in topology", IBM J. v4. (1960) p. 518 *)
(* See "http://www.research.ibm.com/journal/rd/045/ibmrd0405K.pdf". *)
(* *)
(* The script below is quite messy, but at least we avoid formalizing any *)
(* topological machinery; we don't even use barycentric subdivision; this is *)
(* the big advantage of Kuhn's proof over the usual Sperner's lemma one. *)
(* *)
(* (c) Copyright, John Harrison 1998-2008 *)
(* ========================================================================= *)
needs "Multivariate/polytope.ml";;
let KUHN_LABELLING_LEMMA = prove
(`!f:real^N->real^N P Q.
(!x. P x ==> P (f x))
==> (!x. P x ==> (!i. Q i ==> &0 <= x$i /\ x$i <= &1))
==> ?l. (!x i. l x i <= 1) /\
(!x i. P x /\ Q i /\ (x$i = &0) ==> (l x i = 0)) /\
(!x i. P x /\ Q i /\ (x$i = &1) ==> (l x i = 1)) /\
(!x i. P x /\ Q i /\ (l x i = 0) ==> x$i <= f(x)$i) /\
(!x i. P x /\ Q i /\ (l x i = 1) ==> f(x)$i <= x$i)`,
let KUHN_COUNTING_LEMMA = prove
(`!face:F->S->bool faces simplices comp comp' bnd.
FINITE faces /\
FINITE simplices /\
(!f. f
IN faces /\ bnd f
==> (
CARD {s | s
IN simplices /\ face f s} = 1)) /\
(!f. f
IN faces /\ ~bnd f
==> (
CARD {s | s
IN simplices /\ face f s} = 2)) /\
(!s. s
IN simplices /\ comp s
==> (
CARD {f | f
IN faces /\ face f s /\ comp' f} = 1)) /\
(!s. s
IN simplices /\ ~comp s
==> (
CARD {f | f
IN faces /\ face f s /\ comp' f} = 0) \/
(
CARD {f | f
IN faces /\ face f s /\ comp' f} = 2))
==>
ODD(
CARD {f | f
IN faces /\ comp' f /\ bnd f})
==>
ODD(
CARD {s | s
IN simplices /\ comp s})`,
REPEAT STRIP_TAC THEN
SUBGOAL_THEN
`sum simplices
(\s:S. &(
CARD {f:F | f
IN faces /\ face f s /\ comp' f})) =
sum simplices
(\s. &(
CARD {f | f
IN {f | f
IN faces /\ comp' f /\ bnd f} /\
face f s})) +
sum simplices
(\s. &(
CARD {f | f
IN {f | f
IN faces /\ comp' f /\ ~(bnd f)} /\
face f s}))`
MP_TAC THENL
[ASM_SIMP_TAC[GSYM
SUM_ADD] THEN MATCH_MP_TAC
SUM_EQ THEN
ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN CONV_TAC SYM_CONV THEN
REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_EQ] THEN
MATCH_MP_TAC
CARD_UNION_EQ THEN ASM_SIMP_TAC[
FINITE_RESTRICT] THEN
REWRITE_TAC[
EXTENSION;
IN_ELIM_THM;
IN_INTER;
IN_UNION;
NOT_IN_EMPTY] THEN
CONJ_TAC THEN GEN_TAC THEN CONV_TAC TAUT;
ALL_TAC] THEN
MP_TAC(ISPECL
[`\s f. (face:F->S->bool) f s`; `simplices:S->bool`;
`{f:F | f
IN faces /\ comp' f /\ bnd f}`; `1`]
SUM_MULTICOUNT) THEN
MP_TAC(ISPECL
[`\s f. (face:F->S->bool) f s`; `simplices:S->bool`;
`{f:F | f
IN faces /\ comp' f /\ ~(bnd f)}`; `2`]
SUM_MULTICOUNT) THEN
REWRITE_TAC[] THEN
REPEAT(ANTS_TAC THENL
[ASM_SIMP_TAC[
FINITE_RESTRICT] THEN GEN_TAC THEN
DISCH_THEN(fun th -> FIRST_ASSUM MATCH_MP_TAC THEN MP_TAC th) THEN
SIMP_TAC[
IN_ELIM_THM];
DISCH_THEN SUBST1_TAC]) THEN
SUBGOAL_THEN
`sum simplices
(\s:S. &(
CARD {f:F | f
IN faces /\ face f s /\ comp' f})) =
sum {s | s
IN simplices /\ comp s}
(\s:S. &(
CARD {f:F | f
IN faces /\ face f s /\ comp' f})) +
sum {s | s
IN simplices /\ ~(comp s)}
(\s:S. &(
CARD {f:F | f
IN faces /\ face f s /\ comp' f}))`
SUBST1_TAC THENL
[CONV_TAC SYM_CONV THEN MATCH_MP_TAC
SUM_UNION_EQ THEN
ASM_REWRITE_TAC[] THEN REWRITE_TAC[
EXTENSION;
NOT_IN_EMPTY] THEN
REWRITE_TAC[
IN_ELIM_THM;
IN_INTER;
IN_UNION] THEN
CONJ_TAC THEN GEN_TAC THEN CONV_TAC TAUT;
ALL_TAC] THEN
SUBGOAL_THEN
`sum {s | s
IN simplices /\ comp s}
(\s:S. &(
CARD {f:F | f
IN faces /\ face f s /\ comp' f})) =
sum {s | s
IN simplices /\ comp s} (\s. &1)`
SUBST1_TAC THENL
[MATCH_MP_TAC
SUM_EQ THEN ASM_SIMP_TAC[
FINITE_RESTRICT] THEN
GEN_TAC THEN REWRITE_TAC[REAL_OF_NUM_EQ] THEN
DISCH_THEN(fun th -> FIRST_ASSUM MATCH_MP_TAC THEN MP_TAC th) THEN
SIMP_TAC[
IN_ELIM_THM];
ALL_TAC] THEN
SUBGOAL_THEN
`sum {s | s
IN simplices /\ ~(comp s)}
(\s:S. &(
CARD {f:F | f
IN faces /\ face f s /\ comp' f})) =
sum {s | s
IN simplices /\ ~(comp s) /\
(
CARD {f | f
IN faces /\ face f s /\ comp' f} = 0)}
(\s:S. &(
CARD {f:F | f
IN faces /\ face f s /\ comp' f})) +
sum {s | s
IN simplices /\ ~(comp s) /\
(
CARD {f | f
IN faces /\ face f s /\ comp' f} = 2)}
(\s:S. &(
CARD {f:F | f
IN faces /\ face f s /\ comp' f}))`
SUBST1_TAC THENL
[CONV_TAC SYM_CONV THEN MATCH_MP_TAC
SUM_UNION_EQ THEN
ASM_SIMP_TAC[
FINITE_RESTRICT] THEN
REWRITE_TAC[
EXTENSION;
NOT_IN_EMPTY;
IN_INTER;
IN_UNION] THEN
CONJ_TAC THENL
[REWRITE_TAC[
IN_ELIM_THM] THEN MESON_TAC[ARITH_RULE `~(2 = 0)`];
ALL_TAC] THEN
X_GEN_TAC `s:S` THEN UNDISCH_TAC
`!s:S. s
IN simplices /\ ~comp s
==> (
CARD {f:F | f
IN faces /\ face f s /\ comp' f} = 0) \/
(
CARD {f | f
IN faces /\ face f s /\ comp' f} = 2)` THEN
DISCH_THEN(MP_TAC o SPEC `s:S`) THEN
REWRITE_TAC[
IN_ELIM_THM] THEN CONV_TAC TAUT;
ALL_TAC] THEN
SUBGOAL_THEN
`!n. sum {s | s
IN simplices /\ ~(comp s) /\
(
CARD {f | f
IN faces /\ face f s /\ comp' f} = n)}
(\s:S. &(
CARD {f:F | f
IN faces /\ face f s /\ comp' f})) =
sum {s | s
IN simplices /\ ~(comp s) /\
(
CARD {f | f
IN faces /\ face f s /\ comp' f} = n)}
(\s:S. &n)`
(fun th -> REWRITE_TAC[th])
THENL
[GEN_TAC THEN MATCH_MP_TAC
SUM_EQ THEN ASM_SIMP_TAC[
FINITE_RESTRICT] THEN
SIMP_TAC[
IN_ELIM_THM];
ALL_TAC] THEN
REWRITE_TAC[
SUM_0] THEN ASM_SIMP_TAC[
SUM_CONST;
FINITE_RESTRICT] THEN
REWRITE_TAC[REAL_OF_NUM_MUL; REAL_OF_NUM_ADD; REAL_OF_NUM_EQ] THEN
REWRITE_TAC[
ADD_CLAUSES;
MULT_CLAUSES] THEN
FIRST_X_ASSUM(CHOOSE_THEN SUBST1_TAC o GEN_REWRITE_RULE I [
ODD_EXISTS]) THEN
DISCH_THEN(MP_TAC o AP_TERM `
ODD`) THEN
REWRITE_TAC[
ODD_ADD;
ODD_MULT;
ARITH_ODD;
ODD]);;
let KUHN_COMPLETE_LEMMA = prove
(`!face:(A->bool)->(A->bool)->bool simplices rl bnd n.
FINITE simplices /\
(!f s. face f s <=> ?a. a
IN s /\ (f = s
DELETE a)) /\
(!s. s
IN simplices ==> s
HAS_SIZE (n + 2) /\
(
IMAGE rl s)
SUBSET 0..n+1) /\
(!f. f
IN {f | ?s. s
IN simplices /\ face f s} /\ bnd f
==> (
CARD {s | s
IN simplices /\ face f s} = 1)) /\
(!f. f
IN {f | ?s. s
IN simplices /\ face f s} /\ ~bnd f
==> (
CARD {s | s
IN simplices /\ face f s} = 2))
==>
ODD(
CARD {f | f
IN {f | ?s. s
IN simplices /\ face f s} /\
(
IMAGE rl f = 0..n) /\ bnd f})
==>
ODD(
CARD {s | s
IN simplices /\ (
IMAGE rl s = 0..n+1)})`,
let KLE_ANTISYM = prove
(`!n x y. kle n x y /\ kle n y x <=> (x = y)`,
REPEAT GEN_TAC THEN EQ_TAC THENL [REWRITE_TAC[kle]; MESON_TAC[
KLE_REFL]] THEN
DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
ASM_REWRITE_TAC[
FUN_EQ_THM] THEN
MESON_TAC[ARITH_RULE `(x = (x + a) + b) ==> (x = x + a:num)`]);;
let KLE_TRANS = prove
(`!x y z n. kle n x y /\ kle n y z /\ (kle n x z \/ kle n z x)
==> kle n x z`,
let KLE_STRICT = prove
(`!n x y. kle n x y /\ ~(x = y)
==> (!j. x(j) <= y(j)) /\ (?k. 1 <= k /\ k <= n /\ x(k) < y(k))`,
REPEAT GEN_TAC THEN REWRITE_TAC[kle] THEN
DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
DISCH_THEN(X_CHOOSE_THEN `k:num->bool` MP_TAC) THEN
ASM_CASES_TAC `k:num->bool = {}` THENL
[ASM_REWRITE_TAC[
NOT_IN_EMPTY;
ADD_CLAUSES; GSYM
FUN_EQ_THM; ETA_AX];
STRIP_TAC THEN ASM_REWRITE_TAC[
LE_ADD] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM
MEMBER_NOT_EMPTY]) THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `i:num` THEN
STRIP_TAC THEN ASM_REWRITE_TAC[ARITH_RULE `n < n + 1`] THEN
ASM_MESON_TAC[
SUBSET;
IN_NUMSEG]]);;
let KLE_MINIMAL = prove
(`!s n.
FINITE s /\ ~(s = {}) /\
(!x y. x
IN s /\ y
IN s ==> kle n x y \/ kle n y x)
==> ?a. a
IN s /\ !x. x
IN s ==> kle n a x`,
REPEAT STRIP_TAC THEN
SUBGOAL_THEN `?a:num->num. a
IN s /\ !x. x
IN s ==> !j. a(j) <= x(j)`
MP_TAC THENL
[MATCH_MP_TAC(REWRITE_RULE[IMP_IMP] POINTWISE_MINIMAL); ALL_TAC] THEN
ASM_MESON_TAC[
POINTWISE_ANTISYM;
KLE_IMP_POINTWISE]);;
let KLE_MAXIMAL = prove
(`!s n.
FINITE s /\ ~(s = {}) /\
(!x y. x
IN s /\ y
IN s ==> kle n x y \/ kle n y x)
==> ?a. a
IN s /\ !x. x
IN s ==> kle n x a`,
REPEAT STRIP_TAC THEN
SUBGOAL_THEN `?a:num->num. a
IN s /\ !x. x
IN s ==> !j. x(j) <= a(j)`
MP_TAC THENL
[MATCH_MP_TAC(REWRITE_RULE[IMP_IMP] POINTWISE_MAXIMAL); ALL_TAC] THEN
ASM_MESON_TAC[
POINTWISE_ANTISYM;
KLE_IMP_POINTWISE]);;
let KLE_RANGE_COMBINE = prove
(`!n x y m1 m2.
kle n x y /\ kle n y z /\ (kle n x z \/ kle n z x) /\
m1 <=
CARD {k | k
IN 1..n /\ x(k) < y(k)} /\
m2 <=
CARD {k | k
IN 1..n /\ y(k) < z(k)}
==> kle n x z /\ m1 + m2 <=
CARD {k | k
IN 1..n /\ x(k) < z(k)}`,
REPEAT GEN_TAC THEN DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
[ASM_MESON_TAC[
KLE_TRANS]; DISCH_TAC] THEN
MATCH_MP_TAC
LE_TRANS THEN
EXISTS_TAC `
CARD {k | k
IN 1..n /\ x(k):num < y(k)} +
CARD {k | k
IN 1..n /\ y(k) < z(k)}` THEN
ASM_SIMP_TAC[
LE_ADD2] THEN MATCH_MP_TAC
EQ_IMP_LE THEN
MATCH_MP_TAC
CARD_UNION_EQ THEN
SIMP_TAC[
FINITE_RESTRICT;
FINITE_NUMSEG] THEN
REWRITE_TAC[
EXTENSION;
IN_ELIM_THM;
IN_INTER;
IN_UNION;
NOT_IN_EMPTY] THEN
CONJ_TAC THENL
[ALL_TAC;
ASM_MESON_TAC[
KLE_IMP_POINTWISE; ARITH_RULE
`x <= y:num /\ y <= z ==> (x < y \/ y < z <=> x < z)`]] THEN
X_GEN_TAC `i:num` THEN UNDISCH_TAC `kle n x z` THEN
REWRITE_TAC[kle] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
ASM_CASES_TAC `i
IN 1..n` THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC(ARITH_RULE `d <= 1 ==> ~(a < x /\ x < a + d)`) THEN
COND_CASES_TAC THEN REWRITE_TAC[ARITH]);;
let KLE_RANGE_COMBINE_L = prove
(`!n x y m.
kle n x y /\ kle n y z /\ (kle n x z \/ kle n z x) /\
m <=
CARD {k | k
IN 1..n /\ y(k) < z(k)}
==> kle n x z /\ m <=
CARD {k | k
IN 1..n /\ x(k) < z(k)}`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `x:num->num = y` THEN ASM_SIMP_TAC[] THEN
DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
SUBGOAL_THEN `kle n x z /\ 1 + m <=
CARD {k | k
IN 1 .. n /\ x k < z k}`
(fun th -> MESON_TAC[th; ARITH_RULE `1 + m <= x ==> m <= x`]) THEN
MATCH_MP_TAC
KLE_RANGE_COMBINE THEN EXISTS_TAC `y:num->num` THEN
ASM_SIMP_TAC[
KLE_STRICT_SET]);;
let KLE_RANGE_COMBINE_R = prove
(`!n x y m.
kle n x y /\ kle n y z /\ (kle n x z \/ kle n z x) /\
m <=
CARD {k | k
IN 1..n /\ x(k) < y(k)}
==> kle n x z /\ m <=
CARD {k | k
IN 1..n /\ x(k) < z(k)}`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `y:num->num = z` THEN ASM_SIMP_TAC[] THEN
DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
SUBGOAL_THEN `kle n x z /\ m + 1 <=
CARD {k | k
IN 1 .. n /\ x k < z k}`
(fun th -> MESON_TAC[th; ARITH_RULE `m + 1 <= x ==> m <= x`]) THEN
MATCH_MP_TAC
KLE_RANGE_COMBINE THEN EXISTS_TAC `y:num->num` THEN
ASM_SIMP_TAC[
KLE_STRICT_SET]);;
let KLE_RANGE_INDUCT = prove
(`!n m s. s
HAS_SIZE (SUC m)
==> (!x y. x
IN s /\ y
IN s ==> kle n x y \/ kle n y x)
==> ?x y. x
IN s /\ y
IN s /\ kle n x y /\
m <=
CARD {k | k
IN 1..n /\ x(k) < y(k)}`,
GEN_TAC THEN INDUCT_TAC THENL
[GEN_TAC THEN REWRITE_TAC[ARITH;
LE_0] THEN
CONV_TAC(LAND_CONV HAS_SIZE_CONV) THEN MESON_TAC[
IN_SING;
KLE_REFL];
ALL_TAC] THEN
X_GEN_TAC `s:(num->num)->bool` THEN
ONCE_REWRITE_TAC[
HAS_SIZE_SUC] THEN REPEAT STRIP_TAC THEN
MP_TAC(SPECL [`s:(num->num)->bool`; `n:num`]
KLE_MINIMAL) THEN
ANTS_TAC THENL [ASM_MESON_TAC[
HAS_SIZE_SUC;
HAS_SIZE]; ALL_TAC] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `a:num->num` THEN
STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `s
DELETE (a:num->num)`) THEN
REPEAT(ANTS_TAC THENL [ASM_MESON_TAC[
IN_DELETE]; ALL_TAC]) THEN
DISCH_THEN(X_CHOOSE_THEN `x:num->num` MP_TAC) THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `b:num->num` THEN
REWRITE_TAC[
IN_DELETE] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[ARITH_RULE `SUC m = 1 + m`] THEN
MATCH_MP_TAC
KLE_RANGE_COMBINE THEN EXISTS_TAC `x:num->num` THEN
ASM_SIMP_TAC[
KLE_STRICT_SET]);;
let KLE_SUC = prove
(`!n x y. kle n x y ==> kle (n + 1) x y`,
REPEAT GEN_TAC THEN REWRITE_TAC[kle] THEN MATCH_MP_TAC
MONO_EXISTS THEN
REWRITE_TAC[
SUBSET;
IN_NUMSEG] THEN
MESON_TAC[ARITH_RULE `k <= n ==> k <= n + 1`]);;
let KLE_TRANS_2 = prove
(`!a b c. kle n a b /\ kle n b c /\ (!j. c j <= a j + 1)
==> kle n a c`,
REPEAT GEN_TAC THEN REWRITE_TAC[
IMP_CONJ] THEN
REWRITE_TAC[kle] THEN
DISCH_THEN(X_CHOOSE_THEN `kk1:num->bool` STRIP_ASSUME_TAC) THEN
DISCH_THEN(X_CHOOSE_THEN `kk2:num->bool` STRIP_ASSUME_TAC) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(fun th ->
EXISTS_TAC `(kk1:num->bool)
UNION kk2` THEN MP_TAC th) THEN
ASM_REWRITE_TAC[
UNION_SUBSET;
IN_UNION] THEN
MATCH_MP_TAC
MONO_FORALL THEN X_GEN_TAC `i:num` THEN
ASM_CASES_TAC `(i:num)
IN kk1` THEN ASM_CASES_TAC `(i:num)
IN kk2` THEN
ASM_REWRITE_TAC[] THEN ARITH_TAC);;
let KLE_BETWEEN_R = prove
(`!a b c x. kle n a b /\ kle n b c /\ kle n a x /\ kle n c x
==> kle n b x`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC
KLE_TRANS_2 THEN
EXISTS_TAC `c:num->num` THEN ASM_REWRITE_TAC[] THEN
ASM_MESON_TAC[
KLE_TRANS_1; ARITH_RULE
`x <= c + 1 /\ c <= b ==> x <= b + 1`]);;
let KLE_BETWEEN_L = prove
(`!a b c x. kle n a b /\ kle n b c /\ kle n x a /\ kle n x c
==> kle n x b`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC
KLE_TRANS_2 THEN
EXISTS_TAC `a:num->num` THEN ASM_REWRITE_TAC[] THEN
ASM_MESON_TAC[
KLE_TRANS_1; ARITH_RULE
`c <= x + 1 /\ b <= c ==> b <= x + 1`]);;
let KLE_ADJACENT = prove
(`!a b x k.
1 <= k /\ k <= n /\ (!j. b(j) = if j = k then a(j) + 1 else a(j)) /\
kle n a x /\ kle n x b
==> (x = a) \/ (x = b)`,
REPEAT STRIP_TAC THEN
REPEAT(FIRST_X_ASSUM(MP_TAC o MATCH_MP
KLE_IMP_POINTWISE)) THEN
ASM_REWRITE_TAC[
FUN_EQ_THM; IMP_IMP;
AND_FORALL_THM] THEN
ASM_CASES_TAC `(x:num->num) k = a k` THENL
[DISCH_THEN(fun th -> DISJ1_TAC THEN MP_TAC th);
DISCH_THEN(fun th -> DISJ2_TAC THEN MP_TAC th)] THEN
MATCH_MP_TAC
MONO_FORALL THEN GEN_TAC THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[
LE_ANTISYM] THEN
ASM_MESON_TAC[ARITH_RULE
`a <= x /\ x <= a + 1 /\ ~(x = a) ==> (x = a + 1)`]);;
let KSIMPLEX_EXTREMA = prove
(`!p n s.
ksimplex p n s
==> ?a b. a
IN s /\ b
IN s /\
(!x. x
IN s ==> kle n a x /\ kle n x b) /\
(!i. b(i) = if 1 <= i /\ i <= n then a(i) + 1 else a(i))`,
REPEAT GEN_TAC THEN REWRITE_TAC[ksimplex] THEN ASM_CASES_TAC `n = 0` THENL
[ASM_REWRITE_TAC[ARITH_RULE `1 <= i /\ i <= 0 <=> F`; GSYM
FUN_EQ_THM] THEN
REWRITE_TAC[
ADD_CLAUSES; ETA_AX] THEN
CONV_TAC(LAND_CONV(LAND_CONV HAS_SIZE_CONV)) THEN
DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
ASM_REWRITE_TAC[
IN_SING] THEN MESON_TAC[
KLE_REFL];
ALL_TAC] THEN
REPEAT STRIP_TAC THEN
MP_TAC(SPECL [`s:(num->num)->bool`; `n:num`]
KLE_MINIMAL) THEN
ANTS_TAC THENL [ASM_MESON_TAC[
HAS_SIZE;
HAS_SIZE_SUC;
ADD1]; ALL_TAC] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `a:num->num` THEN STRIP_TAC THEN
MP_TAC(SPECL [`s:(num->num)->bool`; `n:num`]
KLE_MAXIMAL) THEN
ANTS_TAC THENL [ASM_MESON_TAC[
HAS_SIZE;
HAS_SIZE_SUC;
ADD1]; ALL_TAC] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `b:num->num` THEN STRIP_TAC THEN
ASM_SIMP_TAC[] THEN
MP_TAC(SPECL [`n:num`; `n:num`; `s:(num->num)->bool`]
KLE_RANGE_INDUCT) THEN
ASM_REWRITE_TAC[
ADD1] THEN
DISCH_THEN(X_CHOOSE_THEN `c:num->num` (X_CHOOSE_THEN `d:num->num`
STRIP_ASSUME_TAC)) THEN
SUBGOAL_THEN `{k | k
IN 1 .. n /\ a k :num < b k} = 1..n` MP_TAC THENL
[MATCH_MP_TAC
CARD_SUBSET_LE THEN
ASM_REWRITE_TAC[
CARD_NUMSEG;
ADD_SUB;
FINITE_NUMSEG;
SUBSET_RESTRICT] THEN
SUBGOAL_THEN `kle n a b /\ n <=
CARD {k | k
IN 1..n /\ a(k) < b(k)}`
(fun th -> REWRITE_TAC[th]) THEN
MATCH_MP_TAC
KLE_RANGE_COMBINE_L THEN EXISTS_TAC `c:num->num` THEN
ASM_SIMP_TAC[] THEN
SUBGOAL_THEN `kle n c b /\ n <=
CARD {k | k
IN 1 .. n /\ c k < b k}`
(fun th -> REWRITE_TAC[th]) THEN
MATCH_MP_TAC
KLE_RANGE_COMBINE_R THEN EXISTS_TAC `d:num->num` THEN
ASM_SIMP_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN `kle n a b` MP_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
DISCH_THEN(STRIP_ASSUME_TAC o GEN_REWRITE_RULE I [kle]) THEN
ASM_REWRITE_TAC[
EXTENSION;
IN_ELIM_THM;
IN_NUMSEG] THEN
MATCH_MP_TAC
MONO_FORALL THEN X_GEN_TAC `i:num` THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[
ADD_CLAUSES;
LT_REFL] THEN
ASM_MESON_TAC[
SUBSET;
IN_NUMSEG]);;
let KSIMPLEX_EXTREMA_STRONG = prove
(`!p n s.
ksimplex p n s /\ ~(n = 0)
==> ?a b. a
IN s /\ b
IN s /\ ~(a = b) /\
(!x. x
IN s ==> kle n a x /\ kle n x b) /\
(!i. b(i) = if 1 <= i /\ i <= n then a(i) + 1 else a(i))`,
REPEAT STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o MATCH_MP
KSIMPLEX_EXTREMA) THEN
REPEAT(MATCH_MP_TAC
MONO_EXISTS THEN GEN_TAC) THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST_ALL_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `1`) THEN
ASM_REWRITE_TAC[
LE_REFL; ARITH_RULE `1 <= n <=> ~(n = 0)`] THEN ARITH_TAC);;
let KSIMPLEX_SUCCESSOR = prove
(`!a p n s.
ksimplex p n s /\ a
IN s
==> (!x. x
IN s ==> kle n x a) \/
(?y. y
IN s /\ ?k. 1 <= k /\ k <= n /\
!j. y(j) = if j = k then a(j) + 1 else a(j))`,
REWRITE_TAC[ksimplex] THEN REPEAT STRIP_TAC THEN
REWRITE_TAC[TAUT `a \/ b <=> ~a ==> b`] THEN
REWRITE_TAC[
NOT_FORALL_THM; NOT_IMP] THEN DISCH_TAC THEN
MP_TAC(SPECL [`{x | x
IN s /\ ~kle n x a}`; `n:num`]
KLE_MINIMAL) THEN
RULE_ASSUM_TAC(REWRITE_RULE[
HAS_SIZE]) THEN
ASM_SIMP_TAC[
FINITE_RESTRICT] THEN
ASM_SIMP_TAC[GSYM
MEMBER_NOT_EMPTY;
IN_ELIM_THM] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `b:num->num` THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `1 <=
CARD {k | k
IN 1..n /\ a(k):num < b(k)}` MP_TAC THENL
[MATCH_MP_TAC
KLE_STRICT_SET THEN ASM_MESON_TAC[]; ALL_TAC] THEN
DISCH_THEN(DISJ_CASES_THEN MP_TAC o MATCH_MP (ARITH_RULE
`1 <= n ==> (n = 1) \/ 2 <= n`))
THENL
[DISCH_TAC THEN
MP_TAC(HAS_SIZE_CONV `{k | k
IN 1 .. n /\ a k :num < b k}
HAS_SIZE 1`) THEN
ASM_SIMP_TAC[
HAS_SIZE;
FINITE_RESTRICT;
FINITE_NUMSEG] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `k:num` THEN
REWRITE_TAC[
EXTENSION;
IN_ELIM_THM;
IN_SING;
IN_NUMSEG] THEN
DISCH_THEN(fun th -> CONJ_TAC THENL [MESON_TAC[th]; MP_TAC th]) THEN
DISCH_THEN(fun th -> CONJ_TAC THENL [MESON_TAC[th]; MP_TAC th]) THEN
MATCH_MP_TAC
MONO_FORALL THEN X_GEN_TAC `i:num` THEN
SUBGOAL_THEN `kle n a b` MP_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
DISCH_THEN(STRIP_ASSUME_TAC o GEN_REWRITE_RULE I [kle]) THEN
ASM_REWRITE_TAC[
EXTENSION;
IN_ELIM_THM;
IN_NUMSEG] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[
ADD_CLAUSES;
LT_REFL] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[
ADD_CLAUSES;
LT_REFL] THEN
ASM_MESON_TAC[
SUBSET;
IN_NUMSEG; ARITH_RULE `~(a + 1 = a)`;
ARITH_RULE `a < a + 1`];
ALL_TAC] THEN
DISCH_TAC THEN
MP_TAC(SPECL [`n:num`; `
PRE(
CARD {x | x
IN s /\ ~(kle n x a)})`;
`{x | x
IN s /\ ~(kle n x a)}`]
KLE_RANGE_INDUCT) THEN
ASM_SIMP_TAC[
HAS_SIZE;
FINITE_RESTRICT;
CARD_EQ_0; GSYM
MEMBER_NOT_EMPTY;
ARITH_RULE `(n = SUC(
PRE n)) <=> ~(n = 0)`] THEN
REPEAT(ANTS_TAC THENL
[REWRITE_TAC[
IN_ELIM_THM] THEN ASM_MESON_TAC[]; ALL_TAC]) THEN
DISCH_THEN(X_CHOOSE_THEN `c:num->num`
(X_CHOOSE_THEN `d:num->num` MP_TAC)) THEN
REPEAT(DISCH_THEN(CONJUNCTS_THEN2
(STRIP_ASSUME_TAC o REWRITE_RULE[
IN_ELIM_THM]) MP_TAC)) THEN
DISCH_TAC THEN
MP_TAC(SPECL [`n:num`; `
PRE(
CARD {x | x
IN s /\ kle n x a})`;
`{x | x
IN s /\ kle n x a}`]
KLE_RANGE_INDUCT) THEN
ASM_SIMP_TAC[
HAS_SIZE;
FINITE_RESTRICT;
CARD_EQ_0; GSYM
MEMBER_NOT_EMPTY;
ARITH_RULE `(n = SUC(
PRE n)) <=> ~(n = 0)`] THEN
REPEAT(ANTS_TAC THENL
[REWRITE_TAC[
IN_ELIM_THM] THEN ASM_MESON_TAC[
KLE_REFL]; ALL_TAC]) THEN
DISCH_THEN(X_CHOOSE_THEN `e:num->num`
(X_CHOOSE_THEN `f:num->num` MP_TAC)) THEN
REPEAT(DISCH_THEN(CONJUNCTS_THEN2
(STRIP_ASSUME_TAC o REWRITE_RULE[
IN_ELIM_THM]) MP_TAC)) THEN
DISCH_TAC THEN
SUBGOAL_THEN `kle n e d /\ n + 1 <=
CARD {k | k
IN 1..n /\ e(k) < d(k)}`
MP_TAC THENL
[ALL_TAC;
ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN DISCH_THEN(K ALL_TAC) THEN
DISCH_THEN(MP_TAC o CONJUNCT2) THEN
REWRITE_TAC[ARITH_RULE `~(n + 1 <= x) <=> x <= n`] THEN
MATCH_MP_TAC
LE_TRANS THEN EXISTS_TAC `
CARD(1..n)` THEN
SIMP_TAC[
CARD_SUBSET;
SUBSET_RESTRICT;
FINITE_RESTRICT;
FINITE_NUMSEG] THEN
REWRITE_TAC[
CARD_NUMSEG;
ADD_SUB;
LE_REFL]] THEN
SUBGOAL_THEN
`(
CARD {x | x
IN s /\ kle n x a} - 1) +
2 + (
CARD {x | x
IN s /\ ~kle n x a} - 1) = n + 1`
(SUBST1_TAC o SYM)
THENL
[MATCH_MP_TAC(ARITH_RULE
`~(a = 0) /\ ~(b = 0) /\ (a + b = n + 1)
==> ((a - 1) + 2 + (b - 1) = n + 1)`) THEN
ASM_SIMP_TAC[
CARD_EQ_0;
FINITE_RESTRICT; GSYM
MEMBER_NOT_EMPTY] THEN
REPEAT (CONJ_TAC THENL
[REWRITE_TAC[
IN_ELIM_THM] THEN ASM_MESON_TAC[]; ALL_TAC]) THEN
FIRST_ASSUM(SUBST1_TAC o SYM o CONJUNCT2) THEN
MATCH_MP_TAC
CARD_UNION_EQ THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[
EXTENSION;
NOT_IN_EMPTY;
IN_INTER;
IN_UNION;
IN_ELIM_THM] THEN
ASM_MESON_TAC[];
ALL_TAC] THEN
MATCH_MP_TAC
KLE_RANGE_COMBINE THEN EXISTS_TAC `a:num->num` THEN
CONJ_TAC THENL [ASM_MESON_TAC[
KLE_TRANS]; ALL_TAC] THEN
CONJ_TAC THENL [ASM_MESON_TAC[
KLE_TRANS]; ALL_TAC] THEN
CONJ_TAC THENL [ASM_MESON_TAC[
KLE_TRANS]; ALL_TAC] THEN CONJ_TAC THENL
[W(fun(asl,w) -> SUBGOAL_THEN(mk_conj(`kle n e a`,w))
(fun th -> REWRITE_TAC[th])) THEN
MATCH_MP_TAC
KLE_RANGE_COMBINE_R THEN EXISTS_TAC `f:num->num` THEN
ASM_REWRITE_TAC[ARITH_RULE `k - 1 =
PRE k`];
ALL_TAC] THEN
W(fun(asl,w) -> SUBGOAL_THEN(mk_conj(`kle n a d`,w))
(fun th -> REWRITE_TAC[th])) THEN
MATCH_MP_TAC
KLE_RANGE_COMBINE THEN EXISTS_TAC `b:num->num` THEN
ASM_REWRITE_TAC[ARITH_RULE `k - 1 =
PRE k`] THEN
CONJ_TAC THENL [ASM_MESON_TAC[
KLE_TRANS]; ALL_TAC] THEN
CONJ_TAC THENL [ASM_MESON_TAC[
KLE_TRANS]; ALL_TAC] THEN
CONJ_TAC THENL [ASM_MESON_TAC[
KLE_TRANS]; ALL_TAC] THEN
W(fun(asl,w) -> SUBGOAL_THEN(mk_conj(`kle n b d`,w))
(fun th -> REWRITE_TAC[th])) THEN
MATCH_MP_TAC
KLE_RANGE_COMBINE_L THEN EXISTS_TAC `c:num->num` THEN
ASM_REWRITE_TAC[ARITH_RULE `k - 1 =
PRE k`] THEN ASM_MESON_TAC[
KLE_TRANS]);;
let KSIMPLEX_PREDECESSOR = prove
(`!a p n s.
ksimplex p n s /\ a
IN s
==> (!x. x
IN s ==> kle n a x) \/
(?y. y
IN s /\ ?k. 1 <= k /\ k <= n /\
!j. a(j) = if j = k then y(j) + 1 else y(j))`,
REWRITE_TAC[ksimplex] THEN REPEAT STRIP_TAC THEN
REWRITE_TAC[TAUT `a \/ b <=> ~a ==> b`] THEN
REWRITE_TAC[
NOT_FORALL_THM; NOT_IMP] THEN DISCH_TAC THEN
MP_TAC(SPECL [`{x | x
IN s /\ ~kle n a x}`; `n:num`]
KLE_MAXIMAL) THEN
RULE_ASSUM_TAC(REWRITE_RULE[
HAS_SIZE]) THEN
ASM_SIMP_TAC[
FINITE_RESTRICT] THEN
ASM_SIMP_TAC[GSYM
MEMBER_NOT_EMPTY;
IN_ELIM_THM] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `b:num->num` THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `1 <=
CARD {k | k
IN 1..n /\ b(k):num < a(k)}` MP_TAC THENL
[MATCH_MP_TAC
KLE_STRICT_SET THEN ASM_MESON_TAC[]; ALL_TAC] THEN
DISCH_THEN(DISJ_CASES_THEN MP_TAC o MATCH_MP (ARITH_RULE
`1 <= n ==> (n = 1) \/ 2 <= n`))
THENL
[DISCH_TAC THEN
MP_TAC(HAS_SIZE_CONV `{k | k
IN 1 .. n /\ b k :num < a k}
HAS_SIZE 1`) THEN
ASM_SIMP_TAC[
HAS_SIZE;
FINITE_RESTRICT;
FINITE_NUMSEG] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `k:num` THEN
REWRITE_TAC[
EXTENSION;
IN_ELIM_THM;
IN_SING;
IN_NUMSEG] THEN
DISCH_THEN(fun th -> CONJ_TAC THENL [MESON_TAC[th]; MP_TAC th]) THEN
DISCH_THEN(fun th -> CONJ_TAC THENL [MESON_TAC[th]; MP_TAC th]) THEN
MATCH_MP_TAC
MONO_FORALL THEN X_GEN_TAC `i:num` THEN
SUBGOAL_THEN `kle n b a` MP_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
DISCH_THEN(STRIP_ASSUME_TAC o GEN_REWRITE_RULE I [kle]) THEN
ASM_REWRITE_TAC[
EXTENSION;
IN_ELIM_THM;
IN_NUMSEG] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[
ADD_CLAUSES;
LT_REFL] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[
ADD_CLAUSES;
LT_REFL] THEN
ASM_MESON_TAC[
SUBSET;
IN_NUMSEG; ARITH_RULE `~(a + 1 = a)`;
ARITH_RULE `a < a + 1`];
ALL_TAC] THEN
DISCH_TAC THEN
MP_TAC(SPECL [`n:num`; `
PRE(
CARD {x | x
IN s /\ ~(kle n a x)})`;
`{x | x
IN s /\ ~(kle n a x)}`]
KLE_RANGE_INDUCT) THEN
ASM_SIMP_TAC[
HAS_SIZE;
FINITE_RESTRICT;
CARD_EQ_0; GSYM
MEMBER_NOT_EMPTY;
ARITH_RULE `(n = SUC(
PRE n)) <=> ~(n = 0)`] THEN
REPEAT(ANTS_TAC THENL
[REWRITE_TAC[
IN_ELIM_THM] THEN ASM_MESON_TAC[]; ALL_TAC]) THEN
DISCH_THEN(X_CHOOSE_THEN `d:num->num`
(X_CHOOSE_THEN `c:num->num` MP_TAC)) THEN
REPEAT(DISCH_THEN(CONJUNCTS_THEN2
(STRIP_ASSUME_TAC o REWRITE_RULE[
IN_ELIM_THM]) MP_TAC)) THEN
DISCH_TAC THEN
MP_TAC(SPECL [`n:num`; `
PRE(
CARD {x | x
IN s /\ kle n a x})`;
`{x | x
IN s /\ kle n a x}`]
KLE_RANGE_INDUCT) THEN
ASM_SIMP_TAC[
HAS_SIZE;
FINITE_RESTRICT;
CARD_EQ_0; GSYM
MEMBER_NOT_EMPTY;
ARITH_RULE `(n = SUC(
PRE n)) <=> ~(n = 0)`] THEN
REPEAT(ANTS_TAC THENL
[REWRITE_TAC[
IN_ELIM_THM] THEN ASM_MESON_TAC[
KLE_REFL]; ALL_TAC]) THEN
DISCH_THEN(X_CHOOSE_THEN `f:num->num`
(X_CHOOSE_THEN `e:num->num` MP_TAC)) THEN
REPEAT(DISCH_THEN(CONJUNCTS_THEN2
(STRIP_ASSUME_TAC o REWRITE_RULE[
IN_ELIM_THM]) MP_TAC)) THEN
DISCH_TAC THEN
SUBGOAL_THEN `kle n d e /\ n + 1 <=
CARD {k | k
IN 1..n /\ d(k) < e(k)}`
MP_TAC THENL
[ALL_TAC;
ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN DISCH_THEN(K ALL_TAC) THEN
DISCH_THEN(MP_TAC o CONJUNCT2) THEN
REWRITE_TAC[ARITH_RULE `~(n + 1 <= x) <=> x <= n`] THEN
MATCH_MP_TAC
LE_TRANS THEN EXISTS_TAC `
CARD(1..n)` THEN
SIMP_TAC[
CARD_SUBSET;
SUBSET_RESTRICT;
FINITE_RESTRICT;
FINITE_NUMSEG] THEN
REWRITE_TAC[
CARD_NUMSEG;
ADD_SUB;
LE_REFL]] THEN
SUBGOAL_THEN
`((
CARD {x | x
IN s /\ ~kle n a x} - 1) + 2) +
(
CARD {x | x
IN s /\ kle n a x} - 1) = n + 1`
(SUBST1_TAC o SYM)
THENL
[MATCH_MP_TAC(ARITH_RULE
`~(a = 0) /\ ~(b = 0) /\ (a + b = n + 1)
==> (((b - 1) + 2) + (a - 1) = n + 1)`) THEN
ASM_SIMP_TAC[
CARD_EQ_0;
FINITE_RESTRICT; GSYM
MEMBER_NOT_EMPTY] THEN
REPEAT (CONJ_TAC THENL
[REWRITE_TAC[
IN_ELIM_THM] THEN ASM_MESON_TAC[]; ALL_TAC]) THEN
FIRST_ASSUM(SUBST1_TAC o SYM o CONJUNCT2) THEN
MATCH_MP_TAC
CARD_UNION_EQ THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[
EXTENSION;
NOT_IN_EMPTY;
IN_INTER;
IN_UNION;
IN_ELIM_THM] THEN
ASM_MESON_TAC[];
ALL_TAC] THEN
MATCH_MP_TAC
KLE_RANGE_COMBINE THEN EXISTS_TAC `a:num->num` THEN
CONJ_TAC THENL [ASM_MESON_TAC[
KLE_TRANS]; ALL_TAC] THEN
CONJ_TAC THENL [ASM_MESON_TAC[
KLE_TRANS]; ALL_TAC] THEN
CONJ_TAC THENL [ASM_MESON_TAC[
KLE_TRANS]; ALL_TAC] THEN CONJ_TAC THENL
[ALL_TAC;
W(fun(asl,w) -> SUBGOAL_THEN(mk_conj(`kle n a e`,w))
(fun th -> REWRITE_TAC[th])) THEN
MATCH_MP_TAC
KLE_RANGE_COMBINE_L THEN EXISTS_TAC `f:num->num` THEN
ASM_REWRITE_TAC[ARITH_RULE `k - 1 =
PRE k`]] THEN
W(fun(asl,w) -> SUBGOAL_THEN(mk_conj(`kle n d a`,w))
(fun th -> REWRITE_TAC[th])) THEN
MATCH_MP_TAC
KLE_RANGE_COMBINE THEN EXISTS_TAC `b:num->num` THEN
ASM_REWRITE_TAC[ARITH_RULE `k - 1 =
PRE k`] THEN
CONJ_TAC THENL [ASM_MESON_TAC[
KLE_TRANS]; ALL_TAC] THEN
CONJ_TAC THENL [ASM_MESON_TAC[
KLE_TRANS]; ALL_TAC] THEN
CONJ_TAC THENL [ASM_MESON_TAC[
KLE_TRANS]; ALL_TAC] THEN
W(fun(asl,w) -> SUBGOAL_THEN(mk_conj(`kle n d b`,w))
(fun th -> REWRITE_TAC[th])) THEN
MATCH_MP_TAC
KLE_RANGE_COMBINE_R THEN EXISTS_TAC `c:num->num` THEN
ASM_REWRITE_TAC[ARITH_RULE `k - 1 =
PRE k`] THEN ASM_MESON_TAC[
KLE_TRANS]);;
let SIMPLEX_TOP_FACE = prove
(`0 < p /\
(!x. x
IN f ==> (x(n + 1) = p))
==> ((?s a. ksimplex p (n + 1) s /\ a
IN s /\ (f = s
DELETE a)) <=>
ksimplex p n f)`,
REPEAT STRIP_TAC THEN EQ_TAC THENL
[REWRITE_TAC[ksimplex;
LEFT_IMP_EXISTS_THM] THEN
REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[
IN_DELETE] THEN
REPEAT CONJ_TAC THENL
[UNDISCH_TAC `(s:(num->num)->bool)
HAS_SIZE ((n + 1) + 1)` THEN
SIMP_TAC[
HAS_SIZE;
CARD_DELETE;
FINITE_DELETE] THEN
ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ARITH_TAC;
REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
GEN_TAC THEN X_GEN_TAC `j:num` THEN
ONCE_REWRITE_TAC[ARITH_RULE
`(1 <= j /\ j <= n) <=> (1 <= j /\ j <= n + 1) /\ ~(j = (n + 1))`] THEN
ASM_MESON_TAC[
IN_DELETE];
REPEAT STRIP_TAC THEN
SUBGOAL_THEN `kle (n + 1) x y \/ kle (n + 1) y x` MP_TAC THENL
[ASM_MESON_TAC[]; ALL_TAC] THEN
MATCH_MP_TAC MONO_OR THEN CONJ_TAC THEN
(REWRITE_TAC[kle] THEN
MATCH_MP_TAC
MONO_EXISTS THEN
REWRITE_TAC[GSYM
ADD1;
NUMSEG_CLAUSES; ARITH_RULE `1 <= SUC n`] THEN
X_GEN_TAC `k:num->bool` THEN SIMP_TAC[] THEN
REWRITE_TAC[
SUBSET;
IN_INSERT] THEN
ASM_CASES_TAC `(SUC n)
IN k` THENL
[ALL_TAC; ASM_MESON_TAC[]] THEN
DISCH_THEN(MP_TAC o SPEC `n + 1` o CONJUNCT2) THEN
ASM_REWRITE_TAC[GSYM
ADD1] THEN
ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN DISCH_THEN(K ALL_TAC) THEN
MATCH_MP_TAC(ARITH_RULE `(x = p) /\ (y = p) ==> ~(x = SUC y)`) THEN
CONJ_TAC THEN ASM_MESON_TAC[
ADD1;
IN_DELETE])];
ALL_TAC] THEN
DISCH_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP
KSIMPLEX_EXTREMA) THEN
DISCH_THEN(X_CHOOSE_THEN `a:num->num` (X_CHOOSE_THEN `b:num->num`
STRIP_ASSUME_TAC)) THEN
ABBREV_TAC `c = \i. if i = (n + 1) then p - 1 else a(i)` THEN
MAP_EVERY EXISTS_TAC [`(c:num->num)
INSERT f`; `c:num->num`] THEN
REWRITE_TAC[
IN_INSERT;
DELETE_INSERT] THEN
SUBGOAL_THEN `~((c:num->num)
IN f)` ASSUME_TAC THENL
[DISCH_TAC THEN UNDISCH_TAC `!x:num->num. x
IN f ==> (x (n + 1) = p)` THEN
DISCH_THEN(MP_TAC o SPEC `c:num->num`) THEN ASM_REWRITE_TAC[] THEN
EXPAND_TAC "c" THEN REWRITE_TAC[] THEN UNDISCH_TAC `0 < p` THEN ARITH_TAC;
ALL_TAC] THEN
CONJ_TAC THENL
[ALL_TAC; UNDISCH_TAC `~((c:num->num)
IN f)` THEN SET_TAC[]] THEN
UNDISCH_TAC `ksimplex p n f` THEN REWRITE_TAC[ksimplex] THEN
REPEAT(MATCH_MP_TAC MONO_AND THEN CONJ_TAC) THENL
[SIMP_TAC[
HAS_SIZE;
FINITE_RULES;
CARD_CLAUSES] THEN ASM_REWRITE_TAC[
ADD1];
EXPAND_TAC "c" THEN REWRITE_TAC[
IN_INSERT] THEN
SIMP_TAC[TAUT `(a \/ b ==> c) <=> (a ==> c) /\ (b ==> c)`] THEN
ASM_MESON_TAC[ARITH_RULE `p - 1 <= p`];
EXPAND_TAC "c" THEN REWRITE_TAC[
IN_INSERT; TAUT
`(a \/ b) /\ c ==> d <=> (a /\ c ==> d) /\ (b /\ c ==> d)`] THEN
DISCH_TAC THEN REPEAT GEN_TAC THEN CONJ_TAC THENL
[DISCH_THEN(CONJUNCTS_THEN2 SUBST1_TAC MP_TAC); ALL_TAC] THEN
ASM_MESON_TAC[
LE_REFL; ARITH_RULE `1 <= n + 1`;
ARITH_RULE `j <= n ==> j <= n + 1`];
ALL_TAC] THEN
DISCH_TAC THEN REWRITE_TAC[
IN_INSERT] THEN
SUBGOAL_THEN `!x. x
IN f ==> kle (n + 1) c x`
(fun th -> ASM_MESON_TAC[th;
KLE_SUC;
KLE_REFL]) THEN
X_GEN_TAC `x:num->num` THEN DISCH_TAC THEN
SUBGOAL_THEN `kle (n + 1) a x` MP_TAC THENL
[ASM_MESON_TAC[
KLE_SUC]; ALL_TAC] THEN
EXPAND_TAC "c" THEN REWRITE_TAC[kle] THEN
DISCH_THEN(X_CHOOSE_THEN `k:num->bool` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `(n + 1)
INSERT k` THEN
ASM_REWRITE_TAC[
INSERT_SUBSET;
IN_NUMSEG] THEN
ASM_REWRITE_TAC[
LE_REFL; ARITH_RULE `1 <= n + 1`] THEN
X_GEN_TAC `j:num` THEN REWRITE_TAC[
IN_INSERT] THEN
ASM_CASES_TAC `j = n + 1` THEN ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `~(n + 1
IN k)`
(fun th -> ASM_MESON_TAC[th; ARITH_RULE `0 < p ==> (p = (p - 1) + 1)`]) THEN
DISCH_TAC THEN UNDISCH_TAC `!x:num->num. x
IN f ==> (x (n + 1) = p)` THEN
DISCH_THEN(fun th -> MP_TAC(SPEC `x:num->num` th) THEN
MP_TAC(SPEC `a:num->num` th)) THEN
ASM_REWRITE_TAC[] THEN MESON_TAC[ARITH_RULE `~(p + 1 = p)`]);;
let KSIMPLEX_FIX_PLANE = prove
(`!p q n j s a a0 a1.
ksimplex p n s /\ a
IN s /\
1 <= j /\ j <= n /\ (!x. x
IN (s
DELETE a) ==> (x j = q)) /\
a0
IN s /\ a1
IN s /\
(!i. a1 i = (if 1 <= i /\ i <= n then a0 i + 1 else a0 i))
==> (a = a0) \/ (a = a1)`,
REPEAT STRIP_TAC THEN
MATCH_MP_TAC(TAUT `(~a /\ ~b ==> F) ==> a \/ b`) THEN STRIP_TAC THEN
UNDISCH_TAC `!x:num->num. x
IN s
DELETE a ==> (x j = q)` THEN
DISCH_THEN(fun th ->
MP_TAC(SPEC `a0:num->num` th) THEN MP_TAC(SPEC `a1:num->num` th)) THEN
ASM_REWRITE_TAC[
IN_DELETE] THEN ARITH_TAC);;
let KSIMPLEX_FIX_PLANE_0 = prove
(`!p n j s a a0 a1.
ksimplex p n s /\ a
IN s /\
1 <= j /\ j <= n /\ (!x. x
IN (s
DELETE a) ==> (x j = 0)) /\
a0
IN s /\ a1
IN s /\
(!i. a1 i = (if 1 <= i /\ i <= n then a0 i + 1 else a0 i))
==> (a = a1)`,
REPEAT STRIP_TAC THEN
SUBGOAL_THEN `(a = a0) \/ (a = a1:num->num)` MP_TAC THENL
[MATCH_MP_TAC
KSIMPLEX_FIX_PLANE THEN
MAP_EVERY EXISTS_TAC
[`p:num`; `0`; `n:num`; `j:num`; `s:(num->num)->bool`] THEN
ASM_REWRITE_TAC[];
ALL_TAC] THEN
ASM_CASES_TAC `a0:num->num = a1` THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC(TAUT `~a ==> (a \/ b ==> b)`) THEN
DISCH_THEN SUBST_ALL_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `a1:num->num`) THEN
ASM_REWRITE_TAC[
IN_DELETE] THEN ARITH_TAC);;
let KSIMPLEX_FIX_PLANE_P = prove
(`!p n j s a a0 a1.
ksimplex p n s /\ a
IN s /\
1 <= j /\ j <= n /\ (!x. x
IN (s
DELETE a) ==> (x j = p)) /\
a0
IN s /\ a1
IN s /\
(!i. a1 i = (if 1 <= i /\ i <= n then a0 i + 1 else a0 i))
==> (a = a0)`,
REPEAT STRIP_TAC THEN
SUBGOAL_THEN `(a = a0) \/ (a = a1:num->num)` MP_TAC THENL
[MATCH_MP_TAC
KSIMPLEX_FIX_PLANE THEN
MAP_EVERY EXISTS_TAC
[`p:num`; `p:num`; `n:num`; `j:num`; `s:(num->num)->bool`] THEN
ASM_REWRITE_TAC[];
ALL_TAC] THEN
ASM_CASES_TAC `a0:num->num = a1` THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC(TAUT `~b ==> (a \/ b ==> a)`) THEN
DISCH_THEN SUBST_ALL_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `a0:num->num`) THEN
ASM_REWRITE_TAC[
IN_DELETE] THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [ksimplex]) THEN
DISCH_THEN(MP_TAC o SPEC `a1:num->num` o CONJUNCT1 o CONJUNCT2) THEN
DISCH_THEN(MP_TAC o SPEC `j:num`) THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);;
let KSIMPLEX_REPLACE_0 = prove
(`ksimplex p n s /\ a
IN s /\ ~(n = 0) /\
(?j. 1 <= j /\ j <= n /\ !x. x
IN (s
DELETE a) ==> (x j = 0))
==> (
CARD
{s' | ksimplex p n s' /\ ?b. b
IN s' /\ (s'
DELETE b = s
DELETE a)} =
1)`,
let lemma = prove
(`!a a'. (s' DELETE a' = s DELETE a) /\ (a' = a) /\ a' IN s' /\ a IN s
==> (s' = s)`,
SET_TAC[]) in
REPEAT STRIP_TAC THEN MATCH_MP_TAC HAS_SIZE_CARD THEN
REWRITE_TAC[HAS_SIZE_1_EXISTS] THEN REWRITE_TAC[IN_ELIM_THM] THEN
SUBGOAL_THEN
`!s' a'. ksimplex p n s' /\ a' IN s' /\ (s' DELETE a' = s DELETE a)
==> (s' = s)`
(fun th -> ASM_MESON_TAC[th]) THEN
REPEAT STRIP_TAC THEN
MP_TAC(SPECL [`p:num`; `n:num`; `s:(num->num)->bool`]
KSIMPLEX_EXTREMA_STRONG) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `a0:num->num` (X_CHOOSE_THEN `a1:num->num`
STRIP_ASSUME_TAC)) THEN
MP_TAC(SPECL [`p:num`; `n:num`; `s':(num->num)->bool`]
KSIMPLEX_EXTREMA_STRONG) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `b0:num->num` (X_CHOOSE_THEN `b1:num->num`
STRIP_ASSUME_TAC)) THEN
SUBGOAL_THEN `a:num->num = a1` SUBST_ALL_TAC THENL
[MATCH_MP_TAC KSIMPLEX_FIX_PLANE_0 THEN MAP_EVERY EXISTS_TAC
[`p:num`; `n:num`; `j:num`; `s:(num->num)->bool`; `a0:num->num`] THEN
ASM_REWRITE_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN `a':num->num = b1` SUBST_ALL_TAC THENL
[MATCH_MP_TAC KSIMPLEX_FIX_PLANE_0 THEN MAP_EVERY EXISTS_TAC
[`p:num`; `n:num`; `j:num`; `s':(num->num)->bool`; `b0:num->num`] THEN
ASM_REWRITE_TAC[];
ALL_TAC] THEN
MATCH_MP_TAC lemma THEN
MAP_EVERY EXISTS_TAC [`a1:num->num`; `b1:num->num`] THEN
ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `b0:num->num = a0` MP_TAC THENL
[ONCE_REWRITE_TAC[GSYM KLE_ANTISYM] THEN ASM_MESON_TAC[IN_DELETE];
ASM_REWRITE_TAC[FUN_EQ_THM] THEN MESON_TAC[]]);;
let KSIMPLEX_REPLACE_1 = prove
(`ksimplex p n s /\ a
IN s /\ ~(n = 0) /\
(?j. 1 <= j /\ j <= n /\ !x. x
IN (s
DELETE a) ==> (x j = p))
==> (
CARD
{s' | ksimplex p n s' /\ ?b. b
IN s' /\ (s'
DELETE b = s
DELETE a)} =
1)`,
let lemma = prove
(`!a a'. (s' DELETE a' = s DELETE a) /\ (a' = a) /\ a' IN s' /\ a IN s
==> (s' = s)`,
SET_TAC[]) in
REPEAT STRIP_TAC THEN MATCH_MP_TAC HAS_SIZE_CARD THEN
REWRITE_TAC[HAS_SIZE_1_EXISTS] THEN REWRITE_TAC[IN_ELIM_THM] THEN
SUBGOAL_THEN
`!s' a'. ksimplex p n s' /\ a' IN s' /\ (s' DELETE a' = s DELETE a)
==> (s' = s)`
(fun th -> ASM_MESON_TAC[th]) THEN
REPEAT STRIP_TAC THEN
MP_TAC(SPECL [`p:num`; `n:num`; `s:(num->num)->bool`]
KSIMPLEX_EXTREMA_STRONG) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `a0:num->num` (X_CHOOSE_THEN `a1:num->num`
STRIP_ASSUME_TAC)) THEN
MP_TAC(SPECL [`p:num`; `n:num`; `s':(num->num)->bool`]
KSIMPLEX_EXTREMA_STRONG) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `b0:num->num` (X_CHOOSE_THEN `b1:num->num`
STRIP_ASSUME_TAC)) THEN
SUBGOAL_THEN `a:num->num = a0` SUBST_ALL_TAC THENL
[MATCH_MP_TAC KSIMPLEX_FIX_PLANE_P THEN MAP_EVERY EXISTS_TAC
[`p:num`; `n:num`; `j:num`; `s:(num->num)->bool`; `a1:num->num`] THEN
ASM_REWRITE_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN `a':num->num = b0` SUBST_ALL_TAC THENL
[MATCH_MP_TAC KSIMPLEX_FIX_PLANE_P THEN MAP_EVERY EXISTS_TAC
[`p:num`; `n:num`; `j:num`; `s':(num->num)->bool`; `b1:num->num`] THEN
ASM_REWRITE_TAC[];
ALL_TAC] THEN
MATCH_MP_TAC lemma THEN
MAP_EVERY EXISTS_TAC [`a0:num->num`; `b0:num->num`] THEN
ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `b1:num->num = a1` MP_TAC THENL
[ONCE_REWRITE_TAC[GSYM KLE_ANTISYM] THEN ASM_MESON_TAC[IN_DELETE];
ASM_REWRITE_TAC[FUN_EQ_THM] THEN MATCH_MP_TAC MONO_FORALL THEN
MESON_TAC[EQ_ADD_RCANCEL]]);;
let KSIMPLEX_REPLACE_2 = prove
(`ksimplex p n s /\ a
IN s /\ ~(n = 0) /\
~(?j. 1 <= j /\ j <= n /\ !x. x
IN (s
DELETE a) ==> (x j = 0)) /\
~(?j. 1 <= j /\ j <= n /\ !x. x
IN (s
DELETE a) ==> (x j = p))
==> (
CARD
{s' | ksimplex p n s' /\ ?b. b
IN s' /\ (s'
DELETE b = s
DELETE a)} =
2)`,
let lemma = prove
(`!a a'. (s' DELETE a' = s DELETE a) /\ (a' = a) /\ a' IN s' /\ a IN s
==> (s' = s)`,
SET_TAC[])
and lemma_1 = prove
(`a IN s /\ ~(b = a) ==> ~(s = b INSERT (s DELETE a))`,
SET_TAC[]) in
REPEAT STRIP_TAC THEN
MP_TAC(SPECL [`p:num`; `n:num`; `s:(num->num)->bool`]
KSIMPLEX_EXTREMA_STRONG) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `a0:num->num` (X_CHOOSE_THEN `a1:num->num`
STRIP_ASSUME_TAC)) THEN
ASM_CASES_TAC `a:num->num = a0` THENL
[FIRST_X_ASSUM SUBST_ALL_TAC THEN
MP_TAC(SPECL [`a0:num->num`; `p:num`; `n:num`; `s:(num->num)->bool`]
KSIMPLEX_SUCCESSOR) THEN
ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC(TAUT `~a /\ (b ==> c) ==> a \/ b ==> c`) THEN CONJ_TAC THENL
[DISCH_THEN(MP_TAC o SPEC `a1:num->num`) THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN(MP_TAC o SPEC `1` o MATCH_MP KLE_IMP_POINTWISE) THEN
ASM_REWRITE_TAC[ARITH_RULE `1 <= n <=> ~(n = 0)`; ARITH] THEN ARITH_TAC;
ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `a2:num->num`
(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
DISCH_THEN(X_CHOOSE_THEN `k:num` STRIP_ASSUME_TAC) THEN
ABBREV_TAC `a3 = \j:num. if j = k then a1 j + 1 else a1 j` THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [FUN_EQ_THM]) THEN
REWRITE_TAC[] THEN DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
MATCH_MP_TAC HAS_SIZE_CARD THEN CONV_TAC HAS_SIZE_CONV THEN
MAP_EVERY EXISTS_TAC
[`s:(num->num)->bool`; `a3 INSERT (s DELETE (a0:num->num))`] THEN
SUBGOAL_THEN `~((a3:num->num) IN s)` ASSUME_TAC THENL
[DISCH_TAC THEN SUBGOAL_THEN `kle n a3 a1` MP_TAC THENL
[ASM_MESON_TAC[]; ALL_TAC] THEN
DISCH_THEN(MP_TAC o SPEC `k:num` o MATCH_MP KLE_IMP_POINTWISE) THEN
ASM_REWRITE_TAC[LE_REFL] THEN ARITH_TAC;
ALL_TAC] THEN
SUBGOAL_THEN `~(a3:num->num = a0) /\ ~(a3 = a1)` STRIP_ASSUME_TAC THENL
[ASM_MESON_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN `~(a2:num->num = a0)` ASSUME_TAC THENL
[ASM_REWRITE_TAC[FUN_EQ_THM] THEN MESON_TAC[ARITH_RULE `~(x + 1 = x)`];
ALL_TAC] THEN
CONJ_TAC THENL [MATCH_MP_TAC lemma_1 THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN `!x. x IN (s DELETE a0) ==> kle n a2 x` ASSUME_TAC THENL
[GEN_TAC THEN REWRITE_TAC[IN_DELETE] THEN STRIP_TAC THEN
SUBGOAL_THEN `kle n a2 x \/ kle n x a2` MP_TAC THENL
[ASM_MESON_TAC[ksimplex]; ALL_TAC] THEN
MATCH_MP_TAC(TAUT `(~b ==> ~a) ==> b \/ a ==> b`) THEN
DISCH_TAC THEN SUBGOAL_THEN `kle n a0 x` MP_TAC THENL
[ASM_MESON_TAC[]; ALL_TAC] THEN REPEAT STRIP_TAC THEN
SUBGOAL_THEN `(x:num->num = a0) \/ (x = a2)`
(fun th -> ASM_MESON_TAC[KLE_REFL; th]) THEN
MATCH_MP_TAC KLE_ADJACENT THEN
EXISTS_TAC `k:num` THEN ASM_REWRITE_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN `ksimplex p n (a3 INSERT (s DELETE a0))` ASSUME_TAC THENL
[MP_TAC(ASSUME `ksimplex p n s`) THEN REWRITE_TAC[ksimplex] THEN
MATCH_MP_TAC MONO_AND THEN CONJ_TAC THENL
[SIMP_TAC[HAS_SIZE; FINITE_INSERT; FINITE_DELETE; CARD_CLAUSES;
CARD_DELETE] THEN
ASM_REWRITE_TAC[IN_DELETE] THEN STRIP_TAC THEN ARITH_TAC;
ALL_TAC] THEN
MATCH_MP_TAC MONO_AND THEN CONJ_TAC THENL
[DISCH_TAC THEN REWRITE_TAC[IN_INSERT; IN_DELETE] THEN
SUBGOAL_THEN `!j. (a3:num->num) j <= p`
(fun th -> ASM_MESON_TAC[th]) THEN
X_GEN_TAC `j:num` THEN ONCE_ASM_REWRITE_TAC[] THEN COND_CASES_TAC THENL
[ALL_TAC; ASM_MESON_TAC[]] THEN
FIRST_X_ASSUM SUBST_ALL_TAC THEN
UNDISCH_TAC
`~(?j. 1 <= j /\ j <= n /\
(!x. x IN s DELETE a0 ==> (x j = (p:num))))` THEN
REWRITE_TAC[NOT_EXISTS_THM] THEN DISCH_THEN(MP_TAC o SPEC `k:num`) THEN
REWRITE_TAC[ASSUME `1 <= k`; ASSUME `k:num <= n`; NOT_FORALL_THM] THEN
DISCH_THEN(X_CHOOSE_THEN `a4:num->num` MP_TAC) THEN
REWRITE_TAC[IN_DELETE; NOT_IMP] THEN STRIP_TAC THEN
UNDISCH_TAC `!x. x IN s DELETE a0 ==> kle n a2 x` THEN
DISCH_THEN(MP_TAC o SPEC `a4:num->num`) THEN
ASM_REWRITE_TAC[IN_DELETE] THEN
DISCH_THEN(MP_TAC o MATCH_MP KLE_IMP_POINTWISE) THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o SPEC `k:num`) THEN
ASM_REWRITE_TAC[] THEN
UNDISCH_TAC `~((a4:num->num) k = p)` THEN
SUBGOAL_THEN `(a4:num->num) k <= p` MP_TAC THENL
[ASM_MESON_TAC[ksimplex]; ARITH_TAC];
ALL_TAC] THEN
MATCH_MP_TAC MONO_AND THEN CONJ_TAC THENL
[REWRITE_TAC[IN_INSERT; IN_DELETE] THEN REPEAT STRIP_TAC THENL
[ALL_TAC; ASM_MESON_TAC[]] THEN
FIRST_X_ASSUM SUBST_ALL_TAC THEN
ONCE_ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[];
ALL_TAC] THEN
DISCH_TAC THEN REWRITE_TAC[IN_INSERT; IN_DELETE] THEN
SUBGOAL_THEN `!x. x IN s /\ ~(x = a0) ==> kle n x a3`
(fun th -> ASM_MESON_TAC[th; KLE_REFL]) THEN
X_GEN_TAC `x:num->num` THEN STRIP_TAC THEN
SUBGOAL_THEN `kle n a2 x /\ kle n x a1` MP_TAC THENL
[ASM_MESON_TAC[IN_DELETE]; ALL_TAC] THEN
REWRITE_TAC[IMP_CONJ] THEN
DISCH_THEN(MP_TAC o SPEC `k:num` o MATCH_MP KLE_IMP_POINTWISE) THEN
DISCH_TAC THEN REWRITE_TAC[kle] THEN
DISCH_THEN(X_CHOOSE_THEN `kk:num->bool` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `(k:num) INSERT kk` THEN
REWRITE_TAC[INSERT_SUBSET; IN_NUMSEG] THEN
CONJ_TAC THENL [ASM_REWRITE_TAC[]; ALL_TAC] THEN
X_GEN_TAC `j:num` THEN
FIRST_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [th]) THEN
REWRITE_TAC[IN_INSERT] THEN ASM_CASES_TAC `j:num = k` THENL
[ALL_TAC; ASM_MESON_TAC[]] THEN
FIRST_X_ASSUM SUBST_ALL_TAC THEN REWRITE_TAC[] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (ARITH_RULE
`a2 <= x ==> !a0. x <= a1 /\ (a1 = a0 + 1) /\ (a2 = a0 + 1)
==> (a1 + 1 = x + 1)`)) THEN
EXISTS_TAC `(a0:num->num) k` THEN
ASM_MESON_TAC[KLE_IMP_POINTWISE];
ALL_TAC] THEN
GEN_REWRITE_TAC I [EXTENSION] THEN
REWRITE_TAC[IN_ELIM_THM; IN_INSERT; NOT_IN_EMPTY] THEN
X_GEN_TAC `s':(num->num)->bool` THEN EQ_TAC THENL
[ALL_TAC;
DISCH_THEN(DISJ_CASES_THEN SUBST_ALL_TAC) THENL
[ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]; ALL_TAC] THEN
ASM_REWRITE_TAC[] THEN EXISTS_TAC `a3:num->num` THEN
REWRITE_TAC[IN_INSERT; DELETE_INSERT] THEN
UNDISCH_TAC `~((a3:num->num) IN s)` THEN SET_TAC[]] THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
DISCH_THEN(X_CHOOSE_THEN `a':num->num` STRIP_ASSUME_TAC) THEN
MP_TAC(SPECL [`p:num`; `n:num`; `s':(num->num)->bool`]
KSIMPLEX_EXTREMA_STRONG) THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `a_min:num->num` (X_CHOOSE_THEN `a_max:num->num`
STRIP_ASSUME_TAC)) THEN
SUBGOAL_THEN `(a':num->num = a_min) \/ (a' = a_max)` MP_TAC THENL
[MATCH_MP_TAC KSIMPLEX_FIX_PLANE THEN MAP_EVERY EXISTS_TAC
[`p:num`; `(a2:num->num) k`; `n:num`;
`k:num`; `s':(num->num)->bool`] THEN
REPEAT CONJ_TAC THEN TRY(FIRST_ASSUM MATCH_ACCEPT_TAC) THEN
X_GEN_TAC `x:num->num` THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
SUBGOAL_THEN `kle n a2 x /\ kle n x a1` MP_TAC THENL
[ASM_MESON_TAC[IN_DELETE]; ALL_TAC] THEN
DISCH_THEN(CONJUNCTS_THEN (MP_TAC o SPEC `k:num` o MATCH_MP
KLE_IMP_POINTWISE)) THEN
ASM_REWRITE_TAC[] THEN ARITH_TAC;
ALL_TAC] THEN
DISCH_THEN(DISJ_CASES_THEN SUBST_ALL_TAC) THENL
[DISJ1_TAC THEN MATCH_MP_TAC lemma THEN
MAP_EVERY EXISTS_TAC [`a0:num->num`; `a_min:num->num`] THEN
ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `a_max:num->num = a1` MP_TAC THENL
[SUBGOAL_THEN `a1:num->num IN (s' DELETE a_min) /\
a_max:num->num IN (s DELETE a0)`
MP_TAC THENL
[ASM_MESON_TAC[IN_DELETE]; ASM_MESON_TAC[KLE_ANTISYM; IN_DELETE]];
ALL_TAC] THEN
ASM_REWRITE_TAC[FUN_EQ_THM] THEN MATCH_MP_TAC MONO_FORALL THEN
MESON_TAC[EQ_ADD_RCANCEL];
DISJ2_TAC THEN MATCH_MP_TAC lemma THEN
MAP_EVERY EXISTS_TAC [`a3:num->num`; `a_max:num->num`] THEN
ASM_REWRITE_TAC[IN_INSERT] THEN CONJ_TAC THENL
[UNDISCH_TAC `~(a3:num->num IN s)` THEN SET_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN `a_min:num->num = a2` MP_TAC THENL
[SUBGOAL_THEN `a2:num->num IN (s' DELETE a_max) /\
a_min:num->num IN (s DELETE a0)`
MP_TAC THENL
[ASM_MESON_TAC[IN_DELETE]; ASM_MESON_TAC[KLE_ANTISYM; IN_DELETE]];
ALL_TAC] THEN
ASM_REWRITE_TAC[FUN_EQ_THM] THEN MATCH_MP_TAC MONO_FORALL THEN
MESON_TAC[EQ_ADD_RCANCEL]];
ALL_TAC] THEN
ASM_CASES_TAC `a:num->num = a1` THENL
[FIRST_X_ASSUM SUBST_ALL_TAC THEN
MP_TAC(SPECL [`a1:num->num`; `p:num`; `n:num`; `s:(num->num)->bool`]
KSIMPLEX_PREDECESSOR) THEN
ANTS_TAC THENL [ASM_REWRITE_TAC[]; ALL_TAC] THEN
MATCH_MP_TAC(TAUT `~a /\ (b ==> c) ==> a \/ b ==> c`) THEN CONJ_TAC THENL
[DISCH_THEN(MP_TAC o SPEC `a0:num->num`) THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN(MP_TAC o SPEC `1` o MATCH_MP KLE_IMP_POINTWISE) THEN
ASM_REWRITE_TAC[ARITH_RULE `1 <= n <=> ~(n = 0)`; ARITH] THEN ARITH_TAC;
ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `a2:num->num`
(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
DISCH_THEN(X_CHOOSE_THEN `k:num` STRIP_ASSUME_TAC) THEN
SUBGOAL_THEN `!x. x IN (s DELETE a1) ==> kle n x a2` ASSUME_TAC THENL
[GEN_TAC THEN REWRITE_TAC[IN_DELETE] THEN STRIP_TAC THEN
SUBGOAL_THEN `kle n a2 x \/ kle n x a2` MP_TAC THENL
[ASM_MESON_TAC[ksimplex]; ALL_TAC] THEN
MATCH_MP_TAC(TAUT `(~b ==> ~a) ==> a \/ b ==> b`) THEN
DISCH_TAC THEN SUBGOAL_THEN `kle n x a1` MP_TAC THENL
[ASM_MESON_TAC[]; ALL_TAC] THEN REPEAT STRIP_TAC THEN
SUBGOAL_THEN `(x:num->num = a2) \/ (x = a1)`
(fun th -> ASM_MESON_TAC[KLE_REFL; th]) THEN
MATCH_MP_TAC KLE_ADJACENT THEN EXISTS_TAC `k:num` THEN
REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_ACCEPT_TAC;
ALL_TAC] THEN
SUBGOAL_THEN `~(a2:num->num = a1)` ASSUME_TAC THENL
[REWRITE_TAC[FUN_EQ_THM] THEN ASM_MESON_TAC[ARITH_RULE `~(x + 1 = x)`];
ALL_TAC] THEN
ABBREV_TAC `a3 = \j:num. if j = k then a0 j - 1 else a0 j` THEN
SUBGOAL_THEN `!j:num. a0(j) = if j = k then a3(j) + 1 else a3 j`
ASSUME_TAC THENL
[X_GEN_TAC `j:num` THEN EXPAND_TAC "a3" THEN REWRITE_TAC[] THEN
COND_CASES_TAC THEN
REWRITE_TAC[ARITH_RULE `(a = a - 1 + 1) <=> ~(a = 0)`] THEN
FIRST_X_ASSUM SUBST_ALL_TAC THEN DISCH_TAC THEN
UNDISCH_TAC `!j:num. a1 j = (if j = k then a2 j + 1 else a2 j)` THEN
DISCH_THEN(MP_TAC o SPEC `k:num`) THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[ARITH_RULE `(0 + 1 = x + 1) <=> (x = 0)`] THEN DISCH_TAC THEN
UNDISCH_TAC
`~(?j. 1 <= j /\ j <= n /\ (!x. x IN s DELETE a1 ==> (x j = 0)))` THEN
REWRITE_TAC[NOT_EXISTS_THM] THEN EXISTS_TAC `k:num` THEN
ASM_MESON_TAC[KLE_IMP_POINTWISE; LE];
ALL_TAC] THEN
SUBGOAL_THEN `~(kle n a0 a3)` ASSUME_TAC THENL
[ASM_MESON_TAC[KLE_IMP_POINTWISE; ARITH_RULE `~(a + 1 <= a)`];
ALL_TAC] THEN
SUBGOAL_THEN `~(a3:num->num IN s)` ASSUME_TAC THENL
[ASM_MESON_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN `kle n a3 a2` ASSUME_TAC THENL
[SUBGOAL_THEN `kle n a0 a1` MP_TAC THENL
[ASM_MESON_TAC[]; ALL_TAC] THEN
REWRITE_TAC[kle] THEN MATCH_MP_TAC MONO_EXISTS THEN
GEN_TAC THEN MATCH_MP_TAC MONO_AND THEN REWRITE_TAC[] THEN
MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN
ONCE_REWRITE_TAC[
ASSUME `!j:num. a0 j = (if j = k then a3 j + 1 else a3 j)`;
ASSUME `!j:num. a1 j = (if j = k then a2 j + 1 else a2 j)`] THEN
REPEAT(COND_CASES_TAC THEN REWRITE_TAC[]) THEN ARITH_TAC;
ALL_TAC] THEN
SUBGOAL_THEN `kle n a3 a0` ASSUME_TAC THENL
[REWRITE_TAC[kle] THEN EXISTS_TAC `{k:num}` THEN
ASM_REWRITE_TAC[SUBSET; IN_SING; IN_NUMSEG] THEN
ASM_MESON_TAC[ADD_CLAUSES];
ALL_TAC] THEN
MATCH_MP_TAC HAS_SIZE_CARD THEN CONV_TAC HAS_SIZE_CONV THEN
MAP_EVERY EXISTS_TAC
[`s:(num->num)->bool`; `a3 INSERT (s DELETE (a1:num->num))`] THEN
SUBGOAL_THEN `~(a3:num->num = a1) /\ ~(a3 = a0)` STRIP_ASSUME_TAC THENL
[ASM_MESON_TAC[]; ALL_TAC] THEN
CONJ_TAC THENL [MATCH_MP_TAC lemma_1 THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN `ksimplex p n (a3 INSERT (s DELETE a1))` ASSUME_TAC THENL
[MP_TAC(ASSUME `ksimplex p n s`) THEN REWRITE_TAC[ksimplex] THEN
MATCH_MP_TAC MONO_AND THEN CONJ_TAC THENL
[SIMP_TAC[HAS_SIZE; FINITE_INSERT; FINITE_DELETE; CARD_CLAUSES;
CARD_DELETE] THEN
ASM_REWRITE_TAC[IN_DELETE] THEN STRIP_TAC THEN ARITH_TAC;
ALL_TAC] THEN
MATCH_MP_TAC MONO_AND THEN CONJ_TAC THENL
[DISCH_TAC THEN REWRITE_TAC[IN_INSERT; IN_DELETE] THEN
SUBGOAL_THEN `!j. (a3:num->num) j <= p`
(fun th -> ASM_MESON_TAC[th]) THEN
X_GEN_TAC `j:num` THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`a0:num->num`; `j:num`]) THEN
ASM_REWRITE_TAC[] THEN COND_CASES_TAC THEN ARITH_TAC;
ALL_TAC] THEN
MATCH_MP_TAC MONO_AND THEN CONJ_TAC THENL
[REWRITE_TAC[IN_INSERT; IN_DELETE] THEN REPEAT STRIP_TAC THENL
[ALL_TAC; ASM_MESON_TAC[]] THEN
FIRST_X_ASSUM SUBST_ALL_TAC THEN
EXPAND_TAC "a3" THEN REWRITE_TAC[] THEN ASM_MESON_TAC[];
ALL_TAC] THEN
DISCH_TAC THEN REWRITE_TAC[IN_INSERT; IN_DELETE] THEN
SUBGOAL_THEN `!x. x IN s /\ ~(x = a1) ==> kle n a3 x`
(fun th -> ASM_MESON_TAC[th; KLE_REFL]) THEN
X_GEN_TAC `x:num->num` THEN STRIP_TAC THEN
MATCH_MP_TAC KLE_BETWEEN_L THEN
MAP_EVERY EXISTS_TAC [`a0:num->num`; `a2:num->num`] THEN
ASM_MESON_TAC[IN_DELETE];
ALL_TAC] THEN
GEN_REWRITE_TAC I [EXTENSION] THEN
REWRITE_TAC[IN_ELIM_THM; IN_INSERT; NOT_IN_EMPTY] THEN
X_GEN_TAC `s':(num->num)->bool` THEN EQ_TAC THENL
[ALL_TAC;
DISCH_THEN(DISJ_CASES_THEN SUBST_ALL_TAC) THENL
[ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]; ALL_TAC] THEN
ASM_REWRITE_TAC[] THEN EXISTS_TAC `a3:num->num` THEN
REWRITE_TAC[IN_INSERT; DELETE_INSERT] THEN
UNDISCH_TAC `~((a3:num->num) IN s)` THEN SET_TAC[]] THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
DISCH_THEN(X_CHOOSE_THEN `a':num->num` STRIP_ASSUME_TAC) THEN
MP_TAC(SPECL [`p:num`; `n:num`; `s':(num->num)->bool`]
KSIMPLEX_EXTREMA_STRONG) THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `a_min:num->num` (X_CHOOSE_THEN `a_max:num->num`
STRIP_ASSUME_TAC)) THEN
SUBGOAL_THEN `(a':num->num = a_min) \/ (a' = a_max)` MP_TAC THENL
[MATCH_MP_TAC KSIMPLEX_FIX_PLANE THEN MAP_EVERY EXISTS_TAC
[`p:num`; `(a2:num->num) k`; `n:num`;
`k:num`; `s':(num->num)->bool`] THEN
REPEAT CONJ_TAC THEN TRY(FIRST_ASSUM MATCH_ACCEPT_TAC) THEN
X_GEN_TAC `x:num->num` THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
SUBGOAL_THEN `kle n a0 x /\ kle n x a2` MP_TAC THENL
[ASM_MESON_TAC[IN_DELETE]; ALL_TAC] THEN
DISCH_THEN(CONJUNCTS_THEN (MP_TAC o SPEC `k:num` o MATCH_MP
KLE_IMP_POINTWISE)) THEN
SUBGOAL_THEN `(a2:num->num) k <= a0 k`
(fun th -> MP_TAC th THEN ARITH_TAC) THEN
UNDISCH_TAC `!j:num. a1 j = (if j = k then a2 j + 1 else a2 j)` THEN
DISCH_THEN(MP_TAC o SPEC `k:num`) THEN ASM_REWRITE_TAC[] THEN ARITH_TAC;
ALL_TAC] THEN
DISCH_THEN(DISJ_CASES_THEN SUBST_ALL_TAC) THENL
[DISJ2_TAC THEN MATCH_MP_TAC lemma THEN
MAP_EVERY EXISTS_TAC [`a3:num->num`; `a_min:num->num`] THEN
ASM_REWRITE_TAC[IN_INSERT] THEN CONJ_TAC THENL
[UNDISCH_TAC `~(a3:num->num IN s)` THEN SET_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN `a_max:num->num = a2` MP_TAC THENL
[SUBGOAL_THEN `a2:num->num IN (s' DELETE a_min) /\
a_max:num->num IN (s DELETE a1)`
MP_TAC THENL
[ASM_MESON_TAC[IN_DELETE]; ASM_MESON_TAC[KLE_ANTISYM; IN_DELETE]];
ALL_TAC] THEN
SUBGOAL_THEN
`!j. a2 j = if 1 <= j /\ j <= n then a3 j + 1 else a3 j`
(fun th -> ASM_REWRITE_TAC[th; FUN_EQ_THM])
THENL
[ALL_TAC;
MATCH_MP_TAC MONO_FORALL THEN MESON_TAC[EQ_ADD_RCANCEL]] THEN
UNDISCH_TAC `!j:num. a1 j = (if j = k then a2 j + 1 else a2 j)` THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MONO_FORALL THEN
MESON_TAC[EQ_ADD_RCANCEL];
DISJ1_TAC THEN MATCH_MP_TAC lemma THEN
MAP_EVERY EXISTS_TAC [`a1:num->num`; `a_max:num->num`] THEN
REPEAT CONJ_TAC THEN TRY(FIRST_ASSUM ACCEPT_TAC) THEN
SUBGOAL_THEN `a_min:num->num = a0` MP_TAC THENL
[SUBGOAL_THEN `a0:num->num IN (s' DELETE a_max) /\
a_min:num->num IN (s DELETE a1)`
MP_TAC THENL
[ASM_MESON_TAC[IN_DELETE]; ASM_MESON_TAC[KLE_ANTISYM; IN_DELETE]];
ALL_TAC] THEN
UNDISCH_THEN `!j:num. a1 j = (if j = k then a2 j + 1 else a2 j)`
(K ALL_TAC) THEN
ASM_REWRITE_TAC[FUN_EQ_THM] THEN MATCH_MP_TAC MONO_FORALL THEN
MESON_TAC[EQ_ADD_RCANCEL]];
ALL_TAC] THEN
MP_TAC(SPECL [`a:num->num`; `p:num`; `n:num`; `s:(num->num)->bool`]
KSIMPLEX_PREDECESSOR) THEN ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC(TAUT `~a /\ (b ==> c) ==> a \/ b ==> c`) THEN CONJ_TAC THENL
[ASM_MESON_TAC[KLE_ANTISYM]; ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `u:num->num`
(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
DISCH_THEN(X_CHOOSE_THEN `k:num` STRIP_ASSUME_TAC) THEN
MP_TAC(SPECL [`a:num->num`; `p:num`; `n:num`; `s:(num->num)->bool`]
KSIMPLEX_SUCCESSOR) THEN
REWRITE_TAC[ASSUME `ksimplex p n s`; ASSUME `a:num->num IN s`] THEN
MATCH_MP_TAC(TAUT `~a /\ (b ==> c) ==> a \/ b ==> c`) THEN CONJ_TAC THENL
[ASM_MESON_TAC[KLE_ANTISYM]; ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `v:num->num`
(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
DISCH_THEN(X_CHOOSE_THEN `l:num` STRIP_ASSUME_TAC) THEN
ABBREV_TAC `a' = \j:num. if j = l then u(j) + 1 else u(j)` THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [FUN_EQ_THM]) THEN
REWRITE_TAC[] THEN DISCH_THEN(ASSUME_TAC o GSYM) THEN
SUBGOAL_THEN `~(k:num = l)` ASSUME_TAC THENL
[DISCH_TAC THEN
UNDISCH_TAC `!j:num. v j = (if j = l then a j + 1 else a j)` THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o SPEC `l:num`) THEN
REWRITE_TAC[] THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [ksimplex]) THEN
DISCH_THEN(MP_TAC o last o CONJUNCTS) THEN
DISCH_THEN(MP_TAC o SPECL [`u:num->num`; `v:num->num`]) THEN
ASM_REWRITE_TAC[] THEN
ASM_REWRITE_TAC[kle] THEN
DISCH_THEN(DISJ_CASES_THEN (CHOOSE_THEN (MP_TAC o SPEC `l:num` o
CONJUNCT2))) THEN
ASM_REWRITE_TAC[] THEN COND_CASES_TAC THEN ARITH_TAC;
ALL_TAC] THEN
SUBGOAL_THEN `~(a':num->num = a)` ASSUME_TAC THENL
[ASM_REWRITE_TAC[FUN_EQ_THM] THEN DISCH_THEN(MP_TAC o SPEC `k:num`) THEN
ASM_REWRITE_TAC[] THEN ARITH_TAC;
ALL_TAC] THEN
SUBGOAL_THEN `~((a':num->num) IN s)` ASSUME_TAC THENL
[DISCH_TAC THEN FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [ksimplex]) THEN
DISCH_THEN(MP_TAC o SPECL [`a:num->num`; `a':num->num`] o
last o CONJUNCTS) THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN(DISJ_CASES_THEN (MP_TAC o MATCH_MP KLE_IMP_POINTWISE)) THENL
[DISCH_THEN(MP_TAC o SPEC `k:num`) THEN ASM_REWRITE_TAC[] THEN ARITH_TAC;
DISCH_THEN(MP_TAC o SPEC `l:num`) THEN ASM_REWRITE_TAC[] THEN
ARITH_TAC];
ALL_TAC] THEN
SUBGOAL_THEN
`kle n u a /\ kle n u a' /\ kle n a v /\ kle n a' v`
STRIP_ASSUME_TAC THENL
[REWRITE_TAC[kle] THEN REPEAT CONJ_TAC THENL
[EXISTS_TAC `{k:num}`;
EXISTS_TAC `{l:num}`;
EXISTS_TAC `{l:num}`;
EXISTS_TAC `{k:num}`] THEN
ASM_REWRITE_TAC[IN_SING; SUBSET; IN_NUMSEG] THEN
ASM_MESON_TAC[ADD_CLAUSES];
ALL_TAC] THEN
SUBGOAL_THEN `!x. kle n u x /\ kle n x v
==> ((x = u) \/ (x = a) \/ (x = a') \/ (x = v))`
ASSUME_TAC THENL
[X_GEN_TAC `x:num->num` THEN
DISCH_THEN(CONJUNCTS_THEN (MP_TAC o MATCH_MP KLE_IMP_POINTWISE)) THEN
ASM_REWRITE_TAC[FUN_EQ_THM; IMP_IMP; AND_FORALL_THM] THEN
ONCE_REWRITE_TAC[COND_RAND] THEN
ASM_CASES_TAC `(x:num->num) k = u k` THEN
ASM_CASES_TAC `(x:num->num) l = u l` THENL
[DISCH_THEN(fun th -> DISJ1_TAC THEN MP_TAC th);
DISCH_THEN(fun th -> DISJ2_TAC THEN DISJ2_TAC THEN DISJ1_TAC THEN
MP_TAC th);
DISCH_THEN(fun th -> DISJ2_TAC THEN DISJ1_TAC THEN MP_TAC th);
DISCH_THEN(fun th -> REPEAT DISJ2_TAC THEN MP_TAC th)] THEN
MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `j:num` THEN
REPEAT(COND_CASES_TAC THEN
ASM_REWRITE_TAC[LE_ANTISYM;
ARITH_RULE `x <= u + 1 /\ u <= x <=> (x = u) \/ (x = u + 1)`]);
ALL_TAC] THEN
SUBGOAL_THEN `kle n u v` ASSUME_TAC THENL
[ASM_MESON_TAC[KLE_TRANS; ksimplex]; ALL_TAC] THEN
SUBGOAL_THEN `ksimplex p n (a' INSERT (s DELETE a))` ASSUME_TAC THENL
[MP_TAC(ASSUME `ksimplex p n s`) THEN REWRITE_TAC[ksimplex] THEN
MATCH_MP_TAC MONO_AND THEN CONJ_TAC THENL
[SIMP_TAC[HAS_SIZE; FINITE_INSERT; FINITE_DELETE; CARD_CLAUSES;
CARD_DELETE; IN_DELETE] THEN
ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ARITH_TAC;
ALL_TAC] THEN
MATCH_MP_TAC MONO_AND THEN CONJ_TAC THENL
[REWRITE_TAC[IN_INSERT; IN_DELETE] THEN
SIMP_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
REWRITE_TAC[RIGHT_FORALL_IMP_THM; LEFT_FORALL_IMP_THM; EXISTS_REFL] THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(fun th -> X_GEN_TAC `j:num` THEN MP_TAC th) THEN
COND_CASES_TAC THEN ASM_SIMP_TAC[] THEN
DISCH_THEN(MP_TAC o SPEC `v:num->num`) THEN ASM_REWRITE_TAC[] THEN
DISCH_THEN(MP_TAC o SPEC `l:num`) THEN ASM_REWRITE_TAC[];
ALL_TAC] THEN
MATCH_MP_TAC MONO_AND THEN CONJ_TAC THENL
[REWRITE_TAC[IN_INSERT; IN_DELETE] THEN
REWRITE_TAC[TAUT `(a \/ b) /\ c <=> a /\ c \/ b /\ c`] THEN
SIMP_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
REWRITE_TAC[EXISTS_REFL; LEFT_FORALL_IMP_THM] THEN
ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[];
ALL_TAC] THEN
REWRITE_TAC[IN_INSERT; IN_DELETE] THEN
SUBGOAL_THEN
`!x. x IN s /\ kle n v x ==> kle n a' x`
ASSUME_TAC THENL
[X_GEN_TAC `x:num->num` THEN STRIP_TAC THEN
MATCH_MP_TAC KLE_BETWEEN_R THEN
MAP_EVERY EXISTS_TAC [`u:num->num`; `v:num->num`] THEN
ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[ksimplex; KLE_TRANS];
ALL_TAC] THEN
SUBGOAL_THEN
`!x. x IN s /\ kle n x u ==> kle n x a'`
ASSUME_TAC THENL
[X_GEN_TAC `x:num->num` THEN STRIP_TAC THEN
MATCH_MP_TAC KLE_BETWEEN_L THEN
MAP_EVERY EXISTS_TAC [`u:num->num`; `v:num->num`] THEN
ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[ksimplex; KLE_TRANS];
ALL_TAC] THEN
SUBGOAL_THEN
`!x. x IN s /\ ~(x = a) ==> kle n a' x \/ kle n x a'`
(fun th -> MESON_TAC[th; KLE_REFL; ASSUME `(a:num->num) IN s`]) THEN
X_GEN_TAC `x:num->num` THEN STRIP_TAC THEN
ASM_CASES_TAC `kle n v x` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
ASM_CASES_TAC `kle n x u` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
SUBGOAL_THEN `(x:num->num = u) \/ (x = a) \/ (x = a') \/ (x = v)`
(fun th -> ASM_MESON_TAC[th; KLE_REFL]) THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[ksimplex];
ALL_TAC] THEN
MATCH_MP_TAC HAS_SIZE_CARD THEN CONV_TAC HAS_SIZE_CONV THEN
MAP_EVERY EXISTS_TAC
[`s:(num->num)->bool`; `a' INSERT (s DELETE (a:num->num))`] THEN
CONJ_TAC THENL
[REWRITE_TAC[EXTENSION; IN_DELETE; IN_INSERT] THEN ASM_MESON_TAC[];
ALL_TAC] THEN
GEN_REWRITE_TAC I [EXTENSION] THEN REWRITE_TAC[IN_ELIM_THM] THEN
X_GEN_TAC `s':(num->num)->bool` THEN
REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN EQ_TAC THENL
[ALL_TAC;
DISCH_THEN(DISJ_CASES_THEN SUBST1_TAC) THENL
[ASM_MESON_TAC[]; ALL_TAC] THEN
ASM_REWRITE_TAC[] THEN EXISTS_TAC `a':num->num` THEN
REWRITE_TAC[EXTENSION; IN_INSERT; IN_DELETE] THEN ASM_MESON_TAC[]] THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
DISCH_THEN(X_CHOOSE_THEN `a'':num->num` STRIP_ASSUME_TAC) THEN
SUBGOAL_THEN `(a:num->num) IN s' \/ a' IN s'` MP_TAC THENL
[ALL_TAC;
MATCH_MP_TAC MONO_OR THEN CONJ_TAC THEN DISCH_TAC THEN
MP_TAC(ASSUME `s' DELETE a'' = s DELETE (a:num->num)`) THEN
REWRITE_TAC[EXTENSION] THEN
DISCH_THEN(fun th -> MP_TAC th THEN MP_TAC th) THENL
[DISCH_THEN(MP_TAC o SPEC `a:num->num`);
DISCH_THEN(MP_TAC o SPEC `a':num->num`)] THEN
REWRITE_TAC[IN_DELETE] THEN ASM_REWRITE_TAC[IN_INSERT; IN_DELETE] THEN
DISCH_THEN(SUBST_ALL_TAC o SYM) THEN ASM_MESON_TAC[]] THEN
SUBGOAL_THEN `~(u:num->num = v)` ASSUME_TAC THENL
[ASM_REWRITE_TAC[FUN_EQ_THM] THEN DISCH_THEN(MP_TAC o SPEC `l:num`) THEN
ASM_REWRITE_TAC[] THEN ARITH_TAC;
ALL_TAC] THEN
SUBGOAL_THEN `~(kle n v u)` ASSUME_TAC THENL
[ASM_MESON_TAC[KLE_ANTISYM]; ALL_TAC] THEN
SUBGOAL_THEN `~(u:num->num = a)` ASSUME_TAC THENL
[ASM_REWRITE_TAC[FUN_EQ_THM] THEN DISCH_THEN(MP_TAC o SPEC `k:num`) THEN
ASM_REWRITE_TAC[] THEN ARITH_TAC;
ALL_TAC] THEN
SUBGOAL_THEN `~(v:num->num = a)` ASSUME_TAC THENL
[ASM_REWRITE_TAC[FUN_EQ_THM] THEN DISCH_THEN(MP_TAC o SPEC `l:num`) THEN
ASM_REWRITE_TAC[] THEN ARITH_TAC;
ALL_TAC] THEN
SUBGOAL_THEN `u:num->num IN s' /\ v IN s'` STRIP_ASSUME_TAC THENL
[ASM_MESON_TAC[EXTENSION; IN_DELETE]; ALL_TAC] THEN
ASM_CASES_TAC
`!x. x IN s' ==> kle n x u \/ kle n v x`
THENL
[ALL_TAC;
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_FORALL_THM]) THEN
DISCH_THEN(X_CHOOSE_THEN `w:num->num` MP_TAC) THEN
REWRITE_TAC[NOT_IMP; DE_MORGAN_THM] THEN STRIP_TAC THEN
SUBGOAL_THEN `(w:num->num = u) \/ (w = a) \/ (w = a') \/ (w = v)`
(fun th -> ASM_MESON_TAC[KLE_REFL; th]) THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[ksimplex]] THEN
MP_TAC(SPECL [`u:num->num`; `p:num`; `n:num`; `s':(num->num)->bool`]
KSIMPLEX_SUCCESSOR) THEN
ANTS_TAC THENL [ASM_MESON_TAC[EXTENSION; IN_DELETE]; ALL_TAC] THEN
DISCH_THEN(DISJ_CASES_THEN2 (MP_TAC o SPEC `v:num->num`) MP_TAC) THENL
[ASM_MESON_TAC[EXTENSION; IN_DELETE]; ALL_TAC] THEN
ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN DISCH_THEN(K ALL_TAC) THEN
UNDISCH_TAC `!x. x IN s' ==> kle n x u \/ kle n v x` THEN
REWRITE_TAC[NOT_EXISTS_THM] THEN MATCH_MP_TAC MONO_FORALL THEN
X_GEN_TAC `w:num->num` THEN
DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(DISJ_CASES_THEN(MP_TAC o MATCH_MP KLE_IMP_POINTWISE)) THEN
ASM_REWRITE_TAC[] THENL
[MESON_TAC[ARITH_RULE `~(i + 1 <= i)`]; ALL_TAC] THEN
DISCH_THEN(fun th -> MP_TAC(SPEC `k:num` th) THEN
MP_TAC(SPEC `l:num` th)) THEN
ASM_REWRITE_TAC[] THEN
REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN TRY ARITH_TAC THEN
UNDISCH_TAC `~(k:num = l)` THEN ASM_REWRITE_TAC[]);;
let KUHN_SIMPLEX_LEMMA = prove
(`!p n. (!s. ksimplex p (n + 1) s ==> (
IMAGE rl s
SUBSET 0..n+1)) /\
ODD(
CARD{f | (?s a. ksimplex p (n + 1) s /\
a
IN s /\
(f = s
DELETE a)) /\
(
IMAGE rl f = 0 .. n) /\
((?j. 1 <= j /\ j <= n + 1 /\
!x. x
IN f ==> (x j = 0)) \/
(?j. 1 <= j /\ j <= n + 1 /\
!x. x
IN f ==> (x j = p)))})
==>
ODD(
CARD {s | s
IN {s | ksimplex p (n + 1) s} /\
(
IMAGE rl s = 0..n+1)})`,
let reduced = new_definition
`reduced label n (x:num->num) =
@k. k <= n /\
(!i. 1 <= i /\ i < k + 1 ==> (label x i = 0)) /\
((k = n) \/ ~(label x (k + 1) = 0))`;;let REDUCED_LABELLING = prove
(`!label x n.
reduced label n x <= n /\
(!i. 1 <= i /\ i < reduced label n x + 1 ==> (label x i = 0)) /\
((reduced label n x = n) \/ ~(label x (reduced label n x + 1) = 0))`,
REPEAT GEN_TAC THEN REWRITE_TAC[reduced] THEN CONV_TAC SELECT_CONV THEN
MP_TAC(SPEC `\j. j <= n /\ ~(label (x:num->num) (j + 1) = 0) \/ (n = j)`
num_WOP) THEN
REWRITE_TAC[] THEN
MATCH_MP_TAC(TAUT `a /\ (b ==> c) ==> (a <=> b) ==> c`) THEN
CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `k:num` THEN
ASM_CASES_TAC `k = n:num` THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
ASM_REWRITE_TAC[
LE_REFL] THEN X_GEN_TAC `i:num` THEN STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `i - 1`) THEN
SIMP_TAC[
LT_IMP_LE] THEN
ASM_SIMP_TAC[ARITH_RULE `1 <= i /\ i < n + 1 ==> i - 1 < n`] THEN
ASM_SIMP_TAC[ARITH_RULE `1 <= i /\ i < n + 1 ==> ~(n = i - 1)`] THEN
ASM_SIMP_TAC[
SUB_ADD] THEN POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
ARITH_TAC);;
let REDUCED_LABELLING_UNIQUE = prove
(`!label x n.
r <= n /\
(!i. 1 <= i /\ i < r + 1 ==> (label x i = 0)) /\
((r = n) \/ ~(label x (r + 1) = 0))
==> (reduced label n x = r)`,
REPEAT GEN_TAC THEN DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC(SPECL
[`label:(num->num)->(num->num)`; `x:num->num`; `n:num`]
REDUCED_LABELLING) THEN
MATCH_MP_TAC(ARITH_RULE `~(a < b) /\ ~(b < a:num) ==> (a = b)`) THEN
ASM_MESON_TAC[ARITH_RULE `s < r:num /\ r <= n ==> ~(s = n)`;
ARITH_RULE `s < r ==> 1 <= s + 1 /\ s + 1 < r + 1`]);;
let REDUCED_LABELLING_0 = prove
(`!label n x j.
1 <= j /\ j <= n /\ (label x j = 0)
==> ~(reduced label n x = j - 1)`,
REPEAT STRIP_TAC THEN
MP_TAC(SPECL [`label:(num->num)->num->num`; `x:num->num`; `n:num`]
REDUCED_LABELLING) THEN
ASM_SIMP_TAC[
SUB_ADD; ARITH_RULE `1 <= j /\ j <= n ==> ~(j - 1 = n)`]);;
let REDUCED_LABELLING_1 = prove
(`!label n x j.
1 <= j /\ j <= n /\ ~(label x j = 0)
==> reduced label n x < j`,
REWRITE_TAC[GSYM
NOT_LE] THEN REPEAT STRIP_TAC THEN
MP_TAC(SPECL [`label:(num->num)->num->num`; `x:num->num`; `n:num`]
REDUCED_LABELLING) THEN
DISCH_THEN(MP_TAC o SPEC `j:num` o CONJUNCT1 o CONJUNCT2) THEN
ASM_REWRITE_TAC[ARITH_RULE `y < x + 1 <=> (y <= x)`]);;
let COMPLETE_FACE_TOP = prove
(`!lab f n.
(!x j. x
IN f /\ 1 <= j /\ j <= n + 1 /\ (x j = 0)
==> (lab x j = 0)) /\
(!x j. x
IN f /\ 1 <= j /\ j <= n + 1 /\ (x j = p)
==> (lab x j = 1))
==> ((
IMAGE (reduced lab (n + 1)) f = 0..n) /\
((?j. 1 <= j /\ j <= n + 1 /\ !x. x
IN f ==> (x j = 0)) \/
(?j. 1 <= j /\ j <= n + 1 /\ !x. x
IN f ==> (x j = p))) <=>
(
IMAGE (reduced lab (n + 1)) f = 0..n) /\
(!x. x
IN f ==> (x (n + 1) = p)))`,
REPEAT STRIP_TAC THEN EQ_TAC THENL
[ALL_TAC; MESON_TAC[ARITH_RULE `1 <= n + 1`;
LE_REFL]] THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
EXTENSION]) THENL
[DISCH_THEN(MP_TAC o SPEC `j - 1`) THEN
ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN DISCH_THEN(K ALL_TAC) THEN
ASM_SIMP_TAC[
IN_IMAGE;
IN_NUMSEG;
LE_0;
NOT_EXISTS_THM;
ARITH_RULE `j <= n + 1 ==> j - 1 <= n`] THEN
ASM_MESON_TAC[
REDUCED_LABELLING_0];
DISCH_THEN(MP_TAC o SPEC `j:num`) THEN
REWRITE_TAC[
IN_IMAGE;
IN_NUMSEG;
LE_0;
NOT_LE] THEN
ASM_SIMP_TAC[ARITH_RULE `j <= n + 1 ==> ((j <= n) <=> ~(j = n + 1))`] THEN
ASM_MESON_TAC[
REDUCED_LABELLING_1; ARITH_RULE `~(1 = 0)`;
LT_REFL]]);;
let KUHN_INDUCTION = prove
(`!p n. 0 < p /\
(!x j. (!j. x(j) <= p) /\ 1 <= j /\ j <= n + 1 /\ (x j = 0)
==> (lab x j = 0)) /\
(!x j. (!j. x(j) <= p) /\ 1 <= j /\ j <= n + 1 /\ (x j = p)
==> (lab x j = 1))
==>
ODD(
CARD {f | ksimplex p n f /\
(
IMAGE (reduced lab n) f = 0..n)})
==>
ODD(
CARD {s | ksimplex p (n + 1) s /\
(
IMAGE (reduced lab (n + 1)) s = 0..n+1)})`,
REPEAT STRIP_TAC THEN
MATCH_MP_TAC(REWRITE_RULE[
IN_ELIM_THM]
KUHN_SIMPLEX_LEMMA) THEN
CONJ_TAC THENL
[REWRITE_TAC[
SUBSET;
FORALL_IN_IMAGE;
IN_NUMSEG;
LE_0] THEN
MESON_TAC[ARITH_RULE `x <= n ==> x <= n + 1`;
REDUCED_LABELLING];
ALL_TAC] THEN
FIRST_ASSUM(fun th -> MP_TAC th THEN
MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC) THEN
AP_TERM_TAC THEN GEN_REWRITE_TAC I [
EXTENSION] THEN
X_GEN_TAC `f:(num->num)->bool` THEN REWRITE_TAC[
IN_ELIM_THM] THEN
ASM_CASES_TAC
`(!x j. x
IN f /\ 1 <= j /\ j <= n + 1 /\ (x j = 0) ==> (lab x j = 0)) /\
(!x j. x
IN f /\ 1 <= j /\ j <= n + 1 /\ (x j = p) ==> (lab x j = 1))`
THENL
[ALL_TAC;
MATCH_MP_TAC(TAUT `~a /\ ~b ==> (a /\ c <=> b /\ d)`) THEN
CONJ_TAC THEN FIRST_X_ASSUM(MP_TAC o check (is_neg o concl)) THEN
REWRITE_TAC[CONTRAPOS_THM] THEN REWRITE_TAC[ksimplex] THEN
ASM_MESON_TAC[
IN_DELETE]] THEN
ASM_SIMP_TAC[
COMPLETE_FACE_TOP] THEN
ASM_CASES_TAC `!x. x
IN f ==> (x(n + 1):num = p)` THENL
[ALL_TAC;
ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o CONJUNCT1) THEN
REWRITE_TAC[ksimplex] THEN
ASM_MESON_TAC[ARITH_RULE `~(n + 1 <= n)`]] THEN
ASM_SIMP_TAC[
SIMPLEX_TOP_FACE] THEN
ASM_CASES_TAC `ksimplex p n f` THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[
EXTENSION;
IN_IMAGE] THEN
AP_TERM_TAC THEN GEN_REWRITE_TAC I [
FUN_EQ_THM] THEN
X_GEN_TAC `k:num` THEN REWRITE_TAC[] THEN AP_THM_TAC THEN AP_TERM_TAC THEN
AP_TERM_TAC THEN GEN_REWRITE_TAC I [
FUN_EQ_THM] THEN
X_GEN_TAC `x:num->num` THEN REWRITE_TAC[] THEN
ASM_CASES_TAC `(x:num->num)
IN f` THEN ASM_REWRITE_TAC[] THEN
AP_TERM_TAC THEN CONV_TAC SYM_CONV THEN
MATCH_MP_TAC
REDUCED_LABELLING_SUC THEN
MATCH_MP_TAC(ARITH_RULE `a:num < b ==> ~(a = b)`) THEN
MATCH_MP_TAC
REDUCED_LABELLING_1 THEN
REWRITE_TAC[
LE_REFL; ARITH_RULE `1 <= n + 1`] THEN
MATCH_MP_TAC(ARITH_RULE `(n = 1) ==> ~(n = 0)`) THEN
FIRST_X_ASSUM MATCH_MP_TAC THEN
REWRITE_TAC[
LE_REFL; ARITH_RULE `1 <= n + 1`] THEN
ASM_MESON_TAC[ksimplex]);;
let KUHN_COMBINATORIAL = prove
(`!lab p n.
0 < p /\
(!x j. (!j. x(j) <= p) /\ 1 <= j /\ j <= n /\ (x j = 0)
==> (lab x j = 0)) /\
(!x j. (!j. x(j) <= p) /\ 1 <= j /\ j <= n /\ (x j = p)
==> (lab x j = 1))
==>
ODD(
CARD {s | ksimplex p n s /\
(
IMAGE (reduced lab n) s = 0..n)})`,
let KUHN_LEMMA = prove
(`!n p label.
0 < p /\ 0 < n /\
(!x. (!i. 1 <= i /\ i <= n ==> x(i) <= p)
==> !i. 1 <= i /\ i <= n ==> (label x i = 0) \/ (label x i = 1)) /\
(!x. (!i. 1 <= i /\ i <= n ==> x(i) <= p)
==> !i. 1 <= i /\ i <= n /\ (x i = 0) ==> (label x i = 0)) /\
(!x. (!i. 1 <= i /\ i <= n ==> x(i) <= p)
==> !i. 1 <= i /\ i <= n /\ (x i = p) ==> (label x i = 1))
==> ?q. (!i. 1 <= i /\ i <= n ==> q(i) < p) /\
(!i. 1 <= i /\ i <= n
==> ?r s. (!j. 1 <= j /\ j <= n
==> q(j) <= r(j) /\ r(j) <= q(j) + 1) /\
(!j. 1 <= j /\ j <= n
==> q(j) <= s(j) /\ s(j) <= q(j) + 1) /\
~(label r i = label s i))`,
REPEAT STRIP_TAC THEN
MP_TAC(SPECL [`label:(num->num)->num->num`; `p:num`; `n:num`]
KUHN_COMBINATORIAL) THEN
ANTS_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
ASM_CASES_TAC
`{s | ksimplex p n s /\ (
IMAGE (reduced label n) s = 0 .. n)} = {}`
THENL [ASM_REWRITE_TAC[
CARD_CLAUSES; ARITH]; ALL_TAC] THEN
DISCH_THEN(K ALL_TAC) THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM
MEMBER_NOT_EMPTY]) THEN
REWRITE_TAC[
IN_ELIM_THM] THEN
DISCH_THEN(X_CHOOSE_THEN `s:(num->num)->bool` STRIP_ASSUME_TAC) THEN
MP_TAC(SPECL [`p:num`; `n:num`; `s:(num->num)->bool`]
KSIMPLEX_EXTREMA_STRONG) THEN
ASM_REWRITE_TAC[GSYM
LT_NZ] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `a:num->num` THEN
DISCH_THEN(X_CHOOSE_THEN `b:num->num` STRIP_ASSUME_TAC) THEN
CONJ_TAC THEN X_GEN_TAC `i:num` THEN STRIP_TAC THENL
[MATCH_MP_TAC(ARITH_RULE `x + 1 <= y ==> x < y`) THEN
MATCH_MP_TAC
LE_TRANS THEN EXISTS_TAC `(b:num->num) i` THEN
CONJ_TAC THENL [ASM_REWRITE_TAC[
LE_REFL]; ALL_TAC] THEN
ASM_MESON_TAC[ksimplex];
ALL_TAC] THEN
UNDISCH_TAC `
IMAGE (reduced label n) s = 0 .. n` THEN
REWRITE_TAC[
EXTENSION;
IN_IMAGE] THEN
DISCH_THEN(fun th ->
MP_TAC(SPEC `i - 1` th) THEN MP_TAC(SPEC `i:num` th)) THEN
ASM_REWRITE_TAC[
IN_NUMSEG;
LE_0] THEN
DISCH_THEN(X_CHOOSE_THEN `u:num->num` (STRIP_ASSUME_TAC o GSYM)) THEN
ASM_SIMP_TAC[ARITH_RULE `1 <= i /\ i <= n ==> i - 1 <= n`] THEN
DISCH_THEN(X_CHOOSE_THEN `v:num->num` (STRIP_ASSUME_TAC o GSYM)) THEN
MAP_EVERY EXISTS_TAC [`u:num->num`; `v:num->num`] THEN
REWRITE_TAC[
CONJ_ASSOC] THEN
CONJ_TAC THENL [ASM_MESON_TAC[
KLE_IMP_POINTWISE]; ALL_TAC] THEN
MP_TAC(SPECL [`label:(num->num)->num->num`; `u:num->num`; `n:num`]
REDUCED_LABELLING) THEN
MP_TAC(SPECL [`label:(num->num)->num->num`; `v:num->num`; `n:num`]
REDUCED_LABELLING) THEN
ASM_REWRITE_TAC[] THEN
ASM_SIMP_TAC[ARITH_RULE `1 <= i /\ i <= n ==> ~(i - 1 = n)`] THEN
ASM_SIMP_TAC[
SUB_ADD] THEN ASM_MESON_TAC[ARITH_RULE `i < i + 1`]);;
let RETRACTION_o = prove
(`!f g s t u:real^N->bool.
retraction (s,t) f /\ retraction (t,u) g
==> retraction (s,u) (g o f)`,
REPEAT GEN_TAC THEN REWRITE_TAC[retraction] THEN REPEAT STRIP_TAC THENL
[ASM SET_TAC[];
MATCH_MP_TAC
CONTINUOUS_ON_COMPOSE THEN ASM_REWRITE_TAC[] THEN
ASM_MESON_TAC[
CONTINUOUS_ON_SUBSET];
REWRITE_TAC[
IMAGE_o] THEN ASM SET_TAC[];
REWRITE_TAC[
o_THM] THEN ASM SET_TAC[]]);;
let AR = new_definition
`AR(s:real^N->bool) <=>
!u s':real^(N,1)finite_sum->bool.
s homeomorphic s' /\ closed_in (subtopology euclidean u) s'
==> s' retract_of u`;;let ANR = new_definition
`ANR(s:real^N->bool) <=>
!u s':real^(N,1)finite_sum->bool.
s homeomorphic s' /\ closed_in (subtopology euclidean u) s'
==> ?t. open_in (subtopology euclidean u) t /\
s' retract_of t`;;let AR_IMP_ABSOLUTE_EXTENSOR = prove
(`!f:real^M->real^N u t s.
AR s /\ f
continuous_on t /\
IMAGE f t
SUBSET s /\
closed_in (subtopology euclidean u) t
==> ?g. g
continuous_on u /\
IMAGE g u
SUBSET s /\
!x. x
IN t ==> g x = f x`,
REPEAT STRIP_TAC THEN
SUBGOAL_THEN
`?c s':real^(N,1)finite_sum->bool.
convex c /\ ~(c = {}) /\
closed_in (subtopology euclidean c) s' /\
(s:real^N->bool) homeomorphic s'`
STRIP_ASSUME_TAC THENL
[MATCH_MP_TAC
HOMEOMORPHIC_CLOSED_IN_CONVEX THEN
REWRITE_TAC[
DIMINDEX_FINITE_SUM; DIMINDEX_1; GSYM
INT_OF_NUM_ADD] THEN
REWRITE_TAC[INT_ARITH `x:int < y + &1 <=> x <= y`;
AFF_DIM_LE_UNIV];
ALL_TAC] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
AR]) THEN
DISCH_THEN(MP_TAC o SPECL
[`c:real^(N,1)finite_sum->bool`; `s':real^(N,1)finite_sum->bool`]) THEN
ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [homeomorphic]) THEN
REWRITE_TAC[homeomorphism;
LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC
[`g:real^N->real^(N,1)finite_sum`; `h:real^(N,1)finite_sum->real^N`] THEN
STRIP_TAC THEN MP_TAC(ISPECL
[`(g:real^N->real^(N,1)finite_sum) o (f:real^M->real^N)`;
`c:real^(N,1)finite_sum->bool`; `u:real^M->bool`; `t:real^M->bool`]
DUGUNDJI) THEN
ASM_REWRITE_TAC[
IMAGE_o;
o_THM] THEN
FIRST_ASSUM(ASSUME_TAC o MATCH_MP
RETRACT_OF_IMP_SUBSET) THEN ANTS_TAC THENL
[CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
MATCH_MP_TAC
CONTINUOUS_ON_COMPOSE THEN ASM_REWRITE_TAC[] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[
IMP_CONJ]
CONTINUOUS_ON_SUBSET)) THEN
ASM SET_TAC[];
ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `f':real^M->real^(N,1)finite_sum`
STRIP_ASSUME_TAC) THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
retract_of]) THEN
REWRITE_TAC[retraction;
LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `r:real^(N,1)finite_sum->real^(N,1)finite_sum` THEN
STRIP_TAC THEN
EXISTS_TAC `(h:real^(N,1)finite_sum->real^N) o r o
(f':real^M->real^(N,1)finite_sum)` THEN
ASM_REWRITE_TAC[
IMAGE_o;
o_THM] THEN
CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
REWRITE_TAC[
o_ASSOC] THEN MATCH_MP_TAC
CONTINUOUS_ON_COMPOSE THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC
CONTINUOUS_ON_COMPOSE THEN
CONJ_TAC THEN FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[
IMP_CONJ]
CONTINUOUS_ON_SUBSET)) THEN ASM SET_TAC[]);;
let AR_IMP_ABSOLUTE_RETRACT = prove
(`!s:real^N->bool u s':real^M->bool.
AR s /\ s homeomorphic s' /\
closed_in (subtopology euclidean u) s'
==> s'
retract_of u`,
REPEAT STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [homeomorphic]) THEN
REWRITE_TAC[homeomorphism;
LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`g:real^N->real^M`; `h:real^M->real^N`] THEN
STRIP_TAC THEN
MP_TAC(ISPECL [`h:real^M->real^N`; `u:real^M->bool`; `s':real^M->bool`;
`s:real^N->bool`]
AR_IMP_ABSOLUTE_EXTENSOR) THEN
ASM_REWRITE_TAC[
SUBSET_REFL] THEN
DISCH_THEN(X_CHOOSE_THEN `h':real^M->real^N` STRIP_ASSUME_TAC) THEN
REWRITE_TAC[
retract_of; retraction] THEN
EXISTS_TAC `(g:real^N->real^M) o (h':real^M->real^N)` THEN
FIRST_ASSUM(ASSUME_TAC o MATCH_MP
CLOSED_IN_IMP_SUBSET) THEN
ASM_SIMP_TAC[
o_THM;
IMAGE_o] THEN
CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
MATCH_MP_TAC
CONTINUOUS_ON_COMPOSE THEN ASM_REWRITE_TAC[] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[
IMP_CONJ]
CONTINUOUS_ON_SUBSET)) THEN ASM SET_TAC[]);;
let ABSOLUTE_EXTENSOR_IMP_AR = prove
(`!s:real^N->bool.
(!f:real^(N,1)finite_sum->real^N u t.
f
continuous_on t /\
IMAGE f t
SUBSET s /\
closed_in (subtopology euclidean u) t
==> ?g. g
continuous_on u /\
IMAGE g u
SUBSET s /\
!x. x
IN t ==> g x = f x)
==>
AR s`,
REPEAT STRIP_TAC THEN REWRITE_TAC[
AR] THEN MAP_EVERY X_GEN_TAC
[`u:real^(N,1)finite_sum->bool`; `t:real^(N,1)finite_sum->bool`] THEN
STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [homeomorphic]) THEN
REWRITE_TAC[homeomorphism;
LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC
[`g:real^N->real^(N,1)finite_sum`; `h:real^(N,1)finite_sum->real^N`] THEN
STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o ISPECL
[`h:real^(N,1)finite_sum->real^N`;
`u:real^(N,1)finite_sum->bool`; `t:real^(N,1)finite_sum->bool`]) THEN
ASM_REWRITE_TAC[
SUBSET_REFL] THEN DISCH_THEN(X_CHOOSE_THEN
`h':real^(N,1)finite_sum->real^N` STRIP_ASSUME_TAC) THEN
REWRITE_TAC[
retract_of; retraction] THEN
EXISTS_TAC `(g:real^N->real^(N,1)finite_sum) o
(h':real^(N,1)finite_sum->real^N)` THEN
FIRST_ASSUM(ASSUME_TAC o MATCH_MP
CLOSED_IN_IMP_SUBSET) THEN
ASM_SIMP_TAC[
o_THM;
IMAGE_o] THEN
CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
MATCH_MP_TAC
CONTINUOUS_ON_COMPOSE THEN ASM_REWRITE_TAC[] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[
IMP_CONJ]
CONTINUOUS_ON_SUBSET)) THEN ASM SET_TAC[]);;
let ANR_IMP_ABSOLUTE_NEIGHBOURHOOD_EXTENSOR = prove
(`!f:real^M->real^N u t s.
ANR s /\ f
continuous_on t /\
IMAGE f t
SUBSET s /\
closed_in (subtopology euclidean u) t
==> ?v g. t
SUBSET v /\
open_in (subtopology euclidean u) v /\
g
continuous_on v /\
IMAGE g v
SUBSET s /\
!x. x
IN t ==> g x = f x`,
REPEAT STRIP_TAC THEN
SUBGOAL_THEN
`?c s':real^(N,1)finite_sum->bool.
convex c /\ ~(c = {}) /\
closed_in (subtopology euclidean c) s' /\
(s:real^N->bool) homeomorphic s'`
STRIP_ASSUME_TAC THENL
[MATCH_MP_TAC
HOMEOMORPHIC_CLOSED_IN_CONVEX THEN
REWRITE_TAC[
DIMINDEX_FINITE_SUM; DIMINDEX_1; GSYM
INT_OF_NUM_ADD] THEN
REWRITE_TAC[INT_ARITH `x:int < y + &1 <=> x <= y`;
AFF_DIM_LE_UNIV];
ALL_TAC] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
ANR]) THEN
DISCH_THEN(MP_TAC o SPECL
[`c:real^(N,1)finite_sum->bool`; `s':real^(N,1)finite_sum->bool`]) THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN
`d:real^(N,1)finite_sum->bool` STRIP_ASSUME_TAC) THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [homeomorphic]) THEN
REWRITE_TAC[homeomorphism;
LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC
[`g:real^N->real^(N,1)finite_sum`; `h:real^(N,1)finite_sum->real^N`] THEN
STRIP_TAC THEN MP_TAC(ISPECL
[`(g:real^N->real^(N,1)finite_sum) o (f:real^M->real^N)`;
`c:real^(N,1)finite_sum->bool`; `u:real^M->bool`; `t:real^M->bool`]
DUGUNDJI) THEN
ASM_REWRITE_TAC[
IMAGE_o;
o_THM] THEN
FIRST_ASSUM(ASSUME_TAC o MATCH_MP
OPEN_IN_IMP_SUBSET) THEN
FIRST_ASSUM(ASSUME_TAC o MATCH_MP
RETRACT_OF_IMP_SUBSET) THEN ANTS_TAC THENL
[CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
MATCH_MP_TAC
CONTINUOUS_ON_COMPOSE THEN ASM_REWRITE_TAC[] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[
IMP_CONJ]
CONTINUOUS_ON_SUBSET)) THEN
ASM SET_TAC[];
ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `f':real^M->real^(N,1)finite_sum`
STRIP_ASSUME_TAC) THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
retract_of]) THEN
REWRITE_TAC[retraction;
LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `r:real^(N,1)finite_sum->real^(N,1)finite_sum` THEN
STRIP_TAC THEN
EXISTS_TAC `{x | x
IN u /\ (f':real^M->real^(N,1)finite_sum) x
IN d}` THEN
EXISTS_TAC `(h:real^(N,1)finite_sum->real^N) o r o
(f':real^M->real^(N,1)finite_sum)` THEN
ASM_REWRITE_TAC[
IMAGE_o;
o_THM] THEN REPEAT CONJ_TAC THENL
[REPEAT(FIRST_X_ASSUM(ASSUME_TAC o MATCH_MP
CLOSED_IN_IMP_SUBSET)) THEN
ASM SET_TAC[];
MATCH_MP_TAC
CONTINUOUS_OPEN_IN_PREIMAGE_GEN THEN ASM_MESON_TAC[];
REPEAT(MATCH_MP_TAC
CONTINUOUS_ON_COMPOSE THEN CONJ_TAC) THEN
REWRITE_TAC[
IMAGE_o] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[
IMP_CONJ]
CONTINUOUS_ON_SUBSET)) THEN ASM SET_TAC[];
ASM SET_TAC[];
ASM SET_TAC[]]);;
let ABSOLUTE_NEIGHBOURHOOD_EXTENSOR_IMP_ANR = prove
(`!s:real^N->bool.
(!f:real^(N,1)finite_sum->real^N u t.
f
continuous_on t /\
IMAGE f t
SUBSET s /\
closed_in (subtopology euclidean u) t
==> ?v g. t
SUBSET v /\
open_in (subtopology euclidean u) v /\
g
continuous_on v /\
IMAGE g v
SUBSET s /\
!x. x
IN t ==> g x = f x)
==>
ANR s`,
REPEAT STRIP_TAC THEN REWRITE_TAC[
ANR] THEN MAP_EVERY X_GEN_TAC
[`u:real^(N,1)finite_sum->bool`; `t:real^(N,1)finite_sum->bool`] THEN
STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [homeomorphic]) THEN
REWRITE_TAC[homeomorphism;
LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC
[`g:real^N->real^(N,1)finite_sum`; `h:real^(N,1)finite_sum->real^N`] THEN
STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o ISPECL
[`h:real^(N,1)finite_sum->real^N`;
`u:real^(N,1)finite_sum->bool`; `t:real^(N,1)finite_sum->bool`]) THEN
ASM_REWRITE_TAC[
SUBSET_REFL] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `v:real^(N,1)finite_sum->bool` THEN
DISCH_THEN(X_CHOOSE_THEN `h':real^(N,1)finite_sum->real^N`
STRIP_ASSUME_TAC) THEN
ASM_REWRITE_TAC[
retract_of; retraction] THEN
EXISTS_TAC `(g:real^N->real^(N,1)finite_sum) o
(h':real^(N,1)finite_sum->real^N)` THEN
FIRST_ASSUM(ASSUME_TAC o MATCH_MP
CLOSED_IN_IMP_SUBSET) THEN
ASM_SIMP_TAC[
o_THM;
IMAGE_o] THEN
CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
MATCH_MP_TAC
CONTINUOUS_ON_COMPOSE THEN ASM_REWRITE_TAC[] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[
IMP_CONJ]
CONTINUOUS_ON_SUBSET)) THEN ASM SET_TAC[]);;
let AR_ANR = prove
(`!s:real^N->bool.
AR s <=>
ANR s /\ contractible s /\ ~(s = {})`,
GEN_TAC THEN EQ_TAC THEN STRIP_TAC THEN ASM_SIMP_TAC[
AR_IMP_ANR] THENL
[CONJ_TAC THENL
[ALL_TAC;
ASM_MESON_TAC[
AR;
HOMEOMORPHIC_EMPTY;
RETRACT_OF_EMPTY;
FORALL_UNWIND_THM2;
CLOSED_IN_EMPTY;
UNIV_NOT_EMPTY]] THEN
SUBGOAL_THEN
`?c s':real^(N,1)finite_sum->bool.
convex c /\ ~(c = {}) /\
closed_in (subtopology euclidean c) s' /\
(s:real^N->bool) homeomorphic s'`
STRIP_ASSUME_TAC THENL
[MATCH_MP_TAC
HOMEOMORPHIC_CLOSED_IN_CONVEX THEN
REWRITE_TAC[
DIMINDEX_FINITE_SUM; DIMINDEX_1; GSYM
INT_OF_NUM_ADD] THEN
REWRITE_TAC[INT_ARITH `x:int < y + &1 <=> x <= y`;
AFF_DIM_LE_UNIV];
ALL_TAC] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
AR]) THEN
DISCH_THEN(MP_TAC o SPECL
[`c:real^(N,1)finite_sum->bool`; `s':real^(N,1)finite_sum->bool`]) THEN
ASM_REWRITE_TAC[] THEN
ASM_MESON_TAC[
HOMEOMORPHIC_SYM;
HOMEOMORPHIC_CONTRACTIBLE;
RETRACT_OF_CONTRACTIBLE;
CONVEX_IMP_CONTRACTIBLE];
ALL_TAC] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [contractible]) THEN
REWRITE_TAC[
LEFT_IMP_EXISTS_THM;
homotopic_with] THEN
MAP_EVERY X_GEN_TAC [`a:real^N`; `h:real^(1,N)finite_sum->real^N`] THEN
STRIP_TAC THEN REWRITE_TAC[
AR_EQ_ABSOLUTE_EXTENSOR] THEN
MAP_EVERY X_GEN_TAC
[`f:real^(N,1)finite_sum->real^N`; `w:real^(N,1)finite_sum->bool`;
`t:real^(N,1)finite_sum->bool`] THEN
STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o ISPECL
[`f:real^(N,1)finite_sum->real^N`; `w:real^(N,1)finite_sum->bool`;
`t:real^(N,1)finite_sum->bool`] o
REWRITE_RULE[
ANR_EQ_ABSOLUTE_NEIGHBOURHOOD_EXTENSOR]) THEN
ASM_REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC
[`u:real^(N,1)finite_sum->bool`; `g:real^(N,1)finite_sum->real^N`] THEN
STRIP_TAC THEN
MP_TAC(ISPECL
[`t:real^(N,1)finite_sum->bool`; `w
DIFF u:real^(N,1)finite_sum->bool`;
`w:real^(N,1)finite_sum->bool`]
SEPARATION_NORMAL_LOCAL) THEN
ASM_SIMP_TAC[
CLOSED_IN_DIFF;
CLOSED_IN_REFL] THEN
ANTS_TAC THENL [ASM SET_TAC[]; REWRITE_TAC[
LEFT_IMP_EXISTS_THM]] THEN
MAP_EVERY X_GEN_TAC
[`v:real^(N,1)finite_sum->bool`; `v':real^(N,1)finite_sum->bool`] THEN
STRIP_TAC THEN
MP_TAC(ISPECL
[`t:real^(N,1)finite_sum->bool`; `w
DIFF v:real^(N,1)finite_sum->bool`;
`w:real^(N,1)finite_sum->bool`; `vec 0:real^1`; `vec 1:real^1`]
URYSOHN_LOCAL) THEN
ASM_SIMP_TAC[
SEGMENT_1;
CLOSED_IN_DIFF;
CLOSED_IN_REFL] THEN
ANTS_TAC THENL [ASM SET_TAC[]; REWRITE_TAC[
LEFT_IMP_EXISTS_THM]] THEN
REWRITE_TAC[
DROP_VEC;
REAL_POS] THEN
X_GEN_TAC `e:real^(N,1)finite_sum->real^1` THEN STRIP_TAC THEN
EXISTS_TAC
`\x. if (x:real^(N,1)finite_sum)
IN w
DIFF v then a
else (h:real^(1,N)finite_sum->real^N) (pastecart (e x) (g x))` THEN
REWRITE_TAC[] THEN CONJ_TAC THENL
[SUBGOAL_THEN `w:real^(N,1)finite_sum->bool = (w
DIFF v)
UNION (w
DIFF v')`
MP_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
DISCH_THEN(fun th ->
GEN_REWRITE_TAC RAND_CONV [th] THEN
MATCH_MP_TAC
CONTINUOUS_ON_CASES_LOCAL THEN
REWRITE_TAC[GSYM th]) THEN
ASM_SIMP_TAC[
CLOSED_IN_DIFF;
CLOSED_IN_REFL;
CONTINUOUS_ON_CONST] THEN
CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
GEN_REWRITE_TAC LAND_CONV [GSYM
o_DEF] THEN
MATCH_MP_TAC
CONTINUOUS_ON_COMPOSE THEN CONJ_TAC THENL
[MATCH_MP_TAC
CONTINUOUS_ON_PASTECART THEN CONJ_TAC; ALL_TAC] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[
IMP_CONJ]
CONTINUOUS_ON_SUBSET)) THEN
REWRITE_TAC[
SUBSET;
FORALL_IN_IMAGE;
PASTECART_IN_PCROSS] THEN
ASM SET_TAC[];
ASM_SIMP_TAC[
SUBSET;
FORALL_IN_IMAGE] THEN RULE_ASSUM_TAC
(REWRITE_RULE[
SUBSET;
FORALL_IN_IMAGE;
FORALL_IN_PCROSS]) THEN
CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[
IN_DIFF] THEN
COND_CASES_TAC THEN ASM SET_TAC[]]);;
let ANR_RETRACT_OF_ANR = prove
(`!s t:real^N->bool.
ANR t /\ s
retract_of t ==>
ANR s`,
REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
REWRITE_TAC[
ANR_EQ_ABSOLUTE_NEIGHBOURHOOD_EXTENSOR] THEN
REPEAT(MATCH_MP_TAC
MONO_FORALL THEN GEN_TAC) THEN
DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
retract_of]) THEN
REWRITE_TAC[retraction;
LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `r:real^N->real^N` THEN STRIP_TAC THEN
ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
MATCH_MP_TAC
MONO_EXISTS THEN GEN_TAC THEN
DISCH_THEN(X_CHOOSE_THEN `g:real^(N,1)finite_sum->real^N`
STRIP_ASSUME_TAC) THEN
EXISTS_TAC `(r:real^N->real^N) o (g:real^(N,1)finite_sum->real^N)` THEN
ASM_SIMP_TAC[
IMAGE_o;
o_THM] THEN
CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
MATCH_MP_TAC
CONTINUOUS_ON_COMPOSE THEN ASM_REWRITE_TAC[] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[
IMP_CONJ]
CONTINUOUS_ON_SUBSET)) THEN
ASM SET_TAC[]);;
let ANR_OPEN_IN = prove
(`!s t:real^N->bool.
open_in (subtopology euclidean t) s /\
ANR t ==>
ANR s`,
REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
REWRITE_TAC[
ANR_EQ_ABSOLUTE_NEIGHBOURHOOD_EXTENSOR] THEN
REPEAT(MATCH_MP_TAC
MONO_FORALL THEN GEN_TAC) THEN
DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
FIRST_ASSUM(ASSUME_TAC o MATCH_MP
OPEN_IN_IMP_SUBSET) THEN
ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
ONCE_REWRITE_TAC[
SWAP_EXISTS_THM] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `g:real^(N,1)finite_sum->real^N` THEN
DISCH_THEN(X_CHOOSE_THEN `w:real^(N,1)finite_sum->bool`
STRIP_ASSUME_TAC) THEN
EXISTS_TAC `{x | x
IN w /\ (g:real^(N,1)finite_sum->real^N) x
IN s}` THEN
ASM_REWRITE_TAC[] THEN
CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN CONJ_TAC THENL
[MATCH_MP_TAC
OPEN_IN_TRANS THEN
EXISTS_TAC `w:real^(N,1)finite_sum->bool` THEN
ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC
CONTINUOUS_OPEN_IN_PREIMAGE_GEN THEN ASM_MESON_TAC[];
CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[
IMP_CONJ]
CONTINUOUS_ON_SUBSET)) THEN ASM SET_TAC[]]);;
let AR_INTERVAL = prove
(`(!a b:real^N.
AR(interval[a,b]) <=> ~(interval[a,b] = {})) /\
(!a b:real^N.
AR(interval(a,b)) <=> ~(interval(a,b) = {}))`,
let ANR_PCROSS = prove
(`!s:real^M->bool t:real^N->bool.
ANR s /\
ANR t ==>
ANR(s
PCROSS t)`,
REPEAT STRIP_TAC THEN SIMP_TAC[
ANR_EQ_ABSOLUTE_NEIGHBOURHOOD_EXTENSOR] THEN
MAP_EVERY X_GEN_TAC
[`f:real^((M,N)finite_sum,1)finite_sum->real^(M,N)finite_sum`;
`u:real^((M,N)finite_sum,1)finite_sum->bool`;
`c:real^((M,N)finite_sum,1)finite_sum->bool`] THEN
STRIP_TAC THEN
MP_TAC(ISPECL
[`fstcart o (f:real^((M,N)finite_sum,1)finite_sum->real^(M,N)finite_sum)`;
`u:real^((M,N)finite_sum,1)finite_sum->bool`;
`c:real^((M,N)finite_sum,1)finite_sum->bool`;
`s:real^M->bool`]
ANR_IMP_ABSOLUTE_NEIGHBOURHOOD_EXTENSOR) THEN
MP_TAC(ISPECL
[`sndcart o (f:real^((M,N)finite_sum,1)finite_sum->real^(M,N)finite_sum)`;
`u:real^((M,N)finite_sum,1)finite_sum->bool`;
`c:real^((M,N)finite_sum,1)finite_sum->bool`;
`t:real^N->bool`]
ANR_IMP_ABSOLUTE_NEIGHBOURHOOD_EXTENSOR) THEN
ASM_SIMP_TAC[
CONTINUOUS_ON_COMPOSE;
LINEAR_CONTINUOUS_ON;
LINEAR_FSTCART;
LINEAR_SNDCART;
IMAGE_o] THEN
RULE_ASSUM_TAC
(REWRITE_RULE[
SUBSET;
FORALL_IN_IMAGE;
PCROSS;
IN_ELIM_THM]) THEN
REWRITE_TAC[
SUBSET;
FORALL_IN_IMAGE] THEN ANTS_TAC THENL
[ASM_MESON_TAC[
SNDCART_PASTECART]; REWRITE_TAC[
LEFT_IMP_EXISTS_THM]] THEN
MAP_EVERY X_GEN_TAC
[`w2:real^((M,N)finite_sum,1)finite_sum->bool`;
`h:real^((M,N)finite_sum,1)finite_sum->real^N`] THEN
STRIP_TAC THEN ANTS_TAC THENL
[ASM_MESON_TAC[
FSTCART_PASTECART]; REWRITE_TAC[
LEFT_IMP_EXISTS_THM]] THEN
MAP_EVERY X_GEN_TAC
[`w1:real^((M,N)finite_sum,1)finite_sum->bool`;
`g:real^((M,N)finite_sum,1)finite_sum->real^M`] THEN
STRIP_TAC THEN MAP_EVERY EXISTS_TAC
[`w1
INTER w2:real^((M,N)finite_sum,1)finite_sum->bool`;
`\x:real^((M,N)finite_sum,1)finite_sum.
pastecart (g x:real^M) (h x:real^N)`] THEN
ASM_SIMP_TAC[
OPEN_IN_INTER;
IN_INTER;
o_DEF;
PASTECART_IN_PCROSS;
PASTECART_FST_SND] THEN
MATCH_MP_TAC
CONTINUOUS_ON_PASTECART THEN
ASM_MESON_TAC[
CONTINUOUS_ON_SUBSET;
INTER_SUBSET]);;
let BORSUK_HOMOTOPY_EXTENSION_HOMOTOPIC = prove
(`!f:real^M->real^N g s t u.
closed_in (subtopology euclidean t) s /\
(
ANR s /\
ANR t \/
ANR u) /\
f
continuous_on t /\
IMAGE f t
SUBSET u /\
homotopic_with (\x. T) (s,u) f g
==> ?g'.
homotopic_with (\x. T) (t,u) f g' /\
g'
continuous_on t /\
IMAGE g' t
SUBSET u /\
!x. x
IN s ==> g'(x) = g(x)`,
REPEAT GEN_TAC THEN DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
FIRST_ASSUM(ASSUME_TAC o MATCH_MP
CLOSED_IN_IMP_SUBSET) THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
homotopic_with]) THEN
REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `h:real^(1,M)finite_sum->real^N`
STRIP_ASSUME_TAC) THEN
MAP_EVERY ABBREV_TAC
[`h' = \z. if sndcart z
IN s then (h:real^(1,M)finite_sum->real^N) z
else f(sndcart z)`;
`B:real^(1,M)finite_sum->bool =
{vec 0}
PCROSS t
UNION interval[vec 0,vec 1]
PCROSS s`] THEN
SUBGOAL_THEN
`
closed_in (subtopology euclidean (interval[vec 0:real^1,vec 1]
PCROSS t))
({vec 0}
PCROSS (t:real^M->bool)) /\
closed_in (subtopology euclidean (interval[vec 0:real^1,vec 1]
PCROSS t))
(interval[vec 0,vec 1]
PCROSS s)`
STRIP_ASSUME_TAC THENL
[CONJ_TAC THEN MATCH_MP_TAC
CLOSED_IN_PCROSS THEN
ASM_REWRITE_TAC[
CLOSED_IN_SING;
CLOSED_IN_REFL;
ENDS_IN_UNIT_INTERVAL];
ALL_TAC] THEN
SUBGOAL_THEN `(h':real^(1,M)finite_sum->real^N)
continuous_on B`
ASSUME_TAC THENL
[MAP_EVERY EXPAND_TAC ["h'";
let HOMOTOPIC_NEIGHBOURHOOD_EXTENSION = prove
(`!f g:real^M->real^N s t u.
f
continuous_on s /\
IMAGE f s
SUBSET u /\
g
continuous_on s /\
IMAGE g s
SUBSET u /\
closed_in (subtopology euclidean s) t /\
ANR u /\
homotopic_with (\x. T) (t,u) f g
==> ?v. t
SUBSET v /\
open_in (subtopology euclidean s) v /\
homotopic_with (\x. T) (v,u) f g`,
REPEAT STRIP_TAC THEN
FIRST_ASSUM(ASSUME_TAC o MATCH_MP
CLOSED_IN_IMP_SUBSET) THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [
homotopic_with]) THEN
DISCH_THEN(X_CHOOSE_THEN `h:real^(1,M)finite_sum->real^N`
STRIP_ASSUME_TAC) THEN
ABBREV_TAC
`h' = \z. if fstcart z
IN {vec 0} then f(sndcart z)
else if fstcart z
IN {vec 1} then g(sndcart z)
else (h:real^(1,M)finite_sum->real^N) z` THEN
MP_TAC(ISPECL
[`h':real^(1,M)finite_sum->real^N`;
`interval[vec 0:real^1,vec 1]
PCROSS (s:real^M->bool)`;
`{vec 0:real^1,vec 1}
PCROSS (s:real^M->bool)
UNION
interval[vec 0,vec 1]
PCROSS t`;
`u:real^N->bool`]
ANR_IMP_ABSOLUTE_NEIGHBOURHOOD_EXTENSOR) THEN
ASM_SIMP_TAC[
ENR_IMP_ANR] THEN ANTS_TAC THENL
[REPEAT CONJ_TAC THENL
[REWRITE_TAC[SET_RULE `{a,b} = {a}
UNION {b}`] THEN
REWRITE_TAC[
PCROSS_UNION;
UNION_ASSOC] THEN EXPAND_TAC "h'" THEN
REPLICATE_TAC 2 (MATCH_MP_TAC
CONTINUOUS_ON_CASES_LOCAL THEN
REPLICATE_TAC 2 (CONJ_TAC THENL
[MATCH_MP_TAC
CLOSED_IN_SUBSET_TRANS THEN
EXISTS_TAC `interval[vec 0:real^1,vec 1]
PCROSS (s:real^M->bool)` THEN
REWRITE_TAC[SET_RULE `t
UNION u
SUBSET s
UNION t
UNION u`] THEN
REWRITE_TAC[
SUBSET_UNION;
UNION_SUBSET;
SUBSET_PCROSS] THEN
REWRITE_TAC[
INSERT_SUBSET;
EMPTY_SUBSET;
ENDS_IN_UNIT_INTERVAL] THEN
ASM_REWRITE_TAC[
SUBSET_REFL] THEN
TRY(MATCH_MP_TAC
CLOSED_IN_UNION THEN CONJ_TAC) THEN
MATCH_MP_TAC
CLOSED_IN_PCROSS THEN
ASM_REWRITE_TAC[
CLOSED_IN_REFL] THEN MATCH_MP_TAC
CLOSED_SUBSET THEN
REWRITE_TAC[
SING_SUBSET;
ENDS_IN_UNIT_INTERVAL;
CLOSED_SING];
ALL_TAC]) THEN
REPEAT CONJ_TAC THENL
[GEN_REWRITE_TAC LAND_CONV [GSYM
o_DEF] THEN
MATCH_MP_TAC
CONTINUOUS_ON_COMPOSE THEN
SIMP_TAC[
LINEAR_SNDCART;
LINEAR_CONTINUOUS_ON] THEN
ASM_REWRITE_TAC[
IMAGE_SNDCART_PCROSS;
NOT_INSERT_EMPTY];
ASM_REWRITE_TAC[];
REWRITE_TAC[
FORALL_PASTECART;
IN_UNION;
PASTECART_IN_PCROSS] THEN
REWRITE_TAC[
FSTCART_PASTECART;
IN_SING;
SNDCART_PASTECART] THEN
MAP_EVERY X_GEN_TAC [`x:real^1`; `y:real^M`] THEN
ASM_CASES_TAC `x:real^1 = vec 0` THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[
VEC_EQ;
ARITH_EQ;
ENDS_IN_UNIT_INTERVAL] THEN
ASM_CASES_TAC `x:real^1 = vec 1` THEN ASM_REWRITE_TAC[]]);
REWRITE_TAC[
SUBSET;
FORALL_IN_IMAGE;
FORALL_PASTECART] THEN
REWRITE_TAC[
IN_UNION;
PASTECART_IN_PCROSS;
IN_SING;
NOT_IN_EMPTY] THEN
MAP_EVERY X_GEN_TAC [`x:real^1`; `y:real^M`] THEN
REWRITE_TAC[
IN_INSERT;
NOT_IN_EMPTY] THEN
EXPAND_TAC "h'" THEN
REWRITE_TAC[
FSTCART_PASTECART;
SNDCART_PASTECART;
IN_SING] THEN
REPEAT(COND_CASES_TAC THENL [ASM SET_TAC[]; ASM_REWRITE_TAC[]]) THEN
STRIP_TAC THEN FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
`
IMAGE f s
SUBSET u ==> b
IN s ==> f b
IN u`)) THEN
ASM_REWRITE_TAC[
PASTECART_IN_PCROSS];
MATCH_MP_TAC
CLOSED_IN_UNION THEN CONJ_TAC THEN
MATCH_MP_TAC
CLOSED_IN_PCROSS THEN
ASM_REWRITE_TAC[
CLOSED_IN_REFL] THEN
MATCH_MP_TAC
CLOSED_SUBSET THEN
REWRITE_TAC[
INSERT_SUBSET;
EMPTY_SUBSET;
ENDS_IN_UNIT_INTERVAL] THEN
SIMP_TAC[
CLOSED_INSERT;
CLOSED_EMPTY]];
REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN MAP_EVERY X_GEN_TAC
[`w:real^(1,M)finite_sum->bool`; `k:real^(1,M)finite_sum->real^N`] THEN
STRIP_TAC] THEN
MP_TAC(ISPECL [`interval[vec 0:real^1,vec 1]`;
`t:real^M->bool`; `s:real^M->bool`;
`w:real^(1,M)finite_sum->bool`]
TUBE_LEMMA_GEN) THEN
ASM_REWRITE_TAC[
COMPACT_INTERVAL;
UNIT_INTERVAL_NONEMPTY] THEN
ANTS_TAC THENL [ASM SET_TAC[]; MATCH_MP_TAC
MONO_EXISTS] THEN
X_GEN_TAC `t':real^M->bool` THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
SIMP_TAC[
HOMOTOPIC_WITH] THEN
EXISTS_TAC `k:real^(1,M)finite_sum->real^N` THEN
CONJ_TAC THENL [ASM_MESON_TAC[
CONTINUOUS_ON_SUBSET]; ALL_TAC] THEN
CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
FIRST_ASSUM(ASSUME_TAC o MATCH_MP
OPEN_IN_IMP_SUBSET) THEN
CONJ_TAC THEN X_GEN_TAC `x:real^M` THEN DISCH_TAC THEN
FIRST_X_ASSUM(fun th ->
W(MP_TAC o PART_MATCH (lhs o snd o dest_imp) th o lhs o snd)) THEN
REWRITE_TAC[
IN_UNION;
PASTECART_IN_PCROSS;
IN_INSERT] THEN
(ANTS_TAC THENL [ASM SET_TAC[]; DISCH_THEN SUBST1_TAC]) THEN
EXPAND_TAC "h'" THEN
REWRITE_TAC[
FSTCART_PASTECART;
SNDCART_PASTECART;
IN_SING] THEN
REWRITE_TAC[
VEC_EQ;
ARITH_EQ]);;
let DEFORMATION_RETRACT = prove
(`!s t:real^N->bool.
(?r.
homotopic_with (\x. T) (s,s) (\x. x) r /\ retraction(s,t) r) <=>
t
retract_of s /\
?f.
homotopic_with (\x. T) (s,s) (\x. x) f /\
IMAGE f s
SUBSET t`,
REPEAT GEN_TAC THEN REWRITE_TAC[
retract_of; retraction] THEN EQ_TAC THENL
[REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `r:real^N->real^N` THEN
REPEAT STRIP_TAC THEN EXISTS_TAC `r:real^N->real^N` THEN ASM_REWRITE_TAC[];
DISCH_THEN(CONJUNCTS_THEN2
(X_CHOOSE_THEN `r:real^N->real^N` STRIP_ASSUME_TAC) MP_TAC) THEN
REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `f:real^N->real^N` THEN
STRIP_TAC THEN EXISTS_TAC `r:real^N->real^N` THEN ASM_REWRITE_TAC[] THEN
TRANS_TAC
HOMOTOPIC_WITH_TRANS `f:real^N->real^N` THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC
HOMOTOPIC_WITH_EQ THEN
MAP_EVERY EXISTS_TAC
[`(r:real^N->real^N) o (f:real^N->real^N)`;
`(r:real^N->real^N) o (\x. x)`] THEN
ASM_SIMP_TAC[
o_THM] THEN CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
MATCH_MP_TAC
HOMOTOPIC_WITH_COMPOSE_CONTINUOUS_LEFT THEN
EXISTS_TAC `s:real^N->bool` THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
[ASM_MESON_TAC[
HOMOTOPIC_WITH_SYM]; ASM SET_TAC[]]]);;
let interval_bij = new_definition
`interval_bij (a:real^N,b:real^N) (u:real^N,v:real^N) (x:real^N) =
(lambda i. u$i + (x$i - a$i) / (b$i - a$i) * (v$i - u$i)):real^N`;;let INFNORM_EQ_1_2 = prove
(`infnorm (x:real^2) = &1 <=>
abs(x$1) <= &1 /\ abs(x$2) <= &1 /\
(x$1 = -- &1 \/ x$1 = &1 \/ x$2 = -- &1 \/ x$2 = &1)`,
REWRITE_TAC[
INFNORM_2] THEN REAL_ARITH_TAC);;
let FASHODA_UNIT = prove
(`!f:real^1->real^2 g:real^1->real^2.
IMAGE f (interval[--vec 1,vec 1])
SUBSET interval[--vec 1,vec 1] /\
IMAGE g (interval[--vec 1,vec 1])
SUBSET interval[--vec 1,vec 1] /\
f
continuous_on interval[--vec 1,vec 1] /\
g
continuous_on interval[--vec 1,vec 1] /\
f(--vec 1)$1 = -- &1 /\ f(vec 1)$1 = &1 /\
g(--vec 1)$2 = -- &1 /\ g(vec 1)$2 = &1
==> ?s t. s
IN interval[--vec 1,vec 1] /\
t
IN interval[--vec 1,vec 1] /\
f(s) = g(t)`,
let FASHODA = prove
(`!f g a b:real^2.
path f /\ path g /\
path_image f
SUBSET interval[a,b] /\
path_image g
SUBSET interval[a,b] /\
(pathstart f)$1 = a$1 /\ (pathfinish f)$1 = b$1 /\
(pathstart g)$2 = a$2 /\ (pathfinish g)$2 = b$2
==> ?z. z
IN path_image f /\ z
IN path_image g`,
REPEAT STRIP_TAC THEN
SUBGOAL_THEN `~(interval[a:real^2,b] = {})` MP_TAC THENL
[FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
`s
SUBSET t ==> ~(s = {}) ==> ~(t = {})`)) THEN
REWRITE_TAC[
PATH_IMAGE_NONEMPTY];
ALL_TAC] THEN
REWRITE_TAC[
INTERVAL_NE_EMPTY; DIMINDEX_2;
FORALL_2] THEN STRIP_TAC THEN
MP_TAC(ASSUME `(a:real^2)$1 <= (b:real^2)$1`) THEN
REWRITE_TAC[REAL_ARITH `a <= b <=> b = a \/ a < b`] THEN STRIP_TAC THENL
[SUBGOAL_THEN
`?z:real^2. z
IN path_image g /\ z$2 = (pathstart f:real^2)$2`
MP_TAC THENL
[MATCH_MP_TAC
CONNECTED_IVT_COMPONENT THEN
MAP_EVERY EXISTS_TAC [`pathstart(g:real^1->real^2)`;
`pathfinish(g:real^1->real^2)`] THEN
ASM_SIMP_TAC[
CONNECTED_PATH_IMAGE;
PATHSTART_IN_PATH_IMAGE;
REAL_LE_REFL;
PATHFINISH_IN_PATH_IMAGE; DIMINDEX_2; ARITH] THEN
UNDISCH_TAC `
path_image f
SUBSET interval[a:real^2,b]` THEN
REWRITE_TAC[
SUBSET;
path_image;
IN_INTERVAL_1;
FORALL_IN_IMAGE] THEN
DISCH_THEN(MP_TAC o SPEC `vec 0:real^1`) THEN SIMP_TAC[pathstart] THEN
SIMP_TAC[
DROP_VEC;
REAL_POS;
IN_INTERVAL;
FORALL_2; DIMINDEX_2];
ALL_TAC] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `z:real^2` THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN SIMP_TAC[
path_image;
IN_IMAGE] THEN
EXISTS_TAC `vec 0:real^1` THEN
REWRITE_TAC[
IN_INTERVAL_1;
DROP_VEC;
REAL_POS] THEN
ASM_REWRITE_TAC[
CART_EQ;
FORALL_2; DIMINDEX_2; pathstart] THEN
SUBGOAL_THEN
`(z:real^2)
IN interval[a,b] /\ f(vec 0:real^1)
IN interval[a,b]`
MP_TAC THENL
[ASM_MESON_TAC[
SUBSET;
path_image;
IN_IMAGE;
PATHSTART_IN_PATH_IMAGE;
pathstart];
ASM_REWRITE_TAC[
IN_INTERVAL;
FORALL_2; DIMINDEX_2] THEN REAL_ARITH_TAC];
ALL_TAC] THEN
MP_TAC(ASSUME `(a:real^2)$2 <= (b:real^2)$2`) THEN
REWRITE_TAC[REAL_ARITH `a <= b <=> b = a \/ a < b`] THEN STRIP_TAC THENL
[SUBGOAL_THEN
`?z:real^2. z
IN path_image f /\ z$1 = (pathstart g:real^2)$1`
MP_TAC THENL
[MATCH_MP_TAC
CONNECTED_IVT_COMPONENT THEN
MAP_EVERY EXISTS_TAC [`pathstart(f:real^1->real^2)`;
`pathfinish(f:real^1->real^2)`] THEN
ASM_SIMP_TAC[
CONNECTED_PATH_IMAGE;
PATHSTART_IN_PATH_IMAGE;
REAL_LE_REFL;
PATHFINISH_IN_PATH_IMAGE; DIMINDEX_2; ARITH] THEN
UNDISCH_TAC `
path_image g
SUBSET interval[a:real^2,b]` THEN
REWRITE_TAC[
SUBSET;
path_image;
IN_INTERVAL_1;
FORALL_IN_IMAGE] THEN
DISCH_THEN(MP_TAC o SPEC `vec 0:real^1`) THEN SIMP_TAC[pathstart] THEN
SIMP_TAC[
DROP_VEC;
REAL_POS;
IN_INTERVAL;
FORALL_2; DIMINDEX_2];
ALL_TAC] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `z:real^2` THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN SIMP_TAC[
path_image;
IN_IMAGE] THEN
EXISTS_TAC `vec 0:real^1` THEN
REWRITE_TAC[
IN_INTERVAL_1;
DROP_VEC;
REAL_POS] THEN
ASM_REWRITE_TAC[
CART_EQ;
FORALL_2; DIMINDEX_2; pathstart] THEN
SUBGOAL_THEN
`(z:real^2)
IN interval[a,b] /\ g(vec 0:real^1)
IN interval[a,b]`
MP_TAC THENL
[ASM_MESON_TAC[
SUBSET;
path_image;
IN_IMAGE;
PATHSTART_IN_PATH_IMAGE;
pathstart];
ASM_REWRITE_TAC[
IN_INTERVAL;
FORALL_2; DIMINDEX_2] THEN REAL_ARITH_TAC];
ALL_TAC] THEN
MP_TAC(ISPECL
[`
interval_bij (a,b) (--vec 1,vec 1) o (f:real^1->real^2)`;
`
interval_bij (a,b) (--vec 1,vec 1) o (g:real^1->real^2)`]
FASHODA_UNIT_PATH) THEN
RULE_ASSUM_TAC(REWRITE_RULE[path;
path_image; pathstart; pathfinish]) THEN
ASM_REWRITE_TAC[path;
path_image; pathstart; pathfinish;
o_THM] THEN
ANTS_TAC THENL
[ASM_SIMP_TAC[
CONTINUOUS_ON_COMPOSE;
CONTINUOUS_ON_INTERVAL_BIJ] THEN
REWRITE_TAC[
IMAGE_o] THEN REPLICATE_TAC 2 (CONJ_TAC THENL
[REWRITE_TAC[
SUBSET] THEN ONCE_REWRITE_TAC[
FORALL_IN_IMAGE] THEN
REPEAT STRIP_TAC THEN MATCH_MP_TAC
IN_INTERVAL_INTERVAL_BIJ THEN
SIMP_TAC[
INTERVAL_NE_EMPTY;
VECTOR_NEG_COMPONENT;
VEC_COMPONENT] THEN
CONV_TAC REAL_RAT_REDUCE_CONV THEN ASM SET_TAC[];
ALL_TAC]) THEN
ASM_SIMP_TAC[
interval_bij;
LAMBDA_BETA; DIMINDEX_2; ARITH] THEN
ASM_SIMP_TAC[
REAL_DIV_REFL;
REAL_LT_IMP_NZ;
REAL_SUB_LT] THEN
REWRITE_TAC[
real_div;
REAL_SUB_REFL;
REAL_MUL_LZERO] THEN
SIMP_TAC[
VECTOR_NEG_COMPONENT;
VEC_COMPONENT; DIMINDEX_2; ARITH] THEN
CONV_TAC REAL_RAT_REDUCE_CONV;
ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `z:real^2`
(fun th -> EXISTS_TAC `
interval_bij (--vec 1,vec 1) (a,b) (z:real^2)` THEN
MP_TAC th)) THEN
MATCH_MP_TAC MONO_AND THEN CONJ_TAC THEN REWRITE_TAC[
IMAGE_o] THEN
MATCH_MP_TAC(SET_RULE
`(!x. x
IN s ==> g(f(x)) = x) ==> x
IN IMAGE f s ==> g x
IN s`) THEN
REPEAT STRIP_TAC THEN MATCH_MP_TAC
INTERVAL_BIJ_BIJ THEN
ASM_SIMP_TAC[
FORALL_2; DIMINDEX_2;
VECTOR_NEG_COMPONENT;
VEC_COMPONENT;
ARITH] THEN
CONV_TAC REAL_RAT_REDUCE_CONV);;
let SEGMENT_VERTICAL = prove
(`!a:real^2 b:real^2 x:real^2.
a$1 = b$1
==> (x
IN segment[a,b] <=>
x$1 = a$1 /\ x$1 = b$1 /\
(a$2 <= x$2 /\ x$2 <= b$2 \/ b$2 <= x$2 /\ x$2 <= a$2))`,
let SEGMENT_HORIZONTAL = prove
(`!a:real^2 b:real^2 x:real^2.
a$2 = b$2
==> (x
IN segment[a,b] <=>
x$2 = a$2 /\ x$2 = b$2 /\
(a$1 <= x$1 /\ x$1 <= b$1 \/ b$1 <= x$1 /\ x$1 <= a$1))`,
let FASHODA_INTERLACE = prove
(`!f g a b:real^2.
path f /\ path g /\
path_image f
SUBSET interval[a,b] /\
path_image g
SUBSET interval[a,b] /\
(pathstart f)$2 = a$2 /\ (pathfinish f)$2 = a$2 /\
(pathstart g)$2 = a$2 /\ (pathfinish g)$2 = a$2 /\
(pathstart f)$1 < (pathstart g)$1 /\
(pathstart g)$1 < (pathfinish f)$1 /\
(pathfinish f)$1 < (pathfinish g)$1
==> ?z. z
IN path_image f /\ z
IN path_image g`,
REPEAT STRIP_TAC THEN
SUBGOAL_THEN `~(interval[a:real^2,b] = {})` MP_TAC THENL
[FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
`s
SUBSET t ==> ~(s = {}) ==> ~(t = {})`)) THEN
REWRITE_TAC[
PATH_IMAGE_NONEMPTY];
ALL_TAC] THEN
SUBGOAL_THEN
`pathstart (f:real^1->real^2)
IN interval[a,b] /\
pathfinish f
IN interval[a,b] /\
pathstart g
IN interval[a,b] /\
pathfinish g
IN interval[a,b]`
MP_TAC THENL
[ASM_MESON_TAC[
SUBSET;
PATHSTART_IN_PATH_IMAGE;
PATHFINISH_IN_PATH_IMAGE];
ALL_TAC] THEN
REWRITE_TAC[
INTERVAL_NE_EMPTY;
IN_INTERVAL;
FORALL_2; DIMINDEX_2] THEN
REPEAT STRIP_TAC THEN
MP_TAC(SPECL
[`linepath(vector[a$1 - &2;a$2 - &2],vector[(pathstart f)$1;a$2 - &2]) ++
linepath(vector[(pathstart f)$1;(a:real^2)$2 - &2],pathstart f) ++
(f:real^1->real^2) ++
linepath(pathfinish f,vector[(pathfinish f)$1;a$2 - &2]) ++
linepath(vector[(pathfinish f)$1;a$2 - &2],
vector[(b:real^2)$1 + &2;a$2 - &2])`;
`linepath(vector[(pathstart g)$1; (pathstart g)$2 - &3],pathstart g) ++
(g:real^1->real^2) ++
linepath(pathfinish g,vector[(pathfinish g)$1;(a:real^2)$2 - &1]) ++
linepath(vector[(pathfinish g)$1;a$2 - &1],vector[b$1 + &1;a$2 - &1]) ++
linepath(vector[b$1 + &1;a$2 - &1],vector[(b:real^2)$1 + &1;b$2 + &3])`;
`vector[(a:real^2)$1 - &2; a$2 - &3]:real^2`;
`vector[(b:real^2)$1 + &2; b$2 + &3]:real^2`]
FASHODA) THEN
ASM_SIMP_TAC[
PATH_JOIN;
PATHSTART_JOIN;
PATHFINISH_JOIN;
PATH_IMAGE_JOIN;
PATHSTART_LINEPATH;
PATHFINISH_LINEPATH;
PATH_LINEPATH] THEN
REWRITE_TAC[
VECTOR_2] THEN ANTS_TAC THENL
[CONJ_TAC THEN
REPEAT(MATCH_MP_TAC
(SET_RULE `s
SUBSET u /\ t
SUBSET u ==> (s
UNION t)
SUBSET u`) THEN
CONJ_TAC) THEN
TRY(REWRITE_TAC[
PATH_IMAGE_LINEPATH] THEN
MATCH_MP_TAC(REWRITE_RULE[
CONVEX_CONTAINS_SEGMENT]
(CONJUNCT1 (SPEC_ALL
CONVEX_INTERVAL))) THEN
ASM_REWRITE_TAC[
IN_INTERVAL;
FORALL_2; DIMINDEX_2;
VECTOR_2] THEN
ASM_REAL_ARITH_TAC) THEN
MATCH_MP_TAC
SUBSET_TRANS THEN
EXISTS_TAC `interval[a:real^2,b:real^2]` THEN
ASM_REWRITE_TAC[
SUBSET_REFL] THEN
REWRITE_TAC[
SUBSET_INTERVAL;
FORALL_2; DIMINDEX_2;
VECTOR_2] THEN
ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `z:real^2` THEN
REWRITE_TAC[
PATH_IMAGE_LINEPATH] THEN
SUBGOAL_THEN
`!f s:real^2->bool.
path_image f
UNION s =
path_image f
UNION (s
DIFF {pathstart f,pathfinish f})`
(fun th -> ONCE_REWRITE_TAC[th] THEN
REWRITE_TAC[GSYM
UNION_ASSOC] THEN
ONCE_REWRITE_TAC[SET_RULE `(s
UNION t)
UNION u =
u
UNION t
UNION s`] THEN
ONCE_REWRITE_TAC[th])
THENL
[REWRITE_TAC[
EXTENSION;
IN_UNION;
IN_DIFF;
IN_INSERT;
NOT_IN_EMPTY] THEN
ASM_MESON_TAC[
PATHSTART_IN_PATH_IMAGE;
PATHFINISH_IN_PATH_IMAGE];
ALL_TAC] THEN
REWRITE_TAC[
IN_UNION;
IN_DIFF; GSYM
DISJ_ASSOC;
LEFT_OR_DISTRIB;
RIGHT_OR_DISTRIB; GSYM
CONJ_ASSOC;
SET_RULE `~(z
IN {x,y}) <=> ~(z = x) /\ ~(z = y)`] THEN
DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN MP_TAC) THEN
ASM_SIMP_TAC[
SEGMENT_VERTICAL;
SEGMENT_HORIZONTAL;
VECTOR_2] THEN
REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
UNDISCH_TAC `
path_image (f:real^1->real^2)
SUBSET interval [a,b]` THEN
REWRITE_TAC[
SUBSET] THEN DISCH_THEN(MP_TAC o SPEC `z:real^2`) THEN
UNDISCH_TAC `
path_image (g:real^1->real^2)
SUBSET interval [a,b]` THEN
REWRITE_TAC[
SUBSET] THEN DISCH_THEN(MP_TAC o SPEC `z:real^2`) THEN
ASM_REWRITE_TAC[
IN_INTERVAL;
FORALL_2; DIMINDEX_2] THEN
REPEAT(DISCH_THEN(fun th -> if is_imp(concl th) then ALL_TAC else
ASSUME_TAC th)) THEN
REPEAT(POP_ASSUM MP_TAC) THEN TRY REAL_ARITH_TAC THEN
REWRITE_TAC[
CART_EQ;
FORALL_2; DIMINDEX_2] THEN REAL_ARITH_TAC);;