← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/data-structures/list-defthms.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/list-defthms.lisp
85
85
;   (iff (no-duplicatesp-eq l)
86
86
;        (no-duplicatesp-equal l)))
87
87
 
88
 
(local 
 
88
(local
89
89
 (defthm occurrences-ac->occurrences-equal-ac
90
90
   (equal (occurrences-ac x l ac)
91
91
          (occurrences-equal-ac x l ac))))
94
94
  (equal (occurrences x l)
95
95
         (occurrences-equal x l)))
96
96
 
97
 
(local 
 
97
(local
98
98
 (defthm occurrences-eq-ac->occurrences-equal-ac
99
99
   (equal (occurrences-eq-ac x l ac)
100
100
          (occurrences-equal-ac x l ac))))
104
104
         (occurrences-equal x l)))
105
105
 
106
106
; [Removed by Matt K. to handle changes to member, assoc, etc. after ACL2 4.2.]
107
 
; (local 
 
107
; (local
108
108
;  (defthm position-ac->position-equal-ac
109
109
;    (equal (position-ac x l ac)
110
110
;           (position-equal-ac x l ac))))
115
115
;          (position-equal x l)))
116
116
 
117
117
; [Removed by Matt K. to handle changes to member, assoc, etc. after ACL2 4.2.]
118
 
; (local 
 
118
; (local
119
119
;  (defthm position-eq-ac->position-equal-ac
120
120
;    (equal (position-eq-ac x l ac)
121
121
;           (position-equal-ac x l ac))))
143
143
                       (implies (consp b)
144
144
                                (consp (append a b))))))
145
145
 
146
 
(defthm consp-revappend 
 
146
(defthm consp-revappend
147
147
  (equal (consp (revappend a b))
148
148
         (or (consp a)
149
149
             (consp b)))
165
165
                       (implies (consp a)
166
166
                                (consp (reverse a))))))
167
167
 
168
 
(local 
 
168
(local
169
169
 (defthm consp-first-n-ac
170
170
   (equal (consp (first-n-ac i l ac))
171
171
          (if (zp i) (consp ac) t))
176
176
                                               (consp (first-n-ac i l ac)))))
177
177
   :hints (("Goal" :induct (first-n-ac i l ac)))))
178
178
 
179
 
(local 
 
179
(local
180
180
 (defthm consp-take
181
181
   (equal (consp (take n l))
182
182
          (not (zp n)))
239
239
                           (iff (not (consp (member-equal x l)))
240
240
                                (equal (member-equal x l) nil)))))
241
241
 
242
 
(local 
 
242
(local
243
243
 (defthm nthcdr-nil
244
244
   (implies (and (integerp n)
245
245
                 (<= 0 n))
292
292
                    (and (integerp end)
293
293
                         (<= 0 end))))
294
294
           (iff (consp (subseq list start end))
295
 
                (< start (if (null end) 
 
295
                (< start (if (null end)
296
296
                             (len list)
297
297
                           end))))
298
298
  :hints (("Goal" :do-not-induct t :in-theory (disable take))))
299
299
 
300
300
;; UPDATE-NTH is always a CONS
301
 
                         
 
301
 
302
302
; ------------------------------------------------------------
303
303
; TRUE-LISTP type prescription and rewrite rules
304
304
; ------------------------------------------------------------
336
336
     :rule-classes (:rewrite :type-prescription)
337
337
     :hints (("Goal" :induct (first-n-ac i l ac)))))
338
338
 
339
 
(local 
 
339
(local
340
340
 (defthm true-listp-take
341
341
   (true-listp (take n l))
342
342
   :rule-classes (:rewrite :type-prescription)))
387
387
           (true-listp (put-seg i seg l)))
388
388
  :rule-classes (:rewrite :type-prescription))
389
389
 
390
 
(local 
 
390
(local
391
391
 (defthm true-listp-subseq-list
392
392
   (true-listp (subseq-list lst start end))
393
393
   :hints (("Goal" :do-not-induct t :in-theory (disable take)))
405
405
; NATURALP type prescription rules
406
406
; ------------------------------------------------------------
407
407
 
408
 
(local 
 
408
(local
409
409
   (defthm naturalp-occurrences-equal-ac
410
410
     (implies (and (integerp acc) (<= 0 acc))
411
411
              (and (integerp (occurrences-equal-ac item lst acc))
434
434
; Some support lemmas
435
435
; We use these lemmas to define non-recursive forms for some
436
436
; recursive functions. These non-recursive forms are easier to
437
 
; reason about at times.                                        ; 
 
437
; reason about at times.                                        ;
438
438
; ------------------------------------------------------------
439
439
 
440
440
(local
468
468
  :rule-classes :forward-chaining)
469
469
 
470
470
 
471
 
(defthm len-append 
 
471
(defthm len-append
472
472
  (equal (len (append a b))
473
473
         (+ (len a) (len b))))
474
474
 
475
 
(defthm len-revappend 
 
475
(defthm len-revappend
476
476
  (equal (len (revappend a b))
477
477
         (+ (len a) (len b))))
478
478
 
479
 
(defthm len-reverse 
 
479
(defthm len-reverse
480
480
  (equal (len (reverse a)) (len a)))
481
481
 
482
 
(local 
 
482
(local
483
483
   (defthm len-first-n-ac
484
484
     (equal (len (first-n-ac n l ac))
485
485
            (+ (nfix n) (len ac)))
486
486
     :hints (("Goal" :induct (first-n-ac n l ac)))))
487
487
 
488
 
(local 
 
488
(local
489
489
 (defthm len-take
490
490
   (equal (len (take n l)) (nfix n))))
491
491
 
495
495
                  (if (<= (len lst) n)
496
496
                      0
497
497
                    (- (len lst) n))))
498
 
  :hints (("Goal" :do-not-induct t 
 
498
  :hints (("Goal" :do-not-induct t
499
499
           :in-theory (disable take))))
500
500
 
501
501
(defthm len-firstn
505
505
             (len l)))
506
506
  :hints (("Goal" :induct (firstn n l))))
507
507
 
508
 
(defthm len-last 
 
508
(defthm len-last
509
509
  (equal (len (last l))
510
510
         (if (consp l)
511
511
             1
548
548
                (not (< i 0)))
549
549
           (equal (len (put-seg i seg l))
550
550
                  (len l))))
551
 
  
 
551
 
552
552
(local
553
553
   (defthm occurrences-equal-ac+1
554
554
     (implies (acl2-numberp ac)
572
572
           (- (len l) (occurrences-equal x l)))
573
573
    :hints (("Goal" :do-not-induct t
574
574
             :use ((:instance len-remove-equal-ac (ac 0))))))
575
 
  
 
575
 
576
576
(defthm len-subseq
577
577
  (implies (and (true-listp l)
578
578
                (integerp start) (<= 0 start)
591
591
             (len l)
592
592
           (+ 1 (nfix n))))
593
593
  :hints (("Goal" :induct (update-nth n val l))))
594
 
         
 
594
 
595
595
; ------------------------------------------------------------
596
596
; LEN inequalities
597
597
; ------------------------------------------------------------
602
602
              (not (< (+ (len l) ac) (occurrences-equal-ac x l ac))))
603
603
     :rule-classes nil))
604
604
 
605
 
(defthm leq-occurrences-equal-len 
 
605
(defthm leq-occurrences-equal-len
606
606
    (not (< (len l) (occurrences-equal x l)))
607
607
    :rule-classes (:rewrite :linear)
608
608
    :hints (("Goal" :do-not-induct t
614
614
              (not (< (+ (len l) ac) (position-equal-ac x l ac))))
615
615
     :rule-classes nil))
616
616
 
617
 
(defthm leq-position-equal-len 
 
617
(defthm leq-position-equal-len
618
618
    (implies (member-equal x l)
619
619
             (not (< (len l) (position-equal x l))))
620
620
    :rule-classes (:rewrite :linear)
637
637
(defthm associativity-of-append
638
638
  (equal (append (append a b) c)
639
639
         (append a (append b c))))
640
 
 
 
640
 
641
641
(defthm append-firstn-nthcdr
642
642
  (implies (true-listp l)
643
643
           (equal (append (firstn n l) (nthcdr n l)) l)))
689
689
    (implies (true-listp l)
690
690
             (equal (take (len l) l) l))))
691
691
 
692
 
(local 
 
692
(local
693
693
   (defthm first-n-ac-append1
694
694
     (implies (<= n (len a))
695
695
              (equal (first-n-ac n (append a b) ac)
696
696
                     (first-n-ac n a ac)))
697
697
     :hints (("Goal" :induct (first-n-ac n a ac))))   )
698
698
 
699
 
(local 
 
699
(local
700
700
 (defthm take-append1
701
701
   (implies (<= n (len a))
702
702
            (equal (take n (append a b))
703
703
                   (take n a)))
704
704
   :hints (("Goal" :do-not-induct t))))
705
 
  
 
705
 
706
706
 
707
707
(defthm butlast-append1-crock
708
708
    (IMPLIES (and (TRUE-LISTP A)
718
718
    :hints (("Goal" :do-not-induct t
719
719
             :use ((:instance butlast-append1-crock (i (len b))))
720
720
             :in-theory (disable take))))
721
 
  
 
721
 
722
722
 
723
723
; ------------------------------------------------------------
724
724
; FIRSTN
728
728
  (implies (and (<= (len l) (nfix n))
729
729
                (true-listp l))
730
730
           (equal (firstn n l) l)))
731
 
                
 
731
 
732
732
(defthm firstn-append
733
733
  (equal (firstn n (append a b))
734
734
         (if (<= (nfix n) (len a))
735
735
             (firstn n a)
736
736
             (append a (firstn (- n (len a)) b)))))
737
737
 
738
 
(defthm firstn-firstn 
 
738
(defthm firstn-firstn
739
739
  (equal (firstn i (firstn j l))
740
740
         (if (< (nfix i) (nfix j))
741
741
             (firstn i l)
747
747
             (make-list-ac i v nil)
748
748
             (make-list-ac j v (firstn (- i (nfix j)) ac)))))
749
749
 
750
 
(local 
751
 
   (defthm firstn-cons 
 
750
(local
 
751
   (defthm firstn-cons
752
752
     (equal (firstn n (cons a l))
753
753
            (if (zp n)
754
754
                nil
755
755
              (cons a (firstn (1- n) l))))))
756
756
 
757
 
(defthm firstn-put-nth 
 
757
(defthm firstn-put-nth
758
758
    (equal (firstn i (put-nth j v l))
759
759
           (if (<= (nfix i) (nfix j))
760
760
               (firstn i l)
764
764
               (implies (<= (nfix i) (nfix j))
765
765
                        (equal (firstn i (put-nth j v l))
766
766
                               (firstn i l))))))
767
 
  
 
767
 
768
768
; ------------------------------------------------------------
769
769
; MEMBER
770
770
; ------------------------------------------------------------
771
771
 
772
 
(defthm member-equal-append 
 
772
(defthm member-equal-append
773
773
  (iff (member-equal x (append a b))
774
774
       (or (member-equal x a)
775
775
           (member-equal x b))))
842
842
; MEMBERP
843
843
; ------------------------------------------------------------
844
844
 
845
 
(defthm memberp-equal-append 
 
845
(defthm memberp-equal-append
846
846
  (iff (memberp-equal x (append a b))
847
847
       (or (memberp-equal x a)
848
848
           (memberp-equal x b))))
922
922
(defthm nth-of-nil
923
923
  (equal (nth n nil) nil))
924
924
 
925
 
(defthm nth-with-large-index 
 
925
(defthm nth-with-large-index
926
926
  (implies (<= (len l) (nfix n))
927
927
           (equal (nth n l) nil)))
928
928
 
939
939
           (nth (- (nfix n) (len a)) b)))
940
940
  :hints (("Goal" :induct (revappend a b))))
941
941
 
942
 
(defthm nth-reverse 
 
942
(defthm nth-reverse
943
943
  (implies (and (integerp n)
944
944
                (<= 0 n))
945
945
           (equal (nth n (reverse a))
950
950
;; In the following event we show how NTH interacts with TAKE, BUTLAST
951
951
;; and SUBSEQ. The proof strategy is to rewrite the basic FIRST-N-AC
952
952
;; term into one involving REVAPPEND and a version of firstn called
953
 
;; XFIRSTN. 
 
953
;; XFIRSTN.
954
954
 
955
955
 
956
956
(defun xfirstn (n l)
999
999
  :hints (("Goal" :do-not-induct t)))
1000
1000
 
1001
1001
(defthm nth-butlast
1002
 
    (implies (and (integerp i) 
 
1002
    (implies (and (integerp i)
1003
1003
                  (<= 0 i)
1004
 
                  (integerp n) 
 
1004
                  (integerp n)
1005
1005
                  (<= 0 n))
1006
1006
             (equal (nth i (butlast l n))
1007
1007
                    (if (< i (- (len l) n))
1031
1031
  (equal (nth i (nthcdr j l))
1032
1032
         (nth (+ (nfix j) (nfix i)) l)))
1033
1033
 
1034
 
(defthm nth-subseq 
 
1034
(defthm nth-subseq
1035
1035
    (implies (and (true-listp l)
1036
1036
                  (integerp start) (<= 0 start)
1037
1037
                  (or (and (integerp end) (<= start end))
1047
1047
; Apologia:  See nth-butlast.
1048
1048
 
1049
1049
             :in-theory (disable revappend))))
1050
 
  
1051
 
  
 
1050
 
 
1051
 
1052
1052
(defthm nth-firstn
1053
1053
  (equal (nth i (firstn j l))
1054
1054
         (if (< (nfix i) (nfix j))
1135
1135
                (true-listp l))
1136
1136
           (equal (nthcdr n l) nil)))
1137
1137
 
1138
 
(defthm nthcdr-append 
 
1138
(defthm nthcdr-append
1139
1139
  (equal (nthcdr n (append a b))
1140
1140
         (if (<= (nfix n) (len a))
1141
1141
             (append (nthcdr n a) b)
1196
1196
         ((eql x (car l)) (1+ (xoccurrences-equal x (cdr l))))
1197
1197
         (t (xoccurrences-equal x (cdr l))))))
1198
1198
 
1199
 
(local 
 
1199
(local
1200
1200
 (defthm occurrences-equal-ac-equals-xoccurrences-equal
1201
1201
   (implies (integerp ac)
1202
1202
            (equal (occurrences-equal-ac x l ac)
1205
1205
;; Throughout the rest of this script, we'll take the strategy of
1206
1206
;; proving facts about POSITION by first proving the fact about XPOSITION.
1207
1207
 
1208
 
(local 
 
1208
(local
1209
1209
 (defun xposition-equal (x l)
1210
1210
   (declare (xargs :guard (and (true-listp l)
1211
1211
                               (or (symbolp x) (symbol-listp l)))))
1237
1237
; OCCURRENCES
1238
1238
; ------------------------------------------------------------
1239
1239
 
1240
 
(local 
1241
 
   (defthm equal-occurrences-equal-ac-zero 
 
1240
(local
 
1241
   (defthm equal-occurrences-equal-ac-zero
1242
1242
     (implies (and (not (member-equal x l))
1243
1243
                   (integerp acc))
1244
1244
              (equal (occurrences-equal-ac x l acc)
1245
1245
                     acc))))
1246
1246
 
1247
 
(defthm equal-occurrences-equal-zero 
 
1247
(defthm equal-occurrences-equal-zero
1248
1248
  (implies (not (member-equal x l))
1249
1249
           (equal (occurrences-equal x l)
1250
1250
                  0)))
1260
1260
                (no-duplicatesp-equal l))
1261
1261
           (equal (occurrences-equal x l) 1)))
1262
1262
 
1263
 
(local 
 
1263
(local
1264
1264
   (defthm xoccurrences-equal-append
1265
1265
     (implies (integerp ac)
1266
1266
              (equal (xoccurrences-equal x (append a b))
1282
1282
    (equal (occurrences-equal x (reverse a))
1283
1283
           (occurrences-equal x a)))
1284
1284
 
1285
 
(local 
 
1285
(local
1286
1286
   (defthm leq-xoccurrences-equal-firstn
1287
1287
     (<= (xoccurrences-equal x (firstn n l))
1288
1288
         (xoccurrences-equal x l))))
1292
1292
        (occurrences-equal x l))
1293
1293
    :rule-classes :linear)
1294
1294
 
1295
 
(local 
 
1295
(local
1296
1296
   (defthm xoccurrences-equal-firstn-xposition-equal
1297
1297
     (implies (member-equal x l)
1298
1298
              (equal (xoccurrences-equal x (firstn (xposition-equal x l) l))
1330
1330
             (equal (occurrences-equal x (member-equal x l))
1331
1331
                    (occurrences-equal x l))))
1332
1332
 
1333
 
(local 
 
1333
(local
1334
1334
   (defthm leq-xoccurrences-equal-nthcdr
1335
1335
     (<= (xoccurrences-equal x (nthcdr n l))
1336
1336
         (xoccurrences-equal x l))))
1340
1340
        (occurrences-equal x l))
1341
1341
    :rule-classes :linear)
1342
1342
 
1343
 
(local 
 
1343
(local
1344
1344
   (defthm xoccurrences-equal-nthcdr-xposition-equal
1345
1345
     (implies (member-equal x l)
1346
1346
              (equal (xoccurrences-equal x (nthcdr (xposition-equal x l) l))
1351
1351
             (equal (occurrences-equal x (nthcdr (position-equal x l) l))
1352
1352
                    (occurrences-equal x l))))
1353
1353
 
1354
 
(local 
 
1354
(local
1355
1355
   (defthm xoccurrences-equal-put-nth
1356
1356
     (equal (xoccurrences-equal x (put-nth n v l))
1357
1357
            (if (< (nfix n) (len l))
1379
1379
             (occurrences-equal x l)))
1380
1380
    :hints (("Goal" :do-not-induct t)))
1381
1381
 
1382
 
(local 
 
1382
(local
1383
1383
   (defthm xoccurrences-equal-remove-equal
1384
1384
     (equal (xoccurrences-equal x (remove-equal y l))
1385
1385
            (if (equal x y)
1394
1394
             (occurrences-equal x l)))
1395
1395
    :hints (("Goal" :do-not-induct t)))
1396
1396
 
1397
 
(local 
 
1397
(local
1398
1398
   (defthm xoccurrences-equal-remove-duplicates-equal
1399
1399
     (<= (xoccurrences-equal x (remove-duplicates-equal l))
1400
1400
         1)))
1434
1434
                (+ (len a) (position-equal x b))
1435
1435
              nil))))
1436
1436
  :hints (("Goal" :do-not-induct t)))
1437
 
  
1438
 
    
 
1437
 
 
1438
 
1439
1439
; ------------------------------------------------------------
1440
1440
; PUT-NTH
1441
1441
; ------------------------------------------------------------
1442
1442
 
1443
 
(defthm put-nth-with-large-index 
 
1443
(defthm put-nth-with-large-index
1444
1444
  (implies (and (true-listp l)
1445
1445
                (<= (len l) (nfix n)))
1446
1446
           (equal (put-nth n v l) l)))
1471
1471
  (equal (put-nth i v (nthcdr j l))
1472
1472
         (nthcdr j (put-nth (+ (nfix j) (nfix i)) v l)))
1473
1473
  :hints (("Goal" :induct t)))
1474
 
 
1475
 
(defthm put-nth-nth 
 
1474
 
 
1475
(defthm put-nth-nth
1476
1476
  (implies (true-listp l)
1477
1477
           (equal (put-nth i (nth i l) l) l)))
1478
 
 
 
1478
 
1479
1479
(defthm put-nth-put-nth
1480
1480
  (equal (put-nth j b (put-nth i a l))
1481
1481
         (if (= (nfix i) (nfix j))
1482
1482
             (put-nth j b l)
1483
1483
             (put-nth i a (put-nth j b l))))
1484
 
  :rule-classes 
 
1484
  :rule-classes
1485
1485
  ((:rewrite :corollary
1486
1486
             (implies (= (nfix i) (nfix j))
1487
1487
                      (equal (put-nth j b (put-nth i a l))
1495
1495
; REMOVE
1496
1496
; ------------------------------------------------------------
1497
1497
 
1498
 
(defthm remove-equal-non-member-equal 
 
1498
(defthm remove-equal-non-member-equal
1499
1499
  (implies (and (true-listp l)
1500
1500
                (not (member-equal x l)))
1501
1501
           (equal (remove-equal x l) l)))
1509
1509
         (if (equal x y)
1510
1510
             (remove-equal x l)
1511
1511
             (remove-equal x (remove-equal y l))))
1512
 
  :rule-classes 
 
1512
  :rule-classes
1513
1513
  ((:rewrite :corollary
1514
1514
             (equal (remove-equal x (remove-equal x l))
1515
1515
                    (remove-equal x l)))))
1524
1524
             (append (update-nth n v a) b)
1525
1525
             (append a (update-nth (- n (len a)) v b)))))
1526
1526
 
1527
 
(defthm update-nth-nth 
 
1527
(defthm update-nth-nth
1528
1528
  (implies (and (integerp n)
1529
1529
                (<= 0 n)
1530
1530
                (< n (len l)))
1536
1536
         (if (= (nfix i) (nfix j))
1537
1537
             (update-nth j b l)
1538
1538
           (update-nth i a (update-nth j b l))))
1539
 
  :rule-classes 
 
1539
  :rule-classes
1540
1540
  ((:rewrite :corollary
1541
1541
    (implies (= (nfix i) (nfix j))
1542
1542
             (equal (update-nth j b (update-nth i a l))
1607
1607
  (equal (len (resize-list lst m default))
1608
1608
         (nfix m)))
1609
1609
 
1610
 
  
 
1610
 
1611
1611
; ------------------------------------------------------------
1612
1612
; MAKE-LIST-AC
1613
1613
; ------------------------------------------------------------