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
(defun fringe (x) (if (consp x) (append (fringe (car x)) (fringe (cdr x))) (list x)))
(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
(defthm leaf-p-iff-member-fringe (iff (leaf-p atm x) (member-equal atm (fringe x))))