1\DOC
2
3\TYPE {WORD_SUB_CONV : conv}
4
5\DESCRIBE
6
7The conversion {WORD_SUB_CONV} is designed to eliminate occurrences of
8multiplication by a negative coefficient, introducing unary-minus (2's
9complement) and subtraction wherever possible.
10
11\EXAMPLE
12{
13> wordsLib.WORD_SUB_CONV ``a + -3w * b + -1w * c = -1w * d + e: 'a word``;
14val it =
15   |- (a + -3w * b + -1w * c = -1w * d + e) <=> (a - 3w * b - c = e - d):
16   thm
17
18> wordsLib.WORD_SUB_CONV ``-1w * a: 'a word``;
19val it = |- -1w * a = -a: thm
20
21wordsLib.WORD_SUB_CONV ``-1w * a + -2w * b: 'a word``;
22val it =
23   |- -1w * a + -2w * b = -(2w * b + a):
24   thm
25}
26
27\COMMENTS
28
29This conversion forms the basis of {wordsLib.WORD_SUB_ss}. Care should be taken
30when using this conversion in combination with other bit-vector tools. For
31example, {wordsLib.WORD_ARITH_CONV} will undo all of the work of
32{WORD_SUB_CONV}.
33
34\SEEALSO
35
36wordsLib.WORD_SUB_ss
37
38\ENDDOC
39