;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; Theory of Arrays
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; depends on : th_base.plf

; sorts

(declare Array (! s1 sort (! s2 sort sort)))	; s1 is index, s2 is element

; functions
(declare write (! s1 sort
               (! s2 sort
                 (term (arrow (Array s1 s2)
                       (arrow s1
                       (arrow s2 (Array s1 s2))))))))

(declare read (! s1 sort
              (! s2 sort
              	(term (arrow (Array s1 s2)
               	      (arrow s1 s2))))))

; inference rules

; read( a[i] = b, i ) == b
(declare row1 (! s1 sort
              (! s2 sort
              (! t1 (term (Array s1 s2))
              (! t2 (term s1)
              (! t3 (term s2)
              	(th_holds (= _
		(apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t3)) t2) t3))))))))

(declare row (! s1 sort
             (! s2 sort
             (! t2 (term s1)
             (! t3 (term s1)
             (! t1 (term (Array s1 s2))
             (! t4 (term s2)
             (! u (th_holds (not (= _ t2 t3)))
               (th_holds (= _ (apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t4)) t3)
               		      (apply _ _ (apply _ _ (read s1 s2) t1) t3)))))))))))

(declare negativerow (! s1 sort
                     (! s2 sort
                     (! t2 (term s1)
                     (! t3 (term s1)
                     (! t1 (term (Array s1 s2))
                     (! t4 (term s2)
		     (! u (th_holds (not (= _
                        (apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t4)) t3)
                        (apply _ _ (apply _ _ (read s1 s2) t1) t3))))
                     (th_holds (= _ t2 t3))))))))))

(declare ext (! s1 sort
             (! s2 sort
             (! t1 (term (Array s1 s2))
             (! t2 (term (Array s1 s2))
             (! u1 (! k (term s1)
                   (! u2 (th_holds (or (= _ t1 t2) (not (= _ (apply _ _ (apply _ _ (read s1 s2) t1) k) (apply _ _ (apply _ _ (read s1 s2) t2) k)))))
                     (holds cln)))
               (holds cln)))))))