1 files changed, 33 insertions, 67 deletions
diff --git a/proofs/signatures/th_base.plf b/proofs/signatures/th_base.plf
index 7b0b086dc..977409b6a 100755
--- a/proofs/signatures/th_base.plf
+++ b/proofs/signatures/th_base.plf
@@ -1,80 +1,28 @@
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;
-; Atomization / Clausification
-;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-; 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)
-         (holds cln)))
-    (holds cln))))
-
-; 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)
-    (holds cln)))
 
 
-(declare th_let_pf
-  (! f formula
-  (! u (th_holds f)
-  (! u2 (! v (th_holds f) (holds cln))
-    (holds cln)))))
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;
-; 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"
+; Theory of Equality and Congruence Closure
 ;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; depends on : smt.plf
 
-(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))))))))
+; sorts :
 
-(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 arrow (! s1 sort (! s2 sort sort)))	; function constructor
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;
-; Theory of Equality and Congruence Closure
-;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; functions :
 
-; temporary :
-(declare trust (th_holds false))
+(declare apply (! s1 sort
+               (! s2 sort
+               (! t1 (term (arrow s1 s2))
+               (! t2 (term s1)
+                (term s2))))))
+                
+                
+; inference rules :
+
+(declare trust (th_holds false))	; temporary
 
 (declare refl
   (! s sort
@@ -105,3 +53,21 @@
               (! u2 (th_holds (= _ a2 b2))
                 (th_holds (= _ (apply _ _ a1 a2) (apply _ _ b1 b2))))))))))))
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; 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.
+;  ...