SOLUTION-TO-SIMPLE-EXAMPLE

solution to a simple example 
Major Section:  TUTORIAL-EXAMPLES

To see a statement of the problem solved below, see tutorial-examples.

Here is a sequence of ACL2 events that illustrates the use of ACL2 to make definitions and prove theorems. We will introduce the notion of the fringe of a tree, as well as the notion of a leaf of a tree, and then prove that the members of the fringe are exactly the leaves.

We begin by defining the fringe of a tree, where we identify trees simply as cons structures, with atoms at the leaves. The definition is recursive, breaking into two cases. If x is a cons, then the fringe of x is obtained by appending together the fringes of the car and cdr (left and right child) of x. Otherwise, x is an atom and its fringe is the one-element list containing only x. 



  (defun fringe (x)
    (if (consp x)
        (append (fringe (car x))
                (fringe (cdr x)))
      (list x)))
Now that fringe has been defined, let us proceed by defining the notion of an atom appearing as a ``leaf'', with the goal of proving that the leaves of a tree are exactly the members of its fringe. 


  (defun leaf-p (atm x)
    (if (consp x)
        (or (leaf-p atm (car x))
            (leaf-p atm (cdr x)))
      (equal atm x)))
The main theorem is now as follows. Note that the rewrite rule below uses the equivalence relation iff (see equivalence) rather than equal, since member returns the tail of the given list that begins with the indicated member, rather than returning a Boolean. (Use :pe member to see the definition of member.) 


  (defthm leaf-p-iff-member-fringe
    (iff (leaf-p atm x)
         (member-equal atm (fringe x))))