tuned signature (again): anticipate different kinds of procs;

--- a/src/Pure/raw_simplifier.ML	Wed Aug 14 13:10:39 2024 +0200
+++ b/src/Pure/raw_simplifier.ML	Wed Aug 14 13:51:36 2024 +0200
@@ -246,8 +246,8 @@
     congs: association list of congruence rules and
            a list of `weak' congruence constants.
            A congruence is `weak' if it avoids normalization of some argument.
-    simprocs: discrimination net of simplification procedures
-      (functions that prove rewrite rules on the fly);
+    procs: simplification procedures indexed via discrimination net
+      simprocs: functions that prove rewrite rules on the fly;
     mk_rews:
       mk: turn simplification thms into rewrite rules;
       mk_cong: prepare congruence rules;
@@ -261,7 +261,7 @@
     prems: thm list,
     depth: int * bool Unsynchronized.ref} *
    {congs: thm Congtab.table * cong_name list,
-    simprocs: term procedure Net.net,
+    procs: term procedure Net.net,
     mk_rews:
      {mk: Proof.context -> thm -> thm list,
       mk_cong: Proof.context -> thm -> thm,
@@ -279,21 +279,24 @@
 
 fun map_ss1 f {rules, prems, depth} = make_ss1 (f (rules, prems, depth));
 
-fun make_ss2 (congs, simprocs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =
-  {congs = congs, simprocs = simprocs, mk_rews = mk_rews, term_ord = term_ord,
+fun make_ss2 (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =
+  {congs = congs, procs = procs, mk_rews = mk_rews, term_ord = term_ord,
     subgoal_tac = subgoal_tac, loop_tacs = loop_tacs, solvers = solvers};
 
-fun map_ss2 f {congs, simprocs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers} =
-  make_ss2 (f (congs, simprocs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers));
+fun map_ss2 f {congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers} =
+  make_ss2 (f (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers));
 
 fun make_simpset (args1, args2) = Simpset (make_ss1 args1, make_ss2 args2);
 
-fun dest_ss (Simpset ({rules, ...}, {congs, simprocs, loop_tacs, solvers, ...})) =
+fun dest_procs procs =
+  Net.entries procs
+  |> partition_eq eq_procedure_id
+  |> map (fn ps as Procedure {name, ...} :: _ => (name, map (fn Procedure {lhs, ...} => lhs) ps));
+
+fun dest_ss (Simpset ({rules, ...}, {congs, procs = simprocs, loop_tacs, solvers, ...})) =
  {simps = Net.entries rules
     |> map (fn {name, thm, ...} => (name, thm)),
-  simprocs = Net.entries simprocs
-    |> partition_eq eq_procedure_id
-    |> map (fn ps as Procedure {name, ...} :: _ => (name, map (fn Procedure {lhs, ...} => lhs) ps)),
+  simprocs = dest_procs simprocs,
   congs = congs |> fst |> Congtab.dest,
   weak_congs = congs |> snd,
   loopers = map fst loop_tacs,
@@ -328,10 +331,10 @@
   else
     let
       val Simpset ({rules = rules1, prems = prems1, depth = depth1},
-       {congs = (congs1, weak1), simprocs = simprocs1, mk_rews, term_ord, subgoal_tac,
+       {congs = (congs1, weak1), procs = simprocs1, mk_rews, term_ord, subgoal_tac,
         loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1;
       val Simpset ({rules = rules2, prems = prems2, depth = depth2},
-       {congs = (congs2, weak2), simprocs = simprocs2, mk_rews = _, term_ord = _, subgoal_tac = _,
+       {congs = (congs2, weak2), procs = simprocs2, mk_rews = _, term_ord = _, subgoal_tac = _,
         loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2;
 
       val rules' = Net.merge eq_rrule (rules1, rules2);
@@ -686,7 +689,7 @@
 in
 
 fun add_eqcong thm ctxt = ctxt |> map_simpset2
-  (fn (congs, simprocs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
+  (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
     let
       val (lhs, _) = Logic.dest_equals (Thm.concl_of thm)
         handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", [thm]);
@@ -696,10 +699,10 @@
       val (xs, weak) = congs;
       val xs' = Congtab.update (a, Thm.trim_context thm) xs;
       val weak' = if is_full_cong thm then weak else a :: weak;
-    in ((xs', weak'), simprocs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) end);
+    in ((xs', weak'), procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) end);
 
 fun del_eqcong thm ctxt = ctxt |> map_simpset2
-  (fn (congs, simprocs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
+  (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
     let
       val (lhs, _) = Logic.dest_equals (Thm.concl_of thm)
         handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", [thm]);
@@ -709,7 +712,7 @@
       val (xs, _) = congs;
       val xs' = Congtab.delete_safe a xs;
       val weak' = Congtab.fold (fn (a, th) => if is_full_cong th then I else insert (op =) a) xs' [];
-    in ((xs', weak'), simprocs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) end);
+    in ((xs', weak'), procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) end);
 
 fun add_cong thm ctxt = add_eqcong (mk_cong ctxt thm) ctxt;
 fun del_cong thm ctxt = del_eqcong (mk_cong ctxt thm) ctxt;
@@ -748,8 +751,8 @@
  (cond_tracing ctxt (fn () =>
     print_term ctxt ("Adding simplification procedure " ^ quote name ^ " for") lhs);
   ctxt |> map_simpset2
-    (fn (congs, simprocs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
-      (congs, Net.insert_term eq_procedure_id (lhs, proc) simprocs,
+    (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
+      (congs, Net.insert_term eq_procedure_id (lhs, proc) procs,
         mk_rews, term_ord, subgoal_tac, loop_tacs, solvers))
   handle Net.INSERT =>
     (cond_warning ctxt (fn () => "Ignoring duplicate simplification procedure " ^ quote name);
@@ -757,8 +760,8 @@
 
 fun del_proc1 (proc as Procedure {name, lhs, ...}) ctxt =
   ctxt |> map_simpset2
-    (fn (congs, simprocs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
-      (congs, Net.delete_term eq_procedure_id (lhs, proc) simprocs,
+    (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
+      (congs, Net.delete_term eq_procedure_id (lhs, proc) procs,
         mk_rews, term_ord, subgoal_tac, loop_tacs, solvers))
   handle Net.DELETE =>
     (cond_warning ctxt (fn () => "Simplification procedure " ^ quote name ^ " not in simpset");
@@ -783,14 +786,14 @@
 local
 
 fun map_mk_rews f =
-  map_simpset2 (fn (congs, simprocs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
+  map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
     let
       val {mk, mk_cong, mk_sym, mk_eq_True, reorient} = mk_rews;
       val (mk', mk_cong', mk_sym', mk_eq_True', reorient') =
         f (mk, mk_cong, mk_sym, mk_eq_True, reorient);
       val mk_rews' = {mk = mk', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True',
         reorient = reorient'};
-    in (congs, simprocs, mk_rews', term_ord, subgoal_tac, loop_tacs, solvers) end);
+    in (congs, procs, mk_rews', term_ord, subgoal_tac, loop_tacs, solvers) end);
 
 in
 
@@ -819,50 +822,50 @@
 (* term_ord *)
 
 fun set_term_ord term_ord =
-  map_simpset2 (fn (congs, simprocs, mk_rews, _, subgoal_tac, loop_tacs, solvers) =>
-   (congs, simprocs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers));
+  map_simpset2 (fn (congs, procs, mk_rews, _, subgoal_tac, loop_tacs, solvers) =>
+   (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers));
 
 
 (* tactics *)
 
 fun set_subgoaler subgoal_tac =
-  map_simpset2 (fn (congs, simprocs, mk_rews, term_ord, _, loop_tacs, solvers) =>
-   (congs, simprocs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers));
+  map_simpset2 (fn (congs, procs, mk_rews, term_ord, _, loop_tacs, solvers) =>
+   (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers));
 
 fun ctxt setloop tac = ctxt |>
-  map_simpset2 (fn (congs, simprocs, mk_rews, term_ord, subgoal_tac, _, solvers) =>
-   (congs, simprocs, mk_rews, term_ord, subgoal_tac, [("", tac)], solvers));
+  map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, _, solvers) =>
+   (congs, procs, mk_rews, term_ord, subgoal_tac, [("", tac)], solvers));
 
 fun ctxt addloop (name, tac) = ctxt |>
-  map_simpset2 (fn (congs, simprocs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
-    (congs, simprocs, mk_rews, term_ord, subgoal_tac,
+  map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
+    (congs, procs, mk_rews, term_ord, subgoal_tac,
      AList.update (op =) (name, tac) loop_tacs, solvers));
 
 fun ctxt delloop name = ctxt |>
-  map_simpset2 (fn (congs, simprocs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
-    (congs, simprocs, mk_rews, term_ord, subgoal_tac,
+  map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
+    (congs, procs, mk_rews, term_ord, subgoal_tac,
      (if AList.defined (op =) loop_tacs name then ()
       else cond_warning ctxt (fn () => "No such looper in simpset: " ^ quote name);
       AList.delete (op =) name loop_tacs), solvers));
 
 fun ctxt setSSolver solver = ctxt |> map_simpset2
-  (fn (congs, simprocs, mk_rews, term_ord, subgoal_tac, loop_tacs, (unsafe_solvers, _)) =>
-    (congs, simprocs, mk_rews, term_ord, subgoal_tac, loop_tacs, (unsafe_solvers, [solver])));
+  (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, (unsafe_solvers, _)) =>
+    (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, (unsafe_solvers, [solver])));
 
-fun ctxt addSSolver solver = ctxt |> map_simpset2 (fn (congs, simprocs, mk_rews, term_ord,
-  subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, simprocs, mk_rews, term_ord,
+fun ctxt addSSolver solver = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, term_ord,
+  subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, term_ord,
     subgoal_tac, loop_tacs, (unsafe_solvers, insert eq_solver solver solvers)));
 
-fun ctxt setSolver solver = ctxt |> map_simpset2 (fn (congs, simprocs, mk_rews, term_ord,
-  subgoal_tac, loop_tacs, (_, solvers)) => (congs, simprocs, mk_rews, term_ord,
+fun ctxt setSolver solver = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, term_ord,
+  subgoal_tac, loop_tacs, (_, solvers)) => (congs, procs, mk_rews, term_ord,
     subgoal_tac, loop_tacs, ([solver], solvers)));
 
-fun ctxt addSolver solver = ctxt |> map_simpset2 (fn (congs, simprocs, mk_rews, term_ord,
-  subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, simprocs, mk_rews, term_ord,
+fun ctxt addSolver solver = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, term_ord,
+  subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, term_ord,
     subgoal_tac, loop_tacs, (insert eq_solver solver unsafe_solvers, solvers)));
 
-fun set_solvers solvers = map_simpset2 (fn (congs, simprocs, mk_rews, term_ord,
-  subgoal_tac, loop_tacs, _) => (congs, simprocs, mk_rews, term_ord,
+fun set_solvers solvers = map_simpset2 (fn (congs, procs, mk_rews, term_ord,
+  subgoal_tac, loop_tacs, _) => (congs, procs, mk_rews, term_ord,
   subgoal_tac, loop_tacs, (solvers, solvers)));
 
 
@@ -982,7 +985,7 @@
 
 fun rewritec (prover, maxt) ctxt t =
   let
-    val Simpset ({rules, ...}, {congs, simprocs, term_ord, ...}) = simpset_of ctxt;
+    val Simpset ({rules, ...}, {congs, procs = simprocs, term_ord, ...}) = simpset_of ctxt;
     val eta_thm = Thm.eta_conversion t;
     val eta_t' = Thm.rhs_of eta_thm;
     val eta_t = Thm.term_of eta_t';