intersectp

(in-package "ACL2")

(defsection std/lists/intersectp
  :parents (std/lists intersectp)
  :short "Lemmas about @(see intersectp) available in the @(see std/lists)
library."
  (defthm intersectp-equal-of-atom-left
    (implies (atom x) (equal (intersectp-equal x y) nil)))
  (defthm intersectp-equal-of-atom-right
    (implies (atom y) (equal (intersectp-equal x y) nil)))
  (defthm intersect-equal-of-cons-left
    (equal (intersectp-equal (cons a x) y)
      (if (member-equal a y)
        t
        (intersectp-equal x y))))
  (defthm intersectp-equal-of-cons-right
    (equal (intersectp-equal x (cons a y))
      (if (member-equal a x)
        t
        (intersectp-equal x y))))
  "<h5>Basic set reasoning</h5>"
  (defcong set-equiv equal (intersectp x y) 1)
  (defcong set-equiv equal (intersectp x y) 2)
  (defthm intersectp-of-self
    (equal (intersectp x x) (consp x))))