Filtering...

compatiblep

books/std/omaps/compatiblep
other
(in-package "OMAP")
other
(include-book "std/util/define-sk" :dir :system)
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
(defruled compatiblep-of-tail-when-compatiblep
  (implies (compatiblep map0 map1)
    (compatiblep (tail map0) map1))
  :enable compatiblep)
other
(defrule compatiblep-of-tail-when-compatiblep-cheap
  (implies (compatiblep map0 map1)
    (compatiblep (tail map0) map1))
  :rule-classes ((:rewrite :backchain-limit-lst (0)))
  :by compatiblep-of-tail-when-compatiblep)
other
(defruled compatiblep-of-arg1-and-tail-when-compatiblep
  (implies (compatiblep map0 map1)
    (compatiblep map0 (tail map1)))
  :induct t
  :enable compatiblep)
other
(defrule compatiblep-of-arg1-and-tail-when-compatiblep-cheap
  (implies (compatiblep map0 map1)
    (compatiblep map0 (tail map1)))
  :rule-classes ((:rewrite :backchain-limit-lst (0)))
  :by compatiblep-of-arg1-and-tail-when-compatiblep)
other
(defruled assoc-when-compatiblep-and-assoc
  (implies (and (compatiblep map0 map1)
      (assoc key map0)
      (assoc key map1))
    (equal (assoc key map0)
      (assoc key map1)))
  :induct t
  :enable compatiblep
  :prep-lemmas ((defrule equal-of-assoc-and-cons
     (equal (equal (assoc key0 map) (cons key1 val))
       (and (assoc key0 map)
         (equal key0 key1)
         (equal (cdr (assoc key0 map)) val)))
     :induct t
     :enable assoc)))
other
(defrule assoc-when-compatiblep-and-assoc-syntaxp
  (implies (and (compatiblep map0 map1)
      (syntaxp (<< map1 map0))
      (assoc key map0)
      (assoc key map1))
    (equal (assoc key map0)
      (assoc key map1)))
  :by assoc-when-compatiblep-and-assoc)
other
(defrule equal-of-assoc-assoc-when-compatiblep
  (implies (compatiblep map0 map1)
    (equal (equal (assoc key map0)
        (assoc key map1))
      (iff (assoc key map0)
        (assoc key map1))))
  :use assoc-when-compatiblep-and-assoc)
other
(defrule compatiblep-when-submap
  (implies (submap sub sup)
    (compatiblep sub sup))
  :induct t
  :enable (compatiblep submap))
other
(defrule reflexivity-of-compatiblep
  (compatiblep map map))
other
(defruled symmetry-of-compatiblep-weak
  (implies (compatiblep map1 map0)
    (compatiblep map0 map1))
  :induct (compatiblep map0 map1)
  :enable compatiblep)
other
(defrule symmetry-of-compatiblep
  (equal (compatiblep map1 map0)
    (compatiblep map0 map1))
  :use (symmetry-of-compatiblep-weak (:instance symmetry-of-compatiblep-weak
      (map0 map1)
      (map1 map0))))
other
(defrule compatiblep-when-submap-2
  (implies (submap sub sup)
    (compatiblep sup sub)))
other
(defrule compatiblep-weaken-arg2
  (implies (and (compatiblep map sup)
      (submap sub sup))
    (compatiblep map sub))
  :induct (compatiblep map sub)
  :enable (compatiblep assoc-when-submap-and-assoc))
other
(defrule compatiblep-weaken-arg1
  (implies (and (compatiblep sup map)
      (submap sub sup))
    (compatiblep sub map)))