Theory: bword_num

Parents

• word_num
• word_bitop

Types

Constants

• NBWORD  :num -> num -> bool word
• BV  :bool -> num
• VB  :num -> bool
• BNVAL  :bool word -> num

Definitions

BNVAL_DEF

|- !l. BNVAL (WORD l) = LVAL BV 2 l

BV_DEF

|- !b. BV b = (if b then SUC 0 else 0)

NBWORD_DEF

|- !n m. NBWORD n m = WORD (NLIST n VB 2 m)

VB_DEF

|- !n. VB n = ~(n MOD 2 = 0)

Theorems

ADD_BNVAL_LEFT

|- !n (w1::PWORDLEN (SUC n)) (w2::PWORDLEN (SUC n)).
     BNVAL w1 + BNVAL w2 =
     (BV (BIT n w1) + BV (BIT n w2)) * 2 ** n +
     (BNVAL (WSEG n 0 w1) + BNVAL (WSEG n 0 w2))

ADD_BNVAL_RIGHT

|- !n (w1::PWORDLEN (SUC n)) (w2::PWORDLEN (SUC n)).
     BNVAL w1 + BNVAL w2 =
     (BNVAL (WSEG n 1 w1) + BNVAL (WSEG n 1 w2)) * 2 +
     (BV (BIT 0 w1) + BV (BIT 0 w2))

ADD_BNVAL_SPLIT

|- !n1 n2 (w1::PWORDLEN (n1 + n2)) (w2::PWORDLEN (n1 + n2)).
     BNVAL w1 + BNVAL w2 =
     (BNVAL (WSEG n1 n2 w1) + BNVAL (WSEG n1 n2 w2)) * 2 ** n2 +
     (BNVAL (WSEG n2 0 w1) + BNVAL (WSEG n2 0 w2))

BIT_NBWORD0

|- !k n. k < n ==> (BIT k (NBWORD n 0) = F)

BNVAL0

|- BNVAL (WORD []) = 0

BNVAL_11

|- !w1 w2. (WORDLEN w1 = WORDLEN w2) ==> (BNVAL w1 = BNVAL w2) ==> (w1 = w2)

BNVAL_MAX

|- !n (w::PWORDLEN n). BNVAL w < 2 ** n

BNVAL_NBWORD

|- !n m. m < 2 ** n ==> (BNVAL (NBWORD n m) = m)

BNVAL_NVAL

|- !w. BNVAL w = NVAL BV 2 w

BNVAL_ONTO

|- !w. ?n. BNVAL w = n

BNVAL_WCAT

|- !n m (w1::PWORDLEN n) (w2::PWORDLEN m).
     BNVAL (WCAT (w1,w2)) = BNVAL w1 * 2 ** m + BNVAL w2

BNVAL_WCAT1

|- !n (w::PWORDLEN n) x. BNVAL (WCAT (w,WORD [x])) = BNVAL w * 2 + BV x

BNVAL_WCAT2

|- !n (w::PWORDLEN n) x. BNVAL (WCAT (WORD [x],w)) = BV x * 2 ** n + BNVAL w

BV_LESS_2

|- !x. BV x < 2

BV_VB

|- !x. x < 2 ==> (BV (VB x) = x)

DOUBL_EQ_SHL

|- !n.
     0 < n ==>
     !(w::PWORDLEN n) b. NBWORD n (BNVAL w + BNVAL w + BV b) = SND (SHL F w b)

EQ_NBWORD0_SPLIT

|- !n (w::PWORDLEN n) m.
     m <= n ==>
     ((w = NBWORD n 0) =
      (WSEG (n - m) m w = NBWORD (n - m) 0) /\ (WSEG m 0 w = NBWORD m 0))

MSB_NBWORD

|- !n m. BIT n (NBWORD (SUC n) m) = VB ((m DIV 2 ** n) MOD 2)

NBWORD0

|- !m. NBWORD 0 m = WORD []

NBWORD_BNVAL

|- !n (w::PWORDLEN n). NBWORD n (BNVAL w) = w

NBWORD_MOD

|- !n m. NBWORD n (m MOD 2 ** n) = NBWORD n m

NBWORD_SPLIT

|- !n1 n2 m. NBWORD (n1 + n2) m = WCAT (NBWORD n1 (m DIV 2 ** n2),NBWORD n2 m)

NBWORD_SUC

|- !n m. NBWORD (SUC n) m = WCAT (NBWORD n (m DIV 2),WORD [VB (m MOD 2)])

NBWORD_SUC_FST

|- !n m. NBWORD (SUC n) m = WCAT (WORD [VB ((m DIV 2 ** n) MOD 2)],NBWORD n m)

NBWORD_SUC_WSEG

|- !n (w::PWORDLEN (SUC n)). NBWORD n (BNVAL w) = WSEG n 0 w

PWORDLEN_NBWORD

|- !n m. PWORDLEN n (NBWORD n m)

VB_BV

|- !x. VB (BV x) = x

WCAT_NBWORD_0

|- !n1 n2. WCAT (NBWORD n1 0,NBWORD n2 0) = NBWORD (n1 + n2) 0

WORDLEN_NBWORD

|- !n m. WORDLEN (NBWORD n m) = n

WSEG_NBWORD

|- !m k n. m + k <= n ==> !l. WSEG m k (NBWORD n l) = NBWORD m (l DIV 2 ** k)

WSEG_NBWORD_SUC

|- !n m. WSEG n 0 (NBWORD (SUC n) m) = NBWORD n m

WSPLIT_NBWORD_0

|- !n m. m <= n ==> (WSPLIT m (NBWORD n 0) = (NBWORD (n - m) 0,NBWORD m 0))

ZERO_WORD_VAL

|- !n (w::PWORDLEN n). (w = NBWORD n 0) = (BNVAL w = 0)