Major Section: ACL2-TUTORIAL

Beginning users may find these annotated scripts useful. We suggest that you read these in the following order:

Tutorial1-Towers-of-Hanoi Tutorial2-Eights-Problem Tutorial3-Phonebook-Example Tutorial4-Defun-Sk-Example Tutorial5-Miscellaneous-Examples

The page http://www.cs.utexas.edu/users/moore/publications/tutorial/rev3.html contains a script that illustrates how it feels to use The Method to prove an unusual list reverse function correct. The screen shots of ACL2's proof output are outdated -- in the version shown, ACL2 does not print Key Checkpoints, but the concept of key checkpoint is clear in the discussion and the behavior of the user.

See http://www.cs.utexas.edu/users/moore/acl2/contrib/POLISHING-PROOFS-TUTORIAL.html for a tutorial on becoming successful at approaching a formalization and proof problem in ACL2. That tutorial, written by Shilpi Goel and Sandip Ray, has two parts: it illustrates how to guide the theorem prover to a successful proof, and it shows how to clean up the proof in order to facilitate maintenance and extension of the resulting book (see books).

At http://www.cs.utexas.edu/users/moore/publications/tutorial/kaufmann-TPHOLs08/index.html is the demo given by Matt Kaufmann at TPHOLs08, including all the scripts. There is a gzipped tar file containing the entire contents of the demos.

At http://www.cs.utexas.edu/users/moore/publications/tutorial/sort-equivalence is a
collection of scripts illustrating both high-level strategy and lower-level tactics dealing
with the functional equivalence of various list sorting algorithms. Start with the
`README`

on that directory. There is also a gzipped tar file containing all the
scripts, at
http://www.cs.utexas.edu/users/moore/publications/tutorial/sort-equivalence.tgz.

When you feel you have read enough examples, you might want to try the following very simple example on your own. (See solution-to-simple-example for a solution, after you work on this example.) First define the notion of the ``fringe'' of a tree, where we identify trees simply as cons structures, with atoms at the leaves. For example:

ACL2 !>(fringe '((a . b) c . d)) (A B C D)Next, define the notion of a ``leaf'' of a tree, i.e., a predicate

`leaf-p`

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 `fringe`

. Finally, prove the following theorem, whose
proof may well be automatic (i.e., not require any lemmas).
(defthm leaf-p-iff-member-fringe (iff (leaf-p atm x) (member-equal atm (fringe x))))

### SOLUTION-TO-SIMPLE-EXAMPLE -- solution to a simple example

### TUTORIAL1-TOWERS-OF-HANOI -- The Towers of Hanoi Example

### TUTORIAL2-EIGHTS-PROBLEM -- The Eights Problem Example

### TUTORIAL3-PHONEBOOK-EXAMPLE -- A Phonebook Specification

### TUTORIAL4-DEFUN-SK-EXAMPLE -- example of quantified notions

### TUTORIAL5-MISCELLANEOUS-EXAMPLES -- miscellaneous ACL2 examples