← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/std/util/deflist.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/std/util/deflist.lisp
34
34
; Kookamara LLC, which is also available under an MIT/X11 style license.
35
35
 
36
36
(in-package "STD")
37
 
(include-book "xdoc/top" :dir :system)
38
 
(include-book "tools/bstar" :dir :system)
39
 
(include-book "std/osets/top" :dir :system)
 
37
(include-book "deflist-base")
 
38
(include-book "std/osets/element-list" :dir :system)
40
39
(include-book "defsort/duplicated-members" :dir :system)
41
40
(include-book "std/lists/sets" :dir :system)
42
41
(include-book "std/lists/list-fix" :dir :system)
43
42
(include-book "std/lists/take" :dir :system)
44
43
(include-book "std/lists/repeat" :dir :system)
45
44
(include-book "std/lists/rev" :dir :system)
46
 
(include-book "maybe-defthm")
47
 
(include-book "support")
48
 
(set-state-ok t)
49
 
 
50
 
(defxdoc deflist
51
 
  :parents (std/util)
52
 
  :short "Introduce a recognizer for a typed list."
53
 
 
54
 
  :long "<p>Deflist lets you to quickly introduce recognizers for typed lists
55
 
like @(see nat-listp).  It defines the new recognizer function, sets up a basic
56
 
theory with rules about @(see len), @(see append), @(see member), etc., and
57
 
generates basic, automatic @(see xdoc) documentation.</p>
58
 
 
59
 
<h4>General Form</h4>
60
 
 
61
 
@({
62
 
 (deflist name formals
63
 
   element
64
 
   [keyword options]
65
 
   [/// other events]
66
 
   )
67
 
 
68
 
 Options                  Defaults
69
 
   :negatedp                nil
70
 
   :true-listp              nil
71
 
   :elementp-of-nil         :unknown
72
 
   :guard                   t
73
 
   :verify-guards           t
74
 
   :guard-hints             nil
75
 
   :guard-debug             nil
76
 
   :mode                    current defun-mode
77
 
   :verbosep                nil
78
 
   :parents                 nil
79
 
   :short                   nil
80
 
   :long                    nil
81
 
})
82
 
 
83
 
<h4>Basic Examples</h4>
84
 
 
85
 
<p>The following introduces a new function, @('my-integer-listp'), which
86
 
recognizes lists whose every element satisfies @('integerp'), and also
87
 
introduces many theorems about this new function.</p>
88
 
 
89
 
@({
90
 
 (deflist my-integer-listp (x)
91
 
   (integerp x))
92
 
})
93
 
 
94
 
<p><b><color rgb='#ff0000'>Note</color></b>: @('x') is treated in a special
95
 
way.  It refers to the whole list in formals and guards, but refers to
96
 
individual elements of the list in the @('element') portion.  This is similar
97
 
to how other macros like @(see defalist), @(see defprojection), and @(see
98
 
defmapappend) handle @('x').</p>
99
 
 
100
 
<p>Here is a recognizer for lists with no natural numbers:</p>
101
 
 
102
 
@({
103
 
 (deflist nat-free-listp (x)
104
 
   (natp x)
105
 
   :negatedp t)
106
 
})
107
 
 
108
 
<p>Here is a recognizer for lists whose elements must exceed some minimum:</p>
109
 
 
110
 
@({
111
 
 (deflist all-greaterp (min x)
112
 
   (> x min)
113
 
   :guard (and (natp min)
114
 
               (nat-listp x)))
115
 
})
116
 
 
117
 
<h3>Usage and Optional Arguments</h3>
118
 
 
119
 
<p>Let @('pkg') be the package of @('name').  All functions, theorems, and
120
 
variables are created in this package.  One of the formals must be @('pkg::x'),
121
 
and this argument represents the list to check.  Otherwise, the only
122
 
restriction on the formals is that you may not use the names @('pkg::a'),
123
 
@('pkg::n'), or @('pkg::y'), because we use these variables in the theorems we
124
 
generate.</p>
125
 
 
126
 
<p>The optional @(':negatedp') keyword can be used to recognize a list whose
127
 
every element does not satisfy elementp.</p>
128
 
 
129
 
<p>The optional @(':true-listp') keyword can be used to require that the new
130
 
recognizer is \"strict\" and will only accept lists that are
131
 
@('nil')-terminated; by default the recognizer will be \"loose\" and will not
132
 
pay attention to the final @('cdr').  There are various reasons to prefer one
133
 
behavior or another; see @(see strict-list-recognizers) for details.</p>
134
 
 
135
 
<p>The optional @(':elementp-of-nil') keyword can be used when @('(elementp nil
136
 
...)') is always known to be @('t') or @('nil').  When it is provided,
137
 
@('deflist') can generate slightly better theorems.</p>
138
 
 
139
 
<p>The optional @(':guard'), @(':verify-guards'), @(':guard-debug'), and
140
 
@(':guard-hints') are options for the @(see defun) we introduce.  These are for
141
 
the guards of the new list recognizer, not the element recognizer.</p>
142
 
 
143
 
<p>The optional @(':mode') keyword can be set to @(':logic') or @(':program')
144
 
to introduce the recognizer in logic or program mode.  The default is whatever
145
 
the current default defun-mode is for ACL2, i.e., if you are already in program
146
 
mode, it will default to program mode, etc.</p>
147
 
 
148
 
<p>The optional @(':verbosep') flag can be set to @('t') if you want deflist to
149
 
print everything it's doing.  This may be useful if you run into any failures,
150
 
or if you are simply curious about what is being introduced.</p>
151
 
 
152
 
<p>The optional @(':parents'), @(':short'), and @(':long') keywords are as in
153
 
@(see defxdoc).  Typically you only need to specify @(':parents'), perhaps
154
 
implicitly with @(see xdoc::set-default-parents), and suitable documentation
155
 
will be automatically generated for @(':short') and @(':long').  If you don't
156
 
like this documentation, you can supply your own @(':short') and/or @(':long')
157
 
to override it.</p>
158
 
 
159
 
<h3>Support for Other Events</h3>
160
 
 
161
 
<p>Deflist implements the same @('///') syntax as other macros like @(see
162
 
define).  This allows you to put related events near the definition and have
163
 
them included in the automatic documentation.  As with define, the new
164
 
recognizer is enabled during the @('///') section.  Here is an example:</p>
165
 
 
166
 
@({
167
 
 (deflist even-integer-list-p (x)
168
 
   (even-integer-p x)
169
 
   :true-listp t
170
 
   ///
171
 
   (defthm integer-listp-when-even-integer-list-p
172
 
     (implies (even-integer-list-p x)
173
 
              (integer-listp x))))
174
 
})
175
 
 
176
 
<p>Deprecated.  The optional @(':rest') keyword was a precursor to @('///').
177
 
It is still implemented, but its use is now discouraged.  If both @(':rest')
178
 
and @('///') events are used, we arbitrarily put the @(':rest') events
179
 
first.</p>
180
 
 
181
 
<p>Deprecated.  The optional @(':already-definedp') keyword can be set if you
182
 
have already defined the function.  This was previously useful when you wanted
183
 
to generate the ordinary @('deflist') theorems without generating a @('defund')
184
 
event, e.g., because you are dealing with mutually recursive recognizers.  We
185
 
still accept this option for backwards compatibility but it is useless, because
186
 
@('deflist') is now smart enough to notice that the function is already
187
 
defined.</p>")
188
 
 
189
 
(defxdoc strict-list-recognizers
190
 
  :parents (deflist)
191
 
  :short "Should your list recognizers require @('nil')-terminated lists?"
192
 
 
193
 
  :long "<p>Here are two ways that you could write a list recognizer:</p>
194
 
 
195
 
<p>The \"strict\" way:</p>
196
 
 
197
 
@({
198
 
   (defun foo-listp (x)
199
 
     (if (atom x)
200
 
         (not x)
201
 
       (and (foop (car x))
202
 
            (foo-listp (cdr x)))))
203
 
})
204
 
 
205
 
<p>The \"loose\" way:</p>
206
 
 
207
 
@({
208
 
   (defun foo-listp (x)
209
 
     (if (atom x)
210
 
         t
211
 
       (and (foop (car x))
212
 
            (foo-listp (cdr x)))))
213
 
})
214
 
 
215
 
<p>The only difference is that in the base case, the strict recognizer requires
216
 
X to be NIL, whereas the loose recognizer allows X to be any atom.</p>
217
 
 
218
 
<p>By default, the recognizers introduced by @(see deflist) follow the loose
219
 
approach.  You can use the @(':true-listp') option to change this behavior, and
220
 
instead introduce a strict recognizer.</p>
221
 
 
222
 
<p>Why in the world would we use a loose recognizer?  Well, there are
223
 
advantages to either approach.</p>
224
 
 
225
 
<p>The strict approach is certainly more clear and less weird.  It is nice that
226
 
a strict recognizer always implies @(see true-listp).  And it makes EQUAL more
227
 
meaningful when applied to FOO-LISTP objects.</p>
228
 
 
229
 
<p>That is, when FOO-LISTP is strict, there is only one FOO-LISTP that has
230
 
length 3 and whose first three elements are (A B C).  However, when FOO-LISTP
231
 
is loose, there are infinitely many lists like this, and the only difference
232
 
between them is their final cdr.</p>
233
 
 
234
 
<p>This nicer equality behavior makes the strict approach especially appealing
235
 
when you are building new data types that include FOO-LISTP components, and
236
 
you'd like to just reuse EQUAL instead of having new equivalence relations for
237
 
each structure.</p>
238
 
 
239
 
<p>But the loose approach more nicely follows the @(see list-fix) convention:
240
 
\"a function that takes a list as an argument should coerce the final-cdr to
241
 
NIL, and produce the same result regardless of the final cdr.\" More formally,
242
 
you might say that F respects the list-fix convention when you can prove</p>
243
 
 
244
 
@({
245
 
   (defcong list-equiv equal (f ... x ...) n)
246
 
})
247
 
 
248
 
<p>Where list-equiv is equality up to the final cdr, e.g.,</p>
249
 
 
250
 
@({
251
 
   (list-equiv x y) = (equal (list-fix x) (list-fix y))
252
 
})
253
 
 
254
 
<p>Many functions follow this convention or something similar to it, and
255
 
because of this there are sometimes nicer theorems about loose list recognizers
256
 
than about strict list recognizers.  For instance, consider @(see append).  In
257
 
the loose style, we can prove:</p>
258
 
 
259
 
@({
260
 
   (equal (foo-listp (append x y))
261
 
          (and (foo-listp x)
262
 
               (foo-listp y)))
263
 
})
264
 
 
265
 
<p>In the strict style, we have to prove something uglier, e.g.,</p>
266
 
 
267
 
@({
268
 
   (equal (foo-listp (append x y))
269
 
          (and (foo-listp (list-fix x))
270
 
               (foo-listp y)))
271
 
})
272
 
 
273
 
<p>There are many other nice theorems, but just as a few examples, each of
274
 
these theorems are very nice in the loose style, and are uglier in the strict
275
 
style:</p>
276
 
 
277
 
@({
278
 
   (equal (foo-listp (list-fix x))
279
 
          (foo-listp x))
280
 
 
281
 
   (equal (foo-listp (rev x))
282
 
          (foo-listp x))
283
 
 
284
 
   (equal (foo-listp (mergesort x))
285
 
          (foo-listp x))
286
 
 
287
 
   (implies (and (subsetp-equal x y)
288
 
                 (foo-listp y))
289
 
            (foo-listp x))
290
 
})
291
 
 
292
 
<p>@(see deflist) originally came out of <a
293
 
href='http://www.cs.utexas.edu/users/jared/milawa/Web/'>Milawa</a>, where I
294
 
universally applied the loose approach, and in that context I think it is very
295
 
nice.  It's not entirely clear that loose recognizers are a good fit for ACL2.
296
 
Really one of the main objections to the loose style is: ACL2's built-in list
297
 
recognizers use the strict approach, and it can become irritating to keep track
298
 
of which recognizers require true-listp and which don't.</p>")
 
45
(local
 
46
 (progn
 
47
   (include-book "std/lists/nth" :dir :system)
 
48
   (include-book "std/lists/update-nth" :dir :system)
 
49
   (include-book "std/lists/butlast" :dir :system)
 
50
   (include-book "std/lists/nthcdr" :dir :system)
 
51
   (include-book "std/lists/append" :dir :system)
 
52
   (include-book "std/lists/last" :dir :system)
 
53
   (include-book "std/lists/rcons" :dir :system)
 
54
   (include-book "std/lists/remove" :dir :system)
 
55
   (include-book "std/lists/revappend" :dir :system)
 
56
   (include-book "defredundant")))
 
57
 
 
58
 
 
59
;; Harvest the listp rules from the above books by non-locally setting the
 
60
;; listp-rules table to its (local) value.  Redundantly define the theorems
 
61
;; referenced by the table.
 
62
(make-event
 
63
 (let ((tab (table-alist 'acl2::listp-rules (w state))))
 
64
   `(table acl2::listp-rules nil ',tab :clear)))
 
65
 
 
66
(make-event
 
67
 (defredundant-fn (strip-cars (table-alist 'acl2::listp-rules (w state))) nil state))
 
68
 
299
69
 
300
70
(defsection deflist-lemmas
301
71
 
317
87
         (subsetp-equal (intersection-equal x y) y)))
318
88
 
319
89
  (defthmd deflist-lemma-subsetp-equal-of-duplicated-members
320
 
    (subsetp-equal (duplicated-members x) x))
 
90
    (subsetp-equal (duplicated-members x) x)
 
91
    :hints(("Goal" :in-theory (enable acl2::duplicity)))
 
92
    :otf-flg t)
321
93
 
322
94
  (defthmd deflist-lemma-subsetp-of-nthcdr
323
95
    (subsetp-equal (nthcdr n x) x))
428
200
         (subsetp-equal (union x y) (append (sfix x) (sfix y))))))
429
201
 
430
202
 
431
 
 
432
203
(deftheory deflist-support-lemmas
433
204
  '((:type-prescription intersection-equal)
434
205
    (:type-prescription set-difference-equal)
487
258
    acl2::list-fix-under-list-equiv
488
259
    set::mergesort-under-set-equiv
489
260
    acl2::binary-append-without-guard))
490
 
 
491
 
 
492
 
(defconst *deflist-valid-keywords*
493
 
  '(:negatedp
494
 
    :guard
495
 
    :verify-guards
496
 
    :guard-debug
497
 
    :guard-hints
498
 
    :already-definedp
499
 
    :elementp-of-nil
500
 
    :mode
501
 
    :parents
502
 
    :short
503
 
    :long
504
 
    :true-listp
505
 
    :rest
506
 
    :verbosep
507
 
    ;; Undocumented option for customizing the theory, mainly meant for
508
 
    ;; problematic cases, e.g., built-in functions where ACL2 "knows too much"
509
 
    :theory-hack))
510
 
 
511
 
(defun deflist-fn (name formals element kwd-alist other-events state)
512
 
  (declare (xargs :mode :program))
513
 
  (b* ((__function__ 'deflist)
514
 
       (mksym-package-symbol name)
515
 
 
516
 
       ;; Special variables that are reserved by deflist.
517
 
       (x (intern-in-package-of-symbol "X" name))
518
 
       (a (intern-in-package-of-symbol "A" name))
519
 
       (n (intern-in-package-of-symbol "N" name))
520
 
       (y (intern-in-package-of-symbol "Y" name))
521
 
 
522
 
       ((unless (and (symbol-listp formals)
523
 
                     (no-duplicatesp formals)))
524
 
        (raise "The formals must be a list of unique symbols, but are ~x0."
525
 
               formals))
526
 
       ((unless (member x formals))
527
 
        (raise "The formals must contain ~x0, but are ~x1.~%" x formals))
528
 
       ((unless (and (not (member a formals))
529
 
                     (not (member n formals))
530
 
                     (not (member y formals))))
531
 
        (raise "As a special restriction, formals may not mention ~x0, ~x1, ~
532
 
                or ~x2, but the formals are ~x3." a n y formals))
533
 
       ((unless (and (consp element)
534
 
                     (symbolp (car element))))
535
 
        (raise "The element recognizer must be a function applied to the ~
536
 
                formals, but is ~x0." element))
537
 
 
538
 
       (elementp     (car element))
539
 
       (elem-formals (cdr element))
540
 
 
541
 
       ;; We previously required the user to tell us if the function was
542
 
       ;; already defined.  Now we---you know---actually look to see.  Duh.
543
 
       (looks-already-defined-p
544
 
        (or (not (eq (getprop name 'acl2::formals :none 'acl2::current-acl2-world
545
 
                              (w state))
546
 
                     :none))
547
 
            (not (eq (getprop name 'acl2::macro-args :none 'acl2::current-acl2-world
548
 
                              (w state))
549
 
                     :none))))
550
 
       (already-definedp (getarg :already-definedp :unknown kwd-alist))
551
 
       ((unless (or (eq already-definedp :unknown)
552
 
                    (eq already-definedp looks-already-defined-p)))
553
 
        (raise "Found :already-definedp ~x0, but ~x1 is ~s2."
554
 
               already-definedp name
555
 
               (if looks-already-defined-p
556
 
                   "already defined."
557
 
                 "not defined.")))
558
 
       (already-definedp looks-already-defined-p)
559
 
 
560
 
       (negatedp         (getarg :negatedp         nil      kwd-alist))
561
 
       (true-listp       (getarg :true-listp       nil      kwd-alist))
562
 
       (verify-guards    (getarg :verify-guards    t        kwd-alist))
563
 
       (guard            (getarg :guard            t        kwd-alist))
564
 
       (guard-debug      (getarg :guard-debug      nil      kwd-alist))
565
 
       (guard-hints      (getarg :guard-hints      nil      kwd-alist))
566
 
 
567
 
       (elementp-of-nil  (getarg :elementp-of-nil  :unknown kwd-alist))
568
 
       (short            (getarg :short            nil      kwd-alist))
569
 
       (long             (getarg :long             nil      kwd-alist))
570
 
       (theory-hack      (getarg :theory-hack      nil      kwd-alist))
571
 
 
572
 
 
573
 
 
574
 
       (rest             (append
575
 
                          (getarg :rest nil kwd-alist)
576
 
                          other-events))
577
 
 
578
 
       (mode             (getarg :mode
579
 
                                 (default-defun-mode (w state))
580
 
                                 kwd-alist))
581
 
 
582
 
       (parents-p (assoc :parents kwd-alist))
583
 
       (parents   (cdr parents-p))
584
 
       (parents   (if parents-p
585
 
                      parents
586
 
                    (or (xdoc::get-default-parents (w state))
587
 
                        '(acl2::undocumented))))
588
 
 
589
 
       ((unless (booleanp negatedp))
590
 
        (raise ":negatedp must be a boolean, but is ~x0." negatedp))
591
 
       ((unless (booleanp true-listp))
592
 
        (raise ":true-listp must be a boolean, but is ~x0." true-listp))
593
 
       ((unless (booleanp verify-guards))
594
 
        (raise ":verify-guards must be a boolean, but is ~x0." verify-guards))
595
 
       ((unless (or (eq mode :logic)
596
 
                    (eq mode :program)))
597
 
        (raise ":mode must be one of :logic or :program, but is ~x0." mode))
598
 
       ((unless (or (eq mode :logic)
599
 
                    (not already-definedp)))
600
 
        (raise ":mode :program and already-definedp cannot be used together."))
601
 
       ((unless (member elementp-of-nil '(t nil :unknown)))
602
 
        (raise ":elementp-of-nil must be t, nil, or :unknown"))
603
 
 
604
 
       (short (or short
605
 
                  (and parents
606
 
                       (concatenate
607
 
                        'string "@(call " (xdoc::full-escape-symbol name)
608
 
                                 ") recognizes lists where every element "
609
 
                                 (if negatedp
610
 
                                     "is rejected by "
611
 
                                   "satisfies ")
612
 
                                 ;; bozo it'd be better to put the formals in
613
 
                                 ;; here, for multi-arity functions.
614
 
                                 "@(see? " (xdoc::full-escape-symbol elementp) ")."))))
615
 
 
616
 
       (long (or long
617
 
                 (and parents
618
 
                      (if true-listp
619
 
                          "<p>This is an ordinary @(see std::deflist).  It is
620
 
                           \"strict\" in that it requires @('x') to be a
621
 
                           \"properly\" nil-terminated list.</p>"
622
 
                        "<p>This is an ordinary @(see std::deflist).  It is
623
 
                         \"loose\" in that it does not care whether @('x') is
624
 
                         nil-terminated.</p>"))))
625
 
 
626
 
       (def (if already-definedp
627
 
                nil
628
 
              `((defund ,name (,@formals)
629
 
                  (declare (xargs :guard ,guard
630
 
                                  ;; We tell ACL2 not to normalize because
631
 
                                  ;; otherwise type reasoning can rewrite the
632
 
                                  ;; definition, and ruin some of our theorems
633
 
                                  ;; below, e.g., when ELEMENTP is known to
634
 
                                  ;; always be true.
635
 
                                  :normalize nil
636
 
                                  ,@(and (eq mode :logic)
637
 
                                         `(:verify-guards ,verify-guards
638
 
                                           :guard-debug   ,guard-debug
639
 
                                           :guard-hints   ,guard-hints))))
640
 
                  (if (consp ,x)
641
 
                      (and ,(if negatedp
642
 
                                `(not (,elementp ,@(subst `(car ,x) x elem-formals)))
643
 
                              `(,elementp ,@(subst `(car ,x) x elem-formals)))
644
 
                           (,name ,@(subst `(cdr ,x) x formals)))
645
 
                    ,(if true-listp
646
 
                         `(null ,x)
647
 
                       t))))))
648
 
 
649
 
       ((when (eq mode :program))
650
 
        `(defsection ,name
651
 
           ,@(and parents `(:parents ,parents))
652
 
           ,@(and short   `(:short ,short))
653
 
           ,@(and long    `(:long ,long))
654
 
           (program)
655
 
           ,@def
656
 
           ,@rest))
657
 
 
658
 
       (events
659
 
        `((logic)
660
 
          (set-inhibit-warnings ;; implicitly local
661
 
           "theory" "free" "non-rec" "double-rewrite" "subsume" "disable")
662
 
 
663
 
          (value-triple
664
 
           (cw "~|~%Deflist: attempting to show, using your current theory, ~
665
 
                that ~x0 is always Boolean valued.~%" ',element))
666
 
 
667
 
          (with-output
668
 
            :stack :pop
669
 
            :off (acl2::summary acl2::observation)
670
 
            (local (defthm deflist-local-booleanp-element-thm
671
 
                     (or (equal ,element t)
672
 
                         (equal ,element nil))
673
 
                     :rule-classes :type-prescription)))
674
 
 
675
 
          ,@(and (not (eq elementp-of-nil  :unknown))
676
 
                 `((value-triple
677
 
                    (cw "~|~%Deflist: attempting to justify, using your ~
678
 
                         current theory, :ELEMENTP-OF-NIL ~x0.~%"
679
 
                        ',elementp-of-nil))
680
 
 
681
 
                   (with-output
682
 
                     :stack :pop
683
 
                     :off (acl2::summary)
684
 
                     (local (maybe-defthm-as-rewrite
685
 
                             deflist-local-elementp-of-nil-thm
686
 
                             (equal (,elementp ,@(subst ''nil x elem-formals))
687
 
                                    ',elementp-of-nil))))))
688
 
 
689
 
          (value-triple
690
 
           (cw "~|~%Deflist: introducing ~x0 and proving deflist theorems.~%"
691
 
               ',name))
692
 
 
693
 
          ,@def
694
 
 
695
 
          (local (in-theory (theory 'minimal-theory)))
696
 
          (local (in-theory (enable deflist-support-lemmas
697
 
                                    ,name
698
 
                                    (:type-prescription ,name)
699
 
                                    deflist-local-booleanp-element-thm
700
 
                                    )))
701
 
          (local (enable-if-theorem deflist-local-elementp-of-nil-thm))
702
 
          ,@theory-hack
703
 
 
704
 
          (defthm ,(mksym name '-when-not-consp)
705
 
            (implies (not (consp ,x))
706
 
                     (equal (,name ,@formals)
707
 
                            ,(if true-listp
708
 
                                 `(not ,x)
709
 
                               t)))
710
 
            :hints(("Goal" :in-theory (enable ,name))))
711
 
 
712
 
          (defthm ,(mksym name '-of-cons)
713
 
            (equal (,name ,@(subst `(cons ,a ,x) x formals))
714
 
                   (and ,(if negatedp
715
 
                             `(not (,elementp ,@(subst a x elem-formals)))
716
 
                           `(,elementp ,@(subst a x elem-formals)))
717
 
                        (,name ,@formals)))
718
 
            :hints(("Goal" :in-theory (enable ,name))))
719
 
 
720
 
          ;; Occasionally the user might prove these theorems on his own, e.g.,
721
 
          ;; due to a mutual recursion.  When this happens, they can end up
722
 
          ;; locally DISABLED!!!!  because of the theory hint we gave above.  So,
723
 
          ;; make sure they're explicitly enabled.
724
 
          (local (in-theory (enable ,(mksym name '-when-not-consp)
725
 
                                    ,(mksym name '-of-cons))))
726
 
 
727
 
          (local (in-theory (disable ,name)))
728
 
 
729
 
          ,@(and true-listp
730
 
                 `((defthm ,(mksym 'true-listp-when- name)
731
 
                     (implies (,name ,@formals)
732
 
                              (true-listp ,x))
733
 
                     :rule-classes
734
 
                     ,(if (eql (len formals) 1)
735
 
                          :compound-recognizer
736
 
                        ;; Unfortunately we can't use a compound recognizer rule
737
 
                        ;; in this case.  I guess we'll try a rewrite rule, even
738
 
                        ;; though it could get expensive.
739
 
                        :rewrite)
740
 
                     :hints(("Goal" :induct (len ,x))))
741
 
 
742
 
                   (defthm ,(mksym name '-of-list-fix)
743
 
                     ;; This is not very satisfying.  Ideally, ACL2 would
744
 
                     ;; deeply understand, from the compound-recognizer rule
745
 
                     ;; showing true-listp when foo-listp, that whenever
746
 
                     ;; (foo-listp x) holds then (true-listp x) holds.
747
 
                     ;; Ideally, it could use this knowledge to rewrite
748
 
                     ;; (list-fix x) to x whenever we can show (foo-listp x).
749
 
                     ;;
750
 
                     ;; But compound recognizers aren't quite good enough for
751
 
                     ;; this.  For instance, ACL2 won't rewrite a term like
752
 
                     ;; (list-fix (accessor x)) into (accessor x) even if we
753
 
                     ;; have a rewrite rule that says (foo-listp (accessor x)).
754
 
                     ;;
755
 
                     ;; Some alternatives we considered:
756
 
                     ;;
757
 
                     ;;  - A rewrite rule version of (foo-listp x) ==>
758
 
                     ;;    (true-listp x).  But it seems like this would get
759
 
                     ;;    *really* expensive when you have 100 list
760
 
                     ;;    recognizers and you encounter a true-listp term.
761
 
                     ;;
762
 
                     ;;  - A rewrite rule that rewrites (list-fix x) ==> x when
763
 
                     ;;    (foo-listp x) is known.  This might be the right
764
 
                     ;;    compromise.  It's at least somewhat less common to
765
 
                     ;;    see list-fix than true-listp.  But it still suffers
766
 
                     ;;    from the same kind of scaling problem.
767
 
                     ;;
768
 
                     ;; David's rule, below, is not as powerful as either of
769
 
                     ;; these approaches, but it at least manages to localize
770
 
                     ;; the performance impact, and helps at least in some
771
 
                     ;; cases.  Perhaps TAU can somehow help with this in the
772
 
                     ;; future.
773
 
                     (implies (,name ,@formals)
774
 
                              (,name ,@(subst `(list-fix ,x) x formals))))))
775
 
 
776
 
          (defthm ,(mksym elementp '-when-member-equal-of- name)
777
 
            ;; We previously used double-rewrite here, but it interferes with
778
 
            ;; free-variable matching
779
 
            (implies (and (,name ,@formals)
780
 
                          (member-equal ,a ,x))
781
 
                     (equal (,elementp ,@(subst a x elem-formals))
782
 
                            ,(not negatedp)))
783
 
            :rule-classes ((:rewrite)
784
 
                           (:rewrite
785
 
                            :corollary
786
 
                            (implies (and (member-equal ,a ,x)
787
 
                                          (,name ,@formals))
788
 
                                     (equal (,elementp ,@(subst a x elem-formals))
789
 
                                            ,(not negatedp)))))
790
 
            :hints(("Goal"
791
 
                    :induct (len ,x)
792
 
                    :in-theory (enable member-equal))))
793
 
 
794
 
          (defthm ,(mksym name '-when-subsetp-equal)
795
 
            ;; We previously used double-rewrite here, but it interferes with
796
 
            ;; free-variable matching
797
 
            (implies (and (,name ,@(subst y x formals))
798
 
                          (subsetp-equal ,x ,y))
799
 
                     (equal (,name ,@formals)
800
 
                            ,(if true-listp
801
 
                                 `(true-listp ,x)
802
 
                               t)))
803
 
            :rule-classes ((:rewrite)
804
 
                           (:rewrite :corollary
805
 
                                     (implies (and (subsetp-equal ,x ,y)
806
 
                                                   (,name ,@(subst y x formals)))
807
 
                                              (equal (,name ,@formals)
808
 
                                                     ,(if true-listp
809
 
                                                          `(true-listp ,x)
810
 
                                                        t)))))
811
 
            :hints(("Goal"
812
 
                    :induct (len ,x)
813
 
                    :in-theory (enable subsetp-equal ,name)
814
 
                    :expand (true-listp ,x)
815
 
                    :do-not '(eliminate-destructors))
816
 
 
817
 
                   ;; Horrible, horrible hack.  I found that I couldn't get
818
 
                   ;; deflist to process ATOM-LISTP because ACL2 knows too much
819
 
                   ;; about ATOM, so the member-equal rule above ends up being
820
 
                   ;; no good because it tries to target ATOM instead of CONSP,
821
 
                   ;; and we get nowhere.  Solution: try to explicitly use the
822
 
                   ;; member rule if we get stuck.
823
 
                   (and stable-under-simplificationp
824
 
                        '(:in-theory (disable
825
 
                                      ,(mksym elementp '-when-member-equal-of- name))
826
 
                          :use ((:instance
827
 
                                 ,(mksym elementp '-when-member-equal-of- name)
828
 
                                 (,a (car ,x))
829
 
                                 (,x ,y)))))))
830
 
 
831
 
          ,@(and (not true-listp)
832
 
                 ;; Awesome set congruence rule for loose recognizers, but not
833
 
                 ;; a theorem for strict recognizers.
834
 
                 `((defthm ,(mksym name '-preserves-set-equiv)
835
 
                     (implies (set-equiv ,x ,y)
836
 
                              (equal (,name ,@formals)
837
 
                                     (,name ,@(subst y x formals))))
838
 
                     :rule-classes :congruence
839
 
                     :hints(("Goal"
840
 
                             :in-theory (enable set-equiv)
841
 
                             :cases ((,name ,@formals))
842
 
                             :do-not-induct t)))))
843
 
 
844
 
          (defthm ,(mksym name '-of-append)
845
 
            (equal (,name ,@(subst `(append ,x ,y) x formals))
846
 
                   (and (,name ,@(if true-listp
847
 
                                     (subst `(list-fix ,x) x formals)
848
 
                                   formals))
849
 
                        (,name ,@(subst y x formals))))
850
 
            :hints(("Goal"
851
 
                    :induct (len ,x)
852
 
                    :expand (list-fix ,x)
853
 
                    :in-theory (enable append))))
854
 
 
855
 
          ,@(and true-listp
856
 
                 ;; We don't bother proving these for loose recognizers because
857
 
                 ;; the set-equiv congruence should handle them automatically
858
 
                 `((defthm ,(mksym name '-of-rev)
859
 
                     (equal (,name ,@(subst `(rev ,x) x formals))
860
 
                            (,name ,@(if true-listp
861
 
                                         (subst `(list-fix ,x) x formals)
862
 
                                       formals)))
863
 
                     :hints(("Goal"
864
 
                             :induct (len ,x)
865
 
                             :expand (list-fix ,x)
866
 
                             :in-theory (enable rev))))
867
 
 
868
 
                   (defthm ,(mksym name '-of-revappend)
869
 
                     (equal (,name ,@(subst `(revappend ,x ,y) x formals))
870
 
                            (and (,name ,@(if true-listp
871
 
                                              (subst `(list-fix ,x) x formals)
872
 
                                            formals))
873
 
                                 (,name ,@(subst y x formals))))
874
 
                     :hints(("Goal"
875
 
                             :induct (revappend ,x ,y)
876
 
                             :in-theory (enable revappend))))))
877
 
 
878
 
          (defthm ,(mksym elementp '-of-car-when- name)
879
 
            (implies
880
 
             (,name ,@(subst `(double-rewrite ,x) x formals))
881
 
             (equal (,elementp ,@(subst `(car ,x) x elem-formals))
882
 
                    ,(cond
883
 
                      ((eq elementp-of-nil nil)
884
 
                       (if negatedp
885
 
                           ;; If x is a cons, then its car is not an element.
886
 
                           ;; Else its car is nil, which is not an element.
887
 
                           nil
888
 
                         ;; If x is a cons, then its car is an element.
889
 
                         ;; Else its car is nil, which is not an element.
890
 
                         `(consp ,x)))
891
 
                      ((eq elementp-of-nil t)
892
 
                       (if negatedp
893
 
                           ;; If x is a cons, then its car is not an element.
894
 
                           ;; Else its car is nil, which is an element.
895
 
                           `(not (consp ,x))
896
 
                         ;; If x is a cons, then its car is an element.
897
 
                         ;; Else its car is nil, which is an element.
898
 
                         t))
899
 
                      (t ;; elementp-of-nil is :unknown
900
 
                       `(if (consp ,x)
901
 
                            ,(not negatedp)
902
 
                          (,elementp ,@(subst nil x elem-formals)))))))
903
 
            :hints(("Goal"
904
 
                    :in-theory (enable default-car)
905
 
                    :expand ((,name . ,formals)))))
906
 
 
907
 
          (defthm ,(mksym name '-of-cdr-when- name)
908
 
            (implies (,name ,@(subst `(double-rewrite ,x) x formals))
909
 
                     (equal (,name ,@(subst `(cdr ,x) x formals))
910
 
                            t)))
911
 
 
912
 
          (defthm ,(mksym elementp '-of-nth-when- name)
913
 
            (implies
914
 
             (,name ,@(subst `(double-rewrite ,x) x formals))
915
 
             (equal (,elementp ,@(subst `(nth ,n ,x) x formals))
916
 
                    ,(cond
917
 
                      ((eq elementp-of-nil nil)
918
 
                       (if negatedp
919
 
                           ;; (elementp {e \in X}) = NIL, (elementp nil) = NIL
920
 
                           nil
921
 
                         ;; (elementp {(e \in X}) = T, (elementp nil) = NIL
922
 
                         `(< (nfix ,n) (len ,x))))
923
 
                      ((eq elementp-of-nil t)
924
 
                       (if negatedp
925
 
                           ;; (elementp {e \in X}) = NIL, (elementp nil) = T
926
 
                           `(>= (nfix ,n) (len ,x))
927
 
                         ;; (elementp {e \in X}) = T, (elementp nil) = T
928
 
                         t))
929
 
                      (t
930
 
                       (if negatedp
931
 
                           ;; (elementp {e \in X}) = NIL, (elementp nil) = ???
932
 
                           `(and (,elementp ,@(subst nil x elem-formals))
933
 
                                 (>= (nfix ,n) (len ,x)))
934
 
                         ;; (elementp {e \in X}) = T, (elementp nil) = ???
935
 
                         `(or (,elementp ,@(subst nil x elem-formals))
936
 
                              (< (nfix ,n) (len ,x))))))))
937
 
            :hints(("Goal" :induct (nth ,n ,x))))
938
 
 
939
 
          (defthm ,(mksym name '-of-update-nth-when- elementp)
940
 
            ;; 1. When (elementp nil) = NIL, there's a strong bound because if
941
 
            ;; you update something past the length of the list, you introduce
942
 
            ;; NILs into the list and then ruin foo-listp.
943
 
            ;;
944
 
            ;; 2. When (elementp nil) = T, there's no bound because no matter
945
 
            ;; whether you add NILs, they're still valid.
946
 
            ;;
947
 
            ;; 3. When (elementp nil) = Unknown, we restrict the rule to only
948
 
            ;; fire if N is in bounds
949
 
            ,(let ((val-okp (if negatedp
950
 
                                `(not (,elementp ,@(subst y x elem-formals)))
951
 
                              `(,elementp ,@(subst y x elem-formals)))))
952
 
               (cond ((eq elementp-of-nil negatedp)
953
 
                      `(implies
954
 
                        (,name ,@(subst `(double-rewrite ,x) x formals))
955
 
                        (equal (,name ,@(subst `(update-nth ,n ,y ,x) x formals))
956
 
                               (and (<= (nfix ,n) (len ,x))
957
 
                                    ,val-okp))))
958
 
                     ((eq elementp-of-nil (not negatedp))
959
 
                      `(implies
960
 
                        (,name ,@(subst `(double-rewrite ,x) x formals))
961
 
                        (equal (,name ,@(subst `(update-nth ,n ,y ,x) x formals))
962
 
                               ,val-okp)))
963
 
                     (t
964
 
                      `(implies
965
 
                        (and (<= (nfix ,n) (len ,x))
966
 
                             (,name ,@(subst `(double-rewrite ,x) x formals)))
967
 
                        (equal (,name ,@(subst `(update-nth ,n ,y ,x) x formals))
968
 
                               ,val-okp))))))
969
 
 
970
 
          (defthm ,(mksym name '-of-nthcdr)
971
 
            (implies (,name ,@(subst `(double-rewrite ,x) x formals))
972
 
                     (equal (,name ,@(subst `(nthcdr ,n ,x) x formals))
973
 
                            t))
974
 
            :hints(("Goal" :do-not-induct t)))
975
 
 
976
 
          (defthm ,(mksym name '-of-take)
977
 
            (implies
978
 
             (,name ,@(subst `(double-rewrite ,x) x formals))
979
 
             (equal (,name ,@(subst `(take ,n ,x) x formals))
980
 
                    ,(cond
981
 
                      ((eq elementp-of-nil nil)
982
 
                       (if negatedp
983
 
                           t
984
 
                         `(<= (nfix ,n) (len ,x))))
985
 
                      ((eq elementp-of-nil t)
986
 
                       (if negatedp
987
 
                           `(<= (nfix ,n) (len ,x))
988
 
                         t))
989
 
                      (t
990
 
                       (if negatedp
991
 
                           `(or (not (,elementp ,@(subst nil x elem-formals)))
992
 
                                (<= (nfix ,n) (len ,x)))
993
 
                         `(or (,elementp ,@(subst nil x elem-formals))
994
 
                              (<= (nfix ,n) (len ,x))))))))
995
 
            :hints(("Goal"
996
 
                    :in-theory (enable acl2::take-redefinition)
997
 
                    :induct (take ,n ,x)
998
 
                    :expand ((,name ,@formals)
999
 
                             (:free (,x ,y)
1000
 
                                    (,name ,@(subst `(cons ,x ,y) x formals)))))))
1001
 
 
1002
 
          (defthm ,(mksym name '-of-replicate)
1003
 
            (equal (,name ,@(subst `(replicate ,n ,x) x formals))
1004
 
                   (or ,(cond (negatedp
1005
 
                               `(not (,elementp ,@formals)))
1006
 
                              (t
1007
 
                               `(,elementp ,@formals)))
1008
 
                       (zp ,n)))
1009
 
            :hints(("Goal"
1010
 
                    :induct (replicate ,n ,x)
1011
 
                    :in-theory (enable replicate deflist-local-booleanp-element-thm)
1012
 
                    :expand ((,name ,@formals)
1013
 
                             (:free (,x ,y)
1014
 
                                    (,name ,@(subst `(cons ,x ,y) x formals)))))))
1015
 
 
1016
 
          (defthm ,(mksym name '-of-last)
1017
 
            (implies (,name ,@(subst `(double-rewrite ,x) x formals))
1018
 
                     (equal (,name ,@(subst `(last ,x) x formals))
1019
 
                            t))
1020
 
            :hints(("Goal" :do-not-induct t)))
1021
 
 
1022
 
          (defthm ,(mksym name '-of-butlast)
1023
 
            ;; Historically this was much more complicated, but after Matt
1024
 
            ;; fixed up butlast to not be totally crazy in the -N case
1025
 
            ;; (introduce NILs, etc.)  it simplifies down nicely.
1026
 
            (implies (,name ,@(subst `(double-rewrite ,x) x formals))
1027
 
                     (equal (,name ,@(subst `(butlast ,x ,n) x formals))
1028
 
                            t))
1029
 
            :hints(("Goal" :do-not-induct t)))
1030
 
 
1031
 
          (defthm ,(mksym name '-of-rcons)
1032
 
            (equal (,name ,@(subst `(rcons ,a ,x) x formals))
1033
 
                   (and ,(if negatedp
1034
 
                             `(not (,elementp ,@(subst a x elem-formals)))
1035
 
                           `(,elementp ,@(subst a x elem-formals)))
1036
 
                        (,name ,@(if true-listp
1037
 
                                     (subst `(list-fix ,x) x formals)
1038
 
                                   formals))))
1039
 
            :hints(("Goal" :in-theory (enable rcons))))
1040
 
 
1041
 
          (defthm ,(mksym name '-of-duplicated-members)
1042
 
            (implies (,name ,@(subst `(double-rewrite ,x) x formals))
1043
 
                     (equal (,name ,@(subst `(duplicated-members ,x) x formals))
1044
 
                            t))
1045
 
            :hints(("Goal" :do-not-induct t)))
1046
 
 
1047
 
          (defthm ,(mksym name '-of-set-difference-equal)
1048
 
            (implies (,name ,@(subst `(double-rewrite ,x) x formals))
1049
 
                     (equal (,name ,@(subst `(set-difference-equal ,x ,y) x formals))
1050
 
                            t))
1051
 
            :hints(("Goal" :do-not-induct t)))
1052
 
 
1053
 
          (defthm ,(mksym name '-of-intersection-equal-1)
1054
 
            (implies (,name ,@(subst `(double-rewrite ,x) x formals))
1055
 
                     (equal (,name ,@(subst `(intersection-equal ,x ,y) x formals))
1056
 
                            t))
1057
 
            :hints(("Goal" :do-not-induct t)))
1058
 
 
1059
 
          (defthm ,(mksym name '-of-intersection-equal-2)
1060
 
            (implies (,name ,@(subst `(double-rewrite ,y) x formals))
1061
 
                     (equal (,name ,@(subst `(intersection-equal ,x ,y) x formals))
1062
 
                            t))
1063
 
            :hints(("Goal" :do-not-induct t)))
1064
 
 
1065
 
          (defthm ,(mksym name '-of-sfix)
1066
 
            ;; This rule is important for set::under-set-equiv rules to work
1067
 
            ;; right in the context of a foo-listp.
1068
 
            (implies (,name ,@(subst `(double-rewrite ,x) x formals))
1069
 
                     (equal (,name ,@(subst `(sfix ,x) x formals))
1070
 
                            t))
1071
 
            :hints(("Goal"
1072
 
                    :do-not-induct t
1073
 
                    :cases ((setp ,x)))))
1074
 
 
1075
 
          ,@(and true-listp
1076
 
                 ;; These aren't needed in the non true-listp case, because set
1077
 
                 ;; reasoning will reduce them to, e.g., append,
1078
 
                 ;; set-difference-equal, intersection-equal, etc.
1079
 
                 `((defthm ,(mksym name '-of-union-equal)
1080
 
                     (equal (,name ,@(subst `(union-equal ,x ,y) x formals))
1081
 
                            (and (,name ,@(subst `(list-fix ,x) x formals))
1082
 
                                 (,name ,@(subst `(double-rewrite ,y) x formals))))
1083
 
                     :hints(("Goal"
1084
 
                             :induct (len ,x)
1085
 
                             :in-theory (enable union-equal))))
1086
 
 
1087
 
                   (defthm ,(mksym name '-of-difference)
1088
 
                     (implies (,name ,@formals)
1089
 
                              (equal (,name ,@(subst `(difference ,x ,y) x formals))
1090
 
                                     t))
1091
 
                     :hints(("Goal" :do-not-induct t)))
1092
 
 
1093
 
                   (defthm ,(mksym name '-of-intersect-1)
1094
 
                     (implies (,name ,@formals)
1095
 
                              (equal (,name ,@(subst `(intersect ,x ,y) x formals))
1096
 
                                     t))
1097
 
                     :hints(("Goal" :do-not-induct t)))
1098
 
 
1099
 
                   (defthm ,(mksym name '-of-intersect-2)
1100
 
                     (implies (,name ,@(subst y x formals))
1101
 
                              (equal (,name ,@(subst `(intersect ,x ,y) x formals))
1102
 
                                     t))
1103
 
                     :hints(("Goal" :do-not-induct t)))
1104
 
 
1105
 
                   (defthm ,(mksym name '-of-mergesort)
1106
 
                     (equal (,name ,@(subst `(mergesort ,x) x formals))
1107
 
                            (,name ,@(subst `(list-fix ,x) x formals)))
1108
 
                     :hints(("Goal"
1109
 
                             :do-not-induct t
1110
 
                             :in-theory (disable ,(mksym name '-when-subsetp-equal))
1111
 
                             :use ((:instance ,(mksym name '-when-subsetp-equal)
1112
 
                                              (,x (mergesort ,x))
1113
 
                                              (,y (list-fix ,x)))
1114
 
                                   (:instance ,(mksym name '-when-subsetp-equal)
1115
 
                                              (,y (mergesort ,x))
1116
 
                                              (,x (list-fix ,x)))))))
1117
 
 
1118
 
                   (local
1119
 
                    (defthm ,(mksym name '-of-union-lemma-1)
1120
 
                      (implies (,name ,@(subst `(union ,x ,y) x formals))
1121
 
                               (and (,name ,@(subst `(sfix ,x) x formals))
1122
 
                                    (,name ,@(subst `(sfix ,y) x formals))))
1123
 
                      :hints(("Goal" :do-not-induct t))))
1124
 
 
1125
 
                   (local
1126
 
                    (defthm ,(mksym name '-of-union-lemma-2)
1127
 
                      (implies (and (,name ,@(subst `(sfix ,x) x formals))
1128
 
                                    (,name ,@(subst `(sfix ,y) x formals)))
1129
 
                               (,name ,@(subst `(union ,x ,y) x formals)))
1130
 
                      :hints(("Goal"
1131
 
                              :do-not-induct t
1132
 
                              :in-theory (disable set::union-under-set-equiv
1133
 
                                                  deflist-lemma-subsetp-of-union)
1134
 
                              :use ((:instance deflist-lemma-subsetp-of-union
1135
 
                                               (x ,x)
1136
 
                                               (y ,y)))))))
1137
 
 
1138
 
                   (defthm ,(mksym name '-of-union)
1139
 
                     (equal (,name ,@(subst `(union ,x ,y) x formals))
1140
 
                            (and (,name ,@(subst `(sfix ,x) x formals))
1141
 
                                 (,name ,@(subst `(sfix ,y) x formals))))
1142
 
                     :hints(("Goal"
1143
 
                             :cases ((,name ,@(subst `(union ,x ,y) x formals)))
1144
 
                             :do-not-induct t)))
1145
 
                   ))
1146
 
 
1147
 
          )))
1148
 
 
1149
 
    `(defsection ,name
1150
 
       ,@(and parents `(:parents ,parents))
1151
 
       ,@(and short   `(:short ,short))
1152
 
       ,@(and long    `(:long ,long))
1153
 
       ;; keep all our deflist theory stuff bottled up.  BOZO encapsulate is
1154
 
       ;; slow, better to use a progn here
1155
 
       (encapsulate ()
1156
 
         . ,events)
1157
 
       ;; now do the rest of the events with name enabled, so they get included
1158
 
       ;; in the section
1159
 
       . ,(and rest
1160
 
               `((value-triple (cw "Deflist: submitting /// events.~%"))
1161
 
                 (with-output
1162
 
                   :stack :pop
1163
 
                   (progn
1164
 
                     (local (in-theory (enable ,name)))
1165
 
                     . ,rest)))))))
1166
 
 
1167
 
 
1168
 
(defmacro deflist (name &rest args)
1169
 
  (b* ((__function__ 'deflist)
1170
 
       ((unless (symbolp name))
1171
 
        (raise "Name must be a symbol."))
1172
 
       (ctx (list 'deflist name))
1173
 
       ((mv main-stuff other-events) (split-/// ctx args))
1174
 
       ((mv kwd-alist formals-elem)
1175
 
        (extract-keywords ctx *deflist-valid-keywords* main-stuff nil))
1176
 
       ((unless (tuplep 2 formals-elem))
1177
 
        (raise "Wrong number of arguments to deflist."))
1178
 
       ((list formals element) formals-elem)
1179
 
       (verbosep (getarg :verbosep nil kwd-alist)))
1180
 
    `(with-output
1181
 
       :stack :push
1182
 
       ,@(if verbosep
1183
 
             nil
1184
 
           '(:gag-mode t :off (acl2::summary
1185
 
                               acl2::observation
1186
 
                               acl2::prove
1187
 
                               acl2::proof-tree
1188
 
                               acl2::event)))
1189
 
       (make-event
1190
 
        `(progn ,(deflist-fn ',name ',formals ',element ',kwd-alist
1191
 
                   ',other-events state)
1192
 
                (value-triple '(deflist ,',name)))))))
1193
 
 
1194
 
 
1195