# HG changeset patch
# User haftmann
# Date 1645701909 0
# Node ID cd77ffb01e15331755762f4d9d8df88616b85444
# Parent  6b29b37de52e2b8a81d54070420b4d9a2842c360
simp rules for negative numerals

diff -r 6b29b37de52e -r cd77ffb01e15 src/HOL/Bit_Operations.thy
--- 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)