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 `defun-sk` definition of

Also see simplify-defun for an analogous utility for simplifying
`defun` forms.

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-sk` or the soft::soft tool, `simplify` to obtain an
essentially equivalent call.

(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.

Evaluation of

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

FN was defined using the soft::soft tooldefun-sk2 , then the new function symbol is also introduced withdefun-sk2 .

Determines the assumptions for simplification.

The value of

:assumptions must be 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 assumingH' , whereH' is the result of simplifyingH .

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) . Similarly, if only this:disable or:enable is 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: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.

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.

Specify the new guard.

The value of

:guard is 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: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.

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 isnil . However, this keyword is ignored if the keyword:simplify-body has valuenil .

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 will that results in a new function symbol. Note: the valuenil is 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-only ist , then

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

Specify the

:rewrite option for the generateddefun-sk form.By default, the

:rewrite field of the generateddefun-sk form (ordefun-sk2 form) corresponds to that of the corresponding form for the input function symbol. (Exception: currently, custom:rewrite fields are dropped. A comment about a proposedsimplify-defthm in source filesimplify-defun-sk.lisp discusses this issue.) If the:rewrite option is supplied, then its value is used for the:rewrite field of the generateddefun-sk (ordefun-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: thematrixof the body, which occurs after the quantifier). If this keyword has valuenil , 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-sk form, as well as the enabled status and name for the generated theorem.If

:thm-enable has valuenil , 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:auto ornil , then the name of the theorem will beFN-becomes-NEW . When:skolem-name is supplied, it becomes the:skolem-name of the generateddefun-sk form.

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 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-sk NEW (...) (declare ...) NEW-BODY)

where

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

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