Generalize
Make a rule to restrict generalizations
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.
