Package word-bits-def: Definition of word to bit-list conversions

Information

nameword-bits-def
version1.51
descriptionDefinition of word to bit-list conversions
authorJoe Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2012-06-10
requiresbool
list
showData.Bool
Data.List
Data.Word
Data.Word.Bits
Number.Natural

Files

Defined Constants

Theorems

toWord [] = 0

q. compare q [] [] q

l. normal l length l = width

w. not w = toWord (map (¬) (fromWord w))

w. fromWord w = map (bit w) (interval 0 width)

w n. bit w n odd (toNatural (shiftRight w n))

w1 w2. and w1 w2 = toWord (zipWith () (fromWord w1) (fromWord w2))

w1 w2. or w1 w2 = toWord (zipWith () (fromWord w1) (fromWord w2))

w n. shiftLeft w n = fromNatural (2 n * toNatural w)

w n. shiftRight w n = fromNatural (toNatural w div 2 n)

h t.
    toWord (h :: t) =
    if h then shiftLeft (toWord t) 1 + 1 else shiftLeft (toWord t) 1

q h1 h2 t1 t2.
    compare q (h1 :: t1) (h2 :: t2)
    compare (¬h1 h2 ¬(h1 ¬h2) q) t1 t2

Input Type Operators

Input Constants

Assumptions

() = λp. p ((select) p)

t. (x. t) t

() = λp. p = λx.

() = λp q. p q p

h t. head (h :: t) = h

h t. tail (h :: t) = t

() = λp q. (λf. f p q) = λf. f

() = λp. q. (x. p x q) q

p. (x. y. p x y) y. x. p x (y x)

b f. fn. fn [] = b h t. fn (h :: t) = f h t (fn t)