equal
deleted
inserted
replaced
642 |
642 |
643 lift_definition xor_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" |
643 lift_definition xor_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" |
644 is xor |
644 is xor |
645 by simp |
645 by simp |
646 |
646 |
647 instance proof |
647 lift_definition mask_word :: \<open>nat \<Rightarrow> 'a word\<close> |
648 fix a b :: \<open>'a word\<close> and n :: nat |
648 is mask . |
649 show \<open>- a = NOT (a - 1)\<close> |
649 |
650 by transfer (simp add: minus_eq_not_minus_1) |
650 instance by (standard; transfer) |
651 show \<open>bit (NOT a) n \<longleftrightarrow> (2 :: 'a word) ^ n \<noteq> 0 \<and> \<not> bit a n\<close> |
651 (auto simp add: minus_eq_not_minus_1 mask_eq_exp_minus_1 |
652 by transfer (simp add: bit_not_iff) |
652 bit_not_iff bit_and_iff bit_or_iff bit_xor_iff) |
653 show \<open>bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close> |
|
654 by transfer (auto simp add: bit_and_iff) |
|
655 show \<open>bit (a OR b) n \<longleftrightarrow> bit a n \<or> bit b n\<close> |
|
656 by transfer (auto simp add: bit_or_iff) |
|
657 show \<open>bit (a XOR b) n \<longleftrightarrow> bit a n \<noteq> bit b n\<close> |
|
658 by transfer (auto simp add: bit_xor_iff) |
|
659 qed |
|
660 |
653 |
661 end |
654 end |
662 |
655 |
663 definition even_word :: \<open>'a::len word \<Rightarrow> bool\<close> |
656 definition even_word :: \<open>'a::len word \<Rightarrow> bool\<close> |
664 where [code_abbrev]: \<open>even_word = even\<close> |
657 where [code_abbrev]: \<open>even_word = even\<close> |