# HG changeset patch
# User haftmann
# Date 1590091209 0
# Node ID 6a51e64ba13df930acc4aae03bd01ade34931b9f
# Parent  30d92e668b52113422e3f8cfa7c7c9bdbabe0bfd
slightly more specific implementations

diff -r 30d92e668b52 -r 6a51e64ba13d src/HOL/ex/Word.thy
--- 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