feat: complete the set of bitvector theorems

SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean

@@ -103,12 +103,33 @@ def AndOrXor2515_rhs (w : ℕ) :
 def ushr_xor_right_distrib (c1 c2 c3 : BitVec w): (c1 ^^^ c2) >>> c3 = (c1 >>> c3) ^^^ (c2 >>> c3) := by
   unfold HShiftRight.hShiftRight instHShiftRightBitVec
   ext
+  simp only []
+  simp only [getLsb_ushiftRight]
+  simp?
+
+def ushr_xor_left_distrib (c1 c2 c3 : BitVec w): c1 >>> (c2 ^^^ c3) = (c1 >>> c2) ^^^ (c1 >>> c3) := by
+  unfold HShiftRight.hShiftRight instHShiftRightBitVec
+  simp only []
+  ext
   simp [getLsb_ushiftRight]
+  sorry
+
+#check Nat.right_distrib
+#check Nat.left_distrib
 
 def xor_assoc (c1 c2 c3 : BitVec w): c1 ^^^ c2 ^^^ c3 = c1 ^^^ (c2 ^^^ c3) := by
   ext i
   simp
 
+def and_assoc (c1 c2 c3 : BitVec w): c1 &&& c2 &&& c3 = c1 &&& (c2 &&& c3) := by
+  ext i
+  simp [Bool.and_assoc]
+
+def or_assoc (c1 c2 c3 : BitVec w): c1 ||| c2 ||| c3 = c1 ||| (c2 ||| c3) := by
+  ext i
+  simp [Bool.or_assoc]
+
+
 def alive_simplifyAndOrXor2515 (w : Nat) :
   AndOrXor2515_lhs w ⊑ AndOrXor2515_rhs w := by
   simp only [AndOrXor2515_lhs, AndOrXor2515_rhs]