;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; SMT syntax and semantics (not theory-specific)
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(declare formula type)
(declare th_holds (! f formula type))

; constants
(declare true formula)
(declare false formula)

; logical connectives
(declare not (! f formula formula))
(declare and (! f1 formula (! f2 formula formula)))
(declare or (! f1 formula (! f2 formula formula)))
(declare impl (! f1 formula (! f2 formula formula)))
(declare iff (! f1 formula (! f2 formula formula)))
(declare xor (! f1 formula (! f2 formula formula)))
(declare ifte (! b formula (! f1 formula (! f2 formula formula))))

; terms
(declare sort type)		; sort in the theory
(declare arrow (! s1 sort (! s2 sort sort)))	; function constructor

(declare term (! t sort type))	; declared terms in formula

(declare apply (! s1 sort
               (! s2 sort
               (! t1 (term (arrow s1 s2))
               (! t2 (term s1)
                (term s2))))))
                
(declare ite (! s sort
             (! f formula
             (! t1 (term s)
             (! t2 (term s)
               (term s))))))

; let/flet
(declare let (! s sort
             (! t (term s)
             (! f (! v (term s) formula)
               formula))))
(declare flet (! f1 formula
              (! f2 (! v formula formula)
                formula)))

; predicates
(declare = (! s sort
           (! x (term s)
           (! y (term s)
             formula))))

(declare distinct (! s sort
                  (! x (term s)
                  (! y (term s)
                    formula))))

; To avoid duplicating some of the rules (e.g., cong), we will view
; applications of predicates as terms of sort "Bool".
; Such terms can be injected as atomic formulas using "p_app".

(declare Bool sort)							; the special sort for predicates
(declare p_app (! x (term Bool) formula))	; propositional application of term


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Examples

; an example of "(p1 or p2(0)) and t1=t2(1)"
;(! p1 (term Bool)
;(! p2 (term (arrow Int Bool))
;(! t1 (term Int)
;(! t2 (term (arrow Int Int))
;(! F (th_holds (and (or (p_app p1) (p_app (apply _ _ p2 0)))
;                    (= _ t1 (apply _ _ t2 1))))
;  ...

; another example of "p3(a,b)"
;(! a (term Int)
;(! b (term Int)
;(! p3 (term (arrow Int (arrow Int Bool)))	; arrow is right assoc.
;(! F (th_holds (p_app (apply _ _ (apply _ _ p3 a) b))) ; apply is left assoc.
;  ...

; natural deduction rules here

(declare LEM 
  (! f formula
    (th_holds (or (not f) f))))

; bottom elim
(declare bottom_elim  
  (! f formula
  (! u bottom
    (th_holds f))))


;; not not

(declare not_not_intro
  (! f formula
  (! u (th_holds f)
    (th_holds (not (not f))))))
    
(declare not_not_elim
  (! f formula
  (! u (th_holds (not (not f)))
    (th_holds f))))

;; or elimination

(declare or_elim_1
  (! f1 formula
  (! f2 formula
  (! u1 (th_holds (not f1))
  (! u2 (th_holds (or f1 f2))
    (th_holds f2))))))
    
(declare or_elim_2
  (! f1 formula
  (! f2 formula
  (! u1 (th_holds (not f2))
  (! u2 (th_holds (or f1 f2))
    (th_holds f1))))))

;; and elimination

(declare and_intro
  (! f1 formula
  (! f2 formula
  (! u1 (th_holds f1)
  (! u2 (th_holds f2)
    (th_holds (and f1 f2)))))))

(declare and_elim_1
  (! f1 formula
  (! f2 formula
  (! u (th_holds (and f1 f2))
    (th_holds f1)))))
    
(declare and_elim_2
  (! f1 formula
  (! f2 formula
  (! u (th_holds (and f1 f2))
    (th_holds f2)))))
    
;; not impl elimination

(declare not_impl_elim_1
  (! f1 formula
  (! f2 formula
  (! u (th_holds (not (impl f1 f2)))
    (th_holds f1)))))
    
(declare not_impl_elim_2
  (! f1 formula
  (! f2 formula
  (! u (th_holds (not (impl f1 f2)))
    (th_holds (not f2))))))
    
;; impl elimination

(declare impl_intro (! f1 formula
                    (! f2 formula
                    (! i1 (! u (th_holds f1) 
                              (th_holds f2))
                      (th_holds (impl f1 f2))))))

(declare impl_elim
  (! f1 formula
  (! f2 formula
  (! u1 (th_holds f1)
  (! u2 (th_holds (impl f1 f2))  
    (th_holds f2))))))
    
;; iff elimination

(declare iff_elim_1
  (! f1 formula
  (! f2 formula
  (! u1 (th_holds (iff f1 f2))
    (th_holds (impl f1 f2))))))
    
(declare iff_elim_2
  (! f1 formula
  (! f2 formula
  (! u1 (th_holds (iff f1 f2))
    (th_holds (impl f2 f1))))))

(declare not_iff_elim_1
  (! f1 formula
  (! f2 formula
  (! u1 (th_holds (not f1))
  (! u2 (th_holds (not (iff f1 f2)))
    (th_holds f2))))))

(declare not_iff_elim_2
  (! f1 formula
  (! f2 formula
  (! u1 (th_holds f1)
  (! u2 (th_holds (not (iff f1 f2)))
    (th_holds (not f2)))))))

;; ite elimination

(declare ite_elim_1
  (! a formula
  (! b formula
  (! c formula
  (! u1 (th_holds a)
  (! u2 (th_holds (ifte a b c))
    (th_holds b)))))))
    
(declare ite_elim_2
  (! a formula
  (! b formula
  (! c formula
  (! u1 (th_holds (not a))
  (! u2 (th_holds (ifte a b c))
    (th_holds c)))))))
    
(declare ite_elim_3
  (! a formula
  (! b formula
  (! c formula
  (! u1 (th_holds (not b))
  (! u2 (th_holds (ifte a b c))
    (th_holds c)))))))
    
(declare ite_elim_2n
  (! a formula
  (! b formula
  (! c formula
  (! u1 (th_holds a)
  (! u2 (th_holds (ifte (not a) b c))
    (th_holds c)))))))

(declare not_ite_elim_1
  (! a formula
  (! b formula
  (! c formula
  (! u1 (th_holds a)
  (! u2 (th_holds (not (ifte a b c)))
    (th_holds (not b))))))))
    
(declare not_ite_elim_2
  (! a formula
  (! b formula
  (! c formula
  (! u1 (th_holds (not a))
  (! u2 (th_holds (not (ifte a b c)))
    (th_holds (not c))))))))
    
(declare not_ite_elim_3
  (! a formula
  (! b formula
  (! c formula
  (! u1 (th_holds b)
  (! u2 (th_holds (not (ifte a b c)))
    (th_holds (not c))))))))
    
(declare not_ite_elim_2n
  (! a formula
  (! b formula
  (! c formula
  (! u1 (th_holds a)
  (! u2 (th_holds (not (ifte (not a) b c)))
    (th_holds (not c))))))))