WORD_DP : conv -> conv -> conv
STRUCTURE
wordsLib
SYNOPSIS
Constructs a decision procedure for words.
DESCRIPTION
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
WORD_BIT_EQ_CONV, WORD_DECIDE
HOL  Trindemossen-1