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