equal
deleted
inserted
replaced
1 (* Title: HOL/Binomial.thy |
1 (* Title: HOL/Binomial.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson |
3 Author: Lawrence C Paulson |
4 Copyright 1997 University of Cambridge |
4 Copyright 1997 University of Cambridge |
5 |
|
6 *) |
5 *) |
7 |
6 |
8 header{*Binomial Coefficients*} |
7 header{*Binomial Coefficients*} |
9 |
8 |
10 theory Binomial |
9 theory Binomial |
11 imports SetInterval |
10 imports GCD |
12 begin |
11 begin |
13 |
12 |
14 text{*This development is based on the work of Andy Gordon and |
13 text{*This development is based on the work of Andy Gordon and |
15 Florian Kammueller*} |
14 Florian Kammueller*} |
16 |
15 |
22 |
21 |
23 binomial_Suc: "(Suc n choose k) = |
22 binomial_Suc: "(Suc n choose k) = |
24 (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))" |
23 (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))" |
25 |
24 |
26 lemma binomial_n_0 [simp]: "(n choose 0) = 1" |
25 lemma binomial_n_0 [simp]: "(n choose 0) = 1" |
27 by (case_tac "n", simp_all) |
26 by (cases n) simp_all |
28 |
27 |
29 lemma binomial_0_Suc [simp]: "(0 choose Suc k) = 0" |
28 lemma binomial_0_Suc [simp]: "(0 choose Suc k) = 0" |
30 by simp |
29 by simp |
31 |
30 |
32 lemma binomial_Suc_Suc [simp]: |
31 lemma binomial_Suc_Suc [simp]: |
186 also have "\<dots> = (\<Sum>k=0..n+1. (n+1 choose k) * a^k * b^(n+1-k))" |
185 also have "\<dots> = (\<Sum>k=0..n+1. (n+1 choose k) * a^k * b^(n+1-k))" |
187 using decomp by simp |
186 using decomp by simp |
188 finally show ?case by simp |
187 finally show ?case by simp |
189 qed |
188 qed |
190 |
189 |
191 ML |
|
192 {* |
|
193 val binomial_n_0 = thm"binomial_n_0"; |
|
194 val binomial_0_Suc = thm"binomial_0_Suc"; |
|
195 val binomial_Suc_Suc = thm"binomial_Suc_Suc"; |
|
196 val binomial_eq_0 = thm"binomial_eq_0"; |
|
197 val binomial_n_n = thm"binomial_n_n"; |
|
198 val binomial_Suc_n = thm"binomial_Suc_n"; |
|
199 val binomial_1 = thm"binomial_1"; |
|
200 val zero_less_binomial = thm"zero_less_binomial"; |
|
201 val binomial_eq_0_iff = thm"binomial_eq_0_iff"; |
|
202 val zero_less_binomial_iff = thm"zero_less_binomial_iff"; |
|
203 val Suc_times_binomial_eq = thm"Suc_times_binomial_eq"; |
|
204 val binomial_Suc_Suc_eq_times = thm"binomial_Suc_Suc_eq_times"; |
|
205 val times_binomial_minus1_eq = thm"times_binomial_minus1_eq"; |
|
206 *} |
|
207 |
|
208 end |
190 end |