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.

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)
         (:executable-counterpart assoc)
         (:rewrite car-cons)
         (:rewrite car-cdr-elim)
         (:elim car-cdr-elim)} .

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.

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:

     (in-theory (disable name1 name2 ... namek)) ; globally
     :in-theory (disable name1 name2 ... namek)  ; locally

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

     (in-theory (enable name1 name2 ... namek)) ; globally
     :in-theory (enable name1 name2 ... namek)  ; locally

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 executing 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 theory does not contain both runes.  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 as many as four rules:
one for symbolically replacing a function call by its instantiated body,
one for evaluating the function on constants, and two for determining
the type of a call of the function (one of which is deduced before guard
verification and the other of which is deduced after guard
verification).  Defthm may introduce several rules, one for each of the
:rule-classes specified (where one rule class is specified if
:ilc[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 THEORIESand 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 a hard or soft error is invoked by ACL2.
     (break-on-error)     ; same as above
     (break-on-error nil) ; uninstall the above trace

(Break-on-error) is actually a macro that expands as follows.

     (trace$ (illegal :entry (break))
             (error1  :entry (break)))

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

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.

OPEN-TRACE-FILE    redirect trace output to a file

     Example:
     (open-trace-file "foo") ; trace output will go to file foo

     General Form:
     (open-trace-file filename) ; trace output will go to file filename

Output from trace$ normally goes to the screen, i.e., standard-co.  But
it can be redirected to a file as shown above.  See
CLOSE-TRACE-FILE for how to send trace output back to the screen.

Note that the backtrace printed by wet always goes to standard-co, even
after the use of open-trace-file.

TRACE$    trace the indicated functions

     Example:
     (trace$ foo bar)

     General Form:
     (trace$ fn1 fn2 ... fnk)

where the fni are defined or even constrained functions.

see UNTRACE$ for how to undo the effect of trace$.

Basically, trace$ calls on the underlying Lisp to trace the specified
functions as well as their executable-counterparts.  However, for GCL,
Allegro CL, and OpenMCL, the underlying Lisp trace routines are modified
before an image is saved in order to hide the ACL2 world and other large
data structures and provide slightly prettier output.

Recursive calls of functions whose guards have not been verified will
not generally be traced.  If you want to see traces for corresponding
evaluations in raw Lisp, which will generally show recursive calls
(except, in some Lisp implementations, for compiled tail recursive
functions), then you can quit into raw Lisp (:q) and execute your form
there.  Alternatively, you can avoid executable-counterpart functions by
using :set-raw-mode to enter a raw Lisp version of the ACL2 loop,
provided you do not intend to run certify-book later in that session;
see SET-RAW-MODE.

Output from trace$ normally goes to the screen, i.e., standard-co.  But
it can be redirected to a file; see OPEN-TRACE-FILE.

Also see WET ("with-error-trace") for a different way that ACL2
takes advantage of the underlying Lisp, namely to provide a backtrace
when there is an error.

Note that from a logical perspective all trace printing is a fiction.
For a related fiction, see CW.  Trace$ returns nil.

The following example will give an idea of the options available other
than just (trace$ fn1 fn2 ... fnk).  It works about as shown in Allegro
CL and GCL, but in OpenMCL the recursive calls are omitted unless you
escape into raw Lisp and redefine fact with (declare (notinline fact)).

     ACL2 !>(defun fact (n)
              (declare (xargs :guard (natp n) :mode :program))
              (if (zp n)
                  1
                (* n (fact (1- n)))))

     Summary
     Form:  ( DEFUN FACT ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FACT
     ACL2 !>(trace$ (fact :entry (car arglist) :exit values))
     NIL
     ACL2 !>(fact 5)
     1> (ACL2_*1*_ACL2::FACT . 5)
       2> (FACT . 5)
         3> (FACT . 4)
           4> (FACT . 3)
             5> (FACT . 2)
               6> (FACT . 1)
                 7> (FACT . 0)
                 <7 (FACT 1)
               <6 (FACT 1)
             <5 (FACT 2)
           <4 (FACT 6)
         <3 (FACT 24)
       <2 (FACT 120)
     <1 (ACL2_*1*_ACL2::FACT 120)
     120
     ACL2 !>

Here is another example.

     ACL2 !>(defun fact2 (n acc)
              (declare (xargs :guard (and (natp n) (natp acc))))
              (if (zp n)
                  (mv acc (* 2 acc))
                (fact2 (1- n) (* n acc))))

     The admission of FACT2 is trivial, using the relation O< (which is
     known to be well-founded on the domain recognized by O-P) and the measure
     (ACL2-COUNT N).  We observe that the type of FACT2 is described by
     the theorem (AND (CONSP (FACT2 N ACC)) (TRUE-LISTP (FACT2 N ACC))).
     We used primitive type reasoning.

     (FACT2 * *) => (MV * *).

     The guard conjecture for FACT2 is trivial to prove.  FACT2 is compliant
     with Common Lisp.

     Summary
     Form:  ( DEFUN FACT2 ...)
     Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER)
             (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
             (:FAKE-RUNE-FOR-TYPE-SET NIL))
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FACT2
     ACL2 !>(trace$ (fact2 :entry (list 'my-entry (car arglist))
                           :exit (list 'my-second-value (cadr values))))
     NIL
     ACL2 !>(fact2 6 1)

       1> (ACL2_*1*_ACL2::FACT2 MY-ENTRY 6)>
         2> (FACT2 MY-ENTRY 6)>
           3> (FACT2 MY-ENTRY 5)>
             4> (FACT2 MY-ENTRY 4)>
               5> (FACT2 MY-ENTRY 3)>
                 6> (FACT2 MY-ENTRY 2)>
                   7> (FACT2 MY-ENTRY 1)>
                     8> (FACT2 MY-ENTRY 0)>
                     <8 (FACT2 MY-SECOND-VALUE 1440)>
                   <7 (FACT2 MY-SECOND-VALUE 1440)>
                 <6 (FACT2 MY-SECOND-VALUE 1440)>
               <5 (FACT2 MY-SECOND-VALUE 1440)>
             <4 (FACT2 MY-SECOND-VALUE 1440)>
           <3 (FACT2 MY-SECOND-VALUE 1440)>
         <2 (FACT2 MY-SECOND-VALUE 1440)>
       <1 (ACL2_*1*_ACL2::FACT2 MY-SECOND-VALUE 1440)>
     (720 1440)
     ACL2 !>(trace$ (fact2 :entry (list 'my-args-reversed
                                        (list (cadr arglist) (car arglist)))
                           :exit (list 'values-reversed
                                       (cadr values) (car values))))
     NIL
     ACL2 !>(fact2 6 1)

       1> (ACL2_*1*_ACL2::FACT2 MY-ARGS-REVERSED (1 6))>
         2> (FACT2 MY-ARGS-REVERSED (1 6))>
           3> (FACT2 MY-ARGS-REVERSED (6 5))>
             4> (FACT2 MY-ARGS-REVERSED (30 4))>
               5> (FACT2 MY-ARGS-REVERSED (120 3))>
                 6> (FACT2 MY-ARGS-REVERSED (360 2))>
                   7> (FACT2 MY-ARGS-REVERSED (720 1))>
                     8> (FACT2 MY-ARGS-REVERSED (720 0))>
                     <8 (FACT2 VALUES-REVERSED 1440 720)>
                   <7 (FACT2 VALUES-REVERSED 1440 720)>
                 <6 (FACT2 VALUES-REVERSED 1440 720)>
               <5 (FACT2 VALUES-REVERSED 1440 720)>
             <4 (FACT2 VALUES-REVERSED 1440 720)>
           <3 (FACT2 VALUES-REVERSED 1440 720)>
         <2 (FACT2 VALUES-REVERSED 1440 720)>
       <1 (ACL2_*1*_ACL2::FACT2 VALUES-REVERSED 1440 720)>
     (720 1440)
     ACL2 !>