WORD_DP
wordsLib.WORD_DP : conv -> conv -> conv
Constructs a decision procedure for words.
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”
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.