merged
authorwenzelm
Mon Mar 20 21:53:37 2017 +0100 (2017-03-20)
changeset 6533727144776aefe
parent 65330 d83f709b7580
parent 65336 8e5274fc0093
child 65338 2ffda850f844
merged
     1.1 --- a/src/HOL/Word/Tools/smt_word.ML	Mon Mar 20 21:01:47 2017 +0100
     1.2 +++ b/src/HOL/Word/Tools/smt_word.ML	Mon Mar 20 21:53:37 2017 +0100
     1.3 @@ -99,30 +99,30 @@
     1.4  val setup_builtins =
     1.5    SMT_Builtin.add_builtin_typ smtlibC (wordT, word_typ, word_num) #>
     1.6    fold (add_word_fun if_fixed_all) [
     1.7 -    (@{term "uminus :: 'a::len word => _"}, "bvneg"),
     1.8 -    (@{term "plus :: 'a::len word => _"}, "bvadd"),
     1.9 -    (@{term "minus :: 'a::len word => _"}, "bvsub"),
    1.10 -    (@{term "times :: 'a::len word => _"}, "bvmul"),
    1.11 -    (@{term "bitNOT :: 'a::len word => _"}, "bvnot"),
    1.12 -    (@{term "bitAND :: 'a::len word => _"}, "bvand"),
    1.13 -    (@{term "bitOR :: 'a::len word => _"}, "bvor"),
    1.14 -    (@{term "bitXOR :: 'a::len word => _"}, "bvxor"),
    1.15 -    (@{term "word_cat :: 'a::len word => _"}, "concat") ] #>
    1.16 +    (@{term "uminus :: 'a::len word \<Rightarrow> _"}, "bvneg"),
    1.17 +    (@{term "plus :: 'a::len word \<Rightarrow> _"}, "bvadd"),
    1.18 +    (@{term "minus :: 'a::len word \<Rightarrow> _"}, "bvsub"),
    1.19 +    (@{term "times :: 'a::len word \<Rightarrow> _"}, "bvmul"),
    1.20 +    (@{term "bitNOT :: 'a::len word \<Rightarrow> _"}, "bvnot"),
    1.21 +    (@{term "bitAND :: 'a::len word \<Rightarrow> _"}, "bvand"),
    1.22 +    (@{term "bitOR :: 'a::len word \<Rightarrow> _"}, "bvor"),
    1.23 +    (@{term "bitXOR :: 'a::len word \<Rightarrow> _"}, "bvxor"),
    1.24 +    (@{term "word_cat :: 'a::len word \<Rightarrow> _"}, "concat") ] #>
    1.25    fold (add_word_fun shift) [
    1.26 -    (@{term "shiftl :: 'a::len word => _ "}, "bvshl"),
    1.27 -    (@{term "shiftr :: 'a::len word => _"}, "bvlshr"),
    1.28 -    (@{term "sshiftr :: 'a::len word => _"}, "bvashr") ] #>
    1.29 +    (@{term "shiftl :: 'a::len word \<Rightarrow> _ "}, "bvshl"),
    1.30 +    (@{term "shiftr :: 'a::len word \<Rightarrow> _"}, "bvlshr"),
    1.31 +    (@{term "sshiftr :: 'a::len word \<Rightarrow> _"}, "bvashr") ] #>
    1.32    add_word_fun extract
    1.33 -    (@{term "slice :: _ => 'a::len word => _"}, "extract") #>
    1.34 +    (@{term "slice :: _ \<Rightarrow> 'a::len word \<Rightarrow> _"}, "extract") #>
    1.35    fold (add_word_fun extend) [
    1.36 -    (@{term "ucast :: 'a::len word => _"}, "zero_extend"),
    1.37 -    (@{term "scast :: 'a::len word => _"}, "sign_extend") ] #>
    1.38 +    (@{term "ucast :: 'a::len word \<Rightarrow> _"}, "zero_extend"),
    1.39 +    (@{term "scast :: 'a::len word \<Rightarrow> _"}, "sign_extend") ] #>
    1.40    fold (add_word_fun rotate) [
    1.41      (@{term word_rotl}, "rotate_left"),
    1.42      (@{term word_rotr}, "rotate_right") ] #>
    1.43    fold (add_word_fun if_fixed_args) [
    1.44 -    (@{term "less :: 'a::len word => _"}, "bvult"),
    1.45 -    (@{term "less_eq :: 'a::len word => _"}, "bvule"),
    1.46 +    (@{term "less :: 'a::len word \<Rightarrow> _"}, "bvult"),
    1.47 +    (@{term "less_eq :: 'a::len word \<Rightarrow> _"}, "bvule"),
    1.48      (@{term word_sless}, "bvslt"),
    1.49      (@{term word_sle}, "bvsle") ]
    1.50  
     2.1 --- a/src/HOL/Word/Word.thy	Mon Mar 20 21:01:47 2017 +0100
     2.2 +++ b/src/HOL/Word/Word.thy	Mon Mar 20 21:53:37 2017 +0100
     2.3 @@ -3315,25 +3315,21 @@
     2.4    apply (simp add: word_size)
     2.5    done
     2.6  
     2.7 -lemma nth_slice:
     2.8 -  "(slice n w :: 'a::len0 word) !! m =
     2.9 -   (w !! (m + n) & m < len_of TYPE('a))"
    2.10 -  unfolding slice_shiftr
    2.11 -  by (simp add : nth_ucast nth_shiftr)
    2.12 +lemma nth_slice: "(slice n w :: 'a::len0 word) !! m = (w !! (m + n) \<and> m < len_of TYPE('a))"
    2.13 +  by (simp add: slice_shiftr nth_ucast nth_shiftr)
    2.14  
    2.15  lemma slice1_down_alt':
    2.16    "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs + k = n \<Longrightarrow>
    2.17      to_bl sl = takefill False fs (drop k (to_bl w))"
    2.18 -  unfolding slice1_def word_size of_bl_def uint_bl
    2.19 -  by (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop drop_takefill)
    2.20 +  by (auto simp: slice1_def word_size of_bl_def uint_bl
    2.21 +      word_ubin.eq_norm bl_bin_bl_rep_drop drop_takefill)
    2.22  
    2.23  lemma slice1_up_alt':
    2.24    "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs = n + k \<Longrightarrow>
    2.25      to_bl sl = takefill False fs (replicate k False @ (to_bl w))"
    2.26    apply (unfold slice1_def word_size of_bl_def uint_bl)
    2.27 -  apply (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop
    2.28 -                        takefill_append [symmetric])
    2.29 -  apply (rule_tac f = "%k. takefill False (len_of TYPE('a))
    2.30 +  apply (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop takefill_append [symmetric])
    2.31 +  apply (rule_tac f = "\<lambda>k. takefill False (len_of TYPE('a))
    2.32      (replicate k False @ bin_to_bl (len_of TYPE('b)) (uint w))" in arg_cong)
    2.33    apply arith
    2.34    done
    2.35 @@ -3346,42 +3342,40 @@
    2.36    le_add_diff_inverse2 [symmetric, THEN su1]
    2.37  
    2.38  lemma ucast_slice1: "ucast w = slice1 (size w) w"
    2.39 -  unfolding slice1_def ucast_bl
    2.40 -  by (simp add : takefill_same' word_size)
    2.41 +  by (simp add: slice1_def ucast_bl takefill_same' word_size)
    2.42  
    2.43  lemma ucast_slice: "ucast w = slice 0 w"
    2.44 -  unfolding slice_def by (simp add : ucast_slice1)
    2.45 +  by (simp add: slice_def ucast_slice1)
    2.46  
    2.47  lemma slice_id: "slice 0 t = t"
    2.48    by (simp only: ucast_slice [symmetric] ucast_id)
    2.49  
    2.50 -lemma revcast_slice1 [OF refl]:
    2.51 -  "rc = revcast w \<Longrightarrow> slice1 (size rc) w = rc"
    2.52 -  unfolding slice1_def revcast_def' by (simp add : word_size)
    2.53 +lemma revcast_slice1 [OF refl]: "rc = revcast w \<Longrightarrow> slice1 (size rc) w = rc"
    2.54 +  by (simp add: slice1_def revcast_def' word_size)
    2.55  
    2.56  lemma slice1_tf_tf':
    2.57    "to_bl (slice1 n w :: 'a::len0 word) =
    2.58 -   rev (takefill False (len_of TYPE('a)) (rev (takefill False n (to_bl w))))"
    2.59 +    rev (takefill False (len_of TYPE('a)) (rev (takefill False n (to_bl w))))"
    2.60    unfolding slice1_def by (rule word_rev_tf)
    2.61  
    2.62  lemmas slice1_tf_tf = slice1_tf_tf' [THEN word_bl.Rep_inverse', symmetric]
    2.63  
    2.64  lemma rev_slice1:
    2.65    "n + k = len_of TYPE('a) + len_of TYPE('b) \<Longrightarrow>
    2.66 -  slice1 n (word_reverse w :: 'b::len0 word) =
    2.67 -  word_reverse (slice1 k w :: 'a::len0 word)"
    2.68 +    slice1 n (word_reverse w :: 'b::len0 word) =
    2.69 +    word_reverse (slice1 k w :: 'a::len0 word)"
    2.70    apply (unfold word_reverse_def slice1_tf_tf)
    2.71    apply (rule word_bl.Rep_inverse')
    2.72    apply (rule rev_swap [THEN iffD1])
    2.73    apply (rule trans [symmetric])
    2.74 -  apply (rule tf_rev)
    2.75 +   apply (rule tf_rev)
    2.76     apply (simp add: word_bl.Abs_inverse)
    2.77    apply (simp add: word_bl.Abs_inverse)
    2.78    done
    2.79  
    2.80  lemma rev_slice:
    2.81    "n + k + len_of TYPE('a::len0) = len_of TYPE('b::len0) \<Longrightarrow>
    2.82 -    slice n (word_reverse (w::'b word)) = word_reverse (slice k w::'a word)"
    2.83 +    slice n (word_reverse (w::'b word)) = word_reverse (slice k w :: 'a word)"
    2.84    apply (unfold slice_def word_size)
    2.85    apply (rule rev_slice1)
    2.86    apply arith
    2.87 @@ -3394,8 +3388,9 @@
    2.88        criterion for overflow of addition of signed integers\<close>
    2.89  
    2.90  lemma sofl_test:
    2.91 -  "(sint (x :: 'a::len word) + sint y = sint (x + y)) =
    2.92 -     ((((x+y) XOR x) AND ((x+y) XOR y)) >> (size x - 1) = 0)"
    2.93 +  "(sint x + sint y = sint (x + y)) =
    2.94 +     ((((x + y) XOR x) AND ((x + y) XOR y)) >> (size x - 1) = 0)"
    2.95 +  for x y :: "'a::len word"
    2.96    apply (unfold word_size)
    2.97    apply (cases "len_of TYPE('a)", simp)
    2.98    apply (subst msb_shift [THEN sym_notr])
    2.99 @@ -3406,19 +3401,19 @@
   2.100       apply (unfold sint_word_ariths)
   2.101       apply (unfold word_sbin.set_iff_norm [symmetric] sints_num)
   2.102       apply safe
   2.103 -        apply (insert sint_range' [where x=x])
   2.104 -        apply (insert sint_range' [where x=y])
   2.105 -        defer
   2.106 +         apply (insert sint_range' [where x=x])
   2.107 +         apply (insert sint_range' [where x=y])
   2.108 +         defer
   2.109 +         apply (simp (no_asm), arith)
   2.110          apply (simp (no_asm), arith)
   2.111 +       defer
   2.112 +       defer
   2.113         apply (simp (no_asm), arith)
   2.114 -      defer
   2.115 -      defer
   2.116        apply (simp (no_asm), arith)
   2.117 -     apply (simp (no_asm), arith)
   2.118 -    apply (rule notI [THEN notnotD],
   2.119 -           drule leI not_le_imp_less,
   2.120 -           drule sbintrunc_inc sbintrunc_dec,
   2.121 -           simp)+
   2.122 +     apply (rule notI [THEN notnotD],
   2.123 +      drule leI not_le_imp_less,
   2.124 +      drule sbintrunc_inc sbintrunc_dec,
   2.125 +      simp)+
   2.126    done
   2.127  
   2.128  
   2.129 @@ -3431,57 +3426,49 @@
   2.130    "(word_rsplit (numeral bin :: 'b::len0 word) :: 'a word list) =
   2.131      map word_of_int (bin_rsplit (len_of TYPE('a::len))
   2.132        (len_of TYPE('b), bintrunc (len_of TYPE('b)) (numeral bin)))"
   2.133 -  unfolding word_rsplit_def by (simp add: word_ubin.eq_norm)
   2.134 +  by (simp add: word_rsplit_def word_ubin.eq_norm)
   2.135  
   2.136  lemmas word_rsplit_no_cl [simp] = word_rsplit_no
   2.137    [unfolded bin_rsplitl_def bin_rsplit_l [symmetric]]
   2.138  
   2.139  lemma test_bit_cat:
   2.140 -  "wc = word_cat a b \<Longrightarrow> wc !! n = (n < size wc &
   2.141 +  "wc = word_cat a b \<Longrightarrow> wc !! n = (n < size wc \<and>
   2.142      (if n < size b then b !! n else a !! (n - size b)))"
   2.143 -  apply (unfold word_cat_bin' test_bit_bin)
   2.144 -  apply (auto simp add : word_ubin.eq_norm nth_bintr bin_nth_cat word_size)
   2.145 +  apply (auto simp: word_cat_bin' test_bit_bin word_ubin.eq_norm nth_bintr bin_nth_cat word_size)
   2.146    apply (erule bin_nth_uint_imp)
   2.147    done
   2.148  
   2.149  lemma word_cat_bl: "word_cat a b = of_bl (to_bl a @ to_bl b)"
   2.150 -  apply (unfold of_bl_def to_bl_def word_cat_bin')
   2.151 -  apply (simp add: bl_to_bin_app_cat)
   2.152 -  done
   2.153 +  by (simp add: of_bl_def to_bl_def word_cat_bin' bl_to_bin_app_cat)
   2.154  
   2.155  lemma of_bl_append:
   2.156    "(of_bl (xs @ ys) :: 'a::len word) = of_bl xs * 2^(length ys) + of_bl ys"
   2.157 -  apply (unfold of_bl_def)
   2.158 -  apply (simp add: bl_to_bin_app_cat bin_cat_num)
   2.159 +  apply (simp add: of_bl_def bl_to_bin_app_cat bin_cat_num)
   2.160    apply (simp add: word_of_int_power_hom [symmetric] word_of_int_hom_syms)
   2.161    done
   2.162  
   2.163 -lemma of_bl_False [simp]:
   2.164 -  "of_bl (False#xs) = of_bl xs"
   2.165 -  by (rule word_eqI)
   2.166 -     (auto simp add: test_bit_of_bl nth_append)
   2.167 -
   2.168 -lemma of_bl_True [simp]:
   2.169 -  "(of_bl (True#xs)::'a::len word) = 2^length xs + of_bl xs"
   2.170 -  by (subst of_bl_append [where xs="[True]", simplified])
   2.171 -     (simp add: word_1_bl)
   2.172 -
   2.173 -lemma of_bl_Cons:
   2.174 -  "of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs"
   2.175 +lemma of_bl_False [simp]: "of_bl (False#xs) = of_bl xs"
   2.176 +  by (rule word_eqI) (auto simp: test_bit_of_bl nth_append)
   2.177 +
   2.178 +lemma of_bl_True [simp]: "(of_bl (True # xs) :: 'a::len word) = 2^length xs + of_bl xs"
   2.179 +  by (subst of_bl_append [where xs="[True]", simplified]) (simp add: word_1_bl)
   2.180 +
   2.181 +lemma of_bl_Cons: "of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs"
   2.182    by (cases x) simp_all
   2.183  
   2.184 -lemma split_uint_lem: "bin_split n (uint (w :: 'a::len0 word)) = (a, b) \<Longrightarrow>
   2.185 -  a = bintrunc (len_of TYPE('a) - n) a & b = bintrunc (len_of TYPE('a)) b"
   2.186 +lemma split_uint_lem: "bin_split n (uint w) = (a, b) \<Longrightarrow>
   2.187 +    a = bintrunc (len_of TYPE('a) - n) a \<and> b = bintrunc (len_of TYPE('a)) b"
   2.188 +  for w :: "'a::len0 word"
   2.189    apply (frule word_ubin.norm_Rep [THEN ssubst])
   2.190    apply (drule bin_split_trunc1)
   2.191    apply (drule sym [THEN trans])
   2.192 -  apply assumption
   2.193 +   apply assumption
   2.194    apply safe
   2.195    done
   2.196  
   2.197  lemma word_split_bl':
   2.198    "std = size c - size b \<Longrightarrow> (word_split c = (a, b)) \<Longrightarrow>
   2.199 -    (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c)))"
   2.200 +    (a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c)))"
   2.201    apply (unfold word_split_bin')
   2.202    apply safe
   2.203     defer
   2.204 @@ -3489,12 +3476,12 @@
   2.205     apply hypsubst_thin
   2.206     apply (drule word_ubin.norm_Rep [THEN ssubst])
   2.207     apply (drule split_bintrunc)
   2.208 -   apply (simp add : of_bl_def bl2bin_drop word_size
   2.209 -       word_ubin.norm_eq_iff [symmetric] min_def del : word_ubin.norm_Rep)
   2.210 +   apply (simp add: of_bl_def bl2bin_drop word_size
   2.211 +      word_ubin.norm_eq_iff [symmetric] min_def del: word_ubin.norm_Rep)
   2.212    apply (clarsimp split: prod.splits)
   2.213    apply (frule split_uint_lem [THEN conjunct1])
   2.214    apply (unfold word_size)
   2.215 -  apply (cases "len_of TYPE('a) >= len_of TYPE('b)")
   2.216 +  apply (cases "len_of TYPE('a) \<ge> len_of TYPE('b)")
   2.217     defer
   2.218     apply simp
   2.219    apply (simp add : of_bl_def to_bl_def)
   2.220 @@ -3508,30 +3495,33 @@
   2.221    done
   2.222  
   2.223  lemma word_split_bl: "std = size c - size b \<Longrightarrow>
   2.224 -    (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c))) \<longleftrightarrow>
   2.225 +    (a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c))) \<longleftrightarrow>
   2.226      word_split c = (a, b)"
   2.227    apply (rule iffI)
   2.228     defer
   2.229     apply (erule (1) word_split_bl')
   2.230    apply (case_tac "word_split c")
   2.231 -  apply (auto simp add : word_size)
   2.232 +  apply (auto simp add: word_size)
   2.233    apply (frule word_split_bl' [rotated])
   2.234 -  apply (auto simp add : word_size)
   2.235 +   apply (auto simp add: word_size)
   2.236    done
   2.237  
   2.238  lemma word_split_bl_eq:
   2.239 -   "(word_split (c::'a::len word) :: ('c::len0 word * 'd::len0 word)) =
   2.240 -      (of_bl (take (len_of TYPE('a::len) - len_of TYPE('d::len0)) (to_bl c)),
   2.241 -       of_bl (drop (len_of TYPE('a) - len_of TYPE('d)) (to_bl c)))"
   2.242 +  "(word_split c :: ('c::len0 word \<times> 'd::len0 word)) =
   2.243 +    (of_bl (take (len_of TYPE('a::len) - len_of TYPE('d::len0)) (to_bl c)),
   2.244 +     of_bl (drop (len_of TYPE('a) - len_of TYPE('d)) (to_bl c)))"
   2.245 +  for c :: "'a::len word"
   2.246    apply (rule word_split_bl [THEN iffD1])
   2.247 -  apply (unfold word_size)
   2.248 -  apply (rule refl conjI)+
   2.249 +   apply (unfold word_size)
   2.250 +   apply (rule refl conjI)+
   2.251    done
   2.252  
   2.253  \<comment> "keep quantifiers for use in simplification"
   2.254  lemma test_bit_split':
   2.255 -  "word_split c = (a, b) --> (ALL n m. b !! n = (n < size b & c !! n) &
   2.256 -    a !! m = (m < size a & c !! (m + size b)))"
   2.257 +  "word_split c = (a, b) \<longrightarrow>
   2.258 +    (\<forall>n m.
   2.259 +      b !! n = (n < size b \<and> c !! n) \<and>
   2.260 +      a !! m = (m < size a \<and> c !! (m + size b)))"
   2.261    apply (unfold word_split_bin' test_bit_bin)
   2.262    apply (clarify)
   2.263    apply (clarsimp simp: word_ubin.eq_norm nth_bintr word_size split: prod.splits)
   2.264 @@ -3543,12 +3533,14 @@
   2.265  
   2.266  lemma test_bit_split:
   2.267    "word_split c = (a, b) \<Longrightarrow>
   2.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))"
   2.269 +    (\<forall>n::nat. b !! n \<longleftrightarrow> n < size b \<and> c !! n) \<and>
   2.270 +    (\<forall>m::nat. a !! m \<longleftrightarrow> m < size a \<and> c !! (m + size b))"
   2.271    by (simp add: test_bit_split')
   2.272  
   2.273 -lemma test_bit_split_eq: "word_split c = (a, b) \<longleftrightarrow>
   2.274 -  ((ALL n::nat. b !! n = (n < size b & c !! n)) &
   2.275 -    (ALL m::nat. a !! m = (m < size a & c !! (m + size b))))"
   2.276 +lemma test_bit_split_eq:
   2.277 +  "word_split c = (a, b) \<longleftrightarrow>
   2.278 +    ((\<forall>n::nat. b !! n = (n < size b \<and> c !! n)) \<and>
   2.279 +     (\<forall>m::nat. a !! m = (m < size a \<and> c !! (m + size b))))"
   2.280    apply (rule_tac iffI)
   2.281     apply (rule_tac conjI)
   2.282      apply (erule test_bit_split [THEN conjunct1])
   2.283 @@ -3556,28 +3548,24 @@
   2.284    apply (case_tac "word_split c")
   2.285    apply (frule test_bit_split)
   2.286    apply (erule trans)
   2.287 -  apply (fastforce intro ! : word_eqI simp add : word_size)
   2.288 +  apply (fastforce intro!: word_eqI simp add: word_size)
   2.289    done
   2.290  
   2.291  \<comment> \<open>this odd result is analogous to \<open>ucast_id\<close>,
   2.292        result to the length given by the result type\<close>
   2.293  
   2.294  lemma word_cat_id: "word_cat a b = b"
   2.295 -  unfolding word_cat_bin' by (simp add: word_ubin.inverse_norm)
   2.296 +  by (simp add: word_cat_bin' word_ubin.inverse_norm)
   2.297  
   2.298  \<comment> "limited hom result"
   2.299  lemma word_cat_hom:
   2.300 -  "len_of TYPE('a::len0) <= len_of TYPE('b::len0) + len_of TYPE('c::len0)
   2.301 -  \<Longrightarrow>
   2.302 -  (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) =
   2.303 -  word_of_int (bin_cat w (size b) (uint b))"
   2.304 -  apply (unfold word_cat_def word_size)
   2.305 -  apply (clarsimp simp add: word_ubin.norm_eq_iff [symmetric]
   2.306 +  "len_of TYPE('a::len0) \<le> len_of TYPE('b::len0) + len_of TYPE('c::len0) \<Longrightarrow>
   2.307 +    (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) =
   2.308 +    word_of_int (bin_cat w (size b) (uint b))"
   2.309 +  by (auto simp: word_cat_def word_size word_ubin.norm_eq_iff [symmetric]
   2.310        word_ubin.eq_norm bintr_cat min.absorb1)
   2.311 -  done
   2.312 -
   2.313 -lemma word_cat_split_alt:
   2.314 -  "size w <= size u + size v \<Longrightarrow> word_split w = (u, v) \<Longrightarrow> word_cat u v = w"
   2.315 +
   2.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"
   2.317    apply (rule word_eqI)
   2.318    apply (drule test_bit_split)
   2.319    apply (clarsimp simp add : test_bit_cat word_size)
   2.320 @@ -3590,8 +3578,7 @@
   2.321  
   2.322  subsubsection \<open>Split and slice\<close>
   2.323  
   2.324 -lemma split_slices:
   2.325 -  "word_split w = (u, v) \<Longrightarrow> u = slice (size v) w & v = slice 0 w"
   2.326 +lemma split_slices: "word_split w = (u, v) \<Longrightarrow> u = slice (size v) w \<and> v = slice 0 w"
   2.327    apply (drule test_bit_split)
   2.328    apply (rule conjI)
   2.329     apply (rule word_eqI, clarsimp simp: nth_slice word_size)+
   2.330 @@ -3617,7 +3604,7 @@
   2.331    done
   2.332  
   2.333  lemma word_split_cat_alt:
   2.334 -  "w = word_cat u v \<Longrightarrow> size u + size v <= size w \<Longrightarrow> word_split w = (u, v)"
   2.335 +  "w = word_cat u v \<Longrightarrow> size u + size v \<le> size w \<Longrightarrow> word_split w = (u, v)"
   2.336    apply (case_tac "word_split w")
   2.337    apply (rule trans, assumption)
   2.338    apply (drule test_bit_split)
   2.339 @@ -3626,31 +3613,30 @@
   2.340    done
   2.341  
   2.342  lemmas word_cat_bl_no_bin [simp] =
   2.343 -  word_cat_bl [where a="numeral a" and b="numeral b",
   2.344 -    unfolded to_bl_numeral]
   2.345 +  word_cat_bl [where a="numeral a" and b="numeral b", unfolded to_bl_numeral]
   2.346    for a b (* FIXME: negative numerals, 0 and 1 *)
   2.347  
   2.348  lemmas word_split_bl_no_bin [simp] =
   2.349    word_split_bl_eq [where c="numeral c", unfolded to_bl_numeral] for c
   2.350  
   2.351 -text \<open>this odd result arises from the fact that the statement of the
   2.352 -      result implies that the decoded words are of the same type,
   2.353 -      and therefore of the same length, as the original word\<close>
   2.354 +text \<open>
   2.355 +  This odd result arises from the fact that the statement of the
   2.356 +  result implies that the decoded words are of the same type,
   2.357 +  and therefore of the same length, as the original word.\<close>
   2.358  
   2.359  lemma word_rsplit_same: "word_rsplit w = [w]"
   2.360 -  unfolding word_rsplit_def by (simp add : bin_rsplit_all)
   2.361 -
   2.362 -lemma word_rsplit_empty_iff_size:
   2.363 -  "(word_rsplit w = []) = (size w = 0)"
   2.364 -  unfolding word_rsplit_def bin_rsplit_def word_size
   2.365 -  by (simp add: bin_rsplit_aux_simp_alt Let_def split: prod.split)
   2.366 +  by (simp add: word_rsplit_def bin_rsplit_all)
   2.367 +
   2.368 +lemma word_rsplit_empty_iff_size: "word_rsplit w = [] \<longleftrightarrow> size w = 0"
   2.369 +  by (simp add: word_rsplit_def bin_rsplit_def word_size bin_rsplit_aux_simp_alt Let_def
   2.370 +      split: prod.split)
   2.371  
   2.372  lemma test_bit_rsplit:
   2.373    "sw = word_rsplit w \<Longrightarrow> m < size (hd sw :: 'a::len word) \<Longrightarrow>
   2.374      k < length sw \<Longrightarrow> (rev sw ! k) !! m = (w !! (k * size (hd sw) + m))"
   2.375    apply (unfold word_rsplit_def word_test_bit_def)
   2.376    apply (rule trans)
   2.377 -   apply (rule_tac f = "%x. bin_nth x m" in arg_cong)
   2.378 +   apply (rule_tac f = "\<lambda>x. bin_nth x m" in arg_cong)
   2.379     apply (rule nth_map [symmetric])
   2.380     apply simp
   2.381    apply (rule bin_nth_rsplit)
   2.382 @@ -3665,12 +3651,10 @@
   2.383    done
   2.384  
   2.385  lemma word_rcat_bl: "word_rcat wl = of_bl (concat (map to_bl wl))"
   2.386 -  unfolding word_rcat_def to_bl_def' of_bl_def
   2.387 -  by (clarsimp simp add : bin_rcat_bl)
   2.388 -
   2.389 -lemma size_rcat_lem':
   2.390 -  "size (concat (map to_bl wl)) = length wl * size (hd wl)"
   2.391 -  unfolding word_size by (induct wl) auto
   2.392 +  by (auto simp: word_rcat_def to_bl_def' of_bl_def bin_rcat_bl)
   2.393 +
   2.394 +lemma size_rcat_lem': "size (concat (map to_bl wl)) = length wl * size (hd wl)"
   2.395 +  by (induct wl) (auto simp: word_size)
   2.396  
   2.397  lemmas size_rcat_lem = size_rcat_lem' [unfolded word_size]
   2.398  
   2.399 @@ -3680,7 +3664,7 @@
   2.400    "n < length (wl::'a word list) * len_of TYPE('a::len) \<Longrightarrow>
   2.401      rev (concat (map to_bl wl)) ! n =
   2.402      rev (to_bl (rev wl ! (n div len_of TYPE('a)))) ! (n mod len_of TYPE('a))"
   2.403 -  apply (induct "wl")
   2.404 +  apply (induct wl)
   2.405     apply clarsimp
   2.406    apply (clarsimp simp add : nth_append size_rcat_lem)
   2.407    apply (simp (no_asm_use) only:  mult_Suc [symmetric]
   2.408 @@ -3690,18 +3674,16 @@
   2.409  
   2.410  lemma test_bit_rcat:
   2.411    "sw = size (hd wl :: 'a::len word) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> rc !! n =
   2.412 -    (n < size rc & n div sw < size wl & (rev wl) ! (n div sw) !! (n mod sw))"
   2.413 +    (n < size rc \<and> n div sw < size wl \<and> (rev wl) ! (n div sw) !! (n mod sw))"
   2.414    apply (unfold word_rcat_bl word_size)
   2.415 -  apply (clarsimp simp add :
   2.416 -    test_bit_of_bl size_rcat_lem word_size td_gal_lt_len)
   2.417 +  apply (clarsimp simp add: test_bit_of_bl size_rcat_lem word_size td_gal_lt_len)
   2.418    apply safe
   2.419 -   apply (auto simp add :
   2.420 -    test_bit_bl word_size td_gal_lt_len [THEN iffD2, THEN nth_rcat_lem])
   2.421 +   apply (auto simp: test_bit_bl word_size td_gal_lt_len [THEN iffD2, THEN nth_rcat_lem])
   2.422    done
   2.423  
   2.424 -lemma foldl_eq_foldr:
   2.425 -  "foldl op + x xs = foldr op + (x # xs) (0 :: 'a :: comm_monoid_add)"
   2.426 -  by (induct xs arbitrary: x) (auto simp add : add.assoc)
   2.427 +lemma foldl_eq_foldr: "foldl op + x xs = foldr op + (x # xs) 0"
   2.428 +  for x :: "'a::comm_monoid_add"
   2.429 +  by (induct xs arbitrary: x) (auto simp: add.assoc)
   2.430  
   2.431  lemmas test_bit_cong = arg_cong [where f = "test_bit", THEN fun_cong]
   2.432  
   2.433 @@ -3713,16 +3695,12 @@
   2.434  lemma word_rsplit_len_indep [OF refl refl refl refl]:
   2.435    "[u,v] = p \<Longrightarrow> [su,sv] = q \<Longrightarrow> word_rsplit u = su \<Longrightarrow>
   2.436      word_rsplit v = sv \<Longrightarrow> length su = length sv"
   2.437 -  apply (unfold word_rsplit_def)
   2.438 -  apply (auto simp add : bin_rsplit_len_indep)
   2.439 -  done
   2.440 +  by (auto simp: word_rsplit_def bin_rsplit_len_indep)
   2.441  
   2.442  lemma length_word_rsplit_size:
   2.443    "n = len_of TYPE('a::len) \<Longrightarrow>
   2.444 -    (length (word_rsplit w :: 'a word list) <= m) = (size w <= m * n)"
   2.445 -  apply (unfold word_rsplit_def word_size)
   2.446 -  apply (clarsimp simp add : bin_rsplit_len_le)
   2.447 -  done
   2.448 +    length (word_rsplit w :: 'a word list) \<le> m \<longleftrightarrow> size w \<le> m * n"
   2.449 +  by (auto simp: word_rsplit_def word_size bin_rsplit_len_le)
   2.450  
   2.451  lemmas length_word_rsplit_lt_size =
   2.452    length_word_rsplit_size [unfolded Not_eq_iff linorder_not_less [symmetric]]
   2.453 @@ -3730,12 +3708,12 @@
   2.454  lemma length_word_rsplit_exp_size:
   2.455    "n = len_of TYPE('a::len) \<Longrightarrow>
   2.456      length (word_rsplit w :: 'a word list) = (size w + n - 1) div n"
   2.457 -  unfolding word_rsplit_def by (clarsimp simp add : word_size bin_rsplit_len)
   2.458 +  by (auto simp: word_rsplit_def word_size bin_rsplit_len)
   2.459  
   2.460  lemma length_word_rsplit_even_size:
   2.461    "n = len_of TYPE('a::len) \<Longrightarrow> size w = m * n \<Longrightarrow>
   2.462      length (word_rsplit w :: 'a word list) = m"
   2.463 -  by (clarsimp simp add : length_word_rsplit_exp_size given_quot_alt)
   2.464 +  by (auto simp: length_word_rsplit_exp_size given_quot_alt)
   2.465  
   2.466  lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size]
   2.467  
   2.468 @@ -3745,7 +3723,7 @@
   2.469  
   2.470  lemma word_rcat_rsplit: "word_rcat (word_rsplit w) = w"
   2.471    apply (rule word_eqI)
   2.472 -  apply (clarsimp simp add : test_bit_rcat word_size)
   2.473 +  apply (clarsimp simp: test_bit_rcat word_size)
   2.474    apply (subst refl [THEN test_bit_rsplit])
   2.475      apply (simp_all add: word_size
   2.476        refl [THEN length_word_rsplit_size [simplified not_less [symmetric], simplified]])
   2.477 @@ -3754,22 +3732,23 @@
   2.478    done
   2.479  
   2.480  lemma size_word_rsplit_rcat_size:
   2.481 -  "\<lbrakk>word_rcat (ws::'a::len word list) = (frcw::'b::len0 word);
   2.482 -     size frcw = length ws * len_of TYPE('a)\<rbrakk>
   2.483 +  "word_rcat ws = frcw \<Longrightarrow> size frcw = length ws * len_of TYPE('a)
   2.484      \<Longrightarrow> length (word_rsplit frcw::'a word list) = length ws"
   2.485 -  apply (clarsimp simp add : word_size length_word_rsplit_exp_size')
   2.486 +  for ws :: "'a::len word list" and frcw :: "'b::len0 word"
   2.487 +  apply (clarsimp simp: word_size length_word_rsplit_exp_size')
   2.488    apply (fast intro: given_quot_alt)
   2.489    done
   2.490  
   2.491  lemma msrevs:
   2.492 -  fixes n::nat
   2.493 -  shows "0 < n \<Longrightarrow> (k * n + m) div n = m div n + k"
   2.494 -  and   "(k * n + m) mod n = m mod n"
   2.495 +  "0 < n \<Longrightarrow> (k * n + m) div n = m div n + k"
   2.496 +  "(k * n + m) mod n = m mod n"
   2.497 +  for n :: nat
   2.498    by (auto simp: add.commute)
   2.499  
   2.500  lemma word_rsplit_rcat_size [OF refl]:
   2.501 -  "word_rcat (ws :: 'a::len word list) = frcw \<Longrightarrow>
   2.502 +  "word_rcat ws = frcw \<Longrightarrow>
   2.503      size frcw = length ws * len_of TYPE('a) \<Longrightarrow> word_rsplit frcw = ws"
   2.504 +  for ws :: "'a::len word list"
   2.505    apply (frule size_word_rsplit_rcat_size, assumption)
   2.506    apply (clarsimp simp add : word_size)
   2.507    apply (rule nth_equalityI, assumption)
   2.508 @@ -3779,7 +3758,7 @@
   2.509     apply (rule test_bit_rsplit_alt)
   2.510       apply (clarsimp simp: word_size)+
   2.511    apply (rule trans)
   2.512 -  apply (rule test_bit_rcat [OF refl refl])
   2.513 +   apply (rule test_bit_rcat [OF refl refl])
   2.514    apply (simp add: word_size)
   2.515    apply (subst nth_rev)
   2.516     apply arith
   2.517 @@ -3787,8 +3766,8 @@
   2.518    apply safe
   2.519    apply (simp add: diff_mult_distrib)
   2.520    apply (rule mpl_lem)
   2.521 -  apply (cases "size ws")
   2.522 -   apply simp_all
   2.523 +   apply (cases "size ws")
   2.524 +    apply simp_all
   2.525    done
   2.526  
   2.527  
   2.528 @@ -3798,8 +3777,7 @@
   2.529  
   2.530  lemmas word_rot_defs = word_roti_def word_rotr_def word_rotl_def
   2.531  
   2.532 -lemma rotate_eq_mod:
   2.533 -  "m mod length xs = n mod length xs \<Longrightarrow> rotate m xs = rotate n xs"
   2.534 +lemma rotate_eq_mod: "m mod length xs = n mod length xs \<Longrightarrow> rotate m xs = rotate n xs"
   2.535    apply (rule box_equals)
   2.536      defer
   2.537      apply (rule rotate_conv_mod [symmetric])+
   2.538 @@ -3817,47 +3795,42 @@
   2.539  subsubsection \<open>Rotation of list to right\<close>
   2.540  
   2.541  lemma rotate1_rl': "rotater1 (l @ [a]) = a # l"
   2.542 -  unfolding rotater1_def by (cases l) auto
   2.543 +  by (cases l) (auto simp: rotater1_def)
   2.544  
   2.545  lemma rotate1_rl [simp] : "rotater1 (rotate1 l) = l"
   2.546    apply (unfold rotater1_def)
   2.547    apply (cases "l")
   2.548 -  apply (case_tac [2] "list")
   2.549 -  apply auto
   2.550 +   apply (case_tac [2] "list")
   2.551 +    apply auto
   2.552    done
   2.553  
   2.554  lemma rotate1_lr [simp] : "rotate1 (rotater1 l) = l"
   2.555 -  unfolding rotater1_def by (cases l) auto
   2.556 +  by (cases l) (auto simp: rotater1_def)
   2.557  
   2.558  lemma rotater1_rev': "rotater1 (rev xs) = rev (rotate1 xs)"
   2.559 -  apply (cases "xs")
   2.560 -  apply (simp add : rotater1_def)
   2.561 -  apply (simp add : rotate1_rl')
   2.562 -  done
   2.563 +  by (cases "xs") (simp add: rotater1_def, simp add: rotate1_rl')
   2.564  
   2.565  lemma rotater_rev': "rotater n (rev xs) = rev (rotate n xs)"
   2.566 -  unfolding rotater_def by (induct n) (auto intro: rotater1_rev')
   2.567 +  by (induct n) (auto simp: rotater_def intro: rotater1_rev')
   2.568  
   2.569  lemma rotater_rev: "rotater n ys = rev (rotate n (rev ys))"
   2.570    using rotater_rev' [where xs = "rev ys"] by simp
   2.571  
   2.572  lemma rotater_drop_take:
   2.573    "rotater n xs =
   2.574 -   drop (length xs - n mod length xs) xs @
   2.575 -   take (length xs - n mod length xs) xs"
   2.576 -  by (clarsimp simp add : rotater_rev rotate_drop_take rev_take rev_drop)
   2.577 -
   2.578 -lemma rotater_Suc [simp] :
   2.579 -  "rotater (Suc n) xs = rotater1 (rotater n xs)"
   2.580 +    drop (length xs - n mod length xs) xs @
   2.581 +    take (length xs - n mod length xs) xs"
   2.582 +  by (auto simp: rotater_rev rotate_drop_take rev_take rev_drop)
   2.583 +
   2.584 +lemma rotater_Suc [simp]: "rotater (Suc n) xs = rotater1 (rotater n xs)"
   2.585    unfolding rotater_def by auto
   2.586  
   2.587  lemma rotate_inv_plus [rule_format] :
   2.588 -  "ALL k. k = m + n --> rotater k (rotate n xs) = rotater m xs &
   2.589 -    rotate k (rotater n xs) = rotate m xs &
   2.590 -    rotater n (rotate k xs) = rotate m xs &
   2.591 +  "\<forall>k. k = m + n \<longrightarrow> rotater k (rotate n xs) = rotater m xs \<and>
   2.592 +    rotate k (rotater n xs) = rotate m xs \<and>
   2.593 +    rotater n (rotate k xs) = rotate m xs \<and>
   2.594      rotate n (rotater k xs) = rotater m xs"
   2.595 -  unfolding rotater_def rotate_def
   2.596 -  by (induct n) (auto intro: funpow_swap1 [THEN trans])
   2.597 +  by (induct n) (auto simp: rotater_def rotate_def intro: funpow_swap1 [THEN trans])
   2.598  
   2.599  lemmas rotate_inv_rel = le_add_diff_inverse2 [symmetric, THEN rotate_inv_plus]
   2.600  
   2.601 @@ -3866,20 +3839,17 @@
   2.602  lemmas rotate_lr [simp] = rotate_inv_eq [THEN conjunct1]
   2.603  lemmas rotate_rl [simp] = rotate_inv_eq [THEN conjunct2, THEN conjunct1]
   2.604  
   2.605 -lemma rotate_gal: "(rotater n xs = ys) = (rotate n ys = xs)"
   2.606 +lemma rotate_gal: "rotater n xs = ys \<longleftrightarrow> rotate n ys = xs"
   2.607    by auto
   2.608  
   2.609 -lemma rotate_gal': "(ys = rotater n xs) = (xs = rotate n ys)"
   2.610 +lemma rotate_gal': "ys = rotater n xs \<longleftrightarrow> xs = rotate n ys"
   2.611    by auto
   2.612  
   2.613 -lemma length_rotater [simp]:
   2.614 -  "length (rotater n xs) = length xs"
   2.615 +lemma length_rotater [simp]: "length (rotater n xs) = length xs"
   2.616    by (simp add : rotater_rev)
   2.617  
   2.618 -lemma restrict_to_left:
   2.619 -  assumes "x = y"
   2.620 -  shows "(x = z) = (y = z)"
   2.621 -  using assms by simp
   2.622 +lemma restrict_to_left: "x = y \<Longrightarrow> x = z \<longleftrightarrow> y = z"
   2.623 +  by simp
   2.624  
   2.625  lemmas rrs0 = rotate_eqs [THEN restrict_to_left,
   2.626    simplified rotate_gal [symmetric] rotate_gal' [symmetric]]
   2.627 @@ -3891,34 +3861,30 @@
   2.628  
   2.629  subsubsection \<open>map, map2, commuting with rotate(r)\<close>
   2.630  
   2.631 -lemma butlast_map:
   2.632 -  "xs ~= [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)"
   2.633 +lemma butlast_map: "xs \<noteq> [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)"
   2.634    by (induct xs) auto
   2.635  
   2.636  lemma rotater1_map: "rotater1 (map f xs) = map f (rotater1 xs)"
   2.637 -  unfolding rotater1_def
   2.638 -  by (cases xs) (auto simp add: last_map butlast_map)
   2.639 -
   2.640 -lemma rotater_map:
   2.641 -  "rotater n (map f xs) = map f (rotater n xs)"
   2.642 -  unfolding rotater_def
   2.643 -  by (induct n) (auto simp add : rotater1_map)
   2.644 +  by (cases xs) (auto simp: rotater1_def last_map butlast_map)
   2.645 +
   2.646 +lemma rotater_map: "rotater n (map f xs) = map f (rotater n xs)"
   2.647 +  by (induct n) (auto simp: rotater_def rotater1_map)
   2.648  
   2.649  lemma but_last_zip [rule_format] :
   2.650 -  "ALL ys. length xs = length ys --> xs ~= [] -->
   2.651 -    last (zip xs ys) = (last xs, last ys) &
   2.652 +  "\<forall>ys. length xs = length ys \<longrightarrow> xs \<noteq> [] \<longrightarrow>
   2.653 +    last (zip xs ys) = (last xs, last ys) \<and>
   2.654      butlast (zip xs ys) = zip (butlast xs) (butlast ys)"
   2.655 -  apply (induct "xs")
   2.656 -  apply auto
   2.657 +  apply (induct xs)
   2.658 +   apply auto
   2.659       apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
   2.660    done
   2.661  
   2.662  lemma but_last_map2 [rule_format] :
   2.663 -  "ALL ys. length xs = length ys --> xs ~= [] -->
   2.664 -    last (map2 f xs ys) = f (last xs) (last ys) &
   2.665 +  "\<forall>ys. length xs = length ys \<longrightarrow> xs \<noteq> [] \<longrightarrow>
   2.666 +    last (map2 f xs ys) = f (last xs) (last ys) \<and>
   2.667      butlast (map2 f xs ys) = map2 f (butlast xs) (butlast ys)"
   2.668 -  apply (induct "xs")
   2.669 -  apply auto
   2.670 +  apply (induct xs)
   2.671 +   apply auto
   2.672       apply (unfold map2_def)
   2.673       apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
   2.674    done
   2.675 @@ -3927,7 +3893,7 @@
   2.676    "length xs = length ys \<Longrightarrow>
   2.677      rotater1 (zip xs ys) = zip (rotater1 xs) (rotater1 ys)"
   2.678    apply (unfold rotater1_def)
   2.679 -  apply (cases "xs")
   2.680 +  apply (cases xs)
   2.681     apply auto
   2.682     apply ((case_tac ys, auto simp: neq_Nil_conv but_last_zip)[1])+
   2.683    done
   2.684 @@ -3935,7 +3901,7 @@
   2.685  lemma rotater1_map2:
   2.686    "length xs = length ys \<Longrightarrow>
   2.687      rotater1 (map2 f xs ys) = map2 f (rotater1 xs) (rotater1 ys)"
   2.688 -  unfolding map2_def by (simp add: rotater1_map rotater1_zip)
   2.689 +  by (simp add: map2_def rotater1_map rotater1_zip)
   2.690  
   2.691  lemmas lrth =
   2.692    box_equals [OF asm_rl length_rotater [symmetric]
   2.693 @@ -3950,10 +3916,7 @@
   2.694  lemma rotate1_map2:
   2.695    "length xs = length ys \<Longrightarrow>
   2.696      rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)"
   2.697 -  apply (unfold map2_def)
   2.698 -  apply (cases xs)
   2.699 -   apply (cases ys, auto)+
   2.700 -  done
   2.701 +  by (cases xs; cases ys) (auto simp: map2_def)
   2.702  
   2.703  lemmas lth = box_equals [OF asm_rl length_rotate [symmetric]
   2.704    length_rotate [symmetric], THEN rotate1_map2]
   2.705 @@ -3966,8 +3929,7 @@
   2.706  
   2.707  \<comment> "corresponding equalities for word rotation"
   2.708  
   2.709 -lemma to_bl_rotl:
   2.710 -  "to_bl (word_rotl n w) = rotate n (to_bl w)"
   2.711 +lemma to_bl_rotl: "to_bl (word_rotl n w) = rotate n (to_bl w)"
   2.712    by (simp add: word_bl.Abs_inverse' word_rotl_def)
   2.713  
   2.714  lemmas blrs0 = rotate_eqs [THEN to_bl_rotl [THEN trans]]
   2.715 @@ -3975,8 +3937,7 @@
   2.716  lemmas word_rotl_eqs =
   2.717    blrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotl [symmetric]]
   2.718  
   2.719 -lemma to_bl_rotr:
   2.720 -  "to_bl (word_rotr n w) = rotater n (to_bl w)"
   2.721 +lemma to_bl_rotr: "to_bl (word_rotr n w) = rotater n (to_bl w)"
   2.722    by (simp add: word_bl.Abs_inverse' word_rotr_def)
   2.723  
   2.724  lemmas brrs0 = rotater_eqs [THEN to_bl_rotr [THEN trans]]
   2.725 @@ -3987,40 +3948,28 @@
   2.726  declare word_rotr_eqs (1) [simp]
   2.727  declare word_rotl_eqs (1) [simp]
   2.728  
   2.729 -lemma
   2.730 -  word_rot_rl [simp]:
   2.731 -  "word_rotl k (word_rotr k v) = v" and
   2.732 -  word_rot_lr [simp]:
   2.733 -  "word_rotr k (word_rotl k v) = v"
   2.734 +lemma word_rot_rl [simp]: "word_rotl k (word_rotr k v) = v"
   2.735 +  and word_rot_lr [simp]: "word_rotr k (word_rotl k v) = v"
   2.736    by (auto simp add: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric])
   2.737  
   2.738 -lemma
   2.739 -  word_rot_gal:
   2.740 -  "(word_rotr n v = w) = (word_rotl n w = v)" and
   2.741 -  word_rot_gal':
   2.742 -  "(w = word_rotr n v) = (v = word_rotl n w)"
   2.743 -  by (auto simp: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric]
   2.744 -           dest: sym)
   2.745 -
   2.746 -lemma word_rotr_rev:
   2.747 -  "word_rotr n w = word_reverse (word_rotl n (word_reverse w))"
   2.748 -  by (simp only: word_bl.Rep_inject [symmetric] to_bl_word_rev
   2.749 -                to_bl_rotr to_bl_rotl rotater_rev)
   2.750 +lemma word_rot_gal: "word_rotr n v = w \<longleftrightarrow> word_rotl n w = v"
   2.751 +  and word_rot_gal': "w = word_rotr n v \<longleftrightarrow> v = word_rotl n w"
   2.752 +  by (auto simp: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric] dest: sym)
   2.753 +
   2.754 +lemma word_rotr_rev: "word_rotr n w = word_reverse (word_rotl n (word_reverse w))"
   2.755 +  by (simp only: word_bl.Rep_inject [symmetric] to_bl_word_rev to_bl_rotr to_bl_rotl rotater_rev)
   2.756  
   2.757  lemma word_roti_0 [simp]: "word_roti 0 w = w"
   2.758 -  by (unfold word_rot_defs) auto
   2.759 +  by (auto simp: word_rot_defs)
   2.760  
   2.761  lemmas abl_cong = arg_cong [where f = "of_bl"]
   2.762  
   2.763 -lemma word_roti_add:
   2.764 -  "word_roti (m + n) w = word_roti m (word_roti n w)"
   2.765 +lemma word_roti_add: "word_roti (m + n) w = word_roti m (word_roti n w)"
   2.766  proof -
   2.767 -  have rotater_eq_lem:
   2.768 -    "\<And>m n xs. m = n \<Longrightarrow> rotater m xs = rotater n xs"
   2.769 +  have rotater_eq_lem: "\<And>m n xs. m = n \<Longrightarrow> rotater m xs = rotater n xs"
   2.770      by auto
   2.771  
   2.772 -  have rotate_eq_lem:
   2.773 -    "\<And>m n xs. m = n \<Longrightarrow> rotate m xs = rotate n xs"
   2.774 +  have rotate_eq_lem: "\<And>m n xs. m = n \<Longrightarrow> rotate m xs = rotate n xs"
   2.775      by auto
   2.776  
   2.777    note rpts [symmetric] =
   2.778 @@ -4033,17 +3982,17 @@
   2.779    note rrrp = trans [symmetric, OF rotater_add [symmetric] rotater_eq_lem]
   2.780  
   2.781    show ?thesis
   2.782 -  apply (unfold word_rot_defs)
   2.783 -  apply (simp only: split: if_split)
   2.784 -  apply (safe intro!: abl_cong)
   2.785 -  apply (simp_all only: to_bl_rotl [THEN word_bl.Rep_inverse']
   2.786 -                    to_bl_rotl
   2.787 -                    to_bl_rotr [THEN word_bl.Rep_inverse']
   2.788 -                    to_bl_rotr)
   2.789 -  apply (rule rrp rrrp rpts,
   2.790 -         simp add: nat_add_distrib [symmetric]
   2.791 -                   nat_diff_distrib [symmetric])+
   2.792 -  done
   2.793 +    apply (unfold word_rot_defs)
   2.794 +    apply (simp only: split: if_split)
   2.795 +    apply (safe intro!: abl_cong)
   2.796 +           apply (simp_all only: to_bl_rotl [THEN word_bl.Rep_inverse']
   2.797 +                  to_bl_rotl
   2.798 +                  to_bl_rotr [THEN word_bl.Rep_inverse']
   2.799 +                  to_bl_rotr)
   2.800 +         apply (rule rrp rrrp rpts,
   2.801 +                simp add: nat_add_distrib [symmetric]
   2.802 +                nat_diff_distrib [symmetric])+
   2.803 +    done
   2.804  qed
   2.805  
   2.806  lemma word_roti_conv_mod': "word_roti n w = word_roti (n mod int (size w)) w"
   2.807 @@ -4129,11 +4078,11 @@
   2.808  lemmas word_rotr_dt = bl_word_rotr_dt [THEN word_bl.Rep_inverse' [symmetric]]
   2.809  lemmas word_roti_dt = bl_word_roti_dt [THEN word_bl.Rep_inverse' [symmetric]]
   2.810  
   2.811 -lemma word_rotx_0 [simp] : "word_rotr i 0 = 0 & word_rotl i 0 = 0"
   2.812 -  by (simp add : word_rotr_dt word_rotl_dt replicate_add [symmetric])
   2.813 +lemma word_rotx_0 [simp] : "word_rotr i 0 = 0 \<and> word_rotl i 0 = 0"
   2.814 +  by (simp add: word_rotr_dt word_rotl_dt replicate_add [symmetric])
   2.815  
   2.816  lemma word_roti_0' [simp] : "word_roti n 0 = 0"
   2.817 -  unfolding word_roti_def by auto
   2.818 +  by (auto simp: word_roti_def)
   2.819  
   2.820  lemmas word_rotr_dt_no_bin' [simp] =
   2.821    word_rotr_dt [where w="numeral w", unfolded to_bl_numeral] for w
   2.822 @@ -4149,11 +4098,13 @@
   2.823  subsection \<open>Maximum machine word\<close>
   2.824  
   2.825  lemma word_int_cases:
   2.826 -  obtains n where "(x ::'a::len0 word) = word_of_int n" and "0 \<le> n" and "n < 2^len_of TYPE('a)"
   2.827 +  fixes x :: "'a::len0 word"
   2.828 +  obtains n where "x = word_of_int n" and "0 \<le> n" and "n < 2^len_of TYPE('a)"
   2.829    by (cases x rule: word_uint.Abs_cases) (simp add: uints_num)
   2.830  
   2.831  lemma word_nat_cases [cases type: word]:
   2.832 -  obtains n where "(x ::'a::len word) = of_nat n" and "n < 2^len_of TYPE('a)"
   2.833 +  fixes x :: "'a::len word"
   2.834 +  obtains n where "x = of_nat n" and "n < 2^len_of TYPE('a)"
   2.835    by (cases x rule: word_unat.Abs_cases) (simp add: unats_def)
   2.836  
   2.837  lemma max_word_eq: "(max_word::'a::len word) = 2^len_of TYPE('a) - 1"
   2.838 @@ -4166,62 +4117,55 @@
   2.839  lemma word_of_int_2p_len: "word_of_int (2 ^ len_of TYPE('a)) = (0::'a::len0 word)"
   2.840    by (subst word_uint.Abs_norm [symmetric]) simp
   2.841  
   2.842 -lemma word_pow_0:
   2.843 -  "(2::'a::len word) ^ len_of TYPE('a) = 0"
   2.844 +lemma word_pow_0: "(2::'a::len word) ^ len_of TYPE('a) = 0"
   2.845  proof -
   2.846    have "word_of_int (2 ^ len_of TYPE('a)) = (0::'a word)"
   2.847      by (rule word_of_int_2p_len)
   2.848 -  thus ?thesis by (simp add: word_of_int_2p)
   2.849 +  then show ?thesis by (simp add: word_of_int_2p)
   2.850  qed
   2.851  
   2.852  lemma max_word_wrap: "x + 1 = 0 \<Longrightarrow> x = max_word"
   2.853    apply (simp add: max_word_eq)
   2.854    apply uint_arith
   2.855 -  apply auto
   2.856 -  apply (simp add: word_pow_0)
   2.857 +  apply (auto simp: word_pow_0)
   2.858    done
   2.859  
   2.860 -lemma max_word_minus:
   2.861 -  "max_word = (-1::'a::len word)"
   2.862 +lemma max_word_minus: "max_word = (-1::'a::len word)"
   2.863  proof -
   2.864 -  have "-1 + 1 = (0::'a word)" by simp
   2.865 -  thus ?thesis by (rule max_word_wrap [symmetric])
   2.866 +  have "-1 + 1 = (0::'a word)"
   2.867 +    by simp
   2.868 +  then show ?thesis
   2.869 +    by (rule max_word_wrap [symmetric])
   2.870  qed
   2.871  
   2.872 -lemma max_word_bl [simp]:
   2.873 -  "to_bl (max_word::'a::len word) = replicate (len_of TYPE('a)) True"
   2.874 +lemma max_word_bl [simp]: "to_bl (max_word::'a::len word) = replicate (len_of TYPE('a)) True"
   2.875    by (subst max_word_minus to_bl_n1)+ simp
   2.876  
   2.877 -lemma max_test_bit [simp]:
   2.878 -  "(max_word::'a::len word) !! n = (n < len_of TYPE('a))"
   2.879 -  by (auto simp add: test_bit_bl word_size)
   2.880 -
   2.881 -lemma word_and_max [simp]:
   2.882 -  "x AND max_word = x"
   2.883 +lemma max_test_bit [simp]: "(max_word::'a::len word) !! n \<longleftrightarrow> n < len_of TYPE('a)"
   2.884 +  by (auto simp: test_bit_bl word_size)
   2.885 +
   2.886 +lemma word_and_max [simp]: "x AND max_word = x"
   2.887    by (rule word_eqI) (simp add: word_ops_nth_size word_size)
   2.888  
   2.889 -lemma word_or_max [simp]:
   2.890 -  "x OR max_word = max_word"
   2.891 +lemma word_or_max [simp]: "x OR max_word = max_word"
   2.892    by (rule word_eqI) (simp add: word_ops_nth_size word_size)
   2.893  
   2.894 -lemma word_ao_dist2:
   2.895 -  "x AND (y OR z) = x AND y OR x AND (z::'a::len0 word)"
   2.896 +lemma word_ao_dist2: "x AND (y OR z) = x AND y OR x AND z"
   2.897 +  for x y z :: "'a::len0 word"
   2.898    by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
   2.899  
   2.900 -lemma word_oa_dist2:
   2.901 -  "x OR y AND z = (x OR y) AND (x OR (z::'a::len0 word))"
   2.902 +lemma word_oa_dist2: "x OR y AND z = (x OR y) AND (x OR z)"
   2.903 +  for x y z :: "'a::len0 word"
   2.904    by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
   2.905  
   2.906 -lemma word_and_not [simp]:
   2.907 -  "x AND NOT x = (0::'a::len0 word)"
   2.908 +lemma word_and_not [simp]: "x AND NOT x = 0"
   2.909 +  for x :: "'a::len0 word"
   2.910    by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
   2.911  
   2.912 -lemma word_or_not [simp]:
   2.913 -  "x OR NOT x = max_word"
   2.914 +lemma word_or_not [simp]: "x OR NOT x = max_word"
   2.915    by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
   2.916  
   2.917 -lemma word_boolean:
   2.918 -  "boolean (op AND) (op OR) bitNOT 0 max_word"
   2.919 +lemma word_boolean: "boolean (op AND) (op OR) bitNOT 0 max_word"
   2.920    apply (rule boolean.intro)
   2.921             apply (rule word_bw_assocs)
   2.922            apply (rule word_bw_assocs)
   2.923 @@ -4235,48 +4179,42 @@
   2.924    apply (rule word_or_not)
   2.925    done
   2.926  
   2.927 -interpretation word_bool_alg:
   2.928 -  boolean "op AND" "op OR" bitNOT 0 max_word
   2.929 +interpretation word_bool_alg: boolean "op AND" "op OR" bitNOT 0 max_word
   2.930    by (rule word_boolean)
   2.931  
   2.932 -lemma word_xor_and_or:
   2.933 -  "x XOR y = x AND NOT y OR NOT x AND (y::'a::len0 word)"
   2.934 +lemma word_xor_and_or: "x XOR y = x AND NOT y OR NOT x AND y"
   2.935 +  for x y :: "'a::len0 word"
   2.936    by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
   2.937  
   2.938 -interpretation word_bool_alg:
   2.939 -  boolean_xor "op AND" "op OR" bitNOT 0 max_word "op XOR"
   2.940 +interpretation word_bool_alg: boolean_xor "op AND" "op OR" bitNOT 0 max_word "op XOR"
   2.941    apply (rule boolean_xor.intro)
   2.942     apply (rule word_boolean)
   2.943    apply (rule boolean_xor_axioms.intro)
   2.944    apply (rule word_xor_and_or)
   2.945    done
   2.946  
   2.947 -lemma shiftr_x_0 [iff]:
   2.948 -  "(x::'a::len0 word) >> 0 = x"
   2.949 +lemma shiftr_x_0 [iff]: "x >> 0 = x"
   2.950 +  for x :: "'a::len0 word"
   2.951    by (simp add: shiftr_bl)
   2.952  
   2.953 -lemma shiftl_x_0 [simp]:
   2.954 -  "(x :: 'a::len word) << 0 = x"
   2.955 +lemma shiftl_x_0 [simp]: "x << 0 = x"
   2.956 +  for x :: "'a::len word"
   2.957    by (simp add: shiftl_t2n)
   2.958  
   2.959 -lemma shiftl_1 [simp]:
   2.960 -  "(1::'a::len word) << n = 2^n"
   2.961 +lemma shiftl_1 [simp]: "(1::'a::len word) << n = 2^n"
   2.962    by (simp add: shiftl_t2n)
   2.963  
   2.964 -lemma uint_lt_0 [simp]:
   2.965 -  "uint x < 0 = False"
   2.966 +lemma uint_lt_0 [simp]: "uint x < 0 = False"
   2.967    by (simp add: linorder_not_less)
   2.968  
   2.969 -lemma shiftr1_1 [simp]:
   2.970 -  "shiftr1 (1::'a::len word) = 0"
   2.971 +lemma shiftr1_1 [simp]: "shiftr1 (1::'a::len word) = 0"
   2.972    unfolding shiftr1_def by simp
   2.973  
   2.974 -lemma shiftr_1[simp]:
   2.975 -  "(1::'a::len word) >> n = (if n = 0 then 1 else 0)"
   2.976 +lemma shiftr_1[simp]: "(1::'a::len word) >> n = (if n = 0 then 1 else 0)"
   2.977    by (induct n) (auto simp: shiftr_def)
   2.978  
   2.979 -lemma word_less_1 [simp]:
   2.980 -  "((x::'a::len word) < 1) = (x = 0)"
   2.981 +lemma word_less_1 [simp]: "x < 1 \<longleftrightarrow> x = 0"
   2.982 +  for x :: "'a::len word"
   2.983    by (simp add: word_less_nat_alt unat_0_iff)
   2.984  
   2.985  lemma to_bl_mask:
   2.986 @@ -4287,33 +4225,29 @@
   2.987  
   2.988  lemma map_replicate_True:
   2.989    "n = length xs \<Longrightarrow>
   2.990 -    map (\<lambda>(x,y). x & y) (zip xs (replicate n True)) = xs"
   2.991 +    map (\<lambda>(x,y). x \<and> y) (zip xs (replicate n True)) = xs"
   2.992    by (induct xs arbitrary: n) auto
   2.993  
   2.994  lemma map_replicate_False:
   2.995 -  "n = length xs \<Longrightarrow> map (\<lambda>(x,y). x & y)
   2.996 +  "n = length xs \<Longrightarrow> map (\<lambda>(x,y). x \<and> y)
   2.997      (zip xs (replicate n False)) = replicate n False"
   2.998    by (induct xs arbitrary: n) auto
   2.999  
  2.1000  lemma bl_and_mask:
  2.1001    fixes w :: "'a::len word"
  2.1002 -  fixes n
  2.1003 +    and n :: nat
  2.1004    defines "n' \<equiv> len_of TYPE('a) - n"
  2.1005 -  shows "to_bl (w AND mask n) =  replicate n' False @ drop n' (to_bl w)"
  2.1006 +  shows "to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)"
  2.1007  proof -
  2.1008    note [simp] = map_replicate_True map_replicate_False
  2.1009 -  have "to_bl (w AND mask n) =
  2.1010 -        map2 op & (to_bl w) (to_bl (mask n::'a::len word))"
  2.1011 +  have "to_bl (w AND mask n) = map2 op \<and> (to_bl w) (to_bl (mask n::'a::len word))"
  2.1012      by (simp add: bl_word_and)
  2.1013 -  also
  2.1014 -  have "to_bl w = take n' (to_bl w) @ drop n' (to_bl w)" by simp
  2.1015 -  also
  2.1016 -  have "map2 op & \<dots> (to_bl (mask n::'a::len word)) =
  2.1017 -        replicate n' False @ drop n' (to_bl w)"
  2.1018 -    unfolding to_bl_mask n'_def map2_def
  2.1019 -    by (subst zip_append) auto
  2.1020 -  finally
  2.1021 -  show ?thesis .
  2.1022 +  also have "to_bl w = take n' (to_bl w) @ drop n' (to_bl w)"
  2.1023 +    by simp
  2.1024 +  also have "map2 op \<and> \<dots> (to_bl (mask n::'a::len word)) =
  2.1025 +      replicate n' False @ drop n' (to_bl w)"
  2.1026 +    unfolding to_bl_mask n'_def map2_def by (subst zip_append) auto
  2.1027 +  finally show ?thesis .
  2.1028  qed
  2.1029  
  2.1030  lemma drop_rev_takefill:
  2.1031 @@ -4321,61 +4255,53 @@
  2.1032      drop (n - length xs) (rev (takefill False n (rev xs))) = xs"
  2.1033    by (simp add: takefill_alt rev_take)
  2.1034  
  2.1035 -lemma map_nth_0 [simp]:
  2.1036 -  "map (op !! (0::'a::len0 word)) xs = replicate (length xs) False"
  2.1037 +lemma map_nth_0 [simp]: "map (op !! (0::'a::len0 word)) xs = replicate (length xs) False"
  2.1038    by (induct xs) auto
  2.1039  
  2.1040  lemma uint_plus_if_size:
  2.1041    "uint (x + y) =
  2.1042 -  (if uint x + uint y < 2^size x then
  2.1043 -      uint x + uint y
  2.1044 -   else
  2.1045 -      uint x + uint y - 2^size x)"
  2.1046 -  by (simp add: word_arith_wis int_word_uint mod_add_if_z
  2.1047 -                word_size)
  2.1048 +    (if uint x + uint y < 2^size x
  2.1049 +     then uint x + uint y
  2.1050 +     else uint x + uint y - 2^size x)"
  2.1051 +  by (simp add: word_arith_wis int_word_uint mod_add_if_z word_size)
  2.1052  
  2.1053  lemma unat_plus_if_size:
  2.1054    "unat (x + (y::'a::len word)) =
  2.1055 -  (if unat x + unat y < 2^size x then
  2.1056 -      unat x + unat y
  2.1057 -   else
  2.1058 -      unat x + unat y - 2^size x)"
  2.1059 +    (if unat x + unat y < 2^size x
  2.1060 +     then unat x + unat y
  2.1061 +     else unat x + unat y - 2^size x)"
  2.1062    apply (subst word_arith_nat_defs)
  2.1063    apply (subst unat_of_nat)
  2.1064    apply (simp add:  mod_nat_add word_size)
  2.1065    done
  2.1066  
  2.1067 -lemma word_neq_0_conv:
  2.1068 -  fixes w :: "'a::len word"
  2.1069 -  shows "(w \<noteq> 0) = (0 < w)"
  2.1070 -  unfolding word_gt_0 by simp
  2.1071 -
  2.1072 -lemma max_lt:
  2.1073 -  "unat (max a b div c) = unat (max a b) div unat (c:: 'a::len word)"
  2.1074 +lemma word_neq_0_conv: "w \<noteq> 0 \<longleftrightarrow> 0 < w"
  2.1075 +  for w :: "'a::len word"
  2.1076 +  by (simp add: word_gt_0)
  2.1077 +
  2.1078 +lemma max_lt: "unat (max a b div c) = unat (max a b) div unat c"
  2.1079 +  for c :: "'a::len word"
  2.1080    by (fact unat_div)
  2.1081  
  2.1082  lemma uint_sub_if_size:
  2.1083    "uint (x - y) =
  2.1084 -  (if uint y \<le> uint x then
  2.1085 -      uint x - uint y
  2.1086 -   else
  2.1087 -      uint x - uint y + 2^size x)"
  2.1088 -  by (simp add: word_arith_wis int_word_uint mod_sub_if_z
  2.1089 -                word_size)
  2.1090 -
  2.1091 -lemma unat_sub:
  2.1092 -  "b <= a \<Longrightarrow> unat (a - b) = unat a - unat b"
  2.1093 +    (if uint y \<le> uint x
  2.1094 +     then uint x - uint y
  2.1095 +     else uint x - uint y + 2^size x)"
  2.1096 +  by (simp add: word_arith_wis int_word_uint mod_sub_if_z word_size)
  2.1097 +
  2.1098 +lemma unat_sub: "b \<le> a \<Longrightarrow> unat (a - b) = unat a - unat b"
  2.1099    by (simp add: unat_def uint_sub_if_size word_le_def nat_diff_distrib)
  2.1100  
  2.1101  lemmas word_less_sub1_numberof [simp] = word_less_sub1 [of "numeral w"] for w
  2.1102  lemmas word_le_sub1_numberof [simp] = word_le_sub1 [of "numeral w"] for w
  2.1103  
  2.1104 -lemma word_of_int_minus:
  2.1105 -  "word_of_int (2^len_of TYPE('a) - i) = (word_of_int (-i)::'a::len word)"
  2.1106 +lemma word_of_int_minus: "word_of_int (2^len_of TYPE('a) - i) = (word_of_int (-i)::'a::len word)"
  2.1107  proof -
  2.1108 -  have x: "2^len_of TYPE('a) - i = -i + 2^len_of TYPE('a)" by simp
  2.1109 +  have *: "2^len_of TYPE('a) - i = -i + 2^len_of TYPE('a)"
  2.1110 +    by simp
  2.1111    show ?thesis
  2.1112 -    apply (subst x)
  2.1113 +    apply (subst *)
  2.1114      apply (subst word_uint.Abs_norm [symmetric], subst mod_add_self2)
  2.1115      apply simp
  2.1116      done
  2.1117 @@ -4384,35 +4310,37 @@
  2.1118  lemmas word_of_int_inj =
  2.1119    word_uint.Abs_inject [unfolded uints_num, simplified]
  2.1120  
  2.1121 -lemma word_le_less_eq:
  2.1122 -  "(x ::'z::len word) \<le> y = (x = y \<or> x < y)"
  2.1123 +lemma word_le_less_eq: "x \<le> y \<longleftrightarrow> x = y \<or> x < y"
  2.1124 +  for x y :: "'z::len word"
  2.1125    by (auto simp add: order_class.le_less)
  2.1126  
  2.1127  lemma mod_plus_cong:
  2.1128 -  assumes 1: "(b::int) = b'"
  2.1129 -      and 2: "x mod b' = x' mod b'"
  2.1130 -      and 3: "y mod b' = y' mod b'"
  2.1131 -      and 4: "x' + y' = z'"
  2.1132 +  fixes b b' :: int
  2.1133 +  assumes 1: "b = b'"
  2.1134 +    and 2: "x mod b' = x' mod b'"
  2.1135 +    and 3: "y mod b' = y' mod b'"
  2.1136 +    and 4: "x' + y' = z'"
  2.1137    shows "(x + y) mod b = z' mod b'"
  2.1138  proof -
  2.1139    from 1 2[symmetric] 3[symmetric] have "(x + y) mod b = (x' mod b' + y' mod b') mod b'"
  2.1140      by (simp add: mod_add_eq)
  2.1141    also have "\<dots> = (x' + y') mod b'"
  2.1142      by (simp add: mod_add_eq)
  2.1143 -  finally show ?thesis by (simp add: 4)
  2.1144 +  finally show ?thesis
  2.1145 +    by (simp add: 4)
  2.1146  qed
  2.1147  
  2.1148  lemma mod_minus_cong:
  2.1149 -  assumes 1: "(b::int) = b'"
  2.1150 -      and 2: "x mod b' = x' mod b'"
  2.1151 -      and 3: "y mod b' = y' mod b'"
  2.1152 -      and 4: "x' - y' = z'"
  2.1153 +  fixes b b' :: int
  2.1154 +  assumes "b = b'"
  2.1155 +    and "x mod b' = x' mod b'"
  2.1156 +    and "y mod b' = y' mod b'"
  2.1157 +    and "x' - y' = z'"
  2.1158    shows "(x - y) mod b = z' mod b'"
  2.1159 -  using 1 2 3 4 [symmetric]
  2.1160 -  by (auto intro: mod_diff_cong)
  2.1161 -
  2.1162 -lemma word_induct_less:
  2.1163 -  "\<lbrakk>P (0::'a::len word); \<And>n. \<lbrakk>n < m; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
  2.1164 +  using assms [symmetric] by (auto intro: mod_diff_cong)
  2.1165 +
  2.1166 +lemma word_induct_less: "\<lbrakk>P 0; \<And>n. \<lbrakk>n < m; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
  2.1167 +  for P :: "'a::len word \<Rightarrow> bool"
  2.1168    apply (cases m)
  2.1169    apply atomize
  2.1170    apply (erule rev_mp)+
  2.1171 @@ -4434,22 +4362,23 @@
  2.1172    apply simp
  2.1173    done
  2.1174  
  2.1175 -lemma word_induct:
  2.1176 -  "\<lbrakk>P (0::'a::len word); \<And>n. P n \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
  2.1177 -  by (erule word_induct_less, simp)
  2.1178 -
  2.1179 -lemma word_induct2 [induct type]:
  2.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)"
  2.1181 -  apply (rule word_induct, simp)
  2.1182 -  apply (case_tac "1+n = 0", auto)
  2.1183 +lemma word_induct: "\<lbrakk>P 0; \<And>n. P n \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
  2.1184 +  for P :: "'a::len word \<Rightarrow> bool"
  2.1185 +  by (erule word_induct_less) simp
  2.1186 +
  2.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"
  2.1188 +  for P :: "'b::len word \<Rightarrow> bool"
  2.1189 +  apply (rule word_induct)
  2.1190 +   apply simp
  2.1191 +  apply (case_tac "1 + n = 0")
  2.1192 +   apply auto
  2.1193    done
  2.1194  
  2.1195  
  2.1196  subsection \<open>Recursion combinator for words\<close>
  2.1197  
  2.1198  definition word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a"
  2.1199 -where
  2.1200 -  "word_rec forZero forSuc n = rec_nat forZero (forSuc \<circ> of_nat) (unat n)"
  2.1201 +  where "word_rec forZero forSuc n = rec_nat forZero (forSuc \<circ> of_nat) (unat n)"
  2.1202  
  2.1203  lemma word_rec_0: "word_rec z s 0 = z"
  2.1204    by (simp add: word_rec_def)
  2.1205 @@ -4471,79 +4400,75 @@
  2.1206    apply simp
  2.1207    done
  2.1208  
  2.1209 -lemma word_rec_in:
  2.1210 -  "f (word_rec z (\<lambda>_. f) n) = word_rec (f z) (\<lambda>_. f) n"
  2.1211 +lemma word_rec_in: "f (word_rec z (\<lambda>_. f) n) = word_rec (f z) (\<lambda>_. f) n"
  2.1212    by (induct n) (simp_all add: word_rec_0 word_rec_Suc)
  2.1213  
  2.1214 -lemma word_rec_in2:
  2.1215 -  "f n (word_rec z f n) = word_rec (f 0 z) (f \<circ> op + 1) n"
  2.1216 +lemma word_rec_in2: "f n (word_rec z f n) = word_rec (f 0 z) (f \<circ> op + 1) n"
  2.1217    by (induct n) (simp_all add: word_rec_0 word_rec_Suc)
  2.1218  
  2.1219  lemma word_rec_twice:
  2.1220    "m \<le> n \<Longrightarrow> word_rec z f n = word_rec (word_rec z f (n - m)) (f \<circ> op + (n - m)) m"
  2.1221 -apply (erule rev_mp)
  2.1222 -apply (rule_tac x=z in spec)
  2.1223 -apply (rule_tac x=f in spec)
  2.1224 -apply (induct n)
  2.1225 - apply (simp add: word_rec_0)
  2.1226 -apply clarsimp
  2.1227 -apply (rule_tac t="1 + n - m" and s="1 + (n - m)" in subst)
  2.1228 - apply simp
  2.1229 -apply (case_tac "1 + (n - m) = 0")
  2.1230 - apply (simp add: word_rec_0)
  2.1231 - apply (rule_tac f = "word_rec a b" for a b in arg_cong)
  2.1232 - apply (rule_tac t="m" and s="m + (1 + (n - m))" in subst)
  2.1233 +  apply (erule rev_mp)
  2.1234 +  apply (rule_tac x=z in spec)
  2.1235 +  apply (rule_tac x=f in spec)
  2.1236 +  apply (induct n)
  2.1237 +   apply (simp add: word_rec_0)
  2.1238 +  apply clarsimp
  2.1239 +  apply (rule_tac t="1 + n - m" and s="1 + (n - m)" in subst)
  2.1240 +   apply simp
  2.1241 +  apply (case_tac "1 + (n - m) = 0")
  2.1242 +   apply (simp add: word_rec_0)
  2.1243 +   apply (rule_tac f = "word_rec a b" for a b in arg_cong)
  2.1244 +   apply (rule_tac t="m" and s="m + (1 + (n - m))" in subst)
  2.1245 +    apply simp
  2.1246 +   apply (simp (no_asm_use))
  2.1247 +  apply (simp add: word_rec_Suc word_rec_in2)
  2.1248 +  apply (erule impE)
  2.1249 +   apply uint_arith
  2.1250 +  apply (drule_tac x="x \<circ> op + 1" in spec)
  2.1251 +  apply (drule_tac x="x 0 xa" in spec)
  2.1252    apply simp
  2.1253 - apply (simp (no_asm_use))
  2.1254 -apply (simp add: word_rec_Suc word_rec_in2)
  2.1255 -apply (erule impE)
  2.1256 - apply uint_arith
  2.1257 -apply (drule_tac x="x \<circ> op + 1" in spec)
  2.1258 -apply (drule_tac x="x 0 xa" in spec)
  2.1259 -apply simp
  2.1260 -apply (rule_tac t="\<lambda>a. x (1 + (n - m + a))" and s="\<lambda>a. x (1 + (n - m) + a)"
  2.1261 -       in subst)
  2.1262 - apply (clarsimp simp add: fun_eq_iff)
  2.1263 - apply (rule_tac t="(1 + (n - m + xb))" and s="1 + (n - m) + xb" in subst)
  2.1264 -  apply simp
  2.1265 - apply (rule refl)
  2.1266 -apply (rule refl)
  2.1267 -done
  2.1268 +  apply (rule_tac t="\<lambda>a. x (1 + (n - m + a))" and s="\<lambda>a. x (1 + (n - m) + a)" in subst)
  2.1269 +   apply (clarsimp simp add: fun_eq_iff)
  2.1270 +   apply (rule_tac t="(1 + (n - m + xb))" and s="1 + (n - m) + xb" in subst)
  2.1271 +    apply simp
  2.1272 +   apply (rule refl)
  2.1273 +  apply (rule refl)
  2.1274 +  done
  2.1275  
  2.1276  lemma word_rec_id: "word_rec z (\<lambda>_. id) n = z"
  2.1277    by (induct n) (auto simp add: word_rec_0 word_rec_Suc)
  2.1278  
  2.1279  lemma word_rec_id_eq: "\<forall>m < n. f m = id \<Longrightarrow> word_rec z f n = z"
  2.1280 -apply (erule rev_mp)
  2.1281 -apply (induct n)
  2.1282 - apply (auto simp add: word_rec_0 word_rec_Suc)
  2.1283 - apply (drule spec, erule mp)
  2.1284 - apply uint_arith
  2.1285 -apply (drule_tac x=n in spec, erule impE)
  2.1286 - apply uint_arith
  2.1287 -apply simp
  2.1288 -done
  2.1289 +  apply (erule rev_mp)
  2.1290 +  apply (induct n)
  2.1291 +   apply (auto simp add: word_rec_0 word_rec_Suc)
  2.1292 +   apply (drule spec, erule mp)
  2.1293 +   apply uint_arith
  2.1294 +  apply (drule_tac x=n in spec, erule impE)
  2.1295 +   apply uint_arith
  2.1296 +  apply simp
  2.1297 +  done
  2.1298  
  2.1299  lemma word_rec_max:
  2.1300    "\<forall>m\<ge>n. m \<noteq> - 1 \<longrightarrow> f m = id \<Longrightarrow> word_rec z f (- 1) = word_rec z f n"
  2.1301 -apply (subst word_rec_twice[where n="-1" and m="-1 - n"])
  2.1302 - apply simp
  2.1303 -apply simp
  2.1304 -apply (rule word_rec_id_eq)
  2.1305 -apply clarsimp
  2.1306 -apply (drule spec, rule mp, erule mp)
  2.1307 - apply (rule word_plus_mono_right2[OF _ order_less_imp_le])
  2.1308 -  prefer 2
  2.1309 -  apply assumption
  2.1310 - apply simp
  2.1311 -apply (erule contrapos_pn)
  2.1312 -apply simp
  2.1313 -apply (drule arg_cong[where f="\<lambda>x. x - n"])
  2.1314 -apply simp
  2.1315 -done
  2.1316 -
  2.1317 -lemma unatSuc:
  2.1318 -  "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> unat (1 + n) = Suc (unat n)"
  2.1319 +  apply (subst word_rec_twice[where n="-1" and m="-1 - n"])
  2.1320 +   apply simp
  2.1321 +  apply simp
  2.1322 +  apply (rule word_rec_id_eq)
  2.1323 +  apply clarsimp
  2.1324 +  apply (drule spec, rule mp, erule mp)
  2.1325 +   apply (rule word_plus_mono_right2[OF _ order_less_imp_le])
  2.1326 +    prefer 2
  2.1327 +    apply assumption
  2.1328 +   apply simp
  2.1329 +  apply (erule contrapos_pn)
  2.1330 +  apply simp
  2.1331 +  apply (drule arg_cong[where f="\<lambda>x. x - n"])
  2.1332 +  apply simp
  2.1333 +  done
  2.1334 +
  2.1335 +lemma unatSuc: "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> unat (1 + n) = Suc (unat n)"
  2.1336    by unat_arith
  2.1337  
  2.1338  declare bin_to_bl_def [simp]
     3.1 --- a/src/Pure/General/symbol.scala	Mon Mar 20 21:01:47 2017 +0100
     3.2 +++ b/src/Pure/General/symbol.scala	Mon Mar 20 21:53:37 2017 +0100
     3.3 @@ -198,6 +198,25 @@
     3.4      case class Id(id: Document_ID.Generic) extends Name
     3.5      case class File(name: String) extends Name
     3.6  
     3.7 +    val encode_name: XML.Encode.T[Name] =
     3.8 +    {
     3.9 +      import XML.Encode._
    3.10 +      variant(List(
    3.11 +        { case Default => (Nil, Nil) },
    3.12 +        { case Id(a) => (List(long_atom(a)), Nil) },
    3.13 +        { case File(a) => (List(a), Nil) }))
    3.14 +    }
    3.15 +
    3.16 +    val decode_name: XML.Decode.T[Name] =
    3.17 +    {
    3.18 +      import XML.Decode._
    3.19 +      variant(List(
    3.20 +        { case (Nil, Nil) => Default },
    3.21 +        { case (List(a), Nil) => Id(long_atom(a)) },
    3.22 +        { case (List(a), Nil) => File(a) }))
    3.23 +    }
    3.24 +
    3.25 +
    3.26      def apply(text: CharSequence): Text_Chunk =
    3.27        new Text_Chunk(Text.Range(0, text.length), Index(text))
    3.28    }
     4.1 --- a/src/Pure/Isar/token.scala	Mon Mar 20 21:01:47 2017 +0100
     4.2 +++ b/src/Pure/Isar/token.scala	Mon Mar 20 21:53:37 2017 +0100
     4.3 @@ -218,6 +218,22 @@
     4.4  
     4.5    def reader(tokens: List[Token], start: Token.Pos): Reader =
     4.6      new Token_Reader(tokens, start)
     4.7 +
     4.8 +
     4.9 +  /* XML data representation */
    4.10 +
    4.11 +  val encode: XML.Encode.T[Token] = (tok: Token) =>
    4.12 +  {
    4.13 +    import XML.Encode._
    4.14 +    pair(int, string)(tok.kind.id, tok.source)
    4.15 +  }
    4.16 +
    4.17 +  val decode: XML.Decode.T[Token] = (body: XML.Body) =>
    4.18 +  {
    4.19 +    import XML.Decode._
    4.20 +    val (k, s) = pair(int, string)(body)
    4.21 +    Token(Kind(k), s)
    4.22 +  }
    4.23  }
    4.24  
    4.25  
     5.1 --- a/src/Pure/PIDE/command.scala	Mon Mar 20 21:01:47 2017 +0100
     5.2 +++ b/src/Pure/PIDE/command.scala	Mon Mar 20 21:53:37 2017 +0100
     5.3 @@ -31,6 +31,15 @@
     5.4      val empty = new Results(SortedMap.empty)
     5.5      def make(args: TraversableOnce[Results.Entry]): Results = (empty /: args)(_ + _)
     5.6      def merge(args: TraversableOnce[Results]): Results = (empty /: args)(_ ++ _)
     5.7 +
     5.8 +
     5.9 +    /* XML data representation */
    5.10 +
    5.11 +    val encode: XML.Encode.T[Results] = (results: Results) =>
    5.12 +    { import XML.Encode._; list(pair(long, tree))(results.rep.toList) }
    5.13 +
    5.14 +    val decode: XML.Decode.T[Results] = (body: XML.Body) =>
    5.15 +    { import XML.Decode._; make(list(pair(long, tree))(body)) }
    5.16    }
    5.17  
    5.18    final class Results private(private val rep: SortedMap[Long, XML.Tree])
    5.19 @@ -71,9 +80,37 @@
    5.20    object Markups
    5.21    {
    5.22      val empty: Markups = new Markups(Map.empty)
    5.23 +    def init(markup: Markup_Tree): Markups = new Markups(Map(Markup_Index.markup -> markup))
    5.24 +    def merge(args: TraversableOnce[Markups]): Markups = (empty /: args)(_ ++ _)
    5.25  
    5.26 -    def init(markup: Markup_Tree): Markups =
    5.27 -      new Markups(Map(Markup_Index.markup -> markup))
    5.28 +
    5.29 +    /* XML data representation */
    5.30 +
    5.31 +    def encode(source_length: Int): XML.Encode.T[Markups] = (markups: Markups) =>
    5.32 +    {
    5.33 +      import XML.Encode._
    5.34 +
    5.35 +      val markup_index: T[Markup_Index] = (index: Markup_Index) =>
    5.36 +        pair(bool, Symbol.Text_Chunk.encode_name)(index.status, index.chunk_name)
    5.37 +
    5.38 +      val markup_tree: T[Markup_Tree] =
    5.39 +        _.to_XML(Text.Range(0, source_length), Symbol.spaces(source_length), Markup.Elements.full)
    5.40 +
    5.41 +      list(pair(markup_index, markup_tree))(markups.rep.toList)
    5.42 +    }
    5.43 +
    5.44 +    val decode: XML.Decode.T[Markups] = (body: XML.Body) =>
    5.45 +    {
    5.46 +      import XML.Decode._
    5.47 +
    5.48 +      val markup_index: T[Markup_Index] = (body: XML.Body) =>
    5.49 +      {
    5.50 +        val (status, chunk_name) = pair(bool, Symbol.Text_Chunk.decode_name)(body)
    5.51 +        Markup_Index(status, chunk_name)
    5.52 +      }
    5.53 +
    5.54 +      (Markups.empty /: list(pair(markup_index, Markup_Tree.from_XML(_)))(body))(_ + _)
    5.55 +    }
    5.56    }
    5.57  
    5.58    final class Markups private(private val rep: Map[Markup_Index, Markup_Tree])
    5.59 @@ -86,6 +123,17 @@
    5.60      def add(index: Markup_Index, markup: Text.Markup): Markups =
    5.61        new Markups(rep + (index -> (this(index) + markup)))
    5.62  
    5.63 +    def + (entry: (Markup_Index, Markup_Tree)): Markups =
    5.64 +    {
    5.65 +      val (index, tree) = entry
    5.66 +      new Markups(rep + (index -> (this(index).merge(tree, Text.Range.full, Markup.Elements.full))))
    5.67 +    }
    5.68 +
    5.69 +    def ++ (other: Markups): Markups =
    5.70 +      if (this eq other) this
    5.71 +      else if (rep.isEmpty) other
    5.72 +      else (this /: other.rep.iterator)(_ + _)
    5.73 +
    5.74      def redirection_iterator: Iterator[Document_ID.Generic] =
    5.75        for (Markup_Index(_, Symbol.Text_Chunk.Id(id)) <- rep.keysIterator)
    5.76          yield id
    5.77 @@ -114,12 +162,49 @@
    5.78  
    5.79    object State
    5.80    {
    5.81 -    def merge_results(states: List[State]): Command.Results =
    5.82 +    def merge_results(states: List[State]): Results =
    5.83        Results.merge(states.map(_.results))
    5.84  
    5.85 +    def merge_markups(states: List[State]): Markups =
    5.86 +      Markups.merge(states.map(_.markups))
    5.87 +
    5.88      def merge_markup(states: List[State], index: Markup_Index,
    5.89          range: Text.Range, elements: Markup.Elements): Markup_Tree =
    5.90        Markup_Tree.merge(states.map(_.markup(index)), range, elements)
    5.91 +
    5.92 +    def merge(command: Command, states: List[State]): State =
    5.93 +      State(command, states.flatMap(_.status), merge_results(states), merge_markups(states))
    5.94 +
    5.95 +
    5.96 +    /* XML data representation */
    5.97 +
    5.98 +    val encode: XML.Encode.T[State] = (st: State) =>
    5.99 +    {
   5.100 +      import XML.Encode._
   5.101 +
   5.102 +      val command = st.command
   5.103 +      val blobs_names = command.blobs_names.map(_.node)
   5.104 +      val blobs_index = command.blobs_index
   5.105 +      require(command.blobs_ok)
   5.106 +
   5.107 +      pair(long, pair(string, pair(pair(list(string), int), pair(Command_Span.encode,
   5.108 +          pair(list(Markup.encode), pair(Results.encode, Markups.encode(command.source.length)))))))(
   5.109 +        (command.id, (command.node_name.node, ((blobs_names, blobs_index), (command.span,
   5.110 +          (st.status, (st.results, st.markups)))))))
   5.111 +    }
   5.112 +
   5.113 +    def decode(node_name: String => Document.Node.Name): XML.Decode.T[State] = (body: XML.Body) =>
   5.114 +    {
   5.115 +      import XML.Decode._
   5.116 +      val (id, (node, ((blobs_names, blobs_index), (span, (status, (results, markups)))))) =
   5.117 +        pair(long, pair(string, pair(pair(list(string), int), pair(Command_Span.decode,
   5.118 +          pair(list(Markup.decode), pair(Results.decode, Markups.decode))))))(body)
   5.119 +
   5.120 +      val blobs_info: Blobs_Info =
   5.121 +        (blobs_names.map(name => Exn.Res((node_name(name), None)): Blob), blobs_index)
   5.122 +      val command = Command(id, node_name(node), blobs_info, span)
   5.123 +      State(command, status, results, markups)
   5.124 +    }
   5.125    }
   5.126  
   5.127    sealed case class State(
   5.128 @@ -404,6 +489,9 @@
   5.129    def blobs: List[Command.Blob] = blobs_info._1
   5.130    def blobs_index: Int = blobs_info._2
   5.131  
   5.132 +  def blobs_ok: Boolean =
   5.133 +    blobs.forall({ case Exn.Res(_) => true case _ => false })
   5.134 +
   5.135    def blobs_names: List[Document.Node.Name] =
   5.136      for (Exn.Res((name, _)) <- blobs) yield name
   5.137  
     6.1 --- a/src/Pure/PIDE/command_span.scala	Mon Mar 20 21:01:47 2017 +0100
     6.2 +++ b/src/Pure/PIDE/command_span.scala	Mon Mar 20 21:53:37 2017 +0100
     6.3 @@ -56,4 +56,30 @@
     6.4  
     6.5    def unparsed(source: String): Span =
     6.6      Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
     6.7 +
     6.8 +
     6.9 +  /* XML data representation */
    6.10 +
    6.11 +  def encode: XML.Encode.T[Span] = (span: Span) =>
    6.12 +  {
    6.13 +    import XML.Encode._
    6.14 +    val kind: T[Kind] =
    6.15 +      variant(List(
    6.16 +        { case Command_Span(a, b) => (List(a), properties(b)) },
    6.17 +        { case Ignored_Span => (Nil, Nil) },
    6.18 +        { case Malformed_Span => (Nil, Nil) }))
    6.19 +    pair(kind, list(Token.encode))((span.kind, span.content))
    6.20 +  }
    6.21 +
    6.22 +  def decode: XML.Decode.T[Span] = (body: XML.Body) =>
    6.23 +  {
    6.24 +    import XML.Decode._
    6.25 +    val kind: T[Kind] =
    6.26 +      variant(List(
    6.27 +        { case (List(a), b) => Command_Span(a, properties(b)) },
    6.28 +        { case (Nil, Nil) => Ignored_Span },
    6.29 +        { case (Nil, Nil) => Malformed_Span }))
    6.30 +    val (k, toks) = pair(kind, list(Token.decode))(body)
    6.31 +    Span(k, toks)
    6.32 +  }
    6.33  }
     7.1 --- a/src/Pure/PIDE/document.scala	Mon Mar 20 21:01:47 2017 +0100
     7.2 +++ b/src/Pure/PIDE/document.scala	Mon Mar 20 21:53:37 2017 +0100
     7.3 @@ -449,7 +449,6 @@
     7.4      def node: Node
     7.5      def commands_loading: List[Command]
     7.6      def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range]
     7.7 -    def command_results(command: Command): Command.Results
     7.8      def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command]
     7.9  
    7.10      def find_command(id: Document_ID.Generic): Option[(Node, Command)]
    7.11 @@ -468,6 +467,9 @@
    7.12        elements: Markup.Elements,
    7.13        result: List[Command.State] => Text.Markup => Option[A],
    7.14        status: Boolean = false): List[Text.Info[A]]
    7.15 +
    7.16 +    def command_results(range: Text.Range): Command.Results
    7.17 +    def command_results(command: Command): Command.Results
    7.18    }
    7.19  
    7.20  
    7.21 @@ -827,9 +829,6 @@
    7.22              start <- node.command_start(cmd)
    7.23            } yield convert(cmd.proper_range + start)).toList
    7.24  
    7.25 -        def command_results(command: Command): Command.Results =
    7.26 -          state.command_results(version, command)
    7.27 -
    7.28          def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command] =
    7.29            if (other_node_name.is_theory) {
    7.30              val other_node = version.nodes(other_node_name)
    7.31 @@ -919,6 +918,17 @@
    7.32          }
    7.33  
    7.34  
    7.35 +        /* command results */
    7.36 +
    7.37 +        def command_results(range: Text.Range): Command.Results =
    7.38 +          Command.State.merge_results(
    7.39 +            select[List[Command.State]](range, Markup.Elements.full, command_states =>
    7.40 +              { case _ => Some(command_states) }).flatMap(_.info))
    7.41 +
    7.42 +        def command_results(command: Command): Command.Results =
    7.43 +          state.command_results(version, command)
    7.44 +
    7.45 +
    7.46          /* output */
    7.47  
    7.48          override def toString: String =
     8.1 --- a/src/Pure/PIDE/markup.scala	Mon Mar 20 21:01:47 2017 +0100
     8.2 +++ b/src/Pure/PIDE/markup.scala	Mon Mar 20 21:53:37 2017 +0100
     8.3 @@ -607,6 +607,22 @@
     8.4          case _ => None
     8.5        }
     8.6    }
     8.7 +
     8.8 +
     8.9 +  /* XML data representation */
    8.10 +
    8.11 +  def encode: XML.Encode.T[Markup] = (markup: Markup) =>
    8.12 +  {
    8.13 +    import XML.Encode._
    8.14 +    pair(string, properties)((markup.name, markup.properties))
    8.15 +  }
    8.16 +
    8.17 +  def decode: XML.Decode.T[Markup] = (body: XML.Body) =>
    8.18 +  {
    8.19 +    import XML.Decode._
    8.20 +    val (name, props) = pair(string, properties)(body)
    8.21 +    Markup(name, props)
    8.22 +  }
    8.23  }
    8.24  
    8.25  
     9.1 --- a/src/Pure/PIDE/xml.ML	Mon Mar 20 21:01:47 2017 +0100
     9.2 +++ b/src/Pure/PIDE/xml.ML	Mon Mar 20 21:53:37 2017 +0100
     9.3 @@ -52,8 +52,16 @@
     9.4    val parse: string -> tree
     9.5    exception XML_ATOM of string
     9.6    exception XML_BODY of body
     9.7 -  structure Encode: XML_DATA_OPS
     9.8 -  structure Decode: XML_DATA_OPS
     9.9 +  structure Encode:
    9.10 +  sig
    9.11 +    include XML_DATA_OPS
    9.12 +    val tree: tree T
    9.13 +  end
    9.14 +  structure Decode:
    9.15 +  sig
    9.16 +    include XML_DATA_OPS
    9.17 +    val tree: tree T
    9.18 +  end
    9.19  end;
    9.20  
    9.21  structure XML: XML =
    9.22 @@ -302,6 +310,8 @@
    9.23  
    9.24  (* representation of standard types *)
    9.25  
    9.26 +fun tree (t: tree) = [t];
    9.27 +
    9.28  fun properties props = [Elem ((":", props), [])];
    9.29  
    9.30  fun string "" = []
    9.31 @@ -364,6 +374,9 @@
    9.32  
    9.33  (* representation of standard types *)
    9.34  
    9.35 +fun tree [t] = t
    9.36 +  | tree ts = raise XML_BODY ts;
    9.37 +
    9.38  fun properties [Elem ((":", props), [])] = props
    9.39    | properties ts = raise XML_BODY ts;
    9.40  
    10.1 --- a/src/Pure/PIDE/xml.scala	Mon Mar 20 21:01:47 2017 +0100
    10.2 +++ b/src/Pure/PIDE/xml.scala	Mon Mar 20 21:53:37 2017 +0100
    10.3 @@ -214,6 +214,7 @@
    10.4    object Encode
    10.5    {
    10.6      type T[A] = A => XML.Body
    10.7 +    type V[A] = PartialFunction[A, (List[String], XML.Body)]
    10.8  
    10.9  
   10.10      /* atomic values */
   10.11 @@ -240,6 +241,8 @@
   10.12  
   10.13      /* representation of standard types */
   10.14  
   10.15 +    val tree: T[XML.Tree] = (t => List(t))
   10.16 +
   10.17      val properties: T[Properties.T] =
   10.18        (props => List(XML.Elem(Markup(":", props), Nil)))
   10.19  
   10.20 @@ -268,7 +271,7 @@
   10.21        case Some(x) => List(node(f(x)))
   10.22      }
   10.23  
   10.24 -    def variant[A](fs: List[PartialFunction[A, (List[String], XML.Body)]]): T[A] =
   10.25 +    def variant[A](fs: List[V[A]]): T[A] =
   10.26      {
   10.27        case x =>
   10.28          val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
   10.29 @@ -322,6 +325,12 @@
   10.30  
   10.31      /* representation of standard types */
   10.32  
   10.33 +    val tree: T[XML.Tree] =
   10.34 +    {
   10.35 +      case List(t) => t
   10.36 +      case ts => throw new XML_Body(ts)
   10.37 +    }
   10.38 +
   10.39      val properties: T[Properties.T] =
   10.40      {
   10.41        case List(XML.Elem(Markup(":", props), Nil)) => props
    11.1 --- a/src/Tools/jEdit/src/document_view.scala	Mon Mar 20 21:01:47 2017 +0100
    11.2 +++ b/src/Tools/jEdit/src/document_view.scala	Mon Mar 20 21:53:37 2017 +0100
    11.3 @@ -213,7 +213,6 @@
    11.4                val snapshot = model.snapshot()
    11.5  
    11.6                if (changed.assignment ||
    11.7 -                  snapshot.commands_loading.exists(changed.commands.contains) ||
    11.8                    (changed.nodes.contains(model.node_name) &&
    11.9                     changed.commands.exists(snapshot.node.commands.contains)))
   11.10                  text_overview.invoke()
    12.1 --- a/src/Tools/jEdit/src/jedit_rendering.scala	Mon Mar 20 21:01:47 2017 +0100
    12.2 +++ b/src/Tools/jEdit/src/jedit_rendering.scala	Mon Mar 20 21:53:37 2017 +0100
    12.3 @@ -353,11 +353,6 @@
    12.4            else Some(Text.Info(snapshot.convert(info_range), elem))
    12.5        }).headOption.map(_.info)
    12.6  
    12.7 -  def command_results(range: Text.Range): Command.Results =
    12.8 -    Command.State.merge_results(
    12.9 -      snapshot.select[List[Command.State]](range, Markup.Elements.full, command_states =>
   12.10 -        { case _ => Some(command_states) }).flatMap(_.info))
   12.11 -
   12.12  
   12.13    /* tooltips */
   12.14  
    13.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Mar 20 21:01:47 2017 +0100
    13.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Mar 20 21:53:37 2017 +0100
    13.3 @@ -271,7 +271,7 @@
    13.4                          case Some(tip) =>
    13.5                            val painter = text_area.getPainter
    13.6                            val loc = new Point(x, y + painter.getLineHeight / 2)
    13.7 -                          val results = rendering.command_results(tip.range)
    13.8 +                          val results = snapshot.command_results(tip.range)
    13.9                            Pretty_Tooltip(view, painter, loc, rendering, results, tip)
   13.10                        }
   13.11                    }