Major Section: RULE-CLASSES

See rule-classes for a general discussion of rule classes and
how they are used to build rules from formulas. An example
`:`

`corollary`

formula from which an `:elim`

rule might be built is:

Example: (implies (consp x) when (car v) or (cdr v) appears (equal (cons (car x) (cdr x)) in a conjecture, and v is a x)) variable, consider replacing v by (cons a b), for two new variables a and b.General Form: (implies hyp (equiv lhs x))

where `equiv`

is a known equivalence relation See defequiv, `x`

is a variable symbol and `lhs`

contains one or more terms (called
``destructor terms'') of the form `(fn v1 ... vn)`

, where `fn`

is
a function symbol and the `vi`

are distinct variable symbols,
`v1`

, ..., `vn`

include all the variable symbols in the formula,
no `fn`

occurs in `lhs`

in more than one destructor term, and all
occurrences of `x`

in `lhs`

are inside destructor terms.

To use an `:elim`

rule, the theorem prover waits until a conjecture
has been maximally simplified. If it then finds an instance of some
destructor term `(fn v1 ... vn)`

in the conjecture, where the instance
for `x`

is some variable symbol, `vi`

, and every occurrence of `vi`

outside the destructor terms is in an `equiv`

-hittable position, then
it instantiates the `:elim`

formula as indicated by the destructor term
matched, splits the conjecture into two goals, according to whether the
instantiated hypothesis, `hyp`

, holds, and in the case that it does,
generalizes all the instantiated destructor terms in the conjecture to
new variables and then replaces `vi`

in the conjecture by the generalized
instantiated `lhs`

. An occurrence of `vi`

is ```equiv`

-hittable''
if sufficient congruence rules (see defcong) have been proved to establish
that the propositional value of the clause is not altered by replacing that
occurrence of `vi`

by some `equiv`

-equivalent term.

If an `:elim`

rule is not applied when you think it should have been,
and the rule uses an equivalence relation, `equiv`

, other than `equal`

,
it is most likely that there is an occurrence of the variable that is not
`equiv`

-hittable. Easy occurrences to overlook are those in
in the governing hypotheses. If you see an unjustified occurrence of the
variable, you must prove the appropriate congruence rule to allow the
`:elim`

to fire.

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

rules are used
may be found in the discussion of ``ELIM Rules,'' pp 247 of A
Computational Logic Handbook.