On this page:
assert$
defaxiom
deflabel
defstub
deftheory
defthm
in-theory
include-book
mutual-recursion
theory-invariant
defconst
defun
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 ...")

  rename-below: used outside of begin-below in: (rename-below

  (sbar19 sbar))

(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)
Defines a theorem to be proved and named.

Example:

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

  rename-below: used outside of begin-below in: (rename-below

  (x+x=2x20 x+x=2x))

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

  rename-below: used outside of begin-below in: (rename-below

  (evenlp2123 evenlp21) (oddlp2224 oddlp22))

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

  rename-below: used outside of begin-below in: (rename-below

  (the-ref *PI*))

  > (* 2 *PI*)

  eval:600:0: *PI*: undefined in: *PI*

(defun name (args) (declare decl ...) ... body)
Defines a function.

Examples:

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

  rename-below: used outside of begin-below in: (rename-below

  (absolute-value2526 absolute-value25))

  > (absolute-value 5)

  compile: unbound identifier (and no #%top syntax

  transformer is bound) in: absolute-value25

  > (absolute-value -5)

  compile: unbound identifier (and no #%top syntax

  transformer is bound) in: absolute-value25

(declare d ...)
Used in defun 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))