merged

--- a/src/HOL/Bit_Operations.thy	Tue Aug 03 10:14:48 2021 +0200
+++ b/src/HOL/Bit_Operations.thy	Wed Aug 04 08:27:16 2021 +0200
@@ -610,27 +610,154 @@
 
 end
 
-class semiring_bit_shifts = semiring_bits +
-  fixes push_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
-  assumes push_bit_eq_mult: \<open>push_bit n a = a * 2 ^ n\<close>
-  fixes drop_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
-  assumes drop_bit_eq_div: \<open>drop_bit n a = a div 2 ^ n\<close>
-  fixes take_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
-  assumes take_bit_eq_mod: \<open>take_bit n a = a mod 2 ^ n\<close>
+lemma bit_not_int_iff':
+  \<open>bit (- k - 1) n \<longleftrightarrow> \<not> bit k n\<close>
+  for k :: int
+proof (induction n arbitrary: k)
+  case 0
+  show ?case
+    by simp
+next
+  case (Suc n)
+  have \<open>- k - 1 = - (k + 2) + 1\<close>
+    by simp
+  also have \<open>(- (k + 2) + 1) div 2 = - (k div 2) - 1\<close>
+  proof (cases \<open>even k\<close>)
+    case True
+    then have \<open>- k div 2 = - (k div 2)\<close>
+      by rule (simp flip: mult_minus_right)
+    with True show ?thesis
+      by simp
+  next
+    case False
+    have \<open>4 = 2 * (2::int)\<close>
+      by simp
+    also have \<open>2 * 2 div 2 = (2::int)\<close>
+      by (simp only: nonzero_mult_div_cancel_left)
+    finally have *: \<open>4 div 2 = (2::int)\<close> .
+    from False obtain l where k: \<open>k = 2 * l + 1\<close> ..
+    then have \<open>- k - 2 = 2 * - (l + 2) + 1\<close>
+      by simp
+    then have \<open>(- k - 2) div 2 + 1 = - (k div 2) - 1\<close>
+      by (simp flip: mult_minus_right add: *) (simp add: k)
+    with False show ?thesis
+      by simp
+  qed
+  finally have \<open>(- k - 1) div 2 = - (k div 2) - 1\<close> .
+  with Suc show ?case
+    by (simp add: bit_Suc)
+qed
+
+lemma bit_nat_iff [bit_simps]:
+  \<open>bit (nat k) n \<longleftrightarrow> k \<ge> 0 \<and> bit k n\<close>
+proof (cases \<open>k \<ge> 0\<close>)
+  case True
+  moreover define m where \<open>m = nat k\<close>
+  ultimately have \<open>k = int m\<close>
+    by simp
+  then show ?thesis
+    by (simp add: bit_simps)
+next
+  case False
+  then show ?thesis
+    by simp
+qed
+
+
+subsection \<open>Bit operations\<close>
+
+class semiring_bit_operations = semiring_bits +
+  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>
+    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>
+    and push_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
+    and drop_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
+    and take_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>
+    and push_bit_eq_mult: \<open>push_bit n a = a * 2 ^ n\<close>
+    and drop_bit_eq_div: \<open>drop_bit n a = a div 2 ^ n\<close>
+    and take_bit_eq_mod: \<open>take_bit n a = a mod 2 ^ n\<close>
 begin
 
 text \<open>
+  We want the bitwise operations to bind slightly weaker
+  than \<open>+\<close> and \<open>-\<close>.
+
   Logically, \<^const>\<open>push_bit\<close>,
   \<^const>\<open>drop_bit\<close> and \<^const>\<open>take_bit\<close> are just aliases; having them
   as separate operations makes proofs easier, otherwise proof automation
   would fiddle with concrete expressions \<^term>\<open>2 ^ n\<close> in a way obfuscating the basic
   algebraic relationships between those operations.
-  Having
-  them as definitional class operations
-  takes into account that specific instances of these can be implemented
+
+  For the sake of code generation operations 
+  are specified as definitional class operations,
+  taking into account that specific instances of these can be implemented
   differently wrt. code generation.
 \<close>
 
+sublocale "and": semilattice \<open>(AND)\<close>
+  by standard (auto simp add: bit_eq_iff bit_and_iff)
+
+sublocale or: semilattice_neutr \<open>(OR)\<close> 0
+  by standard (auto simp add: bit_eq_iff bit_or_iff)
+
+sublocale xor: comm_monoid \<open>(XOR)\<close> 0
+  by standard (auto simp add: bit_eq_iff bit_xor_iff)
+
+lemma even_and_iff:
+  \<open>even (a AND b) \<longleftrightarrow> even a \<or> even b\<close>
+  using bit_and_iff [of a b 0] by auto
+
+lemma even_or_iff:
+  \<open>even (a OR b) \<longleftrightarrow> even a \<and> even b\<close>
+  using bit_or_iff [of a b 0] by auto
+
+lemma even_xor_iff:
+  \<open>even (a XOR b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)\<close>
+  using bit_xor_iff [of a b 0] by auto
+
+lemma zero_and_eq [simp]:
+  \<open>0 AND a = 0\<close>
+  by (simp add: bit_eq_iff bit_and_iff)
+
+lemma and_zero_eq [simp]:
+  \<open>a AND 0 = 0\<close>
+  by (simp add: bit_eq_iff bit_and_iff)
+
+lemma one_and_eq:
+  \<open>1 AND a = a mod 2\<close>
+  by (simp add: bit_eq_iff bit_and_iff) (auto simp add: bit_1_iff)
+
+lemma and_one_eq:
+  \<open>a AND 1 = a mod 2\<close>
+  using one_and_eq [of a] by (simp add: ac_simps)
+
+lemma one_or_eq:
+  \<open>1 OR a = a + of_bool (even a)\<close>
+  by (simp add: bit_eq_iff bit_or_iff add.commute [of _ 1] even_bit_succ_iff) (auto simp add: bit_1_iff)
+
+lemma or_one_eq:
+  \<open>a OR 1 = a + of_bool (even a)\<close>
+  using one_or_eq [of a] by (simp add: ac_simps)
+
+lemma one_xor_eq:
+  \<open>1 XOR a = a + of_bool (even a) - of_bool (odd a)\<close>
+  by (simp add: bit_eq_iff bit_xor_iff add.commute [of _ 1] even_bit_succ_iff) (auto simp add: bit_1_iff odd_bit_iff_bit_pred elim: oddE)
+
+lemma xor_one_eq:
+  \<open>a XOR 1 = a + of_bool (even a) - of_bool (odd a)\<close>
+  using one_xor_eq [of a] by (simp add: ac_simps)
+
 lemma bit_iff_odd_drop_bit:
   \<open>bit a n \<longleftrightarrow> odd (drop_bit n a)\<close>
   by (simp add: bit_iff_odd drop_bit_eq_div)
@@ -893,558 +1020,6 @@
   \<open>drop_bit m (2 ^ n) = of_bool (m \<le> n \<and> 2 ^ n \<noteq> 0) * 2 ^ (n - m)\<close>
   by (rule bit_eqI) (auto simp add: bit_simps)
 
-end
-
-instantiation nat :: semiring_bit_shifts
-begin
-
-definition push_bit_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
-  where \<open>push_bit_nat n m = m * 2 ^ n\<close>
-
-definition drop_bit_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
-  where \<open>drop_bit_nat n m = m div 2 ^ n\<close>
-
-definition take_bit_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
-  where \<open>take_bit_nat n m = m mod 2 ^ n\<close>
-
-instance
-  by standard (simp_all add: push_bit_nat_def drop_bit_nat_def take_bit_nat_def)
-
-end
-
-context semiring_bit_shifts
-begin
-
-lemma push_bit_of_nat:
-  \<open>push_bit n (of_nat m) = of_nat (push_bit n m)\<close>
-  by (simp add: push_bit_eq_mult semiring_bit_shifts_class.push_bit_eq_mult)
-
-lemma of_nat_push_bit:
-  \<open>of_nat (push_bit m n) = push_bit m (of_nat n)\<close>
-  by (simp add: push_bit_eq_mult semiring_bit_shifts_class.push_bit_eq_mult)
-
-lemma take_bit_of_nat:
-  \<open>take_bit n (of_nat m) = of_nat (take_bit n m)\<close>
-  by (rule bit_eqI) (simp add: bit_take_bit_iff Bit_Operations.bit_take_bit_iff bit_of_nat_iff)
-
-lemma of_nat_take_bit:
-  \<open>of_nat (take_bit n m) = take_bit n (of_nat m)\<close>
-  by (rule bit_eqI) (simp add: bit_take_bit_iff Bit_Operations.bit_take_bit_iff bit_of_nat_iff)
-
-end
-
-instantiation int :: semiring_bit_shifts
-begin
-
-definition push_bit_int :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
-  where \<open>push_bit_int n k = k * 2 ^ n\<close>
-
-definition drop_bit_int :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
-  where \<open>drop_bit_int n k = k div 2 ^ n\<close>
-
-definition take_bit_int :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
-  where \<open>take_bit_int n k = k mod 2 ^ n\<close>
-
-instance
-  by standard (simp_all add: push_bit_int_def drop_bit_int_def take_bit_int_def)
-
-end
-
-lemma bit_push_bit_iff_nat:
-  \<open>bit (push_bit m q) n \<longleftrightarrow> m \<le> n \<and> bit q (n - m)\<close> for q :: nat
-  by (auto simp add: bit_push_bit_iff)
-
-lemma bit_push_bit_iff_int:
-  \<open>bit (push_bit m k) n \<longleftrightarrow> m \<le> n \<and> bit k (n - m)\<close> for k :: int
-  by (auto simp add: bit_push_bit_iff)
-
-lemma take_bit_nat_less_exp [simp]:
-  \<open>take_bit n m < 2 ^ n\<close> for n m ::nat 
-  by (simp add: take_bit_eq_mod)
-
-lemma take_bit_nonnegative [simp]:
-  \<open>take_bit n k \<ge> 0\<close> for k :: int
-  by (simp add: take_bit_eq_mod)
-
-lemma not_take_bit_negative [simp]:
-  \<open>\<not> take_bit n k < 0\<close> for k :: int
-  by (simp add: not_less)
-
-lemma take_bit_int_less_exp [simp]:
-  \<open>take_bit n k < 2 ^ n\<close> for k :: int
-  by (simp add: take_bit_eq_mod)
-
-lemma take_bit_nat_eq_self_iff:
-  \<open>take_bit n m = m \<longleftrightarrow> m < 2 ^ n\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
-  for n m :: nat
-proof
-  assume ?P
-  moreover note take_bit_nat_less_exp [of n m]
-  ultimately show ?Q
-    by simp
-next
-  assume ?Q
-  then show ?P
-    by (simp add: take_bit_eq_mod)
-qed
-
-lemma take_bit_nat_eq_self:
-  \<open>take_bit n m = m\<close> if \<open>m < 2 ^ n\<close> for m n :: nat
-  using that by (simp add: take_bit_nat_eq_self_iff)
-
-lemma take_bit_int_eq_self_iff:
-  \<open>take_bit n k = k \<longleftrightarrow> 0 \<le> k \<and> k < 2 ^ n\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
-  for k :: int
-proof
-  assume ?P
-  moreover note take_bit_int_less_exp [of n k] take_bit_nonnegative [of n k]
-  ultimately show ?Q
-    by simp
-next
-  assume ?Q
-  then show ?P
-    by (simp add: take_bit_eq_mod)
-qed
-
-lemma take_bit_int_eq_self:
-  \<open>take_bit n k = k\<close> if \<open>0 \<le> k\<close> \<open>k < 2 ^ n\<close> for k :: int
-  using that by (simp add: take_bit_int_eq_self_iff)
-
-lemma take_bit_nat_less_eq_self [simp]:
-  \<open>take_bit n m \<le> m\<close> for n m :: nat
-  by (simp add: take_bit_eq_mod)
-
-lemma take_bit_nat_less_self_iff:
-  \<open>take_bit n m < m \<longleftrightarrow> 2 ^ n \<le> m\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
-  for m n :: nat
-proof
-  assume ?P
-  then have \<open>take_bit n m \<noteq> m\<close>
-    by simp
-  then show \<open>?Q\<close>
-    by (simp add: take_bit_nat_eq_self_iff)
-next
-  have \<open>take_bit n m < 2 ^ n\<close>
-    by (fact take_bit_nat_less_exp)
-  also assume ?Q
-  finally show ?P .
-qed
-
-class unique_euclidean_semiring_with_bit_shifts =
-  unique_euclidean_semiring_with_nat + semiring_bit_shifts
-begin
-
-lemma take_bit_of_exp [simp]:
-  \<open>take_bit m (2 ^ n) = of_bool (n < m) * 2 ^ n\<close>
-  by (simp add: take_bit_eq_mod exp_mod_exp)
-
-lemma take_bit_of_2 [simp]:
-  \<open>take_bit n 2 = of_bool (2 \<le> n) * 2\<close>
-  using take_bit_of_exp [of n 1] by simp
-
-lemma take_bit_of_mask:
-  \<open>take_bit m (2 ^ n - 1) = 2 ^ min m n - 1\<close>
-  by (simp add: take_bit_eq_mod mask_mod_exp)
-
-lemma push_bit_eq_0_iff [simp]:
-  "push_bit n a = 0 \<longleftrightarrow> a = 0"
-  by (simp add: push_bit_eq_mult)
-
-lemma take_bit_add:
-  "take_bit n (take_bit n a + take_bit n b) = take_bit n (a + b)"
-  by (simp add: take_bit_eq_mod mod_simps)
-
-lemma take_bit_of_1_eq_0_iff [simp]:
-  "take_bit n 1 = 0 \<longleftrightarrow> n = 0"
-  by (simp add: take_bit_eq_mod)
-
-lemma take_bit_Suc_1 [simp]:
-  \<open>take_bit (Suc n) 1 = 1\<close>
-  by (simp add: take_bit_Suc)
-
-lemma take_bit_Suc_bit0 [simp]:
-  \<open>take_bit (Suc n) (numeral (Num.Bit0 k)) = take_bit n (numeral k) * 2\<close>
-  by (simp add: take_bit_Suc numeral_Bit0_div_2)
-
-lemma take_bit_Suc_bit1 [simp]:
-  \<open>take_bit (Suc n) (numeral (Num.Bit1 k)) = take_bit n (numeral k) * 2 + 1\<close>
-  by (simp add: take_bit_Suc numeral_Bit1_div_2 mod_2_eq_odd)
-
-lemma take_bit_numeral_1 [simp]:
-  \<open>take_bit (numeral l) 1 = 1\<close>
-  by (simp add: take_bit_rec [of \<open>numeral l\<close> 1])
-
-lemma take_bit_numeral_bit0 [simp]:
-  \<open>take_bit (numeral l) (numeral (Num.Bit0 k)) = take_bit (pred_numeral l) (numeral k) * 2\<close>
-  by (simp add: take_bit_rec numeral_Bit0_div_2)
-
-lemma take_bit_numeral_bit1 [simp]:
-  \<open>take_bit (numeral l) (numeral (Num.Bit1 k)) = take_bit (pred_numeral l) (numeral k) * 2 + 1\<close>
-  by (simp add: take_bit_rec numeral_Bit1_div_2 mod_2_eq_odd)
-
-lemma drop_bit_Suc_bit0 [simp]:
-  \<open>drop_bit (Suc n) (numeral (Num.Bit0 k)) = drop_bit n (numeral k)\<close>
-  by (simp add: drop_bit_Suc numeral_Bit0_div_2)
-
-lemma drop_bit_Suc_bit1 [simp]:
-  \<open>drop_bit (Suc n) (numeral (Num.Bit1 k)) = drop_bit n (numeral k)\<close>
-  by (simp add: drop_bit_Suc numeral_Bit1_div_2)
-
-lemma drop_bit_numeral_bit0 [simp]:
-  \<open>drop_bit (numeral l) (numeral (Num.Bit0 k)) = drop_bit (pred_numeral l) (numeral k)\<close>
-  by (simp add: drop_bit_rec numeral_Bit0_div_2)
-
-lemma drop_bit_numeral_bit1 [simp]:
-  \<open>drop_bit (numeral l) (numeral (Num.Bit1 k)) = drop_bit (pred_numeral l) (numeral k)\<close>
-  by (simp add: drop_bit_rec numeral_Bit1_div_2)
-
-lemma drop_bit_of_nat:
-  "drop_bit n (of_nat m) = of_nat (drop_bit n m)"
-  by (simp add: drop_bit_eq_div Bit_Operations.drop_bit_eq_div of_nat_div [of m "2 ^ n"])
-
-lemma bit_of_nat_iff_bit [bit_simps]:
-  \<open>bit (of_nat m) n \<longleftrightarrow> bit m n\<close>
-proof -
-  have \<open>even (m div 2 ^ n) \<longleftrightarrow> even (of_nat (m div 2 ^ n))\<close>
-    by simp
-  also have \<open>of_nat (m div 2 ^ n) = of_nat m div of_nat (2 ^ n)\<close>
-    by (simp add: of_nat_div)
-  finally show ?thesis
-    by (simp add: bit_iff_odd semiring_bits_class.bit_iff_odd)
-qed
-
-lemma of_nat_drop_bit:
-  \<open>of_nat (drop_bit m n) = drop_bit m (of_nat n)\<close>
-  by (simp add: drop_bit_eq_div semiring_bit_shifts_class.drop_bit_eq_div of_nat_div)
-
-lemma bit_push_bit_iff_of_nat_iff [bit_simps]:
-  \<open>bit (push_bit m (of_nat r)) n \<longleftrightarrow> m \<le> n \<and> bit (of_nat r) (n - m)\<close>
-  by (auto simp add: bit_push_bit_iff)
-
-lemma take_bit_sum:
-  "take_bit n a = (\<Sum>k = 0..<n. push_bit k (of_bool (bit a k)))"
-  for n :: nat
-proof (induction n arbitrary: a)
-  case 0
-  then show ?case
-    by simp
-next
-  case (Suc n)
-  have "(\<Sum>k = 0..<Suc n. push_bit k (of_bool (bit a k))) = 
-    of_bool (odd a) + (\<Sum>k = Suc 0..<Suc n. push_bit k (of_bool (bit a k)))"
-    by (simp add: sum.atLeast_Suc_lessThan ac_simps)
-  also have "(\<Sum>k = Suc 0..<Suc n. push_bit k (of_bool (bit a k)))
-    = (\<Sum>k = 0..<n. push_bit k (of_bool (bit (a div 2) k))) * 2"
-    by (simp only: sum.atLeast_Suc_lessThan_Suc_shift) (simp add: sum_distrib_right push_bit_double drop_bit_Suc bit_Suc)
-  finally show ?case
-    using Suc [of "a div 2"] by (simp add: ac_simps take_bit_Suc mod_2_eq_odd)
-qed
-
-end
-
-instance nat :: unique_euclidean_semiring_with_bit_shifts ..
-
-instance int :: unique_euclidean_semiring_with_bit_shifts ..
-
-lemma bit_numeral_int_iff [bit_simps]:
-  \<open>bit (numeral m :: int) n \<longleftrightarrow> bit (numeral m :: nat) n\<close>
-  using bit_of_nat_iff_bit [of \<open>numeral m\<close> n] by simp
-
-lemma bit_not_int_iff':
-  \<open>bit (- k - 1) n \<longleftrightarrow> \<not> bit k n\<close>
-  for k :: int
-proof (induction n arbitrary: k)
-  case 0
-  show ?case
-    by simp
-next
-  case (Suc n)
-  have \<open>- k - 1 = - (k + 2) + 1\<close>
-    by simp
-  also have \<open>(- (k + 2) + 1) div 2 = - (k div 2) - 1\<close>
-  proof (cases \<open>even k\<close>)
-    case True
-    then have \<open>- k div 2 = - (k div 2)\<close>
-      by rule (simp flip: mult_minus_right)
-    with True show ?thesis
-      by simp
-  next
-    case False
-    have \<open>4 = 2 * (2::int)\<close>
-      by simp
-    also have \<open>2 * 2 div 2 = (2::int)\<close>
-      by (simp only: nonzero_mult_div_cancel_left)
-    finally have *: \<open>4 div 2 = (2::int)\<close> .
-    from False obtain l where k: \<open>k = 2 * l + 1\<close> ..
-    then have \<open>- k - 2 = 2 * - (l + 2) + 1\<close>
-      by simp
-    then have \<open>(- k - 2) div 2 + 1 = - (k div 2) - 1\<close>
-      by (simp flip: mult_minus_right add: *) (simp add: k)
-    with False show ?thesis
-      by simp
-  qed
-  finally have \<open>(- k - 1) div 2 = - (k div 2) - 1\<close> .
-  with Suc show ?case
-    by (simp add: bit_Suc)
-qed
-
-lemma bit_minus_int_iff [bit_simps]:
-  \<open>bit (- k) n \<longleftrightarrow> \<not> bit (k - 1) n\<close>
-  for k :: int
-  using bit_not_int_iff' [of \<open>k - 1\<close>] by simp
-
-lemma bit_nat_iff [bit_simps]:
-  \<open>bit (nat k) n \<longleftrightarrow> k \<ge> 0 \<and> bit k n\<close>
-proof (cases \<open>k \<ge> 0\<close>)
-  case True
-  moreover define m where \<open>m = nat k\<close>
-  ultimately have \<open>k = int m\<close>
-    by simp
-  then show ?thesis
-    by (simp add: bit_simps)
-next
-  case False
-  then show ?thesis
-    by simp
-qed
-
-lemma bit_numeral_int_simps [simp]:
-  \<open>bit (1 :: int) (numeral n) \<longleftrightarrow> bit (0 :: int) (pred_numeral n)\<close>
-  \<open>bit (numeral (num.Bit0 w) :: int) (numeral n) \<longleftrightarrow> bit (numeral w :: int) (pred_numeral n)\<close>
-  \<open>bit (numeral (num.Bit1 w) :: int) (numeral n) \<longleftrightarrow> bit (numeral w :: int) (pred_numeral n)\<close>
-  \<open>bit (numeral (Num.BitM w) :: int) (numeral n) \<longleftrightarrow> \<not> bit (- numeral w :: int) (pred_numeral n)\<close>
-  \<open>bit (- numeral (num.Bit0 w) :: int) (numeral n) \<longleftrightarrow> bit (- numeral w :: int) (pred_numeral n)\<close>
-  \<open>bit (- numeral (num.Bit1 w) :: int) (numeral n) \<longleftrightarrow> \<not> bit (numeral w :: int) (pred_numeral n)\<close>
-  \<open>bit (- numeral (Num.BitM w) :: int) (numeral n) \<longleftrightarrow> bit (- (numeral w) :: int) (pred_numeral n)\<close>
-  by (simp_all add: bit_1_iff numeral_eq_Suc bit_Suc add_One sub_inc_One_eq bit_minus_int_iff)
-
-lemma bit_numeral_Bit0_Suc_iff [simp]:
-  \<open>bit (numeral (Num.Bit0 m) :: int) (Suc n) \<longleftrightarrow> bit (numeral m :: int) n\<close>
-  by (simp add: bit_Suc)
-
-lemma bit_numeral_Bit1_Suc_iff [simp]:
-  \<open>bit (numeral (Num.Bit1 m) :: int) (Suc n) \<longleftrightarrow> bit (numeral m :: int) n\<close>
-  by (simp add: bit_Suc)
-
-lemma push_bit_nat_eq:
-  \<open>push_bit n (nat k) = nat (push_bit n k)\<close>
-  by (cases \<open>k \<ge> 0\<close>) (simp_all add: push_bit_eq_mult nat_mult_distrib not_le mult_nonneg_nonpos2)
-
-lemma drop_bit_nat_eq:
-  \<open>drop_bit n (nat k) = nat (drop_bit n k)\<close>
-  apply (cases \<open>k \<ge> 0\<close>)
-   apply (simp_all add: drop_bit_eq_div nat_div_distrib nat_power_eq not_le)
-  apply (simp add: divide_int_def)
-  done
-
-lemma take_bit_nat_eq:
-  \<open>take_bit n (nat k) = nat (take_bit n k)\<close> if \<open>k \<ge> 0\<close>
-  using that by (simp add: take_bit_eq_mod nat_mod_distrib nat_power_eq)
-
-lemma nat_take_bit_eq:
-  \<open>nat (take_bit n k) = take_bit n (nat k)\<close>
-  if \<open>k \<ge> 0\<close>
-  using that by (simp add: take_bit_eq_mod nat_mod_distrib nat_power_eq)
-
-lemma not_exp_less_eq_0_int [simp]:
-  \<open>\<not> 2 ^ n \<le> (0::int)\<close>
-  by (simp add: power_le_zero_eq)
-
-lemma half_nonnegative_int_iff [simp]:
-  \<open>k div 2 \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
-proof (cases \<open>k \<ge> 0\<close>)
-  case True
-  then show ?thesis
-    by (auto simp add: divide_int_def sgn_1_pos)
-next
-  case False
-  then show ?thesis
-    by (auto simp add: divide_int_def not_le elim!: evenE)
-qed
-
-lemma half_negative_int_iff [simp]:
-  \<open>k div 2 < 0 \<longleftrightarrow> k < 0\<close> for k :: int
-  by (subst Not_eq_iff [symmetric]) (simp add: not_less)
-
-lemma push_bit_of_Suc_0 [simp]:
-  "push_bit n (Suc 0) = 2 ^ n"
-  using push_bit_of_1 [where ?'a = nat] by simp
-
-lemma take_bit_of_Suc_0 [simp]:
-  "take_bit n (Suc 0) = of_bool (0 < n)"
-  using take_bit_of_1 [where ?'a = nat] by simp
-
-lemma drop_bit_of_Suc_0 [simp]:
-  "drop_bit n (Suc 0) = of_bool (n = 0)"
-  using drop_bit_of_1 [where ?'a = nat] by simp
-
-lemma push_bit_minus_one:
-  "push_bit n (- 1 :: int) = - (2 ^ n)"
-  by (simp add: push_bit_eq_mult)
-
-lemma minus_1_div_exp_eq_int:
-  \<open>- 1 div (2 :: int) ^ n = - 1\<close>
-  by (induction n) (use div_exp_eq [symmetric, of \<open>- 1 :: int\<close> 1] in \<open>simp_all add: ac_simps\<close>)
-
-lemma drop_bit_minus_one [simp]:
-  \<open>drop_bit n (- 1 :: int) = - 1\<close>
-  by (simp add: drop_bit_eq_div minus_1_div_exp_eq_int)
-
-lemma take_bit_Suc_from_most:
-  \<open>take_bit (Suc n) k = 2 ^ n * of_bool (bit k n) + take_bit n k\<close> for k :: int
-  by (simp only: take_bit_eq_mod power_Suc2) (simp_all add: bit_iff_odd odd_iff_mod_2_eq_one zmod_zmult2_eq)
-
-lemma take_bit_minus:
-  \<open>take_bit n (- take_bit n k) = take_bit n (- k)\<close>
-    for k :: int
-  by (simp add: take_bit_eq_mod mod_minus_eq)
-
-lemma take_bit_diff:
-  \<open>take_bit n (take_bit n k - take_bit n l) = take_bit n (k - l)\<close>
-    for k l :: int
-  by (simp add: take_bit_eq_mod mod_diff_eq)
-
-lemma bit_imp_take_bit_positive:
-  \<open>0 < take_bit m k\<close> if \<open>n < m\<close> and \<open>bit k n\<close> for k :: int
-proof (rule ccontr)
-  assume \<open>\<not> 0 < take_bit m k\<close>
-  then have \<open>take_bit m k = 0\<close>
-    by (auto simp add: not_less intro: order_antisym)
-  then have \<open>bit (take_bit m k) n = bit 0 n\<close>
-    by simp
-  with that show False
-    by (simp add: bit_take_bit_iff)
-qed
-
-lemma take_bit_mult:
-  \<open>take_bit n (take_bit n k * take_bit n l) = take_bit n (k * l)\<close>
-  for k l :: int
-  by (simp add: take_bit_eq_mod mod_mult_eq)
-
-lemma (in ring_1) of_nat_nat_take_bit_eq [simp]:
-  \<open>of_nat (nat (take_bit n k)) = of_int (take_bit n k)\<close>
-  by simp
-
-lemma take_bit_minus_small_eq:
-  \<open>take_bit n (- k) = 2 ^ n - k\<close> if \<open>0 < k\<close> \<open>k \<le> 2 ^ n\<close> for k :: int
-proof -
-  define m where \<open>m = nat k\<close>
-  with that have \<open>k = int m\<close> and \<open>0 < m\<close> and \<open>m \<le> 2 ^ n\<close>
-    by simp_all
-  have \<open>(2 ^ n - m) mod 2 ^ n = 2 ^ n - m\<close>
-    using \<open>0 < m\<close> by simp
-  then have \<open>int ((2 ^ n - m) mod 2 ^ n) = int (2 ^ n - m)\<close>
-    by simp
-  then have \<open>(2 ^ n - int m) mod 2 ^ n = 2 ^ n - int m\<close>
-    using \<open>m \<le> 2 ^ n\<close> by (simp only: of_nat_mod of_nat_diff) simp
-  with \<open>k = int m\<close> have \<open>(2 ^ n - k) mod 2 ^ n = 2 ^ n - k\<close>
-    by simp
-  then show ?thesis
-    by (simp add: take_bit_eq_mod)
-qed
-
-lemma drop_bit_push_bit_int:
-  \<open>drop_bit m (push_bit n k) = drop_bit (m - n) (push_bit (n - m) k)\<close> for k :: int
-  by (cases \<open>m \<le> n\<close>) (auto simp add: mult.left_commute [of _ \<open>2 ^ n\<close>] mult.commute [of _ \<open>2 ^ n\<close>] mult.assoc
-    mult.commute [of k] drop_bit_eq_div push_bit_eq_mult not_le power_add dest!: le_Suc_ex less_imp_Suc_add)
-
-lemma push_bit_nonnegative_int_iff [simp]:
-  \<open>push_bit n k \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
-  by (simp add: push_bit_eq_mult zero_le_mult_iff)
-
-lemma push_bit_negative_int_iff [simp]:
-  \<open>push_bit n k < 0 \<longleftrightarrow> k < 0\<close> for k :: int
-  by (subst Not_eq_iff [symmetric]) (simp add: not_less)
-
-lemma drop_bit_nonnegative_int_iff [simp]:
-  \<open>drop_bit n k \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
-  by (induction n) (simp_all add: drop_bit_Suc drop_bit_half)
-
-lemma drop_bit_negative_int_iff [simp]:
-  \<open>drop_bit n k < 0 \<longleftrightarrow> k < 0\<close> for k :: int
-  by (subst Not_eq_iff [symmetric]) (simp add: not_less)
-
-
-subsection \<open>Bit operations\<close>
-
-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>
-    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>.
-  For the sake of code generation
-  the operations \<^const>\<open>and\<close>, \<^const>\<open>or\<close> and \<^const>\<open>xor\<close>
-  are specified as definitional class operations.
-\<close>
-
-sublocale "and": semilattice \<open>(AND)\<close>
-  by standard (auto simp add: bit_eq_iff bit_and_iff)
-
-sublocale or: semilattice_neutr \<open>(OR)\<close> 0
-  by standard (auto simp add: bit_eq_iff bit_or_iff)
-
-sublocale xor: comm_monoid \<open>(XOR)\<close> 0
-  by standard (auto simp add: bit_eq_iff bit_xor_iff)
-
-lemma even_and_iff:
-  \<open>even (a AND b) \<longleftrightarrow> even a \<or> even b\<close>
-  using bit_and_iff [of a b 0] by auto
-
-lemma even_or_iff:
-  \<open>even (a OR b) \<longleftrightarrow> even a \<and> even b\<close>
-  using bit_or_iff [of a b 0] by auto
-
-lemma even_xor_iff:
-  \<open>even (a XOR b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)\<close>
-  using bit_xor_iff [of a b 0] by auto
-
-lemma zero_and_eq [simp]:
-  \<open>0 AND a = 0\<close>
-  by (simp add: bit_eq_iff bit_and_iff)
-
-lemma and_zero_eq [simp]:
-  \<open>a AND 0 = 0\<close>
-  by (simp add: bit_eq_iff bit_and_iff)
-
-lemma one_and_eq:
-  \<open>1 AND a = a mod 2\<close>
-  by (simp add: bit_eq_iff bit_and_iff) (auto simp add: bit_1_iff)
-
-lemma and_one_eq:
-  \<open>a AND 1 = a mod 2\<close>
-  using one_and_eq [of a] by (simp add: ac_simps)
-
-lemma one_or_eq:
-  \<open>1 OR a = a + of_bool (even a)\<close>
-  by (simp add: bit_eq_iff bit_or_iff add.commute [of _ 1] even_bit_succ_iff) (auto simp add: bit_1_iff)
-
-lemma or_one_eq:
-  \<open>a OR 1 = a + of_bool (even a)\<close>
-  using one_or_eq [of a] by (simp add: ac_simps)
-
-lemma one_xor_eq:
-  \<open>1 XOR a = a + of_bool (even a) - of_bool (odd a)\<close>
-  by (simp add: bit_eq_iff bit_xor_iff add.commute [of _ 1] even_bit_succ_iff) (auto simp add: bit_1_iff odd_bit_iff_bit_pred elim: oddE)
-
-lemma xor_one_eq:
-  \<open>a XOR 1 = a + of_bool (even a) - of_bool (odd a)\<close>
-  using one_xor_eq [of a] by (simp add: ac_simps)
-
 lemma take_bit_and [simp]:
   \<open>take_bit n (a AND b) = take_bit n a AND take_bit n b\<close>
   by (auto simp add: bit_eq_iff bit_take_bit_iff bit_and_iff)
@@ -1693,7 +1268,6 @@
   \<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 +
@@ -1780,7 +1354,7 @@
   \<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:
+lemma 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>
@@ -1875,79 +1449,6 @@
 
 subsection \<open>Instance \<^typ>\<open>int\<close>\<close>
 
-lemma int_bit_bound:
-  fixes k :: int
-  obtains n where \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m \<longleftrightarrow> bit k n\<close>
-    and \<open>n > 0 \<Longrightarrow> bit k (n - 1) \<noteq> bit k n\<close>
-proof -
-  obtain q where *: \<open>\<And>m. q \<le> m \<Longrightarrow> bit k m \<longleftrightarrow> bit k q\<close>
-  proof (cases \<open>k \<ge> 0\<close>)
-    case True
-    moreover from power_gt_expt [of 2 \<open>nat k\<close>]
-    have \<open>nat k < 2 ^ nat k\<close>
-      by simp
-    then have \<open>int (nat k) < int (2 ^ nat k)\<close>
-      by (simp only: of_nat_less_iff)
-    ultimately have *: \<open>k div 2 ^ nat k = 0\<close>
-      by simp
-    show thesis
-    proof (rule that [of \<open>nat k\<close>])
-      fix m
-      assume \<open>nat k \<le> m\<close>
-      then show \<open>bit k m \<longleftrightarrow> bit k (nat k)\<close>
-        by (auto simp add: * bit_iff_odd power_add zdiv_zmult2_eq dest!: le_Suc_ex)
-    qed
-  next
-    case False
-    moreover from power_gt_expt [of 2 \<open>nat (- k)\<close>]
-    have \<open>nat (- k) < 2 ^ nat (- k)\<close>
-      by simp
-    then have \<open>int (nat (- k)) < int (2 ^ nat (- k))\<close>
-      by (simp only: of_nat_less_iff)
-    ultimately have \<open>- k div - (2 ^ nat (- k)) = - 1\<close>
-      by (subst div_pos_neg_trivial) simp_all
-    then have *: \<open>k div 2 ^ nat (- k) = - 1\<close>
-      by simp
-    show thesis
-    proof (rule that [of \<open>nat (- k)\<close>])
-      fix m
-      assume \<open>nat (- k) \<le> m\<close>
-      then show \<open>bit k m \<longleftrightarrow> bit k (nat (- k))\<close>
-        by (auto simp add: * bit_iff_odd power_add zdiv_zmult2_eq minus_1_div_exp_eq_int dest!: le_Suc_ex)
-    qed
-  qed
-  show thesis
-  proof (cases \<open>\<forall>m. bit k m \<longleftrightarrow> bit k q\<close>)
-    case True
-    then have \<open>bit k 0 \<longleftrightarrow> bit k q\<close>
-      by blast
-    with True that [of 0] show thesis
-      by simp
-  next
-    case False
-    then obtain r where **: \<open>bit k r \<noteq> bit k q\<close>
-      by blast
-    have \<open>r < q\<close>
-      by (rule ccontr) (use * [of r] ** in simp)
-    define N where \<open>N = {n. n < q \<and> bit k n \<noteq> bit k q}\<close>
-    moreover have \<open>finite N\<close> \<open>r \<in> N\<close>
-      using ** N_def \<open>r < q\<close> by auto
-    moreover define n where \<open>n = Suc (Max N)\<close>
-    ultimately have \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m \<longleftrightarrow> bit k n\<close>
-      apply auto
-         apply (metis (full_types, lifting) "*" Max_ge_iff Suc_n_not_le_n \<open>finite N\<close> all_not_in_conv mem_Collect_eq not_le)
-        apply (metis "*" Max_ge Suc_n_not_le_n \<open>finite N\<close> linorder_not_less mem_Collect_eq)
-        apply (metis "*" Max_ge Suc_n_not_le_n \<open>finite N\<close> linorder_not_less mem_Collect_eq)
-      apply (metis (full_types, lifting) "*" Max_ge_iff Suc_n_not_le_n \<open>finite N\<close> all_not_in_conv mem_Collect_eq not_le)
-      done
-    have \<open>bit k (Max N) \<noteq> bit k n\<close>
-      by (metis (mono_tags, lifting) "*" Max_in N_def \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m = bit k n\<close> \<open>finite N\<close> \<open>r \<in> N\<close> empty_iff le_cases mem_Collect_eq)
-    show thesis apply (rule that [of n])
-      using \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m = bit k n\<close> apply blast
-      using \<open>bit k (Max N) \<noteq> bit k n\<close> n_def by auto
-  qed
-qed
-
 instantiation int :: ring_bit_operations
 begin
 
@@ -2083,6 +1584,15 @@
 definition mask_int :: \<open>nat \<Rightarrow> int\<close>
   where \<open>mask n = (2 :: int) ^ n - 1\<close>
 
+definition push_bit_int :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
+  where \<open>push_bit_int n k = k * 2 ^ n\<close>
+
+definition drop_bit_int :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
+  where \<open>drop_bit_int n k = k div 2 ^ n\<close>
+
+definition take_bit_int :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
+  where \<open>take_bit_int n k = k mod 2 ^ n\<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
 
@@ -2108,12 +1618,48 @@
       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)
+    finally show ?thesis by (simp only: bit_simps bit_and_int_iff)
+      (auto simp add: bit_simps bit_not_int_iff' push_bit_int_def)
   qed
-qed (simp_all add: bit_not_int_iff mask_int_def set_bit_int_def flip_bit_int_def)
+qed (simp_all add: bit_not_int_iff mask_int_def set_bit_int_def flip_bit_int_def
+  push_bit_int_def drop_bit_int_def take_bit_int_def)
 
 end
 
+lemma bit_push_bit_iff_int:
+  \<open>bit (push_bit m k) n \<longleftrightarrow> m \<le> n \<and> bit k (n - m)\<close> for k :: int
+  by (auto simp add: bit_push_bit_iff)
+
+lemma take_bit_nonnegative [simp]:
+  \<open>take_bit n k \<ge> 0\<close> for k :: int
+  by (simp add: take_bit_eq_mod)
+
+lemma not_take_bit_negative [simp]:
+  \<open>\<not> take_bit n k < 0\<close> for k :: int
+  by (simp add: not_less)
+
+lemma take_bit_int_less_exp [simp]:
+  \<open>take_bit n k < 2 ^ n\<close> for k :: int
+  by (simp add: take_bit_eq_mod)
+
+lemma take_bit_int_eq_self_iff:
+  \<open>take_bit n k = k \<longleftrightarrow> 0 \<le> k \<and> k < 2 ^ n\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+  for k :: int
+proof
+  assume ?P
+  moreover note take_bit_int_less_exp [of n k] take_bit_nonnegative [of n k]
+  ultimately show ?Q
+    by simp
+next
+  assume ?Q
+  then show ?P
+    by (simp add: take_bit_eq_mod)
+qed
+
+lemma take_bit_int_eq_self:
+  \<open>take_bit n k = k\<close> if \<open>0 \<le> k\<close> \<open>k < 2 ^ n\<close> for k :: int
+  using that by (simp add: take_bit_int_eq_self_iff)
+
 lemma mask_half_int:
   \<open>mask n div 2 = (mask (n - 1) :: int)\<close>
   by (cases n) (simp_all add: mask_eq_exp_minus_1 algebra_simps)
@@ -2183,7 +1729,7 @@
   case (odd k)
   from odd.IH [of \<open>l div 2\<close>] odd.hyps odd.prems
   show ?case
-    by (simp add: and_int_rec [of _ l])
+    by (simp add: and_int_rec [of _ l]) linarith
 qed
 
 lemma or_nonnegative_int_iff [simp]:
@@ -2208,7 +1754,7 @@
   case (even k)
   from even.IH [of \<open>l div 2\<close>] even.hyps even.prems
   show ?case
-    by (simp add: or_int_rec [of _ l])
+    by (simp add: or_int_rec [of _ l]) linarith
 next
   case (odd k)
   from odd.IH [of \<open>l div 2\<close>] odd.hyps odd.prems
@@ -2335,6 +1881,92 @@
     by (auto simp add: and_int_rec [of _ y] or_int_rec [of _ y] elim: oddE)
 qed
 
+lemma push_bit_minus_one:
+  "push_bit n (- 1 :: int) = - (2 ^ n)"
+  by (simp add: push_bit_eq_mult)
+
+lemma minus_1_div_exp_eq_int:
+  \<open>- 1 div (2 :: int) ^ n = - 1\<close>
+  by (induction n) (use div_exp_eq [symmetric, of \<open>- 1 :: int\<close> 1] in \<open>simp_all add: ac_simps\<close>)
+
+lemma drop_bit_minus_one [simp]:
+  \<open>drop_bit n (- 1 :: int) = - 1\<close>
+  by (simp add: drop_bit_eq_div minus_1_div_exp_eq_int)
+
+lemma take_bit_Suc_from_most:
+  \<open>take_bit (Suc n) k = 2 ^ n * of_bool (bit k n) + take_bit n k\<close> for k :: int
+  by (simp only: take_bit_eq_mod power_Suc2) (simp_all add: bit_iff_odd odd_iff_mod_2_eq_one zmod_zmult2_eq)
+
+lemma take_bit_minus:
+  \<open>take_bit n (- take_bit n k) = take_bit n (- k)\<close>
+    for k :: int
+  by (simp add: take_bit_eq_mod mod_minus_eq)
+
+lemma take_bit_diff:
+  \<open>take_bit n (take_bit n k - take_bit n l) = take_bit n (k - l)\<close>
+    for k l :: int
+  by (simp add: take_bit_eq_mod mod_diff_eq)
+
+lemma bit_imp_take_bit_positive:
+  \<open>0 < take_bit m k\<close> if \<open>n < m\<close> and \<open>bit k n\<close> for k :: int
+proof (rule ccontr)
+  assume \<open>\<not> 0 < take_bit m k\<close>
+  then have \<open>take_bit m k = 0\<close>
+    by (auto simp add: not_less intro: order_antisym)
+  then have \<open>bit (take_bit m k) n = bit 0 n\<close>
+    by simp
+  with that show False
+    by (simp add: bit_take_bit_iff)
+qed
+
+lemma take_bit_mult:
+  \<open>take_bit n (take_bit n k * take_bit n l) = take_bit n (k * l)\<close>
+  for k l :: int
+  by (simp add: take_bit_eq_mod mod_mult_eq)
+
+lemma (in ring_1) of_nat_nat_take_bit_eq [simp]:
+  \<open>of_nat (nat (take_bit n k)) = of_int (take_bit n k)\<close>
+  by simp
+
+lemma take_bit_minus_small_eq:
+  \<open>take_bit n (- k) = 2 ^ n - k\<close> if \<open>0 < k\<close> \<open>k \<le> 2 ^ n\<close> for k :: int
+proof -
+  define m where \<open>m = nat k\<close>
+  with that have \<open>k = int m\<close> and \<open>0 < m\<close> and \<open>m \<le> 2 ^ n\<close>
+    by simp_all
+  have \<open>(2 ^ n - m) mod 2 ^ n = 2 ^ n - m\<close>
+    using \<open>0 < m\<close> by simp
+  then have \<open>int ((2 ^ n - m) mod 2 ^ n) = int (2 ^ n - m)\<close>
+    by simp
+  then have \<open>(2 ^ n - int m) mod 2 ^ n = 2 ^ n - int m\<close>
+    using \<open>m \<le> 2 ^ n\<close> by (simp only: of_nat_mod of_nat_diff) simp
+  with \<open>k = int m\<close> have \<open>(2 ^ n - k) mod 2 ^ n = 2 ^ n - k\<close>
+    by simp
+  then show ?thesis
+    by (simp add: take_bit_eq_mod)
+qed
+
+lemma drop_bit_push_bit_int:
+  \<open>drop_bit m (push_bit n k) = drop_bit (m - n) (push_bit (n - m) k)\<close> for k :: int
+  by (cases \<open>m \<le> n\<close>) (auto simp add: mult.left_commute [of _ \<open>2 ^ n\<close>] mult.commute [of _ \<open>2 ^ n\<close>] mult.assoc
+    mult.commute [of k] drop_bit_eq_div push_bit_eq_mult not_le power_add dest!: le_Suc_ex less_imp_Suc_add)
+
+lemma push_bit_nonnegative_int_iff [simp]:
+  \<open>push_bit n k \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
+  by (simp add: push_bit_eq_mult zero_le_mult_iff power_le_zero_eq)
+
+lemma push_bit_negative_int_iff [simp]:
+  \<open>push_bit n k < 0 \<longleftrightarrow> k < 0\<close> for k :: int
+  by (subst Not_eq_iff [symmetric]) (simp add: not_less)
+
+lemma drop_bit_nonnegative_int_iff [simp]:
+  \<open>drop_bit n k \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
+  by (induction n) (auto simp add: drop_bit_Suc drop_bit_half)
+
+lemma drop_bit_negative_int_iff [simp]:
+  \<open>drop_bit n k < 0 \<longleftrightarrow> k < 0\<close> for k :: int
+  by (subst Not_eq_iff [symmetric]) (simp add: not_less)
+
 lemma set_bit_nonnegative_int_iff [simp]:
   \<open>set_bit n k \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
   by (simp add: set_bit_def)
@@ -2413,13 +2045,311 @@
   qed
 qed
 
+lemma and_int_unfold [code]:
+  \<open>k AND l = (if k = 0 \<or> l = 0 then 0 else if k = - 1 then l else if l = - 1 then k
+    else (k mod 2) * (l mod 2) + 2 * ((k div 2) AND (l div 2)))\<close> for k l :: int
+  by (auto simp add: and_int_rec [of k l] zmult_eq_1_iff elim: oddE)
+
+lemma or_int_unfold [code]:
+  \<open>k OR l = (if k = - 1 \<or> l = - 1 then - 1 else if k = 0 then l else if l = 0 then k
+    else max (k mod 2) (l mod 2) + 2 * ((k div 2) OR (l div 2)))\<close> for k l :: int
+  by (auto simp add: or_int_rec [of k l] elim: oddE)
+
+lemma xor_int_unfold [code]:
+  \<open>k XOR l = (if k = - 1 then NOT l else if l = - 1 then NOT k else if k = 0 then l else if l = 0 then k
+    else \<bar>k mod 2 - l mod 2\<bar> + 2 * ((k div 2) XOR (l div 2)))\<close> for k l :: int
+  by (auto simp add: xor_int_rec [of k l] not_int_def elim!: oddE)
+
+
+subsection \<open>Instance \<^typ>\<open>nat\<close>\<close>
+
+instantiation nat :: semiring_bit_operations
+begin
+
+definition and_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
+  where \<open>m AND n = nat (int m AND int n)\<close> for m n :: nat
+
+definition or_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
+  where \<open>m OR n = nat (int m OR int n)\<close> for m n :: nat
+
+definition xor_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
+  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 push_bit_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
+  where \<open>push_bit_nat n m = m * 2 ^ n\<close>
+
+definition drop_bit_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
+  where \<open>drop_bit_nat n m = m div 2 ^ n\<close>
+
+definition take_bit_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
+  where \<open>take_bit_nat n m = m mod 2 ^ n\<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 = nat (unset_bit m (int 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)
+  show \<open>bit (unset_bit m n) q \<longleftrightarrow> bit n q \<and> m \<noteq> q\<close>
+    by (simp add: unset_bit_nat_def bit_simps)
+qed (simp_all add: mask_nat_def set_bit_nat_def flip_bit_nat_def push_bit_nat_def drop_bit_nat_def take_bit_nat_def)
+
+end
+
+lemma take_bit_nat_less_exp [simp]:
+  \<open>take_bit n m < 2 ^ n\<close> for n m ::nat 
+  by (simp add: take_bit_eq_mod)
+
+lemma take_bit_nat_eq_self_iff:
+  \<open>take_bit n m = m \<longleftrightarrow> m < 2 ^ n\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+  for n m :: nat
+proof
+  assume ?P
+  moreover note take_bit_nat_less_exp [of n m]
+  ultimately show ?Q
+    by simp
+next
+  assume ?Q
+  then show ?P
+    by (simp add: take_bit_eq_mod)
+qed
+
+lemma take_bit_nat_eq_self:
+  \<open>take_bit n m = m\<close> if \<open>m < 2 ^ n\<close> for m n :: nat
+  using that by (simp add: take_bit_nat_eq_self_iff)
+
+lemma take_bit_nat_less_eq_self [simp]:
+  \<open>take_bit n m \<le> m\<close> for n m :: nat
+  by (simp add: take_bit_eq_mod)
+
+lemma take_bit_nat_less_self_iff:
+  \<open>take_bit n m < m \<longleftrightarrow> 2 ^ n \<le> m\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+  for m n :: nat
+proof
+  assume ?P
+  then have \<open>take_bit n m \<noteq> m\<close>
+    by simp
+  then show \<open>?Q\<close>
+    by (simp add: take_bit_nat_eq_self_iff)
+next
+  have \<open>take_bit n m < 2 ^ n\<close>
+    by (fact take_bit_nat_less_exp)
+  also assume ?Q
+  finally show ?P .
+qed
+
+lemma bit_push_bit_iff_nat:
+  \<open>bit (push_bit m q) n \<longleftrightarrow> m \<le> n \<and> bit q (n - m)\<close> for q :: nat
+  by (auto simp add: bit_push_bit_iff)
+
+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
+  apply (simp add: and_nat_def and_int_rec [of \<open>int m\<close> \<open>int n\<close>] zdiv_int nat_add_distrib nat_mult_distrib)
+  apply (subst nat_add_distrib)
+    apply auto
+  done
+
+lemma or_nat_rec:
+  \<open>m OR n = of_bool (odd m \<or> odd n) + 2 * ((m div 2) OR (n div 2))\<close> for m n :: nat
+  apply (simp add: or_nat_def or_int_rec [of \<open>int m\<close> \<open>int n\<close>] zdiv_int nat_add_distrib nat_mult_distrib)
+  apply (subst nat_add_distrib)
+    apply auto
+  done
+
+lemma xor_nat_rec:
+  \<open>m XOR n = of_bool (odd m \<noteq> odd n) + 2 * ((m div 2) XOR (n div 2))\<close> for m n :: nat
+  apply (simp add: xor_nat_def xor_int_rec [of \<open>int m\<close> \<open>int n\<close>] zdiv_int nat_add_distrib nat_mult_distrib)
+  apply (subst nat_add_distrib)
+    apply auto
+  done
+
+lemma Suc_0_and_eq [simp]:
+  \<open>Suc 0 AND n = n mod 2\<close>
+  using one_and_eq [of n] by simp
+
+lemma and_Suc_0_eq [simp]:
+  \<open>n AND Suc 0 = n mod 2\<close>
+  using and_one_eq [of n] by simp
+
+lemma Suc_0_or_eq:
+  \<open>Suc 0 OR n = n + of_bool (even n)\<close>
+  using one_or_eq [of n] by simp
+
+lemma or_Suc_0_eq:
+  \<open>n OR Suc 0 = n + of_bool (even n)\<close>
+  using or_one_eq [of n] by simp
+
+lemma Suc_0_xor_eq:
+  \<open>Suc 0 XOR n = n + of_bool (even n) - of_bool (odd n)\<close>
+  using one_xor_eq [of n] by simp
+
+lemma xor_Suc_0_eq:
+  \<open>n XOR Suc 0 = n + of_bool (even n) - of_bool (odd n)\<close>
+  using xor_one_eq [of n] by simp
+
+lemma and_nat_unfold [code]:
+  \<open>m AND n = (if m = 0 \<or> n = 0 then 0 else (m mod 2) * (n mod 2) + 2 * ((m div 2) AND (n div 2)))\<close>
+    for m n :: nat
+  by (auto simp add: and_nat_rec [of m n] elim: oddE)
+
+lemma or_nat_unfold [code]:
+  \<open>m OR n = (if m = 0 then n else if n = 0 then m
+    else max (m mod 2) (n mod 2) + 2 * ((m div 2) OR (n div 2)))\<close> for m n :: nat
+  by (auto simp add: or_nat_rec [of m n] elim: oddE)
+
+lemma xor_nat_unfold [code]:
+  \<open>m XOR n = (if m = 0 then n else if n = 0 then m
+    else (m mod 2 + n mod 2) mod 2 + 2 * ((m div 2) XOR (n div 2)))\<close> for m n :: nat
+  by (auto simp add: xor_nat_rec [of m n] elim!: oddE)
+
+lemma [code]:
+  \<open>unset_bit 0 m = 2 * (m div 2)\<close>
+  \<open>unset_bit (Suc n) m = m mod 2 + 2 * unset_bit n (m div 2)\<close>
+  by (simp_all add: unset_bit_Suc)
+  
+
+subsection \<open>Common algebraic structure\<close>
+
+class unique_euclidean_semiring_with_bit_operations =
+  unique_euclidean_semiring_with_nat + semiring_bit_operations
+begin
+
+lemma take_bit_of_exp [simp]:
+  \<open>take_bit m (2 ^ n) = of_bool (n < m) * 2 ^ n\<close>
+  by (simp add: take_bit_eq_mod exp_mod_exp)
+
+lemma take_bit_of_2 [simp]:
+  \<open>take_bit n 2 = of_bool (2 \<le> n) * 2\<close>
+  using take_bit_of_exp [of n 1] by simp
+
+lemma take_bit_of_mask:
+  \<open>take_bit m (2 ^ n - 1) = 2 ^ min m n - 1\<close>
+  by (simp add: take_bit_eq_mod mask_mod_exp)
+
+lemma push_bit_eq_0_iff [simp]:
+  "push_bit n a = 0 \<longleftrightarrow> a = 0"
+  by (simp add: push_bit_eq_mult)
+
+lemma take_bit_add:
+  "take_bit n (take_bit n a + take_bit n b) = take_bit n (a + b)"
+  by (simp add: take_bit_eq_mod mod_simps)
+
+lemma take_bit_of_1_eq_0_iff [simp]:
+  "take_bit n 1 = 0 \<longleftrightarrow> n = 0"
+  by (simp add: take_bit_eq_mod)
+
+lemma take_bit_Suc_1 [simp]:
+  \<open>take_bit (Suc n) 1 = 1\<close>
+  by (simp add: take_bit_Suc)
+
+lemma take_bit_Suc_bit0 [simp]:
+  \<open>take_bit (Suc n) (numeral (Num.Bit0 k)) = take_bit n (numeral k) * 2\<close>
+  by (simp add: take_bit_Suc numeral_Bit0_div_2)
+
+lemma take_bit_Suc_bit1 [simp]:
+  \<open>take_bit (Suc n) (numeral (Num.Bit1 k)) = take_bit n (numeral k) * 2 + 1\<close>
+  by (simp add: take_bit_Suc numeral_Bit1_div_2 mod_2_eq_odd)
+
+lemma take_bit_numeral_1 [simp]:
+  \<open>take_bit (numeral l) 1 = 1\<close>
+  by (simp add: take_bit_rec [of \<open>numeral l\<close> 1])
+
+lemma take_bit_numeral_bit0 [simp]:
+  \<open>take_bit (numeral l) (numeral (Num.Bit0 k)) = take_bit (pred_numeral l) (numeral k) * 2\<close>
+  by (simp add: take_bit_rec numeral_Bit0_div_2)
+
+lemma take_bit_numeral_bit1 [simp]:
+  \<open>take_bit (numeral l) (numeral (Num.Bit1 k)) = take_bit (pred_numeral l) (numeral k) * 2 + 1\<close>
+  by (simp add: take_bit_rec numeral_Bit1_div_2 mod_2_eq_odd)
+
+lemma drop_bit_Suc_bit0 [simp]:
+  \<open>drop_bit (Suc n) (numeral (Num.Bit0 k)) = drop_bit n (numeral k)\<close>
+  by (simp add: drop_bit_Suc numeral_Bit0_div_2)
+
+lemma drop_bit_Suc_bit1 [simp]:
+  \<open>drop_bit (Suc n) (numeral (Num.Bit1 k)) = drop_bit n (numeral k)\<close>
+  by (simp add: drop_bit_Suc numeral_Bit1_div_2)
+
+lemma drop_bit_numeral_bit0 [simp]:
+  \<open>drop_bit (numeral l) (numeral (Num.Bit0 k)) = drop_bit (pred_numeral l) (numeral k)\<close>
+  by (simp add: drop_bit_rec numeral_Bit0_div_2)
+
+lemma drop_bit_numeral_bit1 [simp]:
+  \<open>drop_bit (numeral l) (numeral (Num.Bit1 k)) = drop_bit (pred_numeral l) (numeral k)\<close>
+  by (simp add: drop_bit_rec numeral_Bit1_div_2)
+
+lemma drop_bit_of_nat:
+  "drop_bit n (of_nat m) = of_nat (drop_bit n m)"
+  by (simp add: drop_bit_eq_div Bit_Operations.drop_bit_eq_div of_nat_div [of m "2 ^ n"])
+
+lemma bit_of_nat_iff_bit [bit_simps]:
+  \<open>bit (of_nat m) n \<longleftrightarrow> bit m n\<close>
+proof -
+  have \<open>even (m div 2 ^ n) \<longleftrightarrow> even (of_nat (m div 2 ^ n))\<close>
+    by simp
+  also have \<open>of_nat (m div 2 ^ n) = of_nat m div of_nat (2 ^ n)\<close>
+    by (simp add: of_nat_div)
+  finally show ?thesis
+    by (simp add: bit_iff_odd semiring_bits_class.bit_iff_odd)
+qed
+
+lemma of_nat_drop_bit:
+  \<open>of_nat (drop_bit m n) = drop_bit m (of_nat n)\<close>
+  by (simp add: drop_bit_eq_div Bit_Operations.drop_bit_eq_div of_nat_div)
+
+lemma bit_push_bit_iff_of_nat_iff [bit_simps]:
+  \<open>bit (push_bit m (of_nat r)) n \<longleftrightarrow> m \<le> n \<and> bit (of_nat r) (n - m)\<close>
+  by (auto simp add: bit_push_bit_iff)
+
+lemma take_bit_sum:
+  "take_bit n a = (\<Sum>k = 0..<n. push_bit k (of_bool (bit a k)))"
+  for n :: nat
+proof (induction n arbitrary: a)
+  case 0
+  then show ?case
+    by simp
+next
+  case (Suc n)
+  have "(\<Sum>k = 0..<Suc n. push_bit k (of_bool (bit a k))) = 
+    of_bool (odd a) + (\<Sum>k = Suc 0..<Suc n. push_bit k (of_bool (bit a k)))"
+    by (simp add: sum.atLeast_Suc_lessThan ac_simps)
+  also have "(\<Sum>k = Suc 0..<Suc n. push_bit k (of_bool (bit a k)))
+    = (\<Sum>k = 0..<n. push_bit k (of_bool (bit (a div 2) k))) * 2"
+    by (simp only: sum.atLeast_Suc_lessThan_Suc_shift) (simp add: sum_distrib_right push_bit_double drop_bit_Suc bit_Suc)
+  finally show ?case
+    using Suc [of "a div 2"] by (simp add: ac_simps take_bit_Suc mod_2_eq_odd)
+qed
+
+end
+
+instance nat :: unique_euclidean_semiring_with_bit_operations ..
+
+instance int :: unique_euclidean_semiring_with_bit_operations ..
+
+
+subsection \<open>More properties\<close>
+
 lemma take_bit_eq_mask_iff:
   \<open>take_bit n k = mask n \<longleftrightarrow> take_bit n (k + 1) = 0\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
   for k :: int
 proof
   assume ?P
   then have \<open>take_bit n (take_bit n k + take_bit n 1) = 0\<close>
-    by (simp add: mask_eq_exp_minus_1)
+    by (simp add: mask_eq_exp_minus_1 take_bit_eq_0_iff)
   then show ?Q
     by (simp only: take_bit_add)
 next
@@ -2480,11 +2410,11 @@
 
 lemma push_bit_of_int:
   \<open>push_bit n (of_int k) = of_int (push_bit n k)\<close>
-  by (simp add: push_bit_eq_mult semiring_bit_shifts_class.push_bit_eq_mult)
+  by (simp add: push_bit_eq_mult Bit_Operations.push_bit_eq_mult)
 
 lemma of_int_push_bit:
   \<open>of_int (push_bit n k) = push_bit n (of_int k)\<close>
-  by (simp add: push_bit_eq_mult semiring_bit_shifts_class.push_bit_eq_mult)
+  by (simp add: push_bit_eq_mult Bit_Operations.push_bit_eq_mult)
 
 lemma take_bit_of_int:
   \<open>take_bit n (of_int k) = of_int (take_bit n k)\<close>
@@ -2628,6 +2558,33 @@
   \<open>Num.sub n num.One = NOT (- numeral n :: int)\<close>
   by (simp add: not_int_def)
 
+lemma bit_numeral_int_iff [bit_simps]:
+  \<open>bit (numeral m :: int) n \<longleftrightarrow> bit (numeral m :: nat) n\<close>
+  using bit_of_nat_iff_bit [of \<open>numeral m\<close> n] by simp
+
+lemma bit_minus_int_iff [bit_simps]:
+  \<open>bit (- k) n \<longleftrightarrow> \<not> bit (k - 1) n\<close>
+  for k :: int
+  using bit_not_int_iff' [of \<open>k - 1\<close>] by simp
+
+lemma bit_numeral_int_simps [simp]:
+  \<open>bit (1 :: int) (numeral n) \<longleftrightarrow> bit (0 :: int) (pred_numeral n)\<close>
+  \<open>bit (numeral (num.Bit0 w) :: int) (numeral n) \<longleftrightarrow> bit (numeral w :: int) (pred_numeral n)\<close>
+  \<open>bit (numeral (num.Bit1 w) :: int) (numeral n) \<longleftrightarrow> bit (numeral w :: int) (pred_numeral n)\<close>
+  \<open>bit (numeral (Num.BitM w) :: int) (numeral n) \<longleftrightarrow> \<not> bit (- numeral w :: int) (pred_numeral n)\<close>
+  \<open>bit (- numeral (num.Bit0 w) :: int) (numeral n) \<longleftrightarrow> bit (- numeral w :: int) (pred_numeral n)\<close>
+  \<open>bit (- numeral (num.Bit1 w) :: int) (numeral n) \<longleftrightarrow> \<not> bit (numeral w :: int) (pred_numeral n)\<close>
+  \<open>bit (- numeral (Num.BitM w) :: int) (numeral n) \<longleftrightarrow> bit (- (numeral w) :: int) (pred_numeral n)\<close>
+  by (simp_all add: bit_1_iff numeral_eq_Suc bit_Suc add_One sub_inc_One_eq bit_minus_int_iff)
+
+lemma bit_numeral_Bit0_Suc_iff [simp]:
+  \<open>bit (numeral (Num.Bit0 m) :: int) (Suc n) \<longleftrightarrow> bit (numeral m :: int) n\<close>
+  by (simp add: bit_Suc)
+
+lemma bit_numeral_Bit1_Suc_iff [simp]:
+  \<open>bit (numeral (Num.Bit1 m) :: int) (Suc n) \<longleftrightarrow> bit (numeral m :: int) n\<close>
+  by (simp add: bit_Suc)
+
 lemma int_not_numerals [simp]:
   \<open>NOT (numeral (Num.Bit0 n) :: int) = - numeral (Num.Bit1 n)\<close>
   \<open>NOT (numeral (Num.Bit1 n) :: int) = - numeral (Num.inc (num.Bit1 n))\<close>
@@ -2744,6 +2701,203 @@
 
 end
 
+context semiring_bit_operations
+begin
+
+lemma push_bit_of_nat:
+  \<open>push_bit n (of_nat m) = of_nat (push_bit n m)\<close>
+  by (simp add: push_bit_eq_mult Bit_Operations.push_bit_eq_mult)
+
+lemma of_nat_push_bit:
+  \<open>of_nat (push_bit m n) = push_bit m (of_nat n)\<close>
+  by (simp add: push_bit_eq_mult Bit_Operations.push_bit_eq_mult)
+
+lemma take_bit_of_nat:
+  \<open>take_bit n (of_nat m) = of_nat (take_bit n m)\<close>
+  by (rule bit_eqI) (simp add: bit_take_bit_iff Bit_Operations.bit_take_bit_iff bit_of_nat_iff)
+
+lemma of_nat_take_bit:
+  \<open>of_nat (take_bit n m) = take_bit n (of_nat m)\<close>
+  by (rule bit_eqI) (simp add: bit_take_bit_iff Bit_Operations.bit_take_bit_iff bit_of_nat_iff)
+
+end
+
+lemma push_bit_nat_eq:
+  \<open>push_bit n (nat k) = nat (push_bit n k)\<close>
+  by (cases \<open>k \<ge> 0\<close>) (simp_all add: push_bit_eq_mult nat_mult_distrib not_le mult_nonneg_nonpos2)
+
+lemma drop_bit_nat_eq:
+  \<open>drop_bit n (nat k) = nat (drop_bit n k)\<close>
+  apply (cases \<open>k \<ge> 0\<close>)
+   apply (simp_all add: drop_bit_eq_div nat_div_distrib nat_power_eq not_le)
+  apply (simp add: divide_int_def)
+  done
+
+lemma take_bit_nat_eq:
+  \<open>take_bit n (nat k) = nat (take_bit n k)\<close> if \<open>k \<ge> 0\<close>
+  using that by (simp add: take_bit_eq_mod nat_mod_distrib nat_power_eq)
+
+lemma nat_take_bit_eq:
+  \<open>nat (take_bit n k) = take_bit n (nat k)\<close>
+  if \<open>k \<ge> 0\<close>
+  using that by (simp add: take_bit_eq_mod nat_mod_distrib nat_power_eq)
+
+lemma not_exp_less_eq_0_int [simp]:
+  \<open>\<not> 2 ^ n \<le> (0::int)\<close>
+  by (simp add: power_le_zero_eq)
+
+lemma half_nonnegative_int_iff [simp]:
+  \<open>k div 2 \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
+proof (cases \<open>k \<ge> 0\<close>)
+  case True
+  then show ?thesis
+    by (auto simp add: divide_int_def sgn_1_pos)
+next
+  case False
+  then show ?thesis
+    by (auto simp add: divide_int_def not_le elim!: evenE)
+qed
+
+lemma half_negative_int_iff [simp]:
+  \<open>k div 2 < 0 \<longleftrightarrow> k < 0\<close> for k :: int
+  by (subst Not_eq_iff [symmetric]) (simp add: not_less)
+
+lemma push_bit_of_Suc_0 [simp]:
+  "push_bit n (Suc 0) = 2 ^ n"
+  using push_bit_of_1 [where ?'a = nat] by simp
+
+lemma take_bit_of_Suc_0 [simp]:
+  "take_bit n (Suc 0) = of_bool (0 < n)"
+  using take_bit_of_1 [where ?'a = nat] by simp
+
+lemma drop_bit_of_Suc_0 [simp]:
+  "drop_bit n (Suc 0) = of_bool (n = 0)"
+  using drop_bit_of_1 [where ?'a = nat] by simp
+
+lemma int_bit_bound:
+  fixes k :: int
+  obtains n where \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m \<longleftrightarrow> bit k n\<close>
+    and \<open>n > 0 \<Longrightarrow> bit k (n - 1) \<noteq> bit k n\<close>
+proof -
+  obtain q where *: \<open>\<And>m. q \<le> m \<Longrightarrow> bit k m \<longleftrightarrow> bit k q\<close>
+  proof (cases \<open>k \<ge> 0\<close>)
+    case True
+    moreover from power_gt_expt [of 2 \<open>nat k\<close>]
+    have \<open>nat k < 2 ^ nat k\<close>
+      by simp
+    then have \<open>int (nat k) < int (2 ^ nat k)\<close>
+      by (simp only: of_nat_less_iff)
+    ultimately have *: \<open>k div 2 ^ nat k = 0\<close>
+      by simp
+    show thesis
+    proof (rule that [of \<open>nat k\<close>])
+      fix m
+      assume \<open>nat k \<le> m\<close>
+      then show \<open>bit k m \<longleftrightarrow> bit k (nat k)\<close>
+        by (auto simp add: * bit_iff_odd power_add zdiv_zmult2_eq dest!: le_Suc_ex)
+    qed
+  next
+    case False
+    moreover from power_gt_expt [of 2 \<open>nat (- k)\<close>]
+    have \<open>nat (- k) < 2 ^ nat (- k)\<close>
+      by simp
+    then have \<open>int (nat (- k)) < int (2 ^ nat (- k))\<close>
+      by (simp only: of_nat_less_iff)
+    ultimately have \<open>- k div - (2 ^ nat (- k)) = - 1\<close>
+      by (subst div_pos_neg_trivial) simp_all
+    then have *: \<open>k div 2 ^ nat (- k) = - 1\<close>
+      by simp
+    show thesis
+    proof (rule that [of \<open>nat (- k)\<close>])
+      fix m
+      assume \<open>nat (- k) \<le> m\<close>
+      then show \<open>bit k m \<longleftrightarrow> bit k (nat (- k))\<close>
+        by (auto simp add: * bit_iff_odd power_add zdiv_zmult2_eq minus_1_div_exp_eq_int dest!: le_Suc_ex)
+    qed
+  qed
+  show thesis
+  proof (cases \<open>\<forall>m. bit k m \<longleftrightarrow> bit k q\<close>)
+    case True
+    then have \<open>bit k 0 \<longleftrightarrow> bit k q\<close>
+      by blast
+    with True that [of 0] show thesis
+      by simp
+  next
+    case False
+    then obtain r where **: \<open>bit k r \<noteq> bit k q\<close>
+      by blast
+    have \<open>r < q\<close>
+      by (rule ccontr) (use * [of r] ** in simp)
+    define N where \<open>N = {n. n < q \<and> bit k n \<noteq> bit k q}\<close>
+    moreover have \<open>finite N\<close> \<open>r \<in> N\<close>
+      using ** N_def \<open>r < q\<close> by auto
+    moreover define n where \<open>n = Suc (Max N)\<close>
+    ultimately have \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m \<longleftrightarrow> bit k n\<close>
+      apply auto
+         apply (metis (full_types, lifting) "*" Max_ge_iff Suc_n_not_le_n \<open>finite N\<close> all_not_in_conv mem_Collect_eq not_le)
+        apply (metis "*" Max_ge Suc_n_not_le_n \<open>finite N\<close> linorder_not_less mem_Collect_eq)
+        apply (metis "*" Max_ge Suc_n_not_le_n \<open>finite N\<close> linorder_not_less mem_Collect_eq)
+      apply (metis (full_types, lifting) "*" Max_ge_iff Suc_n_not_le_n \<open>finite N\<close> all_not_in_conv mem_Collect_eq not_le)
+      done
+    have \<open>bit k (Max N) \<noteq> bit k n\<close>
+      by (metis (mono_tags, lifting) "*" Max_in N_def \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m = bit k n\<close> \<open>finite N\<close> \<open>r \<in> N\<close> empty_iff le_cases mem_Collect_eq)
+    show thesis apply (rule that [of n])
+      using \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m = bit k n\<close> apply blast
+      using \<open>bit k (Max N) \<noteq> bit k n\<close> n_def by auto
+  qed
+qed
+
+context semiring_bit_operations
+begin
+
+lemma of_nat_and_eq:
+  \<open>of_nat (m AND n) = of_nat m AND of_nat n\<close>
+  by (rule bit_eqI) (simp add: bit_of_nat_iff bit_and_iff Bit_Operations.bit_and_iff)
+
+lemma of_nat_or_eq:
+  \<open>of_nat (m OR n) = of_nat m OR of_nat n\<close>
+  by (rule bit_eqI) (simp add: bit_of_nat_iff bit_or_iff Bit_Operations.bit_or_iff)
+
+lemma of_nat_xor_eq:
+  \<open>of_nat (m XOR n) = of_nat m XOR of_nat n\<close>
+  by (rule bit_eqI) (simp add: bit_of_nat_iff bit_xor_iff Bit_Operations.bit_xor_iff)
+
+end
+
+context ring_bit_operations
+begin
+
+lemma of_nat_mask_eq:
+  \<open>of_nat (mask n) = mask n\<close>
+  by (induction n) (simp_all add: mask_Suc_double Bit_Operations.mask_Suc_double of_nat_or_eq)
+
+end
+
+lemma Suc_mask_eq_exp:
+  \<open>Suc (mask n) = 2 ^ n\<close>
+  by (simp add: mask_eq_exp_minus_1)
+
+lemma less_eq_mask:
+  \<open>n \<le> mask n\<close>
+  by (simp add: mask_eq_exp_minus_1 le_diff_conv2)
+    (metis Suc_mask_eq_exp diff_Suc_1 diff_le_diff_pow diff_zero le_refl not_less_eq_eq power_0)
+
+lemma less_mask:
+  \<open>n < mask n\<close> if \<open>Suc 0 < n\<close>
+proof -
+  define m where \<open>m = n - 2\<close>
+  with that have *: \<open>n = m + 2\<close>
+    by simp
+  have \<open>Suc (Suc (Suc m)) < 4 * 2 ^ m\<close>
+    by (induction m) simp_all
+  then have \<open>Suc (m + 2) < Suc (mask (m + 2))\<close>
+    by (simp add: Suc_mask_eq_exp)
+  then have \<open>m + 2 < mask (m + 2)\<close>
+    by (simp add: less_le)
+  with * show ?thesis
+    by simp
+qed
+
 
 subsection \<open>Bit concatenation\<close>
 
@@ -3140,156 +3294,11 @@
 qed
 
 
-subsection \<open>Instance \<^typ>\<open>nat\<close>\<close>
-
-instantiation nat :: semiring_bit_operations
-begin
-
-definition and_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
-  where \<open>m AND n = nat (int m AND int n)\<close> for m n :: nat
-
-definition or_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
-  where \<open>m OR n = nat (int m OR int n)\<close> for m n :: nat
-
-definition xor_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
-  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)
-  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
-  by (simp add: and_nat_def and_int_rec [of \<open>int m\<close> \<open>int n\<close>] zdiv_int nat_add_distrib nat_mult_distrib)
-
-lemma or_nat_rec:
-  \<open>m OR n = of_bool (odd m \<or> odd n) + 2 * ((m div 2) OR (n div 2))\<close> for m n :: nat
-  by (simp add: or_nat_def or_int_rec [of \<open>int m\<close> \<open>int n\<close>] zdiv_int nat_add_distrib nat_mult_distrib)
-
-lemma xor_nat_rec:
-  \<open>m XOR n = of_bool (odd m \<noteq> odd n) + 2 * ((m div 2) XOR (n div 2))\<close> for m n :: nat
-  by (simp add: xor_nat_def xor_int_rec [of \<open>int m\<close> \<open>int n\<close>] zdiv_int nat_add_distrib nat_mult_distrib)
-
-lemma Suc_0_and_eq [simp]:
-  \<open>Suc 0 AND n = n mod 2\<close>
-  using one_and_eq [of n] by simp
-
-lemma and_Suc_0_eq [simp]:
-  \<open>n AND Suc 0 = n mod 2\<close>
-  using and_one_eq [of n] by simp
-
-lemma Suc_0_or_eq:
-  \<open>Suc 0 OR n = n + of_bool (even n)\<close>
-  using one_or_eq [of n] by simp
-
-lemma or_Suc_0_eq:
-  \<open>n OR Suc 0 = n + of_bool (even n)\<close>
-  using or_one_eq [of n] by simp
-
-lemma Suc_0_xor_eq:
-  \<open>Suc 0 XOR n = n + of_bool (even n) - of_bool (odd n)\<close>
-  using one_xor_eq [of n] by simp
-
-lemma xor_Suc_0_eq:
-  \<open>n XOR Suc 0 = n + of_bool (even n) - of_bool (odd n)\<close>
-  using xor_one_eq [of n] by simp
+subsection \<open>Horner sums\<close>
 
 context semiring_bit_operations
 begin
 
-lemma of_nat_and_eq:
-  \<open>of_nat (m AND n) = of_nat m AND of_nat n\<close>
-  by (rule bit_eqI) (simp add: bit_of_nat_iff bit_and_iff Bit_Operations.bit_and_iff)
-
-lemma of_nat_or_eq:
-  \<open>of_nat (m OR n) = of_nat m OR of_nat n\<close>
-  by (rule bit_eqI) (simp add: bit_of_nat_iff bit_or_iff Bit_Operations.bit_or_iff)
-
-lemma of_nat_xor_eq:
-  \<open>of_nat (m XOR n) = of_nat m XOR of_nat n\<close>
-  by (rule bit_eqI) (simp add: bit_of_nat_iff bit_xor_iff Bit_Operations.bit_xor_iff)
-
-end
-
-context ring_bit_operations
-begin
-
-lemma of_nat_mask_eq:
-  \<open>of_nat (mask n) = mask n\<close>
-  by (induction n) (simp_all add: mask_Suc_double Bit_Operations.mask_Suc_double of_nat_or_eq)
-
-end
-
-lemma Suc_mask_eq_exp:
-  \<open>Suc (mask n) = 2 ^ n\<close>
-  by (simp add: mask_eq_exp_minus_1)
-
-lemma less_eq_mask:
-  \<open>n \<le> mask n\<close>
-  by (simp add: mask_eq_exp_minus_1 le_diff_conv2)
-    (metis Suc_mask_eq_exp diff_Suc_1 diff_le_diff_pow diff_zero le_refl not_less_eq_eq power_0)
-
-lemma less_mask:
-  \<open>n < mask n\<close> if \<open>Suc 0 < n\<close>
-proof -
-  define m where \<open>m = n - 2\<close>
-  with that have *: \<open>n = m + 2\<close>
-    by simp
-  have \<open>Suc (Suc (Suc m)) < 4 * 2 ^ m\<close>
-    by (induction m) simp_all
-  then have \<open>Suc (m + 2) < Suc (mask (m + 2))\<close>
-    by (simp add: Suc_mask_eq_exp)
-  then have \<open>m + 2 < mask (m + 2)\<close>
-    by (simp add: less_le)
-  with * show ?thesis
-    by simp
-qed
-
-
-subsection \<open>Horner sums\<close>
-
-context semiring_bit_shifts
-begin
-
 lemma horner_sum_bit_eq_take_bit:
   \<open>horner_sum of_bool 2 (map (bit a) [0..<n]) = take_bit n a\<close>
 proof (induction a arbitrary: n rule: bits_induct)
@@ -3321,7 +3330,7 @@
 
 end
 
-context unique_euclidean_semiring_with_bit_shifts
+context unique_euclidean_semiring_with_bit_operations
 begin
 
 lemma bit_horner_sum_bit_iff [bit_simps]:
@@ -3556,6 +3565,8 @@
       \<^item> (Bounded) conversion from and to a list of bits: @{thm horner_sum_bit_eq_take_bit [where ?'a = int, no_vars]}
 \<close>
 
+find_theorems \<open>(_ AND _) * _ = _\<close>
+
 no_notation
   "and"  (infixr \<open>AND\<close> 64)
     and or  (infixr \<open>OR\<close>  59)

--- a/src/HOL/Code_Numeral.thy	Tue Aug 03 10:14:48 2021 +0200
+++ b/src/HOL/Code_Numeral.thy	Wed Aug 04 08:27:16 2021 +0200
@@ -293,12 +293,36 @@
 instance integer :: unique_euclidean_ring_with_nat
   by (standard; transfer) (simp_all add: of_nat_div division_segment_int_def)
 
-instantiation integer :: semiring_bit_shifts
+instantiation integer :: ring_bit_operations
 begin
 
 lift_definition bit_integer :: \<open>integer \<Rightarrow> nat \<Rightarrow> bool\<close>
   is bit .
 
+lift_definition not_integer :: \<open>integer \<Rightarrow> integer\<close>
+  is not .
+
+lift_definition and_integer :: \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close>
+  is \<open>and\<close> .
+
+lift_definition or_integer :: \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close>
+  is or .
+
+lift_definition xor_integer ::  \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close>
+  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 .
+
 lift_definition push_bit_integer :: \<open>nat \<Rightarrow> integer \<Rightarrow> integer\<close>
   is push_bit .
 
@@ -312,18 +336,47 @@
   (fact bit_eq_rec bits_induct bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod
     bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
     exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq
-    even_mask_div_iff even_mult_exp_div_exp_iff)+
+    even_mask_div_iff even_mult_exp_div_exp_iff
+    bit_and_iff bit_or_iff bit_xor_iff mask_eq_exp_minus_1
+    set_bit_def bit_unset_bit_iff flip_bit_def bit_not_iff minus_eq_not_minus_1)+
 
 end
 
-instance integer :: unique_euclidean_semiring_with_bit_shifts ..
+instance integer :: unique_euclidean_semiring_with_bit_operations ..
+
+context
+  includes bit_operations_syntax
+begin
 
 lemma [code]:
   \<open>bit k n \<longleftrightarrow> odd (drop_bit n k)\<close>
+  \<open>NOT k = - k - 1\<close>
+  \<open>mask n = 2 ^ n - (1 :: integer)\<close>
+  \<open>set_bit n k = k OR push_bit n 1\<close>
+  \<open>unset_bit n k = k AND NOT (push_bit n 1)\<close>
+  \<open>flip_bit n k = k XOR push_bit n 1\<close>
   \<open>push_bit n k = k * 2 ^ n\<close>
   \<open>drop_bit n k = k div 2 ^ n\<close>
   \<open>take_bit n k = k mod 2 ^ n\<close> for k :: integer
-  by (fact bit_iff_odd_drop_bit push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+
+  by (fact bit_iff_odd_drop_bit not_eq_complement mask_eq_exp_minus_1
+    set_bit_eq_or unset_bit_eq_and_not flip_bit_eq_xor push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+
+
+lemma [code]:
+  \<open>k AND l = (if k = 0 \<or> l = 0 then 0 else if k = - 1 then l else if l = - 1 then k
+    else (k mod 2) * (l mod 2) + 2 * ((k div 2) AND (l div 2)))\<close> for k l :: integer
+  by transfer (fact and_int_unfold) 
+
+lemma [code]:
+  \<open>k OR l = (if k = - 1 \<or> l = - 1 then - 1 else if k = 0 then l else if l = 0 then k
+    else max (k mod 2) (l mod 2) + 2 * ((k div 2) OR (l div 2)))\<close> for k l :: integer
+  by transfer (fact or_int_unfold)
+
+lemma [code]:
+  \<open>k XOR l = (if k = - 1 then NOT l else if l = - 1 then NOT k else if k = 0 then l else if l = 0 then k
+    else \<bar>k mod 2 - l mod 2\<bar> + 2 * ((k div 2) XOR (l div 2)))\<close> for k l :: integer
+  by transfer (fact xor_int_unfold)
+
+end
 
 instantiation integer :: unique_euclidean_semiring_numeral
 begin
@@ -1018,12 +1071,33 @@
 instance natural :: unique_euclidean_semiring_with_nat
   by (standard; transfer) simp_all
 
-instantiation natural :: semiring_bit_shifts
+instantiation natural :: semiring_bit_operations
 begin
 
 lift_definition bit_natural :: \<open>natural \<Rightarrow> nat \<Rightarrow> bool\<close>
   is bit .
 
+lift_definition and_natural :: \<open>natural \<Rightarrow> natural \<Rightarrow> natural\<close>
+  is \<open>and\<close> .
+
+lift_definition or_natural :: \<open>natural \<Rightarrow> natural \<Rightarrow> natural\<close>
+  is or .
+
+lift_definition xor_natural ::  \<open>natural \<Rightarrow> natural \<Rightarrow> natural\<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 .
+
 lift_definition push_bit_natural :: \<open>nat \<Rightarrow> natural \<Rightarrow> natural\<close>
   is push_bit .
 
@@ -1037,18 +1111,49 @@
   (fact bit_eq_rec bits_induct bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod
     bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
     exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq
-    even_mask_div_iff even_mult_exp_div_exp_iff)+
+    even_mask_div_iff even_mult_exp_div_exp_iff bit_and_iff bit_or_iff bit_xor_iff
+    mask_eq_exp_minus_1 set_bit_def bit_unset_bit_iff flip_bit_def)+
 
 end
 
-instance natural :: unique_euclidean_semiring_with_bit_shifts ..
+instance natural :: unique_euclidean_semiring_with_bit_operations ..
+
+context
+  includes bit_operations_syntax
+begin
 
 lemma [code]:
   \<open>bit m n \<longleftrightarrow> odd (drop_bit n m)\<close>
+  \<open>mask n = 2 ^ n - (1 :: integer)\<close>
+  \<open>set_bit n m = m OR push_bit n 1\<close>
+  \<open>flip_bit n m = m XOR push_bit n 1\<close>
   \<open>push_bit n m = m * 2 ^ n\<close>
   \<open>drop_bit n m = m div 2 ^ n\<close>
   \<open>take_bit n m = m mod 2 ^ n\<close> for m :: natural
-  by (fact bit_iff_odd_drop_bit push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+
+  by (fact bit_iff_odd_drop_bit mask_eq_exp_minus_1
+    set_bit_eq_or flip_bit_eq_xor push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+
+
+lemma [code]:
+  \<open>m AND n = (if m = 0 \<or> n = 0 then 0
+    else (m mod 2) * (n mod 2) + 2 * ((m div 2) AND (n div 2)))\<close> for m n :: natural
+  by transfer (fact and_nat_unfold)
+
+lemma [code]:
+  \<open>m OR n = (if m = 0 then n else if n = 0 then m
+    else max (m mod 2) (n mod 2) + 2 * ((m div 2) OR (n div 2)))\<close> for m n :: natural
+  by transfer (fact or_nat_unfold)
+
+lemma [code]:
+  \<open>m XOR n = (if m = 0 then n else if n = 0 then m
+    else (m mod 2 + n mod 2) mod 2 + 2 * ((m div 2) XOR (n div 2)))\<close> for m n :: natural
+  by transfer (fact xor_nat_unfold)
+
+lemma [code]:
+  \<open>unset_bit 0 m = 2 * (m div 2)\<close>
+  \<open>unset_bit (Suc n) m = m mod 2 + 2 * unset_bit n (m div 2)\<close> for m :: natural
+  by (transfer; simp add: unset_bit_Suc)+
+
+end
 
 lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
   is "nat :: int \<Rightarrow> nat"
@@ -1142,6 +1247,10 @@
   "integer_of_natural (natural_of_integer k) = max 0 k"
   by simp
 
+lemma [code]:
+  \<open>integer_of_natural (mask n) = mask n\<close>
+  by transfer (simp add: mask_eq_exp_minus_1 of_nat_diff)
+
 lemma [code_abbrev]:
   "natural_of_integer (Code_Numeral.Pos k) = numeral k"
   by transfer simp
@@ -1211,83 +1320,6 @@
     "modulo :: natural \<Rightarrow> _"
     integer_of_natural natural_of_integer
 
-
-subsection \<open>Bit operations\<close>
-
-instantiation integer :: ring_bit_operations
-begin
-
-lift_definition not_integer :: \<open>integer \<Rightarrow> integer\<close>
-  is not .
-
-lift_definition and_integer :: \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close>
-  is \<open>and\<close> .
-
-lift_definition or_integer :: \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close>
-  is or .
-
-lift_definition xor_integer ::  \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close>
-  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
-    set_bit_def bit_unset_bit_iff flip_bit_def)
-
-end
-
-lemma [code]:
-  \<open>mask n = 2 ^ n - (1::integer)\<close>
-  by (simp add: mask_eq_exp_minus_1)
-
-instantiation natural :: semiring_bit_operations
-begin
-
-lift_definition and_natural :: \<open>natural \<Rightarrow> natural \<Rightarrow> natural\<close>
-  is \<open>and\<close> .
-
-lift_definition or_natural :: \<open>natural \<Rightarrow> natural \<Rightarrow> natural\<close>
-  is or .
-
-lift_definition xor_natural ::  \<open>natural \<Rightarrow> natural \<Rightarrow> natural\<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
-    set_bit_def bit_unset_bit_iff flip_bit_def)
-
-end
-
-lemma [code]:
-  \<open>integer_of_natural (mask n) = mask n\<close>
-  by transfer (simp add: mask_eq_exp_minus_1 of_nat_diff)
-
-
 lifting_update integer.lifting
 lifting_forget integer.lifting
 

--- a/src/HOL/Library/Word.thy	Tue Aug 03 10:14:48 2021 +0200
+++ b/src/HOL/Library/Word.thy	Wed Aug 04 08:27:16 2021 +0200
@@ -928,59 +928,6 @@
     \<longleftrightarrow> n < LENGTH('a) \<and> bit (- numeral w :: int) n\<close>
   by transfer simp
 
-instantiation word :: (len) semiring_bit_shifts
-begin
-
-lift_definition push_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
-  is push_bit
-proof -
-  show \<open>take_bit LENGTH('a) (push_bit n k) = take_bit LENGTH('a) (push_bit n l)\<close>
-    if \<open>take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close> for k l :: int and n :: nat
-  proof -
-    from that
-    have \<open>take_bit (LENGTH('a) - n) (take_bit LENGTH('a) k)
-      = take_bit (LENGTH('a) - n) (take_bit LENGTH('a) l)\<close>
-      by simp
-    moreover have \<open>min (LENGTH('a) - n) LENGTH('a) = LENGTH('a) - n\<close>
-      by simp
-    ultimately show ?thesis
-      by (simp add: take_bit_push_bit)
-  qed
-qed
-
-lift_definition drop_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
-  is \<open>\<lambda>n. drop_bit n \<circ> take_bit LENGTH('a)\<close>
-  by (simp add: take_bit_eq_mod)
-
-lift_definition take_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
-  is \<open>\<lambda>n. take_bit (min LENGTH('a) n)\<close>
-  by (simp add: ac_simps) (simp only: flip: take_bit_take_bit)
-
-instance proof
-  show \<open>push_bit n a = a * 2 ^ n\<close> for n :: nat and a :: \<open>'a word\<close>
-    by transfer (simp add: push_bit_eq_mult)
-  show \<open>drop_bit n a = a div 2 ^ n\<close> for n :: nat and a :: \<open>'a word\<close>
-    by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit)
-  show \<open>take_bit n a = a mod 2 ^ n\<close> for n :: nat and a :: \<open>'a word\<close>
-    by transfer (auto simp flip: take_bit_eq_mod)
-qed
-
-end
-
-lemma [code]:
-  \<open>push_bit n w = w * 2 ^ n\<close> for w :: \<open>'a::len word\<close>
-  by (fact push_bit_eq_mult)
-
-lemma [code]:
-  \<open>Word.the_int (drop_bit n w) = drop_bit n (Word.the_int w)\<close>
-  by transfer (simp add: drop_bit_take_bit min_def le_less less_diff_conv)
-
-lemma [code]:
-  \<open>Word.the_int (take_bit n w) = (if n < LENGTH('a::len) then take_bit n (Word.the_int w) else Word.the_int w)\<close>
-  for w :: \<open>'a::len word\<close>
-  by transfer (simp add: not_le not_less ac_simps min_absorb2)
-
-
 instantiation word :: (len) ring_bit_operations
 begin
 
@@ -1016,12 +963,53 @@
   is flip_bit
   by (simp add: flip_bit_def)
 
-instance by (standard; transfer)
-  (auto simp add: minus_eq_not_minus_1 mask_eq_exp_minus_1
-    bit_simps set_bit_def flip_bit_def)
+lift_definition push_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
+  is push_bit
+proof -
+  show \<open>take_bit LENGTH('a) (push_bit n k) = take_bit LENGTH('a) (push_bit n l)\<close>
+    if \<open>take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close> for k l :: int and n :: nat
+  proof -
+    from that
+    have \<open>take_bit (LENGTH('a) - n) (take_bit LENGTH('a) k)
+      = take_bit (LENGTH('a) - n) (take_bit LENGTH('a) l)\<close>
+      by simp
+    moreover have \<open>min (LENGTH('a) - n) LENGTH('a) = LENGTH('a) - n\<close>
+      by simp
+    ultimately show ?thesis
+      by (simp add: take_bit_push_bit)
+  qed
+qed
+
+lift_definition drop_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
+  is \<open>\<lambda>n. drop_bit n \<circ> take_bit LENGTH('a)\<close>
+  by (simp add: take_bit_eq_mod)
+
+lift_definition take_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
+  is \<open>\<lambda>n. take_bit (min LENGTH('a) n)\<close>
+  by (simp add: ac_simps) (simp only: flip: take_bit_take_bit)
+
+instance apply (standard; transfer)
+  apply (auto simp add: minus_eq_not_minus_1 mask_eq_exp_minus_1
+    bit_simps set_bit_def flip_bit_def take_bit_drop_bit
+    simp flip: drop_bit_eq_div take_bit_eq_mod)
+   apply (simp_all add: drop_bit_take_bit flip: push_bit_eq_mult)
+  done
 
 end
 
+lemma [code]:
+  \<open>push_bit n w = w * 2 ^ n\<close> for w :: \<open>'a::len word\<close>
+  by (fact push_bit_eq_mult)
+
+lemma [code]:
+  \<open>Word.the_int (drop_bit n w) = drop_bit n (Word.the_int w)\<close>
+  by transfer (simp add: drop_bit_take_bit min_def le_less less_diff_conv)
+
+lemma [code]:
+  \<open>Word.the_int (take_bit n w) = (if n < LENGTH('a::len) then take_bit n (Word.the_int w) else Word.the_int w)\<close>
+  for w :: \<open>'a::len word\<close>
+  by transfer (simp add: not_le not_less ac_simps min_absorb2)
+
 lemma [code_abbrev]:
   \<open>push_bit n 1 = (2 :: 'a::len word) ^ n\<close>
   by (fact push_bit_of_1)
@@ -1114,7 +1102,7 @@
 
 end
 
-context semiring_bit_shifts
+context semiring_bit_operations
 begin
 
 lemma unsigned_push_bit_eq:
@@ -1144,7 +1132,7 @@
 
 end
 
-context unique_euclidean_semiring_with_bit_shifts
+context unique_euclidean_semiring_with_bit_operations
 begin
 
 lemma unsigned_drop_bit_eq:
@@ -1400,7 +1388,7 @@
     by (simp add: of_nat_mod)
 qed
 
-context semiring_bit_shifts
+context semiring_bit_operations
 begin
 
 lemma unsigned_ucast_eq:

--- a/src/HOL/Library/Z2.thy	Tue Aug 03 10:14:48 2021 +0200
+++ b/src/HOL/Library/Z2.thy	Wed Aug 04 08:27:16 2021 +0200
@@ -43,7 +43,7 @@
   \<open>a \<noteq> 0 \<longleftrightarrow> a = 1\<close> for a :: bit
   by (cases a) simp_all
 
-lemma bit_not_one_imp [simp]:
+lemma bit_not_one_iff [simp]:
   \<open>a \<noteq> 1 \<longleftrightarrow> a = 0\<close> for a :: bit
   by (cases a) simp_all
 
@@ -144,6 +144,24 @@
   \<open>a ^ n = of_bool (odd a \<or> n = 0)\<close> for a :: bit
   by (cases a) simp_all
 
+instantiation bit :: field
+begin
+
+definition uminus_bit :: \<open>bit \<Rightarrow> bit\<close>
+  where [simp]: \<open>uminus_bit = id\<close>
+
+definition inverse_bit :: \<open>bit \<Rightarrow> bit\<close>
+  where [simp]: \<open>inverse_bit = id\<close>
+
+instance
+  apply standard
+  apply simp_all
+  apply (simp only: Z2.bit_eq_iff even_add)
+  apply simp
+  done
+
+end
+
 instantiation bit :: semiring_bits
 begin
 
@@ -158,30 +176,16 @@
 
 end
 
-instantiation bit :: semiring_bit_shifts
-begin
-
-definition push_bit_bit :: \<open>nat \<Rightarrow> bit \<Rightarrow> bit\<close>
-  where [simp]: \<open>push_bit n b = of_bool (odd b \<and> n = 0)\<close> for b :: bit
-
-definition drop_bit_bit :: \<open>nat \<Rightarrow> bit \<Rightarrow> bit\<close>
-  where [simp]: \<open>drop_bit_bit = push_bit\<close>
-
-definition take_bit_bit :: \<open>nat \<Rightarrow> bit \<Rightarrow> bit\<close>
-  where [simp]: \<open>take_bit n b = of_bool (odd b \<and> n > 0)\<close> for b :: bit
-
-instance
-  by standard simp_all
-
-end
-
-instantiation bit :: semiring_bit_operations
+instantiation bit :: ring_bit_operations
 begin
 
 context
   includes bit_operations_syntax
 begin
 
+definition not_bit :: \<open>bit \<Rightarrow> bit\<close>
+  where [simp]: \<open>NOT b = of_bool (even b)\<close> for b :: bit
+
 definition and_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close>
   where [simp]: \<open>b AND c = of_bool (odd b \<and> odd c)\<close> for b c :: bit
 
@@ -203,10 +207,22 @@
 definition flip_bit_bit :: \<open>nat \<Rightarrow> bit \<Rightarrow> bit\<close>
   where [simp]: \<open>flip_bit n b = of_bool ((n = 0) \<noteq> odd b)\<close> for b :: bit
 
+definition push_bit_bit :: \<open>nat \<Rightarrow> bit \<Rightarrow> bit\<close>
+  where [simp]: \<open>push_bit n b = of_bool (odd b \<and> n = 0)\<close> for b :: bit
+
+definition drop_bit_bit :: \<open>nat \<Rightarrow> bit \<Rightarrow> bit\<close>
+  where [simp]: \<open>drop_bit n b = of_bool (odd b \<and> n = 0)\<close> for b :: bit
+
+definition take_bit_bit :: \<open>nat \<Rightarrow> bit \<Rightarrow> bit\<close>
+  where [simp]: \<open>take_bit n b = of_bool (odd b \<and> n > 0)\<close> for b :: bit
+
 end
 
 instance
-  by standard auto
+  apply standard
+             apply auto
+  apply (simp only: Z2.bit_eq_iff even_add even_zero)
+  done
 
 end
 
@@ -218,30 +234,6 @@
   \<open>(*) = (Bit_Operations.and :: bit \<Rightarrow> _)\<close>
   by (simp add: fun_eq_iff)
 
-instantiation bit :: field
-begin
-
-definition uminus_bit :: \<open>bit \<Rightarrow> bit\<close>
-  where [simp]: \<open>uminus_bit = id\<close>
-
-definition inverse_bit :: \<open>bit \<Rightarrow> bit\<close>
-  where [simp]: \<open>inverse_bit = id\<close>
-
-instance
-  by standard simp_all
-
-end
-
-instantiation bit :: ring_bit_operations
-begin
-
-definition not_bit :: \<open>bit \<Rightarrow> bit\<close>
-  where [simp]: \<open>NOT b = of_bool (even b)\<close> for b :: bit
-
-instance
-  by standard auto
-
-end
 
 lemma bit_numeral_even [simp]: "numeral (Num.Bit0 w) = (0 :: bit)"
   by (simp only: Z2.bit_eq_iff even_numeral) simp

--- a/src/HOL/ROOT	Tue Aug 03 10:14:48 2021 +0200
+++ b/src/HOL/ROOT	Wed Aug 04 08:27:16 2021 +0200
@@ -646,7 +646,6 @@
     Ballot
     BinEx
     Birthday_Paradox
-    Bit_Lists
     Bubblesort
     CTL
     Cartouche_Examples

--- a/src/HOL/String.thy	Tue Aug 03 10:14:48 2021 +0200
+++ b/src/HOL/String.thy	Wed Aug 04 08:27:16 2021 +0200
@@ -38,7 +38,7 @@
 
 end
 
-context unique_euclidean_semiring_with_bit_shifts
+context unique_euclidean_semiring_with_bit_operations
 begin
 
 definition char_of :: \<open>'a \<Rightarrow> char\<close>

--- a/src/HOL/ex/Bit_Lists.thy	Tue Aug 03 10:14:48 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,356 +0,0 @@
- (*  Author:  Florian Haftmann, TUM
-*)
-
-section \<open>Proof(s) of concept for algebraically founded lists of bits\<close>
-
-theory Bit_Lists
-  imports
-    "HOL-Library.Word" "HOL-Library.More_List"
-begin
-
-subsection \<open>Fragments of algebraic bit representations\<close>
-
-context comm_semiring_1
-begin
- 
-abbreviation (input) unsigned_of_bits :: "bool list \<Rightarrow> 'a"
-  where "unsigned_of_bits \<equiv> horner_sum of_bool 2"
-
-lemma unsigned_of_bits_replicate_False [simp]:
-  "unsigned_of_bits (replicate n False) = 0"
-  by (induction n) simp_all
-
-end
-
-context unique_euclidean_semiring_with_bit_shifts
-begin
-
-lemma unsigned_of_bits_append [simp]:
-  "unsigned_of_bits (bs @ cs) = unsigned_of_bits bs
-    + push_bit (length bs) (unsigned_of_bits cs)"
-  by (induction bs) (simp_all add: push_bit_double,
-    simp_all add: algebra_simps)
-
-lemma unsigned_of_bits_take [simp]:
-  "unsigned_of_bits (take n bs) = take_bit n (unsigned_of_bits bs)"
-proof (induction bs arbitrary: n)
-  case Nil
-  then show ?case
-    by simp
-next
-  case (Cons b bs)
-  then show ?case
-    by (cases n) (simp_all add: ac_simps take_bit_Suc)
-qed
-
-lemma unsigned_of_bits_drop [simp]:
-  "unsigned_of_bits (drop n bs) = drop_bit n (unsigned_of_bits bs)"
-proof (induction bs arbitrary: n)
-  case Nil
-  then show ?case
-    by simp
-next
-  case (Cons b bs)
-  then show ?case
-    by (cases n) (simp_all add: drop_bit_Suc)
-qed
-
-lemma bit_unsigned_of_bits_iff:
-  \<open>bit (unsigned_of_bits bs) n \<longleftrightarrow> nth_default False bs n\<close>
-proof (induction bs arbitrary: n)
-  case Nil
-  then show ?case
-    by simp
-next
-  case (Cons b bs)
-  then show ?case
-    by (cases n) (simp_all add: bit_Suc)
-qed
-
-primrec n_bits_of :: "nat \<Rightarrow> 'a \<Rightarrow> bool list"
-  where
-    "n_bits_of 0 a = []"
-  | "n_bits_of (Suc n) a = odd a # n_bits_of n (a div 2)"
-
-lemma n_bits_of_eq_iff:
-  "n_bits_of n a = n_bits_of n b \<longleftrightarrow> take_bit n a = take_bit n b"
-  apply (induction n arbitrary: a b)
-   apply (auto elim!: evenE oddE simp add: take_bit_Suc mod_2_eq_odd)
-    apply (metis dvd_triv_right even_plus_one_iff odd_iff_mod_2_eq_one)
-   apply (metis dvd_triv_right even_plus_one_iff odd_iff_mod_2_eq_one)
-  done
-
-lemma take_n_bits_of [simp]:
-  "take m (n_bits_of n a) = n_bits_of (min m n) a"
-proof -
-  define q and v and w where "q = min m n" and "v = m - q" and "w = n - q"
-  then have "v = 0 \<or> w = 0"
-    by auto
-  then have "take (q + v) (n_bits_of (q + w) a) = n_bits_of q a"
-    by (induction q arbitrary: a) auto
-  with q_def v_def w_def show ?thesis
-    by simp
-qed
-
-lemma unsigned_of_bits_n_bits_of [simp]:
-  "unsigned_of_bits (n_bits_of n a) = take_bit n a"
-  by (induction n arbitrary: a) (simp_all add: ac_simps take_bit_Suc mod_2_eq_odd)
-
-end
-
-
-subsection \<open>Syntactic bit representation\<close>
-
-class bit_representation =
-  fixes bits_of :: "'a \<Rightarrow> bool list"
-    and of_bits :: "bool list \<Rightarrow> 'a"
-  assumes of_bits_of [simp]: "of_bits (bits_of a) = a"
-
-instantiation nat :: bit_representation
-begin
-
-fun bits_of_nat :: "nat \<Rightarrow> bool list"
-  where "bits_of (n::nat) =
-    (if n = 0 then [] else odd n # bits_of (n div 2))"
-
-lemma bits_of_nat_simps [simp]:
-  "bits_of (0::nat) = []"
-  "n > 0 \<Longrightarrow> bits_of n = odd n # bits_of (n div 2)" for n :: nat
-  by simp_all
-
-declare bits_of_nat.simps [simp del]
-
-definition of_bits_nat :: "bool list \<Rightarrow> nat"
-  where [simp]: "of_bits_nat = unsigned_of_bits"
-  \<comment> \<open>remove simp\<close>
-
-instance proof
-  show "of_bits (bits_of n) = n" for n :: nat
-    by (induction n rule: nat_bit_induct) simp_all
-qed
-
-end
-
-lemma bit_of_bits_nat_iff:
-  \<open>bit (of_bits bs :: nat) n \<longleftrightarrow> nth_default False bs n\<close>
-  by (simp add: bit_unsigned_of_bits_iff)
-
-lemma bits_of_Suc_0 [simp]:
-  "bits_of (Suc 0) = [True]"
-  by simp
-
-lemma bits_of_1_nat [simp]:
-  "bits_of (1 :: nat) = [True]"
-  by simp
-
-lemma bits_of_nat_numeral_simps [simp]:
-  "bits_of (numeral Num.One :: nat) = [True]" (is ?One)
-  "bits_of (numeral (Num.Bit0 n) :: nat) = False # bits_of (numeral n :: nat)" (is ?Bit0)
-  "bits_of (numeral (Num.Bit1 n) :: nat) = True # bits_of (numeral n :: nat)" (is ?Bit1)
-proof -
-  show ?One
-    by simp
-  define m :: nat where "m = numeral n"
-  then have "m > 0" and *: "numeral n = m" "numeral (Num.Bit0 n) = 2 * m" "numeral (Num.Bit1 n) = Suc (2 * m)"
-    by simp_all
-  from \<open>m > 0\<close> show ?Bit0 ?Bit1
-    by (simp_all add: *)
-qed
-
-lemma unsigned_of_bits_of_nat [simp]:
-  "unsigned_of_bits (bits_of n) = n" for n :: nat
-  using of_bits_of [of n] by simp
-
-instantiation int :: bit_representation
-begin
-
-fun bits_of_int :: "int \<Rightarrow> bool list"
-  where "bits_of_int k = odd k #
-    (if k = 0 \<or> k = - 1 then [] else bits_of_int (k div 2))"
-
-lemma bits_of_int_simps [simp]:
-  "bits_of (0 :: int) = [False]"
-  "bits_of (- 1 :: int) = [True]"
-  "k \<noteq> 0 \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> bits_of k = odd k # bits_of (k div 2)" for k :: int
-  by simp_all
-
-lemma bits_of_not_Nil [simp]:
-  "bits_of k \<noteq> []" for k :: int
-  by simp
-
-declare bits_of_int.simps [simp del]
-
-definition of_bits_int :: "bool list \<Rightarrow> int"
-  where "of_bits_int bs = (if bs = [] \<or> \<not> last bs then unsigned_of_bits bs
-    else unsigned_of_bits bs - 2 ^ length bs)"
-
-lemma of_bits_int_simps [simp]:
-  "of_bits [] = (0 :: int)"
-  "of_bits [False] = (0 :: int)"
-  "of_bits [True] = (- 1 :: int)"
-  "of_bits (bs @ [b]) = (unsigned_of_bits bs :: int) - (2 ^ length bs) * of_bool b"
-  "of_bits (False # bs) = 2 * (of_bits bs :: int)"
-  "bs \<noteq> [] \<Longrightarrow> of_bits (True # bs) = 1 + 2 * (of_bits bs :: int)"
-  by (simp_all add: of_bits_int_def push_bit_of_1)
-
-instance proof
-  show "of_bits (bits_of k) = k" for k :: int
-    by (induction k rule: int_bit_induct) simp_all
-qed
-
-lemma bits_of_1_int [simp]:
-  "bits_of (1 :: int) = [True, False]"
-  by simp
-
-lemma bits_of_int_numeral_simps [simp]:
-  "bits_of (numeral Num.One :: int) = [True, False]" (is ?One)
-  "bits_of (numeral (Num.Bit0 n) :: int) = False # bits_of (numeral n :: int)" (is ?Bit0)
-  "bits_of (numeral (Num.Bit1 n) :: int) = True # bits_of (numeral n :: int)" (is ?Bit1)
-  "bits_of (- numeral (Num.Bit0 n) :: int) = False # bits_of (- numeral n :: int)" (is ?nBit0)
-  "bits_of (- numeral (Num.Bit1 n) :: int) = True # bits_of (- numeral (Num.inc n) :: int)" (is ?nBit1)
-proof -
-  show ?One
-    by simp
-  define k :: int where "k = numeral n"
-  then have "k > 0" and *: "numeral n = k" "numeral (Num.Bit0 n) = 2 * k" "numeral (Num.Bit1 n) = 2 * k + 1"
-    "numeral (Num.inc n) = k + 1"
-    by (simp_all add: add_One)
-  have "- (2 * k) div 2 = - k" "(- (2 * k) - 1) div 2 = - k - 1"
-    by simp_all
-  with \<open>k > 0\<close> show ?Bit0 ?Bit1 ?nBit0 ?nBit1
-    by (simp_all add: *)
-qed
-
-lemma bit_of_bits_int_iff:
-  \<open>bit (of_bits bs :: int) n \<longleftrightarrow> nth_default (bs \<noteq> [] \<and> last bs) bs n\<close>
-proof (induction bs arbitrary: n)
-  case Nil
-  then show ?case
-    by simp
-next
-  case (Cons b bs)
-  then show ?case
-    by (cases n; cases b; cases bs) (simp_all add: bit_Suc)
-qed
-
-lemma of_bits_append [simp]:
-  "of_bits (bs @ cs) = of_bits bs + push_bit (length bs) (of_bits cs :: int)"
-    if "bs \<noteq> []" "\<not> last bs"
-using that proof (induction bs rule: list_nonempty_induct)
-  case (single b)
-  then show ?case
-    by simp
-next
-  case (cons b bs)
-  then show ?case
-    by (cases b) (simp_all add: push_bit_double)
-qed
-
-lemma of_bits_replicate_False [simp]:
-  "of_bits (replicate n False) = (0 :: int)"
-  by (auto simp add: of_bits_int_def)
-
-lemma of_bits_drop [simp]:
-  "of_bits (drop n bs) = drop_bit n (of_bits bs :: int)"
-    if "n < length bs"
-using that proof (induction bs arbitrary: n)
-  case Nil
-  then show ?case
-    by simp
-next
-  case (Cons b bs)
-  show ?case
-  proof (cases n)
-    case 0
-    then show ?thesis
-      by simp
-  next
-    case (Suc n)
-    with Cons.prems have "bs \<noteq> []"
-      by auto
-    with Suc Cons.IH [of n] Cons.prems show ?thesis
-      by (cases b) (simp_all add: drop_bit_Suc)
-  qed
-qed
-
-end
-
-lemma unsigned_of_bits_eq_of_bits:
-  "unsigned_of_bits bs = (of_bits (bs @ [False]) :: int)"
-  by (simp add: of_bits_int_def)
-
-unbundle word.lifting
-
-instantiation word :: (len) bit_representation
-begin
-
-lift_definition bits_of_word :: "'a word \<Rightarrow> bool list"
-  is "n_bits_of LENGTH('a)"
-  by (simp add: n_bits_of_eq_iff)
-
-lift_definition of_bits_word :: "bool list \<Rightarrow> 'a word"
-  is unsigned_of_bits .
-
-instance proof
-  fix a :: "'a word"
-  show "of_bits (bits_of a) = a"
-    by transfer simp
-qed
-
-end
-
-lifting_update word.lifting
-lifting_forget word.lifting
-
-
-subsection \<open>Bit representations with bit operations\<close>
-
-class semiring_bit_representation = semiring_bit_operations + bit_representation
-  opening bit_operations_syntax +
-  assumes and_eq: "length bs = length cs \<Longrightarrow>
-      of_bits bs AND of_bits cs = of_bits (map2 (\<and>) bs cs)"
-    and or_eq: "length bs = length cs \<Longrightarrow>
-      of_bits bs OR of_bits cs = of_bits (map2 (\<or>) bs cs)"
-    and xor_eq: "length bs = length cs \<Longrightarrow>
-      of_bits bs XOR of_bits cs = of_bits (map2 (\<noteq>) bs cs)"
-    and push_bit_eq: "push_bit n a = of_bits (replicate n False @ bits_of a)"
-    and drop_bit_eq: "n < length (bits_of a) \<Longrightarrow> drop_bit n a = of_bits (drop n (bits_of a))"
-
-class ring_bit_representation = ring_bit_operations + semiring_bit_representation +
-  assumes not_eq: "not = of_bits \<circ> map Not \<circ> bits_of"
-
-instance nat :: semiring_bit_representation
-  by standard (simp_all add: bit_eq_iff bit_unsigned_of_bits_iff nth_default_map2 [of _ _ _ False False]
-    bit_and_iff bit_or_iff bit_xor_iff)
-
-instance int :: ring_bit_representation
-including bit_operations_syntax proof
-  {
-    fix bs cs :: \<open>bool list\<close>
-    assume \<open>length bs = length cs\<close>
-    then have \<open>cs = [] \<longleftrightarrow> bs = []\<close>
-      by auto
-    with \<open>length bs = length cs\<close> have \<open>zip bs cs \<noteq> [] \<and> last (map2 (\<and>) bs cs) \<longleftrightarrow> (bs \<noteq> [] \<and> last bs) \<and> (cs \<noteq> [] \<and> last cs)\<close>
-      and \<open>zip bs cs \<noteq> [] \<and> last (map2 (\<or>) bs cs) \<longleftrightarrow> (bs \<noteq> [] \<and> last bs) \<or> (cs \<noteq> [] \<and> last cs)\<close>
-      and \<open>zip bs cs \<noteq> [] \<and> last (map2 (\<noteq>) bs cs) \<longleftrightarrow> ((bs \<noteq> [] \<and> last bs) \<noteq> (cs \<noteq> [] \<and> last cs))\<close>
-      by (auto simp add: last_map last_zip zip_eq_Nil_iff prod_eq_iff)
-    then show \<open>of_bits bs AND of_bits cs = (of_bits (map2 (\<and>) bs cs) :: int)\<close>
-      and \<open>of_bits bs OR of_bits cs = (of_bits (map2 (\<or>) bs cs) :: int)\<close>
-      and \<open>of_bits bs XOR of_bits cs = (of_bits (map2 (\<noteq>) bs cs) :: int)\<close>
-      by (simp_all add: fun_eq_iff bit_eq_iff bit_and_iff bit_or_iff bit_xor_iff bit_not_iff bit_of_bits_int_iff \<open>length bs = length cs\<close> nth_default_map2 [of bs cs _ \<open>bs \<noteq> [] \<and> last bs\<close> \<open>cs \<noteq> [] \<and> last cs\<close>])
-  }
-  show \<open>push_bit n k = of_bits (replicate n False @ bits_of k)\<close>
-    for k :: int and n :: nat
-    by (cases "n = 0") simp_all
-  show \<open>drop_bit n k = of_bits (drop n (bits_of k))\<close>
-    if \<open>n < length (bits_of k)\<close> for k :: int and n :: nat
-    using that by simp
-  show \<open>(not :: int \<Rightarrow> _) = of_bits \<circ> map Not \<circ> bits_of\<close>
-  proof (rule sym, rule ext)
-    fix k :: int
-    show \<open>(of_bits \<circ> map Not \<circ> bits_of) k = NOT k\<close>
-      by (induction k rule: int_bit_induct) (simp_all add: not_int_def)
-  qed
-qed
-
-end

--- a/src/Tools/Haskell/Haskell.thy	Tue Aug 03 10:14:48 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Wed Aug 04 08:27:16 2021 +0200
@@ -1521,9 +1521,9 @@
     Name, T, names, none, make, markup_element, markup_report, make_report
   ) where
 
-import Isabelle.Library
 import qualified Isabelle.Bytes as Bytes
-import Isabelle.Bytes (Bytes)
+import qualified Isabelle.Name as Name
+import Isabelle.Name (Name)
 import qualified Isabelle.Properties as Properties
 import qualified Isabelle.Markup as Markup
 import qualified Isabelle.XML.Encode as Encode
@@ -1531,26 +1531,19 @@
 import qualified Isabelle.YXML as YXML
 
 
-type Name = (Bytes, (Bytes, Bytes))  -- external name, kind, internal name
-data T = Completion Properties.T Int [Name]  -- position, total length, names
-
-names :: Int -> Properties.T -> [Name] -> T
+type Names = [(Name, (Name, Name))]  -- external name, kind, internal name
+data T = Completion Properties.T Int Names  -- position, total length, names
+
+names :: Int -> Properties.T -> Names -> T
 names limit props names = Completion props (length names) (take limit names)
 
 none :: T
 none = names 0 [] []
 
-clean_name :: Bytes -> Bytes
-clean_name bs =
-  if not (Bytes.null bs) && Bytes.last bs == u then
-    Bytes.unpack bs |> reverse |> dropWhile (== u) |> reverse |> Bytes.pack
-  else bs
-  where u = Bytes.byte '_'
-
-make :: Int -> (Bytes, Properties.T) -> ((Bytes -> Bool) -> [Name]) -> T
+make :: Int -> (Name, Properties.T) -> ((Name -> Bool) -> Names) -> T
 make limit (name, props) make_names =
   if name /= "" && name /= "_" then
-    names limit props (make_names (Bytes.isPrefixOf (clean_name name)))
+    names limit props (make_names (Bytes.isPrefixOf (Name.clean name)))
   else none
 
 markup_element :: T -> (Markup.T, XML.Body)
@@ -1565,12 +1558,12 @@
     in (markup, body)
   else (Markup.empty, [])
 
-markup_report :: [T] -> Bytes
+markup_report :: [T] -> Name
 markup_report [] = Bytes.empty
 markup_report elems =
   YXML.string_of $ XML.Elem (Markup.report, map (XML.Elem . markup_element) elems)
 
-make_report :: Int -> (Bytes, Properties.T) -> ((Bytes -> Bool) -> [Name]) -> Bytes
+make_report :: Int -> (Name, Properties.T) -> ((Name -> Bool) -> Names) -> Name
 make_report limit name_props make_names =
   markup_report [make limit name_props make_names]
 \<close>
@@ -1760,6 +1753,100 @@
 big_list name prts = block (fbreaks (str name : prts))
 \<close>
 
+generate_file "Isabelle/Name.hs" = \<open>
+{-  Title:      Isabelle/Name.hs
+    Author:     Makarius
+
+Names of basic logical entities (variables etc.).
+
+See also \<^file>\<open>$ISABELLE_HOME/src/Pure/name.ML\<close>.
+-}
+
+{-# LANGUAGE OverloadedStrings #-}
+
+module Isabelle.Name (
+  Name, clean_index, clean,
+  Context, declare, is_declared, context, make_context, variant
+)
+where
+
+import Data.Word (Word8)
+import qualified Data.Set as Set
+import Data.Set (Set)
+import qualified Isabelle.Bytes as Bytes
+import Isabelle.Bytes (Bytes)
+import qualified Isabelle.Symbol as Symbol
+import Isabelle.Library
+
+
+type Name = Bytes
+
+
+{- suffix for internal names -}
+
+underscore :: Word8
+underscore = Bytes.byte '_'
+
+clean_index :: Name -> (Name, Int)
+clean_index x =
+  if Bytes.null x || Bytes.last x /= underscore then (x, 0)
+  else
+    let
+      rev = reverse (Bytes.unpack x)
+      n = length (takeWhile (== underscore) rev)
+      y = Bytes.pack (reverse (drop n rev))
+    in (y, n)
+
+clean :: Name -> Name
+clean = fst . clean_index
+
+
+{- context for used names -}
+
+data Context = Context (Set Name)
+
+declare :: Name -> Context -> Context
+declare x (Context names) = Context (Set.insert x names)
+
+is_declared :: Context -> Name -> Bool
+is_declared (Context names) x = Set.member x names
+
+context :: Context
+context = Context (Set.fromList ["", "'"])
+
+make_context :: [Name] -> Context
+make_context used = fold declare used context
+
+
+{- generating fresh names -}
+
+bump_init :: Name -> Name
+bump_init str = str <> "a"
+
+bump_string :: Name -> Name
+bump_string str =
+  let
+    a = Bytes.byte 'a'
+    z = Bytes.byte 'z'
+    bump (b : bs) | b == z = a : bump bs
+    bump (b : bs) | a <= b && b < z = b + 1 : bs
+    bump bs = a : bs
+
+    rev = reverse (Bytes.unpack str)
+    part2 = reverse (takeWhile (Symbol.is_ascii_quasi . Bytes.char) rev)
+    part1 = reverse (bump (drop (length part2) rev))
+  in Bytes.pack (part1 <> part2)
+
+variant :: Name -> Context -> (Name, Context)
+variant name names =
+  let
+    vary bump x = if is_declared names x then bump x |> vary bump_string else x
+    (x, n) = clean_index name
+    x' = x |> vary bump_init
+    names' = declare x' names;
+  in (x' <> Bytes.pack (replicate n underscore), names')
+\<close>
+
 generate_file "Isabelle/Term.hs" = \<open>
 {-  Title:      Isabelle/Term.hs
     Author:     Makarius
@@ -1773,14 +1860,17 @@
 {-# LANGUAGE OverloadedStrings #-}
 
 module Isabelle.Term (
-  Name, Indexname, Sort, Typ(..), Term(..), Free,
+  Indexname, Sort, Typ(..), Term(..),
+  Free, lambda, declare_frees, incr_boundvars, subst_bound, dest_abs,
   type_op0, type_op1, op0, op1, op2, typed_op2, binder,
   dummyS, dummyT, is_dummyT, propT, is_propT, (-->), dest_funT, (--->),
-  aconv, list_comb, strip_comb, head_of, lambda
+  aconv, list_comb, strip_comb, head_of
 )
 where
 
-import Isabelle.Bytes (Bytes)
+import Isabelle.Library
+import qualified Isabelle.Name as Name
+import Isabelle.Name (Name)
 
 infixr 5 -->
 infixr --->
@@ -1788,8 +1878,6 @@
 
 {- types and terms -}
 
-type Name = Bytes
-
 type Indexname = (Name, Int)
 
 type Sort = [Name]
@@ -1809,8 +1897,52 @@
   | App (Term, Term)
   deriving (Show, Eq, Ord)
 
+
+{- free and bound variables -}
+
 type Free = (Name, Typ)
 
+lambda :: Free -> Term -> Term
+lambda (name, typ) body = Abs (name, typ, abstract 0 body)
+  where
+    abstract lev (Free (x, ty)) | name == x && typ == ty = Bound lev
+    abstract lev (Abs (a, ty, t)) = Abs (a, ty, abstract (lev + 1) t)
+    abstract lev (App (t, u)) = App (abstract lev t, abstract lev u)
+    abstract _ t = t
+
+declare_frees :: Term -> Name.Context -> Name.Context
+declare_frees (Free (x, _)) = Name.declare x
+declare_frees (Abs (_, _, b)) = declare_frees b
+declare_frees (App (t, u)) = declare_frees t #> declare_frees u
+declare_frees _ = id
+
+incr_boundvars :: Int -> Term -> Term
+incr_boundvars inc = if inc == 0 then id else incr 0
+  where
+    incr lev (Bound i) = if i >= lev then Bound (i + inc) else Bound i
+    incr lev (Abs (a, ty, b)) = Abs (a, ty, incr (lev + 1) b)
+    incr lev (App (t, u)) = App (incr lev t, incr lev u)
+    incr _ t = t
+
+subst_bound :: Term -> Term -> Term
+subst_bound arg = subst 0
+  where
+    subst lev (Bound i) =
+      if i < lev then Bound i
+      else if i == lev then incr_boundvars lev arg
+      else Bound (i - 1)
+    subst lev (Abs (a, ty, b)) = Abs (a, ty, subst (lev + 1) b)
+    subst lev (App (t, u)) = App (subst lev t, subst lev u)
+    subst _ t = t
+
+dest_abs :: Name.Context -> Term -> Maybe (Free, Term)
+dest_abs names (Abs (x, ty, b)) =
+  let
+    (x', _) = Name.variant x (declare_frees b names)
+    v = (x', ty)
+  in Just (v, subst_bound (Free v) b)
+dest_abs _ _ = Nothing
+
 
 {- type and term operators -}
 
@@ -1906,14 +2038,6 @@
 head_of :: Term -> Term
 head_of (App (f, _)) = head_of f
 head_of u = u
-
-lambda :: Free -> Term -> Term
-lambda (name, typ) body = Abs (name, typ, abstract 0 body)
-  where
-    abstract lev (Free (x, ty)) | name == x && typ == ty = Bound lev
-    abstract lev (Abs (a, ty, t)) = Abs (a, ty, abstract (lev + 1) t)
-    abstract lev (App (t, u)) = App (abstract lev t, abstract lev u)
-    abstract _ t = t
 \<close>
 
 generate_file "Isabelle/Pure.hs" = \<open>