(load-file "general-alloy.ath")


(domain NODE)
(domain ELM)

(declare Node (Set-Of NODE))
(declare Elm (Set-Of ELM))
(declare next (Set-Of (Pair-Of NODE NODE)))
(declare data (Set-Of (Pair-Of NODE ELM)))

(define next-left-constraint 
  (forall* [?x ?y]
    (if (in (tup [?x ?y]) next)
        (in (tup [?x]) Node))))

(define next-right-constraint 
  (forall* [?x ?y]
    (if (in (tup [?x ?y]) next)
        (in (tup [?y]) Node))))

(define data-left-constraint 
  (forall* [?x ?y]
    (if (in (tup [?x ?y]) data)
        (in (tup [?x]) Node))))

(define data-right-constraint 
  (forall* [?x ?y]
    (if (in (tup [?x ?y]) data)
        (in (tup [?y]) Elm))))

(define membership-constraints 
  [next-left-constraint next-right-constraint data-left-constraint data-right-constraint])


(assert membership-constraints)

(define data-is-total
  (forall ?x
    (if (in (tup [?x]) Node)
        (exists ?y
          (and (holds data [?x ?y])
	       (forall ?y' 
		 (if (holds data [?x ?y'])
		     (= ?y ?y'))))))))

(assert data-is-total)

(assert (is-function next))

;(declare elms (-> (NODE) (Set-Of (Pair-Of ELM Unit))))

;(define elms-semantics
;  (forall ?n
;     (and (if (not (exists ?m (holds next [?n ?m])))
;              (= (elms ?n) (sbdot (scalar ?n) data)))
;          (forall ?m
;            (if (holds next [?n ?m])
;	        (= (elms ?n) (union (sbdot (scalar ?n) data) (elms ?m))))))))


(declare elms (-> ((Set-Of NODE)) (Set-Of ELM)))

(define elms-def
  (forall ?node-set ?result
    (iff (= (elms ?node-set) ?result)
	 (and (is-singleton ?node-set)
	      (and (subset ?node-set Node)
	           (and (if (empty (sbdot ?node-set next)) 
			    (= ?result (sbdot ?node-set data)))
                        (if (not (empty (sbdot ?node-set next)))
			    (= ?result (union (sbdot ?node-set data) (elms (sbdot ?node-set ?next)))))))))))

(assert elms-def)

(define elms-def-1
  (forall ?n
    (if (empty (sbdot (scalar ?n) next))
	(= (elms (scalar ?n)) (sbdot (scalar ?n) data)))))

(!pf elms-def-1 [elms-def singleton-def is-singleton-def id-axiom]) 

(define elms-def-2
  (forall ?n
    (if (not (empty (sbdot (scalar ?n) next)))
	(= (elms (scalar ?n)) (union (sbdot (scalar ?n) data) (elms (sbdot (scalar ?n) next)))))))

;; elms-axiom-2:  "ALL n | ~ empty({[n]}.next) ==> elms({[n]}) =  {[n]}.data union elms({[n]}.next)")

(!pf elms-def-2 [elms-def singleton-def is-singleton-def id-axiom]) 

(define acyclicity
  (forall ?n 
    (not (in (tup [?n]) (sbdot (scalar ?n) (tc next))))))

  
(assert acyclicity)

(primitive-method (list-induction ind-goal)
  (let ((base (forall ?n (if (not (exists ?m (holds next [?n ?m])))
			     (ind-goal ?n))))
	(step (forall ?n ?m
		  (if (holds next [?n ?m])
		      (if (ind-goal ?m)
			  (ind-goal ?n))))))
   (check ((& (holds? base)
	      (holds? step)
	      (holds? acyclicity)) (forall ?n (ind-goal ?n))))))