src/Pure/Isar/context_rules.ML

--- a/src/Pure/Isar/context_rules.ML	Sun Jul 06 13:58:41 2025 +0200
+++ b/src/Pure/Isar/context_rules.ML	Sun Jul 06 14:53:20 2025 +0200
@@ -37,35 +37,11 @@
 
 (** rule declaration contexts **)
 
-(* rule kinds *)
-
-val intro_bangK = (0, false);
-val elim_bangK = (0, true);
-val introK = (1, false);
-val elimK = (1, true);
-val intro_queryK = (2, false);
-val elim_queryK = (2, true);
-
-val kind_names =
- [(intro_bangK, "safe introduction rules (intro!)"),
-  (elim_bangK, "safe elimination rules (elim!)"),
-  (introK, "introduction rules (intro)"),
-  (elimK, "elimination rules (elim)"),
-  (intro_queryK, "extra introduction rules (intro?)"),
-  (elim_queryK, "extra elimination rules (elim?)")];
-
-val rule_kinds = map #1 kind_names;
-val rule_indexes = distinct (op =) (map #1 rule_kinds);
-
-
 (* context data *)
 
-val empty_netpairs: Bires.netpair list =
-  replicate (length rule_indexes) Bires.empty_netpair;
-
 datatype rules = Rules of
  {next: int,
-  rules: (int * ((int * bool) * thm)) list,
+  rules: (int * (Bires.kind * thm)) list,
   netpairs: Bires.netpair list,
   wrappers:
     ((Proof.context -> (int -> tactic) -> int -> tactic) * stamp) list *
@@ -74,23 +50,25 @@
 fun make_rules next rules netpairs wrappers =
   Rules {next = next, rules = rules, netpairs = netpairs, wrappers = wrappers};
 
-fun add_rule (i, b) opt_weight th (Rules {next, rules, netpairs, wrappers}) =
+fun add_rule kind opt_weight th (Rules {next, rules, netpairs, wrappers}) =
   let
-    val weight = opt_weight |> \<^if_none>\<open>Bires.subgoals_of (b, th)\<close>;
+    val weight = opt_weight |> \<^if_none>\<open>Bires.subgoals_of (Bires.kind_rule kind th)\<close>;
     val tag = {weight = weight, index = next};
     val th' = Thm.trim_context th;
-  in
-    make_rules (next - 1) ((weight, ((i, b), th')) :: rules)
-      (nth_map i (Bires.insert_tagged_rule (tag, (b, th'))) netpairs) wrappers
-  end;
+    val rules' = (weight, (kind, th')) :: rules;
+    val netpairs' = netpairs
+      |> Bires.kind_map kind (Bires.insert_tagged_rule (tag, Bires.kind_rule kind th'));
+  in make_rules (next - 1) rules' netpairs' wrappers end;
 
 fun del_rule0 th (rs as Rules {next, rules, netpairs, wrappers}) =
   let
     fun eq_th (_, (_, th')) = Thm.eq_thm_prop (th, th');
     fun del b netpair = Bires.delete_tagged_rule (b, th) netpair handle Net.DELETE => netpair;
+    val rules' = filter_out eq_th rules;
+    val netpairs' = map (del false o del true) netpairs;
   in
     if not (exists eq_th rules) then rs
-    else make_rules next (filter_out eq_th rules) (map (del false o del true) netpairs) wrappers
+    else make_rules next rules' netpairs' wrappers
   end;
 
 fun del_rule th = del_rule0 th o del_rule0 (Tactic.make_elim th);
@@ -98,7 +76,7 @@
 structure Data = Generic_Data
 (
   type T = rules;
-  val empty = make_rules ~1 [] empty_netpairs ([], []);
+  val empty = make_rules ~1 [] Bires.kind_netpairs ([], []);
   fun merge
     (Rules {rules = rules1, wrappers = (ws1, ws1'), ...},
       Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) =
@@ -108,21 +86,23 @@
       val rules = Library.merge (fn ((_, (k1, th1)), (_, (k2, th2))) =>
           k1 = k2 andalso Thm.eq_thm_prop (th1, th2)) (rules1, rules2);
       val next = ~ (length rules);
-      val netpairs = fold (fn (index, (weight, ((i, b), th))) =>
-          nth_map i (Bires.insert_tagged_rule ({weight = weight, index = index}, (b, th))))
-        (next upto ~1 ~~ rules) empty_netpairs;
+      val netpairs =
+        fold (fn (index, (weight, (kind, th))) =>
+          Bires.kind_map kind
+            (Bires.insert_tagged_rule ({weight = weight, index = index}, (Bires.kind_elim kind, th))))
+        (next upto ~1 ~~ rules) Bires.kind_netpairs;
     in make_rules (next - 1) rules netpairs wrappers end;
 );
 
 fun print_rules ctxt =
   let
     val Rules {rules, ...} = Data.get (Context.Proof ctxt);
-    fun prt_kind (i, b) =
-      Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
-        (map_filter (fn (_, (k, th)) =>
-            if k = (i, b) then SOME (Thm.pretty_thm_item ctxt th) else NONE)
+    fun prt_kind kind =
+      Pretty.big_list (Bires.kind_title kind ^ ":")
+        (map_filter (fn (_, (kind', th)) =>
+            if kind = kind' then SOME (Thm.pretty_thm_item ctxt th) else NONE)
           (sort (int_ord o apply2 fst) rules));
-  in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
+  in Pretty.writeln (Pretty.chunks (map prt_kind Bires.kind_domain)) end;
 
 
 (* access data *)
@@ -188,15 +168,15 @@
 fun rule_add k view opt_w =
   Thm.declaration_attribute (fn th => Data.map (add_rule k opt_w (view th) o del_rule th));
 
-val intro_bang  = rule_add intro_bangK I;
-val elim_bang   = rule_add elim_bangK I;
-val dest_bang   = rule_add elim_bangK Tactic.make_elim;
-val intro       = rule_add introK I;
-val elim        = rule_add elimK I;
-val dest        = rule_add elimK Tactic.make_elim;
-val intro_query = rule_add intro_queryK I;
-val elim_query  = rule_add elim_queryK I;
-val dest_query  = rule_add elim_queryK Tactic.make_elim;
+val intro_bang  = rule_add Bires.intro_bang_kind I;
+val elim_bang   = rule_add Bires.elim_bang_kind I;
+val dest_bang   = rule_add Bires.elim_bang_kind Tactic.make_elim;
+val intro       = rule_add Bires.intro_kind I;
+val elim        = rule_add Bires.elim_kind I;
+val dest        = rule_add Bires.elim_kind Tactic.make_elim;
+val intro_query = rule_add Bires.intro_query_kind I;
+val elim_query  = rule_add Bires.elim_query_kind I;
+val dest_query  = rule_add Bires.elim_query_kind Tactic.make_elim;
 
 val _ = Theory.setup
   (snd o Global_Theory.add_thms [((Binding.empty, Drule.equal_intr_rule), [intro_query NONE])]);