Filtering...

alists-compatible

books/std/alists/alists-compatible

Included Books

alist-equiv hons-assoc-equal
other
(in-package "ACL2")
include-book
(include-book "alist-equiv")
local
(local (include-book "hons-assoc-equal"))
alists-compatible-on-keysfunction
(defun alists-compatible-on-keys
  (keys a b)
  (declare (xargs :guard t))
  (or (atom keys)
    (and (let ((alook (hons-get (car keys) a)) (blook (hons-get (car keys) b)))
        (or (not alook) (not blook) (equal alook blook)))
      (alists-compatible-on-keys (cdr keys) a b))))
alists-compatible-on-keys-of-list-fixtheorem
(defthm alists-compatible-on-keys-of-list-fix
  (equal (alists-compatible-on-keys (list-fix keys) a b)
    (alists-compatible-on-keys keys a b)))
other
(defcong list-equiv
  equal
  (alists-compatible-on-keys keys a b)
  1
  :hints (("Goal" :in-theory (e/d (list-equiv) (alists-compatible-on-keys-of-list-fix))
     :use ((:instance alists-compatible-on-keys-of-list-fix
        (keys keys)) (:instance alists-compatible-on-keys-of-list-fix
         (keys keys-equiv))))))
alists-compatiblefunction
(defund alists-compatible
  (a b)
  (declare (xargs :guard t))
  (alists-compatible-on-keys (alist-keys a) a b))
local
(local (defthm member-intersection
    (iff (member x (intersection-equal a b))
      (and (member x a) (member x b)))))
alists-compatible-on-keys-in-terms-of-alists-agreetheorem
(defthmd alists-compatible-on-keys-in-terms-of-alists-agree
  (equal (alists-compatible-on-keys keys a b)
    (alists-agree (intersection-equal keys
        (intersection-equal (alist-keys a) (alist-keys b)))
      a
      b))
  :hints (("Goal" :in-theory (enable alists-compatible-on-keys
       alists-agree
       alist-keys
       intersection-equal)))
  :rule-classes :definition)
local
(local (defthm intersection-equal-repeat-1
    (implies (subsetp-equal a b)
      (equal (intersection-equal a (intersection-equal b c))
        (intersection-equal a c)))
    :hints (("Goal" :in-theory (enable intersection-equal)))))
local
(local (defthm subsetp-equal-cons
    (implies (subsetp-equal a b) (subsetp-equal a (cons x b)))))
local
(local (defthm subsetp-equal-refl (subsetp-equal a a)))
local
(local (defthm intersection-equal-repeat
    (equal (intersection-equal a (intersection-equal a c))
      (intersection-equal a c))))
alists-compatible-in-terms-of-alists-agreetheorem
(defthmd alists-compatible-in-terms-of-alists-agree
  (equal (alists-compatible a b)
    (alists-agree (intersection-equal (alist-keys a) (alist-keys b))
      a
      b))
  :hints (("Goal" :in-theory (enable alists-compatible
       alists-compatible-on-keys-in-terms-of-alists-agree
       alists-agree
       alist-keys
       intersection-equal)))
  :rule-classes :definition)
local
(local (in-theory (enable alists-compatible-in-terms-of-alists-agree)))
alists-incompatible-witnessfunction
(defund alists-incompatible-witness
  (a b)
  (alists-disagree-witness (intersection-equal (alist-keys a) (alist-keys b))
    a
    b))
local
(local (in-theory (enable alists-incompatible-witness)))
local
(local (defthm member-intersection-equal
    (iff (member x (intersection-equal a b))
      (and (member x a) (member x b)))))
alists-compatible-iff-agree-on-bad-guytheorem
(defthmd alists-compatible-iff-agree-on-bad-guy
  (iff (alists-compatible a b)
    (let ((x (alists-incompatible-witness a b)))
      (implies (and (hons-assoc-equal x a) (hons-assoc-equal x b))
        (equal (hons-assoc-equal x a) (hons-assoc-equal x b)))))
  :hints (("Goal" :in-theory (enable alists-agree-iff-witness))))
alists-compatible-iff-agree-on-bad-guy-concltheorem
(defthmd alists-compatible-iff-agree-on-bad-guy-concl
  (implies (syntaxp (let ((a a) (b b) (mfc mfc) (state state))
        (declare (ignore state))
        (member-equal `(alists-compatible ,A ,B) (mfc-clause mfc))))
    (iff (alists-compatible a b)
      (let ((x (alists-incompatible-witness a b)))
        (implies (and (hons-assoc-equal x a) (hons-assoc-equal x b))
          (equal (hons-assoc-equal x a) (hons-assoc-equal x b))))))
  :hints (("Goal" :in-theory (enable alists-agree-iff-witness))))
alists-compatible-hons-assoc-equaltheorem
(defthmd alists-compatible-hons-assoc-equal
  (implies (and (alists-compatible a b)
      (hons-assoc-equal x a)
      (hons-assoc-equal x b))
    (equal (hons-assoc-equal x a) (hons-assoc-equal x b)))
  :hints (("Goal" :in-theory (enable alists-agree-hons-assoc-equal))))
local
(local (in-theory (enable cons-key-cdr-hons-assoc-equal)))
local
(local (in-theory (disable alists-compatible-in-terms-of-alists-agree)))
alists-compatible-acons-1theorem
(defthm alists-compatible-acons-1
  (implies (alists-compatible a b)
    (iff (alists-compatible (cons (cons key val) a) b)
      (or (not (hons-assoc-equal key b))
        (equal (cdr (hons-assoc-equal key b)) val))))
  :hints (("Goal" :in-theory (e/d (alists-compatible-iff-agree-on-bad-guy-concl alists-compatible-hons-assoc-equal)
       (alists-incompatible-witness))
     :use ((:instance alists-compatible-hons-assoc-equal
        (x key)
        (a (cons (cons key val) a))
        (b b)))
     :do-not-induct t))
  :otf-flg t)
alists-compatible-acons-2theorem
(defthm alists-compatible-acons-2
  (implies (alists-compatible a b)
    (iff (alists-compatible a (cons (cons key val) b))
      (or (not (hons-assoc-equal key a))
        (equal (cdr (hons-assoc-equal key a)) val))))
  :hints (("Goal" :in-theory (e/d (alists-compatible-iff-agree-on-bad-guy-concl alists-compatible-hons-assoc-equal)
       (alists-incompatible-witness))
     :use ((:instance alists-compatible-hons-assoc-equal
        (x key)
        (a (cons (cons key val) a))
        (b b)))
     :do-not-induct t))
  :otf-flg t)
alists-compatible-append-1theorem
(defthm alists-compatible-append-1
  (implies (alists-compatible a b)
    (iff (alists-compatible (append c a) b)
      (alists-compatible c b)))
  :hints (("Goal" :in-theory (e/d (alists-compatible-iff-agree-on-bad-guy-concl alists-compatible-hons-assoc-equal)
       (alists-incompatible-witness))
     :use ((:instance alists-compatible-hons-assoc-equal
        (x (alists-incompatible-witness c b))
        (a (append c a))
        (b b)))
     :do-not-induct t)))
alists-compatible-append-2theorem
(defthm alists-compatible-append-2
  (implies (alists-compatible a b)
    (iff (alists-compatible a (append c b))
      (alists-compatible a c)))
  :hints (("Goal" :in-theory (e/d (alists-compatible-iff-agree-on-bad-guy-concl alists-compatible-hons-assoc-equal)
       (alists-compatible alists-incompatible-witness))
     :use ((:instance alists-compatible-hons-assoc-equal
        (x (alists-incompatible-witness a c))
        (a a)
        (b (append c b))))
     :do-not-induct t)))
other
(defsection alists-compatible-on-keys
  (local (in-theory (enable alists-compatible-on-keys)))
  (defthm alists-compatible-on-keys-refl
    (alists-compatible-on-keys keys a a))
  (defthmd alists-compatible-on-keys-sym
    (implies (alists-compatible-on-keys keys b a)
      (alists-compatible-on-keys keys a b)))
  (defthmd alists-compatible-on-keys-hons-assoc-equal
    (implies (and (alists-compatible-on-keys keys a b)
        (member-equal x keys)
        (hons-assoc-equal x a)
        (hons-assoc-equal x b))
      (equal (cdr (hons-assoc-equal x a))
        (cdr (hons-assoc-equal x b)))))
  (defun alists-incompatible-on-keys-witness
    (keys a b)
    (if (atom keys)
      nil
      (if (let ((alook (hons-get (car keys) a)) (blook (hons-get (car keys) b)))
          (and alook blook (not (equal alook blook))))
        (car keys)
        (alists-incompatible-on-keys-witness (cdr keys) a b))))
  (defthmd alists-incompatible-on-keys-witness-correct
    (equal (alists-compatible-on-keys keys a b)
      (let ((witness (alists-incompatible-on-keys-witness keys a b)))
        (not (and (member-equal witness keys)
            (hons-assoc-equal witness a)
            (hons-assoc-equal witness b)
            (not (equal (cdr (hons-assoc-equal witness a))
                (cdr (hons-assoc-equal witness b))))))))
    :hints (("Goal" :in-theory (enable car-hons-assoc-equal-split))))
  (defthmd alists-compatible-on-keys-alist-keys
    (implies (alists-compatible-on-keys (alist-keys a) a b)
      (alists-compatible-on-keys (alist-keys b) a b))
    :hints (("Goal" :use ((:instance alists-incompatible-on-keys-witness-correct
          (keys (alist-keys b))) (:instance alists-compatible-on-keys-hons-assoc-equal
           (keys (alist-keys a))
           (x (alists-incompatible-on-keys-witness (alist-keys b) a b))))
       :do-not-induct t))))
local
(local (in-theory (enable alists-compatible)))
alists-compatible-refltheorem
(defthm alists-compatible-refl (alists-compatible a a))
alists-compatible-symtheorem
(defthmd alists-compatible-sym
  (implies (alists-compatible a b) (alists-compatible b a))
  :hints (("goal" :in-theory (enable alists-compatible-on-keys-alist-keys
       alists-compatible-on-keys-sym))))
alists-compatible-on-keys-niltheorem
(defthm alists-compatible-on-keys-nil
  (alists-compatible-on-keys keys a nil))
alists-compatible-niltheorem
(defthm alists-compatible-nil
  (and (alists-compatible a nil) (alists-compatible nil a)))