feat: add ac_nf and test [ac_nf|ac_rfl] for BitVec

[tobiasgrosser]

ac_nf is a counterpart to ac_rfl, which normalizes bitvector expressions with respect to associativity and commutativity.

While there, also add test coverage for ac_rfl and ac_nf for BitVec, complementing the existing test coverage.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 4cd4bcc9be195f0b0a6a6a9e47522a41e044eabc --onto 9460f79d28d3a72d7484766b5f2c83362e91dd5b. (2024-09-29 20:44:37)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 4cd4bcc9be195f0b0a6a6a9e47522a41e044eabc --onto 994cfa4c74a066df050ca889da912e71fa70cd85. (2024-09-30 04:47:42)

[kim-em]

Would you mind adding a small number of tests, just to exercise that it works for one or two other types besides BitVec? Int would be fine.

[tobiasgrosser]

Would you mind adding a small number of tests, just to exercise that it works for one or two other types besides BitVec? Int would be fine.

When searching for ac_rfl uses, I missed to add the test folder to my search path. There are indeed test cases already available. I now moved the BitVec test cases in the existing test file. This is now ready to go from my side.