(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 (empty (sbdot (scalar ?n) next))
		  (= ?S (sbdot (scalar ?n) data)))
	      (if (not (empty (sbdot (scalar ?n) next)))
                (exists ?m ?S' 
                  (and (holds next [?n ?m])
		       (and (elms (scalar ?m) ?S')
		            (= ?S (union ?S' (sbdot (scalar ?n) data)))))))))))


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

(define elms-semantics-2
  (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]))
		  (forall ?S' (if (elms (scalar ?m) ?S')
				   (= ?S (union ?S' (sbdot (scalar ?n) data))))))))))

;; "ALL n | empty({[n]}.next) ==> (ALL S | elms({[n]},S) <==> S = {[n]}.data)")
(define elms-axiom-1 
(forall ?n
  (if (empty (sbdot (singl (cons ?n unit))
                     next))
      (forall ?S
        (iff (elms (singl (cons ?n unit))
                   ?S)
             (= ?S
                (sbdot (singl (cons ?n unit))
                       data)))))))




;;"ALL n | ~ empty({[n]}.next) ==> (ALL S | elms({[n]},S) <==> (EXISTS m S' | [n m] in next & elms({[m]},S') & S = S' union {[n]}.data))")

(define elms-axiom-2
(forall ?n
  (if (not (empty (sbdot (singl (cons ?n unit))
                           next)))
      (forall ?S
        (iff (elms (singl (cons ?n unit))
                   ?S)
             (exists ?m
               (exists ?S'
                 (and (in (cons ?n
                                (cons ?m unit))
                          next)
                      (and (elms (singl (cons ?m unit))
                                 ?S')
                           (= ?S
                              (union ?S'
                                     (sbdot (singl (cons ?n unit))
                                            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))))))