eliminated some old folds;
authorwenzelm
Tue Oct 27 22:57:23 2009 +0100 (2009-10-27)
changeset 3324646e47aa1558f
parent 33245 65232054ffd0
child 33263 03c08ce703bf
eliminated some old folds;
src/HOL/Tools/refute.ML
     1.1 --- a/src/HOL/Tools/refute.ML	Tue Oct 27 22:56:14 2009 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Tue Oct 27 22:57:23 2009 +0100
     1.3 @@ -430,9 +430,8 @@
     1.4      (* (Term.indexname * Term.typ) list *)
     1.5      val vars = sort_wrt (fst o fst) (map dest_Var (OldTerm.term_vars t))
     1.6    in
     1.7 -    Library.foldl (fn (t', ((x, i), T)) =>
     1.8 -      (Term.all T) $ Abs (x, T, abstract_over (Var ((x, i), T), t')))
     1.9 -      (t, vars)
    1.10 +    fold (fn ((x, i), T) => fn t' =>
    1.11 +      Term.all T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t
    1.12    end;
    1.13  
    1.14  (* ------------------------------------------------------------------------- *)
    1.15 @@ -765,60 +764,55 @@
    1.16      val _ = tracing "Adding axioms..."
    1.17      val axioms = Theory.all_axioms_of thy
    1.18      fun collect_this_axiom (axname, ax) axs =
    1.19 -    let
    1.20 -      val ax' = unfold_defs thy ax
    1.21 -    in
    1.22 -      if member (op aconv) axs ax' then axs
    1.23 -      else (tracing axname; collect_term_axioms (ax' :: axs, ax'))
    1.24 -    end
    1.25 -    (* Term.term list * Term.typ -> Term.term list *)
    1.26 -    and collect_sort_axioms (axs, T) =
    1.27 -    let
    1.28 -      (* string list *)
    1.29 -      val sort = (case T of
    1.30 -          TFree (_, sort) => sort
    1.31 -        | TVar (_, sort)  => sort
    1.32 -        | _               => raise REFUTE ("collect_axioms", "type " ^
    1.33 -          Syntax.string_of_typ_global thy T ^ " is not a variable"))
    1.34 -      (* obtain axioms for all superclasses *)
    1.35 -      val superclasses = sort @ (maps (Sign.super_classes thy) sort)
    1.36 -      (* merely an optimization, because 'collect_this_axiom' disallows *)
    1.37 -      (* duplicate axioms anyway:                                       *)
    1.38 -      val superclasses = distinct (op =) superclasses
    1.39 -      val class_axioms = maps (fn class => map (fn ax =>
    1.40 -        ("<" ^ class ^ ">", Thm.prop_of ax))
    1.41 -        (#axioms (AxClass.get_info thy class) handle ERROR _ => []))
    1.42 -        superclasses
    1.43 -      (* replace the (at most one) schematic type variable in each axiom *)
    1.44 -      (* by the actual type 'T'                                          *)
    1.45 -      val monomorphic_class_axioms = map (fn (axname, ax) =>
    1.46 -        (case Term.add_tvars ax [] of
    1.47 -          [] =>
    1.48 -          (axname, ax)
    1.49 -        | [(idx, S)] =>
    1.50 -          (axname, monomorphic_term (Vartab.make [(idx, (S, T))]) ax)
    1.51 -        | _ =>
    1.52 -          raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^
    1.53 -            Syntax.string_of_term_global thy ax ^
    1.54 -            ") contains more than one type variable")))
    1.55 -        class_axioms
    1.56 -    in
    1.57 -      fold collect_this_axiom monomorphic_class_axioms axs
    1.58 -    end
    1.59 -    (* Term.term list * Term.typ -> Term.term list *)
    1.60 -    and collect_type_axioms (axs, T) =
    1.61 +      let
    1.62 +        val ax' = unfold_defs thy ax
    1.63 +      in
    1.64 +        if member (op aconv) axs ax' then axs
    1.65 +        else (tracing axname; collect_term_axioms ax' (ax' :: axs))
    1.66 +      end
    1.67 +    and collect_sort_axioms T axs =
    1.68 +      let
    1.69 +        val sort =
    1.70 +          (case T of
    1.71 +            TFree (_, sort) => sort
    1.72 +          | TVar (_, sort)  => sort
    1.73 +          | _ => raise REFUTE ("collect_axioms",
    1.74 +              "type " ^ Syntax.string_of_typ_global thy T ^ " is not a variable"))
    1.75 +        (* obtain axioms for all superclasses *)
    1.76 +        val superclasses = sort @ maps (Sign.super_classes thy) sort
    1.77 +        (* merely an optimization, because 'collect_this_axiom' disallows *)
    1.78 +        (* duplicate axioms anyway:                                       *)
    1.79 +        val superclasses = distinct (op =) superclasses
    1.80 +        val class_axioms = maps (fn class => map (fn ax =>
    1.81 +          ("<" ^ class ^ ">", Thm.prop_of ax))
    1.82 +          (#axioms (AxClass.get_info thy class) handle ERROR _ => []))
    1.83 +          superclasses
    1.84 +        (* replace the (at most one) schematic type variable in each axiom *)
    1.85 +        (* by the actual type 'T'                                          *)
    1.86 +        val monomorphic_class_axioms = map (fn (axname, ax) =>
    1.87 +          (case Term.add_tvars ax [] of
    1.88 +            [] => (axname, ax)
    1.89 +          | [(idx, S)] => (axname, monomorphic_term (Vartab.make [(idx, (S, T))]) ax)
    1.90 +          | _ =>
    1.91 +            raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^
    1.92 +              Syntax.string_of_term_global thy ax ^
    1.93 +              ") contains more than one type variable")))
    1.94 +          class_axioms
    1.95 +      in
    1.96 +        fold collect_this_axiom monomorphic_class_axioms axs
    1.97 +      end
    1.98 +    and collect_type_axioms T axs =
    1.99        case T of
   1.100        (* simple types *)
   1.101 -        Type ("prop", [])      => axs
   1.102 -      | Type ("fun", [T1, T2]) => collect_type_axioms
   1.103 -        (collect_type_axioms (axs, T1), T2)
   1.104 +        Type ("prop", []) => axs
   1.105 +      | Type ("fun", [T1, T2]) => collect_type_axioms T2 (collect_type_axioms T1 axs)
   1.106        (* axiomatic type classes *)
   1.107 -      | Type ("itself", [T1])  => collect_type_axioms (axs, T1)
   1.108 -      | Type (s, Ts)           =>
   1.109 +      | Type ("itself", [T1]) => collect_type_axioms T1 axs
   1.110 +      | Type (s, Ts) =>
   1.111          (case Datatype.get_info thy s of
   1.112            SOME info =>  (* inductive datatype *)
   1.113              (* only collect relevant type axioms for the argument types *)
   1.114 -            Library.foldl collect_type_axioms (axs, Ts)
   1.115 +            fold collect_type_axioms Ts axs
   1.116          | NONE =>
   1.117            (case get_typedef thy T of
   1.118              SOME (axname, ax) =>
   1.119 @@ -826,20 +820,19 @@
   1.120            | NONE =>
   1.121              (* unspecified type, perhaps introduced with "typedecl" *)
   1.122              (* at least collect relevant type axioms for the argument types *)
   1.123 -            Library.foldl collect_type_axioms (axs, Ts)))
   1.124 -      (* axiomatic type classes *)
   1.125 -      | TFree _                => collect_sort_axioms (axs, T)
   1.126 +            fold collect_type_axioms Ts axs))
   1.127        (* axiomatic type classes *)
   1.128 -      | TVar _                 => collect_sort_axioms (axs, T)
   1.129 -    (* Term.term list * Term.term -> Term.term list *)
   1.130 -    and collect_term_axioms (axs, t) =
   1.131 +      | TFree _ => collect_sort_axioms T axs
   1.132 +      (* axiomatic type classes *)
   1.133 +      | TVar _ => collect_sort_axioms T axs
   1.134 +    and collect_term_axioms t axs =
   1.135        case t of
   1.136        (* Pure *)
   1.137          Const (@{const_name all}, _) => axs
   1.138        | Const (@{const_name "=="}, _) => axs
   1.139        | Const (@{const_name "==>"}, _) => axs
   1.140        (* axiomatic type classes *)
   1.141 -      | Const (@{const_name TYPE}, T) => collect_type_axioms (axs, T)
   1.142 +      | Const (@{const_name TYPE}, T) => collect_type_axioms T axs
   1.143        (* HOL *)
   1.144        | Const (@{const_name Trueprop}, _) => axs
   1.145        | Const (@{const_name Not}, _) => axs
   1.146 @@ -847,7 +840,7 @@
   1.147        | Const (@{const_name True}, _) => axs
   1.148        (* redundant, since 'False' is also an IDT constructor *)
   1.149        | Const (@{const_name False}, _) => axs
   1.150 -      | Const (@{const_name undefined}, T) => collect_type_axioms (axs, T)
   1.151 +      | Const (@{const_name undefined}, T) => collect_type_axioms T axs
   1.152        | Const (@{const_name The}, T) =>
   1.153          let
   1.154            val ax = specialize_type thy (@{const_name The}, T)
   1.155 @@ -862,74 +855,68 @@
   1.156          in
   1.157            collect_this_axiom ("Hilbert_Choice.someI", ax) axs
   1.158          end
   1.159 -      | Const (@{const_name All}, T) => collect_type_axioms (axs, T)
   1.160 -      | Const (@{const_name Ex}, T) => collect_type_axioms (axs, T)
   1.161 -      | Const (@{const_name "op ="}, T) => collect_type_axioms (axs, T)
   1.162 +      | Const (@{const_name All}, T) => collect_type_axioms T axs
   1.163 +      | Const (@{const_name Ex}, T) => collect_type_axioms T axs
   1.164 +      | Const (@{const_name "op ="}, T) => collect_type_axioms T axs
   1.165        | Const (@{const_name "op &"}, _) => axs
   1.166        | Const (@{const_name "op |"}, _) => axs
   1.167        | Const (@{const_name "op -->"}, _) => axs
   1.168        (* sets *)
   1.169 -      | Const (@{const_name Collect}, T) => collect_type_axioms (axs, T)
   1.170 -      | Const (@{const_name "op :"}, T) => collect_type_axioms (axs, T)
   1.171 +      | Const (@{const_name Collect}, T) => collect_type_axioms T axs
   1.172 +      | Const (@{const_name "op :"}, T) => collect_type_axioms T axs
   1.173        (* other optimizations *)
   1.174 -      | Const (@{const_name Finite_Set.card}, T) => collect_type_axioms (axs, T)
   1.175 +      | Const (@{const_name Finite_Set.card}, T) => collect_type_axioms T axs
   1.176        | Const (@{const_name Finite_Set.finite}, T) =>
   1.177 -        collect_type_axioms (axs, T)
   1.178 +        collect_type_axioms T axs
   1.179        | Const (@{const_name HOL.less}, T as Type ("fun", [Type ("nat", []),
   1.180          Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
   1.181 -          collect_type_axioms (axs, T)
   1.182 +          collect_type_axioms T axs
   1.183        | Const (@{const_name HOL.plus}, T as Type ("fun", [Type ("nat", []),
   1.184          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
   1.185 -          collect_type_axioms (axs, T)
   1.186 +          collect_type_axioms T axs
   1.187        | Const (@{const_name HOL.minus}, T as Type ("fun", [Type ("nat", []),
   1.188          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
   1.189 -          collect_type_axioms (axs, T)
   1.190 +          collect_type_axioms T axs
   1.191        | Const (@{const_name HOL.times}, T as Type ("fun", [Type ("nat", []),
   1.192          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
   1.193 -          collect_type_axioms (axs, T)
   1.194 -      | Const (@{const_name List.append}, T) => collect_type_axioms (axs, T)
   1.195 -      | Const (@{const_name lfp}, T) => collect_type_axioms (axs, T)
   1.196 -      | Const (@{const_name gfp}, T) => collect_type_axioms (axs, T)
   1.197 -      | Const (@{const_name fst}, T) => collect_type_axioms (axs, T)
   1.198 -      | Const (@{const_name snd}, T) => collect_type_axioms (axs, T)
   1.199 +          collect_type_axioms T axs
   1.200 +      | Const (@{const_name List.append}, T) => collect_type_axioms T axs
   1.201 +      | Const (@{const_name lfp}, T) => collect_type_axioms T axs
   1.202 +      | Const (@{const_name gfp}, T) => collect_type_axioms T axs
   1.203 +      | Const (@{const_name fst}, T) => collect_type_axioms T axs
   1.204 +      | Const (@{const_name snd}, T) => collect_type_axioms T axs
   1.205        (* simply-typed lambda calculus *)
   1.206        | Const (s, T) =>
   1.207            if is_const_of_class thy (s, T) then
   1.208              (* axiomatic type classes: add "OFCLASS(?'a::c, c_class)" *)
   1.209              (* and the class definition                               *)
   1.210              let
   1.211 -              val class   = Logic.class_of_const s
   1.212 +              val class = Logic.class_of_const s
   1.213                val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]), class)
   1.214 -              val ax_in   = SOME (specialize_type thy (s, T) of_class)
   1.215 +              val ax_in = SOME (specialize_type thy (s, T) of_class)
   1.216                  (* type match may fail due to sort constraints *)
   1.217                  handle Type.TYPE_MATCH => NONE
   1.218 -              val ax_1 = Option.map (fn ax => (Syntax.string_of_term_global thy ax, ax))
   1.219 -                ax_in
   1.220 -              val ax_2 = Option.map (apsnd (specialize_type thy (s, T)))
   1.221 -                (get_classdef thy class)
   1.222 +              val ax_1 = Option.map (fn ax => (Syntax.string_of_term_global thy ax, ax)) ax_in
   1.223 +              val ax_2 = Option.map (apsnd (specialize_type thy (s, T))) (get_classdef thy class)
   1.224              in
   1.225 -              collect_type_axioms (fold collect_this_axiom
   1.226 -                (map_filter I [ax_1, ax_2]) axs, T)
   1.227 +              collect_type_axioms T (fold collect_this_axiom (map_filter I [ax_1, ax_2]) axs)
   1.228              end
   1.229            else if is_IDT_constructor thy (s, T)
   1.230              orelse is_IDT_recursor thy (s, T) then
   1.231              (* only collect relevant type axioms *)
   1.232 -            collect_type_axioms (axs, T)
   1.233 +            collect_type_axioms T axs
   1.234            else
   1.235              (* other constants should have been unfolded, with some *)
   1.236              (* exceptions: e.g. Abs_xxx/Rep_xxx functions for       *)
   1.237              (* typedefs, or type-class related constants            *)
   1.238              (* only collect relevant type axioms *)
   1.239 -            collect_type_axioms (axs, T)
   1.240 -      | Free (_, T)      => collect_type_axioms (axs, T)
   1.241 -      | Var (_, T)       => collect_type_axioms (axs, T)
   1.242 -      | Bound i          => axs
   1.243 -      | Abs (_, T, body) => collect_term_axioms
   1.244 -        (collect_type_axioms (axs, T), body)
   1.245 -      | t1 $ t2          => collect_term_axioms
   1.246 -        (collect_term_axioms (axs, t1), t2)
   1.247 -    (* Term.term list *)
   1.248 -    val result = map close_form (collect_term_axioms ([], t))
   1.249 +            collect_type_axioms T axs
   1.250 +      | Free (_, T) => collect_type_axioms T axs
   1.251 +      | Var (_, T) => collect_type_axioms T axs
   1.252 +      | Bound _ => axs
   1.253 +      | Abs (_, T, body) => collect_term_axioms body (collect_type_axioms T axs)
   1.254 +      | t1 $ t2 => collect_term_axioms t2 (collect_term_axioms t1 axs)
   1.255 +    val result = map close_form (collect_term_axioms t [])
   1.256      val _ = tracing " ...done."
   1.257    in
   1.258      result
   1.259 @@ -1037,7 +1024,7 @@
   1.260      fun size_of_typ T =
   1.261        case AList.lookup (op =) sizes (string_of_typ T) of
   1.262          SOME n => n
   1.263 -      | NONE   => minsize
   1.264 +      | NONE => minsize
   1.265    in
   1.266      map (fn T => (T, size_of_typ T)) xs
   1.267    end;
   1.268 @@ -1091,13 +1078,13 @@
   1.269      case next (maxsize-minsize) 0 0 diffs of
   1.270        SOME diffs' =>
   1.271        (* merge with those types for which the size is fixed *)
   1.272 -      SOME (snd (Library.foldl_map (fn (ds, (T, _)) =>
   1.273 +      SOME (fst (fold_map (fn (T, _) => fn ds =>
   1.274          case AList.lookup (op =) sizes (string_of_typ T) of
   1.275          (* return the fixed size *)
   1.276 -          SOME n => (ds, (T, n))
   1.277 +          SOME n => ((T, n), ds)
   1.278          (* consume the head of 'ds', add 'minsize' *)
   1.279 -        | NONE   => (tl ds, (T, minsize + hd ds)))
   1.280 -        (diffs', xs)))
   1.281 +        | NONE   => ((T, minsize + hd ds), tl ds))
   1.282 +        xs diffs'))
   1.283      | NONE =>
   1.284        NONE
   1.285    end;
   1.286 @@ -1154,8 +1141,7 @@
   1.287        val _      = tracing ("Unfolded term: " ^ Syntax.string_of_term_global thy u)
   1.288        val axioms = collect_axioms thy u
   1.289        (* Term.typ list *)
   1.290 -      val types = Library.foldl (fn (acc, t') =>
   1.291 -        uncurry (union (op =)) (acc, (ground_types thy t'))) ([], u :: axioms)
   1.292 +      val types = fold (union (op =) o ground_types thy) (u :: axioms) []
   1.293        val _     = tracing ("Ground types: "
   1.294          ^ (if null types then "none."
   1.295             else commas (map (Syntax.string_of_typ_global thy) types)))
   1.296 @@ -1194,15 +1180,15 @@
   1.297          val _ = tracing ("Translating term (sizes: "
   1.298            ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...")
   1.299          (* translate 'u' and all axioms *)
   1.300 -        val ((model, args), intrs) = Library.foldl_map (fn ((m, a), t') =>
   1.301 +        val (intrs, (model, args)) = fold_map (fn t' => fn (m, a) =>
   1.302            let
   1.303              val (i, m', a') = interpret thy m a t'
   1.304            in
   1.305              (* set 'def_eq' to 'true' *)
   1.306 -            ((m', {maxvars = #maxvars a', def_eq = true,
   1.307 +            (i, (m', {maxvars = #maxvars a', def_eq = true,
   1.308                next_idx = #next_idx a', bounds = #bounds a',
   1.309 -              wellformed = #wellformed a'}), i)
   1.310 -          end) ((init_model, init_args), u :: axioms)
   1.311 +              wellformed = #wellformed a'}))
   1.312 +          end) (u :: axioms) (init_model, init_args)
   1.313          (* make 'u' either true or false, and make all axioms true, and *)
   1.314          (* add the well-formedness side condition                       *)
   1.315          val fm_u  = (if negate then toFalse else toTrue) (hd intrs)
   1.316 @@ -1306,10 +1292,9 @@
   1.317      (* (Term.indexname * Term.typ) list *)
   1.318      val vars = sort_wrt (fst o fst) (map dest_Var (OldTerm.term_vars t))
   1.319      (* Term.term *)
   1.320 -    val ex_closure = Library.foldl (fn (t', ((x, i), T)) =>
   1.321 -      (HOLogic.exists_const T) $
   1.322 -        Abs (x, T, abstract_over (Var ((x, i), T), t')))
   1.323 -      (t, vars)
   1.324 +    val ex_closure = fold (fn ((x, i), T) => fn t' =>
   1.325 +      HOLogic.exists_const T $
   1.326 +        Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t
   1.327      (* Note: If 't' is of type 'propT' (rather than 'boolT'), applying   *)
   1.328      (* 'HOLogic.exists_const' is not type-correct.  However, this is not *)
   1.329      (* really a problem as long as 'find_model' still interprets the     *)
   1.330 @@ -1730,8 +1715,8 @@
   1.331            (* create all constants of type 'T' *)
   1.332            val constants = make_constants thy model T
   1.333            (* interpret the 'body' separately for each constant *)
   1.334 -          val ((model', args'), bodies) = Library.foldl_map
   1.335 -            (fn ((m, a), c) =>
   1.336 +          val (bodies, (model', args')) = fold_map
   1.337 +            (fn c => fn (m, a) =>
   1.338                let
   1.339                  (* add 'c' to 'bounds' *)
   1.340                  val (i', m', a') = interpret thy m {maxvars = #maxvars a,
   1.341 @@ -1740,15 +1725,15 @@
   1.342                in
   1.343                  (* keep the new model m' and 'next_idx' and 'wellformed', *)
   1.344                  (* but use old 'bounds'                                   *)
   1.345 -                ((m', {maxvars = maxvars, def_eq = def_eq,
   1.346 +                (i', (m', {maxvars = maxvars, def_eq = def_eq,
   1.347                    next_idx = #next_idx a', bounds = bounds,
   1.348 -                  wellformed = #wellformed a'}), i')
   1.349 +                  wellformed = #wellformed a'}))
   1.350                end)
   1.351 -            ((model, args), constants)
   1.352 +            constants (model, args)
   1.353          in
   1.354            SOME (Node bodies, model', args')
   1.355          end
   1.356 -      | t1 $ t2          =>
   1.357 +      | t1 $ t2 =>
   1.358          let
   1.359            (* interpret 't1' and 't2' separately *)
   1.360            val (intr1, model1, args1) = interpret thy model args t1
   1.361 @@ -2209,14 +2194,14 @@
   1.362                        Node (replicate size (make_undef ds))
   1.363                      end
   1.364                    (* returns the interpretation for a constructor *)
   1.365 -                  fun make_constr (offset, []) =
   1.366 -                    if offset<total then
   1.367 -                      (offset+1, Leaf ((replicate offset False) @ True ::
   1.368 -                        (replicate (total-offset-1) False)))
   1.369 +                  fun make_constr [] offset =
   1.370 +                    if offset < total then
   1.371 +                      (Leaf (replicate offset False @ True ::
   1.372 +                        (replicate (total - offset - 1) False)), offset + 1)
   1.373                      else
   1.374                        raise REFUTE ("IDT_constructor_interpreter",
   1.375                          "offset >= total")
   1.376 -                    | make_constr (offset, d::ds) =
   1.377 +                    | make_constr (d::ds) offset =
   1.378                      let
   1.379                        (* Term.typ *)
   1.380                        val dT = typ_of_dtyp descr typ_assoc d
   1.381 @@ -2225,8 +2210,8 @@
   1.382                        (* for the IDT)                                     *)
   1.383                        val terms' = canonical_terms typs' dT
   1.384                        (* sanity check *)
   1.385 -                      val _ = if length terms' <>
   1.386 -                        size_of_type thy (typs', []) dT
   1.387 +                      val _ =
   1.388 +                        if length terms' <> size_of_type thy (typs', []) dT
   1.389                          then
   1.390                            raise REFUTE ("IDT_constructor_interpreter",
   1.391                              "length of terms' is not equal to old size")
   1.392 @@ -2236,46 +2221,52 @@
   1.393                        (* for the IDT)                                     *)
   1.394                        val terms = canonical_terms typs dT
   1.395                        (* sanity check *)
   1.396 -                      val _ = if length terms <> size_of_type thy (typs, []) dT
   1.397 +                      val _ =
   1.398 +                        if length terms <> size_of_type thy (typs, []) dT
   1.399                          then
   1.400                            raise REFUTE ("IDT_constructor_interpreter",
   1.401                              "length of terms is not equal to current size")
   1.402                          else ()
   1.403                        (* sanity check *)
   1.404 -                      val _ = if length terms < length terms' then
   1.405 +                      val _ =
   1.406 +                        if length terms < length terms' then
   1.407                            raise REFUTE ("IDT_constructor_interpreter",
   1.408                              "current size is less than old size")
   1.409                          else ()
   1.410                        (* sanity check: every element of terms' must also be *)
   1.411                        (*               present in terms                     *)
   1.412 -                      val _ = if List.all (member op= terms) terms' then ()
   1.413 +                      val _ =
   1.414 +                        if List.all (member (op =) terms) terms' then ()
   1.415                          else
   1.416                            raise REFUTE ("IDT_constructor_interpreter",
   1.417                              "element has disappeared")
   1.418                        (* sanity check: the order on elements of terms' is    *)
   1.419                        (*               the same in terms, for those elements *)
   1.420 -                      val _ = let
   1.421 +                      val _ =
   1.422 +                        let
   1.423                            fun search (x::xs) (y::ys) =
   1.424 -                            if x = y then search xs ys else search (x::xs) ys
   1.425 +                                if x = y then search xs ys else search (x::xs) ys
   1.426                              | search (x::xs) [] =
   1.427 -                            raise REFUTE ("IDT_constructor_interpreter",
   1.428 -                              "element order not preserved")
   1.429 +                                raise REFUTE ("IDT_constructor_interpreter",
   1.430 +                                  "element order not preserved")
   1.431                              | search [] _ = ()
   1.432                          in  search terms' terms  end
   1.433                        (* int * interpretation list *)
   1.434 -                      val (new_offset, intrs) = Library.foldl_map (fn (off, t_elem) =>
   1.435 -                        (* if 't_elem' existed at the previous depth,    *)
   1.436 -                        (* proceed recursively, otherwise map the entire *)
   1.437 -                        (* subtree to "undefined"                        *)
   1.438 -                        if t_elem mem terms' then
   1.439 -                          make_constr (off, ds)
   1.440 -                        else
   1.441 -                          (off, make_undef ds)) (offset, terms)
   1.442 +                      val (intrs, new_offset) =
   1.443 +                        fold_map (fn t_elem => fn off =>
   1.444 +                          (* if 't_elem' existed at the previous depth,    *)
   1.445 +                          (* proceed recursively, otherwise map the entire *)
   1.446 +                          (* subtree to "undefined"                        *)
   1.447 +                          if t_elem mem terms' then
   1.448 +                            make_constr ds off
   1.449 +                          else
   1.450 +                            (make_undef ds, off))
   1.451 +                        terms offset
   1.452                      in
   1.453 -                      (new_offset, Node intrs)
   1.454 +                      (Node intrs, new_offset)
   1.455                      end
   1.456                  in
   1.457 -                  SOME (snd (make_constr (offset, ctypes)), model, args)
   1.458 +                  SOME (fst (make_constr ctypes offset), model, args)
   1.459                  end
   1.460              end
   1.461            | NONE =>  (* body type is not an inductive datatype *)
   1.462 @@ -2329,12 +2320,12 @@
   1.463                else  (* mconstrs_count = length params *)
   1.464                  let
   1.465                    (* interpret each parameter separately *)
   1.466 -                  val ((model', args'), p_intrs) = Library.foldl_map (fn ((m, a), p) =>
   1.467 +                  val (p_intrs, (model', args')) = fold_map (fn p => fn (m, a) =>
   1.468                      let
   1.469                        val (i, m', a') = interpret thy m a p
   1.470                      in
   1.471 -                      ((m', a'), i)
   1.472 -                    end) ((model, args), params)
   1.473 +                      (i, (m', a'))
   1.474 +                    end) params (model, args)
   1.475                    val (typs, _) = model'
   1.476                    (* 'index' is /not/ necessarily the index of the IDT that *)
   1.477                    (* the recursion operator is associated with, but merely  *)
   1.478 @@ -2437,14 +2428,14 @@
   1.479                      end) descr
   1.480                    (* associate constructors with corresponding parameters *)
   1.481                    (* (int * (interpretation * interpretation) list) list *)
   1.482 -                  val (p_intrs', mc_p_intrs) = Library.foldl_map
   1.483 -                    (fn (p_intrs', (idx, c_intrs)) =>
   1.484 +                  val (mc_p_intrs, p_intrs') = fold_map
   1.485 +                    (fn (idx, c_intrs) => fn p_intrs' =>
   1.486                        let
   1.487                          val len = length c_intrs
   1.488                        in
   1.489 -                        (List.drop (p_intrs', len),
   1.490 -                          (idx, c_intrs ~~ List.take (p_intrs', len)))
   1.491 -                      end) (p_intrs, mc_intrs)
   1.492 +                        ((idx, c_intrs ~~ List.take (p_intrs', len)),
   1.493 +                          List.drop (p_intrs', len))
   1.494 +                      end) mc_intrs p_intrs
   1.495                    (* sanity check: no 'p_intr' may be left afterwards *)
   1.496                    val _ = if p_intrs' <> [] then
   1.497                        raise REFUTE ("IDT_recursion_interpreter",
   1.498 @@ -2669,15 +2660,15 @@
   1.499        let
   1.500          (* interpretation -> int *)
   1.501          fun number_of_elements (Node xs) =
   1.502 -          Library.foldl (fn (n, x) =>
   1.503 -            if x=TT then
   1.504 -              n+1
   1.505 -            else if x=FF then
   1.506 -              n
   1.507 -            else
   1.508 -              raise REFUTE ("Finite_Set_card_interpreter",
   1.509 -                "interpretation for set type does not yield a Boolean"))
   1.510 -            (0, xs)
   1.511 +            fold (fn x => fn n =>
   1.512 +              if x = TT then
   1.513 +                n + 1
   1.514 +              else if x = FF then
   1.515 +                n
   1.516 +              else
   1.517 +                raise REFUTE ("Finite_Set_card_interpreter",
   1.518 +                  "interpretation for set type does not yield a Boolean"))
   1.519 +              xs 0
   1.520            | number_of_elements (Leaf _) =
   1.521            raise REFUTE ("Finite_Set_card_interpreter",
   1.522              "interpretation for set type is a leaf")
   1.523 @@ -2882,7 +2873,7 @@
   1.524          (* of width 'size_elem' and depth 'length_list' (with 'size_list'    *)
   1.525          (* nodes total)                                                      *)
   1.526          (* (int * (int * int)) list *)
   1.527 -        val (_, lenoff_lists) = Library.foldl_map (fn ((offsets, off), elem) =>
   1.528 +        val (lenoff_lists, _) = fold_map (fn elem => fn (offsets, off) =>
   1.529            (* corresponds to a pre-order traversal of the tree *)
   1.530            let
   1.531              val len = length offsets
   1.532 @@ -2891,10 +2882,10 @@
   1.533            in
   1.534              if len < list_length then
   1.535                (* go to first child node *)
   1.536 -              ((off :: offsets, off * size_elem), assoc)
   1.537 +              (assoc, (off :: offsets, off * size_elem))
   1.538              else if off mod size_elem < size_elem - 1 then
   1.539                (* go to next sibling node *)
   1.540 -              ((offsets, off + 1), assoc)
   1.541 +              (assoc, (offsets, off + 1))
   1.542              else
   1.543                (* go back up the stack until we find a level where we can go *)
   1.544                (* to the next sibling node                                   *)
   1.545 @@ -2906,12 +2897,12 @@
   1.546                    [] =>
   1.547                    (* we're at the last node in the tree; the next value *)
   1.548                    (* won't be used anyway                               *)
   1.549 -                  (([], 0), assoc)
   1.550 +                  (assoc, ([], 0))
   1.551                  | off'::offs' =>
   1.552                    (* go to next sibling node *)
   1.553 -                  ((offs', off' + 1), assoc)
   1.554 +                  (assoc, (offs', off' + 1))
   1.555                end
   1.556 -          end) (([], 0), elements)
   1.557 +          end) elements ([], 0)
   1.558          (* we also need the reverse association (from length/offset to *)
   1.559          (* index)                                                      *)
   1.560          val lenoff'_lists = map Library.swap lenoff_lists
   1.561 @@ -3248,7 +3239,7 @@
   1.562                  print thy (typs, []) dT (List.nth (consts, n)) assignment
   1.563                end) (cargs ~~ args)
   1.564            in
   1.565 -            SOME (Library.foldl op$ (cTerm, argsTerms))
   1.566 +            SOME (list_comb (cTerm, argsTerms))
   1.567            end
   1.568          end
   1.569        | NONE =>  (* not an inductive datatype *)