Apply a sequence of pre-increment and pre-decrement operators to an expression.
(apply-pre-inc/dec-ops ops expr) → new-expr
The first one in the list will be the outermost, and the last one in the list will be the innermost.
Function:
(defun apply-pre-inc/dec-ops (ops expr) (declare (xargs :guard (and (inc/dec-op-listp ops) (exprp expr)))) (let ((__function__ 'apply-pre-inc/dec-ops)) (declare (ignorable __function__)) (b* (((when (endp ops)) (expr-fix expr)) (op (car ops)) (expr (apply-pre-inc/dec-ops (cdr ops) expr))) (inc/dec-op-case op :inc (make-expr-unary :op (unop-preinc) :arg expr) :dec (make-expr-unary :op (unop-predec) :arg expr)))))
Theorem:
(defthm exprp-of-apply-pre-inc/dec-ops (b* ((new-expr (apply-pre-inc/dec-ops ops expr))) (exprp new-expr)) :rule-classes :rewrite)
Theorem:
(defthm apply-pre-inc/dec-ops-of-inc/dec-op-list-fix-ops (equal (apply-pre-inc/dec-ops (inc/dec-op-list-fix ops) expr) (apply-pre-inc/dec-ops ops expr)))
Theorem:
(defthm apply-pre-inc/dec-ops-inc/dec-op-list-equiv-congruence-on-ops (implies (inc/dec-op-list-equiv ops ops-equiv) (equal (apply-pre-inc/dec-ops ops expr) (apply-pre-inc/dec-ops ops-equiv expr))) :rule-classes :congruence)
Theorem:
(defthm apply-pre-inc/dec-ops-of-expr-fix-expr (equal (apply-pre-inc/dec-ops ops (expr-fix expr)) (apply-pre-inc/dec-ops ops expr)))
Theorem:
(defthm apply-pre-inc/dec-ops-expr-equiv-congruence-on-expr (implies (expr-equiv expr expr-equiv) (equal (apply-pre-inc/dec-ops ops expr) (apply-pre-inc/dec-ops ops expr-equiv))) :rule-classes :congruence)