Package byte-bits: Byte to bit-list conversions

Information

namebyte-bits
version1.83
descriptionByte to bit-list conversions
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2014-11-01
checksumbcdeec28e3a9a8809a08b21706fb7350d2a439db
requiresbase
byte-def
showData.Bool
Data.Byte
Data.Byte.Bits
Data.List
Number.Natural

Files

Theorem

b.
    x0 x1 x2 x3 x4 x5 x6 x7.
      b = toByte (x0 :: x1 :: x2 :: x3 :: x4 :: x5 :: x6 :: x7 :: [])

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. toByte (fromByte w) = w

w. length (fromByte w) = width

n. ¬(suc n = 0)

n. 0 + n = n

width = 8

n. bit1 n = suc (bit0 n)

() = λ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