1\DOC 2 3\TYPE {SIZES_ss : ssfrag} 4 5\SYNOPSIS 6 7Simplification fragment for words. 8 9\KEYWORDS 10 11simplification, words. 12 13\DESCRIBE 14 15The fragment {SIZES_ss} evaluates terms {``dimindex(:'a)``}, {``dimword(:'a)``}, 16{``INT_MIN(:'a)``}, and {``FINITE (UNIV : 'a set)``} for numeric types. 17 18\EXAMPLE 19{ 20- SIMP_CONV (pure_ss++SIZES_ss) [] ``dimindex(:32) + INT_MIN(:32) + dimword(:32)`` 21> val it = 22 |- dimindex (:32) + INT_MIN (:32) + dimword (:32) = 23 32 + 2147483648 + 4294967296 : thm 24} 25 26\SEEALSO 27 28wordsLib.SIZES_CONV, wordsLib.WORD_CONV, fcpLib.FCP_ss, wordsLib.BIT_ss, 29wordsLib.WORD_ARITH_ss, wordsLib.WORD_LOGIC_ss, wordsLib.WORD_SHIFT_ss, 30wordsLib.WORD_ARITH_EQ_ss, wordsLib.WORD_BIT_EQ_ss, wordsLib.WORD_EXTRACT_ss, 31wordsLib.WORD_MUL_LSL_ss, wordsLib.WORD_ss 32 33\ENDDOC 34