TUTORIAL-EXAMPLES

examples of ACL2 usage 
Major Section:  ACL2-TUTORIAL

Beginning users may find these examples at least as useful as the extensive documentation on particular topics. 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 may also wish to visit the other introductory sections, startup and tidbits. These contain further information related to the use of ACL2.

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 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))))
For a solution, see solution-to-simple-example.