|
|
|---|
|
|
|
|---|
(maybe-posp-fix x) is the identity for maybe-posps, or
coerces any non-posp to
Performance note. In the execution this is just an inlined identity function, i.e., it should have zero runtime cost.
Function:
(defun maybe-posp-fix$inline (x) (declare (xargs :guard (maybe-posp x))) (mbe :logic (if x (pos-fix x) nil) :exec x))
Theorem:
(defthm maybe-posp-of-maybe-posp-fix (maybe-posp (maybe-posp-fix x)) :rule-classes (:rewrite :type-prescription))
Theorem:
(defthm maybe-posp-fix-when-maybe-posp (implies (maybe-posp x) (equal (maybe-posp-fix x) x)))
Theorem:
(defthm maybe-posp-fix-under-iff (iff (maybe-posp-fix x) x))
Theorem:
(defthm maybe-posp-fix-under-pos-equiv (pos-equiv (maybe-posp-fix x) x))