QUANTIFIERS-USING-RECURSION

recursion for implementing quantification
Major Section:  QUANTIFIERS

The following example illustrates the use of recursion as a means of avoiding proof difficulties that can arise from the use of explicit quantification (via defun-sk). See quantifiers for more about the context of this example.

(in-package "ACL2")

; We prove that if every member A of each of two lists satisfies the
; predicate (P A), then this holds of their append; and, conversely.

; Here is a solution using recursively-defined functions.

(defstub p (x) t)

(defun all-p (x)
  (if (atom x)
      t
    (and (p (car x))
         (all-p (cdr x)))))

(defthm all-p-append
  (equal (all-p (append x1 x2))
         (and (all-p x1) (all-p x2))))