blob: ffa8667a4ed4cbcf9e02f521c7013034389b2448 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; 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 trust_f (! f formula (th_holds f))) ; 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 negsymm (! s sort
(! x (term s)
(! y (term s)
(! u (th_holds (not (= _ x y)))
(th_holds (not (= _ y x))))))))
(declare negtrans1 (! s sort
(! x (term s)
(! y (term s)
(! z (term s)
(! u (th_holds (not (= _ x y)))
(! u (th_holds (= _ y z))
(th_holds (not (= _ x z))))))))))
(declare negtrans2 (! s sort
(! x (term s)
(! y (term s)
(! z (term s)
(! u (th_holds (= _ x y))
(! u (th_holds (not (= _ y z)))
(th_holds (not (= _ x z))))))))))
(define negtrans negtrans1)
(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.
; ...
|
