merged
authorhuffman
Tue Nov 30 20:02:01 2010 -0800 (2010-11-30)
changeset 40835fc750e794458
parent 40834 a1249aeff5b6
parent 40829 edd1e0764da1
child 40836 a81d66d72e70
child 40846 5a2ae8cc9d0e
child 40855 149dcaa26728
merged
     1.1 --- a/src/HOL/Tools/SMT/smt_failure.ML	Tue Nov 30 15:56:19 2010 -0800
     1.2 +++ b/src/HOL/Tools/SMT/smt_failure.ML	Tue Nov 30 20:02:01 2010 -0800
     1.3 @@ -6,12 +6,17 @@
     1.4  
     1.5  signature SMT_FAILURE =
     1.6  sig
     1.7 +  type counterexample = {
     1.8 +    is_real_cex: bool,
     1.9 +    free_constraints: term list,
    1.10 +    const_defs: term list}
    1.11    datatype failure =
    1.12 -    Counterexample of bool * term list |
    1.13 +    Counterexample of counterexample |
    1.14      Time_Out |
    1.15      Out_Of_Memory |
    1.16      Abnormal_Termination of int |
    1.17      Other_Failure of string
    1.18 +  val pretty_counterexample: Proof.context -> counterexample -> Pretty.T
    1.19    val string_of_failure: Proof.context -> failure -> string
    1.20    exception SMT of failure
    1.21  end
    1.22 @@ -19,23 +24,32 @@
    1.23  structure SMT_Failure: SMT_FAILURE =
    1.24  struct
    1.25  
    1.26 +type counterexample = {
    1.27 +  is_real_cex: bool,
    1.28 +  free_constraints: term list,
    1.29 +  const_defs: term list}
    1.30 +
    1.31  datatype failure =
    1.32 -  Counterexample of bool * term list |
    1.33 +  Counterexample of counterexample |
    1.34    Time_Out |
    1.35    Out_Of_Memory |
    1.36    Abnormal_Termination of int |
    1.37    Other_Failure of string
    1.38  
    1.39 -fun string_of_failure ctxt (Counterexample (real, ex)) =
    1.40 -      let
    1.41 -        val msg =
    1.42 -          if real then "Counterexample found (possibly spurious)"
    1.43 -          else "Potential counterexample found"
    1.44 -      in
    1.45 -        if null ex then msg
    1.46 -        else Pretty.string_of (Pretty.big_list (msg ^ ":")
    1.47 -          (map (Syntax.pretty_term ctxt) ex))
    1.48 -      end
    1.49 +fun pretty_counterexample ctxt {is_real_cex, free_constraints, const_defs} =
    1.50 +  let
    1.51 +    val msg =
    1.52 +      if is_real_cex then "Counterexample found (possibly spurious)"
    1.53 +      else "Potential counterexample found"
    1.54 +  in
    1.55 +    if null free_constraints andalso null const_defs then Pretty.str msg
    1.56 +    else
    1.57 +      Pretty.big_list (msg ^ ":")
    1.58 +        (map (Syntax.pretty_term ctxt) (free_constraints @ const_defs))
    1.59 +  end
    1.60 +
    1.61 +fun string_of_failure ctxt (Counterexample cex) =
    1.62 +      Pretty.string_of (pretty_counterexample ctxt cex)
    1.63    | string_of_failure _ Time_Out = "Timed out"
    1.64    | string_of_failure _ Out_Of_Memory = "Ran out of memory"
    1.65    | string_of_failure _ (Abnormal_Termination err) =
     2.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Tue Nov 30 15:56:19 2010 -0800
     2.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Tue Nov 30 20:02:01 2010 -0800
     2.3 @@ -19,7 +19,7 @@
     2.4      interface: interface,
     2.5      outcome: string -> string list -> outcome * string list,
     2.6      cex_parser: (Proof.context -> SMT_Translate.recon -> string list ->
     2.7 -      term list) option,
     2.8 +      term list * term list) option,
     2.9      reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
    2.10        (int list * thm) * Proof.context) option }
    2.11  
    2.12 @@ -65,7 +65,7 @@
    2.13    interface: interface,
    2.14    outcome: string -> string list -> outcome * string list,
    2.15    cex_parser: (Proof.context -> SMT_Translate.recon -> string list ->
    2.16 -    term list) option,
    2.17 +    term list * term list) option,
    2.18    reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
    2.19      (int list * thm) * Proof.context) option }
    2.20  
    2.21 @@ -260,9 +260,14 @@
    2.22          then the reconstruct ctxt recon ls
    2.23          else (([], ocl ()), ctxt)
    2.24      | (result, ls) =>
    2.25 -        let val ts = (case cex_parser of SOME f => f ctxt recon ls | _ => [])
    2.26 -        in
    2.27 -          raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat, ts))
    2.28 +        let
    2.29 +          val (ts, us) =
    2.30 +            (case cex_parser of SOME f => f ctxt recon ls | _ => ([], []))
    2.31 +         in
    2.32 +          raise SMT_Failure.SMT (SMT_Failure.Counterexample {
    2.33 +            is_real_cex = (result = Sat),
    2.34 +            free_constraints = ts,
    2.35 +            const_defs = us})
    2.36          end)
    2.37  
    2.38    val cfalse = Thm.cterm_of @{theory} (@{const Trueprop} $ @{const False})
    2.39 @@ -351,15 +356,14 @@
    2.40      let
    2.41        fun solve irules = snd (smt_solver NONE ctxt' irules)
    2.42        val tag = "Solver " ^ C.solver_of ctxt' ^ ": "
    2.43 -      val str_of = SMT_Failure.string_of_failure ctxt'
    2.44 +      val str_of = prefix tag o SMT_Failure.string_of_failure ctxt'
    2.45        fun safe_solve irules =
    2.46          if pass_exns then SOME (solve irules)
    2.47          else (SOME (solve irules)
    2.48            handle
    2.49              SMT_Failure.SMT (fail as SMT_Failure.Counterexample _) =>
    2.50 -              (C.verbose_msg ctxt' (prefix tag o str_of) fail; NONE)
    2.51 -          | SMT_Failure.SMT fail =>
    2.52 -              (C.trace_msg ctxt' (prefix tag o str_of) fail; NONE))
    2.53 +              (C.verbose_msg ctxt' str_of fail; NONE)
    2.54 +          | SMT_Failure.SMT fail => (C.trace_msg ctxt' str_of fail; NONE))
    2.55      in
    2.56        safe_solve (map (pair ~1) (rules @ prems))
    2.57        |> (fn SOME thm => Tactic.rtac thm 1 | _ => Tactical.no_tac)
     3.1 --- a/src/HOL/Tools/SMT/z3_model.ML	Tue Nov 30 15:56:19 2010 -0800
     3.2 +++ b/src/HOL/Tools/SMT/z3_model.ML	Tue Nov 30 20:02:01 2010 -0800
     3.3 @@ -7,7 +7,7 @@
     3.4  signature Z3_MODEL =
     3.5  sig
     3.6    val parse_counterex: Proof.context -> SMT_Translate.recon -> string list ->
     3.7 -    term list
     3.8 +    term list * term list
     3.9  end
    3.10  
    3.11  structure Z3_Model: Z3_MODEL =
    3.12 @@ -70,117 +70,51 @@
    3.13  val cex = space |--
    3.14    Scan.repeat (name --| $$$ "->" -- (func || expr >> (single o pair [])))
    3.15  
    3.16 -fun read_cex ls =
    3.17 +fun resolve terms ((n, k), cases) =
    3.18 +  (case Symtab.lookup terms n of
    3.19 +    NONE => NONE
    3.20 +  | SOME t => SOME ((t, k), cases))
    3.21 +
    3.22 +fun annotate _ (_, []) = NONE
    3.23 +  | annotate terms (n, [([], c)]) = resolve terms ((n, 0), (c, []))
    3.24 +  | annotate _ (_, [_]) = NONE
    3.25 +  | annotate terms (n, cases as (args, _) :: _) =
    3.26 +      let val (cases', (_, else_case)) = split_last cases
    3.27 +      in resolve terms ((n, length args), (else_case, cases')) end
    3.28 +
    3.29 +fun read_cex terms ls =
    3.30    maps (cons "\n" o raw_explode) ls
    3.31    |> try (fst o Scan.finite Symbol.stopper cex)
    3.32    |> the_default []
    3.33 -
    3.34 -
    3.35 -(* normalization *)
    3.36 -
    3.37 -local
    3.38 -  fun matches terms f n =
    3.39 -    (case Symtab.lookup terms n of
    3.40 -      NONE => false
    3.41 -    | SOME t => f t)
    3.42 -
    3.43 -  fun subst f (n, cases) = (n, map (fn (args, v) => (map f args, f v)) cases)
    3.44 -in
    3.45 -
    3.46 -fun reduce_function (n, [c]) = SOME ((n, 0), [c])
    3.47 -  | reduce_function (n, cases) =
    3.48 -      let val (patterns, else_case as (_, e)) = split_last cases
    3.49 -      in
    3.50 -        (case patterns of
    3.51 -          [] => NONE
    3.52 -        | (args, _) :: _ => SOME ((n, length args),
    3.53 -            filter_out (equal e o snd) patterns @ [else_case]))
    3.54 -      end
    3.55 -
    3.56 -fun drop_skolem_constants terms = filter (Symtab.defined terms o fst o fst)
    3.57 -
    3.58 -fun substitute_constants terms =
    3.59 -  let
    3.60 -    fun check vs1 [] = rev vs1
    3.61 -      | check vs1 ((v as ((n, k), [([], Value i)])) :: vs2) =
    3.62 -          if matches terms (fn Free _ => true | _ => false) n orelse k > 0
    3.63 -          then check (v :: vs1) vs2
    3.64 -          else
    3.65 -            let
    3.66 -              fun sub (e as Value j) = if i = j then App (n, []) else e
    3.67 -                | sub e = e
    3.68 -            in check (map (subst sub) vs1) (map (subst sub) vs2) end
    3.69 -      | check vs1 (v :: vs2) = check (v :: vs1) vs2
    3.70 -  in check [] end
    3.71 -
    3.72 -fun remove_int_nat_coercions terms vs =
    3.73 -  let
    3.74 -    fun match ts ((n, _), _) = matches terms (member (op aconv) ts) n
    3.75 -
    3.76 -    val (default_int, ints) =
    3.77 -      (case find_first (match [@{const of_nat (int)}]) vs of
    3.78 -        NONE => (NONE, [])
    3.79 -      | SOME (_, cases) =>
    3.80 -          let val (cs, (_, e)) = split_last cases
    3.81 -          in (SOME e, map (apfst hd) cs) end)
    3.82 -
    3.83 -    fun nat_of @{typ nat} (v as Value _) =
    3.84 -          AList.lookup (op =) ints v |> the_default (the_default v default_int)
    3.85 -      | nat_of _ e = e
    3.86 -
    3.87 -    fun subst_nat T k ([], e) =
    3.88 -          let fun app f i = if i <= 0 then I else app f (i-1) o f
    3.89 -          in ([], nat_of (app Term.range_type k T) e) end
    3.90 -      | subst_nat T k (arg :: args, e) =
    3.91 -          subst_nat (Term.range_type T) (k-1) (args, e)
    3.92 -          |> apfst (cons (nat_of (Term.domain_type T) arg))
    3.93 -
    3.94 -    fun subst_nats (v as ((n, k), cases)) =
    3.95 -      (case Symtab.lookup terms n of
    3.96 -        NONE => v
    3.97 -      | SOME t => ((n, k), map (subst_nat (Term.fastype_of t) k) cases))
    3.98 -  in
    3.99 -    map subst_nats vs
   3.100 -    |> filter_out (match [@{const of_nat (int)}, @{const nat}])
   3.101 -  end
   3.102 -
   3.103 -fun filter_valid_valuations terms = map_filter (fn
   3.104 -    (_, []) => NONE
   3.105 -  | ((n, i), cases) =>
   3.106 -      let
   3.107 -        fun valid_expr (Array a) = valid_array a
   3.108 -          | valid_expr (App (n, es)) =
   3.109 -              Symtab.defined terms n andalso forall valid_expr es
   3.110 -          | valid_expr _ = true
   3.111 -        and valid_array (Fresh e) = valid_expr e
   3.112 -          | valid_array (Store ((a, e1), e2)) =
   3.113 -              valid_array a andalso valid_expr e1 andalso valid_expr e2
   3.114 -        fun valid_case (es, e) = forall valid_expr (e :: es)
   3.115 -      in
   3.116 -        if not (forall valid_case cases) then NONE
   3.117 -        else Option.map (rpair cases o rpair i) (Symtab.lookup terms n)
   3.118 -      end)
   3.119 -
   3.120 -end
   3.121 +  |> map_filter (annotate terms)
   3.122  
   3.123  
   3.124  (* translation into terms *)
   3.125  
   3.126 -fun with_context ctxt terms f vs =
   3.127 -  fst (fold_map f vs (ctxt, terms, Inttab.empty))
   3.128 +fun max_value vs =
   3.129 +  let
   3.130 +    fun max_val_expr (Value i) = Integer.max i
   3.131 +      | max_val_expr (App (_, es)) = fold max_val_expr es
   3.132 +      | max_val_expr (Array a) = max_val_array a
   3.133 +      | max_val_expr _ = I
   3.134  
   3.135 -fun fresh_term T (ctxt, terms, values) =
   3.136 -  let val (n, ctxt') = yield_singleton Variable.variant_fixes "" ctxt
   3.137 -  in (Free (n, T), (ctxt', terms, values)) end
   3.138 +    and max_val_array (Fresh e) = max_val_expr e
   3.139 +      | max_val_array (Store ((a, e1), e2)) =
   3.140 +          max_val_array a #> max_val_expr e1 #> max_val_expr e2
   3.141  
   3.142 -fun term_of_value T i (cx as (_, _, values)) =
   3.143 -  (case Inttab.lookup values i of
   3.144 -    SOME t => (t, cx)
   3.145 +    fun max_val (_, (ec, cs)) =
   3.146 +      max_val_expr ec #> fold (fn (es, e) => fold max_val_expr (e :: es)) cs
   3.147 +
   3.148 +  in fold max_val vs ~1 end
   3.149 +
   3.150 +fun with_context terms f vs = fst (fold_map f vs (terms, max_value vs + 1))
   3.151 +
   3.152 +fun get_term n T es (cx as (terms, next_val)) =
   3.153 +  (case Symtab.lookup terms n of
   3.154 +    SOME t => ((t, es), cx)
   3.155    | NONE =>
   3.156 -      let val (t, (ctxt', terms', values')) = fresh_term T cx
   3.157 -      in (t, (ctxt', terms', Inttab.update (i, t) values')) end)
   3.158 -
   3.159 -fun get_term n (cx as (_, terms, _)) = (the (Symtab.lookup terms n), cx)
   3.160 +      let val t = Var (("fresh", next_val), T)
   3.161 +      in ((t, []), (Symtab.update (n, t) terms, next_val + 1)) end)
   3.162  
   3.163  fun trans_expr _ True = pair @{const True}
   3.164    | trans_expr _ False = pair @{const False}
   3.165 @@ -188,18 +122,16 @@
   3.166    | trans_expr T (Number (i, SOME j)) =
   3.167        pair (Const (@{const_name divide}, [T, T] ---> T) $
   3.168          HOLogic.mk_number T i $ HOLogic.mk_number T j)
   3.169 -  | trans_expr T (Value i) = term_of_value T i
   3.170 +  | trans_expr T (Value i) = pair (Var (("value", i), T))
   3.171    | trans_expr T (Array a) = trans_array T a
   3.172 -  | trans_expr _ (App (n, es)) =
   3.173 -      let val get_Ts = take (length es) o Term.binder_types o Term.fastype_of
   3.174 +  | trans_expr T (App (n, es)) = get_term n T es #-> (fn (t, es') =>
   3.175 +      let val Ts = fst (U.dest_funT (length es') (Term.fastype_of t))
   3.176        in
   3.177 -        get_term n #-> (fn t =>
   3.178 -        fold_map (uncurry trans_expr) (get_Ts t ~~ es) #>>
   3.179 -        Term.list_comb o pair t)
   3.180 -      end
   3.181 +        fold_map (uncurry trans_expr) (Ts ~~ es') #>> Term.list_comb o pair t
   3.182 +      end)
   3.183  
   3.184  and trans_array T a =
   3.185 -  let val dT = Term.domain_type T and rT = Term.range_type T
   3.186 +  let val (dT, rT) = U.split_type T
   3.187    in
   3.188      (case a of
   3.189        Fresh e => trans_expr rT e #>> (fn t => Abs ("x", dT, t))
   3.190 @@ -232,35 +164,131 @@
   3.191  fun mk_lambda Ts (t, pats) =
   3.192    fold_rev (curry Term.absdummy) Ts t |> fold mk_update pats
   3.193  
   3.194 -fun translate' T i [([], e)] =
   3.195 -      if i = 0 then trans_expr T e
   3.196 -      else 
   3.197 -        let val ((Us1, Us2), U) = Term.strip_type T |>> chop i
   3.198 -        in trans_expr (Us2 ---> U) e #>> mk_lambda Us1 o rpair [] end
   3.199 -  | translate' T i cases =
   3.200 -      let
   3.201 -        val (pat_cases, def) = split_last cases |> apsnd snd
   3.202 -        val ((Us1, Us2), U) = Term.strip_type T |>> chop i
   3.203 -      in
   3.204 -        trans_expr (Us2 ---> U) def ##>>
   3.205 -        fold_map (trans_pattern T) pat_cases #>>
   3.206 -        mk_lambda Us1
   3.207 -      end
   3.208 +fun translate ((t, k), (e, cs)) =
   3.209 +  let
   3.210 +    val T = Term.fastype_of t
   3.211 +    val (Us, U) = U.dest_funT k (Term.fastype_of t)
   3.212 +
   3.213 +    fun mk_full_def u' pats =
   3.214 +      pats
   3.215 +      |> filter_out (fn (_, u) => u aconv u')
   3.216 +      |> HOLogic.mk_eq o pair t o mk_lambda Us o pair u'
   3.217 +
   3.218 +    fun mk_eq (us, u) = HOLogic.mk_eq (Term.list_comb (t, us), u)
   3.219 +    fun mk_eqs u' [] = [HOLogic.mk_eq (t, u')]
   3.220 +      | mk_eqs _ pats = map mk_eq pats
   3.221 +  in
   3.222 +    trans_expr U e ##>>
   3.223 +    (if k = 0 then pair [] else fold_map (trans_pattern T) cs) #>>
   3.224 +    (fn (u', pats) => (mk_eqs u' pats, mk_full_def u' pats))
   3.225 +  end
   3.226 +
   3.227 +
   3.228 +(* normalization *)
   3.229 +
   3.230 +fun partition_eqs f =
   3.231 +  let
   3.232 +    fun part t (xs, ts) =
   3.233 +      (case try HOLogic.dest_eq t of
   3.234 +        SOME (l, r) => (case f l r of SOME x => (x::xs, ts) | _ => (xs, t::ts))
   3.235 +      | NONE => (xs, t :: ts))
   3.236 +  in (fn ts => fold part ts ([], [])) end
   3.237 +
   3.238 +fun replace_vars tab =
   3.239 +  let
   3.240 +    fun replace (v as Var _) = the_default v (AList.lookup (op aconv) tab v)
   3.241 +      | replace t = t
   3.242 +  in map (Term.map_aterms replace) end
   3.243 +
   3.244 +fun remove_int_nat_coercions (eqs, defs) =
   3.245 +  let
   3.246 +    fun mk_nat_num t i =
   3.247 +      (case try HOLogic.dest_number i of
   3.248 +        SOME (_, n) => SOME (t, HOLogic.mk_number @{typ nat} n)
   3.249 +      | NONE => NONE)
   3.250 +    fun nat_of (@{const of_nat (int)} $ (t as Var _)) i = mk_nat_num t i
   3.251 +      | nat_of (@{const nat} $ i) (t as Var _) = mk_nat_num t i
   3.252 +      | nat_of _ _ = NONE
   3.253 +    val (nats, eqs') = partition_eqs nat_of eqs
   3.254  
   3.255 -fun translate ((t, i), cases) =
   3.256 -  translate' (Term.fastype_of t) i cases #>> HOLogic.mk_eq o pair t
   3.257 +    fun is_coercion t =
   3.258 +      (case try HOLogic.dest_eq t of
   3.259 +        SOME (@{const of_nat (int)}, _) => true
   3.260 +      | SOME (@{const nat}, _) => true
   3.261 +      | _ => false)
   3.262 +  in pairself (replace_vars nats) (eqs', filter_out is_coercion defs) end
   3.263 +
   3.264 +fun unfold_funapp (eqs, defs) =
   3.265 +  let
   3.266 +    fun unfold_app (Const (@{const_name SMT.fun_app}, _) $ f $ t) = f $ t
   3.267 +      | unfold_app t = t
   3.268 +    fun unfold_eq ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) =
   3.269 +          eq $ unfold_app t $ u
   3.270 +      | unfold_eq t = t
   3.271 +
   3.272 +    fun is_fun_app t =
   3.273 +      (case try HOLogic.dest_eq t of
   3.274 +        SOME (Const (@{const_name SMT.fun_app}, _), _) => true
   3.275 +      | _ => false)
   3.276 +
   3.277 +  in (map unfold_eq eqs, filter_out is_fun_app defs) end
   3.278 +
   3.279 +fun unfold_simple_eqs (eqs, defs) =
   3.280 +  let
   3.281 +    fun add_rewr (l as Const _) (r as Var _) = SOME (r, l)
   3.282 +      | add_rewr (l as Free _) (r as Var _) = SOME (r, l)
   3.283 +      | add_rewr _ _ = NONE
   3.284 +    val (rs, eqs') = partition_eqs add_rewr eqs
   3.285 +
   3.286 +    fun is_trivial (Const (@{const_name HOL.eq}, _) $ t $ u) = t aconv u
   3.287 +      | is_trivial _ = false
   3.288 +  in pairself (replace_vars rs #> filter_out is_trivial) (eqs', defs) end
   3.289 +
   3.290 +fun swap_free ((eq as Const (@{const_name HOL.eq}, _)) $ t $ (u as Free _)) =
   3.291 +      eq $ u $ t
   3.292 +  | swap_free t = t
   3.293 +
   3.294 +fun frees_for_vars ctxt (eqs, defs) =
   3.295 +  let
   3.296 +    fun fresh_free i T (cx as (frees, ctxt)) =
   3.297 +      (case Inttab.lookup frees i of
   3.298 +        SOME t => (t, cx)
   3.299 +      | NONE =>
   3.300 +          let
   3.301 +            val (n, ctxt') = yield_singleton Variable.variant_fixes "" ctxt
   3.302 +            val t = Free (n, T)
   3.303 +          in (t, (Inttab.update (i, t) frees, ctxt')) end)
   3.304 +
   3.305 +    fun repl_var (Var ((_, i), T)) = fresh_free i T
   3.306 +      | repl_var (t $ u) = repl_var t ##>> repl_var u #>> op $
   3.307 +      | repl_var (Abs (n, T, t)) = repl_var t #>> (fn t' => Abs (n, T, t'))
   3.308 +      | repl_var t = pair t
   3.309 +  in
   3.310 +    (Inttab.empty, ctxt)
   3.311 +    |> fold_map repl_var eqs
   3.312 +    ||>> fold_map repl_var defs
   3.313 +    |> fst
   3.314 +  end
   3.315  
   3.316  
   3.317  (* overall procedure *)
   3.318  
   3.319 +val is_free_constraint = Term.exists_subterm (fn Free _ => true | _ => false)
   3.320 +
   3.321 +fun is_const_def (Const (@{const_name HOL.eq}, _) $ Const _ $ _) = true
   3.322 +  | is_const_def _ = false
   3.323 +
   3.324  fun parse_counterex ctxt ({terms, ...} : SMT_Translate.recon) ls =
   3.325 -  read_cex ls
   3.326 -  |> map_filter reduce_function
   3.327 -  |> drop_skolem_constants terms
   3.328 -  |> substitute_constants terms
   3.329 -  |> remove_int_nat_coercions terms
   3.330 -  |> filter_valid_valuations terms
   3.331 -  |> with_context ctxt terms translate
   3.332 +  read_cex terms ls
   3.333 +  |> with_context terms translate
   3.334 +  |> apfst flat o split_list
   3.335 +  |> remove_int_nat_coercions
   3.336 +  |> unfold_funapp
   3.337 +  |> unfold_simple_eqs
   3.338 +  |>> map swap_free
   3.339 +  |>> filter is_free_constraint
   3.340 +  |> frees_for_vars ctxt
   3.341 +  ||> filter is_const_def
   3.342  
   3.343  end
   3.344  
     4.1 --- a/src/HOL/Word/Word.thy	Tue Nov 30 15:56:19 2010 -0800
     4.2 +++ b/src/HOL/Word/Word.thy	Tue Nov 30 20:02:01 2010 -0800
     4.3 @@ -184,13 +184,13 @@
     4.4    "word_pred a = word_of_int (Int.pred (uint a))"
     4.5  
     4.6  definition udvd :: "'a::len word => 'a::len word => bool" (infixl "udvd" 50) where
     4.7 -  "a udvd b == EX n>=0. uint b = n * uint a"
     4.8 +  "a udvd b = (EX n>=0. uint b = n * uint a)"
     4.9  
    4.10  definition word_sle :: "'a :: len word => 'a word => bool" ("(_/ <=s _)" [50, 51] 50) where
    4.11 -  "a <=s b == sint a <= sint b"
    4.12 +  "a <=s b = (sint a <= sint b)"
    4.13  
    4.14  definition word_sless :: "'a :: len word => 'a word => bool" ("(_/ <s _)" [50, 51] 50) where
    4.15 -  "(x <s y) == (x <=s y & x ~= y)"
    4.16 +  "(x <s y) = (x <=s y & x ~= y)"
    4.17  
    4.18  
    4.19  
    4.20 @@ -245,76 +245,76 @@
    4.21    by (simp only: word_msb_def Min_def)
    4.22  
    4.23  definition setBit :: "'a :: len0 word => nat => 'a word" where 
    4.24 -  "setBit w n == set_bit w n True"
    4.25 +  "setBit w n = set_bit w n True"
    4.26  
    4.27  definition clearBit :: "'a :: len0 word => nat => 'a word" where
    4.28 -  "clearBit w n == set_bit w n False"
    4.29 +  "clearBit w n = set_bit w n False"
    4.30  
    4.31  
    4.32  subsection "Shift operations"
    4.33  
    4.34  definition sshiftr1 :: "'a :: len word => 'a word" where 
    4.35 -  "sshiftr1 w == word_of_int (bin_rest (sint w))"
    4.36 +  "sshiftr1 w = word_of_int (bin_rest (sint w))"
    4.37  
    4.38  definition bshiftr1 :: "bool => 'a :: len word => 'a word" where
    4.39 -  "bshiftr1 b w == of_bl (b # butlast (to_bl w))"
    4.40 +  "bshiftr1 b w = of_bl (b # butlast (to_bl w))"
    4.41  
    4.42  definition sshiftr :: "'a :: len word => nat => 'a word" (infixl ">>>" 55) where
    4.43 -  "w >>> n == (sshiftr1 ^^ n) w"
    4.44 +  "w >>> n = (sshiftr1 ^^ n) w"
    4.45  
    4.46  definition mask :: "nat => 'a::len word" where
    4.47 -  "mask n == (1 << n) - 1"
    4.48 +  "mask n = (1 << n) - 1"
    4.49  
    4.50  definition revcast :: "'a :: len0 word => 'b :: len0 word" where
    4.51 -  "revcast w ==  of_bl (takefill False (len_of TYPE('b)) (to_bl w))"
    4.52 +  "revcast w =  of_bl (takefill False (len_of TYPE('b)) (to_bl w))"
    4.53  
    4.54  definition slice1 :: "nat => 'a :: len0 word => 'b :: len0 word" where
    4.55 -  "slice1 n w == of_bl (takefill False n (to_bl w))"
    4.56 +  "slice1 n w = of_bl (takefill False n (to_bl w))"
    4.57  
    4.58  definition slice :: "nat => 'a :: len0 word => 'b :: len0 word" where
    4.59 -  "slice n w == slice1 (size w - n) w"
    4.60 +  "slice n w = slice1 (size w - n) w"
    4.61  
    4.62  
    4.63  subsection "Rotation"
    4.64  
    4.65  definition rotater1 :: "'a list => 'a list" where
    4.66 -  "rotater1 ys == 
    4.67 -    case ys of [] => [] | x # xs => last ys # butlast ys"
    4.68 +  "rotater1 ys = 
    4.69 +    (case ys of [] => [] | x # xs => last ys # butlast ys)"
    4.70  
    4.71  definition rotater :: "nat => 'a list => 'a list" where
    4.72 -  "rotater n == rotater1 ^^ n"
    4.73 +  "rotater n = rotater1 ^^ n"
    4.74  
    4.75  definition word_rotr :: "nat => 'a :: len0 word => 'a :: len0 word" where
    4.76 -  "word_rotr n w == of_bl (rotater n (to_bl w))"
    4.77 +  "word_rotr n w = of_bl (rotater n (to_bl w))"
    4.78  
    4.79  definition word_rotl :: "nat => 'a :: len0 word => 'a :: len0 word" where
    4.80 -  "word_rotl n w == of_bl (rotate n (to_bl w))"
    4.81 +  "word_rotl n w = of_bl (rotate n (to_bl w))"
    4.82  
    4.83  definition word_roti :: "int => 'a :: len0 word => 'a :: len0 word" where
    4.84 -  "word_roti i w == if i >= 0 then word_rotr (nat i) w
    4.85 -                    else word_rotl (nat (- i)) w"
    4.86 +  "word_roti i w = (if i >= 0 then word_rotr (nat i) w
    4.87 +                    else word_rotl (nat (- i)) w)"
    4.88  
    4.89  
    4.90  subsection "Split and cat operations"
    4.91  
    4.92  definition word_cat :: "'a :: len0 word => 'b :: len0 word => 'c :: len0 word" where
    4.93 -  "word_cat a b == word_of_int (bin_cat (uint a) (len_of TYPE ('b)) (uint b))"
    4.94 +  "word_cat a b = word_of_int (bin_cat (uint a) (len_of TYPE ('b)) (uint b))"
    4.95  
    4.96  definition word_split :: "'a :: len0 word => ('b :: len0 word) * ('c :: len0 word)" where
    4.97 -  "word_split a == 
    4.98 -   case bin_split (len_of TYPE ('c)) (uint a) of 
    4.99 -     (u, v) => (word_of_int u, word_of_int v)"
   4.100 +  "word_split a = 
   4.101 +   (case bin_split (len_of TYPE ('c)) (uint a) of 
   4.102 +     (u, v) => (word_of_int u, word_of_int v))"
   4.103  
   4.104  definition word_rcat :: "'a :: len0 word list => 'b :: len0 word" where
   4.105 -  "word_rcat ws == 
   4.106 +  "word_rcat ws = 
   4.107    word_of_int (bin_rcat (len_of TYPE ('a)) (map uint ws))"
   4.108  
   4.109  definition word_rsplit :: "'a :: len0 word => 'b :: len word list" where
   4.110 -  "word_rsplit w == 
   4.111 +  "word_rsplit w = 
   4.112    map word_of_int (bin_rsplit (len_of TYPE ('b)) (len_of TYPE ('a), uint w))"
   4.113  
   4.114  definition max_word :: "'a::len word" -- "Largest representable machine integer." where
   4.115 -  "max_word \<equiv> word_of_int (2 ^ len_of TYPE('a) - 1)"
   4.116 +  "max_word = word_of_int (2 ^ len_of TYPE('a) - 1)"
   4.117  
   4.118  primrec of_bool :: "bool \<Rightarrow> 'a::len word" where
   4.119    "of_bool False = 0"
   4.120 @@ -337,7 +337,7 @@
   4.121  lemmas atLeastLessThan_alt = atLeastLessThan_def [unfolded 
   4.122    atLeast_def lessThan_def Collect_conj_eq [symmetric]]
   4.123    
   4.124 -lemma mod_in_reps: "m > 0 ==> y mod m : {0::int ..< m}"
   4.125 +lemma mod_in_reps: "m > 0 \<Longrightarrow> y mod m : {0::int ..< m}"
   4.126    unfolding atLeastLessThan_alt by auto
   4.127  
   4.128  lemma 
   4.129 @@ -390,7 +390,7 @@
   4.130    unfolding sint_uint by (auto simp: bintrunc_sbintrunc_le)
   4.131  
   4.132  lemma bintr_uint': 
   4.133 -  "n >= size w ==> bintrunc n (uint w) = uint w"
   4.134 +  "n >= size w \<Longrightarrow> bintrunc n (uint w) = uint w"
   4.135    apply (unfold word_size)
   4.136    apply (subst word_ubin.norm_Rep [symmetric]) 
   4.137    apply (simp only: bintrunc_bintrunc_min word_size)
   4.138 @@ -398,7 +398,7 @@
   4.139    done
   4.140  
   4.141  lemma wi_bintr': 
   4.142 -  "wb = word_of_int bin ==> n >= size wb ==> 
   4.143 +  "wb = word_of_int bin \<Longrightarrow> n >= size wb \<Longrightarrow> 
   4.144      word_of_int (bintrunc n bin) = wb"
   4.145    unfolding word_size
   4.146    by (clarsimp simp add: word_ubin.norm_eq_iff [symmetric] min_max.inf_absorb1)
   4.147 @@ -446,8 +446,9 @@
   4.148  
   4.149  lemmas td_sint = word_sint.td
   4.150  
   4.151 -lemma word_number_of_alt: "number_of b == word_of_int (number_of b)"
   4.152 -  unfolding word_number_of_def by (simp add: number_of_eq)
   4.153 +lemma word_number_of_alt [code_unfold_post]:
   4.154 +  "number_of b = word_of_int (number_of b)"
   4.155 +  by (simp add: number_of_eq word_number_of_def)
   4.156  
   4.157  lemma word_no_wi: "number_of = word_of_int"
   4.158    by (auto simp: word_number_of_def intro: ext)
   4.159 @@ -483,7 +484,7 @@
   4.160    sint_sbintrunc [simp] 
   4.161    unat_bintrunc [simp]
   4.162  
   4.163 -lemma size_0_eq: "size (w :: 'a :: len0 word) = 0 ==> v = w"
   4.164 +lemma size_0_eq: "size (w :: 'a :: len0 word) = 0 \<Longrightarrow> v = w"
   4.165    apply (unfold word_size)
   4.166    apply (rule word_uint.Rep_eqD)
   4.167    apply (rule box_equals)
   4.168 @@ -508,13 +509,13 @@
   4.169    iffD2 [OF linorder_not_le uint_m2p_neg, standard]
   4.170  
   4.171  lemma lt2p_lem:
   4.172 -  "len_of TYPE('a) <= n ==> uint (w :: 'a :: len0 word) < 2 ^ n"
   4.173 +  "len_of TYPE('a) <= n \<Longrightarrow> uint (w :: 'a :: len0 word) < 2 ^ n"
   4.174    by (rule xtr8 [OF _ uint_lt2p]) simp
   4.175  
   4.176  lemmas uint_le_0_iff [simp] = 
   4.177    uint_ge_0 [THEN leD, THEN linorder_antisym_conv1, standard]
   4.178  
   4.179 -lemma uint_nat: "uint w == int (unat w)"
   4.180 +lemma uint_nat: "uint w = int (unat w)"
   4.181    unfolding unat_def by auto
   4.182  
   4.183  lemma uint_number_of:
   4.184 @@ -523,7 +524,7 @@
   4.185    by (simp only: int_word_uint)
   4.186  
   4.187  lemma unat_number_of: 
   4.188 -  "bin_sign b = Int.Pls ==> 
   4.189 +  "bin_sign b = Int.Pls \<Longrightarrow> 
   4.190    unat (number_of b::'a::len0 word) = number_of b mod 2 ^ len_of TYPE ('a)"
   4.191    apply (unfold unat_def)
   4.192    apply (clarsimp simp only: uint_number_of)
   4.193 @@ -590,7 +591,7 @@
   4.194  
   4.195  lemma word_eqI [rule_format] : 
   4.196    fixes u :: "'a::len0 word"
   4.197 -  shows "(ALL n. n < size u --> u !! n = v !! n) ==> u = v"
   4.198 +  shows "(ALL n. n < size u --> u !! n = v !! n) \<Longrightarrow> u = v"
   4.199    apply (rule test_bit_eq_iff [THEN iffD1])
   4.200    apply (rule ext)
   4.201    apply (erule allE)
   4.202 @@ -645,7 +646,7 @@
   4.203                    "{bl. length bl = len_of TYPE('a::len0)}"
   4.204    by (rule td_bl)
   4.205  
   4.206 -lemma word_size_bl: "size w == size (to_bl w)"
   4.207 +lemma word_size_bl: "size w = size (to_bl w)"
   4.208    unfolding word_size by auto
   4.209  
   4.210  lemma to_bl_use_of_bl:
   4.211 @@ -658,7 +659,7 @@
   4.212  lemma word_rev_rev [simp] : "word_reverse (word_reverse w) = w"
   4.213    unfolding word_reverse_def by (simp add : word_bl.Abs_inverse)
   4.214  
   4.215 -lemma word_rev_gal: "word_reverse w = u ==> word_reverse u = w"
   4.216 +lemma word_rev_gal: "word_reverse w = u \<Longrightarrow> word_reverse u = w"
   4.217    by auto
   4.218  
   4.219  lemmas word_rev_gal' = sym [THEN word_rev_gal, symmetric, standard]
   4.220 @@ -675,7 +676,7 @@
   4.221    done
   4.222  
   4.223  lemma of_bl_drop': 
   4.224 -  "lend = length bl - len_of TYPE ('a :: len0) ==> 
   4.225 +  "lend = length bl - len_of TYPE ('a :: len0) \<Longrightarrow> 
   4.226      of_bl (drop lend bl) = (of_bl bl :: 'a word)"
   4.227    apply (unfold of_bl_def)
   4.228    apply (clarsimp simp add : trunc_bl2bin [symmetric])
   4.229 @@ -693,7 +694,7 @@
   4.230    "(number_of bin ::'a::len0 word) = of_bl (bin_to_bl (len_of TYPE ('a)) bin)"
   4.231    unfolding word_size of_bl_no by (simp add : word_number_of_def)
   4.232  
   4.233 -lemma uint_bl: "to_bl w == bin_to_bl (size w) (uint w)"
   4.234 +lemma uint_bl: "to_bl w = bin_to_bl (size w) (uint w)"
   4.235    unfolding word_size to_bl_def by auto
   4.236  
   4.237  lemma to_bl_bin: "bl_to_bin (to_bl w) = uint w"
   4.238 @@ -742,14 +743,14 @@
   4.239    may want these in reverse, but loop as simp rules, so use following *)
   4.240  
   4.241  lemma num_of_bintr':
   4.242 -  "bintrunc (len_of TYPE('a :: len0)) a = b ==> 
   4.243 +  "bintrunc (len_of TYPE('a :: len0)) a = b \<Longrightarrow> 
   4.244      number_of a = (number_of b :: 'a word)"
   4.245    apply safe
   4.246    apply (rule_tac num_of_bintr [symmetric])
   4.247    done
   4.248  
   4.249  lemma num_of_sbintr':
   4.250 -  "sbintrunc (len_of TYPE('a :: len) - 1) a = b ==> 
   4.251 +  "sbintrunc (len_of TYPE('a :: len) - 1) a = b \<Longrightarrow> 
   4.252      number_of a = (number_of b :: 'a word)"
   4.253    apply safe
   4.254    apply (rule_tac num_of_sbintr [symmetric])
   4.255 @@ -769,7 +770,7 @@
   4.256  lemma scast_id: "scast w = w"
   4.257    unfolding scast_def by auto
   4.258  
   4.259 -lemma ucast_bl: "ucast w == of_bl (to_bl w)"
   4.260 +lemma ucast_bl: "ucast w = of_bl (to_bl w)"
   4.261    unfolding ucast_def of_bl_def uint_bl
   4.262    by (auto simp add : word_size)
   4.263  
   4.264 @@ -799,7 +800,7 @@
   4.265  
   4.266  lemmas is_up_down =  trans [OF is_up is_down [symmetric], standard]
   4.267  
   4.268 -lemma down_cast_same': "uc = ucast ==> is_down uc ==> uc = scast"
   4.269 +lemma down_cast_same': "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc = scast"
   4.270    apply (unfold is_down)
   4.271    apply safe
   4.272    apply (rule ext)
   4.273 @@ -809,7 +810,7 @@
   4.274    done
   4.275  
   4.276  lemma word_rev_tf': 
   4.277 -  "r = to_bl (of_bl bl) ==> r = rev (takefill False (length r) (rev bl))"
   4.278 +  "r = to_bl (of_bl bl) \<Longrightarrow> r = rev (takefill False (length r) (rev bl))"
   4.279    unfolding of_bl_def uint_bl
   4.280    by (clarsimp simp add: bl_bin_bl_rtf word_ubin.eq_norm word_size)
   4.281  
   4.282 @@ -829,17 +830,17 @@
   4.283    done
   4.284  
   4.285  lemma ucast_up_app': 
   4.286 -  "uc = ucast ==> source_size uc + n = target_size uc ==> 
   4.287 +  "uc = ucast \<Longrightarrow> source_size uc + n = target_size uc \<Longrightarrow> 
   4.288      to_bl (uc w) = replicate n False @ (to_bl w)"
   4.289    by (auto simp add : source_size target_size to_bl_ucast)
   4.290  
   4.291  lemma ucast_down_drop': 
   4.292 -  "uc = ucast ==> source_size uc = target_size uc + n ==> 
   4.293 +  "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow> 
   4.294      to_bl (uc w) = drop n (to_bl w)"
   4.295    by (auto simp add : source_size target_size to_bl_ucast)
   4.296  
   4.297  lemma scast_down_drop': 
   4.298 -  "sc = scast ==> source_size sc = target_size sc + n ==> 
   4.299 +  "sc = scast \<Longrightarrow> source_size sc = target_size sc + n \<Longrightarrow> 
   4.300      to_bl (sc w) = drop n (to_bl w)"
   4.301    apply (subgoal_tac "sc = ucast")
   4.302     apply safe
   4.303 @@ -850,7 +851,7 @@
   4.304    done
   4.305  
   4.306  lemma sint_up_scast': 
   4.307 -  "sc = scast ==> is_up sc ==> sint (sc w) = sint w"
   4.308 +  "sc = scast \<Longrightarrow> is_up sc \<Longrightarrow> sint (sc w) = sint w"
   4.309    apply (unfold is_up)
   4.310    apply safe
   4.311    apply (simp add: scast_def word_sbin.eq_norm)
   4.312 @@ -865,7 +866,7 @@
   4.313    done
   4.314  
   4.315  lemma uint_up_ucast':
   4.316 -  "uc = ucast ==> is_up uc ==> uint (uc w) = uint w"
   4.317 +  "uc = ucast \<Longrightarrow> is_up uc \<Longrightarrow> uint (uc w) = uint w"
   4.318    apply (unfold is_up)
   4.319    apply safe
   4.320    apply (rule bin_eqI)
   4.321 @@ -881,18 +882,18 @@
   4.322  lemmas uint_up_ucast = refl [THEN uint_up_ucast']
   4.323  lemmas sint_up_scast = refl [THEN sint_up_scast']
   4.324  
   4.325 -lemma ucast_up_ucast': "uc = ucast ==> is_up uc ==> ucast (uc w) = ucast w"
   4.326 +lemma ucast_up_ucast': "uc = ucast \<Longrightarrow> is_up uc \<Longrightarrow> ucast (uc w) = ucast w"
   4.327    apply (simp (no_asm) add: ucast_def)
   4.328    apply (clarsimp simp add: uint_up_ucast)
   4.329    done
   4.330      
   4.331 -lemma scast_up_scast': "sc = scast ==> is_up sc ==> scast (sc w) = scast w"
   4.332 +lemma scast_up_scast': "sc = scast \<Longrightarrow> is_up sc \<Longrightarrow> scast (sc w) = scast w"
   4.333    apply (simp (no_asm) add: scast_def)
   4.334    apply (clarsimp simp add: sint_up_scast)
   4.335    done
   4.336      
   4.337  lemma ucast_of_bl_up': 
   4.338 -  "w = of_bl bl ==> size bl <= size w ==> ucast w = of_bl bl"
   4.339 +  "w = of_bl bl \<Longrightarrow> size bl <= size w \<Longrightarrow> ucast w = of_bl bl"
   4.340    by (auto simp add : nth_ucast word_size test_bit_of_bl intro!: word_eqI)
   4.341  
   4.342  lemmas ucast_up_ucast = refl [THEN ucast_up_ucast']
   4.343 @@ -908,22 +909,22 @@
   4.344  lemmas scast_down_scast_id = isdus [THEN ucast_up_ucast_id]
   4.345  
   4.346  lemma up_ucast_surj:
   4.347 -  "is_up (ucast :: 'b::len0 word => 'a::len0 word) ==> 
   4.348 +  "is_up (ucast :: 'b::len0 word => 'a::len0 word) \<Longrightarrow> 
   4.349     surj (ucast :: 'a word => 'b word)"
   4.350    by (rule surjI, erule ucast_up_ucast_id)
   4.351  
   4.352  lemma up_scast_surj:
   4.353 -  "is_up (scast :: 'b::len word => 'a::len word) ==> 
   4.354 +  "is_up (scast :: 'b::len word => 'a::len word) \<Longrightarrow> 
   4.355     surj (scast :: 'a word => 'b word)"
   4.356    by (rule surjI, erule scast_up_scast_id)
   4.357  
   4.358  lemma down_scast_inj:
   4.359 -  "is_down (scast :: 'b::len word => 'a::len word) ==> 
   4.360 +  "is_down (scast :: 'b::len word => 'a::len word) \<Longrightarrow> 
   4.361     inj_on (ucast :: 'a word => 'b word) A"
   4.362    by (rule inj_on_inverseI, erule scast_down_scast_id)
   4.363  
   4.364  lemma down_ucast_inj:
   4.365 -  "is_down (ucast :: 'b::len0 word => 'a::len0 word) ==> 
   4.366 +  "is_down (ucast :: 'b::len0 word => 'a::len0 word) \<Longrightarrow> 
   4.367     inj_on (ucast :: 'a word => 'b word) A"
   4.368    by (rule inj_on_inverseI, erule ucast_down_ucast_id)
   4.369  
   4.370 @@ -931,7 +932,7 @@
   4.371    by (rule word_bl.Rep_eqD) (simp add: word_rep_drop)
   4.372    
   4.373  lemma ucast_down_no': 
   4.374 -  "uc = ucast ==> is_down uc ==> uc (number_of bin) = number_of bin"
   4.375 +  "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (number_of bin) = number_of bin"
   4.376    apply (unfold word_number_of_def is_down)
   4.377    apply (clarsimp simp add: ucast_def word_ubin.eq_norm)
   4.378    apply (rule word_ubin.norm_eq_iff [THEN iffD1])
   4.379 @@ -940,7 +941,7 @@
   4.380      
   4.381  lemmas ucast_down_no = ucast_down_no' [OF refl]
   4.382  
   4.383 -lemma ucast_down_bl': "uc = ucast ==> is_down uc ==> uc (of_bl bl) = of_bl bl"
   4.384 +lemma ucast_down_bl': "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (of_bl bl) = of_bl bl"
   4.385    unfolding of_bl_no by clarify (erule ucast_down_no)
   4.386      
   4.387  lemmas ucast_down_bl = ucast_down_bl' [OF refl]
   4.388 @@ -984,7 +985,7 @@
   4.389    word_succ_def word_pred_def word_0_wi word_1_wi
   4.390  
   4.391  lemma udvdI: 
   4.392 -  "0 \<le> n ==> uint b = n * uint a ==> a udvd b"
   4.393 +  "0 \<le> n \<Longrightarrow> uint b = n * uint a \<Longrightarrow> a udvd b"
   4.394    by (auto simp: udvd_def)
   4.395  
   4.396  lemmas word_div_no [simp] = 
   4.397 @@ -1015,14 +1016,14 @@
   4.398  lemmas word_0_wi_Pls = word_0_wi [folded Pls_def]
   4.399  lemmas word_0_no = word_0_wi_Pls [folded word_no_wi]
   4.400  
   4.401 -lemma int_one_bin: "(1 :: int) == (Int.Pls BIT 1)"
   4.402 +lemma int_one_bin: "(1 :: int) = (Int.Pls BIT 1)"
   4.403    unfolding Pls_def Bit_def by auto
   4.404  
   4.405  lemma word_1_no: 
   4.406 -  "(1 :: 'a :: len0 word) == number_of (Int.Pls BIT 1)"
   4.407 +  "(1 :: 'a :: len0 word) = number_of (Int.Pls BIT 1)"
   4.408    unfolding word_1_wi word_number_of_def int_one_bin by auto
   4.409  
   4.410 -lemma word_m1_wi: "-1 == word_of_int -1" 
   4.411 +lemma word_m1_wi: "-1 = word_of_int -1" 
   4.412    by (rule word_number_of_alt)
   4.413  
   4.414  lemma word_m1_wi_Min: "-1 = word_of_int Int.Min"
   4.415 @@ -1056,7 +1057,7 @@
   4.416  lemma unat_0 [simp]: "unat 0 = 0"
   4.417    unfolding unat_def by auto
   4.418  
   4.419 -lemma size_0_same': "size w = 0 ==> w = (v :: 'a :: len0 word)"
   4.420 +lemma size_0_same': "size w = 0 \<Longrightarrow> w = (v :: 'a :: len0 word)"
   4.421    apply (unfold word_size)
   4.422    apply (rule box_equals)
   4.423      defer
   4.424 @@ -1129,11 +1130,11 @@
   4.425  
   4.426  lemmas wi_hom_syms = wi_homs [symmetric]
   4.427  
   4.428 -lemma word_sub_def: "a - b == a + - (b :: 'a :: len0 word)"
   4.429 +lemma word_sub_def: "a - b = a + - (b :: 'a :: len0 word)"
   4.430    unfolding word_sub_wi diff_minus
   4.431    by (simp only : word_uint.Rep_inverse wi_hom_syms)
   4.432      
   4.433 -lemmas word_diff_minus = word_sub_def [THEN meta_eq_to_obj_eq, standard]
   4.434 +lemmas word_diff_minus = word_sub_def [standard]
   4.435  
   4.436  lemma word_of_int_sub_hom:
   4.437    "(word_of_int a) - word_of_int b = word_of_int (a - b)"
   4.438 @@ -1265,13 +1266,13 @@
   4.439  
   4.440  subsection "Order on fixed-length words"
   4.441  
   4.442 -lemma word_order_trans: "x <= y ==> y <= z ==> x <= (z :: 'a :: len0 word)"
   4.443 +lemma word_order_trans: "x <= y \<Longrightarrow> y <= z \<Longrightarrow> x <= (z :: 'a :: len0 word)"
   4.444    unfolding word_le_def by auto
   4.445  
   4.446  lemma word_order_refl: "z <= (z :: 'a :: len0 word)"
   4.447    unfolding word_le_def by auto
   4.448  
   4.449 -lemma word_order_antisym: "x <= y ==> y <= x ==> x = (y :: 'a :: len0 word)"
   4.450 +lemma word_order_antisym: "x <= y \<Longrightarrow> y <= x \<Longrightarrow> x = (y :: 'a :: len0 word)"
   4.451    unfolding word_le_def by (auto intro!: word_uint.Rep_eqD)
   4.452  
   4.453  lemma word_order_linear:
   4.454 @@ -1307,7 +1308,7 @@
   4.455  
   4.456  lemmas word_gt_0_no [simp] = word_gt_0 [of "number_of y", standard]
   4.457  
   4.458 -lemma word_sless_alt: "(a <s b) == (sint a < sint b)"
   4.459 +lemma word_sless_alt: "(a <s b) = (sint a < sint b)"
   4.460    unfolding word_sle_def word_sless_def
   4.461    by (auto simp add: less_le)
   4.462  
   4.463 @@ -1347,7 +1348,7 @@
   4.464  
   4.465  lemmas unat_mono = word_less_nat_alt [THEN iffD1, standard]
   4.466  
   4.467 -lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) ==> (0 :: 'a word) ~= 1";
   4.468 +lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) \<Longrightarrow> (0 :: 'a word) ~= 1";
   4.469    unfolding word_arith_wis
   4.470    by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc)
   4.471  
   4.472 @@ -1356,7 +1357,7 @@
   4.473  lemma no_no [simp] : "number_of (number_of b) = number_of b"
   4.474    by (simp add: number_of_eq)
   4.475  
   4.476 -lemma unat_minus_one: "x ~= 0 ==> unat (x - 1) = unat x - 1"
   4.477 +lemma unat_minus_one: "x ~= 0 \<Longrightarrow> unat (x - 1) = unat x - 1"
   4.478    apply (unfold unat_def)
   4.479    apply (simp only: int_word_uint word_arith_alts rdmods)
   4.480    apply (subgoal_tac "uint x >= 1")
   4.481 @@ -1378,7 +1379,7 @@
   4.482    apply simp
   4.483    done
   4.484      
   4.485 -lemma measure_unat: "p ~= 0 ==> unat (p - 1) < unat p"
   4.486 +lemma measure_unat: "p ~= 0 \<Longrightarrow> unat (p - 1) < unat p"
   4.487    by (simp add: unat_minus_one) (simp add: unat_0_iff [symmetric])
   4.488    
   4.489  lemmas uint_add_ge0 [simp] =
   4.490 @@ -1423,7 +1424,7 @@
   4.491  subsection {* Definition of uint\_arith *}
   4.492  
   4.493  lemma word_of_int_inverse:
   4.494 -  "word_of_int r = a ==> 0 <= r ==> r < 2 ^ len_of TYPE('a) ==> 
   4.495 +  "word_of_int r = a \<Longrightarrow> 0 <= r \<Longrightarrow> r < 2 ^ len_of TYPE('a) \<Longrightarrow> 
   4.496     uint (a::'a::len0 word) = r"
   4.497    apply (erule word_uint.Abs_inverse' [rotated])
   4.498    apply (simp add: uints_num)
   4.499 @@ -1454,7 +1455,7 @@
   4.500    uint_sub_if' uint_plus_if'
   4.501  
   4.502  (* use this to stop, eg, 2 ^ len_of TYPE (32) being simplified *)
   4.503 -lemma power_False_cong: "False ==> a ^ b = c ^ d" 
   4.504 +lemma power_False_cong: "False \<Longrightarrow> a ^ b = c ^ d" 
   4.505    by auto
   4.506  
   4.507  (* uint_arith_tac: reduce to arithmetic on int, try to solve by arith *)
   4.508 @@ -1520,11 +1521,11 @@
   4.509  lemmas word_sub_le = word_sub_le_iff [THEN iffD2, standard]
   4.510  
   4.511  lemma word_less_sub1: 
   4.512 -  "(x :: 'a :: len word) ~= 0 ==> (1 < x) = (0 < x - 1)"
   4.513 +  "(x :: 'a :: len word) ~= 0 \<Longrightarrow> (1 < x) = (0 < x - 1)"
   4.514    by uint_arith
   4.515  
   4.516  lemma word_le_sub1: 
   4.517 -  "(x :: 'a :: len word) ~= 0 ==> (1 <= x) = (0 <= x - 1)"
   4.518 +  "(x :: 'a :: len word) ~= 0 \<Longrightarrow> (1 <= x) = (0 <= x - 1)"
   4.519    by uint_arith
   4.520  
   4.521  lemma sub_wrap_lt: 
   4.522 @@ -1536,19 +1537,19 @@
   4.523    by uint_arith
   4.524  
   4.525  lemma plus_minus_not_NULL_ab: 
   4.526 -  "(x :: 'a :: len0 word) <= ab - c ==> c <= ab ==> c ~= 0 ==> x + c ~= 0"
   4.527 +  "(x :: 'a :: len0 word) <= ab - c \<Longrightarrow> c <= ab \<Longrightarrow> c ~= 0 \<Longrightarrow> x + c ~= 0"
   4.528    by uint_arith
   4.529  
   4.530  lemma plus_minus_no_overflow_ab: 
   4.531 -  "(x :: 'a :: len0 word) <= ab - c ==> c <= ab ==> x <= x + c" 
   4.532 +  "(x :: 'a :: len0 word) <= ab - c \<Longrightarrow> c <= ab \<Longrightarrow> x <= x + c" 
   4.533    by uint_arith
   4.534  
   4.535  lemma le_minus': 
   4.536 -  "(a :: 'a :: len0 word) + c <= b ==> a <= a + c ==> c <= b - a"
   4.537 +  "(a :: 'a :: len0 word) + c <= b \<Longrightarrow> a <= a + c \<Longrightarrow> c <= b - a"
   4.538    by uint_arith
   4.539  
   4.540  lemma le_plus': 
   4.541 -  "(a :: 'a :: len0 word) <= b ==> c <= b - a ==> a + c <= b"
   4.542 +  "(a :: 'a :: len0 word) <= b \<Longrightarrow> c <= b - a \<Longrightarrow> a + c <= b"
   4.543    by uint_arith
   4.544  
   4.545  lemmas le_plus = le_plus' [rotated]
   4.546 @@ -1556,90 +1557,90 @@
   4.547  lemmas le_minus = leD [THEN thin_rl, THEN le_minus', standard]
   4.548  
   4.549  lemma word_plus_mono_right: 
   4.550 -  "(y :: 'a :: len0 word) <= z ==> x <= x + z ==> x + y <= x + z"
   4.551 +  "(y :: 'a :: len0 word) <= z \<Longrightarrow> x <= x + z \<Longrightarrow> x + y <= x + z"
   4.552    by uint_arith
   4.553  
   4.554  lemma word_less_minus_cancel: 
   4.555 -  "y - x < z - x ==> x <= z ==> (y :: 'a :: len0 word) < z"
   4.556 +  "y - x < z - x \<Longrightarrow> x <= z \<Longrightarrow> (y :: 'a :: len0 word) < z"
   4.557    by uint_arith
   4.558  
   4.559  lemma word_less_minus_mono_left: 
   4.560 -  "(y :: 'a :: len0 word) < z ==> x <= y ==> y - x < z - x"
   4.561 +  "(y :: 'a :: len0 word) < z \<Longrightarrow> x <= y \<Longrightarrow> y - x < z - x"
   4.562    by uint_arith
   4.563  
   4.564  lemma word_less_minus_mono:  
   4.565 -  "a < c ==> d < b ==> a - b < a ==> c - d < c 
   4.566 -  ==> a - b < c - (d::'a::len word)"
   4.567 +  "a < c \<Longrightarrow> d < b \<Longrightarrow> a - b < a \<Longrightarrow> c - d < c 
   4.568 +  \<Longrightarrow> a - b < c - (d::'a::len word)"
   4.569    by uint_arith
   4.570  
   4.571  lemma word_le_minus_cancel: 
   4.572 -  "y - x <= z - x ==> x <= z ==> (y :: 'a :: len0 word) <= z"
   4.573 +  "y - x <= z - x \<Longrightarrow> x <= z \<Longrightarrow> (y :: 'a :: len0 word) <= z"
   4.574    by uint_arith
   4.575  
   4.576  lemma word_le_minus_mono_left: 
   4.577 -  "(y :: 'a :: len0 word) <= z ==> x <= y ==> y - x <= z - x"
   4.578 +  "(y :: 'a :: len0 word) <= z \<Longrightarrow> x <= y \<Longrightarrow> y - x <= z - x"
   4.579    by uint_arith
   4.580  
   4.581  lemma word_le_minus_mono:  
   4.582 -  "a <= c ==> d <= b ==> a - b <= a ==> c - d <= c 
   4.583 -  ==> a - b <= c - (d::'a::len word)"
   4.584 +  "a <= c \<Longrightarrow> d <= b \<Longrightarrow> a - b <= a \<Longrightarrow> c - d <= c 
   4.585 +  \<Longrightarrow> a - b <= c - (d::'a::len word)"
   4.586    by uint_arith
   4.587  
   4.588  lemma plus_le_left_cancel_wrap: 
   4.589 -  "(x :: 'a :: len0 word) + y' < x ==> x + y < x ==> (x + y' < x + y) = (y' < y)"
   4.590 +  "(x :: 'a :: len0 word) + y' < x \<Longrightarrow> x + y < x \<Longrightarrow> (x + y' < x + y) = (y' < y)"
   4.591    by uint_arith
   4.592  
   4.593  lemma plus_le_left_cancel_nowrap: 
   4.594 -  "(x :: 'a :: len0 word) <= x + y' ==> x <= x + y ==> 
   4.595 +  "(x :: 'a :: len0 word) <= x + y' \<Longrightarrow> x <= x + y \<Longrightarrow> 
   4.596      (x + y' < x + y) = (y' < y)" 
   4.597    by uint_arith
   4.598  
   4.599  lemma word_plus_mono_right2: 
   4.600 -  "(a :: 'a :: len0 word) <= a + b ==> c <= b ==> a <= a + c"
   4.601 +  "(a :: 'a :: len0 word) <= a + b \<Longrightarrow> c <= b \<Longrightarrow> a <= a + c"
   4.602    by uint_arith
   4.603  
   4.604  lemma word_less_add_right: 
   4.605 -  "(x :: 'a :: len0 word) < y - z ==> z <= y ==> x + z < y"
   4.606 +  "(x :: 'a :: len0 word) < y - z \<Longrightarrow> z <= y \<Longrightarrow> x + z < y"
   4.607    by uint_arith
   4.608  
   4.609  lemma word_less_sub_right: 
   4.610 -  "(x :: 'a :: len0 word) < y + z ==> y <= x ==> x - y < z"
   4.611 +  "(x :: 'a :: len0 word) < y + z \<Longrightarrow> y <= x \<Longrightarrow> x - y < z"
   4.612    by uint_arith
   4.613  
   4.614  lemma word_le_plus_either: 
   4.615 -  "(x :: 'a :: len0 word) <= y | x <= z ==> y <= y + z ==> x <= y + z"
   4.616 +  "(x :: 'a :: len0 word) <= y | x <= z \<Longrightarrow> y <= y + z \<Longrightarrow> x <= y + z"
   4.617    by uint_arith
   4.618  
   4.619  lemma word_less_nowrapI: 
   4.620 -  "(x :: 'a :: len0 word) < z - k ==> k <= z ==> 0 < k ==> x < x + k"
   4.621 +  "(x :: 'a :: len0 word) < z - k \<Longrightarrow> k <= z \<Longrightarrow> 0 < k \<Longrightarrow> x < x + k"
   4.622    by uint_arith
   4.623  
   4.624 -lemma inc_le: "(i :: 'a :: len word) < m ==> i + 1 <= m"
   4.625 +lemma inc_le: "(i :: 'a :: len word) < m \<Longrightarrow> i + 1 <= m"
   4.626    by uint_arith
   4.627  
   4.628  lemma inc_i: 
   4.629 -  "(1 :: 'a :: len word) <= i ==> i < m ==> 1 <= (i + 1) & i + 1 <= m"
   4.630 +  "(1 :: 'a :: len word) <= i \<Longrightarrow> i < m \<Longrightarrow> 1 <= (i + 1) & i + 1 <= m"
   4.631    by uint_arith
   4.632  
   4.633  lemma udvd_incr_lem:
   4.634 -  "up < uq ==> up = ua + n * uint K ==> 
   4.635 -    uq = ua + n' * uint K ==> up + uint K <= uq"
   4.636 +  "up < uq \<Longrightarrow> up = ua + n * uint K \<Longrightarrow> 
   4.637 +    uq = ua + n' * uint K \<Longrightarrow> up + uint K <= uq"
   4.638    apply clarsimp
   4.639    apply (drule less_le_mult)
   4.640    apply safe
   4.641    done
   4.642  
   4.643  lemma udvd_incr': 
   4.644 -  "p < q ==> uint p = ua + n * uint K ==> 
   4.645 -    uint q = ua + n' * uint K ==> p + K <= q" 
   4.646 +  "p < q \<Longrightarrow> uint p = ua + n * uint K \<Longrightarrow> 
   4.647 +    uint q = ua + n' * uint K \<Longrightarrow> p + K <= q" 
   4.648    apply (unfold word_less_alt word_le_def)
   4.649    apply (drule (2) udvd_incr_lem)
   4.650    apply (erule uint_add_le [THEN order_trans])
   4.651    done
   4.652  
   4.653  lemma udvd_decr': 
   4.654 -  "p < q ==> uint p = ua + n * uint K ==> 
   4.655 -    uint q = ua + n' * uint K ==> p <= q - K"
   4.656 +  "p < q \<Longrightarrow> uint p = ua + n * uint K \<Longrightarrow> 
   4.657 +    uint q = ua + n' * uint K \<Longrightarrow> p <= q - K"
   4.658    apply (unfold word_less_alt word_le_def)
   4.659    apply (drule (2) udvd_incr_lem)
   4.660    apply (drule le_diff_eq [THEN iffD2])
   4.661 @@ -1652,7 +1653,7 @@
   4.662  lemmas udvd_decr0 = udvd_decr' [where ua=0, simplified]
   4.663  
   4.664  lemma udvd_minus_le': 
   4.665 -  "xy < k ==> z udvd xy ==> z udvd k ==> xy <= k - z"
   4.666 +  "xy < k \<Longrightarrow> z udvd xy \<Longrightarrow> z udvd k \<Longrightarrow> xy <= k - z"
   4.667    apply (unfold udvd_def)
   4.668    apply clarify
   4.669    apply (erule (2) udvd_decr0)
   4.670 @@ -1661,8 +1662,8 @@
   4.671  ML {* Delsimprocs Numeral_Simprocs.cancel_factors *}
   4.672  
   4.673  lemma udvd_incr2_K: 
   4.674 -  "p < a + s ==> a <= a + s ==> K udvd s ==> K udvd p - a ==> a <= p ==> 
   4.675 -    0 < K ==> p <= p + K & p + K <= a + s"
   4.676 +  "p < a + s \<Longrightarrow> a <= a + s \<Longrightarrow> K udvd s \<Longrightarrow> K udvd p - a \<Longrightarrow> a <= p \<Longrightarrow> 
   4.677 +    0 < K \<Longrightarrow> p <= p + K & p + K <= a + s"
   4.678    apply (unfold udvd_def)
   4.679    apply clarify
   4.680    apply (simp add: uint_arith_simps split: split_if_asm)
   4.681 @@ -1680,7 +1681,7 @@
   4.682  
   4.683  (* links with rbl operations *)
   4.684  lemma word_succ_rbl:
   4.685 -  "to_bl w = bl ==> to_bl (word_succ w) = (rev (rbl_succ (rev bl)))"
   4.686 +  "to_bl w = bl \<Longrightarrow> to_bl (word_succ w) = (rev (rbl_succ (rev bl)))"
   4.687    apply (unfold word_succ_def)
   4.688    apply clarify
   4.689    apply (simp add: to_bl_of_bin)
   4.690 @@ -1688,7 +1689,7 @@
   4.691    done
   4.692  
   4.693  lemma word_pred_rbl:
   4.694 -  "to_bl w = bl ==> to_bl (word_pred w) = (rev (rbl_pred (rev bl)))"
   4.695 +  "to_bl w = bl \<Longrightarrow> to_bl (word_pred w) = (rev (rbl_pred (rev bl)))"
   4.696    apply (unfold word_pred_def)
   4.697    apply clarify
   4.698    apply (simp add: to_bl_of_bin)
   4.699 @@ -1696,7 +1697,7 @@
   4.700    done
   4.701  
   4.702  lemma word_add_rbl:
   4.703 -  "to_bl v = vbl ==> to_bl w = wbl ==> 
   4.704 +  "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow> 
   4.705      to_bl (v + w) = (rev (rbl_add (rev vbl) (rev wbl)))"
   4.706    apply (unfold word_add_def)
   4.707    apply clarify
   4.708 @@ -1705,7 +1706,7 @@
   4.709    done
   4.710  
   4.711  lemma word_mult_rbl:
   4.712 -  "to_bl v = vbl ==> to_bl w = wbl ==> 
   4.713 +  "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow> 
   4.714      to_bl (v * w) = (rev (rbl_mult (rev vbl) (rev wbl)))"
   4.715    apply (unfold word_mult_def)
   4.716    apply clarify
   4.717 @@ -1715,14 +1716,9 @@
   4.718  
   4.719  lemma rtb_rbl_ariths:
   4.720    "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_succ w)) = rbl_succ ys"
   4.721 -
   4.722    "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_pred w)) = rbl_pred ys"
   4.723 -
   4.724 -  "[| rev (to_bl v) = ys; rev (to_bl w) = xs |] 
   4.725 -  ==> rev (to_bl (v * w)) = rbl_mult ys xs"
   4.726 -
   4.727 -  "[| rev (to_bl v) = ys; rev (to_bl w) = xs |] 
   4.728 -  ==> rev (to_bl (v + w)) = rbl_add ys xs"
   4.729 +  "rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v * w)) = rbl_mult ys xs"
   4.730 +  "rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v + w)) = rbl_add ys xs"
   4.731    by (auto simp: rev_swap [symmetric] word_succ_rbl 
   4.732                   word_pred_rbl word_mult_rbl word_add_rbl)
   4.733  
   4.734 @@ -1784,7 +1780,7 @@
   4.735    done
   4.736  
   4.737  lemma word_of_int_nat: 
   4.738 -  "0 <= x ==> word_of_int x = of_nat (nat x)"
   4.739 +  "0 <= x \<Longrightarrow> word_of_int x = of_nat (nat x)"
   4.740    by (simp add: of_nat_nat word_of_int)
   4.741  
   4.742  lemma word_number_of_eq: 
   4.743 @@ -1806,7 +1802,7 @@
   4.744  subsection "Word and nat"
   4.745  
   4.746  lemma td_ext_unat':
   4.747 -  "n = len_of TYPE ('a :: len) ==> 
   4.748 +  "n = len_of TYPE ('a :: len) \<Longrightarrow> 
   4.749      td_ext (unat :: 'a word => nat) of_nat 
   4.750      (unats n) (%i. i mod 2 ^ n)"
   4.751    apply (unfold td_ext_def' unat_def word_of_nat unats_uints)
   4.752 @@ -1829,7 +1825,7 @@
   4.753  
   4.754  lemmas unat_lt2p [iff] = word_unat.Rep [unfolded unats_def mem_Collect_eq]
   4.755  
   4.756 -lemma unat_le: "y <= unat (z :: 'a :: len word) ==> y : unats (len_of TYPE ('a))"
   4.757 +lemma unat_le: "y <= unat (z :: 'a :: len word) \<Longrightarrow> y : unats (len_of TYPE ('a))"
   4.758    apply (unfold unats_def)
   4.759    apply clarsimp
   4.760    apply (rule xtrans, rule unat_lt2p, assumption) 
   4.761 @@ -1864,11 +1860,11 @@
   4.762  
   4.763  lemmas of_nat_2p = mult_1 [symmetric, THEN iffD2 [OF of_nat_0 exI]]
   4.764  
   4.765 -lemma of_nat_gt_0: "of_nat k ~= 0 ==> 0 < k"
   4.766 +lemma of_nat_gt_0: "of_nat k ~= 0 \<Longrightarrow> 0 < k"
   4.767    by (cases k) auto
   4.768  
   4.769  lemma of_nat_neq_0: 
   4.770 -  "0 < k ==> k < 2 ^ len_of TYPE ('a :: len) ==> of_nat k ~= (0 :: 'a word)"
   4.771 +  "0 < k \<Longrightarrow> k < 2 ^ len_of TYPE ('a :: len) \<Longrightarrow> of_nat k ~= (0 :: 'a word)"
   4.772    by (clarsimp simp add : of_nat_0)
   4.773  
   4.774  lemma Abs_fnat_hom_add:
   4.775 @@ -1943,7 +1939,7 @@
   4.776    trans [OF unat_word_ariths(1) mod_nat_add, simplified, standard]
   4.777  
   4.778  lemma le_no_overflow: 
   4.779 -  "x <= b ==> a <= a + b ==> x <= a + (b :: 'a :: len0 word)"
   4.780 +  "x <= b \<Longrightarrow> a <= a + b \<Longrightarrow> x <= a + (b :: 'a :: len0 word)"
   4.781    apply (erule order_trans)
   4.782    apply (erule olen_add_eqv [THEN iffD1])
   4.783    done
   4.784 @@ -2064,7 +2060,7 @@
   4.785  lemmas unat_plus_simple = trans [OF no_olen_add_nat unat_add_lem, standard]
   4.786  
   4.787  lemma word_div_mult: 
   4.788 -  "(0 :: 'a :: len word) < y ==> unat x * unat y < 2 ^ len_of TYPE('a) ==> 
   4.789 +  "(0 :: 'a :: len word) < y \<Longrightarrow> unat x * unat y < 2 ^ len_of TYPE('a) \<Longrightarrow> 
   4.790      x * y div y = x"
   4.791    apply unat_arith
   4.792    apply clarsimp
   4.793 @@ -2072,7 +2068,7 @@
   4.794    apply auto
   4.795    done
   4.796  
   4.797 -lemma div_lt': "(i :: 'a :: len word) <= k div x ==> 
   4.798 +lemma div_lt': "(i :: 'a :: len word) <= k div x \<Longrightarrow> 
   4.799      unat i * unat x < 2 ^ len_of TYPE('a)"
   4.800    apply unat_arith
   4.801    apply clarsimp
   4.802 @@ -2083,7 +2079,7 @@
   4.803  
   4.804  lemmas div_lt'' = order_less_imp_le [THEN div_lt']
   4.805  
   4.806 -lemma div_lt_mult: "(i :: 'a :: len word) < k div x ==> 0 < x ==> i * x < k"
   4.807 +lemma div_lt_mult: "(i :: 'a :: len word) < k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x < k"
   4.808    apply (frule div_lt'' [THEN unat_mult_lem [THEN iffD1]])
   4.809    apply (simp add: unat_arith_simps)
   4.810    apply (drule (1) mult_less_mono1)
   4.811 @@ -2092,7 +2088,7 @@
   4.812    done
   4.813  
   4.814  lemma div_le_mult: 
   4.815 -  "(i :: 'a :: len word) <= k div x ==> 0 < x ==> i * x <= k"
   4.816 +  "(i :: 'a :: len word) <= k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x <= k"
   4.817    apply (frule div_lt' [THEN unat_mult_lem [THEN iffD1]])
   4.818    apply (simp add: unat_arith_simps)
   4.819    apply (drule mult_le_mono1)
   4.820 @@ -2101,7 +2097,7 @@
   4.821    done
   4.822  
   4.823  lemma div_lt_uint': 
   4.824 -  "(i :: 'a :: len word) <= k div x ==> uint i * uint x < 2 ^ len_of TYPE('a)"
   4.825 +  "(i :: 'a :: len word) <= k div x \<Longrightarrow> uint i * uint x < 2 ^ len_of TYPE('a)"
   4.826    apply (unfold uint_nat)
   4.827    apply (drule div_lt')
   4.828    apply (simp add: zmult_int zless_nat_eq_int_zless [symmetric] 
   4.829 @@ -2111,7 +2107,7 @@
   4.830  lemmas div_lt_uint'' = order_less_imp_le [THEN div_lt_uint']
   4.831  
   4.832  lemma word_le_exists': 
   4.833 -  "(x :: 'a :: len0 word) <= y ==> 
   4.834 +  "(x :: 'a :: len0 word) <= y \<Longrightarrow> 
   4.835      (EX z. y = x + z & uint x + uint z < 2 ^ len_of TYPE('a))"
   4.836    apply (rule exI)
   4.837    apply (rule conjI)
   4.838 @@ -2164,7 +2160,7 @@
   4.839    apply simp
   4.840    done
   4.841  
   4.842 -lemma word_mod_less_divisor: "0 < n ==> m mod n < (n :: 'a :: len word)"
   4.843 +lemma word_mod_less_divisor: "0 < n \<Longrightarrow> m mod n < (n :: 'a :: len word)"
   4.844    apply (simp only: word_less_nat_alt word_arith_nat_defs)
   4.845    apply (clarsimp simp add : uno_simps)
   4.846    done
   4.847 @@ -2178,7 +2174,7 @@
   4.848    by (simp add : word_of_int_power_hom [symmetric])
   4.849  
   4.850  lemma of_bl_length_less: 
   4.851 -  "length x = k ==> k < len_of TYPE('a) ==> (of_bl x :: 'a :: len word) < 2 ^ k"
   4.852 +  "length x = k \<Longrightarrow> k < len_of TYPE('a) \<Longrightarrow> (of_bl x :: 'a :: len word) < 2 ^ k"
   4.853    apply (unfold of_bl_no [unfolded word_number_of_def]
   4.854                  word_less_alt word_number_of_alt)
   4.855    apply safe
   4.856 @@ -2246,7 +2242,7 @@
   4.857                  bin_trunc_ao(1) [symmetric]) 
   4.858  
   4.859  lemma word_ops_nth_size:
   4.860 -  "n < size (x::'a::len0 word) ==> 
   4.861 +  "n < size (x::'a::len0 word) \<Longrightarrow> 
   4.862      (x OR y) !! n = (x !! n | y !! n) & 
   4.863      (x AND y) !! n = (x !! n & y !! n) & 
   4.864      (x XOR y) !! n = (x !! n ~= y !! n) & 
   4.865 @@ -2392,10 +2388,10 @@
   4.866  
   4.867  lemma leoa:   
   4.868    fixes x :: "'a::len0 word"
   4.869 -  shows "(w = (x OR y)) ==> (y = (w AND y))" by auto
   4.870 +  shows "(w = (x OR y)) \<Longrightarrow> (y = (w AND y))" by auto
   4.871  lemma leao: 
   4.872    fixes x' :: "'a::len0 word"
   4.873 -  shows "(w' = (x' AND y')) ==> (x' = (x' OR w'))" by auto 
   4.874 +  shows "(w' = (x' AND y')) \<Longrightarrow> (x' = (x' OR w'))" by auto 
   4.875  
   4.876  lemmas word_ao_equiv = leao [COMP leoa [COMP iffI]]
   4.877  
   4.878 @@ -2447,7 +2443,7 @@
   4.879    by (simp add : sign_Min_lt_0 number_of_is_id)
   4.880    
   4.881  lemma word_msb_no': 
   4.882 -  "w = number_of bin ==> msb (w::'a::len word) = bin_nth bin (size w - 1)"
   4.883 +  "w = number_of bin \<Longrightarrow> msb (w::'a::len word) = bin_nth bin (size w - 1)"
   4.884    unfolding word_msb_def word_number_of_def
   4.885    by (clarsimp simp add: word_sbin.eq_norm word_size bin_sign_lem)
   4.886  
   4.887 @@ -2487,7 +2483,7 @@
   4.888    unfolding to_bl_def word_test_bit_def word_size
   4.889    by (rule bin_nth_uint)
   4.890  
   4.891 -lemma to_bl_nth: "n < size w ==> to_bl w ! n = w !! (size w - Suc n)"
   4.892 +lemma to_bl_nth: "n < size w \<Longrightarrow> to_bl w ! n = w !! (size w - Suc n)"
   4.893    apply (unfold test_bit_bl)
   4.894    apply clarsimp
   4.895    apply (rule trans)
   4.896 @@ -2530,7 +2526,7 @@
   4.897  lemmas word_ops_lsb = lsb0 [unfolded word_lsb_alt]
   4.898  
   4.899  lemma td_ext_nth':
   4.900 -  "n = size (w::'a::len0 word) ==> ofn = set_bits ==> [w, ofn g] = l ==> 
   4.901 +  "n = size (w::'a::len0 word) \<Longrightarrow> ofn = set_bits \<Longrightarrow> [w, ofn g] = l \<Longrightarrow> 
   4.902      td_ext test_bit ofn {f. ALL i. f i --> i < n} (%h i. h i & i < n)"
   4.903    apply (unfold word_size td_ext_def')
   4.904    apply (safe del: subset_antisym)
   4.905 @@ -2575,7 +2571,7 @@
   4.906      
   4.907  lemma test_bit_no': 
   4.908    fixes w :: "'a::len0 word"
   4.909 -  shows "w = number_of bin ==> test_bit w n = (n < size w & bin_nth bin n)"
   4.910 +  shows "w = number_of bin \<Longrightarrow> test_bit w n = (n < size w & bin_nth bin n)"
   4.911    unfolding word_test_bit_def word_number_of_def word_size
   4.912    by (simp add : nth_bintr [symmetric] word_ubin.eq_norm)
   4.913  
   4.914 @@ -2605,10 +2601,13 @@
   4.915                          test_bit_no nth_bintr)
   4.916    done
   4.917  
   4.918 -lemmas setBit_no = setBit_def [THEN trans [OF meta_eq_to_obj_eq word_set_no],
   4.919 -  simplified if_simps, THEN eq_reflection, standard]
   4.920 -lemmas clearBit_no = clearBit_def [THEN trans [OF meta_eq_to_obj_eq word_set_no],
   4.921 -  simplified if_simps, THEN eq_reflection, standard]
   4.922 +lemma setBit_no:
   4.923 +  "setBit (number_of bin) n = number_of (bin_sc n 1 bin) "
   4.924 +  by (simp add: setBit_def word_set_no)
   4.925 +
   4.926 +lemma clearBit_no:
   4.927 +  "clearBit (number_of bin) n = number_of (bin_sc n 0 bin)"
   4.928 +  by (simp add: clearBit_def word_set_no)
   4.929  
   4.930  lemma to_bl_n1: 
   4.931    "to_bl (-1::'a::len0 word) = replicate (len_of TYPE ('a)) True"
   4.932 @@ -2643,7 +2642,7 @@
   4.933    done
   4.934  
   4.935  lemma test_bit_2p': 
   4.936 -  "w = word_of_int (2 ^ n) ==> 
   4.937 +  "w = word_of_int (2 ^ n) \<Longrightarrow> 
   4.938      w !! m = (m = n & m < size (w :: 'a :: len word))"
   4.939    unfolding word_test_bit_def word_size
   4.940    by (auto simp add: word_ubin.eq_norm nth_bintr nth_2p_bin)
   4.941 @@ -2656,7 +2655,7 @@
   4.942    by (simp add:  of_int_power)
   4.943  
   4.944  lemma uint_2p: 
   4.945 -  "(0::'a::len word) < 2 ^ n ==> uint (2 ^ n::'a::len word) = 2 ^ n"
   4.946 +  "(0::'a::len word) < 2 ^ n \<Longrightarrow> uint (2 ^ n::'a::len word) = 2 ^ n"
   4.947    apply (unfold word_arith_power_alt)
   4.948    apply (case_tac "len_of TYPE ('a)")
   4.949     apply clarsimp
   4.950 @@ -2682,7 +2681,7 @@
   4.951    apply simp 
   4.952    done
   4.953  
   4.954 -lemma bang_is_le: "x !! m ==> 2 ^ m <= (x :: 'a :: len word)" 
   4.955 +lemma bang_is_le: "x !! m \<Longrightarrow> 2 ^ m <= (x :: 'a :: len word)" 
   4.956    apply (rule xtr3) 
   4.957    apply (rule_tac [2] y = "x" in le_word_or2)
   4.958    apply (rule word_eqI)
   4.959 @@ -2996,7 +2995,7 @@
   4.960  lemmas hd_sshiftr = take_sshiftr' [THEN conjunct1, standard]
   4.961  lemmas take_sshiftr = take_sshiftr' [THEN conjunct2, standard]
   4.962  
   4.963 -lemma atd_lem: "take n xs = t ==> drop n xs = d ==> xs = t @ d"
   4.964 +lemma atd_lem: "take n xs = t \<Longrightarrow> drop n xs = d \<Longrightarrow> xs = t @ d"
   4.965    by (auto intro: append_take_drop_id [symmetric])
   4.966  
   4.967  lemmas bl_shiftr = atd_lem [OF take_shiftr drop_shiftr]
   4.968 @@ -3022,7 +3021,7 @@
   4.969  
   4.970  lemma shiftl_zero_size: 
   4.971    fixes x :: "'a::len0 word"
   4.972 -  shows "size x <= n ==> x << n = 0"
   4.973 +  shows "size x <= n \<Longrightarrow> x << n = 0"
   4.974    apply (unfold word_size)
   4.975    apply (rule word_eqI)
   4.976    apply (clarsimp simp add: shiftl_bl word_size test_bit_of_bl nth_append)
   4.977 @@ -3059,7 +3058,7 @@
   4.978    by (simp add : word_sbin.eq_norm)
   4.979  
   4.980  lemma shiftr_no': 
   4.981 -  "w = number_of bin ==> 
   4.982 +  "w = number_of bin \<Longrightarrow> 
   4.983    (w::'a::len0 word) >> n = number_of ((bin_rest ^^ n) (bintrunc (size w) bin))"
   4.984    apply clarsimp
   4.985    apply (rule word_eqI)
   4.986 @@ -3067,7 +3066,7 @@
   4.987    done
   4.988  
   4.989  lemma sshiftr_no': 
   4.990 -  "w = number_of bin ==> w >>> n = number_of ((bin_rest ^^ n) 
   4.991 +  "w = number_of bin \<Longrightarrow> w >>> n = number_of ((bin_rest ^^ n) 
   4.992      (sbintrunc (size w - 1) bin))"
   4.993    apply clarsimp
   4.994    apply (rule word_eqI)
   4.995 @@ -3082,7 +3081,7 @@
   4.996    shiftr_no' [where w = "number_of w", OF refl, unfolded word_size, standard]
   4.997  
   4.998  lemma shiftr1_bl_of': 
   4.999 -  "us = shiftr1 (of_bl bl) ==> length bl <= size us ==> 
  4.1000 +  "us = shiftr1 (of_bl bl) \<Longrightarrow> length bl <= size us \<Longrightarrow> 
  4.1001      us = of_bl (butlast bl)"
  4.1002    by (clarsimp simp: shiftr1_def of_bl_def word_size butlast_rest_bl2bin 
  4.1003                       word_ubin.eq_norm trunc_bl2bin)
  4.1004 @@ -3090,7 +3089,7 @@
  4.1005  lemmas shiftr1_bl_of = refl [THEN shiftr1_bl_of', unfolded word_size]
  4.1006  
  4.1007  lemma shiftr_bl_of' [rule_format]: 
  4.1008 -  "us = of_bl bl >> n ==> length bl <= size us --> 
  4.1009 +  "us = of_bl bl >> n \<Longrightarrow> length bl <= size us --> 
  4.1010     us = of_bl (take (length bl - n) bl)"
  4.1011    apply (unfold shiftr_def)
  4.1012    apply hypsubst
  4.1013 @@ -3147,8 +3146,8 @@
  4.1014    done
  4.1015  
  4.1016  lemma aligned_bl_add_size':
  4.1017 -  "size x - n = m ==> n <= size x ==> drop m (to_bl x) = replicate n False ==>
  4.1018 -    take m (to_bl y) = replicate m False ==> 
  4.1019 +  "size x - n = m \<Longrightarrow> n <= size x \<Longrightarrow> drop m (to_bl x) = replicate n False \<Longrightarrow>
  4.1020 +    take m (to_bl y) = replicate m False \<Longrightarrow> 
  4.1021      to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)"
  4.1022    apply (subgoal_tac "x AND y = 0")
  4.1023     prefer 2
  4.1024 @@ -3167,7 +3166,7 @@
  4.1025  
  4.1026  subsubsection "Mask"
  4.1027  
  4.1028 -lemma nth_mask': "m = mask n ==> test_bit m i = (i < n & i < size m)"
  4.1029 +lemma nth_mask': "m = mask n \<Longrightarrow> test_bit m i = (i < n & i < size m)"
  4.1030    apply (unfold mask_def test_bit_bl)
  4.1031    apply (simp only: word_1_bl [symmetric] shiftl_of_bl)
  4.1032    apply (clarsimp simp add: word_size)
  4.1033 @@ -3247,14 +3246,14 @@
  4.1034    done
  4.1035  
  4.1036  lemma word_2p_lem: 
  4.1037 -  "n < size w ==> w < 2 ^ n = (uint (w :: 'a :: len word) < 2 ^ n)"
  4.1038 +  "n < size w \<Longrightarrow> w < 2 ^ n = (uint (w :: 'a :: len word) < 2 ^ n)"
  4.1039    apply (unfold word_size word_less_alt word_number_of_alt)
  4.1040    apply (clarsimp simp add: word_of_int_power_hom word_uint.eq_norm 
  4.1041                              int_mod_eq'
  4.1042                    simp del: word_of_int_bin)
  4.1043    done
  4.1044  
  4.1045 -lemma less_mask_eq: "x < 2 ^ n ==> x AND mask n = (x :: 'a :: len word)"
  4.1046 +lemma less_mask_eq: "x < 2 ^ n \<Longrightarrow> x AND mask n = (x :: 'a :: len word)"
  4.1047    apply (unfold word_less_alt word_number_of_alt)
  4.1048    apply (clarsimp simp add: and_mask_mod_2p word_of_int_power_hom 
  4.1049                              word_uint.eq_norm
  4.1050 @@ -3270,11 +3269,11 @@
  4.1051  lemmas and_mask_less' = 
  4.1052    iffD2 [OF word_2p_lem and_mask_lt_2p, simplified word_size, standard]
  4.1053  
  4.1054 -lemma and_mask_less_size: "n < size x ==> x AND mask n < 2^n"
  4.1055 +lemma and_mask_less_size: "n < size x \<Longrightarrow> x AND mask n < 2^n"
  4.1056    unfolding word_size by (erule and_mask_less')
  4.1057  
  4.1058  lemma word_mod_2p_is_mask':
  4.1059 -  "c = 2 ^ n ==> c > 0 ==> x mod c = (x :: 'a :: len word) AND mask n" 
  4.1060 +  "c = 2 ^ n \<Longrightarrow> c > 0 \<Longrightarrow> x mod c = (x :: 'a :: len word) AND mask n" 
  4.1061    by (clarsimp simp add: word_mod_def uint_2p and_mask_mod_2p) 
  4.1062  
  4.1063  lemmas word_mod_2p_is_mask = refl [THEN word_mod_2p_is_mask'] 
  4.1064 @@ -3317,7 +3316,7 @@
  4.1065    done
  4.1066  
  4.1067  lemma revcast_rev_ucast': 
  4.1068 -  "cs = [rc, uc] ==> rc = revcast (word_reverse w) ==> uc = ucast w ==> 
  4.1069 +  "cs = [rc, uc] \<Longrightarrow> rc = revcast (word_reverse w) \<Longrightarrow> uc = ucast w \<Longrightarrow> 
  4.1070      rc = word_reverse uc"
  4.1071    apply (unfold ucast_def revcast_def' Let_def word_reverse_def)
  4.1072    apply (clarsimp simp add : to_bl_of_bin takefill_bintrunc)
  4.1073 @@ -3338,7 +3337,7 @@
  4.1074  lemmas wsst_TYs = source_size target_size word_size
  4.1075  
  4.1076  lemma revcast_down_uu': 
  4.1077 -  "rc = revcast ==> source_size rc = target_size rc + n ==> 
  4.1078 +  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> 
  4.1079      rc (w :: 'a :: len word) = ucast (w >> n)"
  4.1080    apply (simp add: revcast_def')
  4.1081    apply (rule word_bl.Rep_inverse')
  4.1082 @@ -3349,7 +3348,7 @@
  4.1083    done
  4.1084  
  4.1085  lemma revcast_down_us': 
  4.1086 -  "rc = revcast ==> source_size rc = target_size rc + n ==> 
  4.1087 +  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> 
  4.1088      rc (w :: 'a :: len word) = ucast (w >>> n)"
  4.1089    apply (simp add: revcast_def')
  4.1090    apply (rule word_bl.Rep_inverse')
  4.1091 @@ -3360,7 +3359,7 @@
  4.1092    done
  4.1093  
  4.1094  lemma revcast_down_su': 
  4.1095 -  "rc = revcast ==> source_size rc = target_size rc + n ==> 
  4.1096 +  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> 
  4.1097      rc (w :: 'a :: len word) = scast (w >> n)"
  4.1098    apply (simp add: revcast_def')
  4.1099    apply (rule word_bl.Rep_inverse')
  4.1100 @@ -3371,7 +3370,7 @@
  4.1101    done
  4.1102  
  4.1103  lemma revcast_down_ss': 
  4.1104 -  "rc = revcast ==> source_size rc = target_size rc + n ==> 
  4.1105 +  "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> 
  4.1106      rc (w :: 'a :: len word) = scast (w >>> n)"
  4.1107    apply (simp add: revcast_def')
  4.1108    apply (rule word_bl.Rep_inverse')
  4.1109 @@ -3387,7 +3386,7 @@
  4.1110  lemmas revcast_down_ss = refl [THEN revcast_down_ss']
  4.1111  
  4.1112  lemma cast_down_rev: 
  4.1113 -  "uc = ucast ==> source_size uc = target_size uc + n ==> 
  4.1114 +  "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow> 
  4.1115      uc w = revcast ((w :: 'a :: len word) << n)"
  4.1116    apply (unfold shiftl_rev)
  4.1117    apply clarify
  4.1118 @@ -3399,7 +3398,7 @@
  4.1119    done
  4.1120  
  4.1121  lemma revcast_up': 
  4.1122 -  "rc = revcast ==> source_size rc + n = target_size rc ==> 
  4.1123 +  "rc = revcast \<Longrightarrow> source_size rc + n = target_size rc \<Longrightarrow> 
  4.1124      rc w = (ucast w :: 'a :: len word) << n" 
  4.1125    apply (simp add: revcast_def')
  4.1126    apply (rule word_bl.Rep_inverse')
  4.1127 @@ -3424,13 +3423,14 @@
  4.1128  
  4.1129  subsubsection "Slices"
  4.1130  
  4.1131 -lemmas slice1_no_bin [simp] =
  4.1132 -  slice1_def [where w="number_of w", unfolded to_bl_no_bin, standard]
  4.1133 -
  4.1134 -lemmas slice_no_bin [simp] = 
  4.1135 -   trans [OF slice_def [THEN meta_eq_to_obj_eq] 
  4.1136 -             slice1_no_bin [THEN meta_eq_to_obj_eq], 
  4.1137 -          unfolded word_size, standard]
  4.1138 +lemma slice1_no_bin [simp]:
  4.1139 +  "slice1 n (number_of w :: 'b word) = of_bl (takefill False n (bin_to_bl (len_of TYPE('b :: len0)) w))"
  4.1140 +  by (simp add: slice1_def)
  4.1141 +
  4.1142 +lemma slice_no_bin [simp]:
  4.1143 +  "slice n (number_of w :: 'b word) = of_bl (takefill False (len_of TYPE('b :: len0) - n)
  4.1144 +    (bin_to_bl (len_of TYPE('b :: len0)) w))"
  4.1145 +  by (simp add: slice_def word_size)
  4.1146  
  4.1147  lemma slice1_0 [simp] : "slice1 n 0 = 0"
  4.1148    unfolding slice1_def by (simp add : to_bl_0)
  4.1149 @@ -3462,13 +3462,13 @@
  4.1150    by (simp add : nth_ucast nth_shiftr)
  4.1151  
  4.1152  lemma slice1_down_alt': 
  4.1153 -  "sl = slice1 n w ==> fs = size sl ==> fs + k = n ==> 
  4.1154 +  "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs + k = n \<Longrightarrow> 
  4.1155      to_bl sl = takefill False fs (drop k (to_bl w))"
  4.1156    unfolding slice1_def word_size of_bl_def uint_bl
  4.1157    by (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop drop_takefill)
  4.1158  
  4.1159  lemma slice1_up_alt': 
  4.1160 -  "sl = slice1 n w ==> fs = size sl ==> fs = n + k ==> 
  4.1161 +  "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs = n + k \<Longrightarrow> 
  4.1162      to_bl sl = takefill False fs (replicate k False @ (to_bl w))"
  4.1163    apply (unfold slice1_def word_size of_bl_def uint_bl)
  4.1164    apply (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop 
  4.1165 @@ -3495,7 +3495,7 @@
  4.1166  lemmas slice_id = trans [OF ucast_slice [symmetric] ucast_id]
  4.1167  
  4.1168  lemma revcast_slice1': 
  4.1169 -  "rc = revcast w ==> slice1 (size rc) w = rc"
  4.1170 +  "rc = revcast w \<Longrightarrow> slice1 (size rc) w = rc"
  4.1171    unfolding slice1_def revcast_def' by (simp add : word_size)
  4.1172  
  4.1173  lemmas revcast_slice1 = refl [THEN revcast_slice1']
  4.1174 @@ -3522,7 +3522,7 @@
  4.1175    done
  4.1176  
  4.1177  lemma rev_slice': 
  4.1178 -  "res = slice n (word_reverse w) ==> n + k + size res = size w ==> 
  4.1179 +  "res = slice n (word_reverse w) \<Longrightarrow> n + k + size res = size w \<Longrightarrow> 
  4.1180      res = word_reverse (slice k w)"
  4.1181    apply (unfold slice_def word_size)
  4.1182    apply clarify
  4.1183 @@ -3569,8 +3569,8 @@
  4.1184  
  4.1185  subsection "Split and cat"
  4.1186  
  4.1187 -lemmas word_split_bin' = word_split_def [THEN meta_eq_to_obj_eq, standard]
  4.1188 -lemmas word_cat_bin' = word_cat_def [THEN meta_eq_to_obj_eq, standard]
  4.1189 +lemmas word_split_bin' = word_split_def
  4.1190 +lemmas word_cat_bin' = word_cat_def
  4.1191  
  4.1192  lemma word_rsplit_no:
  4.1193    "(word_rsplit (number_of bin :: 'b :: len0 word) :: 'a word list) = 
  4.1194 @@ -3584,7 +3584,7 @@
  4.1195    [unfolded bin_rsplitl_def bin_rsplit_l [symmetric]]
  4.1196  
  4.1197  lemma test_bit_cat:
  4.1198 -  "wc = word_cat a b ==> wc !! n = (n < size wc & 
  4.1199 +  "wc = word_cat a b \<Longrightarrow> wc !! n = (n < size wc & 
  4.1200      (if n < size b then b !! n else a !! (n - size b)))"
  4.1201    apply (unfold word_cat_bin' test_bit_bin)
  4.1202    apply (auto simp add : word_ubin.eq_norm nth_bintr bin_nth_cat word_size)
  4.1203 @@ -3617,7 +3617,7 @@
  4.1204    "of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs"
  4.1205    by (cases x) (simp_all add: of_bl_True)
  4.1206  
  4.1207 -lemma split_uint_lem: "bin_split n (uint (w :: 'a :: len0 word)) = (a, b) ==> 
  4.1208 +lemma split_uint_lem: "bin_split n (uint (w :: 'a :: len0 word)) = (a, b) \<Longrightarrow> 
  4.1209    a = bintrunc (len_of TYPE('a) - n) a & b = bintrunc (len_of TYPE('a)) b"
  4.1210    apply (frule word_ubin.norm_Rep [THEN ssubst])
  4.1211    apply (drule bin_split_trunc1)
  4.1212 @@ -3627,7 +3627,7 @@
  4.1213    done
  4.1214  
  4.1215  lemma word_split_bl': 
  4.1216 -  "std = size c - size b ==> (word_split c = (a, b)) ==> 
  4.1217 +  "std = size c - size b \<Longrightarrow> (word_split c = (a, b)) \<Longrightarrow> 
  4.1218      (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c)))"
  4.1219    apply (unfold word_split_bin')
  4.1220    apply safe
  4.1221 @@ -3653,7 +3653,7 @@
  4.1222    apply (simp add : word_ubin.norm_eq_iff [symmetric])
  4.1223    done
  4.1224  
  4.1225 -lemma word_split_bl: "std = size c - size b ==> 
  4.1226 +lemma word_split_bl: "std = size c - size b \<Longrightarrow> 
  4.1227      (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c))) <-> 
  4.1228      word_split c = (a, b)"
  4.1229    apply (rule iffI)
  4.1230 @@ -3714,7 +3714,7 @@
  4.1231  -- "limited hom result"
  4.1232  lemma word_cat_hom:
  4.1233    "len_of TYPE('a::len0) <= len_of TYPE('b::len0) + len_of TYPE ('c::len0)
  4.1234 -  ==>
  4.1235 +  \<Longrightarrow>
  4.1236    (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) = 
  4.1237    word_of_int (bin_cat w (size b) (uint b))"
  4.1238    apply (unfold word_cat_def word_size) 
  4.1239 @@ -3723,7 +3723,7 @@
  4.1240    done
  4.1241  
  4.1242  lemma word_cat_split_alt:
  4.1243 -  "size w <= size u + size v ==> word_split w = (u, v) ==> word_cat u v = w"
  4.1244 +  "size w <= size u + size v \<Longrightarrow> word_split w = (u, v) \<Longrightarrow> word_cat u v = w"
  4.1245    apply (rule word_eqI)
  4.1246    apply (drule test_bit_split)
  4.1247    apply (clarsimp simp add : test_bit_cat word_size)
  4.1248 @@ -3738,14 +3738,14 @@
  4.1249  subsubsection "Split and slice"
  4.1250  
  4.1251  lemma split_slices: 
  4.1252 -  "word_split w = (u, v) ==> u = slice (size v) w & v = slice 0 w"
  4.1253 +  "word_split w = (u, v) \<Longrightarrow> u = slice (size v) w & v = slice 0 w"
  4.1254    apply (drule test_bit_split)
  4.1255    apply (rule conjI)
  4.1256     apply (rule word_eqI, clarsimp simp: nth_slice word_size)+
  4.1257    done
  4.1258  
  4.1259  lemma slice_cat1':
  4.1260 -  "wc = word_cat a b ==> size wc >= size a + size b ==> slice (size b) wc = a"
  4.1261 +  "wc = word_cat a b \<Longrightarrow> size wc >= size a + size b \<Longrightarrow> slice (size b) wc = a"
  4.1262    apply safe
  4.1263    apply (rule word_eqI)
  4.1264    apply (simp add: nth_slice test_bit_cat word_size)
  4.1265 @@ -3755,8 +3755,8 @@
  4.1266  lemmas slice_cat2 = trans [OF slice_id word_cat_id]
  4.1267  
  4.1268  lemma cat_slices:
  4.1269 -  "a = slice n c ==> b = slice 0 c ==> n = size b ==>
  4.1270 -    size a + size b >= size c ==> word_cat a b = c"
  4.1271 +  "a = slice n c \<Longrightarrow> b = slice 0 c \<Longrightarrow> n = size b \<Longrightarrow>
  4.1272 +    size a + size b >= size c \<Longrightarrow> word_cat a b = c"
  4.1273    apply safe
  4.1274    apply (rule word_eqI)
  4.1275    apply (simp add: nth_slice test_bit_cat word_size)
  4.1276 @@ -3765,7 +3765,7 @@
  4.1277    done
  4.1278  
  4.1279  lemma word_split_cat_alt:
  4.1280 -  "w = word_cat u v ==> size u + size v <= size w ==> word_split w = (u, v)"
  4.1281 +  "w = word_cat u v \<Longrightarrow> size u + size v <= size w \<Longrightarrow> word_split w = (u, v)"
  4.1282    apply (case_tac "word_split ?w")
  4.1283    apply (rule trans, assumption)
  4.1284    apply (drule test_bit_split)
  4.1285 @@ -3794,8 +3794,8 @@
  4.1286    by (simp add: bin_rsplit_aux_simp_alt Let_def split: Product_Type.split_split)
  4.1287  
  4.1288  lemma test_bit_rsplit:
  4.1289 -  "sw = word_rsplit w ==> m < size (hd sw :: 'a :: len word) ==> 
  4.1290 -    k < length sw ==> (rev sw ! k) !! m = (w !! (k * size (hd sw) + m))"
  4.1291 +  "sw = word_rsplit w \<Longrightarrow> m < size (hd sw :: 'a :: len word) \<Longrightarrow> 
  4.1292 +    k < length sw \<Longrightarrow> (rev sw ! k) !! m = (w !! (k * size (hd sw) + m))"
  4.1293    apply (unfold word_rsplit_def word_test_bit_def)
  4.1294    apply (rule trans)
  4.1295     apply (rule_tac f = "%x. bin_nth x m" in arg_cong)
  4.1296 @@ -3812,7 +3812,7 @@
  4.1297    apply (erule bin_rsplit_size_sign [OF len_gt_0 refl])
  4.1298    done
  4.1299  
  4.1300 -lemma word_rcat_bl: "word_rcat wl == of_bl (concat (map to_bl wl))"
  4.1301 +lemma word_rcat_bl: "word_rcat wl = of_bl (concat (map to_bl wl))"
  4.1302    unfolding word_rcat_def to_bl_def' of_bl_def
  4.1303    by (clarsimp simp add : bin_rcat_bl)
  4.1304  
  4.1305 @@ -3825,7 +3825,7 @@
  4.1306  lemmas td_gal_lt_len = len_gt_0 [THEN td_gal_lt, standard]
  4.1307  
  4.1308  lemma nth_rcat_lem' [rule_format] :
  4.1309 -  "sw = size (hd wl  :: 'a :: len word) ==> (ALL n. n < size wl * sw --> 
  4.1310 +  "sw = size (hd wl  :: 'a :: len word) \<Longrightarrow> (ALL n. n < size wl * sw --> 
  4.1311      rev (concat (map to_bl wl)) ! n = 
  4.1312      rev (to_bl (rev wl ! (n div sw))) ! (n mod sw))"
  4.1313    apply (unfold word_size)
  4.1314 @@ -3840,7 +3840,7 @@
  4.1315  lemmas nth_rcat_lem = refl [THEN nth_rcat_lem', unfolded word_size]
  4.1316  
  4.1317  lemma test_bit_rcat:
  4.1318 -  "sw = size (hd wl :: 'a :: len word) ==> rc = word_rcat wl ==> rc !! n = 
  4.1319 +  "sw = size (hd wl :: 'a :: len word) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> rc !! n = 
  4.1320      (n < size rc & n div sw < size wl & (rev wl) ! (n div sw) !! (n mod sw))"
  4.1321    apply (unfold word_rcat_bl word_size)
  4.1322    apply (clarsimp simp add : 
  4.1323 @@ -3862,8 +3862,8 @@
  4.1324  
  4.1325  -- "lazy way of expressing that u and v, and su and sv, have same types"
  4.1326  lemma word_rsplit_len_indep':
  4.1327 -  "[u,v] = p ==> [su,sv] = q ==> word_rsplit u = su ==> 
  4.1328 -    word_rsplit v = sv ==> length su = length sv"
  4.1329 +  "[u,v] = p \<Longrightarrow> [su,sv] = q \<Longrightarrow> word_rsplit u = su \<Longrightarrow> 
  4.1330 +    word_rsplit v = sv \<Longrightarrow> length su = length sv"
  4.1331    apply (unfold word_rsplit_def)
  4.1332    apply (auto simp add : bin_rsplit_len_indep)
  4.1333    done
  4.1334 @@ -3871,7 +3871,7 @@
  4.1335  lemmas word_rsplit_len_indep = word_rsplit_len_indep' [OF refl refl refl refl]
  4.1336  
  4.1337  lemma length_word_rsplit_size: 
  4.1338 -  "n = len_of TYPE ('a :: len) ==> 
  4.1339 +  "n = len_of TYPE ('a :: len) \<Longrightarrow> 
  4.1340      (length (word_rsplit w :: 'a word list) <= m) = (size w <= m * n)"
  4.1341    apply (unfold word_rsplit_def word_size)
  4.1342    apply (clarsimp simp add : bin_rsplit_len_le)
  4.1343 @@ -3881,12 +3881,12 @@
  4.1344    length_word_rsplit_size [unfolded Not_eq_iff linorder_not_less [symmetric]]
  4.1345  
  4.1346  lemma length_word_rsplit_exp_size: 
  4.1347 -  "n = len_of TYPE ('a :: len) ==> 
  4.1348 +  "n = len_of TYPE ('a :: len) \<Longrightarrow> 
  4.1349      length (word_rsplit w :: 'a word list) = (size w + n - 1) div n"
  4.1350    unfolding word_rsplit_def by (clarsimp simp add : word_size bin_rsplit_len)
  4.1351  
  4.1352  lemma length_word_rsplit_even_size: 
  4.1353 -  "n = len_of TYPE ('a :: len) ==> size w = m * n ==> 
  4.1354 +  "n = len_of TYPE ('a :: len) \<Longrightarrow> size w = m * n \<Longrightarrow> 
  4.1355      length (word_rsplit w :: 'a word list) = m"
  4.1356    by (clarsimp simp add : length_word_rsplit_exp_size given_quot_alt)
  4.1357  
  4.1358 @@ -3907,8 +3907,8 @@
  4.1359    done
  4.1360  
  4.1361  lemma size_word_rsplit_rcat_size':
  4.1362 -  "word_rcat (ws :: 'a :: len word list) = frcw ==> 
  4.1363 -    size frcw = length ws * len_of TYPE ('a) ==> 
  4.1364 +  "word_rcat (ws :: 'a :: len word list) = frcw \<Longrightarrow> 
  4.1365 +    size frcw = length ws * len_of TYPE ('a) \<Longrightarrow> 
  4.1366      size (hd [word_rsplit frcw, ws]) = size ws" 
  4.1367    apply (clarsimp simp add : word_size length_word_rsplit_exp_size')
  4.1368    apply (fast intro: given_quot_alt)
  4.1369 @@ -3924,8 +3924,8 @@
  4.1370    by (auto simp: add_commute)
  4.1371  
  4.1372  lemma word_rsplit_rcat_size':
  4.1373 -  "word_rcat (ws :: 'a :: len word list) = frcw ==> 
  4.1374 -    size frcw = length ws * len_of TYPE ('a) ==> word_rsplit frcw = ws" 
  4.1375 +  "word_rcat (ws :: 'a :: len word list) = frcw \<Longrightarrow> 
  4.1376 +    size frcw = length ws * len_of TYPE ('a) \<Longrightarrow> word_rsplit frcw = ws" 
  4.1377    apply (frule size_word_rsplit_rcat_size, assumption)
  4.1378    apply (clarsimp simp add : word_size)
  4.1379    apply (rule nth_equalityI, assumption)
  4.1380 @@ -3957,7 +3957,7 @@
  4.1381  lemmas word_rot_defs = word_roti_def word_rotr_def word_rotl_def
  4.1382  
  4.1383  lemma rotate_eq_mod: 
  4.1384 -  "m mod length xs = n mod length xs ==> rotate m xs = rotate n xs"
  4.1385 +  "m mod length xs = n mod length xs \<Longrightarrow> rotate m xs = rotate n xs"
  4.1386    apply (rule box_equals)
  4.1387      defer
  4.1388      apply (rule rotate_conv_mod [symmetric])+
  4.1389 @@ -4049,11 +4049,11 @@
  4.1390  
  4.1391  subsubsection "map, map2, commuting with rotate(r)"
  4.1392  
  4.1393 -lemma last_map: "xs ~= [] ==> last (map f xs) = f (last xs)"
  4.1394 +lemma last_map: "xs ~= [] \<Longrightarrow> last (map f xs) = f (last xs)"
  4.1395    by (induct xs) auto
  4.1396  
  4.1397  lemma butlast_map:
  4.1398 -  "xs ~= [] ==> butlast (map f xs) = map f (butlast xs)"
  4.1399 +  "xs ~= [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)"
  4.1400    by (induct xs) auto
  4.1401  
  4.1402  lemma rotater1_map: "rotater1 (map f xs) = map f (rotater1 xs)" 
  4.1403 @@ -4085,7 +4085,7 @@
  4.1404    done
  4.1405  
  4.1406  lemma rotater1_zip:
  4.1407 -  "length xs = length ys ==> 
  4.1408 +  "length xs = length ys \<Longrightarrow> 
  4.1409      rotater1 (zip xs ys) = zip (rotater1 xs) (rotater1 ys)" 
  4.1410    apply (unfold rotater1_def)
  4.1411    apply (cases "xs")
  4.1412 @@ -4094,7 +4094,7 @@
  4.1413    done
  4.1414  
  4.1415  lemma rotater1_map2:
  4.1416 -  "length xs = length ys ==> 
  4.1417 +  "length xs = length ys \<Longrightarrow> 
  4.1418      rotater1 (map2 f xs ys) = map2 f (rotater1 xs) (rotater1 ys)" 
  4.1419    unfolding map2_def by (simp add: rotater1_map rotater1_zip)
  4.1420  
  4.1421 @@ -4104,12 +4104,12 @@
  4.1422                THEN rotater1_map2]
  4.1423  
  4.1424  lemma rotater_map2: 
  4.1425 -  "length xs = length ys ==> 
  4.1426 +  "length xs = length ys \<Longrightarrow> 
  4.1427      rotater n (map2 f xs ys) = map2 f (rotater n xs) (rotater n ys)" 
  4.1428    by (induct n) (auto intro!: lrth)
  4.1429  
  4.1430  lemma rotate1_map2:
  4.1431 -  "length xs = length ys ==> 
  4.1432 +  "length xs = length ys \<Longrightarrow> 
  4.1433      rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)" 
  4.1434    apply (unfold map2_def)
  4.1435    apply (cases xs)
  4.1436 @@ -4120,7 +4120,7 @@
  4.1437    length_rotate [symmetric], THEN rotate1_map2]
  4.1438  
  4.1439  lemma rotate_map2: 
  4.1440 -  "length xs = length ys ==> 
  4.1441 +  "length xs = length ys \<Longrightarrow> 
  4.1442      rotate n (map2 f xs ys) = map2 f (rotate n xs) (rotate n ys)" 
  4.1443    by (induct n) (auto intro!: lth)
  4.1444  
  4.1445 @@ -4177,11 +4177,11 @@
  4.1446    "word_roti (m + n) w = word_roti m (word_roti n w)"
  4.1447  proof -
  4.1448    have rotater_eq_lem: 
  4.1449 -    "\<And>m n xs. m = n ==> rotater m xs = rotater n xs"
  4.1450 +    "\<And>m n xs. m = n \<Longrightarrow> rotater m xs = rotater n xs"
  4.1451      by auto
  4.1452  
  4.1453    have rotate_eq_lem: 
  4.1454 -    "\<And>m n xs. m = n ==> rotate m xs = rotate n xs"
  4.1455 +    "\<And>m n xs. m = n \<Longrightarrow> rotate m xs = rotate n xs"
  4.1456      by auto
  4.1457  
  4.1458    note rpts [symmetric, standard] = 
  4.1459 @@ -4271,7 +4271,7 @@
  4.1460    simplified word_bl.Rep', standard]
  4.1461  
  4.1462  lemma bl_word_roti_dt': 
  4.1463 -  "n = nat ((- i) mod int (size (w :: 'a :: len word))) ==> 
  4.1464 +  "n = nat ((- i) mod int (size (w :: 'a :: len word))) \<Longrightarrow> 
  4.1465      to_bl (word_roti i w) = drop n (to_bl w) @ take n (to_bl w)"
  4.1466    apply (unfold word_roti_def)
  4.1467    apply (simp add: bl_word_rotl_dt bl_word_rotr_dt word_size)
  4.1468 @@ -4457,12 +4457,12 @@
  4.1469    by (simp add: mask_bl word_rep_drop min_def)
  4.1470  
  4.1471  lemma map_replicate_True:
  4.1472 -  "n = length xs ==>
  4.1473 +  "n = length xs \<Longrightarrow>
  4.1474      map (\<lambda>(x,y). x & y) (zip xs (replicate n True)) = xs"
  4.1475    by (induct xs arbitrary: n) auto
  4.1476  
  4.1477  lemma map_replicate_False:
  4.1478 -  "n = length xs ==> map (\<lambda>(x,y). x & y)
  4.1479 +  "n = length xs \<Longrightarrow> map (\<lambda>(x,y). x & y)
  4.1480      (zip xs (replicate n False)) = replicate n False"
  4.1481    by (induct xs arbitrary: n) auto
  4.1482  
  4.1483 @@ -4488,7 +4488,7 @@
  4.1484  qed
  4.1485  
  4.1486  lemma drop_rev_takefill:
  4.1487 -  "length xs \<le> n ==>
  4.1488 +  "length xs \<le> n \<Longrightarrow>
  4.1489      drop (n - length xs) (rev (takefill False n (rev xs))) = xs"
  4.1490    by (simp add: takefill_alt rev_take)
  4.1491  
  4.1492 @@ -4547,7 +4547,7 @@
  4.1493                  word_size)
  4.1494  
  4.1495  lemma unat_sub:
  4.1496 -  "b <= a ==> unat (a - b) = unat a - unat b"
  4.1497 +  "b <= a \<Longrightarrow> unat (a - b) = unat a - unat b"
  4.1498    by (simp add: unat_def uint_sub_if_size word_le_def nat_diff_distrib)
  4.1499  
  4.1500  lemmas word_less_sub1_numberof [simp] =
  4.1501 @@ -4633,7 +4633,7 @@
  4.1502    done
  4.1503  
  4.1504  definition word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a" where
  4.1505 -  "word_rec forZero forSuc n \<equiv> nat_rec forZero (forSuc \<circ> of_nat) (unat n)"
  4.1506 +  "word_rec forZero forSuc n = nat_rec forZero (forSuc \<circ> of_nat) (unat n)"
  4.1507  
  4.1508  lemma word_rec_0: "word_rec z s 0 = z"
  4.1509    by (simp add: word_rec_def)