# [isabelle-dev] HOL-Codegenerator_Test error

Manuel Eberl eberlm at in.tum.de
Tue Jan 12 09:56:10 CET 2016

```I tried to trace this issue and I am really confused now.

The problem is apparently the following code equation I added for
"binomial" at the end of Binomial.thy:

lemma binomial_code [code]:
"(n choose k) =
(if k > n then 0
else if 2 * k > n then (n choose (n - k))
else (fold_atLeastAtMost_nat (op *) (n-k+1) n 1 div fact k))"

If I delete this rule, everything works again. I then tried the
following, which also produces the same error:

lemma binomial_code [code]:
"n choose k = (if k ≤ n then fact n div (fact k * fact (n - k)) else 0)"

The following two, on the other hand, work:

lemma binomial_code [code]:
"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))"

lemma binomial_code [code]:
"n choose k = (if k = 0 then 1 else if n = 0 then 0 else ((n - 1) choose
(k - 1)) + ((n - 1) choose k))"

So I thought maybe the "fact" is the problem, but the following works as
well, even though it contains "fact":

lemma binomial_code [code]:
"n choose k =
(if k = 0 then 1 else if n = 0 ∧ fact n = fact n then 0 else ((n -
1) choose (k - 1)) + ((n - 1) choose k))"

Does anybody have any idea what is going on here?

Manuel

```