		Search-engine friendly clone of the ACL2 documentation.

Interp-flags

!interp-flags->simplify-logic

Update the |FGL|::|SIMPLIFY-LOGIC| field of a interp-flags bit structure.

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

Definitions and Theorems

Function: !interp-flags->simplify-logic

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

Theorem: interp-flags-p-of-!interp-flags->simplify-logic

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

Theorem: !interp-flags->simplify-logic-of-bool-fix-simplify-logic

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

Theorem: !interp-flags->simplify-logic-iff-congruence-on-simplify-logic

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

Theorem: !interp-flags->simplify-logic-of-interp-flags-fix-x

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

Theorem: !interp-flags->simplify-logic-interp-flags-equiv-congruence-on-x

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

Theorem: !interp-flags->simplify-logic-is-interp-flags

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

Theorem: interp-flags->simplify-logic-of-!interp-flags->simplify-logic

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

Theorem: !interp-flags->simplify-logic-equiv-under-mask

(defthm !interp-flags->simplify-logic-equiv-under-mask
  (b* ((?new-x (!interp-flags->simplify-logic simplify-logic x)))
    (interp-flags-equiv-under-mask new-x x -5)))