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