src/HOL/Nominal/nominal_datatype.ML
changeset 33338 de76079f973a
parent 33317 b4534348b8fd
child 33368 b1cf34f1855c
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Thu Oct 29 23:48:56 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Oct 29 23:49:55 2009 +0100
     1.3 @@ -526,7 +526,7 @@
     1.4  
     1.5      fun make_intr s T (cname, cargs) =
     1.6        let
     1.7 -        fun mk_prem (dt, (j, j', prems, ts)) =
     1.8 +        fun mk_prem dt (j, j', prems, ts) =
     1.9            let
    1.10              val (dts, dt') = strip_option dt;
    1.11              val (dts', dt'') = strip_dtyp dt';
    1.12 @@ -535,7 +535,7 @@
    1.13              val T = typ_of_dtyp descr sorts dt'';
    1.14              val free = mk_Free "x" (Us ---> T) j;
    1.15              val free' = app_bnds free (length Us);
    1.16 -            fun mk_abs_fun (T, (i, t)) =
    1.17 +            fun mk_abs_fun T (i, t) =
    1.18                let val U = fastype_of t
    1.19                in (i + 1, Const ("Nominal.abs_fun", [T, U, T] --->
    1.20                  Type ("Nominal.noption", [U])) $ mk_Free "y" T i $ t)
    1.21 @@ -546,10 +546,10 @@
    1.22                    HOLogic.mk_Trueprop (Free (List.nth (rep_set_names, k),
    1.23                      T --> HOLogic.boolT) $ free')) :: prems
    1.24                | _ => prems,
    1.25 -            snd (List.foldr mk_abs_fun (j', free) Ts) :: ts)
    1.26 +            snd (fold_rev mk_abs_fun Ts (j', free)) :: ts)
    1.27            end;
    1.28  
    1.29 -        val (_, _, prems, ts) = List.foldr mk_prem (1, 1, [], []) cargs;
    1.30 +        val (_, _, prems, ts) = fold_rev mk_prem cargs (1, 1, [], []);
    1.31          val concl = HOLogic.mk_Trueprop (Free (s, T --> HOLogic.boolT) $
    1.32            list_comb (Const (cname, map fastype_of ts ---> T), ts))
    1.33        in Logic.list_implies (prems, concl)
    1.34 @@ -710,7 +710,7 @@
    1.35  
    1.36      (**** constructors ****)
    1.37  
    1.38 -    fun mk_abs_fun (x, t) =
    1.39 +    fun mk_abs_fun x t =
    1.40        let
    1.41          val T = fastype_of x;
    1.42          val U = fastype_of t
    1.43 @@ -776,7 +776,7 @@
    1.44      fun make_constr_def tname T T' (((cname_rep, _), (cname, cargs)), (cname', mx))
    1.45          (thy, defs, eqns) =
    1.46        let
    1.47 -        fun constr_arg ((dts, dt), (j, l_args, r_args)) =
    1.48 +        fun constr_arg (dts, dt) (j, l_args, r_args) =
    1.49            let
    1.50              val xs = map (fn (dt, i) => mk_Free "x" (typ_of_dtyp descr'' sorts dt) i)
    1.51                (dts ~~ (j upto j + length dts - 1))
    1.52 @@ -784,16 +784,16 @@
    1.53            in
    1.54              (j + length dts + 1,
    1.55               xs @ x :: l_args,
    1.56 -             List.foldr mk_abs_fun
    1.57 +             fold_rev mk_abs_fun xs
    1.58                 (case dt of
    1.59                    DtRec k => if k < length new_type_names then
    1.60                        Const (List.nth (rep_names, k), typ_of_dtyp descr'' sorts dt -->
    1.61                          typ_of_dtyp descr sorts dt) $ x
    1.62                      else error "nested recursion not (yet) supported"
    1.63 -                | _ => x) xs :: r_args)
    1.64 +                | _ => x) :: r_args)
    1.65            end
    1.66  
    1.67 -        val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) cargs;
    1.68 +        val (_, l_args, r_args) = fold_rev constr_arg cargs (1, [], []);
    1.69          val abs_name = Sign.intern_const thy ("Abs_" ^ tname);
    1.70          val rep_name = Sign.intern_const thy ("Rep_" ^ tname);
    1.71          val constrT = map fastype_of l_args ---> T;
    1.72 @@ -902,7 +902,7 @@
    1.73              let val T = fastype_of t
    1.74              in Const ("Nominal.perm", permT --> T --> T) $ pi $ t end;
    1.75  
    1.76 -          fun constr_arg ((dts, dt), (j, l_args, r_args)) =
    1.77 +          fun constr_arg (dts, dt) (j, l_args, r_args) =
    1.78              let
    1.79                val Ts = map (typ_of_dtyp descr'' sorts) dts;
    1.80                val xs = map (fn (T, i) => mk_Free "x" T i)
    1.81 @@ -914,7 +914,7 @@
    1.82                 map perm (xs @ [x]) @ r_args)
    1.83              end
    1.84  
    1.85 -          val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) dts;
    1.86 +          val (_, l_args, r_args) = fold_rev constr_arg dts (1, [], []);
    1.87            val c = Const (cname, map fastype_of l_args ---> T)
    1.88          in
    1.89            Goal.prove_global thy8 [] []
    1.90 @@ -952,7 +952,7 @@
    1.91            val cname = Sign.intern_const thy8
    1.92              (Long_Name.append tname (Long_Name.base_name cname));
    1.93  
    1.94 -          fun make_inj ((dts, dt), (j, args1, args2, eqs)) =
    1.95 +          fun make_inj (dts, dt) (j, args1, args2, eqs) =
    1.96              let
    1.97                val Ts_idx = map (typ_of_dtyp descr'' sorts) dts ~~ (j upto j + length dts - 1);
    1.98                val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
    1.99 @@ -963,10 +963,10 @@
   1.100                (j + length dts + 1,
   1.101                 xs @ (x :: args1), ys @ (y :: args2),
   1.102                 HOLogic.mk_eq
   1.103 -                 (List.foldr mk_abs_fun x xs, List.foldr mk_abs_fun y ys) :: eqs)
   1.104 +                 (fold_rev mk_abs_fun xs x, fold_rev mk_abs_fun ys y) :: eqs)
   1.105              end;
   1.106  
   1.107 -          val (_, args1, args2, eqs) = List.foldr make_inj (1, [], [], []) dts;
   1.108 +          val (_, args1, args2, eqs) = fold_rev make_inj dts (1, [], [], []);
   1.109            val Ts = map fastype_of args1;
   1.110            val c = Const (cname, Ts ---> T)
   1.111          in
   1.112 @@ -995,17 +995,17 @@
   1.113              (Long_Name.append tname (Long_Name.base_name cname));
   1.114            val atomT = Type (atom, []);
   1.115  
   1.116 -          fun process_constr ((dts, dt), (j, args1, args2)) =
   1.117 +          fun process_constr (dts, dt) (j, args1, args2) =
   1.118              let
   1.119                val Ts_idx = map (typ_of_dtyp descr'' sorts) dts ~~ (j upto j + length dts - 1);
   1.120                val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
   1.121                val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts)
   1.122              in
   1.123                (j + length dts + 1,
   1.124 -               xs @ (x :: args1), List.foldr mk_abs_fun x xs :: args2)
   1.125 +               xs @ (x :: args1), fold_rev mk_abs_fun xs x :: args2)
   1.126              end;
   1.127  
   1.128 -          val (_, args1, args2) = List.foldr process_constr (1, [], []) dts;
   1.129 +          val (_, args1, args2) = fold_rev process_constr dts (1, [], []);
   1.130            val Ts = map fastype_of args1;
   1.131            val c = list_comb (Const (cname, Ts ---> T), args1);
   1.132            fun supp t =