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

Information

namenatural-bits-def
version1.10
descriptionDefinition of natural number to bit-list conversions
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2012-08-13
requiresbool
list
natural
pair
probability
relation
showData.Bool
Data.List
Data.Pair
Number.Natural
Probability.Random

Files

Defined Constants

Theorems

Bits.toNatural [] = 0

l. Bits.normal l null l last l

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

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

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

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

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'

Input Type Operators

Input 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)

xy. x y. xy = (x, y)

() = λ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. x y. fn (x, y) = f x y

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

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

b f. fn. fn [] = b h t. fn (h :: t) = f h t (fn t)