replaced itlist by fold_rev;
authorwenzelm
Thu Jul 14 19:28:38 2005 +0200 (2005-07-14)
changeset 1685333b886cbdc8f
parent 16852 b950180e243d
child 16854 fdd362b7e980
replaced itlist by fold_rev;
replaced rev_itlist by fold;
TFL/rules.ML
TFL/tfl.ML
TFL/usyntax.ML
     1.1 --- a/TFL/rules.ML	Thu Jul 14 19:28:37 2005 +0200
     1.2 +++ b/TFL/rules.ML	Thu Jul 14 19:28:38 2005 +0200
     1.3 @@ -128,7 +128,7 @@
     1.4  fun DISCH tm thm = Thm.implies_intr (D.mk_prop tm) thm COMP impI
     1.5    handle THM (msg, _, _) => raise RULES_ERR "DISCH" msg;
     1.6  
     1.7 -fun DISCH_ALL thm = U.itlist DISCH (#hyps (Thm.crep_thm thm)) thm;
     1.8 +fun DISCH_ALL thm = fold_rev DISCH (#hyps (Thm.crep_thm thm)) thm;
     1.9  
    1.10  
    1.11  fun FILTER_DISCH_ALL P thm =
    1.12 @@ -202,9 +202,9 @@
    1.13          | blue ldisjs (th::rst) rdisjs =
    1.14              let val tail = tl rdisjs
    1.15                  val rdisj_tl = D.list_mk_disj tail
    1.16 -            in U.itlist DISJ2 ldisjs (DISJ1 th rdisj_tl)
    1.17 +            in fold_rev DISJ2 ldisjs (DISJ1 th rdisj_tl)
    1.18                 :: blue (ldisjs @ [cconcl th]) rst tail
    1.19 -            end handle U.ERR _ => [U.itlist DISJ2 ldisjs th]
    1.20 +            end handle U.ERR _ => [fold_rev DISJ2 ldisjs th]
    1.21     in blue [] thms (map cconcl thms) end;
    1.22  
    1.23  
    1.24 @@ -287,10 +287,10 @@
    1.25     end
    1.26  end;
    1.27  
    1.28 -fun SPEC_ALL thm = U.rev_itlist SPEC (#1(D.strip_forall(cconcl thm))) thm;
    1.29 +fun SPEC_ALL thm = fold SPEC (#1(D.strip_forall(cconcl thm))) thm;
    1.30  
    1.31  val ISPEC = SPEC
    1.32 -val ISPECL = U.rev_itlist ISPEC;
    1.33 +val ISPECL = fold ISPEC;
    1.34  
    1.35  (* Not optimized! Too complicated. *)
    1.36  local val {prop,sign,...} = rep_thm allI
    1.37 @@ -318,7 +318,7 @@
    1.38     end
    1.39  end;
    1.40  
    1.41 -val GENL = U.itlist GEN;
    1.42 +val GENL = fold_rev GEN;
    1.43  
    1.44  fun GEN_ALL thm =
    1.45     let val {prop,sign,...} = rep_thm thm
    1.46 @@ -383,7 +383,7 @@
    1.47   *---------------------------------------------------------------------------*)
    1.48  
    1.49  fun EXISTL vlist th =
    1.50 -  U.itlist (fn v => fn thm => EXISTS(D.mk_exists(v,cconcl thm), v) thm)
    1.51 +  fold_rev (fn v => fn thm => EXISTS(D.mk_exists(v,cconcl thm), v) thm)
    1.52             vlist th;
    1.53  
    1.54  
    1.55 @@ -404,7 +404,7 @@
    1.56         fun ?v M  = cterm_of sign (S.mk_exists{Bvar=v,Body = M})
    1.57  
    1.58    in
    1.59 -  U.itlist (fn (b as (r1,r2)) => fn thm =>
    1.60 +  fold_rev (fn (b as (r1,r2)) => fn thm =>
    1.61          EXISTS(?r2(subst_free[b]
    1.62                     (HOLogic.dest_Trueprop(#prop(rep_thm thm)))), tych r1)
    1.63                thm)
    1.64 @@ -527,7 +527,7 @@
    1.65        val ants = Logic.strip_imp_prems prop
    1.66        val news = get (ants,1,[])
    1.67    in
    1.68 -  U.rev_itlist rename_params_rule news thm
    1.69 +  fold rename_params_rule news thm
    1.70    end;
    1.71  
    1.72  
    1.73 @@ -567,7 +567,7 @@
    1.74    handle U.ERR _ => S.mk_pabs {varstruct = vstr, body = body};
    1.75  
    1.76  fun list_mk_aabs (vstrl,tm) =
    1.77 -    U.itlist (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm;
    1.78 +    fold_rev (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm;
    1.79  
    1.80  fun dest_aabs used tm =
    1.81     let val ({Bvar,Body}, used') = S.dest_abs used tm
    1.82 @@ -765,7 +765,7 @@
    1.83                     sign,...} = rep_thm thm
    1.84                fun genl tm = let val vlist = gen_rems (op aconv)
    1.85                                             (add_term_frees(tm,[]), globals)
    1.86 -                            in U.itlist Forall vlist tm
    1.87 +                            in fold_rev Forall vlist tm
    1.88                              end
    1.89                (*--------------------------------------------------------------
    1.90                 * This actually isn't quite right, since it will think that
     2.1 --- a/TFL/tfl.ML	Thu Jul 14 19:28:37 2005 +0200
     2.2 +++ b/TFL/tfl.ML	Thu Jul 14 19:28:38 2005 +0200
     2.3 @@ -104,7 +104,7 @@
     2.4            let val (c, T) = dest_Const c
     2.5                val L = binder_types T
     2.6                val (in_group, not_in_group) =
     2.7 -               U.itlist (fn (row as (p::rst, rhs)) =>
     2.8 +               fold_rev (fn (row as (p::rst, rhs)) =>
     2.9                           fn (in_group,not_in_group) =>
    2.10                    let val (pc,args) = S.strip_comb p
    2.11                    in if (#1(dest_Const pc) = c)
    2.12 @@ -160,7 +160,7 @@
    2.13   * pattern with constructor = name.
    2.14   *---------------------------------------------------------------------------*)
    2.15  fun mk_group name rows =
    2.16 -  U.itlist (fn (row as ((prfx, p::rst), rhs)) =>
    2.17 +  fold_rev (fn (row as ((prfx, p::rst), rhs)) =>
    2.18              fn (in_group,not_in_group) =>
    2.19                 let val (pc,args) = S.strip_comb p
    2.20                 in if ((#1 (Term.dest_Const pc) = name) handle TERM _ => false)
    2.21 @@ -565,14 +565,14 @@
    2.22       val full_rqt_prop = map (Dcterm.mk_prop o tych) full_rqt
    2.23           (*lcp: a lot of object-logic inference to remove*)
    2.24       val baz = R.DISCH_ALL
    2.25 -                 (U.itlist R.DISCH full_rqt_prop
    2.26 +                 (fold_rev R.DISCH full_rqt_prop
    2.27                    (R.LIST_CONJ extractants))
    2.28       val dum = if !trace then writeln ("baz = " ^ string_of_thm baz)
    2.29                             else ()
    2.30       val f_free = Free (fid, fastype_of f)  (*'cos f is a Const*)
    2.31       val SV' = map tych SV;
    2.32       val SVrefls = map reflexive SV'
    2.33 -     val def0 = (U.rev_itlist (fn x => fn th => R.rbeta(combination th x))
    2.34 +     val def0 = (fold (fn x => fn th => R.rbeta(combination th x))
    2.35                     SVrefls def)
    2.36                  RS meta_eq_to_obj_eq
    2.37       val def' = R.MP (R.SPEC (tych R') (R.GEN (tych R1) baz)) def0
    2.38 @@ -584,7 +584,7 @@
    2.39      "defer_recdef requires theory Main or at least Hilbert_Choice as parent"
    2.40       val bar = R.MP (R.ISPECL[tych R'abs, tych R1] SELECT_AX) body_th
    2.41   in {theory = theory, R=R1, SV=SV,
    2.42 -     rules = U.rev_itlist (U.C R.MP) (R.CONJUNCTS bar) def',
    2.43 +     rules = fold (U.C R.MP) (R.CONJUNCTS bar) def',
    2.44       full_pats_TCs = merge (map pat_of pats) (ListPair.zip (givens pats, TCl)),
    2.45       patterns = pats}
    2.46   end;
    2.47 @@ -834,7 +834,7 @@
    2.48        val [veq] = List.filter (can S.dest_eq) (#1 (R.dest_thm thm))
    2.49        val {lhs,rhs} = S.dest_eq veq
    2.50        val L = S.free_vars_lr rhs
    2.51 -  in  #2 (U.itlist CHOOSER L (veq,thm))  end;
    2.52 +  in  #2 (fold_rev CHOOSER L (veq,thm))  end;
    2.53  
    2.54  
    2.55  (*----------------------------------------------------------------------------
    2.56 @@ -873,7 +873,7 @@
    2.57      val dc = R.MP Sinduct dant
    2.58      val Parg_ty = type_of(#Bvar(S.dest_forall(concl dc)))
    2.59      val vars = map (gvvariant[Pname]) (S.strip_prod_type Parg_ty)
    2.60 -    val dc' = U.itlist (R.GEN o tych) vars
    2.61 +    val dc' = fold_rev (R.GEN o tych) vars
    2.62                         (R.SPEC (tych(S.mk_vstruct Parg_ty vars)) dc)
    2.63  in
    2.64     R.GEN (tych P) (R.DISCH (tych(concl Rinduct_assum)) dc')
    2.65 @@ -999,7 +999,7 @@
    2.66          let val tcs = #1(strip_imp (concl r))
    2.67              val extra_tcs = gen_rems (op aconv) (ftcs, tcs)
    2.68              val extra_tc_thms = map simplify_nested_tc extra_tcs
    2.69 -            val (r1,ind1) = U.rev_itlist simplify_tc tcs (r,ind)
    2.70 +            val (r1,ind1) = fold simplify_tc tcs (r,ind)
    2.71              val r2 = R.FILTER_DISCH_ALL(not o S.is_WFR) r1
    2.72          in loop(rst, nthms@extra_tc_thms, r2::R, ind1)
    2.73          end
     3.1 --- a/TFL/usyntax.ML	Thu Jul 14 19:28:37 2005 +0200
     3.2 +++ b/TFL/usyntax.ML	Thu Jul 14 19:28:38 2005 +0200
     3.3 @@ -115,7 +115,7 @@
     3.4  val is_vartype = can dest_vtype;
     3.5  
     3.6  val type_vars  = map mk_prim_vartype o typ_tvars
     3.7 -fun type_varsl L = distinct (Utils.rev_itlist (curry op @ o type_vars) L []);
     3.8 +fun type_varsl L = distinct (fold (curry op @ o type_vars) L []);
     3.9  
    3.10  val alpha  = mk_vartype "'a"
    3.11  val beta   = mk_vartype "'b"
    3.12 @@ -312,11 +312,11 @@
    3.13  
    3.14  (* Construction of a cterm from a list of Terms *)
    3.15  
    3.16 -fun list_mk_abs(L,tm) = Utils.itlist (fn v => fn M => mk_abs{Bvar=v, Body=M}) L tm;
    3.17 +fun list_mk_abs(L,tm) = fold_rev (fn v => fn M => mk_abs{Bvar=v, Body=M}) L tm;
    3.18  
    3.19  (* These others are almost never used *)
    3.20 -fun list_mk_imp(A,c) = Utils.itlist(fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c;
    3.21 -fun list_mk_forall(V,t) = Utils.itlist(fn v => fn b => mk_forall{Bvar=v, Body=b})V t;
    3.22 +fun list_mk_imp(A,c) = fold_rev (fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c;
    3.23 +fun list_mk_forall(V,t) = fold_rev (fn v => fn b => mk_forall{Bvar=v, Body=b})V t;
    3.24  val list_mk_conj = Utils.end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm})
    3.25  
    3.26