1

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

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

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

  2. 有哪些注意事项？

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

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

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

from a ≡ note a then
...
from this ≡ then

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

from a = note a then = note a from this = note a note this then ...

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

然后在同一页面上，有：

also   ~   note calculation = this

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

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

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

,... 为什么note需要？

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

4

2 回答 2

2

没有人以问题的方式使用它。看到那个证明很痛苦。Isar ref 告诉您事物是如何在内部定义的，但它是对 Isar 的糟糕介绍。不要读它。忘记你在那里读到的一切。真的。

启动 Isar 的正确方法是 prog-prove。或用于教学的幻灯片。

没有任何事实被隐含使用。伊莎贝尔只使用您告诉它使用的事实。这就是为什么您需要using或将定理作为战术参数传递的原因。

通常的使用方法note是给还没有名字的东西命名，比如：

   case Suc
   note meaningfull_name_one = this(1) and meaningfull_name_two = this(2)

或变体。这允许您按名称引用定理，meaningfull_name_one而不是写下完整的表达式。这不是必需的，但更容易（也是维护方面）。当你有 10 个假设时，你不想使用prems(1)orSuc(8)或其他什么。

如上所述@ManuelEberl

note [simp] = ...

将定理局部声明为 simp 很有用。

简短的摘要：

   this           ::= last fact
   note H = ...   ::= name facts
   that           ::= name of the fact generate by obtain/obtain

永远不要calculation直接使用。

通过不给事物命名并依赖其副作用，可能会像所讨论的那样滥用注释。不要这样做。

于 2021-02-12T08:55:28.493 回答
1

原因之一是您可以使用 [OF _] 等低级运算创建新定理。为了简化重用这样一个定理，你可以给它一个名字。

于 2021-02-12T11:37:24.743 回答