Filtering...

g-ash

books/centaur/gl/g-ash
other
(in-package "GL")
other
(include-book "g-if")
other
(include-book "g-primitives-help")
other
(include-book "symbolic-arithmetic")
other
(include-book "eval-g-base")
other
(local (include-book "eval-g-base-help"))
other
(local (include-book "hyp-fix"))
other
(local (include-book "clause-processors/just-expand" :dir :system))
other
(set-inhibit-warnings "theory")
g-ash-of-integersfunction
(defun g-ash-of-integers
  (i c)
  (declare (xargs :guard (and (general-integerp i)
        (general-integerp c))))
  (mk-g-integer (bfr-ash-ss 1
      (general-integer-bits i)
      (general-integer-bits c))))
other
(in-theory (disable (g-ash-of-integers)))
other
(defthm deps-of-g-ash-of-integers
  (implies (and (not (gobj-depends-on k p i))
      (not (gobj-depends-on k p c))
      (general-integerp i)
      (general-integerp c))
    (not (gobj-depends-on k
        p
        (g-ash-of-integers i c)))))
other
(defthm g-ash-of-integers-correct
  (implies (and (general-integerp x)
      (general-integerp y))
    (equal (eval-g-base (g-ash-of-integers x y)
        env)
      (ash (eval-g-base x env)
        (eval-g-base y env))))
  :hints (("goal" :in-theory (e/d* ((:ruleset general-object-possibilities))
       (general-integerp))
     :do-not-induct t)))
other
(def-g-binary-op ash
  (b* ((i-num (if (general-integerp i)
         i
         0)) (c-num (if (general-integerp c)
          c
          0)))
    (gret (g-ash-of-integers i-num c-num))))
other
(verify-g-guards ash
  :hints `(("Goal" :in-theory (disable ,GL::GFN))))
other
(local (defthm pbfr-list-depends-on-of-empty
    (not (pbfr-list-depends-on k p '(nil)))
    :hints (("Goal" :in-theory (enable pbfr-list-depends-on)))))
other
(def-gobj-dependency-thm ash
  :hints `(("goal" :in-theory (e/d ((:i ,GL::GFN))
       ((:d ,GL::GFN) gobj-depends-on))) (just-induct-and-expand ,GL::GCALL)))
other
(local (defthm ash-of-non-integers
    (and (implies (not (integerp i))
        (equal (ash i c) (ash 0 c)))
      (implies (not (integerp c))
        (equal (ash i c) (ash i 0))))))
other
(local (in-theory (disable ash)))
other
(def-g-correct-thm ash
  eval-g-base
  :hints `(("goal" :in-theory (enable eval-g-base-list)
     :induct ,GL::GCALL
     :expand (,GL::GCALL)
     :do-not-induct t)))