g-logbitp

(in-package "GL")

(include-book "g-if")

(include-book "g-primitives-help")

(include-book "symbolic-arithmetic")

(include-book "eval-g-base")

(local (include-book "eval-g-base-help"))

(local (include-book "hyp-fix"))

(set-inhibit-warnings "theory")

(defun g-logbitp-of-integers
  (a b)
  (declare (xargs :guard (and (general-integerp a)
        (general-integerp b))))
  (b* ((abits (general-integer-bits a)))
    (mk-g-boolean (bfr-logbitp-n2v 1
        (bfr-ite-bvv-fn (bfr-sign-s abits)
          nil
          abits)
        (general-integer-bits b)))))

(in-theory (disable (g-logbitp-of-integers)))

(local (defthm pbfr-list-depends-on-of-nil
    (not (pbfr-list-depends-on k p nil))
    :hints (("Goal" :in-theory (enable pbfr-list-depends-on)))))

(defthm deps-of-g-logbitp-of-integers
  (implies (and (not (gobj-depends-on k p x))
      (not (gobj-depends-on k p y))
      (general-integerp x)
      (general-integerp y))
    (not (gobj-depends-on k
        p
        (g-logbitp-of-integers x y)))))

(local (include-book "arithmetic/top-with-meta" :dir :system))

(local (defthm logbitp-when-zp
    (implies (and (syntaxp (not (equal x ''0))) (zp x))
      (equal (logbitp x y) (logbitp 0 y)))))

(local (defthm bfr-list->s-when-positive
    (implies (<= 0 (bfr-list->s x env))
      (equal (bfr-list->s x env)
        (bfr-list->u x env)))
    :hints (("Goal" :in-theory (e/d (scdr s-endp) (bfix-bitp))))))

(local (defthm g-logbitp-of-integers-correct
    (implies (and (general-integerp a)
        (general-integerp b))
      (equal (eval-g-base (g-logbitp-of-integers a b)
          env)
        (logbitp (eval-g-base a env)
          (eval-g-base b env))))
    :hints (("goal" :in-theory (e/d* ((:ruleset general-object-possibilities))
         (general-integerp general-integer-bits logbitp))
       :do-not-induct t))))

(in-theory (disable g-logbitp-of-integers))

(def-g-binary-op logbitp
  (b* ((i-num (if (general-integerp i)
         i
         0)) (j-num (if (general-integerp j)
          j
          0)))
    (gret (g-logbitp-of-integers i-num j-num))))

(verify-g-guards logbitp
  :hints `(("Goal" :in-theory (disable* ,GL::GFN
       (:rules-of-class :type-prescription :here)))))

(def-gobj-dependency-thm logbitp
  :hints `(("goal" :induct ,GL::GCALL
     :expand (,GL::GCALL)
     :in-theory (disable (:d ,GL::GFN)))))

(local (defthm logbitp-when-not-integers
    (and (implies (not (integerp a))
        (equal (logbitp a b) (logbitp 0 b)))
      (implies (not (integerp b))
        (equal (logbitp a b) (logbitp a 0))))
    :hints (("Goal" :in-theory (enable logbitp)))))

(def-g-correct-thm logbitp
  eval-g-base
  :hints `(("Goal" :in-theory (e/d* (general-concretep-atom (:ruleset general-object-possibilities))
       ((:definition ,GL::GFN) general-integerp-eval-to-integerp
         general-boolean-value-correct
         bool-cond-itep-eval
         boolean-listp
         member-equal
         general-concretep-def
         general-concretep-def
         equal-of-booleans-rewrite
         hons-assoc-equal
         default-car
         default-cdr
         mv-nth-cons-meta
         possibilities-for-x-5
         possibilities-for-x-3
         general-boolean-value-cases
         logbitp
         bfr-list->s
         bfr-list->u
         (:rules-of-class :type-prescription :here))
       ((:type-prescription bfr-eval)))
     :induct (,GL::GFN i j . ,GL::PARAMS)
     :expand ((,GL::GFN i j . ,GL::PARAMS)))))