diff options
Diffstat (limited to 'proofs/signatures/th_base.plf')
| -rwxr-xr-x | proofs/signatures/th_base.plf | 214 |
1 files changed, 107 insertions, 107 deletions
diff --git a/proofs/signatures/th_base.plf b/proofs/signatures/th_base.plf index e66990de4..7b0b086dc 100755 --- a/proofs/signatures/th_base.plf +++ b/proofs/signatures/th_base.plf @@ -1,107 +1,107 @@ -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;
-; 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))))))))))))
-
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; +; 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)))))))))))) + |