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