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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
