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

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

     Examples:
     (with-output
        :off summary      ; turn off the event summary when evaluating the following:
        :gag-mode :goals  ; use gag-mode, with goal names printed
        (defthm app-assoc (equal (app (app x y) z) (app x (app y z)))))

     (with-output ; turn off all output
      :off :all
      :gag-mode nil
      (thm (equal (app (app x y) z) (app x (app y z)))))

     (with-output ; same as above, showing all output types
      :off (error warning warning! observation prove proof-checker event expansion
                  summary proof-tree)
      :gag-mode nil
      (thm (equal (app (app x y) z) (app x (app y z)))))

     (with-output ; as above, but :stack :push says to save current
                  ; inhibit-output-lst, which can be restored in subsidiary
                  ; with-output call that specifies :stack :pop
      :stack :push
      :off :all
      :gag-mode nil
      (thm (equal (app (app x y) z) (app x (app y z)))))

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

where each :keyi is either :off, :on, :stack, or :gag-mode and vali is
as follows.  If :keyi is :off or :on, then vali can be :all, and
otherwise is a symbol or non-empty list of symbols representing output
types that can be inhibited; see SET-INHIBIT-OUTPUT-LST.  If
:keyi is :gag-mode, then :vali is one of the legal values for
:set-gag-mode.  Otherwise :keyi is :stack, in which case :vali is :push
or :pop; for now assume that :stack is not specified (we'll return to
it below).  The result of evaluating the General Form above is to
evaluate form, but in an environment where output occurs as follows.
If :on :all is specified, then all output is turned on except as
inhibited by :off; else if :off :all is specified, then all output is
inhibited except as specified by :on; and otherwise, the
currently-inhibited output types are reduced as specified by :on and
then extended as specified by :off.  But if :gag-mode is specified,
then before modifying how output is inhibited, gag-mode is set for the
evaluation of form as specified by the value of :gag-mode; see
SET-GAG-MODE.

Note: When the scope of with-output is exited, then all modifications
are undone, reverting gag-mode and the state of output inhibition to
those which were present before the with-output call was entered.

The :stack keyword's effect is illustrated by the following example,
where "(encapsulate nil)" may replaced by "(progn" without any change
to the output that is printed.

     (with-output
      :stack :push :off :all
      (encapsulate ()
        (defun f1 (x) x)
        (with-output :stack :pop (defun f2 (x) x))
        (defun f3 (x) x)
        (with-output :stack :pop :off warning (in-theory nil))
        (defun f4 (x) x)))

The outer with-output call saves the current output settings (as may
have been modified by earlier calls of set-inhibit-output-lst), by
pushing them onto a stack, and then turns off all output.  Each inner
with-output call temporarily pops that stack, restoring the starting
output settings, until it completes and undoes the effects of that pop.
Unless event output was inhibited at the top level (see
SET-INHIBIT-OUTPUT-LST), the following output is shown:

     Since F2 is non-recursive, its admission is trivial.  We observe that
     the type of F2 is described by the theorem (EQUAL (F2 X) X).

And then, if summary output was not inhibited at the top level, we get
the rest of this output:

     Summary
     Form:  ( DEFUN F2 ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

     Summary
     Form:  ( IN-THEORY NIL)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

Note that the use of :off warning supresses a "Theory" warning for the
(in-theory nil) event, and that in no case will output be printed for
definitions of f1, f3, or f4, or for the encapsulate event itself.

The following more detailed explanation of :stack is intended only for
advanced users.  After :gag-mode is handled (if present) but before :on
or :off is handled, the value of :stack is handled as follows.  If the
value is :push, then state global inhibit-output-lst-stack is modified
by pushing the value of state global inhibit-output-lst onto the value
of state global inhibit-output-lst-stack, which is nil at the top
level.  If the value is :pop, then state global
inhibit-output-lst-stack is modified only if non-nil, in which case its
top element is popped and becomes the value of of state global
inhibit-output-lst.

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

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

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

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

Note that with-output is allowed in books.  See
EMBEDDED-EVENT-FORM.

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 a trace utility, trace$, with corresponding reverse
operation untrace$.  These can be used without any dependence on the
underlying Lisp utility, and are the tracing utilities of choice in
ACL2; see TRACE$ and see UNTRACE$.

However, for advanced users we note that the underlying host Lisp may
also provide a trace utility, trace, and corresponding untrace.
Moreover, these have been modified in the case that the host Lisp is
GCL, Allegro CL, or CCL (OpenMCL), to provide limited support for
:entry, :exit, and perhaps :cond keywords, to hide certain large data
structures (world, enabled structure, rewrite constant), and to trace
executable counterparts.  See source files *-trace.lisp.  For the above
Lisps, you can invoke the original trace and untrace by invoking
old-trace and old-untrace, respectively, in raw Lisp rather than in the
normal ACL2 loop.

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:

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

This trace should cause entry to the Lisp debugger 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$.

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.

SET-TRACE-EVISC-TUPLE    set the trace evisc tuple

A trace evisc-tuple, which is set by this utility, provides a means to
restrict printing during tracing.  By default the ACL2 trace mechanism,
trace$, automatically deals with stobjs, the logical world, and certain
other large structures.  See TRACE$, in particular the
documentation of trace$ option :hide.  However, even with that default
behavior you may want to restrict what is printed according to the
print-level and print-length of an evisc-tuple; see
LD-EVISC-TUPLE.

     Examples:

     ; Set trace evisc tuple to a standard value, using current Lisp *print-level*
     ; and *print-length* variables:
     (set-trace-evisc-tuple t)

     ; Set trace evisc tuple back to its default:
     (set-trace-evisc-tuple nil)

     ; Set trace evisc tuple to restrict print-level to 3 and print-length to 4,
     ; while hiding the logical world and suitably printing stobjs even if trace$
     ; option ``:hide nil'' is used.
     (set-trace-evisc-tuple
      (evisc-tuple 3 4 (trace-evisceration-alist state) nil))

     General Forms:

     (set-trace-evisc-tuple nil) ; default trace evisc-tuple set to standard value
     (set-trace-evisc-tuple t)   ; default trace evisc-tuple set to hide the
                                 ;   logical world and deal with stobjs even when
                                 ;   trace$ option ``:hide nil'' is supplied
     (set-trace-evisc-tuple
                    evisc-tuple) ; default trace evisc-tuple set to evisc-tuple

See TRACE$ for a discussion of ACL2 tracing.  The evisc-tuple
(e.g., see LD-EVISC-TUPLE) used by that trace utility is the
one last installed by set-trace-evisc-tuple -- initially to the default
of nil -- unless overriden by trace option :evisc-tuple.

*Remark*.  If you use value t, then ACL2 will ensure that the logical
world and stobjs are kept up-to-date in the trace evisc-tuple.

TRACE!    trace the indicated functions after creating an active trust tag

     Example:
     (trace! (fact :native t :entry *foo*))

     General Form:
     (trace! spec1 ... specn)

where the fni are suitable arguments to trace$.

Trace! is a version of trace$ that avoids the need for an
already-active trust tag (or "ttag"; see DEFTTAG), as explained
below.  See TRACE$ for when a trust tag can be necessary.

See UNTRACE$ for how to undo the effect of trace!.

The evaluation of a trace! form causes temporary creation of an active
trust tag, :trace!, followed by the corresponding trace$ form.  The
trust tag will disappear when the call to trace! completes.  Even though
trace! will remove its temporary ttag, it will still print a "TTAG
NOTE", which indicates that the session is suspect.  See DEFTTAG
and see TTAGS-SEEN for further remarks on this issue.