llvm: BitVec.xor_neg_one will enable ring_nf to be more powerful

[tobiasgrosser]

The pattern a ^^^ (-1#w) = (-1#w) - a arises several times in AliveStatements. Proofing it will in certain cases enable ring to close goals, but it also breaks certain extensionality proofs. We may want to use it carefully (meaning, only after the ext proof in alive_auto has been executed).

This should resolve four theorems.

[bollu]

Right. This is the type of thing that wants us to write an ad-hoc proof procedure, which tries multiple styles of proof, since there’s no good “normal form” for all cases we want to cover.

[tobiasgrosser]

This lemma appears in theorem bitvec_AddSub_1560 and might be a good next one for @eurquhart1.

[emmau678]

Hi, I was just checking through and I see this was assigned to me and looks like it remains open (if so, I can try to complete it if it would still be useful?)