# HG changeset patch
# User haftmann
# Date 1127140715 -7200
# Node ID c39871c5297751d276f4729f8dc7d0284f5b9b3b
# Parent  f6a225f97f0a74e214c7d3810750f76c38d05697
introduced AList module

diff -r f6a225f97f0a -r c39871c52977 src/HOL/Integ/cooper_dec.ML
--- 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) 
diff -r f6a225f97f0a -r c39871c52977 src/HOL/Integ/cooper_proof.ML
--- 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))  
diff -r f6a225f97f0a -r c39871c52977 src/HOL/Tools/Presburger/cooper_dec.ML
--- 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) 
diff -r f6a225f97f0a -r c39871c52977 src/HOL/Tools/Presburger/cooper_proof.ML
--- 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))  
diff -r f6a225f97f0a -r c39871c52977 src/HOL/Tools/datatype_aux.ML
--- 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")
diff -r f6a225f97f0a -r c39871c52977 src/HOL/Tools/inductive_package.ML
--- 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;
diff -r f6a225f97f0a -r c39871c52977 src/HOL/Tools/inductive_realizer.ML
--- 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;
 
diff -r f6a225f97f0a -r c39871c52977 src/HOL/Tools/record_package.ML
--- 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 *)
diff -r f6a225f97f0a -r c39871c52977 src/Pure/Isar/locale.ML
--- 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), _), _) =>