• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • 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
      • Listpos
      • List-equiv
      • Final-cdr
      • Std/lists/append
      • Std/lists/remove
      • Subseq-list
      • Rcons
      • Std/lists/revappend
      • Std/lists/remove-duplicates-equal
      • Std/lists/reverse
      • Std/lists/last
      • Std/lists/resize-list
      • Flatten
      • Suffixp
      • Std/lists/butlast
      • Std/lists/set-difference
      • 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
      • Std/lists/add-to-set
      • Append-without-guard
      • Std/lists/subsetp
      • Std/lists/member
        • Basic-member-lemmas
    • Omaps
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/osets
    • Std/io
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Std/lists/member

Basic-member-lemmas

Very basic lemmas about member.

Definitions and Theorems

Theorem: member-when-atom

(defthm member-when-atom
  (implies (atom x) (not (member a x))))

Theorem: member-of-cons

(defthm member-of-cons
  (equal (member a (cons b x))
         (if (equal a b)
             (cons b x)
           (member a x))))

Theorem: member-of-car

(defthm member-of-car
  (equal (member (car x) x)
         (if (consp x) x nil)))

Theorem: member-of-append

(defthm member-of-append
  (iff (member a (append x y))
       (or (member a x) (member a y))))

Theorem: member-of-set-difference-equal

(defthm member-of-set-difference-equal
  (iff (member a (set-difference-equal x y))
       (and (member a x) (not (member a y)))))

Theorem: member-of-intersection-equal

(defthm member-of-intersection-equal
  (iff (member a (intersection-equal x y))
       (and (member a x) (member a y))))

Theorem: member-of-remove

(defthm member-of-remove
  (iff (member a (remove b x))
       (and (member a x) (not (equal a b)))))

Theorem: acl2-count-when-member

(defthm acl2-count-when-member
  (implies (member a x)
           (< (acl2-count a) (acl2-count x)))
  :rule-classes ((:rewrite) (:linear)))

Theorem: member-self

(defthm member-self (not (member x x)))

Theorem: element-p-when-member-equal-of-element-list-not-negated

(defthm element-p-when-member-equal-of-element-list-not-negated
  (and (implies (and (member-equal a x)
                     (element-list-p x))
                (element-p a))
       (implies (and (element-list-p x)
                     (member-equal a x))
                (element-p a)))
  :rule-classes :rewrite)

Theorem: element-p-when-member-equal-of-element-list-negated

(defthm element-p-when-member-equal-of-element-list-negated
  (and (implies (and (member-equal a x)
                     (element-list-p x))
                (not (non-element-p a)))
       (implies (and (element-list-p x)
                     (member-equal a x))
                (not (non-element-p a))))
  :rule-classes :rewrite)

Theorem: member-of-element-xformer-in-elementlist-projection

(defthm member-of-element-xformer-in-elementlist-projection
  (implies (member k x)
           (member (element-xformer k)
                   (elementlist-projection x)))
  :rule-classes :rewrite)

Theorem: member-in-elementlist-mapappend

(defthm member-in-elementlist-mapappend
  (implies (and (member k (element-listxformer j))
                (member j x))
           (member k (elementlist-mapappend x)))
  :rule-classes :rewrite)