logand-helper - ACL2 Book

Included Books

top more-floor-mod floor-mod floor-mod-basic truncate-rem

other

(in-package "ACL2")

local

(local (include-book "../basic-ops/top"))

local

(local (include-book "more-floor-mod"))

local

(local (include-book "floor-mod"))

local

(local (include-book "floor-mod-basic"))

local

(local (include-book "truncate-rem"))

local

(local (set-default-hints '((nonlinearp-default-hint stable-under-simplificationp
       hist
       pspv))))

local

(local (in-theory (disable not-integerp-type-set-rules
      integerp-mod-1
      integerp-mod-2
      integerp-mod-3
      mod-bounds-1
      |(floor (+ x y) z) where (< 0 z)|
      reduce-additive-constant-<
      default-times-1
      default-times-2
      mod-x-y-=-x-y
      mod-x-y-=-x+y
      cancel-mod-+
      default-plus-1
      default-plus-2
      default-floor-1
      default-floor-2
      linear-floor-bounds-1
      linear-floor-bounds-2
      linear-floor-bounds-3
      expt-type-prescription-nonpositive-base-odd-exponent
      expt-type-prescription-nonpositive-base-even-exponent
      expt-type-prescription-negative-base-odd-exponent
      expt-type-prescription-negative-base-even-exponent
      expt-type-prescription-integerp-base
      expt-type-prescription-positive-base
      expt-type-prescription-integerp-base-b
      expt-type-prescription-integerp-base-a)))

local

(local (encapsulate ((op (x y) t))
    (local (defun op (x y) (+ x y)))
    (defthm op-comm (equal (op y x) (op x y)))
    (defthm op-assoc (equal (op (op x y) z) (op x (op y z))))))

local

(local (defthm op-comm-2
    (equal (op y (op x z)) (op x (op y z)))
    :hints (("Goal" :in-theory (disable op-comm op-assoc)
       :use ((:instance op-assoc (x y) (y x) (z z)) (:instance op-comm)
         (:instance op-assoc))))))

|(equal (logand x y) -1)|theorem

(defthm |(equal (logand x y) -1)|
  (equal (equal (logand x y) -1)
    (and (equal x -1) (equal y -1))))

local

(local (defthm logand-=-0-crock-a
    (implies (equal (logand y z) 0)
      (equal (logand (logand x y) z) 0))))

logand-assoctheorem

(defthm logand-assoc
  (equal (logand (logand x y) z) (logand x (logand y z)))
  :hints (("Goal" :do-not '(generalize eliminate-destructors))))

logand-y-xtheorem

(defthm logand-y-x (equal (logand y x) (logand x y)))

logand-y-x-ztheorem

(defthm logand-y-x-z
  (equal (logand y x z) (logand x y z))
  :hints (("Goal" :use (:functional-instance op-comm-2 (op binary-logand)))))