[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. ]]
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:
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,
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