1 files changed, 73 insertions, 107 deletions
diff --git a/proofs/signatures/th_base.plf b/proofs/signatures/th_base.plf
index e66990de4..977409b6a 100755
--- a/proofs/signatures/th_base.plf
+++ b/proofs/signatures/th_base.plf
@@ -1,107 +1,73 @@
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;
-; 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"
-;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(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))))))))
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;
-; Theory of Equality and Congruence Closure
-;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-; temporary : 
-(declare trust (th_holds false))
-
-(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))))))))))))
-                
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;
+; Theory of Equality and Congruence Closure
+;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; depends on : smt.plf
+
+; sorts :
+
+(declare arrow (! s1 sort (! s2 sort sort)))	; function constructor
+
+; functions :
+
+(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
+  (! 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))))))))))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; 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.
+;  ...