WORD_ARITH_ss : ssfrag
STRUCTURE
SYNOPSIS
Simplification fragment for words.
DESCRIPTION
The fragment WORD_ARITH_ss does AC simplification for word multiplication, addition and subtraction. It also simplifies INT_MINw, INT_MAXw and UINT_MAXw. If the word length is known then further simplification may occur, in particular for $- (n2w n) and w2n (n2w n).
EXAMPLE
- SIMP_CONV (pure_ss++WORD_ARITH_ss) [] ``3w * b + a + 2w * b - a * 4w``
<<HOL message: inventing new type variable names: 'a>>
> val it = |- 3w * b + a + 2w * b - a * 4w = $- 3w * a + 5w * b : thm

- SIMP_CONV (pure_ss++WORD_ARITH_ss) [] ``INT_MINw + INT_MAXw + UINT_MAXw``
<<HOL message: inventing new type variable names: 'a>>
> val it = |- INT_MINw + INT_MAXw + UINT_MAXw = $- 2w : thm

More simplification occurs when the word length is known.

- SIMP_CONV (pure_ss++WORD_ARITH_ss) [] ``3w * b + a + 2w * b - a * 4w:word2``
> val it = |- 3w * b + a + 2w * b - a * 4w = a + b : thm

- SIMP_CONV (pure_ss++WORD_ARITH_ss) [] ``w2n (33w:word4)``;
> val it = |- w2n 33w = 1 : thm
COMMENTS
Any term of value UINT_MAXw simplifies to $- 1w even when the word length is known - this helps when simplifying bitwise operations. If the word length is not known then INT_MAXw becomes INT_MINw + $- 1w.
SEEALSO
HOL  Kananaskis-14