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

BRR@    to access context sensitive information within break-rewrite

     Example:
     (brr@ :target)      ; the term being rewritten
     (brr@ :unify-subst) ; the unifying substitution

     General Form:
     (brr@ :symbol)

where :symbol is one of the following keywords.  Those marked with *
probably require an implementor's knowledge of the system to use
effectively.  They are supported but not well documented.  More is said
on this topic following the table.

     :symbol             (brr@ :symbol)
     -------             ---------------------

     :target             the term to be rewritten.  This term is an
                         instantiation of the left-hand side of the
                         conclusion of the rewrite-rule being broken.
                         This term is in translated form!  Thus, if
                         you are expecting (equal x nil) -- and your
                         expectation is almost right -- you will see
                         (equal x 'nil); similarly, instead of (cadr a)
                         you will see (car (cdr a)).  In translated
                         forms, all constants are quoted (even nil, t,
                         strings and numbers) and all macros are
                         expanded.

     :unify-subst        the substitution that, when applied to :target,
                         produces the left-hand side of the rule being
                         broken.  This substitution is an alist pairing
                         variable symbols to translated (!) terms.

     :wonp               t or nil indicating whether the rune was
                         successfully applied.  (brr@ :wonp) returns
                         nil if evaluated before :EVALing the rule.

     :rewritten-rhs      the result of successfully applying the rule
                         or else nil if (brr@ :wonp) is nil.  The result
                         of successfully applying the rule is always a
                         translated (!) term and is never nil.

     :failure-reason     some non-nil lisp object indicating why the rule
                         was not applied or else nil.  Before the rule is
                         :EVALed, (brr@ :failure-reason) is nil.  After
                         :EVALing the rule, (brr@ :failure-reason) is nil
                         if (brr@ :wonp) is t.  Rather than document the
                         various non-nil objects returned as the failure
                         reason, we encourage you simply to evaluate
                         (brr@ :failure-reason) in the contexts of interest.
                         Alternatively, study the ACL2 function tilde-@-
                         failure-reason-phrase.

     :lemma           *  the rewrite rule being broken.  For example,
                         (access rewrite-rule (brr@ :lemma) :lhs) will
                         return the left-hand side of the conclusion
                         of the rule.

     :type-alist      *  a display of the type-alist governing :target.
                         Elements on the displayed list are of the form
                         (term type), where term is a term and type
                         describes information about term assumed to hold
                         in the current context.  The type-alist may be
                         used to determine the current assumptions, e.g.,
                         whether A is a CONSP.

     :ancestors       *  a stack of frames indicating the backchain history
                         of the current context.  The theorem prover is in
                         the process of trying to establish each hypothesis
                         in this stack.  Thus, the negation of each hypothesis
                         can be assumed false.  Each frame also records the
                         rules on behalf of which this backchaining is being
                         done and the weight (function symbol count) of the
                         hypothesis.  All three items are involved in the
                         heuristic for preventing infinite backchaining.
                         Exception:  Some frames are ``binding hypotheses''
                         (equal var term) or (equiv var (double-rewrite term))
                         that bind variable var to the result of rewriting
                         term.

     :gstack          *  the current goal stack.  The gstack is maintained
                         by rewrite and is the data structure printed as the
                         current ``path.''  Thus, any information derivable
                         from the :path brr command is derivable from gstack.
                         For example, from gstack one might determine that
                         the current term is the second hypothesis of a
                         certain rewrite rule.

In general brr@-expressions are used in break conditions, the
expressions that determine whether interactive breaks occur when
monitored runes are applied.  See MONITOR.  For example, you
might want to break only those attempts in which one particular term is
being rewritten or only those attempts in which the binding for the
variable a is known to be a consp.  Such conditions can be expressed
using ACL2 system functions and the information provided by brr@.
Unfortunately, digging some of this information out of the internal
data structures may be awkward or may, at least, require intimate
knowledge of the system functions.  But since conditional expressions
may employ arbitrary functions and macros, we anticipate that a set of
convenient primitives will gradually evolve within the ACL2 community.
It is to encourage this evolution that brr@ provides access to the *'d
data.

MONITOR    to monitor the attempted application of a rule name

     Example:
     (monitor '(:rewrite assoc-of-app) 't)
     :monitor (:rewrite assoc-of-app) t
     :monitor (:definition app) (equal (brr@ :target) '(app c d))

     General Form:
     (monitor rune term)

where rune is a rune and term is a term, called the "break condition."
Rune must be either a :rewrite rune or a :definition rune.

When a rune is monitored any attempt to apply it may result in an
interactive break in an ACL2 "wormhole state." There you will get a
chance to see how the application proceeds.  See BREAK-REWRITE
for a description of the interactive loop entered.  Whether an
interactive break occurs depends on the value of the break condition
expression associated with the monitored rune.

NOTE: Some :rewrite rules are considered "simple abbreviations"; see
SIMPLE.  These can be be monitored, but only at certain times
during the proof.  Monitoring is carried out by code inside the
rewriter but abbreviation rules may be applied by a special purpose
simplifier inside the so-called _preprocess_ phase of a proof.  If you
desire to monitor an abbreviation rule, a warning will be printed
suggesting that you may want to supply the hint :DO-NOT '(PREPROCESS);
see HINTS.  Without such a hint, an abbreviation rule can be
applied during the preprocess phase of a proof, and no such application
will cause an interactive break.

To remove a rune from the list of monitored runes, use unmonitor.  To
see which runes are monitored and what their break conditions are,
evaluate (monitored-runes).

Monitor, unmonitor and monitored-runes are macros that expand into
expressions involving state.  While these macros appear to return the
list of monitored runes this is an illusion.  They all print monitored
rune information to the comment window and then return values
(so-called "error triples") instructing ld to print nothing.  It is
impossible to return the list of monitored runes because it exists only
in the wormhole state with which you interact when a break occurs.
This allows you to change the monitored runes and their conditions
during the course of a proof attempt without changing the state in
which the the proof is being constructed.

Unconditional break points are obtained by using the break condition t.
We now discuss conditional break points.  The break condition, expr,
must be a term that contains no free variables other than state and
that returns a single non-state result.  In fact, the result should be
nil, t, or a true list of commands to be fed to the resulting
interactive break.  Whenever the system attempts to use the associated
rule, expr is evaluated in the wormhole interaction state.  A break
occurs only if the result of evaluating expr is non-nil.  If the result
is a true list, that list is appended to the front of standard-oi and
hence is taken as the initial user commands issued to the interactive
break.

In order to develop effective break conditions it must be possible to
access context sensitive information, i.e., information about the
context in which the monitored rune is being tried.  The brr@ macro may
be used in break conditions to access such information as the term
being rewritten and the current governing assumptions.  This
information is not stored in the proof state but is transferred into
the wormhole state when breaks occur.  The macro form is (brr@ :sym)
where :sym is one of several keyword symbols, including :target (the
term being rewritten), :unify-subst (the substitution that instantiates
the left-hand side of the conclusion of the rule so that it is the
target term), and :type-alist (the governing assumptions).  See
BRR@.

For example,

     ACL2 !>:monitor (:rewrite assoc-of-app)
                     (equal (brr@ :target) '(app a (app b c)))

will monitor (:rewrite assoc-of-app) but will cause an interactive
break only when the target term, the term being rewritten, is (app a
(app b c)).

Because break conditions are evaluated in the interaction environment,
the user developing a break condition for a given rune can test
candidate break conditions before installing them.  For example,
suppose an unconditional break has been installed on a rune, that an
interactive break has occurred and that the user has determined both
that this particular application is uninteresting and that many more
such applications will likely occur.  An appropriate response would be
to develop an expression that recognizes such applications and returns
nil.  Of course, the hard task is figuring out what makes the current
application uninteresting.  But once a candidate expression is
developed, the user can evaluate it in the current context simply to
confirm that it returns nil.

Recall that when a break condition returns a non-nil true list that
list is appended to the front of standard-oi.  For example,

     ACL2 !>:monitor (:rewrite assoc-of-app) '(:go)

will cause (:rewrite assoc-of-app) to be monitored and will make the
break condition be '(:go).  This break condition always evaluates the
non-nil true list (:go).  Thus, an interactive break will occur every
time (:rewrite assoc-of-app) is tried.  The break is fed the command
:go.  Now the command :go causes break-rewrite to (a) evaluate the
attempt to apply the lemma, (b) print the result of that attempt, and
(c) exit from the interactive break and let the proof attempt continue.
Thus, in effect, the above :monitor merely "traces" the attempted
applications of the rune but never causes an interactive break
requiring input from the user.

It is possible to use this feature to cause a conditional break where
the effective break condition is tested *after* the lemma has been
tried.  For example:

     ACL2 !>:monitor (:rewrite lemma12)
                     '(:unify-subst
                       :eval$ nil
                       :ok-if (or (not (brr@ :wonp))
                                  (not (equal (brr@ :rewritten-rhs) '(foo a))))
                       :rewritten-rhs)

causes the following behavior when (:rewrite lemma12) is tried.  A
break always occurs, but it is fed the commands above.  The first,
:unify-subst, causes break-rewrite to print out the unifying
substitution.  Then in response to :eval$ nil the lemma is tried but
with all runes temporarily unmonitored.  Thus no breaks will occur
during the rewriting of the hypotheses of the lemma.  When the attempt
has been made, control returns to break-rewrite (which will print the
results of the attempt, i.e., whether the lemma was applied, if so what
the result is, if not why it failed).  The next command, the :ok-if
with its following expression, is a conditional exit command.  It means
exit break-rewrite if either the attempt was unsuccessful, (not (brr@
:wonp)), or if the result of the rewrite is any term other than (foo
a).  If this condition is met, the break is exited and the remaining
break commands are irrelevant.  If this condition is not met then the
next command, :rewritten-rhs, prints the result of the application
(which in this contrived example is known to be (foo a)).  Finally, the
list of supplied commands is exhausted but break-rewrite expects more
input.  Therefore, it begins prompting the user for input.  The end
result, then, of the above :monitor command is that the rune in
question is elaborately traced and interactive breaks occur whenever it
rewrites its target to (foo a).

We recognize that the above break condition is fairly arcane.  We
suspect that with experience we will develop some useful idioms.  For
example, it is straightforward now to define macros that monitor runes
in the ways suggested by the following names:  trace-rune,
break-if-target-is, and break-if-result-is.  For example, the last
could be defined as

     (defmacro break-if-result-is (rune term)
       `(monitor ',rune
                 '(quote (:eval :ok-if
                                (not (equal (brr@ :rewritten-rhs) ',term))))))

(Note however that the submitted term must be in translated form.)

Since we don't have any experience with this kind of control on lemmas
we thought it best to provide a general (if arcane) mechanism and hope
that the ACL2 community will develop the special cases that we find
most convenient.

MONITORED-RUNES    print the monitored runes and their break conditions

     Example and General Form:
     :monitored-runes

This macro prints a list, each element of which is of the form (rune
expr), showing each monitored rune and its current break condition.

OK-IF    conditional exit from break-rewrite

     Example Form:
     :ok-if (null (brr@ :wonp))

     General Form:
     :ok-if expr

where expr is a term involving no free variables other than state and
returning one non-state result which is treated as Boolean.  This form
is intended to be executed from within break-rewrite (see
BREAK-REWRITE).

Consider first the simple situation that the (ok-if term) is a command
read by break-rewrite.  Then, if the term is non-nil, break-rewrite
exits and otherwise it does not.

More generally, ok-if returns an ACL2 error triple (mv erp val state).
(See LD or see PROGRAMMING-WITH-STATE for more on error
triples.)  If any form being evaluated as a command by break-rewrite
returns the triple returned by (ok-if term) then the effect of that
form is to exit break-rewrite if term is non-nil.  Thus, one might
define a function or macro that returns the value of ok-if expressions
on all outputs and thus create a convenient new way to exit
break-rewrite.

The exit test, term, generally uses brr@ to access context sensitive
information about the attempted rule application.  See BRR@.
Ok-if is useful inside of command sequences produced by
break conditions.  See MONITOR.  :ok-if is most useful after an
:eval command has caused break-rewrite to try to apply the rule because
in the resulting break environment expr can access such things as
whether the rule succeeded, if so, what term it produced, and if not,
why.  There is no need to use :ok-if before :evaling the rule since the
same effects could be achieved with the break condition on the rule
itself.  Perhaps we should replace this concept with
:eval-and-break-if?  Time will tell.

UNMONITOR    to stop monitoring a rule name

     Examples:
     (unmonitor '(:rewrite assoc-of-app))
     :unmonitor (:rewrite assoc-of-app)
     :unmonitor :all

     General Forms:
     (unmonitor rune)
     (unmonitor :all)

Here, rune is a rune that is currently among those with break points
installed.  This function removes the break.

Subtle point:  Because you may want to unmonitor a "rune" that is no
longer a rune in the current ACL2 world, we don't actually check this
about rune.  Instead, we simply check that rune is a consp beginning
with a keywordp.  That way, you'll know you've made a mistake if you
try to :unmonitor binary-append instead of :unmonitor (:definition
binary-append), for example.

DOCUMENTATION    functions that display documentation

This section explains the ACL2 online documentation system.  Thus, most
of it assumes that you are typing at the terminal, inside an ACL2
session.  If you are reading this description in another setting (for
example, in a web browser, in Emacs info, or on paper), simply ignore
the parts of this description that involve typing at the terminal.

ACL2 users are welcome to contribute additional documentation.  See the
web page `http://www.cs.utexas.edu/users/moore/acl2/contrib/'.

For an introduction to the ACL2 online documentation system, type :more
below.  Whenever the documentation system concludes with "(type :more
for more, :more! for the rest)" you may type :more to see the next
block of documentation.

Topics related to documentation are documented individually:

To view the documentation in a web browser, open a browser to file
doc/HTML/acl2-doc.html under your ACL2 source directory, or just go to
the ACL2 home page at `http://www.cs.utexas.edu/users/moore/acl2/'.
Alternatively, follow a link on the ACL2 home page to the new "xdoc"
version of the manual, which can be found locally after running a
regression by pointing your web browser at file
books/xdoc/manual/preview.html.

To use Emacs Info (inside Emacs), first load distributed file
emacs/emacs-acl2.el (perhaps inside your .emacs file) and then execute
meta-x acl2-info.  In order to see true links to external web pages,
you may find the following addition to your .emacs file to be helpful.

     ; For emacs-version 22 or (presumably) later, you can probably set
     ; arrange that in Emacs Info, URLs become links, in the sense that
     ; if you hit <RETURN> while standing on a URL, then you will be
     ; taken to that location in a web browser.  If this does not happen
     ; automatically, then evaluating the `setq' form below might work
     ; if you have firefox.  If that does not work, then you can probably
     ; figure out what to do as follows.  First type
     ;   control-h v browse-url-browser-function
     ; and then from the resulting help page,
     ; hit <return> on the link ``customize'' in:
     ; ``You can customize this variable''
     ; and then follow instructions.
     (setq browse-url-browser-function (quote browse-url-firefox))

There is a print version of the documentation, though we recommend
using one of the other methods (web, Emacs Info, or online) to browse
it.  If you really want the print version, you can find it here:
`http://www.cs.utexas.edu/users/moore/publications/acl2-book.ps.gz'.

Below we focus on how to access the online documentation, but some of
the discussion is relevant to other formats.

The ACL2 online documentation feature allows you to see extensive
documentation on many ACL2 functions and ideas.  You may use the
documentation facilities to document your own ACL2 functions and
theorems.

If there is some name you wish to know more about, then type

     ACL2 !>:doc name

in the top-level loop.  If the name is documented, a brief blurb will
be printed.  If the name is not documented, but is "similar" to some
documented names, they will be listed.  Otherwise, nil is returned.

Every name that is documented contains a one-line description, a few
notes, and some details.  :Doc will print the one-liner and the notes.
When :doc has finished it stops with the message "(type :more for more,
:more! for the rest)" to remind you that details are available.  If you
then type

     ACL2 !>:more

a block of the continued text will be printed, again concluding with
"(type :more for more, :more! for the rest)" if the text continues
further, or concluding with "*-" if the text has been exhausted.  By
continuing to type :more until exhausting the text you can read
successive blocks.  Alternatively, you can type :more! to get all the
remaining blocks.

If you want to get the details and don't want to see the elementary
stuff typed by :doc name, type:

     ACL2 !>:MORE-DOC name

We have documented not just function names but names of certain
important ideas too.  For example, see REWRITE and see
META to learn about :rewrite rules and :meta rules, respectively.
See HINTS to learn about the structure of the :hints argument
to the prover.  The deflabel event (see DEFLABEL) is a way to
introduce a logical name for no reason other than to attach
documentation to it; also see DEFDOC.

How do you know what names are documented?  There is a documentation
data base which is querried with the :docs command.

The documentation data base is divided into sections.  The sections are
listed by

     ACL2 !>:docs *

Each section has a name, sect, and by typing

     ACL2 !>:docs sect

or equivalently

     ACL2 !>:doc sect

you will get an enumeration of the topics within that section.  Those
topics can be further explored by using :doc (and :more) on them.  In
fact the section name itself is just a documented name.  :more
generally gives an informal overview of the general subject of the
section.

     ACL2 !>:docs **

will list all documented topics, by section.  This fills several pages
but might be a good place to start.

If you want documentation on some topic, but none of our names or brief
descriptions seem to deal with that topic, you can invoke a command to
search the text in the data base for a given string.  This is like the
GNU Emacs "apropos" command.

     ACL2 !>:docs "functional inst"

will list every documented topic whose :doc or :more-doc text includes
the substring "functional inst", where case and the exact number of
spaces are irrelevant.

If you want documentation on an ACL2 function or macro and the
documentation data base does not contain any entries for it, there are
still several alternatives.

     ACL2 !>:args fn

will print the arguments and some other relevant information about the
named function or macro.  This information is all gleaned from the
definition (not from the documentation data base) and hence this is a
definitive way to determine if fn is defined as a function or macro.

You might also want to type:

     ACL2 !>:pc fn

which will print the command which introduced fn.  You should see
COMMAND-DESCRIPTOR for details on the kinds of input you can give the
:pc command.

The entire ACL2 documentation data base is user extensible.  That is,
if you document your function definitions or theorems, then that
documentation is made available via the data base and its query
commands.

The implementation of our online documentation system makes use of
Common Lisp's "documentation strings." While Common Lisp permits a
documentation string to be attached to any defined concept, Common Lisp
assigns no interpretation to these strings.  ACL2 attaches special
significance to documentation strings that begin with the characters
":Doc-Section".  When such a documentation string is seen, it is stored
in the data base and may be displayed via :doc, :more, :docs, etc.
Such documentation strings must follow rigid syntactic rules to permit
their processing by our commands.  These are spelled out elsewhere; see
DOC-STRING.

A description of the structure of the documentation data base may also
be found; see DOC-STRING.

Finally: To build the HTML documentation, proceed with the following
sequence of steps.

     1. In the doc/ subdirectory of the ACL2 distribution, start ACL2
     and then evaluate (certify-book "write-acl2-html").

     2. Exit ACL2 and start it up again (or, evaluate :u).

     3. Include the documented books within your ACL2 loop using
     include-book.

     4. Evaluate (include-book "../doc/write-acl2-html" :dir :system).

     5. Call macro write-html-file, following the instructions at the
     end of distributed file doc/write-acl2-html.lisp.

*TERMINAL-MARKUP-TABLE*    a markup table used for printing to the terminal

The value of the ACL2 constant *terminal-markup-table* is an association
list pairing markup keys with strings, to be used for printing to the
terminal.  See MARKUP for a description of the ACL2 markup
language.

The entries in *terminal-markup-table* are of the form

     (key flag . fmt-string)

where key is one of the doc-string tilde directives (see
MARKUP), flag is a Boolean as described below, and fmt-string is a
string as expected by the ACL2 printing function fmt.  The system
arranges that for any arg, when an expression ~key[arg] is encountered
by the documentation printer, fmt will print fmt-string in an
association list, binding keys based on arg as follows.

     #\p --- the `pointer'     ; only used if flag is t
     #\s --- the print name version of the pointer, e.g., |abc| or ABC
     #\c --- the parent file   ; only used if flag is t
     #\t --- the displayed text
     #\T --- uppercased displayed text

The first three entries are used only when the flag associated with key
is t, indicating that the argument arg of ~key is to be parsed as
starting with a symbol; for example, ~key[foo bar] will bind #\p to the
symbol FOO.

The discussion of the above association list for printing fmt-string
applies when printing documentation to other than the terminal as well.
Such tools exist for Texinfo and for HTML; see files
doc/write-acl2-html.lisp and doc/write-acl2-texinfo.lisp distributed
with ACL2.

ARGS    args, guard, type, constraint, etc., of a function symbol

     Example:
     :args assoc-eq

Args takes one argument, a symbol which must be the name of a function
or macro, and prints out the formal parameters, the guard expression,
the output signature, the deduced type, the constraint (if any), and
whether documentation about the symbol is available via :doc.

DOC    brief documentation (type :doc name)

NOTE:  The :doc command only makes sense at the terminal.  Furthermore
it only works at the terminal when a "full-size" image has been built.
Most users will probably access the ACL2 documentation in other ways,
as explained in the file "doc/README" that comes with the ACL2
distribution.

     Examples:
     ACL2 !>:doc DEFTHM          ; print documentation of DEFTHM
     ACL2 !>:doc logical-name    ; print documentation of LOGICAL-NAME
     ACL2 !>:doc "MY-PKG"      ; print documentation of "MY-PKG"

     Related Topics:
     :more                      ; continues last :doc or :more-doc text
     :more-doc name             ; prints more documentation for name
     :docs **                   ; lists all documented symbols
     :docs "compil"             ; documented symbols apropos "compil"
     :DOC documentation         ; describes how documentation works

     General Form:
     ACL2>:doc logical-name

where logical-name is a logical name (see LOGICAL-NAME) for
which you hope there is documentation.  Chances are there is no
documentation at the moment, but we are working on adding documentation
strings for all the user level ACL2 functions.

For a general discussion of our treatment of documentation strings, see
DOCUMENTATION.

This is the first cut at online documentation.  Users can be
particularly helpful by sending mail on the inadequacies of the system.
Address it just to Moore and put Documentation in the subject line.
There are several things that trouble me about what I've done here.

First, many concepts aren't documented.  Ultimately, I'd like to .
document (a) every CLTL primitive (e.g., case and coerce) and (b) every
ACL2 extension (e.g., aref1 and getprop).  But so far I have focussed
on documenting (c) the ACL2 system primitives (e.g., defthm and what
hints look like).  My priorities are (c), then (b), and then (a),
following the philosophy that the most unstable features should get
online documentation in these early releases.  Having gotten the basic
documentation in place, I'll document new things as they are added, and
in response to your pleas I'll try to add documentation to old things
that are widely regarded as important.

Second, I worry that the existing documentation is unhelpful because it
provides too much or too little detail, or it provides the detail too
far away from where it is needed.  Please be on the lookout for this.
Did you get what you needed when you appealed to :doc or :more-doc?  If
not, what was it you needed?  Would more cross-references help?  Did
you get lost in maze of cross-references?

DOC!    all the documentation for a name (type :doc! name)

NOTE:  The :doc! command only makes sense at the terminal.

     Examples:
     ACL2 !>:doc! defthm
     ACL2 !>:doc! certificate

This command is like :doc name followed by :more!.  It prints all the
documentation of name.

DOC-STRING    formatted documentation strings

     Examples:
     ":Doc-Section name
     one-liner~/notes~/details"

     ":Doc-Section name
     one-liner~/
     notes~/
     details~/
     :cite old-name1
     :cited-by old-name2"

Use (get-doc-string 'name state) to see other examples.

Documentation strings not beginning with ":Doc-Section" (case is
irrelevant) are ignored.  See MARKUP for how to supply
formatting information (such as fonts and displayed text) in
documentation strings.

ACL2 attaches special importance to documentation strings beginning
with the header ":Doc-Section" (or any variant thereof obtained by
changing case).  Any documentation string that does not begin with such
a header is considered unformatted and is ignored.  For the rest of
this discussion, we use the phrase "documentation string" as though it
read "formatted documentation string."

Documentation strings are always processed in the context of some
symbol, name, being defined.  (Indeed, if an event defines no symbol,
e.g., verify-guards or in-theory, then it is not permitted to have a
formatted documentation string.)  The string will be associated with
name in the "documentation data base." The data base is divided into
"sections" and each section is named by a symbol.  Among the sections
are events, documentation, history, other, and miscellaneous.  A
complete list of the sections may be obtained by typing :docs * at the
terminal.  You can create new sections.  The main purpose of sections
is simply to partition the large set of names into smaller subsets
whose contents can be enumerated separately.  The idea is that the user
may remember (or recognize) the relevant section name and then read its
contents to find interesting items.

Within a section are "documentation tuples" which associate with each
documented name its documentation string and a list of related
documented names, called the "related names" of the name.  When :doc
prints the documentation for name, it always lists the related names.

When a formatted documentation string is submitted with the defining
event of some name, the section name and an initial set of related
names are parsed from the string.  In addition, the formatted string
contains various "levels" of detail that are printed out at different
times.  Finally, it is possible for a string to cause the newly
documented name to be added to the related names of any previously
documented name.  Thus, as new names are introduced they can be grouped
with old ones.

The general form of an ACL2 formatted documentation string is

     ":DOC-SECTION <section-name>
       <one-liner>~/
       <notes>~/
       <details>~/
       :CITE <n1>
       ...
       :CITE <nn>
       :CITED-BY <m1>
       ...
       :CITED-BY <mm>"

Before we explain this, let it be noted that (get-doc-string name
state) will return the documentation string associated with name in the
documentation data base.  You may want to call get-doc-string on 'pe
and 'union-theories just to see some concrete documentation strings.
This documentation string, which is rather long, is under 'doc-string.

A formatted documentation string has five parts: the header and
section-name (terminating in the first #\Newline), the <one-liner>,
<notes>, and <details> (each terminating in a tilde-slash ("~/") pair),
and a citation part.  These five parts are parsed into six components.
<section-name> is read as the name of a symbol, section-name.
<one-liner>, <notes>, and <details> are arbitrary sequences of
characters (ignoring initial white space and not including the
tilde-slash pairs which terminate them).  The <ni> are read as symbols
and assembled into a list called the "cite" symbols.  The <mi> are read
as symbols and assembled into a list called the "cited-by" symbols.
See the warning below regarding the hackish nature of our symbol reader.

Section-name must either be a previously documented symbol or else be
name, the symbol being documented.  To open a new section of the data
base, named section-name, you should define the logical name
section-name (as by deflabel or any other event; also see
DEFDOC) and attach to it a documentation string for section
section-name.  You might wish to print out the documentation string we
use for some of our section names, e.g., (get-doc-string 'events
state).  By forcing section names to be documented symbols, we permit
sections themselves to have one line descriptions and discussions,
presented by the standard documentation facilities like the facilities
:doc and :more-doc that may be used at the terminal.

Each of the ni's and mi's must be previously documented symbols.

Both <one-liner> and <details> must be non-empty, i.e., must contain
some non-whitespace characters.  <notes> may be empty.  The :cites and
:cited-bys pairs may be intermingled and may be separated by either
newlines or spaces.  The citation part may be empty.  When the citation
part is empty, the tilde-slash pair terminating the <details> part may
be omitted.  Thus, the simplest form of a formatted documentation
string is:

     ":Doc-Section <section-name>
      <one-liner>~/~/
      <details>"

Since white space at the front of <one-liner>, <notes> and <details> is
ignored, we often precede those parts by #\Newlines to make the strings
easier to read in our source files.  We also typically indent all of
the text in the string by starting each line with a few spaces.  (The
Emacs commands for formatting Lisp get confused if you have arbitrary
characters on the left margin.)  We assume that every line in
<one-liner>, <notes>, and <details> starts with at least as many spaces
as <one-liner> does, i.e., we assume they are all indented the same
amount (or more).  Let d be the number of spaces separating <one-liner>
from the #\Newline preceding it.  When the various parts are printed,
we "de-indent" by stripping out the first d spaces following each
#\Newline.

However, we find that when documentation is printed flush against the
left margin it is difficult to distinguish the documentation text from
previous output.  We therefore prefix each line we print by a special
pad of characters.  By default, this pad is "| " so that documentation
text has a vertical bar running down the left margin.  But the pad is
just the value of the global variable doc-prefix and you may assign it
any string you wish.

To add such a string to the data base under the symbol name we make a
new entry in the section-name section of the data base.  The entry
associates name with the string and uses the string's cites list as the
initial value of the related names field.  In addition, we add name to
the related names field of each of the names listed in the string's
cited-by list.  We also add name to the related names field of its
section-name.  Observe that the cites list in a string is only the
initial value of the related names of the names.  Future documentation
strings may add to it via :cited-by or :Doc-Section.  Indeed, this is
generally the case.  We discuss this further below.

When a brief description of name is required (as by :docs **), name and
<one-liner> are printed.  <one-liner> is usually printed starting in
column 15 (however see PRINT-DOC-START-COLUMN).  Despite its
name, <one-liner> need not be one line.  It usually is one line,
however.

When you type :doc name at the terminal, the first response will be to
print name and <one-liner>.  Then :doc prints <notes>, if any.  Then,
if name is the name of a section, it prints the <one-liner>s for each
of its related names.  For example, try :doc events.  If name is not a
section name but does have some related names, they are merely listed
but not explained.  Try :doc theory-functions.  :more-doc name prints
<details>.

Our style is to let each new concept add itself to the related names of
old concepts.  To do otherwise increases the chances that documentation
gets outdated because one often forgets to update supposedly complete
lists of the relevant topics when new topics are invented.  For
example, :doc theory-functions lists each available theory function.
But get-doc-string of 'theory-functions just shows a few examples and
has an empty cites list.  From where do we get the names of the theory
functions listed by :doc?  The answer is that each theory function has
its own documentation string and those strings each specify :cited-by
theory-functions.  See for example get-doc-string of 'union-theories.
So by the time the entire system is assembled, the related names of
'theory-functions contains all the (documented) theory functions.  This
makes it easy to add new theory functions without changing the general
discussion in 'theory-functions.

When an event or command form is printed, as by :pe or :pc, that
contains a formatted documentation string, we do not print the actual
documentation string (since they are usually large and distracting).
Instead we print the string:

       "Documentation available via :doc"

inviting you to use :doc and :more-doc (or get-doc-string) if you wish
to see the documentation at the terminal.

_Warning on Reading Symbols from Strings:_ When we read a symbol, such
as the section-symbol, from a documentation string, we use a quick and
dirty imitation of the much more powerful CLTL read program.  In
particular, we scan past any whitespace, collect all the characters we
see until we get to more whitespace or the end of the string, convert
the characters to upper case, make a string out of them, and intern
that string.  Thus, if you typed ":Doc-Section 123 ..." we would read
the 123 as the symbol |123|.  Observe that special characters, such as
parentheses and escape characters, are not afforded their usual
reverence by our hack.  Furthermore, the question arises: in which
package do we intern the symbol?  The answer is, usually, the package
containing the name being defined.  I.e., if you are documenting
my-pkg::name and you attach a documentation string that begins
":Doc-Section: Machines ..." then the section-symbol will be
my-pkg::machines.  We recognize two special cases. If the first
character read is a colon, we use the keyword package.  If the first
five characters read are acl2:: then we intern in the "ACL2" package.
Our own section names, e.g., events, are in the "ACL2" package.

In a related area, when you ask for the documentation of a name, e.g.,
when you type :doc name at the terminal, that name is read with the
full ACL2 reader, not the hack just described.  That name is read into
the current package.  Thus, if you are operating in-package "MY-PKG"
and type :doc events, what is read is my-pkg::events.  The data base
may not contain an entry for this symbol.  Before reporting that no
documentation exists, we try acl2::events.

One last note: defpkg permits a formatted documentation string, which
is associated in the data base with the name of the package.  But the
name of the package is a string, not a symbol.  It is permitted to
access the documentation of a string (i.e., package name).  But there
are no facilities for getting such a stringp name into the related
names of another name nor of making such stringp names be section
names.  That is because we always read symbols from strings and never
read strings from strings.  I.e., if you did write "Doc-Section
\"MY-PKG\" ..." it would read in as a weird symbol.

DOCS    available documentation topics (by section)

NOTE:  The :docs command only makes sense at the terminal.

When the :docs command is given a stringp argument it searches the text
produced by :doc and :more-doc and lists all the documented topics
whose text contains the given string.  For purposes of this string
matching we ignore distinctions of case and the amount and kind (but
not presence) of white space.  We also treat hyphen as whitespace.

However, the following examples show how :docs can be used on other than
string patterns.

     Examples:
     ACL2 !>:docs *           ; lists documentation sections
     ACL2 !>:docs **          ; lists all documented topics within all sections
     ACL2 !>:docs events      ; lists all topics in section EVENTS
     ACL2 !>:docs "compil"    ; lists topics ``apropos''

The data base of formatted documentation strings is structured into
sections.  Within a section are topics.  Each topic has a one-liner,
some notes, and some detailed discussions.  The :docs command provides
a view of the entire data base.

:docs takes one argument, as described below:

     arg               effect

     *                 list all section headings in the data base
     **                list all section headings and all topics within
                       each section
     name              list all topics in the section named name (where
                       name is some symbol other than * and **).  This
                       is always the same as :doc name.
     pattern           list all topics whose :doc or :more-doc text
                       mentions the string pattern.  For purposes of this
                       string matching we ignore distinctions of case and
                       the amount and kind (but not presence) of white
                       space.  We also treat hyphen as whitespace.

HELP    brief survey of ACL2 features

     Example:
     ACL2 !>:help

See LP for general information about the top-level command
environment for ACL2.

MARKUP    the markup language for ACL2 documentation strings

ACL2 documentation strings make special use of the tilde character (~).
In particular, we describe here a "markup language" for which the tilde
character plays a special role.  The markup language is valuable if you
want to write documentation that is to be displayed outside your ACL2
session.  If you are not writing such documentation, and if also you do
not use the character `~', then there is no need to read on.

Three uses of the tilde character (~) in documentation strings are as
follows.  Below we explain the uses that constitute the ACL2 markup
language.

     ~/
     Indicates the end of a documentation *section*; see
     DOC-STRING.

     ~~
     Indicates the literal insertion of a tilde character (~).

     ~]
     This directive in a documentation string is effective only during
     the processing of part 2, the details (see DOC-STRING), and
     controls how much is shown on each round of :more processing when
     printing to the terminal.  If the system is not doing :more
     processing, then it acts as though the ~] is not present.
     Otherwise, the system put out a newline and halts documentation
     printing on the present topic, which can be resumed if the user
     types :more at the terminal.

The other uses of the tilde character are of the following form.

       ~key[arg]

Before launching into an explanation of how this works in detail, let
us consider some small examples.

Here is a word that is code:

       ~c[function-name].

Here is a phrase with an "emphasized" word, "not":

       Do ~em[not] do that.

Here is the same phrase, but where "not" receives stronger emphasis
(presumably boldface in a printed version):

       Do ~st[not] do that.

Here is a passage that is set off as a display, in a fixed-width font:

       ~bv[]
       This passage has been set off as ``verbatim''.
       The present line starts just after a line break.  Normally, printed
       text is formatted, but inside ~bv[]...~ev[], line breaks are taken
       literally.
       ~ev[]

In general, the idea is to provide a "markup language" that can be
reasonably interpreted not only at the terminal (via :doc), but also
via translators into other languages.  In fact, translators have been
written into Texinfo and HTML.

Let us turn to a more systematic consideration of how to mark text in
documentation strings using expressions of the form ~key[arg], which we
will call "doc-string tilde directives."  The idea is that key informs
the documentation printer (which could be the terminal, a hardcopy
printer, or some hypertext tool) about the "style" used to display arg.
The intention is that each such printer should do the best it can.  For
example, we have seen above that ~em[arg] tells the printer to emphasize
arg if possible, using an appropriate display to indicate emphasis
(italics, or perhaps surrounding arg with some character like _, or
...).  For another example, the directive for bold font, ~b[arg], says
that printed text for arg should be in bold if possible, but if there
is no bold font available (such as at the terminal), then the argument
should be printed in some other reasonable manner (for example, as
ordinary text).  The key part is case-insensitive; for example, you can
use ~BV[] or ~Bv[] or ~bV[] in place of ~bv[].

Every form below may have any string as the argument (inside [..]), as
long as it does not contain a newline (more on that below).  However,
when an argument does not make much sense to us, we show it below as
the empty string, e.g., "~bv[]" rather than "~bv[arg]".

     ~-[]      Print the equivalent of a dash

     ~b[arg]   Print the argument in bold font, if available

     ~bid[arg]   ``Begin implementation dependent'' -- Ignores argument at
               terminal.

     ~bf[]     Begin formatted text (respecting spaces and line breaks),
               but in ordinary font (rather than, say, fixed-width font)
               if possible

     ~bq[]     Begin quotation (indented text, if possible)

     ~bv[]     Begin verbatim (print in fixed-width font, respecting
               spaces and line breaks)

     ~c[arg]   Print arg as ``code'', such as in a fixed-width font

     ~ef[]     End format; balances ~bf[]

     ~eid[arg]   ``End implementation dependent'' -- Ignores argument at
               terminal.

     ~em[arg]  Emphasize arg, perhaps using italics

     ~eq[]     End quotation; balances ~bq[]

     ~ev[]     End verbatim; balances ~bv[]

     ~i[arg]   Print arg in italics font

     ~id[arg]   ``Implementation dependent'' -- Ignores argument at
               terminal.

     ~il[arg]  Print argument as is, but make it a link to another doc
               topic (for true hypertext environments).  Note that the
               link argument must match the package name for the desired
               topic unless the package name is ``ACL2''.  That is, to
               link to documentation on ``foo::topic'', one needs to use
               the full name for ``foo::topic'', including its package
               name.

     ~ilc[arg] Same as ~il[arg], except that arg should be printed as
               with ~c[arg]

     ~l[arg]   Ordinary link to another doc topic; prints as ``See :DOC
               arg'' at the terminal (but also see ~pl below, which puts
               ``see'' in lower case)

     ~nl[]     Print a newline

     ~par[]    Paragraph mark, of no significance at the terminal
               (can be safely ignored; see also notes below)

     ~pl[arg]  Parenthetical link (borrowing from Texinfo):  same as
               ~l[arg], except that ``see'' is in lower case.  This is
               typically used at other than the beginning of a sentence.

     ~sc[arg]  Print arg in (small, if possible) capital letters

     ~st[arg]  Strongly emphasize arg, perhaps using a bold font

     ~t[arg]   Typewriter font; similar to ~c[arg], but leaves less
               doubt about the font that will be used.

     ~terminal[arg]  Terminal only; arg is to be ignored except when
               reading documentation at the terminal, using :DOC.

     ~url[arg]  Print arg as HTML hyperlink if possible (else print like ~c)

_Style notes and further details_

It is not a good idea to put doc-string tilde directives inside
verbatim environments, ~bv[] ... ~ev[].

Do not nest doc-string tilde directives; that is, do not write

       The ~c[~il[append] function ...

but note that the "equivalent" expression

       The ~ilc[append] function ...

is fine.  The following phrase is also acceptable:

       ~bf[]This is
       ~em[formatted] text.
       ~ef[]

because the nesting is only conceptual, not literal.

We recommend that for displayed text, ~bv[] and ~ev[] should usually
each be on lines by themselves.  That way, printed text may be less
encumbered with excessive blank lines.  Here is an example.

       Here is some normal text.  Now start a display:
       ~bv[]
         2 + 2 = 4
       ~ev[]
       And here is the end of that paragraph.

       Here is the start of the next paragraph.

The analogous consideration applies to ~bf[] and ~ef[] as well as ~bq[]
and ~eq[].

You may "quote" characters inside the arg part of ~key[arg], by
preceding them with ~.  This is, in fact, the only legal way to use a
newline character or a right bracket (]) inside the argument to a
doc-string tilde directive.

Write your documentation strings without hyphens.  Otherwise, you may
find your text printed on paper (via TeX, for example) like this --

       Here is a hyphe- nated word.

even if what you had in mind was:

       Here is a hyphe-
       nated word.

When you want to use a dash (as opposed to a hyphen), consider using
~-[], which is intended to be interpreted as a "dash."  For example:

       This sentence ~-[] which is broken with dashes ~-[] is boring.

would be written to the terminal (using :doc) by replacing ~-[] with
two hyphen characters, but would presumably be printed on paper with a
dash.

Be careful to balance the "begin" and "end" pairs, such as ~bv[] and
~ev[].  Also, do not use two "begin" directives (~bf[], ~bq[], or
~bv[]) without an intervening "end" directive.  It is permissible (and
perhaps this is not surprising) to use the doc-string part separator ~/
while between such a begin-end pair.

Because of a bug in texinfo (as of this writing), you may wish to avoid
beginning a line with (any number of spaces followed by) the -
character or ~-[].

The "paragraph" directive, ~par[], is rarely if ever used.  There is a
low-level capability, not presently documented, that interprets two
successive newlines as though they were ~par[].  This is useful for the
HTML driver.  For further details, see the authors of ACL2.

Emacs code is available for manipulating documentation strings that
contain doc-string tilde-directives (for example, for doing a
reasonable job filling such documentation strings).  See the authors if
you are interested.

We tend to use ~em[arg] for "section headers," such as "Style notes and
further details" above.  We tend to use ~st[arg] for emphasis of words
inside text.  This division seems to work well for our Texinfo driver.
Note that ~st[arg] causes arg to be printed in upper-case at the
terminal (using :doc), while ~em[arg] causes arg to be printed at the
terminal as though arg were not marked for emphasis.

Our Texinfo and HTML drivers both take advantage of capabilities for
indicating which characters need to be "escaped," and how.  Unless you
intend to write your own driver, you probably do not need to know more
about this issue; otherwise, contact the ACL2 authors.  We should
probably mention, however, that Texinfo makes the following
requirement:  when using ~l[arg], where arg contains one of the special
characters @, {, or }, you must immediately follow this use with a
period or comma.  Also, the Emacs "info" documentation that we generate
by using our Texinfo driver has the property that in node names, : has
been replaced by | (because of quirks in info); so for example, the
"proof-checker" simplification command, s, is documented under
acl2-pc||s rather than under acl2-pc::s.

We have tried to keep this markup language fairly simple; in
particular, there is no way to refer to a link by other than the actual
name.  So for example, when we want to make :doc an invisible link in
"code" font, we write the following form, which indicates that : should
be in that font and then doc should both be in that font and be an
invisible link.

       ~c[:]~ilc[doc]

MORE    your response to :doc or :more's "(type :more...)"

NOTE:  The command :more only makes sense at the terminal.

     Example:
     ACL2 !>:more

will continue printing whatever documentation was started by :doc or
:more-doc.

When you type :doc name, for some documented name, the system responds
by typing the one-liner and the notes sections of the documentation for
name.  It then types "(type :more for more, :more! for the rest)".  If
you then type

     ACL2 !>:more

the system will start to print the details section of name.  The same
thing could be achieved by typing :more-doc name, but that requires you
to type name again.

Similarly, if you have typed :more-doc name, the system will print the
first "block" of the details section and then print "(type :more for
more, :more! for the rest)".  Typing :more at that point will cause the
next block of the details section to be printed.  Eventually :more will
conclude by printing "*-" which is the indicator that the text has been
exhausted.

What is a "block" of text?  :More looks for the end of a paragraph (two
adjacent newlines) after printing n lines.  If it doesn't find one
before it has printed k lines, it just stops there.  N and k here are
the values of the two state global variables 'more-doc-min-lines and
'more-doc-max-lines.  You may use @ and assign to inspect and set these
variables, e.g., (@ more-doc-max-lines) will return the current maximum
number of lines printed by :more and (assign more-doc-max-lines 19) will
set it to 19.  On terminals having only 24 lines, we find min and max
settings of 12 and 19 the most pleasant.

If you want :more to print all of the details instead of feeding them
to you one block at a time, type :more! instead.

MORE!    another response to "(type :more for more, :more! for the rest)"

NOTE:  The command :more! only makes sense at the terminal.

     Example:
     ACL2 !>:more!

will print all of the remaining documentation started by the last :doc
or :more-doc.

See MORE for some background.  Typing :more! will print all
remaining blocks of documentation.

:More! is like :more except that it prints all the text at once.  For
example, if you type :doc name you will see some text followed by
"(type :more for more, :more! for the rest)".  If you then type simply
:more! you will see all of the details, while if you type :more you
will be fed the next block of details.

MORE-DOC    a continuation of the :doc documentation

NOTE:  The :more-doc command only makes sense at the terminal.

     Examples:
     ACL2 !>:more-doc DEFTHM
     ACL2 !>:more-doc logical-name

Often it is assumed in the text provided by :more-doc name that you
have read the text provided by :doc name.

:More-doc just continues spewing out at you the documentation string
provided with a definition.  If the user has done his job, :doc will
probably remind you of the basics and :more-doc, if read after :doc,
will address obscure details that are nevertheless worth noting.

When :more-doc types "(type :more for more, :more! for the rest)" you
can get the next block of the continuation by typing :more or all of
the remaining blocks by typing :more!.  See MORE.

NQTHM-TO-ACL2    ACL2 analogues of Nqthm functions and commands

     Example Forms:
     :nqthm-to-acl2 prove-lemma   ; Display ACL2 topic(s) and/or print
                                  ; information corresponding to Nqthm
                                  ; PROVE-LEMMA command.
     (nqthm-to-acl2 'prove-lemma) ; Same as above.

     General Form:
     (nqthm-to-acl2 name)

where name is a notion documented for Nqthm:  either a function in the
Nqthm logic, or a command.  If there is corresponding information
available for ACL2, it will be printed in response to this command.
This information is not intended to be completely precise, but rather,
is intended to help those familiar with Nqthm to make the transition to
ACL2.

We close with two tables that contain all the information used by this
nqthm-to-acl2 command.  The first shows the correspondence between
functions in the Nqthm logic and corresponding ACL2 functions (when
possible); the second is similar, but for commands rather than
functions.

     Nqthm functions  -->     ACL2
     ----------------------------------------
     ADD1          -->  1+
     ADD-TO-SET    -->  ADD-TO-SET-EQUAL and ADD-TO-SET-EQ
     AND           -->  AND
     APPEND        -->  APPEND and BINARY-APPEND
     APPLY-SUBR    -->  No correspondent, but see the documentation for
                        DEFEVALUATOR and META.
     APPLY$        -->  No correspondent, but see the documentation for
                        DEFEVALUATOR and META.
     ASSOC         -->  ASSOC-EQUAL, ASSOC and ASSOC-EQ
     BODY          -->  No correspondent, but see the documentation for
                        DEFEVALUATOR and META.
     CAR           -->  CAR
     CDR           -->  CDR
     CONS          -->  CONS
     COUNT         -->  ACL2-COUNT
     DIFFERENCE    -->  -
     EQUAL         -->  EQUAL, EQ, EQL and =
     EVAL$         -->  No correspondent, but see the documentation for
                        DEFEVALUATOR and META.
     FALSE         -->  Nqthm's F corresponds to the ACL2 symbol NIL.
     FALSEP        -->  NOT and NULL
     FORMALS       -->  No correspondent, but see the documentation for
                        DEFEVALUATOR and META.
     GEQ           -->  >=
     GREATERP      -->  >
     IDENTITY      -->  IDENTITY
     IF            -->  IF
     IFF           -->  IFF
     IMPLIES       -->  IMPLIES
     LEQ           -->  <=
     LESSP         -->  <
     LISTP         -->  CONSP
     LITATOM       -->  SYMBOLP
     MAX           -->  MAX
     MEMBER        -->  MEMBER-EQUAL, MEMBER and MEMBER-EQ
     MINUS         -->  - and UNARY--
     NEGATIVEP     -->  MINUSP
     NEGATIVE-GUTS -->  ABS
     NLISTP        -->  ATOM
     NOT           -->  NOT
     NUMBERP       -->  ACL2-NUMBERP, INTEGERP and RATIONALP
     OR            -->  OR
     ORDINALP      -->  O-P
     ORD-LESSP     -->  O<
     PACK          -->  See intern and coerce.
     PAIRLIST      -->  PAIRLIS$
     PLUS          -->  + and BINARY-+
     QUOTIENT      -->  /
     REMAINDER     -->  REM and MOD
     STRIP-CARS    -->  STRIP-CARS
     SUB1          -->  1-
     TIMES         -->  * and BINARY-*
     TRUE          -->  The symbol T.
     UNION         -->  UNION-EQUAL and UNION-EQ
     UNPACK        -->  See symbol-name and coerce.
     V&C$          -->  No correspondent, but see the documentation for
                        DEFEVALUATOR and META.
     V&C-APPLY$    -->  No correspondent, but see the documentation for
                        DEFEVALUATOR and META.
     ZERO          -->  The number 0.
     ZEROP         -->  ZP

     ========================================

     Nqthm commands   -->     ACL2
     ----------------------------------------
     ACCUMULATED-PERSISTENCE
                   -->  ACCUMULATED-PERSISTENCE
     ADD-AXIOM     -->  DEFAXIOM
     ADD-SHELL     -->  There is no shell principle in ACL2.
     AXIOM         -->  DEFAXIOM
     BACKQUOTE-SETTING
                   -->  Backquote is supported in ACL2, but not
                        currently documented.
     BOOT-STRAP    -->  GROUND-ZERO
     BREAK-LEMMA   -->  MONITOR
     BREAK-REWRITE -->  BREAK-REWRITE
     CH            -->  PBT
                        See also :DOC history.
     CHRONOLOGY    -->  PBT
                        See also :DOC history.
     COMMENT       -->  DEFLABEL
     COMPILE-UNCOMPILED-DEFNS
                   -->  COMP
     CONSTRAIN     -->  See :DOC encapsulate and :DOC local.
     DATA-BASE     -->  Perhaps the closest ACL2 analogue of DATA-BASE
                        is PROPS.  But see :DOC history for a collection
                        of commands for querying the ACL2 database
                        (``world'').  Note that the notions of
                        supporters and dependents are not supported in
                        ACL2.
     DCL           -->  DEFSTUB
     DEFN          -->  DEFUN and DEFMACRO
     DEFTHEORY     -->  DEFTHEORY
     DISABLE       -->  DISABLE
     DISABLE-THEORY
                   -->  See :DOC theories.  The Nqthm command
                        (DISABLE-THEORY FOO) corresponds roughly to the
                        ACL2 command
                        (in-theory (set-difference-theories
                                     (current-theory :here)
                                     (theory 'foo))).
     DO-EVENTS     -->  LD
     DO-FILE       -->  LD
     ELIM          -->  ELIM
     ENABLE        -->  ENABLE
     ENABLE-THEORY -->  See :DOC theories.  The Nqthm command
                        (ENABLE-THEORY FOO) corresponds roughly to the
                        ACL2 command
                        (in-theory (union-theories
                                     (theory 'foo)
                                     (current-theory :here))).
     EVENTS-SINCE  -->  PBT
     FUNCTIONALLY-INSTANTIATE
                   -->  ACL2 provides a form of the :USE hint that
                        corresponds roughly to the
                        FUNCTIONALLY-INSTANTIATE event of Nqthm. See
                        :DOC lemma-instance.
     GENERALIZE    -->  GENERALIZE
     HINTS         -->  HINTS
     LEMMA         -->  DEFTHM
     MAINTAIN-REWRITE-PATH
                   -->  BRR
     MAKE-LIB      -->  There is no direct analogue of Nqthm's notion of
                        ``library.''  See :DOC books for a description
                        of ACL2's mechanism for creating and saving
                        collections of events.
     META          -->  META
     NAMES         -->  NAME
     NOTE-LIB      -->  INCLUDE-BOOK
     PPE           -->  PE
     PROVE         -->  THM
     PROVEALL      -->  See :DOC ld and :DOC certify-book.  The latter
                        corresponds to Nqthm's PROVE-FILE,which may be
                        what you're interested in,really.
     PROVE-FILE    -->  CERTIFY-BOOK
     PROVE-FILE-OUT
                   -->  CERTIFY-BOOK
     PROVE-LEMMA   -->  DEFTHM
                        See also :DOC hints.
     R-LOOP        -->  The top-level ACL2 loop is an evaluation loop as
                        well, so no analogue of R-LOOP is necessary.
     REWRITE       -->  REWRITE
     RULE-CLASSES  -->  RULE-CLASSES
     SET-STATUS    -->  IN-THEORY
     SKIM-FILE     -->  LD-SKIP-PROOFSP
     TOGGLE        -->  IN-THEORY
     TOGGLE-DEFINED-FUNCTIONS
                   -->  EXECUTABLE-COUNTERPART-THEORY
     TRANSLATE     -->  TRANS and TRANS1
     UBT           -->  UBT and U
     UNBREAK-LEMMA -->  UNMONITOR
     UNDO-BACK-THROUGH
                   -->  UBT
     UNDO-NAME     -->  See :DOC ubt.  There is no way to undo names in
                        ACL2 without undoing back through such names.
                        However, see :DOC ld-skip-proofsp for
                        information about how to quickly recover the
                        state.

EVENTS    functions that extend the logic

Any extension of the syntax of ACL2 (i.e., the definition of a new
constant or macro), the axioms (i.e., the definition of a function), or
the rule data base (i.e., the proof of a theorem), constitutes a
logical "event."  Events change the ACL2 logical world (see
WORLD).  Indeed, the only way to change the ACL2 world is via the
successful evaluation of an event function.  Every time the world is
changed by an event, a landmark is left on the world and it is thus
possible to identify the world "as of" the evaluation of a given event.
An event may introduce new logical names.  Some events introduce no new
names (e.g., verify-guards), some introduce exactly one (e.g., defmacro
and defthm), and some may introduce many (e.g., encapsulate ).

ACL2 typically completes processing of an event by printing a summary
that includes a breakdown of runtime (cpu time) used and, unless proofs
are skipped (see LD-SKIP-PROOFSP) or summary output is inhibited
(see SET-INHIBIT-OUTPUT-LST), information about the proof
attempt (if any) including a list of rules used, a summary of warnings,
and the number of "prover steps" (if any; see
WITH-PROVER-STEP-LIMIT).  A detail: The time is calculated using
Common Lisp function get-internal-run-time, which may ignore calls to
external tools (see SYS-CALL and see CLAUSE-PROCESSOR).

See EMBEDDED-EVENT-FORM for a discussion of events permitted in
books.

ADD-CUSTOM-KEYWORD-HINT    add a new custom keyword hint

     Examples:
     (add-custom-keyword-hint :my-hint (my-hint-fn val ...))

     (add-custom-keyword-hint :my-hint
                              (my-hint-fn val ...)
                              :checker (my-hint-checker-fn val ...))

     General Form:
     (add-custom-keyword-hint :key term1 :checker term2)

where :key is a keywordp not among the primitive keyword hints listed
in *hint-keywords*, the :checker argument is optional, and term1 and
(if supplied) term2 are terms with certain free-variable and signature
restrictions described below.  Henceforth, :key is treated as a custom
keyword hint, e.g., the user can employ :key in hints to defthm, such
as:

     (defthm name ...
       :hints (("Subgoal *1/1'" ... :key val ...))).

Custom keyword hints are complicated.  To use them you must understand
state, multiple values (e.g., mv and mv-let), ACL2's notion of error
triples (see PROGRAMMING-WITH-STATE), how to generate "soft"
errors with er, how to use fmt-strings to control output, how to use
computed hints (see COMPUTED-HINTS) and some aspects of ACL2's
internal event processing.  Furthermore, it is possible to implement a
custom keyword hint that can make an event non-reproducible!  So we
recommend that these hints be developed by ACL2 experts.  Basically the
custom keyword feature allows the implementors and other experts to
extend the hint facility without modifying the ACL2 sources.

Term1 is called the "generator" term and term2 is called the "checker"
term of the custom keyword hint :key.  Together they specify the
semantics of the new custom keyword hint :key.  Roughly speaking, when
a custom keyword hint is supplied by the user, as in

     (defthm name ...
       :hints (("Subgoal *1/1'" ... :my-hint val ...))).

the checker term is evaluated on val to check that val is of the
expected shape.  Provided val passes the check, the generator term is
used to compute a standard hint.  Like computed hints, the generator of
a custom keyword hint is allowed to inspect the actual clause on which
it is being fired.  Indeed, it is allowed to inspect the entire list of
hints (standard and custom) supplied for that clause.  Thus, in the
most general case, a custom keyword hint is just a very special kind of
computed hint.

The generator, term1, must have no free variables other than:

     (val keyword-alist
      id clause world stable-under-simplificationp
      hist pspv ctx state).

Moreover, either term1 must evaluate to a single non-stobj value, or
else it must be single-threaded in state and have the standard
error-triple output signature, (mv * * state).

The restrictions on the checker, term2, are that it be single-threaded
in state, have the standard error-triple output signature, (mv * *
state), and have no free variables other than:

     (val world ctx state).

For examples, see the books distributed with ACL2 in directory
books/hints/, in particular basic-tests.lisp.

To delete a previously added custom keyword hint, see
REMOVE-CUSTOM-KEYWORD-HINT.

The distributed book hints/merge-hint.lisp can be useful in writing
custom keyword hints.  See the examples near the of the file.

Note: This is an event!  It does not print the usual event summary but
nevertheless changes the ACL2 logical world and is so recorded.

ASSERT-EVENT    assert that a given form returns a non-nil value

     Examples:
     (assert-event (equal (+ 3 4) 7))
     (assert-event (equal (+ 3 4) 7) :msg (msg "Error: ~x0" 'equal-check))
     (assert-event (equal (+ 3 4) 7) :on-skip-proofs t)

     General Forms:
     (assert-event form)
     (assert-event form :on-skip-proofs t)

Assert-event takes a ground form, i.e., one with no free variables;
stobjs are allowed but only a single non-stobj value can be returned.
The form is then evaluated and if the result is nil, then a so-called
hard error (see ER) results.  This evaluation is however not
done if proofs are being skipped, as during include-book (also see
SKIP-PROOFS and see LD-SKIP-PROOFSP), unless
:on-skip-proofs t is supplied.

Normally, if an assert-event call fails then a generic failure message
is printed, showing the offending form.  However, if keyword argument
:msg is supplied, then the failure message is printed as with fmt
argument ~@0; see FMT.  In particular, :msg is typically a
string or a call (msg str arg-0 arg-1 ... arg-k), where str is a string
and each arg-i is the value to be associated with #i upon formatted
printing (as with fmt) of the string str.

This form may be put into a book to be certified (see BOOKS),
because assert-event is a macro whose calls expand to calls of
value-triple (see EMBEDDED-EVENT-FORM).  When certifying a
book, guard-checking is off, as though (set-guard-checking nil) has
been evaluated; see SET-GUARD-CHECKING.  That, together with a
"safe mode," guarantees that assert-event forms are evaluated in the
logic without guard violations while certifying a book.

COMP    compile some ACL2 functions

NOTE: Comp is a no-op if explicit compilation is suppressed; see
COMPILATION.  The documentation here assumes that this is not the
case.

     Examples:
     :comp t          ; compile all uncompiled ACL2 functions
     (comp t)         ; same as above, but can be put into a book
     (comp :exec)     ; compile all uncompiled logic (``*1*'') definitions
     :comp foo        ; compile the defined function foo
     :comp (:raw foo) ; compile the raw Lisp version of the defined function foo
                        but not the corresponding logic definition
     :comp (foo bar)  ; compile the defined functions foo and bar
     :comp (foo (:raw bar))  ; compile the defined functions foo and bar, but for
                             ; bar do not compile the corresponding logic definition

     General Form:
     :comp specifier
     where specifier is one of the following:

       t                     compile all user-defined ACL2 functions that are
                               currently uncompiled (redefined built-in functions
                               are not recompiled)
       :exec                 same as t, except that only logic versions are
                               compiled (see below), not raw Lisp definitions
       :raw                  same as t, except that only raw Lisp definitions are
                               compiled, not logic version (see below)
       (name-1 ... name-k)   a non-empty list of names of functions defined by
                               DEFUN in ACL2, except that each name-i can be of
                               the form (:raw sym) or (:exec sym), where sym is
                             the name of such a function
       name                  same as (name)

When you define a function in ACL2, you are really causing two
definitions to be made "under the hood" in Common Lisp: the definition
is submitted explicitly to raw Lisp, but so is a corresponding "logic
definition".  If guards have not been verified, then only the logic
definition will be evaluated; see GUARDS-AND-EVALUATION, in
particular the section titled "Guards and evaluation V: efficiency
issues".

Thus, if you are not verifying guards and you want the benefit of Lisp
compilation for speed and space efficiency, then you may want to place
the form (comp :exec) in your books.

Generally it is not necessary to place the form (comp t), or the form
(comp :raw), in a book, because certify-book compiles the raw Lisp
definitions anyhow, by default.  But you may wish to put (comp t) or
(comp fn1 fn2 ... fnk) in a book when such a form precedes expensive
calls of functions, for example for proofs involving calls of functions
on large constants, or to support computationally expensive
macroexpansion.

As suggested by the examples above, if a function specifier is of the
form (:raw fn), then fn will be compiled in raw Common Lisp but its
corresponding logic definition will not be compiled; and for (:exec fn),
it's the other way around.

The use of :comp may create various files whose names start with
"TMP*", but it then deletes them.  If you want to save these files,
evaluate (assign keep-tmp-files t).

Also see SET-COMPILE-FNS for a way to compile each function as
it is defined.  But note that set-compile-fns is ignored during
include-book.

Note that if functions are traced (see TRACE$), then comp will
first untrace the functions that are to be compiled, then will do the
compile(s), and finally will re-trace the functions that it untraced
(using their original trace specs).  In particular, if you have traced
a function and then you compile it using :comp, the resulting traced
function will be compiled as well unless you specified :compile nil in
your trace spec; and after you untrace the function it will definitely
run compiled.

We conclude with a technical remark only for those who use trust tags to
write raw Lisp code.  :Comp generally creates files to compile unless it
is given a single function to compile.  Those files contain the ACL2
definitions of all functions to compile, omitting those in the lists
obtained by evaluating the forms (@ logic-fns-with-raw-code) and (@
program-fns-with-raw-code).  If you define function symbols with raw
Lisp code, say by using trust tags (see DEFTTAG) and readtime
conditionals #-acl2-loop-only, then you are advised to add all such
symbols to one of the lists stored in the two state globals above: to
logic-fns-with-raw-code if the function symbol is in :logic mode, else
to program-fns-with-raw-code.  Then, instead of the corresponding ACL2
definition (without raw Lisp code) being written to a file, the
function symbol will be passed directly to the Lisp compile function.
Note that the above two state globals are both untouchable, so you may
need to deal with that before modifying them, for example as follows
(also see REMOVE-UNTOUCHABLE).

     (defttag t)
     (state-global-let*
      ((temp-touchable-vars t set-temp-touchable-vars))
      (progn! (f-put-global 'logic-fns-with-raw-code
                            (cons 'my-fn (@ logic-fns-with-raw-code))
                            state)))

COMP-GCL    compile some ACL2 functions leaving .c and .h files

Comp-gcl is for use by experts who want to examine the results of GCL
compilation, and it may only be used with ACL2 implementations built on
top of GCL.  It takes exactly the same arguments as comp, and has the
same basic functionality (see COMP), but has two additional
effects.  First, files "TMP.lisp" and "TMP1.lisp" are always created,
even when a single function is specified.  Second, comp-gcl always
leaves files "TMP.c", "TMP.h", "TMP1.c", and "TMP1.h" when compilation
is complete.

DEFABBREV    a convenient form of macro definition for simple expansions

     Examples:
     (defabbrev snoc (x y) (append y (list x)))
     (defabbrev sq (x) (declare (type (signed-byte 8) x)) (* x x))

     General Form:
     (defabbrev name (v1 ... vn) doc-string decl1 ... declk body)

where name is a new function symbol, the vi are distinct variable
symbols, and body is a term.  The decli, if supplied, should be legal
declare forms; see DECLARE.  Doc-string is an optional
documentation string; see DOC-STRING.

Roughly speaking, the defabbrev event is akin to defining f so that (f
v1 ... vn) = body.  But rather than do this by adding a new axiom,
defabbrev defines f to be a macro so that (f a1 ... an) expands to
body, with the "formals," vi, replaced by the "actuals," ai.

For example, if snoc is defined as shown in the first example above,
then (snoc (+ i j) temp) is just an abbreviation for

     (append temp (list (+ i j))).

In order to generate efficiently executable Lisp code, the macro that
defabbrev introduces uses a let to bind the "formals" to the "actuals."
Consider the second example above.  Logically speaking, (sq (ack i j))
is an abbreviation for (* (ack i j) (ack i j)).  But in fact the macro
for sq introduced by defabbrev actually arranges for (sq (ack i j)) to
expand to:

     (let ((x (ack i j)))
       (* x x))

which executes more efficiently than (* (ack i j) (ack i j)).

In the theorem prover, the let above expands to

     ((lambda (x) (* x x)) (ack i j))

and thence to (* (ack i j) (ack i j)).

It is important to note that the term in body should not contain a call
of name -- i.e., defabbrev should not be used in place of defun when
the function is recursive.  ACL2 will not complain when the defabbrev
form is processed, but instead ACL2 will more than likely go into an
infinite loop during macroexpansion of any form that has a call of name.

It is also important to note that the parameters of any call of a macro
defined by defabbrev will, as is the case for the parameters of a
function call, be evaluated before the body is evaluated, since this is
the evaluation order of let.  This may lead to some errors or
unexpected inefficiencies during evaluation if the body contains any
conditionally evaluted forms like cond, case, or if.  Consider the
following example.

     (defabbrev foo (x y)
       (if (test x) (bar y) nil))

Notice a typical one-step expansion of a call of foo (see
TRANS1):

     ACL2 !>:trans1 (foo expr1 expr2)
      (LET ((X EXPR1) (Y EXPR2))
           (IF (TEST X) (BAR Y) NIL))
     ACL2 !>

Now imagine that expr2 is a complicated expression whose evaluation is
intended only when the predicate test holds of expr1.  The expansion
above suggests that expr2 will always be evaluated by the call (foo
expr1 expr2), which may be inefficient (since perhaps we only need that
value when test is true of expr1).  The evaluation of expr2 may even
cause an error, for example in :program mode if the expression expr2 has
been constructed in a manner that could cause a guard violation unless
test holds of expr1.

DEFABSSTOBJ    define a new abstract single-threaded object

We assume familiarity with single-threaded objects; see STOBJ
and see DEFSTOBJ.  The event defabsstobj defines a so-called
"abstract stobj", a notion we introduce briefly now and then explain in
more depth below.

The evaluation of a defstobj event produces logical definitions for
several functions: a recognizer, which characterizes the stobj in terms
of lists; a creator, which produces an initial suitable list structure;
and field accessors and updators, defined in terms of nth and
update-nth.  Defabsstobj provides a way to define alternate definitions
for a recognizer, creator, and primitive read/write functions.  In
essence, defabsstobj establishes interface functions, or "exports", on
a new stobj that is a copy of an indicated "concrete" stobj that already
exists.

We begin below with an introduction to abstract stobjs.  We then explain
the defabsstobj event by way of an example.  We conclude by giving
summary documentation for the defabsstobj event.

*INTRODUCTION*

We start with a brief review of stobjs and some potential problems with
them, followed by an introduction to abstract stobjs and how they can
avoid these problems.  Prior experience with stobjs will probably help
the reader to absorb the ideas below.

Recall that single-threaded objects, or stobjs, provide a way for ACL2
users to stay within the ACL2 logic, where every data object is an atom
or a cons of data objects, while obtaining the benefits of fast
evaluation through destructive updates.  Consider for example this very
simple event.

     (defstobj st fld)

This event introduces a recognizer, stp, and a creator, create-st, for
a data structure consisting of a single field accessed and updated by
functions fld and update-fld, respectively.  Each of these four
primitive functions has both a logical definition, which is used when
the prover reasons about the function, and an executable definition,
which is used in raw Lisp.  In the logic, stp recognizes objects that
have the requisite fields.  In raw Lisp, there is a "live stobj", which
is an array object whose fields correspond to those specified by the
defstobj event, implemented as Lisp arrays.

Here are the logical definition and the executable definition,
respectively, that are introduced for the field accessor, fld,
introduced above.  Notice that since a stobj is represented in raw Lisp
using an array, the raw Lisp accessor uses a raw Lisp array accessor,
svref.  (You can see all the logical and executable definitions by
evaluating the form (trace$ defstobj-axiomatic-defs defstobj-raw-defs)
before evaluating the defstobj form.)

     ; logical definition
     (defun fld (st)
       (declare (xargs :guard (stp st)
                       :verify-guards t))
       (nth 0 st))

     ; executable (raw Lisp) definition
     (defun fld (st)
       (svref st 0))

Sophisticated programming with stobjs can provide efficient
implementations of algorithms, but may require the preservation of a
complex invariant.  One can, of course, define a function to implement
such an invariant after introducing the stobj, as follows.

     ; Introduce a stobj.
     (defstobj st fld1 ... fldk)

     ; Define an invariant on that stobj.
     (defun good-stp (st)
       (declare (xargs :stobjs st))
       ...)

     ; Define some basic functions that update the stobj and preserve the
     ; invariant.
     (defun update-st (... st ...)
       (declare (xargs :stobjs st
                       :guard (and (good-stp st) ...)))
       ...)
     ...

     ; Prove that the invariant is indeed preserved by those basic functions.
     (defthm good-stp-update-st
       (implies (and (good-stp st)
                     ...)
                (good-stp (update-st ... st ...))))
     ...

     ; Implement algorithms built on the basic functions.
     (defun foo (... st ...)
       (declare (xargs :stobjs st
                       :guard (and (good-stp st) ...)))
       ... (update-st ... st ...) ...)

     ; Prove invariance theorems about these algorithms.
     (defthm good-stp-foo
       (implies (and (good-stp st)
                     ...)
                (good-stp (foo ... st ...))))
     ...

     ; Prove other properties of these algorithms.
     (defthm foo-is-correct
       (implies (and (good-stp st)
                     ...)
                (some-property (foo ... st ...))))
     ...

But there are at least two potential difficulties in using stobjs as
described above.

     1. When foo is executed on concrete data in the ACL2 loop, the
     guard check may be expensive because (good-stp st) is expensive.

     2. Reasoning about foo (using rules like foo-is-correct above)
     involves proving hypotheses of invariance theorems, which may be
     complicated for the user to manage or slow for the theorem prover.

The defabsstobj event offers an opportunity to address these issues.  It
introduces a new stobj, which we call an "abstract stobj", which is
associated with a corresponding "concrete stobj" introduced by an
earlier defstobj event.  The defabsstobj event specifies a logical
(:LOGIC) and an executable (:EXEC) definition for each primitive
operation involving that stobj.  As is the case for defstobj, the
logical definition is what ACL2 reasons about, and is appropriate to
apply to an ACL2 object satisfying the logical definition of the
recognizer function for the stobj.  The executable definition is
applied in raw Lisp to a live stobj, which is an array object
associated with the given stobj name.

Consider an abstract stobj st with corresponding concrete stobj st$c.
The live stobjs for st and st$c have the same structure, but are
distinct arrays.  Indeed, the raw Lisp creator function for st$c is
called to create a new initial live stobj for st.  As we will see below,
reads and writes in raw Lisp to the live stobj for st are ultimately
performed using the primitive acccessors and updaters defined for st$c.
One might think of the live stobjs for st and st$c as being congruent
stobjs (see DEFSTOBJ), except that the stobjs themselves are
not congruent: only exported functions (not arbitrary field updaters of
st$c, for example) may be applied to st.  As one might expect, the :EXEC
function for an exported function is applied to the live stobj for st in
raw Lisp.  As of this writing, congruent stobjs are not supported for
abstract stobjs.  Users who see a need for this feature are welcome to
explain that need to the ACL2 implementors.

*EXAMPLE*

We present examples, with detailed comments intended to explain abstract
stobjs, in two distributed books: books/misc/defabsstobj-example-1.lisp
and books/misc/defabsstobj-example-2.lisp.  In this section we outline
the first of these.  We suggest that after you finish this documentation
topic, you read through those two books.

Here is the first of two closely related defabsstobj events from the
book defabsstobj-example-1.lisp, but in expanded form.  We will show the
abbreviated form later, which omits most of data in the form that is
immediately below.  Thus most of the information shown here is default
information.  We believe that the comments below explain most or all of
what you need to know in order to start using defabsstobj, and that you
will learn the remainder when you see error messages.  For example, we
do not say in the comments below that every :LOGIC and :EXEC function
must be guard-verified, but that is indeed a requirement.

     (defabsstobj st ; The new abstract stobj is named st.

     ; The concrete stobj corresponding to st is st$c:

       :concrete st$c

     ; The recognizer for the new abstract stobj is stp, which is defined to be
     ; st$ap in the logic, and is executed on the live stobj in raw Lisp using
     ; st$cp.

       :recognizer (stp :logic st$ap :exec st$cp)

     ; The initial stobj is defined as create-st (a function of no arguments),
     ; which is defined logically as create-st$a, though create-st$c is invoked to
     ; create the initial live stobj for st.  The :correspondence and :preserved
     ; keywords refer to proof obligations, discussed below.

       :creator (create-st :logic create-st$a :exec create-st$c
                           :correspondence create-st{correspondence}
                           :preserved create-st{preserved})

     ; Proof obligations are generated that involve a correspondence between the
     ; new abstract stobj and corresponding concrete stobj.  The function
     ; st$corr, which need not be executable (see :DOC defun-nx), takes two
     ; arguments, a concrete stobj and an abstract stobj.  This function symbol is
     ; used in the statements of the proof obligations.

       :corr-fn st$corr

     ; In this example we have four exports.  In each case a new function is
     ; introduced that has the same signature as its :EXEC function, except that
     ; st$c is replaced by st.  The :LOGIC and :EXEC functions are as specified,
     ; and the other keywords refer to proof obligations that we discuss below.

       :exports ((lookup :logic lookup$a
                         :exec mem$ci
                         :correspondence lookup{correspondence}
                         :guard-thm lookup{guard-thm})
                 (update :logic update$a
                         :exec update-mem$ci
                         :correspondence update{correspondence}
                         :preserved update{preserved}
                         :guard-thm update{guard-thm})
                 (misc :logic misc$a
                       :exec misc$c
                       :correspondence misc{correspondence})
                 (update-misc :logic update-misc$a
                              :exec update-misc$c
                              :correspondence update-misc{correspondence}
                              :preserved update-misc{preserved}))
       :doc nil)

Note that the recognizer, creator, and all exported functions are
defined in the logic in terms of their :LOGIC functions and in raw Lisp
in terms of their :EXEC functions.  In the former case, a defun form
defines a function, while in the latter case, a defmacro form defines a
macro (for efficiency).  Here is how that works, for example, for the
recognizer.  (You can see all the logical and executable definitions by
evaluating the form (trace$ defabsstobj-axiomatic-defs
defabsstobj-raw-defs) before evaluating the defstobj form.)

     ; In the logic:
     (defun stp (st)
       (declare (xargs :guard 't))
       (st$ap st))

     ; In raw Lisp:
     (defmacro stp (&rest args) (cons 'st$cp args))

We turn now to the proof obligations, as promised above.  There are
three types: :CORRESPONDENCE, :PRESERVED, and :GUARD-THM.  All required
lemmas may be printed simply by defining the necessary :LOGIC and :EXEC
functions and then submitting the defabsstobj event.  (To advanced
users: also see DEFABSSTOBJ-MISSING-EVENTS for a utility that
returns the required formulas in translated form.)  Although the
defabsstobj event will fail if the required lemmas have not been proved,
first it will print the defthm forms that must be admitted in order to
complete submission of the defabsstobj event.

The detailed theory explaining the need for these lemmas may be found
in a comment in ACL2 source file other-events.lisp, in a comment
entitled "Essay on the Correctness of Abstract Stobjs".  Here, we give
an informal sense of the importance of these lemmas as we present
examples of them.  Fundamental is the notion of evaluation in the logic
versus evaluation using live stobjs, where one imagines tracking the
current value of each abstract stobj during each of these two
evaluations.

We start with the :CORRESPONDENCE lemmas.  These guarantee that
evaluation in the logic agrees with evaluation using live stobjs, in the
sense that the only difference is between a logical stobj and a live
stobj, where the two correspond in the sense of the function specified
by :CORR-FN.  We start with the :CREATOR function where the statement is
quite simple, stating that the :CORR-FN holds initially.

     (defthm create-st{correspondence}
       (st$corr (create-st$c) (create-st$a)))

For the exported functions, there are essentially two cases.  If an
exported function returns other than the new abstract stobj, then the
theorem asserts the equality of the results of applying the :LOGIC and
:EXEC functions for the exported function.  Hypotheses include the
:CORR-FN correspondence followed by the guard for the :LOGIC function,
which is stated in terms of the formal parameters of the :EXEC function
except using the abstract stobj (here, st) in place of the concrete
stobj (here, st$c).  The conclusion uses the :EXEC formals, modified in
the call of the :LOGIC function (here, lookup$a) to use the abstract
stobj, as in the hypotheses.

     (defthm lookup{correspondence}
       (implies (and (st$corr st$c st)
                     (integerp i) (<= 0 i) (<= i 49)
                     (st$ap st))
                (equal (mem$ci i st$c)
                       (lookup$a i st)))
       :rule-classes nil)

By contrast, if the exported function returns the new abstract stobj,
then the conclusion uses the correspondence function insted of EQUAL,
as in the following.

     (defthm update{correspondence}
       (implies (and (st$corr st$c st)
                     (integerp i) (<= 0 i) (<= i 49)
                     (integerp v) (<= 0 v)
                     (st$ap st)
                     (mem$c-entryp v))
                (st$corr (update-mem$ci i v st$c)
                         (update$a i v st)))
       :rule-classes nil)

For exported functions that return multiple values, such conclusions are
conjoined together over the returned values.

The :PRESERVED lemmas guarantee that updates to the abstract stobj
preserve its recognizer.  The fact that every exported function has this
property provides justification for an optimization performed by ACL2
during generation of proof obligations for guard verification, by
assuming that the recognizer always holds.  The :PRESERVED lemma for
the :CREATOR shows that the recognizer holds initially.

     (defthm create-st{preserved}
       (st$ap (create-st$a)))

Here is a typical such lemma, for the exported function update.  Note
that there is no such lemma for lookup, since lookup does not return st.

     (defthm update{preserved}
       (implies (and (integerp i) (<= 0 i) (<= i 49)
                     (integerp v) (<= 0 v)
                     (st$ap st)
                     (mem$c-entryp v))
                (st$ap (update$a i v st))))

Finally, we consider the :GUARD-THM lemmas.  These serve to guarantee
that the guard holds for each :EXEC function.  During guard
verification, logical definitions are used; in particular, since each
exported function is defined in the logic as the corresponding call of
its :LOGIC function, guard verification shows that each call of the
:LOGIC function for an exported function satisfies that function's
guard.  But why is this true for raw Lisp evaluation using live stobjs,
where the :EXEC function is called for an exported function?  The
:GUARD-THM lemmas provide the answer, as they state that if the :LOGIC
function's guard holds, then the :EXEC function's guard holds.  Here is
an example.  Note that the hypotheses come from the correspondence of
the concrete and abstract function as guaranteed by the :CORR function,
together with the guard of the :LOGIC function; and the conclusion
comes from the guard of the :EXEC function.

     (defthm lookup{guard-thm}
       (implies (and (st$corr st$c c)
                     (integerp i)
                     (<= 0 i)
                     (<= i 49)
                     (st$ap st))
                (and (integerp i)
                     (<= 0 i)
                     (< i (mem$c-length st$c))))
       :rule-classes nil)

We conclude this EXAMPLE section by showing a short form for the
defabsstobj form displayed above.

     (defabsstobj st
       :exports ((lookup :exec mem$ci)
                 (update :exec update-mem$ci)
                 misc update-misc))

*SUMMARY DOCUMENTATION*

The General Form is as shown below, where the order of keywords is
unimportant.  Duplicate keywords are discouraged; while permitted, only
the first (leftmost) occurrence of a given keyword is used.  Only the
:exports keyword is required.

     (defabsstobj st
       :concrete concrete
       :recognizer recognizer
       :creator creator
       :corr-fn corr-fn
       :exports (e1 ... ek)
       :doc doc)

The keyword argument :EXPORTS must be supplied, and missing or nil
keyword arguments have defaults as indicated below.  All arguments must
satisfy the conditions below.

Before we describe the arguments, we define a notion of a "function
spec" and its "completion".  A function spec is either a symbol or else
a list of the form

     (fn :kwd1 val1 ... :kwdn valn),

that is, a symbol followed by a keyword-value-listp.  We view the case
of a symbol, s, as the function spec (s), with no keywords.  There must
be no duplicate keywords.  In each case that we expect a function spec,
the context provides a set of valid keywords for that function spec; it
is an error to provide any other keyword in the function spec.  Each
function spec is interpreted as its "completion", obtained by extending
the function spec with a default value for each valid keyword as
indicated below.  With that interpretation, the "exported function" of
a function spec is its car, and that function symbol and each keyword
value must be a guard-verified function symbols; and moreover, the
:EXEC function must not include the new abstract stobj name, st, among
its formals.

We are ready to describe the arguments of defabsstobj.

     St is a symbol, which names the new abstract stobj.

     Concrete is the name of an existing stobj that is not an abstract
     stobj, i.e., was introduced with defstobj (not defabsstobj).

     Recognizer is a function spec (for the recognizer function).  The
     valid keywords are :LOGIC and :EXEC.  The default for recognizer is
     obtained by adding the suffix "P" to name.  The default value for
     :LOGIC is formed by adding the suffix "$AP" to recognizer; for
     :EXEC, by adding the suffix "$CP".

     Creator is a function spec (for the creator function).  The valid
     keywords are :LOGIC and :EXEC.  The default for creator is
     obtained by adding the prefix "CREATE-" to name.  The default value
     for :LOGIC is formed by adding the suffix "$A" to creator; for
     :EXEC, by adding the suffix "$C".

     Corr-fn is a known function symbol that takes two arguments (for
     the correspondence theorems).

     The value of :EXPORTS is a non-empty true list.  Each ei is a
     function spec (for an exported function).  The valid keywords are
     :LOGIC, :EXEC, :CORRESPONDENCE, and :GUARD-THM, and also :PRESERVED
     if and only if the specified :EXEC function returns the :CONCRETE
     stobj.  The default values for these keywords are obtained by
     respectively adding the suffix "$A" "$C", "{CORRESPONDENCE}",
     "{GUARD-THM}", or "{PRESERVED}".

     Doc, if non-nil, is a documentation string (see
     DOC-STRING).

Not shown is the keyword, :MISSING; the effect of :missing t is to turn
the call of defabsstobj into a corresponding call of
defabsstobj-missing-events.

Note that a defabsstobj event will fail if the required lemmas -- that
is, those for valid keywords :CORRESPONDENCE, :GUARD-THM, and
:PRESERVED -- have not been proved, unless proofs are being skipped.
Note that the exemption when skipping proofs allows the supporting
lemmas to be local to books and encapsulate events.  If the ld special
ld-skip-proofsp is t, then the missing events are printed with a
warning before the defabsstobj event is admitted; but if
ld-skip-proofsp is the symbol INCLUDE-BOOK, then that warning is
omitted.  (Also see SKIP-PROOFS and see
LD-SKIP-PROOFSP.)  If however proofs are not being skipped, then the
defabsstobj event will fail after printing the missing events.
Advanced users may wish to see DEFABSSTOBJ-MISSING-EVENTS for a
utility that returns a data structure containing the missing lemmas.
There are a few additional restrictions, as follows.

     All exported function names must be new (unless redefinition is on;
     see LD-REDEFINITION-ACTION), and there must be no
     duplicates among them.

     The :CONCRETE stobj name must be a formal parameter of the :EXEC fn
     of every function spec, except for the :CREATOR function spec.
     Also the input signatures of the :LOGIC and :EXEC function for a
     function spec must agree, except perhaps at the position of that
     :CONCRETE formal.

     For function specs other than the :CREATOR function spec, the
     output signatures of the :LOGIC and :EXEC functions must have the
     same length and must agree, except perhaps at position p_out of the
     :CONCRETE stobj in the :EXEC function's output.  If p_in is the
     position of the :CONCRETE stobj in the :EXEC function's formals,
     then the :LOGIC function's output at position p_out should match
     the :LOGIC function's formal at position p_in.

We conclude with some remarks.

Unlike defstobj, there is no :renaming argument.  Instead, the scheme
described above provides a flexible way to assign names.

Those who use the experimental extension ACL2(h), which includes
function memoization (see MEMOIZE), may be aware that the memo
table for a function is flushed whenever it is the case that one of its
stobj inputs is updated.  In fact, such flushing happens even when a
stobj that is congruent to one of its stobj inputs is updated.  For
that purpose, an abstract stobj is considered to be congruent to its
corresponding concrete stobj.

DEFABSSTOBJ-MISSING-EVENTS    obtain the events needed to admit a defabsstobj event

We assume familiarity with defabsstobj.  Defabsstobj-missing-events is
a macro is for advanced users (who, for example, understand the role of
the translate and untranslate functions), who want programmatic access
to the defthm events required to admit a specific defabsstobj event.

This macro has the same syntax as defabsstobj -- to use it, just
replace a call of defabsstobj by a call of defabsstobj-missing-events
on the same arguments.  The result is an error triple (mv erp val
state).  If erp is nil, then val is the list of all objects (name
formula . old-formula), where a defthm event named name remains to be
admitted whose translated formula is formula, and where old-formula is
nil unless the indicated event already exists (hence with a different
formula), in which case old-formula is the existing translated formula.

To build a defthm event from the above value, val, we suggest
evaluating a form like (untranslate formula t (w state)).

DEFATTACH    execute constrained functions using corresponding attached functions

This documentation topic is organized into the following sections:

*Introductory example.*
*Syntax and semantics of defattach.*
*Three primary uses of defattach.*
*Miscellaneous remarks, with discussion of possible user errors.*

Please see ENCAPSULATE if you intend to use defattach but are
not already familiar with the use of encapsulate to introduce
constrained functions.

See distributed book books/misc/defattach-example.lisp for a small
example.  it illustrates how defattach may be used to build something
like "higher-order" programs, in which constrained functions may be
refined to different executable functions.  More uses of defattach may
be found in the ACL2 source code, specifically, file
boot-strap-pass-2.lisp.

The argument :skip-checks t enables easy experimentation with
defattach, by permitting use of :program mode functions and the
skipping of semantic checks.  Also permitted is :skip-checks nil (the
default) and :skip-checks :cycles, which turns off only the update of
the extended ancestor relation and hence the check for cycles in this
relation; see below.  We do not make any logical claims when the value
of :skip-checks is non-nil; indeed, a trust tag is required in this
case (see DEFTTAG).  Remark for those who use the experimental
HONS extension (see HONS-AND-MEMOIZATION): the interaction of
memoization and attachments is not tracked for attachments introduced
with a non-nil value of :skip-checks.  For more discussion of
:skip-checks t, see DEFPROXY; we do not discuss :skip-checks
further, here.

*Introductory example.*

We begin with a short log illustrating the use of defattach.  Notice
that after evaluating the event (defattach f g), a call of the
constrained function f is evaluated by instead calling g on the
arguments.

     ACL2 !>(encapsulate
             ((f (x) t :guard (true-listp x)))
             (local (defun f (x) x))
             (defthm f-property
               (implies (consp x) (consp (f x)))))
     [... output omitted ...]
      T
     ACL2 !>(defun g (x)
              (declare (xargs :guard (or (consp x) (null x))))
              (cons 17 (car x)))
     [... output omitted ...]
      G
     ACL2 !>(f '(3 4)) ; undefined function error

     ACL2 Error in TOP-LEVEL:  ACL2 cannot ev the call of undefined function
     F on argument list:

     ((3 4))

     To debug see :DOC print-gv, see :DOC trace, and see :DOC wet.

     ACL2 !>(defattach f g)
     [... output omitted ...]
      :ATTACHMENTS-RECORDED
     ACL2 !>(f '(3 4)) ; f is evaluated using g
     (17 . 3)
     ACL2 !>(trace$ f g)
      ((F) (G))
     ACL2 !>(f '(3 4)) ; f is evaluated using g
     1> (ACL2_*1*_ACL2::F (3 4))
       2> (ACL2_*1*_ACL2::G (3 4))
         3> (G (3 4))
         <3 (G (17 . 3))
       <2 (ACL2_*1*_ACL2::G (17 . 3))
     <1 (ACL2_*1*_ACL2::F (17 . 3))
     (17 . 3)
     ACL2 !>(defattach f nil) ; unattach f (remove its attachment)
     [... output omitted ...]
      :ATTACHMENTS-RECORDED
     ACL2 !>(f '(3 4)) ; undefined function error once again
     1> (ACL2_*1*_ACL2::F (3 4))

     ACL2 Error in TOP-LEVEL:  ACL2 cannot ev the call of undefined function
     F on argument list:

     ((3 4))

     To debug see :DOC print-gv, see :DOC trace, and see :DOC wet.

     ACL2 !>

*Syntax and semantics of defattach.*

The log above shows that the event (defattach f g) allows g to be used
for evaluating calls of f.  From a logical perspective, the evaluation
takes place in the addition to the current session of an "attachment
equation" axiom (universally quantified over all x) for each defattach
event:

     (equal (f x) (g x)) ;;; attachment equation axiom for (defattach f g)

Below we explain defattach in some detail.  But it is important to keep
in mind that evaluation with the attachment equations takes place in an
extension of the logical theory of the session.  ACL2 guarantees that
this so-called "evaluation theory" remains consistent, assuming that
the absence of defaxiom events from the user.  A deeper discussion of
the logical issues is available (but not intended to be read by most
users) in a comment in the ACL2 source code labeled "Essay on
Defattach."

     Example Forms:
     (defattach f g)   ; call g in place of calling constrained function f
     (defattach (f g)) ; same as just above
     (defattach (f g :hints (("Goal" :in-theory (enable foo)))))
                       ; equivalent to first form above, except with hints for the
                       ; proof that the guard of f implies the guard of g
     (defattach (f g :hints (("Goal" :in-theory (enable foo)))
                     :otf-flg t))
                       ; as above, except with an :otf-flg of t for the proof that
                       ; the guard of f implies the guard of g
     (defattach (f g)
                :hints (("Goal" :use my-thm)))
                       ; equivalent to first form above, except with hints for the
                       ; proof that the constraints on f hold for g
     (defattach (f g)
                :hints (("Goal" :use my-thm))
                :otf-flg t)
                       ; as above, except with an :otf-flg of t for the proof that
                       ; the constraints on f hold for g
     (defattach (f g)
                (h j)) ; Attach g to f and attach j to h
     (defattach (f g :attach nil)
                (h j)) ; Same as just above, including the same proof obligations,
                       ; except for one difference: because of :attach nil, calls
                       ; of f will not be evaluated, i.e., there will be no
                       ; executable attachment of g to f
     (defattach (f nil)
                (h j)) ; Attach j to h and unattach f
     (defattach (f g :hints (("Goal" :in-theory (enable foo))))
                (h j :hints (("Goal" :in-theory (enable bar))))
                :hints (("Goal" :use my-thm)))
                       ; Attach g to f and attach j to h, with hints:
                       ; - For proving that the guard of f implies the guard of g,
                       ;   enable foo;
                       ; - For proving that the guard of h implies the guard of j,
                       ;   enable bar; and
                       ; - For proving that the constraints on f and h hold for
                       ;   g and j (respectively), use theorem my-thm.

     (defattach f nil)   ; remove the attachment of f, if any (e.g., g above)
     (defattach (f nil)) ; same as just above

     General Forms:
     (defattach f g)   ; single attach or, if g is nil, unattach
     (defattach (f1 g1 :kwd val ...)
                ...
                (fk gk :kwd' val' ...)
                :kwd'' val'' ...)

where each indicated keyword-value pair is optional and each keyword is
one of :ATTACH, :HINTS, :OTF-FLG, or :INSTRUCTIONS.  The value of each
:ATTACH keyword is either t or nil, with default t except that the
value of :ATTACH at the "top level," after each entry (fi gi ...), is
the default for each :ATTACH keyword supplied in such an entry.  The
associated values for the other keywords have the usual meanings for
the proof obligations described below: the guard proof obligation for
keywords within each (fi gi ...) entry, and the constraint proof
obligation for keywords at the top level.  No keyword may occur twice
in the same context, i.e., within the same (fi gi ...) entry or at the
top level; and :INSTRUCTIONS may not occur in the same context with
:HINTS or :OTF-FLG.

The first General Form above is simply an abbreviation for the form
(defattach (f g)), which is an instance of the second General Form
above.  For the second General Form we say that gi is "attached to" fi
(by the defattach event) if gi is not nil, and otherwise we say that fi
is "unattached" (by the defattach event).  It is also convenient to
refer to <fi,gi> as an "attachment pair" (of the event) if gi is not
nil.  We may refer to the set of fi as the "attachment nest" of each fi.

We start with a brief introduction to the first General Form in the
case that g is not nil.  This form arranges that during evaluation, with
exceptions noted below, every call of the constrained function symbol f
will in essence be replaced by a call of the function symbol g on the
same arguments.  We may then refer to g as the "attachment of" f, or
say that "g is attached to f."  Notable exceptions, where we do not use
attachments during evaluation, are for macroexpansion, evaluation of
defconst and defpkg terms, evaluation during table events, some stobj
operations including all updates, and especially evaluation of ground
terms (terms without free variables) during proofs.  However, even for
these cases we allow the use of attachments in the first argument of
prog2$ and, more generally, the next-to-last (i.e., second) argument of
return-last when its first argument is not of the form 'm for some
macro, m.

To see why attachments are disallowed during evaluation of ground terms
during proofs (except for the prog2$ and return-last cases mentioned
above), consider the following example.

     (defstub f (x) t)
     (defun g (x) (+ 3 x))
     (defattach f g)

If the form (f 2) is submitted at the ACL2 prompt, the result will be 5
because the attachment g of f is called on the argument, 2.  However,
during a proof the term (f 2) will not be simplified to 5, since that
would be unsound, as there are no axioms about f that would justify
such a simplification.

For the case that g is nil in the first General Form above, the result
is the removal of the existing attachment to f, if any.  After this
removal, calls of f will once again cause errors saying that "ACL2
cannot ev the call of undefined function f ...".  In this case not only
is the previous attachment to f removed; moreover, for every function
symbol f' in the attachment nest of f in the defattach event that
introduced the existing attachment to f, then f' is unattached.  (An
example near the end of this documentation topic shows why this
unattachment needs to be done.) Such removal takes place before the
current defattach is processed, but is restored if the new event fails
to be admitted.

We focus henceforth on the second General Form.  There must be at least
one attachment, i.e., i must be at least 1.  All keywords are optional;
their role is described below.  The fi must be distinct constrained
function symbols, that is, function symbols all introduced in
signatures of encapsulate events (or macros such as defstub that
generate encapsulate events).  Each non-nil gi is a :logic-mode
function symbol that has had its guards verified, with the same
signature as fi (though formal parameters for fi and gi may have
different names).  (Note: The macro defattach!, defined in distributed
book books/misc/defattach-bang, avoids this restriction.)  This event
generates proof obligations and an ordering check, both described
below.  The effect of this event is first to remove any existing
attachments for all the function symbols fi, as described above for the
first General Form, and then to attach each gi to fi.

Proof obligations must be checked before making attachments.  For this
discussion we assume that each gi is non-nil (otherwise first remove
all attachment pairs <fi,gi> for which gi is nil).  Let s be the
functional substitution mapping each fi to gi.  For any term u, we
write u\s for the result of applying s to u; that is, u\s is the
"functional instance" obtained by replacing each fi by gi in u.  Let
G_fi and G_gi be the guards of fi and gi, respectively.  Let G_fi' be
the result of replacing each formal of fi by the corresponding formal
of gi in G_fi.  ACL2 first proves, for each i (in order), the formula
(implies G_fi' G_gi)\s.  If this sequence of proofs succeeds, then the
remaining formula to prove is the functional instance C\s of the
conjunction C of the constraints on the symbols fi; see
CONSTRAINT.  This last proof obligation is thus similar to the one
generated by functional instantiation (see CONSTRAINT).  As
with functional instantiation, ACL2 stores the fact that such proofs
have been done so that they are avoided in future events (see
LEMMA-INSTANCE).  Thus, you will likely avoid some proofs with the
sequence

     (defattach f g)
     (defattach f nil)
     (defattach f g)
     (defattach f nil)
     ...

rather than the sequence:

     (defattach f g)
     :u
     (defattach f g)
     :u
     ...

It remains to describe an ordering check.  We begin with the following
motivating example.

     (defstub f (x) t) ; constrained function with no constraints
     (defun g (x) (declare (xargs :guard t)) (not (f x)))
     (defattach f g) ; ILLEGAL!

Were the above defattach event to succeed, the evaluation theory
(discussed above) would be inconsistent: (f x) equals (g x) by the new
attachment equation, which in turn equals (not (f x)) by definition of
g.  The evaluation would therefore be meaningless.  Also, from a
practical perspective, there would be an infinite loop resulting from
any call of f.

We consider a function symbol g to be an "extended ancestor of" a
function symbol f if either of the following two criteria is met: (a) g
occurs in the formula that introduces f (i.e., definition body or
constraint) and g is introduced by an event different from (earlier
than) the event introducing f; or (b) g is attached to f.  For a
proposed defattach event, we check that the resulting extended ancestor
relation has no cycles, where for condition (b) we include all
attachment pairs that would result, including those remaining from
earlier defattach events.

Of course, a special case is that no function symbol may be attached to
itself.  Similarly, no function symbol may be attached to any of its
"siblings" -- function symbols introduced by the same event -- as
siblings are considered equivalent for purposes of the acyclicity check.

*Three primary uses of defattach.*
We anticipate three uses of defattach:

(1) Constrained function execution

(2) Sound modification of the ACL2 system

(3) Program refinement

We discuss these in turn.

(1) The example at the beginning of this documentation illustrates
constrained function execution.

(2) ACL2 is written essentially in itself.  Thus, there is an
opportunity to attaching to system functions.  For example, encapsulated
function too-many-ifs-post-rewrite, in the ACL2 source code, receives an
attachment of too-many-ifs-post-rewrite-builtin, which implements a
heuristic used in the rewriter.  To find all such examples, search the
source code for the string `-builtin'.

Over time, we expect to continue replacing ACL2 source code in a similar
manner.  We invite the ACL2 community to assist in this "open
architecture" enterprise; feel free to email the ACL2 implementors if
you are interested in such activity.

(3) Recall that for an attachment pair <f,g>, a proof obligation is
(speaking informally) that g satisfies the constraint on f.  Yet more
informally speaking, g is "more defined" than f; we can think of g as
"refining" f.  With these informal notions as motivation, we can view
defattach as providing refinement though the following formal
observation: the evaluation theory extends the theory of the ACL2
session, specifically by the addition of all attachment equations.  For
the logic-inclined, it may be useful to think model-theoretically: The
class of models of the evaluation theory is non-empty but is a subset
of the class of models of the current session theory.

*Miscellaneous remarks, with discussion of possible user errors.*

We conclude with remarks on some details.

A defattach event is never redundant (see REDUNDANT-EVENTS); in
that sense it is analogous to in-theory.

As mentioned above, the use of attachments is disabled for evaluation of
ground terms during proofs.  However, attachments can be used on code
during the proof process, essentially when the "program refinement" is
on theorem prover code rather than on functions we are reasoning about.
The attachment to too-many-ifs-post-rewrite described above provides
one example of such attachments.  Meta functions and clause-processor
functions can also have attachments, with the restriction that no
common ancestor with the evaluator can have an attachment; see
EVALUATOR-RESTRICTIONS.

For an attachment pair <f,g>, evaluation of f never consults the guard
of f.  Rather, control passes to g, whose guard is checked if
necessary.  The proof obligation related to guards, as described above,
guarantees that any legal call of f is also a legal call of g.  Thus
for guard-verified code that results in calls of f in raw Lisp, it is
sound to replace these calls with corresponding calls of g.

Defattach events are illegal inside any encapsulate event with a
non-empty signature unless they are local to the encapsulate.

To see all attachments: (all-attachments (w state)).  (Note that
attachments introduced with a non-nil value of :skip-checks will be
omitted from this list.)

We conclude with an example promised above, showing why it is necessary
in general to unattach all function symbols in an existing attachment
nest when unattaching any one of those function symbols.  Consider the
following example.

     (defstub f1 () t)
     (encapsulate ((f2 () t))
       (local (defun f2 () (f1)))
       (defthm f2=f1 (equal (f2) (f1))))
     (encapsulate ((f3 () t))
       (local (defun f3 () (f1)))
       (defthm f3=f1 (equal (f3) (f1))))
     (defun four () (declare (xargs :guard t)) 4)
     (defun five () (declare (xargs :guard t)) 5)
     (defattach (f1 four) (f2 four))
     (defattach (f1 five) (f3 five))

The second defattach replaces erases the existing attachment pair
<f1,four> before installing the new attachment pairs <f1,five> and
<f3,five>.  After the second defattach, both (f1) and (f3) evaluate to
5.  Now suppose that the attachment pair <f2,four> were not erased.
Then we would have (f1) evaluating to 5 and (f2) evaluating to 4,
contradicting the constraint f2=f1.  The evaluation theory would thus
be inconsistent, and at a more concrete level, the user might well be
surprised by evaluation results if the code were written with the
assumption specified in the constraint f2=f1.

DEFAXIOM    add an axiom

WARNING: We strongly recommend that you not add axioms.  If at all
possible you should use defun or mutual-recursion to define new
concepts recursively or use encapsulate to constrain them
constructively.  If your goal is to defer a proof by using a top-down
style, consider using skip-proofs; see the discussion on "Top-Down
Proof" in Section B.1.2 of "Computer-Aided Reasoning: An Approach."
Adding new axioms frequently renders the logic inconsistent.

     Example:
     (defaxiom sbar (equal t nil)
               :rule-classes nil
               :doc ":Doc-Section ...")

     General Form:
     (defaxiom name term
              :rule-classes rule-classes
              :doc          doc-string)

where name is a new symbolic name (see NAME), term is a term
intended to be a new axiom, and rule-classes and doc-string are as
described in the corresponding documentation topics .  The two keyword
arguments are optional.  If :rule-classes is not supplied, the list
(:rewrite) is used; if you wish the axiom to generate no rules, specify
:rule-classes nil.

DEFCHOOSE    define a Skolem (witnessing) function

     Examples:
     (defchoose choose-x-for-p1-and-p2 (x) (y z)
       (and (p1 x y z)
            (p2 x y z)))

     (defchoose choose-x-for-p1-and-p2 x (y z) ; equivalent to the above
       (and (p1 x y z)
            (p2 x y z)))

     ; The following is as above, but strengthens the axiom added to pick a sort
     ; of canonical witness, as described below.
     (defchoose choose-x-for-p1-and-p2 x (y z)
       (and (p1 x y z)
            (p2 x y z))
       :strengthen t)

     (defchoose choose-x-and-y-for-p1-and-p2 (x y) (z)
       (and (p1 x y z)
            (p2 x y z)))

     * Menu:

     * CONSERVATIVITY-OF-DEFCHOOSE:: proof of conservativity of defchoose

     General Form:
     (defchoose fn
                (bound-var1 ... bound-varn)
                (free-var1 ... free-vark)
                body
                :doc doc-string
                :strengthen b),

where fn is the symbol you wish to define and is a new symbolic name
(see NAME), (bound-var1 ... bound-varn) is a list of distinct
`bound' variables (see below), (free-var1 ... free-vark) is the list of
formal parameters of fn and is disjoint from the bound variables, and
body is a term.  The use of lambda-list keywords (such as &optional) is
not allowed.  The documentation string argument, :doc doc-string, is
optional; for a description of the form of doc-string see
DOC-STRING.  The :strengthen keyword argument is optional; if
supplied, it must be t or nil.

The system treats fn very much as though it were declared in the
signature of an encapsulate event, with a single axiom exported as
described below.  If you supply a :use hint (see HINTS), :use
fn, it will refer to that axiom.  No rule (of class :rewrite or
otherwise; see RULE-CLASSES) is created for fn.

Defchoose is only executed in defun-mode :logic; see
DEFUN-MODE.  Also see DEFUN-SK.

In the most common case, where there is only one bound variable, it is
permissible to omit the enclosing parentheses on that variable.  The
effect is the same whether or not those parentheses are omitted.  We
describe this case first, where there is only one bound variable, and
then address the other case.  Both cases are discussed assuming
:strengthen is nil, which is the default.  We deal with the case
:strengthen t at the end.

The effect of the form

     (defchoose fn bound-var (free-var1 ... free-vark)
       body)

is to introduce a new function symbol, fn, with formal parameters
(free-var1 ... free-vark).  Now consider the following axiom, which
states that fn picks a value of bound-var so that the body will be
true, if such a value exists:

     (1)   (implies body
                    (let ((bound-var (fn free-var1 ... free-vark)))
                      body))

This axiom is "clearly conservative" under the conditions expressed
above: the function fn simply picks out a "witnessing" value of
bound-var if there is one.  For a rigorous statement and proof of this
conservativity claim, see CONSERVATIVITY-OF-DEFCHOOSE.

Next consider the case that there is more than one bound variable, i.e.,
there is more than one bound-var in the following.

     (defchoose fn
                (bound-var1 ... bound-varn)
                (free-var1 ... free-vark)
                body)

Then fn returns a multiple value with n components, and formula (1)
above is expressed using mv-let as follows:

     (implies body
              (mv-let (bound-var1 ... bound-varn)
                      (fn free-var1 ... free-vark)
                      body))

We now discuss the case that :strengthen t is supplied.  For simplicity
we return to our simplest case, with defchoose applied to function fn,
a single free variable y, and a single bound variable bound-var.  The
idea is that if we pick the "smallest" witnessing bound-var for two
different free variables y and y1, then either those two witnesses are
the same, or else one is less than the other, in which case the smaller
one is a witness for its free variable but not for the other.  (See
comments in source function defchoose-constraint-extra for more
details.)  Below, body1 is the result of replacing y by y1 in body.

     (2)   (or (equal (fn y) (fn y1))
               (let ((bound-var (fn y)))
                 (and body
                      (not body1)))
               (let ((bound-var (fn y1)))
                 (and body1
                      (not body))))

An important application of this additional axiom is to be able to
define a "fixing" function that picks a canonical representative of
each equivalence class, for a given equivalence relation.  The
following events illustrate this point.

     (encapsulate
      ((equiv (x y) t))
      (local (defun equiv (x y) (equal x y)))
      (defequiv equiv))

     (defchoose efix (x) (y)
       (equiv x y)
       :strengthen t)

     (defthm equiv-implies-equal-efix-1
       (implies (equiv y y1)
                (equal (efix y) (efix y1)))
       :hints (("Goal" :use efix))
       :rule-classes (:congruence))

     (defthm efix-fixes
       (equiv (efix x) x)
       :hints (("Goal" :use ((:instance efix (y x))))))

If there is more than one bound variable, then (2) is modified in
complete analogy to (1) to use mv-let in place of let.

Comment for logicians:  As we point out in the documentation for
defun-sk, defchoose is "appropriate," by which we mean that it is
conservative, even in the presence of epsilon-0 induction.  For a
proof, See CONSERVATIVITY-OF-DEFCHOOSE.

CONSERVATIVITY-OF-DEFCHOOSE    proof of conservativity of defchoose

This documentation topic provides underlying theory.  It is of
theoretical interest only; it has no relationship to the effective use
of ACL2.

The argument below for the conservativity of defchoose replaces the
terse and somewhat misleading reference to a forcing argument in
Appendix B of the paper by ACL2 authors Kaufmann and Moore, "Structured
Theory Development for a Mechanized Logic" (Journal of Automated
Reasoning 26, no. 2 (2001), pp. 161-203).

Our basic idea is to to take a (countable) first-order structure for
ACL2, M, together with a function symbol, f, introduced by defchoose,
and find a way to expand M with an interpretation of f (without
changing the universe of M) so that e0-induction continues to hold in
the expansion.  A remark at the end of this documentation topic shows
why care is necessary.  A concept called "forcing", originally
introduced by Paul Cohen for set theory, has long since been adapted by
logicians (in a simplified form) to model theory.  This simplified
model-theoretic forcing provides the means for making our careful
expansion.

The forcing argument presented below is intended to be completely
self-contained for those familiar with basic first-order logic and
ACL2.  No background in forcing (model-theoretic or otherwise) is
expected, though we do expect a rudimentary background in first-order
logic and familiarity with the following.

Preliminaries.  We write s[p<-p0] to denote the result of extending or
modifying the assignment s by binding p to p0.  Now let A be a subset
of the universe U of a first-order structure M.  A is said to be
"first-order definable with parameters" in M if for some formula phi,
variable x, and assignment s binding the free variables of phi except
perhaps for x, A = {a \in U: M |= phi[s[x<-a]].  Note that we are
writing "\in" to denote set membership.  Finally, we indicate the end
of a proof (or of a theorem statement, when the proof is omitted) with
the symbol "-|".

We gratefully acknowledge very helpful feedback from John Cowles, who
found several errors in a draft of this note and suggested the
exercises.  We also thank Ruben Gamboa for helpful feedback, and we
thank Jim Schmerl for an observation that led us directly to this proof
in the first place.

We are given a consistent first-order theory T, extending the ACL2
ground-zero theory, that satisfies the e0-induction scheme.  We wish to
show that the extension of T by the following arbitrary defchoose event
is conservative, where g is a new function symbol.

          (defchoose g <bound-vars> <free-vars> <body>)

Note that by "the extension of T" here we mean the extension of T by not
only the new defchoose axiom displayed just below, but also the
addition of e0-induction axioms for formulas in the language with the
new defchoose function symbol, g.

          <body> -> (LET <free-vars> = g(<bound-vars>) in <body>)

By definition of conservativity, since proofs are finite, it clearly
suffices to consider an arbitrary finite subset of T.  Then by the
completeness, soundness, and downward Lowenheim-Skolem theorems of
first-order logic, it suffices to show that an arbitrary countable
model of T can be expanded (i.e., by interpreting the new symbol g
without changing the universe of the model) to a model of the
corresponding defchoose axiom above, in which all e0-induction axioms
hold in the language of that model.

Below, we will carry out a so-called _forcing_ construction, which
allows us to expand any countable model M of T to a model M[G] that
satisfies e0-induction and also satisfies the above axiom generated
from the above defchoose event.  The ideas in this argument are
standard in model theory; no novelty is claimed here.

Fix a countable model M of a theory T that satisfies e0-induction and
extends the ACL2 ground-zero theory.  Also fix the above defchoose
axiom, where g is not in the language of T.

We start by defining a partial order P as follows.  Let Nb and Nf be the
lengths of <bound-vars> and <free-vars>, respectively.  P consists of
all fn in M such that the following formula is true in M.  Roughly
speaking, it says that fn is a finite function witnessing the above
requirement for g.

            alistp(fn) &
            no-duplicatesp-equal(strip-cars(fn)) &
            (forall <bound-vars>, <free-vars> .
               (member-equal(cons(<bound-vars>,<free-vars>), fn) ->
                (length(<bound-vars>) = Nb &
                 length(<free-vars>)  = Nf &
                 ((exists <free-vars> . <body>) -> <body>))))

P is ordered by subset, i.e., we say that p2 _extends_ p1 if p1 is a
subset (not necessarily proper) of p2 (more precisely, M |=
subsetp-equal(p1,p2)).

Remark.  The original argument in Appendix B of the aforementioned
paper can essentially be salvaged, as we now show.  The key observation
is that the particular choice of P is nearly irrelevant for the
argument that follows below.  In particular, we can instead define P to
consist of finite one-one functions with domain contained in the set of
natural numbers.  More precisely, consider the following definitions.

          (defun function-p (fn)
            (declare (xargs :guard t))
            (and (alistp fn)
                 (no-duplicatesp-equal (strip-cars fn))))

          (defun nat-listp (x)
            (declare (xargs :guard t))
            (cond ((atom x)
                   (equal x nil))
                  (t (and (natp (car x))
                          (nat-listp (cdr x))))))

          (defun nat-function-p (x)
            (and (function-p x)
                 (nat-listp (strip-cars x))))

and define inverse as follows.

          (defun inverse (fn)
            (declare (xargs :guard (alistp fn)))
            (if (endp fn)
                nil
              (cons (cons (cdar fn) (caar fn))
                    (inverse (cdr fn)))))

Then P may instead be defined to consist of those fn for which
nat-function-p(fn) & function-p(inverse(fn)).  With this alternate
definition of P, the argument below then goes through virtually
unchanged, and we get an expansion M[G] of M in which there is a
definable enumeration of the universe.  The conservativity of defchoose
then follows easily because the function being introduced can be
defined explicitly using that enumeration (namely, always pick the
least witness in the sense of the enumeration).

End of Remark.

Next we present the relevant forcing concepts from model theory.

A _dense_ subset of P is a subset D of P such that for every p \in P,
there is d \in D such that d extends p.  A subset G of P is _generic_
with respect to a collection Ds of dense subsets of P, also written "G
is Ds-generic," if G is closed under subset (if p2 \in G and p2 extends
p1 then p1 \in G), G is pairwise compatible (the union-equal of any two
elements of G is in G), and every set in Ds has non-empty intersection
with G.

For p \in P, we say that a subset D of P is _dense beyond_ p if for all
p1 extending p there exists p2 extending p1 such that p2 \in D.  This
notion makes sense even for D not a subset of P if we treat elements of
D not in P as nil.

Proposition 1.  For any partial order P and countable collection Ds of
dense subsets of P, there is a Ds-generic subset of P.

Proof.  Let Ds = {D0,D1,D2,...}.  Define a sequence <p_0,p_1,...> such
that for all i, p_i \in Di and p_(i+1) extends p_i.  Let G = {p \in P:
for some i, pi extends p}.  Then G is Ds-generic. -|

Note that P is first-order definable (with parameters) in M.  Let Df be
the set of dense subsets of P that are first-order definable (with
parameters) in M.  A standard argument shows there are only countably
many first-order definitions with parameters in a countable model M --
for example, we can Goedel number all terms and then all formulas --
hence, Df is countable.

By Proposition 1, let G be Df-generic.  Notice that for any list x of
length Nb in M, the set of elements f of P for which x is in the domain
of f is dense and first-order definable.  We may thus define a function
g0 as follows: g0(x_1,...,x_Nb) = y if there is some element of G
containing the pair ((x_1 ... x_Nb) . y).  It is easy to see that g0 is
a total function on M.  Let L be the language of T and let L[g] be the
union of L with a set containing a single new function symbol, g.  Let
M[G] be the expansion of M to L[g] obtained by interpreting g to be g0
(see also Proposition 5 below).

So now we have fixed M, P, Df, G, and g0, where G is Df-generic.

Proposition 2.  Let Df be the set of dense subsets of P that are
first-order definable (with parameters) in M.  Suppose that p \in G and
D \in Df.  Then for some q \in G extending p, q \in D.

Proof.  Let D0 be the set of p' \in D that either extend p or have no
extension in D that extends p.  We leave it as a straightforward
exercise to show that D0 is dense, and D0 is clearly first-order
definable (with parameters) in M.  So by genericity of G, we may pick q
\in D0 such that q \in G.  Thus q \in D.  By definition of generic,
some extension q1 of both p and q belongs to G.  Pick q2 \in D
extending q1; thus q has an extension in D that extends p (namely, q2),
so by definition of D0, q extends p. -|

Definition of forcing.  Let phi(x1,...,xk) be a first-order formula in
L[g] and let p \in P.  We define a formula of L, denoted "p ||- phi" ("p
forces phi"), by recursion on phi (in the metatheory) as follows.
(Here, we view "or" and "forall" as abbreviations.)

       If phi is atomic, then let phi'(A) be the result of replacing,
     inside-out,   each subterm of the form g(x_1,...,x_Nb) with the
     term (cdr (assoc-equal   (list x_1 ... x_Nb) A)), where A is
     neither p nor a variable occurring in   phi.  Then p ||- phi is
     defined as follows: "The set {A \in P: A extends   p and phi'(A)}
     is dense beyond p".  That is, p ||- phi is the following   formula:

              (forall p1 \in P extending p)
               (exists p2 \in P extending p1) phi'(p2).

     p ||- ~phi is:  (forall p' \in P extending p) ~(p' ||- phi)

     p ||- phi_1 & phi_2 is: (p ||- phi_1) & (p ||- phi_2)

     p ||- (exists x) phi is:  (exists x) (p ||- phi)

We will need the following definition later.

Definition.  p ||-w phi (p _weakly forces_ phi) is an abbreviation for p
||- ~~phi.

The following exercises were suggested by John Cowles as a means for
gaining familiarity with the definition of forcing.

Exercise 1. Consider the formula (phi_1 OR phi_2) as an abbreviation for
~(~phi_1 & ~phi_2), Show that p ||- (phi_1 OR phi_2) is equivalent to
the following.

          (forall p' \in P extending p) (exists p'' \in P extending p')
           ((p'' ||- phi_1) OR (p'' ||- phi_2))

Exercise 2. Consider the formula (forall x)phi as an abbreviation for
~(exists x)~phi, Show that p ||- (forall x)phi is equivalent to the
following.

          (forall x)
           (forall p1 \in P extending p)
            (exists p2 \in P extending p1) (p2 ||- phi).

Exercise 3. Prove that p ||-w phi is equivalent to the following.

          (forall p' \in P extending p)
           (exists p'' \in P extending p') (p'' ||- phi).

Exercise 4. Let phi be a formula of L[g].  Prove:      M |= (p ||-
phi)[s[p<-p0]] implies      M |= (p ||-w phi)[s[p<-p0]].

Exercise 5. Let phi be a formula of L[g].  Prove:      M |= (p ||-
~phi)[s[p<-p0]] iff      M |= (p ||-w ~phi)[s[p<-p0]].

[End of exercises.]

The definition of forcing stipulates how to view "p ||- phi(x1,...,xk)"
as a new formula theta(p,x1,...,xk).  That is, "||-" transforms
formulas, so for any first-order formula phi, "p ||- phi" is just
another first-order formula.  That observation shows that a formula
such as ((p ||- phi) OR (p ||- ~phi)) is really just another
first-order formula.  The following proposition thus follows easily.

Proposition 3. For any formula phi of L[g], {p0: M |= ((p ||- phi) OR
(p ||- ~phi))[s[p<-p0]]]} is a dense subset of P, which (since it is
first-order definable with parameters in M) intersects G. -|

The following proposition is easily proved by a structural induction on
phi, and is left to the reader.

Proposition 4. Let phi be a formula of L[g].  Suppose p0 in P, p1 in P,
M |= (p ||- phi)[s[p<-p0]] and p1 extends p0.  Then
M |= (p ||- phi)[s[p<-p1]]. -|

We will also need the following.

Proposition 5. The following is dense for any finite set S of
Nb-tuples: {p \in P: for some <x_1 ... x_Nb> \in S, (list x_1 ... x_Nb)
\in strip-cars(p)}.  Thus, the function g0 is a total function. -|

The next lemma tells us that the sentences true in M[G] are those that
are forced by an element of G.

Truth Lemma.  Let phi be a formula in L[g], let s be an assignment to
the free variables of phi, and let p be a variable not in the domain of
s.  Then M[G] |= phi[s] iff for some p0 \in G, M |= (p ||-
phi)[s[p<-p0]].

Proof.  The proof is by induction on the structure of phi.  First
suppose phi is atomic.  Let D* be the set of elements p0 \in P such
that every assoc-equal evaluation from the definition of forcing phi
returns a pair when A is bound to p0.  (Intuitively, this means that p0
is a sufficiently large approximation from any G containing p0 to make
sense of phi in M[G].)  We make the following claim.

     (*)   For all p0 \in G such that p0 \in D*,
           M[G] |= phi[s] iff M |= (p ||- phi)[s[p<-p0]].

To prove the claim, fix p0 in both G and D*, and recall the function g0
constructed from G in the definition of M[G].  Suppose that t_1, ...,
t_Nb are terms and g(t_1, ..., t_Nb) is a subterm of phi.  Then s
assigns a value in M to each of the t_i.  Let a_i be the value assigned
by s to t_i.  Then g0(a_1, ..., a_Nb) = (cdr (assoc-equal (list a_1 ...
a_Nb) p0)), as the assoc-equal is a pair (since p0 \in D*) and has the
indicated value (because p0 \in G).  It follows by the definition of
formula phi' in the definition of forcing:

          M[G] |= phi[s]  iff  M |= phi'(p)[s[p<-p0]]

Moreover, because p0 \in D* it is clear that this holds if p0 is
replaced by an arbitrary extension of p0.  Then (*) easily follows.

By Proposition 5, D* is dense, so there is some p0 in the intersection
of D* and G.  The forward direction of the conclusion then follows by
(*).  The reverse direction is clear from (*) by application of
Proposition 2 to D* and Proposition 4.

Next, suppose M[G] |= ~phi[x].  Then it is not the case that M[G] |=
phi, so by the inductive hypothesis, there is no p0 \in G for which M
|= (p ||- phi)[s[p<-p0]].  By Proposition 3, there is p0 \in G for
which M |= (p ||- ~phi)[s[p<-p0]].  For the other direction, suppose it
is not the case that M[G] |= ~phi[s].  So M[G] |= phi[s], and by the
inductive hypothesis, there is p0 \in G for which M |= (p ||-
phi)[s[p<-p0]].  It follows that there is no p1 \in G for which M |= (p
||- ~phi)[s[p<-p1]], since from such p1 we can find a common extension
p2 of p0 and p1 (since G is generic), and since p2 extends p0 then by
Proposition 4, M |= (p ||- phi)[s[p<-p2]], contradicting (by definition
of forcing) M |= (p ||- ~phi)[s[p<-p1]] since p2 extends p1.

The case (phi_1 & phi_2) follows easily from the inductive hypothesis.
For the forward direction, apply Proposition 4 and the observation that
by genericity, if p0 \in G and p1 \in G then p0 and p1 they have a
common extension in G.

Finally, the case (exists x) phi follows trivially from the inductive
hypothesis. -|

Truth Lemma Corollary.  The Truth Lemma holds with ||-w replacing ||-.

Proof.  This is clear by applying the Truth Lemma to ~~phi. -|

Here is our main theorem.  Recall that all first-order theories in our
ACL2 context satisfy the e0-induction scheme.

Theorem.  M[G] satisfies e0-induction.

Proof.  We consider an arbitrary instance of e0-induction in L[g],
stated using a strict well-founded relation <| and a formula phi.  We
write phi(y) to indicate that y may be among the free variables of phi,
and phi(y<-x) to denote the result of substituting x for y in phi.

       theta(y):   (forall y) [((forall x <| y) phi(y<-x)) -> phi(y)]
                -> (forall y) phi(y)

Our goal is to prove that theta holds in M[G].

Below, we abuse notation by leaving assignments implicit and by writing
"p ||- phi(y0)" to signify that the formula (p ||- phi(y)) is true in M
under the extension of the explicit assignment that binds y to y0.  We
believe that the intended meaning will be clear.

Consider the following set D.

       D = {p \in P: either p ||-w phi(y0) for all y0,
                     or else
                     for some y0, p ||- ~phi(y0) and
                                  for all y1 <| y0 p ||-w phi(y1)}.

The set D is clearly first-order definable (with parameters) in M.  We
claim that D is a dense subset of P.  For suppose p0 \in P; we find p1
\in D extending p0, as follows.  If p0 ||-w phi(y0) for all y0, then we
may take p1 to be p0.  Otherwise, by definition of ||-w and ||-, there
is some y0 such that for some extension p0' of p0, p0' ||- ~phi(y0).
Pick a <|-minimal such y0, and correspondingly pick p1 so that p1
extends p0 and p1 ||- ~phi(y0).  In order to show that p1 \in D, it
remains to show that for all y1 <| y0, p1 ||-w phi(y1), i.e., there is
no q extending p1 such that q ||- ~phi(y1).  This is indeed the case
since otherwise q and y1 would contradict the <|-minimality of y0.

Applying the genericity of G and just-proved density of D, pick p0 \in G
such that p0 \in D.  If p0 ||-w phi(y0) for all y0, then by the Truth
Lemma Corollary, M[G] |= phi(y0) for all y0, and thus M[G] |= theta.
Otherwise, since p0 \in D we may choose y0 such that p0 ||- ~phi(y0)
and for all y1 <| y0, p0 ||-w phi(y1).  By the Truth Lemma and its
corollary, since p0 \in G we have:

     (1)   M[G] |= ~phi(y0).
     (2)   For all y1 <| y0, M[G] |= phi(y1).

It follows that the antecedent of theta is false in M[G], as witnessed
by y = y0; thus M[G] |= theta. -|

Remark.  We close by returning, as promised above, to the question of
why so much care is necessary in constructing an expansion of M.  We
assume familiarity here with the notion of a "non-standard" natural
number of M, i.e., one that is greater than the interpretation of any
term that has the form (+ 1 1 1 ... 1).  Here is a very simple example
that illustrates the need for some care.  Consider the following event,
which introduces a function foo with the following property: for all x,
if natp(x) then natp(foo(x)).

          (defchoose foo (y) (x)
            (implies (natp x) (natp y)))

Certainly we can build a model of the above property from a model M of
the ground-zero theory, by interpreting foo so that for all x for which
M satisfies natp(x), foo(x) is also a natp in M.  But suppose we start
with a non-standard model M of the ground-zero theory, and we happen to
define foo(x) to be 1 for all non-standard natural numbers x and 0 for
all other x.  The resulting expansion of M will not satisfy the
e0-induction scheme or even the ordinary natural number induction
scheme: foo(0)=0 holds in that expansion as does the implication
foo(n)=0 => foo(n+1)=0 for every natural number n of M, standard or
not; and yet foo(k)=0 fails for every non-standard natural number k of
M.

DEFCONG    prove congruence rule

     Defcong is used to prove that one equivalence relation preserves
     another in a given argument position of a given function.
     Example:
     (defcong set-equal iff (memb x y) 2)

     is an abbreviation for
     (defthm set-equal-implies-iff-memb-2
       (implies (set-equal y y-equiv)
                (iff (memb x y) (memb x y-equiv)))
       :rule-classes (:congruence))

See CONGRUENCE and also see EQUIVALENCE.

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

where equiv1 and equiv2 are known equivalence relations, term is a call
of a function fn on the correct number of distinct variable arguments
(fn x1 ... xn), k is a positive integer less than or equal to the arity
of fn, and other arguments are as specified in the documentation for
defthm.  The defcong macro expands into a call of defthm.  The name of
the defthm event is equiv1-implies-equiv2-fn-k unless an :event-name
keyword argument is supplied for the name.  The term of the theorem is

     (implies (equiv1 xk yk)
              (equiv2 (fn x1... xk ...xn)
                      (fn x1... yk ...xn))).

The rule-class :congruence is added to the rule-classes specified, if
it is not already there.  All other arguments to the generated defthm
form are as specified by the keyword arguments above.

DEFCONST    define a constant

     Examples:
     (defconst *digits* '(0 1 2 3 4 5 6 7 8 9))
     (defconst *n-digits* (the unsigned-byte (length *digits*)))

     General Form:
     (defconst name term doc-string)

where name is a symbol beginning and ending with the character *, term
is a variable-free term that is evaluated to determine the value of the
constant, and doc-string is an optional documentation string (see
DOC-STRING).

When a constant symbol is used as a term, ACL2 replaces it by its
value; see TERM.

Note that defconst uses a "safe mode" to evaluate its form, in order to
avoids soundness issues but with an efficiency penalty (perhaps
increasing the evaluation time by several hundred percent).  If
efficiency is a concern, or if for some reason you need the form to be
evaluated without safe mode (e.g., you are an advanced system hacker
using trust tags to traffic in raw Lisp code), consider using the macro
defconst-fast instead, defined in books/make-event/defconst-fast.lisp,
for example:

     (defconst-fast *x* (expensive-fn ...))

A more general utility may be found in books/tools/defconsts.lisp.  Also
using-tables-efficiently for an analogous issue with table events.

It may be of interest to note that defconst is implemented at the lisp
level using defparameter, as opposed to defconstant.  (Implementation
note:  this is important for proper support of undoing and
redefinition.)

We close with a technical remark, perhaps of interest only to users of
ACL2(h), the experimental extension of ACL2 that supports hash cons,
function memoization, and hash-table-based "fast alists"; see
HONS-AND-MEMOIZATION.  For an event of the form (defconst *C* (quote
OBJ)), i.e., (defconst *C* 'OBJ), then the value associated with *C* is
OBJ; that is, the value of *C* is eq to the actual object OBJ occurring
in the defconst form.  So for example, if make-event is used to
generate such a defconst event, as it is in the two books mentioned
above, and OBJ is a fast alist (using ACL2(h)), then the value of *C*
is a fast alist.  This guarantee disappears if the term in the defconst
form is not a quoted object, i.e., if it is not of the form (quote OBJ).

DEFDOC    add a documentation topic

     Examples:
     (defdoc interp-section
        ":Doc-Section ...")

     General Form:
     (defdoc name doc-string)

where name is a symbol or string to be documented and doc-string is a
documentation string (see DOC-STRING).  This event adds the
documentation string for symbol name to the :doc data base.  It may
also be used to change the documentation for name if name already has
documentation.  The difference between this event and deflabel is that,
unlike deflabel (but like table), it does not mark the current history
with the name.  But like deflabel, defdoc events are never considered
redundant (see REDUNDANT-EVENTS).

See DEFLABEL for a means of attaching a documentation string to
a name that marks the current history with that name.  We now elaborate
further on how defdoc may be useful in place of deflabel.

It is usually sufficient to use deflabel when you might be tempted to
use defdoc.  However, unlike deflabel, defdoc does not mark the current
history with name.  Thus, defdoc is useful for introducing the
documentation for a defun or deftheory event, for example, several
events before the function or theory is actually defined.

For example, suppose you want to define a theory (using deftheory).
You need to prove the lemmas in that theory before executing the
deftheory event.  However, it is quite natural to define a :Doc-Section
(see DOC-STRING) whose name is the name of the theory to be
defined, and put the documentation for that theory's lemmas into that
:Doc-Section.  Defdoc is ideal for this purpose, since it can be used
to introduce the :Doc-Section, followed by the lemmas referring to that
:Doc-Section, and finally concluded with a deftheory event of the same
name.  If deflabel were used instead of defdoc, for example, then the
deftheory event would be disallowed because the name is already in use
by the deflabel event.

We also imagine that some users will want to use defdoc to insert the
documentation for a function under development.  This defdoc event
would be followed by definitions of all the subroutines of that
function, followed in turn by the function definition itself.

Any time defdoc is used to attach documentation to an
already-documented name, the name must not be attached to a new
:Doc-Section.  We make this requirement as a way of avoiding loops in
the documentation tree.  When documentation is redefined, a warning
will be printed to the terminal.

DEFEQUIV    prove that a function is an equivalence relation

     Example:
     (defequiv set-equal)

     is an abbreviation for
     (defthm set-equal-is-an-equivalence
       (and (booleanp (set-equal x y))
            (set-equal x x)
            (implies (set-equal x y) (set-equal y x))
            (implies (and (set-equal x y)
                          (set-equal y z))
                     (set-equal x z)))
       :rule-classes (:equivalence))

See EQUIVALENCE.

     General Form:
     (defequiv fn
       :rule-classes rule-classes
       :instructions instructions
       :hints hints
       :otf-flg otf-flg
       :event-name event-name
       :doc doc)

where fn is a function symbol of arity 2, event-name, if supplied, is a
symbol, and all other arguments are as specified in the documentation
for defthm.  The defequiv macro expands into a call of defthm.  The
name of the defthm is fn-is-an-equivalence, unless event-name is
supplied, in which case event-name is the name used.  The term
generated for the defthm event states that fn is Boolean, reflexive,
symmetric, and transitive.  The rule-class :equivalence is added to the
rule-classes specified, if it is not already there.  All other
arguments to the generated defthm form are as specified by the other
keyword arguments above.

DEFEVALUATOR    introduce an evaluator function

     Example:
     (defevaluator evl evl-list
       ((length x) (member-equal x y)))

See META.

     General Form:
     (defevaluator ev ev-list
        ((g1 x1 ... xn_1)
         ...
         (gk x1 ... xn_k))

where ev and ev-list are new function symbols and g1, ..., gk are old
function symbols with the indicated number of formals, i.e., each gi
has n_i formals.

This function provides a convenient way to constrain ev and ev-list to
be mutually-recursive evaluator functions for the symbols g1, ..., gk.
Roughly speaking, an evaluator function for a fixed, finite set of
function symbols is a restriction of the universal evaluator to terms
composed of variables, constants, lambda expressions, and applications
of the given functions.  However, evaluator functions are constrained
rather than defined, so that the proof that a given metafunction is
correct vis-a-vis a particular evaluator function can be lifted (by
functional instantiation) to a proof that it is correct for any larger
evaluator function.  See META for a discussion of metafunctions.

Defevaluator executes an encapsulate after generating the appropriate
defun and defthm events.  Perhaps the easiest way to understand what
defevaluator does is to execute the keyword command

     :trans1 (defevaluator evl evl-list ((length x) (member-equal x y)))

and inspect the output.  This trick is also useful in the rare case
that the event fails because a hint is needed.  In that case, the
output of :trans1 can be edited by adding hints, then submitted
directly.

Formally, ev is said to be an "evaluator function for g1, ..., gk, with
mutually-recursive counterpart ev-list" iff ev and ev-list are
constrained functions satisfying just the constraints discussed below.

Ev and ev-list must satisfy constraints (0)-(4) and (k):

     (0) How to ev an arbitrary function application:
         (implies (and (consp x)
                       (syntaxp (not (equal a ''nil)))
                       (not (equal (car x) 'quote)))
                  (equal (ev x a)
                         (ev (cons (car x)
                                   (kwote-lst (ev-list (cdr x) a)))
                             nil)))

     (1) How to ev a variable symbol:
         (implies (symbolp x)
                  (equal (ev x a) (and x (cdr (assoc-equal x a)))))

     (2) How to ev a constant:
         (implies (and (consp x)
                       (equal (car x) 'quote))
                  (equal (ev x a) (cadr x)))

     (3) How to ev a lambda application:
         (implies (and (consp x)
                       (consp (car x)))
                  (equal (ev x a)
                         (ev (caddar x)
                             (pairlis$ (cadar x)
                                       (ev-list (cdr x) a)))))

     (4) How to ev an argument list:
         (implies (consp x-lst)
                  (equal (ev-list x-lst a)
                         (cons (ev (car x-lst) a)
                               (ev-list (cdr x-lst) a))))
         (implies (not (consp x-lst))
                  (equal (ev-list x-lst a)
                         nil))

     (k) For each i from 1 to k, how to ev an application of gi,
         where gi is a function symbol of n arguments:
         (implies (and (consp x)
                       (equal (car x) 'gi))
                  (equal (ev x a)
                         (gi (ev x1 a)
                             ...
                             (ev xn a)))),
         where xi is the (cad...dr x) expression equivalent to (nth i x).

Defevaluator defines suitable witnesses for ev and ev-list, proves the
theorems about them, and constrains ev and ev-list appropriately.  We
expect defevaluator to work without assistance from you, though the
proofs do take some time and generate a lot of output.  The proofs are
done in the context of a fixed theory, namely the value of the constant
*defevaluator-form-base-theory*.

(Aside: (3) above may seem surprising, since the bindings of a are not
included in the environment that is used to evaluate the lambda body,
(caddar x).  However, ACL2 lambda expressions are all _closed_: in
(lambda (v1 ... vn) body), the only free variables in body are among
the vi.  See TERM.)

DEFEXEC    attach a terminating executable function to a definition

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

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

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

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

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

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

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

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

     Example:

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

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

The above example macroexpands to the following.

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

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

CAVEAT: Termination is not considered for calls of mbe under the
top-level call.  Moreover, the :exec part of an mbe call under the
:logic part of any superior mbe call is completely ignored.

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

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

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

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

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

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

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

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

DEFINE-TRUSTED-CLAUSE-PROCESSOR    define a trusted (unverified) goal-level simplifier

This documentation assumes familiarity with :clause-processor rules;
see CLAUSE-PROCESSOR.  Briefly put, a _clause-processor_ is a
user-defined function that takes as input the ACL2 representation of a
goal -- a _clause_ -- and returns a list of goals (i.e., a list of
clauses).  A :clause-processor rule is a way to inform ACL2 that a
clause-processor has been proved correct and now may be specified in
:clause-processor hints.

Here we describe a utility, define-trusted-clause-processor, that
provides another way to inform ACL2 that a function is to be considered
a clause-processor that can be specified in a :clause-processor hint.
You can find examples of correct and incorrect use of this utility in
distributed book books/clause-processors/basic-examples.

Consider the simple example already presented for :clause-processor
rules (again, see CLAUSE-PROCESSOR), for a simple
clause-processor named note-fact-clause-processor.  Instead of
introducing an evaluator and proving a correctness theorem with
:rule-classes :clause-processor, we can simply inform ACL2 that we
trust the function note-fact-clause-processor to serve as a
clause-processor.

     (define-trusted-clause-processor
       note-fact-clause-processor
       nil
       :ttag my-ttag)

A non-nil :ttag argument generates a defttag event in order to
acknowledge the dependence of the ACL2 session on the (unproved)
correctness of this clause-processor.  That argument can be omitted if
there is currently an active trust tag.  See DEFTTAG.  Because
we are trusting this clause-processor, rather than having proved it
correct, we refer to it as a "trusted" clause-processor to contrast
with a proved-correct, or "verified", clause-processor.

Now that the event displayed above has established
note-fact-clause-processor as a (trusted) clause-processor, we can use
it in a :clause-processor hint, for example as follows.  Notice that
the output is identical to that for the corresponding example presented
for the verified case (see CLAUSE-PROCESSOR), except that the
word "verified" has been replaced by the word "trusted".

     ACL2 !>(thm (equal (car (cons x y))
                        x)
                 :hints
                 (("Goal"
                   :clause-processor
                   (note-fact-clause-processor clause '(equal a a)))))

     [Note:  A hint was supplied for our processing of the goal above.
     Thanks!]

     We now apply the trusted :CLAUSE-PROCESSOR function NOTE-FACT-CLAUSE-
     PROCESSOR to produce two new subgoals.

     Subgoal 2
     (IMPLIES (EQUAL A A)
              (EQUAL (CAR (CONS X Y)) X)).

     But we reduce the conjecture to T, by the :executable-counterpart of
     IF and the simple :rewrite rule CAR-CONS.

     Subgoal 1
     (EQUAL A A).

     But we reduce the conjecture to T, by primitive type reasoning.

     Q.E.D.

     Summary
     Form:  ( THM ...)
     Rules: ((:EXECUTABLE-COUNTERPART IF)
             (:EXECUTABLE-COUNTERPART NOT)
             (:FAKE-RUNE-FOR-TYPE-SET NIL)
             (:REWRITE CAR-CONS))
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

     Proof succeeded.
     ACL2 !>

Indeed, if one runs this example first and subsequently verifies the
clause-processor, one will see the word "trusted" change to "verified".

The general form is as follows.

     (define-trusted-clause-processor
       cl-proc           ;;; clause-processor function
       supporters        ;;; see below
       &key
       label             ;;; optional, but required if doc is non-nil
       doc               ;;; optional
       ttag              ;;; discussed above
       partial-theory    ;;; optional encapsulate event
       )

If a :label LAB is supplied, then a subsidiary deflabel event will be
generated with name LAB, which will enable you to to undo this
define-trusted-clause-processor event using: :ubt LAB.  If you supply a
:label then you may supply a :doc argument to use with that generated
deflabel event.  We discussed the :ttag argument above.  The entire
form is considered redundant (skipped) if it is identical to one
already executed in the current ACL2 world; but if it is not redundant,
then cl-proc must not already have been similarly designated as a
trusted clause-processor.

Note that cl-proc may be defined either in :program-mode or :logic-mode.

The supporters argument should be a true list of function symbols in the
current ACL2 world.  It is important that this list include user-defined
functions whose definitions support the correctness of the
clause-processor function.  Otherwise, local definitions of those
missing supporters can render the use of this clause-processor unsound,
as discussed in the paper referenced at the end of the clause-processor
documentation topic.  Moreover, ACL2 assumes for dependent
clause-processors (discussed below) that every function symbol
constrained by the "promised encapsulate" of that event is either among
those supporters or ancestral in one of them (i.e. a supporter of a
supporter, a supporter of one of those, etc.).

*Dependent clause-processors and promised encapsulates*: The
:partial-theory argument

Suppose you want to introduce a clause-processor to reason about a
complex hardware simulator that is implemented outside ACL2.  Sawada
and Reeber had just such a problem, as reported in their FMCAD 2006
paper.  Indeed, they used sys-call to implement a :program-mode
function in ACL2 that can invoke that simulator.  In principle one
could code the simulator directly in ACL2; but it would be a tremendous
amount of work that has no practical purpose, given the interface to
the external simulator.  So: In what sense can we have a
clause-processor that proves properties about a simulator when that
simulator is not fully axiomatized in ACL2?  Our answer, in a nutshell,
is this: The above :partial-theory argument provides a way to write
merely some of the constraints on the external tool (or even no
constraints at all), with the understanding that such constraints are
present implicitly in a stronger "promised" encapsulate, for example by
exporting the full definition.

If a trusted clause-processor is introduced with a :partial-theory
argument, we call it a "dependent" clause-processor, because its
correctness is dependent on the constraints implicitly introduced by the
:partial-theory encapsulate form.  The implicit constraints should
logically imply the constraints actually introduced by the explicit
encapsulate, but they should also be sufficient to justify every
possible invocation of the clause-processor in a :clause-processor
hint.  The user of a define-trusted-clause-processor form is making a
guarantee -- or, is relying on a guarantee provided by the writer of
that form -- that in principle, there exists a so-called "promised
encapsulate": an encapsulate form with the same signature as the
:partial-theory encapsulate form associated with the trusted
clause-processor, but whose constraints introduced are the
aforementioned implicit constraints.

There are several additional requirements on a :partial-theory argument.
First, it must be an encapsulate event with non-empty signature.
Moreover, the functions introduced by that event must be exactly those
specified in the signature, and no more.  And further still, the
define-trusted-clause-processor form cannot be executed inside any
encapsulate form with non-empty signature; we can think of this
situation as attempting to associate more than one encapsulate with the
functions introduced in the inner encapsulate.

The :partial-theory event will (in essence) be executed as part of the
evaluation of the define-trusted-clause-processor form.  Again, a
critical obligation rests on the user who provides a :partial-theory:
there must exist (in principle at least) a corresponding promised
encapsulate form with the same signature that could logically be
admitted, whenever the above define-trusted-clause-processor form is
evaluated successfully, that justifies the designation of cl-proc as a
clause-processor.  See also the paper mentioned above for more about
promised encapsulates.  A key consequence is that the constraints are
unknown for the functions introduced in (the signature of) a
:partial-theory encapsulate form.  Thus, functional instantiation (see
FUNCTIONAL-INSTANTIATION-EXAMPLE) is disabled for function in
the signature of a :partial-theory form.

*A remark on the underlying implementation*

You can see all of the current trusted clause-processors by issuing the
command (table trusted-clause-processor-table).  Those that are
dependent clause-processors will be associated in the resulting
association list with a pair whose car is the list of supporters and
whose cdr is t, i.e., with (supporters . t); the others will be
associated just with (supporters).

Thus, define-trusted-clause-processor is actually a macro that generates
(among other things) a table event for a table named
trusted-clause-processor-table; see TABLE.  You are invited to
use :trans1 to see expansions of calls of this macro.

*A technique for using raw Lisp to define a trusted clause-processor*

The following code is intended to give an idea for how one might define
the "guts" of a trusted clause-processor in raw Lisp.  The idea is to
stub out functions, such as acl2-my-prove below, that you want to
define in raw Lisp; and then, load a raw Lisp file to overwrite any
such function with the real code.  But then we make any such
overwritten function untouchable.  (This last step is important because
otherwise, one can prove nil using a :functional-instance :use hint, by
exploiting the fact that this function has executable code for which
there is no corresponding definitional axiom.)

     (defstub acl2-my-prove (term hint) t)

     (program)

     (defttag :my-cl-proc)

     (progn

     ; We wrap everything here in a single progn, so that the entire form is
     ; atomic.  That's important because we want the use of push-untouchable to
     ; prevent anything besides my-clause-processor from calling acl2-my-prove.

       (progn!

        (set-raw-mode-on state)

        (load "my-hint-raw.lsp") ; defines my-prove in raw Lisp

        (defun acl2-my-prove (term hint)
          (my-prove term hint)))

       (defun my-clause-processor (cl hint)
         (declare (xargs :guard (pseudo-term-listp cl)
                         :mode :program))
         (if (acl2-my-prove (disjoin cl) hint)
             (disjoin-clause-segments-to-clause
              (pairlis$ (hint-to-termlist hint) nil)
              cl)
           (prog2$ (cw "~|~%NOTE: Unable to prove goal with ~
                       my-clause-processor and indicated hint.~|")
                   (list cl))))

       (push-untouchable acl2-my-prove t)
       )

DEFLABEL    build a landmark and/or add a documentation topic

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

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

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

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

DEFMACRO    define a macro

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

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

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

     Example Expansions:
     term                    macroexpansion

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

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

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

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

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

where name is a new symbolic name (see NAME), macro-args
specifies the formal parameters of the macro, and body is a term.  The
formal parameters can be specified in a much more general way than is
allowed by ACL2 defun events; see MACRO-ARGS for a description
of keyword (&key) and optional (&optional) parameters as well as other
so-called "lambda-list keywords", &rest and &whole.  Doc-string is an
optional documentation string; see DOC-STRING.  Each dcl is an
optional declaration (see DECLARE) except that the only xargs
keyword permitted by defmacro is :guard.

For compute-intensive applications see the distributed book
misc/defmac.lisp, which can speed up macroexpansion by introducing an
auxiliary defun.  For more information, evaluate the form (include-book
"misc/defmac" :dir :system) and then evaluate :doc defmac.

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

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

DEFMACRO-LAST    define a macro that returns its last argument, but with side effects

This is an advanced feature that requires a trust tag.  For explanation,
including an example, see RETURN-LAST.

DEFN    definition with guard t

Defn is defun with guard t.

DEFND    disabled definition with guard t

Defnd is defund with guard t.

DEFPKG    define a new symbol package

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

     * Menu:

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

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

     * MANAGING-ACL2-PACKAGES:: user-contributed documentation on packages

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

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

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

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

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

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

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

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

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

Upon admission of a defpkg event, the function pkg-imports is extended
to compute a list of all symbols imported into the given package,
without duplicates.

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

The Common Lisp function intern is weakly supported by ACL2; see
INTERN.  A more general form of that function is also provided: see
INTERN$.

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

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

NOTE: Also see MANAGING-ACL2-PACKAGES for contributed
documentation on managing ACL2 packages.

HIDDEN-DEATH-PACKAGE    handling defpkg events that are local

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

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

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

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

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

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

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

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

HIDDEN-DEFPKG    handling defpkg events that are local

See HIDDEN-DEATH-PACKAGE

MANAGING-ACL2-PACKAGES    user-contributed documentation on packages

Jared Davis has contributed documentation on managing ACL2 packages.
See
`http://www.cs.utexas.edu/users/moore/acl2/contrib/managing-acl2-packages.html'.

DEFPROXY    define a non-executable :program-mode function for attachment

This event is provided for those who want to experiment with defattach
using :program mode functions, and without proof obligations or
constraints on cycles in the extended ancestors graph; see
DEFATTACH.  If you merely want to define a stub or a non-executable
function, see DEFSTUB or see DEFUN-NX, respectively.

See distributed book books/misc/defproxy-test.lisp for an extended (but
simple) example.

     Example Forms:
     (defproxy subr1 (* *) => *)
     (defproxy add-hash (* * hashtable) => (mv * hashtable))

     General Form:
     (defproxy name args-sig => output-sig)

where name is a new function symbol and (name . args-sig) =>
output-sig) is a signature; see SIGNATURE.

The macro defproxy provides a convenient way to introduce a "proxy": a
:program mode function that can be given attachments for execution (see
DEFATTACH), assuming that there is an active trust tag (see
DEFTTAG).  Thus, a defproxy calls expands to a defun form with
the following xargs declare form: :non-executable :program.  Note that
verify-termination is not permitted for such a function.  However, it
is permitted to put the proxy function into :logic mode by use of an
encapsulate event; indeed, this is the way to "upgrade" an attachment
so that the normal checks are performed and no trust tag is necessary.

In order to take advantage of a defproxy form, one provides a
subsequent defattach form to attach an executable function to the
defproxy-introduced function.  When :skip-checks t is provided in a
defattach form, the usual checks for defattach events are skipped,
including proof obligations and the check that the extended ancestor
relation has no cycles (see DEFATTACH).  There must be an
active trust tag (see DEFTTAG) in order to use :skip-checks t.
In that case the use of :skip-checks t is permitted; but note that its
use is in fact required if a :program mode function is involved, and
even if a :logic mode function is involved that has not been
guard-verified.

The following log shows a simple use of defproxy.

     ACL2 !>(defproxy foo-stub (*) => *)

     Summary
     Form:  ( DEFUN FOO-STUB ...)
     Rules: NIL
     Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
      FOO-STUB
     ACL2 !>(foo-stub '(3 4 5))

     ACL2 Error in TOP-LEVEL:  ACL2 cannot ev the call of undefined function
     FOO-STUB on argument list:

     ((3 4 5))

     To debug see :DOC print-gv, see :DOC trace, and see :DOC wet.

     ACL2 !>(defun foo-impl (x)
              (declare (xargs :mode :program
                              :guard (or (consp x) (eq x nil))))
              (car x))

     Summary
     Form:  ( DEFUN FOO-IMPL ...)
     Rules: NIL
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FOO-IMPL
     ACL2 !>(defttag t)

     TTAG NOTE: Adding ttag :T from the top level loop.
      T
     ACL2 !>(defattach (foo-stub foo-impl) :skip-checks t)

     Summary
     Form:  ( DEFATTACH (FOO-STUB FOO-IMPL) ...)
     Rules: NIL
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      :ATTACHMENTS-RECORDED
     ACL2 !>(foo-stub '(3 4 5))
     3
     ACL2 !>

One can replace this attachment with one that uses :logic mode
functions and does not skip checks.  The idea is to reintroduce the
proxy function using an encapsulate form, which does not require
redefinition (see LD-REDEFINITION-ACTION) to be enabled, and
either to put the attachment into :logic mode with the guard verified,
as we do in the example below, or else to attach to a different
guard-verified :logic mode function.

     ACL2 !>(defattach (foo-stub nil) :skip-checks t) ; remove attachment

     Summary
     Form:  ( DEFATTACH (FOO-STUB NIL) ...)
     Rules: NIL
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      :ATTACHMENTS-RECORDED
     ACL2 !>(encapsulate
             ((foo-stub (x) t :guard (true-listp x)))
             (local (defun foo-stub (x) (cdr x)))
             (defthm foo-stub-reduces-acl2-count
               (implies (consp x)
                        (< (acl2-count (foo-stub x))
                           (acl2-count x)))))

     [[ ... output omitted here ... ]]

     The following constraint is associated with the function FOO-STUB:

     (IMPLIES (CONSP X) (< (ACL2-COUNT (FOO-STUB X)) (ACL2-COUNT X)))

     Summary
     Form:  ( ENCAPSULATE ((FOO-STUB ...) ...) ...)
     Rules: NIL
     Warnings:  Non-rec
     Time:  0.02 seconds (prove: 0.01, print: 0.00, other: 0.01)
      T
     ACL2 !>(verify-termination foo-impl)

     Since FOO-IMPL is non-recursive, its admission is trivial.  We could
     deduce no constraints on the type of FOO-IMPL.

     Computing the guard conjecture for FOO-IMPL....

     The guard conjecture for FOO-IMPL is trivial to prove.  FOO-IMPL is
     compliant with Common Lisp.

     Summary
     Form:  ( DEFUN FOO-IMPL ...)
     Rules: NIL
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

     Summary
     Form:  ( MAKE-EVENT (VERIFY-TERMINATION-FN ...))
     Rules: NIL
     Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
      FOO-IMPL
     ACL2 !>(defttag nil) ; optional
      NIL
     ACL2 !>(defattach (foo-stub foo-impl))

     The guard proof obligation is

     (IMPLIES (TRUE-LISTP X)
              (OR (CONSP X) (EQ X NIL))).

     But we reduce the conjecture to T, by primitive type reasoning.

     Q.E.D.

     This concludes the guard proof.

     We now prove that the attachment satisfies the required constraint.
     The goal to prove is

     (IMPLIES (CONSP X)
              (< (ACL2-COUNT (FOO-IMPL X))
                 (ACL2-COUNT X))).

     [[ ... output omitted here ... ]]

     Q.E.D.

     Summary
     Form:  ( DEFATTACH (FOO-STUB FOO-IMPL))
     Rules: ((:DEFINITION ACL2-COUNT)
             (:DEFINITION FOO-IMPL)
             (:ELIM CAR-CDR-ELIM)
             (:FAKE-RUNE-FOR-LINEAR NIL)
             (:FAKE-RUNE-FOR-TYPE-SET NIL)
             (:REWRITE CAR-CONS)
             (:REWRITE CDR-CONS)
             (:TYPE-PRESCRIPTION ACL2-COUNT))
     Time:  0.02 seconds (prove: 0.01, print: 0.01, other: 0.00)
      :ATTACHMENTS-RECORDED
     ACL2 !>

We close with some remarks on the checking of guards in the case that
defattach has been called with keyword argument :skip-checks t.  We
illustrate with examples, where we assume an attachment pair (f . g)
created by an event (defattach ... (f g) ... :skip-checks t ...).  A
good model for the treatment of :skip-checks t is dependent on whether f
was introduced with defproxy or with encapsulate: for defproxy, the
normal guard-related checks are treated as skipped, while for
encapsulate, they are assumed to hold.

First suppose that f was introduced using defproxy, and consider the
following example.

     (defproxy f (*) => *)
     (defun g (x) (car x)) ; not guard-verified; implicit guard of t is too weak
     (defttag t) ; trust tag needed for :skip-checks t
     (defattach (f g) :skip-checks t)

If we try to evaluate the form (f 3) in ACL2, then the top-level
so-called "executable counterpart" (i.e., the logically-defined
funcction, also known as the "*1*" function) of f is invoked.  It calls
the executable counterpart of g, which calls the executable counterpart
of car, which in turn checks the guard of car and causes a guard
violation error (unless we first turn off guard-checking; see
SET-GUARD-CHECKING).

     ACL2 !>(trace$ f g)
      ((F) (G))
     ACL2 !>(f 3)
     1> (ACL2_*1*_ACL2::F 3)
       2> (ACL2_*1*_ACL2::G 3)

     ACL2 Error in TOP-LEVEL:  The guard for the function call (CAR X),
     which is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments
     in the call (CAR 3).  To debug see :DOC print-gv, see :DOC trace, and
     see :DOC wet.  See :DOC set-guard-checking for information about suppressing
     this check with (set-guard-checking :none), as recommended for new
     users.

     ACL2 !>

Little changes if we modify the example above by strengtheing the guard
of g.

     (defproxy f (*) => *)
     (defun g (x)
       (declare (xargs :guard (consp x)))
       (car x))
     (defttag t) ; trust tag needed for :skip-checks t
     (defattach (f g) :skip-checks t)

The result of evaluating (f 3) is as before, except that this time the
guard violation occurs at the time that g is called.

     ACL2 !>(trace$ f g)
      ((F) (G))
     ACL2 !>(f 3)
     1> (ACL2_*1*_ACL2::F 3)
       2> (ACL2_*1*_ACL2::G 3)

     ACL2 Error in TOP-LEVEL:  The guard for the function call (G X), which
     is (CONSP X), is violated by the arguments in the call (G 3).  To debug
     see :DOC print-gv, see :DOC trace, and see :DOC wet.  See :DOC set-
     guard-checking for information about suppressing this check with (set-
     guard-checking :none), as recommended for new users.

     ACL2 !>

Now consider a slight variation of the example just above, in which f is
introduced using encapsulate instead of using defproxy.

     (encapsulate ( ((f *) => *) )
                  (local (defun f (x) x)))
     (defun g (x)
       (declare (xargs :guard (consp x)))
       (car x))
     (defttag t) ; trust tag needed for :skip-checks t
     (defattach (f g) :skip-checks t)

Since f was introduced by encapsulate instead of by defproxy, ACL2
assumes that the usual guard properties hold.  In particular, it assumes
that (informally speaking) the guard of f implies the guard of g; see
DEFATTACH for details.  So in this case, ACL2 proceeds under
that assumption even though it's actually false, and the result is a
raw Lisp error.

     ACL2 !>(trace$ f g)
      ((F) (G))
     ACL2 !>(f 3)
     1> (ACL2_*1*_ACL2::F 3)
       2> (G 3)

     ***********************************************
     ************ ABORTING from raw Lisp ***********
     Error:  Attempt to take the car of 3 which is not listp.
     ***********************************************

     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 !>

If you replace g by its definition in the first example of this series,
i.e. with a guard (implicitly) of t, you will see the same error, this
time because the defattach event assumed that g was guard-verified.

DEFPUN    define a tail-recursive function symbol

Defpun is a macro developed by Pete Manolios and J Moore that allows
tail-recursive definitions.  It is defined in distributed book
books/misc/defpun.lisp, so to use it, execute the following event.

     (include-book "misc/defpun" :dir :system)

Details of defpun are provided by Manolios and Moore in the "Partial
Functions in ACL2" published with the ACL2 2000 workshop; see
`http://www.cs.utexas.edu/users/moore/acl2/workshop-2000/'.  Also see
`http://www.cs.utexas.edu/users/moore/publications/defpun/index.html'.

A variant, defp, has been developed by Matt Kaufmann to allow more
general forms of tail recursion.  If defpun doesn't work for you, try
defp by first executing the following event.

     (include-book "misc/defp" :dir :system)

Sandip Ray has contributed a variant of defpun, defpun-exec, that
supports executability.  See distributed book
books/defexec/defpun-exec/defpun-exec.lisp:

     (include-book "defexec/defpun-exec/defpun-exec" :dir :system)

He has also contributed book
books/misc/misc2/defpun-exec-domain-example.lisp, for functions that are
uniquely defined in a particular domain.

DEFREFINEMENT    prove that equiv1 refines equiv2

     Example:
     (defrefinement equiv1 equiv2)

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

See REFINEMENT.

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

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

DEFSTOBJ    define a new single-threaded object

Note: Novices are advised to avoid defstobj, perhaps instead using
distributed book books/data-structures/structures.lisp.  At the least,
consider using (set-verify-guards-eagerness 0) to avoid guard
verification.  On the other hand, after you learn to use defstobj, see
DEFABSSTOBJ for another way to introduce single-threaded
objects.

     Example:
     (defconst *mem-size* 10) ; for use of *mem-size* just below
     (defstobj st
               (reg :type (array (unsigned-byte 31) (8))
                    :initially 0)
               (p-c :type (unsigned-byte 31)
                    :initially 555)
               halt                  ; = (halt :type t :initially nil)
               (mem :type (array (unsigned-byte 31) (*mem-size*))
                    :initially 0 :resizable t))

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

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

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

_The Single-Threaded Object Introduced_

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

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

_Restrictions on the Field Descriptions in Defstobj_

Each field descriptor is of the form:

     (fieldi :TYPE typei :INITIALLY vali)

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

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

     (INTEGER 0 31)
     (SIGNED-BYTE 31)
     (ARRAY (SIGNED-BYTE 31) (16))
     (ARRAY (SIGNED-BYTE 31) (*c*)) ; where *c* has a non-negative integer value

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

Non-Array Types

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

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

     (days-off :initially (saturday sunday))

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

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

it would be equivalent to writing

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

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

Array Types

When typei is of the form (ARRAY type-spec (max)), the field is
supposed to be a list of items, initially of length specified by max,
each of which satisfies the indicated type-spec.  Max must be a
non-negative integer or a defined constant evaluating to a non-negative
integer. Thus, each of

     (ARRAY (SIGNED-BYTE 31) (16))
     (ARRAY (SIGNED-BYTE 31) (*c*)) ; given previous event (defconst *c* 16)

restricts the field to be a list of integers, initially of length 16,
where each integer in the list is a (SIGNED-BYTE 31).  We sometimes
call such a list an "array" (because it is represented as an array in
the underlying Common Lisp).  The elements of an array field are
indexed by position, starting at 0.  Thus, the maximum legal index of
an array field one less than is specified by max.  Note that the value
of max must be less than the Common Lisp constant
array-dimension-limit, and also (though this presumably follows) less
than the Common Lisp constant array-total-size-limit.

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

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

Array fields can be "resized," that is, their lengths can be changed, if
:resizable t is supplied as shown in the example and General Form above.
The new length must satisfy the same restriction as does max, as
described above.  Each array field in a defstobj event gives rise to a
length function, which gives the length of the field, and a resize
function, which modifies the length of the field if :resizable t was
supplied with the field when the defstobj was introduced and otherwise
causes an error.  If :resizable t was supplied and the resize function
specifies a new length k, then: if k is less than the existing array
length, the array is shortened simply by dropping elements with index
at least k; otherwise, the array is extended to length k by mapping the
new indices to the initial value (supplied by :initially, else default
nil).

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

_The Default Function Names_

To recap, in

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

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

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

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

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

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

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

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

For example, the event

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

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

This event introduces the following sequence of definitions:

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

_Avoiding the Default Function Names_

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

For example

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

introduces the following definitions

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

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

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

_Constants_

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

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

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

_Inspecting the Effects of a Defstobj_

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

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

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

_immediately after_ the defstobj event has been processed.

A defstobj is considered redundant only if the name, field descriptors,
renaming alist, and inline flag are identical to a previously executed
defstobj.  Note that a redundant defstobj does not reset the stobj
fields to their initial values.

_Inlining and Performance_

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

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

_Specifying Congruent Stobjs_

Two stobjs are may be considered to be "congruent" if they have the same
structure, that is, their defstobj events are identical when ignoring
field names.  In particular, every stobj is congruent to itself.  In
order to tell ACL2 that a new stobj st2 is indeed to be considered as
congruent to an existing stobj st1, the defstobj event introducing st2
is given the keyword argument :congruent-to st1.  Congruence is an
equivalence relation: when you specify a new stobj to be congruent to
an old one, you are also specifying that the new stobj is congruent to
all other stobjs that are congruent to the old one.  Thus, continuing
the example above, if you specify that st3 is :congruent-to st2, then
st1, st2, and st3 will all be congruent to each other.

When two stobjs are congruent, ACL2 allows you to substitute one for
another in a function call.  Any number of stobjs may be replaced with
congruent stobjs in the call, provided no two get replaced with the
same stobj.  The return values are correspondingly modified: if stobj
st1 is replaced by st2 at an argument position, and if st1 is returned
in the output signature of the function, then st2 is returned in place
of st1.

The following example illustrates congruent stobjs.  For more examples
of how to take advantage of congruent stobjs, and also of how to misuse
them, see distributed book books/misc/congruent-stobjs-test.lisp.

     (defstobj st1 fld1)
     (defstobj st2 fld2 :congruent-to st1)
     (defstobj st3 fld3 :congruent-to st2) ; equivalently, :congruent-to st1
     (defun f (st1 st2 st3)
       (declare (xargs :stobjs (st1 st2 st3)))
       (list (fld2 st1) (fld3 st2) (fld1 st3)))
     (update-fld1 1 st1)
     (update-fld1 2 st2) ; notice use of update-fld1 on st2
     (update-fld1 3 st3) ; notice use of update-fld1 on st3
     (assert-event (equal (f st3 st2 st1) '(3 2 1)))

The following example shows an error that occurs when stobj arguments
are repeated, i.e., at least two stobj arguments (in this case, three)
get replaced by the same stobj.

     ACL2 !>(f st1 st1 st1)

     ACL2 Error in TOP-LEVEL:  The form ST1 is being used, as an argument
     to a call of F, where the single-threaded object ST2 was expected,
     even though these are congruent stobjs.  See :DOC defstobj, in particular
     the discussion of congruent stobjs.  Note:  this error occurred in
     the context (F ST1 ST1 ST1).

     ACL2 !>

DEFSTUB    stub-out a function symbol

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

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

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

Defstub macro expands into an encapsulate event (see
ENCAPSULATE).  Thus, no axioms are available about name but it may be
used wherever a function of the given signature is permitted.
Exception: if output-sig is of the form (mv ...), then a
:type-prescription rule is introduced stating that name returns a value
satisfying true-listp.

Old Style:

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

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

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

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

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

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

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

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

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

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

Note that the theory being defined depends on the context.  For example,
consider the following (contrived) example book.

       (in-package "ACL2")
       (defund foo (x) (consp x)) ; defund disables foo
       (local (in-theory (enable foo)))
       (deftheory my-theory (current-theory :here))
       (in-theory (disable foo))
       (defthm foo-property
         (implies (consp x)
                  (foo x))
         :hints (("Goal" :in-theory (enable my-theory))))

At the time foo-property is proved admissible during book certification
(see CERTIFY-BOOK), the local in-theory event has previously
been evaluated, so the definition of foo is enabled.  Thus, the
:in-theory hint on foo-property will enable foo, and the theorem
proves.  HOWEVER, when the book is later included (see
INCLUDE-BOOK), the local event is skipped, so the definition of foo
is disabled at the time the theory my-theory is defined.  Hence, unlike
the case for the admissibility pass of the book's certification, that
theory does not include the definition of foo when the book is included.

There is, however, a way to ensure that a theory defined in a book is
the same at include-book time as it was during the admissibility pass
of the book's certification; see DEFTHEORY-STATIC.

DEFTHEORY-STATIC    define a `static' theory (to enable or disable a set of rules)

This macro provides a variant of deftheory, such that the resulting
theory is the same at include-book time as it was at certify-book time.

We assume that the reader is familiar with theories; see
DEFTHEORY.  We begin here by illustrating how deftheory-static
differs from deftheory.  Suppose for example that the following events
are the first two events in a book, where that book is certified in the
initial ACL2 world (see GROUND-ZERO).

     (deftheory my-theory
       (current-theory :here))
     (deftheory-static my-static-theory
       (current-theory :here))

Now suppose we include that book after executing the following event.

     (in-theory (disable car-cons))

Suppose that later we execute (in-theory (theory 'my-theory)).  Then the
rule car-cons will be disabled, because it was disabled at the time the
expression (current-theory :here) was evaluated when processing the
deftheory of my-theory while including the book.  However, if we
execute (in-theory (theory 'my-static-theory)), then the rule car-cons
will be enabled, because the value of the theory my-static-theory was
saved at the time the book was certified.

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

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

As for deftheory, the value returned is the length of the resulting
theory.

We conclude with an optional discussion about the implementation of
deftheory-static, for those familiar with make-event.  The following
macroexpansion of the deftheory-static form above shows how this works
(see TRANS1).

     ACL2 !>:trans1 (deftheory-static my-static-theory
                      (current-theory :here))
      (MAKE-EVENT (LET ((WORLD (W STATE)))
                       (LIST 'DEFTHEORY
                             'MY-STATIC-THEORY
                             (LIST 'QUOTE (CURRENT-THEORY :HERE)))))
     ACL2 !>

The idea is that upon evaluation of this make-event form, the first step
is to evaluate the indicated LET expression to obtain a form (deftheory
my-theory '(...)), where "(...)" is a list of all runes in current
theory.  If this form is in a book being certified, then the resulting
deftheory form is stored in the book's certificate, and is used when
the book is included later.

DEFTHM    prove and name a theorem

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

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

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

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

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

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

DEFTHMD    prove and name a theorem and then disable it

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

     (defthmd NAME TERM ...)

expands to:

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

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

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

DEFTTAG    introduce a trust tag (ttag)

*Introduction*.  This event is intended for advanced users who, in
essence, want to build extensions of ACL2.  The typical intended use is
to create books that extend the functionality of ACL2 in ways not
allowed without a so-called "active trust tag".  A trust tag thus
represents a contract: The writer of such a book is guaranteeing that
the book extends ACL2 in a "correct" way as defined by the writer of
the book.  The writer of the book will often have a small section of
the book in the scope of an active trust tag that can be inspected by
potential users of that book:

     <initial part of book, which does not use trust tags>
     (defttag :some-ttag) ; install :some-ttag as an active trust tag
     <various code that requires an active trust tag>
     (defttag nil)        ; remove active trust tag
     <initial part of book, which does not use trust tags>

Why might trust tags be needed?  The evaluation of certain functions can
introduce bugs and even unsoundness, but can be useful in restricted
ways that avoid such issues.  For example, sys-call can be used in an
unsafe way, for example to overwrite files, or worse; see
SYS-CALL for a frightening example from Bob Boyer.  The following
example shows that the function sys-call is restricted by default, but
can be called after installing an active trust tag.

     ACL2 !>(sys-call "pwd" nil)

     ACL2 Error in TOP-LEVEL:  The SYS-CALL function cannot be called unless
     a trust tag is in effect.  See :DOC defttag.

     ACL2 !>(defttag t) ; Install :T as an active trust tag.

     TTAG NOTE: Adding ttag :T from the top level loop.
      T
     ACL2 !>(sys-call "pwd" nil) ; print the current directory and return NIL
     /u/kaufmann
     NIL
     ACL2 !>(defttag nil) ; Remove the active trust tag (using value NIL).
      NIL
     ACL2 !>(sys-call "pwd" nil) ; Now we get the error again:

     ACL2 Error in TOP-LEVEL:  The SYS-CALL function cannot be called unless
     a trust tag is in effect.  See :DOC defttag.

     ACL2 !>

Of course, using sys-call with the Linux command pwd is not likely to
cause any soundness problems!  So suppose we want to create a function
that prints the working directory.  We might put the following events
into a book that is to be certified.

     (in-package "ACL2")
     (defttag :pwd-ttag)
     (defun print-working-dir ()
       (declare (xargs :mode :program))
       (sys-call "pwd" nil))
     (defttag nil) ; optional (books end with this implicitly)

We can certify this book with a specification that :pwd-ttag is a legal
trust tag:

     (certify-book "pwd" 0 t :ttags (:pwd-ttag))

One can now use this book by executing include-book with keyword
parameter :ttags (:pwd-ttag) and then calling function
print-working-dir:

     (include-book "pwd" :ttags (:pwd-ttag))
     (print-working-dir) ; working directory is printed to terminal

*Detailed documentation.*

     General Forms:
     (defttag tag-name)
     (defttag tag-name :doc doc-string)

where tag-name is a symbol.  The :doc doc-string argument is optional;
if supplied, then it must be a valid documentation string (see
DOC-STRING), and the defttag call will generate a corresponding
defdoc event for tag-name.  (For the rest of this discussion we ignore
the :doc argument.)

Note however that (other than the :doc argument), if tag-name is not
nil then it is converted to a "corresponding keyword": a symbol in the
"KEYWORD" package with the same symbol-name as tag-name.  Thus, for
example, (defttag foo) is equivalent to (defttag :foo).  Moreover, a
non-nil symbol with a symbol-name of "NIL" is illegal for trust tags;
thus, for example, (defttag :nil) is illegal.

This event introduces or removes a so-called active trust tag (or
"ttag", pronounced "tee tag").  An active ttag is a keyword symbol that
is associated with potentially unsafe evaluation.  For example, calls of
sys-call are illegal unless there is an active trust tag.  An active
trust tag can be installed using a defttag event.  If one introduces an
active ttag and then writes definitions that calls sys-call, presumably
in a defensibly "safe" way, then responsibility for those calls is
attributed to that ttag.  This attribution (or blame!) is at the level
of books; a book's certificate contains a list of ttags that are active
in that book, or in a book that is included (possibly locally), or in a
book included in a book that is included (either inclusion being
potentially local), and so on.  We explain all this in more detail
below.

(Defttag :tag-name) is essentially equivalent to

     (table acl2-defaults-table :ttag :tag-name)

and hence is local to any books and encapsulate events in which it
occurs; see ACL2-DEFAULTS-TABLE.  We say more about the scope of
defttag forms below.

Note: This is an event!  It does not print the usual event summary but
nevertheless executes the above table event and hence changes the ACL2
logical world, and is so recorded.  Although no event summary is
printed, it is important to note that the "TTAG NOTE", discussed below,
is always printed for a non-nil :tag-name (unless deferred; see
SET-DEFERRED-TTAG-NOTES).

*Active ttags.*  Suppose tag-name is a non-nil symbol.  Then (defttag
:tag-name) sets :tag-name to be the (unique) "active ttag."  There must
be an active ttag in order for there to be any mention of certain
function and macro symbols, including sys-call; evaluate the form
(strip-cars *ttag-fns-and-macros*) to see the full list of such
symbols.  On the other hand, (defttag nil) removes the active ttag, if
any; there is then no active ttag.  The scope of a defttag form in a
book being certified or included is limited to subsequent forms in the
same book before the next defttag (if any) in that book.  Similarly, if
a defttag form is evaluated in the top-level loop, then its effect is
limited to subsequent forms in the top-level loop before the next
defttag in the top-level loop (if any).  Moreoever, certify-book is
illegal when a ttag is active; of course, in such a circumstance one
can execute (defttag nil) in order to allow book certification.

*Ttag notes and the "certifier."*  When a defttag is executed with an
argument other than nil, output is printed, starting on a fresh line
with:  TTAG NOTE.  For example:

     ACL2 !>(defttag :foo)

     TTAG NOTE: Adding ttag :FOO from the top level loop.
      :FOO
     ACL2 !>

If the defttag occurs in an included book, the message looks like this.

     TTAG NOTE (for included book): Adding ttag :FOO from file /u/smith/acl2/my-book.lisp.

The "TTAG NOTE" message is always printed on a single line.  The
intention is that one can search the standard output for all such notes
in order to find all defttag events.  In a sense, defttag events can
allow you to define your own system on top of ACL2 (for example, see
PROGN!).  So in order for someone else (who we might call the
"certifier") to be confident that your collection of books is
meaningful, that certifier should certify all the user-supplied books
from scratch and check either that no :ttags were supplied to
certify-book, or else look for every TTAG NOTE in the standard output
in order to locate all defttag events with non-nil tag name.  In this
way, the certifier can in principle decide whether to be satisfied that
those defttag events did not allow inappropriate forms in the
user-supplied books.

In order to eliminate much of the output from TTAG NOTEs, see
SET-DEFERRED-TTAG-NOTES.  Note however that the resulting security is
somewhat less; therefore, a TTAG NOTE is printed when invoking
set-deferred-ttag-notes to defer printing of ttag notes.

*Allowed ttags when certifying and including books.*  A defttag form
may not be evaluated unless its argument is a so-called "allowed" ttag.
All ttags are allowed in the interactive top-level loop.  However,
during certify-book and include-book, the set of allowed ttags is
restricted according to the :ttags keyword argument.  If this argument
is omitted then no ttag is allowed, so a defttag call will fail during
book certification or inclusion in this case.  This restriction applies
even to defttag forms already evaluated in the so-called certification
world at the time certify-book is called.  But note that (defttag nil)
is always legal.

A :ttags argument of certify-book and include-book can have value :all,
indicating that every ttag is allowed, i.e., no restriction is being
placed on the arguments, just as in the interactive top-level loop.  In
the case of include-book, an omitted :ttags argument or an argument of
:default is treated as :all, except that warnings will occur when the
book's certificate includes ttags; but for certify-book, an omitted
ttags argument is treated as nil.  Otherwise, if the :ttags argument is
supplied but not :all, then its value is a true list of ttag
specifications, each having one of the following forms, where sym is a
non-nil symbol which is treated as the corresponding keyword.

     (1) :sym

     (2) (:sym)

     (3) (:sym x1 x2 ... xk), where k > 0 and each xi is a string,
     except that one xi may be nil.

In Case (1), (defttag :sym) is allowed to occur in at most one book or
else in the top-level loop (i.e., the certification world for a book
under certification or a book being included).  Case (2) allows
(defttag :sym) to occur in an unlimited number of books.  For case (3)
the xi specify where (defttag :sym) may occur, as follows.  The case
that xi is nil refers to the top-level loop, while all other xi are
filenames, where the ".lisp" extension is optional and relative
pathnames are considered to be relative to the connected book directory
(see CBD).  Note that the restrictions on (defttag :sym) apply
equally to any equivalent for based on the notion of "corresponding
keyword" discussed above, e.g., (defttag acl2::sym).

An error message, as shown below, illustrates how ACL2 enforcess the
notion of allowed ttags.  Suppose that you call certify-book with
argument :ttags (:foo), where you have already executed (defttag :foo)
in the certification world (i.e., before calling certify-book).  Then
ACL2 immediately associates the ttag :foo with nil, where again, nil
refers to the top-level loop.  If ACL2 then encounters (defttag foo)
inside that book, you will get the following error (using the full book
name for the book, as shown):

     ACL2 Error in ( TABLE ACL2-DEFAULTS-TABLE ...):  The ttag :FOO associated
     with file /u/smith/work/my-book.lisp is not among the set of ttags permitted
     in the current context, specified as follows:
       ((:FOO NIL)).
     See :DOC defttag.

In general the structure displayed by the error message, which is
((:FOO NIL)) in this case, represents the currently allowed ttags with
elements as discussed in (1) through (3) above.  In this case, that
list's unique element is (:FOO NIL), meaning that ttag :FOO is only
allowed at the top level (as represented by NIL).

*Associating ttags with books and with the top-level loop.*  When a book
is certified, each form (defttag tag) that is encountered for non-nil
tag in that book or an included book is recorded in the generated
certificate, which associates the keyword corresponding to tag with the
full-book-name of the book containing that deftag.  If such a defttag
form is encountered outside a book, hence in the portcullis of the book
being certified or one of its included books, then that keyword is
associated with nil in the generated certificate.  Note that the notion
of "included book" here applies to the recursive notion of a book
either included directly in the book being certified or else included
in such a book, where we account even for locally included books.

For examples of ways to take advantage of ttags, see
books/hacking/hacker.lisp and see TTAGS-SEEN, see
PROGN!, see REMOVE-UNTOUCHABLE, see SET-RAW-MODE, and
see SYS-CALL.

DEFUN    define a function symbol

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

     (o-p (m x y)).

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

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

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

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

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

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

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

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

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

This completes the brief sketch of the ACL2 definitional principle.
Optionally, see RULER-EXTENDERS for a more detailed discussion
of the termination analysis and resulting proof obligations for
admissibility, as well as a discussion of the relation to how ACL2
stores induction schemes.

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

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

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

DEFUN-INLINE    define a potentially inlined function symbol and associated macro

You may be able to improve performance by replacing an event (defun f
...) with a corresponding event (defun-inline f ...), in order to
encourage the host Lisp compiler to inline calls of f.

     Example Form:
     (defun-inline lng (x)
       (declare (xargs :guard (true-listp x)))
       (if (endp x) 0 (1+ (lng (cdr x)))))

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

satisfying the same requirements as in the General Form for defun.  The
effect is to define a macro fn and a function fn$inline (i.e., a symbol
in the same package as fn but whose symbol-name has the suffix
"$INLINE", such that each call of fn expands to a call of the function
symbol fn$inline on the same arguments.  If doc-string is supplied,
then it is associated with fn, not with fn$inline.  Moreover, table
events are generated that allow the use of fn in theory expressions to
represent fn$inline and that cause any untranslated (user-level) call
of fn$inline to be printed as the corresponding call of fn.

A form (defun-inline f ...) actually defines a function named f$inline
and a corresponding macro named f whose calls expand to calls of
f$inline, while providing the illusion that there is just the
"function" f.  For example, the Example Form above macroexpands in one
step to the following form.

     (progn (defmacro lng (non-stobj-var0)
              (list 'lng$inline non-stobj-var0))
            (add-macro-fn lng lng$inline)
            (defun lng$inline (x)
              (declare (xargs :guard (true-listp x)))
              (if (endp x) 0 (1+ (lng (cdr x))))))

Note that the above call of add-macro-fn generates the aforementioned
two table events (see ADD-MACRO-FN), which provide the illusion
that we are just defining a function lng, as you can see in the
following log: lng appears rather than lng$inline.

     ACL2 !>(set-gag-mode nil)
     <state>
     ACL2 !>(thm (equal (lng (append x y))
                        (+ (lng x) (lng y)))
                 :hints (("Goal" :in-theory (enable lng))))

     [.. output omitted ..]

     Subgoal *1/2
     (IMPLIES (AND (NOT (ENDP X))
                   (EQUAL (LNG (APPEND (CDR X) Y))
                          (+ (LNG (CDR X)) (LNG Y))))
              (EQUAL (LNG (APPEND X Y))
                     (+ (LNG X) (LNG Y)))).

     [.. output omitted ..]

Under the hood, ACL2 arranges that every function symbol with suffix
"$INLINE" is presented to the compiler as one whose calls we would
prefer to inline.  Technically: the Common Lisp form (declaim (inline
f$inline)) is generated for a function symbol f$inline before that
symbol's definition is submitted.  However, the Common Lisp spec
explicitly avoids requiring that the compiler respect this declaim
form.  Fortunately, Common Lisp implementations often do respect it.

Also see DEFUND-INLINE, see DEFUN-NOTINLINE, and see
DEFUND-NOTINLINE.

_Remarks_.

(1) None of these macros (including defun-inline) is supported for use
inside a mutual-recursion.

(2) Every function symbol defined in ACL2 whose symbol-name has the
suffix "$INLINE" is proclaimed to be inline; similarly for "$NOTINLINE"
and notinline.

(3) No special treatment for inlining (or notinlining) is given for
function symbols locally defined by flet, except in the case of symbols
discussed in (1) and (2) above that, at some point in the current ACL2
session, were defined as function symbols in ACL2 (even if not currently
defined because of undoing or being local).

(4) The function symbol actually being defined by (defun-inline foo ...)
is foo$inline.  As mentioned above, one can be oblivious to this fact
when writing theory expressions or perusing prover output.  However, for
other purposes (for example, verify-guards and defabsstobj :exports)
you will need to supply the name of the function symbol rather than the
name of the macro; e.g., for the above form (defun-inline foo ...), you
may subsequently issue the event (verify-guards foo$inline) but not
(verify-guards foo).

(5) Obscure Remark.  Suppose that you certify a book with compilation
(the default) in one host Lisp, saving the expansion file.  Suppose
that you then compile in another host Lisp by using include-book with
argument :load-compiled-file :comp.  Then in subsequent sessions,
including that book with the second host Lisp will not result in any
inline or notinline behavior for functions defined in the book.  This
may be fixed in a future release if someone complains.

DEFUN-NOTINLINE    define a not-to-be-inlined function symbol and associated macro

See DEFUN-INLINE for an analogous utility that supports
inlining.  The present utility is probably far less useful; it tells
the compiler _not_ to inline calls of the function being defined.  Also
see DEFUND-NOTINLINE for a variant of this event that disables
the newly-defined function symbol.

Under the hood, (defun-inline f ...) and (defun-notinline f ...)  cause
evaluation of Common Lisp forms (declaim (inline f$inline)) and
(declaim (notinline f$notinline)), respectively.  According to the
Common Lisp spec, the compiler need not respect the first of these (for
inline), but it must respect the second of these (for notinline).
Fortunately, Common Lisp implementations often do respect the first of
these as well.

DEFUN-NX    define a non-executable function symbol

     Example:

     (set-state-ok t)
     (defun-nx foo (x state)
       (mv-let (a b c)
               (cons x state)
               (list a b c b a)))
     ; Note ``ill-formed'' call of foo just below.
     (defun bar (state y)
       (foo state y))

The macro defun-nx introduces definitions using the defun macro, always
in :logic mode, such that the calls of the resulting function cannot be
evaluated.  Such a definition is admitted without enforcing syntactic
restrictions for executability, in particular for single-threadedness
(see STOBJ) and multiple-values passing (see MV and see
MV-LET).  After such a definition is admitted, the usual
syntactic rules for state and user-defined stobjs are relaxed for calls
of the function it defines.  Also see NON-EXEC for a way to
designate subterms of function bodies, or subterms of code to be
executed at the top level, as non-executable.

The syntax of defun-nx is identical to that of defun.  A form

     (defun-nx name (x1 ... xk) ... body)

expands to the following form.

     (defun name (x1 ... xk)
       (declare (xargs :non-executable t :mode :logic))
       ...
       (prog2$ (throw-nonexec-error 'name (list x1 ... xk))
               body))

Note that because of the insertion of the above call of
throw-nonexec-error, no formal is ignored when using defun-nx.

During proofs, the error is silent; it is "caught" by the proof
mechanism and generally results in the introduction of a call of hide
during a proof.  If an error message is produced by evaluating a call
of the function on a list of arguments that includes state or
user-defined stobjs, these arguments will be shown as symbols such as
|<state>| in the error message.  In the case of a user-defined stobj
bound by with-local-stobj, the symbol printed will include the suffix
{local-stobj}, for example, |<st>{local-stobj}|.

It is harmless to include :non-executable t in your own xargs declare
form; defun-nx will still lay down its own such declaration, but ACL2
can tolerate the duplication.

Note that defund-nx is also available.  It has an effect identical to
that of defun-nx except that as with defund, it leaves the function
disabled.

If you use guards (see GUARD), please be aware that even though
syntactic restrictions are relaxed for defun-nx, guard verification
proceeds exactly as for defun.  If you want ACL2 to skip a form for
purposes of generating guard proof obligations, use the macro non-exec,
which generates a call of throw-nonexec-error that differs somewhat
from the one displayed above.  See NON-EXEC.

See DEFUN for documentation of defun.

DEFUN-SK    define a function whose body has an outermost quantifier

     Examples:
     (defun-sk exists-x-p0-and-q0 (y z)
       (exists x
               (and (p0 x y z)
                    (q0 x y z))))

     (defun-sk exists-x-p0-and-q0 (y z) ; equivalent to the above
       (exists (x)
               (and (p0 x y z)
                    (q0 x y z))))

     (defun-sk forall-x-y-p0-and-q0 (z)
       (forall (x y)
               (and (p0 x y z)
                    (q0 x y z)))
       :strengthen t)

     * Menu:

     * DEFUN-SK-EXAMPLE:: a simple example using defun-sk

     * EXISTS:: existential quantifier

     * FORALL:: universal quantifier

     * QUANTIFIER-TUTORIAL:: A Beginner's Guide to Reasoning about Quantification in ACL2

     * QUANTIFIERS:: issues about quantification in ACL2

     General Form:
     (defun-sk fn (var1 ... varn) body
       &key rewrite doc quant-ok skolem-name thm-name witness-dcls strengthen)

where fn is the symbol you wish to define and is a new symbolic name
(see NAME), (var1 ... varn) is its list of formal parameters
(see NAME), and body is its body, which must be quantified as
described below.  The &key argument doc is an optional documentation
string to be associated with fn; for a description of its form, see
DOC-STRING.  In the case that n is 1, the list (var1) may be
replaced by simply var1.  The other arguments are explained below.

For a simple example, see DEFUN-SK-EXAMPLE.  For a more
elaborate example, see TUTORIAL4-DEFUN-SK-EXAMPLE.  See
QUANTIFIER-TUTORIAL for a careful beginner's introduction that takes
you through typical kinds of quantifier-based reasoning in ACL2.  Also
see QUANTIFIERS for an example illustrating how the use of
recursion, rather than explicit quantification with defun-sk, may be
preferable.

Below we describe the defun-sk event precisely.  First, let us consider
the examples above.  The first example, again, is:

     (defun-sk exists-x-p0-and-q0 (y z)
       (exists x
               (and (p0 x y z)
                    (q0 x y z))))

It is intended to represent the predicate with formal parameters y and
z that holds when for some x, (and (p0 x y z) (q0 x y z)) holds.  In
fact defun-sk is a macro that adds the following two events, as shown
just below.  The first event guarantees that if this new predicate
holds of y and z, then the term shown, (exists-x-p0-and-q0-witness y
z), is an example of the x that is therefore supposed to exist.
(Intuitively, we are axiomatizing exists-x-p0-and-q0-witness to pick a
witness if there is one.  We comment below on the use of defun-nx; for
now, consider defun-nx to be defun.)  Conversely, the second event
below guarantees that if there is any x for which the term in question
holds, then the new predicate does indeed hold of y and z.

     (defun-nx exists-x-p0-and-q0 (y z)
       (let ((x (exists-x-p0-and-q0-witness y z)))
         (and (p0 x y z) (q0 x y z))))
     (defthm exists-x-p0-and-q0-suff
       (implies (and (p0 x y z) (q0 x y z))
                (exists-x-p0-and-q0 y z)))

Now let us look at the third example from the introduction above:

     (defun-sk forall-x-y-p0-and-q0 (z)
       (forall (x y)
               (and (p0 x y z)
                    (q0 x y z))))

The intention is to introduce a new predicate (forall-x-y-p0-and-q0 z)
which states that the indicated conjunction holds of all x and all y
together with the given z.  This time, the axioms introduced are as
shown below.  The first event guarantees that if the application of
function forall-x-y-p0-and-q0-witness to z picks out values x and y for
which the given term (and (p0 x y z) (q0 x y z)) holds, then the new
predicate forall-x-y-p0-and-q0 holds of z.  Conversely, the
(contrapositive of) the second axiom guarantees that if the new
predicate holds of z, then the given term holds for all choices of x
and y (and that same z).

     (defun-nx forall-x-y-p0-and-q0 (z)
       (mv-let (x y)
               (forall-x-y-p0-and-q0-witness z)
               (and (p0 x y z) (q0 x y z))))
     (defthm forall-x-y-p0-and-q0-necc
       (implies (not (and (p0 x y z) (q0 x y z)))
                (not (forall-x-y-p0-and-q0 z))))

The examples above suggest the critical property of defun-sk:  it
indeed does introduce the quantified notions that it claims to
introduce.

Notice that the defthm event just above, forall-x-y-p0-and-q0-necc, may
not be of optimal form as a rewrite rule.  Users sometimes find that
when the quantifier is forall, it is useful to state this rule in a
form where the new quantified predicate is a hypothesis instead.  In
this case that form would be as follows:

     (defthm forall-x-y-p0-and-q0-necc
       (implies (forall-x-y-p0-and-q0 z)
                (and (p0 x y z) (q0 x y z))))

ACL2 will turn this into one :rewrite rule for each conjunct, (p0 x y
z) and (q0 x y z), with hypothesis (forall-x-y-p0-and-q0 z) in each
case.  In order to get this effect, use :rewrite :direct, in this case
as follows.

     (defun-sk forall-x-y-p0-and-q0 (z)
       (forall (x y)
               (and (p0 x y z)
                    (q0 x y z)))
       :rewrite :direct)

We now turn to a detailed description of defun-sk, starting with a
discussion of its arguments as shown in the "General Form" above.

The third argument, body, must be of the form

     (Q bound-vars term)

where:  Q is the symbol forall or exists (in the "ACL2" package),
bound-vars is a variable or true list of variables disjoint from (var1
... varn) and not including state, and term is a term.  The case that
bound-vars is a single variable v is treated exactly the same as the
case that bound-vars is (v).

The result of this event is to introduce a "Skolem function," whose
name is the keyword argument skolem-name if that is supplied, and
otherwise is the result of modifying fn by suffixing "-WITNESS" to its
name.  The following definition and one of the following two theorems
(as indicated) are introduced for skolem-name and fn in the case that
bound-vars (see above) is a single variable v.  The name of the defthm
event may be supplied as the value of the keyword argument :thm-name;
if it is not supplied, then it is the result of modifying fn by
suffixing "-SUFF" to its name in the case that the quantifier is
exists, and "-NECC" in the case that the quantifier is forall.

     (defun-nx fn (var1 ... varn)
       (let ((v (skolem-name var1 ... varn)))
         term))

     (defthm fn-suff ;in case the quantifier is EXISTS
       (implies term
                (fn var1 ... varn)))

     (defthm fn-necc ;in case the quantifier is FORALL
       (implies (not term)
                (not (fn var1 ... varn))))

In the forall case, however, the keyword pair :rewrite :direct may be
supplied after the body of the defun-sk form, in which case the
contrapositive of the above form is used instead:

     (defthm fn-necc ;in case the quantifier is FORALL
       (implies (fn var1 ... varn)
                term))

This is often a better choice for the "-NECC" rule, provided ACL2 can
parse term as a :rewrite rule.  A second possible value of the :rewrite
argument of defun-sk is :default, which gives the same behavior as when
:rewrite is omitted.  Otherwise, the value of :rewrite should be the
term to use as the body of the fn-necc theorem shown above; ACL2 will
attempt to do the requisite proof in this case.  If that term is weaker
than the default, the properties introduced by defun-sk may of course
be weaker than they would be otherwise.  Finally, note that the
:rewrite keyword argument for defun-sk only makes sense if the
quantifier is forall; it is thus illegal if the quantifier is exists.
Enough said about :rewrite!

In the case that bound-vars is a list of at least two variables, say
(bv1 ... bvk), the definition above (with no keywords) is the following
instead, but the theorem remains unchanged.

     (defun-nx fn (var1 ... varn)
       (mv-let (bv1 ... bvk)
               (skolem-name var1 ... varn)
               term))

In order to emphasize that the last element of the list, body, is a
term, defun-sk checks that the symbols forall and exists do not appear
anywhere in it.  However, on rare occasions one might deliberately
choose to violate this convention, presumably because forall or exists
is being used as a variable or because a macro call will be eliminating
"calls of" forall and exists.  In these cases, the keyword argument
quant-ok may be supplied a non-nil value.  Then defun-sk will permit
forall and exists in the body, but it will still cause an error if
there is a real attempt to use these symbols as quantifiers.

The use of defun-nx above, rather than defun, disables certain checks
that are required for evaluation, in particular the single-threaded use
of stobjs.  However, there is a price: calls of these defined functions
cannot be evaluated; see DEFUN-NX.  Normally that is not a
problem, since these notions involve quantifiers.  But you are welcome
to replace this declare form with your own, as follows: if you supply a
list of declare forms to keyword argument :witness-dcls, these will
become the declare forms in the generated defun.  Note that if your
value of witness-dcls does not contain the form (declare (xargs
:non-executable t)), then the appropriate wrapper for non-executable
functions will not be added automatically, i.e., defun will be used in
place of defun-nx.  Note also that if guard verification is attempted,
then it will likely fail with an error message complaining that "guard
verification may depend on local properties."  In that case, you may
wish to delay guard verification, as in the following example.

     (encapsulate
      ()
      (defun-sk foo (x)
        (exists n (and (integerp n)
                       (< n x)))
        :witness-dcls ((declare (xargs :guard (integerp x)
                                       :verify-guards nil))))
      (verify-guards foo))

Defun-sk is a macro implemented using defchoose.  Hence, it should only
be executed in defun-mode :logic; see DEFUN-MODE and see
DEFCHOOSE.  Advanced feature: If argument :strengthen t is passed to
defun-sk, then :strengthen t will generate the extra constraint that
that is generated for the corresponding defchoose event; see
DEFCHOOSE.  You can use the command :pcb! to see the event generated
by a call of the defun-sk macro.

If you find that the rewrite rules introduced with a particular use of
defun-sk are not ideal, even when using the :rewrite keyword discussed
above (in the forall case), then at least two reasonable courses of
action are available for you.  Perhaps the best option is to prove the
rewrite rules you want.  If you see a pattern for creating rewrite
rules from your defun-sk events, you might want to write a macro that
executes a defun-sk followed by one or more defthm events.  Another
option is to write your own variant of the defun-sk macro, say,
my-defun-sk, for example by modifying a copy of the definition of
defun-sk from the ACL2 sources.

If you want to represent nested quantifiers, you can use more than one
defun-sk event.  For example, in order to represent

     (forall x (exists y (p x y z)))

you can use defun-sk twice, for example as follows.

     (defun-sk exists-y-p (x z)
       (exists y (p x y z)))

     (defun-sk forall-x-exists-y-p (z)
       (forall x (exists-y-p x z)))

Some distracting and unimportant warnings are inhibited during defun-sk.

Note that this way of implementing quantifiers is not a new idea.
Hilbert was certainly aware of it 60 years ago!  Also see
CONSERVATIVITY-OF-DEFCHOOSE for a technical argument that justifies
the logical conservativity of the defchoose event in the sense of the
paper by Kaufmann and Moore entitled "Structured Theory Development for
a Mechanized Logic" (Journal of Automated Reasoning 26, no. 2 (2001),
pp. 161-203).

DEFUN-SK-EXAMPLE    a simple example using defun-sk

For a more through, systematic beginner's introduction to
quantification in ACL2, see QUANTIFIER-TUTORIAL.

The following example illustrates how to do proofs about functions
defined with defun-sk.  The events below can be put into a certifiable
book (see BOOKS).  The example is contrived and rather silly,
in that it shows how to prove that a quantified notion implies itself,
where the antecedent and conclusion are defined with different defun-sk
events.  But it illustrates the formulas that are generated by
defun-sk, and how to use them.  Thanks to Julien Schmaltz for
presenting this example as a challenge.

     (in-package "ACL2")

     (encapsulate
      (((p *) => *)
       ((expr *) => *))

      (local (defun p (x) x))
      (local (defun expr (x) x)))

     (defun-sk forall-expr1 (x)
       (forall (y) (implies (p x) (expr y))))

     (defun-sk forall-expr2 (x)
       (forall (y) (implies (p x) (expr y)))))

     ; We want to prove the theorem my-theorem below.  What axioms are there that
     ; can help us?  If you submit the command

     ; :pcb! forall-expr1

     ; then you will see the following two key events.  (They are completely
     ; analogous of course for FORALL-EXPR2.)

     ;   (DEFUN FORALL-EXPR1 (X)
     ;     (LET ((Y (FORALL-EXPR1-WITNESS X)))
     ;          (IMPLIES (P X) (EXPR Y))))
     ;
     ;   (DEFTHM FORALL-EXPR1-NECC
     ;     (IMPLIES (NOT (IMPLIES (P X) (EXPR Y)))
     ;              (NOT (FORALL-EXPR1 X)))
     ;     :HINTS
     ;     (("Goal" :USE FORALL-EXPR1-WITNESS)))

     ; We see that the latter has value when FORALL-EXPR1 occurs negated in a
     ; conclusion, or (therefore) positively in a hypothesis.  A good rule to
     ; remember is that the former has value in the opposite circumstance: negated
     ; in a hypothesis or positively in a conclusion.

     ; In our theorem, FORALL-EXPR2 occurs positively in the conclusion, so its
     ; definition should be of use.  We therefore leave its definition enabled,
     ; and disable the definition of FORALL-EXPR1.

     ;   (thm
     ;     (implies (and (p x) (forall-expr1 x))
     ;              (forall-expr2 x))
     ;     :hints (("Goal" :in-theory (disable forall-expr1))))
     ;
     ;   ; which yields this unproved subgoal:
     ;
     ;   (IMPLIES (AND (P X) (FORALL-EXPR1 X))
     ;            (EXPR (FORALL-EXPR2-WITNESS X)))

     ; Now we can see how to use FORALL-EXPR1-NECC to complete the proof, by
     ; binding y to (FORALL-EXPR2-WITNESS X).

     ; We use defthmd below so that the following doesn't interfere with the
     ; second proof, in my-theorem-again that follows.
     (defthmd my-theorem
       (implies (and (p x) (forall-expr1 x))
                (forall-expr2 x))
       :hints (("Goal"
                :use ((:instance forall-expr1-necc
                                 (x x)
                                 (y (forall-expr2-witness x)))))))

     ; The following illustrates a more advanced technique to consider in such
     ; cases.  If we disable forall-expr1, then we can similarly succeed by having
     ; FORALL-EXPR1-NECC applied as a :rewrite rule, with an appropriate hint in how
     ; to instantiate its free variable.  See :doc hints.

     (defthm my-theorem-again
       (implies (and (P x) (forall-expr1 x))
                (forall-expr2 x))
       :hints (("Goal"
                :in-theory (disable forall-expr1)
                :restrict ((forall-expr1-necc
                            ((y (forall-expr2-witness x))))))))

EXISTS    existential quantifier

The symbol exists (in the ACL2 package) represents existential
quantification in the context of a defun-sk form.  See DEFUN-SK
and see FORALL.

See QUANTIFIERS for an example illustrating how the use of
recursion, rather than explicit quantification with defun-sk, may be
preferable.

FORALL    universal quantifier

The symbol forall (in the ACL2 package) represents universal
quantification in the context of a defun-sk form.  See DEFUN-SK
and see EXISTS.

See QUANTIFIERS for an example illustrating how the use of
recursion, rather than explicit quantification with defun-sk, may be
preferable.