• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
    • Std/lists
      • Std/lists/abstract
      • Rev
      • Defsort
      • List-fix
        • Llist-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
• True-listp

List-fix

(list-fix x) converts x into a true-listp by, if necessary, changing its final-cdr to nil.

list-fix is really a macro which expands to a call to true-list-fix with the same argument.

See also llist-fix, a "logical list fix" that is guarded with true-listp for greater efficiency.

Macro: list-fix-exec

(defmacro list-fix-exec (x)
          (cons 'true-list-fix-exec
                (cons x 'nil)))

Macro: list-fix

(defmacro list-fix (x)
          (cons 'true-list-fix (cons x 'nil)))

Definitions and Theorems

Theorem: list-fix-when-not-consp

(defthm list-fix-when-not-consp
        (implies (not (consp x))
                 (equal (list-fix x) nil)))

Theorem: list-fix-of-cons

(defthm list-fix-of-cons
        (equal (list-fix (cons a x))
               (cons a (list-fix x))))

Theorem: list-fix-exec-removal

(defthm list-fix-exec-removal
        (equal (list-fix-exec x) (list-fix x)))

Theorem: car-of-list-fix

(defthm car-of-list-fix
        (equal (car (list-fix x)) (car x)))

Theorem: cdr-of-list-fix

(defthm cdr-of-list-fix
        (equal (cdr (list-fix x))
               (list-fix (cdr x))))

Theorem: list-fix-when-len-zero

(defthm list-fix-when-len-zero
        (implies (equal (len x) 0)
                 (equal (list-fix x) nil)))

Theorem: true-listp-of-list-fix

(defthm true-listp-of-list-fix
        (true-listp (list-fix x)))

Theorem: len-of-list-fix

(defthm len-of-list-fix
        (equal (len (list-fix x)) (len x)))

Theorem: list-fix-when-true-listp

(defthm list-fix-when-true-listp
        (implies (true-listp x)
                 (equal (list-fix x) x)))

Theorem: list-fix-under-iff

(defthm list-fix-under-iff
        (iff (list-fix x) (consp x)))

Theorem: consp-of-list-fix

(defthm consp-of-list-fix
        (equal (consp (list-fix x)) (consp x)))

Theorem: last-of-list-fix

(defthm last-of-list-fix
        (equal (last (list-fix x))
               (list-fix (last x))))

Theorem: equal-of-list-fix-and-self

(defthm equal-of-list-fix-and-self
        (equal (equal x (list-fix x))
               (true-listp x)))

Theorem: element-list-p-of-list-fix-non-true-listp

(defthm element-list-p-of-list-fix-non-true-listp
        (implies (element-list-final-cdr-p t)
                 (equal (element-list-p (list-fix x))
                        (element-list-p x)))
        :rule-classes :rewrite)

Theorem: element-list-p-of-list-fix-true-listp

(defthm element-list-p-of-list-fix-true-listp
        (implies (element-list-p x)
                 (element-list-p (list-fix x)))
        :rule-classes :rewrite)

Theorem: element-list-fix-of-list-fix-true-list

(defthm element-list-fix-of-list-fix-true-list
        (implies (not (element-list-final-cdr-p t))
                 (equal (element-list-fix (list-fix x))
                        (element-list-fix x)))
        :rule-classes :rewrite)

Theorem: element-list-fix-of-list-fix-non-true-list

(defthm element-list-fix-of-list-fix-non-true-list
        (implies (element-list-final-cdr-p t)
                 (equal (element-list-fix (list-fix x))
                        (list-fix (element-list-fix x))))
        :rule-classes :rewrite)

Theorem: elementlist-projection-of-list-fix

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

Theorem: elementlist-mapappend-of-list-fix

(defthm elementlist-mapappend-of-list-fix
        (equal (elementlist-mapappend (list-fix x))
               (elementlist-mapappend x))
        :rule-classes :rewrite)

Subtopics

Llist-fix

(llist-fix x) is locally just list-fix, but it is guarded with true-listp so that in the execution it is just an identity function.