An object denoting an instance of a theorem

Lemma instances are the objects one provides via

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

or

: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

(1)

(2) `corollary` justifying the rule named by the rune.

(3)

(4) `symbol-name` as

(5) `not`, `member`, `implies`, and `o<`, and a few others, as listed by the constant
*a
priori* relation is imposed between the `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 `encapsulate` event
that either has a non-empty signature list or is ``empty'' (stores
no events), and then avoids re-proving that constraint in future events.

See functional-instantiation-example for an example of the use of

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

(6)

Consider the application of `mutual-recursion`. Suppose
that

Finally, note that an optional second argument to

(7)

Obscure case for definitions. If the lemma instance refers to a
`corollary` formula
of that rune, which can be a normalized (simplified) form of the definition
body; see normalize. However, if the hint is a `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

We conclude with remarks on (6) and (7). The termination theorem actually
used is an unsimplified version of what was originally proved for the
indicated function; the guard theorem is, by default, partially simplified.
That is: while in general, the termination theorem is simplified before being
given to the prover, nevertheless the unsimplified theorem is what is actually
used for `measure-debug` and `guard-debug` keywords for `xargs` are ignored when generating the termination or guard theorem. You can
see the termination or guard theorem for an existing function symbol `fmt`; see msg.

Also see make-termination-theorem.

Why do we avoid simplification for `make-event`. For now, by avoiding simplification we guarantee that the
theorem we are using is truly a theorem. The theorem being used might not be
exactly the theorem originally proved, for example because of the use of case-split-limitations, which depends on the current logical world;
but we expect the two theorems to be logically equivalent.

- Termination-theorem-example
- How to use a previously-proved measure theorem
- Guard-theorem-example
- How to use a previously-proved guard theorem
- Guard-theorem
- Use a previously-proved guard theorem
- Termination-theorem
- Use a (functional instance of a) previously-proved measure theorem