open HolKernel Parse boolLib bossLib arithmeticTheory realTheory
     seqTheory pred_setTheory ind_typeTheory listTheory
     rich_listTheory pairTheory combinTheory realLib probTools
     boolean_sequenceTheory boolean_sequenceTools prob_extraTheory
     prob_extraTools prob_canonTheory prob_canonTools numSyntax;

val _ = new_theory "prob_algebra";

infixr 0 ++ << || ORELSEC ## -->;
infix 1 >> |->;
nonfix THEN ORELSE;

val op++ = op THEN;
val op<< = op THENL;
val op|| = op ORELSE;
val op>> = op THEN1;
val std_ss' = simpLib.++ (std_ss, boolSimps.ETA_ss);

(* ------------------------------------------------------------------------- *)
(* Definition of the embedding function from boolean list lists to boolean   *)
(* sequences.                                                                *)
(* ------------------------------------------------------------------------- *)

val alg_embed_def = Define `(alg_embed [] s = T)
  /\ (alg_embed (h::t) s = (h = SHD s) /\ alg_embed t (STL s))`;

val algebra_embed_def = Define `(algebra_embed [] = {})
  /\ (algebra_embed (h::t) = alg_embed h UNION algebra_embed t)`;

val measurable_def = Define `measurable s = (?b. s = algebra_embed b)`;

(* ------------------------------------------------------------------------- *)
(* Theorems leading to:                                                      *)
(* 1. algebra_embed (alg_canon b) = algebra_embed b                          *)
(* 2. (alg_canon b = alg_canon c) = (algebra_embed b = algebra_embed c)      *)
(* 3. measurable a ==> measurable (COMPL a)                                  *)
(* 4. measurable a /\ measurable b ==> measurable (a UNION b)                *)
(* 5. measurable a /\ measurable b ==> measurable (a INTER b)                *)
(* 6. measurable (a o STL) = measurable a                                    *)
(* 7. measurable (a o SDROP n) = measurable a                                *)
(* ------------------------------------------------------------------------- *)

val HALVES_INTER = store_thm
  ("HALVES_INTER",
   ``(\x. SHD x = T) INTER (\x. SHD x = F) = {}``,
   PSET_TAC []);

val INTER_STL = store_thm
  ("INTER_STL",
   ``!p q. (p INTER q) o STL = p o STL INTER q o STL``,
   PSET_TAC [o_DEF]);

val COMPL_SHD = store_thm
  ("COMPL_SHD",
   ``!b. COMPL (\x. SHD x = b) = (\x. SHD x = ~b)``,
   PSET_TAC []
   ++ Cases_on `b`
   ++ PROVE_TAC []);

val ALG_EMBED_BASIC = store_thm
  ("ALG_EMBED_BASIC",
   ``(alg_embed [] = UNIV)
     /\ (!h t. alg_embed (h::t) = (\x. SHD x = h) INTER alg_embed t o STL)``,
   PSET_TAC [o_DEF, alg_embed_def]
   ++ PROVE_TAC []);

val ALG_EMBED_NIL = store_thm
  ("ALG_EMBED_NIL",
   ``!c. (!x. alg_embed c x) = (c = [])``,
   Cases >> RW_TAC std_ss [alg_embed_def]
   ++ RW_TAC std_ss []
   ++ Q.EXISTS_TAC `SCONST (~h)`
   ++ RW_TAC std_ss [alg_embed_def, SHD_SCONST]
   ++ Cases_on `h`
   ++ RW_TAC std_ss []);

val ALG_EMBED_POPULATED = store_thm
  ("ALG_EMBED_POPULATED",
   ``!b. ?x. alg_embed b x``,
   Induct >> PROVE_TAC [alg_embed_def]
   ++ REWRITE_TAC [alg_embed_def]
   ++ POP_ASSUM MP_TAC
   ++ REPEAT STRIP_TAC
   ++ MP_TAC (SPECL [``h:bool``, ``x:num->bool``] SHD_STL_ISO)
   ++ STRIP_TAC
   ++ PROVE_TAC []);

val ALG_EMBED_PREFIX = store_thm
  ("ALG_EMBED_PREFIX",
   ``!b c s. alg_embed b s /\ alg_embed c s
             ==> IS_PREFIX b c \/ IS_PREFIX c b``,
   Induct >> RW_TAC list_ss [IS_PREFIX]
   ++ Cases_on `c` >> RW_TAC list_ss [IS_PREFIX]
   ++ RW_TAC list_ss [alg_embed_def, IS_PREFIX]
   ++ PROVE_TAC []);

val ALG_EMBED_PREFIX_SUBSET = store_thm
  ("ALG_EMBED_PREFIX_SUBSET",
   ``!b c. alg_embed b SUBSET alg_embed c = IS_PREFIX b c``,
   Induct
   >> (PSET_TAC []
       ++ RW_TAC list_ss [IS_PREFIX_NIL, alg_embed_def, ALG_EMBED_NIL])
   ++ PSET_TAC []
   ++ Cases_on `c` >> RW_TAC std_ss [alg_embed_def, IS_PREFIX]
   ++ RW_TAC std_ss [alg_embed_def, IS_PREFIX]
   ++ Q.PAT_ASSUM `!c. P c = Q c` (fn th => REWRITE_TAC [SYM (Q.SPEC `t` th)])
   ++ EQ_TAC <<
   [STRIP_TAC
    ++ KNOW_TAC `h = h'`
    >> (MP_TAC (Q.SPEC `b` ALG_EMBED_POPULATED)
        ++ STRIP_TAC
        ++ Q.PAT_ASSUM `!x. P x ==> Q x` (MP_TAC o Q.SPEC `SCONS h x`)
        ++ RW_TAC std_ss [SHD_SCONS, STL_SCONS])
    ++ RW_TAC std_ss []
    ++ Q.PAT_ASSUM `!x. P x ==> Q x` (MP_TAC o Q.SPEC `SCONS h x`)
    ++ RW_TAC std_ss [SHD_SCONS, STL_SCONS],
    RW_TAC std_ss []]);

val ALG_EMBED_TWINS = store_thm
  ("ALG_EMBED_TWINS",
   ``!l. alg_embed (SNOC T l) UNION alg_embed (SNOC F l) = alg_embed l``,
   Induct <<
   [PSET_TAC []
    ++ SEQ_CASES_TAC `v`
    ++ RW_TAC std_ss [SNOC, alg_embed_def, SHD_SCONS, STL_SCONS],
    RW_TAC std_ss [SNOC]
    ++ PSET_TAC [alg_embed_def]
    ++ SEQ_CASES_TAC `v`
    ++ POP_ASSUM (MP_TAC o Q.SPEC `t`)
    ++ RW_TAC std_ss [SHD_SCONS, STL_SCONS]
    ++ PROVE_TAC []]);

val ALGEBRA_EMBED_BASIC = store_thm
  ("ALGEBRA_EMBED_BASIC",
   ``(algebra_embed [] = {}) /\ (algebra_embed [[]] = UNIV)
     /\ (!b. algebra_embed [[b]] = (\s. SHD s = b))``,
   PSET_TAC [algebra_embed_def, alg_embed_def]
   ++ PROVE_TAC []);

val ALGEBRA_EMBED_MEM = store_thm
  ("ALGEBRA_EMBED_MEM",
   ``!b x. algebra_embed b x ==> (?l. MEM l b /\ alg_embed l x)``,
   Induct >> PSET_TAC [algebra_embed_def]
   ++ PSET_TAC [algebra_embed_def, MEM] <<
   [PROVE_TAC [],
    PROVE_TAC []]);

val ALGEBRA_EMBED_APPEND = store_thm
  ("ALGEBRA_EMBED_APPEND",
   ``!l1 l2. algebra_embed (APPEND l1 l2)
             = algebra_embed l1 UNION algebra_embed l2``,
   REPEAT STRIP_TAC
   ++ Induct_on `l1` >> PSET_TAC [APPEND, algebra_embed_def]
   ++ STRIP_TAC
   ++ POP_ASSUM MP_TAC
   ++ RW_TAC list_ss [algebra_embed_def]
   ++ PSET_TAC []
   ++ PROVE_TAC []);

val ALGEBRA_EMBED_TLS = store_thm
  ("ALGEBRA_EMBED_TLS",
   ``!l b. algebra_embed (MAP (CONS b) l) (SCONS h t)
           = (h = b) /\ algebra_embed l t``,
   REPEAT STRIP_TAC
   ++ Induct_on `l` >> PSET_TAC [MAP, algebra_embed_def]
   ++ STRIP_TAC
   ++ POP_ASSUM MP_TAC
   ++ PSET_TAC [MAP, algebra_embed_def, alg_embed_def, SHD_SCONS, STL_SCONS]
   ++ KILL_ALL_TAC
   ++ PROVE_TAC []);

val ALG_CANON_PREFS_EMBED = store_thm
  ("ALG_CANON_PREFS_EMBED",
   ``!l b. algebra_embed (alg_canon_prefs l b) = algebra_embed (l::b)``,
   STRIP_TAC
   ++ Induct >> RW_TAC list_ss [alg_canon_prefs_def]
   ++ RW_TAC list_ss [alg_canon_prefs_def]
   ++ PSET_TAC [algebra_embed_def]
   ++ SUFF_TAC `alg_embed h SUBSET alg_embed l`
   >> (PSET_TAC [] ++ PROVE_TAC [])
   ++ PROVE_TAC [ALG_EMBED_PREFIX_SUBSET]);

val ALG_CANON_FIND_EMBED = store_thm
  ("ALG_CANON_FIND_EMBED",
   ``!l b. algebra_embed (alg_canon_find l b) = algebra_embed (l::b)``,
   STRIP_TAC
   ++ Induct >> RW_TAC list_ss [alg_canon_find_def]
   ++ POP_ASSUM MP_TAC
   ++ BasicProvers.NORM_TAC list_ss [alg_canon_find_def, algebra_embed_def] <<
   [MP_TAC (Q.SPECL [`l`, `h`] ALG_EMBED_PREFIX_SUBSET)
    ++ PSET_TAC []
    ++ PROVE_TAC [],
    PSET_TAC [] ++ PROVE_TAC [],
    MP_TAC (Q.SPECL [`l`, `h::b`] ALG_CANON_PREFS_EMBED)
    ++ BasicProvers.NORM_TAC std_ss [algebra_embed_def]]);

val ALG_CANON1_EMBED = store_thm
  ("ALG_CANON1_EMBED",
   ``!l. algebra_embed (alg_canon1 l) = algebra_embed l``,
   REWRITE_TAC [alg_canon1_def]
   ++ Induct >> RW_TAC list_ss [FOLDR]
   ++ STRIP_TAC
   ++ POP_ASSUM MP_TAC
   ++ MP_TAC ALG_CANON_FIND_EMBED
   ++ RW_TAC list_ss [algebra_embed_def, FOLDR]);

val ALG_CANON_MERGE_EMBED = store_thm
  ("ALG_CANON_MERGE_EMBED",
   ``!l b. algebra_embed (alg_canon_merge l b) = algebra_embed (l::b)``,
   Induct_on `b` >> RW_TAC std_ss [alg_canon_merge_def]
   ++ RW_TAC list_ss [alg_canon_merge_def, alg_twin_def]
   ++ POP_ASSUM (K ALL_TAC)
   ++ RW_TAC std_ss [BUTLAST, algebra_embed_def]
   ++ MP_TAC (Q.SPEC `l'` ALG_EMBED_TWINS)
   ++ PSET_TAC []
   ++ PROVE_TAC []);

val ALG_CANON2_EMBED = store_thm
  ("ALG_CANON2_EMBED",
   ``!l. algebra_embed (alg_canon2 l) = algebra_embed l``,
   REWRITE_TAC [alg_canon2_def]
   ++ Induct >> RW_TAC list_ss [FOLDR]
   ++ STRIP_TAC
   ++ POP_ASSUM MP_TAC
   ++ MP_TAC ALG_CANON_MERGE_EMBED
   ++ RW_TAC list_ss [algebra_embed_def, FOLDR]);

val ALG_CANON_EMBED = store_thm
  ("ALG_CANON_EMBED",
   ``!l. algebra_embed (alg_canon l) = algebra_embed l``,
   RW_TAC std_ss [alg_canon_def, ALG_CANON1_EMBED, ALG_CANON2_EMBED]);

val ALGEBRA_CANON_UNIV = store_thm
  ("ALGEBRA_CANON_UNIV",
   ``!l. algebra_canon l ==> ((algebra_embed l = UNIV) ==> (l = [[]]))``,
   HO_MATCH_MP_TAC ALGEBRA_CANON_INDUCTION
   ++ RW_TAC std_ss []
   >> PSET_TAC [algebra_embed_def, FOLDR]
   ++ KNOW_TAC `(algebra_embed l = UNIV)`
   >> (POP_ASSUM MP_TAC
       ++ PSET_TAC [ALGEBRA_EMBED_APPEND]
       ++ POP_ASSUM (MP_TAC o Q.SPEC `SCONS T v`)
       ++ RW_TAC std_ss [ALGEBRA_EMBED_TLS])
   ++ KNOW_TAC `(algebra_embed l' = UNIV)`
   >> (Q.PAT_ASSUM `algebra_embed (APPEND X Y) = UNIV` MP_TAC
       ++ PSET_TAC [ALGEBRA_EMBED_APPEND]
       ++ POP_ASSUM (MP_TAC o Q.SPEC `SCONS F v`)
       ++ RW_TAC std_ss [ALGEBRA_EMBED_TLS])
   ++ RES_TAC
   ++ Q.PAT_ASSUM `algebra_canon (APPEND X Y)` MP_TAC
   ++ RW_TAC prob_canon_ss [algebra_canon_def]);

val ALG_CANON_REP = store_thm
  ("ALG_CANON_REP",
   ``!b c. (alg_canon b = alg_canon c)
           = (algebra_embed b = algebra_embed c)``,
   REPEAT STRIP_TAC
   ++ EQ_TAC >> PROVE_TAC [ALG_CANON_EMBED]
   ++ SUFF_TAC `!b. algebra_canon b ==> (!c. algebra_canon c ==>
                  (algebra_embed b = algebra_embed c) ==> (b = c))`
   >> (DISCH_THEN (MP_TAC o Q.SPEC `alg_canon b`)
       ++ RW_TAC std_ss [algebra_canon_def, ALG_CANON_IDEMPOT]
       ++ Q.PAT_ASSUM `!c. P c` (MP_TAC o Q.SPEC `alg_canon c`)
       ++ RW_TAC std_ss [ALG_CANON_IDEMPOT, ALG_CANON_EMBED])
   ++ HO_MATCH_MP_TAC ALGEBRA_CANON_INDUCTION
   ++ RW_TAC std_ss [] <<
   [Cases_on `c` >> RW_TAC std_ss []
    ++ PSET_TAC [algebra_embed_def, FOLDR]
    ++ PROVE_TAC [ALG_EMBED_POPULATED],
    PROVE_TAC [ALGEBRA_EMBED_BASIC, ALGEBRA_CANON_UNIV],
    NTAC 2 (POP_ASSUM MP_TAC)
    ++ Q.SPEC_TAC (`c`, `c`)
    ++ HO_MATCH_MP_TAC ALGEBRA_CANON_CASES
    ++ RW_TAC std_ss [] <<
    [POP_ASSUM MP_TAC
     ++ REVERSE (Cases_on `b`)
     >> (PSET_TAC [algebra_embed_def, FOLDR, APPEND, MAP]
         ++ PROVE_TAC [ALG_EMBED_POPULATED])
     ++ REVERSE (Cases_on `b'`)
     >> (PSET_TAC [algebra_embed_def, FOLDR, APPEND, MAP]
         ++ PROVE_TAC [ALG_EMBED_POPULATED])
     ++ RW_TAC list_ss [MAP],
     PROVE_TAC [ALGEBRA_EMBED_BASIC, ALGEBRA_CANON_UNIV],
     KNOW_TAC `algebra_embed b = algebra_embed l1`
     >> (POP_ASSUM MP_TAC
         ++ KILL_ALL_TAC
         ++ PSET_TAC [ALGEBRA_EMBED_APPEND]
         ++ POP_ASSUM (MP_TAC o Q.SPEC `SCONS T v`)
         ++ RW_TAC std_ss [ALGEBRA_EMBED_TLS])
     ++ KNOW_TAC `algebra_embed b' = algebra_embed l2`
     >> (POP_ASSUM (K ALL_TAC)
         ++ POP_ASSUM MP_TAC
         ++ KILL_ALL_TAC
         ++ PSET_TAC [ALGEBRA_EMBED_APPEND]
         ++ POP_ASSUM (MP_TAC o Q.SPEC `SCONS F v`)
         ++ RW_TAC std_ss [ALGEBRA_EMBED_TLS])
     ++ RES_TAC
     ++ RW_TAC std_ss []]]);

val ALGEBRA_CANON_EMBED_EMPTY = store_thm
  ("ALGEBRA_CANON_EMBED_EMPTY",
   ``!l. algebra_canon l ==> ((!v. ~algebra_embed l v) = (l = []))``,
   RW_TAC std_ss []
   ++ REVERSE EQ_TAC >> PSET_TAC [ALGEBRA_EMBED_BASIC]
   ++ RW_TAC std_ss []
   ++ SUFF_TAC `alg_canon l = alg_canon []`
   >> PROVE_TAC [algebra_canon_def, ALG_CANON_BASIC]
   ++ PSET_TAC [ALG_CANON_REP, ALGEBRA_EMBED_BASIC]);

val ALGEBRA_CANON_EMBED_UNIV = store_thm
  ("ALGEBRA_CANON_EMBED_UNIV",
   ``!l. algebra_canon l ==> ((!v. algebra_embed l v) = (l = [[]]))``,
   RW_TAC std_ss []
   ++ REVERSE EQ_TAC >> PSET_TAC [ALGEBRA_EMBED_BASIC]
   ++ RW_TAC std_ss []
   ++ SUFF_TAC `alg_canon l = alg_canon [[]]`
   >> PROVE_TAC [algebra_canon_def, ALG_CANON_BASIC]
   ++ PSET_TAC [ALG_CANON_REP, ALGEBRA_EMBED_BASIC]);

val MEASURABLE_ALGEBRA = store_thm
  ("MEASURABLE_ALGEBRA",
   ``!b. measurable (algebra_embed b)``,
   RW_TAC std_ss [measurable_def]
   ++ PROVE_TAC []);

val MEASURABLE_BASIC = store_thm
  ("MEASURABLE_BASIC",
   ``measurable {} /\ measurable UNIV /\ (!b. measurable (\s. SHD s = b))``,
   RW_TAC std_ss [measurable_def] <<
   [Q.EXISTS_TAC `[]`
    ++ RW_TAC std_ss [ALGEBRA_EMBED_BASIC],
    Q.EXISTS_TAC `[[]]`
    ++ RW_TAC std_ss [ALGEBRA_EMBED_BASIC],
    Q.EXISTS_TAC `[[b]]`
    ++ PSET_TAC [algebra_embed_def, alg_embed_def]
    ++ PROVE_TAC []]);

val MEASURABLE_SHD = store_thm
  ("MEASURABLE_SHD",
   ``!b. measurable (\s. SHD s = b)``,
   RW_TAC std_ss [MEASURABLE_BASIC]);

val ALGEBRA_EMBED_COMPL = store_thm
  ("ALGEBRA_EMBED_COMPL",
   ``!l. ?l'. COMPL (algebra_embed l) = algebra_embed l'``,
   STRIP_TAC
   ++ SUFF_TAC `!l. algebra_canon l ==>
                  (?l'. COMPL (algebra_embed l) = algebra_embed l')`
   >> (DISCH_THEN (MP_TAC o Q.SPEC `alg_canon l`)
       ++ RW_TAC std_ss [algebra_canon_def, ALG_CANON_EMBED, ALG_CANON_IDEMPOT])
   ++ HO_MATCH_MP_TAC ALGEBRA_CANON_INDUCTION
   ++ PSET_TAC [ALGEBRA_EMBED_BASIC] <<
   [Q.EXISTS_TAC `[[]]`
    ++ PSET_TAC [ALGEBRA_EMBED_BASIC],
    Q.EXISTS_TAC `[]`
    ++ PSET_TAC [ALGEBRA_EMBED_BASIC],
    Q.EXISTS_TAC `APPEND (MAP (CONS T) l'') (MAP (CONS F) l''')`
    ++ STRIP_TAC
    ++ SEQ_CASES_TAC `v`
    ++ PSET_TAC [ALGEBRA_EMBED_APPEND, ALGEBRA_EMBED_TLS]
    ++ PROVE_TAC []]);

val MEASURABLE_COMPL = store_thm
  ("MEASURABLE_COMPL",
   ``!s. measurable (COMPL s) = measurable s``,
   SUFF_TAC `!s. measurable s ==> measurable (COMPL s)`
   >> PROVE_TAC [COMPL_COMPL]
   ++ RW_TAC std_ss [measurable_def]
   ++ PROVE_TAC [ALGEBRA_EMBED_COMPL]);

val MEASURABLE_UNION = store_thm
  ("MEASURABLE_UNION",
   ``!s t. measurable s /\ measurable t ==> measurable (s UNION t)``,
   RW_TAC std_ss [measurable_def]
   ++ Q.EXISTS_TAC `APPEND b b'`
   ++ RW_TAC std_ss [ALGEBRA_EMBED_APPEND]);

val MEASURABLE_INTER = store_thm
  ("MEASURABLE_INTER",
   ``!s t. measurable s /\ measurable t ==> measurable (s INTER t)``,
   RW_TAC std_ss [INTER_UNION_COMPL, MEASURABLE_COMPL,
		  MEASURABLE_UNION]);

val MEASURABLE_STL = store_thm
  ("MEASURABLE_STL",
   ``!p. measurable (p o STL) = measurable p``,
   RW_TAC std_ss [measurable_def]
   ++ EQ_TAC <<
   [STRIP_TAC
    ++ POP_ASSUM MP_TAC
    ++ SUFF_TAC `!b. algebra_canon b ==>
                     (p o STL = algebra_embed b) ==>
		     ?b'. (p = algebra_embed b')`
     >> (DISCH_THEN (MP_TAC o Q.SPEC `alg_canon b`)
	 ++ RW_TAC std_ss [algebra_canon_def, ALG_CANON_IDEMPOT,
                           ALG_CANON_EMBED])
   ++ HO_MATCH_MP_TAC ALGEBRA_CANON_CASES
   ++ PSET_TAC [o_DEF, ALGEBRA_EMBED_BASIC] <<
   [Q.EXISTS_TAC `[]`
    ++ PSET_TAC [ALGEBRA_EMBED_BASIC]
    ++ POP_ASSUM (MP_TAC o Q.SPEC `SCONS T v`)
    ++ RW_TAC std_ss [STL_SCONS],
    Q.EXISTS_TAC `[[]]`
    ++ PSET_TAC [ALGEBRA_EMBED_BASIC]
    ++ POP_ASSUM (MP_TAC o Q.SPEC `SCONS T v`)
    ++ RW_TAC std_ss [STL_SCONS],
    Q.EXISTS_TAC `l1`
    ++ PSET_TAC [ALGEBRA_EMBED_APPEND]
    ++ POP_ASSUM (MP_TAC o Q.SPEC `SCONS T v`)
    ++ RW_TAC std_ss [STL_SCONS, ALGEBRA_EMBED_TLS]],
    PSET_TAC [o_DEF]
    ++ Q.EXISTS_TAC `APPEND (MAP (CONS T) b) (MAP (CONS F) b)`
    ++ PSET_TAC [ALGEBRA_EMBED_APPEND]
    ++ SEQ_CASES_TAC `v`
    ++ RW_TAC std_ss [STL_SCONS, ALGEBRA_EMBED_TLS]
    ++ PROVE_TAC []]);

val MEASURABLE_SDROP = store_thm
  ("MEASURABLE_SDROP",
   ``!n p. measurable (p o SDROP n) = measurable p``,
   Induct >> RW_TAC std_ss' [SDROP_def, o_DEF, I_THM]
   ++ RW_TAC bool_ss [SDROP_def, o_ASSOC, MEASURABLE_STL]);

val MEASURABLE_INTER_HALVES = store_thm
  ("MEASURABLE_INTER_HALVES",
   ``!p. measurable ((\x. SHD x = T) INTER p)
         /\ measurable ((\x. SHD x = F) INTER p) = measurable p``,
   STRIP_TAC
   ++ REVERSE EQ_TAC <<
   [REPEAT STRIP_TAC
    ++ MATCH_MP_TAC MEASURABLE_INTER
    ++ RW_TAC std_ss [MEASURABLE_BASIC],
    REPEAT STRIP_TAC
    ++ ONCE_REWRITE_TAC [(GSYM o Q.SPECL [`(\x. SHD x = T)`, `p`]
                          o INST_TYPE [alpha |-> (num --> bool)]) COMPL_SPLITS]
    ++ MATCH_MP_TAC MEASURABLE_UNION
    ++ PURE_ASM_REWRITE_TAC [COMPL_SHD]
    ++ PROVE_TAC []]);

val MEASURABLE_HALVES = store_thm
  ("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)``,
   REPEAT STRIP_TAC
   ++ REVERSE EQ_TAC <<
   [REPEAT STRIP_TAC
    ++ MATCH_MP_TAC MEASURABLE_UNION
    ++ RW_TAC std_ss [],
    REPEAT STRIP_TAC <<
    [SUFF_TAC `(\x. SHD x = T) INTER p = ((\x. SHD x = T) INTER
                 ((\x. SHD x = T) INTER p UNION (\x. SHD x = F) INTER q))`
     >> (DISCH_THEN (fn th => ONCE_REWRITE_TAC [th])
         ++ MATCH_MP_TAC MEASURABLE_INTER
         ++ RW_TAC std_ss [MEASURABLE_BASIC])
     ++ RW_TAC pset_ss []
     ++ PROVE_TAC [],
     SUFF_TAC `(\x. SHD x = F) INTER q = ((\x. SHD x = F) INTER
                 ((\x. SHD x = T) INTER p UNION (\x. SHD x = F) INTER q))`
     >> (DISCH_THEN (fn th => ONCE_REWRITE_TAC [th])
         ++ MATCH_MP_TAC MEASURABLE_INTER
         ++ RW_TAC std_ss [MEASURABLE_BASIC])
     ++ RW_TAC pset_ss []
     ++ PROVE_TAC []]]);

val MEASURABLE_INTER_SHD = store_thm
  ("MEASURABLE_INTER_SHD",
   ``!b p. measurable ((\x. SHD x = b) INTER p o STL) = measurable p``,
   RW_TAC std_ss []
   ++ REVERSE EQ_TAC <<
   [STRIP_TAC
    ++ MATCH_MP_TAC MEASURABLE_INTER
    ++ RW_TAC std_ss [MEASURABLE_BASIC, MEASURABLE_STL],
    PSET_TAC [measurable_def, o_DEF]
    ++ POP_ASSUM MP_TAC
    ++ SUFF_TAC `!b'. algebra_canon b' ==>
           (!v. (SHD v = b) /\ p (STL v) = algebra_embed b' v) ==>
           ?b. !v. p v = algebra_embed b v`
    >> (DISCH_THEN (MP_TAC o Q.SPEC `alg_canon b'`)
        ++ RW_TAC std_ss [ALG_CANON_EMBED, ALG_CANON_IDEMPOT,
                          algebra_canon_def])
    ++ HO_MATCH_MP_TAC ALGEBRA_CANON_CASES
    ++ REPEAT CONJ_TAC <<
    [PSET_TAC [ALGEBRA_EMBED_BASIC]
     ++ Q.EXISTS_TAC `[]`
     ++ STRIP_TAC
     ++ POP_ASSUM (MP_TAC o Q.SPEC `SCONS b v`)
     ++ PSET_TAC [ALGEBRA_EMBED_BASIC, SHD_SCONS, STL_SCONS],
     RW_TAC std_ss []
     ++ Q.EXISTS_TAC `[[]]`
     ++ STRIP_TAC
     ++ POP_ASSUM (MP_TAC o Q.SPEC `SCONS b v`)
     ++ PSET_TAC [ALGEBRA_EMBED_BASIC, SHD_SCONS, STL_SCONS],
     RW_TAC std_ss []
     ++ Q.EXISTS_TAC `if b then l1 else l2`
     ++ STRIP_TAC
     ++ POP_ASSUM (MP_TAC o Q.SPEC `SCONS b v`)
     ++ PSET_TAC [ALGEBRA_EMBED_APPEND, ALGEBRA_EMBED_TLS, SHD_SCONS,
                  STL_SCONS]]]);

val _ = export_theory ();