isabelle - Isabelle Isar 中的“shows”和“obtains”有什么区别？

Question

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

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

shows似乎直截了当。

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

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

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

Answer 1

引理“显示‹∃x.P x›”和“获得x，其中‹P x›`非常相似，但不完全相同。

在证明方面，获取版本需要找到明确的证人（查看that此类证明中调用的事实）。类似的事情可以通过exI在演出后应用该定理来实现。

生成的引理是不同的。该obtains版本生成消除规则而不是量化规则，因为 Pure 中没有存在量词。但是，在使用该定理时，差异并不重要。