Add bm_check_disjointness

[aqjune]

Given a bitmatch term tm, bm_check_disjointness tm checks whether there exist two bit patterns that overlap. Two bit patterns overlap if there exists at least one bitvector that can be matched to both of them. If there exists such overlapping patterns, bm_check_disjointness throws Invalid_argument. This function is useful when you want to ensure that the bitmatch can be successfully handled by BITMATCH_CONV.

At the end of the file, I added a few unit tests that ensure bm_check_disjointness works as anticipated. If it does not work as expected, it raises a failure, halting loading this library. I wonder whether leaving tests in the file is consistent with HOL Light's style though, so the unit test part is rather an additional change. I am okay with dropping it if unnecessary.

[aqjune]

Updated the message and rebased to the latest master branch

[jrh13]

Thanks, this is a convenient tool.