		Search-engine friendly clone of the ACL2 documentation.

Eliminate-other-candidates

Remove-all

Remove all elements in x from y

Signature
(remove-all x y) → *
Arguments: x — Guard (true-listp x).; y — Guard (true-listp y).

Definitions and Theorems

Function: remove-all

(defun remove-all (x y)
  (declare (xargs :guard (and (true-listp x) (true-listp y))))
  (let ((__function__ 'remove-all))
    (declare (ignorable __function__))
    (if (endp x)
        y
      (remove-all (cdr x)
                  (remove-equal (car x) y)))))

Theorem: remove-all-cons-to-remove-all-remove-equal

(defthm remove-all-cons-to-remove-all-remove-equal
  (equal (remove-all (cons e x) y)
         (remove-all x (remove-equal e y))))

Theorem: remove-all-x-and-cdr-x

(defthm remove-all-x-and-cdr-x
  (equal (remove-all x (cdr x)) nil))

Theorem: remove-all-x-x-is-nil

(defthm remove-all-x-x-is-nil
  (implies (true-listp x)
           (equal (remove-all x x) nil)))

Theorem: remove-all-and-remove-equal-commute

(defthm remove-all-and-remove-equal-commute
  (equal (remove-all as (remove-equal e bs))
         (remove-equal e (remove-all as bs))))

Theorem: remove-all-commutes

(defthm remove-all-commutes
  (equal (remove-all as (remove-all bs cs))
         (remove-all bs (remove-all as cs))))

Theorem: remove-all-returns-a-subset-of-the-list

(defthm remove-all-returns-a-subset-of-the-list
  (subsetp-equal (remove-all x y) y))

Theorem: remove-all-and-member-equal-1

(defthm remove-all-and-member-equal-1
  (implies (member-equal e a)
           (equal (member-equal e (remove-all a b))
                  nil)))

Theorem: remove-all-and-member-equal-2

(defthm remove-all-and-member-equal-2
  (implies (not (member-equal e a))
           (iff (member-equal e (remove-all a b))
                (member-equal e b))))

Theorem: remove-all-of-nil-is-nil

(defthm remove-all-of-nil-is-nil
  (equal (remove-all x nil) nil))

Theorem: remove-all-x-from-cons-e-y

(defthm remove-all-x-from-cons-e-y
  (equal (remove-all x (cons e y))
         (if (member-equal e x)
             (remove-all x y)
           (cons e (remove-all x y)))))

Theorem: remove-all-superset-from-subset-is-nil

(defthm remove-all-superset-from-subset-is-nil
  (implies (and (subsetp-equal y x) (true-listp y))
           (equal (remove-all x y) nil)))

Theorem: remove-all-and-set-equiv

(defthm remove-all-and-set-equiv
  (implies (and (acl2::set-equiv x y)
                (true-listp y))
           (equal (remove-all x y) nil)))

Theorem: nested-remove-alls-and-subsetp-equal

(defthm nested-remove-alls-and-subsetp-equal
  (implies (subsetp-equal a c)
           (subsetp-equal a (remove-all (remove-all a b) c))))