如何管理所有各种证明方法

是否存在Isabelle用户遵循的"通用"非正式算法,当他们试图证明某些事情未被立即证明auto或sledgehammer？如果auto需要额外的引理,由用户制定成功或者如果使用更好的一些其他证明方法,一种通用的方法.

一个相关的问题是:是否可能在某处找到一个表格,其中包含所有证明方法以及应用它们的上下文？当我阅读 编程和校对教程时,各种方法的描述(分别是某些方法的变体,例如许多变体auto)都散布在文本中,这不断让我回到文本和Isabelle代码之间(这也会导致忘记究竟用于什么),这导致工作效率非常低.

不,没有"通用"的非正式方式.你可以用try0它尝试所有标准的证明方法(如auto,blast,fastforce,...)和/或sledgehammer哪个更先进.

之后,有趣的部分开始了.

这个定理可以用更简单的辅助词来表示吗？您可以使用命令"sorry"来假设引理为真.

我怎么在一张纸上证明这一点？然后尝试在Isabelle中做这个证明.

寻求帮助:)很多人在堆栈溢出,freenode上的#isabelle和Isabelle邮件列表等着你的问题.

对于你的第二个问题:不,没有这样的概述.也许有人应该写一个,但如前所述,你可以简单地使用try0.