WORD_LOGIC_ss

wordsLib.WORD_LOGIC_ss : ssfrag

Simplification fragment for words.

The fragment WORD_LOGIC_ss does AC simplification for word conjunction, disjunction and 1’s complement (negation). If the word length is known then further simplification occurs, in particular for ~(n2w n).

Example

> SIMP_CONV (pure_ss++wordsLib.WORD_LOGIC_ss) [] “3w !! 12w && a !! ~4w !! a && 16w”
val it = ⊢ 3w ‖ 12w && a ‖ ¬4w ‖ a && 16w = 28w && a ‖ -5w: thm

More simplification occurs when the word length is known.

> SIMP_CONV (pure_ss++wordsLib.WORD_LOGIC_ss) [] “~12w !! ~14w : word8”
val it = ⊢ ¬12w ‖ ¬14w = 243w: thm

Comments

The term $- 1w represents UINT_MAXw, which is the supremum in bitwise operations.

See also

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