term-lemmas

other

(in-package "ACL2")

include-book

(include-book "term-defuns")

include-book

(include-book "pseudo-termp-lemmas")

delete-non-membertheorem

(defthm delete-non-member
  (implies (not (memb x y)) (equal (del x y) y)))

member-deletetheorem

(defthm member-delete
  (implies (memb x (del u v)) (memb x v)))

delete-commutativitytheorem

(defthm delete-commutativity
  (equal (del x (del y z)) (del y (del x z))))

subbagp-deletetheorem

(defthm subbagp-delete
  (implies (subbagp x (del u y)) (subbagp x y)))

subbagp-cdr1theorem

(defthm subbagp-cdr1
  (implies (and (subbagp x y) (consp x)) (subbagp (cdr x) y)))

subbagp-cdr2theorem

(defthm subbagp-cdr2
  (implies (and (subbagp x (cdr y)) (consp y)) (subbagp x y)))

subbagp-bagint1theorem

(defthm subbagp-bagint1 (subbagp (bagint x y) x))

subbagp-bagint2theorem

(defthm subbagp-bagint2 (subbagp (bagint x y) y))

memb-appendtheorem

(defthm memb-append
  (equal (memb a (append x y)) (or (memb a x) (memb a y))))

binary-op_tree-openertheorem

(defthm binary-op_tree-opener
  (and (implies (not (consp lst))
      (equal (binary-op_tree binary-op-name constant-name fix-name lst)
        (list 'quote constant-name)))
    (equal (binary-op_tree binary-op-name
        constant-name
        fix-name
        (cons x lst))
      (cond ((not (consp lst)) (list fix-name x))
        ((and (consp lst) (not (consp (cdr lst)))) (list binary-op-name x (car lst)))
        (t (list binary-op-name
            x
            (binary-op_tree binary-op-name constant-name fix-name lst)))))))

binary-op_tree-simple-openertheorem

(defthm binary-op_tree-simple-opener
  (and (implies (not (consp lst))
      (equal (binary-op_tree-simple binary-op-name constant-name lst)
        (list 'quote constant-name)))
    (equal (binary-op_tree-simple binary-op-name
        constant-name
        (cons x lst))
      (cond ((not (consp lst)) x)
        (t (list binary-op-name
            x
            (binary-op_tree-simple binary-op-name constant-name lst)))))))

fringe-occur-same-as-occur-in-fringetheorem

(defthm fringe-occur-same-as-occur-in-fringe
  (equal (fringe-occur binop arg term)
    (memb arg (binary-op_fringe binop term))))

pseudo-termp-term-list-to-type-termtheorem

(defthm pseudo-termp-term-list-to-type-term
  (implies (and (pseudo-term-listp x) (symbolp unary-op-name))
    (pseudo-termp (term-list-to-type-term unary-op-name x))))

pseudo-term-listp-deltheorem

(defthm pseudo-term-listp-del
  (implies (pseudo-term-listp x)
    (pseudo-term-listp (del a x))))

pseudo-term-listp-bagdifftheorem

(defthm pseudo-term-listp-bagdiff
  (implies (pseudo-term-listp x)
    (pseudo-term-listp (bagdiff x y))))

pseudo-term-listp-baginttheorem

(defthm pseudo-term-listp-bagint
  (implies (pseudo-term-listp x)
    (pseudo-term-listp (bagint x y))))

pseudo-term-listp-binary-op_fringetheorem

(defthm pseudo-term-listp-binary-op_fringe
  (implies (and (symbolp binary-op-name)
      (not (equal binary-op-name 'quote))
      (pseudo-termp x))
    (pseudo-term-listp (binary-op_fringe binary-op-name x))))

psuedo-termp-binary-op_treetheorem

(defthm psuedo-termp-binary-op_tree
  (implies (and (pseudo-term-listp l)
      (symbolp binary-op-name)
      (symbolp fix-name)
      (not (equal binary-op-name 'quote))
      (atom constant-name))
    (pseudo-termp (binary-op_tree binary-op-name constant-name fix-name l)))
  :rule-classes (:rewrite (:forward-chaining :trigger-terms ((binary-op_tree binary-op-name constant-name fix-name l)))))

pseudo-term-listp-remove-duplicates-membtheorem

(defthm pseudo-term-listp-remove-duplicates-memb
  (implies (pseudo-term-listp lst)
    (pseudo-term-listp (remove-duplicates-memb lst))))

Included Books