[isabelle-dev] docs for new datatype package

[Gerwin Klein]

> On 21 Apr 2015, at 9:19 pm, Jasmin Blanchette <jasmin.blanchette at inria.fr> wrote:
>>
>> 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.

Just did that and it’s much smoother sailing now.


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

Does it really fully unregister?

Declaring my manual rules as

lemmas typ_desc_typ_struct_inducts [case_names ..., induct type] =
  typ_desc_induct typ_struct_induct typ_list_induct typ_dt_pair_induct

overwrote the standard list induction rule (because typ_list_induct has conclusion “P (x :: ‘a some_thing list)”. However, declaring

declare list.induct [induct type]

afterwards, brings back the list induction rule and seems to keep typ_list_induct around - at least it seems to be different to never having declared typ_list_induct as induct rule at all.

I’m pretty much poking in the dark here, though. I briefly looked at the code of the induct method and then remembered why I never wanted to do that again..

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.