← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2004/davis/support/quantify.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/davis/support/quantify.lisp
 
1
; Fully Ordered Finite Sets, Version 0.9
 
2
; Copyright (C) 2003, 2004 Kookamara LLC
 
3
;
 
4
; Contact:
 
5
;
 
6
;   Kookamara LLC
 
7
;   11410 Windermere Meadows
 
8
;   Austin, TX 78759, USA
 
9
;   http://www.kookamara.com/
 
10
;
 
11
; License: (An MIT/X11-style license)
 
12
;
 
13
;   Permission is hereby granted, free of charge, to any person obtaining a
 
14
;   copy of this software and associated documentation files (the "Software"),
 
15
;   to deal in the Software without restriction, including without limitation
 
16
;   the rights to use, copy, modify, merge, publish, distribute, sublicense,
 
17
;   and/or sell copies of the Software, and to permit persons to whom the
 
18
;   Software is furnished to do so, subject to the following conditions:
 
19
;
 
20
;   The above copyright notice and this permission notice shall be included in
 
21
;   all copies or substantial portions of the Software.
 
22
;
 
23
;   THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 
24
;   IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 
25
;   FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 
26
;   AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 
27
;   LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
 
28
;   FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
 
29
;   DEALINGS IN THE SOFTWARE.
 
30
;
 
31
; Original author: Jared Davis <jared@kookamara.com>
 
32
;
 
33
;
 
34
; quantify.lisp
 
35
;
 
36
; This is an optional extension of the sets library, and is not included by
 
37
; default when you run (include-book "sets").
 
38
;
 
39
;
 
40
; Constructive Quantification over Sets and Lists.
 
41
;
 
42
; We create the macro, quantify-predicate, which introduces the following
 
43
; functions for any arbitrary predicate.
 
44
;
 
45
;     all<predicate>           all<not-predicate>
 
46
;     exists<predicate>        exists<not-predicate>
 
47
;     find<predicate>          find<not-predicate>
 
48
;     filter<predicate>        filter<not-predicate>
 
49
;
 
50
;     all-list<predicate>      all-list<not-predicate>
 
51
;     exists-list<predicate>   exists-list<not-predicate>
 
52
;     find-list<predicate>     find-list<not-predicate>
 
53
;     filter-list<predicate>   filter-list<not-predicate>
 
54
;
 
55
; In addition to introducing these functions, an entire rewriting strategy is
 
56
; introduced for reasoning about these functions with respect to sets and
 
57
; lists.
 
58
;
 
59
; Introductory Examples.
 
60
;
 
61
; Here are some of the most simple examples.  All of these predicates have only
 
62
; a single argument, and their guard is "t".
 
63
;
 
64
;     (SET::quantify-predicate (integerp x))
 
65
;     (SET::quantify-predicate (symbolp x))
 
66
;     (SET::quantify-predicate (rationalp x))
 
67
;     (SET::quantify-predicate (natp x))
 
68
;
 
69
; Notice that you cannot use macros here.  For example, the following is an
 
70
; error: (quantify-predicate (real/rationalp x)).  Once you have done the
 
71
; above, you can now run these functions, e.g.,
 
72
;
 
73
;     (SET::all<integerp> '(1 2 3)) = t
 
74
;     (SET::all<not-integerp> '(a b c)) = t
 
75
;     (SET::find<symbolp> '(1 2 3 a b c)) = a
 
76
;
 
77
; Controlling Packages.
 
78
;
 
79
; As you can see, all of these functions are introduced in the SETS package by
 
80
; default.  If you'd like them to be in a different place instead, you can
 
81
; specify the :in-package-of argument and provide a symbol from some other
 
82
; package.  For example, since defthm is in the ACL2 package, we might write:
 
83
;
 
84
;     (SET::quantify-predicate (eqlablep x)
 
85
;       :in-package-of defthm)
 
86
;
 
87
; And then the functions all<integerp>, all<not-integerp>, and so forth will be
 
88
; in the ACL2 package instead of the LISTS package.
 
89
;
 
90
;
 
91
; Multi-Argument Predicates.
 
92
;
 
93
; You can also quantify over predicates with many arguments.  As an example, we
 
94
; introduce the function lessp as follows:
 
95
;
 
96
;     (defun lessp (a b)
 
97
;       (declare (xargs :guard t))
 
98
;       (< (rfix a) (rfix b)))
 
99
;
 
100
;     (quantify-predicate (lessp a b))
 
101
;
 
102
; We could now ask, is every element in a set less than some maximum value?
 
103
; For example:
 
104
;
 
105
;     (all<lessp> '(1 2 3) 6) = t
 
106
;     (all<lessp> '(1 2 3) 2) = nil
 
107
;
 
108
;
 
109
;
 
110
; Supporting Guards.
 
111
;
 
112
; If efficiency is important, our predicate may have guards and we may want to
 
113
; put guards on the introduced functions.  For example, we might write
 
114
; fast-lessp below:
 
115
;
 
116
;     (defun fast-lessp (a b)
 
117
;       (declare (xargs :guard (and (rationalp a)
 
118
;                                   (rationalp b))))
 
119
;       (< a b))
 
120
;
 
121
; Now we need to supply an extra :guard argument so that the guards of
 
122
; all<fast-lessp>, exists<fast-lessp>, and so forth can be verified.
 
123
;
 
124
; When writing this guard, the list which all-list<fast-lessp> and so forth are
 
125
; iterating over will be called ?list, and the set that all<fast-lessp> and so
 
126
; forth are iterating over will be called ?set.  The other arguments will all
 
127
; be named with whatever names you gave them when you called
 
128
; quantify-predicate.  For example, below we name fast-lessp's second argument
 
129
; "max", so it will be named "max" in our guards as well.
 
130
;
 
131
;   Here's an example:
 
132
;
 
133
;     (in-package "ACL2")
 
134
;
 
135
;     (SET::quantify-predicate (rationalp x)
 
136
;       :in-package-of defthm)
 
137
;
 
138
;     (SET::quantify-predicate (fast-lessp x max)
 
139
;       :set-guard  ((all<rationalp> ?set))
 
140
;       :list-guard ((all-list<rationalp> ?list))
 
141
;       :arg-guard  ((rationalp max))
 
142
;       :in-package-of defthm)
 
143
;
 
144
;
 
145
; Disabling the theory.
 
146
;
 
147
; Calling quantify-predicate will result in a lot of theorems being introduced.
 
148
; You can disable all of these theorems by using the deftheory event
 
149
; theory<predicate>.  For example,
 
150
;
 
151
;     (in-theory (disable theory<integerp>))
 
152
;     (in-theory (disable theory<fast-lessp>))
 
153
;
 
154
; And so forth.
 
155
 
 
156
 
 
157
(in-package "SET")
 
158
(include-book "sets")
 
159
(set-verify-guards-eagerness 2)
 
160
 
 
161
 
 
162
 
 
163
; We introduce our theory as a constant so that we can derive
 
164
; new instances of it for concrete predicates
 
165
 
 
166
(defconst *positive-functions* '(
 
167
 
 
168
;; We introduce "list versions" of the functions so that we can reason
 
169
;; through mergesorts.
 
170
 
 
171
  (defun all-list (list-for-all-reduction)
 
172
    (declare (xargs :guard (true-listp list-for-all-reduction)))
 
173
    (if (endp list-for-all-reduction)
 
174
        t
 
175
      (and (predicate (car list-for-all-reduction))
 
176
           (all-list (cdr list-for-all-reduction)))))
 
177
 
 
178
  (defun exists-list (x)
 
179
    (declare (xargs :guard (true-listp x)))
 
180
    (cond ((endp x) nil)
 
181
          ((predicate (car x)) t)
 
182
          (t (exists-list (cdr x)))))
 
183
 
 
184
  (defun find-list (x)
 
185
    (declare (xargs :guard (true-listp x)))
 
186
    (cond ((endp x) nil)
 
187
          ((predicate (car x)) (car x))
 
188
          (t (find-list (cdr x)))))
 
189
 
 
190
  (defun filter-list (x)
 
191
    (declare (xargs :guard (true-listp x)))
 
192
    (cond ((endp x) nil)
 
193
          ((predicate (car x))
 
194
           (cons (car x) (filter-list (cdr x))))
 
195
          (t (filter-list (cdr x)))))
 
196
 
 
197
 
 
198
;; We also introduce "set versions" of the functions, so that we can
 
199
;; reason about sets.
 
200
 
 
201
  (defun all (set-for-all-reduction)
 
202
    (declare (xargs :guard (setp set-for-all-reduction)))
 
203
    (if (empty set-for-all-reduction)
 
204
        t
 
205
      (and (predicate (head set-for-all-reduction))
 
206
           (all (tail set-for-all-reduction)))))
 
207
 
 
208
  (defun exists (X)
 
209
    (declare (xargs :guard (setp X)))
 
210
    (cond ((empty X) nil)
 
211
          ((predicate (head X)) t)
 
212
          (t (exists (tail X)))))
 
213
 
 
214
  (defun find (X)
 
215
    (declare (xargs :guard (setp X)))
 
216
    (cond ((empty X) nil)
 
217
          ((predicate (head X)) (head X))
 
218
          (t (find (tail X)))))
 
219
 
 
220
  (defun filter (X)
 
221
    (declare (xargs :guard (setp X)))
 
222
    (declare (xargs :verify-guards nil))
 
223
    (cond ((empty X) (sfix X))
 
224
          ((predicate (head X))
 
225
           (insert (head X) (filter (tail X))))
 
226
          (t (filter (tail X)))))
 
227
 
 
228
  ))
 
229
 
 
230
; We then create "negative" versions of the above functions by
 
231
; performing a set of substitutions on the constants.
 
232
 
 
233
(defconst *negative-functions*
 
234
  (INSTANCE::instance-defuns *positive-functions*
 
235
     '(((predicate ?x)   (not (predicate ?x)))
 
236
       ((all ?x)         (all<not> ?x))
 
237
       ((exists ?x)      (exists<not> ?x))
 
238
       ((find ?x)        (find<not> ?x))
 
239
       ((filter ?x)      (filter<not> ?x))
 
240
       ((all-list ?x)    (all-list<not> ?x))
 
241
       ((exists-list ?x) (exists-list<not> ?x))
 
242
       ((find-list ?x)   (find-list<not> ?x))
 
243
       ((filter-list ?x) (filter-list<not> ?x)))))
 
244
 
 
245
 
 
246
; And then we smash together the positive and negative functions to
 
247
; create a single function list which can be instantiated later.
 
248
 
 
249
(defconst *functions*
 
250
  (append *positive-functions* *negative-functions*))
 
251
 
 
252
 
 
253
; Now we create the instance-*functions* macro which will allow us
 
254
; to actually derive an instance of all of the functions
 
255
 
 
256
(INSTANCE::instance *functions*)
 
257
 
 
258
 
 
259
; And we call the macro with no arguments, to introduce a verbatim
 
260
; copy of the theory.  In other words, we introduce the generic
 
261
; theory itself here.
 
262
 
 
263
(instance-*functions*)
 
264
 
 
265
 
 
266
(defconst *positive-theorems* '(
 
267
 
 
268
; List Theory Reasoning
 
269
;
 
270
; We begin with several theorems about the "list versions" of the
 
271
; above functions.
 
272
 
 
273
  (defthm all-list-type
 
274
    (or (equal (all-list x) t)
 
275
        (equal (all-list x) nil))
 
276
    :rule-classes :type-prescription)
 
277
 
 
278
  (defthm all-list-cdr
 
279
    (implies (all-list x)
 
280
             (all-list (cdr x))))
 
281
 
 
282
  (defthm all-list-endp
 
283
    (implies (endp x)
 
284
             (all-list x)))
 
285
 
 
286
  (defthm all-list-in
 
287
    (implies (and (all-list x)
 
288
                  (in-list a x))
 
289
             (predicate a)))
 
290
 
 
291
  (defthm all-list-in-2
 
292
    (implies (and (all-list x)
 
293
                  (not (predicate a)))
 
294
             (not (in-list a x))))
 
295
 
 
296
  (defthm all-list-cons
 
297
    (equal (all-list (cons a x))
 
298
           (and (predicate a)
 
299
                (all-list x))))
 
300
 
 
301
  (defthm all-list-append
 
302
    (equal (all-list (append x y))
 
303
           (and (all-list x)
 
304
                (all-list y))))
 
305
 
 
306
  (defthm all-list-nth
 
307
    (implies (and (all-list x)
 
308
                  (<= 0 n)
 
309
                  (< n (len x)))
 
310
             (predicate (nth n x))))
 
311
 
 
312
  (encapsulate nil
 
313
 
 
314
    (local (defthm lemma1
 
315
             (implies (and (all-list acc)
 
316
                           (all-list x))
 
317
                      (all-list (revappend x acc)))))
 
318
 
 
319
    (local (defthm lemma2
 
320
             (implies (not (all-list acc))
 
321
                      (not (all-list (revappend x acc))))))
 
322
 
 
323
    (local (defthm lemma3
 
324
             (implies (and (all-list acc)
 
325
                           (not (all-list x)))
 
326
                      (not (all-list (revappend x acc))))))
 
327
 
 
328
    (defthm all-list-revappend
 
329
      (equal (all-list (revappend x acc))
 
330
             (and (all-list x)
 
331
                  (all-list acc))))
 
332
  )
 
333
 
 
334
  (defthm all-list-reverse
 
335
    (equal (all-list (reverse x))
 
336
           (all-list x)))
 
337
 
 
338
  (defthm exists-list-elimination
 
339
    (equal (exists-list x)
 
340
           (not (all-list<not> x))))
 
341
 
 
342
  (defthm filter-list-true-list
 
343
    (true-listp (filter-list x))
 
344
    :rule-classes :type-prescription)
 
345
 
 
346
  (defthm filter-list-membership
 
347
    (equal (in-list a (filter-list x))
 
348
           (and (predicate a)
 
349
                (in-list a x))))
 
350
 
 
351
  (defthm filter-list-all-list
 
352
    (all-list (filter-list x)))
 
353
 
 
354
 
 
355
 
 
356
 
 
357
 
 
358
 
 
359
; Set Theory Reasoning
 
360
;
 
361
; Of course, really we are more interested in reasoning about sets
 
362
; than lists.  We write several theorems about our set functions.
 
363
 
 
364
  (defthm all-type
 
365
    (or (equal (all X) t)
 
366
        (equal (all X) nil))
 
367
    :rule-classes :type-prescription)
 
368
 
 
369
  (defthm all-sfix
 
370
    (equal (all (sfix X))
 
371
           (all X)))
 
372
 
 
373
  ;; TODO: extend to forward chaining.
 
374
 
 
375
  (defthm all-tail
 
376
    (implies (all X)
 
377
             (all (tail X))))
 
378
 
 
379
  (defthm all-empty
 
380
    (implies (empty X)
 
381
             (all X)))
 
382
 
 
383
  (defthm all-in
 
384
    (implies (and (all X)
 
385
                  (in a X))
 
386
             (predicate a)))
 
387
 
 
388
  (defthm all-in-2
 
389
    (implies (and (all X)
 
390
                  (not (predicate a)))
 
391
             (not (in a X))))
 
392
 
 
393
  (defthm all-insert
 
394
    (equal (all (insert a X))
 
395
           (and (predicate a)
 
396
                (all X)))
 
397
    :hints(("Goal" :induct (insert a X))))
 
398
 
 
399
  (defthm all-delete
 
400
    (implies (all X)
 
401
             (all (delete a X))))
 
402
 
 
403
  (defthm all-delete-2
 
404
    (implies (predicate a)
 
405
             (equal (all (delete a X))
 
406
                    (all X))))
 
407
 
 
408
  (defthm all-union
 
409
    (equal (all (union X Y))
 
410
           (and (all X)
 
411
                (all Y))))
 
412
 
 
413
  (defthm all-intersect-X
 
414
    (implies (all X)
 
415
             (all (intersect X Y))))
 
416
 
 
417
  (defthm all-intersect-Y
 
418
    (implies (all X)
 
419
             (all (intersect Y X))))
 
420
 
 
421
  (defthm all-difference
 
422
    (implies (all X)
 
423
             (all (difference X Y))))
 
424
 
 
425
  (defthm all-difference-2
 
426
    (implies (all Y)
 
427
             (equal (all (difference X Y))
 
428
                    (all X))))
 
429
 
 
430
 
 
431
  (defthm exists-elimination
 
432
    (equal (exists X)
 
433
           (not (all<not> X))))
 
434
 
 
435
 
 
436
  (defthm find-sfix
 
437
    (equal (find (sfix X))
 
438
           (find X)))
 
439
 
 
440
  (defthm find-witness
 
441
    (implies (not (all X))
 
442
             (and (in (find<not> X) X)
 
443
                  (not (predicate (find<not> X)))))
 
444
    :rule-classes :forward-chaining)
 
445
 
 
446
 
 
447
  (defthm filter-set
 
448
    (setp (filter X)))
 
449
 
 
450
  (defthm filter-sfix
 
451
    (equal (filter (sfix X))
 
452
           (filter X)))
 
453
 
 
454
  (defthm filter-in
 
455
    (equal (in a (filter X))
 
456
           (and (predicate a)
 
457
                (in a X)))
 
458
    :hints(("Goal" :induct (filter X))))
 
459
 
 
460
  (defthm filter-subset
 
461
    (subset (filter X) X))
 
462
 
 
463
  (defthm filter-all
 
464
    (all (filter X)))
 
465
 
 
466
  (defthm filter-all-2
 
467
    (implies (all X)
 
468
             (equal (filter X) (sfix X)))
 
469
    :hints(("Goal" :in-theory (disable double-containment))))
 
470
 
 
471
 
 
472
 
 
473
 
 
474
; In order to reason past a mergesort, we need to provide some
 
475
; theorems that tie together our list and set theories.  We begin
 
476
; this here.
 
477
 
 
478
  (defthm all-mergesort
 
479
    (equal (all (mergesort X))
 
480
           (all-list X)))
 
481
 
 
482
  (defthm all-list-applied-to-set
 
483
    (implies (setp X)
 
484
             (equal (all-list X)
 
485
                    (all X)))
 
486
    :hints(("Goal" :in-theory (enable setp empty sfix head tail))))
 
487
 
 
488
))
 
489
 
 
490
 
 
491
 
 
492
; Notice that the positive functions and the negative functions are
 
493
; symmetric.  We now invert the above theorem to create the
 
494
; corresponding theorems for the negative functions.
 
495
 
 
496
(defconst *negative-theorems*
 
497
  (INSTANCE::instance-rewrite *positive-theorems*
 
498
 
 
499
    ;; we first replace calls to "positive" functions with calls to
 
500
    ;; temporary symbols, which simply acts as placeholders.
 
501
 
 
502
   '(((predicate ?x)   (predicate-temp ?x))
 
503
     ((all ?x)         (all-temp ?x))
 
504
     ((exists ?x)      (exists-temp ?x))
 
505
     ((find ?x)        (find-temp ?x))
 
506
     ((filter ?x)      (filter-temp ?x))
 
507
     ((all-list ?x)    (all-list-temp ?x))
 
508
     ((exists-list ?x) (exists-list-temp ?x))
 
509
     ((find-list ?x)   (find-list-temp ?x))
 
510
     ((filter-list ?x) (filter-list-temp ?x))
 
511
 
 
512
     ;; now we replace calls to "negative" functions with calls to
 
513
     ;; positive functions.
 
514
 
 
515
     ((not (predicate ?x))  (predicate ?x))
 
516
     ((all<not> ?x)         (all ?x))
 
517
     ((exists<not> ?x)      (exists ?x))
 
518
     ((find<not> ?x)        (find ?x))
 
519
     ((filter<not> ?x)      (filter ?x))
 
520
     ((all-list<not> ?x)    (all-list ?x))
 
521
     ((exists-list<not> ?x) (exists-list ?x))
 
522
     ((find-list<not> ?x)   (find-list ?x))
 
523
     ((filter-list<not> ?x) (filter-list ?x))
 
524
 
 
525
     ;; and finally we replace our temporary placeholder symbols with
 
526
     ;; calls to the actual negative functions.
 
527
 
 
528
     ((predicate-temp ?x)   (not (predicate ?x)))
 
529
     ((all-temp ?x)         (all<not> ?x))
 
530
     ((exists-temp ?x)      (exists<not> ?x))
 
531
     ((find-temp ?x)        (find<not> ?x))
 
532
     ((filter-temp ?x)      (filter<not> ?x))
 
533
     ((all-list-temp ?x)    (all-list<not> ?x))
 
534
     ((exists-list-temp ?x) (exists-list<not> ?x))
 
535
     ((find-list-temp ?x)   (find-list<not> ?x))
 
536
     ((filter-list-temp ?x) (filter-list<not> ?x))
 
537
)))
 
538
 
 
539
 
 
540
; We now smash together the positive and negative theorems to form a
 
541
; single, complete theory.  Note that we have to rename all of the
 
542
; defthms in *negative-theorems* so that their names will not collide
 
543
; with the theorems in *theorems*.
 
544
 
 
545
(defconst *theorems*
 
546
  (append *positive-theorems*
 
547
          (INSTANCE::rename-defthms *negative-theorems* '-not)))
 
548
 
 
549
 
 
550
; As with the functions, we create a new macro which will allow us to
 
551
; derive new instances of our theorems.
 
552
 
 
553
(INSTANCE::instance *theorems*)
 
554
 
 
555
 
 
556
; And as before, we call the resulting macro with no arguments, which
 
557
; gives us a verbatim copy of the positive and negative theorems.
 
558
 
 
559
(instance-*theorems*)
 
560
 
 
561
 
 
562
 
 
563
 
 
564
 
 
565
 
 
566
 
 
567
; We already have an all-by-membership theorem set up for sets.  But,
 
568
; we would like to have a corresponding theorem to use with lists.  We
 
569
; create that here.
 
570
 
 
571
(encapsulate
 
572
 (((all-list-hyps) => *)
 
573
  ((all-list-list) => *))
 
574
 
 
575
 (local (defun all-list-hyps () nil))
 
576
 (local (defun all-list-list () nil))
 
577
 
 
578
 (defthmd list-membership-constraint
 
579
   (implies (all-list-hyps)
 
580
            (implies (in-list arbitrary-element (all-list-list))
 
581
                     (predicate arbitrary-element))))
 
582
)
 
583
 
 
584
(encapsulate ()
 
585
 
 
586
  (local (defthm witness-lemma
 
587
           (implies (not (all-list x))
 
588
                    (and (in-list (find-list<not> x) x)
 
589
                         (not (predicate (find-list<not> x)))))))
 
590
 
 
591
  (defthmd all-list-by-membership
 
592
    (implies (all-list-hyps)
 
593
             (all-list (all-list-list)))
 
594
    :hints(("Goal"
 
595
            :use (:instance list-membership-constraint
 
596
                  (arbitrary-element (find-list<not> (all-list-list)))))))
 
597
)
 
598
 
 
599
 
 
600
 
 
601
(defconst *final-theorems* '(
 
602
 
 
603
  (defthm cardinality-filter
 
604
    (equal (cardinality X)
 
605
           (+ (cardinality (filter X))
 
606
              (cardinality (filter<not> X))))
 
607
    :rule-classes :linear)
 
608
 
 
609
  (defthm all-subset
 
610
    (implies (and (all Y)
 
611
                  (subset X Y))
 
612
             (all X))
 
613
    :hints(("Goal"
 
614
            :use (:functional-instance all-by-membership
 
615
                  (all-hyps (lambda () (and (all Y)
 
616
                                            (subset X Y))))
 
617
                  (all-set  (lambda () X))))))
 
618
 
 
619
  (defthm all-subset-not
 
620
    (implies (and (all<not> Y)
 
621
                  (subset X Y))
 
622
             (all<not> X))
 
623
    :hints(("Goal"
 
624
            :use (:functional-instance all-by-membership
 
625
                  (all-hyps  (lambda () (and (all<not> Y)
 
626
                                             (subset X Y))))
 
627
                  (all-set   (lambda () X))
 
628
                  (predicate (lambda (x) (not (predicate x))))
 
629
                  (all       (lambda (x) (all<not> x)))))))
 
630
 
 
631
))
 
632
 
 
633
(INSTANCE::instance *final-theorems*)
 
634
(instance-*final-theorems*)
 
635
 
 
636
(verify-guards filter)
 
637
(verify-guards filter<not>)
 
638
 
 
639
 
 
640
 
 
641
 
 
642
; -------------------------------------------------------------------
 
643
;
 
644
;                   Instancing Concrete Theories
 
645
;
 
646
; -------------------------------------------------------------------
 
647
 
 
648
; Each concrete theory we instantiate will require the introduction of
 
649
; 16 new functions and a wealth of theorems.  We don't want to
 
650
; overburden the user with having to instantiate all of these and give
 
651
; them names, so we adopt a naming convention where the predicate's
 
652
; name is used to generate the names of the new functions.  Of course,
 
653
; we still have to generate the new names.
 
654
 
 
655
(defun mksym (name sym)
 
656
  (declare (xargs :mode :program))
 
657
  (intern-in-package-of-symbol (string-upcase name) sym))
 
658
 
 
659
(defun app (x y)
 
660
  (declare (xargs :mode :program))
 
661
  (string-append x y))
 
662
 
 
663
(defun ?ify (args)
 
664
  (declare (xargs :mode :program))
 
665
  (if (endp args)
 
666
      nil
 
667
    (cons (mksym (app "?" (symbol-name (car args)))
 
668
                 (car args))
 
669
          (?ify (cdr args)))))
 
670
 
 
671
(defun standardize-to-package (symbol-name replacement term)
 
672
  (declare (xargs :mode :program))
 
673
  (if (atom term)
 
674
      (if (and (symbolp term)
 
675
               (equal (symbol-name term) symbol-name))
 
676
          replacement
 
677
        term)
 
678
    (cons (standardize-to-package symbol-name replacement (car term))
 
679
          (standardize-to-package symbol-name replacement (cdr term)))))
 
680
 
 
681
 
 
682
(defun quantify-simple-predicate (predicate in-package
 
683
                                  set-guard list-guard arg-guard)
 
684
  (declare (xargs :guard (symbolp in-package)
 
685
                  :mode :program))
 
686
  (let* ((name          (car predicate))
 
687
         (args          (cons '?x (cddr predicate)))
 
688
         (wrap          (app "<" (app (symbol-name name) ">")))
 
689
         (not-wrap      (app "<" (app "not-" (app (symbol-name name) ">"))))
 
690
 
 
691
         ;; First we build up all the symbols that we will use.
 
692
 
 
693
         (all<p>             (mksym (app "all" wrap) in-package))
 
694
         (exists<p>          (mksym (app "exists" wrap) in-package))
 
695
         (find<p>            (mksym (app "find" wrap) in-package))
 
696
         (filter<p>          (mksym (app "filter" wrap) in-package))
 
697
         (all<not-p>         (mksym (app "all" not-wrap) in-package))
 
698
         (exists<not-p>      (mksym (app "exists" not-wrap) in-package))
 
699
         (find<not-p>        (mksym (app "find" not-wrap) in-package))
 
700
         (filter<not-p>      (mksym (app "filter" not-wrap) in-package))
 
701
         (all-list<p>        (mksym (app "all-list" wrap) in-package))
 
702
         (exists-list<p>     (mksym (app "exists-list" wrap) in-package))
 
703
         (find-list<p>       (mksym (app "find-list" wrap) in-package))
 
704
         (filter-list<p>     (mksym (app "filter-list" wrap) in-package))
 
705
         (all-list<not-p>    (mksym (app "all-list" not-wrap) in-package))
 
706
         (exists-list<not-p> (mksym (app "exists-list" not-wrap) in-package))
 
707
         (find-list<not-p>   (mksym (app "find-list" not-wrap) in-package))
 
708
         (filter-list<not-p> (mksym (app "filter-list" not-wrap) in-package))
 
709
 
 
710
         ;; And we create a substitution list, to instantiate the
 
711
         ;; generic theory/functions with their new, concrete values.
 
712
 
 
713
         (subs `(((predicate ?x)        (,name ,@args))
 
714
                 ((all ?x)              (,all<p> ,@args))
 
715
                 ((exists ?x)           (,exists<p> ,@args))
 
716
                 ((find ?x)             (,find<p> ,@args))
 
717
                 ((filter ?x)           (,filter<p> ,@args))
 
718
                 ((all<not> ?x)         (,all<not-p> ,@args))
 
719
                 ((exists<not> ?x)      (,exists<not-p> ,@args))
 
720
                 ((find<not> ?x)        (,find<not-p> ,@args))
 
721
                 ((filter<not> ?x)      (,filter<not-p> ,@args))
 
722
                 ((all-list ?x)         (,all-list<p> ,@args))
 
723
                 ((exists-list ?x)      (,exists-list<p> ,@args))
 
724
                 ((find-list ?x)        (,find-list<p> ,@args))
 
725
                 ((filter-list ?x)      (,filter-list<p> ,@args))
 
726
                 ((all-list<not> ?x)    (,all-list<not-p> ,@args))
 
727
                 ((exists-list<not> ?x) (,exists-list<not-p> ,@args))
 
728
                 ((find-list<not> ?x)   (,find-list<not-p> ,@args))
 
729
                 ((filter-list<not> ?x) (,filter-list<not-p> ,@args))))
 
730
 
 
731
         ;; We use this hack to support alternate guards.  We
 
732
         ;; basically use our rewriter to inject the extra guards into
 
733
         ;; the function's existing guards.
 
734
 
 
735
         (fn-subs
 
736
          (list* `((declare (xargs :guard (true-listp ?list)))
 
737
                   (declare (xargs :guard (and (true-listp ?list)
 
738
                                               ,@list-guard
 
739
                                               ,@arg-guard))))
 
740
                 `((declare (xargs :guard (setp ?set)))
 
741
                   (declare (xargs :guard (and (setp ?set)
 
742
                                               ,@set-guard
 
743
                                               ,@arg-guard))))
 
744
                 subs))
 
745
 
 
746
 
 
747
         ;; And we make some symbols for use in automating the all-by-membership
 
748
         ;; strategy with computed hints.
 
749
 
 
750
         (all-trigger<p>           (mksym (app "all-trigger" wrap) in-package))
 
751
         (all-trigger<not-p>       (mksym (app "all-trigger" not-wrap) in-package))
 
752
         (all-strategy<p>          (mksym (app "all-strategy" wrap) in-package))
 
753
         (all-strategy<not-p>      (mksym (app "all-strategy" not-wrap) in-package))
 
754
         (all-list-trigger<p>      (mksym (app "all-list-trigger" wrap) in-package))
 
755
         (all-list-trigger<not-p>  (mksym (app "all-list-trigger" not-wrap) in-package))
 
756
         (all-list-strategy<p>     (mksym (app "all-list-strategy" wrap) in-package))
 
757
         (all-list-strategy<not-p> (mksym (app "all-list-strategy" not-wrap) in-package))
 
758
 
 
759
         ;; We finally make a deftheory event with the following name, which
 
760
         ;; holds all of these theorems:
 
761
 
 
762
         (theory<p>         (mksym (app "theory" wrap) in-package))
 
763
         (suffix            (mksym wrap in-package))
 
764
         (thm-names         (append (INSTANCE::defthm-names *theorems*)
 
765
                                    (INSTANCE::defthm-names *final-theorems*)))
 
766
         (thm-name-map      (INSTANCE::create-new-names thm-names suffix))
 
767
         (theory<p>-defthms (sublis thm-name-map thm-names))
 
768
 
 
769
         )
 
770
 
 
771
    `(encapsulate ()
 
772
 
 
773
        ;; It's now quite easy to instantiate all of our functions.
 
774
 
 
775
        (instance-*functions*
 
776
         :subs ,fn-subs
 
777
         :suffix ,name)
 
778
 
 
779
        ;; And similarly we can instantiate all of the theorems.
 
780
 
 
781
        (instance-*theorems*
 
782
         :subs ,subs
 
783
         :suffix ,(mksym wrap in-package))
 
784
         ;:extra-defs (empty))
 
785
 
 
786
 
 
787
        ;; Automating the computed hints is a pain in the ass.  We
 
788
        ;; first need triggers as aliases for all<p>, all<not-p>, etc.
 
789
 
 
790
        (defund ,all-trigger<p> (,@args)
 
791
          (declare (xargs :verify-guards nil))
 
792
          (,all<p> ,@args))
 
793
 
 
794
        (defund ,all-trigger<not-p> (,@args)
 
795
          (declare (xargs :verify-guards nil))
 
796
          (,all<not-p> ,@args))
 
797
 
 
798
        (defund ,all-list-trigger<p> (,@args)
 
799
          (declare (xargs :verify-guards nil))
 
800
          (,all-list<p> ,@args))
 
801
 
 
802
        (defund ,all-list-trigger<not-p> (,@args)
 
803
          (declare (xargs :verify-guards nil))
 
804
          (,all-list<not-p> ,@args))
 
805
 
 
806
 
 
807
        ;; Now we need "tagging theorems" that instruct the rewriter
 
808
        ;; to tag the appropriate terms.
 
809
 
 
810
        (defthm ,all-strategy<p>
 
811
          (implies (and (syntaxp (rewriting-goal-lit mfc state))
 
812
                        (syntaxp (rewriting-conc-lit (list ',all<p> ,@args)
 
813
                                  mfc state)))
 
814
                   (equal (,all<p> ,@args)
 
815
                          (,all-trigger<p> ,@args)))
 
816
          :hints(("Goal"
 
817
                  :in-theory (union-theories
 
818
                              (theory 'minimal-theory)
 
819
                              '((:definition ,all-trigger<p>))))))
 
820
 
 
821
        (defthm ,all-strategy<not-p>
 
822
          (implies (and (syntaxp (rewriting-goal-lit mfc state))
 
823
                        (syntaxp (rewriting-conc-lit (list ',all<not-p> ,@args)
 
824
                                  mfc state)))
 
825
                   (equal (,all<not-p> ,@args)
 
826
                          (,all-trigger<not-p> ,@args)))
 
827
          :hints(("Goal"
 
828
                  :in-theory (union-theories
 
829
                              (theory 'minimal-theory)
 
830
                              '((:definition ,all-trigger<not-p>))))))
 
831
 
 
832
        (defthm ,all-list-strategy<p>
 
833
          (implies (and (syntaxp (rewriting-goal-lit mfc state))
 
834
                        (syntaxp (rewriting-conc-lit (list ',all-list<p> ,@args)
 
835
                                  mfc state)))
 
836
                   (equal (,all-list<p> ,@args)
 
837
                          (,all-list-trigger<p> ,@args)))
 
838
          :hints(("Goal"
 
839
                  :in-theory (union-theories
 
840
                              (theory 'minimal-theory)
 
841
                              '((:definition ,all-list-trigger<p>))))))
 
842
 
 
843
        (defthm ,all-list-strategy<not-p>
 
844
          (implies (and (syntaxp (rewriting-goal-lit mfc state))
 
845
                        (syntaxp (rewriting-conc-lit (list ',all-list<not-p> ,@args)
 
846
                                  mfc state)))
 
847
                   (equal (,all-list<not-p> ,@args)
 
848
                          (,all-list-trigger<not-p> ,@args)))
 
849
          :hints(("Goal"
 
850
                  :in-theory (union-theories
 
851
                              (theory 'minimal-theory)
 
852
                              '((:definition ,all-list-trigger<not-p>))))))
 
853
 
 
854
 
 
855
        ;; And then we call upon our computed hints routines to generate a
 
856
        ;; computed hint for us to use, and add it to the default hints.
 
857
 
 
858
        (COMPUTED-HINTS::automate-instantiation
 
859
          :new-hint-name ,(mksym (app "all-by-membership-hint" wrap) in-package)
 
860
          :generic-theorem all-by-membership
 
861
          :generic-predicate predicate
 
862
          :generic-hyps all-hyps
 
863
          :generic-collection all-set
 
864
          :generic-collection-predicate all
 
865
          :actual-collection-predicate ,all<p>
 
866
          :actual-trigger ,all-trigger<p>
 
867
          :predicate-rewrite (((predicate ,@(?ify args))
 
868
                               (,name ,@(?ify args))))
 
869
          :tagging-theorem ,all-strategy<p>
 
870
        )
 
871
 
 
872
        (COMPUTED-HINTS::automate-instantiation
 
873
          :new-hint-name ,(mksym (app "all-by-membership-hint" not-wrap) in-package)
 
874
          :generic-theorem all-by-membership
 
875
          :generic-predicate predicate
 
876
          :generic-hyps all-hyps
 
877
          :generic-collection all-set
 
878
          :generic-collection-predicate all
 
879
          :actual-collection-predicate ,all<not-p>
 
880
          :actual-trigger ,all-trigger<not-p>
 
881
          :predicate-rewrite (((predicate ,@(?ify args))
 
882
                               (not (,name ,@(?ify args)))))
 
883
          :tagging-theorem ,all-strategy<not-p>
 
884
        )
 
885
 
 
886
        (COMPUTED-HINTS::automate-instantiation
 
887
          :new-hint-name ,(mksym (app "all-list-by-membership-hint" wrap) in-package)
 
888
          :generic-theorem all-list-by-membership
 
889
          :generic-predicate predicate
 
890
          :generic-hyps all-list-hyps
 
891
          :generic-collection all-list-list
 
892
          :generic-collection-predicate all-list
 
893
          :actual-collection-predicate ,all-list<p>
 
894
          :actual-trigger ,all-list-trigger<p>
 
895
          :predicate-rewrite (((predicate ,@(?ify args))
 
896
                               (,name ,@(?ify args))))
 
897
          :tagging-theorem ,all-list-strategy<p>
 
898
        )
 
899
 
 
900
        (COMPUTED-HINTS::automate-instantiation
 
901
          :new-hint-name ,(mksym (app "all-list-by-membership-hint" not-wrap) in-package)
 
902
          :generic-theorem all-list-by-membership
 
903
          :generic-predicate predicate
 
904
          :generic-hyps all-list-hyps
 
905
          :generic-collection all-list-list
 
906
          :generic-collection-predicate all-list
 
907
          :actual-collection-predicate ,all-list<not-p>
 
908
          :actual-trigger ,all-list-trigger<not-p>
 
909
          :predicate-rewrite (((predicate ,@(?ify args))
 
910
                               (not (,name ,@(?ify args)))))
 
911
          :tagging-theorem ,all-list-strategy<not-p>
 
912
        )
 
913
 
 
914
 
 
915
        (instance-*final-theorems*
 
916
         :subs ,subs
 
917
         :suffix ,(mksym wrap in-package))
 
918
         ;:extra-defs (empty))
 
919
 
 
920
 
 
921
        (verify-guards ,filter<p>)
 
922
        (verify-guards ,filter<not-p>)
 
923
 
 
924
        ;; In the end, we want to create a deftheory event so that you can
 
925
        ;; easily turn off the reasoning about these functions when you
 
926
        ;; don't need it.  We do that with the following event:
 
927
 
 
928
        (deftheory ,theory<p> '(,@theory<p>-defthms
 
929
                                ,all<p>              ,all-list<p>
 
930
                                ,exists<p>           ,exists-list<p>
 
931
                                ,find<p>             ,find-list<p>
 
932
                                ,filter<p>           ,filter-list<p>
 
933
                                ,all<not-p>          ,all-list<not-p>
 
934
                                ,exists<not-p>       ,exists-list<not-p>
 
935
                                ,find<not-p>         ,find-list<not-p>
 
936
                                ,filter<not-p>       ,filter-list<not-p>
 
937
                                ,all-trigger<p>      ,all-list-trigger<p>
 
938
                                ,all-trigger<not-p>  ,all-list-trigger<not-p>
 
939
                                ,all-strategy<p>     ,all-list-strategy<p>
 
940
                                ,all-strategy<not-p> ,all-list-strategy<not-p>
 
941
                                ))
 
942
        )))
 
943
 
 
944
 
 
945
(defmacro quantify-predicate (predicate
 
946
                              &key in-package-of
 
947
                                   set-guard list-guard arg-guard)
 
948
  (quantify-simple-predicate predicate
 
949
                             (if in-package-of in-package-of 'in)
 
950
                             (standardize-to-package "?SET" '?set set-guard)
 
951
                             (standardize-to-package "?LIST" '?list list-guard)
 
952
                             arg-guard))
 
953
 
 
954
 
 
955
 
 
956
; We don't want to keep all these generic theorems around, because
 
957
; many of them are rewrite rules with targets that are actual
 
958
; functions.  For example, if a rule concludes with (in a X), we don't
 
959
; want to start backchaining on it if its hypothese include generic
 
960
; rules.
 
961
 
 
962
(deftheory generic-quantification-theory
 
963
  `(,@(INSTANCE::defthm-names *theorems*)
 
964
    ,@(INSTANCE::defthm-names *final-theorems*)
 
965
    all exists find filter
 
966
    all-list exists-list find-list filter-list
 
967
    all<not> exists<not> find<not> filter<not>
 
968
    all-list<not> exists-list<not> find-list<not> filter-list<not>))
 
969
 
 
970
(in-theory (disable generic-quantification-theory))