pseudo-termp-lemmas

other

(in-package "ACL2")

pseudo-term-listp-cdrtheorem

(defthm pseudo-term-listp-cdr
  (implies (and (pseudo-termp x) (not (equal (car x) 'quote)))
    (pseudo-term-listp (cdr x))))

pseudo-termp-openertheorem

(defthm pseudo-termp-opener
  (implies (and (consp x)
      (symbolp (car x))
      (not (equal (car x) 'quote)))
    (equal (pseudo-termp x) (pseudo-term-listp (cdr x)))))

pseudo-term-listp-of-atomtheorem

(defthm pseudo-term-listp-of-atom
  (implies (not (consp x))
    (equal (pseudo-term-listp x) (equal x nil)))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

pseudo-term-listp-of-constheorem

(defthm pseudo-term-listp-of-cons
  (equal (pseudo-term-listp (cons a x))
    (and (pseudo-termp a) (pseudo-term-listp x))))

pseudo-termp-list-cdrtheorem

(defthm pseudo-termp-list-cdr
  (implies (pseudo-term-listp x) (pseudo-term-listp (cdr x))))

pseudo-termp-cartheorem

(defthm pseudo-termp-car
  (implies (pseudo-term-listp x) (pseudo-termp (car x))))

pseudo-termp-cadr-from-pseudo-term-listptheorem

(defthm pseudo-termp-cadr-from-pseudo-term-listp
  (implies (pseudo-term-listp x) (pseudo-termp (cadr x))))

pseudo-term-listp-appendtheorem

(defthm pseudo-term-listp-append
  (implies (and (pseudo-term-listp x) (pseudo-term-listp y))
    (pseudo-term-listp (append x y))))

pseudo-term-substpfunction

(defund pseudo-term-substp
  (x)
  (declare (xargs :guard t))
  (if (atom x)
    (eq x nil)
    (and (consp (car x))
      (symbolp (caar x))
      (pseudo-termp (cdar x))
      (pseudo-term-substp (cdr x)))))

local

(local (in-theory (enable pseudo-term-substp)))

pseudo-termp-of-lookup-in-substtheorem

(defthm pseudo-termp-of-lookup-in-subst
  (implies (pseudo-term-substp x)
    (pseudo-termp (cdr (assoc k x)))))

pseudo-term-substp-of-aconstheorem

(defthm pseudo-term-substp-of-acons
  (equal (pseudo-term-substp (cons (cons k v) x))
    (and (symbolp k) (pseudo-termp v) (pseudo-term-substp x))))

pseudo-term-substp-of-atomtheorem

(defthm pseudo-term-substp-of-atom
  (implies (not (consp x))
    (equal (pseudo-term-substp x) (equal x nil)))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

pseudo-term-substp-of-pairlistheorem

(defthm pseudo-term-substp-of-pairlis
  (implies (and (symbol-listp x) (pseudo-term-listp y))
    (pseudo-term-substp (pairlis$ x y))))

pseudo-term-substp-of-appendtheorem

(defthm pseudo-term-substp-of-append
  (implies (and (pseudo-term-substp a) (pseudo-term-substp b))
    (pseudo-term-substp (append a b))))

pseudo-term-val-alistpfunction

(defund pseudo-term-val-alistp
  (x)
  (declare (xargs :guard t))
  (if (atom x)
    (eq x nil)
    (and (consp (car x))
      (pseudo-termp (cdar x))
      (pseudo-term-val-alistp (cdr x)))))

local

(local (in-theory (enable pseudo-term-val-alistp)))

pseudo-termp-of-lookup-in-pseudo-term-val-alistptheorem

(defthm pseudo-termp-of-lookup-in-pseudo-term-val-alistp
  (implies (pseudo-term-val-alistp x)
    (pseudo-termp (cdr (assoc k x)))))

pseudo-term-val-alistp-of-aconstheorem

(defthm pseudo-term-val-alistp-of-acons
  (equal (pseudo-term-val-alistp (cons (cons k v) x))
    (and (pseudo-termp v) (pseudo-term-val-alistp x))))

pseudo-term-val-alistp-of-atomtheorem

(defthm pseudo-term-val-alistp-of-atom
  (implies (not (consp x))
    (equal (pseudo-term-val-alistp x) (equal x nil)))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

pseudo-term-val-alistp-of-pairlistheorem

(defthm pseudo-term-val-alistp-of-pairlis
  (implies (pseudo-term-listp y)
    (pseudo-term-val-alistp (pairlis$ x y))))

pseudo-term-val-alistp-of-appendtheorem

(defthm pseudo-term-val-alistp-of-append
  (implies (and (pseudo-term-val-alistp a) (pseudo-term-val-alistp b))
    (pseudo-term-val-alistp (append a b))))