[isabelle-dev] docs for new datatype package

[Gerwin Klein]

> On 21 Apr 2015, at 6:13 pm, Jasmin Blanchette <jasmin.blanchette at inria.fr> wrote:
>
>>
>>> The rule set I’d need is “typ_desc_typ_struct.inducts”, which datatype_compat doesn’t generate.
>
>> The rule you’re looking for is called “compat_a_b_a_list_b_list.induct” (no s).
>
> Actually, it’s the other way around. With the old package, the “inducts” rule is just a collection of four rules, hence the s. These four rules have now separate names. They are assembled together by the “induct … and …” method. Now it’s a bit more tedious, because they have separate names, as you observed. See e.g. this line in “FOL-Fitting” (AFP), which used to use “inducts” (implicitly):
>
>  apply (induct t and ts rule: closedt.induct closedts.induct)
>
> Strangely enough, hardly anybody uses the old “induct” rule, which combines everything together — but that’s the one I referred to in my previous email.

My guess is that it’s not used, because you need to atomize the goal for it to be applicable to anything larger. You can’t have different meta-implications for each of the “P” if you have a object-level conjunction.


> In short, everything should be there, but under different names. “isabelle doc datatype” also documents this.

Yes, these are all fine, I’m using them. Having a collection is very useful if you have type more than 2 rules for every induction, but it’s easy enough to add manually.

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.

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.