[isabelle] Auto sledgehammer fails to find proofs sledgehammer finds.



[[ Originally posted to the Isabelle 2013-1 RC1 issue tracker. Re-posting
to Isabelle-users by request of Makarius. ]]

Hi all,

In Isabelle/jEdit, when "Auto Sledgehammer" is enabled, typing:

    lemma "2 + 2 = (4::nat)"

quickly gives a proof in the output window:

    Auto Sledgehammer ("e") found a proof: by (metis numeral_Bit0).

However, the (marginally) more complex lemma:

    lemma "length xs > 0 ⟹ hd (rev xs) = last  xs"

fails to provide any automatic sledgehammer results, despite the fact
that it can be solved quickly by explicitly writing:

    sledgehammer [provers=e,timeout=1.0]

which gives the results:

    "e": Try this: by (metis hd_rev length_0_conv less_numeral_extra(3)) (11 ms).

Is this expected behaviour (for example, because the latter does time
slicing which enables it to find proofs that the former does not), or
could there be a deeper problem here?

(Isabelle 2013-RC1, running under 64-bit Ubuntu 13.04, with Unity.)

Thanks so much,
David


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




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