assoc-keyword - ACL2 Book

other

(in-package "ACL2")

in-theory

(in-theory (disable assoc-keyword))

consp-of-cdr-of-assoc-keywordtheorem

(defthm consp-of-cdr-of-assoc-keyword
  (implies (keyword-value-listp keyword-value-list)
    (iff (consp (cdr (assoc-keyword key keyword-value-list)))
      (assoc-keyword key keyword-value-list)))
  :hints (("Goal" :in-theory (enable keyword-value-listp assoc-keyword))))

cdr-of-assoc-keyword-ifftheorem

(defthm cdr-of-assoc-keyword-iff
  (implies (keyword-value-listp keyword-value-list)
    (iff (cdr (assoc-keyword key keyword-value-list))
      (assoc-keyword key keyword-value-list)))
  :hints (("Goal" :in-theory (enable keyword-value-listp assoc-keyword))))

keywordp-of-car-of-assoc-keywordtheorem

(defthm keywordp-of-car-of-assoc-keyword
  (implies (keyword-value-listp keyword-value-list)
    (iff (keywordp (car (assoc-keyword key keyword-value-list)))
      (assoc-keyword key keyword-value-list)))
  :hints (("Goal" :in-theory (enable keyword-value-listp assoc-keyword))))

keywordp-when-assoc-keywordtheorem

(defthm keywordp-when-assoc-keyword
  (implies (and (assoc-keyword key keyword-value-list)
      (keyword-value-listp keyword-value-list))
    (keywordp key))
  :hints (("Goal" :in-theory (enable keyword-value-listp assoc-keyword))))

symbolp-when-assoc-keywordtheorem

(defthmd symbolp-when-assoc-keyword
  (implies (and (assoc-keyword key keyword-value-list)
      (keyword-value-listp keyword-value-list))
    (symbolp key))
  :hints (("Goal" :in-theory (enable keyword-value-listp assoc-keyword))))

<=-of-len-of-assoc-keyword-forward-lineartheorem

(defthm <=-of-len-of-assoc-keyword-forward-linear
  (implies (and (assoc-keyword key keyword-value-list)
      (keyword-value-listp keyword-value-list))
    (<= 2 (len (assoc-keyword key keyword-value-list))))
  :rule-classes :linear :hints (("Goal" :in-theory (enable keyword-value-listp assoc-keyword))))

assoc-keyword-of-cons-sametheorem

(defthm assoc-keyword-of-cons-same
  (equal (assoc-keyword key (cons key lst)) (cons key lst))
  :hints (("Goal" :in-theory (enable assoc-keyword))))

assoc-keyword-of-cons-difftheorem

(defthm assoc-keyword-of-cons-diff
  (implies (not (equal key key2))
    (equal (assoc-keyword key (cons key2 lst))
      (assoc-keyword key (cdr lst))))
  :hints (("Goal" :in-theory (enable assoc-keyword))))