(* ========================================================================= *)
(* Binomial coefficients and the binomial theorem.                           *)
(* ========================================================================= *)

prioritize_num();;

(* ------------------------------------------------------------------------- *)
(* Binomial coefficients.                                                    *)
(* ------------------------------------------------------------------------- *)

let binom = define
  `(!n. binom(n,0) = 1) /\
   (!k. binom(0,SUC(k)) = 0) /\
   (!n k. binom(SUC(n),SUC(k)) = binom(n,SUC(k)) + binom(n,k))`;;

let BINOM_0 = prove
 (`!n. binom(0,n) = if n = 0 then 1 else 0`,
  INDUCT_TAC THEN REWRITE_TAC[binom; NOT_SUC]);;

let BINOM_LT = prove
 (`!n k. n < k ==> (binom(n,k) = 0)`,
  INDUCT_TAC THEN INDUCT_TAC THEN REWRITE_TAC[binom; ARITH; LT_SUC; LT] THEN
  ASM_SIMP_TAC[ARITH_RULE `n < k ==> n < SUC(k)`; ARITH]);;

let BINOM_REFL = prove
 (`!n. binom(n,n) = 1`,
  INDUCT_TAC THEN ASM_SIMP_TAC[binom; BINOM_LT; LT; ARITH]);;

let BINOM_1 = prove
 (`!n. binom(n,1) = n`,
  REWRITE_TAC[num_CONV `1`] THEN
  INDUCT_TAC THEN ASM_REWRITE_TAC[binom] THEN ARITH_TAC);;

let BINOM_FACT = prove
 (`!n k. FACT n * FACT k * binom(n+k,k) = FACT(n + k)`,
  INDUCT_TAC THEN REWRITE_TAC[FACT; ADD_CLAUSES; MULT_CLAUSES; BINOM_REFL] THEN
  INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; FACT; MULT_CLAUSES; binom] THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `SUC k`) THEN POP_ASSUM MP_TAC THEN
  REWRITE_TAC[ADD_CLAUSES; FACT; binom] THEN CONV_TAC NUM_RING);;

let BINOM_EQ_0 = prove
 (`!n k. binom(n,k) = 0 <=> n < k`,
  REPEAT GEN_TAC THEN EQ_TAC THENL [ALL_TAC; MESON_TAC[BINOM_LT]] THEN
  ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
  REWRITE_TAC[NOT_LT; LE_EXISTS] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
  DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC) THEN
  DISCH_TAC THEN MP_TAC(SYM(SPECL [`d:num`; `k:num`] BINOM_FACT)) THEN
  ASM_REWRITE_TAC[GSYM LT_NZ; MULT_CLAUSES; FACT_LT]);;

let BINOM_PENULT = prove
 (`!n. binom(SUC n,n) = SUC n`,
  INDUCT_TAC THEN ASM_REWRITE_TAC [binom; ONE; BINOM_REFL] THEN
  SUBGOAL_THEN `binom(n,SUC n)=0` SUBST1_TAC THENL
   [REWRITE_TAC [BINOM_EQ_0; LT]; REWRITE_TAC [ADD; ADD_0; ADD_SUC; SUC_INJ]]);;

let BINOM_GE_TOP = prove
 (`!m n. 1 <= m /\ m < n ==> n <= binom(n,m)`,
  INDUCT_TAC THEN INDUCT_TAC THEN REWRITE_TAC[binom] THEN
  CONV_TAC NUM_REDUCE_CONV THEN STRIP_TAC THEN ASM_CASES_TAC `m = 0` THEN
  ASM_SIMP_TAC[BINOM_1; ARITH_SUC; binom] THEN REWRITE_TAC[ADD1; LE_REFL] THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `n:num`) THEN
  ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
  MATCH_MP_TAC(ARITH_RULE `~(c = 0) ==> n <= b ==> n + 1 <= c + b`) THEN
  REWRITE_TAC[BINOM_EQ_0] THEN ASM_ARITH_TAC);;

(* ------------------------------------------------------------------------- *)
(* More potentially useful lemmas.                                           *)
(* ------------------------------------------------------------------------- *)

let BINOM_TOP_STEP = prove
 (`!n k. ((n + 1) - k) * binom(n + 1,k) = (n + 1) * binom(n,k)`,
  REPEAT GEN_TAC THEN ASM_CASES_TAC `n < k:num` THENL
   [FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP
     (ARITH_RULE `n < k ==> n + 1 = k \/ n + 1 < k`)) THEN
    ASM_SIMP_TAC[BINOM_LT; SUB_REFL; MULT_CLAUSES];
    ALL_TAC] THEN
  FIRST_X_ASSUM(MP_TAC o REWRITE_RULE[NOT_LT; LE_EXISTS]) THEN
  DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC) THEN
  REWRITE_TAC[GSYM ADD_ASSOC; ADD_SUB; ADD_SUB2] THEN
  MP_TAC(SPECL [`d + 1`; `k:num`] BINOM_FACT) THEN
  MP_TAC(SPECL [`d:num`; `k:num`] BINOM_FACT) THEN
  REWRITE_TAC[GSYM ADD1; ADD_CLAUSES; FACT; ADD_AC] THEN
  MAP_EVERY (fun t -> MP_TAC(SPEC t FACT_LT)) [`d:num`; `k:num`] THEN
  REWRITE_TAC[LT_NZ] THEN CONV_TAC NUM_RING);;

let BINOM_BOTTOM_STEP = prove
 (`!n k. (k + 1) * binom(n,k + 1) = (n - k) * binom(n,k)`,
  REPEAT GEN_TAC THEN ASM_CASES_TAC `n < k + 1` THENL
   [FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP
     (ARITH_RULE `n < k + 1 ==> n = k \/ n < k`)) THEN
    ASM_SIMP_TAC[BINOM_LT; SUB_REFL; MULT_CLAUSES];
    ALL_TAC] THEN
  FIRST_X_ASSUM(MP_TAC o REWRITE_RULE[NOT_LT; LE_EXISTS]) THEN
  DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC) THEN
  REWRITE_TAC[GSYM ADD_ASSOC; ADD_SUB; ADD_SUB2] THEN
  MP_TAC(SPECL [`d + 1`; `k:num`] BINOM_FACT) THEN
  MP_TAC(SPECL [`d:num`; `k + 1`] BINOM_FACT) THEN
  REWRITE_TAC[GSYM ADD1; ADD_CLAUSES; FACT; ADD_AC] THEN
  MAP_EVERY (fun t -> MP_TAC(SPEC t FACT_LT)) [`d:num`; `k:num`] THEN
  REWRITE_TAC[LT_NZ] THEN CONV_TAC NUM_RING);;

(* ------------------------------------------------------------------------- *)
(* Binomial expansion.                                                       *)
(* ------------------------------------------------------------------------- *)

let BINOMIAL_THEOREM = prove
 (`!n x y.
      (x + y) EXP n = nsum(0..n) (\k. binom(n,k) * x EXP k * y EXP (n - k))`,
  INDUCT_TAC THEN REPEAT GEN_TAC THEN ASM_REWRITE_TAC[EXP] THEN
  REWRITE_TAC[NSUM_SING_NUMSEG; binom; SUB_REFL; EXP; MULT_CLAUSES] THEN
  SIMP_TAC[NSUM_CLAUSES_LEFT; ADD1; ARITH_RULE `0 <= n + 1`; NSUM_OFFSET] THEN
  ASM_REWRITE_TAC[EXP; binom; GSYM ADD1; GSYM NSUM_LMUL] THEN
  REWRITE_TAC[RIGHT_ADD_DISTRIB; NSUM_ADD_NUMSEG; MULT_CLAUSES; SUB_0] THEN
  MATCH_MP_TAC(ARITH_RULE `a = e /\ b = c + d ==> a + b = c + d + e`) THEN
  CONJ_TAC THENL [REWRITE_TAC[MULT_AC; SUB_SUC]; REWRITE_TAC[GSYM EXP]] THEN
  SIMP_TAC[ADD1; SYM(REWRITE_CONV[NSUM_OFFSET]`nsum(m+1..n+1) (\i. f i)`)] THEN
  REWRITE_TAC[NSUM_CLAUSES_NUMSEG; GSYM ADD1; LE_SUC; LE_0] THEN
  SIMP_TAC[NSUM_CLAUSES_LEFT; LE_0] THEN
  SIMP_TAC[BINOM_LT; LT; MULT_CLAUSES; ADD_CLAUSES; SUB_0; EXP; binom] THEN
  SIMP_TAC[ARITH; ARITH_RULE `k <= n ==> SUC n - k = SUC(n - k)`; EXP] THEN
  REWRITE_TAC[MULT_AC]);;

(* ------------------------------------------------------------------------- *)
(* Same thing for the reals.                                                 *)
(* ------------------------------------------------------------------------- *)

prioritize_real();;

let REAL_BINOMIAL_THEOREM = prove
 (`!n x y.
     (x + y) pow n = sum(0..n) (\k. &(binom(n,k)) * x pow k * y pow (n - k))`,
  INDUCT_TAC THEN REPEAT GEN_TAC THEN ASM_REWRITE_TAC[real_pow] THEN
  REWRITE_TAC[SUM_SING_NUMSEG; binom; SUB_REFL; real_pow; REAL_MUL_LID] THEN
  SIMP_TAC[SUM_CLAUSES_LEFT; ADD1; ARITH_RULE `0 <= n + 1`; SUM_OFFSET] THEN
  ASM_REWRITE_TAC[real_pow; binom; GSYM ADD1; GSYM SUM_LMUL] THEN
  REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN
  REWRITE_TAC[REAL_ADD_RDISTRIB; SUM_ADD_NUMSEG; REAL_MUL_LID; SUB_0] THEN
  MATCH_MP_TAC(ARITH_RULE `a = e /\ b = c + d ==> a + b = c + d + e`) THEN
  CONJ_TAC THENL [SIMP_TAC[REAL_MUL_AC; SUB_SUC]; SIMP_TAC[GSYM real_pow]] THEN
  SIMP_TAC[ADD1; SYM(REWRITE_CONV[SUM_OFFSET]`sum(m+1..n+1) (\i. f i)`)] THEN
  REWRITE_TAC[SUM_CLAUSES_NUMSEG; GSYM ADD1; LE_SUC; LE_0] THEN
  SIMP_TAC[SUM_CLAUSES_LEFT; LE_0; BINOM_LT; LT; REAL_MUL_LID; SUB_0; real_pow;
           binom; REAL_MUL_LZERO; REAL_ADD_RID] THEN
  SIMP_TAC[ARITH; ARITH_RULE `k <= n ==> SUC n - k = SUC(n - k)`; real_pow] THEN
  REWRITE_TAC[REAL_MUL_AC]);;

(* ------------------------------------------------------------------------- *)
(* More direct stepping theorems over the reals.                             *)
(* ------------------------------------------------------------------------- *)

let BINOM_TOP_STEP_REAL = prove
 (`!n k. &(binom(n + 1,k)) =
           if k = n + 1 then &1
           else (&n + &1) / (&n + &1 - &k) * &(binom(n,k))`,
  REPEAT STRIP_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[BINOM_REFL] THEN
  FIRST_X_ASSUM(STRIP_ASSUME_TAC o MATCH_MP (ARITH_RULE
   `~(k = n + 1) ==> n < k /\ n + 1 < k \/ k <= n /\ k <= n + 1`)) THEN
  ASM_SIMP_TAC[BINOM_LT; REAL_MUL_RZERO] THEN
  MP_TAC(SPECL [`n:num`; `k:num`] BINOM_TOP_STEP) THEN
  ASM_SIMP_TAC[GSYM REAL_OF_NUM_EQ; GSYM REAL_OF_NUM_MUL; GSYM REAL_OF_NUM_ADD;
               GSYM REAL_OF_NUM_SUB] THEN
  UNDISCH_TAC `k <= n:num` THEN REWRITE_TAC[GSYM REAL_OF_NUM_LE] THEN
  CONV_TAC REAL_FIELD);;

let BINOM_BOTTOM_STEP_REAL = prove
 (`!n k. &(binom(n,k+1)) = (&n - &k) / (&k + &1) * &(binom(n,k))`,
  REPEAT GEN_TAC THEN DISJ_CASES_TAC(ARITH_RULE `n:num < k \/ k <= n`) THENL
   [ASM_SIMP_TAC[BINOM_LT; ARITH_RULE `n < k ==> n < k + 1`; REAL_MUL_RZERO];
    MP_TAC(SPECL [`n:num`; `k:num`] BINOM_BOTTOM_STEP) THEN
    ASM_SIMP_TAC[GSYM REAL_OF_NUM_EQ; GSYM REAL_OF_NUM_MUL;
                 GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_SUB] THEN
    CONV_TAC REAL_FIELD]);;

let REAL_OF_NUM_BINOM = prove
 (`!n k. &(binom(n,k)) =
             if k <= n then &(FACT n) / (&(FACT(n - k)) * &(FACT k))
             else &0`,
  REPEAT GEN_TAC THEN COND_CASES_TAC THEN
  ASM_SIMP_TAC[BINOM_LT; GSYM NOT_LE] THEN
  SIMP_TAC[REAL_EQ_RDIV_EQ; REAL_LT_MUL; REAL_OF_NUM_LT; FACT_LT] THEN
  FIRST_ASSUM(CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[LE_EXISTS]) THEN
  REWRITE_TAC[ADD_SUB2] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
  REWRITE_TAC[GSYM BINOM_FACT] THEN REWRITE_TAC[REAL_OF_NUM_MUL; MULT_AC]);;

(* ------------------------------------------------------------------------- *)
(* Some additional theorems for stepping both arguments together.            *)
(* ------------------------------------------------------------------------- *)

let BINOM_BOTH_STEP_REAL = prove
 (`!p k. &(binom(p + 1,k + 1)) = (&p + &1) / (&k + &1) * &(binom(p,k))`,
  REWRITE_TAC[BINOM_TOP_STEP_REAL; BINOM_BOTTOM_STEP_REAL] THEN
  REPEAT GEN_TAC THEN REWRITE_TAC[EQ_ADD_RCANCEL] THEN
  COND_CASES_TAC THEN ASM_REWRITE_TAC[BINOM_REFL] THEN POP_ASSUM MP_TAC THEN
  REWRITE_TAC[GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_EQ] THEN
  CONV_TAC REAL_FIELD);;

let BINOM_BOTH_STEP = prove
 (`!p k. (k + 1) * binom(p + 1,k + 1) = (p + 1) * binom(p,k)`,
  REWRITE_TAC[GSYM REAL_OF_NUM_EQ; GSYM REAL_OF_NUM_MUL] THEN
  REWRITE_TAC[BINOM_BOTH_STEP_REAL; GSYM REAL_OF_NUM_ADD] THEN
  CONV_TAC REAL_FIELD);;

let BINOM_BOTH_STEP_DOWN = prove
 (`!p k. (k = 0 ==> p = 0) ==> k * binom(p,k) = p * binom(p - 1,k - 1)`,
  REPEAT INDUCT_TAC THEN
  SIMP_TAC[BINOM_LT; LT_0; LT_REFL; ARITH] THEN
  REWRITE_TAC[SUC_SUB1; ADD1; BINOM_BOTH_STEP] THEN
  REWRITE_TAC[MULT_CLAUSES]);;

let BINOM = prove
 (`!n k. binom(n,k) =
            if k <= n then FACT(n) DIV (FACT(n - k) * FACT(k))
            else 0`,
  REPEAT GEN_TAC THEN COND_CASES_TAC THEN
  ASM_SIMP_TAC[BINOM_EQ_0; GSYM NOT_LE] THEN CONV_TAC SYM_CONV THEN
  MATCH_MP_TAC DIV_UNIQ THEN EXISTS_TAC `0` THEN
  SIMP_TAC[LT_MULT; FACT_LT; ADD_CLAUSES] THEN
  FIRST_X_ASSUM(CHOOSE_THEN SUBST1_TAC o GEN_REWRITE_RULE I [LE_EXISTS]) THEN
  ONCE_REWRITE_TAC[ADD_SYM] THEN
  REWRITE_TAC[GSYM BINOM_FACT; ADD_SUB] THEN REWRITE_TAC[MULT_AC]);;

(* ------------------------------------------------------------------------- *)
(* Additional lemmas.                                                        *)
(* ------------------------------------------------------------------------- *)

let BINOM_SYM = prove
 (`!n k. binom(n,n-k) = if k <= n then binom(n,k) else 1`,
  REPEAT GEN_TAC THEN COND_CASES_TAC THEN
  ASM_SIMP_TAC[binom; ARITH_RULE `~(k <= n) ==> n - k = 0`] THEN
  REWRITE_TAC[GSYM REAL_OF_NUM_EQ; REAL_OF_NUM_BINOM] THEN
  ASM_REWRITE_TAC[ARITH_RULE `n - k:num <= n`] THEN
  ASM_SIMP_TAC[ARITH_RULE `k:num <= n ==> n - (n - k) = k`] THEN
  REWRITE_TAC[REAL_OF_NUM_MUL; MULT_SYM]);;

let BINOM_MUL_SHIFT = prove
 (`!m n k. k <= m
           ==> binom(n,m) * binom(m,k) = binom(n,k) * binom(n - k,m - k)`,
  REPEAT STRIP_TAC THEN
  SIMP_TAC[GSYM REAL_OF_NUM_EQ; GSYM REAL_OF_NUM_MUL; REAL_OF_NUM_BINOM] THEN
  ASM_CASES_TAC `n:num < m` THENL
   [REPEAT(COND_CASES_TAC THEN
      ASM_REWRITE_TAC[REAL_MUL_LZERO; REAL_MUL_RZERO]) THEN
    MATCH_MP_TAC(TAUT `F ==> p`) THEN ASM_ARITH_TAC;
    REPEAT(COND_CASES_TAC THENL
     [ALL_TAC; MATCH_MP_TAC(TAUT `F ==> p`) THEN  ASM_ARITH_TAC]) THEN
    RULE_ASSUM_TAC(REWRITE_RULE[NOT_LT]) THEN
    ASM_SIMP_TAC[ARITH_RULE
     `k:num <= m /\ m <= n ==> n - k - (m - k) = n - m`] THEN
    MAP_EVERY (MP_TAC o C SPEC FACT_NZ)
     [`n:num`; `m:num`; `n - m:num`; `n - k:num`; `m - k:num`] THEN
    REWRITE_TAC[GSYM REAL_OF_NUM_EQ] THEN CONV_TAC REAL_FIELD]);;

let APPELL_SEQUENCE = prove
 (`!c n x y. sum (0..n)
               (\k.  &(binom(n,k)) *
                     sum(0..k)
                        (\l. &(binom(k,l)) * c l * x pow (k - l)) *
                     y pow (n - k)) =
           sum (0..n) (\k. &(binom(n,k)) * c k * (x + y) pow (n - k))`,
  REPEAT GEN_TAC THEN REWRITE_TAC[REAL_BINOMIAL_THEOREM] THEN
  REWRITE_TAC[GSYM SUM_LMUL; GSYM SUM_RMUL] THEN
  SIMP_TAC[SUM_SUM_PRODUCT; FINITE_NUMSEG] THEN
  MATCH_MP_TAC SUM_EQ_GENERAL_INVERSES THEN
  EXISTS_TAC `(\(x,y). y,x - y):num#num->num#num` THEN
  EXISTS_TAC `(\(x,y). x + y,x):num#num->num#num` THEN
  REWRITE_TAC[FORALL_IN_GSPEC; IN_ELIM_PAIR_THM] THEN
  REWRITE_TAC[PAIR_EQ; IN_NUMSEG] THEN
  CONJ_TAC THENL [ARITH_TAC; REPEAT GEN_TAC THEN STRIP_TAC] THEN
  REPEAT(CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC]) THEN
  ASM_SIMP_TAC[ARITH_RULE
   `j:num <= k /\ k <= n ==> (n - j) - (k - j) = n - k`] THEN
  MATCH_MP_TAC(REAL_RING
   `c * d:real = a * b ==> a * z * b * x * y = c * (d * z * x) * y`) THEN
  ASM_SIMP_TAC[REAL_OF_NUM_MUL; REAL_OF_NUM_EQ; BINOM_MUL_SHIFT]);;

(* ------------------------------------------------------------------------- *)
(* Numerical computation of binom.                                           *)
(* ------------------------------------------------------------------------- *)

let NUM_BINOM_CONV =
  let pth_step = prove
   (`binom(n,k) = y
     ==> k <= n
         ==> (SUC n) * y = ((n + 1) - k) * x ==> binom(SUC n,k) = x`,
    DISCH_THEN(SUBST1_TAC o SYM) THEN
    REWRITE_TAC[ADD1; GSYM BINOM_TOP_STEP; EQ_MULT_LCANCEL; SUB_EQ_0] THEN
    ARITH_TAC)
  and pth_0 = prove
   (`n < k ==> binom(n,k) = 0`,
    REWRITE_TAC[BINOM_LT])
  and pth_1 = prove
   (`binom(n,n) = 1`,
    REWRITE_TAC[BINOM_REFL])
  and pth_swap = prove
   (`k <= n ==> binom(n,k) = binom(n,n - k)`,
    MESON_TAC[BINOM_SYM])
  and k_tm = `k:num` and n_tm = `n:num`
  and x_tm = `x:num` and y_tm = `y:num`
  and binom_tm = `binom` in
  let rec BINOM_RULE(n,k) =
    if n </ k then
      let th = INST [mk_numeral n,n_tm; mk_numeral k,k_tm] pth_0 in
      MP_CONV NUM_LT_CONV th
    else if n =/ k then
      INST [mk_numeral n,n_tm] pth_1
    else if Int 2 */ k </ n then
      let th1 = INST [mk_numeral n,n_tm; mk_numeral k,k_tm] pth_swap in
      let th2 = MP th1 (EQT_ELIM(NUM_LE_CONV (lhand(concl th1)))) in
      let th3 = CONV_RULE(funpow 3 RAND_CONV NUM_SUB_CONV) th2 in
      TRANS th3 (BINOM_RULE(n,n -/ k))
    else
      let th1 = BINOM_RULE(n -/ Int 1,k) in
      let y = dest_numeral(rand(concl th1)) in
      let x = (n // (n -/ k)) */ y in
      let th2 = INST [mk_numeral(n -/ Int 1),n_tm; mk_numeral k,k_tm;
                      mk_numeral x,x_tm; mk_numeral y,y_tm] pth_step in
      let th3 = MP_CONV NUM_REDUCE_CONV (MP_CONV NUM_LE_CONV (MP th2 th1)) in
      CONV_RULE (LAND_CONV(RAND_CONV(LAND_CONV NUM_SUC_CONV))) th3 in
  fun tm ->
    let bop,nkp = dest_comb tm in
    if bop <> binom_tm then failwith "NUM_BINOM_CONV" else
    let nt,kt = dest_pair nkp in
    BINOM_RULE(dest_numeral nt,dest_numeral kt);;