1 (* ========================================================================= *)
2 (* Binomial coefficients and the binomial theorem. *)
3 (* ========================================================================= *)
7 (* ------------------------------------------------------------------------- *)
8 (* Binomial coefficients. *)
9 (* ------------------------------------------------------------------------- *)
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))`;;
17 (`!n. binom(0,n) = if n = 0 then 1 else 0`,
18 INDUCT_TAC THEN REWRITE_TAC[binom; NOT_SUC]);;
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]);;
25 let BINOM_REFL = prove
26 (`!n. binom(n,n) = 1`,
27 INDUCT_TAC THEN ASM_SIMP_TAC[binom; BINOM_LT; LT; ARITH]);;
30 (`!n. binom(n,1) = n`,
31 REWRITE_TAC[num_CONV `1`] THEN
32 INDUCT_TAC THEN ASM_REWRITE_TAC[binom] THEN ARITH_TAC);;
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);;
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]);;
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]]);;
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);;
66 (* ------------------------------------------------------------------------- *)
67 (* More potentially useful lemmas. *)
68 (* ------------------------------------------------------------------------- *)
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];
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);;
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];
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);;
102 (* ------------------------------------------------------------------------- *)
103 (* Binomial expansion. *)
104 (* ------------------------------------------------------------------------- *)
106 let BINOMIAL_THEOREM = prove
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]);;
123 (* ------------------------------------------------------------------------- *)
124 (* Same thing for the reals. *)
125 (* ------------------------------------------------------------------------- *)
129 let REAL_BINOMIAL_THEOREM = prove
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]);;
147 (* ------------------------------------------------------------------------- *)
148 (* More direct stepping theorems over the reals. *)
149 (* ------------------------------------------------------------------------- *)
151 let BINOM_TOP_STEP_REAL = prove
152 (`!n k. &(binom(n + 1,k)) =
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);;
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]);;
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))
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]);;
185 (* ------------------------------------------------------------------------- *)
186 (* Some additional theorems for stepping both arguments together. *)
187 (* ------------------------------------------------------------------------- *)
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);;
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);;
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]);;
212 if k <= n then FACT(n) DIV (FACT(n - k) * FACT(k))
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]);;
222 (* ------------------------------------------------------------------------- *)
223 (* Additional lemmas. *)
224 (* ------------------------------------------------------------------------- *)
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]);;
235 let BINOM_MUL_SHIFT = prove
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]);;
253 let APPELL_SEQUENCE = prove
254 (`!c n x y. sum (0..n)
257 (\l. &(binom(k,l)) * c l * x pow (k - l)) *
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]);;
276 (* ------------------------------------------------------------------------- *)
277 (* Numerical computation of binom. *)
278 (* ------------------------------------------------------------------------- *)
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
289 (`n < k ==> binom(n,k) = 0`,
290 REWRITE_TAC[BINOM_LT])
293 REWRITE_TAC[BINOM_REFL])
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) =
302 let th = INST [mk_numeral n,n_tm; mk_numeral k,k_tm] pth_0 in
303 MP_CONV NUM_LT_CONV th
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))
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
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);;