WORD_ARITH_ss

wordsLib.WORD_ARITH_ss : ssfrag

Simplification fragment for words.

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++wordsLib.WORD_ARITH_ss) [] “3w * b + a + 2w * b - a * 4w”
val it = ⊢ 3w * b + a + 2w * b − a * 4w = -3w * a + 5w * b: thm

> SIMP_CONV (pure_ss++wordsLib.WORD_ARITH_ss) [] “INT_MINw + INT_MAXw + UINT_MAXw”
val it = ⊢ INT_MINw + INT_MAXw + UINT_MAXw = -2w: thm

More simplification occurs when the word length is known.

> SIMP_CONV (pure_ss++wordsLib.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++wordsLib.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.

See also

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