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
|
<html>
<head><title>TUTORIAL-EXAMPLES.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>TUTORIAL-EXAMPLES</h2>examples of ACL2 usage
<pre>Major Section: <a href="ACL2-TUTORIAL.html">ACL2-TUTORIAL</a>
</pre><p>
Beginning users may find these examples at least as useful as the
extensive <a href="DOCUMENTATION.html">documentation</a> on particular topics. We suggest that you
read these in the following order:
<pre>
<a href="TUTORIAL1-TOWERS-OF-HANOI.html">Tutorial1-Towers-of-Hanoi</a>
<a href="TUTORIAL2-EIGHTS-PROBLEM.html">Tutorial2-Eights-Problem</a>
<a href="TUTORIAL3-PHONEBOOK-EXAMPLE.html">Tutorial3-Phonebook-Example</a>
<a href="TUTORIAL4-DEFUN-SK-EXAMPLE.html">Tutorial4-Defun-Sk-Example</a>
<a href="TUTORIAL5-MISCELLANEOUS-EXAMPLES.html">Tutorial5-Miscellaneous-Examples</a>
</pre>
You may also wish to visit the other introductory sections,
<a href="STARTUP.html">startup</a> and <a href="TIDBITS.html">tidbits</a>. These contain further information
related to the use of ACL2.
<p>
<ul>
<li><h3><a href="SOLUTION-TO-SIMPLE-EXAMPLE.html">SOLUTION-TO-SIMPLE-EXAMPLE</a> -- solution to a simple example
</h3>
</li>
<li><h3><a href="TUTORIAL1-TOWERS-OF-HANOI.html">TUTORIAL1-TOWERS-OF-HANOI</a> -- The Towers of Hanoi Example
</h3>
</li>
<li><h3><a href="TUTORIAL2-EIGHTS-PROBLEM.html">TUTORIAL2-EIGHTS-PROBLEM</a> -- The Eights Problem Example
</h3>
</li>
<li><h3><a href="TUTORIAL3-PHONEBOOK-EXAMPLE.html">TUTORIAL3-PHONEBOOK-EXAMPLE</a> -- A Phonebook Specification
</h3>
</li>
<li><h3><a href="TUTORIAL4-DEFUN-SK-EXAMPLE.html">TUTORIAL4-DEFUN-SK-EXAMPLE</a> -- example of quantified notions
</h3>
</li>
<li><h3><a href="TUTORIAL5-MISCELLANEOUS-EXAMPLES.html">TUTORIAL5-MISCELLANEOUS-EXAMPLES</a> -- miscellaneous ACL2 examples
</h3>
</li>
</ul>
When you feel you have read enough examples, you might want to try
the following very simple example on your own. First define the
notion of the ``fringe'' of a tree, where we identify trees simply
as <a href="CONS.html">cons</a> structures, with <a href="ATOM.html">atom</a>s at the leaves. For
example:
<pre><p>
ACL2 !>(fringe '((a . b) c . d))
(A B C D)<p>
</pre>
Next, define the notion of a ``leaf'' of a tree, i.e., a predicate
<code>leaf-p</code> that is true of an atom if and only if that atom appears
at the tip of the tree. Define this notion without referencing the
function <code>fringe</code>. Finally, prove the following theorem, whose
proof may well be automatic (i.e., not require any lemmas).
<pre><p>
(defthm leaf-p-iff-member-fringe
(iff (leaf-p atm x)
(member-equal atm (fringe x))))<p>
</pre>
For a solution, see <a href="SOLUTION-TO-SIMPLE-EXAMPLE.html">solution-to-simple-example</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>
|
