WORD_BIT_EQ_ss

wordsLib.WORD_BIT_EQ_ss : ssfrag

Simplification fragment for words.

The fragment WORD_BIT_EQ_ss simplifies using fcpLib.FCP_ss and the definitions of “bitwise” operations, e.g., conjunction, disjunction, 1’s complement, shifts, concatenation and sub-word extraction. Can be used in combination with decision procedures to test for the bitwise equality of words.

Example

> SIMP_CONV (std_ss++wordsLib.WORD_BIT_EQ_ss) [] “a = b : 'a word”
val it = ⊢ a = b ⇔ ∀i. i < dimindex (:α) ⇒ (a ' i ⇔ b ' i): thm

Further simplification occurs when the word length is known.

> SIMP_CONV (std_ss++wordsLib.WORD_BIT_EQ_ss) [] “a = b : word2”
val it = ⊢ a = b ⇔ (a ' 1 ⇔ b ' 1) ∧ (a ' 0 ⇔ b ' 0): thm

Best used in combination with decision procedures.

> (SIMP_CONV (std_ss++wordsLib.WORD_BIT_EQ_ss) [] THENC tautLib.TAUT_CONV) “a && b && a = a && b”
val it = ⊢ a && b && a = a && b ⇔ T: thm

Comments

This fragment is not included in WORDS_ss.

See also

wordsLib.WORD_BIT_EQ_CONV, fcpLib.FCP_ss, blastLib.BBLAST_CONV, wordsLib.BIT_ss, wordsLib.SIZES_ss, wordsLib.WORD_ARITH_ss, wordsLib.WORD_LOGIC_ss, wordsLib.WORD_SHIFT_ss, wordsLib.WORD_ARITH_EQ_ss, wordsLib.WORD_EXTRACT_ss, wordsLib.WORD_MUL_LSL_ss, wordsLib.WORD_ss