src/HOL/Tools/datatype_abs_proofs.ML
changeset 15570 8d8c70b41bab
parent 15459 16dd63c78049
child 15574 b1d1b5bfc464
     1.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -54,9 +54,9 @@
     1.4    let
     1.5      val _ = message "Proving case distinction theorems ...";
     1.6  
     1.7 -    val descr' = flat descr;
     1.8 +    val descr' = List.concat descr;
     1.9      val recTs = get_rec_types descr' sorts;
    1.10 -    val newTs = take (length (hd descr), recTs);
    1.11 +    val newTs = Library.take (length (hd descr), recTs);
    1.12  
    1.13      val {maxidx, ...} = rep_thm induct;
    1.14      val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
    1.15 @@ -67,11 +67,11 @@
    1.16            Abs ("z", T', Const ("True", T''))) induct_Ps;
    1.17          val P = Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", maxidx+1), T), Bound 0) $
    1.18            Var (("P", 0), HOLogic.boolT))
    1.19 -        val insts = take (i, dummyPs) @ (P::(drop (i + 1, dummyPs)));
    1.20 +        val insts = Library.take (i, dummyPs) @ (P::(Library.drop (i + 1, dummyPs)));
    1.21          val cert = cterm_of (Theory.sign_of thy);
    1.22          val insts' = (map cert induct_Ps) ~~ (map cert insts);
    1.23 -        val induct' = refl RS ((nth_elem (i,
    1.24 -          split_conj_thm (cterm_instantiate insts' induct))) RSN (2, rev_mp))
    1.25 +        val induct' = refl RS ((List.nth
    1.26 +          (split_conj_thm (cterm_instantiate insts' induct), i)) RSN (2, rev_mp))
    1.27  
    1.28        in prove_goalw_cterm [] (cert t) (fn prems =>
    1.29          [rtac induct' 1,
    1.30 @@ -95,10 +95,10 @@
    1.31      val big_name = space_implode "_" new_type_names;
    1.32      val thy0 = add_path flat_names big_name thy;
    1.33  
    1.34 -    val descr' = flat descr;
    1.35 +    val descr' = List.concat descr;
    1.36      val recTs = get_rec_types descr' sorts;
    1.37 -    val used = foldr add_typ_tfree_names (recTs, []);
    1.38 -    val newTs = take (length (hd descr), recTs);
    1.39 +    val used = Library.foldr add_typ_tfree_names (recTs, []);
    1.40 +    val newTs = Library.take (length (hd descr), recTs);
    1.41  
    1.42      val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
    1.43  
    1.44 @@ -127,27 +127,27 @@
    1.45            in (case (strip_dtyp dt, strip_type U) of
    1.46               ((_, DtRec m), (Us, _)) =>
    1.47                 let
    1.48 -                 val free2 = mk_Free "y" (Us ---> nth_elem (m, rec_result_Ts)) k;
    1.49 +                 val free2 = mk_Free "y" (Us ---> List.nth (rec_result_Ts, m)) k;
    1.50                   val i = length Us
    1.51                 in (j + 1, k + 1, HOLogic.mk_Trueprop (HOLogic.list_all
    1.52                       (map (pair "x") Us, HOLogic.mk_mem (HOLogic.mk_prod
    1.53                         (app_bnds free1 i, app_bnds free2 i),
    1.54 -                         nth_elem (m, rec_sets)))) :: prems,
    1.55 +                         List.nth (rec_sets, m)))) :: prems,
    1.56                     free1::t1s, free2::t2s)
    1.57                 end
    1.58             | _ => (j + 1, k, prems, free1::t1s, t2s))
    1.59            end;
    1.60  
    1.61          val Ts = map (typ_of_dtyp descr' sorts) cargs;
    1.62 -        val (_, _, prems, t1s, t2s) = foldr mk_prem (cargs ~~ Ts, (1, 1, [], [], []))
    1.63 +        val (_, _, prems, t1s, t2s) = Library.foldr mk_prem (cargs ~~ Ts, (1, 1, [], [], []))
    1.64  
    1.65        in (rec_intr_ts @ [Logic.list_implies (prems, HOLogic.mk_Trueprop (HOLogic.mk_mem
    1.66          (HOLogic.mk_prod (list_comb (Const (cname, Ts ---> T), t1s),
    1.67 -          list_comb (nth_elem (l, rec_fns), t1s @ t2s)), set_name)))], l + 1)
    1.68 +          list_comb (List.nth (rec_fns, l), t1s @ t2s)), set_name)))], l + 1)
    1.69        end;
    1.70  
    1.71 -    val (rec_intr_ts, _) = foldl (fn (x, ((d, T), set_name)) =>
    1.72 -      foldl (make_rec_intr T set_name) (x, #3 (snd d)))
    1.73 +    val (rec_intr_ts, _) = Library.foldl (fn (x, ((d, T), set_name)) =>
    1.74 +      Library.foldl (make_rec_intr T set_name) (x, #3 (snd d)))
    1.75          (([], 0), descr' ~~ recTs ~~ rec_sets);
    1.76  
    1.77      val (thy1, {intrs = rec_intrs, elims = rec_elims, ...}) =
    1.78 @@ -163,16 +163,16 @@
    1.79        let
    1.80          val distinct_tac = (etac Pair_inject 1) THEN
    1.81            (if i < length newTs then
    1.82 -             full_simp_tac (HOL_ss addsimps (nth_elem (i, dist_rewrites))) 1
    1.83 +             full_simp_tac (HOL_ss addsimps (List.nth (dist_rewrites, i))) 1
    1.84             else full_simp_tac dist_ss 1);
    1.85  
    1.86          val inject = map (fn r => r RS iffD1)
    1.87 -          (if i < length newTs then nth_elem (i, constr_inject)
    1.88 -            else #inject (the (Symtab.lookup (dt_info, tname))));
    1.89 +          (if i < length newTs then List.nth (constr_inject, i)
    1.90 +            else #inject (valOf (Symtab.lookup (dt_info, tname))));
    1.91  
    1.92          fun mk_unique_constr_tac n ((tac, intr::intrs, j), (cname, cargs)) =
    1.93            let
    1.94 -            val k = length (filter is_rec_type cargs)
    1.95 +            val k = length (List.filter is_rec_type cargs)
    1.96  
    1.97            in (EVERY [DETERM tac,
    1.98                  REPEAT (etac ex1E 1), rtac ex1I 1,
    1.99 @@ -189,7 +189,7 @@
   1.100                intrs, j + 1)
   1.101            end;
   1.102  
   1.103 -        val (tac', intrs', _) = foldl (mk_unique_constr_tac (length constrs))
   1.104 +        val (tac', intrs', _) = Library.foldl (mk_unique_constr_tac (length constrs))
   1.105            ((tac, intrs, 0), constrs);
   1.106  
   1.107        in (tac', intrs') end;
   1.108 @@ -206,7 +206,7 @@
   1.109            ((1 upto length recTs) ~~ recTs ~~ rec_unique_ts);
   1.110          val induct' = cterm_instantiate ((map cert induct_Ps) ~~
   1.111            (map cert insts)) induct;
   1.112 -        val (tac, _) = foldl mk_unique_tac
   1.113 +        val (tac, _) = Library.foldl mk_unique_tac
   1.114            (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_tac) 1
   1.115                THEN rewtac (mk_meta_eq choice_eq), rec_intrs),
   1.116              descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts);
   1.117 @@ -255,7 +255,7 @@
   1.118    in
   1.119      thy2 |> Theory.add_path (space_implode "_" new_type_names) |>
   1.120      PureThy.add_thmss [(("recs", rec_thms), [])] |>>
   1.121 -    Theory.parent_path |> apsnd (pair reccomb_names o flat)
   1.122 +    Theory.parent_path |> apsnd (pair reccomb_names o List.concat)
   1.123    end;
   1.124  
   1.125  
   1.126 @@ -267,10 +267,10 @@
   1.127  
   1.128      val thy1 = add_path flat_names (space_implode "_" new_type_names) thy;
   1.129  
   1.130 -    val descr' = flat descr;
   1.131 +    val descr' = List.concat descr;
   1.132      val recTs = get_rec_types descr' sorts;
   1.133 -    val used = foldr add_typ_tfree_names (recTs, []);
   1.134 -    val newTs = take (length (hd descr), recTs);
   1.135 +    val used = Library.foldr add_typ_tfree_names (recTs, []);
   1.136 +    val newTs = Library.take (length (hd descr), recTs);
   1.137      val T' = TFree (variant used "'t", HOLogic.typeS);
   1.138  
   1.139      fun mk_dummyT dt = binder_types (typ_of_dtyp descr' sorts dt) ---> T';
   1.140 @@ -278,7 +278,7 @@
   1.141      val case_dummy_fns = map (fn (_, (_, _, constrs)) => map (fn (_, cargs) =>
   1.142        let
   1.143          val Ts = map (typ_of_dtyp descr' sorts) cargs;
   1.144 -        val Ts' = map mk_dummyT (filter is_rec_type cargs)
   1.145 +        val Ts' = map mk_dummyT (List.filter is_rec_type cargs)
   1.146        in Const ("arbitrary", Ts @ Ts' ---> T')
   1.147        end) constrs) descr';
   1.148  
   1.149 @@ -287,15 +287,15 @@
   1.150  
   1.151      (* define case combinators via primrec combinators *)
   1.152  
   1.153 -    val (case_defs, thy2) = foldl (fn ((defs, thy),
   1.154 +    val (case_defs, thy2) = Library.foldl (fn ((defs, thy),
   1.155        ((((i, (_, _, constrs)), T), name), recname)) =>
   1.156          let
   1.157            val (fns1, fns2) = ListPair.unzip (map (fn ((_, cargs), j) =>
   1.158              let
   1.159                val Ts = map (typ_of_dtyp descr' sorts) cargs;
   1.160 -              val Ts' = Ts @ map mk_dummyT (filter is_rec_type cargs);
   1.161 +              val Ts' = Ts @ map mk_dummyT (List.filter is_rec_type cargs);
   1.162                val frees' = map (uncurry (mk_Free "x")) (Ts' ~~ (1 upto length Ts'));
   1.163 -              val frees = take (length cargs, frees');
   1.164 +              val frees = Library.take (length cargs, frees');
   1.165                val free = mk_Free "f" (Ts ---> T') j
   1.166              in
   1.167               (free, list_abs_free (map dest_Free frees',
   1.168 @@ -303,20 +303,20 @@
   1.169              end) (constrs ~~ (1 upto length constrs)));
   1.170  
   1.171            val caseT = (map (snd o dest_Free) fns1) @ [T] ---> T';
   1.172 -          val fns = (flat (take (i, case_dummy_fns))) @
   1.173 -            fns2 @ (flat (drop (i + 1, case_dummy_fns)));
   1.174 +          val fns = (List.concat (Library.take (i, case_dummy_fns))) @
   1.175 +            fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns)));
   1.176            val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
   1.177            val decl = (Sign.base_name name, caseT, NoSyn);
   1.178            val def = ((Sign.base_name name) ^ "_def",
   1.179              Logic.mk_equals (list_comb (Const (name, caseT), fns1),
   1.180 -              list_comb (reccomb, (flat (take (i, case_dummy_fns))) @
   1.181 -                fns2 @ (flat (drop (i + 1, case_dummy_fns))) )));
   1.182 +              list_comb (reccomb, (List.concat (Library.take (i, case_dummy_fns))) @
   1.183 +                fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns))) )));
   1.184            val (thy', [def_thm]) = thy |>
   1.185              Theory.add_consts_i [decl] |> (PureThy.add_defs_i false o map Thm.no_attributes) [def];
   1.186  
   1.187          in (defs @ [def_thm], thy')
   1.188          end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~
   1.189 -          (take (length newTs, reccomb_names)));
   1.190 +          (Library.take (length newTs, reccomb_names)));
   1.191  
   1.192      val case_thms = map (map (fn t => prove_goalw_cterm (case_defs @
   1.193        (map mk_meta_eq primrec_thms)) (cterm_of (Theory.sign_of thy2) t)
   1.194 @@ -338,9 +338,9 @@
   1.195    let
   1.196      val _ = message "Proving equations for case splitting ...";
   1.197  
   1.198 -    val descr' = flat descr;
   1.199 +    val descr' = List.concat descr;
   1.200      val recTs = get_rec_types descr' sorts;
   1.201 -    val newTs = take (length (hd descr), recTs);
   1.202 +    val newTs = Library.take (length (hd descr), recTs);
   1.203  
   1.204      fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'),
   1.205          exhaustion), case_thms'), T) =
   1.206 @@ -372,7 +372,7 @@
   1.207  fun prove_size_thms flat_names new_type_names descr sorts reccomb_names primrec_thms thy =
   1.208    if exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt =>
   1.209      is_rec_type dt andalso not (null (fst (strip_dtyp dt)))) cargs) constrs)
   1.210 -      (flat descr)
   1.211 +      (List.concat descr)
   1.212    then
   1.213      (thy, [])
   1.214    else
   1.215 @@ -382,13 +382,13 @@
   1.216      val big_name = space_implode "_" new_type_names;
   1.217      val thy1 = add_path flat_names big_name thy;
   1.218  
   1.219 -    val descr' = flat descr;
   1.220 +    val descr' = List.concat descr;
   1.221      val recTs = get_rec_types descr' sorts;
   1.222  
   1.223      val size_name = "Nat.size";
   1.224      val size_names = replicate (length (hd descr)) size_name @
   1.225        map (Sign.full_name (Theory.sign_of thy1)) (DatatypeProp.indexify_names
   1.226 -        (map (fn T => name_of_typ T ^ "_size") (drop (length (hd descr), recTs))));
   1.227 +        (map (fn T => name_of_typ T ^ "_size") (Library.drop (length (hd descr), recTs))));
   1.228      val def_names = map (fn s => s ^ "_def") (DatatypeProp.indexify_names
   1.229        (map (fn T => name_of_typ T ^ "_size") recTs));
   1.230  
   1.231 @@ -397,20 +397,20 @@
   1.232      fun make_sizefun (_, cargs) =
   1.233        let
   1.234          val Ts = map (typ_of_dtyp descr' sorts) cargs;
   1.235 -        val k = length (filter is_rec_type cargs);
   1.236 +        val k = length (List.filter is_rec_type cargs);
   1.237          val t = if k = 0 then HOLogic.zero else
   1.238            foldl1 plus (map Bound (k - 1 downto 0) @ [HOLogic.mk_nat 1])
   1.239        in
   1.240 -        foldr (fn (T, t') => Abs ("x", T, t')) (Ts @ replicate k HOLogic.natT, t)
   1.241 +        Library.foldr (fn (T, t') => Abs ("x", T, t')) (Ts @ replicate k HOLogic.natT, t)
   1.242        end;
   1.243  
   1.244 -    val fs = flat (map (fn (_, (_, _, constrs)) => map make_sizefun constrs) descr');
   1.245 +    val fs = List.concat (map (fn (_, (_, _, constrs)) => map make_sizefun constrs) descr');
   1.246      val fTs = map fastype_of fs;
   1.247  
   1.248      val (thy', size_def_thms) = thy1 |>
   1.249        Theory.add_consts_i (map (fn (s, T) =>
   1.250          (Sign.base_name s, T --> HOLogic.natT, NoSyn))
   1.251 -          (drop (length (hd descr), size_names ~~ recTs))) |>
   1.252 +          (Library.drop (length (hd descr), size_names ~~ recTs))) |>
   1.253        (PureThy.add_defs_i true o map Thm.no_attributes) (map (fn (((s, T), def_name), rec_name) =>
   1.254          (def_name, Logic.mk_equals (Const (s, T --> HOLogic.natT),
   1.255            list_comb (Const (rec_name, fTs @ [T] ---> HOLogic.natT), fs))))
   1.256 @@ -426,7 +426,7 @@
   1.257    in
   1.258      thy' |> Theory.add_path big_name |>
   1.259      PureThy.add_thmss [(("size", size_thms), [])] |>>
   1.260 -    Theory.parent_path |> apsnd flat
   1.261 +    Theory.parent_path |> apsnd List.concat
   1.262    end;
   1.263  
   1.264  fun prove_weak_case_congs new_type_names descr sorts thy =