--- a/src/HOL/Library/Bit_Operations.thy Wed Jun 23 18:38:37 2021 +0000
+++ b/src/HOL/Library/Bit_Operations.thy Thu Jun 24 06:06:32 2021 +0000
@@ -9,11 +9,6 @@
"HOL-Library.Boolean_Algebra"
begin
-lemma bit_numeral_int_iff [bit_simps]: \<comment> \<open>TODO: move\<close>
- \<open>bit (numeral m :: int) n \<longleftrightarrow> bit (numeral m :: nat) n\<close>
- using bit_of_nat_iff_bit [of \<open>numeral m\<close> n] by simp
-
-
subsection \<open>Bit operations\<close>
class semiring_bit_operations = semiring_bit_shifts +
--- a/src/HOL/Parity.thy Wed Jun 23 18:38:37 2021 +0000
+++ b/src/HOL/Parity.thy Thu Jun 24 06:06:32 2021 +0000
@@ -1818,6 +1818,10 @@
instance int :: unique_euclidean_semiring_with_bit_shifts ..
+lemma bit_numeral_int_iff [bit_simps]:
+ \<open>bit (numeral m :: int) n \<longleftrightarrow> bit (numeral m :: nat) n\<close>
+ using bit_of_nat_iff_bit [of \<open>numeral m\<close> n] by simp
+
lemma bit_not_int_iff':
\<open>bit (- k - 1) n \<longleftrightarrow> \<not> bit k n\<close>
for k :: int