more complete rules on numerals

--- a/src/HOL/Parity.thy	Thu Apr 16 00:37:07 2020 +0200
+++ b/src/HOL/Parity.thy	Thu Apr 16 08:09:28 2020 +0200
@@ -152,6 +152,10 @@
   then show False by simp
 qed
 
+lemma odd_numeral_BitM [simp]:
+  \<open>odd (numeral (Num.BitM w))\<close>
+  by (cases w) simp_all
+
 lemma even_power [simp]: "even (a ^ n) \<longleftrightarrow> even a \<and> n > 0"
   by (induct n) auto