--- 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>\<open>eq ("r = s") = \<open>K eq_proc\<close>\<close>;
+
+* 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>\<open>...\<close> with 'catch' or 'finally', or
as last resort declare [[ML_catch_all]] within the theory context.
--- 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
--- 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}}
--- 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>\<open>x = ct and y = \<open>if b then \<^cterm>\<open>True\<close> else \<^cterm>\<open>False\<close>\<close>
in cterm \<open>x \<equiv> y\<close> for x y :: bool\<close>;
- val (_, dvd_oracle) = Context.>>> (Context.map_theory_result
- (Thm.add_oracle (\<^binding>\<open>dvd\<close>, raw_dvd)));
+ val (_, dvd_oracle) = Theory.setup_result (Thm.add_oracle (\<^binding>\<open>dvd\<close>, raw_dvd));
in
--- 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 \<open>Simplification procedures \label{sec:simproc}\<close>
text \<open>
- 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>\<open>simplification procedure\<close> or \<^emph>\<open>simproc\<close> is an ML function that produces
+ proven rewrite rules on demand. Simprocs are guarded by multiple \<^emph>\<open>patterns\<close>
+ 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 \<open>t \<equiv>
- u\<close> 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>\<open>internal form\<close>,
- bypassing the automatic preprocessing of object-level equivalences.
+ The successful result of a simproc needs to be a (possibly conditional)
+ rewrite rule \<open>t \<equiv> u\<close> 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>\<open>internal form\<close> of the Pure logic, bypassing the automatic preprocessing
+ of object-level equivalences.
\begin{matharray}{rcl}
@{command_def "simproc_setup"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
+ @{ML_antiquotation_def "simproc_setup"} & : & \<open>ML antiquotation\<close> \\
simproc & : & \<open>attribute\<close> \\
\end{matharray}
\<^rail>\<open>
- @@{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}+)
\<close>
- \<^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>\<open>morphism -> Proof.context -> cterm -> thm option\<close>, where the
- \<^ML_type>\<open>cterm\<close> represents the current redex \<open>r\<close> and the result is supposed
- to be some proven rewrite rule \<open>r \<equiv> r'\<close> (or a generalized version), or \<^ML>\<open>NONE\<close> to indicate failure. The \<^ML_type>\<open>Proof.context\<close> argument holds the
- full context of the current Simplifier invocation. The \<^ML_type>\<open>morphism\<close>
- 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>\<open>morphism -> Proof.context -> cterm -> thm option\<close>,
+ where the \<^ML_type>\<open>cterm\<close> represents the current redex \<open>r\<close> and the result
+ is supposed to be \<^ML>\<open>SOME\<close> proven rewrite rule \<open>r \<equiv> r'\<close> (or a
+ generalized version); \<^ML>\<open>NONE\<close> indicates failure. The
+ \<^ML_type>\<open>Proof.context\<close> argument holds the full context of the current
+ Simplifier invocation.
+
+ The \<^ML_type>\<open>morphism\<close> 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>\<open>in\<close>'' 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>\<open>active\<close>. The keyword \<^theory_text>\<open>passive\<close> avoids that: it merely defines a
+ simproc that can be activated in a different context later on.
- \<^descr> \<open>simproc add: name\<close> and \<open>simproc del: name\<close> 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>\<open>identifier\<close> 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 \<open>[simproc add: name]\<close> and \<open>[simproc del: name]\<close> 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>\<open>passive\<close>.
\<close>
-subsubsection \<open>Example\<close>
+subsubsection \<open>Examples\<close>
text \<open>
The following simplification procedure for @{thm [source = false,
@@ -847,7 +872,22 @@
text \<open>
Since the Simplifier applies simplification procedures frequently, it is
- important to make the failure check in ML reasonably fast.\<close>
+ 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:
+\<close>
+
+locale loc = fixes x y :: 'a assumes eq: "x = y"
+begin
+
+ML \<open>
+ \<^simproc_setup>\<open>proc (x) =
+ \<open>fn phi => fn _ => fn _ => SOME (Morphism.thm phi @{thm eq})\<close>
+ identifier loc_axioms\<close>
+\<close>
+
+end
subsection \<open>Configurable Simplifier strategies \label{sec:simp-strategies}\<close>
--- 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>\<open>tag important\<close> measurable = \<open> Scan.lift (Scan.succeed (METHOD o Measurable.measurable_tac)) \<close>
"measurability prover"
-simproc_setup\<^marker>\<open>tag important\<close> measurable ("A \<in> sets M" | "f \<in> measurable M N") = \<open>K Measurable.simproc\<close>
+simproc_setup\<^marker>\<open>tag important\<close> measurable ("A \<in> sets M" | "f \<in> measurable M N") =
+ \<open>K Measurable.proc\<close>
setup \<open>
Global_Theory.add_thms_dynamic (\<^binding>\<open>measurable\<close>, Measurable.get_all)
--- 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 = _ } =
--- 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 \<open>Tools/datatype_simprocs.ML\<close>
simproc_setup datatype_no_proper_subterm
- ("(x :: 'a :: size) = y") = \<open>K Datatype_Simprocs.no_proper_subterm_simproc\<close>
+ ("(x :: 'a :: size) = y") = \<open>K Datatype_Simprocs.no_proper_subterm_proc\<close>
end
--- 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>\<open>x = ct and y = \<open>Thm.cterm_of ctxt t\<close>
in cterm \<open>x \<equiv> y\<close> for x y :: pol\<close>;
-val (_, raw_pol_oracle) = Context.>>> (Context.map_theory_result
- (Thm.add_oracle (\<^binding>\<open>pnsubstl\<close>, pol)));
+val (_, raw_pol_oracle) = Theory.setup_result (Thm.add_oracle (\<^binding>\<open>pnsubstl\<close>, pol));
fun pol_oracle ctxt ct t = raw_pol_oracle (ctxt, ct, t);
--- 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>\<open>x = ct and y = \<open>Thm.cterm_of ctxt t\<close>
in cterm \<open>x \<equiv> y\<close> for x y :: \<open>pexpr \<times> pexpr \<times> pexpr list\<close>\<close>;
-val (_, raw_fnorm_oracle) = Context.>>> (Context.map_theory_result
- (Thm.add_oracle (\<^binding>\<open>fnorm\<close>, fnorm)));
+val (_, raw_fnorm_oracle) = Theory.setup_result (Thm.add_oracle (\<^binding>\<open>fnorm\<close>, fnorm));
fun fnorm_oracle ctxt ct t = raw_fnorm_oracle (ctxt, ct, t);
--- 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_>\<open>Ex _ for \<open>Abs _\<close>\<close> =>
let
@@ -168,9 +168,7 @@
in
-val reduce_ex_simproc =
- Simplifier.make_simproc \<^context> "reduce_ex_simproc"
- {lhss = [\<^term>\<open>\<exists>x. P x\<close>], proc = K proc};
+val reduce_ex_simproc = \<^simproc_setup>\<open>passive reduce_ex ("\<exists>x. P x") = \<open>K reduce_ex_proc\<close>\<close>;
end;
--- 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)") = \<open>K Set_Comprehension_Pointfree.simproc\<close>
+simproc_setup finite_Collect ("finite (Collect P)") = \<open>K Set_Comprehension_Pointfree.proc\<close>
declare [[simproc del: finite_Collect]]
--- 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 \<open>~~/src/Tools/induction.ML\<close>
+simproc_setup passive swap_induct_false ("induct_false \<Longrightarrow> PROP P \<Longrightarrow> PROP Q") =
+ \<open>fn _ => fn _ => fn ct =>
+ (case Thm.term_of ct of
+ _ $ (P as _ $ \<^Const_>\<open>induct_false\<close>) $ (_ $ Q $ _) =>
+ if P <> Q then SOME Drule.swap_prems_eq else NONE
+ | _ => NONE)\<close>
+
+simproc_setup passive induct_equal_conj_curry ("induct_conj P Q \<Longrightarrow> PROP R") =
+ \<open>fn _ => fn _ => fn ct =>
+ (case Thm.term_of ct of
+ _ $ (_ $ P) $ _ =>
+ let
+ fun is_conj \<^Const_>\<open>induct_conj for P Q\<close> = is_conj P andalso is_conj Q
+ | is_conj \<^Const_>\<open>induct_equal _ for _ _\<close> = true
+ | is_conj \<^Const_>\<open>induct_true\<close> = true
+ | is_conj \<^Const_>\<open>induct_false\<close> = true
+ | is_conj _ = false
+ in if is_conj P then SOME @{thm induct_conj_curry} else NONE end
+ | _ => NONE)\<close>
+
declaration \<open>
- fn _ => Induct.map_simpset (fn ss => ss
- addsimprocs
- [Simplifier.make_simproc \<^context> "swap_induct_false"
- {lhss = [\<^term>\<open>induct_false \<Longrightarrow> PROP P \<Longrightarrow> PROP Q\<close>],
- proc = fn _ => fn _ => fn ct =>
- (case Thm.term_of ct of
- _ $ (P as _ $ \<^Const_>\<open>induct_false\<close>) $ (_ $ Q $ _) =>
- if P <> Q then SOME Drule.swap_prems_eq else NONE
- | _ => NONE)},
- Simplifier.make_simproc \<^context> "induct_equal_conj_curry"
- {lhss = [\<^term>\<open>induct_conj P Q \<Longrightarrow> PROP R\<close>],
- proc = fn _ => fn _ => fn ct =>
- (case Thm.term_of ct of
- _ $ (_ $ P) $ _ =>
- let
- fun is_conj \<^Const_>\<open>induct_conj for P Q\<close> =
- is_conj P andalso is_conj Q
- | is_conj \<^Const_>\<open>induct_equal _ for _ _\<close> = true
- | is_conj \<^Const_>\<open>induct_true\<close> = true
- | is_conj \<^Const_>\<open>induct_false\<close> = 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>\<open>swap_induct_false\<close>, \<^simproc>\<open>induct_equal_conj_curry\<close>]
|> 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})))))
\<close>
text \<open>Pre-simplification of induction and cases rules\<close>
@@ -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 \<open>
- Code_Preproc.map_pre (fn ctxt =>
- ctxt addsimprocs
- [Simplifier.make_simproc \<^context> "equal"
- {lhss = [\<^term>\<open>HOL.eq\<close>],
- proc = fn _ => fn _ => fn ct =>
- (case Thm.term_of ct of
- Const (_, Type (\<^type_name>\<open>fun\<close>, [Type _, _])) => SOME @{thm eq_equal}
- | _ => NONE)}])
-\<close>
+simproc_setup passive equal (HOL.eq) =
+ \<open>fn _ => fn _ => fn ct =>
+ (case Thm.term_of ct of
+ Const (_, Type (\<^type_name>\<open>fun\<close>, [Type _, _])) => SOME @{thm eq_equal}
+ | _ => NONE)\<close>
+
+setup \<open>Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs [\<^simproc>\<open>equal\<close>])\<close>
subsubsection \<open>Generic code generator foundation\<close>
--- 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 \<open>Tools/Domain/domain_take_proofs.ML\<close>
ML_file \<open>Tools/cont_consts.ML\<close>
ML_file \<open>Tools/cont_proc.ML\<close>
+simproc_setup cont ("cont f") = \<open>K ContProc.cont_proc\<close>
+
ML_file \<open>Tools/Domain/domain_constructors.ML\<close>
ML_file \<open>Tools/Domain/domain_induction.ML\<close>
--- 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>\<open>cont f\<close>], 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
--- 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 =
--- 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 =
--- 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 =
--- 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 @@
\<close>
simproc_setup list_to_set_comprehension ("set xs") =
- \<open>K List_to_Set_Comprehension.simproc\<close>
+ \<open>K List_to_Set_Comprehension.proc\<close>
code_datatype set coset
hide_const (open) coset
--- 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>\<open>compute\<close>, fn (thy, hyps, shyps, prop) =>
+val (_, export_oracle) =
+ Theory.setup_result (Thm.add_oracle (\<^binding>\<open>compute\<close>, 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
--- 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>\<open>Nominal.perm\<close>, 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>\<open>Nominal.perm\<close>, T) $ t $ (u as Const (\<^const_name>\<open>Nominal.perm\<close>, U) $ r $ s) =>
let
@@ -115,9 +115,7 @@
end
| _ => NONE);
-val perm_simproc =
- Simplifier.make_simproc \<^context> "perm_simp"
- {lhss = [\<^term>\<open>pi1 \<bullet> (pi2 \<bullet> x)\<close>], proc = K perm_simproc'};
+val perm_simproc = \<^simproc_setup>\<open>passive perm_simp ("pi1 \<bullet> (pi2 \<bullet> x)") = \<open>K perm_proc\<close>\<close>;
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));
--- 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>\<open>perm pi x\<close>],
+ Simplifier.make_simproc \<^context>
+ {name = "perm_bool",
+ lhss = [\<^term>\<open>perm pi x\<close>],
proc = fn _ => fn _ => fn ct =>
(case Thm.term_of ct of
Const (\<^const_name>\<open>Nominal.perm\<close>, _) $ _ $ 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>\<open>Fun.id\<close>],
- 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 =
--- 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>\<open>perm pi x\<close>],
+ Simplifier.make_simproc \<^context>
+ {name = "perm_bool",
+ lhss = [\<^term>\<open>perm pi x\<close>],
proc = fn _ => fn _ => fn ct =>
(case Thm.term_of ct of
Const (\<^const_name>\<open>Nominal.perm\<close>, _) $ _ $ 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>\<open>Fun.id\<close>],
- 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;
--- 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>\<open>Nominal.perm pi x\<close>], proc = K perm_simproc_app'}
+val perm_app_simproc = \<^simproc_setup>\<open>passive perm_app ("Nominal.perm pi x") = \<open>K perm_app_proc\<close>\<close>
(* 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>\<open>Nominal.perm pi x\<close>], proc = K perm_simproc_fun'}
+val perm_fun_simproc = \<^simproc_setup>\<open>passive perm_fun ("Nominal.perm pi x") = \<open>K perm_fun_proc\<close>\<close>
(* 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>\<open>Nominal.perm\<close>, Type (\<^type_name>\<open>fun\<close>, [Type (\<^type_name>\<open>list\<close>,
[Type (\<^type_name>\<open>Product_Type.prod\<close>, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const (\<^const_name>\<open>Nominal.perm\<close>,
@@ -217,9 +213,7 @@
| _ => NONE);
val perm_compose_simproc =
- Simplifier.make_simproc \<^context> "perm_compose"
- {lhss = [\<^term>\<open>Nominal.perm pi1 (Nominal.perm pi2 t)\<close>],
- proc = K perm_compose_simproc'}
+ \<^simproc_setup>\<open>passive perm_compose ("perm pi1 (perm pi2 t)") = \<open>K perm_compose_proc\<close>\<close>;
fun perm_compose_tac ctxt i =
("analysing permutation compositions on the lhs",
--- 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 \<open>Tools/set_comprehension_pointfree.ML\<close>
-setup \<open>
- Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs
- [Simplifier.make_simproc \<^context> "set comprehension"
- {lhss = [\<^term>\<open>Collect P\<close>],
- proc = K Set_Comprehension_Pointfree.code_simproc}])
-\<close>
+simproc_setup passive set_comprehension ("Collect P") =
+ \<open>K Set_Comprehension_Pointfree.code_proc\<close>
+
+setup \<open>Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs [\<^simproc>\<open>set_comprehension\<close>])\<close>
+
subsection \<open>Lemmas about disjointness\<close>
--- 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>\<open>x = y\<close>],
+ Simplifier.make_simproc \<^context>
+ {name = "DistinctTreeProver.distinct_simproc",
+ lhss = [\<^term>\<open>x = y\<close>],
proc = fn _ => fn ctxt => fn ct =>
(case Thm.term_of ct of
Const (\<^const_name>\<open>HOL.eq\<close>, _) $ 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;
--- 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>\<open>P & Q\<close>],
- proc = fn _ => fn ctxt => fn ct =>
+ \<^simproc_setup>\<open>passive lazy_conj_simp ("P & Q") =
+ \<open>fn _ => fn ctxt => fn ct =>
(case Thm.term_of ct of
Const (\<^const_name>\<open>HOL.conj\<close>,_) $ P $ Q =>
let
@@ -75,7 +74,7 @@
else SOME (conj_cong OF [P_P', Q_Q'])
end
end
- | _ => NONE)};
+ | _ => NONE)\<close>\<close>;
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>\<open>lookup d n (update d' c m v s)\<close>],
- proc = fn _ => fn ctxt => fn ct =>
+ \<^simproc_setup>\<open>passive lookup_simp ("lookup d n (update d' c m v s)") =
+ \<open>fn _ => fn ctxt => fn ct =>
(case Thm.term_of ct of (Const (\<^const_name>\<open>StateFun.lookup\<close>, lT) $ destr $ n $
(s as Const (\<^const_name>\<open>StateFun.update\<close>, uT) $ _ $ _ $ _ $ _ $ _)) =>
(let
@@ -166,8 +164,7 @@
else SOME thm
end
handle Option.Option => NONE)
- | _ => NONE)};
-
+ | _ => NONE)\<close>\<close>;
local
@@ -182,9 +179,8 @@
in
val update_simproc =
- Simplifier.make_simproc \<^context> "update_simp"
- {lhss = [\<^term>\<open>update d c n v s\<close>],
- proc = fn _ => fn ctxt => fn ct =>
+ \<^simproc_setup>\<open>passive update_simp ("update d c n v s") =
+ \<open>fn _ => fn ctxt => fn ct =>
(case Thm.term_of ct of
Const (\<^const_name>\<open>StateFun.update\<close>, uT) $ _ $ _ $ _ $ _ $ _ =>
let
@@ -271,7 +267,7 @@
in SOME (Thm.transitive eq1 eq2) end
| _ => NONE)
end
- | _ => NONE)};
+ | _ => NONE)\<close>\<close>;
end;
@@ -287,9 +283,8 @@
in
val ex_lookup_eq_simproc =
- Simplifier.make_simproc \<^context> "ex_lookup_eq_simproc"
- {lhss = [\<^term>\<open>Ex t\<close>],
- proc = fn _ => fn ctxt => fn ct =>
+ \<^simproc_setup>\<open>passive ex_lookup_eq ("Ex t") =
+ \<open>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\<close>\<close>;
end;
--- 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>\<open>x = y\<close>],
- proc = fn _ => fn ctxt => fn ct =>
+ \<^simproc_setup>\<open>passive distinct_simproc ("x = y") =
+ \<open>fn _ => fn ctxt => fn ct =>
(case Thm.term_of ct of
Const (\<^const_name>\<open>HOL.eq\<close>,_) $ (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)\<close>\<close>;
fun interprete_parent name dist_thm_name parent_expr thy =
let
--- 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;
--- 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>\<open>cooper\<close>,
+val (_, oracle) =
+ Theory.setup_result (Thm.add_oracle (\<^binding>\<open>cooper\<close>,
(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});
--- 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>\<open>quot_equiv\<close>))
val regularize_simproc =
- Simplifier.make_simproc \<^context> "regularize"
- {lhss = [\<^term>\<open>Ball (Respects (R1 ===> R2)) P\<close>, \<^term>\<open>Bex (Respects (R1 ===> R2)) P\<close>],
- proc = K ball_bex_range_simproc};
+ \<^simproc_setup>\<open>passive regularize
+ ("Ball (Respects (R1 ===> R2)) P" | "Bex (Respects (R1 ===> R2)) P") =
+ \<open>K ball_bex_range_simproc\<close>\<close>
fun regularize_tac ctxt =
let
--- 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>\<open>(m::real) < n\<close>, \<^term>\<open>(m::real) \<le> n\<close>, \<^term>\<open>(m::real) = n\<close>],
- proc = K Lin_Arith.simproc}
+val real_linarith_simproc =
+ \<^simproc_setup>\<open>passive fast_real_arith ("(m::real) < n" | "(m::real) \<le> n" | "(m::real) = n") =
+ \<open>K Lin_Arith.simproc\<close>\<close>;
(* setup *)
@@ -128,6 +127,6 @@
SMTLIB_Interface.add_logic (10, smtlib_logic) #>
setup_builtins #>
Z3_Interface.add_mk_builtins smt_mk_builtins #>
- SMT_Replay.add_simproc real_linarith_proc))
+ SMT_Replay.add_simproc real_linarith_simproc))
end;
--- 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>\<open>passive fast_int_arith ("(m::int) < n" | "(m::int) \<le> n" | "(m::int) = n") =
+ \<open>K Lin_Arith.simproc\<close>\<close>
+
+ val antisym_le_simproc =
+ \<^simproc_setup>\<open>passive antisym_le ("(x::'a::order) \<le> y") = \<open>K prove_antisym_le\<close>\<close>
+
+ val antisym_less_simproc =
+ \<^simproc_setup>\<open>passive antisym_less ("\<not> (x::'a::linorder) < y") = \<open>K prove_antisym_less\<close>\<close>
+
val basic_simpset =
simpset_of (put_simpset HOL_ss \<^context>
addsimps @{thms field_simps times_divide_eq_right times_divide_eq_left arith_special
arith_simps rel_simps array_rules z3div_def z3mod_def NO_MATCH_def}
- addsimprocs [\<^simproc>\<open>numeral_divmod\<close>,
- Simplifier.make_simproc \<^context> "fast_int_arith"
- {lhss = [\<^term>\<open>(m::int) < n\<close>, \<^term>\<open>(m::int) \<le> n\<close>, \<^term>\<open>(m::int) = n\<close>],
- proc = K Lin_Arith.simproc},
- Simplifier.make_simproc \<^context> "antisym_le"
- {lhss = [\<^term>\<open>(x::'a::order) \<le> y\<close>],
- proc = K prove_antisym_le},
- Simplifier.make_simproc \<^context> "antisym_less"
- {lhss = [\<^term>\<open>\<not> (x::'a::linorder) < y\<close>],
- proc = K prove_antisym_less}])
+ addsimprocs [\<^simproc>\<open>numeral_divmod\<close>, fast_int_arith_simproc,
+ antisym_le_simproc, antisym_less_simproc])
structure Simpset = Generic_Data
(
--- 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 =
--- 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)
--- 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 =
--- 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>\<open>x::'a::{}\<close>],
+ Simplifier.make_simproc \<^context>
+ {name = "strong_ind",
+ lhss = [\<^term>\<open>x::'a::{}\<close>],
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 =
--- 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>\<open>0::'a::ring\<close>],
- proc = fn _ => fn _ => fn ct =>
+ \<^simproc_setup>\<open>passive zero_to_of_int_zero ("0::'a::ring") =
+ \<open>fn _ => fn _ => fn ct =>
let val T = Thm.ctyp_of_cterm ct in
if Thm.typ_of T = \<^typ>\<open>int\<close> then NONE
else SOME (Thm.instantiate' [SOME T] [] zeroth)
- end};
+ end\<close>\<close>;
val oneth = Thm.symmetric (mk_meta_eq @{thm of_int_1});
val one_to_of_int_one_simproc =
- Simplifier.make_simproc \<^context> "one_to_of_int_one_simproc"
- {lhss = [\<^term>\<open>1::'a::ring_1\<close>],
- proc = fn _ => fn _ => fn ct =>
+ \<^simproc_setup>\<open>passive one_to_of_int_one ("1::'a::ring_1") =
+ \<open>fn _ => fn _ => fn ct =>
let val T = Thm.ctyp_of_cterm ct in
if Thm.typ_of T = \<^typ>\<open>int\<close> then NONE
else SOME (Thm.instantiate' [SOME T] [] oneth)
- end};
+ end\<close>\<close>;
fun check (Const (\<^const_name>\<open>Groups.one\<close>, \<^typ>\<open>int\<close>)) = false
| check (Const (\<^const_name>\<open>Groups.one\<close>, _)) = true
@@ -63,14 +61,11 @@
|> simpset_of;
val zero_one_idom_simproc =
- Simplifier.make_simproc \<^context> "zero_one_idom_simproc"
- {lhss =
- [\<^term>\<open>(x::'a::ring_char_0) = y\<close>,
- \<^term>\<open>(x::'a::linordered_idom) < y\<close>,
- \<^term>\<open>(x::'a::linordered_idom) \<le> y\<close>],
- proc = fn _ => fn ctxt => fn ct =>
+ \<^simproc_setup>\<open>passive zero_one_idom
+ ("(x::'a::ring_char_0) = y" | "(u::'b::linordered_idom) < v" | "(u::'b::linordered_idom) \<le> v") =
+ \<open>fn _ => fn ctxt => fn ct =>
if check (Thm.term_of ct)
then SOME (Simplifier.rewrite (put_simpset conv_ss ctxt) ct)
- else NONE};
+ else NONE\<close>\<close>
end;
--- 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
--- 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 =
--- 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>\<open>((l::'a::field) * m) / n\<close>,
- \<^term>\<open>(l::'a::field) / (m * n)\<close>,
- \<^term>\<open>((numeral v)::'a::field) / (numeral w)\<close>,
- \<^term>\<open>((numeral v)::'a::field) / (- numeral w)\<close>,
- \<^term>\<open>((- numeral v)::'a::field) / (numeral w)\<close>,
- \<^term>\<open>((- numeral v)::'a::field) / (- numeral w)\<close>],
- proc = K DivideCancelNumeralFactor.proc}
+ \<^simproc_setup>\<open>passive field_divide_cancel_numeral_factor
+ ("((l::'a::field) * m) / n" | "(l::'a::field) / (m * n)" |
+ "((numeral v)::'a::field) / (numeral w)" |
+ "((numeral v)::'a::field) / (- numeral w)" |
+ "((- numeral v)::'a::field) / (numeral w)" |
+ "((- numeral v)::'a::field) / (- numeral w)") =
+ \<open>K DivideCancelNumeralFactor.proc\<close>\<close>;
+
+val field_eq_cancel_numeral_factor =
+ \<^simproc_setup>\<open>passive field_eq_cancel_numeral_factor
+ ("(l::'a::field) * m = n" | "(l::'a::field) = m * n") =
+ \<open>K EqCancelNumeralFactor.proc\<close>\<close>;
val field_cancel_numeral_factors =
- [Simplifier.make_simproc \<^context> "field_eq_cancel_numeral_factor"
- {lhss =
- [\<^term>\<open>(l::'a::field) * m = n\<close>,
- \<^term>\<open>(l::'a::field) = m * n\<close>],
- proc = K EqCancelNumeralFactor.proc},
- field_divide_cancel_numeral_factor]
+ [field_divide_cancel_numeral_factor, field_eq_cancel_numeral_factor]
(** Declarations for ExtractCommonTerm **)
@@ -599,7 +597,7 @@
(Thm.apply (Thm.apply eq t) z)))
in Thm.equal_elim (Thm.symmetric th) TrueI end
-fun proc ctxt ct =
+fun add_frac_frac_proc ctxt ct =
let
val ((x,y),(w,z)) =
(Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct
@@ -610,7 +608,7 @@
in SOME (Thm.implies_elim (Thm.implies_elim th y_nz) z_nz) end
handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
-fun proc2 ctxt ct =
+fun add_frac_num_proc ctxt ct =
let
val (l,r) = Thm.dest_binop ct
val T = Thm.ctyp_of_cterm l
@@ -636,7 +634,7 @@
val is_number = is_number o Thm.term_of
-fun proc3 ctxt ct =
+fun ord_frac_proc ct =
(case Thm.term_of ct of
Const(\<^const_name>\<open>Orderings.less\<close>,_)$(Const(\<^const_name>\<open>Rings.divide\<close>,_)$_$_)$_ =>
let
@@ -683,25 +681,22 @@
| _ => NONE) handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE
val add_frac_frac_simproc =
- Simplifier.make_simproc \<^context> "add_frac_frac_simproc"
- {lhss = [\<^term>\<open>(x::'a::field) / y + (w::'a::field) / z\<close>],
- proc = K proc}
+ \<^simproc_setup>\<open>passive add_frac_frac ("(x::'a::field) / y + (w::'a::field) / z") =
+ \<open>K add_frac_frac_proc\<close>\<close>
val add_frac_num_simproc =
- Simplifier.make_simproc \<^context> "add_frac_num_simproc"
- {lhss = [\<^term>\<open>(x::'a::field) / y + z\<close>, \<^term>\<open>z + (x::'a::field) / y\<close>],
- proc = K proc2}
+ \<^simproc_setup>\<open>passive add_frac_num ("(x::'a::field) / y + z" | "z + (x::'a::field) / y") =
+ \<open>K add_frac_num_proc\<close>\<close>
val ord_frac_simproc =
- Simplifier.make_simproc \<^context> "ord_frac_simproc"
- {lhss =
- [\<^term>\<open>(a::'a::{field,ord}) / b < c\<close>,
- \<^term>\<open>(a::'a::{field,ord}) / b \<le> c\<close>,
- \<^term>\<open>c < (a::'a::{field,ord}) / b\<close>,
- \<^term>\<open>c \<le> (a::'a::{field,ord}) / b\<close>,
- \<^term>\<open>c = (a::'a::{field,ord}) / b\<close>,
- \<^term>\<open>(a::'a::{field, ord}) / b = c\<close>],
- proc = K proc3}
+ \<^simproc_setup>\<open>passive ord_frac
+ ("(a::'a::{field,ord}) / b < c" |
+ "(a::'a::{field,ord}) / b \<le> c" |
+ "c < (a::'a::{field,ord}) / b" |
+ "c \<le> (a::'a::{field,ord}) / b" |
+ "c = (a::'a::{field,ord}) / b" |
+ "(a::'a::{field, ord}) / b = c") =
+ \<open>K (K ord_frac_proc)\<close>\<close>
val field_comp_ss =
simpset_of
--- 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>\<open>select_update\<close>
- {lhss = [\<^term>\<open>x::'a::{}\<close>],
- 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>\<open>select_update ("x::'a::{}") = \<open>K select_update_proc\<close>\<close>
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>\<open>update\<close>
- {lhss = [\<^term>\<open>x::'a::{}\<close>],
- 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>\<open>Fun.comp\<close>, 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>\<open>Fun.comp\<close>, 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>\<open>update ("x::'a::{}") = \<open>K upd_proc\<close>\<close>
end;
@@ -1304,21 +1300,18 @@
Complexity: #components * #updates #updates
*)
-val _ = Theory.setup (Named_Target.theory_map (Simplifier.define_simproc \<^binding>\<open>eq\<close>
- {lhss = [\<^term>\<open>r = s\<close>],
- proc = fn _ => fn ctxt => fn ct =>
- (case Thm.term_of ct of
- \<^Const_>\<open>HOL.eq T for _ _\<close> =>
- (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_>\<open>HOL.eq T for _ _\<close> =>
+ (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>\<open>eq ("r = s") = \<open>K eq_proc\<close>\<close>;
(* 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>\<open>x::'a::{}\<close>],
+ Simplifier.make_simproc \<^context>
+ {name = "record_split",
+ lhss = [\<^term>\<open>x::'a::{}\<close>],
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>\<open>ex_sel_eq\<close>
- {lhss = [\<^term>\<open>Ex t\<close>],
- 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>\<open>HOL.eq T for l r\<close> end
- else raise TERM ("", [Const (sel, Tsel)]);
-
- fun dest_sel_eq (\<^Const_>\<open>HOL.eq T\<close> $ (Const (sel, Tsel) $ Bound 0) $ X) =
- (true, T, (sel, Tsel), X)
- | dest_sel_eq (\<^Const_>\<open>HOL.eq T\<close> $ X $ (Const (sel, Tsel) $ Bound 0)) =
- (false, T, (sel, Tsel), X)
- | dest_sel_eq _ = raise TERM ("", []);
- in
- (case t of
- \<^Const_>\<open>Ex T for \<open>Abs (s, _, t)\<close>\<close> =>
- (let
- val eq = mkeq (dest_sel_eq t) 0;
- val prop =
- Logic.list_all ([("r", T)],
- Logic.mk_equals (\<^Const>\<open>Ex T for \<open>Abs (s, T, eq)\<close>\<close>, \<^Const>\<open>True\<close>));
- 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>\<open>HOL.eq T for l r\<close> end
+ else raise TERM ("", [Const (sel, Tsel)]);
+
+ fun dest_sel_eq (\<^Const_>\<open>HOL.eq T\<close> $ (Const (sel, Tsel) $ Bound 0) $ X) =
+ (true, T, (sel, Tsel), X)
+ | dest_sel_eq (\<^Const_>\<open>HOL.eq T\<close> $ X $ (Const (sel, Tsel) $ Bound 0)) =
+ (false, T, (sel, Tsel), X)
+ | dest_sel_eq _ = raise TERM ("", []);
+ in
+ (case t of
+ \<^Const_>\<open>Ex T for \<open>Abs (s, _, t)\<close>\<close> =>
+ (let
+ val eq = mkeq (dest_sel_eq t) 0;
+ val prop =
+ Logic.list_all ([("r", T)],
+ Logic.mk_equals (\<^Const>\<open>Ex T for \<open>Abs (s, T, eq)\<close>\<close>, \<^Const>\<open>True\<close>));
+ 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>\<open>passive ex_sel_eq ("Ex t") = \<open>K ex_sel_eq_proc\<close>\<close>;
(* split_simp_tac *)
--- 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
--- 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)") =
- \<open>K Root_Numeral_Simproc.sqrt_simproc\<close>
+ \<open>K Root_Numeral_Simproc.sqrt_proc\<close>
simproc_setup root_numeral ("root (numeral n) (numeral x)") =
- \<open>K (Root_Numeral_Simproc.root_simproc (200, Integer.pow 200 2))\<close>
+ \<open>K (Root_Numeral_Simproc.root_proc (200, Integer.pow 200 2))\<close>
simproc_setup powr_divide_numeral
("numeral x powr (m / numeral n :: real)" | "numeral x powr (inverse (numeral n) :: real)") =
- \<open>K (Root_Numeral_Simproc.powr_simproc (200, Integer.pow 200 2))\<close>
+ \<open>K (Root_Numeral_Simproc.powr_proc (200, Integer.pow 200 2))\<close>
lemma "root 100 1267650600228229401496703205376 = 2"
--- 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>\<open>cancel_type_definition\<close>, cancel_type_definition_cterm)));
+val (_, cancel_type_definition_oracle) =
+ Theory.setup_result
+ (Thm.add_oracle (\<^binding>\<open>cancel_type_definition\<close>, 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));
--- 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>\<open>unoverload\<close>,
- fn (const, thm) => unoverload_impl const thm)));
+val (_, unoverload_oracle) =
+ Theory.setup_result
+ (Thm.add_oracle (\<^binding>\<open>unoverload\<close>, fn (const, thm) => unoverload_impl const thm));
fun unoverload const thm = unoverload_oracle (const, thm);
--- 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>\<open>x = ct and y = \<open>Thm.cterm_of ctxt (term_of_int_list ks)\<close>
in cterm \<open>x \<equiv> y\<close> for x y :: \<open>int list\<close>\<close>;
- val (_, sort_oracle) = Context.>>> (Context.map_theory_result
- (Thm.add_oracle (\<^binding>\<open>sort\<close>, raw_sort)));
+ val (_, sort_oracle) = Theory.setup_result (Thm.add_oracle (\<^binding>\<open>sort\<close>, raw_sort));
in
--- 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;
--- 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*)
--- 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 =
--- 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
--- 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,
--- 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 =
--- 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;
--- 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));
--- 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);
--- 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;
--- 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 *)
--- 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>\<open>if_none\<close> true
- (fn _ => fn src => fn ctxt =>
+ (ML_Context.add_antiquotation_embedded \<^binding>\<open>if_none\<close>
+ (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'';
--- 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)))
--- 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>\<open>instantiate\<close> true
- (fn range => fn src => fn ctxt =>
+ (ML_Context.add_antiquotation_embedded \<^binding>\<open>instantiate\<close>
+ (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
--- 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);
--- 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 ()
--- 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
"!!" "!" "+" ":" ";" "<" "<=" "==" "=>" "?" "[" "\<comment>" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
- "\<subseteq>" "]" "binder" "by" "in" "infix" "infixl" "infixr" "is" "open" "output"
- "overloaded" "pervasive" "premises" "structure" "unchecked"
+ "\<subseteq>" "]" "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>\<open>simproc_setup\<close> "define simproc in ML"
- (Parse.name_position --
- (\<^keyword>\<open>(\<close> |-- Parse.enum1 "|" Parse.term --| \<^keyword>\<open>)\<close> --| \<^keyword>\<open>=\<close>) --
- Parse.ML_source >> (fn ((a, b), c) => Isar_Cmd.simproc_setup a b c));
+ Simplifier.simproc_setup_command;
in end\<close>
--- 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";
--- 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 *)
--- 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);
--- 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>\<open>expand_def\<close>
- {lhss = [Free ("x", TFree ("'a", []))], proc = K get_def});
+val _ = \<^simproc_setup>\<open>expand_def ("x::'a") = \<open>K get_def\<close>\<close>;
(* Isar command *)
--- 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);
--- 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>\<open>simproc_setup\<close>
+ (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>\<open>...\<close>" ^ Position.here pos)));
+
(** congruence rule to protect foundational terms of local definitions **)
--- 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);
--- 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 *)
--- 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>\<open>PROP Code_Generator.holds\<close> else ct)
end;
-val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result
- (Thm.add_oracle (\<^binding>\<open>holds_by_evaluation\<close>,
- 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>\<open>holds_by_evaluation\<close>,
+ 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>\<open>Pure.eq :: prop \<Rightarrow> prop \<Rightarrow> prop\<close>
ct \<^cprop>\<open>PROP Code_Generator.holds\<close>;
-val (_, holds_oracle) = Context.>>> (Context.map_theory_result
- (Thm.add_oracle (\<^binding>\<open>holds\<close>, holds)));
+val (_, holds_oracle) = Theory.setup_result (Thm.add_oracle (\<^binding>\<open>holds\<close>, holds));
in
--- 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>\<open>Pure.all (t :: 'a::{} \<Rightarrow> prop)\<close>],
- proc = fn _ => fn ctxt => fn ct => mk_swap_rrule ctxt ct};
+ \<^simproc_setup>\<open>passive rearrange_eqs ("Pure.all (t :: 'a::{} \<Rightarrow> prop)") = \<open>K mk_swap_rrule\<close>\<close>;
(* rotate k premises to the left by j, skipping over first j premises *)
--- 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>\<open>triv_of_class\<close>, 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>\<open>triv_of_class\<close>,
+ 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>\<open>normalization_by_evaluation\<close>,
+val (_, raw_oracle) =
+ Theory.setup_result (Thm.add_oracle (\<^binding>\<open>normalization_by_evaluation\<close>,
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);
--- 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 \<open>Arithmetic simplification\<close>
+
ML_file \<open>~~/src/Provers/Arith/cancel_numerals.ML\<close>
ML_file \<open>~~/src/Provers/Arith/combine_numerals.ML\<close>
ML_file \<open>arith_data.ML\<close>
+simproc_setup nateq_cancel_numerals
+ ("l #+ m = n" | "l = m #+ n" | "l #* m = n" | "l = m #* n" | "succ(m) = n" | "m = succ(n)") =
+ \<open>K ArithData.nateq_cancel_numerals_proc\<close>
+
+simproc_setup natless_cancel_numerals
+ ("l #+ m < n" | "l < m #+ n" | "l #* m < n" | "l < m #* n" | "succ(m) < n" | "m < succ(n)") =
+ \<open>K ArithData.natless_cancel_numerals_proc\<close>
+
+simproc_setup natdiff_cancel_numerals
+ ("(l #+ m) #- n" | "l #- (m #+ n)" | "(l #* m) #- n" | "l #- (m #* n)" |
+ "succ(m) #- n" | "m #- succ(n)") =
+ \<open>K ArithData.natdiff_cancel_numerals_proc\<close>
+
+
+subsubsection \<open>Examples\<close>
+
+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 \<le> 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) \<le> succ(z #+ x)" apply simp oops
+
subsection\<open>Difference\<close>
--- 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 \<open>int_arith.ML\<close>
-subsection \<open>examples:\<close>
+simproc_setup inteq_cancel_numerals
+ ("l $+ m = n" | "l = m $+ n" | "l $- m = n" | "l = m $- n" | "l $* m = n" | "l = m $* n") =
+ \<open>K Int_Numeral_Simprocs.inteq_cancel_numerals_proc\<close>
+
+simproc_setup intless_cancel_numerals
+ ("l $+ m $< n" | "l $< m $+ n" | "l $- m $< n" | "l $< m $- n" | "l $* m $< n" | "l $< m $* n") =
+ \<open>K Int_Numeral_Simprocs.intless_cancel_numerals_proc\<close>
+
+simproc_setup intle_cancel_numerals
+ ("l $+ m $\<le> n" | "l $\<le> m $+ n" | "l $- m $\<le> n" | "l $\<le> m $- n" | "l $* m $\<le> n" | "l $\<le> m $* n") =
+ \<open>K Int_Numeral_Simprocs.intle_cancel_numerals_proc\<close>
+
+simproc_setup int_combine_numerals ("i $+ j" | "i $- j") =
+ \<open>K Int_Numeral_Simprocs.int_combine_numerals_proc\<close>
+
+simproc_setup int_combine_numerals_prod ("i $* j") =
+ \<open>K Int_Numeral_Simprocs.int_combine_numerals_prod_proc\<close>
+
+
+subsubsection \<open>Examples\<close>
text \<open>\<open>combine_numerals_prod\<close> (products of separate literals)\<close>
lemma "#5 $* x $* #3 = y" apply simp oops
--- 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>\<open>data_free_trace\<close> (K false);
- fun mk_new ([],[]) = \<^Const>\<open>True\<close>
- | mk_new (largs,rargs) =
- Balanced_Tree.make FOLogic.mk_conj
+fun mk_new ([],[]) = \<^Const>\<open>True\<close>
+ | 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>\<open>False\<close>
- 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>\<open>(x::i) = y\<close>], 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>\<open>False\<close>
+ 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;
\<close>
-setup \<open>
- Simplifier.map_theory_simpset (fn ctxt => ctxt addsimprocs [DataFree.conv])
-\<close>
+simproc_setup data_free ("(x::i) = y") = \<open>fn _ => Data_Free.proc\<close>
end
--- 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>\<open>l #+ m = n\<close>, \<^term>\<open>l = m #+ n\<close>,
- \<^term>\<open>l #* m = n\<close>, \<^term>\<open>l = m #* n\<close>,
- \<^term>\<open>succ(m) = n\<close>, \<^term>\<open>m = succ(n)\<close>],
- proc = K EqCancelNumerals.proc},
- Simplifier.make_simproc \<^context> "natless_cancel_numerals"
- {lhss =
- [\<^term>\<open>l #+ m < n\<close>, \<^term>\<open>l < m #+ n\<close>,
- \<^term>\<open>l #* m < n\<close>, \<^term>\<open>l < m #* n\<close>,
- \<^term>\<open>succ(m) < n\<close>, \<^term>\<open>m < succ(n)\<close>],
- proc = K LessCancelNumerals.proc},
- Simplifier.make_simproc \<^context> "natdiff_cancel_numerals"
- {lhss =
- [\<^term>\<open>(l #+ m) #- n\<close>, \<^term>\<open>l #- (m #+ n)\<close>,
- \<^term>\<open>(l #* m) #- n\<close>, \<^term>\<open>l #- (m #* n)\<close>,
- \<^term>\<open>succ(m) #- n\<close>, \<^term>\<open>m #- succ(n)\<close>],
- 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)";
-*)
--- 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>\<open>zadd for t u\<close>;
@@ -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>\<open>l $+ m = n\<close>, \<^term>\<open>l = m $+ n\<close>,
- \<^term>\<open>l $- m = n\<close>, \<^term>\<open>l = m $- n\<close>,
- \<^term>\<open>l $* m = n\<close>, \<^term>\<open>l = m $* n\<close>],
- proc = K EqCancelNumerals.proc},
- Simplifier.make_simproc \<^context> "intless_cancel_numerals"
- {lhss =
- [\<^term>\<open>l $+ m $< n\<close>, \<^term>\<open>l $< m $+ n\<close>,
- \<^term>\<open>l $- m $< n\<close>, \<^term>\<open>l $< m $- n\<close>,
- \<^term>\<open>l $* m $< n\<close>, \<^term>\<open>l $< m $* n\<close>],
- proc = K LessCancelNumerals.proc},
- Simplifier.make_simproc \<^context> "intle_cancel_numerals"
- {lhss =
- [\<^term>\<open>l $+ m $\<le> n\<close>, \<^term>\<open>l $\<le> m $+ n\<close>,
- \<^term>\<open>l $- m $\<le> n\<close>, \<^term>\<open>l $\<le> m $- n\<close>,
- \<^term>\<open>l $* m $\<le> n\<close>, \<^term>\<open>l $\<le> m $* n\<close>],
- 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>\<open>i $+ j\<close>, \<^term>\<open>i $- j\<close>],
- 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>\<open>i $* j\<close>], 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])));