(load-file "util.ath")

(domain (Set-Of T))

(declare in ((T) -> (T (Set-Of T)) Boolean))

(declare empty ((T) -> ((Set-Of T)) Boolean))

(declare null ((T) (Set-Of T)))

(define null-axiom (forall ?x (not (in ?x null))))

(define empty-axiom
  (forall ?s
    (iff (empty ?s)
      (forall ?x (not (in ?x ?s))))))


(assert empty-axiom)


(declare singl ((T) -> (T) (Set-Of T)))

(define singleton-axiom
  (forall ?x
    (forall ?y 
      (iff (in ?x (singl ?y))
	   (= ?x ?y)))))

(define singleton-axiom-1
  (forall ?x (in ?x (singl ?x))))

(assert singleton-axiom singleton-axiom-1)

(define singleton-hc-1 
  (forall* [?x ?y]
   (if (= ?x ?y)
       (in ?x (singl ?y)))))

(assert singleton-hc-1)

(declare is-singleton ((T) -> ((Set-Of T)) Boolean))

(define is-singleton-axiom
  (forall ?s
    (iff (is-singleton ?s)
	 (exists ?x (= ?s (singl ?x))))))

(assert is-singleton-axiom)            

(declare insert ((T) -> (T (Set-Of T)) (Set-Of T)))

(define insert-axiom1
  (forall ?e ?s
    (in ?e (insert ?e ?s))))

(define insert-axiom2
  (forall ?e ?e' ?s
    (if (in ?e' ?s)
        (in ?e' (insert ?e ?s)))))

(assert insert-axiom1 insert-axiom2)

(declare subset ((T) -> ((Set-Of T) (Set-Of T)) Boolean))

(define subset-axiom 
  (forall ?s1
    (forall ?s2
      (iff (subset ?s1 ?s2)
           (forall ?x
             (if (in ?x ?s1)
                 (in ?x ?s2)))))))

(assert subset-axiom)

(define ext-axiom
  (forall ?s1
    (forall ?s2
      (iff (= ?s1 ?s2)
	   (forall ?x
	     (iff (in ?x ?s1)
		  (in ?x ?s2)))))))

(assert ext-axiom)

(define set-equality
  (forall ?s1 ?s2
    (iff (= ?s1 ?s2)
	 (and (subset ?s1 ?s2) (subset ?s2 ?s1)))))

; darko commented out so that he can run this file from his account
; (!pf set-equality [ext-axiom subset-axiom])

(declare union ((T) -> ((Set-Of T) (Set-Of T)) (Set-Of T)))

(declare intersection ((T) -> ((Set-Of T) (Set-Of T)) (Set-Of T)))

(define union-axiom
  (forall ?s1 
    (forall ?s2
      (forall ?x
        (iff (in ?x (union ?s1 ?s2))
             (or (in ?x ?s1)
                 (in ?x ?s2)))))))

(assert union-axiom)

(define union-hc-1
  (forall* [?s1 ?s2 ?x]
    (if (in ?x ?s1)
	(in ?x (union ?s1 ?s2)))))

(define union-hc-2
  (forall* [?s1 ?s2 ?x]
    (if (in ?x ?s2)
	(in ?x (union ?s1 ?s2)))))

(assert union-hc-1 union-hc-2)