diff options
Diffstat (limited to 'proofs/signatures/th_arrays.plf')
| -rwxr-xr-x | proofs/signatures/th_arrays.plf | 53 |
1 files changed, 53 insertions, 0 deletions
diff --git a/proofs/signatures/th_arrays.plf b/proofs/signatures/th_arrays.plf new file mode 100755 index 000000000..6e0e6438d --- /dev/null +++ b/proofs/signatures/th_arrays.plf @@ -0,0 +1,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)))))))))
+
\ No newline at end of file |