Package natural-bits: Natural number to bit-list conversions

Information

namenatural-bits
version1.25
descriptionNatural number to bit-list conversions
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
requiresbool
function
list
natural
pair
probability
relation
showData.Bool
Data.List
Data.Pair
Function
Number.Natural
Probability.Random

Files

Defined Constants

Theorems

Bits.normal []

¬Bits.head 0

Bits.head 1

fromBool = 0

Bits.toNatural [] = 0

Bits.width 0 = 0

0 = []

n. Bits.normal (Bits.fromNatural n)

¬Bits.head 2

fromBool = 1

Bits.tail 1 = 0

i. ¬Bits.bit 0 i

b. Bits.head (fromBool b) b

b. Bits.tail (fromBool b) = 0

n. Bits.head n odd n

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

n. Bits.append [] n = n

k. Bits.shiftLeft 0 k = 0

n. Bits.shiftLeft n 0 = n

k. Bits.shiftRight 0 k = 0

n. Bits.shiftRight n 0 = n

1 = :: []

b. Bits.cons b 0 = fromBool b

n. Bits.bit n 0 Bits.head n

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

k. Bits.toNatural (replicate k) = 0

l. Bits.toNatural l = Bits.append l 0

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

b. fromBool b = 0 ¬b

b. Bits.toNatural (b :: []) = fromBool b

b. fromBool b = 1 b

n. ¬Bits.head (2 * n)

n. Bits.head (suc n) ¬Bits.head n

n. Bits.cons (Bits.head n) (Bits.tail n) = n

h t. Bits.head (Bits.cons h t) h

h t. Bits.tail (Bits.cons h t) = t

b. fromBool b = if b then 1 else 0

n. h t. n = Bits.cons h t

n. n < 2 Bits.width n

n. Bits.tail n = n div 2

n. Bits.bit (Bits.tail n) = Bits.bit n suc

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

n. suc (Bits.cons n) = Bits.cons n

l. Bits.normal l null l last l

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

b. fromBool b mod 2 = fromBool b

n. fromBool (Bits.head n) = n mod 2

n. Bits.cons n = 2 * n

n. suc (Bits.cons n) = Bits.cons (suc n)

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

l. Bits.toNatural l < 2 length l

n i. Bits.bit n i Bits.head (Bits.shiftRight n i)

n k. Bits.shiftRight n k = (Bits.tail k) n

l n. Bits.append l n = foldr Bits.cons n l

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

n. Bits.shiftLeft n 1 = 2 * n

k. Bits.shiftLeft 1 k = 2 k

h t. Bits.toNatural (h :: t) = Bits.cons h (Bits.toNatural t)

n k. Bits.shiftLeft n k = (Bits.cons k) n

n1 n2. n1 n2 Bits.width n1 Bits.width n2

n i. Bits.bit n (suc i) Bits.bit (Bits.tail n) i

n k. Bits.shiftRight n (suc k) = Bits.tail (Bits.shiftRight n k)

n k. Bits.shiftRight n (suc k) = Bits.shiftRight (Bits.tail n) k

k n. Bits.shiftLeft n k = 0 n = 0

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

b k. Bits.normal (replicate b k) k = 0 b

n1 n2. Bits.head (n1 * n2) Bits.head n1 Bits.head n2

n k. Bits.shiftLeft n (suc k) = Bits.cons (Bits.shiftLeft n k)

n k. Bits.shiftLeft n (suc k) = Bits.shiftLeft (Bits.cons n) k

h t. Bits.normal (h :: t) if null t then h else Bits.normal t

n k. Bits.bound n k = n mod 2 k

n k. Bits.shiftLeft n k = 2 k * n

n k. Bits.shiftRight n k = n div 2 k

n1 n2. Bits.head (n1 + n2) ¬(Bits.head n1 Bits.head n2)

n k. Bits.shiftLeft (Bits.shiftRight n k) k + Bits.bound n k = n

k. Bits.toNatural (replicate k) = 2 k - 1

h t. Bits.cons h t = fromBool h + 2 * t

h t. Bits.cons h t = 0 ¬h t = 0

h t. Bits.cons h t = 1 h t = 0

h t1 t2. Bits.cons h t1 Bits.cons h t2 t1 t2

h t n. Bits.append (h :: t) n = Bits.cons h (Bits.append t n)

n k i. Bits.bit n (k + i) Bits.bit (Bits.shiftRight n k) i

n k1 k2.
    Bits.shiftLeft n (k1 + k2) = Bits.shiftLeft (Bits.shiftLeft n k1) k2

n k1 k2.
    Bits.shiftRight n (k1 + k2) = Bits.shiftRight (Bits.shiftRight n k1) k2

k n1 n2. Bits.shiftLeft n1 k = Bits.shiftLeft n2 k n1 = n2

k n1 n2. Bits.shiftLeft n1 k Bits.shiftLeft n2 k n1 n2

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

n.
    Bits.fromNatural n =
    if n = 0 then [] else Bits.head n :: Bits.fromNatural (Bits.tail n)

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

l1 l2.
    Bits.toNatural (l1 @ l2) =
    Bits.toNatural l1 + Bits.shiftLeft (Bits.toNatural l2) (length l1)

h t. Bits.toNatural (h :: t) = 0 ¬h Bits.toNatural t = 0

h1 h2 t. Bits.cons h1 t Bits.cons h2 t fromBool h1 fromBool h2

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

p. p 0 (h t. p t p (Bits.cons h t)) n. p n

h1 h2 t1 t2. Bits.cons h1 t1 = Bits.cons h2 t2 (h1 h2) t1 = t2

p. p 0 (n. ¬(n = 0) p (Bits.tail n) p n) n. p n

n r.
    Uniform.fromRandom n r =
    let w Bits.width (n - 1) in
    let (r1, r2) split r in
    (Uniform.fromRandom.loop n w r1 mod n, r2)

n w r.
    Uniform.fromRandom.loop n w r =
    let (l, r') bits w r in
    let m Bits.toNatural l in
    if m < n then m else Uniform.fromRandom.loop n w r'

External Type Operators

External Constants

Assumptions

null []

¬odd 0

¬

¬

length [] = 0

bit0 0 = 0

n. 0 n

p. p

x. id x = x

t. t ¬t

m. ¬(m < 0)

n. 0 < suc n

n. n < suc n

(¬) = λp. p

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

t. (x. t) t

t. (λx. t x) = t

() = λp. p = λx.

x. replicate x 0 = []

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)

m. m * 0 = 0

n. 0 + n = n

m. m + 0 = m

m. interval m 0 = []

l. [] @ l = l

f. f 0 = id

f. map f [] = []

x. last (x :: []) = x

t. ( t) ¬t

t. (t ) ¬t

t. t ¬t

n. bit1 n = suc (bit0 n)

n. ¬odd n even n

m. m 0 = 1

m. m * 1 = m

n. n 1 = n

n. n div 1 = n

m. 1 * m = m

l. null l l = []

h t. ¬null (h :: t)

() = λp q. p q p

t. (t ) (t )

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

x n. length (replicate x n) = n

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

m n. length (interval m n) = n

p x. p x p ((select) p)

f b. foldr f b [] = b

n. 0 < n ¬(n = 0)

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

x. a b. x = (a, b)

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

m n. m + n = n + m

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

n. 2 * n = n + n

x n. null (replicate x n) n = 0

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

n. even n n mod 2 = 0

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 = n m = 0

n. odd n n mod 2 = 1

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

x n. replicate x (suc n) = x :: replicate x n

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

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

m n. odd (m * n) odd m odd n

m n. m * suc n = m + m * n

m n. m suc n = m * m n

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

f n. f suc n = f f n

f n. f suc n = f n f

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

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

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

f. fn. a b. fn (a, b) = f a b

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)

m n p. m * (n * p) = m * n * p

m n p. m + (n + p) = m + n + p

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

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

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

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

l h t. (h :: t) @ l = h :: t @ l

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

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

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

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

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

m n p. m * (n + p) = m * n + m * p

f m n. f (m + n) = f m f n

p g h. f. x. f x = if p x then f (g x) else h x

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

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

f b h t. foldr f b (h :: t) = f h (foldr f b t)

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)

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

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

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

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

k n1 n2. 1 < k ¬(n1 = 0) n1 n2 log k n1 log k n2

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

k p. 1 < k p 0 (n. ¬(n = 0) p (n div k) p n) n. p n

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)