		Search-engine friendly clone of the ACL2 documentation.

Rewrite

Rewrite-lambda-object-actions

actions available when rewriting lambda objects

As explained in rewrite-lambda-object the rewriter can be applied to eligible occurrences of quoted lambda objects. That documentation also describes eligibility, what happens during, and what happens after the specified action, with a focus on recursively rewriting the lambda body. This topic discusses how to specify the desired action.

The user can specify one of three actions by manipulating the enabled status of the rune (:executable-counterpart rewrite-lambda-modep) and the enabled status of (:definition rewrite-lambda-modep). Recall that such runes can be abbreviated (:e rewrite-lambda-modep) and (:d rewrite-lambda-modep). But in this discussion, we'll abbreviate them still further by e and d, respectively.

The actions available on the body of an eligible lambda object occurrence are

rewrite: e and d enabled
syntactically clean: e enabled and d disabled
hands-off (no action): e disabled

Since the action is determined by the enabled status of runes, it can be specified by the user by appropriate global in-theory events or by goal-specific, local :in-theory :hints. There are three 0-ary macros that expand into appropriate theories provided the only runes you wish to affect are our so-called e and d.

The three macros are rewrite-lambda-objects-theory, syntactically-clean-lambda-objects-theory, and hands-off-lambda-objects-theory, with the obvious meanings. For example, (syntactically-clean-lambda-objects-theory) macroexpands to

(e/d ((:executable-counterpart rewrite-lambda-modep))   ; enable ``e''
     ((:definition rewrite-lambda-modep)))              ; disable ``d''

Since e and d are both initially enabled in ACL2, eligible lambda objects are rewritten by default unless you change the status of e and/or d.

For example, to make the prover just syntactically clean eligible lambda objects in Subgoal 3 of some proof attempt you could provide the :hint

("Subgoal 3"
  :in-theory (syntactically-clean-lambda-objects-theory))

Note however that if you also need to adjust the status of some other rune in that same hint you must create a theory expression that includes the appropriate use of e and d. For example, to also enable LEMMA1 but disable LEMMA2 while specifying use of syntactic cleaning you could write:

("Subgoal 3"
 :in-theory (e/d ((:executable-counterpart rewrite-lambda-modep)
                  LEMMA1)
                 ((:definition rewrite-lambda-modep)
                  LEMMA2)))

For details on what syntactic cleaning is and why it is sometimes useful, see rewriting-versus-cleaning-up-lambda-objects.