Rewrite a term

- An introductory example
- Return values
- General Form
- Basic options
- Hint options, each with default
nil - Advanced options
- Summary of algorithm
- Related tools

We begin with the following example of a call of `append`. We see
that the call of

ACL2 !>(rewrite$ '(car (append (cons x y) z)) :translate t) (X ((:DEFINITION BINARY-APPEND) (:REWRITE CDR-CONS) (:REWRITE CAR-CONS) (:FAKE-RUNE-FOR-TYPE-SET NIL))) ACL2 !>

Notice the ``fake rune'' that is returned. Fake runes are easy to remove;
see for example the constant

Other simple examples may be found in community book

A call

rewritten-term is the result of rewritingterm as directed by the other inputs; andrunes is a list containing the runes that participated in the rewriting ofterm torewritten-term .

Because of forcing (see force), rewriting of the input term may
generate goals to be proved later, based on the forced hypotheses encountered
during rewriting that were not relieved at that time. We call these ``forced
assumptions''. If there are forced assumptions, then they are conjoined into
a single goal, which by default is the target of a separate call to the
prover, much like a call of `thm`. The return value

There are many keyword arguments that control the rewriting process. One
of particular importance semantically is

All arguments of

(rewrite$ term ; Basic options (in alphabetical order): :alist ; default nil :ctx ; default 'rewrite$ :default-hints-p ; default t :equiv ; default nil :geneqv ; default nil :hyps ; default nil :must-rewrite ; default nil :prove-forced-assumptions ; default t :repeat ; default 1 :translate ; default nil :untranslate ; default nil ; Hint options (in alphabetical order), each with default nil: :backchain-limit-rw :expand :hands-off :in-theory :no-thanks :nonlinearp :restrict :rw-cache-state ; Advanced options (in alphabetical order): :obj ; default '? :rrec ; default nil :wrld ; default (w state) )

IMPORTANT: The keyword options, discussed below according to the groups above, are all evaluated. So for example:

; Correct (rewrite$ '(cons a (cdr x)) :alist '((a . (car x))) :hyps '((consp x))) ; WRONG! (rewrite$ '(cons a (cdr x)) :alist ((a . (car x))) :hyps ((consp x)))

:alist (defaultnil )

is an association list mapping variables to terms, where each term is already translated or else is untranslated according to whether the value of:translate isnil or non-nil , respectively.:ctx (default'rewrite$ )

is a ``context'', such as thectx argument of`er`.:default-hints-p (defaultt )

is non-nil when the construction of hints for the rewriter call is to take into account the default-hints in the current world.:equiv and:geneqv (both with defaultnil )

specify the equivalence relation(s) to be preserved by (congruence-based) rewriting. It is illegal to specify a non-nil value for more than one of these. Most users will prefer to use:equiv , which should be a function symbol that is a known (to ACL2) equivalence relation. The keyword option:geneqv is really only for those who know how generated equivalence relations are represented in the ACL2 system.:hyps (defaultnil )

is a non-empty list of hypotheses under which rewriting takes place. Each hypothesis is already translated or is untranslated according to whether the value of:translate isnil or non-nil , respectively.:must-rewrite (defaultnil )

indicates, when its value is non-nil , that the rewritten term must not be equal to the input term. It is illegal to supply non-nil values for both:alist and:must-rewrite , since it's usually not a sensible combination since at the least, the alist will be substituted into the term.:prove-forced-assumptions (defaultt )

affects the proof of the forced assumptions. It has the following legal values.t : prove the forced assumptions as mentioned above: a single prover call to prove their conjunction.:same-hints : same ast , except generate the same:hints for the prover call as are generated for the rewriting (from the eight hint options discussed below).nil : do not attempt a proof of the forced assumptions, instead returning a non-nil `pairs ' value as discussed above.:none-forced : cause an error if there are any forced assumptions.- Otherwise, the value of
:prove-forced-assumptions should be of the form expected for the value of:hints supplied to`defthm`. For example, the following might follow:prove-forced-assumptions in a call ofrewrite$ :'(("Goal" :in-theory (enable reverse))) .

:repeat (default1 )

indicates how many times to call the rewriter. The value should be a positive integer. If the value of:repeat is greater than 1, then the term resulting from the first call is the input term for the second call, whose result (if the value of:repeat is greater than 2) is the input term for the third call, and so on. Note that the value of:alist isnil for all calls after the first.:translate (defaultnil )

indicates whether or not terms in the input are to be translated or not (see term for a discussed of ``translate''). If the value isnil then translation will not take place, so the given terms — not only the input term, but also terms in thecdr positions of the:alist and terms in the:hyps — should already be in translated form. But if the value is notnil , then all of these will be translated.:untranslate (defaultnil )

indicates whether the rewritten term will be given in translated or untranslated form. It also specifies, when notnil , that certain error messages display terms in untranslated form.

The eight hint options displayed above are the same as discussed in the
documentation topic, hints. These are the only legal hint keywords for

The ``advanced options''

Here we provide a brief summary of the algorithm used by

Not surprisingly, the primary simplification technique used by

Initially, a function called

Replace term with its rewrite with respect to the alist, hyps, fc-pair-lst, and pot-lst. If the alist is empty and the term didn't change, exit the loop.

See rewrite$-hyps for a tool that rewrites a list of hypotheses.
That tool does more than just apply rewriting directly to each hypothesis: it
also uses forward-chaining and linear-arithmetic derived from
the hypotheses. A related tool rewrite$-context, is similar but takes
an ``

For related tools see expander and easy-simplify-term. In
particular, code from the expander function