ELIM

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.