[isabelle-dev] docs for new datatype package

[Gerwin Klein]

>> How long did we plan on keeping the old datatype package around?
>
> For as long as this is necessary.

Sounds encouraging ;-)


> However, surely the situation is not as bleak as you appear to think, if those 3000 lines are all there is.

It’s not so much about the size, more about the messiness. I gave up the first pass after less than 20% into the file..


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

Thanks for that pointer. FOL-Fitting looks reasonably well behaved with its 2-way nesting. This file has 4-way nesting and something seems to have changed in the order of the subgoals that the induction leaves, which makes the unstructured apply scripts a pain to update.

Is the goal order sensitive to the order I give the induct rules in, the induction statement, or the primrec equations, or all of these?

And of course these horrid proofs rely on Isabelle-generated names all over the place. That needs to be fixed in any case, though.


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

Maybe datatype_compat is the one I should go with for now. Need to check if that has an influence on the induction order.


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

I don’t think I really need the specific semantics, but I’m having a hard time understanding what the actual problem is. In particular, it is this lemma td_set_size_lte’ and the few corollaries following it

https://github.com/seL4/l4v/blob/2015/tools/c-parser/umm_heap/CTypes.thy#L578

lemma td_set_size_lte’ doesn’t seem to be provable any more if you dig into it a bit and the corollaries don’t seem to follow any more either. Replicating the old size definition would probably do it, but it would be nice not to have to.

(You should be able to just clone the 2015 branch of this repo and load up the file in JEdit with base logic HOL if you want to see what’s going on).

I have the feeling that a real overhaul of this file should use mapping functions to reduce the nesting, but that’s more than I have time for at the moment.

Cheers,
Gerwin



________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.