255 by (simp add: bit_not_iff bit_mask_iff bit_push_bit_iff not_le) |
255 by (simp add: bit_not_iff bit_mask_iff bit_push_bit_iff not_le) |
256 qed |
256 qed |
257 qed |
257 qed |
258 |
258 |
259 definition set_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close> |
259 definition set_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close> |
260 where \<open>set_bit n a = a OR 2 ^ n\<close> |
260 where \<open>set_bit n a = a OR push_bit n 1\<close> |
261 |
261 |
262 definition unset_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close> |
262 definition unset_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close> |
263 where \<open>unset_bit n a = a AND NOT (2 ^ n)\<close> |
263 where \<open>unset_bit n a = a AND NOT (push_bit n 1)\<close> |
264 |
264 |
265 definition flip_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close> |
265 definition flip_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close> |
266 where \<open>flip_bit n a = a XOR 2 ^ n\<close> |
266 where \<open>flip_bit n a = a XOR push_bit n 1\<close> |
267 |
267 |
268 lemma bit_set_bit_iff: |
268 lemma bit_set_bit_iff: |
269 \<open>bit (set_bit m a) n \<longleftrightarrow> bit a n \<or> (m = n \<and> 2 ^ n \<noteq> 0)\<close> |
269 \<open>bit (set_bit m a) n \<longleftrightarrow> bit a n \<or> (m = n \<and> 2 ^ n \<noteq> 0)\<close> |
270 by (auto simp add: set_bit_def bit_or_iff bit_exp_iff) |
270 by (auto simp add: set_bit_def push_bit_of_1 bit_or_iff bit_exp_iff) |
271 |
271 |
272 lemma even_set_bit_iff: |
272 lemma even_set_bit_iff: |
273 \<open>even (set_bit m a) \<longleftrightarrow> even a \<and> m \<noteq> 0\<close> |
273 \<open>even (set_bit m a) \<longleftrightarrow> even a \<and> m \<noteq> 0\<close> |
274 using bit_set_bit_iff [of m a 0] by auto |
274 using bit_set_bit_iff [of m a 0] by auto |
275 |
275 |
276 lemma bit_unset_bit_iff: |
276 lemma bit_unset_bit_iff: |
277 \<open>bit (unset_bit m a) n \<longleftrightarrow> bit a n \<and> m \<noteq> n\<close> |
277 \<open>bit (unset_bit m a) n \<longleftrightarrow> bit a n \<and> m \<noteq> n\<close> |
278 by (auto simp add: unset_bit_def bit_and_iff bit_not_iff bit_exp_iff exp_eq_0_imp_not_bit) |
278 by (auto simp add: unset_bit_def push_bit_of_1 bit_and_iff bit_not_iff bit_exp_iff exp_eq_0_imp_not_bit) |
279 |
279 |
280 lemma even_unset_bit_iff: |
280 lemma even_unset_bit_iff: |
281 \<open>even (unset_bit m a) \<longleftrightarrow> even a \<or> m = 0\<close> |
281 \<open>even (unset_bit m a) \<longleftrightarrow> even a \<or> m = 0\<close> |
282 using bit_unset_bit_iff [of m a 0] by auto |
282 using bit_unset_bit_iff [of m a 0] by auto |
283 |
283 |
284 lemma bit_flip_bit_iff: |
284 lemma bit_flip_bit_iff: |
285 \<open>bit (flip_bit m a) n \<longleftrightarrow> (m = n \<longleftrightarrow> \<not> bit a n) \<and> 2 ^ n \<noteq> 0\<close> |
285 \<open>bit (flip_bit m a) n \<longleftrightarrow> (m = n \<longleftrightarrow> \<not> bit a n) \<and> 2 ^ n \<noteq> 0\<close> |
286 by (auto simp add: flip_bit_def bit_xor_iff bit_exp_iff exp_eq_0_imp_not_bit) |
286 by (auto simp add: flip_bit_def push_bit_of_1 bit_xor_iff bit_exp_iff exp_eq_0_imp_not_bit) |
287 |
287 |
288 lemma even_flip_bit_iff: |
288 lemma even_flip_bit_iff: |
289 \<open>even (flip_bit m a) \<longleftrightarrow> \<not> (even a \<longleftrightarrow> m = 0)\<close> |
289 \<open>even (flip_bit m a) \<longleftrightarrow> \<not> (even a \<longleftrightarrow> m = 0)\<close> |
290 using bit_flip_bit_iff [of m a 0] by auto |
290 using bit_flip_bit_iff [of m a 0] by auto |
291 |
291 |