Major Section: ACL2 Documentation

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

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

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

### DISABLE -- deletes names from current theory

### 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

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

### INTERSECTION-THEORIES -- intersect two theories

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

### RUNE -- a rule name

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

### 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

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

These conventions attempt to implement the Nqthm-1992 treatment of theories. For example, including a function name, e.g.,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 set containing the runes`(:definition symb)`

and`(:induction 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`

.

`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`

.

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.

Major Section: THEORIES

Example: (disable fact (fact) associativity-of-app)where eachGeneral Form: (disable name1 name2 ... namek)

`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) ; locallyNote 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)`

.
Major Section: THEORIES

Example: (enable fact (fact) associativity-of-app)where eachGeneral Form: (enable name1 name2 ... namek)

`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) ; locallyNote 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)`

.
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.

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.

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.

Major Section: THEORIES

Example: (theory-invariant (incompatible (:rewrite left-to-right) (:rewrite right-to-left)))whereGeneral Form: (incompatible rune1 rune2)

`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.
Major Section: THEORIES

Example: (intersection-theories (current-theory :here) (theory 'arith-patch))whereGeneral Form: (intersection-theories th1 th2)

`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.`world`

. When theory expressions
are evaluated by `in-theory`

or the `:`

`in-theory`

hint, `world`

is bound to
the current ACL2 world.

Major Section: THEORIES

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

See rune.

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.

Major Section: THEORIES

Example: (set-difference-theories (current-theory :here) '(fact (fact)))whereGeneral Form: (set-difference-theories th1 th2)

`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))`

.

`world`

. When theory expressions
are evaluated by `in-theory`

or the `:`

`in-theory`

hint, `world`

is bound to
the current ACL2 world.

Major Section: THEORIES

Example: (theory 'my-theory)whereGeneral Form: (theory name)

`name`

is the name of a previously executed `deftheory`

event.
Returns the named theory. See theories.`world`

. When theory expressions
are evaluated by `in-theory`

or the `:`

`in-theory`

hint, `world`

is bound to
the current ACL2 world.

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:

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

### DISABLE -- deletes names from current theory

### 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

### INTERSECTION-THEORIES -- intersect two theories

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

### THEORY -- retrieve named theory

### UNION-THEORIES -- union two theories

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

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

Major Section: THEORIES

Example: (union-theories (current-theory 'lemma3) (theory 'arith-patch))whereGeneral Form: (union-theories th1 th2)

`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.`world`

. When theory expressions
are evaluated by `in-theory`

or the `:`

`in-theory`

hint, `world`

is bound to
the current ACL2 world.

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.

`world`

. When theory expressions
are evaluated by `in-theory`

or the `:`

`in-theory`

hint, `world`

is bound to
the current ACL2 world.