Package probability-thm: Properties of probability

Information

nameprobability-thm
version1.3
descriptionProperties of probability
authorJoe Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2012-08-13
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

Input Type Operators

Input 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

x y. fst (x, y) = x

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

xy. x y. xy = (x, y)

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. x y. fn (x, y) = f x y

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