stub-out a function symbol
Major Section:  EVENTS

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.


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

(deftheory interp-theory
             (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
Major Section:  EVENTS

(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)
                :induct (and (nth n a) (nth n b))
                :use ((:instance assoc-of-append
                                 (x a) (y b) (z c))
                        (: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
Major Section:  EVENTS

(defun app (x y)
  (if (consp x)
      (cons (car x) (app (cdr x) 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)
                           :induct (and (nth n a) (nth n b))
                           :use ((:instance assoc-of-append
                                            (x a) (y b) (z c))
                                   (: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))


define a function whose body has an outermost quantifier
Major Section:  EVENTS

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

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

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.


existential quantifier
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.


universal quantifier
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.


constrain some functions and/or hide some events
Major Section:  EVENTS

(encapsulate (((an-element *) => *))

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

where each signature is as described in the documentation for signature, each signature describes a different function symbol, and each 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.


designate ``current'' theory (enabling its rules)
Major Section:  EVENTS

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


load the events in a file
Major Section:  EVENTS

(include-book "my-arith")
(include-book (:RELATIVE "my-arith"))
(include-book "/home/smith/my-arith")
(include-book (:ABSOLUTE "home" "smith" "my-arith"))

General Form: (include-book file :load-compiled-file action :doc doc-string)

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