Filtering...

arith-equivs

books/std/basic/arith-equivs

Included Books

arith-equiv-defs mfc-utils
other
(in-package "ACL2")
include-book
(include-book "arith-equiv-defs")
include-book
(include-book "std/lists/mfc-utils" :dir :system)
posp-redefinitiontheorem
(defthm posp-redefinition (equal (posp x) (not (zp x))))
ifix-when-integerptheorem
(defthm ifix-when-integerp
  (implies (integerp x) (equal (ifix x) x)))
nfix-when-natptheorem
(defthm nfix-when-natp
  (implies (natp x) (equal (nfix x) x)))
bfix-when-bitptheorem
(defthm bfix-when-bitp
  (implies (bitp x) (equal (bfix x) x)))
ifix-when-not-integerptheorem
(defthm ifix-when-not-integerp
  (implies (not (integerp x)) (equal (ifix x) 0))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))
nfix-when-not-natptheorem
(defthm nfix-when-not-natp
  (implies (not (natp x)) (equal (nfix x) 0))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))
bfix-when-not-bitptheorem
(defthm bfix-when-not-bitp
  (implies (not (bitp x)) (equal (bfix x) 0))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))
int-equiv-zerotheorem
(defthm int-equiv-zero (equal (int-equiv x 0) (zip x)))
nat-equiv-zerotheorem
(defthm nat-equiv-zero (equal (nat-equiv x 0) (zp x)))
ifix-equal-to-0theorem
(defthm ifix-equal-to-0 (equal (equal (ifix x) 0) (zip x)))
nfix-equal-to-zerotheorem
(defthm nfix-equal-to-zero
  (equal (equal (nfix x) 0) (zp x)))
ifix-equal-to-nonzero-consttheorem
(defthm ifix-equal-to-nonzero-const
  (implies (and (syntaxp (quotep n)) (not (zip n)))
    (equal (equal (ifix x) n) (equal x n))))
nfix-equal-to-nonzero-consttheorem
(defthm nfix-equal-to-nonzero-const
  (implies (and (syntaxp (quotep n)) (not (zp n)))
    (equal (equal (nfix x) n) (equal x n))))
ifix-equal-to-nonzerotheorem
(defthm ifix-equal-to-nonzero
  (implies (not (zip n))
    (equal (equal (ifix x) n) (equal x n))))
nfix-equal-to-nonzerotheorem
(defthm nfix-equal-to-nonzero
  (implies (not (zp n))
    (equal (equal (nfix x) n) (equal x n))))
bfix-gt-0theorem
(defthm bfix-gt-0 (equal (< 0 (bfix x)) (equal x 1)))
bfix-equal-0theorem
(defthm bfix-equal-0
  (equal (equal 0 (bfix x)) (not (bit->bool x)))
  :hints (("Goal" :in-theory (enable bit->bool))))
bfix-equal-1theorem
(defthm bfix-equal-1
  (equal (equal 1 (bfix x)) (bit->bool x))
  :hints (("Goal" :in-theory (enable bit->bool))))
bfix-when-not-1theorem
(defthm bfix-when-not-1
  (implies (not (equal x 1)) (equal (bfix x) 0)))
local
(local (in-theory (enable negp)))
negp-when-integerptheorem
(defthm negp-when-integerp
  (implies (integerp x) (equal (negp x) (< x 0)))
  :hints (("Goal" :in-theory (enable negp)))
  :rule-classes ((:rewrite :backchain-limit-lst (1))))
negp-when-less-than-0theorem
(defthm negp-when-less-than-0
  (implies (< x 0) (equal (negp x) (integerp x)))
  :hints (("Goal" :in-theory (enable negp)))
  :rule-classes ((:rewrite :backchain-limit-lst (1))))
natp-when-integerptheorem
(defthm natp-when-integerp
  (implies (integerp x) (equal (natp x) (<= 0 x)))
  :hints (("Goal" :in-theory (enable negp)))
  :rule-classes ((:rewrite :backchain-limit-lst (1))))
natp-when-gte-0theorem
(defthm natp-when-gte-0
  (implies (<= 0 x) (equal (natp x) (integerp x)))
  :hints (("Goal" :in-theory (enable negp)))
  :rule-classes ((:rewrite :backchain-limit-lst (1))))
zp-when-integerptheorem
(defthm zp-when-integerp
  (implies (integerp x) (equal (zp x) (<= x 0)))
  :hints (("Goal" :in-theory (enable negp)))
  :rule-classes ((:rewrite :backchain-limit-lst (1))))
zp-when-gt-0theorem
(defthm zp-when-gt-0
  (implies (< 0 x) (equal (zp x) (not (integerp x))))
  :hints (("Goal" :in-theory (enable negp)))
  :rule-classes ((:rewrite :backchain-limit-lst (1))))
negp-fc-1theorem
(defthm negp-fc-1
  (implies (negp x) (integerp x))
  :rule-classes :forward-chaining)
negp-fc-2theorem
(defthm negp-fc-2
  (implies (negp x) (< x 0))
  :rule-classes :forward-chaining)
ifix-negative-to-negptheorem
(defthm ifix-negative-to-negp
  (equal (< (ifix x) 0) (negp x)))
ifix-positive-to-non-zptheorem
(defthm ifix-positive-to-non-zp
  (equal (< 0 (ifix x)) (not (zp x))))
nfix-positive-to-non-zptheorem
(defthm nfix-positive-to-non-zp
  (equal (< 0 (nfix x)) (not (zp x))))
bfix-positive-to-equal-1theorem
(defthm bfix-positive-to-equal-1
  (equal (< 0 (bfix x)) (equal 1 x)))
zip-forward-to-int-equiv-0theorem
(defthm zip-forward-to-int-equiv-0
  (implies (zip x) (int-equiv x 0))
  :rule-classes :forward-chaining)
zp-forward-to-nat-equiv-0theorem
(defthm zp-forward-to-nat-equiv-0
  (implies (zp x) (nat-equiv x 0))
  :rule-classes :forward-chaining)
zbp-forward-to-bit-equiv-0theorem
(defthm zbp-forward-to-bit-equiv-0
  (implies (zbp x) (bit-equiv x 0))
  :rule-classes :forward-chaining)
not-negp-implies-ifix-nonnegativetheorem
(defthm not-negp-implies-ifix-nonnegative
  (implies (not (negp x)) (<= 0 (ifix x)))
  :rule-classes :forward-chaining)
zp-implies-ifix-nonpositivetheorem
(defthm zp-implies-ifix-nonpositive
  (implies (zp x) (<= (ifix x) 0))
  :rule-classes :forward-chaining)
other
(def-ruleset! arith-equiv-minimal-forwarding
  '(zip-forward-to-int-equiv-0 zp-forward-to-nat-equiv-0
    zbp-forward-to-bit-equiv-0
    not-negp-implies-ifix-nonnegative
    zp-implies-ifix-nonpositive))
negative-forward-to-nat-equiv-0theorem
(defthm negative-forward-to-nat-equiv-0
  (implies (< n 0) (nat-equiv n 0))
  :rule-classes :forward-chaining)
nonpositive-forward-to-nat-equiv-0theorem
(defthm nonpositive-forward-to-nat-equiv-0
  (implies (<= n 0) (nat-equiv n 0))
  :rule-classes :forward-chaining)
not-integerp-forward-to-int-equiv-0theorem
(defthm not-integerp-forward-to-int-equiv-0
  (implies (not (integerp x)) (int-equiv x 0))
  :rule-classes :forward-chaining)
not-natp-forward-to-int-equiv-0theorem
(defthm not-natp-forward-to-int-equiv-0
  (implies (not (natp x)) (nat-equiv x 0))
  :rule-classes :forward-chaining)
not-bitp-forward-to-int-equiv-0theorem
(defthm not-bitp-forward-to-int-equiv-0
  (implies (not (bitp x)) (bit-equiv x 0))
  :rule-classes :forward-chaining)
equal-ifix-foward-to-int-equivtheorem
(defthm equal-ifix-foward-to-int-equiv
  (implies (and (equal (ifix x) y)
      (syntaxp (not (and (consp y) (eq (car y) 'ifix)))))
    (int-equiv x y))
  :rule-classes :forward-chaining)
equal-ifix-foward-to-int-equiv-boththeorem
(defthm equal-ifix-foward-to-int-equiv-both
  (implies (equal (ifix x) (ifix y)) (int-equiv x y))
  :rule-classes :forward-chaining)
equal-nfix-foward-to-nat-equivtheorem
(defthm equal-nfix-foward-to-nat-equiv
  (implies (and (equal (nfix x) y)
      (syntaxp (not (and (consp y) (eq (car y) 'nfix)))))
    (nat-equiv x y))
  :rule-classes :forward-chaining)
equal-nfix-foward-to-nat-equiv-boththeorem
(defthm equal-nfix-foward-to-nat-equiv-both
  (implies (equal (nfix x) (nfix y)) (nat-equiv x y))
  :rule-classes :forward-chaining)
equal-bfix-foward-to-bit-equivtheorem
(defthm equal-bfix-foward-to-bit-equiv
  (implies (and (equal (bfix x) y)
      (syntaxp (not (and (consp y) (eq (car y) 'bfix)))))
    (bit-equiv x y))
  :rule-classes :forward-chaining)
equal-bfix-foward-to-bit-equiv-boththeorem
(defthm equal-bfix-foward-to-bit-equiv-both
  (implies (equal (bfix x) (bfix y)) (bit-equiv x y))
  :rule-classes :forward-chaining)
equal-bit->bool-foward-to-bit-equivtheorem
(defthm equal-bit->bool-foward-to-bit-equiv
  (implies (and (equal (bit->bool x) y)
      (syntaxp (not (and (consp y) (eq (car y) 'bit->bool)))))
    (bit-equiv x (bool->bit y)))
  :hints (("Goal" :in-theory (enable bit->bool)))
  :rule-classes :forward-chaining)
equal-bit->bool-foward-to-bit-equiv-boththeorem
(defthm equal-bit->bool-foward-to-bit-equiv-both
  (implies (equal (bit->bool x) (bit->bool y))
    (bit-equiv x y))
  :hints (("Goal" :in-theory (enable bit->bool)))
  :rule-classes :forward-chaining)
not-equal-1-forward-to-bit-equivtheorem
(defthm not-equal-1-forward-to-bit-equiv
  (implies (not (equal x 1)) (bit-equiv x 0))
  :rule-classes :forward-chaining)
not-bit->bool-forward-to-bit-equiv-0theorem
(defthm not-bit->bool-forward-to-bit-equiv-0
  (implies (not (bit->bool x)) (bit-equiv x 0))
  :hints (("Goal" :in-theory (enable bit->bool)))
  :rule-classes :forward-chaining)
bit->bool-forward-to-equal-1theorem
(defthm bit->bool-forward-to-equal-1
  (implies (bit->bool x) (equal x 1))
  :hints (("Goal" :in-theory (enable bit->bool)))
  :rule-classes :forward-chaining)
inequality-with-nfix-forward-to-natp-1theorem
(defthmd inequality-with-nfix-forward-to-natp-1
  (implies (and (< a (nfix n)) (<= 0 a)) (natp n))
  :rule-classes :forward-chaining)
inequality-with-nfix-forward-to-natp-2theorem
(defthmd inequality-with-nfix-forward-to-natp-2
  (implies (and (<= a (nfix n)) (< 0 a)) (natp n))
  :rule-classes :forward-chaining)
inequality-with-nfix-hyp-1theorem
(defthm inequality-with-nfix-hyp-1
  (implies (and (syntaxp (rewriting-negative-literal-fn `(< ,A (nfix ,N)) mfc state))
      (<= 0 a))
    (equal (< a (nfix n)) (and (natp n) (< a n)))))
inequality-with-nfix-hyp-2theorem
(defthm inequality-with-nfix-hyp-2
  (implies (and (syntaxp (rewriting-positive-literal-fn `(< (nfix ,N) ,A) mfc state))
      (< 0 a))
    (equal (< (nfix n) a) (not (and (natp n) (<= a n)))))
  :hints (("Goal" :in-theory (enable nfix))))
other
(def-ruleset! arith-equiv-forwarding
  '(negative-forward-to-nat-equiv-0 nonpositive-forward-to-nat-equiv-0
    not-integerp-forward-to-int-equiv-0
    not-natp-forward-to-int-equiv-0
    not-bitp-forward-to-int-equiv-0
    equal-ifix-foward-to-int-equiv
    equal-ifix-foward-to-int-equiv-both
    equal-nfix-foward-to-nat-equiv
    equal-nfix-foward-to-nat-equiv-both
    equal-bfix-foward-to-bit-equiv
    equal-bfix-foward-to-bit-equiv-both
    equal-bit->bool-foward-to-bit-equiv
    equal-bit->bool-foward-to-bit-equiv-both
    not-equal-1-forward-to-bit-equiv))
equal-of-ifixestheorem
(defthmd equal-of-ifixes
  (equal (equal (ifix a) (ifix b)) (int-equiv a b)))
equal-of-nfixestheorem
(defthmd equal-of-nfixes
  (equal (equal (nfix a) (nfix b)) (nat-equiv a b)))
equal-of-bfixestheorem
(defthmd equal-of-bfixes
  (equal (equal (bfix a) (bfix b)) (bit-equiv a b)))
equal-of-bit->boolstheorem
(defthmd equal-of-bit->bools
  (equal (equal (bit->bool a) (bit->bool b)) (bit-equiv a b))
  :hints (("Goal" :in-theory (enable bit->bool))))
in-theory
(in-theory (disable natp nfix bitp bfix ifix))
other
(defcong nat-equiv equal (nth n x) 1)
other
(defcong nat-equiv equal (update-nth n v x) 1)
other
(defcong nat-equiv equal (nthcdr n x) 1)
other
(defcong nat-equiv equal (take n x) 1)
other
(defcong nat-equiv equal (resize-list lst n default) 2)
other
(defcong nat-equiv
  equal
  (logbitp n x)
  1
  :hints (("Goal" :in-theory (enable logbitp))))
other
(defcong int-equiv
  equal
  (logbitp n x)
  2
  :hints (("Goal" :in-theory (enable logbitp))))
other
(defcong nat-equiv
  equal
  (logbit n x)
  1
  :hints (("Goal" :in-theory (enable logbit))))
other
(defcong int-equiv
  equal
  (logbit n x)
  2
  :hints (("Goal" :in-theory (enable logbit))))
other
(defcong int-equiv
  equal
  (logcar x)
  1
  :hints (("Goal" :in-theory (enable logcar))))
other
(defcong int-equiv
  equal
  (logcdr x)
  1
  :hints (("Goal" :in-theory (enable logcdr))))
other
(defcong bit-equiv
  equal
  (logcons b x)
  1
  :hints (("Goal" :in-theory (enable logcons))))
other
(defcong int-equiv
  equal
  (logcons b x)
  2
  :hints (("Goal" :in-theory (enable logcons))))
other
(defcong bit-equiv equal (b-not x) 1)
other
(defcong bit-equiv equal (b-and x y) 1)
other
(defcong bit-equiv equal (b-and x y) 2)
other
(defcong bit-equiv equal (b-ior x y) 1)
other
(defcong bit-equiv equal (b-ior x y) 2)
other
(defcong bit-equiv equal (b-xor x y) 1)
other
(defcong bit-equiv equal (b-xor x y) 2)
other
(defcong bit-equiv equal (b-eqv x y) 1)
other
(defcong bit-equiv equal (b-eqv x y) 2)
other
(defcong bit-equiv equal (b-nand x y) 1)
other
(defcong bit-equiv equal (b-nand x y) 2)
other
(defcong bit-equiv equal (b-nor x y) 1)
other
(defcong bit-equiv equal (b-nor x y) 2)
other
(defcong bit-equiv equal (b-andc1 x y) 1)
other
(defcong bit-equiv equal (b-andc1 x y) 2)
other
(defcong bit-equiv equal (b-andc2 x y) 1)
other
(defcong bit-equiv equal (b-andc2 x y) 2)
other
(defcong bit-equiv equal (b-orc1 x y) 1)
other
(defcong bit-equiv equal (b-orc1 x y) 2)
other
(defcong bit-equiv equal (b-orc2 x y) 1)
other
(defcong bit-equiv equal (b-orc2 x y) 2)
other
(defcong bit-equiv equal (b-ite test then else) 1)
other
(defcong bit-equiv equal (b-ite test then else) 2)
other
(defcong bit-equiv equal (b-ite test then else) 3)
other
(defcong int-equiv equal (lognot x) 1)
other
(defcong int-equiv
  equal
  (logand x y)
  1
  :hints (("goal" :in-theory (enable ifix))))
other
(defcong int-equiv
  equal
  (logand x y)
  2
  :hints (("goal" :in-theory (enable ifix))))
other
(defcong int-equiv
  equal
  (logior x y)
  1
  :hints (("goal" :in-theory (enable ifix))))
other
(defcong int-equiv
  equal
  (logior x y)
  2
  :hints (("goal" :in-theory (enable ifix))))
other
(defcong int-equiv
  equal
  (logxor x y)
  1
  :hints (("goal" :in-theory (enable ifix))))
other
(defcong int-equiv
  equal
  (logxor x y)
  2
  :hints (("goal" :in-theory (enable ifix))))
other
(defcong int-equiv
  equal
  (logite test then else)
  1
  :hints (("goal" :in-theory (e/d (ifix logite) ((force))))))
other
(defcong int-equiv
  equal
  (logite test then else)
  2
  :hints (("goal" :in-theory (e/d (ifix logite) ((force))))))
other
(defcong int-equiv
  equal
  (logite test then else)
  3
  :hints (("goal" :in-theory (e/d (ifix logite) ((force))))))
other
(defcong nat-equiv equal (loghead n x) 1)
other
(defcong int-equiv equal (loghead n x) 2)
other
(defcong nat-equiv equal (logtail n x) 1)
other
(defcong int-equiv equal (logtail n x) 2)
other
(defcong int-equiv
  equal
  (expt b i)
  2
  :hints (("Goal" :in-theory (enable ifix))))
other
(defcong int-equiv
  equal
  (ash i c)
  1
  :hints (("Goal" :in-theory (e/d (ifix) (floor)))))
other
(defcong int-equiv
  equal
  (ash i c)
  2
  :hints (("Goal" :in-theory (e/d (ifix) (floor)))))
other
(defcong int-equiv
  equal
  (integer-length x)
  1
  :hints (("Goal" :in-theory (enable ifix))))
other
(defcong nat-equiv equal (logapp size i j) 1)
other
(defcong int-equiv equal (logapp size i j) 2)
other
(defcong int-equiv equal (logapp size i j) 3)
other
(defcong nat-equiv
  equal
  (logext n x)
  1
  :hints (("Goal" :in-theory (e/d (nfix) (floor oddp expt)))))
other
(defcong int-equiv
  equal
  (logext n x)
  2
  :hints (("Goal" :in-theory (e/d (ifix) (logbitp logapp expt)))))
other
(defcong nat-equiv equal (logmask n) 1)
equal-1-of-bool->bitencapsulate
(encapsulate nil
  (local (in-theory (enable bool->bit bit->bool)))
  (defthm equal-1-of-bool->bit
    (iff (equal 1 (bool->bit x)) x))
  (defthm equal-0-of-bool->bit
    (equal (equal 0 (bool->bit x)) (not x)))
  (defthm bit->bool-of-bool->bit
    (equal (bit->bool (bool->bit x)) (not (not x))))
  (defthm bool->bit-of-equal-1
    (equal (bool->bit (equal 1 x)) (bfix x)))
  (defthm bool->bit-of-bit->bool
    (equal (bool->bit (bit->bool x)) (bfix x)))
  (defthm bool->bit-of-not
    (equal (bool->bit (not x)) (b-not (bool->bit x)))
    :hints (("Goal" :in-theory (enable b-not))))
  (defcong iff equal (bool->bit x) 1)
  (defthm bfix-when-bit->bool
    (implies (bit->bool x) (equal (bfix x) 1))
    :rule-classes ((:rewrite :backchain-limit-lst 0)))
  (defthm bfix-when-not-bit->bool
    (implies (not (bit->bool x)) (equal (bfix x) 0))
    :rule-classes ((:rewrite :backchain-limit-lst 0))))
other
(defsection bitops-in-terms-of-bit->bool
  (local (in-theory (enable bit->bool b-not b-and b-ior b-xor)))
  (defthmd bfix-in-terms-of-bit->bool
    (equal (bfix x)
      (if (bit->bool x)
        1
        0))
    :hints (("Goal" :in-theory (enable bfix))))
  (defthmd b-not-in-terms-of-bit->bool
    (equal (b-not x)
      (if (bit->bool x)
        0
        1))
    :hints (("Goal" :in-theory (enable bfix))))
  (defthmd b-and-in-terms-of-bit->bool
    (equal (b-and x y)
      (if (bit->bool x)
        (bfix y)
        0))
    :hints (("Goal" :in-theory (enable bfix))))
  (defthmd b-ior-in-terms-of-bit->bool
    (equal (b-ior x y)
      (if (bit->bool x)
        1
        (bfix y)))
    :hints (("Goal" :in-theory (enable bfix))))
  (defthmd b-xor-in-terms-of-bit->bool
    (equal (b-xor x y)
      (if (bit->bool x)
        (b-not y)
        (bfix y)))
    :hints (("Goal" :in-theory (enable bfix)))))
in-theory
(in-theory (disable* arith-equiv-forwarding))