Theory: probIndep

Parents

• prob
• stateTransformer

Types

Constants

• indep  :((num -> bool) -> 'a # (num -> bool)) -> bool
• indep_set  :((num -> bool) -> bool) -> ((num -> bool) -> bool) -> bool
• alg_cover_set  :bool list list -> bool
• alg_cover  :bool list list -> (num -> bool) -> bool list

Definitions

alg_cover_def

|- !l x. alg_cover l x = @b. MEM b l /\ alg_embed b x

alg_cover_set_def

|- !l.
     alg_cover_set l =
     alg_sorted l /\ alg_prefixfree l /\ (algebra_embed l = UNIV)

indep_def

|- !f.
     indep f =
     ?l r.
       alg_cover_set l /\
       !s. f s = (let c = alg_cover l s in (r c,SDROP (LENGTH c) s))

indep_set_def

|- !p q.
     indep_set p q =
     measurable p /\ measurable q /\ (prob (p INTER q) = prob p * prob q)

Theorems

ALG_COVER_EXISTS_UNIQUE

|- !l. alg_cover_set l ==> !s. ?!x. MEM x l /\ alg_embed x s

ALG_COVER_HEAD

|- !l. alg_cover_set l ==> !f. f o alg_cover l = algebra_embed (FILTER f l)

ALG_COVER_SET_BASIC

|- ~alg_cover_set [] /\ alg_cover_set [[]] /\ alg_cover_set [[T]; [F]]

ALG_COVER_SET_CASES

|- !P.
     P [[]] /\
     (!l1 l2.
        alg_cover_set l1 /\ alg_cover_set l2 /\
        alg_cover_set (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2)) ==>
        P (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2))) ==>
     !l. alg_cover_set l ==> P l

ALG_COVER_SET_CASES_THM

|- !l.
     alg_cover_set l =
     (l = [[]]) \/
     ?l1 l2.
       alg_cover_set l1 /\ alg_cover_set l2 /\
       (l = APPEND (MAP (CONS T) l1) (MAP (CONS F) l2))

ALG_COVER_SET_INDUCTION

|- !P.
     P [[]] /\
     (!l1 l2.
        alg_cover_set l1 /\ alg_cover_set l2 /\ P l1 /\ P l2 /\
        alg_cover_set (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2)) ==>
        P (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2))) ==>
     !l. alg_cover_set l ==> P l

ALG_COVER_STEP

|- !l1 l2 h t.
     alg_cover_set l1 /\ alg_cover_set l2 ==>
     (alg_cover (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2)) (SCONS h t) =
      (if h then T::alg_cover l1 t else F::alg_cover l2 t))

ALG_COVER_TAIL_MEASURABLE

|- !l.
     alg_cover_set l ==>
     !q.
       measurable (q o (\x. SDROP (LENGTH (alg_cover l x)) x)) = measurable q

ALG_COVER_TAIL_PROB

|- !l.
     alg_cover_set l ==>
     !q.
       measurable q ==>
       (prob (q o (\x. SDROP (LENGTH (alg_cover l x)) x)) = prob q)

ALG_COVER_TAIL_STEP

|- !l1 l2 q.
     alg_cover_set l1 /\ alg_cover_set l2 ==>
     (q o
      (\x.
         SDROP
           (LENGTH (alg_cover (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2)) x))
           x) =
      (\x. SHD x = T) INTER
      q o (\x. SDROP (LENGTH (alg_cover l1 x)) x) o STL UNION
      (\x. SHD x = F) INTER q o (\x. SDROP (LENGTH (alg_cover l2 x)) x) o STL)

ALG_COVER_UNIQUE

|- !l x s. alg_cover_set l /\ MEM x l /\ alg_embed x s ==> (alg_cover l s = x)

ALG_COVER_UNIV

|- alg_cover [[]] = K []

ALG_COVER_WELL_DEFINED

|- !l x.
     alg_cover_set l ==> MEM (alg_cover l x) l /\ alg_embed (alg_cover l x) x

BIND_STEP

|- !f. BIND SDEST (\k. f o SCONS k) = f

INDEP_BIND

|- !f g. indep f /\ (!x. indep (g x)) ==> indep (BIND f g)

INDEP_BIND_SDEST

|- !f. (!x. indep (f x)) ==> indep (BIND SDEST f)

INDEP_INDEP_SET

|- !f p q. indep f /\ measurable q ==> indep_set (p o FST o f) (q o SND o f)

INDEP_INDEP_SET_LEMMA

|- !l.
     alg_cover_set l ==>
     !q.
       measurable q ==>
       !x.
         MEM x l ==>
         (prob
            (alg_embed x INTER q o (\x. SDROP (LENGTH (alg_cover l x)) x)) =
          (1 / 2) pow LENGTH x * prob q)

INDEP_MEASURABLE1

|- !f p. indep f ==> measurable (p o FST o f)

INDEP_MEASURABLE2

|- !f q. indep f /\ measurable q ==> measurable (q o SND o f)

INDEP_PROB

|- !f p q.
     indep f /\ measurable q ==>
     (prob (p o FST o f INTER q o SND o f) = prob (p o FST o f) * prob q)

INDEP_SDEST

|- indep SDEST

INDEP_SET_BASIC

|- !p. measurable p ==> indep_set {} p /\ indep_set UNIV p

INDEP_SET_DISJOINT_DECOMP

|- !p q r.
     indep_set p r /\ indep_set q r /\ (p INTER q = {}) ==>
     indep_set (p UNION q) r

INDEP_SET_LIST

|- !q l.
     alg_sorted l /\ alg_prefixfree l /\ measurable q /\
     (!x. MEM x l ==> indep_set (alg_embed x) q) ==>
     indep_set (algebra_embed l) q

INDEP_SET_SYM

|- !p q. indep_set p q = indep_set p q

INDEP_UNIT

|- !x. indep (UNIT x)

MAP_CONS_TL_FILTER

|- !l b.
     ~MEM [] l ==>
     (MAP (CONS b) (MAP TL (FILTER (\x. HD x = b) l)) =
      FILTER (\x. HD x = b) l)

PROB_INDEP_BOUND

|- !f n.
     indep f ==>
     (prob (\s. FST (f s) < SUC n) =
      prob (\s. FST (f s) < n) + prob (\s. FST (f s) = n))