# THEORIES

sets of runes to enable/disable in concert
```Major Section:  ACL2 Documentation
```

```Example: '((:definition app)
(:executable-counterpart app)
rv
(rv)
assoc-of-app)
```
See:

• ### 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.,

```'(assoc (assoc) (: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

```   '(assoc (assoc) (:rewrite car-cons) car-cdr-elim)
```
corresponds to the set of runes
```   {(:definition assoc)
(:executable-counterpart assoc)
(:rewrite car-cons)
(:rewrite car-cdr-elim)
(:elim car-cdr-elim)} .
```
Observe that the theory contains four elements but its runic correspondent contains five. That is because some designators denote sets of several runes. If the above theory were selected as current then the five 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.

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

o If `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 `(:definition symb)`.

o If `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`.

These conventions attempt to implement the Nqthm-1992 treatment of theories. For example, including a function name, e.g., `assoc`, in the current theory enables that function but does not enable the executable counterpart. Similarly, including `(assoc)` enables the executable counterpart (Nqthm's `*1*assoc`) but not the symbolic definition. And including the name of a proved lemma enables all of the rules added by the event. These conventions are entirely consistent with Nqthm usage. Of course, in ACL2 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`.

## CURRENT-THEORY

currently enabled rules as of logical name
```Major Section:  THEORIES
```

```Examples:
(current-theory :here)
(current-theory 'lemma3)
```
See logical-name.

```General Form:
(current-theory logical-name)
```
Returns the current theory as it existed immediately after the introduction of `logical-name` provided it is evaluated in an environment in which the variable symbol WORLD is bound to the current ACL2 logical world, `(w state)`. Thus,
```ACL2 !>(current-theory :here)
```
will cause an (unbound variable) error while
```ACL2 !>(let ((world (w state))) (current-theory :here))
```
will return the current theory in world.

See theories and see logical-name for a discussion of theories in general and why the commonly used ``theory functions'' such as `current-theory` are really macros that expand into terms involving the variable `world`.

The theory returned by `current-theory` is in fact the theory selected by the `in-theory` event most recently preceding logical name, extended by the rules introduced up through `logical-name`.

You may experience a fencepost problem in deciding which logical name to use. `Deflabel` can always be used to mark unambiguously for future reference a particular point in the development of your theory. The order of events in the vicinity of an `encapsulate` is confusing. See encapsulate.

This ``function'' is actually a macro that expands to a term mentioning the single free variable `world`. When theory expressions are evaluated by `in-theory` or the `:``in-theory` hint, `world` is bound to the current ACL2 world.

## DISABLE

deletes names from current theory
```Major Section:  THEORIES
```

```Example:
(disable fact (fact) associativity-of-app)

General Form:
(disable name1 name2 ... namek)
```
where each `namei` is a runic designator; see theories. The result is the theory that contains all the names in the current theory except those listed. Note that this is merely a function that returns a theory. The result is generally a very long list of runes and you will probably regret printing it.

The standard way to ``disable'' a fixed set of names, is:

```(in-theory (disable name1 name2 ... namek)) ; globally
:in-theory (disable name1 name2 ... namek)  ; locally
```
Note that all the names are implicitly quoted. If you wish to disable a computed list of names, `lst`, use the theory expression `(set-difference-theories (current-theory :here) lst)`.

## ENABLE

```Major Section:  THEORIES
```

```Example:
(enable fact (fact) associativity-of-app)

General Form:
(enable name1 name2 ... namek)
```
where each `namei` is a runic designator; see theories. The result is the theory that contains all the names in the current theory plus those listed. Note that this is merely a function that returns a theory. The result is generally a very long list of runes and you will probably regret printing it.

The standard way to ``enable'' a fixed set of names, is

```(in-theory (enable name1 name2 ... namek)) ; globally
:in-theory (enable name1 name2 ... namek)  ; locally
```
Note that all the names are implicitly quoted. If you wish to enable a computed list of names, `lst`, use the theory expression `(union-theories (current-theory :here) lst)`.

## EXECUTABLE-COUNTERPART-THEORY

executable counterpart rules as of logical name
```Major Section:  THEORIES
```

```Examples:
(executable-counterpart-theory :here)
(executable-counterpart-theory 'lemma3)
```
See logical-name.

```General Form:
(executable-counterpart-theory logical-name)
```
Returns the theory containing all the `:``executable-counterpart` runes, whether enabled or not, that existed immediately after `logical-name` was introduced. See the documentation for theories, logical-name, executable-counterpart and `function-theory`.

You may experience a fencepost problem in deciding which logical name to use. `Deflabel` can always be used to mark unambiguously for future reference a particular point in the development of your theory. The order of events in the vicinity of an `encapsulate` is confusing. See encapsulate.

This ``function'' is actually a macro that expands to a term mentioning the single free variable `world`. When theory expressions are evaluated by `in-theory` or the `:``in-theory` hint, `world` is bound to the current ACL2 world.

## FUNCTION-THEORY

function symbol rules as of logical name
```Major Section:  THEORIES
```

```Examples:
(function-theory :here)
(function-theory 'lemma3)
```
See logical-name.

```General Form:
(function-theory logical-name)
```
Returns the theory containing all the `:``definition` runes, whether enabled or not, that existed immediately after `logical-name` was introduced. See the documentation for theories, logical-name and `executable-counterpart-theory`.

You may experience a fencepost problem in deciding which logical name to use. `Deflabel` can always be used to mark unambiguously for future reference a particular point in the development of your theory. The order of events in the vicinity of an `encapsulate` is confusing. See encapsulate.

This ``function'' is actually a macro that expands to a term mentioning the single free variable `world`. When theory expressions are evaluated by `in-theory` or the `:``in-theory` hint, `world` is bound to the current ACL2 world.

## GROUND-ZERO

enabled rules in the startup theory
```Major Section:  THEORIES
```

ACL2 concludes its initialization `(boot-strapping)` procedure by defining the theory `ground-zero`; see theories. In fact, this theory is just the theory defined by `(current-theory :here)` at the conclusion of initialization; see current-theory.

Note that by executing the event

```(in-theory (current-theory 'ground-zero))
```
you can restore the current theory to its value at the time you started up ACL2.

## INCOMPATIBLE

declaring that two rules should not both be enabled
```Major Section:  THEORIES
```

```Example:
(theory-invariant (incompatible (:rewrite left-to-right)
(:rewrite right-to-left)))

General Form:
(incompatible rune1 rune2)
```
where `rune1` and `rune2` are two specific runes. The arguments are not evaluated. `Invariant` is just a macro that expands into a term that checks that `theory` does not contain both runes. See theory-invariant.

## INTERSECTION-THEORIES

intersect two theories
```Major Section:  THEORIES
```

```Example:
(intersection-theories (current-theory :here)
(theory 'arith-patch))

General Form:
(intersection-theories th1 th2)
```
where `th1` and `th2` are theories (see theories). To each of the arguments there corresponds a runic theory. This function returns the intersection of those two runic theories, represented as a list and ordered chronologically.

This ``function'' is actually a macro that expands to a term mentioning the single free variable `world`. When theory expressions are evaluated by `in-theory` or the `:``in-theory` hint, `world` is bound to the current ACL2 world.

## RULE-NAMES

How rules are named.
```Major Section:  THEORIES
```

```Examples:
(:rewrite assoc-of-app)
(:linear delta-aref . 2)
(:definition length)
(:executable-counterpart length)
```

See rune.

## RUNE

a rule name
```Major Section:  THEORIES
```

```Examples:
(:rewrite assoc-of-app)
(:linear delta-aref . 2)
(:definition length)
(:executable-counterpart length)
```

Background: The theorem prover is driven from a data base of rules. The most common rules are `:``rewrite` rules, which cause the simplifier to replace one term with another. Events introduce rules into the data base. For example, a `defun` event may introduce as many as four rules: one for symbolically replacing a function call by its instantiated body, one for evaluating the function on constants, and two for determining the type of a call of the function (one of which is deduced before guard verification and the other of which is deduced after guard verification). `Defthm` may introduce several rules, one for each of the rule classes specified.

Every rule in the system has a name. Each name is a structured object called a ``rune,'' which is short for ``rule name''. Runes are always of the form `(:token symbol . x)`, where `:token` is some keyword symbol indicating what kind of rule is named, `symbol` is the event name that created the rule (and is called the ``base symbol'' of the rune), and `x` is either `nil` or a natural number that makes the rule name unique.

For example, an event of the form

```(defthm name thm
:rule-classes ((:REWRITE :COROLLARY term1)
(:REWRITE :COROLLARY term2)
(:ELIM    :COROLLARY term3)))
```
creates three rules, each with a unique rune. The runes are
```(:REWRITE name . 1), (:REWRITE name . 2), and (:ELIM name).
```
The function `corollary` will return the corollary term associated with a given rune in a given world. Example:
```(corollary '(:TYPE-PRESCRIPTION DIGIT-TO-CHAR) (w state))
```
However, the preferred way to see the corollary term associated with a rune or a name is to use `:pf`; see pf.

The `defun` event creates as many as four rules. `(:definition fn)` is the rune given to the equality axiom defining the function, `fn`. `(:executable-counterpart fn)` is the rune given to the rule for computing `fn` on known arguments. A type prescription rule may be created under the name `(:type-prescription fn)`, and an induction rule may be created under the name `(:induction fn)`.

Runes may be individually enabled and disabled, according to whether they are included in the current theory. See theories. Thus, it is permitted to disable `(:elim name)`, say, while enabling the other rules derived from name. Similarly, `(:definition fn)` may be disabled while `(:executable-counterpart fn)` and the type prescriptions for `fn` are enabled.

Associated with most runes is the formula justifying the rule named. This is called the ``corollary formula'' of the rune and may be obtained via the function `corollary`, which takes as its argument a rune and a property list world. Also see pf. The corollary formula for `(:rewrite name . 1)` after the `defthm` event above is `term1`. The corollary formulas for `(:definition fn)` and `(:executable-counterpart fn)` are always identical: the defining axiom. Some runes, e.g., `(:definition car)`, do not have corollary formulas. `Corollary` returns `nil` on such runes. In any case, the corollary formula of a rune, when it is non-`nil`, is a theorem and may be used in the `:use` and `:by` hints.

Note: The system has many built in rules that, for regularity, ought to have names but don't because they can never be disabled. One such rule is that implemented by the linear arithmetic package. Because many of our subroutines are required by their calling conventions to return the justifying rune, we have invented the notion of ``fake runes.'' Fake runes always have the base symbol `nil`, use a keyword token that includes the phrase ``fake-rune'', and are always enabled. For example, `(:fake-rune-for-linear nil)` is a fake rune. Occasionally the system will print a fake rune where a rune is expected. For example, when the linear arithmetic fake rune is reported among the rules used in a proof, it is an indication that the linear arithmetic package was used. However, fake runes are not allowed in theories, they cannot be enabled or disabled, and they do not have associated corollary formulas. In short, despite the fact that the user may sometimes see fake runes printed, they should never be typed.

## SET-DIFFERENCE-THEORIES

difference of two theories
```Major Section:  THEORIES
```

```Example:
(set-difference-theories (current-theory :here)
'(fact (fact)))

General Form:
(set-difference-theories th1 th2)
```
where `th1` and `th2` are theories (see theories). To each of the arguments there corresponds a runic theory. This function returns the set-difference of those two runic theories, represented as a list and ordered chronologically. That is, a rune is in the result iff it is in the first runic theory but not in the second.

The standard way to ``disable'' a theory, `lst`, is: `(in-theory (set-difference-theories (current-theory :here) lst))`.

This ``function'' is actually a macro that expands to a term mentioning the single free variable `world`. When theory expressions are evaluated by `in-theory` or the `:``in-theory` hint, `world` is bound to the current ACL2 world.

## THEORY

retrieve named theory
```Major Section:  THEORIES
```

```Example:
(theory 'my-theory)

General Form:
(theory name)
```
where `name` is the name of a previously executed `deftheory` event. Returns the named theory. See theories.

This ``function'' is actually a macro that expands to a term mentioning the single free variable `world`. When theory expressions are evaluated by `in-theory` or the `:``in-theory` hint, `world` is bound to the current ACL2 world.

## THEORY-FUNCTIONS

functions for obtaining or producing theories
```Major Section:  THEORIES
```

```Example Calls of Theory Functions:
(universal-theory :here)
(union-theories th1 th2)
(set-difference-theories th1 th2)
```
The theory functions are documented individually:

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

The functions (actually, macros) mentioned above are convenient ways to produce theories. (See theories.) Some, like `universal-theory`, take a logical name (see logical-name) as an argument and return the relevant theory as of the time that name was introduced. Others, like `union-theories`, take two theories and produce a new one. See redundant-events for a caution about the use of logical names in theory expressions.

Theory expressions are generally composed of applications of theory functions. Formally, theory expressions are expressions that involve, at most, the free variable `world` and that when evaluated with `world` bound to the current ACL2 world (see world) return theories. The ``theory functions'' are actually macros that expand into forms that involve the free variable `world`. Thus, for example `(universal-theory :here)` actually expands to `(universal-theory-fn :here world)` and when that form is evaluated with `world` bound to the current ACL2 world, `universal-theory-fn` scans the ACL2 property lists and computes the current universal theory. Because the theory functions all implicitly use `world`, the variable does not generally appear in anything the user types.

## UNION-THEORIES

union two theories
```Major Section:  THEORIES
```

```Example:
(union-theories (current-theory 'lemma3)
(theory 'arith-patch))

General Form:
(union-theories th1 th2)
```
where `th1` and `th2` are theories (see theories). To each of the arguments there corresponds a runic theory. This function returns the union of those two runic theories, represented as a list and ordered chronologically.

This ``function'' is actually a macro that expands to a term mentioning the single free variable `world`. When theory expressions are evaluated by `in-theory` or the `:``in-theory` hint, `world` is bound to the current ACL2 world.

## UNIVERSAL-THEORY

all rules as of logical name
```Major Section:  THEORIES
```

```Examples:
(universal-theory :here)
(universal-theory 'lemma3)
```
See logical-name.

```General Form:
(universal-theory logical-name)
```
Returns the theory consisting of all the runes that existed immediately after `logical-name` was introduced. See theories and see logical-name. The theory includes `logical-name` itself (if there is a rule by that name). (Note that since some events do not introduce rules (e.g., `defmacro`, `defconst` or `defthm` with `:``rule-classes` `nil`), the universal-theory does not necessarily include a rune for every event name.) The universal-theory is very long and you will probably regret printing it.

You may experience a fencepost problem in deciding which logical-name to use. `Deflabel` can always be used to mark unambiguously for future reference a particular point in the development of your theory. This is convenient because `deflabel` does not introduce any rules and hence it doesn't matter if you count it as being in the interval or not. The order of events in the vicinity of an `encapsulate` is confusing. See encapsulate.

This ``function'' is actually a macro that expands to a term mentioning the single free variable `world`. When theory expressions are evaluated by `in-theory` or the `:``in-theory` hint, `world` is bound to the current ACL2 world.