This is documentation for ACL2 Version 3.2
Copyright (C) 2007  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.

DEFCONST    define a constant

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

     General Form:
     (defconst name term doc-string)

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

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

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

DEFDOC    add a documentation topic

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

     General Form:
     (defdoc name doc-string)

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

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

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

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

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

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

DEFEQUIV    prove that a function is an equivalence relation

     Example:
     (defequiv set-equal)

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

See EQUIVALENCE.

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

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

DEFEVALUATOR    introduce an evaluator function

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

See META.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

DEFEXEC    attach a terminating executable function to a definition

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

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

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

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

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

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

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

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

     Example:

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

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

The above example macroexpands to the following.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

     Subgoal 1
     (EQUAL A A).

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

     Q.E.D.

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

     Proof succeeded.
     ACL2 !>

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

The general form is as follows.

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

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

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

The :supporters argument will often be nil.  In general, it is a true
list of symbols, all of which must be function symbols in the current
ACL2 world at the time the define-trusted-clause-processor form is
evaluated.  It is important that this list include user-defined
functions whose definitions support the correctness of the
clause-processor function.  Otherwise, local definitions of those
missing supporters can render the use of this clause-processor unsound,
as discussed in the paper referenced at the end of the clause-processor
documentation topic.

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

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

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

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

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

*A remark on the underlying implementation*

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

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

DEFLABEL    build a landmark and/or add a documentation topic

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

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

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

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

DEFMACRO    define a macro

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

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

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

     Example Expansions:
     term                    macroexpansion

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

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

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

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

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

where name is a new symbolic name (see NAME), macro-args
specifies the formals of the macro (see MACRO-ARGS for a
description), and body is a term.  Doc-string is an optional
documentation string; see DOC-STRING.  Each dcl is an optional
declaration (see DECLARE) except that the only xargs keyword
permitted by defmacro is :guard.

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

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

DEFPKG    define a new symbol package

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

     * Menu:

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

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

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

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

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

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

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

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

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

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

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

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

The Common Lisp function intern is weakly supported by ACL2.  See
INTERN.

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

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

HIDDEN-DEATH-PACKAGE    handling defpkg events that are local

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

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

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

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

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

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

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

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

HIDDEN-DEFPKG    handling defpkg events that are local

See HIDDEN-DEATH-PACKAGE

DEFREFINEMENT    prove that equiv1 refines equiv2

     Example:
     (defrefinement equiv1 equiv2)

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

See REFINEMENT.

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

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