Filtering...

delete

books/std/omaps/delete
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
(defrule assoc-of-delete
  (equal (assoc x (delete y map))
    (if (equal x y)
      nil
      (assoc x map)))
  :induct t
  :enable delete)
other
(defrule lookup-of-delete
  (equal (lookup x (delete y map))
    (if (equal x y)
      nil
      (lookup x map)))
  :enable lookup)
other
(defrule assoc-of-delete*
  (equal (assoc key (delete* keys map))
    (if (in key keys)
      nil
      (assoc key map)))
  :induct t
  :enable delete*)
other
(defrule lookup-of-delete*
  (equal (lookup key (delete* keys map))
    (if (in key keys)
      nil
      (lookup key map)))
  :enable lookup)
other
(defrule delete-when-not-assoc
  (implies (not (assoc key map))
    (equal (delete key map) (mfix map)))
  :enable extensionality)
other
(defrule idempotence-of-delete
  (equal (delete key (delete key map))
    (delete key map)))
other
(defrule commutativity-of-delete
  (equal (delete y (delete x map))
    (delete x (delete y map)))
  :enable extensionality)
other
(defrule delete-of-update
  (equal (delete key (update key val map))
    (delete key map))
  :enable extensionality)
other
(defrule submap-of-delete
  (submap (delete key map) map)
  :enable pick-a-point)
other
(defrule submap-of-delete*
  (submap (delete* key map) map)
  :enable pick-a-point)
other
(defrule compatiblep-of-delete
  (implies (compatiblep map0 map1)
    (compatiblep map0 (delete key map1))))
other
(defrule compatiblep-of-delete-same
  (compatiblep map (delete key map)))
other
(defrule keys-of-delete
  (equal (keys (delete key map))
    (delete key (keys map)))
  :enable (expensive-rules in-of-keys-to-assoc))
other
(defrule keys-of-delete*
  (equal (keys (delete* keys map))
    (difference (keys map) keys))
  :enable (expensive-rules in-of-keys-to-assoc))
other
(defruled size-of-delete
  (equal (size (delete key map))
    (if (assoc key map)
      (- (size map) 1)
      (size map)))
  :enable (size-to-cardinality-of-keys delete-cardinality
    in-of-keys-to-assoc))
other
(defrule size-of-delete-linear
  (<= (size (delete key map)) (size map))
  :rule-classes :linear :enable size-of-delete)
other
(defrule size-of-delete-when-assoc-linear
  (implies (assoc key map)
    (< (size (delete key map)) (size map)))
  :rule-classes :linear :enable size-of-delete)
other
(defrule size-of-delete*-linear
  (<= (size (delete* keys map))
    (size map))
  :rule-classes :linear :induct t
  :enable delete*)