clarified signature: rule declarations work via "info" as internal rule (which coincides with external rule);
--- a/src/Pure/Isar/context_rules.ML Thu Jul 10 17:29:25 2025 +0200
+++ b/src/Pure/Isar/context_rules.ML Fri Jul 11 11:52:43 2025 +0200
@@ -37,10 +37,26 @@
(** rule declaration contexts **)
+(* rule declarations *)
+
+type decl = thm Bires.decl;
+type decls = thm Bires.decls;
+
+fun init_decl kind opt_weight th : decl =
+ let val weight = opt_weight |> \<^if_none>\<open>Bires.subgoals_of (Bires.kind_rule kind th)\<close>;
+ in {kind = kind, tag = Bires.weight_tag weight, info = th} end;
+
+fun insert_decl ({kind, tag, info = th}: decl) =
+ Bires.insert_tagged_rule (tag, Bires.kind_rule kind th);
+
+fun remove_decl ({info = th, ...}: decl) =
+ Bires.delete_tagged_rule (false, th) o Bires.delete_tagged_rule (true, th);
+
+
(* context data *)
datatype rules = Rules of
- {decls: unit Bires.decls,
+ {decls: decls,
netpairs: Bires.netpair list,
wrappers:
((Proof.context -> (int -> tactic) -> int -> tactic) * stamp) list *
@@ -51,21 +67,24 @@
fun add_rule kind opt_weight th (rules as Rules {decls, netpairs, wrappers}) =
let
- val weight = opt_weight |> \<^if_none>\<open>Bires.subgoals_of (Bires.kind_rule kind th)\<close>;
- val decl = {kind = kind, tag = Bires.weight_tag weight, info = ()};
+ val th' = Thm.trim_context th;
+ val decl' = init_decl kind opt_weight th';
in
- (case Bires.extend_decls (Thm.trim_context th, decl) decls of
- NONE => rules
- | SOME (new_rule, decls') =>
- let val netpairs' = netpairs |> Bires.kind_map kind (Bires.insert_rule new_rule)
+ (case Bires.extend_decls (th', decl') decls of
+ (NONE, _) => rules
+ | (SOME new_decl, decls') =>
+ let val netpairs' = Bires.kind_map kind (insert_decl new_decl) netpairs
in make_rules decls' netpairs' wrappers end)
end;
fun del_rule0 th (rules as Rules {decls, netpairs, wrappers}) =
(case Bires.remove_decls th decls of
- NONE => rules
- | SOME decls' =>
- let val netpairs' = map (Bires.remove_rule th) netpairs
+ ([], _) => rules
+ | (old_decls, decls') =>
+ let
+ val netpairs' =
+ fold (fn decl as {kind, ...} => Bires.kind_map kind (remove_decl decl))
+ old_decls netpairs;
in make_rules decls' netpairs' wrappers end);
fun del_rule th = del_rule0 th o del_rule0 (Tactic.make_elim th);
@@ -81,8 +100,8 @@
val (new_rules, decls) = Bires.merge_decls (decls1, decls2);
val netpairs =
netpairs1 |> map_index (uncurry (fn i =>
- new_rules |> fold (fn (th, decl) =>
- Bires.kind_index (#kind decl) = i ? Bires.insert_rule (th, decl))));
+ new_rules |> fold (fn decl =>
+ if Bires.kind_index (#kind decl) = i then insert_decl decl else I)))
val wrappers =
(Library.merge (eq_snd (op =)) (ws1, ws2),
Library.merge (eq_snd (op =)) (ws1', ws2'));
--- a/src/Pure/bires.ML Thu Jul 10 17:29:25 2025 +0200
+++ b/src/Pure/bires.ML Fri Jul 11 11:52:43 2025 +0200
@@ -39,11 +39,12 @@
val decl_ord: 'a decl ord
type 'a decls
val has_decls: 'a decls -> thm -> bool
+ val get_decls: 'a decls -> thm -> 'a decl list
val list_decls: (thm * 'a decl -> bool) -> 'a decls -> (thm * 'a decl) list
val pretty_decls: Proof.context -> kind list -> 'a decls -> Pretty.T list
- val merge_decls: 'a decls * 'a decls -> (thm * 'a decl) list * 'a decls
- val extend_decls: thm * 'a decl -> 'a decls -> ((thm * 'a decl) * 'a decls) option
- val remove_decls: thm -> 'a decls -> 'a decls option
+ val merge_decls: 'a decls * 'a decls -> 'a decl list * 'a decls
+ val extend_decls: thm * 'a decl -> 'a decls -> 'a decl option * 'a decls
+ val remove_decls: thm -> 'a decls -> 'a decl list * 'a decls
val empty_decls: 'a decls
type netpair = (tag * rule) Net.net * (tag * rule) Net.net
@@ -52,8 +53,6 @@
val insert_tagged_rules: (tag * rule) list -> netpair -> netpair
val delete_tagged_rule: rule -> netpair -> netpair
val delete_tagged_rules: rule list -> netpair -> netpair
- val insert_rule: thm * 'a decl -> netpair -> netpair
- val remove_rule: thm -> netpair -> netpair
val biresolution_from_nets_tac: Proof.context -> tag ord -> (rule -> bool) option ->
bool -> netpair -> int -> tactic
@@ -169,12 +168,14 @@
let
val decl' = next_decl next decl;
val decls' = Decls {next = next - 1, rules = Thmtab.cons_list (thm, decl') rules};
- in ((thm, decl'), decls') end;
+ in (decl', decls') end;
in
fun has_decls (Decls {rules, ...}) = Thmtab.defined rules;
+fun get_decls (Decls {rules, ...}) = Thmtab.lookup_list rules;
+
fun list_decls pred =
dest_decls pred #> sort (rev_order o decl_ord o apply2 #2);
@@ -189,13 +190,13 @@
decls1 |> fold_map add_decls (list_decls (not o dup_decls decls1) decls2);
fun extend_decls (thm, decl) decls =
- if dup_decls decls (thm, decl) then NONE
- else SOME (add_decls (thm, decl) decls);
+ if dup_decls decls (thm, decl) then (NONE, decls)
+ else add_decls (thm, decl) decls |>> SOME;
fun remove_decls thm (decls as Decls {next, rules}) =
- if has_decls decls thm
- then SOME (Decls {next = next, rules = Thmtab.delete thm rules})
- else NONE;
+ (case get_decls decls thm of
+ [] => ([], decls)
+ | old_decls => (old_decls, Decls {next = next, rules = Thmtab.delete thm rules}));
val empty_decls = Decls {next = ~1, rules = Thmtab.empty};
@@ -242,13 +243,6 @@
fun delete_tagged_rules rls = fold_rev delete_tagged_rule rls;
-fun insert_rule (thm, {kind, tag, ...}: 'a decl) netpair =
- insert_tagged_rule (tag, kind_rule kind thm) netpair;
-
-fun remove_rule thm =
- delete_tagged_rule (false, thm) o delete_tagged_rule (true, thm);
-
-
(*biresolution using a pair of nets rather than rules:
boolean "match" indicates matching or unification.*)
fun biresolution_from_nets_tac ctxt ord pred match ((inet, enet): netpair) =