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