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