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