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
|
<html>
<head><title>STARTUP.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>STARTUP</h2>How to start using ACL2; the ACL2 <a href="COMMAND.html">command</a> loop
<pre>Major Section: <a href="ACL2-TUTORIAL.html">ACL2-TUTORIAL</a>
</pre><p>
<p>
When you start up ACL2, you'll probably find yourself inside the
ACL2 <a href="COMMAND.html">command</a> loop, as indicated by the following <a href="PROMPT.html">prompt</a>.
<pre><p>
ACL2 !><p>
</pre>
If not, you should type <code>(LP)</code>. See <a href="LP.html">lp</a>, which has a lot more
information about the ACL2 <a href="COMMAND.html">command</a> loop.<p>
You should now be in ACL2. The current ``<a href="DEFAULT-DEFUN-MODE.html">default-defun-mode</a>'' is
<code>:</code><code><a href="LOGIC.html">logic</a></code>; the other mode is <code>:</code><code><a href="PROGRAM.html">program</a></code>, which would cause the letter <code>p</code>
to be printed in the <a href="PROMPT.html">prompt</a>. <code>:</code><code><a href="LOGIC.html">Logic</a></code> means that any function we
define is not only executable but also is axiomatically defined in
the ACL2 logic. See <a href="DEFUN-MODE.html">defun-mode</a> and
see <a href="DEFAULT-DEFUN-MODE.html">default-defun-mode</a>. For example we can define a function
<code>my-cons</code> as follows. (You may find it useful to start up ACL2 and
submit this and other <a href="COMMAND.html">command</a>s below to the ACL2 <a href="COMMAND.html">command</a> loop, as we
won't include output below.)
<pre><p>
ACL2 !>(defun my-cons (x y) (cons x y))<p>
</pre>
An easy theorem may then be proved: the <code><a href="CAR.html">car</a></code> of <code>(my-cons a b)</code> is
A.
<pre><p>
ACL2 !>(defthm car-my-cons (equal (car (my-cons a b)) a))<p>
</pre>
<p>
You can place raw Lisp forms to evaluate at start-up into file
<code>acl2-init.lsp</code> in your home directory. For example, if you put the
following into <code>acl2-init.lsp</code>, then ACL2 will print "HI" when it starts
up.
<pre>
(print "HI")
</pre>
But be careful; all bets are off when you submit forms to raw Lisp, so this
capability should only be used when you are hacking or when you are setting
some Lisp parameters (e.g., <code>(setq si::*notify-gbc* nil)</code> to turn off
garbage collection notices in GCL).<p>
Notice that unlike Nqthm, the theorem <a href="COMMAND.html">command</a> is <code><a href="DEFTHM.html">defthm</a></code> rather than
<code>prove-lemma</code>. See <a href="DEFTHM.html">defthm</a>, which explains (among other things)
that the default is to turn theorems into <a href="REWRITE.html">rewrite</a> rules.<p>
Various keyword commands are available to query the ACL2 ``<a href="WORLD.html">world</a>'',
or database. For example, we may view the definition of <code>my-cons</code> by
invoking a command to print <a href="EVENTS.html">events</a>, as follows.
<pre><p>
ACL2 !>:pe my-cons<p>
</pre>
Also see <a href="PE.html">pe</a>. We may also view all the lemmas that <a href="REWRITE.html">rewrite</a>
<a href="TERM.html">term</a>s whose top function symbol is <code><a href="CAR.html">car</a></code> by using the following
command, whose output will refer to the lemma <code>car-my-cons</code> proved
above.
<pre><p>
ACL2 !>:pl car<p>
</pre>
Also see <a href="PL.html">pl</a>. Finally, we may print all the <a href="COMMAND.html">command</a>s back
through the initial <a href="WORLD.html">world</a> as follows.
<pre><p>
ACL2 !>:pbt 0<p>
</pre>
See <a href="HISTORY.html">history</a> for a list of commands, including these, for
viewing the current ACL2 <a href="WORLD.html">world</a>.<p>
Continue with the <a href="DOCUMENTATION.html">documentation</a> for <a href="TUTORIAL-EXAMPLES.html">tutorial-examples</a> to
see a simple but illustrative example in the use of ACL2 for
reasoning about functions.
<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>
|
