Sets of runes to enable/disable in concert

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

See:

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 interesting
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,

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,

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, `append` is `binary-append`, and the macro-aliases dereference of
`nth` is

- A rune is a runic designator and denotes the singleton set containing that rune.
- Suppose that
symb is a symbol andsymb' is the macro-aliases dereference ofsymb , wheresymb' is a function symbol introduced with a`defun`(or`defuns`) event. Thensymb 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 ofsymb' is not singly recursive). - Suppose that
symb is a symbol andsymb' is the macro-aliases dereference ofsymb , wheresymb' 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')`. - If
symb is the name of a`defthm`(or`defaxiom`) event that introduced at least one rule, thensymb is a runic designator and denotes the set of the names of all rules introduced by the named event. - If
str is the string naming some`defpkg`event andsymb is the symbol returned by(intern (concatenate 'string str "-PACKAGE") "ACL2") , thensymb 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) isstr . - If
symb is the name of a`deftheory`event, thensymb is a runic designator and denotes the runic theory (as defined below) corresponding tosymb . - Finally, suppose that
symb is a symbol andsymb' is the macro-aliases dereference ofsymb . Then(:KWD symb . rest) is a runic designator, known as a ``runic abbreviation'', if(:KWD' symb' . rest) is a rune, where::KWD is one of:d ,:e ,:i ,:r , or:t ; and:KWD' is:definition ,:executable-counterpart ,:induction ,:rewrite , or:type-prescription , respectively. In this case,(:KWD symb . rest) denotes the runic theory (as defined below) 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

Because a rune is a runic designator denoting the set containing
that rune, a list of runes is a theory and denotes itself.
There is a natural ``canonical'' ordering of runes by order of their creation.
We call a canonically ordered true list of runes a ``runic theory.'' To every
theory there corresponds a runic theory, sometimes called its runic
correspondent, 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`.

- Rune
- A rule name
- In-theory
- Designate ``current'' theory (enabling its rules)
- Disable
- Deletes names from current theory
- Enable
- Adds names to current theory
- Theories-and-primitives
- Warnings from disabling or enabling certain built-in functions
- Deftheory
- Define a theory (to enable or disable a set of rules)
- Theory-functions
- Functions for obtaining or producing theories
- Deftheory-static
- Define a `static' theory (to enable or disable a set of rules)
- Current-theory
- Currently enabled rules as of logical name
- Syntactically-clean-lambda-objects-theory
- how to specify syntactic cleaning of lambda objects
- Hands-off-lambda-objects-theory
- how to specify no modification of lambda objects
- Rewrite-lambda-objects-theory
- how to specify rewriting of lambda objects
- Rulesets
- Table-based alternative to ACL2's named theories.
- Theory
- Retrieve named theory
- Disabledp
- Determine whether a given name or rune is disabled
- Universal-theory
- All rules as of logical name
- Using-enabled-rules
- Avoiding
:use hints for enabled: `rewrite`rules - E/d
- Enable/disable rules
- Active-runep
- Check that a rune exists and is enabled
- Executable-counterpart-theory
- Executable-counterpart rules as of logical name
- Function-theory
- Function symbol rules as of logical name
- Set-difference-theories
- Difference of two theories
- Minimal-theory
- A minimal theory to enable
- Ground-zero
- enabled rules in the startup theory
- Union-theories
- Union two theories
- Intersection-theories
- Intersect two theories
- Incompatible
- Declaring that two rules should not both be enabled
- Defthy
- Define a theory (to enable or disable a set of rules)
- Incompatible!
- Declaring that two rules must exist and should not both be enabled
- Active-or-non-runep
- Require a rune to exist, and check that it is enabled
- Rule-names
- How rules are named.