isabelle - 有没有办法自动拆分连词？

Question

我想A /\ B /\ C /\ D /\ E /\ F在伊莎贝尔身上证明。如何在 中自动将子目标拆分为 6 个单独的子目标proof(rule ...)，然后我可以分别证明它们？

当然，我可以写proof(rule conjI)5 次，但也许有更优雅的方式来一步拆分？

Answer 1

使用intro方法：proof (intro conjI)

Answer 2

证明此类目标的另一种方法是使用原始证明块。例如，如下

lemma "A & B & C & D & E & F"
proof -
  { have "A" ... }
  moreover
  { have "B" ... }
  moreover
  { have "C" ... }
  moreover
  { have "D" ... }
  moreover
  { have "E" ... }
  moreover
  { have "F" ... }
  ultimately
  show ?thesis by blast
qed

不同之处在于，在这里你做了一个更前向的证明（我发现有时更具可读性）。你只是从你知道的开始，无论如何你必须在某个时候证明，最后让一些自动化方法（这里blast）找出“微不足道”的步骤。