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