--- a/src/HOL/Bit_Operations.thy Wed Feb 23 23:24:26 2022 +0100
+++ b/src/HOL/Bit_Operations.thy Thu Feb 24 11:25:09 2022 +0000
@@ -2792,13 +2792,9 @@
subsection \<open>Symbolic computations on numeral expressions\<close>
-context unique_euclidean_semiring_with_bit_operations
+context semiring_bits
begin
-lemma bit_numeral_iff:
- \<open>bit (numeral m) n \<longleftrightarrow> bit (numeral m :: nat) n\<close>
- using bit_of_nat_iff_bit [of \<open>numeral m\<close> n] by simp
-
lemma not_bit_numeral_Bit0_0 [simp]:
\<open>\<not> bit (numeral (Num.Bit0 m)) 0\<close>
by (simp add: bit_0)
@@ -2807,6 +2803,28 @@
\<open>bit (numeral (Num.Bit1 m)) 0\<close>
by (simp add: bit_0)
+end
+
+context ring_bit_operations
+begin
+
+lemma not_bit_minus_numeral_Bit0_0 [simp]:
+ \<open>\<not> bit (- numeral (Num.Bit0 m)) 0\<close>
+ by (simp add: bit_0)
+
+lemma bit_minus_numeral_Bit1_0 [simp]:
+ \<open>bit (- numeral (Num.Bit1 m)) 0\<close>
+ by (simp add: bit_0)
+
+end
+
+context unique_euclidean_semiring_with_bit_operations
+begin
+
+lemma bit_numeral_iff:
+ \<open>bit (numeral m) n \<longleftrightarrow> bit (numeral m :: nat) n\<close>
+ using bit_of_nat_iff_bit [of \<open>numeral m\<close> n] by simp
+
lemma bit_numeral_Bit0_Suc_iff [simp]:
\<open>bit (numeral (Num.Bit0 m)) (Suc n) \<longleftrightarrow> bit (numeral m) n\<close>
by (simp add: bit_Suc numeral_Bit0_div_2)