Filtering...

bits-equiv

books/std/lists/bits-equiv

Included Books

list-defuns arith-equiv-defs universal-equiv equiv take
other
(in-package "ACL2")
include-book
(include-book "list-defuns")
include-book
(include-book "std/basic/arith-equiv-defs" :dir :system)
include-book
(include-book "centaur/misc/universal-equiv" :dir :system)
local
(local (include-book "equiv"))
local
(local (include-book "take"))
other
(def-universal-equiv bits-equiv
  :qvars (i)
  :equiv-terms ((bit-equiv (nth i x)))
  :parents (bitarr)
  :short "Bit-for-bit list equivalence: @('bits-equiv') recognizes lists whose
  @(see nth) elements are @(see bit-equiv) to one another.  It is often useful
  for reasoning about bit arrays like @(see bitarr).")
other
(defsection bits-equiv-thms
  :extension (bits-equiv)
  (defcong bits-equiv
    bit-equiv
    (nth i x)
    2
    :hints (("Goal" :in-theory (e/d (bits-equiv-necc) (bit-equiv)))))
  (defcong bits-equiv
    bits-equiv
    (update-nth i v x)
    3
    :hints ((and stable-under-simplificationp
       `(:expand (,(CAR (LAST CLAUSE)))))))
  (defcong bit-equiv
    bits-equiv
    (update-nth i v x)
    2
    :hints ((and stable-under-simplificationp
       `(:expand (,(CAR (LAST CLAUSE)))))))
  (defcong bits-equiv
    bits-equiv
    (cdr a)
    1
    :hints (("goal" :in-theory (disable default-cdr nth)) (and stable-under-simplificationp
        `(:expand (,(CAR (LAST CLAUSE)))))
      (and stable-under-simplificationp
        '(:use ((:instance bits-equiv-necc
             (i (+ 1 (nfix (bits-equiv-witness (cdr a) (cdr a-equiv)))))
             (x a)
             (y a-equiv)))
          :in-theory (e/d nil
            (bits-equiv-necc bits-equiv-implies-bit-equiv-nth-2))))))
  (defcong bits-equiv
    bit-equiv
    (car x)
    1
    :hints (("goal" :use ((:instance bits-equiv-implies-bit-equiv-nth-2 (i 0)))
       :in-theory (disable bits-equiv-implies-bit-equiv-nth-2))))
  (defcong bit-equiv
    bits-equiv
    (cons a b)
    1
    :hints (("Goal" :in-theory (enable bits-equiv)
       :expand ((:free (a b c) (nth a (cons b c)))))))
  (defcong bits-equiv
    bits-equiv
    (cons a b)
    2
    :hints ((and stable-under-simplificationp
       `(:expand (,(CAR (LAST CLAUSE)) (:free (a b c) (nth a (cons b c))))
         :in-theory (disable bit-equiv))))))