wordsLib.WORD_ARITH

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

WORD_ARITH_CONV, WORD_CONV, FCP_ss, BIT_ss, SIZES_ss, WORD_LOGIC_ss, WORD_SHIFT_ss, WORD_ARITH_EQ_ss, WORD_BIT_EQ_ss, WORD_EXTRACT_ss, WORD_MUL_LSL_ss, WORD_ss