►Dracula: Reference Manual
▼1 ACL2
On this page:
assert$
defaxiom
deflabel
defstub
deftheory
defthm
defthmd
in-theory
include-book
mutual-recursion
theory-invariant
defconst
defun
defund
declare
defequiv
  ← prev  up  next → 

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

  ← prev  up  next →