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
nameis a new symbolic name (see name),
termis a term that when evaluated will produce a theory (see theories), and
doc-stringis an optional documentation string (see doc-string). Except for the variable
termmust contain no free variables.
Termis evaluated with
worldbound 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
The value returned is the length of the resulting theory. For example, in
the following, the theory associated with
'FOO has 54 runes:
ACL2 !>(deftheory foo (union-theories '(binary-append) (theory 'minimal-theory))) Summary Form: ( DEFTHEORY FOO ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) 54 ACL2 !>
Note that the theory being defined depends on the context. For example, consider the following (contrived) example book.
(in-package "ACL2") (defund foo (x) (consp x)) ; defund disables foo (local (in-theory (enable foo))) (deftheory my-theory (current-theory :here)) (in-theory (disable foo)) (defthm foo-property (implies (consp x) (foo x)) :hints (("Goal" :in-theory (enable my-theory))))At the time
foo-propertyis proved admissible during book certification (see certify-book), the
in-theoryevent has previously been evaluated, so the definition of
foois enabled. Thus, the
foo, and the theorem proves. HOWEVER, when the book is later included (see include-book), the
localevent is skipped, so the definition of
foois disabled at the time the theory
my-theoryis defined. Hence, unlike the case for the admissibility pass of the book's certification, that theory does not include the definition of
foowhen the book is included.
There is, however, a way to ensure that a theory defined in a book is
the same at
include-book time as it was during the admissibility pass
of the book's certification; see deftheory-static.