src/HOL/ex/Word.thy

   \<open>even (a * 2 ^ m div 2 ^ n) \<longleftrightarrow> \<not> (
     m \<le> n \<and>
     n < LENGTH('a) \<and> odd (a div 2 ^ (n - m)))\<close> for a :: \<open>'a::len word\<close>
   by transfer
     (auto simp flip: drop_bit_eq_div simp add: even_drop_bit_iff_not_bit bit_take_bit_iff,
-      simp_all flip: push_bit_eq_mult add: bit_push_bit_eq_int)
-
-(*lemma even_range_div_iff_word:
+      simp_all flip: push_bit_eq_mult add: bit_push_bit_iff_int)
+
+(*lemma even_mask_div_iff_word:
   \<open>even ((2 ^ m - 1) div (2::'a word) ^ n) \<longleftrightarrow> 2 ^ n = (0::'a::len word) \<or> m \<le> n\<close>
-  by transfer (auto simp add: take_bit_of_range even_range_div_iff)*)
+  by transfer (auto simp add: take_bit_of_mask even_mask_div_iff)*)
 
 instance word :: (len) semiring_bits
 proof
   show \<open>P a\<close> if stable: \<open>\<And>a. a div 2 = a \<Longrightarrow> P a\<close>
     and rec: \<open>\<And>a b. P a \<Longrightarrow> (of_bool b + 2 * a) div 2 = a \<Longrightarrow> P (of_bool b + 2 * a)\<close>