top

(in-package "SET")

(set-verify-guards-eagerness 2)

(include-book "misc/total-order" :dir :system)

(include-book "tools/rulesets" :dir :system)

(include-book "std/lists/list-defuns" :dir :system)

(include-book "computed-hints")

(local (include-book "std/lists/sets" :dir :system))

(local (table xdoc 'doc nil))

(local (include-book "primitives"))

(local (include-book "membership"))

(local (include-book "outer"))

(local (include-book "sort"))

(local (include-book "under-set-equiv"))

(make-event (let ((slurped-docs (get-xdoc-table (w state))))
    (value `(table xdoc
        'doc
        (union-equal ',SET::SLURPED-DOCS
          (get-xdoc-table world))))))

(defxdoc std/osets
  :parents (std)
  :short "A finite set theory implementation for ACL2 based on fully ordered
lists.  Some major features of this approach are that set equality is just
@(see equal), and set operations like @(see union), @(see intersect), and so
forth have O(n) implementations."
  :long "<p>Osets mostly hides the fact that sets are represented as ordered
lists.  You should not have to reason about the set order unless you are trying
to exploit it to make some function faster.  Instead, we generally try to
reason about sets with a membership-based approach, via @(see in) and @(see
subset).</p>

<p>The osets library offers some automation for pick-a-point style reasoning,
see for instance @(see all-by-membership), @(see pick-a-point-subset-strategy),
and @(see double-containment).</p>

<p>You can load the library with:</p>
@({
 (include-book "std/osets/top" :dir :system)
})

<p>The definitions of the main set-manipulation functions are disabled, but are
in a ruleset and may be enabled using:</p>
@({
 (in-theory (acl2::enable* set::definitions))
})

<p>Some potentially useful (but potentially expensive) rules are also left
disabled and may be enabled using:</p>
@({
 (in-theory (acl2::enable* set::expensive-rules))
})

<p>Besides this @(see xdoc::xdoc) documentation, you may be interested in the
2004 ACL2 workshop paper, <a
href='https://www.cs.utexas.edu/users/moore/acl2/workshop-2004/contrib/davis/set-theory.pdf'>Finite
Set Theory based on Fully Ordered Lists</a>, and see also the <a
href='https://www.cs.utexas.edu/users/moore/acl2/workshop-2004/contrib/davis/workshop-osets-slides.pdf'>slides</a>
from the accompanying talk.</p>")

(defund setp
  (x)
  (declare (xargs :guard t))
  (if (atom x)
    (null x)
    (or (null (cdr x))
      (and (consp (cdr x))
        (fast-<< (car x) (cadr x))
        (setp (cdr x))))))

(defthm setp-type
  (or (equal (setp x) t)
    (equal (setp x) nil))
  :rule-classes :type-prescription)

(defund-inline emptyp
  (x)
  (declare (xargs :guard (setp x)))
  (mbe :logic (or (null x) (not (setp x)))
    :exec (null x)))

(defthm emptyp-type
  (or (equal (emptyp x) t)
    (equal (emptyp x) nil))
  :rule-classes :type-prescription)

(defund-inline sfix
  (x)
  (declare (xargs :guard (setp x)))
  (mbe :logic (if (emptyp x)
      nil
      x)
    :exec x))

(defund-inline head
  (x)
  (declare (xargs :guard (and (setp x) (not (emptyp x)))))
  (mbe :logic (car (sfix x))
    :exec (car x)))

(defund-inline tail
  (x)
  (declare (xargs :guard (and (setp x) (not (emptyp x)))))
  (mbe :logic (cdr (sfix x))
    :exec (cdr x)))

(defund insert
  (a x)
  (declare (xargs :guard (setp x)))
  (mbe :logic (cond ((emptyp x) (list a))
      ((equal (head x) a) x)
      ((<< a (head x)) (cons a x))
      (t (cons (head x)
          (insert a (tail x)))))
    :exec (cond ((null x) (cons a nil))
      ((equal (car x) a) x)
      ((fast-lexorder a (car x)) (cons a x))
      ((null (cdr x)) (cons (car x) (cons a nil)))
      ((equal (cadr x) a) x)
      ((fast-lexorder a (cadr x)) (cons (car x) (cons a (cdr x))))
      (t (cons (car x)
          (cons (cadr x) (insert a (cddr x))))))))

(defun in
  (a x)
  (declare (xargs :guard (setp x)))
  (mbe :logic (and (not (emptyp x))
      (or (equal a (head x))
        (in a (tail x))))
    :exec (and x
      (or (equal a (car x))
        (and (cdr x)
          (or (equal a (cadr x))
            (in a (cddr x))))))))

(defthm in-type
  (or (equal (in a x) t)
    (equal (in a x) nil))
  :rule-classes :type-prescription)

(defund fast-subset
  (x y)
  (declare (xargs :guard (and (setp x) (setp y))))
  (mbe :logic (cond ((emptyp x) t)
      ((emptyp y) nil)
      ((<< (head x) (head y)) nil)
      ((equal (head x) (head y)) (fast-subset (tail x) (tail y)))
      (t (fast-subset x (tail y))))
    :exec (cond ((null x) t)
      ((null y) nil)
      ((fast-lexorder (car x) (car y)) (and (equal (car x) (car y))
          (fast-subset (cdr x) (cdr y))))
      (t (fast-subset x (cdr y))))))

(defun-inline subset
  (x y)
  (declare (xargs :guard (and (setp x) (setp y))))
  (mbe :logic (if (emptyp x)
      t
      (and (in (head x) y)
        (subset (tail x) y)))
    :exec (fast-subset x y)))

(defthm subset-type
  (or (equal (subset x y) t)
    (equal (subset x y) nil))
  :rule-classes :type-prescription)

(defund fast-measure
  (x y)
  (+ (acl2-count x) (acl2-count y)))

(defun fast-union
  (x y acc)
  (declare (xargs :measure (fast-measure x y)
      :guard (and (setp x)
        (setp y)
        (true-listp acc))))
  (cond ((endp x) (revappend acc y))
    ((endp y) (revappend acc x))
    ((equal (car x) (car y)) (fast-union (cdr x)
        (cdr y)
        (cons (car x) acc)))
    ((mbe :logic (<< (car x) (car y))
       :exec (fast-lexorder (car x) (car y))) (fast-union (cdr x)
        y
        (cons (car x) acc)))
    (t (fast-union x
        (cdr y)
        (cons (car y) acc)))))

(defun fast-intersect
  (x y acc)
  (declare (xargs :measure (fast-measure x y)
      :guard (and (setp x)
        (setp y)
        (true-listp acc))))
  (cond ((endp x) (revappend acc nil))
    ((endp y) (revappend acc nil))
    ((equal (car x) (car y)) (fast-intersect (cdr x)
        (cdr y)
        (cons (car x) acc)))
    ((mbe :logic (<< (car x) (car y))
       :exec (fast-lexorder (car x) (car y))) (fast-intersect (cdr x) y acc))
    (t (fast-intersect x (cdr y) acc))))

(defun fast-intersectp
  (x y)
  (declare (xargs :guard (and (setp x) (setp y))
      :measure (fast-measure x y)))
  (cond ((endp x) nil)
    ((endp y) nil)
    ((equal (car x) (car y)) t)
    ((mbe :logic (<< (car x) (car y))
       :exec (fast-lexorder (car x) (car y))) (fast-intersectp (cdr x) y))
    (t (fast-intersectp x (cdr y)))))

(defun fast-difference
  (x y acc)
  (declare (xargs :measure (fast-measure x y)
      :guard (and (setp x)
        (setp y)
        (true-listp acc))))
  (cond ((endp x) (revappend acc nil))
    ((endp y) (revappend acc x))
    ((equal (car x) (car y)) (fast-difference (cdr x) (cdr y) acc))
    ((mbe :logic (<< (car x) (car y))
       :exec (fast-lexorder (car x) (car y))) (fast-difference (cdr x)
        y
        (cons (car x) acc)))
    (t (fast-difference x (cdr y) acc))))

(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)))))))

(defun-inline union
  (x y)
  (declare (xargs :guard (and (setp x) (setp y))))
  (mbe :logic (if (emptyp x)
      (sfix y)
      (insert (head x)
        (union (tail x) y)))
    :exec (fast-union x y nil)))

(defun-inline intersect
  (x y)
  (declare (xargs :guard (and (setp x) (setp y))))
  (mbe :logic (cond ((emptyp x) (sfix x))
      ((in (head x) y) (insert (head x)
          (intersect (tail x) y)))
      (t (intersect (tail x) y)))
    :exec (fast-intersect x y nil)))

(defun-inline intersectp
  (x y)
  (declare (xargs :guard (and (setp x) (setp y))))
  (mbe :logic (not (emptyp (intersect x y)))
    :exec (fast-intersectp x y)))

(defun-inline difference
  (x y)
  (declare (xargs :guard (and (setp x) (setp y))))
  (mbe :logic (cond ((emptyp x) (sfix x))
      ((in (head x) y) (difference (tail x) y))
      (t (insert (head x)
          (difference (tail x) y))))
    :exec (fast-difference x y nil)))

(defun-inline cardinality
  (x)
  (declare (xargs :guard (setp x)))
  (mbe :logic (if (emptyp x)
      0
      (1+ (cardinality (tail x))))
    :exec (length (the list x))))

(defund halve-list-aux
  (mid x acc)
  (declare (xargs :guard (<= (len x) (len mid))))
  (if (or (atom x) (atom (cdr x)))
    (mv acc mid)
    (halve-list-aux (cdr mid)
      (cdr (cdr x))
      (cons (car mid) acc))))

(defund-inline halve-list
  (x)
  (declare (xargs :guard t))
  (halve-list-aux x x nil))

(defun mergesort-exec
  (x)
  (declare (xargs :guard t :measure (len x)))
  (cond ((atom x) nil)
    ((atom (cdr x)) (mbe :logic (insert (car x) nil)
        :exec (list (car x))))
    (t (mv-let (part1 part2)
        (halve-list x)
        (fast-union (mergesort-exec part1)
          (mergesort-exec part2)
          nil)))))

(defun-inline mergesort
  (x)
  (declare (xargs :guard t))
  (mbe :logic (if (endp x)
      nil
      (insert (car x) (mergesort (cdr x))))
    :exec (mergesort-exec x)))

(encapsulate (((predicate *) => *))
  (local (defun predicate (x) x)))

(defun all
  (set-for-all-reduction)
  (declare (xargs :guard (setp set-for-all-reduction)))
  (if (emptyp set-for-all-reduction)
    t
    (and (predicate (head set-for-all-reduction))
      (all (tail set-for-all-reduction)))))

(encapsulate (((all-hyps) => *) ((all-set) => *))
  (local (defun all-hyps nil nil))
  (local (defun all-set nil nil))
  (defthmd membership-constraint
    (implies (all-hyps)
      (implies (in arbitrary-element (all-set))
        (predicate arbitrary-element)))))

(defthmd all-by-membership
  (implies (all-hyps) (all (all-set))))

(defund subset-trigger
  (x y)
  (declare (xargs :guard (and (setp x) (setp y))))
  (subset x y))

(defthm pick-a-point-subset-strategy
  (implies (and (syntaxp (rewriting-goal-lit mfc state))
      (syntaxp (rewriting-conc-lit `(subset$inline ,SET::X ,SET::Y)
          mfc
          state)))
    (equal (subset x y)
      (subset-trigger x y))))

(automate-instantiation :new-hint-name pick-a-point-subset-hint
  :generic-theorem all-by-membership
  :generic-predicate predicate
  :generic-hyps all-hyps
  :generic-collection all-set
  :generic-collection-predicate all
  :actual-collection-predicate subset
  :actual-trigger subset-trigger
  :predicate-rewrite (((predicate ?x ?y) (in ?x ?y)))
  :tagging-theorem pick-a-point-subset-strategy)

(defthm pick-a-point-subset-constraint-helper
  (implies (syntaxp (equal set-for-all-reduction
        'set-for-all-reduction))
    (equal (subset set-for-all-reduction rhs)
      (cond ((emptyp set-for-all-reduction) t)
        ((in (head set-for-all-reduction) rhs) (subset (tail set-for-all-reduction)
            rhs))
        (t nil)))))

(defthm double-containment
  (implies (and (setp x) (setp y))
    (equal (equal x y)
      (and (subset x y)
        (subset y x))))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

(defthmd double-containment-no-backchain-limit
  (implies (and (setp x) (setp y))
    (equal (equal x y)
      (and (subset x y)
        (subset y x)))))

(defthmd sets-are-true-lists
  (implies (setp x) (true-listp x)))

(defthm sets-are-true-lists-compound-recognizer
  (implies (setp x) (true-listp x))
  :rule-classes :compound-recognizer)

(defthm sets-are-true-lists-cheap
  (implies (setp x) (true-listp x))
  :rule-classes ((:rewrite :backchain-limit-lst (1))))

(defthm tail-count
  (implies (not (emptyp x))
    (< (acl2-count (tail x))
      (acl2-count x)))
  :rule-classes ((:rewrite) (:linear)))

(defthm head-count
  (implies (not (emptyp x))
    (< (acl2-count (head x))
      (acl2-count x)))
  :rule-classes ((:rewrite) (:linear)))

(defthm tail-count-built-in
  (implies (not (emptyp x))
    (o< (acl2-count (tail x))
      (acl2-count x)))
  :rule-classes :built-in-clause)

(defthm head-count-built-in
  (implies (not (emptyp x))
    (o< (acl2-count (head x))
      (acl2-count x)))
  :rule-classes :built-in-clause)

(defthm insert-insert
  (equal (insert a (insert b x))
    (insert b (insert a x)))
  :rule-classes ((:rewrite :loop-stopper ((a b)))))

(defthm sfix-produces-set
  (setp (sfix x)))

(defthm tail-produces-set
  (setp (tail x)))

(defthm insert-produces-set
  (setp (insert a x)))

(defthm insert-never-empty
  (not (emptyp (insert a x))))

(defthm nonempty-means-set
  (implies (not (emptyp x)) (setp x)))

(defthm sfix-set-identity
  (implies (setp x)
    (equal (sfix x) x)))

(defthm emptyp-sfix-cancel
  (equal (emptyp (sfix x))
    (emptyp x)))

(defthm head-sfix-cancel
  (equal (head (sfix x)) (head x)))

(defthm tail-sfix-cancel
  (equal (tail (sfix x)) (tail x)))

(defthm insert-head
  (implies (not (emptyp x))
    (equal (insert (head x) x) x)))

(defthm insert-head-tail
  (implies (not (emptyp x))
    (equal (insert (head x) (tail x))
      x)))

(defthm repeated-insert
  (equal (insert a (insert a x))
    (insert a x)))

(defthm insert-sfix-cancel
  (equal (insert a (sfix x))
    (insert a x)))

(defthm head-when-emptyp
  (implies (emptyp x)
    (equal (head x) nil)))

(defthm tail-when-emptyp
  (implies (emptyp x)
    (equal (tail x) nil)))

(defthm insert-when-emptyp
  (implies (and (syntaxp (not (equal x ''nil)))
      (emptyp x))
    (equal (insert a x) (insert a nil))))

(defthm head-of-insert-a-nil
  (equal (head (insert a nil)) a))

(defthm tail-of-insert-a-nil
  (equal (tail (insert a nil)) nil))

(defthm sfix-when-emptyp
  (implies (emptyp x)
    (equal (sfix x) nil)))

(defthm subset-membership-tail
  (implies (and (subset x y)
      (in a (tail x)))
    (in a (tail y))))

(defthm subset-membership-tail-2
  (implies (and (subset x y)
      (not (in a (tail y))))
    (not (in a (tail x)))))

(defthm not-in-self (not (in x x)))

(defthm in-sfix-cancel
  (equal (in a (sfix x))
    (in a x)))

(defthm never-in-empty
  (implies (emptyp x)
    (not (in a x))))

(defthm in-set
  (implies (in a x) (setp x)))

(defthm in-tail
  (implies (in a (tail x))
    (in a x)))

(defthm in-tail-or-head
  (implies (and (in a x)
      (not (in a (tail x))))
    (equal (head x) a)))

(defthm in-head
  (equal (in (head x) x)
    (not (emptyp x))))

(defthm head-unique
  (not (in (head x) (tail x))))

(defthm insert-identity
  (implies (in a x)
    (equal (insert a x) x)))

(defthm in-insert
  (equal (in a (insert b x))
    (or (in a x) (equal a b))))

(defthm subset-transitive
  (and (implies (and (subset x y)
        (subset y z))
      (subset x z))
    (implies (and (subset y z)
        (subset x y))
      (subset x z))))

(defthm subset-insert-x
  (equal (subset (insert a x) y)
    (and (subset x y) (in a y))))

(defthm subset-sfix-cancel-x
  (equal (subset (sfix x) y)
    (subset x y)))

(defthm subset-sfix-cancel-y
  (equal (subset x (sfix y))
    (subset x y)))

(defthm subset-in
  (and (implies (and (subset x y) (in a x))
      (in a y))
    (implies (and (in a x) (subset x y))
      (in a y))))

(defthm subset-in-2
  (and (implies (and (subset x y)
        (not (in a y)))
      (not (in a x)))
    (implies (and (not (in a y))
        (subset x y))
      (not (in a x)))))

(defthm emptyp-subset
  (implies (emptyp x)
    (subset x y)))

(defthm emptyp-subset-2
  (implies (emptyp y)
    (equal (subset x y) (emptyp x))))

(defthm subset-reflexive
  (subset x x))

(defthm subset-insert
  (subset x (insert a x)))

(defthm subset-tail
  (subset (tail x) x)
  :rule-classes ((:rewrite) (:forward-chaining :trigger-terms ((tail x)))))

(defthm weak-insert-induction-helper-1
  (implies (and (not (in a x))
      (not (equal (head (insert a x)) a)))
    (equal (head (insert a x))
      (head x))))

(defthm weak-insert-induction-helper-2
  (implies (and (not (in a x))
      (not (equal (head (insert a x)) a)))
    (equal (tail (insert a x))
      (insert a (tail x)))))

(defthm weak-insert-induction-helper-3
  (implies (and (not (in a x))
      (equal (head (insert a x)) a))
    (equal (tail (insert a x))
      (sfix x))))

(defun weak-insert-induction
  (a x)
  (declare (xargs :guard (setp x)))
  (cond ((emptyp x) nil)
    ((in a x) nil)
    ((equal (head (insert a x)) a) nil)
    (t (list (weak-insert-induction a (tail x))))))

(defthm use-weak-insert-induction
  t
  :rule-classes ((:induction :pattern (insert a x)
     :scheme (weak-insert-induction a x))))

(defthm delete-delete
  (equal (delete a (delete b x))
    (delete b (delete a x)))
  :rule-classes ((:rewrite :loop-stopper ((a b)))))

(defthm delete-set
  (setp (delete a x)))

(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 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))

(defthm union-symmetric
  (equal (union x y) (union y x))
  :rule-classes ((:rewrite :loop-stopper ((x y)))))

(defthm union-commutative
  (equal (union x (union y z))
    (union y (union x z)))
  :rule-classes ((:rewrite :loop-stopper ((x y)))))

(defthm union-insert-x
  (equal (union (insert a x) y)
    (insert a (union x y))))

(defthm union-insert-y
  (equal (union x (insert a y))
    (insert a (union x y))))

(defthm union-delete-x
  (equal (union (delete a x) y)
    (if (in a y)
      (union x y)
      (delete a (union x y)))))

(defthm union-delete-y
  (equal (union x (delete a y))
    (if (in a x)
      (union x y)
      (delete a (union x y)))))

(defthm union-set
  (setp (union x y)))

(defthm union-sfix-cancel-x
  (equal (union (sfix x) y)
    (union x y)))

(defthm union-sfix-cancel-y
  (equal (union x (sfix y))
    (union x y)))

(defthm union-emptyp-x
  (implies (emptyp x)
    (equal (union x y) (sfix y))))

(defthm union-emptyp-y
  (implies (emptyp y)
    (equal (union x y) (sfix x))))

(defthm union-emptyp
  (equal (emptyp (union x y))
    (and (emptyp x) (emptyp y))))

(defthm union-in
  (equal (in a (union x y))
    (or (in a x) (in a y))))

(defthm union-subset-x
  (subset x (union x y)))

(defthm union-subset-y
  (subset y (union x y)))

(defthm union-with-subset-left
  (implies (subset x y)
    (equal (union x y) (sfix y)))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

(defthm union-with-subset-right
  (implies (subset x y)
    (equal (union y x) (sfix y)))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

(defthm union-self
  (equal (union x x) (sfix x)))

(defthm union-associative
  (equal (union (union x y) z)
    (union x (union y z))))

(defthm union-outer-cancel
  (equal (union x (union x z))
    (union x z)))

(defthm intersect-symmetric
  (equal (intersect x y)
    (intersect y x))
  :rule-classes ((:rewrite :loop-stopper ((x y)))))

(defthm intersect-insert-x
  (implies (not (in a y))
    (equal (intersect (insert a x) y)
      (intersect x y))))

(defthm intersect-insert-y
  (implies (not (in a x))
    (equal (intersect x (insert a y))
      (intersect x y))))

(defthm intersect-delete-x
  (equal (intersect (delete a x) y)
    (delete a (intersect x y))))

(defthm intersect-delete-y
  (equal (intersect x (delete a y))
    (delete a (intersect x y))))

(defthm intersect-set
  (setp (intersect x y)))

(defthm intersect-sfix-cancel-x
  (equal (intersect (sfix x) y)
    (intersect x y)))

(defthm intersect-sfix-cancel-y
  (equal (intersect x (sfix y))
    (intersect x y)))

(defthm intersect-emptyp-x
  (implies (emptyp x)
    (equal (intersect x y) nil)))

(defthm intersect-emptyp-y
  (implies (emptyp y)
    (equal (intersect x y) nil)))

(defthm intersect-in
  (equal (in a (intersect x y))
    (and (in a y) (in a x))))

(defthm intersect-subset-x
  (subset (intersect x y) x))

(defthm intersect-subset-y
  (subset (intersect x y) y))

(defthm intersect-with-subset-left
  (implies (subset x y)
    (equal (intersect x y) (sfix x)))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

(defthm intersect-with-subset-right
  (implies (subset x y)
    (equal (intersect y x) (sfix x)))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

(defthm intersect-self
  (equal (intersect x x) (sfix x)))

(defthm intersect-associative
  (equal (intersect (intersect x y) z)
    (intersect x (intersect y z))))

(defthmd union-over-intersect
  (equal (union x (intersect y z))
    (intersect (union x y) (union x z))))

(defthm intersect-over-union
  (equal (intersect x (union y z))
    (union (intersect x y)
      (intersect x z))))

(defthm intersect-commutative
  (equal (intersect x (intersect y z))
    (intersect y (intersect x z)))
  :rule-classes ((:rewrite :loop-stopper ((x y)))))

(defthm intersect-outer-cancel
  (equal (intersect x (intersect x z))
    (intersect x z)))

(defthm difference-set
  (setp (difference x y)))

(defthm difference-sfix-x
  (equal (difference (sfix x) y)
    (difference x y)))

(defthm difference-sfix-y
  (equal (difference x (sfix y))
    (difference x y)))

(defthm difference-emptyp-x
  (implies (emptyp x)
    (equal (difference x y) (sfix x))))

(defthm difference-emptyp-y
  (implies (emptyp y)
    (equal (difference x y) (sfix x))))

(defthm difference-in
  (equal (in a (difference x y))
    (and (in a x) (not (in a y)))))

(defthm difference-subset-x
  (subset (difference x y) x))

(defthm subset-difference
  (equal (emptyp (difference x y))
    (subset x y)))

(defthm difference-over-union
  (equal (difference x (union y z))
    (intersect (difference x y)
      (difference x z))))

(defthm difference-over-intersect
  (equal (difference x (intersect y z))
    (union (difference x y)
      (difference x z))))

(defthm difference-insert-x
  (equal (difference (insert a x) y)
    (if (in a y)
      (difference x y)
      (insert a (difference x y)))))

(defthm difference-insert-y
  (equal (difference x (insert a y))
    (delete a (difference x y))))

(defthm difference-delete-x
  (equal (difference (delete a x) y)
    (delete a (difference x y))))

(defthm difference-delete-y
  (equal (difference x (delete a y))
    (if (in a x)
      (insert a (difference x y))
      (difference x y))))

(defthm difference-preserves-subset
  (implies (subset x y)
    (subset (difference x z)
      (difference y z))))

(defthm cardinality-type
  (and (integerp (cardinality x))
    (<= 0 (cardinality x)))
  :rule-classes :type-prescription)

(defthm cardinality-zero-emptyp
  (equal (equal (cardinality x) 0)
    (emptyp x)))

(defthm cardinality-sfix-cancel
  (equal (cardinality (sfix x))
    (cardinality x)))

(defthm insert-cardinality
  (equal (cardinality (insert a x))
    (if (in a x)
      (cardinality x)
      (1+ (cardinality x)))))

(defthm delete-cardinality
  (equal (cardinality (delete a x))
    (if (in a x)
      (1- (cardinality x))
      (cardinality x))))

(defthm subset-cardinality
  (implies (subset x y)
    (<= (cardinality x) (cardinality y)))
  :rule-classes (:rewrite :linear))

(defthm proper-subset-cardinality
  (implies (and (subset x y)
      (not (subset y x)))
    (< (cardinality x) (cardinality y)))
  :rule-classes (:rewrite :linear))

(defthmd equal-cardinality-subset-is-equality
  (implies (and (setp x)
      (setp y)
      (subset x y)
      (equal (cardinality x) (cardinality y)))
    (equal (equal x y) t)))

(defthm intersect-cardinality-x
  (<= (cardinality (intersect x y))
    (cardinality x))
  :rule-classes (:rewrite :linear))

(defthm intersect-cardinality-y
  (<= (cardinality (intersect x y))
    (cardinality y))
  :rule-classes (:rewrite :linear))

(defthm expand-cardinality-of-union
  (equal (cardinality (union x y))
    (- (+ (cardinality x) (cardinality y))
      (cardinality (intersect x y)))))

(defthmd expand-cardinality-of-intersect
  (equal (cardinality (intersect x y))
    (+ (cardinality x)
      (cardinality y)
      (- (cardinality (union x y))))))

(defthm expand-cardinality-of-difference
  (equal (cardinality (difference x y))
    (- (cardinality x)
      (cardinality (intersect x y)))))

(defthm intersect-cardinality-non-subset
  (implies (not (subset x y))
    (< (cardinality (intersect x y))
      (cardinality x)))
  :rule-classes (:rewrite :linear))

(defthm intersect-cardinality-subset-2
  (equal (equal (cardinality (intersect x y))
      (cardinality x))
    (subset x y)))

(defthm intersect-cardinality-non-subset-2
  (equal (< (cardinality (intersect x y))
      (cardinality x))
    (not (subset x y))))

(defthm mergesort-set
  (setp (mergesort x)))

(defthm in-mergesort
  (equal (in a (mergesort x))
    (if (member a x)
      t
      nil)))

(defthm in-mergesort-under-iff
  (iff (in a (mergesort x))
    (member a x)))

(defthm mergesort-set-identity
  (implies (setp x)
    (equal (mergesort x) x)))

(defthmd insert-induction-case
  (implies (and (not (<< a (head x)))
      (not (equal a (head x)))
      (not (emptyp x)))
    (equal (insert (head x)
        (insert a (tail x)))
      (insert a x))))

(defthmd head-insert
  (equal (head (insert a x))
    (cond ((emptyp x) a)
      ((<< a (head x)) a)
      (t (head x)))))

(defthmd tail-insert
  (equal (tail (insert a x))
    (cond ((emptyp x) nil)
      ((<< a (head x)) x)
      ((equal a (head x)) (tail x))
      (t (insert a (tail x))))))

(defthmd head-tail-order
  (implies (not (emptyp (tail x)))
    (<< (head x) (head (tail x)))))

(defthmd head-tail-order-contrapositive
  (implies (not (<< (head x) (head (tail x))))
    (emptyp (tail x))))

(defthmd head-minimal
  (implies (<< a (head x))
    (not (in a x))))

(defthmd head-minimal-2
  (implies (in a x)
    (not (<< a (head x)))))

(defthmd setp-of-cons
  (equal (setp (cons a x))
    (and (setp x)
      (or (<< a (head x))
        (emptyp x)))))

(defthmd in-to-member
  (implies (setp x)
    (equal (in a x)
      (if (member a x)
        t
        nil))))

(defthmd not-member-when-smaller
  (implies (and (<< a (car x)) (setp x))
    (not (member a x))))

(defthmd subset-to-subsetp
  (implies (and (setp x) (setp y))
    (equal (subset x y) (subsetp x y))))

(defthmd lexorder-<<-equiv
  (implies (not (equal a b))
    (equal (equal (<< a b)
        (lexorder a b))
      t)))

(make-event (let* ((primitive-rules (get-ruleset 'primitive-rules (w state))) (order-rules (get-ruleset 'order-rules (w state)))
      (low-level-rules (get-ruleset 'low-level-rules (w state))))
    (value `(progn (def-ruleset! primitive-rules
          ',SET::PRIMITIVE-RULES)
        (def-ruleset! order-rules ',SET::ORDER-RULES)
        (def-ruleset! low-level-rules
          ',SET::LOW-LEVEL-RULES)))))

(defthm insert-under-set-equiv
  (set-equiv (insert a x)
    (cons a (sfix x))))

(defthm delete-under-set-equiv
  (set-equiv (delete a x)
    (remove-equal a (sfix x))))

(defthm union-under-set-equiv
  (set-equiv (union x y)
    (append (sfix x) (sfix y))))

(defthm intersect-under-set-equiv
  (set-equiv (intersect x y)
    (intersection-equal (sfix x)
      (sfix y))))

(defthm difference-under-set-equiv
  (set-equiv (difference x y)
    (set-difference-equal (sfix x)
      (sfix y))))

(defthm mergesort-under-set-equiv
  (set-equiv (mergesort x) x))

(defcong set-equiv
  equal
  (mergesort x)
  1
  :event-name set-equiv-implies-equal-mergesort-1)

(def-ruleset! definitions
  '(in subset
    delete
    union
    intersect
    difference
    cardinality
    mergesort))

(def-ruleset! expensive-rules
  '(pick-a-point-subset-strategy double-containment
    subset-membership-tail
    subset-membership-tail-2
    subset-transitive
    subset-in
    subset-in-2
    union-symmetric
    union-commutative
    union-delete-x
    union-delete-y
    union-with-subset-left
    union-with-subset-right
    intersect-symmetric
    intersect-commutative
    intersect-insert-x
    intersect-insert-y
    intersect-with-subset-left
    intersect-with-subset-right
    intersect-over-union
    difference-over-union
    difference-over-intersect
    difference-insert-x
    difference-delete-y
    insert-cardinality
    delete-cardinality
    in-mergesort))

(in-theory (disable* definitions expensive-rules))