# [isabelle] Binomial Coefficient as Factorial

Dear all,
Hi, in Isabelle the definition we have for Binomial Coefficient is:
primrec binomial :: "nat â nat â nat" (infixl "choose" 65)
where
"0 choose k = (if k = 0 then 1 else 0)"
| "Suc n choose k = (if k = 0 then 1 else (n choose (k - 1)) + (n choose
k))"
But according to my (limited) number theory knowledge, n choose k can also
be calculated using factorials and n choose k = n! / k! *(n-k)!.
So I want to prove the following lemma:
fun fac :: "nat â nat" where
"fac 0 = Suc 0"
| "fac n = n * fac (n - 1)"
lemma bin_as_fac[simp]:"n choose k = fac n div ((fac k) * fac (n - k))"
try
When I typed try Isabelle quickly found a counter example for me,
n = 0
k = Suc 0
Evaluated terms:
n choose k = 0
fac n div (fac k * fac (n - k)) = Suc 0
I am just wondering where did things went wrong? Is the two calculation of
binomial coefficient not compatible with each other?
Thanks a lot.
Best,
Bob
--
Boyu Fang

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*