1\DOC 2 3\TYPE {WORD_ARITH_ss : ssfrag} 4 5\SYNOPSIS 6 7Simplification fragment for words. 8 9\KEYWORDS 10 11simplification, words. 12 13\DESCRIBE 14 15The fragment {WORD_ARITH_ss} does AC simplification for word multiplication, 16addition and subtraction. It also simplifies {INT_MINw}, {INT_MAXw} and 17{UINT_MAXw}. If the word length is known then further simplification may 18occur, in particular for {$- (n2w n)} and {w2n (n2w n)}. 19 20\EXAMPLE 21 22{ 23- SIMP_CONV (pure_ss++WORD_ARITH_ss) [] ``3w * b + a + 2w * b - a * 4w`` 24<<HOL message: inventing new type variable names: 'a>> 25> val it = |- 3w * b + a + 2w * b - a * 4w = $- 3w * a + 5w * b : thm 26 27- SIMP_CONV (pure_ss++WORD_ARITH_ss) [] ``INT_MINw + INT_MAXw + UINT_MAXw`` 28<<HOL message: inventing new type variable names: 'a>> 29> val it = |- INT_MINw + INT_MAXw + UINT_MAXw = $- 2w : thm 30} 31 32More simplification occurs when the word length is known. 33{ 34- SIMP_CONV (pure_ss++WORD_ARITH_ss) [] ``3w * b + a + 2w * b - a * 4w:word2`` 35> val it = |- 3w * b + a + 2w * b - a * 4w = a + b : thm 36 37- SIMP_CONV (pure_ss++WORD_ARITH_ss) [] ``w2n (33w:word4)``; 38> val it = |- w2n 33w = 1 : thm 39} 40 41\COMMENTS 42 43Any term of value {UINT_MAXw} simplifies to {$- 1w} even when the word length 44is known - this helps when simplifying bitwise operations. If the word length 45is not known then {INT_MAXw} becomes {INT_MINw + $- 1w}. 46 47\SEEALSO 48 49wordsLib.WORD_ARITH_CONV, wordsLib.WORD_CONV, fcpLib.FCP_ss, wordsLib.BIT_ss, 50wordsLib.SIZES_ss, wordsLib.WORD_LOGIC_ss, wordsLib.WORD_SHIFT_ss, 51wordsLib.WORD_ARITH_EQ_ss, wordsLib.WORD_BIT_EQ_ss, wordsLib.WORD_EXTRACT_ss, 52wordsLib.WORD_MUL_LSL_ss, wordsLib.WORD_ss 53 54\ENDDOC 55