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