WORD_DP : conv -> conv -> conv

- STRUCTURE
- 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

HOL Kananaskis-14