Theory: prob

Parents

• probAlgebra

Types

Constants

• alg_measure  :bool list list -> real
• prob  :((num -> bool) -> bool) -> real
• algebra_measure  :bool list list -> real

Definitions

alg_measure_def

|- (alg_measure [] = 0) /\
   !l rest. alg_measure (l::rest) = (1 / 2) pow LENGTH l + alg_measure rest

algebra_measure_def

|- !b.
     algebra_measure b =
     inf (\r. ?c. (algebra_embed b = algebra_embed c) /\ (alg_measure c = r))

prob_def

|- !s.
     prob s =
     sup (\r. ?b. (algebra_measure b = r) /\ algebra_embed b SUBSET s)

Theorems

ABS_PROB

|- !p. abs (prob p) = prob p

ALG_CANON1_MONO

|- !l. alg_measure (alg_canon1 l) <= alg_measure l

ALG_CANON2_MONO

|- !l. alg_measure (alg_canon2 l) <= alg_measure l

ALG_CANON_FIND_MONO

|- !l b. alg_measure (alg_canon_find l b) <= alg_measure (l::b)

ALG_CANON_MERGE_MONO

|- !l b. alg_measure (alg_canon_merge l b) <= alg_measure (l::b)

ALG_CANON_MONO

|- !l. alg_measure (alg_canon l) <= alg_measure l

ALG_CANON_PREFS_MONO

|- !l b. alg_measure (alg_canon_prefs l b) <= alg_measure (l::b)

ALG_MEASURE_ADDITIVE

|- !b.
     algebra_canon b ==>
     !c.
       algebra_canon c ==>
       !d.
         algebra_canon d ==>
         (algebra_embed c INTER algebra_embed d = {}) /\
         (algebra_embed b = algebra_embed c UNION algebra_embed d) ==>
         (alg_measure b = alg_measure c + alg_measure d)

ALG_MEASURE_APPEND

|- !l1 l2. alg_measure (APPEND l1 l2) = alg_measure l1 + alg_measure l2

ALG_MEASURE_BASIC

|- (alg_measure [] = 0) /\ (alg_measure [[]] = 1) /\
   !b. alg_measure [[b]] = 1 / 2

ALG_MEASURE_COMPL

|- !b.
     algebra_canon b ==>
     !c.
       algebra_canon c ==>
       (COMPL (algebra_embed b) = algebra_embed c) ==>
       (alg_measure b + alg_measure c = 1)

ALG_MEASURE_POS

|- !l. 0 <= alg_measure l

ALG_MEASURE_TLS

|- !l b. 2 * alg_measure (MAP (CONS b) l) = alg_measure l

ALG_TWINS_MEASURE

|- !l.
     (1 / 2) pow LENGTH (SNOC T l) + (1 / 2) pow LENGTH (SNOC F l) =
     (1 / 2) pow LENGTH l

ALGEBRA_CANON_MEASURE_MAX

|- !l. algebra_canon l ==> alg_measure l <= 1

ALGEBRA_MEASURE_BASIC

|- (algebra_measure [] = 0) /\ (algebra_measure [[]] = 1) /\
   !b. algebra_measure [[b]] = 1 / 2

ALGEBRA_MEASURE_DEF_ALT

|- !l. algebra_measure l = alg_measure (alg_canon l)

ALGEBRA_MEASURE_MAX

|- !l. algebra_measure l <= 1

ALGEBRA_MEASURE_MONO_EMBED

|- !b c.
     algebra_embed b SUBSET algebra_embed c ==>
     algebra_measure b <= algebra_measure c

ALGEBRA_MEASURE_POS

|- !l. 0 <= algebra_measure l

ALGEBRA_MEASURE_RANGE

|- !l. 0 <= algebra_measure l /\ algebra_measure l <= 1

PROB_ADDITIVE

|- !s t.
     measurable s /\ measurable t /\ (s INTER t = {}) ==>
     (prob (s UNION t) = prob s + prob t)

PROB_ALG

|- !x. prob (alg_embed x) = (1 / 2) pow LENGTH x

PROB_ALGEBRA

|- !l. prob (algebra_embed l) = algebra_measure l

PROB_BASIC

|- (prob {} = 0) /\ (prob UNIV = 1) /\ !b. prob (\s. SHD s = b) = 1 / 2

PROB_COMPL

|- !s. measurable s ==> (prob (COMPL s) = 1 - prob s)

PROB_COMPL_LE1

|- !p r. measurable p ==> (prob (COMPL p) <= r = 1 - r <= prob p)

PROB_INTER_HALVES

|- !p.
     measurable p ==>
     (prob ((\x. SHD x = T) INTER p) + prob ((\x. SHD x = F) INTER p) =
      prob p)

PROB_INTER_SHD

|- !b p.
     measurable p ==> (prob ((\x. SHD x = b) INTER p o STL) = 1 / 2 * prob p)

PROB_LE_X

|- !s x. (!s'. measurable s' /\ s' SUBSET s ==> prob s' <= x) ==> prob s <= x

PROB_MAX

|- !p. prob p <= 1

PROB_POS

|- !p. 0 <= prob p

PROB_RANGE

|- !p. 0 <= prob p /\ prob p <= 1

PROB_SDROP

|- !n p. measurable p ==> (prob (p o SDROP n) = prob p)

PROB_SHD

|- !b. prob (\s. SHD s = b) = 1 / 2

PROB_STL

|- !p. measurable p ==> (prob (p o STL) = prob p)

PROB_SUBSET_MONO

|- !s t. s SUBSET t ==> prob s <= prob t

PROB_SUP_EXISTS1

|- !s. ?r b. (algebra_measure b = r) /\ algebra_embed b SUBSET s

PROB_SUP_EXISTS2

|- !s.
     ?z.
       !r.
         (?b. (algebra_measure b = r) /\ algebra_embed b SUBSET s) ==> r <= z

X_LE_PROB

|- !s x. (?s'. measurable s' /\ s' SUBSET s /\ x <= prob s') ==> x <= prob s