1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
|
<html>
<head><title>RUNE.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>RUNE</h2>a rule name
<pre>Major Section: <a href="THEORIES.html">THEORIES</a>
</pre><p>
<pre>
Examples:
(:rewrite assoc-of-app)
(:linear delta-aref . 2)
(:definition length)
(:executable-counterpart length)
</pre>
<p>
Background: The theorem prover is driven from a data base of rules. The most
common rules are <code>:</code><code><a href="REWRITE.html">rewrite</a></code> rules, which cause the simplifier to
replace one term with another. <a href="EVENTS.html">Events</a> introduce rules into the data
base. For example, a <code><a href="DEFUN.html">defun</a></code> 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.
<code><a href="DEFTHM.html">Defthm</a></code> may introduce several rules, one for each of the
<code>:</code><code><a href="RULE-CLASSES.html">rule-classes</a></code> specified (where one rule class is specified if
<code>:</code><code><a href="RULE-CLASSES.html">rule-classes</a></code> is omitted, namely, <code>:rewrite</code>).<p>
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 <code>(:token symbol . x)</code>, where <code>:token</code> is some
keyword symbol indicating what kind of rule is named, <code>symbol</code> is the
event name that created the rule (and is called the ``base symbol''
of the rune), and <code>x</code> is either <code>nil</code> or a natural number that makes the
rule name distinct from that of rules generated by other <a href="EVENTS.html">events</a> or
by other <code>:</code><code><a href="RULE-CLASSES.html">rule-classes</a></code> within the same event.<p>
For example, an event of the form
<pre>
(defthm name thm
:rule-classes ((:REWRITE :COROLLARY term1)
(:REWRITE :COROLLARY term2)
(:ELIM :COROLLARY term3)))
</pre>
typically creates three rules, each with a unique rune. The runes are
<pre>
(:REWRITE name . 1), (:REWRITE name . 2), and (:ELIM name).
</pre>
However, a given formula may create more than one rule, and all rules
generated by the same <code>:corollary</code> formula will share the same rune.
Consider the following example.
<pre>
(defthm my-thm
(and (equal (foo (bar x)) x)
(equal (bar (foo x)) x)))
</pre>
This is treated identically to the following.
<pre>
(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)))))
</pre>
In either case, two rules are created: one rewriting <code>(foo (bar x))</code> to
<code>x</code>, and one rewriting <code>(bar (foo x))</code> to <code>x</code>. However, only a single
rune is created, <code>(:REWRITE MY-THM)</code>, because there is only one rule class.
But now consider the following example.
<pre>
(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))))))
</pre>
This time there are four rules created. The first two rules are as before,
and are assigned the rune <code>(:REWRITE MY-THM . 1)</code>. The other two rules are
similarly generated for the second <code>:corollary</code>, and are assigned the rune
<code>(:REWRITE MY-THM . 2)</code>.<p>
The function <code><a href="COROLLARY.html">corollary</a></code> will return the <a href="COROLLARY.html">corollary</a> term associated
with a given rune in a given <a href="WORLD.html">world</a>. Example:
<pre>
(corollary '(:TYPE-PRESCRIPTION DIGIT-TO-CHAR) (w state))
</pre>
However, the preferred way to see the corollary term associated with
a rune or a name is to use <code>:pf</code>; see <a href="PF.html">pf</a>.<p>
The <code><a href="DEFUN.html">defun</a></code> event creates as many as four rules. <code>(:definition fn)</code> is
the rune given to the equality axiom defining the function, <code>fn</code>.
<code>(:executable-counterpart fn)</code> is the rune given to the rule for computing
<code>fn</code> on known arguments. A type prescription rule may be created under the
name <code>(:type-prescription fn)</code>, and an <a href="INDUCTION.html">induction</a> rule may be created under
the name <code>(:induction fn)</code>.<p>
Runes may be individually <a href="ENABLE.html">enable</a>d and <a href="DISABLE.html">disable</a>d, according to whether
they are included in the current theory. See <a href="THEORIES.html">theories</a>. Thus,
it is permitted to <a href="DISABLE.html">disable</a> <code>(:elim name)</code>, say, while enabling the
other rules derived from name. Similarly, <code>(:definition fn)</code> may be
<a href="DISABLE.html">disable</a>d while <code>(:executable-counterpart fn)</code> and the type
prescriptions for <code>fn</code> are <a href="ENABLE.html">enable</a>d.<p>
Associated with most runes is the formula justifying the rule named. This is
called the ``<a href="COROLLARY.html">corollary</a> formula'' of the rune and may be obtained via the
function <code><a href="COROLLARY.html">corollary</a></code>, which takes as its argument a rune and a property
list <a href="WORLD.html">world</a>. Also see <a href="PF.html">pf</a>. The <a href="COROLLARY.html">corollary</a> formula for <code>(:rewrite name . 1)</code>
after the <code><a href="DEFTHM.html">defthm</a></code> event above is <code>term1</code>. The corollary formulas for
<code>(:definition fn)</code> and <code>(:executable-counterpart fn)</code> are always
identical: the defining axiom. Some runes, e.g., <code>(:definition car)</code>, do
not have corollary formulas. <code><a href="COROLLARY.html">Corollary</a></code> returns <code>nil</code> on such runes.
In any case, the corollary formula of a rune, when it is non-<code>nil</code>, is a
theorem and may be used in the <code>:use</code> and <code>:by</code> <a href="HINTS.html">hints</a>.<p>
Note: The system has many built in rules that, for regularity, ought
to have names but don't because they can never be <a href="DISABLE.html">disable</a>d. 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
<code>nil</code>, use a keyword token that includes the phrase ``fake-rune'', and
are always <a href="ENABLE.html">enable</a>d. For example, <code>(:fake-rune-for-linear nil)</code> 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 <a href="THEORIES.html">theories</a>, they cannot be <a href="ENABLE.html">enable</a>d or <a href="DISABLE.html">disable</a>d, and
they do not have associated <a href="COROLLARY.html">corollary</a> formulas. In short, despite
the fact that the user may sometimes see fake runes printed, they
should never be typed.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
