100/derangements.ml

   1 (* ========================================================================= *)
   2 (* #88: Formula for the number of derangements: round[n!/e]                  *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/transc.ml";;
   6 needs "Library/calc_real.ml";;
   7 needs "Library/floor.ml";;
   8
   9 let PAIR_BETA_THM = GEN_BETA_CONV `(\(x,y). P x y) (a,b)`;;
  10
  11 (* ------------------------------------------------------------------------- *)
  12 (* Domain and range of a relation.                                           *)
  13 (* ------------------------------------------------------------------------- *)
  14
  15 let domain = new_definition
  16  `domain r = {x | ?y. r(x,y)}`;;
  17
  18 let range = new_definition
  19  `range r = {y | ?x. r(x,y)}`;;
  20
  21 (* ------------------------------------------------------------------------- *)
  22 (* Relational composition.                                                   *)
  23 (* ------------------------------------------------------------------------- *)
  24
  25 parse_as_infix("%",(26, "right"));;
  26
  27 let compose = new_definition
  28  `(r % s) (x,y) <=> ?z. r(x,z) /\ s(z,y)`;;
  29
  30 (* ------------------------------------------------------------------------- *)
  31 (* Identity relation on a domain.                                            *)
  32 (* ------------------------------------------------------------------------- *)
  33
  34 let id = new_definition
  35  `id(s) (x,y) <=> x IN s /\ x = y`;;
  36
  37 (* ------------------------------------------------------------------------- *)
  38 (* Converse relation.                                                        *)
  39 (* ------------------------------------------------------------------------- *)
  40
  41 let converse = new_definition
  42  `converse(r) (x,y) = r(y,x)`;;
  43
  44 (* ------------------------------------------------------------------------- *)
  45 (* Transposition.                                                            *)
  46 (* ------------------------------------------------------------------------- *)
  47
  48 let swap = new_definition
  49  `swap(a,b) (x,y) <=> x = a /\ y = b \/ x = b /\ y = a`;;
  50
  51 (* ------------------------------------------------------------------------- *)
  52 (* When a relation "pairs up" two sets bijectively.                          *)
  53 (* ------------------------------------------------------------------------- *)
  54
  55 parse_as_infix("pairsup",(12,"right"));;
  56
  57 let pairsup = new_definition
  58  `r pairsup (s,t) <=> (r % converse(r) = id(s)) /\ (converse(r) % r = id(t))`;;
  59
  60 (* ------------------------------------------------------------------------- *)
  61 (* Special case of a permutation.                                            *)
  62 (* ------------------------------------------------------------------------- *)
  63
  64 parse_as_infix("permutes",(12,"right"));;
  65
  66 let permutes = new_definition
  67  `r permutes s <=> r pairsup (s,s)`;;
  68
  69 (* ------------------------------------------------------------------------- *)
  70 (* Even more special case of derangement.                                    *)
  71 (* ------------------------------------------------------------------------- *)
  72
  73 parse_as_infix("deranges",(12,"right"));;
  74
  75 let deranges = new_definition
  76  `r deranges s <=> r permutes s /\ !x. ~(r(x,x))`;;
  77
  78 (* ------------------------------------------------------------------------- *)
  79 (* Trivial tactic for properties of relations.                               *)
  80 (* ------------------------------------------------------------------------- *)
  81
  82 let REL_TAC =
  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
  92   ASM_MESON_TAC[];;
  93
  94 let REL_RULE tm = prove(tm,REL_TAC);;
  95
  96 (* ------------------------------------------------------------------------- *)
  97 (* Some general properties of relations.                                     *)
  98 (* ------------------------------------------------------------------------- *)
  99
 100 let CONVERSE_COMPOSE = prove
 101  (`!r s. converse(r % s) = converse(s) % converse(r)`,
 102   REL_TAC);;
 103
 104 let CONVERSE_CONVERSE = prove
 105  (`!r. converse(converse r) = r`,
 106   REL_TAC);;
 107
 108 (* ------------------------------------------------------------------------- *)
 109 (* More "explicit" definition of pairing and permutation.                    *)
 110 (* ------------------------------------------------------------------------- *)
 111
 112 let PAIRSUP_EXPLICIT = prove
 113  (`!p s t.
 114         p pairsup (s,t) <=>
 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))`,
 118   REL_TAC);;
 119
 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))`,
 125   REL_TAC);;
 126
 127 (* ------------------------------------------------------------------------- *)
 128 (* Other low-level properties.                                               *)
 129 (* ------------------------------------------------------------------------- *)
 130
 131 let PAIRSUP_DOMRAN = prove
 132  (`!p s t. p pairsup (s,t) ==> domain p = s /\ range p = t`,
 133   REL_TAC);;
 134
 135 let PERMUTES_DOMRAN = prove
 136  (`!p s. p permutes s ==> domain p = s /\ range p = s`,
 137   REL_TAC);;
 138
 139 let PAIRSUP_FUNCTIONAL = prove
 140  (`!p s t. p pairsup (s,t) ==> !x y y'. p(x,y) /\ p(x,y') ==> y = y'`,
 141   REL_TAC);;
 142
 143 let PERMUTES_FUNCTIONAL = prove
 144  (`!p s. p permutes s ==> !x y y'. p(x,y) /\ p(x,y') ==> y = y'`,
 145   REL_TAC);;
 146
 147 let PAIRSUP_COFUNCTIONAL = prove
 148  (`!p s t. p pairsup (s,t) ==> !x x' y. p(x,y) /\ p(x',y) ==> x = x'`,
 149   REL_TAC);;
 150
 151 let PERMUTES_COFUNCTIONAL = prove
 152  (`!p s. p permutes s ==> !x x' y. p(x,y) /\ p(x',y) ==> x = x'`,
 153   REL_TAC);;
 154
 155 (* ------------------------------------------------------------------------- *)
 156 (* Some more abstract properties.                                            *)
 157 (* ------------------------------------------------------------------------- *)
 158
 159 let PAIRSUP_ID = prove
 160  (`!s. id(s) pairsup (s,s)`,
 161   REL_TAC);;
 162
 163 let PERMUTES_ID = prove
 164  (`!s. id(s) permutes s`,
 165   REL_TAC);;
 166
 167 let PAIRSUP_CONVERSE = prove
 168  (`!p s t. p pairsup (s,t) ==> converse(p) pairsup (t,s)`,
 169   REL_TAC);;
 170
 171 let PERMUTES_CONVERSE = prove
 172  (`!p s. p permutes s ==> converse(p) permutes s`,
 173   REL_TAC);;
 174
 175 let PAIRSUP_COMPOSE = prove
 176  (`!p p' s t u. p pairsup (s,t) /\ p' pairsup (t,u) ==> (p % p') pairsup (s,u)`,
 177   REL_TAC);;
 178
 179 let PERMUTES_COMPOSE = prove
 180  (`!p p' s. p permutes s /\ p' permutes s ==> (p % p') permutes s`,
 181   REL_TAC);;
 182
 183 (* ------------------------------------------------------------------------- *)
 184 (* Transpositions are permutations.                                          *)
 185 (* ------------------------------------------------------------------------- *)
 186
 187 let PERMUTES_SWAP = prove
 188  (`swap(a,b) permutes {a,b}`,
 189   REL_TAC);;
 190
 191 (* ------------------------------------------------------------------------- *)
 192 (* Clausal theorems for cases on first set.                                  *)
 193 (* ------------------------------------------------------------------------- *)
 194
 195 let PAIRSUP_EMPTY = prove
 196  (`p pairsup ({},{}) <=> (p = {})`,
 197   REL_TAC);;
 198
 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
 206    [ALL_TAC;
 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);;
 214
 215 (* ------------------------------------------------------------------------- *)
 216 (* Number of pairings and permutations.                                      *)
 217 (* ------------------------------------------------------------------------- *)
 218
 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)`,
 223   let lemma = prove
 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];
 233     ALL_TAC] THEN
 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]);;
 247
 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]);;
 251
 252 (* ------------------------------------------------------------------------- *)
 253 (* Number of derangements (we need to justify this later).                   *)
 254 (* ------------------------------------------------------------------------- *)
 255
 256 let derangements = define
 257  `(derangements 0 = 1) /\
 258   (derangements 1 = 0) /\
 259   (derangements(n + 2) = (n + 1) * (derangements n + derangements(n + 1)))`;;
 260
 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]);;
 267
 268 (* ------------------------------------------------------------------------- *)
 269 (* Expanding a derangement.                                                  *)
 270 (* ------------------------------------------------------------------------- *)
 271
 272 let DERANGEMENT_ADD2 = prove
 273  (`!p s x y.
 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)`,
 276   REL_TAC);;
 277
 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)`,
 282   REL_TAC);;
 283
 284 (* ------------------------------------------------------------------------- *)
 285 (* Number of derangements.                                                   *)
 286 (* ------------------------------------------------------------------------- *)
 287
 288 let DERANGEMENT_EMPTY = prove
 289  (`!p. p deranges {} <=> p = {}`,
 290   REL_TAC);;
 291
 292 let DERANGEMENT_SING = prove
 293  (`!x p. ~(p deranges {x})`,
 294   REL_TAC);;
 295
 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[];
 306     ALL_TAC] THEN
 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
 312   SUBGOAL_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)))
 318                {(y,p) | y IN s /\
 319                         p IN {p | p deranges (x INSERT (s DELETE y))}})`
 320   SUBST1_TAC THENL
 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
 330       STRIP_TAC THENL
 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
 334         ASM_MESON_TAC[];
 335         ALL_TAC] 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;
 341         ALL_TAC] THEN
 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))`
 346       SUBST1_TAC THENL
 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[];
 350       ALL_TAC] THEN
 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
 357       CONJ_TAC THENL
 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[];
 360         ALL_TAC] THEN
 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;
 365       ALL_TAC] THEN
 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
 373     SUBGOAL_THEN
 374      `(@w:A. ((x,z) INSERT (p DELETE (x,y) DELETE (y,z))) (x,w)) = z`
 375     SUBST1_TAC THENL
 376      [MATCH_MP_TAC SELECT_UNIQUE THEN REPEAT(POP_ASSUM MP_TAC) THEN REL_TAC;
 377       ALL_TAC] THEN
 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;
 385       ALL_TAC] THEN
 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;
 390     ALL_TAC] THEN
 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;
 398                   PAIR_EQ] THEN
 399       UNDISCH_TAC `~(x:A IN s)` THEN REL_TAC;
 400       ALL_TAC] THEN
 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];
 406
 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;
 420         ALL_TAC] THEN
 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)
 426       THENL
 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;
 430         ALL_TAC] THEN
 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;
 442       ALL_TAC] THEN
 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;
 449
 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;
 469       ALL_TAC] THEN
 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;
 478       ALL_TAC] THEN
 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]);;
 482
 483 (* ------------------------------------------------------------------------- *)
 484 (* Trivia.                                                                   *)
 485 (* ------------------------------------------------------------------------- *)
 486
 487 let SUM_1 = prove
 488  (`sum(0..1) f = f 0 + f 1`,
 489   REWRITE_TAC[num_CONV `1`; SUM_CLAUSES_NUMSEG; LE_0]);;
 490
 491 let SUM_2 = prove
 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;
 494            REAL_ADD_AC]);;
 495
 496 (* ------------------------------------------------------------------------- *)
 497 (* The key result.                                                           *)
 498 (* ------------------------------------------------------------------------- *)
 499
 500 let DERANGEMENTS = prove
 501  (`!n. ~(n = 0)
 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;
 510     ALL_TAC] THEN
 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);;
 521
 522 (* ------------------------------------------------------------------------- *)
 523 (* A more "explicit" formula. We could sharpen 1/2 to 0.3678794+epsilon      *)
 524 (* ------------------------------------------------------------------------- *)
 525
 526 let DERANGEMENTS_EXP = prove
 527  (`!n. ~(n = 0)
 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;
 540     ALL_TAC] THEN
 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;
 557     ALL_TAC] THEN
 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
 561   REAL_ARITH_TAC);;
 562
 563 (* ------------------------------------------------------------------------- *)
 564 (* Hence the critical "rounding" property.                                   *)
 565 (* ------------------------------------------------------------------------- *)
 566
 567 let round = new_definition
 568  `round x = @n. integer(n) /\ n - &1 / &2 <= x /\ x < n + &1 / &2`;;
 569
 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);;
 575
 576 let DERANGEMENTS_EXP = prove
 577  (`!n. ~(n = 0)
 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);;
 585
 586 (* ------------------------------------------------------------------------- *)
 587 (* Put them together.                                                        *)
 588 (* ------------------------------------------------------------------------- *)
 589
 590 let THE_DERANGEMENTS_FORMULA = prove
 591  (`!n s. s HAS_SIZE n /\ ~(n = 0)
 592          ==> FINITE {p | p deranges s} /\
 593              let e = exp(&1) in
 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]);;