WORD_LOGIC_ss : ssfrag
STRUCTURE
wordsLib
SYNOPSIS
Simplification fragment for words.
DESCRIPTION
The fragment WORD_LOGIC_ss does AC simplification for word conjunction, disjunction and 1’s complement (negation). If the word length is known then further simplification occurs, in particular for ~(n2w n).
EXAMPLE
- SIMP_CONV (pure_ss++WORD_LOGIC_ss) [] ``3w !! 12w && a !! ~4w !! a && 16w``
<<HOL message: inventing new type variable names: 'a>>
> val it = |- 3w !! 12w && a !! ~4w !! a && 16w = 28w && a !! $- 5w : thm

More simplification occurs when the word length is known. 

- SIMP_CONV (pure_ss++WORD_LOGIC_ss) [] ``~12w !! ~14w : word8``
> val it = |- ~12w !! ~14w = 243w : thm
COMMENTS
The term $- 1w represents UINT_MAXw, which is the supremum in bitwise operations.
SEEALSO
WORD_LOGIC_CONV, WORD_CONV, FCP_ss, BIT_ss, SIZES_ss, WORD_ARITH_ss, WORD_SHIFT_ss, WORD_ARITH_EQ_ss, WORD_BIT_EQ_ss, WORD_EXTRACT_ss, WORD_MUL_LSL_ss, WORD_ss
HOL  Kananaskis-14