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
|
<html>
<head><title>MINIMAL-THEORY.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>MINIMAL-THEORY</h2>a minimal theory to enable
<pre>Major Section: <a href="THEORIES.html">THEORIES</a>
</pre><p>
<p>
This <code><a href="THEORY.html">theory</a></code> (see <a href="THEORIES.html">theories</a>) enables only a few built-in functions and
executable counterparts. It can be useful when you want to formulate lemmas
that rather immediately imply the theorem to be proved, by way of a <code>:use</code>
hint (see <a href="HINTS.html">hints</a>), for example as follows.
<pre>
:use (lemma-1 lemma-2 lemma-3)
:in-theory (union-theories '(f1 f2) (theory 'minimal-theory))
</pre>
In this example, we expect the current goal to follow from lemmas
<code>lemma-1</code>, <code>lemma-2</code>, and <code>lemma-3</code> together with rules <code>f1</code> and
<code>f2</code> and some obvious facts about built-in functions (such as the
<a href="DEFINITION.html">definition</a> of <code><a href="IMPLIES.html">implies</a></code> and the <code>:</code><code><a href="EXECUTABLE-COUNTERPART.html">executable-counterpart</a></code> of
<code><a href="CAR.html">car</a></code>). The <code>:</code><code><a href="IN-THEORY.html">in-theory</a></code> hint above is intended to speed up the
proof by turning off all inessential rules.
<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>
|
