• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • 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
        • Take-of-too-many
        • Make-list-ac-removal
        • Replicate
      • 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
• Make-list

Repeat

(repeat n x) creates a list of xes with length n; it is a simpler alternative to make-list.

Definitions and Theorems

Function: repeat

(defun repeat (n x)
       (declare (xargs :guard (natp n)))
       (mbe :logic (if (zp n)
                       nil (cons x (repeat (- n 1) x)))
            :exec (make-list n :initial-element x)))

Theorem: repeat-when-zp

(defthm repeat-when-zp
        (implies (zp n)
                 (equal (repeat n a) nil)))

Theorem: (repeat 0 x)

(defthm |(repeat 0 x)| (equal (repeat 0 x) nil))

Theorem: repeat-under-iff

(defthm repeat-under-iff
        (iff (repeat n x) (not (zp n))))

Theorem: consp-of-repeat

(defthm consp-of-repeat
        (equal (consp (repeat n a))
               (not (zp n))))

Theorem: repeat-1

(defthm repeat-1 (equal (repeat 1 a) (list a)))

Theorem: take-when-atom

(defthm take-when-atom
        (implies (atom x)
                 (equal (take n x) (repeat n nil))))

Theorem: len-of-repeat

(defthm len-of-repeat
        (equal (len (repeat n x)) (nfix n)))

Theorem: repeat-of-nfix

(defthm repeat-of-nfix
        (equal (repeat (nfix n) x)
               (repeat n x)))

Theorem: car-of-repeat-increment

(defthm car-of-repeat-increment
        (implies (natp n)
                 (equal (car (repeat (+ 1 n) x)) x)))

Theorem: cdr-of-repeat-increment

(defthm cdr-of-repeat-increment
        (implies (natp n)
                 (equal (cdr (repeat (+ 1 n) x))
                        (repeat n x))))

Theorem: member-of-repeat

(defthm member-of-repeat
        (equal (member a (repeat n b))
               (if (equal a b) (repeat n b) nil)))

Theorem: take-of-repeat

(defthm take-of-repeat
        (equal (take n (repeat k a))
               (if (<= (nfix n) (nfix k))
                   (repeat n a)
                   (append (repeat k a)
                           (repeat (- (nfix n) (nfix k)) nil)))))

Theorem: nthcdr-of-repeat

(defthm nthcdr-of-repeat
        (equal (nthcdr n (repeat k a))
               (if (<= (nfix n) (nfix k))
                   (repeat (- (nfix k) (nfix n)) a)
                   nil)))

Theorem: append-of-repeat-to-cons-of-same

(defthm append-of-repeat-to-cons-of-same
        (equal (append (repeat n a) (cons a x))
               (cons a (append (repeat n a) x))))

Theorem: equal-of-append-repeat

(defthm equal-of-append-repeat
        (implies (case-split (<= n (len y)))
                 (equal (equal (append (repeat n a) x) y)
                        (and (equal (repeat n a) (take n y))
                             (equal x (nthcdr n y))))))

Theorem: rev-of-repeat

(defthm rev-of-repeat
        (equal (rev (repeat n a)) (repeat n a)))

Theorem: subsetp-of-repeat

(defthm subsetp-of-repeat
        (iff (subsetp-equal (repeat n x) y)
             (or (zp n) (member-equal x y))))

Theorem: element-list-p-of-repeat

(defthm element-list-p-of-repeat
        (iff (element-list-p (repeat n x))
             (or (element-p x) (zp n)))
        :rule-classes :rewrite)

Subtopics

Take-of-too-many

Rewrite (take n x) when n is more than (len x).

Make-list-ac-removal

Rewrite rule that eliminates make-list-ac (and hence make-list) in favor of repeat.

Replicate

Alias for repeat.