Rune
A rule name
Examples:
(:rewrite assoc-of-app)
(:linear delta-aref . 2)
(:definition length)
(:executable-counterpart length)
Note: This topic discusses a basic notion of ``rule name'', or ``rune'' for
short. Users often use abbreviations for runes; for example, a theory
expression (DISABLE APPEND) abbreviates the following set of runes:
{(:DEFINITION BINARY-APPEND), (:INDUCTION BINARY-APPEND)}. See theories for a discussion of so-called ``runic designators'', which include
expressions like APPEND (as above) as well as (APPEND) (for the
executable-counterpart of BINARY-APPEND). Runic designators can
also be ``runic abbreviations'' such as (:d APPEND), (:e APPEND),
(:i APPEND), and (:t APPEND), which designate the definition,
executable-counterpart, induction, and type-prescription rules for
BINARY-APPEND. For a complete description of runic designators, see
theories; we return now to the more basic notion of a rune.
Background: The theorem prover is driven from a database of rules. The
most common rules are :rewrite rules, which cause the simplifier
to replace one term with another. Events introduce rules into the
database. For example, a defun event may introduce runes for
symbolically replacing a function call by its instantiated body, for
evaluating the function on constants, for determining the type of a call of
the function, and for the induction scheme introduced upon defining the
function. Defthm may introduce several rules, one for each of the
:rule-classes specified (where one rule class is specified if
: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 distinct from
that of rules generated by other events or by other :rule-classes within the same event.
For example, an event of the form
(defthm name thm
:rule-classes ((:REWRITE :COROLLARY term1)
(:REWRITE :COROLLARY term2)
(:ELIM :COROLLARY term3)))
typically creates three rules, each with a unique rune. The runes are
(:REWRITE name . 1), (:REWRITE name . 2), and (:ELIM name).
However, a given formula may create more than one rule, and all rules
generated by the same :corollary formula will share the same rune.
Consider the following example.
(defthm my-thm
(and (equal (foo (bar x)) x)
(equal (bar (foo x)) x)))
This is treated identically to the following.
(defthm my-thm
(and (equal (foo (bar x)) x)
(equal (bar (foo x)) x))
:rule-classes ((:rewrite
:corollary
(and (equal (foo (bar x)) x)
(equal (bar (foo x)) x)))))
In either case, two rules are created: one rewriting (foo (bar x)) to
x, and one rewriting (bar (foo x)) to x. However, only a
single rune is created, (:REWRITE MY-THM), because there is only one rule
class. But now consider the following example.
(defthm my-thm2
(and (equal (foo (bar x)) x)
(equal (bar (foo x)) x))
:rule-classes ((:rewrite
:corollary
(and (equal (foo (bar x)) x)
(equal (bar (foo x)) x)))
(:rewrite
:corollary
(and (equal (foo (bar (foo x))) (foo x))
(equal (bar (foo (bar x))) (bar x))))))
This time there are four rules created. The first two rules are as before,
and are assigned the rune (:REWRITE MY-THM . 1). The other two rules are
similarly generated for the second :corollary, and are assigned the rune
(:REWRITE MY-THM . 2).
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 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. Here is the list of fake
runes.
((:fake-rune-for-linear nil)
(:fake-rune-for-linear-equalities nil)
(:fake-rune-for-type-set nil)
(:fake-rune-for-cert-data nil))
Occasionally the system will print a fake rune where a rune is expected.
For example, when (:FAKE-RUNE-FOR-LINEAR NIL) 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.
Subtopics
- Find-rules-of-rune
- Find the rules named rune
