[isabelle-dev] New (Co)datatypes: Status & Plan (FYI)
krauss at in.tum.de
Wed Aug 21 00:03:20 CEST 2013
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
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
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
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.
More information about the isabelle-dev