WORD_SUB_CONV
wordsLib.WORD_SUB_CONV : conv
The conversion WORD_SUB_CONV is designed to eliminate occurrences of
multiplication by a negative coefficient, introducing unary-minus (2's
complement) and subtraction wherever possible.
Example
> wordsLib.WORD_SUB_CONV “a + -3w * b + -1w * c = -1w * d + e: 'a word”;
val it = ⊢ a + -3w * b + -1w * c = -1w * d + e ⇔ a − 3w * b − c = e − d: thm
> wordsLib.WORD_SUB_CONV “-1w * a: 'a word”;
val it = ⊢ -1w * a = -a: thm
Comments
This conversion forms the basis of wordsLib.WORD_SUB_ss. Care should
be taken when using this conversion in combination with other bit-vector
tools. For example, wordsLib.WORD_ARITH_CONV will undo all of the work
of WORD_SUB_CONV.