equiv, rewrite, and s.
expand and (maybe) simplify function call at the current subterm
Major Section: PROOF-CHECKER-COMMANDS
Examples: x -- expand and simplify.For example, if the current subterm is (append a b), then after
x
the current subterm will probably be (cons (car a) (append (cdr a)
b)) if (consp a) and (true-listp a) are among the top-level
hypotheses and governors. If there are no top-level hypotheses and
governors, then after x the current subterm will probably be:
(if (true-listp x)
(if x
(cons (car x) (append (cdr x) y))
y)
(apply 'binary-append (list x y))).
General Form:
(X &key
rewrite normalize backchain-limit in-theory hands-off expand)
Expand the function call at the current subterm, and simplify
using the same conventions as with the s command (see documentation
for s).
Unlike s, it is permitted to set both :rewrite and :normalize to
nil, which will result in no simplification; see x-dumb.
Note (obscure): On rare occasions the current address may be
affected by the use of x. For example, suppose we have the
definition
(defun g (x) (if (consp x) x 3))and then we enter the proof-checker with
(verify (if (integerp x) (equal (g x) 3) t)) .Then after invoking the instruction
(dive 2 1), so that the
current subterm is (g x), followed by the instruction x, we would
expect the conclusion to be (if (integerp x) (equal 3 3) t).
However, the system actually replaces (equal 3 3) with t (because we
use the ACL2 term-forming primitives), and hence the conclusion is
actually (if (integerp x) (equal 3 3) t). Therefore, the current
address is put at (2) rather than (2 1). In such cases, a warning
``NOTE'' will be printed to the terminal.
The other primitive commands to which the above ``truncation'' note
applies are equiv, rewrite, and s.