• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
    • Std/lists
      • Std/lists/abstract
      • Rev
      • Defsort
      • List-fix
      • Std/lists/nth
      • Hons-remove-duplicates
      • Std/lists/update-nth
      • Set-equiv
      • Duplicity
      • Prefixp
      • Std/lists/take
      • Std/lists/intersection$
      • Nats-equiv
      • Repeat
      • Index-of
      • All-equalp
      • Sublistp
      • Std/lists/nthcdr
      • Std/lists/append
      • Listpos
      • List-equiv
      • Final-cdr
      • Std/lists/remove
      • Subseq-list
      • Rcons
      • Std/lists/revappend
      • Std/lists/remove-duplicates-equal
      • Std/lists/last
      • Std/lists/reverse
      • Std/lists/resize-list
      • Flatten
      • Suffixp
      • Std/lists/set-difference
      • Std/lists/butlast
      • Std/lists/len
      • Std/lists/intersectp
      • Std/lists/true-listp
      • Intersectp-witness
      • Subsetp-witness
      • Std/lists/remove1-equal
      • Rest-n
      • First-n
      • Std/lists/union
      • Append-without-guard
      • Std/lists/subsetp
        • Basic-subsetp-lemmas
      • Std/lists/member
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/system
    • Std/basic
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• 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)