LEMMA-INSTANCE

Major Section:  MISCELLANEOUS

Lemma instances are the objects one provides via :use and :by hints (see hints) to bring to the theorem prover's attention some previously proved or easily provable fact. A typical use of the :use hint is given below. The value specified is a list of five lemma instances.

:use (reverse-reverse
      (:type-prescription app)
      (:instance assoc-of-app
                 (x a) (y b) (z c))
      (:functional-instance p-f
                            (p consp) (f flatten))
      (:instance (:theorem (equal x x))
                 (x (flatten a))))

:use reverse-reverse

:use (:instance assoc-of-app (x a) (y b) (z c))

A lemma instance denotes a formula which is either known to be a theorem or which must be proved to be a theorem before it can be used. To use a lemma instance in a particular subgoal, the theorem prover adds the formula as a hypothesis to the subgoal before the normal theorem proving heuristics are applied.

A lemma instance, or lmi, is of one of the following five forms:

(1) name, where name names a previously proved theorem, axiom, or definition and denotes the formula (theorem) of that name.

(2) rune, where rune is a rune (see rune) denoting the :corollary justifying the rule named by the rune.

(3) (:theorem term), where term is any term alleged to be a theorem. Such a lemma instance denotes the formula term. But before using such a lemma instance the system will undertake to prove term.

(4) (:instance lmi (v1 t1) ... (vn tn)), where lmi is recursively a lemma instance, the vi's are distinct variables and the ti's are terms. Such a lemma instance denotes the formula obtained by instantiating the formula denoted by lmi, replacing each vi by ti. Normally ACL2 enforces the requirement that every variable vi must be bound in the formula denoted by lmi. However, the keyword :extra-bindings-ok may be inserted immediately after the lemma instance in order to remove that requirement: (:instance lmi :extra-bindings-ok (v1 t1) ... (vn tn)).

(5) (:functional-instance lmi (f1 g1) ... (fn gn)), where lmi is recursively a lemma instance and each fi is an ``instantiable'' function symbol of arity ni and gi is a function symbol, a macro alias for a function symbol gi' (see macro-aliases-table) in which case we treat gi as gi', or a pseudo-lambda expression of arity ni. An instantiable function symbol is any defined or constrained function symbol except the primitives not, member, implies, and o<, and a few others, as listed by the constant *non-instantiable-primitives*. These are built-in in such a way that we cannot recover the constraints on them. (Special case: a function introduced in the :partial-theory of a dependent clause-processor is not instantiable; see define-trusted-clause-processor.) A pseudo-lambda expression is an expression of the form (lambda (v1 ... vn) body) where the vi are distinct variable symbols and body is any term. No a priori relation is imposed between the vi and the variables of body, i.e., body may ignore some vi's and may contain ``free'' variables. However, we do not permit v to occur freely in body if the functional substitution is to be applied to any formula (lmi or the constraints to be satisfied) in a way that inserts v into the scope of a binding of v by let or mv-let (or, lambda). If you happen to violate this restriction, an informative error message will be printed. That message will list for you the potentially illegal choices for v in the context in which the functional substitution is offered. A :functional-instance lemma instance denotes the formula obtained by functionally instantiating the formula denoted by lmi, replacing fi by gi. However, before such a lemma instance can be used, the system will generate proof obligations arising from the replacement of the fi's by the gi's in constraints that ``support'' the lemma to be functionally instantiated; see constraint. One might expect that if the same instantiated constraint were generated on behalf of several events, then each of those instances would have to be proved. However, for the sake of efficiency, ACL2 stores the fact that such an instantiated constraint has been proved and avoids it in future events.

Note that ACL2(r) (see real) imposes additional requirements for functional instantiation. See functional-instantiation-in-acl2r.

Obscure case for definitions. If the lemma instance refers to a :definition rune, then it refers to the corollary formula of that rune, which can be a simplified (``normalized'') form of the original formula. However, if the hint is a :by hint and the lemma instance is based on a name (i.e., a symbol), rather than a rune, then the formula is the original formula of the event, as shown by :pe, rather than the normalized version, as shown by :pf. This is as one would expect: If you supply the name of an event, you expect it to refer to the original event. For :use hints we use the simplified (normalized) form instead, which is reasonable since one would expect simplification during the proof that re-traces the normalization done at the time the rule was created.

See functional-instantiation-example for an example of the use of :functional-instance (so-called ``functional instantiation).''