		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)))