我的故事很长，我真正想做的代码也很长。所以首先我将描述我用标题中的公式尝试过的事情，然后我将描述我在实践中是如何遇到这样的事情的，将我的实际代码放在最底部。

我知道也许我应该以完全不同的方式完成我想做的事情：我之前没有使用 Isabelle 的经验（甚至没有使用 Haskell 等函数式编程语言的丰富经验），所以我的代码可能不是惯用的。

我用它做了什么

首先，我知道本节中的所有内容都可以用by presburger（try告诉我的）来证明。不过，这不适用于我的实际问题，而且可能不应该，因为我在那里处理包含整数的自定义数据类型，而不是整数本身。

在尝试将其简化为一个最小的完整可验证示例时，我注意到即使是简单的公式"∃(x::nat). (x ≠ 2)"也很难为 Isabelle 证明。但是，我认为具体的东西x = 1可能会有所帮助。的确，

工作轻松，但是

仍然失败。我想也许我应该把具体部分放在第一位，但是当我尝试

该by auto行在 jEdit 中保持紫色，我认为这表示无限循环。

我是怎么遇到的

我正在尝试使用 Isabelle 为Shogi制作模型，并最终证明解决某些 Shogi 问题的唯一性。当我试图证明一个简单的配置是一个将死时，伊莎贝尔被困在了（为了上下文，我有datatype coord = Coord int int）：

我知道这看起来像一团糟。让我稍微调整一下缩进，希望它更容易被人眼解析。

希望可以看到src = Coord 5 2满足单行src，然后dst = Coord 5 1满足整个事情。

我试图把它作为一个引理并证明它by auto——当然那是行不通的。我终于试过by try了，它告诉我：

好的，这行得通。但我真的很困惑，因为我什至不知道是什么smt。

无论如何，该方法（应用后auto）成功地证明了玩家 2 处于检查状态。我尝试使用相同的方法来证明它是一个将死（至少，这相当于证明在几个配置中玩家 2 仍然处于检查状态），但这也导致了一个错误：

甚至sledgehammer没有帮助我。

由于检查和将死是将棋问题的基本规则，我认为我需要能够自动识别它们，然后才能做任何重要的事情。我愿意写下并手动证明一些引理，但现在我相信我可能在做一些根本错误的事情。

我的代码

如果有什么我需要澄清的，请在评论中提问。

存在一种快捷方式或命令，可以直接进入符号或引理的定义。（就像 Emacs 的 GTAGS 中的“ALT+”）

与 Coq 的相反（只是恕我直言），它非常方便，其中一个必须在 IDE 中执行 Search 命令。

我忘记了应该按哪个组合键在基于 jEdit 的标准 Isabelle IDE 中查找定义。

你能提醒我一下吗？

假设我们有这样的 Modus Ponens 变体

可以用来证明定理吗？（我的意思是 A:=A、B:=A 和 A-->A 我们使用，就好像它之前已被证明一样）

如果不是，为什么？我知道证明这个定理的其他几种方法（“应用假设”或弗雷格命题演算公理的 5 步证明。），但我对证明机制的这种细微差别感兴趣。

我有一个规则，现在我想获得另一个 [admissible] 规则，有什么问题？

1）如何选择我想在 Isabelle/FOL 定理中应用的假设？

有一个证明案例，我不能使用“应用假设”。

我有这种交互式证明状态的情况：

解决这个问题的另一种方法是选择另一个目标。

2) 如何选择我接下来要证明的目标？

另一种方法是用公式“〜A”用问号（？B9）替换变量，所以

3）如何在证明过程中用公式指定元变量？

我读过这篇论文 http://www21.in.tum.de/~berghofe/papers/TYPES2002_slides.pdf。

它包含第 7 页上的 Isabelle 类型系统的微积分。在这个微积分中，“术语有类型”和“证明有术语”。

1）关于这个微积分是否存在更详细的论文？

2）我不明白的唯一两个规则是与常量有关的规则。

2.1) “c_{[\vec{\tau}_n / \vec{\alpha}_n]}”是什么意思？它是一个常数的证明。例如，我们在第 9 页有常量“impI”。这些 tau 和 alpha 如何与“impI 的术语”相关联。

2.2)能否请您澄清一下规则 $\Sigma(c) [\vec{\tau}_n / \vec{\alpha}_n] $。?
乍一看，它可能被翻译为“任何依赖于证明（！）常量的任何一组术语，具有任意数量的类型而不是原子类型”，但我认为它没有任何意义。

3）我也对关于这种微积分的语义和/或它的正确性定理的论文感兴趣。

我感谢任何相关信息。谢谢！

我想在 Isabelle/Isar 中进行规则归纳。我发现

或者

做我想做的事。但是我怎么能用“新风格”伊萨尔写那行呢？如您所见，我只是想告诉 Isabelle 如何P在我的函数的归纳规则中实例化变量f。

我有以下内容：

我认为这取决于基本推理规则，但阅读Isar 参考手册rule部分的文档9.4.3 Structured Methods后发现，它使用了具有各种规则的 Classical Reasoner。并且，将by子句替换为..也解决了目标，因此不需要提及隐含消除和连词介绍。

是否可以在 Isar 中编写严格的形式化，即不使用程序文本中未明确的任何自动化和额外规则？类似于 HOL4 中的前向证明。

我想将这个证明转换为 Isar 作为 ab 练习（让我自己学习 Isar），只使用命题逻辑中的基本自然演绎规则 (ND)（例如notI, notE, impI, impE... 等）。

我可以很容易地在应用脚本中做到这一点：

但我对 Isar 证明的尝试失败了：

我的主要错误是：

这对我来说似乎很神秘，因为规则在之前的应用脚本中工作得很好。

我究竟做错了什么？

请注意，这也会导致错误：

与上述相同的错误：

为什么？

编辑：

我了解到“方法”仍然需要工作rule impI，或者metis etc脚本仍然失败：

编辑2：

我仍然无法完成证明。

我正在阅读第 5 章（Isar）并尝试进行结构归纳证明，"Σ{0..n::nat} = n*(n+1) div 2"但失败了：

它说：

我不知道为什么。大锤也没有解决。我确实尝试过blast，auto等等，但我知道他们会失败，因为大锤之前曾向我提出过​​这些建议，但值得一试吗？

我尝试使用应用样式来查看发生了什么：

同样的错误：

为什么这不起作用？我的 Isabelle 安装有问题吗？

我还尝试了一个没有任何东西的文件的证明，它也失败了，所以它不是我之前的任何定义（我假设很有可能）。

在使用 Isar 时，我发现了一个令人惊讶的行为（对我来说）。我尝试使用假设，有时 Isar 抱怨它无法解决未决目标，例如我最典型的示例是有一个假设但无法假设它：

尽管以下确实有效：

这并不奇怪。

但是下一个令我惊讶的是，鉴于我的第一个示例失败了，它可以工作：

为什么第一个和第二个不一样？

错误信息：