src/HOL/Library/Bit_Operations.thy

 class semiring_bit_operations = semiring_bit_shifts +
   fixes "and" :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr \<open>AND\<close> 64)
     and or :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr \<open>OR\<close>  59)
     and xor :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr \<open>XOR\<close> 59)
     and mask :: \<open>nat \<Rightarrow> 'a\<close>
-  assumes bit_and_iff [bit_simps]: \<open>\<And>n. bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close>
-    and bit_or_iff [bit_simps]: \<open>\<And>n. bit (a OR b) n \<longleftrightarrow> bit a n \<or> bit b n\<close>
-    and bit_xor_iff [bit_simps]: \<open>\<And>n. bit (a XOR b) n \<longleftrightarrow> bit a n \<noteq> bit b n\<close>
+    and set_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
+    and unset_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
+    and flip_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
+  assumes bit_and_iff [bit_simps]: \<open>bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close>
+    and bit_or_iff [bit_simps]: \<open>bit (a OR b) n \<longleftrightarrow> bit a n \<or> bit b n\<close>
+    and bit_xor_iff [bit_simps]: \<open>bit (a XOR b) n \<longleftrightarrow> bit a n \<noteq> bit b n\<close>
     and mask_eq_exp_minus_1: \<open>mask n = 2 ^ n - 1\<close>
+    and set_bit_eq_or: \<open>set_bit n a = a OR push_bit n 1\<close>
+    and bit_unset_bit_iff [bit_simps]: \<open>bit (unset_bit m a) n \<longleftrightarrow> bit a n \<and> m \<noteq> n\<close>
+    and flip_bit_eq_xor: \<open>flip_bit n a = a XOR push_bit n 1\<close>
 begin
 
 text \<open>
   We want the bitwise operations to bind slightly weaker
   than \<open>+\<close> and \<open>-\<close>.

   apply (cases \<open>2 ^ n = 0\<close>)
   apply (simp_all add: push_bit_of_1 bit_eq_iff bit_and_iff bit_push_bit_iff exp_eq_0_imp_not_bit)
   apply (simp_all add: bit_exp_iff)
   done
 
-end
-
-class ring_bit_operations = semiring_bit_operations + ring_parity +
-  fixes not :: \<open>'a \<Rightarrow> 'a\<close>  (\<open>NOT\<close>)
-  assumes bit_not_iff [bit_simps]: \<open>\<And>n. bit (NOT a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> \<not> bit a n\<close>
-  assumes minus_eq_not_minus_1: \<open>- a = NOT (a - 1)\<close>
-begin
-
-text \<open>
-  For the sake of code generation \<^const>\<open>not\<close> is specified as
-  definitional class operation.  Note that \<^const>\<open>not\<close> has no
-  sensible definition for unlimited but only positive bit strings
-  (type \<^typ>\<open>nat\<close>).
-\<close>
-
-lemma bits_minus_1_mod_2_eq [simp]:
-  \<open>(- 1) mod 2 = 1\<close>
-  by (simp add: mod_2_eq_odd)
-
-lemma not_eq_complement:
-  \<open>NOT a = - a - 1\<close>
-  using minus_eq_not_minus_1 [of \<open>a + 1\<close>] by simp
-
-lemma minus_eq_not_plus_1:
-  \<open>- a = NOT a + 1\<close>
-  using not_eq_complement [of a] by simp
-
-lemma bit_minus_iff [bit_simps]:
-  \<open>bit (- a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> \<not> bit (a - 1) n\<close>
-  by (simp add: minus_eq_not_minus_1 bit_not_iff)
-
-lemma even_not_iff [simp]:
-  "even (NOT a) \<longleftrightarrow> odd a"
-  using bit_not_iff [of a 0] by auto
-
-lemma bit_not_exp_iff [bit_simps]:
-  \<open>bit (NOT (2 ^ m)) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n \<noteq> m\<close>
-  by (auto simp add: bit_not_iff bit_exp_iff)
-
-lemma bit_minus_1_iff [simp]:
-  \<open>bit (- 1) n \<longleftrightarrow> 2 ^ n \<noteq> 0\<close>
-  by (simp add: bit_minus_iff)
-
-lemma bit_minus_exp_iff [bit_simps]:
-  \<open>bit (- (2 ^ m)) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n \<ge> m\<close>
-  by (auto simp add: bit_simps simp flip: mask_eq_exp_minus_1)
-
-lemma bit_minus_2_iff [simp]:
-  \<open>bit (- 2) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n > 0\<close>
-  by (simp add: bit_minus_iff bit_1_iff)
-
-lemma not_one [simp]:
-  "NOT 1 = - 2"
-  by (simp add: bit_eq_iff bit_not_iff) (simp add: bit_1_iff)
-
-sublocale "and": semilattice_neutr \<open>(AND)\<close> \<open>- 1\<close>
-  by standard (rule bit_eqI, simp add: bit_and_iff)
-
-sublocale bit: boolean_algebra \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close>
-  rewrites \<open>bit.xor = (XOR)\<close>
-proof -
-  interpret bit: boolean_algebra \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close>
-    by standard (auto simp add: bit_and_iff bit_or_iff bit_not_iff intro: bit_eqI)
-  show \<open>boolean_algebra (AND) (OR) NOT 0 (- 1)\<close>
-    by standard
-  show \<open>boolean_algebra.xor (AND) (OR) NOT = (XOR)\<close>
-    by (rule ext, rule ext, rule bit_eqI)
-      (auto simp add: bit.xor_def bit_and_iff bit_or_iff bit_xor_iff bit_not_iff)
-qed
-
-lemma and_eq_not_not_or:
-  \<open>a AND b = NOT (NOT a OR NOT b)\<close>
-  by simp
-
-lemma or_eq_not_not_and:
-  \<open>a OR b = NOT (NOT a AND NOT b)\<close>
-  by simp
-
-lemma not_add_distrib:
-  \<open>NOT (a + b) = NOT a - b\<close>
-  by (simp add: not_eq_complement algebra_simps)
-
-lemma not_diff_distrib:
-  \<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 -
-  have \<open>NOT a + b = NOT a OR b\<close>
-    by (rule disjunctive_add) (auto simp add: bit_not_iff dest: that)
-  then have \<open>NOT (NOT a + b) = NOT (NOT a OR b)\<close>
-    by simp
-  then show ?thesis
-    by (simp add: not_add_distrib)
-qed
-
-lemma push_bit_minus:
-  \<open>push_bit n (- a) = - push_bit n a\<close>
-  by (simp add: push_bit_eq_mult)
-
-lemma take_bit_not_take_bit:
-  \<open>take_bit n (NOT (take_bit n a)) = take_bit n (NOT a)\<close>
-  by (auto simp add: bit_eq_iff bit_take_bit_iff bit_not_iff)
-
-lemma take_bit_not_iff:
-  "take_bit n (NOT a) = take_bit n (NOT b) \<longleftrightarrow> take_bit n a = take_bit n b"
-  apply (simp add: bit_eq_iff)
-  apply (simp add: bit_not_iff bit_take_bit_iff bit_exp_iff)
-  apply (use exp_eq_0_imp_not_bit in blast)
-  done
-
-lemma take_bit_not_eq_mask_diff:
-  \<open>take_bit n (NOT a) = mask n - take_bit n a\<close>
-proof -
-  have \<open>take_bit n (NOT a) = take_bit n (NOT (take_bit n a))\<close>
-    by (simp add: take_bit_not_take_bit)
-  also have \<open>\<dots> = mask n AND NOT (take_bit n a)\<close>
-    by (simp add: take_bit_eq_mask ac_simps)
-  also have \<open>\<dots> = mask n - take_bit n a\<close>
-    by (subst disjunctive_diff)
-      (auto simp add: bit_take_bit_iff bit_mask_iff exp_eq_0_imp_not_bit)
-  finally show ?thesis
-    by simp
-qed
-
-lemma mask_eq_take_bit_minus_one:
-  \<open>mask n = take_bit n (- 1)\<close>
-  by (simp add: bit_eq_iff bit_mask_iff bit_take_bit_iff conj_commute)
-
-lemma take_bit_minus_one_eq_mask:
-  \<open>take_bit n (- 1) = mask n\<close>
-  by (simp add: mask_eq_take_bit_minus_one)
-
-lemma minus_exp_eq_not_mask:
-  \<open>- (2 ^ n) = NOT (mask n)\<close>
-  by (rule bit_eqI) (simp add: bit_minus_iff bit_not_iff flip: mask_eq_exp_minus_1)
-
-lemma push_bit_minus_one_eq_not_mask:
-  \<open>push_bit n (- 1) = NOT (mask n)\<close>
-  by (simp add: push_bit_eq_mult minus_exp_eq_not_mask)
-
-lemma take_bit_not_mask_eq_0:
-  \<open>take_bit m (NOT (mask n)) = 0\<close> if \<open>n \<ge> m\<close>
-  by (rule bit_eqI) (use that in \<open>simp add: bit_take_bit_iff bit_not_iff bit_mask_iff\<close>)
-
-lemma take_bit_mask [simp]:
-  \<open>take_bit m (mask n) = mask (min m n)\<close>
-  by (simp add: mask_eq_take_bit_minus_one)
-
-definition set_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
-  where \<open>set_bit n a = a OR push_bit n 1\<close>
-
-definition unset_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
-  where \<open>unset_bit n a = a AND NOT (push_bit n 1)\<close>
-
-definition flip_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
-  where \<open>flip_bit n a = a XOR push_bit n 1\<close>
+lemmas set_bit_def = set_bit_eq_or
 
 lemma bit_set_bit_iff [bit_simps]:
   \<open>bit (set_bit m a) n \<longleftrightarrow> bit a n \<or> (m = n \<and> 2 ^ n \<noteq> 0)\<close>
   by (auto simp add: set_bit_def push_bit_of_1 bit_or_iff bit_exp_iff)
 
 lemma even_set_bit_iff:
   \<open>even (set_bit m a) \<longleftrightarrow> even a \<and> m \<noteq> 0\<close>
   using bit_set_bit_iff [of m a 0] by auto
 
-lemma bit_unset_bit_iff [bit_simps]:
-  \<open>bit (unset_bit m a) n \<longleftrightarrow> bit a n \<and> m \<noteq> n\<close>
-  by (auto simp add: unset_bit_def push_bit_of_1 bit_and_iff bit_not_iff bit_exp_iff exp_eq_0_imp_not_bit)
-
 lemma even_unset_bit_iff:
   \<open>even (unset_bit m a) \<longleftrightarrow> even a \<or> m = 0\<close>
   using bit_unset_bit_iff [of m a 0] by auto
+
+lemmas flip_bit_def = flip_bit_eq_xor
 
 lemma bit_flip_bit_iff [bit_simps]:
   \<open>bit (flip_bit m a) n \<longleftrightarrow> (m = n \<longleftrightarrow> \<not> bit a n) \<and> 2 ^ n \<noteq> 0\<close>
   by (auto simp add: flip_bit_def push_bit_of_1 bit_xor_iff bit_exp_iff exp_eq_0_imp_not_bit)
 

   by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_unset_bit_iff)
 
 lemma take_bit_flip_bit_eq:
   \<open>take_bit n (flip_bit m a) = (if n \<le> m then take_bit n a else flip_bit m (take_bit n a))\<close>
   by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_flip_bit_iff)
+
+
+end
+
+class ring_bit_operations = semiring_bit_operations + ring_parity +
+  fixes not :: \<open>'a \<Rightarrow> 'a\<close>  (\<open>NOT\<close>)
+  assumes bit_not_iff [bit_simps]: \<open>\<And>n. bit (NOT a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> \<not> bit a n\<close>
+  assumes minus_eq_not_minus_1: \<open>- a = NOT (a - 1)\<close>
+begin
+
+text \<open>
+  For the sake of code generation \<^const>\<open>not\<close> is specified as
+  definitional class operation.  Note that \<^const>\<open>not\<close> has no
+  sensible definition for unlimited but only positive bit strings
+  (type \<^typ>\<open>nat\<close>).
+\<close>
+
+lemma bits_minus_1_mod_2_eq [simp]:
+  \<open>(- 1) mod 2 = 1\<close>
+  by (simp add: mod_2_eq_odd)
+
+lemma not_eq_complement:
+  \<open>NOT a = - a - 1\<close>
+  using minus_eq_not_minus_1 [of \<open>a + 1\<close>] by simp
+
+lemma minus_eq_not_plus_1:
+  \<open>- a = NOT a + 1\<close>
+  using not_eq_complement [of a] by simp
+
+lemma bit_minus_iff [bit_simps]:
+  \<open>bit (- a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> \<not> bit (a - 1) n\<close>
+  by (simp add: minus_eq_not_minus_1 bit_not_iff)
+
+lemma even_not_iff [simp]:
+  "even (NOT a) \<longleftrightarrow> odd a"
+  using bit_not_iff [of a 0] by auto
+
+lemma bit_not_exp_iff [bit_simps]:
+  \<open>bit (NOT (2 ^ m)) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n \<noteq> m\<close>
+  by (auto simp add: bit_not_iff bit_exp_iff)
+
+lemma bit_minus_1_iff [simp]:
+  \<open>bit (- 1) n \<longleftrightarrow> 2 ^ n \<noteq> 0\<close>
+  by (simp add: bit_minus_iff)
+
+lemma bit_minus_exp_iff [bit_simps]:
+  \<open>bit (- (2 ^ m)) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n \<ge> m\<close>
+  by (auto simp add: bit_simps simp flip: mask_eq_exp_minus_1)
+
+lemma bit_minus_2_iff [simp]:
+  \<open>bit (- 2) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n > 0\<close>
+  by (simp add: bit_minus_iff bit_1_iff)
+
+lemma not_one [simp]:
+  "NOT 1 = - 2"
+  by (simp add: bit_eq_iff bit_not_iff) (simp add: bit_1_iff)
+
+sublocale "and": semilattice_neutr \<open>(AND)\<close> \<open>- 1\<close>
+  by standard (rule bit_eqI, simp add: bit_and_iff)
+
+sublocale bit: boolean_algebra \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close>
+  rewrites \<open>bit.xor = (XOR)\<close>
+proof -
+  interpret bit: boolean_algebra \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close>
+    by standard (auto simp add: bit_and_iff bit_or_iff bit_not_iff intro: bit_eqI)
+  show \<open>boolean_algebra (AND) (OR) NOT 0 (- 1)\<close>
+    by standard
+  show \<open>boolean_algebra.xor (AND) (OR) NOT = (XOR)\<close>
+    by (rule ext, rule ext, rule bit_eqI)
+      (auto simp add: bit.xor_def bit_and_iff bit_or_iff bit_xor_iff bit_not_iff)
+qed
+
+lemma and_eq_not_not_or:
+  \<open>a AND b = NOT (NOT a OR NOT b)\<close>
+  by simp
+
+lemma or_eq_not_not_and:
+  \<open>a OR b = NOT (NOT a AND NOT b)\<close>
+  by simp
+
+lemma not_add_distrib:
+  \<open>NOT (a + b) = NOT a - b\<close>
+  by (simp add: not_eq_complement algebra_simps)
+
+lemma not_diff_distrib:
+  \<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 -
+  have \<open>NOT a + b = NOT a OR b\<close>
+    by (rule disjunctive_add) (auto simp add: bit_not_iff dest: that)
+  then have \<open>NOT (NOT a + b) = NOT (NOT a OR b)\<close>
+    by simp
+  then show ?thesis
+    by (simp add: not_add_distrib)
+qed
+
+lemma push_bit_minus:
+  \<open>push_bit n (- a) = - push_bit n a\<close>
+  by (simp add: push_bit_eq_mult)
+
+lemma take_bit_not_take_bit:
+  \<open>take_bit n (NOT (take_bit n a)) = take_bit n (NOT a)\<close>
+  by (auto simp add: bit_eq_iff bit_take_bit_iff bit_not_iff)
+
+lemma take_bit_not_iff:
+  "take_bit n (NOT a) = take_bit n (NOT b) \<longleftrightarrow> take_bit n a = take_bit n b"
+  apply (simp add: bit_eq_iff)
+  apply (simp add: bit_not_iff bit_take_bit_iff bit_exp_iff)
+  apply (use exp_eq_0_imp_not_bit in blast)
+  done
+
+lemma take_bit_not_eq_mask_diff:
+  \<open>take_bit n (NOT a) = mask n - take_bit n a\<close>
+proof -
+  have \<open>take_bit n (NOT a) = take_bit n (NOT (take_bit n a))\<close>
+    by (simp add: take_bit_not_take_bit)
+  also have \<open>\<dots> = mask n AND NOT (take_bit n a)\<close>
+    by (simp add: take_bit_eq_mask ac_simps)
+  also have \<open>\<dots> = mask n - take_bit n a\<close>
+    by (subst disjunctive_diff)
+      (auto simp add: bit_take_bit_iff bit_mask_iff exp_eq_0_imp_not_bit)
+  finally show ?thesis
+    by simp
+qed
+
+lemma mask_eq_take_bit_minus_one:
+  \<open>mask n = take_bit n (- 1)\<close>
+  by (simp add: bit_eq_iff bit_mask_iff bit_take_bit_iff conj_commute)
+
+lemma take_bit_minus_one_eq_mask:
+  \<open>take_bit n (- 1) = mask n\<close>
+  by (simp add: mask_eq_take_bit_minus_one)
+
+lemma minus_exp_eq_not_mask:
+  \<open>- (2 ^ n) = NOT (mask n)\<close>
+  by (rule bit_eqI) (simp add: bit_minus_iff bit_not_iff flip: mask_eq_exp_minus_1)
+
+lemma push_bit_minus_one_eq_not_mask:
+  \<open>push_bit n (- 1) = NOT (mask n)\<close>
+  by (simp add: push_bit_eq_mult minus_exp_eq_not_mask)
+
+lemma take_bit_not_mask_eq_0:
+  \<open>take_bit m (NOT (mask n)) = 0\<close> if \<open>n \<ge> m\<close>
+  by (rule bit_eqI) (use that in \<open>simp add: bit_take_bit_iff bit_not_iff bit_mask_iff\<close>)
+
+lemma unset_bit_eq_and_not:
+  \<open>unset_bit n a = a AND NOT (push_bit n 1)\<close>
+  by (rule bit_eqI) (auto simp add: bit_simps)
+
+lemmas unset_bit_def = unset_bit_eq_and_not
 
 end
 
 
 subsection \<open>Instance \<^typ>\<open>int\<close>\<close>

   by (auto simp add: xor_int_def bit_or_int_iff bit_and_int_iff bit_not_int_iff)
 
 definition mask_int :: \<open>nat \<Rightarrow> int\<close>
   where \<open>mask n = (2 :: int) ^ n - 1\<close>
 
+definition set_bit_int :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
+  where \<open>set_bit n k = k OR push_bit n 1\<close> for k :: int
+
+definition unset_bit_int :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
+  where \<open>unset_bit n k = k AND NOT (push_bit n 1)\<close> for k :: int
+
+definition flip_bit_int :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
+  where \<open>flip_bit n k = k XOR push_bit n 1\<close> for k :: int
+
 instance proof
-  fix k l :: int and n :: nat
+  fix k l :: int and m n :: nat
   show \<open>- k = NOT (k - 1)\<close>
     by (simp add: not_int_def)
   show \<open>bit (k AND l) n \<longleftrightarrow> bit k n \<and> bit l n\<close>
     by (fact bit_and_int_iff)
   show \<open>bit (k OR l) n \<longleftrightarrow> bit k n \<or> bit l n\<close>
     by (fact bit_or_int_iff)
   show \<open>bit (k XOR l) n \<longleftrightarrow> bit k n \<noteq> bit l n\<close>
     by (fact bit_xor_int_iff)
-qed (simp_all add: bit_not_int_iff mask_int_def)
+  show \<open>bit (unset_bit m k) n \<longleftrightarrow> bit k n \<and> m \<noteq> n\<close>
+  proof -
+    have \<open>unset_bit m k = k AND NOT (push_bit m 1)\<close>
+      by (simp add: unset_bit_int_def)
+    also have \<open>NOT (push_bit m 1 :: int) = - (push_bit m 1 + 1)\<close>
+      by (simp add: not_int_def)
+    finally show ?thesis by (simp only: bit_simps bit_and_int_iff) (auto simp add: bit_simps)
+  qed
+qed (simp_all add: bit_not_int_iff mask_int_def set_bit_int_def flip_bit_int_def)
 
 end
 
 
 lemma mask_half_int:

   where \<open>m XOR n = nat (int m XOR int n)\<close> for m n :: nat
 
 definition mask_nat :: \<open>nat \<Rightarrow> nat\<close>
   where \<open>mask n = (2 :: nat) ^ n - 1\<close>
 
+definition set_bit_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
+  where \<open>set_bit m n = n OR push_bit m 1\<close> for m n :: nat
+
+definition unset_bit_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
+  where \<open>unset_bit m n = (if bit n m then n - push_bit m 1 else n)\<close> for m n :: nat
+
+definition flip_bit_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
+  where \<open>flip_bit m n = n XOR push_bit m 1\<close> for m n :: nat
+
 instance proof
   fix m n q :: nat
   show \<open>bit (m AND n) q \<longleftrightarrow> bit m q \<and> bit n q\<close>
     by (simp add: and_nat_def bit_simps)
   show \<open>bit (m OR n) q \<longleftrightarrow> bit m q \<or> bit n q\<close>
     by (simp add: or_nat_def bit_simps)
   show \<open>bit (m XOR n) q \<longleftrightarrow> bit m q \<noteq> bit n q\<close>
     by (simp add: xor_nat_def bit_simps)
-qed (simp add: mask_nat_def)
+  show \<open>bit (unset_bit m n) q \<longleftrightarrow> bit n q \<and> m \<noteq> q\<close>
+  proof (cases \<open>bit n m\<close>)
+    case False
+    then show ?thesis by (auto simp add: unset_bit_nat_def)
+  next
+    case True
+    have \<open>push_bit m (drop_bit m n) + take_bit m n = n\<close>
+      by (fact bits_ident)
+    also from \<open>bit n m\<close> have \<open>drop_bit m n = 2 * drop_bit (Suc m) n  + 1\<close>
+      by (simp add: drop_bit_Suc drop_bit_half even_drop_bit_iff_not_bit ac_simps)
+    finally have \<open>push_bit m (2 * drop_bit (Suc m) n) + take_bit m n + push_bit m 1 = n\<close>
+      by (simp only: push_bit_add ac_simps)
+    then have \<open>n - push_bit m 1 = push_bit m (2 * drop_bit (Suc m) n) + take_bit m n\<close>
+      by simp
+    then have \<open>n - push_bit m 1 = push_bit m (2 * drop_bit (Suc m) n) OR take_bit m n\<close>
+      by (simp add: or_nat_def bit_simps flip: disjunctive_add)
+    with \<open>bit n m\<close> show ?thesis
+      by (auto simp add: unset_bit_nat_def or_nat_def bit_simps)
+  qed
+qed (simp_all add: mask_nat_def set_bit_nat_def flip_bit_nat_def)
 
 end
 
 lemma and_nat_rec:
   \<open>m AND n = of_bool (odd m \<and> odd n) + 2 * ((m div 2) AND (n div 2))\<close> for m n :: nat

   is xor .
 
 lift_definition mask_integer :: \<open>nat \<Rightarrow> integer\<close>
   is mask .
 
+lift_definition set_bit_integer :: \<open>nat \<Rightarrow> integer \<Rightarrow> integer\<close>
+  is set_bit .
+
+lift_definition unset_bit_integer :: \<open>nat \<Rightarrow> integer \<Rightarrow> integer\<close>
+  is unset_bit .
+
+lift_definition flip_bit_integer :: \<open>nat \<Rightarrow> integer \<Rightarrow> integer\<close>
+  is flip_bit .
+
 instance by (standard; transfer)
   (simp_all add: minus_eq_not_minus_1 mask_eq_exp_minus_1
-    bit_not_iff bit_and_iff bit_or_iff bit_xor_iff)
+    bit_not_iff bit_and_iff bit_or_iff bit_xor_iff
+    set_bit_def bit_unset_bit_iff flip_bit_def)
 
 end
 
 lemma [code]:
   \<open>mask n = 2 ^ n - (1::integer)\<close>

   is xor .
 
 lift_definition mask_natural :: \<open>nat \<Rightarrow> natural\<close>
   is mask .
 
+lift_definition set_bit_natural :: \<open>nat \<Rightarrow> natural \<Rightarrow> natural\<close>
+  is set_bit .
+
+lift_definition unset_bit_natural :: \<open>nat \<Rightarrow> natural \<Rightarrow> natural\<close>
+  is unset_bit .
+
+lift_definition flip_bit_natural :: \<open>nat \<Rightarrow> natural \<Rightarrow> natural\<close>
+  is flip_bit .
+
 instance by (standard; transfer)
-  (simp_all add: mask_eq_exp_minus_1 bit_and_iff bit_or_iff bit_xor_iff)
+  (simp_all add: mask_eq_exp_minus_1
+    bit_and_iff bit_or_iff bit_xor_iff
+    set_bit_def bit_unset_bit_iff flip_bit_def)
 
 end
 
 lemma [code]:
   \<open>integer_of_natural (mask n) = mask n\<close>