Isabelle 中的“note”命令有什么作用，什么时候需要？答案

【问题标题】：What does the "note" command do in Isabelle and when is it necessary?Isabelle 中的“note”命令有什么作用，什么时候需要？
【发布时间】：2021-02-12 19:37:24
【问题描述】：

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

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

什么时候需要note什么的？不是自动使用目前已知的所有事实和/或假设，还是我必须明确note 某些事实才能使用它们？如果是，哪些是noted，哪些不需要？
有哪些注意事项？

在文档 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”（在某种程度上是“注意”）是可选的。这就是为什么它在这里让我如此困惑的部分原因，因为它似乎是必需的，我不确定它的作用。（我可以理解其他内容，例如assume，因为它将一些事实转移到上下文中。）

我在note 命令中看到了this 和that（例如这里的Why are the following trivial self-equalities needed in the Isabelle/Isar proof?）。这让我很困惑。

关于note 对事物的作用（this、that、calculation 等）是否有字典（英文字典）样式解释？ p>

,... 为什么需要note？

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

【问题讨论】：

标签： isabelle isar

【解决方案1】：

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

开始 Isar 的正确方法是前卫证明。或者用于教学的幻灯片。

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

使用note 的常用方法是为尚未命名的事物命名，例如：

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

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

如上所述@ManuelEberl

note [simp] = ...

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

简短的总结：

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

永远不要直接使用calculation。

可能会像question 那样滥用注释，方法是不给事物命名并依赖其副作用。不要这样做。

【讨论】：

我经常用它来声明事物，例如simp 规则：note [simp] = my_equation。或者，当我有一个已经证明的方程式我想在also 链中使用时：have "a = b" by some_method also note ‹b = c› finally have "a = c"
另外，虽然 Mathias 说 Isar 没有隐式使用事实是非常正确的，但特定的证明方法（如 simp、auto）确实隐式使用了事实，例如那些已声明为simp 或intro。
Isar 也使用例如当您执行 also 链时，trans 明确规则。
@ManuelEberl 我的教学印象是人们相信（或期望）在后来的haves 中使用了假设。但是您显然是对的， simp 隐含地做事。
虽然我同意 Isar-ref 可能不是对 Isar 的最佳介绍，但 Don't read it. Forget everything you read there. Really. 对于 SO 的答案听起来非常过分，总的来说，在我看来，这可能不是最好的建议。根据我自己的经验，当我开始从教科书中学习 Isar 时，如果不使用 Isar-ref 来补充我的学习，很可能我会比我更努力。对不起，我很痛苦，但我无法抗拒:-)。

【解决方案2】：

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

【讨论】：