blob: 6e0e6438d0e1587d88c45cae84d5341c48f7b7a7 (
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
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; Theory of Arrays
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; depdends on : th_base.plf
; sorts
(declare array (! s1 sort (! s2 sort sort))) ; s1 is index, s2 is element
; functions
(declare write (! s1 sort
(! s2 sort
(! t1 (term (array s1 s2))
(! t2 (term s1)
(! t3 (term s2)
(term (array s1 s2))))))))
(declare read (! s1 sort
(! s2 sort
(! t1 (term (array s1 s2))
(! t2 (term s1)
(term s2))))))
; inference rules
(declare row1 (! s1 sort
(! s2 sort
(! t1 (term (array s1 s2))
(! t2 (term s1)
(! t3 (term s2)
(th_holds (= _ (read (write t1 t2 t3) t2) t3))))))))
(declare row (! s1 sort
(! s2 sort
(! t1 (term (array s1 s2))
(! t2 (term s1)
(! t3 (term s1)
(! t4 (term s2)
(! u (th_holds (not (= _ t2 t3)))
(th_holds (= _ (read (write t1 t2 t4) t3) (read t1 t3))))))))))
(declare ext (! s1 sort
(! s2 sort
(! f formula
(! t1 (term (array s1 s2))
(! t2 (term (array s1 s2))
(! u (th_holds (not (= _ t1 t2)))
(! u1 (! k (term s1)
(! u2 (th_holds (not (= _ (read t1 k) (read t2 k))))
(th_holds f)))
(th_holds f)))))))))
|
