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.