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

Std/lists/revappend

Lemmas about revappend available in the std/lists library.

Note: we typically avoid reasoning about revappend because the following rule can always rewrite it away:

Theorem: revappend-removal

(defthm revappend-removal
  (equal (revappend x y)
         (append (rev x) y)))

However, if for some reason you need to disable revappend-removal, these lemmas may be useful.

Definitions and Theorems

Theorem: true-listp-of-revappend

(defthm true-listp-of-revappend
  (equal (true-listp (revappend x y))
         (true-listp y)))

Theorem: consp-of-revappend

(defthm consp-of-revappend
  (equal (consp (revappend x y))
         (or (consp x) (consp y))))

Theorem: len-of-revappend

(defthm len-of-revappend
  (equal (len (revappend x y))
         (+ (len x) (len y))))

Theorem: equal-when-revappend-same

(defthm equal-when-revappend-same
  (equal (equal (revappend x y1)
                (revappend x y2))
         (equal y1 y2)))

Theorem: list-fix-of-revappend

(defthm list-fix-of-revappend
  (equal (list-fix (revappend x y))
         (revappend x (list-fix y))))

Theorem: equal-of-revappends-when-true-listps

(defthm equal-of-revappends-when-true-listps
  (implies (and (true-listp x1) (true-listp x2))
           (equal (equal (revappend x1 y)
                         (revappend x2 y))
                  (equal x1 x2))))

Theorem: element-list-p-of-revappend

(defthm element-list-p-of-revappend
  (equal (element-list-p (revappend x y))
         (and (element-list-p (list-fix x))
              (element-list-p y)))
  :rule-classes :rewrite)

Theorem: element-list-fix-of-revappend

(defthm element-list-fix-of-revappend
  (equal (element-list-fix (revappend x y))
         (revappend (element-list-fix x)
                    (element-list-fix y)))
  :rule-classes :rewrite)

Theorem: elementlist-projection-of-revappend

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