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
153
154
155
156
157
158
|
<html>
<head><title>BUILT-IN-CLAUSES.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>BUILT-IN-CLAUSES</h2>to build a clause into the simplifier
<pre>Major Section: <a href="RULE-CLASSES.html">RULE-CLASSES</a>
</pre><p>
See <a href="RULE-CLASSES.html">rule-classes</a> for a general discussion of rule classes and
how they are used to build rules from formulas. A <code>:built-in-clause</code>
rule can be built from any formula other than propositional
tautologies. Roughly speaking, the system uses the list of built-in
clauses as the first method of proof when attacking a new goal. Any
goal that is subsumed by a built in clause is proved ``silently.''
<p>
ACL2 maintains a set of ``built-in'' clauses that are used to
short-circuit certain theorem proving tasks. We discuss this at
length below. When a theorem is given the rule class
<code>:built-in-clause</code> ACL2 flattens the <code><a href="IMPLIES.html">implies</a></code> and <code><a href="AND.html">and</a></code> structure of the
<code>:</code><code><a href="COROLLARY.html">corollary</a></code> formula so as to obtain a set of formulas whose
conjunction is equivalent to the given corollary. It then converts
each of these to clausal form and adds each clause to the set of
built-in clauses.<p>
For example, the following <code>:</code><code><a href="COROLLARY.html">corollary</a></code> (regardless of the definition
of <code>abl</code>)
<pre>
(and (implies (and (true-listp x)
(not (equal x nil)))
(< (acl2-count (abl x))
(acl2-count x)))
(implies (and (true-listp x)
(not (equal nil x)))
(< (acl2-count (abl x))
(acl2-count x))))
</pre>
will build in two clauses,
<pre>
{(not (true-listp x))
(equal x nil)
(< (acl2-count (abl x)) (acl2-count x))}
</pre>
and
<pre>
{(not (true-listp x))
(equal nil x)
(< (acl2-count (abl x)) (acl2-count x))}.
</pre>
We now give more background.<p>
Recall that a clause is a set of terms, implicitly representing the
disjunction of the terms. Clause <code>c1</code> is ``subsumed'' by clause <code>c2</code> if
some instance of <code>c2</code> is a subset <code>c1</code>.<p>
For example, let <code>c1</code> be
<pre>
{(not (consp l))
(equal a (car l))
(< (acl2-count (cdr l)) (acl2-count l))}.
</pre>
Then <code>c1</code> is subsumed by <code>c2</code>, shown below,
<pre>
{(not (consp x))
; second term omitted here
(< (acl2-count (cdr x)) (acl2-count x))}
</pre>
because we can instantiate <code>x</code> in <code>c2</code> with <code>l</code> to obtain a subset of
<code>c1</code>.<p>
Observe that <code>c1</code> is the clausal form of
<pre>
(implies (and (consp l)
(not (equal a (car l))))
(< (acl2-count (cdr l)) (acl2-count l))),
</pre>
<code>c2</code> is the clausal form of
<pre>
(implies (consp l)
(< (acl2-count (cdr l)) (acl2-count l)))
</pre>
and the subsumption property just means that <code>c1</code> follows trivially
from <code>c2</code> by instantiation.<p>
The set of built-in clauses is just a set of known theorems in
clausal form. Any formula that is subsumed by a built-in clause is
thus a theorem. If the set of built-in theorems is reasonably
small, this little theorem prover is fast. ACL2 uses the ``built-in
clause check'' in four places: (1) at the top of the iteration in
the prover -- thus if a built-in clause is generated as a subgoal it
will be recognized when that goal is considered, (2) within the
simplifier so that no built-in clause is ever generated by
simplification, (3) as a filter on the clauses generated to prove
the termination of recursively <code><a href="DEFUN.html">defun</a></code>'d functions and (4) as a
filter on the clauses generated to verify the guards of a function.<p>
The latter two uses are the ones that most often motivate an
extension to the set of built-in clauses. Frequently a given
formalization problem requires the definition of many functions
which require virtually identical termination and/or guard proofs.
These proofs can be short-circuited by extending the set of built-in
clauses to contain the most general forms of the clauses generated
by the definitional schemes in use.<p>
The attentive user might have noticed that there are some recursive
schemes, e.g., recursion by <code><a href="CDR.html">cdr</a></code> after testing <code><a href="CONSP.html">consp</a></code>, that ACL2 just
seems to ``know'' are ok, while for others it generates measure
clauses to prove. Actually, it always generates measure clauses but
then filters out any that pass the built-in clause check. When ACL2
is initialized, the clause justifying <code><a href="CDR.html">cdr</a></code> recursion after a <code><a href="CONSP.html">consp</a></code>
test is added to the set of built-in clauses. (That clause is <code>c2</code>
above.)<p>
Note that only a subsumption check is made; no rewriting or
simplification is done. Thus, if we want the system to ``know''
that <code><a href="CDR.html">cdr</a></code> recursion is ok after a negative <code><a href="ATOM.html">atom</a></code> test (which, by the
definition of <code><a href="ATOM.html">atom</a></code>, is the same as a <code><a href="CONSP.html">consp</a></code> test), we have to build
in a second clause. The subsumption algorithm does not ``know''
about commutative functions. Thus, for predictability, we have
built in commuted versions of each clause involving commutative
functions. For example, we build in both
<pre>
{(not (integerp x))
(< 0 x)
(= x 0)
(< (acl2-count (+ -1 x)) (acl2-count x))}
</pre>
and the commuted version
<pre>
{(not (integerp x))
(< 0 x)
(= 0 x)
(< (acl2-count (+ -1 x)) (acl2-count x))}
</pre>
so that the user need not worry whether to write <code>(= x 0)</code> or <code>(= 0 x)</code>
in definitions.<p>
<code>:built-in-clause</code> rules added by the user can be enabled and
disabled.
<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>
|
