hons-put-assoc

(in-package "ACL2")

(include-book "alist-defuns")

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

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

(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-hons-put-assoc
  (implies (and (no-duplicatesp-equal keys) (hons-assoc-equal k x))
    (equal (fal-extract keys (hons-put-assoc k v x))
      (if (member-equal k keys)
        (hons-put-assoc k v (fal-extract keys x))
        (fal-extract keys x))))
  :hints (("Goal" :in-theory (enable fal-extract hons-put-assoc))))

(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-hons-put-assoc
  (implies (no-duplicatesp-equal (alist-keys x))
    (no-duplicatesp-equal (alist-keys (hons-put-assoc k v x))))
  :hints (("Goal" :in-theory (enable alist-keys no-duplicatesp-equal hons-put-assoc))))

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

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

(defthm alist-keys-of-hons-put-assoc
  (implies (or (alistp x) k)
    (equal (alist-keys (hons-put-assoc 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 hons-put-assoc))))

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

(defthm alistp-of-hons-put-assoc
  (implies (alistp x) (alistp (hons-put-assoc k v x)))
  :hints (("Goal" :in-theory (enable hons-put-assoc))))