[isabelle-dev] HOL-Codegenerator_Test error
Andreas Lochbihler
andreas.lochbihler at inf.ethz.ch
Tue Jan 12 10:16:04 CET 2016
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
More information about the isabelle-dev
mailing list