slightly more specific implementations
authorhaftmann
Thu May 21 20:00:09 2020 +0000 (6 weeks ago)
changeset 718546a51e64ba13d
parent 71853 30d92e668b52
child 71855 3e343c0c2138
child 71861 1330fa4a2b85
slightly more specific implementations
src/HOL/ex/Word.thy
     1.1 --- a/src/HOL/ex/Word.thy	Thu May 21 20:00:08 2020 +0000
     1.2 +++ b/src/HOL/ex/Word.thy	Thu May 21 20:00:09 2020 +0000
     1.3 @@ -716,6 +716,20 @@
     1.4  
     1.5  end
     1.6  
     1.7 +definition even_word :: \<open>'a::len word \<Rightarrow> bool\<close>
     1.8 +  where [code_abbrev]: \<open>even_word = even\<close>
     1.9 +
    1.10 +lemma even_word_iff [code]:
    1.11 +  \<open>even_word a \<longleftrightarrow> a AND 1 = 0\<close>
    1.12 +  by (simp add: even_word_def even_iff_mod_2_eq_zero)
    1.13 +
    1.14 +definition bit_word :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> bool\<close>
    1.15 +  where [code_abbrev]: \<open>bit_word = bit\<close>
    1.16 +
    1.17 +lemma bit_word_iff [code]:
    1.18 +  \<open>bit_word a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close>
    1.19 +  by (simp add: bit_word_def bit_iff_odd_drop_bit odd_iff_mod_2_eq_one)
    1.20 +
    1.21  lifting_update word.lifting
    1.22  lifting_forget word.lifting
    1.23