WORD_BIT_EQ_ss : ssfrag

- STRUCTURE
- SYNOPSIS
- Simplification fragment for words.
- DESCRIPTION
- 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
- Further simplification occurs when the word length is known.
- SIMP_CONV (std_ss++WORD_BIT_EQ_ss) [] ``a = b : 'a word`` > val it = |- (a = b) = !i. i < dimindex (:'a) ==> (a ' i = b ' i) : thm

Best used in combination with decision procedures.- SIMP_CONV (std_ss++WORD_BIT_EQ_ss) [] ``a = b : word2`` > val it = |- (a = b) = (a ' 1 = b ' 1) /\ (a ' 0 = b ' 0) : thm

- (SIMP_CONV (std_ss++WORD_BIT_EQ_ss) [] THENC tautLib.TAUT_CONV) ``a && b && a = a && b`` <<HOL message: inventing new type variable names: 'a>> > val it = |- (a && b && a = a && b) = T : thm

- COMMENTS
- This fragment is not included in WORDS_ss.
- SEEALSO

HOL Kananaskis-14