		Search-engine friendly clone of the ACL2 documentation.

Std/alists

Alist-fix

Basic fixing function for "modern" alists that respects the behavior of hons-assoc-equal.

Definitions and Theorems

Function: alist-fix

(defun alist-fix (x)
       (declare (xargs :guard t))
       (if (atom x)
           nil
           (if (consp (car x))
               (cons (car x) (alist-fix (cdr x)))
               (alist-fix (cdr x)))))

Theorem: alistp-of-alist-fix

(defthm alistp-of-alist-fix
        (alistp (alist-fix x)))

Theorem: alist-fix-when-alistp

(defthm alist-fix-when-alistp
        (implies (alistp x)
                 (equal (alist-fix x) x)))

Theorem: hons-assoc-equal-of-alist-fix

(defthm hons-assoc-equal-of-alist-fix
        (equal (hons-assoc-equal k (alist-fix x))
               (hons-assoc-equal k x)))

Theorem: alist-fix-of-cons

(defthm alist-fix-of-cons
        (equal (alist-fix (cons a b))
               (if (consp a)
                   (cons a (alist-fix b))
                   (alist-fix b))))

Theorem: alist-fix-of-atom

(defthm alist-fix-of-atom
        (implies (not (consp x))
                 (equal (alist-fix x) nil))
        :rule-classes ((:rewrite :backchain-limit-lst 0)))