证明中的自定义案例区别

Question

伊莎贝尔在证明陈述时是否支持自定义案例区分？假设我想为所有自然数 n 证明一个命题，但根据 n 是偶数还是奇数，证明完全不同。是否可以在证明中区分大小写，例如

 proof(cases n) 
   assume "n mod 2 = 0"
   <proof>
   next assume "n mod 2 = 1"
   <proof>
qed

到目前为止，我将 lemma/theorem 分成两个独立的部分（假设 n even/odd），然后使用这些部分来证明所有自然数的陈述，但是这似乎不是最佳解决方案。

Answer 1

在Isabelle2017中，您可以轻松证明ad-hoc case区分规则，如下所示：

lemma "P (n::nat)"
proof -
  consider (odd) "odd n" | (even) "even n" by auto
  then show ?thesis
  proof cases
    case odd
    then show ?thesis sorry
  next
    case even
    then show ?thesis sorry
  qed
qed

Answer 2

您或许可以尝试以下操作：

proof -
   have "your statement" when "n mod 2 = 0"
   <proof>
   moreover
   have "your statement" when "n mod 2 = 1"
   <proof>
   ultimately
   show "your statement"
     by <some tactic>
qed

证明中的自定义案例区别

Custom case distinctions in proofs

isabelle

isar