keyword-value-lists2

Included Books

other

(in-package "ACL2")

include-book

(include-book "keyword-value-listp")

include-book

(include-book "lookup-keyword")

keyword-value-listp-of-remove-keywordtheorem

(defthm keyword-value-listp-of-remove-keyword
  (implies (keyword-value-listp l)
    (keyword-value-listp (remove-keyword word l)))
  :hints (("Goal" :in-theory (enable keyword-value-listp))))

keyword-value-list-keysfunction

(defun keyword-value-list-keys
  (k)
  (declare (xargs :guard (keyword-value-listp k)))
  (if (endp k)
    nil
    (cons (car k) (keyword-value-list-keys (cddr k)))))

keyword-listp-of-keyword-value-list-keystheorem

(defthm keyword-listp-of-keyword-value-list-keys
  (implies (keyword-value-listp l)
    (keyword-listp (keyword-value-list-keys l)))
  :hints (("Goal" :in-theory (enable keyword-value-listp))))

symbol-listp-of-keyword-value-list-keystheorem

(defthm symbol-listp-of-keyword-value-list-keys
  (implies (keyword-value-listp l)
    (symbol-listp (keyword-value-list-keys l)))
  :hints (("Goal" :in-theory (enable keyword-value-listp))))