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:

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

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

adds names to current theory 
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:

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.