src/HOL/Word/Word.thy

 lemma uint_word_of_int [code]: "uint (word_of_int w \<Colon> 'a\<Colon>len0 word) = w mod 2 ^ len_of TYPE('a)"
   by (auto simp add: word_of_int_def bintrunc_mod2p intro: Abs_word_inverse)
 
 code_datatype word_of_int
 
+subsection {* Random instance *}
+
 notation fcomp (infixl "\<circ>>" 60)
 notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
 instantiation word :: ("{len0, typerep}") random
 begin

 syntax
   of_int :: "int => 'a"
 translations
   "case x of CONST of_int y => b" == "CONST word_int_case (%y. b) x"
 
-
-subsection  "Arithmetic operations"
-
-instantiation word :: (len0) "{number, uminus, minus, plus, one, zero, times, Divides.div, ord}"
-begin
-
-definition
-  word_0_wi: "0 = word_of_int 0"
-
-definition
-  word_1_wi: "1 = word_of_int 1"
-
-definition
-  word_add_def: "a + b = word_of_int (uint a + uint b)"
-
-definition
-  word_sub_wi: "a - b = word_of_int (uint a - uint b)"
-
-definition
-  word_minus_def: "- a = word_of_int (- uint a)"
-
-definition
-  word_mult_def: "a * b = word_of_int (uint a * uint b)"
-
-definition
-  word_div_def: "a div b = word_of_int (uint a div uint b)"
-
-definition
-  word_mod_def: "a mod b = word_of_int (uint a mod uint b)"
-
-definition
-  word_number_of_def: "number_of w = word_of_int w"
-
-definition
-  word_le_def: "a \<le> b \<longleftrightarrow> uint a \<le> uint b"
-
-definition
-  word_less_def: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> (y \<Colon> 'a word)"
-
-instance ..
-
-end
-
-definition
-  word_succ :: "'a :: len0 word => 'a word"
-where
-  "word_succ a = word_of_int (Int.succ (uint a))"
-
-definition
-  word_pred :: "'a :: len0 word => 'a word"
-where
-  "word_pred a = word_of_int (Int.pred (uint a))"
-
-definition udvd :: "'a::len word => 'a::len word => bool" (infixl "udvd" 50) where
-  "a udvd b = (EX n>=0. uint b = n * uint a)"
-
-definition word_sle :: "'a :: len word => 'a word => bool" ("(_/ <=s _)" [50, 51] 50) where
-  "a <=s b = (sint a <= sint b)"
-
-definition word_sless :: "'a :: len word => 'a word => bool" ("(_/ <s _)" [50, 51] 50) where
-  "(x <s y) = (x <=s y & x ~= y)"
-
-
-
-subsection "Bit-wise operations"
-
-instantiation word :: (len0) bits
-begin
-
-definition
-  word_and_def: 
-  "(a::'a word) AND b = word_of_int (uint a AND uint b)"
-
-definition
-  word_or_def:  
-  "(a::'a word) OR b = word_of_int (uint a OR uint b)"
-
-definition
-  word_xor_def: 
-  "(a::'a word) XOR b = word_of_int (uint a XOR uint b)"
-
-definition
-  word_not_def: 
-  "NOT (a::'a word) = word_of_int (NOT (uint a))"
-
-definition
-  word_test_bit_def: "test_bit a = bin_nth (uint a)"
-
-definition
-  word_set_bit_def: "set_bit a n x =
-   word_of_int (bin_sc n (If x 1 0) (uint a))"
-
-definition
-  word_set_bits_def: "(BITS n. f n) = of_bl (bl_of_nth (len_of TYPE ('a)) f)"
-
-definition
-  word_lsb_def: "lsb a \<longleftrightarrow> bin_last (uint a) = 1"
-
-definition shiftl1 :: "'a word \<Rightarrow> 'a word" where
-  "shiftl1 w = word_of_int (uint w BIT 0)"
-
-definition shiftr1 :: "'a word \<Rightarrow> 'a word" where
-  -- "shift right as unsigned or as signed, ie logical or arithmetic"
-  "shiftr1 w = word_of_int (bin_rest (uint w))"
-
-definition
-  shiftl_def: "w << n = (shiftl1 ^^ n) w"
-
-definition
-  shiftr_def: "w >> n = (shiftr1 ^^ n) w"
-
-instance ..
-
-end
-
-instantiation word :: (len) bitss
-begin
-
-definition
-  word_msb_def: 
-  "msb a \<longleftrightarrow> bin_sign (sint a) = Int.Min"
-
-instance ..
-
-end
-
-lemma [code]:
-  "msb a \<longleftrightarrow> bin_sign (sint a) = (- 1 :: int)"
-  by (simp only: word_msb_def Min_def)
-
-definition setBit :: "'a :: len0 word => nat => 'a word" where 
-  "setBit w n = set_bit w n True"
-
-definition clearBit :: "'a :: len0 word => nat => 'a word" where
-  "clearBit w n = set_bit w n False"
-
-
-subsection "Shift operations"
-
-definition sshiftr1 :: "'a :: len word => 'a word" where 
-  "sshiftr1 w = word_of_int (bin_rest (sint w))"
-
-definition bshiftr1 :: "bool => 'a :: len word => 'a word" where
-  "bshiftr1 b w = of_bl (b # butlast (to_bl w))"
-
-definition sshiftr :: "'a :: len word => nat => 'a word" (infixl ">>>" 55) where
-  "w >>> n = (sshiftr1 ^^ n) w"
-
-definition mask :: "nat => 'a::len word" where
-  "mask n = (1 << n) - 1"
-
-definition revcast :: "'a :: len0 word => 'b :: len0 word" where
-  "revcast w =  of_bl (takefill False (len_of TYPE('b)) (to_bl w))"
-
-definition slice1 :: "nat => 'a :: len0 word => 'b :: len0 word" where
-  "slice1 n w = of_bl (takefill False n (to_bl w))"
-
-definition slice :: "nat => 'a :: len0 word => 'b :: len0 word" where
-  "slice n w = slice1 (size w - n) w"
-
-
-subsection "Rotation"
-
-definition rotater1 :: "'a list => 'a list" where
-  "rotater1 ys = 
-    (case ys of [] => [] | x # xs => last ys # butlast ys)"
-
-definition rotater :: "nat => 'a list => 'a list" where
-  "rotater n = rotater1 ^^ n"
-
-definition word_rotr :: "nat => 'a :: len0 word => 'a :: len0 word" where
-  "word_rotr n w = of_bl (rotater n (to_bl w))"
-
-definition word_rotl :: "nat => 'a :: len0 word => 'a :: len0 word" where
-  "word_rotl n w = of_bl (rotate n (to_bl w))"
-
-definition word_roti :: "int => 'a :: len0 word => 'a :: len0 word" where
-  "word_roti i w = (if i >= 0 then word_rotr (nat i) w
-                    else word_rotl (nat (- i)) w)"
-
-
-subsection "Split and cat operations"
-
-definition word_cat :: "'a :: len0 word => 'b :: len0 word => 'c :: len0 word" where
-  "word_cat a b = word_of_int (bin_cat (uint a) (len_of TYPE ('b)) (uint b))"
-
-definition word_split :: "'a :: len0 word => ('b :: len0 word) * ('c :: len0 word)" where
-  "word_split a = 
-   (case bin_split (len_of TYPE ('c)) (uint a) of 
-     (u, v) => (word_of_int u, word_of_int v))"
-
-definition word_rcat :: "'a :: len0 word list => 'b :: len0 word" where
-  "word_rcat ws = 
-  word_of_int (bin_rcat (len_of TYPE ('a)) (map uint ws))"
-
-definition word_rsplit :: "'a :: len0 word => 'b :: len word list" where
-  "word_rsplit w = 
-  map word_of_int (bin_rsplit (len_of TYPE ('b)) (len_of TYPE ('a), uint w))"
-
-definition max_word :: "'a::len word" -- "Largest representable machine integer." where
-  "max_word = word_of_int (2 ^ len_of TYPE('a) - 1)"
-
-primrec of_bool :: "bool \<Rightarrow> 'a::len word" where
-  "of_bool False = 0"
-| "of_bool True = 1"
-
-
-lemmas of_nth_def = word_set_bits_def
+subsection {* Type-definition locale instantiations *}
 
 lemmas word_size_gt_0 [iff] = 
   xtr1 [OF word_size len_gt_0, standard]
 lemmas lens_gt_0 = word_size_gt_0 len_gt_0
 lemmas lens_not_0 [iff] = lens_gt_0 [THEN gr_implies_not0, standard]

   td_ext "uint::'a::len0 word \<Rightarrow> int" 
          word_of_int 
          "uints (len_of TYPE('a::len0))"
          "bintrunc (len_of TYPE('a::len0))"
   by (rule td_ext_ubin)
+
+lemma split_word_all:
+  "(\<And>x::'a::len0 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)"
+  hence "PROP P (word_of_int (uint x))" .
+  thus "PROP P x" by simp
+qed
+
+subsection  "Arithmetic operations"
+
+definition
+  word_succ :: "'a :: len0 word => 'a word"
+where
+  "word_succ a = word_of_int (Int.succ (uint a))"
+
+definition
+  word_pred :: "'a :: len0 word => 'a word"
+where
+  "word_pred a = word_of_int (Int.pred (uint a))"
+
+instantiation word :: (len0) "{number, Divides.div, ord, comm_monoid_mult, comm_ring}"
+begin
+
+definition
+  word_0_wi: "0 = word_of_int 0"
+
+definition
+  word_1_wi: "1 = word_of_int 1"
+
+definition
+  word_add_def: "a + b = word_of_int (uint a + uint b)"
+
+definition
+  word_sub_wi: "a - b = word_of_int (uint a - uint b)"
+
+definition
+  word_minus_def: "- a = word_of_int (- uint a)"
+
+definition
+  word_mult_def: "a * b = word_of_int (uint a * uint b)"
+
+definition
+  word_div_def: "a div b = word_of_int (uint a div uint b)"
+
+definition
+  word_mod_def: "a mod b = word_of_int (uint a mod uint b)"
+
+definition
+  word_number_of_def: "number_of w = word_of_int w"
+
+definition
+  word_le_def: "a \<le> b \<longleftrightarrow> uint a \<le> uint b"
+
+definition
+  word_less_def: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> (y \<Colon> 'a word)"
+
+lemmas word_arith_wis = 
+  word_add_def word_mult_def word_minus_def 
+  word_succ_def word_pred_def word_0_wi word_1_wi
+
+lemmas arths = 
+  bintr_ariths [THEN word_ubin.norm_eq_iff [THEN iffD1],
+                folded word_ubin.eq_norm, standard]
+
+lemma wi_homs: 
+  shows
+  wi_hom_add: "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 (Int.succ a)" and
+  wi_hom_pred: "word_pred (word_of_int a) = word_of_int (Int.pred a)"
+  by (auto simp: word_arith_wis arths)
+
+lemmas wi_hom_syms = wi_homs [symmetric]
+
+lemma word_sub_def: "a - b = a + - (b :: 'a :: len0 word)"
+  unfolding word_sub_wi diff_minus
+  by (simp only : word_uint.Rep_inverse wi_hom_syms)
+    
+lemmas word_diff_minus = word_sub_def [standard]
+
+lemma word_of_int_sub_hom:
+  "(word_of_int a) - word_of_int b = word_of_int (a - b)"
+  unfolding word_sub_def diff_minus by (simp only : wi_homs)
+
+lemmas new_word_of_int_homs = 
+  word_of_int_sub_hom wi_homs word_0_wi word_1_wi 
+
+lemmas new_word_of_int_hom_syms = new_word_of_int_homs [symmetric, standard]
+
+lemmas word_of_int_hom_syms =
+  new_word_of_int_hom_syms [unfolded succ_def pred_def]
+
+lemmas word_of_int_homs =
+  new_word_of_int_homs [unfolded succ_def pred_def]
+
+lemmas word_of_int_add_hom = word_of_int_homs (2)
+lemmas word_of_int_mult_hom = word_of_int_homs (3)
+lemmas word_of_int_minus_hom = word_of_int_homs (4)
+lemmas word_of_int_succ_hom = word_of_int_homs (5)
+lemmas word_of_int_pred_hom = word_of_int_homs (6)
+lemmas word_of_int_0_hom = word_of_int_homs (7)
+lemmas word_of_int_1_hom = word_of_int_homs (8)
+
+instance
+  by default (auto simp: split_word_all word_of_int_homs algebra_simps)
+
+end
+
+lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) \<Longrightarrow> (0 :: 'a word) ~= 1"
+  unfolding word_arith_wis
+  by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc)
+
+lemmas lenw1_zero_neq_one = len_gt_0 [THEN word_zero_neq_one]
+
+instance word :: (len) comm_ring_1
+  by (intro_classes) (simp add: lenw1_zero_neq_one)
+
+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 word_of_int_sub_hom)
+  done
+
+lemma word_number_of_eq: 
+  "number_of w = (of_int w :: 'a :: len word)"
+  unfolding word_number_of_def word_of_int by auto
+
+instance word :: (len) number_ring
+  by (intro_classes) (simp add : word_number_of_eq)
+
+definition udvd :: "'a::len word => 'a::len word => bool" (infixl "udvd" 50) where
+  "a udvd b = (EX n>=0. uint b = n * uint a)"
+
+definition word_sle :: "'a :: len word => 'a word => bool" ("(_/ <=s _)" [50, 51] 50) where
+  "a <=s b = (sint a <= sint b)"
+
+definition word_sless :: "'a :: len word => 'a word => bool" ("(_/ <s _)" [50, 51] 50) where
+  "(x <s y) = (x <=s y & x ~= y)"
+
+
+subsection "Bit-wise operations"
+
+instantiation word :: (len0) bits
+begin
+
+definition
+  word_and_def: 
+  "(a::'a word) AND b = word_of_int (uint a AND uint b)"
+
+definition
+  word_or_def:  
+  "(a::'a word) OR b = word_of_int (uint a OR uint b)"
+
+definition
+  word_xor_def: 
+  "(a::'a word) XOR b = word_of_int (uint a XOR uint b)"
+
+definition
+  word_not_def: 
+  "NOT (a::'a word) = word_of_int (NOT (uint a))"
+
+definition
+  word_test_bit_def: "test_bit a = bin_nth (uint a)"
+
+definition
+  word_set_bit_def: "set_bit a n x =
+   word_of_int (bin_sc n (If x 1 0) (uint a))"
+
+definition
+  word_set_bits_def: "(BITS n. f n) = of_bl (bl_of_nth (len_of TYPE ('a)) f)"
+
+definition
+  word_lsb_def: "lsb a \<longleftrightarrow> bin_last (uint a) = 1"
+
+definition shiftl1 :: "'a word \<Rightarrow> 'a word" where
+  "shiftl1 w = word_of_int (uint w BIT 0)"
+
+definition shiftr1 :: "'a word \<Rightarrow> 'a word" where
+  -- "shift right as unsigned or as signed, ie logical or arithmetic"
+  "shiftr1 w = word_of_int (bin_rest (uint w))"
+
+definition
+  shiftl_def: "w << n = (shiftl1 ^^ n) w"
+
+definition
+  shiftr_def: "w >> n = (shiftr1 ^^ n) w"
+
+instance ..
+
+end
+
+instantiation word :: (len) bitss
+begin
+
+definition
+  word_msb_def: 
+  "msb a \<longleftrightarrow> bin_sign (sint a) = Int.Min"
+
+instance ..
+
+end
+
+lemma [code]:
+  "msb a \<longleftrightarrow> bin_sign (sint a) = (- 1 :: int)"
+  by (simp only: word_msb_def Min_def)
+
+definition setBit :: "'a :: len0 word => nat => 'a word" where 
+  "setBit w n = set_bit w n True"
+
+definition clearBit :: "'a :: len0 word => nat => 'a word" where
+  "clearBit w n = set_bit w n False"
+
+
+subsection "Shift operations"
+
+definition sshiftr1 :: "'a :: len word => 'a word" where 
+  "sshiftr1 w = word_of_int (bin_rest (sint w))"
+
+definition bshiftr1 :: "bool => 'a :: len word => 'a word" where
+  "bshiftr1 b w = of_bl (b # butlast (to_bl w))"
+
+definition sshiftr :: "'a :: len word => nat => 'a word" (infixl ">>>" 55) where
+  "w >>> n = (sshiftr1 ^^ n) w"
+
+definition mask :: "nat => 'a::len word" where
+  "mask n = (1 << n) - 1"
+
+definition revcast :: "'a :: len0 word => 'b :: len0 word" where
+  "revcast w =  of_bl (takefill False (len_of TYPE('b)) (to_bl w))"
+
+definition slice1 :: "nat => 'a :: len0 word => 'b :: len0 word" where
+  "slice1 n w = of_bl (takefill False n (to_bl w))"
+
+definition slice :: "nat => 'a :: len0 word => 'b :: len0 word" where
+  "slice n w = slice1 (size w - n) w"
+
+
+subsection "Rotation"
+
+definition rotater1 :: "'a list => 'a list" where
+  "rotater1 ys = 
+    (case ys of [] => [] | x # xs => last ys # butlast ys)"
+
+definition rotater :: "nat => 'a list => 'a list" where
+  "rotater n = rotater1 ^^ n"
+
+definition word_rotr :: "nat => 'a :: len0 word => 'a :: len0 word" where
+  "word_rotr n w = of_bl (rotater n (to_bl w))"
+
+definition word_rotl :: "nat => 'a :: len0 word => 'a :: len0 word" where
+  "word_rotl n w = of_bl (rotate n (to_bl w))"
+
+definition word_roti :: "int => 'a :: len0 word => 'a :: len0 word" where
+  "word_roti i w = (if i >= 0 then word_rotr (nat i) w
+                    else word_rotl (nat (- i)) w)"
+
+
+subsection "Split and cat operations"
+
+definition word_cat :: "'a :: len0 word => 'b :: len0 word => 'c :: len0 word" where
+  "word_cat a b = word_of_int (bin_cat (uint a) (len_of TYPE ('b)) (uint b))"
+
+definition word_split :: "'a :: len0 word => ('b :: len0 word) * ('c :: len0 word)" where
+  "word_split a = 
+   (case bin_split (len_of TYPE ('c)) (uint a) of 
+     (u, v) => (word_of_int u, word_of_int v))"
+
+definition word_rcat :: "'a :: len0 word list => 'b :: len0 word" where
+  "word_rcat ws = 
+  word_of_int (bin_rcat (len_of TYPE ('a)) (map uint ws))"
+
+definition word_rsplit :: "'a :: len0 word => 'b :: len word list" where
+  "word_rsplit w = 
+  map word_of_int (bin_rsplit (len_of TYPE ('b)) (len_of TYPE ('a), uint w))"
+
+definition max_word :: "'a::len word" -- "Largest representable machine integer." where
+  "max_word = word_of_int (2 ^ len_of TYPE('a) - 1)"
+
+primrec of_bool :: "bool \<Rightarrow> 'a::len word" where
+  "of_bool False = 0"
+| "of_bool True = 1"
+
+
+lemmas of_nth_def = word_set_bits_def
 
 lemma sint_sbintrunc': 
   "sint (word_of_int bin :: 'a word) = 
     (sbintrunc (len_of TYPE ('a :: len) - 1) bin)"
   unfolding sint_uint 

 qed (unfold word_sle_def word_sless_def, auto)
 
 interpretation signed: linorder "word_sle" "word_sless"
   by (rule signed_linorder)
 
-lemmas word_arith_wis = 
-  word_add_def word_mult_def word_minus_def 
-  word_succ_def word_pred_def word_0_wi word_1_wi
-
 lemma udvdI: 
   "0 \<le> n \<Longrightarrow> uint b = n * uint a \<Longrightarrow> a udvd b"
   by (auto simp: udvd_def)
 
 lemmas word_div_no [simp] = 

 
 lemma ucast_1 [simp] : "ucast (1 :: 'a :: len word) = 1"
   unfolding ucast_def word_1_wi
   by (simp add: word_ubin.eq_norm int_one_bin bintrunc_minus_simps)
 
-(* abstraction preserves the operations
-  (the definitions tell this for bins in range uint) *)
-
-lemmas arths = 
-  bintr_ariths [THEN word_ubin.norm_eq_iff [THEN iffD1],
-                folded word_ubin.eq_norm, standard]
-
-lemma wi_homs: 
-  shows
-  wi_hom_add: "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 (Int.succ a)" and
-  wi_hom_pred: "word_pred (word_of_int a) = word_of_int (Int.pred a)"
-  by (auto simp: word_arith_wis arths)
-
-lemmas wi_hom_syms = wi_homs [symmetric]
-
-lemma word_sub_def: "a - b = a + - (b :: 'a :: len0 word)"
-  unfolding word_sub_wi diff_minus
-  by (simp only : word_uint.Rep_inverse wi_hom_syms)
-    
-lemmas word_diff_minus = word_sub_def [standard]
-
-lemma word_of_int_sub_hom:
-  "(word_of_int a) - word_of_int b = word_of_int (a - b)"
-  unfolding word_sub_def diff_minus by (simp only : wi_homs)
-
-lemmas new_word_of_int_homs = 
-  word_of_int_sub_hom wi_homs word_0_wi word_1_wi 
-
-lemmas new_word_of_int_hom_syms = new_word_of_int_homs [symmetric, standard]
-
-lemmas word_of_int_hom_syms =
-  new_word_of_int_hom_syms [unfolded succ_def pred_def]
-
-lemmas word_of_int_homs =
-  new_word_of_int_homs [unfolded succ_def pred_def]
-
-lemmas word_of_int_add_hom = word_of_int_homs (2)
-lemmas word_of_int_mult_hom = word_of_int_homs (3)
-lemmas word_of_int_minus_hom = word_of_int_homs (4)
-lemmas word_of_int_succ_hom = word_of_int_homs (5)
-lemmas word_of_int_pred_hom = word_of_int_homs (6)
-lemmas word_of_int_0_hom = word_of_int_homs (7)
-lemmas word_of_int_1_hom = word_of_int_homs (8)
-
 (* now, to get the weaker results analogous to word_div/mod_def *)
 
 lemmas word_arith_alts = 
   word_sub_wi [unfolded succ_def pred_def, standard]
   word_arith_wis [unfolded succ_def pred_def, standard]
 
+(* FIXME: Lots of duplicate lemmas *)
 lemmas word_sub_alt = word_arith_alts (1)
 lemmas word_add_alt = word_arith_alts (2)
 lemmas word_mult_alt = word_arith_alts (3)
 lemmas word_minus_alt = word_arith_alts (4)
 lemmas word_succ_alt = word_arith_alts (5)

 (* alternative approach to lifting arithmetic equalities *)
 lemma word_of_int_Ex:
   "\<exists>y. x = word_of_int y"
   by (rule_tac x="uint x" in exI) simp
 
+(* FIXME: redundant theorems *)
 lemma word_arith_eqs:
   fixes a :: "'a::len0 word"
   fixes b :: "'a::len0 word"
   shows
   word_add_0: "0 + a = a" and

 
 lemma word_zero_le [simp] :
   "0 <= (y :: 'a :: len0 word)"
   unfolding word_le_def by auto
   
-instance word :: (len0) semigroup_add
-  by intro_classes (simp add: word_add_assoc)
-
 instance word :: (len0) linorder
   by intro_classes (auto simp: word_less_def word_le_def)
-
-instance word :: (len0) ring
-  by intro_classes
-     (auto simp: word_arith_eqs word_diff_minus 
-                 word_diff_self [unfolded word_diff_minus])
 
 lemma word_m1_ge [simp] : "word_pred 0 >= y"
   unfolding word_le_def
   by (simp only : word_pred_0_n1 word_uint.eq_norm m1mod2k) auto
 

 
 lemma udvd_iff_dvd: "x udvd y <-> unat x dvd unat y"
   unfolding dvd_def udvd_nat_alt by force
 
 lemmas unat_mono = word_less_nat_alt [THEN iffD1, standard]
-
-lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) \<Longrightarrow> (0 :: 'a word) ~= 1"
-  unfolding word_arith_wis
-  by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc)
-
-lemmas lenw1_zero_neq_one = len_gt_0 [THEN word_zero_neq_one]
 
 lemma no_no [simp] : "number_of (number_of b) = number_of b"
   by (simp add: number_of_eq)
 
 lemma unat_minus_one: "x ~= 0 \<Longrightarrow> unat (x - 1) = unat x - 1"

                  word_pred_rbl word_mult_rbl word_add_rbl)
 
 
 subsection "Arithmetic type class instantiations"
 
-instance word :: (len0) comm_monoid_add ..
-
-instance word :: (len0) comm_monoid_mult
-  apply (intro_classes)
-   apply (simp add: word_mult_commute)
-  apply (simp add: word_mult_1)
-  done
-
-instance word :: (len0) comm_semiring 
-  by (intro_classes) (simp add : word_left_distrib)
-
-instance word :: (len0) ab_group_add ..
-
-instance word :: (len0) comm_ring ..
-
-instance word :: (len) comm_semiring_1 
-  by (intro_classes) (simp add: lenw1_zero_neq_one)
-
-instance word :: (len) comm_ring_1 ..
-
-instance word :: (len0) comm_semiring_0 ..
-
-instance word :: (len0) order ..
-
 (* note that iszero_def is only for class comm_semiring_1_cancel,
    which requires word length >= 1, ie 'a :: len word *) 
 lemma zero_bintrunc:
   "iszero (number_of x :: 'a :: len word) = 
     (bintrunc (len_of TYPE('a)) x = Int.Pls)"

   done
 
 lemmas word_le_0_iff [simp] =
   word_zero_le [THEN leD, THEN linorder_antisym_conv1]
 
-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 word_of_int_sub_hom)
-  done
-
 lemma word_of_int_nat: 
   "0 <= x \<Longrightarrow> word_of_int x = of_nat (nat x)"
   by (simp add: of_nat_nat word_of_int)
-
-lemma word_number_of_eq: 
-  "number_of w = (of_int w :: 'a :: len word)"
-  unfolding word_number_of_def word_of_int by auto
-
-instance word :: (len) number_ring
-  by (intro_classes) (simp add : word_number_of_eq)
 
 lemma iszero_word_no [simp] : 
   "iszero (number_of bin :: 'a :: len word) = 
     iszero (number_of (bintrunc (len_of TYPE('a)) bin) :: int)"
   apply (simp add: zero_bintrunc number_of_is_id)