Filtering...

fast-alists

books/centaur/misc/fast-alists

Included Books

alist-fix alist-witness equal-sets universal-equiv top
other
(in-package "ACL2")
include-book
(include-book "std/alists/alist-fix" :dir :system)
include-book
(include-book "alist-witness")
include-book
(include-book "equal-sets")
include-book
(include-book "universal-equiv")
include-book
(include-book "std/alists/top" :dir :system)
other
(defsection al-shrink
  (defthm hons-assoc-equal-hshrink-alist
    (equal (hons-assoc-equal key (hshrink-alist a b))
      (or (hons-assoc-equal key b) (hons-assoc-equal key a)))
    :hints (("Goal" :in-theory (enable hons-assoc-equal hons-shrink-alist))))
  (defthmd hons-assoc-equal-al-shrink
    (equal (hons-assoc-equal key (al-shrink a))
      (hons-assoc-equal key a))
    :hints (("Goal" :in-theory (enable al-shrink))))
  (defthm alist-equiv-al-shrink
    (alist-equiv (al-shrink a) a)
    :hints (("Goal" :in-theory (enable alist-equiv-iff-agree-on-bad-guy
         hons-assoc-equal-al-shrink)))))
associativity-of-appendtheorem
(defthm associativity-of-append
  (equal (append (append a b) c) (append a (append b c))))
hshrink-alist-alist-equiv-appendtheorem
(defthm hshrink-alist-alist-equiv-append
  (alist-equiv (hons-shrink-alist a b) (append b a))
  :hints (("Goal" :in-theory (enable alist-equiv-iff-agree-on-bad-guy))))
hons-assoc-equal-make-faltheorem
(defthm hons-assoc-equal-make-fal
  (equal (hons-assoc-equal x (make-fal a b))
    (or (hons-assoc-equal x a) (hons-assoc-equal x b))))
make-fal-alist-equiv-appendtheorem
(defthm make-fal-alist-equiv-append
  (alist-equiv (make-fal a b) (append a b))
  :hints (("Goal" :in-theory (enable alist-equiv-iff-agree-on-bad-guy))))
in-theory
(in-theory (disable car-hons-assoc-equal-split))
other
(defcong set-equiv
  alist-equiv
  (fal-extract keys al)
  1
  :hints (("Goal" :in-theory (enable fal-extract alist-equiv-iff-agree-on-bad-guy)) (set-reasoning)))
alist-keys-hons-put-listtheorem
(defthm alist-keys-hons-put-list
  (set-equiv (alist-keys (hons-put-list vars vals rest))
    (union-equal vars (alist-keys rest)))
  :hints (("goal" :in-theory (enable alist-keys append)) (set-reasoning)))
alist-fix-alist-equivtheorem
(defthm alist-fix-alist-equiv
  (alist-equiv (alist-fix a) a)
  :hints (("Goal" :in-theory (enable alist-equiv-iff-agree-on-bad-guy))))
other
(defn nonempty-alistp
  (x)
  (and (consp x)
    (or (consp (car x)) (nonempty-alistp (cdr x)))))
other
(defn first-key
  (x)
  (and (consp x)
    (if (consp (car x))
      (caar x)
      (first-key (cdr x)))))
nonempty-alistp-first-keytheorem
(defthmd nonempty-alistp-first-key
  (iff (nonempty-alistp a) (hons-assoc-equal (first-key a) a)))
empty-alist-hons-assoc-equaltheorem
(defthmd empty-alist-hons-assoc-equal
  (implies (not (nonempty-alistp a))
    (not (hons-assoc-equal x a)))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))
other
(defcong alist-equiv
  equal
  (nonempty-alistp a)
  1
  :hints (("Goal" :use ((:instance nonempty-alistp-first-key) (:instance empty-alist-hons-assoc-equal
         (x (first-key a))
         (a a-equiv))
       (:instance nonempty-alistp-first-key (a a-equiv))
       (:instance empty-alist-hons-assoc-equal
         (x (first-key a-equiv)))))))
other
(defn al-covers-keys
  (keys al)
  (or (atom keys)
    (and (hons-get (car keys) al)
      (al-covers-keys (cdr keys) al))))
al-covers-keys-to-subsettheorem
(defthm al-covers-keys-to-subset
  (equal (al-covers-keys keys al)
    (subsetp-equal keys (alist-keys al)))
  :hints (("Goal" :in-theory (enable subsetp-equal))))
other
(defcong alist-equiv equal (al-covers-keys keys al) 2)
other
(defcong set-equiv
  equal
  (al-covers-keys keys al)
  1
  :hints (("goal" :in-theory (disable set-equiv))))
other
(defsection hons-acons-each
  (local (in-theory (enable hons-acons-each)))
  (defthm hons-assoc-equal-hons-acons-each
    (equal (hons-assoc-equal x (hons-acons-each keys val rest))
      (if (member-equal x keys)
        (cons x val)
        (hons-assoc-equal x rest))))
  (defthm alist-keys-hons-acons-each
    (equal (alist-keys (hons-acons-each keys val rest))
      (append keys (alist-keys rest)))))
other
(defsection keys-equiv
  (def-universal-equiv keys-equiv
    :qvars k
    :equiv-terms ((iff (hons-assoc-equal k x)))
    :defquant t
    :witness-dcls ((declare (xargs :guard t :verify-guards nil))))
  (defexample keys-equiv-example
    :pattern (hons-assoc-equal k x)
    :templates (k)
    :instance-rulename keys-equiv-instancing)
  (verify-guards keys-equiv)
  (defcong keys-equiv
    iff
    (hons-assoc-equal k x)
    2
    :hints ((witness)))
  (defcong keys-equiv
    set-equiv
    (alist-keys x)
    1
    :hints (("Goal" :in-theory (e/d nil (set-equiv))) (witness)))
  (defthm keys-equiv-when-alist-keys
    (implies (set-equiv (double-rewrite (alist-keys env1))
        (double-rewrite (alist-keys env2)))
      (equal (keys-equiv env1 env2) t))
    :hints (("Goal" :in-theory (e/d (hons-assoc-equal-iff-member-alist-keys)
         (set-equiv alist-keys-member-hons-assoc-equal))) (witness))))