Filtering...

assoc

books/std/omaps/assoc
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
(defruled assoc-of-head-key
  (equal (assoc (mv-nth 0 (head map)) map)
    (if (emptyp map)
      nil
      (cons (mv-nth 0 (head map))
        (mv-nth 1 (head map)))))
  :enable assoc)
other
(defruled assoc-when-assoc-of-tail
  (implies (assoc key (tail map))
    (equal (assoc key map)
      (assoc key (tail map))))
  :by assoc-of-tail-when-assoc-of-tail)
other
(theory-invariant (incompatible! (:rewrite assoc-of-tail-when-assoc-of-tail)
    (:rewrite assoc-when-assoc-of-tail)))
other
(defrule assoc-when-assoc-of-tail-cheap
  (implies (assoc key (tail map))
    (equal (assoc key map)
      (assoc key (tail map))))
  :rule-classes ((:rewrite :backchain-limit-lst (0)))
  :by assoc-when-assoc-of-tail)
other
(theory-invariant (incompatible! (:rewrite assoc-of-tail-when-assoc-of-tail)
    (:rewrite assoc-when-assoc-of-tail-cheap)))
other
(defruled assoc-when-<<-head
  (implies (<< (mv-nth 0 (head map)) key)
    (equal (assoc key map)
      (assoc key (tail map)))))
other
(defruled head-key-minimal-2
  (implies (assoc key map)
    (not (<< key (mv-nth 0 (head map)))))
  :by head-key-minimal)
other
(defruled head-key-minimal-3
  (implies (assoc key (tail map))
    (<< (mv-nth 0 (head map)) key))
  :enable head-key-minimal-2
  :disable <<-trichotomy
  :use (:instance <<-trichotomy
    (y key)
    (x (mv-nth 0 (head map)))))
other
(defrule set-in-of-rlookup
  (equal (in key (rlookup val map))
    (and (assoc key map)
      (equal (cdr (assoc key map)) val)))
  :induct t
  :enable rlookup)