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
|
<html>
<head><title>THEORY-FUNCTIONS.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>THEORY-FUNCTIONS</h2>functions for obtaining or producing <a href="THEORIES.html">theories</a>
<pre>Major Section: <a href="THEORIES.html">THEORIES</a>
</pre><p>
<pre>
Example Calls of Theory Functions:
(universal-theory :here)
(union-theories th1 th2)
(set-difference-theories th1 th2)
</pre>
The theory functions are documented individually:
<p>
<ul>
<li><h3><a href="CURRENT-THEORY.html">CURRENT-THEORY</a> -- currently <a href="ENABLE.html">enable</a>d rules as of logical name
</h3>
</li>
<li><h3><a href="DISABLE.html">DISABLE</a> -- deletes names from current theory
</h3>
</li>
<li><h3><a href="E_slash_D.html">E/D</a> -- enable/disable rules
</h3>
</li>
<li><h3><a href="ENABLE.html">ENABLE</a> -- adds names to current theory
</h3>
</li>
<li><h3><a href="EXECUTABLE-COUNTERPART-THEORY.html">EXECUTABLE-COUNTERPART-THEORY</a> -- executable counterpart rules as of logical name
</h3>
</li>
<li><h3><a href="FUNCTION-THEORY.html">FUNCTION-THEORY</a> -- function symbol rules as of logical name
</h3>
</li>
<li><h3><a href="GROUND-ZERO.html">GROUND-ZERO</a> -- <a href="ENABLE.html">enable</a>d rules in the <a href="STARTUP.html">startup</a> theory
</h3>
</li>
<li><h3><a href="INTERSECTION-THEORIES.html">INTERSECTION-THEORIES</a> -- intersect two <a href="THEORIES.html">theories</a>
</h3>
</li>
<li><h3><a href="MINIMAL-THEORY.html">MINIMAL-THEORY</a> -- a minimal theory to enable
</h3>
</li>
<li><h3><a href="SET-DIFFERENCE-THEORIES.html">SET-DIFFERENCE-THEORIES</a> -- difference of two <a href="THEORIES.html">theories</a>
</h3>
</li>
<li><h3><a href="THEORY.html">THEORY</a> -- retrieve named theory
</h3>
</li>
<li><h3><a href="UNION-THEORIES.html">UNION-THEORIES</a> -- union two <a href="THEORIES.html">theories</a>
</h3>
</li>
<li><h3><a href="UNIVERSAL-THEORY.html">UNIVERSAL-THEORY</a> -- all rules as of logical name
</h3>
</li>
</ul>
The functions (actually, macros) mentioned above are convenient ways
to produce <a href="THEORIES.html">theories</a>. (See <a href="THEORIES.html">theories</a>.) Some, like
<code><a href="UNIVERSAL-THEORY.html">universal-theory</a></code>, take a logical name (see <a href="LOGICAL-NAME.html">logical-name</a>) as an
argument and return the relevant theory as of the time that name was
introduced. Others, like <code><a href="UNION-THEORIES.html">union-theories</a></code>, take two <a href="THEORIES.html">theories</a> and
produce a new one. See <a href="REDUNDANT-EVENTS.html">redundant-events</a> for a caution about
the use of logical names in theory expressions.<p>
Theory expressions are generally composed of applications of theory
functions. Formally, theory expressions are expressions that
involve, at most, the free variable <code><a href="WORLD.html">world</a></code> and that when evaluated
with <code><a href="WORLD.html">world</a></code> bound to the current ACL2 world (see <a href="WORLD.html">world</a>) return
<a href="THEORIES.html">theories</a>. The ``theory functions'' are actually macros that expand
into forms that involve the free variable <code><a href="WORLD.html">world</a></code>. Thus, for example
<code>(universal-theory :here)</code> actually expands to
<code>(universal-theory-fn :here world)</code> and when that form is evaluated
with <code><a href="WORLD.html">world</a></code> bound to the current ACL2 <a href="WORLD.html">world</a>, <code>universal-theory-fn</code>
scans the ACL2 property lists and computes the current universal
theory. Because the theory functions all implicitly use <code><a href="WORLD.html">world</a></code>,
the variable does not generally appear in anything the user
types.
<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>
|
