Package probability-def: Definition of probability

Information

nameprobability-def
version1.33
descriptionDefinition of probability
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2014-01-13
requiresbool
list
natural
pair
relation
stream
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'')

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

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