WORD_LOGIC_ss : ssfrag
STRUCTURE
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
HOL  Kananaskis-14