Solution to a simple example

To see a statement of the problem solved below, see annotated-ACL2-scripts (in particular the end of that topic).

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 `car` and `cdr` (left and right child) of

(defun fringe (x) (if (consp x) (append (fringe (car x)) (fringe (cdr x))) (list x)))

Now that

(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
`member`.)

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