1 (* ========================================================================= *)
2 (* #88: Formula for the number of derangements: round[n!/e] *)
3 (* ========================================================================= *)
5 needs "Library/transc.ml";;
6 needs "Library/calc_real.ml";;
7 needs "Library/floor.ml";;
9 let PAIR_BETA_THM = GEN_BETA_CONV `(\(x,y). P x y) (a,b)`;;
11 (* ------------------------------------------------------------------------- *)
12 (* Domain and range of a relation. *)
13 (* ------------------------------------------------------------------------- *)
15 let domain = new_definition
16 `domain r = {x | ?y. r(x,y)}`;;
18 let range = new_definition
19 `range r = {y | ?x. r(x,y)}`;;
21 (* ------------------------------------------------------------------------- *)
22 (* Relational composition. *)
23 (* ------------------------------------------------------------------------- *)
25 parse_as_infix("%",(26, "right"));;
27 let compose = new_definition
28 `(r % s) (x,y) <=> ?z. r(x,z) /\ s(z,y)`;;
30 (* ------------------------------------------------------------------------- *)
31 (* Identity relation on a domain. *)
32 (* ------------------------------------------------------------------------- *)
34 let id = new_definition
35 `id(s) (x,y) <=> x IN s /\ x = y`;;
37 (* ------------------------------------------------------------------------- *)
38 (* Converse relation. *)
39 (* ------------------------------------------------------------------------- *)
41 let converse = new_definition
42 `converse(r) (x,y) = r(y,x)`;;
44 (* ------------------------------------------------------------------------- *)
46 (* ------------------------------------------------------------------------- *)
48 let swap = new_definition
49 `swap(a,b) (x,y) <=> x = a /\ y = b \/ x = b /\ y = a`;;
51 (* ------------------------------------------------------------------------- *)
52 (* When a relation "pairs up" two sets bijectively. *)
53 (* ------------------------------------------------------------------------- *)
55 parse_as_infix("pairsup",(12,"right"));;
57 let pairsup = new_definition
58 `r pairsup (s,t) <=> (r % converse(r) = id(s)) /\ (converse(r) % r = id(t))`;;
60 (* ------------------------------------------------------------------------- *)
61 (* Special case of a permutation. *)
62 (* ------------------------------------------------------------------------- *)
64 parse_as_infix("permutes",(12,"right"));;
66 let permutes = new_definition
67 `r permutes s <=> r pairsup (s,s)`;;
69 (* ------------------------------------------------------------------------- *)
70 (* Even more special case of derangement. *)
71 (* ------------------------------------------------------------------------- *)
73 parse_as_infix("deranges",(12,"right"));;
75 let deranges = new_definition
76 `r deranges s <=> r permutes s /\ !x. ~(r(x,x))`;;
78 (* ------------------------------------------------------------------------- *)
79 (* Trivial tactic for properties of relations. *)
80 (* ------------------------------------------------------------------------- *)
83 POP_ASSUM_LIST(K ALL_TAC) THEN
84 REWRITE_TAC[FUN_EQ_THM; FORALL_PAIR_THM; EXISTS_PAIR_THM; PAIR_BETA_THM;
85 permutes; pairsup; domain; range; compose; id; converse; swap;
86 deranges; IN_INSERT; IN_DELETE; NOT_IN_EMPTY; IN_ELIM_THM] THEN
87 REWRITE_TAC[IN; EMPTY; INSERT; DELETE; UNION; IN_ELIM_THM; PAIR_EQ;
88 id; converse; swap] THEN
89 REPEAT(STRIP_TAC ORELSE EQ_TAC) THEN
90 REPEAT(FIRST_X_ASSUM(SUBST_ALL_TAC o check (is_var o lhs o concl))) THEN
91 REPEAT(FIRST_X_ASSUM(SUBST_ALL_TAC o SYM o check (is_var o rhs o concl))) THEN
94 let REL_RULE tm = prove(tm,REL_TAC);;
96 (* ------------------------------------------------------------------------- *)
97 (* Some general properties of relations. *)
98 (* ------------------------------------------------------------------------- *)
100 let CONVERSE_COMPOSE = prove
101 (`!r s. converse(r % s) = converse(s) % converse(r)`,
104 let CONVERSE_CONVERSE = prove
105 (`!r. converse(converse r) = r`,
108 (* ------------------------------------------------------------------------- *)
109 (* More "explicit" definition of pairing and permutation. *)
110 (* ------------------------------------------------------------------------- *)
112 let PAIRSUP_EXPLICIT = prove
115 (!x y. p(x,y) ==> x IN s /\ y IN t) /\
116 (!x. x IN s ==> ?!y. y IN t /\ p(x,y)) /\
117 (!y. y IN t ==> ?!x. x IN s /\ p(x,y))`,
120 let PERMUTES_EXPLICIT = prove
121 (`!p s. p permutes s <=>
122 (!x y. p(x,y) ==> x IN s /\ y IN s) /\
123 (!x. x IN s ==> ?!y. y IN s /\ p(x,y)) /\
124 (!y. y IN s ==> ?!x. x IN s /\ p(x,y))`,
127 (* ------------------------------------------------------------------------- *)
128 (* Other low-level properties. *)
129 (* ------------------------------------------------------------------------- *)
131 let PAIRSUP_DOMRAN = prove
132 (`!p s t. p pairsup (s,t) ==> domain p = s /\ range p = t`,
135 let PERMUTES_DOMRAN = prove
136 (`!p s. p permutes s ==> domain p = s /\ range p = s`,
139 let PAIRSUP_FUNCTIONAL = prove
140 (`!p s t. p pairsup (s,t) ==> !x y y'. p(x,y) /\ p(x,y') ==> y = y'`,
143 let PERMUTES_FUNCTIONAL = prove
144 (`!p s. p permutes s ==> !x y y'. p(x,y) /\ p(x,y') ==> y = y'`,
147 let PAIRSUP_COFUNCTIONAL = prove
148 (`!p s t. p pairsup (s,t) ==> !x x' y. p(x,y) /\ p(x',y) ==> x = x'`,
151 let PERMUTES_COFUNCTIONAL = prove
152 (`!p s. p permutes s ==> !x x' y. p(x,y) /\ p(x',y) ==> x = x'`,
155 (* ------------------------------------------------------------------------- *)
156 (* Some more abstract properties. *)
157 (* ------------------------------------------------------------------------- *)
159 let PAIRSUP_ID = prove
160 (`!s. id(s) pairsup (s,s)`,
163 let PERMUTES_ID = prove
164 (`!s. id(s) permutes s`,
167 let PAIRSUP_CONVERSE = prove
168 (`!p s t. p pairsup (s,t) ==> converse(p) pairsup (t,s)`,
171 let PERMUTES_CONVERSE = prove
172 (`!p s. p permutes s ==> converse(p) permutes s`,
175 let PAIRSUP_COMPOSE = prove
176 (`!p p' s t u. p pairsup (s,t) /\ p' pairsup (t,u) ==> (p % p') pairsup (s,u)`,
179 let PERMUTES_COMPOSE = prove
180 (`!p p' s. p permutes s /\ p' permutes s ==> (p % p') permutes s`,
183 (* ------------------------------------------------------------------------- *)
184 (* Transpositions are permutations. *)
185 (* ------------------------------------------------------------------------- *)
187 let PERMUTES_SWAP = prove
188 (`swap(a,b) permutes {a,b}`,
191 (* ------------------------------------------------------------------------- *)
192 (* Clausal theorems for cases on first set. *)
193 (* ------------------------------------------------------------------------- *)
195 let PAIRSUP_EMPTY = prove
196 (`p pairsup ({},{}) <=> (p = {})`,
199 let PAIRSUP_INSERT = prove
200 (`!x:A s t:B->bool p.
201 p pairsup (x INSERT s,t) <=>
202 if x IN s then p pairsup (s,t)
203 else ?y q. y IN t /\ p = (x,y) INSERT q /\ q pairsup (s,t DELETE y)`,
204 REPEAT GEN_TAC THEN COND_CASES_TAC THEN
205 ASM_SIMP_TAC[SET_RULE `x IN s ==> x INSERT s = s`] THEN EQ_TAC THENL
207 REPEAT STRIP_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN
208 REPEAT(POP_ASSUM MP_TAC) THEN REL_TAC] THEN
209 DISCH_TAC THEN SUBGOAL_THEN `?y. y IN t /\ p(x:A,y:B)` MP_TAC THENL
210 [POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN REL_TAC; ALL_TAC] THEN
211 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `y:B` THEN STRIP_TAC THEN
212 EXISTS_TAC `p DELETE (x:A,y:B)` THEN
213 POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN REL_TAC);;
215 (* ------------------------------------------------------------------------- *)
216 (* Number of pairings and permutations. *)
217 (* ------------------------------------------------------------------------- *)
219 let NUMBER_OF_PAIRINGS = prove
220 (`!n s:A->bool t:B->bool.
221 s HAS_SIZE n /\ t HAS_SIZE n
222 ==> {p | p pairsup (s,t)} HAS_SIZE (FACT n)`,
224 (`{p | ?y. y IN t /\ A y p} = UNIONS {{p | A y p} | y IN t} /\
225 {p | ?q. p = (a,y) INSERT q /\ A y q} =
226 IMAGE (\q. (a,y) INSERT q) {q | A y q}`,
227 CONJ_TAC THEN GEN_REWRITE_TAC I [EXTENSION] THEN
228 REWRITE_TAC[IN_ELIM_THM; IN_UNIONS; IN_IMAGE] THEN SET_TAC[]) in
229 INDUCT_TAC THEN REPEAT GEN_TAC THENL
230 [REWRITE_TAC[HAS_SIZE_CLAUSES] THEN
231 SIMP_TAC[PAIRSUP_EMPTY; SET_RULE `{x | x = a} = {a}`] THEN
232 SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_RULES; NOT_IN_EMPTY; ARITH; FACT];
234 GEN_REWRITE_TAC (funpow 2 LAND_CONV) [HAS_SIZE_CLAUSES] THEN
235 REWRITE_TAC[HAS_SIZE_SUC] THEN
236 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN
237 REPEAT STRIP_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN
238 ASM_REWRITE_TAC[PAIRSUP_INSERT; RIGHT_EXISTS_AND_THM; lemma; FACT] THEN
239 MATCH_MP_TAC HAS_SIZE_UNIONS THEN REPEAT CONJ_TAC THENL
240 [ASM_REWRITE_TAC[HAS_SIZE_SUC];
241 REPEAT STRIP_TAC THEN MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN
242 ASM_SIMP_TAC[] THEN REPEAT(POP_ASSUM MP_TAC) THEN REL_TAC;
243 REPEAT STRIP_TAC THEN REWRITE_TAC[DISJOINT] THEN
244 GEN_REWRITE_TAC I [EXTENSION] THEN
245 REWRITE_TAC[IN_INTER; IN_IMAGE; NOT_IN_EMPTY] THEN
246 REPEAT(POP_ASSUM MP_TAC) THEN REL_TAC]);;
248 let NUMBER_OF_PERMUTATIONS = prove
249 (`!s n. s HAS_SIZE n ==> {p | p permutes s} HAS_SIZE (FACT n)`,
250 SIMP_TAC[permutes; NUMBER_OF_PAIRINGS]);;
252 (* ------------------------------------------------------------------------- *)
253 (* Number of derangements (we need to justify this later). *)
254 (* ------------------------------------------------------------------------- *)
256 let derangements = define
257 `(derangements 0 = 1) /\
258 (derangements 1 = 0) /\
259 (derangements(n + 2) = (n + 1) * (derangements n + derangements(n + 1)))`;;
261 let DERANGEMENT_INDUCT = prove
262 (`!P. P 0 /\ P 1 /\ (!n. P n /\ P(n + 1) ==> P(n + 2)) ==> !n. P n`,
263 GEN_TAC THEN STRIP_TAC THEN
264 SUBGOAL_THEN `!n. P n /\ P(n + 1)` (fun th -> MESON_TAC[th]) THEN
265 INDUCT_TAC THEN ASM_SIMP_TAC[ADD1; GSYM ADD_ASSOC] THEN
266 ASM_SIMP_TAC[ARITH]);;
268 (* ------------------------------------------------------------------------- *)
269 (* Expanding a derangement. *)
270 (* ------------------------------------------------------------------------- *)
272 let DERANGEMENT_ADD2 = prove
274 p deranges s /\ ~(x IN s) /\ ~(y IN s) /\ ~(x = y)
275 ==> ((x,y) INSERT (y,x) INSERT p) deranges (x INSERT y INSERT s)`,
278 let DERANGEMENT_ADD1 = prove
279 (`!p s y x. p deranges s /\ ~(y IN s) /\ p(x,z)
280 ==> ((x,y) INSERT (y,z) INSERT (p DELETE (x,z)))
281 deranges (y INSERT s)`,
284 (* ------------------------------------------------------------------------- *)
285 (* Number of derangements. *)
286 (* ------------------------------------------------------------------------- *)
288 let DERANGEMENT_EMPTY = prove
289 (`!p. p deranges {} <=> p = {}`,
292 let DERANGEMENT_SING = prove
293 (`!x p. ~(p deranges {x})`,
296 let NUMBER_OF_DERANGEMENTS = prove
297 (`!n s:A->bool. s HAS_SIZE n ==> {p | p deranges s} HAS_SIZE (derangements n)`,
298 MATCH_MP_TAC DERANGEMENT_INDUCT THEN REWRITE_TAC[derangements] THEN
299 REPEAT CONJ_TAC THENL
300 [CONV_TAC(ONCE_DEPTH_CONV HAS_SIZE_CONV) THEN REPEAT STRIP_TAC THEN
301 EXISTS_TAC `{}:A#A->bool` THEN
302 ASM_REWRITE_TAC[DERANGEMENT_EMPTY; EXTENSION; IN_ELIM_THM] THEN
303 REWRITE_TAC[NOT_IN_EMPTY; IN_SING] THEN MESON_TAC[MEMBER_NOT_EMPTY];
304 CONV_TAC(ONCE_DEPTH_CONV HAS_SIZE_CONV) THEN REPEAT STRIP_TAC THEN
305 ASM_REWRITE_TAC[DERANGEMENT_SING] THEN SET_TAC[];
307 X_GEN_TAC `n:num` THEN STRIP_TAC THEN X_GEN_TAC `t:A->bool` THEN
308 REWRITE_TAC[ARITH_RULE `n + 2 = SUC(n + 1)`; HAS_SIZE_CLAUSES] THEN
309 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
310 MAP_EVERY X_GEN_TAC [`x:A`; `s:A->bool`] THEN
311 STRIP_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN
313 `{p | p deranges (x:A INSERT s)} =
314 (IMAGE (\(y,p). (x,y) INSERT (y,x) INSERT p)
315 {(y,p) | y IN s /\ p IN {p | p deranges (s DELETE y)}}) UNION
316 (IMAGE (\(y,p). let z = @z. p(x,z) in
317 (x,y) INSERT (y,z) INSERT (p DELETE (x,z)))
319 p IN {p | p deranges (x INSERT (s DELETE y))}})`
321 [GEN_REWRITE_TAC I [EXTENSION] THEN
322 REWRITE_TAC[TAUT `(a <=> b) <=> (b ==> a) /\ (a ==> b)`] THEN
323 REWRITE_TAC[FORALL_AND_THM] THEN CONJ_TAC THENL
324 [REWRITE_TAC[IN_UNION; TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`;
325 FORALL_AND_THM; FORALL_IN_IMAGE] THEN
326 REWRITE_TAC[FORALL_PAIR_THM; PAIR_BETA_THM; IN_ELIM_THM; PAIR_EQ] THEN
327 ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ c /\ d <=> c /\ d /\ a /\ b`] THEN
328 REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
329 CONJ_TAC THEN MAP_EVERY X_GEN_TAC [`y:A`; `p:A#A->bool`] THEN
331 [FIRST_ASSUM(SUBST1_TAC o MATCH_MP (SET_RULE
332 `y IN s ==> s = y INSERT (s DELETE y)`)) THEN
333 MATCH_MP_TAC DERANGEMENT_ADD2 THEN ASM_REWRITE_TAC[IN_DELETE] THEN
336 ABBREV_TAC `z = @z. p(x:A,z:A)` THEN
337 SUBGOAL_THEN `(p:A#A->bool)(x:A,z:A)` STRIP_ASSUME_TAC THENL
338 [REPEAT(FIRST_X_ASSUM(SUBST1_TAC o SYM)) THEN
339 CONV_TAC SELECT_CONV THEN
340 REPEAT(POP_ASSUM MP_TAC) THEN REL_TAC;
342 SUBGOAL_THEN `z:A IN s` STRIP_ASSUME_TAC THENL
343 [REPEAT(POP_ASSUM MP_TAC) THEN REL_TAC; ALL_TAC] THEN
344 REWRITE_TAC[LET_DEF; LET_END_DEF] THEN
345 SUBGOAL_THEN `(x:A) INSERT s = y INSERT (x INSERT (s DELETE y))`
347 [REPEAT(POP_ASSUM MP_TAC) THEN SET_TAC[]; ALL_TAC] THEN
348 MATCH_MP_TAC DERANGEMENT_ADD1 THEN ASM_REWRITE_TAC[] THEN
349 ASM_REWRITE_TAC[IN_DELETE; IN_INSERT] THEN ASM_MESON_TAC[];
351 X_GEN_TAC `p:A#A->bool` THEN REWRITE_TAC[IN_ELIM_THM] THEN DISCH_TAC THEN
352 SUBGOAL_THEN `?y. y IN s /\ p(x:A,y:A)` STRIP_ASSUME_TAC THENL
353 [REPEAT(POP_ASSUM MP_TAC) THEN REL_TAC; ALL_TAC] THEN
354 REWRITE_TAC[IN_UNION] THEN ASM_CASES_TAC `(p:A#A->bool)(y,x)` THENL
355 [DISJ1_TAC THEN REWRITE_TAC[IN_IMAGE] THEN
356 EXISTS_TAC `y:A,(p DELETE (y,x)) DELETE (x:A,y:A)` THEN
358 [REWRITE_TAC[PAIR_BETA_THM] THEN MAP_EVERY UNDISCH_TAC
359 [`(p:A#A->bool)(x,y)`; `(p:A#A->bool)(y,x)`] THEN SET_TAC[];
361 REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN
362 ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ c /\ d <=> c /\ d /\ a /\ b`] THEN
363 ASM_REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
364 REPEAT(POP_ASSUM MP_TAC) THEN REL_TAC;
366 SUBGOAL_THEN `?z. p(y:A,z:A)` STRIP_ASSUME_TAC THENL
367 [REPEAT(POP_ASSUM MP_TAC) THEN REL_TAC; ALL_TAC] THEN
368 SUBGOAL_THEN `z:A IN s` ASSUME_TAC THENL
369 [REPEAT(POP_ASSUM MP_TAC) THEN REL_TAC; ALL_TAC] THEN
370 DISJ2_TAC THEN REWRITE_TAC[IN_IMAGE; EXISTS_PAIR_THM; PAIR_BETA_THM] THEN
371 EXISTS_TAC `y:A` THEN
372 EXISTS_TAC `(x:A,z:A) INSERT ((p DELETE (x,y)) DELETE (y,z))` THEN
374 `(@w:A. ((x,z) INSERT (p DELETE (x,y) DELETE (y,z))) (x,w)) = z`
376 [MATCH_MP_TAC SELECT_UNIQUE THEN REPEAT(POP_ASSUM MP_TAC) THEN REL_TAC;
378 REWRITE_TAC[LET_DEF; LET_END_DEF] THEN CONJ_TAC THENL
379 [REWRITE_TAC[EXTENSION; FORALL_PAIR_THM; PAIR_BETA_THM] THEN
380 REWRITE_TAC[IN; INSERT; DELETE; PAIR_BETA_THM; IN_ELIM_THM; PAIR_EQ] THEN
381 MAP_EVERY X_GEN_TAC [`u:A`; `v:A`] THEN
382 ASM_CASES_TAC `u:A = x` THEN ASM_REWRITE_TAC[] THENL
383 [ALL_TAC; REPEAT(POP_ASSUM MP_TAC) THEN REL_TAC] THEN
384 FIRST_X_ASSUM SUBST_ALL_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN REL_TAC;
386 REWRITE_TAC[IN_ELIM_THM; PAIR_EQ] THEN
387 ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ c /\ d <=> c /\ d /\ a /\ b`] THEN
388 ASM_REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
389 REPEAT(POP_ASSUM MP_TAC) THEN REL_TAC;
391 REWRITE_TAC[LEFT_ADD_DISTRIB] THEN MATCH_MP_TAC HAS_SIZE_UNION THEN
392 REPEAT CONJ_TAC THENL
393 [MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN CONJ_TAC THENL
394 [REWRITE_TAC[FORALL_PAIR_THM; IN_ELIM_THM; PAIR_BETA_THM; PAIR_EQ] THEN
395 ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ c /\ d <=> c /\ d /\ a /\ b`] THEN
396 REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
397 REWRITE_TAC[FUN_EQ_THM; INSERT; IN_ELIM_THM; FORALL_PAIR_THM;
399 UNDISCH_TAC `~(x:A IN s)` THEN REL_TAC;
401 MATCH_MP_TAC HAS_SIZE_PRODUCT_DEPENDENT THEN ASM_REWRITE_TAC[] THEN
402 REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
403 UNDISCH_TAC `(s:A->bool) HAS_SIZE (n + 1)` THEN
404 SIMP_TAC[HAS_SIZE; FINITE_DELETE; CARD_DELETE] THEN
405 ASM_REWRITE_TAC[ADD_SUB];
407 MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN CONJ_TAC THENL
408 [REWRITE_TAC[FORALL_PAIR_THM; IN_ELIM_THM; PAIR_BETA_THM; PAIR_EQ] THEN
409 ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ c /\ d <=> c /\ d /\ a /\ b`] THEN
410 REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN MAP_EVERY X_GEN_TAC
411 [`y:A`; `p:(A#A)->bool`; `y':A`; `p':(A#A->bool)`] THEN
412 DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
413 DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
414 MAP_EVERY ABBREV_TAC [`z = @z. p(x:A,z:A)`; `z' = @z. p'(x:A,z:A)`] THEN
415 REWRITE_TAC[LET_DEF; LET_END_DEF] THEN
416 SUBGOAL_THEN `p(x:A,z:A) /\ p'(x:A,z':A)` STRIP_ASSUME_TAC THENL
417 [REPEAT(FIRST_X_ASSUM(SUBST1_TAC o SYM)) THEN
418 CONJ_TAC THEN CONV_TAC SELECT_CONV THEN
419 REPEAT(POP_ASSUM MP_TAC) THEN REL_TAC;
421 REPEAT(FIRST_X_ASSUM(K ALL_TAC o SYM)) THEN
422 SUBGOAL_THEN `z:A IN s /\ z':A IN s` STRIP_ASSUME_TAC THENL
423 [REPEAT(POP_ASSUM MP_TAC) THEN REL_TAC; ALL_TAC] THEN
424 DISCH_THEN(fun th -> MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN
425 CONJ_TAC THEN MP_TAC th)
427 [DISCH_THEN(MP_TAC o C AP_THM `(x:A,y:A)`) THEN
428 REWRITE_TAC[INSERT; DELETE; IN_ELIM_THM; PAIR_BETA_THM; PAIR_EQ] THEN
429 REPEAT(POP_ASSUM MP_TAC) THEN REL_TAC;
431 ONCE_REWRITE_TAC[TAUT `a ==> b ==> c <=> b ==> a ==> c`] THEN
432 DISCH_THEN(SUBST_ALL_TAC o SYM) THEN
433 ASM_CASES_TAC `z':A = z` THEN ASM_REWRITE_TAC[] THENL
434 [FIRST_X_ASSUM SUBST_ALL_TAC;
435 DISCH_THEN(MP_TAC o C AP_THM `(y:A,z:A)`) THEN
436 REWRITE_TAC[INSERT; DELETE; IN_ELIM_THM; PAIR_BETA_THM; PAIR_EQ] THEN
437 REPEAT(POP_ASSUM MP_TAC) THEN REL_TAC] THEN
438 DISCH_THEN(MP_TAC o MATCH_MP (SET_RULE
439 `a INSERT b INSERT s = a INSERT b INSERT t
440 ==> ~(a IN s) /\ ~(a IN t) /\ ~(b IN s) /\ ~(b IN t) ==> s = t`)) THEN
441 REPEAT(POP_ASSUM MP_TAC) THEN REL_TAC;
443 MATCH_MP_TAC HAS_SIZE_PRODUCT_DEPENDENT THEN ASM_REWRITE_TAC[] THEN
444 REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
445 ASM_REWRITE_TAC[] THEN UNDISCH_TAC `(s:A->bool) HAS_SIZE n + 1` THEN
446 ASM_SIMP_TAC[HAS_SIZE; FINITE_INSERT; FINITE_DELETE] THEN
447 ASM_SIMP_TAC[CARD_DELETE; CARD_CLAUSES; FINITE_DELETE] THEN
448 ASM_REWRITE_TAC[IN_DELETE] THEN ARITH_TAC;
450 REWRITE_TAC[DISJOINT] THEN
451 GEN_REWRITE_TAC I [EXTENSION] THEN
452 REWRITE_TAC[NOT_IN_EMPTY; IN_INTER; TAUT `~(a /\ b) <=> a ==> ~b`] THEN
453 REWRITE_TAC[FORALL_IN_IMAGE] THEN REWRITE_TAC[FORALL_PAIR_THM] THEN
454 MAP_EVERY X_GEN_TAC [`y:A`; `p:A#A->bool`] THEN
455 REWRITE_TAC[IN_ELIM_THM; PAIR_BETA_THM; PAIR_EQ] THEN
456 ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ c /\ d <=> c /\ d /\ a /\ b`] THEN
457 REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
458 STRIP_TAC THEN REWRITE_TAC[IN_IMAGE; EXISTS_PAIR_THM; NOT_EXISTS_THM] THEN
459 MAP_EVERY X_GEN_TAC [`z:A`; `q:A#A->bool`] THEN
460 REWRITE_TAC[PAIR_BETA_THM; IN_ELIM_THM; PAIR_EQ] THEN
461 ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ c /\ d <=> c /\ d /\ a /\ b`] THEN
462 REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
463 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN
464 ABBREV_TAC `w = @w. q(x:A,w:A)` THEN
465 SUBGOAL_THEN `(q:A#A->bool)(x:A,w:A)` STRIP_ASSUME_TAC THENL
466 [REPEAT(FIRST_X_ASSUM(SUBST1_TAC o SYM)) THEN
467 CONV_TAC SELECT_CONV THEN
468 REPEAT(POP_ASSUM MP_TAC) THEN REL_TAC;
470 SUBGOAL_THEN `w:A IN s` STRIP_ASSUME_TAC THENL
471 [REPEAT(POP_ASSUM MP_TAC) THEN REL_TAC; ALL_TAC] THEN
472 REWRITE_TAC[LET_DEF; LET_END_DEF] THEN FIRST_X_ASSUM(K ALL_TAC o SYM) THEN
473 ASM_CASES_TAC `w:A = z` THEN ASM_REWRITE_TAC[] THENL
474 [REPEAT(POP_ASSUM MP_TAC) THEN REL_TAC; ALL_TAC] THEN
475 ASM_CASES_TAC `w:A = y` THEN ASM_REWRITE_TAC[] THENL
476 [FIRST_X_ASSUM SUBST_ALL_TAC THEN
477 REPEAT(POP_ASSUM MP_TAC) THEN REL_TAC;
479 ASM_CASES_TAC `y:A = z` THENL
480 [FIRST_X_ASSUM SUBST_ALL_TAC; ALL_TAC] THEN
481 REPEAT(POP_ASSUM MP_TAC) THEN REL_TAC]);;
483 (* ------------------------------------------------------------------------- *)
485 (* ------------------------------------------------------------------------- *)
488 (`sum(0..1) f = f 0 + f 1`,
489 REWRITE_TAC[num_CONV `1`; SUM_CLAUSES_NUMSEG; LE_0]);;
492 (`sum(0..2) f = f 0 + f 1 + f 2`,
493 SIMP_TAC[num_CONV `2`; num_CONV `1`; SUM_CLAUSES_NUMSEG; LE_0;
496 (* ------------------------------------------------------------------------- *)
497 (* The key result. *)
498 (* ------------------------------------------------------------------------- *)
500 let DERANGEMENTS = prove
502 ==> &(derangements n) =
503 &(FACT n) * sum(0..n) (\k. --(&1) pow k / &(FACT k))`,
504 MATCH_MP_TAC DERANGEMENT_INDUCT THEN REWRITE_TAC[ADD_EQ_0; ARITH_EQ] THEN
505 REWRITE_TAC[derangements; SUM_1] THEN
506 CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
507 X_GEN_TAC `n:num` THEN ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[] THENL
508 [ASM_REWRITE_TAC[derangements; ARITH; SUM_2; SUM_1] THEN
509 CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC REAL_RAT_REDUCE_CONV;
511 REWRITE_TAC[GSYM REAL_OF_NUM_MUL; GSYM REAL_OF_NUM_ADD] THEN
512 DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN
513 REWRITE_TAC[ARITH_RULE `n + 2 = (n + 1) + 1`] THEN
514 SIMP_TAC[SUM_ADD_SPLIT; LE_0; SUM_SING_NUMSEG] THEN
515 REWRITE_TAC[GSYM ADD1; FACT; GSYM REAL_OF_NUM_MUL] THEN
516 REWRITE_TAC[real_pow] THEN REWRITE_TAC[ARITH_RULE `SUC(SUC n) = n + 2`] THEN
517 REWRITE_TAC[GSYM REAL_OF_NUM_SUC; GSYM REAL_OF_NUM_ADD] THEN
518 MP_TAC(SPEC `n:num` FACT_LT) THEN UNDISCH_TAC `~(n = 0)` THEN
519 REWRITE_TAC[GSYM LT_NZ; REAL_POW_NEG; GSYM REAL_OF_NUM_LT; REAL_POW_ONE] THEN
520 CONV_TAC REAL_FIELD);;
522 (* ------------------------------------------------------------------------- *)
523 (* A more "explicit" formula. We could sharpen 1/2 to 0.3678794+epsilon *)
524 (* ------------------------------------------------------------------------- *)
526 let DERANGEMENTS_EXP = prove
528 ==> let e = exp(&1) in
529 abs(&(derangements n) - &(FACT n) / e) < &1 / &2`,
530 REPEAT STRIP_TAC THEN ASM_SIMP_TAC[DERANGEMENTS; LET_DEF; LET_END_DEF] THEN
531 REWRITE_TAC[real_div; GSYM REAL_EXP_NEG] THEN ASM_CASES_TAC `n < 5` THENL
532 [FIRST_X_ASSUM(REPEAT_TCL DISJ_CASES_THEN SUBST_ALL_TAC o MATCH_MP
533 (ARITH_RULE `n < 5 ==> n = 0 \/ n = 1 \/ n = 2 \/ n = 3 \/ n = 4`)) THEN
534 POP_ASSUM MP_TAC THEN REWRITE_TAC[ARITH] THEN
535 REWRITE_TAC(map (num_CONV o mk_small_numeral) (1--5)) THEN
536 REWRITE_TAC[SUM_CLAUSES_NUMSEG] THEN CONV_TAC NUM_REDUCE_CONV THEN
537 CONV_TAC REAL_RAT_REDUCE_CONV THEN
538 REWRITE_TAC[REAL_ARITH `abs x < a <=> --a < x /\ x < a`] THEN
539 REWRITE_TAC[real_sub] THEN CONJ_TAC THEN CONV_TAC REALCALC_REL_CONV;
541 MP_TAC(SPECL [`-- &1`; `n + 1`] MCLAURIN_EXP_LE) THEN
542 SIMP_TAC[PSUM_SUM_NUMSEG; ADD_EQ_0; ARITH_EQ] THEN
543 REWRITE_TAC[ARITH_RULE `(0 + n + 1) - 1 = n`; GSYM real_div] THEN
544 DISCH_THEN(X_CHOOSE_THEN `u:real` STRIP_ASSUME_TAC) THEN
545 ASM_REWRITE_TAC[REAL_ARITH `abs(a * b - a * (b + c)) = abs(a * c)`] THEN
546 REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_DIV; REAL_ABS_POW; REAL_ABS_NEG] THEN
547 REWRITE_TAC[REAL_ABS_NUM; REAL_POW_ONE; REAL_MUL_RID] THEN
548 REWRITE_TAC[GSYM ADD1; FACT; GSYM REAL_OF_NUM_MUL] THEN
549 REWRITE_TAC[GSYM REAL_OF_NUM_SUC] THEN
550 SIMP_TAC[REAL_OF_NUM_LT; FACT_LT; REAL_FIELD
551 `&0 < a ==> a * b / ((&n + &1) * a) = b / (&n + &1)`] THEN
552 SIMP_TAC[REAL_LT_LDIV_EQ; REAL_ARITH `&0 < &n + &1`] THEN
553 REWRITE_TAC[real_abs; REAL_EXP_POS_LE] THEN
554 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `exp(&1)` THEN CONJ_TAC THENL
555 [REWRITE_TAC[REAL_EXP_MONO_LE] THEN
556 UNDISCH_TAC `abs(u) <= abs(-- &1)` THEN REAL_ARITH_TAC;
558 MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&3` THEN CONJ_TAC THENL
559 [CONV_TAC REALCALC_REL_CONV; ALL_TAC] THEN
560 UNDISCH_TAC `~(n < 5)` THEN REWRITE_TAC[NOT_LT; GSYM REAL_OF_NUM_LE] THEN
563 (* ------------------------------------------------------------------------- *)
564 (* Hence the critical "rounding" property. *)
565 (* ------------------------------------------------------------------------- *)
567 let round = new_definition
568 `round x = @n. integer(n) /\ n - &1 / &2 <= x /\ x < n + &1 / &2`;;
570 let ROUND_WORKS = prove
571 (`!x. integer(round x) /\ round x - &1 / &2 <= x /\ x < round x + &1 / &2`,
572 GEN_TAC THEN REWRITE_TAC[round] THEN CONV_TAC SELECT_CONV THEN
573 EXISTS_TAC `floor(x + &1 / &2)` THEN MP_TAC(SPEC `x + &1 / &2` FLOOR) THEN
574 SIMP_TAC[INTEGER_CLOSED] THEN REAL_ARITH_TAC);;
576 let DERANGEMENTS_EXP = prove
578 ==> let e = exp(&1) in &(derangements n) = round(&(FACT n) / e)`,
579 REPEAT STRIP_TAC THEN LET_TAC THEN
580 MATCH_MP_TAC REAL_EQ_INTEGERS_IMP THEN
581 REWRITE_TAC[INTEGER_CLOSED; ROUND_WORKS] THEN
582 MP_TAC(SPEC `&(FACT n) / e` ROUND_WORKS) THEN
583 FIRST_X_ASSUM(MP_TAC o MATCH_MP DERANGEMENTS_EXP) THEN
584 ASM_REWRITE_TAC[LET_DEF; LET_END_DEF] THEN REAL_ARITH_TAC);;
586 (* ------------------------------------------------------------------------- *)
587 (* Put them together. *)
588 (* ------------------------------------------------------------------------- *)
590 let THE_DERANGEMENTS_FORMULA = prove
591 (`!n s. s HAS_SIZE n /\ ~(n = 0)
592 ==> FINITE {p | p deranges s} /\
594 &(CARD {p | p deranges s}) = round(&(FACT n) / e)`,
595 REPEAT STRIP_TAC THEN
596 FIRST_X_ASSUM(MP_TAC o MATCH_MP NUMBER_OF_DERANGEMENTS) THEN
597 ASM_SIMP_TAC[HAS_SIZE; DERANGEMENTS_EXP]);;