--- a/src/HOL/ex/Word.thy Thu May 21 20:00:08 2020 +0000
+++ b/src/HOL/ex/Word.thy Thu May 21 20:00:09 2020 +0000
@@ -716,6 +716,20 @@
end
+definition even_word :: \<open>'a::len word \<Rightarrow> bool\<close>
+ where [code_abbrev]: \<open>even_word = even\<close>
+
+lemma even_word_iff [code]:
+ \<open>even_word a \<longleftrightarrow> a AND 1 = 0\<close>
+ by (simp add: even_word_def even_iff_mod_2_eq_zero)
+
+definition bit_word :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> bool\<close>
+ where [code_abbrev]: \<open>bit_word = bit\<close>
+
+lemma bit_word_iff [code]:
+ \<open>bit_word a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close>
+ by (simp add: bit_word_def bit_iff_odd_drop_bit odd_iff_mod_2_eq_one)
+
lifting_update word.lifting
lifting_forget word.lifting