Major Section: EVENTS

Example: (table term-table t '((binary-+ x y) '3 'nil (car x)))

See table for a general discussion of tables and the `table`

event used to manipulate tables.

The ```term-table`

'' is used at the time a meta rule is checked for
syntactic correctness. Each proposed metafunction is run on each
term in this table, and the result in each case is checked to make
sure that it is a `termp`

in the current world. In each case where
this test fails, a warning is printed.

Whenever a metafunction is run in support of the application of a
meta rule, the result must be a term in the current world. When the
result is not a term, a hard error arises. The `term-table`

is simply
a means for providing feedback to the user at the time a meta rule
is submitted, warning of the definite possibility that such a hard
error will occur at some point in the future.

The key used in `term-table`

is arbitrary. The top-most value is
always the one that is used; it is the entire list of terms to be
considered. Each must be a `termp`

in the current ACL2 world.

Major Section: EVENTS

Example: (theory-invariant (not (and (member-equal '(:rewrite left-to-right) theory) (member-equal '(:rewrite right-to-left) theory))))whereGeneral Forms: (theory-invariant term) ; conjoin a new invariant term or (theory-invariant term key) ; change an existing invariant term

`term`

is a term that uses no variables other than `theory`

and
`world`

, and `key`

is an arbitrary ``name'' for this invariant. If `key`

is omitted, an integer is generated and used. `Theory-invariant`

is
an event that adds to or modifies the table of user-supplied theory
invariants that are checked each time a theory expression is
evaluated.
The theory invariant mechanism is provided via a table
(see table) named `theory-invariant-table`

. In fact, the
`theory-invariant`

``event'' is just a macro that expands into a use
of the `table`

event. More general access to the `theory-invariant`

table is provided by `table`

itself. For example, the table can be
inspected or cleared (setting the invariant to `t`

) with `table`

.

`Theory-invariant-table`

maps arbitrary keys to terms mentioning, at
most, the variables `theory`

and `world`

. Every time an alleged theory
expression is evaluated, e.g., in the `in-theory`

event or `:`

`in-theory`

hint, each of the terms in `theory-invariant-table`

is evaluated with
`theory`

bound to the runic theory (see theories) obtained from
the theory expression and `world`

bound to the current ACL2 world
(see world). If the result is `nil`

, a warning message is
printed. Thus, the table can be thought of as a list of conjuncts.
Each `term`

in the table has a ``name,'' which is just the key under
which the term is stored. When a theory violates the restrictions
specified by some term, both the name and the term are printed. By
calling `theory-invariant`

with a new term but the same name, you can
overwrite that conjunct of the theory invariant.

Theory invariants are particularly useful in the context of large rule sets intended for re-use. Such sets often contain conflicting rules, e.g., rules that are to be enabled when certain function symbols are disabled, rules that rewrite in opposite directions and thus loop if simultaneously enabled, groups of rules which should be enabled in concert, etc. The developer of such rule sets understands these restrictions and probably documents them. The theory invariant mechanism allows the developer to codify his restrictions so that when they are violated the user is warned.

Since theory invariants are arbitrary terms, macros may be used to express commonly used restrictions. Because theory invariants are a new idea in ACL2, we have only defined one such macro for illustrative purposes. Executing the event

(theory-invariant (incompatible (:rewrite left-to-right) (:rewrite right-to-left)))would subsequently cause a warning message any time the current theory contained both of the two runes shown. Of course, incompatible is just defined as a macro. Its definition may be inspected with

`:pe incompatible`

.
Note: If the table event is used directly to `:put`

a term into the
theory invariant table, be aware that the term must be in translated
form. This is enforced by the `value`

invariant for
`theory-invariant-table`

. But the upshot of this is that you will be
unable to use macros in theory invariants stored directly with the
`:put`

table event.

Major Section: EVENTS

Examples: (verify-guards flatten) (verify-guards flatten :hints (("Goal" :use (:instance assoc-of-app))) :otf-flg t :doc "string")See guard for a general discussion of guards. In the General Form above,General Form: (verify-guards name :hints hints :otf-flg otf-flg :doc doc-string)

`name`

is the name of a `:`

`logic`

function
(see defun-mode) or of a theorem or axiom. In the most common
case `name`

is the name of a function that has not yet had its
guards verified, each
subroutine of which has had its guards verified. `hints`

and
`otf-flg`

are as described in the corresponding `:`

`doc`

entries;
and `doc-string`

, if supplied, is a string `:Doc-Section`

''. The three keyword arguments above are all
optional. `Verify-guards`

will attempt to prove that the guard on
the named function implies the guards of all of the subroutines
called in the body of the function. If successful, `name`

is
considered to have had its guards verified.
If `name`

is one of several functions in a mutually recursive clique,
`verify-guards`

will attempt to verify the guards of all of the
functions.

If `name`

is a theorem or axiom name, `verify-guards`

verifies the
guards of the associated formula. When a theorem has had its guards
verified then you know that the theorem will evaluate to non-`nil`

in all Common Lisps, without causing a runtime error (other than possibly
a resource error). In particular, you know that the theorem's validity
does not depend upon ACL2's arbitrary completion of the domains of partial
Common Lisp functions.

For example, if `app`

is defined as

(defun app (x y) (declare (xargs :guard (true-listp x))) (if (endp x) y (cons (car x) (app (cdr x) y))))then we can verify the guards of

`app`

and we can prove the theorem:
(defthm assoc-of-app (equal (app (app a b) c) (app a (app b c))))However, if you go into almost any Common Lisp in which

`app`

is defined
as shown and evaluate
(equal (app (app 1 2) 3) (app 1 (app 2 3)))we get an error or, perhaps, something worse like

`nil`

! How can
this happen since the formula is an instance of a theorem? It is supposed
to be true!
It happens because the theorem exploits the fact that ACL2 has completed
the domains of the partially defined Common Lisp functions like `car`

and `cdr`

, defining them to be `nil`

on all non-conses. The formula
above violates the guards on `app`

. It is therefore ``unreasonable''
to expect it to be valid in Common Lisp.

But the following formula is valid in Common Lisp:

(if (and (true-listp a) (true-listp b)) (equal (app (app a b) c) (app a (app b c))) t)That is, no matter what the values of

`a`

, `b`

and `c`

the formula
above evaluates to `t`

in all Common Lisps (unless the Lisp engine runs out
of memory or stack computing it). Furthermore the above formula is a theorem:
(defthm guarded-assoc-of-app (if (and (true-listp a) (true-listp b)) (equal (app (app a b) c) (app a (app b c))) t))This formula,

`guarded-assoc-of-app`

, is very easy to prove from
`assoc-of-app`

. So why prove it? The interesting thing about
`guarded-assoc-of-app`

is that we can verify the guards of the
formula. That is, `(verify-guards guarded-assoc-of-app)`

succeeds.
Note that it has to prove that if `a`

and `b`

are true lists then
so is `(app a b)`

to establish that the guard on the outermost `app`

on the left is satisfied. By verifying the guards of the theorem we
know it will evaluate to true in all Common Lisps. Put another way,
we know that the validity of the formula does not depend on ACL2's
completion of the partial functions or that the formula is ``well-typed.''
One last complication: The careful reader might have thought we could
state `guarded-assoc-of-app`

as

(implies (and (true-listp a) (true-listp b)) (equal (app (app a b) c) (app a (app b c))))rather than using the

`if`

form of the theorem. We cannot! The
reason is technical: `implies`

is defined as a function in ACL2.
When it is called, both arguments are evaluated and then the obvious truth
table is checked. That is, `implies`

is not ``lazy.'' Hence, when
we write the guarded theorem in the `implies`

form we have to prove
the guards on the conclusion without knowing that the hypothesis is true.
It would have been better had we defined `implies`

as a macro that
expanded to the `if`

form, making it lazy. But we did not and after
we introduced guards we did not want to make such a basic change.
Recall however that `verify-guards`

is almost always used to verify
the guards on a function definition rather than a theorem. We now
return to that discussion.

Because `name`

is not uniquely associated with the `verify-guards`

event
(it necessarily names a previously defined function) the
documentation string, `doc-string`

, is not stored in the
documentation data base. Thus, we actually prohibit `doc-string`

from having the form of an ACL2 documentation string;
see doc-string.

`Verify-guards`

must often be used when the value of a recursive call
of a defined function is given as an argument to a subroutine that
is guarded. An example of such a situation is given below. Suppose
`app`

(read ``append'') has a guard requiring its first argument to be
a `true-listp`

. Consider

(defun rev (x) (declare (xargs :guard (true-listp x))) (cond ((endp x) nil) (t (app (rev (cdr x)) (list (car x))))))Observe that the value of a recursive call of

`rev`

is being passed
into a guarded subroutine, `app`

. In order to verify the guards of
this definition we must show that `(rev (cdr x))`

produces a
`true-listp`

, since that is what the guard of `app`

requires. How do we
know that `(rev (cdr x))`

is a `true-listp`

? The most elegant argument
is a two-step one, appealing to the following two lemmas: (1) When `x`

is a `true-listp`

, `(cdr x)`

is a `true-listp`

. (2) When `z`

is a
`true-listp`

, `(rev z)`

is a `true-listp`

. But the second lemma is a
generalized property of `rev`

, the function we are defining. This
property could not be stated before `rev`

is defined and so is not
known to the theorem prover when `rev`

is defined.
Therefore, we might break the admission of `rev`

into three steps:
define `rev`

without addressing its guard verification, prove some
general properties about `rev`

, and then verify the guards. This can
be done as follows:

(defun rev (x) (declare (xargs :guard (true-listp x) :verify-guards nil)) ; Note this additional xarg. (cond ((endp x) nil) (t (app (rev (cdr x)) (list (car x))))))The ACL2 system can actually admit the original definition of(defthm true-listp-rev (implies (true-listp x2) (true-listp (rev x2))))

(verify-guards rev)

`rev`

, verifying the guards as part of the `defun`

event. The
reason is that, in this particular case, the system's heuristics
just happen to hit upon the lemma `true-listp-rev`

. But in many
more complicated functions it is necessary for the user to formulate
the inductively provable properties before guard verification is
attempted.
Major Section: EVENTS

Examples: (verify-termination fact) (verify-termination fact (declare (xargs :guard (and (integerp x) (>= x 0)))))whereGeneral Forms: (verify-termination fn dcl ... dcl) (verify-termination (fn1 dcl ... dcl) (fn2 dcl ... dcl) ...)

`fn`

and the `fni`

are function symbols having `:`

`program`

mode
(see defun-mode) and all of the `dcl`

s are either `declare`

forms or documentation strings. The first form above is an
abbreviation for
(verify-termination (fn dcl ... dcl))so we limit our discussion to the second form. Each of the

`fni`

must be in the same clique of mutually recursively defined
functions, but not every function in the clique need be among the
`fni`

.
`Verify-termination`

attempts to establish the admissibility of the
`fni`

. `Verify-termination`

retrieves their definitions, creates modified
definitions using the `dcl`

s supplied above, and resubmits these
definitions. You could avoid using `verify-termination`

by typing the new
definitions yourself. So in that sense, `verify-termination`

adds no new
functionality. But if you have prototyped your system in `:`

`program`

mode and tested it, you can use `verify-termination`

to resubmit your
definitions and change their defun-modes to `:`

`logic`

, addings
hints without having to retype or recopy the code. You can also add or
modify guards at this time.

The `defun`

command executed by `verify-termination`

is obtained
by retrieving the `defun`

(or `mutual-recursion`

) command that
introduced the clique in question and then possibly modifying each
definition as follows. Consider a function, `fn`

, in the clique.
If `fn`

is not among the `fni`

above, its definition is left
unmodified. Otherwise, `fn`

is some `fni`

and we modify its
definition by inserting into it the corresponding `dcl`

s listed
with `fni`

in the arguments to `verify-termination`

. In addition,
we throw out from the old declarations in `fn`

the `:mode`

specification and anything that is specified in the new `dcl`

s.

For example, suppose that `fact`

was introduced with:

(defun fact (n) (declare (type integer n) (xargs :mode :program)) (if (zp n) 1 (* n (fact (1- n))))).Suppose later we do

`(verify-termination fact)`

. Then the
following definition is submitted.
(defun fact (n) (declare (type integer n)) (if (zp n) 1 (* n (fact (1- n))))).Observe that this is the same definition as the original one, except the old specification of the

`:mode`

has been deleted so that the
defun-mode now defaults to `:`

`logic`

. Although the termination
proof succeeds, ACL2 also tries to verify the guard, because we have
(implicitly) provided a guard, namely `(integerp n)`

, for this
function. (See guard for a general discussion of guards, and
see type-spec for a discussion of how type declarations are
used in guards.) Unfortunately, the guard verification fails,
because the subterm `(zp n)`

requires that `n`

be nonnegative, as
can be seen by invoking `:args zp`

. (For a discussion of termination
issues relating to recursion on the naturals, see zero-test-idioms.)
So we might want to submit
(verify-termination fact (declare (xargs :guard (and (integerp n) (<= 0 n)))))which will submit the definition

(defun fact (n) (declare (xargs :guard (and (integerp n) (<= 0 n)))) (if (zp n) 1 (* n (fact (1- n))))).Observe that the declaration in the

`verify-termination`

command has
been inserted into the definition. In fact, this command succeeds.