This is documentation for ACL2 Version 3.0
Copyright (C) 2006  University of Texas at Austin

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

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

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

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

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

     * Menu:

     * DEFUN-SK-EXAMPLE:: a simple example using defun-sk

     * EXISTS:: existential quantifier

     * FORALL:: universal quantifier

     * QUANTIFIERS:: issues about quantification in ACL2

     General Form:
     (defun-sk fn (var1 ... varn) body
       &key doc quant-ok skolem-name thm-name witness-dcls)

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.  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.)  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 exists-x-p0-and-q0 (y z)
       (declare (xargs :non-executable t))
       (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 forall-x-y-p0-and-q0 (z)
       (declare (xargs :non-executable t))
       (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.

We now turn to a detailed description 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 fn (var1 ... varn)
       (declare (xargs :non-executable t))
       (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 case that bound-vars is a list of at least two variables, say
(bv1 ... bvk), the definition above is the following instead, but the
theorem remains unchanged.

     (defun fn (var1 ... varn)
       (declare (xargs :non-executable t))
       (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.

Note the form (declare (xargs :non-executable t)) that appears in each
defun above.  These forms disable certain checks that are required for
execution, in particular the single-threaded use of stobjs.  However,
there is a price: calls of these defined functions cannot be evaluated.
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.

Defun-sk is a macro implemented using defchoose, and hence should only
be executed in defun-mode :logic; see DEFUN-MODE and see
DEFCHOOSE.

If you find that the rewrite rules introduced with a particular use of
defun-sk are not ideal, 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!  A paper by ACL2 authors
Kaufmann and Moore, entitled "Structured Theory Development for a
Mechanized Logic" (Journal of Automated Reasoning 26, no. 2 (2001),
pp. 161-203) explains why our use of defchoose is appropriate, even in
the presence of epsilon-0 induction.

DEFUN-SK-EXAMPLE    a simple example using defun-sk

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.

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, we recommend 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-EXTENDEDfor
an elaboration on that solution.

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.

DELETE-INCLUDE-BOOK-DIR    remove association of keyword for include-book's :dir argument

     Example Forms:
     (delete-include-book-dir :smith)
      ; Remove association of directory with :smith for include-book.

     General Form:
     (delete-include-book-dir kwd)

where kwd is a keywordp.  The effect of this event is to modify the
meaning of the :dir keyword argument of include-book as indicated by the
examples above, namely by removing association of any directory with the
indicated keyword for purposes of the include-book :dir argument.
Normally one would instead use add-include-book-dir to associate a new
directory with that keyword; see ADD-INCLUDE-BOOK-DIR.

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

This macro generates a call (table acl2-defaults-table
:include-book-dir-alist ...)  and hence is local to any books and
encapsulate events in which is occurs. See ACL2-DEFAULTS-TABLE.

DIVE-INTO-MACROS-TABLE    right-associated function information for the proof-checker

     Examples:
     ACL2 !>(dive-into-macros-table (w state))
     ((CAT . EXPAND-ADDRESS-CAT)
      (LXOR . EXPAND-ADDRESS-LXOR)

This table associates macro names with functions used by the
proof-checker's DV and numeric diving commands (e.g., 3) in order to
dive properly into subterms.  See PROOF-CHECKER, in particular
the documentation for DV.

This table can be extended easily.  See ADD-DIVE-INTO-MACRO and
also see REMOVE-DIVE-INTO-MACRO.

The symbol associated with a macro should be a function symbol taking
four arguments, in this order:

     car-addr ; the first number in the list given to the proof-checker's
                DV command
     raw-term ; the untranslated term into which we will dive
     term     ; the translated term into which we will dive
     wrld     ; the current ACL2 logical world

The function will normally return a list of positive integers,
representing the (one-based) address for diving into term that
corresponds to the single-address dive into raw-term by car-address.
However, it can return (cons str alist), where str is a string suitable
for fmt and args is the corresponding alist for fmt.

Referring to the example above, expand-address-cat would be such a
function, which will be called on raw-term values that are calls of cat.
See the distributed book books/misc/rtl-untranslate.lisp for the
definition of such a function.

See TABLE for a general discussion of tables.

ENCAPSULATE    constrain some functions and/or hide some events

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

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

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.  See REDUNDANT-EVENTS.

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.

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  ; [default :warn]
                        :uncertified-okp t/nil      ; [default t]
                        :defaxioms-okp t/nil        ; [default t]
                        :skip-proofs-okp t/nil      ; [default t]
                        :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,
:warn (the default), :try, or :comp; these values are explained below.
The first 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, :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 there is a compiled file for the book that was created more recently
than the book itself and the value action of the :load-compiled-file
argument is not nil, or is omitted, then the compiled file is
automatically loaded; otherwise it is not loaded.  If action is t then
the compiled file must be loaded or an error will occur; if action is
:warn (the default) then a warning will be printed; if action is :try
then no warning will be printed; and if action is :comp then the file
will be immediately compiled (if the compiled file does not already
exist) and loaded.  Certify-book can also be used to compile a book.  An
effect of compilation is to speed up the execution of the functions
defined within the book when those functions are applied to specific
values.  Compilation can also remove tail recursion, thus avoiding stack
overflows.  The presence of compiled code for the functions in the book
should not otherwise affect the performance of ACL2.  See GUARD
for a discussion.  NOTE: the :load-compiled-file argument is not
recursive; that is, calls of include-book that are inside the book
supplied to include-book will use their own :load-compiled-file
arguments (default :warn), not the :load-compiled-file argument for the
enclosing book.

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.

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

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

INVISIBLE-FNS-TABLE    functions that are invisible to the loop-stopper algorithm

     Examples:
     ACL2 !>(invisible-fns-table (w state))
     ((binary-+ unary--)
      (binary-* unary-/)
      (unary-- unary--)
      (unary-/ unary-/))

Among other things, the setting above has the effect of making unary--
"invisible" for the purposes of applying permutative :rewrite rules to
binary-+ trees.  Also see ADD-INVISIBLE-FNS, see
REMOVE-INVISIBLE-FNS, and see SET-INVISIBLE-FNS-TABLE.

See TABLE for a general discussion of tables.

The "invisible functions table" is an alist with elements of the
following form, where fn is a function symbol and the ufni are unary
function symbols in the current ACL2 world, and k is at least 1.

     (fn ufn1 ufn2 ... ufnk)

This table thus associates with certain function symbols, e.g., fn
above, a set of unary functions, e.g., the ufni above.  The ufni
associated with fn in the invisible functions table are said to be
"invisible with respect to fn."  If fn is not the car of any pair in the
alist, then no function is invisible for it.  Thus for example, setting
the invisible functions alist to nil completely eliminates the
consideration of invisibility.

The notion of invisibility is involved in the use of the :loop-stopper
field of :rewrite rules to prevent the indefinite application of
permutative rewrite rules.  Roughly speaking, if rewrite rules are being
used to permute arg and (ufni arg) inside of a nest of fn calls, and
ufni is invisible with respect to fn, then arg and (ufni arg) are
considered to have the same "weight" and will be permuted so as to end
up as adjacent tips in the fn nest.  See LOOP-STOPPER.

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.

LOGIC    to set the default defun-mode to :logic

     Example:
     ACL2 p!>:logic
     ACL2 !>

Typing the keyword :logic sets the default defun-mode to :logic.

Functions defined in :logic mode are logically defined.  See
DEFUN-MODE.

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

See DEFUN-MODE for a discussion of the defun-modes available and
what their effects on the logic are.  See DEFAULT-DEFUN-MODE for
a discussion of how the default defun-mode is used.  This event is
equivalent to (table acl2-defaults-table :defun-mode :logic), and hence
is local to any books and encapsulate events in which is occurs. See
ACL2-DEFAULTS-TABLE.

Recall that the top-level form :logic is equivalent to (logic); see
KEYWORD-COMMANDS.  Thus, to change the default defun-mode to
:logic in a book, use (logic), which is an embedded event form, rather
than :logic, which is not a legal form for books.  See
EMBEDDED-EVENT-FORM.

MACRO-ALIASES-TABLE    a table used to associate function names with macro names

     Example:
     (table macro-aliases-table 'append 'binary-append)

This example associates the function symbol binary-append with the macro
name append.  As a result, the name append may be used as a runic
designator (see THEORIES) by the various theory functions.
Thus, for example, it will be legal to write

     (in-theory (disable append))

as an abbreviation for

     (in-theory (disable binary-append))

which in turn really abbreviates

     (in-theory (set-difference-theories (current-theory :here)
                                         '(binary-append)))

     General Form:

     (table macro-aliases-table 'macro-name 'function-name)

or very generally

     (table macro-aliases-table macro-name-form function-name-form)

where macro-name-form and function-name-form evaluate, respectively, to
a macro name and a function name in the current ACL2 world.  See
TABLE for a general discussion of tables and the table event used to
manipulate tables.

The table macro-aliases-table is an alist that associates macro symbols
with function symbols, so that macro names may be used as runic
designators (see THEORIES).  For a convenient way to add entries
to this table, see ADD-MACRO-ALIAS.  To remove entries from the
table with ease, see REMOVE-MACRO-ALIAS.

This table is used by the theory functions.  For example, in order that
(disable append) be interpreted as (disable binary-append), it is
necessary that the example form above has been executed.  In fact, this
table does indeed associate many of the macros provided by the ACL2
system, including append, with function symbols.  Loosely speaking, it
only does so when the macro is "essentially the same thing as" a
corresponding function; for example, (append x y) and (binary-append x
y) represent the same term, for any expressions x and y.

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

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

*Caveat.*

As explained above, expansion for make-event is the process of
evaluating its argument, which is an arbitrary ACL2 expression, to
obtain an event as the expansion result.  Because the expression is
arbitrary, you can cause significant damage, as illustrated by the
following example from Bob Boyer.  (The setting of the raw Lisp variable
*features* is just to illustrate that any such mischief is possible.
Normally *features* is a list with more than a few elements.)

     % cat foo
     print *0x85d2064=0x838E920
     detach
     q
     % acl2
     ... boilerplate deleted
     ACL2 !>(sys-call "gdb -p $PPID -w < foo >& /dev/null " nil)
     NIL
     ACL2 !>:q

     Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
     ACL2>*features*

     (:AKCL-SET-MV)

     ACL2>

Sandip Ray has observed that this problem occurs in the interactive loop
even without using make-event.  Make-event makes it easy to conceal such
mischief inside a book, though Robert Krug points out that value-triple
allows such mischief as well (see EMBEDDED-EVENT-FORM).  We may
address this issue in future releases of ACL2.