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