equal
deleted
inserted
replaced
1582 then show \<open>bit (take_bit n a) m \<longleftrightarrow> bit a m\<close> |
1582 then show \<open>bit (take_bit n a) m \<longleftrightarrow> bit a m\<close> |
1583 by (cases \<open>m < n\<close>) (auto simp add: bit_simps) |
1583 by (cases \<open>m < n\<close>) (auto simp add: bit_simps) |
1584 qed |
1584 qed |
1585 qed |
1585 qed |
1586 |
1586 |
|
1587 lemma drop_bit_exp_eq: |
|
1588 \<open>drop_bit m (2 ^ n) = of_bool (m \<le> n \<and> 2 ^ n \<noteq> 0) * 2 ^ (n - m)\<close> |
|
1589 by (rule bit_eqI) (auto simp add: bit_simps) |
|
1590 |
1587 end |
1591 end |
1588 |
1592 |
1589 instantiation nat :: semiring_bit_shifts |
1593 instantiation nat :: semiring_bit_shifts |
1590 begin |
1594 begin |
1591 |
1595 |