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

Question

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

所以问题是:我什么时候会使用 presume而不是 assume ，以及我可以用 presume 做什么好技巧?

Answer 1

presume不会使 Isar 语言更具表现力，因为您可以使用 presume 重构每个证明与 assume 合二为一只要。尽管如此，至少有两个(或多或少)用例:

一、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风格，我们要做的证明 E暗示 C两次。当然，这总是可以分解为引理，但如果证明需要来自上下文的大量事实，那可能会变得丑陋。

二、可以使用 presume当您编写证明以查找 assume 中的打字错误时s 和 show s。假设你有

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

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