我正在尝试[] |- p /\ q <=> q /\ p :thm使用带有 HOL 推理规则的 SML 来证明该定理。这是 SML 代码：

上述代码的结果产生：

我究竟做错了什么？

我试图通过打包用于证明目标的策略来创建一个名为“absorptionRule”的定理!(p:bool) (q:bool). (p==>q) ==> p ==> p /\ q。但是，我在 ACCEPT_TAC 上遇到了异常。当我一个接一个地执行每个策略时，一切正常。

如果我将括号中的步骤THENL按顺序输入到 HOL 解释器中，则括号中的步骤可以正常工作。但是当我将它们与TAC_PROOFusing结合使用时THENL，出现错误。

THEN我想我理解和THENL （所有子目标与单个子目标）之间的区别。但我找不到区分这两个初始子目标的语法。DISJ1_TAC并且RES_TAC应该只适用于 subgoal1。虽然DISJ2_TAC并且RES_TAC应该只适用于 subgoal2。

我怎样才能解决这个问题？

我正在尝试将定理添加到现有理论中。我要添加的定理是：

我的第一步是证明这个定理；但是，当我尝试设定目标时，我收到了几条错误消息：

我在 Isabelle/HOL 中有一些定义和定理，需要在 HOL 中使用这些相同的定义和定理。手动翻译代码当然是可能的，但很麻烦。有没有（半）自动执行这种翻译的程序？

如果由于某种原因这是不可能的，请解释原因，因为这对我来说是一个重要的学习。

我在 HOL4 中陈述了以下目标：

导致证明状态

我试图找到使用这些假设的适当策略。我想出了ASM_MESON_TAC：

它证明了目标：

这是在这种情况下的标准策略吗？或者，有没有更简单的？

我需要在一篇论文上做一个演示，该论文在某些时候使用了 Isabelle/Isar 和 Isabelle/HOL。

我尝试在网上搜索有关 Isabelle/HOL 和 Isabelle/Isar 的信息，以便能够在一两张幻灯片中说明这些关系。以下是我目前理解的关系：

• Isabelle - 为演绎系统提供通用基础架构
  • 基于标准 ML 编程语言
  • 提供了一个 IDE，允许您编写以后可以证明的理论。
• Isabelle/Pure - 根据此链接 的高阶逻辑的最小版本：
  • 它是可以输入到 isabelle IDE 中的实际语言吗？
  • 还是技术规范？

• Isabelle/HOL（高阶逻辑）：

  • 它是图书馆还是语言？
  • 它与 Isabelle/Pure 有什么关系？
  • 它本质上是程序性的吗？
    • 战术只存在于 Isabelle/HOL 中吗？
    • 是 LCF - 逻辑可交换函数吗？

• 伊莎贝尔/伊萨尔：

  • 基于 Isabelle/Pure 的结构化证明语言
  • 声明式
  • 它是此处所述的 Isabelle/HOL 的扩展吗？
  • 语言环境是否只存在于 Isabelle/Isar？

Isabelle/IDE 默认支持什么？

只是觉得我从不同的来源获得了相互矛盾的信息，并想解决这个问题。

提前致谢

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

我知道也许我应该以完全不同的方式完成我想做的事情：我之前没有使用 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没有帮助我。

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

我的代码

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

我想在 Isabelle 中创建一个给定公式的函数 F

如果公式是重言式的，则返回 True，否则返回 False。

例如：

谁能帮我？我发现很难理解 Isabelle 的文档，而且我找不到这样的功能（我认为它应该已经存在）。

我花了一些时间使用 HOL 中的定理库构建“前向证明”。我现在希望转向应用策略来制作“向后证明”。

我想知道是否有一种方法可以在应用策略后查看该策略应用的定理列表，即详细重建前向证明。这主要是为了帮助我理解战术是如何运作的。

例如：

谢谢！