Package probability: Probability

Information

nameprobability
version1.52
descriptionProbability
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
homepagehttp://opentheory.gilith.com/?pkg=probability
hol-light-int-filehol-light.int
hol-light-thm-filehol-light.art
haskell-int-filehaskell.int
haskell-src-filehaskell.art
haskell-arbitrary-type"Probability.Random.random"
checksum3a36731fa2149c1a29fde66a2d1df2f9862211f5
requiresbase
stream
showData.Bool
Data.List
Data.Pair
Data.Stream
Function
Number.Natural
Probability.Random

Files

Defined Type Operator

Defined Constants

Theorems

Geometric.random = Geometric.random.loop 0

bits = random bit

r. fromStream (toStream r) = r

s. toStream (fromStream s) = s

b. r. bit r b

r. bit r head (toStream r)

n r. length (bits n r) = n

f r. random f 0 r = []

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

f n r. length (random f n r) = n

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

f n l. surjective f length l = n r. random f n r = l

r.
    split r =
    let (s1, s2) split (toStream r) in (fromStream s1, fromStream s2)

f r.
    Geometric.random f r =
    let (r1, r2) split r in random f (Geometric.random r1) r2

n r.
    Geometric.random.loop n r =
    let (r1, r2) split r in
    if bit r1 then n else Geometric.random.loop (suc n) r2

n r.
    Geometric.random.loop n r =
    let (r1, r2) split r in
    if bit r1 then n else Geometric.random.loop (n + 1) r2

f r n.
    random f (suc n) r = let (r1, r2) split r in f r1 :: random f n r2

f n r.
    random f n r =
    if n = 0 then []
    else let (r1, r2) split r in f r1 :: random f (n - 1) r2

External Type Operators

External Constants

Assumptions

¬

¬

length [] = 0

p. p

(¬) = λp. p

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

t. (x. t) t

t. (x. t) t

t. (λx. t x) = t

() = λp. p = λx.

t. ( t) t

t. t t

t. t

n. ¬(suc n = 0)

s. head s = nth s 0

() = λp q. p q p

t. (t ) (t )

m. suc m = m + 1

n. suc n - 1 = n

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

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

a n. nth (replicate a) n = a

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

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

x y. x = y y = x

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

m. m = 0 n. m = suc n

s1 s2. split (interleave s1 s2) = (s1, s2)

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

f. surjective f y. x. y = f x

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

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

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

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