src/HOL/Tools/datatype_rep_proofs.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15574 b1d1b5bfc464
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -35,7 +35,7 @@
     1.4  
     1.5  
     1.6  fun exh_thm_of (dt_info : datatype_info Symtab.table) tname =
     1.7 -  #exhaustion (the (Symtab.lookup (dt_info, tname)));
     1.8 +  #exhaustion (valOf (Symtab.lookup (dt_info, tname)));
     1.9  
    1.10  (******************************************************************************)
    1.11  
    1.12 @@ -62,7 +62,7 @@
    1.13           "In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0",
    1.14           "Lim_inject", "Suml_inject", "Sumr_inject"];
    1.15  
    1.16 -    val descr' = flat descr;
    1.17 +    val descr' = List.concat descr;
    1.18  
    1.19      val big_name = space_implode "_" new_type_names;
    1.20      val thy1 = add_path flat_names big_name thy;
    1.21 @@ -78,11 +78,11 @@
    1.22      val branchT = if null branchTs then HOLogic.unitT
    1.23        else fold_bal (fn (T, U) => Type ("+", [T, U])) branchTs;
    1.24      val arities = get_arities descr' \ 0;
    1.25 -    val unneeded_vars = hd tyvars \\ foldr add_typ_tfree_names (leafTs' @ branchTs, []);
    1.26 -    val leafTs = leafTs' @ (map (fn n => TFree (n, the (assoc (sorts, n)))) unneeded_vars);
    1.27 +    val unneeded_vars = hd tyvars \\ Library.foldr add_typ_tfree_names (leafTs' @ branchTs, []);
    1.28 +    val leafTs = leafTs' @ (map (fn n => TFree (n, valOf (assoc (sorts, n)))) unneeded_vars);
    1.29      val recTs = get_rec_types descr' sorts;
    1.30 -    val newTs = take (length (hd descr), recTs);
    1.31 -    val oldTs = drop (length (hd descr), recTs);
    1.32 +    val newTs = Library.take (length (hd descr), recTs);
    1.33 +    val oldTs = Library.drop (length (hd descr), recTs);
    1.34      val sumT = if null leafTs then HOLogic.unitT
    1.35        else fold_bal (fn (T, U) => Type ("+", [T, U])) leafTs;
    1.36      val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT]));
    1.37 @@ -134,7 +134,7 @@
    1.38        in mk_inj branchT (length branchTs) (1 + find_index_eq T' branchTs)
    1.39        end;
    1.40  
    1.41 -    val mk_lim = foldr (fn (T, t) => Lim $ mk_fun_inj T (Abs ("x", T, t)));
    1.42 +    val mk_lim = Library.foldr (fn (T, t) => Lim $ mk_fun_inj T (Abs ("x", T, t)));
    1.43  
    1.44      (************** generate introduction rules for representing set **********)
    1.45  
    1.46 @@ -152,7 +152,7 @@
    1.47                    app_bnds (mk_Free "x" (Ts ---> Univ_elT) j) (length Ts)
    1.48                in (j + 1, list_all (map (pair "x") Ts,
    1.49                    HOLogic.mk_Trueprop (HOLogic.mk_mem (free_t,
    1.50 -                    Const (nth_elem (k, rep_set_names), UnivT)))) :: prems,
    1.51 +                    Const (List.nth (rep_set_names, k), UnivT)))) :: prems,
    1.52                  mk_lim (Ts, free_t) :: ts)
    1.53                end
    1.54            | _ =>
    1.55 @@ -160,7 +160,7 @@
    1.56                in (j + 1, prems, (Leaf $ mk_inj T (mk_Free "x" T j))::ts)
    1.57                end);
    1.58  
    1.59 -        val (_, prems, ts) = foldr mk_prem (cargs, (1, [], []));
    1.60 +        val (_, prems, ts) = Library.foldr mk_prem (cargs, (1, [], []));
    1.61          val concl = HOLogic.mk_Trueprop (HOLogic.mk_mem
    1.62            (mk_univ_inj ts n i, Const (s, UnivT)))
    1.63        in Logic.list_implies (prems, concl)
    1.64 @@ -168,7 +168,7 @@
    1.65  
    1.66      val consts = map (fn s => Const (s, UnivT)) rep_set_names;
    1.67  
    1.68 -    val intr_ts = flat (map (fn ((_, (_, _, constrs)), rep_set_name) =>
    1.69 +    val intr_ts = List.concat (map (fn ((_, (_, _, constrs)), rep_set_name) =>
    1.70        map (make_intr rep_set_name (length constrs))
    1.71          ((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names));
    1.72  
    1.73 @@ -179,21 +179,21 @@
    1.74  
    1.75      (********************************* typedef ********************************)
    1.76  
    1.77 -    val thy3 = add_path flat_names big_name (foldl (fn (thy, ((((name, mx), tvs), c), name')) =>
    1.78 +    val thy3 = add_path flat_names big_name (Library.foldl (fn (thy, ((((name, mx), tvs), c), name')) =>
    1.79        setmp TypedefPackage.quiet_mode true
    1.80          (TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) c NONE
    1.81            (rtac exI 1 THEN
    1.82              QUIET_BREADTH_FIRST (has_fewer_prems 1)
    1.83              (resolve_tac rep_intrs 1))) thy |> #1)
    1.84                (parent_path flat_names thy2, types_syntax ~~ tyvars ~~
    1.85 -                (take (length newTs, consts)) ~~ new_type_names));
    1.86 +                (Library.take (length newTs, consts)) ~~ new_type_names));
    1.87  
    1.88      (*********************** definition of constructors ***********************)
    1.89  
    1.90      val big_rep_name = (space_implode "_" new_type_names) ^ "_Rep_";
    1.91      val rep_names = map (curry op ^ "Rep_") new_type_names;
    1.92      val rep_names' = map (fn i => big_rep_name ^ (string_of_int i))
    1.93 -      (1 upto (length (flat (tl descr))));
    1.94 +      (1 upto (length (List.concat (tl descr))));
    1.95      val all_rep_names = map (Sign.intern_const (Theory.sign_of thy3)) rep_names @
    1.96        map (Sign.full_name (Theory.sign_of thy3)) rep_names';
    1.97  
    1.98 @@ -211,12 +211,12 @@
    1.99                val free_t = mk_Free "x" T j
   1.100            in (case (strip_dtyp dt, strip_type T) of
   1.101                ((_, DtRec m), (Us, U)) => (j + 1, free_t :: l_args, mk_lim (Us,
   1.102 -                Const (nth_elem (m, all_rep_names), U --> Univ_elT) $
   1.103 +                Const (List.nth (all_rep_names, m), U --> Univ_elT) $
   1.104                    app_bnds free_t (length Us)) :: r_args)
   1.105              | _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args))
   1.106            end;
   1.107  
   1.108 -        val (_, l_args, r_args) = foldr constr_arg (cargs, (1, [], []));
   1.109 +        val (_, l_args, r_args) = Library.foldr constr_arg (cargs, (1, [], []));
   1.110          val constrT = (map (typ_of_dtyp descr' sorts) cargs) ---> T;
   1.111          val abs_name = Sign.intern_const (Theory.sign_of thy) ("Abs_" ^ tname);
   1.112          val rep_name = Sign.intern_const (Theory.sign_of thy) ("Rep_" ^ tname);
   1.113 @@ -243,14 +243,14 @@
   1.114            (Const (Sign.intern_const sg ("Rep_" ^ tname), T --> Univ_elT));
   1.115          val cong' = standard (cterm_instantiate [(cterm_of sg cong_f, rep_const)] arg_cong);
   1.116          val dist = standard (cterm_instantiate [(cterm_of sg distinct_f, rep_const)] distinct_lemma);
   1.117 -        val (thy', defs', eqns', _) = foldl ((make_constr_def tname T) (length constrs))
   1.118 +        val (thy', defs', eqns', _) = Library.foldl ((make_constr_def tname T) (length constrs))
   1.119            ((add_path flat_names tname thy, defs, [], 1), constrs ~~ constr_syntax)
   1.120        in
   1.121          (parent_path flat_names thy', defs', eqns @ [eqns'],
   1.122            rep_congs @ [cong'], dist_lemmas @ [dist])
   1.123        end;
   1.124  
   1.125 -    val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = foldl dt_constr_defs
   1.126 +    val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = Library.foldl dt_constr_defs
   1.127        ((thy3 |> Theory.add_consts_i iso_decls |> parent_path flat_names, [], [], [], []),
   1.128          hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax);
   1.129  
   1.130 @@ -300,7 +300,7 @@
   1.131  
   1.132      val newT_iso_inj_thms = map prove_newT_iso_inj_thm
   1.133        (new_type_names ~~ newT_iso_axms ~~ newTs ~~
   1.134 -        take (length newTs, rep_set_names));
   1.135 +        Library.take (length newTs, rep_set_names));
   1.136  
   1.137      (********* isomorphisms between existing types and "unfolded" types *******)
   1.138  
   1.139 @@ -318,8 +318,8 @@
   1.140      fun make_iso_def k ks n ((fs, eqns, i), (cname, cargs)) =
   1.141        let
   1.142          val argTs = map (typ_of_dtyp descr' sorts) cargs;
   1.143 -        val T = nth_elem (k, recTs);
   1.144 -        val rep_name = nth_elem (k, all_rep_names);
   1.145 +        val T = List.nth (recTs, k);
   1.146 +        val rep_name = List.nth (all_rep_names, k);
   1.147          val rep_const = Const (rep_name, T --> Univ_elT);
   1.148          val constr = Const (cname, argTs ---> T);
   1.149  
   1.150 @@ -334,17 +334,17 @@
   1.151                     Ts @ [Us ---> Univ_elT])
   1.152                  else
   1.153                    (i2 + 1, i2', ts @ [mk_lim (Us,
   1.154 -                     Const (nth_elem (j, all_rep_names), U --> Univ_elT) $
   1.155 +                     Const (List.nth (all_rep_names, j), U --> Univ_elT) $
   1.156                         app_bnds (mk_Free "x" T' i2) (length Us))], Ts)
   1.157              | _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (mk_Free "x" T' i2)], Ts))
   1.158            end;
   1.159  
   1.160 -        val (i2, i2', ts, Ts) = foldl (process_arg ks) ((1, 1, [], []), cargs);
   1.161 +        val (i2, i2', ts, Ts) = Library.foldl (process_arg ks) ((1, 1, [], []), cargs);
   1.162          val xs = map (uncurry (mk_Free "x")) (argTs ~~ (1 upto (i2 - 1)));
   1.163          val ys = map (uncurry (mk_Free "y")) (Ts ~~ (1 upto (i2' - 1)));
   1.164          val f = list_abs_free (map dest_Free (xs @ ys), mk_univ_inj ts n i);
   1.165  
   1.166 -        val (_, _, ts', _) = foldl (process_arg []) ((1, 1, [], []), cargs);
   1.167 +        val (_, _, ts', _) = Library.foldl (process_arg []) ((1, 1, [], []), cargs);
   1.168          val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.169            (rep_const $ list_comb (constr, xs), mk_univ_inj ts' n i))
   1.170  
   1.171 @@ -356,16 +356,16 @@
   1.172        let
   1.173          val ks = map fst ds;
   1.174          val (_, (tname, _, _)) = hd ds;
   1.175 -        val {rec_rewrites, rec_names, ...} = the (Symtab.lookup (dt_info, tname));
   1.176 +        val {rec_rewrites, rec_names, ...} = valOf (Symtab.lookup (dt_info, tname));
   1.177  
   1.178          fun process_dt ((fs, eqns, isos), (k, (tname, _, constrs))) =
   1.179            let
   1.180 -            val (fs', eqns', _) = foldl (make_iso_def k ks (length constrs))
   1.181 +            val (fs', eqns', _) = Library.foldl (make_iso_def k ks (length constrs))
   1.182                ((fs, eqns, 1), constrs);
   1.183 -            val iso = (nth_elem (k, recTs), nth_elem (k, all_rep_names))
   1.184 +            val iso = (List.nth (recTs, k), List.nth (all_rep_names, k))
   1.185            in (fs', eqns', isos @ [iso]) end;
   1.186          
   1.187 -        val (fs, eqns, isos) = foldl process_dt (([], [], []), ds);
   1.188 +        val (fs, eqns, isos) = Library.foldl process_dt (([], [], []), ds);
   1.189          val fTs = map fastype_of fs;
   1.190          val defs = map (fn (rec_name, (T, iso_name)) => ((Sign.base_name iso_name) ^ "_def",
   1.191            equals (T --> Univ_elT) $ Const (iso_name, T --> Univ_elT) $
   1.192 @@ -380,7 +380,7 @@
   1.193  
   1.194        in (thy', char_thms' @ char_thms) end;
   1.195  
   1.196 -    val (thy5, iso_char_thms) = foldr make_iso_defs
   1.197 +    val (thy5, iso_char_thms) = Library.foldr make_iso_defs
   1.198        (tl descr, (add_path flat_names big_name thy4, []));
   1.199  
   1.200      (* prove isomorphism properties *)
   1.201 @@ -412,13 +412,13 @@
   1.202      fun prove_iso_thms (ds, (inj_thms, elem_thms)) =
   1.203        let
   1.204          val (_, (tname, _, _)) = hd ds;
   1.205 -        val {induction, ...} = the (Symtab.lookup (dt_info, tname));
   1.206 +        val {induction, ...} = valOf (Symtab.lookup (dt_info, tname));
   1.207  
   1.208          fun mk_ind_concl (i, _) =
   1.209            let
   1.210 -            val T = nth_elem (i, recTs);
   1.211 -            val Rep_t = Const (nth_elem (i, all_rep_names), T --> Univ_elT);
   1.212 -            val rep_set_name = nth_elem (i, rep_set_names)
   1.213 +            val T = List.nth (recTs, i);
   1.214 +            val Rep_t = Const (List.nth (all_rep_names, i), T --> Univ_elT);
   1.215 +            val rep_set_name = List.nth (rep_set_names, i)
   1.216            in (HOLogic.all_const T $ Abs ("y", T, HOLogic.imp $
   1.217                  HOLogic.mk_eq (Rep_t $ mk_Free "x" T i, Rep_t $ Bound 0) $
   1.218                    HOLogic.mk_eq (mk_Free "x" T i, Bound 0)),
   1.219 @@ -469,7 +469,7 @@
   1.220        in (inj_thms'' @ inj_thms, elem_thms @ (split_conj_thm elem_thm))
   1.221        end;
   1.222  
   1.223 -    val (iso_inj_thms_unfolded, iso_elem_thms) = foldr prove_iso_thms
   1.224 +    val (iso_inj_thms_unfolded, iso_elem_thms) = Library.foldr prove_iso_thms
   1.225        (tl descr, ([], map #3 newT_iso_axms));
   1.226      val iso_inj_thms = map snd newT_iso_inj_thms @ iso_inj_thms_unfolded;
   1.227  
   1.228 @@ -494,7 +494,7 @@
   1.229        iso_inj_thms_unfolded;
   1.230  
   1.231      val iso_thms = if length descr = 1 then [] else
   1.232 -      drop (length newTs, split_conj_thm
   1.233 +      Library.drop (length newTs, split_conj_thm
   1.234          (prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) iso_t) (fn _ =>
   1.235             [(indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
   1.236              REPEAT (rtac TrueI 1),
   1.237 @@ -503,7 +503,7 @@
   1.238              rewrite_goals_tac (map symmetric range_eqs),
   1.239              REPEAT (EVERY
   1.240                [REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @
   1.241 -                 flat (map (mk_funs_inv o #1) newT_iso_axms)) 1),
   1.242 +                 List.concat (map (mk_funs_inv o #1) newT_iso_axms)) 1),
   1.243                 TRY (hyp_subst_tac 1),
   1.244                 rtac (sym RS range_eqI) 1,
   1.245                 resolve_tac iso_char_thms 1])])));
   1.246 @@ -513,7 +513,7 @@
   1.247        map2 (fn (r_inj, r) => f_myinv_f OF [r_inj, r RS mp])
   1.248          (iso_inj_thms_unfolded, iso_thms);
   1.249  
   1.250 -    val Abs_inverse_thms = flat (map mk_funs_inv Abs_inverse_thms');
   1.251 +    val Abs_inverse_thms = List.concat (map mk_funs_inv Abs_inverse_thms');
   1.252  
   1.253      (******************* freeness theorems for constructors *******************)
   1.254  
   1.255 @@ -596,23 +596,23 @@
   1.256  
   1.257      fun mk_indrule_lemma ((prems, concls), ((i, _), T)) =
   1.258        let
   1.259 -        val Rep_t = Const (nth_elem (i, all_rep_names), T --> Univ_elT) $
   1.260 +        val Rep_t = Const (List.nth (all_rep_names, i), T --> Univ_elT) $
   1.261            mk_Free "x" T i;
   1.262  
   1.263          val Abs_t = if i < length newTs then
   1.264              Const (Sign.intern_const (Theory.sign_of thy6)
   1.265 -              ("Abs_" ^ (nth_elem (i, new_type_names))), Univ_elT --> T)
   1.266 +              ("Abs_" ^ (List.nth (new_type_names, i))), Univ_elT --> T)
   1.267            else Const ("Inductive.myinv", [T --> Univ_elT, Univ_elT] ---> T) $
   1.268 -            Const (nth_elem (i, all_rep_names), T --> Univ_elT)
   1.269 +            Const (List.nth (all_rep_names, i), T --> Univ_elT)
   1.270  
   1.271        in (prems @ [HOLogic.imp $ HOLogic.mk_mem (Rep_t,
   1.272 -            Const (nth_elem (i, rep_set_names), UnivT)) $
   1.273 +            Const (List.nth (rep_set_names, i), UnivT)) $
   1.274                (mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))],
   1.275            concls @ [mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ mk_Free "x" T i])
   1.276        end;
   1.277  
   1.278      val (indrule_lemma_prems, indrule_lemma_concls) =
   1.279 -      foldl mk_indrule_lemma (([], []), (descr' ~~ recTs));
   1.280 +      Library.foldl mk_indrule_lemma (([], []), (descr' ~~ recTs));
   1.281  
   1.282      val cert = cterm_of (Theory.sign_of thy6);
   1.283