equal
deleted
inserted
replaced
6 theory Bit_Operations |
6 theory Bit_Operations |
7 imports |
7 imports |
8 Main |
8 Main |
9 "HOL-Library.Boolean_Algebra" |
9 "HOL-Library.Boolean_Algebra" |
10 begin |
10 begin |
|
11 |
|
12 lemma bit_numeral_int_iff [bit_simps]: \<comment> \<open>TODO: move\<close> |
|
13 \<open>bit (numeral m :: int) n \<longleftrightarrow> bit (numeral m :: nat) n\<close> |
|
14 using bit_of_nat_iff_bit [of \<open>numeral m\<close> n] by simp |
|
15 |
11 |
16 |
12 subsection \<open>Bit operations\<close> |
17 subsection \<open>Bit operations\<close> |
13 |
18 |
14 class semiring_bit_operations = semiring_bit_shifts + |
19 class semiring_bit_operations = semiring_bit_shifts + |
15 fixes "and" :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixr \<open>AND\<close> 64) |
20 fixes "and" :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixr \<open>AND\<close> 64) |