• 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->dont-expand-def

Update the |FGL|::|DONT-EXPAND-DEF| field of a fgl-function-mode bit structure.

Signature

(!fgl-function-mode->dont-expand-def dont-expand-def x) 
  → 
new-x

Arguments

dont-expand-def — Guard (booleanp dont-expand-def).

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

Returns

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

Definitions and Theorems

Function: !fgl-function-mode->dont-expand-def

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

Theorem: fgl-function-mode-p-of-!fgl-function-mode->dont-expand-def

(defthm fgl-function-mode-p-of-!fgl-function-mode->dont-expand-def
  (b*
   ((new-x (!fgl-function-mode->dont-expand-def dont-expand-def x)))
   (fgl-function-mode-p new-x))
  :rule-classes :rewrite)

Theorem: !fgl-function-mode->dont-expand-def-of-bool-fix-dont-expand-def

(defthm
    !fgl-function-mode->dont-expand-def-of-bool-fix-dont-expand-def
 (equal
     (!fgl-function-mode->dont-expand-def (bool-fix dont-expand-def)
                                          x)
     (!fgl-function-mode->dont-expand-def dont-expand-def x)))

Theorem: !fgl-function-mode->dont-expand-def-iff-congruence-on-dont-expand-def

(defthm
 !fgl-function-mode->dont-expand-def-iff-congruence-on-dont-expand-def
 (implies
  (iff dont-expand-def dont-expand-def-equiv)
  (equal
     (!fgl-function-mode->dont-expand-def dont-expand-def x)
     (!fgl-function-mode->dont-expand-def dont-expand-def-equiv x)))
 :rule-classes :congruence)

Theorem: !fgl-function-mode->dont-expand-def-of-fgl-function-mode-fix-x

(defthm
     !fgl-function-mode->dont-expand-def-of-fgl-function-mode-fix-x
 (equal
     (!fgl-function-mode->dont-expand-def dont-expand-def
                                          (fgl-function-mode-fix x))
     (!fgl-function-mode->dont-expand-def dont-expand-def x)))

Theorem: !fgl-function-mode->dont-expand-def-fgl-function-mode-equiv-congruence-on-x

(defthm
 !fgl-function-mode->dont-expand-def-fgl-function-mode-equiv-congruence-on-x
 (implies
  (fgl-function-mode-equiv x x-equiv)
  (equal
     (!fgl-function-mode->dont-expand-def dont-expand-def x)
     (!fgl-function-mode->dont-expand-def dont-expand-def x-equiv)))
 :rule-classes :congruence)

Theorem: !fgl-function-mode->dont-expand-def-is-fgl-function-mode

(defthm !fgl-function-mode->dont-expand-def-is-fgl-function-mode
  (equal
       (!fgl-function-mode->dont-expand-def dont-expand-def x)
       (change-fgl-function-mode x
                                 :dont-expand-def dont-expand-def)))

Theorem: fgl-function-mode->dont-expand-def-of-!fgl-function-mode->dont-expand-def

(defthm
 fgl-function-mode->dont-expand-def-of-!fgl-function-mode->dont-expand-def
 (b*
  ((?new-x (!fgl-function-mode->dont-expand-def dont-expand-def x)))
  (equal (fgl-function-mode->dont-expand-def new-x)
         (bool-fix dont-expand-def))))

Theorem: !fgl-function-mode->dont-expand-def-equiv-under-mask

(defthm !fgl-function-mode->dont-expand-def-equiv-under-mask
 (b*
  ((?new-x (!fgl-function-mode->dont-expand-def dont-expand-def x)))
  (fgl-function-mode-equiv-under-mask new-x x -5)))