chore: add theorem for bitvec_152 (#605)

PR to solve [issue#602](#602) (`b * BitVec.allOnes w = -b`) --------- Co-authored-by: Tobias Grosser <[email protected]>
opencompl · Sep 8, 2024 · cefc98a · cefc98a
1 parent a938776
commit cefc98a
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean
@@ -528,6 +528,11 @@ theorem one_shiftLeft_mul {x y : BitVec w} :
     1#w <<< x.toNat * y = y <<< x.toNat := by
   simp [←BitVec.mul_twoPow_eq_shiftLeft, BitVec.mul_comm]
 
+@[simp]
+theorem mul_allOnes {x : BitVec w} :
+    x * BitVec.allOnes w = -x := by
+  simp [← BitVec.negOne_eq_allOnes]
+
 end BitVec
 
 namespace Bool