		Search-engine friendly clone of the ACL2 documentation.

Tuple-operations

Op-tuple-write

Leo tuple writing operation.

Signature
(op-tuple-write tupval index newval) → result
Arguments: tupval — Guard (valuep tupval).; index — Guard (natp index).; newval — Guard (valuep newval).
Returns: result — Type (value-resultp result).

This formalizes the replacement of a tuple component with a new value. The new value must have the same type as the old one, otherwise we defensively return an error indication: this ensures that tuples maintain their types under writing, an invariant that we will eventually prove.

Definitions and Theorems

Function: op-tuple-write

(defun op-tuple-write (tupval index newval)
  (declare (xargs :guard (and (valuep tupval)
                              (natp index)
                              (valuep newval))))
  (let ((__function__ 'op-tuple-write))
    (declare (ignorable __function__))
    (b* ((err (reserrf (list :op-tuple-write (value-fix tupval)
                             (nfix index)
                             (value-fix newval))))
         ((unless (value-case tupval :tuple))
          err)
         (vals (value-tuple->components tupval))
         ((unless (< (nfix index) (len vals)))
          err)
         (oldval (nth (nfix index) vals))
         ((unless (equal (type-of-value newval)
                         (type-of-value oldval)))
          err))
      (value-tuple (update-nth (nfix index)
                               newval vals)))))

Theorem: value-resultp-of-op-tuple-write

(defthm value-resultp-of-op-tuple-write
  (b* ((result (op-tuple-write tupval index newval)))
    (value-resultp result))
  :rule-classes :rewrite)

Theorem: op-tuple-write-of-value-fix-tupval

(defthm op-tuple-write-of-value-fix-tupval
  (equal (op-tuple-write (value-fix tupval)
                         index newval)
         (op-tuple-write tupval index newval)))

Theorem: op-tuple-write-value-equiv-congruence-on-tupval

(defthm op-tuple-write-value-equiv-congruence-on-tupval
  (implies (value-equiv tupval tupval-equiv)
           (equal (op-tuple-write tupval index newval)
                  (op-tuple-write tupval-equiv index newval)))
  :rule-classes :congruence)

Theorem: op-tuple-write-of-nfix-index

(defthm op-tuple-write-of-nfix-index
  (equal (op-tuple-write tupval (nfix index)
                         newval)
         (op-tuple-write tupval index newval)))

Theorem: op-tuple-write-nat-equiv-congruence-on-index

(defthm op-tuple-write-nat-equiv-congruence-on-index
  (implies (acl2::nat-equiv index index-equiv)
           (equal (op-tuple-write tupval index newval)
                  (op-tuple-write tupval index-equiv newval)))
  :rule-classes :congruence)

Theorem: op-tuple-write-of-value-fix-newval

(defthm op-tuple-write-of-value-fix-newval
  (equal (op-tuple-write tupval index (value-fix newval))
         (op-tuple-write tupval index newval)))

Theorem: op-tuple-write-value-equiv-congruence-on-newval

(defthm op-tuple-write-value-equiv-congruence-on-newval
  (implies (value-equiv newval newval-equiv)
           (equal (op-tuple-write tupval index newval)
                  (op-tuple-write tupval index newval-equiv)))
  :rule-classes :congruence)