# HG changeset patch
# User wenzelm
# Date 1752227563 -7200
# Node ID 60ec2b2dc55a58dcd1cfed70c22361659531784c
# Parent  ca600cbfd4bfc8def14fb03ca953253e7d90d768
clarified signature: rule declarations work via "info" as internal rule (which coincides with external rule);

diff -r ca600cbfd4bf -r 60ec2b2dc55a src/Pure/Isar/context_rules.ML
--- 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'));
diff -r ca600cbfd4bf -r 60ec2b2dc55a src/Pure/bires.ML
--- 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) =