Why the odd-even cases differ?

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.