#### QUANTIFIERS-USING-DEFUN-SK

quantification example
Major Section: QUANTIFIERS

See quantifiers for the context of this example. It should be
compared to a corresponding example in which a simpler proof is
attained by using recursion in place of explicit quantification;
see quantifiers-using-recursion.

(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 explicit quantification.

(defstub p (x) t)

(defun-sk forall-p (x)
(forall a (implies (member a x)
(p a))))

(defthm member-append
(iff (member a (append x1 x2))
(or (member a x1) (member a x2))))

(defthm forall-p-append
(equal (forall-p (append x1 x2))
(and (forall-p x1) (forall-p x2)))
:hints (("Goal" ; ``should'' disable forall-p-necc, but no need
:use
((:instance forall-p-necc
(x (append x1 x2))
(a (forall-p-witness x1)))
(:instance forall-p-necc
(x (append x1 x2))
(a (forall-p-witness x2)))
(:instance forall-p-necc
(x x1)
(a (forall-p-witness (append x1 x2))))
(:instance forall-p-necc
(x x2)
(a (forall-p-witness (append x1 x2))))))))

Also see quantifiers-using-defun-sk-extended for an
elaboration on this example.