问题标签 [isar]

Isar 参考手册第 6.1.3 节

指出 oops 的类型是

证明 → local_theory | 理论

这是什么类型proof？这是证明（证明）、证明（状态）和证明（链）的总称吗？

通常，当以“证明”模式证明一个陈述时，我发现自己需要一些尚未陈述或证明的中间陈述。为了说明它们，我通常使用subgoal命令，然后proof-更改为“状态”模式。然而，在这个过程中，所有的局部假设都被删除了。一个典型的例子可能看起来像这样

我知道我可以assume明确地陈述假设。然而，当涉及多个假设时，这很快就会变得相当乏味。有没有更简单的方法来简单地引用所有假设？或者，是否有一种直接在“证明”模式下实现带有简短证明的语句的好方法？

在做一些基本代数时，我经常会遇到以下类型的子目标（有时是有限和，有时是有限乘积）。

这对我来说似乎很明显，但既auto不能也auto cong: sum.cong split: if_splits不能处理这个问题。更重要的是，sledgehammer当调用这个引理时也会投降。如何有效地处理一般包含的有限和和乘积if-then-else，特别是如何处理这种情况？

我正在尝试实现 Isabelle/JEdit 的命令行版本，所以我可以

1. 在另一个 docker/machine 中运行 Isabelle 服务器
2. 允许集成更多编辑器，如 Vim 或 Emacs
3. 允许自动化代理检查和编写证明。

从这个问题来看，似乎没有办法将 JEdit 与 Isabelle 进程分开。我还阅读了 Isabelle系统手册，该手册在协议方面没有太多信息。例如

另一个提供这种功能的库是scala-isabelle，但我不清楚它是否可以执行这种交互。

我想在Latex中显示Isabelle/Isar和Coq语言，例如

当我以 *.pdf 格式（用于学术论文）进行编码时。我该怎么做呢？（我希望这可以推广到Python和Coq等其他语言，这样对每个人都有用）。我也希望这也能在背面工作。

我正在尝试学习 Isar 语言（截至 Isabelle 2020），并理解note命令。它似乎是该语言的一个基本元素，因为许多“派生元素”都是基于它定义的。

我不确定它在英语等价物方面的作用：

1. 什么时候有必要note做点什么？不是自动使用了此时已知的所有事实和/或假设，还是我必须先明确note某些事实才能使用它们？如果是这样，哪些需要，哪些不需要note？

2. 有哪些注意事项？

在文档 Isar-ref.PDF 的附录 A1.2 (pp319) 的“Primitives”下，它说：

注意 a = b 重新考虑并声明事实

所以似乎需要注意一个平等。然后，在同一页面的 A 1.3 中，它说：

这里note似乎不适用于平等。此外，似乎有一个无限循环。

（then扩展到from并返回到then）。

然后在同一页面上，有：

在英语中，单词“also”（在某种程度上是“note that”）是可选的。这就是为什么它在这里让我如此困惑的部分原因，因为它似乎是必需的，我不确定它的作用。（我可以理解其他事情，例如assume它将一些事实转移到上下文中。）

我已经在命令中看到this并that使用过note（例如，在这里为什么 Isabelle/Isar 证明中需要以下琐碎的自等式？）。这让我很困惑。

是否有字典（英语字典）样式解释在某处note对事物（this，that等calculation）的作用？

,... 为什么note需要？

（上面的附录是我能找到的最接近规范的东西。）

我试图了解 Isar 中的shows和obtains命令之间的区别（截至 Isabelle 2020）。（pp 137.）中的文档isar-ref.pdf似乎有一些错字，让我感到困惑。

...此外，有两种结论：表明陈述了几个同时命题（本质上是一个大合取），同时获得了几个同时同时的上下文（本质上是消除的参数和假设的大析取，参见§6.6）。

shows似乎直截了当。

从我到目前为止的有限经验来看，这似乎obtains是关于证明一个以存在量词开头的结论，如this question所示（其中结论是存在的，然后目标是 a obtains）。

这真的是shows和obtains（普遍与存在）之间的区别吗？

如果不是，正确的预期用途是obtains什么？

我有伊莎贝尔的定义：

带输出

我可以从这个定义中获得价值：

输出：

因此，这是可识别且正确的表达/术语。但是我尝试使用这个定义来声明引理：

不幸的是，这个引理不被接受（没有生成目标/子目标），而是给出了错误消息：

我的引理有什么问题？我只是使用了不正确的相等操作（也许有一些微妙之处 - nat 实例与 nat 集的混淆）还是更普遍的问题？也许我不允许为（可能是终止）定义陈述定理/引理，并且我只能为已经完成终止证明的函数陈述引理（在函数声明时）？

是否可以更正（如果可以为定义说明引理）我的引理，使其被接受并生成证明目标？

假设我正在证明一个假设“ n ≥ m”（都是自然数）的定理，并且我对n. 在基本情况下，假设是“ n = 0”。有了这两个，我们可以得出结论，在基本情况下，“ m = 0”。

但是，我在使用语句“ n = 0”时遇到了麻烦：

我试过using "n = 0"了，但它似乎是一个“ Undefined fact”。我也尝试将其添加为假设，但无济于事。尽管如此，很明显，在分析基本情况时，这是一个隐含的假设。

那么，如何在我的证明中直接使用基本情况的假设呢？