Theory: bword_bitop

Parents

• word_bitop

Types

Constants

• WAND  :bool word -> bool word -> bool word
• WNOT  :bool word -> bool word
• WXOR  :bool word -> bool word -> bool word
• WOR  :bool word -> bool word -> bool word

Definitions

WAND_DEF

|- !l1 l2. WORD l1 WAND WORD l2 = WORD (MAP2 $/\ l1 l2)

WNOT_DEF

|- !l. WNOT (WORD l) = WORD (MAP $~ l)

WOR_DEF

|- !l1 l2. WORD l1 WOR WORD l2 = WORD (MAP2 $\/ l1 l2)

WXOR_DEF

|- !l1 l2. WORD l1 WXOR WORD l2 = WORD (MAP2 (\x y. ~(x = y)) l1 l2)

Theorems

PBITBOP_WAND

|- PBITBOP $WAND

PBITBOP_WOR

|- PBITBOP $WOR

PBITBOP_WXOR

|- PBITBOP $WXOR

PBITOP_WNOT

|- PBITOP WNOT

WCAT_WNOT

|- !n1 n2 (w1::PWORDLEN n1) (w2::PWORDLEN n2).
     WCAT (WNOT w1,WNOT w2) = WNOT (WCAT (w1,w2))

WNOT_WNOT

|- !w. WNOT (WNOT w) = w