# HG changeset patch
# User haftmann
# Date 1555767856 0
# Node ID ac1706cdde25403d06c61b87dae96e6b6fdf2d94
# Parent  a7aba6db79a143c5a47e0cfadc01c50e155f6403
clarified notation

diff -r a7aba6db79a1 -r ac1706cdde25 src/HOL/Library/Saturated.thy
--- a/src/HOL/Library/Saturated.thy	Thu Apr 18 16:34:04 2019 +0200
+++ b/src/HOL/Library/Saturated.thy	Sat Apr 20 13:44:16 2019 +0000
@@ -12,7 +12,7 @@
 
 subsection \<open>The type of saturated naturals\<close>
 
-typedef (overloaded) ('a::len) sat = "{.. len_of TYPE('a)}"
+typedef (overloaded) ('a::len) sat = "{.. LENGTH('a)}"
   morphisms nat_of Abs_sat
   by auto
 
@@ -29,22 +29,22 @@
   by (fact nat_of_inverse)
 
 definition Abs_sat' :: "nat \<Rightarrow> 'a::len sat" where
-  "Abs_sat' n = Abs_sat (min (len_of TYPE('a)) n)"
+  "Abs_sat' n = Abs_sat (min (LENGTH('a)) n)"
 
 lemma nat_of_Abs_sat' [simp]:
-  "nat_of (Abs_sat' n :: ('a::len) sat) = min (len_of TYPE('a)) n"
+  "nat_of (Abs_sat' n :: ('a::len) sat) = min (LENGTH('a)) n"
   unfolding Abs_sat'_def by (rule Abs_sat_inverse) simp
 
 lemma nat_of_le_len_of [simp]:
-  "nat_of (n :: ('a::len) sat) \<le> len_of TYPE('a)"
+  "nat_of (n :: ('a::len) sat) \<le> LENGTH('a)"
   using nat_of [where x = n] by simp
 
 lemma min_len_of_nat_of [simp]:
-  "min (len_of TYPE('a)) (nat_of (n::('a::len) sat)) = nat_of n"
+  "min (LENGTH('a)) (nat_of (n::('a::len) sat)) = nat_of n"
   by (rule min.absorb2 [OF nat_of_le_len_of])
 
 lemma min_nat_of_len_of [simp]:
-  "min (nat_of (n::('a::len) sat)) (len_of TYPE('a)) = nat_of n"
+  "min (nat_of (n::('a::len) sat)) (LENGTH('a)) = nat_of n"
   by (subst min.commute) simp
 
 lemma Abs_sat'_nat_of [simp]:
@@ -80,14 +80,14 @@
   by (simp add: zero_sat_def)
 
 lemma nat_of_one_sat [simp, code abstract]:
-  "nat_of 1 = min 1 (len_of TYPE('a))"
+  "nat_of 1 = min 1 (LENGTH('a))"
   by (simp add: one_sat_def)
 
 definition
   "x + y = Abs_sat' (nat_of x + nat_of y)"
 
 lemma nat_of_plus_sat [simp, code abstract]:
-  "nat_of (x + y) = min (nat_of x + nat_of y) (len_of TYPE('a))"
+  "nat_of (x + y) = min (nat_of x + nat_of y) (LENGTH('a))"
   by (simp add: plus_sat_def)
 
 definition
@@ -96,7 +96,7 @@
 lemma nat_of_minus_sat [simp, code abstract]:
   "nat_of (x - y) = nat_of x - nat_of y"
 proof -
-  from nat_of_le_len_of [of x] have "nat_of x - nat_of y \<le> len_of TYPE('a)" by arith
+  from nat_of_le_len_of [of x] have "nat_of x - nat_of y \<le> LENGTH('a)" by arith
   then show ?thesis by (simp add: minus_sat_def)
 qed
 
@@ -104,7 +104,7 @@
   "x * y = Abs_sat' (nat_of x * nat_of y)"
 
 lemma nat_of_times_sat [simp, code abstract]:
-  "nat_of (x * y) = min (nat_of x * nat_of y) (len_of TYPE('a))"
+  "nat_of (x * y) = min (nat_of x * nat_of y) (LENGTH('a))"
   by (simp add: times_sat_def)
 
 instance
@@ -153,7 +153,7 @@
   "Sat \<equiv> of_nat"
 
 lemma nat_of_Sat [simp]:
-  "nat_of (Sat n :: ('a::len) sat) = min (len_of TYPE('a)) n"
+  "nat_of (Sat n :: ('a::len) sat) = min (LENGTH('a)) n"
   by (rule nat_of_Abs_sat' [unfolded Abs_sat'_eq_of_nat])
 
 lemma [code_abbrev]:
@@ -167,7 +167,7 @@
   where [code_abbrev]: "sat_of_nat = of_nat"
 
 lemma [code abstract]:
-  "nat_of (sat_of_nat n :: ('a::len) sat) = min (len_of TYPE('a)) n"
+  "nat_of (sat_of_nat n :: ('a::len) sat) = min (LENGTH('a)) n"
   by (simp add: sat_of_nat_def)
 
 end
@@ -195,7 +195,7 @@
 definition "(inf :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = min"
 definition "(sup :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = max"
 definition "bot = (0 :: 'a sat)"
-definition "top = Sat (len_of TYPE('a))"
+definition "top = Sat (LENGTH('a))"
 
 instance
   by standard
diff -r a7aba6db79a1 -r ac1706cdde25 src/HOL/SPARK/Examples/RIPEMD-160/Round.thy
--- a/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy	Thu Apr 18 16:34:04 2019 +0200
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy	Sat Apr 20 13:44:16 2019 +0000
@@ -191,14 +191,14 @@
       by (simp add: int_mod_eq')
     have "e mod ?MM = e" using \<open>0 <= e\<close> \<open>e <= ?M\<close>
       by (simp add: int_mod_eq')
-    have "(?MM::int) = 2 ^ len_of TYPE(32)" by simp
+    have "(?MM::int) = 2 ^ LENGTH(32)" by simp
     show ?thesis
       unfolding
         word_add_def
         uint_word_of_int_id[OF \<open>0 <= a\<close> \<open>a <= ?M\<close>]
         uint_word_of_int_id[OF \<open>0 <= ?X\<close> \<open>?X <= ?M\<close>]
         int_word_uint
-      unfolding \<open>?MM = 2 ^ len_of TYPE(32)\<close>
+      unfolding \<open>?MM = 2 ^ LENGTH(32)\<close>
       unfolding word_uint.Abs_norm
       by (simp add:
         \<open>a mod ?MM = a\<close>
@@ -231,7 +231,7 @@
       by (simp add: int_mod_eq')
     have "e' mod ?MM = e'" using \<open>0 <= e'\<close> \<open>e' <= ?M\<close>
       by (simp add: int_mod_eq')
-    have "(?MM::int) = 2 ^ len_of TYPE(32)" by simp
+    have "(?MM::int) = 2 ^ LENGTH(32)" by simp
     have nat_transfer: "79 - nat j = nat (79 - j)"
       using nat_diff_distrib \<open>0 <= j\<close>  \<open>j <= 79\<close>
       by simp
@@ -242,7 +242,7 @@
         uint_word_of_int_id[OF \<open>0 <= ?X\<close> \<open>?X <= ?M\<close>]
         int_word_uint
         nat_transfer
-      unfolding \<open>?MM = 2 ^ len_of TYPE(32)\<close>
+      unfolding \<open>?MM = 2 ^ LENGTH(32)\<close>
       unfolding word_uint.Abs_norm
       by (simp add:
         \<open>a' mod ?MM = a'\<close>
diff -r a7aba6db79a1 -r ac1706cdde25 src/HOL/SPARK/SPARK.thy
--- a/src/HOL/SPARK/SPARK.thy	Thu Apr 18 16:34:04 2019 +0200
+++ b/src/HOL/SPARK/SPARK.thy	Sat Apr 20 13:44:16 2019 +0000
@@ -38,10 +38,10 @@
 
 lemma bit_not_spark_eq:
   "NOT (word_of_int x :: ('a::len0) word) =
-  word_of_int (2 ^ len_of TYPE('a) - 1 - x)"
+  word_of_int (2 ^ LENGTH('a) - 1 - x)"
 proof -
   have "word_of_int x + NOT (word_of_int x) =
-    word_of_int x + (word_of_int (2 ^ len_of TYPE('a) - 1 - x)::'a word)"
+    word_of_int x + (word_of_int (2 ^ LENGTH('a) - 1 - x)::'a word)"
     by (simp only: bwsimps bin_add_not Min_def)
       (simp add: word_of_int_hom_syms word_of_int_2p_len)
   then show ?thesis by (rule add_left_imp_eq)
diff -r a7aba6db79a1 -r ac1706cdde25 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Thu Apr 18 16:34:04 2019 +0200
+++ b/src/HOL/Word/Word.thy	Sat Apr 20 13:44:16 2019 +0000
@@ -18,17 +18,17 @@
 
 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)
 
@@ -41,9 +41,9 @@
 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"
@@ -111,7 +111,7 @@
 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"
@@ -131,7 +131,7 @@
   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))"
@@ -150,13 +150,13 @@
   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
@@ -164,7 +164,7 @@
 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)
 
@@ -216,8 +216,8 @@
 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
@@ -228,24 +228,24 @@
   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)
 
 
@@ -317,7 +317,7 @@
 
 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
@@ -431,7 +431,7 @@
   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))"
@@ -463,36 +463,36 @@
 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)
@@ -500,16 +500,16 @@
   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)
@@ -519,9 +519,9 @@
   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>
@@ -534,24 +534,24 @@
   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] =
@@ -578,27 +578,27 @@
 
 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"
@@ -615,30 +615,30 @@
   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)
 
@@ -648,13 +648,13 @@
 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])
@@ -665,8 +665,8 @@
 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"
@@ -686,17 +686,17 @@
   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]
@@ -731,7 +731,7 @@
   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])
@@ -749,7 +749,7 @@
 
 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)
@@ -757,8 +757,8 @@
   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)
@@ -769,7 +769,7 @@
   "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
@@ -781,7 +781,7 @@
   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]
@@ -823,16 +823,16 @@
   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)"
@@ -841,23 +841,23 @@
 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])
 
@@ -878,23 +878,23 @@
   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>
@@ -911,34 +911,34 @@
 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)
 
@@ -955,19 +955,19 @@
 
 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)
@@ -1117,7 +1117,7 @@
 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"
@@ -1189,38 +1189,38 @@
 
 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
@@ -1284,12 +1284,12 @@
 
 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)"
@@ -1319,11 +1319,11 @@
     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)
@@ -1335,7 +1335,7 @@
 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
 
@@ -1343,13 +1343,13 @@
 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])
@@ -1371,8 +1371,8 @@
 
 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)
 
@@ -1385,7 +1385,7 @@
 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)
 
@@ -1393,14 +1393,14 @@
 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
@@ -1408,7 +1408,7 @@
   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
@@ -1421,7 +1421,7 @@
   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
 
@@ -1474,7 +1474,7 @@
   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)
 
@@ -1696,7 +1696,7 @@
 \<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])
 
@@ -1709,7 +1709,7 @@
 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)
@@ -1723,29 +1723,29 @@
   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)
@@ -1753,16 +1753,16 @@
 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)"
@@ -1815,12 +1815,12 @@
   [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])
 
@@ -1885,11 +1885,11 @@
 
 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)
 
@@ -1947,7 +1947,7 @@
 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
@@ -1955,7 +1955,7 @@
    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
@@ -1984,7 +1984,7 @@
   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')
@@ -1993,7 +1993,7 @@
 
 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)
@@ -2050,7 +2050,7 @@
   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
@@ -2157,12 +2157,12 @@
   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:
@@ -2182,12 +2182,12 @@
 
 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"
@@ -2196,7 +2196,7 @@
 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>
@@ -2344,25 +2344,25 @@
 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)
 
@@ -2415,7 +2415,7 @@
 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)
 
@@ -2450,8 +2450,8 @@
   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
@@ -2468,7 +2468,7 @@
 
 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])
@@ -2508,7 +2508,7 @@
   "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)
@@ -2534,15 +2534,15 @@
   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
@@ -2925,36 +2925,36 @@
 
 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)
@@ -2965,11 +2965,11 @@
   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)
@@ -3069,8 +3069,8 @@
 
 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)
@@ -3178,7 +3178,7 @@
 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
@@ -3288,12 +3288,12 @@
 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"
@@ -3318,7 +3318,7 @@
   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':
@@ -3332,8 +3332,8 @@
     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
 
@@ -3358,13 +3358,13 @@
 
 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)
@@ -3377,7 +3377,7 @@
   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)
@@ -3395,7 +3395,7 @@
      ((((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)
@@ -3431,8 +3431,8 @@
 
 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
@@ -3464,7 +3464,7 @@
   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)
@@ -3488,7 +3488,7 @@
   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)
@@ -3515,8 +3515,8 @@
 
 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)
@@ -3566,7 +3566,7 @@
 
 \<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]
@@ -3669,9 +3669,9 @@
 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)
@@ -3707,7 +3707,7 @@
   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)
 
@@ -3715,12 +3715,12 @@
   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)
 
@@ -3741,7 +3741,7 @@
   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')
@@ -3756,7 +3756,7 @@
 
 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)
@@ -4136,27 +4136,27 @@
 
 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
@@ -4175,10 +4175,10 @@
     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"
@@ -4256,8 +4256,8 @@
 
 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:
@@ -4273,7 +4273,7 @@
 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
@@ -4334,9 +4334,9 @@
 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 *)
@@ -4513,7 +4513,7 @@
   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]:
diff -r a7aba6db79a1 -r ac1706cdde25 src/HOL/Word/Word_Bitwise.thy
--- a/src/HOL/Word/Word_Bitwise.thy	Thu Apr 18 16:34:04 2019 +0200
+++ b/src/HOL/Word/Word_Bitwise.thy	Sat Apr 20 13:44:16 2019 +0000
@@ -54,12 +54,12 @@
 lemma bl_word_sub: "to_bl (x - y) = to_bl (x + (- y))"
   by simp
 
-lemma rbl_word_1: "rev (to_bl (1 :: 'a::len0 word)) = takefill False (len_of TYPE('a)) [True]"
+lemma rbl_word_1: "rev (to_bl (1 :: 'a::len0 word)) = takefill False (LENGTH('a)) [True]"
   apply (rule_tac s="rev (to_bl (word_succ (0 :: 'a word)))" in trans)
    apply simp
   apply (simp only: rtb_rbl_ariths(1)[OF refl])
   apply simp
-  apply (case_tac "len_of TYPE('a)")
+  apply (case_tac "LENGTH('a)")
    apply simp
   apply (simp add: takefill_alt)
   done
@@ -120,21 +120,21 @@
 
 lemma rbl_word_cat:
   "rev (to_bl (word_cat x y :: 'a::len0 word)) =
-    takefill False (len_of TYPE('a)) (rev (to_bl y) @ rev (to_bl x))"
+    takefill False (LENGTH('a)) (rev (to_bl y) @ rev (to_bl x))"
   by (simp add: word_cat_bl word_rev_tf)
 
 lemma rbl_word_slice:
   "rev (to_bl (slice n w :: 'a::len0 word)) =
-    takefill False (len_of TYPE('a)) (drop n (rev (to_bl w)))"
+    takefill False (LENGTH('a)) (drop n (rev (to_bl w)))"
   apply (simp add: slice_take word_rev_tf rev_take)
-  apply (cases "n < len_of TYPE('b)", simp_all)
+  apply (cases "n < LENGTH('b)", simp_all)
   done
 
 lemma rbl_word_ucast:
-  "rev (to_bl (ucast x :: 'a::len0 word)) = takefill False (len_of TYPE('a)) (rev (to_bl x))"
+  "rev (to_bl (ucast x :: 'a::len0 word)) = takefill False (LENGTH('a)) (rev (to_bl x))"
   apply (simp add: to_bl_ucast takefill_alt)
   apply (simp add: rev_drop)
-  apply (cases "len_of TYPE('a) < len_of TYPE('b)")
+  apply (cases "LENGTH('a) < LENGTH('b)")
    apply simp_all
   done
 
@@ -172,14 +172,14 @@
    apply (simp add: word_size takefill_last_def takefill_alt
       last_rev word_msb_alt word_rev_tf
       drop_nonempty_def take_Cons')
-   apply (case_tac "len_of TYPE('a)", simp_all)
+   apply (case_tac "LENGTH('a)", simp_all)
   apply (rule word_eqI)
   apply (simp add: nth_sshiftr word_size test_bit_of_bl
       msb_nth)
   done
 
 lemma nth_word_of_int:
-  "(word_of_int x :: 'a::len0 word) !! n = (n < len_of TYPE('a) \<and> bin_nth x n)"
+  "(word_of_int x :: 'a::len0 word) !! n = (n < LENGTH('a) \<and> bin_nth x n)"
   apply (simp add: test_bit_bl word_size to_bl_of_bin)
   apply (subst conj_cong[OF refl], erule bin_nth_bl)
   apply auto
@@ -187,18 +187,18 @@
 
 lemma nth_scast:
   "(scast (x :: 'a::len word) :: 'b::len word) !! n =
-    (n < len_of TYPE('b) \<and>
-    (if n < len_of TYPE('a) - 1 then x !! n
-     else x !! (len_of TYPE('a) - 1)))"
+    (n < LENGTH('b) \<and>
+    (if n < LENGTH('a) - 1 then x !! n
+     else x !! (LENGTH('a) - 1)))"
   by (simp add: scast_def nth_sint)
 
 lemma rbl_word_scast:
-  "rev (to_bl (scast x :: 'a::len word)) = takefill_last False (len_of TYPE('a)) (rev (to_bl x))"
+  "rev (to_bl (scast x :: 'a::len word)) = takefill_last False (LENGTH('a)) (rev (to_bl x))"
   apply (rule nth_equalityI)
    apply (simp add: word_size takefill_last_def)
   apply (clarsimp simp: nth_scast takefill_last_def
       nth_takefill word_size nth_rev to_bl_nth)
-  apply (cases "len_of TYPE('b)")
+  apply (cases "LENGTH('b)")
    apply simp
   apply (clarsimp simp: less_Suc_eq_le linorder_not_less
       last_rev word_msb_alt[symmetric]
@@ -313,7 +313,7 @@
    apply (simp add: sints_num word_size)
    apply (rule conjI)
     apply (simp add: le_diff_eq')
-    apply (rule order_trans[where y="2 ^ (len_of TYPE('a) - 1)"])
+    apply (rule order_trans[where y="2 ^ (LENGTH('a) - 1)"])
      apply (simp add: power_Suc[symmetric])
     apply (simp add: linorder_not_less[symmetric] mask_eq_iff[symmetric])
     apply (rule notI, drule word_eqD[where x="size x - 1"])