• Top
  • Documentation
  • Books
  • 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
      • 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
      • Std/lists/add-to-set
      • 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
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Std/lists/abstract

Elementlist-projection

Generic projection over a typed list.

Definitions and Theorems

Function: elementlist-projection

(defun elementlist-projection (x)
  (if (atom x)
      nil
    (cons (element-xformer (car x))
          (elementlist-projection (cdr x)))))

Theorem: outelement-list-p-of-elementlist-projection

(defthm outelement-list-p-of-elementlist-projection
  (implies (element-list-p x)
           (outelement-list-p (elementlist-projection x)))
  :rule-classes :rewrite)

Theorem: elementlist-projection-of-cons

(defthm elementlist-projection-of-cons
  (equal (elementlist-projection (cons a b))
         (cons (element-xformer a)
               (elementlist-projection b)))
  :rule-classes :rewrite)

Theorem: elementlist-projection-when-not-consp

(defthm elementlist-projection-when-not-consp
  (implies (not (consp x))
           (equal (elementlist-projection x) nil))
  :rule-classes :rewrite)

Theorem: true-listp-of-elementlist-projection

(defthm true-listp-of-elementlist-projection
  (true-listp (elementlist-projection x))
  :rule-classes :type-prescription)

Theorem: len-of-elementlist-projection

(defthm len-of-elementlist-projection
  (equal (len (elementlist-projection x))
         (len x))
  :rule-classes :rewrite)

Theorem: consp-of-elementlist-projection

(defthm consp-of-elementlist-projection
  (equal (consp (elementlist-projection x))
         (consp x))
  :rule-classes :rewrite)

Theorem: elementlist-projection-under-iff

(defthm elementlist-projection-under-iff
  (iff (elementlist-projection x)
       (consp x))
  :rule-classes :rewrite)

Theorem: car-of-elementlist-projection-when-nil-preservingp

(defthm car-of-elementlist-projection-when-nil-preservingp
  (implies (equal nil (element-xformer nil))
           (equal (car (elementlist-projection x))
                  (element-xformer (car x))))
  :rule-classes :rewrite)

Theorem: car-of-elementlist-projection

(defthm car-of-elementlist-projection
  (equal (car (elementlist-projection x))
         (and (consp x)
              (element-xformer (car x))))
  :rule-classes :rewrite)

Theorem: cdr-of-elementlist-projection

(defthm cdr-of-elementlist-projection
  (equal (cdr (elementlist-projection x))
         (elementlist-projection (cdr x)))
  :rule-classes :rewrite)

Theorem: elementlist-projection-of-append

(defthm elementlist-projection-of-append
  (equal (elementlist-projection (append a b))
         (append (elementlist-projection a)
                 (elementlist-projection b)))
  :rule-classes :rewrite)