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
|
<html>
<head><title>SIMPLE.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>SIMPLE</h2><code>:</code><code><a href="DEFINITION.html">definition</a></code> and <code>:</code><code><a href="REWRITE.html">rewrite</a></code> rules used in preprocessing
<pre>Major Section: <a href="MISCELLANEOUS.html">MISCELLANEOUS</a>
</pre><p>
<pre>
Example of simple rewrite rule:
(equal (car (cons x y)) x)<p>
Examples of simple definition:
(defun file-clock-p (x) (integerp x))
(defun naturalp (x)
(and (integerp x) (>= x 0)))
</pre>
<p>
The theorem prover output sometimes refers to ``simple'' definitions
and rewrite rules. These rules can be used by the preprocessor,
which is one of the theorem prover's ``processes'' understood by the
<code>:do-not</code> hint; see <a href="HINTS.html">hints</a>.<p>
The preprocessor expands certain definitions and uses certain
rewrite rules that it considers to be ``fast''. There are two ways
to qualify as fast. One is to be an ``abbreviation'', where a
rewrite rule with no hypotheses or loop stopper is an
``abbreviation'' if the right side contains no more variable
occurrences than the left side, and the right side does not call the
functions <code><a href="IF.html">if</a></code>, <code><a href="NOT.html">not</a></code> or <code><a href="IMPLIES.html">implies</a></code>. Definitions and rewrite rules can
both be abbreviations; the criterion for definitions is similar,
except that the definition must not be recursive. The other way to
qualify applies only to a non-recursive definition, and applies when
its body is a disjunction or conjunction, according to a perhaps
subtle criterion that is intended to avoid case splits.
<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>
|
