		Search-engine friendly clone of the ACL2 documentation.

Interp-flags

!interp-flags->intro-bvars

Update the |FGL|::|INTRO-BVARS| field of a interp-flags bit structure.

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

Definitions and Theorems

Function: !interp-flags->intro-bvars

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

Theorem: interp-flags-p-of-!interp-flags->intro-bvars

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

Theorem: !interp-flags->intro-bvars-of-bool-fix-intro-bvars

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

Theorem: !interp-flags->intro-bvars-iff-congruence-on-intro-bvars

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

Theorem: !interp-flags->intro-bvars-of-interp-flags-fix-x

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

Theorem: !interp-flags->intro-bvars-interp-flags-equiv-congruence-on-x

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

Theorem: !interp-flags->intro-bvars-is-interp-flags

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

Theorem: interp-flags->intro-bvars-of-!interp-flags->intro-bvars

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

Theorem: !interp-flags->intro-bvars-equiv-under-mask

(defthm !interp-flags->intro-bvars-equiv-under-mask
  (b* ((?new-x (!interp-flags->intro-bvars intro-bvars x)))
    (interp-flags-equiv-under-mask new-x x -2)))