This is documentation for ACL2 Version 3.2
Copyright (C) 2007  University of Texas at Austin

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

Written by:  Matt Kaufmann and J Strother Moore
Department of Computer Sciences
University of Texas at Austin
Austin, TX 78712-1188 U.S.A.

SET-MATCH-FREE-DEFAULT    provide default for :match-free in future rules

     General Forms:
     (set-match-free-default :once)
     (set-match-free-default :all)
     (set-match-free-default nil)

As described elsewhere (see FREE-VARIABLES), a rewrite, linear,
or forward-chaining rule may have free variables in its hypotheses, and
ACL2 can be directed either to try all bindings (":all") or just the
first (":once") when relieving that hypothesis, as a basis for
relieving subsequent hypotheses.  This direction of :all or :once is
generally provided by specifying either :match-free :once or
:match-free :all in the :rule-classes of the rule.  If neither of these
is specified, then the most recent set-match-free-default is used by
ACL2 to fill in this missing :match-free field.  See
RULE-CLASSES.  Except: If the last set-match-free-default specifies
nil, then ACL2 reverts to the behavior it had at start-up, as described
in Remarks (2) and (3) below.

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.  It
uses the acl2-defaults-table, and hence its effect is local to the book
or encapsulate form in which it occurs.

Remarks.

(1) The use of set-match-free-default has no effect on existing rules.
In order to change the behavior of existing rules with respect to
free-variable matching, see ADD-MATCH-FREE-OVERRIDE.

(2) If you submit a rewrite, linear, or forward-chaining rule with a
free variable in a hypothesis, and no default setting was previously
specified with set-match-free-default or the default setting is nil,
and the rule is not within a book being processed with include-book,
certify-book, or rebuild, then a warning or error is caused.  In order
to make this an error instead of a warning, see
SET-MATCH-FREE-ERROR.

(3) If you submit a rewrite, linear, or forward-chaining rule with a
free variable in a hypothesis, and no default setting has been
previously specified with set-match-free-default or the default setting
is nil, and no error is caused (see (2) above), then the default :all
is used.

SET-MATCH-FREE-ERROR    control error vs. warning when :match-free is missing

     Legal Forms:
     (set-match-free-error nil)
     :set-match-free-error nil
     (set-match-free-error t)
     :set-match-free-error t

As described elsewhere (see FREE-VARIABLES), when a rewrite,
linear, or forward-chaining rule has free variables in its hypotheses,
the user can specify whether to try all bindings (":all") or just the
first (":once") when relieving its hypotheses, as a basis for relieving
subsequent hypotheses.  This direction of :all or :once is generally
provided by specifying either :match-free :once or :match-free :all in
the :rule-classes of the rule.

But suppose that neither of these is specified, and that
set-match-free-default has not specified a default of :once or :all
(see SET-MATCH-FREE-DEFAULT).  In this case a warning will occur
except when in the context of include-book.  If you prefer to see an
error in such cases, except in the context of certify-book, execute
(set-match-free-error t).  If there is no error, then a default of :all
is used.

Note: This is NOT an event!  Instead, set-match-free-error sets the
state global 'match-free-error (see STATE and see
ASSIGN).  Thus, this form cannot be put into a book.  If you are
tempted to put it into a book, consider the fact that it really isn't
needed there, since the absence of :match-free does not cause an error
in the context of certify-book or include-book.  If you still feel the
need for such a form, consider using set-match-free-default to provide
a default, at least within the scope of the current book (if any); see
SET-MATCH-FREE-DEFAULT.

SET-MEASURE-FUNCTION    set the default measure function symbol

     Examples:
     (set-measure-function nqthm::count)

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.

     General Form:
     (set-measure-function name)

where name is a function symbol of one argument.  This macro is
equivalent to (table acl2-defaults-table :measure-function 'name), and
hence is local to any books and encapsulate events in which it occurs;
see ACL2-DEFAULTS-TABLE.  Although this is thus an event (see
TABLE), nevertheless no output results from a
set-measure-function event.

This event sets the default measure function to name.  Subsequently, if
a recursively defined function is submitted to defun with no explicitly
given :measure argument, defun "guesses" the measure (name var), where
name is the then current default measure function and var is the first
formal found to be tested along every branch and changed in every
recursive call.

Note that if (table acl2-defaults-table :measure-function 'name) has its
default value of nil, then the default measure function is acl2-count.

SET-NON-LINEARP    to turn on or off non-linear arithmetic reasoning

     Examples:
     (set-non-linearp t)
     (set-non-linearp nil)

See NON-LINEAR-ARITHMETIC.   This event is equivalent to (table
acl2-defaults-table :non-linearp <t-or-nil>), and hence is local to any
books and encapsulate events in which it occurs; see
ACL2-DEFAULTS-TABLE.

The initial value is nil.

SET-NU-REWRITER-MODE    to turn on and off the nu-rewriter

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.

This event sets a flag that controls whether the ACL2 rewriter uses the
special-purpose nth/update-nth rewriter (nu-rewriter).  The flag may
have one of three values: nil, t, or :literals.

     :set-nu-rewriter-mode nil        ; do not use nu-rewriter
     :set-nu-rewriter-mode t          ; use nu-rewriter in rewriting
     :set-nu-rewriter-mode :literals  ; use nu-rewriter in rewriting after
                                      ;  a pre-pass through every literal
     (set-nu-rewriter-mode :literals) ; same as above

The value nil prevents the use of the nu-rewriter.  The other two
values allow the use of the nu-rewriter.

When the flag is non-nil and the rewriter encounters a term that
"begins with an nth", the nu-rewriter is applied.  By "begins with an
nth" here we mean either the term is an application of nth or is an
application of some nonrecursive function or lambda expression whose
body contains an expression that begins with an nth.

Note that the use of the nu-rewriter here described above is driven by
the rewriter, i.e., the nu-rewriter is applied only to terms visited by
the rewriter in its inside-out sweep.  When the flag is set to
:literals the system makes a pre-pass through every goal clause and
applies the nu-rewriter to every subterm.  The rewriter is then used on
the output of that pre-pass.

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.
Moreover, its effect is to set the acl2-defaults-table, and hence its
effect is local to the book or encapsulate form containing it; see
ACL2-DEFAULTS-TABLE.

We expect to write more documentation as we gain experience with the
nu-rewriter.

SET-REWRITE-STACK-LIMIT    Sets the rewrite stack depth used by the rewriter

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.

     Example Forms:
     (set-rewrite-stack-limit 30)                            ; set to small limit
     :set-rewrite-stack-limit 30                             ; same as above
     (set-rewrite-stack-limit *default-rewrite-stack-limit*) ; the default
     :set-rewrite-stack-limit (1- (expt 2 28))               ; maximum legal limit
     :set-rewrite-stack-limit nil         ; same as above -- essentially, no limit

This event sets the maximum stack depth for calls of certain functions
that implement the ACL2 rewriter; see REWRITE-STACK-LIMIT.  It
must be a non-negative integer less than 2^28.  A call
(set-rewrite-stack-limit limit) is equivalent to:

     (table acl2-defaults-table :rewrite-stack-limit limit).

The use of acl2-defaults-table ensures that this event's effect is
implicitly local to the book or encapsulate form in which it occurs.

For a different but somewhat related concept, see
BACKCHAIN-LIMIT.

SET-STATE-OK    allow the use of STATE as a formal parameter

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.

In brief:  The variable symbol STATE has an unusual status in ACL2.  In
order to use it, you either need to issue :set-state-ok t, as we
explain below, or you need to declare it to be a stobj, as explained
elsewhere (see DECLARE-STOBJS).  Now we explain in more detail.

Because the variable symbol STATE denotes the "current ACL2 state,"
ACL2 treats the symbol very restrictively when it occurs as a formal
parameter of a defined function.  The novice user, who is unlikely to
be aware of the special status of that symbol, is likely to be confused
when error messages about STATE are printed in response to the innocent
choice of that symbol as a formal variable.  Therefore the top-level
ACL2 loop can operate in a mode in which STATE is simply disallowed as
a formal parameter.

For a discussion of STATE, See STATE and see STOBJ.
Roughly speaking, at the top-level, the "current ACL2 state" is denoted
by the variable symbol STATE.  Only the current state may be passed
into a function expecting a state as an argument.  Furthermore, the
name of the formal parameter into which the current state is passed
must be STATE and nothing but the current state may be passed into a
formal of that name.  Therefore, only certain access and change
functions can use that formal - namely with a STATE formal - and if any
such function produces a new state it becomes the "current state" and
must be passed along in the STATE position thereafter.  Thus, ACL2
requires that the state be single-threaded.  This, in turn, allows us
to represent only one state at a time and to produce new states from it
destructively in a von Neumaneque fashion.  The syntactic restrictions
on the variable STATE are enforced by the translate mechanism (see
TRANS and see TERM) when terms are read.

To prevent the novice user from seeing messages prohibiting certain
uses of the variable symbol STATE ACL2 has a mode in which it simply
disallows the use of that symbol as a formal parameter.  Use of the
symbol causes a simple error message.  The system is initially in that
mode.

To get out of that mode, execute:

     :set-state-ok t ;;; or, (set-state-ok t)

It is not recommended that you do this until you have read the
documentation of STATE.

To enter the mode in which use of state is prohibited as a formal
parameter, do:

     :set-state-ok nil

The mode is stored in the defaults table, See
ACL2-DEFAULTS-TABLE.  Thus, the mode may be set locally in books.

SET-VERIFY-GUARDS-EAGERNESS    the eagerness with which guard verification is tried.

     Example Forms:                        try guard verification?
     (set-verify-guards-eagerness 0) ; no, unless :verify-guards t
     (set-verify-guards-eagerness 1) ; yes if a :guard is supplied
     (set-verify-guards-eagerness 2) ; yes, unless :verify-guards nil

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.

     General Form:
     (set-verify-guards-eagerness n)

where n is a variable-free term that evaluates to 0, 1, or 2.  This
macro is essentially equivalent to

     (table acl2-defaults-table :verify-guards-eagerness n)

and hence is local to any books and encapsulate events in which it
occurs; see ACL2-DEFAULTS-TABLE.  However, unlike the above
simple call of the table event function (see TABLE), no output
results from a set-verify-guards-eagerness event.

Set-verify-guards-eagerness may be thought of as an event that merely
sets a flag to 0, 1, or 2.  The flag is used by certain defun events to
determine whether guard verification is tried.  The flag is irrelevant
to those defun events in :program mode and to those defun events in
which an explicit :verify-guards setting is provided among the xargs.
In the former case, guard verification is not done because it can only
be done when logical functions are being defined.  In the latter case,
the explicit :verify-guards setting determines whether guard
verification is tried.  So consider a :logic mode defun in which no
:verify-guards setting is provided.  Is guard verification tried?  The
answer depends on the eagerness setting as follows.  If the eagerness
is 0, guard verification is not tried.  If the eagerness is 1, it is
tried iff a :guard is explicitly provided in the defun.  If the
eagerness is 2, guard verification is tried.

The default behavior of the system is as though the
:verify-guards-eagerness is 1.  The current behavior can be ascertained
by evaluating the form (default-verify-guards-eagerness (w state)).

SET-WELL-FOUNDED-RELATION    set the default well-founded relation

     Examples:
     (set-well-founded-relation lex2)

provided lex2 has been proved to be a well-founded relation (see
WELL-FOUNDED-RELATION).  Note: This is an event!  It does not print
the usual event summary but nevertheless changes the ACL2 logical world
and is so recorded.

     General Form:
     (set-well-founded-relation rel)

where rel has been proved to be a well-founded relation on objects
satisfying some predicate, mp; see WELL-FOUNDED-RELATION.  This
macro is equivalent to (table acl2-defaults-table
:well-founded-relation 'rel), and hence is local to any books and
encapsulate events in which it occurs; see ACL2-DEFAULTS-TABLE.

This event sets the default well-founded relation to be that imposed on
mp-measures by the relation rel.  Subsequently, if a recursively
defined function is submitted to defun with no explicitly given
:well-founded-relation argument, defun uses the default relation, rel,
and the associated domain predicate mp used in its well-foundedness
theorem.  That is, the termination conditions generated will require
proving that the measure used by the defun is an mp-measure and that in
every recursive call the measure of the arguments decreases according
to rel.

TERM-TABLE    a table used to validate meta rules

     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.

USER-DEFINED-FUNCTIONS-TABLE    an advanced table used to replace certain system functions

     Examples:
     (table user-defined-functions-table 'untranslate-preprocess 'my-preprocess)
     (table user-defined-functions-table 'untranslate 'my-untranslate)

This feature should perhaps only be used by advanced users who have a
thorough understanding of the system functions being replaced.  There
are currently two ways a user can affect the way ACL2 prints terms.

The first example associates the user-defined function symbol
my-preprocess with untranslate-preprocess.  As a result, when ACL2
prints a term, say during a proof, using its so-called "untranslate"
process the first thing it does is to call my-preprocess on two
arguments: that term and the current ACL2 logical world.  If the call
produces a non-nil result, then that result is passed to the untranslate
process.

The second example associates the user-defined function symbol
my-untranslate with the built-in function symbol untranslate.  As a
result, the code for my-untranslate will be run whenever the untranslate
process is run.  The formals of the two functions must agree and must
not contain any stobj names.  Note that these overrides fail to occur
upon guard violations and some other evaluation errors.

The untranslate-preprocess approach may suffice for most cases in which
a user wants to modify the way output is produced by the theorem
prover.  We present an example immediately below, but see
books/misc/untranslate-patterns.lisp for a more elaborate example.  If
the untranslate-preprocess approach does not seem sufficient for your
purposes, you are invited to look at file
books/misc/rtl-untranslate.lisp for an example of user-defined
untranslate (i.e., following the second example displayed above).

Suppose you have a large constant that you would prefer not to see in
proofs.  For example, you may have submitted the following definition
(but imagine a much larger constant, say, a list of length 1,000,000).

     (defconst *a* '(a b c d))

If you submit the following (silly) theorem

     (thm (equal (cons x *a*) (car (cons yyy zzz))))

then you will see the following output:

     (EQUAL (CONS X '(A B C D)) YYY).

If *a* had represented a much larger structure, we would wish we could
see the following instead.

     (EQUAL (CONS X *A*) YYY)

That can be accomplished as follows.  First we make the following
definition.

     (defun my-preprocess (term wrld)
       (declare (ignore wrld))
       (if (equal term (list 'quote *a*))
           '*a*
         term))

Now we submit the following table event.

     (table user-defined-functions-table
            'untranslate-preprocess
            'my-preprocess)

This will install my-preprocess as a preprocessor before the normal
untranslation routine is applied to printing a term.  When the
untranslation routine encounters the constant (QUOTE (A B C D)), it
will replace it with *a*, and the usual untranlation routine will print
this as *A*.

WITH-OUTPUT    suppressing or turning on specified output for an event

     Example:
     (with-output
        :off summary ; turn off the event summary when evaluating the following:
        (in-theory (disable name)))

     General Form:
     (with-output :key1 val1 ... :keyk valk form)

where each :keyi is either :off or :on and either vali is either :all
or else a symbol or non-empty list of symbols representing output types
that can be inhibited (see SET-INHIBIT-OUTPUT-LST).  The result
of evaluating the General Form above is to evaluate form, but in an
environment where the current set of inhibited output types is
modified: if :on :all is specified, then all output is turned on except
as specified by :off; else if :off :all is specified, then all output
is inhibited except as specified by :on; and otherwise, the
currently-inhibited output types are reduced as specified by :on and
then extended as specified by :off.

Warning: With-output has no effect in raw Lisp, and hence is disallowed
in function bodies.  However, you can probably get the effect you want
as illustrated below, where <form> must return an error triple (mv erp
val state); see LD.

     Examples avoiding with-output, for use in function definitions:

     ; Inhibit all output:
     (state-global-let*
      ((inhibit-output-lst *valid-output-names*))
      <form>)

     ; Inhibit all warning output:
     (state-global-let*
      ((inhibit-output-lst
        (union-eq (f-get-global 'inhibit-output-lst state)
                  '(warning warning!))))
      <form>)

TABLE    user-managed tables

     Examples:
     (table tests 1 '(...))                ; set contents of tests[1] to '(...)
     (table tests 25)                      ; get contents of tests[25]
     (table tests)                         ; return table tests as an alist
     (table tests nil nil :clear)          ; clear table tests
     (table tests nil '((foo . 7)) :clear) ; set table tests to (foo 7)
     (table tests nil nil :guard)          ; fetch the table guard
     (table tests nil nil :guard term)     ; set the table guard

     General Form:
     (table table-name key-term value-term op term)

where table-name is a symbol that is the name of a (possibly new)
table, key-term and value-term, if present, are arbitrary terms
involving (at most) the single variable world, op, if present, is one
of the table operations below, and term, if present, is a term.  Table
returns an acl2 "error triple." The effect of table on state depends on
op and how many arguments are presented.  Some invocations actually
have no effect on the ACL2 world and hence an invocation of table is
not always an "event".  We explain below, after giving some background
information.

Important Note:  The table forms above are calls of a macro that expand
to involve the special variable state.  This will prevent you from
accessing a table from within a hint or theory where where you do not
have the state variable.  However, the form

     (table-alist 'tests world)

returns the alist representation of the table named test in the given
world.  Often you have access to world.

The ACL2 system provides "tables" by which the user can associate one
object with another.  Tables are in essence just conventional
association lists -- lists of pairs -- but the ACL2 environment
provides a means of storing these lists in the "ACL2 world" of the
current state.  The ACL2 user could accomplish the same ends by using
ACL2 "global variables;" however, limitations on global variable names
are imposed to ensure ACL2's soundness.  By convention, no table is
important to ACL2's soundness, even though some features of the system
use tables, and the user is invited to make free use of tables.
Because tables are stored in the ACL2 world they are restored by
include-book and undone by :ubt.  Many users of Nqthm requested a
facility by which user data could be saved in Nqthm "lib files" and
tables are ACL2's answer to that request.

Abstractly, each table is an association list mapping "keys" to
"values." In addition, each table has a ":guard," which is a term that
must be true of any key and value used.  By setting the :guard on a
table you may enforce an invariant on the objects in the table, e.g.,
that all keys are positive integers and all values are symbols.  Each
table has a "name," which must be a symbol.  Given a table name, there
are six operations one might perform on the table.

:put -- associate a value with a key (possibly changing the value
currently associated with that key).

:get -- retrieve the value associated with a key (or nil if no value
has been associated with that key).

:alist -- return an alist showing all keys and non-nil values in the
table.

:clear -- clear the table (so that every value is nil), or if val is
supplied then set table to that value (which must be an alist).

:guard -- fetch or set the :guard of the table.

When the operations above suggest that the table or its :guard are
modified, what is actually meant is that the current state is redefined
so that in it, the affected table name has the appropriate properties.
in such cases, the table form is an event (see EVENTS).  In the
:put case, if the key is already in the table and associated with the
proposed value, then the table event is redundant (see
REDUNDANT-EVENTS).

Table forms are commonly typed by the user while interacting with the
system.  :Put and :get forms are especially common.  Therefore, we have
adopted a positional syntax that is intended to be convenient for most
applications.  Essentially, some operations admit a "short form" of
invocation.

     (table name key-term value-term :put)   ; long form
     (table name key-term value-term)        ; short form

evaluates the key- and value-terms, obtaining two objects that we call
key and value, checks that the key and value satisfy the :guard on the
named table and then "modifies" the named table so that the value
associated with key is value.  When used like this, table is actually
an event in the sense that it changes the ACL2 world.  In general, the
forms evaluated to obtain the key and value may involve the variable
world, which is bound to the then-current world during the evaluation
of the forms.  However, in the special case that the table in question
is named acl2-defaults-table, the key and value terms may not contain
any variables.  Essentially, the keys and values used in events setting
the acl2-defaults-table must be explicitly given constants.  See
ACL2-DEFAULTS-TABLE.

     (table name key-term nil :get)          ; long form
     (table name key-term)                   ; short form

evaluates the key-term (see note below), obtaining an object, key, and
returns the value associated with key in the named table (or, nil if
there is no value associated with key).  When used like this, table is
not an event; the value is simply returned.

     (table name nil nil :alist)             ; long form
     (table name)                            ; short form

returns an alist representing the named table; for every key in the
table with a non-nil associated value, the alist pairs the key and its
value.  The order in which the keys are presented is unspecified.  When
used like this, table is not an event; the alist is simply returned.

     (table name nil val :clear)

sets the named table to the alist val, making the checks that :put
makes for each key and value of val.  When used like this, table is an
event because it changes the ACL2 world.

     (table name nil nil :guard)

returns the translated form of the guard of the named table.

     (table name nil nil :guard term)

Provided the named table is empty and has not yet been assigned a
:guard and term (which is not evaluated) is a term that mentions at
most the variables key, val and world, this event sets the :guard of
the named table to term.  Whenever a subsequent :put occurs, term will
be evaluated with key bound to the key argument of the :put, val bound
to the val argument of the :put, and world bound to the then current
world.  An error will be caused by the :put if the result of the
evaluation is nil.

Note that it is not allowed to change the :guard on a table once it has
been explicitly set.  Before the :guard is explicitly set, it is
effectively just t.  After it is set it can be changed only by undoing
the event that set it.  The purpose of this restriction is to prevent
the user from changing the :guards on tables provided by other people
or the system.

The intuition behind the :guard mechanism on tables is to enforce
invariants on the keys and values in a table, so that the values, say,
can be used without run-time checking.  But if the :guard of a table is
sensitive to the ACL2 world, it may be possible to cause some value in
the table to cease satisfying the :guard without doing any operations
on the table.  Consider for example the :guard "no value in this table
is the name of an event." As described, that is enforced each time a
value is stored.  Thus, 'bang can be :put in the table provided there
is no event named bang.  But once it is in the table, there is nothing
to prevent the user from defining bang as a function, causing the table
to contain a value that could not be :put there anymore.  Observe that
not all state-sensitive :guards suffer this problem.  The :guard "every
value is an event name" remains invariant, courtesy of the fact that
undoing back through an event name in the table would necessarily undo
the :put of the name into the table.

Table was designed primarily for convenient top-level use.  Tables are
not especially efficient.  Each table is represented by an alist stored
on the property list of the table name.  :Get is just a getprop and
assoc-equal.  :Put does a getprop to the get the table alist, a
put-assoc-equal to record the new association, and a putprop to store
the new table alist -- plus the overhead associated with :guards and
undoable events, and checking (for redundancy) if the key is already
bound to its proposed value.  Note that there are never duplicate keys
in the resulting alist; in particular, when the operation :clear is
used to install new alist, duplicate keys are removed from that alist.

A table name may be any symbol whatsoever.  Symbols already in use as
function or theorem names, for example, may be used as table names.
Symbols in use only as table names may be defined with defun, etc.
Because there are no restrictions on the user's choice of table names,
table names are not included among the logical names.  Thus, :pe name
will never display a table event (for a logical name other than :here).
Either :pe name will display a "normal" event such as (defun name ...)
or (defthm name ...) or else :pe name will cause an error indicating
that name is not a logical name.  This happens even if name is in use
as a table name.  Similarly, we do not permit table names to have
documentation strings, since the same name might already have a
documentation string.  If you want to associate a documentation string
with a table name that is being used no other way, define the name as a
label and use the :doc feature of deflabel (see DEFLABEL); also
see DEFDOC.

THEORY-INVARIANT    user-specified invariants on theories

     Examples:
     (theory-invariant (not (and (active-runep '(:rewrite left-to-right))
                                 (active-runep '(:rewrite right-to-left))))
                       :key my-invariant
                       :error nil)

     ; Equivalent to the above:
     (theory-invariant (incompatible (:rewrite left-to-right)
                                     (:rewrite right-to-left))
                       :key my-invariant
                       :error nil)

     General Form:
     (theory-invariant term &key key error)

where:

     o term is a term that uses no variables other than ens and state;

     o key is an arbitrary "name" for this invariant (if omitted, an
     integer is generated and used); and

     o :error specifies the action to be taken when an invariant is
     violated -- either nil if a warning is to be printed, else t (the
     default) if an error is to be caused.

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 with table;
you can clear an individual theory invariant by setting the invariant
to t, or eliminate all theory invariants with the command (table
theory-invariant-table nil nil :clear).

Theory-invariant-table maps arbitrary keys to records containing terms
that mention, at most, the variables ens and state.  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 ens bound to a so-called "enabled structure" obtained
from the theory expression and state bound to the current ACL2 state
(see STATE).  Users generally need not know about the enabled
structure, other than that it can be accessed using the macros
active-runep and incompatible; see ACTIVE-RUNEP and see
INCOMPATIBLE.  If the result is nil, a message is printed and an
error occurs (except, only a warning occurs if :error nil is
specified).  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; but see the Local Redefinition
Caveat at the end of this note.  You may want to avoid using explicit
names, since otherwise the subsequent inclusion of another book that
defines a theory invariant with the same name will override your 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 the
user is alerted when they are violated.

Since theory invariants are arbitrary terms, macros may be used to
express commonly used restrictions.  For example, executing the event

     (theory-invariant (incompatible (:rewrite left-to-right)
                                     (:rewrite right-to-left)))

would subsequently cause an error 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.

In order for a theory-invariant event to be accepted, the proposed
theory invariant must be satisfied by the current theory (see
CURRENT-THEORY).  The value returned upon successful execution of the
event is the key (whether user-supplied or generated).

Local Redefinition Caveat.  Care needs to be taken when redefining a
theory invariant in a local context.  Consider the following example.

     (theory-invariant
      (active-runep '(:definition binary-append))
      :key app-inv)

     (encapsulate
      ()
      (local (theory-invariant t :key app-inv))
      (in-theory (disable binary-append))
      (defthm ...))

The second pass of the encapsulate will fail, because the in-theory
event violates the original theory-invariant and the local
theory-invariant is skipped in the second pass of the encapsulate.  Of
course, local theory-invariants in books can cause the analogous
problem in the second (include-book) pass of a certify-book.  In both
cases, though, the theory invariants are only checked at the conclusion
of the (include-book or encapsulate) event.  Indeed, theory invariants
are checked at the end of every event related to theories, including
defun, defthm, in-theory, encapsulate, and include-book, except for
events executed on behalf of an include-book or the second pass of an
encapsulate.

VERIFY-GUARDS    verify the guards of a function

     Examples:
     (verify-guards flatten)
     (verify-guards flatten
                    :hints (("Goal" :use (:instance assoc-of-app)))
                    :otf-flg t
                    :doc "string")

     General Form:
     (verify-guards name
             :hints        hints
             :otf-flg      otf-flg
             :doc          doc-string)

See GUARD for a general discussion of guards.  In the General
Form above, 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 *not* beginning with ":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, and that the
guards are satisfied for all function calls in the guard itself (under
an implicit guard of t).  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.

If the guard on a function is not t, then guard verification requires
not only consideration of the body under the assumption that the guard
is true, but also consideration of the guard itself.  Thus, for
example, guard verification fails in the following example, even though
there are no proof obligations arising from the body, because the guard
itself can cause a guard violation when evaluated for an arbitrary
value of x:

     (defun foo (x)
       (declare (xargs :guard (car x)))
       x)

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))))))

     (defthm true-listp-rev
       (implies (true-listp x2)
                (true-listp (rev x2))))

     (verify-guards rev)

The ACL2 system can actually admit the original definition of 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.

*Note on computation of guard conjectures and evaluation*.  When ACL2
computes the guard conjecture for the body of a function, it evaluates
any ground subexpressions (those with no free variables), for calls of
functions whose :executable-counterpart runes are enabled.  Note that
here, "enabled" refers to the current global theory, not to any :hints
given to the guard verification process; after all, the guard
conjecture is computed even before its initial goal is produced.  Also
note that this evaluation is done in an environment as though
:set-guard-checking :all had been executed, so that we can trust that
this evaluation takes place without guard violations; see
SET-GUARD-CHECKING.

VERIFY-TERMINATION    convert a function from :program mode to :logic mode

     Example:
     (verify-termination fact)

     General Forms:
     (verify-termination fn dcl ... dcl)
     (verify-termination (fn1 dcl ... dcl)
                         (fn2 dcl ... dcl)
                         ...)

where fn and the fni are function symbols having :program mode (see
DEFUN-MODE) and all of the dcls 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 dcls 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.

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 other than to add
(declare (xargs :mode :logic)).  Otherwise, fn is some fni and we
modify its definition by inserting into it the corresponding dcls listed
with fni in the arguments to verify-termination, as well as (declare
(xargs :mode :logic)).  In addition, we throw out from the old
declarations in fn the :mode specification and anything that is
specified in the new dcls.

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
be tempted to submit the following:

     (verify-termination
      fact
      (declare (xargs :guard (and (integerp n) (<= 0 n))))).

However, this is considered a changing of the guard (from (integerp n)),
which is illegal.  If we instead change the guard in the earlier defun
after undoing that earlier definition with :ubt fact, then
(verify-termination fact) will succeed.