WORD_MUL_LSL_ss : ssfrag
STRUCTURE
wordsLib
SYNOPSIS
Simplification fragment for words.
DESCRIPTION
The fragment WORD_MUL_LSL_ss simplifies a multiplication by a word literal into a sum of left shifts.
EXAMPLE
- SIMP_CONV (std_ss++WORD_MUL_LSL_ss) [] ``49w * a``
> val it = |- 49w * a = a << 5 + a << 4 + a : thm

- SIMP_CONV (std_ss++WORD_ss++WORD_MUL_LSL_ss) [] ``2w * a + a << 1``
<<HOL message: inventing new type variable names: 'a>>
> val it = |- 2w * a + a << 1 = a << 2 : thm
COMMENTS
This fragment is not included in WORDS_ss. It should not be used in combination with WORD_ARITH_EQ_ss or wordsLib.WORD_ARITH_CONV, since these convert left shifts into multiplications.
SEEALSO
WORD_MUL_LSL_CONV, FCP_ss, BIT_ss, SIZES_ss, WORD_ARITH_ss, WORD_LOGIC_ss, WORD_ARITH_EQ_ss, WORD_BIT_EQ_ss, WORD_SHIFT_ss, WORD_EXTRACT_ss, WORD_ss
HOL  Kananaskis-14