simplify the current subterm
Major Section: PROOF-CHECKER-COMMANDS
Examples: S -- simplify the current subterm (S :backchain-limit 2 :normalize t :expand (append x z)) -- simplify the current subterm, but during the rewriting process first ``normalize'' it by pushing IFs to the top-level, and also force the term (append x z) to be expanded during the rewriting process General Form: (s &key rewrite normalize backchain-limit repeat in-theory hands-off expand)Simplify the current subterm according to the keyword parameters supplied. First if-normalization is applied (unless the
nil), i.e., each subterm of the form
(f ... (if test x y) ...)is replaced by the term
(if test (f ... x ...) (f ... y ...))except, of course, when
ifand the indicated
ifsubterm is in the second or third argument position. Then rewriting is applied (unless the rewrite argument is
nil). Finally this pair of actions is repeated -- until the rewriting step causes no change in the term. A description of each parameter follows.
:rewrite -- default tWhen non-
nil, instructs the system to use ACL2's rewriter (or, something close to it) during simplification.
:normalize -- default tWhen non-
nil, instructs the system to use if-normalization (as described above) during simplification.
:backchain-limit -- default 0Sets the number of recursive calls to the rewriter that are allowed for backchaining. Even with the default of 0, some reasoning is allowed (technically speaking, type-set reasoning is allowed) in the relieving of hypotheses. The value should be
nilor a non-negative integer, and limits backchaining only for rewriting, not for type-set reasoning.
:repeat -- default 0Sets the number of times the current term is to be rewritten. If this value is
t, then the default is used (as specified by the constant
:in-theory, :hands-off, :expandThese have their usual meaning; see hints.
Remark: if conditional rewrite rules are used that cause case splits
because of the use of
force, then appropriate new subgoals will be
created, i.e., with the same current subterm (and address) but with
each new (forced) hypothesis being negated and then used to create a
corresponding new subgoal. In that case, the current goal will have
all such new hypotheses added to the list of top-level hypotheses.