Simplify a term.

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

Evaluation of the form

Also see simplify for an analogous utilities for simplifying definitions.

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

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: logicmode function symbols, that is, not calls of: programmode function symbols. Successful evaluation produces a new term,NEW , and a theorem equatingOLD withNEW . Details may be controlled by keyword parameters as described below.

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

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 isnil or not specified, then the equivalence relation used isEQUAL . For example, the successful application ofsimplify-term 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.

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

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.

By default, or if

:rewrite is specified for:rule-classes , thedefthmordefthmdevent created bysimplify-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 thesimplify-term call will be provided as the:rule-classes argument of the generated event.

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.

If this keyword has value

t , which is the default, then the input term is simplified. 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.

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.

Determines the name and enabled status of the new theorem.

If

:thm-enable has valuenil , then the generated theorem that equates the input term,OLD with the new term,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 .

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

The generated theorem generally has the form

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

where

(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

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