		Search-engine friendly clone of the ACL2 documentation.

Parser

Make-expr-unary-with-preinc/predec-ops

Apply to an expression all the pre-increment and pre-decrement operators in a list.

Signature
(make-expr-unary-with-preinc/predec-ops ops expr) → new-expr
Arguments: ops — Guard (inc/dec-op-listp ops).; expr — Guard (exprp expr).
Returns: new-expr — Type (exprp new-expr).

The operators are applied starting from the right, i.e. the last one in the list is applied first, then the second-to-last, and so on until the first (i.e. car). If the list is empty, the expression is unchanged.

Definitions and Theorems

Function: make-expr-unary-with-preinc/predec-ops

(defun make-expr-unary-with-preinc/predec-ops (ops expr)
  (declare (xargs :guard (and (inc/dec-op-listp ops)
                              (exprp expr))))
  (let ((__function__ 'make-expr-unary-with-preinc/predec-ops))
    (declare (ignorable __function__))
    (b* (((when (endp ops)) (expr-fix expr))
         (op (car ops))
         (preop (inc/dec-op-case op
                                 :inc (unop-preinc)
                                 :dec (unop-predec)))
         (expr1 (make-expr-unary-with-preinc/predec-ops (cdr ops)
                                                        expr)))
      (make-expr-unary :op preop
                       :arg expr1
                       :info nil))))

Theorem: exprp-of-make-expr-unary-with-preinc/predec-ops

(defthm exprp-of-make-expr-unary-with-preinc/predec-ops
  (b* ((new-expr (make-expr-unary-with-preinc/predec-ops ops expr)))
    (exprp new-expr))
  :rule-classes :rewrite)

Theorem: make-expr-unary-with-preinc/predec-ops-of-inc/dec-op-list-fix-ops

(defthm
  make-expr-unary-with-preinc/predec-ops-of-inc/dec-op-list-fix-ops
 (equal
   (make-expr-unary-with-preinc/predec-ops (inc/dec-op-list-fix ops)
                                           expr)
   (make-expr-unary-with-preinc/predec-ops ops expr)))

Theorem: make-expr-unary-with-preinc/predec-ops-inc/dec-op-list-equiv-congruence-on-ops

(defthm
 make-expr-unary-with-preinc/predec-ops-inc/dec-op-list-equiv-congruence-on-ops
 (implies
    (inc/dec-op-list-equiv ops ops-equiv)
    (equal (make-expr-unary-with-preinc/predec-ops ops expr)
           (make-expr-unary-with-preinc/predec-ops ops-equiv expr)))
 :rule-classes :congruence)

Theorem: make-expr-unary-with-preinc/predec-ops-of-expr-fix-expr

(defthm make-expr-unary-with-preinc/predec-ops-of-expr-fix-expr
 (equal (make-expr-unary-with-preinc/predec-ops ops (expr-fix expr))
        (make-expr-unary-with-preinc/predec-ops ops expr)))

Theorem: make-expr-unary-with-preinc/predec-ops-expr-equiv-congruence-on-expr

(defthm
 make-expr-unary-with-preinc/predec-ops-expr-equiv-congruence-on-expr
 (implies
    (expr-equiv expr expr-equiv)
    (equal (make-expr-unary-with-preinc/predec-ops ops expr)
           (make-expr-unary-with-preinc/predec-ops ops expr-equiv)))
 :rule-classes :congruence)