Define a function symbol

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

See also mutual-recursion for how to use `xargs` declarations in one

Note that ACL2 does not support the use of

The *declarations* (see declare), `mutual-recursion` (exception: a measure of `program` mode; see defun-mode.

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,

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

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

This discussion has assumed that the definition of

The final conditions on admissibility concern the termination of the
recursion. Roughly put, all applications of

The default well-founded relation is `o<`, an ``ordinal less-than''
relation (discussed further below) that reduces to ordinary

The only primitive well-founded relation in ACL2 is `o<`, which is
known to be well-founded on the `o-p`s. 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 `o<` on the `o-p`s.

For example, for our generic definition of

(o-p (m x y)).

The second shows that

(implies (not (test x y)) (o< (m (d x) y) (m x y))).

Observe that in the latter formula we must show that the ``

See o< 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, `o<` is just the familiar ``less than''
relation (`<`). Thus, it is very common to use a measure

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, `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-clause to extend
the class of trivially admissible recursive schemes.

We now turn to the question of which well-founded relation `o<`) and a domain predicate (e.g., `o-p`) on
which that relation is known to be well-founded. But, as noted elsewhere (see
well-founded-relation-rule), 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
`xargs`
for a

If no `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 `o<` (with domain predicate `o-p`).

This completes the brief sketch of the ACL2 definitional principle. Optionally, see rulers for a more detailed discussion of the termination analysis and resulting proof obligations for admissibility, as well as a discussion of the relation to how ACL2 stores induction schemes.

On very rare occasions ACL2 will seem to "hang" when processing a
definition, especially if there are many subexpressions of the body whose
function symbol is `if` (or which macroexpand to such an expression).
In those cases you may wish to supply the following to `xargs`:

When a

The following example illustrates all of the available declarations, but it
is completely nonsensical and it shows only a few of the many

(defun example (x y z a b c i j) (declare (ignore a b c) (ignorable x y) (irrelevant c) (type integer i j) (optimize (safety 3)) (xargs :guard (symbolp x) :measure (- i j) :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 :verify-guards nil :type-prescription (natp (example x y z a b c i j)))) (example-body x y z i j))

- Xargs
- Extra arguments, for example to give hints to
`defun` - Defun-mode
- Determines whether a function definition is a logical act
- Mutual-recursion
- Define some mutually recursive functions
- Defun-inline
- Define a potentially inlined function symbol and associated macro
- Rulers
- Control for ACL2's termination and induction analyses
- Defun-nx
- Define a non-executable function symbol
- Defund
- Define a function symbol and then disable it
- Set-ignore-ok
- Allow unused formals and locals without an
ignore orignorable declaration - Set-well-founded-relation
- Set the default well-founded relation
- Set-measure-function
- Set the default measure function symbol
- Set-irrelevant-formals-ok
- Allow irrelevant formals in definitions
- Defun-notinline
- Define a not-to-be-inlined function symbol and associated macro
- Set-bogus-defun-hints-ok
- Allow unnecessary
(xargs :hints ...) and measures. - Defund-nx
- Define a disabled non-executable function symbol
- Defun$
- Define a function symbol and generate a warrant
- Defund-notinline
- Define a disabled, not-to-be-inlined function symbol and associated macro
- Defnd
- disabled definition with guard
t - Defn
- Definition with guard
t - Defund-inline
- Define a potentially disabled, inlined function symbol and associated macro
- Set-bogus-measure-ok
- Allow unnecessary measures and
(xargs :hints ...) .