[isabelle-dev] docs for new datatype package

[Jasmin Blanchette]

Hi Gerwin,

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

I don’t entirely understand what some of the suggested “dependencies” are, but if you are using the induction schemes generated by “primrec” I can’t guarantee that the order will be the same as it used to be. It might be that the order of the primrec equations have an impact. But:

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

“datatype_compat” should give exactly the same induction principle as before, modulo naming of its schematic variables, even in the presence of 4-way nesting.

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

OK, I’m also a bit time-limited at the moment but will look into this once I get a chance. Let me know if you discover anything important until then. I suspect the above issue is just an instance of the “off-by-one” issue I mentioned. With the old package, the “size” overloaded instance did not always coincide with the more general “size_t” function, which I found unsatisfactory both on aesthetic grounds and to avoid duplicating proofs. A simple example is

    thm option.size

which used to be

  size_sum ?fa ?fb (Inl ?a) = ?fa ?a + Suc 0
  size (Inl ?a) = 0

whereas now “size (Inl _) = Suc 0” for consistency with “size_sum” (by taking ?fa = ?fb = %_. 0).

Sorry about the trouble.

Jasmin