1 (* ========================================================================= *)
2 (* The friendship theorem. *)
4 (* Proof from "Combinatorics Tutorial 2: Friendship Theorem", copyright *)
5 (* MathOlymp.com, 2001. Apparently due to J. Q. Longyear and T. D. Parsons. *)
6 (* ========================================================================= *)
8 needs "Library/prime.ml";;
9 needs "Library/pocklington.ml";;
11 (* ------------------------------------------------------------------------- *)
12 (* Useful inductive breakdown principle ending at gcd. *)
13 (* ------------------------------------------------------------------------- *)
15 let GCD_INDUCT = prove
16 (`!P. (!m n. P m /\ P (m + n) ==> P n)
17 ==> !m n. P m /\ P n ==> P (gcd(m,n))`,
18 GEN_TAC THEN STRIP_TAC THEN REPEAT GEN_TAC THEN
19 WF_INDUCT_TAC `m + n:num` THEN REPEAT(POP_ASSUM MP_TAC) THEN
20 MAP_EVERY (fun t -> SPEC_TAC(t,t)) [`n:num`; `m:num`] THEN
21 MATCH_MP_TAC WLOG_LE THEN CONJ_TAC THENL
22 [REWRITE_TAC[CONJ_ACI; GCD_SYM; ADD_SYM]; REPEAT STRIP_TAC] THEN
23 ASM_CASES_TAC `m = 0` THENL [ASM_MESON_TAC[GCD_0]; ALL_TAC] THEN
24 UNDISCH_TAC `!m n:num. P m /\ P (m + n) ==> P n` THEN
25 DISCH_THEN(MP_TAC o SPECL [`m:num`; `n - m:num`]) THEN
26 ONCE_REWRITE_TAC[ADD_SYM] THEN ASM_SIMP_TAC[SUB_ADD; LT_IMP_LE] THEN
27 DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPECL [`m:num`; `n - m:num`]) THEN
28 REWRITE_TAC[IMP_IMP] THEN ANTS_TAC THENL
29 [ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC;
31 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [LE_EXISTS]) THEN
32 DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST_ALL_TAC) THEN
33 REWRITE_TAC[ADD_SUB2; GCD_ADD]);;
35 (* ------------------------------------------------------------------------- *)
36 (* General theorems about loops in a sequence. *)
37 (* ------------------------------------------------------------------------- *)
40 (`!x m n. (!i. x(i + m) = x(i)) /\ (!i. x(i + n) = x(i))
41 ==> !i. x(i + gcd(m,n)) = x(i)`,
42 GEN_TAC THEN MATCH_MP_TAC GCD_INDUCT THEN MESON_TAC[ADD_AC]);;
44 let LOOP_COPRIME = prove
45 (`!x m n. (!i. x(i + m) = x(i)) /\ (!i. x(i + n) = x(i)) /\ coprime(m,n)
47 REPEAT GEN_TAC THEN STRIP_TAC THEN INDUCT_TAC THEN REWRITE_TAC[ADD1] THEN
48 ASM_MESON_TAC[LOOP_GCD; COPRIME_GCD]);;
50 (* ------------------------------------------------------------------------- *)
51 (* General theorem about partition into equally-sized eqv classes. *)
52 (* ------------------------------------------------------------------------- *)
54 let EQUIVALENCE_UNIFORM_PARTITION = prove
56 (!x. x IN s ==> R x x) /\
57 (!x y. R x y ==> R y x) /\
58 (!x y z. R x y /\ R y z ==> R x z) /\
59 (!x:A. x IN s ==> CARD {y | y IN s /\ R x y} = k)
60 ==> k divides (CARD s)`,
62 WF_INDUCT_TAC `CARD(s:A->bool)` THEN
63 ASM_CASES_TAC `s:A->bool = {}` THENL
64 [ASM_MESON_TAC[CARD_CLAUSES; DIVIDES_0]; REPEAT STRIP_TAC] THEN
65 FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
66 DISCH_THEN(X_CHOOSE_TAC `a:A`) THEN
67 FIRST_X_ASSUM(MP_TAC o SPEC `{y:A | y IN s /\ ~(R (a:A) y)}`) THEN
68 REWRITE_TAC[IMP_IMP] THEN ANTS_TAC THENL
69 [ASM_SIMP_TAC[IN_ELIM_THM; FINITE_RESTRICT] THEN ASM_REWRITE_TAC[] THEN
71 [MATCH_MP_TAC CARD_PSUBSET THEN
72 ASM_SIMP_TAC[PSUBSET; SUBSET; EXTENSION; IN_ELIM_THM] THEN
74 GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN
75 DISCH_THEN(CONJUNCTS_THEN2 (ANTE_RES_THEN MP_TAC) ASSUME_TAC) THEN
76 DISCH_TAC THEN MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN AP_TERM_TAC THEN
77 AP_TERM_TAC THEN ASM SET_TAC[]];
80 SUBGOAL_THEN `CARD(s) = CARD {y | y IN s /\ (R:A->A->bool) a y} +
81 CARD {y | y IN s /\ ~(R a y)}`
82 (fun th -> ASM_SIMP_TAC[th; DIVIDES_ADD; DIVIDES_REFL]) THEN
83 CONV_TAC SYM_CONV THEN MATCH_MP_TAC CARD_UNION_EQ THEN ASM SET_TAC[]);;
85 (* ------------------------------------------------------------------------- *)
86 (* With explicit restricted quantification. *)
87 (* ------------------------------------------------------------------------- *)
89 let EQUIVALENCE_UNIFORM_PARTITION_RESTRICT = prove
91 (!x. x IN s ==> R x x) /\
92 (!x y. x IN s /\ y IN s /\ R x y ==> R y x) /\
93 (!x y z. x IN s /\ y IN s /\ z IN s /\ R x y /\ R y z ==> R x z) /\
94 (!x:A. x IN s ==> CARD {y | y IN s /\ R x y} = k)
95 ==> k divides (CARD s)`,
96 REPEAT STRIP_TAC THEN MATCH_MP_TAC EQUIVALENCE_UNIFORM_PARTITION THEN
97 EXISTS_TAC `\x y:A. x IN s /\ y IN s /\ R x y` THEN
98 SIMP_TAC[] THEN ASM_REWRITE_TAC[CONJ_ASSOC] THEN ASM_MESON_TAC[]);;
100 (* ------------------------------------------------------------------------- *)
101 (* General theorem about pairing up elements of a set. *)
102 (* ------------------------------------------------------------------------- *)
104 let ELEMENTS_PAIR_UP = prove
106 (!x. x IN s ==> ~(r x x)) /\
107 (!x y. x IN s /\ y IN s /\ r x y ==> r y x) /\
108 (!x:A. x IN s ==> ?!y. y IN s /\ r x y)
110 REPEAT GEN_TAC THEN WF_INDUCT_TAC `CARD(s:A->bool)` THEN
111 STRIP_TAC THEN ASM_CASES_TAC `s:A->bool = {}` THEN
112 ASM_REWRITE_TAC[CARD_CLAUSES; ARITH] THEN
113 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
114 DISCH_THEN(X_CHOOSE_TAC `a:A`) THEN
115 MP_TAC(ASSUME `!x:A. x IN s ==> (?!y:A. y IN s /\ r x y)`) THEN
116 DISCH_THEN(MP_TAC o SPEC `a:A`) THEN REWRITE_TAC[ASSUME `a:A IN s`] THEN
117 DISCH_THEN(MP_TAC o EXISTENCE) THEN
118 DISCH_THEN(X_CHOOSE_THEN `b:A` STRIP_ASSUME_TAC) THEN
119 FIRST_X_ASSUM(MP_TAC o SPEC `s DELETE (a:A) DELETE b`) THEN
120 REWRITE_TAC[IMP_IMP] THEN ANTS_TAC THENL
123 SUBGOAL_THEN `s = (a:A) INSERT b INSERT (s DELETE a DELETE b)`
124 SUBST1_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
125 ASM_SIMP_TAC[CARD_CLAUSES; FINITE_DELETE; FINITE_INSERT] THEN
126 REWRITE_TAC[IN_INSERT; IN_DELETE] THEN ASM_MESON_TAC[EVEN]] THEN
127 ASM_SIMP_TAC[FINITE_DELETE; IN_DELETE] THEN CONJ_TAC THENL
128 [MATCH_MP_TAC CARD_PSUBSET THEN ASM SET_TAC[]; ALL_TAC] THEN
129 X_GEN_TAC `x:A` THEN STRIP_TAC THEN
130 MP_TAC(ASSUME `!x:A. x IN s ==> (?!y. y IN s /\ r x y)`) THEN
131 DISCH_THEN(MP_TAC o SPEC `x:A`) THEN REWRITE_TAC[ASSUME `x:A IN s`] THEN
132 MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN
133 X_GEN_TAC `y:A` THEN EQ_TAC THEN SIMP_TAC[] THEN ASM_MESON_TAC[]);;
135 (* ------------------------------------------------------------------------- *)
136 (* Cycles and paths. *)
137 (* ------------------------------------------------------------------------- *)
139 let cycle = new_definition
140 `cycle r k x <=> (!i. r (x i) (x(i + 1))) /\ (!i. x(i + k) = x(i))`;;
142 let path = new_definition
143 `path r k x <=> (!i. i < k ==> r (x i) (x(i + 1))) /\
144 (!i. k < i ==> x(i) = @x. T)`;;
146 (* ------------------------------------------------------------------------- *)
147 (* Lemmas about these concepts. *)
148 (* ------------------------------------------------------------------------- *)
150 let CYCLE_OFFSET = prove
151 (`!r k x:num->A. cycle r k x ==> !i m. x(m * k + i) = x(i)`,
152 REPEAT GEN_TAC THEN REWRITE_TAC[cycle] THEN STRIP_TAC THEN GEN_TAC THEN
153 INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES] THEN
154 ASM_MESON_TAC[ADD_AC]);;
156 let CYCLE_MOD = prove
157 (`!r k x:num->A. cycle r k x /\ ~(k = 0) ==> !i. x(i MOD k) = x(i)`,
158 MESON_TAC[CYCLE_OFFSET; DIVISION]);;
160 let PATHS_MONO = prove
161 (`(!x y. r x y ==> s x y) ==> {x | path r k x} SUBSET {x | path s k x}`,
162 REWRITE_TAC[path; IN_ELIM_THM; SUBSET] THEN MESON_TAC[]);;
164 let HAS_SIZE_PATHS = prove
165 (`!N m r k. (:A) HAS_SIZE N /\ (!x. {y | r x y} HAS_SIZE m)
166 ==> {x:num->A | path r k x} HAS_SIZE (N * m EXP k)`,
167 REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
168 INDUCT_TAC THEN REWRITE_TAC[EXP; MULT_CLAUSES] THENL
169 [SUBGOAL_THEN `{x:num->A | path r 0 x} =
170 IMAGE (\a i. if i = 0 then a else @x. T) (:A)`
172 [REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_IMAGE; IN_UNIV; path; LT] THEN
173 REWRITE_TAC[FUN_EQ_THM; LT_NZ] THEN MESON_TAC[];
175 MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN ASM_REWRITE_TAC[IN_UNIV] THEN
176 REWRITE_TAC[FUN_EQ_THM] THEN MESON_TAC[];
179 `{x:num->A | path r (SUC k) x} =
180 IMAGE (\(x,a) i. if i = SUC k then a else x i)
181 {x,a | x IN {x | path r k x} /\ a IN {u | r (x k) u}}`
183 [REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_IMAGE; EXISTS_PAIR_THM] THEN
184 X_GEN_TAC `x:num->A` THEN REWRITE_TAC[PAIR_EQ] THEN
185 ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ c /\ d <=> c /\ d /\ a /\ b`] THEN
186 REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
187 REWRITE_TAC[FUN_EQ_THM; path; LT] THEN EQ_TAC THENL
188 [STRIP_TAC THEN EXISTS_TAC `\i. if i = SUC k then @x. T else x(i):A` THEN
189 EXISTS_TAC `x(SUC k):A` THEN SIMP_TAC[] THEN
190 CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN
191 SIMP_TAC[ARITH_RULE `~(k = SUC k) /\ (i < k ==> ~(i = SUC k))`] THEN
192 ASM_SIMP_TAC[ADD1; ARITH_RULE `i < k ==> ~(i + 1 = SUC k)`] THEN
193 ASM_MESON_TAC[ARITH_RULE `k < i /\ ~(i = k + 1) ==> SUC k < i`];
195 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
196 MAP_EVERY X_GEN_TAC [`z:num->A`; `a:A`] THEN STRIP_TAC THEN
197 ASM_REWRITE_TAC[] THEN
198 SIMP_TAC[ARITH_RULE `i = k \/ i < k ==> ~(i = SUC k)`] THEN
199 REWRITE_TAC[ARITH_RULE `i + 1 = SUC k <=> i = k`] THEN
200 ASM_MESON_TAC[ARITH_RULE `SUC k < i ==> ~(i = SUC k) /\ k < i`];
202 ONCE_REWRITE_TAC[ARITH_RULE `N * m * m EXP k = (N * m EXP k) * m`] THEN
203 MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN CONJ_TAC THENL
204 [REWRITE_TAC[FORALL_PAIR_THM; IN_ELIM_PAIR_THM; IN_ELIM_THM] THEN
205 REWRITE_TAC[FUN_EQ_THM; path; PAIR_EQ] THEN REPEAT GEN_TAC THEN
206 STRIP_TAC THEN CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
207 X_GEN_TAC `i:num` THEN ASM_CASES_TAC `i = SUC k` THEN
208 ASM_MESON_TAC[ARITH_RULE `k < SUC k`];
210 ASM_SIMP_TAC[HAS_SIZE_PRODUCT_DEPENDENT]);;
212 let FINITE_PATHS = prove
213 (`!r k. FINITE(:A) ==> FINITE {x:num->A | path r k x}`,
214 REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN
215 EXISTS_TAC `{x:num->A | path (\a b. T) k x}` THEN SIMP_TAC[PATHS_MONO] THEN
216 MP_TAC(ISPECL [`CARD(:A)`; `CARD(:A)`; `\a:A b:A. T`; `k:num`]
218 ANTS_TAC THEN ASM_SIMP_TAC[HAS_SIZE; SET_RULE `{y | T} = (:A)`]);;
220 let HAS_SIZE_CYCLES = prove
221 (`!r k. FINITE(:A) /\ ~(k = 0)
222 ==> {x:num->A | cycle r k x} HAS_SIZE
223 CARD{x:num->A | path r k x /\ x(k) = x(0)}`,
224 REPEAT STRIP_TAC THEN
226 `{x:num->A | cycle r k x} =
227 IMAGE (\x i. x(i MOD k)) {x | path r k x /\ x(k) = x(0)}`
229 [REWRITE_TAC[EXTENSION; IN_IMAGE; IN_ELIM_THM] THEN
230 X_GEN_TAC `x:num->A` THEN EQ_TAC THENL
232 EXISTS_TAC `\i. if i <= k then x(i):A else @x. T` THEN
233 REPEAT CONJ_TAC THENL
234 [ASM_SIMP_TAC[FUN_EQ_THM; LT_IMP_LE; DIVISION] THEN
235 ASM_MESON_TAC[CYCLE_MOD];
236 SIMP_TAC[path; LT_IMP_LE] THEN REWRITE_TAC[GSYM NOT_LT] THEN
237 SIMP_TAC[ARITH_RULE `i < k ==> ~(k < i + 1)`] THEN
238 ASM_MESON_TAC[cycle];
239 REWRITE_TAC[LE_0; LE_REFL] THEN ASM_MESON_TAC[cycle; ADD_CLAUSES]];
240 REWRITE_TAC[LEFT_AND_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN
241 X_GEN_TAC `y:num->A` THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
242 REWRITE_TAC[cycle] THEN CONJ_TAC THEN X_GEN_TAC `i:num` THENL
244 AP_TERM_TAC THEN MATCH_MP_TAC MOD_EQ THEN EXISTS_TAC `1` THEN
245 REWRITE_TAC[MULT_CLAUSES]] THEN
246 SUBGOAL_THEN `y((i + 1) MOD k):A = y(i MOD k + 1)` SUBST1_TAC THENL
247 [ALL_TAC; ASM_MESON_TAC[path; DIVISION]] THEN
248 SUBGOAL_THEN `(i + 1) MOD k = (i MOD k + 1) MOD k` SUBST1_TAC THENL
249 [MATCH_MP_TAC MOD_EQ THEN EXISTS_TAC `i DIV k` THEN
250 REWRITE_TAC[ARITH_RULE `i + 1 = (m + 1) + ik <=> i = ik + m`] THEN
251 ASM_MESON_TAC[DIVISION];
253 FIRST_ASSUM(MP_TAC o CONJUNCT2 o SPEC `i:num` o MATCH_MP DIVISION) THEN
254 SPEC_TAC(`i MOD k`,`j:num`) THEN GEN_TAC THEN
255 ONCE_REWRITE_TAC[ARITH_RULE `j < k <=> j + 1 < k \/ j + 1 = k`] THEN
256 STRIP_TAC THEN ASM_SIMP_TAC[MOD_LT] THEN AP_TERM_TAC THEN
257 MATCH_MP_TAC MOD_UNIQ THEN EXISTS_TAC `1` THEN
258 UNDISCH_TAC `~(k = 0)` THEN ARITH_TAC];
260 MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN CONJ_TAC THENL
262 REWRITE_TAC[HAS_SIZE] THEN MATCH_MP_TAC FINITE_SUBSET THEN
263 EXISTS_TAC `{x:num->A | path r k x}` THEN
264 ASM_SIMP_TAC[FINITE_PATHS] THEN SET_TAC[]] THEN
265 MAP_EVERY X_GEN_TAC [`x:num->A`; `y:num->A`] THEN SIMP_TAC[IN_ELIM_THM] THEN
266 REWRITE_TAC[path; FUN_EQ_THM] THEN STRIP_TAC THEN X_GEN_TAC `i:num` THEN
267 REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
268 (SPECL [`i:num`; `k:num`] LT_CASES)
269 THENL [ASM_MESON_TAC[MOD_LT]; ASM_MESON_TAC[]; ASM_REWRITE_TAC[]] THEN
270 ASM_MESON_TAC[MOD_0]);;
272 let FINITE_CYCLES = prove
273 (`!r k. FINITE(:A) /\ ~(k = 0) ==> FINITE {x:num->A | cycle r k x}`,
274 MESON_TAC[HAS_SIZE_CYCLES; HAS_SIZE]);;
276 let CARD_PATHCYCLES_STEP = prove
278 (:A) HAS_SIZE N /\ ~(k = 0) /\ ~(m = 0) /\
279 (!x:A. {y | r x y} HAS_SIZE m) /\
280 (!x y. r x y ==> r y x) /\
281 (!x y. ~(x = y) ==> ?!z. r x z /\ r z y)
282 ==> {x | path r (k + 2) x /\ x(k + 2) = x(0)} HAS_SIZE
283 (m * CARD {x | path r k x /\ x(k) = x(0)} +
284 CARD {x | path r (k) x /\ ~(x(k) = x(0))})`,
285 REPEAT STRIP_TAC THEN
287 `{x | path r (k + 2) x /\ x(k + 2) = x(0)} =
288 {x | path r (k + 2) x /\ x k = x 0 /\ x(k + 2) = x(0)} UNION
289 {x | path r (k + 2) x /\ ~(x k = x 0) /\ x(k + 2) = x(0)}`] THEN
290 MATCH_MP_TAC HAS_SIZE_UNION THEN GEN_REWRITE_TAC I [CONJ_ASSOC] THEN
291 CONJ_TAC THENL [ALL_TAC; SET_TAC[]] THEN CONJ_TAC THENL
293 `{x:num->A | path r (k + 2) x /\ x k = x 0 /\ x (k + 2) = x 0} =
294 IMAGE (\(x,a) i. if i = k + 1 then a
295 else if i = k + 2 then x(0)
297 {x,a | x IN {x | path r k x /\ x(k) = x(0)} /\
298 a IN {u | r (x k) u}}`
301 MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN CONJ_TAC THENL
302 [REWRITE_TAC[FORALL_PAIR_THM; IN_ELIM_PAIR_THM] THEN
303 REWRITE_TAC[IN_ELIM_THM; FUN_EQ_THM; PAIR_EQ] THEN
304 MAP_EVERY X_GEN_TAC [`y:num->A`; `a:A`; `z:num->A`; `b:A`] THEN
305 DISCH_THEN(fun th -> CONJ_TAC THEN MP_TAC th THENL
306 [ALL_TAC; MESON_TAC[]]) THEN
307 REPEAT(DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC)) THEN
308 DISCH_THEN(fun th -> X_GEN_TAC `i:num` THEN MP_TAC th) THEN
309 DISCH_THEN(fun th -> MP_TAC th THEN MP_TAC(SPEC `0` th)) THEN
310 REWRITE_TAC[ARITH_RULE `~(0 = k + 1) /\ ~(0 = k + 2)`] THEN
311 DISCH_TAC THEN ASM_CASES_TAC `k:num < i` THENL
312 [ASM_MESON_TAC[path]; ALL_TAC] THEN
313 DISCH_THEN(MP_TAC o SPEC `i:num`) THEN
314 ASM_MESON_TAC[ARITH_RULE `k < k + 1 /\ k < k + 2`];
316 ONCE_REWRITE_TAC[MULT_SYM] THEN
317 MATCH_MP_TAC HAS_SIZE_PRODUCT_DEPENDENT THEN
318 ASM_REWRITE_TAC[] THEN REWRITE_TAC[HAS_SIZE] THEN
319 MATCH_MP_TAC FINITE_SUBSET THEN
320 EXISTS_TAC `{x:num->A | path r k x}` THEN CONJ_TAC THENL
321 [ALL_TAC; SET_TAC[]] THEN
322 ASM_MESON_TAC[HAS_SIZE; FINITE_PATHS]] THEN
323 REWRITE_TAC[EXTENSION; IN_IMAGE] THEN
324 REWRITE_TAC[EXISTS_PAIR_THM; IN_ELIM_PAIR_THM] THEN
325 REWRITE_TAC[FUN_EQ_THM; IN_ELIM_THM] THEN
326 X_GEN_TAC `x:num->A` THEN EQ_TAC THENL
328 EXISTS_TAC `\i. if i <= k then x(i):A else @x. T` THEN
329 EXISTS_TAC `(x:num->A) (k + 1)` THEN
330 REWRITE_TAC[IN_ELIM_THM; LE_REFL; LE_0] THEN
331 ASM_REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL
332 [ALL_TAC; ASM_MESON_TAC[path; ARITH_RULE `k < k + 2`]] THEN
335 UNDISCH_TAC `path r (k + 2) (x:num->A)` THEN
336 SIMP_TAC[path; LT_IMP_LE; ARITH_RULE `i < k ==> i + 1 <= k`] THEN
337 SIMP_TAC[GSYM NOT_LT] THEN
338 MESON_TAC[ARITH_RULE `i < k ==> i < k + 2`]] THEN
339 X_GEN_TAC `i:num` THEN
340 ASM_CASES_TAC `i = k + 1` THEN ASM_REWRITE_TAC[] THEN
341 ASM_CASES_TAC `i = k + 2` THEN ASM_REWRITE_TAC[] THEN
342 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [path]) THEN
343 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
344 DISCH_THEN(MP_TAC o SPEC `i:num` o CONJUNCT2) THEN
345 ASM_REWRITE_TAC[ARITH_RULE
346 `k + 2 < i <=> ~(i <= k) /\ ~(i = k + 1) /\ ~(i = k + 2)`];
348 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
349 MAP_EVERY X_GEN_TAC [`z:num->A`; `b:A`] THEN
350 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN
351 DISCH_THEN(fun th -> MP_TAC th THEN MP_TAC(SPEC `0` th)) THEN
352 REWRITE_TAC[COND_ID; ARITH_RULE `~(0 = k + 1)`] THEN DISCH_TAC THEN
353 REWRITE_TAC[CONJ_ASSOC] THEN DISCH_THEN(LABEL_TAC "*") THEN CONJ_TAC THENL
354 [ALL_TAC; REMOVE_THEN "*" (MP_TAC o SPEC `k + 2`) THEN
355 ASM_REWRITE_TAC[ARITH_RULE `~(k + 2 = k + 1)`]] THEN
357 [ALL_TAC; REMOVE_THEN "*" (MP_TAC o SPEC `k:num`) THEN
358 ASM_REWRITE_TAC[ARITH_RULE `~(k = k + 2) /\ ~(k = k + 1)`]] THEN
359 UNDISCH_TAC `path r k (z:num->A)` THEN ASM_REWRITE_TAC[path] THEN
361 `k + 2 < i ==> k < i /\ ~(i = k + 1) /\ ~(i = k + 2)`] THEN
362 STRIP_TAC THEN X_GEN_TAC `i:num` THEN DISCH_TAC THEN
363 ASM_SIMP_TAC[ARITH_RULE `i < k + 2 ==> ~(i = k + 2)`] THEN
364 REWRITE_TAC[ARITH_RULE `i + 1 = k + 2 <=> i = k + 1`] THEN
365 ASM_CASES_TAC `i = k + 1` THEN ASM_REWRITE_TAC[] THENL
366 [ASM_MESON_TAC[ARITH_RULE `~(x + 1 = x)`]; ALL_TAC] THEN
367 REWRITE_TAC[EQ_ADD_RCANCEL] THEN COND_CASES_TAC THEN ASM_SIMP_TAC[] THENL
368 [ASM_MESON_TAC[]; ALL_TAC] THEN
369 ASM_MESON_TAC[ARITH_RULE `i < k + 2 /\ ~(i = k) /\ ~(i = k + 1)
373 `{x:num->A | path r (k + 2) x /\ ~(x k = x 0) /\ x (k + 2) = x 0} =
374 IMAGE (\x i. if i = k + 1 then @z. r (x k) z /\ r z (x 0)
375 else if i = k + 2 then x(0)
377 {x | path r k x /\ ~(x(k) = x(0))}`
380 MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN CONJ_TAC THENL
382 REWRITE_TAC[HAS_SIZE] THEN
383 MATCH_MP_TAC FINITE_SUBSET THEN
384 EXISTS_TAC `{x:num->A | path r k x}` THEN CONJ_TAC THENL
385 [ALL_TAC; SET_TAC[]] THEN
386 ASM_MESON_TAC[HAS_SIZE; FINITE_PATHS]] THEN
387 MAP_EVERY X_GEN_TAC [`x:num->A`; `y:num->A`] THEN
388 REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN
389 REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `i:num` THEN
390 ASM_CASES_TAC `k:num < i` THENL
391 [ASM_MESON_TAC[path]; ALL_TAC] THEN
392 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [FUN_EQ_THM]) THEN
393 DISCH_THEN(MP_TAC o SPEC `i:num`) THEN
394 ASM_MESON_TAC[ARITH_RULE `k < k + 1 /\ k < k + 2`]] THEN
395 REWRITE_TAC[EXTENSION; IN_IMAGE; IN_ELIM_THM] THEN
396 X_GEN_TAC `x:num->A` THEN REWRITE_TAC[IN_ELIM_THM] THEN EQ_TAC THENL
398 EXISTS_TAC `\i. if i <= k then x(i):A else @x. T` THEN
399 ASM_REWRITE_TAC[LE_REFL; LE_0] THEN CONJ_TAC THENL
401 UNDISCH_TAC `path r (k + 2) (x:num->A)` THEN
402 SIMP_TAC[path; LT_IMP_LE; ARITH_RULE `i < k ==> i + 1 <= k`] THEN
403 SIMP_TAC[GSYM NOT_LT] THEN
404 MESON_TAC[ARITH_RULE `i < k ==> i < k + 2`]] THEN
405 REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `i:num` THEN
406 ASM_CASES_TAC `i = k + 1` THEN ASM_REWRITE_TAC[] THENL
407 [CONV_TAC SYM_CONV THEN MATCH_MP_TAC SELECT_UNIQUE THEN
408 UNDISCH_TAC `path r (k + 2) (x:num->A)` THEN REWRITE_TAC[path] THEN
409 DISCH_THEN(MP_TAC o CONJUNCT1) THEN
410 DISCH_THEN(fun th -> MP_TAC(SPEC `k:num` th) THEN
411 MP_TAC(SPEC `k + 1` th)) THEN
412 REWRITE_TAC[ARITH_RULE `k < k + 2 /\ k + 1 < k + 2`] THEN
413 REWRITE_TAC[GSYM ADD_ASSOC; ARITH] THEN ASM_MESON_TAC[];
415 ASM_CASES_TAC `i = k + 2` THEN ASM_REWRITE_TAC[] THEN
416 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
417 UNDISCH_TAC `path r (k + 2) (x:num->A)` THEN REWRITE_TAC[path] THEN
418 DISCH_THEN(MP_TAC o CONJUNCT2) THEN
419 ASM_MESON_TAC[ARITH_RULE `~(i <= k) /\ ~(i = k + 1) /\ ~(i = k + 2)
422 DISCH_THEN(X_CHOOSE_THEN `y:num->A` STRIP_ASSUME_TAC) THEN
423 ASM_REWRITE_TAC[ARITH_RULE
424 `~(k + 2 = k + 1) /\ ~(0 = k + 1) /\ ~(0 = k + 2) /\ ~(k = k + 1) /\
426 REWRITE_TAC[path] THEN CONJ_TAC THEN X_GEN_TAC `i:num` THEN DISCH_TAC THENL
427 [REWRITE_TAC[ARITH_RULE `i + 1 = k + 2 <=> i = k + 1`] THEN
428 ASM_CASES_TAC `i = k + 1` THEN ASM_REWRITE_TAC[] THENL
429 [REWRITE_TAC[ARITH_RULE `(k + 1) + 1 = k + 1 <=> F`] THEN ASM_MESON_TAC[];
431 ASM_SIMP_TAC[ARITH_RULE `i < k + 2 ==> ~(i = k + 2)`] THEN
432 REWRITE_TAC[EQ_ADD_RCANCEL] THEN COND_CASES_TAC THEN ASM_SIMP_TAC[] THENL
433 [ASM_MESON_TAC[]; ALL_TAC] THEN
434 UNDISCH_TAC `path r k (y:num->A)` THEN REWRITE_TAC[path] THEN
435 DISCH_THEN(MATCH_MP_TAC o CONJUNCT1) THEN
436 MAP_EVERY UNDISCH_TAC [`~(i:num = k)`; `~(i = k + 1)`; `i < k + 2`] THEN
439 ASM_SIMP_TAC[ARITH_RULE `k + 2 < i ==> ~(i = k + 1) /\ ~(i = k + 2)`] THEN
440 ASM_MESON_TAC[path; ARITH_RULE `k + 2 < i ==> k < i`]);;
442 (* ------------------------------------------------------------------------- *)
443 (* The first lemma about the number of cycles. *)
444 (* ------------------------------------------------------------------------- *)
446 let shiftable = new_definition
447 `shiftable x y <=> ?k. !i. x(i) = y(i + k)`;;
449 let SHIFTABLE_REFL = prove
450 (`!x. shiftable x x`,
451 REWRITE_TAC[shiftable] THEN MESON_TAC[ADD_CLAUSES]);;
453 let SHIFTABLE_TRANS = prove
454 (`!x y z. shiftable x y /\ shiftable y z ==> shiftable x z`,
455 REWRITE_TAC[shiftable] THEN MESON_TAC[ADD_ASSOC]);;
457 let SHIFTABLE_LOCAL = prove
458 (`!x y p r. cycle r p x /\ cycle r p y /\ ~(p = 0)
459 ==> (shiftable x y <=> ?k. k < p /\ !i. x(i) = y(i + k))`,
460 REPEAT STRIP_TAC THEN REWRITE_TAC[shiftable] THEN
461 EQ_TAC THENL [ALL_TAC; MESON_TAC[]] THEN
462 DISCH_THEN(X_CHOOSE_TAC `k:num`) THEN EXISTS_TAC `k MOD p` THEN
463 FIRST_ASSUM(MP_TAC o SPEC `k:num` o MATCH_MP DIVISION) THEN
464 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN ASM_REWRITE_TAC[] THEN
465 DISCH_THEN(fun th -> GEN_REWRITE_TAC
466 (BINDER_CONV o LAND_CONV o ONCE_DEPTH_CONV) [th]) THEN
467 ASM_MESON_TAC[CYCLE_OFFSET; ADD_AC]);;
469 let SHIFTABLE_SYM = prove
470 (`!x y p r. cycle r p x /\ cycle r p y /\ ~(p = 0) /\ shiftable x y
473 ONCE_REWRITE_TAC[TAUT `a /\ b /\ c /\ d <=> (a /\ b /\ c) /\ d`] THEN
474 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
475 FIRST_ASSUM(SUBST1_TAC o MATCH_MP SHIFTABLE_LOCAL) THEN
476 DISCH_THEN(X_CHOOSE_THEN `k:num` STRIP_ASSUME_TAC) THEN
477 REWRITE_TAC[shiftable] THEN EXISTS_TAC `p - k:num` THEN
478 ASM_SIMP_TAC[ARITH_RULE `k < p ==> (i + (p - k)) + k = i + p:num`] THEN
479 ASM_MESON_TAC[cycle]);;
481 let CYCLES_PRIME_LEMMA = prove
482 (`!r p x. FINITE(:A) /\ prime p /\ (!x. ~(r x x))
483 ==> p divides CARD {x:num->A | cycle r p x}`,
484 REPEAT GEN_TAC THEN ASM_CASES_TAC `p = 0` THEN ASM_REWRITE_TAC[PRIME_0] THEN
485 STRIP_TAC THEN MATCH_MP_TAC EQUIVALENCE_UNIFORM_PARTITION_RESTRICT THEN
486 EXISTS_TAC `shiftable:(num->A)->(num->A)->bool` THEN
487 ASM_SIMP_TAC[IN_ELIM_THM; FINITE_CYCLES] THEN
488 CONJ_TAC THENL [MESON_TAC[SHIFTABLE_REFL]; ALL_TAC] THEN
489 CONJ_TAC THENL [ASM_MESON_TAC[SHIFTABLE_SYM]; ALL_TAC] THEN
490 CONJ_TAC THENL [MESON_TAC[SHIFTABLE_TRANS]; ALL_TAC] THEN
491 X_GEN_TAC `x:num->A` THEN DISCH_TAC THEN
492 SUBGOAL_THEN `{y:num->A | cycle r p y /\ shiftable x y} HAS_SIZE p`
493 (fun th -> MESON_TAC[HAS_SIZE; th]) THEN
494 SUBGOAL_THEN `{y:num->A | cycle r p y /\ shiftable x y} =
495 IMAGE (\k i. x(i + k)) {k | k < p}`
497 [REWRITE_TAC[EXTENSION; IN_IMAGE; IN_ELIM_THM] THEN
498 X_GEN_TAC `y:num->A` THEN REWRITE_TAC[FUN_EQ_THM] THEN EQ_TAC THENL
499 [ASM_MESON_TAC[SHIFTABLE_LOCAL; SHIFTABLE_SYM]; ALL_TAC] THEN
500 REPEAT STRIP_TAC THENL
501 [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [cycle]) THEN
502 ASM_REWRITE_TAC[cycle] THEN MESON_TAC[ADD_AC];
504 MATCH_MP_TAC SHIFTABLE_SYM THEN
505 MAP_EVERY EXISTS_TAC [`p:num`; `r:A->A->bool`] THEN
506 ASM_REWRITE_TAC[] THEN
507 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [cycle]) THEN
508 ASM_REWRITE_TAC[cycle; shiftable] THEN MESON_TAC[ADD_AC];
510 MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN REWRITE_TAC[HAS_SIZE_NUMSEG_LT] THEN
511 REWRITE_TAC[IN_ELIM_THM] THEN MATCH_MP_TAC WLOG_LE THEN
512 REWRITE_TAC[FUN_EQ_THM] THEN CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN
513 MAP_EVERY X_GEN_TAC [`k:num`; `l:num`] THEN REPEAT STRIP_TAC THEN
514 MATCH_MP_TAC(TAUT `(~p ==> F) ==> p`) THEN DISCH_TAC THEN
515 SUBGOAL_THEN `!i. x(i):A = x(0)` MP_TAC THENL
516 [ALL_TAC; ASM_MESON_TAC[cycle]] THEN
517 MATCH_MP_TAC LOOP_COPRIME THEN EXISTS_TAC `p:num` THEN
518 REWRITE_TAC[RIGHT_EXISTS_AND_THM] THEN
519 CONJ_TAC THENL [ASM_MESON_TAC[cycle]; ALL_TAC] THEN
520 EXISTS_TAC `l + (p - k):num` THEN CONJ_TAC THENL
521 [X_GEN_TAC `i:num` THEN
522 ONCE_REWRITE_TAC[ARITH_RULE `i + l + pk = (i + pk) + l:num`] THEN
523 ASSUM_LIST(REWRITE_TAC o map GSYM) THEN
524 SIMP_TAC[ARITH_RULE `k < p ==> (i + p - k) + k = i + p:num`;
525 ASSUME `k < p:num`] THEN
526 ASM_MESON_TAC[cycle];
528 SUBGOAL_THEN `l + p - k = p + l - k:num` SUBST1_TAC THENL
529 [MAP_EVERY UNDISCH_TAC [`k < p:num`; `k <= l:num`] THEN ARITH_TAC;
531 REWRITE_TAC[NUMBER_RULE `coprime(p,p + d) <=> coprime(d,p)`] THEN
532 MATCH_MP_TAC PRIME_COPRIME_LT THEN
533 ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC);;
535 (* ------------------------------------------------------------------------- *)
536 (* The theorem itself. *)
537 (* ------------------------------------------------------------------------- *)
539 let FRIENDSHIP = prove
540 (`!friend:person->person->bool.
542 (!x. ~(friend x x)) /\
543 (!x y. friend x y ==> friend y x) /\
544 (!x y. ~(x = y) ==> ?!z. friend x z /\ friend y z)
545 ==> ?u. !v. ~(v = u) ==> friend u v`,
546 REPEAT STRIP_TAC THEN UNDISCH_TAC
547 `!x y:person. ~(x = y) ==> ?!z:person. friend x z /\ friend y z` THEN
548 REWRITE_TAC[EXISTS_UNIQUE_THM] THEN
549 REWRITE_TAC[TAUT `a ==> b /\ c <=> (a ==> b) /\ (a ==> c)`] THEN
550 REWRITE_TAC[FORALL_AND_THM; RIGHT_IMP_FORALL_THM] THEN
551 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [RIGHT_IMP_EXISTS_THM] THEN
552 REWRITE_TAC[SKOLEM_THM; IMP_IMP; GSYM CONJ_ASSOC] THEN
553 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN
554 DISCH_THEN(X_CHOOSE_TAC `mutualfriend:person->person->person`) THEN
555 SUBGOAL_THEN `!s:person->bool. FINITE s` ASSUME_TAC THENL
556 [ASM_MESON_TAC[SUBSET_UNIV; FINITE_SUBSET]; ALL_TAC] THEN
557 ABBREV_TAC `degree = \p:person. CARD {q:person | friend p q}` THEN
558 SUBGOAL_THEN `!x y:person. ~(friend x y) ==> degree(x):num <= degree(y)`
560 [REPEAT STRIP_TAC THEN ASM_CASES_TAC `x:person = y` THENL
561 [ASM_MESON_TAC[LE_REFL]; ALL_TAC] THEN
562 EXPAND_TAC "degree" THEN MATCH_MP_TAC LE_TRANS THEN
563 EXISTS_TAC `CARD(IMAGE (\u. (mutualfriend:person->person->person) u y)
564 {q | friend (x:person) q})` THEN
566 [ALL_TAC; MATCH_MP_TAC CARD_SUBSET THEN ASM SET_TAC[]] THEN
567 MATCH_MP_TAC EQ_IMP_LE THEN CONV_TAC SYM_CONV THEN
568 MATCH_MP_TAC CARD_IMAGE_INJ THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN
569 MAP_EVERY X_GEN_TAC [`u1:person`; `u2:person`] THEN STRIP_TAC THEN
570 FIRST_X_ASSUM(MP_TAC o SPECL
571 [`x:person`; `(mutualfriend:person->person->person) u1 y`;
572 `u1:person`; `u2:person`]) THEN ASM_MESON_TAC[];
574 SUBGOAL_THEN `!x y:person. ~(friend x y) ==> degree x:num = degree y`
575 ASSUME_TAC THENL [ASM_MESON_TAC[LE_ANTISYM]; ALL_TAC] THEN
576 GEN_REWRITE_TAC I [TAUT `p <=> ~ ~ p`] THEN
577 GEN_REWRITE_TAC RAND_CONV [NOT_EXISTS_THM] THEN
578 DISCH_THEN(ASSUME_TAC o REWRITE_RULE[NOT_FORALL_THM; NOT_IMP]) THEN
579 SUBGOAL_THEN `?m:num. !x:person. degree(x) = m` STRIP_ASSUME_TAC THENL
580 [FIRST_ASSUM(X_CHOOSE_THEN `b:person` STRIP_ASSUME_TAC o
581 SPEC `a:person`) THEN
582 ABBREV_TAC `c = (mutualfriend:person->person->person) a b` THEN
583 ABBREV_TAC `k = (degree:person->num) a` THEN EXISTS_TAC `k:num` THEN
584 SUBGOAL_THEN `(degree:person->num)(b) = k /\ ~(friend a b) /\
585 friend a c /\ friend b c`
586 STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
587 SUBGOAL_THEN `!x:person. ~(x = c) ==> degree x = (k:num)` ASSUME_TAC THEN
590 SUBGOAL_THEN `!p:person. {q:person | friend p q} HAS_SIZE m`
591 ASSUME_TAC THENL [ASM_MESON_TAC[HAS_SIZE]; ALL_TAC] THEN
592 SUBGOAL_THEN `~(m = 0)` ASSUME_TAC THENL
594 UNDISCH_TAC `!p:person. {q:person | friend p q} HAS_SIZE m` THEN
595 ASM_REWRITE_TAC[HAS_SIZE_0; EXTENSION; IN_ELIM_THM; NOT_IN_EMPTY] THEN
598 SUBGOAL_THEN `EVEN(m)` ASSUME_TAC THENL
599 [UNDISCH_TAC `!x:person. degree x = (m:num)` THEN
600 DISCH_THEN(SUBST1_TAC o SYM o SPEC `a:person`) THEN
601 EXPAND_TAC "degree" THEN MATCH_MP_TAC ELEMENTS_PAIR_UP THEN
602 EXISTS_TAC `\x y:person. friend a x /\ friend a y /\ friend x y` THEN
603 REWRITE_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[HAS_SIZE];
605 ABBREV_TAC `N = CARD(:person)` THEN
606 SUBGOAL_THEN `N = m * (m - 1) + 1` ASSUME_TAC THENL
607 [ABBREV_TAC `t = {q:person | friend (a:person) q}` THEN
608 SUBGOAL_THEN `FINITE(t:person->bool) /\ CARD t = m` STRIP_ASSUME_TAC THENL
609 [ASM_MESON_TAC[HAS_SIZE]; ALL_TAC] THEN
611 `u = \b:person. {c:person | friend b c /\ ~(c IN (a INSERT t))}` THEN
613 SUBGOAL_THEN `(:person) = (a INSERT t) UNION UNIONS {u(b) | b IN t}`
615 [REWRITE_TAC[EXTENSION; IN_INSERT; IN_UNIV; IN_UNION; IN_UNIONS] THEN
616 MAP_EVERY EXPAND_TAC ["t"; "u"] THEN REWRITE_TAC[IN_ELIM_THM] THEN
617 X_GEN_TAC `x:person` THEN
618 MATCH_MP_TAC(TAUT `(~a /\ ~b ==> c) ==> (a \/ b) \/ c`) THEN
619 STRIP_TAC THEN REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
620 ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ c <=> b /\ a /\ c`] THEN
621 ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN REWRITE_TAC[UNWIND_THM2] THEN
622 REWRITE_TAC[IN_ELIM_THM; IN_INSERT; DE_MORGAN_THM] THEN
623 EXISTS_TAC `mutualfriend (a:person) (x:person) :person` THEN
624 EXPAND_TAC "t" THEN REWRITE_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[];
626 SUBGOAL_THEN `m * (m - 1) + 1 = (m + 1) + m * (m - 2)` SUBST1_TAC THENL
627 [SIMP_TAC[ARITH_RULE `a + 1 = (m + 1) + m * c <=> a = m * (1 + c)`] THEN
628 AP_TERM_TAC THEN UNDISCH_TAC `EVEN m` THEN
629 ASM_CASES_TAC `m = 1` THEN ASM_REWRITE_TAC[ARITH] THEN DISCH_TAC THEN
630 MAP_EVERY UNDISCH_TAC [`~(m = 0)`; `~(m = 1)`] THEN ARITH_TAC;
632 SUBGOAL_THEN `m + 1 = CARD((a:person) INSERT t)` SUBST1_TAC THENL
633 [ASM_SIMP_TAC[CARD_CLAUSES; ADD1] THEN EXPAND_TAC "t" THEN
634 REWRITE_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[];
637 `UNIONS {u b :person->bool | (b:person) IN t} HAS_SIZE m * (m - 2)`
639 [MATCH_MP_TAC HAS_SIZE_UNIONS THEN CONJ_TAC THENL
640 [ASM_MESON_TAC[HAS_SIZE]; ALL_TAC] THEN
643 EXPAND_TAC "u" THEN REWRITE_TAC[DISJOINT; EXTENSION; IN_INTER] THEN
644 REWRITE_TAC[NOT_IN_EMPTY; IN_ELIM_THM; IN_INSERT] THEN
645 EXPAND_TAC "t" THEN REWRITE_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[]] THEN
646 REPEAT STRIP_TAC THEN
647 MP_TAC(ASSUME `(b:person) IN t`) THEN EXPAND_TAC "t" THEN
648 REWRITE_TAC[IN_ELIM_THM] THEN DISCH_TAC THEN
651 {q:person | friend q b} DELETE a DELETE (mutualfriend a b)`
653 [MAP_EVERY EXPAND_TAC ["u"; "t"] THEN
654 REWRITE_TAC[EXTENSION; IN_INSERT; IN_DELETE; IN_ELIM_THM] THEN
655 X_GEN_TAC `x:person` THEN
656 FIRST_X_ASSUM(MP_TAC o SPECL [`a:person`; `b:person`;
657 `(mutualfriend:person->person->person) a b`; `x:person`]) THEN
660 ASM_SIMP_TAC[CARD_DELETE; HAS_SIZE] THEN
661 REWRITE_TAC[IN_ELIM_THM; IN_DELETE] THEN
662 COND_CASES_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
663 SUBGOAL_THEN `{q:person | friend q (b:person)} = {q | friend b q}`
664 SUBST1_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
665 ASM_REWRITE_TAC[ARITH_RULE `m - 1 - 1 = m - 2`] THEN
666 ASM_MESON_TAC[HAS_SIZE];
668 REWRITE_TAC[HAS_SIZE] THEN DISCH_THEN(SUBST1_TAC o SYM o CONJUNCT2) THEN
669 MATCH_MP_TAC CARD_UNION THEN ASM_REWRITE_TAC[] THEN
670 REWRITE_TAC[EXTENSION; IN_INSERT; IN_INTER; NOT_IN_EMPTY; IN_UNIONS] THEN
671 REWRITE_TAC[IN_ELIM_THM; LEFT_AND_EXISTS_THM] THEN
672 ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ c <=> b /\ a /\ c`] THEN
673 ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN REWRITE_TAC[UNWIND_THM2] THEN
674 MAP_EVERY EXPAND_TAC ["u"; "t"] THEN
675 REWRITE_TAC[IN_ELIM_THM; IN_INSERT] THEN ASM_MESON_TAC[];
677 SUBGOAL_THEN `~(m = 2)` ASSUME_TAC THENL
678 [DISCH_THEN SUBST_ALL_TAC THEN
679 RULE_ASSUM_TAC(CONV_RULE NUM_REDUCE_CONV) THEN
680 SUBGOAL_THEN `(:person) HAS_SIZE 3` MP_TAC THENL
681 [ASM_REWRITE_TAC[HAS_SIZE]; ALL_TAC] THEN
682 CONV_TAC(LAND_CONV HAS_SIZE_CONV) THEN REWRITE_TAC[NOT_EXISTS_THM] THEN
683 MAP_EVERY X_GEN_TAC [`a:person`; `b:person`; `c:person`] THEN
684 REWRITE_TAC[EXTENSION; IN_UNIV; IN_INSERT; NOT_IN_EMPTY] THEN
686 UNDISCH_TAC `!u:person. ?v:person. ~(v = u) /\ ~friend u v` THEN
687 REWRITE_TAC[NOT_FORALL_THM; NOT_EXISTS_THM] THEN
688 EXISTS_TAC `a:person` THEN
689 UNDISCH_TAC `!p:person. {q:person | friend p q} HAS_SIZE 2` THEN
690 DISCH_THEN(MP_TAC o SPEC `a:person`) THEN ASM_REWRITE_TAC[] THEN
691 CONV_TAC(LAND_CONV HAS_SIZE_CONV) THEN
692 REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_INSERT; NOT_IN_EMPTY] THEN
693 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
694 MAP_EVERY X_GEN_TAC [`x:person`; `y:person`] THEN
695 STRIP_TAC THEN X_GEN_TAC `z:person` THEN
696 UNDISCH_TAC `!x:person. x = a \/ x = b \/ x = c` THEN
697 DISCH_THEN(fun th -> MAP_EVERY (fun x -> MP_TAC(SPEC x th))
698 [`x:person`; `y:person`; `z:person`]) THEN
701 MP_TAC(SPEC `m - 1` PRIME_FACTOR) THEN ANTS_TAC THENL
702 [UNDISCH_TAC `~(m = 2)` THEN ARITH_TAC; ALL_TAC] THEN
703 DISCH_THEN(X_CHOOSE_THEN `p:num` STRIP_ASSUME_TAC) THEN
704 SUBGOAL_THEN `~(p divides 1)` MP_TAC THENL
705 [ASM_MESON_TAC[DIVIDES_ONE; PRIME_1]; ALL_TAC] THEN
707 MATCH_MP_TAC(NUMBER_RULE
708 `!x. p divides (x + 1) /\ p divides x ==> p divides 1`) THEN
709 EXISTS_TAC `m - 1` THEN ASM_REWRITE_TAC[] THEN
710 ASM_SIMP_TAC[ARITH_RULE `~(m = 0) ==> m - 1 + 1 = m`] THEN
711 MATCH_MP_TAC PRIME_DIVEXP THEN EXISTS_TAC `p - 2` THEN
712 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(NUMBER_RULE
714 p divides q /\ p divides c /\
715 c = (q + 1) * K1 + K2 /\
716 K1 + K2 = ((q + 1) * q + 1) * nep2
717 ==> p divides nep2`) THEN
719 [`m - 1`; `CARD {x:num->person | cycle friend p x}`;
720 `CARD {x:num->person | path friend (p-2) x /\ x (p-2) = x 0}`;
721 `CARD {x:num->person | path friend (p-2) x /\ ~(x (p-2) = x 0)}`] THEN
722 ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
723 [MATCH_MP_TAC CYCLES_PRIME_LEMMA THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
724 SUBGOAL_THEN `3 <= p` ASSUME_TAC THENL
725 [MATCH_MP_TAC(ARITH_RULE `2 <= p /\ ~(p = 2) ==> 3 <= p`) THEN
726 ASM_SIMP_TAC[PRIME_GE_2] THEN DISCH_THEN SUBST_ALL_TAC THEN
727 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM DIVIDES_2]) THEN
728 MP_TAC(DIVIDES_CONV `2 divides 1`) THEN REWRITE_TAC[CONTRAPOS_THM] THEN
729 MATCH_MP_TAC(NUMBER_RULE
730 `!q. t divides q /\ m = q + 1 ==> t divides m ==> t divides w`) THEN
731 EXISTS_TAC `m - 1` THEN ASM_REWRITE_TAC[] THEN
732 UNDISCH_TAC `~(m = 0)` THEN ARITH_TAC;
734 ASM_SIMP_TAC[ARITH_RULE `~(m = 0) ==> m - 1 + 1 = m`] THEN CONJ_TAC THENL
735 [MP_TAC(ISPECL[`friend:person->person->bool`; `p:num`] HAS_SIZE_CYCLES) THEN
736 ANTS_TAC THENL [ASM_MESON_TAC[PRIME_0]; ALL_TAC] THEN
737 SIMP_TAC[HAS_SIZE] THEN DISCH_THEN(K ALL_TAC) THEN
738 MATCH_MP_TAC HAS_SIZE_CARD THEN
739 SUBGOAL_THEN `p = (p - 2) + 2` (fun th ->
740 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th])
741 THENL [ASM_MESON_TAC[PRIME_GE_2; SUB_ADD]; ALL_TAC] THEN
742 MATCH_MP_TAC CARD_PATHCYCLES_STEP THEN EXISTS_TAC `N:num` THEN
743 ASM_REWRITE_TAC[] THEN
744 CONJ_TAC THENL [ASM_MESON_TAC[HAS_SIZE]; ALL_TAC] THEN
745 CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
746 UNDISCH_TAC `3 <= p` THEN ARITH_TAC;
748 MP_TAC(ISPECL [`N:num`; `m:num`; `friend:person->person->bool`; `p - 2`]
750 ANTS_TAC THENL [ASM_MESON_TAC[HAS_SIZE]; ALL_TAC] THEN
751 ASM_REWRITE_TAC[HAS_SIZE] THEN
752 DISCH_THEN(SUBST1_TAC o SYM o CONJUNCT2) THEN
753 MATCH_MP_TAC CARD_UNION_EQ THEN ASM_SIMP_TAC[FINITE_PATHS] THEN SET_TAC[]);;