assoc-equal - ACL2 Book

other

(in-package "ACL2")

in-theory

(in-theory (disable assoc-equal))

assoc-equal-of-niltheorem

(defthm assoc-equal-of-nil
  (equal (assoc-equal x nil) nil)
  :hints (("Goal" :in-theory (enable assoc-equal))))

assoc-equal-when-not-consptheorem

(defthmd assoc-equal-when-not-consp
  (implies (not (consp alist))
    (equal (assoc-equal x alist) nil))
  :hints (("Goal" :in-theory (enable assoc-equal))))

assoc-equal-when-not-consp-cheaptheorem

(defthm assoc-equal-when-not-consp-cheap
  (implies (not (consp alist))
    (equal (assoc-equal x alist) nil))
  :rule-classes ((:rewrite :backchain-limit-lst (0)))
  :hints (("Goal" :in-theory (enable assoc-equal))))

assoc-equal-of-constheorem

(defthmd assoc-equal-of-cons
  (equal (assoc-equal x (cons pair alist))
    (if (equal x (car pair))
      pair
      (assoc-equal x alist)))
  :hints (("Goal" :in-theory (enable assoc-equal))))

assoc-equal-of-cons-safetheorem

(defthm assoc-equal-of-cons-safe
  (implies (syntaxp (not (and (quotep pair) (quotep alist))))
    (equal (assoc-equal x (cons pair alist))
      (if (equal x (car pair))
        pair
        (assoc-equal x alist))))
  :hints (("Goal" :in-theory (enable assoc-equal))))

assoc-equal-of-aconstheorem

(defthm assoc-equal-of-acons
  (equal (assoc-equal x (acons key datum alist))
    (if (equal x key)
      (cons x datum)
      (assoc-equal x alist)))
  :hints (("Goal" :in-theory (enable assoc-equal))))

assoc-equal-of-acons-difftheorem

(defthm assoc-equal-of-acons-diff
  (implies (not (equal x key))
    (equal (assoc-equal x (acons key datum alist))
      (assoc-equal x alist))))

assoc-equal-of-acons-sametheorem

(defthm assoc-equal-of-acons-same
  (equal (assoc-equal x (acons x datum alist)) (cons x datum)))

assoc-equal-of-append-1theorem

(defthm assoc-equal-of-append-1
  (implies (assoc-equal x alist1)
    (equal (assoc-equal x (append alist1 alist2))
      (assoc-equal x alist1)))
  :hints (("Goal" :in-theory (enable assoc-equal))))

assoc-equal-of-append-2theorem

(defthm assoc-equal-of-append-2
  (implies (and (not (assoc-equal x alist1)) (or (alistp alist1) x))
    (equal (assoc-equal x (append alist1 alist2))
      (assoc-equal x alist2)))
  :hints (("Goal" :in-theory (enable assoc-equal))))

assoc-equal-of-appendtheorem

(defthm assoc-equal-of-append
  (implies (or (alistp alist1) x)
    (equal (assoc-equal x (append alist1 alist2))
      (if (assoc-equal x alist1)
        (assoc-equal x alist1)
        (assoc-equal x alist2))))
  :hints (("Goal" :in-theory (enable assoc-equal))))

consp-of-assoc-equal-gentheorem

(defthm consp-of-assoc-equal-gen
  (implies (or (alistp alist) key)
    (iff (consp (assoc-equal key alist))
      (assoc-equal key alist)))
  :hints (("Goal" :in-theory (enable alistp assoc-equal))))

assoc-equal-iff-member-equal-of-strip-carstheorem

(defthmd assoc-equal-iff-member-equal-of-strip-cars
  (implies (or (alistp alist) key)
    (iff (assoc-equal key alist)
      (member-equal key (strip-cars alist))))
  :hints (("Goal" :in-theory (enable assoc-equal))))

assoc-equal-when-member-equal-of-strip-cars-iff-cheaptheorem

(defthm assoc-equal-when-member-equal-of-strip-cars-iff-cheap
  (implies (and (syntaxp (not (equal key ''nil)))
      (member-equal key (strip-cars alist)))
    (iff (assoc-equal key alist)
      (if (equal nil key)
        (assoc-equal nil alist)
        t)))
  :rule-classes ((:rewrite :backchain-limit-lst (nil 0)))
  :hints (("Goal" :in-theory (enable assoc-equal member-equal))))

member-equal-of-strip-cars-iff-assoc-equaltheorem

(defthmd member-equal-of-strip-cars-iff-assoc-equal
  (implies (or (alistp alist) key)
    (iff (member-equal key (strip-cars alist))
      (assoc-equal key alist)))
  :hints (("Goal" :in-theory (enable assoc-equal))))

member-equal-of-strip-cars-when-assoc-equaltheorem

(defthmd member-equal-of-strip-cars-when-assoc-equal
  (implies (assoc-equal key alist)
    (member-equal key (strip-cars alist)))
  :hints (("Goal" :in-theory (enable assoc-equal))))

other

(theory-invariant (incompatible (:rewrite assoc-equal-iff-member-equal-of-strip-cars)
    (:rewrite member-equal-of-strip-cars-iff-assoc-equal)))

assoc-equal-typetheorem

(defthm assoc-equal-type
  (implies (or x (alistp alist))
    (or (consp (assoc-equal x alist))
      (null (assoc-equal x alist))))
  :rule-classes :type-prescription :hints (("Goal" :in-theory (enable alistp assoc-equal))))

<-of-0-and-len-of-assoc-equal-ifftheorem

(defthm <-of-0-and-len-of-assoc-equal-iff
  (implies (alistp alist)
    (iff (< 0 (len (assoc-equal key alist)))
      (assoc-equal key alist))))

car-of-assoc-equal-cheaptheorem

(defthm car-of-assoc-equal-cheap
  (implies (assoc-equal x alist)
    (equal (car (assoc-equal x alist)) x))
  :rule-classes ((:rewrite :backchain-limit-lst (0)))
  :hints (("Goal" :in-theory (enable assoc-equal))))

car-of-assoc-equal-strongtheorem

(defthm car-of-assoc-equal-strong
  (equal (car (assoc-equal x alist))
    (if (assoc-equal x alist)
      x
      nil))
  :hints (("Goal" :in-theory (enable assoc-equal))))

acl2-count-of-assoc-equal-lineartheorem

(defthm acl2-count-of-assoc-equal-linear
  (<= (acl2-count (assoc-equal x alist)) (acl2-count alist))
  :rule-classes :linear :hints (("Goal" :in-theory (enable assoc-equal))))

acl2-count-of-assoc-equal-when-consp-lineartheorem

(defthm acl2-count-of-assoc-equal-when-consp-linear
  (implies (or (assoc-equal x alist) (consp alist))
    (< (acl2-count (assoc-equal x alist)) (acl2-count alist)))
  :rule-classes :linear :hints (("Goal" :in-theory (enable assoc-equal))))