Rewrite-lambda-objects-theory
how to specify rewriting of lambda objects
The enabled status of two rewrite-lambda-modep runes are used
as flags to determine the action taken when eligible lambda objects are
encountered by the ACL2 rewriter. See rewrite-lambda-object and
rewrite-lambda-object-actions. To make the rewriter dive into the
body of an eligible lambda object, both (:executable-counterpart
rewrite-lambda-modep) and (:definition rewrite-lambda-modep) must be
enabled in the then-current theory. The 0-ary function
rewrite-lambda-objects-theory returns such a theory.
In fact, diving into eligible quoted lambda object constants to
rewrite the body is the default action when ACL2 starts up. See rewriting-versus-cleaning-up-lambda-objects for why you might want to change
the default action when eligible lambda objects are encountered by the
rewriter.
The expression (rewrite-lambda-objects-theory) macroexpands to the
theory expression
(e/d ((:executable-counterpart rewrite-lambda-modep)
(:definition rewrite-lambda-modep))
nil)
which is a theory equal to then current theory except that the
executable-counterpart rune and the definition rune of
rewrite-lambda-modep are enabled. This expansion is suitable for use in
an in-theory event or :in-theory hint (see :hints).
Both these two runes are initally enabled, so eligible lambda object
bodies are rewritten by default until and unless some event (e.g., an in-theory or include-book) or a superior local subgoal hint changes
the status of those runes.
For example, if lambda object rewriting has been disabled globally
and you wish to enable it for Subgoal 3 of some proof, you could use
the :hints
("Subgoal 3"
:in-theory (rewrite-lambda-objects-theory))
Note that if you also wish to enable or disable other runes in the same
subgoal you must construct an appropriate theory.
For example, if in Subgoal 3 of some proof you wanted to enable
LEMMA1 and disable LEMMA2 in a theory that will also allow
rewriting of lambda objects, you might write
("Subgoal 3"
:in-theory (set-difference-theories
(union-theories (rewrite-lambda-objects-theory)
'(LEMMA1))
'(LEMMA2)))
Some users might prefer
("Subgoal 3"
:in-theory (e/d ((:executable-counterpart rewrite-lambda-modep)
(:definition rewrite-lambda-modep)
LEMMA1)
(LEMMA2)))
See theories for general information about theories and how to
create and use them.
