feat: bitvec_AddSub_1152 proof (#298)

Co-authored-by: Siddharth Bhat <[email protected]>
Co-authored-by: Tobias Grosser <[email protected]>

SSA/Projects/InstCombine/ForLean.lean

@@ -205,6 +205,12 @@ theorem udiv_one_eq_zero (a : BitVec w) (h : a > 1)
       assumption
     rw [Nat.div_eq_zero_iff] <;> omega
 
+@[simp]
+lemma add_eq_xor (a b : BitVec 1) : a.add b = a.xor b := by
+  have ha : a = 0 ∨ a = 1 := width_one_cases _
+  have hb : b = 0 ∨ b = 1 := width_one_cases _
+  rcases ha with h | h <;> (rcases hb with h' | h' <;> (simp [h, h']))
+
 lemma toNat_neq_of_neq_ofNat {a : BitVec w} {n : Nat} (h : a ≠ n#w) : a.toNat ≠ n := by
   intros haeq
   have hn : n < 2 ^ w := by