		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Apply-post-inc/dec-ops

Apply a sequence of post-increment and post-decrement operators to an expression.

Signature
(apply-post-inc/dec-ops expr ops) → new-expr
Arguments: expr — Guard (exprp expr).; ops — Guard (inc/dec-op-listp ops).
Returns: new-expr — Type (exprp new-expr).

The first one in the list will be the innermost, and the last one in the list will be the outermost.

Definitions and Theorems

Function: apply-post-inc/dec-ops

(defun apply-post-inc/dec-ops (expr ops)
  (declare (xargs :guard (and (exprp expr)
                              (inc/dec-op-listp ops))))
  (b*
    (((when (endp ops)) (expr-fix expr))
     (op (car ops))
     (expr (inc/dec-op-case op
                            :inc (make-expr-unary :op (unop-postinc)
                                                  :arg expr
                                                  :info nil)
                            :dec (make-expr-unary :op (unop-postdec)
                                                  :arg expr
                                                  :info nil))))
    (apply-post-inc/dec-ops expr (cdr ops))))

Theorem: exprp-of-apply-post-inc/dec-ops

(defthm exprp-of-apply-post-inc/dec-ops
  (b* ((new-expr (apply-post-inc/dec-ops expr ops)))
    (exprp new-expr))
  :rule-classes :rewrite)

Theorem: apply-post-inc/dec-ops-of-expr-fix-expr

(defthm apply-post-inc/dec-ops-of-expr-fix-expr
  (equal (apply-post-inc/dec-ops (expr-fix expr)
                                 ops)
         (apply-post-inc/dec-ops expr ops)))

Theorem: apply-post-inc/dec-ops-expr-equiv-congruence-on-expr

(defthm apply-post-inc/dec-ops-expr-equiv-congruence-on-expr
  (implies (expr-equiv expr expr-equiv)
           (equal (apply-post-inc/dec-ops expr ops)
                  (apply-post-inc/dec-ops expr-equiv ops)))
  :rule-classes :congruence)

Theorem: apply-post-inc/dec-ops-of-inc/dec-op-list-fix-ops

(defthm apply-post-inc/dec-ops-of-inc/dec-op-list-fix-ops
  (equal (apply-post-inc/dec-ops expr (inc/dec-op-list-fix ops))
         (apply-post-inc/dec-ops expr ops)))

Theorem: apply-post-inc/dec-ops-inc/dec-op-list-equiv-congruence-on-ops

(defthm
     apply-post-inc/dec-ops-inc/dec-op-list-equiv-congruence-on-ops
  (implies (inc/dec-op-list-equiv ops ops-equiv)
           (equal (apply-post-inc/dec-ops expr ops)
                  (apply-post-inc/dec-ops expr ops-equiv)))
  :rule-classes :congruence)