diff -r 74440d820ba5 -r 127ba61b2630 src/HOL/Bit_Operations.thy
--- a/src/HOL/Bit_Operations.thy	Tue Nov 21 19:19:16 2023 +0000
+++ b/src/HOL/Bit_Operations.thy	Tue Nov 21 19:19:16 2023 +0000
@@ -72,9 +72,8 @@
 
 lemma even_succ_mod_exp [simp]:
   \<open>(1 + a) mod 2 ^ n = 1 + (a mod 2 ^ n)\<close> if \<open>even a\<close> and \<open>n > 0\<close>
-  using div_mult_mod_eq [of \<open>1 + a\<close> \<open>2 ^ n\<close>] that
-  apply simp
-  by (metis local.add.left_commute local.add_left_cancel local.div_mult_mod_eq)
+  using div_mult_mod_eq [of \<open>1 + a\<close> \<open>2 ^ n\<close>] div_mult_mod_eq [of a \<open>2 ^ n\<close>] that
+  by simp (metis (full_types) add.left_commute add_left_imp_eq)
 
 lemma bits_mod_by_1 [simp]:
   \<open>a mod 1 = 0\<close>
@@ -155,33 +154,33 @@
   \<open>\<not> bit a n\<close> if \<open>2 ^ n = 0\<close>
   using that by (simp add: bit_iff_odd)
 
-definition
-  possible_bit :: "'a itself \<Rightarrow> nat \<Rightarrow> bool"
-  where
-  "possible_bit tyrep n = (2 ^ n \<noteq> (0 :: 'a))"
-
-lemma possible_bit_0[simp]:
-  "possible_bit ty 0"
+definition possible_bit :: \<open>'a itself \<Rightarrow> nat \<Rightarrow> bool\<close>
+  where \<open>possible_bit TYPE('a) n \<longleftrightarrow> 2 ^ n \<noteq> 0\<close>
+
+lemma possible_bit_0 [simp]:
+  \<open>possible_bit TYPE('a) 0\<close>
   by (simp add: possible_bit_def)
 
 lemma fold_possible_bit:
-  "2 ^ n = (0 :: 'a) \<longleftrightarrow> \<not> possible_bit TYPE('a) n"
+  \<open>2 ^ n = 0 \<longleftrightarrow> \<not> possible_bit TYPE('a) n\<close>
   by (simp add: possible_bit_def)
 
-lemmas impossible_bit = exp_eq_0_imp_not_bit[simplified fold_possible_bit]
-
 lemma bit_imp_possible_bit:
-  "bit a n \<Longrightarrow> possible_bit TYPE('a) n"
-  by (rule ccontr) (simp add: impossible_bit)
+  \<open>possible_bit TYPE('a) n\<close> if \<open>bit a n\<close>
+  using that by (auto simp add: possible_bit_def exp_eq_0_imp_not_bit)
+
+lemma impossible_bit:
+  \<open>\<not> bit a n\<close> if \<open>\<not> possible_bit TYPE('a) n\<close>
+  using that by (blast dest: bit_imp_possible_bit)
 
 lemma possible_bit_less_imp:
-  "possible_bit tyrep i \<Longrightarrow> j \<le> i \<Longrightarrow> possible_bit tyrep j"
-  using power_add[of "2 :: 'a" j "i - j"]
-  by (clarsimp simp: possible_bit_def eq_commute[where a=0])
-
-lemma possible_bit_min[simp]:
-  "possible_bit tyrep (min i j) \<longleftrightarrow> possible_bit tyrep i \<or> possible_bit tyrep j"
-  by (auto simp: min_def elim: possible_bit_less_imp)
+  \<open>possible_bit TYPE('a) j\<close> if \<open>possible_bit TYPE('a) i\<close> \<open>j \<le> i\<close>
+  using power_add [of 2 j \<open>i - j\<close>] that mult_not_zero [of \<open>2 ^ j\<close> \<open>2 ^ (i - j)\<close>]
+  by (simp add: possible_bit_def)
+
+lemma possible_bit_min [simp]:
+  \<open>possible_bit TYPE('a) (min i j) \<longleftrightarrow> possible_bit TYPE('a) i \<or> possible_bit TYPE('a) j\<close>
+  by (auto simp add: min_def elim: possible_bit_less_imp)
 
 lemma bit_eqI:
   \<open>a = b\<close> if \<open>\<And>n. possible_bit TYPE('a) n \<Longrightarrow> bit a n \<longleftrightarrow> bit b n\<close>
@@ -389,32 +388,36 @@
     by simp
 qed
 
+lemma bit_of_bool_iff [bit_simps]:
+  \<open>bit (of_bool b) n \<longleftrightarrow> b \<and> n = 0\<close>
+  by (simp add: bit_1_iff)
+
 end
 
 lemma nat_bit_induct [case_names zero even odd]:
-  "P n" if zero: "P 0"
-    and even: "\<And>n. P n \<Longrightarrow> n > 0 \<Longrightarrow> P (2 * n)"
-    and odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
+  \<open>P n\<close> if zero: \<open>P 0\<close>
+    and even: \<open>\<And>n. P n \<Longrightarrow> n > 0 \<Longrightarrow> P (2 * n)\<close>
+    and odd: \<open>\<And>n. P n \<Longrightarrow> P (Suc (2 * n))\<close>
 proof (induction n rule: less_induct)
   case (less n)
-  show "P n"
-  proof (cases "n = 0")
+  show \<open>P n\<close>
+  proof (cases \<open>n = 0\<close>)
     case True with zero show ?thesis by simp
   next
     case False
-    with less have hyp: "P (n div 2)" by simp
+    with less have hyp: \<open>P (n div 2)\<close> by simp
     show ?thesis
-    proof (cases "even n")
+    proof (cases \<open>even n\<close>)
       case True
-      then have "n \<noteq> 1"
+      then have \<open>n \<noteq> 1\<close>
         by auto
-      with \<open>n \<noteq> 0\<close> have "n div 2 > 0"
+      with \<open>n \<noteq> 0\<close> have \<open>n div 2 > 0\<close>
         by simp
-      with \<open>even n\<close> hyp even [of "n div 2"] show ?thesis
+      with \<open>even n\<close> hyp even [of \<open>n div 2\<close>] show ?thesis
         by simp
     next
       case False
-      with hyp odd [of "n div 2"] show ?thesis
+      with hyp odd [of \<open>n div 2\<close>] show ?thesis
         by simp
     qed
   qed
@@ -466,8 +469,8 @@
 
 end
 
-lemma possible_bit_nat[simp]:
-  "possible_bit TYPE(nat) n"
+lemma possible_bit_nat [simp]:
+  \<open>possible_bit TYPE(nat) n\<close>
   by (simp add: possible_bit_def)
 
 lemma not_bit_Suc_0_Suc [simp]:
@@ -478,70 +481,9 @@
   \<open>\<not> bit (Suc 0) (numeral n)\<close>
   by (simp add: numeral_eq_Suc)
 
-lemma int_bit_induct [case_names zero minus even odd]:
-  "P k" if zero_int: "P 0"
-    and minus_int: "P (- 1)"
-    and even_int: "\<And>k. P k \<Longrightarrow> k \<noteq> 0 \<Longrightarrow> P (k * 2)"
-    and odd_int: "\<And>k. P k \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> P (1 + (k * 2))" for k :: int
-proof (cases "k \<ge> 0")
-  case True
-  define n where "n = nat k"
-  with True have "k = int n"
-    by simp
-  then show "P k"
-  proof (induction n arbitrary: k rule: nat_bit_induct)
-    case zero
-    then show ?case
-      by (simp add: zero_int)
-  next
-    case (even n)
-    have "P (int n * 2)"
-      by (rule even_int) (use even in simp_all)
-    with even show ?case
-      by (simp add: ac_simps)
-  next
-    case (odd n)
-    have "P (1 + (int n * 2))"
-      by (rule odd_int) (use odd in simp_all)
-    with odd show ?case
-      by (simp add: ac_simps)
-  qed
-next
-  case False
-  define n where "n = nat (- k - 1)"
-  with False have "k = - int n - 1"
-    by simp
-  then show "P k"
-  proof (induction n arbitrary: k rule: nat_bit_induct)
-    case zero
-    then show ?case
-      by (simp add: minus_int)
-  next
-    case (even n)
-    have "P (1 + (- int (Suc n) * 2))"
-      by (rule odd_int) (use even in \<open>simp_all add: algebra_simps\<close>)
-    also have "\<dots> = - int (2 * n) - 1"
-      by (simp add: algebra_simps)
-    finally show ?case
-      using even.prems by simp
-  next
-    case (odd n)
-    have "P (- int (Suc n) * 2)"
-      by (rule even_int) (use odd in \<open>simp_all add: algebra_simps\<close>)
-    also have "\<dots> = - int (Suc (2 * n)) - 1"
-      by (simp add: algebra_simps)
-    finally show ?case
-      using odd.prems by simp
-  qed
-qed
-
 context semiring_bits
 begin
 
-lemma bit_of_bool_iff [bit_simps]:
-  \<open>bit (of_bool b) n \<longleftrightarrow> b \<and> n = 0\<close>
-  by (simp add: bit_1_iff)
-
 lemma bit_of_nat_iff [bit_simps]:
   \<open>bit (of_nat m) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> bit m n\<close>
 proof (cases \<open>(2::'a) ^ n = 0\<close>)
@@ -573,6 +515,63 @@
 
 end
 
+lemma int_bit_induct [case_names zero minus even odd]:
+  \<open>P k\<close> if zero_int: \<open>P 0\<close>
+    and minus_int: \<open>P (- 1)\<close>
+    and even_int: \<open>\<And>k. P k \<Longrightarrow> k \<noteq> 0 \<Longrightarrow> P (k * 2)\<close>
+    and odd_int: \<open>\<And>k. P k \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> P (1 + (k * 2))\<close> for k :: int
+proof (cases \<open>k \<ge> 0\<close>)
+  case True
+  define n where \<open>n = nat k\<close>
+  with True have \<open>k = int n\<close>
+    by simp
+  then show \<open>P k\<close>
+  proof (induction n arbitrary: k rule: nat_bit_induct)
+    case zero
+    then show ?case
+      by (simp add: zero_int)
+  next
+    case (even n)
+    have \<open>P (int n * 2)\<close>
+      by (rule even_int) (use even in simp_all)
+    with even show ?case
+      by (simp add: ac_simps)
+  next
+    case (odd n)
+    have \<open>P (1 + (int n * 2))\<close>
+      by (rule odd_int) (use odd in simp_all)
+    with odd show ?case
+      by (simp add: ac_simps)
+  qed
+next
+  case False
+  define n where \<open>n = nat (- k - 1)\<close>
+  with False have \<open>k = - int n - 1\<close>
+    by simp
+  then show \<open>P k\<close>
+  proof (induction n arbitrary: k rule: nat_bit_induct)
+    case zero
+    then show ?case
+      by (simp add: minus_int)
+  next
+    case (even n)
+    have \<open>P (1 + (- int (Suc n) * 2))\<close>
+      by (rule odd_int) (use even in \<open>simp_all add: algebra_simps\<close>)
+    also have \<open>\<dots> = - int (2 * n) - 1\<close>
+      by (simp add: algebra_simps)
+    finally show ?case
+      using even.prems by simp
+  next
+    case (odd n)
+    have \<open>P (- int (Suc n) * 2)\<close>
+      by (rule even_int) (use odd in \<open>simp_all add: algebra_simps\<close>)
+    also have \<open>\<dots> = - int (Suc (2 * n)) - 1\<close>
+      by (simp add: algebra_simps)
+    finally show ?case
+      using odd.prems by simp
+  qed
+qed
+
 instantiation int :: semiring_bits
 begin
 
@@ -644,13 +643,12 @@
 
 end
 
-lemma possible_bit_int[simp]:
-  "possible_bit TYPE(int) n"
+lemma possible_bit_int [simp]:
+  \<open>possible_bit TYPE(int) n\<close>
   by (simp add: possible_bit_def)
 
 lemma bit_not_int_iff':
-  \<open>bit (- k - 1) n \<longleftrightarrow> \<not> bit k n\<close>
-  for k :: int
+  \<open>bit (- k - 1) n \<longleftrightarrow> \<not> bit k n\<close> for k :: int
 proof (induction n arbitrary: k)
   case 0
   show ?case
@@ -857,35 +855,35 @@
   by (simp add: push_bit_eq_mult drop_bit_eq_div)
 
 lemma bits_ident:
-  "push_bit n (drop_bit n a) + take_bit n a = a"
+  \<open>push_bit n (drop_bit n a) + take_bit n a = a\<close>
   using div_mult_mod_eq by (simp add: push_bit_eq_mult take_bit_eq_mod drop_bit_eq_div)
 
 lemma push_bit_push_bit [simp]:
-  "push_bit m (push_bit n a) = push_bit (m + n) a"
+  \<open>push_bit m (push_bit n a) = push_bit (m + n) a\<close>
   by (simp add: push_bit_eq_mult power_add ac_simps)
 
 lemma push_bit_0_id [simp]:
-  "push_bit 0 = id"
+  \<open>push_bit 0 = id\<close>
   by (simp add: fun_eq_iff push_bit_eq_mult)
 
 lemma push_bit_of_0 [simp]:
-  "push_bit n 0 = 0"
+  \<open>push_bit n 0 = 0\<close>
   by (simp add: push_bit_eq_mult)
 
 lemma push_bit_of_1 [simp]:
-  "push_bit n 1 = 2 ^ n"
+  \<open>push_bit n 1 = 2 ^ n\<close>
   by (simp add: push_bit_eq_mult)
 
 lemma push_bit_Suc [simp]:
-  "push_bit (Suc n) a = push_bit n (a * 2)"
+  \<open>push_bit (Suc n) a = push_bit n (a * 2)\<close>
   by (simp add: push_bit_eq_mult ac_simps)
 
 lemma push_bit_double:
-  "push_bit n (a * 2) = push_bit n a * 2"
+  \<open>push_bit n (a * 2) = push_bit n a * 2\<close>
   by (simp add: push_bit_eq_mult ac_simps)
 
 lemma push_bit_add:
-  "push_bit n (a + b) = push_bit n a + push_bit n b"
+  \<open>push_bit n (a + b) = push_bit n a + push_bit n b\<close>
   by (simp add: push_bit_eq_mult algebra_simps)
 
 lemma push_bit_numeral [simp]:
@@ -916,39 +914,39 @@
   by (simp add: take_bit_eq_mod)
 
 lemma take_bit_of_0 [simp]:
-  "take_bit n 0 = 0"
+  \<open>take_bit n 0 = 0\<close>
   by (simp add: take_bit_eq_mod)
 
 lemma take_bit_of_1 [simp]:
-  "take_bit n 1 = of_bool (n > 0)"
+  \<open>take_bit n 1 = of_bool (n > 0)\<close>
   by (cases n) (simp_all add: take_bit_Suc)
 
 lemma drop_bit_of_0 [simp]:
-  "drop_bit n 0 = 0"
+  \<open>drop_bit n 0 = 0\<close>
   by (simp add: drop_bit_eq_div)
 
 lemma drop_bit_of_1 [simp]:
-  "drop_bit n 1 = of_bool (n = 0)"
+  \<open>drop_bit n 1 = of_bool (n = 0)\<close>
   by (simp add: drop_bit_eq_div)
 
 lemma drop_bit_0 [simp]:
-  "drop_bit 0 = id"
+  \<open>drop_bit 0 = id\<close>
   by (simp add: fun_eq_iff drop_bit_eq_div)
 
 lemma drop_bit_Suc:
-  "drop_bit (Suc n) a = drop_bit n (a div 2)"
+  \<open>drop_bit (Suc n) a = drop_bit n (a div 2)\<close>
   using div_exp_eq [of a 1] by (simp add: drop_bit_eq_div)
 
 lemma drop_bit_rec:
-  "drop_bit n a = (if n = 0 then a else drop_bit (n - 1) (a div 2))"
+  \<open>drop_bit n a = (if n = 0 then a else drop_bit (n - 1) (a div 2))\<close>
   by (cases n) (simp_all add: drop_bit_Suc)
 
 lemma drop_bit_half:
-  "drop_bit n (a div 2) = drop_bit n a div 2"
+  \<open>drop_bit n (a div 2) = drop_bit n a div 2\<close>
   by (induction n arbitrary: a) (simp_all add: drop_bit_Suc)
 
 lemma drop_bit_of_bool [simp]:
-  "drop_bit n (of_bool b) = of_bool (n = 0 \<and> b)"
+  \<open>drop_bit n (of_bool b) = of_bool (n = 0 \<and> b)\<close>
   by (cases n) simp_all
 
 lemma even_take_bit_eq [simp]:
@@ -956,22 +954,22 @@
   by (simp add: take_bit_rec [of n a])
 
 lemma take_bit_take_bit [simp]:
-  "take_bit m (take_bit n a) = take_bit (min m n) a"
+  \<open>take_bit m (take_bit n a) = take_bit (min m n) a\<close>
   by (simp add: take_bit_eq_mod mod_exp_eq ac_simps)
 
 lemma drop_bit_drop_bit [simp]:
-  "drop_bit m (drop_bit n a) = drop_bit (m + n) a"
+  \<open>drop_bit m (drop_bit n a) = drop_bit (m + n) a\<close>
   by (simp add: drop_bit_eq_div power_add div_exp_eq ac_simps)
 
 lemma push_bit_take_bit:
-  "push_bit m (take_bit n a) = take_bit (m + n) (push_bit m a)"
+  \<open>push_bit m (take_bit n a) = take_bit (m + n) (push_bit m a)\<close>
   apply (simp add: push_bit_eq_mult take_bit_eq_mod power_add ac_simps)
   using mult_exp_mod_exp_eq [of m \<open>m + n\<close> a] apply (simp add: ac_simps power_add)
   done
 
 lemma take_bit_push_bit:
-  "take_bit m (push_bit n a) = push_bit n (take_bit (m - n) a)"
-proof (cases "m \<le> n")
+  \<open>take_bit m (push_bit n a) = push_bit n (take_bit (m - n) a)\<close>
+proof (cases \<open>m \<le> n\<close>)
   case True
   then show ?thesis
     apply (simp add:)
@@ -983,16 +981,16 @@
 next
   case False
   then show ?thesis
-    using push_bit_take_bit [of n "m - n" a]
+    using push_bit_take_bit [of n \<open>m - n\<close> a]
     by simp
 qed
 
 lemma take_bit_drop_bit:
-  "take_bit m (drop_bit n a) = drop_bit n (take_bit (m + n) a)"
+  \<open>take_bit m (drop_bit n a) = drop_bit n (take_bit (m + n) a)\<close>
   by (simp add: drop_bit_eq_div take_bit_eq_mod ac_simps div_exp_mod_exp_eq)
 
 lemma drop_bit_take_bit:
-  "drop_bit m (take_bit n a) = take_bit (n - m) (drop_bit m a)"
+  \<open>drop_bit m (take_bit n a) = take_bit (n - m) (drop_bit m a)\<close>
 proof (cases "m \<le> n")
   case True
   then show ?thesis
@@ -1197,11 +1195,9 @@
   apply (simp_all add: bit_exp_iff)
   done
 
-lemmas set_bit_def = set_bit_eq_or
-
 lemma bit_set_bit_iff [bit_simps]:
   \<open>bit (set_bit m a) n \<longleftrightarrow> bit a n \<or> (m = n \<and> possible_bit TYPE('a) n)\<close>
-  by (auto simp add: set_bit_def bit_or_iff bit_exp_iff)
+  by (auto simp add: set_bit_eq_or bit_or_iff bit_exp_iff)
 
 lemma even_set_bit_iff:
   \<open>even (set_bit m a) \<longleftrightarrow> even a \<and> m \<noteq> 0\<close>
@@ -1216,8 +1212,6 @@
   using bit_imp_possible_bit[of a n]
   by (auto simp add: bit_eq_iff bit_simps)
 
-lemmas flip_bit_def = flip_bit_eq_xor
-
 lemma bit_flip_bit_iff [bit_simps]:
   \<open>bit (flip_bit m a) n \<longleftrightarrow> (m = n \<longleftrightarrow> \<not> bit a n) \<and> possible_bit TYPE('a) n\<close>
   by (auto simp add: bit_eq_iff bit_simps flip_bit_eq_xor bit_imp_possible_bit)
@@ -1295,6 +1289,44 @@
   \<open>mask n = 0 \<longleftrightarrow> n = 0\<close>
   by (cases n) (simp_all add: mask_Suc_double or_eq_0_iff)
 
+lemma bit_horner_sum_bit_iff [bit_simps]:
+  \<open>bit (horner_sum of_bool 2 bs) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> n < length bs \<and> bs ! n\<close>
+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 add: bit_0)
+  next
+    case (Suc m)
+    with bit_rec [of _ n] Cons.prems Cons.IH [of m]
+    show ?thesis
+      by (simp add: bit_simps)
+        (auto simp add: possible_bit_less_imp bit_simps simp flip: bit_Suc)
+  qed
+qed
+
+lemma horner_sum_bit_eq_take_bit:
+  \<open>horner_sum of_bool 2 (map (bit a) [0..<n]) = take_bit n a\<close>
+  by (rule bit_eqI) (auto simp add: bit_simps)
+
+lemma take_bit_horner_sum_bit_eq:
+  \<open>take_bit n (horner_sum of_bool 2 bs) = horner_sum of_bool 2 (take n bs)\<close>
+  by (auto simp add: bit_eq_iff bit_take_bit_iff bit_horner_sum_bit_iff)
+
+lemma take_bit_sum:
+  \<open>take_bit n a = (\<Sum>k = 0..<n. push_bit k (of_bool (bit a k)))\<close>
+  by (simp flip: horner_sum_bit_eq_take_bit add: horner_sum_eq_sum push_bit_eq_mult)
+
+lemmas set_bit_def = set_bit_eq_or
+
+lemmas flip_bit_def = flip_bit_eq_xor
+
 end
 
 class ring_bit_operations = semiring_bit_operations + ring_parity +
@@ -1303,8 +1335,6 @@
   assumes minus_eq_not_minus_1: \<open>- a = NOT (a - 1)\<close>
 begin
 
-lemmas bit_not_iff[bit_simps] = bit_not_iff_eq[unfolded fold_possible_bit]
-
 text \<open>
   For the sake of code generation \<^const>\<open>not\<close> is specified as
   definitional class operation.  Note that \<^const>\<open>not\<close> has no
@@ -1312,6 +1342,10 @@
   (type \<^typ>\<open>nat\<close>).
 \<close>
 
+lemma bit_not_iff [bit_simps]:
+  \<open>bit (NOT a) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> \<not> bit a n\<close>
+  by (simp add: bit_not_iff_eq fold_possible_bit)
+
 lemma bits_minus_1_mod_2_eq [simp]:
   \<open>(- 1) mod 2 = 1\<close>
   by (simp add: mod_2_eq_odd)
@@ -1448,8 +1482,6 @@
   \<open>unset_bit n a = a AND NOT (push_bit n 1)\<close>
   by (rule bit_eqI) (auto simp add: bit_simps)
 
-lemmas unset_bit_def = unset_bit_eq_and_not
-
 lemma push_bit_Suc_minus_numeral [simp]:
   \<open>push_bit (Suc n) (- numeral k) = push_bit n (- numeral (Num.Bit0 k))\<close>
   apply (simp only: numeral_Bit0)
@@ -1486,6 +1518,8 @@
   \<open>push_bit (numeral n) (- 1) = - (2 ^ numeral n)\<close>
   by (simp add: push_bit_eq_mult)
 
+lemmas unset_bit_def = unset_bit_eq_and_not
+
 end
 
 
@@ -1521,27 +1555,15 @@
   by auto
 
 termination proof (relation \<open>measure (\<lambda>(k, l). nat (\<bar>k\<bar> + \<bar>l\<bar>))\<close>)
+  have less_eq: \<open>\<bar>k div 2\<bar> \<le> \<bar>k\<bar>\<close> for k :: int
+    by (cases k) (simp_all add: divide_int_def nat_add_distrib)
+  then have less: \<open>\<bar>k div 2\<bar> < \<bar>k\<bar>\<close> if \<open>k \<notin> {0, - 1}\<close> for k :: int
+    using that by (auto simp add: less_le [of k])
   show \<open>wf (measure (\<lambda>(k, l). nat (\<bar>k\<bar> + \<bar>l\<bar>)))\<close>
     by simp
   show \<open>((k div 2, l div 2), k, l) \<in> measure (\<lambda>(k, l). nat (\<bar>k\<bar> + \<bar>l\<bar>))\<close>
     if \<open>\<not> (k \<in> {0, - 1} \<and> l \<in> {0, - 1})\<close> for k l
   proof -
-    have less_eq: \<open>\<bar>k div 2\<bar> \<le> \<bar>k\<bar>\<close> for k :: int
-      by (cases k) (simp_all add: divide_int_def nat_add_distrib)
-    have less: \<open>\<bar>k div 2\<bar> < \<bar>k\<bar>\<close> if \<open>k \<notin> {0, - 1}\<close> for k :: int
-    proof (cases k)
-      case (nonneg n)
-      with that show ?thesis
-        by (simp add: int_div_less_self)
-    next
-      case (neg n)
-      with that have \<open>n \<noteq> 0\<close>
-        by simp
-      then have \<open>n div 2 < n\<close>
-        by (simp add: div_less_iff_less_mult)
-      with neg that show ?thesis
-        by (simp add: divide_int_def nat_add_distrib)
-    qed
     from that have *: \<open>k \<notin> {0, - 1} \<or> l \<notin> {0, - 1}\<close>
       by simp
     then have \<open>0 < \<bar>k\<bar> + \<bar>l\<bar>\<close>
@@ -1813,10 +1835,8 @@
   by (subst Not_eq_iff [symmetric]) (auto simp add: not_less)
 
 lemma OR_upper: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
-  fixes x y :: int
-  assumes \<open>0 \<le> x\<close> \<open>x < 2 ^ n\<close> \<open>y < 2 ^ n\<close>
-  shows \<open>x OR y < 2 ^ n\<close>
-using assms proof (induction x arbitrary: y n rule: int_bit_induct)
+  \<open>x OR y < 2 ^ n\<close> if \<open>0 \<le> x\<close> \<open>x < 2 ^ n\<close> \<open>y < 2 ^ n\<close> for x y :: int
+using that proof (induction x arbitrary: y n rule: int_bit_induct)
   case zero
   then show ?case
     by simp
@@ -1837,10 +1857,8 @@
 qed
 
 lemma XOR_upper: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
-  fixes x y :: int
-  assumes \<open>0 \<le> x\<close> \<open>x < 2 ^ n\<close> \<open>y < 2 ^ n\<close>
-  shows \<open>x XOR y < 2 ^ n\<close>
-using assms proof (induction x arbitrary: y n rule: int_bit_induct)
+  \<open>x XOR y < 2 ^ n\<close> if \<open>0 \<le> x\<close> \<open>x < 2 ^ n\<close> \<open>y < 2 ^ n\<close> for x y :: int
+using that proof (induction x arbitrary: y n rule: int_bit_induct)
   case zero
   then show ?case
     by simp
@@ -1861,28 +1879,20 @@
 qed
 
 lemma AND_lower [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
-  fixes x y :: int
-  assumes \<open>0 \<le> x\<close>
-  shows \<open>0 \<le> x AND y\<close>
-  using assms by simp
+  \<open>0 \<le> x AND y\<close> if \<open>0 \<le> x\<close> for x y :: int
+  using that by simp
 
 lemma OR_lower [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
-  fixes x y :: int
-  assumes \<open>0 \<le> x\<close> \<open>0 \<le> y\<close>
-  shows \<open>0 \<le> x OR y\<close>
-  using assms by simp
+  \<open>0 \<le> x OR y\<close> if \<open>0 \<le> x\<close> \<open>0 \<le> y\<close> for x y :: int
+  using that by simp
 
 lemma XOR_lower [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
-  fixes x y :: int
-  assumes \<open>0 \<le> x\<close> \<open>0 \<le> y\<close>
-  shows \<open>0 \<le> x XOR y\<close>
-  using assms by simp
+  \<open>0 \<le> x XOR y\<close> if \<open>0 \<le> x\<close> \<open>0 \<le> y\<close> for x y :: int
+  using that by simp
 
 lemma AND_upper1 [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
-  fixes x y :: int
-  assumes \<open>0 \<le> x\<close>
-  shows \<open>x AND y \<le> x\<close>
-using assms proof (induction x arbitrary: y rule: int_bit_induct)
+  \<open>x AND y \<le> x\<close> if \<open>0 \<le> x\<close> for x y :: int
+using that proof (induction x arbitrary: y rule: int_bit_induct)
   case (odd k)
   then have \<open>k AND y div 2 \<le> k\<close>
     by simp
@@ -1890,19 +1900,28 @@
     by (simp add: and_int_rec [of \<open>1 + _ * 2\<close>])
 qed (simp_all add: and_int_rec [of \<open>_ * 2\<close>])
 
-lemmas AND_upper1' [simp] = order_trans [OF AND_upper1] \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
-lemmas AND_upper1'' [simp] = order_le_less_trans [OF AND_upper1] \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
+lemma AND_upper1' [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
+  \<open>y AND x \<le> z\<close> if \<open>0 \<le> y\<close> \<open>y \<le> z\<close> for x y z :: int
+  using _ \<open>y \<le> z\<close> by (rule order_trans) (use \<open>0 \<le> y\<close> in simp)
+
+lemma AND_upper1'' [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
+  \<open>y AND x < z\<close> if \<open>0 \<le> y\<close> \<open>y < z\<close> for x y z :: int
+  using _ \<open>y < z\<close> by (rule order_le_less_trans) (use \<open>0 \<le> y\<close> in simp)
 
 lemma AND_upper2 [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
-  fixes x y :: int
-  assumes \<open>0 \<le> y\<close>
-  shows \<open>x AND y \<le> y\<close>
-  using assms AND_upper1 [of y x] by (simp add: ac_simps)
-
-lemmas AND_upper2' [simp] = order_trans [OF AND_upper2] \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
-lemmas AND_upper2'' [simp] = order_le_less_trans [OF AND_upper2] \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
-
-lemma plus_and_or: \<open>(x AND y) + (x OR y) = x + y\<close> for x y :: int
+  \<open>x AND y \<le> y\<close> if \<open>0 \<le> y\<close> for x y :: int
+  using that AND_upper1 [of y x] by (simp add: ac_simps)
+
+lemma AND_upper2' [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
+  \<open>x AND y \<le> z\<close> if \<open>0 \<le> y\<close> \<open>y \<le> z\<close> for x y :: int
+  using that AND_upper1' [of y z x] by (simp add: ac_simps)
+
+lemma AND_upper2'' [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
+  \<open>x AND y < z\<close> if \<open>0 \<le> y\<close> \<open>y < z\<close> for x y :: int
+  using that AND_upper1'' [of y z x] by (simp add: ac_simps)
+
+lemma plus_and_or:
+  \<open>(x AND y) + (x OR y) = x + y\<close> for x y :: int
 proof (induction x arbitrary: y rule: int_bit_induct)
   case zero
   then show ?case
@@ -1924,7 +1943,7 @@
 qed
 
 lemma push_bit_minus_one:
-  "push_bit n (- 1 :: int) = - (2 ^ n)"
+  \<open>push_bit n (- 1 :: int) = - (2 ^ n)\<close>
   by (simp add: push_bit_eq_mult)
 
 lemma minus_1_div_exp_eq_int:
@@ -2103,13 +2122,11 @@
   by (auto simp add: xor_int_rec [of k l] not_int_def elim!: oddE)
 
 lemma bit_minus_int_iff:
-  \<open>bit (- k) n \<longleftrightarrow> bit (NOT (k - 1)) n\<close>
-  for k :: int
+  \<open>bit (- k) n \<longleftrightarrow> bit (NOT (k - 1)) n\<close> for k :: int
   by (simp add: bit_simps)
 
 lemma take_bit_incr_eq:
-  \<open>take_bit n (k + 1) = 1 + take_bit n k\<close> if \<open>take_bit n k \<noteq> 2 ^ n - 1\<close>
-  for k :: int
+  \<open>take_bit n (k + 1) = 1 + take_bit n k\<close> if \<open>take_bit n k \<noteq> 2 ^ n - 1\<close> for k :: int
 proof -
   from that have \<open>2 ^ n \<noteq> k mod 2 ^ n + 1\<close>
     by (simp add: take_bit_eq_mod)
@@ -2127,8 +2144,7 @@
 qed
 
 lemma take_bit_decr_eq:
-  \<open>take_bit n (k - 1) = take_bit n k - 1\<close> if \<open>take_bit n k \<noteq> 0\<close>
-  for k :: int
+  \<open>take_bit n (k - 1) = take_bit n k - 1\<close> if \<open>take_bit n k \<noteq> 0\<close> for k :: int
 proof -
   from that have \<open>k mod 2 ^ n \<noteq> 0\<close>
     by (simp add: take_bit_eq_mod)
@@ -2173,8 +2189,7 @@
   by (simp add: take_bit_eq_mod)
 
 lemma take_bit_int_less_eq_self_iff:
-  \<open>take_bit n k \<le> k \<longleftrightarrow> 0 \<le> k\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
-  for k :: int
+  \<open>take_bit n k \<le> k \<longleftrightarrow> 0 \<le> k\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>) for k :: int
 proof
   assume ?P
   show ?Q
@@ -2195,19 +2210,16 @@
 qed
 
 lemma take_bit_int_less_self_iff:
-  \<open>take_bit n k < k \<longleftrightarrow> 2 ^ n \<le> k\<close>
-  for k :: int
+  \<open>take_bit n k < k \<longleftrightarrow> 2 ^ n \<le> k\<close> for k :: int
   by (auto simp add: less_le take_bit_int_less_eq_self_iff take_bit_int_eq_self_iff
     intro: order_trans [of 0 \<open>2 ^ n\<close> k])
 
 lemma take_bit_int_greater_self_iff:
-  \<open>k < take_bit n k \<longleftrightarrow> k < 0\<close>
-  for k :: int
+  \<open>k < take_bit n k \<longleftrightarrow> k < 0\<close> for k :: int
   using take_bit_int_less_eq_self_iff [of n k] by auto
 
 lemma take_bit_int_greater_eq_self_iff:
-  \<open>k \<le> take_bit n k \<longleftrightarrow> k < 2 ^ n\<close>
-  for k :: int
+  \<open>k \<le> take_bit n k \<longleftrightarrow> k < 2 ^ n\<close> for k :: int
   by (auto simp add: le_less take_bit_int_greater_self_iff take_bit_int_eq_self_iff
     dest: sym not_sym intro: less_trans [of k 0 \<open>2 ^ n\<close>])
 
@@ -2431,12 +2443,11 @@
 end
 
 lemma take_bit_nat_less_exp [simp]:
-  \<open>take_bit n m < 2 ^ n\<close> for n m ::nat 
+  \<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
+  \<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]
@@ -2457,8 +2468,7 @@
   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
+  \<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>
@@ -2637,11 +2647,6 @@
   \<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
-
-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)
@@ -2684,15 +2689,15 @@
   using take_bit_of_exp [of n 1] by simp
 
 lemma push_bit_eq_0_iff [simp]:
-  "push_bit n a = 0 \<longleftrightarrow> a = 0"
+  \<open>push_bit n a = 0 \<longleftrightarrow> a = 0\<close>
   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)"
+  \<open>take_bit n (take_bit n a + take_bit n b) = take_bit n (a + b)\<close>
   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"
+  \<open>take_bit n 1 = 0 \<longleftrightarrow> n = 0\<close>
   by (simp add: take_bit_eq_mod)
 
 lemma drop_bit_Suc_bit0 [simp]:
@@ -2758,63 +2763,12 @@
   \<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 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 bit_0)
-  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 :: linordered_euclidean_semiring_bit_operations ..
 
 instance int :: linordered_euclidean_semiring_bit_operations ..
 
-lemma drop_bit_Suc_minus_bit0 [simp]:
-  \<open>drop_bit (Suc n) (- numeral (Num.Bit0 k)) = drop_bit n (- numeral k :: int)\<close>
-  by (simp add: drop_bit_Suc numeral_Bit0_div_2)
-
-lemma drop_bit_Suc_minus_bit1 [simp]:
-  \<open>drop_bit (Suc n) (- numeral (Num.Bit1 k)) = drop_bit n (- numeral (Num.inc k) :: int)\<close>
-  by (simp add: drop_bit_Suc numeral_Bit1_div_2 add_One)
-
-lemma drop_bit_numeral_minus_bit0 [simp]:
-  \<open>drop_bit (numeral l) (- numeral (Num.Bit0 k)) = drop_bit (pred_numeral l) (- numeral k :: int)\<close>
-  by (simp add: numeral_eq_Suc numeral_Bit0_div_2)
-
-lemma drop_bit_numeral_minus_bit1 [simp]:
-  \<open>drop_bit (numeral l) (- numeral (Num.Bit1 k)) = drop_bit (pred_numeral l) (- numeral (Num.inc k) :: int)\<close>
-  by (simp add: numeral_eq_Suc numeral_Bit1_div_2)
-
-lemma take_bit_Suc_minus_bit0:
-  \<open>take_bit (Suc n) (- numeral (Num.Bit0 k)) = take_bit n (- numeral k) * (2 :: int)\<close>
-  by (simp add: take_bit_Suc numeral_Bit0_div_2)
-
-lemma take_bit_Suc_minus_bit1:
-  \<open>take_bit (Suc n) (- numeral (Num.Bit1 k)) = take_bit n (- numeral (Num.inc k)) * 2 + (1 :: int)\<close>
-  by (simp add: take_bit_Suc numeral_Bit1_div_2 add_One)
-
-lemma take_bit_numeral_minus_bit0:
-  \<open>take_bit (numeral l) (- numeral (Num.Bit0 k)) = take_bit (pred_numeral l) (- numeral k) * (2 :: int)\<close>
-  by (simp add: numeral_eq_Suc numeral_Bit0_div_2 take_bit_Suc_minus_bit0)
-
-lemma take_bit_numeral_minus_bit1:
-  \<open>take_bit (numeral l) (- numeral (Num.Bit1 k)) = take_bit (pred_numeral l) (- numeral (Num.inc k)) * 2 + (1 :: int)\<close>
-  by (simp add: numeral_eq_Suc numeral_Bit1_div_2 take_bit_Suc_minus_bit1)
-
 
 subsection \<open>Symbolic computations on numeral expressions\<close>
 
@@ -2973,6 +2927,38 @@
 
 end
 
+lemma drop_bit_Suc_minus_bit0 [simp]:
+  \<open>drop_bit (Suc n) (- numeral (Num.Bit0 k)) = drop_bit n (- numeral k :: int)\<close>
+  by (simp add: drop_bit_Suc numeral_Bit0_div_2)
+
+lemma drop_bit_Suc_minus_bit1 [simp]:
+  \<open>drop_bit (Suc n) (- numeral (Num.Bit1 k)) = drop_bit n (- numeral (Num.inc k) :: int)\<close>
+  by (simp add: drop_bit_Suc numeral_Bit1_div_2 add_One)
+
+lemma drop_bit_numeral_minus_bit0 [simp]:
+  \<open>drop_bit (numeral l) (- numeral (Num.Bit0 k)) = drop_bit (pred_numeral l) (- numeral k :: int)\<close>
+  by (simp add: numeral_eq_Suc numeral_Bit0_div_2)
+
+lemma drop_bit_numeral_minus_bit1 [simp]:
+  \<open>drop_bit (numeral l) (- numeral (Num.Bit1 k)) = drop_bit (pred_numeral l) (- numeral (Num.inc k) :: int)\<close>
+  by (simp add: numeral_eq_Suc numeral_Bit1_div_2)
+
+lemma take_bit_Suc_minus_bit0:
+  \<open>take_bit (Suc n) (- numeral (Num.Bit0 k)) = take_bit n (- numeral k) * (2 :: int)\<close>
+  by (simp add: take_bit_Suc numeral_Bit0_div_2)
+
+lemma take_bit_Suc_minus_bit1:
+  \<open>take_bit (Suc n) (- numeral (Num.Bit1 k)) = take_bit n (- numeral (Num.inc k)) * 2 + (1 :: int)\<close>
+  by (simp add: take_bit_Suc numeral_Bit1_div_2 add_One)
+
+lemma take_bit_numeral_minus_bit0:
+  \<open>take_bit (numeral l) (- numeral (Num.Bit0 k)) = take_bit (pred_numeral l) (- numeral k) * (2 :: int)\<close>
+  by (simp add: numeral_eq_Suc numeral_Bit0_div_2 take_bit_Suc_minus_bit0)
+
+lemma take_bit_numeral_minus_bit1:
+  \<open>take_bit (numeral l) (- numeral (Num.Bit1 k)) = take_bit (pred_numeral l) (- numeral (Num.inc k)) * 2 + (1 :: int)\<close>
+  by (simp add: numeral_eq_Suc numeral_Bit1_div_2 take_bit_Suc_minus_bit1)
+
 lemma bit_Suc_0_iff [bit_simps]:
   \<open>bit (Suc 0) n \<longleftrightarrow> n = 0\<close>
   using bit_1_iff [of n, where ?'a = nat] by simp
@@ -3661,83 +3647,6 @@
 qed
 
 
-subsection \<open>Horner sums\<close>
-
-context semiring_bit_operations
-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)
-  case (stable a)
-  moreover have \<open>bit a = (\<lambda>_. odd a)\<close>
-    using stable by (simp add: stable_imp_bit_iff_odd fun_eq_iff)
-  moreover have \<open>{q. q < n} = {0..<n}\<close>
-    by auto
-  ultimately show ?case
-    by (simp add: stable_imp_take_bit_eq horner_sum_eq_sum mask_eq_sum_exp)
-next
-  case (rec a b)
-  show ?case
-  proof (cases n)
-    case 0
-    then show ?thesis
-      by simp
-  next
-    case (Suc m)
-    have \<open>map (bit (of_bool b + 2 * a)) [0..<Suc m] = b # map (bit (of_bool b + 2 * a)) [Suc 0..<Suc m]\<close>
-      by (simp only: upt_conv_Cons) (simp add: bit_0)
-    also have \<open>\<dots> = b # map (bit a) [0..<m]\<close>
-      by (simp only: flip: map_Suc_upt) (simp add: bit_Suc rec.hyps)
-    finally show ?thesis
-      using Suc rec.IH [of m] by (simp add: take_bit_Suc rec.hyps)
-        (simp_all add: ac_simps mod_2_eq_odd)
-  qed
-qed
-
-end
-
-context linordered_euclidean_semiring_bit_operations
-begin
-
-lemma bit_horner_sum_bit_iff [bit_simps]:
-  \<open>bit (horner_sum of_bool 2 bs) n \<longleftrightarrow> n < length bs \<and> bs ! n\<close>
-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 add: bit_0)
-  next
-    case (Suc m)
-    with bit_rec [of _ n] Cons.prems Cons.IH [of m]
-    show ?thesis by simp
-  qed
-qed
-
-lemma take_bit_horner_sum_bit_eq:
-  \<open>take_bit n (horner_sum of_bool 2 bs) = horner_sum of_bool 2 (take n bs)\<close>
-  by (auto simp add: bit_eq_iff bit_take_bit_iff bit_horner_sum_bit_iff)
-
-end
-
-lemma horner_sum_of_bool_2_less:
-  \<open>(horner_sum of_bool 2 bs :: int) < 2 ^ length bs\<close>
-proof -
-  have \<open>(\<Sum>n = 0..<length bs. of_bool (bs ! n) * (2::int) ^ n) \<le> (\<Sum>n = 0..<length bs. 2 ^ n)\<close>
-    by (rule sum_mono) simp
-  also have \<open>\<dots> = 2 ^ length bs - 1\<close>
-    by (induction bs) simp_all
-  finally show ?thesis
-    by (simp add: horner_sum_eq_sum)
-qed
-
-
 subsection \<open>Symbolic computations for code generation\<close>
 
 lemma bit_int_code [code]: