		Search-engine friendly clone of the ACL2 documentation.

Fgl-syntactic-checker-binders

Check-int-sign

FGL binder that checks whether x is syntactically known to be either positive or negative when fixed to an integer; returns 0 or -1 (the tail of the integer) if it can be determined and NIL otherwise.

Signature
(check-int-sign ans x) → *

See fgl-syntactic-checker-binders and see binder for details.

Definitions and Theorems

Function: check-int-sign

(defun check-int-sign (ans x)
  (declare (xargs :guard t))
  (let ((__function__ 'check-int-sign))
    (declare (ignorable __function__))
    (and ans (if (< (ifix x) 0) -1 0))))

Theorem: check-int-sign-implies-sign

(defthm check-int-sign-implies-sign
 (implies
  (acl2::rewriting-negative-literal (cons 'check-int-sign
                                          (cons ans (cons x 'nil))))
  (iff (check-int-sign ans x)
       (and (or (and (< (ifix x) 0)
                     (equal (check-int-sign ans x) -1))
                (and (<= 0 (ifix x))
                     (equal (check-int-sign ans x) 0)))
            (hide (check-int-sign ans x))))))

Theorem: check-int-sign-equals-val

(defthm check-int-sign-equals-val
 (implies
  (and
   (syntaxp
     (and (quotep val)
          (or (acl2::rewriting-negative-literal-fn
                   (cons 'equal
                         (cons (cons 'check-int-sign
                                     (cons ans (cons x 'nil)))
                               (cons val 'nil)))
                   mfc state)
              (acl2::rewriting-negative-literal-fn
                   (cons 'equal
                         (cons val
                               (cons (cons 'check-int-sign
                                           (cons ans (cons x 'nil)))
                                     'nil)))
                   mfc state))))
   val)
  (iff (equal (check-int-sign ans x) val)
       (and (or (and (equal val -1) (< (ifix x) 0))
                (and (equal val 0) (<= 0 (ifix x))))
            (hide (equal (check-int-sign ans x) val))))))