Package natural-bits-thm: Properties of natural number to bit-list conversions

Information

namenatural-bits-thm
version1.9
descriptionProperties of natural number to bit-list conversions
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2012-08-13
requiresbool
function
list
natural
natural-bits-def
showData.Bool
Data.List
Function
Number.Natural

Files

Theorems

Bits.normal []

Bits.width 0 = 0

0 = []

n. Bits.normal (Bits.fromNatural n)

i. ¬Bits.bit 0 i

n. Bits.toNatural (Bits.fromNatural n) = n

1 = :: []

n. Bits.bit n 0 odd n

n. length (Bits.fromNatural n) = Bits.width n

l. Bits.width (Bits.toNatural l) length l

n. n < 2 Bits.width n

n. Bits.fromNatural n = [] n = 0

l. Bits.normal l Bits.fromNatural (Bits.toNatural l) = l

l. Bits.normal l Bits.width (Bits.toNatural l) = length l

l. Bits.toNatural l < 2 length l

n. Bits.bit (n div 2) = Bits.bit n suc

m. Bits.width (2 m - 1) = m

h t. Bits.toNatural (h :: t) div 2 = Bits.toNatural t

n i. Bits.bit n (suc i) Bits.bit (n div 2) i

l i. Bits.bit (Bits.toNatural l) i i < length l nth l i

n. Bits.width n = if n = 0 then 0 else Bits.width (n div 2) + 1

n.
    Bits.fromNatural n =
    if n = 0 then [] else odd n :: Bits.fromNatural (n div 2)

Input Type Operators

Input Constants

Assumptions

null []

¬odd 0

¬

¬

length [] = 0

bit0 0 = 0

Bits.toNatural [] = 0

t. t t

n. 0 n

p. p

t. t ¬t

m. ¬(m < 0)

n. 0 < suc n

n. n < suc n

(¬) = λp. p

t. (x. t) t

() = λp. p = λx.

t. ¬¬t t

t. ( t) t

t. (t ) t

t. t

t. t t

t. t t

t. t

t. t t

t. t

t. t t

t. t

t. t t

n. ¬(suc n = 0)

n. even n odd n

n. 0 * n = 0

m. m * 0 = 0

n. 0 + n = n

m. m + 0 = m

n. n - n = 0

m. interval m 0 = []

f. map f [] = []

t. ( t) ¬t

t. (t ) ¬t

t. t ¬t

n. even (2 * n)

n. bit1 n = suc (bit0 n)

n. ¬odd n even n

m. m 0 = 1

n. n div 1 = n

h t. ¬null (h :: t)

() = λp q. p q p

t. (t ) (t )

n. odd (suc (2 * n))

m. suc m = m + 1

n. even (suc n) ¬even n

n. odd (suc n) ¬odd n

m. m 0 m = 0

n. suc n - 1 = n

t1 t2. (if then t1 else t2) = t2

t1 t2. (if then t1 else t2) = t1

h t. ¬(h :: t = [])

m n. length (interval m n) = n

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

l. Bits.normal l null l last l

x y. x = y y = x

x y. x = y y = x

h t. nth (h :: t) 0 = h

t1 t2. t1 t2 t2 t1

m n. m * n = n * m

f l. length (map f l) = length l

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. ¬(m n) n < m

m n. suc m n m < n

m. m = 0 n. m = suc n

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

n. even n n mod 2 = 0

n. Bits.fromNatural n = map (Bits.bit n) (interval 0 (Bits.width n))

n. ¬(n = 0) 0 div n = 0

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

m n. m < n m div n = 0

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. suc m < suc n m < n

m n. suc m suc n m n

m n. m + n = m n = 0

n. odd n n mod 2 = 1

f g x. (f g) x = f (g x)

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

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

m n. m suc n = m * m n

m n. map suc (interval m n) = interval (suc m) n

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

f g. (x. f x = g x) f = g

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

h t. last (h :: t) = if null t then h else last t

m n. m n m < n m = n

m n. odd (m + n) ¬(odd m odd n)

m n. interval m (suc n) = m :: interval (suc m) n

m n. m n n m m = n

n i. Bits.bit n i odd (n div 2 i)

m n. ¬(m = 0) m * n div m = n

m n. ¬(m = 0) m * n mod m = 0

x y z. x = y y = z x = z

x1 x2 l. last (x1 :: x2 :: l) = last (x2 :: l)

t1 t2 t3. (t1 t2) t3 t1 t2 t3

m n p. m + p = n + p m = n

m n p. m < n n p m < p

f g l. map (f g) l = map f (map g l)

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

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

m n. m + n = 0 m = 0 n = 0

f h t. map f (h :: t) = f h :: map f t

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

m n. ¬(n = 0) (m div n = 0 m < n)

m n. m n = 0 m = 0 ¬(n = 0)

m n i. i < n nth (interval m n) i = m + i

n. Bits.width n = if n = 0 then 0 else log 2 n + 1

x n. x n = 1 x = 1 n = 0

m n. ¬(n = 0) (m div n) * n + m mod n = m

p. p [] (h t. p t p (h :: t)) l. p l

h t n. n < length t nth (h :: t) (suc n) = nth t n

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

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

f l i. i < length l nth (map f l) i = f (nth l i)

h t. Bits.toNatural (h :: t) = 2 * Bits.toNatural t + if h then 1 else 0

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

k m. 1 < k log k (k (m + 1) - 1) = m

p c x y. p (if c then x else y) (c p x) (¬c p y)

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

m n q r. m = q * n + r r < n m div n = q

m n q r. m = q * n + r r < n m mod n = r

k n. 1 < k ¬(n = 0) n < k (log k n + 1)

p. p 0 (n. ¬(n = 0) p (n div 2) p n) n. p n

l1 l2.
    length l1 = length l2 (i. i < length l1 nth l1 i = nth l2 i)
    l1 = l2

k n.
    1 < k ¬(n = 0) log k n = if n < k then 0 else log k (n div k) + 1

x m n. x m x n if x = 0 then m = 0 n = 0 else x = 1 m n

a b n.
    ¬(n = 0)
    ((a + b) mod n = a mod n + b mod n (a + b) div n = a div n + b div n)