Re: [isabelle] sledgehammer issue
> 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:
((![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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and