WORD_ss

wordsLib.WORD_ss : ssfrag

Simplification fragment for words.

The fragment WORD_ss contains BIT_ss, SIZES_ss, WORD_LOGIC_ss, WORD_ARITH_ss and WORD_SHIFT_ss. It also performs ground term evaluation.

Example

> SIMP_CONV (pure_ss++wordsLib.WORD_ss) [] “BIT i 42”
val it = ⊢ BIT i 42 ⇔ i ∈ {1; 3; 5}: thm

> SIMP_CONV (pure_ss++wordsLib.WORD_ss) [] “dimword(:42)”
val it = ⊢ dimword (:42) = 4398046511104: thm

> SIMP_CONV (pure_ss++wordsLib.WORD_ss) [] “((a #<< 2 #>> 2 + a) && $- 1w) - a”
Exception- HOL_ERR
  (at Preterm.type-analysis: on line 1, characters 69-72:
       
Type error in function application.
  Function: $&& (a ⇆ 2 ⇄ 2 + a) :α word -> α word
  Argument: $- 1w :α word -> α word
  Reason: Attempt to unify different type operators: fcp$cart and min$fun
) raised

> SIMP_CONV (pure_ss++wordsLib.WORD_ss) [] “(4 -- 2) ($- 1w : word8)”
Exception- HOL_ERR
  (at Preterm.type-analysis: on line 1, characters 55-58:
       
Type constraint failure: 
  Term: $- 1w :α word -> α word
  Constraint: :word8
) raised

Comments

The WORD_ss fragment does not include WORD_ARITH_EQ_ss, WORD_BIT_EQ_ss, WORD_EXTRACT_ss or WORD_MUL_LSL_ss. These extra fragments have more specialised applications.

See also

wordsLib.WORD_CONV, fcpLib.FCP_ss, wordsLib.BIT_ss, wordsLib.SIZES_ss, wordsLib.WORD_ARITH_ss, wordsLib.WORD_LOGIC_ss, wordsLib.WORD_ARITH_EQ_ss, wordsLib.WORD_BIT_EQ_ss, wordsLib.WORD_SHIFT_ss, wordsLib.WORD_EXTRACT_ss, wordsLib.WORD_MUL_LSL_ss