bit-lemmas

(in-package "AIGNET")

(include-book "centaur/bitops/ihsext-basics" :dir :system)

(defthm b-xor-lemma1
  (equal (b-xor a
      (b-not (b-xor b a)))
    (b-not b))
  :hints (("Goal" :in-theory (enable b-xor b-not))))

(defthm b-xor-lemma2
  (equal (b-xor (b-not a)
      (b-xor a b))
    (b-not b))
  :hints (("Goal" :in-theory (enable b-xor b-not))))

(defthm b-xor-lemma3
  (equal (b-xor a
      (b-xor b a))
    (bfix b))
  :hints (("Goal" :in-theory (enable b-xor))))

(defthm b-xor-lemma4
  (equal (b-xor (b-xor a b)
      (b-xor a c))
    (b-xor b c))
  :hints (("Goal" :in-theory (enable b-xor))))

(table invisible-fns-table
  'bfix$inline
  '(b-not$inline))

(defthm associativity-of-b-xor
  (equal (b-xor (b-xor a b)
      c)
    (b-xor a
      (b-xor b c)))
  :hints (("Goal" :in-theory (enable b-xor b-not))))

(defthm commutativity-2-of-b-xor
  (equal (b-xor a
      (b-xor b c))
    (b-xor b
      (b-xor a c)))
  :hints (("Goal" :in-theory (enable b-xor b-not)))
  :rule-classes ((:rewrite :loop-stopper ((a b bfix$inline)))))

(defthm b-xor-same-2
  (equal (b-xor a
      (b-xor a b))
    (bfix b))
  :hints (("Goal" :in-theory (enable b-xor))))