1

假设我有一个前提，例如A ∨ B ∨ C，并且想证明P。证明它的自然方法是证明A ⟹ P和。但是，它适用于 2 种情况，因此我必须应用两次：B ⟹ PC ⟹ PdisjE

lemma foo: 
  assumes "A ∨ B ∨ C"
  shows "P"
proof (rule disjE)
  assume "A"
  ...
  then show "P"
next
  assume "B ∨ C"
  then show "P"
  proof (rule disjE)
    assume "B"
    ...
    then show "P"
  next
    assume "C"
    ...
    then show "P"
  qed
qed

当然，现在我可以证明我自己的lemma disjE_3 [rulify]: assumes "P ∨ Q ∨ R" "P ⟹ A" "Q ⟹ A" "R ⟹ A" shows "A"并改用它，这将产生一个更具可读性的证明：

lemma foo: 
  assumes "A ∨ B ∨ C"
  shows "P"
proof (rule disjE_3)
  assume "A"
  ...
  then show "P"
next
  assume "B"
  ...
  then show "P"
next
  assume "C"
  ...
  then show "P"
qed

另一方面，如果我有 4 例、5 例或 10 例怎么办？为您可能需要的每个案例创建规则似乎非常不方便。尽管您可以一次应用多个规则，proof (rule disjE disjE)但在这种情况下似乎并没有削减它。

那么，有没有办法通过尽可能多地应用规则来将子目标减少到“最小形式”？

4

0 回答 0