def-hash-theory

(in-package "STOBJS")

(include-book "std/alists/alist-defuns" :dir :system)

(include-book "std/alists/alist-fix" :dir :system)

(local (include-book "std/alists/hons-remove-assoc" :dir :system))

(local (include-book "std/alists/hons-put-assoc" :dir :system))

(local (include-book "std/alists/alist-equiv" :dir :system))

(defthm defhash-member-of-append
  (iff (member-equal k
      (append x y))
    (or (member-equal k x)
      (member-equal k y)))
  :hints (("Goal" :in-theory (enable member-equal append))))

(defthm defhash-no-duplicatesp-of-append
  (iff (no-duplicatesp-equal (append x y))
    (and (no-duplicatesp-equal x)
      (no-duplicatesp-equal y)
      (not (intersectp-equal x y))))
  :hints (("Goal" :in-theory (enable no-duplicatesp-equal
       intersectp-equal
       append))))

(defcong alist-equiv
  alist-equiv
  (hons-remove-assoc k x)
  2
  :hints (("Goal" :in-theory (enable alist-equiv-when-agree-on-bad-guy))))

(defthm defhash-intersectp-of-singleton
  (iff (intersectp-equal x (list k))
    (member-equal k x))
  :hints (("Goal" :in-theory (enable intersectp-equal
       member-equal))))

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

(defthm defhash-alist-keys-of-hons-remove-assoc
  (equal (alist-keys (hons-remove-assoc k x))
    (remove-equal k (alist-keys x)))
  :hints (("Goal" :in-theory (enable alist-keys
       hons-remove-assoc
       remove-equal))))

(defthm defhash-member-of-remove
  (implies (not (member-equal j x))
    (not (member-equal j
        (remove-equal k x)))))

(defthm defhash-no-duplicates-of-remove
  (implies (no-duplicatesp-equal x)
    (no-duplicatesp-equal (remove-equal k x)))
  :hints (("Goal" :in-theory (enable no-duplicatesp-equal
       remove-equal))))

(defthm defhash-alist-keys-of-alist-fix
  (equal (alist-keys (alist-fix x))
    (alist-keys x))
  :hints (("Goal" :in-theory (enable alist-fix alist-keys))))

(defthm defhash-alist-fix-under-alist-equiv
  (alist-equiv (alist-fix x) x)
  :hints (("Goal" :in-theory (enable alist-equiv-iff-agree-on-bad-guy))))

(defthm defhash-alist-equiv-of-hons-put-assoc
  (alist-equiv (cons (cons k v) x)
    (hons-put-assoc k v x))
  :hints (("Goal" :in-theory (enable alist-equiv-iff-agree-on-bad-guy))))

(defcong alist-equiv
  alist-equiv
  (hons-put-assoc k v x)
  3
  :hints (("Goal" :in-theory (enable alist-equiv-when-agree-on-bad-guy))))

(defthm defhash-duplicate-keys-of-hons-put-assoc
  (implies (no-duplicatesp-equal (alist-keys x))
    (no-duplicatesp-equal (alist-keys (hons-put-assoc k v x)))))

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

(defcong alist-equiv
  equal
  (hons-assoc-equal k x)
  2)