A way to quantify over sets.

The most important role of

More generally, we could show that a set satisfies a predicate like

We begin by explaining how pick-a-point proofs of subset can be carried out. In traditional mathematics, subset is defined using quantification over members, e.g., as follows:

(equal (subset X Y) (forall a (implies (in a X) (in a Y))))

This definition is very useful for **pick-a-point** proofs that some set

These kinds of arguments are extremely useful, and we would like to be able to carry them out in ACL2 about osets. But since ACL2 does not have explicit quantifiers, we cannot even write a theorem like this:

(implies (forall a (implies (in a X) (in a Y))) (subset X Y))

But consider the contrapositive of this theorem:

(implies (not (subset X Y)) (exists a (and (in a X) (not (in a Y)))))

We *can* prove something like this, by writing an explicit function to
search for an element of

(implies (not (subset X Y)) (let ((a (find-witness X Y))) (and (in a X) (not (in a Y)))))

Once we prove the above, we still need to be able to "reduce" a proof of

- Using encapsulate, we introduce functions
sub andsuper with the constraint that(implies (in a (sub)) (in a (super)))

- Using this constraint, we prove the generic theorem:
(subset (sub) (super))

Then, when we want to prove

sub <-- (lambda () X) super <-- (lambda () Y)

And this allows us to prove

In earlier versions of the osets library, we used an explicit argument to reduce subset proofs to pick-a-point style membership arguments. But we later generalized the approach to arbitrary predicates instead.

First, notice that if you let the predicate

(forall a (implies (in a X) (P a)))

Our generalization basically lets you reduce a proof of

The mechanism is just an adaptation of that described in the previous section.

- We begin by introducing a completely arbitrary
predicate . - Based on
predicate , we introduce a new function,all , which checks to see if every member in a set satisfiespredicate . - We set up an encapsulate which allows us to assume that some hypotheses are
true and that any member of some set satisfies
predicate .

Finally, we prove

(implies (in a X) (P a))

**Function: **

(defun all (set-for-all-reduction) (declare (xargs :guard (setp set-for-all-reduction))) (if (empty set-for-all-reduction) t (and (predicate (head set-for-all-reduction)) (all (tail set-for-all-reduction)))))

**Theorem: **

(defthm membership-constraint (implies (all-hyps) (implies (in arbitrary-element (all-set)) (predicate arbitrary-element))))

**Theorem: **

(defthm all-by-membership (implies (all-hyps) (all (all-set))))