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

Information

namenatural-bits-thm
version1.57
descriptionProperties of natural number to bit-list conversions
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2015-11-01
checksumcee34b637312544f60b2db476dcb9d01b881d29a
requiresbase
natural-bits-def
probability
showData.Bool
Data.List
Data.Pair
Function
Number.Natural
Probability.Random

Files

Theorems

Bits.normalList []

¬Bits.head 0

Bits.head 1

fromBool = 0

Bits.fromList [] = 0

Bits.tail 0 = 0

Bits.width 0 = 0

Bits.toList 0 = []

n. Bits.normalList (Bits.toList n)

¬Bits.head 2

fromBool = 1

Bits.tail 1 = 0

i. ¬Bits.bit 0 i

Bits.width 1 = 1

b. Bits.head (fromBool b) b

b. Bits.tail (fromBool b) = 0

n. Bits.fromList (Bits.toList n) = n

n. Bits.and 0 n = 0

n. Bits.and n 0 = 0

n. Bits.and n n = n

n. Bits.append [] n = n

k. Bits.bound 0 k = 0

n. Bits.bound n 0 = 0

n. Bits.or 0 n = n

n. Bits.or n 0 = n

n. Bits.or n 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

Bits.toList 1 = :: []

b. fromBool b < 2

b. Bits.width (fromBool b) = fromBool b

b. Bits.cons b 0 = fromBool b

n. Bits.bit n 0 Bits.head n

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

k. Bits.fromList (replicate k) = 0

n. Bits.bound n (Bits.width n) = n

n. Bits.shiftRight n (Bits.width n) = 0

l. Bits.width (Bits.fromList l) length l

m n. m Bits.or m n

m n. n Bits.or m n

m n. Bits.and m n m

m n. Bits.and m n n

n k. Bits.bound n k n

b. fromBool b = 0 ¬b

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

b. fromBool b = 1 b

n. ¬Bits.head (2 * n)

n. Bits.tail n = Bits.shiftRight n 1

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

k. Bits.toVector 0 k = replicate k

n. Bits.shiftRight n 1 = Bits.tail 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

n k. length (Bits.toVector n k) = k

n k. Bits.width (Bits.bound n k) k

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

n. n < 2 Bits.width n

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

n. Bits.width n = 0 n = 0

n. Bits.toList n = [] n = 0

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

n. Bits.bound n 1 = fromBool (Bits.head n)

l. Bits.normalList l Bits.toList (Bits.fromList l) = l

l. Bits.fromList l = 0 all (¬) l

m n. Bits.and m n = Bits.and n m

m n. Bits.or m n = Bits.or n m

m n. max m n Bits.or m n

m n. Bits.and m n min m n

n k. Bits.bound (Bits.shiftLeft n k) k = 0

n k. Bits.shiftRight (Bits.bound n k) k = 0

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

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.normalList l Bits.width (Bits.fromList l) = length l

l. Bits.fromList l < 2 length l

h t. Bits.width (Bits.cons h t) suc (Bits.width t)

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

n i. Bits.bit n i i < Bits.width n

n k. Bits.fromList (Bits.toVector n k) = Bits.bound n k

n. (i. ¬Bits.bit n i) n = 0

n. (i. ¬Bits.bit n i) n = 0

n. Bits.shiftLeft n 1 = 2 * n

k. Bits.shiftLeft 1 k = 2 k

k. Bits.width (Bits.shiftLeft 1 k) = k + 1

b1 b2. fromBool b1 = fromBool b2 b1 b2

h t. Bits.fromList (h :: t) = Bits.cons h (Bits.fromList 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

n k. Bits.width (Bits.shiftLeft n k) Bits.width n + k

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

n k. Bits.bound (Bits.bound n k) k = Bits.bound n k

n k. Bits.toVector (Bits.bound n k) k = Bits.toVector n k

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

b1 b2. fromBool b1 < fromBool b2 ¬b1 b2

b1 b2. fromBool b1 fromBool b2 ¬b1 b2

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

q n. Bits.compare q n 0 q n = 0

n k. Bits.toVector n k = map (Bits.bit n) (interval 0 k)

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

m n. Bits.head (Bits.and m n) Bits.head m Bits.head n

m n. Bits.head (Bits.or m n) Bits.head m Bits.head n

m n. Bits.tail (Bits.and m n) = Bits.and (Bits.tail m) (Bits.tail n)

m n. Bits.tail (Bits.or m n) = Bits.or (Bits.tail m) (Bits.tail n)

m n. Bits.width (max m n) = max (Bits.width m) (Bits.width n)

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

m n. Bits.width (m * n) Bits.width m + Bits.width n

n k. Bits.bound n k = n Bits.width n k

n k. Bits.shiftRight n k = 0 Bits.width n k

n i. i < n r. Uniform.random n r = i

n. Bits.cons n = 1 + 2 * n

q n. Bits.compare q 0 n q ¬(n = 0)

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

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

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

n1 n2. Bits.tail (n1 + Bits.cons n2) = Bits.tail n1 + n2

m n. Bits.or m n + Bits.and m n = m + n

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

n.
    Uniform.random n =
    λr. let w Bits.width (n - 1) in Uniform.random.loop n w r

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

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

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

n k. Bits.width n k n < 2 k

n k.
    Bits.bound n (suc k) =
    Bits.cons (Bits.head n) (Bits.bound (Bits.tail n) k)

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

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

n j k. Bits.bound (Bits.bound n j) k = Bits.bound n (min j k)

k n1 n2. Bits.shiftLeft (n1 * n2) k = n1 * Bits.shiftLeft n2 k

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

n1 n2 k. Bits.bound (n1 + Bits.shiftLeft n2 k) k = Bits.bound n1 k

m n. (i. Bits.bit m i Bits.bit n i) m = n

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

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

h t. ¬(t = 0) Bits.width (Bits.cons h t) = suc (Bits.width t)

m n. Bits.width (m + n) max (Bits.width m) (Bits.width n) + 1

m n. Bits.or m n = 0 m = 0 n = 0

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

l k. k length l Bits.toVector (Bits.fromList l) k = take k l

l k. Bits.toVector (Bits.fromList l) (length l + k) = l @ replicate k

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

h1 h2 t1 t2. t1 < t2 Bits.cons h1 t1 < Bits.cons h2 t2

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

n k. ¬(n = 0) Bits.width (Bits.shiftLeft n k) = Bits.width n + k

n k. Bits.and n (2 k - 1) = Bits.bound n k

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

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

m n i. Bits.bit (Bits.and m n) i Bits.bit m i Bits.bit n i

n i k. Bits.bit (Bits.bound n k) i i < k Bits.bit n i

m n i. Bits.bit (Bits.or m n) i Bits.bit m i Bits.bit n i

m n k.
    Bits.bound (Bits.and m n) k =
    Bits.and (Bits.bound m k) (Bits.bound n k)

m n k.
    Bits.bound (Bits.or m n) k = Bits.or (Bits.bound m k) (Bits.bound n k)

k n1 n2.
    Bits.shiftLeft (n1 + n2) k = Bits.shiftLeft n1 k + Bits.shiftLeft n2 k

n j k. Bits.width n j + k Bits.width (Bits.shiftRight n k) j

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

n1 n2 k.
    Bits.shiftRight (n1 + Bits.shiftLeft n2 k) k =
    Bits.shiftRight n1 k + n2

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

n k.
    Bits.bound n (suc k) =
    Bits.bound n k + Bits.shiftLeft (fromBool (Bits.bit n k)) k

l k.
    Bits.bound (Bits.fromList l) k =
    Bits.fromList (if length l k then l else take k l)

l k.
    Bits.shiftRight (Bits.fromList l) k =
    if length l k then 0 else Bits.fromList (drop k l)

m n k.
    Bits.toVector (Bits.and m n) k =
    zipWith () (Bits.toVector m k) (Bits.toVector n k)

m n k.
    Bits.toVector (Bits.or m n) k =
    zipWith () (Bits.toVector m k) (Bits.toVector n k)

n i. i < n r. Uniform.random.loop n (Bits.width (n - 1)) r = i

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

n k i. Bits.bit (Bits.shiftLeft n k) i k i Bits.bit n (i - k)

m n k.
    Bits.bound (Bits.bound m k * Bits.bound n k) k = Bits.bound (m * n) k

m n k.
    Bits.bound (Bits.bound m k + Bits.bound n k) k = Bits.bound (m + n) k

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

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

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

m n p k. m = n + Bits.shiftLeft p k Bits.bound m k = Bits.bound n k

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

n k.
    Bits.toVector n k =
    if k = 0 then []
    else Bits.head n :: Bits.toVector (Bits.tail n) (k - 1)

m n j k.
    Bits.width (Bits.bound m k + Bits.shiftLeft n k) j + k
    Bits.width n j

l k.
    Bits.toVector (Bits.fromList l) k =
    if length l k then l @ replicate (k - length l) else take k l

h1 h2 t1 t2.
    Bits.cons h1 t1 < Bits.cons h2 t2
    t1 < t2 t1 = t2 fromBool h1 < fromBool h2

h1 h2 t1 t2.
    Bits.cons h1 t1 Bits.cons h2 t2
    t1 < t2 t1 = t2 fromBool h1 fromBool h2

q h1 h2 t1 t2.
    Bits.compare q (Bits.cons h1 t1) (Bits.cons h2 t2)
    Bits.compare (¬h1 h2 ¬(h1 ¬h2) q) t1 t2

External Type Operators

External Constants

Assumptions

null []

¬odd 0

¬

¬

length [] = 0

bit0 0 = 0

t. t t

n. 0 n

n. n n

p. all p []

p. p

x. id x = x

t. t ¬t

m. ¬(m < 0)

n. 0 < suc n

n. n < suc n

n. n suc n

(¬) = λp. 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. t

t. t t

t. t

t. t t

t. t

t. t t t

n. ¬(suc n = 0)

n. Bits.head n odd n

m. m * 0 = 0

n. 0 + n = n

m. m + 0 = m

n. min n n = n

n. Bits.toVector n 0 = []

m. interval m 0 = []

l. [] @ l = l

l. drop 0 l = l

l. take 0 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 = []

l. Bits.fromList l = Bits.append l 0

f. zipWith f [] [] = []

h t. ¬null (h :: t)

m n. m m + n

m n. m max m n

m n. n m + n

m n. n max m n

() = λp q. p q p

t. (t ) (t )

m. suc m = m + 1

n. Bits.toList n = Bits.toVector n (Bits.width 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 = [])

b t. (if b then t else t) = t

m n. length (interval m n) = n

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

f b. foldr f b [] = b

b. fromBool b = if b then 1 else 0

n. Bits.tail n = n div 2

n. 0 < n ¬(n = 0)

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

l. Bits.normalList 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

t1 t2. t1 t2 t2 t1

m n. m * n = n * m

m n. m + n = n + m

m n. m < n m n

m n. m + n - m = n

m n. m + n - n = m

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

n. 2 * n = n + n

r1 r2. r. split r = (r1, r2)

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

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

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

m n. ¬(m < n) n m

m n. ¬(m n) n < m

m n. m < suc n m n

m n. suc m n m < n

m. m = 0 n. m = suc n

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

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

t1 t2. ¬t1 ¬t2 t2 t1

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

m n. m + n = n m = 0

n. odd n n mod 2 = 1

k. 1 < k log k 1 = 0

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

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

t1 t2. ¬(t1 t2) ¬t1 ¬t2

t1 t2. ¬(t1 t2) ¬t1 ¬t2

m n. max m n = if m n then n else m

m n. min m n = if m n then m else 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

l1 l2. length (l1 @ l2) = length l1 + length l2

f n. f suc n = f f n

f n. f suc n = f n f

m n. m n d. n = m + d

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

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

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

n l. length l = n r. bits n r = l

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

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

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

n k.
    Bits.toVector n (suc k) = Bits.head n :: Bits.toVector (Bits.tail n) k

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)

x n i. i < n nth (replicate x n) i = x

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

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

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

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

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

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

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)

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

n r.
    Uniform.random n r =
    let w Bits.width (n - 1) in Uniform.random.loop n w r

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

p h t. all p (h :: t) p h all p 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)

q m n. Bits.compare q m n if q then m n else m < n

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

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

m n p. m min n p m n m p

m n p. max n p m n m p m

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

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

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

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

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

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

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)

k m n. 1 < k k m n m log k n

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

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

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

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)

m n.
    Bits.and m n =
    Bits.fromList
      (map (λi. Bits.bit m i Bits.bit n i)
         (interval 0 (min (Bits.width m) (Bits.width n))))

m n.
    Bits.or m n =
    Bits.fromList
      (map (λi. Bits.bit m i Bits.bit n i)
         (interval 0 (max (Bits.width m) (Bits.width n))))

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

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

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

f h1 h2 t1 t2.
    length t1 = length t2
    zipWith f (h1 :: t1) (h2 :: t2) = f h1 h2 :: zipWith f t1 t2

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

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

n w r.
    Uniform.random.loop n w r =
    let (r1, r2) split r in
    let l bits w r1 in
    let m Bits.fromList l in
    if m < n then m else Uniform.random.loop n w r2

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)