ACL2-pc::generalize
(primitive)
perform a generalization
Example:
(generalize
((and (true-listp x) (true-listp y)) 0)
((append x y) w))
General Form:
(generalize &rest substitution)
Generalize using the indicated substitution, which should be a non-empty
list. Each element of that list should be a two-element list of the form
(term variable), where term may use abbreviations. The effect of
the instruction is to replace each such term in the current goal by the
corresponding variable. This replacement is carried out by a parallel
substitution, outside-in in each hypothesis and in the conclusion. More
generally, actually, the ``variable'' (second) component of each pair may be
nil or a number, which causes the system to generate a new name of the
form _ or _n, with n a natural number; more on this below.
However, when a variable is supplied, it must not occur in any goal of the
current state of the interactive proof-builder.
When the ``variable'' above is nil, the system will treat it as the
variable |_| if that variable does not occur in any goal of the current
proof-builder state. Otherwise it treats it as |_0|, or |_1|, or
|_2|, and so on, until one of these is not among the variables of the
current proof-builder state. If the ``variable'' is a non-negative integer
n, then the system treats it as |_n| unless that variable already
occurs among the current goals, in which case it increments n just as above
until it obtains a new variable.
Remark: The same variable may not occur as the variable component of
two different arguments (though nil may occur arbitrarily many times, as
may a positive integer).
