证明中的自定义案例区别答案

【问题标题】：Custom case distinctions in proofs证明中的自定义案例区别
【发布时间】：2018-07-05 18:32:54
【问题描述】：

Isabelle 在证明陈述时是否支持自定义案例区分？假设我想证明所有自然数 n 的陈述，但证明完全不同，具体取决于 n 是偶数还是奇数。是否可以在证明中区分这种情况，例如

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

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

【问题讨论】：

标签： isabelle isar

【解决方案1】：

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

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

【讨论】：

虽然这是真的（并且有一些优点，例如可以使用case），但odd n 只是¬even n 的缩写，所以可以只使用默认大小写区分规则：have P proof cases assume "even n" … next assume "odd n" … qed

【解决方案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

【讨论】：