Package word12-bits: 12-bit word to bit-list conversions

Information

nameword12-bits
version1.26
description12-bit word to bit-list conversions
authorJoe Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2011-11-28
requiresbool
natural
list
word12-def
showData.Bool
Data.List
Data.Word12
Data.Word12.Bits
Number.Natural

Files

Theorem

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

Input Type Operators

Input Constants

Assumptions

T

¬F T

¬T F

length [] = 0

bit0 0 = 0

t. t t

n. 0 n

F p. p

(¬) = λp. p F

t. (x. t) t

() = λp. p = λx. T

t. (T t) t

t. (t T) t

t. F t F

t. T t t

t. t T t

t. F t T

t. F t t

t. T t T

w. toWord (fromWord w) = w

w. length (fromWord w) = width

n. ¬(suc n = 0)

n. 0 + n = n

width = 12

t. (t F) ¬t

t. t F ¬t

n. bit1 n = suc (bit0 n)

() = λp q. p q p

n. even (suc n) ¬even n

m. m 0 m = 0

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 = []

t1 t2. t1 t2 t2 t1

n. 2 * n = n + n

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

m n. ¬(m < n n m)

m n. ¬(m n n < m)

m n. suc m n m < n

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

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

m n. even (m * n) even m even n

m n. even (m + n) even m even n

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

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

m n. m n m < n m = n

m n. m n n m m = n

m n. m suc n m = suc n m n

m n. m * n = 0 m = 0 n = 0

P. P 0 (n. P n P (suc n)) n. P n

m n p. m * n = m * p m = 0 n = p

m n p. m * n m * p m = 0 n p

m n p. m * n < m * p ¬(m = 0) n < p

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