问题标签 [isar]

我有兴趣使用 Isar 作为一种元语言来编写关于J的正式证明，这是一种可执行的数学符号和编程语言，我希望能够使用 J 作为内部语法。

J 由大量原语组成，并为每个 ASCII 字符分配（多个！）含义，包括单引号和双引号。

我在哪里可以找到实现全新内部语法的文档或示例代码？或者这甚至可能吗？（我一直在src/目录中四处寻找，但它有点压倒性，我不完全确定我在寻找什么。）

我试图证明一个定理，但陷入了一个子目标（我更愿意跳过并稍后证明）。我怎样才能跳过这个并证明其他人？

首先，我尝试过oops，sorry但他们都中止了整个证明（而不是唯一的子目标）。我还尝试将子目标放入虚拟引理（假设用 证明sorry）然后使用它（apply (rule [my dummy lemma])），但它将虚拟引理应用于所有其他子目标（不仅是第一个子目标）。

大多数证明助手都是具有依赖类型的函数式编程语言。他们可以证明程序/算法。相反，我对最适合数学且仅适用于数学的证明助手感兴趣（例如微积分）。你能推荐一个吗？我听说过 Mizar，但我不喜欢源代码是封闭的，但如果它最适合数学，我会使用它。Agda 和 Idris 等新语言在多大程度上适合数学证明？

我试图在 Isabelle 中为一些（概念上）简单的算术语句证明一个很大的案例区别。在证明过程中，我偶然发现了以下子目标。

在数学上，它相当简单：这两个陈述¬ 2 * k + 1 ≤ 2 * l和k ≤ l暗示k=l，因此最后一个公式成立。

但是，我无法在伊莎贝尔身上证明这一点。我认为应该可以使用我在 Isar 中的上述推理来构建一个证明，但我仍然是一个初学者，我很难找到正确的关键字。我收到各种令人沮丧的错误。这是我的尝试之一：

我收到一个奇怪的“类型统一失败”错误。

有人有什么想法吗？也许如何才能整体证明这个陈述更简单？

这是一个证明：

在整个证明过程中该depth值为 0，但之后

它变为

这里是什么depth意思？进行证明时是否重要？

我仍在努力了解平等关系以及如何在 Isabelle 中定义平等关系。幸运的是，在 isar 参考手册 2.3.1 p38f 中有一个关于此的章节。

我试图重建给定的例子。为了避免与既定语法有任何重叠，我重命名了所有内容。我还添加了一些引号，因为示例中似乎缺少它们。

下一步是我不太明白的判断，但是嘿会出什么问题：

即使重命名 Trueprop 也不会产生另一个结果。

我不能在这里以某种方式使用 bool 而不是定义我自己的对象命题吗？还是我需要在其他地方介绍 u_play？

但让我们更进一步。下一步是相等关系，也被复制和重命名。

这给出了一个Type unification failed: Clash of types "u_play" and "bool"错误。当我将 u_play 替换为 bool 时，一切都很好，我什至可以EQ在一些琐碎的东西中使用lemma t : "x EQ x"，但是替换规则似乎不起作用，这让我想到了两个 B 在那里的问题。我在 HOL.thy 中看到了相同的构造，但使用了 P，而在 isar rm 的下方，它们被省略了。只是说明impD [dest]: (A --> B) ==> A ==> B

需要做什么才能使替换起作用？

我仍在尝试对 Isabelle 中的语义平等进行推理。我想比较两个公式，看看它们是否相等。之前有人告诉我，我需要商类型。所以我试图给自己定义一个quotiernttype，但显然我的定义并不完整，因为我似乎无法在我的定义之后编写任何代码。到目前为止，我的代码是：

我有一些基本公式和它的复杂版本，我想对复杂类型进行推理，因此我用相等关系的三个公理和另外三个简单的公理定义了 equals。

编辑：显然我是一个忘记添加引号的白痴-.-仍然不知道如何从这里继续思考。

我有

证明后我得到

我从大锤那里接到了梅蒂斯的电话

结构性偶数.intros(1) =结构性偶数0

我明白了

然后。但是，在接下来我得到

因此，尽管系统说“成功尝试通过导出规则解决目标”，但在 1 处仍有一个微不足道的剩余子目标。

为什么会发生这种情况，我该如何解决？

当我有像"∀x. P x"伊莎贝尔这样的目标时，我知道我可以写作

但是，当目标是 时"∀x>0. P x"，我不能那样做。proof为了简化我的目标，我可以使用类似的规则/方法吗？对于您有表单目标的情况，我也会感兴趣"∃x>0. P x"。

proof (rule something)我正在寻找使用该样式的 Isar 证明。