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

Question

当我在 Isabelle 中陈述引理时，我经常输入 nitpick ，如果那没有给我一个反例。
然后我输入 sledgehammer尝试自动找到证明。

我想知道:是否可以调用 Nitpick 和 Sledgehammer 以便它们同时运行？
既然 Sledgehammer 已经将我的引理发送给一群自动证明者，那么这些证明者中的一个真的不能成为像 Nitpick 这样的反例发现者吗？

Answer 1

您可以尝试使用 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

将返回大锤的结果。