--- a/src/HOL/Integ/cooper_dec.ML Mon Sep 19 15:12:13 2005 +0200
+++ b/src/HOL/Integ/cooper_dec.ML Mon Sep 19 16:38:35 2005 +0200
@@ -483,13 +483,13 @@
fun evalc_atom at = case at of
(Const (p,_) $ s $ t) =>
- ( case assoc (operations,p) of
+ ( case AList.lookup (op =) operations p of
SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const
else HOLogic.false_const)
handle _ => at)
| _ => at)
|Const("Not",_)$(Const (p,_) $ s $ t) =>(
- case assoc (operations,p) of
+ case AList.lookup (op =) operations p of
SOME f => ((if (f ((dest_numeral s),(dest_numeral t)))
then HOLogic.false_const else HOLogic.true_const)
handle _ => at)
--- a/src/HOL/Integ/cooper_proof.ML Mon Sep 19 15:12:13 2005 +0200
+++ b/src/HOL/Integ/cooper_proof.ML Mon Sep 19 16:38:35 2005 +0200
@@ -787,7 +787,7 @@
fun rho_for_evalc sg at = case at of
(Const (p,_) $ s $ t) =>(
- case assoc (operations,p) of
+ case AList.lookup (op =) operations p of
SOME f =>
((if (f ((dest_numeral s),(dest_numeral t)))
then prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const))
@@ -795,7 +795,7 @@
handle _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl)
| _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl )
|Const("Not",_)$(Const (p,_) $ s $ t) =>(
- case assoc (operations,p) of
+ case AList.lookup (op =) operations p of
SOME f =>
((if (f ((dest_numeral s),(dest_numeral t)))
then prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const))
--- a/src/HOL/Tools/Presburger/cooper_dec.ML Mon Sep 19 15:12:13 2005 +0200
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML Mon Sep 19 16:38:35 2005 +0200
@@ -483,13 +483,13 @@
fun evalc_atom at = case at of
(Const (p,_) $ s $ t) =>
- ( case assoc (operations,p) of
+ ( case AList.lookup (op =) operations p of
SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const
else HOLogic.false_const)
handle _ => at)
| _ => at)
|Const("Not",_)$(Const (p,_) $ s $ t) =>(
- case assoc (operations,p) of
+ case AList.lookup (op =) operations p of
SOME f => ((if (f ((dest_numeral s),(dest_numeral t)))
then HOLogic.false_const else HOLogic.true_const)
handle _ => at)
--- a/src/HOL/Tools/Presburger/cooper_proof.ML Mon Sep 19 15:12:13 2005 +0200
+++ b/src/HOL/Tools/Presburger/cooper_proof.ML Mon Sep 19 16:38:35 2005 +0200
@@ -787,7 +787,7 @@
fun rho_for_evalc sg at = case at of
(Const (p,_) $ s $ t) =>(
- case assoc (operations,p) of
+ case AList.lookup (op =) operations p of
SOME f =>
((if (f ((dest_numeral s),(dest_numeral t)))
then prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const))
@@ -795,7 +795,7 @@
handle _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl)
| _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl )
|Const("Not",_)$(Const (p,_) $ s $ t) =>(
- case assoc (operations,p) of
+ case AList.lookup (op =) operations p of
SOME f =>
((if (f ((dest_numeral s),(dest_numeral t)))
then prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const))
--- a/src/HOL/Tools/datatype_aux.ML Mon Sep 19 15:12:13 2005 +0200
+++ b/src/HOL/Tools/datatype_aux.ML Mon Sep 19 16:38:35 2005 +0200
@@ -196,9 +196,7 @@
fun mk_Free s T i = Free (s ^ (string_of_int i), T);
fun subst_DtTFree _ substs (T as (DtTFree name)) =
- (case assoc (substs, name) of
- NONE => T
- | SOME U => U)
+ AList.lookup (op =) substs name |> the_default T
| subst_DtTFree i substs (DtType (name, ts)) =
DtType (name, map (subst_DtTFree i substs) ts)
| subst_DtTFree i _ (DtRec j) = DtRec (i + j);
@@ -236,15 +234,15 @@
fun dtyp_of_typ _ (TFree (n, _)) = DtTFree n
| dtyp_of_typ _ (TVar _) = error "Illegal schematic type variable(s)"
| dtyp_of_typ new_dts (Type (tname, Ts)) =
- (case assoc (new_dts, tname) of
+ (case AList.lookup (op =) new_dts tname of
NONE => DtType (tname, map (dtyp_of_typ new_dts) Ts)
| SOME vs => if map (try dest_TFree) Ts = map SOME vs then
DtRec (find_index (curry op = tname o fst) new_dts)
else error ("Illegal occurence of recursive type " ^ tname));
-fun typ_of_dtyp descr sorts (DtTFree a) = TFree (a, valOf (assoc (sorts, a)))
+fun typ_of_dtyp descr sorts (DtTFree a) = TFree (a, (the o AList.lookup (op =) sorts) a)
| typ_of_dtyp descr sorts (DtRec i) =
- let val (s, ds, _) = valOf (assoc (descr, i))
+ let val (s, ds, _) = (the o AList.lookup (op =) descr) i
in Type (s, map (typ_of_dtyp descr sorts) ds) end
| typ_of_dtyp descr sorts (DtType (s, ds)) =
Type (s, map (typ_of_dtyp descr sorts) ds);
@@ -279,7 +277,7 @@
val descr' = List.concat descr;
fun is_nonempty_dt is i =
let
- val (_, _, constrs) = valOf (assoc (descr', i));
+ val (_, _, constrs) = (the o AList.lookup (op =) descr') i;
fun arg_nonempty (_, DtRec i) = if i mem is then false
else is_nonempty_dt (i::is) i
| arg_nonempty _ = true;
@@ -303,7 +301,7 @@
NONE => typ_error T (tname ^ " is not a datatype - can't use it in\
\ nested recursion")
| (SOME {index, descr, ...}) =>
- let val (_, vars, _) = valOf (assoc (descr, index));
+ let val (_, vars, _) = (the o AList.lookup (op =) descr) index;
val subst = ((map dest_DtTFree vars) ~~ dts) handle UnequalLengths =>
typ_error T ("Type constructor " ^ tname ^ " used with wrong\
\ number of arguments")
--- a/src/HOL/Tools/inductive_package.ML Mon Sep 19 15:12:13 2005 +0200
+++ b/src/HOL/Tools/inductive_package.ML Mon Sep 19 16:38:35 2005 +0200
@@ -228,12 +228,12 @@
p :: prod_factors (1::p) t @ prod_factors (2::p) u
| prod_factors p _ = [];
-fun mg_prod_factors ts (fs, t $ u) = if t mem ts then
+fun mg_prod_factors ts (t $ u) fs = if t mem ts then
let val f = prod_factors [] u
in AList.update (op =) (t, f inter (AList.lookup (op =) fs t) |> the_default f) fs end
- else mg_prod_factors ts (mg_prod_factors ts (fs, t), u)
- | mg_prod_factors ts (fs, Abs (_, _, t)) = mg_prod_factors ts (fs, t)
- | mg_prod_factors ts (fs, _) = fs;
+ else mg_prod_factors ts u (mg_prod_factors ts t fs)
+ | mg_prod_factors ts (Abs (_, _, t)) fs = mg_prod_factors ts t fs
+ | mg_prod_factors ts _ fs = fs;
fun prodT_factors p ps (T as Type ("*", [T1, T2])) =
if p mem ps then prodT_factors (1::p) ps T1 @ prodT_factors (2::p) ps T2
@@ -265,11 +265,11 @@
val remove_split = rewrite_rule [split_conv RS eq_reflection];
fun split_rule_vars vs rl = standard (remove_split (foldr split_rule_var'
- rl (mg_prod_factors vs ([], Thm.prop_of rl))));
+ rl (mg_prod_factors vs (Thm.prop_of rl) [])));
fun split_rule vs rl = standard (remove_split (foldr split_rule_var'
rl (List.mapPartial (fn (t as Var ((a, _), _)) =>
- Option.map (pair t) (assoc (vs, a))) (term_vars (Thm.prop_of rl)))));
+ Option.map (pair t) (AList.lookup (op =) vs a)) (term_vars (Thm.prop_of rl)))));
(** process rules **)
@@ -377,7 +377,7 @@
let
val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
- val pred_of = curry (Library.gen_assoc (op aconv)) (cs ~~ preds);
+ val pred_of = AList.lookup (op aconv) (cs ~~ preds);
fun subst (s as ((m as Const ("op :", T)) $ t $ u)) =
(case pred_of u of
@@ -408,13 +408,13 @@
val ind_prems = map mk_ind_prem intr_ts;
- val factors = Library.foldl (mg_prod_factors preds) ([], ind_prems);
+ val factors = Library.fold (mg_prod_factors preds) ind_prems [];
(* make conclusions for induction rules *)
fun mk_ind_concl ((c, P), (ts, x)) =
let val T = HOLogic.dest_setT (fastype_of c);
- val ps = getOpt (assoc (factors, P), []);
+ val ps = AList.lookup (op =) factors P |> the_default [];
val Ts = prodT_factors [] ps T;
val (frees, x') = foldr (fn (T', (fs, s)) =>
((Free (s, T'))::fs, Symbol.bump_string s)) ([], x) Ts;
--- a/src/HOL/Tools/inductive_realizer.ML Mon Sep 19 15:12:13 2005 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Mon Sep 19 16:38:35 2005 +0200
@@ -112,7 +112,7 @@
val rname = space_implode "_" (s ^ "R" :: vs);
fun mk_Tprem n v =
- let val SOME T = assoc (rvs, v)
+ let val T = (the o AList.lookup (op =) rvs) v
in (Const ("typeof", T --> Type ("Type", [])) $ Var ((v, 0), T),
Extraction.mk_typ (if n then Extraction.nullT
else TVar (("'" ^ v, 0), HOLogic.typeS)))
@@ -226,7 +226,7 @@
val x = Free ("x", Extraction.etype_of thy vs [] (hd (prems_of induct)));
fun name_of_fn intr = "r" ^ Sign.base_name (Thm.name_of_thm intr);
val r' = list_abs_free (List.mapPartial (fn intr =>
- Option.map (pair (name_of_fn intr)) (assoc (frees, name_of_fn intr))) intrs,
+ Option.map (pair (name_of_fn intr)) (AList.lookup (op =) frees (name_of_fn intr))) intrs,
if length concls = 1 then r $ x else r)
in
if length concls = 1 then lambda x r' else r'
@@ -253,7 +253,7 @@
val xs = rev (Term.add_vars (prop_of rule) []);
val vs1 = map Var (filter_out (fn ((a, _), _) => a mem rvs) xs);
val rlzvs = rev (Term.add_vars (prop_of rrule) []);
- val vs2 = map (fn (ixn, _) => Var (ixn, valOf (assoc (rlzvs, ixn)))) xs;
+ val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs;
val rs = gen_rems (op = o pairself fst) (rlzvs, xs);
fun mk_prf _ [] prf = prf
@@ -270,12 +270,15 @@
(prf_of rrule, map PBound (length prems - 1 downto 0)))) vs2))
end;
-fun add_rule (rss, r) =
+fun add_rule r rss =
let
val _ $ (_ $ _ $ S) = concl_of r;
val (Const (s, _), _) = strip_comb S;
- val rs = getOpt (assoc (rss, s), []);
- in AList.update (op =) (s, rs @ [r]) rss end;
+ in
+ rss
+ |> AList.default (op =) (s, [])
+ |> AList.map_entry (op =) s (fn rs => rs @ [r])
+ end;
fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) =
let
@@ -284,7 +287,7 @@
val (_ $ (_ $ _ $ S)) = Logic.strip_imp_concl (prop_of (hd intrs));
val (_, params) = strip_comb S;
val params' = map dest_Var params;
- val rss = Library.foldl add_rule ([], intrs);
+ val rss = [] |> Library.fold add_rule intrs;
val (prfx, _) = split_last (NameSpace.unpack (fst (hd rss)));
val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
--- a/src/HOL/Tools/record_package.ML Mon Sep 19 15:12:13 2005 +0200
+++ b/src/HOL/Tools/record_package.ML Mon Sep 19 16:38:35 2005 +0200
@@ -2054,7 +2054,7 @@
(* args *)
val defaultS = Sign.defaultS sign;
- val args = map (fn x => (x, getOpt (assoc (envir, x), defaultS))) params;
+ val args = map (fn x => (x, AList.lookup (op =) envir x |> the_default defaultS)) params;
(* errors *)
--- a/src/Pure/Isar/locale.ML Mon Sep 19 15:12:13 2005 +0200
+++ b/src/Pure/Isar/locale.ML Mon Sep 19 16:38:35 2005 +0200
@@ -205,7 +205,7 @@
else thm |> Drule.implies_intr_list (map cert hyps)
|> Drule.tvars_intr_list (map #1 tinst')
|> (fn (th, al) => th |> Thm.instantiate
- ((map (fn (a, T) => (certT (TVar (valOf (assoc (al, a)))), certT T)) tinst'),
+ ((map (fn (a, T) => (certT (TVar ((the o AList.lookup (op =) al) a)), certT T)) tinst'),
[]))
|> (fn th => Drule.implies_elim_list th
(map (Thm.assume o cert o tinst_tab_term tinst) hyps))
@@ -251,7 +251,7 @@
else thm |> Drule.implies_intr_list (map cert hyps)
|> Drule.tvars_intr_list (map #1 tinst')
|> (fn (th, al) => th |> Thm.instantiate
- ((map (fn (a, T) => (certT (TVar (valOf (assoc (al, a)))), certT T)) tinst'),
+ ((map (fn (a, T) => (certT (TVar ((the o AList.lookup (op =) al) a)), certT T)) tinst'),
[]))
|> Drule.forall_intr_list (map (cert o #1) inst')
|> Drule.forall_elim_list (map (cert o #2) inst')
@@ -691,7 +691,7 @@
(* type instantiation *)
fun inst_type [] T = T
- | inst_type env T = Term.map_type_tfree (fn v => getOpt (assoc (env, v), TFree v)) T;
+ | inst_type env T = Term.map_type_tfree (fn v => AList.lookup (op =) env v |> the_default (TFree v)) T;
fun inst_term [] t = t
| inst_term env t = Term.map_term_types (inst_type env) t;
@@ -713,7 +713,7 @@
|> Drule.tvars_intr_list (map (#1 o #1) env')
|> (fn (th', al) => th' |>
Thm.instantiate ((map (fn ((a, _), T) =>
- (certT (TVar (valOf (assoc (al, a)))), certT T)) env'), []))
+ (certT (TVar ((the o AList.lookup (op =) al) a)), certT T)) env'), []))
|> (fn th'' => Drule.implies_elim_list th''
(map (Thm.assume o cert o inst_term env') hyps))
end;
@@ -941,7 +941,7 @@
((name, map (rename ren) ps), ths)) regs;
val new_regs = gen_rems eq_fst (regs', ids);
val new_ids = map fst new_regs;
- val new_idTs = map (apsnd (map (fn p => (p, valOf (assoc (ps, p)))))) new_ids;
+ val new_idTs = map (apsnd (map (fn p => (p, (the o AList.lookup (op =) ps) p)))) new_ids;
val new_ths = map (fn (_, ths') =>
map (Drule.satisfy_hyps ths o rename_thm ren o inst_thm ctxt env) ths') new_regs;
@@ -1048,7 +1048,7 @@
val all_params' = params_of' elemss;
val all_params = param_types all_params';
val elemss' = map (fn (((name, _), (ps, mode)), elems) =>
- (((name, map (fn p => (p, assoc (all_params, p))) ps), mode), elems))
+ (((name, map (fn p => (p, AList.lookup (op =) all_params p)) ps), mode), elems))
elemss;
fun inst_th th = let
val {hyps, prop, ...} = Thm.rep_thm th;
@@ -1423,7 +1423,7 @@
If so, which are these??? *)
fun finish_parms parms (((name, ps), mode), elems) =
- (((name, map (fn (x, _) => (x, assoc (parms, x))) ps), mode), elems);
+ (((name, map (fn (x, _) => (x, AList.lookup (op =) parms x)) ps), mode), elems);
fun finish_elems ctxt parms _ ((text, wits), ((id, Int e), _)) =
let
@@ -1582,7 +1582,7 @@
context fixed_params (raw_import_elemss @ raw_elemss) raw_concl;
(* replace extended ids (for axioms) by ids *)
val all_elemss' = map (fn (((_, ps), _), (((n, ps'), mode), elems)) =>
- (((n, map (fn p => (p, assoc (ps', p) |> valOf)) ps), mode), elems))
+ (((n, map (fn p => (p, (the o AList.lookup (op =) ps') p)) ps), mode), elems))
(ids ~~ all_elemss);
(* CB: all_elemss and parms contain the correct parameter types *)
@@ -2229,7 +2229,7 @@
val (given_ps, given_insts) = split_list given;
val tvars = foldr Term.add_typ_tvars [] pvTs;
val used = foldr Term.add_typ_varnames [] pvTs;
- fun sorts (a, i) = assoc (tvars, (a, i));
+ fun sorts (a, i) = AList.lookup (op =) tvars (a, i);
val (vs, vinst) = read_terms thy_ctxt sorts used given_insts;
val vars = foldl Term.add_term_tvar_ixns [] vs \\ map fst tvars;
val vars' = fold Term.add_term_varnames vs vars;
@@ -2242,7 +2242,7 @@
val renameT =
if is_local then I
else Type.unvarifyT o Term.map_type_tfree (fn (a, s) =>
- TFree (valOf (assoc (new_Tnames ~~ new_Tnames', a)), s));
+ TFree ((the o AList.lookup (op =) (new_Tnames ~~ new_Tnames')) a, s));
val rename =
if is_local then I
else Term.map_term_types renameT;
@@ -2269,7 +2269,7 @@
(* restore "small" ids *)
val ids' = map (fn ((n, ps), (_, mode)) =>
- ((n, map (fn p => Free (p, valOf (assoc (parms, p)))) ps), mode)) ids;
+ ((n, map (fn p => Free (p, (the o AList.lookup (op =) parms) p)) ps), mode)) ids;
(* instantiate ids and elements *)
val inst_elemss = map
(fn ((id, _), ((_, mode), elems)) =>
@@ -2348,8 +2348,8 @@
fun activate_reg (vts, ((prfx, atts2), _)) thy = let
val ((inst, tinst), wits) =
collect_global_witnesses thy fixed t_ids vts;
- fun inst_parms ps = map (fn p =>
- valOf (assoc (map #1 fixed ~~ vts, p))) ps;
+ fun inst_parms ps = map
+ (the o AList.lookup (op =) (map #1 fixed ~~ vts)) ps;
val disch = Drule.fconv_rule (Thm.beta_conversion true) o
Drule.satisfy_hyps wits;
val new_elemss = List.filter (fn (((name, ps), _), _) =>