1(in-package "ACL2")
2
3
4#|
5
6     records.lisp
7     ~~~~~~~~~~~~
8
9We define properties of a generic record accessor function and updater
10function.  The basic functions are (g a r) and (s a v r) where a is an
11address/key, v is a value, r is a record, and (g a r) returns the
12value set to address a in record r, and (s a v r) returns a new record
13with address a set to value v in record r.
14
15We normalize the record structures (which allows the 'equal-ity based
16rewrite rules) as alists where the keys (cars) are ordered using
17Pete's total-order added to ACL2. We define a set of -aux functions
18which assume well-formed records -- defined by rcdp -- and then prove
19the desired properties using hypothesis assuming well-formed objects.
20
21We then remove these well-formed object hypothesis by defining a invertible
22mapping (acl2->rcd) from any ACL2 object to a well-formed records. We then
23prove the desired properties using the proper translations of the -aux
24functions to the acl2 objects, and subsequently remove the well-founded
25hypothesis.
26
27|#
28
29(include-book "apply-total-order")
30
31;; BEGIN records definitions.
32
33(defun rcdp (x)
34  (or (null x)
35      (and (consp x)
36           (consp (car x))
37           (rcdp (cdr x))
38           (cdar x)
39           (or (null (cdr x))
40               (<< (caar x) (caadr x))))))
41
42(defun ifrp (x) ;; ill-formed rcdp
43  (or (not (rcdp x))
44      (and (consp x)
45           (null (cdr x))
46           (consp (car x))
47           (null (caar x))
48           (ifrp (cdar x)))))
49
50(defun acl2->rcd (x)
51  (if (ifrp x) (list (cons nil x)) x))
52
53(defun rcd->acl2 (x)
54  (if (ifrp x) (cdar x) x))
55
56(defun g-aux (a x)
57  (cond ((or (endp x)
58             (<< a (caar x)))
59         nil)
60        ((equal a (caar x))
61         (cdar x))
62        (t
63         (g-aux a (cdr x)))))
64
65(defun g (a x)
66  (g-aux a (acl2->rcd x)))
67
68(defun s-aux (a v r)
69  (cond ((or (endp r)
70             (<< a (caar r)))
71         (if v (cons (cons a v) r) r))
72        ((equal a (caar r))
73         (if v (cons (cons a v) (cdr r)) (cdr r)))
74        (t
75         (cons (car r) (s-aux a v (cdr r))))))
76
77(defun s (a v x)
78  (rcd->acl2 (s-aux a v (acl2->rcd x))))
79
80(defun keys-aux (x)
81  (cond ((endp x)
82         ())
83        (t (cons (caar x)
84                 (keys-aux (cdr x))))))
85
86(defun keys (x)
87  (keys-aux (acl2->rcd x)))
88
89
90
91;;;; basic property of records ;;;;
92
93(local
94(defthm rcdp-implies-true-listp
95  (implies (rcdp x)
96           (true-listp x))
97  :rule-classes (:forward-chaining
98                 :rewrite)))
99
100
101;;;; initial properties of s-aux and g-aux ;;;;
102
103(local
104(defthm s-aux-is-bounded
105  (implies (and (rcdp r)
106                (s-aux a v r)
107                (<< e a)
108                (<< e (caar r)))
109           (<< e (caar (s-aux a v r))))))
110
111(local
112(defthm s-aux-preserves-rcdp
113  (implies (rcdp r)
114           (rcdp (s-aux a v r)))))
115
116(local
117(defthm g-aux-same-s-aux
118  (implies (rcdp r)
119           (equal (g-aux a (s-aux a v r))
120                  v))))
121
122(local
123(defthm g-aux-diff-s-aux
124  (implies (and (rcdp r)
125                (not (equal a b)))
126           (equal (g-aux a (s-aux b v r))
127                  (g-aux a r)))))
128
129(local
130(defthm s-aux-same-g-aux
131  (implies (rcdp r)
132           (equal (s-aux a (g-aux a r) r)
133                  r))))
134
135(local
136(defthm s-aux-same-s-aux
137  (implies (rcdp r)
138           (equal (s-aux a y (s-aux a x r))
139                  (s-aux a y r)))))
140
141(local
142(defthm s-aux-diff-s-aux
143  (implies (and (rcdp r)
144                (not (equal a b)))
145           (equal (s-aux b y (s-aux a x r))
146                  (s-aux a x (s-aux b y r))))
147  :rule-classes ((:rewrite :loop-stopper ((b a s))))))
148
149(local
150(defthm s-aux-non-nil-cannot-be-nil
151  (implies (and v (rcdp r))
152           (s-aux a v r))))
153
154(local
155(defthm g-aux-is-nil-for-<<
156  (implies (and (rcdp r)
157                (<< a (caar r)))
158           (equal (g-aux a r) nil))))
159
160(local
161(defthm g-keys-aux-relationship
162  (implies (rcdp r)
163           (iff (memberp a (keys-aux r))
164                (g-aux a r)))))
165
166(local
167(defthm s-keys-aux-reduction
168  (implies (rcdp r)
169           (equal (keys-aux (s-aux a v r))
170                  (if v
171                      (insert a (keys-aux r))
172                    (drop a (keys-aux r)))))))
173
174(local
175(defthm keys-aux-are-ordered
176  (implies (rcdp r)
177           (orderedp (keys-aux r)))))
178
179
180;;;; properties of acl2->rcd and rcd->acl2 ;;;;
181
182(local
183(defthm acl2->rcd-rcd->acl2-of-rcdp
184  (implies (rcdp x)
185           (equal (acl2->rcd (rcd->acl2 x))
186                  x))))
187
188(local
189(defthm acl2->rcd-returns-rcdp
190  (rcdp (acl2->rcd x))))
191
192(local
193(defthm acl2->rcd-preserves-equality
194  (iff (equal (acl2->rcd x) (acl2->rcd y))
195       (equal x y))))
196
197(local
198(defthm rcd->acl2-acl2->rcd-inverse
199  (equal (rcd->acl2 (acl2->rcd x)) x)))
200
201(local
202(defthm rcd->acl2-of-record-non-nil
203  (implies (and r (rcdp r))
204           (rcd->acl2 r))))
205
206(in-theory (disable acl2->rcd rcd->acl2))
207
208
209;;;; final properties of record g(et) and s(et) ;;;;
210
211(defthm g-same-s
212  (equal (g a (s a v r))
213	 v))
214
215(defthm g-diff-s
216  (implies (not (equal a b))
217           (equal (g a (s b v r))
218                  (g a r))))
219
220;;;; NOTE: I often use the following instead of the above rules
221;;;; to force ACL2 to do a case-split. In some cases, I will
222;;;; disable this rule ACL2 is sluggish or if the number of cases
223;;;; is unreasonable
224
225(defthm g-of-s-redux
226  (equal (g a (s b v r))
227         (if (equal a b) v (g a r))))
228
229(in-theory (disable g-of-s-redux))
230
231(defthm s-same-g
232  (equal (s a (g a r) r)
233	 r))
234
235(defthm s-same-s
236  (equal (s a y (s a x r))
237	 (s a y r)))
238
239(defthm s-diff-s
240  (implies (not (equal a b))
241           (equal (s b y (s a x r))
242                  (s a x (s b y r))))
243  :rule-classes ((:rewrite :loop-stopper ((b a s)))))
244
245(defthm g-keys-relationship
246  (iff (memberp a (keys r))
247       (g a r)))
248
249(defthm s-keys-reduction
250  (equal (keys (s a v r))
251         (if v
252             (insert a (keys r))
253           (drop a (keys r)))))
254
255(defthm keys-are-ordered
256  (orderedp (keys r)))
257
258(defthm g-of-nil-is-nil
259  (not (g a nil)))
260
261(defthm s-non-nil-cannot-be-nil
262  (implies v (s a v r))
263  :hints (("Goal"
264           :in-theory (disable rcd->acl2-of-record-non-nil)
265           :use (:instance rcd->acl2-of-record-non-nil
266                           (r (s-aux a v (acl2->rcd r)))))))
267
268(defthm non-nil-if-g-non-nil
269  (implies (g a r) r)
270  :rule-classes :forward-chaining)
271
272
273(defthm s-same-g-back-chaining
274  (implies (equal v (g a r))
275           (equal (s a v r) r)))
276
277
278;; We disable s and g, assuming the rules proven in this book are sufficient to
279;; manipulate record terms which are encountered
280
281(in-theory (disable s g keys))
282
283(defmacro <- (x a) `(g ,a ,x))
284
285(defmacro -> (x a v) `(s ,a ,v ,x))
286
287(defun update-macro (upds result)
288  (declare (xargs :guard (keyword-value-listp upds)))
289  (if (endp upds) result
290    (update-macro (cddr upds)
291                  (list 's (car upds) (cadr upds) result))))
292
293(defmacro update (old &rest updates)
294  (declare (xargs :guard (keyword-value-listp updates)))
295  (update-macro updates old))
296
297
298
299
300