		Search-engine friendly clone of the ACL2 documentation.

Std/osets

Delete

(delete a x) removes the element a from the set X.

If a is not a member of X, then the result is just X itself.

Efficiency note. Delete is O(n). It is very inefficient to call it repeatedly. Instead, consider removing multiple elements with difference or intersect.

The theorem delete-in is the essential correctness property for delete.

Definitions and Theorems

Function: delete

(defun delete (a x)
  (declare (xargs :guard (setp x)))
  (mbe :logic (cond ((emptyp x) nil)
                    ((equal a (head x)) (tail x))
                    (t (insert (head x) (delete a (tail x)))))
       :exec (cond ((endp x) nil)
                   ((equal a (car x)) (cdr x))
                   (t (insert (car x) (delete a (cdr x)))))))

Theorem: delete-set

(defthm delete-set (setp (delete a x)))

Theorem: delete-preserves-emptyp

(defthm delete-preserves-emptyp
  (implies (emptyp x)
           (emptyp (delete a x))))

Theorem: delete-in

(defthm delete-in
  (equal (in a (delete b x))
         (and (in a x) (not (equal a b)))))

Theorem: delete-sfix-cancel

(defthm delete-sfix-cancel
  (equal (delete a (sfix x))
         (delete a x)))

Theorem: delete-nonmember-cancel

(defthm delete-nonmember-cancel
  (implies (not (in a x))
           (equal (delete a x) (sfix x))))

Theorem: delete-delete

(defthm delete-delete
  (equal (delete a (delete b x))
         (delete b (delete a x)))
  :rule-classes ((:rewrite :loop-stopper ((a b)))))

Theorem: repeated-delete

(defthm repeated-delete
  (equal (delete a (delete a x))
         (delete a x)))

Theorem: delete-insert-cancel

(defthm delete-insert-cancel
  (equal (delete a (insert a x))
         (delete a x)))

Theorem: insert-delete-cancel

(defthm insert-delete-cancel
  (equal (insert a (delete a x))
         (insert a x)))

Theorem: subset-delete

(defthm subset-delete
  (subset (delete a x) x))