put-assoc-equal

(in-package "ACL2")

(include-book "alist-defuns")

(defthm put-assoc-equal-identity
  (implies (and (assoc-equal k x)
      (alistp x)
      (equal v (cdr (assoc-equal k x))))
    (equal (put-assoc-equal k v x) x))
  :hints (("Goal" :in-theory (enable assoc-equal put-assoc-equal))))

(defthm hons-assoc-equal-of-put-assoc-equal
  (equal (hons-assoc-equal k (put-assoc-equal k1 v x))
    (if (equal k k1)
      (cons k v)
      (hons-assoc-equal k x)))
  :hints (("Goal" :in-theory (enable hons-assoc-equal put-assoc-equal))))

(local (defthm fal-extract-of-acons-non-mem
    (implies (not (member-equal k keys))
      (equal (fal-extract keys (cons (cons k v) x))
        (fal-extract keys x)))
    :hints (("Goal" :in-theory (enable fal-extract)))))

(local (defthm car-hons-assoc-equal
    (equal (car (hons-assoc-equal k x))
      (and (hons-assoc-equal k x) k))))

(defthm fal-extract-of-put-assoc-equal
  (implies (and (no-duplicatesp-equal keys) (hons-assoc-equal k x))
    (equal (fal-extract keys (put-assoc-equal k v x))
      (if (member-equal k keys)
        (put-assoc-equal k v (fal-extract keys x))
        (fal-extract keys x))))
  :hints (("Goal" :in-theory (enable fal-extract put-assoc-equal))))

(local (defthm member-alist-keys
    (iff (member-equal k (alist-keys x)) (hons-assoc-equal k x))
    :hints (("Goal" :in-theory (enable alist-keys)))))

(defthm no-duplicate-keys-of-put-assoc-equal
  (implies (and (no-duplicatesp-equal (alist-keys x)) (alistp x))
    (no-duplicatesp-equal (alist-keys (put-assoc-equal k v x))))
  :hints (("Goal" :in-theory (enable alist-keys no-duplicatesp-equal put-assoc-equal))))

(defthm put-assoc-equal-alternate
  (implies (hons-assoc-equal k1 x)
    (equal (put-assoc-equal k1
        v1
        (put-assoc-equal k2 v2 (put-assoc-equal k1 v3 x)))
      (put-assoc-equal k1 v1 (put-assoc-equal k2 v2 x))))
  :hints (("Goal" :in-theory (enable put-assoc-equal))))

(defthm put-assoc-equal-redundant
  (equal (put-assoc-equal k1 v1 (put-assoc-equal k1 v2 x))
    (put-assoc-equal k1 v1 x))
  :hints (("Goal" :in-theory (enable put-assoc-equal))))

(defthm alist-keys-of-put-assoc-equal
  (implies (or (alistp x) k)
    (equal (alist-keys (put-assoc-equal k v x))
      (if (hons-assoc-equal k x)
        (alist-keys x)
        (append (alist-keys x) (list k)))))
  :hints (("Goal" :in-theory (enable alist-keys put-assoc-equal))))

(defthm remove-assoc-equal-of-put-assoc-equal
  (equal (remove-assoc-equal name (put-assoc-equal name val x))
    (remove-assoc-equal name x))
  :hints (("Goal" :in-theory (enable remove-assoc-equal put-assoc-equal))))

(defthm alistp-of-put-assoc-equal
  (implies (alistp x) (alistp (put-assoc-equal k v x))))