← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/1999/ivy/ivy-v2/ivy-sources/sets.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/1999/ivy/ivy-v2/ivy-sources/sets.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
;; This book is about set operations on lists.  The definitions
 
4
;; of member-equal, subsetp-equal, and union-equal are built into
 
5
;; ACL2.  Here we define remove-equal, set-equal, setp, and disjoint.
 
6
;;
 
7
;; The lemmas are just what arose in practice, without much thought
 
8
;; on designing good sets of rewrite rules for these operations.
 
9
;;
 
10
;; This includes some congruence theorems for set-equal.
 
11
 
 
12
;;-----------------------
 
13
;; First, some properties of subsetp-equal, member-equal, union-equal.
 
14
 
 
15
;;-----------------------
 
16
;; subsetp-equal
 
17
 
 
18
(defthm subset-cons
 
19
  (implies (subsetp-equal a b)
 
20
           (subsetp-equal a (cons x b))))
 
21
 
 
22
(defthm subset-reflexive
 
23
  (subsetp-equal x x))
 
24
 
 
25
(defthm subsetp-equal-transitive
 
26
  (implies (and (subsetp-equal x y)
 
27
                (subsetp-equal y z))
 
28
           (subsetp-equal x z)))
 
29
 
 
30
(defthm subset-member-subset-cons
 
31
  (implies (and (subsetp-equal a b)
 
32
                (member-equal x b))
 
33
           (subsetp-equal (cons x a) b)))
 
34
 
 
35
(defthm not-member-subset
 
36
  (implies (and (not (member-equal a y))
 
37
                (subsetp-equal x y))
 
38
           (not (member-equal a x))))
 
39
 
 
40
(defun subset-skolem (a b)  ;; first member of a not in b
 
41
  (declare (xargs :guard (and (true-listp a) (true-listp b))))
 
42
  (cond ((atom a) nil)
 
43
        ((not (member-equal (car a) b)) (car a))
 
44
        (t (subset-skolem (cdr a) b))))
 
45
 
 
46
(defthm subset-skolem-lemma
 
47
  (implies (implies (member-equal (subset-skolem a b) a)
 
48
                    (member-equal (subset-skolem a b) b))
 
49
           (subsetp-equal a b))
 
50
  :rule-classes nil)
 
51
 
 
52
;;-----------------------
 
53
;; union-equal
 
54
 
 
55
(defthm union-equal-preserves-true-listp
 
56
  (implies (true-listp y)
 
57
           (true-listp (union-equal x y))))
 
58
 
 
59
(defthm union-nil-left
 
60
  (equal (union-equal nil x) x))
 
61
 
 
62
(defthm union-nil-right
 
63
  (implies (true-listp x)
 
64
           (equal (union-equal x nil) x)))
 
65
 
 
66
(defthm member-union-or
 
67
  (implies (or (member-equal x a)
 
68
               (member-equal x b))
 
69
           (member-equal x (union-equal a b))))
 
70
 
 
71
(defthm not-member-union-equal
 
72
  (implies (and (not (member-equal x a))
 
73
                (not (member-equal x b)))
 
74
           (not (member-equal x (union-equal a b)))))
 
75
 
 
76
(defthm union-not-nil-if-either-argument-is-a-cons
 
77
  (implies (or (consp x) (consp y))
 
78
           (union-equal x y)))
 
79
 
 
80
(defthm subset-union-2
 
81
  (implies (subsetp-equal a b)
 
82
           (equal (union-equal a b) b)))
 
83
 
 
84
(defthm union-equal-idempotent
 
85
  (equal (union-equal x x) x))
 
86
 
 
87
(defthm subset-union-3
 
88
  (implies (and (subsetp-equal a c)
 
89
                (subsetp-equal b c))
 
90
           (subsetp-equal (union-equal a b) c)))
 
91
 
 
92
(defthm subset-union
 
93
  (implies (and (subsetp-equal a b)
 
94
                (subsetp-equal c d))
 
95
           (subsetp-equal (union-equal a c)
 
96
                          (union-equal b d))))
 
97
 
 
98
(defthm subset-union-4
 
99
  (implies (subsetp-equal a b)
 
100
           (subsetp-equal a (union-equal c b))))
 
101
 
 
102
(defthm subset-union-left-2
 
103
  (implies (subsetp-equal a b)
 
104
           (subsetp-equal a (union-equal b c))))
 
105
 
 
106
(defthm subset-union-left-not
 
107
  (implies (not (subsetp-equal a c))
 
108
           (not (subsetp-equal (union-equal a b) c))))
 
109
                 
 
110
(defthm subset-union-right-not
 
111
  (implies (not (subsetp-equal b c))
 
112
           (not (subsetp-equal (union-equal a b) c))))
 
113
 
 
114
;;-----------------------
 
115
;; Function remove-equal (x lst) removes all occurrences of x.
 
116
 
 
117
; Matt K.: Commented out after v2-9-3 because remove-equal is now defined in
 
118
; axioms.lisp, very slightly differently.
 
119
;(defun remove-equal (x l)
 
120
;  (declare (xargs :guard (true-listp l)))
 
121
;  (cond ((atom l) l)
 
122
;       ((equal x (car l)) (remove-equal x (cdr l)))
 
123
;       (t (cons (car l) (remove-equal x (cdr l))))))
 
124
 
 
125
(defthm removed-element-is-not-member
 
126
  (not (member-equal x (remove-equal x a))))
 
127
 
 
128
(defthm subset-equal-remove
 
129
  (implies (subsetp-equal a b)
 
130
           (subsetp-equal (remove-equal x a)
 
131
                          (remove-equal x b)))
 
132
  :hints (("Goal" :do-not generalize)))
 
133
 
 
134
(defthm not-member-not-member-remove
 
135
  (implies (not (member-equal y a))
 
136
           (not (member-equal y (remove-equal x a)))))
 
137
 
 
138
(defthm remove-distributes-over-union
 
139
  (equal (remove-equal x (union-equal a b))
 
140
         (union-equal (remove-equal x a) (remove-equal x b)))
 
141
  :hints (("Goal"
 
142
           :do-not generalize)))
 
143
 
 
144
(defthm subset-cons-remove
 
145
  (subsetp-equal a (cons x (remove-equal x a))))
 
146
 
 
147
(defthm subset-remove-append-one
 
148
  (subsetp-equal a (append (remove-equal x a) (list x))))
 
149
 
 
150
(defthm not-equal-member-remove
 
151
  (implies (and (not (equal x v1))
 
152
                (member-equal x a))
 
153
           (member-equal x (remove-equal v1 a))))
 
154
 
 
155
(defthm remove-equal-commutative
 
156
  (equal (remove-equal x (remove-equal y a))
 
157
         (remove-equal y (remove-equal x a))))
 
158
 
 
159
(defthm remove-equal-idempotent
 
160
  (equal (remove-equal x (remove-equal x a))
 
161
         (remove-equal x a)))
 
162
 
 
163
(defthm true-listp-remove-equal
 
164
  (implies (true-listp l)
 
165
           (true-listp (remove-equal x l))))
 
166
 
 
167
;;-----------------------
 
168
;; set-equal (nonrecursive)  (I now think recursive might be better.)
 
169
 
 
170
(defun set-equal (a b)
 
171
  (declare (xargs :guard (and (true-listp a)
 
172
                              (true-listp b))))
 
173
  (and (subsetp-equal a b)
 
174
       (subsetp-equal b a)))
 
175
 
 
176
(defthm set-equal-reflexive
 
177
  (set-equal x x))
 
178
 
 
179
(defequiv set-equal)
 
180
 
 
181
(defcong set-equal set-equal (union-equal a b) 1)
 
182
 
 
183
(defcong set-equal set-equal (union-equal a b) 2)
 
184
 
 
185
(defcong set-equal set-equal (remove-equal x a) 2)
 
186
 
 
187
(defcong set-equal set-equal (cons x a) 2)
 
188
 
 
189
(defthm member-append-left
 
190
  (implies (member-equal x a)
 
191
           (member-equal x (append a b))))
 
192
 
 
193
(defthm member-append-right
 
194
  (implies (member-equal x b)
 
195
           (member-equal x (append a b))))
 
196
 
 
197
(defthm subset-append-left
 
198
  (implies (subsetp-equal a b)
 
199
           (subsetp-equal (append a c) (append b c))))
 
200
 
 
201
(defcong set-equal set-equal (append a b) 1)
 
202
 
 
203
(defcong set-equal set-equal (append a b) 2)
 
204
 
 
205
(defthm set-equal-member-equal-cons
 
206
  (implies (member-equal x a)
 
207
           (set-equal (cons x a) a)))
 
208
 
 
209
(defthm set-equal-nil
 
210
  (not (set-equal nil (cons x a))))
 
211
 
 
212
;;---------------------------------------------------------------
 
213
;; A collection of rewrite rules for canonicalizing union-equal expressions.
 
214
 
 
215
(defthm union-equal-commute-subset
 
216
  (subsetp-equal (union-equal a b) (union-equal b a)))
 
217
 
 
218
(defthm union-equal-commutative
 
219
  (set-equal (union-equal a b) (union-equal b a)))
 
220
 
 
221
(defthm union-equal-associative
 
222
  (equal (union-equal (union-equal a b) c)
 
223
         (union-equal a (union-equal b c))))
 
224
 
 
225
(defthm union-equal-assoc-commute-subset
 
226
  (subsetp-equal (union-equal a (union-equal b c))
 
227
                 (union-equal b (union-equal a c))))
 
228
 
 
229
(defthm union-equal-assoc-commute
 
230
  (set-equal (union-equal a (union-equal b c))
 
231
             (union-equal b (union-equal a c))))
 
232
 
 
233
(defthm union-equal-idempotent-general
 
234
  (equal (union-equal x (union-equal x y))
 
235
         (union-equal x y))
 
236
  :hints (("Goal"
 
237
           :do-not-induct t
 
238
           :use ((:instance union-equal-associative
 
239
                            (a x) (b x) (c y))))))
 
240
 
 
241
;;-----------------  append and subsetp-equal
 
242
 
 
243
(defthm subset-append-1
 
244
  (implies (not (subsetp-equal a b))
 
245
           (not (subsetp-equal (append a c) b))))
 
246
 
 
247
(defthm subset-append-2
 
248
  (implies (not (subsetp-equal a b))
 
249
           (not (subsetp-equal (append c a) b))))
 
250
 
 
251
(defthm member-append-cons  
 
252
  (member-equal x (append a (cons x b))))
 
253
 
 
254
(defthm subset-append-cons
 
255
  (subsetp-equal (append b c) (append b (cons x c))))
 
256
 
 
257
(defthm subset-append-cons-2
 
258
  (implies (subsetp-equal a (append b c))
 
259
           (subsetp-equal a (append b (cons x c))))
 
260
  :hints (("Goal"
 
261
           :use ((:instance subsetp-equal-transitive
 
262
                            (x a) (y (append b c))
 
263
                            (z (append b (cons x c))))))))
 
264
 
 
265
(defthm subset-append-cons-3
 
266
  (implies (subsetp-equal (append a b) c)
 
267
           (subsetp-equal (append a (cons x b)) (cons x c))))
 
268
 
 
269
;;--------------------------
 
270
;; The setp predicate checks that a list has no duplicates.
 
271
 
 
272
(defun setp (a)
 
273
  (declare (xargs :guard (true-listp a)))
 
274
  (cond ((atom a) t)
 
275
        ((member-equal (car a) (cdr a)) nil)
 
276
        (t (setp (cdr a)))))
 
277
 
 
278
(defthm union-equal-setp
 
279
  (implies (and (setp a)
 
280
                (setp b))
 
281
           (setp (union-equal a b))))
 
282
 
 
283
(defthm remove-equal-setp
 
284
  (implies (setp a)
 
285
           (setp (remove-equal x a))))
 
286
 
 
287
(defthm setp-append-1
 
288
  (implies (not (setp b))
 
289
           (not (setp (append a b)))))
 
290
 
 
291
(defthm setp-append-2
 
292
  (implies (not (setp a))
 
293
           (not (setp (append a b))))
 
294
  :hints (("Goal"
 
295
           :do-not generalize)))
 
296
 
 
297
;;--------------------------------
 
298
;; set-difference-equal
 
299
 
 
300
(defthm not-member-set-difference
 
301
  (implies (not (member-equal x c))
 
302
           (not (member-equal x (set-difference-equal c d)))))
 
303
 
 
304
(defthm set-difference-equal-nil
 
305
  (implies (true-listp a)
 
306
           (equal (set-difference-equal a nil) a)))
 
307
 
 
308
 
 
309
;;--------------------------------
 
310
;; misc
 
311
 
 
312
(defthm consp-has-member-equal
 
313
  (implies (consp x)
 
314
           (member-equal (car x) x))
 
315
  :rule-classes nil)
 
316
 
 
317
;;--------------------------------
 
318
;; This section is a bunch of special-purpose lemmas about subset and union.
 
319
 
 
320
(defthm subset-union-6
 
321
  (subsetp-equal a (union-equal c (union-equal a d))))
 
322
 
 
323
(defthm special-set-lemma-2
 
324
  (implies (subsetp-equal b (union-equal c (union-equal a d)))
 
325
           (subsetp-equal (union-equal a b)
 
326
                          (union-equal c (union-equal a d)))))
 
327
 
 
328
(defthm subset-union-7
 
329
  (subsetp-equal a (union-equal c (cons x (union-equal a d)))))
 
330
 
 
331
(defthm special-set-lemma-3
 
332
  (implies (subsetp-equal b (union-equal c (cons x (union-equal a d))))
 
333
           (subsetp-equal (union-equal a b)
 
334
                          (union-equal c (cons x (union-equal a d))))))
 
335
 
 
336
(defthm subset-union-8
 
337
  (implies (subsetp-equal a (union-equal b m))
 
338
           (subsetp-equal a (union-equal b (union-equal d m)))))
 
339
 
 
340
(defthm subset-union-9
 
341
  (implies (subsetp-equal c (union-equal d m))
 
342
           (subsetp-equal c (union-equal b (union-equal d m)))))
 
343
 
 
344
(defthm special-set-lemma-4
 
345
  (implies (and (subsetp-equal a (union-equal b m))
 
346
                (subsetp-equal c (union-equal d m)))
 
347
           (subsetp-equal (union-equal a c)
 
348
                          (union-equal b (union-equal d m)))))
 
349
 
 
350
(defthm special-set-lemma-6
 
351
  (implies (and (subsetp-equal fs (union-equal fl ft))
 
352
                (subsetp-equal fl s)
 
353
                (subsetp-equal ft s))
 
354
           (subsetp-equal fs s))
 
355
  :rule-classes nil)
 
356
 
 
357
;;-----------------
 
358
;; Disjoint lists.
 
359
           
 
360
(defun disjoint (a b)
 
361
  (declare (xargs :guard (and (true-listp a) (true-listp b))))
 
362
  (cond ((atom a) t)
 
363
        ((member-equal (car a) b) nil)
 
364
        (t (disjoint (cdr a) b))))
 
365
 
 
366
(defthm disjoint-nil-right
 
367
  (disjoint a nil))
 
368
 
 
369
(defthm disjoint-append-union-1
 
370
  (implies (not (disjoint a b))
 
371
           (not (disjoint (append d a) (union-equal c b)))))
 
372
 
 
373
(defthm disjoint-append-union-2
 
374
  (implies (not (disjoint a b))
 
375
           (not (disjoint (append a d) (union-equal b c)))))
 
376
 
 
377
(defthm disjoint-member-remove
 
378
  (implies (and (not (disjoint a b))
 
379
                (not (member-equal x a)))
 
380
           (not (disjoint a (remove-equal x b)))))
 
381
 
 
382
(defthm disjoint-append-union-3
 
383
  (implies (not (disjoint a b))
 
384
           (not (disjoint (append a d) (union-equal c b)))))
 
385
 
 
386
(defthm disjoint-append-union-4
 
387
  (implies (not (disjoint a b))
 
388
           (not (disjoint (append d a) (union-equal b c)))))
 
389
 
 
390
(defthm disjoint-append-1
 
391
  (implies (not (disjoint a b))
 
392
           (not (disjoint (append a c) b))))
 
393
 
 
394
(defthm disjoint-append-2
 
395
  (implies (not (disjoint a b))
 
396
           (not (disjoint (append c a) b))))
 
397
 
 
398
(defthm disjoint-append-3
 
399
  (implies (not (disjoint a b))
 
400
           (not (disjoint a (append b c)))))
 
401
 
 
402
(defthm disjoint-append-4
 
403
  (implies (not (disjoint a b))
 
404
           (not (disjoint a (append c b)))))
 
405
 
 
406
(defthm disjoint-union-1
 
407
  (implies (not (disjoint a b))
 
408
           (not (disjoint a (union-equal b c)))))
 
409
 
 
410
(defthm disjoint-union-2
 
411
  (implies (not (disjoint a b))
 
412
           (not (disjoint a (union-equal c b)))))
 
413
 
 
414
;;------------------
 
415
 
 
416
(defun disjoint-skolem (a b)  ;; first member of a in b
 
417
  (declare (xargs :guard (and (true-listp a) (true-listp b))))
 
418
  (cond ((atom a) nil)
 
419
        ((member-equal (car a) b) (car a))
 
420
        (t (disjoint-skolem (cdr a) b))))
 
421
 
 
422
(defthm disjoint-skolem-lemma
 
423
  (implies (implies (member-equal (disjoint-skolem a b) a)
 
424
                    (not (member-equal (disjoint-skolem a b) b)))
 
425
           (disjoint a b))
 
426
  :rule-classes nil)
 
427