# HG changeset patch
# User wenzelm
# Date 1697561729 -7200
# Node ID 103467dc5117ff8dfdde04786fad2f35f1123c08
# Parent  4f7dce5c1a81e89ed02639c1f7f3f80ecad8f788
support for "simproc_setup ... (passive)": allow to define simprocs in Isar that are not added to the simpset (yet);

diff -r 4f7dce5c1a81 -r 103467dc5117 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Tue Oct 17 15:51:28 2023 +0200
+++ b/src/HOL/Tools/record.ML	Tue Oct 17 18:55:29 2023 +0200
@@ -1062,6 +1062,7 @@
 *)
 val  _ = Theory.setup (Named_Target.theory_map (Simplifier.define_simproc \<^binding>\<open>select_update\<close>
    {lhss = [\<^term>\<open>x::'a::{}\<close>],
+    passive = false,
     proc = fn _ => fn ctxt => fn ct =>
       let
         val thy = Proof_Context.theory_of ctxt;
@@ -1166,6 +1167,7 @@
   both a more update and an update to a field within it.*)
 val  _ = Theory.setup (Named_Target.theory_map (Simplifier.define_simproc \<^binding>\<open>update\<close>
    {lhss = [\<^term>\<open>x::'a::{}\<close>],
+    passive = false,
     proc = fn _ => fn ctxt => fn ct =>
       let
         val thy = Proof_Context.theory_of ctxt;
@@ -1306,6 +1308,7 @@
 
 val  _ = Theory.setup (Named_Target.theory_map (Simplifier.define_simproc \<^binding>\<open>eq\<close>
    {lhss = [\<^term>\<open>r = s\<close>],
+    passive = false,
     proc = fn _ => fn ctxt => fn ct =>
       (case Thm.term_of ct of
         \<^Const_>\<open>HOL.eq T for _ _\<close> =>
@@ -1359,6 +1362,7 @@
 
 val  _ = Theory.setup (Named_Target.theory_map (Simplifier.define_simproc \<^binding>\<open>ex_sel_eq\<close>
    {lhss = [\<^term>\<open>Ex t\<close>],
+    passive = false,
     proc = fn _ => fn ctxt => fn ct =>
       let
         val thy = Proof_Context.theory_of ctxt;
diff -r 4f7dce5c1a81 -r 103467dc5117 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Oct 17 15:51:28 2023 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Oct 17 18:55:29 2023 +0200
@@ -17,7 +17,7 @@
   val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
   val oracle: bstring * Position.range -> Input.source -> theory -> theory
   val declaration: {syntax: bool, pervasive: bool} -> Input.source -> local_theory -> local_theory
-  val simproc_setup: string * Position.T -> string list -> Input.source ->
+  val simproc_setup: string * Position.T -> string list -> Input.source -> bool ->
     local_theory -> local_theory
   val qed: Method.text_range option -> Toplevel.transition -> Toplevel.transition
   val terminal_proof: Method.text_range * Method.text_range option ->
@@ -138,11 +138,12 @@
 
 (* simprocs *)
 
-fun simproc_setup name lhss source =
+fun simproc_setup name lhss source passive =
   ML_Context.expression (Input.pos_of source)
     (ML_Lex.read
       ("Theory.local_setup (Simplifier.define_simproc_cmd (" ^
         ML_Syntax.make_binding name ^ ") {lhss = " ^ ML_Syntax.print_strings lhss ^
+        ", passive = " ^ Bool.toString passive ^
         ", proc = (") @ ML_Lex.read_source source @ ML_Lex.read ")})")
   |> Context.proof_map;
 
diff -r 4f7dce5c1a81 -r 103467dc5117 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Tue Oct 17 15:51:28 2023 +0200
+++ b/src/Pure/Pure.thy	Tue Oct 17 18:55:29 2023 +0200
@@ -8,7 +8,7 @@
 keywords
     "!!" "!" "+" ":" ";" "<" "<=" "==" "=>" "?" "[" "\<comment>" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
     "\<subseteq>" "]" "binder" "by" "in" "infix" "infixl" "infixr" "is" "open" "output"
-    "overloaded" "pervasive" "premises" "structure" "unchecked"
+    "overloaded" "passive" "pervasive" "premises" "structure" "unchecked"
   and "private" "qualified" :: before_command
   and "assumes" "constrains" "defines" "fixes" "for" "if" "includes" "notes" "rewrites"
     "obtains" "shows" "when" "where" "|" :: quasi_command
@@ -334,8 +334,10 @@
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>simproc_setup\<close> "define simproc in ML"
     (Parse.name_position --
-      (\<^keyword>\<open>(\<close> |-- Parse.enum1 "|" Parse.term --| \<^keyword>\<open>)\<close> --| \<^keyword>\<open>=\<close>) --
-      Parse.ML_source >> (fn ((a, b), c) => Isar_Cmd.simproc_setup a b c));
+      (\<^keyword>\<open>(\<close> |-- Parse.enum1 "|" Parse.term --| \<^keyword>\<open>)\<close>) --
+      (\<^keyword>\<open>=\<close> |-- Parse.ML_source) --
+      Parse.opt_keyword "passive"
+    >> (fn (((a, b), c), d) => Isar_Cmd.simproc_setup a b c d));
 
 in end\<close>
 
diff -r 4f7dce5c1a81 -r 103467dc5117 src/Pure/ex/Def.thy
--- a/src/Pure/ex/Def.thy	Tue Oct 17 15:51:28 2023 +0200
+++ b/src/Pure/ex/Def.thy	Tue Oct 17 18:55:29 2023 +0200
@@ -68,7 +68,7 @@
 val _ =
   (Theory.setup o Named_Target.theory_map)
     (Simplifier.define_simproc \<^binding>\<open>expand_def\<close>
-      {lhss = [Free ("x", TFree ("'a", []))], proc = K get_def});
+      {lhss = [Free ("x", TFree ("'a", []))], passive = false, proc = K get_def});
 
 
 (* Isar command *)
diff -r 4f7dce5c1a81 -r 103467dc5117 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Tue Oct 17 15:51:28 2023 +0200
+++ b/src/Pure/simplifier.ML	Tue Oct 17 18:55:29 2023 +0200
@@ -37,8 +37,10 @@
   val cong_del: attribute
   val check_simproc: Proof.context -> xstring * Position.T -> string * simproc
   val the_simproc: Proof.context -> string -> simproc
-  type 'a simproc_spec = {lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option}
-  val make_simproc: Proof.context -> string -> term simproc_spec -> simproc
+  val make_simproc: Proof.context -> string ->
+    {lhss: term list, proc: morphism -> Proof.context -> cterm -> thm option} -> simproc
+  type 'a simproc_spec =
+    {lhss: 'a list, passive: bool, proc: morphism -> Proof.context -> cterm -> thm option}
   val define_simproc: binding -> term simproc_spec -> local_theory -> local_theory
   val define_simproc_cmd: binding -> string simproc_spec -> local_theory -> local_theory
   val pretty_simpset: bool -> Proof.context -> Pretty.T
@@ -120,8 +122,6 @@
 
 (* define simprocs *)
 
-type 'a simproc_spec = {lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option};
-
 fun make_simproc ctxt name {lhss, proc} =
   let
     val ctxt' = fold Proof_Context.augment lhss ctxt;
@@ -131,9 +131,14 @@
       {lhss = lhss', proc = Morphism.entity proc}
   end;
 
+type 'a simproc_spec =
+ {lhss: 'a list,
+  passive: bool,
+  proc: morphism -> Proof.context -> cterm -> thm option};
+
 local
 
-fun def_simproc prep b {lhss, proc} lthy =
+fun def_simproc prep b {lhss, passive, proc} lthy =
   let
     val simproc0 =
       make_simproc lthy (Local_Theory.full_name lthy b) {lhss = prep lthy lhss, proc = proc};
@@ -146,7 +151,7 @@
         in
           context
           |> Simprocs.map (#2 o Name_Space.define context true (b', simproc'))
-          |> map_ss (fn ctxt => ctxt addsimprocs [simproc'])
+          |> not passive ? map_ss (fn ctxt => ctxt addsimprocs [simproc'])
         end)
   end;