Package natural-bits-def: Definition of natural number to bit-list conversions

Information

namenatural-bits-def
version1.31
descriptionDefinition of natural number to bit-list conversions
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2015-04-18
checksumd3b322d91850c4c6fedf840cc18dcc7fb27aca1d
requiresbase
probability
showData.Bool
Data.List
Data.Pair
Number.Natural
Probability.Random

Files

Defined Constants

Theorems

n. Bits.head n odd n

n. Bits.toVector n 0 = []

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

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

b. fromBool b = if b then 1 else 0

n. Bits.tail n = n div 2

l. Bits.normalList l null l last l

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

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

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

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

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

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

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

n. Bits.width n = if n = 0 then 0 else log 2 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 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

External Type Operators

External Constants

Assumptions

¬

¬

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

t. (λx. t x) = t

() = λp. p = λx.

t. t

() = λp q. p q p

t. (t ) (t )

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

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

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

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

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

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

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

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

r. (x. y. r x y) f. x. r x (f x)

(∃!) = λp. () p x y. p x p y x = y

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

e f. ∃!fn. fn 0 = e n. fn (suc n) = f (fn n) n