src/HOL/Word/Word.thy
changeset 65328 2510b0ce28da
parent 65268 75f2aa8ecb12
child 65336 8e5274fc0093
     1.1 --- a/src/HOL/Word/Word.thy	Sun Mar 19 14:50:37 2017 +0100
     1.2 +++ b/src/HOL/Word/Word.thy	Sun Mar 19 18:28:32 2017 +0100
     1.3 @@ -276,11 +276,9 @@
     1.4  lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "op *"
     1.5    by (auto simp add: bintrunc_mod2p intro: mod_mult_cong)
     1.6  
     1.7 -definition
     1.8 -  word_div_def: "a div b = word_of_int (uint a div uint b)"
     1.9 -
    1.10 -definition
    1.11 -  word_mod_def: "a mod b = word_of_int (uint a mod uint b)"
    1.12 +definition word_div_def: "a div b = word_of_int (uint a div uint b)"
    1.13 +
    1.14 +definition word_mod_def: "a mod b = word_of_int (uint a mod uint b)"
    1.15  
    1.16  instance
    1.17    by standard (transfer, simp add: algebra_simps)+
    1.18 @@ -387,9 +385,8 @@
    1.19    where "shiftl1 w = word_of_int (uint w BIT False)"
    1.20  
    1.21  definition shiftr1 :: "'a word \<Rightarrow> 'a word"
    1.22 -where
    1.23    \<comment> "shift right as unsigned or as signed, ie logical or arithmetic"
    1.24 -  "shiftr1 w = word_of_int (bin_rest (uint w))"
    1.25 +  where "shiftr1 w = word_of_int (bin_rest (uint w))"
    1.26  
    1.27  definition shiftl_def: "w << n = (shiftl1 ^^ n) w"
    1.28  
    1.29 @@ -482,7 +479,8 @@
    1.30  definition word_rsplit :: "'a::len0 word \<Rightarrow> 'b::len word list"
    1.31    where "word_rsplit w = map word_of_int (bin_rsplit (len_of TYPE('b)) (len_of TYPE('a), uint w))"
    1.32  
    1.33 -definition max_word :: "'a::len word"  \<comment> "Largest representable machine integer."
    1.34 +definition max_word :: "'a::len word"
    1.35 +  \<comment> "Largest representable machine integer."
    1.36    where "max_word = word_of_int (2 ^ len_of TYPE('a) - 1)"
    1.37  
    1.38  lemmas of_nth_def = word_set_bits_def (* FIXME duplicate *)
    1.39 @@ -493,7 +491,8 @@
    1.40  lemma sint_sbintrunc': "sint (word_of_int bin :: 'a word) = sbintrunc (len_of TYPE('a::len) - 1) bin"
    1.41    by (auto simp: sint_uint word_ubin.eq_norm sbintrunc_bintrunc_lt)
    1.42  
    1.43 -lemma uint_sint: "uint w = bintrunc (len_of TYPE('a)) (sint (w :: 'a::len word))"
    1.44 +lemma uint_sint: "uint w = bintrunc (len_of TYPE('a)) (sint w)"
    1.45 +  for w :: "'a::len word"
    1.46    by (auto simp: sint_uint bintrunc_sbintrunc_le)
    1.47  
    1.48  lemma bintr_uint: "len_of TYPE('a) \<le> n \<Longrightarrow> bintrunc n (uint w) = uint w"
    1.49 @@ -603,7 +602,8 @@
    1.50    "unat (- numeral bin :: 'a::len0 word) = nat (bintrunc (len_of TYPE('a)) (- numeral bin))"
    1.51    by (simp only: unat_def uint_bintrunc_neg)
    1.52  
    1.53 -lemma size_0_eq: "size (w :: 'a::len0 word) = 0 \<Longrightarrow> v = w"
    1.54 +lemma size_0_eq: "size w = 0 \<Longrightarrow> v = w"
    1.55 +  for v w :: "'a::len0 word"
    1.56    apply (unfold word_size)
    1.57    apply (rule word_uint.Rep_eqD)
    1.58    apply (rule box_equals)
    1.59 @@ -758,7 +758,8 @@
    1.60    done
    1.61  
    1.62  lemma bin_nth_sint:
    1.63 -  "len_of TYPE('a) \<le> n \<Longrightarrow> bin_nth (sint w) n = bin_nth (sint w) (len_of TYPE('a) - 1)"
    1.64 +  "len_of TYPE('a) \<le> n \<Longrightarrow>
    1.65 +    bin_nth (sint w) n = bin_nth (sint w) (len_of TYPE('a) - 1)"
    1.66    for w :: "'a::len word"
    1.67    apply (subst word_sbin.norm_Rep [symmetric])
    1.68    apply (auto simp add: nth_sbintr)
    1.69 @@ -829,7 +830,8 @@
    1.70  
    1.71  lemma test_bit_of_bl:
    1.72    "(of_bl bl::'a::len0 word) !! n = (rev bl ! n \<and> n < len_of TYPE('a) \<and> n < length bl)"
    1.73 -  by (auto simp add: of_bl_def word_test_bit_def word_size word_ubin.eq_norm nth_bintr bin_nth_of_bl)
    1.74 +  by (auto simp add: of_bl_def word_test_bit_def word_size
    1.75 +      word_ubin.eq_norm nth_bintr bin_nth_of_bl)
    1.76  
    1.77  lemma no_of_bl: "(numeral bin ::'a::len0 word) = of_bl (bin_to_bl (len_of TYPE('a)) (numeral bin))"
    1.78    by (simp add: of_bl_def)
    1.79 @@ -919,7 +921,8 @@
    1.80  (* for literal u(s)cast *)
    1.81  
    1.82  lemma ucast_bintr [simp]:
    1.83 -  "ucast (numeral w ::'a::len0 word) =  word_of_int (bintrunc (len_of TYPE('a)) (numeral w))"
    1.84 +  "ucast (numeral w :: 'a::len0 word) =
    1.85 +    word_of_int (bintrunc (len_of TYPE('a)) (numeral w))"
    1.86    by (simp add: ucast_def)
    1.87  
    1.88  (* TODO: neg_numeral *)
    1.89 @@ -1252,35 +1255,34 @@
    1.90  
    1.91  subsection \<open>Order on fixed-length words\<close>
    1.92  
    1.93 -lemma word_zero_le [simp] :
    1.94 -  "0 <= (y :: 'a::len0 word)"
    1.95 +lemma word_zero_le [simp]: "0 \<le> y"
    1.96 +  for y :: "'a::len0 word"
    1.97    unfolding word_le_def by auto
    1.98  
    1.99 -lemma word_m1_ge [simp] : "word_pred 0 >= y" (* FIXME: delete *)
   1.100 -  unfolding word_le_def
   1.101 -  by (simp only : word_pred_0_n1 word_uint.eq_norm m1mod2k) auto
   1.102 -
   1.103 -lemma word_n1_ge [simp]: "y \<le> (-1::'a::len0 word)"
   1.104 -  unfolding word_le_def
   1.105 -  by (simp only: word_m1_wi word_uint.eq_norm m1mod2k) auto
   1.106 +lemma word_m1_ge [simp] : "word_pred 0 \<ge> y" (* FIXME: delete *)
   1.107 +  by (simp only: word_le_def word_pred_0_n1 word_uint.eq_norm m1mod2k) auto
   1.108 +
   1.109 +lemma word_n1_ge [simp]: "y \<le> -1"
   1.110 +  for y :: "'a::len0 word"
   1.111 +  by (simp only: word_le_def word_m1_wi word_uint.eq_norm m1mod2k) auto
   1.112  
   1.113  lemmas word_not_simps [simp] =
   1.114    word_zero_le [THEN leD] word_m1_ge [THEN leD] word_n1_ge [THEN leD]
   1.115  
   1.116 -lemma word_gt_0: "0 < y \<longleftrightarrow> 0 \<noteq> (y :: 'a::len0 word)"
   1.117 +lemma word_gt_0: "0 < y \<longleftrightarrow> 0 \<noteq> y"
   1.118 +  for y :: "'a::len0 word"
   1.119    by (simp add: less_le)
   1.120  
   1.121  lemmas word_gt_0_no [simp] = word_gt_0 [of "numeral y"] for y
   1.122  
   1.123 -lemma word_sless_alt: "(a <s b) = (sint a < sint b)"
   1.124 -  unfolding word_sle_def word_sless_def
   1.125 -  by (auto simp add: less_le)
   1.126 -
   1.127 -lemma word_le_nat_alt: "(a <= b) = (unat a <= unat b)"
   1.128 +lemma word_sless_alt: "a <s b \<longleftrightarrow> sint a < sint b"
   1.129 +  by (auto simp add: word_sle_def word_sless_def less_le)
   1.130 +
   1.131 +lemma word_le_nat_alt: "a \<le> b \<longleftrightarrow> unat a \<le> unat b"
   1.132    unfolding unat_def word_le_def
   1.133    by (rule nat_le_eq_zle [symmetric]) simp
   1.134  
   1.135 -lemma word_less_nat_alt: "(a < b) = (unat a < unat b)"
   1.136 +lemma word_less_nat_alt: "a < b \<longleftrightarrow> unat a < unat b"
   1.137    unfolding unat_def word_less_alt
   1.138    by (rule nat_less_eq_zless [symmetric]) simp
   1.139  
   1.140 @@ -1290,15 +1292,15 @@
   1.141    unfolding word_less_alt by (simp add: word_uint.eq_norm)
   1.142  
   1.143  lemma wi_le:
   1.144 -  "(word_of_int n <= (word_of_int m :: 'a::len0 word)) =
   1.145 -    (n mod 2 ^ len_of TYPE('a) <= m mod 2 ^ len_of TYPE('a))"
   1.146 +  "(word_of_int n \<le> (word_of_int m :: 'a::len0 word)) =
   1.147 +    (n mod 2 ^ len_of TYPE('a) \<le> m mod 2 ^ len_of TYPE('a))"
   1.148    unfolding word_le_def by (simp add: word_uint.eq_norm)
   1.149  
   1.150 -lemma udvd_nat_alt: "a udvd b = (EX n>=0. unat b = n * unat a)"
   1.151 +lemma udvd_nat_alt: "a udvd b \<longleftrightarrow> (\<exists>n\<ge>0. unat b = n * unat a)"
   1.152    apply (unfold udvd_def)
   1.153    apply safe
   1.154     apply (simp add: unat_def nat_mult_distrib)
   1.155 -  apply (simp add: uint_nat of_nat_mult)
   1.156 +  apply (simp add: uint_nat)
   1.157    apply (rule exI)
   1.158    apply safe
   1.159     prefer 2
   1.160 @@ -1317,9 +1319,12 @@
   1.161    shows "unat (w - 1) = unat w - 1"
   1.162  proof -
   1.163    have "0 \<le> uint w" by (fact uint_nonnegative)
   1.164 -  moreover from assms have "0 \<noteq> uint w" by (simp add: uint_0_iff)
   1.165 -  ultimately have "1 \<le> uint w" by arith
   1.166 -  from uint_lt2p [of w] have "uint w - 1 < 2 ^ len_of TYPE('a)" by arith
   1.167 +  moreover from assms have "0 \<noteq> uint w"
   1.168 +    by (simp add: uint_0_iff)
   1.169 +  ultimately have "1 \<le> uint w"
   1.170 +    by arith
   1.171 +  from uint_lt2p [of w] have "uint w - 1 < 2 ^ len_of TYPE('a)"
   1.172 +    by arith
   1.173    with \<open>1 \<le> uint w\<close> have "(uint w - 1) mod 2 ^ len_of TYPE('a) = uint w - 1"
   1.174      by (auto intro: mod_pos_pos_trivial)
   1.175    with \<open>1 \<le> uint w\<close> have "nat ((uint w - 1) mod 2 ^ len_of TYPE('a)) = nat (uint w) - 1"
   1.176 @@ -1328,15 +1333,14 @@
   1.177      by (simp only: unat_def int_word_uint word_arith_wis mod_diff_right_eq)
   1.178  qed
   1.179  
   1.180 -lemma measure_unat: "p ~= 0 \<Longrightarrow> unat (p - 1) < unat p"
   1.181 +lemma measure_unat: "p \<noteq> 0 \<Longrightarrow> unat (p - 1) < unat p"
   1.182    by (simp add: unat_minus_one) (simp add: unat_0_iff [symmetric])
   1.183  
   1.184  lemmas uint_add_ge0 [simp] = add_nonneg_nonneg [OF uint_ge_0 uint_ge_0]
   1.185  lemmas uint_mult_ge0 [simp] = mult_nonneg_nonneg [OF uint_ge_0 uint_ge_0]
   1.186  
   1.187 -lemma uint_sub_lt2p [simp]:
   1.188 -  "uint (x :: 'a::len0 word) - uint (y :: 'b::len0 word) <
   1.189 -    2 ^ len_of TYPE('a)"
   1.190 +lemma uint_sub_lt2p [simp]: "uint x - uint y < 2 ^ len_of TYPE('a)"
   1.191 +  for x :: "'a::len0 word" and y :: "'b::len0 word"
   1.192    using uint_ge_0 [of y] uint_lt2p [of x] by arith
   1.193  
   1.194  
   1.195 @@ -1344,72 +1348,75 @@
   1.196  
   1.197  lemma uint_add_lem:
   1.198    "(uint x + uint y < 2 ^ len_of TYPE('a)) =
   1.199 -    (uint (x + y :: 'a::len0 word) = uint x + uint y)"
   1.200 +    (uint (x + y) = uint x + uint y)"
   1.201 +  for x y :: "'a::len0 word"
   1.202    by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])
   1.203  
   1.204  lemma uint_mult_lem:
   1.205    "(uint x * uint y < 2 ^ len_of TYPE('a)) =
   1.206 -    (uint (x * y :: 'a::len0 word) = uint x * uint y)"
   1.207 -  by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])
   1.208 -
   1.209 -lemma uint_sub_lem:
   1.210 -  "(uint x >= uint y) = (uint (x - y) = uint x - uint y)"
   1.211 +    (uint (x * y) = uint x * uint y)"
   1.212 +  for x y :: "'a::len0 word"
   1.213    by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])
   1.214  
   1.215 -lemma uint_add_le: "uint (x + y) <= uint x + uint y"
   1.216 +lemma uint_sub_lem: "uint x \<ge> uint y \<longleftrightarrow> uint (x - y) = uint x - uint y"
   1.217 +  by (auto simp: uint_word_ariths intro!: trans [OF _ int_mod_lem])
   1.218 +
   1.219 +lemma uint_add_le: "uint (x + y) \<le> uint x + uint y"
   1.220    unfolding uint_word_ariths by (metis uint_add_ge0 zmod_le_nonneg_dividend)
   1.221  
   1.222 -lemma uint_sub_ge: "uint (x - y) >= uint x - uint y"
   1.223 +lemma uint_sub_ge: "uint (x - y) \<ge> uint x - uint y"
   1.224    unfolding uint_word_ariths by (metis int_mod_ge uint_sub_lt2p zless2p)
   1.225  
   1.226  lemma mod_add_if_z:
   1.227 -  "(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==>
   1.228 -   (x + y) mod z = (if x + y < z then x + y else x + y - z)"
   1.229 +  "x < z \<Longrightarrow> y < z \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> z \<Longrightarrow>
   1.230 +    (x + y) mod z = (if x + y < z then x + y else x + y - z)"
   1.231 +  for x y z :: int
   1.232    by (auto intro: int_mod_eq)
   1.233  
   1.234  lemma uint_plus_if':
   1.235 -  "uint ((a::'a word) + b) =
   1.236 -  (if uint a + uint b < 2 ^ len_of TYPE('a::len0) then uint a + uint b
   1.237 -   else uint a + uint b - 2 ^ len_of TYPE('a))"
   1.238 +  "uint (a + b) =
   1.239 +    (if uint a + uint b < 2 ^ len_of TYPE('a) then uint a + uint b
   1.240 +     else uint a + uint b - 2 ^ len_of TYPE('a))"
   1.241 +  for a b :: "'a::len0 word"
   1.242    using mod_add_if_z [of "uint a" _ "uint b"] by (simp add: uint_word_ariths)
   1.243  
   1.244  lemma mod_sub_if_z:
   1.245 -  "(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==>
   1.246 -   (x - y) mod z = (if y <= x then x - y else x - y + z)"
   1.247 +  "x < z \<Longrightarrow> y < z \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> z \<Longrightarrow>
   1.248 +    (x - y) mod z = (if y \<le> x then x - y else x - y + z)"
   1.249 +  for x y z :: int
   1.250    by (auto intro: int_mod_eq)
   1.251  
   1.252  lemma uint_sub_if':
   1.253 -  "uint ((a::'a word) - b) =
   1.254 -  (if uint b \<le> uint a then uint a - uint b
   1.255 -   else uint a - uint b + 2 ^ len_of TYPE('a::len0))"
   1.256 +  "uint (a - b) =
   1.257 +    (if uint b \<le> uint a then uint a - uint b
   1.258 +     else uint a - uint b + 2 ^ len_of TYPE('a))"
   1.259 +  for a b :: "'a::len0 word"
   1.260    using mod_sub_if_z [of "uint a" _ "uint b"] by (simp add: uint_word_ariths)
   1.261  
   1.262  
   1.263  subsection \<open>Definition of \<open>uint_arith\<close>\<close>
   1.264  
   1.265  lemma word_of_int_inverse:
   1.266 -  "word_of_int r = a \<Longrightarrow> 0 <= r \<Longrightarrow> r < 2 ^ len_of TYPE('a) \<Longrightarrow>
   1.267 -   uint (a::'a::len0 word) = r"
   1.268 +  "word_of_int r = a \<Longrightarrow> 0 \<le> r \<Longrightarrow> r < 2 ^ len_of TYPE('a) \<Longrightarrow> uint a = r"
   1.269 +  for a :: "'a::len0 word"
   1.270    apply (erule word_uint.Abs_inverse' [rotated])
   1.271    apply (simp add: uints_num)
   1.272    done
   1.273  
   1.274  lemma uint_split:
   1.275 -  fixes x::"'a::len0 word"
   1.276 -  shows "P (uint x) =
   1.277 -         (ALL i. word_of_int i = x & 0 <= i & i < 2^len_of TYPE('a) --> P i)"
   1.278 +  "P (uint x) = (\<forall>i. word_of_int i = x \<and> 0 \<le> i \<and> i < 2^len_of TYPE('a) \<longrightarrow> P i)"
   1.279 +  for x :: "'a::len0 word"
   1.280    apply (fold word_int_case_def)
   1.281    apply (auto dest!: word_of_int_inverse simp: int_word_uint mod_pos_pos_trivial
   1.282 -              split: word_int_split)
   1.283 +      split: word_int_split)
   1.284    done
   1.285  
   1.286  lemma uint_split_asm:
   1.287 -  fixes x::"'a::len0 word"
   1.288 -  shows "P (uint x) =
   1.289 -         (~(EX i. word_of_int i = x & 0 <= i & i < 2^len_of TYPE('a) & ~ P i))"
   1.290 +  "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)"
   1.291 +  for x :: "'a::len0 word"
   1.292    by (auto dest!: word_of_int_inverse
   1.293 -           simp: int_word_uint mod_pos_pos_trivial
   1.294 -           split: uint_split)
   1.295 +      simp: int_word_uint mod_pos_pos_trivial
   1.296 +      split: uint_split)
   1.297  
   1.298  lemmas uint_splits = uint_split uint_split_asm
   1.299  
   1.300 @@ -1461,18 +1468,18 @@
   1.301  
   1.302  subsection \<open>More on overflows and monotonicity\<close>
   1.303  
   1.304 -lemma no_plus_overflow_uint_size:
   1.305 -  "((x :: 'a::len0 word) <= x + y) = (uint x + uint y < 2 ^ size x)"
   1.306 +lemma no_plus_overflow_uint_size: "x \<le> x + y \<longleftrightarrow> uint x + uint y < 2 ^ size x"
   1.307 +  for x y :: "'a::len0 word"
   1.308    unfolding word_size by uint_arith
   1.309  
   1.310  lemmas no_olen_add = no_plus_overflow_uint_size [unfolded word_size]
   1.311  
   1.312 -lemma no_ulen_sub: "((x :: 'a::len0 word) >= x - y) = (uint y <= uint x)"
   1.313 +lemma no_ulen_sub: "x \<ge> x - y \<longleftrightarrow> uint y \<le> uint x"
   1.314 +  for x y :: "'a::len0 word"
   1.315    by uint_arith
   1.316  
   1.317 -lemma no_olen_add':
   1.318 -  fixes x :: "'a::len0 word"
   1.319 -  shows "(x \<le> y + x) = (uint y + uint x < 2 ^ len_of TYPE('a))"
   1.320 +lemma no_olen_add': "x \<le> y + x \<longleftrightarrow> uint y + uint x < 2 ^ len_of TYPE('a)"
   1.321 +  for x y :: "'a::len0 word"
   1.322    by (simp add: ac_simps no_olen_add)
   1.323  
   1.324  lemmas olen_add_eqv = trans [OF no_olen_add no_olen_add' [symmetric]]
   1.325 @@ -1484,120 +1491,118 @@
   1.326  lemmas word_sub_le_iff = no_ulen_sub [folded word_le_def]
   1.327  lemmas word_sub_le = word_sub_le_iff [THEN iffD2]
   1.328  
   1.329 -lemma word_less_sub1:
   1.330 -  "(x :: 'a::len word) ~= 0 \<Longrightarrow> (1 < x) = (0 < x - 1)"
   1.331 +lemma word_less_sub1: "x \<noteq> 0 \<Longrightarrow> 1 < x \<longleftrightarrow> 0 < x - 1"
   1.332 +  for x :: "'a::len word"
   1.333    by uint_arith
   1.334  
   1.335 -lemma word_le_sub1:
   1.336 -  "(x :: 'a::len word) ~= 0 \<Longrightarrow> (1 <= x) = (0 <= x - 1)"
   1.337 +lemma word_le_sub1: "x \<noteq> 0 \<Longrightarrow> 1 \<le> x \<longleftrightarrow> 0 \<le> x - 1"
   1.338 +  for x :: "'a::len word"
   1.339    by uint_arith
   1.340  
   1.341 -lemma sub_wrap_lt:
   1.342 -  "((x :: 'a::len0 word) < x - z) = (x < z)"
   1.343 +lemma sub_wrap_lt: "x < x - z \<longleftrightarrow> x < z"
   1.344 +  for x z :: "'a::len0 word"
   1.345    by uint_arith
   1.346  
   1.347 -lemma sub_wrap:
   1.348 -  "((x :: 'a::len0 word) <= x - z) = (z = 0 | x < z)"
   1.349 +lemma sub_wrap: "x \<le> x - z \<longleftrightarrow> z = 0 \<or> x < z"
   1.350 +  for x z :: "'a::len0 word"
   1.351    by uint_arith
   1.352  
   1.353 -lemma plus_minus_not_NULL_ab:
   1.354 -  "(x :: 'a::len0 word) <= ab - c \<Longrightarrow> c <= ab \<Longrightarrow> c ~= 0 \<Longrightarrow> x + c ~= 0"
   1.355 +lemma plus_minus_not_NULL_ab: "x \<le> ab - c \<Longrightarrow> c \<le> ab \<Longrightarrow> c \<noteq> 0 \<Longrightarrow> x + c \<noteq> 0"
   1.356 +  for x ab c :: "'a::len0 word"
   1.357    by uint_arith
   1.358  
   1.359 -lemma plus_minus_no_overflow_ab:
   1.360 -  "(x :: 'a::len0 word) <= ab - c \<Longrightarrow> c <= ab \<Longrightarrow> x <= x + c"
   1.361 +lemma plus_minus_no_overflow_ab: "x \<le> ab - c \<Longrightarrow> c \<le> ab \<Longrightarrow> x \<le> x + c"
   1.362 +  for x ab c :: "'a::len0 word"
   1.363    by uint_arith
   1.364  
   1.365 -lemma le_minus':
   1.366 -  "(a :: 'a::len0 word) + c <= b \<Longrightarrow> a <= a + c \<Longrightarrow> c <= b - a"
   1.367 +lemma le_minus': "a + c \<le> b \<Longrightarrow> a \<le> a + c \<Longrightarrow> c \<le> b - a"
   1.368 +  for a b c :: "'a::len0 word"
   1.369    by uint_arith
   1.370  
   1.371 -lemma le_plus':
   1.372 -  "(a :: 'a::len0 word) <= b \<Longrightarrow> c <= b - a \<Longrightarrow> a + c <= b"
   1.373 +lemma le_plus': "a \<le> b \<Longrightarrow> c \<le> b - a \<Longrightarrow> a + c \<le> b"
   1.374 +  for a b c :: "'a::len0 word"
   1.375    by uint_arith
   1.376  
   1.377  lemmas le_plus = le_plus' [rotated]
   1.378  
   1.379  lemmas le_minus = leD [THEN thin_rl, THEN le_minus'] (* FIXME *)
   1.380  
   1.381 -lemma word_plus_mono_right:
   1.382 -  "(y :: 'a::len0 word) <= z \<Longrightarrow> x <= x + z \<Longrightarrow> x + y <= x + z"
   1.383 +lemma word_plus_mono_right: "y \<le> z \<Longrightarrow> x \<le> x + z \<Longrightarrow> x + y \<le> x + z"
   1.384 +  for x y z :: "'a::len0 word"
   1.385    by uint_arith
   1.386  
   1.387 -lemma word_less_minus_cancel:
   1.388 -  "y - x < z - x \<Longrightarrow> x <= z \<Longrightarrow> (y :: 'a::len0 word) < z"
   1.389 +lemma word_less_minus_cancel: "y - x < z - x \<Longrightarrow> x \<le> z \<Longrightarrow> y < z"
   1.390 +  for x y z :: "'a::len0 word"
   1.391    by uint_arith
   1.392  
   1.393 -lemma word_less_minus_mono_left:
   1.394 -  "(y :: 'a::len0 word) < z \<Longrightarrow> x <= y \<Longrightarrow> y - x < z - x"
   1.395 +lemma word_less_minus_mono_left: "y < z \<Longrightarrow> x \<le> y \<Longrightarrow> y - x < z - x"
   1.396 +  for x y z :: "'a::len0 word"
   1.397    by uint_arith
   1.398  
   1.399 -lemma word_less_minus_mono:
   1.400 -  "a < c \<Longrightarrow> d < b \<Longrightarrow> a - b < a \<Longrightarrow> c - d < c
   1.401 -  \<Longrightarrow> a - b < c - (d::'a::len word)"
   1.402 +lemma word_less_minus_mono: "a < c \<Longrightarrow> d < b \<Longrightarrow> a - b < a \<Longrightarrow> c - d < c \<Longrightarrow> a - b < c - d"
   1.403 +  for a b c d :: "'a::len word"
   1.404    by uint_arith
   1.405  
   1.406 -lemma word_le_minus_cancel:
   1.407 -  "y - x <= z - x \<Longrightarrow> x <= z \<Longrightarrow> (y :: 'a::len0 word) <= z"
   1.408 +lemma word_le_minus_cancel: "y - x \<le> z - x \<Longrightarrow> x \<le> z \<Longrightarrow> y \<le> z"
   1.409 +  for x y z :: "'a::len0 word"
   1.410    by uint_arith
   1.411  
   1.412 -lemma word_le_minus_mono_left:
   1.413 -  "(y :: 'a::len0 word) <= z \<Longrightarrow> x <= y \<Longrightarrow> y - x <= z - x"
   1.414 +lemma word_le_minus_mono_left: "y \<le> z \<Longrightarrow> x \<le> y \<Longrightarrow> y - x \<le> z - x"
   1.415 +  for x y z :: "'a::len0 word"
   1.416    by uint_arith
   1.417  
   1.418  lemma word_le_minus_mono:
   1.419 -  "a <= c \<Longrightarrow> d <= b \<Longrightarrow> a - b <= a \<Longrightarrow> c - d <= c
   1.420 -  \<Longrightarrow> a - b <= c - (d::'a::len word)"
   1.421 +  "a \<le> c \<Longrightarrow> d \<le> b \<Longrightarrow> a - b \<le> a \<Longrightarrow> c - d \<le> c \<Longrightarrow> a - b \<le> c - d"
   1.422 +  for a b c d :: "'a::len word"
   1.423    by uint_arith
   1.424  
   1.425 -lemma plus_le_left_cancel_wrap:
   1.426 -  "(x :: 'a::len0 word) + y' < x \<Longrightarrow> x + y < x \<Longrightarrow> (x + y' < x + y) = (y' < y)"
   1.427 +lemma plus_le_left_cancel_wrap: "x + y' < x \<Longrightarrow> x + y < x \<Longrightarrow> x + y' < x + y \<longleftrightarrow> y' < y"
   1.428 +  for x y y' :: "'a::len0 word"
   1.429    by uint_arith
   1.430  
   1.431 -lemma plus_le_left_cancel_nowrap:
   1.432 -  "(x :: 'a::len0 word) <= x + y' \<Longrightarrow> x <= x + y \<Longrightarrow>
   1.433 -    (x + y' < x + y) = (y' < y)"
   1.434 +lemma plus_le_left_cancel_nowrap: "x \<le> x + y' \<Longrightarrow> x \<le> x + y \<Longrightarrow> x + y' < x + y \<longleftrightarrow> y' < y"
   1.435 +  for x y y' :: "'a::len0 word"
   1.436    by uint_arith
   1.437  
   1.438 -lemma word_plus_mono_right2:
   1.439 -  "(a :: 'a::len0 word) <= a + b \<Longrightarrow> c <= b \<Longrightarrow> a <= a + c"
   1.440 +lemma word_plus_mono_right2: "a \<le> a + b \<Longrightarrow> c \<le> b \<Longrightarrow> a \<le> a + c"
   1.441 +  for a b c :: "'a::len0 word"
   1.442 +  by uint_arith
   1.443 +
   1.444 +lemma word_less_add_right: "x < y - z \<Longrightarrow> z \<le> y \<Longrightarrow> x + z < y"
   1.445 +  for x y z :: "'a::len0 word"
   1.446    by uint_arith
   1.447  
   1.448 -lemma word_less_add_right:
   1.449 -  "(x :: 'a::len0 word) < y - z \<Longrightarrow> z <= y \<Longrightarrow> x + z < y"
   1.450 +lemma word_less_sub_right: "x < y + z \<Longrightarrow> y \<le> x \<Longrightarrow> x - y < z"
   1.451 +  for x y z :: "'a::len0 word"
   1.452    by uint_arith
   1.453  
   1.454 -lemma word_less_sub_right:
   1.455 -  "(x :: 'a::len0 word) < y + z \<Longrightarrow> y <= x \<Longrightarrow> x - y < z"
   1.456 -  by uint_arith
   1.457 -
   1.458 -lemma word_le_plus_either:
   1.459 -  "(x :: 'a::len0 word) <= y | x <= z \<Longrightarrow> y <= y + z \<Longrightarrow> x <= y + z"
   1.460 +lemma word_le_plus_either: "x \<le> y \<or> x \<le> z \<Longrightarrow> y \<le> y + z \<Longrightarrow> x \<le> y + z"
   1.461 +  for x y z :: "'a::len0 word"
   1.462    by uint_arith
   1.463  
   1.464 -lemma word_less_nowrapI:
   1.465 -  "(x :: 'a::len0 word) < z - k \<Longrightarrow> k <= z \<Longrightarrow> 0 < k \<Longrightarrow> x < x + k"
   1.466 +lemma word_less_nowrapI: "x < z - k \<Longrightarrow> k \<le> z \<Longrightarrow> 0 < k \<Longrightarrow> x < x + k"
   1.467 +  for x z k :: "'a::len0 word"
   1.468    by uint_arith
   1.469  
   1.470 -lemma inc_le: "(i :: 'a::len word) < m \<Longrightarrow> i + 1 <= m"
   1.471 +lemma inc_le: "i < m \<Longrightarrow> i + 1 \<le> m"
   1.472 +  for i m :: "'a::len word"
   1.473    by uint_arith
   1.474  
   1.475 -lemma inc_i:
   1.476 -  "(1 :: 'a::len word) <= i \<Longrightarrow> i < m \<Longrightarrow> 1 <= (i + 1) & i + 1 <= m"
   1.477 +lemma inc_i: "1 \<le> i \<Longrightarrow> i < m \<Longrightarrow> 1 \<le> i + 1 \<and> i + 1 \<le> m"
   1.478 +  for i m :: "'a::len word"
   1.479    by uint_arith
   1.480  
   1.481  lemma udvd_incr_lem:
   1.482    "up < uq \<Longrightarrow> up = ua + n * uint K \<Longrightarrow>
   1.483 -    uq = ua + n' * uint K \<Longrightarrow> up + uint K <= uq"
   1.484 +    uq = ua + n' * uint K \<Longrightarrow> up + uint K \<le> uq"
   1.485    apply clarsimp
   1.486 -
   1.487    apply (drule less_le_mult)
   1.488 -  apply safe
   1.489 +   apply safe
   1.490    done
   1.491  
   1.492  lemma udvd_incr':
   1.493    "p < q \<Longrightarrow> uint p = ua + n * uint K \<Longrightarrow>
   1.494 -    uint q = ua + n' * uint K \<Longrightarrow> p + K <= q"
   1.495 +    uint q = ua + n' * uint K \<Longrightarrow> p + K \<le> q"
   1.496    apply (unfold word_less_alt word_le_def)
   1.497    apply (drule (2) udvd_incr_lem)
   1.498    apply (erule uint_add_le [THEN order_trans])
   1.499 @@ -1605,7 +1610,7 @@
   1.500  
   1.501  lemma udvd_decr':
   1.502    "p < q \<Longrightarrow> uint p = ua + n * uint K \<Longrightarrow>
   1.503 -    uint q = ua + n' * uint K \<Longrightarrow> p <= q - K"
   1.504 +    uint q = ua + n' * uint K \<Longrightarrow> p \<le> q - K"
   1.505    apply (unfold word_less_alt word_le_def)
   1.506    apply (drule (2) udvd_incr_lem)
   1.507    apply (drule le_diff_eq [THEN iffD2])
   1.508 @@ -1617,17 +1622,16 @@
   1.509  lemmas udvd_incr0 = udvd_incr' [where ua=0, unfolded add_0_left]
   1.510  lemmas udvd_decr0 = udvd_decr' [where ua=0, unfolded add_0_left]
   1.511  
   1.512 -lemma udvd_minus_le':
   1.513 -  "xy < k \<Longrightarrow> z udvd xy \<Longrightarrow> z udvd k \<Longrightarrow> xy <= k - z"
   1.514 +lemma udvd_minus_le': "xy < k \<Longrightarrow> z udvd xy \<Longrightarrow> z udvd k \<Longrightarrow> xy \<le> k - z"
   1.515    apply (unfold udvd_def)
   1.516    apply clarify
   1.517    apply (erule (2) udvd_decr0)
   1.518    done
   1.519  
   1.520  lemma udvd_incr2_K:
   1.521 -  "p < a + s \<Longrightarrow> a <= a + s \<Longrightarrow> K udvd s \<Longrightarrow> K udvd p - a \<Longrightarrow> a <= p \<Longrightarrow>
   1.522 -    0 < K \<Longrightarrow> p <= p + K & p + K <= a + s"
   1.523 -  using [[simproc del: linordered_ring_less_cancel_factor]]
   1.524 +  "p < a + s \<Longrightarrow> a \<le> a + s \<Longrightarrow> K udvd s \<Longrightarrow> K udvd p - a \<Longrightarrow> a \<le> p \<Longrightarrow>
   1.525 +    0 < K \<Longrightarrow> p \<le> p + K \<and> p + K \<le> a + s"
   1.526 +  supply [[simproc del: linordered_ring_less_cancel_factor]]
   1.527    apply (unfold udvd_def)
   1.528    apply clarify
   1.529    apply (simp add: uint_arith_simps split: if_split_asm)
   1.530 @@ -1642,16 +1646,14 @@
   1.531    done
   1.532  
   1.533  (* links with rbl operations *)
   1.534 -lemma word_succ_rbl:
   1.535 -  "to_bl w = bl \<Longrightarrow> to_bl (word_succ w) = (rev (rbl_succ (rev bl)))"
   1.536 +lemma word_succ_rbl: "to_bl w = bl \<Longrightarrow> to_bl (word_succ w) = rev (rbl_succ (rev bl))"
   1.537    apply (unfold word_succ_def)
   1.538    apply clarify
   1.539    apply (simp add: to_bl_of_bin)
   1.540    apply (simp add: to_bl_def rbl_succ)
   1.541    done
   1.542  
   1.543 -lemma word_pred_rbl:
   1.544 -  "to_bl w = bl \<Longrightarrow> to_bl (word_pred w) = (rev (rbl_pred (rev bl)))"
   1.545 +lemma word_pred_rbl: "to_bl w = bl \<Longrightarrow> to_bl (word_pred w) = rev (rbl_pred (rev bl))"
   1.546    apply (unfold word_pred_def)
   1.547    apply clarify
   1.548    apply (simp add: to_bl_of_bin)
   1.549 @@ -1660,7 +1662,7 @@
   1.550  
   1.551  lemma word_add_rbl:
   1.552    "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow>
   1.553 -    to_bl (v + w) = (rev (rbl_add (rev vbl) (rev wbl)))"
   1.554 +    to_bl (v + w) = rev (rbl_add (rev vbl) (rev wbl))"
   1.555    apply (unfold word_add_def)
   1.556    apply clarify
   1.557    apply (simp add: to_bl_of_bin)
   1.558 @@ -1669,7 +1671,7 @@
   1.559  
   1.560  lemma word_mult_rbl:
   1.561    "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow>
   1.562 -    to_bl (v * w) = (rev (rbl_mult (rev vbl) (rev wbl)))"
   1.563 +    to_bl (v * w) = rev (rbl_mult (rev vbl) (rev wbl))"
   1.564    apply (unfold word_mult_def)
   1.565    apply clarify
   1.566    apply (simp add: to_bl_of_bin)
   1.567 @@ -1681,8 +1683,7 @@
   1.568    "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_pred w)) = rbl_pred ys"
   1.569    "rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v * w)) = rbl_mult ys xs"
   1.570    "rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v + w)) = rbl_add ys xs"
   1.571 -  by (auto simp: rev_swap [symmetric] word_succ_rbl
   1.572 -                 word_pred_rbl word_mult_rbl word_add_rbl)
   1.573 +  by (auto simp: rev_swap [symmetric] word_succ_rbl word_pred_rbl word_mult_rbl word_add_rbl)
   1.574  
   1.575  
   1.576  subsection \<open>Arithmetic type class instantiations\<close>
   1.577 @@ -1690,9 +1691,8 @@
   1.578  lemmas word_le_0_iff [simp] =
   1.579    word_zero_le [THEN leD, THEN linorder_antisym_conv1]
   1.580  
   1.581 -lemma word_of_int_nat:
   1.582 -  "0 <= x \<Longrightarrow> word_of_int x = of_nat (nat x)"
   1.583 -  by (simp add: of_nat_nat word_of_int)
   1.584 +lemma word_of_int_nat: "0 \<le> x \<Longrightarrow> word_of_int x = of_nat (nat x)"
   1.585 +  by (simp add: word_of_int)
   1.586  
   1.587  (* note that iszero_def is only for class comm_semiring_1_cancel,
   1.588     which requires word length >= 1, ie 'a::len word *)
   1.589 @@ -1712,44 +1712,43 @@
   1.590  
   1.591  lemma td_ext_unat [OF refl]:
   1.592    "n = len_of TYPE('a::len) \<Longrightarrow>
   1.593 -    td_ext (unat :: 'a word => nat) of_nat
   1.594 -    (unats n) (%i. i mod 2 ^ n)"
   1.595 +    td_ext (unat :: 'a word \<Rightarrow> nat) of_nat (unats n) (\<lambda>i. i mod 2 ^ n)"
   1.596    apply (unfold td_ext_def' unat_def word_of_nat unats_uints)
   1.597    apply (auto intro!: imageI simp add : word_of_int_hom_syms)
   1.598 -  apply (erule word_uint.Abs_inverse [THEN arg_cong])
   1.599 +   apply (erule word_uint.Abs_inverse [THEN arg_cong])
   1.600    apply (simp add: int_word_uint nat_mod_distrib nat_power_eq)
   1.601    done
   1.602  
   1.603  lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm]
   1.604  
   1.605  interpretation word_unat:
   1.606 -  td_ext "unat::'a::len word => nat"
   1.607 -         of_nat
   1.608 -         "unats (len_of TYPE('a::len))"
   1.609 -         "%i. i mod 2 ^ len_of TYPE('a::len)"
   1.610 +  td_ext
   1.611 +    "unat::'a::len word \<Rightarrow> nat"
   1.612 +    of_nat
   1.613 +    "unats (len_of TYPE('a::len))"
   1.614 +    "\<lambda>i. i mod 2 ^ len_of TYPE('a::len)"
   1.615    by (rule td_ext_unat)
   1.616  
   1.617  lemmas td_unat = word_unat.td_thm
   1.618  
   1.619  lemmas unat_lt2p [iff] = word_unat.Rep [unfolded unats_def mem_Collect_eq]
   1.620  
   1.621 -lemma unat_le: "y <= unat (z :: 'a::len word) \<Longrightarrow> y : unats (len_of TYPE('a))"
   1.622 +lemma unat_le: "y \<le> unat z \<Longrightarrow> y \<in> unats (len_of TYPE('a))"
   1.623 +  for z :: "'a::len word"
   1.624    apply (unfold unats_def)
   1.625    apply clarsimp
   1.626    apply (rule xtrans, rule unat_lt2p, assumption)
   1.627    done
   1.628  
   1.629 -lemma word_nchotomy:
   1.630 -  "ALL w. EX n. (w :: 'a::len word) = of_nat n & n < 2 ^ len_of TYPE('a)"
   1.631 +lemma word_nchotomy: "\<forall>w :: 'a::len word. \<exists>n. w = of_nat n \<and> n < 2 ^ len_of TYPE('a)"
   1.632    apply (rule allI)
   1.633    apply (rule word_unat.Abs_cases)
   1.634    apply (unfold unats_def)
   1.635    apply auto
   1.636    done
   1.637  
   1.638 -lemma of_nat_eq:
   1.639 -  fixes w :: "'a::len word"
   1.640 -  shows "(of_nat n = w) = (\<exists>q. n = unat w + q * 2 ^ len_of TYPE('a))"
   1.641 +lemma of_nat_eq: "of_nat n = w \<longleftrightarrow> (\<exists>q. n = unat w + q * 2 ^ len_of TYPE('a))"
   1.642 +  for w :: "'a::len word"
   1.643    apply (rule trans)
   1.644     apply (rule word_unat.inverse_norm)
   1.645    apply (rule iffI)
   1.646 @@ -1758,35 +1757,28 @@
   1.647    apply clarsimp
   1.648    done
   1.649  
   1.650 -lemma of_nat_eq_size:
   1.651 -  "(of_nat n = w) = (EX q. n = unat w + q * 2 ^ size w)"
   1.652 +lemma of_nat_eq_size: "of_nat n = w \<longleftrightarrow> (\<exists>q. n = unat w + q * 2 ^ size w)"
   1.653    unfolding word_size by (rule of_nat_eq)
   1.654  
   1.655 -lemma of_nat_0:
   1.656 -  "(of_nat m = (0::'a::len word)) = (\<exists>q. m = q * 2 ^ len_of TYPE('a))"
   1.657 +lemma of_nat_0: "of_nat m = (0::'a::len word) \<longleftrightarrow> (\<exists>q. m = q * 2 ^ len_of TYPE('a))"
   1.658    by (simp add: of_nat_eq)
   1.659  
   1.660 -lemma of_nat_2p [simp]:
   1.661 -  "of_nat (2 ^ len_of TYPE('a)) = (0::'a::len word)"
   1.662 +lemma of_nat_2p [simp]: "of_nat (2 ^ len_of TYPE('a)) = (0::'a::len word)"
   1.663    by (fact mult_1 [symmetric, THEN iffD2 [OF of_nat_0 exI]])
   1.664  
   1.665 -lemma of_nat_gt_0: "of_nat k ~= 0 \<Longrightarrow> 0 < k"
   1.666 +lemma of_nat_gt_0: "of_nat k \<noteq> 0 \<Longrightarrow> 0 < k"
   1.667    by (cases k) auto
   1.668  
   1.669 -lemma of_nat_neq_0:
   1.670 -  "0 < k \<Longrightarrow> k < 2 ^ len_of TYPE('a::len) \<Longrightarrow> of_nat k ~= (0 :: 'a word)"
   1.671 -  by (clarsimp simp add : of_nat_0)
   1.672 -
   1.673 -lemma Abs_fnat_hom_add:
   1.674 -  "of_nat a + of_nat b = of_nat (a + b)"
   1.675 +lemma of_nat_neq_0: "0 < k \<Longrightarrow> k < 2 ^ len_of TYPE('a::len) \<Longrightarrow> of_nat k \<noteq> (0 :: 'a word)"
   1.676 +  by (auto simp add : of_nat_0)
   1.677 +
   1.678 +lemma Abs_fnat_hom_add: "of_nat a + of_nat b = of_nat (a + b)"
   1.679    by simp
   1.680  
   1.681 -lemma Abs_fnat_hom_mult:
   1.682 -  "of_nat a * of_nat b = (of_nat (a * b) :: 'a::len word)"
   1.683 +lemma Abs_fnat_hom_mult: "of_nat a * of_nat b = (of_nat (a * b) :: 'a::len word)"
   1.684    by (simp add: word_of_nat wi_hom_mult)
   1.685  
   1.686 -lemma Abs_fnat_hom_Suc:
   1.687 -  "word_succ (of_nat a) = of_nat (Suc a)"
   1.688 +lemma Abs_fnat_hom_Suc: "word_succ (of_nat a) = of_nat (Suc a)"
   1.689    by (simp add: word_of_nat wi_hom_succ ac_simps)
   1.690  
   1.691  lemma Abs_fnat_hom_0: "(0::'a::len word) = of_nat 0"
   1.692 @@ -1799,24 +1791,19 @@
   1.693    Abs_fnat_hom_add Abs_fnat_hom_mult Abs_fnat_hom_Suc
   1.694    Abs_fnat_hom_0 Abs_fnat_hom_1
   1.695  
   1.696 -lemma word_arith_nat_add:
   1.697 -  "a + b = of_nat (unat a + unat b)"
   1.698 +lemma word_arith_nat_add: "a + b = of_nat (unat a + unat b)"
   1.699 +  by simp
   1.700 +
   1.701 +lemma word_arith_nat_mult: "a * b = of_nat (unat a * unat b)"
   1.702    by simp
   1.703  
   1.704 -lemma word_arith_nat_mult:
   1.705 -  "a * b = of_nat (unat a * unat b)"
   1.706 -  by (simp add: of_nat_mult)
   1.707 -
   1.708 -lemma word_arith_nat_Suc:
   1.709 -  "word_succ a = of_nat (Suc (unat a))"
   1.710 +lemma word_arith_nat_Suc: "word_succ a = of_nat (Suc (unat a))"
   1.711    by (subst Abs_fnat_hom_Suc [symmetric]) simp
   1.712  
   1.713 -lemma word_arith_nat_div:
   1.714 -  "a div b = of_nat (unat a div unat b)"
   1.715 +lemma word_arith_nat_div: "a div b = of_nat (unat a div unat b)"
   1.716    by (simp add: word_div_def word_of_nat zdiv_int uint_nat)
   1.717  
   1.718 -lemma word_arith_nat_mod:
   1.719 -  "a mod b = of_nat (unat a mod unat b)"
   1.720 +lemma word_arith_nat_mod: "a mod b = of_nat (unat a mod unat b)"
   1.721    by (simp add: word_mod_def word_of_nat zmod_int uint_nat)
   1.722  
   1.723  lemmas word_arith_nat_defs =
   1.724 @@ -1835,31 +1822,32 @@
   1.725    [unfolded linorder_not_less [symmetric] Not_eq_iff]
   1.726  
   1.727  lemma unat_add_lem:
   1.728 -  "(unat x + unat y < 2 ^ len_of TYPE('a)) =
   1.729 -    (unat (x + y :: 'a::len word) = unat x + unat y)"
   1.730 -  unfolding unat_word_ariths
   1.731 -  by (auto intro!: trans [OF _ nat_mod_lem])
   1.732 +  "unat x + unat y < 2 ^ len_of TYPE('a) \<longleftrightarrow> unat (x + y) = unat x + unat y"
   1.733 +  for x y :: "'a::len word"
   1.734 +  by (auto simp: unat_word_ariths intro!: trans [OF _ nat_mod_lem])
   1.735  
   1.736  lemma unat_mult_lem:
   1.737 -  "(unat x * unat y < 2 ^ len_of TYPE('a)) =
   1.738 -    (unat (x * y :: 'a::len word) = unat x * unat y)"
   1.739 -  unfolding unat_word_ariths
   1.740 -  by (auto intro!: trans [OF _ nat_mod_lem])
   1.741 -
   1.742 -lemmas unat_plus_if' = trans [OF unat_word_ariths(1) mod_nat_add, simplified]
   1.743 -
   1.744 -lemma le_no_overflow:
   1.745 -  "x <= b \<Longrightarrow> a <= a + b \<Longrightarrow> x <= a + (b :: 'a::len0 word)"
   1.746 +  "unat x * unat y < 2 ^ len_of TYPE('a) \<longleftrightarrow>
   1.747 +    unat (x * y :: 'a::len word) = unat x * unat y"
   1.748 +  by (auto simp: unat_word_ariths intro!: trans [OF _ nat_mod_lem])
   1.749 +
   1.750 +lemmas unat_plus_if' =
   1.751 +  trans [OF unat_word_ariths(1) mod_nat_add, simplified]
   1.752 +
   1.753 +lemma le_no_overflow: "x \<le> b \<Longrightarrow> a \<le> a + b \<Longrightarrow> x \<le> a + b"
   1.754 +  for a b x :: "'a::len0 word"
   1.755    apply (erule order_trans)
   1.756    apply (erule olen_add_eqv [THEN iffD1])
   1.757    done
   1.758  
   1.759 -lemmas un_ui_le = trans [OF word_le_nat_alt [symmetric] word_le_def]
   1.760 +lemmas un_ui_le =
   1.761 +  trans [OF word_le_nat_alt [symmetric] word_le_def]
   1.762  
   1.763  lemma unat_sub_if_size:
   1.764 -  "unat (x - y) = (if unat y <= unat x
   1.765 -   then unat x - unat y
   1.766 -   else unat x + 2 ^ size x - unat y)"
   1.767 +  "unat (x - y) =
   1.768 +    (if unat y \<le> unat x
   1.769 +     then unat x - unat y
   1.770 +     else unat x + 2 ^ size x - unat y)"
   1.771    apply (unfold word_size)
   1.772    apply (simp add: un_ui_le)
   1.773    apply (auto simp add: unat_def uint_sub_if')
   1.774 @@ -1877,13 +1865,15 @@
   1.775  
   1.776  lemmas unat_sub_if' = unat_sub_if_size [unfolded word_size]
   1.777  
   1.778 -lemma unat_div: "unat ((x :: 'a::len word) div y) = unat x div unat y"
   1.779 +lemma unat_div: "unat (x div y) = unat x div unat y"
   1.780 +  for x y :: " 'a::len word"
   1.781    apply (simp add : unat_word_ariths)
   1.782    apply (rule unat_lt2p [THEN xtr7, THEN nat_mod_eq'])
   1.783    apply (rule div_le_dividend)
   1.784    done
   1.785  
   1.786 -lemma unat_mod: "unat ((x :: 'a::len word) mod y) = unat x mod unat y"
   1.787 +lemma unat_mod: "unat (x mod y) = unat x mod unat y"
   1.788 +  for x y :: "'a::len word"
   1.789    apply (clarsimp simp add : unat_word_ariths)
   1.790    apply (cases "unat y")
   1.791     prefer 2
   1.792 @@ -1892,25 +1882,23 @@
   1.793     apply auto
   1.794    done
   1.795  
   1.796 -lemma uint_div: "uint ((x :: 'a::len word) div y) = uint x div uint y"
   1.797 -  unfolding uint_nat by (simp add : unat_div zdiv_int)
   1.798 -
   1.799 -lemma uint_mod: "uint ((x :: 'a::len word) mod y) = uint x mod uint y"
   1.800 -  unfolding uint_nat by (simp add : unat_mod zmod_int)
   1.801 +lemma uint_div: "uint (x div y) = uint x div uint y"
   1.802 +  for x y :: "'a::len word"
   1.803 +  by (simp add: uint_nat unat_div zdiv_int)
   1.804 +
   1.805 +lemma uint_mod: "uint (x mod y) = uint x mod uint y"
   1.806 +  for x y :: "'a::len word"
   1.807 +  by (simp add: uint_nat unat_mod zmod_int)
   1.808  
   1.809  
   1.810  subsection \<open>Definition of \<open>unat_arith\<close> tactic\<close>
   1.811  
   1.812 -lemma unat_split:
   1.813 -  fixes x::"'a::len word"
   1.814 -  shows "P (unat x) =
   1.815 -         (ALL n. of_nat n = x & n < 2^len_of TYPE('a) --> P n)"
   1.816 +lemma unat_split: "P (unat x) \<longleftrightarrow> (\<forall>n. of_nat n = x \<and> n < 2^len_of TYPE('a) \<longrightarrow> P n)"
   1.817 +  for x :: "'a::len word"
   1.818    by (auto simp: unat_of_nat)
   1.819  
   1.820 -lemma unat_split_asm:
   1.821 -  fixes x::"'a::len word"
   1.822 -  shows "P (unat x) =
   1.823 -         (~(EX n. of_nat n = x & n < 2^len_of TYPE('a) & ~ P n))"
   1.824 +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)"
   1.825 +  for x :: "'a::len word"
   1.826    by (auto simp: unat_of_nat)
   1.827  
   1.828  lemmas of_nat_inverse =
   1.829 @@ -1958,25 +1946,26 @@
   1.830    \<open>Scan.succeed (SIMPLE_METHOD' o unat_arith_tac)\<close>
   1.831    "solving word arithmetic via natural numbers and arith"
   1.832  
   1.833 -lemma no_plus_overflow_unat_size:
   1.834 -  "((x :: 'a::len word) <= x + y) = (unat x + unat y < 2 ^ size x)"
   1.835 +lemma no_plus_overflow_unat_size: "x \<le> x + y \<longleftrightarrow> unat x + unat y < 2 ^ size x"
   1.836 +  for x y :: "'a::len word"
   1.837    unfolding word_size by unat_arith
   1.838  
   1.839 -lemmas no_olen_add_nat = no_plus_overflow_unat_size [unfolded word_size]
   1.840 -
   1.841 -lemmas unat_plus_simple = trans [OF no_olen_add_nat unat_add_lem]
   1.842 -
   1.843 -lemma word_div_mult:
   1.844 -  "(0 :: 'a::len word) < y \<Longrightarrow> unat x * unat y < 2 ^ len_of TYPE('a) \<Longrightarrow>
   1.845 -    x * y div y = x"
   1.846 +lemmas no_olen_add_nat =
   1.847 +  no_plus_overflow_unat_size [unfolded word_size]
   1.848 +
   1.849 +lemmas unat_plus_simple =
   1.850 +  trans [OF no_olen_add_nat unat_add_lem]
   1.851 +
   1.852 +lemma word_div_mult: "0 < y \<Longrightarrow> unat x * unat y < 2 ^ len_of TYPE('a) \<Longrightarrow> x * y div y = x"
   1.853 +  for x y :: "'a::len word"
   1.854    apply unat_arith
   1.855    apply clarsimp
   1.856    apply (subst unat_mult_lem [THEN iffD1])
   1.857 -  apply auto
   1.858 +   apply auto
   1.859    done
   1.860  
   1.861 -lemma div_lt': "(i :: 'a::len word) <= k div x \<Longrightarrow>
   1.862 -    unat i * unat x < 2 ^ len_of TYPE('a)"
   1.863 +lemma div_lt': "i \<le> k div x \<Longrightarrow> unat i * unat x < 2 ^ len_of TYPE('a)"
   1.864 +  for i k x :: "'a::len word"
   1.865    apply unat_arith
   1.866    apply clarsimp
   1.867    apply (drule mult_le_mono1)
   1.868 @@ -1986,7 +1975,8 @@
   1.869  
   1.870  lemmas div_lt'' = order_less_imp_le [THEN div_lt']
   1.871  
   1.872 -lemma div_lt_mult: "(i :: 'a::len word) < k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x < k"
   1.873 +lemma div_lt_mult: "i < k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x < k"
   1.874 +  for i k x :: "'a::len word"
   1.875    apply (frule div_lt'' [THEN unat_mult_lem [THEN iffD1]])
   1.876    apply (simp add: unat_arith_simps)
   1.877    apply (drule (1) mult_less_mono1)
   1.878 @@ -1994,8 +1984,8 @@
   1.879    apply (rule div_mult_le)
   1.880    done
   1.881  
   1.882 -lemma div_le_mult:
   1.883 -  "(i :: 'a::len word) <= k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x <= k"
   1.884 +lemma div_le_mult: "i \<le> k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x \<le> k"
   1.885 +  for i k x :: "'a::len word"
   1.886    apply (frule div_lt' [THEN unat_mult_lem [THEN iffD1]])
   1.887    apply (simp add: unat_arith_simps)
   1.888    apply (drule mult_le_mono1)
   1.889 @@ -2003,20 +1993,20 @@
   1.890    apply (rule div_mult_le)
   1.891    done
   1.892  
   1.893 -lemma div_lt_uint':
   1.894 -  "(i :: 'a::len word) <= k div x \<Longrightarrow> uint i * uint x < 2 ^ len_of TYPE('a)"
   1.895 +lemma div_lt_uint': "i \<le> k div x \<Longrightarrow> uint i * uint x < 2 ^ len_of TYPE('a)"
   1.896 +  for i k x :: "'a::len word"
   1.897    apply (unfold uint_nat)
   1.898    apply (drule div_lt')
   1.899 -  by (metis of_nat_less_iff of_nat_mult of_nat_numeral of_nat_power)
   1.900 +  apply (metis of_nat_less_iff of_nat_mult of_nat_numeral of_nat_power)
   1.901 +  done
   1.902  
   1.903  lemmas div_lt_uint'' = order_less_imp_le [THEN div_lt_uint']
   1.904  
   1.905 -lemma word_le_exists':
   1.906 -  "(x :: 'a::len0 word) <= y \<Longrightarrow>
   1.907 -    (EX z. y = x + z & uint x + uint z < 2 ^ len_of TYPE('a))"
   1.908 +lemma word_le_exists': "x \<le> y \<Longrightarrow> (\<exists>z. y = x + z \<and> uint x + uint z < 2 ^ len_of TYPE('a))"
   1.909 +  for x y z :: "'a::len0 word"
   1.910    apply (rule exI)
   1.911    apply (rule conjI)
   1.912 -  apply (rule zadd_diff_inverse)
   1.913 +   apply (rule zadd_diff_inverse)
   1.914    apply uint_arith
   1.915    done
   1.916  
   1.917 @@ -2038,8 +2028,8 @@
   1.918  
   1.919  lemmas uno_simps [THEN le_unat_uoi] = mod_le_divisor div_le_dividend dtle
   1.920  
   1.921 -lemma word_mod_div_equality:
   1.922 -  "(n div b) * b + (n mod b) = (n :: 'a::len word)"
   1.923 +lemma word_mod_div_equality: "(n div b) * b + (n mod b) = n"
   1.924 +  for n b :: "'a::len word"
   1.925    apply (unfold word_less_nat_alt word_arith_nat_defs)
   1.926    apply (cut_tac y="unat b" in gt_or_eq_0)
   1.927    apply (erule disjE)
   1.928 @@ -2047,7 +2037,8 @@
   1.929    apply simp
   1.930    done
   1.931  
   1.932 -lemma word_div_mult_le: "a div b * b <= (a::'a::len word)"
   1.933 +lemma word_div_mult_le: "a div b * b \<le> a"
   1.934 +  for a b :: "'a::len word"
   1.935    apply (unfold word_le_nat_alt word_arith_nat_defs)
   1.936    apply (cut_tac y="unat b" in gt_or_eq_0)
   1.937    apply (erule disjE)
   1.938 @@ -2055,17 +2046,16 @@
   1.939    apply simp
   1.940    done
   1.941  
   1.942 -lemma word_mod_less_divisor: "0 < n \<Longrightarrow> m mod n < (n :: 'a::len word)"
   1.943 +lemma word_mod_less_divisor: "0 < n \<Longrightarrow> m mod n < n"
   1.944 +  for m n :: "'a::len word"
   1.945    apply (simp only: word_less_nat_alt word_arith_nat_defs)
   1.946 -  apply (clarsimp simp add : uno_simps)
   1.947 +  apply (auto simp: uno_simps)
   1.948    done
   1.949  
   1.950 -lemma word_of_int_power_hom:
   1.951 -  "word_of_int a ^ n = (word_of_int (a ^ n) :: 'a::len word)"
   1.952 +lemma word_of_int_power_hom: "word_of_int a ^ n = (word_of_int (a ^ n) :: 'a::len word)"
   1.953    by (induct n) (simp_all add: wi_hom_mult [symmetric])
   1.954  
   1.955 -lemma word_arith_power_alt:
   1.956 -  "a ^ n = (word_of_int (uint a ^ n) :: 'a::len word)"
   1.957 +lemma word_arith_power_alt: "a ^ n = (word_of_int (uint a ^ n) :: 'a::len word)"
   1.958    by (simp add : word_of_int_power_hom [symmetric])
   1.959  
   1.960  lemma of_bl_length_less:
   1.961 @@ -2073,7 +2063,7 @@
   1.962    apply (unfold of_bl_def word_less_alt word_numeral_alt)
   1.963    apply safe
   1.964    apply (simp (no_asm) add: word_of_int_power_hom word_uint.eq_norm
   1.965 -                       del: word_of_int_numeral)
   1.966 +      del: word_of_int_numeral)
   1.967    apply (simp add: mod_pos_pos_trivial)
   1.968    apply (subst mod_pos_pos_trivial)
   1.969      apply (rule bl_to_bin_ge0)
   1.970 @@ -2092,9 +2082,9 @@
   1.971  lemma card_word: "CARD('a::len0 word) = 2 ^ len_of TYPE('a)"
   1.972    by (simp add: type_definition.card [OF type_definition_word] nat_power_eq)
   1.973  
   1.974 -lemma card_word_size:
   1.975 -  "card (UNIV :: 'a::len0 word set) = (2 ^ size (x :: 'a word))"
   1.976 -unfolding word_size by (rule card_word)
   1.977 +lemma card_word_size: "card (UNIV :: 'a word set) = (2 ^ size x)"
   1.978 +  for x :: "'a::len0 word"
   1.979 +  unfolding word_size by (rule card_word)
   1.980  
   1.981  
   1.982  subsection \<open>Bitwise Operations on Words\<close>
   1.983 @@ -2166,16 +2156,15 @@
   1.984    "x XOR (-1::'a::len0 word) = NOT x"
   1.985    by (transfer, simp)+
   1.986  
   1.987 -lemma uint_or: "uint (x OR y) = (uint x) OR (uint y)"
   1.988 +lemma uint_or: "uint (x OR y) = uint x OR uint y"
   1.989    by (transfer, simp add: bin_trunc_ao)
   1.990  
   1.991 -lemma uint_and: "uint (x AND y) = (uint x) AND (uint y)"
   1.992 +lemma uint_and: "uint (x AND y) = uint x AND uint y"
   1.993    by (transfer, simp add: bin_trunc_ao)
   1.994  
   1.995  lemma test_bit_wi [simp]:
   1.996 -  "(word_of_int x::'a::len0 word) !! n \<longleftrightarrow> n < len_of TYPE('a) \<and> bin_nth x n"
   1.997 -  unfolding word_test_bit_def
   1.998 -  by (simp add: word_ubin.eq_norm nth_bintr)
   1.999 +  "(word_of_int x :: 'a::len0 word) !! n \<longleftrightarrow> n < len_of TYPE('a) \<and> bin_nth x n"
  1.1000 +  by (simp add: word_test_bit_def word_ubin.eq_norm nth_bintr)
  1.1001  
  1.1002  lemma word_test_bit_transfer [transfer_rule]:
  1.1003    "(rel_fun pcr_word (rel_fun op = op =))
  1.1004 @@ -2183,17 +2172,18 @@
  1.1005    unfolding rel_fun_def word.pcr_cr_eq cr_word_def by simp
  1.1006  
  1.1007  lemma word_ops_nth_size:
  1.1008 -  "n < size (x::'a::len0 word) \<Longrightarrow>
  1.1009 -    (x OR y) !! n = (x !! n | y !! n) &
  1.1010 -    (x AND y) !! n = (x !! n & y !! n) &
  1.1011 -    (x XOR y) !! n = (x !! n ~= y !! n) &
  1.1012 -    (NOT x) !! n = (~ x !! n)"
  1.1013 +  "n < size x \<Longrightarrow>
  1.1014 +    (x OR y) !! n = (x !! n | y !! n) \<and>
  1.1015 +    (x AND y) !! n = (x !! n \<and> y !! n) \<and>
  1.1016 +    (x XOR y) !! n = (x !! n \<noteq> y !! n) \<and>
  1.1017 +    (NOT x) !! n = (\<not> x !! n)"
  1.1018 +  for x :: "'a::len0 word"
  1.1019    unfolding word_size by transfer (simp add: bin_nth_ops)
  1.1020  
  1.1021  lemma word_ao_nth:
  1.1022 -  fixes x :: "'a::len0 word"
  1.1023 -  shows "(x OR y) !! n = (x !! n | y !! n) &
  1.1024 -         (x AND y) !! n = (x !! n & y !! n)"
  1.1025 +  "(x OR y) !! n = (x !! n | y !! n) \<and>
  1.1026 +    (x AND y) !! n = (x !! n \<and> y !! n)"
  1.1027 +  for x :: "'a::len0 word"
  1.1028    by transfer (auto simp add: bin_nth_ops)
  1.1029  
  1.1030  lemma test_bit_numeral [simp]:
  1.1031 @@ -2206,13 +2196,13 @@
  1.1032      n < len_of TYPE('a) \<and> bin_nth (- numeral w) n"
  1.1033    by transfer (rule refl)
  1.1034  
  1.1035 -lemma test_bit_1 [simp]: "(1::'a::len word) !! n \<longleftrightarrow> n = 0"
  1.1036 +lemma test_bit_1 [simp]: "(1 :: 'a::len word) !! n \<longleftrightarrow> n = 0"
  1.1037    by transfer auto
  1.1038  
  1.1039 -lemma nth_0 [simp]: "~ (0::'a::len0 word) !! n"
  1.1040 +lemma nth_0 [simp]: "\<not> (0 :: 'a::len0 word) !! n"
  1.1041    by transfer simp
  1.1042  
  1.1043 -lemma nth_minus1 [simp]: "(-1::'a::len0 word) !! n \<longleftrightarrow> n < len_of TYPE('a)"
  1.1044 +lemma nth_minus1 [simp]: "(-1 :: 'a::len0 word) !! n \<longleftrightarrow> n < len_of TYPE('a)"
  1.1045    by transfer simp
  1.1046  
  1.1047  (* get from commutativity, associativity etc of int_and etc
  1.1048 @@ -2223,32 +2213,27 @@
  1.1049    word_wi_log_defs
  1.1050  
  1.1051  lemma word_bw_assocs:
  1.1052 -  fixes x :: "'a::len0 word"
  1.1053 -  shows
  1.1054    "(x AND y) AND z = x AND y AND z"
  1.1055    "(x OR y) OR z = x OR y OR z"
  1.1056    "(x XOR y) XOR z = x XOR y XOR z"
  1.1057 +  for x :: "'a::len0 word"
  1.1058    by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  1.1059  
  1.1060  lemma word_bw_comms:
  1.1061 -  fixes x :: "'a::len0 word"
  1.1062 -  shows
  1.1063    "x AND y = y AND x"
  1.1064    "x OR y = y OR x"
  1.1065    "x XOR y = y XOR x"
  1.1066 +  for x :: "'a::len0 word"
  1.1067    by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  1.1068  
  1.1069  lemma word_bw_lcs:
  1.1070 -  fixes x :: "'a::len0 word"
  1.1071 -  shows
  1.1072    "y AND x AND z = x AND y AND z"
  1.1073    "y OR x OR z = x OR y OR z"
  1.1074    "y XOR x XOR z = x XOR y XOR z"
  1.1075 +  for x :: "'a::len0 word"
  1.1076    by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  1.1077  
  1.1078  lemma word_log_esimps [simp]:
  1.1079 -  fixes x :: "'a::len0 word"
  1.1080 -  shows
  1.1081    "x AND 0 = 0"
  1.1082    "x AND -1 = x"
  1.1083    "x OR 0 = x"
  1.1084 @@ -2261,26 +2246,23 @@
  1.1085    "-1 OR x = -1"
  1.1086    "0 XOR x = x"
  1.1087    "-1 XOR x = NOT x"
  1.1088 +  for x :: "'a::len0 word"
  1.1089    by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  1.1090  
  1.1091  lemma word_not_dist:
  1.1092 -  fixes x :: "'a::len0 word"
  1.1093 -  shows
  1.1094    "NOT (x OR y) = NOT x AND NOT y"
  1.1095    "NOT (x AND y) = NOT x OR NOT y"
  1.1096 +  for x :: "'a::len0 word"
  1.1097    by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  1.1098  
  1.1099  lemma word_bw_same:
  1.1100 -  fixes x :: "'a::len0 word"
  1.1101 -  shows
  1.1102    "x AND x = x"
  1.1103    "x OR x = x"
  1.1104    "x XOR x = 0"
  1.1105 +  for x :: "'a::len0 word"
  1.1106    by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  1.1107  
  1.1108  lemma word_ao_absorbs [simp]:
  1.1109 -  fixes x :: "'a::len0 word"
  1.1110 -  shows
  1.1111    "x AND (y OR x) = x"
  1.1112    "x OR y AND x = x"
  1.1113    "x AND (x OR y) = x"
  1.1114 @@ -2289,47 +2271,44 @@
  1.1115    "x OR x AND y = x"
  1.1116    "(x OR y) AND x = x"
  1.1117    "x AND y OR x = x"
  1.1118 -  by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  1.1119 -
  1.1120 -lemma word_not_not [simp]:
  1.1121 -  "NOT NOT (x::'a::len0 word) = x"
  1.1122 +  for x :: "'a::len0 word"
  1.1123    by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  1.1124  
  1.1125 -lemma word_ao_dist:
  1.1126 -  fixes x :: "'a::len0 word"
  1.1127 -  shows "(x OR y) AND z = x AND z OR y AND z"
  1.1128 +lemma word_not_not [simp]: "NOT NOT x = x"
  1.1129 +  for x :: "'a::len0 word"
  1.1130    by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  1.1131  
  1.1132 -lemma word_oa_dist:
  1.1133 -  fixes x :: "'a::len0 word"
  1.1134 -  shows "x AND y OR z = (x OR z) AND (y OR z)"
  1.1135 +lemma word_ao_dist: "(x OR y) AND z = x AND z OR y AND z"
  1.1136 +  for x :: "'a::len0 word"
  1.1137    by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  1.1138  
  1.1139 -lemma word_add_not [simp]:
  1.1140 -  fixes x :: "'a::len0 word"
  1.1141 -  shows "x + NOT x = -1"
  1.1142 +lemma word_oa_dist: "x AND y OR z = (x OR z) AND (y OR z)"
  1.1143 +  for x :: "'a::len0 word"
  1.1144 +  by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  1.1145 +
  1.1146 +lemma word_add_not [simp]: "x + NOT x = -1"
  1.1147 +  for x :: "'a::len0 word"
  1.1148    by transfer (simp add: bin_add_not)
  1.1149  
  1.1150 -lemma word_plus_and_or [simp]:
  1.1151 -  fixes x :: "'a::len0 word"
  1.1152 -  shows "(x AND y) + (x OR y) = x + y"
  1.1153 +lemma word_plus_and_or [simp]: "(x AND y) + (x OR y) = x + y"
  1.1154 +  for x :: "'a::len0 word"
  1.1155    by transfer (simp add: plus_and_or)
  1.1156  
  1.1157 -lemma leoa:
  1.1158 -  fixes x :: "'a::len0 word"
  1.1159 -  shows "(w = (x OR y)) \<Longrightarrow> (y = (w AND y))" by auto
  1.1160 -lemma leao:
  1.1161 -  fixes x' :: "'a::len0 word"
  1.1162 -  shows "(w' = (x' AND y')) \<Longrightarrow> (x' = (x' OR w'))" by auto
  1.1163 -
  1.1164 -lemma word_ao_equiv:
  1.1165 -  fixes w w' :: "'a::len0 word"
  1.1166 -  shows "(w = w OR w') = (w' = w AND w')"
  1.1167 +lemma leoa: "w = x OR y \<Longrightarrow> y = w AND y"
  1.1168 +  for x :: "'a::len0 word"
  1.1169 +  by auto
  1.1170 +
  1.1171 +lemma leao: "w' = x' AND y' \<Longrightarrow> x' = x' OR w'"
  1.1172 +  for x' :: "'a::len0 word"
  1.1173 +  by auto
  1.1174 +
  1.1175 +lemma word_ao_equiv: "w = w OR w' \<longleftrightarrow> w' = w AND w'"
  1.1176 +  for w w' :: "'a::len0 word"
  1.1177    by (auto intro: leoa leao)
  1.1178  
  1.1179 -lemma le_word_or2: "x <= x OR (y::'a::len0 word)"
  1.1180 -  unfolding word_le_def uint_or
  1.1181 -  by (auto intro: le_int_or)
  1.1182 +lemma le_word_or2: "x \<le> x OR y"
  1.1183 +  for x y :: "'a::len0 word"
  1.1184 +  by (auto simp: word_le_def uint_or intro: le_int_or)
  1.1185  
  1.1186  lemmas le_word_or1 = xtr3 [OF word_bw_comms (2) le_word_or2]
  1.1187  lemmas word_and_le1 = xtr3 [OF word_ao_absorbs (4) [symmetric] le_word_or2]
  1.1188 @@ -2339,22 +2318,22 @@
  1.1189    unfolding to_bl_def word_log_defs bl_not_bin
  1.1190    by (simp add: word_ubin.eq_norm)
  1.1191  
  1.1192 -lemma bl_word_xor: "to_bl (v XOR w) = map2 op ~= (to_bl v) (to_bl w)"
  1.1193 +lemma bl_word_xor: "to_bl (v XOR w) = map2 op \<noteq> (to_bl v) (to_bl w)"
  1.1194    unfolding to_bl_def word_log_defs bl_xor_bin
  1.1195    by (simp add: word_ubin.eq_norm)
  1.1196  
  1.1197 -lemma bl_word_or: "to_bl (v OR w) = map2 op | (to_bl v) (to_bl w)"
  1.1198 +lemma bl_word_or: "to_bl (v OR w) = map2 op \<or> (to_bl v) (to_bl w)"
  1.1199    unfolding to_bl_def word_log_defs bl_or_bin
  1.1200    by (simp add: word_ubin.eq_norm)
  1.1201  
  1.1202 -lemma bl_word_and: "to_bl (v AND w) = map2 op & (to_bl v) (to_bl w)"
  1.1203 +lemma bl_word_and: "to_bl (v AND w) = map2 op \<and> (to_bl v) (to_bl w)"
  1.1204    unfolding to_bl_def word_log_defs bl_and_bin
  1.1205    by (simp add: word_ubin.eq_norm)
  1.1206  
  1.1207  lemma word_lsb_alt: "lsb (w::'a::len0 word) = test_bit w 0"
  1.1208    by (auto simp: word_test_bit_def word_lsb_def)
  1.1209  
  1.1210 -lemma word_lsb_1_0 [simp]: "lsb (1::'a::len word) & ~ lsb (0::'b::len0 word)"
  1.1211 +lemma word_lsb_1_0 [simp]: "lsb (1::'a::len word) \<and> \<not> lsb (0::'b::len0 word)"
  1.1212    unfolding word_lsb_def uint_eq_0 uint_1 by simp
  1.1213  
  1.1214  lemma word_lsb_last: "lsb (w::'a::len word) = last (to_bl w)"
  1.1215 @@ -2365,15 +2344,14 @@
  1.1216     apply (auto simp add: bin_to_bl_aux_alt)
  1.1217    done
  1.1218  
  1.1219 -lemma word_lsb_int: "lsb w = (uint w mod 2 = 1)"
  1.1220 -  unfolding word_lsb_def bin_last_def by auto
  1.1221 -
  1.1222 -lemma word_msb_sint: "msb w = (sint w < 0)"
  1.1223 -  unfolding word_msb_def sign_Min_lt_0 ..
  1.1224 -
  1.1225 -lemma msb_word_of_int:
  1.1226 -  "msb (word_of_int x::'a::len word) = bin_nth x (len_of TYPE('a) - 1)"
  1.1227 -  unfolding word_msb_def by (simp add: word_sbin.eq_norm bin_sign_lem)
  1.1228 +lemma word_lsb_int: "lsb w \<longleftrightarrow> uint w mod 2 = 1"
  1.1229 +  by (auto simp: word_lsb_def bin_last_def)
  1.1230 +
  1.1231 +lemma word_msb_sint: "msb w \<longleftrightarrow> sint w < 0"
  1.1232 +  by (simp only: word_msb_def sign_Min_lt_0)
  1.1233 +
  1.1234 +lemma msb_word_of_int: "msb (word_of_int x::'a::len word) = bin_nth x (len_of TYPE('a) - 1)"
  1.1235 +  by (simp add: word_msb_def word_sbin.eq_norm bin_sign_lem)
  1.1236  
  1.1237  lemma word_msb_numeral [simp]:
  1.1238    "msb (numeral w::'a::len word) = bin_nth (numeral w) (len_of TYPE('a) - 1)"
  1.1239 @@ -2384,30 +2362,30 @@
  1.1240    unfolding word_neg_numeral_alt by (rule msb_word_of_int)
  1.1241  
  1.1242  lemma word_msb_0 [simp]: "\<not> msb (0::'a::len word)"
  1.1243 -  unfolding word_msb_def by simp
  1.1244 +  by (simp add: word_msb_def)
  1.1245  
  1.1246  lemma word_msb_1 [simp]: "msb (1::'a::len word) \<longleftrightarrow> len_of TYPE('a) = 1"
  1.1247    unfolding word_1_wi msb_word_of_int eq_iff [where 'a=nat]
  1.1248    by (simp add: Suc_le_eq)
  1.1249  
  1.1250 -lemma word_msb_nth:
  1.1251 -  "msb (w::'a::len word) = bin_nth (uint w) (len_of TYPE('a) - 1)"
  1.1252 -  unfolding word_msb_def sint_uint by (simp add: bin_sign_lem)
  1.1253 -
  1.1254 -lemma word_msb_alt: "msb (w::'a::len word) = hd (to_bl w)"
  1.1255 +lemma word_msb_nth: "msb w = bin_nth (uint w) (len_of TYPE('a) - 1)"
  1.1256 +  for w :: "'a::len word"
  1.1257 +  by (simp add: word_msb_def sint_uint bin_sign_lem)
  1.1258 +
  1.1259 +lemma word_msb_alt: "msb w = hd (to_bl w)"
  1.1260 +  for w :: "'a::len word"
  1.1261    apply (unfold word_msb_nth uint_bl)
  1.1262    apply (subst hd_conv_nth)
  1.1263 -  apply (rule length_greater_0_conv [THEN iffD1])
  1.1264 +   apply (rule length_greater_0_conv [THEN iffD1])
  1.1265     apply simp
  1.1266    apply (simp add : nth_bin_to_bl word_size)
  1.1267    done
  1.1268  
  1.1269 -lemma word_set_nth [simp]:
  1.1270 -  "set_bit w n (test_bit w n) = (w::'a::len0 word)"
  1.1271 -  unfolding word_test_bit_def word_set_bit_def by auto
  1.1272 -
  1.1273 -lemma bin_nth_uint':
  1.1274 -  "bin_nth (uint w) n = (rev (bin_to_bl (size w) (uint w)) ! n & n < size w)"
  1.1275 +lemma word_set_nth [simp]: "set_bit w n (test_bit w n) = w"
  1.1276 +  for w :: "'a::len0 word"
  1.1277 +  by (auto simp: word_test_bit_def word_set_bit_def)
  1.1278 +
  1.1279 +lemma bin_nth_uint': "bin_nth (uint w) n \<longleftrightarrow> rev (bin_to_bl (size w) (uint w)) ! n \<and> n < size w"
  1.1280    apply (unfold word_size)
  1.1281    apply (safe elim!: bin_nth_uint_imp)
  1.1282     apply (frule bin_nth_uint_imp)
  1.1283 @@ -2416,9 +2394,8 @@
  1.1284  
  1.1285  lemmas bin_nth_uint = bin_nth_uint' [unfolded word_size]
  1.1286  
  1.1287 -lemma test_bit_bl: "w !! n = (rev (to_bl w) ! n & n < size w)"
  1.1288 -  unfolding to_bl_def word_test_bit_def word_size
  1.1289 -  by (rule bin_nth_uint)
  1.1290 +lemma test_bit_bl: "w !! n \<longleftrightarrow> rev (to_bl w) ! n \<and> n < size w"
  1.1291 +  unfolding to_bl_def word_test_bit_def word_size by (rule bin_nth_uint)
  1.1292  
  1.1293  lemma to_bl_nth: "n < size w \<Longrightarrow> to_bl w ! n = w !! (size w - Suc n)"
  1.1294    apply (unfold test_bit_bl)
  1.1295 @@ -2428,29 +2405,25 @@
  1.1296     apply (auto simp add: word_size)
  1.1297    done
  1.1298  
  1.1299 -lemma test_bit_set:
  1.1300 -  fixes w :: "'a::len0 word"
  1.1301 -  shows "(set_bit w n x) !! n = (n < size w & x)"
  1.1302 -  unfolding word_size word_test_bit_def word_set_bit_def
  1.1303 -  by (clarsimp simp add : word_ubin.eq_norm nth_bintr)
  1.1304 +lemma test_bit_set: "(set_bit w n x) !! n \<longleftrightarrow> n < size w \<and> x"
  1.1305 +  for w :: "'a::len0 word"
  1.1306 +  by (auto simp: word_size word_test_bit_def word_set_bit_def word_ubin.eq_norm nth_bintr)
  1.1307  
  1.1308  lemma test_bit_set_gen:
  1.1309 -  fixes w :: "'a::len0 word"
  1.1310 -  shows "test_bit (set_bit w n x) m =
  1.1311 -         (if m = n then n < size w & x else test_bit w m)"
  1.1312 +  "test_bit (set_bit w n x) m = (if m = n then n < size w \<and> x else test_bit w m)"
  1.1313 +  for w :: "'a::len0 word"
  1.1314    apply (unfold word_size word_test_bit_def word_set_bit_def)
  1.1315    apply (clarsimp simp add: word_ubin.eq_norm nth_bintr bin_nth_sc_gen)
  1.1316    apply (auto elim!: test_bit_size [unfolded word_size]
  1.1317 -              simp add: word_test_bit_def [symmetric])
  1.1318 +      simp add: word_test_bit_def [symmetric])
  1.1319    done
  1.1320  
  1.1321  lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs"
  1.1322    unfolding of_bl_def bl_to_bin_rep_F by auto
  1.1323  
  1.1324 -lemma msb_nth:
  1.1325 -  fixes w :: "'a::len word"
  1.1326 -  shows "msb w = w !! (len_of TYPE('a) - 1)"
  1.1327 -  unfolding word_msb_nth word_test_bit_def by simp
  1.1328 +lemma msb_nth: "msb w = w !! (len_of TYPE('a) - 1)"
  1.1329 +  for w :: "'a::len word"
  1.1330 +  by (simp add: word_msb_nth word_test_bit_def)
  1.1331  
  1.1332  lemmas msb0 = len_gt_0 [THEN diff_Suc_less, THEN word_ops_nth_size [unfolded word_size]]
  1.1333  lemmas msb1 = msb0 [where i = 0]
  1.1334 @@ -2460,8 +2433,9 @@
  1.1335  lemmas word_ops_lsb = lsb0 [unfolded word_lsb_alt]
  1.1336  
  1.1337  lemma td_ext_nth [OF refl refl refl, unfolded word_size]:
  1.1338 -  "n = size (w::'a::len0 word) \<Longrightarrow> ofn = set_bits \<Longrightarrow> [w, ofn g] = l \<Longrightarrow>
  1.1339 -    td_ext test_bit ofn {f. ALL i. f i --> i < n} (%h i. h i & i < n)"
  1.1340 +  "n = size w \<Longrightarrow> ofn = set_bits \<Longrightarrow> [w, ofn g] = l \<Longrightarrow>
  1.1341 +    td_ext test_bit ofn {f. \<forall>i. f i \<longrightarrow> i < n} (\<lambda>h i. h i \<and> i < n)"
  1.1342 +  for w :: "'a::len0 word"
  1.1343    apply (unfold word_size td_ext_def')
  1.1344    apply safe
  1.1345       apply (rule_tac [3] ext)
  1.1346 @@ -2472,38 +2446,38 @@
  1.1347         apply (clarsimp simp: word_bl.Abs_inverse)+
  1.1348    apply (rule word_bl.Rep_inverse')
  1.1349    apply (rule sym [THEN trans])
  1.1350 -  apply (rule bl_of_nth_nth)
  1.1351 +   apply (rule bl_of_nth_nth)
  1.1352    apply simp
  1.1353    apply (rule bl_of_nth_inj)
  1.1354    apply (clarsimp simp add : test_bit_bl word_size)
  1.1355    done
  1.1356  
  1.1357  interpretation test_bit:
  1.1358 -  td_ext "op !! :: 'a::len0 word => nat => bool"
  1.1359 -         set_bits
  1.1360 -         "{f. \<forall>i. f i \<longrightarrow> i < len_of TYPE('a::len0)}"
  1.1361 -         "(\<lambda>h i. h i \<and> i < len_of TYPE('a::len0))"
  1.1362 +  td_ext
  1.1363 +    "op !! :: 'a::len0 word \<Rightarrow> nat \<Rightarrow> bool"
  1.1364 +    set_bits
  1.1365 +    "{f. \<forall>i. f i \<longrightarrow> i < len_of TYPE('a::len0)}"
  1.1366 +    "(\<lambda>h i. h i \<and> i < len_of TYPE('a::len0))"
  1.1367    by (rule td_ext_nth)
  1.1368  
  1.1369  lemmas td_nth = test_bit.td_thm
  1.1370  
  1.1371 -lemma word_set_set_same [simp]:
  1.1372 -  fixes w :: "'a::len0 word"
  1.1373 -  shows "set_bit (set_bit w n x) n y = set_bit w n y"
  1.1374 +lemma word_set_set_same [simp]: "set_bit (set_bit w n x) n y = set_bit w n y"
  1.1375 +  for w :: "'a::len0 word"
  1.1376    by (rule word_eqI) (simp add : test_bit_set_gen word_size)
  1.1377  
  1.1378  lemma word_set_set_diff:
  1.1379    fixes w :: "'a::len0 word"
  1.1380 -  assumes "m ~= n"
  1.1381 +  assumes "m \<noteq> n"
  1.1382    shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x"
  1.1383 -  by (rule word_eqI) (clarsimp simp add: test_bit_set_gen word_size assms)
  1.1384 +  by (rule word_eqI) (auto simp: test_bit_set_gen word_size assms)
  1.1385  
  1.1386  lemma nth_sint:
  1.1387    fixes w :: "'a::len word"
  1.1388    defines "l \<equiv> len_of TYPE('a)"
  1.1389    shows "bin_nth (sint w) n = (if n < l - 1 then w !! n else w !! (l - 1))"
  1.1390    unfolding sint_uint l_def
  1.1391 -  by (clarsimp simp add: nth_sbintr word_test_bit_def [symmetric])
  1.1392 +  by (auto simp: nth_sbintr word_test_bit_def [symmetric])
  1.1393  
  1.1394  lemma word_lsb_numeral [simp]:
  1.1395    "lsb (numeral bin :: 'a::len word) \<longleftrightarrow> bin_last (numeral bin)"
  1.1396 @@ -2511,14 +2485,11 @@
  1.1397  
  1.1398  lemma word_lsb_neg_numeral [simp]:
  1.1399    "lsb (- numeral bin :: 'a::len word) \<longleftrightarrow> bin_last (- numeral bin)"
  1.1400 -  unfolding word_lsb_alt test_bit_neg_numeral by simp
  1.1401 -
  1.1402 -lemma set_bit_word_of_int:
  1.1403 -  "set_bit (word_of_int x) n b = word_of_int (bin_sc n b x)"
  1.1404 +  by (simp add: word_lsb_alt)
  1.1405 +
  1.1406 +lemma set_bit_word_of_int: "set_bit (word_of_int x) n b = word_of_int (bin_sc n b x)"
  1.1407    unfolding word_set_bit_def
  1.1408 -  apply (rule word_eqI)
  1.1409 -  apply (simp add: word_size bin_nth_sc_gen word_ubin.eq_norm nth_bintr)
  1.1410 -  done
  1.1411 +  by (rule word_eqI)(simp add: word_size bin_nth_sc_gen word_ubin.eq_norm nth_bintr)
  1.1412  
  1.1413  lemma word_set_numeral [simp]:
  1.1414    "set_bit (numeral bin::'a::len0 word) n b =
  1.1415 @@ -2530,24 +2501,20 @@
  1.1416      word_of_int (bin_sc n b (- numeral bin))"
  1.1417    unfolding word_neg_numeral_alt by (rule set_bit_word_of_int)
  1.1418  
  1.1419 -lemma word_set_bit_0 [simp]:
  1.1420 -  "set_bit 0 n b = word_of_int (bin_sc n b 0)"
  1.1421 +lemma word_set_bit_0 [simp]: "set_bit 0 n b = word_of_int (bin_sc n b 0)"
  1.1422    unfolding word_0_wi by (rule set_bit_word_of_int)
  1.1423  
  1.1424 -lemma word_set_bit_1 [simp]:
  1.1425 -  "set_bit 1 n b = word_of_int (bin_sc n b 1)"
  1.1426 +lemma word_set_bit_1 [simp]: "set_bit 1 n b = word_of_int (bin_sc n b 1)"
  1.1427    unfolding word_1_wi by (rule set_bit_word_of_int)
  1.1428  
  1.1429 -lemma setBit_no [simp]:
  1.1430 -  "setBit (numeral bin) n = word_of_int (bin_sc n True (numeral bin))"
  1.1431 +lemma setBit_no [simp]: "setBit (numeral bin) n = word_of_int (bin_sc n True (numeral bin))"
  1.1432    by (simp add: setBit_def)
  1.1433  
  1.1434  lemma clearBit_no [simp]:
  1.1435    "clearBit (numeral bin) n = word_of_int (bin_sc n False (numeral bin))"
  1.1436    by (simp add: clearBit_def)
  1.1437  
  1.1438 -lemma to_bl_n1:
  1.1439 -  "to_bl (-1::'a::len0 word) = replicate (len_of TYPE('a)) True"
  1.1440 +lemma to_bl_n1: "to_bl (-1::'a::len0 word) = replicate (len_of TYPE('a)) True"
  1.1441    apply (rule word_bl.Abs_inverse')
  1.1442     apply simp
  1.1443    apply (rule word_eqI)
  1.1444 @@ -2558,8 +2525,8 @@
  1.1445  lemma word_msb_n1 [simp]: "msb (-1::'a::len word)"
  1.1446    unfolding word_msb_alt to_bl_n1 by simp
  1.1447  
  1.1448 -lemma word_set_nth_iff:
  1.1449 -  "(set_bit w n b = w) = (w !! n = b | n >= size (w::'a::len0 word))"
  1.1450 +lemma word_set_nth_iff: "set_bit w n b = w \<longleftrightarrow> w !! n = b \<or> n \<ge> size w"
  1.1451 +  for w :: "'a::len0 word"
  1.1452    apply (rule iffI)
  1.1453     apply (rule disjCI)
  1.1454     apply (drule word_eqD)
  1.1455 @@ -2573,18 +2540,13 @@
  1.1456    apply force
  1.1457    done
  1.1458  
  1.1459 -lemma test_bit_2p:
  1.1460 -  "(word_of_int (2 ^ n)::'a::len word) !! m \<longleftrightarrow> m = n \<and> m < len_of TYPE('a)"
  1.1461 -  unfolding word_test_bit_def
  1.1462 -  by (auto simp add: word_ubin.eq_norm nth_bintr nth_2p_bin)
  1.1463 -
  1.1464 -lemma nth_w2p:
  1.1465 -  "((2::'a::len word) ^ n) !! m \<longleftrightarrow> m = n \<and> m < len_of TYPE('a::len)"
  1.1466 -  unfolding test_bit_2p [symmetric] word_of_int [symmetric]
  1.1467 -  by simp
  1.1468 -
  1.1469 -lemma uint_2p:
  1.1470 -  "(0::'a::len word) < 2 ^ n \<Longrightarrow> uint (2 ^ n::'a::len word) = 2 ^ n"
  1.1471 +lemma test_bit_2p: "(word_of_int (2 ^ n)::'a::len word) !! m \<longleftrightarrow> m = n \<and> m < len_of TYPE('a)"
  1.1472 +  by (auto simp: word_test_bit_def word_ubin.eq_norm nth_bintr nth_2p_bin)
  1.1473 +
  1.1474 +lemma nth_w2p: "((2::'a::len word) ^ n) !! m \<longleftrightarrow> m = n \<and> m < len_of TYPE('a::len)"
  1.1475 +  by (simp add: test_bit_2p [symmetric] word_of_int [symmetric])
  1.1476 +
  1.1477 +lemma uint_2p: "(0::'a::len word) < 2 ^ n \<Longrightarrow> uint (2 ^ n::'a::len word) = 2 ^ n"
  1.1478    apply (unfold word_arith_power_alt)
  1.1479    apply (case_tac "len_of TYPE('a)")
  1.1480     apply clarsimp
  1.1481 @@ -2595,37 +2557,36 @@
  1.1482     apply clarsimp
  1.1483    apply (drule word_gt_0 [THEN iffD1])
  1.1484    apply (safe intro!: word_eqI)
  1.1485 -  apply (auto simp add: nth_2p_bin)
  1.1486 +   apply (auto simp add: nth_2p_bin)
  1.1487    apply (erule notE)
  1.1488    apply (simp (no_asm_use) add: uint_word_of_int word_size)
  1.1489    apply (subst mod_pos_pos_trivial)
  1.1490 -  apply simp
  1.1491 -  apply (rule power_strict_increasing)
  1.1492 -  apply simp_all
  1.1493 +    apply simp
  1.1494 +   apply (rule power_strict_increasing)
  1.1495 +    apply simp_all
  1.1496    done
  1.1497  
  1.1498  lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a::len word) = 2 ^ n"
  1.1499    by (induct n) (simp_all add: wi_hom_syms)
  1.1500  
  1.1501 -lemma bang_is_le: "x !! m \<Longrightarrow> 2 ^ m <= (x :: 'a::len word)"
  1.1502 +lemma bang_is_le: "x !! m \<Longrightarrow> 2 ^ m \<le> x"
  1.1503 +  for x :: "'a::len word"
  1.1504    apply (rule xtr3)
  1.1505 -  apply (rule_tac [2] y = "x" in le_word_or2)
  1.1506 +   apply (rule_tac [2] y = "x" in le_word_or2)
  1.1507    apply (rule word_eqI)
  1.1508    apply (auto simp add: word_ao_nth nth_w2p word_size)
  1.1509    done
  1.1510  
  1.1511 -lemma word_clr_le:
  1.1512 -  fixes w :: "'a::len0 word"
  1.1513 -  shows "w >= set_bit w n False"
  1.1514 +lemma word_clr_le: "w \<ge> set_bit w n False"
  1.1515 +  for w :: "'a::len0 word"
  1.1516    apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
  1.1517    apply (rule order_trans)
  1.1518     apply (rule bintr_bin_clr_le)
  1.1519    apply simp
  1.1520    done
  1.1521  
  1.1522 -lemma word_set_ge:
  1.1523 -  fixes w :: "'a::len word"
  1.1524 -  shows "w <= set_bit w n True"
  1.1525 +lemma word_set_ge: "w \<le> set_bit w n True"
  1.1526 +  for w :: "'a::len word"
  1.1527    apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
  1.1528    apply (rule order_trans [OF _ bintr_bin_set_ge])
  1.1529    apply simp
  1.1530 @@ -2642,55 +2603,53 @@
  1.1531    apply simp
  1.1532    done
  1.1533  
  1.1534 -lemma shiftl1_numeral [simp]:
  1.1535 -  "shiftl1 (numeral w) = numeral (Num.Bit0 w)"
  1.1536 +lemma shiftl1_numeral [simp]: "shiftl1 (numeral w) = numeral (Num.Bit0 w)"
  1.1537    unfolding word_numeral_alt shiftl1_wi by simp
  1.1538  
  1.1539 -lemma shiftl1_neg_numeral [simp]:
  1.1540 -  "shiftl1 (- numeral w) = - numeral (Num.Bit0 w)"
  1.1541 +lemma shiftl1_neg_numeral [simp]: "shiftl1 (- numeral w) = - numeral (Num.Bit0 w)"
  1.1542    unfolding word_neg_numeral_alt shiftl1_wi by simp
  1.1543  
  1.1544  lemma shiftl1_0 [simp] : "shiftl1 0 = 0"
  1.1545 -  unfolding shiftl1_def by simp
  1.1546 +  by (simp add: shiftl1_def)
  1.1547  
  1.1548  lemma shiftl1_def_u: "shiftl1 w = word_of_int (uint w BIT False)"
  1.1549    by (simp only: shiftl1_def) (* FIXME: duplicate *)
  1.1550  
  1.1551  lemma shiftl1_def_s: "shiftl1 w = word_of_int (sint w BIT False)"
  1.1552 -  unfolding shiftl1_def Bit_B0 wi_hom_syms by simp
  1.1553 +  by (simp add: shiftl1_def Bit_B0 wi_hom_syms)
  1.1554  
  1.1555  lemma shiftr1_0 [simp]: "shiftr1 0 = 0"
  1.1556 -  unfolding shiftr1_def by simp
  1.1557 +  by (simp add: shiftr1_def)
  1.1558  
  1.1559  lemma sshiftr1_0 [simp]: "sshiftr1 0 = 0"
  1.1560 -  unfolding sshiftr1_def by simp
  1.1561 -
  1.1562 -lemma sshiftr1_n1 [simp] : "sshiftr1 (- 1) = - 1"
  1.1563 -  unfolding sshiftr1_def by simp
  1.1564 -
  1.1565 -lemma shiftl_0 [simp] : "(0::'a::len0 word) << n = 0"
  1.1566 -  unfolding shiftl_def by (induct n) auto
  1.1567 -
  1.1568 -lemma shiftr_0 [simp] : "(0::'a::len0 word) >> n = 0"
  1.1569 -  unfolding shiftr_def by (induct n) auto
  1.1570 -
  1.1571 -lemma sshiftr_0 [simp] : "0 >>> n = 0"
  1.1572 -  unfolding sshiftr_def by (induct n) auto
  1.1573 -
  1.1574 -lemma sshiftr_n1 [simp] : "-1 >>> n = -1"
  1.1575 -  unfolding sshiftr_def by (induct n) auto
  1.1576 -
  1.1577 -lemma nth_shiftl1: "shiftl1 w !! n = (n < size w & n > 0 & w !! (n - 1))"
  1.1578 +  by (simp add: sshiftr1_def)
  1.1579 +
  1.1580 +lemma sshiftr1_n1 [simp]: "sshiftr1 (- 1) = - 1"
  1.1581 +  by (simp add: sshiftr1_def)
  1.1582 +
  1.1583 +lemma shiftl_0 [simp]: "(0::'a::len0 word) << n = 0"
  1.1584 +  by (induct n) (auto simp: shiftl_def)
  1.1585 +
  1.1586 +lemma shiftr_0 [simp]: "(0::'a::len0 word) >> n = 0"
  1.1587 +  by (induct n) (auto simp: shiftr_def)
  1.1588 +
  1.1589 +lemma sshiftr_0 [simp]: "0 >>> n = 0"
  1.1590 +  by (induct n) (auto simp: sshiftr_def)
  1.1591 +
  1.1592 +lemma sshiftr_n1 [simp]: "-1 >>> n = -1"
  1.1593 +  by (induct n) (auto simp: sshiftr_def)
  1.1594 +
  1.1595 +lemma nth_shiftl1: "shiftl1 w !! n \<longleftrightarrow> n < size w \<and> n > 0 \<and> w !! (n - 1)"
  1.1596    apply (unfold shiftl1_def word_test_bit_def)
  1.1597    apply (simp add: nth_bintr word_ubin.eq_norm word_size)
  1.1598    apply (cases n)
  1.1599     apply auto
  1.1600    done
  1.1601  
  1.1602 -lemma nth_shiftl' [rule_format]:
  1.1603 -  "ALL n. ((w::'a::len0 word) << m) !! n = (n < size w & n >= m & w !! (n - m))"
  1.1604 +lemma nth_shiftl': "(w << m) !! n \<longleftrightarrow> n < size w \<and> n >= m \<and> w !! (n - m)"
  1.1605 +  for w :: "'a::len0 word"
  1.1606    apply (unfold shiftl_def)
  1.1607 -  apply (induct "m")
  1.1608 +  apply (induct m arbitrary: n)
  1.1609     apply (force elim!: test_bit_size)
  1.1610    apply (clarsimp simp add : nth_shiftl1 word_size)
  1.1611    apply arith
  1.1612 @@ -2706,11 +2665,11 @@
  1.1613    apply simp
  1.1614    done
  1.1615  
  1.1616 -lemma nth_shiftr:
  1.1617 -  "\<And>n. ((w::'a::len0 word) >> m) !! n = w !! (n + m)"
  1.1618 +lemma nth_shiftr: "(w >> m) !! n = w !! (n + m)"
  1.1619 +  for w :: "'a::len0 word"
  1.1620    apply (unfold shiftr_def)
  1.1621 -  apply (induct "m")
  1.1622 -   apply (auto simp add : nth_shiftr1)
  1.1623 +  apply (induct "m" arbitrary: n)
  1.1624 +   apply (auto simp add: nth_shiftr1)
  1.1625    done
  1.1626  
  1.1627  (* see paper page 10, (1), (2), shiftr1_def is of the form of (1),
  1.1628 @@ -2724,21 +2683,19 @@
  1.1629    apply simp
  1.1630    done
  1.1631  
  1.1632 -lemma nth_sshiftr1:
  1.1633 -  "sshiftr1 w !! n = (if n = size w - 1 then w !! n else w !! Suc n)"
  1.1634 +lemma nth_sshiftr1: "sshiftr1 w !! n = (if n = size w - 1 then w !! n else w !! Suc n)"
  1.1635    apply (unfold sshiftr1_def word_test_bit_def)
  1.1636 -  apply (simp add: nth_bintr word_ubin.eq_norm
  1.1637 -                   bin_nth.Suc [symmetric] word_size
  1.1638 -             del: bin_nth.simps)
  1.1639 +  apply (simp add: nth_bintr word_ubin.eq_norm bin_nth.Suc [symmetric] word_size
  1.1640 +      del: bin_nth.simps)
  1.1641    apply (simp add: nth_bintr uint_sint del : bin_nth.simps)
  1.1642    apply (auto simp add: bin_nth_sint)
  1.1643    done
  1.1644  
  1.1645  lemma nth_sshiftr [rule_format] :
  1.1646 -  "ALL n. sshiftr w m !! n = (n < size w &
  1.1647 -    (if n + m >= size w then w !! (size w - 1) else w !! (n + m)))"
  1.1648 +  "\<forall>n. sshiftr w m !! n =
  1.1649 +    (n < size w \<and> (if n + m \<ge> size w then w !! (size w - 1) else w !! (n + m)))"
  1.1650    apply (unfold sshiftr_def)
  1.1651 -  apply (induct_tac "m")
  1.1652 +  apply (induct_tac m)
  1.1653     apply (simp add: test_bit_bl)
  1.1654    apply (clarsimp simp add: nth_sshiftr1 word_size)
  1.1655    apply safe
  1.1656 @@ -2781,18 +2738,16 @@
  1.1657  
  1.1658  lemma shiftr_div_2n: "uint (shiftr w n) = uint w div 2 ^ n"
  1.1659    apply (unfold shiftr_def)
  1.1660 -  apply (induct "n")
  1.1661 +  apply (induct n)
  1.1662     apply simp
  1.1663 -  apply (simp add: shiftr1_div_2 mult.commute
  1.1664 -                   zdiv_zmult2_eq [symmetric])
  1.1665 +  apply (simp add: shiftr1_div_2 mult.commute zdiv_zmult2_eq [symmetric])
  1.1666    done
  1.1667  
  1.1668  lemma sshiftr_div_2n: "sint (sshiftr w n) = sint w div 2 ^ n"
  1.1669    apply (unfold sshiftr_def)
  1.1670 -  apply (induct "n")
  1.1671 +  apply (induct n)
  1.1672     apply simp
  1.1673 -  apply (simp add: sshiftr1_div_2 mult.commute
  1.1674 -                   zdiv_zmult2_eq [symmetric])
  1.1675 +  apply (simp add: sshiftr1_div_2 mult.commute zdiv_zmult2_eq [symmetric])
  1.1676    done
  1.1677  
  1.1678  
  1.1679 @@ -2809,22 +2764,20 @@
  1.1680  
  1.1681  lemma shiftl1_bl: "shiftl1 (w::'a::len0 word) = of_bl (to_bl w @ [False])"
  1.1682  proof -
  1.1683 -  have "shiftl1 w = shiftl1 (of_bl (to_bl w))" by simp
  1.1684 -  also have "\<dots> = of_bl (to_bl w @ [False])" by (rule shiftl1_of_bl)
  1.1685 +  have "shiftl1 w = shiftl1 (of_bl (to_bl w))"
  1.1686 +    by simp
  1.1687 +  also have "\<dots> = of_bl (to_bl w @ [False])"
  1.1688 +    by (rule shiftl1_of_bl)
  1.1689    finally show ?thesis .
  1.1690  qed
  1.1691  
  1.1692 -lemma bl_shiftl1:
  1.1693 -  "to_bl (shiftl1 (w :: 'a::len word)) = tl (to_bl w) @ [False]"
  1.1694 -  apply (simp add: shiftl1_bl word_rep_drop drop_Suc drop_Cons')
  1.1695 -  apply (fast intro!: Suc_leI)
  1.1696 -  done
  1.1697 +lemma bl_shiftl1: "to_bl (shiftl1 w) = tl (to_bl w) @ [False]"
  1.1698 +  for w :: "'a::len word"
  1.1699 +  by (simp add: shiftl1_bl word_rep_drop drop_Suc drop_Cons') (fast intro!: Suc_leI)
  1.1700  
  1.1701  (* Generalized version of bl_shiftl1. Maybe this one should replace it? *)
  1.1702 -lemma bl_shiftl1':
  1.1703 -  "to_bl (shiftl1 w) = tl (to_bl w @ [False])"
  1.1704 -  unfolding shiftl1_bl
  1.1705 -  by (simp add: word_rep_drop drop_Suc del: drop_append)
  1.1706 +lemma bl_shiftl1': "to_bl (shiftl1 w) = tl (to_bl w @ [False])"
  1.1707 +  by (simp add: shiftl1_bl word_rep_drop drop_Suc del: drop_append)
  1.1708  
  1.1709  lemma shiftr1_bl: "shiftr1 w = of_bl (butlast (to_bl w))"
  1.1710    apply (unfold shiftr1_def uint_bl of_bl_def)
  1.1711 @@ -2832,21 +2785,18 @@
  1.1712    apply (simp add: bin_rest_trunc [symmetric, unfolded One_nat_def])
  1.1713    done
  1.1714  
  1.1715 -lemma bl_shiftr1:
  1.1716 -  "to_bl (shiftr1 (w :: 'a::len word)) = False # butlast (to_bl w)"
  1.1717 -  unfolding shiftr1_bl
  1.1718 -  by (simp add : word_rep_drop len_gt_0 [THEN Suc_leI])
  1.1719 +lemma bl_shiftr1: "to_bl (shiftr1 w) = False # butlast (to_bl w)"
  1.1720 +  for w :: "'a::len word"
  1.1721 +  by (simp add: shiftr1_bl word_rep_drop len_gt_0 [THEN Suc_leI])
  1.1722  
  1.1723  (* Generalized version of bl_shiftr1. Maybe this one should replace it? *)
  1.1724 -lemma bl_shiftr1':
  1.1725 -  "to_bl (shiftr1 w) = butlast (False # to_bl w)"
  1.1726 +lemma bl_shiftr1': "to_bl (shiftr1 w) = butlast (False # to_bl w)"
  1.1727    apply (rule word_bl.Abs_inverse')
  1.1728 -  apply (simp del: butlast.simps)
  1.1729 +   apply (simp del: butlast.simps)
  1.1730    apply (simp add: shiftr1_bl of_bl_def)
  1.1731    done
  1.1732  
  1.1733 -lemma shiftl1_rev:
  1.1734 -  "shiftl1 w = word_reverse (shiftr1 (word_reverse w))"
  1.1735 +lemma shiftl1_rev: "shiftl1 w = word_reverse (shiftr1 (word_reverse w))"
  1.1736    apply (unfold word_reverse_def)
  1.1737    apply (rule word_bl.Rep_inverse' [symmetric])
  1.1738    apply (simp add: bl_shiftl1' bl_shiftr1' word_bl.Abs_inverse)
  1.1739 @@ -2854,12 +2804,8 @@
  1.1740     apply auto
  1.1741    done
  1.1742  
  1.1743 -lemma shiftl_rev:
  1.1744 -  "shiftl w n = word_reverse (shiftr (word_reverse w) n)"
  1.1745 -  apply (unfold shiftl_def shiftr_def)
  1.1746 -  apply (induct "n")
  1.1747 -   apply (auto simp add : shiftl1_rev)
  1.1748 -  done
  1.1749 +lemma shiftl_rev: "shiftl w n = word_reverse (shiftr (word_reverse w) n)"
  1.1750 +  by (induct n) (auto simp add: shiftl_def shiftr_def shiftl1_rev)
  1.1751  
  1.1752  lemma rev_shiftl: "word_reverse w << n = word_reverse (w >> n)"
  1.1753    by (simp add: shiftl_rev)
  1.1754 @@ -2870,8 +2816,8 @@
  1.1755  lemma rev_shiftr: "word_reverse w >> n = word_reverse (w << n)"
  1.1756    by (simp add: shiftr_rev)
  1.1757  
  1.1758 -lemma bl_sshiftr1:
  1.1759 -  "to_bl (sshiftr1 (w :: 'a::len word)) = hd (to_bl w) # butlast (to_bl w)"
  1.1760 +lemma bl_sshiftr1: "to_bl (sshiftr1 w) = hd (to_bl w) # butlast (to_bl w)"
  1.1761 +  for w :: "'a::len word"
  1.1762    apply (unfold sshiftr1_def uint_bl word_size)
  1.1763    apply (simp add: butlast_rest_bin word_ubin.eq_norm)
  1.1764    apply (simp add: sint_uint)
  1.1765 @@ -2880,55 +2826,54 @@
  1.1766    apply clarsimp
  1.1767    apply (case_tac i)
  1.1768     apply (simp_all add: hd_conv_nth length_0_conv [symmetric]
  1.1769 -                        nth_bin_to_bl bin_nth.Suc [symmetric]
  1.1770 -                        nth_sbintr
  1.1771 -                   del: bin_nth.Suc)
  1.1772 +      nth_bin_to_bl bin_nth.Suc [symmetric] nth_sbintr
  1.1773 +      del: bin_nth.Suc)
  1.1774     apply force
  1.1775    apply (rule impI)
  1.1776    apply (rule_tac f = "bin_nth (uint w)" in arg_cong)
  1.1777    apply simp
  1.1778    done
  1.1779  
  1.1780 -lemma drop_shiftr:
  1.1781 -  "drop n (to_bl ((w :: 'a::len word) >> n)) = take (size w - n) (to_bl w)"
  1.1782 +lemma drop_shiftr: "drop n (to_bl (w >> n)) = take (size w - n) (to_bl w)"
  1.1783 +  for w :: "'a::len word"
  1.1784    apply (unfold shiftr_def)
  1.1785    apply (induct n)
  1.1786     prefer 2
  1.1787     apply (simp add: drop_Suc bl_shiftr1 butlast_drop [symmetric])
  1.1788     apply (rule butlast_take [THEN trans])
  1.1789 -  apply (auto simp: word_size)
  1.1790 +    apply (auto simp: word_size)
  1.1791    done
  1.1792  
  1.1793 -lemma drop_sshiftr:
  1.1794 -  "drop n (to_bl ((w :: 'a::len word) >>> n)) = take (size w - n) (to_bl w)"
  1.1795 +lemma drop_sshiftr: "drop n (to_bl (w >>> n)) = take (size w - n) (to_bl w)"
  1.1796 +  for w :: "'a::len word"
  1.1797    apply (unfold sshiftr_def)
  1.1798    apply (induct n)
  1.1799     prefer 2
  1.1800     apply (simp add: drop_Suc bl_sshiftr1 butlast_drop [symmetric])
  1.1801     apply (rule butlast_take [THEN trans])
  1.1802 -  apply (auto simp: word_size)
  1.1803 +    apply (auto simp: word_size)
  1.1804    done
  1.1805  
  1.1806 -lemma take_shiftr:
  1.1807 -  "n \<le> size w \<Longrightarrow> take n (to_bl (w >> n)) = replicate n False"
  1.1808 +lemma take_shiftr: "n \<le> size w \<Longrightarrow> take n (to_bl (w >> n)) = replicate n False"
  1.1809    apply (unfold shiftr_def)
  1.1810    apply (induct n)
  1.1811     prefer 2
  1.1812     apply (simp add: bl_shiftr1' length_0_conv [symmetric] word_size)
  1.1813     apply (rule take_butlast [THEN trans])
  1.1814 -  apply (auto simp: word_size)
  1.1815 +    apply (auto simp: word_size)
  1.1816    done
  1.1817  
  1.1818  lemma take_sshiftr' [rule_format] :
  1.1819 -  "n <= size (w :: 'a::len word) --> hd (to_bl (w >>> n)) = hd (to_bl w) &
  1.1820 +  "n \<le> size w \<longrightarrow> hd (to_bl (w >>> n)) = hd (to_bl w) \<and>
  1.1821      take n (to_bl (w >>> n)) = replicate n (hd (to_bl w))"
  1.1822 +  for w :: "'a::len word"
  1.1823    apply (unfold sshiftr_def)
  1.1824    apply (induct n)
  1.1825     prefer 2
  1.1826     apply (simp add: bl_sshiftr1)
  1.1827     apply (rule impI)
  1.1828     apply (rule take_butlast [THEN trans])
  1.1829 -  apply (auto simp: word_size)
  1.1830 +    apply (auto simp: word_size)
  1.1831    done
  1.1832  
  1.1833  lemmas hd_sshiftr = take_sshiftr' [THEN conjunct1]
  1.1834 @@ -2941,26 +2886,25 @@
  1.1835  lemmas bl_sshiftr = atd_lem [OF take_sshiftr drop_sshiftr]
  1.1836  
  1.1837  lemma shiftl_of_bl: "of_bl bl << n = of_bl (bl @ replicate n False)"
  1.1838 -  unfolding shiftl_def
  1.1839 -  by (induct n) (auto simp: shiftl1_of_bl replicate_app_Cons_same)
  1.1840 -
  1.1841 -lemma shiftl_bl:
  1.1842 -  "(w::'a::len0 word) << (n::nat) = of_bl (to_bl w @ replicate n False)"
  1.1843 +  by (induct n) (auto simp: shiftl_def shiftl1_of_bl replicate_app_Cons_same)
  1.1844 +
  1.1845 +lemma shiftl_bl: "w << n = of_bl (to_bl w @ replicate n False)"
  1.1846 +  for w :: "'a::len0 word"
  1.1847  proof -
  1.1848 -  have "w << n = of_bl (to_bl w) << n" by simp
  1.1849 -  also have "\<dots> = of_bl (to_bl w @ replicate n False)" by (rule shiftl_of_bl)
  1.1850 +  have "w << n = of_bl (to_bl w) << n"
  1.1851 +    by simp
  1.1852 +  also have "\<dots> = of_bl (to_bl w @ replicate n False)"
  1.1853 +    by (rule shiftl_of_bl)
  1.1854    finally show ?thesis .
  1.1855  qed
  1.1856  
  1.1857  lemmas shiftl_numeral [simp] = shiftl_def [where w="numeral w"] for w
  1.1858  
  1.1859 -lemma bl_shiftl:
  1.1860 -  "to_bl (w << n) = drop n (to_bl w) @ replicate (min (size w) n) False"
  1.1861 +lemma bl_shiftl: "to_bl (w << n) = drop n (to_bl w) @ replicate (min (size w) n) False"
  1.1862    by (simp add: shiftl_bl word_rep_drop word_size)
  1.1863  
  1.1864 -lemma shiftl_zero_size:
  1.1865 -  fixes x :: "'a::len0 word"
  1.1866 -  shows "size x <= n \<Longrightarrow> x << n = 0"
  1.1867 +lemma shiftl_zero_size: "size x \<le> n \<Longrightarrow> x << n = 0"
  1.1868 +  for x :: "'a::len0 word"
  1.1869    apply (unfold word_size)
  1.1870    apply (rule word_eqI)
  1.1871    apply (clarsimp simp add: shiftl_bl word_size test_bit_of_bl nth_append)
  1.1872 @@ -2968,35 +2912,33 @@
  1.1873  
  1.1874  (* note - the following results use 'a::len word < number_ring *)
  1.1875  
  1.1876 -lemma shiftl1_2t: "shiftl1 (w :: 'a::len word) = 2 * w"
  1.1877 +lemma shiftl1_2t: "shiftl1 w = 2 * w"
  1.1878 +  for w :: "'a::len word"
  1.1879    by (simp add: shiftl1_def Bit_def wi_hom_mult [symmetric])
  1.1880  
  1.1881 -lemma shiftl1_p: "shiftl1 (w :: 'a::len word) = w + w"
  1.1882 +lemma shiftl1_p: "shiftl1 w = w + w"
  1.1883 +  for w :: "'a::len word"
  1.1884    by (simp add: shiftl1_2t)
  1.1885  
  1.1886 -lemma shiftl_t2n: "shiftl (w :: 'a::len word) n = 2 ^ n * w"
  1.1887 -  unfolding shiftl_def
  1.1888 -  by (induct n) (auto simp: shiftl1_2t)
  1.1889 +lemma shiftl_t2n: "shiftl w n = 2 ^ n * w"
  1.1890 +  for w :: "'a::len word"
  1.1891 +  by (induct n) (auto simp: shiftl_def shiftl1_2t)
  1.1892  
  1.1893  lemma shiftr1_bintr [simp]:
  1.1894    "(shiftr1 (numeral w) :: 'a::len0 word) =
  1.1895      word_of_int (bin_rest (bintrunc (len_of TYPE('a)) (numeral w)))"
  1.1896 -  unfolding shiftr1_def word_numeral_alt
  1.1897 -  by (simp add: word_ubin.eq_norm)
  1.1898 +  unfolding shiftr1_def word_numeral_alt by (simp add: word_ubin.eq_norm)
  1.1899  
  1.1900  lemma sshiftr1_sbintr [simp]:
  1.1901    "(sshiftr1 (numeral w) :: 'a::len word) =
  1.1902      word_of_int (bin_rest (sbintrunc (len_of TYPE('a) - 1) (numeral w)))"
  1.1903 -  unfolding sshiftr1_def word_numeral_alt
  1.1904 -  by (simp add: word_sbin.eq_norm)
  1.1905 +  unfolding sshiftr1_def word_numeral_alt by (simp add: word_sbin.eq_norm)
  1.1906  
  1.1907  lemma shiftr_no [simp]:
  1.1908    (* FIXME: neg_numeral *)
  1.1909    "(numeral w::'a::len0 word) >> n = word_of_int
  1.1910      ((bin_rest ^^ n) (bintrunc (len_of TYPE('a)) (numeral w)))"
  1.1911 -  apply (rule word_eqI)
  1.1912 -  apply (auto simp: nth_shiftr nth_rest_power_bin nth_bintr word_size)
  1.1913 -  done
  1.1914 +  by (rule word_eqI) (auto simp: nth_shiftr nth_rest_power_bin nth_bintr word_size)
  1.1915  
  1.1916  lemma sshiftr_no [simp]:
  1.1917    (* FIXME: neg_numeral *)
  1.1918 @@ -3010,8 +2952,7 @@
  1.1919  lemma shiftr1_bl_of:
  1.1920    "length bl \<le> len_of TYPE('a) \<Longrightarrow>
  1.1921      shiftr1 (of_bl bl::'a::len0 word) = of_bl (butlast bl)"
  1.1922 -  by (clarsimp simp: shiftr1_def of_bl_def butlast_rest_bl2bin
  1.1923 -                     word_ubin.eq_norm trunc_bl2bin)
  1.1924 +  by (clarsimp simp: shiftr1_def of_bl_def butlast_rest_bl2bin word_ubin.eq_norm trunc_bl2bin)
  1.1925  
  1.1926  lemma shiftr_bl_of:
  1.1927    "length bl \<le> len_of TYPE('a) \<Longrightarrow>
  1.1928 @@ -3025,53 +2966,57 @@
  1.1929    apply (simp add: butlast_take)
  1.1930    done
  1.1931  
  1.1932 -lemma shiftr_bl:
  1.1933 -  "(x::'a::len0 word) >> n \<equiv> of_bl (take (len_of TYPE('a) - n) (to_bl x))"
  1.1934 +lemma shiftr_bl: "x >> n \<equiv> of_bl (take (len_of TYPE('a) - n) (to_bl x))"
  1.1935 +  for x :: "'a::len0 word"
  1.1936    using shiftr_bl_of [where 'a='a, of "to_bl x"] by simp
  1.1937  
  1.1938 -lemma msb_shift:
  1.1939 -  "msb (w::'a::len word) \<longleftrightarrow> (w >> (len_of TYPE('a) - 1)) \<noteq> 0"
  1.1940 +lemma msb_shift: "msb w \<longleftrightarrow> (w >> (len_of TYPE('a) - 1)) \<noteq> 0"
  1.1941 +  for w :: "'a::len word"
  1.1942    apply (unfold shiftr_bl word_msb_alt)
  1.1943    apply (simp add: word_size Suc_le_eq take_Suc)
  1.1944    apply (cases "hd (to_bl w)")
  1.1945 -   apply (auto simp: word_1_bl
  1.1946 -                     of_bl_rep_False [where n=1 and bs="[]", simplified])
  1.1947 +   apply (auto simp: word_1_bl of_bl_rep_False [where n=1 and bs="[]", simplified])
  1.1948    done
  1.1949  
  1.1950 -lemma zip_replicate:
  1.1951 -  "n \<ge> length ys \<Longrightarrow> zip (replicate n x) ys = map (\<lambda>y. (x, y)) ys"
  1.1952 -  apply (induct ys arbitrary: n, simp_all)
  1.1953 -  apply (case_tac n, simp_all)
  1.1954 +lemma zip_replicate: "n \<ge> length ys \<Longrightarrow> zip (replicate n x) ys = map (\<lambda>y. (x, y)) ys"
  1.1955 +  apply (induct ys arbitrary: n)
  1.1956 +   apply simp_all
  1.1957 +  apply (case_tac n)
  1.1958 +   apply simp_all
  1.1959    done
  1.1960  
  1.1961  lemma align_lem_or [rule_format] :
  1.1962 -  "ALL x m. length x = n + m --> length y = n + m -->
  1.1963 -    drop m x = replicate n False --> take m y = replicate m False -->
  1.1964 +  "\<forall>x m. length x = n + m \<longrightarrow> length y = n + m \<longrightarrow>
  1.1965 +    drop m x = replicate n False \<longrightarrow> take m y = replicate m False \<longrightarrow>
  1.1966      map2 op | x y = take m x @ drop m y"
  1.1967 -  apply (induct_tac y)
  1.1968 +  apply (induct y)
  1.1969     apply force
  1.1970    apply clarsimp
  1.1971 -  apply (case_tac x, force)
  1.1972 -  apply (case_tac m, auto)
  1.1973 +  apply (case_tac x)
  1.1974 +   apply force
  1.1975 +  apply (case_tac m)
  1.1976 +   apply auto
  1.1977    apply (drule_tac t="length xs" for xs in sym)
  1.1978 -  apply (clarsimp simp: map2_def zip_replicate o_def)
  1.1979 +  apply (auto simp: map2_def zip_replicate o_def)
  1.1980    done
  1.1981  
  1.1982  lemma align_lem_and [rule_format] :
  1.1983 -  "ALL x m. length x = n + m --> length y = n + m -->
  1.1984 -    drop m x = replicate n False --> take m y = replicate m False -->
  1.1985 -    map2 op & x y = replicate (n + m) False"
  1.1986 -  apply (induct_tac y)
  1.1987 +  "\<forall>x m. length x = n + m \<longrightarrow> length y = n + m \<longrightarrow>
  1.1988 +    drop m x = replicate n False \<longrightarrow> take m y = replicate m False \<longrightarrow>
  1.1989 +    map2 op \<and> x y = replicate (n + m) False"
  1.1990 +  apply (induct y)
  1.1991     apply force
  1.1992    apply clarsimp
  1.1993 -  apply (case_tac x, force)
  1.1994 -  apply (case_tac m, auto)
  1.1995 +  apply (case_tac x)
  1.1996 +   apply force
  1.1997 +  apply (case_tac m)
  1.1998 +  apply auto
  1.1999    apply (drule_tac t="length xs" for xs in sym)
  1.2000 -  apply (clarsimp simp: map2_def zip_replicate o_def map_replicate_const)
  1.2001 +  apply (auto simp: map2_def zip_replicate o_def map_replicate_const)
  1.2002    done
  1.2003  
  1.2004  lemma aligned_bl_add_size [OF refl]:
  1.2005 -  "size x - n = m \<Longrightarrow> n <= size x \<Longrightarrow> drop m (to_bl x) = replicate n False \<Longrightarrow>
  1.2006 +  "size x - n = m \<Longrightarrow> n \<le> size x \<Longrightarrow> drop m (to_bl x) = replicate n False \<Longrightarrow>
  1.2007      take m (to_bl y) = replicate m False \<Longrightarrow>
  1.2008      to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)"
  1.2009    apply (subgoal_tac "x AND y = 0")
  1.2010 @@ -3090,8 +3035,7 @@
  1.2011  
  1.2012  subsubsection \<open>Mask\<close>
  1.2013  
  1.2014 -lemma nth_mask [OF refl, simp]:
  1.2015 -  "m = mask n \<Longrightarrow> test_bit m i = (i < n & i < size m)"
  1.2016 +lemma nth_mask [OF refl, simp]: "m = mask n \<Longrightarrow> test_bit m i \<longleftrightarrow> i < n \<and> i < size m"
  1.2017    apply (unfold mask_def test_bit_bl)
  1.2018    apply (simp only: word_1_bl [symmetric] shiftl_of_bl)
  1.2019    apply (clarsimp simp add: word_size)
  1.2020 @@ -3117,7 +3061,8 @@
  1.2021  lemma and_mask_wi: "word_of_int i AND mask n = word_of_int (bintrunc n i)"
  1.2022    by (auto simp add: nth_bintr word_size word_ops_nth_size word_eq_iff)
  1.2023  
  1.2024 -lemma and_mask_wi': "word_of_int i AND mask n = (word_of_int (bintrunc (min LENGTH('a) n) i) :: 'a::len word)"
  1.2025 +lemma and_mask_wi':
  1.2026 +  "word_of_int i AND mask n = (word_of_int (bintrunc (min LENGTH('a) n) i) :: 'a::len word)"
  1.2027    by (auto simp add: nth_bintr word_size word_ops_nth_size word_eq_iff)
  1.2028  
  1.2029  lemma and_mask_no: "numeral i AND mask n = word_of_int (bintrunc n (numeral i))"
  1.2030 @@ -3143,7 +3088,7 @@
  1.2031    apply (rule xtr8)
  1.2032     prefer 2
  1.2033     apply (rule pos_mod_bound)
  1.2034 -  apply auto
  1.2035 +   apply auto
  1.2036    done
  1.2037  
  1.2038  lemma eq_mod_iff: "0 < (n::int) \<Longrightarrow> b = b mod n \<longleftrightarrow> 0 \<le> b \<and> b < n"
  1.2039 @@ -3156,41 +3101,39 @@
  1.2040    apply (fast intro!: lt2p_lem)
  1.2041    done
  1.2042  
  1.2043 -lemma and_mask_dvd: "2 ^ n dvd uint w = (w AND mask n = 0)"
  1.2044 +lemma and_mask_dvd: "2 ^ n dvd uint w \<longleftrightarrow> w AND mask n = 0"
  1.2045    apply (simp add: dvd_eq_mod_eq_0 and_mask_mod_2p)
  1.2046 -  apply (simp add: word_uint.norm_eq_iff [symmetric] word_of_int_homs
  1.2047 -    del: word_of_int_0)
  1.2048 +  apply (simp add: word_uint.norm_eq_iff [symmetric] word_of_int_homs del: word_of_int_0)
  1.2049    apply (subst word_uint.norm_Rep [symmetric])
  1.2050    apply (simp only: bintrunc_bintrunc_min bintrunc_mod2p [symmetric] min_def)
  1.2051    apply auto
  1.2052    done
  1.2053  
  1.2054 -lemma and_mask_dvd_nat: "2 ^ n dvd unat w = (w AND mask n = 0)"
  1.2055 +lemma and_mask_dvd_nat: "2 ^ n dvd unat w \<longleftrightarrow> w AND mask n = 0"
  1.2056    apply (unfold unat_def)
  1.2057    apply (rule trans [OF _ and_mask_dvd])
  1.2058    apply (unfold dvd_def)
  1.2059    apply auto
  1.2060 -  apply (drule uint_ge_0 [THEN nat_int.Abs_inverse' [simplified], symmetric])
  1.2061 -  apply (simp add : of_nat_mult of_nat_power)
  1.2062 -  apply (simp add : nat_mult_distrib nat_power_eq)
  1.2063 +   apply (drule uint_ge_0 [THEN nat_int.Abs_inverse' [simplified], symmetric])
  1.2064 +   apply simp
  1.2065 +  apply (simp add: nat_mult_distrib nat_power_eq)
  1.2066    done
  1.2067  
  1.2068 -lemma word_2p_lem:
  1.2069 -  "n < size w \<Longrightarrow> w < 2 ^ n = (uint (w :: 'a::len word) < 2 ^ n)"
  1.2070 +lemma word_2p_lem: "n < size w \<Longrightarrow> w < 2 ^ n = (uint w < 2 ^ n)"
  1.2071 +  for w :: "'a::len word"
  1.2072    apply (unfold word_size word_less_alt word_numeral_alt)
  1.2073 -  apply (clarsimp simp add: word_of_int_power_hom word_uint.eq_norm
  1.2074 -                            mod_pos_pos_trivial
  1.2075 -                  simp del: word_of_int_numeral)
  1.2076 +  apply (auto simp add: word_of_int_power_hom word_uint.eq_norm mod_pos_pos_trivial
  1.2077 +      simp del: word_of_int_numeral)
  1.2078    done
  1.2079  
  1.2080 -lemma less_mask_eq: "x < 2 ^ n \<Longrightarrow> x AND mask n = (x :: 'a::len word)"
  1.2081 +lemma less_mask_eq: "x < 2 ^ n \<Longrightarrow> x AND mask n = x"
  1.2082 +  for x :: "'a::len word"
  1.2083    apply (unfold word_less_alt word_numeral_alt)
  1.2084 -  apply (clarsimp simp add: and_mask_mod_2p word_of_int_power_hom
  1.2085 -                            word_uint.eq_norm
  1.2086 -                  simp del: word_of_int_numeral)
  1.2087 +  apply (clarsimp simp add: and_mask_mod_2p word_of_int_power_hom word_uint.eq_norm
  1.2088 +      simp del: word_of_int_numeral)
  1.2089    apply (drule xtr8 [rotated])
  1.2090 -  apply (rule int_mod_le)
  1.2091 -  apply (auto simp add : mod_pos_pos_trivial)
  1.2092 +   apply (rule int_mod_le)
  1.2093 +   apply (auto simp add : mod_pos_pos_trivial)
  1.2094    done
  1.2095  
  1.2096  lemmas mask_eq_iff_w2p = trans [OF mask_eq_iff word_2p_lem [symmetric]]
  1.2097 @@ -3200,9 +3143,9 @@
  1.2098  lemma and_mask_less_size: "n < size x \<Longrightarrow> x AND mask n < 2^n"
  1.2099    unfolding word_size by (erule and_mask_less')
  1.2100  
  1.2101 -lemma word_mod_2p_is_mask [OF refl]:
  1.2102 -  "c = 2 ^ n \<Longrightarrow> c > 0 \<Longrightarrow> x mod c = (x :: 'a::len word) AND mask n"
  1.2103 -  by (clarsimp simp add: word_mod_def uint_2p and_mask_mod_2p)
  1.2104 +lemma word_mod_2p_is_mask [OF refl]: "c = 2 ^ n \<Longrightarrow> c > 0 \<Longrightarrow> x mod c = x AND mask n"
  1.2105 +  for c x :: "'a::len word"
  1.2106 +  by (auto simp: word_mod_def uint_2p and_mask_mod_2p)
  1.2107  
  1.2108  lemma mask_eqs:
  1.2109    "(a AND mask n) + b AND mask n = a + b AND mask n"
  1.2110 @@ -3218,12 +3161,11 @@
  1.2111    "word_succ (a AND mask n) AND mask n = word_succ a AND mask n"
  1.2112    "word_pred (a AND mask n) AND mask n = word_pred a AND mask n"
  1.2113    using word_of_int_Ex [where x=a] word_of_int_Ex [where x=b]
  1.2114 -  by (auto simp add: and_mask_wi' word_of_int_homs word.abs_eq_iff bintrunc_mod2p mod_simps)
  1.2115 -
  1.2116 -lemma mask_power_eq:
  1.2117 -  "(x AND mask n) ^ k AND mask n = x ^ k AND mask n"
  1.2118 +  by (auto simp: and_mask_wi' word_of_int_homs word.abs_eq_iff bintrunc_mod2p mod_simps)
  1.2119 +
  1.2120 +lemma mask_power_eq: "(x AND mask n) ^ k AND mask n = x ^ k AND mask n"
  1.2121    using word_of_int_Ex [where x=x]
  1.2122 -  by (auto simp add: and_mask_wi' word_of_int_power_hom word.abs_eq_iff bintrunc_mod2p mod_simps)
  1.2123 +  by (auto simp: and_mask_wi' word_of_int_power_hom word.abs_eq_iff bintrunc_mod2p mod_simps)
  1.2124  
  1.2125  
  1.2126  subsubsection \<open>Revcast\<close>
  1.2127 @@ -3233,8 +3175,7 @@
  1.2128  lemmas revcast_no_def [simp] = revcast_def' [where w="numeral w", unfolded word_size] for w
  1.2129  
  1.2130  lemma to_bl_revcast:
  1.2131 -  "to_bl (revcast w :: 'a::len0 word) =
  1.2132 -   takefill False (len_of TYPE('a)) (to_bl w)"
  1.2133 +  "to_bl (revcast w :: 'a::len0 word) = takefill False (len_of TYPE('a)) (to_bl w)"
  1.2134    apply (unfold revcast_def' word_size)
  1.2135    apply (rule word_bl.Abs_inverse)
  1.2136    apply simp
  1.2137 @@ -3244,8 +3185,8 @@
  1.2138    "cs = [rc, uc] \<Longrightarrow> rc = revcast (word_reverse w) \<Longrightarrow> uc = ucast w \<Longrightarrow>
  1.2139      rc = word_reverse uc"
  1.2140    apply (unfold ucast_def revcast_def' Let_def word_reverse_def)
  1.2141 -  apply (clarsimp simp add : to_bl_of_bin takefill_bintrunc)
  1.2142 -  apply (simp add : word_bl.Abs_inverse word_size)
  1.2143 +  apply (auto simp: to_bl_of_bin takefill_bintrunc)
  1.2144 +  apply (simp add: word_bl.Abs_inverse word_size)
  1.2145    done
  1.2146  
  1.2147  lemma revcast_ucast: "revcast w = word_reverse (ucast (word_reverse w))"
  1.2148 @@ -3258,13 +3199,13 @@
  1.2149    by (fact revcast_ucast [THEN word_rev_gal'])
  1.2150  
  1.2151  
  1.2152 -\<comment> "linking revcast and cast via shift"
  1.2153 +text "linking revcast and cast via shift"
  1.2154  
  1.2155  lemmas wsst_TYs = source_size target_size word_size
  1.2156  
  1.2157  lemma revcast_down_uu [OF refl]:
  1.2158 -  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow>
  1.2159 -    rc (w :: 'a::len word) = ucast (w >> n)"
  1.2160 +  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = ucast (w >> n)"
  1.2161 +  for w :: "'a::len word"
  1.2162    apply (simp add: revcast_def')
  1.2163    apply (rule word_bl.Rep_inverse')
  1.2164    apply (rule trans, rule ucast_down_drop)
  1.2165 @@ -3274,8 +3215,8 @@
  1.2166    done
  1.2167  
  1.2168  lemma revcast_down_us [OF refl]:
  1.2169 -  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow>
  1.2170 -    rc (w :: 'a::len word) = ucast (w >>> n)"
  1.2171 +  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = ucast (w >>> n)"
  1.2172 +  for w :: "'a::len word"
  1.2173    apply (simp add: revcast_def')
  1.2174    apply (rule word_bl.Rep_inverse')
  1.2175    apply (rule trans, rule ucast_down_drop)
  1.2176 @@ -3285,8 +3226,8 @@
  1.2177    done
  1.2178  
  1.2179  lemma revcast_down_su [OF refl]:
  1.2180 -  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow>
  1.2181 -    rc (w :: 'a::len word) = scast (w >> n)"
  1.2182 +  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = scast (w >> n)"
  1.2183 +  for w :: "'a::len word"
  1.2184    apply (simp add: revcast_def')
  1.2185    apply (rule word_bl.Rep_inverse')
  1.2186    apply (rule trans, rule scast_down_drop)
  1.2187 @@ -3296,8 +3237,8 @@
  1.2188    done
  1.2189  
  1.2190  lemma revcast_down_ss [OF refl]:
  1.2191 -  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow>
  1.2192 -    rc (w :: 'a::len word) = scast (w >>> n)"
  1.2193 +  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = scast (w >>> n)"
  1.2194 +  for w :: "'a::len word"
  1.2195    apply (simp add: revcast_def')
  1.2196    apply (rule word_bl.Rep_inverse')
  1.2197    apply (rule trans, rule scast_down_drop)
  1.2198 @@ -3308,8 +3249,8 @@
  1.2199  
  1.2200  (* FIXME: should this also be [OF refl] ? *)
  1.2201  lemma cast_down_rev:
  1.2202 -  "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow>
  1.2203 -    uc w = revcast ((w :: 'a::len word) << n)"
  1.2204 +  "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow> uc w = revcast (w << n)"
  1.2205 +  for w :: "'a::len word"
  1.2206    apply (unfold shiftl_rev)
  1.2207    apply clarify
  1.2208    apply (simp add: revcast_rev_ucast)
  1.2209 @@ -3327,7 +3268,7 @@
  1.2210    apply (simp add: takefill_alt)
  1.2211    apply (rule bl_shiftl [THEN trans])
  1.2212    apply (subst ucast_up_app)
  1.2213 -  apply (auto simp add: wsst_TYs)
  1.2214 +   apply (auto simp add: wsst_TYs)
  1.2215    done
  1.2216  
  1.2217  lemmas rc1 = revcast_up [THEN