pos-fix

(in-package "ACL2")

(defsection pos-fix
  :parents (posp std/basic)
  :short "@(call pos-fix) is a fixing function for @(see posp): it is the
identity for positive integers, or returns 1 for any other object."
  :long "<p>This has guard @('t').  For better efficiency, see @(see lposfix).</p>"
  (defund pos-fix
    (x)
    (declare (xargs :guard t))
    (if (posp x)
      x
      1))
  (local (in-theory (enable pos-fix)))
  (defthm posp-of-pos-fix
    (posp (pos-fix x))
    :rule-classes :type-prescription)
  (defthm pos-fix-when-posp
    (implies (posp x) (equal (pos-fix x) x))))