tuned fold on terms;
authorwenzelm
Fri Jul 15 15:44:15 2005 +0200 (2005-07-15 ago)
changeset 168617446b4be013b
parent 16860 43abdba4da5c
child 16862 6cb403552988
tuned fold on terms;
src/HOL/Library/EfficientNat.thy
src/HOL/Orderings.thy
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/inductive_realizer.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/proof_context.ML
src/Pure/Proof/proof_rewrite_rules.ML
src/Pure/drule.ML
src/Pure/meta_simplifier.ML
     1.1 --- a/src/HOL/Library/EfficientNat.thy	Fri Jul 15 15:44:11 2005 +0200
     1.2 +++ b/src/HOL/Library/EfficientNat.thy	Fri Jul 15 15:44:15 2005 +0200
     1.3 @@ -110,10 +110,10 @@
     1.4  fun remove_suc thy thms =
     1.5    let
     1.6      val Suc_if_eq' = Thm.transfer thy Suc_if_eq;
     1.7 -    val ctzero = cterm_of (sign_of Main.thy) HOLogic.zero;
     1.8 +    val ctzero = cterm_of Main.thy HOLogic.zero;
     1.9      val vname = variant (map fst
    1.10 -      (Library.foldl add_term_varnames ([], map prop_of thms))) "x";
    1.11 -    val cv = cterm_of (sign_of Main.thy) (Var ((vname, 0), HOLogic.natT));
    1.12 +      (fold (add_term_varnames o Thm.full_prop_of) thms [])) "x";
    1.13 +    val cv = cterm_of Main.thy (Var ((vname, 0), HOLogic.natT));
    1.14      fun lhs_of th = snd (Thm.dest_comb
    1.15        (fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))))));
    1.16      fun rhs_of th = snd (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))));
    1.17 @@ -172,7 +172,7 @@
    1.18    let
    1.19      val Suc_clause' = Thm.transfer thy Suc_clause;
    1.20      val vname = variant (map fst
    1.21 -      (Library.foldl add_term_varnames ([], map prop_of thms))) "x";
    1.22 +      (fold (add_term_varnames o Thm.full_prop_of) thms [])) "x";
    1.23      fun find_var (t as Const ("Suc", _) $ (v as Var _)) = SOME (t, v)
    1.24        | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
    1.25        | find_var _ = NONE;
    1.26 @@ -184,7 +184,7 @@
    1.27        NONE => thms
    1.28      | SOME ((th, th'), (Sucv, v)) =>
    1.29          let
    1.30 -          val cert = cterm_of (sign_of_thm th);
    1.31 +          val cert = cterm_of (Thm.theory_of_thm th);
    1.32            val th'' = ObjectLogic.rulify (Thm.implies_elim
    1.33              (Drule.fconv_rule (Thm.beta_conversion true)
    1.34                (Drule.instantiate' []
     2.1 --- a/src/HOL/Orderings.thy	Fri Jul 15 15:44:11 2005 +0200
     2.2 +++ b/src/HOL/Orderings.thy	Fri Jul 15 15:44:15 2005 +0200
     2.3 @@ -545,7 +545,7 @@
     2.4  print_translation {*
     2.5  let
     2.6    fun mk v v' q n P =
     2.7 -    if v=v' andalso not(v  mem (map fst (Term.add_frees([],n))))
     2.8 +    if v=v' andalso not (v mem (map fst (Term.add_frees n [])))
     2.9      then Syntax.const q $ Syntax.mark_bound v' $ n $ P else raise Match;
    2.10    fun all_tr' [Const ("_bound",_) $ Free (v,_),
    2.11                 Const("op -->",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
     3.1 --- a/src/HOL/Tools/inductive_codegen.ML	Fri Jul 15 15:44:11 2005 +0200
     3.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Fri Jul 15 15:44:15 2005 +0200
     3.3 @@ -180,8 +180,8 @@
     3.4  val terms_vs = distinct o List.concat o (map term_vs);
     3.5  
     3.6  (** collect all Vars in a term (with duplicates!) **)
     3.7 -fun term_vTs t = map (apfst fst o dest_Var)
     3.8 -  (List.filter is_Var (foldl_aterms (op :: o Library.swap) ([], t)));
     3.9 +fun term_vTs tm =
    3.10 +  fold_aterms (fn Var ((x, _), T) => cons (x, T) | _ => I) tm [];
    3.11  
    3.12  fun get_args _ _ [] = ([], [])
    3.13    | get_args is i (x::xs) = (if i mem is then apfst else apsnd) (cons x)
     4.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Jul 15 15:44:11 2005 +0200
     4.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Jul 15 15:44:15 2005 +0200
     4.3 @@ -178,15 +178,14 @@
     4.4  fun unify_consts thy cs intr_ts =
     4.5    (let
     4.6      val tsig = Sign.tsig_of thy;
     4.7 -    val add_term_consts_2 =
     4.8 -      foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs);
     4.9 +    val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
    4.10      fun varify (t, (i, ts)) =
    4.11        let val t' = map_term_types (incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
    4.12        in (maxidx_of_term t', t'::ts) end;
    4.13      val (i, cs') = foldr varify (~1, []) cs;
    4.14      val (i', intr_ts') = foldr varify (i, []) intr_ts;
    4.15 -    val rec_consts = Library.foldl add_term_consts_2 ([], cs');
    4.16 -    val intr_consts = Library.foldl add_term_consts_2 ([], intr_ts');
    4.17 +    val rec_consts = fold add_term_consts_2 cs' [];
    4.18 +    val intr_consts = fold add_term_consts_2 intr_ts' [];
    4.19      fun unify (env, (cname, cT)) =
    4.20        let val consts = map snd (List.filter (fn c => fst c = cname) intr_consts)
    4.21        in Library.foldl (fn ((env', j'), Tp) => (Type.unify tsig (env', j') Tp))
     5.1 --- a/src/HOL/Tools/inductive_realizer.ML	Fri Jul 15 15:44:11 2005 +0200
     5.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Fri Jul 15 15:44:15 2005 +0200
     5.3 @@ -60,7 +60,7 @@
     5.4      val params = map dest_Var ts;
     5.5      val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs);
     5.6      fun constr_of_intr intr = (Sign.base_name (Thm.name_of_thm intr),
     5.7 -      map (Type.unvarifyT o snd) (rev (Term.add_vars ([], prop_of intr)) \\ params) @
     5.8 +      map (Type.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
     5.9          filter_out (equal Extraction.nullT) (map
    5.10            (Type.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
    5.11              NoSyn);
    5.12 @@ -137,7 +137,7 @@
    5.13      val args = map (Free o apfst fst o dest_Var)
    5.14        (add_term_vars (prop_of intr, []) \\ map Var params);
    5.15      val args' = map (Free o apfst fst)
    5.16 -      (Term.add_vars ([], prop_of intr) \\ params);
    5.17 +      (Term.add_vars (prop_of intr) [] \\ params);
    5.18      val rule' = strip_all rule;
    5.19      val conclT = Extraction.etype_of thy vs [] (Logic.strip_imp_concl rule');
    5.20      val used = map (fst o dest_Free) args;
    5.21 @@ -213,7 +213,7 @@
    5.22            HOLogic.unitT --> body_type (fastype_of (hd fs))) :: fs
    5.23          else fs)
    5.24        end) (intrs, (premss ~~ dummies))));
    5.25 -    val frees = Library.foldl Term.add_frees ([], fs);
    5.26 +    val frees = fold Term.add_frees fs [];
    5.27      val Ts = map fastype_of fs;
    5.28      val rlzs = List.mapPartial (fn (a, concl) =>
    5.29        let val T = Extraction.etype_of thy vs [] concl
    5.30 @@ -250,9 +250,9 @@
    5.31    let
    5.32      val prems = prems_of rule ~~ prems_of rrule;
    5.33      val rvs = map fst (relevant_vars (prop_of rule));
    5.34 -    val xs = rev (Term.add_vars ([], prop_of rule));
    5.35 +    val xs = rev (Term.add_vars (prop_of rule) []);
    5.36      val vs1 = map Var (filter_out (fn ((a, _), _) => a mem rvs) xs);
    5.37 -    val rlzvs = rev (Term.add_vars ([], prop_of rrule));
    5.38 +    val rlzvs = rev (Term.add_vars (prop_of rrule) []);
    5.39      val vs2 = map (fn (ixn, _) => Var (ixn, valOf (assoc (rlzvs, ixn)))) xs;
    5.40      val rs = gen_rems (op = o pairself fst) (rlzvs, xs);
    5.41  
    5.42 @@ -327,7 +327,7 @@
    5.43      val rintrs = map (fn (intr, c) => Pattern.eta_contract
    5.44        (Extraction.realizes_of thy2 vs
    5.45          c (prop_of (forall_intr_list (map (cterm_of (sign_of thy2) o Var)
    5.46 -          (rev (Term.add_vars ([], prop_of intr)) \\ params')) intr))))
    5.47 +          (rev (Term.add_vars (prop_of intr) []) \\ params')) intr))))
    5.48              (intrs ~~ List.concat constrss);
    5.49      val rlzsets = distinct (map (fn rintr => snd (HOLogic.dest_mem
    5.50        (HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr)))) rintrs);
    5.51 @@ -384,11 +384,11 @@
    5.52          val (prem :: prems) = prems_of elim;
    5.53          fun reorder1 (p, intr) =
    5.54            Library.foldl (fn (t, ((s, _), T)) => all T $ lambda (Free (s, T)) t)
    5.55 -            (strip_all p, Term.add_vars ([], prop_of intr) \\ params');
    5.56 +            (strip_all p, Term.add_vars (prop_of intr) [] \\ params');
    5.57          fun reorder2 (intr, i) =
    5.58            let
    5.59              val fs1 = term_vars (prop_of intr) \\ params;
    5.60 -            val fs2 = Term.add_vars ([], prop_of intr) \\ params'
    5.61 +            val fs2 = Term.add_vars (prop_of intr) [] \\ params'
    5.62            in Library.foldl (fn (t, x) => lambda (Var x) t)
    5.63              (list_comb (Bound (i + length fs1), fs1), fs2)
    5.64            end;
    5.65 @@ -429,7 +429,7 @@
    5.66      val thy5 = Extraction.add_realizers_i
    5.67        (map (mk_realizer thy4 vs params')
    5.68           (map (fn ((rule, rrule), c) => ((rule, rrule), list_comb (c,
    5.69 -            map Var (rev (Term.add_vars ([], prop_of rule)) \\ params')))) 
    5.70 +            map Var (rev (Term.add_vars (prop_of rule) []) \\ params')))) 
    5.71                (List.concat (map snd rss) ~~ rintr_thms ~~ List.concat constrss))) thy4;
    5.72      val elimps = List.mapPartial (fn (s, intrs) => if s mem rsets then
    5.73          Option.map (rpair intrs) (find_first (fn (thm, _) =>
     6.1 --- a/src/Pure/Isar/locale.ML	Fri Jul 15 15:44:11 2005 +0200
     6.2 +++ b/src/Pure/Isar/locale.ML	Fri Jul 15 15:44:15 2005 +0200
     6.3 @@ -623,7 +623,7 @@
     6.4    let
     6.5      val {thy, hyps, prop, maxidx, ...} = Thm.rep_thm th;
     6.6      val cert = Thm.cterm_of thy;
     6.7 -    val (xs, Ts) = Library.split_list (Library.foldl Term.add_frees ([], prop :: hyps));
     6.8 +    val (xs, Ts) = Library.split_list (fold Term.add_frees (prop :: hyps) []);
     6.9      val xs' = map (rename ren) xs;
    6.10      fun cert_frees names = map (cert o Free) (names ~~ Ts);
    6.11      fun cert_vars names = map (cert o Var o apfst (rpair (maxidx + 1))) (names ~~ Ts);
    6.12 @@ -705,7 +705,7 @@
    6.13  
    6.14  fun frozen_tvars ctxt Ts =
    6.15    let
    6.16 -    val tvars = rev (Library.foldl Term.add_tvarsT ([], Ts));
    6.17 +    val tvars = rev (fold Term.add_tvarsT Ts []);
    6.18      val tfrees = map TFree
    6.19        (Term.invent_names (ProofContext.used_types ctxt) "'a" (length tvars) ~~ map #2 tvars);
    6.20    in map (fn ((x, S), y) => (x, (S, y))) (tvars ~~ tfrees) end;
    6.21 @@ -951,7 +951,7 @@
    6.22           elemss;
    6.23      fun inst_ax th = let
    6.24           val {hyps, prop, ...} = Thm.rep_thm th;
    6.25 -         val ps = map (apsnd SOME) (Library.foldl Term.add_frees ([], prop :: hyps));
    6.26 +         val ps = map (apsnd SOME) (fold Term.add_frees (prop :: hyps) []);
    6.27           val [env] = unify_parms ctxt all_params [ps];
    6.28           val th' = inst_thm ctxt env th;
    6.29         in th' end;
    6.30 @@ -1208,7 +1208,7 @@
    6.31        err "Attempt to define previously specified variable");
    6.32      conditional (exists (fn (Free (y', _), _) => y = y' | _ => false) env) (fn () =>
    6.33        err "Attempt to redefine variable");
    6.34 -    (Term.add_frees (xs, b'), (Free (y, T), b') :: env, th :: ths)
    6.35 +    (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths)
    6.36    end;
    6.37  
    6.38  (* CB: for finish_elems (Int and Ext) *)
    6.39 @@ -1222,7 +1222,7 @@
    6.40          val spec' =
    6.41            if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
    6.42            else ((exts, exts'), (ints @ ts, ints' @ ts'));
    6.43 -      in (spec', (Library.foldl Term.add_frees (xs, ts'), env, defs)) end
    6.44 +      in (spec', (fold Term.add_frees ts' xs, env, defs)) end
    6.45    | eval_text ctxt (id, _) _ ((spec, binds), Defines defs) =
    6.46        (spec, Library.foldl (bind_def ctxt id) (binds, map (#1 o #2) defs))
    6.47    | eval_text _ _ _ (text, Notes _) = text;
    6.48 @@ -1234,7 +1234,7 @@
    6.49        let
    6.50          fun close_frees t =
    6.51            let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1)
    6.52 -            (Term.add_frees ([], t)))
    6.53 +            (Term.add_frees t []))
    6.54            in Term.list_all_free (frees, t) end;
    6.55  
    6.56          fun no_binds [] = []
    6.57 @@ -1966,7 +1966,7 @@
    6.58      fun sorts (a, i) = assoc (tvars, (a, i));
    6.59      val (vs, vinst) = read_terms thy_ctxt sorts used given_insts;
    6.60      val vars = foldl Term.add_term_tvar_ixns [] vs \\ map fst tvars;
    6.61 -    val vars' = Library.foldl Term.add_term_varnames (vars, vs);
    6.62 +    val vars' = fold Term.add_term_varnames vs vars;
    6.63      val _ = if null vars' then ()
    6.64           else error ("Illegal schematic variable(s) in instantiation: " ^
    6.65             commas_quote (map Syntax.string_of_vname vars'));
     7.1 --- a/src/Pure/Isar/proof_context.ML	Fri Jul 15 15:44:11 2005 +0200
     7.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Jul 15 15:44:15 2005 +0200
     7.3 @@ -565,28 +565,26 @@
     7.4  
     7.5  local
     7.6  
     7.7 -val ins_types = foldl_aterms
     7.8 -  (fn (types, Free (x, T)) => Vartab.update (((x, ~1), T), types)
     7.9 -    | (types, Var v) => Vartab.update (v, types)
    7.10 -    | (types, _) => types);
    7.11 +val ins_types = fold_aterms
    7.12 +  (fn Free (x, T) => curry Vartab.update ((x, ~1), T)
    7.13 +    | Var v => curry Vartab.update v
    7.14 +    | _ => I);
    7.15  
    7.16 -val ins_sorts = foldl_types (foldl_atyps
    7.17 -  (fn (sorts, TFree (x, S)) => Vartab.update (((x, ~1), S), sorts)
    7.18 -    | (sorts, TVar v) => Vartab.update (v, sorts)
    7.19 -    | (sorts, _) => sorts));
    7.20 +val ins_sorts = fold_types (fold_atyps
    7.21 +  (fn TFree (x, S) => curry Vartab.update ((x, ~1), S)
    7.22 +    | TVar v => curry Vartab.update v
    7.23 +    | _ => I));
    7.24  
    7.25 -val ins_used = foldl_term_types (fn t => foldl_atyps
    7.26 -  (fn (used, TFree (x, _)) => x ins_string used
    7.27 -    | (used, _) => used));
    7.28 +val ins_used = fold_term_types (fn t =>
    7.29 +  fold_atyps (fn TFree (x, _) => insert (op =) x | _ => I));
    7.30  
    7.31 -val ins_occs = foldl_term_types (fn t => foldl_atyps
    7.32 -  (fn (tab, TFree (x, _)) => Symtab.update_multi ((x, t), tab) | (tab, _) => tab));
    7.33 +val ins_occs = fold_term_types (fn t =>
    7.34 +  fold_atyps (fn TFree (x, _) => curry Symtab.update_multi (x, t) | _ => I));
    7.35  
    7.36 -fun ins_skolem def_ty = foldr
    7.37 -  (fn ((x, x'), types) =>
    7.38 -    (case def_ty x' of
    7.39 -      SOME T => Vartab.update (((x, ~1), T), types)
    7.40 -    | NONE => types));
    7.41 +fun ins_skolem def_ty = fold_rev (fn (x, x') =>
    7.42 +  (case def_ty x' of
    7.43 +    SOME T => curry Vartab.update ((x, ~1), T)
    7.44 +  | NONE => I));
    7.45  
    7.46  fun map_defaults f = map_context (fn (syntax, asms, binds, thms, cases, defs) =>
    7.47    (syntax, asms, binds, thms, cases, f defs));
    7.48 @@ -595,17 +593,17 @@
    7.49  
    7.50  fun declare_term_syntax t ctxt =
    7.51    ctxt
    7.52 -  |> map_defaults (fn (types, sorts, used, occ) => (ins_types (types, t), sorts, used, occ))
    7.53 -  |> map_defaults (fn (types, sorts, used, occ) => (types, ins_sorts (sorts, t), used, occ))
    7.54 -  |> map_defaults (fn (types, sorts, used, occ) => (types, sorts, ins_used (used, t), occ));
    7.55 +  |> map_defaults (fn (types, sorts, used, occ) => (ins_types t types, sorts, used, occ))
    7.56 +  |> map_defaults (fn (types, sorts, used, occ) => (types, ins_sorts t sorts, used, occ))
    7.57 +  |> map_defaults (fn (types, sorts, used, occ) => (types, sorts, ins_used t used, occ));
    7.58  
    7.59  fun declare_term t ctxt =
    7.60    ctxt
    7.61    |> declare_term_syntax t
    7.62 -  |> map_defaults (fn (types, sorts, used, occ) => (types, sorts, used, ins_occs (occ, t)))
    7.63 +  |> map_defaults (fn (types, sorts, used, occ) => (types, sorts, used, ins_occs t occ))
    7.64    |> map_defaults (fn (types, sorts, used, occ) =>
    7.65 -      (ins_skolem (fn x =>
    7.66 -        Vartab.lookup (types, (x, ~1))) types (fixes_of ctxt), sorts, used, occ));
    7.67 +      (ins_skolem (fn x => Vartab.lookup (types, (x, ~1))) (fixes_of ctxt) types,
    7.68 +        sorts, used, occ));
    7.69  
    7.70  end;
    7.71  
    7.72 @@ -676,10 +674,10 @@
    7.73  
    7.74  (** export theorems **)
    7.75  
    7.76 -fun get_free x (NONE, t as Free (y, _)) = if x = y then SOME t else NONE
    7.77 -  | get_free _ (opt, _) = opt;
    7.78 +fun get_free x (t as Free (y, _)) NONE = if x = y then SOME t else NONE
    7.79 +  | get_free _ _ opt = opt;
    7.80  
    7.81 -fun find_free t x = foldl_aterms (get_free x) (NONE, t);
    7.82 +fun find_free t x = fold_aterms (get_free x) t NONE;
    7.83  
    7.84  fun export_view view is_goal inner outer =
    7.85    let
    7.86 @@ -1177,7 +1175,7 @@
    7.87  
    7.88  fun fix_frees ts ctxt =
    7.89    let
    7.90 -    val frees = Library.foldl Term.add_frees ([], ts);
    7.91 +    val frees = fold Term.add_frees ts [];
    7.92      fun new (x, T) = if is_fixed ctxt x then NONE else SOME ([x], SOME T);
    7.93    in fix_direct false (rev (List.mapPartial new frees)) ctxt end;
    7.94  
     8.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Jul 15 15:44:11 2005 +0200
     8.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Jul 15 15:44:15 2005 +0200
     8.3 @@ -210,8 +210,7 @@
     8.4  
     8.5  (**** eliminate definitions in proof ****)
     8.6  
     8.7 -fun vars_of t = rev (fold_aterms
     8.8 -  (fn v as Var _ => (fn vs => v ins vs) | _ => I) t []);
     8.9 +fun vars_of t = rev (fold_aterms (fn v as Var _ => insert (op =) v | _ => I) t []);
    8.10  
    8.11  fun insert_refl defs Ts (prf1 %% prf2) =
    8.12        insert_refl defs Ts prf1 %% insert_refl defs Ts prf2
     9.1 --- a/src/Pure/drule.ML	Fri Jul 15 15:44:11 2005 +0200
     9.2 +++ b/src/Pure/drule.ML	Fri Jul 15 15:44:15 2005 +0200
     9.3 @@ -958,8 +958,8 @@
     9.4  
     9.5  (* vars in left-to-right order *)
     9.6  
     9.7 -fun tvars_of_terms ts = rev (Library.foldl Term.add_tvars ([], ts));
     9.8 -fun vars_of_terms ts = rev (Library.foldl Term.add_vars ([], ts));
     9.9 +fun tvars_of_terms ts = rev (fold Term.add_tvars ts []);
    9.10 +fun vars_of_terms ts = rev (fold Term.add_vars ts []);
    9.11  
    9.12  fun tvars_of thm = tvars_of_terms [Thm.full_prop_of thm];
    9.13  fun vars_of thm = vars_of_terms [Thm.full_prop_of thm];
    10.1 --- a/src/Pure/meta_simplifier.ML	Fri Jul 15 15:44:11 2005 +0200
    10.2 +++ b/src/Pure/meta_simplifier.ML	Fri Jul 15 15:44:15 2005 +0200
    10.3 @@ -403,7 +403,7 @@
    10.4  all its Vars? Better: a dynamic check each time a rule is applied.
    10.5  *)
    10.6  fun rewrite_rule_extra_vars prems elhs erhs =
    10.7 -  not (term_varnames erhs subset Library.foldl add_term_varnames (term_varnames elhs, prems))
    10.8 +  not (term_varnames erhs subset fold add_term_varnames prems (term_varnames elhs))
    10.9    orelse
   10.10    not (term_tvars erhs subset (term_tvars elhs union List.concat (map term_tvars prems)));
   10.11