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