Major Section: EVENTS

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.

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.

Major Section: EVENTS

Example: (deftheory interp-theory (set-difference-theories (universal-theory :here) (universal-theory 'interp-section)))whereGeneral Form: (deftheory name term :doc doc-string)

`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 `name`

. Henceforth, this runic theory is returned as the value of the
theory expression `(theory name)`

.
Major Section: EVENTS

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]")whereGeneral Form: (defthm name term :rule-classes rule-classes :instructions instructions :hints hints :otf-flg otf-flg :doc doc-string)

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

Major Section: EVENTS

Examples: (defun app (x y) (if (consp x) (cons (car x) (app (cdr x) y)) y))where(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),

`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 multiple `dcl`

forms appear, 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.

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 `e0-ord-<`

(see e0-ord-<), which is known to be well-founded on the
`e0-ordinalp`

s (see e0-ordinalp). 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
`e0-ord-<`

on the `e0-ordinalp`

s.

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:

(e0-ordinalp (m x y)).The second shows that

`m`

decreases in the (only) recursive call of
`fn`

:
(implies (not (test x y)) (e0-ord-< (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 e0-ord-< 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, `e0-ord-<`

is just
the familiar ``less than'' relation (`<`

). Thus, it is very common
to use a measure `m`

that returns a nonnegative integer, for then
`(e0-ordinalp (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-count`

s 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-clauses 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., `e0-ord-<`

) and a domain predicate (e.g.,
`e0-ordinalp`

) 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 `e0-ord-<`

(with domain
predicate `e0-ordinalp`

).

This completes the brief sketch of the ACL2 definitional principle.

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,
`xargs`

, and hints, but is completely nonsensical.

(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) :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 :otf-flg t)) (example-body x y z i j))

Major Section: EVENTS

Examples: (defun-sk forall-x-p-and-q (y z) (forall x (and (p x y z) (q x y z))))(defun-sk forall-x-p-and-q (y z) ; equivalent to the above (forall (x) (and (p x y z) (q x y z))))

(defun-sk some-x-y-p-and-q (z) (exists (x y) (and (p x y z) (q x y z))))

General Form:

(defun-sk fn (var1 ... varn) body &key doc quant-ok skolem-name thm-name)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. The other arguments are explained
below. For a more elaborate example than those above,
see Tutorial4-Defun-Sk-Example.
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
the following two theorems 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) (let ((v (skolem-name var1 ... varn))) body))In the case that(defthm fn-suff ;in case the quantifier is EXISTS (implies body (fn var1 ... varn)))

(defthm fn-necc ;in case the quantifier is FORALL (implies (not body) (not (fn var1 ... varn))))

`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) (mv-let (bv1 ... bvk) (skolem-name var1 ... varn) body))

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.

Those who want a more flexible version of `defun-sk`

that allows
nested quantifiers, should contact the implementors. In the
meantime, if you want to represent nested quantifiers, you have to
manage that yourself. For example, in order to represent

(forall x (exists y (p x y z)))you would 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`

.

`Defun-sk`

is implemented using `defchoose`

, and hence should only
be executed in defun-mode `:`

`logic`

; see defun-mode and
see defchoose.

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'' (to appear in the Journal of Automated
Reasoning, 2000) explains why our use of `defchoose`

is
appropriate, even in the presence of `epsilon-0`

induction.

Major Section: DEFUN-SK

The symbol `exists`

(in the ACL2 package) represents existential
quantification in the context of a `defun-sk`

form.
See defun-sk and see forall.

Major Section: DEFUN-SK

The symbol `forall`

(in the ACL2 package) represents universal
quantification in the context of a `defun-sk`

form.
See defun-sk and see exists.

Major Section: EVENTS

Examples: (encapsulate (((an-element *) => *))where each signature is as described in the documentation for signature, each signature describes a different function symbol, and each; 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)

`evi`

is an embedded event form as described in
the documentation for 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 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.

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.

Major Section: EVENTS

Example: (in-theory (set-difference-theories (universal-theory :here) '(flatten (:executable-counterpart flatten))))whereGeneral Form: (in-theory term :doc doc-string)

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

Major Section: EVENTS

Examples: (include-book "my-arith") (include-book "/home/smith/my-arith") (include-book "/../../my-arith")whereGeneral 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] :doc doc-string)

`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 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. `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 insure 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. The effect of compilation is to speed up the
execution of the functions defined within the book when those
functions are applied to specific values. 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.

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

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.