如何解决Isabelle Isar 中的“shows”和“obtains”有什么区别？
我试图了解 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 中没有存在量词。然而，在使用该定理时，差异并不重要。
版权声明：本文内容由互联网用户自发贡献，该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容， 请发送邮件至 dio@foxmail.com 举报，一经查实，本站将立刻删除。
