WORD_SHIFT_ss

wordsLib.WORD_SHIFT_ss : ssfrag

Simplification fragment for words.

The fragment WORD_SHIFT_ss does some basic simplifications for the operations: << (left shift), >> (arithmetic right shift), >>> (logical right shift), #>> (rotate right) and #<< (rotate left). More simplification is possible when used in combination with wordsLib.SIZES_ss.

Example

> SIMP_CONV (std_ss++wordsLib.WORD_SHIFT_ss) [] “a << 2 << 3 + a >> 3 >> 2 + a >>> 1 >>> 2 + a #<< 1 #<< 2”
val it =
   ⊢ a ≪ 2 ≪ 3 + a ≫ 3 ≫ 2 + a ⋙ 1 ⋙ 2 + a ⇆ 1 ⇆ 2 =
     a ≪ 5 + a ≫ 5 + a ⋙ 3 + a ⇆ 3: thm

> SIMP_CONV (std_ss++wordsLib.WORD_SHIFT_ss) [] “a >> 0 + 0w << n + a #<< 2 #>> 2”
val it = ⊢ a ≫ 0 + 0w ≪ n + a ⇆ 2 ⇄ 2 = a + 0w + a: thm

More simplification is possible when the word length is known.

> SIMP_CONV (std_ss++wordsLib.SIZES_ss++wordsLib.WORD_SHIFT_ss) [] “a << 4 + (a #<< 6) : word4”
val it = ⊢ a ≪ 4 + a ⇆ 6 = 0w + a ⇆ 2: thm

Comments

When the word length is known the fragment WORD_ss simplifies #<< to #>>.

See also

fcpLib.FCP_ss, wordsLib.BIT_ss, wordsLib.SIZES_ss, wordsLib.WORD_ARITH_ss, wordsLib.WORD_LOGIC_ss, wordsLib.WORD_ARITH_EQ_ss, wordsLib.WORD_BIT_EQ_ss, wordsLib.WORD_EXTRACT_ss, wordsLib.WORD_MUL_LSL_ss, wordsLib.WORD_ss