[isabelle-dev] HOL-Codegenerator_Test error

[Manuel Eberl]

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