[isabelle-dev] docs for new datatype package

[Gerwin Klein]

> On 21 Apr 2015, at 6:07 pm, Jasmin Blanchette <jasmin.blanchette at inria.fr> wrote:
>
>> (Independent of all this, it would be nice if the primrec package did that declaration now automatically in any case)
>
> Again, I believe it does:
>
>    primrec (nonexhaustive) f and fs and g and gs where
>      "f (A bs) = A (gs bs)"
>    | "fs Nil = Nil"
>    | "g (B as) = B (fs as)"
>    | "gs Nil = Nil"
>    print_theorems
>
> Look for “f_fs_g_gs.induct” (no s).

It proves and exports the rule, but it doesn’t declare it as a standard induct rule that the induction package can pick up. You now basically have to always explicitly mention a rule or set of rules to the induct method when you are doing nested recursion.

I think (could be wrong) that there’s not really a need for that, it could be as automatic as before, it just needs an additional attribute declaration. datatype_compat and primrec could both be places for this (might not even interfere if you do both of them).


>> The trouble is probably more in the current proof scripts than in the datatype package update.
>
> Yes and no. The new package’s modular approach has many advantages, including performance, and I think it stands on its own feet. We’ve had quite some positive feedback about it yet, both about the flexibility it gives (e.g. recursion through non-datatypes), the nice induction rules, and the performance.

I’m actually quite happy with the new datatype package and its flexibility. It’s just this set of theories that seems particularly hairy to update. Just need to get through that one.

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.