theorem BitVec.testBit_toNat {w i : Nat} (x : BitVec w) : x.toNat.testBit i = x.getLsbD i

@[simp]

theorem BitVec.getLsbD_ofFin {n : Nat} (x : Fin (2 ^ n)) (i : Nat) : { toFin := x }.getLsbD i = (↑x).testBit i

@[simp]

theorem BitVec.getLsbD_of_ge {w : Nat} (x : BitVec w) (i : Nat) (ge : w ≤ i) : x.getLsbD i = false

theorem BitVec.eq_of_toNat_eq {n : Nat} {x y : BitVec n} : x.toNat = y.toNat → x = y

Prove equality of bitvectors in terms of nat operations.

theorem BitVec.eq_of_getLsbD_eq {w : Nat} {x y : BitVec w} (pred : ∀ (i : Nat), i < w → x.getLsbD i = y.getLsbD i) : x = y

@[simp]

theorem BitVec.toNat_ofNat (x w : Nat) : (BitVec.ofNat w x).toNat = x % 2 ^ w

theorem BitVec.eq_of_getElem_eq {n : Nat} {x y : BitVec n} : (∀ (i : Nat) (hi : i < n), x[i] = y[i]) → x = y

theorem BitVec.eq_of_getElem_eq_iff {n : Nat} {x y : BitVec n} : x = y ↔ ∀ (i : Nat) (hi : i < n), x[i] = y[i]

@[simp]

theorem BitVec.toNat_append {m n : Nat} (x : BitVec m) (y : BitVec n) : (x ++ y).toNat = x.toNat <<< n ||| y.toNat

@[simp]

theorem BitVec.toNat_ofBool (b : Bool) : (ofBool b).toNat = b.toNat

@[simp]

theorem BitVec.toNat_cast {w v : Nat} (h : w = v) (x : BitVec w) : (BitVec.cast h x).toNat = x.toNat

@[simp]

theorem BitVec.toNat_ofFin {n : Nat} (x : Fin (2 ^ n)) : { toFin := x }.toNat = ↑x

@[simp]

theorem BitVec.toNat_ofNatLT {w : Nat} (x : Nat) (p : x < 2 ^ w) : (x#'p).toNat = x

@[simp]

theorem BitVec.toNat_cons {w : Nat} (b : Bool) (x : BitVec w) : (cons b x).toNat = b.toNat <<< w ||| x.toNat

theorem BitVec.getElem_cons {b : Bool} {n : Nat} {x : BitVec n} {i : Nat} (h : i < n + 1) : (cons b x)[i] = if h : i = n then b else x[i]

@[simp]

theorem BitVec.toNat_setWidth' {m n : Nat} (p : m ≤ n) (x : BitVec m) : (setWidth' p x).toNat = x.toNat

@[simp]

theorem BitVec.toNat_setWidth {n : Nat} (i : Nat) (x : BitVec n) : (setWidth i x).toNat = x.toNat % 2 ^ i

@[simp]

theorem BitVec.ofNat_toNat {n : Nat} (m : Nat) (x : BitVec n) : BitVec.ofNat m x.toNat = setWidth m x

theorem BitVec.getElem_setWidth' {w v : Nat} (x : BitVec w) (i : Nat) (h : w ≤ v) (hi : i < v) : (setWidth' h x)[i] = x.getLsbD i

@[simp]

theorem BitVec.getElem_setWidth {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) (h : i < m) : (setWidth m x)[i] = x.getLsbD i

@[simp]

theorem BitVec.cons_msb_setWidth {w : Nat} (x : BitVec (w + 1)) : cons x.msb (setWidth w x) = x

@[simp]

theorem BitVec.toNat_neg {n : Nat} (x : BitVec n) : (-x).toNat = (2 ^ n - x.toNat) % 2 ^ n

@[simp]

theorem BitVec.setWidth_neg_of_le {v w : Nat} {x : BitVec v} (h : w ≤ v) : setWidth w (-x) = -setWidth w x