[isabelle-dev] AFP: Session AVL-Trees broken
makarius at sketis.net
Mon Nov 19 16:05:15 CET 2012
On Fri, 9 Nov 2012, Ondřej Kunčar wrote:
> On 11/08/2012 11:59 AM, Tobias Nipkow wrote:
>> This is exactly why I am against SMT certificates in AFP entries. Ondrej,
>> you possibly remove them?
> All SMT calls are now removed (changeset 3685878ce7b7).
> But AVL-Trees were already broken in Isabelle's changeset 791157a4179a
> (ensured that rewr_conv rule t = "t == u" literally not just modulo beta-eta)
> before Jasmin's changeset 34b0464d7eef. It seems that the changeset fixing
> rewr_conv interacts with smt.
The latter changeset is 791157a4179a by Tobias, and luckily it does not
claim to "fix" things in the log message. As I've pointed out on the
corresponding isabelle-users thread, "fixed" and "broken" are basically
the same thing -- it is hard to make moves that don't just increase
entropy of the sources.
Anyway, inspecting 791157a4179a further, I see a difference in the result
(without trying out anything): Drule.instantiate_normalize is replaced by
the non-normalizing Thm.instantiate plus full Thm.beta_conversion of the
result. Is that really the same normalizing as before?
I would have omitted the post-hoc checks and normalization that make the
code a bit unclear, and instead used a beta/eta-convertible transitivity
step *before* applying the instantiated (and normalized) rewrite rule, to
fit into its potentially changed lhs. This usually works via COMP or
COMP_INCR together with Drule.transitive_thm, instead of the direct
Thm.transitive. Then you don't even have to know what normalization COMP
really does, as long as it is somehow compatible with the normalization of
Disclaimer: this is just a hint based on brief inspection of this incident
(which should be mostly trivial nonetheless).
More information about the isabelle-dev