# HG changeset patch
# User paulson
# Date 1599575437 -3600
# Node ID 9c6787cfd70e640ffe6437a396e65b507cd61729
# Parent  4b011fa5e83bed1b935a06fd45e66934985ce09c# Parent  cbe7aa1c2bdc9f48feb87186cc5f7d17af60fb74
merged

diff -r cbe7aa1c2bdc -r 9c6787cfd70e src/HOL/Library/Bit_Operations.thy
--- a/src/HOL/Library/Bit_Operations.thy	Tue Sep 08 15:30:15 2020 +0100
+++ b/src/HOL/Library/Bit_Operations.thy	Tue Sep 08 15:30:37 2020 +0100
@@ -95,6 +95,30 @@
   \<open>take_bit n (a XOR b) = take_bit n a XOR take_bit n b\<close>
   by (auto simp add: bit_eq_iff bit_take_bit_iff bit_xor_iff)
 
+lemma push_bit_and [simp]:
+  \<open>push_bit n (a AND b) = push_bit n a AND push_bit n b\<close>
+  by (rule bit_eqI) (auto simp add: bit_push_bit_iff bit_and_iff)
+
+lemma push_bit_or [simp]:
+  \<open>push_bit n (a OR b) = push_bit n a OR push_bit n b\<close>
+  by (rule bit_eqI) (auto simp add: bit_push_bit_iff bit_or_iff)
+
+lemma push_bit_xor [simp]:
+  \<open>push_bit n (a XOR b) = push_bit n a XOR push_bit n b\<close>
+  by (rule bit_eqI) (auto simp add: bit_push_bit_iff bit_xor_iff)
+
+lemma drop_bit_and [simp]:
+  \<open>drop_bit n (a AND b) = drop_bit n a AND drop_bit n b\<close>
+  by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_and_iff)
+
+lemma drop_bit_or [simp]:
+  \<open>drop_bit n (a OR b) = drop_bit n a OR drop_bit n b\<close>
+  by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_or_iff)
+
+lemma drop_bit_xor [simp]:
+  \<open>drop_bit n (a XOR b) = drop_bit n a XOR drop_bit n b\<close>
+  by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_xor_iff)
+
 lemma bit_mask_iff:
   \<open>bit (mask m) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n < m\<close>
   by (simp add: mask_eq_exp_minus_1 bit_mask_iff)
@@ -135,6 +159,10 @@
   by (rule bit_eqI)
     (auto simp add: bit_take_bit_iff bit_and_iff bit_mask_iff)
 
+lemma disjunctive_add:
+  \<open>a + b = a OR b\<close> if \<open>\<And>n. \<not> bit a n \<or> \<not> bit b n\<close>
+  by (rule bit_eqI) (use that in \<open>simp add: bit_disjunctive_add_iff bit_or_iff\<close>)
+
 end
 
 class ring_bit_operations = semiring_bit_operations + ring_parity +
@@ -191,25 +219,18 @@
   by (simp add: bit_eq_iff bit_not_iff) (simp add: bit_1_iff)
 
 sublocale "and": semilattice_neutr \<open>(AND)\<close> \<open>- 1\<close>
-  apply standard
-  apply (simp add: bit_eq_iff bit_and_iff)
-  apply (auto simp add: exp_eq_0_imp_not_bit bit_exp_iff)
-  done
+  by standard (rule bit_eqI, simp add: bit_and_iff)
 
 sublocale bit: boolean_algebra \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close>
   rewrites \<open>bit.xor = (XOR)\<close>
 proof -
   interpret bit: boolean_algebra \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close>
-    apply standard
-         apply (simp_all add: bit_eq_iff)
-       apply (auto simp add: bit_and_iff bit_or_iff bit_not_iff bit_exp_iff exp_eq_0_imp_not_bit)
-    done
+    by standard (auto simp add: bit_and_iff bit_or_iff bit_not_iff intro: bit_eqI)
   show \<open>boolean_algebra (AND) (OR) NOT 0 (- 1)\<close>
     by standard
   show \<open>boolean_algebra.xor (AND) (OR) NOT = (XOR)\<close>
-    apply (simp add: fun_eq_iff bit_eq_iff bit.xor_def)
-    apply (auto simp add: bit_and_iff bit_or_iff bit_not_iff bit_xor_iff exp_eq_0_imp_not_bit)
-    done
+    by (rule ext, rule ext, rule bit_eqI)
+      (auto simp add: bit.xor_def bit_and_iff bit_or_iff bit_xor_iff bit_not_iff)
 qed
 
 lemma and_eq_not_not_or:
@@ -228,6 +249,17 @@
   \<open>NOT (a - b) = NOT a + b\<close>
   using not_add_distrib [of a \<open>- b\<close>] by simp
 
+lemma disjunctive_diff:
+  \<open>a - b = a AND NOT b\<close> if \<open>\<And>n. bit b n \<Longrightarrow> bit a n\<close>
+proof -
+  have \<open>NOT a + b = NOT a OR b\<close>
+    by (rule disjunctive_add) (auto simp add: bit_not_iff dest: that)
+  then have \<open>NOT (NOT a + b) = NOT (NOT a OR b)\<close>
+    by simp
+  then show ?thesis
+    by (simp add: not_add_distrib)
+qed
+
 lemma push_bit_minus:
   \<open>push_bit n (- a) = - push_bit n a\<close>
   by (simp add: push_bit_eq_mult)
@@ -238,9 +270,9 @@
 
 lemma take_bit_not_iff:
   "take_bit n (NOT a) = take_bit n (NOT b) \<longleftrightarrow> take_bit n a = take_bit n b"
-  apply (simp add: bit_eq_iff bit_not_iff bit_take_bit_iff)
-  apply (simp add: bit_exp_iff)
-  apply (use local.exp_eq_0_imp_not_bit in blast)
+  apply (simp add: bit_eq_iff)
+  apply (simp add: bit_not_iff bit_take_bit_iff bit_exp_iff)
+  apply (use exp_eq_0_imp_not_bit in blast)
   done
 
 lemma mask_eq_take_bit_minus_one:
@@ -519,40 +551,10 @@
 
 end
 
-lemma disjunctive_add:
-  \<open>k + l = k OR l\<close> if \<open>\<And>n. \<not> bit k n \<or> \<not> bit l n\<close> for k l :: int
-  \<comment> \<open>TODO: may integrate (indirectly) into \<^class>\<open>semiring_bits\<close> premises\<close>
-proof (rule bit_eqI)
-  fix n
-  from that have \<open>bit (k + l) n \<longleftrightarrow> bit k n \<or> bit l n\<close>
-  proof (induction n arbitrary: k l)
-    case 0
-    from this [of 0] show ?case
-      by auto
-  next
-    case (Suc n)
-    have \<open>bit ((k + l) div 2) n \<longleftrightarrow> bit (k div 2 + l div 2) n\<close>
-      using Suc.prems [of 0] div_add1_eq [of k l] by auto
-    also have \<open>bit (k div 2 + l div 2) n \<longleftrightarrow> bit (k div 2) n \<or> bit (l div 2) n\<close>
-      by (rule Suc.IH) (use Suc.prems in \<open>simp flip: bit_Suc\<close>)
-    finally show ?case
-      by (simp add: bit_Suc)
-  qed
-  also have \<open>\<dots> \<longleftrightarrow> bit (k OR l) n\<close>
-    by (simp add: bit_or_iff)
-  finally show \<open>bit (k + l) n \<longleftrightarrow> bit (k OR l) n\<close> .
-qed
 
-lemma disjunctive_diff:
-  \<open>k - l = k AND NOT l\<close> if \<open>\<And>n. bit l n \<Longrightarrow> bit k n\<close> for k l :: int
-proof -
-  have \<open>NOT k + l = NOT k OR l\<close>
-    by (rule disjunctive_add) (auto simp add: bit_not_iff dest: that)
-  then have \<open>NOT (NOT k + l) = NOT (NOT k OR l)\<close>
-    by simp
-  then show ?thesis
-    by (simp add: not_add_distrib)
-qed
+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)
 
 lemma mask_nonnegative_int [simp]:
   \<open>mask n \<ge> (0::int)\<close>
@@ -898,43 +900,55 @@
     (auto simp add: bit_take_bit_iff bit_concat_bit_iff min_def)  
 
 
-subsection \<open>Taking bit with sign propagation\<close>
+subsection \<open>Taking bits with sign propagation\<close>
 
-definition signed_take_bit :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
-  where \<open>signed_take_bit n k = concat_bit n k (- of_bool (bit k n))\<close>
+context ring_bit_operations
+begin
 
-lemma signed_take_bit_unfold:
-  \<open>signed_take_bit n k = take_bit n k OR (of_bool (bit k n) * NOT (mask n))\<close>
-  by (simp add: signed_take_bit_def concat_bit_def push_bit_minus_one_eq_not_mask)
+definition signed_take_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
+  where \<open>signed_take_bit n a = take_bit n a OR (of_bool (bit a n) * NOT (mask n))\<close>
 
-lemma signed_take_bit_eq:
-  \<open>signed_take_bit n k = take_bit n k\<close> if \<open>\<not> bit k n\<close>
+lemma signed_take_bit_eq_if_positive:
+  \<open>signed_take_bit n a = take_bit n a\<close> if \<open>\<not> bit a n\<close>
   using that by (simp add: signed_take_bit_def)
 
-lemma signed_take_bit_eq_or:
-  \<open>signed_take_bit n k = take_bit n k OR NOT (mask n)\<close> if \<open>bit k n\<close>
-  using that by (simp add: signed_take_bit_def concat_bit_def take_bit_eq_mask push_bit_minus_one_eq_not_mask)
+lemma signed_take_bit_eq_if_negative:
+  \<open>signed_take_bit n a = take_bit n a OR NOT (mask n)\<close> if \<open>bit a n\<close>
+  using that by (simp add: signed_take_bit_def)
+
+lemma even_signed_take_bit_iff:
+  \<open>even (signed_take_bit m a) \<longleftrightarrow> even a\<close>
+  by (auto simp add: signed_take_bit_def even_or_iff even_mask_iff bit_double_iff)
+
+lemma bit_signed_take_bit_iff:
+  \<open>bit (signed_take_bit m a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> bit a (min m n)\<close>
+  by (simp add: signed_take_bit_def bit_take_bit_iff bit_or_iff bit_not_iff bit_mask_iff min_def not_le)
+    (use exp_eq_0_imp_not_bit in blast)
 
 lemma signed_take_bit_0 [simp]:
-  \<open>signed_take_bit 0 k = - (k mod 2)\<close>
+  \<open>signed_take_bit 0 a = - (a mod 2)\<close>
   by (simp add: signed_take_bit_def odd_iff_mod_2_eq_one)
 
-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)
-
 lemma signed_take_bit_Suc:
-  \<open>signed_take_bit (Suc n) k = k mod 2 + 2 * signed_take_bit n (k div 2)\<close>
-  by (unfold signed_take_bit_def or_int_rec [of \<open>take_bit (Suc n) k\<close>])
-    (simp add: bit_Suc concat_bit_Suc even_or_iff even_mask_iff odd_iff_mod_2_eq_one not_int_div_2 mask_half_int)
-
-lemma signed_take_bit_rec:
-  \<open>signed_take_bit n k = (if n = 0 then - (k mod 2) else k mod 2 + 2 * signed_take_bit (n - 1) (k div 2))\<close>
-  by (cases n) (simp_all add: signed_take_bit_Suc)
-
-lemma bit_signed_take_bit_iff:
-  \<open>bit (signed_take_bit m k) n = bit k (min m n)\<close>
-  by (simp add: signed_take_bit_def bit_or_iff bit_concat_bit_iff bit_not_iff bit_mask_iff min_def)
+  \<open>signed_take_bit (Suc n) a = a mod 2 + 2 * signed_take_bit n (a div 2)\<close>
+proof (rule bit_eqI)
+  fix m
+  assume *: \<open>2 ^ m \<noteq> 0\<close>
+  show \<open>bit (signed_take_bit (Suc n) a) m \<longleftrightarrow>
+    bit (a mod 2 + 2 * signed_take_bit n (a div 2)) m\<close>
+  proof (cases m)
+    case 0
+    then show ?thesis
+      by (simp add: even_signed_take_bit_iff)
+  next
+    case (Suc m)
+    with * have \<open>2 ^ m \<noteq> 0\<close>
+      by (metis mult_not_zero power_Suc)
+    with Suc show ?thesis
+      by (simp add: bit_signed_take_bit_iff mod2_eq_if bit_double_iff even_bit_succ_iff
+        ac_simps flip: bit_Suc)
+  qed
+qed
 
 lemma signed_take_bit_of_0 [simp]:
   \<open>signed_take_bit n 0 = 0\<close>
@@ -942,36 +956,56 @@
 
 lemma signed_take_bit_of_minus_1 [simp]:
   \<open>signed_take_bit n (- 1) = - 1\<close>
-  by (simp add: signed_take_bit_def concat_bit_def push_bit_minus_one_eq_not_mask take_bit_minus_one_eq_mask)
+  by (simp add: signed_take_bit_def take_bit_minus_one_eq_mask mask_eq_exp_minus_1)
 
-lemma signed_take_bit_signed_take_bit [simp]:
-  \<open>signed_take_bit m (signed_take_bit n k) = signed_take_bit (min m n) k\<close>
-  by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_or_iff bit_not_iff bit_mask_iff bit_take_bit_iff)
+lemma signed_take_bit_Suc_1 [simp]:
+  \<open>signed_take_bit (Suc n) 1 = 1\<close>
+  by (simp add: signed_take_bit_Suc)
+
+lemma signed_take_bit_rec:
+  \<open>signed_take_bit n a = (if n = 0 then - (a mod 2) else a mod 2 + 2 * signed_take_bit (n - 1) (a div 2))\<close>
+  by (cases n) (simp_all add: signed_take_bit_Suc)
 
 lemma signed_take_bit_eq_iff_take_bit_eq:
-  \<open>signed_take_bit n k = signed_take_bit n l \<longleftrightarrow> take_bit (Suc n) k = take_bit (Suc n) l\<close>
-proof (cases \<open>bit k n \<longleftrightarrow> bit l n\<close>)
-  case True
-  moreover have \<open>take_bit n k OR NOT (mask n) = take_bit n k - 2 ^ n\<close>
-    for k :: int
-    by (auto simp add: disjunctive_add [symmetric] bit_not_iff bit_mask_iff bit_take_bit_iff minus_exp_eq_not_mask)
-  ultimately show ?thesis
-    by (simp add: signed_take_bit_def take_bit_Suc_from_most concat_bit_eq)
-next
-  case False
-  then have \<open>signed_take_bit n k \<noteq> signed_take_bit n l\<close> and \<open>take_bit (Suc n) k \<noteq> take_bit (Suc n) l\<close>
-    by (auto simp add: bit_eq_iff bit_take_bit_iff bit_signed_take_bit_iff min_def)
+  \<open>signed_take_bit n a = signed_take_bit n b \<longleftrightarrow> take_bit (Suc n) a = take_bit (Suc n) b\<close>
+proof -
+  have \<open>bit (signed_take_bit n a) = bit (signed_take_bit n b) \<longleftrightarrow> bit (take_bit (Suc n) a) = bit (take_bit (Suc n) b)\<close>
+    by (simp add: fun_eq_iff bit_signed_take_bit_iff bit_take_bit_iff not_le less_Suc_eq_le min_def)
+      (use exp_eq_0_imp_not_bit in fastforce)
   then show ?thesis
-    by simp
+    by (simp add: bit_eq_iff fun_eq_iff)
 qed
 
+lemma signed_take_bit_signed_take_bit [simp]:
+  \<open>signed_take_bit m (signed_take_bit n a) = signed_take_bit (min m n) a\<close>
+proof (rule bit_eqI)
+  fix q
+  show \<open>bit (signed_take_bit m (signed_take_bit n a)) q \<longleftrightarrow>
+    bit (signed_take_bit (min m n) a) q\<close>
+    by (simp add: bit_signed_take_bit_iff min_def bit_or_iff bit_not_iff bit_mask_iff bit_take_bit_iff)
+      (use le_Suc_ex exp_add_not_zero_imp in blast)
+qed
+
+lemma signed_take_bit_take_bit:
+  \<open>signed_take_bit m (take_bit n a) = (if n \<le> m then take_bit n else signed_take_bit m) a\<close>
+  by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_take_bit_iff)
+
 lemma take_bit_signed_take_bit:
-  \<open>take_bit m (signed_take_bit n k) = take_bit m k\<close> if \<open>m \<le> Suc n\<close>
+  \<open>take_bit m (signed_take_bit n a) = take_bit m a\<close> if \<open>m \<le> Suc n\<close>
   using that by (rule le_SucE; intro bit_eqI)
    (auto simp add: bit_take_bit_iff bit_signed_take_bit_iff min_def less_Suc_eq)
 
+end
+
+text \<open>Modulus centered around 0\<close>
+
+lemma signed_take_bit_eq_concat_bit:
+  \<open>signed_take_bit n k = concat_bit n k (- of_bool (bit k n))\<close>
+  by (simp add: concat_bit_def signed_take_bit_def push_bit_minus_one_eq_not_mask)
+
 lemma signed_take_bit_add:
   \<open>signed_take_bit n (signed_take_bit n k + signed_take_bit n l) = signed_take_bit n (k + l)\<close>
+  for k l :: int
 proof -
   have \<open>take_bit (Suc n)
      (take_bit (Suc n) (signed_take_bit n k) +
@@ -984,6 +1018,7 @@
 
 lemma signed_take_bit_diff:
   \<open>signed_take_bit n (signed_take_bit n k - signed_take_bit n l) = signed_take_bit n (k - l)\<close>
+  for k l :: int
 proof -
   have \<open>take_bit (Suc n)
      (take_bit (Suc n) (signed_take_bit n k) -
@@ -996,6 +1031,7 @@
 
 lemma signed_take_bit_minus:
   \<open>signed_take_bit n (- signed_take_bit n k) = signed_take_bit n (- k)\<close>
+  for k :: int
 proof -
   have \<open>take_bit (Suc n)
      (- take_bit (Suc n) (signed_take_bit n k)) =
@@ -1007,6 +1043,7 @@
 
 lemma signed_take_bit_mult:
   \<open>signed_take_bit n (signed_take_bit n k * signed_take_bit n l) = signed_take_bit n (k * l)\<close>
+  for k l :: int
 proof -
   have \<open>take_bit (Suc n)
      (take_bit (Suc n) (signed_take_bit n k) *
@@ -1017,10 +1054,9 @@
     by (simp only: signed_take_bit_eq_iff_take_bit_eq take_bit_mult)
 qed
 
-text \<open>Modulus centered around 0\<close>
-
 lemma signed_take_bit_eq_take_bit_minus:
   \<open>signed_take_bit n k = take_bit (Suc n) k - 2 ^ Suc n * of_bool (bit k n)\<close>
+  for k :: int
 proof (cases \<open>bit k n\<close>)
   case True
   have \<open>signed_take_bit n k = take_bit (Suc n) k OR NOT (mask (Suc n))\<close>
@@ -1031,13 +1067,13 @@
     by (simp flip: minus_exp_eq_not_mask)
 next
   case False
-  then show ?thesis
-    by (simp add: bit_eq_iff bit_take_bit_iff bit_signed_take_bit_iff min_def)
-      (auto intro: bit_eqI simp add: less_Suc_eq)
+  show ?thesis
+    by (rule bit_eqI) (simp add: False bit_signed_take_bit_iff bit_take_bit_iff min_def less_Suc_eq)
 qed
 
 lemma signed_take_bit_eq_take_bit_shift:
   \<open>signed_take_bit n k = take_bit (Suc n) (k + 2 ^ n) - 2 ^ n\<close>
+  for k :: int
 proof -
   have *: \<open>take_bit n k OR 2 ^ n = take_bit n k + 2 ^ n\<close>
     by (simp add: disjunctive_add bit_exp_iff bit_take_bit_iff)
@@ -1057,87 +1093,80 @@
     by (rule disjunctive_add)
       (auto simp add: disjunctive_add bit_take_bit_iff bit_double_iff bit_exp_iff)
   finally show ?thesis
-    using * **
-    by (simp add: signed_take_bit_def concat_bit_Suc min_def ac_simps)
-      (simp add: concat_bit_def take_bit_eq_mask push_bit_minus_one_eq_not_mask ac_simps)
+    using * ** by (simp add: signed_take_bit_def concat_bit_Suc min_def ac_simps)
 qed
 
-lemma signed_take_bit_take_bit:
-  \<open>signed_take_bit m (take_bit n k) = (if n \<le> m then take_bit n else signed_take_bit m) k\<close>
-  by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_take_bit_iff)
-
 lemma signed_take_bit_nonnegative_iff [simp]:
   \<open>0 \<le> signed_take_bit n k \<longleftrightarrow> \<not> bit k n\<close>
+  for k :: int
   by (simp add: signed_take_bit_def not_less concat_bit_def)
 
 lemma signed_take_bit_negative_iff [simp]:
   \<open>signed_take_bit n k < 0 \<longleftrightarrow> bit k n\<close>
+  for k :: int
   by (simp add: signed_take_bit_def not_less concat_bit_def)
 
 lemma signed_take_bit_greater_eq:
   \<open>k + 2 ^ Suc n \<le> signed_take_bit n k\<close> if \<open>k < - (2 ^ n)\<close>
+  for k :: int
   using that take_bit_greater_eq [of \<open>k + 2 ^ n\<close> \<open>Suc n\<close>]
   by (simp add: signed_take_bit_eq_take_bit_shift)
 
 lemma signed_take_bit_less_eq:
   \<open>signed_take_bit n k \<le> k - 2 ^ Suc n\<close> if \<open>k \<ge> 2 ^ n\<close>
+  for k :: int
   using that take_bit_less_eq [of \<open>Suc n\<close> \<open>k + 2 ^ n\<close>]
   by (simp add: signed_take_bit_eq_take_bit_shift)
 
 lemma signed_take_bit_eq_self:
   \<open>signed_take_bit n k = k\<close> if \<open>- (2 ^ n) \<le> k\<close> \<open>k < 2 ^ n\<close>
+  for k :: int
   using that by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_eq_self)
 
-lemma signed_take_bit_Suc_1 [simp]:
-  \<open>signed_take_bit (Suc n) 1 = 1\<close>
-  by (simp add: signed_take_bit_Suc)
-
 lemma signed_take_bit_Suc_bit0 [simp]:
-  \<open>signed_take_bit (Suc n) (numeral (Num.Bit0 k)) = signed_take_bit n (numeral k) * 2\<close>
+  \<open>signed_take_bit (Suc n) (numeral (Num.Bit0 k)) = signed_take_bit n (numeral k) * (2 :: int)\<close>
   by (simp add: signed_take_bit_Suc)
 
 lemma signed_take_bit_Suc_bit1 [simp]:
-  \<open>signed_take_bit (Suc n) (numeral (Num.Bit1 k)) = signed_take_bit n (numeral k) * 2 + 1\<close>
+  \<open>signed_take_bit (Suc n) (numeral (Num.Bit1 k)) = signed_take_bit n (numeral k) * 2 + (1 :: int)\<close>
   by (simp add: signed_take_bit_Suc)
 
 lemma signed_take_bit_Suc_minus_bit0 [simp]:
-  \<open>signed_take_bit (Suc n) (- numeral (Num.Bit0 k)) = signed_take_bit n (- numeral k) * 2\<close>
+  \<open>signed_take_bit (Suc n) (- numeral (Num.Bit0 k)) = signed_take_bit n (- numeral k) * (2 :: int)\<close>
   by (simp add: signed_take_bit_Suc)
 
 lemma signed_take_bit_Suc_minus_bit1 [simp]:
-  \<open>signed_take_bit (Suc n) (- numeral (Num.Bit1 k)) = signed_take_bit n (- numeral k - 1) * 2 + 1\<close>
+  \<open>signed_take_bit (Suc n) (- numeral (Num.Bit1 k)) = signed_take_bit n (- numeral k - 1) * 2 + (1 :: int)\<close>
   by (simp add: signed_take_bit_Suc)
 
 lemma signed_take_bit_numeral_bit0 [simp]:
-  \<open>signed_take_bit (numeral l) (numeral (Num.Bit0 k)) = signed_take_bit (pred_numeral l) (numeral k) * 2\<close>
+  \<open>signed_take_bit (numeral l) (numeral (Num.Bit0 k)) = signed_take_bit (pred_numeral l) (numeral k) * (2 :: int)\<close>
   by (simp add: signed_take_bit_rec)
 
 lemma signed_take_bit_numeral_bit1 [simp]:
-  \<open>signed_take_bit (numeral l) (numeral (Num.Bit1 k)) = signed_take_bit (pred_numeral l) (numeral k) * 2 + 1\<close>
+  \<open>signed_take_bit (numeral l) (numeral (Num.Bit1 k)) = signed_take_bit (pred_numeral l) (numeral k) * 2 + (1 :: int)\<close>
   by (simp add: signed_take_bit_rec)
 
 lemma signed_take_bit_numeral_minus_bit0 [simp]:
-  \<open>signed_take_bit (numeral l) (- numeral (Num.Bit0 k)) = signed_take_bit (pred_numeral l) (- numeral k) * 2\<close>
+  \<open>signed_take_bit (numeral l) (- numeral (Num.Bit0 k)) = signed_take_bit (pred_numeral l) (- numeral k) * (2 :: int)\<close>
   by (simp add: signed_take_bit_rec)
 
 lemma signed_take_bit_numeral_minus_bit1 [simp]:
-  \<open>signed_take_bit (numeral l) (- numeral (Num.Bit1 k)) = signed_take_bit (pred_numeral l) (- numeral k - 1) * 2 + 1\<close>
+  \<open>signed_take_bit (numeral l) (- numeral (Num.Bit1 k)) = signed_take_bit (pred_numeral l) (- numeral k - 1) * 2 + (1 :: int)\<close>
   by (simp add: signed_take_bit_rec)
 
 lemma signed_take_bit_code [code]:
-  \<open>signed_take_bit n k =
-  (let l = take_bit (Suc n) k
-   in if bit l n then l - (push_bit n 2) else l)\<close>
+  \<open>signed_take_bit n a =
+  (let l = take_bit (Suc n) a
+   in if bit l n then l + push_bit (Suc n) (- 1) else l)\<close>
 proof -
-  have *: \<open>(take_bit (Suc n) k) - 2 * 2 ^ n = take_bit (Suc n) k OR NOT (mask (Suc n))\<close>
-    apply (subst disjunctive_add [symmetric])
-    apply (simp_all add: bit_and_iff bit_mask_iff bit_not_iff bit_take_bit_iff)
-    apply (simp flip: minus_exp_eq_not_mask)
-    done
+  have *: \<open>take_bit (Suc n) a + push_bit n (- 2) =
+    take_bit (Suc n) a OR NOT (mask (Suc n))\<close>
+    by (auto simp add: bit_take_bit_iff bit_push_bit_iff bit_not_iff bit_mask_iff disjunctive_add
+       simp flip: push_bit_minus_one_eq_not_mask)
   show ?thesis
     by (rule bit_eqI)
-     (auto simp add: Let_def bit_and_iff bit_signed_take_bit_iff push_bit_eq_mult min_def not_le
-       bit_mask_iff bit_exp_iff less_Suc_eq * bit_or_iff bit_take_bit_iff bit_not_iff)
+      (auto simp add: Let_def * bit_signed_take_bit_iff bit_take_bit_iff min_def less_Suc_eq bit_not_iff bit_mask_iff bit_or_iff)
 qed
 
 
@@ -1360,40 +1389,11 @@
 
       \<^item> Flip a single bit: @{thm flip_bit_def [where ?'a = int, no_vars]}
 
-      \<^item> Bit concatenation: @{thm concat_bit_def [no_vars]}
+      \<^item> Signed truncation, or modulus centered around \<^term>\<open>0::int\<close>: @{thm signed_take_bit_def [no_vars]}
 
-      \<^item> Truncation centered towards \<^term>\<open>0::int\<close>: @{thm signed_take_bit_def [no_vars]}
+      \<^item> Bit concatenation: @{thm concat_bit_def [no_vars]}
 
       \<^item> (Bounded) conversion from and to a list of bits: @{thm horner_sum_bit_eq_take_bit [where ?'a = int, no_vars]}
 \<close>
 
-context semiring_bit_operations
-begin
-
-lemma push_bit_and [simp]:
-  \<open>push_bit n (a AND b) = push_bit n a AND push_bit n b\<close>
-  by (rule bit_eqI) (auto simp add: bit_push_bit_iff bit_and_iff)
-
-lemma push_bit_or [simp]:
-  \<open>push_bit n (a OR b) = push_bit n a OR push_bit n b\<close>
-  by (rule bit_eqI) (auto simp add: bit_push_bit_iff bit_or_iff)
-
-lemma push_bit_xor [simp]:
-  \<open>push_bit n (a XOR b) = push_bit n a XOR push_bit n b\<close>
-  by (rule bit_eqI) (auto simp add: bit_push_bit_iff bit_xor_iff)
-
-lemma drop_bit_and [simp]:
-  \<open>drop_bit n (a AND b) = drop_bit n a AND drop_bit n b\<close>
-  by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_and_iff)
-
-lemma drop_bit_or [simp]:
-  \<open>drop_bit n (a OR b) = drop_bit n a OR drop_bit n b\<close>
-  by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_or_iff)
-
-lemma drop_bit_xor [simp]:
-  \<open>drop_bit n (a XOR b) = drop_bit n a XOR drop_bit n b\<close>
-  by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_xor_iff)
-
 end
-
-end
diff -r cbe7aa1c2bdc -r 9c6787cfd70e src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Tue Sep 08 15:30:15 2020 +0100
+++ b/src/HOL/Parity.thy	Tue Sep 08 15:30:37 2020 +0100
@@ -990,6 +990,40 @@
     by simp_all
 qed
 
+lemma bit_disjunctive_add_iff:
+  \<open>bit (a + b) n \<longleftrightarrow> bit a n \<or> bit b n\<close>
+  if \<open>\<And>n. \<not> bit a n \<or> \<not> bit b n\<close>
+proof (cases \<open>2 ^ n = 0\<close>)
+  case True
+  then show ?thesis
+    by (simp add: exp_eq_0_imp_not_bit)
+next
+  case False
+  with that show ?thesis proof (induction n arbitrary: a b)
+    case 0
+    from "0.prems"(1) [of 0] show ?case
+      by auto
+  next
+    case (Suc n)
+    from Suc.prems(1) [of 0] have even: \<open>even a \<or> even b\<close>
+      by auto
+    have bit: \<open>\<not> bit (a div 2) n \<or> \<not> bit (b div 2) n\<close> for n
+      using Suc.prems(1) [of \<open>Suc n\<close>] by (simp add: bit_Suc)
+    from Suc.prems(2) have \<open>2 * 2 ^ n \<noteq> 0\<close> \<open>2 ^ n \<noteq> 0\<close>
+      by (auto simp add: mult_2)
+    have \<open>a + b = (a div 2 * 2 + a mod 2) + (b div 2 * 2 + b mod 2)\<close>
+      using div_mult_mod_eq [of a 2] div_mult_mod_eq [of b 2] by simp
+    also have \<open>\<dots> = of_bool (odd a \<or> odd b) + 2 * (a div 2 + b div 2)\<close>
+      using even by (auto simp add: algebra_simps mod2_eq_if)
+    finally have \<open>bit ((a + b) div 2) n \<longleftrightarrow> bit (a div 2 + b div 2) n\<close>
+      using \<open>2 * 2 ^ n \<noteq> 0\<close> by simp (simp flip: bit_Suc add: bit_double_iff)
+    also have \<open>\<dots> \<longleftrightarrow> bit (a div 2) n \<or> bit (b div 2) n\<close>
+      using bit \<open>2 ^ n \<noteq> 0\<close> by (rule Suc.IH)
+    finally show ?case
+      by (simp add: bit_Suc)
+  qed
+qed
+
 end
 
 lemma nat_bit_induct [case_names zero even odd]:
diff -r cbe7aa1c2bdc -r 9c6787cfd70e src/HOL/Word/Ancient_Numeral.thy
--- a/src/HOL/Word/Ancient_Numeral.thy	Tue Sep 08 15:30:15 2020 +0100
+++ b/src/HOL/Word/Ancient_Numeral.thy	Tue Sep 08 15:30:37 2020 +0100
@@ -163,14 +163,14 @@
   by (cases n) auto
 
 lemmas sbintrunc_Suc_BIT [simp] =
-  signed_take_bit_Suc [where k="w BIT b", simplified bin_last_BIT bin_rest_BIT] for w b
+  signed_take_bit_Suc [where a="w BIT b", simplified bin_last_BIT bin_rest_BIT] for w b
 
 lemmas sbintrunc_0_BIT_B0 [simp] =
-  signed_take_bit_0 [where k="w BIT False", simplified bin_last_numeral_simps bin_rest_numeral_simps]
+  signed_take_bit_0 [where a="w BIT False", simplified bin_last_numeral_simps bin_rest_numeral_simps]
   for w
 
 lemmas sbintrunc_0_BIT_B1 [simp] =
-  signed_take_bit_0 [where k="w BIT True", simplified bin_last_BIT bin_rest_numeral_simps]
+  signed_take_bit_0 [where a="w BIT True", simplified bin_last_BIT bin_rest_numeral_simps]
   for w
 
 lemma sbintrunc_Suc_minus_Is:
diff -r cbe7aa1c2bdc -r 9c6787cfd70e src/HOL/Word/Bits_Int.thy
--- a/src/HOL/Word/Bits_Int.thy	Tue Sep 08 15:30:15 2020 +0100
+++ b/src/HOL/Word/Bits_Int.thy	Tue Sep 08 15:30:37 2020 +0100
@@ -227,19 +227,19 @@
   by (rule bin_eqI) (auto simp: nth_sbintr min.absorb1 min.absorb2)
 
 lemmas sbintrunc_Suc_Pls =
-  signed_take_bit_Suc [where k="0", simplified bin_last_numeral_simps bin_rest_numeral_simps]
+  signed_take_bit_Suc [where a="0::int", simplified bin_last_numeral_simps bin_rest_numeral_simps]
 
 lemmas sbintrunc_Suc_Min =
-  signed_take_bit_Suc [where k="-1", simplified bin_last_numeral_simps bin_rest_numeral_simps]
+  signed_take_bit_Suc [where a="-1::int", simplified bin_last_numeral_simps bin_rest_numeral_simps]
 
 lemmas sbintrunc_Sucs = sbintrunc_Suc_Pls sbintrunc_Suc_Min
   sbintrunc_Suc_numeral
 
 lemmas sbintrunc_Pls =
-  signed_take_bit_0 [where k="0", simplified bin_last_numeral_simps bin_rest_numeral_simps]
+  signed_take_bit_0 [where a="0::int", simplified bin_last_numeral_simps bin_rest_numeral_simps]
 
 lemmas sbintrunc_Min =
-  signed_take_bit_0 [where k="-1", simplified bin_last_numeral_simps bin_rest_numeral_simps]
+  signed_take_bit_0 [where a="-1::int", simplified bin_last_numeral_simps bin_rest_numeral_simps]
 
 lemmas sbintrunc_0_simps =
   sbintrunc_Pls sbintrunc_Min
diff -r cbe7aa1c2bdc -r 9c6787cfd70e src/HOL/Word/Conversions.thy
--- a/src/HOL/Word/Conversions.thy	Tue Sep 08 15:30:15 2020 +0100
+++ b/src/HOL/Word/Conversions.thy	Tue Sep 08 15:30:37 2020 +0100
@@ -13,6 +13,41 @@
 
 hide_const (open) unat uint sint word_of_int ucast scast
 
+context semiring_bits
+begin
+
+lemma
+  exp_add_not_zero_imp_left: \<open>2 ^ m \<noteq> 0\<close>
+  and exp_add_not_zero_imp_right: \<open>2 ^ n \<noteq> 0\<close> if \<open>2 ^ (m + n) \<noteq> 0\<close>
+proof -
+  have \<open>\<not> (2 ^ m = 0 \<or> 2 ^ n = 0)\<close>
+  proof (rule notI)
+    assume \<open>2 ^ m = 0 \<or> 2 ^ n = 0\<close>
+    then have \<open>2 ^ (m + n) = 0\<close>
+      by (rule disjE) (simp_all add: power_add)
+    with that show False ..
+  qed
+  then show \<open>2 ^ m \<noteq> 0\<close> and \<open>2 ^ n \<noteq> 0\<close>
+    by simp_all
+qed
+
+lemma exp_not_zero_imp_exp_diff_not_zero:
+  \<open>2 ^ (n - m) \<noteq> 0\<close> if \<open>2 ^ n \<noteq> 0\<close>
+proof (cases \<open>m \<le> n\<close>)
+  case True
+  moreover define q where \<open>q = n - m\<close>
+  ultimately have \<open>n = m + q\<close>
+    by simp
+  with that show ?thesis
+    by (simp add: exp_add_not_zero_imp_right)
+next
+  case False
+  with that show ?thesis
+    by simp
+qed
+
+end
+
 
 subsection \<open>Conversions to word\<close>
 
@@ -205,7 +240,7 @@
 begin
 
 lift_definition signed :: \<open>'b::len word \<Rightarrow> 'a\<close>
-  is \<open>of_int \<circ> signed_take_bit (LENGTH('b) - 1)\<close>
+  is \<open>of_int \<circ> signed_take_bit (LENGTH('b) - Suc 0)\<close>
   by (simp flip: signed_take_bit_decr_length_iff)
 
 lemma signed_0 [simp]:
@@ -214,8 +249,8 @@
 
 lemma signed_1 [simp]:
   \<open>signed (1 :: 'b::len word) = (if LENGTH('b) = 1 then - 1 else 1)\<close>
-  by (transfer fixing: uminus)
-    (simp_all add: signed_take_bit_eq not_le Suc_lessI)
+  by (transfer fixing: uminus; cases \<open>LENGTH('b)\<close>)
+    (simp_all add: sbintrunc_minus_simps)
 
 lemma signed_minus_1 [simp]:
   \<open>signed (- 1 :: 'b::len word) = - 1\<close>
@@ -242,11 +277,11 @@
 lemma bit_signed_iff:
   \<open>bit (signed w) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> bit w (min (LENGTH('b) - Suc 0) n)\<close>
   for w :: \<open>'b::len word\<close>
-  by (transfer fixing: bit) (auto simp add: bit_of_int_iff bit_signed_take_bit_iff min_def)
+  by (transfer fixing: bit)
+    (auto simp add: bit_of_int_iff Bit_Operations.bit_signed_take_bit_iff min_def)
 
 lemma signed_push_bit_eq:
-  \<open>signed (push_bit n w) = take_bit (LENGTH('b) - Suc 0) (push_bit n (signed w))
-    OR of_bool (n < LENGTH('b) \<and> bit w (LENGTH('b) - Suc n)) * NOT (mask (LENGTH('b) - Suc 0))\<close>
+  \<open>signed (push_bit n w) = signed_take_bit (LENGTH('b) - 1) (push_bit n (signed w :: 'a))\<close>
   for w :: \<open>'b::len word\<close>
 proof (rule bit_eqI)
   fix m
@@ -255,18 +290,27 @@
   then have *: \<open>LENGTH('b) = Suc q\<close>
     by simp
   show \<open>bit (signed (push_bit n w)) m \<longleftrightarrow>
-    bit (take_bit (LENGTH('b) - Suc 0) (push_bit n (signed w)) OR
-      of_bool (n < LENGTH('b) \<and> bit w (LENGTH('b) - Suc n)) * NOT (mask (LENGTH('b) - Suc 0))) m\<close>
-  proof (cases \<open>n \<le> m\<close>)
+    bit (signed_take_bit (LENGTH('b) - 1) (push_bit n (signed w :: 'a))) m\<close>
+  proof (cases \<open>q \<le> m\<close>)
     case True
-    with \<open>2 ^ m \<noteq> 0\<close> have \<open>2 ^ (m - n) \<noteq> 0\<close>
-      by (metis (full_types) diff_add exp_add_not_zero_imp)
-    with True show ?thesis
-      by (auto simp add: * bit_signed_iff bit_push_bit_iff Parity.bit_push_bit_iff bit_or_iff bit_take_bit_iff bit_not_iff bit_mask_iff exp_eq_zero_iff min_def)
+    moreover define r where \<open>r = m - q\<close>
+    ultimately have \<open>m = q + r\<close>
+      by simp
+    moreover from \<open>m = q + r\<close> \<open>2 ^ m \<noteq> 0\<close> have \<open>2 ^ q \<noteq> 0\<close> \<open>2 ^ r \<noteq> 0\<close>
+      using exp_add_not_zero_imp_left [of q r] exp_add_not_zero_imp_right [of q r]
+      by simp_all
+    moreover from \<open>2 ^ q \<noteq> 0\<close> have \<open>2 ^ (q - n) \<noteq> 0\<close>
+      by (rule exp_not_zero_imp_exp_diff_not_zero)
+    ultimately show ?thesis
+      by (auto simp add: bit_signed_iff bit_signed_take_bit_iff bit_push_bit_iff Parity.bit_push_bit_iff
+      min_def * exp_eq_zero_iff le_diff_conv2)
   next
     case False
     then show ?thesis
-      by (simp add: * bit_signed_iff bit_push_bit_iff Parity.bit_push_bit_iff bit_or_iff bit_take_bit_iff bit_not_iff bit_mask_iff)
+      using exp_not_zero_imp_exp_diff_not_zero [of m n]
+      by (auto simp add: bit_signed_iff bit_signed_take_bit_iff bit_push_bit_iff Parity.bit_push_bit_iff
+      min_def not_le not_less * le_diff_conv2 less_diff_conv2 Parity.exp_eq_0_imp_not_bit exp_eq_0_imp_not_bit
+      exp_eq_zero_iff)
   qed
 qed
 
@@ -274,30 +318,35 @@
   \<open>signed (take_bit n w) = (if n < LENGTH('b) then take_bit n (signed w) else signed w)\<close>
   for w :: \<open>'b::len word\<close>
   by (transfer fixing: take_bit; cases \<open>LENGTH('b)\<close>)
-    (auto simp add: signed_take_bit_take_bit take_bit_signed_take_bit take_bit_of_int min_def)
+    (auto simp add: Bit_Operations.signed_take_bit_take_bit Bit_Operations.take_bit_signed_take_bit take_bit_of_int min_def less_Suc_eq)
 
 lemma signed_not_eq:
-  \<open>signed (NOT w) = take_bit LENGTH('b) (NOT (signed w)) OR of_bool (bit (NOT (signed w)) LENGTH('b)) * NOT (mask LENGTH('b))\<close>
+  \<open>signed (NOT w) = signed_take_bit LENGTH('b) (NOT (signed w))\<close>
   for w :: \<open>'b::len word\<close>
 proof (rule bit_eqI)
   fix n
   assume \<open>2 ^ n \<noteq> 0\<close>
+  define q where \<open>q = LENGTH('b) - Suc 0\<close>
+  then have *: \<open>LENGTH('b) = Suc q\<close>
+    by simp
   show \<open>bit (signed (NOT w)) n \<longleftrightarrow>
-    bit (take_bit LENGTH('b) (NOT (signed w)) OR
-    of_bool (bit (NOT (signed w)) LENGTH('b)) * NOT (mask LENGTH('b))) n\<close>
-  proof (cases \<open>LENGTH('b) \<le> n\<close>)
+    bit (signed_take_bit LENGTH('b) (NOT (signed w))) n\<close>
+  proof (cases \<open>q < n\<close>)
+    case True
+    moreover define r where \<open>r = n - Suc q\<close>
+    ultimately have \<open>n = r + Suc q\<close>
+      by simp
+    moreover from \<open>2 ^ n \<noteq> 0\<close> \<open>n = r + Suc q\<close>
+      have \<open>2 ^ Suc q \<noteq> 0\<close>
+      using exp_add_not_zero_imp_right by blast 
+    ultimately show ?thesis
+      by (simp add: * bit_signed_iff bit_not_iff bit_signed_take_bit_iff Bit_Operations.bit_not_iff min_def
+        exp_eq_zero_iff)
+  next
     case False
     then show ?thesis
-      by (auto simp add: bit_signed_iff bit_not_iff bit_or_iff bit_take_bit_iff bit_mask_iff Bit_Operations.bit_not_iff exp_eq_zero_iff)
-  next
-    case True
-    moreover define q where \<open>q = n - LENGTH('b)\<close>
-    ultimately have \<open>n = LENGTH('b) + q\<close>
-      by simp
-    with \<open>2 ^ n \<noteq> 0\<close> have \<open>2 ^ q \<noteq> 0\<close> \<open>2 ^ LENGTH('b) \<noteq> 0\<close>
-      by (simp_all add: power_add) (use mult_not_zero in blast)+
-    then show ?thesis
-      by (simp add: bit_signed_iff bit_not_iff bit_or_iff bit_take_bit_iff bit_mask_iff Bit_Operations.bit_not_iff exp_eq_zero_iff min_def not_le not_less le_diff_conv le_Suc_eq)
+      by (auto simp add: * bit_signed_iff bit_not_iff bit_signed_take_bit_iff Bit_Operations.bit_not_iff min_def
+        exp_eq_zero_iff)
   qed
 qed
 
@@ -374,15 +423,15 @@
 qed
 
 lemma [transfer_rule]:
-  \<open>(pcr_word ===> pcr_word) (signed_take_bit (LENGTH('a) - 1)) (scast :: 'a::len word \<Rightarrow> 'b::len word)\<close>
+  \<open>(pcr_word ===> pcr_word) (signed_take_bit (LENGTH('a) - Suc 0)) (scast :: 'a::len word \<Rightarrow> 'b::len word)\<close>
 proof (rule rel_funI)
   fix k :: int and w :: \<open>'a word\<close>
   assume \<open>pcr_word k w\<close>
   then have \<open>w = word_of_int k\<close>
     by (simp add: pcr_word_def cr_word_def relcompp_apply)
-  moreover have \<open>pcr_word (signed_take_bit (LENGTH('a) - 1) k) (scast (word_of_int k :: 'a word))\<close>
+  moreover have \<open>pcr_word (signed_take_bit (LENGTH('a) - Suc 0) k) (scast (word_of_int k :: 'a word))\<close>
     by transfer (simp add: pcr_word_def cr_word_def relcompp_apply)
-  ultimately show \<open>pcr_word (signed_take_bit (LENGTH('a) - 1) k) (scast w)\<close>
+  ultimately show \<open>pcr_word (signed_take_bit (LENGTH('a) - Suc 0) k) (scast w)\<close>
     by simp
 qed
 
@@ -444,24 +493,12 @@
   \<open>of_int (sint a) = signed a\<close>
   by transfer (simp_all add: take_bit_signed_take_bit)
 
-lemma sint_not_eq:
-  \<open>sint (NOT w) = signed_take_bit LENGTH('a) (NOT (sint w))\<close>
-  for w :: \<open>'a::len word\<close>
-  by (simp add: signed_not_eq signed_take_bit_unfold)
-
-lemma sint_push_bit_eq:
-  \<open>signed (push_bit n w) = signed_take_bit (LENGTH('a) - 1) (push_bit n (signed w))\<close>
-  for w :: \<open>'a::len word\<close>
-  by (transfer fixing: n; cases \<open>LENGTH('a)\<close>)
-     (auto simp add: signed_take_bit_def bit_concat_bit_iff bit_push_bit_iff bit_take_bit_iff bit_or_iff le_diff_conv2,
-        auto simp add: take_bit_push_bit not_less concat_bit_eq_iff take_bit_concat_bit_eq le_diff_conv2)
-
 lemma sint_greater_eq:
-  \<open>- (2 ^ (LENGTH('a) - 1)) \<le> sint w\<close> for w :: \<open>'a::len word\<close>
-proof (cases \<open>bit w (LENGTH('a) - 1)\<close>)
+  \<open>- (2 ^ (LENGTH('a) - Suc 0)) \<le> sint w\<close> for w :: \<open>'a::len word\<close>
+proof (cases \<open>bit w (LENGTH('a) - Suc 0)\<close>)
   case True
   then show ?thesis
-    by transfer (simp add: signed_take_bit_eq_or minus_exp_eq_not_mask or_greater_eq ac_simps)
+    by transfer (simp add: signed_take_bit_eq_if_negative minus_exp_eq_not_mask or_greater_eq ac_simps)
 next
   have *: \<open>- (2 ^ (LENGTH('a) - Suc 0)) \<le> (0::int)\<close>
     by simp
@@ -471,8 +508,49 @@
 qed
 
 lemma sint_less:
-  \<open>sint w < 2 ^ (LENGTH('a) - 1)\<close> for w :: \<open>'a::len word\<close>
-  by (cases \<open>bit w (LENGTH('a) - 1)\<close>; transfer)
-    (simp_all add: signed_take_bit_eq signed_take_bit_unfold take_bit_int_less_exp not_eq_complement mask_eq_exp_minus_1 OR_upper)
+  \<open>sint w < 2 ^ (LENGTH('a) - Suc 0)\<close> for w :: \<open>'a::len word\<close>
+  by (cases \<open>bit w (LENGTH('a) - Suc 0)\<close>; transfer)
+    (simp_all add: signed_take_bit_eq signed_take_bit_def take_bit_int_less_exp not_eq_complement mask_eq_exp_minus_1 OR_upper)
+
+context semiring_bit_shifts
+begin
+
+lemma unsigned_ucast_eq:
+  \<open>unsigned (ucast w :: 'c::len word) = take_bit LENGTH('c) (unsigned w)\<close>
+  for w :: \<open>'b::len word\<close>
+  by (rule bit_eqI) (simp add: bit_unsigned_iff Conversions.bit_unsigned_iff bit_take_bit_iff exp_eq_zero_iff not_le)
 
 end
+
+context ring_bit_operations
+begin
+
+lemma signed_ucast_eq:
+  \<open>signed (ucast w :: 'c::len word) = signed_take_bit (LENGTH('c) - Suc 0) (unsigned w)\<close>
+  for w :: \<open>'b::len word\<close>
+proof (rule bit_eqI)
+  fix n
+  assume \<open>2 ^ n \<noteq> 0\<close>
+  then have \<open>2 ^ (min (LENGTH('c) - Suc 0) n) \<noteq> 0\<close>
+    by (simp add: min_def)
+      (metis (mono_tags) diff_diff_cancel local.exp_not_zero_imp_exp_diff_not_zero)
+  then show \<open>bit (signed (ucast w :: 'c::len word)) n \<longleftrightarrow> bit (signed_take_bit (LENGTH('c) - Suc 0) (unsigned w)) n\<close>
+    by (simp add: bit_signed_iff bit_unsigned_iff Conversions.bit_unsigned_iff bit_signed_take_bit_iff exp_eq_zero_iff not_le)
+qed
+
+lemma signed_scast_eq:
+  \<open>signed (scast w :: 'c::len word) = signed_take_bit (LENGTH('c) - Suc 0) (signed w)\<close>
+  for w :: \<open>'b::len word\<close>
+proof (rule bit_eqI)
+  fix n
+  assume \<open>2 ^ n \<noteq> 0\<close>
+  then have \<open>2 ^ (min (LENGTH('c) - Suc 0) n) \<noteq> 0\<close>
+    by (simp add: min_def)
+      (metis (mono_tags) diff_diff_cancel local.exp_not_zero_imp_exp_diff_not_zero)
+  then show \<open>bit (signed (scast w :: 'c::len word)) n \<longleftrightarrow> bit (signed_take_bit (LENGTH('c) - Suc 0) (signed w)) n\<close>
+    by (simp add: bit_signed_iff bit_unsigned_iff Conversions.bit_signed_iff bit_signed_take_bit_iff exp_eq_zero_iff not_le)
+qed
+
+end
+
+end
diff -r cbe7aa1c2bdc -r 9c6787cfd70e src/HOL/Word/More_Word.thy
--- a/src/HOL/Word/More_Word.thy	Tue Sep 08 15:30:15 2020 +0100
+++ b/src/HOL/Word/More_Word.thy	Tue Sep 08 15:30:37 2020 +0100
@@ -37,6 +37,11 @@
 lemmas word_sle_def = word_sle_eq
 lemmas word_sless_def = word_sless_eq
 
+lemmas uint_0 = uint_nonnegative
+lemmas uint_lt = uint_bounded
+lemmas uint_mod_same = uint_idem
+lemmas of_nth_def = word_set_bits_def
+
 lemma shiftl_transfer [transfer_rule]:
   includes lifting_syntax
   shows "(pcr_word ===> (=) ===> pcr_word) (<<) (<<)"
diff -r cbe7aa1c2bdc -r 9c6787cfd70e src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Tue Sep 08 15:30:15 2020 +0100
+++ b/src/HOL/Word/Word.thy	Tue Sep 08 15:30:37 2020 +0100
@@ -15,52 +15,7 @@
   Misc_Typedef
 begin
 
-subsection \<open>Type definition\<close>
-
-quotient_type (overloaded) 'a word = int / \<open>\<lambda>k l. take_bit LENGTH('a) k = take_bit LENGTH('a::len) l\<close>
-  morphisms rep_word Word by (auto intro!: equivpI reflpI sympI transpI)
-
-hide_const (open) Word \<comment> \<open>only for code generation\<close>
-
-lift_definition word_of_int :: \<open>int \<Rightarrow> 'a::len word\<close>
-  is \<open>\<lambda>k. k\<close> .
-
-lift_definition uint :: \<open>'a::len word \<Rightarrow> int\<close>
-  is \<open>take_bit LENGTH('a)\<close> .
-
-lemma uint_nonnegative: "0 \<le> uint w"
-  by transfer simp
-
-lemma uint_bounded: "uint w < 2 ^ LENGTH('a)"
-  for w :: "'a::len word"
-  by transfer (simp add: take_bit_eq_mod)
-
-lemma uint_idem: "uint w mod 2 ^ LENGTH('a) = uint w"
-  for w :: "'a::len word"
-  using uint_nonnegative uint_bounded by (rule mod_pos_pos_trivial)
-
-lemma word_uint_eqI: "uint a = uint b \<Longrightarrow> a = b"
-  by transfer simp
-
-lemma word_uint_eq_iff: "a = b \<longleftrightarrow> uint a = uint b"
-  using word_uint_eqI by auto
-
-lemma uint_word_of_int: "uint (word_of_int k :: 'a::len word) = k mod 2 ^ LENGTH('a)"
-  by transfer (simp add: take_bit_eq_mod)
-  
-lemma word_of_int_uint: "word_of_int (uint w) = w"
-  by transfer simp
-
-lemma split_word_all: "(\<And>x::'a::len word. PROP P x) \<equiv> (\<And>x. PROP P (word_of_int x))"
-proof
-  fix x :: "'a word"
-  assume "\<And>x. PROP P (word_of_int x)"
-  then have "PROP P (word_of_int (uint x))" .
-  then show "PROP P x" by (simp add: word_of_int_uint)
-qed
-
-
-subsection \<open>Type conversions and casting\<close>
+subsection \<open>Preliminaries\<close>
 
 lemma signed_take_bit_decr_length_iff:
   \<open>signed_take_bit (LENGTH('a::len) - Suc 0) k = signed_take_bit (LENGTH('a) - Suc 0) l
@@ -68,410 +23,85 @@
   by (cases \<open>LENGTH('a)\<close>)
     (simp_all add: signed_take_bit_eq_iff_take_bit_eq)
 
-lift_definition sint :: \<open>'a::len word \<Rightarrow> int\<close>
-  \<comment> \<open>treats the most-significant bit as a sign bit\<close>
-  is \<open>signed_take_bit (LENGTH('a) - 1)\<close>  
-  by (simp add: signed_take_bit_decr_length_iff)
-
-lemma sint_uint [code]:
-  \<open>sint w = signed_take_bit (LENGTH('a) - 1) (uint w)\<close>
-  for w :: \<open>'a::len word\<close>
-  by (cases \<open>LENGTH('a)\<close>; transfer) (simp_all add: signed_take_bit_take_bit)
-
-lift_definition unat :: \<open>'a::len word \<Rightarrow> nat\<close>
-  is \<open>nat \<circ> take_bit LENGTH('a)\<close>
-  by transfer simp
-
-lemma nat_uint_eq [simp]:
-  \<open>nat (uint w) = unat w\<close>
-  by transfer simp
-
-lemma unat_eq_nat_uint [code]:
-  \<open>unat w = nat (uint w)\<close>
-  by simp
-
-lift_definition ucast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close>
-  is \<open>take_bit LENGTH('a)\<close>
-  by simp
-
-lemma ucast_eq [code]:
-  \<open>ucast w = word_of_int (uint w)\<close>
-  by transfer simp
-
-lift_definition scast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close>
-  is \<open>signed_take_bit (LENGTH('a) - 1)\<close>
-  by (simp flip: signed_take_bit_decr_length_iff)
-
-lemma scast_eq [code]:
-  \<open>scast w = word_of_int (sint w)\<close>
-  by transfer simp
-
-instantiation word :: (len) size
+
+subsection \<open>Fundamentals\<close>
+
+subsubsection \<open>Type definition\<close>
+
+quotient_type (overloaded) 'a word = int / \<open>\<lambda>k l. take_bit LENGTH('a) k = take_bit LENGTH('a::len) l\<close>
+  morphisms rep Word by (auto intro!: equivpI reflpI sympI transpI)
+
+hide_const (open) rep \<comment> \<open>only for foundational purpose\<close>
+hide_const (open) Word \<comment> \<open>only for code generation\<close>
+
+
+subsubsection \<open>Basic arithmetic\<close>
+
+instantiation word :: (len) comm_ring_1
 begin
 
-lift_definition size_word :: \<open>'a word \<Rightarrow> nat\<close>
-  is \<open>\<lambda>_. LENGTH('a)\<close> ..
-
-instance ..
-
-end
-
-lemma word_size [code]:
-  \<open>size w = LENGTH('a)\<close> for w :: \<open>'a::len word\<close>
-  by (fact size_word.rep_eq)
-
-lemma word_size_gt_0 [iff]: "0 < size w"
-  for w :: "'a::len word"
-  by (simp add: word_size)
-
-lemmas lens_gt_0 = word_size_gt_0 len_gt_0
-
-lemma lens_not_0 [iff]:
-  \<open>size w \<noteq> 0\<close> for  w :: \<open>'a::len word\<close>
-  by auto
-
-lift_definition source_size :: \<open>('a::len word \<Rightarrow> 'b) \<Rightarrow> nat\<close>
-  is \<open>\<lambda>_. LENGTH('a)\<close> .
-
-lift_definition target_size :: \<open>('a \<Rightarrow> 'b::len word) \<Rightarrow> nat\<close>
-  is \<open>\<lambda>_. LENGTH('b)\<close> ..
-
-lift_definition is_up :: \<open>('a::len word \<Rightarrow> 'b::len word) \<Rightarrow> bool\<close>
-  is \<open>\<lambda>_. LENGTH('a) \<le> LENGTH('b)\<close> ..
-
-lift_definition is_down :: \<open>('a::len word \<Rightarrow> 'b::len word) \<Rightarrow> bool\<close>
-  is \<open>\<lambda>_. LENGTH('a) \<ge> LENGTH('b)\<close> ..
-
-lemma is_up_eq:
-  \<open>is_up f \<longleftrightarrow> source_size f \<le> target_size f\<close>
-  for f :: \<open>'a::len word \<Rightarrow> 'b::len word\<close>
-  by (simp add: source_size.rep_eq target_size.rep_eq is_up.rep_eq)
-
-lemma is_down_eq:
-  \<open>is_down f \<longleftrightarrow> target_size f \<le> source_size f\<close>
-  for f :: \<open>'a::len word \<Rightarrow> 'b::len word\<close>
-  by (simp add: source_size.rep_eq target_size.rep_eq is_down.rep_eq)
-
-lift_definition word_int_case :: \<open>(int \<Rightarrow> 'b) \<Rightarrow> 'a::len word \<Rightarrow> 'b\<close>
-  is \<open>\<lambda>f. f \<circ> take_bit LENGTH('a)\<close> by simp
-
-lemma word_int_case_eq_uint [code]:
-  \<open>word_int_case f w = f (uint w)\<close>
-  by transfer simp
-
-translations
-  "case x of XCONST of_int y \<Rightarrow> b" \<rightleftharpoons> "CONST word_int_case (\<lambda>y. b) x"
-  "case x of (XCONST of_int :: 'a) y \<Rightarrow> b" \<rightharpoonup> "CONST word_int_case (\<lambda>y. b) x"
-
-
-subsection \<open>Basic code generation setup\<close>
-
-lemma Word_eq_word_of_int [code_post]:
-  \<open>Word.Word = word_of_int\<close>
-  by rule (transfer, rule)
-
-lemma [code abstype]:
-  \<open>Word.Word (uint w) = w\<close>
-  by transfer simp
-
-lemma [code abstract]:
-  \<open>uint (word_of_int k :: 'a::len word) = take_bit LENGTH('a) k\<close>
-  by transfer rule
-
-instantiation word :: (len) equal
-begin
-
-lift_definition equal_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> bool\<close>
-  is \<open>\<lambda>k l. take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close>
-  by simp
+lift_definition zero_word :: \<open>'a word\<close>
+  is 0 .
+
+lift_definition one_word :: \<open>'a word\<close>
+  is 1 .
+
+lift_definition plus_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
+  is \<open>(+)\<close>
+  by (auto simp add: take_bit_eq_mod intro: mod_add_cong)
+
+lift_definition minus_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
+  is \<open>(-)\<close>
+  by (auto simp add: take_bit_eq_mod intro: mod_diff_cong)
+
+lift_definition uminus_word :: \<open>'a word \<Rightarrow> 'a word\<close>
+  is uminus
+  by (auto simp add: take_bit_eq_mod intro: mod_minus_cong)
+
+lift_definition times_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
+  is \<open>(*)\<close>
+  by (auto simp add: take_bit_eq_mod intro: mod_mult_cong)
 
 instance
-  by (standard; transfer) rule
+  by (standard; transfer) (simp_all add: algebra_simps)
 
 end
 
-lemma [code]:
-  \<open>HOL.equal k l \<longleftrightarrow> HOL.equal (uint k) (uint l)\<close>
-  by transfer (simp add: equal)
-
-notation fcomp (infixl "\<circ>>" 60)
-notation scomp (infixl "\<circ>\<rightarrow>" 60)
-
-instantiation word :: ("{len, typerep}") random
-begin
-
-definition
-  "random_word i = Random.range i \<circ>\<rightarrow> (\<lambda>k. Pair (
-     let j = word_of_int (int_of_integer (integer_of_natural k)) :: 'a word
-     in (j, \<lambda>_::unit. Code_Evaluation.term_of j)))"
-
-instance ..
-
-end
-
-no_notation fcomp (infixl "\<circ>>" 60)
-no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
-
-
-subsection \<open>Type-definition locale instantiations\<close>
-
-lemmas uint_0 = uint_nonnegative (* FIXME duplicate *)
-lemmas uint_lt = uint_bounded (* FIXME duplicate *)
-lemmas uint_mod_same = uint_idem (* FIXME duplicate *)
-
-definition uints :: "nat \<Rightarrow> int set"
-  \<comment> \<open>the sets of integers representing the words\<close>
-  where "uints n = range (take_bit n)"
-
-definition sints :: "nat \<Rightarrow> int set"
-  where "sints n = range (signed_take_bit (n - 1))"
-
-lemma uints_num: "uints n = {i. 0 \<le> i \<and> i < 2 ^ n}"
-  by (simp add: uints_def range_bintrunc)
-
-lemma sints_num: "sints n = {i. - (2 ^ (n - 1)) \<le> i \<and> i < 2 ^ (n - 1)}"
-  by (simp add: sints_def range_sbintrunc)
-
-definition unats :: "nat \<Rightarrow> nat set"
-  where "unats n = {i. i < 2 ^ n}"
-
-\<comment> \<open>naturals\<close>
-lemma uints_unats: "uints n = int ` unats n"
-  apply (unfold unats_def uints_num)
-  apply safe
-    apply (rule_tac image_eqI)
-     apply (erule_tac nat_0_le [symmetric])
-  by auto
-
-lemma unats_uints: "unats n = nat ` uints n"
-  by (auto simp: uints_unats image_iff)
-
-lemma td_ext_uint:
-  "td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (LENGTH('a::len)))
-    (\<lambda>w::int. w mod 2 ^ LENGTH('a))"
-  apply (unfold td_ext_def')
-  apply transfer
-  apply (simp add: uints_num take_bit_eq_mod)
-  done
-
-interpretation word_uint:
-  td_ext
-    "uint::'a::len word \<Rightarrow> int"
-    word_of_int
-    "uints (LENGTH('a::len))"
-    "\<lambda>w. w mod 2 ^ LENGTH('a::len)"
-  by (fact td_ext_uint)
-
-lemmas td_uint = word_uint.td_thm
-lemmas int_word_uint = word_uint.eq_norm
-
-lemma td_ext_ubin:
-  "td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (LENGTH('a::len)))
-    (take_bit (LENGTH('a)))"
-  apply standard
-  apply transfer
-  apply simp
-  done
-
-interpretation word_ubin:
-  td_ext
-    "uint::'a::len word \<Rightarrow> int"
-    word_of_int
-    "uints (LENGTH('a::len))"
-    "take_bit (LENGTH('a::len))"
-  by (fact td_ext_ubin)
-
-
-subsection \<open>Arithmetic operations\<close>
-
-lift_definition word_succ :: "'a::len word \<Rightarrow> 'a word" is "\<lambda>x. x + 1"
-  by (auto simp add: take_bit_eq_mod intro: mod_add_cong)
-
-lift_definition word_pred :: "'a::len word \<Rightarrow> 'a word" is "\<lambda>x. x - 1"
-  by (auto simp add: take_bit_eq_mod intro: mod_diff_cong)
-
-instantiation word :: (len) "{neg_numeral, modulo, comm_monoid_mult, comm_ring}"
-begin
-
-lift_definition zero_word :: "'a word" is "0" .
-
-lift_definition one_word :: "'a word" is "1" .
-
-lift_definition plus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "(+)"
-  by (auto simp add: take_bit_eq_mod intro: mod_add_cong)
-
-lift_definition minus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "(-)"
-  by (auto simp add: take_bit_eq_mod intro: mod_diff_cong)
-
-lift_definition uminus_word :: "'a word \<Rightarrow> 'a word" is uminus
-  by (auto simp add: take_bit_eq_mod intro: mod_minus_cong)
-
-lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "(*)"
-  by (auto simp add: take_bit_eq_mod intro: mod_mult_cong)
-
-lift_definition divide_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
-  is "\<lambda>a b. take_bit LENGTH('a) a div take_bit LENGTH('a) b"
-  by simp
-
-lift_definition modulo_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
-  is "\<lambda>a b. take_bit LENGTH('a) a mod take_bit LENGTH('a) b"
-  by simp
-
-instance
-  by standard (transfer, simp add: algebra_simps)+
-
-end
-
-lemma uint_0_eq [simp, code]:
-  \<open>uint 0 = 0\<close>
-  by transfer simp
-
-quickcheck_generator word
-  constructors:
-    \<open>0 :: 'a::len word\<close>,
-    \<open>numeral :: num \<Rightarrow> 'a::len word\<close>,
-    \<open>uminus :: 'a word \<Rightarrow> 'a::len word\<close>
-
-lemma uint_1_eq [simp, code]:
-  \<open>uint 1 = 1\<close>
-  by transfer simp
-
-lemma word_div_def [code]:
-  "a div b = word_of_int (uint a div uint b)"
-  by transfer rule
-
-lemma word_mod_def [code]:
-  "a mod b = word_of_int (uint a mod uint b)"
-  by transfer rule
-
 context
   includes lifting_syntax
-  notes power_transfer [transfer_rule]
+  notes
+    power_transfer [transfer_rule]
+    transfer_rule_of_bool [transfer_rule]
+    transfer_rule_numeral [transfer_rule]
+    transfer_rule_of_nat [transfer_rule]
+    transfer_rule_of_int [transfer_rule]
+
 begin
 
 lemma power_transfer_word [transfer_rule]:
   \<open>(pcr_word ===> (=) ===> pcr_word) (^) (^)\<close>
   by transfer_prover
 
-end
-
-
-text \<open>Legacy theorems:\<close>
-
-lemma word_add_def [code]:
-  "a + b = word_of_int (uint a + uint b)"
-  by transfer (simp add: take_bit_add)
-
-lemma word_sub_wi [code]:
-  "a - b = word_of_int (uint a - uint b)"
-  by transfer (simp add: take_bit_diff)
-
-lemma word_mult_def [code]:
-  "a * b = word_of_int (uint a * uint b)"
-  by transfer (simp add: take_bit_eq_mod mod_simps)
-
-lemma word_minus_def [code]:
-  "- a = word_of_int (- uint a)"
-  by transfer (simp add: take_bit_minus)
-
-lemma word_succ_alt [code]:
-  "word_succ a = word_of_int (uint a + 1)"
-  by transfer (simp add: take_bit_eq_mod mod_simps)
-
-lemma word_pred_alt [code]:
-  "word_pred a = word_of_int (uint a - 1)"
-  by transfer (simp add: take_bit_eq_mod mod_simps)
-
-lemma word_0_wi:
-  "0 = word_of_int 0"
-  by transfer simp
-
-lemma word_1_wi:
-  "1 = word_of_int 1"
-  by transfer simp
-
-lemmas word_arith_wis = 
-  word_add_def word_sub_wi word_mult_def
-  word_minus_def word_succ_alt word_pred_alt
-  word_0_wi word_1_wi
-
-lemma wi_homs:
-  shows wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)"
-    and wi_hom_sub: "word_of_int a - word_of_int b = word_of_int (a - b)"
-    and wi_hom_mult: "word_of_int a * word_of_int b = word_of_int (a * b)"
-    and wi_hom_neg: "- word_of_int a = word_of_int (- a)"
-    and wi_hom_succ: "word_succ (word_of_int a) = word_of_int (a + 1)"
-    and wi_hom_pred: "word_pred (word_of_int a) = word_of_int (a - 1)"
-  by (transfer, simp)+
-
-lemmas wi_hom_syms = wi_homs [symmetric]
-
-lemmas word_of_int_homs = wi_homs word_0_wi word_1_wi
-
-lemmas word_of_int_hom_syms = word_of_int_homs [symmetric]
-
-instance word :: (len) comm_monoid_add ..
-
-instance word :: (len) semiring_numeral ..
-
-instance word :: (len) comm_ring_1
-proof
-  have *: "0 < LENGTH('a)" by (rule len_gt_0)
-  show "(0::'a word) \<noteq> 1"
-    by transfer (use * in \<open>auto simp add: gr0_conv_Suc\<close>)
-qed
-
-lemma word_of_nat: "of_nat n = word_of_int (int n)"
-  by (induct n) (auto simp add : word_of_int_hom_syms)
-
-lemma word_of_int: "of_int = word_of_int"
-  apply (rule ext)
-  apply (case_tac x rule: int_diff_cases)
-  apply (simp add: word_of_nat wi_hom_sub)
-  done
-
-context
-  includes lifting_syntax
-  notes 
-    transfer_rule_of_bool [transfer_rule]
-    transfer_rule_numeral [transfer_rule]
-    transfer_rule_of_nat [transfer_rule]
-    transfer_rule_of_int [transfer_rule]
-begin
+lemma [transfer_rule]:
+  \<open>((=) ===> pcr_word) of_bool of_bool\<close>
+  by transfer_prover
 
 lemma [transfer_rule]:
-  "((=) ===> pcr_word) of_bool of_bool"
+  \<open>((=) ===> pcr_word) numeral numeral\<close>
   by transfer_prover
 
 lemma [transfer_rule]:
-  "((=) ===> pcr_word) numeral numeral"
+  \<open>((=) ===> pcr_word) int of_nat\<close>
   by transfer_prover
 
 lemma [transfer_rule]:
-  "((=) ===> pcr_word) int of_nat"
-  by transfer_prover
-
-lemma [transfer_rule]:
-  "((=) ===> pcr_word) (\<lambda>k. k) of_int"
+  \<open>((=) ===> pcr_word) (\<lambda>k. k) of_int\<close>
 proof -
-  have "((=) ===> pcr_word) of_int of_int"
+  have \<open>((=) ===> pcr_word) of_int of_int\<close>
     by transfer_prover
   then show ?thesis by (simp add: id_def)
 qed
 
-end
-
-lemma word_of_int_eq:
-  "word_of_int = of_int"
-  by (rule ext) (transfer, rule)
-
-definition udvd :: "'a::len word \<Rightarrow> 'a::len word \<Rightarrow> bool" (infixl "udvd" 50)
-  where "a udvd b = (\<exists>n\<ge>0. uint b = n * uint a)"
-
-context
-  includes lifting_syntax
-begin
-
 lemma [transfer_rule]:
   \<open>(pcr_word ===> (\<longleftrightarrow>)) even ((dvd) 2 :: 'a::len word \<Rightarrow> bool)\<close>
 proof -
@@ -495,68 +125,106 @@
 
 end
 
-instance word :: (len) semiring_modulo
-proof
-  show "a div b * b + a mod b = a" for a b :: "'a word"
-  proof transfer
-    fix k l :: int
-    define r :: int where "r = 2 ^ LENGTH('a)"
-    then have r: "take_bit LENGTH('a) k = k mod r" for k
-      by (simp add: take_bit_eq_mod)
-    have "k mod r = ((k mod r) div (l mod r) * (l mod r)
-      + (k mod r) mod (l mod r)) mod r"
-      by (simp add: div_mult_mod_eq)
-    also have "... = (((k mod r) div (l mod r) * (l mod r)) mod r
-      + (k mod r) mod (l mod r)) mod r"
-      by (simp add: mod_add_left_eq)
-    also have "... = (((k mod r) div (l mod r) * l) mod r
-      + (k mod r) mod (l mod r)) mod r"
-      by (simp add: mod_mult_right_eq)
-    finally have "k mod r = ((k mod r) div (l mod r) * l
-      + (k mod r) mod (l mod r)) mod r"
-      by (simp add: mod_simps)
-    with r show "take_bit LENGTH('a) (take_bit LENGTH('a) k div take_bit LENGTH('a) l * l
-      + take_bit LENGTH('a) k mod take_bit LENGTH('a) l) = take_bit LENGTH('a) k"
-      by simp
-  qed
-qed
-
-instance word :: (len) semiring_parity
-proof
-  show "\<not> 2 dvd (1::'a word)"
-    by transfer simp
-  show even_iff_mod_2_eq_0: "2 dvd a \<longleftrightarrow> a mod 2 = 0"
-    for a :: "'a word"
-    by transfer (simp_all add: mod_2_eq_odd take_bit_Suc)
-  show "\<not> 2 dvd a \<longleftrightarrow> a mod 2 = 1"
-    for a :: "'a word"
-    by transfer (simp_all add: mod_2_eq_odd take_bit_Suc)
-qed
-
-lemma exp_eq_zero_iff:
-  \<open>2 ^ n = (0 :: 'a::len word) \<longleftrightarrow> n \<ge> LENGTH('a)\<close>
+lemma word_exp_length_eq_0 [simp]:
+  \<open>(2 :: 'a::len word) ^ LENGTH('a) = 0\<close>
+  by transfer simp
+
+
+subsubsection \<open>Basic code generation setup\<close>
+
+lift_definition uint :: \<open>'a::len word \<Rightarrow> int\<close>
+  is \<open>take_bit LENGTH('a)\<close> .
+
+lemma [code abstype]:
+  \<open>Word.Word (uint w) = w\<close>
+  by transfer simp
+
+quickcheck_generator word
+  constructors:
+    \<open>0 :: 'a::len word\<close>,
+    \<open>numeral :: num \<Rightarrow> 'a::len word\<close>
+
+instantiation word :: (len) equal
+begin
+
+lift_definition equal_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> bool\<close>
+  is \<open>\<lambda>k l. take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close>
+  by simp
+
+instance
+  by (standard; transfer) rule
+
+end
+
+lemma [code]:
+  \<open>HOL.equal v w \<longleftrightarrow> HOL.equal (uint v) (uint w)\<close>
+  by transfer (simp add: equal)
+
+lemma [code]:
+  \<open>uint 0 = 0\<close>
+  by transfer simp
+
+lemma [code]:
+  \<open>uint 1 = 1\<close>
   by transfer simp
 
-lemma double_eq_zero_iff:
-  \<open>2 * a = 0 \<longleftrightarrow> a = 0 \<or> a = 2 ^ (LENGTH('a) - Suc 0)\<close>
-  for a :: \<open>'a::len word\<close>
-proof -
-  define n where \<open>n = LENGTH('a) - Suc 0\<close>
-  then have *: \<open>LENGTH('a) = Suc n\<close>
-    by simp
-  have \<open>a = 0\<close> if \<open>2 * a = 0\<close> and \<open>a \<noteq> 2 ^ (LENGTH('a) - Suc 0)\<close>
-    using that by transfer
-      (auto simp add: take_bit_eq_0_iff take_bit_eq_mod *)
-  moreover have \<open>2 ^ LENGTH('a) = (0 :: 'a word)\<close>
-    by transfer simp
-  then have \<open>2 * 2 ^ (LENGTH('a) - Suc 0) = (0 :: 'a word)\<close>
-    by (simp add: *)
-  ultimately show ?thesis
-    by auto
-qed
-
-
-subsection \<open>Ordering\<close>
+lemma [code]:
+  \<open>uint (v + w) = take_bit LENGTH('a) (uint v + uint w)\<close>
+  for v w :: \<open>'a::len word\<close>
+  by transfer (simp add: take_bit_add)
+
+lemma [code]:
+  \<open>uint (- w) = (let k = uint w in if w = 0 then 0 else 2 ^ LENGTH('a) - k)\<close>
+  for w :: \<open>'a::len word\<close>
+  by transfer (auto simp add: take_bit_eq_mod zmod_zminus1_eq_if)
+
+lemma [code]:
+  \<open>uint (v - w) = take_bit LENGTH('a) (uint v - uint w)\<close>
+  for v w :: \<open>'a::len word\<close>
+  by transfer (simp add: take_bit_diff)
+
+lemma [code]:
+  \<open>uint (v * w) = take_bit LENGTH('a) (uint v * uint w)\<close>
+  for v w :: \<open>'a::len word\<close>
+  by transfer (simp add: take_bit_mult)
+
+
+subsubsection \<open>Basic conversions\<close>
+
+lift_definition word_of_int :: \<open>int \<Rightarrow> 'a::len word\<close>
+  is \<open>\<lambda>k. k\<close> .
+
+lift_definition unat :: \<open>'a::len word \<Rightarrow> nat\<close>
+  is \<open>nat \<circ> take_bit LENGTH('a)\<close>
+  by simp
+
+lift_definition sint :: \<open>'a::len word \<Rightarrow> int\<close>
+  \<comment> \<open>treats the most-significant bit as a sign bit\<close>
+  is \<open>signed_take_bit (LENGTH('a) - 1)\<close>  
+  by (simp add: signed_take_bit_decr_length_iff)
+
+lemma nat_uint_eq [simp]:
+  \<open>nat (uint w) = unat w\<close>
+  by transfer simp
+
+lemma of_nat_word_eq_iff:
+  \<open>of_nat m = (of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m = take_bit LENGTH('a) n\<close>
+  by transfer (simp add: take_bit_of_nat)
+
+lemma of_nat_word_eq_0_iff:
+  \<open>of_nat n = (0 :: 'a::len word) \<longleftrightarrow> 2 ^ LENGTH('a) dvd n\<close>
+  using of_nat_word_eq_iff [where ?'a = 'a, of n 0] by (simp add: take_bit_eq_0_iff)
+
+lemma of_int_word_eq_iff:
+  \<open>of_int k = (of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close>
+  by transfer rule
+
+lemma of_int_word_eq_0_iff:
+  \<open>of_int k = (0 :: 'a::len word) \<longleftrightarrow> 2 ^ LENGTH('a) dvd k\<close>
+  using of_int_word_eq_iff [where ?'a = 'a, of k 0] by (simp add: take_bit_eq_0_iff)
+
+
+subsubsection \<open>Basic ordering\<close>
 
 instantiation word :: (len) linorder
 begin
@@ -592,10 +260,6 @@
   \<open>a > 0 \<longleftrightarrow> a \<noteq> 0\<close> for a :: \<open>'a::len word\<close>
   by transfer (simp add: less_le)
 
-lemma of_nat_word_eq_iff:
-  \<open>of_nat m = (of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m = take_bit LENGTH('a) n\<close>
-  by transfer (simp add: take_bit_of_nat)
-
 lemma of_nat_word_less_eq_iff:
   \<open>of_nat m \<le> (of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m \<le> take_bit LENGTH('a) n\<close>
   by transfer (simp add: take_bit_of_nat)
@@ -604,14 +268,6 @@
   \<open>of_nat m < (of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m < take_bit LENGTH('a) n\<close>
   by transfer (simp add: take_bit_of_nat)
 
-lemma of_nat_word_eq_0_iff:
-  \<open>of_nat n = (0 :: 'a::len word) \<longleftrightarrow> 2 ^ LENGTH('a) dvd n\<close>
-  using of_nat_word_eq_iff [where ?'a = 'a, of n 0] by (simp add: take_bit_eq_0_iff)
-
-lemma of_int_word_eq_iff:
-  \<open>of_int k = (of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close>
-  by transfer rule
-
 lemma of_int_word_less_eq_iff:
   \<open>of_int k \<le> (of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k \<le> take_bit LENGTH('a) l\<close>
   by transfer rule
@@ -620,33 +276,59 @@
   \<open>of_int k < (of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k < take_bit LENGTH('a) l\<close>
   by transfer rule
 
-lemma of_int_word_eq_0_iff:
-  \<open>of_int k = (0 :: 'a::len word) \<longleftrightarrow> 2 ^ LENGTH('a) dvd k\<close>
-  using of_int_word_eq_iff [where ?'a = 'a, of k 0] by (simp add: take_bit_eq_0_iff)
-
-lift_definition word_sle :: \<open>'a::len word \<Rightarrow> 'a word \<Rightarrow> bool\<close>  (\<open>(_/ <=s _)\<close> [50, 51] 50)
-  is \<open>\<lambda>k l. signed_take_bit (LENGTH('a) - 1) k \<le> signed_take_bit (LENGTH('a) - 1) l\<close>
-  by (simp flip: signed_take_bit_decr_length_iff)
-
-lemma word_sle_eq [code]:
-  \<open>a <=s b \<longleftrightarrow> sint a \<le> sint b\<close>
-  by transfer simp
-  
-lift_definition word_sless :: \<open>'a::len word \<Rightarrow> 'a word \<Rightarrow> bool\<close>  (\<open>(_/ <s _)\<close> [50, 51] 50)
-  is \<open>\<lambda>k l. signed_take_bit (LENGTH('a) - 1) k < signed_take_bit (LENGTH('a) - 1) l\<close>
-  by (simp flip: signed_take_bit_decr_length_iff)
-
-lemma word_sless_eq:
-  \<open>x <s y \<longleftrightarrow> x <=s y \<and> x \<noteq> y\<close>
-  by transfer (simp add: signed_take_bit_decr_length_iff less_le)
-
-lemma [code]:
-  \<open>a <s b \<longleftrightarrow> sint a < sint b\<close>
-  by transfer simp
-
 
 subsection \<open>Bit-wise operations\<close>
 
+instantiation word :: (len) semiring_modulo
+begin
+
+lift_definition divide_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
+  is \<open>\<lambda>a b. take_bit LENGTH('a) a div take_bit LENGTH('a) b\<close>
+  by simp
+
+lift_definition modulo_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
+  is \<open>\<lambda>a b. take_bit LENGTH('a) a mod take_bit LENGTH('a) b\<close>
+  by simp
+
+instance proof
+  show "a div b * b + a mod b = a" for a b :: "'a word"
+  proof transfer
+    fix k l :: int
+    define r :: int where "r = 2 ^ LENGTH('a)"
+    then have r: "take_bit LENGTH('a) k = k mod r" for k
+      by (simp add: take_bit_eq_mod)
+    have "k mod r = ((k mod r) div (l mod r) * (l mod r)
+      + (k mod r) mod (l mod r)) mod r"
+      by (simp add: div_mult_mod_eq)
+    also have "... = (((k mod r) div (l mod r) * (l mod r)) mod r
+      + (k mod r) mod (l mod r)) mod r"
+      by (simp add: mod_add_left_eq)
+    also have "... = (((k mod r) div (l mod r) * l) mod r
+      + (k mod r) mod (l mod r)) mod r"
+      by (simp add: mod_mult_right_eq)
+    finally have "k mod r = ((k mod r) div (l mod r) * l
+      + (k mod r) mod (l mod r)) mod r"
+      by (simp add: mod_simps)
+    with r show "take_bit LENGTH('a) (take_bit LENGTH('a) k div take_bit LENGTH('a) l * l
+      + take_bit LENGTH('a) k mod take_bit LENGTH('a) l) = take_bit LENGTH('a) k"
+      by simp
+  qed
+qed
+
+end
+
+instance word :: (len) semiring_parity
+proof
+  show "\<not> 2 dvd (1::'a word)"
+    by transfer simp
+  show even_iff_mod_2_eq_0: "2 dvd a \<longleftrightarrow> a mod 2 = 0"
+    for a :: "'a word"
+    by transfer (simp_all add: mod_2_eq_odd take_bit_Suc)
+  show "\<not> 2 dvd a \<longleftrightarrow> a mod 2 = 1"
+    for a :: "'a word"
+    by transfer (simp_all add: mod_2_eq_odd take_bit_Suc)
+qed
+
 lemma word_bit_induct [case_names zero even odd]:
   \<open>P a\<close> if word_zero: \<open>P 0\<close>
     and word_even: \<open>\<And>a. P a \<Longrightarrow> 0 < a \<Longrightarrow> a < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> P (2 * a)\<close>
@@ -927,6 +609,376 @@
   \<open>\<not> bit w LENGTH('a)\<close> for w :: \<open>'a::len word\<close>
   by transfer simp
 
+
+subsection \<open>Conversions including casts\<close>
+
+lemma uint_nonnegative: "0 \<le> uint w"
+  by transfer simp
+
+lemma uint_bounded: "uint w < 2 ^ LENGTH('a)"
+  for w :: "'a::len word"
+  by transfer (simp add: take_bit_eq_mod)
+
+lemma uint_idem: "uint w mod 2 ^ LENGTH('a) = uint w"
+  for w :: "'a::len word"
+  using uint_nonnegative uint_bounded by (rule mod_pos_pos_trivial)
+
+lemma word_uint_eqI: "uint a = uint b \<Longrightarrow> a = b"
+  by transfer simp
+
+lemma word_uint_eq_iff: "a = b \<longleftrightarrow> uint a = uint b"
+  using word_uint_eqI by auto
+
+lemma Word_eq_word_of_int [code_post]:
+  \<open>Word.Word = word_of_int\<close>
+  by rule (transfer, rule)
+
+lemma uint_word_of_int_eq [code]:
+  \<open>uint (word_of_int k :: 'a::len word) = take_bit LENGTH('a) k\<close>
+  by transfer rule
+
+lemma uint_word_of_int: "uint (word_of_int k :: 'a::len word) = k mod 2 ^ LENGTH('a)"
+  by (simp add: uint_word_of_int_eq take_bit_eq_mod)
+  
+lemma word_of_int_uint: "word_of_int (uint w) = w"
+  by transfer simp
+
+lemma word_div_def [code]:
+  "a div b = word_of_int (uint a div uint b)"
+  by transfer rule
+
+lemma word_mod_def [code]:
+  "a mod b = word_of_int (uint a mod uint b)"
+  by transfer rule
+
+lemma split_word_all: "(\<And>x::'a::len word. PROP P x) \<equiv> (\<And>x. PROP P (word_of_int x))"
+proof
+  fix x :: "'a word"
+  assume "\<And>x. PROP P (word_of_int x)"
+  then have "PROP P (word_of_int (uint x))" .
+  then show "PROP P x" by (simp add: word_of_int_uint)
+qed
+
+lemma sint_uint [code]:
+  \<open>sint w = signed_take_bit (LENGTH('a) - 1) (uint w)\<close>
+  for w :: \<open>'a::len word\<close>
+  by (cases \<open>LENGTH('a)\<close>; transfer) (simp_all add: signed_take_bit_take_bit)
+
+lemma unat_eq_nat_uint [code]:
+  \<open>unat w = nat (uint w)\<close>
+  by simp
+
+lift_definition ucast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close>
+  is \<open>take_bit LENGTH('a)\<close>
+  by simp
+
+lemma ucast_eq [code]:
+  \<open>ucast w = word_of_int (uint w)\<close>
+  by transfer simp
+
+lift_definition scast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close>
+  is \<open>signed_take_bit (LENGTH('a) - 1)\<close>
+  by (simp flip: signed_take_bit_decr_length_iff)
+
+lemma scast_eq [code]:
+  \<open>scast w = word_of_int (sint w)\<close>
+  by transfer simp
+
+lemma uint_0_eq [simp]:
+  \<open>uint 0 = 0\<close>
+  by transfer simp
+
+lemma uint_1_eq [simp]:
+  \<open>uint 1 = 1\<close>
+  by transfer simp
+
+lemma word_m1_wi: "- 1 = word_of_int (- 1)"
+  by transfer rule
+
+lemma uint_0_iff: "uint x = 0 \<longleftrightarrow> x = 0"
+  by (simp add: word_uint_eq_iff)
+
+lemma unat_0_iff: "unat x = 0 \<longleftrightarrow> x = 0"
+  by transfer (auto intro: antisym)
+
+lemma unat_0 [simp]: "unat 0 = 0"
+  by transfer simp
+
+lemma unat_gt_0: "0 < unat x \<longleftrightarrow> x \<noteq> 0"
+  by (auto simp: unat_0_iff [symmetric])
+
+lemma ucast_0 [simp]: "ucast 0 = 0"
+  by transfer simp
+
+lemma sint_0 [simp]: "sint 0 = 0"
+  by (simp add: sint_uint)
+
+lemma scast_0 [simp]: "scast 0 = 0"
+  by transfer simp
+
+lemma sint_n1 [simp] : "sint (- 1) = - 1"
+  by transfer simp
+
+lemma scast_n1 [simp]: "scast (- 1) = - 1"
+  by transfer simp
+
+lemma uint_1: "uint (1::'a::len word) = 1"
+  by (fact uint_1_eq)
+
+lemma unat_1 [simp]: "unat (1::'a::len word) = 1"
+  by transfer simp
+
+lemma ucast_1 [simp]: "ucast (1::'a::len word) = 1"
+  by transfer simp
+
+instantiation word :: (len) size
+begin
+
+lift_definition size_word :: \<open>'a word \<Rightarrow> nat\<close>
+  is \<open>\<lambda>_. LENGTH('a)\<close> ..
+
+instance ..
+
+end
+
+lemma word_size [code]:
+  \<open>size w = LENGTH('a)\<close> for w :: \<open>'a::len word\<close>
+  by (fact size_word.rep_eq)
+
+lemma word_size_gt_0 [iff]: "0 < size w"
+  for w :: "'a::len word"
+  by (simp add: word_size)
+
+lemmas lens_gt_0 = word_size_gt_0 len_gt_0
+
+lemma lens_not_0 [iff]:
+  \<open>size w \<noteq> 0\<close> for  w :: \<open>'a::len word\<close>
+  by auto
+
+lift_definition source_size :: \<open>('a::len word \<Rightarrow> 'b) \<Rightarrow> nat\<close>
+  is \<open>\<lambda>_. LENGTH('a)\<close> .
+
+lift_definition target_size :: \<open>('a \<Rightarrow> 'b::len word) \<Rightarrow> nat\<close>
+  is \<open>\<lambda>_. LENGTH('b)\<close> ..
+
+lift_definition is_up :: \<open>('a::len word \<Rightarrow> 'b::len word) \<Rightarrow> bool\<close>
+  is \<open>\<lambda>_. LENGTH('a) \<le> LENGTH('b)\<close> ..
+
+lift_definition is_down :: \<open>('a::len word \<Rightarrow> 'b::len word) \<Rightarrow> bool\<close>
+  is \<open>\<lambda>_. LENGTH('a) \<ge> LENGTH('b)\<close> ..
+
+lemma is_up_eq:
+  \<open>is_up f \<longleftrightarrow> source_size f \<le> target_size f\<close>
+  for f :: \<open>'a::len word \<Rightarrow> 'b::len word\<close>
+  by (simp add: source_size.rep_eq target_size.rep_eq is_up.rep_eq)
+
+lemma is_down_eq:
+  \<open>is_down f \<longleftrightarrow> target_size f \<le> source_size f\<close>
+  for f :: \<open>'a::len word \<Rightarrow> 'b::len word\<close>
+  by (simp add: source_size.rep_eq target_size.rep_eq is_down.rep_eq)
+
+lift_definition word_int_case :: \<open>(int \<Rightarrow> 'b) \<Rightarrow> 'a::len word \<Rightarrow> 'b\<close>
+  is \<open>\<lambda>f. f \<circ> take_bit LENGTH('a)\<close> by simp
+
+lemma word_int_case_eq_uint [code]:
+  \<open>word_int_case f w = f (uint w)\<close>
+  by transfer simp
+
+translations
+  "case x of XCONST of_int y \<Rightarrow> b" \<rightleftharpoons> "CONST word_int_case (\<lambda>y. b) x"
+  "case x of (XCONST of_int :: 'a) y \<Rightarrow> b" \<rightharpoonup> "CONST word_int_case (\<lambda>y. b) x"
+
+
+subsection \<open>Arithmetic operations\<close>
+
+text \<open>Legacy theorems:\<close>
+
+lemma word_add_def [code]:
+  "a + b = word_of_int (uint a + uint b)"
+  by transfer (simp add: take_bit_add)
+
+lemma word_sub_wi [code]:
+  "a - b = word_of_int (uint a - uint b)"
+  by transfer (simp add: take_bit_diff)
+
+lemma word_mult_def [code]:
+  "a * b = word_of_int (uint a * uint b)"
+  by transfer (simp add: take_bit_eq_mod mod_simps)
+
+lemma word_minus_def [code]:
+  "- a = word_of_int (- uint a)"
+  by transfer (simp add: take_bit_minus)
+
+lemma word_0_wi:
+  "0 = word_of_int 0"
+  by transfer simp
+
+lemma word_1_wi:
+  "1 = word_of_int 1"
+  by transfer simp
+
+lift_definition word_succ :: "'a::len word \<Rightarrow> 'a word" is "\<lambda>x. x + 1"
+  by (auto simp add: take_bit_eq_mod intro: mod_add_cong)
+
+lift_definition word_pred :: "'a::len word \<Rightarrow> 'a word" is "\<lambda>x. x - 1"
+  by (auto simp add: take_bit_eq_mod intro: mod_diff_cong)
+
+lemma word_succ_alt [code]:
+  "word_succ a = word_of_int (uint a + 1)"
+  by transfer (simp add: take_bit_eq_mod mod_simps)
+
+lemma word_pred_alt [code]:
+  "word_pred a = word_of_int (uint a - 1)"
+  by transfer (simp add: take_bit_eq_mod mod_simps)
+
+lemmas word_arith_wis = 
+  word_add_def word_sub_wi word_mult_def
+  word_minus_def word_succ_alt word_pred_alt
+  word_0_wi word_1_wi
+
+lemma wi_homs:
+  shows wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)"
+    and wi_hom_sub: "word_of_int a - word_of_int b = word_of_int (a - b)"
+    and wi_hom_mult: "word_of_int a * word_of_int b = word_of_int (a * b)"
+    and wi_hom_neg: "- word_of_int a = word_of_int (- a)"
+    and wi_hom_succ: "word_succ (word_of_int a) = word_of_int (a + 1)"
+    and wi_hom_pred: "word_pred (word_of_int a) = word_of_int (a - 1)"
+  by (transfer, simp)+
+
+lemmas wi_hom_syms = wi_homs [symmetric]
+
+lemmas word_of_int_homs = wi_homs word_0_wi word_1_wi
+
+lemmas word_of_int_hom_syms = word_of_int_homs [symmetric]
+
+lemma word_of_nat: "of_nat n = word_of_int (int n)"
+  by (induct n) (auto simp add : word_of_int_hom_syms)
+
+lemma word_of_int: "of_int = word_of_int"
+  apply (rule ext)
+  apply (case_tac x rule: int_diff_cases)
+  apply (simp add: word_of_nat wi_hom_sub)
+  done
+
+lemma word_of_int_eq:
+  "word_of_int = of_int"
+  by (rule ext) (transfer, rule)
+
+definition udvd :: "'a::len word \<Rightarrow> 'a::len word \<Rightarrow> bool" (infixl "udvd" 50)
+  where "a udvd b = (\<exists>n\<ge>0. uint b = n * uint a)"
+
+lemma exp_eq_zero_iff:
+  \<open>2 ^ n = (0 :: 'a::len word) \<longleftrightarrow> n \<ge> LENGTH('a)\<close>
+  by transfer simp
+
+lemma double_eq_zero_iff:
+  \<open>2 * a = 0 \<longleftrightarrow> a = 0 \<or> a = 2 ^ (LENGTH('a) - Suc 0)\<close>
+  for a :: \<open>'a::len word\<close>
+proof -
+  define n where \<open>n = LENGTH('a) - Suc 0\<close>
+  then have *: \<open>LENGTH('a) = Suc n\<close>
+    by simp
+  have \<open>a = 0\<close> if \<open>2 * a = 0\<close> and \<open>a \<noteq> 2 ^ (LENGTH('a) - Suc 0)\<close>
+    using that by transfer
+      (auto simp add: take_bit_eq_0_iff take_bit_eq_mod *)
+  moreover have \<open>2 ^ LENGTH('a) = (0 :: 'a word)\<close>
+    by transfer simp
+  then have \<open>2 * 2 ^ (LENGTH('a) - Suc 0) = (0 :: 'a word)\<close>
+    by (simp add: *)
+  ultimately show ?thesis
+    by auto
+qed
+
+
+subsection \<open>Ordering\<close>
+
+lift_definition word_sle :: \<open>'a::len word \<Rightarrow> 'a word \<Rightarrow> bool\<close>  (\<open>(_/ <=s _)\<close> [50, 51] 50)
+  is \<open>\<lambda>k l. signed_take_bit (LENGTH('a) - 1) k \<le> signed_take_bit (LENGTH('a) - 1) l\<close>
+  by (simp flip: signed_take_bit_decr_length_iff)
+
+lemma word_sle_eq [code]:
+  \<open>a <=s b \<longleftrightarrow> sint a \<le> sint b\<close>
+  by transfer simp
+  
+lift_definition word_sless :: \<open>'a::len word \<Rightarrow> 'a word \<Rightarrow> bool\<close>  (\<open>(_/ <s _)\<close> [50, 51] 50)
+  is \<open>\<lambda>k l. signed_take_bit (LENGTH('a) - 1) k < signed_take_bit (LENGTH('a) - 1) l\<close>
+  by (simp flip: signed_take_bit_decr_length_iff)
+
+lemma word_sless_eq:
+  \<open>x <s y \<longleftrightarrow> x <=s y \<and> x \<noteq> y\<close>
+  by transfer (simp add: signed_take_bit_decr_length_iff less_le)
+
+lemma [code]:
+  \<open>a <s b \<longleftrightarrow> sint a < sint b\<close>
+  by transfer simp
+
+lemma word_less_alt: "a < b \<longleftrightarrow> uint a < uint b"
+  by (fact word_less_def)
+
+lemma signed_linorder: "class.linorder word_sle word_sless"
+  by (standard; transfer) (auto simp add: signed_take_bit_decr_length_iff)
+
+interpretation signed: linorder "word_sle" "word_sless"
+  by (rule signed_linorder)
+
+lemma word_zero_le [simp]: "0 \<le> y"
+  for y :: "'a::len word"
+  by transfer simp
+
+lemma word_m1_ge [simp] : "word_pred 0 \<ge> y" (* FIXME: delete *)
+  by transfer (simp add: take_bit_minus_one_eq_mask mask_eq_exp_minus_1 bintr_lt2p)
+
+lemma word_n1_ge [simp]: "y \<le> -1"
+  for y :: "'a::len word"
+  by (fact word_order.extremum)
+
+lemmas word_not_simps [simp] =
+  word_zero_le [THEN leD] word_m1_ge [THEN leD] word_n1_ge [THEN leD]
+
+lemma word_gt_0: "0 < y \<longleftrightarrow> 0 \<noteq> y"
+  for y :: "'a::len word"
+  by (simp add: less_le)
+
+lemmas word_gt_0_no [simp] = word_gt_0 [of "numeral y"] for y
+
+lemma word_sless_alt: "a <s b \<longleftrightarrow> sint a < sint b"
+  by transfer simp
+
+lemma word_le_nat_alt: "a \<le> b \<longleftrightarrow> unat a \<le> unat b"
+  by transfer (simp add: nat_le_eq_zle)
+
+lemma word_less_nat_alt: "a < b \<longleftrightarrow> unat a < unat b"
+  by transfer (auto simp add: less_le [of 0])
+
+lemmas unat_mono = word_less_nat_alt [THEN iffD1]
+
+instance word :: (len) wellorder
+proof
+  fix P :: "'a word \<Rightarrow> bool" and a
+  assume *: "(\<And>b. (\<And>a. a < b \<Longrightarrow> P a) \<Longrightarrow> P b)"
+  have "wf (measure unat)" ..
+  moreover have "{(a, b :: ('a::len) word). a < b} \<subseteq> measure unat"
+    by (auto simp add: word_less_nat_alt)
+  ultimately have "wf {(a, b :: ('a::len) word). a < b}"
+    by (rule wf_subset)
+  then show "P a" using *
+    by induction blast
+qed
+
+lemma wi_less:
+  "(word_of_int n < (word_of_int m :: 'a::len word)) =
+    (n mod 2 ^ LENGTH('a) < m mod 2 ^ LENGTH('a))"
+  by transfer (simp add: take_bit_eq_mod)
+
+lemma wi_le:
+  "(word_of_int n \<le> (word_of_int m :: 'a::len word)) =
+    (n mod 2 ^ LENGTH('a) \<le> m mod 2 ^ LENGTH('a))"
+  by transfer (simp add: take_bit_eq_mod)
+
+
+subsection \<open>Bit-wise operations\<close>
+
+
 lemma uint_take_bit_eq [code]:
   \<open>uint (take_bit n w) = take_bit n (uint w)\<close>
   by transfer (simp add: ac_simps)
@@ -1042,6 +1094,22 @@
   \<open>((=) ===> pcr_word ===> pcr_word) flip_bit flip_bit\<close>
   by (unfold flip_bit_def) transfer_prover
 
+lemma signed_take_bit_word_transfer [transfer_rule]:
+  \<open>((=) ===> pcr_word ===> pcr_word)
+    (\<lambda>n k. signed_take_bit n (take_bit LENGTH('a::len) k))
+    (signed_take_bit :: nat \<Rightarrow> 'a word \<Rightarrow> 'a word)\<close>
+proof -
+  let ?K = \<open>\<lambda>n (k :: int). take_bit (min LENGTH('a) n) k OR of_bool (n < LENGTH('a) \<and> bit k n) * NOT (mask n)\<close>
+  let ?W = \<open>\<lambda>n (w :: 'a word). take_bit n w OR of_bool (bit w n) * NOT (mask n)\<close>
+  have \<open>((=) ===> pcr_word ===> pcr_word) ?K ?W\<close>
+    by transfer_prover
+  also have \<open>?K = (\<lambda>n k. signed_take_bit n (take_bit LENGTH('a::len) k))\<close>
+    by (simp add: fun_eq_iff signed_take_bit_def bit_take_bit_iff ac_simps)
+  also have \<open>?W = signed_take_bit\<close>
+    by (simp add: fun_eq_iff signed_take_bit_def)
+  finally show ?thesis .
+qed
+
 end
 
 instantiation word :: (len) semiring_bit_syntax
@@ -1260,6 +1328,147 @@
 qed
 
 
+subsection \<open>Type-definition locale instantiations\<close>
+
+definition uints :: "nat \<Rightarrow> int set"
+  \<comment> \<open>the sets of integers representing the words\<close>
+  where "uints n = range (take_bit n)"
+
+definition sints :: "nat \<Rightarrow> int set"
+  where "sints n = range (signed_take_bit (n - 1))"
+
+lemma uints_num: "uints n = {i. 0 \<le> i \<and> i < 2 ^ n}"
+  by (simp add: uints_def range_bintrunc)
+
+lemma sints_num: "sints n = {i. - (2 ^ (n - 1)) \<le> i \<and> i < 2 ^ (n - 1)}"
+  by (simp add: sints_def range_sbintrunc)
+
+definition unats :: "nat \<Rightarrow> nat set"
+  where "unats n = {i. i < 2 ^ n}"
+
+\<comment> \<open>naturals\<close>
+lemma uints_unats: "uints n = int ` unats n"
+  apply (unfold unats_def uints_num)
+  apply safe
+    apply (rule_tac image_eqI)
+     apply (erule_tac nat_0_le [symmetric])
+  by auto
+
+lemma unats_uints: "unats n = nat ` uints n"
+  by (auto simp: uints_unats image_iff)
+
+lemma td_ext_uint:
+  "td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (LENGTH('a::len)))
+    (\<lambda>w::int. w mod 2 ^ LENGTH('a))"
+  apply (unfold td_ext_def')
+  apply transfer
+  apply (simp add: uints_num take_bit_eq_mod)
+  done
+
+interpretation word_uint:
+  td_ext
+    "uint::'a::len word \<Rightarrow> int"
+    word_of_int
+    "uints (LENGTH('a::len))"
+    "\<lambda>w. w mod 2 ^ LENGTH('a::len)"
+  by (fact td_ext_uint)
+
+lemmas td_uint = word_uint.td_thm
+lemmas int_word_uint = word_uint.eq_norm
+
+lemma td_ext_ubin:
+  "td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (LENGTH('a::len)))
+    (take_bit (LENGTH('a)))"
+  apply standard
+  apply transfer
+  apply simp
+  done
+
+interpretation word_ubin:
+  td_ext
+    "uint::'a::len word \<Rightarrow> int"
+    word_of_int
+    "uints (LENGTH('a::len))"
+    "take_bit (LENGTH('a::len))"
+  by (fact td_ext_ubin)
+
+lemma td_ext_unat [OF refl]:
+  "n = LENGTH('a::len) \<Longrightarrow>
+    td_ext (unat :: 'a word \<Rightarrow> nat) of_nat (unats n) (\<lambda>i. i mod 2 ^ n)"
+  apply (standard; transfer)
+     apply (simp_all add: unats_def take_bit_int_less_exp take_bit_of_nat take_bit_eq_self)
+  apply (simp add: take_bit_eq_mod)
+  done
+
+lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm]
+
+interpretation word_unat:
+  td_ext
+    "unat::'a::len word \<Rightarrow> nat"
+    of_nat
+    "unats (LENGTH('a::len))"
+    "\<lambda>i. i mod 2 ^ LENGTH('a::len)"
+  by (rule td_ext_unat)
+
+lemmas td_unat = word_unat.td_thm
+
+lemmas unat_lt2p [iff] = word_unat.Rep [unfolded unats_def mem_Collect_eq]
+
+lemma unat_le: "y \<le> unat z \<Longrightarrow> y \<in> unats (LENGTH('a))"
+  for z :: "'a::len word"
+  apply (unfold unats_def)
+  apply clarsimp
+  apply (rule xtrans, rule unat_lt2p, assumption)
+  done
+
+lemma td_ext_sbin:
+  "td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (LENGTH('a::len)))
+    (signed_take_bit (LENGTH('a) - 1))"
+  apply (unfold td_ext_def' sint_uint)
+  apply (simp add : word_ubin.eq_norm)
+  apply (cases "LENGTH('a)")
+   apply (auto simp add : sints_def)
+  apply (rule sym [THEN trans])
+   apply (rule word_ubin.Abs_norm)
+  apply (simp only: bintrunc_sbintrunc)
+  apply (drule sym)
+  apply simp
+  done
+
+lemma td_ext_sint:
+  "td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (LENGTH('a::len)))
+     (\<lambda>w. (w + 2 ^ (LENGTH('a) - 1)) mod 2 ^ LENGTH('a) -
+         2 ^ (LENGTH('a) - 1))"
+  using td_ext_sbin [where ?'a = 'a] by (simp add: no_sbintr_alt2)
+
+text \<open>
+  We do \<open>sint\<close> before \<open>sbin\<close>, before \<open>sint\<close> is the user version
+  and interpretations do not produce thm duplicates. I.e.
+  we get the name \<open>word_sint.Rep_eqD\<close>, but not \<open>word_sbin.Req_eqD\<close>,
+  because the latter is the same thm as the former.
+\<close>
+interpretation word_sint:
+  td_ext
+    "sint ::'a::len word \<Rightarrow> int"
+    word_of_int
+    "sints (LENGTH('a::len))"
+    "\<lambda>w. (w + 2^(LENGTH('a::len) - 1)) mod 2^LENGTH('a::len) -
+      2 ^ (LENGTH('a::len) - 1)"
+  by (rule td_ext_sint)
+
+interpretation word_sbin:
+  td_ext
+    "sint ::'a::len word \<Rightarrow> int"
+    word_of_int
+    "sints (LENGTH('a::len))"
+    "signed_take_bit (LENGTH('a::len) - 1)"
+  by (rule td_ext_sbin)
+
+lemmas int_word_sint = td_ext_sint [THEN td_ext.eq_norm]
+
+lemmas td_sint = word_sint.td
+
+
 subsection \<open>More shift operations\<close>
 
 lift_definition sshiftr1 :: \<open>'a::len word \<Rightarrow> 'a word\<close>
@@ -1281,7 +1490,7 @@
 lemma sshiftr_eq:
   \<open>w >>> n = (sshiftr1 ^^ n) w\<close>
 proof -
-  have *: \<open>(\<lambda>k. take_bit LENGTH('a) (signed_take_bit (LENGTH('a) - Suc 0) k div 2)) ^^ Suc n =
+  have *: \<open>(\<lambda>k::int. take_bit LENGTH('a) (signed_take_bit (LENGTH('a) - Suc 0) k div 2)) ^^ Suc n =
     take_bit LENGTH('a) \<circ> drop_bit (Suc n) \<circ> signed_take_bit (LENGTH('a) - Suc 0)\<close>
     for n
     apply (induction n)
@@ -1521,53 +1730,6 @@
     word_of_int (take_bit n w) = (word_of_int w :: 'a word)"
   by (auto simp: word_ubin.norm_eq_iff [symmetric] min.absorb1)
 
-lemma td_ext_sbin:
-  "td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (LENGTH('a::len)))
-    (signed_take_bit (LENGTH('a) - 1))"
-  apply (unfold td_ext_def' sint_uint)
-  apply (simp add : word_ubin.eq_norm)
-  apply (cases "LENGTH('a)")
-   apply (auto simp add : sints_def)
-  apply (rule sym [THEN trans])
-   apply (rule word_ubin.Abs_norm)
-  apply (simp only: bintrunc_sbintrunc)
-  apply (drule sym)
-  apply simp
-  done
-
-lemma td_ext_sint:
-  "td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (LENGTH('a::len)))
-     (\<lambda>w. (w + 2 ^ (LENGTH('a) - 1)) mod 2 ^ LENGTH('a) -
-         2 ^ (LENGTH('a) - 1))"
-  using td_ext_sbin [where ?'a = 'a] by (simp add: no_sbintr_alt2)
-
-text \<open>
-  We do \<open>sint\<close> before \<open>sbin\<close>, before \<open>sint\<close> is the user version
-  and interpretations do not produce thm duplicates. I.e.
-  we get the name \<open>word_sint.Rep_eqD\<close>, but not \<open>word_sbin.Req_eqD\<close>,
-  because the latter is the same thm as the former.
-\<close>
-interpretation word_sint:
-  td_ext
-    "sint ::'a::len word \<Rightarrow> int"
-    word_of_int
-    "sints (LENGTH('a::len))"
-    "\<lambda>w. (w + 2^(LENGTH('a::len) - 1)) mod 2^LENGTH('a::len) -
-      2 ^ (LENGTH('a::len) - 1)"
-  by (rule td_ext_sint)
-
-interpretation word_sbin:
-  td_ext
-    "sint ::'a::len word \<Rightarrow> int"
-    word_of_int
-    "sints (LENGTH('a::len))"
-    "signed_take_bit (LENGTH('a::len) - 1)"
-  by (rule td_ext_sbin)
-
-lemmas int_word_sint = td_ext_sint [THEN td_ext.eq_norm]
-
-lemmas td_sint = word_sint.td
-
 lemma uints_mod: "uints n = range (\<lambda>w. w mod 2 ^ n)"
   by (fact uints_def [unfolded no_bintr_alt1])
 
@@ -1624,10 +1786,6 @@
   for x :: "'a::len word"
   using word_uint.Rep [of x] by (simp add: uints_num)
 
-lemma word_exp_length_eq_0 [simp]:
-  \<open>(2 :: 'a::len word) ^ LENGTH('a) = 0\<close>
-  by transfer (simp add: take_bit_eq_mod)
-
 lemma sint_ge: "- (2 ^ (LENGTH('a) - 1)) \<le> sint x"
   for x :: "'a::len word"
   using word_sint.Rep [of x] by (simp add: sints_num)
@@ -1804,7 +1962,7 @@
   unfolding bintr_num by (erule subst, simp)
 
 lemma num_of_sbintr':
-  "signed_take_bit (LENGTH('a::len) - 1) (numeral a) = (numeral b) \<Longrightarrow>
+  "signed_take_bit (LENGTH('a::len) - 1) (numeral a :: int) = (numeral b) \<Longrightarrow>
     numeral a = (numeral b :: 'a word)"
   unfolding sbintr_num by (erule subst, simp)
 
@@ -1981,15 +2139,6 @@
 
 subsection \<open>Word Arithmetic\<close>
 
-lemma word_less_alt: "a < b \<longleftrightarrow> uint a < uint b"
-  by (fact word_less_def)
-
-lemma signed_linorder: "class.linorder word_sle word_sless"
-  by (standard; transfer) (auto simp add: signed_take_bit_decr_length_iff)
-
-interpretation signed: linorder "word_sle" "word_sless"
-  by (rule signed_linorder)
-
 lemma udvdI: "0 \<le> n \<Longrightarrow> uint b = n * uint a \<Longrightarrow> a udvd b"
   by (auto simp: udvd_def)
 
@@ -2000,18 +2149,6 @@
 lemmas word_sless_no [simp] = word_sless_eq [of "numeral a" "numeral b"] for a b
 lemmas word_sle_no [simp] = word_sle_eq [of "numeral a" "numeral b"] for a b
 
-lemma word_m1_wi: "- 1 = word_of_int (- 1)"
-  by (simp add: word_neg_numeral_alt [of Num.One])
-
-lemma uint_0_iff: "uint x = 0 \<longleftrightarrow> x = 0"
-  by (simp add: word_uint_eq_iff)
-
-lemma unat_0_iff: "unat x = 0 \<longleftrightarrow> x = 0"
-  by transfer (auto intro: antisym)
-
-lemma unat_0 [simp]: "unat 0 = 0"
-  by transfer simp
-
 lemma size_0_same': "size w = 0 \<Longrightarrow> w = v"
   for v w :: "'a::len word"
   by (unfold word_size) simp
@@ -2021,35 +2158,6 @@
 lemmas unat_eq_0 = unat_0_iff
 lemmas unat_eq_zero = unat_0_iff
 
-lemma unat_gt_0: "0 < unat x \<longleftrightarrow> x \<noteq> 0"
-  by (auto simp: unat_0_iff [symmetric])
-
-lemma ucast_0 [simp]: "ucast 0 = 0"
-  by transfer simp
-
-lemma sint_0 [simp]: "sint 0 = 0"
-  by (simp add: sint_uint)
-
-lemma scast_0 [simp]: "scast 0 = 0"
-  by transfer simp
-
-lemma sint_n1 [simp] : "sint (- 1) = - 1"
-  by transfer simp
-
-lemma scast_n1 [simp]: "scast (- 1) = - 1"
-  by transfer simp
-
-lemma uint_1: "uint (1::'a::len word) = 1"
-  by (fact uint_1_eq)
-
-lemma unat_1 [simp]: "unat (1::'a::len word) = 1"
-  by transfer simp
-
-lemma ucast_1 [simp]: "ucast (1::'a::len word) = 1"
-  by transfer simp
-
-\<comment> \<open>now, to get the weaker results analogous to \<open>word_div\<close>/\<open>mod_def\<close>\<close>
-
 
 subsection \<open>Transferring goals from words to ints\<close>
 
@@ -2130,60 +2238,6 @@
 
 subsection \<open>Order on fixed-length words\<close>
 
-lemma word_zero_le [simp]: "0 \<le> y"
-  for y :: "'a::len word"
-  unfolding word_le_def by auto
-
-lemma word_m1_ge [simp] : "word_pred 0 \<ge> y" (* FIXME: delete *)
-  by transfer (simp add: take_bit_minus_one_eq_mask mask_eq_exp_minus_1 bintr_lt2p)
-
-lemma word_n1_ge [simp]: "y \<le> -1"
-  for y :: "'a::len word"
-  by (fact word_order.extremum)
-
-lemmas word_not_simps [simp] =
-  word_zero_le [THEN leD] word_m1_ge [THEN leD] word_n1_ge [THEN leD]
-
-lemma word_gt_0: "0 < y \<longleftrightarrow> 0 \<noteq> y"
-  for y :: "'a::len word"
-  by (simp add: less_le)
-
-lemmas word_gt_0_no [simp] = word_gt_0 [of "numeral y"] for y
-
-lemma word_sless_alt: "a <s b \<longleftrightarrow> sint a < sint b"
-  by (auto simp add: word_sle_eq word_sless_eq less_le)
-
-lemma word_le_nat_alt: "a \<le> b \<longleftrightarrow> unat a \<le> unat b"
-  by transfer (simp add: nat_le_eq_zle)
-
-lemma word_less_nat_alt: "a < b \<longleftrightarrow> unat a < unat b"
-  by transfer (auto simp add: less_le [of 0])
-
-lemmas unat_mono = word_less_nat_alt [THEN iffD1]
-
-instance word :: (len) wellorder
-proof
-  fix P :: "'a word \<Rightarrow> bool" and a
-  assume *: "(\<And>b. (\<And>a. a < b \<Longrightarrow> P a) \<Longrightarrow> P b)"
-  have "wf (measure unat)" ..
-  moreover have "{(a, b :: ('a::len) word). a < b} \<subseteq> measure unat"
-    by (auto simp add: word_less_nat_alt)
-  ultimately have "wf {(a, b :: ('a::len) word). a < b}"
-    by (rule wf_subset)
-  then show "P a" using *
-    by induction blast
-qed
-
-lemma wi_less:
-  "(word_of_int n < (word_of_int m :: 'a::len word)) =
-    (n mod 2 ^ LENGTH('a) < m mod 2 ^ LENGTH('a))"
-  unfolding word_less_alt by (simp add: word_uint.eq_norm)
-
-lemma wi_le:
-  "(word_of_int n \<le> (word_of_int m :: 'a::len word)) =
-    (n mod 2 ^ LENGTH('a) \<le> m mod 2 ^ LENGTH('a))"
-  unfolding word_le_def by (simp add: word_uint.eq_norm)
-
 lemma udvd_nat_alt: "a udvd b \<longleftrightarrow> (\<exists>n\<ge>0. unat b = n * unat a)"
   supply nat_uint_eq [simp del]
   apply (unfold udvd_def)
@@ -2569,35 +2623,6 @@
 
 subsection \<open>Word and nat\<close>
 
-lemma td_ext_unat [OF refl]:
-  "n = LENGTH('a::len) \<Longrightarrow>
-    td_ext (unat :: 'a word \<Rightarrow> nat) of_nat (unats n) (\<lambda>i. i mod 2 ^ n)"
-  apply (standard; transfer)
-     apply (simp_all add: unats_def take_bit_int_less_exp take_bit_of_nat take_bit_eq_self)
-  apply (simp add: take_bit_eq_mod)
-  done
-
-lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm]
-
-interpretation word_unat:
-  td_ext
-    "unat::'a::len word \<Rightarrow> nat"
-    of_nat
-    "unats (LENGTH('a::len))"
-    "\<lambda>i. i mod 2 ^ LENGTH('a::len)"
-  by (rule td_ext_unat)
-
-lemmas td_unat = word_unat.td_thm
-
-lemmas unat_lt2p [iff] = word_unat.Rep [unfolded unats_def mem_Collect_eq]
-
-lemma unat_le: "y \<le> unat z \<Longrightarrow> y \<in> unats (LENGTH('a))"
-  for z :: "'a::len word"
-  apply (unfold unats_def)
-  apply clarsimp
-  apply (rule xtrans, rule unat_lt2p, assumption)
-  done
-
 lemma word_nchotomy: "\<forall>w :: 'a::len word. \<exists>n. w = of_nat n \<and> n < 2 ^ LENGTH('a)"
   apply (rule allI)
   apply (rule word_unat.Abs_cases)
@@ -3272,8 +3297,6 @@
   \<open>set_bits (\<lambda>_. False) = (0 :: 'a :: len word)\<close>
   by (rule bit_word_eqI) (simp add: bit_set_bits_word_iff)
 
-lemmas of_nth_def = word_set_bits_def (* FIXME duplicate *)
-
 interpretation test_bit:
   td_ext
     "(!!) :: 'a::len word \<Rightarrow> nat \<Rightarrow> bool"
@@ -3404,7 +3427,8 @@
 
 lemma sshiftr_div_2n: "sint (sshiftr w n) = sint w div 2 ^ n"
   apply transfer
-  apply (auto simp add: bit_eq_iff bit_signed_take_bit_iff bit_drop_bit_eq min_def simp flip: drop_bit_eq_div)
+  apply (rule bit_eqI)
+  apply (simp add: bit_signed_take_bit_iff bit_drop_bit_eq min_def flip: drop_bit_eq_div)
   done
 
 lemma bit_bshiftr1_iff:
@@ -4172,7 +4196,7 @@
   apply (simp add: word_rotl_eq_word_rotr word_rotr_word_rotr_eq bit_word_rotr_iff algebra_simps)
   apply (auto dest: bit_imp_le_length)
    apply (metis (no_types, lifting) add.right_neutral add_diff_cancel_right' div_mult_mod_eq mod_add_right_eq mod_add_self2 mod_if mod_mult_self2_is_0)
-  apply (metis (no_types, lifting) add.right_neutral add_diff_cancel_right' bit_imp_le_length div_mult_mod_eq mod_add_right_eq mod_add_self2 mod_less mod_mult_self2_is_0)
+  apply (metis (no_types, lifting) add.right_neutral add_diff_cancel_right' div_mult_mod_eq mod_add_right_eq mod_add_self2 mod_less mod_mult_self2_is_0)
   done
 
 lemma word_rot_lr [simp]:
@@ -4181,7 +4205,7 @@
   apply (simp add: word_rotl_eq_word_rotr word_rotr_word_rotr_eq bit_word_rotr_iff algebra_simps)
   apply (auto dest: bit_imp_le_length)
    apply (metis (no_types, lifting) add.right_neutral add_diff_cancel_right' div_mult_mod_eq mod_add_right_eq mod_add_self2 mod_if mod_mult_self2_is_0)
-  apply (metis (no_types, lifting) add.right_neutral add_diff_cancel_right' bit_imp_le_length div_mult_mod_eq mod_add_right_eq mod_add_self2 mod_less mod_mult_self2_is_0)
+  apply (metis (no_types, lifting) add.right_neutral add_diff_cancel_right' div_mult_mod_eq mod_add_right_eq mod_add_self2 mod_less mod_mult_self2_is_0)
   done
 
 lemma word_rot_gal: