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 theoremTo use a
:generalizerule, the system waits until it has decided to generalize some term,
term, by replacing it with some new variable
v. If any
:generalizeformula 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
rvduring 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
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.