;(load-file "FINAL.ath")

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

;======================= TWO SIMPLE LEMMAS ========================

(define elms-lemma-1 "ALL n | {n}.data subset ({n}.next*).data")
(define elms-lemma-2 "ALL n | {n}.data subset elms({n})")

(!prove elms-lemma-1 [subset-rtc-lemma comp-lemma])
(!prove elms-lemma-2 [elms-def-1 elms-def-2 union-def subset-def])

;===============================  SOUNDNESS ==========================

(define base-step "ALL n | ~(EXISTS m | [n m] in next) ==> elms({n}) subset ({n}.next*).data)")
(!prove base-step [elms-def-1 empty-def scalar-lemma elms-lemma-1])

(define (ind-goal n)
  (subset "elms({n})" 
          "({n}.next*).data"))

(define ind-step
  (pick-any x y
      (assume-let ((hyp "[x y] in next")
                   (ihyp (ind-goal y)))
        (dlet ((P1 (!prove "elms({x}) = {x}.data union elms({y})" 
			[elms-def-2 hyp fun-lemma (is-fun next) scalar-lemma empty-def]))
	       (P2 (!prove "{y}.next* subset {x}.next*" [hyp comp-monotonicity scalar-lemma first-power-lemma]))
               (P3 (!prove "({y}.next*).data subset ({x}.next*).data" [P2 comp-lemma]))
               (P4 (!prove "elms({y}) subset ({x}.next*).data" [P3 ihyp subset-trans])))
          (!prove "elms({x}) subset ({x}.next*).data" [P1 elms-lemma-1 P4 union-lemma id-axiom])))))

(define Elm-Soundness (!list-induction ind-goal))

;======================= COMPLETENESS ==============================

(define ind-lemma "ALL k m n x | [n m] in next^k & [m x] in data ==> x in elms({n})")

(define (goal k) (forall ?m ?n ?x "[n m] in next^k & [m x] in data  ==> x in elms({n})"))

(by-induction-on ?k (goal ?k)
  (zero (!prove (goal zero) [elms-lemma-2 pow-def scalar-lemma subset-def]))
  ((succ k) (pick-any m n x 
	      (assume-let ((hyp "[n m] in next^k+1 & [m x] in data"))
                (!prove "x in elms({n})" [hyp (goal k)  pow-def-2 fun-lemma (is-fun next) 
					    scalar-lemma empty-def elms-def-2 union-def])))))

(define Elm-Completeness "ALL n | ({n}.next*).data subset elms({n})")

(Elm-Completeness BY 
  (pick-any n 
    (!prove-subsets "({n}.next*).data" "elms({n})"
                    [elms-def star-pow-lemma scalar-lemma ind-lemma])))

;; -------------- FINAL EQUALITY CONCLUSION --------------- 

(!prove "ALL n | elms({n}) = ({n}.next*).data" [Elm-Soundness Elm-Completeness set-equality])