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
I'd appreciate an explanation on how the two cases differ, and hints on how to prove odd_mul, as well.
You can prove odd_mul by adding the lemma mod2_eq_if to the simplification rules as follows:
lemma odd_mul : "is_odd (n::nat) ⟹ is_odd (n * n)"
by (simp add: mod2_eq_if)
To understand why the auto method proves even_mul but fails to prove odd_mul, let's have a look at the respective simplifier traces (only the relevant parts are shown). The trace for even_mul is shown below:
...
[1]Rewriting:
is_even (n * n) ≡ n * n mod 2 = 0
[1]Applying instance of rewrite rule "Rings.semidom_modulo_class.dvd_imp_mod_0":
?a1 dvd ?b1 ⟹ ?b1 mod ?a1 ≡ 0
[1]Trying to rewrite:
even (n * n) ⟹ n * n mod 2 ≡ 0
[2]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
even (n * n)
[2]Applying instance of rewrite rule "Parity.semiring_parity_class.even_mult_iff":
even (?a1 * ?b1) ≡ even ?a1 ∨ even ?b1
[2]Rewriting:
even (n * n) ≡ even n ∨ even n
...
We can see that the simplifier is able to use the rewrite rule even (?a1 * ?b1) ≡ even ?a1 ∨ even ?b1 from the Parity theory because the definitions of even and is_even turn out to be the same when rewriting even using dvd_imp_mod_0 from Rings.semidom_modulo_class.
However, this is not the case for odd and is_odd, since odd a ≡ ¬ 2 dvd a and the simplifier cannot rewrite it to use is_odd without additional help from the user, as shown in the output panel:
theorem odd_mul: is_odd ?n ⟹ is_odd (?n * ?n)
Failed to finish proof⌂:
goal (1 subgoal):
1. n mod 2 = Suc 0 ⟹ n * n mod 2 = Suc 0
However, in the proof of odd_mul at the top of this post, we explicitly provide the additional rewrite rule mod2_eq_if to help the simplifier bridge the gap between odd and is_odd as shown in the trace below:
...
[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
is_odd n ⟹ is_odd (n * n)
[1]Applying instance of rewrite rule "??.unknown":
is_odd ?n1 ≡ ?n1 mod 2 ≠ 0
[1]Rewriting:
is_odd n ≡ n mod 2 ≠ 0
[1]Applying instance of rewrite rule "Parity.semiring_parity_class.mod2_eq_if":
?x1 mod 2 ≡ if even ?x1 then 0 else 1
[1]Rewriting:
n mod 2 ≡ if even n then 0 else 1
[1]Applying congruence rule:
even n ≡ ?c ⟹ if even n then 0 else 1 ≡ if ?c then 0 else 1
[2]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
even n ≡ ?c
[1]SUCCEEDED
...
Hope this helps.