----------------------------------------------------------------------
WORD_DP                                                     (wordsLib)
----------------------------------------------------------------------
WORD_DP : conv -> conv -> conv

SYNOPSIS
Constructs a decision procedure for words.

DESCRIBE
The conversion {WORD_DP conv dp} is a decision procedure for words that makes
use of the supplied conversion {conv} and decision procedure {dp}.  Suitable
decision procedures include {tautLib.TAUT_PROVE}, {bossLib.DECIDE},
{intLib.ARITH_PROVE} and {intLib.COOPER_PROVE}.  The procedure will first apply
{conv} and then {WORD_BIT_EQ_CONV}.  If this is not sufficient then an attempt
is made to solve the problem by applying an arithmetic decision procedure {dp},
e.g. {``(a = 0w) \/ (a = 1w :1 word)``} is mapped to the goal
{``w2n a < 2 ==> (w2n a = 0) \/ (w2n a = 1)``}.

FAILURE
The invocation will fail when the decision procedure {dp} fails.

EXAMPLE

- wordsLib.WORD_DP ALL_CONV tautLib.TAUT_PROVE ``a && b && a = a && b``
<<HOL message: inventing new type variable names: 'a>>
> val it = |- a && b && a = a && b : thm

- wordsLib.WORD_DP ALL_CONV DECIDE ``a < b /\ b < c ==> a < c : 'a word``
> val it = |- a < b /\ b < c ==> a < c : thm

- wordsLib.WORD_DP ALL_CONV intLib.ARITH_PROVE ``a <+ 3w:word16 ==> (a = 0w) \/ (a = 1w) \/ (a = 2w)``
> val it = |- a <+ 3w ==> (a = 0w) \/ (a = 1w) \/ (a = 2w) : thm


COMMENTS
On large problems {intLib.ARITH_PROVE} will perform much better than
{bossLib.DECIDE}.

SEEALSO
wordsLib.WORD_BIT_EQ_CONV, wordsLib.WORD_DECIDE.

----------------------------------------------------------------------