← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/basic.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/basic.lisp
 
1
;;; basic.lisp
 
2
;;; Some stuff about lists, sets, sequences and association lists.
 
3
;;; Created: 6-8-99 Last revison: 05-12-2000
 
4
;;; =============================================================================
 
5
 
 
6
#| To certify this book:
 
7
 
 
8
(in-package "ACL2")
 
9
 
 
10
(certify-book "basic")
 
11
 
 
12
|#
 
13
 
 
14
 
 
15
(in-package "ACL2")
 
16
 
 
17
 
 
18
;;; *******************************************************************
 
19
;;; BASIC PROPERTIES ABOUT LISTS, SETS, SEQUENCES AND ASSOCIATION LISTS
 
20
;;; *******************************************************************
 
21
 
 
22
;;; REMARK: This is book is not intended to be a complete tratement of
 
23
;;; such data structures, but and "ad hoc" collection of definition and
 
24
;;; properties, needed for further development of the theory of first
 
25
;;; order terms.
 
26
 
 
27
;;; ============================================================================
 
28
;;; 1. Lists
 
29
;;; ============================================================================
 
30
 
 
31
 
 
32
;;; ======= APPEND
 
33
 
 
34
(defthm append-associative
 
35
  (equal (append (append x y) z)
 
36
         (append x (append y z))))
 
37
 
 
38
(defthm member-append
 
39
  (iff (member x (append a b))
 
40
       (or (member x a) (member x b))))
 
41
 
 
42
 
 
43
(defthm append-nil
 
44
  (implies (true-listp l)
 
45
           (equal (append l nil) l)))
 
46
 
 
47
 
 
48
;;; ======= REVLIST
 
49
 
 
50
(defun revlist (l)
 
51
  (if (endp l)
 
52
      nil
 
53
    (append (revlist (cdr l)) (list (car l)))))
 
54
 
 
55
(defthm revlist-true-listp
 
56
  (true-listp (revlist l)))
 
57
 
 
58
(local
 
59
 (defthm revappend-revlist
 
60
   (equal (revappend l m) (append (revlist l) m))))
 
61
 
 
62
(defthm reverse-revlist
 
63
  (implies (true-listp l)
 
64
           (equal (reverse l) (revlist l))))
 
65
 
 
66
;;; ====== DELETE-ONE
 
67
 
 
68
(defun delete-one (x l)
 
69
  (cond ((atom l) l)
 
70
        ((equal x (car l)) (cdr l))
 
71
        (t (cons (car l) (delete-one x (cdr l))))))
 
72
 
 
73
(defthm delete-one-less-length
 
74
  (implies (member x m)
 
75
           (< (len (delete-one x m)) (len m))))
 
76
 
 
77
(defthm member-delete-one
 
78
  (implies (and (member x m) (not (equal x y)))
 
79
           (member x (delete-one y m))))
 
80
 
 
81
(defthm delete-one-conmute
 
82
  (equal (delete-one x (delete-one y l))
 
83
         (delete-one y (delete-one x l))))
 
84
 
 
85
(defthm subsetp-delete-one
 
86
  (implies (not (member x l))
 
87
           (not (member x (delete-one y l)))))
 
88
 
 
89
;;; ======= ELIMINATE (like remove, but different guard, using equal) 
 
90
 
 
91
(defun eliminate (x l)
 
92
  (declare (xargs :guard (true-listp l)))
 
93
  (cond ((endp l) nil)
 
94
        ((equal x (car l)) (eliminate x (cdr l)))
 
95
        (t (cons (car l) (eliminate x (cdr l))))))
 
96
 
 
97
 
 
98
(defthm eliminate-len
 
99
  (implies (member x l)
 
100
           (< (len (eliminate x l)) (len l)))
 
101
  :rule-classes :linear)
 
102
 
 
103
;;; ====== NATURAL-TRUE-LISTP
 
104
(defun positive-integer-true-listp (l)
 
105
  (declare (xargs :guard t))
 
106
  (if (atom l)
 
107
      (equal l nil)
 
108
    (and (integerp (car l)) (> (car l) 0)
 
109
         (positive-integer-true-listp (cdr l)))))
 
110
 
 
111
;;; ====== REPLACE-LIST
 
112
 
 
113
(defun replace-list (l n x)
 
114
  (declare (xargs :guard
 
115
                  (and (true-listp l) (integerp n) (>= n 0))))
 
116
  (if (endp l)
 
117
      nil
 
118
    (if (zp n)
 
119
        (cons x (cdr l))
 
120
      (cons (car l) (replace-list (cdr l) (- n 1) x))))) 
 
121
 
 
122
 
 
123
(defthm nth-replace-list-same-position
 
124
  (implies (and (integerp i)
 
125
                (<= 0 i)
 
126
                (< i (len l)))
 
127
           (equal (nth i (replace-list l i x)) x)))
 
128
 
 
129
 
 
130
(defthm replace-list-same-length
 
131
  (equal (len (replace-list l i x)) (len l)))
 
132
 
 
133
 
 
134
(defthm nth-replace-list-different-position
 
135
  (implies (and (integerp i) (integerp k)
 
136
                (<= 0 i) (<= 0 k)
 
137
                (< i (len l)) (< k (len l))
 
138
                (not (equal i k)))
 
139
           (equal (nth i (replace-list l k x)) (nth i l))))
 
140
 
 
141
 
 
142
 
 
143
 
 
144
(defthm replace-list-different-position
 
145
  (implies (and (integerp i) (integerp k)
 
146
                (<= 0 i) (<= 0 k)
 
147
                (< i (len l)) (< k (len l))
 
148
                (not (equal i k)))
 
149
           (equal
 
150
            (replace-list (replace-list l i x) k y)
 
151
            (replace-list (replace-list l k y) i x))))
 
152
 
 
153
 
 
154
 
 
155
(defthm replace-list-same-position
 
156
  (implies (and (integerp i)
 
157
                (<= 0 i)
 
158
                (< i (len term)))
 
159
           (equal
 
160
            (replace-list (replace-list term i x) i y)
 
161
            (replace-list term i y)))) 
 
162
 
 
163
 
 
164
 
 
165
 
 
166
 
 
167
;;; ====== PAIR-ARGS
 
168
 
 
169
(defun pair-args (l1 l2)
 
170
  (declare (xargs :guard (and (true-listp l1) (true-listp l2))))
 
171
  (cond ((endp l1) (if (equal l1 l2) (mv nil t) (mv nil nil)))
 
172
        ((endp l2) (mv nil nil))
 
173
        (t (mv-let (pair-rest bool)
 
174
                   (pair-args (cdr l1) (cdr l2))       
 
175
                   (if bool
 
176
                       (mv (cons (cons (car l1) (car l2))
 
177
                                 pair-rest)
 
178
                           t)
 
179
                     (mv nil nil))))))
 
180
 
 
181
;;; **** Guard verification
 
182
(defthm pair-args-true-listp
 
183
  (true-listp (car (pair-args l1 l2))))
 
184
 
 
185
 
 
186
;;; ======= MV-NTH
 
187
 
 
188
;;; REMARK: I prefer to deal with first,second, third, etc... than with
 
189
;;; mv-nth. 
 
190
 
 
191
(defthm mv-nth-0-first
 
192
  (equal (mv-nth 0 l) (first l)))
 
193
 
 
194
(defthm mv-nth-1-second
 
195
  (equal (mv-nth 1 l) (second l)))
 
196
 
 
197
(defthm mv-nth-2-third
 
198
  (equal (mv-nth 2 l) (third l)))
 
199
 
 
200
(defthm mv-nth-3-fourth
 
201
  (equal (mv-nth 3 l) (fourth l)))
 
202
 
 
203
;;; and so on...
 
204
 
 
205
 
 
206
;;; ============================================================================
 
207
;;; 2. Sets
 
208
;;; ============================================================================
 
209
 
 
210
;;; ====== SETP
 
211
;;; A true-list without repeated elements.
 
212
 
 
213
(defun setp (l)
 
214
  (if (atom l)
 
215
      t
 
216
    (and (not (member (car l) (cdr l)))
 
217
         (setp (cdr l)))))
 
218
 
 
219
(encapsulate
 
220
 ()
 
221
 (local (defthm member-eliminate
 
222
          (implies (member y (eliminate x l))
 
223
                   (member y l))))
 
224
 
 
225
 (defthm eliminate-preserves-setp
 
226
  (implies (setp l)
 
227
           (setp (eliminate x l)))))
 
228
 
 
229
 
 
230
 
 
231
 
 
232
;;; ====== SUBSETP
 
233
 
 
234
(defun not-subsetp-witness (l1 l2)
 
235
  (if (atom l1)
 
236
      nil
 
237
      (if (member (car l1) l2)
 
238
          (not-subsetp-witness (cdr l1) l2)
 
239
        (car l1))))
 
240
 
 
241
(defthm not-subsetp-witness-lemma 
 
242
  (equal (subsetp l1 l2)
 
243
         (implies  (member (not-subsetp-witness l1 l2) l1)
 
244
                   (member (not-subsetp-witness l1 l2) l2))))
 
245
 
 
246
 
 
247
(in-theory (disable not-subsetp-witness-lemma))
 
248
 
 
249
(defthm subsetp-append-1 
 
250
  (equal (subsetp (append x y) z)
 
251
         (and (subsetp x z) (subsetp y z))))
 
252
 
 
253
(defthm subsetp-append-2 
 
254
  (implies (subsetp c a)
 
255
           (subsetp c (append b a))))
 
256
 
 
257
(defthm subsetp-append-3 
 
258
  (implies (subsetp b c)
 
259
           (subsetp b (append c a))))
 
260
 
 
261
 
 
262
(defthm subsetp-cons
 
263
  (implies (subsetp l m)
 
264
           (subsetp l (cons x m))))
 
265
 
 
266
(defthm subsetp-reflexive
 
267
  (subsetp l l))
 
268
 
 
269
(defthm delete-one-subsetp
 
270
  (subsetp (delete-one x l) l))
 
271
 
 
272
(defun subset-induction (l m)
 
273
  (if (or (atom l) (atom m) (not (member (car l) m)))
 
274
      t
 
275
    (subset-induction (cdr l) (eliminate (car l) m))))
 
276
 
 
277
(defthm
 
278
   substp-preserved-when-deleting-a-non-member
 
279
   (implies (and (subsetp z m) (not (member x z)))
 
280
            (subsetp z (eliminate x m))))
 
281
 
 
282
 
 
283
;;; ====== DISJOINTP
 
284
 
 
285
;;; No common elements
 
286
 
 
287
(defun disjointp (l1 l2)
 
288
  (if (endp l1)
 
289
      t
 
290
    (and (not (member (car l1) l2))
 
291
         (disjointp (cdr l1) l2))))
 
292
 
 
293
 
 
294
(defthm disjointp-cons 
 
295
  (equal (disjointp l (cons x m))
 
296
         (and (not (member x l))
 
297
              (disjointp l m))))
 
298
 
 
299
(defthm disjointp-append-1 
 
300
  (equal (disjointp (append l m) n)
 
301
         (and (disjointp l n)
 
302
              (disjointp m n))))
 
303
 
 
304
(defthm disjointp-append-2 
 
305
  (equal (disjointp m (append l n))
 
306
         (and (disjointp m l)
 
307
              (disjointp m n))))
 
308
 
 
309
(defthm disjointp-conmutative 
 
310
  (equal (disjointp l1 l2) (disjointp l2 l1)))
 
311
 
 
312
(defthm disjointp-nil
 
313
  (disjointp x nil))
 
314
 
 
315
 
 
316
 
 
317
;;; ======= MAKE-SET
 
318
;;; Eliminate duplicates.
 
319
 
 
320
(defun make-set (l)
 
321
  (if (atom l)
 
322
      nil
 
323
    (if (member (car l) (cdr l))
 
324
        (make-set (cdr l))
 
325
      (cons (car l) (make-set (cdr l))))))
 
326
 
 
327
(defthm member-make-set
 
328
  (iff (member x (make-set l)) (member x l)))
 
329
 
 
330
(defthm setp-make-set 
 
331
  (setp (make-set x)))
 
332
 
 
333
(defthm make-set-of-a-setp-is-the-same 
 
334
  (implies (setp l)
 
335
           (equal (make-set l) (fix-true-list l))))
 
336
 
 
337
(defthm len-fix-true-list
 
338
  (equal (len (fix-true-list l)) (len l)))
 
339
 
 
340
(defthm make-set-lessp-length-if-not-setp
 
341
  (implies (not (setp l))
 
342
           (< (len (make-set l))
 
343
              (len l)))
 
344
  :rule-classes :linear)
 
345
           
 
346
 
 
347
(defthm length-make-set-leq 
 
348
  (>= (len l)
 
349
      (len (make-set l)))
 
350
  :rule-classes :linear)
 
351
 
 
352
(defthm make-set-fix-true-list
 
353
  (equal (fix-true-list (make-set l)) (make-set l)))
 
354
 
 
355
 
 
356
;;; ============ EQUAL-SET: CONGRUENCE AND REWRITE RULES
 
357
 
 
358
(defun equal-set (x y)
 
359
  (and (subsetp x y) (subsetp y x)))
 
360
 
 
361
           
 
362
(defthm subsetp-transitive
 
363
  (implies (and (subsetp l m)
 
364
                (subsetp m n))
 
365
           (subsetp l n)))
 
366
 
 
367
 
 
368
(defequiv equal-set)
 
369
 
 
370
 
 
371
(defcong equal-set iff (subsetp x y) 1)
 
372
(defcong equal-set iff (subsetp x y) 2)
 
373
(defcong equal-set equal (consp l) 1)
 
374
 
 
375
(encapsulate
 
376
 ()
 
377
 (local
 
378
  (defthm subsetp-disjoint-1
 
379
    (implies (and (subsetp x x-equiv)
 
380
                  (disjointp x-equiv y))
 
381
             (disjointp x y))))
 
382
 
 
383
 (defcong equal-set iff (disjointp x y) 1))
 
384
 
 
385
(encapsulate
 
386
 ()
 
387
 (local
 
388
  (defthm subsetp-disjoint-2
 
389
    (implies (and (subsetp y y-equiv)
 
390
                  (disjointp x y-equiv))
 
391
             (disjointp x y))))
 
392
 
 
393
 (defcong equal-set iff (disjointp x y) 2))
 
394
 
 
395
 
 
396
(encapsulate
 
397
 ()
 
398
 (local (defthm equal-set-member-cong-lemma-1
 
399
          (implies (and (not (member x y))
 
400
                        (subsetp y-equiv y))
 
401
                   (not (member x y-equiv)))))
 
402
 
 
403
 (local (defthm equal-set-member-cong-lemma-2
 
404
          (implies (and (member x y)
 
405
                        (subsetp y y-equiv))
 
406
                   (member x y-equiv))))
 
407
 (defcong equal-set iff (member x y) 2))
 
408
 
 
409
 
 
410
(defthm equal-set-make-set
 
411
  (equal-set (make-set l) l))
 
412
 
 
413
;;; REMARK: The following rule is needed in
 
414
;;; equal-size-and-not-inverse-subsumption-implies-not-renaming-almost  
 
415
;;; I don't know why the previous rule is not used (monitoring is not
 
416
;;; possible, because it is a "simple"(?) rule). So I think I need the
 
417
;;; following rule, which is redundant (?) 
 
418
 
 
419
 
 
420
(defthm subsetp-make-set-provisional
 
421
  (iff (subsetp a (make-set b)) (subsetp a b)))
 
422
 
 
423
 
 
424
 
 
425
 
 
426
;;; ====== PERM: CONGRUENCE AND REWRITE RULES
 
427
 
 
428
 
 
429
(defun perm (lst1 lst2)
 
430
  (cond ((atom lst1) (atom lst2))
 
431
        ((member (car lst1) lst2)
 
432
         (perm (cdr lst1) (delete-one (car lst1) lst2)))
 
433
        (t nil)))
 
434
 
 
435
 
 
436
(encapsulate
 
437
 ()
 
438
 
 
439
 (defthm perm-reflexive
 
440
  (perm x x))
 
441
 
 
442
 (local
 
443
  (defthm perm-main-lemma 
 
444
    (implies (and (member x a)
 
445
                  (member x b)
 
446
                  (perm (delete-one x a) (delete-one x b)))
 
447
             (perm a b))))
 
448
 
 
449
 (local
 
450
  (defthm perm-symmetric
 
451
    (implies (perm x y) (perm y x))))
 
452
        
 
453
 
 
454
 (local
 
455
  (defthm perm-transitive-reverse
 
456
    (implies (and (perm a b)
 
457
                  (perm a c))
 
458
             (perm b c))
 
459
    :rule-classes nil))
 
460
 
 
461
 (local 
 
462
  (defthm perm-transitive
 
463
    (implies (and (perm a b)
 
464
                  (perm b c))
 
465
             (perm a c))
 
466
  :hints (("Goal" :use
 
467
           ((:instance perm-symmetric
 
468
                       (x a) (y b))
 
469
            (:instance perm-transitive-reverse
 
470
                       (a b) (b a)))))))
 
471
 (defequiv perm))
 
472
 
 
473
 
 
474
 
 
475
(local (defthm perm-implies-subsetp
 
476
         (implies (perm x y) (subsetp x y))
 
477
         :hints (("Goal" :induct (perm x y)))))
 
478
 
 
479
 
 
480
(defrefinement perm equal-set)
 
481
 
 
482
;;; Rewriting rules
 
483
 
 
484
(defthm perm-fix-true-list
 
485
  (perm (fix-true-list l) l))
 
486
 
 
487
 
 
488
;;; ============================================================================
 
489
;;; 3. Sequences 
 
490
;;; ============================================================================
 
491
 
 
492
;;; Sequences of natural numbers will be used to represent positions of
 
493
;;; terms. 
 
494
 
 
495
;;; ===== PREFIX
 
496
 
 
497
(defun prefix (p1 p2)
 
498
  (cond ((endp p1) t)
 
499
        ((endp p2) nil)
 
500
        ((equal (car p1) (car p2))
 
501
         (prefix (cdr p1) (cdr p2)))
 
502
        (t nil)))
 
503
 
 
504
;;; ===== DIFFERENCE-POS
 
505
 
 
506
(defun difference-pos (p q)
 
507
  (if (atom p)
 
508
      q
 
509
    (difference-pos (cdr p) (cdr q))))
 
510
 
 
511
 
 
512
(defthm difference-the-same
 
513
  (implies (true-listp l)
 
514
           (equal (difference-pos l l) nil)))
 
515
 
 
516
(defthm difference-pos-common-prefix
 
517
  (equal (difference-pos l (append l m))
 
518
         m))
 
519
 
 
520
(defthm difference-pos-common-prefix-append
 
521
  (equal (difference-pos (append l m) (append l n))
 
522
         (difference-pos m n)))
 
523
 
 
524
 
 
525
;;; ===== DISJOINT-POSITIONS
 
526
 
 
527
(defun disjoint-positions (p1 p2)
 
528
  (cond
 
529
   ((or (endp p1) (endp p2)) nil)
 
530
   ((equal (car p1) (car p2))
 
531
    (disjoint-positions (cdr p1) (cdr p2)))
 
532
   (t t)))
 
533
 
 
534
 
 
535
 
 
536
;;; ============================================================================
 
537
;;; 4. Association lists
 
538
;;; ============================================================================
 
539
 
 
540
 
 
541
;;; REMARK: Association lists represent finite domain functions in the
 
542
;;; following way: 
 
543
;;; - Every atom object represents the identity function.
 
544
;;; - If an atom object is member of an association list will be
 
545
;;; considered as (nil . nil).
 
546
;;; - If several pairs (x . t1), (x . t2),... are member of an
 
547
;;; association list only the first one is considered.
 
548
;;; As a consecuence of this representation, different objects represent
 
549
;;; the same finite domain function. Thus, we cannot use equal as a
 
550
;;; predicate to talk about equality of finite domain functions.
 
551
 
 
552
;;; REMARK: We do not use the book alist-theory.list 
 
553
;;; provided by the distribution because we need our own version of
 
554
;;; assoc (see the function val). We want the association list to behave
 
555
;;; like identity outside its domain.
 
556
 
 
557
;;; ======= VAL
 
558
;;; (i.e., sigma(x))
 
559
 
 
560
(defun val (x sigma)
 
561
  (declare (xargs :guard (if (eqlablep x)
 
562
                             (alistp sigma)
 
563
                             (eqlable-alistp sigma))))
 
564
  (if (endp sigma)
 
565
      x
 
566
    (if (eql x (caar sigma)) (cdar sigma) (val x (cdr sigma)))))
 
567
 
 
568
#||
 
569
; [Removed by Matt K. to handle changes to member, assoc, etc. after ACL2 4.2.]
 
570
 
 
571
;;; REMARK: For execution, I will use assoc when the variable is in the
 
572
;;; domain. Sometimes, I have to use assoc-equal (see renamings.lisp).
 
573
;;; The following rule rewrites assoc-equal to assoc. In this way, we
 
574
;;; can build one set of rules about assoc.  WARNING: this is different
 
575
;;; rewriting strategy than the one given in the book alist-defthms.lisp
 
576
;;; in the ACL2 distribution.
 
577
 
 
578
(defthm assoc-equal-assoc-equal
 
579
  (equal (assoc-equal x a) (assoc x a)))
 
580
||#
 
581
 
 
582
 
 
583
;;; This relation between val and assoc is expressed
 
584
;;; here. For reasonig, I prefer to use val (that's the explanation for
 
585
;;; the orientation of the following rule):
 
586
(defthm assoc-val
 
587
         (implies (assoc x l)
 
588
                  (equal (cdr (assoc x l)) (val x l)))) 
 
589
 
 
590
;;; ====== RESTRICTION
 
591
;;; The list of pairs (x. sigma(x)), for all x in l.
 
592
      
 
593
(defun restriction (sigma l)
 
594
  (if (atom l)
 
595
      l
 
596
    (cons (cons (car l) (val (car l) sigma))
 
597
          (restriction sigma (cdr l)))))
 
598
 
 
599
;;; ====== DOMAIN
 
600
;;; domain of association lists (the list of first components of sigma).
 
601
;;; Note: as we said above, the atom elements of sigma are considered
 
602
;;; as (nil . nil). This remark also applies to the following definitions. 
 
603
 
 
604
(defun domain (sigma)
 
605
  (declare (xargs :guard (alistp sigma)))
 
606
  (if (endp sigma)
 
607
      nil
 
608
    (cons (caar sigma) (domain (cdr sigma)))))
 
609
 
 
610
 
 
611
(defthm domain-restriction 
 
612
  (equal (domain (restriction sigma l)) (fix-true-list l)))
 
613
 
 
614
 
 
615
(defthm domain-append
 
616
  (equal (domain (append l1 l2))
 
617
         (append (domain l1) (domain l2))))
 
618
 
 
619
(defthm consp-domain
 
620
   (equal (consp (domain sigma))
 
621
          (consp sigma)))
 
622
 
 
623
 
 
624
(defthm assoc-member-domain
 
625
  (implies (alistp sigma)
 
626
           (iff (member x (domain sigma))
 
627
                (assoc x sigma))))
 
628
 
 
629
 
 
630
;;; ====== CO-DOMAIN
 
631
;;; co-domain of association lists (the list of first components of sigma).
 
632
 
 
633
(defun co-domain (sigma)
 
634
  (if (atom sigma)
 
635
      nil               
 
636
    (cons (cdar sigma) (co-domain (cdr sigma)))))
 
637
 
 
638
 
 
639
 
 
640
;;; ====== INVERSE
 
641
;;; The association list obtained reversing the pairs.
 
642
 
 
643
(defun inverse (sigma)
 
644
  (if (atom sigma)
 
645
      nil
 
646
    (cons (cons (cdar sigma) (caar sigma))
 
647
          (inverse (cdr sigma)))))
 
648
 
 
649
 
 
650
(defthm domain-of-inverse-is-co-domain 
 
651
  (equal (domain (inverse sigma)) (co-domain sigma)))
 
652
 
 
653
(defthm co-domain-of-inverse-is-domain 
 
654
  (equal (co-domain (inverse sigma)) (domain sigma)))
 
655
 
 
656
(defthm same-length-co-domain-and-domain 
 
657
  (equal (len (domain sigma))
 
658
         (len (co-domain sigma))))
 
659
 
 
660
(in-theory (disable same-length-co-domain-and-domain))
 
661
 
 
662
 
 
663
 
 
664
;;; ====== ALISTP (for guard verification)
 
665
 
 
666
(defthm assoc-consp-or-nil
 
667
  (implies (alistp a)
 
668
           (or (consp (assoc x a))
 
669
               (equal (assoc x a) nil)))
 
670
  :rule-classes :type-prescription)
 
671
 
 
672
 
 
673
(defun alistp-acl2-numberp (l)
 
674
  (declare (xargs :guard t))
 
675
  (if (atom l)
 
676
      (equal l nil)
 
677
    (and (consp (car l)) (acl2-numberp (cdar l))
 
678
         (alistp-acl2-numberp (cdr l)))))
 
679