100/combinations.ml

   1 (* ========================================================================= *)
   2 (* Binomial coefficients and relation to number of combinations.             *)
   3 (* ========================================================================= *)
   4
   5 prioritize_num();;
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* Binomial coefficients.                                                    *)
   9 (* ------------------------------------------------------------------------- *)
  10
  11 let binom = define
  12   `(!n. binom(n,0) = 1) /\
  13    (!k. binom(0,SUC(k)) = 0) /\
  14    (!n k. binom(SUC(n),SUC(k)) = binom(n,SUC(k)) + binom(n,k))`;;
  15
  16 let BINOM_LT = prove
  17  (`!n k. n < k ==> (binom(n,k) = 0)`,
  18   INDUCT_TAC THEN INDUCT_TAC THEN REWRITE_TAC[binom; ARITH; LT_SUC; LT] THEN
  19   ASM_SIMP_TAC[ARITH_RULE `n < k ==> n < SUC(k)`; ARITH]);;
  20
  21 let BINOM_REFL = prove
  22  (`!n. binom(n,n) = 1`,
  23   INDUCT_TAC THEN ASM_SIMP_TAC[binom; BINOM_LT; LT; ARITH]);;
  24
  25 (* ------------------------------------------------------------------------- *)
  26 (* Usual "factorial" definition.                                             *)
  27 (* ------------------------------------------------------------------------- *)
  28
  29 let BINOM_FACT = prove
  30  (`!n k. FACT n * FACT k * binom(n+k,k) = FACT(n + k)`,
  31   INDUCT_TAC THEN REWRITE_TAC[FACT; ADD_CLAUSES; MULT_CLAUSES; BINOM_REFL] THEN
  32   INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; FACT; MULT_CLAUSES; binom] THEN
  33   FIRST_X_ASSUM(MP_TAC o SPEC `SUC k`) THEN POP_ASSUM MP_TAC THEN
  34   REWRITE_TAC[ADD_CLAUSES; FACT; binom] THEN CONV_TAC NUM_RING);;
  35
  36 let BINOM_EXPLICIT = prove
  37  (`!n k. binom(n,k) =
  38             if n < k then 0 else FACT(n) DIV (FACT(k) * FACT(n - k))`,
  39   REPEAT STRIP_TAC THEN COND_CASES_TAC THEN ASM_SIMP_TAC[BINOM_LT] THEN
  40   POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_LT; LE_EXISTS] THEN
  41   STRIP_TAC THEN ASM_REWRITE_TAC[ADD_SUB2] THEN CONV_TAC SYM_CONV THEN
  42   MATCH_MP_TAC DIV_UNIQ THEN EXISTS_TAC `0` THEN
  43   SIMP_TAC[LT_MULT; FACT_LT; ADD_CLAUSES] THEN
  44   ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[GSYM BINOM_FACT] THEN
  45   REWRITE_TAC[MULT_AC]);;
  46
  47 (* ------------------------------------------------------------------------- *)
  48 (* A tedious lemma.                                                          *)
  49 (* ------------------------------------------------------------------------- *)
  50
  51 let lemma = prove
  52  (`~(a IN t)
  53    ==> {u | u SUBSET (a:A INSERT t) /\ u HAS_SIZE (SUC m)} =
  54        {u | u SUBSET t /\ u HAS_SIZE (SUC m)} UNION
  55        IMAGE (\u. a INSERT u) {u | u SUBSET t /\ u HAS_SIZE m}`,
  56   REPEAT STRIP_TAC THEN GEN_REWRITE_TAC I [EXTENSION] THEN
  57   REWRITE_TAC[IN_UNION; IN_IMAGE; IN_ELIM_THM] THEN X_GEN_TAC `u:A->bool` THEN
  58   ASM_CASES_TAC `(u:A->bool) SUBSET t` THEN ASM_REWRITE_TAC[] THENL
  59    [ASM_CASES_TAC `(u:A->bool) HAS_SIZE (SUC m)` THEN ASM_REWRITE_TAC[] THEN
  60     ASM SET_TAC[];
  61     ALL_TAC] THEN
  62   EQ_TAC THEN STRIP_TAC THENL
  63    [EXISTS_TAC `u DELETE (a:A)`  THEN
  64     REPEAT (CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC]) THEN
  65     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [HAS_SIZE_SUC]) THEN
  66     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MATCH_MP_TAC) THEN ASM SET_TAC[];
  67     CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
  68     REWRITE_TAC[HAS_SIZE_CLAUSES] THEN
  69     EXISTS_TAC `a:A` THEN EXISTS_TAC `x':A->bool` THEN
  70     ASM SET_TAC[]]);;
  71
  72 (* ------------------------------------------------------------------------- *)
  73 (* The "number of combinations" formula.                                     *)
  74 (* ------------------------------------------------------------------------- *)
  75
  76 let BINOM_INDUCT = prove
  77  (`!P. (!n. P n 0) /\
  78        (!k. P 0 (SUC k)) /\
  79        (!n k. P n (SUC k) /\ P n k ==> P (SUC n) (SUC k))
  80        ==> !m n. P m n`,
  81   GEN_TAC THEN STRIP_TAC THEN REPEAT INDUCT_TAC THEN ASM_MESON_TAC[]);;
  82
  83 let NUMBER_OF_COMBINATIONS = prove
  84  (`!n m s:A->bool.
  85         s HAS_SIZE n
  86         ==> {t | t SUBSET s /\ t HAS_SIZE m} HAS_SIZE binom(n,m)`,
  87   MATCH_MP_TAC BINOM_INDUCT THEN REWRITE_TAC[binom] THEN REPEAT CONJ_TAC THENL
  88    [REPEAT STRIP_TAC THEN CONV_TAC HAS_SIZE_CONV THEN
  89     EXISTS_TAC `{}:A->bool` THEN SIMP_TAC[EXTENSION; IN_SING; IN_ELIM_THM] THEN
  90     REWRITE_TAC[NOT_IN_EMPTY; HAS_SIZE_0] THEN SET_TAC[];
  91     SIMP_TAC[HAS_SIZE_0; SUBSET_EMPTY; HAS_SIZE_SUC] THEN SET_TAC[];
  92     ALL_TAC] THEN
  93   MAP_EVERY X_GEN_TAC [`n:num`; `m:num`] THEN STRIP_TAC THEN
  94   GEN_TAC THEN GEN_REWRITE_TAC LAND_CONV [HAS_SIZE_CLAUSES] THEN
  95   REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
  96   MAP_EVERY X_GEN_TAC [`a:A`; `t:A->bool`] THEN
  97   STRIP_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN
  98   ASM_SIMP_TAC[lemma] THEN MATCH_MP_TAC HAS_SIZE_UNION THEN
  99   ASM_SIMP_TAC[] THEN CONJ_TAC THENL
 100    [MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN ASM_SIMP_TAC[] THEN
 101     UNDISCH_TAC `~(a:A IN t)` THEN SET_TAC[];
 102     ALL_TAC] THEN
 103   REWRITE_TAC[DISJOINT; EXTENSION; IN_INTER; NOT_IN_EMPTY] THEN
 104   REWRITE_TAC[IN_IMAGE; IN_ELIM_THM; HAS_SIZE_SUC] THEN
 105   UNDISCH_TAC `~(a:A IN t)` THEN SET_TAC[]);;
 106
 107 (* ------------------------------------------------------------------------- *)
 108 (* Explicit version.                                                         *)
 109 (* ------------------------------------------------------------------------- *)
 110
 111 let NUMBER_OF_COMBINATIONS_EXPLICIT = prove
 112  (`!n m s:A->bool.
 113         s HAS_SIZE n
 114         ==> {t | t SUBSET s /\ t HAS_SIZE m} HAS_SIZE
 115             (if n < m then 0 else FACT(n) DIV (FACT(m) * FACT(n - m)))`,
 116   REWRITE_TAC[REWRITE_RULE[BINOM_EXPLICIT] NUMBER_OF_COMBINATIONS]);;