Filtering...

from-lists

books/std/omaps/from-lists
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
(include-book "core")
other
(include-book "with-fixing-theorems")
other
(include-book "assoc")
other
(include-book "submap")
other
(include-book "extensionality")
other
(include-book "compatiblep")
other
(include-book "delete")
other
(include-book "update")
other
(include-book "from-alist")
other
(defruled assoc-of-car-of-from-lists
  (equal (assoc (car keys)
      (from-lists keys vals))
    (if (consp keys)
      (cons (car keys) (car vals))
      nil))
  :enable from-lists)
other
(defrule assoc-of-car-of-from-lists-when-consp
  (implies (consp keys)
    (equal (assoc (car keys)
        (from-lists keys vals))
      (cons (car keys) (car vals))))
  :by assoc-of-car-of-from-lists)
other
(defrule assoc-of-from-lists-under-iff
  (iff (assoc key (from-lists keys vals))
    (member-equal key keys))
  :induct t
  :enable (from-lists member-equal))
other
(defrule assoc-of-from-lists-when-not-member-equal-cheap
  (implies (not (member-equal key keys))
    (not (assoc key (from-lists keys vals))))
  :rule-classes ((:rewrite :backchain-limit-lst (0))))