		Search-engine friendly clone of the ACL2 documentation.

Std/lists/update-nth

Lemmas about update-nth available in the std/lists library.

Definitions and Theorems

Theorem: update-nth-when-atom

(defthm update-nth-when-atom
  (implies (atom x)
           (equal (update-nth n v x)
                  (append (repeat n nil) (list v)))))

Theorem: update-nth-when-zp

(defthm update-nth-when-zp
  (implies (zp a)
           (equal (update-nth a v xs)
                  (cons v (cdr xs)))))

Theorem: update-nth-of-cons

(defthm update-nth-of-cons
  (equal (update-nth n x (cons a b))
         (if (zp n)
             (cons x b)
           (cons a (update-nth (1- n) x b)))))

Theorem: true-listp-of-update-nth

(defthm true-listp-of-update-nth
  (equal (true-listp (update-nth n v x))
         (or (<= (len x) (nfix n))
             (true-listp x))))

Theorem: len-of-update-nth

(defthm len-of-update-nth
  (equal (len (update-nth n v x))
         (max (len x) (+ 1 (nfix n)))))

Theorem: car-of-update-nth

(defthm car-of-update-nth
  (equal (car (update-nth n v x))
         (if (zp n) v (car x))))

Theorem: cdr-of-update-nth

(defthm cdr-of-update-nth
  (equal (cdr (update-nth n v x))
         (if (zp n)
             (cdr x)
           (update-nth (1- n) v (cdr x)))))

Theorem: nth-of-update-nth-same

(defthm nth-of-update-nth-same
  (equal (nth n (update-nth n v x)) v))

Theorem: nth-of-update-nth-diff

(defthm nth-of-update-nth-diff
  (implies (not (equal (nfix n1) (nfix n2)))
           (equal (nth n1 (update-nth n2 v x))
                  (nth n1 x))))

Theorem: nth-of-update-nth-split-for-constants

(defthm nth-of-update-nth-split-for-constants
  (implies (and (syntaxp (quotep n1))
                (syntaxp (quotep n2)))
           (equal (nth n1 (update-nth n2 v x))
                  (if (equal (nfix n1) (nfix n2))
                      v
                    (nth n1 x)))))

Theorem: update-nth-of-nth

(defthm update-nth-of-nth
  (implies (< (nfix n) (len x))
           (equal (update-nth n (nth n x) x) x)))

Theorem: update-nth-of-nth-free

(defthm update-nth-of-nth-free
  (implies (and (equal (nth n x) free)
                (< (nfix n) (len x)))
           (equal (update-nth n free x) x)))

Theorem: update-nth-of-update-nth-same

(defthm update-nth-of-update-nth-same
  (equal (update-nth n v1 (update-nth n v2 x))
         (update-nth n v1 x)))

Theorem: update-nth-of-update-nth-diff

(defthm update-nth-of-update-nth-diff
  (implies (not (equal (nfix n1) (nfix n2)))
           (equal (update-nth n1 v1 (update-nth n2 v2 x))
                  (update-nth n2 v2 (update-nth n1 v1 x))))
  :rule-classes ((:rewrite :loop-stopper ((n1 n2 update-nth)))))

Theorem: update-nth-diff-gather-constants

(defthm update-nth-diff-gather-constants
  (implies (and (syntaxp (and (quotep x)
                              (quotep n)
                              (quotep val1)
                              (or (not (quotep m))
                                  (not (quotep val2)))))
                (not (equal (nfix n) (nfix m))))
           (equal (update-nth n val1 (update-nth m val2 x))
                  (update-nth m val2 (update-nth n val1 x))))
  :rule-classes ((:rewrite :loop-stopper nil)))

Theorem: final-cdr-of-update-nth

(defthm final-cdr-of-update-nth
  (equal (final-cdr (update-nth n v x))
         (if (< (nfix n) (len x))
             (final-cdr x)
           nil)))

Theorem: nthcdr-past-update-nth

(defthm nthcdr-past-update-nth
  (implies (and (< (nfix n2) (len x))
                (< (nfix n2) (nfix n1)))
           (equal (nthcdr n1 (update-nth n2 val x))
                  (nthcdr n1 x))))

Theorem: nthcdr-before-update-nth

(defthm nthcdr-before-update-nth
  (implies (and (< (nfix n2) (len x))
                (<= (nfix n1) (nfix n2)))
           (equal (nthcdr n1 (update-nth n2 val x))
                  (update-nth (- (nfix n2) (nfix n1))
                              val (nthcdr n1 x)))))

Theorem: nthcdr-of-update-nth

(defthm nthcdr-of-update-nth
  (equal (nthcdr n1 (update-nth n2 val x))
         (if (< (nfix n2) (nfix n1))
             (nthcdr n1 x)
           (update-nth (- (nfix n2) (nfix n1))
                       val (nthcdr n1 x)))))

Theorem: take-before-update-nth

(defthm take-before-update-nth
  (implies (<= (nfix n1) (nfix n2))
           (equal (take n1 (update-nth n2 val x))
                  (take n1 x))))

Theorem: take-after-update-nth

(defthm take-after-update-nth
  (implies (> (nfix n1) (nfix n2))
           (equal (take n1 (update-nth n2 val x))
                  (update-nth n2 val (take n1 x)))))

Theorem: take-of-update-nth

(defthm take-of-update-nth
  (equal (take n1 (update-nth n2 val x))
         (if (<= (nfix n1) (nfix n2))
             (take n1 x)
           (update-nth n2 val (take n1 x)))))

Theorem: member-equal-update-nth

(defthm member-equal-update-nth
  (member-equal x (update-nth n x l)))

Theorem: update-nth-append

(defthm update-nth-append
  (equal (update-nth n v (append a b))
         (if (< (nfix n) (len a))
             (append (update-nth n v a) b)
           (append a (update-nth (- n (len a)) v b)))))

Theorem: element-list-p-of-update-nth

(defthm element-list-p-of-update-nth
  (implies (element-list-p (double-rewrite x))
           (iff (element-list-p (update-nth n y x))
                (and (element-p y)
                     (or (<= (nfix n) (len x))
                         (element-p nil)))))
  :rule-classes :rewrite)

Theorem: elementlist-projection-of-update-nth

(defthm elementlist-projection-of-update-nth
  (implies (<= (nfix n) (len x))
           (equal (elementlist-projection (update-nth n v x))
                  (update-nth n (element-xformer v)
                              (elementlist-projection x))))
  :rule-classes :rewrite)

Theorem: elementlist-projection-of-update-nth-nil-preserving

(defthm elementlist-projection-of-update-nth-nil-preserving
  (implies (equal (element-xformer nil) nil)
           (equal (elementlist-projection (update-nth n v x))
                  (update-nth n (element-xformer v)
                              (elementlist-projection x))))
  :rule-classes :rewrite)