Major Section: ACL2 Documentation

Example: '((:definition app) ; or (:d app) (:executable-counterpart app) (:i app) rv (rv) assoc-of-app)See:

### ACTIVE-RUNEP -- check that a rune exists and is enabled

### CURRENT-THEORY -- currently enabled rules as of logical name

### DEFTHEORY -- define a theory (to enable or disable a set of rules)

### DEFTHEORY-STATIC -- define a `static' theory (to enable or disable a set of rules)

### DISABLE -- deletes names from current theory

### E/D -- enable/disable rules

### ENABLE -- adds names to current theory

### EXECUTABLE-COUNTERPART-THEORY -- executable counterpart rules as of logical name

### FUNCTION-THEORY -- function symbol rules as of logical name

### GROUND-ZERO -- enabled rules in the startup theory

### IN-THEORY -- designate ``current'' theory (enabling its rules)

### INCOMPATIBLE -- declaring that two rules should not both be enabled

### INTERSECTION-THEORIES -- intersect two theories

### MINIMAL-THEORY -- a minimal theory to enable

### RULE-NAMES -- How rules are named.

### RUNE -- a rule name

### SET-DIFFERENCE-THEORIES -- difference of two theories

### THEORIES-AND-PRIMITIVES -- warnings from disabling certain built-in functions

### THEORY -- retrieve named theory

### THEORY-FUNCTIONS -- functions for obtaining or producing theories

### UNION-THEORIES -- union two theories

### UNIVERSAL-THEORY -- all rules as of logical name

A theory is a list of ``runic designators'' as described below. Each runic
designator denotes a set of ``runes'' (see rune) and by unioning together
the runes denoted by each member of a theory we define the set of runes
corresponding to a theory. Theories are used to control which rules are
``enabled,'' i.e., available for automatic application by the theorem
prover. There is always a ``current'' theory. A rule is enabled
precisely if its rune is an element of the set of runes
corresponding to the current theory. At the top-level, the current theory is
the theory selected by the most recent `in-theory`

event, extended with
the rule names introduced since then. Inside the theorem prover, the
`:`

`in-theory`

hint (see hints) can be used to select a particular
theory as current during the proof attempt for a particular goal.

Theories are generally constructed by ``theory expressions.'' Formally, a
theory expression is any term, containing at most the single free variable
`world`

, that when evaluated with `world`

bound to the current ACL2
world (see world) produces a theory. ACL2 provides various functions for
the convenient construction and manipulation of theories. These are called
``theory functions''(see theory-functions). For example, the theory
function `union-theories`

takes two theories and produces their union.
The theory function `universal-theory`

returns the theory containing all
known rule names as of the introduction of a given logical name. But a
theory expression can contain constants, e.g.,

'(len (len) (:rewrite car-cons) car-cdr-elim)and user-defined functions. The only important criterion is that a theory expression mention no variable freely except

`world`

and evaluate to a
theory.More often than not, theory expressions typed by the user do not mention the
variable `world`

. This is because user-typed theory expressions are
generally composed of applications of ACL2's theory functions. These
``functions'' are actually macros that expand into terms in which `world`

is used freely and appropriately. Thus, the technical definition of ``theory
expression'' should not mislead you into thinking that interestng theory
expressions must mention `world`

; they probably do and you just didn't
know it!

One aspect of this arrangement is that theory expressions cannot generally be
evaluated at the top-level of ACL2, because `world`

is not bound. To see
the value of a theory expression, `expr`

, at the top-level, type

ACL2 !>(LET ((WORLD (W STATE))) expr).However, because the built-in theories are quite long, you may be sorry you printed the value of a theory expression!

A theory is a true list of runic designators and to each theory there corresponds a set of runes, obtained by unioning together the sets of runes denoted by each runic designator. For example, the theory constant

'(len (len) (:e nth) (:rewrite car-cons) car-cdr-elim)corresponds to the set of runes

{(:definition len) (:induction len) (:executable-counterpart len) (:executable-counterpart nth) (:elim car-cdr-elim) (:rewrite car-cons)} .Observe that the theory contains five elements but its runic correspondent contains six. That is because runic designators can denote sets of several runes, as is the case for the first designator,

`len`

. If the above
theory were selected as current then the six rules named in its runic
counterpart would be enabled and all other rules would be disabled.We now precisely define the runic designators and the set of runes
denoted by each. When we refer below to the ``macro-aliases dereference of''
a symbol, `symb`

, we mean the (function) symbol corresponding `symb`

in
the macro-aliases-table if there is such a symbol, else `symb`

itself;
see macro-aliases-table. For example, the macro-aliases dereference of
`append`

is `binary-append`

, and the macro-aliases dereference of
`nth`

is `nth`

.

o A rune is a runic designator and denotes the singleton set containing that rune.

o Suppose that

`symb`

is a symbol and`symb'`

is the macro-aliases dereference of`symb`

, where`symb'`

is a function symbol introduced with a`defun`

(or`defuns`

) event. Then`symb`

is a runic designator and denotes the set containing the runes`(:definition symb')`

and`(:induction symb')`

, omitting the latter if no such induction rune exists (presumably because the definition of`symb'`

is not singly recursive).o Suppose that

`symb`

is a symbol and`symb'`

is the macro-aliases dereference of`symb`

, where`symb'`

is a function symbol introduced with a`defun`

(or`defuns`

) event. Then`(symb)`

is a runic designator and denotes the singleton set containing the rune`(:executable-counterpart symb')`

.o If

`symb`

is the name of a`defthm`

(or`defaxiom`

) event that introduced at least one rule, then`symb`

is a runic designator and denotes the set of the names of all rules introduced by the named event.o If

`str`

is the string naming some`defpkg`

event and`symb`

is the symbol returned by`(intern str "ACL2")`

, then`symb`

is a runic designator and denotes the singleton set containing`(:rewrite symb)`

, which is the name of the rule stating the conditions under which the`symbol-package-name`

of`(intern x str)`

is`str`

.o If

`symb`

is the name of a`deftheory`

event, then`symb`

is a runic designator and denotes the runic theory corresponding to`symb`

.o Finally, suppose that

`symb`

is a symbol and`symb'`

is the macro-aliases dereference of`symb`

. Then`(:KWD symb . rest)`

is a runic designator if`(:KWD' symb' . rest)`

is a rune, where`:KWD`

is one of`:d`

,`:e`

,`:i`

, or`:t`

, and correspondingly`:KWD'`

is`:definition`

,`:executable-counterpart`

,`:induction`

, or`:type-prescription`

, respectively. In this case,`(:KWD symb . rest)`

denotes the runic theory corresponding to the rune`(:KWD' symb' . rest)`

.

Note that including a function name, e.g., `len`

, in the current
theory enables that function but does not enable the executable
counterpart. Similarly, including `(len)`

or `(:e len)`

enables the
executable counterpart but not the symbolic definition. And including the
name of a proved lemma enables all of the rules added by the event. Of
course, one can include explicitly the runes naming the rules in
question and so can avoid entirely the use of non-runic elements in theories.

Because a rune is a runic designator denoting the set containing that
rune, a list of runes is a theory and denotes itself. We call such
theories ``runic theories.'' To every theory there corresponds a runic
theory obtained by unioning together the sets denoted by each designator in
the theory. When a theory is selected as ``current'' it is actually its
runic correspondent that is effectively used. That is, a rune is
enabled iff it is a member of the runic correspondent of the current
theory. The value of a theory defined with `deftheory`

is the runic
correspondent of the theory computed by the defining theory expression. The
theory manipulation functions, e.g., `union-theories`

, actually convert
their theory arguments to their runic correspondents before performing the
required set operation. The manipulation functions always return runic
theories. Thus, it is sometimes convenient to think of
(non-runic) theories as merely abbreviations for their runic
correspondents, abbreviations which are ``expanded'' at the first
opportunity by theory manipulation functions and the ``theory
consumer'' functions such as `in-theory`

and `deftheory`

.