quote

other

(in-package "ACL2")

include-book

(include-book "myquotep")

local

(local (include-book "equal-of-booleans"))

other

(defun-inline unquote$
  (x)
  (declare (xargs :guard (myquotep x)))
  (unquote x))

enquotemacro

(defmacro enquote (val) `(list 'quote ,VAL))

all-myquotepfunction

(defund all-myquotep
  (items)
  (declare (xargs :guard (true-listp items)))
  (if (endp items)
    t
    (and (myquotep (first items)) (all-myquotep (rest items)))))

all-myquotep-of-cdr-cheaptheorem

(defthm all-myquotep-of-cdr-cheap
  (implies (all-myquotep lst) (all-myquotep (cdr lst)))
  :rule-classes ((:rewrite :backchain-limit-lst (0)))
  :hints (("Goal" :in-theory (enable all-myquotep))))

all-myquotep-of-constheorem

(defthm all-myquotep-of-cons
  (equal (all-myquotep (cons item lst))
    (and (myquotep item) (all-myquotep lst)))
  :hints (("Goal" :in-theory (enable all-myquotep))))

all-myquotep-when-not-consptheorem

(defthm all-myquotep-when-not-consp
  (implies (not (consp lst)) (all-myquotep lst))
  :hints (("Goal" :in-theory (enable all-myquotep))))

consp-of-cdr-of-nth-when-all-myquoteptheorem

(defthmd consp-of-cdr-of-nth-when-all-myquotep
  (implies (and (all-myquotep args) (natp n))
    (equal (consp (cdr (nth n args))) (< n (len args)))))

consp-of-nth-when-all-myquoteptheorem

(defthmd consp-of-nth-when-all-myquotep
  (implies (and (all-myquotep args) (natp n))
    (equal (consp (nth n args)) (< n (len args)))))

myquotep-when-all-myquotep-and-member-equaltheorem

(defthmd myquotep-when-all-myquotep-and-member-equal
  (implies (and (all-myquotep items) (member-equal item items))
    (myquotep item))
  :hints (("Goal" :in-theory (enable all-myquotep))))

Included Books