Invoking Nitpick and Sledgehammer together in Isabelle

Question

When I state a lemma in Isabelle, I often type nitpick, and if that doesn't give me a counterexample. I then type sledgehammer to try to find a proof automatically.

I wonder: is it possible to invoke Nitpick and Sledgehammer so that they run concurrently? Since Sledgehammer is already sending off my lemma to a bunch of automatic provers, couldn't one of those provers actually be a counterexample-finder such as Nitpick?

Answer 1

You can try using the try command in Isabelle; it runs sledgehammer, nitpick, quickcheck and a number of other solvers (such as auto, simp, force, etc) in parallel, giving you the results of the first one that finishes.

For example, running the following:

lemma "(a * (b + 1)) = (a * b + a)"
  try

will return a counter-example from nitpick, indicating that the theorem is not true in general. Adding a type constraint:

lemma "((a :: nat) * (b + 1)) = (a * b + a)"
  try

will now return a message telling you that simp is able to solve the goal.

Finally, changing the type constraint to the more challenging 32 word type (available from Word in HOL-Word):

lemma "((a :: 32 word) * (b + 1)) = (a * b + a)"
  try

will return a result from sledgehammer.