# HG changeset patch
# User wenzelm
# Date 1697880274 -7200
# Node ID 64973b03b778345f6ba0ebcbc8bc1c7e8c925301
# Parent  f6d2679ab6c11a245648635551eddc403e30cc30
more standard simproc_setup using ML antiquotation;

diff -r f6d2679ab6c1 -r 64973b03b778 src/HOL/Decision_Procs/langford.ML
--- a/src/HOL/Decision_Procs/langford.ML	Sat Oct 21 00:25:40 2023 +0200
+++ b/src/HOL/Decision_Procs/langford.ML	Sat Oct 21 11:24:34 2023 +0200
@@ -127,7 +127,7 @@
 
 local
 
-fun proc ctxt ct =
+fun reduce_ex_proc ctxt ct =
   (case Thm.term_of ct of
     \<^Const_>\<open>Ex _ for \<open>Abs _\<close>\<close> =>
       let
@@ -168,9 +168,7 @@
 
 in
 
-val reduce_ex_simproc =
-  Simplifier.make_simproc \<^context> "reduce_ex_simproc"
-    {lhss = [\<^term>\<open>\<exists>x. P x\<close>], proc = K proc};
+val reduce_ex_simproc = \<^simproc_setup>\<open>passive reduce_ex ("\<exists>x. P x") = \<open>K reduce_ex_proc\<close>\<close>;
 
 end;
 
diff -r f6d2679ab6c1 -r 64973b03b778 src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Oct 21 00:25:40 2023 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Oct 21 11:24:34 2023 +0200
@@ -148,9 +148,9 @@
   map (OF1 eq_imp_rel) (rev (Named_Theorems.get ctxt \<^named_theorems>\<open>quot_equiv\<close>))
 
 val regularize_simproc =
-  Simplifier.make_simproc \<^context> "regularize"
-    {lhss = [\<^term>\<open>Ball (Respects (R1 ===> R2)) P\<close>, \<^term>\<open>Bex (Respects (R1 ===> R2)) P\<close>],
-     proc = K ball_bex_range_simproc};
+  \<^simproc_setup>\<open>passive regularize
+    ("Ball (Respects (R1 ===> R2)) P" | "Bex (Respects (R1 ===> R2)) P") =
+    \<open>K ball_bex_range_simproc\<close>\<close>
 
 fun regularize_tac ctxt =
   let
diff -r f6d2679ab6c1 -r 64973b03b778 src/HOL/Tools/SMT/smt_real.ML
--- a/src/HOL/Tools/SMT/smt_real.ML	Sat Oct 21 00:25:40 2023 +0200
+++ b/src/HOL/Tools/SMT/smt_real.ML	Sat Oct 21 11:24:34 2023 +0200
@@ -116,10 +116,9 @@
 
 (* Z3 proof replay *)
 
-val real_linarith_proc =
-  Simplifier.make_simproc \<^context> "fast_real_arith"
-   {lhss = [\<^term>\<open>(m::real) < n\<close>, \<^term>\<open>(m::real) \<le> n\<close>, \<^term>\<open>(m::real) = n\<close>],
-    proc = K Lin_Arith.simproc}
+val real_linarith_simproc =
+  \<^simproc_setup>\<open>passive fast_real_arith ("(m::real) < n" | "(m::real) \<le> n" | "(m::real) = n") =
+    \<open>K Lin_Arith.simproc\<close>\<close>;
 
 
 (* setup *)
@@ -128,6 +127,6 @@
   SMTLIB_Interface.add_logic (10, smtlib_logic) #>
   setup_builtins #>
   Z3_Interface.add_mk_builtins smt_mk_builtins #>
-  SMT_Replay.add_simproc real_linarith_proc))
+  SMT_Replay.add_simproc real_linarith_simproc))
 
 end;
diff -r f6d2679ab6c1 -r 64973b03b778 src/HOL/Tools/SMT/smt_replay.ML
--- a/src/HOL/Tools/SMT/smt_replay.ML	Sat Oct 21 00:25:40 2023 +0200
+++ b/src/HOL/Tools/SMT/smt_replay.ML	Sat Oct 21 11:24:34 2023 +0200
@@ -140,20 +140,22 @@
   end
   handle THM _ => NONE
 
+  val fast_int_arith_simproc =
+    \<^simproc_setup>\<open>passive fast_int_arith ("(m::int) < n" | "(m::int) \<le> n" | "(m::int) = n") =
+      \<open>K Lin_Arith.simproc\<close>\<close>
+
+  val antisym_le_simproc =
+    \<^simproc_setup>\<open>passive antisym_le ("(x::'a::order) \<le> y") = \<open>K prove_antisym_le\<close>\<close>
+
+  val antisym_less_simproc =
+    \<^simproc_setup>\<open>passive antisym_less ("\<not> (x::'a::linorder) < y") = \<open>K prove_antisym_less\<close>\<close>
+
   val basic_simpset =
     simpset_of (put_simpset HOL_ss \<^context>
       addsimps @{thms field_simps times_divide_eq_right times_divide_eq_left arith_special
         arith_simps rel_simps array_rules z3div_def z3mod_def NO_MATCH_def}
-      addsimprocs [\<^simproc>\<open>numeral_divmod\<close>,
-        Simplifier.make_simproc \<^context> "fast_int_arith"
-         {lhss = [\<^term>\<open>(m::int) < n\<close>, \<^term>\<open>(m::int) \<le> n\<close>, \<^term>\<open>(m::int) = n\<close>],
-          proc = K Lin_Arith.simproc},
-        Simplifier.make_simproc \<^context> "antisym_le"
-         {lhss = [\<^term>\<open>(x::'a::order) \<le> y\<close>],
-          proc = K prove_antisym_le},
-        Simplifier.make_simproc \<^context> "antisym_less"
-         {lhss = [\<^term>\<open>\<not> (x::'a::linorder) < y\<close>],
-          proc = K prove_antisym_less}])
+      addsimprocs [\<^simproc>\<open>numeral_divmod\<close>, fast_int_arith_simproc,
+        antisym_le_simproc, antisym_less_simproc])
 
   structure Simpset = Generic_Data
   (
diff -r f6d2679ab6c1 -r 64973b03b778 src/HOL/Tools/int_arith.ML
--- a/src/HOL/Tools/int_arith.ML	Sat Oct 21 00:25:40 2023 +0200
+++ b/src/HOL/Tools/int_arith.ML	Sat Oct 21 11:24:34 2023 +0200
@@ -23,24 +23,22 @@
 val zeroth = Thm.symmetric (mk_meta_eq @{thm of_int_0});
 
 val zero_to_of_int_zero_simproc =
-  Simplifier.make_simproc \<^context> "zero_to_of_int_zero_simproc"
-   {lhss = [\<^term>\<open>0::'a::ring\<close>],
-    proc = fn _ => fn _ => fn ct =>
+  \<^simproc_setup>\<open>passive zero_to_of_int_zero ("0::'a::ring") =
+    \<open>fn _ => fn _ => fn ct =>
       let val T = Thm.ctyp_of_cterm ct in
         if Thm.typ_of T = \<^typ>\<open>int\<close> then NONE
         else SOME (Thm.instantiate' [SOME T] [] zeroth)
-      end};
+      end\<close>\<close>;
 
 val oneth = Thm.symmetric (mk_meta_eq @{thm of_int_1});
 
 val one_to_of_int_one_simproc =
-  Simplifier.make_simproc \<^context> "one_to_of_int_one_simproc"
-   {lhss = [\<^term>\<open>1::'a::ring_1\<close>],
-    proc = fn _ => fn _ => fn ct =>
+  \<^simproc_setup>\<open>passive one_to_of_int_one ("1::'a::ring_1") =
+    \<open>fn _ => fn _ => fn ct =>
       let val T = Thm.ctyp_of_cterm ct in
         if Thm.typ_of T = \<^typ>\<open>int\<close> then NONE
         else SOME (Thm.instantiate' [SOME T] [] oneth)
-      end};
+      end\<close>\<close>;
 
 fun check (Const (\<^const_name>\<open>Groups.one\<close>, \<^typ>\<open>int\<close>)) = false
   | check (Const (\<^const_name>\<open>Groups.one\<close>, _)) = true
@@ -63,14 +61,11 @@
   |> simpset_of;
 
 val zero_one_idom_simproc =
-  Simplifier.make_simproc \<^context> "zero_one_idom_simproc"
-   {lhss =
-      [\<^term>\<open>(x::'a::ring_char_0) = y\<close>,
-       \<^term>\<open>(x::'a::linordered_idom) < y\<close>,
-       \<^term>\<open>(x::'a::linordered_idom) \<le> y\<close>],
-    proc = fn _ => fn ctxt => fn ct =>
+  \<^simproc_setup>\<open>passive zero_one_idom
+    ("(x::'a::ring_char_0) = y" | "(u::'b::linordered_idom) < v" | "(u::'b::linordered_idom) \<le> v") =
+    \<open>fn _ => fn ctxt => fn ct =>
       if check (Thm.term_of ct)
       then SOME (Simplifier.rewrite (put_simpset conv_ss ctxt) ct)
-      else NONE};
+      else NONE\<close>\<close>
 
 end;
diff -r f6d2679ab6c1 -r 64973b03b778 src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Sat Oct 21 00:25:40 2023 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML	Sat Oct 21 11:24:34 2023 +0200
@@ -437,23 +437,21 @@
 val divide_cancel_numeral_factor = DivideCancelNumeralFactor.proc
 
 val field_divide_cancel_numeral_factor =
-  Simplifier.make_simproc \<^context> "field_divide_cancel_numeral_factor"
-   {lhss =
-     [\<^term>\<open>((l::'a::field) * m) / n\<close>,
-      \<^term>\<open>(l::'a::field) / (m * n)\<close>,
-      \<^term>\<open>((numeral v)::'a::field) / (numeral w)\<close>,
-      \<^term>\<open>((numeral v)::'a::field) / (- numeral w)\<close>,
-      \<^term>\<open>((- numeral v)::'a::field) / (numeral w)\<close>,
-      \<^term>\<open>((- numeral v)::'a::field) / (- numeral w)\<close>],
-    proc = K DivideCancelNumeralFactor.proc}
+  \<^simproc_setup>\<open>passive field_divide_cancel_numeral_factor
+    ("((l::'a::field) * m) / n" | "(l::'a::field) / (m * n)" |
+      "((numeral v)::'a::field) / (numeral w)" |
+      "((numeral v)::'a::field) / (- numeral w)" |
+      "((- numeral v)::'a::field) / (numeral w)" |
+      "((- numeral v)::'a::field) / (- numeral w)") =
+    \<open>K DivideCancelNumeralFactor.proc\<close>\<close>;
+
+val field_eq_cancel_numeral_factor =
+  \<^simproc_setup>\<open>passive field_eq_cancel_numeral_factor
+    ("(l::'a::field) * m = n" | "(l::'a::field) = m * n") =
+    \<open>K EqCancelNumeralFactor.proc\<close>\<close>;
 
 val field_cancel_numeral_factors =
-  [Simplifier.make_simproc \<^context> "field_eq_cancel_numeral_factor"
-    {lhss =
-       [\<^term>\<open>(l::'a::field) * m = n\<close>,
-        \<^term>\<open>(l::'a::field) = m * n\<close>],
-      proc = K EqCancelNumeralFactor.proc},
-   field_divide_cancel_numeral_factor]
+  [field_divide_cancel_numeral_factor, field_eq_cancel_numeral_factor]
 
 
 (** Declarations for ExtractCommonTerm **)
@@ -599,7 +597,7 @@
           (Thm.apply (Thm.apply eq t) z)))
   in Thm.equal_elim (Thm.symmetric th) TrueI end
 
-fun proc ctxt ct =
+fun add_frac_frac_proc ctxt ct =
   let
     val ((x,y),(w,z)) =
          (Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct
@@ -610,7 +608,7 @@
   in SOME (Thm.implies_elim (Thm.implies_elim th y_nz) z_nz) end
   handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
 
-fun proc2 ctxt ct =
+fun add_frac_num_proc ctxt ct =
   let
     val (l,r) = Thm.dest_binop ct
     val T = Thm.ctyp_of_cterm l
@@ -636,7 +634,7 @@
 
 val is_number = is_number o Thm.term_of
 
-fun proc3 ctxt ct =
+fun ord_frac_proc ct =
   (case Thm.term_of ct of
     Const(\<^const_name>\<open>Orderings.less\<close>,_)$(Const(\<^const_name>\<open>Rings.divide\<close>,_)$_$_)$_ =>
       let
@@ -683,25 +681,22 @@
   | _ => NONE) handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE
 
 val add_frac_frac_simproc =
-  Simplifier.make_simproc \<^context> "add_frac_frac_simproc"
-   {lhss = [\<^term>\<open>(x::'a::field) / y + (w::'a::field) / z\<close>],
-    proc = K proc}
+  \<^simproc_setup>\<open>passive add_frac_frac ("(x::'a::field) / y + (w::'a::field) / z") =
+    \<open>K add_frac_frac_proc\<close>\<close>
 
 val add_frac_num_simproc =
-  Simplifier.make_simproc \<^context> "add_frac_num_simproc"
-   {lhss = [\<^term>\<open>(x::'a::field) / y + z\<close>, \<^term>\<open>z + (x::'a::field) / y\<close>],
-    proc = K proc2}
+  \<^simproc_setup>\<open>passive add_frac_num ("(x::'a::field) / y + z" | "z + (x::'a::field) / y") =
+    \<open>K add_frac_num_proc\<close>\<close>
 
 val ord_frac_simproc =
-  Simplifier.make_simproc \<^context> "ord_frac_simproc"
-   {lhss =
-     [\<^term>\<open>(a::'a::{field,ord}) / b < c\<close>,
-      \<^term>\<open>(a::'a::{field,ord}) / b \<le> c\<close>,
-      \<^term>\<open>c < (a::'a::{field,ord}) / b\<close>,
-      \<^term>\<open>c \<le> (a::'a::{field,ord}) / b\<close>,
-      \<^term>\<open>c = (a::'a::{field,ord}) / b\<close>,
-      \<^term>\<open>(a::'a::{field, ord}) / b = c\<close>],
-    proc = K proc3}
+  \<^simproc_setup>\<open>passive ord_frac
+    ("(a::'a::{field,ord}) / b < c" |
+     "(a::'a::{field,ord}) / b \<le> c" |
+     "c < (a::'a::{field,ord}) / b" |
+     "c \<le> (a::'a::{field,ord}) / b" |
+     "c = (a::'a::{field,ord}) / b" |
+     "(a::'a::{field, ord}) / b = c") =
+    \<open>K (K ord_frac_proc)\<close>\<close>
 
 val field_comp_ss =
   simpset_of
diff -r f6d2679ab6c1 -r 64973b03b778 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Sat Oct 21 00:25:40 2023 +0200
+++ b/src/Tools/induct.ML	Sat Oct 21 11:24:34 2023 +0200
@@ -171,9 +171,7 @@
   | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct));
 
 val rearrange_eqs_simproc =
-  Simplifier.make_simproc \<^context> "rearrange_eqs"
-   {lhss = [\<^term>\<open>Pure.all (t :: 'a::{} \<Rightarrow> prop)\<close>],
-    proc = fn _ => fn ctxt => fn ct => mk_swap_rrule ctxt ct};
+  \<^simproc_setup>\<open>passive rearrange_eqs ("Pure.all (t :: 'a::{} \<Rightarrow> prop)") = \<open>K mk_swap_rrule\<close>\<close>;
 
 
 (* rotate k premises to the left by j, skipping over first j premises *)