		Search-engine friendly clone of the ACL2 documentation.

Interp-flags

!interp-flags->hide

Update the |ACL2|::|HIDE| field of a interp-flags bit structure.

Signature
(!interp-flags->hide hide x) → new-x
Arguments: hide — Guard (booleanp hide).; x — Guard (interp-flags-p x).
Returns: new-x — Type (interp-flags-p new-x).

Definitions and Theorems

Function: !interp-flags->hide

(defun !interp-flags->hide (hide x)
 (declare (xargs :guard (and (booleanp hide)
                             (interp-flags-p x))))
 (mbe
     :logic
     (b* ((hide (bool->bit hide))
          (x (interp-flags-fix x)))
       (acl2::part-install hide x
                           :width 1
                           :low 4))
     :exec
     (the (unsigned-byte 5)
          (logior (the (unsigned-byte 5)
                       (logand (the (unsigned-byte 5) x)
                               (the (signed-byte 6) -17)))
                  (the (unsigned-byte 5)
                       (ash (the (unsigned-byte 1) (bool->bit hide))
                            4))))))

Theorem: interp-flags-p-of-!interp-flags->hide

(defthm interp-flags-p-of-!interp-flags->hide
  (b* ((new-x (!interp-flags->hide hide x)))
    (interp-flags-p new-x))
  :rule-classes :rewrite)

Theorem: !interp-flags->hide-of-bool-fix-hide

(defthm !interp-flags->hide-of-bool-fix-hide
  (equal (!interp-flags->hide (bool-fix hide) x)
         (!interp-flags->hide hide x)))

Theorem: !interp-flags->hide-iff-congruence-on-hide

(defthm !interp-flags->hide-iff-congruence-on-hide
  (implies (iff hide hide-equiv)
           (equal (!interp-flags->hide hide x)
                  (!interp-flags->hide hide-equiv x)))
  :rule-classes :congruence)

Theorem: !interp-flags->hide-of-interp-flags-fix-x

(defthm !interp-flags->hide-of-interp-flags-fix-x
  (equal (!interp-flags->hide hide (interp-flags-fix x))
         (!interp-flags->hide hide x)))

Theorem: !interp-flags->hide-interp-flags-equiv-congruence-on-x

(defthm !interp-flags->hide-interp-flags-equiv-congruence-on-x
  (implies (interp-flags-equiv x x-equiv)
           (equal (!interp-flags->hide hide x)
                  (!interp-flags->hide hide x-equiv)))
  :rule-classes :congruence)

Theorem: !interp-flags->hide-is-interp-flags

(defthm !interp-flags->hide-is-interp-flags
  (equal (!interp-flags->hide hide x)
         (change-interp-flags x :hide hide)))

Theorem: interp-flags->hide-of-!interp-flags->hide

(defthm interp-flags->hide-of-!interp-flags->hide
  (b* ((?new-x (!interp-flags->hide hide x)))
    (equal (interp-flags->hide new-x)
           (bool-fix hide))))

Theorem: !interp-flags->hide-equiv-under-mask

(defthm !interp-flags->hide-equiv-under-mask
  (b* ((?new-x (!interp-flags->hide hide x)))
    (interp-flags-equiv-under-mask new-x x 15)))