This module contains the BitVec simplifying part of the bv_normalize simp set.

theorem Std.Tactic.BVDecide.Normalize.BitVec.le_ult {w : Nat} (x y : BitVec w) : (x ≤ y) = ¬y < x

theorem Std.Tactic.BVDecide.Normalize.BitVec.truncate_eq_zeroExtend {w n : Nat} (x : BitVec w) : BitVec.truncate n x = BitVec.zeroExtend n x

theorem Std.Tactic.BVDecide.Normalize.BitVec.ofNatLt_reduce {w : Nat} (n : Nat) (h : n < 2 ^ w) : n#'h = BitVec.ofNat w n

theorem Std.Tactic.BVDecide.Normalize.BitVec.ofBool_eq_if (b : Bool) : BitVec.ofBool b = if b = true then 1#1 else 0#1

theorem Std.Tactic.BVDecide.Normalize.BitVec.sdiv_udiv {w : Nat} (x y : BitVec w) : x.sdiv y = if x.msb = true then if y.msb = true then -x / -y else -(-x / y) else if y.msb = true then -(x / -y) else x / y

theorem Std.Tactic.BVDecide.Normalize.BitVec.smod_umod {w : Nat} (x y : BitVec w) : x.smod y = if x.msb = true then if y.msb = true then -(-x).umod (-y) else let u := (-x).umod y; if u = 0#w then u else y - u else if y.msb = true then let u := x.umod (-y); if u = 0#w then u else u + y else x.umod y

theorem Std.Tactic.BVDecide.Normalize.BitVec.smtSDiv_smtUDiv {w : Nat} (x y : BitVec w) : x.smtSDiv y = if x.msb = true then if y.msb = true then (-x).smtUDiv (-y) else -(-x).smtUDiv y else if y.msb = true then -x.smtUDiv (-y) else x.smtUDiv y

theorem Std.Tactic.BVDecide.Normalize.BitVec.srem_umod {w : Nat} (x y : BitVec w) : x.srem y = if x.msb = true then if y.msb = true then -(-x % -y) else -(-x % y) else if y.msb = true then x % -y else x % y

theorem Std.Tactic.BVDecide.Normalize.BitVec.getElem_eq_getLsbD {w : Nat} (a : BitVec w) (i : Nat) (h : i < w) : a[i] = a.getLsbD i

theorem Std.Tactic.BVDecide.Normalize.BitVec.ones_and {w : Nat} (a : BitVec w) : -1#w &&& a = a

theorem Std.Tactic.BVDecide.Normalize.BitVec.and_ones {w : Nat} (a : BitVec w) : a &&& -1#w = a

theorem Std.Tactic.BVDecide.Normalize.BitVec.and_contra {w : Nat} (a : BitVec w) : a &&& ~~~a = 0#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.and_contra' {w : Nat} (a : BitVec w) : ~~~a &&& a = 0#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.add_not {w : Nat} (a : BitVec w) : a + ~~~a = -1#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.not_add {w : Nat} (a : BitVec w) : ~~~a + a = -1#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.add_neg {w : Nat} (a : BitVec w) : a + (~~~a + 1#w) = 0#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.add_neg' {w : Nat} (a : BitVec w) : a + (1#w + ~~~a) = 0#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.neg_add {w : Nat} (a : BitVec w) : ~~~a + 1#w + a = 0#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.neg_add' {w : Nat} (a : BitVec w) : 1#w + ~~~a + a = 0#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.not_neg {w : Nat} (x : BitVec w) : ~~~(~~~x + 1#w) = x + -1#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.not_neg' {w : Nat} (x : BitVec w) : ~~~(1#w + ~~~x) = x + -1#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.not_neg'' {w : Nat} (x : BitVec w) : ~~~(x + 1#w) = ~~~x + -1#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.not_neg''' {w : Nat} (x : BitVec w) : ~~~(1#w + x) = ~~~x + -1#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.add_same {w : Nat} (a : BitVec w) : a + a = a * 2#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.add_const_left {w : Nat} (a b c : BitVec w) : a + (b + c) = a + b + c

theorem Std.Tactic.BVDecide.Normalize.BitVec.add_const_right {w : Nat} (a b c : BitVec w) : a + (b + c) = a + c + b

theorem Std.Tactic.BVDecide.Normalize.BitVec.add_const_left' {w : Nat} (a b c : BitVec w) : a + b + c = a + c + b

theorem Std.Tactic.BVDecide.Normalize.BitVec.add_const_right' {w : Nat} (a b c : BitVec w) : a + b + c = b + c + a

theorem Std.Tactic.BVDecide.Normalize.BitVec.shiftLeft_zero' {w w' : Nat} (n : BitVec w) : n <<< 0#w' = n

theorem Std.Tactic.BVDecide.Normalize.BitVec.ushiftRight_zero' {w w' : Nat} (n : BitVec w) : n >>> 0#w' = n

theorem Std.Tactic.BVDecide.Normalize.BitVec.zero_lt_iff_zero_neq {w : Nat} (a : BitVec w) : 0#w < a ↔ a ≠ 0#w

theorem Std.Tactic.BVDecide.Normalize.BitVec.zero_ult' {w : Nat} (a : BitVec w) : (0#w).ult a = (a != 0#w)

theorem Std.Tactic.BVDecide.Normalize.BitVec.max_ult {w : Nat} (a : BitVec w) : ¬-1#w < a

theorem Std.Tactic.BVDecide.Normalize.BitVec.max_ult' {w : Nat} (a : BitVec w) : (-1#w).ult a = false

theorem Std.Tactic.BVDecide.Normalize.BitVec.udiv_ofNat_eq_of_lt (w : Nat) (x : BitVec w) (n k : Nat) (hk : 2 ^ k = n) (hlt : k < w) : x / BitVec.ofNat w n = x >>> k

x / (BitVec.ofNat n) where n = 2^k is the same as shifting x right by k.