[isabelle-dev] docs for new datatype package

[Gerwin Klein]

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

After some more digging, it turns out that this is not quite the case.

The rule set I’d need is “typ_desc_typ_struct.inducts”, which datatype_compat doesn’t generate. It does generate the four constituent rules that I can put in a set myself, but the order of premises in these rules is different to the old datatype package, which means my goal order will still be different.

I can state and derive the old rule set easily enough from these. I had hoped to avoid that, but it’s not so horrible that it can’t be done (at least if you close your eyes and don’t look at it ;-)).

What I won’t get from that is the case names and induct rule declaration so that

“proof (induct t and st and ts and x)”

works with the right case names and without having to spell out the rule each time. There shouldn’t be a conflict with existing induct rules, because none of these get picked either, I just get “Unable to figure out induct rule”.

Is there a good way to extract these declarations anywhere from the old or new datatype package? Would be nice not to have to write them out by hand.

(Independent of all this, it would be nice if the primrec package did that declaration now automatically in any case)


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

Taking ?fa = ?fb = %_. 0 seems to be what throws off the proof. I think I’ll just define size as in the old one to get the proofs working and then there should be a separate cleanup pass to refactor them into something nicer.


> Sorry about the trouble.

The trouble is probably more in the current proof scripts than in the datatype package update.

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.