1\DOC 2 3\TYPE {WORD_SHIFT_ss : ssfrag} 4 5\SYNOPSIS 6 7Simplification fragment for words. 8 9\KEYWORDS 10 11simplification, words. 12 13\DESCRIBE 14 15The fragment {WORD_SHIFT_ss} does some basic simplifications for the 16operations: {<<} (left shift), {>>} (arithmetic right shift), {>>>} (logical 17right shift), {#>>} (rotate right) and {#<<} (rotate left). More 18simplification is possible when used in combination with {wordsLib.SIZES_ss}. 19 20\EXAMPLE 21 22{ 23- SIMP_CONV (std_ss++WORD_SHIFT_ss) [] ``a << 2 << 3 + a >> 3 >> 2 + a >>> 1 >>> 2 + a #<< 1 #<< 2`` 24<<HOL message: inventing new type variable names: 'a>> 25> val it = 26 |- a << 2 << 3 + a >> 3 >> 2 + a >>> 1 >>> 2 + a #<< 1 #<< 2 = 27 a << 5 + a >> 5 + a >>> 3 + a #<< 3 : thm 28 29- SIMP_CONV (std_ss++WORD_SHIFT_ss) [] ``a >> 0 + 0w << n + a #<< 2 #>> 2`` 30<<HOL message: inventing new type variable names: 'a>> 31> val it = |- a >> 0 + 0w << n + a #<< 2 #>> 2 = a + 0w + a : thm 32} 33 34More simplification is possible when the word length is known. 35{ 36- SIMP_CONV (std_ss++SIZES_ss++WORD_SHIFT_ss) [] ``a << 4 + (a #<< 6) : word4`` 37> val it = |- a << 4 = 0w + a #<< 2 : thm 38} 39 40\COMMENTS 41 42When the word length is known the fragment {WORD_ss} simplifies {#<<} to {#>>}. 43 44\SEEALSO 45 46fcpLib.FCP_ss, wordsLib.BIT_ss, wordsLib.SIZES_ss, wordsLib.WORD_ARITH_ss, 47wordsLib.WORD_LOGIC_ss, wordsLib.WORD_ARITH_EQ_ss, wordsLib.WORD_BIT_EQ_ss, 48wordsLib.WORD_EXTRACT_ss, wordsLib.WORD_MUL_LSL_ss, wordsLib.WORD_ss 49 50\ENDDOC 51