----------------------------------------------------------------------
WORD_ss                                                     (wordsLib)
----------------------------------------------------------------------
WORD_ss : ssfrag

SYNOPSIS
Simplification fragment for words.

KEYWORDS
simplification, words.

DESCRIBE
The fragment {WORD_ss} contains {BIT_ss}, {SIZES_ss}, {WORD_LOGIC_ss},
{WORD_ARITH_ss} and {WORD_SHIFT_ss}.  It also performs ground term evaluation.

EXAMPLE

- SIMP_CONV (pure_ss++WORD_ss) [] ``BIT i 42``
> val it = |- BIT i 42 = i IN {1; 3; 5} : thm

- SIMP_CONV (pure_ss++WORD_ss) [] ``dimword(:42)``
> val it = |- dimword (:42) = 4398046511104 : thm

- SIMP_CONV (pure_ss++WORD_ss) [] ``((a #<< 2 #>> 2 + a) && $- 1w) - a``
<<HOL message: inventing new type variable names: 'a>>
> val it = |- (a #<< 2 #>> 2 + a && $- 1w) - a = a : thm

- SIMP_CONV (pure_ss++WORD_ss) [] ``(4 -- 2) ($- 1w : word8)``
> val it = |- (4 -- 2) ($- 1w) = 7w : thm


COMMENTS
The {WORD_ss} fragment does not include {WORD_ARITH_EQ_ss}, {WORD_BIT_EQ_ss},
{WORD_EXTRACT_ss} or {WORD_MUL_LSL_ss}.  These extra fragments have more
specialised applications.

SEEALSO
wordsLib.WORD_CONV, 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_EXTRACT_ss,
wordsLib.WORD_MUL_LSL_ss.

----------------------------------------------------------------------