← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2004/sumners-ray/support/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/2004/sumners-ray/support/sets.lisp
 
1
;; sets.lisp
 
2
 
 
3
(in-package "ACL2")
 
4
 
 
5
(set-match-free-default :all)
 
6
 
 
7
#|
 
8
 
 
9
We define the common boolean operations (and a few other common useful notions)
 
10
on sets canonicalized as ordered lists using Pete's total ordering of all ACL2
 
11
objects. Further, the functions have been defined with a normalization of all
 
12
ACL2 objects as appropriate sets (we define a 1-1 function which maps any ACL2
 
13
object to a corresponding well-formed set) and using this normal (and its
 
14
inverse), we can prove properties about normalized set operations which use
 
15
equal-ity instead of set-equality and require no backtracking to relieve
 
16
well-formed set hypotheses.
 
17
 
 
18
EXPORTED logic functions:
 
19
   
 
20
   (in e x)      -- set membership predicate, is element e a member of set x
 
21
   (subset x y)  -- subset predicate, is set x a subset of set y
 
22
   (isect x y)   -- the set intersection of set x and set y
 
23
   (unite x y)   -- the set union of set x and set y
 
24
   (sdiff x y)   -- the set of elements in set x but not in set y
 
25
   (card x)      -- returns the number of objects in the set x
 
26
   (s1 e)        -- the singleton set consisting only of the element e
 
27
   (scar x)      -- the least (by <<) element in the set x, nil if x is empty
 
28
   ()            -- NIL is unique representative value for empty set,
 
29
                    so use NULL or NOT to test a set for emptiness
 
30
   (c1 x)        -- test which returns true if x is a singleton set
 
31
 
 
32
EXPORTED theorems provided at the end of this file.
 
33
 
 
34
I have removed all of the subgoal hints except for those introduced by the
 
35
macro defthm-ternary-sets. These subgoal hints are reasonable since they are
 
36
introduced in the context of a provided induction scheme and they help speed
 
37
the proofs through considerably by avoiding the problem in ACL2 of
 
38
free-variable matching in the application of <<-transitive.
 
39
 
 
40
|#
 
41
 
 
42
(include-book "total-order")
 
43
 
 
44
;; i needed to add the following forward-chaining rule to make better use
 
45
;; of <<-trichotomy from the included order book.
 
46
 
 
47
(local
 
48
(defthm <<-trichotomy-forward-chain1
 
49
  (implies (and (not (<< x y))
 
50
                (not (equal x y)))
 
51
           (<< y x))
 
52
  :rule-classes :forward-chaining))
 
53
 
 
54
(defun setp (x)
 
55
  (or (null x)
 
56
      (and (consp x)
 
57
           (setp (rest x))
 
58
           (or (null (rest x))
 
59
               (<< (first x) (second x))))))
 
60
 
 
61
(defun ifsp (x) ;; ill-formed setp
 
62
  (or (not (setp x))
 
63
      (and (consp x)
 
64
           (null (cdr x))
 
65
           (ifsp (car x)))))
 
66
 
 
67
(defun norm->set (x)
 
68
  (if (ifsp x) (list x) x))
 
69
 
 
70
(defun set->norm (x)
 
71
  (if (ifsp x) (first x) x))
 
72
 
 
73
(defun in-aux (e x)
 
74
  (and (not (endp x))
 
75
       (or (equal e (first x))
 
76
           (and (<< (first x) e)
 
77
                (in-aux e (rest x))))))
 
78
 
 
79
(defun in (e x)
 
80
  (in-aux e (norm->set x)))
 
81
 
 
82
(defun subset-aux (x y)
 
83
  (or (endp x)
 
84
      (and (not (endp y))
 
85
           (cond ((equal (first x) (first y))
 
86
                  (subset-aux (rest x) (rest y)))
 
87
                 ((<< (first y) (first x))
 
88
                  (subset-aux x (rest y)))
 
89
                 (t nil)))))
 
90
 
 
91
(defun subset (x y)
 
92
  (subset-aux (norm->set x) (norm->set y)))
 
93
 
 
94
(defun isect-aux (x y)
 
95
  (declare (xargs :measure (+ (acl2-count x)
 
96
                              (acl2-count y))))
 
97
  (cond ((endp x) ())
 
98
        ((endp y) ())
 
99
        ((equal (first x) (first y))
 
100
         (cons (first x)
 
101
               (isect-aux (rest x) (rest y))))
 
102
        ((<< (first x) (first y))
 
103
         (isect-aux (rest x) y))
 
104
        (t
 
105
         (isect-aux x (rest y)))))
 
106
 
 
107
(defun isect (x y)
 
108
  (set->norm (isect-aux (norm->set x) (norm->set y))))
 
109
 
 
110
(defun unite-aux (x y)
 
111
  (declare (xargs :measure (+ (acl2-count x)
 
112
                              (acl2-count y))))
 
113
  (cond ((endp x) y)
 
114
        ((endp y) x)
 
115
        ((equal (first x) (first y))
 
116
         (cons (first x)
 
117
               (unite-aux (rest x) (rest y))))
 
118
        ((<< (first x) (first y))
 
119
         (cons (first x)
 
120
               (unite-aux (rest x) y)))
 
121
        (t
 
122
         (cons (first y)
 
123
               (unite-aux x (rest y))))))
 
124
 
 
125
(defun unite (x y)
 
126
  (set->norm (unite-aux (norm->set x) (norm->set y))))
 
127
 
 
128
(defun sdiff-aux (x y)
 
129
  (declare (xargs :measure (+ (acl2-count x)
 
130
                              (acl2-count y))))
 
131
  (cond ((endp x) ())
 
132
        ((endp y) x)
 
133
        ((equal (first x) (first y))
 
134
         (sdiff-aux (rest x) (rest y)))
 
135
        ((<< (first x) (first y))
 
136
         (cons (first x)
 
137
               (sdiff-aux (rest x) y)))
 
138
        (t
 
139
         (sdiff-aux x (rest y)))))
 
140
 
 
141
(defun sdiff (x y)
 
142
  (set->norm (sdiff-aux (norm->set x) (norm->set y))))
 
143
 
 
144
(defun s1 (e)
 
145
  (set->norm (list e)))
 
146
 
 
147
(defun card (x)
 
148
  (len (norm->set x)))
 
149
 
 
150
(defun scar (x)
 
151
  (if (ifsp x) x (first x)))
 
152
 
 
153
(defmacro empty-set ()
 
154
  `())
 
155
 
 
156
(defun c1 (x)
 
157
  (let ((x (norm->set x))) (and (consp x) (not (cdr x)))))
 
158
 
 
159
 
 
160
 
 
161
;;; some useful auxiliary macros which could be removed if
 
162
;;; needed (e.g. if the names conflict with existing fns)
 
163
 
 
164
(defmacro sadd (e x)
 
165
  `(unite (s1 ,e) ,x))
 
166
 
 
167
(defmacro sdrop (e x)
 
168
  `(sdiff ,x (s1 ,e)))
 
169
 
 
170
(defmacro scdr (x)
 
171
  `(sdrop (scar ,x) ,x))
 
172
 
 
173
(defmacro satom (x) 
 
174
  `(not ,x))
 
175
 
 
176
(defmacro common (x y)
 
177
  `(not (satom (isect ,x ,y))))
 
178
 
 
179
 
 
180
;;;; properties of setp ;;;;
 
181
 
 
182
(local
 
183
(defthm setp-implies-true-listp
 
184
  (implies (setp x)
 
185
           (true-listp x))
 
186
  :rule-classes (:forward-chaining
 
187
                 :rewrite)))
 
188
 
 
189
 
 
190
;;;; properties of norm->set and set->norm ;;;;
 
191
 
 
192
(local
 
193
(defthm norm->set-set->norm-of-setp
 
194
  (implies (setp x)
 
195
           (equal (norm->set (set->norm x))
 
196
                  x))))
 
197
 
 
198
(local
 
199
(defthm norm->set-of-wf-setp
 
200
  (implies (not (ifsp x))
 
201
           (equal (norm->set x) x))))
 
202
 
 
203
(local
 
204
(defthm norm->set-of-if-setp
 
205
  (implies (ifsp x)
 
206
           (equal (norm->set x) (list x)))))
 
207
 
 
208
(local
 
209
(defthm norm->set-returns-setp
 
210
  (setp (norm->set x))))
 
211
 
 
212
(local
 
213
(defthm norm->set-preserves-equality
 
214
  (iff (equal (norm->set x) (norm->set y))
 
215
       (equal x y))))
 
216
 
 
217
(local
 
218
(defthm set->norm-norm->set-inverse
 
219
  (equal (set->norm (norm->set x)) x)))
 
220
 
 
221
(local
 
222
(defthm set->norm-nil-iff-passed-nil
 
223
  (implies (setp x)
 
224
           (iff (set->norm x) x))))
 
225
 
 
226
(local
 
227
(defthm norm->set-of-x-is-consp-or-not-x
 
228
  (iff (consp (norm->set x)) x)
 
229
  :rule-classes nil))
 
230
 
 
231
(local
 
232
(defthm norm->set-is-true-listp
 
233
  (true-listp (norm->set x))
 
234
  :rule-classes :type-prescription))
 
235
 
 
236
(in-theory (disable set->norm norm->set))
 
237
 
 
238
 
 
239
;;;; bounded properties ;;;;
 
240
 
 
241
(local
 
242
(defthm unite-aux-bounded-<<
 
243
  (implies (and (<< a (first x))
 
244
                (<< a (first y)))
 
245
           (<< a (first (unite-aux x y))))))
 
246
 
 
247
(local
 
248
(defthm isect-aux-bounded-<<
 
249
  (implies (and (or (<< a (first x))
 
250
                    (<< a (first y)))
 
251
                (isect-aux x y))
 
252
           (<< a (first (isect-aux x y))))))
 
253
 
 
254
(local
 
255
(defthm sdiff-aux-bounded-<<
 
256
  (implies (and (setp x)
 
257
                (<< a (first x))
 
258
                (sdiff-aux x y))
 
259
           (<< a (first (sdiff-aux x y))))))
 
260
 
 
261
 
 
262
;;;; type-correctness properties ;;;;
 
263
 
 
264
(local
 
265
(defthm unite-aux-preserves-setp
 
266
  (implies (and (setp x) (setp y))
 
267
           (setp (unite-aux x y)))
 
268
  :rule-classes ((:forward-chaining
 
269
                  :trigger-terms ((unite-aux x y)))
 
270
                 :rewrite)))
 
271
 
 
272
(local
 
273
(defthm isect-aux-preserves-setp
 
274
  (implies (and (setp x) (setp y))
 
275
           (setp (isect-aux x y)))
 
276
  :rule-classes ((:forward-chaining
 
277
                  :trigger-terms ((isect-aux x y)))
 
278
                 :rewrite)))
 
279
 
 
280
(local
 
281
(defthm sdiff-aux-preserves-setp
 
282
  (implies (setp x)
 
283
           (setp (sdiff-aux x y)))
 
284
  :rule-classes ((:forward-chaining
 
285
                  :trigger-terms ((sdiff-aux x y)))
 
286
                 :rewrite)))
 
287
 
 
288
 
 
289
;;;; properties of membership-aux ;;;;
 
290
 
 
291
(local
 
292
(defthm in-aux-isect-aux-reduce
 
293
  (equal (in-aux e (isect-aux x y))
 
294
         (and (in-aux e x) (in-aux e y)))))
 
295
 
 
296
(local
 
297
(defthm in-aux-unite-aux-reduce
 
298
  (equal (in-aux e (unite-aux x y))
 
299
         (or (in-aux e x) (in-aux e y)))))
 
300
 
 
301
(local
 
302
(defthm in-aux-implies-bounded
 
303
  (implies (and (setp x)
 
304
                (<< a (first x)))
 
305
           (not (in-aux a x)))))
 
306
 
 
307
(local
 
308
(defthm in-aux-sdiff-aux-reduce
 
309
  (implies (setp x)
 
310
           (equal (in-aux e (sdiff-aux x y))
 
311
                  (and (in-aux e x) (not (in-aux e y)))))))
 
312
 
 
313
(local
 
314
(defthm in-aux-subset-aux-transits
 
315
  (implies (and (in-aux e x)
 
316
                (subset-aux x y))
 
317
           (in-aux e y))))
 
318
 
 
319
 
 
320
;;;; ternary variable induction scheme and strategy ;;;;
 
321
 
 
322
;; the following function defines an induction scheme used in theorems
 
323
;; involving three free variables (like associativity proofs).
 
324
 
 
325
(local
 
326
(defun ternary-induct (x y z)
 
327
  (declare (xargs :measure (+ (acl2-count x)
 
328
                              (acl2-count y)
 
329
                              (acl2-count z))))
 
330
  (if (or (endp x) 
 
331
          (endp y) 
 
332
          (endp z))
 
333
 ; The following was changed to avoid SBCL warning, "Asserted type NUMBER
 
334
 ; conflicts with derived type (VALUES LIST &OPTIONAL)."
 
335
      (list x y z)
 
336
    (cond ((<< (first x) (first y))
 
337
           (cond ((<< (first x) (first z))
 
338
                  (ternary-induct (rest x) y z))
 
339
                 ((equal (first x) (first z))
 
340
                  (ternary-induct (rest x) y (rest z)))
 
341
                 ((and (<< (first z) (first x))
 
342
                       (<< (first z) (first y)))
 
343
                  (ternary-induct x y (rest z)))))
 
344
          ((equal (first x) (first y))
 
345
           (cond ((<< (first x) (first z))
 
346
                  (ternary-induct (rest x) (rest y) z))
 
347
                 ((equal (first x) (first z))
 
348
                  (ternary-induct (rest x) (rest y) (rest z)))
 
349
                 ((<< (first z) (first x))
 
350
                  (ternary-induct x y (rest z)))))
 
351
          ((<< (first y) (first x))
 
352
           (cond ((<< (first y) (first z))
 
353
                  (ternary-induct x (rest y) z))
 
354
                 ((equal (first y) (first z))
 
355
                  (ternary-induct x (rest y) (rest z)))
 
356
                 ((and (<< (first z) (first y))
 
357
                       (<< (first z) (first x)))
 
358
                  (ternary-induct x y (rest z)))))))))
 
359
 
 
360
;; the following macro defines an effective strategy for inducting based on the
 
361
;; scheme ternary-induct.
 
362
 
 
363
(defmacro defthm-ternary-sets (name body)
 
364
  `(defthm ,name ,body
 
365
     :hints (("Goal" 
 
366
              :induct (ternary-induct x y z)
 
367
              :in-theory (disable <<-transitive))
 
368
             ("Subgoal *1/13"
 
369
              :in-theory (enable <<-transitive))
 
370
             ("Subgoal *1/5"
 
371
              :in-theory (enable <<-transitive)))))
 
372
 
 
373
 
 
374
;;;; properties of subset-aux ;;;;
 
375
 
 
376
(local
 
377
(defthm unite-aux-x<y-expansion
 
378
  (implies (and (consp x)
 
379
                (consp y)
 
380
                (<< (car x) (car y)))
 
381
           (equal (unite-aux x y)
 
382
                  (cons (car x)
 
383
                        (unite-aux (cdr x) y))))))
 
384
 
 
385
(local
 
386
(defthm subset-aux-x<y-reduces-nil
 
387
  (implies (and (consp x)
 
388
                (consp y)
 
389
                (<< (car x) (car y)))
 
390
           (equal (subset-aux x y)
 
391
                  nil))))
 
392
 
 
393
(local
 
394
(defthm atom-unite-aux-implies-atom-params
 
395
  (implies (not (consp (unite-aux x y)))
 
396
           (and (not (consp x))
 
397
                (not (consp y))))))
 
398
 
 
399
(local
 
400
(defthm-ternary-sets subset-aux-unite-aux-reduction
 
401
  (equal (subset-aux (unite-aux x y) z)
 
402
         (and (subset-aux x z)
 
403
              (subset-aux y z)))))
 
404
 
 
405
(local
 
406
(in-theory (disable unite-aux-x<y-expansion)))
 
407
 
 
408
(local
 
409
(defthm subset-aux-is-reflexive
 
410
  (subset-aux x x)))
 
411
 
 
412
(local
 
413
(defthm subset-aux-unite-aux-property
 
414
  (implies (setp x)
 
415
           (subset-aux x (unite-aux x y)))))
 
416
 
 
417
(local
 
418
(defthm <<-irreflexive-rewrite
 
419
  (implies (<< x y)
 
420
           (not (equal x y)))))
 
421
 
 
422
(local
 
423
(defthm-ternary-sets subset-aux-isect-aux-reduction
 
424
  (equal (subset-aux x (isect-aux y z))
 
425
         (and (subset-aux x y)
 
426
              (subset-aux x z)))))
 
427
 
 
428
(local
 
429
(defthm subset-aux-isect-aux-property
 
430
  (implies (setp x)
 
431
           (subset-aux (isect-aux x y) x))))
 
432
 
 
433
(local
 
434
(defthm subset-aux-sdiff-aux-property
 
435
  (implies (setp x)
 
436
           (subset-aux (sdiff-aux x y) x))))
 
437
 
 
438
(local
 
439
(defthm-ternary-sets subset-aux-is-transitive
 
440
  (implies (and (subset-aux x y)
 
441
                (subset-aux y z))
 
442
           (subset-aux x z))))
 
443
 
 
444
(local
 
445
(defthm subset-aux-is-total-on-sets
 
446
  (implies (and (setp x) (setp y)
 
447
                (subset-aux x y))
 
448
           (equal (subset-aux y x)
 
449
                  (equal x y)))))
 
450
 
 
451
(local
 
452
(defthm subset-length-property
 
453
  (implies (and (setp x)
 
454
                (setp y)
 
455
                (subset-aux x y))
 
456
           (<= (len x) (len y)))))
 
457
 
 
458
(local
 
459
(defthm len<-reduce-when-subset
 
460
  (implies (and (setp x)
 
461
                (setp y)
 
462
                (subset-aux x y))
 
463
           (equal (< (len x) (len y))
 
464
                  (not (equal x y))))))
 
465
 
 
466
 
 
467
;;;; properties of unite-aux ;;;;
 
468
 
 
469
(local
 
470
(defthm unite-aux-implied-by-and
 
471
  (implies (and (setp x)
 
472
                (setp y)
 
473
                x y)
 
474
           (unite-aux x y))))
 
475
 
 
476
(local
 
477
(defthm unite-aux-reflexes
 
478
  (implies (setp x)
 
479
           (equal (unite-aux x x) x))))
 
480
 
 
481
(local
 
482
(defthm unite-aux-commutes
 
483
  (implies (and (setp x) (setp y))
 
484
           (equal (unite-aux x y) 
 
485
                  (unite-aux y x)))))
 
486
 
 
487
(local
 
488
(defthm unite-aux-x<y-expansion-flip
 
489
  (implies (and (consp x)
 
490
                (consp y)
 
491
                (<< (car x) (car y)))
 
492
           (equal (unite-aux y x)
 
493
                  (cons (car x)
 
494
                        (unite-aux y (cdr x)))))))
 
495
 
 
496
(local
 
497
(in-theory (enable unite-aux-x<y-expansion)))
 
498
 
 
499
(local
 
500
(defthm-ternary-sets unite-aux-associates
 
501
  (implies (and (setp x) (setp y) (setp z))
 
502
           (equal (unite-aux (unite-aux x y) z)
 
503
                  (unite-aux x (unite-aux y z))))))
 
504
 
 
505
(local
 
506
(in-theory (disable unite-aux-x<y-expansion-flip
 
507
                    unite-aux-x<y-expansion)))
 
508
 
 
509
(local
 
510
(defthm unite-aux-subset-aux-property
 
511
  (equal (equal (unite-aux x y) y)
 
512
         (subset-aux x y))))
 
513
 
 
514
(local
 
515
(defthm length-of-unite-aux-property
 
516
  (implies (and (setp x) (setp y))
 
517
           (equal (len (unite-aux x y))
 
518
                  (+ (len x)
 
519
                     (len (sdiff-aux y x)))))))
 
520
 
 
521
(local
 
522
(defthm set-norm-equality-transfer
 
523
  (implies (setp x)
 
524
           (equal (equal (set->norm x) y)
 
525
                  (equal x (norm->set y))))))
 
526
 
 
527
 
 
528
;;;; properties of isect-aux ;;;;
 
529
 
 
530
(local
 
531
(defthm isect-aux-reflexes
 
532
  (implies (setp x)
 
533
           (equal (isect-aux x x) x))))
 
534
 
 
535
(local
 
536
(defthm isect-aux-commutes
 
537
  (implies (and (setp x) (setp y))
 
538
           (equal (isect-aux x y) (isect-aux y x)))))
 
539
 
 
540
(local
 
541
(defthm isect-aux-x<y-expansion
 
542
  (implies (and (consp x)
 
543
                (consp y)
 
544
                (<< (car x) (car y)))
 
545
           (equal (isect-aux y x)
 
546
                  (isect-aux y (cdr x))))))
 
547
 
 
548
(local
 
549
(defthm-ternary-sets isect-aux-associates
 
550
  (implies (and (setp x) (setp y) (setp z))
 
551
           (equal (isect-aux (isect-aux x y) z)
 
552
                  (isect-aux x (isect-aux y z))))))
 
553
 
 
554
(local
 
555
(in-theory (disable isect-aux-commutes
 
556
                    unite-aux-commutes)))
 
557
 
 
558
(local
 
559
(defthm isect-aux-bounded-then-not-equal
 
560
  (implies (and (consp z)
 
561
                (or (<< (car z) (car x))
 
562
                    (<< (car z) (car y))))
 
563
           (not (equal (isect-aux x y) z)))))
 
564
 
 
565
(local
 
566
(defthm isect-aux-subset-aux-property
 
567
  (implies (and (setp x) (setp y))
 
568
           (equal (equal (isect-aux x y) x)
 
569
                  (subset-aux x y)))))
 
570
 
 
571
(local
 
572
(defthm <<-irreflexive-rewrite-flip
 
573
  (implies (<< x y)
 
574
           (not (equal y x)))))
 
575
 
 
576
(local
 
577
(defthm-ternary-sets isect-aux-unite-aux-distributes
 
578
  (implies (and (setp x) (setp y) (setp z))
 
579
           (equal (isect-aux (unite-aux x y) z)
 
580
                  (unite-aux (isect-aux x z)
 
581
                             (isect-aux y z))))))
 
582
 
 
583
(local
 
584
(defthm-ternary-sets isect-aux-sdiff-aux-distributes
 
585
  (implies (and (setp x) (setp y) (setp z))
 
586
           (equal (isect-aux (sdiff-aux x y) z)
 
587
                  (sdiff-aux (isect-aux x z) y)))))
 
588
 
 
589
 
 
590
;;;; properties of sdiff-aux ;;;;
 
591
 
 
592
(local
 
593
(defthm sdiff-aux-subset-aux-property
 
594
  (implies (and (setp x) (setp y))
 
595
           (iff (sdiff-aux x y)
 
596
                (not (subset-aux x y))))))
 
597
 
 
598
(local
 
599
(defthm length-of-sdiff-aux-property
 
600
  (implies (and (setp x) (setp y))
 
601
           (equal (len (sdiff-aux x y))
 
602
                  (- (len x) 
 
603
                     (len (isect-aux x y)))))))
 
604
 
 
605
(local
 
606
(defthm-ternary-sets sdiff-aux-unite-aux-distributes
 
607
  (implies (and (setp x) (setp y) (setp z))
 
608
           (equal (sdiff-aux (unite-aux x y) z)
 
609
                  (unite-aux (sdiff-aux x z)
 
610
                             (sdiff-aux y z))))))
 
611
 
 
612
(local
 
613
(defthm-ternary-sets sdiff-aux-unite-aux-reduction
 
614
  (implies (and (setp x) (setp y) (setp z))
 
615
           (equal (sdiff-aux x (unite-aux y z))
 
616
                  (sdiff-aux (sdiff-aux x y) z)))))
 
617
 
 
618
(local
 
619
(defthm sdiff-aux-reduce-no-isect-aux
 
620
  (implies (and (setp x) (setp y) (not (isect-aux x y)))
 
621
           (equal (sdiff-aux x y) x))))
 
622
 
 
623
 
 
624
;;;; properties of s1-aux -- i.e. list ;;;;
 
625
 
 
626
(local
 
627
(defthm subset-aux-reduces-to-membership
 
628
  (implies (setp x)
 
629
           (equal (subset-aux (list e) x)
 
630
                  (in-aux e x)))))
 
631
 
 
632
(local
 
633
(defthm subset-aux-of-singleton
 
634
  (implies (and (setp x) x
 
635
                (subset-aux x (list e)))
 
636
           (equal (equal x (list e)) t))))
 
637
 
 
638
(local
 
639
(defthm isect-aux-of-singleton
 
640
  (implies (setp x)
 
641
           (equal (isect-aux (list e) x)
 
642
                  (if (in-aux e x) (list e) ())))))
 
643
 
 
644
(local
 
645
(defthm sdiff-aux-of-singleton
 
646
  (implies (setp x)
 
647
           (equal (sdiff-aux (list e) x)
 
648
                  (if (in-aux e x) () (list e))))))
 
649
 
 
650
 
 
651
;;;; EXPORTED THEOREMS ;;;;
 
652
;; Note, the order of the these theorems below is relevant for the
 
653
;; order in which ACL2 applies them (later ones first). This is why
 
654
;; the associativity and commutativity theorems are first since
 
655
;; restructuring unite and isect can have the detrimental effect of
 
656
;; disabling the application of other rules.
 
657
 
 
658
(local
 
659
(in-theory (enable unite-aux-commutes
 
660
                   isect-aux-commutes)))
 
661
 
 
662
 
 
663
;;;; EXPORTED associative and commutative properties ;;;;
 
664
 
 
665
(defthm unite-implied-by-and
 
666
  (implies (and x y)
 
667
           (unite x y)))
 
668
 
 
669
(defthm unite-reflexes
 
670
  (equal (unite x x) x))
 
671
 
 
672
(defthm unite-commutes
 
673
  (equal (unite x y) 
 
674
         (unite y x)))
 
675
 
 
676
(defthm unite-associates
 
677
  (equal (unite (unite x y) z)
 
678
         (unite x (unite y z))))
 
679
 
 
680
(defthm unite-associate-2
 
681
  (equal (unite x (unite y z))
 
682
         (unite y (unite x z)))
 
683
  :hints (("Goal" 
 
684
           :in-theory (disable unite-commutes)
 
685
           :use ((:instance unite-commutes
 
686
                            (x x) (y (unite y z)))
 
687
                 (:instance unite-commutes
 
688
                            (x x) (y z))))))
 
689
 
 
690
(defthm isect-reflexes
 
691
  (equal (isect x x) x))
 
692
 
 
693
(defthm isect-commutes
 
694
  (equal (isect x y) 
 
695
         (isect y x)))
 
696
 
 
697
(defthm isect-associates
 
698
  (equal (isect (isect x y) z)
 
699
         (isect x (isect y z))))
 
700
 
 
701
(defthm isect-associate-2
 
702
  (equal (isect x (isect y z))
 
703
         (isect y (isect x z)))
 
704
  :hints (("Goal" 
 
705
           :in-theory (disable isect-commutes)
 
706
           :use ((:instance isect-commutes
 
707
                            (x x) (y (isect y z)))
 
708
                 (:instance isect-commutes
 
709
                            (x x) (y z))))))
 
710
 
 
711
;;;; EXPORTED properties of membership ;;;;
 
712
 
 
713
(defthm in-isect-reduce
 
714
  (equal (in e (isect x y))
 
715
         (and (in e x) (in e y))))
 
716
 
 
717
(defthm in-unite-reduce
 
718
  (equal (in e (unite x y))
 
719
         (or (in e x) (in e y))))
 
720
 
 
721
(defthm in-sdiff-reduce
 
722
  (equal (in e (sdiff x y))
 
723
         (and (in e x) (not (in e y)))))
 
724
 
 
725
(defthm in-subset-transits
 
726
  (implies (and (in e x)
 
727
                (subset x y))
 
728
           (in e y)))
 
729
 
 
730
 
 
731
;;;; EXPORTED properties of susbet ;;;;
 
732
 
 
733
(defthm subset-unite-reduction
 
734
  (equal (subset (unite x y) z)
 
735
         (and (subset x z)
 
736
              (subset y z))))
 
737
 
 
738
(defthm subset-unite-property
 
739
  (subset x (unite x y)))
 
740
 
 
741
(defthm subset-isect-reduction
 
742
  (equal (subset x (isect y z))
 
743
         (and (subset x y)
 
744
              (subset x z))))
 
745
 
 
746
(defthm subset-isect-property
 
747
  (subset (isect x y) x))
 
748
 
 
749
(defthm subset-sdiff-property
 
750
  (subset (sdiff x y) x))
 
751
 
 
752
(defthm subset-is-reflexive
 
753
  (subset x x))
 
754
 
 
755
(defthm subset-is-transitive
 
756
  (implies (and (subset x y)
 
757
                (subset y z))
 
758
           (subset x z)))
 
759
 
 
760
(defthm subset-is-total-order
 
761
  (implies (subset x y)
 
762
           (equal (subset y x)
 
763
                  (equal x y))))
 
764
 
 
765
(defthm subset-card-property
 
766
  (implies (subset x y)
 
767
           (<= (card x) (card y))))
 
768
 
 
769
(defthm card<-reduce-when-subset
 
770
  (implies (subset x y)
 
771
           (equal (< (card x) (card y))
 
772
                  (not (equal x y)))))
 
773
 
 
774
 
 
775
;;;; EXPORTED reductions of unite ;;;;
 
776
 
 
777
(defthm unite-subset-property
 
778
  (equal (equal (unite x y) y)
 
779
         (subset x y)))
 
780
 
 
781
(defthm unite-subset-property-2
 
782
  (equal (equal (unite y x) y)
 
783
         (subset x y)))
 
784
 
 
785
(defthm unite-card-property
 
786
  (equal (card (unite x y))
 
787
         (+ (card x) 
 
788
            (card (sdiff y x)))))
 
789
 
 
790
 
 
791
;;;; EXPORTED reductions of isect ;;;;
 
792
 
 
793
(defthm isect-subset-property
 
794
  (equal (equal (isect x y) x)
 
795
         (subset x y)))
 
796
 
 
797
(defthm isect-unite-distributes-1
 
798
  (equal (isect (unite x y) z)
 
799
         (unite (isect x z)
 
800
                (isect y z))))
 
801
 
 
802
(defthm isect-unite-distributes-2
 
803
  (equal (isect z (unite x y))
 
804
         (unite (isect x z)
 
805
                (isect y z)))
 
806
  :hints (("Goal" :in-theory (disable isect-aux-commutes)
 
807
           :use (:instance isect-aux-commutes
 
808
                           (x (norm->set z))
 
809
                           (y (unite-aux (norm->set x)
 
810
                                         (norm->set y)))))))
 
811
 
 
812
(defthm isect-sdiff-distributes-1
 
813
  (equal (isect (sdiff x y) z)
 
814
         (sdiff (isect x z) y)))
 
815
 
 
816
(defthm isect-sdiff-distributes-2
 
817
  (equal (isect z (sdiff x y))
 
818
         (sdiff (isect x z) y))
 
819
  :hints (("Goal" :in-theory (disable isect-aux-commutes)
 
820
           :use (:instance isect-aux-commutes
 
821
                           (x (norm->set z))
 
822
                           (y (sdiff-aux (norm->set x)
 
823
                                         (norm->set y)))))))
 
824
 
 
825
 
 
826
;;;; EXPORTED reductions of sdiff ;;;;
 
827
 
 
828
(defthm sdiff-subset-property
 
829
  (iff (sdiff x y)
 
830
       (not (subset x y))))
 
831
 
 
832
(defthm sdiff-card-property
 
833
  (equal (card (sdiff x y))
 
834
         (- (card x)
 
835
            (card (isect x y)))))
 
836
 
 
837
(defthm sdiff-unite-distributes
 
838
  (equal (sdiff (unite x y) z)
 
839
         (unite (sdiff x z)
 
840
                (sdiff y z))))
 
841
 
 
842
(defthm sdiff-unite-reduction
 
843
  (equal (sdiff x (unite y z))
 
844
         (sdiff (sdiff x y) z)))
 
845
 
 
846
(defthm sdiff-reduce-no-isect
 
847
  (implies (not (isect x y))
 
848
           (equal (sdiff x y) x)))
 
849
 
 
850
 
 
851
;;;; EXPORTED reductions of s1 ;;;;
 
852
 
 
853
(defthm s1-membership-property
 
854
  (equal (in a (s1 b))
 
855
         (equal a b)))
 
856
 
 
857
(defthm s1-subset-property-1
 
858
  (equal (subset (s1 e) x)
 
859
         (in e x)))
 
860
 
 
861
(defthm s1-subset-property-2
 
862
  (implies (and (subset x (s1 e)) x)
 
863
           (equal x (s1 e)))
 
864
  :hints (("Goal" :use 
 
865
           (:instance norm->set-of-x-is-consp-or-not-x)))
 
866
  :rule-classes :forward-chaining)
 
867
 
 
868
(defthm s1-isect-property-1
 
869
  (equal (isect (s1 e) x)
 
870
         (if (in e x) (s1 e) ())))
 
871
 
 
872
(defthm s1-isect-property-2
 
873
  (equal (isect x (s1 e))
 
874
         (if (in e x) (s1 e) ()))
 
875
  :hints (("Goal" :in-theory (disable isect-aux-commutes)
 
876
           :use (:instance isect-aux-commutes
 
877
                           (x (norm->set x))
 
878
                           (y (list e))))))
 
879
 
 
880
(defthm s1-sdiff-property
 
881
  (equal (sdiff (s1 e) x)
 
882
         (if (in e x) () (s1 e))))
 
883
 
 
884
(defthm s1-card-property
 
885
  (equal (card (s1 e)) 1))
 
886
 
 
887
(defthm s1-iff-t (iff (s1 e) t))
 
888
 
 
889
(defthm s1-equal-nil
 
890
  (equal (equal (s1 e) nil) nil))
 
891
 
 
892
(defthm subset-s1-redux
 
893
  (equal (subset a (s1 e))
 
894
         (if a (equal a (s1 e)) t)))
 
895
 
 
896
 
 
897
 
 
898
;;;; EXPORTED properties of empty-set ;;;;
 
899
 
 
900
(defthm membership-empty-set
 
901
  (not (in e (empty-set))))
 
902
 
 
903
(defthm empty-set-is-subset
 
904
  (subset (empty-set) x))
 
905
 
 
906
(defthm empty-set-is-only-superset-self
 
907
  (equal (subset x (empty-set))
 
908
         (not x)))
 
909
 
 
910
(defthm unite-empty-set-property-1
 
911
  (equal (unite x (empty-set)) x))
 
912
 
 
913
(defthm unite-empty-set-property-2
 
914
  (equal (unite (empty-set) x) x))
 
915
 
 
916
(defthm isect-empty-set-property-1
 
917
  (equal (isect (empty-set) x) (empty-set)))
 
918
 
 
919
(defthm isect-empty-set-property-2
 
920
  (equal (isect x (empty-set)) (empty-set)))
 
921
 
 
922
(defthm sdiff-of-empty-set-1
 
923
  (equal (sdiff (empty-set) x) (empty-set)))
 
924
 
 
925
(defthm sdiff-of-empty-set-2
 
926
  (equal (sdiff x (empty-set)) x))
 
927
 
 
928
(defthm s1-is-not-empty-set
 
929
  (s1 e)
 
930
  :hints (("Goal" :in-theory (enable set->norm)))
 
931
  :rule-classes :type-prescription)
 
932
 
 
933
(defthm card-of-empty-set
 
934
  (iff (not x)
 
935
       (equal (card x) 0))
 
936
  :hints (("Goal" :in-theory (enable norm->set)))
 
937
  :rule-classes :type-prescription)
 
938
 
 
939
 
 
940
;;;; EXPORTED properties of scar ;;;;
 
941
 
 
942
(defthm scar-membership-property
 
943
  (iff (in (scar x) x) x))
 
944
 
 
945
(defthm scar-is-least-member
 
946
  (implies (and (in e x)
 
947
                (not (equal e (scar x))))
 
948
           (<< (scar x) e)))
 
949
 
 
950
(defthm scar-returns-nil-for-empty-set
 
951
  (equal (scar (empty-set)) nil))
 
952
 
 
953
(defthm scar-of-s1
 
954
  (equal (scar (s1 e)) e)
 
955
  :hints (("Goal" :in-theory (enable set->norm))))
 
956
 
 
957
(defthm scar-of-unite
 
958
  (implies (and x y)
 
959
           (equal (scar (unite x y))
 
960
                  (if (<< (scar x) (scar y)) (scar x) (scar y))))
 
961
  :hints (("Goal" :in-theory (enable norm->set set->norm))))
 
962
 
 
963
(defthm scar-of-sdiff
 
964
  (implies (<< (scar x) (scar y))
 
965
           (equal (scar (sdiff x y)) (scar x)))
 
966
  :hints (("Goal" :in-theory (enable norm->set set->norm))))
 
967
 
 
968
 
 
969
;;;; EXPORTED properties of c1 ;;;;
 
970
 
 
971
(defthm c1-of-s1
 
972
  (equal (c1 (s1 e)) t))
 
973
 
 
974
(defthm c1-of-nil
 
975
  (equal (c1 ()) nil))
 
976
 
 
977
(defthm c1-of-unite
 
978
  (equal (c1 (unite x y))
 
979
         (if (c1 x) (implies y (equal x y)) (and (not x) (c1 y))))
 
980
  :hints (("Goal" :in-theory (enable norm->set set->norm)
 
981
           :expand ((unite-aux (list x) y) (unite-aux x y)))))
 
982
           
 
983
(defthm isect-aux-sdiff-aux-prop1
 
984
  (implies (and (setp x) x
 
985
                (not (isect-aux x y)))
 
986
           (sdiff-aux x y)))
 
987
 
 
988
(defthm isect-aux-sdiff-aux-prop2
 
989
  (implies (and (consp x)
 
990
                (setp x)
 
991
                (not (isect-aux x y))
 
992
                (not (cdr (sdiff-aux x y))))
 
993
           (not (cdr x))))
 
994
 
 
995
(defthm c1-of-sdiff
 
996
  (implies (not (isect x y))
 
997
           (equal (c1 (sdiff x y)) (c1 x)))
 
998
  :hints (("Goal" :in-theory (enable norm->set set->norm)
 
999
           :expand ((:free (x) (sdiff-aux (list x) y))
 
1000
                    (:free (x z) (sdiff-aux (list x z) y))
 
1001
                    (:free (x a b) (sdiff-aux (list* x a b) y))))))
 
1002
 
 
1003
(defthm c1-not-sdiff
 
1004
  (implies (and (isect x y) (c1 x))
 
1005
           (not (sdiff x y)))
 
1006
  :hints (("Goal" :in-theory (enable norm->set set->norm)
 
1007
           :expand (:free (x) (sdiff-aux (list x) y)))))
 
1008
 
 
1009
 
 
1010
;; we now disable the top-level functions to keep their
 
1011
;; definitions from being expanded
 
1012
 
 
1013
(in-theory (disable in subset isect unite sdiff card s1 scar c1))
 
1014
 
 
1015
;; the following macro will enable/disable the executable-counterparts
 
1016
 
 
1017
(defmacro ec-sets (x)
 
1018
  `(in-theory (,(if x 'enable 'disable) 
 
1019
               (in) (subset) (isect) (unite) 
 
1020
               (sdiff) (card) (s1) (scar) (c1))))
 
1021
 
 
1022
;; we will begin with the executable-counterparts disabled
 
1023
 
 
1024
(ec-sets nil)
 
1025
 
 
1026
;; the following macro is a convenient way to define constants, it is similar
 
1027
;; to the 'list macro
 
1028
 
 
1029
(defmacro make-set (&rest elems)
 
1030
  (if (endp elems) '(emptyset) 
 
1031
    `(sadd ,(first elems) (make-set ,@(rest elems)))))
 
1032
 
 
1033
 
 
1034
 
 
1035
;; we conclude with a few corollaries
 
1036
 
 
1037
(defthm unite-iff-or
 
1038
  (iff (unite x y) (or x y))
 
1039
  :hints (("Goal" :cases ((not x) (not y)))))
 
1040
 
 
1041
(defthm unite-x-absorption
 
1042
  (equal (unite x (unite x y)) (unite x y)))
 
1043
 
 
1044
(defthm c1-of-sadd
 
1045
  (equal (c1 (sadd e x)) (if (c1 x) (equal x (s1 e)) (not x))))
 
1046
 
 
1047
(defthm equal-s1-redux
 
1048
  (equal (equal (s1 a) (s1 b)) (equal a b))
 
1049
  :hints (("Goal" :in-theory (enable s1))))
 
1050
 
 
1051
(defthm wrap-up-s1-equal-to-c1
 
1052
  (equal (equal (s1 (scar s)) s) (c1 s))
 
1053
  :hints (("Goal" :in-theory (enable s1 scar c1))))
 
1054
 
 
1055
(defthm c1-in-redux-scar
 
1056
  (implies (c1 s) (equal (in e s) (equal e (scar s))))
 
1057
  :hints (("Goal" :in-theory (enable in c1 scar))))
 
1058
 
 
1059
(local
 
1060
(defthm setp-cons-redux
 
1061
  (equal (setp (cons x y))
 
1062
         (and (setp y) (implies y (<< x (car y)))))))
 
1063
 
 
1064
(defthm equal-sadd-s1-redux
 
1065
  (equal (equal (sadd e x) (s1 a))
 
1066
         (and (equal e a) (implies x (equal x (s1 e)))))
 
1067
  :hints (("Goal" :in-theory (enable s1 unite norm->set set->norm)
 
1068
           :expand ((unite-aux (list e) x)))))
 
1069
 
 
1070
 
 
1071
 
 
1072
 
 
1073
#|
 
1074
 
 
1075
 
 
1076
 
 
1077
> I propose the following additions to the sets book:
 
1078
> 
 
1079
> (defthm sdiff-x-x
 
1080
>   (equal (sdiff x x)
 
1081
>        (empty-set)))
 
1082
 
 
1083
The following rule subsumes yours and I think would be
 
1084
a better addition:
 
1085
 
 
1086
(defthm sdiff-superset
 
1087
  (implies (subset x y)
 
1088
           (equal (sdiff x y) 
 
1089
                  (empty-set))))
 
1090
 
 
1091
> ;(add similar lemmas about other functions than unite
 
1092
> (e.g., isect)?
 
1093
> (defthm unite-reflexes-2
 
1094
>   (equal (unite x (unite x y))
 
1095
>        (unite x y)))
 
1096
> 
 
1097
> ;and can you prove this one for me?
 
1098
> (defthm sdiff-sdiff
 
1099
>   (equal (sdiff (sdiff x y) y)
 
1100
>        (sdiff x y))
 
1101
> )
 
1102
 
 
1103
absorption rules for unite, isect, and sdiff (on the right)
 
1104
would be good. I have no idea why I had not considered adding
 
1105
these before. I will probably generalize them to have subset
 
1106
hypothesis.
 
1107
 
 
1108
> BTW, what's the status of the sets book?  Will it be
 
1109
> released with ACL2?
 
1110
 
 
1111
It is in one of the workshops, although I am uncertain if it
 
1112
is updated. I will probably get Matt to add it to the misc
 
1113
directory (especially with some of the recent additions to
 
1114
the records book which make use of the sets book).
 
1115
 
 
1116
> I also need:
 
1117
> 
 
1118
> (defthm unite-sdiff-hack
 
1119
>   (equal (unite x (sdiff y x))
 
1120
>        (unite x y)))
 
1121
 
 
1122
Hmmm. I am uncertain if this is a proper reduction. Intuitively,
 
1123
while the lhs is a bigger term, it is smaller in terms of
 
1124
cardinality. I will need to think about this case, but offhand,
 
1125
I don't see this as an obviously good addition to the sets book.
 
1126
 
 
1127
> (BTW, I'm assuming its okay to ask you to prove these
 
1128
> since they'd make good additions to the sets book,
 
1129
> which you are developing.  If you'd rather not be
 
1130
> bothered with this, let me know.)
 
1131
 
 
1132
Please feel free to make suggestions (just don't expect that I
 
1133
will always be quick in handling the suggestions). I like using
 
1134
the sets book and would like to see others use it as well. (I am
 
1135
generally an advocate of having books with rewrite rules which
 
1136
are "context-free" -- well as context-free as possible).
 
1137
 
 
1138
  -Rob
 
1139
 
 
1140
 
 
1141
> i talked with Matt (the other "old-timer") and we
 
1142
> are
 
1143
> in tacit agreement that we should change
 
1144
> "records.lisp"
 
1145
> to "maps.lisp" (the new version with all of the
 
1146
> various
 
1147
> improvements and which includes the sets book). But,
 
1148
> I want to wait ask about this at the next ACL2
 
1149
> meeting
 
1150
> to get an idea of how many people (if any) are using
 
1151
> the
 
1152
> records book.
 
1153
 
 
1154
Excellent.  
 
1155
 
 
1156
My sense is that people aren't using the records/maps
 
1157
book enough (and that, in general, people don't
 
1158
appreciate the importance of the tricks done to make
 
1159
the records book clean).  Did anyone ever give a talk
 
1160
on records/maps at the ACL2 seminar?
 
1161
 
 
1162
I'm changing my copy of the "M5" JVM model to use
 
1163
records, and I think this is clearly the way to go. 
 
1164
(There are some subtleties, but I now have a fairly
 
1165
clean algebra for the heap.)  If J's folks keep
 
1166
hearing about this from enough people, maybe they'll
 
1167
use records for M6.  Hanbing seems to be in charge of
 
1168
M6.
 
1169
 
 
1170
> > BTW, are there easy proofs for either of the
 
1171
> following
 
1172
> > (which I've left as axioms in order to get on with
 
1173
> my
 
1174
> > JVM proofs)?  I'm not terribly familiar with the
 
1175
> sets
 
1176
> > book, and I didn't find an easy proof for these.
 
1177
> > 
 
1178
> > (defaxiom sdiff-sdiff
 
1179
> >   (equal (ACL2::SDIFF (ACL2::SDIFF Z X) X)
 
1180
> >      (ACL2::SDIFF Z X)))
 
1181
> >
 
1182
> > (defaxiom unite-hack
 
1183
> >   (equal (acl2::unite x (acl2::sdiff z x))
 
1184
> >      (acl2::unite x z)))
 
1185
> 
 
1186
> I believe these are provable, but not easily proven
 
1187
> in
 
1188
> terms of the existing rules.
 
1189
> 
 
1190
> I am planning on doing some work with the records (I
 
1191
> mean
 
1192
> "maps") and sets books this weekend. The updates
 
1193
> should
 
1194
> cover these theorems (and many others). I will send
 
1195
> them
 
1196
> to you on Monday.
 
1197
 
 
1198
That would be great!  Thanks.  I've been spending a
 
1199
lot of time making changes to M5 and thinking about
 
1200
sets, maps, and other implementation details, instead
 
1201
of actually doing the proofs I'm supposed to be doing
 
1202
(about java.util.linkedlist).  Even so, Dill seems
 
1203
satisfied with my progress.  Once we get the JVM model
 
1204
(and the sets and maps books) stabilized, I should be
 
1205
much more productive and should be able to totally
 
1206
impress him.
 
1207
 
 
1208
Thanks,
 
1209
-Eric
 
1210
 
 
1211
 
 
1212
__________________________________________________
 
1213
Do you Yahoo!?
 
1214
Yahoo! Tax Center - forms, calculators, tips, more
 
1215
http://taxes.yahoo.com/
 
1216
 
 
1217
 
 
1218
 
 
1219
 
 
1220
|#