Major Section: EVENTS

Example: (add-macro-alias append binary-append)This example associates the function symbol

`binary-append`

with the
macro name `append`

. As a result, the name `append`

may be used as a
runic designator (see theories) by the various theory
functions. See macro-aliases-table for more details.

General Form: (add-macro-alias macro-name function-name)This is a convenient way to add an entry to

`macro-aliases-table`

.
See macro-aliases-table and also see remove-macro-alias.
Major Section: EVENTS

WARNING: We strongly recommend that you not add axioms. If at all
possible you should use `defun`

or `mutual-recursion`

to define new
concepts recursively or use `encapsulate`

to constrain them
constructively. Adding new axioms frequently renders the logic
inconsistent.

Example: (defaxiom sbar (equal t nil) :rule-classes nil :doc ":Doc-Section ...")whereGeneral Form: (defaxiom name term :rule-classes rule-classes :doc doc-string)

`name`

is a new symbolic name (see name), `term`

is a term
intended to be a new axiom, and `rule-classes`

and `doc-string`

are as
described in the corresponding documentation topics . The two keyword
arguments are optional. If `:`

`rule-classes`

is not supplied, the list
`(:rewrite)`

is used; if you wish the axiom to generate no rules,
specify `:`

`rule-classes`

`nil`

.
Major Section: EVENTS

Examples: (defchoose choose-x-for-p-and-q (x) (y z) (and (p x y z) (q x y z)))where(defchoose choose-x-for-p-and-q x (y z) ; equivalent to the above (and (p x y z) (q x y z)))

(defchoose choose-x-and-y-for-p-and-q (x y) (z) (and (p x y z) (q x y z)))

General Form: (defchoose fn (bound-var1 ... bound-varn) (free-var1 ... free-vark) doc-string ; optional body),

`fn`

is the symbol you wish to define and is a new symbolic
name (see name), `(bound-var1 ... bound-varn)`

is a list of
distinct `bound' variables (see below), `(free-var1 ... free-vark)`

is the list of formal parameters of `fn`

and is disjoint from the
bound variables, and `body`

is a term. The use of `lambda-list`

keywords (such as `&optional`

) is not allowed. The documentation
string, `doc-string`

, is optional; for a description of its form,
see doc-string.In the most common case, where there is only one bound variable, it is permissible to omit the enclosing parentheses on that variable. The effect is the same whether or not those parentheses are omitted. We describe this case first, where there is only one bound variable, and address the other case at the end.

The effect of the form

(defchoose fn bound-var (free-var1 ... free-vark) body)is to introduce a new function symbol,

`fn`

, with formal parameters
`(free-var1 ... free-vark)`

, and the following axiom stating that `fn`

picks a value of `bound-var`

so that the body will be true, if such a
value exists:
(implies body (let ((bound-var (fn free-var1 ... free-vark))) body))This axiom is ``clearly'' conservative under the conditions expressed above: the function

`fn`

merely picks out a ``witnessing''
value of `bound-var`

if there is one. The system in fact treats `fn`

very much as though it were declared in the signature of an
`encapsulate`

event, with the axiom above as the only axiom exported.If there is more than one bound variable, as in

(defchoose fn (bound-var1 ... bound-varn) (free-var1 ... free-vark) body)then

`fn`

returns `n`

multiple values, and the defining axiom is
expressed using `mv-let`

(see mv-let) as follows:
(implies body (mv-let (bound-var1 ... bound-varn) (fn free-var1 ... free-vark) body))

It is illegal for the body to return multiple values. Also, note
that the function introduced by a `defchoose`

form will return
`state' if and only if the body returns `state'; see state.

`Defchoose`

is only executed in defun-mode `:`

`logic`

;
see defun-mode.

Also see defun-sk.

Comment for logicians: As we point out in the documentation for
`defun-sk`

, `defchoose`

is ``appropriate,'' by which we mean that
it is conservative, even in the presence of `epsilon-0`

induction.
See bibliography for a reference to the ``story'' that includes
this argument.

` `

argument position of a given function
Major Section: EVENTS

Example: (defcong set-equal iff (memb x y) 2)See congruence and also see equivalence.is an abbreviation for (defthm set-equal-implies-iff-memb-2 (implies (set-equal y y-equiv) (iff (memb x y) (memb x y-equiv))) :rule-classes (:congruence))

General Form: (defcong equiv1 equiv2 term k :rule-classes rule-classes :instructions instructions :hints hints :otf-flg otf-flg :event-name event-name :doc doc)where

`equiv1`

and `equiv2`

are known equivalence relations, `term`

is a
call of a function `fn`

on the correct number of distinct variable
arguments `(fn x1 ... xn)`

, `k`

is a positive integer less than or equal
to the arity of `fn`

, and other arguments are as specified in the
documentation for `defthm`

. The `defcong`

macro expands into a call
of `defthm`

. The name of the `defthm`

event is
`equiv1-implies-equiv2-fn-k`

unless an `:event-name`

keyword argument is
supplied for the name. The term of the theorem is
(implies (equiv1 xk yk) (equiv2 (fn x1... xk ...xn) (fn x1... yk ...xn))).The rule-class

`:`

`congruence`

is added to the `rule-classes`

specified,
if it is not already there. All other arguments to the generated
`defthm`

form are as specified by the keyword arguments above.
Major Section: EVENTS

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

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

Major Section: EVENTS

Examples: (defdoc interp-section ":Doc-Section ...")whereGeneral Form: (defdoc name doc-string)

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

Major Section: EVENTS

Example: (defequiv set-equal)See equivalence.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))

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.
Major Section: EVENTS

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.

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 (1)-(4) and (k):

(1) How to ev a variable symbol: (implies (symbolp x) (equal (ev x a) (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 result of applying `union-theories`

to two lists: the
function symbols supplied, and the value of the constant
`*defevaluator-form-base-theory*`

.
Major Section: EVENTS

Examples: (deflabel interp-section :doc ":Doc-Section ...")whereGeneral Form: (deflabel name :doc doc-string)

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

Major Section: EVENTS

Example Defmacros: (defmacro xor (x y) (list 'if x (list 'not y) y))where(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)

`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 variables
not among the macro's arguments. See the `git`

example above.

Major Section: EVENTS

Example: (defpkg "MY-PKG" (union-eq *acl2-exports* *common-lisp-symbols-from-main-lisp-package*))whereGeneral Form: (defpkg "name" term doc-string)

`"name"`

is a (case-sensitive) string that names the
package to be created, `term`

is a variable-free expression that
evaluates to a list of symbols (no two of which 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.
`defpkg`

forms can be entered at the top-level of the ACL2 command
loop. They should occur in a file only if the file is not to be
compiled and contains nothing besides `defpkg`

and `in-package`

forms.

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 imports list 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 imports. That is, it is permissible to execute
``redundant'' `defpkg`

commands. The redundancy test is based on the
values of the two import forms, not on the forms themselves.

`equiv1`

refines `equiv2`

Major Section: EVENTS

Example: (defrefinement equiv1 equiv2)See refinement.is an abbreviation for (defthm equiv1-refines-equiv2 (implies (equiv1 x y) (equiv2 x y)) :rule-classes (: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.
Major Section: EVENTS

Examples: ACL2 !>(defstub subr1 (x y state) (mv t state)) ACL2 !>(defstub subr2 (x y) t)whereGeneral Forms: (defstub name formals output) (defstub name formals output :doc doc-string)

`name`

is the name of the function to be stubbed out, `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).
`Defstub`

actually generates an `encapsulate`

event
(see encapsulate). Thus, no axioms are available about `name`

but it may be used wherever a function of its arity, multiplicity,
and state characteristics is permitted.

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.

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