为什么单双数情况不同？

由 发布于

In this exercise auto proves the even_mul lemma while it fails to prove odd_mul.

fun is_odd :: "nat ⇒ bool" where
    "is_odd n = (n mod 2 ≠ 0)"

fun is_even :: "nat ⇒ bool" where
    "is_even n = (n mod 2 = 0)"

lemma even_mul : "is_even (n::nat) ⟹ is_even (n * n)"
  by auto

lemma odd_mul : "is_odd (n::nat) ⟹ is_odd (n * n)"
  by auto

是什么使这两种情况不同？我希望得到一个解释。