ADD-MACRO-ALIAS

associate a function name with a macro name
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.













































































DEFAXIOM

add an axiom
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 ...")

General Form: (defaxiom name term :rule-classes rule-classes :doc doc-string)

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













































































DEFCHOOSE

define a Skolem (witnessing) function
Major Section:  EVENTS

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

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

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













































































DEFCONG

prove that one equivalence relation preserves another in a given argument position of a given function
Major Section:  EVENTS

Example:
(defcong set-equal iff (memb x y) 2)

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

See congruence and also see equivalence.

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.













































































DEFCONST

define a constant
Major Section:  EVENTS

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

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

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













































































DEFLABEL

build a landmark and/or add a documentation topic
Major Section:  EVENTS

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

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













































































DEFPKG

define a new symbol package
Major Section:  EVENTS

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

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

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













































































DEFREFINEMENT

prove that equiv1 refines equiv2
Major Section:  EVENTS

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.













































































DEFSTUB

stub-out a function symbol
Major Section:  EVENTS

Examples:
ACL2 !>(defstub subr1 (x y state) (mv t state))
ACL2 !>(defstub subr2 (x y) t)

General Forms: (defstub name formals output) (defstub name formals output :doc doc-string)

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













































































DEFTHEORY

define a theory (to enable or disable a set of rules)
Major Section:  EVENTS

Example:
(deftheory interp-theory
           (set-difference-theories
             (universal-theory :here)
             (universal-theory 'interp-section)))

General Form: (deftheory name term :doc doc-string)

where 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 runic theory (see theories) and associated with name. Henceforth, this runic theory is returned as the value of the theory expression (theory name).













































































DEFTHM

prove and name a theorem
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]")

General Form: (defthm name term :rule-classes rule-classes :instructions instructions :hints hints :otf-flg otf-flg :doc doc-string)

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













































































DEFUN

define a function symbol
Major Section:  EVENTS

Examples:
(defun app (x y)
  (if (consp x)
      (cons (car x) (app (cdr x) y))
      y))

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

where fn is the symbol you wish to define and is a new symbolic name (see name), (var1 ... varn) is its list of formal parameters (see name), and body is its body. 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-ordinalps (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-ordinalps.

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