This is documentation for ACL2 Version 3.3
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.

STOBJ-EXAMPLE-2    an example of the use of arrays in single-threaded objects

The following event

     (defstobj ms
       (pcn  :type integer                  :initially 0)
       (mem  :type (array integer (100000)) :initially -1)
       (code :type t                        :initially nil))

introduces a single-threaded object named ms (which stands for "machine
state").  The object has three fields, a pcn or program counter, a mem
or memory, and a code field.

The mem field is occupied by an object initially of type (array integer
(100000)).  Logically speaking, this is a list of length 100000, each
element of which is an integer.  But in the underlying implementation
of the ms object, this field is occupied by a raw Lisp array, initially
of size 100000.

You might expect the above defstobj to define the accessor function mem
and the updater update-mem.  _That does not happen!_.

The above event defines the accessor function memi and the updater
update-memi.  These functions do not access/update the mem field of the
ms object; they access/update the individual elements of the array in
that field.

In particular, the logical definitions of the two functions are:

     (defun memi (i ms)
       (declare (xargs :guard
                       (and (msp ms)
                            (integerp i)
                            (<= 0 i)
                            (< i (mem-length ms)))))
       (nth i (nth 1 ms)))

     (defun update-memi (i v ms)
       (declare (xargs :guard
                       (and (msp ms)
                            (integerp i)
                            (<= 0 i)
                            (< i (mem-length ms))
                            (integerp v))))
       (update-nth-array 1 i v ms))

For example, to access the 511th (0-based) memory location of the
current ms you could evaluate:

     ACL2 !>(memi 511 ms)
     -1

The answer is -1 initially, because that is the above-specified initial
value of the elements of the mem array.

To set that element you could do

     ACL2 !>(update-memi 511 777 ms)
     <ms>
     ACL2 !>(memi 511 ms)
     777

The raw Lisp implementing these two functions is shown below.

     (defun memi (i ms)
       (declare (type (integer 0 268435455) i))
       (the integer
            (aref (the (simple-array integer (*))
                       (svref ms 1))
                  (the (integer 0 268435455) i))))

     (defun update-memi (i v ms)
       (declare (type (integer 0 268435455) i)
                (type integer v))
       (progn
        (setf (aref (the (simple-array integer (*))
                         (svref ms 1))
                    (the (integer 0 268435455) i))
              (the integer v))
        ms))

If you want to see the raw Lisp supporting a defstobj, execute the
defstobj and then evaluate the ACL2 form (nth 4 (global-val
'cltl-command (w state))).

To continue the stobj tour, see STOBJ-EXAMPLE-3.

STOBJ-EXAMPLE-3    another example of a single-threaded object

The event

     (defstobj $s
       (x :type integer :initially 0)
       (a :type (array (integer 0 9) (3)) :initially 9 :resizable t))

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.  (Under the hood, this "list" is actually implemented as
an array.)  Initially, the A field has three elements, each of which is
9.

This event introduces the following sequence of function 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 NIL ...)        ; 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

Here is the definition of $SP:

     (DEFUN $SP ($S)
       (DECLARE (XARGS :GUARD T :VERIFY-GUARDS T))
       (AND (TRUE-LISTP $S)
            (= (LENGTH $S) 2)
            (XP (NTH 0 $S))
            (AP (NTH 1 $S))
            T))

This reveals that in order to satisfy $SP an object must be a true list
of length 2 whose first element satisfies XP and whose second satisfies
AP.  By printing the definition of AP one learns that it requires its
argument to be a true list, each element of which is an integer between
0 and 9.

The initial value of stobj $S is given by zero-ary "creator" function
CREATE-$S.  Creator functions may only be used in limited contexts.
See WITH-LOCAL-STOBJ.

Here is the definition of UPDATE-AI, the updater for the A field at
index I:

     (DEFUN UPDATE-AI (I V $S)
       (DECLARE (XARGS :GUARD
                       (AND ($SP $S)
                            (INTEGERP I)
                            (<= 0 I)
                            (< I (A-LENGTH $S))
                            (AND (INTEGERP V) (<= 0 V) (<= V 9)))
                       :VERIFY-GUARDS T))
       (UPDATE-NTH-ARRAY 1 I V $S))

By definition (UPDATE-NTH-ARRAY 1 I V $S) is (UPDATE-NTH 1 (UPDATE-NTH
I V (NTH 1 $S)) $S).  This may be a little surprising but should be
perfectly clear.

First, ignore the guard, since it is irrelevant in the logic.  Reading
from the inside out, (UPDATE-AI I V $S) extracts (NTH 1 $S), which is
array a of $S.  (Recall that NTH is 0-based.)  The next higher
expression in the definition above, (UPDATE-NTH I V a), "modifies" a by
setting its Ith element to V.  Call this a'.  The next higher
expression, (UPDATE-NTH 1 a' $S), "modifies" $S by setting its 1st
component to a'.  Call this result $s'.  Then $s' is the result
returned by UPDATE-AI.

So the first useful observation is that from the perspective of the
logic, the type "restrictions" on stobjs are irrelevant.  They are
"enforced" by ACL2's guard mechanism, not by the definitions of the
updater functions.

As one might also imagine, the accessor functions do not really "care,"
logically, whether they are applied to well-formed stobjs or not.  For
example, (AI I $S) is defined to be (NTH I (NTH 1 $S)).

Thus, you will not be able to prove that (AI 2 $S) is an integer.  That
is,

     (integerp (AI 2 $S))

is not a theorem, because $S may not be well-formed.

Now (integerp (AI 2 $S)) will always evaluate to T in the top-level
ACL2 command loop, because we insist that the current value of the
stobj $S always satisfies $SP by enforcing the guards on the updaters,
independent of whether guard checking is on or off; see
SET-GUARD-CHECKING.  But in a theorem $S is just another variable,
implicitly universally quantified.

So (integerp (AI 2 $S)) is not a theorem because it is not true when
the variable $S is instantiated with, say,

     '(1 (0 1 TWO))

because, logically speaking, (AI 2 '(1 (0 1 TWO))) evaluates to the
symbol TWO.  That is,

     (equal (AI 2 '(1 (0 1 TWO))) 'TWO)

is true.

However,

     (implies (and ($SP $S) (< 2 (A-LENGTH $S))) (integerp (AI 2 $S)))

is a theorem.  To prove it, you will have to prove a lemma about AP.
The following will do:

     (defthm ap-nth
       (implies (and (AP x)
                     (integerp i)
                     (<= 0 i)
                     (< i (len x)))
                (integerp (nth i x)))).

Similarly,

     (implies (and (integerp i)
                   (<= 0 i)
                   (< i (A-LENGTH $S))
                   (integerp v)
                   (<= 0 v)
                   (<= v 9))
              ($SP (UPDATE-AI i v $S)))

is not a theorem until you add the additional hypothesis ($SP $S).  To
prove the resulting theorem, you will need a lemma such as the
following.

     (defthm ap-update-nth
       (implies (and (AP a)
                     (integerp v)
                     (<= 0 v)
                     (<= v 9)
                     (integerp i)
                     (<= 0 i)
                     (< i (len a)))
                (AP (update-nth i v a))))

The moral here is that from the logical perspective, you must provide
the hypotheses that, as a programmer, you think are implicit on the
structure of your stobjs, and you must prove their invariance.  This is
a good area for further support, perhaps in the form of a library of
macros.

_Resizing Array Fields_

Recall the specification of the array field, A for the stobj $S
introduced above:

     (a :type (array (integer 0 9) (3)) :initially 9 :resizable t)

Logically, this field is a list, initially of length 3.  Under the
hood, this field is implemented using a Common Lisp array with 3
elements.  In some applications, one may wish to lengthen an array
field, or even (to reclaim space) to shrink an array field.  The
defstobj event provides functions to access the current length of an
array field and to change the array field, with default names obtained
by suffixing the field name with "LENGTH-" or prefixing it with
"RESIZE-," respectively.  The following log shows the uses of these
fields in the above example.

     ACL2 !>(A-LENGTH $S)
     3
     ACL2 !>(RESIZE-A 10 $S) ; change length of A to 10
     <$s>
     ACL2 !>(A-LENGTH $S)
     10
     ACL2 !>(AI 7 $S)        ; new elements get value from :initially
     9
     ACL2 !>(RESIZE-A 2 $S)  ; truncate A down to first 2 elements
     <$s>
     ACL2 !>(A-LENGTH $S)
     2
     ACL2 !>(AI 7 $S)        ; error:  access past array bound

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol AI, which
     is (AND ($SP $S) (INTEGERP I) (<= 0 I) (< I (A-LENGTH $S))), is violated
     by the arguments in the call (AI 7 $S).

     ACL2 !>

Here are the definitions of the relevant functions for the above
example; also see RESIZE-LIST.

     (DEFUN A-LENGTH ($S)
       (DECLARE (XARGS :GUARD ($SP $S) :VERIFY-GUARDS T))
       (LEN (NTH 1 $S)))

     (DEFUN RESIZE-A (K $S)
       (DECLARE (XARGS :GUARD ($SP $S) :VERIFY-GUARDS T))
       (UPDATE-NTH 1
                   (RESIZE-LIST (NTH 1 $S) K 9)
                   $S))

It is important to note that the implementation of array resizing in
ACL2 involves copying the entire array into a newly allocated space and
thus can be quite costly if performed often.  This approach was chosen
in order to make array access and update as efficient as possible, with
the suspicion that for most applications, array access and update are
considerably more frequent than resizing (especially if the programmer
is aware of the relative costs beforehand).

It should also be noted that computations of lengths of stobj array
fields should be fast (constant-time) in all or most Common Lisp
implementations.

Finally, if :resizable t is not supplied as shown above, then an
attempt to resize the array will result in an error.  If you do not
intend to resize the array, it is better to omit the :resizable option
(or to supply :resizable nil), since then the length function will be
defined to return a constant, namely the initial length, which can
simplify guard proofs (compare with the definition of A-LENGTH above).

This completes the tour through the documentation of stobjs.  However,
you may now wish to read the documentation for the event that
introduces a new single-threaded object; see DEFSTOBJ.

WITH-LOCAL-STOBJ    locally bind a single-threaded object

See STOBJ for an introduction to single-threaded objects.

     Example Form:
     (with-local-stobj
      st
      (mv-let (result st)
              (compute-with-st x st)
              result))

With-local-stobj can be thought of as a macro, where the example form
above expands as follows.

     (mv-let (result st)
             (let ((st (create-st)))
               (compute-with-st x st))
             (declare (ignore st))
             result)

However, ACL2 expects you to use with-local-stobj, not its expansion.
More precisely, stobj creator functions are not allowed except
(implicitly) via with-local-stobj and in logic-only situations (like
theorems and hints).  Moreover, neither with-local-stobj nor its
expansions are legal when typed directly at the top-level loop.

     General Forms:
     (with-local-stobj stobj-name mv-let-form)
     (with-local-stobj stobj-name mv-let-form creator-name)

where stobj-name is the name of a stobj other than state, mv-let-form
is a call of mv-let, and if creator-name is supplied then it should be
the  name of the creator function for stobj-name; see DEFSTOBJ.
For the example form above, its expansion would use creator-name, if
supplied, in place of create-st.

With-local-stobj can be useful when a stobj is used to memoize
intermediate results during a computation, yet it is desired not to
make the stobj a formal parameter for the function and its callers.

ACL2 can reason about these "local stobjs," and in particular about
stobj creator functions.  For technical reasons, ACL2 will not allow
you to enable the :EXECUTABLE-COUNTERPART rune of a stobj creator
function.

Finally, here is a small example concocted ino rder to illustrate that
with-local-stobj calls can be nested.

     (defstobj st fld1)

     (defun foo ()
       (with-local-stobj
        st ; Let us call this the ``outer binding of st''.
        (mv-let (val10 val20 st)
          (let ((st (update-fld1 10 st)))
            ;; At this point the outer binding of st has fld1 = 10.
            (let ((result (with-local-stobj
                           st ; Let us call this the ``inner binding of st''.
                           (mv-let (val st)
                             (let ((st (update-fld1 20 st)))
                               ;; Now fld1 = 20 for the inner binding of st.
                               (mv (fld1 st) st))
                             val))))
              ;; So result has been bound to 20 above, but here we are once again
              ;; looking at the outer binding of st, where fld1 is still 10.
              (mv (fld1 st) result st)))
          (mv val10 val20))))

     (thm (equal (foo) (mv 10 20))) ; succeeds

THEORIES    sets of runes to enable/disable in concert

     Example: '((:definition app)
                (:executable-counterpart app)
                rv
                (rv)
                assoc-of-app)

See:

Related topics other than immediate subtopics:

A theory is a list of "runic designators" as described below.  Each
runic designator denotes a set of "runes" (see RUNE) and by
unioning together the runes denoted by each member of a theory we
define the set of runes corresponding to a theory.  Theories are used
to control which rules are "enabled," i.e., available for automatic
application by the theorem prover.  There is always a "current" theory.
A rule is enabled precisely if its rune is an element of the set of
runes corresponding to the current theory.  At the top-level, the
current theory is the theory selected by the most recent in-theory
event, extended with the rule names introduced since then.  Inside the
theorem prover, the :in-theory hint (see HINTS) can be used to
select a particular theory as current during the proof attempt for a
particular goal.

Theories are generally constructed by "theory expressions."  Formally,
a theory expression is any term, containing at most the single free
variable world, that when evaluated with world bound to the current
ACL2 world (see WORLD) produces a theory.  ACL2 provides
various functions for the convenient construction and manipulation of
theories.  These are called "theory functions" (see
THEORY-FUNCTIONS).  For example, the theory function union-theories
takes two theories and produces their union.  The theory function
universal-theory returns the theory containing all known rule names as
of the introduction of a given logical name.  But a theory expression
can contain constants, e.g.,

     '(assoc (assoc) (:rewrite car-cons) car-cdr-elim)

and user-defined functions.  The only important criterion is that a
theory expression mention no variable freely except world and evaluate
to a theory.

More often than not, theory expressions typed by the user do not
mention the variable world.  This is because user-typed theory
expressions are generally composed of applications of ACL2's theory
functions.  These "functions" are actually macros that expand into
terms in which world is used freely and appropriately.  Thus, the
technical definition of "theory expression" should not mislead you into
thinking that interestng theory expressions must mention world; they
probably do and you just didn't know it!

One aspect of this arrangement is that theory expressions cannot
generally be evaluated at the top-level of ACL2, because world is not
bound.  To see the value of a theory expression, expr, at the
top-level, type

     ACL2 !>(LET ((WORLD (W STATE))) expr).

However, because the built-in theories are quite long, you may be sorry
you printed the value of a theory expression!

A theory is a true list of runic designators and to each theory there
corresponds a set of runes, obtained by unioning together the sets of
runes denoted by each runic designator.  For example, the theory
constant

        '(assoc (assoc) (:rewrite car-cons) car-cdr-elim)

corresponds to the set of runes

        {(:definition assoc)
         (:induction assoc)
         (:executable-counterpart assoc)
         (:elim car-cdr-elim)
         (:rewrite car-cons)} .

Observe that the theory contains four elements but its runic
correspondent contains five.  That is because some designators denote
sets of several runes.  If the above theory were selected as current
then the five rules named in its runic counterpart would be enabled and
all other rules would be disabled.

We now precisely define the runic designators and the set of runes
denoted by each.

     o A rune is a runic designator and denotes the singleton set
     containing that rune.

     o If symb is a function symbol introduced with a defun (or defuns)
     event, then symb is a runic designator and denotes the set
     containing the runes (:definition symb) and (:induction symb),
     omitting the latter if no such induction rule exists (presumably
     because the function's definition is not singly recursive).

     o If symb is a function symbol introduced with a defun (or defuns)
     event, then (symb) is a runic designator and denotes the singleton
     set containing the rune (:executable-counterpart symb).

     o If symb is the name of a defthm (or defaxiom) event that
     introduced at least one rule, then symb is a runic designator and
     denotes the set of the names of all rules introduced by the named
     event.

     o If str is the string naming some defpkg event and symb is the
     symbol returned by (intern str "ACL2"), then symb is a runic
     designator and denotes the singleton set containing (:rewrite
     symb), which is the name of the rule stating the conditions under
     which the symbol-package-name of (intern x str) is str.

     o If symb is the name of a deftheory event, then symb is a runic
     designator and denotes the runic theory corresponding to symb.

These conventions attempt to implement the Nqthm-1992 treatment of
theories.  For example, including a function name, e.g., assoc, in the
current theory enables that function but does not enable the executable
counterpart.  Similarly, including (assoc) enables the executable
counterpart (Nqthm's *1*assoc) but not the symbolic definition.  And
including the name of a proved lemma enables all of the rules added by
the event.  These conventions are entirely consistent with Nqthm usage.
Of course, in ACL2 one can include explicitly the runes naming the
rules in question and so can avoid entirely the use of non-runic
elements in theories.

Because a rune is a runic designator denoting the set containing that
rune, a list of runes is a theory and denotes itself.  We call such
theories "runic theories."  To every theory there corresponds a runic
theory obtained by unioning together the sets denoted by each
designator in the theory.  When a theory is selected as "current" it is
actually its runic correspondent that is effectively used.  That is, a
rune is enabled iff it is a member of the runic correspondent of the
current theory.  The value of a theory defined with deftheory is the
runic correspondent of the theory computed by the defining theory
expression.  The theory manipulation functions, e.g., union-theories,
actually convert their theory arguments to their runic correspondents
before performing the required set operation.  The manipulation
functions always return runic theories.  Thus, it is sometimes
convenient to think of (non-runic) theories as merely abbreviations for
their runic correspondents, abbreviations which are "expanded" at the
first opportunity by theory manipulation functions and the "theory
consumer" functions such as in-theory and deftheory.

ACTIVE-RUNEP    check that a rune exists and is enabled

     Example:
     (active-runep '(:rewrite left-to-right))

     General Form:
     (active-runep rune)

where rune has the shape of a rune.  This macro expands to an
expression using the variables ens and state, and returns non-nil when
the given rune exists and is enabled (according to the given "enabled
structure," ens, and the current logical world of the given state).
See THEORY-INVARIANT for how this macro can be of use.

CURRENT-THEORY    currently enabled rules as of logical name

     Examples:
     (current-theory :here)
     (current-theory 'lemma3)

See LOGICAL-NAME.

     General Form:
     (current-theory logical-name)

Returns the current theory as it existed immediately after the
introduction of logical-name provided it is evaluated in an environment
in which the variable symbol WORLD is bound to the current ACL2 logical
world, (w state).  Thus,

     ACL2 !>(current-theory :here)

will cause an (unbound variable) error while

     ACL2 !>(let ((world (w state))) (current-theory :here))

will return the current theory in world.

See THEORIES and see LOGICAL-NAME for a discussion of
theories in general and why the commonly used "theory functions" such
as current-theory are really macros that expand into terms involving
the variable world.

The theory returned by current-theory is in fact the theory selected by
the in-theory event most recently preceding logical name, extended by
the rules introduced up through logical-name.

You may experience a fencepost problem in deciding which logical name
to use.  Deflabel can always be used to mark unambiguously for future
reference a particular point in the development of your theory.  The
order of events in the vicinity of an encapsulate is confusing.  See
ENCAPSULATE.

This "function" is actually a macro that expands to a term mentioning
the single free variable world.  When theory expressions are evaluated
by in-theory or the :in-theory hint, world is bound to the current ACL2
world.

DISABLE    deletes names from current theory

     Example:
     (disable fact (fact) associativity-of-app)

     General Form:
     (disable name1 name2 ... namek)

where each namei is a runic designator; see THEORIES.  The
result is the theory that contains all the names in the current theory
except those listed.  Note that this is merely a function that returns
a theory.  The result is generally a very long list of runes and you
will probably regret printing it.

The standard way to "disable" a fixed set of names, is as follows; see
HINTS and see IN-THEORY.

     :in-theory (disable name1 name2 ... namek)    ; in a hint
     (in-theory (disable name1 name2 ... namek))   ; as an event
     (local ; often desirable, to avoid exporting from the current context
      (in-theory (disable name1 name2 ... namek)))

Note that all the names are implicitly quoted.  If you wish to disable
a computed list of names, lst, use the theory expression
(set-difference-theories (current-theory :here) lst).

E/D    enable/disable rules

The macro e/d creates theory expressions for use in in-theory hints and
events.  It provides a convenient way to enable and disable
simultaneously, without having to write arcane theory expressions.

     Examples:
     (e/d (lemma1 lemma2))          ; equivalent to (enable lemma1 lemma2)
     (e/d () (lemma))               ; equivalent to (disable lemma)
     (e/d (lemma1) (lemma2 lemma3)) ; Enable lemma1 then disable lemma2, lemma3.
     (e/d () (lemma1) (lemma2))     ; Disable lemma1 then enable lemma2.

     General Form:
     (e/d enables-0 disables-0 ... enables-n disables-n)

where each enables-i and disables-i is a list of runic designators; see
THEORIES, see ENABLE, and see DISABLE.

The e/d macro takes any number of lists suitable for the enable and
disable macros, and creates a theory that is equal to (current-theory
:here) after executing the following commands.

(in-theory (enable . enables-0)) (in-theory (disable . disables-0))
[etc.]  (in-theory (enable . enables-n)) (in-theory (disable .
disables-n))

ENABLE    adds names to current theory

     Example:
     (enable fact (fact) associativity-of-app)

     General Form:
     (enable name1 name2 ... namek)

where each namei is a runic designator; see THEORIES.  The
result is the theory that contains all the names in the current theory
plus those listed.  Note that this is merely a function that returns a
theory.  The result is generally a very long list of runes and you will
probably regret printing it.

The standard way to "enable" a fixed set of names, is as follows; see
HINTS and see IN-THEORY.

     :in-theory (enable name1 name2 ... namek)  ; in a hint
     (in-theory (enable name1 name2 ... namek)) ; as an event
     (local ; often desirable, to avoid exporting from the current context
      (in-theory (enable name1 name2 ... namek)))

Note that all the names are implicitly quoted.  If you wish to enable a
computed list of names, lst, use the theory expression (union-theories
(current-theory :here) lst).

EXECUTABLE-COUNTERPART-THEORY    executable counterpart rules as of logical name

     Examples:
     (executable-counterpart-theory :here)
     (executable-counterpart-theory 'lemma3)

See LOGICAL-NAME.

     General Form:
     (executable-counterpart-theory logical-name)

Returns the theory containing all the :executable-counterpart runes,
whether enabled or not, that existed immediately after logical-name was
introduced.  See the documentation for theories, logical-name,
executable-counterpart and function-theory.

You may experience a fencepost problem in deciding which logical name
to use.  Deflabel can always be used to mark unambiguously for future
reference a particular point in the development of your theory.  The
order of events in the vicinity of an encapsulate is confusing.  See
ENCAPSULATE.

This "function" is actually a macro that expands to a term mentioning
the single free variable world.  When theory expressions are evaluated
by in-theory or the :in-theory hint, world is bound to the current ACL2
world.

FUNCTION-THEORY    function symbol rules as of logical name

     Examples:
     (function-theory :here)
     (function-theory 'lemma3)

See LOGICAL-NAME.

     General Form:
     (function-theory logical-name)

Returns the theory containing all the :definition runes, whether
enabled or not, that existed immediately after logical-name was
introduced.  See the documentation for theories, logical-name and
executable-counterpart-theory.

You may experience a fencepost problem in deciding which logical name
to use.  Deflabel can always be used to mark unambiguously for future
reference a particular point in the development of your theory.  The
order of events in the vicinity of an encapsulate is confusing.  See
ENCAPSULATE.

This "function" is actually a macro that expands to a term mentioning
the single free variable world.  When theory expressions are evaluated
by in-theory or the :in-theory hint, world is bound to the current ACL2
world.

GROUND-ZERO    enabled rules in the startup theory

ACL2 concludes its initialization (boot-strapping) procedure by
defining the theory ground-zero; see THEORIES.  In fact, this
theory is just the theory defined by (current-theory :here) at the
conclusion of initialization; see CURRENT-THEORY.

Note that by evaluating the event

     (in-theory (current-theory 'ground-zero))

you can restore the current theory to its value at the time you started
up ACL2.

INCOMPATIBLE    declaring that two rules should not both be enabled

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

     General Form:
     (incompatible rune1 rune2)

where rune1 and rune2 are two specific runes.  The arguments are not
evaluated.  Invariant is just a macro that expands into a term that
checks that not both runes are enabled.  See THEORY-INVARIANT.

INTERSECTION-THEORIES    intersect two theories

     Example:
     (intersection-theories (current-theory :here)
                            (theory 'arith-patch))

     General Form:
     (intersection-theories th1 th2)

where th1 and th2 are theories (see THEORIES).  To each of the
arguments there corresponds a runic theory.  This function returns the
intersection of those two runic theories, represented as a list and
ordered chronologically.

This "function" is actually a macro that expands to a term mentioning
the single free variable world.  When theory expressions are evaluated
by in-theory or the :in-theory hint, world is bound to the current ACL2
world.

MINIMAL-THEORY    a minimal theory to enable

This theory (see THEORIES) enables only a few built-in
functions and executable counterparts.  It can be useful when you want
to formulate lemmas that rather immediately imply the theorem to be
proved, by way of a :use hint (see HINTS), for example as
follows.

     :use (lemma-1 lemma-2 lemma-3)
     :in-theory (union-theories '(f1 f2) (theory 'minimal-theory))

In this example, we expect the current goal to follow from lemmas
lemma-1, lemma-2, and lemma-3 together with rules f1 and f2 and some
obvious facts about built-in functions (such as the definition of
implies and the :executable-counterpart of car).  The :in-theory hint
above is intended to speed up the proof by turning off all inessential
rules.

RULE-NAMES    How rules are named.

     Examples:
     (:rewrite assoc-of-app)
     (:linear delta-aref . 2)
     (:definition length)
     (:executable-counterpart length)

See RUNE.

RUNE    a rule name

     Examples:
     (:rewrite assoc-of-app)
     (:linear delta-aref . 2)
     (:definition length)
     (:executable-counterpart length)

Background: The theorem prover is driven from a data base of rules.
The most common rules are :rewrite rules, which cause the simplifier to
replace one term with another.  Events introduce rules into the data
base.  For example, a defun event may introduce runes for symbolically
replacing a function call by its instantiated body, for evaluating the
function on constants, for determining the type of a call of the
function, and for the induction scheme introduced upon defining the
function.  Defthm may introduce several rules, one for each of the
:rule-classes specified (where one rule class is specified if
:rule-classes is omitted, namely, :rewrite).

Every rule in the system has a name.  Each name is a structured object
called a "rune," which is short for "rule name".  Runes are always of
the form (:token symbol . x), where :token is some keyword symbol
indicating what kind of rule is named, symbol is the event name that
created the rule (and is called the "base symbol" of the rune), and x
is either nil or a natural number that makes the rule name distinct
from that of rules generated by other events or by other :rule-classes
within the same event.

For example, an event of the form

     (defthm name thm
       :rule-classes ((:REWRITE :COROLLARY term1)
                      (:REWRITE :COROLLARY term2)
                      (:ELIM    :COROLLARY term3)))

typically creates three rules, each with a unique rune.  The runes are

     (:REWRITE name . 1), (:REWRITE name . 2), and (:ELIM name).

However, a given formula may create more than one rule, and all rules
generated by the same :corollary formula will share the same rune.
Consider the following example.

     (defthm my-thm
       (and (equal (foo (bar x)) x)
            (equal (bar (foo x)) x)))

This is treated identically to the following.

     (defthm my-thm
       (and (equal (foo (bar x)) x)
            (equal (bar (foo x)) x))
       :rule-classes ((:rewrite
                       :corollary
                       (and (equal (foo (bar x)) x)
                            (equal (bar (foo x)) x)))))

In either case, two rules are created: one rewriting (foo (bar x)) to
x, and one rewriting (bar (foo x)) to x.  However, only a single rune
is created, (:REWRITE MY-THM), because there is only one rule class.
But now consider the following example.

     (defthm my-thm2
       (and (equal (foo (bar x)) x)
            (equal (bar (foo x)) x))
       :rule-classes ((:rewrite
                       :corollary
                       (and (equal (foo (bar x)) x)
                            (equal (bar (foo x)) x)))
                      (:rewrite
                       :corollary
                       (and (equal (foo (bar (foo x))) (foo x))
                            (equal (bar (foo (bar x))) (bar x))))))

This time there are four rules created.  The first two rules are as
before, and are assigned the rune (:REWRITE MY-THM . 1).  The other two
rules are similarly generated for the second :corollary, and are
assigned the rune (:REWRITE MY-THM . 2).

The function corollary will return the corollary term associated with a
given rune in a given world.  Example:

     (corollary '(:TYPE-PRESCRIPTION DIGIT-TO-CHAR) (w state))

However, the preferred way to see the corollary term associated with a
rune or a name is to use :pf; see PF.

The defun event creates as many as four rules.  (:definition fn) is the
rune given to the equality axiom defining the function, fn.
(:executable-counterpart fn) is the rune given to the rule for computing
fn on known arguments.  A type prescription rule may be created under
the name (:type-prescription fn), and an induction rule may be created
under the name (:induction fn).

Runes may be individually enabled and disabled, according to whether
they are included in the current theory.  See THEORIES.  Thus,
it is permitted to disable (:elim name), say, while enabling the other
rules derived from name.  Similarly, (:definition fn) may be disabled
while (:executable-counterpart fn) and the type prescriptions for fn
are enabled.

Associated with most runes is the formula justifying the rule named.
This is called the "corollary formula" of the rune and may be obtained
via the function corollary, which takes as its argument a rune and a
property list world.  Also see PF.  The corollary formula for
(:rewrite name . 1) after the defthm event above is term1.  The
corollary formulas for (:definition fn) and (:executable-counterpart
fn) are always identical: the defining axiom.  Some runes, e.g.,
(:definition car), do not have corollary formulas.  Corollary returns
nil on such runes.  In any case, the corollary formula of a rune, when
it is non-nil, is a theorem and may be used in the :use and :by hints.

Note: The system has many built in rules that, for regularity, ought to
have names but don't because they can never be disabled.  One such rule
is that implemented by the linear arithmetic package.  Because many of
our subroutines are required by their calling conventions to return the
justifying rune, we have invented the notion of "fake runes." Fake
runes always have the base symbol nil, use a keyword token that
includes the phrase "fake-rune", and are always enabled.  For example,
(:fake-rune-for-linear nil) is a fake rune.  Occasionally the system
will print a fake rune where a rune is expected.  For example, when the
linear arithmetic fake rune is reported among the rules used in a
proof, it is an indication that the linear arithmetic package was used.
However, fake runes are not allowed in theories, they cannot be
enabled or disabled, and they do not have associated corollary
formulas.  In short, despite the fact that the user may sometimes see
fake runes printed, they should never be typed.

SET-DIFFERENCE-THEORIES    difference of two theories

     Example:
     (set-difference-theories (current-theory :here)
                              '(fact (fact)))

     General Form:
     (set-difference-theories th1 th2)

where th1 and th2 are theories (see THEORIES).  To each of the
arguments there corresponds a runic theory.  This function returns the
set-difference of those two runic theories, represented as a list and
ordered chronologically.  That is, a rune is in the result iff it is in
the first runic theory but not in the second.

The standard way to "disable" a theory, lst, is: (in-theory
(set-difference-theories (current-theory :here) lst)).

This "function" is actually a macro that expands to a term mentioning
the single free variable world.  When theory expressions are evaluated
by in-theory or the :in-theory hint, world is bound to the current ACL2
world.

THEORY    retrieve named theory

     Example:
     (theory 'ground-zero)

In the example above, the theory returned is the one in force when ACL2
is started up (see GROUND-ZERO).

     General Form:
     (theory name)

where name is the name of a previously executed deftheory event.
Returns the named theory.  See THEORIES.

This "function" is actually a macro that expands to a term mentioning
the single free variable world.  When theory expressions are evaluated
by in-theory or the :in-theory hint, world is bound to the current ACL2
world.

THEORY-FUNCTIONS    functions for obtaining or producing theories

     Example Calls of Theory Functions:
     (universal-theory :here)
     (union-theories th1 th2)
     (set-difference-theories th1 th2)

The theory functions are documented individually:

Related topics other than immediate subtopics:

The functions (actually, macros) mentioned above are convenient ways to
produce theories.  (See THEORIES.) Some, like universal-theory,
take a logical name (see LOGICAL-NAME) as an argument and
return the relevant theory as of the time that name was introduced.
Others, like union-theories, take two theories and produce a new one.
See REDUNDANT-EVENTS for a caution about the use of logical
names in theory expressions.

Theory expressions are generally composed of applications of theory
functions.  Formally, theory expressions are expressions that involve,
at most, the free variable world and that when evaluated with world
bound to the current ACL2 world (see WORLD) return theories.
The "theory functions" are actually macros that expand into forms that
involve the free variable world.  Thus, for example (universal-theory
:here) actually expands to (universal-theory-fn :here world) and when
that form is evaluated with world bound to the current ACL2 world,
universal-theory-fn scans the ACL2 property lists and computes the
current universal theory.  Because the theory functions all implicitly
use world, the variable does not generally appear in anything the user
types.

UNION-THEORIES    union two theories

     Example:
     (union-theories (current-theory 'lemma3)
                     (theory 'arith-patch))

     General Form:
     (union-theories th1 th2)

where th1 and th2 are theories (see THEORIES).  To each of the
arguments there corresponds a runic theory.  This function returns the
union of those two runic theories, represented as a list and ordered
chronologically.

This "function" is actually a macro that expands to a term mentioning
the single free variable world.  When theory expressions are evaluated
by in-theory or the :in-theory hint, world is bound to the current ACL2
world.

UNIVERSAL-THEORY    all rules as of logical name

     Examples:
     (universal-theory :here)
     (universal-theory 'lemma3)

See LOGICAL-NAME.

     General Form:
     (universal-theory logical-name)

Returns the theory consisting of all the runes that existed immediately
after logical-name was introduced.  See THEORIES and see
LOGICAL-NAME.  The theory includes logical-name itself (if there is a
rule by that name).  (Note that since some events do not introduce
rules (e.g., defmacro, defconst or defthm with :rule-classes nil), the
universal-theory does not necessarily include a rune for every event
name.)  The universal-theory is very long and you will probably regret
printing it.

You may experience a fencepost problem in deciding which logical-name
to use.  Deflabel can always be used to mark unambiguously for future
reference a particular point in the development of your theory.  This
is convenient because deflabel does not introduce any rules and hence
it doesn't matter if you count it as being in the interval or not.  The
order of events in the vicinity of an encapsulate is confusing.  See
ENCAPSULATE.

This "function" is actually a macro that expands to a term mentioning
the single free variable world.  When theory expressions are evaluated
by in-theory or the :in-theory hint, world is bound to the current ACL2
world.

Also see CURRENT-THEORY.  Current-theory is much more commonly
used than universal-theory.  The former includes only the enabled runes
as of the given logical-name, which is probably what you want, while
the latter includes disabled ones as well.

TRACE    tracing functions in ACL2

ACL2 provides utilities that rely on the underlying Lisp image to trace
functions.  There are two interfaces to the underlying lisp trace:

     o Macros trace$ and untrace$ call the underlying Lisp's trace and
     untrace, respectively.  See TRACE$ and see
     UNTRACE$.

     o Macro with-error-trace, or wet for short, provides a backtrace
     showing function calls that lead to an error.  See WET.

NOTES:

1. Wet turns off all tracing (i.e., executes Lisp (untrace)) other than
temporarily doing some tracing under-the-hood in the evaluation of the
form supplied to it.

2. The underlying Lisp trace and untrace utilities have been modified
for GCL and Allegro CL to trace the executable counterparts.  Other
Lisps may give unsatisfying results.  For GCL and Allegro CL, you can
invoke the original trace and untrace by exiting the ACL2 loop and
invoking old-trace and old-untrace, respectively..

3. Trace output for trace$ and untrace$ can be redirected to a file.
See OPEN-TRACE-FILE and see CLOSE-TRACE-FILE.  However,
the backtrace printed by wet always goes to standard-co.

BREAK-ON-ERROR    break when encountering a hard or soft error caused by ACL2

     General forms:
     (break-on-error t)   ; installs a trace causing a continuable error (break)
                          ;   whenever an error is invoked by ACL2.
     (break-on-error)     ; same as above
     (break-on-error nil) ; uninstall the above trace

(Break-on-error) generates roughly the following in raw Lisp:

     (trace (error1 :entry nil :exit (break)))

This trace should cause entry to the Lisp debugger (at least in most
Lisps) whenever ACL2 calls its error routines.

NOTE: Break-on-error causes a hard error if the underlying Lisp does not
comprehend the :entry and :exit keywords for trace$.  As of this
writing, break-on-error works in OpenMCL, GCL, and Allegro CL.

Also see TRACE$.

CLOSE-TRACE-FILE    stop redirecting trace output to a file

     General Form:
     (close-trace-file) ; trace output is no longer redirected to a file

Output from trace$ normally goes to the screen, or more precisely,
standard-co.  It can be redirected to a file; see
OPEN-TRACE-FILE.  Use close-trace-file to redirect trace output to
standard-co.