Simplify the definition of a given function.

This macro is an interface to the `simplify` transformation
for function symbols that the user (or a tool) introduces with `defun`.
When successful, it creates a new

See simplify-defun-examples for an introductory tutorial for

Evaluation of the form

Note that `defun` or macros such as `defund` that expand to calls of `mutual-recursion` to such forms. See simplify-defun-sk for an analogous utility for which the input function
symbol was originally defined with `defun-sk` rather than

A

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 `defun`;
thus, `simplify` to obtain an
essentially equivalent call.

(simplify-defun FN &key :assumptions ; default nil :disable ; default :none :enable ; default :none :equiv ; default nil :expand ; default nil :hints ; default nil :new-enable ; default :auto :new-name ; default :auto :guard-hints ; default :auto :hyp-fn ; default nil :measure ; default :auto :measure-hints ; default :auto :must-simplify ; default (:body t :measure nil :guard nil) :non-executable ; default :auto :print ; default :result :show-only ; default nil :simplify-body ; default t :simplify-guard ; default nil :simplify-measure ; default nil :thm-enable ; default t :thm-name ; default :auto :theory ; default :none :untranslate ; default :nice :verify-guards ; default :auto )

**Special Note on keyword arguments in the case of mutual-recursion.** If

Denotes the target function to transform.

Evaluation of

(simplify-defun FN ...) assumes that the input symbol,FN , is a: logicmode function symbol, defined withdefunor with a macro expanding to a call ofdefun (such asdefund). Successful evaluation admits a newdefun , with the same formals asFN , and a theorem equatingFN with the newly-defined function symbol,NEW . Details, such as whether or not to perform guard verification, may be controlled by keyword parameters as described below.

Determines the assumptions for simplification.

The value of

:assumptions is generally a list of terms (not necessarily translated; see ACL2::term) that only reference variables among the formal parameters ofFN . However,:assumptions may be:guard , which is equivalent to:assumptions (G) whereG is the guard ofFN ; and for:assumptions (A1 ... :guard ... An) ,:guard is similarly replaced byG . Below we imagine that:guard has been replaced in these ways; let us assume below that the value of:assumptions is a list that does not contain:guard .When

:assumptions H is supplied, all simplification will be performed assuming the conjunction ofH' , whereH' is the result of simplifying each term in the listH . For another way to specify assumptions, see the discussion of:hyp-fn , below.If

FN is defined recursively and:assumptions is specified, there will generally be a formula, called an ``applicability condition,'' that must be a theorem in order for the transformation to succeed. Any transformation might have applicability conditions, each of which has a label; in the case ofsimplify-defun , the sole label is:assumptions-preserved . This particular condition is that the assumptions must be preserved by recursive calls of the function.

Determine the theory for simplification.

If

:disable D and:enable E are supplied, then simplification will be performed in the theory(e/d* E D '), whereD' is the result of adding toD the ACL2::runes that were introduced with the given function,FN . The same holds if:disable is omitted, in which caseD is treated asnil . Similarly, if only:disable is supplied, then the theory will be(disable* D '). If either of these keywords is supplied, then it is illegal to supply:theory . Also see the discussion below of the:theory argument. Note that:disable may be useful for preserving calls ofprog2$,ec-call,time$, and other such operators that provide special behavior; see ACL2::return-last-blockers.

Determine the equivalence relation to preserve when simplifying.

By specifying

:equiv EQV simplify-defun attempts to simplify the body to one that is equivalent, in the sense of the equivalence relation,EQV . If:equiv isnil or not specified, then the equivalence relation used isEQUAL . For example, the successful application ofsimplify-defun with argument:equiv iff will result in a body that is Boolean-equivalent to the original body.

Give an

: ACL2::expandhint to the simplifier.When

:expand E is supplied, simplification will take place as though the hint:expand E is given to the top-level goal in the theorem prover. NOTE however that whensimplify-defun is applied to a function defined using recursion, any such directive to expand a call of that function will be ignored.

Specifies the ACL2::hints for proving that assumptions are preserved by recursive calls.

If

:hints is omitted or has valuenil , then the ACL2::definition, ACL2::executable-counterpart, and ACL2::type-prescription ACL2::runes for the given function symbol will all be disabled. If moreover that symbol is introduced withmutual-recursion, then these runes will be disabled for all function symbols in its clique, i.e., all function symbols that were introduced with that symbol.If

:hints has a non-nil value, then that value should be a legal hints-specifier for the single applicability condition,:assumptions-preserved ; see hints-specifier.NOTE: If you supply

:hints with a value other thannil , then you may find it helpful to specify that the runes mentioned above are all disabled:FN ,(:e FN) , and(:t FN) (see ACL2::rune). If you are simplifying amutual-recursionform then you may find it helpful to disable these for everyFN in the clique of functions being introduced.

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:hints of averify-guardsevent. Otherwise such hints are generated automatically. See the discussion of:verify-guards below for a discussion of guard verification and its automatically-generated hints.

Determines whether the new function is enabled.

If this keyword has value

t ornil , 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.

Determines the assumptions for simplification.

If the list of formals of the given function symbol,

FN , is(X1 ... Xk) , then specifying:hyp-fn h forh notnil is equivalent to specifying:assumptions ((h X1 ... Xk)) . It is illegal to provide non-nil values for both:hyp-fn and:assumptions .

Provides the measure for the generated function.

The default is

:auto , in which case: when there is a measureM_FN associated with the input function symbol,FN (because the definition ofFN is recursive), then:measure M_FN is included in thexargs of the new definition. Otherwise:measure M has been supplied for someM that is not:auto ; then:measure M is included in thexargs of the new definition unlessM isnil .

Provides the measure ACL2::hints for the generated function.

The

:measure-hints option is used as thexargs:hints value in the generated definition. A special value:auto , which is the default, creates:hints for the termination proof that use the input function symbol's termination-theorem as well as suitable theory modification if any of:disable ,:enable , or:theory have value other than their default of:none .

Determine where simplification must make a change.

This keyword specifies whether each of the body, measure, and guard of the input definition is required to be simplified. Its value is a

keyword-value-listp, except thatt represents the value(:body t :measure nil :guard nil) . Thus each key is one of:body ,:measure , or:guard , and each value ist ornil , wherenil is the implicit value if the key is omitted. So by default: the body must simplify to a result different from the original body, or an error occurs; but no such requirement is made for simplification of the measure or the guard. Note that the respective value for keyword argument:body ,:measure , or:guard is ignored when, for the:must-simplify keyword argument, the value of keyword:simplify-body ,:simplify-measure , or:simplify-guard isnil . Note that the valuenil for:must-simplify is equivalent to the value(:body nil :measure nil :guard nil) , since the three keywords do not occur in the empty keyword-value-list.

NOTEfor the case that option:simplify-body specifies a pattern. In that case,everysubterm targeted for simplification by the pattern must simplify to a result different from the subterm. When there areLET -bindings above the subterm, the requirement is a bit more subtle: the simplification of the subterm under those bindings must differ from the result of substituting the bindings into the subterm.

Determines whether the new function is enabled.

If this keyword has value

t ornil , 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.

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 numbern that results in a new function symbol. Note: the valuenil is treated the same as:auto , and in the case thatFN was introduced withmutual-recursion, only these two values and a value of the form(:map ...) (as described above) are legal for:new-name .

Specify non-executability of the new function.

When this keyword has value

t , the generated definition is a call ofdefun-nxordefund-nx; if the value isnil , then the generated definition is a call ofdefunordefund. The default is:auto , which is equivalent tot if the original definition is non-executable (defined withdefun-nx ordefund-nx or, more generally, withxargskeyword:non-executable t ), elsenil . This option is useful when simplification transforms the definition into one that violates syntactic rules for executability, such as taking theCAR of a function call that returns multiple values.Note that the body of the generated definition may depend on the value of

:non-executable . Specifically, if the value isnil , then the simplified body may be adjusted in an attempt to make it executable, for example by inserting a call ofmv-listin a context where a single value is expected but multiple values are supplied.

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-only ist , thenNote that if

:show-only ist , then

nil , to submit the events (the default).t , to only show the events.

Specify whether to simplify the body and (optionally) if so, which subterms.

This keyword indicates whether to simplify the body of the input function symbol. Simplification is to be attempted when the value is not

nil , in which case it is an error if simplification leaves the body unchanged.Other than

t ornil , the value can be apattern, which must have at least one occurrence of a variable whose first character is an atsign (@ ) or a call of the form(:@ term) ; these variables and calls are to be matched with subterms to be simplified, according to the following process.

- First, each variable reference
var whose first character is an atsign (@ ) is replaced by a call(:@ _var) , where_var denotes the variable_ (in the ACL2 package) if thesymbol-nameofvar contains just the single atsign character, and otherwise_var denotes the result of prefixing an underscore character to thesymbol-name ofvar , without changing itssymbol-package-name. Note that the result must have at least one call of:@ , but no nested such calls. This replacement is done directly on the supplied pattern, using obvious heuristics to determine what is a variable reference; for example,@ is a variable reference in(foo @) and(let ((x @)) _) but not in(@ x) or(let ((@ x)) _) .- The resulting pattern is then replaced by its translation to an ACL2 term (see termp), which involves macroexpansion and removal of abbreviations; for example, the pattern
(+ (:@ _) 17) is translated to(BINARY-+ (:@ _) '17) . Note that for this purpose,:@ is treated as a unary function symbol.- The resulting pattern
P gives rise to a new patternP' by expanding away calls of:@ as though it were the identity macro, that is, by replacing each call of the form(:@ u) byu . ThenP' is matched against the definition bodyB in a left-to-right depth-first traversal to find the first subtermB' ofB that is an instance ofP' in which only variables whose name starts with the underscore character (_ ) are instantiated, in the following generous sense: for a variable whosesymbol-nameis exactly"_" each occurrence is allowed to match a different term. If no subtermB' exists as described above, then an error occurs.- The terms to be simplified are those subterms of
B' that correspond to subterms ofP' that were originally (that is, inP ) calls of:@ .- Each subterm is simplified with respect to the governing
IF tests (or negated tests, as appropriate) inB as well the simplifications of any:assumptions provided. If any such simplification yields an unchanged subterm, then the call ofsimplify-defun fails. Note that any dive into the body of aLET expression takes into account its bindings.Note: Because of how patterns are handled, you may find it safest to avoid variables

@ and_ in favor of their subscripted versions (e.g.,@3 or_4 ), if you use macros — in particular,or— and are surprised by how patterns are matched. Consider the following example.(defun foo (x y) (if (true-listp (cons 3 x)) (or (eql (length x) 17) y) 'dont-care))Then the following log may seem surprising at first, since the pattern might seem to specify only the call of

foo in the body of the definition.ACL2 !>(simplify-defun foo :simplify-body (or @ _)) (DEFUN FOO$1 (X Y) (DECLARE (XARGS :GUARD T :VERIFY-GUARDS NIL)) (IF (TRUE-LISTP X) (OR (EQUAL (LEN X) 17) Y) 'DONT-CARE)) ACL2 !>But the pattern

(or @ _) translates to(if @ @ _) , which matches the entire body; hence both the test of the top-levelIF call and its true branch were simplified. If instead we provide a subscript as shown below, the result is what we might reasonably expect: the match this time is on theOR call in the body, since(if @1 @1 _) only matches when the test and true branch of theIF call are the same.ACL2 !>(simplify-defun foo :simplify-body (or @1 _)) (DEFUN FOO$1 (X Y) (DECLARE (XARGS :GUARD T :VERIFY-GUARDS NIL)) (IF (TRUE-LISTP (CONS 3 X)) (OR (EQUAL (LEN X) 17) Y) 'DONT-CARE)) ACL2 !>

Determine whether to simplify the guard or the measure of the input function symbol, respectively.

A non-

nil value indicates that simplification is to be attempted.

Determines the name and enabled status of the new theorem.

If

:thm-enable has valuenil , then the generated theorem that equates the old function symbolFN with the new,NEW , will be a call ofdefthmd . Otherwise,defthm will be used. In either case: if:thm-name is missing or is:auto ornil , then the name of the theorem will beOLD-becomes-NEW ; otherwise, the name of the theorem will be the value of:thm-name , but note that in this case, ifFN was introduced withmutual-recursionthen a value of the form(:map ...) (as described above) must be used.

Specify the theory under which simplification is performed.

If

:theory EXPR is supplied, then simplification will be performed in the theory given byEXPR , that is, as though the event(in-theory EXPR) were first evaluated. If either the:disable or:enable keyword is supplied, then it is illegal to supply:theory . Note that if:theory is omitted (or:none ), then the ACL2::definition, ACL2::executable-counterpart, and ACL2::type-prescription ACL2::runes for the given function symbol,FN , will all be added automatically to the:disable argument. Note also that some disabling may be useful if it is desired to preserve certain operators with special behavior such asprog2$,ec-call, andtime$; 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

V of:verify-guards : guard verification is done ifV ist , 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-NEW theorem (see above), by callingverify-guardson the new function symbol. The:guard-hints are utilized, if supplied (and not:auto ). Otherwise, a:guard-hints value is generated that specifies the theory used for simplification (see the discussion of:theory ) augmented by theOLD-becomes-NEW theorem (see above); also, if the old function symbol is guard-verified, the hints apply its guard theorem with a:use hint. This generated:guard-hints value 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 NEW (...) (declare ...) NEW-BODY)

where

The generated theorem generally has the form

(defthm FN-becomes-NEW (equal (FN ...) (NEW ...)))

where the calls of

(defthm FN-becomes-NEW (implies (and A1 A2 ... An) (equal (FN ...) (NEW ...))))

In both cases, the name of the new theorem shown is the default but may be
specified with keyword option

- Simplify-defun-examples
- Examples illustrating
`simplify-defun`.