;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; Atomization
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 

; binding between an LF var and an (atomic) formula
(declare atom (! v var (! p formula type)))

(declare decl_atom
  (! f formula
  (! u (! v var 
       (! a (atom v f)
         bottom))
    bottom)))
    
; direct clausify
(declare clausify_form
  (! f formula
  (! v var
  (! a (atom v f)
  (! u (th_holds f)
    (holds (clc (pos v) cln)))))))
    
(declare clausify_form_not
  (! f formula
  (! v var
  (! a (atom v f)
  (! u (th_holds (not f))
    (holds (clc (neg v) cln)))))))

(declare clausify_false
  (! u (th_holds false)
    bottom))

(declare let_pf 
  (! c clause
  (! c' clause
  (! u (holds c)
  (! u2 (! v (holds c) bottom)
    bottom)))))
    
(declare th_let_pf
  (! f formula
  (! u (th_holds f)
  (! u2 (! v (th_holds f) bottom)
    bottom))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; Theory reasoning
; - make a series of assumptions and then derive a contradiction (or false)
; - then the assumptions yield a formula like "v1 -> v2 -> ... -> vn -> false"
; - In CNF, it becomes a clause: "~v1, ~v2, ..., ~vn"
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(declare ast
  (! v var
  (! f formula
  (! C clause
  (! r (atom v f)       ;this is specified
  (! u (! o (th_holds f)
         (holds C))
    (holds (clc (neg v) C))))))))

(declare asf
  (! v var
  (! f formula
  (! C clause
  (! r (atom v f)
  (! u (! o (th_holds (not f))
         (holds C))
    (holds (clc (pos v) C))))))))

(declare contra
  (! f formula
  (! r1 (th_holds f)
  (! r2 (th_holds (not f))
    (holds cln)))))

(declare th_ast
  (! f formula
  (! u (! o (th_holds f)
         (holds cln))
    (th_holds (not f)))))
    
(declare th_asf
  (! f formula
  (! u (! o (th_holds (not f))
         (holds cln))
    (th_holds f))))
    
(declare lem
  (! f formula
  (! v var
  (! a (atom v f)
    (holds (clc (pos v) (clc (neg v) cln)))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; Theory of Equality and Congruence Closure
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(declare refl
  (! s sort
  (! t (term s)
    (th_holds (= s t t)))))

(declare symm (! s sort
              (! x (term s)
              (! y (term s)
              (! u (th_holds (= _ x y))
                (th_holds (= _ y x)))))))

(declare trans (! s sort
               (! x (term s)
               (! y (term s)
               (! z (term s)
               (! u (th_holds (= _ x y))
               (! u (th_holds (= _ y z))
                 (th_holds (= _ x z)))))))))

(declare cong (! s1 sort
              (! s2 sort
              (! a1 (term (arrow s1 s2))
              (! b1 (term (arrow s1 s2))
              (! a2 (term s1)
              (! b2 (term s1)
              (! u1 (th_holds (= _ a1 b1))
              (! u2 (th_holds (= _ a2 b2))
                (th_holds (= _ (apply _ _ a1 a2) (apply _ _ b1 b2))))))))))))