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