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

[Alexander Krauss]

Hi Jasmin,

On 07/30/2013 05:40 PM, Jasmin Christian Blanchette wrote:
> A rough, optimistic time plan follows.
[...]

Wow, I'm looking forward to it!

Let me quickly review the dependencies of the function package on the
datatype package:

- The package registers a datatype interpretation to generate congruence
rules the case combinator for each type.

- The pattern splitting code and the pat_completeness method both
retrieves the constructors for a given type, using Datatype.get_constrs.

- The pat_completeness method also uses the exhaust theorem.

- partial_function also destructs the case combinator and looks up
rewrite rules for it.

- The automated pattern proofs implicitly invoked by "fun" (essentially,
the "auto" method) rely implicitly on various things in the simpset, in
particular the distinctness and injectivity simp rules. This is the only
situation where freeness is used.

- 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.


In summary, except for the size functions which are somewhat special
(and only used for termination proofs), the function package never uses
any inductiveness and would happily swallow codatatypes as well.

Thus, I would propose to model the concept of a "type made of
constructors" explicitly as a declaration which other tools can look up
and add further interpretations to (in the sense of datatype
interpretations). The function package would only depend on that. If I
understand correctly, that declaration would essentially be rep_datatype
without the induction rule. The function package (and I assume other
tools, such as case syntax generation) can only rely on that and thus
treat datatypes and codadatypes uniformly.

But, according to your schedule, these considerations become important
only after the coming release, so I'll shut up for the moment.

> The corecursive counterpart to "fun", corecursion up-to, is something
> Andrei urges us to work on, but where Dmitry and I are applying the
> brakes because of the pile of work that remains to be done on the new
> (co)datatype package before we can consider adding such nice
> features. In fact, inspired by Leino et al.'s (co)recursion mixture
> in Dafny [*], Andrei has some ideas to support some recursion in
> conjuction with corecursion up-to.

I'd like to learn about corecursion up-to, which I have not come across 
so far. Are there any good references for this? Or should I rather have 
a beer with Andrei?


Alex