[isabelle-dev] HOL-Codegenerator_Test error

[Andreas Lochbihler]

Dear Manuel,

I have not tried this explicitly, but it looks like the standard problem with type classes 
in Scala (see section 7.1 in the code generator tutorial). Probably the problematic code 
equations use two type classes with an operation inherited from the same anchestor. The 
error message in the start of this thread hints at this problem. So you best introduce a 
special type class for Scala (as has already been done for others in the code generator 
tests).

Hope this helps,
Andreas

On 12/01/16 09:56, Manuel Eberl wrote:
> 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev