Re: [isabelle] Isabelle2015-RC0 available for testing



I've attached a small demo theory which exhibits some strange behaviour
when using Sledgehammer on a goal containing a conjunction. I've marked
the problematic statement with (* HERE *).

Steps to reproduce:

1) Go to the blank line between 'defer' and 'sorry'.
2) In the Sledgehammer panel, select provers 'e spass z3 remote_vampire
cvc4' and click 'Apply'.
3) All provers will suggest 'apply simp'.
4) 'apply simp' doesn't solve the first subgoal.

What's even more confusing is that if I invoke sledgehammer via the
command, I get different results for cvc4:

"cvc4": One-line proof reconstruction failed: apply (smt term.collapse(1)).

I've suspected that somehow the 'defer' is at fault here, but even if it
is removed, there's more strange behaviour. In that case, the panel
correctly suggests 'apply auto[1]' (which in fact solves the subgoal),
but the sledgehammer command suggests:

"cvc4": One-line proof reconstruction failed: apply (smt term.collapse(1)).
"remote_vampire": Try this: using term.collapse(1) apply presburger (0.0
ms).

The latter invocation does not solve the subgoal. While I know that
sometimes Sledgehammer suggests an invocation of 'metis' which takes too
long (and might not be able to solve it?), I've never encountered this
with the new (and very helpful) suggestions of 'simp' or 'auto'.

Cheers
Lars

Attachment: Scratch.thy
Description: application/extension-thy



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