Email Gateway (Aug 22 2022 at 15:35): Email Gateway (Aug 22 2022 at 15:35):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Isabelle experts,
I'd like to automate a bunch of constructions and proofs about recursive functions that
are defined with the function package. They would be easy to express and implement if the
functions were expressible using the wfrec combinator from Wfrec.thy, which had been used
by the old recdef package. Clearly, not all features that the function package supports
can be easily expressed using wfrec. From my experience, leaving localisation aside,
almost all the functions I have defined with fun/function fall within the fragment
supported by recdef + currying. So I wonder whether there already exists some (automatic)
way to get a wfrec characterisation for a function defined with the function package.
Would other people/tools also find such a characterisation useful?
Best,
Andreas
Last updated: Apr 26 2024 at 12:28 UTC