WORD_DECIDE

wordsLib.WORD_DECIDE : conv

A decision procedure for words.

The conversion WORD_DECIDE is the same as WORD_DP WORD_CONV bossLib.DECIDE.

Example

> wordsLib.WORD_DECIDE “a && (b !! a) = a !! a && b”
val it = ⊢ a && (b ‖ a) = a ‖ a && b: thm

> wordsLib.WORD_DECIDE “a + 2w <+ 4w = a <+ 2w \/ 13w <+ a :word4”
Exception- Don't expect to find a = in this position after a <+
at line 1, character 37 and on line 1, characters 31-32.
HOL_ERR
  (at Absyn.Absyn: on line 1, characters 31-32:
       Don't expect to find a = in this position after a <+
at line 1, character 37 and on line 1, characters 31-32.
) raised

> wordsLib.WORD_DECIDE “a < 0w = 1w <+ a : word2”
Exception- Don't expect to find a = in this position after a <
at line 1, character 31 and at line 1, character 26.
HOL_ERR
  (at Absyn.Absyn: at line 1, character 26:
       Don't expect to find a = in this position after a <
at line 1, character 31 and at line 1, character 26.
) raised

> wordsLib.WORD_DECIDE “(?w:word4. 14w <+ w) /\ ~(?w:word4. 15w <+ w)”
val it = ⊢ (∃w. 14w <₊ w) ∧ ¬∃w. 15w <₊ w: thm

See also

wordsLib.WORD_DP