• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
      • Std/lists/abstract
        • Element-list-p
        • Element-list-equiv
        • Element-list-nonempty-p
        • Elementlist-projection
        • Element-equiv
        • Generic-eval-requirement
        • Element-list-fix
        • Elementlist-mapappend
        • Element-fix
        • Outelement-list-p
        • Outelement-p
        • Element-xformer
        • Element-listxformer
        • Element-p
        • Def-listp-rule
        • Def-projection-rule
        • Def-nonempty-listp-rule
        • Def-mapappend-rule
        • Def-listfix-rule
      • 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/abstract

Element-list-p

Generic typed list recognizer function.

Definitions and Theorems

Function: element-list-p

(defun element-list-p (x)
       (if (atom x)
           (element-list-final-cdr-p x)
           (and (element-p (car x))
                (element-list-p (cdr x)))))

Theorem: element-list-p-of-cons

(defthm element-list-p-of-cons
        (equal (element-list-p (cons a x))
               (and (element-p a) (element-list-p x)))
        :rule-classes :rewrite)

Theorem: element-list-p-of-cdr-when-element-list-p

(defthm element-list-p-of-cdr-when-element-list-p
        (implies (element-list-p (double-rewrite x))
                 (element-list-p (cdr x)))
        :rule-classes :rewrite)

Theorem: element-list-p-when-not-consp-non-true-list

(defthm element-list-p-when-not-consp-non-true-list
        (implies (and (element-list-final-cdr-p t)
                      (not (consp x)))
                 (element-list-p x))
        :rule-classes :rewrite)

Theorem: element-list-p-when-not-consp-true-list

(defthm element-list-p-when-not-consp-true-list
        (implies (and (not (element-list-final-cdr-p t))
                      (not (consp x)))
                 (equal (element-list-p x) (not x)))
        :rule-classes :rewrite)

Theorem: element-p-of-car-when-element-list-p-when-element-p-nil

(defthm element-p-of-car-when-element-list-p-when-element-p-nil
        (implies (and (element-p nil) (element-list-p x))
                 (element-p (car x)))
        :rule-classes :rewrite)

Theorem: element-p-of-car-when-element-list-p-when-not-element-p-nil-and-not-negated

(defthm
 element-p-of-car-when-element-list-p-when-not-element-p-nil-and-not-negated
 (implies (and (not (element-p nil))
               (element-list-p x))
          (iff (element-p (car x)) (consp x)))
 :rule-classes :rewrite)

Theorem: element-p-of-car-when-element-list-p-when-not-element-p-nil-and-negated

(defthm
 element-p-of-car-when-element-list-p-when-not-element-p-nil-and-negated
 (implies (and (not (element-p nil))
               (element-list-p x))
          (iff (non-element-p (car x))
               (not (consp x))))
 :rule-classes :rewrite)

Theorem: element-p-of-car-when-element-list-p-when-unknown-nil

(defthm element-p-of-car-when-element-list-p-when-unknown-nil
        (implies (element-list-p x)
                 (iff (element-p (car x))
                      (or (consp x) (element-p nil))))
        :rule-classes :rewrite)

Theorem: element-p-of-car-when-element-list-p-when-unknown-nil-negated

(defthm
     element-p-of-car-when-element-list-p-when-unknown-nil-negated
     (implies (element-list-p x)
              (iff (non-element-p (car x))
                   (and (not (consp x))
                        (non-element-p nil))))
     :rule-classes :rewrite)

Theorem: true-listp-when-element-list-p-rewrite

(defthm true-listp-when-element-list-p-rewrite
        (implies (and (element-list-p x)
                      (not (element-list-final-cdr-p t)))
                 (true-listp x))
        :rule-classes :rewrite)

Theorem: true-listp-when-element-list-p-compound-recognizer

(defthm true-listp-when-element-list-p-compound-recognizer
        (implies (and (element-list-p x)
                      (not (element-list-final-cdr-p t)))
                 (true-listp x))
        :rule-classes nil)

Theorem: element-list-p-of-append-non-true-list

(defthm element-list-p-of-append-non-true-list
        (implies (element-list-final-cdr-p t)
                 (equal (element-list-p (append a b))
                        (and (element-list-p a)
                             (element-list-p b))))
        :rule-classes :rewrite)