Email Gateway (Apr 15 2024 at 08:55): Email Gateway (Apr 15 2024 at 08:55):From: Peter Lammich <cl-isabelle-users@lists.cam.ac.uk>
Dear list,
I've encountered the following unexpected behavior of the function
package. Defining a primitive recursive function with fun yields a THM
exception, if
the recursion goes through a Bex and an If. Using Ex x. x:A & ...
instead of Bex, or using primrec, works though. Is this behaviour to be
expected?
Broken down example below.
(note, I'm still on Isabelle 2023)
Email Gateway (Apr 15 2024 at 12:42):From: Manuel Eberl <manuel@pruvisto.org>
For reference, here is the exception trace. Just from looking at it, it
seems to me like this could be an issue with η-expansion. The premise in
the implication is exactly the same as the theorem with which it is to
be eliminated, except for η-expansion.
I don't know that code in the function package at all; I am not even
sure what it does. The obvious solution would be to eta-contract before
applying this elimination, but it would be good to investigate if there
is some deeper systemic problem here. After all, η-expansion/contraction
regularly causes problems like this.
Cheers,
Manuel
Last updated: May 05 2024 at 04:19 UTC