alist-fix

(in-package "ACL2")

(defsection alist-fix
  :parents (std/alists)
  :short "Basic fixing function for "modern" alists that respects the
behavior of @(see hons-assoc-equal)."
  (defund 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)))))
  (local (in-theory (enable alist-fix)))
  (defthm alistp-of-alist-fix (alistp (alist-fix x)))
  (defthm alist-fix-when-alistp
    (implies (alistp x) (equal (alist-fix x) x)))
  (defthm hons-assoc-equal-of-alist-fix
    (equal (hons-assoc-equal k (alist-fix x))
      (hons-assoc-equal k x)))
  (defthm alist-fix-of-cons
    (equal (alist-fix (cons a b))
      (if (consp a)
        (cons a (alist-fix b))
        (alist-fix b))))
  (defthm alist-fix-of-atom
    (implies (not (consp x)) (equal (alist-fix x) nil))
    :rule-classes ((:rewrite :backchain-limit-lst 0))))