# HG changeset patch
# User wenzelm
# Date 1723557665 -7200
# Node ID 34db40261287f3ebade43e530008dc81440de0a5
# Parent  2d2f476ab56e7267c2746876ac6d74a2b8f1d8b7
clarified signature;

diff -r 2d2f476ab56e -r 34db40261287 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Tue Aug 13 15:50:25 2024 +0200
+++ b/src/Pure/raw_simplifier.ML	Tue Aug 13 16:01:05 2024 +0200
@@ -27,7 +27,7 @@
   val merge_ss: simpset * simpset -> simpset
   val dest_ss: simpset ->
    {simps: (Thm_Name.T * thm) list,
-    procs: (string * term list) list,
+    simprocs: (string * term list) list,
     congs: (cong_name * thm) list,
     weak_congs: cong_name list,
     loopers: string list,
@@ -244,7 +244,7 @@
     congs: association list of congruence rules and
            a list of `weak' congruence constants.
            A congruence is `weak' if it avoids normalization of some argument.
-    procs: discrimination net of simplification procedures
+    simprocs: discrimination net of simplification procedures
       (functions that prove rewrite rules on the fly);
     mk_rews:
       mk: turn simplification thms into rewrite rules;
@@ -259,7 +259,7 @@
     prems: thm list,
     depth: int * bool Unsynchronized.ref} *
    {congs: thm Congtab.table * cong_name list,
-    procs: procedure Net.net,
+    simprocs: procedure Net.net,
     mk_rews:
      {mk: Proof.context -> thm -> thm list,
       mk_cong: Proof.context -> thm -> thm,
@@ -277,19 +277,19 @@
 
 fun map_ss1 f {rules, prems, depth} = make_ss1 (f (rules, prems, depth));
 
-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,
+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,
     subgoal_tac = subgoal_tac, loop_tacs = loop_tacs, solvers = 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 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 make_simpset (args1, args2) = Simpset (make_ss1 args1, make_ss2 args2);
 
-fun dest_ss (Simpset ({rules, ...}, {congs, procs, loop_tacs, solvers, ...})) =
+fun dest_ss (Simpset ({rules, ...}, {congs, simprocs, loop_tacs, solvers, ...})) =
  {simps = Net.entries rules
     |> map (fn {name, thm, ...} => (name, thm)),
-  procs = Net.entries procs
+  simprocs = Net.entries simprocs
     |> partition_eq eq_procedure
     |> map (fn ps as Procedure {name, ...} :: _ => (name, map (fn Procedure {lhs, ...} => lhs) ps)),
   congs = congs |> fst |> Congtab.dest,
@@ -326,10 +326,10 @@
   else
     let
       val Simpset ({rules = rules1, prems = prems1, depth = depth1},
-       {congs = (congs1, weak1), procs = procs1, mk_rews, term_ord, subgoal_tac,
+       {congs = (congs1, weak1), simprocs = 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), procs = procs2, mk_rews = _, term_ord = _, subgoal_tac = _,
+       {congs = (congs2, weak2), simprocs = simprocs2, mk_rews = _, term_ord = _, subgoal_tac = _,
         loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2;
 
       val rules' = Net.merge eq_rrule (rules1, rules2);
@@ -337,12 +337,12 @@
       val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1;
       val congs' = Congtab.merge (K true) (congs1, congs2);
       val weak' = merge (op =) (weak1, weak2);
-      val procs' = Net.merge eq_procedure (procs1, procs2);
+      val simprocs' = Net.merge eq_procedure (simprocs1, simprocs2);
       val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2);
       val unsafe_solvers' = merge eq_solver (unsafe_solvers1, unsafe_solvers2);
       val solvers' = merge eq_solver (solvers1, solvers2);
     in
-      make_simpset ((rules', prems', depth'), ((congs', weak'), procs',
+      make_simpset ((rules', prems', depth'), ((congs', weak'), simprocs',
         mk_rews, term_ord, subgoal_tac, loop_tacs', (unsafe_solvers', solvers')))
     end;
 
@@ -684,7 +684,7 @@
 in
 
 fun add_eqcong thm ctxt = ctxt |> map_simpset2
-  (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
+  (fn (congs, simprocs, 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]);
@@ -694,10 +694,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'), procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) end);
+    in ((xs', weak'), simprocs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) end);
 
 fun del_eqcong thm ctxt = ctxt |> map_simpset2
-  (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
+  (fn (congs, simprocs, 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]);
@@ -707,7 +707,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'), procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) end);
+    in ((xs', weak'), simprocs, 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;
@@ -751,8 +751,8 @@
  (cond_tracing ctxt (fn () =>
     print_term ctxt ("Adding simplification procedure " ^ quote name ^ " for") lhs);
   ctxt |> map_simpset2
-    (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
-      (congs, Net.insert_term eq_procedure (lhs, proc) procs,
+    (fn (congs, simprocs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
+      (congs, Net.insert_term eq_procedure (lhs, proc) simprocs,
         mk_rews, term_ord, subgoal_tac, loop_tacs, solvers))
   handle Net.INSERT =>
     (cond_warning ctxt (fn () => "Ignoring duplicate simplification procedure " ^ quote name);
@@ -760,20 +760,20 @@
 
 fun del_proc (proc as Procedure {name, lhs, ...}) ctxt =
   ctxt |> map_simpset2
-    (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
-      (congs, Net.delete_term eq_procedure (lhs, proc) procs,
+    (fn (congs, simprocs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
+      (congs, Net.delete_term eq_procedure (lhs, proc) simprocs,
         mk_rews, term_ord, subgoal_tac, loop_tacs, solvers))
   handle Net.DELETE =>
     (cond_warning ctxt (fn () => "Simplification procedure " ^ quote name ^ " not in simpset");
       ctxt);
 
-fun prep_procs (Simproc {name, lhss, proc, id}) =
+fun prep_simprocs (Simproc {name, lhss, proc, id}) =
   lhss |> map (fn lhs => Procedure {name = name, lhs = lhs, proc = proc, id = id});
 
 in
 
-fun ctxt addsimprocs ps = fold (fold add_proc o prep_procs) ps ctxt;
-fun ctxt delsimprocs ps = fold (fold del_proc o prep_procs) ps ctxt;
+fun ctxt addsimprocs ps = fold (fold add_proc o prep_simprocs) ps ctxt;
+fun ctxt delsimprocs ps = fold (fold del_proc o prep_simprocs) ps ctxt;
 
 end;
 
@@ -783,14 +783,14 @@
 local
 
 fun map_mk_rews f =
-  map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
+  map_simpset2 (fn (congs, simprocs, 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, procs, mk_rews', term_ord, subgoal_tac, loop_tacs, solvers) end);
+    in (congs, simprocs, mk_rews', term_ord, subgoal_tac, loop_tacs, solvers) end);
 
 in
 
@@ -819,50 +819,50 @@
 (* term_ord *)
 
 fun set_term_ord term_ord =
-  map_simpset2 (fn (congs, procs, mk_rews, _, subgoal_tac, loop_tacs, solvers) =>
-   (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers));
+  map_simpset2 (fn (congs, simprocs, mk_rews, _, subgoal_tac, loop_tacs, solvers) =>
+   (congs, simprocs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers));
 
 
 (* tactics *)
 
 fun set_subgoaler subgoal_tac =
-  map_simpset2 (fn (congs, procs, mk_rews, term_ord, _, loop_tacs, solvers) =>
-   (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers));
+  map_simpset2 (fn (congs, simprocs, mk_rews, term_ord, _, loop_tacs, solvers) =>
+   (congs, simprocs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers));
 
 fun ctxt setloop tac = ctxt |>
-  map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, _, solvers) =>
-   (congs, procs, mk_rews, term_ord, subgoal_tac, [("", tac)], solvers));
+  map_simpset2 (fn (congs, simprocs, mk_rews, term_ord, subgoal_tac, _, solvers) =>
+   (congs, simprocs, mk_rews, term_ord, subgoal_tac, [("", tac)], solvers));
 
 fun ctxt addloop (name, tac) = ctxt |>
-  map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
-    (congs, procs, mk_rews, term_ord, subgoal_tac,
+  map_simpset2 (fn (congs, simprocs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
+    (congs, simprocs, mk_rews, term_ord, subgoal_tac,
      AList.update (op =) (name, tac) loop_tacs, solvers));
 
 fun ctxt delloop name = ctxt |>
-  map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
-    (congs, procs, mk_rews, term_ord, subgoal_tac,
+  map_simpset2 (fn (congs, simprocs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
+    (congs, simprocs, 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, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, (unsafe_solvers, _)) =>
-    (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, (unsafe_solvers, [solver])));
+  (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])));
 
-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,
+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,
     subgoal_tac, loop_tacs, (unsafe_solvers, insert eq_solver solver solvers)));
 
-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,
+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,
     subgoal_tac, loop_tacs, ([solver], solvers)));
 
-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,
+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,
     subgoal_tac, loop_tacs, (insert eq_solver solver unsafe_solvers, solvers)));
 
-fun set_solvers solvers = map_simpset2 (fn (congs, procs, mk_rews, term_ord,
-  subgoal_tac, loop_tacs, _) => (congs, procs, mk_rews, term_ord,
+fun set_solvers solvers = map_simpset2 (fn (congs, simprocs, mk_rews, term_ord,
+  subgoal_tac, loop_tacs, _) => (congs, simprocs, mk_rews, term_ord,
   subgoal_tac, loop_tacs, (solvers, solvers)));
 
 
@@ -982,7 +982,7 @@
 
 fun rewritec (prover, maxt) ctxt t =
   let
-    val Simpset ({rules, ...}, {congs, procs, term_ord, ...}) = simpset_of ctxt;
+    val Simpset ({rules, ...}, {congs, 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';
@@ -1086,7 +1086,7 @@
       Abs _ $ _ => SOME (Thm.transitive eta_thm (Thm.beta_conversion false eta_t'), skel0)
     | _ =>
       (case rews (sort_rrules (Net.match_term rules eta_t)) of
-        NONE => proc_rews (Net.match_term procs eta_t)
+        NONE => proc_rews (Net.match_term simprocs eta_t)
       | some => some))
   end;
 
diff -r 2d2f476ab56e -r 34db40261287 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Tue Aug 13 15:50:25 2024 +0200
+++ b/src/Pure/simplifier.ML	Tue Aug 13 16:01:05 2024 +0200
@@ -277,10 +277,11 @@
     fun pretty_cong (name, thm) =
       Pretty.block [pretty_cong_name name, Pretty.str ":", Pretty.brk 1, pretty_thm thm];
 
-    val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} =
+    val {simps, simprocs, congs, loopers, unsafe_solvers, safe_solvers, ...} =
       dest_ss (simpset_of ctxt);
     val simprocs =
-      Name_Space.markup_entries verbose ctxt (Name_Space.space_of_table (get_simprocs ctxt)) procs;
+      Name_Space.markup_entries verbose ctxt
+        (Name_Space.space_of_table (get_simprocs ctxt)) simprocs;
   in
     [Pretty.big_list "simplification rules:" (map (pretty_thm_item o #2) simps),
       Pretty.big_list "simplification procedures:" (map pretty_simproc simprocs),