--- 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
--- 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);
--- 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 **)
--- 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;