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 (where one rule class is specified if :ilc[rule-classes] is omitted, namely, :rewrite).

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

(:REWRITE name . 1), (:REWRITE name . 2), and (:ELIM name).

(corollary '(:TYPE-PRESCRIPTION DIGIT-TO-CHAR) (w state))

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.