ACL2-pc::s
(primitive)
simplify the current subterm
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, normalization, which will push 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 linear normalize backchain-limit repeat in-theory hands-off
expand)
Simplify the current subterm according to the keyword parameters supplied.
First normalization is applied (unless the :normalize argument is
nil), so that for example, 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 f is if and the indicated if
subterm is in the second or third argument position. See normalize for
details. 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 t
When non-nil, instructs the system to use ACL2's rewriter (or,
something close to it) during simplification.
:linear -- default t (except, default nil if :rewrite has value nil)
When non-nil, instructs the system to use ACL2's linear arithmetic to build a suitable context (a
``linear pot list'') from the assumptions
(the top-level hypotheses and the governors). Note that linear arithmetic is used by the
rewriter regardless; by default, when :s invokes the rewriter then linear
arithmetic can take advantage of the information in the top-level hypotheses
and the governors.
:normalize -- default t
When non-nil, instructs the system to use normalization (as
described above) during simplification.
:backchain-limit -- default 0
Sets 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 reasoning
is allowed) in the relieving of hypotheses. The value should be nil or a
non-negative integer, and limits backchaining only for rewriting, not for type
reasoning.
:repeat -- default 0
Sets 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
*default-s-repeat-limit*).
:in-theory, :hands-off, :expand
These 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.
