		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Decompose-expression

Decompose an expression into a list of expressions of given length.

Signature
(decompose-expression expr n) → exprs
Arguments: expr — Guard (expressionp expr).; n — Guard (posp n).
Returns: exprs — Type (expression-listp exprs).

If n is 1, we return a singleton list containing the expression. Otherwise, we return a list of n expressions, each of which is a component expression consisting of the initial expression as target and the list position as index.

The idea is that n is 1 if the expression is single-valued, greater than 1 if the expression is multi-valued. In the latter case, n should be equal to the number of components of the multiple value. Thus, the expression is decomposed into its one or more components.

Definitions and Theorems

Function: decompose-expression-aux

(defun decompose-expression-aux (i n expr)
  (declare (xargs :guard (and (natp i)
                              (natp n)
                              (expressionp expr))))
  (let ((__function__ 'decompose-expression-aux))
    (declare (ignorable __function__))
    (b* ((i (nfix i)) (n (nfix n)))
      (if (>= i n)
          nil
        (cons (make-expression-component :multi expr
                                         :index i)
              (decompose-expression-aux (1+ i)
                                        n expr))))))

Theorem: expression-listp-of-decompose-expression-aux

(defthm expression-listp-of-decompose-expression-aux
  (b* ((exprs (decompose-expression-aux i n expr)))
    (expression-listp exprs))
  :rule-classes :rewrite)

Theorem: len-of-decompose-expression-aux

(defthm len-of-decompose-expression-aux
  (b* ((?exprs (decompose-expression-aux i n expr)))
    (equal (len exprs)
           (nfix (- (nfix n) (nfix i))))))

Theorem: decompose-expression-aux-of-nfix-i

(defthm decompose-expression-aux-of-nfix-i
  (equal (decompose-expression-aux (nfix i)
                                   n expr)
         (decompose-expression-aux i n expr)))

Theorem: decompose-expression-aux-nat-equiv-congruence-on-i

(defthm decompose-expression-aux-nat-equiv-congruence-on-i
  (implies (nat-equiv i i-equiv)
           (equal (decompose-expression-aux i n expr)
                  (decompose-expression-aux i-equiv n expr)))
  :rule-classes :congruence)

Theorem: decompose-expression-aux-of-nfix-n

(defthm decompose-expression-aux-of-nfix-n
  (equal (decompose-expression-aux i (nfix n)
                                   expr)
         (decompose-expression-aux i n expr)))

Theorem: decompose-expression-aux-nat-equiv-congruence-on-n

(defthm decompose-expression-aux-nat-equiv-congruence-on-n
  (implies (nat-equiv n n-equiv)
           (equal (decompose-expression-aux i n expr)
                  (decompose-expression-aux i n-equiv expr)))
  :rule-classes :congruence)

Theorem: decompose-expression-aux-of-expression-fix-expr

(defthm decompose-expression-aux-of-expression-fix-expr
  (equal (decompose-expression-aux i n (expression-fix expr))
         (decompose-expression-aux i n expr)))

Theorem: decompose-expression-aux-expression-equiv-congruence-on-expr

(defthm decompose-expression-aux-expression-equiv-congruence-on-expr
  (implies (expression-equiv expr expr-equiv)
           (equal (decompose-expression-aux i n expr)
                  (decompose-expression-aux i n expr-equiv)))
  :rule-classes :congruence)

Function: decompose-expression

(defun decompose-expression (expr n)
  (declare (xargs :guard (and (expressionp expr) (posp n))))
  (let ((__function__ 'decompose-expression))
    (declare (ignorable __function__))
    (b* ((n (pos-fix n)))
      (if (= n 1)
          (list (expression-fix expr))
        (decompose-expression-aux 0 n expr)))))

Theorem: expression-listp-of-decompose-expression

(defthm expression-listp-of-decompose-expression
  (b* ((exprs (decompose-expression expr n)))
    (expression-listp exprs))
  :rule-classes :rewrite)

Theorem: len-of-decompose-expression

(defthm len-of-decompose-expression
  (b* ((?exprs (decompose-expression expr n)))
    (equal (len exprs) (pos-fix n))))

Theorem: decompose-expression-of-expression-fix-expr

(defthm decompose-expression-of-expression-fix-expr
  (equal (decompose-expression (expression-fix expr)
                               n)
         (decompose-expression expr n)))

Theorem: decompose-expression-expression-equiv-congruence-on-expr

(defthm decompose-expression-expression-equiv-congruence-on-expr
  (implies (expression-equiv expr expr-equiv)
           (equal (decompose-expression expr n)
                  (decompose-expression expr-equiv n)))
  :rule-classes :congruence)

Theorem: decompose-expression-of-pos-fix-n

(defthm decompose-expression-of-pos-fix-n
  (equal (decompose-expression expr (pos-fix n))
         (decompose-expression expr n)))

Theorem: decompose-expression-pos-equiv-congruence-on-n

(defthm decompose-expression-pos-equiv-congruence-on-n
  (implies (pos-equiv n n-equiv)
           (equal (decompose-expression expr n)
                  (decompose-expression expr n-equiv)))
  :rule-classes :congruence)