### SOLUTION-TO-SIMPLE-EXAMPLE

solution to a simple example
Major Section: ANNOTATED-ACL2-SCRIPTS

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

is a cons,
then the `fringe`

of `x`

is obtained by appending together the `fringe`

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