diff -r db43ee05066d -r beeadb35e357 src/HOL/Library/Bit_Operations.thy
--- a/src/HOL/Library/Bit_Operations.thy	Wed Sep 23 08:52:41 2020 +0000
+++ b/src/HOL/Library/Bit_Operations.thy	Wed Sep 23 11:14:38 2020 +0000
@@ -159,6 +159,10 @@
   by (rule bit_eqI)
     (auto simp add: bit_take_bit_iff bit_and_iff bit_mask_iff)
 
+lemma or_eq_0_iff:
+  \<open>a OR b = 0 \<longleftrightarrow> a = 0 \<and> b = 0\<close>
+	by (auto simp add: bit_eq_iff bit_or_iff)
+
 lemma disjunctive_add:
   \<open>a + b = a OR b\<close> if \<open>\<And>n. \<not> bit a n \<or> \<not> bit b n\<close>
   by (rule bit_eqI) (use that in \<open>simp add: bit_disjunctive_add_iff bit_or_iff\<close>)
@@ -249,6 +253,30 @@
   \<open>NOT (a - b) = NOT a + b\<close>
   using not_add_distrib [of a \<open>- b\<close>] by simp
 
+lemma (in ring_bit_operations) and_eq_minus_1_iff:
+  \<open>a AND b = - 1 \<longleftrightarrow> a = - 1 \<and> b = - 1\<close>
+proof
+  assume \<open>a = - 1 \<and> b = - 1\<close>
+  then show \<open>a AND b = - 1\<close>
+	by simp
+next
+  assume \<open>a AND b = - 1\<close>
+  have *: \<open>bit a n\<close> \<open>bit b n\<close> if \<open>2 ^ n \<noteq> 0\<close> for n
+  proof -
+    from \<open>a AND b = - 1\<close>
+    have \<open>bit (a AND b) n = bit (- 1) n\<close>
+      by (simp add: bit_eq_iff)
+    then show \<open>bit a n\<close> \<open>bit b n\<close>
+	    using that by (simp_all add: bit_and_iff)
+  qed
+  have \<open>a = - 1\<close>
+    by (rule bit_eqI) (simp add: *)
+  moreover have \<open>b = - 1\<close>
+    by (rule bit_eqI) (simp add: *)
+  ultimately show \<open>a = - 1 \<and> b = - 1\<close>
+    by simp
+qed
+
 lemma disjunctive_diff:
   \<open>a - b = a AND NOT b\<close> if \<open>\<And>n. bit b n \<Longrightarrow> bit a n\<close>
 proof -