src/HOL/Word/Word.thy
changeset 65336 8e5274fc0093
parent 65328 2510b0ce28da
child 65363 5eb619751b14
     1.1 --- a/src/HOL/Word/Word.thy	Mon Mar 20 20:43:26 2017 +0100
     1.2 +++ b/src/HOL/Word/Word.thy	Mon Mar 20 21:44:41 2017 +0100
     1.3 @@ -3315,25 +3315,21 @@
     1.4    apply (simp add: word_size)
     1.5    done
     1.6  
     1.7 -lemma nth_slice:
     1.8 -  "(slice n w :: 'a::len0 word) !! m =
     1.9 -   (w !! (m + n) & m < len_of TYPE('a))"
    1.10 -  unfolding slice_shiftr
    1.11 -  by (simp add : nth_ucast nth_shiftr)
    1.12 +lemma nth_slice: "(slice n w :: 'a::len0 word) !! m = (w !! (m + n) \<and> m < len_of TYPE('a))"
    1.13 +  by (simp add: slice_shiftr nth_ucast nth_shiftr)
    1.14  
    1.15  lemma slice1_down_alt':
    1.16    "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs + k = n \<Longrightarrow>
    1.17      to_bl sl = takefill False fs (drop k (to_bl w))"
    1.18 -  unfolding slice1_def word_size of_bl_def uint_bl
    1.19 -  by (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop drop_takefill)
    1.20 +  by (auto simp: slice1_def word_size of_bl_def uint_bl
    1.21 +      word_ubin.eq_norm bl_bin_bl_rep_drop drop_takefill)
    1.22  
    1.23  lemma slice1_up_alt':
    1.24    "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs = n + k \<Longrightarrow>
    1.25      to_bl sl = takefill False fs (replicate k False @ (to_bl w))"
    1.26    apply (unfold slice1_def word_size of_bl_def uint_bl)
    1.27 -  apply (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop
    1.28 -                        takefill_append [symmetric])
    1.29 -  apply (rule_tac f = "%k. takefill False (len_of TYPE('a))
    1.30 +  apply (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop takefill_append [symmetric])
    1.31 +  apply (rule_tac f = "\<lambda>k. takefill False (len_of TYPE('a))
    1.32      (replicate k False @ bin_to_bl (len_of TYPE('b)) (uint w))" in arg_cong)
    1.33    apply arith
    1.34    done
    1.35 @@ -3346,42 +3342,40 @@
    1.36    le_add_diff_inverse2 [symmetric, THEN su1]
    1.37  
    1.38  lemma ucast_slice1: "ucast w = slice1 (size w) w"
    1.39 -  unfolding slice1_def ucast_bl
    1.40 -  by (simp add : takefill_same' word_size)
    1.41 +  by (simp add: slice1_def ucast_bl takefill_same' word_size)
    1.42  
    1.43  lemma ucast_slice: "ucast w = slice 0 w"
    1.44 -  unfolding slice_def by (simp add : ucast_slice1)
    1.45 +  by (simp add: slice_def ucast_slice1)
    1.46  
    1.47  lemma slice_id: "slice 0 t = t"
    1.48    by (simp only: ucast_slice [symmetric] ucast_id)
    1.49  
    1.50 -lemma revcast_slice1 [OF refl]:
    1.51 -  "rc = revcast w \<Longrightarrow> slice1 (size rc) w = rc"
    1.52 -  unfolding slice1_def revcast_def' by (simp add : word_size)
    1.53 +lemma revcast_slice1 [OF refl]: "rc = revcast w \<Longrightarrow> slice1 (size rc) w = rc"
    1.54 +  by (simp add: slice1_def revcast_def' word_size)
    1.55  
    1.56  lemma slice1_tf_tf':
    1.57    "to_bl (slice1 n w :: 'a::len0 word) =
    1.58 -   rev (takefill False (len_of TYPE('a)) (rev (takefill False n (to_bl w))))"
    1.59 +    rev (takefill False (len_of TYPE('a)) (rev (takefill False n (to_bl w))))"
    1.60    unfolding slice1_def by (rule word_rev_tf)
    1.61  
    1.62  lemmas slice1_tf_tf = slice1_tf_tf' [THEN word_bl.Rep_inverse', symmetric]
    1.63  
    1.64  lemma rev_slice1:
    1.65    "n + k = len_of TYPE('a) + len_of TYPE('b) \<Longrightarrow>
    1.66 -  slice1 n (word_reverse w :: 'b::len0 word) =
    1.67 -  word_reverse (slice1 k w :: 'a::len0 word)"
    1.68 +    slice1 n (word_reverse w :: 'b::len0 word) =
    1.69 +    word_reverse (slice1 k w :: 'a::len0 word)"
    1.70    apply (unfold word_reverse_def slice1_tf_tf)
    1.71    apply (rule word_bl.Rep_inverse')
    1.72    apply (rule rev_swap [THEN iffD1])
    1.73    apply (rule trans [symmetric])
    1.74 -  apply (rule tf_rev)
    1.75 +   apply (rule tf_rev)
    1.76     apply (simp add: word_bl.Abs_inverse)
    1.77    apply (simp add: word_bl.Abs_inverse)
    1.78    done
    1.79  
    1.80  lemma rev_slice:
    1.81    "n + k + len_of TYPE('a::len0) = len_of TYPE('b::len0) \<Longrightarrow>
    1.82 -    slice n (word_reverse (w::'b word)) = word_reverse (slice k w::'a word)"
    1.83 +    slice n (word_reverse (w::'b word)) = word_reverse (slice k w :: 'a word)"
    1.84    apply (unfold slice_def word_size)
    1.85    apply (rule rev_slice1)
    1.86    apply arith
    1.87 @@ -3394,8 +3388,9 @@
    1.88        criterion for overflow of addition of signed integers\<close>
    1.89  
    1.90  lemma sofl_test:
    1.91 -  "(sint (x :: 'a::len word) + sint y = sint (x + y)) =
    1.92 -     ((((x+y) XOR x) AND ((x+y) XOR y)) >> (size x - 1) = 0)"
    1.93 +  "(sint x + sint y = sint (x + y)) =
    1.94 +     ((((x + y) XOR x) AND ((x + y) XOR y)) >> (size x - 1) = 0)"
    1.95 +  for x y :: "'a::len word"
    1.96    apply (unfold word_size)
    1.97    apply (cases "len_of TYPE('a)", simp)
    1.98    apply (subst msb_shift [THEN sym_notr])
    1.99 @@ -3406,19 +3401,19 @@
   1.100       apply (unfold sint_word_ariths)
   1.101       apply (unfold word_sbin.set_iff_norm [symmetric] sints_num)
   1.102       apply safe
   1.103 -        apply (insert sint_range' [where x=x])
   1.104 -        apply (insert sint_range' [where x=y])
   1.105 -        defer
   1.106 +         apply (insert sint_range' [where x=x])
   1.107 +         apply (insert sint_range' [where x=y])
   1.108 +         defer
   1.109 +         apply (simp (no_asm), arith)
   1.110          apply (simp (no_asm), arith)
   1.111 +       defer
   1.112 +       defer
   1.113         apply (simp (no_asm), arith)
   1.114 -      defer
   1.115 -      defer
   1.116        apply (simp (no_asm), arith)
   1.117 -     apply (simp (no_asm), arith)
   1.118 -    apply (rule notI [THEN notnotD],
   1.119 -           drule leI not_le_imp_less,
   1.120 -           drule sbintrunc_inc sbintrunc_dec,
   1.121 -           simp)+
   1.122 +     apply (rule notI [THEN notnotD],
   1.123 +      drule leI not_le_imp_less,
   1.124 +      drule sbintrunc_inc sbintrunc_dec,
   1.125 +      simp)+
   1.126    done
   1.127  
   1.128  
   1.129 @@ -3431,57 +3426,49 @@
   1.130    "(word_rsplit (numeral bin :: 'b::len0 word) :: 'a word list) =
   1.131      map word_of_int (bin_rsplit (len_of TYPE('a::len))
   1.132        (len_of TYPE('b), bintrunc (len_of TYPE('b)) (numeral bin)))"
   1.133 -  unfolding word_rsplit_def by (simp add: word_ubin.eq_norm)
   1.134 +  by (simp add: word_rsplit_def word_ubin.eq_norm)
   1.135  
   1.136  lemmas word_rsplit_no_cl [simp] = word_rsplit_no
   1.137    [unfolded bin_rsplitl_def bin_rsplit_l [symmetric]]
   1.138  
   1.139  lemma test_bit_cat:
   1.140 -  "wc = word_cat a b \<Longrightarrow> wc !! n = (n < size wc &
   1.141 +  "wc = word_cat a b \<Longrightarrow> wc !! n = (n < size wc \<and>
   1.142      (if n < size b then b !! n else a !! (n - size b)))"
   1.143 -  apply (unfold word_cat_bin' test_bit_bin)
   1.144 -  apply (auto simp add : word_ubin.eq_norm nth_bintr bin_nth_cat word_size)
   1.145 +  apply (auto simp: word_cat_bin' test_bit_bin word_ubin.eq_norm nth_bintr bin_nth_cat word_size)
   1.146    apply (erule bin_nth_uint_imp)
   1.147    done
   1.148  
   1.149  lemma word_cat_bl: "word_cat a b = of_bl (to_bl a @ to_bl b)"
   1.150 -  apply (unfold of_bl_def to_bl_def word_cat_bin')
   1.151 -  apply (simp add: bl_to_bin_app_cat)
   1.152 -  done
   1.153 +  by (simp add: of_bl_def to_bl_def word_cat_bin' bl_to_bin_app_cat)
   1.154  
   1.155  lemma of_bl_append:
   1.156    "(of_bl (xs @ ys) :: 'a::len word) = of_bl xs * 2^(length ys) + of_bl ys"
   1.157 -  apply (unfold of_bl_def)
   1.158 -  apply (simp add: bl_to_bin_app_cat bin_cat_num)
   1.159 +  apply (simp add: of_bl_def bl_to_bin_app_cat bin_cat_num)
   1.160    apply (simp add: word_of_int_power_hom [symmetric] word_of_int_hom_syms)
   1.161    done
   1.162  
   1.163 -lemma of_bl_False [simp]:
   1.164 -  "of_bl (False#xs) = of_bl xs"
   1.165 -  by (rule word_eqI)
   1.166 -     (auto simp add: test_bit_of_bl nth_append)
   1.167 -
   1.168 -lemma of_bl_True [simp]:
   1.169 -  "(of_bl (True#xs)::'a::len word) = 2^length xs + of_bl xs"
   1.170 -  by (subst of_bl_append [where xs="[True]", simplified])
   1.171 -     (simp add: word_1_bl)
   1.172 -
   1.173 -lemma of_bl_Cons:
   1.174 -  "of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs"
   1.175 +lemma of_bl_False [simp]: "of_bl (False#xs) = of_bl xs"
   1.176 +  by (rule word_eqI) (auto simp: test_bit_of_bl nth_append)
   1.177 +
   1.178 +lemma of_bl_True [simp]: "(of_bl (True # xs) :: 'a::len word) = 2^length xs + of_bl xs"
   1.179 +  by (subst of_bl_append [where xs="[True]", simplified]) (simp add: word_1_bl)
   1.180 +
   1.181 +lemma of_bl_Cons: "of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs"
   1.182    by (cases x) simp_all
   1.183  
   1.184 -lemma split_uint_lem: "bin_split n (uint (w :: 'a::len0 word)) = (a, b) \<Longrightarrow>
   1.185 -  a = bintrunc (len_of TYPE('a) - n) a & b = bintrunc (len_of TYPE('a)) b"
   1.186 +lemma split_uint_lem: "bin_split n (uint w) = (a, b) \<Longrightarrow>
   1.187 +    a = bintrunc (len_of TYPE('a) - n) a \<and> b = bintrunc (len_of TYPE('a)) b"
   1.188 +  for w :: "'a::len0 word"
   1.189    apply (frule word_ubin.norm_Rep [THEN ssubst])
   1.190    apply (drule bin_split_trunc1)
   1.191    apply (drule sym [THEN trans])
   1.192 -  apply assumption
   1.193 +   apply assumption
   1.194    apply safe
   1.195    done
   1.196  
   1.197  lemma word_split_bl':
   1.198    "std = size c - size b \<Longrightarrow> (word_split c = (a, b)) \<Longrightarrow>
   1.199 -    (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c)))"
   1.200 +    (a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c)))"
   1.201    apply (unfold word_split_bin')
   1.202    apply safe
   1.203     defer
   1.204 @@ -3489,12 +3476,12 @@
   1.205     apply hypsubst_thin
   1.206     apply (drule word_ubin.norm_Rep [THEN ssubst])
   1.207     apply (drule split_bintrunc)
   1.208 -   apply (simp add : of_bl_def bl2bin_drop word_size
   1.209 -       word_ubin.norm_eq_iff [symmetric] min_def del : word_ubin.norm_Rep)
   1.210 +   apply (simp add: of_bl_def bl2bin_drop word_size
   1.211 +      word_ubin.norm_eq_iff [symmetric] min_def del: word_ubin.norm_Rep)
   1.212    apply (clarsimp split: prod.splits)
   1.213    apply (frule split_uint_lem [THEN conjunct1])
   1.214    apply (unfold word_size)
   1.215 -  apply (cases "len_of TYPE('a) >= len_of TYPE('b)")
   1.216 +  apply (cases "len_of TYPE('a) \<ge> len_of TYPE('b)")
   1.217     defer
   1.218     apply simp
   1.219    apply (simp add : of_bl_def to_bl_def)
   1.220 @@ -3508,30 +3495,33 @@
   1.221    done
   1.222  
   1.223  lemma word_split_bl: "std = size c - size b \<Longrightarrow>
   1.224 -    (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c))) \<longleftrightarrow>
   1.225 +    (a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c))) \<longleftrightarrow>
   1.226      word_split c = (a, b)"
   1.227    apply (rule iffI)
   1.228     defer
   1.229     apply (erule (1) word_split_bl')
   1.230    apply (case_tac "word_split c")
   1.231 -  apply (auto simp add : word_size)
   1.232 +  apply (auto simp add: word_size)
   1.233    apply (frule word_split_bl' [rotated])
   1.234 -  apply (auto simp add : word_size)
   1.235 +   apply (auto simp add: word_size)
   1.236    done
   1.237  
   1.238  lemma word_split_bl_eq:
   1.239 -   "(word_split (c::'a::len word) :: ('c::len0 word * 'd::len0 word)) =
   1.240 -      (of_bl (take (len_of TYPE('a::len) - len_of TYPE('d::len0)) (to_bl c)),
   1.241 -       of_bl (drop (len_of TYPE('a) - len_of TYPE('d)) (to_bl c)))"
   1.242 +  "(word_split c :: ('c::len0 word \<times> 'd::len0 word)) =
   1.243 +    (of_bl (take (len_of TYPE('a::len) - len_of TYPE('d::len0)) (to_bl c)),
   1.244 +     of_bl (drop (len_of TYPE('a) - len_of TYPE('d)) (to_bl c)))"
   1.245 +  for c :: "'a::len word"
   1.246    apply (rule word_split_bl [THEN iffD1])
   1.247 -  apply (unfold word_size)
   1.248 -  apply (rule refl conjI)+
   1.249 +   apply (unfold word_size)
   1.250 +   apply (rule refl conjI)+
   1.251    done
   1.252  
   1.253  \<comment> "keep quantifiers for use in simplification"
   1.254  lemma test_bit_split':
   1.255 -  "word_split c = (a, b) --> (ALL n m. b !! n = (n < size b & c !! n) &
   1.256 -    a !! m = (m < size a & c !! (m + size b)))"
   1.257 +  "word_split c = (a, b) \<longrightarrow>
   1.258 +    (\<forall>n m.
   1.259 +      b !! n = (n < size b \<and> c !! n) \<and>
   1.260 +      a !! m = (m < size a \<and> c !! (m + size b)))"
   1.261    apply (unfold word_split_bin' test_bit_bin)
   1.262    apply (clarify)
   1.263    apply (clarsimp simp: word_ubin.eq_norm nth_bintr word_size split: prod.splits)
   1.264 @@ -3543,12 +3533,14 @@
   1.265  
   1.266  lemma test_bit_split:
   1.267    "word_split c = (a, b) \<Longrightarrow>
   1.268 -    (\<forall>n::nat. b !! n \<longleftrightarrow> n < size b \<and> c !! n) \<and> (\<forall>m::nat. a !! m \<longleftrightarrow> m < size a \<and> c !! (m + size b))"
   1.269 +    (\<forall>n::nat. b !! n \<longleftrightarrow> n < size b \<and> c !! n) \<and>
   1.270 +    (\<forall>m::nat. a !! m \<longleftrightarrow> m < size a \<and> c !! (m + size b))"
   1.271    by (simp add: test_bit_split')
   1.272  
   1.273 -lemma test_bit_split_eq: "word_split c = (a, b) \<longleftrightarrow>
   1.274 -  ((ALL n::nat. b !! n = (n < size b & c !! n)) &
   1.275 -    (ALL m::nat. a !! m = (m < size a & c !! (m + size b))))"
   1.276 +lemma test_bit_split_eq:
   1.277 +  "word_split c = (a, b) \<longleftrightarrow>
   1.278 +    ((\<forall>n::nat. b !! n = (n < size b \<and> c !! n)) \<and>
   1.279 +     (\<forall>m::nat. a !! m = (m < size a \<and> c !! (m + size b))))"
   1.280    apply (rule_tac iffI)
   1.281     apply (rule_tac conjI)
   1.282      apply (erule test_bit_split [THEN conjunct1])
   1.283 @@ -3556,28 +3548,24 @@
   1.284    apply (case_tac "word_split c")
   1.285    apply (frule test_bit_split)
   1.286    apply (erule trans)
   1.287 -  apply (fastforce intro ! : word_eqI simp add : word_size)
   1.288 +  apply (fastforce intro!: word_eqI simp add: word_size)
   1.289    done
   1.290  
   1.291  \<comment> \<open>this odd result is analogous to \<open>ucast_id\<close>,
   1.292        result to the length given by the result type\<close>
   1.293  
   1.294  lemma word_cat_id: "word_cat a b = b"
   1.295 -  unfolding word_cat_bin' by (simp add: word_ubin.inverse_norm)
   1.296 +  by (simp add: word_cat_bin' word_ubin.inverse_norm)
   1.297  
   1.298  \<comment> "limited hom result"
   1.299  lemma word_cat_hom:
   1.300 -  "len_of TYPE('a::len0) <= len_of TYPE('b::len0) + len_of TYPE('c::len0)
   1.301 -  \<Longrightarrow>
   1.302 -  (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) =
   1.303 -  word_of_int (bin_cat w (size b) (uint b))"
   1.304 -  apply (unfold word_cat_def word_size)
   1.305 -  apply (clarsimp simp add: word_ubin.norm_eq_iff [symmetric]
   1.306 +  "len_of TYPE('a::len0) \<le> len_of TYPE('b::len0) + len_of TYPE('c::len0) \<Longrightarrow>
   1.307 +    (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) =
   1.308 +    word_of_int (bin_cat w (size b) (uint b))"
   1.309 +  by (auto simp: word_cat_def word_size word_ubin.norm_eq_iff [symmetric]
   1.310        word_ubin.eq_norm bintr_cat min.absorb1)
   1.311 -  done
   1.312 -
   1.313 -lemma word_cat_split_alt:
   1.314 -  "size w <= size u + size v \<Longrightarrow> word_split w = (u, v) \<Longrightarrow> word_cat u v = w"
   1.315 +
   1.316 +lemma word_cat_split_alt: "size w \<le> size u + size v \<Longrightarrow> word_split w = (u, v) \<Longrightarrow> word_cat u v = w"
   1.317    apply (rule word_eqI)
   1.318    apply (drule test_bit_split)
   1.319    apply (clarsimp simp add : test_bit_cat word_size)
   1.320 @@ -3590,8 +3578,7 @@
   1.321  
   1.322  subsubsection \<open>Split and slice\<close>
   1.323  
   1.324 -lemma split_slices:
   1.325 -  "word_split w = (u, v) \<Longrightarrow> u = slice (size v) w & v = slice 0 w"
   1.326 +lemma split_slices: "word_split w = (u, v) \<Longrightarrow> u = slice (size v) w \<and> v = slice 0 w"
   1.327    apply (drule test_bit_split)
   1.328    apply (rule conjI)
   1.329     apply (rule word_eqI, clarsimp simp: nth_slice word_size)+
   1.330 @@ -3617,7 +3604,7 @@
   1.331    done
   1.332  
   1.333  lemma word_split_cat_alt:
   1.334 -  "w = word_cat u v \<Longrightarrow> size u + size v <= size w \<Longrightarrow> word_split w = (u, v)"
   1.335 +  "w = word_cat u v \<Longrightarrow> size u + size v \<le> size w \<Longrightarrow> word_split w = (u, v)"
   1.336    apply (case_tac "word_split w")
   1.337    apply (rule trans, assumption)
   1.338    apply (drule test_bit_split)
   1.339 @@ -3626,31 +3613,30 @@
   1.340    done
   1.341  
   1.342  lemmas word_cat_bl_no_bin [simp] =
   1.343 -  word_cat_bl [where a="numeral a" and b="numeral b",
   1.344 -    unfolded to_bl_numeral]
   1.345 +  word_cat_bl [where a="numeral a" and b="numeral b", unfolded to_bl_numeral]
   1.346    for a b (* FIXME: negative numerals, 0 and 1 *)
   1.347  
   1.348  lemmas word_split_bl_no_bin [simp] =
   1.349    word_split_bl_eq [where c="numeral c", unfolded to_bl_numeral] for c
   1.350  
   1.351 -text \<open>this odd result arises from the fact that the statement of the
   1.352 -      result implies that the decoded words are of the same type,
   1.353 -      and therefore of the same length, as the original word\<close>
   1.354 +text \<open>
   1.355 +  This odd result arises from the fact that the statement of the
   1.356 +  result implies that the decoded words are of the same type,
   1.357 +  and therefore of the same length, as the original word.\<close>
   1.358  
   1.359  lemma word_rsplit_same: "word_rsplit w = [w]"
   1.360 -  unfolding word_rsplit_def by (simp add : bin_rsplit_all)
   1.361 -
   1.362 -lemma word_rsplit_empty_iff_size:
   1.363 -  "(word_rsplit w = []) = (size w = 0)"
   1.364 -  unfolding word_rsplit_def bin_rsplit_def word_size
   1.365 -  by (simp add: bin_rsplit_aux_simp_alt Let_def split: prod.split)
   1.366 +  by (simp add: word_rsplit_def bin_rsplit_all)
   1.367 +
   1.368 +lemma word_rsplit_empty_iff_size: "word_rsplit w = [] \<longleftrightarrow> size w = 0"
   1.369 +  by (simp add: word_rsplit_def bin_rsplit_def word_size bin_rsplit_aux_simp_alt Let_def
   1.370 +      split: prod.split)
   1.371  
   1.372  lemma test_bit_rsplit:
   1.373    "sw = word_rsplit w \<Longrightarrow> m < size (hd sw :: 'a::len word) \<Longrightarrow>
   1.374      k < length sw \<Longrightarrow> (rev sw ! k) !! m = (w !! (k * size (hd sw) + m))"
   1.375    apply (unfold word_rsplit_def word_test_bit_def)
   1.376    apply (rule trans)
   1.377 -   apply (rule_tac f = "%x. bin_nth x m" in arg_cong)
   1.378 +   apply (rule_tac f = "\<lambda>x. bin_nth x m" in arg_cong)
   1.379     apply (rule nth_map [symmetric])
   1.380     apply simp
   1.381    apply (rule bin_nth_rsplit)
   1.382 @@ -3665,12 +3651,10 @@
   1.383    done
   1.384  
   1.385  lemma word_rcat_bl: "word_rcat wl = of_bl (concat (map to_bl wl))"
   1.386 -  unfolding word_rcat_def to_bl_def' of_bl_def
   1.387 -  by (clarsimp simp add : bin_rcat_bl)
   1.388 -
   1.389 -lemma size_rcat_lem':
   1.390 -  "size (concat (map to_bl wl)) = length wl * size (hd wl)"
   1.391 -  unfolding word_size by (induct wl) auto
   1.392 +  by (auto simp: word_rcat_def to_bl_def' of_bl_def bin_rcat_bl)
   1.393 +
   1.394 +lemma size_rcat_lem': "size (concat (map to_bl wl)) = length wl * size (hd wl)"
   1.395 +  by (induct wl) (auto simp: word_size)
   1.396  
   1.397  lemmas size_rcat_lem = size_rcat_lem' [unfolded word_size]
   1.398  
   1.399 @@ -3680,7 +3664,7 @@
   1.400    "n < length (wl::'a word list) * len_of TYPE('a::len) \<Longrightarrow>
   1.401      rev (concat (map to_bl wl)) ! n =
   1.402      rev (to_bl (rev wl ! (n div len_of TYPE('a)))) ! (n mod len_of TYPE('a))"
   1.403 -  apply (induct "wl")
   1.404 +  apply (induct wl)
   1.405     apply clarsimp
   1.406    apply (clarsimp simp add : nth_append size_rcat_lem)
   1.407    apply (simp (no_asm_use) only:  mult_Suc [symmetric]
   1.408 @@ -3690,18 +3674,16 @@
   1.409  
   1.410  lemma test_bit_rcat:
   1.411    "sw = size (hd wl :: 'a::len word) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> rc !! n =
   1.412 -    (n < size rc & n div sw < size wl & (rev wl) ! (n div sw) !! (n mod sw))"
   1.413 +    (n < size rc \<and> n div sw < size wl \<and> (rev wl) ! (n div sw) !! (n mod sw))"
   1.414    apply (unfold word_rcat_bl word_size)
   1.415 -  apply (clarsimp simp add :
   1.416 -    test_bit_of_bl size_rcat_lem word_size td_gal_lt_len)
   1.417 +  apply (clarsimp simp add: test_bit_of_bl size_rcat_lem word_size td_gal_lt_len)
   1.418    apply safe
   1.419 -   apply (auto simp add :
   1.420 -    test_bit_bl word_size td_gal_lt_len [THEN iffD2, THEN nth_rcat_lem])
   1.421 +   apply (auto simp: test_bit_bl word_size td_gal_lt_len [THEN iffD2, THEN nth_rcat_lem])
   1.422    done
   1.423  
   1.424 -lemma foldl_eq_foldr:
   1.425 -  "foldl op + x xs = foldr op + (x # xs) (0 :: 'a :: comm_monoid_add)"
   1.426 -  by (induct xs arbitrary: x) (auto simp add : add.assoc)
   1.427 +lemma foldl_eq_foldr: "foldl op + x xs = foldr op + (x # xs) 0"
   1.428 +  for x :: "'a::comm_monoid_add"
   1.429 +  by (induct xs arbitrary: x) (auto simp: add.assoc)
   1.430  
   1.431  lemmas test_bit_cong = arg_cong [where f = "test_bit", THEN fun_cong]
   1.432  
   1.433 @@ -3713,16 +3695,12 @@
   1.434  lemma word_rsplit_len_indep [OF refl refl refl refl]:
   1.435    "[u,v] = p \<Longrightarrow> [su,sv] = q \<Longrightarrow> word_rsplit u = su \<Longrightarrow>
   1.436      word_rsplit v = sv \<Longrightarrow> length su = length sv"
   1.437 -  apply (unfold word_rsplit_def)
   1.438 -  apply (auto simp add : bin_rsplit_len_indep)
   1.439 -  done
   1.440 +  by (auto simp: word_rsplit_def bin_rsplit_len_indep)
   1.441  
   1.442  lemma length_word_rsplit_size:
   1.443    "n = len_of TYPE('a::len) \<Longrightarrow>
   1.444 -    (length (word_rsplit w :: 'a word list) <= m) = (size w <= m * n)"
   1.445 -  apply (unfold word_rsplit_def word_size)
   1.446 -  apply (clarsimp simp add : bin_rsplit_len_le)
   1.447 -  done
   1.448 +    length (word_rsplit w :: 'a word list) \<le> m \<longleftrightarrow> size w \<le> m * n"
   1.449 +  by (auto simp: word_rsplit_def word_size bin_rsplit_len_le)
   1.450  
   1.451  lemmas length_word_rsplit_lt_size =
   1.452    length_word_rsplit_size [unfolded Not_eq_iff linorder_not_less [symmetric]]
   1.453 @@ -3730,12 +3708,12 @@
   1.454  lemma length_word_rsplit_exp_size:
   1.455    "n = len_of TYPE('a::len) \<Longrightarrow>
   1.456      length (word_rsplit w :: 'a word list) = (size w + n - 1) div n"
   1.457 -  unfolding word_rsplit_def by (clarsimp simp add : word_size bin_rsplit_len)
   1.458 +  by (auto simp: word_rsplit_def word_size bin_rsplit_len)
   1.459  
   1.460  lemma length_word_rsplit_even_size:
   1.461    "n = len_of TYPE('a::len) \<Longrightarrow> size w = m * n \<Longrightarrow>
   1.462      length (word_rsplit w :: 'a word list) = m"
   1.463 -  by (clarsimp simp add : length_word_rsplit_exp_size given_quot_alt)
   1.464 +  by (auto simp: length_word_rsplit_exp_size given_quot_alt)
   1.465  
   1.466  lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size]
   1.467  
   1.468 @@ -3745,7 +3723,7 @@
   1.469  
   1.470  lemma word_rcat_rsplit: "word_rcat (word_rsplit w) = w"
   1.471    apply (rule word_eqI)
   1.472 -  apply (clarsimp simp add : test_bit_rcat word_size)
   1.473 +  apply (clarsimp simp: test_bit_rcat word_size)
   1.474    apply (subst refl [THEN test_bit_rsplit])
   1.475      apply (simp_all add: word_size
   1.476        refl [THEN length_word_rsplit_size [simplified not_less [symmetric], simplified]])
   1.477 @@ -3754,22 +3732,23 @@
   1.478    done
   1.479  
   1.480  lemma size_word_rsplit_rcat_size:
   1.481 -  "\<lbrakk>word_rcat (ws::'a::len word list) = (frcw::'b::len0 word);
   1.482 -     size frcw = length ws * len_of TYPE('a)\<rbrakk>
   1.483 +  "word_rcat ws = frcw \<Longrightarrow> size frcw = length ws * len_of TYPE('a)
   1.484      \<Longrightarrow> length (word_rsplit frcw::'a word list) = length ws"
   1.485 -  apply (clarsimp simp add : word_size length_word_rsplit_exp_size')
   1.486 +  for ws :: "'a::len word list" and frcw :: "'b::len0 word"
   1.487 +  apply (clarsimp simp: word_size length_word_rsplit_exp_size')
   1.488    apply (fast intro: given_quot_alt)
   1.489    done
   1.490  
   1.491  lemma msrevs:
   1.492 -  fixes n::nat
   1.493 -  shows "0 < n \<Longrightarrow> (k * n + m) div n = m div n + k"
   1.494 -  and   "(k * n + m) mod n = m mod n"
   1.495 +  "0 < n \<Longrightarrow> (k * n + m) div n = m div n + k"
   1.496 +  "(k * n + m) mod n = m mod n"
   1.497 +  for n :: nat
   1.498    by (auto simp: add.commute)
   1.499  
   1.500  lemma word_rsplit_rcat_size [OF refl]:
   1.501 -  "word_rcat (ws :: 'a::len word list) = frcw \<Longrightarrow>
   1.502 +  "word_rcat ws = frcw \<Longrightarrow>
   1.503      size frcw = length ws * len_of TYPE('a) \<Longrightarrow> word_rsplit frcw = ws"
   1.504 +  for ws :: "'a::len word list"
   1.505    apply (frule size_word_rsplit_rcat_size, assumption)
   1.506    apply (clarsimp simp add : word_size)
   1.507    apply (rule nth_equalityI, assumption)
   1.508 @@ -3779,7 +3758,7 @@
   1.509     apply (rule test_bit_rsplit_alt)
   1.510       apply (clarsimp simp: word_size)+
   1.511    apply (rule trans)
   1.512 -  apply (rule test_bit_rcat [OF refl refl])
   1.513 +   apply (rule test_bit_rcat [OF refl refl])
   1.514    apply (simp add: word_size)
   1.515    apply (subst nth_rev)
   1.516     apply arith
   1.517 @@ -3787,8 +3766,8 @@
   1.518    apply safe
   1.519    apply (simp add: diff_mult_distrib)
   1.520    apply (rule mpl_lem)
   1.521 -  apply (cases "size ws")
   1.522 -   apply simp_all
   1.523 +   apply (cases "size ws")
   1.524 +    apply simp_all
   1.525    done
   1.526  
   1.527  
   1.528 @@ -3798,8 +3777,7 @@
   1.529  
   1.530  lemmas word_rot_defs = word_roti_def word_rotr_def word_rotl_def
   1.531  
   1.532 -lemma rotate_eq_mod:
   1.533 -  "m mod length xs = n mod length xs \<Longrightarrow> rotate m xs = rotate n xs"
   1.534 +lemma rotate_eq_mod: "m mod length xs = n mod length xs \<Longrightarrow> rotate m xs = rotate n xs"
   1.535    apply (rule box_equals)
   1.536      defer
   1.537      apply (rule rotate_conv_mod [symmetric])+
   1.538 @@ -3817,47 +3795,42 @@
   1.539  subsubsection \<open>Rotation of list to right\<close>
   1.540  
   1.541  lemma rotate1_rl': "rotater1 (l @ [a]) = a # l"
   1.542 -  unfolding rotater1_def by (cases l) auto
   1.543 +  by (cases l) (auto simp: rotater1_def)
   1.544  
   1.545  lemma rotate1_rl [simp] : "rotater1 (rotate1 l) = l"
   1.546    apply (unfold rotater1_def)
   1.547    apply (cases "l")
   1.548 -  apply (case_tac [2] "list")
   1.549 -  apply auto
   1.550 +   apply (case_tac [2] "list")
   1.551 +    apply auto
   1.552    done
   1.553  
   1.554  lemma rotate1_lr [simp] : "rotate1 (rotater1 l) = l"
   1.555 -  unfolding rotater1_def by (cases l) auto
   1.556 +  by (cases l) (auto simp: rotater1_def)
   1.557  
   1.558  lemma rotater1_rev': "rotater1 (rev xs) = rev (rotate1 xs)"
   1.559 -  apply (cases "xs")
   1.560 -  apply (simp add : rotater1_def)
   1.561 -  apply (simp add : rotate1_rl')
   1.562 -  done
   1.563 +  by (cases "xs") (simp add: rotater1_def, simp add: rotate1_rl')
   1.564  
   1.565  lemma rotater_rev': "rotater n (rev xs) = rev (rotate n xs)"
   1.566 -  unfolding rotater_def by (induct n) (auto intro: rotater1_rev')
   1.567 +  by (induct n) (auto simp: rotater_def intro: rotater1_rev')
   1.568  
   1.569  lemma rotater_rev: "rotater n ys = rev (rotate n (rev ys))"
   1.570    using rotater_rev' [where xs = "rev ys"] by simp
   1.571  
   1.572  lemma rotater_drop_take:
   1.573    "rotater n xs =
   1.574 -   drop (length xs - n mod length xs) xs @
   1.575 -   take (length xs - n mod length xs) xs"
   1.576 -  by (clarsimp simp add : rotater_rev rotate_drop_take rev_take rev_drop)
   1.577 -
   1.578 -lemma rotater_Suc [simp] :
   1.579 -  "rotater (Suc n) xs = rotater1 (rotater n xs)"
   1.580 +    drop (length xs - n mod length xs) xs @
   1.581 +    take (length xs - n mod length xs) xs"
   1.582 +  by (auto simp: rotater_rev rotate_drop_take rev_take rev_drop)
   1.583 +
   1.584 +lemma rotater_Suc [simp]: "rotater (Suc n) xs = rotater1 (rotater n xs)"
   1.585    unfolding rotater_def by auto
   1.586  
   1.587  lemma rotate_inv_plus [rule_format] :
   1.588 -  "ALL k. k = m + n --> rotater k (rotate n xs) = rotater m xs &
   1.589 -    rotate k (rotater n xs) = rotate m xs &
   1.590 -    rotater n (rotate k xs) = rotate m xs &
   1.591 +  "\<forall>k. k = m + n \<longrightarrow> rotater k (rotate n xs) = rotater m xs \<and>
   1.592 +    rotate k (rotater n xs) = rotate m xs \<and>
   1.593 +    rotater n (rotate k xs) = rotate m xs \<and>
   1.594      rotate n (rotater k xs) = rotater m xs"
   1.595 -  unfolding rotater_def rotate_def
   1.596 -  by (induct n) (auto intro: funpow_swap1 [THEN trans])
   1.597 +  by (induct n) (auto simp: rotater_def rotate_def intro: funpow_swap1 [THEN trans])
   1.598  
   1.599  lemmas rotate_inv_rel = le_add_diff_inverse2 [symmetric, THEN rotate_inv_plus]
   1.600  
   1.601 @@ -3866,20 +3839,17 @@
   1.602  lemmas rotate_lr [simp] = rotate_inv_eq [THEN conjunct1]
   1.603  lemmas rotate_rl [simp] = rotate_inv_eq [THEN conjunct2, THEN conjunct1]
   1.604  
   1.605 -lemma rotate_gal: "(rotater n xs = ys) = (rotate n ys = xs)"
   1.606 +lemma rotate_gal: "rotater n xs = ys \<longleftrightarrow> rotate n ys = xs"
   1.607    by auto
   1.608  
   1.609 -lemma rotate_gal': "(ys = rotater n xs) = (xs = rotate n ys)"
   1.610 +lemma rotate_gal': "ys = rotater n xs \<longleftrightarrow> xs = rotate n ys"
   1.611    by auto
   1.612  
   1.613 -lemma length_rotater [simp]:
   1.614 -  "length (rotater n xs) = length xs"
   1.615 +lemma length_rotater [simp]: "length (rotater n xs) = length xs"
   1.616    by (simp add : rotater_rev)
   1.617  
   1.618 -lemma restrict_to_left:
   1.619 -  assumes "x = y"
   1.620 -  shows "(x = z) = (y = z)"
   1.621 -  using assms by simp
   1.622 +lemma restrict_to_left: "x = y \<Longrightarrow> x = z \<longleftrightarrow> y = z"
   1.623 +  by simp
   1.624  
   1.625  lemmas rrs0 = rotate_eqs [THEN restrict_to_left,
   1.626    simplified rotate_gal [symmetric] rotate_gal' [symmetric]]
   1.627 @@ -3891,34 +3861,30 @@
   1.628  
   1.629  subsubsection \<open>map, map2, commuting with rotate(r)\<close>
   1.630  
   1.631 -lemma butlast_map:
   1.632 -  "xs ~= [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)"
   1.633 +lemma butlast_map: "xs \<noteq> [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)"
   1.634    by (induct xs) auto
   1.635  
   1.636  lemma rotater1_map: "rotater1 (map f xs) = map f (rotater1 xs)"
   1.637 -  unfolding rotater1_def
   1.638 -  by (cases xs) (auto simp add: last_map butlast_map)
   1.639 -
   1.640 -lemma rotater_map:
   1.641 -  "rotater n (map f xs) = map f (rotater n xs)"
   1.642 -  unfolding rotater_def
   1.643 -  by (induct n) (auto simp add : rotater1_map)
   1.644 +  by (cases xs) (auto simp: rotater1_def last_map butlast_map)
   1.645 +
   1.646 +lemma rotater_map: "rotater n (map f xs) = map f (rotater n xs)"
   1.647 +  by (induct n) (auto simp: rotater_def rotater1_map)
   1.648  
   1.649  lemma but_last_zip [rule_format] :
   1.650 -  "ALL ys. length xs = length ys --> xs ~= [] -->
   1.651 -    last (zip xs ys) = (last xs, last ys) &
   1.652 +  "\<forall>ys. length xs = length ys \<longrightarrow> xs \<noteq> [] \<longrightarrow>
   1.653 +    last (zip xs ys) = (last xs, last ys) \<and>
   1.654      butlast (zip xs ys) = zip (butlast xs) (butlast ys)"
   1.655 -  apply (induct "xs")
   1.656 -  apply auto
   1.657 +  apply (induct xs)
   1.658 +   apply auto
   1.659       apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
   1.660    done
   1.661  
   1.662  lemma but_last_map2 [rule_format] :
   1.663 -  "ALL ys. length xs = length ys --> xs ~= [] -->
   1.664 -    last (map2 f xs ys) = f (last xs) (last ys) &
   1.665 +  "\<forall>ys. length xs = length ys \<longrightarrow> xs \<noteq> [] \<longrightarrow>
   1.666 +    last (map2 f xs ys) = f (last xs) (last ys) \<and>
   1.667      butlast (map2 f xs ys) = map2 f (butlast xs) (butlast ys)"
   1.668 -  apply (induct "xs")
   1.669 -  apply auto
   1.670 +  apply (induct xs)
   1.671 +   apply auto
   1.672       apply (unfold map2_def)
   1.673       apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
   1.674    done
   1.675 @@ -3927,7 +3893,7 @@
   1.676    "length xs = length ys \<Longrightarrow>
   1.677      rotater1 (zip xs ys) = zip (rotater1 xs) (rotater1 ys)"
   1.678    apply (unfold rotater1_def)
   1.679 -  apply (cases "xs")
   1.680 +  apply (cases xs)
   1.681     apply auto
   1.682     apply ((case_tac ys, auto simp: neq_Nil_conv but_last_zip)[1])+
   1.683    done
   1.684 @@ -3935,7 +3901,7 @@
   1.685  lemma rotater1_map2:
   1.686    "length xs = length ys \<Longrightarrow>
   1.687      rotater1 (map2 f xs ys) = map2 f (rotater1 xs) (rotater1 ys)"
   1.688 -  unfolding map2_def by (simp add: rotater1_map rotater1_zip)
   1.689 +  by (simp add: map2_def rotater1_map rotater1_zip)
   1.690  
   1.691  lemmas lrth =
   1.692    box_equals [OF asm_rl length_rotater [symmetric]
   1.693 @@ -3950,10 +3916,7 @@
   1.694  lemma rotate1_map2:
   1.695    "length xs = length ys \<Longrightarrow>
   1.696      rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)"
   1.697 -  apply (unfold map2_def)
   1.698 -  apply (cases xs)
   1.699 -   apply (cases ys, auto)+
   1.700 -  done
   1.701 +  by (cases xs; cases ys) (auto simp: map2_def)
   1.702  
   1.703  lemmas lth = box_equals [OF asm_rl length_rotate [symmetric]
   1.704    length_rotate [symmetric], THEN rotate1_map2]
   1.705 @@ -3966,8 +3929,7 @@
   1.706  
   1.707  \<comment> "corresponding equalities for word rotation"
   1.708  
   1.709 -lemma to_bl_rotl:
   1.710 -  "to_bl (word_rotl n w) = rotate n (to_bl w)"
   1.711 +lemma to_bl_rotl: "to_bl (word_rotl n w) = rotate n (to_bl w)"
   1.712    by (simp add: word_bl.Abs_inverse' word_rotl_def)
   1.713  
   1.714  lemmas blrs0 = rotate_eqs [THEN to_bl_rotl [THEN trans]]
   1.715 @@ -3975,8 +3937,7 @@
   1.716  lemmas word_rotl_eqs =
   1.717    blrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotl [symmetric]]
   1.718  
   1.719 -lemma to_bl_rotr:
   1.720 -  "to_bl (word_rotr n w) = rotater n (to_bl w)"
   1.721 +lemma to_bl_rotr: "to_bl (word_rotr n w) = rotater n (to_bl w)"
   1.722    by (simp add: word_bl.Abs_inverse' word_rotr_def)
   1.723  
   1.724  lemmas brrs0 = rotater_eqs [THEN to_bl_rotr [THEN trans]]
   1.725 @@ -3987,40 +3948,28 @@
   1.726  declare word_rotr_eqs (1) [simp]
   1.727  declare word_rotl_eqs (1) [simp]
   1.728  
   1.729 -lemma
   1.730 -  word_rot_rl [simp]:
   1.731 -  "word_rotl k (word_rotr k v) = v" and
   1.732 -  word_rot_lr [simp]:
   1.733 -  "word_rotr k (word_rotl k v) = v"
   1.734 +lemma word_rot_rl [simp]: "word_rotl k (word_rotr k v) = v"
   1.735 +  and word_rot_lr [simp]: "word_rotr k (word_rotl k v) = v"
   1.736    by (auto simp add: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric])
   1.737  
   1.738 -lemma
   1.739 -  word_rot_gal:
   1.740 -  "(word_rotr n v = w) = (word_rotl n w = v)" and
   1.741 -  word_rot_gal':
   1.742 -  "(w = word_rotr n v) = (v = word_rotl n w)"
   1.743 -  by (auto simp: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric]
   1.744 -           dest: sym)
   1.745 -
   1.746 -lemma word_rotr_rev:
   1.747 -  "word_rotr n w = word_reverse (word_rotl n (word_reverse w))"
   1.748 -  by (simp only: word_bl.Rep_inject [symmetric] to_bl_word_rev
   1.749 -                to_bl_rotr to_bl_rotl rotater_rev)
   1.750 +lemma word_rot_gal: "word_rotr n v = w \<longleftrightarrow> word_rotl n w = v"
   1.751 +  and word_rot_gal': "w = word_rotr n v \<longleftrightarrow> v = word_rotl n w"
   1.752 +  by (auto simp: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric] dest: sym)
   1.753 +
   1.754 +lemma word_rotr_rev: "word_rotr n w = word_reverse (word_rotl n (word_reverse w))"
   1.755 +  by (simp only: word_bl.Rep_inject [symmetric] to_bl_word_rev to_bl_rotr to_bl_rotl rotater_rev)
   1.756  
   1.757  lemma word_roti_0 [simp]: "word_roti 0 w = w"
   1.758 -  by (unfold word_rot_defs) auto
   1.759 +  by (auto simp: word_rot_defs)
   1.760  
   1.761  lemmas abl_cong = arg_cong [where f = "of_bl"]
   1.762  
   1.763 -lemma word_roti_add:
   1.764 -  "word_roti (m + n) w = word_roti m (word_roti n w)"
   1.765 +lemma word_roti_add: "word_roti (m + n) w = word_roti m (word_roti n w)"
   1.766  proof -
   1.767 -  have rotater_eq_lem:
   1.768 -    "\<And>m n xs. m = n \<Longrightarrow> rotater m xs = rotater n xs"
   1.769 +  have rotater_eq_lem: "\<And>m n xs. m = n \<Longrightarrow> rotater m xs = rotater n xs"
   1.770      by auto
   1.771  
   1.772 -  have rotate_eq_lem:
   1.773 -    "\<And>m n xs. m = n \<Longrightarrow> rotate m xs = rotate n xs"
   1.774 +  have rotate_eq_lem: "\<And>m n xs. m = n \<Longrightarrow> rotate m xs = rotate n xs"
   1.775      by auto
   1.776  
   1.777    note rpts [symmetric] =
   1.778 @@ -4033,17 +3982,17 @@
   1.779    note rrrp = trans [symmetric, OF rotater_add [symmetric] rotater_eq_lem]
   1.780  
   1.781    show ?thesis
   1.782 -  apply (unfold word_rot_defs)
   1.783 -  apply (simp only: split: if_split)
   1.784 -  apply (safe intro!: abl_cong)
   1.785 -  apply (simp_all only: to_bl_rotl [THEN word_bl.Rep_inverse']
   1.786 -                    to_bl_rotl
   1.787 -                    to_bl_rotr [THEN word_bl.Rep_inverse']
   1.788 -                    to_bl_rotr)
   1.789 -  apply (rule rrp rrrp rpts,
   1.790 -         simp add: nat_add_distrib [symmetric]
   1.791 -                   nat_diff_distrib [symmetric])+
   1.792 -  done
   1.793 +    apply (unfold word_rot_defs)
   1.794 +    apply (simp only: split: if_split)
   1.795 +    apply (safe intro!: abl_cong)
   1.796 +           apply (simp_all only: to_bl_rotl [THEN word_bl.Rep_inverse']
   1.797 +                  to_bl_rotl
   1.798 +                  to_bl_rotr [THEN word_bl.Rep_inverse']
   1.799 +                  to_bl_rotr)
   1.800 +         apply (rule rrp rrrp rpts,
   1.801 +                simp add: nat_add_distrib [symmetric]
   1.802 +                nat_diff_distrib [symmetric])+
   1.803 +    done
   1.804  qed
   1.805  
   1.806  lemma word_roti_conv_mod': "word_roti n w = word_roti (n mod int (size w)) w"
   1.807 @@ -4129,11 +4078,11 @@
   1.808  lemmas word_rotr_dt = bl_word_rotr_dt [THEN word_bl.Rep_inverse' [symmetric]]
   1.809  lemmas word_roti_dt = bl_word_roti_dt [THEN word_bl.Rep_inverse' [symmetric]]
   1.810  
   1.811 -lemma word_rotx_0 [simp] : "word_rotr i 0 = 0 & word_rotl i 0 = 0"
   1.812 -  by (simp add : word_rotr_dt word_rotl_dt replicate_add [symmetric])
   1.813 +lemma word_rotx_0 [simp] : "word_rotr i 0 = 0 \<and> word_rotl i 0 = 0"
   1.814 +  by (simp add: word_rotr_dt word_rotl_dt replicate_add [symmetric])
   1.815  
   1.816  lemma word_roti_0' [simp] : "word_roti n 0 = 0"
   1.817 -  unfolding word_roti_def by auto
   1.818 +  by (auto simp: word_roti_def)
   1.819  
   1.820  lemmas word_rotr_dt_no_bin' [simp] =
   1.821    word_rotr_dt [where w="numeral w", unfolded to_bl_numeral] for w
   1.822 @@ -4149,11 +4098,13 @@
   1.823  subsection \<open>Maximum machine word\<close>
   1.824  
   1.825  lemma word_int_cases:
   1.826 -  obtains n where "(x ::'a::len0 word) = word_of_int n" and "0 \<le> n" and "n < 2^len_of TYPE('a)"
   1.827 +  fixes x :: "'a::len0 word"
   1.828 +  obtains n where "x = word_of_int n" and "0 \<le> n" and "n < 2^len_of TYPE('a)"
   1.829    by (cases x rule: word_uint.Abs_cases) (simp add: uints_num)
   1.830  
   1.831  lemma word_nat_cases [cases type: word]:
   1.832 -  obtains n where "(x ::'a::len word) = of_nat n" and "n < 2^len_of TYPE('a)"
   1.833 +  fixes x :: "'a::len word"
   1.834 +  obtains n where "x = of_nat n" and "n < 2^len_of TYPE('a)"
   1.835    by (cases x rule: word_unat.Abs_cases) (simp add: unats_def)
   1.836  
   1.837  lemma max_word_eq: "(max_word::'a::len word) = 2^len_of TYPE('a) - 1"
   1.838 @@ -4166,62 +4117,55 @@
   1.839  lemma word_of_int_2p_len: "word_of_int (2 ^ len_of TYPE('a)) = (0::'a::len0 word)"
   1.840    by (subst word_uint.Abs_norm [symmetric]) simp
   1.841  
   1.842 -lemma word_pow_0:
   1.843 -  "(2::'a::len word) ^ len_of TYPE('a) = 0"
   1.844 +lemma word_pow_0: "(2::'a::len word) ^ len_of TYPE('a) = 0"
   1.845  proof -
   1.846    have "word_of_int (2 ^ len_of TYPE('a)) = (0::'a word)"
   1.847      by (rule word_of_int_2p_len)
   1.848 -  thus ?thesis by (simp add: word_of_int_2p)
   1.849 +  then show ?thesis by (simp add: word_of_int_2p)
   1.850  qed
   1.851  
   1.852  lemma max_word_wrap: "x + 1 = 0 \<Longrightarrow> x = max_word"
   1.853    apply (simp add: max_word_eq)
   1.854    apply uint_arith
   1.855 -  apply auto
   1.856 -  apply (simp add: word_pow_0)
   1.857 +  apply (auto simp: word_pow_0)
   1.858    done
   1.859  
   1.860 -lemma max_word_minus:
   1.861 -  "max_word = (-1::'a::len word)"
   1.862 +lemma max_word_minus: "max_word = (-1::'a::len word)"
   1.863  proof -
   1.864 -  have "-1 + 1 = (0::'a word)" by simp
   1.865 -  thus ?thesis by (rule max_word_wrap [symmetric])
   1.866 +  have "-1 + 1 = (0::'a word)"
   1.867 +    by simp
   1.868 +  then show ?thesis
   1.869 +    by (rule max_word_wrap [symmetric])
   1.870  qed
   1.871  
   1.872 -lemma max_word_bl [simp]:
   1.873 -  "to_bl (max_word::'a::len word) = replicate (len_of TYPE('a)) True"
   1.874 +lemma max_word_bl [simp]: "to_bl (max_word::'a::len word) = replicate (len_of TYPE('a)) True"
   1.875    by (subst max_word_minus to_bl_n1)+ simp
   1.876  
   1.877 -lemma max_test_bit [simp]:
   1.878 -  "(max_word::'a::len word) !! n = (n < len_of TYPE('a))"
   1.879 -  by (auto simp add: test_bit_bl word_size)
   1.880 -
   1.881 -lemma word_and_max [simp]:
   1.882 -  "x AND max_word = x"
   1.883 +lemma max_test_bit [simp]: "(max_word::'a::len word) !! n \<longleftrightarrow> n < len_of TYPE('a)"
   1.884 +  by (auto simp: test_bit_bl word_size)
   1.885 +
   1.886 +lemma word_and_max [simp]: "x AND max_word = x"
   1.887    by (rule word_eqI) (simp add: word_ops_nth_size word_size)
   1.888  
   1.889 -lemma word_or_max [simp]:
   1.890 -  "x OR max_word = max_word"
   1.891 +lemma word_or_max [simp]: "x OR max_word = max_word"
   1.892    by (rule word_eqI) (simp add: word_ops_nth_size word_size)
   1.893  
   1.894 -lemma word_ao_dist2:
   1.895 -  "x AND (y OR z) = x AND y OR x AND (z::'a::len0 word)"
   1.896 +lemma word_ao_dist2: "x AND (y OR z) = x AND y OR x AND z"
   1.897 +  for x y z :: "'a::len0 word"
   1.898    by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
   1.899  
   1.900 -lemma word_oa_dist2:
   1.901 -  "x OR y AND z = (x OR y) AND (x OR (z::'a::len0 word))"
   1.902 +lemma word_oa_dist2: "x OR y AND z = (x OR y) AND (x OR z)"
   1.903 +  for x y z :: "'a::len0 word"
   1.904    by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
   1.905  
   1.906 -lemma word_and_not [simp]:
   1.907 -  "x AND NOT x = (0::'a::len0 word)"
   1.908 +lemma word_and_not [simp]: "x AND NOT x = 0"
   1.909 +  for x :: "'a::len0 word"
   1.910    by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
   1.911  
   1.912 -lemma word_or_not [simp]:
   1.913 -  "x OR NOT x = max_word"
   1.914 +lemma word_or_not [simp]: "x OR NOT x = max_word"
   1.915    by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
   1.916  
   1.917 -lemma word_boolean:
   1.918 -  "boolean (op AND) (op OR) bitNOT 0 max_word"
   1.919 +lemma word_boolean: "boolean (op AND) (op OR) bitNOT 0 max_word"
   1.920    apply (rule boolean.intro)
   1.921             apply (rule word_bw_assocs)
   1.922            apply (rule word_bw_assocs)
   1.923 @@ -4235,48 +4179,42 @@
   1.924    apply (rule word_or_not)
   1.925    done
   1.926  
   1.927 -interpretation word_bool_alg:
   1.928 -  boolean "op AND" "op OR" bitNOT 0 max_word
   1.929 +interpretation word_bool_alg: boolean "op AND" "op OR" bitNOT 0 max_word
   1.930    by (rule word_boolean)
   1.931  
   1.932 -lemma word_xor_and_or:
   1.933 -  "x XOR y = x AND NOT y OR NOT x AND (y::'a::len0 word)"
   1.934 +lemma word_xor_and_or: "x XOR y = x AND NOT y OR NOT x AND y"
   1.935 +  for x y :: "'a::len0 word"
   1.936    by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
   1.937  
   1.938 -interpretation word_bool_alg:
   1.939 -  boolean_xor "op AND" "op OR" bitNOT 0 max_word "op XOR"
   1.940 +interpretation word_bool_alg: boolean_xor "op AND" "op OR" bitNOT 0 max_word "op XOR"
   1.941    apply (rule boolean_xor.intro)
   1.942     apply (rule word_boolean)
   1.943    apply (rule boolean_xor_axioms.intro)
   1.944    apply (rule word_xor_and_or)
   1.945    done
   1.946  
   1.947 -lemma shiftr_x_0 [iff]:
   1.948 -  "(x::'a::len0 word) >> 0 = x"
   1.949 +lemma shiftr_x_0 [iff]: "x >> 0 = x"
   1.950 +  for x :: "'a::len0 word"
   1.951    by (simp add: shiftr_bl)
   1.952  
   1.953 -lemma shiftl_x_0 [simp]:
   1.954 -  "(x :: 'a::len word) << 0 = x"
   1.955 +lemma shiftl_x_0 [simp]: "x << 0 = x"
   1.956 +  for x :: "'a::len word"
   1.957    by (simp add: shiftl_t2n)
   1.958  
   1.959 -lemma shiftl_1 [simp]:
   1.960 -  "(1::'a::len word) << n = 2^n"
   1.961 +lemma shiftl_1 [simp]: "(1::'a::len word) << n = 2^n"
   1.962    by (simp add: shiftl_t2n)
   1.963  
   1.964 -lemma uint_lt_0 [simp]:
   1.965 -  "uint x < 0 = False"
   1.966 +lemma uint_lt_0 [simp]: "uint x < 0 = False"
   1.967    by (simp add: linorder_not_less)
   1.968  
   1.969 -lemma shiftr1_1 [simp]:
   1.970 -  "shiftr1 (1::'a::len word) = 0"
   1.971 +lemma shiftr1_1 [simp]: "shiftr1 (1::'a::len word) = 0"
   1.972    unfolding shiftr1_def by simp
   1.973  
   1.974 -lemma shiftr_1[simp]:
   1.975 -  "(1::'a::len word) >> n = (if n = 0 then 1 else 0)"
   1.976 +lemma shiftr_1[simp]: "(1::'a::len word) >> n = (if n = 0 then 1 else 0)"
   1.977    by (induct n) (auto simp: shiftr_def)
   1.978  
   1.979 -lemma word_less_1 [simp]:
   1.980 -  "((x::'a::len word) < 1) = (x = 0)"
   1.981 +lemma word_less_1 [simp]: "x < 1 \<longleftrightarrow> x = 0"
   1.982 +  for x :: "'a::len word"
   1.983    by (simp add: word_less_nat_alt unat_0_iff)
   1.984  
   1.985  lemma to_bl_mask:
   1.986 @@ -4287,33 +4225,29 @@
   1.987  
   1.988  lemma map_replicate_True:
   1.989    "n = length xs \<Longrightarrow>
   1.990 -    map (\<lambda>(x,y). x & y) (zip xs (replicate n True)) = xs"
   1.991 +    map (\<lambda>(x,y). x \<and> y) (zip xs (replicate n True)) = xs"
   1.992    by (induct xs arbitrary: n) auto
   1.993  
   1.994  lemma map_replicate_False:
   1.995 -  "n = length xs \<Longrightarrow> map (\<lambda>(x,y). x & y)
   1.996 +  "n = length xs \<Longrightarrow> map (\<lambda>(x,y). x \<and> y)
   1.997      (zip xs (replicate n False)) = replicate n False"
   1.998    by (induct xs arbitrary: n) auto
   1.999  
  1.1000  lemma bl_and_mask:
  1.1001    fixes w :: "'a::len word"
  1.1002 -  fixes n
  1.1003 +    and n :: nat
  1.1004    defines "n' \<equiv> len_of TYPE('a) - n"
  1.1005 -  shows "to_bl (w AND mask n) =  replicate n' False @ drop n' (to_bl w)"
  1.1006 +  shows "to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)"
  1.1007  proof -
  1.1008    note [simp] = map_replicate_True map_replicate_False
  1.1009 -  have "to_bl (w AND mask n) =
  1.1010 -        map2 op & (to_bl w) (to_bl (mask n::'a::len word))"
  1.1011 +  have "to_bl (w AND mask n) = map2 op \<and> (to_bl w) (to_bl (mask n::'a::len word))"
  1.1012      by (simp add: bl_word_and)
  1.1013 -  also
  1.1014 -  have "to_bl w = take n' (to_bl w) @ drop n' (to_bl w)" by simp
  1.1015 -  also
  1.1016 -  have "map2 op & \<dots> (to_bl (mask n::'a::len word)) =
  1.1017 -        replicate n' False @ drop n' (to_bl w)"
  1.1018 -    unfolding to_bl_mask n'_def map2_def
  1.1019 -    by (subst zip_append) auto
  1.1020 -  finally
  1.1021 -  show ?thesis .
  1.1022 +  also have "to_bl w = take n' (to_bl w) @ drop n' (to_bl w)"
  1.1023 +    by simp
  1.1024 +  also have "map2 op \<and> \<dots> (to_bl (mask n::'a::len word)) =
  1.1025 +      replicate n' False @ drop n' (to_bl w)"
  1.1026 +    unfolding to_bl_mask n'_def map2_def by (subst zip_append) auto
  1.1027 +  finally show ?thesis .
  1.1028  qed
  1.1029  
  1.1030  lemma drop_rev_takefill:
  1.1031 @@ -4321,61 +4255,53 @@
  1.1032      drop (n - length xs) (rev (takefill False n (rev xs))) = xs"
  1.1033    by (simp add: takefill_alt rev_take)
  1.1034  
  1.1035 -lemma map_nth_0 [simp]:
  1.1036 -  "map (op !! (0::'a::len0 word)) xs = replicate (length xs) False"
  1.1037 +lemma map_nth_0 [simp]: "map (op !! (0::'a::len0 word)) xs = replicate (length xs) False"
  1.1038    by (induct xs) auto
  1.1039  
  1.1040  lemma uint_plus_if_size:
  1.1041    "uint (x + y) =
  1.1042 -  (if uint x + uint y < 2^size x then
  1.1043 -      uint x + uint y
  1.1044 -   else
  1.1045 -      uint x + uint y - 2^size x)"
  1.1046 -  by (simp add: word_arith_wis int_word_uint mod_add_if_z
  1.1047 -                word_size)
  1.1048 +    (if uint x + uint y < 2^size x
  1.1049 +     then uint x + uint y
  1.1050 +     else uint x + uint y - 2^size x)"
  1.1051 +  by (simp add: word_arith_wis int_word_uint mod_add_if_z word_size)
  1.1052  
  1.1053  lemma unat_plus_if_size:
  1.1054    "unat (x + (y::'a::len word)) =
  1.1055 -  (if unat x + unat y < 2^size x then
  1.1056 -      unat x + unat y
  1.1057 -   else
  1.1058 -      unat x + unat y - 2^size x)"
  1.1059 +    (if unat x + unat y < 2^size x
  1.1060 +     then unat x + unat y
  1.1061 +     else unat x + unat y - 2^size x)"
  1.1062    apply (subst word_arith_nat_defs)
  1.1063    apply (subst unat_of_nat)
  1.1064    apply (simp add:  mod_nat_add word_size)
  1.1065    done
  1.1066  
  1.1067 -lemma word_neq_0_conv:
  1.1068 -  fixes w :: "'a::len word"
  1.1069 -  shows "(w \<noteq> 0) = (0 < w)"
  1.1070 -  unfolding word_gt_0 by simp
  1.1071 -
  1.1072 -lemma max_lt:
  1.1073 -  "unat (max a b div c) = unat (max a b) div unat (c:: 'a::len word)"
  1.1074 +lemma word_neq_0_conv: "w \<noteq> 0 \<longleftrightarrow> 0 < w"
  1.1075 +  for w :: "'a::len word"
  1.1076 +  by (simp add: word_gt_0)
  1.1077 +
  1.1078 +lemma max_lt: "unat (max a b div c) = unat (max a b) div unat c"
  1.1079 +  for c :: "'a::len word"
  1.1080    by (fact unat_div)
  1.1081  
  1.1082  lemma uint_sub_if_size:
  1.1083    "uint (x - y) =
  1.1084 -  (if uint y \<le> uint x then
  1.1085 -      uint x - uint y
  1.1086 -   else
  1.1087 -      uint x - uint y + 2^size x)"
  1.1088 -  by (simp add: word_arith_wis int_word_uint mod_sub_if_z
  1.1089 -                word_size)
  1.1090 -
  1.1091 -lemma unat_sub:
  1.1092 -  "b <= a \<Longrightarrow> unat (a - b) = unat a - unat b"
  1.1093 +    (if uint y \<le> uint x
  1.1094 +     then uint x - uint y
  1.1095 +     else uint x - uint y + 2^size x)"
  1.1096 +  by (simp add: word_arith_wis int_word_uint mod_sub_if_z word_size)
  1.1097 +
  1.1098 +lemma unat_sub: "b \<le> a \<Longrightarrow> unat (a - b) = unat a - unat b"
  1.1099    by (simp add: unat_def uint_sub_if_size word_le_def nat_diff_distrib)
  1.1100  
  1.1101  lemmas word_less_sub1_numberof [simp] = word_less_sub1 [of "numeral w"] for w
  1.1102  lemmas word_le_sub1_numberof [simp] = word_le_sub1 [of "numeral w"] for w
  1.1103  
  1.1104 -lemma word_of_int_minus:
  1.1105 -  "word_of_int (2^len_of TYPE('a) - i) = (word_of_int (-i)::'a::len word)"
  1.1106 +lemma word_of_int_minus: "word_of_int (2^len_of TYPE('a) - i) = (word_of_int (-i)::'a::len word)"
  1.1107  proof -
  1.1108 -  have x: "2^len_of TYPE('a) - i = -i + 2^len_of TYPE('a)" by simp
  1.1109 +  have *: "2^len_of TYPE('a) - i = -i + 2^len_of TYPE('a)"
  1.1110 +    by simp
  1.1111    show ?thesis
  1.1112 -    apply (subst x)
  1.1113 +    apply (subst *)
  1.1114      apply (subst word_uint.Abs_norm [symmetric], subst mod_add_self2)
  1.1115      apply simp
  1.1116      done
  1.1117 @@ -4384,35 +4310,37 @@
  1.1118  lemmas word_of_int_inj =
  1.1119    word_uint.Abs_inject [unfolded uints_num, simplified]
  1.1120  
  1.1121 -lemma word_le_less_eq:
  1.1122 -  "(x ::'z::len word) \<le> y = (x = y \<or> x < y)"
  1.1123 +lemma word_le_less_eq: "x \<le> y \<longleftrightarrow> x = y \<or> x < y"
  1.1124 +  for x y :: "'z::len word"
  1.1125    by (auto simp add: order_class.le_less)
  1.1126  
  1.1127  lemma mod_plus_cong:
  1.1128 -  assumes 1: "(b::int) = b'"
  1.1129 -      and 2: "x mod b' = x' mod b'"
  1.1130 -      and 3: "y mod b' = y' mod b'"
  1.1131 -      and 4: "x' + y' = z'"
  1.1132 +  fixes b b' :: int
  1.1133 +  assumes 1: "b = b'"
  1.1134 +    and 2: "x mod b' = x' mod b'"
  1.1135 +    and 3: "y mod b' = y' mod b'"
  1.1136 +    and 4: "x' + y' = z'"
  1.1137    shows "(x + y) mod b = z' mod b'"
  1.1138  proof -
  1.1139    from 1 2[symmetric] 3[symmetric] have "(x + y) mod b = (x' mod b' + y' mod b') mod b'"
  1.1140      by (simp add: mod_add_eq)
  1.1141    also have "\<dots> = (x' + y') mod b'"
  1.1142      by (simp add: mod_add_eq)
  1.1143 -  finally show ?thesis by (simp add: 4)
  1.1144 +  finally show ?thesis
  1.1145 +    by (simp add: 4)
  1.1146  qed
  1.1147  
  1.1148  lemma mod_minus_cong:
  1.1149 -  assumes 1: "(b::int) = b'"
  1.1150 -      and 2: "x mod b' = x' mod b'"
  1.1151 -      and 3: "y mod b' = y' mod b'"
  1.1152 -      and 4: "x' - y' = z'"
  1.1153 +  fixes b b' :: int
  1.1154 +  assumes "b = b'"
  1.1155 +    and "x mod b' = x' mod b'"
  1.1156 +    and "y mod b' = y' mod b'"
  1.1157 +    and "x' - y' = z'"
  1.1158    shows "(x - y) mod b = z' mod b'"
  1.1159 -  using 1 2 3 4 [symmetric]
  1.1160 -  by (auto intro: mod_diff_cong)
  1.1161 -
  1.1162 -lemma word_induct_less:
  1.1163 -  "\<lbrakk>P (0::'a::len word); \<And>n. \<lbrakk>n < m; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
  1.1164 +  using assms [symmetric] by (auto intro: mod_diff_cong)
  1.1165 +
  1.1166 +lemma word_induct_less: "\<lbrakk>P 0; \<And>n. \<lbrakk>n < m; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
  1.1167 +  for P :: "'a::len word \<Rightarrow> bool"
  1.1168    apply (cases m)
  1.1169    apply atomize
  1.1170    apply (erule rev_mp)+
  1.1171 @@ -4434,22 +4362,23 @@
  1.1172    apply simp
  1.1173    done
  1.1174  
  1.1175 -lemma word_induct:
  1.1176 -  "\<lbrakk>P (0::'a::len word); \<And>n. P n \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
  1.1177 -  by (erule word_induct_less, simp)
  1.1178 -
  1.1179 -lemma word_induct2 [induct type]:
  1.1180 -  "\<lbrakk>P 0; \<And>n. \<lbrakk>1 + n \<noteq> 0; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P (n::'b::len word)"
  1.1181 -  apply (rule word_induct, simp)
  1.1182 -  apply (case_tac "1+n = 0", auto)
  1.1183 +lemma word_induct: "\<lbrakk>P 0; \<And>n. P n \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
  1.1184 +  for P :: "'a::len word \<Rightarrow> bool"
  1.1185 +  by (erule word_induct_less) simp
  1.1186 +
  1.1187 +lemma word_induct2 [induct type]: "\<lbrakk>P 0; \<And>n. \<lbrakk>1 + n \<noteq> 0; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P n"
  1.1188 +  for P :: "'b::len word \<Rightarrow> bool"
  1.1189 +  apply (rule word_induct)
  1.1190 +   apply simp
  1.1191 +  apply (case_tac "1 + n = 0")
  1.1192 +   apply auto
  1.1193    done
  1.1194  
  1.1195  
  1.1196  subsection \<open>Recursion combinator for words\<close>
  1.1197  
  1.1198  definition word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a"
  1.1199 -where
  1.1200 -  "word_rec forZero forSuc n = rec_nat forZero (forSuc \<circ> of_nat) (unat n)"
  1.1201 +  where "word_rec forZero forSuc n = rec_nat forZero (forSuc \<circ> of_nat) (unat n)"
  1.1202  
  1.1203  lemma word_rec_0: "word_rec z s 0 = z"
  1.1204    by (simp add: word_rec_def)
  1.1205 @@ -4471,79 +4400,75 @@
  1.1206    apply simp
  1.1207    done
  1.1208  
  1.1209 -lemma word_rec_in:
  1.1210 -  "f (word_rec z (\<lambda>_. f) n) = word_rec (f z) (\<lambda>_. f) n"
  1.1211 +lemma word_rec_in: "f (word_rec z (\<lambda>_. f) n) = word_rec (f z) (\<lambda>_. f) n"
  1.1212    by (induct n) (simp_all add: word_rec_0 word_rec_Suc)
  1.1213  
  1.1214 -lemma word_rec_in2:
  1.1215 -  "f n (word_rec z f n) = word_rec (f 0 z) (f \<circ> op + 1) n"
  1.1216 +lemma word_rec_in2: "f n (word_rec z f n) = word_rec (f 0 z) (f \<circ> op + 1) n"
  1.1217    by (induct n) (simp_all add: word_rec_0 word_rec_Suc)
  1.1218  
  1.1219  lemma word_rec_twice:
  1.1220    "m \<le> n \<Longrightarrow> word_rec z f n = word_rec (word_rec z f (n - m)) (f \<circ> op + (n - m)) m"
  1.1221 -apply (erule rev_mp)
  1.1222 -apply (rule_tac x=z in spec)
  1.1223 -apply (rule_tac x=f in spec)
  1.1224 -apply (induct n)
  1.1225 - apply (simp add: word_rec_0)
  1.1226 -apply clarsimp
  1.1227 -apply (rule_tac t="1 + n - m" and s="1 + (n - m)" in subst)
  1.1228 - apply simp
  1.1229 -apply (case_tac "1 + (n - m) = 0")
  1.1230 - apply (simp add: word_rec_0)
  1.1231 - apply (rule_tac f = "word_rec a b" for a b in arg_cong)
  1.1232 - apply (rule_tac t="m" and s="m + (1 + (n - m))" in subst)
  1.1233 +  apply (erule rev_mp)
  1.1234 +  apply (rule_tac x=z in spec)
  1.1235 +  apply (rule_tac x=f in spec)
  1.1236 +  apply (induct n)
  1.1237 +   apply (simp add: word_rec_0)
  1.1238 +  apply clarsimp
  1.1239 +  apply (rule_tac t="1 + n - m" and s="1 + (n - m)" in subst)
  1.1240 +   apply simp
  1.1241 +  apply (case_tac "1 + (n - m) = 0")
  1.1242 +   apply (simp add: word_rec_0)
  1.1243 +   apply (rule_tac f = "word_rec a b" for a b in arg_cong)
  1.1244 +   apply (rule_tac t="m" and s="m + (1 + (n - m))" in subst)
  1.1245 +    apply simp
  1.1246 +   apply (simp (no_asm_use))
  1.1247 +  apply (simp add: word_rec_Suc word_rec_in2)
  1.1248 +  apply (erule impE)
  1.1249 +   apply uint_arith
  1.1250 +  apply (drule_tac x="x \<circ> op + 1" in spec)
  1.1251 +  apply (drule_tac x="x 0 xa" in spec)
  1.1252    apply simp
  1.1253 - apply (simp (no_asm_use))
  1.1254 -apply (simp add: word_rec_Suc word_rec_in2)
  1.1255 -apply (erule impE)
  1.1256 - apply uint_arith
  1.1257 -apply (drule_tac x="x \<circ> op + 1" in spec)
  1.1258 -apply (drule_tac x="x 0 xa" in spec)
  1.1259 -apply simp
  1.1260 -apply (rule_tac t="\<lambda>a. x (1 + (n - m + a))" and s="\<lambda>a. x (1 + (n - m) + a)"
  1.1261 -       in subst)
  1.1262 - apply (clarsimp simp add: fun_eq_iff)
  1.1263 - apply (rule_tac t="(1 + (n - m + xb))" and s="1 + (n - m) + xb" in subst)
  1.1264 -  apply simp
  1.1265 - apply (rule refl)
  1.1266 -apply (rule refl)
  1.1267 -done
  1.1268 +  apply (rule_tac t="\<lambda>a. x (1 + (n - m + a))" and s="\<lambda>a. x (1 + (n - m) + a)" in subst)
  1.1269 +   apply (clarsimp simp add: fun_eq_iff)
  1.1270 +   apply (rule_tac t="(1 + (n - m + xb))" and s="1 + (n - m) + xb" in subst)
  1.1271 +    apply simp
  1.1272 +   apply (rule refl)
  1.1273 +  apply (rule refl)
  1.1274 +  done
  1.1275  
  1.1276  lemma word_rec_id: "word_rec z (\<lambda>_. id) n = z"
  1.1277    by (induct n) (auto simp add: word_rec_0 word_rec_Suc)
  1.1278  
  1.1279  lemma word_rec_id_eq: "\<forall>m < n. f m = id \<Longrightarrow> word_rec z f n = z"
  1.1280 -apply (erule rev_mp)
  1.1281 -apply (induct n)
  1.1282 - apply (auto simp add: word_rec_0 word_rec_Suc)
  1.1283 - apply (drule spec, erule mp)
  1.1284 - apply uint_arith
  1.1285 -apply (drule_tac x=n in spec, erule impE)
  1.1286 - apply uint_arith
  1.1287 -apply simp
  1.1288 -done
  1.1289 +  apply (erule rev_mp)
  1.1290 +  apply (induct n)
  1.1291 +   apply (auto simp add: word_rec_0 word_rec_Suc)
  1.1292 +   apply (drule spec, erule mp)
  1.1293 +   apply uint_arith
  1.1294 +  apply (drule_tac x=n in spec, erule impE)
  1.1295 +   apply uint_arith
  1.1296 +  apply simp
  1.1297 +  done
  1.1298  
  1.1299  lemma word_rec_max:
  1.1300    "\<forall>m\<ge>n. m \<noteq> - 1 \<longrightarrow> f m = id \<Longrightarrow> word_rec z f (- 1) = word_rec z f n"
  1.1301 -apply (subst word_rec_twice[where n="-1" and m="-1 - n"])
  1.1302 - apply simp
  1.1303 -apply simp
  1.1304 -apply (rule word_rec_id_eq)
  1.1305 -apply clarsimp
  1.1306 -apply (drule spec, rule mp, erule mp)
  1.1307 - apply (rule word_plus_mono_right2[OF _ order_less_imp_le])
  1.1308 -  prefer 2
  1.1309 -  apply assumption
  1.1310 - apply simp
  1.1311 -apply (erule contrapos_pn)
  1.1312 -apply simp
  1.1313 -apply (drule arg_cong[where f="\<lambda>x. x - n"])
  1.1314 -apply simp
  1.1315 -done
  1.1316 -
  1.1317 -lemma unatSuc:
  1.1318 -  "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> unat (1 + n) = Suc (unat n)"
  1.1319 +  apply (subst word_rec_twice[where n="-1" and m="-1 - n"])
  1.1320 +   apply simp
  1.1321 +  apply simp
  1.1322 +  apply (rule word_rec_id_eq)
  1.1323 +  apply clarsimp
  1.1324 +  apply (drule spec, rule mp, erule mp)
  1.1325 +   apply (rule word_plus_mono_right2[OF _ order_less_imp_le])
  1.1326 +    prefer 2
  1.1327 +    apply assumption
  1.1328 +   apply simp
  1.1329 +  apply (erule contrapos_pn)
  1.1330 +  apply simp
  1.1331 +  apply (drule arg_cong[where f="\<lambda>x. x - n"])
  1.1332 +  apply simp
  1.1333 +  done
  1.1334 +
  1.1335 +lemma unatSuc: "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> unat (1 + n) = Suc (unat n)"
  1.1336    by unat_arith
  1.1337  
  1.1338  declare bin_to_bl_def [simp]