		Search-engine friendly clone of the ACL2 documentation.

Simplify-term

Simplify a term.

Introduction

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 simplify-term.

Evaluation of the form (simplify-term OLD) will attempt to create a new term, say, NEW, that is logically equivalent to the input term OLD but is simpler. In the rest of this documentation page, OLD will denote the input term and NEW will generally denote the new, simplified term.

Also see simplify for an analogous utilities for simplifying definitions.

A simplify-term 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-term 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-term 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 simplify-term may be replaced by simplify to obtain an essentially equivalent call.

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

Inputs

OLD

Denotes the term to transform, which need not be translated (see ACL2::term).

Evaluation of (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 OLD with NEW. Details may be controlled by keyword parameters as described below.

: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 that occur in OLD.

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.

:equiv — default nil

Determine the equivalence relation to preserve when simplifying.

By specifying :equiv EQV simplify-term attempts to simplify the input term 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-term 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.

:must-simplify — default t

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

:print — default :result

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.

:rule-classes — default :rewrite

By default, or if :rewrite is specified for :rule-classes, the defthm or defthmd event created by simplify-term will be generated without a :rule-classes argument, hence stored as a rewrite rule (see ACL2::rule-classes). Otherwise, the value specified for the :rule-classes argument of the simplify-term call will be provided as the :rule-classes argument of the generated event.

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

:simplify-body — default t

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.

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

: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 input term, OLD with the new term, 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.

:untranslate — default :nice

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

See untranslate-specifier.

Generated Theorem

The generated theorem generally has the form

(defthm OLD-becomes-NEW
  (equal OLD NEW))

where equal will be replaced by an equivalence relation if specified by keyword argument :equiv. However, if keyword argument :assumptions specifies assumptions A1, ... An, then the generated theorem has the following form (with equal possibly replaced by an equivalence relation as explained above).

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

Subtopics

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