1\DOC 2 3\TYPE {WORD_MUL_LSL_ss : ssfrag} 4 5\SYNOPSIS 6 7Simplification fragment for words. 8 9\KEYWORDS 10 11simplification, words. 12 13\DESCRIBE 14 15The fragment {WORD_MUL_LSL_ss} simplifies a multiplication by a word literal 16into a sum of left shifts. 17 18\EXAMPLE 19 20{ 21- SIMP_CONV (std_ss++WORD_MUL_LSL_ss) [] ``49w * a`` 22> val it = |- 49w * a = a << 5 + a << 4 + a : thm 23 24- SIMP_CONV (std_ss++WORD_ss++WORD_MUL_LSL_ss) [] ``2w * a + a << 1`` 25<<HOL message: inventing new type variable names: 'a>> 26> val it = |- 2w * a + a << 1 = a << 2 : thm 27} 28 29\COMMENTS 30 31This fragment is not included in {WORDS_ss}. It should not be used in 32combination with {WORD_ARITH_EQ_ss} or {wordsLib.WORD_ARITH_CONV}, since these 33convert left shifts into multiplications. 34 35\SEEALSO 36 37wordsLib.WORD_MUL_LSL_CONV, fcpLib.FCP_ss, wordsLib.BIT_ss, wordsLib.SIZES_ss, 38wordsLib.WORD_ARITH_ss, wordsLib.WORD_LOGIC_ss, wordsLib.WORD_ARITH_EQ_ss, 39wordsLib.WORD_BIT_EQ_ss, wordsLib.WORD_SHIFT_ss, wordsLib.WORD_EXTRACT_ss, 40wordsLib.WORD_ss 41 42\ENDDOC 43