		Search-engine friendly clone of the ACL2 documentation.

Guard-theorem-example

How to use a previously-proved guard theorem

See lemma-instance for a discussion of :guard-theorem lemma instances, and see gthm for a related user-level query utility. In this topic, we illustrate the use of such lemma instances to take advantage of a guard theorem already proved for an existing definition, when attempting to admit a new definition.

The following example is contrived but should get the idea across. Suppose that the event displayed just below was previously executed, for example when including a book. The mbe call generates a guard proof obligation, but there is only one thing to know about that for this example: without the local lemma shown, the guard proof fails for f1.

(encapsulate
  ()
  (local (defthm append-revappend
           (equal (append (revappend x y) z)
                  (revappend x (append y z)))))

  (defun f1 (x y)
    (declare (xargs :guard (and (true-listp x)
                                (true-listp y))))
    (mbe :logic (append (reverse x) y)
         :exec (revappend x y))))

Now suppose that later, we wish to admit a function with the same guard and body. Since the lemma append-revappend above is local, guard verification will likely fail. However, we can tell the prover to use the guard theorem already proved for f1, as follows; then the guard verification proof succeeds.

(defun f2 (x y)
  (declare (xargs :guard (and (true-listp x)
                              (true-listp y))
                  :guard-hints (("Goal" :use ((:guard-theorem f1))))))
  (mbe :logic (append (reverse x) y)
       :exec (revappend x y)))

See termination-theorem-example for an example use of the analogous lemma instance type, :termination-theorem. That topic also includes discussion of the use of event names in prover output.