|
|
|---|
|
|
|
|---|
Recursion for implementing quantification
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))))