gl-misc-defs

(encapsulate nil
  (local (include-book "arithmetic/top-with-meta" :dir :system))
  (local (defthm integerp-1/2-x-requires-integerp-x
      (implies (and (acl2-numberp x) (not (integerp x)))
        (not (integerp (* 1/2 x))))
      :hints (("goal" :cases ((equal (imagpart x) 0))))))
  (defthmd evenp-is-logbitp
    (equal (evenp x)
      (or (not (acl2-numberp x))
        (and (integerp x) (equal (logbitp 0 x) nil))))
    :hints (("Goal" :in-theory (enable logbitp)))
    :rule-classes :definition))

(encapsulate nil
  (local (include-book "arithmetic/top-with-meta" :dir :system))
  (defthmd optimize-expt-2-for-gl
    (equal (expt r i)
      (if (and (equal r 2) (natp i))
        (ash 1 i)
        (expt-fallback r i)))))

(encapsulate nil
  (local (include-book "std/basic/two-nats-measure" :dir :system))
  (local (include-book "arithmetic-3/floor-mod/floor-mod" :dir :system))
  (local (in-theory (enable ash logbitp acl2-count)))
  (local (defthm ash-of-negative-1
      (implies (posp x) (equal (ash x -1) (floor x 2)))))
  (local (defthm nonnegative-integer-quotient-of-2
      (implies (natp x)
        (equal (nonnegative-integer-quotient x 2) (floor x 2)))))
  (defun logcount-of-natural
    (n)
    (if (zp n)
      0
      (+ (if (logbitp 0 n)
          1
          0)
        (logcount-of-natural (ash n -1)))))
  (defthm logcount-of-natural-correct
    (implies (natp n)
      (equal (logcount-of-natural n) (logcount n)))
    :hints (("Goal" :in-theory (enable logcount) :induct (logcount n))))
  (defun logcount-for-gl
    (x)
    (cond ((zip x) 0)
      ((< x 0) (logcount-of-natural (lognot x)))
      (t (logcount-of-natural x))))
  (local (defthm crock
      (implies (and (integerp a) (< a 0)) (natp (lognot a)))))
  (defthmd logcount-for-gl-correct
    (equal (logcount x) (logcount-for-gl x))
    :rule-classes :definition))

(encapsulate nil
  (local (include-book "arithmetic-3/floor-mod/floor-mod" :dir :system))
  (local (in-theory (enable nonnegative-integer-quotient)))
  (defthmd nonnegative-integer-quotient-for-gl
    (equal (nonnegative-integer-quotient i j)
      (floor (nfix i) (nfix j)))))

(encapsulate nil
  (local (include-book "centaur/bitops/ihsext-basics" :dir :system))
  (local (include-book "arithmetic/top-with-meta" :dir :system))
  (defthmd logcar-for-gl
    (equal (logcar i) (logand 1 i))
    :hints (("Goal" :in-theory (enable loghead**))))
  (table preferred-defs 'logcar$inline 'logcar-for-gl)
  (defthmd logcdr-for-gl
    (equal (logcdr i) (ash i -1))
    :hints (("Goal" :in-theory (enable logtail**))))
  (table preferred-defs 'logcdr$inline 'logcdr-for-gl)
  (defthmd logcons-for-gl
    (equal (logcons b i) (logior (bfix b) (ash i 1)))
    :hints (("Goal" :in-theory (enable logior** ash**))))
  (table preferred-defs 'logcons$inline 'logcons-for-gl)
  (defun ensure-negative
    (x)
    (declare (xargs :guard (integerp x)))
    (if (<= 0 x)
      (lognot x)
      x))
  (defthm ensure-negative-when-negative
    (implies (negp x) (equal (ensure-negative x) x)))
  (defthmd logtail-for-gl
    (equal (logtail pos i)
      (if (zp pos)
        (ifix i)
        (ash i (ensure-negative (- (pos-fix pos)))))))
  (table preferred-defs 'logtail$inline 'logtail-for-gl)
  (defthmd loghead-for-gl
    (equal (loghead size i) (logapp size i 0)))
  (table preferred-defs 'loghead$inline 'loghead-for-gl))