Package probability-def: Definition of probability

Information

nameprobability-def
version1.24
descriptionDefinition of probability
authorJoe Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2012-08-15
requiresbool
natural
pair
relation
showData.Bool
Data.List
Data.Pair
Data.Stream
Number.Natural
Probability.Random

Files

Defined Type Operator

Defined Constants

Theorems

bits = fromRandom bit

r. fromStream (toStream r) = r

s. toStream (fromStream s) = s

d r. fromRandom d 0 r = ([], r)

r. bit r = (head (toStream r), fromStream (tail (toStream r)))

r.
    Geometric.fromRandom r =
    let (r1, r2) split r in (Geometric.fromRandom.loop 0 r1, r2)

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

d r.
    Geometric.fromRandom d r =
    let (n, r') Geometric.fromRandom r in fromRandom d n r'

n r.
    Geometric.fromRandom.loop n r =
    let (b, r') bit r in
    if b then n else Geometric.fromRandom.loop (suc n) r'

d r n.
    fromRandom d (suc n) r =
    let (h, r') d r in let (t, r'') fromRandom d n r' in (h :: t, r'')

Input Type Operators

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

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. () 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