# HG changeset patch # User wenzelm # Date 1697996428 -7200 # Node ID f0cb320603cb8bae7a90fb936b603fc8e5bbc32a # Parent f2e845c3e65c1740e652b330eb7c5ba94331049b# Parent 9d44cc361f19647ce96cc7f82eb42063e5d348d2 merged diff -r f2e845c3e65c -r f0cb320603cb NEWS --- a/NEWS Fri Oct 20 12:25:35 2023 +0200 +++ b/NEWS Sun Oct 22 19:40:28 2023 +0200 @@ -31,6 +31,21 @@ the current thread attributes (normally interruptible). Various examples occur in the Isabelle sources (.ML and .thy files). +* ML antiquotation "simproc_setup" inlines an invocation of +Simplifier.simproc_setup, using the same concrete syntax as the +corresponding Isar command. This allows to introduce a new simproc +conveniently within an ML module, and refer directly to its ML value. +For example, the simproc "Record.eq" is defined in +~~/src/HOL/Tools/record.ML as follows: + + val eq_simproc = \<^simproc_setup>\eq ("r = s") = \K eq_proc\\; + +* Simplification procedures may be distinguished via characteristic +theorems that are specified as 'identifier' in ML antiquotation +"simproc_setup" (but not in the corresponding Isar command). This allows +to work with several versions of the simproc, e.g. due to locale +interpretations. + * Isabelle/ML explicitly rejects 'handle' with catch-all patterns. INCOMPATIBILITY, better use \<^try>\...\ with 'catch' or 'finally', or as last resort declare [[ML_catch_all]] within the theory context. diff -r f2e845c3e65c -r f0cb320603cb etc/symbols --- a/etc/symbols Fri Oct 20 12:25:35 2023 +0200 +++ b/etc/symbols Sun Oct 22 19:40:28 2023 +0200 @@ -478,6 +478,7 @@ \<^scala_type> argument: cartouche \<^session> argument: cartouche \<^simproc> argument: cartouche +\<^simproc_setup> argument: cartouche \<^sort> argument: cartouche \<^syntax_const> argument: cartouche \<^system_option> argument: cartouche diff -r f2e845c3e65c -r f0cb320603cb lib/texinputs/isabellesym.sty --- a/lib/texinputs/isabellesym.sty Fri Oct 20 12:25:35 2023 +0200 +++ b/lib/texinputs/isabellesym.sty Sun Oct 22 19:40:28 2023 +0200 @@ -467,6 +467,7 @@ \newcommand{\isactrlscalaUNDERSCOREobject}{\isakeywordcontrol{scala{\isacharunderscore}object}} \newcommand{\isactrlscalaUNDERSCOREtype}{\isakeywordcontrol{scala{\isacharunderscore}type}} \newcommand{\isactrlsimproc}{\isakeywordcontrol{simproc}} +\newcommand{\isactrlsimprocUNDERSCOREsetup}{\isakeywordcontrol{simproc{\isacharunderscore}setup}} \newcommand{\isactrlsort}{\isakeywordcontrol{sort}} \newcommand{\isactrlsyntaxUNDERSCOREconst}{\isakeywordcontrol{syntax{\isacharunderscore}const}} \newcommand{\isactrlsystemUNDERSCOREoption}{\isakeywordcontrol{system{\isacharunderscore}option}} diff -r f2e845c3e65c -r f0cb320603cb src/Doc/Codegen/Computations.thy --- a/src/Doc/Codegen/Computations.thy Fri Oct 20 12:25:35 2023 +0200 +++ b/src/Doc/Codegen/Computations.thy Sun Oct 22 19:40:28 2023 +0200 @@ -276,8 +276,7 @@ \<^instantiate>\x = ct and y = \if b then \<^cterm>\True\ else \<^cterm>\False\\ in cterm \x \ y\ for x y :: bool\; - val (_, dvd_oracle) = Context.>>> (Context.map_theory_result - (Thm.add_oracle (\<^binding>\dvd\, raw_dvd))); + val (_, dvd_oracle) = Theory.setup_result (Thm.add_oracle (\<^binding>\dvd\, raw_dvd)); in diff -r f2e845c3e65c -r f0cb320603cb src/Doc/Isar_Ref/Generic.thy --- a/src/Doc/Isar_Ref/Generic.thy Fri Oct 20 12:25:35 2023 +0200 +++ b/src/Doc/Isar_Ref/Generic.thy Sun Oct 22 19:40:28 2023 +0200 @@ -782,53 +782,78 @@ subsection \Simplification procedures \label{sec:simproc}\ text \ - Simplification procedures are ML functions that produce proven rewrite rules - on demand. They are associated with higher-order patterns that approximate - the left-hand sides of equations. The Simplifier first matches the current - redex against one of the LHS patterns; if this succeeds, the corresponding - ML function is invoked, passing the Simplifier context and redex term. Thus - rules may be specifically fashioned for particular situations, resulting in - a more powerful mechanism than term rewriting by a fixed set of rules. + A \<^emph>\simplification procedure\ or \<^emph>\simproc\ is an ML function that produces + proven rewrite rules on demand. Simprocs are guarded by multiple \<^emph>\patterns\ + for the left-hand sides of equations. The Simplifier first matches the + current redex against one of the LHS patterns; if this succeeds, the + corresponding ML function is invoked, passing the Simplifier context and + redex term. The function may choose to succeed with a specific result for + the redex, or fail. - Any successful result needs to be a (possibly conditional) rewrite rule \t \ - u\ that is applicable to the current redex. The rule will be applied just as - any ordinary rewrite rule. It is expected to be already in \<^emph>\internal form\, - bypassing the automatic preprocessing of object-level equivalences. + The successful result of a simproc needs to be a (possibly conditional) + rewrite rule \t \ u\ that is applicable to the current redex. The rule will + be applied just as any ordinary rewrite rule. It is expected to be already + in \<^emph>\internal form\ of the Pure logic, bypassing the automatic preprocessing + of object-level equivalences. \begin{matharray}{rcl} @{command_def "simproc_setup"} & : & \local_theory \ local_theory\ \\ + @{ML_antiquotation_def "simproc_setup"} & : & \ML antiquotation\ \\ simproc & : & \attribute\ \\ \end{matharray} \<^rail>\ - @@{command simproc_setup} @{syntax name} '(' (@{syntax term} + '|') ')' '=' - @{syntax text}; - + @{syntax_def simproc_setup}: (@'passive')? @{syntax name} + patterns '=' @{syntax embedded} + ; + @{syntax_def simproc_setup_id}: + @{syntax simproc_setup} (@'identifier' @{syntax thms})? + ; + patterns: '(' (@{syntax term} + '|') ')' + ; + @@{command simproc_setup} @{syntax simproc_setup} + ; @@{attribute simproc} (('add' ':')? | 'del' ':') (@{syntax name}+) \ - \<^descr> @{command "simproc_setup"} defines a named simplification procedure that - is invoked by the Simplifier whenever any of the given term patterns match - the current redex. The implementation, which is provided as ML source text, - needs to be of type - \<^ML_type>\morphism -> Proof.context -> cterm -> thm option\, where the - \<^ML_type>\cterm\ represents the current redex \r\ and the result is supposed - to be some proven rewrite rule \r \ r'\ (or a generalized version), or \<^ML>\NONE\ to indicate failure. The \<^ML_type>\Proof.context\ argument holds the - full context of the current Simplifier invocation. The \<^ML_type>\morphism\ - informs about the difference of the original compilation context wrt.\ the - one of the actual application later on. + \<^descr> Command @{command "simproc_setup"} defines a named simplification + procedure that is invoked by the Simplifier whenever any of the given term + patterns match the current redex. The implementation, which is provided as + embedded ML source, needs to be of type + \<^ML_type>\morphism -> Proof.context -> cterm -> thm option\, + where the \<^ML_type>\cterm\ represents the current redex \r\ and the result + is supposed to be \<^ML>\SOME\ proven rewrite rule \r \ r'\ (or a + generalized version); \<^ML>\NONE\ indicates failure. The + \<^ML_type>\Proof.context\ argument holds the full context of the current + Simplifier invocation. + + The \<^ML_type>\morphism\ tells how to move from the abstract context of the + original definition into the concrete context of applications. This is only + relevant for simprocs that are defined ``\<^theory_text>\in\'' a local theory context + (e.g.\ @{command "locale"} with later @{command "interpretation"}). - Morphisms are only relevant for simprocs that are defined within a local - target context, e.g.\ in a locale. + By default, the simproc is declared to the current Simplifier context and + thus \<^emph>\active\. The keyword \<^theory_text>\passive\ avoids that: it merely defines a + simproc that can be activated in a different context later on. - \<^descr> \simproc add: name\ and \simproc del: name\ add or delete named simprocs - to the current Simplifier context. The default is to add a simproc. Note - that @{command "simproc_setup"} already adds the new simproc to the - subsequent context. + \<^descr> ML antiquotation @{ML_antiquotation_ref simproc_setup} is like command + @{command simproc_setup}, with slightly extended syntax following @{syntax + simproc_setup_id}. It allows to introduce a new simproc conveniently within + an ML module, and refer directly to its ML value. For example, see various + uses in @{file "~~/src/HOL/Tools/record.ML"}. + + The optional \<^theory_text>\identifier\ specifies characteristic theorems to distinguish + simproc instances after application of morphisms, e.g.\ @{command locale} + with multiple @{command interpretation}. See also the minimal example below. + + \<^descr> Attributes \[simproc add: name]\ and \[simproc del: name]\ add or delete + named simprocs to the current Simplifier context. The default is to add a + simproc. Note that @{command "simproc_setup"} already adds the new simproc + by default, unless it specified as \<^theory_text>\passive\. \ -subsubsection \Example\ +subsubsection \Examples\ text \ The following simplification procedure for @{thm [source = false, @@ -847,7 +872,22 @@ text \ Since the Simplifier applies simplification procedures frequently, it is - important to make the failure check in ML reasonably fast.\ + important to make the failure check in ML reasonably fast. + + \<^medskip> The subsequent example shows how to define a local simproc with extra + identifier to distinguish its instances after interpretation: +\ + +locale loc = fixes x y :: 'a assumes eq: "x = y" +begin + +ML \ + \<^simproc_setup>\proc (x) = + \fn phi => fn _ => fn _ => SOME (Morphism.thm phi @{thm eq})\ + identifier loc_axioms\ +\ + +end subsection \Configurable Simplifier strategies \label{sec:simp-strategies}\ diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Analysis/Measurable.thy --- a/src/HOL/Analysis/Measurable.thy Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Analysis/Measurable.thy Sun Oct 22 19:40:28 2023 +0200 @@ -67,7 +67,8 @@ method_setup\<^marker>\tag important\ measurable = \ Scan.lift (Scan.succeed (METHOD o Measurable.measurable_tac)) \ "measurability prover" -simproc_setup\<^marker>\tag important\ measurable ("A \ sets M" | "f \ measurable M N") = \K Measurable.simproc\ +simproc_setup\<^marker>\tag important\ measurable ("A \ sets M" | "f \ measurable M N") = + \K Measurable.proc\ setup \ Global_Theory.add_thms_dynamic (\<^binding>\measurable\, Measurable.get_all) diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Analysis/measurable.ML --- a/src/HOL/Analysis/measurable.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Analysis/measurable.ML Sun Oct 22 19:40:28 2023 +0200 @@ -22,14 +22,14 @@ val measurable_tac : Proof.context -> thm list -> tactic - val simproc : Proof.context -> cterm -> thm option + val proc : Simplifier.proc val add_preprocessor : string -> preprocessor -> Context.generic -> Context.generic val del_preprocessor : string -> Context.generic -> Context.generic val add_local_cong : thm -> Proof.context -> Proof.context val prepare_facts : Proof.context -> thm list -> (thm list * Proof.context) -end ; +end structure Measurable : MEASURABLE = struct @@ -256,7 +256,7 @@ in debug_tac ctxt (K "start") (REPEAT (single_step_tac 1)) end; -fun simproc ctxt redex = +fun proc ctxt redex = let val t = HOLogic.mk_Trueprop (Thm.term_of redex); fun tac {context = ctxt, prems = _ } = diff -r f2e845c3e65c -r f0cb320603cb src/HOL/BNF_Least_Fixpoint.thy --- a/src/HOL/BNF_Least_Fixpoint.thy Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/BNF_Least_Fixpoint.thy Sun Oct 22 19:40:28 2023 +0200 @@ -199,6 +199,6 @@ ML_file \Tools/datatype_simprocs.ML\ simproc_setup datatype_no_proper_subterm - ("(x :: 'a :: size) = y") = \K Datatype_Simprocs.no_proper_subterm_simproc\ + ("(x :: 'a :: size) = y") = \K Datatype_Simprocs.no_proper_subterm_proc\ end diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Decision_Procs/Commutative_Ring.thy --- a/src/HOL/Decision_Procs/Commutative_Ring.thy Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Sun Oct 22 19:40:28 2023 +0200 @@ -663,8 +663,7 @@ \<^instantiate>\x = ct and y = \Thm.cterm_of ctxt t\ in cterm \x \ y\ for x y :: pol\; -val (_, raw_pol_oracle) = Context.>>> (Context.map_theory_result - (Thm.add_oracle (\<^binding>\pnsubstl\, pol))); +val (_, raw_pol_oracle) = Theory.setup_result (Thm.add_oracle (\<^binding>\pnsubstl\, pol)); fun pol_oracle ctxt ct t = raw_pol_oracle (ctxt, ct, t); diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Decision_Procs/Reflective_Field.thy --- a/src/HOL/Decision_Procs/Reflective_Field.thy Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Decision_Procs/Reflective_Field.thy Sun Oct 22 19:40:28 2023 +0200 @@ -643,8 +643,7 @@ \<^instantiate>\x = ct and y = \Thm.cterm_of ctxt t\ in cterm \x \ y\ for x y :: \pexpr \ pexpr \ pexpr list\\; -val (_, raw_fnorm_oracle) = Context.>>> (Context.map_theory_result - (Thm.add_oracle (\<^binding>\fnorm\, fnorm))); +val (_, raw_fnorm_oracle) = Theory.setup_result (Thm.add_oracle (\<^binding>\fnorm\, fnorm)); fun fnorm_oracle ctxt ct t = raw_fnorm_oracle (ctxt, ct, t); diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Decision_Procs/langford.ML --- a/src/HOL/Decision_Procs/langford.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Decision_Procs/langford.ML Sun Oct 22 19:40:28 2023 +0200 @@ -127,7 +127,7 @@ local -fun proc ctxt ct = +fun reduce_ex_proc ctxt ct = (case Thm.term_of ct of \<^Const_>\Ex _ for \Abs _\\ => let @@ -168,9 +168,7 @@ in -val reduce_ex_simproc = - Simplifier.make_simproc \<^context> "reduce_ex_simproc" - {lhss = [\<^term>\\x. P x\], proc = K proc}; +val reduce_ex_simproc = \<^simproc_setup>\passive reduce_ex ("\x. P x") = \K reduce_ex_proc\\; end; diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Finite_Set.thy Sun Oct 22 19:40:28 2023 +0200 @@ -24,7 +24,7 @@ end -simproc_setup finite_Collect ("finite (Collect P)") = \K Set_Comprehension_Pointfree.simproc\ +simproc_setup finite_Collect ("finite (Collect P)") = \K Set_Comprehension_Pointfree.proc\ declare [[simproc del: finite_Collect]] diff -r f2e845c3e65c -r f0cb320603cb src/HOL/HOL.thy --- a/src/HOL/HOL.thy Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/HOL.thy Sun Oct 22 19:40:28 2023 +0200 @@ -1542,33 +1542,32 @@ ML_file \~~/src/Tools/induction.ML\ +simproc_setup passive swap_induct_false ("induct_false \ PROP P \ PROP Q") = + \fn _ => fn _ => fn ct => + (case Thm.term_of ct of + _ $ (P as _ $ \<^Const_>\induct_false\) $ (_ $ Q $ _) => + if P <> Q then SOME Drule.swap_prems_eq else NONE + | _ => NONE)\ + +simproc_setup passive induct_equal_conj_curry ("induct_conj P Q \ PROP R") = + \fn _ => fn _ => fn ct => + (case Thm.term_of ct of + _ $ (_ $ P) $ _ => + let + fun is_conj \<^Const_>\induct_conj for P Q\ = is_conj P andalso is_conj Q + | is_conj \<^Const_>\induct_equal _ for _ _\ = true + | is_conj \<^Const_>\induct_true\ = true + | is_conj \<^Const_>\induct_false\ = true + | is_conj _ = false + in if is_conj P then SOME @{thm induct_conj_curry} else NONE end + | _ => NONE)\ + declaration \ - fn _ => Induct.map_simpset (fn ss => ss - addsimprocs - [Simplifier.make_simproc \<^context> "swap_induct_false" - {lhss = [\<^term>\induct_false \ PROP P \ PROP Q\], - proc = fn _ => fn _ => fn ct => - (case Thm.term_of ct of - _ $ (P as _ $ \<^Const_>\induct_false\) $ (_ $ Q $ _) => - if P <> Q then SOME Drule.swap_prems_eq else NONE - | _ => NONE)}, - Simplifier.make_simproc \<^context> "induct_equal_conj_curry" - {lhss = [\<^term>\induct_conj P Q \ PROP R\], - proc = fn _ => fn _ => fn ct => - (case Thm.term_of ct of - _ $ (_ $ P) $ _ => - let - fun is_conj \<^Const_>\induct_conj for P Q\ = - is_conj P andalso is_conj Q - | is_conj \<^Const_>\induct_equal _ for _ _\ = true - | is_conj \<^Const_>\induct_true\ = true - | is_conj \<^Const_>\induct_false\ = true - | is_conj _ = false - in if is_conj P then SOME @{thm induct_conj_curry} else NONE end - | _ => NONE)}] + K (Induct.map_simpset (fn ss => ss + addsimprocs [\<^simproc>\swap_induct_false\, \<^simproc>\induct_equal_conj_curry\] |> Simplifier.set_mksimps (fn ctxt => - Simpdata.mksimps Simpdata.mksimps_pairs ctxt #> - map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback})))) + Simpdata.mksimps Simpdata.mksimps_pairs ctxt #> + map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback}))))) \ text \Pre-simplification of induction and cases rules\ @@ -1649,7 +1648,7 @@ signature REORIENT_PROC = sig val add : (term -> bool) -> theory -> theory - val proc : Proof.context -> cterm -> thm option + val proc : Simplifier.proc end; structure Reorient_Proc : REORIENT_PROC = @@ -1933,16 +1932,13 @@ declare eq_equal [symmetric, code_post] declare eq_equal [code] -setup \ - Code_Preproc.map_pre (fn ctxt => - ctxt addsimprocs - [Simplifier.make_simproc \<^context> "equal" - {lhss = [\<^term>\HOL.eq\], - proc = fn _ => fn _ => fn ct => - (case Thm.term_of ct of - Const (_, Type (\<^type_name>\fun\, [Type _, _])) => SOME @{thm eq_equal} - | _ => NONE)}]) -\ +simproc_setup passive equal (HOL.eq) = + \fn _ => fn _ => fn ct => + (case Thm.term_of ct of + Const (_, Type (\<^type_name>\fun\, [Type _, _])) => SOME @{thm eq_equal} + | _ => NONE)\ + +setup \Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs [\<^simproc>\equal\])\ subsubsection \Generic code generator foundation\ diff -r f2e845c3e65c -r f0cb320603cb src/HOL/HOLCF/Domain_Aux.thy --- a/src/HOL/HOLCF/Domain_Aux.thy Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/HOLCF/Domain_Aux.thy Sun Oct 22 19:40:28 2023 +0200 @@ -358,6 +358,8 @@ ML_file \Tools/Domain/domain_take_proofs.ML\ ML_file \Tools/cont_consts.ML\ ML_file \Tools/cont_proc.ML\ +simproc_setup cont ("cont f") = \K ContProc.cont_proc\ + ML_file \Tools/Domain/domain_constructors.ML\ ML_file \Tools/Domain/domain_induction.ML\ diff -r f2e845c3e65c -r f0cb320603cb src/HOL/HOLCF/Tools/cont_proc.ML --- a/src/HOL/HOLCF/Tools/cont_proc.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/HOLCF/Tools/cont_proc.ML Sun Oct 22 19:40:28 2023 +0200 @@ -8,8 +8,7 @@ val cont_thms: term -> thm list val all_cont_thms: term -> thm list val cont_tac: Proof.context -> int -> tactic - val cont_proc: simproc - val setup: theory -> theory + val cont_proc: Simplifier.proc end structure ContProc : CONT_PROC = @@ -115,18 +114,10 @@ cont_tac_of_term (HOLogic.dest_Trueprop t) i) end -local - fun solve_cont ctxt ct = - let - val t = Thm.term_of ct - val tr = Thm.instantiate' [] [SOME (Thm.cterm_of ctxt t)] @{thm Eq_TrueI} - in Option.map fst (Seq.pull (cont_tac ctxt 1 tr)) end -in - val cont_proc = - Simplifier.make_simproc \<^context> "cont_proc" - {lhss = [\<^term>\cont f\], proc = K solve_cont} -end - -val setup = map_theory_simpset (fn ctxt => ctxt addsimprocs [cont_proc]) +fun cont_proc ctxt ct = + let + val t = Thm.term_of ct + val tr = Thm.instantiate' [] [SOME (Thm.cterm_of ctxt t)] @{thm Eq_TrueI} + in Option.map fst (Seq.pull (cont_tac ctxt 1 tr)) end end diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Library/Cancellation/cancel.ML --- a/src/HOL/Library/Cancellation/cancel.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Library/Cancellation/cancel.ML Sun Oct 22 19:40:28 2023 +0200 @@ -35,7 +35,7 @@ signature CANCEL = sig - val proc: Proof.context -> cterm -> thm option + val proc: Simplifier.proc end; functor Cancel_Fun(Data: CANCEL_NUMERALS_DATA): CANCEL = diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Library/Cancellation/cancel_simprocs.ML --- a/src/HOL/Library/Cancellation/cancel_simprocs.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Library/Cancellation/cancel_simprocs.ML Sun Oct 22 19:40:28 2023 +0200 @@ -7,10 +7,10 @@ signature CANCEL_SIMPROCS = sig - val eq_cancel: Proof.context -> cterm -> thm option - val less_cancel: Proof.context -> cterm -> thm option - val less_eq_cancel: Proof.context -> cterm -> thm option - val diff_cancel: Proof.context -> cterm -> thm option + val eq_cancel: Simplifier.proc + val less_cancel: Simplifier.proc + val less_eq_cancel: Simplifier.proc + val diff_cancel: Simplifier.proc end; structure Cancel_Simprocs : CANCEL_SIMPROCS = diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Library/multiset_simprocs.ML --- a/src/HOL/Library/multiset_simprocs.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Library/multiset_simprocs.ML Sun Oct 22 19:40:28 2023 +0200 @@ -7,8 +7,8 @@ signature MULTISET_SIMPROCS = sig - val subset_cancel_msets: Proof.context -> cterm -> thm option - val subseteq_cancel_msets: Proof.context -> cterm -> thm option + val subset_cancel_msets: Simplifier.proc + val subseteq_cancel_msets: Simplifier.proc end; structure Multiset_Simprocs : MULTISET_SIMPROCS = diff -r f2e845c3e65c -r f0cb320603cb src/HOL/List.thy --- a/src/HOL/List.thy Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/List.thy Sun Oct 22 19:40:28 2023 +0200 @@ -557,7 +557,7 @@ signature LIST_TO_SET_COMPREHENSION = sig - val simproc : Proof.context -> cterm -> thm option + val proc: Simplifier.proc end structure List_to_Set_Comprehension : LIST_TO_SET_COMPREHENSION = @@ -717,7 +717,7 @@ in -fun simproc ctxt redex = +fun proc ctxt redex = let fun make_inner_eqs bound_vs Tis eqs t = (case dest_case ctxt t of @@ -774,7 +774,7 @@ \ simproc_setup list_to_set_comprehension ("set xs") = - \K List_to_Set_Comprehension.simproc\ + \K List_to_Set_Comprehension.proc\ code_datatype set coset hide_const (open) coset diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Matrix_LP/Compute_Oracle/compute.ML --- a/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Sun Oct 22 19:40:28 2023 +0200 @@ -339,8 +339,8 @@ fun merge_shyps shyps1 shyps2 = Sorttab.keys (add_shyps shyps2 (add_shyps shyps1 Sorttab.empty)) -val (_, export_oracle) = Context.>>> (Context.map_theory_result - (Thm.add_oracle (\<^binding>\compute\, fn (thy, hyps, shyps, prop) => +val (_, export_oracle) = + Theory.setup_result (Thm.add_oracle (\<^binding>\compute\, fn (thy, hyps, shyps, prop) => let val shyptab = add_shyps shyps Sorttab.empty fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab @@ -355,7 +355,7 @@ else () in Thm.global_cterm_of thy (fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps prop) - end))); + end)); fun export_thm thy hyps shyps prop = let diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Sun Oct 22 19:40:28 2023 +0200 @@ -93,7 +93,7 @@ fun permTs_of (Const (\<^const_name>\Nominal.perm\, T) $ t $ u) = fst (dest_permT T) :: permTs_of u | permTs_of _ = []; -fun perm_simproc' ctxt ct = +fun perm_proc ctxt ct = (case Thm.term_of ct of Const (\<^const_name>\Nominal.perm\, T) $ t $ (u as Const (\<^const_name>\Nominal.perm\, U) $ r $ s) => let @@ -115,9 +115,7 @@ end | _ => NONE); -val perm_simproc = - Simplifier.make_simproc \<^context> "perm_simp" - {lhss = [\<^term>\pi1 \ (pi2 \ x)\], proc = K perm_simproc'}; +val perm_simproc = \<^simproc_setup>\passive perm_simp ("pi1 \ (pi2 \ x)") = \K perm_proc\\; fun projections ctxt rule = Project_Rule.projections ctxt rule @@ -1562,7 +1560,7 @@ resolve_tac ctxt [rec_induct] 1 THEN REPEAT (simp_tac (put_simpset HOL_basic_ss ctxt addsimps flat perm_simps' - addsimprocs [NominalPermeq.perm_simproc_app]) 1 THEN + addsimprocs [NominalPermeq.perm_app_simproc]) 1 THEN (resolve_tac ctxt rec_intrs THEN_ALL_NEW asm_simp_tac (put_simpset HOL_ss ctxt addsimps (fresh_bij @ perm_bij))) 1)))) val ths' = map (fn ((P, Q), th) => @@ -1975,7 +1973,7 @@ [cut_facts_tac [th'] 1, full_simp_tac (put_simpset HOL_ss ctxt addsimps rec_eqns @ pi1_pi2_eqs @ perm_swap - addsimprocs [NominalPermeq.perm_simproc_app]) 1, + addsimprocs [NominalPermeq.perm_app_simproc]) 1, full_simp_tac (put_simpset HOL_ss context'' addsimps (calc_atm @ fresh_prems' @ freshs2' @ perm_fresh_fresh)) 1]) end; @@ -2008,7 +2006,7 @@ (fold_rev (mk_perm []) pi1 rhs', fold_rev (mk_perm []) pi2 lhs'))) (fn _ => simp_tac (put_simpset HOL_ss context'' addsimps pi1_pi2_eqs @ rec_eqns - addsimprocs [NominalPermeq.perm_simproc_app]) 1 THEN + addsimprocs [NominalPermeq.perm_app_simproc]) 1 THEN TRY (simp_tac (put_simpset HOL_ss context'' addsimps (fresh_prems' @ freshs2' @ calc_atm @ perm_fresh_fresh)) 1)); diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Sun Oct 22 19:40:28 2023 +0200 @@ -40,14 +40,16 @@ th RS infer_instantiate ctxt [(#1 (dest_Var (Thm.term_of perm_boolI_pi)), pi)] perm_boolI; fun mk_perm_bool_simproc names = - Simplifier.make_simproc \<^context> "perm_bool" - {lhss = [\<^term>\perm pi x\], + Simplifier.make_simproc \<^context> + {name = "perm_bool", + lhss = [\<^term>\perm pi x\], proc = fn _ => fn _ => fn ct => (case Thm.term_of ct of Const (\<^const_name>\Nominal.perm\, _) $ _ $ t => if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t)) then SOME perm_bool else NONE - | _ => NONE)}; + | _ => NONE), + identifier = []}; fun transp ([] :: _) = [] | transp xs = map hd xs :: transp (map tl xs); @@ -279,7 +281,7 @@ put_simpset HOL_basic_ss ctxt addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms) addsimprocs [mk_perm_bool_simproc [\<^const_name>\Fun.id\], - NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]; + NominalPermeq.perm_app_simproc, NominalPermeq.perm_fun_simproc]; val fresh_bij = Global_Theory.get_thms thy "fresh_bij"; val perm_bij = Global_Theory.get_thms thy "perm_bij"; val fs_atoms = map (fn aT => Global_Theory.get_thm thy @@ -467,7 +469,7 @@ fun cases_eqvt_simpset ctxt = put_simpset HOL_ss ctxt addsimps eqvt_thms @ swap_simps @ perm_pi_simp - addsimprocs [NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]; + addsimprocs [NominalPermeq.perm_app_simproc, NominalPermeq.perm_fun_simproc]; fun simp_fresh_atm ctxt = Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps fresh_atm); @@ -626,7 +628,7 @@ fun eqvt_simpset ctxt = put_simpset HOL_basic_ss ctxt addsimps (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs [mk_perm_bool_simproc names, - NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]; + NominalPermeq.perm_app_simproc, NominalPermeq.perm_fun_simproc]; val ps = map (fst o HOLogic.dest_imp) (HOLogic.dest_conj (HOLogic.dest_Trueprop t)); fun eqvt_tac ctxt pi (intr, vs) st = diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Nominal/nominal_inductive2.ML Sun Oct 22 19:40:28 2023 +0200 @@ -44,14 +44,16 @@ th RS infer_instantiate ctxt [(#1 (dest_Var (Thm.term_of perm_boolI_pi)), pi)] perm_boolI; fun mk_perm_bool_simproc names = - Simplifier.make_simproc \<^context> "perm_bool" - {lhss = [\<^term>\perm pi x\], + Simplifier.make_simproc \<^context> + {name = "perm_bool", + lhss = [\<^term>\perm pi x\], proc = fn _ => fn _ => fn ct => (case Thm.term_of ct of Const (\<^const_name>\Nominal.perm\, _) $ _ $ t => if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t)) then SOME perm_bool else NONE - | _ => NONE)}; + | _ => NONE), + identifier = []}; fun transp ([] :: _) = [] | transp xs = map hd xs :: transp (map tl xs); @@ -298,7 +300,7 @@ put_simpset HOL_basic_ss ctxt addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms) addsimprocs [mk_perm_bool_simproc [\<^const_name>\Fun.id\], - NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]; + NominalPermeq.perm_app_simproc, NominalPermeq.perm_fun_simproc]; val fresh_star_bij = Global_Theory.get_thms thy "fresh_star_bij"; val pt_insts = map (NominalAtoms.pt_inst_of thy) atoms; val at_insts = map (NominalAtoms.at_inst_of thy) atoms; diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Nominal/nominal_permeq.ML --- a/src/HOL/Nominal/nominal_permeq.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Nominal/nominal_permeq.ML Sun Oct 22 19:40:28 2023 +0200 @@ -27,8 +27,8 @@ signature NOMINAL_PERMEQ = sig - val perm_simproc_fun : simproc - val perm_simproc_app : simproc + val perm_fun_simproc : simproc + val perm_app_simproc : simproc val perm_simp_tac : Proof.context -> int -> tactic val perm_extend_simp_tac : Proof.context -> int -> tactic @@ -85,7 +85,7 @@ (* of applications; just adding this rule to the simplifier *) (* would loop; it also needs careful tuning with the simproc *) (* for functions to avoid further possibilities for looping *) -fun perm_simproc_app' ctxt ct = +fun perm_app_proc ctxt ct = let val thy = Proof_Context.theory_of ctxt val redex = Thm.term_of ct @@ -112,12 +112,10 @@ | _ => NONE end -val perm_simproc_app = - Simplifier.make_simproc \<^context> "perm_simproc_app" - {lhss = [\<^term>\Nominal.perm pi x\], proc = K perm_simproc_app'} +val perm_app_simproc = \<^simproc_setup>\passive perm_app ("Nominal.perm pi x") = \K perm_app_proc\\ (* a simproc that deals with permutation instances in front of functions *) -fun perm_simproc_fun' ctxt ct = +fun perm_fun_proc ctxt ct = let val redex = Thm.term_of ct fun applicable_fun t = @@ -134,9 +132,7 @@ | _ => NONE end -val perm_simproc_fun = - Simplifier.make_simproc \<^context> "perm_simproc_fun" - {lhss = [\<^term>\Nominal.perm pi x\], proc = K perm_simproc_fun'} +val perm_fun_simproc = \<^simproc_setup>\passive perm_fun ("Nominal.perm pi x") = \K perm_fun_proc\\ (* function for simplyfying permutations *) (* stac contains the simplifiation tactic that is *) @@ -146,7 +142,7 @@ let val ctxt' = ctxt addsimps (maps (Proof_Context.get_thms ctxt) dyn_thms @ eqvt_thms) - addsimprocs [perm_simproc_fun, perm_simproc_app] + addsimprocs [perm_fun_simproc, perm_app_simproc] |> fold Simplifier.del_cong weak_congs |> fold Simplifier.add_cong strong_congs in @@ -188,7 +184,7 @@ (* generating perm_aux'es for the outermost permutation and then un- *) (* folding the definition *) -fun perm_compose_simproc' ctxt ct = +fun perm_compose_proc ctxt ct = (case Thm.term_of ct of (Const (\<^const_name>\Nominal.perm\, Type (\<^type_name>\fun\, [Type (\<^type_name>\list\, [Type (\<^type_name>\Product_Type.prod\, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const (\<^const_name>\Nominal.perm\, @@ -217,9 +213,7 @@ | _ => NONE); val perm_compose_simproc = - Simplifier.make_simproc \<^context> "perm_compose" - {lhss = [\<^term>\Nominal.perm pi1 (Nominal.perm pi2 t)\], - proc = K perm_compose_simproc'} + \<^simproc_setup>\passive perm_compose ("perm pi1 (perm pi2 t)") = \K perm_compose_proc\\; fun perm_compose_tac ctxt i = ("analysing permutation compositions on the lhs", diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Product_Type.thy Sun Oct 22 19:40:28 2023 +0200 @@ -1303,12 +1303,11 @@ ML_file \Tools/set_comprehension_pointfree.ML\ -setup \ - Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs - [Simplifier.make_simproc \<^context> "set comprehension" - {lhss = [\<^term>\Collect P\], - proc = K Set_Comprehension_Pointfree.code_simproc}]) -\ +simproc_setup passive set_comprehension ("Collect P") = + \K Set_Comprehension_Pointfree.code_proc\ + +setup \Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs [\<^simproc>\set_comprehension\])\ + subsection \Lemmas about disjointness\ diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Statespace/distinct_tree_prover.ML --- a/src/HOL/Statespace/distinct_tree_prover.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Statespace/distinct_tree_prover.ML Sun Oct 22 19:40:28 2023 +0200 @@ -364,14 +364,16 @@ mk_solver "distinctFieldSolver" (distinctTree_tac names); fun distinct_simproc names = - Simplifier.make_simproc \<^context> "DistinctTreeProver.distinct_simproc" - {lhss = [\<^term>\x = y\], + Simplifier.make_simproc \<^context> + {name = "DistinctTreeProver.distinct_simproc", + lhss = [\<^term>\x = y\], proc = fn _ => fn ctxt => fn ct => (case Thm.term_of ct of Const (\<^const_name>\HOL.eq\, _) $ x $ y => Option.map (fn neq => @{thm neq_to_eq_False} OF [neq]) (get_fst_success (neq_x_y ctxt x y) names) - | _ => NONE)}; + | _ => NONE), + identifier = []}; end; diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Statespace/state_fun.ML --- a/src/HOL/Statespace/state_fun.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Statespace/state_fun.ML Sun Oct 22 19:40:28 2023 +0200 @@ -54,9 +54,8 @@ in val lazy_conj_simproc = - Simplifier.make_simproc \<^context> "lazy_conj_simp" - {lhss = [\<^term>\P & Q\], - proc = fn _ => fn ctxt => fn ct => + \<^simproc_setup>\passive lazy_conj_simp ("P & Q") = + \fn _ => fn ctxt => fn ct => (case Thm.term_of ct of Const (\<^const_name>\HOL.conj\,_) $ P $ Q => let @@ -75,7 +74,7 @@ else SOME (conj_cong OF [P_P', Q_Q']) end end - | _ => NONE)}; + | _ => NONE)\\; fun string_eq_simp_tac ctxt = simp_tac (put_simpset HOL_basic_ss ctxt @@ -122,9 +121,8 @@ val _ = Theory.setup (Context.theory_map (Data.put (lookup_ss, ex_lookup_ss, false))); val lookup_simproc = - Simplifier.make_simproc \<^context> "lookup_simp" - {lhss = [\<^term>\lookup d n (update d' c m v s)\], - proc = fn _ => fn ctxt => fn ct => + \<^simproc_setup>\passive lookup_simp ("lookup d n (update d' c m v s)") = + \fn _ => fn ctxt => fn ct => (case Thm.term_of ct of (Const (\<^const_name>\StateFun.lookup\, lT) $ destr $ n $ (s as Const (\<^const_name>\StateFun.update\, uT) $ _ $ _ $ _ $ _ $ _)) => (let @@ -166,8 +164,7 @@ else SOME thm end handle Option.Option => NONE) - | _ => NONE)}; - + | _ => NONE)\\; local @@ -182,9 +179,8 @@ in val update_simproc = - Simplifier.make_simproc \<^context> "update_simp" - {lhss = [\<^term>\update d c n v s\], - proc = fn _ => fn ctxt => fn ct => + \<^simproc_setup>\passive update_simp ("update d c n v s") = + \fn _ => fn ctxt => fn ct => (case Thm.term_of ct of Const (\<^const_name>\StateFun.update\, uT) $ _ $ _ $ _ $ _ $ _ => let @@ -271,7 +267,7 @@ in SOME (Thm.transitive eq1 eq2) end | _ => NONE) end - | _ => NONE)}; + | _ => NONE)\\; end; @@ -287,9 +283,8 @@ in val ex_lookup_eq_simproc = - Simplifier.make_simproc \<^context> "ex_lookup_eq_simproc" - {lhss = [\<^term>\Ex t\], - proc = fn _ => fn ctxt => fn ct => + \<^simproc_setup>\passive ex_lookup_eq ("Ex t") = + \fn _ => fn ctxt => fn ct => let val thy = Proof_Context.theory_of ctxt; val t = Thm.term_of ct; @@ -336,7 +331,7 @@ val thm' = if swap then swap_ex_eq OF [thm] else thm in SOME thm' end handle TERM _ => NONE) | _ => NONE) - end handle Option.Option => NONE}; + end handle Option.Option => NONE\\; end; diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Statespace/state_space.ML Sun Oct 22 19:40:28 2023 +0200 @@ -293,14 +293,13 @@ val distinctNameSolver = mk_solver "distinctNameSolver" distinctTree_tac; val distinct_simproc = - Simplifier.make_simproc \<^context> "StateSpace.distinct_simproc" - {lhss = [\<^term>\x = y\], - proc = fn _ => fn ctxt => fn ct => + \<^simproc_setup>\passive distinct_simproc ("x = y") = + \fn _ => fn ctxt => fn ct => (case Thm.term_of ct of Const (\<^const_name>\HOL.eq\,_) $ (x as Free _) $ (y as Free _) => Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq]) (neq_x_y ctxt x y) - | _ => NONE)}; + | _ => NONE)\\; fun interprete_parent name dist_thm_name parent_expr thy = let diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Sun Oct 22 19:40:28 2023 +0200 @@ -194,8 +194,8 @@ set_inducts = []}} end; -val _ = Theory.setup (Named_Target.theory_map (fn lthy => +val _ = Named_Target.setup (fn lthy => fold (BNF_FP_Def_Sugar.register_fp_sugars (K true) o single o (fn f => f lthy)) - [fp_sugar_of_sum, fp_sugar_of_prod] lthy)); + [fp_sugar_of_sum, fp_sugar_of_prod] lthy); end; diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Sun Oct 22 19:40:28 2023 +0200 @@ -697,11 +697,11 @@ end; -val (_, oracle) = Context.>>> (Context.map_theory_result - (Thm.add_oracle (\<^binding>\cooper\, +val (_, oracle) = + Theory.setup_result (Thm.add_oracle (\<^binding>\cooper\, (fn (ctxt, t) => (Thm.cterm_of ctxt o Logic.mk_equals o apply2 HOLogic.mk_Trueprop) - (t, procedure t))))); + (t, procedure t)))); val comp_ss = simpset_of (put_simpset HOL_ss \<^context> addsimps @{thms semiring_norm}); diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Tools/Quotient/quotient_tacs.ML --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Sun Oct 22 19:40:28 2023 +0200 @@ -148,9 +148,9 @@ map (OF1 eq_imp_rel) (rev (Named_Theorems.get ctxt \<^named_theorems>\quot_equiv\)) val regularize_simproc = - Simplifier.make_simproc \<^context> "regularize" - {lhss = [\<^term>\Ball (Respects (R1 ===> R2)) P\, \<^term>\Bex (Respects (R1 ===> R2)) P\], - proc = K ball_bex_range_simproc}; + \<^simproc_setup>\passive regularize + ("Ball (Respects (R1 ===> R2)) P" | "Bex (Respects (R1 ===> R2)) P") = + \K ball_bex_range_simproc\\ fun regularize_tac ctxt = let diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Tools/SMT/smt_real.ML --- a/src/HOL/Tools/SMT/smt_real.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Tools/SMT/smt_real.ML Sun Oct 22 19:40:28 2023 +0200 @@ -116,10 +116,9 @@ (* Z3 proof replay *) -val real_linarith_proc = - Simplifier.make_simproc \<^context> "fast_real_arith" - {lhss = [\<^term>\(m::real) < n\, \<^term>\(m::real) \ n\, \<^term>\(m::real) = n\], - proc = K Lin_Arith.simproc} +val real_linarith_simproc = + \<^simproc_setup>\passive fast_real_arith ("(m::real) < n" | "(m::real) \ n" | "(m::real) = n") = + \K Lin_Arith.simproc\\; (* 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 f2e845c3e65c -r f0cb320603cb src/HOL/Tools/SMT/smt_replay.ML --- a/src/HOL/Tools/SMT/smt_replay.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Tools/SMT/smt_replay.ML Sun Oct 22 19:40:28 2023 +0200 @@ -140,20 +140,22 @@ end handle THM _ => NONE + val fast_int_arith_simproc = + \<^simproc_setup>\passive fast_int_arith ("(m::int) < n" | "(m::int) \ n" | "(m::int) = n") = + \K Lin_Arith.simproc\\ + + val antisym_le_simproc = + \<^simproc_setup>\passive antisym_le ("(x::'a::order) \ y") = \K prove_antisym_le\\ + + val antisym_less_simproc = + \<^simproc_setup>\passive antisym_less ("\ (x::'a::linorder) < y") = \K prove_antisym_less\\ + 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>\numeral_divmod\, - Simplifier.make_simproc \<^context> "fast_int_arith" - {lhss = [\<^term>\(m::int) < n\, \<^term>\(m::int) \ n\, \<^term>\(m::int) = n\], - proc = K Lin_Arith.simproc}, - Simplifier.make_simproc \<^context> "antisym_le" - {lhss = [\<^term>\(x::'a::order) \ y\], - proc = K prove_antisym_le}, - Simplifier.make_simproc \<^context> "antisym_less" - {lhss = [\<^term>\\ (x::'a::linorder) < y\], - proc = K prove_antisym_less}]) + addsimprocs [\<^simproc>\numeral_divmod\, fast_int_arith_simproc, + antisym_le_simproc, antisym_less_simproc]) structure Simpset = Generic_Data ( diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Tools/SMT/z3_replay_rules.ML --- a/src/HOL/Tools/SMT/z3_replay_rules.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Tools/SMT/z3_replay_rules.ML Sun Oct 22 19:40:28 2023 +0200 @@ -6,7 +6,7 @@ signature Z3_REPLAY_RULES = sig - val apply: Proof.context -> cterm -> thm option + val apply: Simplifier.proc end; structure Z3_Replay_Rules: Z3_REPLAY_RULES = diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Tools/datatype_simprocs.ML --- a/src/HOL/Tools/datatype_simprocs.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Tools/datatype_simprocs.ML Sun Oct 22 19:40:28 2023 +0200 @@ -6,7 +6,7 @@ *) signature DATATYPE_SIMPROCS = sig - val no_proper_subterm_simproc : Proof.context -> cterm -> thm option + val no_proper_subterm_proc : Simplifier.proc end structure Datatype_Simprocs : DATATYPE_SIMPROCS = struct @@ -86,7 +86,7 @@ - support for nested datatypes - replace size-based proof with proper subexpression relation *) -fun no_proper_subterm_simproc ctxt ct = +fun no_proper_subterm_proc ctxt ct = let val (clhs, crhs) = ct |> Thm.dest_comb |> apfst (Thm.dest_comb #> snd) val (lhs, rhs) = apply2 Thm.term_of (clhs, crhs) diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Tools/groebner.ML --- a/src/HOL/Tools/groebner.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Tools/groebner.ML Sun Oct 22 19:40:28 2023 +0200 @@ -779,9 +779,11 @@ let val th = poly_eq_conv ct in if Thm.is_reflexive th then NONE else SOME th end in - Simplifier.cert_simproc (Thm.theory_of_thm idl_sub) "poly_eq_simproc" - {lhss = [Thm.term_of (Thm.lhs_of idl_sub)], - proc = Morphism.entity (fn _ => fn _ => proc)} + Simplifier.cert_simproc (Thm.theory_of_thm idl_sub) + {name = "poly_eq_simproc", + lhss = [Thm.term_of (Thm.lhs_of idl_sub)], + proc = Morphism.entity (fn _ => fn _ => proc), + identifier = []} end; val poly_eq_ss = diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Tools/inductive_set.ML Sun Oct 22 19:40:28 2023 +0200 @@ -38,8 +38,9 @@ val anyt = Free ("t", TFree ("'t", [])); fun strong_ind_simproc tab = - Simplifier.make_simproc \<^context> "strong_ind" - {lhss = [\<^term>\x::'a::{}\], + Simplifier.make_simproc \<^context> + {name = "strong_ind", + lhss = [\<^term>\x::'a::{}\], proc = fn _ => fn ctxt => fn ct => let fun close p t f = @@ -102,7 +103,8 @@ end else NONE | _ => NONE) - end}; + end, + identifier = []}; (* only eta contract terms occurring as arguments of functions satisfying p *) fun eta_contract p = @@ -318,11 +320,13 @@ fun to_pred_simproc rules = let val rules' = map mk_meta_eq rules in - Simplifier.make_simproc \<^context> "to_pred" - {lhss = [anyt], + Simplifier.make_simproc \<^context> + {name = "to_pred", + lhss = [anyt], proc = fn _ => fn ctxt => fn ct => lookup_rule (Proof_Context.theory_of ctxt) - (Thm.prop_of #> Logic.dest_equals) rules' (Thm.term_of ct)} + (Thm.prop_of #> Logic.dest_equals) rules' (Thm.term_of ct), + identifier = []} end; fun to_pred_proc thy rules t = diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Tools/int_arith.ML --- a/src/HOL/Tools/int_arith.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Tools/int_arith.ML Sun Oct 22 19:40:28 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>\0::'a::ring\], - proc = fn _ => fn _ => fn ct => + \<^simproc_setup>\passive zero_to_of_int_zero ("0::'a::ring") = + \fn _ => fn _ => fn ct => let val T = Thm.ctyp_of_cterm ct in if Thm.typ_of T = \<^typ>\int\ then NONE else SOME (Thm.instantiate' [SOME T] [] zeroth) - end}; + end\\; 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>\1::'a::ring_1\], - proc = fn _ => fn _ => fn ct => + \<^simproc_setup>\passive one_to_of_int_one ("1::'a::ring_1") = + \fn _ => fn _ => fn ct => let val T = Thm.ctyp_of_cterm ct in if Thm.typ_of T = \<^typ>\int\ then NONE else SOME (Thm.instantiate' [SOME T] [] oneth) - end}; + end\\; fun check (Const (\<^const_name>\Groups.one\, \<^typ>\int\)) = false | check (Const (\<^const_name>\Groups.one\, _)) = true @@ -63,14 +61,11 @@ |> simpset_of; val zero_one_idom_simproc = - Simplifier.make_simproc \<^context> "zero_one_idom_simproc" - {lhss = - [\<^term>\(x::'a::ring_char_0) = y\, - \<^term>\(x::'a::linordered_idom) < y\, - \<^term>\(x::'a::linordered_idom) \ y\], - proc = fn _ => fn ctxt => fn ct => + \<^simproc_setup>\passive zero_one_idom + ("(x::'a::ring_char_0) = y" | "(u::'b::linordered_idom) < v" | "(u::'b::linordered_idom) \ v") = + \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\\ end; diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Tools/lin_arith.ML Sun Oct 22 19:40:28 2023 +0200 @@ -9,7 +9,7 @@ val pre_tac: Proof.context -> int -> tactic val simple_tac: Proof.context -> int -> tactic val tac: Proof.context -> int -> tactic - val simproc: Proof.context -> cterm -> thm option + val simproc: Simplifier.proc val add_inj_thms: thm list -> Context.generic -> Context.generic val add_lessD: thm -> Context.generic -> Context.generic val add_simps: thm list -> Context.generic -> Context.generic diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Tools/nat_numeral_simprocs.ML --- a/src/HOL/Tools/nat_numeral_simprocs.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML Sun Oct 22 19:40:28 2023 +0200 @@ -5,21 +5,21 @@ signature NAT_NUMERAL_SIMPROCS = sig - val combine_numerals: Proof.context -> cterm -> thm option - val eq_cancel_numerals: Proof.context -> cterm -> thm option - val less_cancel_numerals: Proof.context -> cterm -> thm option - val le_cancel_numerals: Proof.context -> cterm -> thm option - val diff_cancel_numerals: Proof.context -> cterm -> thm option - val eq_cancel_numeral_factor: Proof.context -> cterm -> thm option - val less_cancel_numeral_factor: Proof.context -> cterm -> thm option - val le_cancel_numeral_factor: Proof.context -> cterm -> thm option - val div_cancel_numeral_factor: Proof.context -> cterm -> thm option - val dvd_cancel_numeral_factor: Proof.context -> cterm -> thm option - val eq_cancel_factor: Proof.context -> cterm -> thm option - val less_cancel_factor: Proof.context -> cterm -> thm option - val le_cancel_factor: Proof.context -> cterm -> thm option - val div_cancel_factor: Proof.context -> cterm -> thm option - val dvd_cancel_factor: Proof.context -> cterm -> thm option + val combine_numerals: Simplifier.proc + val eq_cancel_numerals: Simplifier.proc + val less_cancel_numerals: Simplifier.proc + val le_cancel_numerals: Simplifier.proc + val diff_cancel_numerals: Simplifier.proc + val eq_cancel_numeral_factor: Simplifier.proc + val less_cancel_numeral_factor: Simplifier.proc + val le_cancel_numeral_factor: Simplifier.proc + val div_cancel_numeral_factor: Simplifier.proc + val dvd_cancel_numeral_factor: Simplifier.proc + val eq_cancel_factor: Simplifier.proc + val less_cancel_factor: Simplifier.proc + val le_cancel_factor: Simplifier.proc + val div_cancel_factor: Simplifier.proc + val dvd_cancel_factor: Simplifier.proc end; structure Nat_Numeral_Simprocs : NAT_NUMERAL_SIMPROCS = diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Tools/numeral_simprocs.ML --- a/src/HOL/Tools/numeral_simprocs.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Tools/numeral_simprocs.ML Sun Oct 22 19:40:28 2023 +0200 @@ -17,24 +17,24 @@ signature NUMERAL_SIMPROCS = sig val trans_tac: Proof.context -> thm option -> tactic - val assoc_fold: Proof.context -> cterm -> thm option - val combine_numerals: Proof.context -> cterm -> thm option - val eq_cancel_numerals: Proof.context -> cterm -> thm option - val less_cancel_numerals: Proof.context -> cterm -> thm option - val le_cancel_numerals: Proof.context -> cterm -> thm option - val eq_cancel_factor: Proof.context -> cterm -> thm option - val le_cancel_factor: Proof.context -> cterm -> thm option - val less_cancel_factor: Proof.context -> cterm -> thm option - val div_cancel_factor: Proof.context -> cterm -> thm option - val mod_cancel_factor: Proof.context -> cterm -> thm option - val dvd_cancel_factor: Proof.context -> cterm -> thm option - val divide_cancel_factor: Proof.context -> cterm -> thm option - val eq_cancel_numeral_factor: Proof.context -> cterm -> thm option - val less_cancel_numeral_factor: Proof.context -> cterm -> thm option - val le_cancel_numeral_factor: Proof.context -> cterm -> thm option - val div_cancel_numeral_factor: Proof.context -> cterm -> thm option - val divide_cancel_numeral_factor: Proof.context -> cterm -> thm option - val field_combine_numerals: Proof.context -> cterm -> thm option + val assoc_fold: Simplifier.proc + val combine_numerals: Simplifier.proc + val eq_cancel_numerals: Simplifier.proc + val less_cancel_numerals: Simplifier.proc + val le_cancel_numerals: Simplifier.proc + val eq_cancel_factor: Simplifier.proc + val le_cancel_factor: Simplifier.proc + val less_cancel_factor: Simplifier.proc + val div_cancel_factor: Simplifier.proc + val mod_cancel_factor: Simplifier.proc + val dvd_cancel_factor: Simplifier.proc + val divide_cancel_factor: Simplifier.proc + val eq_cancel_numeral_factor: Simplifier.proc + val less_cancel_numeral_factor: Simplifier.proc + val le_cancel_numeral_factor: Simplifier.proc + val div_cancel_numeral_factor: Simplifier.proc + val divide_cancel_numeral_factor: Simplifier.proc + val field_combine_numerals: Simplifier.proc val field_divide_cancel_numeral_factor: simproc val num_ss: simpset val field_comp_conv: Proof.context -> conv @@ -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>\((l::'a::field) * m) / n\, - \<^term>\(l::'a::field) / (m * n)\, - \<^term>\((numeral v)::'a::field) / (numeral w)\, - \<^term>\((numeral v)::'a::field) / (- numeral w)\, - \<^term>\((- numeral v)::'a::field) / (numeral w)\, - \<^term>\((- numeral v)::'a::field) / (- numeral w)\], - proc = K DivideCancelNumeralFactor.proc} + \<^simproc_setup>\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)") = + \K DivideCancelNumeralFactor.proc\\; + +val field_eq_cancel_numeral_factor = + \<^simproc_setup>\passive field_eq_cancel_numeral_factor + ("(l::'a::field) * m = n" | "(l::'a::field) = m * n") = + \K EqCancelNumeralFactor.proc\\; val field_cancel_numeral_factors = - [Simplifier.make_simproc \<^context> "field_eq_cancel_numeral_factor" - {lhss = - [\<^term>\(l::'a::field) * m = n\, - \<^term>\(l::'a::field) = m * n\], - 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>\Orderings.less\,_)$(Const(\<^const_name>\Rings.divide\,_)$_$_)$_ => 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>\(x::'a::field) / y + (w::'a::field) / z\], - proc = K proc} + \<^simproc_setup>\passive add_frac_frac ("(x::'a::field) / y + (w::'a::field) / z") = + \K add_frac_frac_proc\\ val add_frac_num_simproc = - Simplifier.make_simproc \<^context> "add_frac_num_simproc" - {lhss = [\<^term>\(x::'a::field) / y + z\, \<^term>\z + (x::'a::field) / y\], - proc = K proc2} + \<^simproc_setup>\passive add_frac_num ("(x::'a::field) / y + z" | "z + (x::'a::field) / y") = + \K add_frac_num_proc\\ val ord_frac_simproc = - Simplifier.make_simproc \<^context> "ord_frac_simproc" - {lhss = - [\<^term>\(a::'a::{field,ord}) / b < c\, - \<^term>\(a::'a::{field,ord}) / b \ c\, - \<^term>\c < (a::'a::{field,ord}) / b\, - \<^term>\c \ (a::'a::{field,ord}) / b\, - \<^term>\c = (a::'a::{field,ord}) / b\, - \<^term>\(a::'a::{field, ord}) / b = c\], - proc = K proc3} + \<^simproc_setup>\passive ord_frac + ("(a::'a::{field,ord}) / b < c" | + "(a::'a::{field,ord}) / b \ c" | + "c < (a::'a::{field,ord}) / b" | + "c \ (a::'a::{field,ord}) / b" | + "c = (a::'a::{field,ord}) / b" | + "(a::'a::{field, ord}) / b = c") = + \K (K ord_frac_proc)\\ val field_comp_ss = simpset_of diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Tools/record.ML Sun Oct 22 19:40:28 2023 +0200 @@ -1060,64 +1060,62 @@ - If X is a more-selector we have to make sure that S is not in the updated subrecord. *) -val _ = Theory.setup (Named_Target.theory_map (Simplifier.define_simproc \<^binding>\select_update\ - {lhss = [\<^term>\x::'a::{}\], - proc = fn _ => fn ctxt => fn ct => - let - val thy = Proof_Context.theory_of ctxt; - val t = Thm.term_of ct; - in - (case t of - (sel as Const (s, Type (_, [_, rangeS]))) $ - ((upd as Const (u, Type (_, [_, Type (_, [rT, _])]))) $ k $ r) => - if is_selector thy s andalso is_some (get_updates thy u) then - let - val {sel_upd = {updates, ...}, extfields, ...} = Data.get thy; - - fun mk_eq_terms ((upd as Const (u, Type(_, [kT, _]))) $ k $ r) = - (case Symtab.lookup updates u of - NONE => NONE - | SOME u_name => - if u_name = s then - (case mk_eq_terms r of - NONE => - let - val rv = ("r", rT); - val rb = Bound 0; - val (kv, kb) = K_skeleton "k" kT (Bound 1) k; - in SOME (upd $ kb $ rb, kb $ (sel $ rb), [kv, rv]) end - | SOME (trm, trm', vars) => - let - val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k; - in SOME (upd $ kb $ trm, kb $ trm', kv :: vars) end) - else if has_field extfields u_name rangeS orelse - has_field extfields s (domain_type kT) then NONE - else - (case mk_eq_terms r of - SOME (trm, trm', vars) => - let val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k - in SOME (upd $ kb $ trm, trm', kv :: vars) end - | NONE => - let - val rv = ("r", rT); - val rb = Bound 0; - val (kv, kb) = K_skeleton "k" kT (Bound 1) k; - in SOME (upd $ kb $ rb, sel $ rb, [kv, rv]) end)) - | mk_eq_terms _ = NONE; - in - (case mk_eq_terms (upd $ k $ r) of - SOME (trm, trm', vars) => - SOME - (prove_unfold_defs thy [] [] [] - (Logic.list_all (vars, Logic.mk_equals (sel $ trm, trm')))) - | NONE => NONE) - end - else NONE - | _ => NONE) - end})); - -val simproc = - #2 (Simplifier.check_simproc (Context.the_local_context ()) ("select_update", Position.none)); + +fun select_update_proc ctxt ct = + let + val thy = Proof_Context.theory_of ctxt; + val t = Thm.term_of ct; + in + (case t of + (sel as Const (s, Type (_, [_, rangeS]))) $ + ((upd as Const (u, Type (_, [_, Type (_, [rT, _])]))) $ k $ r) => + if is_selector thy s andalso is_some (get_updates thy u) then + let + val {sel_upd = {updates, ...}, extfields, ...} = Data.get thy; + + fun mk_eq_terms ((upd as Const (u, Type(_, [kT, _]))) $ k $ r) = + (case Symtab.lookup updates u of + NONE => NONE + | SOME u_name => + if u_name = s then + (case mk_eq_terms r of + NONE => + let + val rv = ("r", rT); + val rb = Bound 0; + val (kv, kb) = K_skeleton "k" kT (Bound 1) k; + in SOME (upd $ kb $ rb, kb $ (sel $ rb), [kv, rv]) end + | SOME (trm, trm', vars) => + let + val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k; + in SOME (upd $ kb $ trm, kb $ trm', kv :: vars) end) + else if has_field extfields u_name rangeS orelse + has_field extfields s (domain_type kT) then NONE + else + (case mk_eq_terms r of + SOME (trm, trm', vars) => + let val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k + in SOME (upd $ kb $ trm, trm', kv :: vars) end + | NONE => + let + val rv = ("r", rT); + val rb = Bound 0; + val (kv, kb) = K_skeleton "k" kT (Bound 1) k; + in SOME (upd $ kb $ rb, sel $ rb, [kv, rv]) end)) + | mk_eq_terms _ = NONE; + in + (case mk_eq_terms (upd $ k $ r) of + SOME (trm, trm', vars) => + SOME + (prove_unfold_defs thy [] [] [] + (Logic.list_all (vars, Logic.mk_equals (sel $ trm, trm')))) + | NONE => NONE) + end + else NONE + | _ => NONE) + end; + +val simproc = \<^simproc_setup>\select_update ("x::'a::{}") = \K select_update_proc\\ fun get_upd_acc_cong_thm upd acc thy ss = let @@ -1164,127 +1162,125 @@ In both cases "more" updates complicate matters: for this reason we omit considering further updates if doing so would introduce both a more update and an update to a field within it.*) -val _ = Theory.setup (Named_Target.theory_map (Simplifier.define_simproc \<^binding>\update\ - {lhss = [\<^term>\x::'a::{}\], - proc = fn _ => fn ctxt => fn ct => + +fun upd_proc ctxt ct = + let + val thy = Proof_Context.theory_of ctxt; + val t = Thm.term_of ct; + (*We can use more-updators with other updators as long + as none of the other updators go deeper than any more + updator. min here is the depth of the deepest other + updator, max the depth of the shallowest more updator.*) + fun include_depth (dep, true) (min, max) = + if min <= dep + then SOME (min, if dep <= max orelse max = ~1 then dep else max) + else NONE + | include_depth (dep, false) (min, max) = + if dep <= max orelse max = ~1 + then SOME (if min <= dep then dep else min, max) + else NONE; + + fun getupdseq (term as (upd as Const (u, _)) $ f $ tm) min max = + (case get_update_details u thy of + SOME (s, dep, ismore) => + (case include_depth (dep, ismore) (min, max) of + SOME (min', max') => + let val (us, bs, _) = getupdseq tm min' max' + in ((upd, s, f) :: us, bs, fastype_of term) end + | NONE => ([], term, HOLogic.unitT)) + | NONE => ([], term, HOLogic.unitT)) + | getupdseq term _ _ = ([], term, HOLogic.unitT); + + val (upds, base, baseT) = getupdseq t 0 ~1; + val orig_upds = map_index (fn (i, (x, y, z)) => (x, y, z, i)) upds + val upd_ord = rev_order o fast_string_ord o apply2 #2 + val (upds, commuted) = + if not (null orig_upds) andalso Config.get ctxt sort_updates andalso not (sorted upd_ord orig_upds) then + (sort upd_ord orig_upds, true) + else + (orig_upds, false) + + fun is_upd_noop s (Abs (n, T, Const (s', T') $ tm')) tm = + if s = s' andalso null (loose_bnos tm') + andalso subst_bound (HOLogic.unit, tm') = tm + then (true, Abs (n, T, Const (s', T') $ Bound 1)) + else (false, HOLogic.unit) + | is_upd_noop _ _ _ = (false, HOLogic.unit); + + fun get_noop_simps (upd as Const _) (Abs (_, _, (acc as Const _) $ _)) = let - val thy = Proof_Context.theory_of ctxt; - val t = Thm.term_of ct; - (*We can use more-updators with other updators as long - as none of the other updators go deeper than any more - updator. min here is the depth of the deepest other - updator, max the depth of the shallowest more updator.*) - fun include_depth (dep, true) (min, max) = - if min <= dep - then SOME (min, if dep <= max orelse max = ~1 then dep else max) - else NONE - | include_depth (dep, false) (min, max) = - if dep <= max orelse max = ~1 - then SOME (if min <= dep then dep else min, max) - else NONE; - - fun getupdseq (term as (upd as Const (u, _)) $ f $ tm) min max = - (case get_update_details u thy of - SOME (s, dep, ismore) => - (case include_depth (dep, ismore) (min, max) of - SOME (min', max') => - let val (us, bs, _) = getupdseq tm min' max' - in ((upd, s, f) :: us, bs, fastype_of term) end - | NONE => ([], term, HOLogic.unitT)) - | NONE => ([], term, HOLogic.unitT)) - | getupdseq term _ _ = ([], term, HOLogic.unitT); - - val (upds, base, baseT) = getupdseq t 0 ~1; - val orig_upds = map_index (fn (i, (x, y, z)) => (x, y, z, i)) upds - val upd_ord = rev_order o fast_string_ord o apply2 #2 - val (upds, commuted) = - if not (null orig_upds) andalso Config.get ctxt sort_updates andalso not (sorted upd_ord orig_upds) then - (sort upd_ord orig_upds, true) - else - (orig_upds, false) - - fun is_upd_noop s (Abs (n, T, Const (s', T') $ tm')) tm = - if s = s' andalso null (loose_bnos tm') - andalso subst_bound (HOLogic.unit, tm') = tm - then (true, Abs (n, T, Const (s', T') $ Bound 1)) - else (false, HOLogic.unit) - | is_upd_noop _ _ _ = (false, HOLogic.unit); - - fun get_noop_simps (upd as Const _) (Abs (_, _, (acc as Const _) $ _)) = + val ss = get_sel_upd_defs thy; + val uathm = get_upd_acc_cong_thm upd acc thy ss; + in + [Drule.export_without_context (uathm RS updacc_noopE), + Drule.export_without_context (uathm RS updacc_noop_compE)] + end; + + (*If f is constant then (f o g) = f. We know that K_skeleton + only returns constant abstractions thus when we see an + abstraction we can discard inner updates.*) + fun add_upd (f as Abs _) _ = [f] + | add_upd f fs = (f :: fs); + + (*mk_updterm returns + (orig-term-skeleton-update list , simplified-skeleton, + variables, duplicate-updates, simp-flag, noop-simps) + + where duplicate-updates is a table used to pass upward + the list of update functions which can be composed + into an update above them, simp-flag indicates whether + any simplification was achieved, and noop-simps are + used for eliminating case (2) defined above*) + fun mk_updterm ((upd as Const (u, T), s, f, i) :: upds) above term = let - val ss = get_sel_upd_defs thy; - val uathm = get_upd_acc_cong_thm upd acc thy ss; + val (lhs_upds, rhs, vars, dups, simp, noops) = + mk_updterm upds (Symtab.update (u, ()) above) term; + val (fvar, skelf) = + K_skeleton (Long_Name.base_name s) (domain_type T) (Bound (length vars)) f; + val (isnoop, skelf') = is_upd_noop s f term; + val funT = domain_type T; + fun mk_comp_local (f, f') = + Const (\<^const_name>\Fun.comp\, funT --> funT --> funT) $ f $ f'; in - [Drule.export_without_context (uathm RS updacc_noopE), - Drule.export_without_context (uathm RS updacc_noop_compE)] - end; - - (*If f is constant then (f o g) = f. We know that K_skeleton - only returns constant abstractions thus when we see an - abstraction we can discard inner updates.*) - fun add_upd (f as Abs _) _ = [f] - | add_upd f fs = (f :: fs); - - (*mk_updterm returns - (orig-term-skeleton-update list , simplified-skeleton, - variables, duplicate-updates, simp-flag, noop-simps) - - where duplicate-updates is a table used to pass upward - the list of update functions which can be composed - into an update above them, simp-flag indicates whether - any simplification was achieved, and noop-simps are - used for eliminating case (2) defined above*) - fun mk_updterm ((upd as Const (u, T), s, f, i) :: upds) above term = - let - val (lhs_upds, rhs, vars, dups, simp, noops) = - mk_updterm upds (Symtab.update (u, ()) above) term; - val (fvar, skelf) = - K_skeleton (Long_Name.base_name s) (domain_type T) (Bound (length vars)) f; - val (isnoop, skelf') = is_upd_noop s f term; - val funT = domain_type T; - fun mk_comp_local (f, f') = - Const (\<^const_name>\Fun.comp\, funT --> funT --> funT) $ f $ f'; - in - if isnoop then - ((upd $ skelf', i)::lhs_upds, rhs, vars, - Symtab.update (u, []) dups, true, - if Symtab.defined noops u then noops - else Symtab.update (u, get_noop_simps upd skelf') noops) - else if Symtab.defined above u then - ((upd $ skelf, i)::lhs_upds, rhs, fvar :: vars, - Symtab.map_default (u, []) (add_upd skelf) dups, - true, noops) - else - (case Symtab.lookup dups u of - SOME fs => - ((upd $ skelf, i)::lhs_upds, - upd $ foldr1 mk_comp_local (add_upd skelf fs) $ rhs, - fvar :: vars, dups, true, noops) - | NONE => ((upd $ skelf, i)::lhs_upds, upd $ skelf $ rhs, fvar :: vars, dups, simp, noops)) - end - | mk_updterm [] _ _ = - ([], Bound 0, [("r", baseT)], Symtab.empty, false, Symtab.empty) - | mk_updterm us _ _ = raise TERM ("mk_updterm match", map (fn (x, _, _, _) => x) us); - - val (lhs_upds, rhs, vars, _, simp, noops) = mk_updterm upds Symtab.empty base; - val orig_order_lhs_upds = lhs_upds |> sort (rev_order o int_ord o apply2 snd) - val lhs = Bound 0 |> fold (fn (upd, _) => fn s => upd $ s) orig_order_lhs_upds - (* Note that the simplifier works bottom up. So all nested updates are already - normalised, e.g. sorted. 'commuted' thus means that the outermost update has to be - inserted at its place inside the sorted nested updates. The necessary swaps can be - expressed via 'upd_funs' by replicating the outer update at the designated position: *) - val upd_funs = (if commuted then insert_unique_hd upd_ord orig_upds else orig_upds) |> map #1 - val noops' = maps snd (Symtab.dest noops); - in - if simp orelse commuted then - SOME - (prove_unfold_defs thy upd_funs noops' [simproc] - (Logic.list_all (vars, Logic.mk_equals (lhs, rhs)))) - else NONE - end})); - -val upd_simproc = - #2 (Simplifier.check_simproc (Context.the_local_context ()) ("update", Position.none)); + if isnoop then + ((upd $ skelf', i)::lhs_upds, rhs, vars, + Symtab.update (u, []) dups, true, + if Symtab.defined noops u then noops + else Symtab.update (u, get_noop_simps upd skelf') noops) + else if Symtab.defined above u then + ((upd $ skelf, i)::lhs_upds, rhs, fvar :: vars, + Symtab.map_default (u, []) (add_upd skelf) dups, + true, noops) + else + (case Symtab.lookup dups u of + SOME fs => + ((upd $ skelf, i)::lhs_upds, + upd $ foldr1 mk_comp_local (add_upd skelf fs) $ rhs, + fvar :: vars, dups, true, noops) + | NONE => ((upd $ skelf, i)::lhs_upds, upd $ skelf $ rhs, fvar :: vars, dups, simp, noops)) + end + | mk_updterm [] _ _ = + ([], Bound 0, [("r", baseT)], Symtab.empty, false, Symtab.empty) + | mk_updterm us _ _ = raise TERM ("mk_updterm match", map (fn (x, _, _, _) => x) us); + + val (lhs_upds, rhs, vars, _, simp, noops) = mk_updterm upds Symtab.empty base; + val orig_order_lhs_upds = lhs_upds |> sort (rev_order o int_ord o apply2 snd) + val lhs = Bound 0 |> fold (fn (upd, _) => fn s => upd $ s) orig_order_lhs_upds + (* Note that the simplifier works bottom up. So all nested updates are already + normalised, e.g. sorted. 'commuted' thus means that the outermost update has to be + inserted at its place inside the sorted nested updates. The necessary swaps can be + expressed via 'upd_funs' by replicating the outer update at the designated position: *) + val upd_funs = (if commuted then insert_unique_hd upd_ord orig_upds else orig_upds) |> map #1 + val noops' = maps snd (Symtab.dest noops); + in + if simp orelse commuted then + SOME + (prove_unfold_defs thy upd_funs noops' [simproc] + (Logic.list_all (vars, Logic.mk_equals (lhs, rhs)))) + else NONE + end; + +val upd_simproc = \<^simproc_setup>\update ("x::'a::{}") = \K upd_proc\\ end; @@ -1304,21 +1300,18 @@ Complexity: #components * #updates #updates *) -val _ = Theory.setup (Named_Target.theory_map (Simplifier.define_simproc \<^binding>\eq\ - {lhss = [\<^term>\r = s\], - proc = fn _ => fn ctxt => fn ct => - (case Thm.term_of ct of - \<^Const_>\HOL.eq T for _ _\ => - (case rec_id ~1 T of - "" => NONE - | name => - (case get_equalities (Proof_Context.theory_of ctxt) name of - NONE => NONE - | SOME thm => SOME (thm RS @{thm Eq_TrueI}))) - | _ => NONE)})); - -val eq_simproc = - #2 (Simplifier.check_simproc (Context.the_local_context ()) ("eq", Position.none)); +fun eq_proc ctxt ct = + (case Thm.term_of ct of + \<^Const_>\HOL.eq T for _ _\ => + (case rec_id ~1 T of + "" => NONE + | name => + (case get_equalities (Proof_Context.theory_of ctxt) name of + NONE => NONE + | SOME thm => SOME (thm RS @{thm Eq_TrueI}))) + | _ => NONE); + +val eq_simproc = \<^simproc_setup>\eq ("r = s") = \K eq_proc\\; (* split_simproc *) @@ -1329,8 +1322,9 @@ P t = ~1: completely split P t > 0: split up to given bound of record extensions.*) fun split_simproc P = - Simplifier.make_simproc \<^context> "record_split" - {lhss = [\<^term>\x::'a::{}\], + Simplifier.make_simproc \<^context> + {name = "record_split", + lhss = [\<^term>\x::'a::{}\], proc = fn _ => fn ctxt => fn ct => (case Thm.term_of ct of Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ => @@ -1355,52 +1349,48 @@ else NONE end) else NONE - | _ => NONE)}; - -val _ = Theory.setup (Named_Target.theory_map (Simplifier.define_simproc \<^binding>\ex_sel_eq\ - {lhss = [\<^term>\Ex t\], - proc = fn _ => fn ctxt => fn ct => - let - val thy = Proof_Context.theory_of ctxt; - val t = Thm.term_of ct; - fun mkeq (lr, T, (sel, Tsel), x) i = - if is_selector thy sel then - let - val x' = - if not (Term.is_dependent x) - then Free ("x" ^ string_of_int i, range_type Tsel) - else raise TERM ("", [x]); - val sel' = Const (sel, Tsel) $ Bound 0; - val (l, r) = if lr then (sel', x') else (x', sel'); - in \<^Const>\HOL.eq T for l r\ end - else raise TERM ("", [Const (sel, Tsel)]); - - fun dest_sel_eq (\<^Const_>\HOL.eq T\ $ (Const (sel, Tsel) $ Bound 0) $ X) = - (true, T, (sel, Tsel), X) - | dest_sel_eq (\<^Const_>\HOL.eq T\ $ X $ (Const (sel, Tsel) $ Bound 0)) = - (false, T, (sel, Tsel), X) - | dest_sel_eq _ = raise TERM ("", []); - in - (case t of - \<^Const_>\Ex T for \Abs (s, _, t)\\ => - (let - val eq = mkeq (dest_sel_eq t) 0; - val prop = - Logic.list_all ([("r", T)], - Logic.mk_equals (\<^Const>\Ex T for \Abs (s, T, eq)\\, \<^Const>\True\)); - in - SOME (Goal.prove_sorry_global thy [] [] prop - (fn {context = ctxt', ...} => - simp_tac (put_simpset (get_simpset thy) ctxt' - addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1)) - end handle TERM _ => NONE) - | _ => NONE) - end})); - -val ex_sel_eq_simproc = - #2 (Simplifier.check_simproc (Context.the_local_context ()) ("ex_sel_eq", Position.none)); - -val _ = Theory.setup (map_theory_simpset (fn ctxt => ctxt delsimprocs [ex_sel_eq_simproc])); + | _ => NONE), + identifier = []}; + +fun ex_sel_eq_proc ctxt ct = + let + val thy = Proof_Context.theory_of ctxt; + val t = Thm.term_of ct; + fun mkeq (lr, T, (sel, Tsel), x) i = + if is_selector thy sel then + let + val x' = + if not (Term.is_dependent x) + then Free ("x" ^ string_of_int i, range_type Tsel) + else raise TERM ("", [x]); + val sel' = Const (sel, Tsel) $ Bound 0; + val (l, r) = if lr then (sel', x') else (x', sel'); + in \<^Const>\HOL.eq T for l r\ end + else raise TERM ("", [Const (sel, Tsel)]); + + fun dest_sel_eq (\<^Const_>\HOL.eq T\ $ (Const (sel, Tsel) $ Bound 0) $ X) = + (true, T, (sel, Tsel), X) + | dest_sel_eq (\<^Const_>\HOL.eq T\ $ X $ (Const (sel, Tsel) $ Bound 0)) = + (false, T, (sel, Tsel), X) + | dest_sel_eq _ = raise TERM ("", []); + in + (case t of + \<^Const_>\Ex T for \Abs (s, _, t)\\ => + (let + val eq = mkeq (dest_sel_eq t) 0; + val prop = + Logic.list_all ([("r", T)], + Logic.mk_equals (\<^Const>\Ex T for \Abs (s, T, eq)\\, \<^Const>\True\)); + in + SOME (Goal.prove_sorry_global thy [] [] prop + (fn {context = ctxt', ...} => + simp_tac (put_simpset (get_simpset thy) ctxt' + addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1)) + end handle TERM _ => NONE) + | _ => NONE) + end; + +val ex_sel_eq_simproc = \<^simproc_setup>\passive ex_sel_eq ("Ex t") = \K ex_sel_eq_proc\\; (* split_simp_tac *) diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Tools/set_comprehension_pointfree.ML --- a/src/HOL/Tools/set_comprehension_pointfree.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML Sun Oct 22 19:40:28 2023 +0200 @@ -7,9 +7,9 @@ signature SET_COMPREHENSION_POINTFREE = sig - val base_simproc : Proof.context -> cterm -> thm option - val code_simproc : Proof.context -> cterm -> thm option - val simproc : Proof.context -> cterm -> thm option + val base_proc : Simplifier.proc + val code_proc : Simplifier.proc + val proc : Simplifier.proc end structure Set_Comprehension_Pointfree : SET_COMPREHENSION_POINTFREE = @@ -484,7 +484,7 @@ Option.map (export o post o unfold o mk_thm) (rewrite_term t'') end; -fun base_simproc ctxt redex = +fun base_proc ctxt redex = let val set_compr = Thm.term_of redex in @@ -500,7 +500,7 @@ infer_instantiate ctxt [(f, Thm.cterm_of ctxt pred)] arg_cong end; -fun simproc ctxt redex = +fun proc ctxt redex = let val pred $ set_compr = Thm.term_of redex val arg_cong' = instantiate_arg_cong ctxt pred @@ -509,14 +509,14 @@ |> Option.map (fn thm => thm RS arg_cong' RS @{thm eq_reflection}) end; -fun code_simproc ctxt redex = +fun code_proc ctxt redex = let fun unfold_conv thms = Raw_Simplifier.rewrite_cterm (false, false, false) (K (K NONE)) (empty_simpset ctxt addsimps thms) val prep_thm = unfold_conv @{thms eq_equal[symmetric]} redex in - case base_simproc ctxt (Thm.rhs_of prep_thm) of + case base_proc ctxt (Thm.rhs_of prep_thm) of SOME rewr_thm => SOME (transitive_thm OF [transitive_thm OF [prep_thm, rewr_thm], unfold_conv @{thms eq_equal} (Thm.rhs_of rewr_thm)]) | NONE => NONE diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Transcendental.thy Sun Oct 22 19:40:28 2023 +0200 @@ -7352,9 +7352,9 @@ val sqrt' : int option -> int -> int option val nth_root : int option -> int -> int -> int option val nth_root' : int option -> int -> int -> int option -val sqrt_simproc : Proof.context -> cterm -> thm option -val root_simproc : int * int -> Proof.context -> cterm -> thm option -val powr_simproc : int * int -> Proof.context -> cterm -> thm option +val sqrt_proc : Simplifier.proc +val root_proc : int * int -> Simplifier.proc +val powr_proc : int * int -> Simplifier.proc end @@ -7428,7 +7428,7 @@ NONE => NONE | SOME y => if y * y = x then SOME y else NONE -fun sqrt_simproc ctxt ct = +fun sqrt_proc ctxt ct = let val n = ct |> Thm.term_of |> dest_comb |> snd |> dest_comb |> snd |> HOLogic.dest_numeral in @@ -7440,7 +7440,7 @@ end handle TERM _ => NONE -fun root_simproc (threshold1, threshold2) ctxt ct = +fun root_proc (threshold1, threshold2) ctxt ct = let val [n, x] = ct |> Thm.term_of |> strip_comb |> snd |> map (dest_comb #> snd #> HOLogic.dest_numeral) @@ -7455,7 +7455,7 @@ handle TERM _ => NONE | Match => NONE -fun powr_simproc (threshold1, threshold2) ctxt ct = +fun powr_proc (threshold1, threshold2) ctxt ct = let val eq_thm = Conv.try_conv (Conv.rewr_conv @{thm numeral_powr_inverse_eq}) ct val ct = Thm.dest_equals_rhs (Thm.cprop_of eq_thm) @@ -7484,14 +7484,14 @@ end simproc_setup sqrt_numeral ("sqrt (numeral n)") = - \K Root_Numeral_Simproc.sqrt_simproc\ + \K Root_Numeral_Simproc.sqrt_proc\ simproc_setup root_numeral ("root (numeral n) (numeral x)") = - \K (Root_Numeral_Simproc.root_simproc (200, Integer.pow 200 2))\ + \K (Root_Numeral_Simproc.root_proc (200, Integer.pow 200 2))\ simproc_setup powr_divide_numeral ("numeral x powr (m / numeral n :: real)" | "numeral x powr (inverse (numeral n) :: real)") = - \K (Root_Numeral_Simproc.powr_simproc (200, Integer.pow 200 2))\ + \K (Root_Numeral_Simproc.powr_proc (200, Integer.pow 200 2))\ lemma "root 100 1267650600228229401496703205376 = 2" diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Types_To_Sets/local_typedef.ML --- a/src/HOL/Types_To_Sets/local_typedef.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Types_To_Sets/local_typedef.ML Sun Oct 22 19:40:28 2023 +0200 @@ -70,8 +70,9 @@ (** END OF THE CRITICAL CODE **) -val (_, cancel_type_definition_oracle) = Context.>>> (Context.map_theory_result - (Thm.add_oracle (\<^binding>\cancel_type_definition\, cancel_type_definition_cterm))); +val (_, cancel_type_definition_oracle) = + Theory.setup_result + (Thm.add_oracle (\<^binding>\cancel_type_definition\, cancel_type_definition_cterm)); fun cancel_type_definition thm = Drule.implies_elim_list (cancel_type_definition_oracle thm) (map Thm.assume (Thm.chyps_of thm)); diff -r f2e845c3e65c -r f0cb320603cb src/HOL/Types_To_Sets/unoverloading.ML --- a/src/HOL/Types_To_Sets/unoverloading.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/Types_To_Sets/unoverloading.ML Sun Oct 22 19:40:28 2023 +0200 @@ -119,9 +119,9 @@ (** END OF THE CRITICAL CODE **) -val (_, unoverload_oracle) = Context.>>> (Context.map_theory_result - (Thm.add_oracle (\<^binding>\unoverload\, - fn (const, thm) => unoverload_impl const thm))); +val (_, unoverload_oracle) = + Theory.setup_result + (Thm.add_oracle (\<^binding>\unoverload\, fn (const, thm) => unoverload_impl const thm)); fun unoverload const thm = unoverload_oracle (const, thm); diff -r f2e845c3e65c -r f0cb320603cb src/HOL/ex/Sorting_Algorithms_Examples.thy --- a/src/HOL/ex/Sorting_Algorithms_Examples.thy Fri Oct 20 12:25:35 2023 +0200 +++ b/src/HOL/ex/Sorting_Algorithms_Examples.thy Sun Oct 22 19:40:28 2023 +0200 @@ -27,8 +27,7 @@ \<^instantiate>\x = ct and y = \Thm.cterm_of ctxt (term_of_int_list ks)\ in cterm \x \ y\ for x y :: \int list\\; - val (_, sort_oracle) = Context.>>> (Context.map_theory_result - (Thm.add_oracle (\<^binding>\sort\, raw_sort))); + val (_, sort_oracle) = Theory.setup_result (Thm.add_oracle (\<^binding>\sort\, raw_sort)); in diff -r f2e845c3e65c -r f0cb320603cb src/Provers/Arith/cancel_div_mod.ML --- a/src/Provers/Arith/cancel_div_mod.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/Provers/Arith/cancel_div_mod.ML Sun Oct 22 19:40:28 2023 +0200 @@ -27,7 +27,7 @@ signature CANCEL_DIV_MOD = sig - val proc: Proof.context -> cterm -> thm option + val proc: Simplifier.proc end; diff -r f2e845c3e65c -r f0cb320603cb src/Provers/Arith/cancel_numeral_factor.ML --- a/src/Provers/Arith/cancel_numeral_factor.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/Provers/Arith/cancel_numeral_factor.ML Sun Oct 22 19:40:28 2023 +0200 @@ -37,7 +37,7 @@ functor CancelNumeralFactorFun(Data: CANCEL_NUMERAL_FACTOR_DATA): - sig val proc: Proof.context -> cterm -> thm option end = + sig val proc: Simplifier.proc end = struct (*the simplification procedure*) diff -r f2e845c3e65c -r f0cb320603cb src/Provers/Arith/cancel_numerals.ML --- a/src/Provers/Arith/cancel_numerals.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/Provers/Arith/cancel_numerals.ML Sun Oct 22 19:40:28 2023 +0200 @@ -44,7 +44,7 @@ signature CANCEL_NUMERALS = sig - val proc: Proof.context -> cterm -> thm option + val proc: Simplifier.proc end; functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA): CANCEL_NUMERALS = diff -r f2e845c3e65c -r f0cb320603cb src/Provers/Arith/combine_numerals.ML --- a/src/Provers/Arith/combine_numerals.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/Provers/Arith/combine_numerals.ML Sun Oct 22 19:40:28 2023 +0200 @@ -38,7 +38,7 @@ functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA): sig - val proc: Proof.context -> cterm -> thm option + val proc: Simplifier.proc end = struct diff -r f2e845c3e65c -r f0cb320603cb src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Sun Oct 22 19:40:28 2023 +0200 @@ -93,7 +93,7 @@ sig val prems_lin_arith_tac: Proof.context -> int -> tactic val lin_arith_tac: Proof.context -> int -> tactic - val lin_arith_simproc: Proof.context -> cterm -> thm option + val lin_arith_simproc: Simplifier.proc val map_data: ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, lessD: thm list, neqE: thm list, simpset: simpset, diff -r f2e845c3e65c -r f0cb320603cb src/Provers/quantifier1.ML --- a/src/Provers/quantifier1.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/Provers/quantifier1.ML Sun Oct 22 19:40:28 2023 +0200 @@ -65,12 +65,12 @@ signature QUANTIFIER1 = sig - val rearrange_all: Proof.context -> cterm -> thm option - val rearrange_All: Proof.context -> cterm -> thm option - val rearrange_Ball: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option - val rearrange_Ex: Proof.context -> cterm -> thm option - val rearrange_Bex: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option - val rearrange_Collect: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option + val rearrange_all: Simplifier.proc + val rearrange_All: Simplifier.proc + val rearrange_Ball: (Proof.context -> tactic) -> Simplifier.proc + val rearrange_Ex: Simplifier.proc + val rearrange_Bex: (Proof.context -> tactic) -> Simplifier.proc + val rearrange_Collect: (Proof.context -> tactic) -> Simplifier.proc end; functor Quantifier1(Data: QUANTIFIER1_DATA): QUANTIFIER1 = diff -r f2e845c3e65c -r f0cb320603cb src/Pure/General/position.ML --- a/src/Pure/General/position.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/Pure/General/position.ML Sun Oct 22 19:40:28 2023 +0200 @@ -10,6 +10,7 @@ sig eqtype T val ord: T ord + val make0: int -> int -> int -> string -> string -> string -> T val make: Thread_Position.T -> T val dest: T -> Thread_Position.T val line_of: T -> int option @@ -78,6 +79,10 @@ datatype T = Pos of Thread_Position.T; +fun make0 line offset end_offset label file id = + Pos {line = line, offset = offset, end_offset = end_offset, + props = {label = label, file = file, id = id}}; + val make = Pos; fun dest (Pos args) = args; diff -r f2e845c3e65c -r f0cb320603cb src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Sun Oct 22 19:40:28 2023 +0200 @@ -17,8 +17,6 @@ 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 -> - local_theory -> local_theory val qed: Method.text_range option -> Toplevel.transition -> Toplevel.transition val terminal_proof: Method.text_range * Method.text_range option -> Toplevel.transition -> Toplevel.transition @@ -117,10 +115,9 @@ (ML_Lex.read "val " @ ML_Lex.read_range range name @ ML_Lex.read - (" = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (" ^ + (" = snd (Theory.setup_result (Thm.add_oracle (" ^ ML_Syntax.make_binding (name, #1 range) ^ ", ") @ - ML_Lex.read_source source @ - ML_Lex.read "))))") + ML_Lex.read_source source @ ML_Lex.read ")))") |> Context.theory_map; @@ -136,17 +133,6 @@ |> Context.proof_map; -(* simprocs *) - -fun simproc_setup name lhss source = - 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 ^ - ", proc = (") @ ML_Lex.read_source source @ ML_Lex.read ")})") - |> Context.proof_map; - - (* local endings *) fun local_qed m = Toplevel.proof (Proof.local_qed (m, true)); diff -r f2e845c3e65c -r f0cb320603cb src/Pure/Isar/named_target.ML --- a/src/Pure/Isar/named_target.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/Pure/Isar/named_target.ML Sun Oct 22 19:40:28 2023 +0200 @@ -16,6 +16,9 @@ val theory_map: (local_theory -> local_theory) -> theory -> theory val theory_map_result: (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) -> theory -> 'b * theory + val setup: (local_theory -> local_theory) -> unit + val setup_result: (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) -> 'b + val setup_result0: (local_theory -> 'a * local_theory) -> 'a val revoke_reinitializability: local_theory -> local_theory val exit_global_reinitialize: local_theory -> (theory -> local_theory) * theory end; @@ -139,8 +142,12 @@ val theory_init = init [] ""; fun theory_map g = theory_init #> g #> Local_Theory.exit_global; +fun theory_map_result f g = theory_init #> g #> Local_Theory.exit_result_global f; -fun theory_map_result f g = theory_init #> g #> Local_Theory.exit_result_global f; +fun setup g = Context.>> (Context.mapping (theory_map g) g); +fun setup_result f g = + Context.>>> (Context.mapping_result (theory_map_result f g) (g #>> f Morphism.identity)); +fun setup_result0 g = setup_result (K I) g; val revoke_reinitializability = (Data.map o Option.map o apsnd) (K false); diff -r f2e845c3e65c -r f0cb320603cb src/Pure/Isar/parse.ML --- a/src/Pure/Isar/parse.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/Pure/Isar/parse.ML Sun Oct 22 19:40:28 2023 +0200 @@ -123,7 +123,6 @@ val embedded_ml: ML_Lex.token Antiquote.antiquote list parser val read_antiq: Keyword.keywords -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a val read_embedded: Proof.context -> Keyword.keywords -> 'a parser -> Input.source -> 'a - val read_embedded_src: Proof.context -> Keyword.keywords -> 'a parser -> Token.src -> 'a end; structure Parse: PARSE = @@ -533,8 +532,4 @@ | NONE => error ("Bad input" ^ Position.here (Input.pos_of input))) end; -fun read_embedded_src ctxt keywords parse src = - Token.read ctxt embedded_input src - |> read_embedded ctxt keywords parse; - end; diff -r f2e845c3e65c -r f0cb320603cb src/Pure/ML/ml_antiquotation.ML --- a/src/Pure/ML/ml_antiquotation.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/Pure/ML/ml_antiquotation.ML Sun Oct 22 19:40:28 2023 +0200 @@ -70,10 +70,9 @@ (* ML macros *) fun special_form binding parse = - ML_Context.add_antiquotation binding true - (fn _ => fn src => fn ctxt => + ML_Context.add_antiquotation_embedded binding + (fn _ => fn input => fn ctxt => let - val input = Token.read ctxt Parse.embedded_input src; val tokenize = ML_Lex.tokenize_no_range; val tokenize_range = ML_Lex.tokenize_range (Input.range_of input); val eq = tokenize " = "; @@ -97,12 +96,10 @@ in (decl', ctxt') end); fun conditional binding check = - ML_Context.add_antiquotation binding true - (fn _ => fn src => fn ctxt => - let val s = Token.read ctxt Parse.embedded_input src in - if check ctxt then ML_Context.read_antiquotes s ctxt - else (K ([], []), ctxt) - end); + ML_Context.add_antiquotation_embedded binding + (fn _ => fn input => fn ctxt => + if check ctxt then ML_Context.read_antiquotes input ctxt + else (K ([], []), ctxt)); (* basic antiquotations *) diff -r f2e845c3e65c -r f0cb320603cb src/Pure/ML/ml_antiquotations.ML --- a/src/Pure/ML/ml_antiquotations.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/Pure/ML/ml_antiquotations.ML Sun Oct 22 19:40:28 2023 +0200 @@ -229,11 +229,11 @@ fun ml_pair (x, y) = ml_parens (ml_commas [x, y]); fun type_antiquotation binding {function} = - ML_Context.add_antiquotation binding true - (fn range => fn src => fn ctxt => + ML_Context.add_antiquotation_embedded binding + (fn range => fn input => fn ctxt => let - val ((s, type_args), fn_body) = src - |> Parse.read_embedded_src ctxt keywords (parse_name_args -- parse_body function); + val ((s, type_args), fn_body) = input + |> Parse.read_embedded ctxt keywords (parse_name_args -- parse_body function); val pos = Input.pos_of s; val Type (c, Ts) = @@ -264,11 +264,11 @@ in (decl', ctxt2) end); fun const_antiquotation binding {pattern, function} = - ML_Context.add_antiquotation binding true - (fn range => fn src => fn ctxt => + ML_Context.add_antiquotation_embedded binding + (fn range => fn input => fn ctxt => let - val (((s, type_args), term_args), fn_body) = src - |> Parse.read_embedded_src ctxt keywords + val (((s, type_args), term_args), fn_body) = input + |> Parse.read_embedded ctxt keywords (parse_name_args -- parse_for_args -- parse_body function); val Const (c, T) = @@ -400,13 +400,12 @@ (* special form for option type *) val _ = Theory.setup - (ML_Context.add_antiquotation \<^binding>\if_none\ true - (fn _ => fn src => fn ctxt => + (ML_Context.add_antiquotation_embedded \<^binding>\if_none\ + (fn _ => fn input => fn ctxt => let - val s = Token.read ctxt Parse.embedded_input src; val tokenize = ML_Lex.tokenize_no_range; - val (decl, ctxt') = ML_Context.read_antiquotes s ctxt; + val (decl, ctxt') = ML_Context.read_antiquotes input ctxt; fun decl' ctxt'' = let val (ml_env, ml_body) = decl ctxt''; diff -r f2e845c3e65c -r f0cb320603cb src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/Pure/ML/ml_context.ML Sun Oct 22 19:40:28 2023 +0200 @@ -11,8 +11,9 @@ val variant: string -> Proof.context -> string * Proof.context type decl = Proof.context -> ML_Lex.token list * ML_Lex.token list type decls = Proof.context -> (ML_Lex.token list * ML_Lex.token list) list - type antiquotation = Position.range -> Token.src -> Proof.context -> decl * Proof.context - val add_antiquotation: binding -> bool -> antiquotation -> theory -> theory + type 'a antiquotation = Position.range -> 'a -> Proof.context -> decl * Proof.context + val add_antiquotation: binding -> bool -> Token.src antiquotation -> theory -> theory + val add_antiquotation_embedded: binding -> Input.source antiquotation -> theory -> theory val print_antiquotations: bool -> Proof.context -> unit val expand_antiquotes: ML_Lex.token Antiquote.antiquote list -> Proof.context -> decl * Proof.context @@ -62,12 +63,11 @@ type decls = Proof.context -> (ML_Lex.token list * ML_Lex.token list) list; -type antiquotation = - Position.range -> Token.src -> Proof.context -> decl * Proof.context; +type 'a antiquotation = Position.range -> 'a -> Proof.context -> decl * Proof.context; structure Antiquotations = Theory_Data ( - type T = (bool * antiquotation) Name_Space.table; + type T = (bool * Token.src antiquotation) Name_Space.table; val empty : T = Name_Space.empty_table Markup.ML_antiquotationN; fun merge data : T = Name_Space.merge_tables data; ); @@ -81,6 +81,11 @@ thy |> Antiquotations.map (Name_Space.define (Context.Theory thy) true (name, (embedded, antiquotation)) #> #2); +fun add_antiquotation_embedded name antiquotation = + add_antiquotation name true + (fn range => fn src => fn ctxt => + antiquotation range (Token.read ctxt Parse.embedded_input src) ctxt); + fun print_antiquotations verbose ctxt = Pretty.big_list "ML antiquotations:" (map (Pretty.mark_str o #1) (Name_Space.markup_table verbose ctxt (get_antiquotations ctxt))) diff -r f2e845c3e65c -r f0cb320603cb src/Pure/ML/ml_instantiate.ML --- a/src/Pure/ML/ml_instantiate.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/Pure/ML/ml_instantiate.ML Sun Oct 22 19:40:28 2023 +0200 @@ -231,11 +231,11 @@ (command_name "lemma" >> #2) -- parse_schematic -- ML_Thms.embedded_lemma >> prepare_lemma range; val _ = Theory.setup - (ML_Context.add_antiquotation \<^binding>\instantiate\ true - (fn range => fn src => fn ctxt => + (ML_Context.add_antiquotation_embedded \<^binding>\instantiate\ + (fn range => fn input => fn ctxt => let - val (insts, prepare_val) = src - |> Parse.read_embedded_src ctxt (make_keywords ctxt) + val (insts, prepare_val) = input + |> Parse.read_embedded ctxt (make_keywords ctxt) ((parse_insts --| Parse.$$$ "in") -- parse_body range); val (((ml_env, ml_body), decls), ctxt1) = ctxt diff -r f2e845c3e65c -r f0cb320603cb src/Pure/ML/ml_syntax.ML --- a/src/Pure/ML/ml_syntax.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/Pure/ML/ml_syntax.ML Sun Oct 22 19:40:28 2023 +0200 @@ -97,7 +97,11 @@ val print_properties = print_list (print_pair print_string print_string); fun print_position pos = - "Position.of_properties " ^ print_properties (Position.properties_of pos); + let val {line, offset, end_offset, props = {label, file, id}} = Position.dest pos in + space_implode " " + ["Position.make0", print_int line, print_int offset, print_int end_offset, + print_string label, print_string file, print_string id] + end; fun print_range range = "Position.range_of_properties " ^ print_properties (Position.properties_of_range range); diff -r f2e845c3e65c -r f0cb320603cb src/Pure/ML/ml_thms.ML --- a/src/Pure/ML/ml_thms.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/Pure/ML/ml_thms.ML Sun Oct 22 19:40:28 2023 +0200 @@ -8,6 +8,8 @@ sig val the_attributes: Proof.context -> int -> Token.src list val the_thmss: Proof.context -> thm list list + val thm_binding: string -> bool -> thm list -> Proof.context -> + (Proof.context -> string * string) * Proof.context val embedded_lemma: (Proof.context -> thm list * (term list * Proof.context)) parser val get_stored_thms: unit -> thm list val get_stored_thm: unit -> thm @@ -122,8 +124,7 @@ fun ml_store get (name, ths) = let val (_, ths') = - Context.>>> (Context.map_theory_result - (Global_Theory.note_thms "" ((Binding.name name, []), [(ths, [])]))); + Theory.setup_result (Global_Theory.note_thms "" ((Binding.name name, []), [(ths, [])])); val _ = Theory.setup (Data.put ths'); val _ = if name = "" then () diff -r f2e845c3e65c -r f0cb320603cb src/Pure/Pure.thy --- a/src/Pure/Pure.thy Fri Oct 20 12:25:35 2023 +0200 +++ b/src/Pure/Pure.thy Sun Oct 22 19:40:28 2023 +0200 @@ -7,8 +7,8 @@ theory Pure keywords "!!" "!" "+" ":" ";" "<" "<=" "==" "=>" "?" "[" "\" "\" "\" "\" "\" - "\" "]" "binder" "by" "in" "infix" "infixl" "infixr" "is" "open" "output" - "overloaded" "pervasive" "premises" "structure" "unchecked" + "\" "]" "binder" "by" "identifier" "in" "infix" "infixl" "infixr" "is" "open" "output" + "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 @@ -333,9 +333,7 @@ val _ = Outer_Syntax.local_theory \<^command_keyword>\simproc_setup\ "define simproc in ML" - (Parse.name_position -- - (\<^keyword>\(\ |-- Parse.enum1 "|" Parse.term --| \<^keyword>\)\ --| \<^keyword>\=\) -- - Parse.ML_source >> (fn ((a, b), c) => Isar_Cmd.simproc_setup a b c)); + Simplifier.simproc_setup_command; in end\ diff -r f2e845c3e65c -r f0cb320603cb src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/Pure/ROOT.ML Sun Oct 22 19:40:28 2023 +0200 @@ -277,6 +277,7 @@ ML_file "Isar/class_declaration.ML"; ML_file "Isar/target_context.ML"; ML_file "Isar/experiment.ML"; +ML_file "ML/ml_thms.ML"; ML_file "simplifier.ML"; ML_file "Tools/plugin.ML"; @@ -327,7 +328,6 @@ (*ML add-ons*) ML_file "ML/ml_pp.ML"; -ML_file "ML/ml_thms.ML"; ML_file "ML/ml_instantiate.ML"; ML_file "ML/ml_file.ML"; ML_file "ML/ml_pid.ML"; diff -r f2e845c3e65c -r f0cb320603cb src/Pure/Tools/plugin.ML --- a/src/Pure/Tools/plugin.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/Pure/Tools/plugin.ML Sun Oct 22 19:40:28 2023 +0200 @@ -57,13 +57,13 @@ val thy' = Data.put data' thy; in (name, thy') end; -fun define_setup binding rhs = Context.>>> (Context.map_theory_result (define binding rhs)); +fun define_setup binding rhs = Theory.setup_result (define binding rhs); (* immediate entries *) fun declare binding thy = define binding [] thy; -fun declare_setup binding = Context.>>> (Context.map_theory_result (declare binding)); +fun declare_setup binding = Theory.setup_result (declare binding); (* filter *) diff -r f2e845c3e65c -r f0cb320603cb src/Pure/drule.ML --- a/src/Pure/drule.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/Pure/drule.ML Sun Oct 22 19:40:28 2023 +0200 @@ -337,10 +337,10 @@ val read_prop = certify o Simple_Syntax.read_prop; fun store_thm name th = - Context.>>> (Context.map_theory_result (Global_Theory.store_thm (name, th))); + Theory.setup_result (Global_Theory.store_thm (name, th)); fun store_thm_open name th = - Context.>>> (Context.map_theory_result (Global_Theory.store_thm_open (name, th))); + Theory.setup_result (Global_Theory.store_thm_open (name, th)); fun store_standard_thm name th = store_thm name (export_without_context th); fun store_standard_thm_open name th = store_thm_open name (export_without_context_open th); diff -r f2e845c3e65c -r f0cb320603cb src/Pure/ex/Def.thy --- a/src/Pure/ex/Def.thy Fri Oct 20 12:25:35 2023 +0200 +++ b/src/Pure/ex/Def.thy Sun Oct 22 19:40:28 2023 +0200 @@ -65,10 +65,7 @@ (* simproc setup *) -val _ = - (Theory.setup o Named_Target.theory_map) - (Simplifier.define_simproc \<^binding>\expand_def\ - {lhss = [Free ("x", TFree ("'a", []))], proc = K get_def}); +val _ = \<^simproc_setup>\expand_def ("x::'a") = \K get_def\\; (* Isar command *) diff -r f2e845c3e65c -r f0cb320603cb src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/Pure/raw_simplifier.ML Sun Oct 22 19:40:28 2023 +0200 @@ -19,7 +19,8 @@ type rrule val mk_rrules: Proof.context -> thm list -> rrule list val eq_rrule: rrule * rrule -> bool - type proc + type proc = Proof.context -> cterm -> thm option + type simproc0 type solver val mk_solver: string -> (Proof.context -> int -> tactic) -> solver type simpset @@ -35,9 +36,8 @@ safe_solvers: string list} val dest_simps: simpset -> thm list type simproc - val eq_simproc: simproc * simproc -> bool - val cert_simproc: theory -> string -> - {lhss: term list, proc: (Proof.context -> cterm -> thm option) Morphism.entity} -> simproc + val cert_simproc: theory -> + {name: string, lhss: term list, proc: proc Morphism.entity, identifier: thm list} -> simproc val transform_simproc: morphism -> simproc -> simproc val trim_context_simproc: simproc -> simproc val simpset_of: Proof.context -> simpset @@ -208,14 +208,17 @@ (* simplification procedures *) -datatype proc = - Proc of +type proc = Proof.context -> cterm -> thm option; + +datatype simproc0 = + Simproc0 of {name: string, lhs: term, - proc: (Proof.context -> cterm -> thm option) Morphism.entity, - stamp: stamp}; + proc: proc Morphism.entity, + id: stamp * thm list}; -fun eq_proc (Proc {stamp = stamp1, ...}, Proc {stamp = stamp2, ...}) = stamp1 = stamp2; +fun eq_simproc0 (Simproc0 {id = (s1, ths1), ...}, Simproc0 {id = (s2, ths2), ...}) = + s1 = s2 andalso eq_list Thm.eq_thm_prop (ths1, ths2); (* solvers *) @@ -257,7 +260,7 @@ prems: thm list, depth: int * bool Unsynchronized.ref} * {congs: thm Congtab.table * cong_name list, - procs: proc Net.net, + procs: simproc0 Net.net, mk_rews: {mk: Proof.context -> thm -> thm list, mk_cong: Proof.context -> thm -> thm, @@ -288,9 +291,8 @@ {simps = Net.entries rules |> map (fn {name, thm, ...} => (name, thm)), procs = Net.entries procs - |> map (fn Proc {name, lhs, stamp, ...} => ((name, lhs), stamp)) - |> partition_eq (eq_snd op =) - |> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps)), + |> partition_eq eq_simproc0 + |> map (fn ps as Simproc0 {name, ...} :: _ => (name, map (fn Simproc0 {lhs, ...} => lhs) ps)), congs = congs |> fst |> Congtab.dest, weak_congs = congs |> snd, loopers = map fst loop_tacs, @@ -336,7 +338,7 @@ 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_proc (procs1, procs2); + val procs' = Net.merge eq_simproc0 (procs1, procs2); 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); @@ -715,52 +717,54 @@ Simproc of {name: string, lhss: term list, - proc: (Proof.context -> cterm -> thm option) Morphism.entity, - stamp: stamp}; - -fun eq_simproc (Simproc {stamp = stamp1, ...}, Simproc {stamp = stamp2, ...}) = stamp1 = stamp2; + proc: proc Morphism.entity, + id: stamp * thm list}; -fun cert_simproc thy name {lhss, proc} = - Simproc {name = name, lhss = map (Sign.cert_term thy) lhss, proc = proc, stamp = stamp ()}; +fun cert_simproc thy {name, lhss, proc, identifier} = + Simproc + {name = name, + lhss = map (Sign.cert_term thy) lhss, + proc = proc, + id = (stamp (), map (Thm.transfer thy) identifier)}; -fun transform_simproc phi (Simproc {name, lhss, proc, stamp}) = +fun transform_simproc phi (Simproc {name, lhss, proc, id = (stamp, identifier)}) = Simproc {name = name, lhss = map (Morphism.term phi) lhss, proc = Morphism.transform phi proc, - stamp = stamp}; + id = (stamp, Morphism.fact phi identifier)}; -fun trim_context_simproc (Simproc {name, lhss, proc, stamp}) = +fun trim_context_simproc (Simproc {name, lhss, proc, id = (stamp, identifier)}) = Simproc {name = name, lhss = lhss, proc = Morphism.entity_reset_context proc, - stamp = stamp}; + id = (stamp, map Thm.trim_context identifier)}; local -fun add_proc (proc as Proc {name, lhs, ...}) ctxt = +fun add_proc (proc as Simproc0 {name, lhs, ...}) ctxt = (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_proc (lhs, proc) procs, + (congs, Net.insert_term eq_simproc0 (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); ctxt)); -fun del_proc (proc as Proc {name, lhs, ...}) ctxt = +fun del_proc (proc as Simproc0 {name, lhs, ...}) ctxt = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) => - (congs, Net.delete_term eq_proc (lhs, proc) procs, + (congs, Net.delete_term eq_simproc0 (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"); ctxt); -fun prep_procs (Simproc {name, lhss, proc, stamp}) = - lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = proc, stamp = stamp}); +fun prep_procs (Simproc {name, lhss, proc, id}) = + lhss |> map (fn lhs => Simproc0 {name = name, lhs = lhs, proc = proc, id = id}); in @@ -1049,7 +1053,7 @@ in sort rrs ([], []) end; fun proc_rews [] = NONE - | proc_rews (Proc {name, proc, lhs, ...} :: ps) = + | proc_rews (Simproc0 {name, proc, lhs, ...} :: ps) = if Pattern.matches (Proof_Context.theory_of ctxt) (lhs, Thm.term_of t) then (cond_tracing' ctxt simp_debug (fn () => print_term ctxt ("Trying procedure " ^ quote name ^ " on:") eta_t); diff -r f2e845c3e65c -r f0cb320603cb src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/Pure/simplifier.ML Sun Oct 22 19:40:28 2023 +0200 @@ -37,10 +37,17 @@ 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 define_simproc: binding -> term simproc_spec -> local_theory -> local_theory - val define_simproc_cmd: binding -> string simproc_spec -> local_theory -> local_theory + val make_simproc: Proof.context -> + {name: string, lhss: term list, proc: morphism -> proc, identifier: thm list} -> simproc + type ('a, 'b, 'c) simproc_spec = + {passive: bool, name: binding, lhss: 'a list, proc: 'b, identifier: 'c} + val read_simproc_spec: Proof.context -> + (string, 'b, 'c) simproc_spec -> (term, 'b, 'c) simproc_spec + val define_simproc: (term, morphism -> proc, thm list) simproc_spec -> local_theory -> + simproc * local_theory + val simproc_setup: (term, morphism -> proc, thm list) simproc_spec -> simproc + val simproc_setup_cmd: (string, morphism -> proc, thm list) simproc_spec -> simproc + val simproc_setup_command: (local_theory -> local_theory) parser val pretty_simpset: bool -> Proof.context -> Pretty.T val default_mk_sym: Proof.context -> thm -> thm option val prems_of: Proof.context -> thm list @@ -120,42 +127,108 @@ (* define simprocs *) -type 'a simproc_spec = {lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option}; - -fun make_simproc ctxt name {lhss, proc} = +fun make_simproc ctxt {name, lhss, proc, identifier} = let val ctxt' = fold Proof_Context.augment lhss ctxt; val lhss' = Variable.export_terms ctxt' ctxt lhss; in - cert_simproc (Proof_Context.theory_of ctxt) name - {lhss = lhss', proc = Morphism.entity proc} + cert_simproc (Proof_Context.theory_of ctxt) + {name = name, lhss = lhss', proc = Morphism.entity proc, identifier = identifier} end; -local +type ('a, 'b, 'c) simproc_spec = + {passive: bool, name: binding, lhss: 'a list, proc: 'b, identifier: 'c}; -fun def_simproc prep b {lhss, proc} lthy = +fun read_simproc_spec ctxt {passive, name, lhss, proc, identifier} = + let + val lhss' = + Syntax.read_terms ctxt lhss handle ERROR msg => + error (msg ^ Position.here_list (map Syntax.read_input_pos lhss)); + in {passive = passive, name = name, lhss = lhss', proc = proc, identifier = identifier} end; + +fun define_simproc {passive, name, lhss, proc, identifier} lthy = let val simproc0 = - make_simproc lthy (Local_Theory.full_name lthy b) {lhss = prep lthy lhss, proc = proc}; + make_simproc lthy + {name = Local_Theory.full_name lthy name, lhss = lhss, proc = proc, identifier = identifier}; in - lthy |> Local_Theory.declaration {syntax = false, pervasive = false, pos = Binding.pos_of b} + lthy |> Local_Theory.declaration {syntax = false, pervasive = false, pos = Binding.pos_of name} (fn phi => fn context => let - val b' = Morphism.binding phi b; + val name' = Morphism.binding phi name; val simproc' = simproc0 |> transform_simproc phi |> trim_context_simproc; in context - |> Simprocs.map (#2 o Name_Space.define context true (b', simproc')) - |> map_ss (fn ctxt => ctxt addsimprocs [simproc']) + |> Simprocs.map (#2 o Name_Space.define context true (name', simproc')) + |> not passive ? map_ss (fn ctxt => ctxt addsimprocs [simproc']) end) + |> pair simproc0 end; -in + +(* simproc_setup with concrete syntax *) + +val simproc_setup = + Named_Target.setup_result Raw_Simplifier.transform_simproc o define_simproc; + +fun simproc_setup_cmd args = + Named_Target.setup_result Raw_Simplifier.transform_simproc + (fn lthy => lthy |> define_simproc (read_simproc_spec lthy args)); + + +val parse_simproc_spec = + Scan.optional (Parse.$$$ "passive" >> K true) false -- + Parse.binding -- + (Parse.$$$ "(" |-- Parse.enum1 "|" Parse.term --| Parse.$$$ ")") -- + (Parse.$$$ "=" |-- Parse.ML_source) -- + Scan.option ((Parse.position (Parse.$$$ "identifier") >> #2) -- Parse.thms1) + >> (fn ((((a, b), c), d), e) => {passive = a, name = b, lhss = c, proc = d, identifier = e}); + +val _ = Theory.setup + (ML_Context.add_antiquotation_embedded \<^binding>\simproc_setup\ + (fn _ => fn input => fn ctxt => + let + val ml = ML_Lex.tokenize_no_range; + + val {passive, name, lhss, proc, identifier} = input + |> Parse.read_embedded ctxt (Thy_Header.get_keywords' ctxt) parse_simproc_spec + |> read_simproc_spec ctxt; -val define_simproc = def_simproc Syntax.check_terms; -val define_simproc_cmd = def_simproc Syntax.read_terms; + val (decl1, ctxt1) = ML_Context.read_antiquotes proc ctxt; + val (decl2, ctxt2) = + (case identifier of + NONE => (K ("", "[]"), ctxt1) + | SOME (_, thms) => ML_Thms.thm_binding "thms" false (Attrib.eval_thms ctxt1 thms) ctxt1); -end; + fun decl' ctxt' = + let + val (ml_env1, ml_body1) = decl1 ctxt'; + val (ml_env2, ml_body2) = decl2 ctxt' |> apply2 ml; + val ml_body' = + ml "Simplifier.simproc_setup {passive = " @ ml (Bool.toString passive) @ + ml ", name = " @ ml (ML_Syntax.make_binding (Binding.name_of name, Binding.pos_of name)) @ + ml ", lhss = " @ ml (ML_Syntax.print_list ML_Syntax.print_term lhss) @ + ml ", proc = (" @ ml_body1 @ ml ")" @ + ml ", identifier = (" @ ml_body2 @ ml ")}"; + in (ml_env1 @ ml_env2, ml_body') end; + in (decl', ctxt2) end)); + +val simproc_setup_command = + parse_simproc_spec >> (fn {passive, name, lhss, proc, identifier} => + (case identifier of + NONE => + Context.proof_map + (ML_Context.expression (Input.pos_of proc) + (ML_Lex.read + ("Simplifier.simproc_setup_cmd {passive = " ^ Bool.toString passive ^ + ", name = " ^ ML_Syntax.make_binding (Binding.name_of name, Binding.pos_of name) ^ + ", lhss = " ^ ML_Syntax.print_strings lhss ^ + ", proc = (") @ ML_Lex.read_source proc @ ML_Lex.read "), identifier = []}")) + | SOME (pos, _) => + error ("Bad command " ^ Markup.markup Markup.keyword1 "simproc_setup" ^ + " with " ^ Markup.markup Markup.keyword2 "identifier" ^ + ": this is only supported in\nML antiquotation \<^simproc_setup>\...\" ^ Position.here pos))); + (** congruence rule to protect foundational terms of local definitions **) diff -r f2e845c3e65c -r f0cb320603cb src/Pure/skip_proof.ML --- a/src/Pure/skip_proof.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/Pure/skip_proof.ML Sun Oct 22 19:40:28 2023 +0200 @@ -26,8 +26,7 @@ (* oracle setup *) val (_, make_thm_cterm) = - Context.>>> - (Context.map_theory_result (Thm.add_oracle (Binding.make ("skip_proof", \<^here>), I))); + Theory.setup_result (Thm.add_oracle (Binding.make ("skip_proof", \<^here>), I)); fun make_thm thy prop = make_thm_cterm (Thm.global_cterm_of thy prop); diff -r f2e845c3e65c -r f0cb320603cb src/Pure/theory.ML --- a/src/Pure/theory.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/Pure/theory.ML Sun Oct 22 19:40:28 2023 +0200 @@ -10,7 +10,9 @@ val ancestors_of: theory -> theory list val nodes_of: theory -> theory list val setup: (theory -> theory) -> unit + val setup_result: (theory -> 'a * theory) -> 'a val local_setup: (Proof.context -> Proof.context) -> unit + val local_setup_result: (Proof.context -> 'a * Proof.context) -> 'a val install_pure: theory -> unit val get_pure: unit -> theory val get_pure_bootstrap: unit -> theory @@ -49,7 +51,10 @@ fun nodes_of thy = thy :: ancestors_of thy; fun setup f = Context.>> (Context.map_theory f); +fun setup_result f = Context.>>> (Context.map_theory_result f); + fun local_setup f = Context.>> (Context.map_proof f); +fun local_setup_result f = Context.>>> (Context.map_proof_result f); (* implicit theory Pure *) diff -r f2e845c3e65c -r f0cb320603cb src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/Tools/Code/code_runtime.ML Sun Oct 22 19:40:28 2023 +0200 @@ -152,9 +152,9 @@ Thm.mk_binop iff ct (if result then \<^cprop>\PROP Code_Generator.holds\ else ct) end; -val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result - (Thm.add_oracle (\<^binding>\holds_by_evaluation\, - fn (ctxt, evaluator, vs_t, ct) => check_holds ctxt evaluator vs_t ct))); +val (_, raw_check_holds_oracle) = + Theory.setup_result (Thm.add_oracle (\<^binding>\holds_by_evaluation\, + fn (ctxt, evaluator, vs_t, ct) => check_holds ctxt evaluator vs_t ct)); fun check_holds_oracle ctxt evaluator vs_ty_t ct = raw_check_holds_oracle (ctxt, evaluator, vs_ty_t, ct); @@ -417,8 +417,7 @@ fun holds ct = Thm.mk_binop \<^cterm>\Pure.eq :: prop \ prop \ prop\ ct \<^cprop>\PROP Code_Generator.holds\; -val (_, holds_oracle) = Context.>>> (Context.map_theory_result - (Thm.add_oracle (\<^binding>\holds\, holds))); +val (_, holds_oracle) = Theory.setup_result (Thm.add_oracle (\<^binding>\holds\, holds)); in diff -r f2e845c3e65c -r f0cb320603cb src/Tools/induct.ML --- a/src/Tools/induct.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/Tools/induct.ML Sun Oct 22 19:40:28 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>\Pure.all (t :: 'a::{} \ prop)\], - proc = fn _ => fn ctxt => fn ct => mk_swap_rrule ctxt ct}; + \<^simproc_setup>\passive rearrange_eqs ("Pure.all (t :: 'a::{} \ prop)") = \K mk_swap_rrule\\; (* rotate k premises to the left by j, skipping over first j premises *) diff -r f2e845c3e65c -r f0cb320603cb src/Tools/nbe.ML --- a/src/Tools/nbe.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/Tools/nbe.ML Sun Oct 22 19:40:28 2023 +0200 @@ -78,9 +78,9 @@ val get_triv_classes = map fst o Triv_Class_Data.get; -val (_, triv_of_class) = Context.>>> (Context.map_theory_result - (Thm.add_oracle (\<^binding>\triv_of_class\, fn (thy, T, class) => - Thm.global_cterm_of thy (Logic.mk_of_class (T, class))))); +val (_, triv_of_class) = + Theory.setup_result (Thm.add_oracle (\<^binding>\triv_of_class\, + fn (thy, T, class) => Thm.global_cterm_of thy (Logic.mk_of_class (T, class)))); in @@ -592,10 +592,10 @@ val rhs = Thm.cterm_of ctxt raw_rhs; in Thm.mk_binop eq lhs rhs end; -val (_, raw_oracle) = Context.>>> (Context.map_theory_result - (Thm.add_oracle (\<^binding>\normalization_by_evaluation\, +val (_, raw_oracle) = + Theory.setup_result (Thm.add_oracle (\<^binding>\normalization_by_evaluation\, fn (nbe_program_idx_tab, ctxt, vs_ty_t, deps, ct) => - mk_equals ctxt ct (normalize_term nbe_program_idx_tab ctxt (Thm.term_of ct) vs_ty_t deps)))); + mk_equals ctxt ct (normalize_term nbe_program_idx_tab ctxt (Thm.term_of ct) vs_ty_t deps))); fun oracle nbe_program_idx_tab ctxt vs_ty_t deps ct = raw_oracle (nbe_program_idx_tab, ctxt, vs_ty_t, deps, ct); diff -r f2e845c3e65c -r f0cb320603cb src/ZF/ArithSimp.thy --- a/src/ZF/ArithSimp.thy Fri Oct 20 12:25:35 2023 +0200 +++ b/src/ZF/ArithSimp.thy Sun Oct 22 19:40:28 2023 +0200 @@ -9,10 +9,78 @@ imports Arith begin +subsection \Arithmetic simplification\ + ML_file \~~/src/Provers/Arith/cancel_numerals.ML\ ML_file \~~/src/Provers/Arith/combine_numerals.ML\ ML_file \arith_data.ML\ +simproc_setup nateq_cancel_numerals + ("l #+ m = n" | "l = m #+ n" | "l #* m = n" | "l = m #* n" | "succ(m) = n" | "m = succ(n)") = + \K ArithData.nateq_cancel_numerals_proc\ + +simproc_setup natless_cancel_numerals + ("l #+ m < n" | "l < m #+ n" | "l #* m < n" | "l < m #* n" | "succ(m) < n" | "m < succ(n)") = + \K ArithData.natless_cancel_numerals_proc\ + +simproc_setup natdiff_cancel_numerals + ("(l #+ m) #- n" | "l #- (m #+ n)" | "(l #* m) #- n" | "l #- (m #* n)" | + "succ(m) #- n" | "m #- succ(n)") = + \K ArithData.natdiff_cancel_numerals_proc\ + + +subsubsection \Examples\ + +lemma "x #+ y = x #+ z" apply simp oops +lemma "y #+ x = x #+ z" apply simp oops +lemma "x #+ y #+ z = x #+ z" apply simp oops +lemma "y #+ (z #+ x) = z #+ x" apply simp oops +lemma "x #+ y #+ z = (z #+ y) #+ (x #+ w)" apply simp oops +lemma "x#*y #+ z = (z #+ y) #+ (y#*x #+ w)" apply simp oops + +lemma "x #+ succ(y) = x #+ z" apply simp oops +lemma "x #+ succ(y) = succ(z #+ x)" apply simp oops +lemma "succ(x) #+ succ(y) #+ z = succ(z #+ y) #+ succ(x #+ w)" apply simp oops + +lemma "(x #+ y) #- (x #+ z) = w" apply simp oops +lemma "(y #+ x) #- (x #+ z) = dd" apply simp oops +lemma "(x #+ y #+ z) #- (x #+ z) = dd" apply simp oops +lemma "(y #+ (z #+ x)) #- (z #+ x) = dd" apply simp oops +lemma "(x #+ y #+ z) #- ((z #+ y) #+ (x #+ w)) = dd" apply simp oops +lemma "(x#*y #+ z) #- ((z #+ y) #+ (y#*x #+ w)) = dd" apply simp oops + +(*BAD occurrence of natify*) +lemma "(x #+ succ(y)) #- (x #+ z) = dd" apply simp oops + +lemma "x #* y2 #+ y #* x2 = y #* x2 #+ x #* y2" apply simp oops + +lemma "(x #+ succ(y)) #- (succ(z #+ x)) = dd" apply simp oops +lemma "(succ(x) #+ succ(y) #+ z) #- (succ(z #+ y) #+ succ(x #+ w)) = dd" apply simp oops + +(*use of typing information*) +lemma "x : nat ==> x #+ y = x" apply simp oops +lemma "x : nat --> x #+ y = x" apply simp oops +lemma "x : nat ==> x #+ y < x" apply simp oops +lemma "x : nat ==> x < y#+x" apply simp oops +lemma "x : nat ==> x \ succ(x)" apply simp oops + +(*fails: no typing information isn't visible*) +lemma "x #+ y = x" apply simp? oops + +lemma "x #+ y < x #+ z" apply simp oops +lemma "y #+ x < x #+ z" apply simp oops +lemma "x #+ y #+ z < x #+ z" apply simp oops +lemma "y #+ z #+ x < x #+ z" apply simp oops +lemma "y #+ (z #+ x) < z #+ x" apply simp oops +lemma "x #+ y #+ z < (z #+ y) #+ (x #+ w)" apply simp oops +lemma "x#*y #+ z < (z #+ y) #+ (y#*x #+ w)" apply simp oops + +lemma "x #+ succ(y) < x #+ z" apply simp oops +lemma "x #+ succ(y) < succ(z #+ x)" apply simp oops +lemma "succ(x) #+ succ(y) #+ z < succ(z #+ y) #+ succ(x #+ w)" apply simp oops + +lemma "x #+ succ(y) \ succ(z #+ x)" apply simp oops + subsection\Difference\ diff -r f2e845c3e65c -r f0cb320603cb src/ZF/Bin.thy --- a/src/ZF/Bin.thy Fri Oct 20 12:25:35 2023 +0200 +++ b/src/ZF/Bin.thy Sun Oct 22 19:40:28 2023 +0200 @@ -702,7 +702,26 @@ ML_file \int_arith.ML\ -subsection \examples:\ +simproc_setup inteq_cancel_numerals + ("l $+ m = n" | "l = m $+ n" | "l $- m = n" | "l = m $- n" | "l $* m = n" | "l = m $* n") = + \K Int_Numeral_Simprocs.inteq_cancel_numerals_proc\ + +simproc_setup intless_cancel_numerals + ("l $+ m $< n" | "l $< m $+ n" | "l $- m $< n" | "l $< m $- n" | "l $* m $< n" | "l $< m $* n") = + \K Int_Numeral_Simprocs.intless_cancel_numerals_proc\ + +simproc_setup intle_cancel_numerals + ("l $+ m $\ n" | "l $\ m $+ n" | "l $- m $\ n" | "l $\ m $- n" | "l $* m $\ n" | "l $\ m $* n") = + \K Int_Numeral_Simprocs.intle_cancel_numerals_proc\ + +simproc_setup int_combine_numerals ("i $+ j" | "i $- j") = + \K Int_Numeral_Simprocs.int_combine_numerals_proc\ + +simproc_setup int_combine_numerals_prod ("i $* j") = + \K Int_Numeral_Simprocs.int_combine_numerals_prod_proc\ + + +subsubsection \Examples\ text \\combine_numerals_prod\ (products of separate literals)\ lemma "#5 $* x $* #3 = y" apply simp oops diff -r f2e845c3e65c -r f0cb320603cb src/ZF/Datatype.thy --- a/src/ZF/Datatype.thy Fri Oct 20 12:25:35 2023 +0200 +++ b/src/ZF/Datatype.thy Sun Oct 22 19:40:28 2023 +0200 @@ -58,63 +58,63 @@ -(*Simproc for freeness reasoning: compare datatype constructors for equality*) -structure DataFree = +(* Simproc for freeness reasoning: compare datatype constructors for equality *) + +structure Data_Free: +sig + val trace: bool Config.T + val proc: Simplifier.proc +end = struct - val trace = Unsynchronized.ref false; + +val trace = Attrib.setup_config_bool \<^binding>\data_free_trace\ (K false); - fun mk_new ([],[]) = \<^Const>\True\ - | mk_new (largs,rargs) = - Balanced_Tree.make FOLogic.mk_conj +fun mk_new ([],[]) = \<^Const>\True\ + | mk_new (largs,rargs) = + Balanced_Tree.make FOLogic.mk_conj (map FOLogic.mk_eq (ListPair.zip (largs,rargs))); - val datatype_ss = simpset_of \<^context>; +val datatype_ss = simpset_of \<^context>; - fun proc ctxt ct = - let val old = Thm.term_of ct - val thy = Proof_Context.theory_of ctxt - val _ = - if !trace then writeln ("data_free: OLD = " ^ Syntax.string_of_term ctxt old) - else () - val (lhs,rhs) = FOLogic.dest_eq old - val (lhead, largs) = strip_comb lhs - and (rhead, rargs) = strip_comb rhs - val lname = #1 (dest_Const lhead) handle TERM _ => raise Match; - val rname = #1 (dest_Const rhead) handle TERM _ => raise Match; - val lcon_info = the (Symtab.lookup (ConstructorsData.get thy) lname) - handle Option.Option => raise Match; - val rcon_info = the (Symtab.lookup (ConstructorsData.get thy) rname) - handle Option.Option => raise Match; - val new = - if #big_rec_name lcon_info = #big_rec_name rcon_info - andalso not (null (#free_iffs lcon_info)) then - if lname = rname then mk_new (largs, rargs) - else \<^Const>\False\ - else raise Match - val _ = - if !trace then writeln ("NEW = " ^ Syntax.string_of_term ctxt new) - else (); - val goal = Logic.mk_equals (old, new) - val thm = Goal.prove ctxt [] [] goal - (fn _ => resolve_tac ctxt @{thms iff_reflection} 1 THEN - simp_tac (put_simpset datatype_ss ctxt addsimps - (map (Thm.transfer thy) (#free_iffs lcon_info))) 1) - handle ERROR msg => - (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Syntax.string_of_term ctxt goal); - raise Match) - in SOME thm end - handle Match => NONE; - - - val conv = - Simplifier.make_simproc \<^context> "data_free" - {lhss = [\<^term>\(x::i) = y\], proc = K proc}; +fun proc ctxt ct = + let + val old = Thm.term_of ct + val thy = Proof_Context.theory_of ctxt + val _ = + if Config.get ctxt trace then tracing ("data_free: OLD = " ^ Syntax.string_of_term ctxt old) + else () + val (lhs,rhs) = FOLogic.dest_eq old + val (lhead, largs) = strip_comb lhs + and (rhead, rargs) = strip_comb rhs + val lname = #1 (dest_Const lhead) handle TERM _ => raise Match; + val rname = #1 (dest_Const rhead) handle TERM _ => raise Match; + val lcon_info = the (Symtab.lookup (ConstructorsData.get thy) lname) + handle Option.Option => raise Match; + val rcon_info = the (Symtab.lookup (ConstructorsData.get thy) rname) + handle Option.Option => raise Match; + val new = + if #big_rec_name lcon_info = #big_rec_name rcon_info + andalso not (null (#free_iffs lcon_info)) then + if lname = rname then mk_new (largs, rargs) + else \<^Const>\False\ + else raise Match; + val _ = + if Config.get ctxt trace then tracing ("NEW = " ^ Syntax.string_of_term ctxt new) + else (); + val goal = Logic.mk_equals (old, new); + val thm = Goal.prove ctxt [] [] goal + (fn _ => resolve_tac ctxt @{thms iff_reflection} 1 THEN + simp_tac (put_simpset datatype_ss ctxt addsimps + (map (Thm.transfer thy) (#free_iffs lcon_info))) 1) + handle ERROR msg => + (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Syntax.string_of_term ctxt goal); + raise Match) + in SOME thm end + handle Match => NONE; end; \ -setup \ - Simplifier.map_theory_simpset (fn ctxt => ctxt addsimprocs [DataFree.conv]) -\ +simproc_setup data_free ("(x::i) = y") = \fn _ => Data_Free.proc\ end diff -r f2e845c3e65c -r f0cb320603cb src/ZF/arith_data.ML --- a/src/ZF/arith_data.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/ZF/arith_data.ML Sun Oct 22 19:40:28 2023 +0200 @@ -7,7 +7,9 @@ signature ARITH_DATA = sig (*the main outcome*) - val nat_cancel: simproc list + val nateq_cancel_numerals_proc: Simplifier.proc + val natless_cancel_numerals_proc: Simplifier.proc + val natdiff_cancel_numerals_proc: Simplifier.proc (*tools for use in similar applications*) val gen_trans_tac: Proof.context -> thm -> thm option -> tactic val prove_conv: string -> tactic list -> Proof.context -> thm list -> term * term -> thm option @@ -184,87 +186,8 @@ structure DiffCancelNumerals = CancelNumeralsFun(DiffCancelNumeralsData); - -val nat_cancel = - [Simplifier.make_simproc \<^context> "nateq_cancel_numerals" - {lhss = - [\<^term>\l #+ m = n\, \<^term>\l = m #+ n\, - \<^term>\l #* m = n\, \<^term>\l = m #* n\, - \<^term>\succ(m) = n\, \<^term>\m = succ(n)\], - proc = K EqCancelNumerals.proc}, - Simplifier.make_simproc \<^context> "natless_cancel_numerals" - {lhss = - [\<^term>\l #+ m < n\, \<^term>\l < m #+ n\, - \<^term>\l #* m < n\, \<^term>\l < m #* n\, - \<^term>\succ(m) < n\, \<^term>\m < succ(n)\], - proc = K LessCancelNumerals.proc}, - Simplifier.make_simproc \<^context> "natdiff_cancel_numerals" - {lhss = - [\<^term>\(l #+ m) #- n\, \<^term>\l #- (m #+ n)\, - \<^term>\(l #* m) #- n\, \<^term>\l #- (m #* n)\, - \<^term>\succ(m) #- n\, \<^term>\m #- succ(n)\], - proc = K DiffCancelNumerals.proc}]; +val nateq_cancel_numerals_proc = EqCancelNumerals.proc; +val natless_cancel_numerals_proc = LessCancelNumerals.proc; +val natdiff_cancel_numerals_proc = DiffCancelNumerals.proc; end; - -val _ = - Theory.setup (Simplifier.map_theory_simpset (fn ctxt => - ctxt addsimprocs ArithData.nat_cancel)); - - -(*examples: -print_depth 22; -set timing; -set simp_trace; -fun test s = (Goal s; by (Asm_simp_tac 1)); - -test "x #+ y = x #+ z"; -test "y #+ x = x #+ z"; -test "x #+ y #+ z = x #+ z"; -test "y #+ (z #+ x) = z #+ x"; -test "x #+ y #+ z = (z #+ y) #+ (x #+ w)"; -test "x#*y #+ z = (z #+ y) #+ (y#*x #+ w)"; - -test "x #+ succ(y) = x #+ z"; -test "x #+ succ(y) = succ(z #+ x)"; -test "succ(x) #+ succ(y) #+ z = succ(z #+ y) #+ succ(x #+ w)"; - -test "(x #+ y) #- (x #+ z) = w"; -test "(y #+ x) #- (x #+ z) = dd"; -test "(x #+ y #+ z) #- (x #+ z) = dd"; -test "(y #+ (z #+ x)) #- (z #+ x) = dd"; -test "(x #+ y #+ z) #- ((z #+ y) #+ (x #+ w)) = dd"; -test "(x#*y #+ z) #- ((z #+ y) #+ (y#*x #+ w)) = dd"; - -(*BAD occurrence of natify*) -test "(x #+ succ(y)) #- (x #+ z) = dd"; - -test "x #* y2 #+ y #* x2 = y #* x2 #+ x #* y2"; - -test "(x #+ succ(y)) #- (succ(z #+ x)) = dd"; -test "(succ(x) #+ succ(y) #+ z) #- (succ(z #+ y) #+ succ(x #+ w)) = dd"; - -(*use of typing information*) -test "x : nat ==> x #+ y = x"; -test "x : nat --> x #+ y = x"; -test "x : nat ==> x #+ y < x"; -test "x : nat ==> x < y#+x"; -test "x : nat ==> x le succ(x)"; - -(*fails: no typing information isn't visible*) -test "x #+ y = x"; - -test "x #+ y < x #+ z"; -test "y #+ x < x #+ z"; -test "x #+ y #+ z < x #+ z"; -test "y #+ z #+ x < x #+ z"; -test "y #+ (z #+ x) < z #+ x"; -test "x #+ y #+ z < (z #+ y) #+ (x #+ w)"; -test "x#*y #+ z < (z #+ y) #+ (y#*x #+ w)"; - -test "x #+ succ(y) < x #+ z"; -test "x #+ succ(y) < succ(z #+ x)"; -test "succ(x) #+ succ(y) #+ z < succ(z #+ y) #+ succ(x #+ w)"; - -test "x #+ succ(y) le succ(z #+ x)"; -*) diff -r f2e845c3e65c -r f0cb320603cb src/ZF/int_arith.ML --- a/src/ZF/int_arith.ML Fri Oct 20 12:25:35 2023 +0200 +++ b/src/ZF/int_arith.ML Sun Oct 22 19:40:28 2023 +0200 @@ -6,9 +6,11 @@ signature INT_NUMERAL_SIMPROCS = sig - val cancel_numerals: simproc list - val combine_numerals: simproc - val combine_numerals_prod: simproc + val inteq_cancel_numerals_proc: Simplifier.proc + val intless_cancel_numerals_proc: Simplifier.proc + val intle_cancel_numerals_proc: Simplifier.proc + val int_combine_numerals_proc: Simplifier.proc + val int_combine_numerals_prod_proc: Simplifier.proc end structure Int_Numeral_Simprocs: INT_NUMERAL_SIMPROCS = @@ -50,7 +52,7 @@ fun find_first_numeral past (t::terms) = ((dest_numeral t, rev past @ terms) handle TERM _ => find_first_numeral (t::past) terms) - | find_first_numeral past [] = raise TERM("find_first_numeral", []); + | find_first_numeral _ [] = raise TERM("find_first_numeral", []); val zero = mk_numeral 0; fun mk_plus (t, u) = \<^Const>\zadd for t u\; @@ -99,7 +101,7 @@ in (sign*n, mk_prod ts') end; (*Find first coefficient-term THAT MATCHES u*) -fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) +fun find_first_coeff _ _ [] = raise TERM("find_first_coeff", []) | find_first_coeff past u (t::terms) = let val (n,u') = dest_coeff 1 t in if u aconv u' then (n, rev past @ terms) @@ -204,25 +206,9 @@ val bal_add2 = @{thm le_add_iff2} RS @{thm iff_trans} ); -val cancel_numerals = - [Simplifier.make_simproc \<^context> "inteq_cancel_numerals" - {lhss = - [\<^term>\l $+ m = n\, \<^term>\l = m $+ n\, - \<^term>\l $- m = n\, \<^term>\l = m $- n\, - \<^term>\l $* m = n\, \<^term>\l = m $* n\], - proc = K EqCancelNumerals.proc}, - Simplifier.make_simproc \<^context> "intless_cancel_numerals" - {lhss = - [\<^term>\l $+ m $< n\, \<^term>\l $< m $+ n\, - \<^term>\l $- m $< n\, \<^term>\l $< m $- n\, - \<^term>\l $* m $< n\, \<^term>\l $< m $* n\], - proc = K LessCancelNumerals.proc}, - Simplifier.make_simproc \<^context> "intle_cancel_numerals" - {lhss = - [\<^term>\l $+ m $\ n\, \<^term>\l $\ m $+ n\, - \<^term>\l $- m $\ n\, \<^term>\l $\ m $- n\, - \<^term>\l $* m $\ n\, \<^term>\l $\ m $* n\], - proc = K LeCancelNumerals.proc}]; +val inteq_cancel_numerals_proc = EqCancelNumerals.proc; +val intless_cancel_numerals_proc = LessCancelNumerals.proc; +val intle_cancel_numerals_proc = LeCancelNumerals.proc; (*version without the hyps argument*) @@ -263,11 +249,7 @@ end; structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); - -val combine_numerals = - Simplifier.make_simproc \<^context> "int_combine_numerals" - {lhss = [\<^term>\i $+ j\, \<^term>\i $- j\], - proc = K CombineNumerals.proc}; +val int_combine_numerals_proc = CombineNumerals.proc @@ -310,16 +292,6 @@ structure CombineNumeralsProd = CombineNumeralsFun(CombineNumeralsProdData); - -val combine_numerals_prod = - Simplifier.make_simproc \<^context> "int_combine_numerals_prod" - {lhss = [\<^term>\i $* j\], proc = K CombineNumeralsProd.proc}; +val int_combine_numerals_prod_proc = CombineNumeralsProd.proc; end; - -val _ = - Theory.setup (Simplifier.map_theory_simpset (fn ctxt => - ctxt addsimprocs - (Int_Numeral_Simprocs.cancel_numerals @ - [Int_Numeral_Simprocs.combine_numerals, - Int_Numeral_Simprocs.combine_numerals_prod])));