Package probability-thm: Properties of probability

Information

nameprobability-thm
version1.10
descriptionProperties of probability
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2012-12-10
requiresbool
list
natural
pair
probability-def
showData.Bool
Data.List
Data.Pair
Number.Natural
Probability.Random

Files

Theorems

n r. length (fst (bits n r)) = n

d n r. length (fst (fromRandom d n r)) = n

External Type Operators

External Constants

Assumptions

bits = fromRandom bit

length [] = 0

t. t t

t. (x. t) t

t. (λx. t x) = t

() = λp. p = λx.

t. t

() = λp q. p q p

a b. fst (a, b) = a

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

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

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

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

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

() = λp. q. (x. p x q) q

m n. suc m = suc n m = n

f. fn. a b. fn (a, b) = f a b

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

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