		Search-engine friendly clone of the ACL2 documentation.

Std/lists/subsetp

Basic-subsetp-lemmas

Very basic lemmas about subsetp.

Definitions and Theorems

Theorem: subsetp-when-atom-left

(defthm subsetp-when-atom-left
  (implies (atom x) (subsetp x y)))

Theorem: subsetp-when-atom-right

(defthm subsetp-when-atom-right
  (implies (atom y)
           (equal (subsetp x y) (atom x))))

Theorem: subsetp-nil

(defthm subsetp-nil (subsetp nil x))

Theorem: subsetp-of-cons

(defthm subsetp-of-cons
  (equal (subsetp (cons a x) y)
         (if (member a y) (subsetp x y) nil)))

Theorem: subsetp-member

(defthm subsetp-member
  (implies (and (member a x) (subsetp x y))
           (member a y))
  :rule-classes
  ((:rewrite)
   (:rewrite :corollary (implies (and (subsetp x y) (member a x))
                                 (member a y)))
   (:rewrite
        :corollary (implies (and (not (member a y)) (subsetp x y))
                            (not (member a x))))
   (:rewrite
        :corollary (implies (and (subsetp x y) (not (member a y)))
                            (not (member a x))))))

Theorem: element-list-p-when-subsetp-equal-true-list

(defthm element-list-p-when-subsetp-equal-true-list
  (implies (and (subsetp-equal x y)
                (element-list-p y)
                (not (element-list-final-cdr-p t)))
           (equal (element-list-p x)
                  (true-listp x)))
  :rule-classes :rewrite)

Theorem: element-list-p-when-subsetp-equal-non-true-list

(defthm element-list-p-when-subsetp-equal-non-true-list
  (implies (and (subsetp-equal x y)
                (element-list-p y)
                (element-list-final-cdr-p t))
           (element-list-p x))
  :rule-classes :rewrite)

Theorem: subsetp-of-elementlist-projection-when-subsetp

(defthm subsetp-of-elementlist-projection-when-subsetp
  (implies (subsetp x y)
           (subsetp (elementlist-projection x)
                    (elementlist-projection y)))
  :rule-classes :rewrite)

Theorem: subsetp-refl

(defthm subsetp-refl (subsetp x x))

Theorem: subsetp-trans

(defthm subsetp-trans
  (implies (and (subsetp x y) (subsetp y z))
           (subsetp x z)))

Theorem: subsetp-trans2

(defthm subsetp-trans2
  (implies (and (subsetp y z) (subsetp x y))
           (subsetp x z)))

Theorem: subsetp-implies-subsetp-cdr

(defthm subsetp-implies-subsetp-cdr
  (implies (subsetp x y)
           (subsetp (cdr x) y)))

Theorem: subsetp-of-cdr

(defthm subsetp-of-cdr
  (subsetp (cdr x) x))

Theorem: subsetp-cons-same

(defthm subsetp-cons-same
  (implies (subsetp a b)
           (subsetp (cons x a) (cons x b))))

Theorem: subsetp-cons-2

(defthm subsetp-cons-2
  (implies (subsetp a b)
           (subsetp a (cons x b))))

Theorem: subsetp-append1

(defthm subsetp-append1
  (equal (subsetp (append a b) c)
         (and (subsetp a c) (subsetp b c))))

Theorem: subsetp-append2

(defthm subsetp-append2
  (subsetp a (append a b)))

Theorem: subsetp-append3

(defthm subsetp-append3
  (subsetp b (append a b)))

Theorem: subsetp-of-append-when-subset-of-either

(defthm subsetp-of-append-when-subset-of-either
  (implies (or (subsetp a b) (subsetp a c))
           (subsetp a (append b c))))

Theorem: subsetp-car-member

(defthm subsetp-car-member
  (implies (and (subsetp x y) (consp x))
           (member (car x) y)))

Theorem: subsetp-intersection-equal

(defthm subsetp-intersection-equal
  (iff (subsetp a (intersection-equal b c))
       (and (subsetp a b) (subsetp a c))))

Theorem: subsetp-of-elementlist-mapappend-when-subsetp

(defthm subsetp-of-elementlist-mapappend-when-subsetp
  (implies (subsetp x y)
           (subsetp (elementlist-mapappend x)
                    (elementlist-mapappend y)))
  :rule-classes :rewrite)

Theorem: set-equiv-congruence-over-elementlist-mapappend

(defthm set-equiv-congruence-over-elementlist-mapappend
  (implies (set-equiv x y)
           (set-equiv (elementlist-mapappend x)
                      (elementlist-mapappend y)))
  :rule-classes :congruence)