# Annotated-ACL2-scripts

Examples of ACL2 scripts

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

You can also find useful demos in the community-books directory,
books/demos/, and its subdirectories.

The web page Brief
ACL2 Tutorial 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 Polishing
Proofs Tutorial 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).

The ACL2
Demo Given at TPHOLs 2008 by Matt Kaufmann includes scripts and a gzipped
tar file containing the entire contents of the demos.

The sort
equivalence demo 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 with all of these scripts.

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))))

### Subtopics

- Tutorial3-phonebook-example
- A Phonebook Specification
- Tutorial1-towers-of-hanoi
- The Towers of Hanoi Example
- Tutorial2-eights-problem
- The Eights Problem Example
- Solution-to-simple-example
- Solution to a simple example
- Tutorial4-defun-sk-example
- Example of quantified notions
- Tutorial5-miscellaneous-examples
- Miscellaneous ACL2 examples