Theory: word_num

Parents

• word_base

Types

Constants

• NLIST  :num -> (num -> 'a) -> num -> num -> 'a list
• LVAL  :('a -> num) -> num -> 'a list -> num
• NVAL  :('a -> num) -> num -> 'a word -> num
• NWORD  :num -> (num -> 'a) -> num -> num -> 'a word

Definitions

LVAL_DEF

|- !f b l. LVAL f b l = FOLDL (\e x. b * e + f x) 0 l

NLIST_DEF

|- (!frep b m. NLIST 0 frep b m = []) /\
   !n frep b m.
     NLIST (SUC n) frep b m = SNOC (frep (m MOD b)) (NLIST n frep b (m DIV b))

NVAL_DEF

|- !f b l. NVAL f b (WORD l) = LVAL f b l

NWORD_DEF

|- !n frep b m. NWORD n frep b m = WORD (NLIST n frep b m)

Theorems

LVAL

|- (!f b. LVAL f b [] = 0) /\
   !l f b x. LVAL f b (x::l) = f x * b ** LENGTH l + LVAL f b l

LVAL_MAX

|- !l f b. (!x. f x < b) ==> LVAL f b l < b ** LENGTH l

LVAL_SNOC

|- !l h f b. LVAL f b (SNOC h l) = LVAL f b l * b + f h

NVAL0

|- !f b. NVAL f b (WORD []) = 0

NVAL1

|- !f b x. NVAL f b (WORD [x]) = f x

NVAL_MAX

|- !f b. (!x. f x < b) ==> !n (w::PWORDLEN n). NVAL f b w < b ** n

NVAL_WCAT

|- !n m (w1::PWORDLEN n) (w2::PWORDLEN m) f b.
     NVAL f b (WCAT (w1,w2)) = NVAL f b w1 * b ** m + NVAL f b w2

NVAL_WCAT1

|- !w f b x. NVAL f b (WCAT (w,WORD [x])) = NVAL f b w * b + f x

NVAL_WCAT2

|- !n (w::PWORDLEN n) f b x.
     NVAL f b (WCAT (WORD [x],w)) = f x * b ** n + NVAL f b w

NVAL_WORDLEN_0

|- !(w::PWORDLEN 0) fv r. NVAL fv r w = 0

NWORD_LENGTH

|- !n f b m. WORDLEN (NWORD n f b m) = n

NWORD_PWORDLEN

|- !n f b m. PWORDLEN n (NWORD n f b m)