【发布时间】：2021-02-13 06:50:11
【问题描述】：
我试图了解 Isar 中 shows 和 obtains 命令之间的区别（截至 Isabelle 2020）。 isar-ref.pdf (pp 137.) 中的文档似乎有一些拼写错误，让我感到困惑。
... 此外，有两种结论：显示状态数 同时命题（本质上是一个大连词），而 获得索赔几个同时同时的上下文 （本质上是消除参数的大分离和 假设，参见§6.6)。
shows 似乎直截了当。
从我目前的有限经验来看，obtains 似乎是要证明一个以存在量词开头的结论，如in this question 所示（其中结论是存在的，然后目标是obtains )。
这真的是 shows 和 obtains 之间的区别吗（普遍与存在）？
如果不是，obtains 的正确预期用途是什么？
【问题讨论】：
-
obtains是obtain的版本，可以在引理之后使用，例如shows/show或assumes/assume。马卡里乌斯不是偶然选择这些名字的。 prog-prove中obtain的解释你看懂了吗？ -
@MathiasFleury 感谢您的提示。
obtain中的obtain示例（以及其他）是我阅读的第一件事。我无法理解，因为它们有点神奇。这些示例本身有效，但我经常无法将其用于其他数据。除了工作示例之外，通常没有进一步的分析。我想示例集不足以涵盖实践中的所有组合。因此，有关其语法的问题，例如obtains是否翻译成存在量化等，以便理解普通数学意义上的语义。