Major Section: MISCELLANEOUS

ACL2 Version 2.5 -- A Computational Logic for Applicative Common Lisp Copyright (C) 2000 University of Texas at Austin

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

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. See the file `LICENSE`

. If not, write
to the Free Software Foundation, Inc., 675 Mass Ave, Cambridge, MA
02139, USA.

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

Please also see acknowledgments.

Major Section: MISCELLANEOUS

This is a low-level system function at the present time.
See pr and see pr! instead. Also see rule-classes
for the use of the symbol `:corollary`

in specifying a rule
class.

Major Section: MISCELLANEOUS

`Current-package`

is an `ld`

special (see ld). The accessor is
`(current-package state)`

and the updater is
`(set-current-package val state)`

, or more conventionally,
`(in-package val)`

. The value of `current-package`

is actually
the string that names the package. (Common Lisp's ``package''
objects do not exist in ACL2.) The current package must be known to
ACL2, i.e., it must be one of the initial packages or a package
defined with `defpkg`

by the user.

When printing symbols, the package prefix is displayed if it is not
the `current-package`

and may be optionally displayed otherwise.
Thus, if `current-package`

is `"ACL2"`

then the symbol `'ACL2::SYMB`

may
be printed as `SYMB`

or `ACL2::SYMB`

, while `'MY-PKG::SYMB`

must be
printed as `MY-PKG::SYMB`

. But if `current-package`

is `"MY-PKG"`

then
the former symbol must be printed as `ACL2::SYMB`

while the latter may
be printed as `SYMB`

.

In Common Lisp, `current-package`

also affects how objects are read
from character streams. Roughly speaking, read and print are
inverses if the `current-package`

is fixed, so reading from a stream
produced by printing an object must produce an equal object.

In ACL2, the situation is more complicated because we never read
objects from character streams, we only read them from object
``streams'' (channels). Logically speaking, the objects in such a
channel are fixed regardless of the setting of `current-package`

.
However, our host file systems do not support the idea of Lisp
object files and instead only support character files. So when you
open an object input channel to a given (character file) we must
somehow convert it to a list of ACL2 objects. This is done by a
*deus ex machina* (``a person or thing that appears or is introduced
suddenly and unexpectedly and provides a contrived solution to an
apparently insoluble difficulty,'' Webster's Ninth New Collegiate
Dictionary). Roughly speaking, the *deus ex machina* determines what
sequence of calls to `read-object`

will occur in the future and what
the `current-package`

will be during each of those calls, and then
produces a channel containing the sequence of objects produced by an
analogous sequence of Common Lisp reads with `*current-package*`

bound
appropriately for each.

A simple rule suffices to make sane file io possible: before you
read an object from an object channel to a file created by printing
to a character channel, make sure the `current-package`

at read-time
is the same as it was at print-time.

`defun`

'd functions
Major Section: MISCELLANEOUS

When a `defun`

is processed and no `:mode`

`xarg`

is supplied, the
function `default-defun-mode`

is used. To find the default defun-mode
of the current ACL2 world, type `(default-defun-mode (w state))`

.
See defun-mode for a discussion of defun-modes. To change the
default defun-mode of the ACL2 world, type one of the keywords
`:`

`program`

or `:`

`logic`

.

The default ACL2 prompt displays the current default defun-mode by
showing the character `p`

for `:`

`program`

mode, and omitting it for
`:`

`logic`

mode; see default-print-prompt. The default defun-mode
may be changed using the keyword commands `:`

`program`

and `:`

`logic`

,
which are equivalent to the commands `(program)`

and `(logic)`

.
Each of these names is documented separately: see program and
see logic. The default defun-mode is stored in the table
`acl2-defaults-table`

and hence may also be changed by a `table`

command. See table and also see acl2-defaults-table.
Both mode-changing commands are events.

While events that change the default defun-mode are permitted within
an `encapsulate`

or the text of a book, their effects are local in
scope to the duration of the encapsulation or inclusion. For
example, if the default defun-mode is `:`

`logic`

and a book is
included that contains the event `(program)`

, then subsequent
events within the book are processed with the default defun-mode
`:`

`program`

; but when the `include-book`

event completes, the
default defun-mode will still be `:`

`logic`

. Commands that change
the default defun-mode are not permitted inside `local`

forms.

`ld`

Major Section: MISCELLANEOUS

Example prompt: ACL2 p!s>The prompt printed by ACL2 displays the current package, followed by a space, followed by zero or more of the three characters as specified below, followed by the character

`>`

printed one or more
times, reflecting the number of recursive calls of `ld`

. The three
characters in the middle are as follows:
p ; when (default-defun-mode (w state)) is :program ! ; when guard checking is on s ; when (ld-skip-proofsp state) is tSee default-defun-mode, see set-guard-checking, and see ld-skip-proofsp.

Also see ld-prompt to see how to install your own prompt.

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

.

ACL2 !> ; logic mode with guard checking on ACL2 > ; logic mode with guard checking off ACL2 p!> ; program mode with guard checking on ACL2 p> ; program mode with guard checking offHere are some examples with

`default-defun-mode`

of `:`

`logic`

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

Major Section: MISCELLANEOUS

Two ``defun-modes'' are supported, `:`

`program`

and `:`

`logic`

. Roughly
speaking, `:`

`program`

mode allows you to prototype a function for
execution without any proof burdens, while `:`

`logic`

mode allows you to
add a new definitional axiom to the logic. The system comes up in
`:`

`logic`

mode. Execution of functions whose defun-mode is `:`

`program`

may render ACL2 unsound! See defun-mode-caveat.

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

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

Thus, ACL2 introduces the idea of the ``defun-mode'' of a function.
The `:mode`

keyword of `defun`

's `declare`

`xarg`

allows you to
specify the defun-mode of a given definition. If no `:mode`

keyword is supplied, the default defun-mode is used;
see default-defun-mode.

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

`:`

`program`

-- logically undefined but executable outside deductive
contexts.

`:`

`logic`

-- axiomatically defined as per the ACL2 definitional
principle.

It is possible to change the defun-mode of a function from `:`

`program`

to `:`

`logic`

. We discuss this below.

We think of functions having `:`

`program`

mode as ``dangerous''
functions, while functions having `:`

`logic`

mode are ``safe.'' The
only requirement enforced on `:`

`program`

mode functions is the
syntactic one: each definition must be well-formed ACL2. Naively
speaking, if a `:`

`program`

mode function fails to terminate then no
harm is done because no axiom is added (so inconsistency is avoided)
and some invocations of the function may simply never return. This
simplistic justification of `:`

`program`

mode execution is faulty
because it ignores the damage that might be caused by
``mis-guarded'' functions. See defun-mode-caveat.

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

The default defun-mode is `:`

`logic`

. This means that when you `defun`

a
function the system will try to prove termination. If you wish to
introduce a function of a different defun-mode use the `:mode`

`xargs`

keyword. Below we show `fact`

introduced as a function in `:`

`program`

mode.

(defun fact (n) (declare (xargs :mode :program)) (if (or (not (integerp n)) (= n 0)) 1 (* n (fact (1- n)))))No axiom is added to the logic as a result of this definition. By introducing

`fact`

in `:`

`program`

mode we avoid the burden of a
termination proof, while still having the option of executing the
function. For example, you can type
ACL2 !>(fact 3)and get the answer

`6`

. If you type `(fact -1)`

you will get a hard
lisp error due to ``infinite recursion.''
However, the ACL2 theorem prover knows no axioms about `fact`

. In
particular, if the term `(fact 3)`

arises in a proof, the theorem
prover is unable to deduce that it is `6`

. From the perspective of
the theorem prover it is as though `fact`

were an undefined
function symbol of arity `1`

. Thus, modulo certain important
issues (see defun-mode-caveat), the introduction of this
function in `:`

`program`

mode does not imperil the soundness of the
system -- despite the fact that the termination argument for `fact`

was omitted -- because nothing of interest can be proved about
`fact`

. Indeed, we do not allow `fact`

to be used in logical
contexts such as conjectures submitted for proof.

It is possible to convert a function from `:`

`program`

mode to
`:`

`logic`

mode at the cost of proving that it is admissible. This can
be done by invoking

(verify-termination fact)which is equivalent to submitting the

`defun`

of `fact`

, again, but
in `:`

`logic`

mode.
(defun fact (n) (declare (xargs :mode :logic)) (if (or (not (integerp n)) (= n 0)) 1 (* n (fact (1- n)))))This particular event will fail because the termination argument requires that

`n`

be nonnegative. A repaired `defun`

, for example with `=`

replaced by `<=`

, will succeed, and an axiom about `fact`

will
henceforth be available.
Technically, `verify-termination`

submits a redefinition of the
`:`

`program`

mode function. This is permitted, even when
`ld-redefinition-action`

is `nil`

, because the new definition is
identical to the old (except for its `:mode`

and, possibly, other
non-logical properties).

See guard for a discussion of how to restrict the execution of
functions. Guards may be ``verified'' for functions in `:`

`logic`

mode; see verify-guards.

`:`

`program`

considered unsound
Major Section: MISCELLANEOUS

Technically speaking, in the current implementation, the execution
of functions having defun-mode `:`

`program`

may damage the ACL2 system
in a way that renders it unsound. See defun-mode for a
discussion of defun-modes. That discussion describes an imagined
implementation that is slightly different from this one. This note
explains that the current implementation is open to unsoundness.

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

The execution of a function having defun-mode `:`

`program`

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

For example, suppose you make the following `defun`

:

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

Note that the declared guard does not in fact adequately protect the
subroutines in the body of `crash`

; indeed, satisfying the guard to
`crash`

will guarantee that the `car`

expression is in violation
of its guard. Because this function is admitted in
`:`

`program`

-mode, no checks are made concerning the suitability
of the guard. Furthermore, in the current ACL2 implementation,
`crash`

is executed directly in Common Lisp. Thus if you call
`crash`

on an argument satisfying its guard you will cause an
erroneous computation to take place.

ACL2 !>(crash 7) Error: Caught fatal error [memory may be damaged] ...There is no telling how much damage is done by this errant computation. In some lisps your ACL2 job may actually crash back to the operating system. In other lisps you may be able to recover from the ``hard error'' and resume ACL2 in a damaged but apparently functional image.

THUS, HAVING A FUNCTION WITH DEFUN-MODE `:`

`PROGRAM`

IN YOUR SYSTEM
ABSOLVES US, THE ACL2 IMPLEMENTORS, FROM RESPONSIBILITY FOR THE
SOUNDNESS OF OUR SYSTEM.

Furthermore

ACL2 DOES NOT YET PROVIDE ANY MEANS OF REGAINING ASSURANCES OF
SOUNDNESS AFTER THE INTRODUCTION OF A FUNCTION IN `:`

`PROGRAM`

MODE,
EVEN IF IT IS ULTIMATELY CONVERTED TO `:`

`LOGIC`

MODE (since its
execution could have damaged the system in a way that makes it
possible to verify its termination and guards unsoundly).

Finally,

THE VAST MAJORITY OF ACL2 SYSTEM CODE IS IN `:`

`PROGRAM`

MODE AND SO ALL
BETS ARE OFF FROM BEFORE YOU START!

This hopeless state of current affairs will change, we think. We
think we have defined our functions ``correctly'' in the sense that
they can be converted, without ``essential'' modification, to
`:`

`logic`

mode. We think it very unlikely that a mis-guarded
function in `:`

`program`

mode (whether ours or yours) will cause
unsoundness without some sort of hard lisp error accompanying it.
We think that ultimately we can make it possible to execute your
functions (interpretively) without risk to the system, even when some have
`:`

`program`

mode. In that imagined implementation, code using
functions having `:`

`program`

mode would run more slowly, but safely.
These functions could be introduced into the logic ex post facto,
whereupon the code's execution would speed up because Common Lisp
would be allowed to execute it directly. We therefore ask that you
simply pretend that this is that imagined implementation, introduce
functions in `:`

`program`

mode, use them as convenient and perhaps
ultimately introduce some of them in `:`

`logic`

mode and prove their
properties. If you use the system this way we can develop (or
dismiss) this style of formal system development. BUT BE ON THE
LOOKOUT FOR SCREWUPS DUE TO DAMAGE CAUSED BY THE EXECUTION OF YOUR
FUNCTIONS HAVING `:`

`PROGRAM`

MODE!

`mutual-recursion`

Major Section: MISCELLANEOUS

Example: (DEFUNS (evenlp (x) (if (consp x) (oddlp (cdr x)) t)) (oddlp (x) (if (consp x) (evenlp (cdr x)) nil)))is equivalent toGeneral Form: (DEFUNS defuns-tuple1 ... defuns-tuplen)

(MUTUAL-RECURSION (DEFUN . defuns-tuple1) ... (DEFUN . defuns-tuplen))In fact,

`defuns`

is the more primitive of the two and
`mutual-recursion`

is just a macro that expands to a call of `defun`

after stripping off the `defun`

at the `car`

of each argument to
`mutual-recursion`

. We provide and use `mutual-recursion`

rather than
`defuns`

because by leaving the `defun`

s in place, `mutual-recursion`

forms can be processed by the Emacs `tags`

program.
See mutual-recursion.
Major Section: MISCELLANEOUS

General Form: ACL2 !>:disable-forcing ; disallow forced case splitsSee force for a discussion of forced case splits.

Disable-forcing is a macro that disables the executable
counterpart of the function symbol `force`

; see force. When
you want to disable forcing in hints, use a form such as:

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

Major Section: MISCELLANEOUS

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

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

`Disabledp`

takes one argument, an event name or a rune. In the
former case it returns the list of disabled runes associated with
that name (in the sense that the rune's ``base symbol'' is that
name; see rune). In the latter case it returns `t`

if the given
rune is disabled, and `nil`

otherwise.

`epsilon-0`

Major Section: MISCELLANEOUS

If `x`

and `y`

are both `e0-ordinalp`

s (see e0-ordinalp) then
`(e0-ord-< x y)`

is true iff `x`

is strictly less than `y`

. `e0-ord-<`

is
well-founded on the `e0-ordinalp`

s. When `x`

and `y`

are both nonnegative
integers, `e0-ord-<`

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

).

`e0-ord-<`

plays a key role in the formal underpinnings of the ACL2
logic. In order for a recursive definition to be admissible it must
be proved to ``terminate.'' By terminate we mean that the arguments to
the function ``get smaller'' as the function recurses and this sense
of size comparison must be such that there is no ``infinitely
descending'' sequence of ever smaller arguments. That is, the
relation used to compare successive arguments must be well-founded
on the domain being measured.

The most basic way ACL2 provides to prove termination requires the
user to supply (perhaps implicitly) a mapping of the argument tuples
into the ordinals with some ``measure'' expression in such a way
that the measures of the successive argument tuples produced by
recursion decrease according to the relation `e0-ord-<`

. The validity
of this method rests on the well-foundedness of `e0-ord-<`

on the
`e0-ordinalp`

s.

Without loss of generality, suppose the definition in question
introduces the function `f`

, with one formal parameter `x`

(which might
be a list of objects). Then we require that there exist a measure
expression, `(m x)`

, that always produces an `e0-ordinalp`

.
Furthermore, consider any recursive call, `(f (d x))`

, in the body of
the definition. Let `hyps`

be the conjunction terms (each of which is
either the test of an `if`

in the body or else the negation of such a
test) describing the path through the body to the recursive call in
question. Then it must be a theorem that

(IMPLIES hyps (E0-ORD-< (m (d x)) (m x))).When we say

`e0-ord-<`

is ``well-founded'' on the `e0-ordinalp`

s we
mean that there is no infinite sequence of `e0-ordinalp`

s such that
each is smaller than its predecessor in the sequence. Thus, the
theorems that must be proved about `f`

when it is introduced establish
that it cannot recur forever because each time a recursive call is
taken `(m x)`

gets smaller. From this, and the syntactic restrictions
on definitions, it can be shown (as on page 44 in ``A Computational
Logic'', Boyer and Moore, Academic Press, 1979) that there exists a
function satisfying the definition; intuitively, the value assigned
to any given `x`

by the alleged function is that computed by a
sufficiently large machine. Hence, the logic is consistent if the
axiom defining `f`

is added.See e0-ordinalp for a discussion of the ordinals and how to compare two ordinals.

The definitional principle permits the use of relations other than
`e0-ord-<`

but they must first be proved to be well-founded on some
domain. See well-founded-relation. Roughly put, alternative
relations are shown well-founded by providing an order-preserving
mapping from their domain into the ordinals. See defun for
details on how to specify which well-founded relation is to be
used.

Major Section: MISCELLANEOUS

Using the nonnegative integers and lists we can represent the
ordinals up to `epsilon-0`

. The ACL2 notion of `ordinal`

is the same as
that found in `nqthm-1992`

and both are very similar to the
development given in ``New Version of the Consistency Proof for
Elementary Number Theory'' in The Collected Papers of Gerhard
Gentzen, ed. M.E. Szabo, North-Holland Publishing Company,
Amsterdam, 1969, pp 132-213.

The following essay is intended to provide intuition about ordinals.
The truth, of course, lies simply in the ACL2 definitions of
`e0-ordinalp`

and `e0-ord-<`

.

Very intuitively, think of each non-zero natural number as by being denoted by a series of the appropriate number of strokes, i.e.,

0 0 1 | 2 || 3 ||| 4 |||| ... ...Then ``

`omega`

,'' here written as `w`

, is the ordinal that might be
written as
w |||||...,i.e., an infinite number of strokes. Addition here is just concatenation. Observe that adding one to the front of

`w`

in the
picture above produces `w`

again, which gives rise to a standard
definition of `w`

: `w`

is the least ordinal such that adding another
stroke at the beginning does not change the ordinal.
We denote by `w+w`

or `w*2`

the ```doubly infinite`

'' sequence that we
might write as follows.

w*2 |||||... |||||...One way to think of

`w*2`

is that it is obtained by replacing each
stroke in `2`

`(||)`

by `w`

. Thus, one can imagine `w*3`

, `w*4`

, etc., which
leads ultimately to the idea of ```w*w`

,'' the ordinal obtained by
replacing each stroke in `w`

by `w`

. This is also written as ```omega`

squared'' or `w^2`

, or:
2 w |||||... |||||... |||||... |||||... |||||... ...We can analogously construct

`w^3`

by replacing each stroke in `w`

by
`w^2`

(which, it turns out, is the same as replacing each stroke in
`w^2`

by `w`

). That is, we can construct `w^3`

as `w`

copies of `w^2`

,
3 2 2 2 2 w w ... w ... w ... w ... ...Then we can construct

`w^4`

as `w`

copies of `w^3`

, `w^5`

as `w`

copies of
`w^4`

, etc., ultimately suggesting `w^w`

. We can then stack `omega`

s,
i.e., `(w^w)^w`

etc. Consider the ``limit'' of all of those stacks,
which we might display as follows.
. . . w w w w wThat is epsilon-0.

Below we begin listing some ordinals up to `epsilon-0`

; the reader can
fill in the gaps at his or her leisure. We show in the left column
the conventional notation, using `w`

as ```omega`

,'' and in the right
column the ACL2 object representing the corresponding ordinal.

ordinal ACL2 representationObserve that the sequence of0 0 1 1 2 2 3 3 ... ... w '(1 . 0) w+1 '(1 . 1) w+2 '(1 . 2) ... ... w*2 '(1 1 . 0) (w*2)+1 '(1 1 . 1) ... ... w*3 '(1 1 1 . 0) (w*3)+1 '(1 1 1 . 1) ... ...

2 w '(2 . 0) ... ...

2 w +w*4+3 '(2 1 1 1 1 . 3) ... ...

3 w '(3 . 0) ... ...

w w '((1 . 0) . 0) ... ...

w 99 w +w +4w+3 '((1 . 0) 99 1 1 1 1 . 3) ... ...

2 w w '((2 . 0) . 0)

... ...

w w w '(((1 . 0) . 0) . 0) ... ...

`e0-ordinalp`

s starts with the
nonnegative integers. This is convenient because it means that if a
term, such as a measure expression for justifying a recursive
function (see e0-ord-<) must produce an `e0-ordinalp`

it suffices
for it to produce a nonnegative integer.
The ordinals listed above are listed in ascending order. This is
the ordering tested by `e0-ord-<`

.

The ```epsilon-0`

ordinals'' of ACL2 are recognized by the recursively
defined function `e0-ordinalp`

. The base case of the recursion tells
us that nonnegative integers are `epsilon-0`

ordinals. Otherwise, an
`epsilon-0`

ordinal is a `cons`

pair `(o1 . o2)`

, where `o1`

is a non-`0`

`epsilon-0`

ordinal, `o2`

is an `epsilon-0`

ordinal, and if `o2`

is not an
integer then its `car`

(which, by the foregoing, must be an `epsilon-0`

ordinal) is no greater than `o1`

. Thus, if you think of a
(non-integer) `epsilon-0`

ordinal as a list, each element is an non-`0`

`epsilon-0`

ordinal, the ordinals are listed in weakly descending
order, and the final `cdr`

of the list is an integer.

The function `e0-ord-<`

compares two `epsilon-0`

ordinals, `x`

and `y`

. If
both are integers, `e0-ord-<`

is just `x<y`

. If one is an integer and
the other is a `cons`

, the integer is the smaller. Otherwise, the
ordinals in their `car`

s are compared recursively and determines which
is smaller unless the `car`

s are equal, in which case the ordinals in
their `cdr`

s are compared.

Fundamental to ACL2 is the fact that `e0-ord-<`

is well-founded on
`epsilon-0`

ordinals. That is, there is no ``infinitely descending
chain'' of such ordinals. See proof-of-well-foundedness.

Major Section: MISCELLANEOUS

Examples: (defun hd (x) (if (consp x) (car x) 0)) (local (defthm lemma23 ...)) (progn (defun fn1 ...) (local (defun fn2 ...)) ...)An exception: an embedded event form may not set theGeneral Form: An embedded event form is a term, x, such that

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

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

x is of the form (PROGN x1 ... xn), where each xi is an embedded event form;

x is of the form (VALUE &), where & is any term;

x macroexpands to one of the forms above.

`acl2-defaults-table`

when in the context of `local`

. Thus for example,
the form
(local (table acl2-defaults-table :defun-mode :program))is not an embedded event form, nor is the form

`(local (program))`

,
since the latter sets the `acl2-defaults-table`

implicitly. An
example at the end of the discussion below illustrates why there is
this restriction.
When an embedded event is executed while `ld-skip-proofsp`

is
`'`

`include-book`

, those parts of it inside `local`

forms are ignored.
Thus,

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

`f1`

, `f2`

, and `f3`

when `ld-skip-proofsp`

is `nil`

but will
define only `f1`

and `f3`

when `ld-skip-proofsp`

is `'`

`include-book`

.
*Discussion:*

`Encapsulate`

and `include-book`

place restrictions on the kinds of
forms that may be processed. These restrictions insure that the
non-local events (which will ultimately be processed with
`ld-skip-proofs`

`t`

) are indeed admissible provided that the sequence
of local and non-local events is admissible when `ld-skip-proofs`

is
`nil`

.

`Local`

permits the hiding of an event or group of events in the sense
that local events are processed when we are trying to establish the
admissibility of a sequence of embedded events but are ignored when
we are constructing the world produced by assuming that sequence.
Thus, for example, a particularly ugly and inefficient `:`

`rewrite`

rule
might be made local to an encapsulate that ``exports'' a desirable
theorem whose proof requires the ugly lemma.

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

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

(defthm foo-is-1 (equal (foo) 1)).When we process the events with

`ld-skip-proofsp`

, `nil`

the second
`defun`

is executed and the `defthm`

succeeds. But when we process the
events with `ld-skip-proofsp`

`'`

`include-book`

, the second `defun`

is
executed, so that `foo`

no longer has the same definition it did when
we proved `foo-is-1`

. Thus, an invalid formula is assumed when we
process the `defthm`

while skipping proofs. Thus, the first form
above is not a legal embedded event form.
`Defpkg`

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

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

`my-pkg::bar`

must have been read before the
`defpkg`

for `"MY-PKG"`

was executed.
Finally, let us elaborate on the restriction mentioned earlier
related to the `acl2-defaults-table`

. Consider the following form.

(encapsulate () (local (program)) (defun foo (x) (if (equal 0 x) 0 (1+ (foo (- x))))))See local-incompatibility for a discussion of how

`encapsulate`

processes event forms. Briefly, on the first pass through the
events the definition of `foo`

will be accepted in `defun`

mode
`:`

`program`

, and hence accepted. But on the second pass the form
`(local (program))`

is skipped because it is marked as local, and
hence `foo`

is accepted in `defun`

mode `:`

`logic`

. Yet, no proof has been
performed in order to admit `foo`

, and in fact, it is not hard to
prove a contradiction from this definition!