\DOC

\TYPE {WORD_LOGIC_ss : ssfrag}

\SYNOPSIS

Simplification fragment for words.

\KEYWORDS

simplification, words.

\DESCRIBE

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

wordsLib.WORD_LOGIC_CONV, wordsLib.WORD_CONV, fcpLib.FCP_ss, wordsLib.BIT_ss,
wordsLib.SIZES_ss, wordsLib.WORD_ARITH_ss, wordsLib.WORD_SHIFT_ss,
wordsLib.WORD_ARITH_EQ_ss, wordsLib.WORD_BIT_EQ_ss, wordsLib.WORD_EXTRACT_ss,
wordsLib.WORD_MUL_LSL_ss, wordsLib.WORD_ss

\ENDDOC