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
|
<html>
<head><title>IN-ARITHMETIC-THEORY.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>IN-ARITHMETIC-THEORY</h2>designate ``current'' theory for some rewriting done in linear arithmetic
<pre>Major Section: <a href="EVENTS.html">EVENTS</a>
</pre><p>
<pre>
Example:
(in-arithmetic-theory '(lemma1 lemma2))
<p>
General Form:
(in-arithmetic-theory term :doc doc-string)
</pre>
where <code>term</code> is a term that when evaluated will produce a theory
(see <a href="THEORIES.html">theories</a>), and <code><a href="DOC-STRING.html">doc-string</a></code> is an optional <a href="DOCUMENTATION.html">documentation</a>
string not beginning with ``<code>:doc-section</code> ...''. Except for the
variable <code><a href="WORLD.html">world</a></code>, <code>term</code> must contain no free variables. <code>Term</code> is
evaluated with the variable <code><a href="WORLD.html">world</a></code> bound to the current <a href="WORLD.html">world</a> to
obtain a theory and the corresponding runic theory
(see <a href="THEORIES.html">theories</a>) is then made the current theory. Thus,
immediately after the <code>in-arithmetic-theory</code>, a rule is <a href="ENABLE.html">enable</a>d
iff its rule name is a member of the runic interpretation (see <a href="THEORIES.html">theories</a>)
of some member of the value of <code>term</code>.<p>
Warning: If <code>term</code> involves macros such as <code><a href="ENABLE.html">ENABLE</a></code> and <code><a href="DISABLE.html">DISABLE</a></code>
you will probably not get what you expect! Those macros are defined
relative to the <code><a href="CURRENT-THEORY.html">CURRENT-THEORY</a></code>. But in this context you might
wish they were defined in terms of the ``<code>CURRENT-ARITHMETIC-THEORY</code>''
which is not actually a defined function. We do not anticipate that users
will repeatedly modify the arithmetic theory. We expect <code>term</code> most often
to be a constant list of runes and so have not provided ``arithmetic theory
manipulation functions'' analogous to <code><a href="CURRENT-THEORY.html">CURRENT-THEORY</a></code> and <code><a href="ENABLE.html">ENABLE</a></code>.<p>
BECAUSE NO UNIQUE name is associated with an <code>in-arithmetic-theory</code> event,
there is no way we can store the <a href="DOCUMENTATION.html">documentation</a> string <code><a href="DOC-STRING.html">doc-string</a></code>
in our il[documentation] data base. Hence, we actually prohibit <code><a href="DOC-STRING.html">doc-string</a></code>
from having the form of an ACL2 <a href="DOCUMENTATION.html">documentation</a> string;
see <a href="DOC-STRING.html">doc-string</a>.<p>
See <a href="NON-LINEAR-ARITHMETIC.html">non-linear-arithmetic</a>.
<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>
|
