1\DOC 2 3\TYPE {WORD_ARITH_EQ_ss : ssfrag} 4 5\SYNOPSIS 6 7Simplification fragment for words. 8 9\KEYWORDS 10 11simplification, words. 12 13\DESCRIBE 14 15The fragment {WORD_ARITH_EQ_ss} simplifies {``a = b : 'a word``} to 16{``a - b = 0w``}. It also simplifies using the theorems 17{WORD_LEFT_ADD_DISTRIB}, {WORD_RIGHT_ADD_DISTRIB}, {WORD_MUL_LSL} and 18{WORD_NOT}. When combined with {wordsLib.WORD_ARITH_ss} this fragment can be 19used to test for the arithmetic equality of words. 20 21\EXAMPLE 22 23{ 24- SIMP_CONV (pure_ss++WORD_ARITH_ss++WORD_ARITH_EQ_ss) [] ``3w * (a + b) = b + 3w * a`` 25<<HOL message: inventing new type variable names: 'a>> 26> val it = |- (3w * (a + b) = b + 3w * a) = (2w * b = 0w) : thm 27} 28 29\COMMENTS 30 31This fragment is not included in {WORDS_ss}. 32 33\SEEALSO 34 35wordsLib.WORD_ARITH_CONV, fcpLib.FCP_ss, wordsLib.BIT_ss, wordsLib.SIZES_ss, 36wordsLib.WORD_ARITH_ss, wordsLib.WORD_LOGIC_ss, wordsLib.WORD_SHIFT_ss, 37wordsLib.WORD_BIT_EQ_ss, wordsLib.WORD_EXTRACT_ss, wordsLib.WORD_MUL_LSL_ss, 38wordsLib.WORD_ss 39 40\ENDDOC 41