# HG changeset patch
# User wenzelm
# Date 1237295563 -3600
# Node ID 0cc3b7f03ade4d757e79e3456d79ba4c3d7cde51
# Parent  e5987a7ac5dfa5219b0f2578a3184f0a5d3e6460
adapted to general Item_Net;

diff -r e5987a7ac5df -r 0cc3b7f03ade src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Tue Mar 17 14:12:06 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Tue Mar 17 14:12:43 2009 +0100
@@ -91,13 +91,13 @@
 
 structure FundefData = GenericDataFun
 (
-  type T = (term * fundef_context_data) NetRules.T;
-  val empty = NetRules.init
+  type T = (term * fundef_context_data) Item_Net.T;
+  val empty = Item_Net.init
     (op aconv o pairself fst : (term * fundef_context_data) * (term * fundef_context_data) -> bool)
     fst;
   val copy = I;
   val extend = I;
-  fun merge _ (tab1, tab2) = NetRules.merge (tab1, tab2)
+  fun merge _ (tab1, tab2) = Item_Net.merge (tab1, tab2)
 );
 
 val get_fundef = FundefData.get o Context.Proof;
@@ -122,11 +122,11 @@
           SOME (morph_fundef_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))
           handle Pattern.MATCH => NONE
     in 
-      get_first match (NetRules.retrieve (get_fundef ctxt) t)
+      get_first match (Item_Net.retrieve (get_fundef ctxt) t)
     end
 
 fun import_last_fundef ctxt =
-    case NetRules.rules (get_fundef ctxt) of
+    case Item_Net.content (get_fundef ctxt) of
       [] => NONE
     | (t, data) :: _ =>
       let 
@@ -135,10 +135,10 @@
         import_fundef_data t' ctxt'
       end
 
-val all_fundef_data = NetRules.rules o get_fundef
+val all_fundef_data = Item_Net.content o get_fundef
 
 fun add_fundef_data (data as FundefCtxData {fs, termination, ...}) =
-    FundefData.map (fold (fn f => NetRules.insert (f, data)) fs)
+    FundefData.map (fold (fn f => Item_Net.insert (f, data)) fs)
     #> store_termination_rule termination
 
 
diff -r e5987a7ac5df -r 0cc3b7f03ade src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Tue Mar 17 14:12:06 2009 +0100
+++ b/src/Pure/Isar/calculation.ML	Tue Mar 17 14:12:43 2009 +0100
@@ -29,18 +29,18 @@
 
 structure CalculationData = GenericDataFun
 (
-  type T = (thm NetRules.T * thm list) * (thm list * int) option;
-  val empty = ((NetRules.elim, []), NONE);
+  type T = (thm Item_Net.T * thm list) * (thm list * int) option;
+  val empty = ((Thm.elim_rules, []), NONE);
   val extend = I;
 
   fun merge _ (((trans1, sym1), _), ((trans2, sym2), _)) =
-    ((NetRules.merge (trans1, trans2), Thm.merge_thms (sym1, sym2)), NONE);
+    ((Item_Net.merge (trans1, trans2), Thm.merge_thms (sym1, sym2)), NONE);
 );
 
 fun print_rules ctxt =
   let val ((trans, sym), _) = CalculationData.get (Context.Proof ctxt) in
     [Pretty.big_list "transitivity rules:"
-        (map (ProofContext.pretty_thm ctxt) (NetRules.rules trans)),
+        (map (ProofContext.pretty_thm ctxt) (Item_Net.content trans)),
       Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)]
     |> Pretty.chunks |> Pretty.writeln
   end;
@@ -66,8 +66,8 @@
 
 (* add/del rules *)
 
-val trans_add = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.insert);
-val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.delete);
+val trans_add = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.insert);
+val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.delete);
 
 val sym_add =
   Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.add_thm)
@@ -130,8 +130,8 @@
     fun combine ths =
       (case opt_rules of SOME rules => rules
       | NONE =>
-          (case ths of [] => NetRules.rules (#1 (get_rules state))
-          | th :: _ => NetRules.retrieve (#1 (get_rules state)) (strip_assums_concl th)))
+          (case ths of [] => Item_Net.content (#1 (get_rules state))
+          | th :: _ => Item_Net.retrieve (#1 (get_rules state)) (strip_assums_concl th)))
       |> Seq.of_list |> Seq.maps (Drule.multi_resolve ths)
       |> Seq.filter (not o projection ths);
 
diff -r e5987a7ac5df -r 0cc3b7f03ade src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Tue Mar 17 14:12:06 2009 +0100
+++ b/src/Pure/more_thm.ML	Tue Mar 17 14:12:43 2009 +0100
@@ -33,6 +33,8 @@
   val add_thm: thm -> thm list -> thm list
   val del_thm: thm -> thm list -> thm list
   val merge_thms: thm list * thm list -> thm list
+  val intro_rules: thm Item_Net.T
+  val elim_rules: thm Item_Net.T
   val elim_implies: thm -> thm -> thm
   val forall_elim_var: int -> thm -> thm
   val forall_elim_vars: int -> thm -> thm
@@ -213,6 +215,12 @@
 val merge_thms = merge eq_thm_prop;
 
 
+(* indexed collections *)
+
+val intro_rules = Item_Net.init eq_thm_prop Thm.concl_of;
+val elim_rules = Item_Net.init eq_thm_prop Thm.major_prem_of;
+
+
 
 (** basic derived rules **)
 
diff -r e5987a7ac5df -r 0cc3b7f03ade src/Tools/induct.ML
--- a/src/Tools/induct.ML	Tue Mar 17 14:12:06 2009 +0100
+++ b/src/Tools/induct.ML	Tue Mar 17 14:12:43 2009 +0100
@@ -111,19 +111,19 @@
 
 (* rules *)
 
-type rules = (string * thm) NetRules.T;
+type rules = (string * thm) Item_Net.T;
 
 val init_rules =
-  NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso
+  Item_Net.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso
     Thm.eq_thm_prop (th1, th2));
 
 fun filter_rules (rs: rules) th =
-  filter (fn (_, th') => Thm.eq_thm_prop (th, th')) (NetRules.rules rs);
+  filter (fn (_, th') => Thm.eq_thm_prop (th, th')) (Item_Net.content rs);
 
-fun lookup_rule (rs: rules) = AList.lookup (op =) (NetRules.rules rs);
+fun lookup_rule (rs: rules) = AList.lookup (op =) (Item_Net.content rs);
 
 fun pretty_rules ctxt kind rs =
-  let val thms = map snd (NetRules.rules rs)
+  let val thms = map snd (Item_Net.content rs)
   in Pretty.big_list kind (map (ProofContext.pretty_thm ctxt) thms) end;
 
 
@@ -139,21 +139,21 @@
   val extend = I;
   fun merge _ (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1)),
       ((casesT2, casesP2), (inductT2, inductP2), (coinductT2, coinductP2))) =
-    ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesP1, casesP2)),
-      (NetRules.merge (inductT1, inductT2), NetRules.merge (inductP1, inductP2)),
-      (NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductP1, coinductP2)));
+    ((Item_Net.merge (casesT1, casesT2), Item_Net.merge (casesP1, casesP2)),
+      (Item_Net.merge (inductT1, inductT2), Item_Net.merge (inductP1, inductP2)),
+      (Item_Net.merge (coinductT1, coinductT2), Item_Net.merge (coinductP1, coinductP2)));
 );
 
 val get_local = InductData.get o Context.Proof;
 
 fun dest_rules ctxt =
   let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP)) = get_local ctxt in
-    {type_cases = NetRules.rules casesT,
-     pred_cases = NetRules.rules casesP,
-     type_induct = NetRules.rules inductT,
-     pred_induct = NetRules.rules inductP,
-     type_coinduct = NetRules.rules coinductT,
-     pred_coinduct = NetRules.rules coinductP}
+    {type_cases = Item_Net.content casesT,
+     pred_cases = Item_Net.content casesP,
+     type_induct = Item_Net.content inductT,
+     pred_induct = Item_Net.content inductP,
+     type_coinduct = Item_Net.content coinductT,
+     pred_coinduct = Item_Net.content coinductP}
   end;
 
 fun print_rules ctxt =
@@ -184,7 +184,7 @@
 
 
 fun find_rules which how ctxt x =
-  map snd (NetRules.retrieve (which (get_local ctxt)) (how x));
+  map snd (Item_Net.retrieve (which (get_local ctxt)) (how x));
 
 val find_casesT = find_rules (#1 o #1) encode_type;
 val find_casesP = find_rules (#2 o #1) I;
@@ -203,18 +203,18 @@
   let val (x, thm) = g arg in (InductData.map (f (name, thm)) x, thm) end;
 
 fun del_att which = Thm.declaration_attribute (fn th => InductData.map (which (pairself (fn rs =>
-  fold NetRules.delete (filter_rules rs th) rs))));
+  fold Item_Net.delete (filter_rules rs th) rs))));
 
 fun map1 f (x, y, z) = (f x, y, z);
 fun map2 f (x, y, z) = (x, f y, z);
 fun map3 f (x, y, z) = (x, y, f z);
 
-fun add_casesT rule x = map1 (apfst (NetRules.insert rule)) x;
-fun add_casesP rule x = map1 (apsnd (NetRules.insert rule)) x;
-fun add_inductT rule x = map2 (apfst (NetRules.insert rule)) x;
-fun add_inductP rule x = map2 (apsnd (NetRules.insert rule)) x;
-fun add_coinductT rule x = map3 (apfst (NetRules.insert rule)) x;
-fun add_coinductP rule x = map3 (apsnd (NetRules.insert rule)) x;
+fun add_casesT rule x = map1 (apfst (Item_Net.insert rule)) x;
+fun add_casesP rule x = map1 (apsnd (Item_Net.insert rule)) x;
+fun add_inductT rule x = map2 (apfst (Item_Net.insert rule)) x;
+fun add_inductP rule x = map2 (apsnd (Item_Net.insert rule)) x;
+fun add_coinductT rule x = map3 (apfst (Item_Net.insert rule)) x;
+fun add_coinductP rule x = map3 (apsnd (Item_Net.insert rule)) x;
 
 val consumes0 = RuleCases.consumes_default 0;
 val consumes1 = RuleCases.consumes_default 1;