WORD_ARITH_CONV

wordsLib.WORD_ARITH_CONV : conv

Conversion based on WORD_ARITH_ss and WORD_ARITH_EQ_ss.

The conversion WORD_ARITH_CONV converts word arithmetic expressions into a canonical form.

Example

WORD_ARITH_CONV fixes the sign of equalities.

> SIMP_CONV (std_ss++wordsLib.WORD_ARITH_ss++wordsLib.WORD_ARITH_EQ_ss) [] “$- a = b : 'a word”
Exception- HOL_ERR
  (at Preterm.type-analysis: at line 1, character 83:
       
Type error in function application.
  Function: $= ($- a) :(α word -> α word) -> bool
  Argument: b :α word
  Reason: Attempt to unify different type operators: min$fun and fcp$cart
) raised

> wordsLib.WORD_ARITH_CONV “$- a = b : 'a word”
Exception- HOL_ERR
  (at Preterm.type-analysis: at line 1, character 35:
       
Type error in function application.
  Function: $= ($- a) :(α word -> α word) -> bool
  Argument: b :α word
  Reason: Attempt to unify different type operators: min$fun and fcp$cart
) raised

Comments

The fragment WORD_ARITH_EQ_ss and conversion WORD_CONV do not adjust the sign of equalities.

See also

wordsLib.WORD_ARITH_ss, wordsLib.WORD_ARITH_EQ_ss, wordsLib.WORD_LOGIC_CONV, wordsLib.WORD_MUL_LSL_CONV, wordsLib.WORD_CONV, wordsLib.WORD_BIT_EQ_CONV, wordsLib.WORD_EVAL_CONV