← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2002/martin-alonso-hidalgo-ruiz/support/generic-multiset.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/2002/martin-alonso-hidalgo-ruiz/support/generic-multiset.lisp
 
1
;;;============================================================================
 
2
;;;
 
3
;;; Finite multiset generic theory.
 
4
;;;
 
5
;;;============================================================================
 
6
 
 
7
#| Certification code:
 
8
 
 
9
(certify-book "generic-multiset")
 
10
 
 
11
|#
 
12
 
 
13
(in-package "ACL2")
 
14
 
 
15
;;;----------------------------------------------------------------------------
 
16
;;;
 
17
;;; A finite multiset generic model:
 
18
;;;
 
19
;;;----------------------------------------------------------------------------
 
20
 
 
21
(encapsulate
 
22
 (((select *) => *)
 
23
  ((reduct *) => *)
 
24
  ((include * *) => *)
 
25
  ((empty *) => *)
 
26
  ((measure *) => *)
 
27
  ((equiv * *) => *))
 
28
 
 
29
 (local
 
30
  (defun select (m)
 
31
    (car m)))
 
32
 
 
33
 (local
 
34
  (defun reduct (m)
 
35
    (cdr m)))
 
36
 
 
37
 (local
 
38
  (defun include (e m)
 
39
    (cons e m)))
 
40
 
 
41
 (local 
 
42
  (defun empty (m)
 
43
    (atom m)))
 
44
 
 
45
 (local
 
46
  (defun measure (m)
 
47
    (acl2-count m)))
 
48
 
 
49
 (defthm o-p-measure
 
50
   (o-p (measure m)))
 
51
 
 
52
 (defthm reduct-measure
 
53
   (implies (not (empty m))
 
54
            (o< (measure (reduct m)) (measure m))))
 
55
 
 
56
 (local
 
57
  (defun equiv (e1 e2)
 
58
    (equal e1 e2)))
 
59
 
 
60
 (defequiv equiv)
 
61
 
 
62
 (defun count-bag-equiv (e m)
 
63
   (declare (xargs :measure (measure m)))
 
64
   (cond ((empty m) 0)
 
65
         ((equiv e (select m)) 
 
66
          (1+ (count-bag-equiv e (reduct m))))
 
67
         (t (count-bag-equiv e (reduct m)))))
 
68
 
 
69
; The following was added by Matt Kaufmann after ACL2 Version 3.4 because of
 
70
; a soundness bug fix; see ``subversive'' in :doc note-3-5.
 
71
 (defthm count-bag-equiv-type
 
72
   (natp (count-bag-equiv e m))
 
73
   :rule-classes :type-prescription)
 
74
 
 
75
 (defthm count-include
 
76
   (equal (count-bag-equiv e1 (include e2 m))
 
77
          (if (equiv e1 e2)
 
78
              (1+ (count-bag-equiv e1 m))
 
79
              (count-bag-equiv e1 m))))
 
80
 
 
81
 )
 
82
 
 
83
(defun count-bag-equiv-induct (e m)
 
84
  (declare (xargs :measure (measure m)))
 
85
  (cond ((empty m) t)
 
86
        ((equiv e (select m))
 
87
         (count-bag-equiv-induct e (reduct m)))
 
88
        (t (count-bag-equiv-induct e (reduct m)))))
 
89
 
 
90
(defthm count-bag-equiv-induction t
 
91
  :rule-classes
 
92
  ((:induction :pattern (count-bag-equiv e m)
 
93
               :condition t
 
94
               :scheme (count-bag-equiv-induct e m))))
 
95
 
 
96
(defcong equiv equal (count-bag-equiv e m) 1)
 
97
 
 
98
;;;----------------------------------------------------------------------------
 
99
;;;
 
100
;;; Multiset membership relation:
 
101
;;;
 
102
;;;----------------------------------------------------------------------------
 
103
 
 
104
(defun member-bag-equiv (e m)
 
105
  (declare (xargs :measure (measure m)))
 
106
  (cond ((empty m) nil)
 
107
        ((equiv e (select m)) t)
 
108
        (t (member-bag-equiv e (reduct m)))))
 
109
 
 
110
(defcong equiv iff (member-bag-equiv e m) 1)
 
111
 
 
112
(defthm member-bag-equiv-count->=-1
 
113
  (iff (member-bag-equiv e m)
 
114
       (>= (count-bag-equiv e m) 1))
 
115
  :rule-classes
 
116
  ((:definition
 
117
 
 
118
; Added by Matt Kaufmann, 3/25/06, after v2-9-4 in order to accommodate new
 
119
; check that equivalence relation for a definition rule must be 'equal if we
 
120
; are to expand with it.
 
121
 
 
122
    :install-body nil)))
 
123
 
 
124
;;;----------------------------------------------------------------------------
 
125
;;;
 
126
;;; Removing one occurrence from a multiset:
 
127
;;;
 
128
;;;----------------------------------------------------------------------------
 
129
 
 
130
(defun remove-one-bag-equiv (e m)
 
131
  (declare (xargs :measure (measure m)))
 
132
  (cond ((empty m) m)
 
133
        ((equiv e (select m)) (reduct m))
 
134
        (t (include (select m)
 
135
                    (remove-one-bag-equiv e (reduct m))))))
 
136
 
 
137
(defcong equiv equal (remove-one-bag-equiv e m) 1)
 
138
 
 
139
(defthm remove-one-count
 
140
  (equal (count-bag-equiv e1 (remove-one-bag-equiv e2 m))
 
141
         (if (and (member-bag-equiv e2 m)
 
142
                  (equiv e1 e2))
 
143
             (1- (count-bag-equiv e1 m))
 
144
             (count-bag-equiv e1 m))))
 
145
 
 
146
;;;----------------------------------------------------------------------------
 
147
;;;
 
148
;;; Sub-multiset relation:
 
149
;;;
 
150
;;;----------------------------------------------------------------------------
 
151
 
 
152
(defun sub-bag-equiv (m1 m2)
 
153
  (declare (xargs :measure (measure m1)))
 
154
  (cond ((empty m1) t)
 
155
        ((member-bag-equiv (select m1) m2) 
 
156
         (sub-bag-equiv (reduct m1) 
 
157
                        (remove-one-bag-equiv (select m1) m2)))
 
158
        (t nil)))
 
159
 
 
160
(defthm sub-bag-equiv-reflexive
 
161
  (sub-bag-equiv m m))
 
162
 
 
163
(defthm sub-bag-equiv-count
 
164
  (implies (sub-bag-equiv m1 m2)
 
165
    (<= (count-bag-equiv e m1) (count-bag-equiv e m2)))
 
166
  :rule-classes :linear)
 
167
 
 
168
;;; A useful strategy to prove the sub-multiset relation:
 
169
 
 
170
(encapsulate
 
171
 (((sub-bag-strategy-m1) => *)
 
172
  ((sub-bag-strategy-m2) => *)
 
173
  ((sub-bag-strategy-hyp) => *))
 
174
 
 
175
 (local (defun sub-bag-strategy-m1 () nil))
 
176
                       
 
177
 (local (defun sub-bag-strategy-m2 () nil))
 
178
                       
 
179
 (local (defun sub-bag-strategy-hyp () t))
 
180
 
 
181
 (defthm sub-bag-equiv-strategy-constraint
 
182
   (implies (sub-bag-strategy-hyp)
 
183
     (<= (count-bag-equiv strategy-e (sub-bag-strategy-m1))
 
184
         (count-bag-equiv strategy-e (sub-bag-strategy-m2))))))
 
185
 
 
186
(encapsulate
 
187
 ()
 
188
 
 
189
 (local
 
190
  (defun bag-sub-bag-equiv (m1 m2 m3)
 
191
    (declare (xargs :measure (measure m1)))
 
192
    (cond ((empty m1) t)
 
193
          ((<= (count-bag-equiv (select m1) m2)
 
194
               (count-bag-equiv (select m1) m3))
 
195
           (bag-sub-bag-equiv (reduct m1) m2 m3))
 
196
          (t nil))))
 
197
 
 
198
 (local
 
199
  (defthm bag-sub-bag-equiv-remove-one
 
200
    (implies (bag-sub-bag-equiv m1 m2 m3)
 
201
      (bag-sub-bag-equiv m1 (remove-one-bag-equiv e m2)
 
202
                         (remove-one-bag-equiv e m3)))))
 
203
 
 
204
 (local
 
205
  (defthm bag-sub-bag-equiv-sub-bag
 
206
    (implies (bag-sub-bag-equiv m1 m1 m2)
 
207
      (sub-bag-equiv m1 m2))
 
208
    :hints (("Goal" :induct (sub-bag-equiv m1 m2))
 
209
            ("Subgoal *1/2" :use (:instance bag-sub-bag-equiv-remove-one
 
210
                                            (m1 (reduct m1))
 
211
                                            (e (select m1))
 
212
                                            (m2 m1)
 
213
                                            (m3 m2))))))
 
214
 
 
215
 (local
 
216
  (defthm sub-bag-equiv-strategy-aux
 
217
    (implies (sub-bag-strategy-hyp)
 
218
      (bag-sub-bag-equiv m (sub-bag-strategy-m1) (sub-bag-strategy-m2)))))
 
219
 
 
220
 (defthm sub-bag-equiv-strategy
 
221
   (implies (sub-bag-strategy-hyp)
 
222
     (sub-bag-equiv (sub-bag-strategy-m1) (sub-bag-strategy-m2))))
 
223
 
 
224
)
 
225
 
 
226
(defun components-equal-sub-bag (form)
 
227
  (declare (xargs :mode :program))
 
228
 
 
229
  (case-match form
 
230
              
 
231
              (('IMPLIES form-hyp
 
232
                         ('EQUAL-BAG-EQUIV form-m1 form-m2))
 
233
               (mv form-hyp form-m1 form-m2))
 
234
              
 
235
              (('EQUAL-BAG-EQUIV form-m1 form-m2)
 
236
               (mv t form-m1 form-m2))
 
237
              
 
238
              (('IMPLIES form-hyp
 
239
                         ('SUB-BAG-EQUIV form-m1 form-m2))
 
240
               (mv form-hyp form-m1 form-m2))
 
241
              
 
242
              (('SUB-BAG-EQUIV form-m1 form-m2)
 
243
               (mv t form-m1 form-m2))
 
244
              
 
245
              (& (mv nil nil nil))))
 
246
 
 
247
(defun defstrategy-sub-bag-hint (id clause world)
 
248
  (declare (xargs :mode :program)
 
249
           (ignore id world))
 
250
 
 
251
  (mv-let (form-hyp form-m1 form-m2)
 
252
          (components-equal-sub-bag (first clause))
 
253
          (if form-hyp
 
254
              `(:use (:functional-instance 
 
255
                      sub-bag-equiv-strategy
 
256
                      (sub-bag-strategy-m1 (lambda () ,form-m1))
 
257
                      (sub-bag-strategy-m2 (lambda () ,form-m2))
 
258
                      (sub-bag-strategy-hyp (lambda () ,form-hyp))))
 
259
              nil)))
 
260
 
 
261
;;; The first use of the above strategy:
 
262
 
 
263
(defthm sub-bag-equiv-transitive
 
264
  (implies (and (sub-bag-equiv m1 m2)
 
265
                (sub-bag-equiv m2 m3))
 
266
    (sub-bag-equiv m1 m3))
 
267
  :hints (defstrategy-sub-bag-hint))
 
268
 
 
269
;;;----------------------------------------------------------------------------
 
270
;;;
 
271
;;; Multiset equality relation:
 
272
;;;
 
273
;;;----------------------------------------------------------------------------
 
274
 
 
275
(defun equal-bag-equiv (m1 m2)
 
276
  (and (sub-bag-equiv m1 m2)
 
277
       (sub-bag-equiv m2 m1)))
 
278
 
 
279
(defequiv equal-bag-equiv)
 
280
 
 
281
(defcong equal-bag-equiv iff (member-bag-equiv e m) 2)
 
282
 
 
283
(defcong equal-bag-equiv equal (count-bag-equiv e m) 2)
 
284
 
 
285
(defcong equal-bag-equiv iff (sub-bag-equiv m1 m2) 1)
 
286
 
 
287
(defcong equal-bag-equiv iff (sub-bag-equiv m1 m2) 2)
 
288
 
 
289
;;; A useful strategy to check multiset equality
 
290
 
 
291
(encapsulate
 
292
 (((equal-bag-strategy-m1) => *)
 
293
  ((equal-bag-strategy-m2) => *)
 
294
  ((equal-bag-strategy-hyp) => *))
 
295
 
 
296
 (local (defun equal-bag-strategy-m1 () nil))
 
297
                       
 
298
 (local (defun equal-bag-strategy-m2 () nil))
 
299
                       
 
300
 (local (defun equal-bag-strategy-hyp () t))
 
301
 
 
302
 (defthm equal-bag-equiv-strategy-constraint
 
303
   (implies (equal-bag-strategy-hyp)
 
304
     (equal (count-bag-equiv strategy-e (equal-bag-strategy-m1))
 
305
            (count-bag-equiv strategy-e (equal-bag-strategy-m2))))))
 
306
 
 
307
(encapsulate
 
308
 ()
 
309
 
 
310
 (local
 
311
  (defthm equal-bag-equiv-strategy-aux-1
 
312
    (implies (equal-bag-strategy-hyp)
 
313
      (sub-bag-equiv (equal-bag-strategy-m1) 
 
314
                     (equal-bag-strategy-m2)))
 
315
    :hints (defstrategy-sub-bag-hint)))
 
316
  
 
317
 (local
 
318
  (defthm equal-bag-equiv-strategy-aux-2
 
319
    (implies (equal-bag-strategy-hyp)
 
320
      (sub-bag-equiv (equal-bag-strategy-m2) 
 
321
                     (equal-bag-strategy-m1)))
 
322
    :hints (defstrategy-sub-bag-hint)))
 
323
 
 
324
 (defthm equal-bag-equiv-strategy
 
325
   (implies (equal-bag-strategy-hyp)
 
326
     (equal-bag-equiv (equal-bag-strategy-m1) 
 
327
                      (equal-bag-strategy-m2))))
 
328
 
 
329
)
 
330
 
 
331
(defun defstrategy-equal-bag-hint (id clause world)
 
332
  (declare (xargs :mode :program)
 
333
           (ignore id world))
 
334
 
 
335
  (mv-let (form-hyp form-m1 form-m2)
 
336
          (components-equal-sub-bag (first clause))
 
337
          (if form-hyp
 
338
              `(:use (:functional-instance 
 
339
                      equal-bag-equiv-strategy
 
340
                      (equal-bag-strategy-m1 (lambda () ,form-m1))
 
341
                      (equal-bag-strategy-m2 (lambda () ,form-m2))
 
342
                      (equal-bag-strategy-hyp (lambda () ,form-hyp))))
 
343
              nil)))
 
344
 
 
345
;;; The first use of the above strategy
 
346
 
 
347
(defcong equal-bag-equiv equal-bag-equiv (remove-one-bag-equiv e m) 2
 
348
  :hints (defstrategy-equal-bag-hint))
 
349
 
 
350
;;;----------------------------------------------------------------------------
 
351
;;;
 
352
;;; Multiset union:
 
353
;;;
 
354
;;;----------------------------------------------------------------------------
 
355
 
 
356
(defun union-bag-equiv (m1 m2)
 
357
  (declare (xargs :measure (measure m1)))
 
358
  (cond ((empty m1) m2)
 
359
        (t (include (select m1) 
 
360
                    (union-bag-equiv (reduct m1) m2)))))
 
361
 
 
362
(defthm count-union-bag-equiv
 
363
  (equal (count-bag-equiv e (union-bag-equiv m1 m2))
 
364
         (+ (count-bag-equiv e m1)
 
365
            (count-bag-equiv e m2))))
 
366
 
 
367
(defcong equal-bag-equiv equal-bag-equiv (union-bag-equiv m1 m2) 1
 
368
   :hints (defstrategy-equal-bag-hint))
 
369
 
 
370
(defcong equal-bag-equiv equal-bag-equiv (union-bag-equiv m1 m2) 2
 
371
   :hints (defstrategy-equal-bag-hint))
 
372
 
 
373
(defthm union-bag-equiv-conmutative
 
374
  (equal-bag-equiv (union-bag-equiv m2 m1)
 
375
                   (union-bag-equiv m1 m2))
 
376
  :hints (defstrategy-equal-bag-hint))
 
377
 
 
378
(defthm union-bag-equiv-associative
 
379
  (equal-bag-equiv (union-bag-equiv m1 (union-bag-equiv m2 m3))
 
380
                   (union-bag-equiv (union-bag-equiv m1 m2) m3))
 
381
  :hints (defstrategy-equal-bag-hint))
 
382
 
 
383
(defthm sub-union-bag-equiv-1
 
384
  (sub-bag-equiv m1 (union-bag-equiv m1 m2))
 
385
  :hints (defstrategy-sub-bag-hint))
 
386
 
 
387
(defthm sub-union-bag-equiv-2
 
388
  (sub-bag-equiv m2 (union-bag-equiv m1 m2))
 
389
  :hints (defstrategy-sub-bag-hint))
 
390
 
 
391
;;;----------------------------------------------------------------------------
 
392
;;;
 
393
;;; Multiset intersection:
 
394
;;;
 
395
;;;----------------------------------------------------------------------------
 
396
 
 
397
(defun inter-bag-equiv (m1 m2)
 
398
  (declare (xargs :measure (measure m1)))  
 
399
  (cond ((empty m1) m1)
 
400
        ((member-bag-equiv (select m1) m2)
 
401
         (include (select m1)
 
402
                  (inter-bag-equiv (reduct m1) 
 
403
                                   (remove-one-bag-equiv (select m1) m2))))
 
404
        (t (inter-bag-equiv (reduct m1) m2))))
 
405
 
 
406
(defthm count-inter-bag-equiv
 
407
  (equal (count-bag-equiv e (inter-bag-equiv m1 m2))
 
408
         (min (count-bag-equiv e m1)
 
409
              (count-bag-equiv e m2))))
 
410
 
 
411
(defcong equal-bag-equiv equal-bag-equiv (inter-bag-equiv m1 m2) 1
 
412
  :hints (defstrategy-equal-bag-hint))
 
413
 
 
414
(defcong equal-bag-equiv equal-bag-equiv (inter-bag-equiv m1 m2) 2
 
415
  :hints (defstrategy-equal-bag-hint))
 
416
 
 
417
(defthm inter-bag-equiv-idempotent
 
418
  (equal-bag-equiv (inter-bag-equiv m m) m)
 
419
  :hints (defstrategy-equal-bag-hint))
 
420
 
 
421
(defthm inter-bag-equiv-conmutative
 
422
  (equal-bag-equiv (inter-bag-equiv m2 m1)
 
423
                   (inter-bag-equiv m1 m2))
 
424
  :hints (defstrategy-equal-bag-hint))
 
425
 
 
426
(defthm inter-bag-equiv-associative
 
427
  (equal-bag-equiv (inter-bag-equiv m1 (inter-bag-equiv m2 m3))
 
428
                   (inter-bag-equiv (inter-bag-equiv m1 m2) m3))
 
429
  :hints (defstrategy-equal-bag-hint))
 
430
 
 
431
(defthm sub-inter-bag-equiv-1
 
432
  (sub-bag-equiv (inter-bag-equiv m1 m2) m1)
 
433
  :hints (defstrategy-sub-bag-hint))
 
434
 
 
435
(defthm sub-inter-bag-equiv-2
 
436
  (sub-bag-equiv (inter-bag-equiv m1 m2) m2)
 
437
  :hints (defstrategy-sub-bag-hint))
 
438
 
 
439
(defthm inter-bag-equiv-greatest
 
440
  (implies (and (sub-bag-equiv m1 m2)
 
441
                (sub-bag-equiv m1 m3))
 
442
    (sub-bag-equiv m1 (inter-bag-equiv m2 m3)))
 
443
  :hints (defstrategy-sub-bag-hint))
 
444
 
 
445
;;;----------------------------------------------------------------------------
 
446
;;;
 
447
;;; Multiset minimal union:
 
448
;;;
 
449
;;;----------------------------------------------------------------------------
 
450
 
 
451
(defun unimin-bag-equiv (m1 m2)
 
452
  (declare (xargs :measure (measure m1)))
 
453
  (cond ((empty m1) m2)
 
454
        ((member-bag-equiv (select m1) m2)
 
455
         (include (select m1)
 
456
                  (unimin-bag-equiv (reduct m1) 
 
457
                                    (remove-one-bag-equiv (select m1) m2))))
 
458
        (t (include (select m1) (unimin-bag-equiv (reduct m1) m2)))))
 
459
 
 
460
(defthm count-unimin-bag-equiv
 
461
  (equal (count-bag-equiv e (unimin-bag-equiv m1 m2))
 
462
         (max (count-bag-equiv e m1)
 
463
              (count-bag-equiv e m2))))
 
464
 
 
465
(defcong equal-bag-equiv equal-bag-equiv (unimin-bag-equiv m1 m2) 1
 
466
  :hints (defstrategy-equal-bag-hint))
 
467
 
 
468
(defcong equal-bag-equiv equal-bag-equiv (unimin-bag-equiv m1 m2) 2
 
469
  :hints (defstrategy-equal-bag-hint))
 
470
 
 
471
(defthm unimin-bag-equiv-idempotent
 
472
  (equal-bag-equiv (unimin-bag-equiv m m) m)
 
473
  :hints (defstrategy-equal-bag-hint))
 
474
 
 
475
(defthm unimin-bag-equiv-conmutative
 
476
  (equal-bag-equiv (unimin-bag-equiv m2 m1)
 
477
                   (unimin-bag-equiv m1 m2))
 
478
  :hints (defstrategy-equal-bag-hint))
 
479
 
 
480
(defthm unimin-bag-equiv-associative
 
481
  (equal-bag-equiv (unimin-bag-equiv m1 (unimin-bag-equiv m2 m3))
 
482
                   (unimin-bag-equiv (unimin-bag-equiv m1 m2) m3))
 
483
  :hints (defstrategy-equal-bag-hint))
 
484
 
 
485
(defthm sub-unimin-bag-equiv-1
 
486
  (sub-bag-equiv m1 (unimin-bag-equiv m1 m2))
 
487
  :hints (defstrategy-sub-bag-hint))
 
488
 
 
489
(defthm sub-unimin-bag-equiv-2
 
490
  (sub-bag-equiv m2 (unimin-bag-equiv m1 m2))
 
491
  :hints (defstrategy-sub-bag-hint))
 
492
 
 
493
(defthm unimin-bag-equiv-least
 
494
  (implies (and (sub-bag-equiv m1 m3)
 
495
                (sub-bag-equiv m2 m3))
 
496
    (sub-bag-equiv (unimin-bag-equiv m1 m2) m3))
 
497
  :hints (defstrategy-sub-bag-hint))
 
498
 
 
499
;;;----------------------------------------------------------------------------
 
500
;;;
 
501
;;; Multiset difference:
 
502
;;;
 
503
;;;----------------------------------------------------------------------------
 
504
 
 
505
(defun diff-bag-equiv (m1 m2)
 
506
  (declare (xargs :measure (measure m2)))
 
507
  (cond ((empty m2) m1)
 
508
        (t (diff-bag-equiv (remove-one-bag-equiv (select m2) m1) 
 
509
                           (reduct m2)))))
 
510
 
 
511
(defthm count-bag-equiv-diff-bag
 
512
  (equal (count-bag-equiv e (diff-bag-equiv m1 m2))
 
513
         (if (> (- (count-bag-equiv e m1)
 
514
                   (count-bag-equiv e m2)) 0)
 
515
             (- (count-bag-equiv e m1)
 
516
                (count-bag-equiv e m2))
 
517
             0)))
 
518
 
 
519
(defcong equal-bag-equiv equal-bag-equiv (diff-bag-equiv m1 m2) 1
 
520
  :hints (defstrategy-equal-bag-hint))
 
521
 
 
522
(defcong equal-bag-equiv equal-bag-equiv (diff-bag-equiv m1 m2) 2
 
523
  :hints (defstrategy-equal-bag-hint))
 
524
 
 
525
(defthm diff-union-1-equal-bag-equiv
 
526
  (equal-bag-equiv (diff-bag-equiv (union-bag-equiv l1 l2)
 
527
                                   (union-bag-equiv l1 l3))
 
528
                   (diff-bag-equiv l2 l3))
 
529
  :hints (defstrategy-equal-bag-hint))
 
530
 
 
531
(defthm diff-union-2-equal-bag-equiv
 
532
  (equal-bag-equiv (diff-bag-equiv (union-bag-equiv l2 l1)
 
533
                                   (union-bag-equiv l3 l1))
 
534
                   (diff-bag-equiv l2 l3))
 
535
  :hints (defstrategy-equal-bag-hint))
 
536
 
 
537
;;;----------------------------------------------------------------------------
 
538
;;; 
 
539
;;; Defining the generic theory:
 
540
;;;
 
541
;;;----------------------------------------------------------------------------
 
542
 
 
543
(include-book "generic-theory")
 
544
 
 
545
#|
 
546
 
 
547
(get-event-lst 
 
548
 '(member-bag-equiv
 
549
   EQUIV-IMPLIES-IFF-MEMBER-BAG-EQUIV-1
 
550
   remove-one-bag-equiv
 
551
   EQUIV-IMPLIES-EQUAL-REMOVE-ONE-BAG-EQUIV-1
 
552
   sub-bag-equiv
 
553
   sub-bag-equiv-reflexive
 
554
   sub-bag-equiv-transitive
 
555
   equal-bag-equiv
 
556
   EQUAL-BAG-EQUIV-IS-AN-EQUIVALENCE
 
557
   EQUAL-BAG-EQUIV-IMPLIES-IFF-MEMBER-BAG-EQUIV-2
 
558
   EQUAL-BAG-EQUIV-IMPLIES-IFF-SUB-BAG-EQUIV-1
 
559
   EQUAL-BAG-EQUIV-IMPLIES-IFF-SUB-BAG-EQUIV-2
 
560
   EQUAL-BAG-EQUIV-IMPLIES-EQUAL-BAG-EQUIV-REMOVE-ONE-BAG-EQUIV-2
 
561
   union-bag-equiv
 
562
   EQUAL-BAG-EQUIV-IMPLIES-EQUAL-BAG-EQUIV-UNION-BAG-EQUIV-1
 
563
   EQUAL-BAG-EQUIV-IMPLIES-EQUAL-BAG-EQUIV-UNION-BAG-EQUIV-2
 
564
   union-bag-equiv-conmutative
 
565
   union-bag-equiv-associative
 
566
   sub-union-bag-equiv-1
 
567
   sub-union-bag-equiv-2
 
568
   inter-bag-equiv
 
569
   EQUAL-BAG-EQUIV-IMPLIES-EQUAL-BAG-EQUIV-INTER-BAG-EQUIV-1
 
570
   EQUAL-BAG-EQUIV-IMPLIES-EQUAL-BAG-EQUIV-INTER-BAG-EQUIV-2
 
571
   inter-bag-equiv-idempotent
 
572
   inter-bag-equiv-conmutative
 
573
   inter-bag-equiv-associative
 
574
   sub-inter-bag-equiv-1
 
575
   sub-inter-bag-equiv-2
 
576
   inter-bag-equiv-greatest
 
577
   unimin-bag-equiv
 
578
   EQUAL-BAG-EQUIV-IMPLIES-EQUAL-BAG-EQUIV-UNIMIN-BAG-EQUIV-1
 
579
   EQUAL-BAG-EQUIV-IMPLIES-EQUAL-BAG-EQUIV-UNIMIN-BAG-EQUIV-2
 
580
   unimin-bag-equiv-idempotent
 
581
   unimin-bag-equiv-conmutative
 
582
   unimin-bag-equiv-associative
 
583
   sub-unimin-bag-equiv-1
 
584
   sub-unimin-bag-equiv-2
 
585
   unimin-bag-equiv-least
 
586
   diff-bag-equiv
 
587
   EQUAL-BAG-EQUIV-IMPLIES-EQUAL-BAG-EQUIV-DIFF-BAG-EQUIV-1
 
588
   EQUAL-BAG-EQUIV-IMPLIES-EQUAL-BAG-EQUIV-DIFF-BAG-EQUIV-2
 
589
   diff-union-1-equal-bag-equiv
 
590
   diff-union-2-equal-bag-equiv))
 
591
 
 
592
|#
 
593
 
 
594
(defconst *multiset*
 
595
  '((DEFUN MEMBER-BAG-EQUIV (E M)
 
596
      (DECLARE (XARGS :MEASURE (MEASURE M)))
 
597
      (COND ((EMPTY M) NIL)
 
598
            ((EQUIV E (SELECT M)) T)
 
599
            (T (MEMBER-BAG-EQUIV E (REDUCT M)))))
 
600
    (DEFTHM EQUIV-IMPLIES-IFF-MEMBER-BAG-EQUIV-1
 
601
      (IMPLIES (EQUIV E E-EQUIV)
 
602
               (IFF (MEMBER-BAG-EQUIV E M)
 
603
                    (MEMBER-BAG-EQUIV E-EQUIV M)))
 
604
      :RULE-CLASSES (:CONGRUENCE))
 
605
    (DEFUN REMOVE-ONE-BAG-EQUIV (E M)
 
606
      (DECLARE (XARGS :MEASURE (MEASURE M)))
 
607
      (COND ((EMPTY M) M)
 
608
            ((EQUIV E (SELECT M)) (REDUCT M))
 
609
            (T (INCLUDE (SELECT M)
 
610
                        (REMOVE-ONE-BAG-EQUIV E (REDUCT M))))))
 
611
    (DEFTHM EQUIV-IMPLIES-EQUAL-REMOVE-ONE-BAG-EQUIV-1
 
612
      (IMPLIES (EQUIV E E-EQUIV)
 
613
               (EQUAL (REMOVE-ONE-BAG-EQUIV E M)
 
614
                      (REMOVE-ONE-BAG-EQUIV E-EQUIV M)))
 
615
      :RULE-CLASSES (:CONGRUENCE))
 
616
    (DEFUN SUB-BAG-EQUIV (M1 M2)
 
617
      (DECLARE (XARGS :MEASURE (MEASURE M1)))
 
618
      (COND ((EMPTY M1) T)
 
619
            ((MEMBER-BAG-EQUIV (SELECT M1) M2)
 
620
             (SUB-BAG-EQUIV (REDUCT M1)
 
621
                            (REMOVE-ONE-BAG-EQUIV (SELECT M1) M2)))
 
622
            (T NIL)))
 
623
    (DEFTHM SUB-BAG-EQUIV-REFLEXIVE
 
624
      (SUB-BAG-EQUIV M M))
 
625
    (DEFTHM SUB-BAG-EQUIV-TRANSITIVE
 
626
      (IMPLIES (AND (SUB-BAG-EQUIV M1 M2)
 
627
                    (SUB-BAG-EQUIV M2 M3))
 
628
               (SUB-BAG-EQUIV M1 M3))
 
629
      :HINTS (DEFSTRATEGY-SUB-BAG-HINT))
 
630
    (DEFUN EQUAL-BAG-EQUIV (M1 M2)
 
631
      (AND (SUB-BAG-EQUIV M1 M2)
 
632
           (SUB-BAG-EQUIV M2 M1)))
 
633
    (DEFTHM EQUAL-BAG-EQUIV-IS-AN-EQUIVALENCE
 
634
      (AND (BOOLEANP (EQUAL-BAG-EQUIV X Y))
 
635
           (EQUAL-BAG-EQUIV X X)
 
636
           (IMPLIES (EQUAL-BAG-EQUIV X Y)
 
637
                    (EQUAL-BAG-EQUIV Y X))
 
638
           (IMPLIES (AND (EQUAL-BAG-EQUIV X Y)
 
639
                         (EQUAL-BAG-EQUIV Y Z))
 
640
                    (EQUAL-BAG-EQUIV X Z)))
 
641
      :RULE-CLASSES (:EQUIVALENCE))
 
642
    (DEFTHM EQUAL-BAG-EQUIV-IMPLIES-IFF-MEMBER-BAG-EQUIV-2
 
643
      (IMPLIES (EQUAL-BAG-EQUIV M M-EQUIV)
 
644
               (IFF (MEMBER-BAG-EQUIV E M)
 
645
                    (MEMBER-BAG-EQUIV E M-EQUIV)))
 
646
      :RULE-CLASSES (:CONGRUENCE))
 
647
    (DEFTHM EQUAL-BAG-EQUIV-IMPLIES-IFF-SUB-BAG-EQUIV-1
 
648
      (IMPLIES (EQUAL-BAG-EQUIV M1 M1-EQUIV)
 
649
               (IFF (SUB-BAG-EQUIV M1 M2)
 
650
                    (SUB-BAG-EQUIV M1-EQUIV M2)))
 
651
      :RULE-CLASSES (:CONGRUENCE))
 
652
    (DEFTHM EQUAL-BAG-EQUIV-IMPLIES-IFF-SUB-BAG-EQUIV-2
 
653
      (IMPLIES (EQUAL-BAG-EQUIV M2 M2-EQUIV)
 
654
               (IFF (SUB-BAG-EQUIV M1 M2)
 
655
                    (SUB-BAG-EQUIV M1 M2-EQUIV)))
 
656
      :RULE-CLASSES (:CONGRUENCE))
 
657
    (DEFTHM EQUAL-BAG-EQUIV-IMPLIES-EQUAL-BAG-EQUIV-REMOVE-ONE-BAG-EQUIV-2
 
658
      (IMPLIES (EQUAL-BAG-EQUIV M M-EQUIV)
 
659
               (EQUAL-BAG-EQUIV (REMOVE-ONE-BAG-EQUIV E M)
 
660
                                (REMOVE-ONE-BAG-EQUIV E M-EQUIV)))
 
661
      :RULE-CLASSES (:CONGRUENCE)
 
662
      :HINTS (DEFSTRATEGY-EQUAL-BAG-HINT))
 
663
    (DEFUN UNION-BAG-EQUIV (M1 M2)
 
664
      (DECLARE (XARGS :MEASURE (MEASURE M1)))
 
665
      (COND ((EMPTY M1) M2)
 
666
            (T (INCLUDE (SELECT M1)
 
667
                        (UNION-BAG-EQUIV (REDUCT M1) M2)))))
 
668
    (DEFTHM EQUAL-BAG-EQUIV-IMPLIES-EQUAL-BAG-EQUIV-UNION-BAG-EQUIV-1
 
669
      (IMPLIES (EQUAL-BAG-EQUIV M1 M1-EQUIV)
 
670
               (EQUAL-BAG-EQUIV (UNION-BAG-EQUIV M1 M2)
 
671
                                (UNION-BAG-EQUIV M1-EQUIV M2)))
 
672
      :RULE-CLASSES (:CONGRUENCE)
 
673
      :HINTS (DEFSTRATEGY-EQUAL-BAG-HINT))
 
674
    (DEFTHM EQUAL-BAG-EQUIV-IMPLIES-EQUAL-BAG-EQUIV-UNION-BAG-EQUIV-2
 
675
      (IMPLIES (EQUAL-BAG-EQUIV M2 M2-EQUIV)
 
676
               (EQUAL-BAG-EQUIV (UNION-BAG-EQUIV M1 M2)
 
677
                                (UNION-BAG-EQUIV M1 M2-EQUIV)))
 
678
      :RULE-CLASSES (:CONGRUENCE)
 
679
      :HINTS (DEFSTRATEGY-EQUAL-BAG-HINT))
 
680
    (DEFTHM UNION-BAG-EQUIV-CONMUTATIVE
 
681
      (EQUAL-BAG-EQUIV (UNION-BAG-EQUIV M2 M1)
 
682
                       (UNION-BAG-EQUIV M1 M2))
 
683
      :HINTS (DEFSTRATEGY-EQUAL-BAG-HINT))
 
684
    (DEFTHM UNION-BAG-EQUIV-ASSOCIATIVE
 
685
      (EQUAL-BAG-EQUIV (UNION-BAG-EQUIV M1 (UNION-BAG-EQUIV M2 M3))
 
686
                       (UNION-BAG-EQUIV (UNION-BAG-EQUIV M1 M2)
 
687
                                        M3))
 
688
      :HINTS (DEFSTRATEGY-EQUAL-BAG-HINT))
 
689
    (DEFTHM SUB-UNION-BAG-EQUIV-1
 
690
      (SUB-BAG-EQUIV M1 (UNION-BAG-EQUIV M1 M2))
 
691
      :HINTS (DEFSTRATEGY-SUB-BAG-HINT))
 
692
    (DEFTHM SUB-UNION-BAG-EQUIV-2
 
693
      (SUB-BAG-EQUIV M2 (UNION-BAG-EQUIV M1 M2))
 
694
      :HINTS (DEFSTRATEGY-SUB-BAG-HINT))
 
695
    (DEFUN INTER-BAG-EQUIV (M1 M2)
 
696
      (DECLARE (XARGS :MEASURE (MEASURE M1)))
 
697
      (COND ((EMPTY M1) M1)
 
698
            ((MEMBER-BAG-EQUIV (SELECT M1) M2)
 
699
             (INCLUDE (SELECT M1)
 
700
                      (INTER-BAG-EQUIV (REDUCT M1)
 
701
                                       (REMOVE-ONE-BAG-EQUIV (SELECT M1) M2))))
 
702
            (T (INTER-BAG-EQUIV (REDUCT M1) M2))))
 
703
    (DEFTHM EQUAL-BAG-EQUIV-IMPLIES-EQUAL-BAG-EQUIV-INTER-BAG-EQUIV-1
 
704
      (IMPLIES (EQUAL-BAG-EQUIV M1 M1-EQUIV)
 
705
               (EQUAL-BAG-EQUIV (INTER-BAG-EQUIV M1 M2)
 
706
                                (INTER-BAG-EQUIV M1-EQUIV M2)))
 
707
      :RULE-CLASSES (:CONGRUENCE)
 
708
      :HINTS (DEFSTRATEGY-EQUAL-BAG-HINT))
 
709
    (DEFTHM EQUAL-BAG-EQUIV-IMPLIES-EQUAL-BAG-EQUIV-INTER-BAG-EQUIV-2
 
710
      (IMPLIES (EQUAL-BAG-EQUIV M2 M2-EQUIV)
 
711
               (EQUAL-BAG-EQUIV (INTER-BAG-EQUIV M1 M2)
 
712
                                (INTER-BAG-EQUIV M1 M2-EQUIV)))
 
713
      :RULE-CLASSES (:CONGRUENCE)
 
714
      :HINTS (DEFSTRATEGY-EQUAL-BAG-HINT))
 
715
    (DEFTHM INTER-BAG-EQUIV-IDEMPOTENT
 
716
      (EQUAL-BAG-EQUIV (INTER-BAG-EQUIV M M)
 
717
                       M)
 
718
      :HINTS (DEFSTRATEGY-EQUAL-BAG-HINT))
 
719
    (DEFTHM INTER-BAG-EQUIV-CONMUTATIVE
 
720
      (EQUAL-BAG-EQUIV (INTER-BAG-EQUIV M2 M1)
 
721
                       (INTER-BAG-EQUIV M1 M2))
 
722
      :HINTS (DEFSTRATEGY-EQUAL-BAG-HINT))
 
723
    (DEFTHM INTER-BAG-EQUIV-ASSOCIATIVE
 
724
      (EQUAL-BAG-EQUIV (INTER-BAG-EQUIV M1 (INTER-BAG-EQUIV M2 M3))
 
725
                       (INTER-BAG-EQUIV (INTER-BAG-EQUIV M1 M2)
 
726
                                        M3))
 
727
      :HINTS (DEFSTRATEGY-EQUAL-BAG-HINT))
 
728
    (DEFTHM SUB-INTER-BAG-EQUIV-1
 
729
      (SUB-BAG-EQUIV (INTER-BAG-EQUIV M1 M2)
 
730
                     M1)
 
731
      :HINTS (DEFSTRATEGY-SUB-BAG-HINT))
 
732
    (DEFTHM SUB-INTER-BAG-EQUIV-2
 
733
      (SUB-BAG-EQUIV (INTER-BAG-EQUIV M1 M2)
 
734
                     M2)
 
735
      :HINTS (DEFSTRATEGY-SUB-BAG-HINT))
 
736
    (DEFTHM INTER-BAG-EQUIV-GREATEST
 
737
      (IMPLIES (AND (SUB-BAG-EQUIV M1 M2)
 
738
                    (SUB-BAG-EQUIV M1 M3))
 
739
               (SUB-BAG-EQUIV M1 (INTER-BAG-EQUIV M2 M3)))
 
740
      :HINTS (DEFSTRATEGY-SUB-BAG-HINT))
 
741
    (DEFUN UNIMIN-BAG-EQUIV (M1 M2)
 
742
      (DECLARE (XARGS :MEASURE (MEASURE M1)))
 
743
      (COND ((EMPTY M1) M2)
 
744
            ((MEMBER-BAG-EQUIV (SELECT M1) M2)
 
745
             (INCLUDE 
 
746
              (SELECT M1)
 
747
              (UNIMIN-BAG-EQUIV (REDUCT M1)
 
748
                                (REMOVE-ONE-BAG-EQUIV (SELECT M1) M2))))
 
749
            (T (INCLUDE (SELECT M1)
 
750
                        (UNIMIN-BAG-EQUIV (REDUCT M1) M2)))))
 
751
    (DEFTHM EQUAL-BAG-EQUIV-IMPLIES-EQUAL-BAG-EQUIV-UNIMIN-BAG-EQUIV-1
 
752
      (IMPLIES (EQUAL-BAG-EQUIV M1 M1-EQUIV)
 
753
               (EQUAL-BAG-EQUIV (UNIMIN-BAG-EQUIV M1 M2)
 
754
                                (UNIMIN-BAG-EQUIV M1-EQUIV M2)))
 
755
      :RULE-CLASSES (:CONGRUENCE)
 
756
      :HINTS (DEFSTRATEGY-EQUAL-BAG-HINT))
 
757
    (DEFTHM EQUAL-BAG-EQUIV-IMPLIES-EQUAL-BAG-EQUIV-UNIMIN-BAG-EQUIV-2
 
758
      (IMPLIES (EQUAL-BAG-EQUIV M2 M2-EQUIV)
 
759
               (EQUAL-BAG-EQUIV (UNIMIN-BAG-EQUIV M1 M2)
 
760
                                (UNIMIN-BAG-EQUIV M1 M2-EQUIV)))
 
761
      :RULE-CLASSES (:CONGRUENCE)
 
762
      :HINTS (DEFSTRATEGY-EQUAL-BAG-HINT))
 
763
    (DEFTHM UNIMIN-BAG-EQUIV-IDEMPOTENT
 
764
      (EQUAL-BAG-EQUIV (UNIMIN-BAG-EQUIV M M)
 
765
                       M)
 
766
      :HINTS (DEFSTRATEGY-EQUAL-BAG-HINT))
 
767
    (DEFTHM UNIMIN-BAG-EQUIV-CONMUTATIVE
 
768
      (EQUAL-BAG-EQUIV (UNIMIN-BAG-EQUIV M2 M1)
 
769
                       (UNIMIN-BAG-EQUIV M1 M2))
 
770
      :HINTS (DEFSTRATEGY-EQUAL-BAG-HINT))
 
771
    (DEFTHM UNIMIN-BAG-EQUIV-ASSOCIATIVE
 
772
      (EQUAL-BAG-EQUIV (UNIMIN-BAG-EQUIV M1 (UNIMIN-BAG-EQUIV M2 M3))
 
773
                       (UNIMIN-BAG-EQUIV (UNIMIN-BAG-EQUIV M1 M2)
 
774
                                         M3))
 
775
      :HINTS (DEFSTRATEGY-EQUAL-BAG-HINT))
 
776
    (DEFTHM SUB-UNIMIN-BAG-EQUIV-1
 
777
      (SUB-BAG-EQUIV M1 (UNIMIN-BAG-EQUIV M1 M2))
 
778
      :HINTS (DEFSTRATEGY-SUB-BAG-HINT))
 
779
    (DEFTHM SUB-UNIMIN-BAG-EQUIV-2
 
780
      (SUB-BAG-EQUIV M2 (UNIMIN-BAG-EQUIV M1 M2))
 
781
      :HINTS (DEFSTRATEGY-SUB-BAG-HINT))
 
782
    (DEFTHM UNIMIN-BAG-EQUIV-LEAST
 
783
      (IMPLIES (AND (SUB-BAG-EQUIV M1 M3)
 
784
                    (SUB-BAG-EQUIV M2 M3))
 
785
               (SUB-BAG-EQUIV (UNIMIN-BAG-EQUIV M1 M2)
 
786
                              M3))
 
787
      :HINTS (DEFSTRATEGY-SUB-BAG-HINT))
 
788
    (DEFUN DIFF-BAG-EQUIV (M1 M2)
 
789
      (DECLARE (XARGS :MEASURE (MEASURE M2)))
 
790
      (COND ((EMPTY M2) M1)
 
791
            (T (DIFF-BAG-EQUIV (REMOVE-ONE-BAG-EQUIV (SELECT M2) M1)
 
792
                               (REDUCT M2)))))
 
793
    (DEFTHM EQUAL-BAG-EQUIV-IMPLIES-EQUAL-BAG-EQUIV-DIFF-BAG-EQUIV-1
 
794
      (IMPLIES (EQUAL-BAG-EQUIV M1 M1-EQUIV)
 
795
               (EQUAL-BAG-EQUIV (DIFF-BAG-EQUIV M1 M2)
 
796
                                (DIFF-BAG-EQUIV M1-EQUIV M2)))
 
797
      :RULE-CLASSES (:CONGRUENCE)
 
798
      :HINTS (DEFSTRATEGY-EQUAL-BAG-HINT))
 
799
    (DEFTHM EQUAL-BAG-EQUIV-IMPLIES-EQUAL-BAG-EQUIV-DIFF-BAG-EQUIV-2
 
800
      (IMPLIES (EQUAL-BAG-EQUIV M2 M2-EQUIV)
 
801
               (EQUAL-BAG-EQUIV (DIFF-BAG-EQUIV M1 M2)
 
802
                                (DIFF-BAG-EQUIV M1 M2-EQUIV)))
 
803
      :RULE-CLASSES (:CONGRUENCE)
 
804
      :HINTS (DEFSTRATEGY-EQUAL-BAG-HINT))
 
805
    (DEFTHM DIFF-UNION-1-EQUAL-BAG-EQUIV
 
806
      (EQUAL-BAG-EQUIV (DIFF-BAG-EQUIV (UNION-BAG-EQUIV L1 L2)
 
807
                                       (UNION-BAG-EQUIV L1 L3))
 
808
                       (DIFF-BAG-EQUIV L2 L3))
 
809
      :HINTS (DEFSTRATEGY-EQUAL-BAG-HINT))
 
810
    (DEFTHM DIFF-UNION-2-EQUAL-BAG-EQUIV
 
811
      (EQUAL-BAG-EQUIV (DIFF-BAG-EQUIV (UNION-BAG-EQUIV L2 L1)
 
812
                                       (UNION-BAG-EQUIV L3 L1))
 
813
                       (DIFF-BAG-EQUIV L2 L3))
 
814
      :HINTS (DEFSTRATEGY-EQUAL-BAG-HINT)))
 
815
  )
 
816
 
 
817
(make-generic-theory *multiset*)
 
818
 
 
819
;;;============================================================================