		Search-engine friendly clone of the ACL2 documentation.

Atc-arrays

Sint-array-integer-write

Write an element to an array of type signed int, using an ACL2 integer index.

Signature
(sint-array-integer-write array index element) → new-array
Arguments: array — Guard (sint-arrayp array).; index — Guard (integerp index).; element — Guard (sintp element).
Returns: new-array — Type (sint-arrayp new-array).

Definitions and Theorems

Function: sint-array-integer-write

(defun sint-array-integer-write (array index element)
 (declare (xargs :guard (and (sint-arrayp array)
                             (integerp index)
                             (sintp element))))
 (declare (xargs :guard (sint-array-integer-index-okp array index)))
 (let ((__function__ 'sint-array-integer-write))
   (declare (ignorable __function__))
   (b* ((array (sint-array-fix array))
        (index (ifix index))
        (element (sint-fix element)))
     (if (mbt (sint-array-integer-index-okp array index))
         (sint-array-of
              (update-nth index
                          element (sint-array->elements array)))
       array))))

Theorem: sint-arrayp-of-sint-array-integer-write

(defthm sint-arrayp-of-sint-array-integer-write
  (b* ((new-array (sint-array-integer-write array index element)))
    (sint-arrayp new-array))
  :rule-classes :rewrite)

Theorem: len-of-sint-array->elements-of-sint-array-integer-write

(defthm len-of-sint-array->elements-of-sint-array-integer-write
  (equal (len (sint-array->elements
                   (sint-array-integer-write array index element)))
         (len (sint-array->elements array))))

Theorem: sint-array-length-of-sint-array-integer-write

(defthm sint-array-length-of-sint-array-integer-write
 (equal
  (sint-array-length (sint-array-integer-write array index element))
  (sint-array-length array)))

Theorem: sint-array-integer-write-alt-def

(defthm sint-array-integer-write-alt-def
  (implies (and (sint-arrayp array)
                (integerp index)
                (sintp elem)
                (sint-array-integer-index-okp array index))
           (equal (sint-array-integer-write array index elem)
                  (value-array-write index elem array))))

Theorem: sint-array-integer-write-of-sint-array-fix-array

(defthm sint-array-integer-write-of-sint-array-fix-array
  (equal (sint-array-integer-write (sint-array-fix array)
                                   index element)
         (sint-array-integer-write array index element)))

Theorem: sint-array-integer-write-sint-array-equiv-congruence-on-array

(defthm
      sint-array-integer-write-sint-array-equiv-congruence-on-array
  (implies
       (sint-array-equiv array array-equiv)
       (equal (sint-array-integer-write array index element)
              (sint-array-integer-write array-equiv index element)))
  :rule-classes :congruence)

Theorem: sint-array-integer-write-of-ifix-index

(defthm sint-array-integer-write-of-ifix-index
  (equal (sint-array-integer-write array (ifix index)
                                   element)
         (sint-array-integer-write array index element)))

Theorem: sint-array-integer-write-int-equiv-congruence-on-index

(defthm sint-array-integer-write-int-equiv-congruence-on-index
  (implies
       (acl2::int-equiv index index-equiv)
       (equal (sint-array-integer-write array index element)
              (sint-array-integer-write array index-equiv element)))
  :rule-classes :congruence)

Theorem: sint-array-integer-write-of-sint-fix-element

(defthm sint-array-integer-write-of-sint-fix-element
  (equal (sint-array-integer-write array index (sint-fix element))
         (sint-array-integer-write array index element)))

Theorem: sint-array-integer-write-sint-equiv-congruence-on-element

(defthm sint-array-integer-write-sint-equiv-congruence-on-element
  (implies
       (sint-equiv element element-equiv)
       (equal (sint-array-integer-write array index element)
              (sint-array-integer-write array index element-equiv)))
  :rule-classes :congruence)