Theory: probAlgebra

Parents

• booleanSequence
• probCanon

Types

Constants

• algebra_embed  :bool list list -> (num -> bool) -> bool
• alg_embed  :bool list -> (num -> bool) -> bool
• measurable  :((num -> bool) -> bool) -> bool

Definitions

alg_embed_def

|- (!s. alg_embed [] s = T) /\
   !h t s. alg_embed (h::t) s = (h = SHD s) /\ alg_embed t (STL s)

algebra_embed_def

|- (algebra_embed [] = {}) /\
   !h t. algebra_embed (h::t) = alg_embed h UNION algebra_embed t

measurable_def

|- !s. measurable s = ?b. s = algebra_embed b

Theorems

ALG_CANON1_EMBED

|- !l. algebra_embed (alg_canon1 l) = algebra_embed l

ALG_CANON2_EMBED

|- !l. algebra_embed (alg_canon2 l) = algebra_embed l

ALG_CANON_EMBED

|- !l. algebra_embed (alg_canon l) = algebra_embed l

ALG_CANON_FIND_EMBED

|- !l b. algebra_embed (alg_canon_find l b) = algebra_embed (l::b)

ALG_CANON_MERGE_EMBED

|- !l b. algebra_embed (alg_canon_merge l b) = algebra_embed (l::b)

ALG_CANON_PREFS_EMBED

|- !l b. algebra_embed (alg_canon_prefs l b) = algebra_embed (l::b)

ALG_CANON_REP

|- !b c. (alg_canon b = alg_canon c) = (algebra_embed b = algebra_embed c)

ALG_EMBED_BASIC

|- (alg_embed [] = UNIV) /\
   !h t. alg_embed (h::t) = (\x. SHD x = h) INTER alg_embed t o STL

ALG_EMBED_NIL

|- !c. (!x. alg_embed c x) = (c = [])

ALG_EMBED_POPULATED

|- !b. ?x. alg_embed b x

ALG_EMBED_PREFIX

|- !b c s. alg_embed b s /\ alg_embed c s ==> IS_PREFIX b c \/ IS_PREFIX c b

ALG_EMBED_PREFIX_SUBSET

|- !b c. alg_embed b SUBSET alg_embed c = IS_PREFIX b c

ALG_EMBED_TWINS

|- !l. alg_embed (SNOC T l) UNION alg_embed (SNOC F l) = alg_embed l

ALGEBRA_CANON_EMBED_EMPTY

|- !l. algebra_canon l ==> ((!v. ~algebra_embed l v) = (l = []))

ALGEBRA_CANON_EMBED_UNIV

|- !l. algebra_canon l ==> ((!v. algebra_embed l v) = (l = [[]]))

ALGEBRA_CANON_UNIV

|- !l. algebra_canon l ==> (algebra_embed l = UNIV) ==> (l = [[]])

ALGEBRA_EMBED_APPEND

|- !l1 l2.
     algebra_embed (APPEND l1 l2) = algebra_embed l1 UNION algebra_embed l2

ALGEBRA_EMBED_BASIC

|- (algebra_embed [] = {}) /\ (algebra_embed [[]] = UNIV) /\
   !b. algebra_embed [[b]] = (\s. SHD s = b)

ALGEBRA_EMBED_COMPL

|- !l. ?l'. COMPL (algebra_embed l) = algebra_embed l'

ALGEBRA_EMBED_MEM

|- !b x. algebra_embed b x ==> ?l. MEM l b /\ alg_embed l x

ALGEBRA_EMBED_TLS

|- !l b.
     algebra_embed (MAP (CONS b) l) (SCONS h t) = (h = b) /\ algebra_embed l t

COMPL_SHD

|- !b. COMPL (\x. SHD x = b) = (\x. SHD x = ~b)

HALVES_INTER

|- (\x. SHD x = T) INTER (\x. SHD x = F) = {}

INTER_STL

|- !p q. (p INTER q) o STL = p o STL INTER q o STL

MEASURABLE_ALGEBRA

|- !b. measurable (algebra_embed b)

MEASURABLE_BASIC

|- measurable {} /\ measurable UNIV /\ !b. measurable (\s. SHD s = b)

MEASURABLE_COMPL

|- !s. measurable (COMPL s) = measurable s

MEASURABLE_HALVES

|- !p q.
     measurable ((\x. SHD x = T) INTER p UNION (\x. SHD x = F) INTER q) =
     measurable ((\x. SHD x = T) INTER p) /\
     measurable ((\x. SHD x = F) INTER q)

MEASURABLE_INTER

|- !s t. measurable s /\ measurable t ==> measurable (s INTER t)

MEASURABLE_INTER_HALVES

|- !p.
     measurable ((\x. SHD x = T) INTER p) /\
     measurable ((\x. SHD x = F) INTER p) =
     measurable p

MEASURABLE_INTER_SHD

|- !b p. measurable ((\x. SHD x = b) INTER p o STL) = measurable p

MEASURABLE_SDROP

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

MEASURABLE_SHD

|- !b. measurable (\s. SHD s = b)

MEASURABLE_STL

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

MEASURABLE_UNION

|- !s t. measurable s /\ measurable t ==> measurable (s UNION t)