Re: [isabelle] sledgehammer issue



Dear all,

> On 01.09.2016, at 15:40, Peter Lammich <lammich at in.tum.de> wrote:
> 
> On Do, 2016-09-01 at 13:03 +0100, Lawrence Paulson wrote:
>> A bug in E then. 
> 
> If I understand it correctly, the bug could also be in the translation
> from HOL to E, which is done by sledgehammer.

I've just looked into it. As I suspected, the bug *is* in the translation from Isabelle/HOL to E. For those who are into arcane technicalities, this clause is clearly unsound:

    fof(help_fequal_1_1_fequal_001t__Product____Type__Ounit_T, axiom,
        ((![X, Y]: ((~ pp(aa_Product_unit_bool(fequal_Product_unit(X), Y))) | X = Y)))).

There should be a predicate guarding "X" or "Y", as per the paper "Encoding Monomorphic and Polymorphic Types". I can repair this.

Cheers,

Jasmin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.