• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • 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
      • Std/lists/append
      • Listpos
      • List-equiv
      • Final-cdr
      • Std/lists/remove
      • Subseq-list
      • Rcons
      • Std/lists/revappend
      • Std/lists/remove-duplicates-equal
      • Std/lists/last
      • Std/lists/reverse
      • Std/lists/resize-list
      • Flatten
      • Suffixp
      • Std/lists/set-difference
      • Std/lists/butlast
      • 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/system
    • Std/basic
    • 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
  • Testing-utilities
  • Math

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