src/HOL/Tools/inductive_realizer.ML
changeset 17485 c39871c52977
parent 17325 d9d50222808e
child 17959 8db36a108213
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Mon Sep 19 15:12:13 2005 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Mon Sep 19 16:38:35 2005 +0200
     1.3 @@ -112,7 +112,7 @@
     1.4      val rname = space_implode "_" (s ^ "R" :: vs);
     1.5  
     1.6      fun mk_Tprem n v =
     1.7 -      let val SOME T = assoc (rvs, v)
     1.8 +      let val T = (the o AList.lookup (op =) rvs) v
     1.9        in (Const ("typeof", T --> Type ("Type", [])) $ Var ((v, 0), T),
    1.10          Extraction.mk_typ (if n then Extraction.nullT
    1.11            else TVar (("'" ^ v, 0), HOLogic.typeS)))
    1.12 @@ -226,7 +226,7 @@
    1.13        val x = Free ("x", Extraction.etype_of thy vs [] (hd (prems_of induct)));
    1.14        fun name_of_fn intr = "r" ^ Sign.base_name (Thm.name_of_thm intr);
    1.15        val r' = list_abs_free (List.mapPartial (fn intr =>
    1.16 -        Option.map (pair (name_of_fn intr)) (assoc (frees, name_of_fn intr))) intrs,
    1.17 +        Option.map (pair (name_of_fn intr)) (AList.lookup (op =) frees (name_of_fn intr))) intrs,
    1.18            if length concls = 1 then r $ x else r)
    1.19      in
    1.20        if length concls = 1 then lambda x r' else r'
    1.21 @@ -253,7 +253,7 @@
    1.22      val xs = rev (Term.add_vars (prop_of rule) []);
    1.23      val vs1 = map Var (filter_out (fn ((a, _), _) => a mem rvs) xs);
    1.24      val rlzvs = rev (Term.add_vars (prop_of rrule) []);
    1.25 -    val vs2 = map (fn (ixn, _) => Var (ixn, valOf (assoc (rlzvs, ixn)))) xs;
    1.26 +    val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs;
    1.27      val rs = gen_rems (op = o pairself fst) (rlzvs, xs);
    1.28  
    1.29      fun mk_prf _ [] prf = prf
    1.30 @@ -270,12 +270,15 @@
    1.31        (prf_of rrule, map PBound (length prems - 1 downto 0)))) vs2))
    1.32    end;
    1.33  
    1.34 -fun add_rule (rss, r) =
    1.35 +fun add_rule r rss =
    1.36    let
    1.37      val _ $ (_ $ _ $ S) = concl_of r;
    1.38      val (Const (s, _), _) = strip_comb S;
    1.39 -    val rs = getOpt (assoc (rss, s), []);
    1.40 -  in AList.update (op =) (s, rs @ [r]) rss end;
    1.41 +  in
    1.42 +    rss
    1.43 +    |> AList.default (op =) (s, [])
    1.44 +    |> AList.map_entry (op =) s (fn rs => rs @ [r])
    1.45 +  end;
    1.46  
    1.47  fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) =
    1.48    let
    1.49 @@ -284,7 +287,7 @@
    1.50      val (_ $ (_ $ _ $ S)) = Logic.strip_imp_concl (prop_of (hd intrs));
    1.51      val (_, params) = strip_comb S;
    1.52      val params' = map dest_Var params;
    1.53 -    val rss = Library.foldl add_rule ([], intrs);
    1.54 +    val rss = [] |> Library.fold add_rule intrs;
    1.55      val (prfx, _) = split_last (NameSpace.unpack (fst (hd rss)));
    1.56      val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
    1.57