[isabelle-dev] docs for new datatype package

[Jasmin Blanchette]

Hi Gerwin,

From your first email:

> I’m still seeing a different order of premises in the rules themselves, though. Maybe that only occurs for more than 2 constructors, or it has to do with the fact that my case is not just mutual through one set of datatypes, but also involves a third datatype and lists, which all generate separate cases of the induction.
> 
> Specifically, the old rule for P1 was
> 
> ⟦⋀typ_struct list. P2 typ_struct ⟹ P1 (TypDesc typ_struct list); ⋀nat1 nat2 a. P2 (TypScalar nat1 nat2 a);
>     ⋀list. P3 list ⟹ P2 (TypAggregate list); P3 []; ⋀dt_pair list. ⟦P4 dt_pair; P3 list⟧ ⟹ P3 (dt_pair # list);
>     ⋀typ_desc list. P1 typ_desc ⟹ P4 (DTPair typ_desc list)⟧
>    ⟹ P1 typ_desc
> 
> The new rule has P3 and P4 swapped:
> 
> ⟦⋀x1 x2. ?P2.0 x1 ⟹ ?P1.0 (TypDesc x1 x2); ⋀x1 x2 x3. ?P2.0 (TypScalar x1 x2 x3); ⋀x. ?P4.0 x ⟹ ?P2.0 (TypAggregate x);
>     ⋀x1 x2. ?P1.0 x1 ⟹ ?P3.0 (DTPair x1 x2); ?P4.0 []; ⋀x1 x2. ⟦?P3.0 x1; ?P4.0 x2⟧ ⟹ ?P4.0 (x1 # x2)⟧
>    ⟹ ?P1.0 ?typ_desc
> 
> The swapping is consistent in the sense that the order in the rule itself doesn’t really change, but the order in which the rule expects the properties in the goal is what leads to the swapping. The induction package seems to figure out the order by itself and matches them correctly if stated as simultaneous goals (which doesn’t work with the object-level conjunct rule), but through that it will generate a different order of subgoals.

OK, that’s good to know. I’ll look into this, to see if it can be fixed easily or otherwise at least documented. At any rate, it’s probably better not to hold your breath and e.g. to derive the old rule from the new one (which should be easy enough, e.g. using Alex's “induct_schema” tactic or even manually) and use it.

From your second email:

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

From your third email:

> I think my induction troubles are solved with that. Still would be nice to get default attributes, though.

The trouble is that if we set the attribute, then it effectively unregisters the old-fashioned induction rule. The registration is on a per-type basis. You can’t have both “a.induct” and “compat_a.induct” registered as induction rules for type “a”. I like to see compatibility as an add-on to the standard features, not as a replacement.

Jasmin