equal
deleted
inserted
replaced
202 lemmas word_and_le2 = |
202 lemmas word_and_le2 = |
203 xtr3 [OF word_ao_absorbs (8) [symmetric] le_word_or2, standard] |
203 xtr3 [OF word_ao_absorbs (8) [symmetric] le_word_or2, standard] |
204 |
204 |
205 lemma bl_word_not: "to_bl (NOT w) = map Not (to_bl w)" |
205 lemma bl_word_not: "to_bl (NOT w) = map Not (to_bl w)" |
206 unfolding to_bl_def word_log_defs |
206 unfolding to_bl_def word_log_defs |
207 by (simp add: bl_not_bin number_of_is_id word_no_wi [symmetric]) |
207 by (simp add: bl_not_bin number_of_is_id word_no_wi [symmetric] bin_to_bl_def[symmetric]) |
208 |
208 |
209 lemma bl_word_xor: "to_bl (v XOR w) = map2 op ~= (to_bl v) (to_bl w)" |
209 lemma bl_word_xor: "to_bl (v XOR w) = map2 op ~= (to_bl v) (to_bl w)" |
210 unfolding to_bl_def word_log_defs bl_xor_bin |
210 unfolding to_bl_def word_log_defs bl_xor_bin |
211 by (simp add: number_of_is_id word_no_wi [symmetric]) |
211 by (simp add: number_of_is_id word_no_wi [symmetric]) |
212 |
212 |