		Search-engine friendly clone of the ACL2 documentation.

Std/lists/resize-list

Lemmas about resize-list available in the std/lists library.

Definitions and Theorems

Trivial reductions

Theorem: resize-list-when-zp

(defthm resize-list-when-zp
        (implies (zp n)
                 (equal (resize-list lst n default-value)
                        nil)))

Theorem: resize-list-of-nfix

(defthm resize-list-of-nfix
        (equal (resize-list lst (nfix n) default-value)
               (resize-list lst n default-value)))

Theorem: resize-list-when-atom

(defthm resize-list-when-atom
        (implies (atom lst)
                 (equal (resize-list lst n default-value)
                        (repeat n default-value))))

Relation with other basic list functions

Theorem: nth-of-resize-list

(defthm nth-of-resize-list
        (equal (nth n (resize-list lst m default-value))
               (let ((n (nfix n)) (m (nfix m)))
                    (and (< n m)
                         (if (< n (len lst))
                             (nth n lst)
                             default-value)))))

Theorem: len-of-resize-list

(defthm len-of-resize-list
        (equal (len (resize-list lst n default))
               (nfix n)))

Theorem: resize-list-of-len-free

(defthm resize-list-of-len-free
        (implies (equal (nfix n) (len lst))
                 (equal (resize-list lst n default-value)
                        (list-fix lst))))

Theorem: equal-of-resize-list-and-self

(defthm equal-of-resize-list-and-self
        (equal (equal (resize-list lst n default-value)
                      lst)
               (and (true-listp lst)
                    (equal (len lst) (nfix n)))))