Library/binomial.ml

   1 (* ========================================================================= *)
   2 (* Binomial coefficients and the binomial theorem.                           *)
   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_0 = prove
  17  (`!n. binom(0,n) = if n = 0 then 1 else 0`,
  18   INDUCT_TAC THEN REWRITE_TAC[binom; NOT_SUC]);;
  19
  20 let BINOM_LT = prove
  21  (`!n k. n < k ==> (binom(n,k) = 0)`,
  22   INDUCT_TAC THEN INDUCT_TAC THEN REWRITE_TAC[binom; ARITH; LT_SUC; LT] THEN
  23   ASM_SIMP_TAC[ARITH_RULE `n < k ==> n < SUC(k)`; ARITH]);;
  24
  25 let BINOM_REFL = prove
  26  (`!n. binom(n,n) = 1`,
  27   INDUCT_TAC THEN ASM_SIMP_TAC[binom; BINOM_LT; LT; ARITH]);;
  28
  29 let BINOM_1 = prove
  30  (`!n. binom(n,1) = n`,
  31   REWRITE_TAC[num_CONV `1`] THEN
  32   INDUCT_TAC THEN ASM_REWRITE_TAC[binom] THEN ARITH_TAC);;
  33
  34 let BINOM_FACT = prove
  35  (`!n k. FACT n * FACT k * binom(n+k,k) = FACT(n + k)`,
  36   INDUCT_TAC THEN REWRITE_TAC[FACT; ADD_CLAUSES; MULT_CLAUSES; BINOM_REFL] THEN
  37   INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; FACT; MULT_CLAUSES; binom] THEN
  38   FIRST_X_ASSUM(MP_TAC o SPEC `SUC k`) THEN POP_ASSUM MP_TAC THEN
  39   REWRITE_TAC[ADD_CLAUSES; FACT; binom] THEN CONV_TAC NUM_RING);;
  40
  41 let BINOM_EQ_0 = prove
  42  (`!n k. binom(n,k) = 0 <=> n < k`,
  43   REPEAT GEN_TAC THEN EQ_TAC THENL [ALL_TAC; MESON_TAC[BINOM_LT]] THEN
  44   ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
  45   REWRITE_TAC[NOT_LT; LE_EXISTS] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
  46   DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC) THEN
  47   DISCH_TAC THEN MP_TAC(SYM(SPECL [`d:num`; `k:num`] BINOM_FACT)) THEN
  48   ASM_REWRITE_TAC[GSYM LT_NZ; MULT_CLAUSES; FACT_LT]);;
  49
  50 let BINOM_PENULT = prove
  51  (`!n. binom(SUC n,n) = SUC n`,
  52   INDUCT_TAC THEN ASM_REWRITE_TAC [binom; ONE; BINOM_REFL] THEN
  53   SUBGOAL_THEN `binom(n,SUC n)=0` SUBST1_TAC THENL
  54    [REWRITE_TAC [BINOM_EQ_0; LT]; REWRITE_TAC [ADD; ADD_0; ADD_SUC; SUC_INJ]]);;
  55
  56 let BINOM_GE_TOP = prove
  57  (`!m n. 1 <= m /\ m < n ==> n <= binom(n,m)`,
  58   INDUCT_TAC THEN INDUCT_TAC THEN REWRITE_TAC[binom] THEN
  59   CONV_TAC NUM_REDUCE_CONV THEN STRIP_TAC THEN ASM_CASES_TAC `m = 0` THEN
  60   ASM_SIMP_TAC[BINOM_1; ARITH_SUC; binom] THEN REWRITE_TAC[ADD1; LE_REFL] THEN
  61   FIRST_X_ASSUM(MP_TAC o SPEC `n:num`) THEN
  62   ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
  63   MATCH_MP_TAC(ARITH_RULE `~(c = 0) ==> n <= b ==> n + 1 <= c + b`) THEN
  64   REWRITE_TAC[BINOM_EQ_0] THEN ASM_ARITH_TAC);;
  65
  66 (* ------------------------------------------------------------------------- *)
  67 (* More potentially useful lemmas.                                           *)
  68 (* ------------------------------------------------------------------------- *)
  69
  70 let BINOM_TOP_STEP = prove
  71  (`!n k. ((n + 1) - k) * binom(n + 1,k) = (n + 1) * binom(n,k)`,
  72   REPEAT GEN_TAC THEN ASM_CASES_TAC `n < k:num` THENL
  73    [FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP
  74      (ARITH_RULE `n < k ==> n + 1 = k \/ n + 1 < k`)) THEN
  75     ASM_SIMP_TAC[BINOM_LT; SUB_REFL; MULT_CLAUSES];
  76     ALL_TAC] THEN
  77   FIRST_X_ASSUM(MP_TAC o REWRITE_RULE[NOT_LT; LE_EXISTS]) THEN
  78   DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC) THEN
  79   REWRITE_TAC[GSYM ADD_ASSOC; ADD_SUB; ADD_SUB2] THEN
  80   MP_TAC(SPECL [`d + 1`; `k:num`] BINOM_FACT) THEN
  81   MP_TAC(SPECL [`d:num`; `k:num`] BINOM_FACT) THEN
  82   REWRITE_TAC[GSYM ADD1; ADD_CLAUSES; FACT; ADD_AC] THEN
  83   MAP_EVERY (fun t -> MP_TAC(SPEC t FACT_LT)) [`d:num`; `k:num`] THEN
  84   REWRITE_TAC[LT_NZ] THEN CONV_TAC NUM_RING);;
  85
  86 let BINOM_BOTTOM_STEP = prove
  87  (`!n k. (k + 1) * binom(n,k + 1) = (n - k) * binom(n,k)`,
  88   REPEAT GEN_TAC THEN ASM_CASES_TAC `n < k + 1` THENL
  89    [FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP
  90      (ARITH_RULE `n < k + 1 ==> n = k \/ n < k`)) THEN
  91     ASM_SIMP_TAC[BINOM_LT; SUB_REFL; MULT_CLAUSES];
  92     ALL_TAC] THEN
  93   FIRST_X_ASSUM(MP_TAC o REWRITE_RULE[NOT_LT; LE_EXISTS]) THEN
  94   DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC) THEN
  95   REWRITE_TAC[GSYM ADD_ASSOC; ADD_SUB; ADD_SUB2] THEN
  96   MP_TAC(SPECL [`d + 1`; `k:num`] BINOM_FACT) THEN
  97   MP_TAC(SPECL [`d:num`; `k + 1`] BINOM_FACT) THEN
  98   REWRITE_TAC[GSYM ADD1; ADD_CLAUSES; FACT; ADD_AC] THEN
  99   MAP_EVERY (fun t -> MP_TAC(SPEC t FACT_LT)) [`d:num`; `k:num`] THEN
 100   REWRITE_TAC[LT_NZ] THEN CONV_TAC NUM_RING);;
 101
 102 (* ------------------------------------------------------------------------- *)
 103 (* Binomial expansion.                                                       *)
 104 (* ------------------------------------------------------------------------- *)
 105
 106 let BINOMIAL_THEOREM = prove
 107  (`!n x y.
 108       (x + y) EXP n = nsum(0..n) (\k. binom(n,k) * x EXP k * y EXP (n - k))`,
 109   INDUCT_TAC THEN REPEAT GEN_TAC THEN ASM_REWRITE_TAC[EXP] THEN
 110   REWRITE_TAC[NSUM_SING_NUMSEG; binom; SUB_REFL; EXP; MULT_CLAUSES] THEN
 111   SIMP_TAC[NSUM_CLAUSES_LEFT; ADD1; ARITH_RULE `0 <= n + 1`; NSUM_OFFSET] THEN
 112   ASM_REWRITE_TAC[EXP; binom; GSYM ADD1; GSYM NSUM_LMUL] THEN
 113   REWRITE_TAC[RIGHT_ADD_DISTRIB; NSUM_ADD_NUMSEG; MULT_CLAUSES; SUB_0] THEN
 114   MATCH_MP_TAC(ARITH_RULE `a = e /\ b = c + d ==> a + b = c + d + e`) THEN
 115   CONJ_TAC THENL [REWRITE_TAC[MULT_AC; SUB_SUC]; REWRITE_TAC[GSYM EXP]] THEN
 116   SIMP_TAC[ADD1; SYM(REWRITE_CONV[NSUM_OFFSET]`nsum(m+1..n+1) (\i. f i)`)] THEN
 117   REWRITE_TAC[NSUM_CLAUSES_NUMSEG; GSYM ADD1; LE_SUC; LE_0] THEN
 118   SIMP_TAC[NSUM_CLAUSES_LEFT; LE_0] THEN
 119   SIMP_TAC[BINOM_LT; LT; MULT_CLAUSES; ADD_CLAUSES; SUB_0; EXP; binom] THEN
 120   SIMP_TAC[ARITH; ARITH_RULE `k <= n ==> SUC n - k = SUC(n - k)`; EXP] THEN
 121   REWRITE_TAC[MULT_AC]);;
 122
 123 (* ------------------------------------------------------------------------- *)
 124 (* Same thing for the reals.                                                 *)
 125 (* ------------------------------------------------------------------------- *)
 126
 127 prioritize_real();;
 128
 129 let REAL_BINOMIAL_THEOREM = prove
 130  (`!n x y.
 131      (x + y) pow n = sum(0..n) (\k. &(binom(n,k)) * x pow k * y pow (n - k))`,
 132   INDUCT_TAC THEN REPEAT GEN_TAC THEN ASM_REWRITE_TAC[real_pow] THEN
 133   REWRITE_TAC[SUM_SING_NUMSEG; binom; SUB_REFL; real_pow; REAL_MUL_LID] THEN
 134   SIMP_TAC[SUM_CLAUSES_LEFT; ADD1; ARITH_RULE `0 <= n + 1`; SUM_OFFSET] THEN
 135   ASM_REWRITE_TAC[real_pow; binom; GSYM ADD1; GSYM SUM_LMUL] THEN
 136   REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN
 137   REWRITE_TAC[REAL_ADD_RDISTRIB; SUM_ADD_NUMSEG; REAL_MUL_LID; SUB_0] THEN
 138   MATCH_MP_TAC(ARITH_RULE `a = e /\ b = c + d ==> a + b = c + d + e`) THEN
 139   CONJ_TAC THENL [SIMP_TAC[REAL_MUL_AC; SUB_SUC]; SIMP_TAC[GSYM real_pow]] THEN
 140   SIMP_TAC[ADD1; SYM(REWRITE_CONV[SUM_OFFSET]`sum(m+1..n+1) (\i. f i)`)] THEN
 141   REWRITE_TAC[SUM_CLAUSES_NUMSEG; GSYM ADD1; LE_SUC; LE_0] THEN
 142   SIMP_TAC[SUM_CLAUSES_LEFT; LE_0; BINOM_LT; LT; REAL_MUL_LID; SUB_0; real_pow;
 143            binom; REAL_MUL_LZERO; REAL_ADD_RID] THEN
 144   SIMP_TAC[ARITH; ARITH_RULE `k <= n ==> SUC n - k = SUC(n - k)`; real_pow] THEN
 145   REWRITE_TAC[REAL_MUL_AC]);;
 146
 147 (* ------------------------------------------------------------------------- *)
 148 (* More direct stepping theorems over the reals.                             *)
 149 (* ------------------------------------------------------------------------- *)
 150
 151 let BINOM_TOP_STEP_REAL = prove
 152  (`!n k. &(binom(n + 1,k)) =
 153            if k = n + 1 then &1
 154            else (&n + &1) / (&n + &1 - &k) * &(binom(n,k))`,
 155   REPEAT STRIP_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[BINOM_REFL] THEN
 156   FIRST_X_ASSUM(STRIP_ASSUME_TAC o MATCH_MP (ARITH_RULE
 157    `~(k = n + 1) ==> n < k /\ n + 1 < k \/ k <= n /\ k <= n + 1`)) THEN
 158   ASM_SIMP_TAC[BINOM_LT; REAL_MUL_RZERO] THEN
 159   MP_TAC(SPECL [`n:num`; `k:num`] BINOM_TOP_STEP) THEN
 160   ASM_SIMP_TAC[GSYM REAL_OF_NUM_EQ; GSYM REAL_OF_NUM_MUL; GSYM REAL_OF_NUM_ADD;
 161                GSYM REAL_OF_NUM_SUB] THEN
 162   UNDISCH_TAC `k <= n:num` THEN REWRITE_TAC[GSYM REAL_OF_NUM_LE] THEN
 163   CONV_TAC REAL_FIELD);;
 164
 165 let BINOM_BOTTOM_STEP_REAL = prove
 166  (`!n k. &(binom(n,k+1)) = (&n - &k) / (&k + &1) * &(binom(n,k))`,
 167   REPEAT GEN_TAC THEN DISJ_CASES_TAC(ARITH_RULE `n:num < k \/ k <= n`) THENL
 168    [ASM_SIMP_TAC[BINOM_LT; ARITH_RULE `n < k ==> n < k + 1`; REAL_MUL_RZERO];
 169     MP_TAC(SPECL [`n:num`; `k:num`] BINOM_BOTTOM_STEP) THEN
 170     ASM_SIMP_TAC[GSYM REAL_OF_NUM_EQ; GSYM REAL_OF_NUM_MUL;
 171                  GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_SUB] THEN
 172     CONV_TAC REAL_FIELD]);;
 173
 174 let REAL_OF_NUM_BINOM = prove
 175  (`!n k. &(binom(n,k)) =
 176              if k <= n then &(FACT n) / (&(FACT(n - k)) * &(FACT k))
 177              else &0`,
 178   REPEAT GEN_TAC THEN COND_CASES_TAC THEN
 179   ASM_SIMP_TAC[BINOM_LT; GSYM NOT_LE] THEN
 180   SIMP_TAC[REAL_EQ_RDIV_EQ; REAL_LT_MUL; REAL_OF_NUM_LT; FACT_LT] THEN
 181   FIRST_ASSUM(CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[LE_EXISTS]) THEN
 182   REWRITE_TAC[ADD_SUB2] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
 183   REWRITE_TAC[GSYM BINOM_FACT] THEN REWRITE_TAC[REAL_OF_NUM_MUL; MULT_AC]);;
 184
 185 (* ------------------------------------------------------------------------- *)
 186 (* Some additional theorems for stepping both arguments together.            *)
 187 (* ------------------------------------------------------------------------- *)
 188
 189 let BINOM_BOTH_STEP_REAL = prove
 190  (`!p k. &(binom(p + 1,k + 1)) = (&p + &1) / (&k + &1) * &(binom(p,k))`,
 191   REWRITE_TAC[BINOM_TOP_STEP_REAL; BINOM_BOTTOM_STEP_REAL] THEN
 192   REPEAT GEN_TAC THEN REWRITE_TAC[EQ_ADD_RCANCEL] THEN
 193   COND_CASES_TAC THEN ASM_REWRITE_TAC[BINOM_REFL] THEN POP_ASSUM MP_TAC THEN
 194   REWRITE_TAC[GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_EQ] THEN
 195   CONV_TAC REAL_FIELD);;
 196
 197 let BINOM_BOTH_STEP = prove
 198  (`!p k. (k + 1) * binom(p + 1,k + 1) = (p + 1) * binom(p,k)`,
 199   REWRITE_TAC[GSYM REAL_OF_NUM_EQ; GSYM REAL_OF_NUM_MUL] THEN
 200   REWRITE_TAC[BINOM_BOTH_STEP_REAL; GSYM REAL_OF_NUM_ADD] THEN
 201   CONV_TAC REAL_FIELD);;
 202
 203 let BINOM_BOTH_STEP_DOWN = prove
 204  (`!p k. (k = 0 ==> p = 0) ==> k * binom(p,k) = p * binom(p - 1,k - 1)`,
 205   REPEAT INDUCT_TAC THEN
 206   SIMP_TAC[BINOM_LT; LT_0; LT_REFL; ARITH] THEN
 207   REWRITE_TAC[SUC_SUB1; ADD1; BINOM_BOTH_STEP] THEN
 208   REWRITE_TAC[MULT_CLAUSES]);;
 209
 210 let BINOM = prove
 211  (`!n k. binom(n,k) =
 212             if k <= n then FACT(n) DIV (FACT(n - k) * FACT(k))
 213             else 0`,
 214   REPEAT GEN_TAC THEN COND_CASES_TAC THEN
 215   ASM_SIMP_TAC[BINOM_EQ_0; GSYM NOT_LE] THEN CONV_TAC SYM_CONV THEN
 216   MATCH_MP_TAC DIV_UNIQ THEN EXISTS_TAC `0` THEN
 217   SIMP_TAC[LT_MULT; FACT_LT; ADD_CLAUSES] THEN
 218   FIRST_X_ASSUM(CHOOSE_THEN SUBST1_TAC o GEN_REWRITE_RULE I [LE_EXISTS]) THEN
 219   ONCE_REWRITE_TAC[ADD_SYM] THEN
 220   REWRITE_TAC[GSYM BINOM_FACT; ADD_SUB] THEN REWRITE_TAC[MULT_AC]);;
 221
 222 (* ------------------------------------------------------------------------- *)
 223 (* Additional lemmas.                                                        *)
 224 (* ------------------------------------------------------------------------- *)
 225
 226 let BINOM_SYM = prove
 227  (`!n k. binom(n,n-k) = if k <= n then binom(n,k) else 1`,
 228   REPEAT GEN_TAC THEN COND_CASES_TAC THEN
 229   ASM_SIMP_TAC[binom; ARITH_RULE `~(k <= n) ==> n - k = 0`] THEN
 230   REWRITE_TAC[GSYM REAL_OF_NUM_EQ; REAL_OF_NUM_BINOM] THEN
 231   ASM_REWRITE_TAC[ARITH_RULE `n - k:num <= n`] THEN
 232   ASM_SIMP_TAC[ARITH_RULE `k:num <= n ==> n - (n - k) = k`] THEN
 233   REWRITE_TAC[REAL_OF_NUM_MUL; MULT_SYM]);;
 234
 235 let BINOM_MUL_SHIFT = prove
 236  (`!m n k. k <= m
 237            ==> binom(n,m) * binom(m,k) = binom(n,k) * binom(n - k,m - k)`,
 238   REPEAT STRIP_TAC THEN
 239   SIMP_TAC[GSYM REAL_OF_NUM_EQ; GSYM REAL_OF_NUM_MUL; REAL_OF_NUM_BINOM] THEN
 240   ASM_CASES_TAC `n:num < m` THENL
 241    [REPEAT(COND_CASES_TAC THEN
 242       ASM_REWRITE_TAC[REAL_MUL_LZERO; REAL_MUL_RZERO]) THEN
 243     MATCH_MP_TAC(TAUT `F ==> p`) THEN ASM_ARITH_TAC;
 244     REPEAT(COND_CASES_TAC THENL
 245      [ALL_TAC; MATCH_MP_TAC(TAUT `F ==> p`) THEN  ASM_ARITH_TAC]) THEN
 246     RULE_ASSUM_TAC(REWRITE_RULE[NOT_LT]) THEN
 247     ASM_SIMP_TAC[ARITH_RULE
 248      `k:num <= m /\ m <= n ==> n - k - (m - k) = n - m`] THEN
 249     MAP_EVERY (MP_TAC o C SPEC FACT_NZ)
 250      [`n:num`; `m:num`; `n - m:num`; `n - k:num`; `m - k:num`] THEN
 251     REWRITE_TAC[GSYM REAL_OF_NUM_EQ] THEN CONV_TAC REAL_FIELD]);;
 252
 253 let APPELL_SEQUENCE = prove
 254  (`!c n x y. sum (0..n)
 255                (\k.  &(binom(n,k)) *
 256                      sum(0..k)
 257                         (\l. &(binom(k,l)) * c l * x pow (k - l)) *
 258                      y pow (n - k)) =
 259            sum (0..n) (\k. &(binom(n,k)) * c k * (x + y) pow (n - k))`,
 260   REPEAT GEN_TAC THEN REWRITE_TAC[REAL_BINOMIAL_THEOREM] THEN
 261   REWRITE_TAC[GSYM SUM_LMUL; GSYM SUM_RMUL] THEN
 262   SIMP_TAC[SUM_SUM_PRODUCT; FINITE_NUMSEG] THEN
 263   MATCH_MP_TAC SUM_EQ_GENERAL_INVERSES THEN
 264   EXISTS_TAC `(\(x,y). y,x - y):num#num->num#num` THEN
 265   EXISTS_TAC `(\(x,y). x + y,x):num#num->num#num` THEN
 266   REWRITE_TAC[FORALL_IN_GSPEC; IN_ELIM_PAIR_THM] THEN
 267   REWRITE_TAC[PAIR_EQ; IN_NUMSEG] THEN
 268   CONJ_TAC THENL [ARITH_TAC; REPEAT GEN_TAC THEN STRIP_TAC] THEN
 269   REPEAT(CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC]) THEN
 270   ASM_SIMP_TAC[ARITH_RULE
 271    `j:num <= k /\ k <= n ==> (n - j) - (k - j) = n - k`] THEN
 272   MATCH_MP_TAC(REAL_RING
 273    `c * d:real = a * b ==> a * z * b * x * y = c * (d * z * x) * y`) THEN
 274   ASM_SIMP_TAC[REAL_OF_NUM_MUL; REAL_OF_NUM_EQ; BINOM_MUL_SHIFT]);;
 275
 276 (* ------------------------------------------------------------------------- *)
 277 (* Numerical computation of binom.                                           *)
 278 (* ------------------------------------------------------------------------- *)
 279
 280 let NUM_BINOM_CONV =
 281   let pth_step = prove
 282    (`binom(n,k) = y
 283      ==> k <= n
 284          ==> (SUC n) * y = ((n + 1) - k) * x ==> binom(SUC n,k) = x`,
 285     DISCH_THEN(SUBST1_TAC o SYM) THEN
 286     REWRITE_TAC[ADD1; GSYM BINOM_TOP_STEP; EQ_MULT_LCANCEL; SUB_EQ_0] THEN
 287     ARITH_TAC)
 288   and pth_0 = prove
 289    (`n < k ==> binom(n,k) = 0`,
 290     REWRITE_TAC[BINOM_LT])
 291   and pth_1 = prove
 292    (`binom(n,n) = 1`,
 293     REWRITE_TAC[BINOM_REFL])
 294   and pth_swap = prove
 295    (`k <= n ==> binom(n,k) = binom(n,n - k)`,
 296     MESON_TAC[BINOM_SYM])
 297   and k_tm = `k:num` and n_tm = `n:num`
 298   and x_tm = `x:num` and y_tm = `y:num`
 299   and binom_tm = `binom` in
 300   let rec BINOM_RULE(n,k) =
 301     if n </ k then
 302       let th = INST [mk_numeral n,n_tm; mk_numeral k,k_tm] pth_0 in
 303       MP_CONV NUM_LT_CONV th
 304     else if n =/ k then
 305       INST [mk_numeral n,n_tm] pth_1
 306     else if Int 2 */ k </ n then
 307       let th1 = INST [mk_numeral n,n_tm; mk_numeral k,k_tm] pth_swap in
 308       let th2 = MP th1 (EQT_ELIM(NUM_LE_CONV (lhand(concl th1)))) in
 309       let th3 = CONV_RULE(funpow 3 RAND_CONV NUM_SUB_CONV) th2 in
 310       TRANS th3 (BINOM_RULE(n,n -/ k))
 311     else
 312       let th1 = BINOM_RULE(n -/ Int 1,k) in
 313       let y = dest_numeral(rand(concl th1)) in
 314       let x = (n // (n -/ k)) */ y in
 315       let th2 = INST [mk_numeral(n -/ Int 1),n_tm; mk_numeral k,k_tm;
 316                       mk_numeral x,x_tm; mk_numeral y,y_tm] pth_step in
 317       let th3 = MP_CONV NUM_REDUCE_CONV (MP_CONV NUM_LE_CONV (MP th2 th1)) in
 318       CONV_RULE (LAND_CONV(RAND_CONV(LAND_CONV NUM_SUC_CONV))) th3 in
 319   fun tm ->
 320     let bop,nkp = dest_comb tm in
 321     if bop <> binom_tm then failwith "NUM_BINOM_CONV" else
 322     let nt,kt = dest_pair nkp in
 323     BINOM_RULE(dest_numeral nt,dest_numeral kt);;