1\DOC
2
3\TYPE {WORD_LOGIC_ss : ssfrag}
4
5\SYNOPSIS
6
7Simplification fragment for words.
8
9\KEYWORDS
10
11simplification, words.
12
13\DESCRIBE
14
15The fragment {WORD_LOGIC_ss} does AC simplification for word conjunction,
16disjunction and 1's complement (negation).  If the word length is known then
17further simplification occurs, in particular for {~(n2w n)}.
18
19\EXAMPLE
20
21{
22- SIMP_CONV (pure_ss++WORD_LOGIC_ss) [] ``3w !! 12w && a !! ~4w !! a && 16w``
23<<HOL message: inventing new type variable names: 'a>>
24> val it = |- 3w !! 12w && a !! ~4w !! a && 16w = 28w && a !! $- 5w : thm
25}
26
27More simplification occurs when the word length is known.
28{
29- SIMP_CONV (pure_ss++WORD_LOGIC_ss) [] ``~12w !! ~14w : word8``
30> val it = |- ~12w !! ~14w = 243w : thm
31}
32
33\COMMENTS
34
35The term {$- 1w} represents {UINT_MAXw}, which is the supremum in bitwise
36operations.
37
38\SEEALSO
39
40wordsLib.WORD_LOGIC_CONV, wordsLib.WORD_CONV, fcpLib.FCP_ss, wordsLib.BIT_ss,
41wordsLib.SIZES_ss, wordsLib.WORD_ARITH_ss, wordsLib.WORD_SHIFT_ss,
42wordsLib.WORD_ARITH_EQ_ss, wordsLib.WORD_BIT_EQ_ss, wordsLib.WORD_EXTRACT_ss,
43wordsLib.WORD_MUL_LSL_ss, wordsLib.WORD_ss
44
45\ENDDOC
46