remove

(in-package "ACL2")

(defsection std/lists/remove
  :parents (std/lists remove)
  :short "Lemmas about @(see remove) available in the @(see std/lists)
library."
  (defthm remove-when-atom
    (implies (atom x) (equal (remove a x) nil)))
  (defthm remove-of-cons
    (equal (remove a (cons b x))
      (if (equal a b)
        (remove a x)
        (cons b (remove a x)))))
  (defthm consp-of-remove
    (equal (consp (remove a x)) (not (subsetp x (list a)))))
  (defthm remove-under-iff
    (iff (remove a x) (not (subsetp x (list a)))))
  (defthm remove-when-non-member
    (implies (not (member a x))
      (equal (remove a x) (list-fix x))))
  (defthm upper-bound-of-len-of-remove-weak
    (<= (len (remove a x)) (len x))
    :rule-classes ((:rewrite) (:linear)))
  (defthm upper-bound-of-len-of-remove-strong
    (implies (member a x) (< (len (remove a x)) (len x)))
    :rule-classes :linear)
  (defthm len-of-remove-exact
    (equal (len (remove a x)) (- (len x) (duplicity a x))))
  (defthm remove-is-commutative
    (equal (remove b (remove a x)) (remove a (remove b x))))
  (defthm remove-is-idempotent
    (equal (remove a (remove a x)) (remove a x)))
  (defthm duplicity-of-remove
    (equal (duplicity a (remove b x))
      (if (equal a b)
        0
        (duplicity a x))))
  (defthm remove-of-append
    (equal (remove a (append x y))
      (append (remove a x) (remove a y))))
  (defthm remove-of-revappend
    (equal (remove a (revappend x y))
      (revappend (remove a x) (remove a y))))
  (defthm remove-of-rev
    (equal (remove a (rev x)) (rev (remove a x))))
  (defthm remove-of-union-equal
    (equal (remove a (union-equal x y))
      (union-equal (remove a x) (remove a y))))
  (defthm remove-of-intersection-equal
    (equal (remove a (intersection-equal x y))
      (intersection-equal (remove a x) (remove a y))))
  (defthm remove-of-set-difference-equal
    (equal (remove a (set-difference-equal x y))
      (set-difference-equal (remove a x) y)))
  (def-listp-rule element-list-p-of-remove
    (implies (element-list-p x) (element-list-p (remove a x)))))