other
(in-package "OMAP")
other
(include-book "std/util/defrule" :dir :system)
other
(local (include-book "std/basic/controlled-configuration" :dir :system))
other
(local (controlled-configuration :hooks nil))
other
(local (include-book "kestrel/alists-light/remove-assoc-equal" :dir :system))
other
(local (include-book "kestrel/alists-light/strip-cars" :dir :system))
other
(include-book "core")
other
(include-book "extensionality")
other
(include-book "delete")
other
(defrule emptyp-of-from-alist
(equal (emptyp (from-alist alist))
(not (consp alist)))
:expand (from-alist alist))
other
(defrule assoc-of-from-alist (implies (alistp alist) (equal (assoc key (from-alist alist)) (assoc-equal key alist))) :induct t :enable (from-alist assoc-equal alistp))
other
(defrule from-alist-of-acons (equal (from-alist (acons key val alist)) (update key val (from-alist alist))) :enable (from-alist acons))
other
(defruled update-of-from-alist-becomes-from-alist-of-acons
(equal (update key
val
(from-alist alist))
(from-alist (acons key val alist)))
:by from-alist-of-acons)
other
(theory-invariant (incompatible! (:rewrite from-alist-of-acons) (:rewrite update-of-from-alist-becomes-from-alist-of-acons)))
other
(defrule from-alist-of-cons
(equal (from-alist (cons key-val alist))
(update (car key-val)
(cdr key-val)
(from-alist alist)))
:enable from-alist)
other
(theory-invariant (incompatible! (:rewrite from-alist-of-cons) (:rewrite update-of-from-alist-becomes-from-alist-of-acons)))
other
(defrule from-alist-of-remove-assoc-equal (implies (alistp alist) (equal (from-alist (remove-assoc-equal key alist)) (delete key (from-alist alist)))) :enable extensionality)
other
(defruled delete-of-from-alist-becomes-from-alist-of-remove-assoc-equal (implies (alistp alist) (equal (delete key (from-alist alist)) (from-alist (remove-assoc-equal key alist)))) :enable extensionality)
other
(theory-invariant (incompatible! (:rewrite from-alist-of-remove-assoc-equal) (:rewrite delete-of-from-alist-becomes-from-alist-of-remove-assoc-equal)))
other
(defrule keys-of-from-alist (implies (alistp alist) (equal (keys (from-alist alist)) (mergesort (strip-cars alist)))) :enable (expensive-rules in-of-keys-to-assoc member-equal-of-strip-cars-iff))