Package probability-def: Definition of probability

Information

nameprobability-def
version1.42
descriptionDefinition of probability
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2015-04-18
checksumbd32f1836319b2298e22daf5239b4d66583cd8dc
requiresbase
stream
showData.Bool
Data.List
Data.Pair
Data.Stream
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

r. bit r head (toStream r)

f r. random f 0 r = []

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

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

External Type Operators

External Constants

Assumptions

¬

¬

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

t. (x. t) t

t. (λx. t x) = t

() = λp. p = λx.

t. ( t) t

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

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