isabelle - 你什么时候会在 Isar 证明中使用“presume”？

Question

此外，Isar 还具有在 Isar 证明块中引入事实assume的命令。presume从我在文档中看到和阅读的内容来看，它不需要在目标中明确列出假设（假设？），并且似乎添加了一个案例来表明假设的陈述遵循其他目标。

所以问题是：我什么时候用presume代替assume，我可以用什么好技巧presume？

Answer 1

presume不会使 Isar 语言更具表现力，因为您可以将每个证明重组presume为一个 with assumeonly。尽管如此，至少有两个（或多或少常见）用例：

首先，presume有时会导致更自然的校样，因为您可以presume像剪切一样使用。

例如，假设您的证明状态有两个目标A ==> C和B ==> C，并且您可以证明一些E来自A和来自B给定当前上下文中E的事实和当前上下文中的事实暗示C。使用presume，您可以按如下方式构造证明：

   presume E
   show C <proof using E and facts>
   thus C .
 next
   assume A
   thus E <proof using A and facts>
   thus E .
 next
   assume B
   thus E <proof using A and facts>
   thus E .

在assume风格上，这看起来如下：

   assume A
   hence E <proof using A and facts>
   show C <proof using E and facts>
 next
   assume B
   hence E <proof using B and facts>
   show C <proof using E and facts>

有了presume，证明的结构更加明确：显然，我们只需要E展示结果，这可能是证明中有趣的部分。此外，在风格上，我们必须做两次暗示assume的证明。当然，这总是可以分解为引理，但如果证明需要大量来自上下文的事实，那可能会变得丑陋。EC

其次，您可以presume在编写证明时使用来定位assumes 和shows 中的打字错误。假设你有

 fix x
 assume A and B and C and D and E
 show F

但伊莎贝尔告诉你，这show不会解决任何目标，也就是说，你可能在假设或目标陈述中有一些错字。现在，assume变成presume. 如果show仍然失败，那么错误就在目标声明中的某个地方。否则，它可能在假设的某个地方。用关闭show证明sorry并尝试用 解除假设apply_end(assumption)+。它将停留在无法统一的假设上。可能，这是错误的。