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


(domain NODE)
(domain ELM)

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

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

(define next-is-partial-fun
  (forall* [?x ?y ?y']
    (if (and (holds next [?x ?y])
             (holds next [?x ?y']))
        (= ?y ?y'))))

(assert next-is-partial-fun)

;(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 (Pair-Of NODE Unit)) (Set-Of (Pair-Of ELM Unit))) Boolean))

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

(define elms-axiom-1
  (forall ?n 
    (if (not (exists ?m (holds next [?n ?m])))
	(forall ?S 
	  (iff (elms (scalar ?n) ?S)
	       (= ?S (sbdot (scalar ?n) data)))))))

(define elms-axiom-2
  (forall ?n 
    (if (exists ?m (holds next [?n ?m]))
	(forall ?S 
	  (iff (elms (scalar ?n) ?S)
	       (exists ?S' (and (elms (scalar ?m) ?S')
				(= ?S (union ?S' (sbdot (scalar ?n) data))))))))))



(assert elms-semantics elms-axiom-1 elms-axiom-2)


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