src/HOL/Tools/datatype_realizer.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15574 b1d1b5bfc464
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -53,23 +53,23 @@
     1.4  
     1.5      fun make_pred i T U r x =
     1.6        if i mem is then
     1.7 -        Free (nth_elem (i, pnames), T --> U --> HOLogic.boolT) $ r $ x
     1.8 -      else Free (nth_elem (i, pnames), U --> HOLogic.boolT) $ x;
     1.9 +        Free (List.nth (pnames, i), T --> U --> HOLogic.boolT) $ r $ x
    1.10 +      else Free (List.nth (pnames, i), U --> HOLogic.boolT) $ x;
    1.11  
    1.12      fun mk_all i s T t =
    1.13        if i mem is then list_all_free ([(s, T)], t) else t;
    1.14  
    1.15 -    val (prems, rec_fns) = split_list (flat (snd (foldl_map
    1.16 +    val (prems, rec_fns) = split_list (List.concat (snd (foldl_map
    1.17        (fn (j, ((i, (_, _, constrs)), T)) => foldl_map (fn (j, (cname, cargs)) =>
    1.18          let
    1.19            val Ts = map (typ_of_dtyp descr sorts) cargs;
    1.20            val tnames = variantlist (DatatypeProp.make_tnames Ts, pnames);
    1.21 -          val recs = filter (is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
    1.22 +          val recs = List.filter (is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
    1.23            val frees = tnames ~~ Ts;
    1.24  
    1.25            fun mk_prems vs [] = 
    1.26                  let
    1.27 -                  val rT = nth_elem (i, rec_result_Ts);
    1.28 +                  val rT = List.nth (rec_result_Ts, i);
    1.29                    val vs' = filter_out is_unit vs;
    1.30                    val f = mk_Free "f" (map fastype_of vs' ---> rT) j;
    1.31                    val f' = Pattern.eta_contract (list_abs_free
    1.32 @@ -83,7 +83,7 @@
    1.33                    val k = body_index dt;
    1.34                    val (Us, U) = strip_type T;
    1.35                    val i = length Us;
    1.36 -                  val rT = nth_elem (k, rec_result_Ts);
    1.37 +                  val rT = List.nth (rec_result_Ts, k);
    1.38                    val r = Free ("r" ^ s, Us ---> rT);
    1.39                    val (p, f) = mk_prems (vs @ [r]) ds
    1.40                  in (mk_all k ("r" ^ s) (Us ---> rT) (Logic.mk_implies
    1.41 @@ -107,7 +107,7 @@
    1.42        (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Bound 0) (Bound 0)))
    1.43          (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names);
    1.44      val r = if null is then Extraction.nullt else
    1.45 -      foldr1 HOLogic.mk_prod (mapfilter (fn (((((i, _), T), U), s), tname) =>
    1.46 +      foldr1 HOLogic.mk_prod (List.mapPartial (fn (((((i, _), T), U), s), tname) =>
    1.47          if i mem is then SOME
    1.48            (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Free (tname, T))
    1.49          else NONE) (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names ~~ tnames));
    1.50 @@ -130,22 +130,22 @@
    1.51  
    1.52      val {path, ...} = Sign.rep_sg sg;
    1.53      val ind_name = Thm.name_of_thm induction;
    1.54 -    val vs = map (fn i => nth_elem (i, pnames)) is;
    1.55 +    val vs = map (fn i => List.nth (pnames, i)) is;
    1.56      val (thy', thm') = thy
    1.57        |> Theory.absolute_path
    1.58        |> PureThy.store_thm
    1.59          ((space_implode "_" (ind_name :: vs @ ["correctness"]), thm), [])
    1.60 -      |>> Theory.add_path (NameSpace.pack (if_none path []));
    1.61 +      |>> Theory.add_path (NameSpace.pack (getOpt (path,[])));
    1.62  
    1.63      val ivs = Drule.vars_of_terms
    1.64        [Logic.varify (DatatypeProp.make_ind [descr] sorts)];
    1.65      val rvs = Drule.vars_of_terms [prop_of thm'];
    1.66      val ivs1 = map Var (filter_out (fn (_, T) =>
    1.67        tname_of (body_type T) mem ["set", "bool"]) ivs);
    1.68 -    val ivs2 = map (fn (ixn, _) => Var (ixn, the (assoc (rvs, ixn)))) ivs;
    1.69 +    val ivs2 = map (fn (ixn, _) => Var (ixn, valOf (assoc (rvs, ixn)))) ivs;
    1.70  
    1.71 -    val prf = foldr forall_intr_prf (ivs2,
    1.72 -      foldr (fn ((f, p), prf) =>
    1.73 +    val prf = Library.foldr forall_intr_prf (ivs2,
    1.74 +      Library.foldr (fn ((f, p), prf) =>
    1.75          (case head_of (strip_abs_body f) of
    1.76             Free (s, T) =>
    1.77               let val T' = Type.varifyT T
    1.78 @@ -156,7 +156,7 @@
    1.79             (rec_fns ~~ prems_of thm, Proofterm.proof_combP
    1.80               (prf_of thm', map PBound (length prems - 1 downto 0))));
    1.81  
    1.82 -    val r' = if null is then r else Logic.varify (foldr (uncurry lambda)
    1.83 +    val r' = if null is then r else Logic.varify (Library.foldr (uncurry lambda)
    1.84        (map Logic.unvarify ivs1 @ filter_out is_unit
    1.85          (map (head_of o strip_abs_body) rec_fns), r));
    1.86  
    1.87 @@ -184,7 +184,7 @@
    1.88        end;
    1.89  
    1.90      val SOME (_, _, constrs) = assoc (descr, index);
    1.91 -    val T = nth_elem (index, get_rec_types descr sorts);
    1.92 +    val T = List.nth (get_rec_types descr sorts, index);
    1.93      val (rs, prems) = split_list (map (make_casedist_prem T) constrs);
    1.94      val r = Const (case_name, map fastype_of rs ---> T --> rT);
    1.95  
    1.96 @@ -205,11 +205,11 @@
    1.97      val (thy', thm') = thy
    1.98        |> Theory.absolute_path
    1.99        |> PureThy.store_thm ((exh_name ^ "_P_correctness", thm), [])
   1.100 -      |>> Theory.add_path (NameSpace.pack (if_none path []));
   1.101 +      |>> Theory.add_path (NameSpace.pack (getOpt (path,[])));
   1.102  
   1.103      val P = Var (("P", 0), rT' --> HOLogic.boolT);
   1.104      val prf = forall_intr_prf (y, forall_intr_prf (P,
   1.105 -      foldr (fn ((p, r), prf) =>
   1.106 +      Library.foldr (fn ((p, r), prf) =>
   1.107          forall_intr_prf (Logic.varify r, AbsP ("H", SOME (Logic.varify p),
   1.108            prf))) (prems ~~ rs, Proofterm.proof_combP (prf_of thm',
   1.109              map PBound (length prems - 1 downto 0)))));
   1.110 @@ -225,8 +225,8 @@
   1.111  
   1.112  fun add_dt_realizers sorts infos thy = if !proofs < 2 then thy else
   1.113    (message "Adding realizers for induction and case analysis ..."; thy
   1.114 -   |> curry (foldr (make_ind sorts (hd infos)))
   1.115 +   |> curry (Library.foldr (make_ind sorts (hd infos)))
   1.116       (subsets 0 (length (#descr (hd infos)) - 1))
   1.117 -   |> curry (foldr (make_casedists sorts)) infos);
   1.118 +   |> curry (Library.foldr (make_casedists sorts)) infos);
   1.119  
   1.120  end;