equal
deleted
inserted
replaced
1 (* Title: HOL/Binomial.thy |
1 (* Title: HOL/Binomial.thy |
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Amine Chaieb |
2 Author: Lawrence C Paulson, Amine Chaieb |
4 Copyright 1997 University of Cambridge |
3 Copyright 1997 University of Cambridge |
5 *) |
4 *) |
6 |
5 |
7 header {* Binomial Coefficients *} |
6 header {* Binomial Coefficients *} |
11 begin |
10 begin |
12 |
11 |
13 text {* This development is based on the work of Andy Gordon and |
12 text {* This development is based on the work of Andy Gordon and |
14 Florian Kammueller. *} |
13 Florian Kammueller. *} |
15 |
14 |
16 consts |
15 primrec binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat" (infixl "choose" 65) where |
17 binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat" (infixl "choose" 65) |
|
18 primrec |
|
19 binomial_0: "(0 choose k) = (if k = 0 then 1 else 0)" |
16 binomial_0: "(0 choose k) = (if k = 0 then 1 else 0)" |
20 binomial_Suc: "(Suc n choose k) = |
17 | binomial_Suc: "(Suc n choose k) = |
21 (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))" |
18 (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))" |
22 |
19 |
23 lemma binomial_n_0 [simp]: "(n choose 0) = 1" |
20 lemma binomial_n_0 [simp]: "(n choose 0) = 1" |
24 by (cases n) simp_all |
21 by (cases n) simp_all |
25 |
22 |