src/HOL/Word/Word.thy

 
 text \<open>See \<^file>\<open>Word_Examples.thy\<close> for examples.\<close>
 
 subsection \<open>Type definition\<close>
 
-typedef (overloaded) 'a word = "{(0::int) ..< 2 ^ len_of TYPE('a::len0)}"
+typedef (overloaded) 'a word = "{(0::int) ..< 2 ^ LENGTH('a::len0)}"
   morphisms uint Abs_word by auto
 
 lemma uint_nonnegative: "0 \<le> uint w"
   using word.uint [of w] by simp
 
-lemma uint_bounded: "uint w < 2 ^ len_of TYPE('a)"
+lemma uint_bounded: "uint w < 2 ^ LENGTH('a)"
   for w :: "'a::len0 word"
   using word.uint [of w] by simp
 
-lemma uint_idem: "uint w mod 2 ^ len_of TYPE('a) = uint w"
+lemma uint_idem: "uint w mod 2 ^ LENGTH('a) = uint w"
   for w :: "'a::len0 word"
   using uint_nonnegative uint_bounded by (rule mod_pos_pos_trivial)
 
 lemma word_uint_eq_iff: "a = b \<longleftrightarrow> uint a = uint b"
   by (simp add: uint_inject)

   by (simp add: word_uint_eq_iff)
 
 definition word_of_int :: "int \<Rightarrow> 'a::len0 word"
   \<comment> \<open>representation of words using unsigned or signed bins,
     only difference in these is the type class\<close>
-  where "word_of_int k = Abs_word (k mod 2 ^ len_of TYPE('a))"
-
-lemma uint_word_of_int: "uint (word_of_int k :: 'a::len0 word) = k mod 2 ^ len_of TYPE('a)"
+  where "word_of_int k = Abs_word (k mod 2 ^ LENGTH('a))"
+
+lemma uint_word_of_int: "uint (word_of_int k :: 'a::len0 word) = k mod 2 ^ LENGTH('a)"
   by (auto simp add: word_of_int_def intro: Abs_word_inverse)
 
 lemma word_of_int_uint: "word_of_int (uint w) = w"
   by (simp add: word_of_int_def uint_idem uint_inverse)
 

 lemmas lens_gt_0 = word_size_gt_0 len_gt_0
 
 lemma lens_not_0 [iff]:
   fixes w :: "'a::len word"
   shows "size w \<noteq> 0"
-  and "len_of TYPE('a) \<noteq> 0"
+  and "LENGTH('a) \<noteq> 0"
   by auto
 
 definition source_size :: "('a::len0 word \<Rightarrow> 'b) \<Rightarrow> nat"
   \<comment> \<open>whether a cast (or other) function is to a longer or shorter length\<close>
   where [code del]: "source_size c = (let arb = undefined; x = c arb in size arb)"

 
 definition of_bl :: "bool list \<Rightarrow> 'a::len0 word"
   where "of_bl bl = word_of_int (bl_to_bin bl)"
 
 definition to_bl :: "'a::len0 word \<Rightarrow> bool list"
-  where "to_bl w = bin_to_bl (len_of TYPE('a)) (uint w)"
+  where "to_bl w = bin_to_bl (LENGTH('a)) (uint w)"
 
 definition word_reverse :: "'a::len0 word \<Rightarrow> 'a word"
   where "word_reverse w = of_bl (rev (to_bl w))"
 
 definition word_int_case :: "(int \<Rightarrow> 'b) \<Rightarrow> 'a::len0 word \<Rightarrow> 'b"

 
 definition cr_word :: "int \<Rightarrow> 'a::len0 word \<Rightarrow> bool"
   where "cr_word = (\<lambda>x y. word_of_int x = y)"
 
 lemma Quotient_word:
-  "Quotient (\<lambda>x y. bintrunc (len_of TYPE('a)) x = bintrunc (len_of TYPE('a)) y)
+  "Quotient (\<lambda>x y. bintrunc (LENGTH('a)) x = bintrunc (LENGTH('a)) y)
     word_of_int uint (cr_word :: _ \<Rightarrow> 'a::len0 word \<Rightarrow> bool)"
   unfolding Quotient_alt_def cr_word_def
   by (simp add: no_bintr_alt1 word_of_int_uint) (simp add: word_of_int_def Abs_word_inject)
 
 lemma reflp_word:
-  "reflp (\<lambda>x y. bintrunc (len_of TYPE('a::len0)) x = bintrunc (len_of TYPE('a)) y)"
+  "reflp (\<lambda>x y. bintrunc (LENGTH('a::len0)) x = bintrunc (LENGTH('a)) y)"
   by (simp add: reflp_def)
 
 setup_lifting Quotient_word reflp_word
 
 text \<open>TODO: The next lemma could be generated automatically.\<close>
 
 lemma uint_transfer [transfer_rule]:
-  "(rel_fun pcr_word (=)) (bintrunc (len_of TYPE('a))) (uint :: 'a::len0 word \<Rightarrow> int)"
+  "(rel_fun pcr_word (=)) (bintrunc (LENGTH('a))) (uint :: 'a::len0 word \<Rightarrow> int)"
   unfolding rel_fun_def word.pcr_cr_eq cr_word_def
   by (simp add: no_bintr_alt1 uint_word_of_int)
 
 
 subsection \<open>Basic code generation setup\<close>

 lemmas uint_0 = uint_nonnegative (* FIXME duplicate *)
 lemmas uint_lt = uint_bounded (* FIXME duplicate *)
 lemmas uint_mod_same = uint_idem (* FIXME duplicate *)
 
 lemma td_ext_uint:
-  "td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (len_of TYPE('a::len0)))
-    (\<lambda>w::int. w mod 2 ^ len_of TYPE('a))"
+  "td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (LENGTH('a::len0)))
+    (\<lambda>w::int. w mod 2 ^ LENGTH('a))"
   apply (unfold td_ext_def')
   apply (simp add: uints_num word_of_int_def bintrunc_mod2p)
   apply (simp add: uint_mod_same uint_0 uint_lt
                    word.uint_inverse word.Abs_word_inverse int_mod_lem)
   done
 
 interpretation word_uint:
   td_ext
     "uint::'a::len0 word \<Rightarrow> int"
     word_of_int
-    "uints (len_of TYPE('a::len0))"
-    "\<lambda>w. w mod 2 ^ len_of TYPE('a::len0)"
+    "uints (LENGTH('a::len0))"
+    "\<lambda>w. w mod 2 ^ LENGTH('a::len0)"
   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 (len_of TYPE('a::len0)))
-    (bintrunc (len_of TYPE('a)))"
+  "td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (LENGTH('a::len0)))
+    (bintrunc (LENGTH('a)))"
   by (unfold no_bintr_alt1) (fact td_ext_uint)
 
 interpretation word_ubin:
   td_ext
     "uint::'a::len0 word \<Rightarrow> int"
     word_of_int
-    "uints (len_of TYPE('a::len0))"
-    "bintrunc (len_of TYPE('a::len0))"
+    "uints (LENGTH('a::len0))"
+    "bintrunc (LENGTH('a::len0))"
   by (fact td_ext_ubin)
 
 
 subsection \<open>Arithmetic operations\<close>
 

 
 lemmas word_of_int_hom_syms = word_of_int_homs [symmetric]
 
 instance word :: (len) comm_ring_1
 proof
-  have *: "0 < len_of TYPE('a)" by (rule len_gt_0)
+  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)"

 
 definition mask :: "nat \<Rightarrow> 'a::len word"
   where "mask n = (1 << n) - 1"
 
 definition revcast :: "'a::len0 word \<Rightarrow> 'b::len0 word"
-  where "revcast w =  of_bl (takefill False (len_of TYPE('b)) (to_bl w))"
+  where "revcast w =  of_bl (takefill False (LENGTH('b)) (to_bl w))"
 
 definition slice1 :: "nat \<Rightarrow> 'a::len0 word \<Rightarrow> 'b::len0 word"
   where "slice1 n w = of_bl (takefill False n (to_bl w))"
 
 definition slice :: "nat \<Rightarrow> 'a::len0 word \<Rightarrow> 'b::len0 word"

 
 
 subsection \<open>Split and cat operations\<close>
 
 definition word_cat :: "'a::len0 word \<Rightarrow> 'b::len0 word \<Rightarrow> 'c::len0 word"
-  where "word_cat a b = word_of_int (bin_cat (uint a) (len_of TYPE('b)) (uint b))"
+  where "word_cat a b = word_of_int (bin_cat (uint a) (LENGTH('b)) (uint b))"
 
 definition word_split :: "'a::len0 word \<Rightarrow> 'b::len0 word \<times> 'c::len0 word"
   where "word_split a =
-    (case bin_split (len_of TYPE('c)) (uint a) of
+    (case bin_split (LENGTH('c)) (uint a) of
       (u, v) \<Rightarrow> (word_of_int u, word_of_int v))"
 
 definition word_rcat :: "'a::len0 word list \<Rightarrow> 'b::len0 word"
-  where "word_rcat ws = word_of_int (bin_rcat (len_of TYPE('a)) (map uint ws))"
+  where "word_rcat ws = word_of_int (bin_rcat (LENGTH('a)) (map uint ws))"
 
 definition word_rsplit :: "'a::len0 word \<Rightarrow> 'b::len word list"
-  where "word_rsplit w = map word_of_int (bin_rsplit (len_of TYPE('b)) (len_of TYPE('a), uint w))"
+  where "word_rsplit w = map word_of_int (bin_rsplit (LENGTH('b)) (LENGTH('a), uint w))"
 
 definition max_word :: "'a::len word"
   \<comment> \<open>Largest representable machine integer.\<close>
-  where "max_word = word_of_int (2 ^ len_of TYPE('a) - 1)"
+  where "max_word = word_of_int (2 ^ LENGTH('a) - 1)"
 
 lemmas of_nth_def = word_set_bits_def (* FIXME duplicate *)
 
 
 subsection \<open>Theorems about typedefs\<close>
 
-lemma sint_sbintrunc': "sint (word_of_int bin :: 'a word) = sbintrunc (len_of TYPE('a::len) - 1) bin"
+lemma sint_sbintrunc': "sint (word_of_int bin :: 'a word) = sbintrunc (LENGTH('a::len) - 1) bin"
   by (auto simp: sint_uint word_ubin.eq_norm sbintrunc_bintrunc_lt)
 
-lemma uint_sint: "uint w = bintrunc (len_of TYPE('a)) (sint w)"
+lemma uint_sint: "uint w = bintrunc (LENGTH('a)) (sint w)"
   for w :: "'a::len word"
   by (auto simp: sint_uint bintrunc_sbintrunc_le)
 
-lemma bintr_uint: "len_of TYPE('a) \<le> n \<Longrightarrow> bintrunc n (uint w) = uint w"
+lemma bintr_uint: "LENGTH('a) \<le> n \<Longrightarrow> bintrunc n (uint w) = uint w"
   for w :: "'a::len0 word"
   apply (subst word_ubin.norm_Rep [symmetric])
   apply (simp only: bintrunc_bintrunc_min word_size)
   apply (simp add: min.absorb2)
   done
 
 lemma wi_bintr:
-  "len_of TYPE('a::len0) \<le> n \<Longrightarrow>
+  "LENGTH('a::len0) \<le> n \<Longrightarrow>
     word_of_int (bintrunc 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 (len_of TYPE('a::len)))
-    (sbintrunc (len_of TYPE('a) - 1))"
+  "td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (LENGTH('a::len)))
+    (sbintrunc (LENGTH('a) - 1))"
   apply (unfold td_ext_def' sint_uint)
   apply (simp add : word_ubin.eq_norm)
-  apply (cases "len_of TYPE('a)")
+  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 (len_of TYPE('a::len)))
-     (\<lambda>w. (w + 2 ^ (len_of TYPE('a) - 1)) mod 2 ^ len_of TYPE('a) -
-         2 ^ (len_of TYPE('a) - 1))"
+  "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.

 \<close>
 interpretation word_sint:
   td_ext
     "sint ::'a::len word \<Rightarrow> int"
     word_of_int
-    "sints (len_of TYPE('a::len))"
-    "\<lambda>w. (w + 2^(len_of TYPE('a::len) - 1)) mod 2^len_of TYPE('a::len) -
-      2 ^ (len_of TYPE('a::len) - 1)"
+    "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 (len_of TYPE('a::len))"
-    "sbintrunc (len_of TYPE('a::len) - 1)"
+    "sints (LENGTH('a::len))"
+    "sbintrunc (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 to_bl_def': "(to_bl :: 'a::len0 word \<Rightarrow> bool list) = bin_to_bl (len_of TYPE('a)) \<circ> uint"
+lemma to_bl_def': "(to_bl :: 'a::len0 word \<Rightarrow> bool list) = bin_to_bl (LENGTH('a)) \<circ> uint"
   by (auto simp: to_bl_def)
 
 lemmas word_reverse_no_def [simp] =
   word_reverse_def [of "numeral w"] for w
 

   apply (simp_all add: rel_fun_def word.pcr_cr_eq cr_word_def)
   using word_numeral_alt [symmetric] word_neg_numeral_alt [symmetric] by auto
 
 lemma uint_bintrunc [simp]:
   "uint (numeral bin :: 'a word) =
-    bintrunc (len_of TYPE('a::len0)) (numeral bin)"
+    bintrunc (LENGTH('a::len0)) (numeral bin)"
   unfolding word_numeral_alt by (rule word_ubin.eq_norm)
 
 lemma uint_bintrunc_neg [simp]:
-  "uint (- numeral bin :: 'a word) = bintrunc (len_of TYPE('a::len0)) (- numeral bin)"
+  "uint (- numeral bin :: 'a word) = bintrunc (LENGTH('a::len0)) (- numeral bin)"
   by (simp only: word_neg_numeral_alt word_ubin.eq_norm)
 
 lemma sint_sbintrunc [simp]:
-  "sint (numeral bin :: 'a word) = sbintrunc (len_of TYPE('a::len) - 1) (numeral bin)"
+  "sint (numeral bin :: 'a word) = sbintrunc (LENGTH('a::len) - 1) (numeral bin)"
   by (simp only: word_numeral_alt word_sbin.eq_norm)
 
 lemma sint_sbintrunc_neg [simp]:
-  "sint (- numeral bin :: 'a word) = sbintrunc (len_of TYPE('a::len) - 1) (- numeral bin)"
+  "sint (- numeral bin :: 'a word) = sbintrunc (LENGTH('a::len) - 1) (- numeral bin)"
   by (simp only: word_neg_numeral_alt word_sbin.eq_norm)
 
 lemma unat_bintrunc [simp]:
-  "unat (numeral bin :: 'a::len0 word) = nat (bintrunc (len_of TYPE('a)) (numeral bin))"
+  "unat (numeral bin :: 'a::len0 word) = nat (bintrunc (LENGTH('a)) (numeral bin))"
   by (simp only: unat_def uint_bintrunc)
 
 lemma unat_bintrunc_neg [simp]:
-  "unat (- numeral bin :: 'a::len0 word) = nat (bintrunc (len_of TYPE('a)) (- numeral bin))"
+  "unat (- numeral bin :: 'a::len0 word) = nat (bintrunc (LENGTH('a)) (- numeral bin))"
   by (simp only: unat_def uint_bintrunc_neg)
 
 lemma size_0_eq: "size w = 0 \<Longrightarrow> v = w"
   for v w :: "'a::len0 word"
   apply (unfold word_size)

 
 lemma uint_ge_0 [iff]: "0 \<le> uint x"
   for x :: "'a::len0 word"
   using word_uint.Rep [of x] by (simp add: uints_num)
 
-lemma uint_lt2p [iff]: "uint x < 2 ^ len_of TYPE('a)"
+lemma uint_lt2p [iff]: "uint x < 2 ^ LENGTH('a)"
   for x :: "'a::len0 word"
   using word_uint.Rep [of x] by (simp add: uints_num)
 
-lemma sint_ge: "- (2 ^ (len_of TYPE('a) - 1)) \<le> sint x"
+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)
 
-lemma sint_lt: "sint x < 2 ^ (len_of TYPE('a) - 1)"
+lemma sint_lt: "sint x < 2 ^ (LENGTH('a) - 1)"
   for x :: "'a::len word"
   using word_sint.Rep [of x] by (simp add: sints_num)
 
 lemma sign_uint_Pls [simp]: "bin_sign (uint x) = 0"
   by (simp add: sign_Pls_ge_0)
 
-lemma uint_m2p_neg: "uint x - 2 ^ len_of TYPE('a) < 0"
+lemma uint_m2p_neg: "uint x - 2 ^ LENGTH('a) < 0"
   for x :: "'a::len0 word"
   by (simp only: diff_less_0_iff_less uint_lt2p)
 
-lemma uint_m2p_not_non_neg: "\<not> 0 \<le> uint x - 2 ^ len_of TYPE('a)"
+lemma uint_m2p_not_non_neg: "\<not> 0 \<le> uint x - 2 ^ LENGTH('a)"
   for x :: "'a::len0 word"
   by (simp only: not_le uint_m2p_neg)
 
-lemma lt2p_lem: "len_of TYPE('a) \<le> n \<Longrightarrow> uint w < 2 ^ n"
+lemma lt2p_lem: "LENGTH('a) \<le> n \<Longrightarrow> uint w < 2 ^ n"
   for w :: "'a::len0 word"
   by (metis bintr_uint bintrunc_mod2p int_mod_lem zless2p)
 
 lemma uint_le_0_iff [simp]: "uint x \<le> 0 \<longleftrightarrow> uint x = 0"
   by (fact uint_ge_0 [THEN leD, THEN linorder_antisym_conv1])
 
 lemma uint_nat: "uint w = int (unat w)"
   by (auto simp: unat_def)
 
-lemma uint_numeral: "uint (numeral b :: 'a::len0 word) = numeral b mod 2 ^ len_of TYPE('a)"
+lemma uint_numeral: "uint (numeral b :: 'a::len0 word) = numeral b mod 2 ^ LENGTH('a)"
   by (simp only: word_numeral_alt int_word_uint)
 
-lemma uint_neg_numeral: "uint (- numeral b :: 'a::len0 word) = - numeral b mod 2 ^ len_of TYPE('a)"
+lemma uint_neg_numeral: "uint (- numeral b :: 'a::len0 word) = - numeral b mod 2 ^ LENGTH('a)"
   by (simp only: word_neg_numeral_alt int_word_uint)
 
-lemma unat_numeral: "unat (numeral b :: 'a::len0 word) = numeral b mod 2 ^ len_of TYPE('a)"
+lemma unat_numeral: "unat (numeral b :: 'a::len0 word) = numeral b mod 2 ^ LENGTH('a)"
   apply (unfold unat_def)
   apply (clarsimp simp only: uint_numeral)
   apply (rule nat_mod_distrib [THEN trans])
     apply (rule zero_le_numeral)
    apply (simp_all add: nat_power_eq)
   done
 
 lemma sint_numeral:
   "sint (numeral b :: 'a::len word) =
     (numeral b +
-      2 ^ (len_of TYPE('a) - 1)) mod 2 ^ len_of TYPE('a) -
-      2 ^ (len_of TYPE('a) - 1)"
+      2 ^ (LENGTH('a) - 1)) mod 2 ^ LENGTH('a) -
+      2 ^ (LENGTH('a) - 1)"
   unfolding word_numeral_alt by (rule int_word_sint)
 
 lemma word_of_int_0 [simp, code_post]: "word_of_int 0 = 0"
   unfolding word_0_wi ..
 

 lemma word_of_int_neg_numeral [simp]:
   "(word_of_int (- numeral bin) :: 'a::len0 word) = - numeral bin"
   by (simp only: word_numeral_alt wi_hom_syms)
 
 lemma word_int_case_wi:
-  "word_int_case f (word_of_int i :: 'b word) = f (i mod 2 ^ len_of TYPE('b::len0))"
+  "word_int_case f (word_of_int i :: 'b word) = f (i mod 2 ^ LENGTH('b::len0))"
   by (simp add: word_int_case_def word_uint.eq_norm)
 
 lemma word_int_split:
   "P (word_int_case f x) =
-    (\<forall>i. x = (word_of_int i :: 'b::len0 word) \<and> 0 \<le> i \<and> i < 2 ^ len_of TYPE('b) \<longrightarrow> P (f i))"
+    (\<forall>i. x = (word_of_int i :: 'b::len0 word) \<and> 0 \<le> i \<and> i < 2 ^ LENGTH('b) \<longrightarrow> P (f i))"
   by (auto simp: word_int_case_def word_uint.eq_norm mod_pos_pos_trivial)
 
 lemma word_int_split_asm:
   "P (word_int_case f x) =
-    (\<nexists>n. x = (word_of_int n :: 'b::len0 word) \<and> 0 \<le> n \<and> n < 2 ^ len_of TYPE('b::len0) \<and> \<not> P (f n))"
+    (\<nexists>n. x = (word_of_int n :: 'b::len0 word) \<and> 0 \<le> n \<and> n < 2 ^ LENGTH('b::len0) \<and> \<not> P (f n))"
   by (auto simp: word_int_case_def word_uint.eq_norm mod_pos_pos_trivial)
 
 lemmas uint_range' = word_uint.Rep [unfolded uints_num mem_Collect_eq]
 lemmas sint_range' = word_sint.Rep [unfolded One_nat_def sints_num mem_Collect_eq]
 

   apply (subst word_ubin.norm_Rep [symmetric])
   apply (simp only: nth_bintr word_size)
   apply fast
   done
 
-lemma word_eq_iff: "x = y \<longleftrightarrow> (\<forall>n<len_of TYPE('a). x !! n = y !! n)"
+lemma word_eq_iff: "x = y \<longleftrightarrow> (\<forall>n<LENGTH('a). x !! n = y !! n)"
   for x y :: "'a::len0 word"
   unfolding uint_inject [symmetric] bin_eq_iff word_test_bit_def [symmetric]
   by (metis test_bit_size [unfolded word_size])
 
 lemma word_eqI: "(\<And>n. n < size u \<longrightarrow> u !! n = v !! n) \<Longrightarrow> u = v"

 lemma test_bit_bin': "w !! n \<longleftrightarrow> n < size w \<and> bin_nth (uint w) n"
   by (simp add: word_test_bit_def word_size nth_bintr [symmetric])
 
 lemmas test_bit_bin = test_bit_bin' [unfolded word_size]
 
-lemma bin_nth_uint_imp: "bin_nth (uint w) n \<Longrightarrow> n < len_of TYPE('a)"
+lemma bin_nth_uint_imp: "bin_nth (uint w) n \<Longrightarrow> n < LENGTH('a)"
   for w :: "'a::len0 word"
   apply (rule nth_bintr [THEN iffD1, THEN conjunct1])
   apply (subst word_ubin.norm_Rep)
   apply assumption
   done
 
 lemma bin_nth_sint:
-  "len_of TYPE('a) \<le> n \<Longrightarrow>
-    bin_nth (sint w) n = bin_nth (sint w) (len_of TYPE('a) - 1)"
+  "LENGTH('a) \<le> n \<Longrightarrow>
+    bin_nth (sint w) n = bin_nth (sint w) (LENGTH('a) - 1)"
   for w :: "'a::len word"
   apply (subst word_sbin.norm_Rep [symmetric])
   apply (auto simp add: nth_sbintr)
   done
 
 \<comment> \<open>type definitions theorem for in terms of equivalent bool list\<close>
 lemma td_bl:
   "type_definition
     (to_bl :: 'a::len0 word \<Rightarrow> bool list)
     of_bl
-    {bl. length bl = len_of TYPE('a)}"
+    {bl. length bl = LENGTH('a)}"
   apply (unfold type_definition_def of_bl_def to_bl_def)
   apply (simp add: word_ubin.eq_norm)
   apply safe
   apply (drule sym)
   apply simp

 
 interpretation word_bl:
   type_definition
     "to_bl :: 'a::len0 word \<Rightarrow> bool list"
     of_bl
-    "{bl. length bl = len_of TYPE('a::len0)}"
+    "{bl. length bl = LENGTH('a::len0)}"
   by (fact td_bl)
 
 lemmas word_bl_Rep' = word_bl.Rep [unfolded mem_Collect_eq, iff]
 
 lemma word_size_bl: "size w = size (to_bl w)"

   apply (rule trans [OF _ bl_sbin_sign])
   apply simp
   done
 
 lemma of_bl_drop':
-  "lend = length bl - len_of TYPE('a::len0) \<Longrightarrow>
+  "lend = length bl - LENGTH('a::len0) \<Longrightarrow>
     of_bl (drop lend bl) = (of_bl bl :: 'a word)"
   by (auto simp: of_bl_def trunc_bl2bin [symmetric])
 
 lemma test_bit_of_bl:
-  "(of_bl bl::'a::len0 word) !! n = (rev bl ! n \<and> n < len_of TYPE('a) \<and> n < length bl)"
+  "(of_bl bl::'a::len0 word) !! n = (rev bl ! n \<and> n < LENGTH('a) \<and> n < length bl)"
   by (auto simp add: of_bl_def word_test_bit_def word_size
       word_ubin.eq_norm nth_bintr bin_nth_of_bl)
 
-lemma no_of_bl: "(numeral bin ::'a::len0 word) = of_bl (bin_to_bl (len_of TYPE('a)) (numeral bin))"
+lemma no_of_bl: "(numeral bin ::'a::len0 word) = of_bl (bin_to_bl (LENGTH('a)) (numeral bin))"
   by (simp add: of_bl_def)
 
 lemma uint_bl: "to_bl w = bin_to_bl (size w) (uint w)"
   by (auto simp: word_size to_bl_def)
 
 lemma to_bl_bin: "bl_to_bin (to_bl w) = uint w"
   by (simp add: uint_bl word_size)
 
-lemma to_bl_of_bin: "to_bl (word_of_int bin::'a::len0 word) = bin_to_bl (len_of TYPE('a)) bin"
+lemma to_bl_of_bin: "to_bl (word_of_int bin::'a::len0 word) = bin_to_bl (LENGTH('a)) bin"
   by (auto simp: uint_bl word_ubin.eq_norm word_size)
 
 lemma to_bl_numeral [simp]:
   "to_bl (numeral bin::'a::len0 word) =
-    bin_to_bl (len_of TYPE('a)) (numeral bin)"
+    bin_to_bl (LENGTH('a)) (numeral bin)"
   unfolding word_numeral_alt by (rule to_bl_of_bin)
 
 lemma to_bl_neg_numeral [simp]:
   "to_bl (- numeral bin::'a::len0 word) =
-    bin_to_bl (len_of TYPE('a)) (- numeral bin)"
+    bin_to_bl (LENGTH('a)) (- numeral bin)"
   unfolding word_neg_numeral_alt by (rule to_bl_of_bin)
 
 lemma to_bl_to_bin [simp] : "bl_to_bin (to_bl w) = uint w"
   by (simp add: uint_bl word_size)
 
-lemma uint_bl_bin: "bl_to_bin (bin_to_bl (len_of TYPE('a)) (uint x)) = uint x"
+lemma uint_bl_bin: "bl_to_bin (bin_to_bl (LENGTH('a)) (uint x)) = uint x"
   for x :: "'a::len0 word"
   by (rule trans [OF bin_bl_bin word_ubin.norm_Rep])
 
 \<comment> \<open>naturals\<close>
 lemma uints_unats: "uints n = int ` unats n"

   word_ubin.norm_eq_iff [of "numeral a" "numeral b", symmetric, folded word_numeral_alt] for a b
 lemmas sbintr_num =
   word_sbin.norm_eq_iff [of "numeral a" "numeral b", symmetric, folded word_numeral_alt] for a b
 
 lemma num_of_bintr':
-  "bintrunc (len_of TYPE('a::len0)) (numeral a) = (numeral b) \<Longrightarrow>
+  "bintrunc (LENGTH('a::len0)) (numeral a) = (numeral b) \<Longrightarrow>
     numeral a = (numeral b :: 'a word)"
   unfolding bintr_num by (erule subst, simp)
 
 lemma num_of_sbintr':
-  "sbintrunc (len_of TYPE('a::len) - 1) (numeral a) = (numeral b) \<Longrightarrow>
+  "sbintrunc (LENGTH('a::len) - 1) (numeral a) = (numeral b) \<Longrightarrow>
     numeral a = (numeral b :: 'a word)"
   unfolding sbintr_num by (erule subst, simp)
 
 lemma num_abs_bintr:
   "(numeral x :: 'a word) =
-    word_of_int (bintrunc (len_of TYPE('a::len0)) (numeral x))"
+    word_of_int (bintrunc (LENGTH('a::len0)) (numeral x))"
   by (simp only: word_ubin.Abs_norm word_numeral_alt)
 
 lemma num_abs_sbintr:
   "(numeral x :: 'a word) =
-    word_of_int (sbintrunc (len_of TYPE('a::len) - 1) (numeral x))"
+    word_of_int (sbintrunc (LENGTH('a::len) - 1) (numeral x))"
   by (simp only: word_sbin.Abs_norm word_numeral_alt)
 
 text \<open>
   \<open>cast\<close> -- note, no arg for new length, as it's determined by type of result,
   thus in \<open>cast w = w\<close>, the type means cast to length of \<open>w\<close>!

   by (auto simp: scast_def)
 
 lemma ucast_bl: "ucast w = of_bl (to_bl w)"
   by (auto simp: ucast_def of_bl_def uint_bl word_size)
 
-lemma nth_ucast: "(ucast w::'a::len0 word) !! n = (w !! n \<and> n < len_of TYPE('a))"
+lemma nth_ucast: "(ucast w::'a::len0 word) !! n = (w !! n \<and> n < LENGTH('a))"
   by (simp add: ucast_def test_bit_bin word_ubin.eq_norm nth_bintr word_size)
     (fast elim!: bin_nth_uint_imp)
 
 \<comment> \<open>literal u(s)cast\<close>
 lemma ucast_bintr [simp]:
   "ucast (numeral w :: 'a::len0 word) =
-    word_of_int (bintrunc (len_of TYPE('a)) (numeral w))"
+    word_of_int (bintrunc (LENGTH('a)) (numeral w))"
   by (simp add: ucast_def)
 
 (* TODO: neg_numeral *)
 
 lemma scast_sbintr [simp]:
   "scast (numeral w ::'a::len word) =
-    word_of_int (sbintrunc (len_of TYPE('a) - Suc 0) (numeral w))"
+    word_of_int (sbintrunc (LENGTH('a) - Suc 0) (numeral w))"
   by (simp add: scast_def)
 
-lemma source_size: "source_size (c::'a::len0 word \<Rightarrow> _) = len_of TYPE('a)"
+lemma source_size: "source_size (c::'a::len0 word \<Rightarrow> _) = LENGTH('a)"
   unfolding source_size_def word_size Let_def ..
 
-lemma target_size: "target_size (c::_ \<Rightarrow> 'b::len0 word) = len_of TYPE('b)"
+lemma target_size: "target_size (c::_ \<Rightarrow> 'b::len0 word) = LENGTH('b)"
   unfolding target_size_def word_size Let_def ..
 
-lemma is_down: "is_down c \<longleftrightarrow> len_of TYPE('b) \<le> len_of TYPE('a)"
+lemma is_down: "is_down c \<longleftrightarrow> LENGTH('b) \<le> LENGTH('a)"
   for c :: "'a::len0 word \<Rightarrow> 'b::len0 word"
   by (simp only: is_down_def source_size target_size)
 
-lemma is_up: "is_up c \<longleftrightarrow> len_of TYPE('a) \<le> len_of TYPE('b)"
+lemma is_up: "is_up c \<longleftrightarrow> LENGTH('a) \<le> LENGTH('b)"
   for c :: "'a::len0 word \<Rightarrow> 'b::len0 word"
   by (simp only: is_up_def source_size target_size)
 
 lemmas is_up_down = trans [OF is_up is_down [symmetric]]
 

   apply simp
   done
 
 lemma word_rev_tf:
   "to_bl (of_bl bl::'a::len0 word) =
-    rev (takefill False (len_of TYPE('a)) (rev bl))"
+    rev (takefill False (LENGTH('a)) (rev bl))"
   by (auto simp: of_bl_def uint_bl bl_bin_bl_rtf word_ubin.eq_norm word_size)
 
 lemma word_rep_drop:
   "to_bl (of_bl bl::'a::len0 word) =
-    replicate (len_of TYPE('a) - length bl) False @
-    drop (length bl - len_of TYPE('a)) bl"
+    replicate (LENGTH('a) - length bl) False @
+    drop (length bl - LENGTH('a)) bl"
   by (simp add: word_rev_tf takefill_alt rev_take)
 
 lemma to_bl_ucast:
   "to_bl (ucast (w::'b::len0 word) ::'a::len0 word) =
-    replicate (len_of TYPE('a) - len_of TYPE('b)) False @
-    drop (len_of TYPE('b) - len_of TYPE('a)) (to_bl w)"
+    replicate (LENGTH('a) - LENGTH('b)) False @
+    drop (LENGTH('b) - LENGTH('a)) (to_bl w)"
   apply (unfold ucast_bl)
   apply (rule trans)
    apply (rule word_rep_drop)
   apply simp
   done

   unfolding word_0_wi word_ubin.eq_norm by simp
 
 lemma of_bl_0 [simp]: "of_bl (replicate n False) = 0"
   by (simp add: of_bl_def bl_to_bin_rep_False)
 
-lemma to_bl_0 [simp]: "to_bl (0::'a::len0 word) = replicate (len_of TYPE('a)) False"
+lemma to_bl_0 [simp]: "to_bl (0::'a::len0 word) = replicate (LENGTH('a)) False"
   by (simp add: uint_bl word_size bin_to_bl_zero)
 
 lemma uint_0_iff: "uint x = 0 \<longleftrightarrow> x = 0"
   by (simp add: word_uint_eq_iff)
 

 lemma uint_cong: "x = y \<Longrightarrow> uint x = uint y"
   by simp
 
 lemma uint_word_ariths:
   fixes a b :: "'a::len0 word"
-  shows "uint (a + b) = (uint a + uint b) mod 2 ^ len_of TYPE('a::len0)"
-    and "uint (a - b) = (uint a - uint b) mod 2 ^ len_of TYPE('a)"
-    and "uint (a * b) = uint a * uint b mod 2 ^ len_of TYPE('a)"
-    and "uint (- a) = - uint a mod 2 ^ len_of TYPE('a)"
-    and "uint (word_succ a) = (uint a + 1) mod 2 ^ len_of TYPE('a)"
-    and "uint (word_pred a) = (uint a - 1) mod 2 ^ len_of TYPE('a)"
-    and "uint (0 :: 'a word) = 0 mod 2 ^ len_of TYPE('a)"
-    and "uint (1 :: 'a word) = 1 mod 2 ^ len_of TYPE('a)"
+  shows "uint (a + b) = (uint a + uint b) mod 2 ^ LENGTH('a::len0)"
+    and "uint (a - b) = (uint a - uint b) mod 2 ^ LENGTH('a)"
+    and "uint (a * b) = uint a * uint b mod 2 ^ LENGTH('a)"
+    and "uint (- a) = - uint a mod 2 ^ LENGTH('a)"
+    and "uint (word_succ a) = (uint a + 1) mod 2 ^ LENGTH('a)"
+    and "uint (word_pred a) = (uint a - 1) mod 2 ^ LENGTH('a)"
+    and "uint (0 :: 'a word) = 0 mod 2 ^ LENGTH('a)"
+    and "uint (1 :: 'a word) = 1 mod 2 ^ LENGTH('a)"
   by (simp_all add: word_arith_wis [THEN trans [OF uint_cong int_word_uint]])
 
 lemma uint_word_arith_bintrs:
   fixes a b :: "'a::len0 word"
-  shows "uint (a + b) = bintrunc (len_of TYPE('a)) (uint a + uint b)"
-    and "uint (a - b) = bintrunc (len_of TYPE('a)) (uint a - uint b)"
-    and "uint (a * b) = bintrunc (len_of TYPE('a)) (uint a * uint b)"
-    and "uint (- a) = bintrunc (len_of TYPE('a)) (- uint a)"
-    and "uint (word_succ a) = bintrunc (len_of TYPE('a)) (uint a + 1)"
-    and "uint (word_pred a) = bintrunc (len_of TYPE('a)) (uint a - 1)"
-    and "uint (0 :: 'a word) = bintrunc (len_of TYPE('a)) 0"
-    and "uint (1 :: 'a word) = bintrunc (len_of TYPE('a)) 1"
+  shows "uint (a + b) = bintrunc (LENGTH('a)) (uint a + uint b)"
+    and "uint (a - b) = bintrunc (LENGTH('a)) (uint a - uint b)"
+    and "uint (a * b) = bintrunc (LENGTH('a)) (uint a * uint b)"
+    and "uint (- a) = bintrunc (LENGTH('a)) (- uint a)"
+    and "uint (word_succ a) = bintrunc (LENGTH('a)) (uint a + 1)"
+    and "uint (word_pred a) = bintrunc (LENGTH('a)) (uint a - 1)"
+    and "uint (0 :: 'a word) = bintrunc (LENGTH('a)) 0"
+    and "uint (1 :: 'a word) = bintrunc (LENGTH('a)) 1"
   by (simp_all add: uint_word_ariths bintrunc_mod2p)
 
 lemma sint_word_ariths:
   fixes a b :: "'a::len word"
-  shows "sint (a + b) = sbintrunc (len_of TYPE('a) - 1) (sint a + sint b)"
-    and "sint (a - b) = sbintrunc (len_of TYPE('a) - 1) (sint a - sint b)"
-    and "sint (a * b) = sbintrunc (len_of TYPE('a) - 1) (sint a * sint b)"
-    and "sint (- a) = sbintrunc (len_of TYPE('a) - 1) (- sint a)"
-    and "sint (word_succ a) = sbintrunc (len_of TYPE('a) - 1) (sint a + 1)"
-    and "sint (word_pred a) = sbintrunc (len_of TYPE('a) - 1) (sint a - 1)"
-    and "sint (0 :: 'a word) = sbintrunc (len_of TYPE('a) - 1) 0"
-    and "sint (1 :: 'a word) = sbintrunc (len_of TYPE('a) - 1) 1"
+  shows "sint (a + b) = sbintrunc (LENGTH('a) - 1) (sint a + sint b)"
+    and "sint (a - b) = sbintrunc (LENGTH('a) - 1) (sint a - sint b)"
+    and "sint (a * b) = sbintrunc (LENGTH('a) - 1) (sint a * sint b)"
+    and "sint (- a) = sbintrunc (LENGTH('a) - 1) (- sint a)"
+    and "sint (word_succ a) = sbintrunc (LENGTH('a) - 1) (sint a + 1)"
+    and "sint (word_pred a) = sbintrunc (LENGTH('a) - 1) (sint a - 1)"
+    and "sint (0 :: 'a word) = sbintrunc (LENGTH('a) - 1) 0"
+    and "sint (1 :: 'a word) = sbintrunc (LENGTH('a) - 1) 1"
          apply (simp_all only: word_sbin.inverse_norm [symmetric])
          apply (simp_all add: wi_hom_syms)
    apply transfer apply simp
   apply transfer apply simp
   done

   unfolding unat_def word_less_alt
   by (rule nat_less_eq_zless [symmetric]) simp
 
 lemma wi_less:
   "(word_of_int n < (word_of_int m :: 'a::len0 word)) =
-    (n mod 2 ^ len_of TYPE('a) < m mod 2 ^ len_of TYPE('a))"
+    (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::len0 word)) =
-    (n mod 2 ^ len_of TYPE('a) \<le> m mod 2 ^ len_of TYPE('a))"
+    (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)"
   apply (unfold udvd_def)
   apply safe

   have "0 \<le> uint w" by (fact uint_nonnegative)
   moreover from assms have "0 \<noteq> uint w"
     by (simp add: uint_0_iff)
   ultimately have "1 \<le> uint w"
     by arith
-  from uint_lt2p [of w] have "uint w - 1 < 2 ^ len_of TYPE('a)"
+  from uint_lt2p [of w] have "uint w - 1 < 2 ^ LENGTH('a)"
     by arith
-  with \<open>1 \<le> uint w\<close> have "(uint w - 1) mod 2 ^ len_of TYPE('a) = uint w - 1"
+  with \<open>1 \<le> uint w\<close> have "(uint w - 1) mod 2 ^ LENGTH('a) = uint w - 1"
     by (auto intro: mod_pos_pos_trivial)
-  with \<open>1 \<le> uint w\<close> have "nat ((uint w - 1) mod 2 ^ len_of TYPE('a)) = nat (uint w) - 1"
+  with \<open>1 \<le> uint w\<close> have "nat ((uint w - 1) mod 2 ^ LENGTH('a)) = nat (uint w) - 1"
     by auto
   then show ?thesis
     by (simp only: unat_def int_word_uint word_arith_wis mod_diff_right_eq)
 qed
 

   by (simp add: unat_minus_one) (simp add: unat_0_iff [symmetric])
 
 lemmas uint_add_ge0 [simp] = add_nonneg_nonneg [OF uint_ge_0 uint_ge_0]
 lemmas uint_mult_ge0 [simp] = mult_nonneg_nonneg [OF uint_ge_0 uint_ge_0]
 
-lemma uint_sub_lt2p [simp]: "uint x - uint y < 2 ^ len_of TYPE('a)"
+lemma uint_sub_lt2p [simp]: "uint x - uint y < 2 ^ LENGTH('a)"
   for x :: "'a::len0 word" and y :: "'b::len0 word"
   using uint_ge_0 [of y] uint_lt2p [of x] by arith
 
 
 subsection \<open>Conditions for the addition (etc) of two words to overflow\<close>
 
 lemma uint_add_lem:
-  "(uint x + uint y < 2 ^ len_of TYPE('a)) =
+  "(uint x + uint y < 2 ^ LENGTH('a)) =
     (uint (x + y) = uint x + uint y)"
   for x y :: "'a::len0 word"
   by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])
 
 lemma uint_mult_lem:
-  "(uint x * uint y < 2 ^ len_of TYPE('a)) =
+  "(uint x * uint y < 2 ^ LENGTH('a)) =
     (uint (x * y) = uint x * uint y)"
   for x y :: "'a::len0 word"
   by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])
 
 lemma uint_sub_lem: "uint x \<ge> uint y \<longleftrightarrow> uint (x - y) = uint x - uint y"

   for x y z :: int
   by (auto intro: int_mod_eq)
 
 lemma uint_plus_if':
   "uint (a + b) =
-    (if uint a + uint b < 2 ^ len_of TYPE('a) then uint a + uint b
-     else uint a + uint b - 2 ^ len_of TYPE('a))"
+    (if uint a + uint b < 2 ^ LENGTH('a) then uint a + uint b
+     else uint a + uint b - 2 ^ LENGTH('a))"
   for a b :: "'a::len0 word"
   using mod_add_if_z [of "uint a" _ "uint b"] by (simp add: uint_word_ariths)
 
 lemma mod_sub_if_z:
   "x < z \<Longrightarrow> y < z \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> z \<Longrightarrow>

   by (auto intro: int_mod_eq)
 
 lemma uint_sub_if':
   "uint (a - b) =
     (if uint b \<le> uint a then uint a - uint b
-     else uint a - uint b + 2 ^ len_of TYPE('a))"
+     else uint a - uint b + 2 ^ LENGTH('a))"
   for a b :: "'a::len0 word"
   using mod_sub_if_z [of "uint a" _ "uint b"] by (simp add: uint_word_ariths)
 
 
 subsection \<open>Definition of \<open>uint_arith\<close>\<close>
 
 lemma word_of_int_inverse:
-  "word_of_int r = a \<Longrightarrow> 0 \<le> r \<Longrightarrow> r < 2 ^ len_of TYPE('a) \<Longrightarrow> uint a = r"
+  "word_of_int r = a \<Longrightarrow> 0 \<le> r \<Longrightarrow> r < 2 ^ LENGTH('a) \<Longrightarrow> uint a = r"
   for a :: "'a::len0 word"
   apply (erule word_uint.Abs_inverse' [rotated])
   apply (simp add: uints_num)
   done
 
 lemma uint_split:
-  "P (uint x) = (\<forall>i. word_of_int i = x \<and> 0 \<le> i \<and> i < 2^len_of TYPE('a) \<longrightarrow> P i)"
+  "P (uint x) = (\<forall>i. word_of_int i = x \<and> 0 \<le> i \<and> i < 2^LENGTH('a) \<longrightarrow> P i)"
   for x :: "'a::len0 word"
   apply (fold word_int_case_def)
   apply (auto dest!: word_of_int_inverse simp: int_word_uint mod_pos_pos_trivial
       split: word_int_split)
   done
 
 lemma uint_split_asm:
-  "P (uint x) = (\<nexists>i. word_of_int i = x \<and> 0 \<le> i \<and> i < 2^len_of TYPE('a) \<and> \<not> P i)"
+  "P (uint x) = (\<nexists>i. word_of_int i = x \<and> 0 \<le> i \<and> i < 2^LENGTH('a) \<and> \<not> P i)"
   for x :: "'a::len0 word"
   by (auto dest!: word_of_int_inverse
       simp: int_word_uint mod_pos_pos_trivial
       split: uint_split)
 

 lemmas uint_arith_simps =
   word_le_def word_less_alt
   word_uint.Rep_inject [symmetric]
   uint_sub_if' uint_plus_if'
 
-\<comment> \<open>use this to stop, eg. \<open>2 ^ len_of TYPE(32)\<close> being simplified\<close>
+\<comment> \<open>use this to stop, eg. \<open>2 ^ LENGTH(32)\<close> being simplified\<close>
 lemma power_False_cong: "False \<Longrightarrow> a ^ b = c ^ d"
   by auto
 
 \<comment> \<open>\<open>uint_arith_tac\<close>: reduce to arithmetic on int, try to solve by arith\<close>
 ML \<open>

 
 lemma no_ulen_sub: "x \<ge> x - y \<longleftrightarrow> uint y \<le> uint x"
   for x y :: "'a::len0 word"
   by uint_arith
 
-lemma no_olen_add': "x \<le> y + x \<longleftrightarrow> uint y + uint x < 2 ^ len_of TYPE('a)"
+lemma no_olen_add': "x \<le> y + x \<longleftrightarrow> uint y + uint x < 2 ^ LENGTH('a)"
   for x y :: "'a::len0 word"
   by (simp add: ac_simps no_olen_add)
 
 lemmas olen_add_eqv = trans [OF no_olen_add no_olen_add' [symmetric]]
 

   note that \<open>iszero_def\<close> is only for class \<open>comm_semiring_1_cancel\<close>,
   which requires word length \<open>\<ge> 1\<close>, ie \<open>'a::len word\<close>
 \<close>
 lemma iszero_word_no [simp]:
   "iszero (numeral bin :: 'a::len word) =
-    iszero (bintrunc (len_of TYPE('a)) (numeral bin))"
+    iszero (bintrunc (LENGTH('a)) (numeral bin))"
   using word_ubin.norm_eq_iff [where 'a='a, of "numeral bin" 0]
   by (simp add: iszero_def [symmetric])
 
 text \<open>Use \<open>iszero\<close> to simplify equalities between word numerals.\<close>
 

 
 
 subsection \<open>Word and nat\<close>
 
 lemma td_ext_unat [OF refl]:
-  "n = len_of TYPE('a::len) \<Longrightarrow>
+  "n = LENGTH('a::len) \<Longrightarrow>
     td_ext (unat :: 'a word \<Rightarrow> nat) of_nat (unats n) (\<lambda>i. i mod 2 ^ n)"
   apply (unfold td_ext_def' unat_def word_of_nat unats_uints)
   apply (auto intro!: imageI simp add : word_of_int_hom_syms)
    apply (erule word_uint.Abs_inverse [THEN arg_cong])
   apply (simp add: int_word_uint nat_mod_distrib nat_power_eq)

 
 interpretation word_unat:
   td_ext
     "unat::'a::len word \<Rightarrow> nat"
     of_nat
-    "unats (len_of TYPE('a::len))"
-    "\<lambda>i. i mod 2 ^ len_of TYPE('a::len)"
+    "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 (len_of TYPE('a))"
+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 ^ len_of TYPE('a)"
+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)
   apply (unfold unats_def)
   apply auto
   done
 
-lemma of_nat_eq: "of_nat n = w \<longleftrightarrow> (\<exists>q. n = unat w + q * 2 ^ len_of TYPE('a))"
+lemma of_nat_eq: "of_nat n = w \<longleftrightarrow> (\<exists>q. n = unat w + q * 2 ^ LENGTH('a))"
   for w :: "'a::len word"
   using mod_div_mult_eq [of n "2 ^ LENGTH('a)", symmetric]
   by (auto simp add: word_unat.inverse_norm)
 
 lemma of_nat_eq_size: "of_nat n = w \<longleftrightarrow> (\<exists>q. n = unat w + q * 2 ^ size w)"
   unfolding word_size by (rule of_nat_eq)
 
-lemma of_nat_0: "of_nat m = (0::'a::len word) \<longleftrightarrow> (\<exists>q. m = q * 2 ^ len_of TYPE('a))"
+lemma of_nat_0: "of_nat m = (0::'a::len word) \<longleftrightarrow> (\<exists>q. m = q * 2 ^ LENGTH('a))"
   by (simp add: of_nat_eq)
 
-lemma of_nat_2p [simp]: "of_nat (2 ^ len_of TYPE('a)) = (0::'a::len word)"
+lemma of_nat_2p [simp]: "of_nat (2 ^ LENGTH('a)) = (0::'a::len word)"
   by (fact mult_1 [symmetric, THEN iffD2 [OF of_nat_0 exI]])
 
 lemma of_nat_gt_0: "of_nat k \<noteq> 0 \<Longrightarrow> 0 < k"
   by (cases k) auto
 
-lemma of_nat_neq_0: "0 < k \<Longrightarrow> k < 2 ^ len_of TYPE('a::len) \<Longrightarrow> of_nat k \<noteq> (0 :: 'a word)"
+lemma of_nat_neq_0: "0 < k \<Longrightarrow> k < 2 ^ LENGTH('a::len) \<Longrightarrow> of_nat k \<noteq> (0 :: 'a word)"
   by (auto simp add : of_nat_0)
 
 lemma Abs_fnat_hom_add: "of_nat a + of_nat b = of_nat (a + b)"
   by simp
 

 
 lemmas word_sub_less_iff = word_sub_le_iff
   [unfolded linorder_not_less [symmetric] Not_eq_iff]
 
 lemma unat_add_lem:
-  "unat x + unat y < 2 ^ len_of TYPE('a) \<longleftrightarrow> unat (x + y) = unat x + unat y"
+  "unat x + unat y < 2 ^ LENGTH('a) \<longleftrightarrow> unat (x + y) = unat x + unat y"
   for x y :: "'a::len word"
   by (auto simp: unat_word_ariths intro!: trans [OF _ nat_mod_lem])
 
 lemma unat_mult_lem:
-  "unat x * unat y < 2 ^ len_of TYPE('a) \<longleftrightarrow> unat (x * y) = unat x * unat y"
+  "unat x * unat y < 2 ^ LENGTH('a) \<longleftrightarrow> unat (x * y) = unat x * unat y"
   for x y :: "'a::len word"
   by (auto simp: unat_word_ariths intro!: trans [OF _ nat_mod_lem])
 
 lemmas unat_plus_if' =
   trans [OF unat_word_ariths(1) mod_nat_add, simplified]

   for x y :: "'a::len word"
   by (simp add: uint_nat unat_mod zmod_int)
 
 text \<open>Definition of \<open>unat_arith\<close> tactic\<close>
 
-lemma unat_split: "P (unat x) \<longleftrightarrow> (\<forall>n. of_nat n = x \<and> n < 2^len_of TYPE('a) \<longrightarrow> P n)"
+lemma unat_split: "P (unat x) \<longleftrightarrow> (\<forall>n. of_nat n = x \<and> n < 2^LENGTH('a) \<longrightarrow> P n)"
   for x :: "'a::len word"
   by (auto simp: unat_of_nat)
 
-lemma unat_split_asm: "P (unat x) \<longleftrightarrow> (\<nexists>n. of_nat n = x \<and> n < 2^len_of TYPE('a) \<and> \<not> P n)"
+lemma unat_split_asm: "P (unat x) \<longleftrightarrow> (\<nexists>n. of_nat n = x \<and> n < 2^LENGTH('a) \<and> \<not> P n)"
   for x :: "'a::len word"
   by (auto simp: unat_of_nat)
 
 lemmas of_nat_inverse =
   word_unat.Abs_inverse' [rotated, unfolded unats_def, simplified]

   no_plus_overflow_unat_size [unfolded word_size]
 
 lemmas unat_plus_simple =
   trans [OF no_olen_add_nat unat_add_lem]
 
-lemma word_div_mult: "0 < y \<Longrightarrow> unat x * unat y < 2 ^ len_of TYPE('a) \<Longrightarrow> x * y div y = x"
+lemma word_div_mult: "0 < y \<Longrightarrow> unat x * unat y < 2 ^ LENGTH('a) \<Longrightarrow> x * y div y = x"
   for x y :: "'a::len word"
   apply unat_arith
   apply clarsimp
   apply (subst unat_mult_lem [THEN iffD1])
    apply auto
   done
 
-lemma div_lt': "i \<le> k div x \<Longrightarrow> unat i * unat x < 2 ^ len_of TYPE('a)"
+lemma div_lt': "i \<le> k div x \<Longrightarrow> unat i * unat x < 2 ^ LENGTH('a)"
   for i k x :: "'a::len word"
   apply unat_arith
   apply clarsimp
   apply (drule mult_le_mono1)
   apply (erule order_le_less_trans)

   apply (drule mult_le_mono1)
   apply (erule order_trans)
   apply (rule div_mult_le)
   done
 
-lemma div_lt_uint': "i \<le> k div x \<Longrightarrow> uint i * uint x < 2 ^ len_of TYPE('a)"
+lemma div_lt_uint': "i \<le> k div x \<Longrightarrow> uint i * uint x < 2 ^ LENGTH('a)"
   for i k x :: "'a::len word"
   apply (unfold uint_nat)
   apply (drule div_lt')
   apply (metis of_nat_less_iff of_nat_mult of_nat_numeral of_nat_power)
   done
 
 lemmas div_lt_uint'' = order_less_imp_le [THEN div_lt_uint']
 
-lemma word_le_exists': "x \<le> y \<Longrightarrow> \<exists>z. y = x + z \<and> uint x + uint z < 2 ^ len_of TYPE('a)"
+lemma word_le_exists': "x \<le> y \<Longrightarrow> \<exists>z. y = x + z \<and> uint x + uint z < 2 ^ LENGTH('a)"
   for x y z :: "'a::len0 word"
   apply (rule exI)
   apply (rule conjI)
    apply (rule zadd_diff_inverse)
   apply uint_arith

 
 lemma word_arith_power_alt: "a ^ n = (word_of_int (uint a ^ n) :: 'a::len word)"
   by (simp add : word_of_int_power_hom [symmetric])
 
 lemma of_bl_length_less:
-  "length x = k \<Longrightarrow> k < len_of TYPE('a) \<Longrightarrow> (of_bl x :: 'a::len word) < 2 ^ k"
+  "length x = k \<Longrightarrow> k < LENGTH('a) \<Longrightarrow> (of_bl x :: 'a::len word) < 2 ^ k"
   apply (unfold of_bl_def word_less_alt word_numeral_alt)
   apply safe
   apply (simp (no_asm) add: word_of_int_power_hom word_uint.eq_norm
       del: word_of_int_numeral)
   apply (simp add: mod_pos_pos_trivial)

 
 lemma uint_and: "uint (x AND y) = uint x AND uint y"
   by (transfer, simp add: bin_trunc_ao)
 
 lemma test_bit_wi [simp]:
-  "(word_of_int x :: 'a::len0 word) !! n \<longleftrightarrow> n < len_of TYPE('a) \<and> bin_nth x n"
+  "(word_of_int x :: 'a::len0 word) !! n \<longleftrightarrow> n < LENGTH('a) \<and> bin_nth x n"
   by (simp add: word_test_bit_def word_ubin.eq_norm nth_bintr)
 
 lemma word_test_bit_transfer [transfer_rule]:
   "(rel_fun pcr_word (rel_fun (=) (=)))
-    (\<lambda>x n. n < len_of TYPE('a) \<and> bin_nth x n) (test_bit :: 'a::len0 word \<Rightarrow> _)"
+    (\<lambda>x n. n < LENGTH('a) \<and> bin_nth x n) (test_bit :: 'a::len0 word \<Rightarrow> _)"
   unfolding rel_fun_def word.pcr_cr_eq cr_word_def by simp
 
 lemma word_ops_nth_size:
   "n < size x \<Longrightarrow>
     (x OR y) !! n = (x !! n | y !! n) \<and>

   for x :: "'a::len0 word"
   by transfer (auto simp add: bin_nth_ops)
 
 lemma test_bit_numeral [simp]:
   "(numeral w :: 'a::len0 word) !! n \<longleftrightarrow>
-    n < len_of TYPE('a) \<and> bin_nth (numeral w) n"
+    n < LENGTH('a) \<and> bin_nth (numeral w) n"
   by transfer (rule refl)
 
 lemma test_bit_neg_numeral [simp]:
   "(- numeral w :: 'a::len0 word) !! n \<longleftrightarrow>
-    n < len_of TYPE('a) \<and> bin_nth (- numeral w) n"
+    n < LENGTH('a) \<and> bin_nth (- numeral w) n"
   by transfer (rule refl)
 
 lemma test_bit_1 [simp]: "(1 :: 'a::len word) !! n \<longleftrightarrow> n = 0"
   by transfer auto
 
 lemma nth_0 [simp]: "\<not> (0 :: 'a::len0 word) !! n"
   by transfer simp
 
-lemma nth_minus1 [simp]: "(-1 :: 'a::len0 word) !! n \<longleftrightarrow> n < len_of TYPE('a)"
+lemma nth_minus1 [simp]: "(-1 :: 'a::len0 word) !! n \<longleftrightarrow> n < LENGTH('a)"
   by transfer simp
 
 \<comment> \<open>get from commutativity, associativity etc of \<open>int_and\<close> etc to same for \<open>word_and etc\<close>\<close>
 lemmas bwsimps =
   wi_hom_add

   by (auto simp: word_lsb_def bin_last_def)
 
 lemma word_msb_sint: "msb w \<longleftrightarrow> sint w < 0"
   by (simp only: word_msb_def sign_Min_lt_0)
 
-lemma msb_word_of_int: "msb (word_of_int x::'a::len word) = bin_nth x (len_of TYPE('a) - 1)"
+lemma msb_word_of_int: "msb (word_of_int x::'a::len word) = bin_nth x (LENGTH('a) - 1)"
   by (simp add: word_msb_def word_sbin.eq_norm bin_sign_lem)
 
 lemma word_msb_numeral [simp]:
-  "msb (numeral w::'a::len word) = bin_nth (numeral w) (len_of TYPE('a) - 1)"
+  "msb (numeral w::'a::len word) = bin_nth (numeral w) (LENGTH('a) - 1)"
   unfolding word_numeral_alt by (rule msb_word_of_int)
 
 lemma word_msb_neg_numeral [simp]:
-  "msb (- numeral w::'a::len word) = bin_nth (- numeral w) (len_of TYPE('a) - 1)"
+  "msb (- numeral w::'a::len word) = bin_nth (- numeral w) (LENGTH('a) - 1)"
   unfolding word_neg_numeral_alt by (rule msb_word_of_int)
 
 lemma word_msb_0 [simp]: "\<not> msb (0::'a::len word)"
   by (simp add: word_msb_def)
 
-lemma word_msb_1 [simp]: "msb (1::'a::len word) \<longleftrightarrow> len_of TYPE('a) = 1"
+lemma word_msb_1 [simp]: "msb (1::'a::len word) \<longleftrightarrow> LENGTH('a) = 1"
   unfolding word_1_wi msb_word_of_int eq_iff [where 'a=nat]
   by (simp add: Suc_le_eq)
 
-lemma word_msb_nth: "msb w = bin_nth (uint w) (len_of TYPE('a) - 1)"
+lemma word_msb_nth: "msb w = bin_nth (uint w) (LENGTH('a) - 1)"
   for w :: "'a::len word"
   by (simp add: word_msb_def sint_uint bin_sign_lem)
 
 lemma word_msb_alt: "msb w = hd (to_bl w)"
   for w :: "'a::len word"

   done
 
 lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs"
   by (auto simp: of_bl_def bl_to_bin_rep_F)
 
-lemma msb_nth: "msb w = w !! (len_of TYPE('a) - 1)"
+lemma msb_nth: "msb w = w !! (LENGTH('a) - 1)"
   for w :: "'a::len word"
   by (simp add: word_msb_nth word_test_bit_def)
 
 lemmas msb0 = len_gt_0 [THEN diff_Suc_less, THEN word_ops_nth_size [unfolded word_size]]
 lemmas msb1 = msb0 [where i = 0]

 
 interpretation test_bit:
   td_ext
     "(!!) :: 'a::len0 word \<Rightarrow> nat \<Rightarrow> bool"
     set_bits
-    "{f. \<forall>i. f i \<longrightarrow> i < len_of TYPE('a::len0)}"
-    "(\<lambda>h i. h i \<and> i < len_of TYPE('a::len0))"
+    "{f. \<forall>i. f i \<longrightarrow> i < LENGTH('a::len0)}"
+    "(\<lambda>h i. h i \<and> i < LENGTH('a::len0))"
   by (rule td_ext_nth)
 
 lemmas td_nth = test_bit.td_thm
 
 lemma word_set_set_same [simp]: "set_bit (set_bit w n x) n y = set_bit w n y"

   shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x"
   by (rule word_eqI) (auto simp: test_bit_set_gen word_size assms)
 
 lemma nth_sint:
   fixes w :: "'a::len word"
-  defines "l \<equiv> len_of TYPE('a)"
+  defines "l \<equiv> LENGTH('a)"
   shows "bin_nth (sint w) n = (if n < l - 1 then w !! n else w !! (l - 1))"
   unfolding sint_uint l_def
   by (auto simp: nth_sbintr word_test_bit_def [symmetric])
 
 lemma word_lsb_numeral [simp]:

 
 lemma clearBit_no [simp]:
   "clearBit (numeral bin) n = word_of_int (bin_sc n False (numeral bin))"
   by (simp add: clearBit_def)
 
-lemma to_bl_n1: "to_bl (-1::'a::len0 word) = replicate (len_of TYPE('a)) True"
+lemma to_bl_n1: "to_bl (-1::'a::len0 word) = replicate (LENGTH('a)) True"
   apply (rule word_bl.Abs_inverse')
    apply simp
   apply (rule word_eqI)
   apply (clarsimp simp add: word_size)
   apply (auto simp add: word_bl.Abs_inverse test_bit_bl word_size)

   apply (clarsimp simp add : test_bit_set_gen)
   apply (drule test_bit_size)
   apply force
   done
 
-lemma test_bit_2p: "(word_of_int (2 ^ n)::'a::len word) !! m \<longleftrightarrow> m = n \<and> m < len_of TYPE('a)"
+lemma test_bit_2p: "(word_of_int (2 ^ n)::'a::len word) !! m \<longleftrightarrow> m = n \<and> m < LENGTH('a)"
   by (auto simp: word_test_bit_def word_ubin.eq_norm nth_bintr nth_2p_bin)
 
-lemma nth_w2p: "((2::'a::len word) ^ n) !! m \<longleftrightarrow> m = n \<and> m < len_of TYPE('a::len)"
+lemma nth_w2p: "((2::'a::len word) ^ n) !! m \<longleftrightarrow> m = n \<and> m < LENGTH('a::len)"
   by (simp add: test_bit_2p [symmetric] word_of_int [symmetric])
 
 lemma uint_2p: "(0::'a::len word) < 2 ^ n \<Longrightarrow> uint (2 ^ n::'a::len word) = 2 ^ n"
   apply (unfold word_arith_power_alt)
-  apply (case_tac "len_of TYPE('a)")
+  apply (case_tac "LENGTH('a)")
    apply clarsimp
   apply (case_tac "nat")
    apply clarsimp
    apply (case_tac "n")
     apply clarsimp

   for w :: "'a::len word"
   by (induct n) (auto simp: shiftl_def shiftl1_2t)
 
 lemma shiftr1_bintr [simp]:
   "(shiftr1 (numeral w) :: 'a::len0 word) =
-    word_of_int (bin_rest (bintrunc (len_of TYPE('a)) (numeral w)))"
+    word_of_int (bin_rest (bintrunc (LENGTH('a)) (numeral w)))"
   unfolding shiftr1_def word_numeral_alt by (simp add: word_ubin.eq_norm)
 
 lemma sshiftr1_sbintr [simp]:
   "(sshiftr1 (numeral w) :: 'a::len word) =
-    word_of_int (bin_rest (sbintrunc (len_of TYPE('a) - 1) (numeral w)))"
+    word_of_int (bin_rest (sbintrunc (LENGTH('a) - 1) (numeral w)))"
   unfolding sshiftr1_def word_numeral_alt by (simp add: word_sbin.eq_norm)
 
 lemma shiftr_no [simp]:
   (* FIXME: neg_numeral *)
   "(numeral w::'a::len0 word) >> n = word_of_int
-    ((bin_rest ^^ n) (bintrunc (len_of TYPE('a)) (numeral w)))"
+    ((bin_rest ^^ n) (bintrunc (LENGTH('a)) (numeral w)))"
   by (rule word_eqI) (auto simp: nth_shiftr nth_rest_power_bin nth_bintr word_size)
 
 lemma sshiftr_no [simp]:
   (* FIXME: neg_numeral *)
   "(numeral w::'a::len word) >>> n = word_of_int
-    ((bin_rest ^^ n) (sbintrunc (len_of TYPE('a) - 1) (numeral w)))"
+    ((bin_rest ^^ n) (sbintrunc (LENGTH('a) - 1) (numeral w)))"
   apply (rule word_eqI)
   apply (auto simp: nth_sshiftr nth_rest_power_bin nth_sbintr word_size)
-   apply (subgoal_tac "na + n = len_of TYPE('a) - Suc 0", simp, simp)+
+   apply (subgoal_tac "na + n = LENGTH('a) - Suc 0", simp, simp)+
   done
 
 lemma shiftr1_bl_of:
-  "length bl \<le> len_of TYPE('a) \<Longrightarrow>
+  "length bl \<le> LENGTH('a) \<Longrightarrow>
     shiftr1 (of_bl bl::'a::len0 word) = of_bl (butlast bl)"
   by (clarsimp simp: shiftr1_def of_bl_def butlast_rest_bl2bin word_ubin.eq_norm trunc_bl2bin)
 
 lemma shiftr_bl_of:
-  "length bl \<le> len_of TYPE('a) \<Longrightarrow>
+  "length bl \<le> LENGTH('a) \<Longrightarrow>
     (of_bl bl::'a::len0 word) >> n = of_bl (take (length bl - n) bl)"
   apply (unfold shiftr_def)
   apply (induct n)
    apply clarsimp
   apply clarsimp
   apply (subst shiftr1_bl_of)
    apply simp
   apply (simp add: butlast_take)
   done
 
-lemma shiftr_bl: "x >> n \<equiv> of_bl (take (len_of TYPE('a) - n) (to_bl x))"
+lemma shiftr_bl: "x >> n \<equiv> of_bl (take (LENGTH('a) - n) (to_bl x))"
   for x :: "'a::len0 word"
   using shiftr_bl_of [where 'a='a, of "to_bl x"] by simp
 
-lemma msb_shift: "msb w \<longleftrightarrow> w >> (len_of TYPE('a) - 1) \<noteq> 0"
+lemma msb_shift: "msb w \<longleftrightarrow> w >> (LENGTH('a) - 1) \<noteq> 0"
   for w :: "'a::len word"
   apply (unfold shiftr_bl word_msb_alt)
   apply (simp add: word_size Suc_le_eq take_Suc)
   apply (cases "hd (to_bl w)")
    apply (auto simp: word_1_bl of_bl_rep_False [where n=1 and bs="[]", simplified])

 lemma and_mask_no: "numeral i AND mask n = word_of_int (bintrunc n (numeral i))"
   unfolding word_numeral_alt by (rule and_mask_wi)
 
 lemma bl_and_mask':
   "to_bl (w AND mask n :: 'a::len word) =
-    replicate (len_of TYPE('a) - n) False @
-    drop (len_of TYPE('a) - n) (to_bl w)"
+    replicate (LENGTH('a) - n) False @
+    drop (LENGTH('a) - n) (to_bl w)"
   apply (rule nth_equalityI)
    apply simp
   apply (clarsimp simp add: to_bl_nth word_size)
   apply (simp add: word_size word_ops_nth_size)
   apply (auto simp add: word_size test_bit_bl nth_append nth_rev)

 lemmas revcast_def' = revcast_def [simplified]
 lemmas revcast_def'' = revcast_def' [simplified word_size]
 lemmas revcast_no_def [simp] = revcast_def' [where w="numeral w", unfolded word_size] for w
 
 lemma to_bl_revcast:
-  "to_bl (revcast w :: 'a::len0 word) = takefill False (len_of TYPE('a)) (to_bl w)"
+  "to_bl (revcast w :: 'a::len0 word) = takefill False (LENGTH('a)) (to_bl w)"
   apply (unfold revcast_def' word_size)
   apply (rule word_bl.Abs_inverse)
   apply simp
   done
 

 
 
 subsubsection \<open>Slices\<close>
 
 lemma slice1_no_bin [simp]:
-  "slice1 n (numeral w :: 'b word) = of_bl (takefill False n (bin_to_bl (len_of TYPE('b::len0)) (numeral w)))"
+  "slice1 n (numeral w :: 'b word) = of_bl (takefill False n (bin_to_bl (LENGTH('b::len0)) (numeral w)))"
   by (simp add: slice1_def) (* TODO: neg_numeral *)
 
 lemma slice_no_bin [simp]:
-  "slice n (numeral w :: 'b word) = of_bl (takefill False (len_of TYPE('b::len0) - n)
-    (bin_to_bl (len_of TYPE('b::len0)) (numeral w)))"
+  "slice n (numeral w :: 'b word) = of_bl (takefill False (LENGTH('b::len0) - n)
+    (bin_to_bl (LENGTH('b::len0)) (numeral w)))"
   by (simp add: slice_def word_size) (* TODO: neg_numeral *)
 
 lemma slice1_0 [simp] : "slice1 n 0 = 0"
   unfolding slice1_def by simp
 

   apply (unfold slice_take shiftr_bl)
   apply (rule ucast_of_bl_up [symmetric])
   apply (simp add: word_size)
   done
 
-lemma nth_slice: "(slice n w :: 'a::len0 word) !! m = (w !! (m + n) \<and> m < len_of TYPE('a))"
+lemma nth_slice: "(slice n w :: 'a::len0 word) !! m = (w !! (m + n) \<and> m < LENGTH('a))"
   by (simp add: slice_shiftr nth_ucast nth_shiftr)
 
 lemma slice1_down_alt':
   "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs + k = n \<Longrightarrow>
     to_bl sl = takefill False fs (drop k (to_bl w))"

 lemma slice1_up_alt':
   "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs = n + k \<Longrightarrow>
     to_bl sl = takefill False fs (replicate k False @ (to_bl w))"
   apply (unfold slice1_def word_size of_bl_def uint_bl)
   apply (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop takefill_append [symmetric])
-  apply (rule_tac f = "\<lambda>k. takefill False (len_of TYPE('a))
-    (replicate k False @ bin_to_bl (len_of TYPE('b)) (uint w))" in arg_cong)
+  apply (rule_tac f = "\<lambda>k. takefill False (LENGTH('a))
+    (replicate k False @ bin_to_bl (LENGTH('b)) (uint w))" in arg_cong)
   apply arith
   done
 
 lemmas sd1 = slice1_down_alt' [OF refl refl, unfolded word_size]
 lemmas su1 = slice1_up_alt' [OF refl refl, unfolded word_size]

 lemma revcast_slice1 [OF refl]: "rc = revcast w \<Longrightarrow> slice1 (size rc) w = rc"
   by (simp add: slice1_def revcast_def' word_size)
 
 lemma slice1_tf_tf':
   "to_bl (slice1 n w :: 'a::len0 word) =
-    rev (takefill False (len_of TYPE('a)) (rev (takefill False n (to_bl w))))"
+    rev (takefill False (LENGTH('a)) (rev (takefill False n (to_bl w))))"
   unfolding slice1_def by (rule word_rev_tf)
 
 lemmas slice1_tf_tf = slice1_tf_tf' [THEN word_bl.Rep_inverse', symmetric]
 
 lemma rev_slice1:
-  "n + k = len_of TYPE('a) + len_of TYPE('b) \<Longrightarrow>
+  "n + k = LENGTH('a) + LENGTH('b) \<Longrightarrow>
     slice1 n (word_reverse w :: 'b::len0 word) =
     word_reverse (slice1 k w :: 'a::len0 word)"
   apply (unfold word_reverse_def slice1_tf_tf)
   apply (rule word_bl.Rep_inverse')
   apply (rule rev_swap [THEN iffD1])

    apply (simp add: word_bl.Abs_inverse)
   apply (simp add: word_bl.Abs_inverse)
   done
 
 lemma rev_slice:
-  "n + k + len_of TYPE('a::len0) = len_of TYPE('b::len0) \<Longrightarrow>
+  "n + k + LENGTH('a::len0) = LENGTH('b::len0) \<Longrightarrow>
     slice n (word_reverse (w::'b word)) = word_reverse (slice k w :: 'a word)"
   apply (unfold slice_def word_size)
   apply (rule rev_slice1)
   apply arith
   done

 lemma sofl_test:
   "(sint x + sint y = sint (x + y)) =
      ((((x + y) XOR x) AND ((x + y) XOR y)) >> (size x - 1) = 0)"
   for x y :: "'a::len word"
   apply (unfold word_size)
-  apply (cases "len_of TYPE('a)", simp)
+  apply (cases "LENGTH('a)", simp)
   apply (subst msb_shift [THEN sym_notr])
   apply (simp add: word_ops_msb)
   apply (simp add: word_msb_sint)
   apply safe
        apply simp_all

 lemmas word_split_bin' = word_split_def
 lemmas word_cat_bin' = word_cat_def
 
 lemma word_rsplit_no:
   "(word_rsplit (numeral bin :: 'b::len0 word) :: 'a word list) =
-    map word_of_int (bin_rsplit (len_of TYPE('a::len))
-      (len_of TYPE('b), bintrunc (len_of TYPE('b)) (numeral bin)))"
+    map word_of_int (bin_rsplit (LENGTH('a::len))
+      (LENGTH('b), bintrunc (LENGTH('b)) (numeral bin)))"
   by (simp add: word_rsplit_def word_ubin.eq_norm)
 
 lemmas word_rsplit_no_cl [simp] = word_rsplit_no
   [unfolded bin_rsplitl_def bin_rsplit_l [symmetric]]
 

 
 lemma of_bl_Cons: "of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs"
   by (cases x) simp_all
 
 lemma split_uint_lem: "bin_split n (uint w) = (a, b) \<Longrightarrow>
-    a = bintrunc (len_of TYPE('a) - n) a \<and> b = bintrunc (len_of TYPE('a)) b"
+    a = bintrunc (LENGTH('a) - n) a \<and> b = bintrunc (LENGTH('a)) b"
   for w :: "'a::len0 word"
   apply (frule word_ubin.norm_Rep [THEN ssubst])
   apply (drule bin_split_trunc1)
   apply (drule sym [THEN trans])
    apply assumption

    apply (simp add: of_bl_def bl2bin_drop word_size
       word_ubin.norm_eq_iff [symmetric] min_def del: word_ubin.norm_Rep)
   apply (clarsimp split: prod.splits)
   apply (frule split_uint_lem [THEN conjunct1])
   apply (unfold word_size)
-  apply (cases "len_of TYPE('a) \<ge> len_of TYPE('b)")
+  apply (cases "LENGTH('a) \<ge> LENGTH('b)")
    defer
    apply simp
   apply (simp add : of_bl_def to_bl_def)
   apply (subst bin_split_take1 [symmetric])
     prefer 2

    apply (auto simp add: word_size)
   done
 
 lemma word_split_bl_eq:
   "(word_split c :: ('c::len0 word \<times> 'd::len0 word)) =
-    (of_bl (take (len_of TYPE('a::len) - len_of TYPE('d::len0)) (to_bl c)),
-     of_bl (drop (len_of TYPE('a) - len_of TYPE('d)) (to_bl c)))"
+    (of_bl (take (LENGTH('a::len) - LENGTH('d::len0)) (to_bl c)),
+     of_bl (drop (LENGTH('a) - LENGTH('d)) (to_bl c)))"
   for c :: "'a::len word"
   apply (rule word_split_bl [THEN iffD1])
    apply (unfold word_size)
    apply (rule refl conjI)+
   done

 lemma word_cat_id: "word_cat a b = b"
   by (simp add: word_cat_bin' word_ubin.inverse_norm)
 
 \<comment> \<open>limited hom result\<close>
 lemma word_cat_hom:
-  "len_of TYPE('a::len0) \<le> len_of TYPE('b::len0) + len_of TYPE('c::len0) \<Longrightarrow>
+  "LENGTH('a::len0) \<le> LENGTH('b::len0) + LENGTH('c::len0) \<Longrightarrow>
     (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) =
     word_of_int (bin_cat w (size b) (uint b))"
   by (auto simp: word_cat_def word_size word_ubin.norm_eq_iff [symmetric]
       word_ubin.eq_norm bintr_cat min.absorb1)
 

 lemmas size_rcat_lem = size_rcat_lem' [unfolded word_size]
 
 lemmas td_gal_lt_len = len_gt_0 [THEN td_gal_lt]
 
 lemma nth_rcat_lem:
-  "n < length (wl::'a word list) * len_of TYPE('a::len) \<Longrightarrow>
+  "n < length (wl::'a word list) * LENGTH('a::len) \<Longrightarrow>
     rev (concat (map to_bl wl)) ! n =
-    rev (to_bl (rev wl ! (n div len_of TYPE('a)))) ! (n mod len_of TYPE('a))"
+    rev (to_bl (rev wl ! (n div LENGTH('a)))) ! (n mod LENGTH('a))"
   apply (induct wl)
    apply clarsimp
   apply (clarsimp simp add : nth_append size_rcat_lem)
   apply (simp (no_asm_use) only:  mult_Suc [symmetric]
          td_gal_lt_len less_Suc_eq_le minus_div_mult_eq_mod [symmetric])

   "[u,v] = p \<Longrightarrow> [su,sv] = q \<Longrightarrow> word_rsplit u = su \<Longrightarrow>
     word_rsplit v = sv \<Longrightarrow> length su = length sv"
   by (auto simp: word_rsplit_def bin_rsplit_len_indep)
 
 lemma length_word_rsplit_size:
-  "n = len_of TYPE('a::len) \<Longrightarrow>
+  "n = LENGTH('a::len) \<Longrightarrow>
     length (word_rsplit w :: 'a word list) \<le> m \<longleftrightarrow> size w \<le> m * n"
   by (auto simp: word_rsplit_def word_size bin_rsplit_len_le)
 
 lemmas length_word_rsplit_lt_size =
   length_word_rsplit_size [unfolded Not_eq_iff linorder_not_less [symmetric]]
 
 lemma length_word_rsplit_exp_size:
-  "n = len_of TYPE('a::len) \<Longrightarrow>
+  "n = LENGTH('a::len) \<Longrightarrow>
     length (word_rsplit w :: 'a word list) = (size w + n - 1) div n"
   by (auto simp: word_rsplit_def word_size bin_rsplit_len)
 
 lemma length_word_rsplit_even_size:
-  "n = len_of TYPE('a::len) \<Longrightarrow> size w = m * n \<Longrightarrow>
+  "n = LENGTH('a::len) \<Longrightarrow> size w = m * n \<Longrightarrow>
     length (word_rsplit w :: 'a word list) = m"
   by (auto simp: length_word_rsplit_exp_size given_quot_alt)
 
 lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size]
 

    apply safe
    apply (erule xtr7, rule dtle)+
   done
 
 lemma size_word_rsplit_rcat_size:
-  "word_rcat ws = frcw \<Longrightarrow> size frcw = length ws * len_of TYPE('a)
+  "word_rcat ws = frcw \<Longrightarrow> size frcw = length ws * LENGTH('a)
     \<Longrightarrow> length (word_rsplit frcw::'a word list) = length ws"
   for ws :: "'a::len word list" and frcw :: "'b::len0 word"
   apply (clarsimp simp: word_size length_word_rsplit_exp_size')
   apply (fast intro: given_quot_alt)
   done

   for n :: nat
   by (auto simp: add.commute)
 
 lemma word_rsplit_rcat_size [OF refl]:
   "word_rcat ws = frcw \<Longrightarrow>
-    size frcw = length ws * len_of TYPE('a) \<Longrightarrow> word_rsplit frcw = ws"
+    size frcw = length ws * LENGTH('a) \<Longrightarrow> word_rsplit frcw = ws"
   for ws :: "'a::len word list"
   apply (frule size_word_rsplit_rcat_size, assumption)
   apply (clarsimp simp add : word_size)
   apply (rule nth_equalityI, assumption)
   apply clarsimp

 
 subsection \<open>Maximum machine word\<close>
 
 lemma word_int_cases:
   fixes x :: "'a::len0 word"
-  obtains n where "x = word_of_int n" and "0 \<le> n" and "n < 2^len_of TYPE('a)"
+  obtains n where "x = word_of_int n" and "0 \<le> n" and "n < 2^LENGTH('a)"
   by (cases x rule: word_uint.Abs_cases) (simp add: uints_num)
 
 lemma word_nat_cases [cases type: word]:
   fixes x :: "'a::len word"
-  obtains n where "x = of_nat n" and "n < 2^len_of TYPE('a)"
+  obtains n where "x = of_nat n" and "n < 2^LENGTH('a)"
   by (cases x rule: word_unat.Abs_cases) (simp add: unats_def)
 
-lemma max_word_eq: "(max_word::'a::len word) = 2^len_of TYPE('a) - 1"
+lemma max_word_eq: "(max_word::'a::len word) = 2^LENGTH('a) - 1"
   by (simp add: max_word_def word_of_int_hom_syms word_of_int_2p)
 
 lemma max_word_max [simp,intro!]: "n \<le> max_word"
   by (cases n rule: word_int_cases)
     (simp add: max_word_def word_le_def int_word_uint mod_pos_pos_trivial del: minus_mod_self1)
 
-lemma word_of_int_2p_len: "word_of_int (2 ^ len_of TYPE('a)) = (0::'a::len0 word)"
+lemma word_of_int_2p_len: "word_of_int (2 ^ LENGTH('a)) = (0::'a::len0 word)"
   by (subst word_uint.Abs_norm [symmetric]) simp
 
-lemma word_pow_0: "(2::'a::len word) ^ len_of TYPE('a) = 0"
+lemma word_pow_0: "(2::'a::len word) ^ LENGTH('a) = 0"
 proof -
-  have "word_of_int (2 ^ len_of TYPE('a)) = (0::'a word)"
+  have "word_of_int (2 ^ LENGTH('a)) = (0::'a word)"
     by (rule word_of_int_2p_len)
   then show ?thesis by (simp add: word_of_int_2p)
 qed
 
 lemma max_word_wrap: "x + 1 = 0 \<Longrightarrow> x = max_word"

     by simp
   then show ?thesis
     by (rule max_word_wrap [symmetric])
 qed
 
-lemma max_word_bl [simp]: "to_bl (max_word::'a::len word) = replicate (len_of TYPE('a)) True"
+lemma max_word_bl [simp]: "to_bl (max_word::'a::len word) = replicate (LENGTH('a)) True"
   by (subst max_word_minus to_bl_n1)+ simp
 
-lemma max_test_bit [simp]: "(max_word::'a::len word) !! n \<longleftrightarrow> n < len_of TYPE('a)"
+lemma max_test_bit [simp]: "(max_word::'a::len word) !! n \<longleftrightarrow> n < LENGTH('a)"
   by (auto simp: test_bit_bl word_size)
 
 lemma word_and_max [simp]: "x AND max_word = x"
   by (rule word_eqI) (simp add: word_ops_nth_size word_size)
 

   for x :: "'a::len word"
   by (simp add: word_less_nat_alt unat_0_iff)
 
 lemma to_bl_mask:
   "to_bl (mask n :: 'a::len word) =
-  replicate (len_of TYPE('a) - n) False @
-    replicate (min (len_of TYPE('a)) n) True"
+  replicate (LENGTH('a) - n) False @
+    replicate (min (LENGTH('a)) n) True"
   by (simp add: mask_bl word_rep_drop min_def)
 
 lemma map_replicate_True:
   "n = length xs \<Longrightarrow>
     map (\<lambda>(x,y). x \<and> y) (zip xs (replicate n True)) = xs"

   by (induct xs arbitrary: n) auto
 
 lemma bl_and_mask:
   fixes w :: "'a::len word"
     and n :: nat
-  defines "n' \<equiv> len_of TYPE('a) - n"
+  defines "n' \<equiv> LENGTH('a) - n"
   shows "to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)"
 proof -
   note [simp] = map_replicate_True map_replicate_False
   have "to_bl (w AND mask n) = map2 (\<and>) (to_bl w) (to_bl (mask n::'a::len word))"
     by (simp add: bl_word_and)

   by (simp add: unat_def uint_sub_if_size word_le_def nat_diff_distrib)
 
 lemmas word_less_sub1_numberof [simp] = word_less_sub1 [of "numeral w"] for w
 lemmas word_le_sub1_numberof [simp] = word_le_sub1 [of "numeral w"] for w
 
-lemma word_of_int_minus: "word_of_int (2^len_of TYPE('a) - i) = (word_of_int (-i)::'a::len word)"
+lemma word_of_int_minus: "word_of_int (2^LENGTH('a) - i) = (word_of_int (-i)::'a::len word)"
 proof -
-  have *: "2^len_of TYPE('a) - i = -i + 2^len_of TYPE('a)"
+  have *: "2^LENGTH('a) - i = -i + 2^LENGTH('a)"
     by simp
   show ?thesis
     apply (subst *)
     apply (subst word_uint.Abs_norm [symmetric], subst mod_add_self2)
     apply simp

 lemma set_bits_K_False [simp]:
   "set_bits (\<lambda>_. False) = (0 :: 'a :: len0 word)"
   by (rule word_eqI) (simp add: test_bit.eq_norm)
 
 lemma test_bit_1' [simp]:
-  "(1 :: 'a :: len0 word) !! n \<longleftrightarrow> 0 < len_of TYPE('a) \<and> n = 0"
+  "(1 :: 'a :: len0 word) !! n \<longleftrightarrow> 0 < LENGTH('a) \<and> n = 0"
   by (cases n) (simp_all only: one_word_def test_bit_wi bin_nth.simps, simp_all)
 
 lemma mask_0 [simp]:
   "mask 0 = 0"
   by (simp add: Word.mask_def)