[isabelle-dev] docs for new datatype package

[Jasmin Blanchette]

Hi Gerwin,

> On 19.04.2015, at 20:25, Gerwin Klein <Gerwin.Klein at nicta.com.au> wrote:
> 
> Thanks for updating.
> 
> Currently trying to pull through proofs in https://github.com/seL4/l4v/blob/master/tools/c-parser/umm_heap/CTypes.thy
> 
> They are unfortunately pretty horrid to start with (violating half of our own style/maintenance rules), additionally contain lots of nested recursion and some proofs about size_t functions that seem to have changed quite a bit. I’m tempted to use old_datatype here.
> 
> How long did we plan on keeping the old datatype package around?

For as long as this is necessary. However, surely the situation is not as bleak as you appear to think, if those 3000 lines are all there is. I was able to port the whole AFP to the new datatype package over the course of two weeks or so, during which most of my time went into fixing bugs in the package itself. Using “datatype_compat”, or even just “f.induct” etc. for “f” defined using “primrec”, you should be able to keep the same nested-as-mutual recursion idioms without using “old_datatype”. My changes to the “FOL-Fitting” entry can be instructive in this regard.

At some point, I want to add an option to “datatype” to generate “nested-as-mutual” theorems without needing either “datatype_compat” nor a “primrec” definition, but there’s no big harm in using “datatype_compat” for this until this happens.

As for “size”, I’d be curious to know what the exact issue is. It did change, and there are some incompatibilities (typically off-by-ones), but if you can tell me a bit more what you’re doing, I might be able to help here. In the worst case, it’s always possible (and not very difficult) to define “size” manually, if you need a specific semantics.

Also, the IsaFoR guys have quite some expertise at porting code from the old to the new datatypes, including the nested business and size. Maybe they’ll have one or two hints, once we know better what you want to do.

In short: “old_datatype” is probably overkill here.

Jasmin