WORD_ss : ssfrag
STRUCTURE
wordsLib
SYNOPSIS
Simplification fragment for words.
DESCRIPTION
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
WORD_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_MUL_LSL_ss
HOL  Kananaskis-14