Simplify the definition of a given function made with defun-sk.
This macro is an interface to the simplify transformation for
function symbols that the user (or a tool) introduces with defun-sk or
the soft::soft tool,
See simplify-defun-sk-examples for an introductory tutorial for
Evaluation of the form
Also see simplify-defun for an analogous utility for simplifying defun forms.
The following form shows all the keyword arguments in alphabetical order,
together with their default values (i.e., when the keyword is omitted). No
argument is evaluated, except that if an argument is of the form
(simplify-defun-sk fn ; input function symbol previously defined with defun-sk &key :assumptions ; default nil :disable ; default :none :enable ; default :none :new-enable ; default :auto :new-name ; default nil :guard ; default :auto :guard-hints ; default :auto :must-simplify ; default t :print ; default :result :show-only ; default nil :rewrite ; default :auto :simplify-body ; default t :skolem-name ; default nil :thm-enable ; default t :thm-name ; default :auto :theory ; default :none :untranslate ; default :nice :verify-guards ; default :auto )
Denotes the target function to transform.
(simplify-defun-sk FN ...)assumes that the input symbol, FN, is a :logic mode function symbol defined with defun-skor with a macro expanding to a call of defun-sk. Successful evaluation admits a new defun-sk, with the same formals as FN, and a theorem equating FNwith the newly-defined function symbol. Details, such as whether or not to perform guard verification, may be controlled by keyword parameters as described below.
FNwas defined using the soft::soft tool defun-sk2, then the new function symbol is also introduced with defun-sk2.
Determines the assumptions for simplification.
The value of
:assumptionsmust be a list of terms (not necessarily translated; see ACL2::term) that only reference variables among the formal parameters of FN. However, :assumptionsmay be :guard, which is equivalent to :assumptions (G)where Gis the guard of FN; and for :assumptions (A1 ... :guard ... An), :guardis similarly replaced by G. Below we imagine that :guardhas been replaced in these ways; let us assume below that the value of :assumptionsis a list that does not contain :guard.
:assumptions His supplied, all simplification will be performed assuming H', where H'is the result of simplifying H.
Determine the theory for simplification.
:disable Dand :enable Eare supplied, then simplification will be performed in the theory (e/d* E D). Similarly, if only this :disableor :enableis supplied, then the theory will be (disable D)or (enable E), respectively. If either of these keywords is supplied, then it is illegal to supply :theory. Also see the discussion below of the :theoryargument. Note that :disablemay be useful for preserving calls of prog2$, ec-call, time$, and other such operators that provide special behavior; see ACL2::return-last-blockers.
Determines whether the new function is enabled.
If this keyword has value
tor nil, then the new function symbol will be enabled or disabled, respectively. Otherwise its value should be the keyword :auto, and the new function symbol will be enabled or disabled according to whether the input function symbol is disabled or enabled, respectively.
Specify the new guard.
The value of
:guardis a guard for the new function symbol, in place of the default of inheriting the guard of the input function symbol.
Provides ACL2::hints for verifying guards of the generated function. If this argument is supplied with value other than its default of
:auto, then that value becomes the :hintsof a verify-guards event. Otherwise such hints are generated automatically. See the discussion of :verify-guardsbelow for a discussion of guard verification and its automatically-generated hints.
This keyword specifies whether the simplified body must be different from the original body: yes, if the value is
t(the default), and no if the value is nil. However, this keyword is ignored if the keyword :simplify-bodyhas value nil.
Determines the name of the generated function.
This value, if provided, becomes the function symbol of the generated definition. Otherwise the generated function symbol is obtained by adding a suffix
"$n"to the input function symbol's name, for the least natural number nwill that results in a new function symbol. Note: the value nilis treated the same as :auto.
Specify what to print.
By default, only the resulting definition and theorem are printed. In general, the value is a print specifier print-specifier that controls the output.
Determines whether the events generated by the macro should be submitted (the default) or only shown on the screen. Note that if
:show-onlyis t, then
nil, to submit the events (the default).
t, to only show the events.
:rewriteoption for the generated defun-skform.
By default, the
:rewritefield of the generated defun-skform (or defun-sk2form) corresponds to that of the corresponding form for the input function symbol. (Exception: currently, custom :rewritefields are dropped. A comment about a proposed simplify-defthmin source file simplify-defun-sk.lispdiscusses this issue.) If the :rewriteoption is supplied, then its value is used for the :rewritefield of the generated defun-sk(or defun-sk2) form.
If this keyword has value
t, which is the default, then the body of the input function symbol's definition is simplified (more precisely: the matrix of the body, which occurs after the quantifier). If this keyword has value nil, then no simplification is attempted. Otherwise, the value of this keyword is a pattern. See simplify-defun, specifically the documentation there for keyword argument :simplify-body, for a discussion of patterns and how they are matched.
Control the Skolem function for the generated
defun-skform, as well as the enabled status and name for the generated theorem.
:thm-enablehas value nil, then the generated theorem that equates the old and new function symbols will be disabled; else it will be enabled (the default). In either case, the name of the theorem will be the value of :thm-name; if that keyword argument is missing or is :autoor nil, then the name of the theorem will be FN-becomes-NEW. When :skolem-nameis supplied, it becomes the :skolem-nameof the generated defun-skform.
Specify the theory under which simplification is performed.
:theory EXPRis supplied, then simplification will be performed in the theory given by EXPR, that is, as though the event (in-theory EXPR)were first evaluated. If either the :disableor :enablekeyword is supplied, then it is illegal to supply :theory. Note that some disabling may be useful if it is desired to preserve certain operators with special behavior such as prog2$, ec-call, and time$; see ACL2::return-last-blockers.
Specify how to create a user-level term from the simplified body.
Specify whether to verify guards for the new function.
By default, guard verification is performed for the new function symbol if and only if the input function symbol is guard-verified. This default behavior is overridden by a Boolean value
Vof :verify-guards: guard verification is done if Vis t, else is not done.
When guard verification is performed, it is attempted after several other events are admitted, including the new definition and the
OLD-becomes-NEWtheorem (see above), by calling verify-guards on the new function symbol. The :guard-hintsare utilized, if supplied (and not :auto). Otherwise, a :guard-hintsvalue is generated that specifies the theory used for simplification (see the discussion of :theory) augmented by the OLD-becomes-NEWtheorem (see above); also, if the old function symbol is guard-verified, the hints apply its guard theorem with a :usehint. This generated :guard-hintsvalue can cause up to three different proof attempts, each somewhat different from the others, when necessary. (For details use :show-only t.)
The generated definition has the same formals as the definition of
(defun-sk NEW (...) (declare ...) NEW-BODY)
The generated theorem generally has the form
(defthm FN-becomes-NEW (implies (and A1 A2 ... An) (equal (FN ...) (NEW ...))))
where the calls of
(defthm FN-becomes-NEW (iff (FN ...) (NEW ...)))
In both cases, the name of the new theorem shown is the default but may be
specified with keyword option