This is documentation for ACL2 Version 6.0
Copyright (C) 2012  University of Texas at Austin

This program is free software; you can redistribute it and/or modify
it under the terms of Version 2 of the GNU General Public License as
published by the Free Software Foundation.

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.

DEALING-WITH-TAU-PROBLEMS    some advice on dealing with problems caused by the tau system

For background on the tau system, see
INTRODUCTION-TO-THE-TAU-SYSTEM.  The two most common problems caused
by the tau system have to do with the system's interaction with
"legacy" proof scripts.  Such scripts may suffer because they were not
designed to exploit tau reasoning and which may configure the tau
database in quite incomplete and arbitrary ways.  The two most common
problems we have seen are (a) significant slow downs in a few proofs
and (b) failed proof attempts due to hints being misapplied because the
tau system caused subgoals to be renumbered.

We discuss the rather limited means of dealing with these problems
here.  In future-work-related-to-the-tau-system we list some major
inadequacies of the tau system.

If the tau system contributes to a proof, the rune
(:executable-counterpart tau-system) will be listed among the Rules in
the Summary.  However, merely by being attempted the tau system can
slow down proofs in which it makes no contribution.

The most brutal and fool-proof way to isolate a proof from the tau
system is to disable the entire system.  This can be done globally by

     (in-theory (disable (tau-system)))  ; (:executable-counterpart tau-system)

or locally with a subgoal specific hint:

     ...
     :hints (("...subgoal id..." :in-theory (disable (tau-system))))

Conducting a proof with and without the participation of the tau system
can help you determine whether tau reasoning is helping or hurting.

Dealing with Slowdowns

The time-tracker utility was added to allow users to investigate
whether excessive amounts of time are being spent in a given function.
It was then used to annotate the code for the tau system as described in
time-tracker-tau.  The result is that if "excessive" time is spent in
tau reasoning, messages to that effect will be printed to the proof
log.  The question is: aside from disabling the tau system how can the
proof be sped up?

There are two common causes of slowdown in the tau system.  The first
stems from the system's use of :executable-counterparts to determine
whether a constant has a given tau.  Recall that a tau is a conjunction
of monadic predicates.  To determine whether some constant satisfies
the tau, the predicates are executed.  If you have a hard-to-compute
predicate this can be very slow.  The most typical such predicates in
ACL2 applications are those that check invariants, e.g., that recognize
"good states" or "well-formed data."  These are often written
inefficiently because they are intended only for used in theorems and,
before the tau system was added, they may have never been applied to
constants.  The most common constants tau predicates are applied to are
0, T, and NIL, although different models may stress other constants.
To understand why NIL for example is frequently tested, if the test of
an IF-expression is computed to have tau s then the next question we
ask is "does nil satisfy s?"

You may determine whether the tau system is spending time executing tau
predicates by observing the rewriter -- see DMR -- or by
interrupting the system and getting a backtrace (see
SET-DEBUGGER-ENABLE).

If excessive time is being spent in a tau predicate, a draconian
solution is to disable the :executable-counterpart of that predicate,
for example in either of these equivalent ways.  The tau system does
not execute disabled :executable-counterparts.

     (in-theory (disable (:executable-counterpart foo)))
     (in-theory (disable (foo)))

In either case above, you may prefer to provide local :in-theory :hints
rather than :in-theory events.

Disabling the executable counterpart of expensive tau predicates will
weaken the tau system, probably only negligibly, because it can no
longer run the predicates to determine whether they admits given
constants.

A more sophisticated solution is to make the tau system record values
of the :logic-mode function in question, so that the system will look up
the necessary values rather than running the function every time the
question arises.  It will look up recorded values whether the
executable counterpart of the tau predicate is enabled or disabled.
Here is an example of a lemma that can provide such a solution.  See
the discussion of the Eval form of :tau-system rules.

     (defthm lemma
       (and (foo 0)
            (foo 17)
            (foo t)
            (not (foo '(a b c))))
       :rule-classes :tau-system)

It might be difficult to determine which constants are being repeatedly
tested, although tracing (trace$) suspected tau predicates will show
what they are being called on.

At the moment there are no better user-level tools to discover this.
However, some users may wish to consider the following hack: In the ACL2
source file tau.lisp, immediately after the definition of the system
function ev-fncall-w-tau-recog, there is a comment which contains some
raw Lisp code that can be used to investigate whether tau's use of
evaluation on constants is causing a problem and to determine which
constants are involved.

The second main cause of slowdowns by the tau system is that the system
contains "too many" conjunctive rules (see the Conjunctive form in
tau-system).  Unfortunately, we have no tools for either identifying
the problem or addressing it!  That said, let us tell you what we do
know!

Conjunctive rules are used to "complete" each tau as it is built.
Referring to the weekdayp example in tau-system, if a tau is
constructed that recognizes weekdays but not MON, TUE, THU, or FRI, it
is completed by adding that the tau recognizes (only) WED.  This means
that when we construct a tau we scan all known conjunctive rules and
see whether all but one of the literals of any conjunctive rule are
present.  This can be expensive.  To mitigate this expense, the tau
system caches the computation on a per proof basis (the cache is
cleared after every proof).

To learn what conjunctive rules there are in your system, evaluate

     (assoc 'tau-conjunctive-rules (tau-database (w state)))

Perhaps by sending the implementors that list, we can think of ways to
index the conjunctive rules to save time.

Dealing with Misapplied Hints

The second common problem caused by the tau system in legacy proof
scripts is that it can cause subgoals to be renumbered and thus cause
hints to be missed.  The only ways to address this problem is either to
disable the tau system (locally or globally by disabling
(:executable-counterpart tau-system)) or change the legacy hints to use
the new subgoal names.

FUTURE-WORK-RELATED-TO-THE-TAU-SYSTEM    some tau system problems that we hope someone will address

The tau system is inexpressive compared to modern polymorphic type
systems -- something that may be unavoidable in an untyped first-order
language.  However, we believe its effectiveness could be greatly
increased by the development of some additional tools.  We also believe
that most of these tools could be provided by ACL2 users creating
certified community books that exploit the basic tools already
provided.  It is likely the initial attempts to create such books will
show the inadequacy of some of the current algorithms and data
structures in the tau system and might point the way to improvements.

As implementors of ACL2 our preference is to support the improvement of
the core algorithms and data structures and provide customizable hooks
allowing users to exploit them by developing effective and convenient
interfaces.  However, we want the further elaboration and optimization
of the tau system to be based on user experience not just speculation.

Some tools we think might help are listed below.  We invite volunteers
and further suggestions.

A tau-centric signature notation for use in function definitions,
exploited by a macro replacing defun so that input-output relationships
phrased in tau terms are proved as :tau-system rules immediately after
functions are introduced:

We have, for example, experimented with a book defining a macro that
allows the definition of the function ap (append) accompanied by a
signature rule.  Subsequent defsig events can add other signatures in
the same notation.

     (defsig ap (true-listp * true-listp ==> true-listp) (x y)
        (if (consp x)
            (cons (car x) (ap (cdr x) y))
            y))

     (defsig ap (integer-listp * integer-listp ==> integer-listp))

This experimental book provides succinct syntax for all tau signatures.
For example, that book parses the signature

     (NATP (/= 3 5 7) (< 16) * TRUE-LISTP ==> BOOLEANP * INTEGER-LISTP * NATP)
 to be the signature of a function with two inputs and three outputs.
The first input must be a natural number, different from 3, 5, and 7,
and less than 16.  The second input must be a true list.  The first
output is a boolean, the second a list of integers, and the third a
natural.

To express this signature for function fn as a formula requires
significantly more typing by the user:

     (IMPLIES (AND (NATP X)
                   (NOT (EQUAL X 3))
                   (NOT (EQUAL X 5))
                   (NOT (EQUAL X 7))
                   (< X 16)
                   (TRUE-LISTP Y))
              (AND (BOOLEANP (MV-NTH 0 (FN X Y)))
                   (INTEGER-LISP (MV-NTH 1 (FN X Y)))
                   (NATP (MV-NTH 2 (FN X Y)))))

We suspect that the provision of some succinct tau-centric notation (not
necessarily the one above) for signatures at definition-time will mean
users get more benefit from the tau system.

Some tau inference mechanisms: This phrase suggests two different
improvements.  One is to implement a mechanism that adds or completes
signatures for function definitions by exploiting knowledge of commonly
used recursive schemas and the signatures of the subroutines in the
body.  For example, the definition of ap above rather obviously has the
signature

     (integer-listp * integer-listp ==> integer-listp)

and many others just based on the two recursive schemas that (a) collect
certain elements from lists and (b) check that all elements have a
certain property.

The other "tau inference" improvement is to implement a mechanism for
inferring relations between user-defined Booleans, perhaps by exploiting
example generation, testing, and knowledge of recursive schemas.  For
example, it is fairly obvious that symbol-alistp implies alistp.
Making the user state these relations invites omissions that render the
tau system very unpredictable.

A tau assistant: It would be useful to have a way to find out what tau
rules are missing.  Given a term that the user believes should
"obviously" have some tau ("type") what rules might be added to make
the tau algorithm compute that expected tau?  For example, if (g x) is
known to satisfy P and (f x) is known to satisfy R when its argument
satisfies S:

     g : T ==> P
     f : S ==> R

then if the user asserts that (f (g x)) "ought" to have tau R, one
plausible suggestion is the simple tau rule that (P x) implies (S x).
Such assistance -- while still confronting an undecidable problem --
might be easier to implement within the tau framework than more
generally in ACL2.  (Many users have wanted such an assistant to
suggest lemmas for the rewriter.)

IO    input/output facilities in ACL2

     Example:
     (mv-let
       (channel state)
       (open-input-channel "foo.lisp" :object state)
       (mv-let (eofp obj state)
               (read-object channel state)
               (.
                 .
                  (let ((state (close-input-channel channel state)))
                        (mv final-ans state))..)))

Also see FILE-READING-EXAMPLE.

For advanced ways to control printing, see PRINT-CONTROL.

For a discussion of formatted printing, see FMT.

To control ACL2 abbreviation ("evisceration") of objects before printing
them, see SET-EVISC-TUPLE, see WITHOUT-EVISC, and see
SET-IPRINT.

To redirect output to a file, see OUTPUT-TO-FILE.

Related topics other than immediate subtopics:

ACL2 supports input and output facilities equivalent to a subset of
those found in Common Lisp.  ACL2 does not support random access to
files or bidirectional streams.  In Common Lisp, input and output are
to or from objects of type stream.  In ACL2, input and output are to or
from objects called "channels," which are actually symbols.  Although a
channel is a symbol, one may think of it intuitively as corresponding
to a Common Lisp stream.  Channels are in one of two ACL2 packages,
"ACL2-INPUT-CHANNEL" and "ACL2-OUTPUT-CHANNEL".  When one "opens" a
file one gets back a channel whose symbol-name is the file name passed
to "open," postfixed with -n, where n is a counter that is incremented
every time an open or close occurs.

There are three channels which are open from the beginning and which
cannot be closed:

       acl2-input-channel::standard-character-input-0
       acl2-input-channel::standard-object-input-0
       acl2-input-channel::standard-character-output-0

All three of these are really Common Lisp's *standard-input* or
*standard-output*, appropriately.

For convenience, three global variables are bound to these rather
tedious channel names:

       *standard-ci*
       *standard-oi*
       *standard-co*

Common Lisp permits one to open a stream for several different kinds of
io, e.g. character or byte.  ACL2 permits an additional type called
"object".  In ACL2 an "io-type" is a keyword, either :character, :byte,
or :object.  When one opens a file, one specifies a type, which
determines the kind of io operations that can be done on the channel
returned.  The types :character and :byte are familiar.  Type :object
is an abstraction not found in Common Lisp.  An :object file is a file
of Lisp objects.  One uses read-object to read from :object files and
print-object$ (or print-object$-ser) to print to :object files.  (The
reading and printing are really done with the Common Lisp read and
print functions.  For those familiar with read, we note that the
recursive-p argument is nil.)  The function read-object-suppress is
logically the same as read-object except that read-object-suppress
throws away the second returned value, i.e. the value that would
normally be read, simply returning (mv eof state); under the hood,
read-object-suppress avoids errors, for example those caused by
encountering symbols in packages unknown to ACL2.

File-names are strings.  ACL2 does not support the Common Lisp type
pathname.  However, for the file-name argument of the output-related
functions listed below, ACL2 supports a special value, :STRING.  For
this value, the channel connects (by way of a Common Lisp output string
stream) to a string rather than to a file: as characters are written to
the channel they can be retrieved by using get-output-stream-string$.

Here are the names, formals and output descriptions of the ACL2 io
functions.

     Input Functions:
       (open-input-channel (file-name io-type state) (mv channel state))
       (open-input-channel-p (channel io-type state) boolean)
       (close-input-channel (channel state) state)
       (read-char$ (channel state) (mv char/nil state)) ; nil for EOF
       (peek-char$ (channel state) boolean)
       (read-byte$ (channel state) (mv byte/nil state)) ; nil for EOF
       (read-object (channel state) (mv eof-read-flg obj-read state))
       (read-object-suppress (channel state) (mv eof-read-flg state))

     Output Functions:
       (open-output-channel  (file-name io-type state) (mv channel state))
       (open-output-channel! (file-name io-type state) (mv channel state))
       (open-output-channel-p (channel io-type state) boolean)
       (close-output-channel (channel state) state)
       (princ$ (obj channel state) state)
       (write-byte$ (byte channel state) state)
       (print-object$ (obj channel state) state)
       (print-object$-ser (obj serialize-character channel state) state)
       (fms  (string alist channel state evisc-tuple) state)
       (fms! (string alist channel state evisc-tuple) state)
       (fmt  (string alist channel state evisc-tuple) (mv col state))
       (fmt! (string alist channel state evisc-tuple) (mv col state))
       (fmt1 (string alist col channel state evisc-tuple) (mv col state))
       (fmt1! (string alist col channel state evisc-tuple) (mv col state))
       (cw (string arg0 arg1 ... argn) nil)
       (get-output-stream-string$ (channel state
                                   &optional (close-p 't)
                                             (ctx ''get-output-stream-string$))
                                  (mv erp string state))

The "formatting" functions are particularly useful; see FMT and
see CW.  In particular, cw prints to a "comment window" and
does not involve the ACL2 state, so many may find it easier to use than
fmt and its variants.  The functions fms!, fmt!, and fmt1! are the same
as their respective functions without the "!," except that the "!"
functions are guaranteed to print forms that can be read back in (at a
slight readability cost).

When one enters ACL2 with (lp), input and output are taken from
*standard-oi* to *standard-co*.  Because these are synonyms for
*standard-input* and *standard-output*, one can drive ACL2 io off of
arbitrary Common Lisp streams, bound to *standard-input* and
*standard-output* before entry to ACL2.

The macro get-output-stream-string$ returns the string accumulated into
the given channel.  By default, a call of this macro closes the supplied
output channel.  However, a third argument is optional (default t), and
if it evaluates to nil then the channel remains open.  The fourth
argument is an optional context, which generally evaluates to a symbol,
for error reporting.  The following example illustrates.

     ACL2 !>
     (mv-let
        (channel state)
        (open-output-channel :string :object state)
        (pprogn (print-object$-ser 17 nil channel state)
                (print-object$-ser '(a b (c d)) nil channel state)
                (er-let*
                  ((str1 (get-output-stream-string$
                          channel state
                          nil))) ; keep the channel open
                  (pprogn (print-object$-ser 23 nil channel state)
                          (print-object$-ser '((e f)) nil channel state)
                          (er-let* ; close the channel
                            ((str2 (get-output-stream-string$ channel state)))
                            (value (cons str1 str2)))))))
      ("
     17
     (A B (C D))" . "
     23
     ((E F))")
     ACL2 !>

Also see PRINTING-TO-STRINGS for a discussion of formatted
printing functions such as fmt-to-string that do not take a channel or
state argument and return a string.

By default, symbols are printed in upper case when vertical bars are not
required, as specified by Common Lisp.  See SET-PRINT-CASE for
how to get ACL2 to print symbols in lower case.

By default, numbers are printed in radix 10 (base 10).  See
SET-PRINT-BASE for how to get ACL2 to print numbers in radix 2, 8, or
16.

Comment for advanced users: Function open-output-channel! is identical
as a function to open-output-channel, except that the former may be
called even during make-event expansion and clause-processor hints, but
requires that there is an active trust tag (see DEFTTAG).

Finally, we note that the community book books/misc/file-io.lisp
contains useful file io functions whose definitions illustrate some of
the features described above.

*STANDARD-CI*    an ACL2 character-based analogue of CLTL's *standard-input*

The value of the ACL2 constant *standard-ci* is an open character input
channel that is synonymous to Common Lisp's *standard-input*.

ACL2 character input from *standard-ci* is actually obtained by reading
characters from the stream named by Common Lisp's *standard-input*.
That is, by changing the setting of *standard-input* in raw Common Lisp
you can change the source from which ACL2 reads on the channel
*standard-ci*.  See *STANDARD-CO*.

*STANDARD-CO*    the ACL2 analogue of CLTL's *standard-output*

The value of the ACL2 constant *standard-co* is an open character
output channel that is synonymous to Common Lisp's *standard-output*.

ACL2 character output to *standard-co* will go to the stream named by
Common Lisp's *standard-output*.  That is, by changing the setting of
*standard-output* in raw Common Lisp you can change the actual
destination of ACL2 output on the channel named by *standard-co*.
Observe that this happens without changing the logical value of
*standard-co* (which is some channel symbol).  Changing the setting of
*standard-output* in raw Common Lisp essentially just changes the map
that relates ACL2 to the physical world of terminals, files, etc.

To see the value of this observation, consider the following.  Suppose
you write an ACL2 function which does character output to the constant
channel *standard-co*.  During testing you see that the output actually
goes to your terminal.  Can you use the function to output to a file?
Yes, if you are willing to do a little work in raw Common Lisp: open a
stream to the file in question, set *standard-output* to that stream,
call your ACL2 function, and then close the stream and restore
*standard-output* to its nominal value.  Similar observations can be
made about the two ACL2 input channels, *standard-oi* and
*standard-ci*, which are analogues of *standard-input*.

Another reason you might have for wanting to change the actual streams
associated with *standard-oi* and *standard-co* is to drive the ACL2
top-level loop, ld, on alternative input and output streams.  This end
can be accomplished easily within ACL2 by either calling ld on the
desired channels or file names or by resetting the ACL2 state global
variables 'standard-oi and 'standard-co which are used by ld.  See
STANDARD-OI and see STANDARD-CO.

*STANDARD-OI*    an ACL2 object-based analogue of CLTL's *standard-input*

The value of the ACL2 constant *standard-oi* is an open object input
channel that is synonymous to Common Lisp's *standard-input*.

ACL2 object input from *standard-oi* is actually obtained by reading
from the stream named by Common Lisp's *standard-input*.  That is, by
changing the setting of *standard-input* in raw Common Lisp you can
change the source from which ACL2 reads on the channel *standard-oi*.
See *STANDARD-CO*.

CHARACTER-ENCODING    how bytes are parsed into characters

When the Common Lisp reader comes across bytes in a file or at the
terminal, they are parsed into characters.  The simplest case is when
each byte that is read is a standard character (see
STANDARD-CHAR-P).  It is actually quite common that each byte that is
read corresponds to a single character.  The parsing of bytes into
characters is based on a _character encoding_, that is, a mapping that
associates one or more bytes with each legal character.

In order to help guarantee the portability of files (including books),
ACL2 installs a common character encoding for reading files, often
known as iso-8859-1 or latin-1.  For some host Lisps this character
encoding is also used for reading from the terminal; but, sadly, this
may not hold for all host Lisps, and may not even be possible for some
of them.

The use of the above encoding could in principle cause problems if one's
editor produces files using an encoding other than iso-8859-1, at least
if one uses non-standard characters.  In particular, the default Emacs
buffer encoding may be utf-8.  If your file has non-standard
characters, then in Emacs you can evaluate the form

     (setq save-buffer-coding-system 'iso-8859-1)

before saving the buffer into a file.  This will happen automatically
for users who load distributed file emacs/emacs-acl2.el into their Emacs
sessions.

For an example of character encodings in action, see the community book
books/misc/character-encoding-test.lisp.

EVISC-TUPLE    control suppression of details when printing

ACL2 output is generally printed in full.  However, ACL2 can be
directed to abbreviate, or "eviscerate", objects before printing them.
To "eviscerate" an object we replace certain substructures within it by
strings that are printed in their stead.  Such replacement is made
relative to a so-called "evisc-tuple", which has four components:
(evisc-tuple print-level print-length alist hiding-cars) is the same as
the value of (list alist print-level print-length hiding-cars), and the
components are used as follows (with priority order as discussed
below).  The alist component is used to replace any substructure
occurring as a key by the corresponding string.  The print-level and
print-length are analogous to Common Lisp variables *print-level* and
*print-length*, respectively, and cause replacement of substructures
deeper than print-level by `#' and those longer than print-length by
`...'.  Finally, any consp x that starts with one of the symbols in
hiding-cars is printed as <hidden>.

The following example illustrates the use of an evisc-tuple that limits
the print-level to 3 -- only three descents into list structures are
permitted before replacing a subexpression by `#' -- and limits the
print-length to 4 -- only the first four elements of any list structure
will be printed before replacing its tail by `...'.

     ACL2 !>(fms "~x0~%"
                 (list (cons #\0 '((a b ((c d)) e f g) u v w x y)))
                 *standard-co*
                 state
                 (evisc-tuple 3 4 nil nil))

     ((A B (#) E ...) U V W ...)
     <state>
     ACL2 !>

Notice that it is impossible to read the printed value back into ACL2,
since there is no way for the ACL2 reader to interpret `#' or `...'.  To
solve this problem, see SET-IPRINT.

In the above example we pass an evisc-tuple explicitly to a printing
function, in this case, fms (see FMT).  But ACL2 also does its
own printing, for example during a proof attempt.  There are global
evisc-tuples that control ACL2's printing; see SET-EVISC-TUPLE
and see WITHOUT-EVISC.

EVISCERATE-HIDE-TERMS    to print (hide ...) as <hidden>

     Example:
     (assign eviscerate-hide-terms t)
     (assign eviscerate-hide-terms nil)

Eviscerate-hide-terms is a state global variable whose value is either
t or nil.  The variable affects how terms are displayed by default (but
not if you have set the term-evisc-tuple to other than its default; see
SET-EVISC-TUPLE).  If t, terms of the form (hide ...)  are
printed as <hidden>.  Otherwise, they are printed normally.

EXTERNAL-FORMAT    See CHARACTER-ENCODING.

IPRINT    See SET-IPRINT.

IPRINTING    See SET-IPRINT.

OPEN-OUTPUT-CHANNEL!    when trust tags are needed to open output channels

Use this function in place of open-output-channel if you want to open a
channel for output at times this would otherwise be prohibited, for
example during make-event expansion and clause-processor hints.  If
this functionality doesn't quite seem like what you need, take a look
at the definition of open-output-channel! in axioms.lisp, specifically
the binding of state global variable writes-okp.  The following
example, taken from community book books/hons-archive/hons-archive.lisp,
illustrates the latter approach.

     (defmacro har-zip! (x filename &key sortp)
       "See :doc hons-archive"
       `(mv-let (erp val state)
                (progn!
                 :state-global-bindings
                 ((temp-touchable-vars t set-temp-touchable-vars))
                 (state-global-let*
                  ((writes-okp t))
                  (let ((state (har-zip-fn ,x ,filename ,sortp state)))
                    (mv nil nil state))))
                (declare (ignore erp val))
                state))

The book below illustrates the soundness loophole plugged in ACL2
Version_3.2 related to file writes during book certification.

     ; The following example is adapted (with only very slight changes)
     ; from one written by Peter Dillinger.  It illustrates the prohibition
     ; against writing files enforced by with-output-channel during book
     ; certification (more specifically, during make-event expansion).

     ; This book certifies in ACL2 Version_3.1 before the fix discussed in the
     ; paragraph about it being ``possible to write files during book
     ; certification'' in :DOC NOTE-3-2.  The fix was actually made to ACL2
     ; function open-output-channel.

     ; After the fix, in order for certification to succeed one needs to do
     ; two things.  First, in raw lisp:
     ;   (push :after-writes-okp-fix *features*)
     ; Second, certify with this command:
     ;   (certify-book "writes-okp" 0 nil :ttags (:writes-okp))

     (in-package "ACL2")

     (local
      (defun write-objects-to-channel (obj-lst chan state)
        (declare (xargs :mode :program
                        :stobjs state
                        :guard (true-listp obj-lst)))
        (if (consp obj-lst)
            (pprogn (print-object$ (car obj-lst) chan state)
                    (write-objects-to-channel (cdr obj-lst) chan state)
                    state)
          state)))

     #+after-writes-okp-fix
     (defttag :writes-okp)

     (local
      (defun write-objects-to-file (obj-lst filename state)
        (declare (xargs :mode :program
                        :stobjs state
                        :guard (and (stringp filename)
                                    (true-listp obj-lst))))
        (mv-let (chan state)
                #-after-writes-okp-fix
                (open-output-channel filename :object state)
                #+after-writes-okp-fix
                (open-output-channel! filename :object state)
                (if chan
                    (pprogn (write-objects-to-channel obj-lst chan state)
                            (close-output-channel chan state)
                            (value :done))
                  (er soft 'write-object-to-file
                      "Could not open for writing: ~x0"
                      filename)))))

     (local
      (defconst *nil.lisp*
        '((in-package "ACL2")
          (defthm bad nil :rule-classes nil))))

     (local
      (defconst *nil.cert*
        '((IN-PACKAGE "ACL2")
          "ACL2 Version 3.1"
          :BEGIN-PORTCULLIS-CMDS
          :END-PORTCULLIS-CMDS
          NIL
          (("/home/peterd/test/nil.lisp" "nil" "nil"
            ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 134094174))
          62589544
          )))

     (local
      (make-event (er-progn
                   (write-objects-to-file *nil.lisp* "nil.lisp" state)
                   (write-objects-to-file *nil.cert* "nil.cert" state)
                   (value '(value-triple :invisible)))))

     (local (include-book
             "nil" :load-compiled-file nil))

     (defthm bad nil :rule-classes nil)

OUTPUT-TO-FILE    redirecting output to a file

For a general discussion of ACL2 input/output and of the ACL2
read-eval-print loop, see IO and see LD (respectively).
Here we use an example to illustrate how to use some of the options
provided by ld to redirect ACL2 output to a file, other than the
printing of the prompt (which continues to go to the terminal).

There are two ld specials that control output from the ld command:
proofs-co for proof output and standard-co for other output.  The
following example shows how to use these to redirect output to a file
"tmp.out".  The following command opens a character output channel to
to the file "tmp.out" and redirects proof output to that channel, i.e.,
to file "tmp.out".

     (mv-let (chan state)
             (open-output-channel "tmp.out" :character state)
             (set-proofs-co chan state))

Next, we redirect standard output to that same channel.

     (set-standard-co (proofs-co state) state)

Now we can load an input file, in this case file "tmp.lisp", and output
will be redirected to file "tmp.out".  (The use of :ld-pre-eval-print t
is optional; see LD.)

     (ld "tmp.lisp" :ld-pre-eval-print t)

Having completed our load operation, we restore both proof output and
standard output to the terminal, as follows.

     (set-standard-co *standard-co* state)
     (close-output-channel (proofs-co state) state)
     (set-proofs-co *standard-co* state)

The following variant of the above example shows how to redirect output
as above except without changing the global settings of the two ld
specials, proofs-co and standard-co.  This approach uses a notion of
"global variables" stored in the ACL2 state; see ASSIGN and see
@.

     (mv-let (chan state)
             (open-output-channel "tmp.out" :character state)
             (assign tmp-channel chan))
     (ld "tmp.lisp" :ld-pre-eval-print t
                    :proofs-co (@ tmp-channel)
                    :standard-co (@ tmp-channel))
     (close-output-channel (@ tmp-channel) state)

PRINT-CONTROL    advanced controls of ACL2 printing

See IO for a summary of printing in ACL2.  Here we document
some advanced ways to control what is printed by ACL2's primary
printing routines.

See SET-PRINT-BASE, see SET-PRINT-RADIX, and see
SET-PRINT-CASE for discussions of the most common ways to control
what is printed.  Indeed, these are the only ways to control the
behavior of princ$ and prin1$.

The rest of this topic is for advanced users of ACL2.  We refer to
Common Lisp behavior, as described in any good Common Lisp
documentation.

*Print-control variables*.  Set-print-base, set-print-radix, and
set-print-case assign to corresponding so-called "state global
variables" 'print-base, 'print-radix, and 'print-case, which can be
accessed using the expressions (@ print-base), (@ print-radix), and (@
print-case), respectively; see ASSIGN.  Here is a table showing
all print-control variables, their setters, and their defaults.

     print-base          set-print-base          10
     print-case          set-print-case          :upcase
     print-circle        set-print-circle        nil
       [but see remark on print-circle-files, below]
     print-escape        set-print-escape        t
     print-length        set-print-length        nil
     print-level         set-print-level         nil
     print-lines         set-print-lines         nil
     print-pretty        set-print-pretty        nil
     print-radix         set-print-radix         nil
     print-readably      set-print-readably      nil
     print-right-margin  set-print-right-margin  nil

Each ACL2 print-control variable print-xxx can correspond in function to
Common Lisp variable *PRINT-XXX*.  Specifically, the evaluation of forms
(set-print-base t), (set-print-radix t), and (set-print-case t) affects
ACL2 printing functions in much the same way that setting to t Common
Lisp variables *PRINT-BASE*, *PRINT-RADIX*, and *PRINT-CASE*,
respectively, affects Common Lisp printing.  The same is true for
print-escape, except that this does not affect princ$ or prin1$, which
correspond to Common Lisp functions princ and prin1: princ treats
*PRINT-ESCAPE* as nil while prin1 treats *PRINT-ESCAPE* as t.
Moreover, all print-control variables not mentioned in this paragraph
are set to their defaults in princ$ and prin1$, as indicated by ACL2
constant *print-control-defaults*, except that print-readably is set to
nil in princ$.

Fmt and its related functions are sensitive to state globals
'print-base, 'print-radix, 'print-case, 'print-escape, and
'print-readably, in analogy with Common Lisp functions that don't fix
*PRINT-ESCAPE* or *PRINT-READABLY*.  But the fmt functions do not
respect settings of other print-control variables; for example, they act
as though 'print-circle is nil.  Since ACL2 output is produced using
the same underlying print routines as the fmt functions, it also is
insensitive to all print-control variables except for the five above.
To control the print-level and print-length used for producing ACL2
output, see SET-EVISC-TUPLE.

Print-object$ is sensitive to all of the print-control variables.

Remark on print-circle-files: ACL2 typically binds 'print-circle to t
before writing certificate files, or auxiliary files that are compiled
when make-event forms are present in a book, or files in support of
:comp commands.  This binding allows for structure sharing that can
keep these files from growing large.  However, this behavior is
defeated in GCL (Gnu Common Lisp), because of the small number of
indices n available by default (1024) for the #n= reader macro.  For the
files described above, what actually happens is that 'print-circle is
bound to the value of 'print-circle-files, which by default is t unless
the underlying Lisp is GCL, in which case it is set to nil.  See
ASSIGN for how to set state globals such as 'print-circle-files.  For
example, if you build GCL with a larger number of #n= indices
available, you may wish to restore the print-circle behavior for
certificate files by following these instructions from Camm Maguire:

     This can trivially be revised to any larger constant by editing the
     following line of read.d and recompiling:

     #ifndef SHARP_EQ_CONTEXT_SIZE
     #define SHARP_EQ_CONTEXT_SIZE 500
     #endif

End of Remark.

Evaluate (reset-print-control) to restore all print-control variables to
their original settings, as stored in constant *print-control-defaults*.

(Remark for those using ACL2 built on Gnu Common Lisp (GCL) versions
that are non-ANSI, which as of October 2008 is all GCL versions
recommended for ACL2: Note that Common Lisp variables *PRINT-LINES*,
*PRINT-MISER-WIDTH*, *PRINT-READABLY*, *PRINT-PPRINT-DISPATCH*, and
*PRINT-RIGHT-MARGIN* do not have any effect for such GCL versions.)

PRINTING-TO-STRINGS    printing to strings instead of files or standard output

Each of ACL2's formatted printing functions, FM*, has an analoguous
macro FM*-TO-STRING indicated below.  These functions do not include a
channel or state as an argument, and FM*-TO-STRING returns the string
that FM* would print to the state, in place of state; see FMT.
The legal keyword arguments are described below.

     General Forms:                                 result
     (fms-to-string string alist &key ...)          ; string
     (fmt-to-string string alist &key ...)          ; (mv col string)
     (fmt1-to-string string alist column &key ...)  ; (mv col string)
     (fms!-to-string string alist &key ...)         ; string
     (fmt!-to-string string alist &key ...)         ; (mv col string)
     (fmt1!-to-string string alist column &key ...) ; (mv col string)

The legal keyword arguments are as follows.  They are all optional with
a default of nil.

     Evisc-tuple is evaluated, and corresponds exactly to the
     evisc-tuple argument of the corresponding FM* function; see
     FMT.

     Fmt-control-alist should typically evaluate to an alist that maps
     print-control variables to values; see PRINT-CONTROL.  Any
     alist mapping variables to values is legal, however.  By default
     the print controls are set according to the value of constant
     *fmt-control-defaults*; fmt-control-alist overrides these
     defaults.  For example, *fmt-control-defaults* sets the right
     margin just as it is set in the initial ACL2 state, by binding
     fmt-soft-right-margin and fmt-hard-right-margin to their
     respective defaults of *fmt-soft-right-margin-default* and
     *fmt-hard-right-margin-default*.  The following example shows how
     you can override those defaults, in this case arranging to print
     flat by setting the right margin to a large number.

          (fmt-to-string "~x0"
                         (list (cons #\0 (make-list 30)))
                         :fmt-control-alist
                         `((fmt-soft-right-margin . 10000)
                           (fmt-hard-right-margin . 10000)))

     Iprint is typically nil, but t is also a legal value.  See
     SET-IPRINT for the effect of value t, which however is local to
     this call of a FM*-TO-STRING function; the behavior if iprinting
     afterwards is not affected by this call.  In particular, you will
     not be able to look at the values of iprint tokens printed by this
     call, so the value t is probably of limited utility at best.

Also see IO for a discussion of the utility
get-output-stream-string$, which allows for accumulating the results of
more than one printing call into a single string but requires the use
of state.

RESET-PRINT-CONTROL    See PRINT-CONTROL.

SET-EVISC-TUPLE    control suppression of details when printing

ACL2 output is generally printed in full.  However, ACL2 can be
directed to abbreviate, or "eviscerate", objects before printing them,
though the use of a so-called "evisc-tuple".  See EVISC-TUPLE
for a discussion of evisc-tuples.  The utility set-evisc-tuple modifies
certain global evisc-tuples, as explained below, to affect the extent
to which ACL2 eviscerates objects during printing, for example during
proof output or when printing top-level evaluation results.

     General Form:
     (set-evisc-tuple evisc-tuple ; a legal evisc-tuple, or :DEFAULT
                     :iprint val  ; one of *iprint-actions*
                     :sites sites ; either :ALL, or an element or a subset of the
                                  ;   list (:TERM :LD :TRACE :ABBREV)

where the value of :iprint is passed to set-iprint, :sites :all
abbreviates :sites '(:TERM :LD :TRACE :ABBREV), and other documentation
is provided below.  Note that all arguments are evaluated.

See WITHOUT-EVISC for how to avoid evisceration for ACL2 output.

The following example illustrates an invocation of set-evisc-tuple that
limits the print-level to 3 -- only three descents into list structures
are permitted before eviscerating a subterm -- and limits the
print-length to 4 -- only the first four elements of any list structure
will be printed.

     ACL2 !>(set-evisc-tuple (evisc-tuple 3   ; print-level
                                          4   ; print-length
                                          nil ; alist
                                          nil ; hiding-cars
                                          )
                             :iprint :same ; better yet, T
                             :sites :all)
      (:TERM :LD :TRACE :ABBREV)
     ACL2 !>'((a b ((c d)) e f g) u v w x y)
     ((A B (#) E ...) U V W ...)
     ACL2 !>

We recommend however using :iprint t so that eviscerated terms may be
read back in; see SET-IPRINT.  Indeed, the :iprint argument is
required as a reminder to the user to consider that issue, unless
iprinting has been enabled at least once.  If :sites or a required
:iprint argument is omitted, however, ACL2 will query the user for the
missing arguments rather than causing an error.

ACL2 eviscerates by default only in a few cases, primarily in
informational messages for errors, warnings, and queries (i.e., in the
:EVISC case below).  Users can modify the default behavior by supplying
a suitable argument to set-evisc-tuple.  The argument may be :default,
which denotes the evisceration provided when ACL2 starts up.  Otherwise
that argument is an evisc-tuple, which is either nil (no evisceration)
or as described above.  Moreover, there are four evisc-tuple
"evisceration contexts", each with its own evisceration control.  The
value returned by set-evisc-tuple indicates the evisceration contexts
whose evisc-tuple has been set.  The evisceration contexts are as
follows, all of which use a default value of nil for the hiding-cars.
Accessors are also shown for retrieving the corresponding evisc-tuple.

     o :TERM -- used for printing terms.  The accessor is
     (term-evisc-tuple flg state), where flg is ignored if
     set-evisc-tuple has been called for :term with value other than
     :default, and otherwise (hence initially): a flg of nil indicates
     an evisc-tuple of nil, and otherwise the term-evisc-tuple has a
     print-level of 3 and print-length of 4.

     o :ABBREV -- used for printing informational messages for errors,
     warnings, and queries.  Initially, the alist abbreviates the ACL2
     world, print-level is 5, and print-level is 7.  The accessor is
     (abbrev-evisc-tuple state).

     o :GAG-MODE -- used for printing induction schemes (and perhaps,
     in the future, for other printing) when gag-mode is on.  If
     gag-mode is off, the value used for this evisc-tuple is
     (term-evisc-tuple nil state).  But if gag-mode is on (i.e.,
     (gag-mode) evaluates to a non-nil value), then with one exception,
     the value is an evisc-tuple or nil, to be used in gag-mode for
     printing of induction schemes and, during proofs, the "The
     non-trivial part of the guard conjecture".  The exceptional value
     is t, which indicates that in gag-mode, no printing of induction
     schemes should be and the guard conjecture should be printed using
     (term-evisc-tuple t state).  The accessor is (gag-mode-evisc-tuple
     state).

     o :LD -- used by the ACL2 read-eval-print loop.  The accessor is
     (ld-evisc-tuple state).

     o :TRACE -- used for printing trace output.  No accessor is
     available (though in raw Lisp, (trace-evisc-tuple) returns the
     trace-evisc-tuple).

Each context ectx also has an updater, (set-ectx-evisc-tuple val
state), where val is a legal value for set-evisc-tuple as described
above: :default or an evisc-tuple (possibly nil).

Note that the break-rewrite commands and the proof-checker generally do
their printing using the term-evisc-tuple.

SET-FMT-HARD-RIGHT-MARGIN    set the right margin for formatted output

In this documentation topic we discuss setting of both a "soft" and a
"hard" right margin.

     Example Forms:
     (set-fmt-soft-right-margin 55 state) ; set soft right margin to 55
     (set-fmt-hard-right-margin 68 state) ; set hard right margin to 68

Fmt and related functions insert linebreaks when lines get too long.  A
linebreak is inserted at an aesthetically appropriate point once the
column exceeds the value of (@ fmt-soft-right-margin).  If however the
column exceeds the value of (@ fmt-hard-right-margin), then a linebreak
is soon inserted.  Such a "hard" linebreak follows the insertion of a
backslash (\) character unless fmt!, fms!, or fmt1! is used, or state
global write-for-read is true.

SET-FMT-SOFT-RIGHT-MARGIN    set the soft right margin for formatted output

See SET-FMT-HARD-RIGHT-MARGIN for a discussion of the soft and
hard right margin for formatted output.

SET-IPRINT    control whether abbreviated output can be read back in

When ACL2 pretty-prints large expressions using formatted printing (see
FMT), it may save time and space by printing tokens `#' or
`...' in place of certain subexpressions.  By default this only happens
for a few settings such as error and warning messages; see
SET-EVISC-TUPLE for controlling such elision in general.  The full
expression is unavailable to the user when `#' or `...' is printed, but
that is easily solved by evaluating the form

       (set-iprint t)

to enable a mode called "iprinting".  Then, instead of printing `#' or
`...', ACL2 prints `#@i#' for i = 1,2,3,... -- all in base 10.  ACL2
can read back in such `#@i#' because under the hood, i is associated
with its corresponding elided form.  Thus the term "iprint" can be
viewed as suggesting "interactive print" or "index print".  We also
think of "iprint" as suggesting "i printing", to suggest the printing
of token `#@i#'.  We call i the "iprint index" of that token.

The following example should suffice to illustrate how to recover elided
subexpressions.  (Below this example we provide details that may be of
interest only to advanced users.)  Here we cause an error by defining a
macro of one argument and then calling it with two arguments.  By
default, error messages abbreviate subexpressions deeper than level 5
with `#' and past the 7th element of a list with `...'.  We see this
behavior below.

     ACL2 !>(defmacro foo (x) x)

     Summary
     Form:  ( DEFMACRO FOO ...)
     Rules: NIL
     Warnings:  None
     Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
      FOO
     ACL2 !>(foo arg1 (a (b (c (d (e (f (g)))))) h i j k l m n))

     ACL2 Error in macro expansion:  Wrong number of args in macro expansion
     of (FOO ARG1 (A (B (C (D #))) H I J K L ...)).  (See :DOC set-iprint
     to be able to see elided values in this message.)

     ACL2 !>(set-iprint t)

     ACL2 Observation in SET-IPRINT:  Iprinting has been enabled.
     ACL2 !>(foo arg1 (a (b (c (d (e (f (g)))))) h i j k l m n))

     ACL2 Error in macro expansion:  Wrong number of args in macro expansion
     of (FOO ARG1 (A (B (C (D #@1#))) H I J K L . #@2#)).

     ACL2 !>(acl2-count '(FOO ARG1 (A (B (C (D #@1#))) H I J K L . #@2#)))
     23
     ACL2 !>

Sometimes you may want to supply the abbreviated form not to compute
with it, as in the acl2-count example just above, but so that you can
see it.  The macro without-evisc eliminates elision during printing.
Below we show two ways to use this utility: first, we use it to print
the elided form, and then, we use it instead on the original input form
to print the entire error message.

     ACL2 !>(without-evisc '(FOO ARG1 (A (B (C (D #@1#))) H I J K L . #@2#)))
     (FOO ARG1
          (A (B (C (D (E (F (G))))))
             H I J K L M N))
     ACL2 !>(without-evisc (foo arg1 (a (b (c (d (e (f (g)))))) h i j k l m n)))

     ACL2 Error in macro expansion:  Wrong number of args in macro expansion
     of (FOO ARG1 (A (B (C (D (E (F (G)))))) H I J K L M N)).

     ACL2 !>

The documentation above probably suffices for most users.  For those
who want more details, below we detail all the ways to use the
set-iprint utility.

     Example Forms:
     (set-iprint t)   ; enable iprinting (elision with #@i@)
     (set-iprint nil) ; disable iprinting

     General Form:
     (set-iprint action        ; t, nil, :reset, :reset-enable, or :same
                 :soft-bound s ; initially  1000
                 :hard-bound h ; initially 10000)

where all arguments are optional, but ACL2 queries for action if it is
omitted.   We defer the explanations of :soft-bound and :hard-bound.
The values for action are as follows:

     T -- Enable iprinting.

     NIL -- Disable iprinting.

     :RESET -- Reset iprinting to its initial disabled state, so that
     when enabled, the first index i for which `#@i# is printed will be
     1.  Note that all stored information for existing iprint indices
     will be erased.

     :RESET-ENABLE -- Reset iprinting as with :reset, and then enable
     iprinting.

     :SAME -- Make no change to the iprinting state (other than setting
     the :soft-bound and/or :hard-bound if specified, as explained
     below).

Immediately after a top-level form is read, hence before it is
evaluated, a check is made for whether the latest iprint index exceeds
a certain bound, (iprint-soft-bound state) -- 1000, by default.  If so,
then the (iprint-last-index state) is set back to 0.  This soft bound
can be changed to any positive integer k by calling set-iprint with
:soft-bound k, typically (set-iprint :same :soft-bound k)].

The above "soft bound" is applied once for each top-level form, but you
may want finer control by applying a bound after the pretty-printing of
each individual form (since many forms may be pretty-printed between
successive evaluations of top-level forms).  That bound is
(iprint-hard-bound state), and can be set with the :hard-bound argument
in analogy to how :soft-bound is set, as described above.

A "rollover" is the detection that the soft or hard bound has been
exceeded, along with a state update so that the next iprint index will
be 1.  When a rollover occurs, any index beyond the latest iprint index
is no longer available for reading.  At the top level of the ACL2
read-eval-print loop, this works as follows: ACL2 reads the next
top-level form according to the current iprint state, then handles a
rollover if the latest iprint index exceeded the current soft bound.
The following log illustrates a rollover, which follows the description
above.

     ACL2 !>(set-iprint t :soft-bound 3)

     ACL2 Observation in SET-IPRINT:  The soft-bound for iprinting has been
     set to 3.

     ACL2 Observation in SET-IPRINT:  Iprinting has been enabled.
     ACL2 !>(set-evisc-tuple (evisc-tuple 2 3 nil nil) :sites :ld)
      (:LD)
     ACL2 !>'((a b c d e f g) (a b c d e f g) (a b c d e f g))
     ((A B C . #@1#) (A B C . #@2#) (A B C . #@3#))
     ACL2 !>'((a b c d e f g) (a b c d e f g) (a b c d e f g))
     ((A B C . #@4#) (A B C . #@5#) (A B C . #@6#))
     ACL2 !>(without-evisc '((A B C . #@4#) (A B C . #@5#) (A B C . #@6#)))
     ((A B C D E F G)
      (A B C D E F G)
      (A B C D E F G))
     ACL2 !>'(1 2 3 4 5)
     (1 2 3 . #@1#)
     ACL2 !>'((a b c d e f g) (a b c d e f g) (a b c d e f g))
     ((A B C . #@2#) (A B C . #@3#) (A B C . #@4#))
     ACL2 !>(without-evisc '((A B C . #@4#) (A B C . #@5#) (A B C . #@6#)))
     ((A B C D E F G)
      (A B C D E F G)
      (A B C D E F G))
     ACL2 !>(without-evisc '((A B C . #@4#) (A B C . #@5#) (A B C . #@6#)))

     ***********************************************
     ************ ABORTING from raw Lisp ***********
     Error:  Out-of-bounds index in #@5#.  See :DOC set-iprint.
     ***********************************************

     If you didn't cause an explicit interrupt (Control-C),
     then the root cause may be call of a :program mode
     function that has the wrong guard specified, or even no
     guard specified (i.e., an implicit guard of t).
     See :DOC guards.

     To enable breaks into the debugger (also see :DOC acl2-customization):
     (SET-DEBUGGER-ENABLE T)
     ACL2 !>

We conclude by mentioning two cases where iprinting and evisc-tuples are
ignored.  (1) This is typically the case when printing results in raw
Lisp outside the ACL2 loop.  To use iprinting and evisc-tuples in raw
Lisp, use raw-mode; see SET-RAW-MODE.  In raw-mode, results
that are ACL2 objects will be printed in the same way that ACL2 would
print those results if not in raw-mode.  (2) Iprinting and evisc-tuples
are ignored by print-object$, which however is sensitive to many
settings that do not affect formatted (fmt etc.) printing; see
PRINT-CONTROL.

The reader interested in design and implementation issues considered
during the addition of iprinting to ACL2 is invited to read the paper
"Abbreviated Output for Input in ACL2: An Implementation Case Study";
see the proceedings of ACL2 Workshop 2009,
`http://www.cs.utexas.edu/users/moore/acl2/workshop-2009/'.

SET-PRINT-BASE    control radix in which numbers are printed

By default, integers and ratios are printed in base 10.  ACL2 also
supports printing in radix 2, 8, or 16 by calling set-print-base with
the desired radix (base).

       (set-print-base 10 state) ; Default printing
       (set-print-base 16 state) ; Print integers and ratios in hex

Here is a sample log.

       ACL2 !>(list 25 25/3)
       (25 25/3)
       ACL2 !>(set-print-base 16 state)
       <state>
       ACL2 !>(list 25 25/3)
       (19 19/3)
       ACL2 !>

See SET-PRINT-RADIX for how to print the radix, for example,
printing the decimal number 25 in print-base 16 as "#x25" rather than
"25".  Also see PRINT-CONTROL for other user-settable print
controls.

Note: ACL2 events and some other top-level commands (for example, thm,
verify, and history commands such as :pe and :pbt) set the print base
to 10 during their evaluation.  So set-print-base has no effect while
these forms are being processed.

SET-PRINT-CASE    control whether symbols are printed in upper case or in lower case

By default, symbols are printed in upper case when vertical bars are
not required, as specified by Common Lisp.  As with Common Lisp, ACL2
supports printing in a "downcase" mode, where symbols are printed in
lower case.  Many printing functions (some details below) print
characters in lower case for a symbol when the ACL2 state global
variable print-case has value :downcase and vertical bars are not
necessary for printing that symbol.  (Thus, this state global functions
in complete analogy to the Common Lisp global *print-case*.)  The value
print-case is returned by (print-case), and may be set using the
function set-print-case as follows.

       (set-print-case :upcase   state) ; Default printing
       (set-print-case :downcase state) ; Print symbols in lower case when
                                        ; vertical bars are not required

The ACL2 user can expect that the :downcase setting will have an effect
for formatted output (see FMT and see FMS) when the
directives are ~p, ~P, ~q, or ~Q, for built-in functions princ$ and
prin1$, and the ppr family of functions, and _not_ for built-in
function print-object$.  For other printing functions, the effect of
:downcase is unspecified.

Also see PRINT-CONTROL for other user-settable print controls.

SET-PRINT-CIRCLE    See PRINT-CONTROL.

SET-PRINT-ESCAPE    See PRINT-CONTROL.

SET-PRINT-LENGTH    See PRINT-CONTROL.

SET-PRINT-LEVEL    See PRINT-CONTROL.

SET-PRINT-LINES    See PRINT-CONTROL.

SET-PRINT-RADIX    control printing of the radix for numbers

See SET-PRINT-BASE for background on how the print base affects
the printing of numbers.  set-print-radix affects whether a radix
indicated when a number is printed.  The radix is not indicated by
default, or after evaluating (set-print-radix nil state).  But if
set-print-radix is called with a first argument that evaluates to a
nonnil value -- for example, (set-print-radix t state) -- then the
radix is shown when printing.  (This behavior is consistent with the
handling of Common Lisp global *print-radix*.)  The following log
illustrates how this works.

     ACL2 !>(list 25 25/3)
     (25 25/3)
     ACL2 !>(set-print-base 16 state)
     <state>
     ACL2 !>(list 25 25/3)
     (19 19/3)
     ACL2 !>(set-print-radix t state)
     <state>
     ACL2 !>(list 25 25/3)
     (#x19 #x19/3)
     ACL2 !>(set-print-base 10 state)
     <state>
     ACL2 !>(list 25 25/3)
     (25. #10r25/3)
     ACL2 !>(set-print-radix nil state)
     <state>
     ACL2 !>(list 25 25/3)
     (25 25/3)
     ACL2 !>

SET-PRINT-READABLY    See PRINT-CONTROL.

SET-PRINT-RIGHT-MARGIN    See PRINT-CONTROL.

WITHOUT-EVISC    print output in full

     General Form:
     (without-evisc form)

where form is any expression to evaluate.  The effect is to evaluate
form as though the without-evisc wrapper were absent, except that
expressions are printed in full for the ensuing output, regardless of
the current evisc-tuples (see SET-EVISC-TUPLE).  See
SET-IPRINT for an example.

More precisely, without-evisc binds each of the term-evisc-tuple,
ld-evisc-tuple, abbrev-evisc-tuple and gag-mode-evisc-tuple to nil (see
SET-EVISC-TUPLE).  It does not modify the trace evisc-tuple, so
trace output is not modified by without-evisc.  Also note that calls of
printing functions such as fmt that include explicit evisc-tuples will
not have those evisc-tuples overridden.  The following example
illustrates this point.

     ACL2 !>(without-evisc
             (fms "~x0~%"
                  (list (cons #0 '((a b ((c d)) e f g) u v w x y)))
                  *standard-co*
                  state
                  (evisc-tuple 2 3 nil nil)))

     ((A B # ...) U V ...)
     <state>
     ACL2 !>

We conclude with two remarks.  (1) A call of without-evisc on expression
exp actually invokes a specialized call of ld on a one-element list
containing exp, which prints the value returned by evaluation of exp
but actually returns the useless value (mv nil :invisible state).  So do
not use without-evisc in programs; just use it at the top level of the
ACL2 read-eval-print loop, or at least the top level of ld.  (2) Even
when using without-evisc, if the ACL2 logical world is part of the value
returned, it will be printed in abbreviated form because the ACL2
read-eval-print loop always arranges for this to be the case,
regardless of the ld-evisc-tuple.  For example:

     ACL2 !>(without-evisc (w state))
     <world>
     ACL2 !>

An alternative to the use of without-evisc is to explore large objects
using the ACL2 function (walkabout object state).  Some brief
documentation is printed when you enter an interactive loop upon
evaluating a call of walkabout.  We may add documentation for walkabout
if that is requested.

MISCELLANEOUS    a miscellany of documented functions and concepts
               (often cited in more accessible documentation)

Perhaps as the system matures this section will become more structured.

&ALLOW-OTHER-KEYS    See MACRO-ARGS.

&BODY    See MACRO-ARGS.

&KEY    See MACRO-ARGS.

&OPTIONAL    See MACRO-ARGS.

&REST    See MACRO-ARGS.

&WHOLE    See MACRO-ARGS.

A!    to return to the top-level of ACL2's command loop

When (a!) is evaluated inside of ACL2's command loop, the current
computation is aborted and control returns to the top of the command
loop, exactly as though the user had interrupted and aborted the current
computation.  (Note: Versions of ACL2 up to Version_3.4 provided `#.'
for this purpose, but no longer; see SHARP-DOT-READER.)

If you are at an ACL2 prompt (as opposed to a raw Lisp break), then you
may type :a! in place of (a!); see KEYWORD-COMMANDS.

For a related feature that only pops up one level, see P!.

Logically speaking, (a!) = nil.  But imagine that it is defined in such
a way that it causes a stack overflow or other resource exhaustion when
called.

ABORT!    to return to the top-level of ACL2's command loop

This is an alias for a!; see A!.  For a related feature that
only pops up one level, see P!.

ACKNOWLEDGMENTS    some contributors to the well-being of ACL2

The development of ACL2 was initially made possible by funding from the
U. S. Department of Defense, including ARPA and ONR.  We thank all the
organizations that have contributed support, including the following (in
alphabetical order).

     o AMD, for providing significant time over several years for Matt
     Kaufmann to carry out ACL2 research, support, and development
     o Computational Logic, Inc. and its president, Don Good, where the
     first eight years of ACL2 development occurred
     o Centaur Technology
     o DARPA
     o Digital Equipment Corporation
     o EDS, which provided some time for Matt Kaufmann's ACL2 work
     1998-1999
     o ForrestHunt and, more generally, Warren A. Hunt, Jr. (see below)
     o IBM
     o NSF
     o ONR
     o Rockwell Collins
     o SRC
     o Sun Microsystems
     o University of Texas at Austin (in particular support to J Moore
     through the Admiral B. R.  Inman Chair of Computing Theory)

We are especially grateful to Warren A. Hunt, Jr. for his unrivaled
efforts in securing support for the entire ACL2 research group at both
Computational Logic, Inc., and the University of Texas at Austin.
Without his efforts, we would have spent less time working on the
system and fewer students would have been funded to apply it.

ACL2 was started in August, 1989 by Boyer and Moore working together.
They co-authored the first versions of axioms.lisp and basis.lisp, with
Boyer taking the lead in the formalization of "state" and the most
primitive io functions.  Boyer also had a significant hand in the
development of the early versions of the files interface-raw.lisp and
translate.lisp.  For several years, Moore alone was responsible for
developing the ACL2 system code, though he consulted often with both
Boyer and Kaufmann.  In August, 1993, Kaufmann became jointly
responsible with Moore for developing the system.  Boyer has continued
to provide valuable consulting on an informal basis.

Bishop Brock was the heaviest early user of ACL2, and provided many
suggestions for improvements.  In particular, the :cases and :restrict
hints were his idea; he developed an early version of congruence-based
reasoning for Nqthm; and he helped in the development of some early
books about arithmetic.  In a demonstration of his courage and faith in
us, he pushed for Computational Logic, Inc., to agree to the Motorola
CAP contract - which required formalizing a commercial DSP in the
untested ACL2 - and moved to Scottsdale, AZ, to do the work with the
Motorola design team.  His demonstration of ACL2's utility was an
inspiration, even to those of us designing ACL2.

John Cowles also helped in the development of some early books about
arithmetic, and also provided valuable feedback and bug reports.

Other early users of ACL2 at Computational Logic, Inc. helped influence
its development.  In particular, Warren Hunt helped with the port to
Macintosh Common Lisp, and Art Flatau and Mike Smith provided useful
general feedback.

Mike Smith helped develop the Emacs portion of the implementation of
proof trees.

Bill Schelter made some enhancements to akcl (now gcl) that helped to
enhance ACL2 performance in that Common Lisp implementation, and more
generally, responded helpfully to our bug reports.  Camm Maguire has
since provided wonderful gcl support, and has created a Debian package
for ACL2 built on GCL.  We are also grateful to developers of other
Common Lisp implementations.

Kent Pitman helped in our interaction with the ANSI Common Lisp
standardization committee, X3J13.

John Cowles helped with the port to Windows (98) by answering questions
and running tests.

Ruben Gamboa created a modification of ACL2 to allow reasoning about
the real numbers using non-standard analysis.  His work has been
incorporated into the ACL2 distribution; see REAL.

Rob Sumners has made numerous useful suggestions.  In particular, he has
designed and implemented improvements for stobjs and been key in our
development of locally-bound stobjs; see NOTE-2-6.

Robert Krug has designed and implemented many changes in the vicinity
of the linear arithmetic package and its connection to type-set and
rewrite.  He was also instrumental in the development of
extended-metafunctions.

Pete Manolios has made numerous useful suggestions.  In particular, Pete
helped us to organize the first workshop and was a wonderful equal
partner with the two of us (Kaufmann and Moore) in producing the books
that arose from that workshop.  Pete and his student, Daron Vroon,
provided the current implementation of ordinals.

Jared Davis and Sol Swords have our gratitude for starting the
acl2-books repository, `http://acl2-books.googlecode.com/'.

We thank David L. Rager for contributing an initial version of the
support for parallelism in an experimental extension of ACL2.

Bob Boyer and Warren A. Hunt, Jr. developed a canonical representation
for ACL2 data objects and a function memoization mechanism to
facilitate reuse of previously computed results.  We thank them for
their extensive efforts for the corresponding experimental (as of 2008
and 2009) extension of ACL2; see HONS-AND-MEMOIZATION.

We also thank the contributors to the ACL2 workshops for some suggested
improvements and for the extensive collection of publicly distributed
benchmark problems.  And we thank participants at the ACL2 seminar at
the University of Texas for useful feedback.  More generally, we thank
the ACL2 community for feedback, contributed books (see
COMMUNITY-BOOKS), and their interest in the ACL2 project.

_Regarding the documentation:_

     Bill Young wrote significant portions of the original acl2-tutorial
     section of the ACL2 documentation, including what is now called
     alternative-introduction.  This was an especially important task
     in the early years when there was no guide for how to use ACL2 and
     we are very grateful.  He, Bishop Brock, Rich Cohen, and Noah
     Friedman read over considerable amounts of the documentation, and
     made many useful comments.  Others, particularly Bill Bevier and
     John Cowles, have also made useful comments on the documentation.

     Art Flatau helped develop the ACL2 markup language and translators
     from that language to Texinfo and HTML.  Michael "Bogo" Bogomolny
     created a search engine, beginning with Version 2.6, and for that
     purpose modified the HTML translator to create one file per topic
     (a good idea in any case).

     Laura Lawless provided many hours of help in marking up
     appropriate parts of the documentation in typewriter font.

     Noah Friedman developed an Emacs tool that helped us insert
     "invisible links" into the documentation, which improve the
     usability of that documentation under HTML readers such as Mosaic.

     Richard Stallman contributed a texinfo patch, to be found in the
     file doc/texinfo.tex.

ACL2S    See ACL2-SEDAN.

APROPOS    searching the documentation online

The :docs command allows you to search the documentation at the
terminal.  See DOCS.

BACKCHAIN-LIMIT    limiting the effort expended on relieving hypotheses

Before ACL2 can apply a rule with hypotheses, it must establish that the
hypotheses are true.  (We ignore the relaxing of this requirement
afforded by case-splits and forced hypotheses.)  ACL2 typically
establishes each hypothesis by backchaining -- instantiating the
hypothesis and then rewriting it recursively.  Here we describe how
ACL2 allows the user to limit backchaining.  At the end, below, we
describe the function backchain-limit.

Each hypothesis of a rewrite, meta, linear, or type-prescription rule
is assigned a backchain-limit when the rule is stored.  By default,
this limit is nil, denoting infinity (no limit).  However, the value
used for the default may be set to a non-negative integer (or to nil)
by the user; see SET-DEFAULT-BACKCHAIN-LIMIT.  The default is
overridden when a :backchain-limit-lst is supplied explicitly with the
rule; see RULE-CLASSES.  The number of recursive applications of
backchaining starting with the hypothesis of a rule is limited to the
backchain-limit associated with that hypothesis.

Moreover, the user may set global backchain-limits that limit the total
backchaining depth.  See SET-BACKCHAIN-LIMIT.  One limit is for
the use of rewrite, meta, and linear rules, while the other limit is
for so-called "type-set reasoning", which uses rules of class
type-prescription rules.  The two limits operate independently.  Below,
we discuss the first kind of backchain limits, i.e., for other than
type-prescription rules, except as otherwise indicated; but the
mechanism for those rules is similar.

Below we lay out the precise sense in which a global backchain-limit
interacts with the backchain-limits of individual rules in order to
limit backchaining.  But first we note that when further backchaining is
disallowed, ACL2 can still prove a hypothesis in a given context by
using that contextual information.  In fact, type-set reasoning may be
used (except that a weaker version of it is used in the second case
above, i.e., where we are already doing type-set reasoning).  Thus, the
relieving of hypotheses may be limited to the use of contextual
information (without backchaining, i.e., without recursively rewriting
hypotheses) by executing :set-backchain-limit 0.

Recall that there are two sorts of backchain limits: those applied to
hypotheses of individual rules, as assigned by their :rule-classes or
else taken from the default (see SET-DEFAULT-BACKCHAIN-LIMIT);
and the global limit, initially nil (no limit) but settable with
:set-backchain-limit.  Here is how these two types of limits interact
to limit backchaining, i.e., recursive rewriting of hypotheses.  ACL2
maintains a current backchain limit, which is the limit on the depth of
recursive calls to the rewriter, as well as a current backchain depth,
which is initially 0 and is incremented each time ACL2 backchains (and
is decremented when a backchain completes).  When ACL2 begins to
rewrite a literal (crudely, one of the "top-level" terms of the goal
currently being worked on), it sets the current backchain-limit to the
global value, which is initially nil but can be set using
:set-backchain-limit.  When ACL2 is preparing to relieve a hypothesis
by backchaining (hence, after it has already tried type-set reasoning),
it first makes sure that the current backchain limit is greater than
the current backchain depth.  If not, then it refuses to relieve that
hypothesis.  Otherwise, it increments the current backchain depth and
calculates a new current backchain-limit by taking the minimum of two
values: the existing current backchain-limit, and the sum of the
current backchain depth and the backchain-limit associated with the
hypothesis.  Thus, ACL2 only modifies the current backchain-limit if it
is necessary to decrease that limit in order to respect the backchain
limit associated with the hypothesis.

We illustrate with the following examples.

     ; We stub out some functions so that we can reason about them.

     (defstub p0 (x) t)
     (defstub p1 (x) t)
     (defstub p2 (x) t)
     (defstub p3 (x) t)

     ; Initially, the default-backchain-limit is nil, or infinite.

     (defaxiom p2-implies-p1-limitless
       (implies (p2 x)
                (p1 x)))

     ; The following rule will have a backchain-limit of 0.

     (defaxiom p1-implies-p0-limit-0
       (implies (p1 x)
                (p0 x))
       :rule-classes ((:rewrite :backchain-limit-lst 0)))

     ; We have (p2 x) ==> (p1 x) ==> (p0 x).  We wish to establish that
     ; (p2 x) ==> (p0 x).  Normally, this would be no problem, but here
     ; we fail because ACL2 cannot establish (p0 x) by type-set reasoning
     ; alone.

     (thm
       (implies (p2 x)
                (p0 x)))

     ; We set the default-backchain-limit (for rewriting) to 1.

     :set-default-backchain-limit 1

     ; The following is more powerful than p1-implies-p0-limit-0
     ; because it can use rewrite rules to establish (p1 x).

     (defaxiom p1-implies-p0-limit-1
       (implies (p1 x)
                (p0 x)))

     ; This theorem will succeed:

     (thm
       (implies (p2 x)
                (p0 x)))

     ; We return the default-backchain-limit to its initial value.

     :set-default-backchain-limit nil

     ; Here is our last axiom.

     (defaxiom p3-implies-p2-limitless
       (implies (p3 x)
                (p2 x)))

     ; We now have (p3 x) ==> (p2 x) ==> (p1 x) ==> (p0 x).  However the
     ; rule p1-implies-p0-limit-1 has a backchain-limit of 1; hence we
     ; are not allowed to backchain far enough back to use
     ; p3-implies-p2-limitless.  We therefore lose.

     (defthm will-fail
       (implies (p3 x)
                (p0 x)))

Finally, we remark that to see the current global backchain-limits,
issue the following commands.

     (backchain-limit wrld :ts) ; backchain limit for type-set reasoning
     (backchain-limit wrld :rewrite) ; backchain limit for rewriting

BACKCHAIN-LIMIT-RW    hints keyword :BACKCHAIN-LIMIT-RW

See HINTS.

BACKTRACK    hints keyword :BACKTRACK

See HINTS.

BIBLIOGRAPHY    reports about ACL2

For a list of notes and reports about ACL2, see
`http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html'.

BIND-FREE    to bind free variables of a rewrite or linear rule

     Examples:
     (IMPLIES (AND (RATIONALP LHS)
                   (RATIONALP RHS)
                   (BIND-FREE (FIND-MATCH-IN-PLUS-NESTS LHS RHS) (X)))
              (EQUAL (EQUAL LHS RHS)
                     (EQUAL (+ (- X) LHS) (+ (- X) RHS))))

     (IMPLIES (AND (BIND-FREE
                     (FIND-RATIONAL-MATCH-IN-TIMES-NESTS LHS RHS MFC STATE)
                     (X))
                   (RATIONALP X)
                   (CASE-SPLIT (NOT (EQUAL X 0))))
              (EQUAL (< LHS RHS)
                     (IF (< 0 X)
                         (< (* (/ X) LHS) (* (/ X) RHS))
                        (< (* (/ X) RHS) (* (/ X) LHS)))))

General Forms:

     (BIND-FREE term var-list)
     (BIND-FREE term t)
     (BIND-FREE term)

A rule which uses a bind-free hypothesis has similarities to both a
rule which uses a syntaxp hypothesis and to a :meta rule.  Bind-free is
like syntaxp, in that it logically always returns t but may affect the
application of a :rewrite or :linear rule when it is called at the
top-level of a hypothesis.  It is like a :meta rule, in that it allows
the user to perform transformations of terms under progammatic control.

Note that a bind-free hypothesis does not, in general, deal with the
meaning or semantics or values of the terms, but rather with their
syntactic forms.  Before attempting to write a rule which uses
bind-free, the user should be familiar with syntaxp and the internal
form that ACL2 uses for terms.  This internal form is similar to what
the user sees, but there are subtle and important differences.  Trans
can be used to view this internal form.

Just as for a syntaxp hypothesis, there are two types of bind-free
hypotheses.  The simpler type of bind-free hypothesis may be used as
the nth hypothesis in a :rewrite or :linear rule whose :corollary is
(implies (and hyp1 ... hypn ... hypk) (equiv lhs rhs)) provided term is
a term, term contains at least one variable, and every variable
occuring freely in term occurs freely in lhs or in some hypi, i<n.  In
addition, term must not use any stobjs.  (Later below we will describe
the second type, an _extended_ bind-free hypothesis, which may use
state.)

We begin our description of bind-free by examining the first example
above in some detail.

We wish to write a rule which will cancel "like" addends from both
sides of an equality.  Clearly, one could write a series of rules such
as

     (DEFTHM THE-HARD-WAY-2-1
        (EQUAL (EQUAL (+ A X B)
                      (+ X C))
               (EQUAL (+ A B)
                      (FIX C))))

with one rule for each combination of positions the matching addends
might be found in (if one knew before-hand the maximum number of
addends that would appear in a sum).  But there is a better way.  (In
what follows, we assume the presence of an appropriate set of rules for
simplifying sums.)

Consider the following definitions and theorem:

     (DEFUN INTERSECTION-EQUAL (X Y)
       (COND ((ENDP X)
              NIL)
             ((MEMBER-EQUAL (CAR X) Y)
              (CONS (CAR X) (INTERSECTION-EQUAL (CDR X) Y)))
             (T
              (INTERSECTION-EQUAL (CDR X) Y))))

     (DEFUN PLUS-LEAVES (TERM)
       (IF (EQ (FN-SYMB TERM) 'BINARY-+)
           (CONS (FARGN TERM 1)
                 (PLUS-LEAVES (FARGN TERM 2)))
         (LIST TERM)))

     (DEFUN FIND-MATCH-IN-PLUS-NESTS (LHS RHS)
       (IF (AND (EQ (FN-SYMB LHS) 'BINARY-+)
                (EQ (FN-SYMB RHS) 'BINARY-+))
           (LET ((COMMON-ADDENDS (INTERSECTION-EQUAL (PLUS-LEAVES LHS)
                                                     (PLUS-LEAVES RHS))))
             (IF COMMON-ADDENDS
                 (LIST (CONS 'X (CAR COMMON-ADDENDS)))
               NIL))
         NIL))

     (DEFTHM CANCEL-MATCHING-ADDENDS-EQUAL
       (IMPLIES (AND (RATIONALP LHS)
                     (RATIONALP RHS)
                     (BIND-FREE (FIND-MATCH-IN-PLUS-NESTS LHS RHS) (X)))
                (EQUAL (EQUAL LHS RHS)
                       (EQUAL (+ (- X) LHS) (+ (- X) RHS)))))

How is this rule applied to the following term?

     (equal (+ 3 (expt a n) (foo a c))
            (+ (bar b) (expt a n)))

As mentioned above, the internal form of an ACL2 term is not always
what one sees printed out by ACL2.  In this case, by using :trans one
can see that the term is stored internally as

     (equal (binary-+ '3
                      (binary-+ (expt a n) (foo a c)))
            (binary-+ (bar b) (expt a n))).

When ACL2 attempts to apply cancel-matching-addends-equal to the term
under discussion, it first forms a substitution that instantiates the
left-hand side of the conclusion so that it is identical to the target
term.  This substitution is kept track of by the substitution alist:

     ((LHS . (binary-+ '3
                        (binary-+ (expt a n) (foo a c))))
      (RHS . (binary-+ (bar b) (expt a n)))).

ACL2 then attempts to relieve the hypotheses in the order they were
given. Ordinarily this means that we instantiate each hypothesis with
our substitution and then attempt to rewrite the resulting instance to
true.  Thus, in order to relieve the first hypothesis, we rewrite:

     (RATIONALP (binary-+ '3
                           (binary-+ (expt a n) (foo a c)))).

Let us assume that the first two hypotheses rewrite to t.  How do we
relieve the bind-free hypothesis?  Just as for a syntaxp hypothesis,
ACL2 evaluates (find-match-in-plus-nests lhs rhs) in an environment
where lhs and rhs are instantiated as determined by the substitution.
In this case we evaluate

     (FIND-MATCH-IN-PLUS-NESTS '(binary-+ '3
                                           (binary-+ (expt a n) (foo a c)))
                               '(binary-+ (bar b) (expt a n))).

Observe that, just as in the case of a syntaxp hypothesis, we
substitute the quotation of the variables bindings into the term to be
evaluated.  See SYNTAXP for the reasons for this.  The result
of this evaluation, ((X . (EXPT A N))), is then used to extend the
substitution alist:

     ((X . (EXPT A N))
      (LHS . (binary-+ '3
                        (binary-+ (expt a n) (foo a c))))
      (RHS . (binary-+ (bar b) (expt a n)))),

and this extended substitution determines
cancel-matching-addends-equal's result:

     (EQUAL (+ (- X) LHS) (+ (- X) RHS))
     ==>
     (EQUAL (+ (- (EXPT A N)) 3 (EXPT A N) (FOO A C))
            (+ (- (EXPT A N)) (BAR B) (EXPT A N))).

Question: What is the internal form of this result?
Hint: Use :trans.

When this rule fires, it adds the negation of a common term to both
sides of the equality by selecting a binding for the otherwise-free
variable x, under programmatic control.  Note that other mechanisms
such as the binding of free-variables may also extend the substitution
alist.

Just as for a syntaxp test, a bind-free form signals failure by
returning nil.  However, while a syntaxp test signals success by
returning true, a bind-free form signals success by returning an alist
which is used to extend the current substitution alist.  Because of
this use of the alist, there are several restrictions on it -- in
particular the alist must only bind variables, these variables must not
be already bound by the substitution alist, and the variables must be
bound to ACL2 terms.  If term returns an alist and the alist meets
these restrictions, we append the alist to the substitution alist and
use the result as the new current substitution alist.  This new current
substitution alist is then used when we attempt to relieve the next
hypothesis or, if there are no more, instantiate the right hand side of
the rule.

There is also a second, optional, var-list argument to a bind-free
hypothesis.  If provided, it must be either t or a list of variables.
If it is not provided, it defaults to t.  If it is a list of variables,
this second argument is used to place a further restriction on the
possible values of the alist to be returned by term: any variables
bound in the alist must be present in the list of variables.  We
strongly recommend the use of this list of variables, as it allows some
consistency checks to be performed at the time of the rule's admittance
which are not possible otherwise.

An extended bind-free hypothesis is similar to the simple type
described above, but it uses two additional variables, mfc and state,
which must not be bound by the left hand side or an earlier hypothesis
of the rule.  They must be the last two variables mentioned by term:
first mfc, then state.  These two variables give access to the
functions mfc-xxx; see EXTENDED-METAFUNCTIONS.  As described
there, mfc is bound to the so-called metafunction-context and state to
ACL2's state.  See BIND-FREE-EXAMPLES for examples of the use
of these extended bind-free hypotheses.

BIND-FREE-EXAMPLES    examples pertaining to bind-free hypotheses

See BIND-FREE for a basic discussion of the use of bind-free to
control rewriting.

We give examples of the use of bind-free hypotheses from the
perspective of a user interested in reasoning about arithmetic, but it
should be clear that bind-free can be used for many other purposes also.

EXAMPLE 1:  Cancel a common factor.

     (defun bind-divisor (a b)

     ; If a and b are polynomials with a common factor c, we return a
     ; binding for x.  We could imagine writing get-factor to compute the
     ; gcd, or simply to return a single non-invertible factor.

       (let ((c (get-factor a b)))
         (and c (list (cons 'x c)))))

     (defthm cancel-factor
       ;; We use case-split here to ensure that, once we have selected
       ;; a binding for x, the rest of the hypotheses will be relieved.
       (implies (and (acl2-numberp a)
                     (acl2-numberp b)
                     (bind-free (bind-divisor a b) (x))
                     (case-split (not (equal x 0)))
                     (case-split (acl2-numberp x)))
                (iff (equal a b)
                     (equal (/ a x) (/ b x)))))

EXAMPLE 2:  Pull integer summand out of floor.  Note:  This example has
an _extended_ bind-free hypothesis, which uses the term
(find-int-in-sum sum mfc state).

     (defun fl (x)
       ;; This function is defined, and used, in the IHS books.
       (floor x 1))

     (defun int-binding (term mfc state)
       ;; The call to mfc-ts returns the encoded type of term. ;
       ;; Thus, we are asking if term is known by type reasoning to ;
       ;; be an integer. ;
       (declare (xargs :stobjs (state) :mode :program))
       (if (ts-subsetp (mfc-ts term mfc state)
                       *ts-integer*)
           (list (cons 'int term))
         nil))

     (defun find-int-in-sum (sum mfc state)
       (declare (xargs :stobjs (state) :mode :program))
       (if (and (nvariablep sum)
                (not (fquotep sum))
                (eq (ffn-symb sum) 'binary-+))
           (or (int-binding (fargn sum 1) mfc state)
               (find-int-in-sum (fargn sum 2) mfc state))
         (int-binding sum mfc state)))

     ; Some additional work is required to prove the following.  So for
     ; purposes of illustration, we wrap skip-proofs around the defthm.

     (skip-proofs
      (defthm cancel-fl-int
       ;; The use of case-split is probably not needed, since we should
       ;; know that int is an integer by the way we selected it.  But this
       ;; is safer.
        (implies (and (acl2-numberp sum)
                      (bind-free (find-int-in-sum sum mfc state) (int))
                      (case-split (integerp int)))
                 (equal (fl sum)
                        (+ int (fl (- sum int)))))
        :rule-classes ((:rewrite :match-free :all)))
     )

     ; Arithmetic libraries will have this sort of lemma.
     (defthm hack (equal (+ (- x) x y) (fix y)))

     (in-theory (disable fl))

     (thm (implies (and (integerp x) (acl2-numberp y))
                   (equal (fl (+ x y)) (+ x (fl y)))))

EXAMPLE 3:  Simplify terms such as (equal (+ a (* a b)) 0)

     (defun factors (product)
       ;; We return a list of all the factors of product.  We do not
       ;; require that product actually be a product.
       (if (eq (fn-symb product) 'BINARY-*)
           (cons (fargn product 1)
                 (factors (fargn product 2)))
         (list product)))

     (defun make-product (factors)
       ;; Factors is assumed to be a list of ACL2 terms.  We return an
       ;; ACL2 term which is the product of all the ellements of the
       ;; list factors.
       (cond ((atom factors)
              ''1)
             ((null (cdr factors))
              (car factors))
             ((null (cddr factors))
              (list 'BINARY-* (car factors) (cadr factors)))
             (t
              (list 'BINARY-* (car factors) (make-product (cdr factors))))))

     (defun quotient (common-factors sum)
       ;; Common-factors is a list of ACL2 terms.   Sum is an ACL2 term each
       ;; of whose addends have common-factors as factors.  We return
       ;; (/ sum (make-product common-factors)).
       (if (eq (fn-symb sum) 'BINARY-+)
           (let ((first (make-product (set-difference-equal (factors (fargn sum 1))
                                                            common-factors))))
             (list 'BINARY-+ first (quotient common-factors (fargn sum 2))))
         (make-product (set-difference-equal (factors sum)
                                             common-factors))))

     (defun intersection-equal (x y)
       (cond ((endp x)
              nil)
             ((member-equal (car x) y)
              (cons (car x) (intersection-equal (cdr x) y)))
             (t
              (intersection-equal (cdr x) y))))

     (defun common-factors (factors sum)
       ;; Factors is a list of the factors common to all of the addends
       ;; examined so far.  On entry, factors is a list of the factors in
       ;; the first addend of the original sum, and sum is the rest of the
       ;; addends.  We sweep through sum, trying to find a set of factors
       ;; common to all the addends of sum.
       (declare (xargs :measure (acl2-count sum)))
       (cond ((null factors)
              nil)
             ((eq (fn-symb sum) 'BINARY-+)
              (common-factors (intersection-equal factors (factors (fargn sum 1)))
                              (fargn sum 2)))
             (t
              (intersection-equal factors (factors sum)))))

     (defun simplify-terms-such-as-a+ab-rel-0-fn (sum)
       ;; If we can find a set of factors common to all the addends of sum,
       ;; we return an alist binding common to the product of these common
       ;; factors and binding quotient to (/ sum common).
       (if (eq (fn-symb sum) 'BINARY-+)
           (let ((common-factors (common-factors (factors (fargn sum 1))
                                                 (fargn sum 2))))
             (if common-factors
                 (let ((common (make-product common-factors))
                       (quotient (quotient common-factors sum)))
                   (list (cons 'common common)
                         (cons 'quotient quotient)))
               nil))
         nil))

     (defthm simplify-terms-such-as-a+ab-=-0
       (implies (and (bind-free
                      (simplify-terms-such-as-a+ab-rel-0-fn sum)
                      (common quotient))
                     (case-split (acl2-numberp common))
                     (case-split (acl2-numberp quotient))
                     (case-split (equal sum
                                        (* common quotient))))
                (equal (equal sum 0)
                       (or (equal common 0)
                           (equal quotient 0)))))

     (thm (equal (equal (+ u (* u v)) 0)
           (or (equal u 0) (equal v -1))))

BY    hints keyword :BY

See HINTS.

CASE-SPLIT    like force but immediately splits the top-level goal on the hypothesis

When a hypothesis of a conditional rule has the form (case-split hyp)
it is logically equivalent to hyp.  However it affects the application
of the rule generated as follows:  if ACL2 attempts to apply the rule
but cannot establish that the required instance of hyp holds in the
current context, it considers the hypothesis true anyhow, but (assuming
all hypotheses are seen to be true and the rule is applied) creates a
subgoal in which that instance of hyp is assumed false.  (There are
exceptions, noted below.)

For example, given the rule

     (defthm p1->p2
       (implies (case-split (p1 x))
                (p2 x)))

then an attempt to prove

     (implies (p3 x) (p2 (car x)))

can give rise to a single subgoal:

     (IMPLIES (AND (NOT (P1 (CAR X))) (P3 X))
              (P2 (CAR X))).

Unlike force, case-split does not delay the "false case" to a forcing
round but tackles it more or less immediately.

The special "split" treatment of case-split can be disabled by
disabling forcing:  see FORCE for a discussion of disabling
forcing, and also see DISABLE-FORCING.  Finally, we should
mention that the rewriter is never willing to split when there is an if
term present in the goal being simplified.  Since and terms and or
terms are merely abbreviations for if terms, they also prevent
splitting.  Note that if terms are ultimately eliminated using the
ordinary flow of the proof (but see
SET-CASE-SPLIT-LIMITATIONS), so case-split will ultimately function
as intended.

When in the proof checker, case-split behaves like force.

CASE-SPLIT-LIMITATIONS    a list of two "numbers" limiting the number of cases produced at once

     Examples:
     ACL2 !>(case-split-limitations (w state))
     (500 100)

With the setting above, clausify will not try subsumption/replacement
if more than 500 clauses are involved.  Furthermore, the simplifier, as
it sweeps over a clause, will inhibit further case splits when it has
accumulated 100 subgoals.  This inhibition is implemented by continuing
to rewrite subsequent literals but not splitting out their cases.  This
can produce literals containing IFs.

See SET-CASE-SPLIT-LIMITATIONS for a more general discussion.

CASES    hints keyword :CASES

See HINTS.

CLAUSE-IDENTIFIER    the internal form of a goal-spec

To each goal-spec, str, there corresponds a clause-identifier produced
by (parse-clause-id str).  For example,

     (parse-clause-id "[2]Subgoal *4.5.6/7.8.9'''")

returns ((2 4 5 6) (7 8 9) . 3).

The function string-for-tilde-@-clause-id-phrase inverts
parse-clause-id in the sense that given a clause identifier it returns
the corresponding goal-spec.

As noted in the documentation for goal-spec, each clause printed in the
theorem prover's proof attempt is identified by a name.  When these
names are represented as strings they are called "goal specs."  Such
strings are used to specify where in the proof attempt a given hint is
to be applied.  The function parse-clause-id converts goal-specs into
clause identifiers, which are cons-trees containing natural numbers.

Examples of goal-specs and their corresponding clause identifiers are
shown below.

                  parse-clause-id
                        -->

     "Goal"                       ((0) NIL . 0)
     "Subgoal 3.2.1'"             ((0) (3 2 1) . 1)
     "[2]Subgoal *4.5.6/7.8.9'''" ((2 4 5 6) (7 8 9) . 3)

                        <--
           string-for-tilde-@-clause-id-phrase

The caar of a clause id specifies the forcing round, the cdar specifies
the goal being proved by induction, the cadr specifies the particular
subgoal, and the cddr is the number of primes in that subgoal.

Internally, the system maintains clause ids, not goal-specs.  The
system prints clause ids in the form shown by goal-specs.  When a
goal-spec is used in a hint, it is parsed (before the proof attempt
begins) into a clause id.  During the proof attempt, the system watches
for the clause id and uses the corresponding hint when the id arises.
(Because of the expense of creating and garbage collecting a lot of
strings, this design is more efficient than the alternative.)

COMMAND    forms you type at the top-level, but...

...the word "command" usually refers to a top-level form whose
evaluation produces a new logical world.

     Typical commands are:
     (defun foo (x) (cons x x))
     (defthm consp-foo (consp (foo x)))
     (defrec pair (hd . tl) nil)

The first two forms are examples of commands that are in fact primitive
events.  See EVENTS.  Defrec, on the other hand, is a macro
that expands into a progn of several primitive events.  In general, a
world extending command generates one or more events.

Both events and commands leave landmarks on the world that enable us to
determine how the given world was created from the previous one.  Most
of your interactions will occur at the command level, i.e., you type
commands, you print previous commands, and you undo back through
commands.  Commands are denoted by command descriptors.  See
COMMAND-DESCRIPTOR.

COMMAND-DESCRIPTOR    an object describing a particular command typed by the user

     Examples:

     :max      ; the command most recently typed by the user
     :x        ; synonymous with :max
     (:x -1)   ; the command before the most recent one
     (:x -2)   ; the command before that
     :x-2      ; synonymous with (:x -2)
     5         ; the fifth command typed by the user
     1         ; the first command typed by the user
     0         ; the last command of the system initialization
     -1        ; the next-to-last initialization command
     :min      ; the first command of the initialization
     :start    ; the last command of the initial ACL2 logical world
     fn        ; the command that introduced the logical name fn
     (:search (defmacro foo-bar))
               ; the first command encountered in a search from :max to
               ; 0 that either contains defmacro and foo-bar in the
               ; command form or contains defmacro and foo-bar in some
               ; event within its block.

The recorded history of your interactions with the top-level ACL2
command loop is marked by the commands you typed that changed the
logical world.  Each such command generated one or more events, since
the only way for you to change the logical world is to execute an event
function.  See COMMAND and see EVENTS.  We divide
history into "command blocks," grouping together each world changing
command and its events.  A "command descriptor" is an object that can
be used to describe a particular command in the history of the ongoing
session.

Each command is assigned a unique integer called its "command number"
which indicates the command's position in the chronological ordering of
all of the commands ever executed in this session (including those
executed to initialize the system).  We assign the number 1 to the
first command you type to ACL2.  We assign 2 to the second and so on.
The non-positive integers are assigned to "prehistoric" commands, i.e.,
the commands used to initialize the ACL2 system: 0 is the last command
of the initialization, -1 is the one before that, etc.

The legal command descriptors are described below.  We use n to denote
any integer, sym to denote any logical name (see LOGICAL-NAME),
and cd to denote, recursively, any command descriptor.

      command                   command
     descriptor                described

     :max   -- the most recently executed command (i.e., the one with
               the largest command number)
     :x     -- synonymous with :max
     :x-k   -- synonymous with (:x -k), if k is an integer and k>0
     :min   -- the earliest command (i.e., the one with the smallest
               command number and hence the first command of the system
               initialization)
     :start -- the last command when ACL2 starts up
     n      -- command number n  (If n is not in the
               range :min<=n<=:max, n is replaced by the nearest of :min
               and :max.)
     sym    -- the command that introduced the logical name sym
     (cd n) -- the command whose number is n plus the command number of
               the command described by cd
     (:search pat cd1 cd2)
               In this command descriptor, pat must be either an atom or
               a true list of atoms and cd1 and cd2 must be command
               descriptors.  We search the interval from cd1 through cd2
               for the first command that matches pat.  Note that if cd1
               occurs chronologically after cd2, the search is
               ``backwards'' through history while if cd1 occurs
               chronologically before cd2, the search is ``forwards''.  A
               backwards search will find the most recent match; a
               forward search will find the chronologically earliest
               match.  A command matches pat if either the command form
               itself or one of the events in the block contains pat (or
               all of the atoms in pat if pat is a list).
     (:search pat)
               the command found by (:search pat :max 0), i.e., the most
               recent command matching pat that was part of the user's
               session, not part of the system initialization.

COMMON-LISP    relation to Common Lisp, including deviations from the spec

ACL2 is a logic, a theorem prover, and a programming language based on
Common Lisp.  A connection with Common Lisp is established with guards
(see GUARD).

However, here we document potential deviations from Common Lisp
semantics even in the presence of verified guards.  Our view is that
these deviations are extremely unlikely to manifest; indeed, as of this
writing we are unaware of any cases in which these issues arise in
practice.  However, we feel obligated to acknowledge their possibility,
which could result in surprises during evaluation or even proof.

The Common Lisp spec allows certain predicates to return what it calls
"generalized Booleans," which are really arbitrary values that are to be
viewed as either nil or non-nil.  However, in ACL2 these functions are
assumed to return nil or t.  For details,see
GENERALIZED-BOOLEANS.

The execution of forms with :program mode functions can result in calls
of functions on arguments that do not satisfy their guards.  In
practice, this simply causes hard Lisp errors.  But in principle one
could imagine a damaged Lisp image that operates incorrectly.  See
DEFUN-MODE-CAVEAT.

The Common Lisp spec, specifically Section 3.2.2.3 of the Common Lisp
HyperSpec, allows for undefined results when a function is "multiply
defined" in a compiled file.  ACL2 allows redundant defuns in a book,
and in general books are compiled by certify-book (but see
CERTIFY-BOOK and see COMPILATION for how to control such
compilation).  Moreover, ACL2 provides a redefinition capability (see
LD-REDEFINITION-ACTION and see REDEF), and the above
section also allows for undefined results when a function is defined in
a compiled file and then redefined, presumably (for example) because of
inlining.

DEFUN-MODE-CAVEAT    potential soundness issue for functions with defun-mode :program

Technically speaking, in the current implementation, the execution of
functions having defun-mode :program may damage the ACL2 system in a
way that renders it unsound.  In practice, we have never seen this
happen; so, the explanations below can be viewed as extremely paranoid.
Nevertheless, here we document this concern, even if it should be taken
with more than a grain of salt.

See DEFUN-MODE for a discussion of defun-modes.  That discussion
describes an imagined implementation that is slightly different from
this one.  This note explains that the current implementation is open to
unsoundness.

For discussion of a different soundness issue that is also related to
function execution, see GENERALIZED-BOOLEANS.

The execution of a function having defun-mode :program may violate
Common Lisp guards on the subroutines used.  (This may be true even for
calls of a function on arguments that satisfy its guard, because ACL2
has not verified that its guard is sufficient to protect its
subroutines.)  When a guard is violated at runtime all bets are off.
That is, no guarantees are made either about the answer being "right"
or about the continued rationality of the ACL2 system itself.

For example, suppose you make the following defun:

     (defun crash (i)
       (declare (xargs :mode :program :guard (integerp i)))
       (car i))

Note that the declared guard does not in fact adequately protect the
subroutines in the body of crash; indeed, satisfying the guard to crash
will guarantee that the car expression is in violation of its guard.
Because this function is admitted in :program-mode, no checks are made
concerning the suitability of the guard.  Furthermore, in the current
ACL2 implementation, crash is executed directly in Common Lisp.  Thus
if you call crash on an argument satisfying its guard you will cause an
erroneous computation to take place.

     ACL2 !>(crash 7)

     Error: Caught fatal error [memory may be damaged]
     ...

There is no telling how much damage is done by this errant computation.
In some lisps your ACL2 job may actually crash back to the operating
system.  In other lisps you may be able to recover from the "hard
error" and resume ACL2 in a damaged but apparently functional image.

THUS, HAVING A FUNCTION WITH DEFUN-MODE :PROGRAM IN YOUR SYSTEM
ABSOLVES US, THE ACL2 IMPLEMENTORS, FROM RESPONSIBILITY FOR THE
SOUNDNESS OF OUR SYSTEM.

Furthermore

ACL2 DOES NOT YET PROVIDE ANY MEANS OF REGAINING ASSURANCES OF
SOUNDNESS AFTER THE INTRODUCTION OF A FUNCTION IN :PROGRAM MODE, EVEN
IF IT IS ULTIMATELY CONVERTED TO :LOGIC MODE (since its execution could
have damaged the system in a way that makes it possible to verify its
termination and guards unsoundly).

Finally,

THE VAST MAJORITY OF ACL2 SYSTEM CODE IS IN :PROGRAM MODE AND SO ALL
BETS ARE OFF FROM BEFORE YOU START!

This hopeless state of current affairs will change, we think.  We think
we have defined our functions "correctly" in the sense that they can be
converted, without "essential" modification, to :logic mode.  We think
it very unlikely that a mis-guarded function in :program mode (whether
ours or yours) will cause unsoundness without some sort of hard lisp
error accompanying it.  We think that ultimately we can make it
possible to execute your functions (interpretively) without risk to the
system, even when some have :program mode.  In that imagined
implementation, code using functions having :program mode would run
more slowly, but safely.  These functions could be introduced into the
logic ex post facto, whereupon the code's execution would speed up
because Common Lisp would be allowed to execute it directly.  We
therefore ask that you simply pretend that this is that imagined
implementation, introduce functions in :program mode, use them as
convenient and perhaps ultimately introduce some of them in :logic mode
and prove their properties.  If you use the system this way we can
develop (or dismiss) this style of formal system development.  BUT BE
ON THE LOOKOUT FOR SCREWUPS DUE TO DAMAGE CAUSED BY THE EXECUTION OF
YOUR FUNCTIONS HAVING :PROGRAM MODE!

GENERALIZED-BOOLEANS    potential soundness issues related to ACL2 predicates

The discussion below outlines a potential source of unsoundness in
ACL2.  Although to our knowledge there is no existing Lisp
implementation in which this problem can arise, nevertheless we feel
compelled to explain this situation.

Consider for example the question:  What is the value of (equal 3 3)?
According to the ACL2 axioms, it's t.  And as far as we know, based on
considerable testing, the value is t in every Common Lisp
implementation.  However, according the Common Lisp draft proposed ANSI
standard, any non-nil value could result.  Thus for example, (equal 3
3) is allowed by the standard to be 17.

The Common Lisp standard specifies (or soon will) that a number of
Common Lisp functions that one might expect to return Boolean values
may, in fact, return arbitrary values.  Examples of such functions are
equal, rationalp, and <; a much more complete list is given below.
Indeed, we dare to say that every Common Lisp function that one may
believe returns only Booleans is, nevertheless, not specified by the
standard to have that property, with the exceptions of the functions
not and null.  The standard refers to such arbitrary values as
"generalized Booleans," but in fact this terminology makes no
restriction on those values.  Rather, it merely specifies that they are
to be viewed, in an informal sense, as being either nil or not nil.

This situation is problematic for ACL2, which axiomatizes these
functions to return Booleans.  The problem is that because (for
efficiency and simplicity) ACL2 makes very direct use of compiled
Common Lisp functions to support the execution of its functions, there
is in principle a potential for unsoundness due to these "generalized
Booleans."  For example, ACL2's equal function is defined to be Common
Lisp's equal.  Hence if in Common Lisp the form (equal 3 3) were to
evaluate to 17, then in ACL2 we could prove (using the
:executable-counterpart of equal) (equal (equal 3 3) 17).  However,
ACL2 can also prove (equal (equal x x) t), and these two terms together
are contradictory, since they imply (instantiating x in the second term
by 3) that (equal 3 3) is both equal to 17 and to t.

To make matters worse, the standard allows (equal 3 3) to evaluate to
_different_ non-nil values every time.  That is:  equal need not even
be a function!

Fortunately, no existing Lisp implementation takes advantage of the
flexibility to have (most of) its predicates return generalized
Booleans, as far as we know.  We may implement appropriate safeguards
in future releases of ACL2, in analogy to (indeed, probably extending)
the existing safeguards by way of guards (see GUARD).  For now,
we'll sleep a bit better knowing that we have been up-front about this
potential problem.

The following list of functions contains all those that are defined in
Common Lisp to return generalized Booleans but are assumed by ACL2 to
return Booleans.  In addition, the functions acl2-numberp and
complex-rationalp are directly defined in terms of respective Common
Lisp functions numberp and complexp.

     /=
     <
     =
     alpha-char-p
     atom
     char-equal
     char<
     char<=
     char>
     char>=
     characterp
     consp
     digit-char-p
     endp
     eq
     eql
     equal
     evenp
     integerp
     keywordp
     listp
     logbitp
     logtest
     lower-case-p
     minusp
     oddp
     plusp
     rationalp
     standard-char-p
     string-equal
     string<
     string<=
     string>
     string>=
     stringp
     subsetp
     symbolp
     upper-case-p
     zerop

COMPUTED-HINTS    computing advice to the theorem proving process

     General Form of :hints:
     (hint1 hint2 ... hintk)

Each element, hinti, must be either a common hint or a computed hint.

A common hint is of the form

     (goal-spec :key1 val1 ... :keyn valn)

where goal-spec is as specified in goal-spec and each :keyi and vali is
as specified in hints.  Among the "common hints" we include both the
primitive hints and user-defined custom keyword hints (see
CUSTOM-KEYWORD-HINTS).

A computed hint may be a function symbol, fn, of three, four or seven
arguments.  Otherwise, a computed hint is a term with the following
properties:

(a) the only free variables allowed in the term are ID, CLAUSE, WORLD,
STABLE-UNDER-SIMPLIFICATIONP, HIST, PSPV, CTX, and STATE;

(b) the output signature of the term is either (MV * * STATE), which is
to be treated as an error triple (see below), or is *, denoting a single
non-stobj value; and

(c) in the former case of (b) above, the term is single-threaded in
STATE.

If a computed hint is a function symbol fn, whose arity n is therefore
three, four, or seven, then it is treated as the term resulting from
applying that fn to the first n variables shown in (a) above.  Notice
that it must then return a single non-stobj value, not an error triple,
since state is not one of the first seven variables shown in (a).

Note: Error triples are an ACL2 idiom for implementing "errors"; see
ERROR-TRIPLES.  If a computation returns (mv erp val state) in a
context in which ACL2 is respecting the error triple convention (see
LD-ERROR-TRIPLES and see LD-ERROR-ACTION), then an
error is deemed to have occurred if erp is non-nil.  The computation is
expected to have printed an appropriate error message to state and
further computation is aborted.  On the other hand, if a computation
returns an error triple in which erp is nil, then "value" of the
computation is taken to be the second component, val, of the triple
(along with the possibly modified state), and computation continues.
For more information about programming with error triples, see
PROGRAMMING-WITH-STATE.

The function symbol cases are treated as abbreviations of the term (fn
ID CLAUSE WORLD), (fn ID CLAUSE WORLD STABLE-UNDER-SIMPLIFICATIONP), or
(fn ID CLAUSE WORLD STABLE-UNDER-SIMPLIFICATIONP HIST PSPV CTX) as
appropriate for the arity of fn.  (Note that this tells you which
argument of fn is which.)  Moreover, in these cases the value returned
must be a single ordinary (non-stobj) value, not an error triple.  In
the discussion below we assume all computed hints are of the term form.
Indeed, we almost assume all computed hints are of the 3 and 4 argument
forms.  We only comment briefly on the 7 argument form in
using-computed-hints-8.

The semantics of a computed hint term is as follows.  On every subgoal,
the term is evaluated in an environment in which the variables
mentioned in (a) above are bound to context-sensitive values explained
below.  Either the computed hint signals an error, in which the proof
attempt aborts, or else it returns a value, val and a new state, state.
Any changes to those parts of state that affect logical soundness are
undone; more specifically, the values of symbols (sometimes called
"state global variables") in the list *protected-system-state-globals*
in the global table of the state (see STATE) are restored when
changed during evaluation.  The value, val, of a non-erroneous computed
hint calculation is either nil, which means the computed hint did not
apply to the subgoal in question, or it is an alternating list of :keyi
vali pairs as specified in hints.  With one exception, those new hints
are applied to the given subgoal as though the user had typed them
explicitly.

The exception is that the first keyword in the returned val is allowed
to be :COMPUTED-HINT-REPLACEMENT.  Its value should be nil, t, or a
list of terms.  If this keyword is not present, the default value of nil
is provided.  We explain :COMPUTED-HINT-REPLACEMENT below.

The evaluation of a hint term is done with guard checking turned off
(see SET-GUARD-CHECKING); e.g., the form (car 23) in a computed
hint returns nil as per the axioms.

When a non-nil value is returned, the keyword/value pairs (other than
the optional :COMPUTED-HINT-REPLACEMENT) are used as the hint for the
subgoal in question.  Thus, your job as the programmer of computed
hints is either to cause an error, typically by invoking er, or to
return a non-erroneous value triple whose value is the list of keys and
values you would have typed had you supplied a common hint for the
subgoal. (In particular, any theory expressions in it are evaluated
with respect to the global current-theory, not whatever theory is
active at the subgoal in question.)  If the generated list of keywords
and values is illegal, an error will be signaled and the proof attempt
will be aborted.

The purpose of the :COMPUTED-HINT-REPLACEMENT keyword and its value,
chr, is to change the list of hints.  If chr is nil, then the hint
which was applied is removed from the list of hints that is passed down
to the children of the subgoal in question.  This is the default.  If
chr is t, then the hint is left in the list of hints.  This means that
the same hint may act on the children of the subgoal.  Otherwise, chr
must be a list of terms, each of which is treated as a computed hint.
The hint which was applied is deleted from the list of hints and the
hints in chr are added to the list of hints passed to the children of
the subgoal.  The ability to compute new hints and pass them down
allows strange and wonderful behavior.

For these purposes, the goals produced by induction and the top-level
goals of forcing rounds are not considered children; all original hints
are available to them.

Only the first hint applicable to a goal, as specified in the
user-supplied list of :hints followed by the default-hints-table, will
be applied to that goal.  (For an advanced exception, see
OVERRIDE-HINTS.)

It remains only to describe the bindings of the free variables.

Suppose the theorem prover is working on some clause, clause, named by
some goal-spec, e.g., "Subgoal *1/2"'" in some logical world, world.
Corresponding to the printed goal-spec is an internal data structure
called a "clause identifier" id.  See CLAUSE-IDENTIFIER.

In the case of a common hint, the hint applies if the goal-spec of the
hint is the same as the goal-spec of the clause in question.

In the case of a computed hint, the variable ID is bound to the clause
id, the variable CLAUSE is bound to the (translated form of the) clause,
and the variable WORLD is bound to the current ACL2 world.  The variable
STABLE-UNDER-SIMPLIFICATIONP is bound to t or nil.  It is bound to t
only if the clause is known to be stable under simplification.  That
is, the simplifier has been applied to the clause and did not change it.
Such a clause is sometimes known as a "simplification checkpoint."  It
is frequently useful to inject hints (e.g., to enable a rule or provide
a :use hint) only when the goal in question has stabilized.  If a hint
is provided, the processing of the clause starts over with
simplification.

As for CTX and STATE, they are provided so that you can pass them to
the er macro to print error messages.  We recommend not writing
computed hints that otherwise change STATE!

The remaining variables, HIST and PSPV are not documented yet.  Only
users familiar with the internals of ACL2 are likely to need them or
understand their values.

For some instruction about how to use computed hints, see
USING-COMPUTED-HINTS.

CONSTRAINT    restrictions on certain functions introduced in encapsulate events

Suppose that a given theorem, thm, is to be functionally instantiated
using a given functional substitution, alist.  (See
LEMMA-INSTANCE, or for an example, see
FUNCTIONAL-INSTANTIATION-EXAMPLE.)  What is the set of proof
obligations generated?  It is the set obtained by applying alist to all
terms, tm, such that (a) tm mentions some function symbol in the domain
of alist, and (b) either (i) tm arises from the "constraint" on a
function symbol ancestral in thm or in some defaxiom or (ii) tm is the
body of a defaxiom.  Here, a function symbol is "ancestral" in thm if
either it occurs in thm, or it occurs in the definition of some
function symbol that occurs in thm, and so on.

The remainder of this note explains what we mean by "constraint" in the
words above.

In a certain sense, function symbols are introduced in essentially two
ways.  The most common way is to use defun (or when there is mutual
recursion, mutual-recursion or defuns).  There is also a mechanism for
introducing "witness functions"; see DEFCHOOSE.  The
documentation for these events describes the axioms they introduce,
which we will call here their "definitional axioms."  These
definitional axioms are generally the constraints on the function
symbols that these axioms introduce.

However, when a function symbol is introduced in the scope of an
encapsulate event, its constraints may differ from the definitional
axioms introduced for it.  For example, suppose that a function's
definition is local to the encapsulate; that is, suppose the function is
introduced in the signature of the encapsulate.  Then its constraints
include, at the least, those non-local theorems and definitions in the
encapsulate that mention the function symbol.

Actually, it will follow from the discussion below that if the
signature is empty for an encapsulate, then the constraint on each of
its new function symbols is exactly the definitional axiom introduced
for it.  Intuitively, we view such encapsulates just as we view
include-book events.  But the general case, where the signature is not
empty, is more complicated.

In the discussion that follows we describe in detail exactly which
constraints are associated with which function symbols that are
introduced in the scope of an encapsulate event.  In order to simplify
the exposition we make two cuts at it.  In the first cut we present an
over-simplified explanation that nevertheless captures the main ideas.
In the second cut we complete our explanation by explaining how we view
certain events as being "lifted" out of the encapsulate, resulting in a
possibly smaller encapsulate, which becomes the target of the algorithm
described in the first cut.

At the end of this note we present an example showing why a more naive
approach is unsound.

Finally, before we start our "first cut," we note that any information
you want "exported" outside an encapsulate event must be there as an
explicit definition or theorem.  For example, even if a function foo has
output type (mv t t) in its signature, the system will not know
(true-listp (foo x)) merely on account of this information.  Thus, if
you are using functions like foo (constrained mv functions), then you
may find it useful to prove (inside the encapsulate, to be exported) a
:type-prescription rule for the constrained function, for example, the
:type-prescription rule (true-listp (foo x)).

_First cut at constraint-assigning algorithm._  Quite simply, the
formulas introduced in the scope of an encapsulate are conjoined, and
each function symbol introduced by the encapsulate is assigned that
conjunction as its constraint.

Clearly this is a rather severe algorithm.  Let us consider two possible
optimizations in an informal manner before presenting our second cut.

Consider the (rather artificial) event below.  The function before1 does
not refer at all, even indirectly, to the locally-introduced function
sig-fn, so it is unfortunate to saddle it with constraints about sig-fn.

     (encapsulate
      (((sig-fn *) => *))

      (defun before1 (x)
        (if (consp x)
            (before1 (cdr x))
          x))

      (local (defun sig-fn (x) (cons x x)))

      (defthm sig-fn-prop
        (consp (sig-fn x)))
      )

We would like to imagine moving the definition of before1 to just in
front of this encapsulate, as follows.

     (defun before1 (x)
       (if (consp x)
           (before1 (cdr x))
         x))

     (encapsulate
      (((sig-fn *) => *))

      (local (defun sig-fn (x) (cons x x)))

      (defthm sig-fn-prop
        (consp (sig-fn x)))
      )

Thus, we will only assign the constraint (consp (sig-fn x)), from the
theorem sig-fn-prop, to the function sig-fn, not to the function
before1.

More generally, suppose an event in an encapsulate event does not
mention any function symbol in the signature of the encapsulate, nor
any function symbol that mentions any such function symbol, and so on.
(We might say that no function symbol from the signature is an
"ancestor" of any function symbol occurring in the event.)  Then we
imagine moving the event, so that it appears in front of the
encapsulate.  We don't actually move it, but we pretend we do when it
comes time to assign constraints.  Thus, such definitions only
introduce definitional axioms as the constraints on the function
symbols being defined.  In the example above, the event sig-fn-prop
introduces no constraints on function before1.

Once this first optimization is performed, we have in mind a set of
"constrained functions."  These are the functions introduced in the
encapsulate that would remain after moving some of them in front, as
indicated above.  Consider the collection of all formulas introduced by
the encapsulate, except the definitional axioms, that mention these
constrained functions.  So for example, in the event below, no such
formula mentions the function symbol after1.

     (encapsulate
      (((sig-fn *) => *))

      (local (defun sig-fn (x) (cons x x)))

      (defthm sig-fn-prop
        (consp (sig-fn x)))

      (defun after1 (x)
        (sig-fn x))
      )

We can see that there is really no harm in imagining that we move the
definition of after1 out of the encapsulate, to just after the
encapsulate.

Many subtle aspects of this rearrangement process have been omitted.
For example, suppose the function fn uses sig-fn, the latter being a
function in the signature of the encapsulation.  Suppose a formula about
fn is proved in the encapsulation.  Then from the discussion above fn
is among the constrained functions of the encapsulate: it cannot be
moved before the encapsulate and it cannot be moved after the
encapsulation.  But why is fn constrained?  The reason is that the
theorem proved about fn may impose or express constraints on sig-fn.
That is, the theorem proved about fn may depend upon properties of the
witness used for sig-fn.  Here is a simple example:

     (encapsulate
      (((sig-fn *) => *))

      (local (defun sig-fn (x) (declare (ignore x)) 0))

      (defun fn (lst)
        (if (endp lst)
            t
            (and (integerp (sig-fn (car lst)))
                 (fn (cdr lst)))))

      (defthm fn-always-true
        (fn lst)))

In this example, there are no defthm events that mention sig-fn
explicitly.  One might therefore conclude that it is completely
unconstrained.  But the witness we chose for it always returns an
integer.  The function fn uses sig-fn and we prove that fn always
returns true.  Of course, the proof of this theorem depends upon the
properties of the witness for sig-fn, even though those properties were
not explicitly "called out" in theorems proved about sig-fn.  It would
be unsound to move fn-always-true after the encapsulate.  It would also
be unsound to constrain sig-fn to satisfy just fn-always-true without
including in the constraint the relation between sig-fn and fn.  Hence
both sig-fn and fn are constrained by this encapsulation and the
constraint imposed on each is the same and states the relation between
the two as characterized by the equation defining fn as well as the
property that fn always returns true.  Suppose, later, one proved a
theorem about sig-fn and wished to functionally instantiate it.  Then
one must also functionally instantiate fn, even if it is not involved
in the theorem, because it is only through fn that sig-fn inherits its
constrained properties.

This is a pathological example that illustrate a trap into which one may
easily fall: rather than identify the key properties of the constrained
function the user has foreshadowed its intended application and
constrained those notions.  Clearly, the user wishing to introduce the
sig-fn above would be well-advised to use the following instead:

     (encapsulate
      (((sig-fn *) => *))
      (local (defun sig-fn (x) (declare (ignore x)) 0))
      (defthm integerp-sig-fn
        (integerp (sig-fn x))))

     (defun fn (lst)
       (if (endp lst)
           t
         (and (integerp (sig-fn (car lst)))
              (fn (cdr lst)))))

     (defthm fn-always-true
        (fn lst)))

Note that sig-fn is constrained merely to be an integer.  It is the only
constrained function.  Now fn is introduced after the encapsulation, as
a simple function that uses sig-fn.  We prove that fn always returns
true, but this fact does not constrain sig-fn.  Future uses of sig-fn
do not have to consider fn at all.

Sometimes it is necessary to introduce a function such as fn within the
encapsulate merely to state the key properties of the undefined function
sig-fn.  But that is unusual and the user should understand that both
functions are being constrained.

Another subtle aspect of encapsulation that has been brushed over so
far has to do with exactly how functions defined within the
encapsulation use the signature functions.  For example, above we say
"Consider the collection of all formulas introduced by the encapsulate,
_except the definitional axioms_, that mention these constrained
functions."  We seem to suggest that a definitional axiom which
mentions a constrained function can be moved out of the encapsulation
and considered part of the "post-encapsulation" extension of the
logical world, if the defined function is not used in any
non-definitional formula proved in the encapsulation.  For example, in
the encapsulation above that constrained sig-fn and introduced fn
within the encapsulation, fn was constrained because we proved the
formula fn-always-true within the encapsulation.  Had we not proved
fn-always-true within the encapsulation, fn could have been moved after
the encapsulation.  But this suggests an unsound rule because whether
such a function can be moved after the encapsulate depend on whether
its _admission_ used properties of the witnesses!  In particular, we
say a function is "subversive" if any of its governing tests or the
actuals in any recursive call involve a function in which the signature
functions are ancestral.  See SUBVERSIVE-RECURSIONS.

(Aside: The definition of fn in the first enapsulation above that
defines fn, i.e., the encapsulation with fn-always-true inside, is
subversive because the call of the macro AND expands to a call of IF
that governs a recursive call of fn, in this case:

     (defun fn (lst)
       (if (endp lst)
           t
           (if (integerp (sig-fn (car lst)))
               (fn (cdr lst))
             nil))).

If we switch the order of conjuncts in fn, then the definition of fn is
no longer subversive, but it still "infects" the constraint generated
for the encapsulation, hence for sig-fn, because fn-always-true blocks
the definition of fn from being moved back (to after the
encapsulation).  If we both switch the order of conjuncts and drop
fn-always-true from the encapsulation, then the definition of fn is in
essence moved back to after the encapsulation, and the constraint for
sig-fn no longer includes the definition of fn.  End of aside.)

Another aspect we have not discussed is what happens to nested
encapsulations when each introduces constrained functions.  We say an
encapsulate event is "trivial" if it introduces no constrained
functions, i.e., if its signatures is nil.  Trivial encapsulations are
just a way to wrap up a collection of events into a single event.

From the foregoing discussion we see we are interested in exactly how
we can "rearrange" the events in a non-trivial encapsulation - moving
some "before" the encapsulation and others "after" the encapsulation.
We are also interested in which functions introduced by the
encapsulation are "constrained" and what the "constraints" on each are.
We may summarize the observations above as follows, after which we
conclude with a more elaborate example.

_Second cut at constraint-assigning algorithm._  First, we focus only on
non-trivial encapsulations that neither contain nor are contained in
non-trivial encapsulations.  (Nested non-trivial encapsulations are not
rearranged at all: do not put anything in such a nest unless you mean
for it to become part of the constraints generated.)  Second, in what
follows we only consider the non-local events of such an encapsulate,
assuming that they satisfy the restriction of using no locally defined
function symbols other than the signature functions.  Given such an
encapsulate event, move, to just in front of it and in the same order,
all definitions and theorems for which none of the signature functions
is ancestral.  Now collect up all formulas (theorems) introduced in the
encapsulate other than definitional axioms.  Add to this set any of
those definitional equations that is either subversive or defines a
function used in a formula in the set.  The conjunction of the
resulting set of formulas is called the "constraint" and the set of all
the signature functions of the encapsulate together with all function
symbols defined in the encapsulate and mentioned in the constraint is
called the "constrained functions."  Assign the constraint to each of
the constrained functions.  Move, to just after the encapsulate, the
definitions of all function symbols defined in the encapsulate that
have been omitted from the constraint.

Implementation note.  In the implementation we do not actually move
events, but we create constraints that pretend that we did.

Here is an example illustrating our constraint-assigning algorithm.  It
builds on the preceding examples.

     (encapsulate
      (((sig-fn *) => *))

      (defun before1 (x)
        (if (consp x)
            (before1 (cdr x))
          x))

      (local (defun sig-fn (x) (cons x x)))

      (defthm sig-fn-prop
        (consp (sig-fn x)))

      (defun during (x)
        (if (consp x)
            x
          (cons (car (sig-fn x))
                17)))

      (defun before2 (x)
        (before1 x))

      (defthm before2-prop
        (atom (before2 x)))

      (defthm during-prop
        (implies (and (atom x)
                      (before2 x))
                 (equal (car (during x))
                        (car (sig-fn x)))))

      (defun after1 (x)
        (sig-fn x))

      (defchoose after2 (x) (u)
        (and (< u x) (during x)))
      )

Only the functions sig-fn and during receive extra constraints.  The
functions before1 and before2 are viewed as moving in front of the
encapsulate, as is the theorem before2-prop.  The functions after1 and
after2 are viewed as being moved past the encapsulate.  The
implementation reports the following.

     In addition to SIG-FN, we export AFTER2, AFTER1, BEFORE2, DURING and
     BEFORE1.

     The following constraint is associated with both of the functions DURING and
     SIG-FN:

     (AND (EQUAL (DURING X)
                 (IF (CONSP X)
                     X (CONS (CAR (SIG-FN X)) 17)))
          (CONSP (SIG-FN X))
          (IMPLIES (AND (ATOM X) (BEFORE2 X))
                   (EQUAL (CAR (DURING X))
                          (CAR (SIG-FN X)))))

Notice that the formula (consp (during x)) is not a conjunct of the
constraint.  During the first pass of the encapsulate, this formula is
stored as a :type-prescription rule deduced during the definition of
the function during.  However, the rule is not exported because of a
rather subtle soundness issue.  (If you are interested in details, see
the comments in source function putprop-type-prescription-lst.)

We conclude by asking (and to a certain extent, answering) the following
question: Isn't there an approach to assigning constraints that avoids
over-constraining more simply than our "second cut" above?  Perhaps it
seems that given an encapsulate, we should simply assign to each
locally defined function the theorems exported about that function.  If
we adopted that simple approach the events below would be admissible.

     (encapsulate
      (((foo *) => *))
      (local (defun foo (x) x))
      (defun bar (x)
        (foo x))
      (defthm bar-prop
        (equal (bar x) x)
        :rule-classes nil))

     (defthm foo-id
       (equal (foo x) x)
       :hints (("Goal" :use bar-prop)))

     ; The following event is not admissible in ACL2.

     (defthm ouch!
       nil
       :rule-classes nil
       :hints
       (("Goal" :use
         ((:functional-instance foo-id
                                (foo (lambda (x) (cons x x))))))))

Under the simple approach we have in mind, bar is constrained to satisfy
both its definition and bar-prop because bar mentions a function
declared in the signature list of the encapsulation.  In fact, bar is
so-constrained in the ACL2 semantics of encapsulation and the first two
events above (the encapsulate and the consequence that foo must be the
identity function) are actually admissible.  But under the simple
approach to assigning constraints, foo is unconstrained because no
theorem about it is exported.  Under that approach, ouch! is provable
because foo can be instantiated in foo-id to a function other than the
identity function.

It's tempting to think we can fix this by including definitions, not
just theorems, in constraints.  But consider the following slightly
more elaborate example.  The problem is that we need to include as a
constraint on foo not only the definition of bar, which mentions foo
explicitly, but also abc, which has foo as an ancestor.

     (encapsulate
      (((foo *) => *))
      (local (defun foo (x) x))
      (local (defthm foo-prop
               (equal (foo x) x)))
      (defun bar (x)
        (foo x))
      (defun abc (x)
        (bar x))
      (defthm abc-prop
        (equal (abc x) x)
        :rule-classes nil))

     (defthm foo-id
       (equal (foo x) x)
       :hints (("Goal" :use abc-prop)))

     ; The following event is not admissible in ACL2.

     (defthm ouch!
       nil
       :rule-classes nil
       :hints
       (("Goal" :use
         ((:functional-instance foo-id
                                (foo (lambda (x) (cons x x)))
                                (bar (lambda (x) (cons x x))))))))

COPYRIGHT    ACL2 copyright, license, sponsorship

ACL2 Version 6.0 - A Computational Logic for Applicative Common Lisp
Copyright (C) 2012, Regents of the University of Texas

This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright (C)
1997 Computational Logic, Inc.  See the documentation topic NOTE-2-0.

This program is free software; you can redistribute it and/or modify it
under the terms of the LICENSE file distributed with ACL2.

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 LICENSE
for more details.

Written by:  Matt Kaufmann               and J Strother Moore email:
  Kaufmann@cs.utexas.edu      and Moore@cs.utexas.edu Department of
Computer Science University of Texas at Austin Austin, TX 78701 U.S.A.

Please also see ACKNOWLEDGMENTS.

COROLLARY    the corollary formula of a rune

This is a low-level system function at the present time.  See
PR and see PR! instead.  Also see RULE-CLASSES for
the use of the symbol :corollary in specifying a rule class.

CURRENT-PACKAGE    the package used for reading and printing

Current-package is an ld special (see LD).  The accessor is
(current-package state) and the updater is (set-current-package val
state), or more conventionally, (in-package val).  The value of
current-package is actually the string that names the package.  (Common
Lisp's "package" objects do not exist in ACL2.)  The current package
must be known to ACL2, i.e., it must be one of the initial packages or
a package defined with defpkg by the user.

When printing symbols, the package prefix is displayed if it is not the
current-package and may be optionally displayed otherwise.  Thus, if
current-package is "ACL2" then the symbol 'ACL2::SYMB may be printed as
SYMB or ACL2::SYMB, while 'MY-PKG::SYMB must be printed as
MY-PKG::SYMB.  But if current-package is "MY-PKG" then the former
symbol must be printed as ACL2::SYMB while the latter may be printed as
SYMB.

In Common Lisp, current-package also affects how objects are read from
character streams.  Roughly speaking, read and print are inverses if
the current-package is fixed, so reading from a stream produced by
printing an object must produce an equal object.

In ACL2, the situation is more complicated because we never read
objects from character streams, we only read them from object "streams"
(channels).  Logically speaking, the objects in such a channel are
fixed regardless of the setting of current-package.  However, our host
file systems do not support the idea of Lisp object files and instead
only support character files.  So when you open an object input channel
to a given (character file) we must somehow convert it to a list of
ACL2 objects.  This is done by a deus ex machina ("a person or thing
that appears or is introduced suddenly and unexpectedly and provides a
contrived solution to an apparently insoluble difficulty," Webster's
Ninth New Collegiate Dictionary).  Roughly speaking, the deus ex
machina determines what sequence of calls to read-object will occur in
the future and what the current-package will be during each of those
calls, and then produces a channel containing the sequence of objects
produced by an analogous sequence of Common Lisp reads with
*current-package* bound appropriately for each.

A simple rule suffices to make sane file io possible:  before you read
an object from an object channel to a file created by printing to a
character channel, make sure the current-package at read-time is the
same as it was at print-time.

CUSTOM-KEYWORD-HINTS    user-defined hints

See ADD-CUSTOM-KEYWORD-HINT for a discussion of how advanced
users can define their own hint keywords.  For examples, see the
community books directory books/hints/, in particular basic-tests.lisp.

DEFAULT-BACKCHAIN-LIMIT    specifying the backchain limit for a rule

See BACKCHAIN-LIMIT.

The initial value is (nil nil).  To inspect the current value (as
explained elsewhere; see BACKCHAIN-LIMIT):

     (default-backchain-limit wrld :ts) ; for type-set reasoning
     (default-backchain-limit wrld :rewrite) ; for rewriting

DEFAULT-DEFUN-MODE    the default defun-mode of defun'd functions

When a defun is processed and no :mode xarg is supplied, the function
default-defun-mode is used.  To find the default defun-mode of the
current ACL2 world, type (default-defun-mode (w state)).  See
DEFUN-MODE for a discussion of defun-modes.  To change the default
defun-mode of the ACL2 world, type one of the keywords :program or
:logic.

The default ACL2 prompt displays the current default defun-mode by
showing the character p for :program mode, and omitting it for :logic
mode; see DEFAULT-PRINT-PROMPT.  The default defun-mode may be
changed using the keyword commands :program and :logic, which are
equivalent to the commands (program) and (logic).  Each of these names
is documented separately:  see PROGRAM and see LOGIC.
The default defun-mode is stored in the table acl2-defaults-table and
hence may also be changed by a table command.  See TABLE and
also see ACL2-DEFAULTS-TABLE.  Both mode-changing commands are
events.

While events that change the default defun-mode are permitted within an
encapsulate or the text of a book, their effects are local in scope to
the duration of the encapsulation or inclusion.  For example, if the
default defun-mode is :logic and a book is included that contains the
event (program), then subsequent events within the book are processed
with the default defun-mode :program; but when the include-book event
completes, the default defun-mode will still be :logic.  Commands that
change the default defun-mode are not permitted inside local forms.

DEFAULT-HINTS    a list of hints added to every proof attempt

     Examples:
     ACL2 !>(default-hints (w state))
     ((computed-hint-1 clause)
      (computed-hint-2 clause stable-under-simplificationp))

The value returned by this function is added to the right of the :hints
argument of every defthm and thm command, and to hints provided to
defuns as well (:hints, :guard-hints, and (for ACL2(r)) :std-hints).

See SET-DEFAULT-HINTS for a more general discussion.  Advanced
users only: see OVERRIDE-HINTS for an advanced variant of
default hints that are not superseded by :hints arguments.

DEFAULT-PRINT-PROMPT    the default prompt printed by ld

     Example prompt:
     ACL2 p!s>

The prompt printed by ACL2 displays the current package, followed by a
space, followed by zero or more of the three characters as specified
below, followed by the character > printed one or more times,
reflecting the number of recursive calls of ld.  The three characters
in the middle are as follows:

     p     ; when (default-defun-mode (w state)) is :program
     !     ; when guard checking is on
     s     ; when (ld-skip-proofsp state) is t

See DEFAULT-DEFUN-MODE, see SET-GUARD-CHECKING, and see
LD-SKIP-PROOFSP.

Also see LD-PROMPT to see how to install your own prompt.

Here are some examples with ld-skip-proofsp nil.

     ACL2 !>    ; logic mode with guard checking on
     ACL2 >     ; logic mode with guard checking off
     ACL2 p!>   ; program mode with guard checking on
     ACL2 p>    ; program mode with guard checking off

Here are some examples with default-defun-mode of :logic.

     ACL2 >     ; guard checking off, ld-skip-proofsp nil
     ACL2 s>    ; guard checking off, ld-skip-proofsp t
     ACL2 !>    ; guard checking on, ld-skip-proofsp nil
     ACL2 !s>   ; guard checking on, ld-skip-proofsp t

Finally, here is the prompt in raw mode (see SET-RAW-MODE),
regardless of the settings above:

     ACL2 P>

DEFAULT-RULER-EXTENDERS    the default ruler-extenders for defun'd functions

When a defun is processed and no :ruler-extenders xarg is supplied, the
function default-ruler-extenders is used to obtain the current
ruler-extenders; see RULER-EXTENDERS.  To find the default
ruler-extenders of the current ACL2 world, type
(default-ruler-extenders (w state)).

While events that change the default ruler-extenders are permitted
within an encapsulate or the text of a book, their effects are local in
scope to the duration of the encapsulation or inclusion.  See
DEFAULT-DEFUN-MODE for an analogous discussion for defun-modes.

DEFUN-MODE    determines whether a function definition is a logical act

Two "defun-modes" are supported, :program and :logic.  Roughly
speaking, :program mode allows you to prototype a function for
execution without any proof burdens, while :logic mode allows you to
add a new definitional axiom to the logic.  The system comes up in
:logic mode.  Execution of functions whose defun-mode is :program may
render ACL2 unsound!  See DEFUN-MODE-CAVEAT.

Note that calls of local and of many events are skipped in :program
mode; see PROGRAM.

When you define a function in the ACL2 logic, that function can be run
on concrete data.  But it is also possible to reason deductively about
the function because each definition extends the underlying logic with
a definitional axiom.  To ensure that the logic is sound after the
addition of this axiom, certain restrictions have to be met, namely
that the recursion terminates.  This can be quite challenging.

Because ACL2 is a programming language, you often may wish simply to
program in ACL2.  For example, you may wish to define your system and
test it, without any logical burden.  Or, you may wish to define
"utility" functions -- functions that are executed to help manage the
task of building your system but functions whose logical properties are
of no immediate concern.  Such functions might be used to generate test
data or help interpret the results of tests.  They might create files
or explore the ACL2 database.  The termination arguments for such
functions are an unnecessary burden provided no axioms about the
functions are ever used in deductions.

Thus, ACL2 introduces the idea of the "defun-mode" of a function.  The
:mode keyword of defun's declare xarg allows you to specify the
defun-mode of a given definition.  If no :mode keyword is supplied, the
default defun-mode is used; see DEFAULT-DEFUN-MODE.

There are two defun-modes, each of which is written as a keyword:

:program -- logically undefined but executable outside deductive
contexts.

:logic -- axiomatically defined as per the ACL2 definitional principle.

It is possible to change the defun-mode of a function from :program to
:logic.  We discuss this below.

We think of functions having :program mode as "dangerous" functions,
while functions having :logic mode are "safe."  The only requirement
enforced on :program mode functions is the syntactic one:  each
definition must be well-formed ACL2.  Naively speaking, if a :program
mode function fails to terminate then no harm is done because no axiom
is added (so inconsistency is avoided) and some invocations of the
function may simply never return.  This simplistic justification of
:program mode execution is faulty because it ignores the damage that
might be caused by "mis-guarded" functions.  See
DEFUN-MODE-CAVEAT.

We therefore implicitly describe an imagined implementation of
defun-modes that is safe and, we think, effective.  But please see
DEFUN-MODE-CAVEAT.

The default defun-mode is :logic.  This means that when you defun a
function the system will try to prove termination.  If you wish to
introduce a function of a different defun-mode use the :mode xargs
keyword.  Below we show fact introduced as a function in :program mode.

     (defun fact (n)
       (declare (xargs :mode :program))
       (if (or (not (integerp n)) (= n 0))
           1
         (* n (fact (1- n)))))

No axiom is added to the logic as a result of this definition.  By
introducing fact in :program mode we avoid the burden of a termination
proof, while still having the option of executing the function.  For
example, you can type

     ACL2 !>(fact 3)

and get the answer 6.  If you type (fact -1) you will get a hard lisp
error due to "infinite recursion."

However, the ACL2 theorem prover knows no axioms about fact.  In
particular, if the term (fact 3) arises in a proof, the theorem prover
is unable to deduce that it is 6.  From the perspective of the theorem
prover it is as though fact were an undefined function symbol of arity
1.  Thus, modulo certain important issues (see
DEFUN-MODE-CAVEAT), the introduction of this function in :program
mode does not imperil the soundness of the system -- despite the fact
that the termination argument for fact was omitted -- because nothing
of interest can be proved about fact.  Indeed, we do not allow fact to
be used in logical contexts such as conjectures submitted for proof.

It is possible to convert a function from :program mode to :logic mode
at the cost of proving that it is admissible.  This can be done by
invoking

     (verify-termination fact)

which is equivalent to submitting the defun of fact, again, but in
:logic mode.

     (defun fact (n)
       (declare (xargs :mode :logic))
       (if (or (not (integerp n)) (= n 0))
           1
         (* n (fact (1- n)))))

This particular event will fail because the termination argument
requires that n be nonnegative.  A repaired defun, for example with =
replaced by <=, will succeed, and an axiom about fact will henceforth
be available.

Technically, verify-termination submits a redefinition of the :program
mode function.  This is permitted, even when ld-redefinition-action is
nil, because the new definition is identical to the old (except for its
:mode and, possibly, other non-logical properties).

See GUARD for a discussion of how to restrict the execution of
functions.  Guards may be "verified" for functions in :logic mode; see
VERIFY-GUARDS.

DEFUNS    an alternative to mutual-recursion

     Example:
     (DEFUNS
      (evenlp (x)
        (if (consp x) (oddlp (cdr x)) t))
      (oddlp (x)
        (if (consp x) (evenlp (cdr x)) nil)))

     General Form:
     (DEFUNS defuns-tuple1 ... defuns-tuplen)

is equivalent to

     (MUTUAL-RECURSION
       (DEFUN . defuns-tuple1)
       ...
       (DEFUN . defuns-tuplen))

In fact, defuns is the more primitive of the two and mutual-recursion
is just a macro that expands to a call of defun after stripping off the
defun at the car of each argument to mutual-recursion.  We provide and
use mutual-recursion rather than defuns because by leaving the defuns
in place, mutual-recursion forms can be processed by the Emacs tags
program.  See MUTUAL-RECURSION.

DISABLE-FORCING    to disallow forced case-splits

     General Form:
     ACL2 !>:disable-forcing   ; disallow forced case splits

See FORCE and see CASE-SPLIT for a discussion of forced
case splits, which are inhibited by this command.

Disable-forcing is actually a macro that disables the executable
counterpart of the function symbol force; see FORCE.  When you
want to use hints to turn off forced case splits, use a form such as
one of the following (these are equivalent).

     :in-theory (disable (:executable-counterpart force))
     :in-theory (disable (force))

DISABLE-IMMEDIATE-FORCE-MODEP    forced hypotheses are not attacked immediately

     General Form:
     ACL2 !>:disable-immediate-force-modep

This event causes ACL2 to delay forced hypotheses to the next forcing
round, rather than attacking them immediately.  See
IMMEDIATE-FORCE-MODEP.  Or for more basic information, first see
FORCE for a discussion of forced case splits.

Disable-immediate-force-modep is a macro that disables the executable
counterpart of the function symbol immediate-force-modep.  When you
want to disable this mode in hints, use a form such as one of the
following (these are equivalent).

     :in-theory (disable (:executable-counterpart immediate-force-modep))
     :in-theory (disable (immediate-force-modep))

DISABLEDP    determine whether a given name or rune is disabled

     Examples:

     :disabledp foo   ; returns a list of all disabled runes whose base
                      ; symbol is foo (see RUNE)
     (disabledp 'foo) ; same as above (i.e., :disabledp foo)
     :disabledp (:rewrite bar . 1) ; returns t if the indicated rune is
                                   ; disabled, else nil
     (disabledp (:rewrite bar . 1)); same as immediately above

Also see PR, which gives much more information about the rules
associated with a given event.

Disabledp takes one argument, an event name (see EVENTS) other
than nil or a rune.  In the former case it returns the list of disabled
runes associated with that name, in the sense that the rune's "base
symbol" is that name (see RUNE) or, if the event named is a
defmacro event, then the list of disabled runes associated with the
function corresponding to that macro name, if any (see
MACRO-ALIASES-TABLE).  In the latter case, where the argument is a
rune, disabledp returns t if the rune is disabled, and nil otherwise.

DO-NOT    hints keyword :DO-NOT

See HINTS.

DO-NOT-INDUCT    hints keyword :DO-NOT-INDUCT

See HINTS.

DOUBLE-REWRITE    cause a term to be rewritten twice

Logically, double-rewrite is the identity function: (double-rewrite x)
is equal to x.  However, the ACL2 rewriter treats calls of
double-rewrite in the following special manner.  When it encounters a
term (double-rewrite u), it first rewrites u in the current context,
and then the rewriter rewrites the result.

Such double-rewriting is rarely necessary, but it can be useful when
rewriting under non-trivial equivalence relations (see
EQUIVALENCE).  The following example will illustrate the issue.

     ; Define an equivalence relation.
     (defun my-equiv (x y)
       (equal x y))
     (defequiv my-equiv)

     ; Define a unary function whose argument is preserved by my-equiv.
     (defun foo (x)
       (declare (ignore x))
       t)
     (defcong my-equiv equal (foo x) 1)

     ; Define some other unary functions.
     (defun g (x) x)
     (defun h1 (x) x)
     (defun h2 (x) x)

     ; Prove some lemmas and then disable the functions above.
     (defthm lemma-1
       (my-equiv (h1 x) (h2 x)))
     (defthm lemma-2
       (foo (h2 x)))
     (defthm lemma-3
       (implies (foo x)
                (equal (g x) x)))
     (in-theory (union-theories (theory 'minimal-theory)
                                '(lemma-1 lemma-2 lemma-3
                                  my-equiv-implies-equal-foo-1)))

     ; Attempt to prove a simple theorem that follows ``obviously'' from the
     ; events above.
     (thm (equal (g (h1 a)) (h1 a)))

We might expect the proof of this final thm to succeed by the following
reasoning.  It is immediate from lemma-3 provided we can establish (foo
(h1 a)).  By the defcong event above, we know that (foo (h1 a)) equals
(foo (h2 a)) provided (my-equiv (h1 a) (h2 a)); but this is immediate
from lemma-1.  And finally, (foo (h2 a)) is true by lemma-2.

Unfortunately, the proof fails.  But fortunately, ACL2 gives the
following useful warning when lemma-3 is submitted:

     ACL2 Warning [Double-rewrite] in ( DEFTHM LEMMA-3 ...):  In the :REWRITE
     rule generated from LEMMA-3, equivalence relation MY-EQUIV is maintained
     at one problematic occurrence of variable X in hypothesis (FOO X),
     but not at any binding occurrence of X.  Consider replacing that occurrence
     of X in this hypothesis with (DOUBLE-REWRITE X).  See :doc double-
     rewrite for more information on this issue.

We can follow the warning's advice by changing lemma-3 to the following.

     (defthm lemma-3
       (implies (foo (double-rewrite x))
                (equal (g x) x)))

With this change, the proof succeeds for the final thm above.

In practice, it should suffice for users to follow the advice given in
the "Double-rewrite" warnings, by adding calls of double-rewrite around
certain variable occurrences.  But this can cause inefficiency in large
proof efforts.  For that reason, and for completeness, it seems prudent
to explain more carefully what is going on; and that is what we do for
the remainder of this documentation topic.  Optionally, also see the
paper "Double Rewriting for Equivalential Reasoning in ACL2" by Matt
Kaufmann and J Strother Moore, in the proceedings of the 2006 ACL2
Workshop (paper is published in ACM Digital Library,
`http://portal.acm.org/toc.cfm?id=1217975').

*Suggesting congruence rules.*

Sometimes the best way to respond to a "Double-rewrite" warning may be
to prove a congruence rule.  Consider for example this rule.

     (defthm insert-sort-is-id
       (perm (insert-sort x) x))

Assuming that perm has been identified as an equivalence relation (see
DEFEQUIV), we will get the following warning.

     ACL2 Warning [Double-rewrite] in ( DEFTHM INSERT-SORT-IS-ID ...):
     In a :REWRITE rule generated from INSERT-SORT-IS-ID, equivalence relation
     PERM is maintained at one problematic occurrence of variable X in the
     right-hand side, but not at any binding occurrence of X.  Consider
     replacing that occurrence of X in the right-hand side with
     (DOUBLE-REWRITE X).  See :doc double-rewrite for more information on
     this issue.

The problem is that the second occurrence of x (the right-hand side of
the rule insert-sort-is-id) is in a context where perm is to be
maintained, yet in this example, the argument x of insert-sort on the
left-hand side of that rule is in a context where perm will not be
maintained.  This can lead one to consider the possibility that perm
could be maintained in that left-hand side occurrence of x, and if so,
to prove the following congruence rule.

     (defcong perm perm (insert-sort x) 1)

This will eliminate the above warning for insert-sort-is-id.  More
important, this defcong event would probably be useful, since it would
allow rewrite rules with equivalence relation perm to operate on the
first argument of any call of insert-sort whose context calls for
maintaining perm.

*Details on double-rewrite.*

The reader who wants these details may first wish to see
EQUIVALENCE for relevant review.

The ACL2 rewriter takes a number of contextual arguments, including the
generated equivalence relation being maintained (see
CONGRUENCE) and an association list that maps variables to terms.  We
call the latter alist the unify-subst because it is produced by unifying
(actually matching) a pattern against a current term; let us explain
this point by returning to the example above.  Consider what happens
when the rewriter is given the top-level goal of the thm above.

     (equal (g (h1 a)) (h1 a))

This rewrite is performed with the empty alist (unify-subst), and is
begun by rewriting the first argument (in that same empty unify-subst):

     (g (h1 a))

Note that the only equivalence relation being maintained at this point
is equal.  Now, the rewriter notices that the left-hand side of lemma-3,
which is (g x), matches (g (h1 a)).  The rewriter thus creates a
unify-subst binding x to (h1 a): ((x . (h1 a))).  It now attempts to
rewrite the hypothesis of lemma-3 to t under this unify-subst.

Consider what happens now if the hypothesis of lemma-3 is (foo x).  To
rewrite this hypothesis under a unify-subst of ((x . (h1 a))), it will
first rewrite x under this unify-subst.  The key observation here is
that this rewrite takes place simply by returning the value of x in the
unify-subst, namely (h1 a).  No further rewriting is done!  The
efficiency of the ACL2 rewriter depends on such caching of previous
rewriting results.

But suppose that, instead, the hypothesis of lemma-3 is (foo
(double-rewrite x)).  As before, the rewriter dives to the first
argument of this call of foo.  But this time the rewriter sees the call
(double-rewrite x), which it handles as follows.  First, x is rewritten
as before, yielding (h1 a).  But now, because of the call of
double-rewrite, the rewriter takes (h1 a) and rewrites it under the
empty unify-subst.  What's more, because of the defcong event above,
this rewrite takes place in a context where it suffices to maintain the
equivalence relation my-equiv.  This allows for the application of
lemma-1, hence (h1 a) is rewritten (under unify-subst = nil) to (h2 a).
Popping back up, the rewriter will now rewrite the call of foo to t
using lemma-2.

The example above explains how the rewriter treats calls of
double-rewrite, but it may leave the unfortunate impression that the
user needs to consider each :rewrite or :linear rule carefully, just in
case a call of double-rewrite may be appropriate.  Fortunately, ACL2
provides a "[Double-rewrite]" warning to inform the user of just this
sort of situation.  If you don't see this warning when you submit a
(:rewrite or :linear) rule, then the issue described here shouldn't
come up for that rule.  Such warnings may appear for hypotheses or
right-hand side of a :rewrite rule, and for hypotheses or full
conclusion (as opposed to just the trigger term) of a :linear rule.

If you do see a "[Double-rewrite]" warning, then should you add the
indicated call(s) of double-rewrite?  At the time of writing this
documentation, the answer is not clear.  Early experiments with double
rewriting suggested that it may be too expensive to call double-rewrite
in every instance where a warning indicates that there could be an
advantage to doing so.  And at the time of this writing, the ACL2
regression suite has about 1900 such warnings (but note that books were
developed before double-rewrite or the "[Double-rewrite]" warning were
implemented), which suggests that one can often do fine just ignoring
such warnings.  However, it seems advisable to go ahead and add the
calls of double-rewrite indicated by the warnings unless you run across
efficiency problems caused by doing so.  Of course, if you decide to
ignore all such warnings you can execute the event:
(set-inhibit-warnings "Double-rewrite").

Finally, we note that it is generally not necessary to call
double-rewrite in order to get its effect in the following case, where
the discussion above might have led one to consider a call of
double-rewrite: a hypothesis is a variable, or more generally, we are
considering a variable occurrence that is a branch of the top-level IF
structure of a hypothesis.  The automatic handling of this case, by a
form of double rewriting, was instituted in ACL2 Version_2.9 and
remains in place with the introduction of double-rewrite.  Here is a
simple illustrative example.  Notice that foo-holds applies to prove
the final thm below, even without a call of double-rewrite in the
hypothesis of foo-holds, and that there is no "[Double-rewrite]"
warning when submitting foo-holds.

     (encapsulate
      (((foo *) => *)
       ((bar *) => *))

      (local (defun foo (x) (declare (ignore x)) t))
      (local (defun bar (x) (declare (ignore x)) t))

      (defthm foo-holds
        (implies x
                 (equal (foo x) t)))
      (defthm bar-holds-propositionally
        (iff (bar x) t)))

     (thm (foo (bar y)))

EMBEDDED-EVENT-FORM    forms that may be embedded in other events

     Examples:
     (defun hd (x) (if (consp x) (car x) 0))
     (local (defthm lemma23 ...))
     (progn (defun fn1 ...)
            (local (defun fn2 ...))
            ...)

     General Form:
     An embedded event form is a term, x, such that:

     o x is a call of an event function other than DEFPKG (see
     EVENTS for a listing of the event functions);

     o x is of the form (LOCAL x1) where x1 is an embedded event form;

     o x is of the form (SKIP-PROOFS x1) where x1 is an embedded event
     form;

     o x is of the form (MAKE-EVENT &), where & is any term whose
     expansion is an embedded event (see MAKE-EVENT);

     o x is of the form (WITH-OUTPUT ... x1), (WITH-PROVER-STEP-LIMIT
     ... x1 ...), or (WITH-PROVER-TIME-LIMIT ... x1), where x1 is an
     embedded event form;

     o x is a call of ENCAPSULATE, PROGN, PROGN!, or INCLUDE-BOOK;

     o x macroexpands to one of the forms above; or

     o [intended only for the implementation] x is (RECORD-EXPANSION x1
     x2), where x1 and x2 are embedded event forms.

An exception: an embedded event form may not set the
acl2-defaults-table when in the context of local.  Thus for example,
the form

     (local (table acl2-defaults-table :defun-mode :program))

is not an embedded event form, nor is the form (local (program)), since
the latter sets the acl2-defaults-table implicitly.  An example at the
end of the discussion below illustrates why there is this restriction.

Only embedded event forms are allowed in a book after its initial
in-package form.  See BOOKS.  However, you may find that
make-event allows you to get the effect you want for a form that is not
an embedded event form.  For example, you can put the following into a
book, which assigns the value 17 to state global variable x:

     (make-event (er-progn (assign x 17)
                           (value '(value-triple nil)))
                 :check-expansion t)

When an embedded event is executed while ld-skip-proofsp is
'include-book, those parts of it inside local forms are ignored.  Thus,

        (progn (defun f1 () 1)
               (local (defun f2 () 2))
               (defun f3 () 3))

will define f1, f2, and f3 when ld-skip-proofsp is nil or t, but will
define only f1 and f3 when ld-skip-proofsp is 'include-book.

_Discussion:_

Encapsulate, progn, and include-book place restrictions on the kinds of
forms that may be processed.  These restrictions ensure that the
non-local events are indeed admissible provided that the sequence of
local and non-local events is admissible when proofs are done, i.e.,
when ld-skip-proofs is nil.  But progn! places no such restrictions,
hence is potentially dangerous and should be avoided unless you
understand the ramifications; so it is illegal unless there is an active
trust tag (see DEFTTAG).

Local permits the hiding of an event or group of events in the sense
that local events are processed when we are trying to establish the
admissibility of a sequence of events embedded in encapsulate forms or
in books, but are ignored when we are constructing the world produced
by assuming that sequence.  Thus, for example, a particularly ugly and
inefficient :rewrite rule might be made local to an encapsulate that
"exports" a desirable theorem whose proof requires the ugly lemma.

To see why we can't allow just anything as an embedded event, consider
allowing the form

     (if (ld-skip-proofsp state)
         (defun foo () 2)
         (defun foo () 1))

followed by

     (defthm foo-is-1 (equal (foo) 1)).

When we process the events with ld-skip-proofsp is nil, the second
defun is executed and the defthm succeeds.  But when we process the
events with ld-skip-proofsp 'include-book, the second defun is
executed, so that foo no longer has the same definition it did when we
proved foo-is-1.  Thus, an invalid formula is assumed when we process
the defthm while skipping proofs.  Thus, the first form above is not a
legal embedded event form.

If you encounter a situation where these restrictions seem to prevent
you from doing what you want to do, then you may find make-event to be
helpful.  See MAKE-EVENT.

Defpkg is not allowed because it affects how things are read after it
is executed.  But all the forms embedded in an event are read before
any are executed.  That is,

     (encapsulate nil
                  (defpkg "MY-PKG" nil)
                  (defun foo () 'my-pkg::bar))

makes no sense since my-pkg::bar must have been read before the defpkg
for "MY-PKG" was executed.

Finally, let us elaborate on the restriction mentioned earlier related
to the acl2-defaults-table.  Consider the following form.

     (encapsulate
      ()
      (local (program))
      (defun foo (x)
        (if (equal 0 x)
            0
          (1+ (foo (- x))))))

See LOCAL-INCOMPATIBILITY for a discussion of how encapsulate
processes event forms.  Briefly, on the first pass through the events
the definition of foo will be accepted in defun mode :program, and
hence accepted.  But on the second pass the form (local (program)) is
skipped because it is marked as local, and hence foo is accepted in
defun mode :logic.  Yet, no proof has been performed in order to admit
foo, and in fact, it is not hard to prove a contradiction from this
definition!

ENABLE-FORCING    to allow forced splits

     General Form:
     ACL2 !>:enable-forcing    ; allowed forced case splits

See FORCE and see CASE-SPLIT for a discussion of forced
case splits, which are turned back on by this command.  (See
DISABLE-FORCING for how to turn them off.)

Enable-forcing is actually a macro that enables the executable
counterpart of the function symbol force; see FORCE.  When you
want to use hints to turn on forced case splits, use a form such as one
of the following (these are equivalent).

     :in-theory (enable (:executable-counterpart force))
     :in-theory (enable (force))

ENABLE-IMMEDIATE-FORCE-MODEP    forced hypotheses are attacked immediately

     General Form:
     ACL2 !>:enable-immediate-force-modep

This event causes ACL2 to attack forced hypotheses immediately instead
of delaying them to the next forcing round.  See
IMMEDIATE-FORCE-MODEP.  Or for more basic information, first see
FORCE for a discussion of forced case splits.

Enable-immediate-force-modep is a macro that enables the executable
counterpart of the function symbol immediate-force-modep.  When you
want to enable this mode in hints, use a form such as one of the
following (these are equivalent).

     :in-theory (enable (:executable-counterpart immediate-force-modep))
     :in-theory (enable (immediate-force-modep))

ENTER-BOOT-STRAP-MODE    The first millisecond of the Big Bang

ACL2 functions, e.g., if, that show enter-boot-strap-mode as their
defining command are in fact primitives.  It is impossible for the
system to display defining axioms about these symbols.

Enter-boot-strap-mode is a Common Lisp function but not an ACL2
function.  It magically creates from nil an ACL2 property list world
that lets us start the boot-strapping process.  That is, once
enter-boot-strap-mode has created its world, it is possible to process
the defconsts, defuns, and defaxioms, necessary to bring up the rest of
the system.  Before that world is created, the attempt by ACL2 even to
translate a defun form, say, would produce an error because defun is
undefined.

Several ACL2 functions show enter-boot-strap-mode as their defining
command.  Among them are if, cons, car, and cdr.  These functions are
characterized by axioms rather than definitional equations -- axioms
that in most cases are built into our code and hence do not have any
explicit representation among the rules and formulas in the system.

ESCAPE-TO-COMMON-LISP    escaping to Common Lisp

     Example:
     ACL2 !>:Q

There is no Common Lisp escape feature in the lp.  This is part of the
price of purity.  To execute a form in Common Lisp as opposed to ACL2,
exit lp with :q, submit the desired forms to the Common Lisp
read-eval-print loop, and reenter ACL2 with (lp).

EXECUTABLE-COUNTERPART    a rule for computing the value of a function

     Examples:
     (:executable-counterpart length)

which may be abbreviated in theories as

     (length)

Every defun introduces at least two rules used by the theorem prover.
Suppose fn is the name of a defun'd function.  Then (:definition fn) is
the rune (see RUNE) naming the rule that allows the simplifier
to replace calls of fn by its instantiated body.
(:executable-counterpart fn) is the rune for the rule for how to
evaluate the function on known constants.

When typing theories it is convenient to know that (fn) is a runic
designator that denotes (:executable-counterpart fn).  See
THEORIES.

If (:executable-counterpart fn) is enabled, then when applications of
fn to known constants are seen by the simplifier they are computed out
by executing the Common Lisp code for fn (with the appropriate handling
of guards).  Suppose fact is defined as the factorial function.  If the
executable counterpart rune of fact, (:executable-counterpart fact), is
enabled when the simplifier encounters (fact 12), then that term will
be "immediately" expanded to 479001600.  Note that even if subroutines
of fn have disabled executable counterparts, fn will call their Lisp
code nonetheless:  once an executable counterpart function is applied,
no subsidiary enable checks are made.

Such one-step expansions are sometimes counterproductive because they
prevent the anticipated application of certain lemmas about the
subroutines of the expanded function.  Such computed expansions can be
prevented by disabling the executable counterpart rune of the relevant
function.  For example, if (:executable-counterpart fact) is disabled,
(fact 12) will not be expanded by computation.  In this situation,
(fact 12) may be rewritten to (* 12 (fact 11)), using the rule named
(:definition fact), provided the system's heuristics permit the
introduction of the term (fact 11).  Note that lemmas about
multiplication may then be applicable (while such lemmas would be
inapplicable to 479001600).  In many proofs it is desirable to disable
the executable counterpart runes of certain functions to prevent their
expansion by computation.  See EXECUTABLE-COUNTERPART-THEORY.

Finally:  What do we do about functions that are "constrained" rather
than defined, such as the following?  (See ENCAPSULATE.)

     (encapsulate (((foo *) => *))
                  (local (defun foo (x) x)))

Does foo have an executable counterpart?  Yes:  since the vast majority
of functions have sensible executable counterparts, it was decided that
*all* functions, even such "constrained" ones, have executable
counterparts.  We essentially "trap" when such calls are inappropriate.
Thus, consider for example:

     (defun bar (x)
       (if (rationalp x)
           (+ x 1)
         (foo x)))

If the term (bar '3) is encountered by the ACL2 rewriter during a
proof, and if the :executable-counterpart of bar is enabled, then it
will be invoked to reduce this term to '4.  However, if the term (bar
'a) is encountered during a proof, then since 'a is not a rationalp and
since the :executable-counterpart of foo is only a "trap," then this
call of the :executable-counterpart of bar will result in a "trap." In
that case, the rewriter will return the term (hide (bar 'a)) so that it
never has to go through this process again.  See HIDE.

EXIT-BOOT-STRAP-MODE    the end of pre-history

Exit-boot-strap-mode is the last step in creating the ACL2 world in
which the user lives.  It has command number 0.  Commands before it are
part of the system initialization and extend all the way back to :min.
Commands after it are those of the user.

Exit-boot-strap-mode is a Common Lisp function but not an ACL2
function.  It is called when every defconst, defun, etc., in our source
code has been processed under ACL2 and the world is all but complete.
exit-boot-strap-mode has only one job: to signal the completion of the
boot-strapping.

EXPAND    hints keyword :EXPAND

See HINTS.

EXTENDED-METAFUNCTIONS    state and context sensitive metafunctions

     General Form of an Extended :Meta theorem:
     (implies (and (pseudo-termp x)              ; this hyp is optional
                   (alistp a)                    ; this hyp is optional
                   (ev (hyp-fn x mfc state) a)   ; this hyp is optional
                   ; meta-extract hyps may also be included (see below)
                   )
              (equiv (ev x a)
                     (ev (fn x mfc state) a)))

where the restrictions are as described in the documentation for meta
and, in addition, mfc and state are distinct variable symbols
(different also from x and a) and state is literally the symbol STATE.
A :meta theorem of the above form installs fn as a metatheoretic
simplifier with hypothesis function hyp-fn, exactly as for vanilla
metafunctions.  The only difference is that when the metafunctions are
applied, some contextual information is passed in via the mfc argument
and the ACL2 state is made available.

See META for a discussion of vanilla flavored metafunctions.
This documentation assumes you are familiar with the simpler situation,
in particular, how to define a vanilla flavored metafunction, fn, and
its associated hypothesis metafunction, hyp-fn, and how to state and
prove metatheorems installing such functions.  Defining extended
metafunctions requires that you also be familiar with many ACL2
implementation details.  This documentation is sketchy on these
details; see the ACL2 source code or email the acl2-help list if you
need more help.

Additional hypotheses are supported, called "meta-extract hypotheses",
that allow metafunctions to depend on the validity of certain terms
extracted from the context or the logical world.  These hypotheses
provide a relatively advanced form of metatheorem so we explain them
elsewhere; see META-EXTRACT.

The metafunction context, mfc, is a list containing many different data
structures used by various internal ACL2 functions.  We do not document
the form of mfc.  Your extended metafunction should just take mfc as its
second formal and pass it into the functions mentioned below.  The ACL2
state is well-documented (see STATE).  Below we present
expressions below that can be useful in defining extended
metafunctions.  Some of these expressions involve keyword arguments,
:forcep and :ttree, which are optional and in most cases are fine to
omit, and which we explain after we present the useful expressions.

(mfc-clause mfc): returns the current goal, in clausal form.  A clause
is a list of ACL2 terms, implicitly denoting the disjunction of the
listed terms.  The clause returned by mfc-clause is the clausal form of
the translation (see TRANS) of the goal or subgoal on which the
rewriter is working.  When a metafunction calls mfc-clause, the term
being rewritten by the metafunction either occurs somewhere in this
clause or, perhaps more commonly, is being rewritten on behalf of some
lemma to which the rewriter has backchained while trying to rewrite a
term in the clause.

(mfc-ancestors mfc): returns an alist whose keys are the negations of
the backchaining hypotheses being pursued.  In particular, (null
(mfc-ancestors mfc)) will be true exactly when rewriting is on part of
the current goal.  Exception: An element of this alist whose key is of
the form (:binding-hyp hyp unify-subst) indicates that hyp has been
encountered as a hypothesis of the form (equal var term) or (equiv var
(double-rewrite-term)), in each case binding variable var to the result
of rewriting term under unify-subst.

(mfc-rdepth mfc): returns the remaining stack depth for calls of the
rewriter (by default, *default-rewrite-stack-limit* at the top level;
see REWRITE-STACK-LIMIT).  When this is 0, no further calls of
the rewriter can be made without error.

(mfc-type-alist mfc): returns the type-alist governing the occurrence of
the term, x, being rewritten by the metafunction.  A type-alist is an
association list, each element of which is of the form (term ts .
ttree).  Such an element means that the term term has the type-set ts.
The ttree component is probably irrelevant here.  All the terms in the
type-alist are in translated form (see TRANS).  The ts are
numbers denoting finite Boolean combinations of ACL2's primitive types
(see TYPE-SET).  The type-alist includes not only information
gleaned from the conditions governing the term being rewritten but also
that gleaned from forward chaining from the (negations of the) other
literals in the clause returned by mfc-clause.

(w state): returns the ACL2 logical world.

(mfc-ts term mfc state :forcep forcep :ttreep ttreep): returns the
type-set of term in the current context; see TYPE-SET.

(mfc-rw term obj equiv-info mfc state): returns the result of rewriting
term in the current context, mfc, with objective obj and the
equivalence relation described by equiv-info.  Obj should be t, nil, or
?, and describes your objective: try to show that term is true, false,
or anything.  Equiv-info is either nil, t, a function symbol fn naming
a known equivalence relation, or a list of congruence rules.  Nil means
return a term that is equal to term.  T means return a term that is
propositionally equivalent (i.e., in the iff sense) to term, while fn
means return a term fn-equivalent to term.  The final case, which is
intended only for advanced users, allows the specification of generated
equivalence relations, as supplied to the geneqv argument of rewrite.
Generally, if you wish to establish that term is true in the current
context, use the idiom

     (equal (mfc-rw term t t mfc state) *t*)

The constant *t* is set to the internal form of the constant term t,
i.e., 't.

(mfc-rw+ term alist obj equiv-info mfc state): if alist is nil then
this is equivalent to (mfc-rw term obj equiv-info mfc state).  However,
the former takes an argument, alist, that binds variables to terms, and
returns the result of rewriting term under that alist, where this
rewriting is as described for mfc-rw above.  The function mfc-rw+ can
be more efficient than mfc-rw, because the terms in the binding alist
have generally already been rewritten, and it can be inefficient to
rewrite them again.  For example, consider a rewrite rule of the
following form.

     (implies (and ...
                   (syntaxp (... (mfc-rw `(bar ,x) ...) ...))
                   ...)
              (equal (... x ...) ...))

Here, x is bound in the conclusion to the result of rewriting some term,
say, tm.  Then the above call of mfc-rw will rewrite tm, which is
probably unnecessary.  So a preferable form of the rule above may be as
follows, so that tm is not further rewritten by mfc-rw+.

     (implies (and ...
                   (syntaxp (... (mfc-rw+ '(bar v) `((v . ,x)) ...) ...))
                   ...)
              (equal (... x ...) ...))

However, you may find that the additional rewriting done by mfc-rw is
useful in some cases.

(mfc-ap term mfc state): returns t or nil according to whether linear
arithmetic can determine that term is false.  To the cognoscenti:
returns the contradiction flag produced by linearizing term and adding
it to the linear-pot-lst.

(mfc-relieve-hyp hyp alist rune target bkptr mfc state): returns c[t or
nil according to whether the indicated hypothesis term, hyp, can be
relieved (proved) under the giving variable bindings, alist.  Here, hyp
is the hypothesis of the indicated rune at (one-based) position bkptr,
and target is an instantiated term to which rune is being applied.
Note that no indication is returned for whether any assumptions have
been generated by force or case-split.  (If you need such a feature,
feel free to request it of the ACL2 implementors.)

We explain the :forcep and :ttreep keyword arguments provided in some
expressions, as promised above.  Their defaults are :same and nil,
respectively.  A value of :same for :forcep means that forcing will be
allowed if and only if it is allowed in the current rewriting
environment; see FORCE.  A value of t or nil for :forcep
overrides this default and allows or disallows forcing, respectively.
By default these functions return a single value, val, but if :ttreep
is t then they return (mv val ttree), where ttree is the tag-tree (see
TTREE) returned by the indicated operation, with an input
tag-tree of nil).

During the execution of a metafunction by the theorem prover, the
expressions above compute the results specified.  Typically, you should
imagine that there are no axioms about the mfc- function symbols: treat
them as uninterpreted function symbols.  There is an advanced feature,
meta-extract hypotheses, that can avoid this logical weakness in some
cases when proving :meta rules; see META-EXTRACT.  But we
assume for the rest of the present documentation topic that you do not
use meta-extract hypotheses.  Thus, in the proof of the correctness of
a metafunction, no information is available about the results of these
functions: you should _use these functions for heuristic purposes only_.

For example, your metafunction may use these functions to decide
whether to perform a given transformation, but the transformation must
be sound regardless of the value that your metafunction returns.  We
illustrate this below.  It is sometimes possible to use the hypothesis
metafunction, hyp-fn, to generate a sufficient hypothesis to justify the
transformation.  The generated hypothesis might have already been
"proved" internally by your use of mfc-ts or mfc-rw, but the system
will have to prove it "officially" by relieving it.  We illustrate this
below also.

We conclude with a script that defines, verifies, and uses several
extended metafunctions.  This script is based on one provided by Robert
Krug, who was instrumental in the development of this style of
metafunction and whose help we gratefully acknowledge.

     ; Here is an example.  I will define (foo i j) simply to be (+ i j).
     ; But I will keep its definition disabled so the theorem prover
     ; doesn't know that.  Then I will define an extended metafunction
     ; that reduces (foo i (- i)) to 0 provided i has integer type and the
     ; expression (< 10 i) occurs as a hypothesis in the clause.

     ; Note that (foo i (- i)) is 0 in any case.

     (defun foo (i j) (+ i j))

     (defevaluator eva eva-lst ((foo i j)
                                (unary-- i)

     ; I won't need these two cases until the last example below, but I
     ; include them now.

                                (if x y z)
                                (integerp x)))

     (set-state-ok t)

     (defun metafn (x mfc state)
       (cond
        ((and (consp x)
              (equal (car x) 'foo)
              (equal (caddr x) (list 'unary-- (cadr x))))

     ; So x is of the form (foo i (- i)).  Now I want to check some other
     ; conditions.

         (cond ((and (ts-subsetp (mfc-ts (cadr x) mfc state)
                                 *ts-integer*)
                     (member-equal `(NOT (< '10 ,(cadr x)))
                                   (mfc-clause mfc)))
                (quote (quote 0)))
               (t x)))
        (t x)))

     (defthm metafn-correct
       (equal (eva x a) (eva (metafn x mfc state) a))
       :rule-classes ((:meta :trigger-fns (foo))))

     (in-theory (disable foo))

     ; The following will fail because the metafunction won't fire.
     ; We don't know enough about i.

     (thm (equal (foo i (- i)) 0))

     ; Same here.

     (thm (implies (and (integerp i) (< 0 i)) (equal (foo i (- i)) 0)))

     ; But this will work.

     (thm (implies (and (integerp i) (< 10 i))
                   (equal (foo i (- i)) 0)))

     ; This won't, because the metafunction looks for (< 10 i) literally,
     ; not just something that implies it.

     (thm (implies (and (integerp i) (< 11 i))
                   (equal (foo i (- i)) 0)))

     ; Now I will undo the defun of metafn and repeat the exercise, but
     ; this time check the weaker condition that (< 10 i) is provable
     ; (by rewriting it) rather than explicitly present.

     (ubt 'metafn)

     (defun metafn (x mfc state)
       (cond
        ((and (consp x)
              (equal (car x) 'foo)
              (equal (caddr x) (list 'unary-- (cadr x))))
         (cond ((and (ts-subsetp (mfc-ts (cadr x) mfc state)
                                 *ts-integer*)
                     (equal (mfc-rw `(< '10 ,(cadr x)) t t mfc state)
                            *t*))

     ; The mfc-rw above rewrites (< 10 i) with objective t and iffp t.  The
     ; objective means the theorem prover will try to establish it.  The
     ; iffp means the theorem prover can rewrite maintaining propositional
     ; equivalence instead of strict equality.

                (quote (quote 0)))
               (t x)))
        (t x)))

     (defthm metafn-correct
       (equal (eva x a) (eva (metafn x mfc state) a))
       :rule-classes ((:meta :trigger-fns (foo))))

     (in-theory (disable foo))

     ; Now it will prove both:

     (thm (implies (and (integerp i) (< 10 i))
                   (equal (foo i (- i)) 0)))

     (thm (implies (and (integerp i) (< 11 i))
                   (equal (foo i (- i)) 0)))

     ; Now I undo the defun of metafn and change the problem entirely.
     ; This time I will rewrite (integerp (foo i j)) to t.  Note that
     ; this is true if i and j are integers.  I can check this
     ; internally, but have to generate a hyp-fn to make it official.

     (ubt 'metafn)

     (defun metafn (x mfc state)
       (cond
        ((and (consp x)
              (equal (car x) 'integerp)
              (consp (cadr x))
              (equal (car (cadr x)) 'foo))

     ; So x is (integerp (foo i j)).  Now check that i and j are
     ; ``probably'' integers.

         (cond ((and (ts-subsetp (mfc-ts (cadr (cadr x)) mfc state)
                                 *ts-integer*)
                     (ts-subsetp (mfc-ts (caddr (cadr x)) mfc state)
                                 *ts-integer*))
                *t*)
               (t x)))
        (t x)))

     ; To justify this transformation, I generate the appropriate hyps.

     (defun hyp-fn (x mfc state)

       (declare (ignore mfc state))

     ; The hyp-fn is run only if the metafn produces an answer different
     ; from its input.  Thus, we know at execution time that x is of the
     ; form (integerp (foo i j)) and we know that metafn rewrote
     ; (integerp i) and (integerp j) both to t.  So we just produce their
     ; conjunction.  Note that we must produce a translated term; we
     ; cannot use the macro AND and must quote constants!  Sometimes you
     ; must do tests in the hyp-fn to figure out which case the metafn
     ; produced, but not in this example.

                `(if (integerp ,(cadr (cadr x)))
                     (integerp ,(caddr (cadr x)))
                     'nil))

     (defthm metafn-correct
       (implies (eva (hyp-fn x mfc state) a)
                (equal (eva x a) (eva (metafn x mfc state) a)))
       :rule-classes ((:meta :trigger-fns (integerp))))

     (in-theory (disable foo))

     ; This will not be proved.

     (thm (implies (and (rationalp x) (integerp i)) (integerp (foo i j))))

     ; But this will be.

     (thm (implies (and (rationalp x)
                        (integerp i)
                        (integerp j))
                   (integerp (foo i j))))

FAILED-FORCING    how to deal with a proof failure in a forcing round

See FORCING-ROUND for a background discussion of the notion of
forcing rounds.  When a proof fails during a forcing round it means
that the "gist" of the proof succeeded but some "technical detail"
failed.  The first question you must ask yourself is whether the forced
goals are indeed theorems.  We discuss the possibilities below.

If you believe the forced goals are theorems, you should follow the
usual methodology for "fixing" failed ACL2 proofs, e.g., the
identification of key lemmas and their timely and proper use as rules.
See FAILURE, see GAG-MODE, and see PROOF-TREE.

The rules designed for the goals of forcing rounds are often just what
is needed to prove the forced hypothesis at the time it is forced.
Thus, you may find that when the system has been "taught" how to prove
the goals of the forcing round no forcing round is needed.  This is
intended as a feature to help structure the discovery of the necessary
rules.

If a hint must be provided to prove a goal in a forcing round, the
appropriate "goal specifier" (the string used to identify the goal to
which the hint is to be applied) is just the text printed on the line
above the formula, e.g., "[1]Subgoal *1/3"".  See GOAL-SPEC.

If you solve a forcing problem by giving explicit hints for the goals
of forcing rounds, you might consider whether you could avoid forcing
the assumption in the first place by giving those hints in the
appropriate places of the main proof.  This is one reason that we print
out the origins of each forced assumption.  An argument against this
style, however, is that an assumption might be forced in hundreds of
places in the main goal and proved only once in the forcing round, so
that by delaying the proof you actually save time.

We now turn to the possibility that some goal in the forcing round is
not a theorem.

There are two possibilities to consider.  The first is that the
original theorem has insufficient hypotheses to ensure that all the
forced hypotheses are in fact always true.  The "fix" in this case is
to amend the original conjecture so that it has adequate hypotheses.

A more difficult situation can arise and that is when the conjecture
has sufficient hypotheses but they are not present in the forcing round
goal.  This can be caused by what we call "premature" forcing.

Because ACL2 rewrites from the inside out, it is possible that it will
force hypotheses while the context is insufficient to establish them.
Consider trying to prove (p x (foo x)).  We first rewrite the formula
in an empty context, i.e., assuming nothing.  Thus, we rewrite (foo x)
in an empty context.  If rewriting (foo x) forces anything, that forced
assumption will have to be proved in an empty context.  This will
likely be impossible.

On the other hand, suppose we did not attack (foo x) until after we had
expanded p.  We might find that the value of its second argument, (foo
x), is relevant only in some cases and in those cases we might be able
to establish the hypotheses forced by (foo x).  Our premature forcing
is thus seen to be a consequence of our "over eager" rewriting.

Here, just for concreteness, is an example you can try.  In this
example, (foo x) rewrites to x but has a forced hypothesis of
(rationalp x).  P does a case split on that very hypothesis and uses
its second argument only when x is known to be rational.  Thus, the
hypothesis for the (foo x) rewrite is satisfied.  On the false branch
of its case split, p simplies to (p1 x) which can be proved under the
assumption that x is not rational.

     (defun p1 (x) (not (rationalp x)))
     (defun p (x y)(if (rationalp x) (equal x y) (p1 x)))
     (defun foo (x) x)
     (defthm foo-rewrite (implies (force (rationalp x)) (equal (foo x) x)))
     (in-theory (disable foo))

The attempt then to do (thm (p x (foo x))) forces the unprovable goal
(rationalp x).

Since all "formulas" are presented to the theorem prover as single
terms with no hypotheses (e.g., since implies is a function), this
problem would occur routinely were it not for the fact that the theorem
prover expands certain "simple" definitions immediately without doing
anything that can cause a hypothesis to be forced.  See SIMPLE.
This does not solve the problem, since it is possible to hide the
propositional structure arbitrarily deeply.  For example, one could
define p, above, recursively so that the test that x is rational and
the subsequent first "real" use of y occurred arbitrarily deeply.

Therefore, the problem remains: what do you do if an impossible goal is
forced and yet you know that the original conjecture was adequately
protected by hypotheses?

One alternative is to disable forcing entirely.  See
DISABLE-FORCING.  Another is to disable the rule that caused the
force.

A third alternative is to prove that the negation of the main goal
implies the forced hypothesis.  For example,

     (defthm not-p-implies-rationalp
       (implies (not (p x (foo x))) (rationalp x))
       :rule-classes nil)

Observe that we make no rules from this formula.  Instead, we merely
:use it in the subgoal where we must establish (rationalp x).

     (thm (p x (foo x))
          :hints (("Goal" :use not-p-implies-rationalp)))

When we said, above, that (p x (foo x)) is first rewritten in an empty
context we were misrepresenting the situation slightly.  When we
rewrite a literal we know what literal we are rewriting and we
implicitly assume it false.  This assumption is "dangerous" in that it
can lead us to simplify our goal to nil and give up -- we have even
seen people make the mistake of assuming the negation of what they
wished to prove and then via a very complicated series of
transformations convince themselves that the formula is false.  Because
of this "tail biting" we make very weak use of the negation of our
goal.  But the use we make of it is sufficient to establish the forced
hypothesis above.

A fourth alternative is to weaken your desired theorem so as to make
explicit the required hypotheses, e.g., to prove

     (defthm rationalp-implies-main
       (implies (rationalp x) (p x (foo x)))
       :rule-classes nil)

This of course is unsatisfying because it is not what you originally
intended.  But all is not lost.  You can now prove your main theorem
from this one, letting the implies here provide the necessary case
split.

     (thm (p x (foo x))
          :hints (("Goal" :use rationalp-implies-main)))

FAILURE    how to deal with a proof failure

When ACL2 gives up it does not mean that the submitted conjecture is
invalid, even if the last formula ACL2 printed in its proof attempt is
manifestly false.  Since ACL2 sometimes generalizes the goal being
proved, it is possible it adopted an invalid subgoal as a legitimate
(but doomed) strategy for proving a valid goal.  Nevertheless,
conjectures submitted to ACL2 are often invalid and the proof attempt
often leads the careful reader to the realization that a hypothesis has
been omitted or that some special case has been forgotten.  It is good
practice to ask yourself, when you see a proof attempt fail, whether
the conjecture submitted is actually a theorem.

If you think the conjecture is a theorem, then you must figure out from
ACL2's output what you know that ACL2 doesn't about the functions in the
conjecture and how to impart that knowledge to ACL2 in the form of
rules.  The "key checkpoint" information printed at the end of the
summary provides a fine place to start.  See THE-METHOD for a
general discussion of how to prove theorems with ACL2, and see
INTRODUCTION-TO-THE-THEOREM-PROVER for a more detailed tutorial.
Also see SET-GAG-MODE for discussion of key checkpoints and an
abbreviated output mode that focuses attention on them.  You may find
it most useful to start by focusing on key checkpoints that are not
under a proof by induction, if any, both because these are more likely
to suggest useful lemmas and because they are more likely to be
theorems; for example, generalization may have occurred before a proof
by induction has begun.  If you need more information than is provided
by the key checkpoints -- although this should rarely be necessary --
then you can look at the full proof, perhaps with the aid of certain
utilities: see PROOF-TREE, see SET-GAG-MODE, and see
SET-SAVED-OUTPUT.

For information on a tool to help debug failures of encapsulate and
progn events, as well as certify-book failures, see REDO-FLAT.

Again, see THE-METHOD for a general discussion of how to prove
theorems with ACL2, and see INTRODUCTION-TO-THE-THEOREM-PROVER
for a more detailed tutorial.  See also the book "Computer-Aided
Reasoning: An Approach" (Kaufmann, Manolios, Moore), as well as the
discussion of how to read Nqthm proofs and how to use Nqthm rules in "A
Computational Logic Handbook" by Boyer and Moore (Academic Press, 1988).

If the failure occurred during a forcing round, see
FAILED-FORCING.

FIND-RULES-OF-RUNE    find the rules named rune

     General Form:
     (find-rules-of-rune rune wrld)

This function finds all the rules in wrld with :rune rune.  It returns
a list of rules in their internal form (generally as described by the
corresponding defrec).  Decyphering these rules is difficult since one
cannot always look at a rule object and decide what kind of record it
is without exploiting many system invariants (e.g., that :rewrite runes
only name rewrite-rules).

At the moment this function returns nil if the rune in question is a
:refinement rune, because there is no object representing :refinement
rules.  (:refinement rules cause changes in the 'coarsenings
properties.)  In addition, if the rune is an :equivalence rune, then
congruence rules with that rune will be returned -- because
:equivalence lemmas generate some congruence rules -- but the fact that
a certain function is now known to be an equivalence relation is not
represented by any rule object and so no such rule is returned.  (The
fact that the function is an equivalence relation is encoded entirely
in its presence as a 'coarsening of equal.)

FORCE    identity function used to force a hypothesis

When a hypothesis of a conditional rule has the form (force hyp) it is
logically equivalent to hyp but has a pragmatic effect.  In particular,
when the rule is considered, the needed instance of the hypothesis,
hyp', is assumed and a special case is generated, requiring the system
to prove that hyp' is true in the current context.  The proofs of all
such "forced assumptions" are delayed until the successful completion
of the main goal.  See FORCING-ROUND.

Forcing should only be used on hypotheses that are always expected to be
true, as is commonly the case for guards of functions.  All the power of
the theorem prover is brought to bear on a forced hypothesis and no
backtracking is possible.  Forced goals can be attacked immediately
(see IMMEDIATE-FORCE-MODEP) or in a subsequent forcing round
(see FORCING-ROUND).  Also see CASE-SPLIT for a related
utility.  If the :executable-counterpart of the function force is
disabled, then no hypothesis is forced.  For more on enabling and
disabling forcing, see ENABLE-FORCING and see
DISABLE-FORCING.

It sometimes happens that a conditional rule is not applied because
some hypothesis, hyp, could not be relieved, even though the required
instance of hyp, hyp', can be shown true in the context.  This happens
when insufficient resources are brought to bear on hyp' at the time we
try to relieve it.  A sometimes desirable alternative behavior is for
the system to assume hyp', apply the rule, and to generate explicitly a
special case to show that hyp' is true in the context.  This is called
"forcing" hyp.  It can be arranged by restating the rule so that the
offending hypothesis, hyp, is embedded in a call of force, as in (force
hyp).  By using the :corollary field of the rule-classes entry, a
hypothesis can be forced without changing the statement of the theorem
from which the rule is derived.

Technically, force is just a function of one argument that returns that
argument.  It is generally enabled and hence evaporates during
simplification.  But its presence among the hypotheses of a conditional
rule causes case splitting to occur if the hypothesis cannot be
conventionally relieved.

Since a forced hypothesis must be provable whenever the rule is
otherwise applicable, forcing should be used only on hypotheses that
are expected always to be true.

A particularly common situation in which some hypotheses should be
forced is in "most general" type-prescription lemmas.  If a single
lemma describes the "expected" type of a function, for all "expected"
arguments, then it is probably a good idea to force the hypotheses of
the lemma.  Thus, every time a term involving the function arises, the
term will be given the expected type and its arguments will be required
to be of the expected type.  In applying this advice it might be wise
to avoid forcing those hypotheses that are in fact just type predicates
on the arguments, since the routine that applies type-prescription
lemmas has fairly thorough knowledge of the types of all terms.

Force can have the additional benefit of causing the ACL2 typing
mechanism to interact with the ACL2 rewriter to establish the
hypotheses of type-prescription rules.  To understand this remark,
think of the ACL2 type reasoning system as a rather primitive
rule-based theorem prover for questions about Common Lisp types, e.g.,
"does this expression produce a consp?"  "does this expression produce
some kind of ACL2 number, e.g., an integerp, a rationalp, or a
complex-rationalp?" etc.  It is driven by type-prescription rules.  To
relieve the hypotheses of such rules, the type system recursively
invokes itself.  This can be done for any hypothesis, whether it is
"type-like" or not, since any proposition, p, can be phrased as the
type-like question "does p produce an object of type nil?"  However, as
you might expect, the type system is not very good at establishing
hypotheses that are not type-like, unless they happen to be assumed
explicitly in the context in which the question is posed, e.g., "If p
produces a consp then does p produce nil?"  If type reasoning alone is
insufficient to prove some instance of a hypothesis, then the instance
will not be proved by the type system and a type-prescription rule with
that hypothesis will be inapplicable in that case.  But by embedding
such hypotheses in force expressions you can effectively cause the type
system to "punt" them to the rest of the theorem prover.  Of course, as
already noted, this should only be done on hypotheses that are "always
true."  In particular, if rewriting is required to establish some
hypothesis of a type-prescription rule, then the rule will be found
inapplicable because the hypothesis will not be established by type
reasoning alone.

The ACL2 rewriter uses the type reasoning system as a subsystem.  It is
therefore possible that the type system will force a hypothesis that
the rewriter could establish.  Before a forced hypothesis is reported
out of the rewriter, we try to establish it by rewriting.

This makes the following surprising behavior possible: A
type-prescription rule fails to apply because some true hypothesis is
not being relieved.  The user changes the rule so as to *force* the
hypothesis.  The system then applies the rule but reports no forcing.
How can this happen?  The type system "punted" the forced hypothesis to
the rewriter, which established it.

Finally, we should mention that the rewriter is never willing to force
when there is an if term present in the goal being simplified.  Since
and terms and or terms are merely abbreviations for if terms, they also
prevent forcing.  Note that if terms are ultimately eliminated using
the ordinary flow of the proof (but see
SET-CASE-SPLIT-LIMITATIONS), allowing force ultimately to function as
intended.  Moreover, forcing can be disabled, as described above; also
see DISABLE-FORCING.

FORCING-ROUND    a section of a proof dealing with forced assumptions

If ACL2 "forces" some hypothesis of some rule to be true, it is obliged
later to prove the hypothesis.  See FORCE.  ACL2 delays the
consideration of forced hypotheses until the main goal has been proved.
It then undertakes a new round of proofs in which the main goal is
essentially the conjunction of all hypotheses forced in the preceding
proof.  Call this round of proofs the "Forcing Round."  Additional
hypotheses may be forced by the proofs in the Forcing Round.  The
attempt to prove these hypotheses is delayed until the Forcing Round
has been successfully completed.  Then a new Forcing Round is
undertaken to prove the recently forced hypotheses and this continues
until no hypotheses are forced.  Thus, there is a succession of Forcing
Rounds.

The Forcing Rounds are enumerated starting from 1.  The Goals and
Subgoals of a Forcing Round are printed with the round's number
displayed in square brackets.  Thus, "[1]Subgoal 1.3" means that the
goal in question is Subgoal 1.3 of the 1st forcing round.  To supply a
hint for use in the proof of that subgoal, you should use the goal
specifier "[1]Subgoal 1.3".  See GOAL-SPEC.

When a round is successfully completed -- and for these purposes you
may think of the proof of the main goal as being the 0th forcing round
-- the system collects all of the assumptions forced by the
just-completed round.  Here, an assumption should be thought of as an
implication, (implies context hyp), where context describes the context
in which hyp was assumed true.  Before undertaking the proofs of these
assumptions, we try to "clean them up" in an effort to reduce the
amount of work required.  This is often possible because the forced
assumptions are generated by the same rule being applied repeatedly in
a given context.

By delaying and collecting the forced assumptions until the completion
of the "main goal" we gain two advantages.  First, the user gets
confirmation that the "gist" of the proof is complete and that all that
remains are "technical details."  Second, by delaying the proofs of the
forced assumptions ACL2 can undertake the proof of each assumption only
once, no matter how many times it was forced in the main goal.

In order to indicate which proof steps of the previous round were
responsible for which forced assumptions, we print a sentence
explaining the origins of each newly forced goal.  For example,

     [1]Subgoal 1, below, will focus on
     (GOOD-INPUTP (XTRANS I)),
     which was forced in
      Subgoal 14, above,
       by applying (:REWRITE PRED-CRUNCHER) to
       (PRED (XTRANS I) I),
      and
      Subgoal 28, above,
       by applying (:REWRITE PRED-CRUNCHER) to
       (PRED (XTRANS I) I).

In this entry, "[1]Subgoal 1" is the name of a goal which will be
proved in the next forcing round.  On the next line we display the
forced hypothesis, call it x, which is (good-inputp (xtrans i)) in this
example.  This term will be the conclusion of the new subgoal.  Since
the new subgoal will be printed in its entirety when its proof is
undertaken, we do not here exhibit the context in which x was forced.
The sentence then lists (possibly a succession of) a goal name from the
just-completed round and some step in the proof of that goal that
forced x.  In the example above we see that Subgoals 14 and 28 of the
just-completed proof forced (good-inputp (xtrans i)) by applying
(:rewrite pred-cruncher) to the term (pred (xtrans i) i).

If one were to inspect the theorem prover's description of the proof
steps applied to Subgoals 14 and 28 one would find the word "forced"
(or sometimes "forcibly") occurring in the commentary.  Whenever you
see that word in the output, you know you will get a subsequent forcing
round to deal with the hypotheses forced.  Similarly, if at the
beginning of a forcing round a rune is blamed for causing a force in
some subgoal, inspection of the commentary for that subgoal will reveal
the word "forced" after the rule name blamed.

Most forced hypotheses come from within the prover's simplifier.  When
the simplifier encounters a hypothesis of the form (force hyp) it first
attempts to establish it by rewriting hyp to, say, hyp'.  If the truth
or falsity of hyp' is known, forcing is not required.  Otherwise, the
simplifier actually forces hyp'.  That is, the x mentioned above is
hyp', not hyp, when the forced subgoal was generated by the simplifier.

Once the system has printed out the origins of the newly forced goals,
it proceeds to the next forcing round, where those goals are
individually displayed and attacked.

At the beginning of a forcing round, the enabled structure defaults to
the global enabled structure.  For example, suppose some rune, rune, is
globally enabled.  Suppose in some event you disable the rune at "Goal"
and successfully prove the goal but force "[1]Goal".  Then during the
proof of "[1]Goal", rune is enabled "again."  The right way to think
about this is that the rune is "still" enabled.  That is, it is enabled
globally and each forcing round resumes with the global enabled
structure.

FUNCTIONAL-INSTANTIATION-IN-ACL2R    additional requirements for :functional-instance hints in ACL2(r)

This documentation topic relates to ACL2(r), the modification of ACL2
that supports the real numbers (see REAL).

See HINTS and see LEMMA-INSTANCE for a discussion of
:use hints that employ the :functional-instance keyword.  Here, we
document additional requirements for such hints that applies to
ACL2(r).  We assume familiarity with lemma instances; see
LEMMA-INSTANCE.

(1) When functionally instantiating a non-classical formula, it is
illegal to use pseudo-lambda expressions in a lemma instance.

(2) A classical function symbol must be bound either to a classical
function symbol or to a lambda (or, if allowed, pseudo-lambda)
expression with a classical body.  Similarly, a non-classical function
symbol must be bound either to a non-classical function symbol or to a
lambda (or, if allowed, pseudo-lambda) expression with a non-classical
body.

GAG-MODE    verbosity of proof output

Please see SET-GAG-MODE for an explanation of gag-mode, which
can take any of the following values:

     (gag-mode) ; generally evaluates to t, nil, or :goals

GC$    invoke the garbage collector

This function is provided so that the user can call the garbage
collector of the host Lisp from inside the ACL2 loop.  Specifically, a
call of gc$ is translated into a call of a function below on the same
arguments.

     Allegro CL:            excl:gc
     CCL                    ccl::gc
     CLISP                  ext:gc
     CMU Common Lisp        system::gc
     GCL                    si::gbc
     LispWorks              hcl::gc-generation [default argument list:
                                                (7) for 64-bit OS, else (3)]
     SBCL                   sb-ext:gc

The arguments, if any, are as documented in the underlying Common Lisp.
It is up to the user to pass in the right arguments, although we may do
some rudimentary checks.

Also see GC-VERBOSE.

Evaluation of a call of this macro always returns nil.

GC-VERBOSE    control printing from the garbage collector

     General Form:
     (gc-verbose arg)

Garbage collection (gc) is performed by every Lisp implementation; see
GC$.  However, different ACL2 builds might see more or fewer
messages.  This macro is intended to provide an interface for
controlling the verbosity, which is off if the argument evaluates to
nil and otherwise is on.

The above functionality is only supported for the following host Common
Lisp implementations: CCL, CMUCL, and GCL.  Otherwise, the only effect
of this macro is to print a notice that it is not supported.  You are
welcome to contact the ACL2 developers if you would like to help in
adding such support for another host Common Lisp.

Evaluation of a call of this macro always returns nil.

GCL    tips on building and using ACL2 based on Gnu Common Lisp

See the installation instructions for basic information about building
ACL2 on top of GCL, including information about where to fetch GCL.
Here, we provide some tips that may be useful.

1. You can place forms to evaluate at start-up into file init.lsp in the
directory where you are starting ACL2 (GCL), or into file acl2-init.lsp
in your home directory.  For example, in order to evaluate both of the
lisp forms mentioned in 2 below, you could put them both into init.lsp
in the current directory or in ~/acl2-init.lsp (either way, without
(lp) or :q):

     (setq si::*optimize-maximum-pages* nil)
     (si::allocate 'cons 75000 t)

Note that if you want to put ACL2 patches in this file, you should
precede them with (in-package "ACL2").

2. Suppose you run out of space, for example with an error like this:

        Error: The storage for CONS is exhausted.
          Currently, 59470 pages are allocated.
          Use ALLOCATE to expand the space.

The following suggestion from Camm Maguire will minimize the heap size,
at the cost of more garbage collection time.

     :q   ; exit the ACL2 loop
     (setq si::*optimize-maximum-pages* nil)
     (lp) ; re-enter the ACL2 loop

A second thing to try, suggested by several people, is to preallocate
more pages before the run, e.g.:

     :q   ; exit the ACL2 loop
     (si::allocate 'cons 75000 t)
     (lp) ; re-enter the ACL2 loop

Also see RESET-KILL-RING for a suggestion on how to free up
space.

3. Windows users have seen this error:

     cc1.exe: unrecognized option `-fno-zero-initialized-in-bss'

Camm Maguire suggests that a solution may be to evaluate the following
in GCL before building ACL2.

     (in-package 'compiler)
     (let* ((x `-fno-zero-initialized-in-bss')
            (i (search x *cc*)))
             (setq *cc* (concatenate 'string
                                     (subseq *cc* 0 i)
                                     (subseq *cc* (+ i (length x))))))

4. It is possible to profile using ACL2 built on GCL.  See file
save-gprof.lsp in the ACL2 source directory.

5. Some versions of GCL may have garbage-collector bugs that, on rare
occasions, cause ACL2 (when built on GCL) to break.  If you run into
this, a solution may be to execute the following:

     :q
     (si::sgc-on nil)
     (lp)

Alternatively, put (si::sgc-on nil) in your ~/acl2-init.lsp file.

A full regression test and found that this decreased performance by
about 10%.  But even with that, GCL may be the fastest Common Lisp for
ACL2 on Linux (performance figures may often be found by following the
"Recent changes" link on the ACL2 home page).

6. GCL operations on numbers can sometimes be sped up, perhaps by up to
two orders of magnitude, by suitable declare forms (also see
TYPE-SPEC).  The following example, developed with Warren Hunt and
Serita Nelesen, illustrates the use of such declarations.

     ; File iplus.lisp:
     ; Operations on naturals together with positive infinity (represented as -1).

     ; After (ld "iplus.lisp"), escape to raw Lisp with :q and then eavluate
     ; (disassemble 'big-test).  You should see lots of arithmetic operations
     ; in C code, but no calls of C functions CMPmake_fixnum or number_plus.

     (in-package "ACL2")

     (defmacro i-max ()
       (expt 2 (1- 28)))

     (defmacro i+ (x y)
       `(the (signed-byte 28)
             (let ((x ,x)
                   (y ,y))
               (declare (type (signed-byte 28) x y))
               (cond ((or (< x 0)
                          (< y 0))
                      -1)
                     (t (let ((result
                               (the (signed-byte 29) (+ x y))))
                          (declare (type (signed-byte 29) result))
                          (cond ((>= result (i-max)) -1)
                                (t (the (signed-byte 28) result)))))))))

     (defmacro imin (x y)
       `(the (signed-byte 28)
             (let ((x ,x)
                   (y ,y))
               (declare (type (signed-byte 28) x y))
               (cond ((< x 0)
                      (cond ((< y 0) -1)
                            (t y)))
                     ((< y 0)
                      x)
                     (t
                      (the (signed-byte 28) (min x y)))))))

     (defun big-test (x y z)
       (declare (type (signed-byte 28) x y z))
       (imin (i+ x y)
             (i+ y (imin x z))))

GET-WORMHOLE-STATUS    make a wormhole's status visible outside the wormhole

General Form: (get-wormhole-status name state)

Name should be the name of a wormhole (see WORMHOLE).  This
function returns an error triple (see ERROR-TRIPLES) of the form
(mv nil s state), where s is the status of the named wormhole.  The
status is obtained by reading the oracle in the ACL2 state.

This function makes the status of a wormhole visible outside the
wormhole.  But since this function takes state and modifies it, the
function may only be used in contexts in which you may change state.
Otherwise, the wormhole status may stay in the wormhole.  See
wormhole-eval and wormhole.

GOAL-SPEC    to indicate where a hint is to be used

     Examples:
     "Goal"
     "goal"
     "Subgoal *1/3''"
     "subgoal *1/3''"
     "[2]Subgoal *1/3''"

When hints are given to the theorem prover, a goal-spec is provided to
specify the goal to which the hints are to be applied.  The hints
provided are carried along innocuously until the named goal arises.
When it arises, the hints are "activated" for that goal and its
descendents.

A legal goal specification may be extracted from the theorem prover's
output.  Certain lines clearly label formulas, as in

     Subgoal *1/3.2'
     (IMPLIES ... ...)

and these lines all give rise to goal specifications.  In general,
these lines all start either with "Goal" or "Subgoal" or else with
those words preceded by a number in square brackets, as in

     [1]Subgoal *1/3.2'
     (IMPLIES ... ...).

A goal specification may be obtained by deleting any surrounding
whitespace from such a line and embedding the text in string quotation
marks.  Thus

     "[1]Subgoal *1/3.2'"

is the goal specifier for the goal above.

As noted, a hint is applied to a goal when the hint's goal
specification matches the name ACL2 assigns to the goal.  The matching
algorithm is case-insensitive.  Thus, alternative goal specifications
for the goal above are "[1]subgoal *1/3.2'" and "[1]SUBGOAL *1/3.2'".
The matching algorithm does not tolerate non-case discrepancies.  Thus,
"[1]Subgoal*1/3.2'" and " [1]Subgoal *1/3.2'" are unacceptable.

Sometimes a formula is given two names, e.g.,

     Subgoal *1/14.2'
     (IMPLIES ...
              ...)
     Name the formula above *1.1.

It is the first name (the one that starts with "Goal" or "Subgoal") and
not the second which constitutes a legal goal-spec.  Roughly speaking,
when the system prints the line containing the goal specification, it
activates any hints that are attached to that goal-spec.  Consider the
example above.  Suppose Subgoal *1/14.2' could be proved by using a
certain lemma instance.  Then the appropriate entry in the hints would
be:

     ("Subgoal *1/14.2'" :use ...)

This might surprise you because the system appears to do nothing to
*1/14.2' besides push it for a subsequent induction.  But actually
between the time the system printed the goal-spec line and the time it
decides to push the goal, you can think of the system as trying
everything it has.  So a use hint activated when Subgoal *1/14.2'
arises is just what you want.

But what if you want to give an :induct hint?  By the time induction is
tried, the formula has been given the name *1.1.  Well, this is one you
just have to remember:

     ("Subgoal *1/14.2'" :induct ...).

When the above hint is activated the :induct directive short-circuits
the rest of the processing and sends immediately the formula into the
pool of goals to prove by induction.  The induct hint is attached to
the formula in the pool and when the time comes to turn our attention
to that goal, the induct advice is followed.

We conclude by emphasizing a point made above, that a hint is applied
to a goal when the hint's goal specification matches the name ACL2
assigns to the goal.  If there is no such match, then the hint is
ignored.  Consider the following example.

     (thm (equal (append (append x y) z) (append x y z))
          :hints (("Subgoal *1/" :in-theory nil)))

Normally, :in-theory hints are inherited by subgoals (see
HINTS-AND-THE-WATERFALL), so you might expect that the empty theory is
used in Subgoal *1/2 and Subgoal *1/1.  But in fact, since there is no
subgoal printed that is labeled Subgoal *1/, the above :in-theory hint
is ignored.  The above example is in contrast to the following, where
the hint makes the proof fail, because there really is a Subgoal *1/ in
the proof this time.

     (thm (implies (and (not (endp x)) (not (endp (cdr x))))
                   (equal (append (append x y) z) (append x y z)))
          :hints (("Subgoal *1/" :in-theory nil)))

GUARD    restricting the domain of a function

The ACL2 system provides a mechanism for restricting a function to a
particular domain.  Such restrictions are called "guards."  A
definition's guard has no effect on the logical axiom added when that
definition is accepted by ACL2, and novices are often best served by
avoiding guards.  However, guards can be useful as a specification
device or for increasing execution efficiency.  To make such a
restriction, use the :guard keyword (see XARGS) or, especially
if you want the host Lisp compiler to use this information, use type
declarations (see DECLARE).  The general issue of guards and
guard verification is discussed in the topics listed below.

Related topics other than immediate subtopics:

To begin further discussion of guards, see GUARD-INTRODUCTION.
That section directs the reader to further sections for more details.
To see just a summary of some commands related to guards, see
GUARD-QUICK-REFERENCE.  For a discussion of the use of proof to verify
the absence of guard violations, see VERIFY-GUARDS.

EXTRA-INFO    generate markers to indicate sources of guard proof obligations

See GUARD-DEBUG for a discussion of this function, which is
useful for debugging failures during guard verification.

GUARD-DEBUG    generate markers to indicate sources of guard proof obligations

ACL2 guard verification (see GUARD) is often best avoided by
beginning users of ACL2.  When guard verification is employed, it can
generate numerous goals, some of which may not be theorems if the
definition being processed has bugs.  It can be difficult to find such
bugs.  This documentation topic explains a capability provided by ACL2
to help find such bugs.

We begin with the following example.  Although it is contrived and a bit
simplistic, it illustrates how the guard-debug utility works.

     (defun length-repeat (x)
       (length (append x x)))
     (verify-guards length-repeat :guard-debug t)

The output produces two top-level key checkpoints, as follows.

     Subgoal 2
     (IMPLIES (EXTRA-INFO '(:GUARD (:BODY LENGTH-REPEAT))
                          '(APPEND X X))
              (TRUE-LISTP X))

     Subgoal 1
     (IMPLIES (AND (EXTRA-INFO '(:GUARD (:BODY LENGTH-REPEAT))
                               '(LENGTH (APPEND X X)))
                   (NOT (TRUE-LISTP (APPEND X X))))
              (STRINGP (APPEND X X)))

The upper subgoal (numbered 2) says that the body of the definition of
length-repeat contains a call (APPEND X X), which is the source of the
goal.  In this case, that makes sense: the guard for a call (append
arg1 arg2) is (true-listp arg1), which in this case is (TRUE-LISTP X).
The lower subgoal (numbered 1) says that the same definition contains
the call (LENGTH (APPEND X X)), which generates the proof obligation
that if (APPEND X X) does not satisfy true-listp, then it must satisfy
stringp.  That proof obligation comes directly from the guard for
length.

Of course, the example above is a bit obvious.  But for large
definitional bodies such information can be very helpful.  Note that
guard-debug can be specified not only in verify-guards events but also
in xargs declare forms of defun events.

We now describe the guard-debug utility in some detail.

(Extra-info x y) always returns t by definition.  However, if guard
verification takes place with a non-nil setting of guard-debug (see
below), then the goals generated for guard verification can include
hypotheses that are calls of extra-info.  Typically, such a hypothesis
is of the following form:

     (extra-info '(:guard (:body F))
                 '(G ARG1 ... ARGk))

The above form indicates that the goal in which it occurs was generated
to verify that the guard of the function F is satisfied by the
arguments ARG1 through ARGk, where the term (G ARG1 ... ARGk) occurs in
the body of the function F whose guard verification is in progress.  If
however the above call of G occurs in the guard of F instead of the
body of F, then :body is replaced by :guard above:

     (extra-info '(:guard (:guard F))
                 '(G ARG1 ... ARGk))

If the same proof obligation (goal clause) arises from more than one
occurrence of the same call, then a single goal will be generated,
which has several extra-info hypotheses added to show the multiple
sources of that proof obligation.

All rules (see RUNE) associated with extra-info are disabled by
default, so that hypotheses of the form described above are not
simplified to t.  These hypotheses are intended to ride along for free:
you can generally expect the proof to have the same structure whether
or not the :guard-debug option is supplied, though on rare occasions
the proofs may diverge.

It remains to explain the notion of a guard-debug setting of t, that
is, to explain how to obtain the additional hypotheses described above.
If guards are being verified during processing of a defun event (whether
or not inside a call of mutual-recursion), then one specifies
:guard-debug t in an xargs declaration of a declare form; see
XARGS.  If however the guard verification is on behalf of a
verify-guards call, whether for a definition or a theorem, then one
specifies the keyword argument :guard-debug t.

Also see PRINT-GV for a utility for debugging guard violations,
in contrast to the above guard-debug mechanism, which is for debugging
failed proofs arising from guard verification.

GUARD-EVALUATION-EXAMPLES-LOG    log showing combinations of defun-modes and guard-checking

See GUARD-EVALUATION-EXAMPLES-SCRIPT for a script that shows
the interaction of defun-modes with the value set by
set-guard-checking.  Here, we present a log resulting from running this
script.

See SET-GUARD-CHECKING for discussion of the interaction between
defun-modes and guard-checking that is illustrated by this script.
Also see GUARD-EVALUATION-TABLE for a succinct table, with
associated discussion, that covers in detail the interactions
illustrated here.

     ACL2 !>(defun fact (x)
              (declare (xargs :guard (integerp x)
                              :mode :program))
              (if (posp x)
                  (* x (fact (1- x)))
                1))

     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)
      ((FACT))
     ACL2 !>:set-guard-checking t

     Guard-checking-on already has value T.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)

     ACL2 Error in TOP-LEVEL:  The guard for the :program function symbol
     FACT, which is (INTEGERP X), is violated by the arguments in the call
     (FACT T).  See :DOC trace for a useful debugging utility.  See :DOC
     set-guard-checking for information about suppressing this check with
     (set-guard-checking :none), as recommended for new users.

     ACL2 !>:set-guard-checking :all

     Leaving guard checking on, but changing value to :ALL.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)

     ACL2 Error in TOP-LEVEL:  The guard for the :program function symbol
     FACT, which is (INTEGERP X), is violated by the arguments in the call
     (FACT T).  See :DOC trace for a useful debugging utility.  See :DOC
     set-guard-checking for information about suppressing this check with
     (set-guard-checking :none), as recommended for new users.

     ACL2 !>:set-guard-checking :none

     Turning off guard checking entirely.  To allow execution in raw Lisp
     for functions with guards other than T, while continuing to mask guard
     violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:set-guard-checking nil

     Masking guard violations but still checking guards except for self-
     recursive calls.  To avoid guard checking entirely, :SET-GUARD-CHECKING
     :NONE.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
       2> (FACT T)
       <2 (FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:u

               0:x(EXIT-BOOT-STRAP-MODE)
     ACL2 >(defun fact (x)
              (declare (xargs :guard t
                              :mode :program))
              (if (posp x)
                  (* x (fact (1- x)))
                1))

     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)
      ((FACT))
     ACL2 >:set-guard-checking t

     Turning guard checking on, value T.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
       2> (FACT T)
       <2 (FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 !>:set-guard-checking :all

     Leaving guard checking on, but changing value to :ALL.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 !>:set-guard-checking :none

     Turning off guard checking entirely.  To allow execution in raw Lisp
     for functions with guards other than T, while continuing to mask guard
     violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:set-guard-checking nil

     Masking guard violations but still checking guards except for self-
     recursive calls.  To avoid guard checking entirely, :SET-GUARD-CHECKING
     :NONE.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
       2> (FACT T)
       <2 (FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:u

               0:x(EXIT-BOOT-STRAP-MODE)
     ACL2 >(defun fact (x)
              (declare (xargs :guard (integerp x)
                              :verify-guards nil
                              :mode :logic))
              (if (posp x)
                  (* x (fact (1- x)))
                1))

     For the admission of FACT we will use the relation O< (which is known
     to be well-founded on the domain recognized by O-P) and the measure
     (ACL2-COUNT X).  The non-trivial part of the measure conjecture is

     [[output omitted here]]

     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FACT
     ACL2 >(trace$ fact)
      ((FACT))
     ACL2 >:set-guard-checking t

     Turning guard checking on, value T.

     ACL2 !>(fact 2)
     [[Comment added to the log:
       Normally you would get a message about guard-checking being
       inhibited on recursive calls.  However, when a function is
       traced the guard-checking is done on recursive calls unless
       the guards have been verified (see :DOC verify-guards).
     ]]
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol FACT, which
     is (INTEGERP X), is violated by the arguments in the call (FACT T).
     See :DOC trace for a useful debugging utility.  See :DOC set-guard-
     checking for information about suppressing this check with (set-guard-
     checking :none), as recommended for new users.

     ACL2 !>:set-guard-checking :all

     Leaving guard checking on, but changing value to :ALL.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol FACT, which
     is (INTEGERP X), is violated by the arguments in the call (FACT T).
     See :DOC trace for a useful debugging utility.  See :DOC set-guard-
     checking for information about suppressing this check with (set-guard-
     checking :none), as recommended for new users.

     ACL2 !>:set-guard-checking :none

     Turning off guard checking entirely.  To allow execution in raw Lisp
     for functions with guards other than T, while continuing to mask guard
     violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:set-guard-checking nil

     Masking guard violations but still checking guards except for self-
     recursive calls.  To avoid guard checking entirely, :SET-GUARD-CHECKING
     :NONE.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     [[Comment added to the log:
       In spite of the warning above, guards are checked here on
       self-recursive calls, because the function is traced.
     ]]
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >(verify-guards fact)

     Computing the guard conjecture for FACT....

     The guard conjecture for FACT is trivial to prove, given the :compound-
     recognizer rule POSP-COMPOUND-RECOGNIZER, primitive type reasoning
     and the :type-prescription rule FACT.  FACT is compliant with Common
     Lisp.

     Summary
     Form:  ( VERIFY-GUARDS FACT)
     Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER)
             (:FAKE-RUNE-FOR-TYPE-SET NIL)
             (:TYPE-PRESCRIPTION FACT))
     Warnings:  None
     Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
      FACT
     ACL2 >(trace$ fact)
      ((FACT))
     ACL2 >:set-guard-checking t

     Turning guard checking on, value T.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol FACT, which
     is (INTEGERP X), is violated by the arguments in the call (FACT T).
     See :DOC trace for a useful debugging utility.  See :DOC set-guard-
     checking for information about suppressing this check with (set-guard-
     checking :none), as recommended for new users.

     ACL2 !>:set-guard-checking :all

     Leaving guard checking on, but changing value to :ALL.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol FACT, which
     is (INTEGERP X), is violated by the arguments in the call (FACT T).
     See :DOC trace for a useful debugging utility.  See :DOC set-guard-
     checking for information about suppressing this check with (set-guard-
     checking :none), as recommended for new users.

     ACL2 !>:set-guard-checking :none

     Turning off guard checking entirely.  To allow execution in raw Lisp
     for functions with guards other than T, while continuing to mask guard
     violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:set-guard-checking nil

     Masking guard violations but still checking guards except for self-
     recursive calls.  To avoid guard checking entirely, :SET-GUARD-CHECKING
     :NONE.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:u
      L        1:x(DEFUN FACT (X) ...)
     ACL2 >:u
               0:x(EXIT-BOOT-STRAP-MODE)
     ACL2 >(defun fact (x)
              (declare (xargs :guard (integerp x)
                              :mode :logic))
              (if (posp x)
                  (* x (fact (1- x)))
                1))

     For the admission of FACT we will use the relation O< (which is known
     to be well-founded on the domain recognized by O-P) and the measure
     (ACL2-COUNT X).  The non-trivial part of the measure conjecture is

     [[output omitted here]]

     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FACT
     ACL2 >(trace$ fact)
      ((FACT))
     ACL2 >:set-guard-checking t

     Turning guard checking on, value T.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol FACT, which
     is (INTEGERP X), is violated by the arguments in the call (FACT T).
     See :DOC trace for a useful debugging utility.  See :DOC set-guard-
     checking for information about suppressing this check with (set-guard-
     checking :none), as recommended for new users.

     ACL2 !>:set-guard-checking :all

     Leaving guard checking on, but changing value to :ALL.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)

     ACL2 Error in TOP-LEVEL:  The guard for the function symbol FACT, which
     is (INTEGERP X), is violated by the arguments in the call (FACT T).
     See :DOC trace for a useful debugging utility.  See :DOC set-guard-
     checking for information about suppressing this check with (set-guard-
     checking :none), as recommended for new users.

     ACL2 !>:set-guard-checking :none

     Turning off guard checking entirely.  To allow execution in raw Lisp
     for functions with guards other than T, while continuing to mask guard
     violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:set-guard-checking nil

     Masking guard violations but still checking guards except for self-
     recursive calls.  To avoid guard checking entirely, :SET-GUARD-CHECKING
     :NONE.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:u
               0:x(EXIT-BOOT-STRAP-MODE)
     ACL2 >(defun fact (x)
              (declare (xargs :guard t
                              :verify-guards nil
                              :mode :logic))
              (if (posp x)
                  (* x (fact (1- x)))
                1))

     For the admission of FACT we will use the relation O< (which is known
     to be well-founded on the domain recognized by O-P) and the measure
     (ACL2-COUNT X).  The non-trivial part of the measure conjecture is

     [[output omitted here]]

     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FACT
     ACL2 >(trace$ fact)
      ((FACT))
     ACL2 >:set-guard-checking t

     Turning guard checking on, value T.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 !>:set-guard-checking :all

     Leaving guard checking on, but changing value to :ALL.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 !>:set-guard-checking :none

     Turning off guard checking entirely.  To allow execution in raw Lisp
     for functions with guards other than T, while continuing to mask guard
     violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:set-guard-checking nil

     Masking guard violations but still checking guards except for self-
     recursive calls.  To avoid guard checking entirely, :SET-GUARD-CHECKING
     :NONE.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (ACL2_*1*_ACL2::FACT 1)
         3> (ACL2_*1*_ACL2::FACT 0)
         <3 (ACL2_*1*_ACL2::FACT 1)
       <2 (ACL2_*1*_ACL2::FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >(verify-guards fact)

     Computing the guard conjecture for FACT....

     The guard conjecture for FACT is trivial to prove, given the :compound-
     recognizer rule POSP-COMPOUND-RECOGNIZER and the :type-prescription
     rule FACT.  FACT is compliant with Common Lisp.

     Summary
     Form:  ( VERIFY-GUARDS FACT)
     Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER)
             (:TYPE-PRESCRIPTION FACT))
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FACT

     [[Note added to log: No need to trace fact again after verify-guards.]]

     ACL2 >:set-guard-checking t

     Turning guard checking on, value T.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
       2> (FACT T)
       <2 (FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 !>:set-guard-checking :all

     Leaving guard checking on, but changing value to :ALL.

     ACL2 !>(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 !>(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
       2> (FACT T)
       <2 (FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 !>:set-guard-checking :none

     Turning off guard checking entirely.  To allow execution in raw Lisp
     for functions with guards other than T, while continuing to mask guard
     violations, :SET-GUARD-CHECKING NIL.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
       2> (FACT T)
       <2 (FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >:set-guard-checking nil

     Masking guard violations but still checking guards except for self-
     recursive calls.  To avoid guard checking entirely, :SET-GUARD-CHECKING
     :NONE.  See :DOC set-guard-checking.

     ACL2 >(fact 2)
     1> (ACL2_*1*_ACL2::FACT 2)
       2> (FACT 2)
         3> (FACT 1)
           4> (FACT 0)
           <4 (FACT 1)
         <3 (FACT 1)
       <2 (FACT 2)
     <1 (ACL2_*1*_ACL2::FACT 2)
     2
     ACL2 >(fact t)
     1> (ACL2_*1*_ACL2::FACT T)
       2> (FACT T)
       <2 (FACT 1)
     <1 (ACL2_*1*_ACL2::FACT 1)
     1
     ACL2 >

GUARD-EVALUATION-EXAMPLES-SCRIPT    a script to show combinations of defun-modes and guard-checking

Below is a script that illustrates the combination of defun-modes --
:program mode, :logic mode without guards verified, and :logic mode
with guards verified -- with values from set-guard-checking -- t (the
default), :all, :none, and nil.  (It does not illustrate the value
:nowarn, which is the same as t except for inhibiting a warning.)  The
script also illustrates cases where the guard is not, or is, t.

See GUARD-EVALUATION-EXAMPLES-LOG for result of running this
script.  Before presenting the script below, we give some instructions
in case you want to run it yourself.

See SET-GUARD-CHECKING for discussion of the interaction between
defun-modes and guard-checking that is illustrated by this script.
Also see GUARD-EVALUATION-TABLE for a succinct table, with
associated discussion, that covers in detail the interactions
illustrated here.

The script mentions the running of "Tracing Code".  The code is the
following sequence of commands.

     (trace$ fact)
     :set-guard-checking t
     (fact 2)
     (fact t)
     :set-guard-checking :all
     (fact 2)
     (fact t)
     :set-guard-checking :none
     (fact 2)
     (fact t)
     :set-guard-checking nil
     (fact 2)
     (fact t)

If you want to run the script yourself, you may find it handy to use the
following Emacs keyboard macro for running the tracing code in 2-window
mode, with the cursor in the window with the script and ACL2 running in
the other window.

     (fset 'step-guard-script
        [?C-a ?C-  ?C-e ?M-w ?C-a ?C-n
         ?C-x ?o ?M-> ?C-y return ?C-x ?o])

     ; Put it on a key (if you have defined the indicated keymap by using
     ; emacs/emacs-acl2.el):
     (define-key ctl-t-keymap "r" 'step-guard-script)

The script follows.

     ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
     ;;; Program mode
     ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

     (defun fact (x)
              (declare (xargs :guard (integerp x)
                              :mode :program))
              (if (posp x)
                  (* x (fact (1- x)))
                1))

     ; Run the Tracing Code here.  It shows execution in raw Lisp in the t and nil
     ; cases of :set-guard-checking, but not in the :all or :none cases.  We get a
     ; guard violation for argument t in the case :set-guard-checking t.

     :u

     (defun fact (x)
              (declare (xargs :guard t
                              :mode :program))
              (if (posp x)
                  (* x (fact (1- x)))
                1))

     ; Run the Tracing Code here.  It should give the same results as above,
     ; except that we no longer get a guard violation in the case
     ; :set-guard-checking t.

     :u

     ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
     ;;; Logic mode, guard other than t
     ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

     (defun fact (x)
              (declare (xargs :guard (integerp x)
                              :verify-guards nil
                              :mode :logic))
              (if (posp x)
                  (* x (fact (1- x)))
                1))

     ; Run the Tracing Code here.  It should give guard violations for (fact t)
     ; with guard-checking set to t or :all.  It should never run in raw Lisp,
     ; because we have not verified guards.  In the t case, we can get a warning
     ; about avoiding the guard check on recursive calls, but only if we do not
     ; trace the function, fact.

     (verify-guards fact)

     ; Run the Tracing Code here.  The results should be as described just above,
     ; except that now we go into raw Lisp for (fact 2) with guard-checking other
     ; than :none.

     :u
     :u

     ; The following definition is the same as above, except that guards are
     ; verified.

     (defun fact (x)
              (declare (xargs :guard (integerp x)
                              :mode :logic))
              (if (posp x)
                  (* x (fact (1- x)))
                1))

     ; Run the Tracing Code here.  We should get the same traces as in the
     ; immediately preceding case, since guards had been verified in both cases.

     :u

     ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
     ;;; Logic mode, guard t
     ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

     (defun fact (x)
              (declare (xargs :guard t
                              :verify-guards nil
                              :mode :logic))
              (if (posp x)
                  (* x (fact (1- x)))
                1))

     ; Run the Tracing Code here.  We should never go in to raw Lisp, because
     ; guards have not been verified.  We will see the same traces for (fact 2) as
     ; with the (integerp x) guard above with :verify-guards nil specified, except
     ; that even without tracing, there is no warning for :set-guard-checking t
     ; about recursive calls.  And, there are no guard violations for (fact t), of
     ; course, since posp (necessarily, if we are to verify guards) has a guard of
     ; t.

     (verify-guards fact)

     ; Run the Tracing Code here.  You shouldn't see any surprises.  Note however
     ; that if we back up to the start (using :u :u) and then define fact as just
     ; above but without :verify-guards nil, then the :none setting will allow us
     ; to go into raw Lisp: although :none generally avoids execution of raw Lisp
     ; counterparts, it allows this when the guard is T and guards have been
     ; verified.

GUARD-EVALUATION-TABLE    a table that shows combinations of defun-modes and guard-checking

See SET-GUARD-CHECKING for an introduction to the topic
discussed here.  Also see GUARD for a general discussion of
guards, and see GUARD-EVALUATION-EXAMPLES-SCRIPT for a script
that illustrates combinations presented below.

Note: The default setting for guard-checking (that is, the initial
value for (@ guard-checking-on)) is T.

The table below illustrates the interaction of the defun-mode with the
value supplied to set-guard-checking.  The first row considers
functions defined in :program mode; the other two consider functions
defined in :logic mode.  The columns correspond to four values of state
global 'guard-checking-on, as supplied to set-guard-checking.  (A fifth
value, :nowarn, is similar to t but suppresses warnings encountered
with t (as explained in those warning messages), and is not considered
here.)  During proofs, 'guard-checking-on is set to nil regardless of
how this variable has been set in the top-level loop.

Below this table, we make some comments about its entries, ordered by
row and then by column.  For example, when we refer to "b2" we are
discussing the execution of a :logic mode function whose guards have
not been verified, after having executed :set-guard-checking :all.

        guard-checking-on:  (1)t      (2):all   (3):none   (4)nil

      (a) :program             a1        a2        a3        a4
      (b) guards not verified  b1        b2        b3        b4
      (c) guards verified      c1        c2        c3        c4

a1. Check the guard upon entry, then use the raw Lisp code if the guard
checks (else cause an error).  This is a common setting when one wants a
little guard checking but also wants the efficiency of raw Lisp.  But
note that you can get raw Lisp errors.  For example, if you make the
definition (defun foo (x) (car x)) in :program mode and execute
:set-guard-checking t, and then execute (foo 3), you will likely get an
error from the call (car 3) made in raw Lisp.

a2. For built-in (predefined) functions, see a1 instead.  Otherwise:
Check the guard, without exception.  Thus, we never run the raw Lisp
code in this case.  This can be useful when testing :program mode
functions, but you may want to run :comp t or at least :comp :exec in
this case, so that the execution is done using compiled code.

a3. For built-in (predefined) functions, see a4 instead.  Otherwise:
Do not check the guard.  For :program mode functions, we never run the
raw Lisp code in this case; so if you care about efficiency, see the
comment in a2 above about :comp.  This combination is useful if you are
using ACL2 as a programming language and do not want to prove theorems
about your functions or suffer guard violations.  In this case, you can
forget about any connection between ACL2 and Common Lisp.

a4. Run the raw Lisp code without checking guards at all.  Thus, for
:program mode functions, the nil setting is often preferable to the
:none setting because you get the efficiency of raw Lisp execution.
However, with nil you can therefore get hard Lisp errors as in a1 above.

b1. Guards are checked at the top-level, though not at self-recursive
calls.  We never run the raw Lisp code in this case; guards would need
to be verified first.

b2. Unlike the t setting, guards are checked even on self-recursive
calls.  But like the t setting, we do not run the raw Lisp code.  Use
this setting if you want guards checked on each recursive call in spite
of the cost of doing so.

b3, b4. Execution avoids the raw Lisp code and never checks guards.  The
nil and :none settings behave the same in this case (i.e., for :logic
mode functions whose guards have not been verified), except that
recursive calls are never inlined for :none and tracing (see
TRACE) will show recursive calls for :none but not for nil.

c1, c2. Guards are checked.  If the checks pass, evaluation takes place
using the raw Lisp code.  If the checks fail, we get a guard violation.
Either way, we do not execute "in the logic"; we only execute using the
raw Lisp code.  Note that t and :all behave the same in this case,
(i.e. for :logic mode functions whose guards have been verified).

c3, c4. For the :none and nil settings, :logic mode functions whose
guards have been verified will never cause guard violations.  However,
with nil and for built-in functions in :logic mode, guards are still
checked: if the check succeeds, then evaluation is done using the raw
Lisp code, and if not, it is done by the "logic" code, including
self-recursive calls (though unlike the t case, we will not see a
warning about this).  But with :none for user-defined functions, no
guard checking is done, and the only time the raw Lisp code will be
executed is when the guard is t and guards are verified at the time the
executable counterpart of the function is defined (i.e., when the
function is admitted unless it is later defined again and compiled
using :comp).  Thus, if you use :none and you want a function (foo x)
with guard (g x) to execute using raw Lisp code, you can write a
"wrapper"function with a guard of t:

     (defun foo-wrap (x)
       (declare (xargs :guard t))
       (if (g x)
           (foo x)
         'do-not-case))

If you want the speed of executing raw Lisp code and you have
non-trivial guards on functions that you want to call at the top-level,
use nil rather than :none.

GUARD-INTRODUCTION    introduction to guards in ACL2

Most users can probably profit by avoiding dealing with guards most of
the time.  If they seem to get in the way, they can be "turned off"
using the command :set-guard-checking nil; for more about this, see
SET-GUARD-CHECKING.  For more about guards in general, see
GUARD.

The guard on a function symbol is a formula about the formals of the
function.  To see the guard on a function, use the keyword command
:args.  See ARGS.  To specify the guard on a function at
defun-time, use the :guard xarg (See XARGS) or type
declarations (see DECLARE).  The latter may be preferable if
you want the host Lisp compiler to use this information.

Guards can be seen as having either of two roles: (a) they are a
specification device allowing you to characterize the kinds of inputs a
function "should" have, or (b) they are an efficiency device allowing
logically defined functions to be executed directly in Common Lisp.
Briefly:  If the guards of a function definition are "verified" (see
VERIFY-GUARDS), then the evaluation of a call of that function
on arguments satisfying its guard will have the following property:

     All subsequent function calls during that evaluation will be on
     arguments satisfying the guard of the called function.

The consequence of this fact for (a) is that your specification
function is well-formed, in the sense that the values returned by this
function on appropriate arguments only depend on the restrictions of
the called functions to their intended domains.  The consequence of
this fact for (b) is that in the ACL2 system, when a function whose
guards have been verified is called on arguments that satisfy its
guard, then the raw lisp function defined by this function's defun
event is used to evaluate the call.  Note however that even when the
user-supplied defun is not used, ACL2 uses a corresponding "executable
counterpart" that generally performs, we expect, nearly as well as the
raw lisp function.  See COMP to see how compilation can speed
up both kinds of execution.

Let us turn next to the issue of the relationship between guards and
evaluation.  See GUARDS-AND-EVALUATION.

GUARD-MISCELLANY    miscellaneous remarks about guards

The discussion of guards concludes here with a few miscellaneous
remarks.  (Presumably you found this documentation by following a link;
see GUARDS-FOR-SPECIFICATION.)  For further information related
to guards other than what you find under "guard," see any of the
following documentation topics:  guard-example,
set-verify-guards-eagerness, set-guard-checking, and verify-guards.

Defun can be made to try to verify the guards on a function.  This is
controlled by the "defun-mode" of the defun; see DEFUN-MODE.
The defun-mode is either as specified with the :mode xarg of the defun
or else defaults to the default defun-mode.  See
DEFAULT-DEFUN-MODE.  If the defun-mode of the defun is :logic and
either a guard is specified explicitly or :verify-guards t is specified
in the xargs, then we attempt to verify the guards of the function.
Otherwise we do not.  (But see SET-VERIFY-GUARDS-EAGERNESS for
how to modify this behavior.)

It is sometimes impossible for the system to verify the guards of a
recursive function at definition time.  For example, the guard
conjectures might require the invention and proof of some inductively
derived property of the function (as often happens when the value of a
recursive call is fed to a guarded subroutine).  So sometimes it is
necessary to define the function using :verify-guards nil then to state
and prove key theorems about the function, and only then have the
system attempt guard verification.  Post-defun guard verification is
achieved via the event verify-guards.  See VERIFY-GUARDS.

It should be emphasized that guard verification affects only two
things: how fast ACL2 can evaluate the function and whether the
function is executed correctly by raw Common Lisp, without guard
violations.  Since ACL2 does not use the raw Common Lisp definition of
a function to evaluate its calls unless that function's guards have
been verified, the latter effect is felt only if you run functions in
raw Common Lisp rather than via ACL2's command loop.

Guard verification does not otherwise affect the theorem prover or the
semantics of a definition.  If you are not planning on running your
function on "big" inputs and you don't care if your function runs
correctly in raw Common Lisp (e.g., you have formalized some abstract
mathematical property and just happened to use ACL2 as your language),
there is no need to suffer through guard verification.  Often users
start by not doing guard verification and address that problem later.
Sometimes you are driven to it, even in mathematical projects, because
you find that you want to run your functions particularly fast or in
raw Common Lisp.

If certify-book is used to compile a file, and the file contains
functions with unverified guard conjectures, then you will be warned
that the compiled file cannot be loaded into raw Common Lisp with the
expectation that the functions will run correctly.  This is just the
same point we have been making:  ACL2 and Common Lisp agree only on the
restricted domains specified by our guards.  When guards are violated,
Common Lisp can do anything.  When you call a compiled function on
arguments violating its guards, the chances are only increased that
Common Lisp will go berserk, because compiled functions generally check
fewer things at runtime and tend to be more fragile than interpreted
ones.

Finally, we note that ACL2 collects up guards from declare forms in
order of appearance.  So for example, the declare form

     (declare (xargs :guard (foo x))
              (type string x)

will generate the guard (and (foo x) (stringp x)), while the form

     (declare (type string x)
              (xargs :guard (foo x))

will generate the guard (and (stringp x) (foo x)).  The only exception
to this rule is the case that :guard and :stobjs are specified in the
same xargs form, in which case the :stobjs form will be treated as
through it comes before the :guard form.

GUARD-QUICK-REFERENCE    brief summary of guard checking and guard verification

For a careful introduction to guards, see GUARD.

I. GUARD CHECKING DURING EXECUTION

_Effect_

Guards on definitions are checked at execution time (except for guards
on subsidiary calls of recursive or mutually recursive functions).

_When does it happen_

By default, guards are checked for all forms submitted at the top level.

_To disable_
:set-guard-checking nil   ; skip raw Lisp if there is a guard violation
:set-guard-checking :none ; skip guard checking entirely

_To (re-)enable_
:set-guard-checking t

See SET-GUARD-CHECKING for more options.

II. GUARD VERIFICATION

_Effect_

A proof is attempted of the obligations arising from the guards of
subsidiary functions in a defun, defthm, or defaxiom event.  In the
case of a defun, the guard itself is also verified (under an implicit
guard of t).

_When does it happen_

Only names of defined functions, defthms, and defaxioms are subject to
guard verification.  Guard verification may occur when functions are
defined (using defun), but it requires an explicit call of
verify-guards in order to verify guards for defthms and defaxioms.
Constrained functions (see ENCAPSULATE) may not have their
guards verified.

(verify-guards foo ...)
causes guard verification for the defun, defthm, or defaxiom named by
foo, if it has not already been successfully done.  The default
defun-mode (see DEFAULT-DEFUN-MODE) must be :logic, or else
this event is ignored.

(defun foo ...)
causes guard verification of foo if and only if the following two
conditions are both met.  First, foo is processed in :logic mode
(either by setting mode :logic globally, or by including :mode :logic
in the xargs declaration).  Second, at least one of the following
sub-conditions is met.  Also see XARGS, and see
SET-VERIFY-GUARDS-EAGERNESS for how to change this behavior.

     1. The xargs declaration specifies a :guard.

     2. There is at least one type declaration (see DECLARE).

     3. The xargs declaration specifies :stobjs.

     4. The xargs declaration specifies :verify-guards t.

(verify-termination foo ...)
causes guard verification of foo if foo is a function currently defined
in :program mode and the criteria for guard verification of a defun
form are met, as discussed above.  The default defun-mode (see
DEFAULT-DEFUN-MODE) must be :logic, or else this event is ignored.