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