		Search-engine friendly clone of the ACL2 documentation.

Simplify-defun

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 defun form by simplifying the body of the definition of such a function symbol.

Introduction

See simplify-defun-examples for an introductory tutorial for simplify-defun, which presents an extensive series of examples.

Evaluation of the form (simplify-defun FN) will attempt to define a new function, say, FN$1, that is logically equivalent to the definition of FN but is simpler. In the rest of this documentation page, FN will denote the input function symbol and NEW will generally denote the new function symbol.

Note that simplify-defun transforms definitions made using defun or macros such as defund that expand to calls of defun, or the application 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 defun. Also see simplify-defun+ for a variant of simplify-defun, and see transform-and-propagate for a utility that can apply simplify-defun to several function symbols after applying an indicated transformation.

A simplify-defun call causes an error if the proof obligations fail to be met or, by default, if no simplification takes place. The implementation has been carefully orchestrated so that the proof obligations will generally succeed. When this is not the case, you may invoke show-simplify-defun with the same arguments in order to obtain the form that failed to be admitted, so that you can modify it manually. Or equivalently, simply add keyword argument :show-only t in your simplify-defun call.

General Form

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 (:eval x), then the actual argument is the result of evaluating x. Note that FN should be a function symbol previously defined with defun; thus, simplify-defun may be replaced by 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
                )

Inputs

Special Note on keyword arguments in the case of mutual-recursion. If FN was defined with mutual-recursion, then normally all keyword arguments are applied to the simplification of all definitions that were introduced in that same mutual-recursion event. However, every keyword argument except :non-executable, :print, :verify-guards, and :show-only can direct different values to be applied to different definitions, by supplying a keyword argument of the form (:map (fn1 val1) ... (fnk valk)), where (fn1 ... fnk) is the clique introduced by that mutual-recursion. To get that clique, evaluate the form (get-clique 'FN (w state)). Every member of the clique must be specified, but in any order. Moreover, entries can be combined in a way inspired by case: the key may be a list of functions, i.e., (:map ... ((f g ... h) val) ... ) which is equivalent to (:map ... (f val) (g val) ... (h val) ... ); and an optional final entry of the form (:otherwise val) specifies that all remaining clique members should be assigned val. End of Special Note.

Denotes the target function to transform.

Evaluation of (simplify-defun FN ...) assumes that the input symbol, FN, is a :logic mode function symbol, defined with defun or with a macro expanding to a call of defun (such as defund). Successful evaluation admits a new defun, with the same formals as FN, and a theorem equating FN 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.

:assumptions — default nil

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 of FN. However, :assumptions may be :guard, which is equivalent to :assumptions (G) where G is the guard of FN; and for :assumptions (A1 ... :guard ... An), :guard is similarly replaced by G. 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 of H', where H' is the result of simplifying each term in the list H. 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 of simplify-defun, the sole label is :assumptions-preserved. This particular condition is that the assumptions must be preserved by recursive calls of the function.

:disable — default :none
:enable — default :none

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'), where D' is the result of adding to D the ACL2::runes that were introduced with the given function, FN. The same holds if :disable is omitted, in which case D is treated as nil. 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 of prog2$, ec-call, time$, and other such operators that provide special behavior; see ACL2::return-last-blockers.

:equiv — default nil

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 is nil or not specified, then the equivalence relation used is EQUAL. For example, the successful application of simplify-defun with argument :equiv iff will result in a body that is Boolean-equivalent to the original body.

:expand — default nil

Give an :ACL2::expand hint 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 when simplify-defun is applied to a function defined using recursion, any such directive to expand a call of that function will be ignored.

:hints — default nil

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

If :hints is omitted or has value nil, 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 with mutual-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 than nil, 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 a mutual-recursion form then you may find it helpful to disable these for every FN in the clique of functions being introduced.

:guard-hints — default :auto

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

:new-enable — default :auto

Determines whether the new function is enabled.

If this keyword has value t or 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.

:hyp-fn — default nil

Determines the assumptions for simplification.

If the list of formals of the given function symbol, FN, is (X1 ... Xk), then specifying :hyp-fn h for h not nil is equivalent to specifying :assumptions ((h X1 ... Xk)). It is illegal to provide non-nil values for both :hyp-fn and :assumptions.

:measure — default :auto

Provides the measure for the generated function.

The default is :auto, in which case: when there is a measure M_FN associated with the input function symbol, FN (because the definition of FN is recursive), then :measure M_FN is included in the xargs of the new definition. Otherwise :measure M has been supplied for some M that is not :auto; then :measure M is included in the xargs of the new definition unless M is nil.

:measure-hints — default :auto

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

The :measure-hints option is used as the xargs :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.

:must-simplify — default t

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 that t represents the value (:body t :measure nil :guard nil). Thus each key is one of :body, :measure, or :guard, and each value is t or nil, where nil 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 is nil. Note that the value nil 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.

NOTE for the case that option :simplify-body specifies a pattern. In that case, every subterm targeted for simplification by the pattern must simplify to a result different from the subterm. When there are LET-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.

:new-enable — default :auto

Determines whether the new function is enabled.

If this keyword has value t or 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.

:new-name — default :auto

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

:non-executable — default :auto

Specify non-executability of the new function.

When this keyword has value t, the generated definition is a call of defun-nx or defund-nx; if the value is nil, then the generated definition is a call of defun or defund. The default is :auto, which is equivalent to t if the original definition is non-executable (defined with defun-nx or defund-nx or, more generally, with xargs keyword :non-executable t), else nil. This option is useful when simplification transforms the definition into one that violates syntactic rules for executability, such as taking the CAR 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 is nil, then the simplified body may be adjusted in an attempt to make it executable, for example by inserting a call of mv-list in a context where a single value is expected but multiple values are supplied.

:print — default :result

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.

:show-only — default nil

Determines whether the events generated by the macro should be submitted (the default) or only shown on the screen. Note that if :show-only is t, then :print is ignored.

Note that if :show-only is t, then :print is ignored.

nil, to submit the events (the default).

t, to only show the events.

:simplify-body — default t

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 or nil, the value can be a pattern, 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 the symbol-name of var contains just the single atsign character, and otherwise _var denotes the result of prefixing an underscore character to the symbol-name of var, without changing its symbol-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 pattern P' by expanding away calls of :@ as though it were the identity macro, that is, by replacing each call of the form (:@ u) by u. Then P' is matched against the definition body B in a left-to-right depth-first traversal to find the first subterm B' of B that is an instance of P' in which only variables whose name starts with the underscore character (_) are instantiated, in the following generous sense: for a variable whose symbol-name is exactly "_" each occurrence is allowed to match a different term. If no subterm B' exists as described above, then an error occurs.

The terms to be simplified are those subterms of B' that correspond to subterms of P' that were originally (that is, in P) calls of :@.

Each subterm is simplified with respect to the governing IF tests (or negated tests, as appropriate) in B as well the simplifications of any :assumptions provided. If any such simplification yields an unchanged subterm, then the call of simplify-defun fails. Note that any dive into the body of a LET 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-level IF 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 the OR call in the body, since (if @1 @1 _) only matches when the test and true branch of the IF 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 !>

:simplify-guard — default nil
:simplify-measure — default nil

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.

:thm-enable — default t
:thm-name — default :auto

Determines the name and enabled status of the new theorem.

If :thm-enable has value nil, then the generated theorem that equates the old function symbol FN with the new, NEW, will be a call of defthmd. Otherwise, defthm will be used. In either case: if :thm-name is missing or is :auto or 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, but note that in this case, if FN was introduced with mutual-recursion then a value of the form (:map ...) (as described above) must be used.

:theory — default :none

Specify the theory under which simplification is performed.

If :theory EXPR is 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 :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 as prog2$, ec-call, and time$; see ACL2::return-last-blockers.

:untranslate — default :nice

Specify how to create a user-level term from the simplified body.

See untranslate-specifier.

:verify-guards — default :auto

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 if V is 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-NEW theorem (see above), by calling verify-guards on 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 the OLD-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.)

Generated Definition and Theorem

The generated definition has the same formals as the definition of FN, and has the form

(defun NEW (...)
  (declare ...)
  NEW-BODY)

where NEW-BODY is the result of simplifying the body of FN unless keyword option :simplify-body has value nil. See above for how that option controls simplification of the body, measure, and guard. The declare form, if any, in the generated definition is generally consistent with the declarations in the definition of FN, except when overridden by arguments to the simplify (or simplify-defun) call. For example, by default: the generated definition includes a :verify-guards xarg that reflects the guard-verified status of FN, and it includes a declaration of the form (xargs ... :normalize ...) if and only if there is such a declaration in the definition of FN.

The generated theorem generally has the form

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

where the calls of FN and NEW are on the formals of FN, and where equal will be replaced by an equivalence relation if specified by keyword argument :equiv. However, if either keyword argument :assumptions or :hyp-fn specifies assumptions A1, ... An, then the generated theorem has the following form (with equal possibly replaced by an equivalence relation as explained above).

(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 :thm-name.

Subtopics

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