On this page:
assert$
defaxiom
deflabel
defstub
deftheory
defthm
defthmd
in-theory
include-book
mutual-recursion
theory-invariant
defconst
defun
defund
declare
defequiv

1.3 Events and Definitions

ACL2 events are special terms which define new functions or logical rules. Defined names are in scope within their own definition and below; forward references are not allowed. Use the mutual-recursion event for mutually recursive functions.

(assert$ test form)
Raises an error if the given test fails.

Examples:

  > (assert$ (< 0 1) t)

  't

  > (assert$ (< 1 0) t)

  assert$: Assertion failed!

  (< 1 0)

(defaxiom name term :rule-classes rule-classes :doc doc-string)
Defines an axiom. Using defaxiom is not recommended.

Example:

  > (defaxiom sbar (equal t nil)
              :rule-classes nil
              :doc ":Doc-Section ...")

(deflabel name :doc doc-string)
Defines a label, for adding a landmark and/or adding a documentation topic.

Example:

  > (deflabel interp-section
              :doc ":Doc-Section ...")

(defstub name args-sig => output-sig :doc doc-string)

(deftheory name term :doc doc-string)
Defines a theory (to enable or disable a set of rules)

Example:

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

(defthm name term
:rule-classes rule-classes
:instructions instructions
:hints        hints
:otf-flg      otf-flg
:doc          doc-string)
(defthmd name term
:rule-classes rule-classes
:instructions instructions
:hints        hints
:otf-flg      otf-flg
:doc          doc-string)
These two forms both define a theorem to be proved and named. The defthm form defines an enabled function that will be automatically used in subsequent proof attempts. The defthmd form defines a disabled function that must be explicitly mentioned in hints.

Examples:

  > (defthm x+x=2x (= (+ x x) (* 2 x)))
  > (defthmd x=1x (= x (* 1 x)))

(in-theory term :doc doc-string)

Example:

  > (in-theory (set-difference-theories
                 (universal-theory :here)
                 '(flatten (:executable-counterpart flatten))))

(include-book "<basename>")
(include-book "<basename>" :dir :system)
(include-book "<basename>" :dir :teachpacks)
The include-book form imports definitions from a file called a book. Dracula supports three variants.

  (include-book "my-path/my-book")
Without a :dir option, Dracula adds a ".lisp" extension to the base name and attempts to load a file relative to the current directory. In the case above, the program must reside in a directory with a "my-path" subdirectory containing a book named "my-book.lisp".

Books must be valid Dracula programs; they must start with (in-package "ACL2"); and they must contain only events, no top-level expressions.

  (include-book "my-path/my-book" :dir :system)
This variant loads a book from the system directory included with an ACL2 installation. Dracula simulates only a couple of the definitions from these books, but allows other books to be included for theorem proving purposes. See ACL2 Books for the list of books supported by Dracula.

  (include-book "my-path/my-book" :dir :teachpack)
The third variant loads one of the books provided with Dracula, called teachpacks. These books make use of DrScheme features such as interactive animations and other i/o, and are also reflected in the ACL2 logic. See Teachpacks for the list of provided teachpacks.

(mutual-recursion def1 ... defn)
For defining mutually-recursive functions.

Example:

  > (mutual-recursion
     (defun evenlp (x)
       (if (consp x) (oddlp (cdr x)) t))
     (defun oddlp (x)
       (if (consp x) (evenlp (cdr x)) nil)))

  eval:599:0: mutual-recursion: defined outside of

  begin-below at: HERE in: (mutual-recursion (defun evenlp

  (x) (if (consp x) (oddlp (cdr x)) t)) (defun oddlp (x) (if

  (consp x) (evenlp (cdr x)) nil)))

(theory-invariant term :key key :error t/nil)

(defconst name val)
Defines a constant value. The name must begin and end with asterisks.

Examples:

  > (defconst *PI* 22/7)

  eval:600:0: defconst: defined outside of begin-below at:

  here in: (defconst *PI* 22/7)

  > (* 2 *PI*)

  eval:601:0: application: bad syntax in: (top/error . *PI*)

(defun name (args) (declare decl ...) ... body)
(defund name (args) (declare decl ...) ... body)
These two forms both define a function. The defun form defines a logically-enabled function, about which proof attempts can reason automatically. The defund form defines a logically-disabled function, about which proof attempts may only reason if given a hint.

Examples:

  > (defun absolute-value (x)
      (cond
        ((< x 0) (* -1 x))
        (t x)))

  eval:602:0: defun: defined outside of begin-below at: HERE

  in: (defun absolute-value (x) (cond ((< x 0) (* -1 x)) (t

  x)))

  > (absolute-value 5)

  eval:603:0: application: bad syntax in: (top/error .

  absolute-value)

  > (absolute-value -5)

  eval:604:0: application: bad syntax in: (top/error .

  absolute-value)

  > (defun square-of (x)
      (* x x))

  eval:605:0: defun: defined outside of begin-below at: HERE

  in: (defun square-of (x) (* x x))

  > (square-of 3)

  eval:606:0: application: bad syntax in: (top/error .

  square-of)

  > (square-of -3)

  eval:607:0: application: bad syntax in: (top/error .

  square-of)

(declare d ...)
Used in defun and defund to give ACL2 extra information about a function.

(defequiv pred)
Declares pred to be an equivalence predicate. It is equivalent to the following, with the supplied name substituted for pred in all identifiers:
  (defthm pred-is-an-equivalence
    (and (booleanp (pred x y))
         (pred x x)
         (implies (pred x y) (pred y x))
         (implies (and (pred x y)
                       (pred y z))
                  (pred x z)))
    :rule-classes (:equivalence))