• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
    • Gl
    • Witness-cp
    • Ccg
    • Install-not-normalized
    • Rewrite$
    • Fgl
      • Fgl-rewrite-rules
      • Fgl-function-mode
        • !fgl-function-mode->dont-rewrite-under-if-test
        • !fgl-function-mode->dont-primitive-exec
        • !fgl-function-mode->dont-concrete-exec
        • !fgl-function-mode->dont-expand-def
        • !fgl-function-mode->dont-rewrite
        • !fgl-function-mode->split-ifs
        • Fgl-function-mode->dont-rewrite-under-if-test
        • Fgl-function-mode->dont-primitive-exec
        • Fgl-function-mode->dont-expand-def
        • Fgl-function-mode->dont-concrete-exec
        • Fgl-function-mode-p
        • Fgl-function-mode->dont-rewrite
        • Fgl-function-mode->split-ifs
        • Fgl-function-mode-fix
      • Fgl-object
      • Fgl-solving
      • Fgl-handling-if-then-elses
      • Fgl-counterexamples
      • Fgl-getting-bits-from-objects
      • Fgl-primitive-and-meta-rules
      • Fgl-interpreter-overview
      • Fgl-correctness-of-binding-free-variables
      • Fgl-debugging
      • Fgl-testbenches
      • Def-fgl-boolean-constraint
      • Fgl-stack
      • Def-fgl-param-thm
      • Fgl-rewrite-tracing
      • Def-fgl-thm
      • Fgl-fast-alist-support
      • Fgl-array-support
      • Advanced-equivalence-checking-with-fgl
      • Fgl-fty-support
      • Fgl-internals
    • Removable-runes
    • Efficiency
    • Rewrite-bounds
    • Bash
    • Def-dag-measure
    • Bdd
    • Remove-hyps
    • Contextual-rewriting
    • Simp
    • Rewrite$-hyps
    • Bash-term-to-dnf
    • Use-trivial-ancestors-check
    • Minimal-runes
    • Clause-processor-tools
    • Fn-is-body
    • Without-subsumption
    • Rewrite-equiv-hint
    • Def-bounds
    • Rewrite$-context
    • Try-gl-concls
    • Hint-utils
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Fgl-function-mode

!fgl-function-mode->split-ifs

Update the |FGL|::|SPLIT-IFS| field of a fgl-function-mode bit structure.

Signature

(!fgl-function-mode->split-ifs split-ifs x) → new-x

Arguments

split-ifs — Guard (booleanp split-ifs).

x — Guard (fgl-function-mode-p x).

Returns

new-x — Type (fgl-function-mode-p new-x).

Definitions and Theorems

Function: !fgl-function-mode->split-ifs

(defun !fgl-function-mode->split-ifs (split-ifs x)
  (declare (xargs :guard (and (booleanp split-ifs)
                              (fgl-function-mode-p x))))
  (mbe :logic
       (b* ((split-ifs (bool->bit split-ifs))
            (x (fgl-function-mode-fix x)))
         (acl2::part-install split-ifs 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 split-ifs))))))

Theorem: fgl-function-mode-p-of-!fgl-function-mode->split-ifs

(defthm fgl-function-mode-p-of-!fgl-function-mode->split-ifs
  (b* ((new-x (!fgl-function-mode->split-ifs split-ifs x)))
    (fgl-function-mode-p new-x))
  :rule-classes :rewrite)

Theorem: !fgl-function-mode->split-ifs-of-bool-fix-split-ifs

(defthm !fgl-function-mode->split-ifs-of-bool-fix-split-ifs
  (equal (!fgl-function-mode->split-ifs (bool-fix split-ifs)
                                        x)
         (!fgl-function-mode->split-ifs split-ifs x)))

Theorem: !fgl-function-mode->split-ifs-iff-congruence-on-split-ifs

(defthm !fgl-function-mode->split-ifs-iff-congruence-on-split-ifs
 (implies (iff split-ifs split-ifs-equiv)
          (equal (!fgl-function-mode->split-ifs split-ifs x)
                 (!fgl-function-mode->split-ifs split-ifs-equiv x)))
 :rule-classes :congruence)

Theorem: !fgl-function-mode->split-ifs-of-fgl-function-mode-fix-x

(defthm !fgl-function-mode->split-ifs-of-fgl-function-mode-fix-x
  (equal (!fgl-function-mode->split-ifs
              split-ifs (fgl-function-mode-fix x))
         (!fgl-function-mode->split-ifs split-ifs x)))

Theorem: !fgl-function-mode->split-ifs-fgl-function-mode-equiv-congruence-on-x

(defthm
 !fgl-function-mode->split-ifs-fgl-function-mode-equiv-congruence-on-x
 (implies (fgl-function-mode-equiv x x-equiv)
          (equal (!fgl-function-mode->split-ifs split-ifs x)
                 (!fgl-function-mode->split-ifs split-ifs x-equiv)))
 :rule-classes :congruence)

Theorem: !fgl-function-mode->split-ifs-is-fgl-function-mode

(defthm !fgl-function-mode->split-ifs-is-fgl-function-mode
  (equal (!fgl-function-mode->split-ifs split-ifs x)
         (change-fgl-function-mode x
                                   :split-ifs split-ifs)))

Theorem: fgl-function-mode->split-ifs-of-!fgl-function-mode->split-ifs

(defthm
      fgl-function-mode->split-ifs-of-!fgl-function-mode->split-ifs
  (b* ((?new-x (!fgl-function-mode->split-ifs split-ifs x)))
    (equal (fgl-function-mode->split-ifs new-x)
           (bool-fix split-ifs))))

Theorem: !fgl-function-mode->split-ifs-equiv-under-mask

(defthm !fgl-function-mode->split-ifs-equiv-under-mask
  (b* ((?new-x (!fgl-function-mode->split-ifs split-ifs x)))
    (fgl-function-mode-equiv-under-mask new-x x -2)))