This is documentation for ACL2 Version 4.0
Copyright (C) 2010  University of Texas at Austin

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

Written by:  Matt Kaufmann and J Strother Moore
Department of Computer Sciences
University of Texas at Austin
Austin, TX 78712-1188 U.S.A.

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 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 and a summary of warnings.  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).

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 (as briefly explained in ld-error-triples and er-progn), 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 an explanation of how custom keyword hints are processed, see
CUSTOM-KEYWORD-HINTS.

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 creates various files whose names start with "TMP*",
but 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.

:cited-by Programming

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.

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.

*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, and
especially evaluation of ground terms (terms without free variables)
during proofs.  Regarding the last of these, 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).  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 us for the result of applying s to u; that is, us 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.  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 Cs 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.  This is illustrated by
the use of constrained function too-many-ifs-post-rewrite-wrapper in
the ACL2 source code, for a heuristic used in the rewriter.  Early in
an ACL2 build, this function receives a trivial attachment that
implements a trivial heuristic.  Then late in the ACL2 build, that
attachment is replaced, so that the wrapper receives a more interesting
attachment, one which implements the desired heuristic.

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.  We can consider attachment as refinement with a
moreformal perspective: 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-wrapper 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)).

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, consider using the macro defconst-fast
instead, defined in books/make-event/defconst-fast.lisp, for example:

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

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.)

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 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 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-eq 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, see MAKE-EVENT.

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.

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.

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'.

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.

     Example:
     (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) (64))
                    :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 inline-flag)

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 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-flag 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).  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 the corresponding
element of the stobj is initially a list of length 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))

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 max, each of which
satisfies the indicated type-spec.  Max must be a non-negative integer.
Thus,

     (ARRAY (SIGNED-BYTE 31) (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 is max-1.  Note that 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 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.

DEFSTUB    stub-out a function symbol

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

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

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 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 -- often simply in a sound way --.  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 may 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 the rest of this discussion we ignore the :doc
argument.

This event introduces or removes a so-called active trust tag (or
"ttag", pronounced "tee tag").  An active ttag is a non-nil symbol
(tag) 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 "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 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.

     (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).

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 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 tag 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-NX    define a non-executable function symbol

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 the syntactic
restrictions usually imposed on definitions, as opposed to theorems, in
particular regarding function signatures and the use of single-threaded
object names, even though such functions are permitted to declare names
to be :stobjs.

The syntax 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.

If you prefer to avoid the use of defun-nx for non-executable function
definitions in :logic mode, you can use an xargs :non-executable t
declare form, provided the body has the form (prog2$
(throw-nonexec-error ...) ...).  The function throw-nonexec-error is
guaranteed to cause an error, though the :non-executable keyword will
lay down code such that an error generally occurs when calling name
without calling throw-nonexec-error.

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.

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 identitcal to
that of defun-nx except that as with defund, it leaves the function
disabled.

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.

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.

QUANTIFIER-TUTORIAL    A Beginner's Guide to Reasoning about Quantification in ACL2

The initial version of this tutorial was written by Sandip Ray.
Additions and revisions are welcome.  Sandip has said:

     "This is a collection of notes that I wrote to remind myself of
     how to reason about quantifiers when I just started.  Most users
     after they have gotten the hang of quantifiers probably will not
     need this and will be able to use their intuitions to guide them
     in the process.  But since many ACL2 users are not used to
     quantification, I am hoping that this set of notes might help them
     to think clearly while reasoning about quantifiers in ACL2."

Many ACL2 papers start with the sentence "ACL2 is a quantifier-free
first-order logic of recursive functions."  It is true that the _syntax_
of ACL2 is quantifier-free; every formula is assumed to be universally
quantified over all free variables in the formula.  But the _logic_ in
fact does afford arbitrary first-order quantification.  This is
obtained in ACL2 using a construct called defun-sk.  See
DEFUN-SK.

Many ACL2 users do not think in terms of quantifiers.  The focus is
almost always on defining recursive functions and reasoning about them
using induction.  That is entirely justified, in fact, since proving
theorems about recursive functions by induction plays to the strengths
of the theorem prover.  Nevertheless there are situations where it is
reasonable and often useful to think in terms of quantifiers.  However,
reasoning about quantifiers requires that you get into the mindset of
thinking about theorems in terms of quantification.  This note is about
how to do this effectively given ACL2's implementation of
quantification.  This does not discuss defun-sk in detail, but merely
shows some examples.  A detailed explanation of the implementation is
in the ACL2 documentation (see DEFUN-SK); also see
CONSERVATIVITY-OF-DEFCHOOSE.

[Note: Quantifiers can be used for some pretty cool things in ACL2.
Perhaps the most interesting example is the way of using quantifiers to
introduce arbitrary tail-recursive equations; see the paper "Partial
Functions in ACL2" by Panagiotis Manolios and J Strother Moore.  This
note does not address applications of quantifiers, but merely how you
would reason about them once you think you want to use them.]

Assume that you have some function P.  I have just left P as a unary
function stub below, since I do not care about what P is.

     (defstub P (*) => *)

Now suppose you want to specify the concept that "there exists some x
such that (P x) holds".  ACL2 allows you to write that directly using
quantifiers.

     (defun-sk exists-P () (exists x (P x)))

If you submit the above form in ACL2 you will see that the theorem
prover specifies two functions exists-p and exists-p-witness, and
exports the following constraints:

     1.  (defun exists-P () (P (exists-P-witness)))
     2.  (defthm exists-P-suff (implies (p x) (exists-p)))

Here exists-P-witness is a new function symbol in the current ACL2
theory.  What do the constraints above say?  Notice the constraint
exists-p-suff.  It says that if you can provide any x such that (P x)
holds, then you know that exists-p holds.  Think of the other
constraint (definition of exists-p) as going the other way.  That is, it
says that if exists-p holds, then there is some x, call it
(exists-p-witness), for which P holds.  Notice that nothing else is
known about exists-p-witness than the two constraints above.

[Note: exists-p-witness above is actually defined in ACL2 using a
special form called defchoose.  See DEFCHOOSE.  This note does
not talk about defchoose.  So far as this note is concerned, think of
exists-p-witness as a new function symbol that has been generated
somehow in ACL2, about which nothing other than the two facts above is
known.]

Similarly, you can talk about the concept that "for all x (P x) holds."
This can be specified in ACL2 by the form:

     (defun-sk forall-P () (forall x (P x)))

This produces the following two constraints:

     1.  (defun forall-P () (P (forall-p-witness)))
     2.  (defthm forall-p-necc (implies (not (P x)) (not (forall-p))))

To understand these, think of for-all-p-witness as producing some x
which does not satisfy P, if such a thing exists.  The constraint
forall-p-necc merely says that if forall-p holds then P is satisfied
for every x.  (To see this more clearly, just think of the
contrapositive of the formula shown.) The other constraint (definition
of forall-p) implies that if forall-p does not hold then there is some
x, call it (forall-p-witness), which does not satisfy P.  To see this,
just consider the following formula which is immediately derivable from
the definition.

     (implies (not (forall-p)) (not (P (forall-witness))))

The description above suggests that to reason about quantifiers, the
following Rules of Thumb, familiar to most any student of logic, are
useful.

     RT1: To prove (exists-p), construct some object A such that P
     holds for A and then use exists-P-suff.

     RT2: If you assume exists-P in your hypothesis, use the definition
     of exists-p to know that P holds for exists-p-witness.  To use this
     to prove a theorem, you must be able to derive the theorem based
     on the hypothesis that P holds for something, whatever the
     something is.

     RT3: To prove forall-P, prove the theorem (P x) (that is, that P
     holds for an arbitrary x), and then simply instantiate the
     definition of forall-p, that is, show that P holds for the witness.

     RT4: If you assume forall-p in the hypothesis of the theorem, see
     how you can prove your conclusion if indeed you were given (P x)
     as a theorem.  Possibly for the conclusion to hold, you needed
     that P holds for some specific set of x values.  Then use the
     theorem forall-p-necc by instantiating it for the specific x
     values you care about.

Perhaps the above is too terse.  In the remainder of the note, we will
consider several examples of how this is done to prove theorems in ACL2
that involve quantified notions.

Let us consider two trivial theorems.  Assume that for some unary
function r, you have proved (r x) as a theorem.  Let us see how you can
prove that (1) there exists some x such that (r x) holds, and (2) for
all x (r x) holds.

We first model these things using defun-sk.  Below, r is simply some
function for which (r x) is a theorem.

     (encapsulate
      (((r *) => *))
      (local (defun r (x) (declare (ignore x)) t))
      (defthm r-holds (r x)))

     (defun-sk exists-r () (exists x (r x)))
     (defun-sk forall-r () (forall x (r x)))

ACL2 does not have too much reasoning support for quantifiers.  So in
most cases, one would need :use hints to reason about quantifiers.  In
order to apply :use hints, it is preferable to keep the function
definitions and theorems disabled.

     (in-theory (disable exists-r exists-r-suff forall-r forall-r-necc))

Let us now prove that there is some x such that (r x) holds.  Since we
want to prove exists-r, we must use exists-r-suff by RT1.  We do not
need to construct any instance here since r holds for all x by the
theorem above.

     (defthm exists-r-holds
       (exists-r)
       :hints (("Goal" :use ((:instance exists-r-suff)))))

Let us now prove the theorem that for all x, (r x) holds.  By RT3, we
must be able to prove it by definition of forall-r.

     (defthm forall-r-holds
       (forall-r)
       :hints (("Goal" :use ((:instance (:definition forall-r))))))

[Note: Probably no ACL2 user in his or her right mind would prove the
theorems exists-r-holds and forall-r-holds above.  The theorems shown
are only for demonstration purposes.]

For the remainder of this note we will assume that we have two stubbed
out unary functions M and N, and we will look at proving some quantified
properties of these functions.

     (defstub M (*) => *)
     (defstub N (*) => *)

Let us now define the predicates all-M, all-N, ex-M, and ex-N
specifying the various quantifications.

     (defun-sk all-M () (forall x (M x)))
     (defun-sk all-N () (forall x (N x)))
     (defun-sk some-M () (exists x (M x)))
     (defun-sk some-N () (exists x (N x)))

     (in-theory (disable all-M all-N all-M-necc all-N-necc))
     (in-theory (disable some-M some-N some-M-suff some-N-suff))

Let us prove the classic distributive properties of quantification: the
distributivity of universal quantification over conjunction, and the
distributivity of existential quantification over disjunction.  We can
state these properties informally in "pseudo ACL2" notation as follows:

     1.  (exists x: (M x)) or (exists x: (N x)) <=> (exists x: (M x) or (N x))
     2.  (forall x: (M x)) and (forall: x (N x)) <=> (forall x: (M x) and (N x))

To make these notions formal we of course need to define the formulas
at the right-hand sides of 1 and 2.  So we define some-MN and all-MN to
capture these concepts.

     (defun-sk some-MN () (exists x (or (M x) (N x))))
     (defun-sk all-MN () (forall x (and (M x) (N x))))

     (in-theory (disable all-MN all-MN-necc some-MN some-MN-suff))

First consider proving property 1.  The formal statement of this
theorem would be: (iff (some-MN) (or (some-M) (some-N))).

How do we prove this theorem?  Looking at RT1-RT4 above, note that they
suggest how one should reason about quantification when one has an
"implication".  But here we have an "equivalence".  This suggests
another rule of thumb.

     RT5: Whenever possible, prove an equivalence involving quantifiers
     by proving two implications.

Let us apply RT5 to prove the theorems above.  So we will first prove:
(implies (some-MN) (or (some-M) (some-N)))

How can we prove this?  This involves assuming a quantified predicate
(some-MN), so we must use RT2 and apply the definition of some-MN.
Since the conclusion involves a disjunction of two quantified
predicates, by RT1 we must be able to construct two objects A and B
such that either M holds for A or N holds for B, so that we can then
invoke some-M-suff and some-N-suff to prove the conclusion.  But now
notice that if some-MN is true, then there is already an object, in fact
some-MN-witness, such that either M holds for it, or N holds for it.
And we know this is the case from the definition of some-MN! So we will
simply prove the theorem instantiating some-M-suff and some-N-suff with
this witness.  The conclusion is that the following event will go
through with ACL2.

     (defthm le1
       (implies (some-MN)
                (or (some-M) (some-N)))
       :rule-classes nil
       :hints (("Goal"
                 :use ((:instance (:definition some-MN))
                       (:instance some-M-suff
                                  (x (some-MN-witness)))
                       (:instance some-N-suff
                                  (x (some-MN-witness)))))))

This also suggests the following rule of thumb:

     RT6: If a conjecture involves assuming an existentially quantified
     predicate in the hypothesis from which you are trying to prove an
     existentially quantified predicate, use the witness of the
     existential quantification in the hypothesis to construct the
     witness for the existential quantification in the conclusion.

Let us now try to prove the converse of le1, that is: (implies (or
(some-M) (some-N)) (some-MN))

Since the hypothesis is a disjunction, we will just prove each case
individually instead of proving the theorem by a :cases hint.  So we
prove the following two lemmas.

     (defthm le2
       (implies (some-M) (some-MN))
       :rule-classes nil
       :hints (("Goal"
                 :use ((:instance (:definition some-M))
                       (:instance some-MN-suff
                                  (x (some-M-witness)))))))

     (defthm le3
       (implies (some-N) (some-MN))
       :rule-classes nil
       :hints (("Goal"
                 :use ((:instance (:definition some-N))
                       (:instance some-MN-suff
                                  (x (some-N-witness)))))))

Note that the hints above are simply applications of RT6 as in le1.
With these lemmas, of course the main theorem is trivial.

     (defthmd |some disjunction|
       (iff (some-MN) (or (some-M) (some-N)))
       :hints (("Goal"
                 :use ((:instance le1)
                       (:instance le2)
                       (:instance le3)))))

Let us now prove the distributivity of universal quantification over
conjunction, that is, the formula: (iff (all-MN) (and (all-M) (all-N)))

Applying RT5, we will again decompose this into two implications.  So
consider first the one-way implication: (implies (and (all-M) (all-N))
(all-MN)).

Here we get to assume all-M and all-N.  Thus by RT4 we can use
all-M-necc and all-N-necc to think as if we are given the formulas (M
x) and (N x) as theorems.  The conclusion here is also a universal
quantification, namely we have to prove all-MN.  Then RT3 tells us to
proceed as follows.  Take any object y.  Try to find an instantiation z
of the hypothesis that implies (and (M y) (N y)).  Then instantiate y
with all-MN-witness.  Note that the hypothesis lets us assume (M x) and
(N x) to be theorems.  Thus to justify we need to instantiate x with y,
and in this case, therefore, with all-MN-witness.  To make the long
story short, the following event goes through with ACL2:

     (defthm lf1
        (implies (and (all-M) (all-N))
                 (all-MN))
         :rule-classes nil
         :hints (("Goal"
                   :use ((:instance (:definition all-MN))
                         (:instance all-M-necc (x (all-MN-witness)))
                         (:instance all-N-necc (x (all-MN-witness)))))))

This suggests the following rule of thumb which is a dual of RT6:

     RT7: If a conjecture assumes some universally quantified predicate
     in the hypothesis and its conclusion asserts a universallly
     quantified predicate, then instantiate the "necessary condition"
     (forall-mn-necc) of the hypothesis with the witness of the
     conclusion to prove the conjecture.

Applying RT7 now we can easily prove the other theorems that we need to
show that universal quantification distributes over conjunction.  Let
us just go through this motion in ACL2.

     (defthm lf2
       (implies (all-MN)
                (all-M))
       :rule-classes nil
       :hints (("Goal"
                 :use ((:instance (:definition all-M))
                       (:instance all-MN-necc
                                  (x (all-M-witness)))))))

     (defthm lf3
       (implies (all-MN)
                (all-N))
       :rule-classes nil
       :hints (("Goal"
                 :use ((:instance (:definition all-N))
                       (:instance all-MN-necc
                                  (x (all-N-witness)))))))

     (defthmd |all conjunction|
       (iff (all-MN)
            (and (all-M) (all-N)))
      :hints (("Goal" :use ((:instance lf1)
                            (:instance lf2)
                            (:instance lf3)))))

The rules of thumb for universal and existential quantification should
make you realize the duality of their use.  Every reasoning method
about universal quantification can be cast as a way of reasoning about
existential quantification, and vice versa.  Whether you reason using
universal and existential quantifiers depends on what is natural in a
particular context.  But just for the sake of completeness let us prove
the duality of universal and existential quantifiers.  So what we want
to prove is the following:

     3.  (forall x (not (M x))) = (not (exists x (M x)))

We first formalize the notion of (forall x (not (M x))) as a
quantification.

     (defun-sk none-M () (forall x (not (M x))))
     (in-theory (disable none-M none-M-necc))

So we now want to prove: (equal (none-M) (not (some-M))).

As before, we should prove this as a pair of implications.  So let us
prove first: (implies (none-M) (not (some-M))).

This may seem to assert an existential quantification in the
conclusion, but rather, it asserts the _negation_ of an existential
quantification.  We are now trying to prove that something does not
exist.  How do we do that?  We can show that nothing satisfies M by
just showing that (some-M-witness) does not satisfy M.  This suggests
the following rule of thumb:

     RT8: When you encounter the negation of an existential
     quantification think in terms of a universal quantification, and
     vice-versa.

Ok, so now applying RT8 and RT3 you should be trying to apply the
definition of some-M.  The hypothesis is just a pure (non-negated)
universal quantification so you should apply RT4.  A blind application
lets us prove the theorem as below.

     (defthm nl1
       (implies (none-M) (not (some-M)))
       :rule-classes nil
       :hints (("Goal"
                 :use ((:instance (:definition some-M))
                       (:instance none-M-necc (x (some-M-witness)))))))

How about the converse implication?  I have deliberately written it as
(implies (not (none-M)) (some-M)) instead of switching the left-hand and
right-hand sides of nl1, which would have been equivalent.  Again, RH8
tells us how to reason about it, in this case using RH2, and we succeed.

     (defthm nl2
       (implies (not (none-M)) (some-M))
       :rule-classes nil
       :hints (("Goal"
                 :use ((:instance (:definition none-M))
                       (:instance some-M-suff (x (none-M-witness)))))))

So finally we just go through the motions of proving the equality.

     (defthmd |forall not = not exists|
       (equal (none-M) (not (some-M)))
       :hints (("Goal"
                 :use ((:instance nl1)
                       (:instance nl2)))))

Let us now see if we can prove a slightly more advanced theorem which
can be stated informally as: If there is a natural number x which
satisfies M, then there is a least natural number y that satisfies M.

[Note: Any time I have had to reason about existential quantification I
have had to do this particular style of reasoning and state that if
there is an object satisfying a predicate, then there is also a
"minimal" object satisfying the predicate.]

Let us formalize this concept.  We first define the concept of
existence of a natural number satisfying x.

     (defun-sk some-nat-M () (exists x (and (natp x) (M x))))
     (in-theory (disable some-nat-M some-nat-M-suff))

We now talk about what it means to say that x is the least number
satisfying M.

     (defun-sk none-below (y)
       (forall r (implies (and (natp r) (< r y)) (not (M r))))))
     (in-theory (disable none-below none-below-necc))

     (defun-sk min-M () (exists y (and (M y) (natp y) (none-below y))))
     (in-theory (disable min-M min-M-suff))

The predicate none-below says that no natural number less than y
satisfies M.  The predicate min-M says that there is some natural
number y satisfying M such that none-below holds for y.

So the formula we want to prove is: (implies (some-nat-M) (min-M)).

Since the formula requires that we prove an existential quantification,
RT1 tells us to construct some object satisfying the predicate over
which we are quantifying.  We should then be able to instantiate
min-M-suff with this object.  That predicate says that the object must
be the least natural number that satisfies M.  Since such an object is
uniquely computable if we know that there exists some natural number
satisfying M, let us just write a recursive function to compute it.
This function is least-M below.

     (defun least-M-aux (i bound)
       (declare (xargs :measure (nfix (- (1+ bound) i))))
       (cond ((or (not (natp i))
                  (not (natp bound))
                  (> i bound))
              0)
            ((M i) i)
            (t (least-M-aux (+ i 1) bound))))

     (defun least-M (bound) (least-M-aux 0 bound))

Let us now reason about this function as one does typically.  So we
prove that this object is indeed the least natural number that
satisfies M, assuming that bound is a natural number that satisfies M.

     (defthm least-aux-produces-an-M
       (implies (and (natp i)
                     (natp bound)
                     (<= i bound)
                     (M bound))
                (M (least-M-aux i bound))))

     (defthm least-<=bound
       (implies (<= 0 bound)
                (<= (least-M-aux i bound) bound)))

     (defthm least-aux-produces-least
       (implies (and (natp i)
                     (natp j)
                     (natp bound)
                     (<= i j)
                     (<= j bound)
                     (M j))
                 (<= (least-M-aux i bound) j)))

     (defthm least-aux-produces-natp
       (natp (least-M-aux i bound)))

     (defthmd least-is-minimal-satisfying-m
       (implies (and (natp bound)
                     (natp i)
                      (< i (least-M bound)))
                (not (M i)))
       :hints (("Goal"
                 :in-theory (disable least-aux-produces-least least-<=bound)
                 :use ((:instance least-<=bound
                                  (i 0))
                       (:instance least-aux-produces-least
                                  (i 0)
                                  (j i))))))

     (defthm least-has-m
       (implies (and (natp bound)
                     (m bound))
                (M (least-M bound))))

     (defthm least-is-natp
       (natp (least-M bound)))

So we have done that, and hopefully this is all that we need about
least-M.  So we disable everything.

     (in-theory (disable least-M natp))

Now of course we note that the statement of the conjecture we are
interested in has two quantifiers, an inner forall (from none-below)
and an outer exists (from min-M).  Since ACL2 is not very good with
quantification, we hold its hands to reason with the quantifier part.
So we will first prove something about the forall and then use it to
prove what we need about the exists.

     RT9: When you face nested quantifiers, reason about each nesting
     separately.

So what do we want to prove about the inner quantifier?  Looking
carefully at the definition of none-below we see that it is saying that
for all natural numbers r < y, (M r) does not hold.  Well, how would we
want to use this fact when we want to prove our final theorem?  We
expect that we will instantiate min-M-suff with the object (least-M
bound) where we know (via the outermost existential quantifier) that M
holds for bound, and we will then want to show that none-below holds for
(least-M bound).  So let us prove that for any natural number (call it
bound), none-below holds for (least-M bound).  For the final theorem we
only need it for natural numbers satisfying M, but note that from the
lemma least-is-minimal-satisfying-m we really do not need that bound
satisfies M.

So we are now proving: (implies (natp bound) (none-below (least-M
bound))).

Well since this is a standard case of proving a universally quantified
predicate, we just apply RT3.  We have proved that for all naturals i <
(least-M bound), i does not satisfy M (lemma
least-is-minimal-satisfying-M), so we merely need the instantiation of
that lemma with none-below-witness of the thing we are trying to prove,
that is, (least-M bound).  The theorem below thus goes through.

     (defthm least-is-minimal
       (implies (natp bound)
                (none-below (least-M bound)))
       :hints (("Goal"
                 :use ((:instance (:definition none-below)
                                  (y (least-M bound)))
                       (:instance least-is-minimal-satisfying-m
                                  (i (none-below-witness (least-M bound))))))))

Finally we are in the outermost existential quantifier, and are in the
process of applying min-M-suff.  What object should we instantiate it
with?  We must instantiate it with (least-M bound) where bound is an
object which must satisfy M and is a natural.  We have such an object,
namely (some-nat-M-witness) which we know have all these qualities given
the hypothesis.  So the proof now is just RT1 and RT2.

     (defthm |minimal exists|
       (implies (some-nat-M) (min-M))
       :hints (("Goal"
                 :use ((:instance min-M-suff
                                  (y (least-M (some-nat-M-witness))))
                       (:instance (:definition some-nat-M))))))

If you are comfortable with the reasoning above, then you are
comfortable with quantifiers and probably will not need these notes any
more.  In my opinion, the best way of dealing with ACL2 is to ask
yourself why you think something is a theorem, and the rules of thumb
above are simply guides to the questions that you need to ask when you
are dealing with quantification.

Here are a couple of simple exercises for you to test if you understand
the reasoning process.

*Exercise 1*.  Formalize and prove the following theorem.  Suppose there
exists x such that (R x) and suppose that all x satisfy (P x).  Then
prove that there exists x such that (P x) & (R x).  (See
`http://www.cs.utexas.edu/users/moore/acl2/contrib/quantifier-exercise-1-solution.html'
for a solution.)

*Exercise 2*.  Recall the example just before the preceding exercise,
where we showed that if there exists a natural number x satisfying M
then there is another natural number y such that y satisfies M and for
every natural number z < y, z does not.  What would happen if we remove
the restriction of x, y, and z being naturals?  Of course, we will not
talk about < any more, but suppose you use the total order on all ACL2
objects (from "books/misc/total-order").  More concretely, consider the
definition of some-M above.  Let us now define two other functions:

     (include-book "misc/total-order" :dir :system)

     (defun-sk none-below-2 (y)
       (forall r (implies (<< r y) (not (M r)))))

     (defun-sk min-M2 () (exists y (and (M y) (none-below-2 y))))

The question is whether (implies (some-M) (min-M2)) is a theorem.  Can
you prove it?  Can you disprove it?

QUANTIFIERS    issues about quantification in ACL2

ACL2 supports first-order quantifiers exists and forall by way of the
defun-sk event.  However, proof support for quantification is quite
limited.  Therefore, you may prefer using recursion in place of defun-sk
when possible (following common ACL2 practice).

For example, the notion "every member of x has property p" can be
defined either with recursion or explicit quantification, but proofs
may be simpler when recursion is used.  We illustrate this point with
two proofs of the same informal claim, one of which uses recursion
which the other uses explicit quantification.  Notice that with
recursion, the proof goes through fully automatically; but this is far
from true with explicit quantification (especially notable is the ugly
hint).

The informal claim for our examples is:  If every member a of each of
two lists satisfies the predicate (p a), then this holds of their
append; and, conversely.

See QUANTIFIERS-USING-RECURSION for a solution to this example
using recursion.

See QUANTIFIERS-USING-DEFUN-SK for a solution to this example
using defun-sk.  Also See QUANTIFIERS-USING-DEFUN-SK-EXTENDED
for an elaboration on that solution.

But perhaps first, see DEFUN-SK for an ACL2 utility to
introduce first-order quantification in a direct way.  Examples of the
use of defun-sk are also available: see DEFUN-SK-EXAMPLE and
see TUTORIAL4-DEFUN-SK-EXAMPLE for basic examples, and see
QUANTIFIER-TUTORIAL for a more complete, careful beginner's
introduction that takes you through typical kinds of quantifier-based
reasoning in ACL2.

QUANTIFIERS-USING-DEFUN-SK    quantification example

See QUANTIFIERS for the context of this example.  It should be
compared to a corresponding example in which a simpler proof is
attained by using recursion in place of explicit quantification; see
QUANTIFIERS-USING-RECURSION.

     (in-package "ACL2")

     ; We prove that if every member A of each of two lists satisfies the
     ; predicate (P A), then this holds of their append; and, conversely.

     ; Here is a solution using explicit quantification.

     (defstub p (x) t)

     (defun-sk forall-p (x)
       (forall a (implies (member a x)
                          (p a))))

     (defthm member-append
       (iff (member a (append x1 x2))
            (or (member a x1) (member a x2))))

     (defthm forall-p-append
       (equal (forall-p (append x1 x2))
              (and (forall-p x1) (forall-p x2)))
       :hints (("Goal" ; ``should'' disable forall-p-necc, but no need
                :use
                ((:instance forall-p-necc
                            (x (append x1 x2))
                            (a (forall-p-witness x1)))
                 (:instance forall-p-necc
                            (x (append x1 x2))
                            (a (forall-p-witness x2)))
                 (:instance forall-p-necc
                            (x x1)
                            (a (forall-p-witness (append x1 x2))))
                 (:instance forall-p-necc
                            (x x2)
                            (a (forall-p-witness (append x1 x2))))))))

Also see QUANTIFIERS-USING-DEFUN-SK-EXTENDED for an elaboration
on this example.

QUANTIFIERS-USING-DEFUN-SK-EXTENDED    quantification example with details

See QUANTIFIERS-USING-DEFUN-SK for the context of this example.

     (in-package "ACL2")

     ; We prove that if every member A of each of two lists satisfies the
     ; predicate (P A), then this holds of their append; and, conversely.

     ; Here is a solution using explicit quantification.

     (defstub p (x) t)

     (defun-sk forall-p (x)
       (forall a (implies (member a x)
                          (p a))))

     ; The defun-sk above introduces the following axioms.  The idea is that
     ; (FORALL-P-WITNESS X) picks a counterexample to (forall-p x) if there is one.

     #|
     (DEFUN FORALL-P (X)
       (LET ((A (FORALL-P-WITNESS X)))
            (IMPLIES (MEMBER A X) (P A))))

     (DEFTHM FORALL-P-NECC
       (IMPLIES (NOT (IMPLIES (MEMBER A X) (P A)))
                (NOT (FORALL-P X)))
       :HINTS (("Goal" :USE FORALL-P-WITNESS)))
     |#

     ; The following lemma seems critical.

     (defthm member-append
       (iff (member a (append x1 x2))
            (or (member a x1) (member a x2))))

     ; The proof of forall-p-append seems to go out to lunch, so we break into
     ; directions as shown below.

     (defthm forall-p-append-forward
       (implies (forall-p (append x1 x2))
                (and (forall-p x1) (forall-p x2)))
       :hints (("Goal" ; ``should'' disable forall-p-necc, but no need
                :use
                ((:instance forall-p-necc
                            (x (append x1 x2))
                            (a (forall-p-witness x1)))
                 (:instance forall-p-necc
                            (x (append x1 x2))
                            (a (forall-p-witness x2)))))))

     (defthm forall-p-append-reverse
       (implies (and (forall-p x1) (forall-p x2))
                (forall-p (append x1 x2)))
       :hints (("Goal"
                :use
                ((:instance forall-p-necc
                            (x x1)
                            (a (forall-p-witness (append x1 x2))))
                 (:instance forall-p-necc
                            (x x2)
                            (a (forall-p-witness (append x1 x2))))))))

     (defthm forall-p-append
       (equal (forall-p (append x1 x2))
              (and (forall-p x1) (forall-p x2)))
       :hints (("Goal" :use (forall-p-append-forward
                             forall-p-append-reverse))))

QUANTIFIERS-USING-RECURSION    recursion for implementing quantification

The following example illustrates the use of recursion as a means of
avoiding proof difficulties that can arise from the use of explicit
quantification (via defun-sk).  See QUANTIFIERS for more about
the context of this example.

     (in-package "ACL2")

     ; We prove that if every member A of each of two lists satisfies the
     ; predicate (P A), then this holds of their append; and, conversely.

     ; Here is a solution using recursively-defined functions.

     (defstub p (x) t)

     (defun all-p (x)
       (if (atom x)
           t
         (and (p (car x))
              (all-p (cdr x)))))

     (defthm all-p-append
       (equal (all-p (append x1 x2))
              (and (all-p x1) (all-p x2))))

DEFUND    define a function symbol and then disable it

Use defund instead of defun when you want to disable a function
immediately after its definition.  This macro has been provided for
users who prefer working in a mode where functions are only enabled
when explicitly directed by :in-theory.  Specifically, the form

     (defund NAME FORMALS ...)

expands to:

     (progn
       (defun NAME FORMALS ...)
       (with-output
        :off summary
        (in-theory (disable NAME)))
       (value NAME)).

Only the :definition rule (and, for recursively defined functions, the
:induction rule) for the function are disabled, and the summary for the
in-theory event is suppressed.

Note that defund commands are never redundant (see
REDUNDANT-EVENTS).  If the function has already been defined, then
the in-theory event will still be executed.

See DEFUN for documentation of defun.

ENCAPSULATE    constrain some functions and/or hide some events

The following example illustrates the idea of encapsulate.

     (encapsulate

     ; Introduce a function foo of one argument that returns one value:
      ( ((foo *) => *) )

     ; Introduce a ``witness'' (example) for foo, marked as local so that
     ; it is not exported:
      (local (defun foo (x) x))

     ; Introduce a non-local property to be exported:
      (defthm foo-preserves-consp
        (implies (consp x)
                 (consp (foo x))))
     )

The form above introduces a new function symbol, foo, with the indicated
property and no definition.  In fact, the output from ACL2 concludes as
follows.

     The following constraint is associated with the function FOO:

     (IMPLIES (CONSP X) (CONSP (FOO X)))

We turn now to more complete documentation.

     Other Examples:
     (encapsulate (((an-element *) => *))

     ; The list of signatures above could also be written
     ;            ((an-element (lst) t))

       (local (defun an-element (lst)
                (if (consp lst) (car lst) nil)))
       (local (defthm member-equal-car
                 (implies (and lst (true-listp lst))
                          (member-equal (car lst) lst))))
       (defthm thm1
          (implies (null lst) (null (an-element lst))))
       (defthm thm2
          (implies (and (true-listp lst)
                        (not (null lst)))
                   (member-equal (an-element lst) lst))))

     (encapsulate
      () ; empty signature: no constrained functions indicated

      (local (defthm hack
               (implies (and (syntaxp (quotep x))
                             (syntaxp (quotep y)))
                        (equal (+ x y z)
                               (+ (+ x y) z)))))

      (defthm nthcdr-add1-conditional
        (implies (not (zp (1+ n)))
                 (equal (nthcdr (1+ n) x)
                        (nthcdr n (cdr x))))))

     General Form:
     (encapsulate (signature ... signature)
       ev1
       ...
       evn)

where each signature is a well-formed signature (see
SIGNATURE), each signature describes a different function symbol, and
each evi is an embedded event form (See EMBEDDED-EVENT-FORM).
There must be at least one evi.  The evi inside local special forms are
called "local" events below.  Events that are not local are sometimes
said to be "exported" by the encapsulation.  We make the further
restriction that no defaxiom event may be introduced in the scope of an
encapsulate (not even by encapsulate or include-book events that are
among the evi).  Furthermore, no non-local include-book event is
permitted in the scope of any encapsulate with a non-empty list of
signatures.

To be well-formed, an encapsulate event must have the properties that
each event in the body (including the local ones) can be successfully
executed in sequence and that in the resulting theory, each function
mentioned among the signatures was introduced via a local event and has
the signature listed.  (A utility is provided to assist in debugging
failures of such execution; see REDO-FLAT.)  In addition, the
body may contain no "local incompatibilities" which, roughly stated,
means that the events that are not local must not syntactically require
symbols defined by local events, except for the functions listed in the
signatures.  See LOCAL-INCOMPATIBILITY.  Finally, no non-local
recursive definition in the body may involve in its suggested induction
scheme any function symbol listed among the signatures.  See
SUBVERSIVE-RECURSIONS.

The result of an encapsulate event is an extension of the logic in
which, roughly speaking, the functions listed in the signatures are
constrained to have the signatures listed and to satisfy the non-local
theorems proved about them.  In fact, other functions introduced in the
encapsulate event may be considered to have "constraints" as well.
(See CONSTRAINT for details, which are only relevant to
functional instantiation.)  Since the constraints were all theorems in
the "ephemeral" or "local" theory, we are assured that the extension
produced by encapsulate is sound.  In essence, the local definitions of
the constrained functions are just "witness functions" that establish
the consistency of the constraints.  Because those definitions are
local, they are not present in the theory produced by encapsulation.
Encapsulate also exports all rules generated by its non-local events,
but rules generated by local events are not exported.

The default-defun-mode for the first event in an encapsulation is the
default defun-mode "outside" the encapsulation.  But since events
changing the defun-mode are permitted within the body of an
encapsulate, the default defun-mode may be changed.  However,
defun-mode changes occurring within the body of the encapsulate are not
exported.  In particular, the acl2-defaults-table after an encapsulate
is always the same as it was before the encapsulate, even though the
encapsulate body might contain defun-mode changing events, :program and
:logic.  See DEFUN-MODE.  More generally, after execution of an
encapsulate event, the value of acl2-defaults-table is restored to what
it was immediately before that event was executed.  See
ACL2-DEFAULTS-TABLE.

Theorems about the constrained function symbols may then be proved --
theorems whose proofs necessarily employ only the constraints.  Thus,
those theorems may be later functionally instantiated, as with the
:functional-instance lemma instance (see LEMMA-INSTANCE), to
derive analogous theorems about different functions, provided the
constraints (see CONSTRAINT) can be proved about the new
functions.

We make some remarks on guards and evaluation.  Calls of functions
introduced in the signatures list cannot be evaluated in the ACL2
read-eval-print loop.  See DEFATTACH for a way to overcome this
limitation.  Moreover, any :guard supplied in the signature is
automatically associated in the world with its corresponding function
symbol, with no requirement other than that the guard is a legal term
all of whose function symbols are in :logic mode with their guards
verified.  In particular, there need not be any relationship between a
guard in a signature and the guard in a local witness function.
Finally, note that for functions introduced non-locally inside an
encapsulate event, guard verification is illegal unless ACL2 determines
that the proof obligations hold outside the encapsulate event as well.

     (encapsulate
      ((f (x) t))
      (local (defun f (x) (declare (xargs :guard t)) (consp x)))
      ;; ERROR!
      (defun g (x)
        (declare (xargs :guard (f x)))
        (car x)))

Observe that if the signatures list is empty, encapsulate may still be
useful for deriving theorems to be exported whose proofs require lemmas
you prefer to hide (i.e., made local).

The order of the events in the vicinity of an encapsulate is confusing.
We discuss it in some detail here because when logical names are being
used with theory functions to compute sets of rules, it is sometimes
important to know the order in which events were executed.  (See
LOGICAL-NAME and see THEORY-FUNCTIONS.)  What, for example,
is the set of function names extant in the middle of an encapsulation?

If the most recent event is previous and then you execute an
encapsulate constraining an-element with two non-local events in its
body, thm1 and thm2, then the order of the events after the
encapsulation is (reading chronologically forward): previous, thm1,
thm2, an-element (the encapsulate itself).  Actually, between previous
and thm1 certain extensions were made to the world by the superior
encapsulate, to permit an-element to be used as a function symbol in
thm1.

Finally, we note that an encapsulate event is redundant if and only if
a syntactically identical encapsulate has already been executed under
the same default-defun-mode, default-ruler-extenders, and
default-verify-guards-eagerness.  See REDUNDANT-EVENTS.

EVISC-TABLE    support for abbreviated output

The evisc-table is an ACL2 table (see TABLE) whose purpose is
to modify the print representations of specified non-nil objects.  When
a key (some object) is associated with a string value, then that string
is printed instead of that key (as an abbreviation).  For example, the
following log shows how to abbreviate the key (a b c) with the token
<my-abc-list>.

     ACL2 !>(table evisc-table '(a b c) "<my-abc-list>")

     Summary
     Form:  ( TABLE EVISC-TABLE ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      EVISC-TABLE
     ACL2 !>'(a b c)
     <my-abc-list>
     ACL2 !>'(4 5 a b c)
     (4 5 . <my-abc-list>)
     ACL2 !>

Every value in this table must be either a string or nil, where nil
eliminates any association of the key with an abbreviation.  Continuing
with the log above:

     ACL2 !>(table evisc-table '(a b c) nil)

     Summary
     Form:  ( TABLE EVISC-TABLE ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      EVISC-TABLE
     ACL2 !>'(a b c)
     (A B C)
     ACL2 !>'(4 5 a b c)
     (4 5 A B C)
     ACL2 !>

It can be particularly helpful to use this table to abbreviate a
constant introduced by defconst by prefixing the constant name with
"#,", as we now describe.  Consider first the following example.

     (defconst *abc* '(1 2 3 4 5 6 7 8))
     (table evisc-table *abc*
       (concatenate 'string "#," (symbol-name '*abc*)))

Then the constant *abc* is printed as follows -- very helpful if its
associated structure is significantly larger than the 8-element list of
numbers shown above!

     ACL2 !>*abc*
     #,*ABC*
     ACL2 !>

What's more, the ACL2 reader will replace #,*C*, where *C* is defined by
defconst, by its value, regardless of evisc-table; see
SHARP-DOT-READER.  Continuing with the example above, we have:

     ACL2 !>(cdr (quote #,*ABC*))
     (2 3 4 5 6 7 8)
     ACL2 !>

Of course, more care needs to be taken if packages are involved (see
DEFPKG), as we now illustrate.

     ACL2 !>(defpkg "FOO" nil)

     Summary
     Form:  ( DEFPKG "FOO" ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      "FOO"
     ACL2 !>(defconst foo::*a* '(1 2 3))

     Summary
     Form:  ( DEFCONST FOO::*A* ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      FOO::*A*
     ACL2 !>(table evisc-table foo::*a* "#,foo::*a*")

     Summary
     Form:  ( TABLE EVISC-TABLE ...)
     Rules: NIL
     Warnings:  None
     Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
      EVISC-TABLE
     ACL2 !>foo::*a*
     #,foo::*a*
     ACL2 !>'#,foo::*a*
     #,foo::*a*
     ACL2 !>(cdr '#,foo::*a*)
     (2 3)
     ACL2 !>

We conclude by an example showing some extra care that may be important
to consider taking.  We start with:

     (defconst |*BaR*| '(3 4))

Then the following works just fine; but try it without the extra code
for the may-need-slashes case and you'll see that the sharp-dot
printing is missing.  First:

     (table evisc-table
            |*BaR*|
            (let ((x (symbol-name '|*BaR*|)))
              (if (may-need-slashes x)
                  (concatenate 'string "#.|" x "|")
                (concatenate 'string "#." x))))

Then:

     ACL2 !>|*BaR*|
     #,|*BaR*|
     ACL2 !>

IN-ARITHMETIC-THEORY    designate "current" theory for some rewriting done in linear arithmetic

     Example:
     (in-arithmetic-theory '(lemma1 lemma2))

     General Form:
     (in-arithmetic-theory term :doc doc-string)

where term is a term that when evaluated will produce a theory (see
THEORIES), and doc-string is an optional documentation string
not beginning with ":doc-section ...".  Except for the variable world,
term must contain no free variables.  Term is evaluated with the
variable world bound to the current world to obtain a theory and the
corresponding runic theory (see THEORIES) is then made the
current theory.  Thus, immediately after the in-arithmetic-theory, a
rule is enabled iff its rule name is a member of the runic
interpretation (see THEORIES) of some member of the value of
term.

Warning:  If term involves macros such as ENABLE and DISABLE you will
probably not get what you expect!  Those macros are defined relative to
the CURRENT-THEORY.  But in this context you might wish they were
defined in terms of the "CURRENT-ARITHMETIC-THEORY" which is not
actually a defined function.  We do not anticipate that users will
repeatedly modify the arithmetic theory.  We expect term most often to
be a constant list of runes and so have not provided "arithmetic theory
manipulation functions" analogous to CURRENT-THEORY and ENABLE.

BECAUSE NO UNIQUE name is associated with an in-arithmetic-theory event,
there is no way we can store the documentation string doc-string in our
il[documentation] data base.  Hence, we actually prohibit doc-string
from having the form of an ACL2 documentation string; see
DOC-STRING.

See NON-LINEAR-ARITHMETIC.

IN-THEORY    designate "current" theory (enabling its rules)

     Example:
     (in-theory (set-difference-theories
                  (universal-theory :here)
                  '(flatten (:executable-counterpart flatten))))

     General Form:
     (in-theory term :doc doc-string)

where term is a term that when evaluated will produce a theory (see
THEORIES), and doc-string is an optional documentation string
not beginning with ":doc-section ...".  Except for the variable world,
term must contain no free variables.  Term is evaluated with the
variable world bound to the current world to obtain a theory and the
corresponding runic theory (see THEORIES) is then made the
current theory.  Thus, immediately after the in-theory, a rule is
enabled iff its rule name is a member of the runic interpretation (see
THEORIES) of some member of the value of term.  See
THEORY-FUNCTIONS for a list of the commonly used theory manipulation
functions.

Because no unique name is associated with an in-theory event, there is
no way we can store the documentation string doc-string in our
documentation data base.  Hence, we actually prohibit doc-string from
having the form of an ACL2 documentation string; see DOC-STRING.

Note that it is often useful to surround in-theory events with local,
that is, to use (local (in-theory ...)).  This use of local in
encapsulate events and books will prevent the effect of this theory
change from being exported outside the context of that encapsulate or
book.

Also see HINTS for a discussion of the :in-theory hint,
including some explanation of the important point that an :in-theory
hint will always be evaluated relative to the current ACL2 logical
world, not relative to the theory of a previous goal.

INCLUDE-BOOK    load the events in a file

     Examples:
     (include-book "my-arith")
     (include-book "/home/smith/my-arith")
     (include-book "/../../my-arith")

     General Form:
     (include-book file :load-compiled-file action
                        :uncertified-okp t/nil      ; [default t]
                        :defaxioms-okp t/nil        ; [default t]
                        :skip-proofs-okp t/nil      ; [default t]
                        :ttags ttags                ; [default nil]
                        :dir directory
                        :doc doc-string)

where file is a book name.  See BOOKS for general information,
see BOOK-NAME for information about book names, and see
PATHNAME for information about file names.  Action is one of t, nil,
:default, :warn, or :comp; these values are explained below, and the
default is :default.  The three -okp keyword arguments, which default
to t, determine whether errors or warnings are generated under certain
conditions explained below; when the argument is t, warnings are
generated.  The dir argument, if supplied, is a keyword that represents
an absolute pathname for a directory (see PATHNAME), to be used
instead of the current book directory (see CBD) for resolving
the given file argument to an absolute pathname.  In particular, by
default :dir :system resolves file using the distributed books/
directory of your ACL2 installation, unless your ACL2 executable was
built somewhere other than where it currently resides; please see the
"Distributed Books Directory" below.  To define other keywords that can
be used for dir, see ADD-INCLUDE-BOOK-DIR.  Doc-string is an
optional documentation string; see DOC-STRING.  If the book has
no certificate, if its certificate is invalid or if the certificate was
produced by a different version of ACL2, a warning is printed and the
book is included anyway; see CERTIFICATE.  This can lead to
serious errors; see UNCERTIFIED-BOOKS.  If the portcullis of
the certificate (see PORTCULLIS) cannot be raised in the host
logical world, an error is caused and no change occurs to the logic.
Otherwise, the non-local events in file are assumed.  Then the keep of
the certificate is checked to ensure that the correct files were read;
see KEEP.  A warning is printed if uncertified books were
included.  Even if no warning is printed, include-book places a burden
on you; see CERTIFICATE.

If you use guards, please note include-book is executed as though
(set-guard-checking nil) has been evaluated; see
SET-GUARD-CHECKING.  If you want guards checked, please see
LD and/or see REBUILD.

The value, action, of :load-compiled-file controls whether a compiled
file is loaded by include-book.  If compilation has been suppressed by
(set-compiler-enabled nil), then action is coerced to nil; see
COMPILATION.  Otherwise, if action is missing or its value is the
keyword :default, then it is treated as :warn.  If action is nil, no
attempt is made to load the compiled file for the book provided.  In
order to load the compiled file, it must be more recent than the book's
certificate (except in raw mode, where it must be more recent than the
book itself; see SET-RAW-MODE).  For non-nil values of action
that do not result in a loaded compiled file, ACL2 proceeds as follows.
Note that a load of a compiled file or expansion file aborts partway
through whenever an include-book form is encountered for which no
suitable compiled or expansion file can be loaded.  For much more
detail, see BOOK-COMPILED-FILE.

     t: Cause an error if the compiled file is not loaded.  This same
     requirement is imposed on every include-book form evaluated during
     the course of evaluation of the present include-book form, except
     that for those subsidiary include-books that do not themselves
     specify :load-compiled-file t, it suffices to load the expansion
     file (see BOOK-COMPILED-FILE).

     :warn: An attempt is made to load the compiled file, and a warning
     is printed if that load takes place and runs to completion.

     :comp: A compiled file is loaded as with value t, except that if a
     suitable "expansion file" exists, the compiled file is first
     created.  See BOOK-COMPILED-FILE.

The three -okp arguments, :uncertified-okp, defaxioms-okp, and
skip-proofs-okp, determine the system's behavior when the book or any
subbook is found to be uncertified, when the book or any subbook is
found to contain defaxiom events, and when the book or any subbook is
found to contain skip-proofs events, respectively.  All three default
to t, which means it is "ok" for the condition to arise.  In this case,
a warning is printed but the processing to load the book is allowed to
proceed.  When one of these arguments is nil and the corresponding
condition arises, an error is signaled and processing is aborted.
*Exception*: :uncertified-okp is ignored if the include-book is being
performed on behalf of a certify-book.

The keyword argument :ttags may normally be omitted.  A few constructs,
used for example if you are building your own system based on ACL2, may
require it.  See DEFTTAG for an explanation of this argument.

Include-book is similar in spirit to encapsulate in that it is a single
event that "contains" other events, in this case the events listed in
the file named.  Include-book processes the non-local event forms in
the file, assuming that each is admissible.  Local events in the file
are ignored.  You may use include-book to load several books, creating
the logical world that contains the definitions and theorems of all of
them.

If any non-local event of the book attempts to define a name that has
already been defined -- and the book's definition is not syntactically
identical to the existing definition -- the attempt to include the book
fails, an error message is printed, and no change to the logical world
occurs.  See REDUNDANT-EVENTS for the details.

When a book is included, the default defun-mode (see
DEFAULT-DEFUN-MODE) for the first event is always :logic.  That is,
the default defun-mode "outside" the book -- in the environment in
which include-book was called -- is irrelevant to the book.  Events
that change the defun-mode are permitted within a book (provided they
are not in local forms).  However, such changes within a book are not
exported, i.e., at the conclusion of an include-book, the "outside"
default defun-mode is always the same as it was before the include-book.

Unlike every other event in ACL2, include-book puts a burden on you.
Used improperly, include-book can be unsound in the sense that it can
create an inconsistent extension of a consistent logical world.  A
certification mechanism is available to help you carry this burden --
but it must be understood up front that even certification is no
guarantee against inconsistency here.  The fundamental problem is one
of file system security.  See CERTIFICATE for a discussion of
the security issues.

After execution of an include-book form, the value of
acl2-defaults-table is restored to what it was immediately before that
include-book form was executed.  See ACL2-DEFAULTS-TABLE.

Distributed Books Directory.  We refer to the "books directory" of an
executable image as the full pathname string of the books directory
associated with :dir :system for that image.  This is where the
distributed books directory should reside.  By default, it is the books/
subdirectory of the directory where the sources reside and the
executable image is thus built (except for ACL2(r) -- see REAL
--, where it is books/nonstd/).  If those books reside elsewhere, the
environment variable ACL2_SYSTEM_BOOKS can be set to the books/
directory under which they reside (a Unix-style pathname, typically
ending in books/ or books, is permissible).  In most cases, your ACL2
executable is a small script in which you can set this environment
variable just above the line on which the actual ACL2 image is invoked,
for example:

     export ACL2_SYSTEM_BOOKS
     ACL2_SYSTEM_BOOKS=/home/acl2/4-0/acl2-sources/books

This concludes the guided tour through books.  See
SET-COMPILE-FNS for a subtle point about the interaction between
include-book and on-the-fly compilation.  See CERTIFY-BOOK for
a discussion of how to certify a book.

:cited-by Programming

LOCAL    hiding an event in an encapsulation or book

     Examples:
     (local (defthm hack1
              (implies (and (acl2-numberp x)
                            (acl2-numberp y)
                            (equal (* x y) 1))
                       (equal y (/ x)))))

     (local (defun double-naturals-induction (a b)
              (cond ((and (integerp a) (integerp b) (< 0 a) (< 0 b))
                     (double-naturals-induction (1- a) (1- b)))
                    (t (list a b)))))

     General Form:
     (local ev)

where ev is an event form.  If the current default defun-mode (see
DEFAULT-DEFUN-MODE) is :logic and ld-skip-proofsp is nil or t,
then (local ev) is equivalent to ev.  But if the current default
defun-mode is :program or if ld-skip-proofsp is 'include-book, then
(local ev) is a no-op.  Thus, if such forms are in the event list of an
encapsulate event or in a book, they are processed when the
encapsulation or book is checked for admissibility in :logic mode but
are skipped when extending the host world.  Such events are thus
considered "local" to the verification of the encapsulation or book.
The non-local events are the ones "exported" by the encapsulation or
book.  See ENCAPSULATE for a thorough discussion.  Also see
LOCAL-INCOMPATIBILITY for a discussion of a commonly
encountered problem with such event hiding:  you can't make an event
local if its presence is required to make sense of a non-local one.

Note that events that change the default defun-mode, and in fact any
events that set the acl2-defaults-table, are disallowed inside the
scope of local.  See EMBEDDED-EVENT-FORM.

MAKE-EVENT    evaluate (expand) a given form and then evaluate the result

Make-event is a utility for generating events.  It provides a
capability not offered by Lisp macros (see DEFMACRO), as it
allows access to the ACL2 state and logical world.  In essence, the
expression (make-event form) replaces itself with the result of
evaluating form, say, ev, as though one had submitted ev instead of the
make-event call.  But the evaluation of form may involve state and even
modify state, for example by attempting to admit some definitions and
theorems.  Make-event protects the ACL2 logical world so that it is
restored after form is evaluated, before ev is submitted.

     Examples:

     ; Trivial example: evaluate (quote (defun foo (x) x)) to obtain
     ; (defun foo (x) x), which is then evaluated.
     (make-event (quote (defun foo (x) x)))

     ; Evaluate (generate-form state) to obtain (mv nil val state), and
     ; then evaluate val.  (Generate-form is not specified here, but
     ; imagine for example that it explores the state and then generates
     ; some desired definition or theorem.)
     (make-event (generate-form state))

     ; As above, but make sure that if this form is in a book, then when
     ; we include the book, the evaluation of (generate-form state)
     ; should return the same value as it did when the book was
     ; certified.
     (make-event (generate-form state)
                 :check-expansion t)

     ; As above (where the :check-expansion value can be included or
     ; not), where if there is an error during expansion, then the error
     ; message will explain that expansion was on behalf of the indicated
     ; object, typically specified as the first argument.
     (make-event (generate-form state)
                 :on-behalf-of (generate-form state))

     General Form:
     (make-event form :check-expansion chk :on-behalf-of obj)

where chk is nil (the default), t, or the intended "expansion result"
from the evaluation of form (as explained below); and if supplied, obj
is an arbitrary ACL2 object, used only in reporting errors in
expansion, i.e., in the evaluation of form.

We strongly recommend that you look at books/make-event/Readme.lsp,
which summarizes and suggests browsing of some .lisp files in that
directory, in order to understand make-event, perhaps before continuing
to read this documentation.  For example, eval.lisp contains
definitions of macros must-succeed and must-fail that are useful for
testing and are used in many other books in that directory, especially
eval-tests.lisp.  Other than the examples, the explanations here should
suffice for most users.  If you want explanations of subtler details,
see MAKE-EVENT-DETAILS.

Make-event is related to Lisp macroexpansion in the sense that its
argument is evaluated to obtain an expansion result, which is evaluated
again.  Let us elaborate on each of these notions in turn: "is
evaluated," "expansion result", and "evaluated again."

     "is evaluated" -- The argument can be any expression, which is
     evaluated as would be any expression submitted to ACL2's top level
     loop.  Thus, state and user-defined stobjs may appear in the form
     supplied to make-event.  Henceforth, we will refer to this
     evaluation as "expansion."  Expansion is actually done in a way
     that restores ACL2's built-in state global variables, including
     the logical world, to their pre-expansion values (with a few
     exceptions -- see MAKE-EVENT-DETAILS -- and where we note
     that changes to user-defined state global variables (see
     ASSIGN) are preserved).  So, for example, events might be
     evaluated during expansion, but they will disappear from the
     logical world after expansion returns its result.  Moreover,
     proofs are enabled by default at the start of expansion (see
     LD-SKIP-PROOFSP), because an anticipated use of make-event is to
     call the prover to decide which event to generate, and that would
     presumably be necessary even if proofs had been disabled.

     "expansion result" -- The above expansion may result in an ordinary
     (non-state, non-stobj) value, which we call the "expansion
     result."  Or, expansion may result in a multiple value of the form
     (mv erp val state stobj-1 ... stobj-k), where k may be 0; in fact
     the most common case is probably (mv erp val state).  In that
     case, if erp is not nil, then there is no expansion result, and
     the original make-event evaluates to a soft error.  If however erp
     is nil, then the resulting value is val.  Moreover, val must be an
     embedded event form (see EMBEDDED-EVENT-FORM); otherwise,
     the original make-event evaluates to a soft error.  Note that
     error messages from expansion are printed as described under
     "Error Reporting" below.

     "evaluated again" -- the expansion result is evaluated in place of
     the original make-event.

Note that the result of expansion can be an ordinary event, but it can
instead be another call of make-event, or even of a call of a macro that
expands to a call of make-event.  Or, expansion itself can cause
subsidiary calls of make-event, for example if expansion uses ld to
evaluate some make-event forms.  The state global variable
make-event-debug may be set to a non-nil value in order to see a trace
of the expansion process, where the level shown (as in "3>") indicates
the depth of expansions in progress.

Expansion of a make-event call will yield an event that replaces the
original make-event call.  In particular, if you put a make-event form
in a book, then in essence it is replaced by its expansion result,
created during the proof pass of the certify-book process.  We now
elaborate on this idea of keeping the original expansion.

By default, a make-event call in a certified book is replaced (by a
process hidden from the user, in an :expansion-alist field of the book's
certificate) by the expansion result from evaluation of its first
argument.  Thus, although the book is not textually altered during
certification, one may imagine a "book expansion" corresponding to the
original book in which all of the events for which expansion took place
(during the proof phase of certification) have been replaced by their
expansions.  A subsequent include-book will then include the book
expansion corresponding to the indicated book.  When a book is compiled
during certify-book, it is actually the corresponding book expansion,
stored as a temporary file, that is compiled instead.  That temporary
file is deleted after compilation unless one first evaluates the form
(assign keep-tmp-files t).  Note however that all of the original forms
must still be legal events (see EMBEDDED-EVENT-FORM).  So for
example, if the first event in a book is (local (defmacro my-id (x)
x)), followed by (my-id (make-event ...)), the final "include-book"
pass of certify-book will fail because my-id is not defined when the
my-id call is encountered.

The preceding paragraph begins with "by default" because if you specify
:check-expansion t, then subsequent evaluation of the same make-event
call -- during the second pass of an encapsulate or during event
processing on behalf of include-book -- will do the expansion again and
check that the expansion result equals the original expansion result.
In the unusual case that you know the expected expansion result, res,
you can specify :check-expansion res.  This will will cause a check that
every subsequent expansion result for the make-event form is res,
including the original one.  IMPORTANT NOTE: That expansion check is
only done when processing events, not during a preliminary load of a
book's compiled file.  The following paragraph elaborates.

(Here are details on the point made just above, for those who use the
:check-expansion argument to perform side-effects on the state.  When
you include a book, ACL2 generally loads a compiled file before
processing the events in the book; see BOOK-COMPILED-FILE.
While it is true that a non-nil :check-expansion argument causes
include-book to perform expansion of the make-event form during event
processing it does _not_ perform expansion when the compiled file (or
expansion file; again, see BOOK-COMPILED-FILE) is loaded.)

ACL2 performs the following space-saving optimization for book
certificates: a local event arising from make-event expansion is
replaced in that expansion by (local (value-triple :ELIDED)).

Finally, we note that ACL2 extends the notion of "make-event expansion"
to the case that a call of make-event is found in the course of
macroexpansion.  We illustrate with the following example.

     (encapsulate
      ()
      (defmacro my-mac ()
        '(make-event '(defun foo (x) x)))
      (my-mac))
     :pe :here

The above call of pe shows that the form (my-mac) has a make-event
expansion of (DEFUN FOO (X) X):

     (ENCAPSULATE NIL
                  (DEFMACRO MY-MAC
                            NIL
                            '(MAKE-EVENT '(DEFUN FOO (X) X)))
                  (RECORD-EXPANSION (MY-MAC)
                                    (DEFUN FOO (X) X)))

*Error Reporting.*

Suppose that expansion produces a soft error as described above.  That
is, suppose that the argument of a make-event call evaluates to a
multiple value (mv erp val state ...) where erp is not nil.  If erp is
a string, then that string is printed in the error message.  If erp is
a cons pair whose car is a string, then the error prints "~@0" with #\0
bound to that cons pair; see FMT.  Any other non-nil value of
erp causes a generic error message to be printed.

*Restriction to the Top Level.*

Every form enclosing a make-event call must be an embedded event form
(see EMBEDDED-EVENT-FORM).  This restriction enables ACL2 to
track expansions produced by make-event.  For example:

     ; Legal:
     (progn (with-output
             :on summary
             (make-event '(defun foo (x) x))))

     ; Illegal:
     (mv-let (erp val state)
             (make-event '(defun foo (x) x))
             (mv erp val state))

Low-level remark, for system implementors.  There is the one exception
to this restriction: a single state-global-let* form immediately under a
progn! call.  For example:

     (progn! (state-global-let* <bindings> (make-event ...)))

However, the following form may be preferable (see PROGN!):

     (progn! :state-global-bindings <bindings> (make-event ...))

See REMOVE-UNTOUCHABLE for an interesting use of this exception.

*Examples illustrating how to access state*

You can modify the ACL2 state by doing your state-changing computation
during the expansion phase, before expansion returns the event that is
submitted.  Here are some examples.

First consider the following.  Notice that expansion modifies state
global my-global during make-event expansion, and then expansion
returns a defun event to be evaluated.

     (make-event
       (er-progn (assign my-global (length (w state)))
                 (value '(defun foo (x) (cons x x)))))

Then we get:

       ACL2 !>(@ my-global)
       72271
       ACL2 !>:pe foo
        L        1:x(MAKE-EVENT (ER-PROGN # #))

       >L            (DEFUN FOO (X) (CONS X X))
       ACL2 !>

Here's a slightly fancier example, where the computation affects the
defun.  In a new session, execute:

     (make-event
       (er-progn (assign my-global (length (w state)))
                 (value `(defun foo (x) (cons x ,(@ my-global))))))

Then:

       ACL2 !>(@ my-global)
       72271
       ACL2 !>:pe foo
        L        1:x(MAKE-EVENT (ER-PROGN # #))

       >L            (DEFUN FOO (X) (CONS X 72271))
       ACL2 !>

Note that ACL2 table events may avoid the need to use state globals.
For example, instead of the example above, consider this example in a
new session.

     (make-event
       (let ((world-len (length (w state))))
         `(progn (table my-table :stored-world-length ,world-len)
                 (defun foo (x) (cons x ,world-len)))))

Then:

       ACL2 !>(table my-table)
        ((:STORED-WORLD-LENGTH . 72271))
       ACL2 !>:pe foo
                 1:x(MAKE-EVENT (LET # #))

       >L            (DEFUN FOO (X) (CONS X 72271))
       ACL2 !>

By the way, most built-in state globals revert after expansion.  But
your own global (like my-global above) can be set during expansion, and
the new value will persist.

MAKE-EVENT-DETAILS    details on make-event expansion

The normal user of make-event can probably ignore this section, but we
include it for completeness.  We assume that the reader has read and
understood the basic documentation for make-event (see
MAKE-EVENT), but we begin below with a summary of expansion.

*Introduction*

Here is a summary of how we handle expansion involving make-event forms.

(make-event form :check-expansion nil)

This shows the :check-expansion default of nil, and is typical user
input.  We compute the expansion exp of form, which is the expansion of
the original make-event expression and is evaluated in place of that
expression.

(make-event form :check-expansion t)

The user presumably wants it checked that the expansion doesn't change
in the future, in particular during include-book.  If the expansion of
form is exp, then we will evaluate exp to obtain the value as before,
but this time we record that the expansion of the original make-event
expression is (make-event form :check-expansion exp) rather than simply
exp.

(make-event form :check-expansion exp) ; exp a cons

This is generated for the case that :check-expansion is t, as explained
above.  Evaluation is handled as described in that above case, except
here we check that the expansion result is the given exp.  (Actually,
the user is also allowed supply such a form.)  The original make-event
expression does not undergo any expansion (intuitively, it expands to
itself).

Now let us take a look at how we expand progn forms (encapsulate is
handled similarly).

(progn ... (make-event form :check-expansion nil) ...)

The expansion is obtained by replacing the make-event form as follows.
Let exp be the expansion of form,  Then replace the above make-event
form, which we denote as F, by (record-expansion F exp).  Here,
record-expansion is a macro that returns its second argument.

(progn ... (make-event form :check-expansion t) ...)

The expansion is of the form (record-expansion F exp) as in the nil
case above, except that this time exp is (make-event form
:check-expansion exp'), where exp' is the expansion of form.

(progn ... (make-event form :check-expansion exp) ...) ; exp a cons

No expansion takes place unless expansion takes place for at least one
of the other subforms of the progn, in which case each such form F is
replaced by (record-expansion F exp) where exp is the expansion of F.

*Detailed semantics*

In our explanation of the semantics of make-event, we assume familiarity
with the notion of "embedded event form" (see
EMBEDDED-EVENT-FORM).

Let's say that the "actual embedded event form" corresponding to a given
form is the underlying call of an ACL2 event: that is, LOCALs are
dropped when ld-skip-proofsp is 'include-book, and macros are expanded
away, thus leaving us with a progn, a make-event, or an event form
(possibly encapsulate), any of which might have surrounding local,
skip-proofs, or with-output calls.

Thus, such an actual embedded event form can be viewed as having the
form (rebuild-expansion wrappers base-form) where base-form is a progn,
a make-event, or an event form (possibly encapsulate), and wrappers are
(as in ACL2 source function destructure-expansion) the result of
successively removing the event form from the result of macroexpansion,
leaving a sequence of (local), (skip-proofs), and (with-output ...)
forms.  In this case we say that the form "destructures into" the
indicated wrappers and base-form, and that it can be "rebuilt from"
those wrappers and base-form.

Elsewhere we define the notion of the "expansion result" from an
evaluation (see MAKE-EVENT), and we mention that when expansion
concludes, the ACL2 logical world and most of the state are restored to
their pre-expansion values.  Specifically, after evaluation of the
argument of make-event (even if it is aborted), the ACL2 logical world
is restored to its pre-evaluation value, as are all state global
variables in the list *protected-system-state-globals*.  Thus,
assignments to user-defined state globals (see ASSIGN) do
persist after expansion, since they are not in that list.

We recursively define the combination of evaluation and expansion of an
embedded event form, as follows.  We also simultaneously define the
notion of "expansion takes place," which is assumed to propagate upward
(in a sense that will be obvious), such that if no expansion takes
place, then the expansion of the given form is considered to be itself.
It is useful to keep in mind a goal that we will consider later: Every
make-event subterm of an expansion result has a :check-expansion field
that is a consp, where for this purpose make-event is viewed as a macro
that returns its :check-expansion field.  (Implementation note: The
latest expansion of a make-event, progn, progn!, or encapsulate is
stored in state global 'last-make-event-expansion, except that if no
expansion has taken place for that form then 'last-make-event-expansion
has value nil.)

     If the given form is not an embedded event form, then simply cause
     a soft error, (mv erp val state) where erp is not nil.  Otherwise:

     If the evaluation of the given form does not take place
     (presumably because local events are being skipped), then no
     expansion takes place.  Otherwise:

     Let x be the actual embedded event form corresponding to the given
     form, which destructures into wrappers W and base-form B.  Then the
     original form is evaluated by evaluating x, and its expansion is as
     follows.

     If B is (make-event form :check-expansion val), then expansion
     takes place if and only if val is not a consp and no error occurs,
     as now described.  Let R be the expansion result from protected
     evaluation of form, if there is no error.  R must be an embedded
     event form, or it is an error.  Then evaluate/expand R, where if
     val is not nil then state global 'ld-skip-proofsp is initialized
     to nil.  (This initialization is important so that subsequent
     expansions are checked in a corresponding environment, i.e., where
     proofs are turned on in both the original and subsquent
     environments.)  It is an error if this evaluation causes an error.
     Otherwise, the evaluation yields a value, which is the result of
     evaluation of the original make-event expression, as well as an
     expansion, E_R.  Let E be rebuilt from W and E_R.  The expansion of
     the original form is E if val is nil, and otherwise is the result
     of replacing the original form's :check-expansion field with E,
     with the added requirement that if val is not t (thus, a consp)
     then E must equal val or else we cause an error.

     If B is either (progn form1 form2 ...) or (encapsulate sigs form1
     form2 ...), then after evaluating B, the expansion of the original
     form is the result of rebuilding from B, with wrappers W, after
     replacing each formi in B for which expansion takes place by
     (record-expansion formi formi'), where formi' is the expansion of
     formi.  Note that these expansions are determined as the formi are
     evaluated in sequence (where in the case of encapsulate, this
     determination occurs only during the first pass).  Except, if no
     expansion takes place for any formi, then the expansion of the
     original form is itself.

     Otherwise, the expansion of the original form is itself.

Similarly to the progn and encapsulate cases above, book certification
causes a book to be replaced by its so-called "book expansion."  There,
each event ev for which expansion took place during the proof pass of
certification -- say, producing ev' -- is replaced by (record-expansion
ev ev').

Implementation Note.  The book expansion is actually implemented by way
of the :expansion-alist field of its certificate, which associates
0-based positions of top-level forms in the book (not including the
initial in-package form) with their expansions.  Thus, the book's
source file is not overwritten; rather, the certificate's
expansion-alist is applied when the book is included or compiled.  End
of Implementation Note.

It is straightforward by computational induction to see that for any
expansion of an embedded event form, every make-event sub-event has a
consp :check-expansion field.  Here, by "sub-event" we mean to expand
macros; and we also mean to traverse progn and encapsulate forms as
well as :check-expansion fields of make-event forms.  Thus, we will
only see make-event forms with consp :check-expansion fields in the
course of include-book forms, the second pass of encapsulate forms, and
raw Lisp.  This fact guarantees that an event form will always be
treated as its original expansion.

*A note on ttags*

See DEFTTAG for documentation of the notion of "trust tag"
("ttag").  We note here that even if an event (defttag tag-name) for
non-nil tag-name is admitted only during the expansion phase of a
make-event form, then such expansion will nevertheless still cause
tag-name to be recorded in the logical world (assuming that the
make-event form is admitted).  This behavior will avoid surprises
involving ttags and make-event expansion in almost all cases, but we now
point out a case where one might get such a surprise.

Below we consider a make-event specifying :check-expansion t, whose
expansion generates a defttag event during include-book but not
certify-book.  Consider the following book.

     (in-package "ACL2")
     (make-event
      (er-progn
       (if (@ skip-notify-on-defttag) ; non-nil when including a certified book
           (pprogn
            (fms "Value of (@ skip-notify-on-defttag): ~x0~|"
                 (list (cons #0 (@ skip-notify-on-defttag)))
                 *standard-co* state nil)
            (encapsulate
             ()
             (defttag :foo)
             (value-triple "Imagine something bad here!")))
         (value nil))
       (value '(value-triple :some-value)))
      :check-expansion t)

This book certifies successfully without the need for a :ttags argument
for certify-book.  Indeed, the above book's certificate does not
specify :foo as a trust tag associated with the book, because no
defttag event was executed during book certification.  Unfortunately, if
we try to include this book without specifying a value of :ttags that
allows :foo, book inclusion will be attempted and will only fail when
the above defttag event is eventually encountered.

MEMOIZE    turn on memoization for one function

This documentation topic relates to an experimental extension of ACL2
under development by Bob Boyer and Warren Hunt.  See
HONS-AND-MEMOIZATION for a general discussion of memoization and the
related features of hash consing and applicative hash tables.

     Examples:
     (memoize 'foo)                      ; remember the values of calls
                                         ;   of foo
     (memoize 'foo :condition t)         ; same as above
     (memoize 'foo :condition '(test x)) ; memoize for args satisfying
                                         ;   the given condition
     (memoize 'foo :condition-fn 'test)  ; memoize for args satisfying
                                         ;   a call of the given function
     (memoize 'foo :inline nil)          ; do not inline the definition
                                         ;   of foo

     * Menu:

     Related topics other than immediate subtopics:
     * HONS-AND-MEMOIZATION:: hash cons, function memoization, and applicative hash tables

     General Form:
     (memoize fn                         ; memoizes fn and returns fn
              :condition    condition    ; optional (default t)
              :condition-fn condition-fn ; optional
              :hints        hints        ; optional, for verifying the
                                         ;   guards of condition-fn
              :otf-flg      otf-flg      ; optional, for verifying the
                                         ;   guards of condition-fn
              :inline       inline       ; optional (default t)
              :commutative  t/lemma-name ; optional (default nil)
              :forget       t/nil        ; optional (default nil)
              :memo-table-init-size size ; optional (default *mht-default-size*)
              :verbose      t/nil        ; optional (default t)
              )

where fn evaluates to a user-defined function symbol; condition is
either t (the default) or 't or else evaluates to an expression whose
free variables are among the formal parameters of fn; and condition-fn
is either nil (the default) or else evaluates to a legal function
symbol.  Further restrictions and options are discussed below.  Note
that all arguments are evaluated (but for the special handling of value
t for :commutative, the argument must literally be t; see below).

Generally fn must evaluate to a defined function symbol whose guards
have been verified.  However, this value can be the name of a macro
that is associated with such a function symbol; see
MACRO-ALIASES-TABLE.  That associated function symbol is the one
called "memoized" in the discussion below, but we make no more mention
of this subtlety.

It is illegal to memoize a function that is already memoized.  To turn
off memoization, see UNMEMOIZE.

In the most common case, memoize takes a single argument, which
evaluates to a function symbol.  We call this function symbol the
"memoized function" because "memos" are saved and re-used, in the
following sense.  When a call of the memoized function is evaluated,
the result is "memoized" by associating the call's arguments with that
result, in a suitable table.  But first an attempt is made to avoid
such evaluation, by doing a lookup in that table on the given arguments
for the result, as stored for a previous call on those arguments.  If
such a result is found, then it is returned without further
computation.  This paragraph also applies if :condition is supplied but
is t or 't.

If in addition :condition-fn is supplied, but :condition is not, then
the result of evaluating :condition-fn must be a defined function symbol
whose guards have been verified and whose formal parameter list is the
same as for the function being memoized.  Such a "condition function"
will be run whenever the memoized function is called, on the same
parameters, and the lookup or table store described above are only
performed if the result from the condition function call is non-nil.

If however :condition is supplied, then an attempt will be made to
define a condition function whose guard and formal parameters list are
the same as those of the memoized function, and whose body is the
result, r, of evaluating the given condition.  The name of that
condition function is the result of evaluating :condition-fn if
supplied, else is the result of concatenating the string
"-MEMOIZE-CONDITION" to the end of the name of the memoized function.
The condition function will be defined with guard verification turned
off, but that definition will be followed immediately by a
verify-guards event; and this is where the optional :hints and :otf-flg
are attached.  At evaluation time the condition function is used as
described in the preceding paragraph; so in effect, the condition (r,
above) is evaluated, with its variables bound to the corresponding
actuals of the memoized function call, and the memoized function
attempts a lookup or table store if and only if the result of that
evaluation is non-nil.

Calls of this macro generate events of the form (table memoize-table fn
((:condition-fn fn) (:inline i) ...)).  When successful, the returned
value is of the form (mv nil function-symbol state).

When :inline has value nil, then memoize does not use the definitional
body of fn in the body of the new, memoized definition of fn.  Instead,
memoize lays down a call to the symbol-function for fn that was in
effect prior to memoization.  Use value t for :inline to avoid
memoizing recursive calls to fn directly from within fn.

If :trace has a non-nil value, then memoize also traces in a
traditional Lisp style.  If :trace has value notinline or notinline,
then a corresponding declaration is added at the beginning of the new
definition of fn.

A non-nil value for :commutative can be supplied if fn is a binary
function.  If the memoize event is successful, then subsequently:
whenever each argument to fn is either a rational number or a hons,
then when the evaluation of fn on those arguments is memoized, the
evaluation of fn on the swap of those arguments is, in essence, also
memoized.  If :commutative is supplied and is not nil or t, then it
should be the name of a previously-proved theorem whose formula states
the commutativity of fn, i.e., is the formula (equal (fn x y) (fn y x))
for a pair {x,y} of distinct variables.  If :commutative is t -- but
not merely an expression that evaluates to t -- then an attempt to
prove such a lemma will be made on-the-fly.  The name of the lemma is
the symbol in the same package as fn, obtained by adding the suffix
"-COMMUTATIVE" to the symbol-name of fn.  If the proof attempt fails,
then you may want first to prove the lemma yourself with appropriate
hints and perhaps supporting lemmas, and then supply the name of that
lemma as the value of :commutative.

If :memo-table-init-size is supplied, then it should be a positive
integer specifying the initial size of an associated hash table.

If :verbose is supplied, it should either be nil, which will inhibit
proof, event, and summary output (see WITH-OUTPUT), or else t
(the default), which does not inhibit output.  If the output baffles
you, try

     :trans1 (memoize ...)

to see the single-step macroexpansion of your memoize call.

If :commutative is supplied, and a non-commutative condition is provided
by :condition or :condition-fn, then although the results will be
correct, the extra memoization afforded by :commutative is unspecified.

The default for :forget is nil.  If :forget is supplied, and not nil,
then it must be t, which causes all memoization done for a top-level
call of fn to be forgotten when that top-level call exits.

Memoize is illegal for a function whose arguments include state or,
more generally, any stobj.  Also, memoize never allows attachments to
be used (see DEFATTACH); if an attachment is used during
evaluation, then the evaluation result will not be stored.

MUTUAL-RECURSION    define some mutually recursive functions

     Example:
     (mutual-recursion
      (defun evenlp (x)
        (if (consp x) (oddlp (cdr x)) t))
      (defun oddlp (x)
        (if (consp x) (evenlp (cdr x)) nil)))

     General Form:
     (mutual-recursion def1 ... defn)
     where each defi is a defun form or a defund form.

When mutually recursive functions are introduced it is necessary to do
the termination analysis on the entire clique of definitions.  Each
defun form specifies its own measure, either with the :measure keyword
xarg (see XARGS) or by default to acl2-count.  When a function
in the clique calls a function in the clique, the measure of the
callee's actuals must be smaller than the measure of the caller's
formals -- just as in the case of a simply recursive function.  But
with mutual recursion, the callee's actuals are measured as specified
by the callee's defun while the caller's formals are measured as
specified by the caller's defun.  These two measures may be different
but must be comparable in the sense that o< decreases through calls.

If you want to specify :hints or :guard-hints (see XARGS), you
can put them in the xargs declaration of any of the defun forms, as the
:hints from each form will be appended together, as will the
guard-hints from each form.

You may find it helpful to use a lexicographic order, the idea being to
have a measure that returns a list of two arguments, where the first
takes priority over the second.  Here is an example.

     (include-book "ordinals/lexicographic-ordering" :dir :system)

     (encapsulate
      ()
      (set-well-founded-relation l<) ; will be treated as LOCAL

      (mutual-recursion
       (defun foo (x)
         (declare (xargs :measure (list (acl2-count x) 1)))
         (bar x))
       (defun bar (y)
         (declare (xargs :measure (list (acl2-count y) 0)))
         (if (zp y) y (foo (1- y))))))

The guard analysis must also be done for all of the functions at the
same time.  If any one of the defuns specifies the :verify-guards xarg
to be nil, then guard verification is omitted for all of the functions.

Technical Note: Each defi above must be of the form (defun ...).  In
particular, it is not permitted for a defi to be a form that will
macroexpand into a defun form.  This is because mutual-recursion is
itself a macro, and since macroexpansion occurs from the outside in, at
the time (mutual-recursion def1 ... defk) is expanded the defi have not
yet been.  But mutual-recursion must decompose the defi.  We therefore
insist that they be explicitly presented as defuns or defunds (or a
mixture of these).

Suppose you have defined your own defun-like macro and wish to use it
in a mutual-recursion expression.  Well, you can't.  (!)  But you can
define your own version of mutual-recursion that allows your defun-like
form.  Here is an example.  Suppose you define

     (defmacro my-defun (&rest args) (my-defun-fn args))

where my-defun-fn takes the arguments of the my-defun form and produces
from them a defun form.  As noted above, you are not allowed to write
(mutual-recursion (my-defun ...) ...).  But you can define the macro
my-mutual-recursion so that

     (my-mutual-recursion (my-defun ...) ... (my-defun ...))

expands into (mutual-recursion (defun ...) ... (defun ...)) by applying
my-defun-fn to each of the arguments of my-mutual-recursion.

     (defun my-mutual-recursion-fn (lst)
       (declare (xargs :guard (alistp lst)))

     ; Each element of lst must be a consp (whose car, we assume, is always
     ; MY-DEFUN).  We apply my-defun-fn to the arguments of each element and
     ; collect the resulting list of DEFUNs.

       (cond ((atom lst) nil)
             (t (cons (my-defun-fn (cdr (car lst)))
                      (my-mutual-recursion-fn (cdr lst))))))

     (defmacro my-mutual-recursion (&rest lst)

     ; Each element of lst must be a consp (whose car, we assume, is always
     ; MY-DEFUN).  We obtain the DEFUN corresponding to each and list them
     ; all inside a MUTUAL-RECURSION form.

       (declare (xargs :guard (alistp lst)))
       (cons 'mutual-recursion (my-mutual-recursion-fn lst))).

PROGN    evaluate some events

     Example Form:
     (progn (defun foo (x) x)
            (defmacro my-defun (&rest args)
              (cons 'defun args))
            (my-defun bar (x) (foo x)))

     General form:
     (progn event1 event2 ... eventk)

where k >= 0 and each eventi is a legal embedded event form (see
EMBEDDED-EVENT-FORM).  These events are evaluated in sequence.  A
utility is provided to assist in debugging failures of such execution;
see REDO-FLAT.

NOTE: If the eventi above are not all legal embedded event forms (see
EMBEDDED-EVENT-FORM), consider using er-progn or (with great
care!) progn! instead.

For a related event form that does allow introduction of constraints
and local events, see ENCAPSULATE.

ACL2 does not allow the use of progn in definitions.  Instead, the
macro er-progn can be used for sequencing state-oriented operations;
see ER-PROGN and see STATE.  If you are using
single-threaded objects (see STOBJ) you may wish to define a
version of er-progn that cascades the object through successive
changes.  ACL2's pprogn is the state analogue of such a macro.

If your goal is simply to execute a sequence of top-level forms, for
example a sequence of definitions, consider using ld instead; see
LD.

PROGN!    evaluate some forms, not necessarily events

*WARNING!*  This event is intended for advanced users who, in essence,
want to build extensions of ACL2.  See see DEFTTAG, in
particular, the "WARNING" there, and see the warning about stobjs at
the end of this documentation topic.

Progn! can be used like progn, even in books.  But unlike progn, progn!
does not require its constituent forms to be events (see
EMBEDDED-EVENT-FORM), except that the first form cannot be a symbol
unless it is :state-global-bindings (advanced feature, described
below).  However, see MAKE-EVENT for a "Restriction to the Top
Level" that still applies under a call of progn!.

Because progn! allows non-events, it differs from progn in another
important respect: progn! is illegal unless there is an active ttag;
see DEFTTAG.

See books/hacking/hacker.lisp for two macros, with-raw-mode and
with-redef-allowed, each defined in terms of progn!, that allow
arbitrary forms in contexts that would normally require legal embedded
event forms.

Given a form (progn! form1 form2 ... formk), ACL2 will evaluate each
formi in turn (for i from 1 to k).  If a form returns more than one
value (see MV) where the first value returned is not nil, then
no later form will be evaluated and the result returned by the progn!
call will be (mv erp val state) for some non-nil value erp, signifying
an error (see LD-ERROR-TRIPLES).  Otherwise the evaluation is
considered to have succeeded, and will continue with later forms.  The
value returned by a call of progn! with no such error is of the form
(mv nil v state), where v depends on the last form as follows.  If the
last form evaluates to a single value, then v is that value, except if
the value is a stobj, say ST, then v is the symbol REPLACED-ST.
Otherwise the last form evaluates to some (mv nil x ...), and v is x
unless after the final form's evaluation we are in raw-mode (see
SET-RAW-MODE), in which case the progn! call returns nil (so that
ACL2 can at least print the result -- imagine Lisp returning a pathname
object from a load call, for example).

The normal undoing mechanism does not generally apply to forms within a
progn! that are not legal ACL2 events (see EMBEDDED-EVENT-FORM).
In particular, note that a non-local call of progn! in an encapsulate
event will generally be evaluated twice: once on each pass.  This fact
is worth keeping in mind if you are using progn! to change the state of
the system; ask yourself if it is acceptable to apply that
state-changing operation more than once.

Please note that progn! may differ from progn in the following sense:
definitions within a call of progn! might not be compiled.  For
example, consider the following book.

     (in-package "ACL2")
     (defttag :test)
     (progn  (defun f1 (x) x))
     (progn! (defun f2 (x) x))

If the underlying Lisp is GCL 2.6.7, then after including this
certified book (where the default certification took place, creating a
compiled file), then f1 is a compiled function but f2 is not.  For
other Lisps supported by ACL2, both f1 and f2 are compiled, though we
are not sure that every function under every call of progn! would
similarly be compiled.

We now describe, for system hackers only, a sophisticated extension of
progn! not mentioned above: support for keyword argument
:state-global-bindings.  If the first argument of progn! is this
keyword, then the second argument is treated as a list of bindings as
expected by ACl2 system function state-global-let* (not yet documented).
Thus, in the ACL2 loop,

     (progn! :state-global-bindings bindings form1 form2 ... formk)

is treated as follows:

     (progn! (state-global-let* bindings (progn! form1 form2 ... formk)))

However, in raw Lisp the former is just:

     (progn form1 form2 ... formk)

Thus, one should use the :state-global-bindings argument with care,
since the behavior in the ACL2 loop can differ from that in Common
Lisp.  The intention is that one bind only state global variables that
are relevant to evaluation of the forms within the ACL2 loop and are
harmlessly ignored for evaluation of those forms in raw Lisp.  Here is
a typical sort of example, as state global ld-redefinition-action is
not relevant to the evaluation of defun in raw Lisp.

     (progn! (remove-untouchable 'ld-redefinition-action nil)
             (progn! :state-global-bindings
                     ((ld-redefinition-action '(:doit . :overwrite)))
                     (defun foo (x)
                       (cons x x)))
             (push-untouchable 'ld-redefinition-action nil))

Finally, we point out a pitfall of progn! related to stobjs.  The
following book can cause a hard Lisp error, depending on the host Common
Lisp, when certified with a non-nil value for compile-flg (see
CERTIFY-BOOK).

     (in-package "ACL2")
     (defstobj st fld)
     (defttag :my-ttag)
     (progn! (update-fld 3 st))

The problem is that the stobj variable st is not known to raw Lisp.
The compilation problem disappears if the last form above is replaced
with the following two forms.

     (include-book "misc/hacker" :dir :system)
     (with-raw-mode (update-fld 3 *the-live-st*))

REDO-FLAT    redo up through a failure in an encapsulate or progn

When one submits an encapsulate or progn event and one of its
sub-events fails, ACL2 restores its logical world as though the
encapsulate or progn had not been run.  But sometimes one would like to
debug the failure by re-executing all sub-events that succeeded up to
the point of failure, and then re-executing the failed sub-event.  Said
differently, imagine that the top-level encapsulate or progn form, as
well as all such sub-forms, were flattened into a list of events that
were then submitted to ACL2 up to the point of failure.  This would put
us in the state in which the original failed event had failed, so we
could now submit that failed event and try modifying it, or first
proving additional events, in order to get it admitted.

Redo-flat is provided for this purpose.  Consider the following (rather
nonsensical) example, in which the defun of f3 fails (the body is y but
the formal parameter list is (x)).

     (encapsulate
      ()
      (defun f1 (x) x)
      (encapsulate ()
                   (local (defthm hack (equal (car (cons x y)) x))))
      (encapsulate ()
                   (local (defthm hack (equal (+ x y) (+ y x)))))
      (encapsulate ()
                   (make-event '(defun f2 (x) x))
                   (progn (defthm foo (equal x x) :rule-classes nil)
                          (defun f3 (x) y)))
      (defun f4 (x) x)
      (defun f5 (x) y))

After this attempt fails, you can evaluate the following form.

     (redo-flat)

This will first lay down a deflabel event, (deflabel r), so that you
can eventually remove your debugging work with (:ubt! r).  Then the
successful sub-events that preceded the failure will be executed with
proofs skipped (so that this execution is fast).  Then, the failed
event will be executed.  Finally, a :pbt command is executed so that
you can see a summary of the events that executed successfully.

You can eliminate some of the steps above by supplying keyword values,
as follows.

     (redo-flat
      :succ  succ ; Skip the successful sub-events if val is nil.
      :fail  fail ; Skip the failed sub-event if val is nil.
      :label lab  ; Skip deflabel if lab or succ is nil, else use (deflabel lab).
      :pbt   val  ; Skip the final :pbt if val, lab, or succ is nil.
      )

Also, you can avoid skipping proofs for the successful sub-events by
supplying keyword :succ-ld-skip-proofsp with a valid value for
ld-skip-proofsp; see LD-SKIP-PROOFSP.

If you prefer only to see the successful and failed sub-events, without
any events being re-executed, you may evaluate the following form
instead.

     (redo-flat :show t)

For the example above, this command produces the following output.

     List of events (from encapsulate or progn) preceding the failure:

     ((DEFUN F1 (X) X)
      (ENCAPSULATE NIL
                   (LOCAL (DEFTHM HACK (EQUAL (CAR (CONS X Y)) X))))
      (ENCAPSULATE NIL
                   (LOCAL (DEFTHM HACK (EQUAL (+ X Y) (+ Y X)))))
      (MAKE-EVENT '(DEFUN F2 (X) X))
      (DEFTHM FOO (EQUAL X X)
              :RULE-CLASSES NIL))

     Failed event:

     (DEFUN F3 (X) Y)
     ACL2 !>

Redo-flat uses a scheme that should not cause spurious name conflicts
for local events.  Above, it is mentioned that events are "flattened";
now we clarify this notion.  Each sub-event that succeeds and is an
encapsulate or progn is left intact.  Only such events that fail are
replaced by their component events.  Thus, in the example above, there
is no conflict between the two local sub-events named "hack," because
these are contained in successful encapsulate sub-events, which are
therefore not flattened.  The progn and two encapsulate events
surrounding the definition of f3 are, however, flattened, because that
definition failed to be admitted.

Unfortunately, an event must actually fail in order for redo-flat to
work.  So if the system is "stuck" on an event, then you may find it
helpful to insert an illegal event just in front of it before
submitting the encapsulate or progn.

REMOVE-CUSTOM-KEYWORD-HINT    remove a custom keyword hint

     Example Forms:
     (remove-custom-keyword-hint :my-hint)

     General Form:
     (remove-custom-keyword-hint keyword)

where keyword is a keywordp.

For an explanation of how custom keyword hints are processed, see
CUSTOM-KEYWORD-HINTS; also see ADD-CUSTOM-KEYWORD-HINT.

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

SET-BODY    set the definition body

     Examples:
     (set-body foo (:definition foo)) ; restore original definition of foo
     (set-body foo foo) ; same as just above
     (set-body foo my-foo-def) ; use my-foo-def for the body of foo
     (set-body foo (:definition my-foo-def)) ; same as just above

Rules of class :definition can install a new definition body, used for
example by :expand hints.  See DEFINITION and also see
HINTS for a detailed discussion of the :install-body fields of
:definition rules and their role in :expand hints.

There may be several such definitions, but by default, the latest one
is used by :expand hints.  Although the :with keyword may be used in
:expand hints to override this behavior locally (see HINTS), it
may be convenient to install a definition for expansion other than the
latest one -- for example, the original definition.  Set-body may be
used for this purpose.

     General Form:
     (set-body function-symbol rule-name)

where rule-name is either a :definition rune or is a function symbol,
sym, which represents the rune (:definition sym).

You can view all definitions available for expansion; see
SHOW-BODIES.