• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
      • Std/lists/abstract
      • Rev
      • Defsort
      • List-fix
      • Std/lists/nth
      • Hons-remove-duplicates
      • Std/lists/update-nth
      • Set-equiv
      • Duplicity
      • Prefixp
      • Std/lists/take
      • Std/lists/intersection$
      • Nats-equiv
      • Repeat
      • Index-of
      • All-equalp
      • Sublistp
      • Std/lists/nthcdr
      • Listpos
      • List-equiv
      • Final-cdr
      • Std/lists/append
      • Std/lists/remove
      • Subseq-list
      • Rcons
      • Std/lists/revappend
      • Std/lists/remove-duplicates-equal
      • Std/lists/reverse
      • Std/lists/last
      • Std/lists/resize-list
      • Flatten
      • Suffixp
      • Std/lists/butlast
      • Std/lists/set-difference
      • Std/lists/len
      • Std/lists/intersectp
      • Std/lists/true-listp
      • Intersectp-witness
      • Subsetp-witness
      • Std/lists/remove1-equal
      • Rest-n
      • First-n
      • Std/lists/union
      • Append-without-guard
      • Std/lists/subsetp
      • Std/lists/member
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Std/lists
• Update-nth

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)