← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/data-structures/defalist.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/data-structures/defalist.lisp
22
22
;;;    bevier@cli.com
23
23
;;;
24
24
;;;    Modified by Bishop Brock, brock@cli.com
25
 
;;;    
 
25
;;;
26
26
;;;~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
27
27
 
28
 
; To certify this book:
29
 
#|
30
 
 (in-package "ACL2")
31
 
 (defpkg "U" (union-eq *acl2-exports*
32
 
                       *common-lisp-symbols-from-main-lisp-package*))
33
 
 (certify-book "defalist" 1)
34
 
|#
 
28
; Modified by Jared Davis, October 2014, to port documentation to xdoc.
35
29
 
36
30
(in-package "ACL2")
37
31
 
121
115
 
122
116
 
123
117
; For each lemma in the theory, the lemma term is defined by a macro
124
 
; to make it easy to instantiate. The lemma is then proved. 
 
118
; to make it easy to instantiate. The lemma is then proved.
125
119
 
126
120
 
127
121
; The macros in the following script generate forms that are believed to be
132
126
; ran-type-fn
133
127
; dom-elem-type-fn
134
128
; ran-elem-type-fn
135
 
; 
 
129
;
136
130
; formals:      the formal parameter list to alist-type-fn
137
131
;               We assume that the other type fns are unary predicates, either
138
132
;               symbols or lambda expressions.
139
133
;
140
134
; guard         either 't, or an expression in the formal parameters
141
135
;
142
 
; Example: 
 
136
; Example:
143
137
;
144
 
;  (defun bound-numberp (x lub) 
 
138
;  (defun bound-numberp (x lub)
145
139
;    (and (acl2-numberp x) (acl2-numberp lub) (< x lub)))
146
140
;
147
 
;  (defun bound-number-listp (l lub) 
 
141
;  (defun bound-number-listp (l lub)
148
142
;    (cond ((atom l) t)
149
143
;          (t (and (bound-numberp (car l) lub)
150
144
;                  (bound-number-listp (cdr l) lub)))))
161
155
  `(implies ,(my-conjoin (my-conjuncts guard)
162
156
                         `((,alist-type-fn ,@formals)))
163
157
            (alistp l)))
164
 
                                              
 
158
 
165
159
(defthm alist-type-alistp
166
 
  (alist-type-alistp-lemma alist-type domain-type range-type 
 
160
  (alist-type-alistp-lemma alist-type domain-type range-type
167
161
                           domain-elem-type range-elem-type
168
162
                           (l))
169
163
  :rule-classes :forward-chaining
185
179
                           `((,alist-type-fn ,@formals)
186
180
                             (,dom-elem-type-fn ,var1)
187
181
                             (,ran-elem-type-fn ,var2)))
188
 
              (,alist-type-fn ,@(replace-equal 'l 
 
182
              (,alist-type-fn ,@(replace-equal 'l
189
183
                                               `(acons ,var1 ,var2 l)
190
184
                                               formals)))))
191
 
  
 
185
 
192
186
(defthm alist-type-acons
193
 
  (alist-type-acons-lemma alist-type domain-type range-type 
 
187
  (alist-type-acons-lemma alist-type domain-type range-type
194
188
                          domain-elem-type range-elem-type (l))
195
189
  :hints (("Goal" :do-not-induct t
196
190
           :in-theory (enable alist-type-alistp acons))))
205
199
  (let* ((vars (u::unique-symbols 2 (intern-in-package-of-symbol "L" alist-type-fn) formals))
206
200
         (var1 (car vars))
207
201
         (var2 (cadr vars)))
208
 
    `(implies ,(my-conjoin (my-conjuncts guard) 
 
202
    `(implies ,(my-conjoin (my-conjuncts guard)
209
203
                           `((,alist-type-fn ,@(replace-equal 'l var1 formals))
210
204
                             (,alist-type-fn ,@(replace-equal 'l var2 formals))))
211
205
              (,alist-type-fn ,@(replace-equal 'l `(append ,var1 ,var2) formals)))))
212
206
 
213
 
(defthm alist-type-append 
214
 
  (alist-type-append-lemma alist-type domain-type range-type 
 
207
(defthm alist-type-append
 
208
  (alist-type-append-lemma alist-type domain-type range-type
215
209
                           domain-elem-type range-elem-type (l))
216
210
  :hints (("Goal" :induct t)))
217
211
 
229
223
                           `((,alist-type-fn ,@formals)
230
224
                             (,dom-elem-type-fn ,var1)
231
225
                             (,ran-elem-type-fn ,var2)))
232
 
              (,alist-type-fn ,@(replace-equal 'l 
 
226
              (,alist-type-fn ,@(replace-equal 'l
233
227
                                               `(bind-equal ,var1 ,var2 l)
234
228
                                               formals)))))
235
 
  
 
229
 
236
230
(defthm alist-type-bind-equal
237
 
  (alist-type-bind-equal-lemma alist-type domain-type range-type 
 
231
  (alist-type-bind-equal-lemma alist-type domain-type range-type
238
232
                         domain-elem-type range-elem-type (l))
239
233
  :hints (("Goal" :induct t)))
240
234
 
252
246
              (,alist-type-fn ,@(replace-equal 'l `(rembind-equal ,var l) formals)))))
253
247
 
254
248
(defthm alist-type-rembind-equal
255
 
  (alist-type-rembind-equal-lemma alist-type domain-type range-type 
 
249
  (alist-type-rembind-equal-lemma alist-type domain-type range-type
256
250
                            domain-elem-type range-elem-type (l))
257
251
  :hints (("Goal" :induct t)))
258
252
 
276
270
                                               formals)))))
277
271
 
278
272
(defthm alist-type-pairlis$
279
 
  (alist-type-pairlis$-lemma alist-type domain-type range-type 
 
273
  (alist-type-pairlis$-lemma alist-type domain-type range-type
280
274
                             domain-elem-type range-elem-type (l))
281
275
  :hints (("Goal" :induct t)))
282
276
 
290
284
  (let* ((vars (u::unique-symbols 3 (intern-in-package-of-symbol "L" alist-type-fn) formals))
291
285
         (var1 (car vars))
292
286
         (var2 (cadr vars))
293
 
         (var3 (caddr vars)))          
294
 
    `(implies ,(my-conjoin (my-conjuncts guard) 
 
287
         (var3 (caddr vars)))
 
288
    `(implies ,(my-conjoin (my-conjuncts guard)
295
289
                           `((,dom-type-fn ,@(replace-equal 'l var1 formals))
296
290
                             (,ran-type-fn ,@(replace-equal 'l var2 formals))
297
291
                             (,alist-type-fn ,@(replace-equal 'l var3 formals))))
298
292
              (,alist-type-fn ,@(replace-equal 'l `(bind-all-equal ,var1 ,var2 ,var3) formals)))))
299
293
 
300
 
(defthm alist-type-bind-all-equal 
301
 
  (alist-type-bind-all-equal-lemma alist-type domain-type range-type 
 
294
(defthm alist-type-bind-all-equal
 
295
  (alist-type-bind-all-equal-lemma alist-type domain-type range-type
302
296
                           domain-elem-type range-elem-type (l))
303
297
  :hints (("Goal" :induct t)))
304
298
 
318
312
                                               `(domain-restrict-equal ,var l)
319
313
                                               formals)))))
320
314
 
321
 
(defthm alist-type-domain-restrict-equal 
322
 
  (alist-type-domain-restrict-equal-lemma alist-type domain-type range-type 
 
315
(defthm alist-type-domain-restrict-equal
 
316
  (alist-type-domain-restrict-equal-lemma alist-type domain-type range-type
323
317
                                    domain-elem-type range-elem-type (l))
324
318
  :hints (("Goal" :induct t)))
325
319
 
337
331
              (,alist-type-fn ,@(replace-equal 'l `(rembind-all-equal ,var l) formals)))))
338
332
 
339
333
(defthm alist-type-rembind-all-equal
340
 
  (alist-type-rembind-all-equal-lemma alist-type domain-type range-type 
 
334
  (alist-type-rembind-all-equal-lemma alist-type domain-type range-type
341
335
                            domain-elem-type range-elem-type (l))
342
336
  :hints (("Goal" :induct t)))
343
337
 
356
350
              (,alist-type-fn ,@(replace-equal 'l `(bind-pairs-equal ,var l) formals)))))
357
351
 
358
352
(defthm alist-type-bind-pairs-equal
359
 
  (alist-type-bind-pairs-equal-lemma alist-type domain-type range-type 
 
353
  (alist-type-bind-pairs-equal-lemma alist-type domain-type range-type
360
354
                            domain-elem-type range-elem-type (l))
361
355
  :hints (("Goal" :induct t)))
362
356
 
376
370
              (not (assoc-equal ,var l)))))
377
371
 
378
372
(defthm alist-type-assoc-equal
379
 
  (alist-type-assoc-equal-lemma  alist-type domain-type range-type 
 
373
  (alist-type-assoc-equal-lemma  alist-type domain-type range-type
380
374
                      domain-elem-type range-elem-type (l))
381
375
  :hints (("Goal" :in-theory (enable alist-type-alistp assoc-equal))))
382
376
 
395
389
              (not (bound?-equal ,var l)))))
396
390
 
397
391
(defthm alist-type-bound?-equal
398
 
  (alist-type-bound?-equal-lemma  alist-type domain-type range-type 
 
392
  (alist-type-bound?-equal-lemma  alist-type domain-type range-type
399
393
                      domain-elem-type range-elem-type (l))
400
394
  :hints (("Goal" :in-theory (enable alist-type-alistp bound?-equal))))
401
395
 
417
411
 
418
412
 
419
413
(defthm alist-type-all-bound?-equal
420
 
  (alist-type-all-bound?-equal-lemma  alist-type domain-type range-type 
 
414
  (alist-type-all-bound?-equal-lemma  alist-type domain-type range-type
421
415
                      domain-elem-type range-elem-type (l))
422
416
  :hints (("Goal" :in-theory (set-difference-theories (enable alist-type-alistp all-bound?-equal)
423
417
                                                      '(bound?-equal)))))
437
431
              (,ran-elem-type-fn (binding-equal ,var l)))))
438
432
 
439
433
(defthm alist-type-binding-equal
440
 
  (alist-type-binding-equal-lemma alist-type domain-type range-type 
 
434
  (alist-type-binding-equal-lemma alist-type domain-type range-type
441
435
                            domain-elem-type range-elem-type (l))
442
436
  :rule-classes :forward-chaining
443
437
  :hints (("Goal" :in-theory (enable alist-type-alistp binding-equal bound?-equal))))
457
451
              (,ran-elem-type-fn (cdr (assoc-equal ,var l))))))
458
452
 
459
453
(defthm alist-type-cdr-assoc-equal
460
 
  (alist-type-cdr-assoc-equal-lemma alist-type domain-type range-type 
 
454
  (alist-type-cdr-assoc-equal-lemma alist-type domain-type range-type
461
455
                            domain-elem-type range-elem-type (l))
462
456
  :rule-classes :forward-chaining
463
457
  :hints (("Goal" :in-theory (enable alist-type-alistp assoc-equal bound?-equal))))
474
468
            (,dom-type-fn (domain l))))
475
469
 
476
470
(defthm alist-type-domain
477
 
  (alist-type-domain-lemma  alist-type domain-type range-type 
 
471
  (alist-type-domain-lemma  alist-type domain-type range-type
478
472
                            domain-elem-type range-elem-type (l))
479
473
  :hints (("Goal" :in-theory (enable alist-type-alistp domain))))
480
474
 
490
484
            (,ran-type-fn (range l))))
491
485
 
492
486
(defthm alist-type-range
493
 
  (alist-type-range-lemma   alist-type domain-type range-type 
 
487
  (alist-type-range-lemma   alist-type domain-type range-type
494
488
                            domain-elem-type range-elem-type (l))
495
489
  :hints (("Goal" :in-theory (enable alist-type-alistp range))))
496
490
 
508
502
              (,dom-type-fn ,@(replace-equal 'l `(collect-bound-equal ,var l) formals)))))
509
503
 
510
504
(defthm alist-type-collect-bound-equal
511
 
  (alist-type-collect-bound-equal-lemma  alist-type domain-type range-type 
 
505
  (alist-type-collect-bound-equal-lemma  alist-type domain-type range-type
512
506
                      domain-elem-type range-elem-type (l))
513
507
  :hints (("Goal" :in-theory (set-difference-theories (enable alist-type-alistp collect-bound-equal)
514
508
                                                      '(bound?-equal)))))
527
521
              (,ran-type-fn ,@(replace-equal 'l `(all-bindings-equal ,var l) formals)))))
528
522
 
529
523
(defthm alist-type-all-bindings-equal
530
 
  (alist-type-all-bindings-equal-lemma  alist-type domain-type range-type 
 
524
  (alist-type-all-bindings-equal-lemma  alist-type domain-type range-type
531
525
                      domain-elem-type range-elem-type (l))
532
526
  :hints (("Goal" :in-theory (set-difference-theories (enable alist-type-alistp all-bindings-equal)
533
527
                                                      '(bound?-equal binding-equal)))))
556
550
 
557
551
; DEFALIST-DEFTHMS.
558
552
; Generate a list of DEFTHM forms. These defthms explain
559
 
; the properties of standard list operations with 
 
553
; the properties of standard list operations with
560
554
; respect to a typed list predicate.
561
555
; For arguments, see documentation for DEF-TYPED-LIST
562
556
; macro below.
563
557
 
564
 
(u::defloop defalist-defthms (alist-type-fn formals dom-elem-type-fn ran-elem-type-fn 
 
558
(u::defloop defalist-defthms (alist-type-fn formals dom-elem-type-fn ran-elem-type-fn
565
559
                                            dom-type-fn ran-type-fn guard theory binding-equal-rule-classes)
566
560
            (declare (xargs :guard (and (symbolp alist-type-fn)
567
561
                                        (arglistp formals)
584
578
                                          `(("Goal" :in-theory (enable ,fn ,@(if (eq fn 'binding-equal) '(bound?-equal) ()))))
585
579
                                        ;; The functional instance of the domain and range element types are
586
580
                                        ;; presented as lambda forms, since these may be defined as macros.
587
 
                                        (let ((domain-elem-type-instance (if (equal dom-elem-type-fn *defalist-true-fn*) 
 
581
                                        (let ((domain-elem-type-instance (if (equal dom-elem-type-fn *defalist-true-fn*)
588
582
                                                                             (remove-equal '(declare (ignore x)) dom-elem-type-fn)
589
583
                                                                           (cond ((and (consp dom-elem-type-fn)
590
584
                                                                                       (eq (car dom-elem-type-fn) 'acl2::lambda))
591
585
                                                                                  dom-elem-type-fn)
592
586
                                                                                 (t `(lambda (x) (,dom-elem-type-fn x))))))
593
 
                                              (domain-type-instance (if (equal dom-type-fn *defalist-true-fn*) 
 
587
                                              (domain-type-instance (if (equal dom-type-fn *defalist-true-fn*)
594
588
                                                                        (remove-equal '(declare (ignore x)) dom-type-fn)
595
589
                                                                      dom-type-fn))
596
 
                                              (range-elem-type-instance (if (equal ran-elem-type-fn *defalist-true-fn*) 
 
590
                                              (range-elem-type-instance (if (equal ran-elem-type-fn *defalist-true-fn*)
597
591
                                                                            (remove-equal '(declare (ignore x)) ran-elem-type-fn)
598
592
                                                                          (cond ((and (consp ran-elem-type-fn)
599
593
                                                                                      (eq (car ran-elem-type-fn) 'acl2::lambda))
600
594
                                                                                 ran-elem-type-fn)
601
595
                                                                                (t `(lambda (x) (,ran-elem-type-fn x))))))
602
 
                                              (range-type-instance (if (equal ran-type-fn *defalist-true-fn*) 
 
596
                                              (range-type-instance (if (equal ran-type-fn *defalist-true-fn*)
603
597
                                                                       (remove-equal '(declare (ignore x)) ran-type-fn)
604
598
                                                                     ran-type-fn)))
605
599
                                          `(("Goal" :do-not-induct t
628
622
                                                     (u::pack-intern alist-type-fn 'alist-type- fn)
629
623
                                                     hints)))
630
624
                                 nil))))))
631
 
                                       
 
625
 
632
626
 
633
627
(defconst *defalist-options* '(:BINDING-EQUAL-RULE-CLASSES :THEORY :OMIT-DEFUN :DOMAIN-TYPE :RANGE-TYPE :THEORY-NAME)
634
628
  "This list contains all of the  valid keyword options for DEFALIST.")
635
629
 
636
630
(defconst *forward-chaining-elem-types*
637
 
  '(integerp rationalp complex-rationalp symbolp true-listp stringp characterp 
 
631
  '(integerp rationalp complex-rationalp symbolp true-listp stringp characterp
638
632
             alistp acl2-numberp
639
633
             #+:non-standard-analysis realp
640
634
             #+:non-standard-analysis complexp)
692
686
                             or a 1-argument LAMBDA function, and r ~
693
687
                             is either a function symbol or a 1-argument
694
688
                             LAMBDA function. ~p0 does not satisfy this
695
 
                             requirement." predicate))))))) 
 
689
                             requirement." predicate)))))))
696
690
 
697
691
(deftheory minimal-theory-for-defalist
698
692
  (union-theories
719
713
                         (all-bindings-equal (not (equal ran-type-fn *defalist-true-fn*)))
720
714
                         (t t))
721
715
                   (collect fn))))
722
 
                            
723
 
(defmacro defalist (name formals &rest body)
724
 
  ":doc-section data-structures
725
 
  Define a new alist type, and a theory of the alist type.
726
 
  ~/
727
 
 Examples:
728
 
 
 
716
 
 
717
(defsection defalist
 
718
  :parents (data-structures)
 
719
  :short "Define a new alist type, and a theory of the alist type."
 
720
  :long "Examples:
 
721
 
 
722
@({
729
723
  (defalist symbol-to-integer-alistp (l)
730
724
    \"Recognizes an alist mapping symbols to integers.\"
731
 
    (symbolp . integerp))   
732
 
 
 
725
    (symbolp . integerp))
 
726
 
733
727
  (defalist symbol-to-bnatural-alistp (l lub)
734
728
    \"Recognizes an alists mapping symbols to  naturals bounded by lub.\"
735
729
    (symbolp . (lambda (x) (bnaturalp x lub))))
736
 
 
 
730
 
737
731
  (defalist symbol-alistp (l)
738
732
    \"Define an alist theory alists from an unspecified domain type to
739
733
     symbols.\"
740
734
    ((lambda (x) t) . symbolp)
741
735
    (:options :omit-defun (:range-type symbol-listp)))
742
 
 
 
736
 
743
737
  (defalist string-to-integer-alistp (l)
744
 
    \"Recognizes an alist mapping strings to integers. Produce a minimal 
 
738
    \"Recognizes an alist mapping strings to integers. Produce a minimal
745
739
     theory, and store the BINDING-EQUAL lemma as a :TYPE-PRESCRIPTION.\"
746
740
    (stringp . integerp)
747
741
    (:options (:theory nth put) (:binding-equal-rule-classes :type-prescription)
748
742
              (:domain-type string-listp) (:range-type integer-listp)))
749
 
 ~/
750
 
 Syntax:
751
 
 
 
743
})
 
744
 
 
745
<p>Syntax:</p>
 
746
 
 
747
@({
752
748
   DEFALIST name arglist [documentation] {declaration}* type-pair [option-list]
753
 
 
 
749
 
754
750
   option-list ::= (:OPTIONS <<!options>>)
755
 
 
 
751
 
756
752
   options ::= !binding-equal-rule-classes-option |
757
753
               !omit-defun-option |
758
754
               !theory-option |
759
755
               !domain-type-option |
760
756
               !range-type-option |
761
 
               !theory-name-option 
762
 
 
 
757
               !theory-name-option
 
758
 
763
759
   theory-option ::= (:THEORY <<!alist-functions>>)
764
760
 
765
761
   theory-name-option ::= (:THEORY-NAME theory-name)
766
 
 
 
762
 
767
763
   alist-functions ::= acons | alistp | all-bindings-equal| all-bound?-equal | append |
768
 
                       assoc-equal | bind-all-equal | bind-equal | bind-pairs-equal | 
 
764
                       assoc-equal | bind-all-equal | bind-equal | bind-pairs-equal |
769
765
                       binding-equal | bound?-equal | collect-bound-equal | domain |
770
766
                       domain-restrict-equal | pairlis$ | range | rembind-all-equal |
771
767
                       rembind-equal
772
 
 
 
768
 
773
769
   binding-equal-rule-classes-option ::= (:BINDING-EQUAL-RULE-CLASSES rule-classes)
774
 
 
 
770
 
775
771
   omit-defun-option ::= :OMIT-DEFUN
776
 
 
777
 
 Arguments and Values:
778
 
 
 
772
})
 
773
 
 
774
<p>Arguments and Values:</p>
 
775
 
 
776
@({
779
777
   arglist -- an argument list satisfying ACL2::ARGLISTP, and containing
780
778
     exactly one symbol whose `print-name' is \"L\".
781
 
 
 
779
 
782
780
   declaration -- any valid declaration.
783
 
 
 
781
 
784
782
   documentation -- a string; not evaluated.
785
 
  
 
783
 
786
784
   name -- a symbol.
787
785
 
788
786
   theory-name -- any symbol that is a legal name for a deftheory event.
789
 
  
 
787
 
790
788
   type-pair -- A pair (d . r) where d and r are either a function symbol
791
 
     or a one argument LAMBDA function or the constant T. 
792
 
     d designates a predicate to be applied to each element of the domain 
 
789
     or a one argument LAMBDA function or the constant T.
 
790
     d designates a predicate to be applied to each element of the domain
793
791
     of the alist, and r designates a predicate to be applied to each element
794
792
     of the range of the alist. T means no type restriction.
795
793
 
797
795
    of DEFTHM.
798
796
 
799
797
   Acl2-theory-expression -- Any legal Acl2 theory expression
800
 
 
801
 
 Description:
802
 
 
803
 
  DEFALIST defines a recognizer for association lists whose pairs map
804
 
  keys of a given type to values of a given type, and by default creates 
805
 
  an extensive theory for alists of the newly defined type.
806
 
 
807
 
  To define an alist type with DEFALIST you must supply a name for the alist
 
798
})
 
799
 
 
800
<h3>Description:</h3>
 
801
 
 
802
<p>DEFALIST defines a recognizer for association lists whose pairs map
 
803
  keys of a given type to values of a given type, and by default creates
 
804
  an extensive theory for alists of the newly defined type.</p>
 
805
 
 
806
<p>To define an alist type with DEFALIST you must supply a name for the alist
808
807
  recognizer, an argument list for the recognizer, and predicate designator for
809
808
  elements of the alist's range. The name may be any symbol.  The argument list
810
809
  must be valid as a functional argument list, and must contain exactly one
811
810
  symbol whose `print-name'is \"L\".  By convention this is the alist argument
812
 
  recognized by the function defined by DEFALIST.
 
811
  recognized by the function defined by DEFALIST.</p>
813
812
 
814
 
  The type of the domain and range of the alist is given by a pair (d . r)
 
813
<p>The type of the domain and range of the alist is given by a pair (d . r)
815
814
  where d identifies the type of an element of the alist's domain, and r
816
815
  specifies the type of an element of the alist's range. Either of these
817
816
  may be specified by a symbol which names a one-argument function (or macro)
818
817
  which tests the elements of the domain and range of L. Either of d and r may
819
818
  also be specified as a single-argument LAMBDA function. Finally, either of d
820
 
  and r may be specified as the constant t, indicating no type constraint.
821
 
 
822
 
  Any number of other arguments to the alist functions may be supplied, 
823
 
  but only the L argument will change in the recursive structure of the recognizer.
824
 
 
825
 
  Note that DEFALIST does not create any guards for L or any other argument.
 
819
  and r may be specified as the constant t, indicating no type constraint.</p>
 
820
 
 
821
<p>Any number of other arguments to the alist functions may be supplied,
 
822
  but only the L argument will change in the recursive structure of the recognizer.</p>
 
823
 
 
824
<p>Note that DEFALIST does not create any guards for L or any other argument.
826
825
  Guards may be specified in the usual way since any number of DECLARE forms
827
826
  may preceed the predicate specification in the DEFALIST form.  Bear in mind
828
827
  that if you are defining a function to be used as a guard, then you are
829
828
  advised to consider what impact guarding the arguments of the function may
830
829
  have on its utility.  In general the most useful guard functions are those
831
 
  that are guard-free.
832
 
 
833
 
 Theory:
834
 
 
835
 
  By default, DEFALIST creates an extensive theory for the recognized alists.
836
 
  This theory contains appropriate lemmas for all of the alist functions 
 
830
  that are guard-free.</p>
 
831
 
 
832
<h3>Theory</h3>
 
833
 
 
834
<p>By default, DEFALIST creates an extensive theory for the recognized alists.
 
835
  This theory contains appropriate lemmas for all of the alist functions
837
836
  appearing in the `alist-functions' syntax description above.  One can select
838
837
  a subset of this theory to be generated by using the :THEORY option
839
 
  (see below).  DEFALIST always creates a :FORWARD-CHAINING rule from the 
840
 
  recognizer to ALISTP.
 
838
  (see below).  DEFALIST always creates a :FORWARD-CHAINING rule from the
 
839
  recognizer to ALISTP.</p>
841
840
 
842
 
  DEFALIST also creates a DEFTHEORY event that lists all of the lemmas created
 
841
<p>DEFALIST also creates a DEFTHEORY event that lists all of the lemmas created
843
842
  by the DEFALIST.  The name of the theory is formed by concatenating the
844
843
  function name and the string \"-THEORY\", and INTERNing the resulting string
845
 
  in the package of the function name.
846
 
 
847
 
 Options:
848
 
 
849
 
  DEFALIST options are specified with a special :OPTIONS list systax.  If
 
844
  in the package of the function name.</p>
 
845
 
 
846
<h3>Options</h3>
 
847
 
 
848
<p>DEFALIST options are specified with a special :OPTIONS list systax.  If
850
849
  present, the :OPTIONS list must appear as the last form in the body of the
851
 
  DEFALIST.
852
 
 
853
 
  :OMIT-DEFUN
854
 
 
855
 
    If the :OMIT-DEFUN keyword is present then the definition will not be
 
850
  DEFALIST.</p>
 
851
 
 
852
<dl>
 
853
<dt>:OMIT-DEFUN</dt>
 
854
<dd>If the :OMIT-DEFUN keyword is present then the definition will not be
856
855
    created.  Instead, only the list theory for the function is
857
856
    generated. Use this option to create a list theory for recognizers
858
 
    defined elsewhere.
859
 
 
860
 
  :THEORY  
861
 
 
862
 
   This option is used to specify that only a subset of the list theory be
 
857
    defined elsewhere.</dd>
 
858
 
 
859
<dt>:THEORY</dt>
 
860
<dd>This option is used to specify that only a subset of the list theory be
863
861
   created.  In the STRINGP-LISTP example above we specify that only lemmas
864
862
   about STRINGP-LISTP viz-a-viz NTH and PUT are to be generated.  By default
865
863
   the complete list theory for the recognizer is created.  If the option is
866
864
   given as (:THEORY) then the entire theory will be suppressed,
867
 
   except for the :FORWARD-CHAINING rule from the recognizer to TRUE-LISTP.
868
 
 
869
 
  :BINDING-EQUAL-RULE-CLASSES
870
 
 
871
 
   This option specifies a value for the :RULE-CLASSES keyword for the 
 
865
   except for the :FORWARD-CHAINING rule from the recognizer to TRUE-LISTP.</dd>
 
866
 
 
867
<dt>:BINDING-EQUAL-RULE-CLASSES</dt>
 
868
<dd>This option specifies a value for the :RULE-CLASSES keyword for the
872
869
   DEFTHM generated for the BINDING-EQUAL function (and for CDRASSOC) applied to
873
 
   an alist recognized by the DEFALIST recognizer.  The default is :REWRITE.
874
 
 
875
 
  :DOMAIN-TYPE
876
 
 
877
 
   This option specifies a predicate that recognizes a list of domain elements.
 
870
   an alist recognized by the DEFALIST recognizer.  The default is :REWRITE.</dd>
 
871
 
 
872
<dt>:DOMAIN-TYPE</dt>
 
873
<dd>This option specifies a predicate that recognizes a list of domain elements.
878
874
   It may be either a symbol or LAMBDA form. If present, and when not prevented
879
875
   by a :THEORY specification, a rewrite rule for the type of the domain
880
876
   will be generated. A lemma will be generated to check the compatibility
881
 
   of the specified domain type and domain element type.
882
 
 
883
 
  :RANGE-TYPE
884
 
 
885
 
   This option specifies a predicate that recognizes a list of range elements.
 
877
   of the specified domain type and domain element type.</dd>
 
878
 
 
879
<dt>:RANGE-TYPE</dt>
 
880
<dd>This option specifies a predicate that recognizes a list of range elements.
886
881
   It may be either a symbol or LAMBDA form. If present, and when not prevented
887
882
   by a :THEORY specification, a rewrite rule for the type of the range
888
883
   will be generated.  A lemma will be generated to check the compatibility
889
 
   of the specified range type and domain element type.
890
 
 
891
 
  :THEORY-NAME
892
 
 
893
 
   This option allows the user to define the name of the deftheory event
 
884
   of the specified range type and domain element type.</dd>
 
885
 
 
886
<dt>:THEORY-NAME</dt>
 
887
<dd>This option allows the user to define the name of the deftheory event
894
888
   that is automatically generated, and which includes the defthms that
895
 
   are generated. 
896
 
   ~/"
 
889
   are generated.</dd>")
 
890
 
 
891
(defmacro defalist (name formals &rest body)
897
892
  (let*
898
893
    ((syntax-err (defalist-check-syntax name formals body))
899
894
     (last-form (car (last body)))
923
918
                            ctx :BINDING-EQUAL-RULE-CLASSES option-list :FORM
924
919
                            :REWRITE :REWRITE))
925
920
     (domain-type (u::get-option-argument
926
 
                   ctx :DOMAIN-TYPE option-list :FORM 
 
921
                   ctx :DOMAIN-TYPE option-list :FORM
927
922
                   *defalist-true-fn*
928
923
                   *defalist-true-fn*))
929
924
     (range-type (u::get-option-argument
944
939
 
945
940
     ;; We always generate the alistp event.
946
941
 
947
 
     (let ((theory1 
 
942
     (let ((theory1
948
943
            (union-equal '(alistp)
949
944
                         (filter-alist-theory theory dom-elemtype ran-elemtype domain-type range-type))))
950
 
            
 
945
 
951
946
       `(ENCAPSULATE ()
952
947
 
953
948
                     ;; We do the definition and proofs in a minimal theory for speed.
966
961
                                           (,ran-elemtype (cdar ,l))
967
962
                                           (,name ,@(replace-equal l `(CDR ,l) formals))))))
968
963
                          ))
969
 
         
 
964
 
970
965
                     ,@(defalist-defthms
971
966
                         name formals dom-elemtype ran-elemtype domain-type range-type
972
967
                         guard theory1 binding-equal-rule-classes)
985
980
  (:options (:domain-type symbol-listp)
986
981
            (:range-type integer-listp)))
987
982
 
988
 
(defmacro naturalp (n) 
 
983
(defmacro naturalp (n)
989
984
  `(and (integerp ,n) (<= 0 ,n)))
990
985
 
991
986
(defun natural-listp (l)
992
987
  (if (atom l) t
993
988
    (and (naturalp (car l)) (natural-listp (cdr l)))))
994
 
 
 
989
 
995
990
(defalist symbol-to-natural-alistp (l)
996
991
  "Recognizes an alists mapping symbols to  naturals bounded by lub."
997
992
  (symbolp . naturalp)
999
994
            (:range-type natural-listp)
1000
995
            (:theory binding-equal)
1001
996
            (:theory-name sym->nat-theory)))
1002
 
 
 
997
 
1003
998
(defalist string-to-integer-alistp (l)
1004
 
  "Recognizes an alist mapping strings to integers. Produce a minimal 
 
999
  "Recognizes an alist mapping strings to integers. Produce a minimal
1005
1000
  theory, and store the BINDING-EQUAL lemma as a :TYPE-PRESCRIPTION."
1006
1001
  (stringp . integerp)
1007
1002
  (:options (:theory bind binding-equal bound?-equal)
1008
1003
            (:binding-equal-rule-classes :type-prescription)
1009
 
            (:domain-type string-listp) 
 
1004
            (:domain-type string-listp)
1010
1005
            (:range-type integer-listp)))
1011
1006
 
1012
1007
(defalist symbol-alistp (l)