merged

--- a/NEWS	Wed May 21 21:36:59 2025 +0200
+++ b/NEWS	Wed May 21 21:51:56 2025 +0200
@@ -78,7 +78,7 @@
 
 *** HOL ***
 
-* ML bindings for theorms Ball_def, Bex_def, CollectD, CollectE, CollectI,
+* ML bindings for theorems Ball_def, Bex_def, CollectD, CollectE, CollectI,
 Collect_conj_eq, Collect_mem_eq, IntD1, IntD2, IntE, IntI, Int_Collect, UNIV_I,
 UNIV_witness, UnE, UnI1, UnI2, ballE, ballI, bexCI, bexE, bexI, bex_triv, bspec,
 contra_subsetD, equalityCE, equalityD1, equalityD2, equalityE, equalityI,

--- a/src/Doc/Isar_Ref/Generic.thy	Wed May 21 21:36:59 2025 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy	Wed May 21 21:51:56 2025 +0200
@@ -955,10 +955,14 @@
   @{define_ML_type solver} \\
   @{define_ML Simplifier.mk_solver: "string ->
   (Proof.context -> int -> tactic) -> solver"} \\
-  @{define_ML_infix setSolver: "Proof.context * solver -> Proof.context"} \\
-  @{define_ML_infix addSolver: "Proof.context * solver -> Proof.context"} \\
-  @{define_ML_infix setSSolver: "Proof.context * solver -> Proof.context"} \\
-  @{define_ML_infix addSSolver: "Proof.context * solver -> Proof.context"} \\
+  @{define_ML Simplifier.set_safe_solver: "
+  solver -> Proof.context -> Proof.context"} \\
+  @{define_ML Simplifier.add_safe_solver: "
+  solver -> Proof.context -> Proof.context"} \\
+  @{define_ML Simplifier.set_unsafe_solver: "
+  solver -> Proof.context -> Proof.context"} \\
+  @{define_ML Simplifier.add_unsafe_solver: "
+  solver -> Proof.context -> Proof.context"} \\
   \end{mldecls}
 
   A solver is a tactic that attempts to solve a subgoal after simplification.
@@ -989,14 +993,14 @@
   \<^descr> \<^ML>\<open>Simplifier.mk_solver\<close>~\<open>name tac\<close> turns \<open>tac\<close> into a solver; the
   \<open>name\<close> is only attached as a comment and has no further significance.
 
-  \<^descr> \<open>ctxt setSSolver solver\<close> installs \<open>solver\<close> as the safe solver of \<open>ctxt\<close>.
+  \<^descr> \<^ML>\<open>Simplifier.set_safe_solver\<close>~\<open>solver ctxt\<close> installs \<open>solver\<close> as the safe solver of \<open>ctxt\<close>.
 
-  \<^descr> \<open>ctxt addSSolver solver\<close> adds \<open>solver\<close> as an additional safe solver; it
+  \<^descr> \<^ML>\<open>Simplifier.add_safe_solver\<close>~\<open>solver ctxt\<close> adds \<open>solver\<close> as an additional safe solver; it
   will be tried after the solvers which had already been present in \<open>ctxt\<close>.
 
-  \<^descr> \<open>ctxt setSolver solver\<close> installs \<open>solver\<close> as the unsafe solver of \<open>ctxt\<close>.
+  \<^descr> \<^ML>\<open>Simplifier.set_unsafe_solver\<close>~\<open>solver ctxt\<close> installs \<open>solver\<close> as the unsafe solver of \<open>ctxt\<close>.
 
-  \<^descr> \<open>ctxt addSolver solver\<close> adds \<open>solver\<close> as an additional unsafe solver; it
+  \<^descr> \<^ML>\<open>Simplifier.add_unsafe_solver\<close>~\<open>solver ctxt\<close> adds \<open>solver\<close> as an additional unsafe solver; it
   will be tried after the solvers which had already been present in \<open>ctxt\<close>.
 
 
@@ -1038,12 +1042,11 @@
 
 text \<open>
   \begin{mldecls}
-  @{define_ML_infix setloop: "Proof.context *
-  (Proof.context -> int -> tactic) -> Proof.context"} \\
-  @{define_ML_infix addloop: "Proof.context *
-  (string * (Proof.context -> int -> tactic))
-  -> Proof.context"} \\
-  @{define_ML_infix delloop: "Proof.context * string -> Proof.context"} \\
+  @{define_ML Simplifier.set_loop: "(Proof.context -> int -> tactic) ->
+  Proof.context -> Proof.context"} \\
+  @{define_ML Simplifier.add_loop: "string * (Proof.context -> int -> tactic) ->
+  Proof.context -> Proof.context"} \\
+  @{define_ML Simplifier.del_loop: "string -> Proof.context -> Proof.context"} \\
   @{define_ML Splitter.add_split: "thm -> Proof.context -> Proof.context"} \\
   @{define_ML Splitter.add_split: "thm -> Proof.context -> Proof.context"} \\
   @{define_ML Splitter.add_split_bang: "
@@ -1060,14 +1063,14 @@
   Another possibility is to apply an elimination rule on the assumptions. More
   adventurous loopers could start an induction.
 
-    \<^descr> \<open>ctxt setloop tac\<close> installs \<open>tac\<close> as the only looper tactic of \<open>ctxt\<close>.
+    \<^descr> \<^ML>\<open>Simplifier.set_loop\<close>~\<open>tac ctxt\<close> installs \<open>tac\<close> as the only looper tactic of \<open>ctxt\<close>.
 
-    \<^descr> \<open>ctxt addloop (name, tac)\<close> adds \<open>tac\<close> as an additional looper tactic
+    \<^descr> \<^ML>\<open>Simplifier.add_loop\<close>~\<open>(name, tac) ctxt\<close> adds \<open>tac\<close> as an additional looper tactic
     with name \<open>name\<close>, which is significant for managing the collection of
     loopers. The tactic will be tried after the looper tactics that had
     already been present in \<open>ctxt\<close>.
 
-    \<^descr> \<open>ctxt delloop name\<close> deletes the looper tactic that was associated with
+    \<^descr> \<^ML>\<open>Simplifier.del_loop\<close>~\<open>name ctxt\<close> deletes the looper tactic that was associated with
     \<open>name\<close> from \<open>ctxt\<close>.
 
     \<^descr> \<^ML>\<open>Splitter.add_split\<close>~\<open>thm ctxt\<close> adds split tactic

--- a/src/Pure/raw_simplifier.ML	Wed May 21 21:36:59 2025 +0200
+++ b/src/Pure/raw_simplifier.ML	Wed May 21 21:51:56 2025 +0200
@@ -84,8 +84,11 @@
   val get_mksimps_context: Proof.context -> (thm -> Proof.context -> thm list * Proof.context)
   val set_mksimps_context: (thm -> Proof.context -> thm list * Proof.context) ->
     Proof.context -> Proof.context
+  val add_simps: thm list -> Proof.context -> Proof.context
   val add_simp: thm -> Proof.context -> Proof.context
+  val del_simps: thm list -> Proof.context -> Proof.context
   val del_simp: thm -> Proof.context -> Proof.context
+  val flip_simps: thm list -> Proof.context -> Proof.context
   val flip_simp: thm -> Proof.context -> Proof.context
   val mk_cong: Proof.context -> thm -> thm
   val set_mkcong: (Proof.context -> thm -> thm) -> Proof.context -> Proof.context
@@ -102,10 +105,17 @@
   val set_subgoaler: (Proof.context -> int -> tactic) -> Proof.context -> Proof.context
   val prems_of: Proof.context -> thm list
   val add_prems: thm list -> Proof.context -> Proof.context
+  val loop_tac: Proof.context -> int -> tactic
+  val set_loop: (Proof.context -> int -> tactic) -> Proof.context -> Proof.context
+  val add_loop: string * (Proof.context -> int -> tactic) -> Proof.context -> Proof.context
+  val del_loop: string -> Proof.context -> Proof.context
   val solvers: Proof.context -> solver list * solver list
   val solver: Proof.context -> solver -> int -> tactic
+  val set_safe_solver: solver -> Proof.context -> Proof.context
+  val add_safe_solver: solver -> Proof.context -> Proof.context
+  val set_unsafe_solver: solver -> Proof.context -> Proof.context
+  val add_unsafe_solver: solver -> Proof.context -> Proof.context
   val set_solvers: solver list -> Proof.context -> Proof.context
-  val loop_tac: Proof.context -> int -> tactic
   val default_mk_sym: Proof.context -> thm -> thm option
   val set_reorient: (Proof.context -> term list -> term -> term -> bool) ->
     Proof.context -> Proof.context
@@ -630,7 +640,7 @@
 
 local
 
-fun comb_simps ctxt comb mk_rrule sym thms =
+fun comb_simps comb mk_rrule sym thms ctxt =
   let val rews = maps (fn thm => #1 (extract_rews sym (Thm.transfer' ctxt thm) ctxt)) thms;
   in fold (fold comb o mk_rrule) rews ctxt end;
 
@@ -657,27 +667,35 @@
 *)
 in
 
-fun ctxt addsimps thms =
-  comb_simps ctxt insert_rrule (mk_rrule ctxt) false thms;
+fun add_simps thms ctxt =
+  comb_simps insert_rrule (mk_rrule ctxt) false thms ctxt;
 
-fun addsymsimps ctxt thms =
-  comb_simps ctxt insert_rrule (mk_rrule ctxt) true thms;
+fun add_flipped_simps thms ctxt =
+  comb_simps insert_rrule (mk_rrule ctxt) true thms ctxt;
+
+fun ctxt addsimps thms = ctxt |> add_simps thms;
+
+fun add_simp thm = add_simps [thm];
 
-fun ctxt delsimps thms =
-  comb_simps ctxt (del_rrule true) (map mk_rrule2 o mk_rrule ctxt) false thms;
+fun del_simps thms ctxt =
+  comb_simps (del_rrule true) (map mk_rrule2 o mk_rrule ctxt) false thms ctxt;
+
+fun del_simps_quiet thms ctxt =
+  comb_simps (del_rrule false) (map mk_rrule2 o mk_rrule ctxt) false thms ctxt;
 
-fun delsimps_quiet ctxt thms =
-  comb_simps ctxt (del_rrule false) (map mk_rrule2 o mk_rrule ctxt) false thms;
+fun ctxt delsimps thms = ctxt |> del_simps thms;
 
-fun add_simp thm ctxt = ctxt addsimps [thm];
+fun del_simp thm = del_simps [thm];
+
+fun flip_simps thms = del_simps_quiet thms #> add_flipped_simps thms;
 (*
 with check for presence of symmetric version:
   if sym_present ctxt [thm]
   then (cond_warning ctxt (fn () => print_thm0 ctxt "Ignoring rewrite rule:" thm); ctxt)
   else ctxt addsimps [thm];
 *)
-fun del_simp thm ctxt = ctxt delsimps [thm];
-fun flip_simp thm ctxt = addsymsimps (delsimps_quiet ctxt [thm]) [thm];
+
+fun flip_simp thm = flip_simps [thm];
 
 end;
 
@@ -866,38 +884,52 @@
   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 |>
+fun set_loop tac =
   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 |>
+fun ctxt setloop tac = ctxt |> set_loop tac;
+
+fun add_loop (name, 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 |>
+fun ctxt addloop tac = ctxt |> add_loop tac;
+
+fun del_loop name ctxt = ctxt |>
   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
+fun ctxt delloop name = ctxt |> del_loop name;
+
+fun set_safe_solver solver = 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])));
 
-fun ctxt addSSolver solver = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, term_ord,
+fun ctxt setSSolver solver = ctxt |> set_safe_solver solver;
+
+fun add_safe_solver solver = 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, procs, mk_rews, term_ord,
+fun ctxt addSSolver solver = ctxt |> add_safe_solver solver;
+
+fun set_unsafe_solver solver = 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, procs, mk_rews, term_ord,
+fun ctxt setSolver solver = ctxt |> set_unsafe_solver solver;
+
+fun add_unsafe_solver solver = 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 ctxt addSolver solver = ctxt |> add_unsafe_solver solver;
+
 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)));