delete

(in-package "SET")

(include-book "membership")

(set-verify-guards-eagerness 2)

(defsection delete
  :parents (std/osets)
  :short "@(call delete) removes the element @('a') from the set @('X')."
  :long "<p>If @('a') is not a member of @('X'), then the result is just @('X')
itself.</p>

<p>Efficiency note.  Delete is @('O(n)').  It is very inefficient to call it
repeatedly.  Instead, consider removing multiple elements with @(see
difference) or @(see intersect).</p>

<p>The theorem @('delete-in') is the essential correctness property for
@('delete').</p>"
  (defun delete
    (a x)
    (declare (xargs :guard (setp x) :verify-guards nil))
    (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)))))))
  (defthm delete-set
    (setp (delete a x)))
  (verify-guards delete
    :hints (("Goal" :in-theory (enable (:ruleset primitive-rules)))))
  (defthm delete-preserves-emptyp
    (implies (emptyp x)
      (emptyp (delete a x))))
  (defthm delete-in
    (equal (in a (delete b x))
      (and (in a x) (not (equal a b)))))
  (defthm delete-sfix-cancel
    (equal (delete a (sfix x))
      (delete a x)))
  (defthm delete-nonmember-cancel
    (implies (not (in a x))
      (equal (delete a x) (sfix x))))
  (defthm delete-delete
    (equal (delete a (delete b x))
      (delete b (delete a x)))
    :rule-classes ((:rewrite :loop-stopper ((a b)))))
  (defthm repeated-delete
    (equal (delete a (delete a x))
      (delete a x)))
  (defthm delete-insert-cancel
    (equal (delete a (insert a x))
      (delete a x)))
  (defthm insert-delete-cancel
    (equal (insert a (delete a x))
      (insert a x)))
  (defthm subset-delete
    (subset (delete a x) x)))