theorem-proving - 在Isabelle中一起调用Nitpick和Sledgehammer

当我在Isabelle中声明引理时，我经常键入nitpick，如果这没有给我反例。
然后，我键入sledgehammer尝试自动查找证明。

我想知道：是否可以调用Nitpick和Sledgehammer使其同时运行？
由于《大锤》已经将我的引理发送给了一系列自动证明，这些证明中的一个难道不是像Nitpick这样的反例发现者吗？

最佳答案

您可以尝试在Isabelle中使用try命令。它并行运行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

将返回大锤的结果。