		Search-engine friendly clone of the ACL2 documentation.

Simpcode

!simpcode->identity

Update the |COMMON-LISP|::|IDENTITY| field of a simpcode bit structure.

Signature
(!simpcode->identity identity x) → new-x
Arguments: identity — Guard (bitp identity).; x — Guard (simpcode-p x).
Returns: new-x — Type (simpcode-p new-x).

Definitions and Theorems

Function: !simpcode->identity

(defun !simpcode->identity (identity x)
  (declare (xargs :guard (and (bitp identity) (simpcode-p x))))
  (mbe :logic
       (b* ((identity (mbe :logic (bfix identity)
                           :exec identity))
            (x (simpcode-fix x)))
         (part-install identity x
                       :width 1
                       :low 2))
       :exec (the (unsigned-byte 4)
                  (logior (the (unsigned-byte 4)
                               (logand (the (unsigned-byte 4) x)
                                       (the (signed-byte 4) -5)))
                          (the (unsigned-byte 3)
                               (ash (the (unsigned-byte 1) identity)
                                    2))))))

Theorem: simpcode-p-of-!simpcode->identity

(defthm simpcode-p-of-!simpcode->identity
  (b* ((new-x (!simpcode->identity identity x)))
    (simpcode-p new-x))
  :rule-classes :rewrite)

Theorem: !simpcode->identity-of-bfix-identity

(defthm !simpcode->identity-of-bfix-identity
  (equal (!simpcode->identity (bfix identity) x)
         (!simpcode->identity identity x)))

Theorem: !simpcode->identity-bit-equiv-congruence-on-identity

(defthm !simpcode->identity-bit-equiv-congruence-on-identity
  (implies (bit-equiv identity identity-equiv)
           (equal (!simpcode->identity identity x)
                  (!simpcode->identity identity-equiv x)))
  :rule-classes :congruence)

Theorem: !simpcode->identity-of-simpcode-fix-x

(defthm !simpcode->identity-of-simpcode-fix-x
  (equal (!simpcode->identity identity (simpcode-fix x))
         (!simpcode->identity identity x)))

Theorem: !simpcode->identity-simpcode-equiv-congruence-on-x

(defthm !simpcode->identity-simpcode-equiv-congruence-on-x
  (implies (simpcode-equiv x x-equiv)
           (equal (!simpcode->identity identity x)
                  (!simpcode->identity identity x-equiv)))
  :rule-classes :congruence)

Theorem: !simpcode->identity-is-simpcode

(defthm !simpcode->identity-is-simpcode
  (equal (!simpcode->identity identity x)
         (change-simpcode x :identity identity)))

Theorem: simpcode->identity-of-!simpcode->identity

(defthm simpcode->identity-of-!simpcode->identity
  (b* ((?new-x (!simpcode->identity identity x)))
    (equal (simpcode->identity new-x)
           (bfix identity))))

Theorem: !simpcode->identity-equiv-under-mask

(defthm !simpcode->identity-equiv-under-mask
  (b* ((?new-x (!simpcode->identity identity x)))
    (simpcode-equiv-under-mask new-x x -5)))