set-difference

(in-package "ACL2")

(defsection std/lists/set-difference
  :parents (std/lists set-difference$)
  :short "Lemmas about @(see set-difference$) available in the @(see std/lists)
library."
  (defthm set-difference-equal-when-atom
    (implies (atom x) (equal (set-difference-equal x y) nil)))
  (defthm set-difference-equal-of-cons
    (equal (set-difference-equal (cons a x) y)
      (if (member-equal a y)
        (set-difference-equal x y)
        (cons a (set-difference-equal x y)))))
  (defthm set-difference-equal-when-subsetp-equal
    (implies (subsetp-equal x y)
      (equal (set-difference-equal x y) nil)))
  (defthm set-difference-equal-of-self
    (equal (set-difference-equal x x) nil))
  (defthm empty-intersect-with-difference-of-self
    (not (intersectp-equal a (set-difference-equal b a))))
  (defthm no-duplicatesp-of-set-difference-equal
    (implies (no-duplicatesp-equal l1)
      (no-duplicatesp-equal (set-difference-equal l1 l2)))))