associate a function name with a macro name
Parent topic: EVENTS Home
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.
add an axiom
Parent topic: EVENTS Home
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 f)
: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.
define a Skolem (witnessing) function
Parent topic: EVENTS Home
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.
prove that one equivalence relation preserves another in a given
argument position of a given function
Parent topic: EVENTS Home
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.
define a constant
Parent topic: EVENTS Home
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.)
add a documentation topic
Parent topic: EVENTS Home
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.
prove that a function is an equivalence relation
Parent topic: EVENTS Home
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.
introduce an evaluator function
Parent topic: EVENTS Home
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*.
build a landmark and/or add a documentation topic
Parent topic: EVENTS Home
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.
define a macro
Parent topic: EVENTS Home
Example Defmacros: (defmacro xor (x y) (list 'if x (list 'not y) y))where(defmacro git (sym key) (list 'getprop sym key nil ''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.
define a new symbol package
Parent topic: EVENTS Home
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.
prove that equiv1 refines equiv2
Parent topic: EVENTS Home
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.
stub-out a function symbol
Parent topic: EVENTS Home
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.
define a theory (to enable or disable a set of rules)
Parent topic: EVENTS Home
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).
prove and name a theorem
Parent topic: EVENTS Home
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.
define a function symbol
Parent topic: EVENTS Home
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
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 < 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))