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.

See also

wordsLib.WORD_BIT_EQ_CONV, wordsLib.WORD_DECIDE