--- a/src/HOL/Library/Word.thy Fri May 28 20:21:23 2021 +0000
+++ b/src/HOL/Library/Word.thy Fri May 28 20:21:25 2021 +0000
@@ -920,6 +920,16 @@
by (rule finite_subset)
qed
+lemma bit_numeral_word_iff [simp]:
+ \<open>bit (numeral w :: 'a::len word) n
+ \<longleftrightarrow> n < LENGTH('a) \<and> bit (numeral w :: int) n\<close>
+ by transfer simp
+
+lemma bit_neg_numeral_word_iff [simp]:
+ \<open>bit (- numeral w :: 'a::len word) n
+ \<longleftrightarrow> n < LENGTH('a) \<and> bit (- numeral w :: int) n\<close>
+ by transfer simp
+
instantiation word :: (len) semiring_bit_shifts
begin