1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
|
(* ========================================================================= *)
(* Bondy's theorem (first proof from Bollobas's "Combinatorics", page 4). *)
(* ========================================================================= *)
let BONDY = prove
(`!(X:A->bool) f n.
1 <= n /\ X HAS_SIZE n /\ f HAS_SIZE n /\ (!s. s IN f ==> s SUBSET X)
==> ?x. x IN X /\ {s DIFF {x} | s IN f} HAS_SIZE n`,
REPEAT STRIP_TAC THEN
SUBGOAL_THEN
`!m. m <= n - 1
==> ?d:A->bool. d HAS_SIZE m /\ d SUBSET X /\
CARD {s INTER d | s IN f} >= m + 1`
(MP_TAC o SPEC `n - 1`) THEN REWRITE_TAC[GE] THENL
[MATCH_MP_TAC num_INDUCTION THEN CONJ_TAC THENL
[REWRITE_TAC[HAS_SIZE_0; UNWIND_THM2; INTER_EMPTY; EMPTY_SUBSET] THEN
REWRITE_TAC[SIMPLE_IMAGE; IMAGE_CONST; ADD_CLAUSES] THEN
ASM_MESON_TAC[HAS_SIZE; CARD_EQ_0; CARD_SING; LE_REFL];
ALL_TAC] THEN
X_GEN_TAC `m:num` THEN DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
DISCH_THEN(X_CHOOSE_THEN `d:A->bool` STRIP_ASSUME_TAC) THEN
RULE_ASSUM_TAC(REWRITE_RULE[HAS_SIZE]) THEN
FIRST_X_ASSUM(DISJ_CASES_TAC o MATCH_MP (ARITH_RULE
`m + 1 <= n ==> SUC m + 1 <= n \/ n = m + 1`))
THENL
[SUBGOAL_THEN `(d:A->bool) PSUBSET X` MP_TAC THENL
[ASM_MESON_TAC[PSUBSET; ARITH_RULE `SUC m <= n - 1 ==> ~(m = n)`];
ASM_REWRITE_TAC[PSUBSET_ALT]] THEN
DISCH_THEN(X_CHOOSE_THEN `a:A` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `(a:A) INSERT d` THEN
ASM_SIMP_TAC[HAS_SIZE; CARD_CLAUSES; INSERT_SUBSET; FINITE_INSERT] THEN
TRANS_TAC LE_TRANS `CARD {s INTER d:A->bool | s IN f}` THEN
ASM_REWRITE_TAC[] THEN REWRITE_TAC[SIMPLE_IMAGE] THEN
MATCH_MP_TAC CARD_IMAGE_LE2 THEN ASM SET_TAC[];
ALL_TAC] THEN
MP_TAC(ISPECL [`\s:A->bool. s INTER d`; `f:(A->bool)->bool`]
CARD_IMAGE_EQ_INJ) THEN
ASM_SIMP_TAC[GSYM SIMPLE_IMAGE; LEFT_IMP_EXISTS_THM; NOT_FORALL_THM;
ARITH_RULE `SUC m <= n - 1 ==> ~(m + 1 = n)`] THEN
MAP_EVERY X_GEN_TAC [`t:A->bool`; `u:A->bool`] THEN
REWRITE_TAC[NOT_IMP] THEN STRIP_TAC THEN
SUBGOAL_THEN `?e:A. e IN X /\ ~(e IN t <=> e IN u)` STRIP_ASSUME_TAC THENL
[ASM SET_TAC[]; ALL_TAC] THEN
EXISTS_TAC `(e:A) INSERT d` THEN
ASM_SIMP_TAC[HAS_SIZE; CARD_CLAUSES; INSERT_SUBSET; FINITE_INSERT] THEN
CONJ_TAC THENL [COND_CASES_TAC THEN ASM SET_TAC[]; ALL_TAC] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (ARITH_RULE
`x = m + 1 ==> x < y ==> SUC m + 1 <= y`)) THEN
REWRITE_TAC[SIMPLE_IMAGE] THEN MATCH_MP_TAC CARD_IMAGE_LT2 THEN
ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
DISCH_THEN(MP_TAC o SPECL [`t:A->bool`; `u:A->bool`]) THEN ASM SET_TAC[];
ASM_SIMP_TAC[LE_REFL; SUB_ADD] THEN
DISCH_THEN(X_CHOOSE_THEN `d:A->bool` STRIP_ASSUME_TAC) THEN
RULE_ASSUM_TAC(REWRITE_RULE[HAS_SIZE]) THEN
SUBGOAL_THEN `(d:A->bool) PSUBSET X` MP_TAC THENL
[ASM_MESON_TAC[PSUBSET; ARITH_RULE `1 <= n ==> ~(n - 1 = n)`];
ASM_REWRITE_TAC[PSUBSET_ALT]] THEN
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `a:A` THEN STRIP_TAC THEN
SUBGOAL_THEN `d = X DELETE (a:A)` SUBST_ALL_TAC THENL
[ASM_SIMP_TAC[SET_RULE
`a IN X ==> (d = X DELETE a <=> ~(a IN d) /\ a INSERT d = X)`] THEN
MATCH_MP_TAC CARD_SUBSET_EQ THEN
ASM_SIMP_TAC[CARD_CLAUSES; INSERT_SUBSET] THEN ASM_ARITH_TAC;
ASM_SIMP_TAC[HAS_SIZE; SIMPLE_IMAGE; FINITE_IMAGE; GSYM LE_ANTISYM] THEN
CONJ_TAC THENL [ASM_MESON_TAC[CARD_IMAGE_LE]; ALL_TAC] THEN
TRANS_TAC LE_TRANS `CARD {s INTER X DELETE (a:A) | s IN f}` THEN
ASM_REWRITE_TAC[] THEN MATCH_MP_TAC EQ_IMP_LE THEN AP_TERM_TAC THEN
REWRITE_TAC[SIMPLE_IMAGE] THEN MATCH_MP_TAC IMAGE_EQ THEN
ASM SET_TAC[]]]);;
|
