--- a/src/HOL/Analysis/measurable.ML Mon Aug 16 13:00:55 2021 +0200
+++ b/src/HOL/Analysis/measurable.ML Mon Aug 16 23:07:01 2021 +0200
@@ -53,8 +53,8 @@
preprocessors : (string * preprocessor) list }
val empty: T = {
measurable_thms = Item_Net.init eq_measurable_thms (single o Thm.prop_of o fst),
- dest_thms = Thm.full_rules,
- cong_thms = Thm.full_rules,
+ dest_thms = Thm.item_net,
+ cong_thms = Thm.item_net,
preprocessors = [] };
val extend = I;
fun merge ({measurable_thms = t1, dest_thms = dt1, cong_thms = ct1, preprocessors = i1 },
--- a/src/HOL/Eisbach/match_method.ML Mon Aug 16 13:00:55 2021 +0200
+++ b/src/HOL/Eisbach/match_method.ML Mon Aug 16 23:07:01 2021 +0200
@@ -48,7 +48,7 @@
Scan.lift (\<^keyword>\<open>premises\<close> |-- Args.mode "local") >> Match_Prems ||
Scan.lift (\<^keyword>\<open>(\<close>) |-- Args.term --| Scan.lift (\<^keyword>\<open>)\<close>) >>
(fn t => Match_Term (Item_Net.update t aconv_net)) ||
- Attrib.thms >> (fn thms => Match_Fact (fold Item_Net.update thms Thm.full_rules));
+ Attrib.thms >> (fn thms => Match_Fact (fold Item_Net.update thms Thm.item_net));
fun nameable_match m = (case m of Match_Fact _ => true | Match_Prems _ => true | _ => false);
--- a/src/HOL/Tools/Lifting/lifting_info.ML Mon Aug 16 13:00:55 2021 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Mon Aug 16 23:07:01 2021 +0200
@@ -87,7 +87,7 @@
val empty =
{ quot_maps = Symtab.empty,
quotients = Symtab.empty,
- reflexivity_rules = Thm.full_rules,
+ reflexivity_rules = Thm.item_net,
relator_distr_data = Symtab.empty,
restore_data = Symtab.empty,
no_code_types = Symtab.empty
@@ -277,7 +277,7 @@
Data.map (map_restore_data (Symtab.update (bundle_name, restore_data))) context
fun init_restore_data bundle_name qinfo context =
- update_restore_data bundle_name { quotient = qinfo, transfer_rules = Thm.full_rules } context
+ update_restore_data bundle_name { quotient = qinfo, transfer_rules = Thm.item_net } context
fun add_transfer_rules_in_restore_data bundle_name transfer_rules context =
(case Symtab.lookup (get_restore_data' context) bundle_name of
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Mon Aug 16 13:00:55 2021 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Mon Aug 16 23:07:01 2021 +0200
@@ -1026,7 +1026,7 @@
val transfer_rules = filter_transfer_rules_by_rel transfer_rel (Transfer.get_transfer_raw lthy)
in
fn phi => fold_rev
- (Item_Net.update o Morphism.thm phi) transfer_rules Thm.full_rules
+ (Item_Net.update o Morphism.thm phi) transfer_rules Thm.item_net
end
in
case Lifting_Info.lookup_restore_data lthy pointer of
--- a/src/HOL/Tools/Transfer/transfer.ML Mon Aug 16 13:00:55 2021 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML Mon Aug 16 23:07:01 2021 +0200
@@ -94,13 +94,13 @@
relator_domain : thm Item_Net.T,
pred_data : pred_data Symtab.table }
val empty =
- { transfer_raw = Thm.intro_rules,
+ { transfer_raw = Thm.item_net_intro,
known_frees = [],
compound_lhs = compound_xhs_empty_net,
compound_rhs = compound_xhs_empty_net,
relator_eq = rewr_rules,
- relator_eq_raw = Thm.full_rules,
- relator_domain = Thm.full_rules,
+ relator_eq_raw = Thm.item_net,
+ relator_domain = Thm.item_net,
pred_data = Symtab.empty }
val extend = I
fun merge
--- a/src/Pure/Isar/calculation.ML Mon Aug 16 13:00:55 2021 +0200
+++ b/src/Pure/Isar/calculation.ML Mon Aug 16 23:07:01 2021 +0200
@@ -32,23 +32,22 @@
structure Data = Generic_Data
(
- type T = (thm Item_Net.T * thm list) * calculation option;
- val empty = ((Thm.elim_rules, []), NONE);
+ type T = (thm Item_Net.T * thm Item_Net.T) * calculation option;
+ val empty = ((Thm.item_net_elim, Thm.item_net), NONE);
val extend = I;
fun merge (((trans1, sym1), _), ((trans2, sym2), _)) =
- ((Item_Net.merge (trans1, trans2), Thm.merge_thms (sym1, sym2)), NONE);
+ ((Item_Net.merge (trans1, trans2), Item_Net.merge (sym1, sym2)), NONE);
);
val get_rules = #1 o Data.get o Context.Proof;
+val get_trans_rules = Item_Net.content o #1 o get_rules;
+val get_sym_rules = Item_Net.content o #2 o get_rules;
val get_calculation = #2 o Data.get o Context.Proof;
fun print_rules ctxt =
- let
- val pretty_thm = Thm.pretty_thm_item ctxt;
- val (trans, sym) = get_rules ctxt;
- in
- [Pretty.big_list "transitivity rules:" (map pretty_thm (Item_Net.content trans)),
- Pretty.big_list "symmetry rules:" (map pretty_thm sym)]
+ let val pretty_thm = Thm.pretty_thm_item ctxt in
+ [Pretty.big_list "transitivity rules:" (map pretty_thm (get_trans_rules ctxt)),
+ Pretty.big_list "symmetry rules:" (map pretty_thm (get_sym_rules ctxt))]
end |> Pretty.writeln_chunks;
@@ -106,12 +105,12 @@
val sym_add =
Thm.declaration_attribute (fn th =>
- (Data.map o apfst o apsnd) (Thm.add_thm (Thm.trim_context th)) #>
+ (Data.map o apfst o apsnd) (Item_Net.update (Thm.trim_context th)) #>
Thm.attribute_declaration (Context_Rules.elim_query NONE) th);
val sym_del =
Thm.declaration_attribute (fn th =>
- (Data.map o apfst o apsnd) (Thm.del_thm th) #>
+ (Data.map o apfst o apsnd) (Item_Net.remove th) #>
Thm.attribute_declaration Context_Rules.rule_del th);
@@ -119,11 +118,12 @@
val symmetric =
Thm.rule_attribute [] (fn context => fn th =>
- (case Seq.chop 2
- (Drule.multi_resolves (SOME (Context.proof_of context)) [th] (#2 (#1 (Data.get context)))) of
- ([th'], _) => Drule.zero_var_indexes th'
- | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
- | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
+ let val ctxt = Context.proof_of context in
+ (case Seq.chop 2 (Drule.multi_resolves (SOME ctxt) [th] (get_sym_rules ctxt)) of
+ ([th'], _) => Drule.zero_var_indexes th'
+ | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
+ | _ => raise THM ("symmetric: multiple unifiers", 1, [th]))
+ end);
(* concrete syntax *)
--- a/src/Pure/Isar/class.ML Mon Aug 16 13:00:55 2021 +0200
+++ b/src/Pure/Isar/class.ML Mon Aug 16 23:07:01 2021 +0200
@@ -76,7 +76,7 @@
axiom: thm option,
(* dynamic part *)
- defs: thm list,
+ defs: thm Item_Net.T,
operations: (string * (class * ((typ * term) * bool))) list
(* n.b.
@@ -102,7 +102,7 @@
Class_Data {consts = _, base_sort = _, base_morph = _, export_morph = _, assm_intro = _,
of_class = _, axiom = _, defs = defs2, operations = operations2}) =
make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom),
- (Thm.merge_thms (defs1, defs2),
+ (Item_Net.merge (defs1, defs2),
AList.merge (op =) (K true) (operations1, operations2)));
structure Class_Data = Theory_Data
@@ -153,7 +153,7 @@
Graph.fold (fn (_, (Class_Data {assm_intro, ...}, _)) => fold (insert Thm.eq_thm)
(the_list assm_intro)) (Class_Data.get thy) [];
-fun these_defs thy = maps (#defs o the_class_data thy) o ancestry thy;
+fun these_defs thy = maps (Item_Net.content o #defs o the_class_data thy) o ancestry thy;
fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy;
val base_morphism = #base_morph oo the_class_data;
@@ -226,7 +226,8 @@
val add_class = Graph.new_node (class,
make_class_data (((map o apply2) fst params, base_sort,
base_morph, export_morph, Option.map Thm.trim_context some_assm_intro,
- Thm.trim_context of_class, Option.map Thm.trim_context some_axiom), ([], operations)))
+ Thm.trim_context of_class, Option.map Thm.trim_context some_axiom),
+ (Thm.item_net, operations)))
#> fold (curry Graph.add_edge class) sups;
in Class_Data.map add_class thy end;
@@ -261,7 +262,7 @@
in
thy
|> (Class_Data.map o Graph.map_node class o map_class_data o apsnd o apfst)
- (cons sym_thm)
+ (Item_Net.update sym_thm)
|> activate_defs class [sym_thm]
end;
--- a/src/Pure/Isar/locale.ML Mon Aug 16 13:00:55 2021 +0200
+++ b/src/Pure/Isar/locale.ML Mon Aug 16 23:07:01 2021 +0200
@@ -668,33 +668,33 @@
structure Thms = Generic_Data
(
- type T = thm list * thm list * thm list;
- val empty = ([], [], []);
+ type T = thm Item_Net.T * thm Item_Net.T * thm Item_Net.T;
+ val empty = (Thm.item_net, Thm.item_net, Thm.item_net);
val extend = I;
fun merge ((witnesses1, intros1, unfolds1), (witnesses2, intros2, unfolds2)) =
- (Thm.merge_thms (witnesses1, witnesses2),
- Thm.merge_thms (intros1, intros2),
- Thm.merge_thms (unfolds1, unfolds2));
+ (Item_Net.merge (witnesses1, witnesses2),
+ Item_Net.merge (intros1, intros2),
+ Item_Net.merge (unfolds1, unfolds2));
);
fun get_thms which ctxt =
map (Thm.transfer' ctxt) (which (Thms.get (Context.Proof ctxt)));
-val get_witnesses = get_thms #1;
-val get_intros = get_thms #2;
-val get_unfolds = get_thms #3;
+val get_witnesses = get_thms (Item_Net.content o #1);
+val get_intros = get_thms (Item_Net.content o #2);
+val get_unfolds = get_thms (Item_Net.content o #3);
val witness_add =
Thm.declaration_attribute (fn th =>
- Thms.map (fn (x, y, z) => (Thm.add_thm (Thm.trim_context th) x, y, z)));
+ Thms.map (fn (x, y, z) => (Item_Net.update (Thm.trim_context th) x, y, z)));
val intro_add =
Thm.declaration_attribute (fn th =>
- Thms.map (fn (x, y, z) => (x, Thm.add_thm (Thm.trim_context th) y, z)));
+ Thms.map (fn (x, y, z) => (x, Item_Net.update (Thm.trim_context th) y, z)));
val unfold_add =
Thm.declaration_attribute (fn th =>
- Thms.map (fn (x, y, z) => (x, y, Thm.add_thm (Thm.trim_context th) z)));
+ Thms.map (fn (x, y, z) => (x, y, Item_Net.update (Thm.trim_context th) z)));
(* Tactics *)
--- a/src/Pure/Tools/named_theorems.ML Mon Aug 16 13:00:55 2021 +0200
+++ b/src/Pure/Tools/named_theorems.ML Mon Aug 16 23:07:01 2021 +0200
@@ -34,7 +34,7 @@
Data.map (fn data =>
if Symtab.defined data name
then error ("Duplicate declaration of named theorems: " ^ quote name)
- else Symtab.update (name, Thm.full_rules) data);
+ else Symtab.update (name, Thm.item_net) data);
fun undeclared name = "Undeclared named theorems " ^ quote name;
@@ -58,7 +58,7 @@
val get = content o Context.Proof;
-fun clear name = map_entry name (K Thm.full_rules);
+fun clear name = map_entry name (K Thm.item_net);
fun add_thm name th = map_entry name (Item_Net.update (Thm.trim_context th));
fun del_thm name = map_entry name o Item_Net.remove;
--- a/src/Pure/Tools/named_thms.ML Mon Aug 16 13:00:55 2021 +0200
+++ b/src/Pure/Tools/named_thms.ML Mon Aug 16 23:07:01 2021 +0200
@@ -21,7 +21,7 @@
structure Data = Generic_Data
(
type T = thm Item_Net.T;
- val empty = Thm.full_rules;
+ val empty = Thm.item_net;
val extend = I;
val merge = Item_Net.merge;
);
--- a/src/Pure/more_thm.ML Mon Aug 16 13:00:55 2021 +0200
+++ b/src/Pure/more_thm.ML Mon Aug 16 23:07:01 2021 +0200
@@ -56,9 +56,9 @@
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 full_rules: thm Item_Net.T
- val intro_rules: thm Item_Net.T
- val elim_rules: thm Item_Net.T
+ val item_net: thm Item_Net.T
+ val item_net_intro: thm Item_Net.T
+ val item_net_elim: thm Item_Net.T
val declare_hyps: cterm -> Proof.context -> Proof.context
val assume_hyps: cterm -> Proof.context -> thm * Proof.context
val unchecked_hyps: Proof.context -> Proof.context
@@ -265,9 +265,9 @@
val del_thm = remove eq_thm_prop;
val merge_thms = merge eq_thm_prop;
-val full_rules = Item_Net.init eq_thm_prop (single o Thm.full_prop_of);
-val intro_rules = Item_Net.init eq_thm_prop (single o Thm.concl_of);
-val elim_rules = Item_Net.init eq_thm_prop (single o Thm.major_prem_of);
+val item_net = Item_Net.init eq_thm_prop (single o Thm.full_prop_of);
+val item_net_intro = Item_Net.init eq_thm_prop (single o Thm.concl_of);
+val item_net_elim = Item_Net.init eq_thm_prop (single o Thm.major_prem_of);