• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
      • Omaps
      • All-by-membership
      • In
      • Defset
      • Primitives
      • Subset
      • Mergesort
      • Intersect
      • Union
      • Pick-a-point-subset-strategy
      • Delete
      • Difference
      • Cardinality
      • Set
      • Double-containment
      • Intersectp
    • Std/system
    • Std/basic
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• 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 ((empty 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-empty

(defthm delete-preserves-empty
        (implies (empty x)
                 (empty (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))