;; ---------------------------------------------------------------------------
;;  ~/events/sets.events
;; ---------------------------------------------------------------------------
;; This is the set theory needed for the proof.
;; Major portions of it are taken from Matt Kaufmann's set library.
;; ---------------------------------------------------------------------------

;; The function subset should probably be named subbag.

(defn subsetp (a b)
  (if (nlistp a)
      T
      (and (member (car a) b)
	   (subsetp (cdr a) b))))

;; A proper set has no duplicates.

(defn setp (l)
  (if (not (listp l))
      t
      (and (not (member (car l) (cdr l)))
	   (setp (cdr l)))))

;; The cardinality of a set is just the length of the list representing it.

(defn card (l) 
  (if (listp l)
      (add1 (card (cdr l)))
      0))

;; The intersection of two sets is all elements that are members in both.

(defn intersection (x y)
  (if (listp x)
      (if (member (car x) y)
	  (cons (car x) (intersection (cdr x) y))
	  (intersection (cdr x) y))
      nil))

;; This function will make a proper set out of the elements of a list.

(defn mk-unique-set (set)
 (if (nlistp set)
     nil
     (union (car set) (mk-unique-set (cdr set)))))

(deftheory sets (subsetp setp card intersection mk-unique-set))

(disable-theory sets)