Hi Jasmin,
On 08/06/2013 01:59 AM, Jasmin Blanchette wrote:
- The package registers a datatype interpretation to generate
congruence rules the case combinator for each type.
I guess it would make sense to have the package do that, or is there
a specific reason why it is better to do it in a function-related
extension?
It is just about decoupling things: The current picture is that datatype
and core function do not know each other. "fun" (which is an extra layer
on top of function) combines them by means of the datatype interpretation.
[...]
- The generation of size functions (which was moved into the
Function/ subdirectory at some point, but without any real reason)
is extremely cryptic. This is mostly because it does a too complex
task, essentially reversing the nested-to-mutual conversion in this
particular instance. It appears that this should be re-done
completely based on the infrastructure of the new package, and it
would probably become much simpler.
Probably. But Dmitriy told me you had a different idea on how to do
this, based on well-founded relations instead of size functions? Do
you remember what that could be and if so would you be willing to
elaborate?
The point was just that size functions to "nat" are too weak for some
cases, which is the only conceptual point where "fun" does not subsume
"primrec". So theoretically it would be better to switch to either
ordinals or well-founded relations (with some sort of composition
principle).
However, one would need very robust automation for things like ordinal
arithmetic, to make the termination prover really work. This is
overkill, just for the sake of these rare examples involving
infinitely-branching recursion. So we should leave it as it is.
In principle, the datatype package could also just generate a wf
relation for use in manual termination proofs. This might make sense,
but you clearly have more important things to do just now.
Alex
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
