		Search-engine friendly clone of the ACL2 documentation.

Simplify-defun-sk

Simplify the definition of a given function made with defun-sk.

Introduction

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, defun-sk2. When successful, it creates a new such form by simplifying the body of the definition of such a function symbol.

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

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

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

A simplify-defun-sk call causes an error if no simplification takes place or if the proof obligations fail to be met. 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-sk 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 use keyword argument :show-only t in your simplify-defun-sk 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 evaluting of x. Note that FN should be a function symbol previously defined with defun-sk or the soft::soft tool, defun-sk2; thus, simplify-defun-sk may be replaced by 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
                   )

Inputs

Denotes the target function to transform.

Evaluation of (simplify-defun-sk FN ...) assumes that the input symbol, FN, is a :logic mode function symbol defined with defun-sk or 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 FN 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 tool defun-sk2, then the new function symbol is also introduced with defun-sk2.

:assumptions — default nil

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 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 H', where H' is the result of simplifying H.

: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). 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 of prog2$, ec-call, time$, and other such operators that provide special behavior; see ACL2::return-last-blockers.

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

:guard — default :auto

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.

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

:must-simplify — default t

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-body has value nil.

: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 will that results in a new function symbol. Note: the value nil is treated the same as :auto.

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

nil, to submit the events (the default).

t, to only show the events.

:rewrite

Specify the :rewrite option for the generated defun-sk form.

By default, the :rewrite field of the generated defun-sk form (or defun-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 proposed simplify-defthm in source file simplify-defun-sk.lisp discusses this issue.) If the :rewrite option is supplied, then its value is used for the :rewrite field of the generated defun-sk (or defun-sk2) form.

:simplify-body — default t

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.

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

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 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 :auto or nil, then the name of the theorem will be FN-becomes-NEW. When :skolem-name is supplied, it becomes the :skolem-name of the generated defun-sk form.

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

where NEW-BODY is the result of simplifying the body of FN (more precisely, the matrix of that quantified formula) unless keyword option :simplify-body has value nil. See above for how that option controls simplification of the body, measure, and guard. However, if FN was defined using the soft::soft tool defun-sk2, then the definition of NEW is also made with defun-sk2.

The generated theorem generally has the form

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

where the calls of FN and NEW are on the formals of FN. However, if keyword argument :assumptions specifies assumptions A1, ... An, then the generated theorem has the following form.

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

Subtopics

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