src/HOL/Tools/datatype_rep_proofs.ML
changeset 15574 b1d1b5bfc464
parent 15570 8d8c70b41bab
child 16287 7a03b4b4df67
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Fri Mar 04 11:44:26 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Fri Mar 04 15:07:34 2005 +0100
     1.3 @@ -78,7 +78,7 @@
     1.4      val branchT = if null branchTs then HOLogic.unitT
     1.5        else fold_bal (fn (T, U) => Type ("+", [T, U])) branchTs;
     1.6      val arities = get_arities descr' \ 0;
     1.7 -    val unneeded_vars = hd tyvars \\ Library.foldr add_typ_tfree_names (leafTs' @ branchTs, []);
     1.8 +    val unneeded_vars = hd tyvars \\ foldr add_typ_tfree_names [] (leafTs' @ branchTs);
     1.9      val leafTs = leafTs' @ (map (fn n => TFree (n, valOf (assoc (sorts, n)))) unneeded_vars);
    1.10      val recTs = get_rec_types descr' sorts;
    1.11      val newTs = Library.take (length (hd descr), recTs);
    1.12 @@ -134,7 +134,7 @@
    1.13        in mk_inj branchT (length branchTs) (1 + find_index_eq T' branchTs)
    1.14        end;
    1.15  
    1.16 -    val mk_lim = Library.foldr (fn (T, t) => Lim $ mk_fun_inj T (Abs ("x", T, t)));
    1.17 +    val mk_lim = foldr (fn (T, t) => Lim $ mk_fun_inj T (Abs ("x", T, t)));
    1.18  
    1.19      (************** generate introduction rules for representing set **********)
    1.20  
    1.21 @@ -153,14 +153,14 @@
    1.22                in (j + 1, list_all (map (pair "x") Ts,
    1.23                    HOLogic.mk_Trueprop (HOLogic.mk_mem (free_t,
    1.24                      Const (List.nth (rep_set_names, k), UnivT)))) :: prems,
    1.25 -                mk_lim (Ts, free_t) :: ts)
    1.26 +                mk_lim free_t Ts :: ts)
    1.27                end
    1.28            | _ =>
    1.29                let val T = typ_of_dtyp descr' sorts dt
    1.30                in (j + 1, prems, (Leaf $ mk_inj T (mk_Free "x" T j))::ts)
    1.31                end);
    1.32  
    1.33 -        val (_, prems, ts) = Library.foldr mk_prem (cargs, (1, [], []));
    1.34 +        val (_, prems, ts) = foldr mk_prem (1, [], []) cargs;
    1.35          val concl = HOLogic.mk_Trueprop (HOLogic.mk_mem
    1.36            (mk_univ_inj ts n i, Const (s, UnivT)))
    1.37        in Logic.list_implies (prems, concl)
    1.38 @@ -210,13 +210,13 @@
    1.39            let val T = typ_of_dtyp descr' sorts dt;
    1.40                val free_t = mk_Free "x" T j
    1.41            in (case (strip_dtyp dt, strip_type T) of
    1.42 -              ((_, DtRec m), (Us, U)) => (j + 1, free_t :: l_args, mk_lim (Us,
    1.43 -                Const (List.nth (all_rep_names, m), U --> Univ_elT) $
    1.44 -                  app_bnds free_t (length Us)) :: r_args)
    1.45 +              ((_, DtRec m), (Us, U)) => (j + 1, free_t :: l_args, mk_lim
    1.46 +                (Const (List.nth (all_rep_names, m), U --> Univ_elT) $
    1.47 +                   app_bnds free_t (length Us)) Us :: r_args)
    1.48              | _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args))
    1.49            end;
    1.50  
    1.51 -        val (_, l_args, r_args) = Library.foldr constr_arg (cargs, (1, [], []));
    1.52 +        val (_, l_args, r_args) = foldr constr_arg (1, [], []) cargs;
    1.53          val constrT = (map (typ_of_dtyp descr' sorts) cargs) ---> T;
    1.54          val abs_name = Sign.intern_const (Theory.sign_of thy) ("Abs_" ^ tname);
    1.55          val rep_name = Sign.intern_const (Theory.sign_of thy) ("Rep_" ^ tname);
    1.56 @@ -329,13 +329,13 @@
    1.57              val (Us, U) = strip_type T'
    1.58            in (case strip_dtyp dt of
    1.59                (_, DtRec j) => if j mem ks' then
    1.60 -                  (i2 + 1, i2' + 1, ts @ [mk_lim (Us, app_bnds
    1.61 -                     (mk_Free "y" (Us ---> Univ_elT) i2') (length Us))],
    1.62 +                  (i2 + 1, i2' + 1, ts @ [mk_lim (app_bnds
    1.63 +                     (mk_Free "y" (Us ---> Univ_elT) i2') (length Us)) Us],
    1.64                     Ts @ [Us ---> Univ_elT])
    1.65                  else
    1.66 -                  (i2 + 1, i2', ts @ [mk_lim (Us,
    1.67 -                     Const (List.nth (all_rep_names, j), U --> Univ_elT) $
    1.68 -                       app_bnds (mk_Free "x" T' i2) (length Us))], Ts)
    1.69 +                  (i2 + 1, i2', ts @ [mk_lim
    1.70 +                     (Const (List.nth (all_rep_names, j), U --> Univ_elT) $
    1.71 +                        app_bnds (mk_Free "x" T' i2) (length Us)) Us], Ts)
    1.72              | _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (mk_Free "x" T' i2)], Ts))
    1.73            end;
    1.74  
    1.75 @@ -380,8 +380,8 @@
    1.76  
    1.77        in (thy', char_thms' @ char_thms) end;
    1.78  
    1.79 -    val (thy5, iso_char_thms) = Library.foldr make_iso_defs
    1.80 -      (tl descr, (add_path flat_names big_name thy4, []));
    1.81 +    val (thy5, iso_char_thms) = foldr make_iso_defs
    1.82 +      (add_path flat_names big_name thy4, []) (tl descr);
    1.83  
    1.84      (* prove isomorphism properties *)
    1.85  
    1.86 @@ -469,8 +469,8 @@
    1.87        in (inj_thms'' @ inj_thms, elem_thms @ (split_conj_thm elem_thm))
    1.88        end;
    1.89  
    1.90 -    val (iso_inj_thms_unfolded, iso_elem_thms) = Library.foldr prove_iso_thms
    1.91 -      (tl descr, ([], map #3 newT_iso_axms));
    1.92 +    val (iso_inj_thms_unfolded, iso_elem_thms) = foldr prove_iso_thms
    1.93 +      ([], map #3 newT_iso_axms) (tl descr);
    1.94      val iso_inj_thms = map snd newT_iso_inj_thms @ iso_inj_thms_unfolded;
    1.95  
    1.96      (* prove  x : dt_rep_set_i --> x : range dt_Rep_i *)