## GENERALIZE

make a rule to restrict generalizations
Major Section: RULE-CLASSES

See rule-classes for a general discussion of rule classes, including how they
are used to build rules from formulas and a discussion of the various
keywords in a rule class description.

Example:
(defthm integer-listp-rev
(implies (integer-listp x)
(integer-listp (rev x)))
:rule-classes :generalize)
General Form:
any theorem

To use a `:generalize`

rule, the system waits until it has decided to
generalize some term, `term`

, by replacing it with some new variable `v`

.
If any `:generalize`

formula can be instantiated so that some non-variable
subterm becomes `term`

, then that instance of the formula is added as a
hypothesis. Thus for the example above, if the term `(rev x2)`

is
generalized to the variable `rv`

during a proof, then the following is
added as a hypothesis when generalizing to a new goal.
(implies (integer-listp x2)
(integer-listp rv))

At the moment, the best description of how ACL2 `:generalize`

rules
are used may be found in the discussion of ``Generalize Rules,'' page
248 of A Computational Logic Handbook, or ``Generalization,'' page
132 of ``Computer-Aided Reasoning: An Approach.'' Also
see introduction-to-the-theorem-prover for detailed tutorial on using ACL2
to prove theorems, which includes some discussion of generalization.