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.

See also

wordsLib.WORD_SUB_ss