在伊莎贝尔一起召集Nitpick和Sledgehammer

Question

当我在伊莎贝尔中说出一个引理时,我经常打字nitpick,如果这不能给我一个反例.然后我键入sledgehammer以尝试自动查找证明.

我想知道:是否可以调用Nitpick和Sledgehammer以便它们同时运行？由于Sledgehammer已经将我的引理发送给了许多自动证明器,这些证明器中的其中一个实际上不是像Nitpick那样的反例调查器吗？

Answer 1

您可以尝试try在Isabelle中使用该命令; 它运行sledgehammer,nitpick,quickcheck和一些其他求解器(如auto,simp,force等等)并联,给出这样的结束的第一个的结果.

例如,运行以下命令:

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

将返回一个反例nitpick,表明该定理一般不正确.添加类型约束:

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

现在将返回一条消息,告诉您simp能够解决目标.

最后,改变类型约束更具挑战性的32 word类型(可从Word于HOL-Word):

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

将从大锤返回结果.