WORD_EXTRACT_ss

wordsLib.WORD_EXTRACT_ss : ssfrag

Simplification fragment for words.

The fragment WORD_EXTRACT_ss simplifies the operations w2w, sw2sw (signed word-to-word conversion), word_lsb, word_msb, word_bit, >> (arithmetic right shift), >>> (logical right shift), #>> (rotate right), #<< (rotate left), @@ (concatenation), -- (word bits) and '' (word slice). The result is expressed in terms of !! (disjunction), << (left shift) and >< (word extract).

Example

> SIMP_CONV (std_ss++wordsLib.WORD_ss++wordsLib.WORD_EXTRACT_ss) [] “(((7 >< 5) (a:word8)):3 word @@ ((4 >< 0) a):5 word) : word8”
val it = ⊢ (7 >< 5) a @@ (4 >< 0) a = a: thm

> SIMP_CONV (std_ss++wordsLib.WORD_ss++wordsLib.WORD_EXTRACT_ss) [] “(4 -- 2) ((a:word8) #>> 4)”
val it = ⊢ (4 -- 2) (a ⇄ 4) = (0 >< 0) a ≪ 2 ‖ (7 >< 6) a: thm

> SIMP_CONV (std_ss++wordsLib.WORD_ss++wordsLib.WORD_EXTRACT_ss) [] “w2w (sw2sw (a:word4):word8):word4”
val it = ⊢ w2w (sw2sw a) = a: thm

Comments

Best used in combination with WORD_ss.

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_SHIFT_ss, wordsLib.WORD_MUL_LSL_ss, wordsLib.WORD_ss