ACL2-PC::GENERALIZE

(primitive) 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).