> On 21 Apr 2015, at 6:13 pm, Jasmin Blanchette <jasmin.blanche...@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.
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
