symbol-alistp - ACL2 Book

other

(in-package "ACL2")

symbol-alistp-of-constheorem

(defthm symbol-alistp-of-cons
  (equal (symbol-alistp (cons pair alist))
    (and (consp pair)
      (symbolp (car pair))
      (symbol-alistp alist)))
  :hints (("Goal" :in-theory (enable symbol-alistp))))

symbol-alistp-of-aconstheorem

(defthm symbol-alistp-of-acons
  (equal (symbol-alistp (acons key val alist))
    (and (symbolp key) (symbol-alistp alist)))
  :hints (("Goal" :in-theory (enable symbol-alistp acons))))

symbol-alistp-of-appendtheorem

(defthm symbol-alistp-of-append
  (equal (symbol-alistp (append x y))
    (and (symbol-alistp (true-list-fix x)) (symbol-alistp y)))
  :hints (("Goal" :in-theory (enable true-list-fix))))

symbol-alistp-of-union-equaltheorem

(defthm symbol-alistp-of-union-equal
  (implies (and (symbol-alistp x) (symbol-alistp y))
    (symbol-alistp (union-equal x y)))
  :hints (("Goal" :in-theory (enable union-equal))))

symbol-alistp-of-cdrtheorem

(defthm symbol-alistp-of-cdr
  (implies (symbol-alistp alist) (symbol-alistp (cdr alist)))
  :hints (("Goal" :in-theory (enable symbol-alistp))))

symbol-alistp-of-taketheorem

(defthm symbol-alistp-of-take
  (implies (symbol-alistp alist)
    (equal (symbol-alistp (take n alist))
      (<= (nfix n) (len alist))))
  :hints (("Goal" :in-theory (enable symbol-alistp take))))

symbol-alistp-of-nthcdrtheorem

(defthm symbol-alistp-of-nthcdr
  (implies (symbol-alistp alist)
    (symbol-alistp (nthcdr n alist)))
  :hints (("Goal" :in-theory (enable symbol-alistp nthcdr))))

symbolp-of-car-of-car-when-symbol-alistptheorem

(defthmd symbolp-of-car-of-car-when-symbol-alistp
  (implies (symbol-alistp alist) (symbolp (car (car alist))))
  :hints (("Goal" :in-theory (enable symbol-alistp))))

symbolp-of-car-of-car-when-symbol-alistp-cheaptheorem

(defthm symbolp-of-car-of-car-when-symbol-alistp-cheap
  (implies (symbol-alistp alist) (symbolp (car (car alist))))
  :rule-classes ((:rewrite :backchain-limit-lst (0)))
  :hints (("Goal" :in-theory (enable symbol-alistp))))

symbol-listp-of-strip-cars-when-symbol-alistptheorem

(defthm symbol-listp-of-strip-cars-when-symbol-alistp
  (implies (symbol-alistp alist)
    (symbol-listp (strip-cars alist)))
  :hints (("Goal" :in-theory (enable symbol-listp strip-cars))))

symbol-listp-of-strip-cars-when-symbol-alistp-cheaptheorem

(defthm symbol-listp-of-strip-cars-when-symbol-alistp-cheap
  (implies (symbol-alistp alist)
    (symbol-listp (strip-cars alist)))
  :rule-classes ((:rewrite :backchain-limit-lst (0))))

symbol-alistp-of-pairlis$-alttheorem

(defthm symbol-alistp-of-pairlis$-alt
  (implies (symbol-listp symbols)
    (symbol-alistp (pairlis$ symbols vals))))

symbol-alistp-forward-to-alistptheorem

(defthm symbol-alistp-forward-to-alistp
  (implies (symbol-alistp x) (alistp x))
  :rule-classes :forward-chaining)

true-listp-when-symbol-alistptheorem

(defthmd true-listp-when-symbol-alistp
  (implies (symbol-alistp x) (true-listp x)))

alistp-when-symbol-alistptheorem

(defthmd alistp-when-symbol-alistp
  (implies (symbol-alistp x) (alistp x)))

symbol-alistp-of-revappendtheorem

(defthm symbol-alistp-of-revappend
  (equal (symbol-alistp (revappend x y))
    (and (symbol-alistp (true-list-fix x)) (symbol-alistp y)))
  :hints (("Goal" :in-theory (enable revappend))))