canonical member/insert/merge;
authorwenzelm
Fri Feb 03 23:12:28 2006 +0100 (2006-02-03 ago)
changeset 18921f47c46d7d654
parent 18920 7635e0060cd4
child 18922 b05a2952de73
canonical member/insert/merge;
src/HOL/Import/hol4rews.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/specification_package.ML
src/Pure/General/graph.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/method.ML
src/Pure/Isar/net_rules.ML
src/Pure/Proof/extraction.ML
src/Pure/Syntax/syntax.ML
src/Pure/search.ML
     1.1 --- a/src/HOL/Import/hol4rews.ML	Fri Feb 03 17:08:03 2006 +0100
     1.2 +++ b/src/HOL/Import/hol4rews.ML	Fri Feb 03 23:12:28 2006 +0100
     1.3 @@ -264,7 +264,7 @@
     1.4  	val _ = message "Adding HOL4 rewrite"
     1.5  	val th1 = th RS eq_reflection
     1.6  	val current_rews = HOL4Rewrites.get thy
     1.7 -	val new_rews = gen_ins Thm.eq_thm (th1,current_rews)
     1.8 +	val new_rews = insert Thm.eq_thm th1 current_rews
     1.9  	val updated_thy  = HOL4Rewrites.put new_rews thy
    1.10      in
    1.11  	(Context.Theory updated_thy,th1)
     2.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Feb 03 17:08:03 2006 +0100
     2.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Feb 03 23:12:28 2006 +0100
     2.3 @@ -148,8 +148,8 @@
     2.4  
     2.5  (* attributes *)
     2.6  
     2.7 -val mono_add = Thm.declaration_attribute (map_monos o Drule.add_rules o mk_mono);
     2.8 -val mono_del = Thm.declaration_attribute (map_monos o Drule.del_rules o mk_mono);
     2.9 +val mono_add = Thm.declaration_attribute (map_monos o fold Drule.add_rule o mk_mono);
    2.10 +val mono_del = Thm.declaration_attribute (map_monos o fold Drule.del_rule o mk_mono);
    2.11  
    2.12  
    2.13  
     3.1 --- a/src/HOL/Tools/specification_package.ML	Fri Feb 03 17:08:03 2006 +0100
     3.2 +++ b/src/HOL/Tools/specification_package.ML	Fri Feb 03 23:12:28 2006 +0100
     3.3 @@ -95,7 +95,7 @@
     3.4  
     3.5  fun collect_consts (        t $ u,tms) = collect_consts (u,collect_consts (t,tms))
     3.6    | collect_consts (   Abs(_,_,t),tms) = collect_consts (t,tms)
     3.7 -  | collect_consts (tm as Const _,tms) = gen_ins (op aconv) (tm,tms)
     3.8 +  | collect_consts (tm as Const _,tms) = insert (op aconv) tm tms
     3.9    | collect_consts (            _,tms) = tms
    3.10  
    3.11  (* Complementing Type.varify... *)
     4.1 --- a/src/Pure/General/graph.ML	Fri Feb 03 17:08:03 2006 +0100
     4.2 +++ b/src/Pure/General/graph.ML	Fri Feb 03 23:12:28 2006 +0100
     4.3 @@ -55,9 +55,7 @@
     4.4  
     4.5  val eq_key = equal EQUAL o Key.ord;
     4.6  
     4.7 -infix mem_key;
     4.8 -val op mem_key = gen_mem eq_key;
     4.9 -
    4.10 +val member_key = member eq_key;
    4.11  val remove_key = remove eq_key;
    4.12  
    4.13  
    4.14 @@ -68,11 +66,8 @@
    4.15  
    4.16  val empty_keys = Table.empty: keys;
    4.17  
    4.18 -infix mem_keys;
    4.19 -fun x mem_keys tab = Table.defined (tab: keys) x;
    4.20 -
    4.21 -infix ins_keys;
    4.22 -fun x ins_keys tab = Table.insert (K true) (x, ()) (tab: keys);
    4.23 +fun member_keys tab = Table.defined (tab: keys);
    4.24 +fun insert_keys x tab = Table.insert (K true) (x, ()) (tab: keys);
    4.25  
    4.26  
    4.27  (* graphs *)
    4.28 @@ -126,8 +121,8 @@
    4.29  fun reachable next xs =
    4.30    let
    4.31      fun reach x (rs, R) =
    4.32 -      if x mem_keys R then (rs, R)
    4.33 -      else apfst (cons x) (fold reach (next x) (rs, x ins_keys R))
    4.34 +      if member_keys R x then (rs, R)
    4.35 +      else apfst (cons x) (fold reach (next x) (rs, insert_keys x R))
    4.36    in fold_map (fn x => reach x o pair []) xs empty_keys end;
    4.37  
    4.38  (*immediate*)
    4.39 @@ -161,7 +156,7 @@
    4.40      val (_, X) = reachable (imm_succs G) [x];
    4.41      fun paths ps p =
    4.42        if not (null ps) andalso eq_key (p, x) then [p :: ps]
    4.43 -      else if p mem_keys X andalso not (p mem_key ps)
    4.44 +      else if member_keys X p andalso not (member_key ps p)
    4.45        then List.concat (map (paths (p :: ps)) (imm_preds G p))
    4.46        else [];
    4.47    in paths [] y end;
    4.48 @@ -184,7 +179,7 @@
    4.49  
    4.50  (* edges *)
    4.51  
    4.52 -fun is_edge G (x, y) = y mem_key imm_succs G x handle UNDEF _ => false;
    4.53 +fun is_edge G (x, y) = member_key (imm_succs G x) y handle UNDEF _ => false;
    4.54  
    4.55  fun add_edge (x, y) G =
    4.56    if is_edge G (x, y) then G
     5.1 --- a/src/Pure/Isar/context_rules.ML	Fri Feb 03 17:08:03 2006 +0100
     5.2 +++ b/src/Pure/Isar/context_rules.ML	Fri Feb 03 23:12:28 2006 +0100
     5.3 @@ -104,9 +104,9 @@
     5.4        Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) =
     5.5      let
     5.6        val wrappers =
     5.7 -        (gen_merge_lists' (eq_snd (op =)) ws1 ws2, gen_merge_lists' (eq_snd (op =)) ws1' ws2');
     5.8 -      val rules = gen_merge_lists' (fn ((_, (k1, th1)), (_, (k2, th2))) =>
     5.9 -          k1 = k2 andalso Drule.eq_thm_prop (th1, th2)) rules1 rules2;
    5.10 +        (Library.merge (eq_snd (op =)) (ws1, ws2), Library.merge (eq_snd (op =)) (ws1', ws2'));
    5.11 +      val rules = Library.merge (fn ((_, (k1, th1)), (_, (k2, th2))) =>
    5.12 +          k1 = k2 andalso Drule.eq_thm_prop (th1, th2)) (rules1, rules2);
    5.13        val next = ~ (length rules);
    5.14        val netpairs = Library.foldl (fn (nps, (n, (w, ((i, b), th)))) =>
    5.15            nth_map i (curry insert_tagged_brl ((w, n), (b, th))) nps)
     6.1 --- a/src/Pure/Isar/method.ML	Fri Feb 03 17:08:03 2006 +0100
     6.2 +++ b/src/Pure/Isar/method.ML	Fri Feb 03 23:12:28 2006 +0100
     6.3 @@ -325,8 +325,8 @@
     6.4      val ps = Logic.strip_assums_hyp g;
     6.5      val c = Logic.strip_assums_concl g;
     6.6    in
     6.7 -    if gen_mem (fn ((ps1, c1), (ps2, c2)) =>
     6.8 -      c1 aconv c2 andalso gen_eq_set op aconv ps1 ps2) ((ps, c), gs) then no_tac
     6.9 +    if member (fn ((ps1, c1), (ps2, c2)) =>
    6.10 +      c1 aconv c2 andalso gen_eq_set op aconv ps1 ps2) gs (ps, c) then no_tac
    6.11      else (step_tac ctxt THEN_ALL_NEW intprover_tac ctxt ((ps, c) :: gs) (d + 1) lim) i
    6.12    end);
    6.13  
     7.1 --- a/src/Pure/Isar/net_rules.ML	Fri Feb 03 17:08:03 2006 +0100
     7.2 +++ b/src/Pure/Isar/net_rules.ML	Fri Feb 03 23:12:28 2006 +0100
     7.3 @@ -50,7 +50,7 @@
     7.4      (Net.insert_term (K false) (index rule, (next, rule)) net);
     7.5  
     7.6  fun merge (Rules {eq, index, rules = rules1, ...}, Rules {rules = rules2, ...}) =
     7.7 -  let val rules = Library.gen_merge_lists' eq rules1 rules2
     7.8 +  let val rules = Library.merge eq (rules1, rules2)
     7.9    in fold_rev add rules (init eq index) end;
    7.10  
    7.11  fun delete rule (rs as Rules {eq, index, rules, next, net}) =
     8.1 --- a/src/Pure/Proof/extraction.ML	Fri Feb 03 17:08:03 2006 +0100
     8.2 +++ b/src/Pure/Proof/extraction.ML	Fri Feb 03 23:12:28 2006 +0100
     8.3 @@ -374,7 +374,7 @@
     8.4           typeof_eqns = add_rule (([],
     8.5             Logic.dest_equals (prop_of (Drule.abs_def thm))), typeof_eqns),
     8.6           types = types,
     8.7 -         realizers = realizers, defs = gen_ins eq_thm (thm, defs),
     8.8 +         realizers = realizers, defs = insert eq_thm thm defs,
     8.9           expand = expand, prep = prep}
    8.10        else
    8.11          {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
     9.1 --- a/src/Pure/Syntax/syntax.ML	Fri Feb 03 17:08:03 2006 +0100
     9.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Feb 03 23:12:28 2006 +0100
     9.3 @@ -218,8 +218,8 @@
     9.4      ({input = if inout then xprods @ input else input,
     9.5        lexicon = if inout then Scan.extend_lexicon lexicon (SynExt.delims_of xprods) else lexicon,
     9.6        gram = if inout then Parser.extend_gram gram xprods else gram,
     9.7 -      consts = merge_lists' consts1 consts2,
     9.8 -      prmodes = mode ins_string (merge_lists' prmodes1 prmodes2),
     9.9 +      consts = Library.merge (op =) (consts1, consts2),
    9.10 +      prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)),
    9.11        parse_ast_trtab =
    9.12          extend_trtab "parse ast translation" parse_ast_translation parse_ast_trtab,
    9.13        parse_ruletab = extend_ruletab parse_rules parse_ruletab,
    9.14 @@ -278,11 +278,11 @@
    9.15        print_ast_trtab = print_ast_trtab2, tokentrtab = tokentrtab2, prtabs = prtabs2} = tabs2;
    9.16    in
    9.17      Syntax
    9.18 -    ({input = merge_lists' input1 input2,
    9.19 +    ({input = Library.merge (op =) (input1, input2),
    9.20        lexicon = Scan.merge_lexicons lexicon1 lexicon2,
    9.21        gram = Parser.merge_grams gram1 gram2,
    9.22        consts = sort_distinct string_ord (consts1 @ consts2),
    9.23 -      prmodes = merge_lists prmodes1 prmodes2,
    9.24 +      prmodes = Library.merge (op =) (prmodes1, prmodes2),
    9.25        parse_ast_trtab =
    9.26          merge_trtabs "parse ast translation" parse_ast_trtab1 parse_ast_trtab2,
    9.27        parse_ruletab = merge_ruletabs parse_ruletab1 parse_ruletab2,
    10.1 --- a/src/Pure/search.ML	Fri Feb 03 17:08:03 2006 +0100
    10.2 +++ b/src/Pure/search.ML	Fri Feb 03 23:12:28 2006 +0100
    10.3 @@ -63,7 +63,7 @@
    10.4  	  case Seq.pull q of
    10.5  	      NONE         => depth used qs
    10.6  	    | SOME(st,stq) => 
    10.7 -		if satp st andalso not (gen_mem eq_thm (st, used))
    10.8 +		if satp st andalso not (member eq_thm used st)
    10.9  		then SOME(st, Seq.make
   10.10  			         (fn()=> depth (st::used) (stq::qs)))
   10.11  		else depth used (tac st :: stq :: qs)