myquotep - ACL2 Book

other

(in-package "ACL2")

myquotepfunction

(defun myquotep
  (item)
  (declare (xargs :guard t))
  (and (quotep item)
    (consp (cdr item))
    (null (cdr (cdr item)))))

myquotep-forwardtheorem

(defthm myquotep-forward
  (implies (myquotep item) (equal (car item) 'quote))
  :rule-classes :forward-chaining)

myquotep-forward-to-consptheorem

(defthm myquotep-forward-to-consp
  (implies (myquotep item)
    (and (consp item) (true-listp item)))
  :rule-classes :forward-chaining)

myquotep-forward-to-quoteptheorem

(defthm myquotep-forward-to-quotep
  (implies (myquotep item) (quotep item))
  :rule-classes :forward-chaining)

myquotep-forward-to-equal-of-lentheorem

(defthm myquotep-forward-to-equal-of-len
  (implies (myquotep x) (equal 2 (len x)))
  :rule-classes :forward-chaining :hints (("Goal" :in-theory (enable myquotep))))

myquotep-of-list-of-quotetheorem

(defthm myquotep-of-list-of-quote
  (myquotep (list 'quote x))
  :hints (("Goal" :in-theory (enable myquotep))))