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))))Observe that an event name can be a lemma instance. The

`:use`

hint
allows a single lemma instance to be provided in lieu of a list, as
in:
:use reverse-reverseor

: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`

.

(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 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. 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) that
contains `v`

as a variable. This is our draconian restriction to
avoid capture. If you happen to violate this restriction by
choosing a `v`

that does occur, say in one of the relevant
constraints, an informative error message will be printed. That
message will list for you the 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 undertake to prove that the
`gi`

's satisfy the constraints (see constraint) on the
`fi`

's. One might expect that if the same instantiated constraint
were generated on behalf of multiple 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.

See functional-instantiation-example for an example of the use
of `:functional-instance`

(so-called ``functional instantiation).''