An Example of ACL2 in Use

To introduce you to ACL2 we will consider the app function discussed in the Common Lisp page, except we will omit for the moment the declare form, which in ACL2 is called a guard. We will deal with guards later.

Here is the definition again 

(defun app (x y)
  (cond ((endp x) y)
        (t (cons (car x) 
                 (app (cdr x) y)))))

The next few stops along the Walking Tour will show you 

  * how to use the ACL2 documentation,
  * what happens when the above definition is submitted to ACL2,
  * what happens when you evaluate calls of app,
  * what one simple theorem about app looks like, 
  * how ACL2 proves the theorem, and
  * how that theorem can be used in another proof.
Along the way we will talk about the definitional principle, types, the ACL2 read-eval-print loop, and how the theorem prover works.

When we complete this part of the tour we will introduce the notion of guards and revisit several of the topics above in that context.