我常常遇到sledgehammer找到证据的问题，但是当我插入它时，它不会终止。我猜sledgehammer是Isabelle最重要的部分之一，但如果证明失败则会变得很烦人。
在Sledgehammer tutorial中，有一个小章节“为什么Metis无法重建证明？”。
它列出：
isar_proofs选项获得逐步的Isar证明，其中每个步骤都由metis进行校正。由于步骤相当小，metis更有可能重播它们。smt证明方法而不是metis。它通常更强大，但您需要使用Z3重放证明，信任SMT求解器或使用证书。blast或auto证明方法，通过unfolding，using，intro:，elim:，dest:或simp:传递必要的事实。问题是第一个选项使证明更加冗长，并且还涉及手动干预。第二种选择很少有效。
那么第三种选择呢？我可以使用任何易于遵循的启发式方法吗？
unfolding和using有什么区别？还有关于如何使用intro:失败的elim:，dest:和metis的最佳实践吗？
部分例子
proof-
have "(det (?lm)) = (det (transpose ?lm))" by (smt det_transpose)
then have "(det (?lm)) = [...][not shown]"
unfolding det_transpose transpose_mat_factor_col by auto
then show ?thesis [...][not shown]
qed
我想摆脱证明的第一行，因为这条线似乎微不足道。如果我删除第一行，sledgehammer仍会找到证据，但是这个证明失败了（不会终止）。
关于你的陈述大锤是伊莎贝尔最重要的部分之一：你永远不需要大锤就能证明成功。但当然大锤非常方便，可以节省大量繁琐的推理。因此，对于那些没有花费多年时间使用它的人来说，Isabelle更有用，这绝对是一个非常重要的部分（即使是那些大锤每天都能提高效率）。
来到你的问题
尝试使用
blast或auto证明方法，通过unfolding，using，intro:，elim:，dest:或simp:传递必要的事实。 [...] 那么[this]选项呢？我可以使用任何易于遵循的启发式方法吗？
确实有：
unfolding：这个（递归地）展开方程式，即它与apply (simp only: ...)非常相似。启发式是，当你没有得到simp: ...的预期结果时，请尝试unfolding ...（可能是其他方程干扰的情况）。
using：这用于向当前子目标添加其他假设。启发式是，只要事实不适合下面的模式之一，请尝试使用using。
intro:：这用于引入规则，即，只要满足某些假设，就可以引入某些连词（或更一般地说是常数）的形式。
示例：A ==> B ==> A & B（其中引入的常量为(&)）。
elim:：这用于消除规则，即，从存在某个连接词（或更一般地说是常数）的形式，某些事实可以作为附加假设得出结论。
示例：A & B ==> (A ==> B ==> P) ==> P（其中消除了常数(&)，有利于明确地将A和B作为假设）。请注意结论的一般形式（与主要前提A & B无关），这对于不松散的可证明性很重要（另见dest:）。
dest:：这用于销毁规则，即从存在某种常数的形式可以直接得出一些事实。
示例：A & B ==> B（请注意，A保存的信息在结论中丢失，与elim:示例不同。）
simp:：这用于简化规则，即（条件）方程，它们总是从左到右应用（因此有时将[symmetric]添加到事实中是有用的，以便从右到左应用它，但要小心不确定，因为很容易以这种方式引入循环推导）。
说完这些之后，通常只有经验可以让您决定在证明中最好地使用给定事实的方式。当我得到sledgehammer的证据时，我通常会做的，这在Isar中太慢了，就是检查所发现的证据所使用的事实。然后按上面的方式对它们进行分类，适当地调用auto，如果没有完全解决目标，再次应用sledgehammer（希望这次提供“更容易”的证明）。
你问了一些问题，但我会把你的头衔和第二段作为你主要投诉的实质，我最后会给出一个冗长的答案，可以用以下的方式总结，
minimize和preplay_timeout选项可以通过自动播放校样来节省您一些时间和挫折，这会为您提供时间信息，有时会显示找到的证据会失败。从你的第二段开始，你说：
我常常遇到大锤找到证据的问题。但后来我尝试了，但证据没有终止。我想Sledgehammer是Isabelle最重要的部分之一，......
大锤很重要，但我认为它是三管齐下的武器库的一部分，其中三个部分将是：
auto，simp，rule等。其中很大一部分是创建自己的simp重写规则，并学习使用rule定理和无数其他自动校对方法。auto来简化事情，以便Sledgehammer成功，但您可能不会使用auto，因为它会将公式扩展到Sledgehammer无法成功的地方。......但是如果证据失败就会变得很烦人。
所以在这里，你的期望和我对Sledgehammer的期望分歧。这些天，如果我生气，我会生气，我将不得不工作超过30秒来证明一个定理。如果我对一个特定的Sledgehammer证明失败感到非常失望，那是因为我一直试图证明一个定理几个小时或几天没有成功。
自动化有时可以减轻挫败感。点击Sledgehammer证明，只是发现它失败了，这将是令人沮丧的。这是我目前使用Sledgehammer的方式，除非我开始急需证明：
sledgehammer_params[minimize=smart,preplay_timeout=10,timeout=60,verbose=true,
max_relevant=smart,provers="
remote_vampire metis remote_satallax z3_tptp remote_e
remote_e_tofof spass remote_e_sine e z3 yices
"]
选择minimize=smart和preplay_timeout=10与Sledgehammer在发现它们之后播放证据有关。没有使用Sledgehammer发现的许多证据是使用Sledgehammer的重要部分，证明回放是剔除证据的重要部分。
我自己，我并没有太多关于不会终止的Sledgehammer证据，但这可能是因为我有选择性地开始。
我对Sledgehammer证明的第一个标准就是速度相当快，所以当Sledgehammer报告发现它有超过3秒的证据时，我甚至都没有尝试使用它，除非我不顾一切地想知道是否一个定理可以证明。
对我来说使用Sledgehammer通常是这样的：
try和isar-ref.pdf第9.4.4节第208页的自动证明方法。很多时候，我可以获得低至5毫秒或更短的证明。metis证明总时间超过100毫秒，我愿意工作30分钟或更长时间来尝试获得更快的证据。metis证明，我将使用我所知道的所有尝试并将其降低到100毫秒以下，这很多时候意味着转换为详细的证据。smt或metis证明超过1秒我只考虑好作为临时证明。你说，
那么第三种选择呢？我可以使用任何易于遵循的启发式方法吗？
启发式是：
也就是说，启发式是“使用大锤作为三管齐下的武器库的一部分”。
启发式也是“阅读大量的教程和文档，以便你有很多其他东西可以使用Sledgehammer”。大锤是强大的，但它不是无限强大的，对于一些定理，你可以使用你自己的simp规则用apply(simp)或apply(auto)在0ms证明大锤永远不会证明什么。
对于我自己来说，我达到了大约150到200个定理，因此“适当的”对我来说具有更多的意义。基本上，您尝试按照需要设置的方式设置Sledgehammer。
需要建立大锤的方式有时意味着首先运行auto或simp，但有时不会，因为多次运行auto或simp将使大锤失败。
但有时，你甚至不需要大锤的metis证明，除非作为初步证明，直到你能找到更好的证据，对我来说，这通常意味着使用自动证明方法的更快证明。
我对Sledgehammer没有权威，但似乎Sledgehammer擅长匹配旧定理的假设和结论，假设和结论被用于一个新的定理。它不擅长的是通过使用simp和auto来证明我已经大大扩展的公式。
我继续使用以Sledgehammer为中心的冗长启发式：
simp重写规则，以便与simp，auto，fastforce等自动校对方法一起使用，如tutorial.pdf第9章所述。intro和rule一起使用。simp和auto将神奇地证明事物，你将摆脱大锤为你找到的一些metis证明。有时候，你会使用Sledgehammer找到更快的metis证明。使用此命令优化时序：
ML_command "Toplevel.timing := true"
还有另一篇SO帖子提供了更多细节。
我可以回答你的问题“unfolding和using之间有什么区别？”。粗略地说，它就是这样的。
假设引理foo的形式为x = a+b+c。如果你写
unfolding foo
在你的证明中，然后所有出现的x将被替换为a+b+c。另一方面，如果你写
using foo
然后x=a+b+c将被添加到您的假设列表中。