# HG changeset patch
# User haftmann
# Date 1599495272 0
# Node ID eaac77208cf942fd0c518d253fdf7cab0a00c7b0
# Parent  bb002df3e82e3944021024f0c8578d1d1c3649a5
tuned theory structure

diff -r bb002df3e82e -r eaac77208cf9 src/HOL/Word/More_Word.thy
--- a/src/HOL/Word/More_Word.thy	Mon Sep 07 08:47:28 2020 +0000
+++ b/src/HOL/Word/More_Word.thy	Mon Sep 07 16:14:32 2020 +0000
@@ -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 bb002df3e82e -r eaac77208cf9 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Mon Sep 07 08:47:28 2020 +0000
+++ b/src/HOL/Word/Word.thy	Mon Sep 07 16:14:32 2020 +0000
@@ -15,19 +15,161 @@
   Misc_Typedef
 begin
 
-subsection \<open>Type definition\<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
+    \<longleftrightarrow> take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close>
+  by (cases \<open>LENGTH('a)\<close>)
+    (simp_all add: signed_take_bit_eq_iff_take_bit_eq)
+
+
+subsection \<open>Type definition and fundamental arithmetic\<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)
-
+  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>
 
-lift_definition word_of_int :: \<open>int \<Rightarrow> 'a::len word\<close>
-  is \<open>\<lambda>k. k\<close> .
+instantiation word :: (len) comm_ring_1
+begin
+
+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) (simp_all add: algebra_simps)
+
+end
+
+context
+  includes lifting_syntax
+  notes power_transfer [transfer_rule]
+begin
+
+lemma power_transfer_word [transfer_rule]:
+  \<open>(pcr_word ===> (=) ===> pcr_word) (^) (^)\<close>
+  by transfer_prover
+
+end
+
+
+subsection \<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 [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)
+
+
+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
 
@@ -45,8 +187,19 @@
 lemma word_uint_eq_iff: "a = b \<longleftrightarrow> uint a = uint b"
   using word_uint_eqI by auto
 
+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 transfer (simp add: take_bit_eq_mod)
+  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
@@ -59,15 +212,6 @@
   then show "PROP P x" by (simp add: word_of_int_uint)
 qed
 
-
-subsection \<open>Type conversions and casting\<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
-    \<longleftrightarrow> take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close>
-  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>  
@@ -106,6 +250,53 @@
   \<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
 
@@ -164,61 +355,8 @@
   "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
-
-instance
-  by (standard; transfer) rule
-
-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)"
@@ -281,34 +419,88 @@
     "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>
 
-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
@@ -322,20 +514,6 @@
 
 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
@@ -344,16 +522,6 @@
   "a mod b = word_of_int (uint a mod uint b)"
   by transfer rule
 
-context
-  includes lifting_syntax
-  notes power_transfer [transfer_rule]
-begin
-
-lemma power_transfer_word [transfer_rule]:
-  \<open>(pcr_word ===> (=) ===> pcr_word) (^) (^)\<close>
-  by transfer_prover
-
-end
 
 
 text \<open>Legacy theorems:\<close>
@@ -374,6 +542,20 @@
   "- 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)
@@ -382,14 +564,6 @@
   "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
@@ -414,13 +588,6 @@
 
 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)
 
@@ -430,37 +597,6 @@
   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]:
-  "((=) ===> pcr_word) of_bool of_bool"
-  by transfer_prover
-
-lemma [transfer_rule]:
-  "((=) ===> pcr_word) numeral numeral"
-  by transfer_prover
-
-lemma [transfer_rule]:
-  "((=) ===> pcr_word) int of_nat"
-  by transfer_prover
-
-lemma [transfer_rule]:
-  "((=) ===> pcr_word) (\<lambda>k. k) of_int"
-proof -
-  have "((=) ===> pcr_word) of_int of_int"
-    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)
@@ -644,6 +780,69 @@
   \<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>
 
@@ -1537,53 +1736,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])
 
@@ -1640,10 +1792,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)
@@ -1997,15 +2145,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)
 
@@ -2016,18 +2155,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
@@ -2037,35 +2164,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>
 
@@ -2146,60 +2244,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)
@@ -2585,35 +2629,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)
@@ -3288,8 +3303,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"