• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Hons-and-memoization
    • Events
    • History
    • Parallelism
    • Programming
    • Real
    • ACL2-tutorial
    • Debugging
    • Miscellaneous
    • Prover-output
    • Built-in-theorems
      • Built-in-theorems-about-arithmetic
      • Built-in-theorems-about-symbols
      • Built-in-theorems-about-characters
      • Built-in-theorems-about-lists
      • Built-in-theorems-about-arrays
      • Built-in-theorems-about-strings
      • Built-in-theorems-about-alists
      • Built-in-theorems-about-total-order
      • Built-in-theorems-about-system-utilities
      • Built-in-theorems-about-cons-pairs
      • Built-in-theorems-for-tau
      • Built-in-theorems-about-bad-atoms
      • Built-in-theorems-about-logical-connectives
      • Built-in-theorems-about-booleans
      • Built-in-theorems-about-random$
      • Built-in-theorems-about-eqlables
    • Macros
    • Interfacing-tools
    • About-ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Built-in-theorems

Built-in-theorems-about-lists

Built-in theorems about lists.

Theorem: symbol-listp-forward-to-true-listp

(defthm symbol-listp-forward-to-true-listp
        (implies (symbol-listp x)
                 (true-listp x))
        :rule-classes :forward-chaining)

Theorem: true-listp-append

(defthm true-listp-append
        (implies (true-listp b)
                 (true-listp (append a b)))
        :rule-classes :type-prescription)

Theorem: append-to-nil

(defthm append-to-nil
        (implies (true-listp x)
                 (equal (append x nil) x)))

Theorem: character-listp-forward-to-eqlable-listp

(defthm character-listp-forward-to-eqlable-listp
        (implies (character-listp x)
                 (eqlable-listp x))
        :rule-classes :forward-chaining)

Theorem: standard-char-listp-forward-to-character-listp

(defthm standard-char-listp-forward-to-character-listp
        (implies (standard-char-listp x)
                 (character-listp x))
        :rule-classes :forward-chaining)

Theorem: atom-listp-forward-to-true-listp

(defthm atom-listp-forward-to-true-listp
        (implies (atom-listp x) (true-listp x))
        :rule-classes :forward-chaining)

Theorem: eqlable-listp-forward-to-atom-listp

(defthm eqlable-listp-forward-to-atom-listp
        (implies (eqlable-listp x)
                 (atom-listp x))
        :rule-classes :forward-chaining)

Theorem: good-atom-listp-forward-to-atom-listp

(defthm good-atom-listp-forward-to-atom-listp
        (implies (good-atom-listp x)
                 (atom-listp x))
        :rule-classes :forward-chaining)

Theorem: true-listp-revappend-type-prescription

(defthm true-listp-revappend-type-prescription
        (implies (true-listp y)
                 (true-listp (revappend x y)))
        :rule-classes :type-prescription)

Theorem: true-listp-take

(defthm true-listp-take (true-listp (take n l))
        :rule-classes :type-prescription)

Theorem: keyword-value-listp-forward-to-true-listp

(defthm keyword-value-listp-forward-to-true-listp
        (implies (keyword-value-listp x)
                 (true-listp x))
        :rule-classes :forward-chaining)

Theorem: true-list-listp-forward-to-true-listp

(defthm true-list-listp-forward-to-true-listp
        (implies (true-list-listp x)
                 (true-listp x))
        :rule-classes :forward-chaining)

Theorem: true-listp-nthcdr-type-prescription

(defthm true-listp-nthcdr-type-prescription
        (implies (true-listp x)
                 (true-listp (nthcdr n x)))
        :rule-classes :type-prescription)

Theorem: keyword-value-listp-assoc-keyword

(defthm
     keyword-value-listp-assoc-keyword
     (implies (keyword-value-listp l)
              (keyword-value-listp (assoc-keyword key l)))
     :rule-classes
     ((:forward-chaining :trigger-terms ((assoc-keyword key l)))))

Theorem: acl2-number-listp-forward-to-true-listp

(defthm acl2-number-listp-forward-to-true-listp
        (implies (acl2-number-listp x)
                 (true-listp x))
        :rule-classes :forward-chaining)

Theorem: rational-listp-forward-to-acl2-number-listp

(defthm rational-listp-forward-to-acl2-number-listp
        (implies (rational-listp x)
                 (acl2-number-listp x))
        :rule-classes :forward-chaining)

Theorem: integer-listp-forward-to-rational-listp

(defthm integer-listp-forward-to-rational-listp
        (implies (integer-listp x)
                 (rational-listp x))
        :rule-classes :forward-chaining)

Theorem: nat-listp-forward-to-integer-listp

(defthm nat-listp-forward-to-integer-listp
        (implies (nat-listp x)
                 (integer-listp x))
        :rule-classes :forward-chaining)

Theorem: nth-update-nth

(defthm nth-update-nth
        (equal (nth m (update-nth n val l))
               (if (equal (nfix m) (nfix n))
                   val (nth m l))))

Theorem: true-listp-update-nth

(defthm true-listp-update-nth
        (implies (true-listp l)
                 (true-listp (update-nth key val l)))
        :rule-classes :type-prescription)

Theorem: nth-update-nth-array

(defthm nth-update-nth-array
        (equal (nth m (update-nth-array n i val l))
               (if (equal (nfix m) (nfix n))
                   (update-nth i val (nth m l))
                   (nth m l))))

Theorem: len-update-nth

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

Theorem: nth-0-cons

(defthm nth-0-cons (equal (nth 0 (cons a l)) a))

Theorem: nth-add1

(defthm nth-add1
        (implies (and (integerp n) (>= n 0))
                 (equal (nth (+ 1 n) (cons a l))
                        (nth n l))))

Theorem: pairlis$-true-list-fix

(defthm pairlis$-true-list-fix
        (equal (pairlis$ x (true-list-fix y))
               (pairlis$ x y)))