问题描述
我试图了解 Isar 中 shows 和 obtains 命令之间的区别（截至 Isabelle 2020）。 isar-ref.pdf（第 137 页）中的文档似乎有一些拼写错误，让我感到困惑。
... 此外，还有两种结论：显示状态数 同时命题（本质上是一个大连词），而 获得多个同时同时发生的上下文的声明 （本质上是消除的参数和 假设，参见§6.6).
shows 看起来很简单。
从我目前的有限经验来看，似乎 obtains 是关于证明一个以存在量词开头的结论，如图所示 in this question（其中结论是存在的，然后目标是obtains）。
这真的是 shows 和 obtains（普遍与存在）之间的区别吗？
如果不是，obtains 的正确用途是什么？
解决方法
引理“显示‹∃x.P x›”和“获得x，其中‹P x›`非常相似，但并不完全相同。
在证明方面，获取版本需要找到一个明确的见证人（看看这样的证明中称为that的事实）。类似的事情可以通过在节目之后应用定理 exI 来实现。
生成的引理不同。 obtains 版本生成消除规则而不是量词，因为 Pure 中没有存在量词。然而，在使用该定理时，差异并不重要。