# Re: [isabelle] Binomial Coefficient as Factorial

The problem is quite simply that these two definitions of the binomial
coefficient are only equivalent for 0 â k â n. You may be interested in
the lemma binomial_altdef_nat from the Isabelle library:
k â n â n choose k = fact n div (fact k * fact (n - k))
On 28/02/15 16:32, Bob Fang wrote:
> 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
>

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