# HG changeset patch
# User wenzelm
# Date 1489944512 -3600
# Node ID 2510b0ce28da384e04c7e57fac0fbd049491bbfc
# Parent  e886aed88b2cc1c3f947418f557c8fa9b19ddcfc
misc tuning and modernization;

diff -r e886aed88b2c -r 2510b0ce28da src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Sun Mar 19 14:50:37 2017 +0100
+++ b/src/HOL/Word/Word.thy	Sun Mar 19 18:28:32 2017 +0100
@@ -276,11 +276,9 @@
 lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "op *"
   by (auto simp add: bintrunc_mod2p intro: mod_mult_cong)
 
-definition
-  word_div_def: "a div b = word_of_int (uint a div uint b)"
-
-definition
-  word_mod_def: "a mod b = word_of_int (uint a mod uint b)"
+definition word_div_def: "a div b = word_of_int (uint a div uint b)"
+
+definition word_mod_def: "a mod b = word_of_int (uint a mod uint b)"
 
 instance
   by standard (transfer, simp add: algebra_simps)+
@@ -387,9 +385,8 @@
   where "shiftl1 w = word_of_int (uint w BIT False)"
 
 definition shiftr1 :: "'a word \<Rightarrow> 'a word"
-where
   \<comment> "shift right as unsigned or as signed, ie logical or arithmetic"
-  "shiftr1 w = word_of_int (bin_rest (uint w))"
+  where "shiftr1 w = word_of_int (bin_rest (uint w))"
 
 definition shiftl_def: "w << n = (shiftl1 ^^ n) w"
 
@@ -482,7 +479,8 @@
 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))"
 
-definition max_word :: "'a::len word"  \<comment> "Largest representable machine integer."
+definition max_word :: "'a::len word"
+  \<comment> "Largest representable machine integer."
   where "max_word = word_of_int (2 ^ len_of TYPE('a) - 1)"
 
 lemmas of_nth_def = word_set_bits_def (* FIXME duplicate *)
@@ -493,7 +491,8 @@
 lemma sint_sbintrunc': "sint (word_of_int bin :: 'a word) = sbintrunc (len_of TYPE('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 :: 'a::len word))"
+lemma uint_sint: "uint w = bintrunc (len_of TYPE('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"
@@ -603,7 +602,8 @@
   "unat (- numeral bin :: 'a::len0 word) = nat (bintrunc (len_of TYPE('a)) (- numeral bin))"
   by (simp only: unat_def uint_bintrunc_neg)
 
-lemma size_0_eq: "size (w :: 'a::len0 word) = 0 \<Longrightarrow> v = w"
+lemma size_0_eq: "size w = 0 \<Longrightarrow> v = w"
+  for v w :: "'a::len0 word"
   apply (unfold word_size)
   apply (rule word_uint.Rep_eqD)
   apply (rule box_equals)
@@ -758,7 +758,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)"
+  "len_of TYPE('a) \<le> n \<Longrightarrow>
+    bin_nth (sint w) n = bin_nth (sint w) (len_of TYPE('a) - 1)"
   for w :: "'a::len word"
   apply (subst word_sbin.norm_Rep [symmetric])
   apply (auto simp add: nth_sbintr)
@@ -829,7 +830,8 @@
 
 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)"
-  by (auto simp add: of_bl_def word_test_bit_def word_size word_ubin.eq_norm nth_bintr bin_nth_of_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))"
   by (simp add: of_bl_def)
@@ -919,7 +921,8 @@
 (* for literal u(s)cast *)
 
 lemma ucast_bintr [simp]:
-  "ucast (numeral w ::'a::len0 word) =  word_of_int (bintrunc (len_of TYPE('a)) (numeral w))"
+  "ucast (numeral w :: 'a::len0 word) =
+    word_of_int (bintrunc (len_of TYPE('a)) (numeral w))"
   by (simp add: ucast_def)
 
 (* TODO: neg_numeral *)
@@ -1252,35 +1255,34 @@
 
 subsection \<open>Order on fixed-length words\<close>
 
-lemma word_zero_le [simp] :
-  "0 <= (y :: 'a::len0 word)"
+lemma word_zero_le [simp]: "0 \<le> y"
+  for y :: "'a::len0 word"
   unfolding word_le_def by auto
 
-lemma word_m1_ge [simp] : "word_pred 0 >= y" (* FIXME: delete *)
-  unfolding word_le_def
-  by (simp only : word_pred_0_n1 word_uint.eq_norm m1mod2k) auto
-
-lemma word_n1_ge [simp]: "y \<le> (-1::'a::len0 word)"
-  unfolding word_le_def
-  by (simp only: word_m1_wi word_uint.eq_norm m1mod2k) auto
+lemma word_m1_ge [simp] : "word_pred 0 \<ge> y" (* FIXME: delete *)
+  by (simp only: word_le_def word_pred_0_n1 word_uint.eq_norm m1mod2k) auto
+
+lemma word_n1_ge [simp]: "y \<le> -1"
+  for y :: "'a::len0 word"
+  by (simp only: word_le_def word_m1_wi word_uint.eq_norm m1mod2k) auto
 
 lemmas word_not_simps [simp] =
   word_zero_le [THEN leD] word_m1_ge [THEN leD] word_n1_ge [THEN leD]
 
-lemma word_gt_0: "0 < y \<longleftrightarrow> 0 \<noteq> (y :: 'a::len0 word)"
+lemma word_gt_0: "0 < y \<longleftrightarrow> 0 \<noteq> y"
+  for y :: "'a::len0 word"
   by (simp add: less_le)
 
 lemmas word_gt_0_no [simp] = word_gt_0 [of "numeral y"] for y
 
-lemma word_sless_alt: "(a <s b) = (sint a < sint b)"
-  unfolding word_sle_def word_sless_def
-  by (auto simp add: less_le)
-
-lemma word_le_nat_alt: "(a <= b) = (unat a <= unat b)"
+lemma word_sless_alt: "a <s b \<longleftrightarrow> sint a < sint b"
+  by (auto simp add: word_sle_def word_sless_def less_le)
+
+lemma word_le_nat_alt: "a \<le> b \<longleftrightarrow> unat a \<le> unat b"
   unfolding unat_def word_le_def
   by (rule nat_le_eq_zle [symmetric]) simp
 
-lemma word_less_nat_alt: "(a < b) = (unat a < unat b)"
+lemma word_less_nat_alt: "a < b \<longleftrightarrow> unat a < unat b"
   unfolding unat_def word_less_alt
   by (rule nat_less_eq_zless [symmetric]) simp
 
@@ -1290,15 +1292,15 @@
   unfolding word_less_alt by (simp add: word_uint.eq_norm)
 
 lemma wi_le:
-  "(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))"
+  "(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))"
   unfolding word_le_def by (simp add: word_uint.eq_norm)
 
-lemma udvd_nat_alt: "a udvd b = (EX n>=0. unat b = n * unat a)"
+lemma udvd_nat_alt: "a udvd b \<longleftrightarrow> (\<exists>n\<ge>0. unat b = n * unat a)"
   apply (unfold udvd_def)
   apply safe
    apply (simp add: unat_def nat_mult_distrib)
-  apply (simp add: uint_nat of_nat_mult)
+  apply (simp add: uint_nat)
   apply (rule exI)
   apply safe
    prefer 2
@@ -1317,9 +1319,12 @@
   shows "unat (w - 1) = unat w - 1"
 proof -
   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)" by arith
+  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)"
+    by arith
   with \<open>1 \<le> uint w\<close> have "(uint w - 1) mod 2 ^ len_of TYPE('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"
@@ -1328,15 +1333,14 @@
     by (simp only: unat_def int_word_uint word_arith_wis mod_diff_right_eq)
 qed
 
-lemma measure_unat: "p ~= 0 \<Longrightarrow> unat (p - 1) < unat p"
+lemma measure_unat: "p \<noteq> 0 \<Longrightarrow> unat (p - 1) < unat p"
   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 :: 'a::len0 word) - uint (y :: 'b::len0 word) <
-    2 ^ len_of TYPE('a)"
+lemma uint_sub_lt2p [simp]: "uint x - uint y < 2 ^ len_of TYPE('a)"
+  for x :: "'a::len0 word" and y :: "'b::len0 word"
   using uint_ge_0 [of y] uint_lt2p [of x] by arith
 
 
@@ -1344,72 +1348,75 @@
 
 lemma uint_add_lem:
   "(uint x + uint y < 2 ^ len_of TYPE('a)) =
-    (uint (x + y :: 'a::len0 word) = uint x + uint y)"
+    (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 * y :: 'a::len0 word) = uint x * uint y)"
-  by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])
-
-lemma uint_sub_lem:
-  "(uint x >= uint y) = (uint (x - y) = uint x - uint y)"
+    (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_add_le: "uint (x + y) <= uint x + uint y"
+lemma uint_sub_lem: "uint x \<ge> uint y \<longleftrightarrow> uint (x - y) = uint x - uint y"
+  by (auto simp: uint_word_ariths intro!: trans [OF _ int_mod_lem])
+
+lemma uint_add_le: "uint (x + y) \<le> uint x + uint y"
   unfolding uint_word_ariths by (metis uint_add_ge0 zmod_le_nonneg_dividend)
 
-lemma uint_sub_ge: "uint (x - y) >= uint x - uint y"
+lemma uint_sub_ge: "uint (x - y) \<ge> uint x - uint y"
   unfolding uint_word_ariths by (metis int_mod_ge uint_sub_lt2p zless2p)
 
 lemma mod_add_if_z:
-  "(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==>
-   (x + y) mod z = (if x + y < z then x + y else x + y - z)"
+  "x < z \<Longrightarrow> y < z \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> z \<Longrightarrow>
+    (x + y) mod z = (if x + y < z then x + y else x + y - z)"
+  for x y z :: int
   by (auto intro: int_mod_eq)
 
 lemma uint_plus_if':
-  "uint ((a::'a word) + b) =
-  (if uint a + uint b < 2 ^ len_of TYPE('a::len0) then uint a + uint b
-   else uint a + uint b - 2 ^ len_of TYPE('a))"
+  "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))"
+  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 :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==>
-   (x - y) mod z = (if y <= x then x - y else x - y + z)"
+  "x < z \<Longrightarrow> y < z \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> z \<Longrightarrow>
+    (x - y) mod z = (if y \<le> x then x - y else x - y + z)"
+  for x y z :: int
   by (auto intro: int_mod_eq)
 
 lemma uint_sub_if':
-  "uint ((a::'a word) - b) =
-  (if uint b \<le> uint a then uint a - uint b
-   else uint a - uint b + 2 ^ len_of TYPE('a::len0))"
+  "uint (a - b) =
+    (if uint b \<le> uint a then uint a - uint b
+     else uint a - uint b + 2 ^ len_of TYPE('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 <= r \<Longrightarrow> r < 2 ^ len_of TYPE('a) \<Longrightarrow>
-   uint (a::'a::len0 word) = r"
+  "word_of_int r = a \<Longrightarrow> 0 \<le> r \<Longrightarrow> r < 2 ^ len_of TYPE('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:
-  fixes x::"'a::len0 word"
-  shows "P (uint x) =
-         (ALL i. word_of_int i = x & 0 <= i & i < 2^len_of TYPE('a) --> P i)"
+  "P (uint x) = (\<forall>i. word_of_int i = x \<and> 0 \<le> i \<and> i < 2^len_of TYPE('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)
+      split: word_int_split)
   done
 
 lemma uint_split_asm:
-  fixes x::"'a::len0 word"
-  shows "P (uint x) =
-         (~(EX i. word_of_int i = x & 0 <= i & i < 2^len_of TYPE('a) & ~ P i))"
+  "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)"
+  for x :: "'a::len0 word"
   by (auto dest!: word_of_int_inverse
-           simp: int_word_uint mod_pos_pos_trivial
-           split: uint_split)
+      simp: int_word_uint mod_pos_pos_trivial
+      split: uint_split)
 
 lemmas uint_splits = uint_split uint_split_asm
 
@@ -1461,18 +1468,18 @@
 
 subsection \<open>More on overflows and monotonicity\<close>
 
-lemma no_plus_overflow_uint_size:
-  "((x :: 'a::len0 word) <= x + y) = (uint x + uint y < 2 ^ size x)"
+lemma no_plus_overflow_uint_size: "x \<le> x + y \<longleftrightarrow> uint x + uint y < 2 ^ size x"
+  for x y :: "'a::len0 word"
   unfolding word_size by uint_arith
 
 lemmas no_olen_add = no_plus_overflow_uint_size [unfolded word_size]
 
-lemma no_ulen_sub: "((x :: 'a::len0 word) >= x - y) = (uint y <= uint x)"
+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':
-  fixes x :: "'a::len0 word"
-  shows "(x \<le> y + x) = (uint y + uint x < 2 ^ len_of TYPE('a))"
+lemma no_olen_add': "x \<le> y + x \<longleftrightarrow> uint y + uint x < 2 ^ len_of TYPE('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]]
@@ -1484,120 +1491,118 @@
 lemmas word_sub_le_iff = no_ulen_sub [folded word_le_def]
 lemmas word_sub_le = word_sub_le_iff [THEN iffD2]
 
-lemma word_less_sub1:
-  "(x :: 'a::len word) ~= 0 \<Longrightarrow> (1 < x) = (0 < x - 1)"
+lemma word_less_sub1: "x \<noteq> 0 \<Longrightarrow> 1 < x \<longleftrightarrow> 0 < x - 1"
+  for x :: "'a::len word"
   by uint_arith
 
-lemma word_le_sub1:
-  "(x :: 'a::len word) ~= 0 \<Longrightarrow> (1 <= x) = (0 <= x - 1)"
+lemma word_le_sub1: "x \<noteq> 0 \<Longrightarrow> 1 \<le> x \<longleftrightarrow> 0 \<le> x - 1"
+  for x :: "'a::len word"
   by uint_arith
 
-lemma sub_wrap_lt:
-  "((x :: 'a::len0 word) < x - z) = (x < z)"
+lemma sub_wrap_lt: "x < x - z \<longleftrightarrow> x < z"
+  for x z :: "'a::len0 word"
   by uint_arith
 
-lemma sub_wrap:
-  "((x :: 'a::len0 word) <= x - z) = (z = 0 | x < z)"
+lemma sub_wrap: "x \<le> x - z \<longleftrightarrow> z = 0 \<or> x < z"
+  for x z :: "'a::len0 word"
   by uint_arith
 
-lemma plus_minus_not_NULL_ab:
-  "(x :: 'a::len0 word) <= ab - c \<Longrightarrow> c <= ab \<Longrightarrow> c ~= 0 \<Longrightarrow> x + c ~= 0"
+lemma plus_minus_not_NULL_ab: "x \<le> ab - c \<Longrightarrow> c \<le> ab \<Longrightarrow> c \<noteq> 0 \<Longrightarrow> x + c \<noteq> 0"
+  for x ab c :: "'a::len0 word"
   by uint_arith
 
-lemma plus_minus_no_overflow_ab:
-  "(x :: 'a::len0 word) <= ab - c \<Longrightarrow> c <= ab \<Longrightarrow> x <= x + c"
+lemma plus_minus_no_overflow_ab: "x \<le> ab - c \<Longrightarrow> c \<le> ab \<Longrightarrow> x \<le> x + c"
+  for x ab c :: "'a::len0 word"
   by uint_arith
 
-lemma le_minus':
-  "(a :: 'a::len0 word) + c <= b \<Longrightarrow> a <= a + c \<Longrightarrow> c <= b - a"
+lemma le_minus': "a + c \<le> b \<Longrightarrow> a \<le> a + c \<Longrightarrow> c \<le> b - a"
+  for a b c :: "'a::len0 word"
   by uint_arith
 
-lemma le_plus':
-  "(a :: 'a::len0 word) <= b \<Longrightarrow> c <= b - a \<Longrightarrow> a + c <= b"
+lemma le_plus': "a \<le> b \<Longrightarrow> c \<le> b - a \<Longrightarrow> a + c \<le> b"
+  for a b c :: "'a::len0 word"
   by uint_arith
 
 lemmas le_plus = le_plus' [rotated]
 
 lemmas le_minus = leD [THEN thin_rl, THEN le_minus'] (* FIXME *)
 
-lemma word_plus_mono_right:
-  "(y :: 'a::len0 word) <= z \<Longrightarrow> x <= x + z \<Longrightarrow> x + y <= x + z"
+lemma word_plus_mono_right: "y \<le> z \<Longrightarrow> x \<le> x + z \<Longrightarrow> x + y \<le> x + z"
+  for x y z :: "'a::len0 word"
   by uint_arith
 
-lemma word_less_minus_cancel:
-  "y - x < z - x \<Longrightarrow> x <= z \<Longrightarrow> (y :: 'a::len0 word) < z"
+lemma word_less_minus_cancel: "y - x < z - x \<Longrightarrow> x \<le> z \<Longrightarrow> y < z"
+  for x y z :: "'a::len0 word"
   by uint_arith
 
-lemma word_less_minus_mono_left:
-  "(y :: 'a::len0 word) < z \<Longrightarrow> x <= y \<Longrightarrow> y - x < z - x"
+lemma word_less_minus_mono_left: "y < z \<Longrightarrow> x \<le> y \<Longrightarrow> y - x < z - x"
+  for x y z :: "'a::len0 word"
   by uint_arith
 
-lemma word_less_minus_mono:
-  "a < c \<Longrightarrow> d < b \<Longrightarrow> a - b < a \<Longrightarrow> c - d < c
-  \<Longrightarrow> a - b < c - (d::'a::len word)"
+lemma word_less_minus_mono: "a < c \<Longrightarrow> d < b \<Longrightarrow> a - b < a \<Longrightarrow> c - d < c \<Longrightarrow> a - b < c - d"
+  for a b c d :: "'a::len word"
   by uint_arith
 
-lemma word_le_minus_cancel:
-  "y - x <= z - x \<Longrightarrow> x <= z \<Longrightarrow> (y :: 'a::len0 word) <= z"
+lemma word_le_minus_cancel: "y - x \<le> z - x \<Longrightarrow> x \<le> z \<Longrightarrow> y \<le> z"
+  for x y z :: "'a::len0 word"
   by uint_arith
 
-lemma word_le_minus_mono_left:
-  "(y :: 'a::len0 word) <= z \<Longrightarrow> x <= y \<Longrightarrow> y - x <= z - x"
+lemma word_le_minus_mono_left: "y \<le> z \<Longrightarrow> x \<le> y \<Longrightarrow> y - x \<le> z - x"
+  for x y z :: "'a::len0 word"
   by uint_arith
 
 lemma word_le_minus_mono:
-  "a <= c \<Longrightarrow> d <= b \<Longrightarrow> a - b <= a \<Longrightarrow> c - d <= c
-  \<Longrightarrow> a - b <= c - (d::'a::len word)"
+  "a \<le> c \<Longrightarrow> d \<le> b \<Longrightarrow> a - b \<le> a \<Longrightarrow> c - d \<le> c \<Longrightarrow> a - b \<le> c - d"
+  for a b c d :: "'a::len word"
   by uint_arith
 
-lemma plus_le_left_cancel_wrap:
-  "(x :: 'a::len0 word) + y' < x \<Longrightarrow> x + y < x \<Longrightarrow> (x + y' < x + y) = (y' < y)"
+lemma plus_le_left_cancel_wrap: "x + y' < x \<Longrightarrow> x + y < x \<Longrightarrow> x + y' < x + y \<longleftrightarrow> y' < y"
+  for x y y' :: "'a::len0 word"
   by uint_arith
 
-lemma plus_le_left_cancel_nowrap:
-  "(x :: 'a::len0 word) <= x + y' \<Longrightarrow> x <= x + y \<Longrightarrow>
-    (x + y' < x + y) = (y' < y)"
+lemma plus_le_left_cancel_nowrap: "x \<le> x + y' \<Longrightarrow> x \<le> x + y \<Longrightarrow> x + y' < x + y \<longleftrightarrow> y' < y"
+  for x y y' :: "'a::len0 word"
   by uint_arith
 
-lemma word_plus_mono_right2:
-  "(a :: 'a::len0 word) <= a + b \<Longrightarrow> c <= b \<Longrightarrow> a <= a + c"
+lemma word_plus_mono_right2: "a \<le> a + b \<Longrightarrow> c \<le> b \<Longrightarrow> a \<le> a + c"
+  for a b c :: "'a::len0 word"
+  by uint_arith
+
+lemma word_less_add_right: "x < y - z \<Longrightarrow> z \<le> y \<Longrightarrow> x + z < y"
+  for x y z :: "'a::len0 word"
   by uint_arith
 
-lemma word_less_add_right:
-  "(x :: 'a::len0 word) < y - z \<Longrightarrow> z <= y \<Longrightarrow> x + z < y"
+lemma word_less_sub_right: "x < y + z \<Longrightarrow> y \<le> x \<Longrightarrow> x - y < z"
+  for x y z :: "'a::len0 word"
   by uint_arith
 
-lemma word_less_sub_right:
-  "(x :: 'a::len0 word) < y + z \<Longrightarrow> y <= x \<Longrightarrow> x - y < z"
-  by uint_arith
-
-lemma word_le_plus_either:
-  "(x :: 'a::len0 word) <= y | x <= z \<Longrightarrow> y <= y + z \<Longrightarrow> x <= y + z"
+lemma word_le_plus_either: "x \<le> y \<or> x \<le> z \<Longrightarrow> y \<le> y + z \<Longrightarrow> x \<le> y + z"
+  for x y z :: "'a::len0 word"
   by uint_arith
 
-lemma word_less_nowrapI:
-  "(x :: 'a::len0 word) < z - k \<Longrightarrow> k <= z \<Longrightarrow> 0 < k \<Longrightarrow> x < x + k"
+lemma word_less_nowrapI: "x < z - k \<Longrightarrow> k \<le> z \<Longrightarrow> 0 < k \<Longrightarrow> x < x + k"
+  for x z k :: "'a::len0 word"
   by uint_arith
 
-lemma inc_le: "(i :: 'a::len word) < m \<Longrightarrow> i + 1 <= m"
+lemma inc_le: "i < m \<Longrightarrow> i + 1 \<le> m"
+  for i m :: "'a::len word"
   by uint_arith
 
-lemma inc_i:
-  "(1 :: 'a::len word) <= i \<Longrightarrow> i < m \<Longrightarrow> 1 <= (i + 1) & i + 1 <= m"
+lemma inc_i: "1 \<le> i \<Longrightarrow> i < m \<Longrightarrow> 1 \<le> i + 1 \<and> i + 1 \<le> m"
+  for i m :: "'a::len word"
   by uint_arith
 
 lemma udvd_incr_lem:
   "up < uq \<Longrightarrow> up = ua + n * uint K \<Longrightarrow>
-    uq = ua + n' * uint K \<Longrightarrow> up + uint K <= uq"
+    uq = ua + n' * uint K \<Longrightarrow> up + uint K \<le> uq"
   apply clarsimp
-
   apply (drule less_le_mult)
-  apply safe
+   apply safe
   done
 
 lemma udvd_incr':
   "p < q \<Longrightarrow> uint p = ua + n * uint K \<Longrightarrow>
-    uint q = ua + n' * uint K \<Longrightarrow> p + K <= q"
+    uint q = ua + n' * uint K \<Longrightarrow> p + K \<le> q"
   apply (unfold word_less_alt word_le_def)
   apply (drule (2) udvd_incr_lem)
   apply (erule uint_add_le [THEN order_trans])
@@ -1605,7 +1610,7 @@
 
 lemma udvd_decr':
   "p < q \<Longrightarrow> uint p = ua + n * uint K \<Longrightarrow>
-    uint q = ua + n' * uint K \<Longrightarrow> p <= q - K"
+    uint q = ua + n' * uint K \<Longrightarrow> p \<le> q - K"
   apply (unfold word_less_alt word_le_def)
   apply (drule (2) udvd_incr_lem)
   apply (drule le_diff_eq [THEN iffD2])
@@ -1617,17 +1622,16 @@
 lemmas udvd_incr0 = udvd_incr' [where ua=0, unfolded add_0_left]
 lemmas udvd_decr0 = udvd_decr' [where ua=0, unfolded add_0_left]
 
-lemma udvd_minus_le':
-  "xy < k \<Longrightarrow> z udvd xy \<Longrightarrow> z udvd k \<Longrightarrow> xy <= k - z"
+lemma udvd_minus_le': "xy < k \<Longrightarrow> z udvd xy \<Longrightarrow> z udvd k \<Longrightarrow> xy \<le> k - z"
   apply (unfold udvd_def)
   apply clarify
   apply (erule (2) udvd_decr0)
   done
 
 lemma udvd_incr2_K:
-  "p < a + s \<Longrightarrow> a <= a + s \<Longrightarrow> K udvd s \<Longrightarrow> K udvd p - a \<Longrightarrow> a <= p \<Longrightarrow>
-    0 < K \<Longrightarrow> p <= p + K & p + K <= a + s"
-  using [[simproc del: linordered_ring_less_cancel_factor]]
+  "p < a + s \<Longrightarrow> a \<le> a + s \<Longrightarrow> K udvd s \<Longrightarrow> K udvd p - a \<Longrightarrow> a \<le> p \<Longrightarrow>
+    0 < K \<Longrightarrow> p \<le> p + K \<and> p + K \<le> a + s"
+  supply [[simproc del: linordered_ring_less_cancel_factor]]
   apply (unfold udvd_def)
   apply clarify
   apply (simp add: uint_arith_simps split: if_split_asm)
@@ -1642,16 +1646,14 @@
   done
 
 (* links with rbl operations *)
-lemma word_succ_rbl:
-  "to_bl w = bl \<Longrightarrow> to_bl (word_succ w) = (rev (rbl_succ (rev bl)))"
+lemma word_succ_rbl: "to_bl w = bl \<Longrightarrow> to_bl (word_succ w) = rev (rbl_succ (rev bl))"
   apply (unfold word_succ_def)
   apply clarify
   apply (simp add: to_bl_of_bin)
   apply (simp add: to_bl_def rbl_succ)
   done
 
-lemma word_pred_rbl:
-  "to_bl w = bl \<Longrightarrow> to_bl (word_pred w) = (rev (rbl_pred (rev bl)))"
+lemma word_pred_rbl: "to_bl w = bl \<Longrightarrow> to_bl (word_pred w) = rev (rbl_pred (rev bl))"
   apply (unfold word_pred_def)
   apply clarify
   apply (simp add: to_bl_of_bin)
@@ -1660,7 +1662,7 @@
 
 lemma word_add_rbl:
   "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow>
-    to_bl (v + w) = (rev (rbl_add (rev vbl) (rev wbl)))"
+    to_bl (v + w) = rev (rbl_add (rev vbl) (rev wbl))"
   apply (unfold word_add_def)
   apply clarify
   apply (simp add: to_bl_of_bin)
@@ -1669,7 +1671,7 @@
 
 lemma word_mult_rbl:
   "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow>
-    to_bl (v * w) = (rev (rbl_mult (rev vbl) (rev wbl)))"
+    to_bl (v * w) = rev (rbl_mult (rev vbl) (rev wbl))"
   apply (unfold word_mult_def)
   apply clarify
   apply (simp add: to_bl_of_bin)
@@ -1681,8 +1683,7 @@
   "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_pred w)) = rbl_pred ys"
   "rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v * w)) = rbl_mult ys xs"
   "rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v + w)) = rbl_add ys xs"
-  by (auto simp: rev_swap [symmetric] word_succ_rbl
-                 word_pred_rbl word_mult_rbl word_add_rbl)
+  by (auto simp: rev_swap [symmetric] word_succ_rbl word_pred_rbl word_mult_rbl word_add_rbl)
 
 
 subsection \<open>Arithmetic type class instantiations\<close>
@@ -1690,9 +1691,8 @@
 lemmas word_le_0_iff [simp] =
   word_zero_le [THEN leD, THEN linorder_antisym_conv1]
 
-lemma word_of_int_nat:
-  "0 <= x \<Longrightarrow> word_of_int x = of_nat (nat x)"
-  by (simp add: of_nat_nat word_of_int)
+lemma word_of_int_nat: "0 \<le> x \<Longrightarrow> word_of_int x = of_nat (nat x)"
+  by (simp add: word_of_int)
 
 (* note that iszero_def is only for class comm_semiring_1_cancel,
    which requires word length >= 1, ie 'a::len word *)
@@ -1712,44 +1712,43 @@
 
 lemma td_ext_unat [OF refl]:
   "n = len_of TYPE('a::len) \<Longrightarrow>
-    td_ext (unat :: 'a word => nat) of_nat
-    (unats n) (%i. i mod 2 ^ n)"
+    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 (erule word_uint.Abs_inverse [THEN arg_cong])
   apply (simp add: int_word_uint nat_mod_distrib nat_power_eq)
   done
 
 lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm]
 
 interpretation word_unat:
-  td_ext "unat::'a::len word => nat"
-         of_nat
-         "unats (len_of TYPE('a::len))"
-         "%i. i mod 2 ^ len_of TYPE('a::len)"
+  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)"
   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 <= unat (z :: 'a::len word) \<Longrightarrow> y : unats (len_of TYPE('a))"
+lemma unat_le: "y \<le> unat z \<Longrightarrow> y \<in> unats (len_of TYPE('a))"
+  for z :: "'a::len word"
   apply (unfold unats_def)
   apply clarsimp
   apply (rule xtrans, rule unat_lt2p, assumption)
   done
 
-lemma word_nchotomy:
-  "ALL w. EX n. (w :: 'a::len word) = of_nat n & n < 2 ^ len_of TYPE('a)"
+lemma word_nchotomy: "\<forall>w :: 'a::len word. \<exists>n. w = of_nat n \<and> n < 2 ^ len_of TYPE('a)"
   apply (rule allI)
   apply (rule word_unat.Abs_cases)
   apply (unfold unats_def)
   apply auto
   done
 
-lemma of_nat_eq:
-  fixes w :: "'a::len word"
-  shows "(of_nat n = w) = (\<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 ^ len_of TYPE('a))"
+  for w :: "'a::len word"
   apply (rule trans)
    apply (rule word_unat.inverse_norm)
   apply (rule iffI)
@@ -1758,35 +1757,28 @@
   apply clarsimp
   done
 
-lemma of_nat_eq_size:
-  "(of_nat n = w) = (EX q. n = unat w + q * 2 ^ size w)"
+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)) = (\<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 ^ len_of TYPE('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 ^ len_of TYPE('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 ~= 0 \<Longrightarrow> 0 < k"
+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 ~= (0 :: 'a word)"
-  by (clarsimp simp add : of_nat_0)
-
-lemma Abs_fnat_hom_add:
-  "of_nat a + of_nat b = of_nat (a + b)"
+lemma of_nat_neq_0: "0 < k \<Longrightarrow> k < 2 ^ len_of TYPE('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
 
-lemma Abs_fnat_hom_mult:
-  "of_nat a * of_nat b = (of_nat (a * b) :: 'a::len word)"
+lemma Abs_fnat_hom_mult: "of_nat a * of_nat b = (of_nat (a * b) :: 'a::len word)"
   by (simp add: word_of_nat wi_hom_mult)
 
-lemma Abs_fnat_hom_Suc:
-  "word_succ (of_nat a) = of_nat (Suc a)"
+lemma Abs_fnat_hom_Suc: "word_succ (of_nat a) = of_nat (Suc a)"
   by (simp add: word_of_nat wi_hom_succ ac_simps)
 
 lemma Abs_fnat_hom_0: "(0::'a::len word) = of_nat 0"
@@ -1799,24 +1791,19 @@
   Abs_fnat_hom_add Abs_fnat_hom_mult Abs_fnat_hom_Suc
   Abs_fnat_hom_0 Abs_fnat_hom_1
 
-lemma word_arith_nat_add:
-  "a + b = of_nat (unat a + unat b)"
+lemma word_arith_nat_add: "a + b = of_nat (unat a + unat b)"
+  by simp
+
+lemma word_arith_nat_mult: "a * b = of_nat (unat a * unat b)"
   by simp
 
-lemma word_arith_nat_mult:
-  "a * b = of_nat (unat a * unat b)"
-  by (simp add: of_nat_mult)
-
-lemma word_arith_nat_Suc:
-  "word_succ a = of_nat (Suc (unat a))"
+lemma word_arith_nat_Suc: "word_succ a = of_nat (Suc (unat a))"
   by (subst Abs_fnat_hom_Suc [symmetric]) simp
 
-lemma word_arith_nat_div:
-  "a div b = of_nat (unat a div unat b)"
+lemma word_arith_nat_div: "a div b = of_nat (unat a div unat b)"
   by (simp add: word_div_def word_of_nat zdiv_int uint_nat)
 
-lemma word_arith_nat_mod:
-  "a mod b = of_nat (unat a mod unat b)"
+lemma word_arith_nat_mod: "a mod b = of_nat (unat a mod unat b)"
   by (simp add: word_mod_def word_of_nat zmod_int uint_nat)
 
 lemmas word_arith_nat_defs =
@@ -1835,31 +1822,32 @@
   [unfolded linorder_not_less [symmetric] Not_eq_iff]
 
 lemma unat_add_lem:
-  "(unat x + unat y < 2 ^ len_of TYPE('a)) =
-    (unat (x + y :: 'a::len word) = unat x + unat y)"
-  unfolding unat_word_ariths
-  by (auto intro!: trans [OF _ nat_mod_lem])
+  "unat x + unat y < 2 ^ len_of TYPE('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)) =
-    (unat (x * y :: 'a::len word) = unat x * unat y)"
-  unfolding unat_word_ariths
-  by (auto intro!: trans [OF _ nat_mod_lem])
-
-lemmas unat_plus_if' = trans [OF unat_word_ariths(1) mod_nat_add, simplified]
-
-lemma le_no_overflow:
-  "x <= b \<Longrightarrow> a <= a + b \<Longrightarrow> x <= a + (b :: 'a::len0 word)"
+  "unat x * unat y < 2 ^ len_of TYPE('a) \<longleftrightarrow>
+    unat (x * y :: 'a::len word) = unat x * unat y"
+  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]
+
+lemma le_no_overflow: "x \<le> b \<Longrightarrow> a \<le> a + b \<Longrightarrow> x \<le> a + b"
+  for a b x :: "'a::len0 word"
   apply (erule order_trans)
   apply (erule olen_add_eqv [THEN iffD1])
   done
 
-lemmas un_ui_le = trans [OF word_le_nat_alt [symmetric] word_le_def]
+lemmas un_ui_le =
+  trans [OF word_le_nat_alt [symmetric] word_le_def]
 
 lemma unat_sub_if_size:
-  "unat (x - y) = (if unat y <= unat x
-   then unat x - unat y
-   else unat x + 2 ^ size x - unat y)"
+  "unat (x - y) =
+    (if unat y \<le> unat x
+     then unat x - unat y
+     else unat x + 2 ^ size x - unat y)"
   apply (unfold word_size)
   apply (simp add: un_ui_le)
   apply (auto simp add: unat_def uint_sub_if')
@@ -1877,13 +1865,15 @@
 
 lemmas unat_sub_if' = unat_sub_if_size [unfolded word_size]
 
-lemma unat_div: "unat ((x :: 'a::len word) div y) = unat x div unat y"
+lemma unat_div: "unat (x div y) = unat x div unat y"
+  for x y :: " 'a::len word"
   apply (simp add : unat_word_ariths)
   apply (rule unat_lt2p [THEN xtr7, THEN nat_mod_eq'])
   apply (rule div_le_dividend)
   done
 
-lemma unat_mod: "unat ((x :: 'a::len word) mod y) = unat x mod unat y"
+lemma unat_mod: "unat (x mod y) = unat x mod unat y"
+  for x y :: "'a::len word"
   apply (clarsimp simp add : unat_word_ariths)
   apply (cases "unat y")
    prefer 2
@@ -1892,25 +1882,23 @@
    apply auto
   done
 
-lemma uint_div: "uint ((x :: 'a::len word) div y) = uint x div uint y"
-  unfolding uint_nat by (simp add : unat_div zdiv_int)
-
-lemma uint_mod: "uint ((x :: 'a::len word) mod y) = uint x mod uint y"
-  unfolding uint_nat by (simp add : unat_mod zmod_int)
+lemma uint_div: "uint (x div y) = uint x div uint y"
+  for x y :: "'a::len word"
+  by (simp add: uint_nat unat_div zdiv_int)
+
+lemma uint_mod: "uint (x mod y) = uint x mod uint y"
+  for x y :: "'a::len word"
+  by (simp add: uint_nat unat_mod zmod_int)
 
 
 subsection \<open>Definition of \<open>unat_arith\<close> tactic\<close>
 
-lemma unat_split:
-  fixes x::"'a::len word"
-  shows "P (unat x) =
-         (ALL n. of_nat n = x & n < 2^len_of TYPE('a) --> P n)"
+lemma unat_split: "P (unat x) \<longleftrightarrow> (\<forall>n. of_nat n = x \<and> n < 2^len_of TYPE('a) \<longrightarrow> P n)"
+  for x :: "'a::len word"
   by (auto simp: unat_of_nat)
 
-lemma unat_split_asm:
-  fixes x::"'a::len word"
-  shows "P (unat x) =
-         (~(EX n. of_nat n = x & n < 2^len_of TYPE('a) & ~ P n))"
+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)"
+  for x :: "'a::len word"
   by (auto simp: unat_of_nat)
 
 lemmas of_nat_inverse =
@@ -1958,25 +1946,26 @@
   \<open>Scan.succeed (SIMPLE_METHOD' o unat_arith_tac)\<close>
   "solving word arithmetic via natural numbers and arith"
 
-lemma no_plus_overflow_unat_size:
-  "((x :: 'a::len word) <= x + y) = (unat x + unat y < 2 ^ size x)"
+lemma no_plus_overflow_unat_size: "x \<le> x + y \<longleftrightarrow> unat x + unat y < 2 ^ size x"
+  for x y :: "'a::len word"
   unfolding word_size by unat_arith
 
-lemmas no_olen_add_nat = 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 :: 'a::len word) < y \<Longrightarrow> unat x * unat y < 2 ^ len_of TYPE('a) \<Longrightarrow>
-    x * y div y = x"
+lemmas no_olen_add_nat =
+  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"
+  for x y :: "'a::len word"
   apply unat_arith
   apply clarsimp
   apply (subst unat_mult_lem [THEN iffD1])
-  apply auto
+   apply auto
   done
 
-lemma div_lt': "(i :: 'a::len word) <= 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 ^ len_of TYPE('a)"
+  for i k x :: "'a::len word"
   apply unat_arith
   apply clarsimp
   apply (drule mult_le_mono1)
@@ -1986,7 +1975,8 @@
 
 lemmas div_lt'' = order_less_imp_le [THEN div_lt']
 
-lemma div_lt_mult: "(i :: 'a::len word) < k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x < k"
+lemma div_lt_mult: "i < k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x < k"
+  for i k x :: "'a::len word"
   apply (frule div_lt'' [THEN unat_mult_lem [THEN iffD1]])
   apply (simp add: unat_arith_simps)
   apply (drule (1) mult_less_mono1)
@@ -1994,8 +1984,8 @@
   apply (rule div_mult_le)
   done
 
-lemma div_le_mult:
-  "(i :: 'a::len word) <= k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x <= k"
+lemma div_le_mult: "i \<le> k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x \<le> k"
+  for i k x :: "'a::len word"
   apply (frule div_lt' [THEN unat_mult_lem [THEN iffD1]])
   apply (simp add: unat_arith_simps)
   apply (drule mult_le_mono1)
@@ -2003,20 +1993,20 @@
   apply (rule div_mult_le)
   done
 
-lemma div_lt_uint':
-  "(i :: 'a::len word) <= 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 ^ len_of TYPE('a)"
+  for i k x :: "'a::len word"
   apply (unfold uint_nat)
   apply (drule div_lt')
-  by (metis of_nat_less_iff of_nat_mult of_nat_numeral of_nat_power)
+  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 :: 'a::len0 word) <= y \<Longrightarrow>
-    (EX z. y = x + z & 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 ^ len_of TYPE('a))"
+  for x y z :: "'a::len0 word"
   apply (rule exI)
   apply (rule conjI)
-  apply (rule zadd_diff_inverse)
+   apply (rule zadd_diff_inverse)
   apply uint_arith
   done
 
@@ -2038,8 +2028,8 @@
 
 lemmas uno_simps [THEN le_unat_uoi] = mod_le_divisor div_le_dividend dtle
 
-lemma word_mod_div_equality:
-  "(n div b) * b + (n mod b) = (n :: 'a::len word)"
+lemma word_mod_div_equality: "(n div b) * b + (n mod b) = n"
+  for n b :: "'a::len word"
   apply (unfold word_less_nat_alt word_arith_nat_defs)
   apply (cut_tac y="unat b" in gt_or_eq_0)
   apply (erule disjE)
@@ -2047,7 +2037,8 @@
   apply simp
   done
 
-lemma word_div_mult_le: "a div b * b <= (a::'a::len word)"
+lemma word_div_mult_le: "a div b * b \<le> a"
+  for a b :: "'a::len word"
   apply (unfold word_le_nat_alt word_arith_nat_defs)
   apply (cut_tac y="unat b" in gt_or_eq_0)
   apply (erule disjE)
@@ -2055,17 +2046,16 @@
   apply simp
   done
 
-lemma word_mod_less_divisor: "0 < n \<Longrightarrow> m mod n < (n :: 'a::len word)"
+lemma word_mod_less_divisor: "0 < n \<Longrightarrow> m mod n < n"
+  for m n :: "'a::len word"
   apply (simp only: word_less_nat_alt word_arith_nat_defs)
-  apply (clarsimp simp add : uno_simps)
+  apply (auto simp: uno_simps)
   done
 
-lemma word_of_int_power_hom:
-  "word_of_int a ^ n = (word_of_int (a ^ n) :: 'a::len word)"
+lemma word_of_int_power_hom: "word_of_int a ^ n = (word_of_int (a ^ n) :: 'a::len word)"
   by (induct n) (simp_all add: wi_hom_mult [symmetric])
 
-lemma word_arith_power_alt:
-  "a ^ n = (word_of_int (uint a ^ n) :: 'a::len word)"
+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:
@@ -2073,7 +2063,7 @@
   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)
+      del: word_of_int_numeral)
   apply (simp add: mod_pos_pos_trivial)
   apply (subst mod_pos_pos_trivial)
     apply (rule bl_to_bin_ge0)
@@ -2092,9 +2082,9 @@
 lemma card_word: "CARD('a::len0 word) = 2 ^ len_of TYPE('a)"
   by (simp add: type_definition.card [OF type_definition_word] nat_power_eq)
 
-lemma card_word_size:
-  "card (UNIV :: 'a::len0 word set) = (2 ^ size (x :: 'a word))"
-unfolding word_size by (rule card_word)
+lemma card_word_size: "card (UNIV :: 'a word set) = (2 ^ size x)"
+  for x :: "'a::len0 word"
+  unfolding word_size by (rule card_word)
 
 
 subsection \<open>Bitwise Operations on Words\<close>
@@ -2166,16 +2156,15 @@
   "x XOR (-1::'a::len0 word) = NOT x"
   by (transfer, simp)+
 
-lemma uint_or: "uint (x OR y) = (uint x) OR (uint y)"
+lemma uint_or: "uint (x OR y) = uint x OR uint y"
   by (transfer, simp add: bin_trunc_ao)
 
-lemma uint_and: "uint (x AND y) = (uint x) AND (uint y)"
+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"
-  unfolding word_test_bit_def
-  by (simp add: word_ubin.eq_norm nth_bintr)
+  "(word_of_int x :: 'a::len0 word) !! n \<longleftrightarrow> n < len_of TYPE('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 op = op =))
@@ -2183,17 +2172,18 @@
   unfolding rel_fun_def word.pcr_cr_eq cr_word_def by simp
 
 lemma word_ops_nth_size:
-  "n < size (x::'a::len0 word) \<Longrightarrow>
-    (x OR y) !! n = (x !! n | y !! n) &
-    (x AND y) !! n = (x !! n & y !! n) &
-    (x XOR y) !! n = (x !! n ~= y !! n) &
-    (NOT x) !! n = (~ x !! n)"
+  "n < size x \<Longrightarrow>
+    (x OR y) !! n = (x !! n | y !! n) \<and>
+    (x AND y) !! n = (x !! n \<and> y !! n) \<and>
+    (x XOR y) !! n = (x !! n \<noteq> y !! n) \<and>
+    (NOT x) !! n = (\<not> x !! n)"
+  for x :: "'a::len0 word"
   unfolding word_size by transfer (simp add: bin_nth_ops)
 
 lemma word_ao_nth:
-  fixes x :: "'a::len0 word"
-  shows "(x OR y) !! n = (x !! n | y !! n) &
-         (x AND y) !! n = (x !! n & y !! n)"
+  "(x OR y) !! n = (x !! n | y !! n) \<and>
+    (x AND y) !! n = (x !! n \<and> y !! n)"
+  for x :: "'a::len0 word"
   by transfer (auto simp add: bin_nth_ops)
 
 lemma test_bit_numeral [simp]:
@@ -2206,13 +2196,13 @@
     n < len_of TYPE('a) \<and> bin_nth (- numeral w) n"
   by transfer (rule refl)
 
-lemma test_bit_1 [simp]: "(1::'a::len word) !! n \<longleftrightarrow> n = 0"
+lemma test_bit_1 [simp]: "(1 :: 'a::len word) !! n \<longleftrightarrow> n = 0"
   by transfer auto
 
-lemma nth_0 [simp]: "~ (0::'a::len0 word) !! n"
+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 < len_of TYPE('a)"
   by transfer simp
 
 (* get from commutativity, associativity etc of int_and etc
@@ -2223,32 +2213,27 @@
   word_wi_log_defs
 
 lemma word_bw_assocs:
-  fixes x :: "'a::len0 word"
-  shows
   "(x AND y) AND z = x AND y AND z"
   "(x OR y) OR z = x OR y OR z"
   "(x XOR y) XOR z = x XOR y XOR z"
+  for x :: "'a::len0 word"
   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
 
 lemma word_bw_comms:
-  fixes x :: "'a::len0 word"
-  shows
   "x AND y = y AND x"
   "x OR y = y OR x"
   "x XOR y = y XOR x"
+  for x :: "'a::len0 word"
   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
 
 lemma word_bw_lcs:
-  fixes x :: "'a::len0 word"
-  shows
   "y AND x AND z = x AND y AND z"
   "y OR x OR z = x OR y OR z"
   "y XOR x XOR z = x XOR y XOR z"
+  for x :: "'a::len0 word"
   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
 
 lemma word_log_esimps [simp]:
-  fixes x :: "'a::len0 word"
-  shows
   "x AND 0 = 0"
   "x AND -1 = x"
   "x OR 0 = x"
@@ -2261,26 +2246,23 @@
   "-1 OR x = -1"
   "0 XOR x = x"
   "-1 XOR x = NOT x"
+  for x :: "'a::len0 word"
   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
 
 lemma word_not_dist:
-  fixes x :: "'a::len0 word"
-  shows
   "NOT (x OR y) = NOT x AND NOT y"
   "NOT (x AND y) = NOT x OR NOT y"
+  for x :: "'a::len0 word"
   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
 
 lemma word_bw_same:
-  fixes x :: "'a::len0 word"
-  shows
   "x AND x = x"
   "x OR x = x"
   "x XOR x = 0"
+  for x :: "'a::len0 word"
   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
 
 lemma word_ao_absorbs [simp]:
-  fixes x :: "'a::len0 word"
-  shows
   "x AND (y OR x) = x"
   "x OR y AND x = x"
   "x AND (x OR y) = x"
@@ -2289,47 +2271,44 @@
   "x OR x AND y = x"
   "(x OR y) AND x = x"
   "x AND y OR x = x"
-  by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
-
-lemma word_not_not [simp]:
-  "NOT NOT (x::'a::len0 word) = x"
+  for x :: "'a::len0 word"
   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
 
-lemma word_ao_dist:
-  fixes x :: "'a::len0 word"
-  shows "(x OR y) AND z = x AND z OR y AND z"
+lemma word_not_not [simp]: "NOT NOT x = x"
+  for x :: "'a::len0 word"
   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
 
-lemma word_oa_dist:
-  fixes x :: "'a::len0 word"
-  shows "x AND y OR z = (x OR z) AND (y OR z)"
+lemma word_ao_dist: "(x OR y) AND z = x AND z OR y AND z"
+  for x :: "'a::len0 word"
   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
 
-lemma word_add_not [simp]:
-  fixes x :: "'a::len0 word"
-  shows "x + NOT x = -1"
+lemma word_oa_dist: "x AND y OR z = (x OR z) AND (y OR z)"
+  for x :: "'a::len0 word"
+  by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
+
+lemma word_add_not [simp]: "x + NOT x = -1"
+  for x :: "'a::len0 word"
   by transfer (simp add: bin_add_not)
 
-lemma word_plus_and_or [simp]:
-  fixes x :: "'a::len0 word"
-  shows "(x AND y) + (x OR y) = x + y"
+lemma word_plus_and_or [simp]: "(x AND y) + (x OR y) = x + y"
+  for x :: "'a::len0 word"
   by transfer (simp add: plus_and_or)
 
-lemma leoa:
-  fixes x :: "'a::len0 word"
-  shows "(w = (x OR y)) \<Longrightarrow> (y = (w AND y))" by auto
-lemma leao:
-  fixes x' :: "'a::len0 word"
-  shows "(w' = (x' AND y')) \<Longrightarrow> (x' = (x' OR w'))" by auto
-
-lemma word_ao_equiv:
-  fixes w w' :: "'a::len0 word"
-  shows "(w = w OR w') = (w' = w AND w')"
+lemma leoa: "w = x OR y \<Longrightarrow> y = w AND y"
+  for x :: "'a::len0 word"
+  by auto
+
+lemma leao: "w' = x' AND y' \<Longrightarrow> x' = x' OR w'"
+  for x' :: "'a::len0 word"
+  by auto
+
+lemma word_ao_equiv: "w = w OR w' \<longleftrightarrow> w' = w AND w'"
+  for w w' :: "'a::len0 word"
   by (auto intro: leoa leao)
 
-lemma le_word_or2: "x <= x OR (y::'a::len0 word)"
-  unfolding word_le_def uint_or
-  by (auto intro: le_int_or)
+lemma le_word_or2: "x \<le> x OR y"
+  for x y :: "'a::len0 word"
+  by (auto simp: word_le_def uint_or intro: le_int_or)
 
 lemmas le_word_or1 = xtr3 [OF word_bw_comms (2) le_word_or2]
 lemmas word_and_le1 = xtr3 [OF word_ao_absorbs (4) [symmetric] le_word_or2]
@@ -2339,22 +2318,22 @@
   unfolding to_bl_def word_log_defs bl_not_bin
   by (simp add: word_ubin.eq_norm)
 
-lemma bl_word_xor: "to_bl (v XOR w) = map2 op ~= (to_bl v) (to_bl w)"
+lemma bl_word_xor: "to_bl (v XOR w) = map2 op \<noteq> (to_bl v) (to_bl w)"
   unfolding to_bl_def word_log_defs bl_xor_bin
   by (simp add: word_ubin.eq_norm)
 
-lemma bl_word_or: "to_bl (v OR w) = map2 op | (to_bl v) (to_bl w)"
+lemma bl_word_or: "to_bl (v OR w) = map2 op \<or> (to_bl v) (to_bl w)"
   unfolding to_bl_def word_log_defs bl_or_bin
   by (simp add: word_ubin.eq_norm)
 
-lemma bl_word_and: "to_bl (v AND w) = map2 op & (to_bl v) (to_bl w)"
+lemma bl_word_and: "to_bl (v AND w) = map2 op \<and> (to_bl v) (to_bl w)"
   unfolding to_bl_def word_log_defs bl_and_bin
   by (simp add: word_ubin.eq_norm)
 
 lemma word_lsb_alt: "lsb (w::'a::len0 word) = test_bit w 0"
   by (auto simp: word_test_bit_def word_lsb_def)
 
-lemma word_lsb_1_0 [simp]: "lsb (1::'a::len word) & ~ lsb (0::'b::len0 word)"
+lemma word_lsb_1_0 [simp]: "lsb (1::'a::len word) \<and> \<not> lsb (0::'b::len0 word)"
   unfolding word_lsb_def uint_eq_0 uint_1 by simp
 
 lemma word_lsb_last: "lsb (w::'a::len word) = last (to_bl w)"
@@ -2365,15 +2344,14 @@
    apply (auto simp add: bin_to_bl_aux_alt)
   done
 
-lemma word_lsb_int: "lsb w = (uint w mod 2 = 1)"
-  unfolding word_lsb_def bin_last_def by auto
-
-lemma word_msb_sint: "msb w = (sint w < 0)"
-  unfolding 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)"
-  unfolding word_msb_def by (simp add: word_sbin.eq_norm bin_sign_lem)
+lemma word_lsb_int: "lsb w \<longleftrightarrow> uint w mod 2 = 1"
+  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)"
+  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)"
@@ -2384,30 +2362,30 @@
   unfolding word_neg_numeral_alt by (rule msb_word_of_int)
 
 lemma word_msb_0 [simp]: "\<not> msb (0::'a::len word)"
-  unfolding word_msb_def by simp
+  by (simp add: word_msb_def)
 
 lemma word_msb_1 [simp]: "msb (1::'a::len word) \<longleftrightarrow> len_of TYPE('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::'a::len word) = bin_nth (uint w) (len_of TYPE('a) - 1)"
-  unfolding word_msb_def sint_uint by (simp add: bin_sign_lem)
-
-lemma word_msb_alt: "msb (w::'a::len word) = hd (to_bl w)"
+lemma word_msb_nth: "msb w = bin_nth (uint w) (len_of TYPE('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"
   apply (unfold word_msb_nth uint_bl)
   apply (subst hd_conv_nth)
-  apply (rule length_greater_0_conv [THEN iffD1])
+   apply (rule length_greater_0_conv [THEN iffD1])
    apply simp
   apply (simp add : nth_bin_to_bl word_size)
   done
 
-lemma word_set_nth [simp]:
-  "set_bit w n (test_bit w n) = (w::'a::len0 word)"
-  unfolding word_test_bit_def word_set_bit_def by auto
-
-lemma bin_nth_uint':
-  "bin_nth (uint w) n = (rev (bin_to_bl (size w) (uint w)) ! n & n < size w)"
+lemma word_set_nth [simp]: "set_bit w n (test_bit w n) = w"
+  for w :: "'a::len0 word"
+  by (auto simp: word_test_bit_def word_set_bit_def)
+
+lemma bin_nth_uint': "bin_nth (uint w) n \<longleftrightarrow> rev (bin_to_bl (size w) (uint w)) ! n \<and> n < size w"
   apply (unfold word_size)
   apply (safe elim!: bin_nth_uint_imp)
    apply (frule bin_nth_uint_imp)
@@ -2416,9 +2394,8 @@
 
 lemmas bin_nth_uint = bin_nth_uint' [unfolded word_size]
 
-lemma test_bit_bl: "w !! n = (rev (to_bl w) ! n & n < size w)"
-  unfolding to_bl_def word_test_bit_def word_size
-  by (rule bin_nth_uint)
+lemma test_bit_bl: "w !! n \<longleftrightarrow> rev (to_bl w) ! n \<and> n < size w"
+  unfolding to_bl_def word_test_bit_def word_size by (rule bin_nth_uint)
 
 lemma to_bl_nth: "n < size w \<Longrightarrow> to_bl w ! n = w !! (size w - Suc n)"
   apply (unfold test_bit_bl)
@@ -2428,29 +2405,25 @@
    apply (auto simp add: word_size)
   done
 
-lemma test_bit_set:
-  fixes w :: "'a::len0 word"
-  shows "(set_bit w n x) !! n = (n < size w & x)"
-  unfolding word_size word_test_bit_def word_set_bit_def
-  by (clarsimp simp add : word_ubin.eq_norm nth_bintr)
+lemma test_bit_set: "(set_bit w n x) !! n \<longleftrightarrow> n < size w \<and> x"
+  for w :: "'a::len0 word"
+  by (auto simp: word_size word_test_bit_def word_set_bit_def word_ubin.eq_norm nth_bintr)
 
 lemma test_bit_set_gen:
-  fixes w :: "'a::len0 word"
-  shows "test_bit (set_bit w n x) m =
-         (if m = n then n < size w & x else test_bit w m)"
+  "test_bit (set_bit w n x) m = (if m = n then n < size w \<and> x else test_bit w m)"
+  for w :: "'a::len0 word"
   apply (unfold word_size word_test_bit_def word_set_bit_def)
   apply (clarsimp simp add: word_ubin.eq_norm nth_bintr bin_nth_sc_gen)
   apply (auto elim!: test_bit_size [unfolded word_size]
-              simp add: word_test_bit_def [symmetric])
+      simp add: word_test_bit_def [symmetric])
   done
 
 lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs"
   unfolding of_bl_def bl_to_bin_rep_F by auto
 
-lemma msb_nth:
-  fixes w :: "'a::len word"
-  shows "msb w = w !! (len_of TYPE('a) - 1)"
-  unfolding word_msb_nth word_test_bit_def by simp
+lemma msb_nth: "msb w = w !! (len_of TYPE('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]
@@ -2460,8 +2433,9 @@
 lemmas word_ops_lsb = lsb0 [unfolded word_lsb_alt]
 
 lemma td_ext_nth [OF refl refl refl, unfolded word_size]:
-  "n = size (w::'a::len0 word) \<Longrightarrow> ofn = set_bits \<Longrightarrow> [w, ofn g] = l \<Longrightarrow>
-    td_ext test_bit ofn {f. ALL i. f i --> i < n} (%h i. h i & i < n)"
+  "n = size w \<Longrightarrow> ofn = set_bits \<Longrightarrow> [w, ofn g] = l \<Longrightarrow>
+    td_ext test_bit ofn {f. \<forall>i. f i \<longrightarrow> i < n} (\<lambda>h i. h i \<and> i < n)"
+  for w :: "'a::len0 word"
   apply (unfold word_size td_ext_def')
   apply safe
      apply (rule_tac [3] ext)
@@ -2472,38 +2446,38 @@
        apply (clarsimp simp: word_bl.Abs_inverse)+
   apply (rule word_bl.Rep_inverse')
   apply (rule sym [THEN trans])
-  apply (rule bl_of_nth_nth)
+   apply (rule bl_of_nth_nth)
   apply simp
   apply (rule bl_of_nth_inj)
   apply (clarsimp simp add : test_bit_bl word_size)
   done
 
 interpretation test_bit:
-  td_ext "op !! :: 'a::len0 word => nat => 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))"
+  td_ext
+    "op !! :: '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))"
   by (rule td_ext_nth)
 
 lemmas td_nth = test_bit.td_thm
 
-lemma word_set_set_same [simp]:
-  fixes w :: "'a::len0 word"
-  shows "set_bit (set_bit w n x) n y = set_bit w n y"
+lemma word_set_set_same [simp]: "set_bit (set_bit w n x) n y = set_bit w n y"
+  for w :: "'a::len0 word"
   by (rule word_eqI) (simp add : test_bit_set_gen word_size)
 
 lemma word_set_set_diff:
   fixes w :: "'a::len0 word"
-  assumes "m ~= n"
+  assumes "m \<noteq> n"
   shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x"
-  by (rule word_eqI) (clarsimp simp add: test_bit_set_gen word_size assms)
+  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)"
   shows "bin_nth (sint w) n = (if n < l - 1 then w !! n else w !! (l - 1))"
   unfolding sint_uint l_def
-  by (clarsimp simp add: nth_sbintr word_test_bit_def [symmetric])
+  by (auto simp: nth_sbintr word_test_bit_def [symmetric])
 
 lemma word_lsb_numeral [simp]:
   "lsb (numeral bin :: 'a::len word) \<longleftrightarrow> bin_last (numeral bin)"
@@ -2511,14 +2485,11 @@
 
 lemma word_lsb_neg_numeral [simp]:
   "lsb (- numeral bin :: 'a::len word) \<longleftrightarrow> bin_last (- numeral bin)"
-  unfolding word_lsb_alt test_bit_neg_numeral by simp
-
-lemma set_bit_word_of_int:
-  "set_bit (word_of_int x) n b = word_of_int (bin_sc n b x)"
+  by (simp add: word_lsb_alt)
+
+lemma set_bit_word_of_int: "set_bit (word_of_int x) n b = word_of_int (bin_sc n b x)"
   unfolding word_set_bit_def
-  apply (rule word_eqI)
-  apply (simp add: word_size bin_nth_sc_gen word_ubin.eq_norm nth_bintr)
-  done
+  by (rule word_eqI)(simp add: word_size bin_nth_sc_gen word_ubin.eq_norm nth_bintr)
 
 lemma word_set_numeral [simp]:
   "set_bit (numeral bin::'a::len0 word) n b =
@@ -2530,24 +2501,20 @@
     word_of_int (bin_sc n b (- numeral bin))"
   unfolding word_neg_numeral_alt by (rule set_bit_word_of_int)
 
-lemma word_set_bit_0 [simp]:
-  "set_bit 0 n b = word_of_int (bin_sc n b 0)"
+lemma word_set_bit_0 [simp]: "set_bit 0 n b = word_of_int (bin_sc n b 0)"
   unfolding word_0_wi by (rule set_bit_word_of_int)
 
-lemma word_set_bit_1 [simp]:
-  "set_bit 1 n b = word_of_int (bin_sc n b 1)"
+lemma word_set_bit_1 [simp]: "set_bit 1 n b = word_of_int (bin_sc n b 1)"
   unfolding word_1_wi by (rule set_bit_word_of_int)
 
-lemma setBit_no [simp]:
-  "setBit (numeral bin) n = word_of_int (bin_sc n True (numeral bin))"
+lemma setBit_no [simp]: "setBit (numeral bin) n = word_of_int (bin_sc n True (numeral bin))"
   by (simp add: setBit_def)
 
 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 (len_of TYPE('a)) True"
   apply (rule word_bl.Abs_inverse')
    apply simp
   apply (rule word_eqI)
@@ -2558,8 +2525,8 @@
 lemma word_msb_n1 [simp]: "msb (-1::'a::len word)"
   unfolding word_msb_alt to_bl_n1 by simp
 
-lemma word_set_nth_iff:
-  "(set_bit w n b = w) = (w !! n = b | n >= size (w::'a::len0 word))"
+lemma word_set_nth_iff: "set_bit w n b = w \<longleftrightarrow> w !! n = b \<or> n \<ge> size w"
+  for w :: "'a::len0 word"
   apply (rule iffI)
    apply (rule disjCI)
    apply (drule word_eqD)
@@ -2573,18 +2540,13 @@
   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)"
-  unfolding word_test_bit_def
-  by (auto simp add: 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)"
-  unfolding test_bit_2p [symmetric] word_of_int [symmetric]
-  by simp
-
-lemma uint_2p:
-  "(0::'a::len word) < 2 ^ n \<Longrightarrow> uint (2 ^ n::'a::len word) = 2 ^ n"
+lemma test_bit_2p: "(word_of_int (2 ^ n)::'a::len word) !! m \<longleftrightarrow> m = n \<and> m < len_of TYPE('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)"
+  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 clarsimp
@@ -2595,37 +2557,36 @@
    apply clarsimp
   apply (drule word_gt_0 [THEN iffD1])
   apply (safe intro!: word_eqI)
-  apply (auto simp add: nth_2p_bin)
+   apply (auto simp add: nth_2p_bin)
   apply (erule notE)
   apply (simp (no_asm_use) add: uint_word_of_int word_size)
   apply (subst mod_pos_pos_trivial)
-  apply simp
-  apply (rule power_strict_increasing)
-  apply simp_all
+    apply simp
+   apply (rule power_strict_increasing)
+    apply simp_all
   done
 
 lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a::len word) = 2 ^ n"
   by (induct n) (simp_all add: wi_hom_syms)
 
-lemma bang_is_le: "x !! m \<Longrightarrow> 2 ^ m <= (x :: 'a::len word)"
+lemma bang_is_le: "x !! m \<Longrightarrow> 2 ^ m \<le> x"
+  for x :: "'a::len word"
   apply (rule xtr3)
-  apply (rule_tac [2] y = "x" in le_word_or2)
+   apply (rule_tac [2] y = "x" in le_word_or2)
   apply (rule word_eqI)
   apply (auto simp add: word_ao_nth nth_w2p word_size)
   done
 
-lemma word_clr_le:
-  fixes w :: "'a::len0 word"
-  shows "w >= set_bit w n False"
+lemma word_clr_le: "w \<ge> set_bit w n False"
+  for w :: "'a::len0 word"
   apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
   apply (rule order_trans)
    apply (rule bintr_bin_clr_le)
   apply simp
   done
 
-lemma word_set_ge:
-  fixes w :: "'a::len word"
-  shows "w <= set_bit w n True"
+lemma word_set_ge: "w \<le> set_bit w n True"
+  for w :: "'a::len word"
   apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
   apply (rule order_trans [OF _ bintr_bin_set_ge])
   apply simp
@@ -2642,55 +2603,53 @@
   apply simp
   done
 
-lemma shiftl1_numeral [simp]:
-  "shiftl1 (numeral w) = numeral (Num.Bit0 w)"
+lemma shiftl1_numeral [simp]: "shiftl1 (numeral w) = numeral (Num.Bit0 w)"
   unfolding word_numeral_alt shiftl1_wi by simp
 
-lemma shiftl1_neg_numeral [simp]:
-  "shiftl1 (- numeral w) = - numeral (Num.Bit0 w)"
+lemma shiftl1_neg_numeral [simp]: "shiftl1 (- numeral w) = - numeral (Num.Bit0 w)"
   unfolding word_neg_numeral_alt shiftl1_wi by simp
 
 lemma shiftl1_0 [simp] : "shiftl1 0 = 0"
-  unfolding shiftl1_def by simp
+  by (simp add: shiftl1_def)
 
 lemma shiftl1_def_u: "shiftl1 w = word_of_int (uint w BIT False)"
   by (simp only: shiftl1_def) (* FIXME: duplicate *)
 
 lemma shiftl1_def_s: "shiftl1 w = word_of_int (sint w BIT False)"
-  unfolding shiftl1_def Bit_B0 wi_hom_syms by simp
+  by (simp add: shiftl1_def Bit_B0 wi_hom_syms)
 
 lemma shiftr1_0 [simp]: "shiftr1 0 = 0"
-  unfolding shiftr1_def by simp
+  by (simp add: shiftr1_def)
 
 lemma sshiftr1_0 [simp]: "sshiftr1 0 = 0"
-  unfolding sshiftr1_def by simp
-
-lemma sshiftr1_n1 [simp] : "sshiftr1 (- 1) = - 1"
-  unfolding sshiftr1_def by simp
-
-lemma shiftl_0 [simp] : "(0::'a::len0 word) << n = 0"
-  unfolding shiftl_def by (induct n) auto
-
-lemma shiftr_0 [simp] : "(0::'a::len0 word) >> n = 0"
-  unfolding shiftr_def by (induct n) auto
-
-lemma sshiftr_0 [simp] : "0 >>> n = 0"
-  unfolding sshiftr_def by (induct n) auto
-
-lemma sshiftr_n1 [simp] : "-1 >>> n = -1"
-  unfolding sshiftr_def by (induct n) auto
-
-lemma nth_shiftl1: "shiftl1 w !! n = (n < size w & n > 0 & w !! (n - 1))"
+  by (simp add: sshiftr1_def)
+
+lemma sshiftr1_n1 [simp]: "sshiftr1 (- 1) = - 1"
+  by (simp add: sshiftr1_def)
+
+lemma shiftl_0 [simp]: "(0::'a::len0 word) << n = 0"
+  by (induct n) (auto simp: shiftl_def)
+
+lemma shiftr_0 [simp]: "(0::'a::len0 word) >> n = 0"
+  by (induct n) (auto simp: shiftr_def)
+
+lemma sshiftr_0 [simp]: "0 >>> n = 0"
+  by (induct n) (auto simp: sshiftr_def)
+
+lemma sshiftr_n1 [simp]: "-1 >>> n = -1"
+  by (induct n) (auto simp: sshiftr_def)
+
+lemma nth_shiftl1: "shiftl1 w !! n \<longleftrightarrow> n < size w \<and> n > 0 \<and> w !! (n - 1)"
   apply (unfold shiftl1_def word_test_bit_def)
   apply (simp add: nth_bintr word_ubin.eq_norm word_size)
   apply (cases n)
    apply auto
   done
 
-lemma nth_shiftl' [rule_format]:
-  "ALL n. ((w::'a::len0 word) << m) !! n = (n < size w & n >= m & w !! (n - m))"
+lemma nth_shiftl': "(w << m) !! n \<longleftrightarrow> n < size w \<and> n >= m \<and> w !! (n - m)"
+  for w :: "'a::len0 word"
   apply (unfold shiftl_def)
-  apply (induct "m")
+  apply (induct m arbitrary: n)
    apply (force elim!: test_bit_size)
   apply (clarsimp simp add : nth_shiftl1 word_size)
   apply arith
@@ -2706,11 +2665,11 @@
   apply simp
   done
 
-lemma nth_shiftr:
-  "\<And>n. ((w::'a::len0 word) >> m) !! n = w !! (n + m)"
+lemma nth_shiftr: "(w >> m) !! n = w !! (n + m)"
+  for w :: "'a::len0 word"
   apply (unfold shiftr_def)
-  apply (induct "m")
-   apply (auto simp add : nth_shiftr1)
+  apply (induct "m" arbitrary: n)
+   apply (auto simp add: nth_shiftr1)
   done
 
 (* see paper page 10, (1), (2), shiftr1_def is of the form of (1),
@@ -2724,21 +2683,19 @@
   apply simp
   done
 
-lemma nth_sshiftr1:
-  "sshiftr1 w !! n = (if n = size w - 1 then w !! n else w !! Suc n)"
+lemma nth_sshiftr1: "sshiftr1 w !! n = (if n = size w - 1 then w !! n else w !! Suc n)"
   apply (unfold sshiftr1_def word_test_bit_def)
-  apply (simp add: nth_bintr word_ubin.eq_norm
-                   bin_nth.Suc [symmetric] word_size
-             del: bin_nth.simps)
+  apply (simp add: nth_bintr word_ubin.eq_norm bin_nth.Suc [symmetric] word_size
+      del: bin_nth.simps)
   apply (simp add: nth_bintr uint_sint del : bin_nth.simps)
   apply (auto simp add: bin_nth_sint)
   done
 
 lemma nth_sshiftr [rule_format] :
-  "ALL n. sshiftr w m !! n = (n < size w &
-    (if n + m >= size w then w !! (size w - 1) else w !! (n + m)))"
+  "\<forall>n. sshiftr w m !! n =
+    (n < size w \<and> (if n + m \<ge> size w then w !! (size w - 1) else w !! (n + m)))"
   apply (unfold sshiftr_def)
-  apply (induct_tac "m")
+  apply (induct_tac m)
    apply (simp add: test_bit_bl)
   apply (clarsimp simp add: nth_sshiftr1 word_size)
   apply safe
@@ -2781,18 +2738,16 @@
 
 lemma shiftr_div_2n: "uint (shiftr w n) = uint w div 2 ^ n"
   apply (unfold shiftr_def)
-  apply (induct "n")
+  apply (induct n)
    apply simp
-  apply (simp add: shiftr1_div_2 mult.commute
-                   zdiv_zmult2_eq [symmetric])
+  apply (simp add: shiftr1_div_2 mult.commute zdiv_zmult2_eq [symmetric])
   done
 
 lemma sshiftr_div_2n: "sint (sshiftr w n) = sint w div 2 ^ n"
   apply (unfold sshiftr_def)
-  apply (induct "n")
+  apply (induct n)
    apply simp
-  apply (simp add: sshiftr1_div_2 mult.commute
-                   zdiv_zmult2_eq [symmetric])
+  apply (simp add: sshiftr1_div_2 mult.commute zdiv_zmult2_eq [symmetric])
   done
 
 
@@ -2809,22 +2764,20 @@
 
 lemma shiftl1_bl: "shiftl1 (w::'a::len0 word) = of_bl (to_bl w @ [False])"
 proof -
-  have "shiftl1 w = shiftl1 (of_bl (to_bl w))" by simp
-  also have "\<dots> = of_bl (to_bl w @ [False])" by (rule shiftl1_of_bl)
+  have "shiftl1 w = shiftl1 (of_bl (to_bl w))"
+    by simp
+  also have "\<dots> = of_bl (to_bl w @ [False])"
+    by (rule shiftl1_of_bl)
   finally show ?thesis .
 qed
 
-lemma bl_shiftl1:
-  "to_bl (shiftl1 (w :: 'a::len word)) = tl (to_bl w) @ [False]"
-  apply (simp add: shiftl1_bl word_rep_drop drop_Suc drop_Cons')
-  apply (fast intro!: Suc_leI)
-  done
+lemma bl_shiftl1: "to_bl (shiftl1 w) = tl (to_bl w) @ [False]"
+  for w :: "'a::len word"
+  by (simp add: shiftl1_bl word_rep_drop drop_Suc drop_Cons') (fast intro!: Suc_leI)
 
 (* Generalized version of bl_shiftl1. Maybe this one should replace it? *)
-lemma bl_shiftl1':
-  "to_bl (shiftl1 w) = tl (to_bl w @ [False])"
-  unfolding shiftl1_bl
-  by (simp add: word_rep_drop drop_Suc del: drop_append)
+lemma bl_shiftl1': "to_bl (shiftl1 w) = tl (to_bl w @ [False])"
+  by (simp add: shiftl1_bl word_rep_drop drop_Suc del: drop_append)
 
 lemma shiftr1_bl: "shiftr1 w = of_bl (butlast (to_bl w))"
   apply (unfold shiftr1_def uint_bl of_bl_def)
@@ -2832,21 +2785,18 @@
   apply (simp add: bin_rest_trunc [symmetric, unfolded One_nat_def])
   done
 
-lemma bl_shiftr1:
-  "to_bl (shiftr1 (w :: 'a::len word)) = False # butlast (to_bl w)"
-  unfolding shiftr1_bl
-  by (simp add : word_rep_drop len_gt_0 [THEN Suc_leI])
+lemma bl_shiftr1: "to_bl (shiftr1 w) = False # butlast (to_bl w)"
+  for w :: "'a::len word"
+  by (simp add: shiftr1_bl word_rep_drop len_gt_0 [THEN Suc_leI])
 
 (* Generalized version of bl_shiftr1. Maybe this one should replace it? *)
-lemma bl_shiftr1':
-  "to_bl (shiftr1 w) = butlast (False # to_bl w)"
+lemma bl_shiftr1': "to_bl (shiftr1 w) = butlast (False # to_bl w)"
   apply (rule word_bl.Abs_inverse')
-  apply (simp del: butlast.simps)
+   apply (simp del: butlast.simps)
   apply (simp add: shiftr1_bl of_bl_def)
   done
 
-lemma shiftl1_rev:
-  "shiftl1 w = word_reverse (shiftr1 (word_reverse w))"
+lemma shiftl1_rev: "shiftl1 w = word_reverse (shiftr1 (word_reverse w))"
   apply (unfold word_reverse_def)
   apply (rule word_bl.Rep_inverse' [symmetric])
   apply (simp add: bl_shiftl1' bl_shiftr1' word_bl.Abs_inverse)
@@ -2854,12 +2804,8 @@
    apply auto
   done
 
-lemma shiftl_rev:
-  "shiftl w n = word_reverse (shiftr (word_reverse w) n)"
-  apply (unfold shiftl_def shiftr_def)
-  apply (induct "n")
-   apply (auto simp add : shiftl1_rev)
-  done
+lemma shiftl_rev: "shiftl w n = word_reverse (shiftr (word_reverse w) n)"
+  by (induct n) (auto simp add: shiftl_def shiftr_def shiftl1_rev)
 
 lemma rev_shiftl: "word_reverse w << n = word_reverse (w >> n)"
   by (simp add: shiftl_rev)
@@ -2870,8 +2816,8 @@
 lemma rev_shiftr: "word_reverse w >> n = word_reverse (w << n)"
   by (simp add: shiftr_rev)
 
-lemma bl_sshiftr1:
-  "to_bl (sshiftr1 (w :: 'a::len word)) = hd (to_bl w) # butlast (to_bl w)"
+lemma bl_sshiftr1: "to_bl (sshiftr1 w) = hd (to_bl w) # butlast (to_bl w)"
+  for w :: "'a::len word"
   apply (unfold sshiftr1_def uint_bl word_size)
   apply (simp add: butlast_rest_bin word_ubin.eq_norm)
   apply (simp add: sint_uint)
@@ -2880,55 +2826,54 @@
   apply clarsimp
   apply (case_tac i)
    apply (simp_all add: hd_conv_nth length_0_conv [symmetric]
-                        nth_bin_to_bl bin_nth.Suc [symmetric]
-                        nth_sbintr
-                   del: bin_nth.Suc)
+      nth_bin_to_bl bin_nth.Suc [symmetric] nth_sbintr
+      del: bin_nth.Suc)
    apply force
   apply (rule impI)
   apply (rule_tac f = "bin_nth (uint w)" in arg_cong)
   apply simp
   done
 
-lemma drop_shiftr:
-  "drop n (to_bl ((w :: 'a::len word) >> n)) = take (size w - n) (to_bl w)"
+lemma drop_shiftr: "drop n (to_bl (w >> n)) = take (size w - n) (to_bl w)"
+  for w :: "'a::len word"
   apply (unfold shiftr_def)
   apply (induct n)
    prefer 2
    apply (simp add: drop_Suc bl_shiftr1 butlast_drop [symmetric])
    apply (rule butlast_take [THEN trans])
-  apply (auto simp: word_size)
+    apply (auto simp: word_size)
   done
 
-lemma drop_sshiftr:
-  "drop n (to_bl ((w :: 'a::len word) >>> n)) = take (size w - n) (to_bl w)"
+lemma drop_sshiftr: "drop n (to_bl (w >>> n)) = take (size w - n) (to_bl w)"
+  for w :: "'a::len word"
   apply (unfold sshiftr_def)
   apply (induct n)
    prefer 2
    apply (simp add: drop_Suc bl_sshiftr1 butlast_drop [symmetric])
    apply (rule butlast_take [THEN trans])
-  apply (auto simp: word_size)
+    apply (auto simp: word_size)
   done
 
-lemma take_shiftr:
-  "n \<le> size w \<Longrightarrow> take n (to_bl (w >> n)) = replicate n False"
+lemma take_shiftr: "n \<le> size w \<Longrightarrow> take n (to_bl (w >> n)) = replicate n False"
   apply (unfold shiftr_def)
   apply (induct n)
    prefer 2
    apply (simp add: bl_shiftr1' length_0_conv [symmetric] word_size)
    apply (rule take_butlast [THEN trans])
-  apply (auto simp: word_size)
+    apply (auto simp: word_size)
   done
 
 lemma take_sshiftr' [rule_format] :
-  "n <= size (w :: 'a::len word) --> hd (to_bl (w >>> n)) = hd (to_bl w) &
+  "n \<le> size w \<longrightarrow> hd (to_bl (w >>> n)) = hd (to_bl w) \<and>
     take n (to_bl (w >>> n)) = replicate n (hd (to_bl w))"
+  for w :: "'a::len word"
   apply (unfold sshiftr_def)
   apply (induct n)
    prefer 2
    apply (simp add: bl_sshiftr1)
    apply (rule impI)
    apply (rule take_butlast [THEN trans])
-  apply (auto simp: word_size)
+    apply (auto simp: word_size)
   done
 
 lemmas hd_sshiftr = take_sshiftr' [THEN conjunct1]
@@ -2941,26 +2886,25 @@
 lemmas bl_sshiftr = atd_lem [OF take_sshiftr drop_sshiftr]
 
 lemma shiftl_of_bl: "of_bl bl << n = of_bl (bl @ replicate n False)"
-  unfolding shiftl_def
-  by (induct n) (auto simp: shiftl1_of_bl replicate_app_Cons_same)
-
-lemma shiftl_bl:
-  "(w::'a::len0 word) << (n::nat) = of_bl (to_bl w @ replicate n False)"
+  by (induct n) (auto simp: shiftl_def shiftl1_of_bl replicate_app_Cons_same)
+
+lemma shiftl_bl: "w << n = of_bl (to_bl w @ replicate n False)"
+  for w :: "'a::len0 word"
 proof -
-  have "w << n = of_bl (to_bl w) << n" by simp
-  also have "\<dots> = of_bl (to_bl w @ replicate n False)" by (rule shiftl_of_bl)
+  have "w << n = of_bl (to_bl w) << n"
+    by simp
+  also have "\<dots> = of_bl (to_bl w @ replicate n False)"
+    by (rule shiftl_of_bl)
   finally show ?thesis .
 qed
 
 lemmas shiftl_numeral [simp] = shiftl_def [where w="numeral w"] for w
 
-lemma bl_shiftl:
-  "to_bl (w << n) = drop n (to_bl w) @ replicate (min (size w) n) False"
+lemma bl_shiftl: "to_bl (w << n) = drop n (to_bl w) @ replicate (min (size w) n) False"
   by (simp add: shiftl_bl word_rep_drop word_size)
 
-lemma shiftl_zero_size:
-  fixes x :: "'a::len0 word"
-  shows "size x <= n \<Longrightarrow> x << n = 0"
+lemma shiftl_zero_size: "size x \<le> n \<Longrightarrow> x << n = 0"
+  for x :: "'a::len0 word"
   apply (unfold word_size)
   apply (rule word_eqI)
   apply (clarsimp simp add: shiftl_bl word_size test_bit_of_bl nth_append)
@@ -2968,35 +2912,33 @@
 
 (* note - the following results use 'a::len word < number_ring *)
 
-lemma shiftl1_2t: "shiftl1 (w :: 'a::len word) = 2 * w"
+lemma shiftl1_2t: "shiftl1 w = 2 * w"
+  for w :: "'a::len word"
   by (simp add: shiftl1_def Bit_def wi_hom_mult [symmetric])
 
-lemma shiftl1_p: "shiftl1 (w :: 'a::len word) = w + w"
+lemma shiftl1_p: "shiftl1 w = w + w"
+  for w :: "'a::len word"
   by (simp add: shiftl1_2t)
 
-lemma shiftl_t2n: "shiftl (w :: 'a::len word) n = 2 ^ n * w"
-  unfolding shiftl_def
-  by (induct n) (auto simp: shiftl1_2t)
+lemma shiftl_t2n: "shiftl w n = 2 ^ n * w"
+  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)))"
-  unfolding shiftr1_def word_numeral_alt
-  by (simp add: word_ubin.eq_norm)
+  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)))"
-  unfolding sshiftr1_def word_numeral_alt
-  by (simp add: word_sbin.eq_norm)
+  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)))"
-  apply (rule word_eqI)
-  apply (auto simp: nth_shiftr nth_rest_power_bin nth_bintr word_size)
-  done
+  by (rule word_eqI) (auto simp: nth_shiftr nth_rest_power_bin nth_bintr word_size)
 
 lemma sshiftr_no [simp]:
   (* FIXME: neg_numeral *)
@@ -3010,8 +2952,7 @@
 lemma shiftr1_bl_of:
   "length bl \<le> len_of TYPE('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)
+  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>
@@ -3025,53 +2966,57 @@
   apply (simp add: butlast_take)
   done
 
-lemma shiftr_bl:
-  "(x::'a::len0 word) >> n \<equiv> of_bl (take (len_of TYPE('a) - n) (to_bl x))"
+lemma shiftr_bl: "x >> n \<equiv> of_bl (take (len_of TYPE('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::'a::len word) \<longleftrightarrow> (w >> (len_of TYPE('a) - 1)) \<noteq> 0"
+lemma msb_shift: "msb w \<longleftrightarrow> (w >> (len_of TYPE('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])
+   apply (auto simp: word_1_bl of_bl_rep_False [where n=1 and bs="[]", simplified])
   done
 
-lemma zip_replicate:
-  "n \<ge> length ys \<Longrightarrow> zip (replicate n x) ys = map (\<lambda>y. (x, y)) ys"
-  apply (induct ys arbitrary: n, simp_all)
-  apply (case_tac n, simp_all)
+lemma zip_replicate: "n \<ge> length ys \<Longrightarrow> zip (replicate n x) ys = map (\<lambda>y. (x, y)) ys"
+  apply (induct ys arbitrary: n)
+   apply simp_all
+  apply (case_tac n)
+   apply simp_all
   done
 
 lemma align_lem_or [rule_format] :
-  "ALL x m. length x = n + m --> length y = n + m -->
-    drop m x = replicate n False --> take m y = replicate m False -->
+  "\<forall>x m. length x = n + m \<longrightarrow> length y = n + m \<longrightarrow>
+    drop m x = replicate n False \<longrightarrow> take m y = replicate m False \<longrightarrow>
     map2 op | x y = take m x @ drop m y"
-  apply (induct_tac y)
+  apply (induct y)
    apply force
   apply clarsimp
-  apply (case_tac x, force)
-  apply (case_tac m, auto)
+  apply (case_tac x)
+   apply force
+  apply (case_tac m)
+   apply auto
   apply (drule_tac t="length xs" for xs in sym)
-  apply (clarsimp simp: map2_def zip_replicate o_def)
+  apply (auto simp: map2_def zip_replicate o_def)
   done
 
 lemma align_lem_and [rule_format] :
-  "ALL x m. length x = n + m --> length y = n + m -->
-    drop m x = replicate n False --> take m y = replicate m False -->
-    map2 op & x y = replicate (n + m) False"
-  apply (induct_tac y)
+  "\<forall>x m. length x = n + m \<longrightarrow> length y = n + m \<longrightarrow>
+    drop m x = replicate n False \<longrightarrow> take m y = replicate m False \<longrightarrow>
+    map2 op \<and> x y = replicate (n + m) False"
+  apply (induct y)
    apply force
   apply clarsimp
-  apply (case_tac x, force)
-  apply (case_tac m, auto)
+  apply (case_tac x)
+   apply force
+  apply (case_tac m)
+  apply auto
   apply (drule_tac t="length xs" for xs in sym)
-  apply (clarsimp simp: map2_def zip_replicate o_def map_replicate_const)
+  apply (auto simp: map2_def zip_replicate o_def map_replicate_const)
   done
 
 lemma aligned_bl_add_size [OF refl]:
-  "size x - n = m \<Longrightarrow> n <= size x \<Longrightarrow> drop m (to_bl x) = replicate n False \<Longrightarrow>
+  "size x - n = m \<Longrightarrow> n \<le> size x \<Longrightarrow> drop m (to_bl x) = replicate n False \<Longrightarrow>
     take m (to_bl y) = replicate m False \<Longrightarrow>
     to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)"
   apply (subgoal_tac "x AND y = 0")
@@ -3090,8 +3035,7 @@
 
 subsubsection \<open>Mask\<close>
 
-lemma nth_mask [OF refl, simp]:
-  "m = mask n \<Longrightarrow> test_bit m i = (i < n & i < size m)"
+lemma nth_mask [OF refl, simp]: "m = mask n \<Longrightarrow> test_bit m i \<longleftrightarrow> i < n \<and> i < size m"
   apply (unfold mask_def test_bit_bl)
   apply (simp only: word_1_bl [symmetric] shiftl_of_bl)
   apply (clarsimp simp add: word_size)
@@ -3117,7 +3061,8 @@
 lemma and_mask_wi: "word_of_int i AND mask n = word_of_int (bintrunc n i)"
   by (auto simp add: nth_bintr word_size word_ops_nth_size word_eq_iff)
 
-lemma and_mask_wi': "word_of_int i AND mask n = (word_of_int (bintrunc (min LENGTH('a) n) i) :: 'a::len word)"
+lemma and_mask_wi':
+  "word_of_int i AND mask n = (word_of_int (bintrunc (min LENGTH('a) n) i) :: 'a::len word)"
   by (auto simp add: nth_bintr word_size word_ops_nth_size word_eq_iff)
 
 lemma and_mask_no: "numeral i AND mask n = word_of_int (bintrunc n (numeral i))"
@@ -3143,7 +3088,7 @@
   apply (rule xtr8)
    prefer 2
    apply (rule pos_mod_bound)
-  apply auto
+   apply auto
   done
 
 lemma eq_mod_iff: "0 < (n::int) \<Longrightarrow> b = b mod n \<longleftrightarrow> 0 \<le> b \<and> b < n"
@@ -3156,41 +3101,39 @@
   apply (fast intro!: lt2p_lem)
   done
 
-lemma and_mask_dvd: "2 ^ n dvd uint w = (w AND mask n = 0)"
+lemma and_mask_dvd: "2 ^ n dvd uint w \<longleftrightarrow> w AND mask n = 0"
   apply (simp add: dvd_eq_mod_eq_0 and_mask_mod_2p)
-  apply (simp add: word_uint.norm_eq_iff [symmetric] word_of_int_homs
-    del: word_of_int_0)
+  apply (simp add: word_uint.norm_eq_iff [symmetric] word_of_int_homs del: word_of_int_0)
   apply (subst word_uint.norm_Rep [symmetric])
   apply (simp only: bintrunc_bintrunc_min bintrunc_mod2p [symmetric] min_def)
   apply auto
   done
 
-lemma and_mask_dvd_nat: "2 ^ n dvd unat w = (w AND mask n = 0)"
+lemma and_mask_dvd_nat: "2 ^ n dvd unat w \<longleftrightarrow> w AND mask n = 0"
   apply (unfold unat_def)
   apply (rule trans [OF _ and_mask_dvd])
   apply (unfold dvd_def)
   apply auto
-  apply (drule uint_ge_0 [THEN nat_int.Abs_inverse' [simplified], symmetric])
-  apply (simp add : of_nat_mult of_nat_power)
-  apply (simp add : nat_mult_distrib nat_power_eq)
+   apply (drule uint_ge_0 [THEN nat_int.Abs_inverse' [simplified], symmetric])
+   apply simp
+  apply (simp add: nat_mult_distrib nat_power_eq)
   done
 
-lemma word_2p_lem:
-  "n < size w \<Longrightarrow> w < 2 ^ n = (uint (w :: 'a::len word) < 2 ^ n)"
+lemma word_2p_lem: "n < size w \<Longrightarrow> w < 2 ^ n = (uint w < 2 ^ n)"
+  for w :: "'a::len word"
   apply (unfold word_size word_less_alt word_numeral_alt)
-  apply (clarsimp simp add: word_of_int_power_hom word_uint.eq_norm
-                            mod_pos_pos_trivial
-                  simp del: word_of_int_numeral)
+  apply (auto simp add: word_of_int_power_hom word_uint.eq_norm mod_pos_pos_trivial
+      simp del: word_of_int_numeral)
   done
 
-lemma less_mask_eq: "x < 2 ^ n \<Longrightarrow> x AND mask n = (x :: 'a::len word)"
+lemma less_mask_eq: "x < 2 ^ n \<Longrightarrow> x AND mask n = x"
+  for x :: "'a::len word"
   apply (unfold word_less_alt word_numeral_alt)
-  apply (clarsimp simp add: and_mask_mod_2p word_of_int_power_hom
-                            word_uint.eq_norm
-                  simp del: word_of_int_numeral)
+  apply (clarsimp simp add: and_mask_mod_2p word_of_int_power_hom word_uint.eq_norm
+      simp del: word_of_int_numeral)
   apply (drule xtr8 [rotated])
-  apply (rule int_mod_le)
-  apply (auto simp add : mod_pos_pos_trivial)
+   apply (rule int_mod_le)
+   apply (auto simp add : mod_pos_pos_trivial)
   done
 
 lemmas mask_eq_iff_w2p = trans [OF mask_eq_iff word_2p_lem [symmetric]]
@@ -3200,9 +3143,9 @@
 lemma and_mask_less_size: "n < size x \<Longrightarrow> x AND mask n < 2^n"
   unfolding word_size by (erule and_mask_less')
 
-lemma word_mod_2p_is_mask [OF refl]:
-  "c = 2 ^ n \<Longrightarrow> c > 0 \<Longrightarrow> x mod c = (x :: 'a::len word) AND mask n"
-  by (clarsimp simp add: word_mod_def uint_2p and_mask_mod_2p)
+lemma word_mod_2p_is_mask [OF refl]: "c = 2 ^ n \<Longrightarrow> c > 0 \<Longrightarrow> x mod c = x AND mask n"
+  for c x :: "'a::len word"
+  by (auto simp: word_mod_def uint_2p and_mask_mod_2p)
 
 lemma mask_eqs:
   "(a AND mask n) + b AND mask n = a + b AND mask n"
@@ -3218,12 +3161,11 @@
   "word_succ (a AND mask n) AND mask n = word_succ a AND mask n"
   "word_pred (a AND mask n) AND mask n = word_pred a AND mask n"
   using word_of_int_Ex [where x=a] word_of_int_Ex [where x=b]
-  by (auto simp add: and_mask_wi' word_of_int_homs word.abs_eq_iff bintrunc_mod2p mod_simps)
-
-lemma mask_power_eq:
-  "(x AND mask n) ^ k AND mask n = x ^ k AND mask n"
+  by (auto simp: and_mask_wi' word_of_int_homs word.abs_eq_iff bintrunc_mod2p mod_simps)
+
+lemma mask_power_eq: "(x AND mask n) ^ k AND mask n = x ^ k AND mask n"
   using word_of_int_Ex [where x=x]
-  by (auto simp add: and_mask_wi' word_of_int_power_hom word.abs_eq_iff bintrunc_mod2p mod_simps)
+  by (auto simp: and_mask_wi' word_of_int_power_hom word.abs_eq_iff bintrunc_mod2p mod_simps)
 
 
 subsubsection \<open>Revcast\<close>
@@ -3233,8 +3175,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 (len_of TYPE('a)) (to_bl w)"
   apply (unfold revcast_def' word_size)
   apply (rule word_bl.Abs_inverse)
   apply simp
@@ -3244,8 +3185,8 @@
   "cs = [rc, uc] \<Longrightarrow> rc = revcast (word_reverse w) \<Longrightarrow> uc = ucast w \<Longrightarrow>
     rc = word_reverse uc"
   apply (unfold ucast_def revcast_def' Let_def word_reverse_def)
-  apply (clarsimp simp add : to_bl_of_bin takefill_bintrunc)
-  apply (simp add : word_bl.Abs_inverse word_size)
+  apply (auto simp: to_bl_of_bin takefill_bintrunc)
+  apply (simp add: word_bl.Abs_inverse word_size)
   done
 
 lemma revcast_ucast: "revcast w = word_reverse (ucast (word_reverse w))"
@@ -3258,13 +3199,13 @@
   by (fact revcast_ucast [THEN word_rev_gal'])
 
 
-\<comment> "linking revcast and cast via shift"
+text "linking revcast and cast via shift"
 
 lemmas wsst_TYs = source_size target_size word_size
 
 lemma revcast_down_uu [OF refl]:
-  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow>
-    rc (w :: 'a::len word) = ucast (w >> n)"
+  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = ucast (w >> n)"
+  for w :: "'a::len word"
   apply (simp add: revcast_def')
   apply (rule word_bl.Rep_inverse')
   apply (rule trans, rule ucast_down_drop)
@@ -3274,8 +3215,8 @@
   done
 
 lemma revcast_down_us [OF refl]:
-  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow>
-    rc (w :: 'a::len word) = ucast (w >>> n)"
+  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = ucast (w >>> n)"
+  for w :: "'a::len word"
   apply (simp add: revcast_def')
   apply (rule word_bl.Rep_inverse')
   apply (rule trans, rule ucast_down_drop)
@@ -3285,8 +3226,8 @@
   done
 
 lemma revcast_down_su [OF refl]:
-  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow>
-    rc (w :: 'a::len word) = scast (w >> n)"
+  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = scast (w >> n)"
+  for w :: "'a::len word"
   apply (simp add: revcast_def')
   apply (rule word_bl.Rep_inverse')
   apply (rule trans, rule scast_down_drop)
@@ -3296,8 +3237,8 @@
   done
 
 lemma revcast_down_ss [OF refl]:
-  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow>
-    rc (w :: 'a::len word) = scast (w >>> n)"
+  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = scast (w >>> n)"
+  for w :: "'a::len word"
   apply (simp add: revcast_def')
   apply (rule word_bl.Rep_inverse')
   apply (rule trans, rule scast_down_drop)
@@ -3308,8 +3249,8 @@
 
 (* FIXME: should this also be [OF refl] ? *)
 lemma cast_down_rev:
-  "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow>
-    uc w = revcast ((w :: 'a::len word) << n)"
+  "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow> uc w = revcast (w << n)"
+  for w :: "'a::len word"
   apply (unfold shiftl_rev)
   apply clarify
   apply (simp add: revcast_rev_ucast)
@@ -3327,7 +3268,7 @@
   apply (simp add: takefill_alt)
   apply (rule bl_shiftl [THEN trans])
   apply (subst ucast_up_app)
-  apply (auto simp add: wsst_TYs)
+   apply (auto simp add: wsst_TYs)
   done
 
 lemmas rc1 = revcast_up [THEN