--- a/src/HOL/Library/Bit_Operations.thy Fri May 28 20:21:23 2021 +0000
+++ b/src/HOL/Library/Bit_Operations.thy Fri May 28 20:21:25 2021 +0000
@@ -202,6 +202,24 @@
\<open>even (unset_bit m a) \<longleftrightarrow> even a \<or> m = 0\<close>
using bit_unset_bit_iff [of m a 0] by auto
+lemma and_exp_eq_0_iff_not_bit:
+ \<open>a AND 2 ^ n = 0 \<longleftrightarrow> \<not> bit a n\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+proof
+ assume ?Q
+ then show ?P
+ by (auto intro: bit_eqI simp add: bit_simps)
+next
+ assume ?P
+ show ?Q
+ proof (rule notI)
+ assume \<open>bit a n\<close>
+ then have \<open>a AND 2 ^ n = 2 ^ n\<close>
+ by (auto intro: bit_eqI simp add: bit_simps)
+ with \<open>?P\<close> show False
+ using \<open>bit a n\<close> exp_eq_0_imp_not_bit by auto
+ qed
+qed
+
lemmas flip_bit_def = flip_bit_eq_xor
lemma bit_flip_bit_iff [bit_simps]:
--- 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