Isabelle证明中能否实现自定义分情况讨论（如自然数奇偶）？

当然可以直接这么做！Isabelle的cases证明方法完全支持这种自定义的分情况讨论，不需要把命题拆成两个独立引理——这正是分情况证明的标准用法之一，比拆分方案更简洁连贯。

直接用模2条件分情况的示例 #

你给出的思路完全可行，这里给你一个具体的代码示例，比如证明自然数的平方与自身模2结果相等：

theorem nat_square_mod2_eq:
  fixes n :: nat
  shows "n^2 mod 2 = n mod 2"
proof (cases n)
  assume "n mod 2 = 0"
  -- 把偶数表示为2k的形式，简化后续推导
  then obtain k where "n = 2 * k" by (auto simp add: even_iff_divisible_by_2)
  -- 代入平方展开后自动化简
  then show ?thesis by (simp add: power2_eq_square)
next
  assume "n mod 2 = 1"
  -- 把奇数表示为2k+1的形式
  then obtain k where "n = 2 * k + 1" by (auto simp add: odd_iff_not_even)
  -- 展开平方后用代数规则化简
  then show ?thesis by (simp add: power2_eq_square algebra_simps)
qed

更直观的even/odd谓词写法 #

Isabelle的自然数库中已经定义了even n和odd n谓词，还有现成的nat_even_or_odd规则（保证每个自然数要么是偶数要么是奇数），用这个规则分情况会更直观：

theorem nat_square_mod2_eq:
  fixes n :: nat
  shows "n^2 mod 2 = n mod 2"
proof (cases n rule: nat_even_or_odd)
  assume "even n"
  then obtain k where "n = 2 * k" by (rule evenE)
  then show ?thesis by (simp add: power2_eq_square)
next
  assume "odd n"
  then obtain k where "n = 2 * k + 1" by (rule oddE)
  then show ?thesis by (simp add: power2_eq_square algebra_simps)
qed

关键说明 #

• 两种写法都能在同一个证明块内完成奇偶分支的推导，不需要拆分命题；
• 使用obtain可以把奇偶性转化为具体的表达式（2k或2k+1），方便后续的代数运算或逻辑推导；
• 如果你的证明分支逻辑比较复杂，还可以在每个分支内部嵌套子证明（比如用proof - ... qed），保持结构清晰。

内容的提问来源于stack exchange，提问作者Benedikt