[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)


  "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

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))"


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.




Boyu Fang

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