		Search-engine friendly clone of the ACL2 documentation.

Std/lists/intersection$

Lemmas about intersection$ available in the std/lists library.

Definitions and Theorems

We'll take intersectp as the desired normal form for asking whether intersections are empty.

Theorem: intersection$-under-iff

(defthm intersection$-under-iff
        (iff (intersection$ x y)
             (intersectp x y)))

Theorem: consp-of-intersection$

(defthm consp-of-intersection$
        (equal (consp (intersection$ x y))
               (intersectp x y)))

Basic atom/cons rules.

Theorem: intersection$-when-atom-left

(defthm intersection$-when-atom-left
        (implies (atom x)
                 (equal (intersection$ x y) nil)))

Theorem: intersection$-of-cons-left

(defthm intersection$-of-cons-left
        (equal (intersection$ (cons a x) y)
               (if (member a y)
                   (cons a (intersection$ x y))
                   (intersection$ x y))))

Theorem: intersection$-when-atom-right

(defthm intersection$-when-atom-right
        (implies (atom y)
                 (equal (intersection$ x y) nil)))

We don't have a very nice rule for cons on the right if we're trying to maintain equal, because we don't know where in x the element occurs. However, if we're only maintaining set-equiv, then we can just put the element on the front and we get a perfectly nice rule:

Theorem: intersection$-of-cons-right-under-set-equiv

(defthm intersection$-of-cons-right-under-set-equiv
        (set-equiv (intersection$ x (cons a y))
                   (if (member a x)
                       (cons a (intersection$ x y))
                       (intersection$ x y))))

Basic set reasoning

Theorem: member-of-intersection$

(defthm
 member-of-intersection$
 (iff (member a (intersection$ x y))
      (and (member a x) (member a y)))
 :rule-classes
 (:rewrite
   (:type-prescription
        :corollary (implies (not (member a x))
                            (not (member a (intersection$ x y)))))
   (:type-prescription
        :corollary (implies (not (member a y))
                            (not (member a (intersection$ x y)))))))

Theorem: subsetp-equal-of-intersection$-1

(defthm subsetp-equal-of-intersection$-1
        (subsetp-equal (intersection$ x y) x))

Theorem: subsetp-equal-of-intersection$-2

(defthm subsetp-equal-of-intersection$-2
        (subsetp-equal (intersection$ x y) y))

Theorem: intersection$-commutes-under-set-equiv

(defthm intersection$-commutes-under-set-equiv
        (set-equiv (intersection$ x y)
                   (intersection$ y x)))

Length bound

Here is a nice bounding theorem. Note that there is no analogous rule for -right, because, e.g., X could have multiple copies of some member in Y, and if so we end up reproducing them. Consider for instance:

(intersection$ '(a a a) '(a)) ==> '(a a a)

Theorem: len-of-intersection$-upper-bound

(defthm len-of-intersection$-upper-bound
        (<= (len (intersection$ x y)) (len x))
        :rule-classes ((:rewrite) (:linear)))