src/HOL/Tools/Datatype/datatype_abs_proofs.ML
changeset 32906 ac97e8735cc2
parent 32905 5e46c6704cee
child 32915 a7a97960054b
     1.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Mon Oct 12 10:24:08 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Mon Oct 12 11:03:10 2009 +0200
     1.3 @@ -123,7 +123,7 @@
     1.4  
     1.5      (* introduction rules for graph of primrec function *)
     1.6  
     1.7 -    fun make_rec_intr T rec_set ((rec_intr_ts, l), (cname, cargs)) =
     1.8 +    fun make_rec_intr T rec_set (cname, cargs) (rec_intr_ts, l) =
     1.9        let
    1.10          fun mk_prem ((dt, U), (j, k, prems, t1s, t2s)) =
    1.11            let val free1 = mk_Free "x" U j
    1.12 @@ -148,9 +148,9 @@
    1.13            list_comb (nth rec_fns l, t1s @ t2s)))], l + 1)
    1.14        end;
    1.15  
    1.16 -    val (rec_intr_ts, _) = Library.foldl (fn (x, ((d, T), set_name)) =>
    1.17 -      Library.foldl (make_rec_intr T set_name) (x, #3 (snd d)))
    1.18 -        (([], 0), descr' ~~ recTs ~~ rec_sets');
    1.19 +    val (rec_intr_ts, _) = fold (fn ((d, T), set_name) =>
    1.20 +      fold (make_rec_intr T set_name) (#3 (snd d)))
    1.21 +        (descr' ~~ recTs ~~ rec_sets') ([], 0);
    1.22  
    1.23      val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
    1.24          Inductive.add_inductive_global (serial_string ())
    1.25 @@ -165,7 +165,7 @@
    1.26  
    1.27      val _ = message config "Proving termination and uniqueness of primrec functions ...";
    1.28  
    1.29 -    fun mk_unique_tac ((tac, intrs), ((((i, (tname, _, constrs)), elim), T), T')) =
    1.30 +    fun mk_unique_tac ((((i, (tname, _, constrs)), elim), T), T') (tac, intrs) =
    1.31        let
    1.32          val distinct_tac =
    1.33            (if i < length newTs then
    1.34 @@ -176,7 +176,7 @@
    1.35            (if i < length newTs then nth constr_inject i
    1.36              else injects_of tname);
    1.37  
    1.38 -        fun mk_unique_constr_tac n ((tac, intr::intrs, j), (cname, cargs)) =
    1.39 +        fun mk_unique_constr_tac n (cname, cargs) (tac, intr::intrs, j) =
    1.40            let
    1.41              val k = length (filter is_rec_type cargs)
    1.42  
    1.43 @@ -195,8 +195,8 @@
    1.44                intrs, j + 1)
    1.45            end;
    1.46  
    1.47 -        val (tac', intrs', _) = Library.foldl (mk_unique_constr_tac (length constrs))
    1.48 -          ((tac, intrs, 0), constrs);
    1.49 +        val (tac', intrs', _) = fold (mk_unique_constr_tac (length constrs))
    1.50 +          constrs (tac, intrs, 0);
    1.51  
    1.52        in (tac', intrs') end;
    1.53  
    1.54 @@ -211,10 +211,9 @@
    1.55            ((1 upto length recTs) ~~ recTs ~~ rec_unique_ts);
    1.56          val induct' = cterm_instantiate ((map cert induct_Ps) ~~
    1.57            (map cert insts)) induct;
    1.58 -        val (tac, _) = Library.foldl mk_unique_tac
    1.59 -          (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1
    1.60 -              THEN rewrite_goals_tac [mk_meta_eq choice_eq], rec_intrs),
    1.61 -            descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts);
    1.62 +        val (tac, _) = fold mk_unique_tac (descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
    1.63 +           (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1
    1.64 +              THEN rewrite_goals_tac [mk_meta_eq choice_eq], rec_intrs));
    1.65  
    1.66        in split_conj_thm (SkipProof.prove_global thy1 [] []
    1.67          (HOLogic.mk_Trueprop (mk_conj rec_unique_ts)) (K tac))
    1.68 @@ -267,7 +266,7 @@
    1.69           [Nitpick_Const_Simps.add])]
    1.70      ||> Sign.parent_path
    1.71      ||> Theory.checkpoint
    1.72 -    |-> (fn thms => pair (reccomb_names, Library.flat thms))
    1.73 +    |-> (fn thms => pair (reccomb_names, flat thms))
    1.74    end;
    1.75  
    1.76  
    1.77 @@ -298,10 +297,9 @@
    1.78  
    1.79      (* define case combinators via primrec combinators *)
    1.80  
    1.81 -    val (case_defs, thy2) = Library.foldl (fn ((defs, thy),
    1.82 -      ((((i, (_, _, constrs)), T), name), recname)) =>
    1.83 +    val (case_defs, thy2) = fold (fn ((((i, (_, _, constrs)), T), name), recname) => fn (defs, thy) =>
    1.84          let
    1.85 -          val (fns1, fns2) = ListPair.unzip (map (fn ((_, cargs), j) =>
    1.86 +          val (fns1, fns2) = split_list (map (fn ((_, cargs), j) =>
    1.87              let
    1.88                val Ts = map (typ_of_dtyp descr' sorts) cargs;
    1.89                val Ts' = Ts @ map mk_dummyT (List.filter is_rec_type cargs);
    1.90 @@ -328,8 +326,8 @@
    1.91              |> (PureThy.add_defs false o map Thm.no_attributes) [def];
    1.92  
    1.93          in (defs @ [def_thm], thy')
    1.94 -        end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~
    1.95 -          (Library.take (length newTs, reccomb_names)))
    1.96 +        end) (hd descr ~~ newTs ~~ case_names ~~
    1.97 +          Library.take (length newTs, reccomb_names)) ([], thy1)
    1.98        ||> Theory.checkpoint;
    1.99  
   1.100      val case_thms = map (map (fn t => SkipProof.prove_global thy2 [] [] t