Package word16-bits: 16-bit word to bit-list conversions

Information

nameword16-bits
version1.79
description16-bit word to bit-list conversions
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2014-11-01
checksumf11712eb895e0fe29b04cf2da15a2306a99b557a
requiresbool
list
natural
word16-def
showData.Bool
Data.List
Data.Word16
Data.Word16.Bits
Number.Natural

Files

Theorem

w.
    x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15.
      w =
      toWord
        (x0 :: x1 :: x2 :: x3 :: x4 :: x5 :: x6 :: x7 :: x8 :: x9 :: x10 ::
         x11 :: x12 :: x13 :: x14 :: x15 :: [])

External Type Operators

External Constants

Assumptions

length [] = 0

bit0 0 = 0

t. t t

p. p

(¬) = λp. p

t. (x. t) t

() = λp. p = λx.

t. t t

t. t

w. toWord (fromWord w) = w

w. length (fromWord w) = width

n. ¬(suc n = 0)

n. 0 + n = n

n. bit1 n = suc (bit0 n)

width = 16

() = λp q. p q p

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

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

n. bit0 (suc n) = suc (suc (bit0 n))

l. length l = 0 l = []

h t. length (h :: t) = suc (length t)

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

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

m n. m + suc n = suc (m + n)

m n. suc m + n = suc (m + n)

m n. suc m = suc n m = n

l. l = [] h t. l = h :: t

() = λp q. r. (p r) (q r) r

p. p 0 (n. p n p (suc n)) n. p n

h1 h2 t1 t2. h1 :: t1 = h2 :: t2 h1 = h2 t1 = t2