# HG changeset patch
# User haftmann
# Date 1622233285 0
# Node ID aab7975fa070bf59093221ba793754b2dd5d8fe6
# Parent  35217bf33215d6481130f41384ad348445209d49
more lemmas

diff -r 35217bf33215 -r aab7975fa070 src/HOL/Library/Bit_Operations.thy
--- 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]:
diff -r 35217bf33215 -r aab7975fa070 src/HOL/Library/Word.thy
--- 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