Major Section: EVENTS
Examples: ACL2 !>(defstub subr1 (* * state) => (mv * state)) ACL2 !>(defstub add-hash (* * hash-table) => hash-table)General Forms: (defstub name args-sig => output-sig) (defstub name args-sig => output-sig :doc doc-string)
Name is a new function symbol and (name . args-sig) => output-sig)
is a signature. If the optional doc-string is supplied
it should be a documentation string. See also the ``Old Style''
heading below.
Defstub macro expands into an encapsulate event
(see encapsulate). Thus, no axioms are available about name
but it may be used wherever a function of the given signature is
permitted.
Old Style:
Old Style General Form: (defstub name formals output) (defstub name formals output :doc doc-string)where
name is a new function symbol, 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).
Note that with the old style notation it is impossible to stub-out
a function that uses any single-threaded object other than state.
The old style is preserved for compatibility with earlier versions of
ACL2.
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).
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.
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))
Major Section: EVENTS
Examples:
(defun-sk forall-x-p-and-q (y z)
(forall x
(and (p x y z)
(q x y z))))
(defun-sk forall-x-p-and-q (y z) ; equivalent to the above
(forall (x)
(and (p x y z)
(q x y z))))
(defun-sk some-x-y-p-and-q (z)
(exists (x y)
(and (p x y z)
(q x y z))))
General Form:
(defun-sk fn (var1 ... varn) body &key doc quant-ok skolem-name thm-name)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, which must be
quantified as described below. The &key argument doc is an optional
documentation string to be associated with fn; for a description
of its form, see doc-string. The other arguments are explained
below. For a more elaborate example than those above,
see Tutorial4-Defun-Sk-Example.
The third argument, body, must be of the form
(Q bound-vars term)where:
Q is the symbol forall or exists (in the "ACL2"
package), bound-vars is a variable or true list of variables
disjoint from (var1 ... varn) and not including state, and
term is a term. The case that bound-vars is a single variable
v is treated exactly the same as the case that bound-vars is
(v).
The result of this event is to introduce a ``Skolem function,''
whose name is the keyword argument skolem-name if that is
supplied, and otherwise is the result of modifying fn by
suffixing "-WITNESS" to its name. The following definition and
the following two theorems are introduced for skolem-name
and fn in the case that bound-vars (see above) is a single
variable v. The name of the defthm event may be supplied as
the value of the keyword argument :thm-name; if it is not
supplied, then it is the result of modifying fn by suffixing
"-SUFF" to its name in the case that the quantifier is exists,
and "-NECC" in the case that the quantifier is forall.
(defun fn (var1 ... varn)
(let ((v (skolem-name var1 ... varn)))
body))
(defthm fn-suff ;in case the quantifier is EXISTS
(implies body
(fn var1 ... varn)))
(defthm fn-necc ;in case the quantifier is FORALL
(implies (not body)
(not (fn var1 ... varn))))
In the case that bound-vars is a list of at least two variables, say
(bv1 ... bvk), the definition above is the following instead, but
the theorem remains unchanged.
(defun fn (var1 ... varn)
(mv-let (bv1 ... bvk)
(skolem-name var1 ... varn)
body))
In order to emphasize that the last element of the list body is a
term, defun-sk checks that the symbols forall and exists do
not appear anywhere in it. However, on rare occasions one might
deliberately choose to violate this convention, presumably because
forall or exists is being used as a variable or because a
macro call will be eliminating ``calls of'' forall and exists.
In these cases, the keyword argument quant-ok may be supplied a
non-nil value. Then defun-sk will permit forall and
exists in the body, but it will still cause an error if there is
a real attempt to use these symbols as quantifiers.
Those who want a more flexible version of defun-sk that allows
nested quantifiers, should contact the implementors. In the
meantime, if you want to represent nested quantifiers, you have to
manage that yourself. For example, in order to represent
(forall x (exists y (p x y z)))you would use
defun-sk twice, for example as follows.
(defun-sk exists-y-p (x z) (exists y (p x y z)))(defun-sk forall-x-exists-y-p (z) (forall x (exists-y-p x z)))
Some distracting and unimportant warnings are inhibited during
defun-sk.
Defun-sk is implemented using defchoose, and hence should only
be executed in defun-mode :logic; see defun-mode and
see defchoose.
Note that this way of implementing quantifiers is not a new idea.
Hilbert was certainly aware of it 60 years ago! The ``story''
(see bibliography) explains why our use of defchoose is
appropriate, even in the presence of epsilon-0 induction.
Major Section: DEFUN-SK
The symbol exists (in the ACL2 package) represents existential
quantification in the context of a defun-sk form.
See defun-sk and see forall.
Major Section: DEFUN-SK
The symbol forall (in the ACL2 package) represents universal
quantification in the context of a defun-sk form.
See defun-sk and see exists.
Major Section: EVENTS
Examples: (encapsulate (((an-element *) => *))where each signature is as described in the documentation for signature, each signature describes a different function symbol, and each; The list of signatures above could also be written ; ((an-element (lst) t))
(local (defun an-element (lst) (if (consp lst) (car lst) nil))) (local (defthm member-equal-car (implies (and lst (true-listp lst)) (member-equal (car lst) lst)))) (defthm thm1 (implies (null lst) (null (an-element lst)))) (defthm thm2 (implies (and (true-listp lst) (not (null lst))) (member-equal (an-element lst) lst))))
(encapsulate ()
(local (defthm hack (implies (and (syntaxp (quotep x)) (syntaxp (quotep y))) (equal (+ x y z) (+ (+ x y) z)))))
(defthm nthcdr-add1-conditional (implies (not (zp (1+ n))) (equal (nthcdr (1+ n) x) (nthcdr n (cdr x))))))
General Form: (encapsulate (signature ... signature) ev1 ... evn)
evi is an embedded event form as described in
the documentation for embedded-event-form. There must be at
least one evi. The evi inside local special forms are
called ``local'' events below. Events that are not
local are sometimes said to be ``exported'' by the encapsulation.
We make the further restriction that no defaxiom event may be
introduced in the scope of an encapsulate (not even by
encapsulate or include-book events that are among the evi).
Furthermore, no non-local include-book event is permitted in the
scope of any encapsulate with a non-empty list of signatures.
To be well-formed, an encapsulate event must have the properties
that each event in the body (including the local ones) can be
successfully executed in sequence and that in the resulting theory,
each function mentioned among the signatures was introduced via a
local event and has the signature listed. In addition, the body may
contain no ``local incompatibilities'' which, roughly stated, means
that the events that are not local must not syntactically require
symbols defined by local events, except for the functions listed in
the signatures. See local-incompatibility. Finally, no
non-local recursive definition in the body may involve in its
suggested induction scheme any function symbol listed among the
signatures. See subversive-recursions.
The result of an encapsulate event is an extension of the logic
in which, roughly speaking, the functions listed in the
signatures are constrained to have the signatures listed
and to satisfy the non-local theorems proved about them. In
fact, other functions introduced in the encapsulate event may be
considered to have ``constraints'' as well. (See constraint
for details, which are only relevant to functional instantiation.)
Since the constraints were all theorems in the ``ephemeral'' or
``local'' theory, we are assured that the extension produced by
encapsulate is sound. In essence, the local definitions of
the constrained functions are just ``witness functions'' that
establish the consistency of the constraints. Because those
definitions are local, they are not present in the theory
produced by encapsulation. Encapsulate also exports all rules
generated by its non-local events, but rules generated by
local events are not exported.
The default-defun-mode for the first event in an encapsulation is
the default defun-mode ``outside'' the encapsulation. But since
events changing the defun-mode are permitted within the body of an
encapsulate, the default defun-mode may be changed. However,
defun-mode changes occurring within the body of the encapsulate
are not exported. In particular, the acl2-defaults-table after
an encapsulate is always the same as it was before the
encapsulate, even though the encapsulate body might contain
defun-mode changing events, :program and :logic.
See defun-mode. More generally, after execution of an
encapsulate event, the value of acl2-defaults-table is
restored to what it was immediately before that event was executed.
See acl2-defaults-table.
Theorems about the constrained function symbols may then be proved
-- theorems whose proofs necessarily employ only the constraints.
Thus, those theorems may be later functionally instantiated, as with
the :functional-instance lemma instance
(see lemma-instance), to derive analogous theorems about
different functions, provided the constraints (see constraint)
can be proved about the new functions.
Observe that if the signatures list is empty, encapsulate may still
be useful for deriving theorems to be exported whose proofs require
lemmas you prefer to hide (i.e., made local).
The order of the events in the vicinity of an encapsulate is
confusing. We discuss it in some detail here because when logical
names are being used with theory functions to compute sets of rules,
it is sometimes important to know the order in which events were
executed. (See logical-name and see theory-functions.)
What, for example, is the set of function names extant in the middle
of an encapsulation?
If the most recent event is previous and then you execute an
encapsulate constraining an-element with two non-local events in its
body, thm1 and thm2, then the order of the events after the
encapsulation is (reading chronologically forward): previous, thm1,
thm2, an-element (the encapsulate itself). Actually, between
previous and thm1 certain extensions were made to the world by the
superior encapsulate, to permit an-element to be used as a function
symbol in thm1.
Finally, we note that an encapsulate event is redundant if and
only if a syntactically identical encapsulate has already been
executed under the same default-defun-mode.
See redundant-events.
Major Section: EVENTS
Example:
(in-theory (set-difference-theories
(universal-theory :here)
'(flatten (:executable-counterpart flatten))))
General Form:
(in-theory term :doc doc-string)
where term is a term that when evaluated will produce a theory
(see theories), and doc-string is an optional documentation
string not beginning with ``:doc-section ...''. Except for the
variable world, term must contain no free variables. Term is
evaluated with the variable world bound to the current world to
obtain a theory and the corresponding runic theory
(see theories) is then made the current theory. Thus,
immediately after the in-theory, a rule is enabled iff its rule name
is a member of the runic interpretation (see theories) of some
member of the value of term. See theory-functions for a list
of the commonly used theory manipulation functions.
Because no unique name is associated with an in-theory event, there
is no way we can store the documentation string doc-string in our
documentation data base. Hence, we actually prohibit doc-string
from having the form of an ACL2 documentation string;
see doc-string.
Major Section: EVENTS
Examples: (include-book "my-arith") (include-book (:RELATIVE "my-arith")) (include-book "/home/smith/my-arith") (include-book (:ABSOLUTE "home" "smith" "my-arith"))whereGeneral Form: (include-book file :load-compiled-file action :doc doc-string)
file is a book name. See books for general
information, see book-name for information about book names,
and see pathname for information about file names (including
structured pathnames). Action is one of t, nil,
:warn (the default), or :try; these values are explained
below. Doc-string is an optional documentation string;
see doc-string. If the book has no certificate, if its
certificate is invalid or if the certificate was produced by a
different version of ACL2, a warning is printed and the book is
included anyway; see certificate. This can lead to serious
errors; see uncertified-books. If the portcullis of the
certificate (see portcullis) cannot be raised in the host
logical world, an error is caused and no change occurs to the
logic. Otherwise, the non-local events in file are assumed.
Then the keep of the certificate is checked to insure that
the correct files were read; see keep. A warning is printed if
uncertified books were included. Even if no warning is
printed, include-book places a burden on you;
see certificate.
If there is a compiled file for the book that was created more
recently than the book itself and the value action of the
:load-compiled-file argument is not nil, or is omitted, then
the compiled file is automatically loaded; otherwise it is not
loaded. If action is t then the compiled file must be loaded
or an error will occur, while if action is :warn (the default)
then a warning will be printed. Certify-book can be used to
compile a book. The effect of compilation is to speed up the
execution of the functions defined within the book when those
functions are applied to specific values. The presence of compiled
code for the functions in the book should not otherwise affect the
performance of ACL2. See guard for a discussion.
Include-book is similar in spirit to encapsulate in that it is
a single event that ``contains'' other events, in this case the
events listed in the file named. Include-book processes the
non-local event forms in the file, assuming that each is
admissible. Local events in the file are ignored. You may
use include-book to load multiple books, creating the logical
world that contains the definitions and theorems of all of
them.
If any non-local event of the book attempts to define a name
that has already been defined -- and the book's definition is not
syntactically identical to the existing definition -- the attempt to
include the book fails, an error message is printed, and no change
to the logical world occurs. See redundant-events for the
details.
When a book is included, the default defun-mode
(see default-defun-mode) for the first event is always
:logic. That is, the default defun-mode ``outside'' the book --
in the environment in which include-book was called -- is
irrelevant to the book. Events that change the defun-mode are
permitted within a book (provided they are not in local forms).
However, such changes within a book are not exported, i.e., at the
conclusion of an include-book, the ``outside'' default defun-mode
is always the same as it was before the include-book.
Unlike every other event in ACL2, include-book puts a burden on
you. Used improperly, include-book can be unsound in the sense
that it can create an inconsistent extension of a consistent logical
world. A certification mechanism is available to help you
carry this burden -- but it must be understood up front that even
certification is no guarantee against inconsistency here. The
fundamental problem is one of file system security.
See certificate for a discussion of the security issues.
After execution of an include-book form, the value of
acl2-defaults-table is restored to what it was immediately before
that include-book form was executed.
See acl2-defaults-table.
This concludes the guided tour through books.
See set-compile-fns for a subtle point about the interaction
between include-book and on-the-fly compilation.
See certify-book for a discussion of how to certify a book.