The fragment WORD_ARITH_EQ_ss simplifies ``a = b : 'a word`` to
``a - b = 0w``. It also simplifies using the theorems
WORD_LEFT_ADD_DISTRIB, WORD_RIGHT_ADD_DISTRIB, WORD_MUL_LSL and
WORD_NOT. When combined with wordsLib.WORD_ARITH_ss this fragment can be
used to test for the arithmetic equality of words.
EXAMPLE
- SIMP_CONV (pure_ss++WORD_ARITH_ss++WORD_ARITH_EQ_ss) [] ``3w * (a + b) = b + 3w * a``
<<HOL message: inventing new type variable names: 'a>>
> val it = |- (3w * (a + b) = b + 3w * a) = (2w * b = 0w) : thm