• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
      • Deftagsum
      • Defprod
      • Defflexsum
      • Defbitstruct
      • Deflist
      • Defalist
      • Defbyte
      • Deffixequiv
      • Defresult
      • Deffixtype
      • Fty-discipline
      • Defoption
      • Fty-extensions
      • Defsubtype
      • Defset
      • Specific-types
      • Deftypes
      • Defflatsum
      • Deflist-of-len
      • Defbytelist
      • Fty::basetypes
        • Any-p
        • Symbol-fix
        • Maybe-integerp-fix
        • Maybe-integer-equiv
        • Maybe-posp-fix
        • Maybe-natp-fix
        • Maybe-bit-fix
        • Bool-fix
        • Maybe-pos-equiv
        • Maybe-nat-equiv
        • Maybe-bit-equiv
        • Maybe-lit-fix
        • Symbol-equiv
        • True-equiv
        • Pos-equiv
        • Lposfix
        • True-p
        • True-fix
      • Defvisitors
      • Defomap
      • Deffixtype-alias
      • Deffixequiv-sk
      • Defunit
      • Deffixequiv-mutual
      • Fty::baselists
      • Defmap
    • Apt
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Fty::basetypes
• Maybe-posp

Maybe-posp-fix

(maybe-posp-fix x) is the identity for maybe-posps, or coerces any non-posp to nil.

Performance note. In the execution this is just an inlined identity function, i.e., it should have zero runtime cost.

Definitions and Theorems

Function: maybe-posp-fix$inline

(defun maybe-posp-fix$inline (x)
  (declare (xargs :guard (maybe-posp x)))
  (mbe :logic (if x (pos-fix x) nil)
       :exec x))

Theorem: maybe-posp-of-maybe-posp-fix

(defthm maybe-posp-of-maybe-posp-fix
  (maybe-posp (maybe-posp-fix x))
  :rule-classes (:rewrite :type-prescription))

Theorem: maybe-posp-fix-when-maybe-posp

(defthm maybe-posp-fix-when-maybe-posp
  (implies (maybe-posp x)
           (equal (maybe-posp-fix x) x)))

Theorem: maybe-posp-fix-under-iff

(defthm maybe-posp-fix-under-iff
  (iff (maybe-posp-fix x) x))

Theorem: maybe-posp-fix-under-pos-equiv

(defthm maybe-posp-fix-under-pos-equiv
  (pos-equiv (maybe-posp-fix x) x))