5 contains theorems to do with bit-wise (logical) operations on words |
5 contains theorems to do with bit-wise (logical) operations on words |
6 *) |
6 *) |
7 |
7 |
8 header {* Bitwise Operations on Words *} |
8 header {* Bitwise Operations on Words *} |
9 |
9 |
10 theory WordBitwise imports WordArith begin |
10 theory WordBitwise |
|
11 imports WordArith |
|
12 begin |
11 |
13 |
12 lemmas bin_log_bintrs = bin_trunc_not bin_trunc_xor bin_trunc_and bin_trunc_or |
14 lemmas bin_log_bintrs = bin_trunc_not bin_trunc_xor bin_trunc_and bin_trunc_or |
13 |
15 |
14 (* following definitions require both arithmetic and bit-wise word operations *) |
16 (* following definitions require both arithmetic and bit-wise word operations *) |
15 |
17 |
203 |
205 |
204 lemma bl_word_not: "to_bl (NOT w) = map Not (to_bl w)" |
206 lemma bl_word_not: "to_bl (NOT w) = map Not (to_bl w)" |
205 unfolding to_bl_def word_log_defs |
207 unfolding to_bl_def word_log_defs |
206 by (simp add: bl_not_bin number_of_is_id word_no_wi [symmetric]) |
208 by (simp add: bl_not_bin number_of_is_id word_no_wi [symmetric]) |
207 |
209 |
208 lemma bl_word_xor: "to_bl (v XOR w) = app2 op ~= (to_bl v) (to_bl w)" |
210 lemma bl_word_xor: "to_bl (v XOR w) = map2 op ~= (to_bl v) (to_bl w)" |
209 unfolding to_bl_def word_log_defs bl_xor_bin |
211 unfolding to_bl_def word_log_defs bl_xor_bin |
210 by (simp add: number_of_is_id word_no_wi [symmetric]) |
212 by (simp add: number_of_is_id word_no_wi [symmetric]) |
211 |
213 |
212 lemma bl_word_or: "to_bl (v OR w) = app2 op | (to_bl v) (to_bl w)" |
214 lemma bl_word_or: "to_bl (v OR w) = map2 op | (to_bl v) (to_bl w)" |
213 unfolding to_bl_def word_log_defs |
215 unfolding to_bl_def word_log_defs |
214 by (simp add: bl_or_bin number_of_is_id word_no_wi [symmetric]) |
216 by (simp add: bl_or_bin number_of_is_id word_no_wi [symmetric]) |
215 |
217 |
216 lemma bl_word_and: "to_bl (v AND w) = app2 op & (to_bl v) (to_bl w)" |
218 lemma bl_word_and: "to_bl (v AND w) = map2 op & (to_bl v) (to_bl w)" |
217 unfolding to_bl_def word_log_defs |
219 unfolding to_bl_def word_log_defs |
218 by (simp add: bl_and_bin number_of_is_id word_no_wi [symmetric]) |
220 by (simp add: bl_and_bin number_of_is_id word_no_wi [symmetric]) |
219 |
221 |
220 lemma word_lsb_alt: "lsb (w::'a::len0 word) = test_bit w 0" |
222 lemma word_lsb_alt: "lsb (w::'a::len0 word) = test_bit w 0" |
221 by (auto simp: word_test_bit_def word_lsb_def) |
223 by (auto simp: word_test_bit_def word_lsb_def) |