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

[Sascha Boehme]

Sascha Boehme <boehmes at in.tum.de> wrote:
>
> Hi,
>
> Zitat von Ond?ej Kun?ar <kuncar at in.tum.de>:
>>
>> 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.  
>> There is a goal which is the same goal before and after the change  
>> - the term is really the same; no tricks like the pretty-printer  
>> does beta-reduction.
>> And smt fails only after the change and it doesn't matter if the  
>> pregenerated certificates are used. Somebody who understands smt  
>> should take a look at how much the changeset with rewr_conv is  
>> harmful to smt.
>
> I do have an idea what might go wrong. I'll need to investigate it  
> further before committing a patch.

I found the explanation for the problem. It is indeed related to  
Tobias's change in rewr_conv. The normalization code in the smt method  
rewrites arithmetic constants (e.g. max) by replacing them with lambda  
abstractions (e.g. %a b. if a > b then a else b) and not beta-reducing  
the resulting terms. In a later step a conversion goes through the  
terms and does further rewritings. Before Tobias' change, one  
sub-conversion (a rewr_conv) in that process returns a beta-reduced  
equation (reducing one of the above lambda abstractions), and hence  
the left-hand side does not match anymore the term given to the  
conversion. This causes an exception to be thrown by then_con.  
Nevertheless, a surrounding conversion catches that exception and  
tries something else resulting in a term that "by accident" looked as  
expected. Now, after Tobias' change, the inner rewr_conv returns an  
equation with unmodified left-hand side. The outer conversion that  
previously catched the exception does not kick in and the result is  
something different (and not what one would have expected). Summa  
summarum, there is something severly broken in the normalization code  
of the smt method, and Tobias' change of rewr_conv helped to discover  
this flaw. This indicates that the changed rewr_conv behaves in a way  
that causes fewer surprises for users and as such was an improvement  
to the code.

I'll fix the normalization of the smt method.

Cheers,
Sascha