Simplify a term.
This macro is an interface to the simplify transformation that, when successful, creates a new term by simplifying the given input term. The input should not be a symbol, and it need not be translated (see ACL2::term).
See simplify-term-examples for examples that illustrate the use of
Evaluation of the form
Also see simplify for an analogous utilities for simplifying definitions.
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-term old &key :assumptions ; default nil :disable ; default :none :enable ; default :none :equiv ; default nil :expand ; default nil :must-simplify ; default t :print ; default :result :rule-classes ; default :rewrite :show-only ; default nil :simplify-body ; default t :theory ; default :none :thm-enable ; default t :thm-name ; default :auto :untranslate ; default :nice )
Denotes the term to transform, which need not be translated (see ACL2::term).
(simplify-term OLD ...)assumes that the input term contains only calls of :logic mode function symbols, that is, not calls of :program mode function symbols. Successful evaluation produces a new term, NEW, and a theorem equating OLDwith NEW. Details may be controlled by keyword parameters as described below.
Determines the assumptions for simplification.
The value of
:assumptionsmust be a list of terms (not necessarily translated; see ACL2::term) that only reference variables that occur in OLD.
: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.
Determine the equivalence relation to preserve when simplifying.
:equiv EQV simplify-termattempts to simplify the input term to one that is equivalent, in the sense of the equivalence relation, EQV. If :equivis nilor not specified, then the equivalence relation used is EQUAL. For example, the successful application of simplify-termwith argument :equiv iffwill result in a body that is Boolean-equivalent to the original body.
:ACL2::expand hint to the simplifier.
:expand Eis supplied, simplification will take place as though the hint :expand Eis given to the top-level goal in the theorem prover.
This keyword specifies whether the simplified term must be different from the input term: 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.
Specify what to print.
By default, only the resulting theorem is printed. In general, the value is a print specifier print-specifier that controls the output.
By default, or if
:rewriteis specified for :rule-classes, the defthm or defthmd event created by simplify-termwill be generated without a :rule-classesargument, hence stored as a rewrite rule (see ACL2::rule-classes). Otherwise, the value specified for the :rule-classesargument of the simplify-termcall will be provided as the :rule-classesargument of the generated event.
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.
If this keyword has value
t, which is the default, then the input term is simplified. 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.
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.
Determines the name and enabled status of the new theorem.
:thm-enablehas value nil, then the generated theorem that equates the input term, OLDwith the new term, NEW, will be a call of defthmd. Otherwise, defthmwill be used. In either case: if :thm-nameis missing or is :autoor nil, then the name of the theorem will be OLD-becomes-NEW; otherwise, the name of the theorem will be the value of :thm-name.
Specify how to create a user-level term from the simplified term.
The generated theorem generally has the form
(defthm OLD-becomes-NEW (equal OLD NEW))
(defthm OLD-becomes-NEW (implies (and A1 A2 ... An) (equal OLD NEW)))
In both cases, the name of the new theorem shown is the default but may be
specified with keyword option