1\DOC 2 3\TYPE {WORD_ARITH_CONV : conv} 4 5\SYNOPSIS 6 7Conversion based on {WORD_ARITH_ss} and {WORD_ARITH_EQ_ss}. 8 9\DESCRIBE 10 11The conversion {WORD_ARITH_CONV} converts word arithmetic expressions into a 12canonical form. 13 14\EXAMPLE 15{WORD_ARITH_CONV} fixes the sign of equalities. 16{ 17- SIMP_CONV (std_ss++WORD_ARITH_ss++WORD_ARITH_EQ_ss) [] ``$- a = b : 'a word`` 18> val it = |- ($- a = b) = ($- 1w * a + $- 1w * b = 0w) : thm 19 20- WORD_ARITH_CONV ``$- a = b : 'a word`` 21> val it = |- ($- a = b) = (a + b = 0w) : thm 22} 23 24\COMMENTS 25 26The fragment {WORD_ARITH_EQ_ss} and conversion {WORD_CONV} do not adjust the 27sign of equalities. 28 29\SEEALSO 30 31wordsLib.WORD_ARITH_ss, wordsLib.WORD_ARITH_EQ_ss, wordsLib.WORD_LOGIC_CONV, 32wordsLib.WORD_MUL_LSL_CONV, wordsLib.WORD_CONV, wordsLib.WORD_BIT_EQ_CONV, 33wordsLib.WORD_EVAL_CONV 34 35\ENDDOC 36