		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)))))