Major Section: EVENTS

This macro provides a variant of `deftheory`

, such that the resulting
theory is the same at `include-book`

time as it was at `certify-book`

time.

We assume that the reader is familiar with theories; see deftheory. We
begin here by illustrating how `deftheory-static`

differs from
`deftheory`

. Suppose for example that the following events are the first
two events in a book, where that book is certified in the initial ACL2
world (see ground-zero).

(deftheory my-theory (current-theory :here)) (deftheory-static my-static-theory (current-theory :here))Now suppose we include that book after executing the following event.

(in-theory (disable car-cons))Suppose that later we execute

`(in-theory (theory 'my-theory))`

. Then the
rule `car-cons`

will be disabled, because it was disabled at the time the
expression `(current-theory :here)`

was evaluated when processing the
`deftheory`

of `my-theory`

while including the book. However, if we
execute `(in-theory (theory 'my-static-theory))`

, then the rule
`car-cons`

will be enabled, because the value of the theory
`my-static-theory`

was saved at the time the book was certified.

General Form: (deftheory-static name term :doc doc-string)The arguments are handled the same as for

`deftheory`

. Thus, `name`

is
a new symbolic name (see name), `term`

is a term that when evaluated will
produce a theory (see theories), and `doc-string`

is an optional
documentation string (see doc-string). 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 `name`

. Henceforth, this runic theory is returned as the
value of the theory expression `(theory name)`

.As for `deftheory`

, the value returned is the length of the resulting
theory.

We conclude with an optional discussion about the implementation of
`deftheory-static`

, for those familiar with `make-event`

. The
following macroexpansion of the `deftheory-static`

form above shows how
this works (see trans1).

ACL2 !>:trans1 (deftheory-static my-static-theory (current-theory :here)) (MAKE-EVENT (LET ((WORLD (W STATE))) (LIST 'DEFTHEORY 'MY-STATIC-THEORY (LIST 'QUOTE (CURRENT-THEORY :HERE))))) ACL2 !>

The idea is that upon evaluation of this `make-event`

form, the first step
is to evaluate the indicated `LET`

expression to obtain a form
`(deftheory my-theory '(...))`

, where ```(...)`

'' is a list of all
runes in current theory. If this form is in a book being certified,
then the resulting `deftheory`

form is stored in the book's certificate,
and is used when the book is included later.