This is documentation for ACL2 Version 3.0
Copyright (C) 2006  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.

DEFEXEC    attach a terminating executable function to a definition

Suppose you define a function (fn x) with a guard of (good-input-p x),
and you know that when the guard holds, the measure decreases on each
recursive call.  Unfortunately, the definitional principle (see
DEFUN) ignores the guard.  For example, if the definition has the form

     (defun fn (x)
       (declare (xargs :guard (good-input-p x)))
       (if (not-done-yet x)
           (... (fn (destr x)) ...)
         ...))

then in order to admit this definition, ACL2 must prove the appropriate
formula asserting that (destr x) is "smaller than" x under the
assumption (not-done-yet x) but without the assumption (good-input-p x),
even if (not-done-yet x) is true.  In essence, it may be necessary to
submit instead the following definition.

     (defun fn (x)
       (declare (xargs :guard (good-input-p x)))
       (if (good-input-p x)
           (if (not-done-yet x)
               (... (fn (destr x)) ...)
             ...)
         nil)

But it is unfortunate that when calls of fn are evaluated, for example
when fn is applied to an explicit constant during a proof, then a call
of good-input-p must now be evaluated on each recursive call.

Fortunately, defexec provides a way to keep the execution efficient.
For the example above we could use the following form.

     (defexec fn (x)
       (declare (xargs :guard (good-input-p x)))
       (mbe :logic (if (good-input-p x)
                       (if (not-done-yet x)
                           (... (fn (destr x)) ...)
                         ...)
                     nil)
            :exec  (if (not-done-yet x)
                       (... (fn (destr x)) ...)
                     ...)))

Here "mbe" stands for "must-be-equal" and, roughly speaking, its call
above is logically equal to the :logic form but is evaluated using the
:exec form when the guard holds.  See MBE.  The effect is thus
to define fn as shown in the defun form above, but to cause execution of
fn using the :exec body.  The use of defexec instead of defun in the
example above causes a termination proof to be performed, in order to
guarantee that evaluation always theoretically terminates, even when
using the :exec form for evaluation.

     Example:

     ; Some of the keyword arguments in the declarations below are irrelevant or
     ; unnecessary, but they serve to illustrate their use.

     (defexec f (x)
       (declare (xargs :measure (+ 15 (acl2-count x))
                       :hints (("Goal" :in-theory (disable nth)))
                       :guard-hints (("Goal" :in-theory (disable last)))
                       :guard (and (integerp x) (<= 0 x) (< x 25)))
                (exec-xargs
                       :test (and (integerp x) (<= 0 x))
                       :default-value 'undef ; defaults to nil
                       :measure (nfix x)
                       :well-founded-relation o<))
       (mbe :logic (if (zp x)
                       1
                     (* x (f (- x 1))))
            :exec  (if (= x 0)
                       1
                     (* x (f (- x 1))))))

The above example macroexpands to the following.

     (ENCAPSULATE ()
      (LOCAL
       (ENCAPSULATE ()
        (SET-IGNORE-OK T)
        (SET-IRRELEVANT-FORMALS-OK T)
        (LOCAL (DEFUN F (X)
                 (DECLARE
                  (XARGS :VERIFY-GUARDS NIL
                         :HINTS (("Goal" :IN-THEORY (DISABLE NTH)))
                         :MEASURE (NFIX X)
                         :WELL-FOUNDED-RELATION O<))
                 (IF (AND (INTEGERP X) (<= 0 X))
                     (IF (= X 0) 1 (* X (F (- X 1))))
                     'UNDEF)))
        (LOCAL (DEFTHM F-GUARD-IMPLIES-TEST
                 (IMPLIES (AND (INTEGERP X) (<= 0 X) (< X 25))
                          (AND (INTEGERP X) (<= 0 X)))
                 :RULE-CLASSES NIL))))
      (DEFUN F (X)
        (DECLARE (XARGS :MEASURE (+ 15 (ACL2-COUNT X))
                        :HINTS (("Goal" :IN-THEORY (DISABLE NTH)))
                        :GUARD-HINTS (("Goal" :IN-THEORY (DISABLE LAST)))
                        :GUARD (AND (INTEGERP X) (<= 0 X) (< X 25))))
        (MBE :LOGIC
             (IF (ZP X) 1 (* X (F (- X 1))))
             :EXEC
             (IF (= X 0) 1 (* X (F (- X 1)))))))

Notice that in the example above, the :hints in the local definition of
F are inherited from the :hints in the xargs of the defexec form.  We
discuss such inheritance below.

     General Form:
     (defexec fn (var1 ... varn) doc-string dcl ... dcl
       (mbe :LOGIC logic-body
            :EXEC  exec-body))

where the syntax is identical to the syntax of defun where the body is a
call of mbe, with the exceptions described below.  Thus, fn is the
symbol you wish to define and is a new symbolic name and (var1 ... varn)
is its list of formal parameters (see NAME).  The first
exception is that at least one dcl (i.e., declare form) must specify a
:guard, guard.  The second exception is that one of the dcls is allowed
to contain an element of the form (exec-xargs ...).  The exec-xargs
form, if present, must specify a non-empty keyword-value-listp each of
whose keys is one of :test, :default-value, or one of the standard xargs
keys of :measure, :well-founded-relation, :hints, or :stobjs.  Any of
these four standard xargs keys that is present in an xargs of some dcl
but is not specified in the (possibly nonexistent) exec-xargs form is
considered to be specified in the exec-xargs form, as illustrated in the
example above for :hints.  (So for example, if you want :hints in the
final, non-local definition but not in the local definition, then
specify the :hints in the xargs but specify :hints nil in the
exec-xargs.)  If :test is specified and not nil, let test be its value;
otherwise let test default to guard.  If :default-value is specified,
let default-value be its value; else default-value is nil.
Default-value should have the same signature as exec-body; otherwise the
defexec form will fail to be admitted.

The above General Form's macroexpansion is of the form (PROGN encap
final-def), where encap and final-def are as follows.  Final-def is
simply the result of removing the exec-xargs declaration (if any) from
its declare form, and is the result of evaluating the given defexec
form, since encap is of the following form.

     ; encap
     (ENCAPSULATE ()
       (set-ignore-ok t)             ; harmless for proving termination
       (set-irrelevant-formals-ok t) ; harmless for proving termination
       (local local-def)
       (local local-thm))

The purpose of encap is to ensure the the executable version of name
terminates on all arguments.  Thus, local-def and local-thm are as
follows, where the xargs of the declare form are the result of adding
:VERIFY-GUARDS NIL to the result of removing the :test and (optional)
:default-value from the exec-xargs.

     ; local-def
     (DEFUN fn formals
       (DECLARE (XARGS :VERIFY-GUARDS NIL ...))
       (IF test
           exec-body
         default-value))

     ; local-thm
     (DEFTHM fn-EXEC-GUARD-HOLDS
       (IMPLIES guard test)
       :RULE-CLASSES NIL)

We claim that if the above local-def and local-thm are admitted, then
all evaluations of calls of fn terminate.  The concern is that the use
of mbe in final-def allows for the use of exec-body for a call of fn, as
well as for subsequent recursive calls, when guard holds and assuming
that the guards have been verified for final-def.  However, by local-thm
we can conclude in this case that test holds, in which case the call of
fn may be viewed as a call of the version of fn defined in local-def.
Moreover, since guards have been verified for final-def, then guards
hold for subsequent evaluation of exec-body, and in particular for
recursive calls of fn, which can thus continue to be viewed as calls
using local=def.

DEFLABEL    build a landmark and/or add a documentation topic

     Examples:
     (deflabel interp-section
        :doc
        ":Doc-Section ...")

     General Form:
     (deflabel name :doc doc-string)

where name is a new symbolic name (see NAME) and doc-string is
an optional documentation string (see DOC-STRING).  This event
adds the documentation string for symbol name to the :doc data base.  By
virtue of the fact that deflabel is an event, it also marks the current
history with the name.  Thus, even undocumented labels are convenient as
landmarks in a proof development.  For example, you may wish to undo
back through some label or compute a theory expression (see
THEORIES) in terms of some labels.  Deflabel events are never
considered redundant.  See REDUNDANT-EVENTS.

See DEFDOC for a means of attaching a documentation string to a
name without marking the current history with that name.

DEFMACRO    define a macro

     Example Defmacros:
     (defmacro xor (x y)
       (list 'if x (list 'not y) y))

     (defmacro git (sym key)
       (list 'getprop sym key nil
             '(quote current-acl2-world)
             '(w state)))

     (defmacro one-of (x &rest rst)
       (declare (xargs :guard (symbol-listp rst)))
       (cond ((null rst) nil)
             (t (list 'or
                      (list 'eq x (list 'quote (car rst)))
                      (list* 'one-of x (cdr rst))))))

     Example Expansions:
     term                    macroexpansion

     (xor a b)              (if a (not b) b)
     (xor a (foo b))        (if a (not (foo b)) (foo b))

     (git 'car 'lemmas)     (getprop 'car 'lemmas nil
                                     'current-acl2-world
                                     (w state))

     (one-of x a b c)       (or (eq x 'a)
                                (or (eq x 'b)
                                    (or (eq x 'c) nil)))

     (one-of x 1 2 3)       ill-formed (guard violation)

     General Form:
     (defmacro name macro-args doc-string dcl ... dcl body)

where name is a new symbolic name (see NAME), macro-args
specifies the formals of the macro (see MACRO-ARGS for a
description), and body is a term.  Doc-string is an optional
documentation string; see DOC-STRING.  Each dcl is an optional
declaration (see DECLARE) except that the only xargs keyword
permitted by defmacro is :guard.

Macroexpansion occurs when a form is read in, i.e., before the
evaluation or proof of that form is undertaken.  To experiment with
macroexpansion, see TRANS.  When a form whose car is name arises
as the form is read in, the arguments are bound as described in CLTL
pp. 60 and 145, the guard is checked, and then the body is evaluated.
The result is used in place of the original form.

In ACL2, macros do not have access to state.  That is, state is not
allowed among the formal parameters.  This is in part a reflection of
CLTL, pp. 143, "More generally, an implementation of Common Lisp has
great latitude in deciding exactly when to expand macro calls with a
program. ...  Macros should be written in such a way as to depend as
little as possible on the execution environment to produce a correct
expansion." In ACL2, the product of macroexpansion is independent of the
current environment and is determined entirely by the macro body and the
functions and constants it references.  It is possible, however, to
define macros that produce expansions that refer to state or other
single-threaded objects (see STOBJ) or variables not among the
macro's arguments.  See the git example above.

DEFPKG    define a new symbol package

     Example:
     (defpkg "MY-PKG"
             (union-eq *acl2-exports*
                       *common-lisp-symbols-from-main-lisp-package*))

     * Menu:

     * HIDDEN-DEATH-PACKAGE:: handling defpkg events that are local

     * HIDDEN-DEFPKG:: handling defpkg events that are local

     General Form:
     (defpkg "name" term doc-string)

where "name" is a non-empty string consisting of standard characters
(see STANDARD-CHAR-P), none of which is lower case, that names
the package to be created; term is a variable-free expression that
evaluates to a list of symbols, where no two distinct symbols in the
list may have the same symbol-name, to be imported into the newly
created package; and doc-string is an optional documentation string; see
DOC-STRING.  The name of the new package must be "new": the host
lisp must not contain any package of that name.  There are two
exceptions to this newness rule, discussed at the end of this
documentation.

(There is actually an additional argument, book-path, that is used for
error reporting but has no logical content.  Users should generally
ignore this argument, as well as the rest of this sentence: a book-path
will be specified for defpkg events added by ACL2 to the portcullis of a
book's certificate; see HIDDEN-DEATH-PACKAGE.)

Defpkg forms can be entered at the top-level of the ACL2 command loop.
They should not occur in books (see CERTIFY-BOOK).

After a successful defpkg it is possible to "intern" a string into the
package using intern-in-package-of-symbol.  The result is a symbol that
is in the indicated package, provided the imports allow it.  For
example, suppose 'my-pkg::abc is a symbol whose symbol-package-name is
"MY-PKG".  Suppose further that the imports specified in the defpkg for
"MY-PKG" do not include a symbol whose symbol-name is "XYZ".  Then

     (intern-in-package-of-symbol "XYZ" 'my-pkg::abc)

returns a symbol whose symbol-name is "XYZ" and whose
symbol-package-name is "MY-PKG".  On the other hand, if the imports to
the defpkg does include a symbol with the name "XYZ", say in the package
"LISP", then

     (intern-in-package-of-symbol "XYZ" 'my-pkg::abc)

returns that symbol (which is uniquely determined by the restriction on
the imports list above).  See INTERN-IN-PACKAGE-OF-SYMBOL.

Defpkg is the only means by which an ACL2 user can create a new package
or specify what it imports.  That is, ACL2 does not support the Common
Lisp functions make-package or import.  Currently, ACL2 does not support
exporting at all.

The Common Lisp function intern is weakly supported by ACL2.  See
INTERN.

We now explain the two exceptions to the newness rule for package names.
The careful experimenter will note that if a package is created with a
defpkg that is subsequently undone, the host lisp system will contain
the created package even after the undo.  Because ACL2 hangs onto worlds
after they have been undone, e.g., to implement :oops but, more
importantly, to implement error recovery, we cannot actually destroy a
package upon undoing it.  Thus, the first exception to the newness rule
is that name is allowed to be the name of an existing package if that
package was created by an undone defpkg and the newly proposed imports
list is identical to the old one.  See
PACKAGE-REINCARNATION-IMPORT-RESTRICTIONS.  This exception does not
violate the spirit of the newness rule, since one is disinclined to
believe in the existence of undone packages.  The second exception is
that name is allowed to be the name of an existing package if the
package was created by a defpkg with identical imports.  That is, it is
permissible to execute "redundant" defpkg commands.  The redundancy test
is based on the values of the two import forms, not on the forms
themselves.

Finally, we explain why we require the package name to contain standard
characters, none of which is lower case.  We have seen at least one
implementation that handled lower-case package names incorrectly.  Since
we see no need for lower-case characters in package names, which can
lead to confusion anyhow (note for example that foo::bar is a symbol
whose symbol-package-name is "FOO"}, not c["foo"), we simply disallow
them.  Since the notion of "lower case" is only well-specified in Common
Lisp for standard characters, we restrict to these.

HIDDEN-DEATH-PACKAGE    handling defpkg events that are local

This documentation topic explains a little bit about certain errors
users may see when attempting to evaluate a defpkg event.  In brief, if
you see an error that refers you to this topic, you are probably trying
to admit a defpkg event, and you should change the name of the package
to be introduced by that event.

Recall that defpkg events introduce axioms, for example as follows.

     ACL2 !>(defpkg "PKG0" '(a b))

     Summary
     Form:  ( DEFPKG "PKG0" ...)
     Rules: NIL
     Warnings:  None
     Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
      "PKG0"
     ACL2 !>:pr! "PKG0"

     Rune:       (:REWRITE PKG0-PACKAGE)
     Status:     Enabled
     Lhs:        (SYMBOL-PACKAGE-NAME (INTERN-IN-PACKAGE-OF-SYMBOL X Y))
     Rhs:        "PKG0"
     Hyps:       (AND (STRINGP X)
                      (NOT (MEMBER-SYMBOL-NAME X '(A B)))
                      (SYMBOLP Y)
                      (EQUAL (SYMBOL-PACKAGE-NAME Y) "PKG0"))
     Equiv:      EQUAL
     Backchain-limit-lst:    NIL
     Subclass:   BACKCHAIN
     Loop-stopper: NIL
     ACL2 !>

Now, a defpkg event may be executed underneath an encapsulate or
include-book form that is marked local.  In that case, traces of the
added axiom will disappear after the surrounding encapsulate or
include-book form is admitted.  This can cause inconsistencies.  (You
can take our word for it, or you can look at the example shown in the
"Essay on Hidden Packages" in source file axioms.lisp.)

In order to prevent unsoundness, then, ACL2 maintains the following
invariant.  Let us say that a defpkg event is "hidden" if it is in
support of the current logical world but is not present in that world as
an event, because it is local as indicated above.  We maintain the
invariant that all defpkg events, even if "hidden", are tracked
under-the-hood in the current logical world.  Sometimes this property
causes defpkg events to be written to the portcullis of a book's
certificate (see BOOKS).  At any rate, if you then try to define
the package in a manner inconsistent with the earlier such definition,
that is, with a different imports list, you will see an error because of
the above-mentioned tracking.

(By the way, this topic's name comes from Holly Bell, who heard "hidden
death package" instead of "hidden defpkg".  The description seemed to
fit.  Thanks, Holly!)

HIDDEN-DEFPKG    handling defpkg events that are local

See HIDDEN-DEATH-PACKAGE

DEFREFINEMENT    prove that equiv1 refines equiv2

     Example:
     (defrefinement equiv1 equiv2)

     is an abbreviation for
     (defthm equiv1-refines-equiv2
       (implies (equiv1 x y) (equiv2 x y))
       :rule-classes (:refinement))

See REFINEMENT.

     General Form:
     (defrefinement equiv1 equiv2
       :rule-classes rule-classes
       :instructions instructions
       :hints hints
       :otf-flg otf-flg
       :event-name event-name
       :doc doc)

where equiv1 and equiv2 are known equivalence relations, event-name, if
supplied, is a symbol and all other arguments are as specified in the
documentation for defthm.  The defrefinement macro expands into a call
of defthm.  The name supplied is equiv1-refines-equiv2, unless
event-name is supplied, in which case it is used as the name.  The term
supplied states that equiv1 refines equiv2.  The rule-class :refinement
is added to the rule-classes specified, if it is not already there.  All
other arguments to the generated defthm form are as specified by the
other keyword arguments above.

DEFSTOBJ    define a new single-threaded object

     Example:
     (defstobj st
               (reg :type (array (unsigned-byte 31) (8))
                    :initially 0)
               (p-c :type (unsigned-byte 31)
                    :initially 555)
               halt                  ; = (halt :type t :initially nil)
               (mem :type (array (unsigned-byte 31) (64))
                    :initially 0 :resizable t))

     General Form:
     (defstobj name
               (field1 :type type1 :initially val1 :resizable b1)
               ...
               (fieldk :type typek :initially valk :resizable bk)
               :renaming alist
               :doc doc-string
               :inline inline-flag)

where name is a new symbol, each fieldi is a symbol, each typei is
either a type-spec or (ARRAY type-spec (max)), each vali is an object
satisfying typei, and each bi is t or nil.  Each pair :initially vali
and :resizable bi may be omitted; more on this below.  The alist
argument is optional and allows the user to override the default
function names introduced by this event.  The doc-string is also
optional.  The inline-flag Boolean argument is also optional and
declares to ACL2 that the generated access and update functions for the
stobj should be implemented as macros under the hood (which has the
effect of inlining the function calls).  We describe further
restrictions on the fieldi, typei, vali, and on alist below.  We
recommend that you read about single-threaded objects (stobjs) in ACL2
before proceeding; see STOBJ.

The effect of this event is to introduce a new single-threaded object
(i.e., a "stobj"), named name, and the associated recognizers, creator,
accessors, updaters, constants, and, for fields of ARRAY type, length
and resize functions.

*The Single-Threaded Object Introduced*

The defstobj event effectively introduces a new global variable, named
name, which has as its initial logical value a list of k elements, where
k is the number of "field descriptors" provided.  The elements are
listed in the same order in which the field descriptors appear.  If the
:type of a field is (ARRAY type-spec (max)) then the corresponding
element of the stobj is initially a list of length max containing the
value, val, specified by :initially val.  Otherwise, the :type of the
field is a type-spec and the corresponding element of the stobj is the
specified initial value val.  (The actual representation of the stobj in
the underlying Lisp may be quite different; see STOBJ-EXAMPLE-2.
For the moment we focus entirely on the logical aspects of the object.)

In addition, the defstobj event introduces functions for recognizing and
creating the stobj and for recognizing, accessing, and updating its
fields.  For fields of ARRAY type, length and resize functions are also
introduced.  Constants are introduced that correspond to the accessor
functions.

*Restrictions on the Field Descriptions in Defstobj*

Each field descriptor is of the form:

     (fieldi :TYPE typei :INITIALLY vali)

Note that the type and initial value are given in "keyword argument"
format and may be given in either order.  The typei and vali "arguments"
are not evaluated.  If omitted, the type defaults to t (unrestricted)
and the initial value defaults to nil.

Each typei must be either a type-spec or else a list of the form (ARRAY
type-spec (max)).  The latter forms are said to be "array types."
Examples of legal typei are:

     (INTEGERP 0 31)
     (SIGNED-BYTE 31)
     (ARRAY (SIGNED-BYTE 31) (16))

The typei describes the objects which are expected to occupy the given
field.  Those objects in fieldi should satisfy typei.  We are more
precise below about what we mean by "expected."  We first present the
restrictions on typei and vali.

Non-Array Types

When typei is a type-spec it restricts the contents,
x, of fieldi according to the "meaning" formula given in
the table for type-spec.  For example, the first typei
above restricts the field to be an integer between 0 and 31,
inclusive.  The second restricts the field to be an integer between
-2^30 and (2^30)-1, inclusive.

The initial value, vali, of a field description may be any ACL2 object
but must satisfy typei.  Note that vali is not a form to be evaluated
but an object.  A form that evaluates to vali could be written 'vali,
but defstobj does not expect you to write the quote mark.  For example,
the field description

     (days-off :initially (saturday sunday))

describes a field named days-off whose initial value is the list
consisting of the two symbols SATURDAY and SUNDAY.  In particular, the
initial value is NOT obtained by applying the function saturday to the
variable sunday!  Had we written

     (days-off :initially '(saturday sunday))

it would be equivalent to writing

     (days-off :initially (quote (saturday sunday)))

which would initialize the field to a list of length two, whose first
element is the symbol quote and whose second element is a list
containing the symbols saturday and sunday.

Array Types

When typei is of the form (ARRAY type-spec (max)), the field is supposed
to be a list of items, initially of length max, each of which satisfies
the indicated type-spec.  Max must be a non-negative integer less than
(2^28)-1.  We discuss this limitation below. Thus,

     (ARRAY (SIGNED-BYTE 31) (16))

restricts the field to be a list of integers, initially of length 16,
where each integer in the list is a (SIGNED-BYTE 31).  We sometimes call
such a list an "array" (because it is represented as an array in the
underlying Common Lisp).  The elements of an array field are indexed by
position, starting at 0.  Thus, the maximum legal index of an array
field is max-1.

Note that the ARRAY type requires that the max be enclosed in
parentheses.  This makes ACL2's notation consistent with the Common Lisp
convention of describing the (multi-)dimensionality of arrays.  But ACL2
currently supports only single dimensional arrays in stobjs.

For array fields, the initial value vali must be an object satisfying
the type-spec of the ARRAY description.  The initial value of the field
is a list of max repetitions of vali.

Array fields can be "resized," that is, their lengths can be changed, if
:resizable t is supplied as shown in the example and General Form above.
The new length must satisfy the same restriction as does max, as
described above.  Each array field in a defstobj event gives rise to a
length function, which gives the length of the field, and a resize
function, which modifies the length of the field if :resizable t was
supplied with the field when the defstobj was introduced and otherwise
causes an error.

Array resizing is relatively slow, so we recommend using it somewhat
sparingly.

*The Default Function Names*

To recap, in

     (defstobj name
               (field1 :type type1 :initially val1)
               ...
               (fieldk :type typek :initially valk)
               :renaming alist
               :doc doc-string
               :inline inline-flag)

name must be a new symbol, each fieldi must be a symbol, each typei must
be a type-spec or (ARRAY type-spec (max)), and each vali must be an
object satisfying typei.

Roughly speaking, for each fieldi, a defstobj introduces a recognizer
function, an accessor function, and an updater function.  The accessor
function, for example, takes the stobj and returns the indicated
component; the updater takes a new component value and the stobj and
return a new stobj with the component replaced by the new value.  But
that summary is inaccurate for array fields.

The accessor function for an array field does not take the stobj and
return the indicated component array, which is a list of length max.
Instead, it takes an additional index argument and returns the indicated
element of the array component.  Similarly, the updater function for an
array field takes an index, a new value, and the stobj, and returns a
new stobj with the indicated element replaced by the new value.

These functions -- the recognizer, accessor, and updater, and also
length and resize functions in the case of array fields -- have "default
names."  The default names depend on the field name, fieldi, and on
whether the field is an array field or not.  For clarity, suppose fieldi
is named c. The default names are shown below in calls, which also
indicate the arities of the functions.  In the expressions, we use x as
the object to be recognized by field recognizers, i as an array index, v
as the "new value" to be installed by an updater, and name as the
single-threaded object.

                      non-array field        array field
     recognizer         (cP x)                (cP x)
     accessor           (c name)              (cI i name)
     updater            (UPDATE-c v name)     (UPDATE-cI i v name)
     length                                   (c-LENGTH name)
     resize                                   (RESIZE-c k name)

Finally, a recognizer and a creator for the entire single-threaded
object are introduced.  The creator returns the initial stobj, but may
only be used in limited contexts; see WITH-LOCAL-STOBJ.  If the
single-threaded object is named name, then the default names and arities
are as shown below.

     top recognizer     (nameP x)
     creator            (CREATE-name)

For example, the event

     (DEFSTOBJ $S
       (X :TYPE INTEGER :INITIALLY 0)
       (A :TYPE (ARRAY (INTEGER 0 9) (3)) :INITIALLY 9))

introduces a stobj named $S.  The stobj has two fields, X and A.  The A
field is an array.  The X field contains an integer and is initially 0.
The A field contains a list of integers, each between 0 and 9,
inclusively.  Initially, each of the three elements of the A field is 9.

This event introduces the following sequence of definitions:

     (DEFUN XP (X) ...)               ; recognizer for X field
     (DEFUN AP (X) ...)               ; recognizer of A field
     (DEFUN $SP ($S) ...)             ; top-level recognizer for stobj $S
     (DEFUN CREATE-$S () ...)         ; creator for stobj $S
     (DEFUN X ($S) ...)               ; accessor for X field
     (DEFUN UPDATE-X (V $S) ...)      ; updater for X field
     (DEFUN A-LENGTH ($S) ...)        ; length of A field
     (DEFUN RESIZE-A (K $S) ...)      ; resizer for A field
     (DEFUN AI (I $S) ...)            ; accessor for A field at index I
     (DEFUN UPDATE-AI (I V $S) ...)   ; updater for A field at index I

*Avoiding the Default Function Names*

If you do not like the default names listed above you may use the
optional :renaming alist to substitute names of your own choosing.  Each
element of alist should be of the form (fn1 fn2), where fn1 is a default
name and fn2 is your choice for that name.

For example

     (DEFSTOBJ $S
       (X :TYPE INTEGER :INITIALLY 0)
       (A :TYPE (ARRAY (INTEGER 0 9) (3)) :INITIALLY 9)
       :renaming ((X XACCESSOR) (CREATE-$S MAKE$S)))

introduces the following definitions

     (DEFUN XP (X) ...)               ; recognizer for X field
     (DEFUN AP (X) ...)               ; recognizer of A field
     (DEFUN $SP ($S) ...)             ; top-level recognizer for stobj $S
     (DEFUN MAKE$S () ...)            ; creator for stobj $S
     (DEFUN XACCESSOR ($S) ...)       ; accessor for X field
     (DEFUN UPDATE-X (V $S) ...)      ; updater for X field
     (DEFUN A-LENGTH ($S) ...)        ; length of A field
     (DEFUN RESIZE-A (K $S) ...)      ; resizer for A field
     (DEFUN AI (I $S) ...)            ; accessor for A field at index I
     (DEFUN UPDATE-AI (I V $S) ...)   ; updater for A field at index I

Note that even though the renaming alist substitutes "XACCESSOR" for "X"
the updater for the X field is still called "UPDATE-X."  That is because
the renaming is applied to the default function names, not to the field
descriptors in the event.

Use of the :renaming alist may be necessary to avoid name clashes
between the default names and and pre-existing function symbols.

*Constants*

Defstobj events also introduce constant definitions (see
DEFCONST).  One constant is introduced for each accessor function by
prefixing and suffixing a `*' character on the function name.  The value
of that constant is the position of the field being accessed.  For
example, if the accessor functions are a, b, and c, in that order, then
the following constant definitions are introduced.

     (defconst *a* 0)
     (defconst *b* 1)
     (defconst *c* 2)

These constants are used for certain calls of nth and update-nth that
are displayed to the user in proof output.  For example, for stobj st
with accessor functions a, b, and c, in that order, the term (nth '2 st)
would be printed during a proof as (nth *c* st).  Also see TERM,
in particular the discussion there of untranslated terms, and see
NTH-ALIASES-TABLE.

*Inspecting the Effects of a Defstobj*

Because the stobj functions are introduced as "sub-events" of the
defstobj the history commands :pe and :pc will not print the definitions
of these functions but will print the superior defstobj event.  To see
the definitions of these functions use the history command :pcb!.

To see an s-expression containing the definitions what constitute the
raw Lisp implementation of the event, evaluate the form

     (nth 4 (global-val 'cltl-command (w state)))

*immediately after* the defstobj event has been processed.

A defstobj is considered redundant only if the name, field descriptors,
renaming alist, and inline flag are identical to a previously executed
defstobj.

*Inlining and Performance*

The :inline keyword argument controls whether or not accessor, updater,
and length functions are inlined (as macros under the hood, in raw
Lisp).  If :inline t is provided then these are inlined; otherwise they
are not.  The advantage of inlining is potentially better performance;
there have been contrived examples, doing essentially nothing except
accessing and updating array fields, where inlining reduced the time by
a factor of 10 or more; and inlining has sped up realistic examples by a
factor of at least 2.  Inlining may get within a factor of 2 of C
execution times for such contrived examples, and within a few percent of
C execution times on realistic examples.

A drawback to inlining is that redefinition may not work as expected,
much as redefinition may not work as expected for macros: defined
functions that call a macro, or inlined stobj function, will not see a
subsequent redefinition of the macro or inlined function.  Another
drawback to inlining is that because inlined functions are implemented
as macros in raw Lisp, tracing (see TRACE$) will not show their
calls.  These drawbacks are avoided by default, but the user who is not
concerned about them is advised to specify :inline t.

DEFSTUB    stub-out a function symbol

     Examples:
     ACL2 !>(defstub subr1 (* * state) => (mv * state))
     ACL2 !>(defstub add-hash (* * hash-table) => hash-table)

     General Forms:
     (defstub name args-sig => output-sig)
     (defstub name args-sig => output-sig :doc doc-string)

Name is a new function symbol and (name . args-sig) => output-sig) is a
signature.  If the optional doc-string is supplied it should be a
documentation string.  See also the "Old Style" heading below.

Defstub macro expands into an encapsulate event (see
ENCAPSULATE).  Thus, no axioms are available about name but it may be
used wherever a function of the given signature is permitted.

Old Style:

     Old Style General Form:
     (defstub name formals output)
     (defstub name formals output :doc doc-string)

where name is a new function symbol, formals is its list of formal
parameters, and output is either a symbol (indicating that the function
returns one result) or a term of the form (mv s1 ... sn), where each si
is a symbol (indicating that the function returns n results).  Whether
and where the symbol state occurs in formals and output indicates how
the function handles state.  It should be the case that (name formals
output) is in fact a signature (see SIGNATURE).

Note that with the old style notation it is impossible to stub-out a
function that uses any single-threaded object other than state.  The old
style is preserved for compatibility with earlier versions of ACL2.

DEFTHEORY    define a theory (to enable or disable a set of rules)

     Example:
     (deftheory interp-theory
                (set-difference-theories
                  (universal-theory :here)
                  (universal-theory 'interp-section)))

     General Form:
     (deftheory name term :doc doc-string)

where name is a new symbolic name (see NAME), term is a term
that when evaluated will produce a theory (see THEORIES), and
doc-string is an optional documentation string (see DOC-STRING).
Except for the variable world, term must contain no free variables.
Term is evaluated with world bound to the current world (see
WORLD) and the resulting theory is then converted to a *runic theory*
(see THEORIES) and associated with name.  Henceforth, this runic
theory is returned as the value of the theory expression (theory name).

The value returned is the length of the resulting theory.  For example,
in the following, the theory associated with 'FOO has 54 runes:

     ACL2 !>(deftheory foo (union-theories '(binary-append)
                                           (theory 'minimal-theory)))

     Summary
     Form:  ( DEFTHEORY FOO ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      54
     ACL2 !>

DEFTHM    prove and name a theorem

     Examples:
     (defthm assoc-of-app
             (equal (app (app a b) c)
                    (app a (app b c))))

The following nonsensical example illustrates all the optional arguments
but is illegal because not all combinations are permitted.  See
HINTS for a complete list of hints.

     (defthm main
             (implies (hyps x y z) (concl x y z))
            :rule-classes (:REWRITE :GENERALIZE)
            :instructions (induct prove promote (dive 1) x
                                  (dive 2) = top (drop 2) prove)
            :hints (("Goal"
                     :do-not '(generalize fertilize)
                     :in-theory (set-difference-theories
                                  (current-theory :here)
                                  '(assoc))
                     :induct (and (nth n a) (nth n b))
                     :use ((:instance assoc-of-append
                                      (x a) (y b) (z c))
                           (:functional-instance
                             (:instance p-f (x a) (y b))
                             (p consp)
                             (f assoc)))))
            :otf-flg t
            :doc "#0[one-liner/example/details]")

     General Form:
     (defthm name term
             :rule-classes rule-classes
             :instructions instructions
             :hints        hints
             :otf-flg      otf-flg
             :doc          doc-string)

where name is a new symbolic name (see NAME), term is a term
alleged to be a theorem, and rule-classes, instructions, hints, otf-flg
and doc-string are as described in their respective documentation.  The
five keyword arguments above are all optional, however you may not
supply both :instructions and :hints, since one drives the proof checker
and the other drives the theorem prover.  If :rule-classes is not
specified, the list (:rewrite) is used; if you wish the theorem to
generate no rules, specify :rule-classes nil.

When ACL2 processes a defthm event, it first tries to prove the term
using the indicated hints (see HINTS) or instructions (see
PROOF-CHECKER).  If it is successful, it stores the rules described by
the rule-classes (see RULE-CLASSES), proving the necessary
corollaries.

DEFTHMD    prove and name a theorem and then disable it

Use defthmd instead of defthm when you want to disable a theorem
immediately after proving it.  This macro has been provided for users
who prefer working in a mode where theorems are only enabled when
explicitly directed by :in-theory.  Specifically, the form

     (defthmd NAME TERM ...)

expands to:

     (progn
       (defthmd NAME TERM ...)
       (with-output
        :off summary
        (in-theory (disable NAME)))
       (value NAME)).

Note that defthmd commands are never redundant (see
REDUNDANT-EVENTS).  Even if the defthm event is redundant, then the
in-theory event will still be executed.

The summary for the in-theory event is suppressed.  See DEFTHM
for documentation of defthm.

DEFUN    define a function symbol

     Examples:
     (defun app (x y)
       (if (consp x)
           (cons (car x) (app (cdr x) y))
           y))

     (defun fact (n)
       (declare (xargs :guard (and (integerp n)
                                   (>= n 0))))
       (if (zp n)
           1
           (* n (fact (1- n)))))

     General Form:
     (defun fn (var1 ... varn) doc-string dcl ... dcl body),

where fn is the symbol you wish to define and is a new symbolic name
(see NAME), (var1 ... varn) is its list of formal parameters
(see NAME), and body is its body.  The definitional axiom is
logically admissible provided certain restrictions are met.  These are
sketched below.

Note that ACL2 does not support the use of lambda-list keywords (such as
&optional) in the formals list of functions.  We do support some such
keywords in macros and often you can achieve the desired syntax by
defining a macro in addition to the general version of your function.
See DEFMACRO.  The documentation string, doc-string, is
optional; for a description of its form, see DOC-STRING.

The *declarations* (see DECLARE), dcl, are also optional.  If
more than one dcl form appears, they are effectively grouped together as
one.  Perhaps the most commonly used ACL2 specific declaration is of the
form (declare (xargs :guard g :measure m)).  This declaration in the
defun of some function fn has the effect of making the "guard" for fn be
the term g and the "measure" be the term m.  The notion of "measure" is
crucial to ACL2's definitional principle.  The notion of "guard" is not,
and is discussed elsewhere; see VERIFY-GUARDS and see
SET-VERIFY-GUARDS-EAGERNESS.

We now briefly discuss the ACL2 definitional principle, using the
following definition form which is offered as a more or less generic
example.

     (defun fn (x y)
       (declare (xargs :guard (g x y)
                       :measure (m x y)))
       (if (test x y)
           (stop x y)
           (step (fn (d x) y))))

Note that in our generic example, fn has just two arguments, x and y,
the guard and measure terms involve both of them, and the body is a
simple case split on (test x y) leading to a "non-recursive" branch,
(stop x y), and a "recursive" branch.  In the recursive branch, fn is
called after "decrementing" x to (d x) and some step function is applied
to the result.  Of course, this generic example is quite specific in
form but is intended to illustrate the more general case.

Provided this definition is admissible under the logic, as outlined
below, it adds the following axiom to the logic.

     Defining Axiom:
     (fn x y)
       =
     (if (test x y)
         (stop x y)
       (step (fn (d x) y)))

Note that the guard of fn has no bearing on this logical axiom.

This defining axiom is actually implemented in the ACL2 system by a
:definition rule, namely

     (equal (fn x y)
            (if (test a b)
                (stop a b)
              (step (fn (d a) b)))).

See DEFINITION for a discussion of how definition rules are
applied.  Roughly speaking, the rule causes certain instances of (fn x
y) to be replaced by the corresponding instances of the body above.
This is called "opening up" (fn x y).  The instances of (fn x y) opened
are chosen primarily by heuristics which determine that the recursive
calls of fn in the opened body (after simplification) are more desirable
than the unopened call of fn.

This discussion has assumed that the definition of fn was admissible.
Exactly what does that mean?  First, fn must be a previously
unaxiomatized function symbol (however, see
LD-REDEFINITION-ACTION).  Second, the formal parameters must be
distinct variable names.  Third, the guard, measure, and body should all
be terms and should mention no free variables except the formal
parameters.  Thus, for example, body may not contain references to
"global" or "special" variables; ACL2 constants or additional formals
should be used instead.

The final conditions on admissibility concern the termination of the
recursion.  Roughly put, all applications of fn must terminate.  In
particular, there must exist a binary relation, rel, and some unary
predicate mp such that rel is well-founded on objects satisfying mp, the
measure term m must always produce something satisfying mp, and the
measure term must decrease according to rel in each recursive call,
under the hypothesis that all the tests governing the call are
satisfied.  By the meaning of well-foundedness, we know there are no
infinitely descending chains of successively rel-smaller mp-objects.
Thus, the recursion must terminate.

The only primitive well-founded relation in ACL2 is o< (see O<),
which is known to be well-founded on the o-ps (see O-P).  For
the proof of well-foundedness, see PROOF-OF-WELL-FOUNDEDNESS.
However it is possible to add new well-founded relations.  For details,
see WELL-FOUNDED-RELATION.  We discuss later how to specify
which well-founded relation is selected by defun and in the present
discussion we assume, without loss of generality, that it is o< on the
o-ps.

For example, for our generic definition of fn above, with measure term
(m x y), two theorems must be proved.  The first establishes that m
produces an ordinal:

     (o-p (m x y)).

The second shows that m decreases in the (only) recursive call of fn:

     (implies (not (test x y))
              (o< (m (d x) y) (m x y))).

Observe that in the latter formula we must show that the "m-size" of (d
x) and y is "smaller than" the m-size of x and y, provided the test,
(test x y), in the body fails, thus leading to the recursive call (fn (d
x) y).

See O< for a discussion of this notion of "smaller than."  It
should be noted that the most commonly used ordinals are the natural
numbers and that on natural numbers, o< is just the familiar "less than"
relation (<).  Thus, it is very common to use a measure m that returns a
nonnegative integer, for then (o-p (m x y)) becomes a simple conjecture
about the type of m and the second formula above becomes a conjecture
about the less-than relationship of nonnegative integer arithmetic.

The most commonly used measure function is acl2-count, which computes a
nonnegative integer size for all ACL2 objects.  See ACL2-COUNT.

Probably the most common recursive scheme in Lisp programming is when
some formal is supposed to be a list and in the recursive call it is
replaced by its cdr.  For example, (test x y) might be simply (atom x)
and (d x) might be (cdr x).  In that case, (acl2-count x) is a suitable
measure because the acl2-count of a cons is strictly larger than the
acl2-counts of its car and cdr.  Thus, "recursion by car" and "recursion
by cdr" are trivially admitted if acl2-count is used as the measure and
the definition protects every recursive call by a test insuring that the
decremented argument is a consp.  Similarly, "recursion by 1-" in which
a positive integer formal is decremented by one in recursion, is also
trivially admissible.  See BUILT-IN-CLAUSES to extend the class
of trivially admissible recursive schemes.

We now turn to the question of which well-founded relation defun uses.
It should first be observed that defun must actually select both a
relation (e.g., o<) and a domain predicate (e.g., o-p) on which that
relation is known to be well-founded.  But, as noted elsewhere (see
WELL-FOUNDED-RELATION), every known well-founded relation has a
unique domain predicate associated with it and so it suffices to
identify simply the relation here.

The xargs field of a declare permits the explicit specification of any
known well-founded relation with the keyword :well-founded-relation.  An
example is given below.  If the xargs for a defun specifies a
well-founded relation, that relation and its associated domain predicate
are used in generating the termination conditions for the definition.

If no :well-founded-relation is specified, defun uses the
:well-founded-relation specified in the acl2-defaults-table.  See
SET-WELL-FOUNDED-RELATION to see how to set the default well-founded
relation (and, implicitly, its domain predicate).  The initial default
well-founded relation is o< (with domain predicate o-p).

This completes the brief sketch of the ACL2 definitional principle.

On very rare occasions ACL2 will seem to "hang" when processing a
definition, especially if there are many subexpressions of the body
whose function symbol is if (or which macroexpand to such an
expression).  In those cases you may wish to supply the following to
xargs: :normalize nil.  This is an advanced feature that turns off
ACL2's usual propagation upward of if tests.

The following example illustrates all of the available declarations, but
is completely nonsensical.  For documentation, see XARGS and see
HINTS.

     (defun example (x y z a b c i j)
       (declare (ignore a b c)
                (type integer i j)
                (xargs :guard (symbolp x)
                       :measure (- i j)
                       :well-founded-relation my-wfr
                       :hints (("Goal"
                                :do-not-induct t
                                :do-not '(generalize fertilize)
                                :expand ((assoc x a) (member y z))
                                :restrict ((<-trans ((x x) (y (foo x)))))
                                :hands-off (length binary-append)
                                :in-theory (set-difference-theories
                                             (current-theory :here)
                                             '(assoc))
                                :induct (and (nth n a) (nth n b))
                                :non-executable t
                                :use ((:instance assoc-of-append
                                                 (x a) (y b) (z c))
                                      (:functional-instance
                                        (:instance p-f (x a) (y b))
                                        (p consp)
                                        (f assoc)))))
                       :guard-hints (("Subgoal *1/3'"
                                      :use ((:instance assoc-of-append
                                                       (x a) (y b) (z c)))))
                       :mode :logic
                       :normalize nil
                       :otf-flg t))
       (example-body x y z i j))