WORD_SUB_CONV : conv
STRUCTURE
wordsLib
DESCRIPTION
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

wordsLib.WORD_SUB_CONV ``-1w * a + -2w * b: 'a word``;
val it =
   |- -1w * a + -2w * b = -(2w * b + 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.
SEEALSO
WORD_SUB_ss
HOL  Kananaskis-14