在 Isabelle 中将 &&& 形式的连词分解为子目标

Question

如果我用 Isar 写这样的东西：

have "(x ↔ z) ∙ R = (xa ↔ z) ∙ S" 
     "(x ↔ z) ∙ T = (xa ↔ z) ∙ Ta" 
     "(x ↔ z) ∙ q = (xa ↔ z) ∙ t"

我会得到一个子目标：

(x ↔ z) ∙ R = (xa ↔ z) ∙ S &&&
(x ↔ z) ∙ T = (xa ↔ z) ∙ Ta &&&
(x ↔ z) ∙ q = (xa ↔ z) ∙ t

如何将这个 &&& 分成三个子目标？

Answer 1

通常只有当一个引理有多个陈述时才会遇到这样的子目标，这没什么好担心的。这在日常使用中几乎不可能造成任何问题-您可以忽略它。

详细说明：当您写出类似 lemma P1 P2 的内容时，您确实将 P1 &&& P2 视为证明义务。但是，请不要为此感到惊慌：如果您使用运行 any 证明方法，则此元合取会立即拆分，并且您有两个单独的子目标 P1 和P2甚至在该方法看到目标之前。所以从一开始就假设它是两个独立的子目标。

（如果有足够的犯罪能量，这种自动分裂可能是可以避免的，但前提是你要定义自己的证明方法。）

Answer 2

正如@Manuel 所说，通常的证明方法会自动为您拆分子目标。在极少数情况下，您使用的方法不会执行此操作，- 方法也会拆分 &&& 元连词。您可能已经在 proof - 中看到过它，它也可以是 apply-ed.

在 Isabelle 中将 &&& 形式的连词分解为子目标

Breaking conjunctions of the form &&& into subgoals in Isabelle

isabelle