[isabelle-dev] New (Co)datatypes: Status & Plan (FYI)

[Alexander Krauss]

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