perform a generalization
Major Section: PROOF-CHECKER-COMMANDS
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
proof-checker state.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-checker 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-checker 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).
