Deftheory
Define a theory (to enable or disable a set of rules)
Example:
(deftheory interp-theory
(set-difference-theories
(universal-theory :here)
(universal-theory 'interp-section)))
General Forms:
(deftheory name term)
(deftheory name term :redundant-okp flg)
where name is a new symbolic name (see name), term is a
term that when evaluated will produce a theory (see theories), and
flg is expected to be Boolean. 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).
The value returned is the length of the resulting theory. For example, in
the following, the theory associated with 'FOO has 60 runes as of
ACL2 Version 8.6:
ACL2 !>(deftheory foo (union-theories '(binary-append)
(theory 'minimal-theory)))
Summary
Form: ( DEFTHEORY FOO ...)
Rules: NIL
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
60
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-property is proved admissible during book
certification (see certify-book), the local in-theory
event has previously been evaluated, so the definition of foo is
enabled. Thus, the :in-theory hint on foo-property will
enable foo, and the theorem proves. HOWEVER, when the book is
later included (see include-book), the local event is skipped,
so the definition of foo is disabled at the time the theory
my-theory is defined. Hence, unlike the case for the admissibility pass
of the book's certification, that theory does not include the definition of
foo when 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.
Note that a deftheory event is never redundant unless
:redundant-okp t is specified, which supports a limited form of
redundancy. See redundant-events.
Subtopics
- Rulesets
- Table-based alternative to ACL2's named theories.
- Defthy
- Define a theory (to enable or disable a set of rules)
