		Search-engine friendly clone of the ACL2 documentation.

Semantics-deeply-embedded

Eval-expr-list

Lift eval-expr to lists.

Signature
(eval-expr-list exprs asg p) → nats
Arguments: exprs — Guard (expression-listp exprs).; asg — Guard (assignmentp asg).; p — Guard (primep p).
Returns: nats — Type (nat-list-resultp nats), given (primep p).

We prove that evaluating a list of expressions with an assignment that has an added variable that is not in the list of expressions, is like evaluating the list of expressions with the assignment without the added variable.

We prove that evaluating a list of distinct variables (as expressions) with an assignment that assigns values from a list to the variables in the same order, yields those values, in the same order.

Definitions and Theorems

Function: eval-expr-list

(defun eval-expr-list (exprs asg p)
  (declare (xargs :guard (and (expression-listp exprs)
                              (assignmentp asg)
                              (primep p))))
  (declare (xargs :guard (assignment-wfp asg p)))
  (let ((__function__ 'eval-expr-list))
    (declare (ignorable __function__))
    (b* (((when (endp exprs)) nil)
         ((ok val) (eval-expr (car exprs) asg p))
         ((ok vals)
          (eval-expr-list (cdr exprs) asg p)))
      (cons val vals))))

Theorem: nat-list-resultp-of-eval-expr-list

(defthm nat-list-resultp-of-eval-expr-list
  (implies (primep p)
           (b* ((nats (eval-expr-list exprs asg p)))
             (nat-list-resultp nats)))
  :rule-classes :rewrite)

Theorem: fe-listp-of-eval-expr-list

(defthm fe-listp-of-eval-expr-list
  (implies (and (primep p)
                (assignmentp asg)
                (assignment-wfp asg p)
                (not (reserrp (eval-expr-list exprs asg p))))
           (fe-listp (eval-expr-list exprs asg p)
                     p)))

Theorem: len-of-eval-expr-list

(defthm len-of-eval-expr-list
  (b* ((?nats (eval-expr-list exprs asg p)))
    (implies (nat-listp nats)
             (equal (len nats) (len exprs)))))

Theorem: eval-expr-list-of-omap-udpate-of-var-not-in-exprs

(defthm eval-expr-list-of-omap-udpate-of-var-not-in-exprs
  (implies (and (stringp var)
                (natp val)
                (assignmentp asg)
                (not (in var (expression-list-vars exprs))))
           (equal (eval-expr-list exprs (omap::update var val asg)
                                  p)
                  (eval-expr-list exprs asg p))))

Theorem: eval-expr-list-of-expression-var-list-and-omap-from-lists

(defthm eval-expr-list-of-expression-var-list-and-omap-from-lists
  (implies (and (string-listp vars)
                (no-duplicatesp-equal vars)
                (fe-listp vals p)
                (equal (len vars) (len vals)))
           (equal (eval-expr-list (expression-var-list vars)
                                  (omap::from-lists vars vals)
                                  p)
                  vals)))

Theorem: eval-expr-list-of-expression-list-fix-exprs

(defthm eval-expr-list-of-expression-list-fix-exprs
  (equal (eval-expr-list (expression-list-fix exprs)
                         asg p)
         (eval-expr-list exprs asg p)))

Theorem: eval-expr-list-expression-list-equiv-congruence-on-exprs

(defthm eval-expr-list-expression-list-equiv-congruence-on-exprs
  (implies (expression-list-equiv exprs exprs-equiv)
           (equal (eval-expr-list exprs asg p)
                  (eval-expr-list exprs-equiv asg p)))
  :rule-classes :congruence)

Theorem: eval-expr-list-of-assignment-fix-asg

(defthm eval-expr-list-of-assignment-fix-asg
  (equal (eval-expr-list exprs (assignment-fix asg)
                         p)
         (eval-expr-list exprs asg p)))

Theorem: eval-expr-list-assignment-equiv-congruence-on-asg

(defthm eval-expr-list-assignment-equiv-congruence-on-asg
  (implies (assignment-equiv asg asg-equiv)
           (equal (eval-expr-list exprs asg p)
                  (eval-expr-list exprs asg-equiv p)))
  :rule-classes :congruence)