[isabelle-dev] AFP: Session AVL-Trees broken

[Makarius]

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, 
>> can
>> 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 
Drule.instantiate_normalize.

Disclaimer: this is just a hint based on brief inspection of this incident 
(which should be mostly trivial nonetheless).


 	Makarius