diff -r eaac77208cf9 -r 4b011fa5e83b src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Mon Sep 07 16:14:32 2020 +0000
+++ b/src/HOL/Word/Word.thy	Tue Sep 08 11:39:16 2020 +0000
@@ -24,7 +24,9 @@
     (simp_all add: signed_take_bit_eq_iff_take_bit_eq)
 
 
-subsection \<open>Type definition and fundamental arithmetic\<close>
+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)
@@ -32,6 +34,9 @@
 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
 
@@ -64,17 +69,68 @@
 
 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
 
+lemma [transfer_rule]:
+  \<open>((=) ===> pcr_word) of_bool of_bool\<close>
+  by transfer_prover
+
+lemma [transfer_rule]:
+  \<open>((=) ===> pcr_word) numeral numeral\<close>
+  by transfer_prover
+
+lemma [transfer_rule]:
+  \<open>((=) ===> pcr_word) int of_nat\<close>
+  by transfer_prover
+
+lemma [transfer_rule]:
+  \<open>((=) ===> pcr_word) (\<lambda>k. k) of_int\<close>
+proof -
+  have \<open>((=) ===> pcr_word) of_int of_int\<close>
+    by transfer_prover
+  then show ?thesis by (simp add: id_def)
+qed
+
+lemma [transfer_rule]:
+  \<open>(pcr_word ===> (\<longleftrightarrow>)) even ((dvd) 2 :: 'a::len word \<Rightarrow> bool)\<close>
+proof -
+  have even_word_unfold: "even k \<longleftrightarrow> (\<exists>l. take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l))" (is "?P \<longleftrightarrow> ?Q")
+    for k :: int
+  proof
+    assume ?P
+    then show ?Q
+      by auto
+  next
+    assume ?Q
+    then obtain l where "take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l)" ..
+    then have "even (take_bit LENGTH('a) k)"
+      by simp
+    then show ?P
+      by simp
+  qed
+  show ?thesis by (simp only: even_word_unfold [abs_def] dvd_def [where ?'a = "'a word", abs_def])
+    transfer_prover
+qed
+
 end
 
-
-subsection \<open>Basic code generation setup\<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> .
@@ -133,566 +189,42 @@
   by transfer (simp add: take_bit_mult)
 
 
-subsection \<open>Conversions including casts\<close>
-
-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]:
-  \<open>((=) ===> pcr_word) numeral numeral\<close>
-  by transfer_prover
-
-lemma [transfer_rule]:
-  \<open>((=) ===> pcr_word) int of_nat\<close>
-  by transfer_prover
-
-lemma [transfer_rule]:
-  \<open>((=) ===> pcr_word) (\<lambda>k. k) of_int\<close>
-proof -
-  have \<open>((=) ===> pcr_word) of_int of_int\<close>
-    by transfer_prover
-  then show ?thesis by (simp add: id_def)
-qed
-
-end
-
-lemma word_exp_length_eq_0 [simp]:
-  \<open>(2 :: 'a::len word) ^ LENGTH('a) = 0\<close>
-  by transfer simp
-
-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
+subsubsection \<open>Basic conversions\<close>
 
 lift_definition word_of_int :: \<open>int \<Rightarrow> 'a::len word\<close>
   is \<open>\<lambda>k. k\<close> .
 
-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 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
+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 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
-
-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)"
+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 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>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>Arithmetic operations\<close>
-
-instantiation word :: (len) "{neg_numeral, modulo, comm_monoid_mult, comm_ring}"
-begin
-
-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 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
-
-
-
-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]
-
-instance word :: (len) comm_monoid_add ..
-
-instance word :: (len) semiring_numeral ..
-
-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)"
-
-context
-  includes lifting_syntax
-begin
-
-lemma [transfer_rule]:
-  \<open>(pcr_word ===> (\<longleftrightarrow>)) even ((dvd) 2 :: 'a::len word \<Rightarrow> bool)\<close>
-proof -
-  have even_word_unfold: "even k \<longleftrightarrow> (\<exists>l. take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l))" (is "?P \<longleftrightarrow> ?Q")
-    for k :: int
-  proof
-    assume ?P
-    then show ?Q
-      by auto
-  next
-    assume ?Q
-    then obtain l where "take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l)" ..
-    then have "even (take_bit LENGTH('a) k)"
-      by simp
-    then show ?P
-      by simp
-  qed
-  show ?thesis by (simp only: even_word_unfold [abs_def] dvd_def [where ?'a = "'a word", abs_def])
-    transfer_prover
-qed
-
-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>
-  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 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
@@ -728,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)
@@ -740,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
@@ -756,96 +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
-
-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 (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)
-
 
 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>
@@ -1126,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)
@@ -1475,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>