Summon Nitpike and Sledgehammers Together to Isabel

Question

When I state a lemma in Isabel, I often type nitpick , and if that does not give me a counterexample. Then I type sledgehammer to try to find evidence automatically.

Interesting: is it possible to call Nitpick and Sledgehammer so that they run simultaneously? Since Sledgehammer is already sending my lemma to a bunch of automatic providers, could one of these proxists be a counterexample such as Nitpick?

Answer 1

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

For example, do the following:

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

will return a counter example from nitpick , which indicates that the theorem is generally incorrect. Adding a type constraint:

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

will now return a message that simp can solve the problem.

Finally, changing the type restriction to a more complex 32 word type (available from Word in HOL-Word ):

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

will return the result from the sledgehammer.