1(* interactive mode 2loadPath := ["../ho_prover","../subtypes","../formalize"] @ !loadPath; 3app load 4 ["bossLib", "pred_setTheory", "listTheory", "rich_listTheory", 5 "pairTheory", "realLib", "HurdUseful", "extra_listTheory", 6 "measureTheory","probabilityTheory", 7 "sequenceTools","extra_pred_setTools","prob_canonTools"]; 8quietdec := true; 9*) 10 11open HolKernel Parse boolLib bossLib; 12 13open arithmeticTheory pred_setTheory listTheory rich_listTheory pairTheory 14 combinTheory numSyntax extra_pred_setTools 15 extra_listTheory HurdUseful realTheory extra_realTheory realLib 16 extra_numTheory seqTheory simpLib; 17 18open util_probTheory measureTheory probabilityTheory; 19open subtypeTheory extra_pred_setTheory; 20open sequenceTheory sequenceTools; 21open prob_canonTheory prob_canonTools; 22 23(* interactive mode 24quietdec := false; 25*) 26 27val _ = new_theory "prob_algebra"; 28 29val POP_ORW = POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]); 30val std_ss' = std_ss ++ boolSimps.ETA_ss; 31 32(* ------------------------------------------------------------------------- *) 33(* Definition of the embedding function from boolean list lists to boolean *) 34(* sequences. *) 35(* ------------------------------------------------------------------------- *) 36 37val halfspace_def = Define `halfspace (b : bool) = (\x. shd x = b)`; 38 39val mirror_def = Define `mirror (x :num -> bool) = scons (~shd x) (stl x)`; 40 41val prefix_set_def = Define 42 `(prefix_set [] = UNIV) /\ 43 (prefix_set (h :: t) = halfspace h INTER (prefix_set t o stl))`; 44 45val prefix_seq_def = Define `prefix_seq (h :: t) = scons h (prefix_seq t)`; 46 47val prob_embed_def = Define `prob_embed l = UNIONL (MAP prefix_set l)`; 48 49val prob_algebra_def = Define 50 `prob_algebra = (univ(:num -> bool), {s | ?b. s = prob_embed b})`; 51 52val prob_premeasure_def = Define 53 `(prob_premeasure ([] : bool list list) = (0 :real)) /\ 54 (prob_premeasure (l :: rest) = 55 (1 / 2) pow (LENGTH l) + prob_premeasure rest)`; 56 57val prob_measure_def = Define 58 `prob_measure s = 59 inf {r | ?c. (s = prob_embed c) /\ (prob_premeasure c = r)}`; 60 61val premeasurable_def = Define 62 `premeasurable a b = {f | algebra a /\ algebra b /\ 63 f IN (space a -> space b) /\ 64 !s. s IN subsets b ==> ((PREIMAGE f s)INTER(space a)) IN subsets a}`; 65 66val IN_PREMEASURABLE = store_thm 67 ("IN_PREMEASURABLE", 68 ``!a b f. f IN premeasurable a b = 69 algebra a /\ algebra b /\ 70 f IN (space a -> space b) /\ 71 (!s. s IN subsets b ==> (PREIMAGE f s) INTER (space a) IN subsets a)``, 72 RW_TAC std_ss [premeasurable_def, GSPECIFICATION]); 73 74val MEASURABLE_IMP_PREMEASURABLE = store_thm 75 ("MEASURABLE_IMP_PREMEASURABLE", ``!f a b. f IN measurable a b ==> f IN premeasurable a b``, 76 rpt GEN_TAC 77 >> RW_TAC std_ss [measurable_def, premeasurable_def, GSPECIFICATION, 78 SIGMA_ALGEBRA_ALGEBRA]); 79 80val MEASURABLE_IS_PREMEASURABLE = store_thm 81 ("MEASURABLE_IS_PREMEASURABLE", 82 ``!a b. sigma_algebra a /\ sigma_algebra b ==> (measurable a b = premeasurable a b)``, 83 rpt STRIP_TAC 84 >> RW_TAC std_ss [EXTENSION, measurable_def, premeasurable_def, GSPECIFICATION] 85 >> IMP_RES_TAC SIGMA_ALGEBRA_ALGEBRA 86 >> METIS_TAC []); 87 88val PREMEASURABLE_SIGMA = store_thm 89 ("PREMEASURABLE_SIGMA", 90 ``!f a b sp. 91 sigma_algebra a /\ subset_class sp b /\ f IN (space a -> sp) /\ 92 (!s. s IN b ==> (PREIMAGE f s) INTER (space a) IN subsets a) ==> 93 f IN premeasurable a (sigma sp b)``, 94 rpt STRIP_TAC 95 >> MATCH_MP_TAC MEASURABLE_IMP_PREMEASURABLE 96 >> RW_TAC std_ss [MEASURABLE_SIGMA]); 97 98val PREMEASURABLE_SUBSET = store_thm 99 ("PREMEASURABLE_SUBSET", 100 ``!a b. sigma_algebra a ==> 101 premeasurable a b SUBSET premeasurable a (sigma (space b) (subsets b))``, 102 RW_TAC std_ss [SUBSET_DEF] 103 >> MATCH_MP_TAC PREMEASURABLE_SIGMA 104 >> PROVE_TAC [IN_PREMEASURABLE, algebra_def]); 105 106val PREMEASURABLE_LIFT = store_thm 107 ("PREMEASURABLE_LIFT", 108 ``!f a b. 109 sigma_algebra a /\ f IN premeasurable a b ==> 110 f IN premeasurable a (sigma (space b) (subsets b))``, 111 PROVE_TAC [PREMEASURABLE_SUBSET, SUBSET_DEF]); 112 113val PREMEASURABLE_I = store_thm 114 ("PREMEASURABLE_I", 115 ``!a. algebra a ==> I IN premeasurable a a``, 116 RW_TAC std_ss [IN_PREMEASURABLE, I_THM, PREIMAGE_I, IN_FUNSET, 117 GSPEC_ID, SPACE, SUBSET_REFL] 118 >> Know `s INTER space a = s` 119 >- (FULL_SIMP_TAC std_ss [Once EXTENSION, algebra_def, IN_INTER, 120 subset_class_def, SUBSET_DEF] 121 >> METIS_TAC []) 122 >> RW_TAC std_ss []); 123 124val PREMEASURABLE_COMP = store_thm 125 ("PREMEASURABLE_COMP", 126 ``!f g a b c. 127 f IN premeasurable a b /\ g IN premeasurable b c ==> 128 (g o f) IN premeasurable a c``, 129 RW_TAC std_ss [IN_PREMEASURABLE, GSYM PREIMAGE_COMP, IN_FUNSET, 130 algebra_def, space_def, subsets_def, GSPECIFICATION] 131 >> `PREIMAGE f (PREIMAGE g s) INTER space a = 132 PREIMAGE f (PREIMAGE g s INTER space b) INTER space a` 133 by (RW_TAC std_ss [Once EXTENSION, IN_INTER, IN_PREIMAGE] >> METIS_TAC []) 134 >> METIS_TAC []); 135 136val prob_preserving_def = Define 137 `prob_preserving m1 m2 = 138 {f | 139 f IN premeasurable (m_space m1, measurable_sets m1) (m_space m2, measurable_sets m2) /\ 140 !s. 141 s IN measurable_sets m2 ==> 142 (measure m1 ((PREIMAGE f s)INTER(m_space m1)) = measure m2 s)}`; 143 144val PROB_PRESERVING = store_thm ( 145 "PROB_PRESERVING", 146 ``!p1 p2. 147 prob_preserving p1 p2 = 148 {f | 149 f IN premeasurable (p_space p1, events p1) (p_space p2, events p2) /\ 150 !s. s IN events p2 ==> (prob p1 ((PREIMAGE f s) INTER (p_space p1)) = prob p2 s)}``, 151 REPEAT GEN_TAC 152 >> REWRITE_TAC [EXTENSION] 153 >> GEN_TAC 154 >> REWRITE_TAC [GSPECIFICATION] 155 >> BETA_TAC 156 >> REWRITE_TAC [PAIR_EQ] 157 >> RW_TAC std_ss [prob_preserving_def, events_def, prob_def, p_space_def, GSPECIFICATION]); 158 159val IN_PROB_PRESERVING = store_thm 160 ("IN_PROB_PRESERVING", 161 ``!p1 p2 f. 162 f IN prob_preserving p1 p2 = 163 f IN premeasurable (p_space p1, events p1) (p_space p2, events p2) /\ 164 !s. s IN events p2 ==> (prob p1 ((PREIMAGE f s) INTER (p_space p1)) = prob p2 s)``, 165 RW_TAC std_ss [PROB_PRESERVING, GSPECIFICATION]); 166 167val PROB_SPACE_REDUCE = store_thm 168 ("PROB_SPACE_REDUCE", ``!p. (p_space p, events p, prob p) = p``, 169 Cases 170 >> Q.SPEC_TAC (`r`, `r`) 171 >> Cases 172 >> RW_TAC std_ss [p_space_def, events_def, prob_def, 173 m_space_def, measurable_sets_def, measure_def]); 174 175val ALGEBRA_REDUCE = store_thm 176 ("ALGEBRA_REDUCE", ``!a. algebra a ==> ((space a, subsets a) = a)``, 177 Cases >> RW_TAC std_ss [space_def, subsets_def]); 178 179val PROB_PRESERVING_LIFT = store_thm ( 180 "PROB_PRESERVING_LIFT", 181 ``!p1 p2 a f. 182 prob_space p1 /\ prob_space p2 /\ 183 (events p2 = subsets (sigma (p_space p2) a)) /\ 184 f IN prob_preserving p1 (p_space p2, a, prob p2) ==> 185 f IN prob_preserving p1 p2``, 186 RW_TAC std_ss [] 187 >> REVERSE (Cases_on `algebra (p_space p2, a)`) 188 >- ( Q.PAT_X_ASSUM `f IN P` 189 (ASSUME_TAC o (REWRITE_RULE [IN_PROB_PRESERVING, events_def, p_space_def, m_space_def, 190 measurable_sets_def, prob_def, measure_def])) \\ 191 POP_ASSUM (STRIP_ASSUME_TAC o (REWRITE_RULE [IN_PREMEASURABLE])) \\ 192 FULL_SIMP_TAC std_ss [p_space_def] ) 193 >> Suff `f IN prob_preserving p1 (p_space p2, events p2, prob p2)` 194 >- RW_TAC std_ss [PROB_SPACE_REDUCE] 195 >> ASM_REWRITE_TAC [] 196 >> Q.PAT_X_ASSUM `f IN X` MP_TAC 197 >> REWRITE_TAC [IN_PROB_PRESERVING, measurable_sets_def, measure_def, m_space_def, 198 p_space_def, events_def, prob_def] 199 >> STRIP_TAC 200 >> STRONG_CONJ_TAC 201 >- (REWRITE_TAC [SIGMA_REDUCE] 202 >> POP_ASSUM K_TAC 203 >> Know `(sigma (m_space p2) a) = sigma (space (m_space p2, a)) (subsets (m_space p2, a))` 204 >- RW_TAC std_ss [space_def, subsets_def] 205 >> STRIP_TAC >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 206 >> MATCH_MP_TAC PREMEASURABLE_LIFT 207 >> ASM_REWRITE_TAC [] 208 >> FULL_SIMP_TAC std_ss [prob_space_def, measure_space_def]) 209 >> Q.PAT_X_ASSUM `f IN X` K_TAC 210 >> REWRITE_TAC [IN_PREMEASURABLE, space_def, subsets_def] 211 >> STRIP_TAC 212 >> Suff `subsets (sigma (m_space p2) a) SUBSET 213 {s | measure p1 ((PREIMAGE f s) INTER (m_space p1)) = measure p2 s}` 214 >- RW_TAC std_ss [SUBSET_DEF, GSPECIFICATION] 215 >> MATCH_MP_TAC SIGMA_PROPERTY_DISJOINT 216 >> FULL_SIMP_TAC std_ss [p_space_def, prob_space_def, events_def] 217 >> RW_TAC std_ss [GSPECIFICATION, SUBSET_DEF, IN_INTER, IN_FUNSET, 218 IN_UNIV, PREIMAGE_COMPL, PREIMAGE_BIGUNION, IMAGE_IMAGE] >| (* 3 sub-goals here *) 219 [(* goal 1 (of 3) *) 220 Q.PAT_X_ASSUM `mersurable_sets p2 = subsets (sigma (m_space p2) a)` 221 (fn thm => FULL_SIMP_TAC std_ss [SYM thm]) 222 >> RW_TAC std_ss [MEASURE_COMPL] 223 >> Q.PAT_X_ASSUM `measure p1 (PREIMAGE f s INTER m_space p1) = measure p2 s` 224 (fn thm => ONCE_REWRITE_TAC [GSYM thm]) 225 >> Know `m_space p2 IN a` >- PROVE_TAC [ALGEBRA_SPACE, subsets_def, space_def] 226 >> STRIP_TAC 227 >> Q.PAT_X_ASSUM `measure p2 (m_space p2) = 1` K_TAC 228 >> Q.PAT_X_ASSUM `measure p1 (m_space p1) = 1` (REWRITE_TAC o wrap o SYM) 229 >> Know `PREIMAGE f (m_space p2) INTER m_space p1 = m_space p1` 230 >- (FULL_SIMP_TAC std_ss [Once EXTENSION, IN_INTER, IN_PREIMAGE, IN_FUNSET] >> METIS_TAC []) 231 >> RW_TAC std_ss [PREIMAGE_DIFF] 232 >> `((PREIMAGE f (m_space p2) DIFF PREIMAGE f s) INTER m_space p1) = 233 ((PREIMAGE f (m_space p2) INTER m_space p1) DIFF (PREIMAGE f s INTER m_space p1))` 234 by (RW_TAC std_ss [Once EXTENSION, IN_INTER, IN_DIFF, IN_PREIMAGE] >> DECIDE_TAC) 235 >> RW_TAC std_ss [MEASURE_COMPL], 236 (* goal 2 (of 3) *) 237 `BIGUNION (IMAGE (PREIMAGE f o f') UNIV) INTER m_space p1 = 238 BIGUNION (IMAGE (\x:num. (PREIMAGE f o f') x INTER m_space p1) UNIV)` 239 by (RW_TAC std_ss [Once EXTENSION, IN_BIGUNION, IN_INTER, IN_IMAGE, IN_UNIV] 240 >> FULL_SIMP_TAC std_ss [IN_FUNSET] 241 >> EQ_TAC 242 >- (RW_TAC std_ss [] >> Q.EXISTS_TAC `PREIMAGE f (f' x') INTER m_space p1` 243 >> ASM_REWRITE_TAC [IN_INTER] >> Q.EXISTS_TAC `x'` >> RW_TAC std_ss []) 244 >> RW_TAC std_ss [] >> METIS_TAC [IN_PREIMAGE, IN_INTER]) 245 >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 246 >> Suff 247 `(measure p2 o f') --> measure p2 (BIGUNION (IMAGE f' UNIV)) /\ 248 (measure p2 o f') --> 249 measure p1 (BIGUNION (IMAGE (\x. (PREIMAGE f o f') x INTER m_space p1) UNIV))` 250 >- PROVE_TAC [SEQ_UNIQ] 251 >> CONJ_TAC 252 >- (MATCH_MP_TAC MEASURE_COUNTABLE_INCREASING 253 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, SUBSET_DEF]) 254 >> Know `measure p2 o f' = measure p1 o (\x. (PREIMAGE f o f') x INTER m_space p1)` 255 >- (RW_TAC std_ss [FUN_EQ_THM] 256 >> RW_TAC std_ss [o_THM]) 257 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 258 >> MATCH_MP_TAC MEASURE_COUNTABLE_INCREASING 259 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, o_THM, PREIMAGE_EMPTY, INTER_EMPTY] 260 >> Suff `PREIMAGE f (f' n) SUBSET PREIMAGE f (f' (SUC n))` 261 >- RW_TAC std_ss [SUBSET_DEF, IN_INTER] 262 >> MATCH_MP_TAC PREIMAGE_SUBSET 263 >> RW_TAC std_ss [SUBSET_DEF], 264 (* goal 3 (of 3) *) 265 `BIGUNION (IMAGE (PREIMAGE f o f') UNIV) INTER m_space p1 = 266 BIGUNION (IMAGE (\x:num. (PREIMAGE f o f') x INTER m_space p1) UNIV)` 267 by (RW_TAC std_ss [Once EXTENSION, IN_BIGUNION, IN_INTER, IN_IMAGE, IN_UNIV] 268 >> FULL_SIMP_TAC std_ss [IN_FUNSET] 269 >> EQ_TAC 270 >- (RW_TAC std_ss [] >> Q.EXISTS_TAC `PREIMAGE f (f' x') INTER m_space p1` 271 >> ASM_REWRITE_TAC [IN_INTER] >> Q.EXISTS_TAC `x'` >> RW_TAC std_ss []) 272 >> RW_TAC std_ss [] >> METIS_TAC [IN_PREIMAGE, IN_INTER]) 273 >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 274 >> Suff 275 `(measure p2 o f') sums measure p2 (BIGUNION (IMAGE f' UNIV)) /\ 276 (measure p2 o f') sums 277 measure p1 (BIGUNION (IMAGE (\x. (PREIMAGE f o f') x INTER m_space p1) UNIV))` 278 >- PROVE_TAC [SUM_UNIQ] 279 >> CONJ_TAC 280 >- (MATCH_MP_TAC MEASURE_COUNTABLY_ADDITIVE 281 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV]) 282 >> Know `measure p2 o f' = measure p1 o (\x. (PREIMAGE f o f') x INTER m_space p1)` 283 >- (RW_TAC std_ss [FUN_EQ_THM] 284 >> RW_TAC std_ss [o_THM]) 285 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 286 >> MATCH_MP_TAC MEASURE_COUNTABLY_ADDITIVE 287 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, o_THM, IN_DISJOINT, PREIMAGE_DISJOINT, IN_INTER] 288 >> METIS_TAC [IN_DISJOINT, PREIMAGE_DISJOINT]]); 289 290val PROB_PRESERVING_SUBSET = store_thm ( 291 "PROB_PRESERVING_SUBSET", 292 ``!p1 p2 a. 293 prob_space p1 /\ prob_space p2 /\ 294 (events p2 = subsets (sigma (p_space p2) a)) ==> 295 prob_preserving p1 (p_space p2, a, prob p2) SUBSET 296 prob_preserving p1 p2``, 297 RW_TAC std_ss [SUBSET_DEF] 298 >> MATCH_MP_TAC PROB_PRESERVING_LIFT 299 >> PROVE_TAC []); 300 301val PREMEASURABLE_UP_LIFT = store_thm 302 ("PREMEASURABLE_UP_LIFT", 303 ``!sp a b c f. f IN premeasurable (sp, a) c /\ 304 algebra (sp, b) /\ a SUBSET b ==> f IN premeasurable (sp, b) c``, 305 RW_TAC std_ss [IN_PREMEASURABLE, GSPECIFICATION, SUBSET_DEF, IN_FUNSET, space_def, subsets_def]); 306 307val PREMEASURABLE_UP_SUBSET = store_thm 308 ("PREMEASURABLE_UP_SUBSET", 309 ``!sp a b c. a SUBSET b /\ algebra (sp, b) 310 ==> premeasurable (sp, a) c SUBSET premeasurable (sp, b) c``, 311 RW_TAC std_ss [PREMEASURABLE_UP_LIFT, SUBSET_DEF] 312 >> MATCH_MP_TAC PREMEASURABLE_UP_LIFT 313 >> Q.EXISTS_TAC `a` 314 >> ASM_REWRITE_TAC [SUBSET_DEF]); 315 316val PREMEASURABLE_UP_SIGMA = store_thm 317 ("PREMEASURABLE_UP_SIGMA", 318 ``!a b. premeasurable a b SUBSET premeasurable (sigma (space a) (subsets a)) b``, 319 RW_TAC std_ss [SUBSET_DEF, IN_PREMEASURABLE, space_def, subsets_def, SPACE_SIGMA] 320 >- ( MATCH_MP_TAC SIGMA_ALGEBRA_ALGEBRA \\ 321 MATCH_MP_TAC SIGMA_ALGEBRA_SIGMA >> FULL_SIMP_TAC std_ss [algebra_def]) 322 >> PROVE_TAC [SIGMA_SUBSET_SUBSETS, SUBSET_DEF]); 323 324val PROB_PRESERVING_UP_LIFT = store_thm ( 325 "PROB_PRESERVING_UP_LIFT", 326 ``!p1 p2 f a. 327 f IN prob_preserving (p_space p1, a, prob p1) p2 /\ 328 algebra (p_space p1, events p1) /\ 329 a SUBSET events p1 ==> 330 f IN prob_preserving p1 p2``, 331 RW_TAC std_ss [prob_preserving_def, GSPECIFICATION, SUBSET_DEF, events_def, p_space_def, 332 measure_def, measurable_sets_def, m_space_def, SPACE, prob_def] 333 >> MATCH_MP_TAC PREMEASURABLE_UP_LIFT 334 >> Q.EXISTS_TAC `a` 335 >> RW_TAC std_ss [SUBSET_DEF]); 336 337val PROB_PRESERVING_UP_SUBSET = store_thm ( 338 "PROB_PRESERVING_UP_SUBSET", 339 ``!p1 p2 a. 340 prob_space p1 /\ 341 a SUBSET events p1 /\ 342 algebra (p_space p1, events p1) ==> 343 prob_preserving (p_space p1, a, prob p1) p2 SUBSET prob_preserving p1 p2``, 344 RW_TAC std_ss [PROB_PRESERVING_UP_LIFT, SUBSET_DEF] 345 >> MATCH_MP_TAC PROB_PRESERVING_UP_LIFT 346 >> PROVE_TAC [SUBSET_DEF]); 347 348val PROB_PRESERVING_UP_SIGMA = store_thm ( 349 "PROB_PRESERVING_UP_SIGMA", 350 ``!p1 p2 a. 351 prob_space p1 /\ 352 (events p1 = subsets (sigma (p_space p1) a)) ==> 353 prob_preserving (p_space p1, a, prob p1) p2 SUBSET prob_preserving p1 p2``, 354 RW_TAC std_ss [PROB_PRESERVING_UP_LIFT, SUBSET_DEF] 355 >> MATCH_MP_TAC PROB_PRESERVING_UP_LIFT 356 >> ASM_REWRITE_TAC [SIGMA_SUBSET_SUBSETS, SIGMA_REDUCE] 357 >> FULL_SIMP_TAC std_ss [IN_PROB_PRESERVING, IN_PREMEASURABLE, p_space_def, 358 measurable_sets_def, space_def, subsets_def, prob_def, 359 events_def, measure_def, m_space_def] 360 >> Q.EXISTS_TAC `a` >> ASM_REWRITE_TAC [] 361 >> CONJ_TAC 362 >- ( MATCH_MP_TAC SIGMA_ALGEBRA_ALGEBRA \\ 363 MATCH_MP_TAC SIGMA_ALGEBRA_SIGMA \\ 364 Q.PAT_X_ASSUM `algebra (m_space p2, measurable_sets p2)` K_TAC \\ 365 Q.PAT_X_ASSUM `algebra (m_space p1, a)` MP_TAC \\ 366 RW_TAC std_ss [algebra_def, space_def, subsets_def] ) 367 >> KILL_TAC 368 >> REWRITE_TAC [SUBSET_DEF, IN_SIGMA]); 369 370(* ------------------------------------------------------------------------- *) 371(* Theorems leading to: *) 372(* 1. prob_embed (prob_canon b) = prob_embed b *) 373(* 2. (prob_canon b = prob_canon c) = (prob_embed b = prob_embed c) *) 374(* 3. algebra prob_algebra *) 375(* 4. (a o stl) IN prob_algebra = a IN prob_algebra *) 376(* 5. (a o sdrop n) IN prob_algebra = a IN prob_algebra *) 377(* 6. prob_premeasure (prob_canon b) <= prob_premeasure b *) 378(* 7. prob_measure (prob_embed b) = prob_premeasure (prob_canon b) *) 379(* 8. positive (prob_algebra, prob_measure) *) 380(* 9. additive (prob_algebra, prob_measure) *) 381(* 10. countably_additive (prob_algebra, prob_measure) *) 382(* 11. a IN prob_algebra ==> prob_measure (a o stl) = prob_measure a *) 383(* 12. a IN prob_algebra ==> prob_measure (a o sdrop n) = prob_measure a *) 384(* ------------------------------------------------------------------------- *) 385 386val IN_HALFSPACE = store_thm 387 ("IN_HALFSPACE", 388 ``!x b. x IN halfspace b = (shd x = b)``, 389 RW_TAC std_ss [halfspace_def, SPECIFICATION]); 390 391val COMPL_HALFSPACE = store_thm 392 ("COMPL_HALFSPACE", 393 ``!b. COMPL (halfspace b) = halfspace (~b)``, 394 PSET_TAC [IN_HALFSPACE, EXTENSION] 395 >> Cases_on `b` 396 >> PROVE_TAC []); 397 398val HALFSPACE_INTER = store_thm 399 ("HALFSPACE_INTER", 400 ``!b. halfspace T INTER halfspace F = {}``, 401 PSET_TAC [IN_HALFSPACE, EXTENSION]); 402 403val HALFSPACE_UNION = store_thm 404 ("HALFSPACE_UNION", 405 ``!b. halfspace T UNION halfspace F = UNIV``, 406 PSET_TAC [IN_HALFSPACE, EXTENSION]); 407 408val PREFIX_SET_BASIC = store_thm 409 ("PREFIX_SET_BASIC", 410 ``(prefix_set [] = UNIV) /\ (prefix_set [h] = halfspace h)``, 411 PSET_TAC [prefix_set_def, IN_HALFSPACE, EXTENSION]); 412 413val PREFIX_SET_SCONS = store_thm 414 ("PREFIX_SET_SCONS", 415 ``!h t x xs. 416 scons h t IN prefix_set (x :: xs) = (h = x) /\ t IN prefix_set xs``, 417 PSET_TAC [prefix_set_def, IN_HALFSPACE, SHD_SCONS, STL_SCONS, EXTENSION]); 418 419val PREFIX_SET_NIL = store_thm 420 ("PREFIX_SET_NIL", 421 ``!l. (prefix_set l = UNIV) = (l = [])``, 422 Cases >- RW_TAC std_ss [prefix_set_def] 423 >> RW_TAC std_ss [EXTENSION, IN_UNIV] 424 >> Q.EXISTS_TAC `sconst (~h)` 425 >> RW_TAC std_ss [prefix_set_def] 426 >> Cases_on `h` 427 >> RW_TAC std_ss [IN_HALFSPACE, IN_INTER, SHD_SCONST]); 428 429val PREFIX_SET_NONEMPTY = store_thm 430 ("PREFIX_SET_NONEMPTY", 431 ``!b. ~(prefix_set b = {})``, 432 Induct >- PSET_TAC [prefix_set_def, EXTENSION] 433 >> PSET_TAC [prefix_set_def, EXTENSION] 434 >> Q.EXISTS_TAC `scons h x` 435 >> PSET_TAC [IN_HALFSPACE, SHD_SCONS, IN_o, STL_SCONS]); 436 437val PREFIX_SET_POPULATED = store_thm 438 ("PREFIX_SET_POPULATED", 439 ``!b. ?x. x IN prefix_set b``, 440 STRIP_TAC 441 >> MP_TAC (Q.SPEC `b` PREFIX_SET_NONEMPTY) 442 >> PSET_TAC [EXTENSION]); 443 444val PREFIX_SET_PREFIX_SUBSET = store_thm 445 ("PREFIX_SET_PREFIX_SUBSET", 446 ``!b c. prefix_set b SUBSET prefix_set c = IS_PREFIX b c``, 447 Induct 448 >- PSET_TAC [prefix_set_def, IS_PREFIX_NIL, GSYM PREFIX_SET_NIL, EXTENSION] 449 >> Cases_on `c` 450 >- PSET_TAC [prefix_set_def, IS_PREFIX_NIL, GSYM PREFIX_SET_NIL, EXTENSION] 451 >> PSET_TAC [prefix_set_def, IS_PREFIX, IN_HALFSPACE, EXTENSION] 452 >> Q.PAT_X_ASSUM `!c. P c = Q c` (fn th => REWRITE_TAC [SYM (Q.SPEC `t` th)]) 453 >> REVERSE EQ_TAC >- RW_TAC std_ss [] 454 >> STRIP_TAC 455 >> REVERSE STRONG_CONJ_TAC 456 >- (RW_TAC std_ss [] 457 >> Q.PAT_X_ASSUM `!x. P x ==> Q x` (MP_TAC o Q.SPEC `scons h x`) 458 >> RW_TAC std_ss [SHD_SCONS, STL_SCONS]) 459 >> Suff `?x. (shd x = h') /\ stl x IN prefix_set b` 460 >- PROVE_TAC [] 461 >> KILL_TAC 462 >> MP_TAC (Q.SPEC `b` PREFIX_SET_NONEMPTY) 463 >> PSET_TAC [EXTENSION] 464 >> Q.EXISTS_TAC `scons h' x` 465 >> RW_TAC std_ss [SHD_SCONS, STL_SCONS]); 466 467val PREFIX_SET_SUBSET = store_thm 468 ("PREFIX_SET_SUBSET", 469 ``!b c. 470 DISJOINT (prefix_set b) (prefix_set c) \/ 471 (prefix_set b) SUBSET (prefix_set c) \/ 472 (prefix_set c) SUBSET (prefix_set b)``, 473 REWRITE_TAC [PREFIX_SET_PREFIX_SUBSET] 474 >> Induct >- PSET_TAC [IS_PREFIX, EXTENSION] 475 >> Cases_on `c` >- PSET_TAC [IS_PREFIX, EXTENSION] 476 >> PSET_TAC [IS_PREFIX, prefix_set_def, IN_HALFSPACE, EXTENSION] 477 >> POP_ASSUM (MP_TAC o Q.SPEC `t`) 478 >> CONV_TAC (REDEPTH_CONV (LEFT_OR_FORALL_CONV ORELSEC RIGHT_OR_FORALL_CONV)) 479 >> Cases_on `h` 480 >> Cases_on `h'` 481 >> RW_TAC std_ss [OR_CLAUSES, GSYM DISJ_ASSOC] 482 >> POP_ASSUM (MP_TAC o Q.SPEC `stl x`) 483 >> PROVE_TAC []); 484 485val PREFIX_SET_TWINS = store_thm 486 ("PREFIX_SET_TWINS", 487 ``!l. prefix_set (SNOC T l) UNION prefix_set (SNOC F l) = prefix_set l``, 488 Induct >- PSET_TAC [SNOC, prefix_set_def, IN_HALFSPACE, EXTENSION] 489 >> PSET_TAC [SNOC, prefix_set_def, IN_HALFSPACE, EXTENSION] 490 >> PROVE_TAC []); 491 492val PREFIX_SEQ = store_thm 493 ("PREFIX_SEQ", 494 ``!l. prefix_seq l IN prefix_set l``, 495 Induct >- RW_TAC std_ss [prefix_set_def, IN_UNIV] 496 >> RW_TAC std_ss [prefix_set_def, prefix_seq_def, IN_INTER, IN_HALFSPACE, 497 SHD_SCONS, GSYM PREIMAGE_ALT, IN_PREIMAGE, STL_SCONS]); 498 499val IN_PROB_EMBED = store_thm 500 ("IN_PROB_EMBED", 501 ``!b. x IN prob_embed b = (?l. MEM l b /\ x IN prefix_set l)``, 502 RW_TAC std_ss [prob_embed_def, IN_UNIONL, MEM_MAP] 503 >> PROVE_TAC []); 504 505val PROB_EMBED_BASIC = store_thm 506 ("PROB_EMBED_BASIC", 507 ``(prob_embed [] = {}) /\ (prob_embed [[]] = UNIV) /\ 508 (!b. prob_embed [[b]] = halfspace b)``, 509 PSET_TAC [prob_embed_def, prefix_set_def, IN_PROB_EMBED, MEM, EXTENSION]); 510 511val PROB_EMBED_NIL = store_thm 512 ("PROB_EMBED_NIL", 513 ``prob_embed [] = {}``, 514 PSET_TAC [prob_embed_def, MAP_MEM, MEM, EXTENSION]); 515 516val PROB_EMBED_CONS = store_thm 517 ("PROB_EMBED_CONS", 518 ``!x xs. prob_embed (x :: xs) = prefix_set x UNION prob_embed xs``, 519 PSET_TAC [prob_embed_def, MAP_MEM, MEM, EXTENSION] 520 >> PROVE_TAC []); 521 522val PROB_EMBED_TRANSPOSE = store_thm 523 ("PROB_EMBED_TRANSPOSE", 524 ``!x y z. prob_embed (x :: y :: z) = prob_embed (y :: x :: z)``, 525 PSET_TAC [PROB_EMBED_CONS, EXTENSION] 526 >> PROVE_TAC []); 527 528val PROB_EMBED_APPEND = store_thm 529 ("PROB_EMBED_APPEND", 530 ``!l1 l2. 531 prob_embed (APPEND l1 l2) = prob_embed l1 UNION prob_embed l2``, 532 PSET_TAC [IN_PROB_EMBED, APPEND_MEM, EXTENSION] 533 >> PROVE_TAC []); 534 535val PROB_EMBED_TLS = store_thm 536 ("PROB_EMBED_TLS", 537 ``!l b. 538 (scons h t) IN prob_embed (MAP (CONS b) l) = 539 (h = b) /\ t IN prob_embed l``, 540 PSET_TAC [IN_PROB_EMBED, MAP_MEM, EXTENSION] 541 >> EQ_TAC 542 >- (PSET_TAC [PREFIX_SET_SCONS, EXTENSION] 543 >> PROVE_TAC []) 544 >> RW_TAC std_ss [] 545 >> Q.EXISTS_TAC `b :: l'` 546 >> PSET_TAC [PREFIX_SET_SCONS, EXTENSION]); 547 548val PROB_CANON_PREFS_EMBED = store_thm 549 ("PROB_CANON_PREFS_EMBED", 550 ``!l b. prob_embed (prob_canon_prefs l b) = prob_embed (l :: b)``, 551 STRIP_TAC 552 >> Induct >- RW_TAC list_ss [prob_canon_prefs_def] 553 >> RW_TAC list_ss [prob_canon_prefs_def] 554 >> PSET_TAC [prob_embed_def, MAP_MEM, MEM, GSYM PREFIX_SET_PREFIX_SUBSET, 555 EXTENSION] 556 >> Q.PAT_X_ASSUM `!x. P x = Q x` K_TAC 557 >> EQ_TAC >- PROVE_TAC [] 558 >> RW_TAC std_ss [] 559 >> PROVE_TAC []); 560 561val PROB_CANON_FIND_EMBED = store_thm 562 ("PROB_CANON_FIND_EMBED", 563 ``!l b. prob_embed (prob_canon_find l b) = prob_embed (l :: b)``, 564 STRIP_TAC 565 >> Induct >- RW_TAC list_ss [prob_canon_find_def] 566 >> PSET_TAC [prob_canon_find_def, GSYM PREFIX_SET_PREFIX_SUBSET, 567 EXTENSION] >| 568 [Q.PAT_X_ASSUM `!x. P x = Q x` K_TAC 569 >> PSET_TAC [PROB_EMBED_CONS, EXTENSION] 570 >> PROVE_TAC [], 571 ONCE_REWRITE_TAC [PROB_EMBED_TRANSPOSE] 572 >> ONCE_REWRITE_TAC [PROB_EMBED_CONS] 573 >> PSET_TAC [EXTENSION], 574 PSET_TAC [PROB_CANON_PREFS_EMBED, EXTENSION]]); 575 576val PROB_CANON1_EMBED = store_thm 577 ("PROB_CANON1_EMBED", 578 ``!l. prob_embed (prob_canon1 l) = prob_embed l``, 579 REWRITE_TAC [prob_canon1_def] 580 >> Induct >- RW_TAC list_ss [FOLDR] 581 >> STRIP_TAC 582 >> POP_ASSUM MP_TAC 583 >> MP_TAC PROB_CANON_FIND_EMBED 584 >> RW_TAC list_ss [PROB_EMBED_CONS, FOLDR]); 585 586val PROB_CANON_MERGE_EMBED = store_thm 587 ("PROB_CANON_MERGE_EMBED", 588 ``!l b. prob_embed (prob_canon_merge l b) = prob_embed (l :: b)``, 589 Induct_on `b` >- RW_TAC std_ss [prob_canon_merge_def] 590 >> RW_TAC list_ss [prob_canon_merge_def, prob_twin_def] 591 >> POP_ASSUM (K ALL_TAC) 592 >> RW_TAC std_ss [BUTLAST, PROB_EMBED_CONS] 593 >> MP_TAC (Q.SPEC `l'` PREFIX_SET_TWINS) 594 >> PSET_TAC [EXTENSION] 595 >> PROVE_TAC []); 596 597val PROB_CANON2_EMBED = store_thm 598 ("PROB_CANON2_EMBED", 599 ``!l. prob_embed (prob_canon2 l) = prob_embed l``, 600 REWRITE_TAC [prob_canon2_def] 601 >> Induct >- RW_TAC list_ss [FOLDR] 602 >> STRIP_TAC 603 >> POP_ASSUM MP_TAC 604 >> MP_TAC PROB_CANON_MERGE_EMBED 605 >> RW_TAC list_ss [PROB_EMBED_CONS, FOLDR]); 606 607val PROB_CANON_EMBED = store_thm 608 ("PROB_CANON_EMBED", 609 ``!l. prob_embed (prob_canon l) = prob_embed l``, 610 RW_TAC std_ss [prob_canon_def, PROB_CANON1_EMBED, PROB_CANON2_EMBED]); 611 612val PROB_CANONICAL_UNIV = store_thm 613 ("PROB_CANONICAL_UNIV", 614 ``!l. prob_canonical l /\ (prob_embed l = UNIV) ==> (l = [[]])``, 615 Suff `!l. prob_canonical l ==> (prob_embed l = UNIV) ==> (l = [[]])` 616 >- PROVE_TAC [] 617 >> HO_MATCH_MP_TAC PROB_CANONICAL_INDUCT 618 >> PSET_TAC [PROB_EMBED_BASIC, EXTENSION] 619 >> Suff `F` >- PROVE_TAC [] 620 >> Q.PAT_X_ASSUM `prob_canonical x` MP_TAC 621 >> Suff `(l = [[]]) /\ (l' = [[]])` 622 >- RW_TAC prob_canon_ss [prob_canonical_def] 623 >> CONJ_TAC >| 624 [Q.PAT_X_ASSUM `x ==> (l = y)` MATCH_MP_TAC 625 >> PSET_TAC [EXTENSION] 626 >> POP_ASSUM (MP_TAC o Q.SPEC `scons T x`) 627 >> PSET_TAC [PROB_EMBED_TLS, PROB_EMBED_APPEND, EXTENSION], 628 Q.PAT_X_ASSUM `x ==> (l' = y)` MATCH_MP_TAC 629 >> PSET_TAC [EXTENSION] 630 >> POP_ASSUM (MP_TAC o Q.SPEC `scons F x`) 631 >> PSET_TAC [PROB_EMBED_TLS, PROB_EMBED_APPEND, EXTENSION]]); 632 633val PROB_CANON_REP = store_thm 634 ("PROB_CANON_REP", 635 ``!b c. 636 (prob_canon b = prob_canon c) = (prob_embed b = prob_embed c)``, 637 REPEAT STRIP_TAC 638 >> EQ_TAC >- PROVE_TAC [PROB_CANON_EMBED] 639 >> Suff `!b. prob_canonical b ==> (!c. prob_canonical c ==> 640 (prob_embed b = prob_embed c) ==> (b = c))` 641 >- (DISCH_THEN (MP_TAC o Q.SPEC `prob_canon b`) 642 >> RW_TAC std_ss [prob_canonical_def, PROB_CANON_IDEMPOT] 643 >> Q.PAT_X_ASSUM `!c. P c` (MP_TAC o Q.SPEC `prob_canon c`) 644 >> RW_TAC std_ss [PROB_CANON_IDEMPOT, PROB_CANON_EMBED]) 645 >> HO_MATCH_MP_TAC PROB_CANONICAL_INDUCT 646 >> CONJ_TAC 647 >- (Cases >- RW_TAC std_ss [] 648 >> PSET_TAC [PROB_EMBED_NIL, PROB_EMBED_CONS, FOLDR, EXTENSION] 649 >> PROVE_TAC [PREFIX_SET_POPULATED]) 650 >> CONJ_TAC >- PROVE_TAC [PROB_EMBED_BASIC, PROB_CANONICAL_UNIV] 651 >> RW_TAC std_ss [] 652 >> NTAC 2 (POP_ASSUM MP_TAC) 653 >> Q.SPEC_TAC (`c`, `c`) 654 >> HO_MATCH_MP_TAC PROB_CANONICAL_CASES 655 >> CONJ_TAC 656 >- (PSET_TAC [PROB_EMBED_NIL, PROB_EMBED_CONS, FOLDR, EXTENSION] 657 >> REVERSE (Cases_on `b`) 658 >- (PSET_TAC [PROB_EMBED_NIL, FOLDR, APPEND, MAP, PROB_EMBED_CONS, 659 EXTENSION] 660 >> PROVE_TAC [PREFIX_SET_POPULATED]) 661 >> REVERSE (Cases_on `b'`) 662 >- (PSET_TAC [PROB_EMBED_NIL, FOLDR, APPEND, MAP, PROB_EMBED_CONS, 663 EXTENSION] 664 >> PROVE_TAC [PREFIX_SET_POPULATED]) 665 >> RW_TAC list_ss [MAP]) 666 >> CONJ_TAC >- PROVE_TAC [PROB_EMBED_BASIC, PROB_CANONICAL_UNIV] 667 >> RW_TAC std_ss [] 668 >> Suff `(b = l1) /\ (b' = l2)` >- RW_TAC std_ss [] 669 >> CONJ_TAC >| 670 [Suff `prob_embed b = prob_embed l1` >- PROVE_TAC [] 671 >> POP_ASSUM MP_TAC 672 >> KILL_TAC 673 >> PSET_TAC [PROB_EMBED_APPEND, EXTENSION] 674 >> POP_ASSUM (MP_TAC o Q.SPEC `scons T x`) 675 >> RW_TAC std_ss [PROB_EMBED_TLS], 676 Suff `prob_embed b' = prob_embed l2` >- PROVE_TAC [] 677 >> POP_ASSUM MP_TAC 678 >> KILL_TAC 679 >> PSET_TAC [PROB_EMBED_APPEND, EXTENSION] 680 >> POP_ASSUM (MP_TAC o Q.SPEC `scons F x`) 681 >> RW_TAC std_ss [PROB_EMBED_TLS]]); 682 683val PROB_CANONICAL_EMBED_EMPTY = store_thm 684 ("PROB_CANONICAL_EMBED_EMPTY", 685 ``!l. prob_canonical l ==> ((prob_embed l = {}) = (l = []))``, 686 RW_TAC std_ss [] 687 >> REVERSE EQ_TAC >- PSET_TAC [PROB_EMBED_BASIC, EXTENSION] 688 >> RW_TAC std_ss [] 689 >> Suff `prob_canon l = prob_canon []` 690 >- PROVE_TAC [prob_canonical_def, PROB_CANON_BASIC] 691 >> PSET_TAC [PROB_CANON_REP, PROB_EMBED_BASIC, EXTENSION]); 692 693val PROB_CANONICAL_EMBED_UNIV = store_thm 694 ("PROB_CANONICAL_EMBED_UNIV", 695 ``!l. prob_canonical l ==> ((prob_embed l = UNIV) = (l = [[]]))``, 696 RW_TAC std_ss [] 697 >> REVERSE EQ_TAC >- PSET_TAC [PROB_EMBED_BASIC, EXTENSION] 698 >> RW_TAC std_ss [] 699 >> Suff `prob_canon l = prob_canon [[]]` 700 >- PROVE_TAC [prob_canonical_def, PROB_CANON_BASIC] 701 >> PSET_TAC [PROB_CANON_REP, PROB_EMBED_BASIC, EXTENSION]); 702 703val IN_PROB_ALGEBRA = store_thm 704 ("IN_PROB_ALGEBRA", 705 ``!x. x IN (subsets prob_algebra) = (?b. x = prob_embed b)``, 706 RW_TAC std_ss [prob_algebra_def, subsets_def, GSPECIFICATION]); 707 708val PROB_EMBED_ALGEBRA = store_thm 709 ("PROB_EMBED_ALGEBRA", 710 ``!b. (prob_embed b) IN (subsets prob_algebra)``, 711 PROVE_TAC [IN_PROB_ALGEBRA, subsets_def]); 712 713val SPACE_PROB_ALGEBRA = store_thm 714 ("SPACE_PROB_ALGEBRA", ``space prob_algebra = UNIV``, 715 PROVE_TAC [prob_algebra_def, space_def]); 716 717val SPACE_SUBSETS_PROB_ALGEBRA = store_thm 718 ("SPACE_SUBSETS_PROB_ALGEBRA", 719 ``(space prob_algebra, subsets prob_algebra) = prob_algebra``, 720 REWRITE_TAC [prob_algebra_def, space_def, subsets_def]); 721 722val PROB_ALGEBRA_EMPTY = store_thm 723 ("PROB_ALGEBRA_EMPTY", 724 ``{} IN (subsets prob_algebra)``, 725 PROVE_TAC [IN_PROB_ALGEBRA, PROB_EMBED_BASIC, subsets_def]); 726 727val PROB_ALGEBRA_UNION = store_thm 728 ("PROB_ALGEBRA_UNION", 729 ``!s t. s IN (subsets prob_algebra) /\ t IN (subsets prob_algebra) 730 ==> (s UNION t) IN (subsets prob_algebra)``, 731 PSET_TAC [IN_PROB_ALGEBRA, EXTENSION, subsets_def] 732 >> Q.EXISTS_TAC `APPEND b b'` 733 >> PSET_TAC [PROB_EMBED_APPEND, EXTENSION]); 734 735val PROB_ALGEBRA_COMPL = store_thm 736 ("PROB_ALGEBRA_COMPL", 737 ``!s. s IN (subsets prob_algebra) ==> COMPL s IN (subsets prob_algebra)``, 738 PSET_TAC [IN_PROB_ALGEBRA, EXTENSION, subsets_def] 739 >> POP_ASSUM MP_TAC 740 >> Suff `!l. prob_canonical l ==> 741 (?l'. COMPL (prob_embed l) = prob_embed l')` 742 >- (DISCH_THEN (MP_TAC o Q.SPEC `prob_canon b`) 743 >> PSET_TAC [prob_canonical_def, PROB_CANON_EMBED, PROB_CANON_IDEMPOT, 744 EXTENSION]) 745 >> HO_MATCH_MP_TAC PROB_CANONICAL_INDUCT 746 >> CONJ_TAC 747 >- (Q.EXISTS_TAC `[[]]` 748 >> PSET_TAC [PROB_EMBED_BASIC, EXTENSION]) 749 >> CONJ_TAC 750 >- (Q.EXISTS_TAC `[]` 751 >> PSET_TAC [PROB_EMBED_BASIC, EXTENSION]) 752 >> PSET_TAC [EXTENSION] 753 >> Q.EXISTS_TAC `APPEND (MAP (CONS T) l'') (MAP (CONS F) l''')` 754 >> STRIP_TAC 755 >> SEQ_CASES_TAC `x` 756 >> PSET_TAC [PROB_EMBED_APPEND, PROB_EMBED_TLS, EXTENSION] 757 >> PROVE_TAC []); 758 759val PROB_ALGEBRA_UNIV = store_thm 760 ("PROB_ALGEBRA_UNIV", ``UNIV IN (subsets prob_algebra)``, 761 REWRITE_TAC [GSYM COMPL_EMPTY] 762 >> PROVE_TAC [PROB_ALGEBRA_COMPL, PROB_ALGEBRA_EMPTY, subsets_def]); 763 764val PROB_ALGEBRA_ALGEBRA = store_thm 765 ("PROB_ALGEBRA_ALGEBRA", ``algebra prob_algebra``, 766 RW_TAC std_ss [algebra_def, subset_class_def, prob_algebra_def, space_def, subsets_def, 767 PROB_ALGEBRA_EMPTY, PROB_ALGEBRA_UNION, IN_UNIV, SUBSET_UNIV] 768 >> REWRITE_TAC [GSYM COMPL_DEF] 769 >> POP_ASSUM MP_TAC 770 >> REWRITE_TAC [GSYM (REWRITE_CONV [subsets_def, prob_algebra_def] ``subsets prob_algebra``)] 771 >> REWRITE_TAC [PROB_ALGEBRA_COMPL]); 772 773val PROB_ALGEBRA_UNIV = store_thm 774 ("PROB_ALGEBRA_UNIV", ``UNIV IN (subsets prob_algebra)``, 775 `UNIV = space prob_algebra` by PROVE_TAC [prob_algebra_def, space_def] 776 >> PROVE_TAC [PROB_ALGEBRA_ALGEBRA, ALGEBRA_SPACE]); 777 778val PROB_ALGEBRA_INTER = store_thm 779 ("PROB_ALGEBRA_INTER", 780 ``!s t. s IN (subsets prob_algebra) /\ t IN (subsets prob_algebra) 781 ==> (s INTER t) IN (subsets prob_algebra)``, 782 ASSUME_TAC PROB_ALGEBRA_ALGEBRA 783 >> ASSUME_TAC (ISPEC ``prob_algebra`` ALGEBRA_INTER) 784 >> FULL_SIMP_TAC std_ss [subsets_def]); 785 786val PROB_ALGEBRA_HALFSPACE = store_thm 787 ("PROB_ALGEBRA_HALFSPACE", 788 ``!b. halfspace b IN (subsets prob_algebra)``, 789 PSET_TAC [IN_PROB_ALGEBRA, EXTENSION] 790 >> Q.EXISTS_TAC `[[b]]` 791 >> PSET_TAC [IN_PROB_EMBED, IN_HALFSPACE, MAP_MEM, MEM, prefix_set_def, 792 EXTENSION]); 793 794val PROB_ALGEBRA_BASIC = store_thm 795 ("PROB_ALGEBRA_BASIC", 796 ``{} IN (subsets prob_algebra) /\ 797 UNIV IN (subsets prob_algebra) /\ 798 (!b. halfspace b IN (subsets prob_algebra))``, 799 PROVE_TAC [PROB_ALGEBRA_EMPTY, PROB_ALGEBRA_UNIV, PROB_ALGEBRA_HALFSPACE]); 800 801val PROB_ALGEBRA_STL = store_thm 802 ("PROB_ALGEBRA_STL", 803 ``!p. (p o stl) IN (subsets prob_algebra) = p IN (subsets prob_algebra)``, 804 RW_TAC std_ss [IN_PROB_ALGEBRA] 805 >> REVERSE EQ_TAC 806 >- (PSET_TAC [o_DEF, EXTENSION] 807 >> Q.EXISTS_TAC `APPEND (MAP (CONS T) b) (MAP (CONS F) b)` 808 >> PSET_TAC [PROB_EMBED_APPEND, EXTENSION] 809 >> SEQ_CASES_TAC `x` 810 >> RW_TAC std_ss [STL_SCONS, PROB_EMBED_TLS] 811 >> PROVE_TAC []) 812 >> STRIP_TAC 813 >> POP_ASSUM MP_TAC 814 >> Suff 815 `!b. 816 prob_canonical b ==> 817 (p o stl = prob_embed b) ==> ?b'. (p = prob_embed b')` 818 >- (DISCH_THEN (MP_TAC o Q.SPEC `prob_canon b`) 819 >> RW_TAC std_ss [prob_canonical_def, PROB_CANON_IDEMPOT, 820 PROB_CANON_EMBED]) 821 >> HO_MATCH_MP_TAC PROB_CANONICAL_CASES 822 >> CONJ_TAC 823 >- (PSET_TAC [PROB_EMBED_BASIC, EXTENSION] 824 >> Q.EXISTS_TAC `[]` 825 >> PSET_TAC [PROB_EMBED_BASIC, EXTENSION] 826 >> POP_ASSUM (MP_TAC o Q.SPEC `scons T x`) 827 >> RW_TAC std_ss [STL_SCONS]) 828 >> CONJ_TAC 829 >- (PSET_TAC [PROB_EMBED_BASIC, EXTENSION] 830 >> Q.EXISTS_TAC `[[]]` 831 >> PSET_TAC [PROB_EMBED_BASIC, EXTENSION] 832 >> POP_ASSUM (MP_TAC o Q.SPEC `scons T x`) 833 >> RW_TAC std_ss [STL_SCONS]) 834 >> PSET_TAC [EXTENSION] 835 >> Q.EXISTS_TAC `l1` 836 >> STRIP_TAC 837 >> POP_ASSUM (MP_TAC o Q.SPEC `scons T x`) 838 >> PSET_TAC [PROB_EMBED_APPEND, STL_SCONS, PROB_EMBED_TLS, EXTENSION]); 839 840val PROB_ALGEBRA_SDROP = store_thm 841 ("PROB_ALGEBRA_SDROP", 842 ``!n p. (p o sdrop n) IN (subsets prob_algebra) = p IN (subsets prob_algebra)``, 843 Induct >- RW_TAC std_ss' [sdrop_def, o_DEF, I_THM] 844 >> RW_TAC bool_ss [sdrop_def, o_ASSOC, PROB_ALGEBRA_STL]); 845 846val PROB_ALGEBRA_INTER_HALVES = store_thm 847 ("PROB_ALGEBRA_INTER_HALVES", 848 ``!p. 849 (halfspace T INTER p) IN (subsets prob_algebra) /\ 850 (halfspace F INTER p) IN (subsets prob_algebra) = 851 p IN (subsets prob_algebra)``, 852 STRIP_TAC 853 >> REVERSE EQ_TAC >- PROVE_TAC [PROB_ALGEBRA_INTER, PROB_ALGEBRA_HALFSPACE] 854 >> REPEAT STRIP_TAC 855 >> Suff `(halfspace T INTER p) UNION (halfspace F INTER p) = p` 856 >- PROVE_TAC [PROB_ALGEBRA_UNION] 857 >> KILL_TAC 858 >> PSET_TAC [IN_HALFSPACE, EXTENSION] 859 >> PROVE_TAC []); 860 861val PROB_ALGEBRA_HALVES = store_thm 862 ("PROB_ALGEBRA_HALVES", 863 ``!p q. 864 (halfspace T INTER p) UNION (halfspace F INTER q) IN (subsets prob_algebra) = 865 (halfspace T INTER p) IN (subsets prob_algebra) /\ 866 (halfspace F INTER q) IN (subsets prob_algebra)``, 867 REPEAT STRIP_TAC 868 >> REVERSE EQ_TAC >- PROVE_TAC [PROB_ALGEBRA_UNION] 869 >> REPEAT STRIP_TAC >| 870 [Suff 871 `halfspace T INTER p = 872 halfspace T INTER (halfspace T INTER p UNION halfspace F INTER q)` 873 >- PROVE_TAC [PROB_ALGEBRA_HALFSPACE, PROB_ALGEBRA_INTER] 874 >> KILL_TAC 875 >> PSET_TAC [IN_HALFSPACE, EXTENSION] 876 >> PROVE_TAC [], 877 Suff 878 `halfspace F INTER q = 879 halfspace F INTER (halfspace T INTER p UNION halfspace F INTER q)` 880 >- PROVE_TAC [PROB_ALGEBRA_HALFSPACE, PROB_ALGEBRA_INTER] 881 >> KILL_TAC 882 >> PSET_TAC [IN_HALFSPACE, EXTENSION] 883 >> PROVE_TAC []]); 884 885val PROB_ALGEBRA_INTER_SHD = store_thm 886 ("PROB_ALGEBRA_INTER_SHD", 887 ``!b p. (halfspace b INTER p o stl) IN (subsets prob_algebra) = p IN (subsets prob_algebra)``, 888 RW_TAC std_ss [] 889 >> REVERSE EQ_TAC 890 >- PROVE_TAC [PROB_ALGEBRA_STL, PROB_ALGEBRA_HALFSPACE, PROB_ALGEBRA_INTER] 891 >> PSET_TAC [IN_PROB_ALGEBRA, IN_HALFSPACE, EXTENSION] 892 >> POP_ASSUM MP_TAC 893 >> Suff 894 `!c. 895 prob_canonical c ==> 896 (!v. (shd v = b) /\ stl v IN p = v IN prob_embed c) ==> 897 ?d. !v. v IN p = v IN prob_embed d` 898 >- (DISCH_THEN (MP_TAC o Q.SPEC `prob_canon b'`) 899 >> RW_TAC std_ss [PROB_CANON_EMBED, PROB_CANON_IDEMPOT, prob_canonical_def]) 900 >> HO_MATCH_MP_TAC PROB_CANONICAL_CASES 901 >> CONJ_TAC 902 >- (PSET_TAC [PROB_EMBED_BASIC, EXTENSION] 903 >> Q.EXISTS_TAC `[]` 904 >> STRIP_TAC 905 >> POP_ASSUM (MP_TAC o Q.SPEC `scons b v`) 906 >> PSET_TAC [PROB_EMBED_BASIC, SHD_SCONS, STL_SCONS, EXTENSION]) 907 >> CONJ_TAC 908 >- (PSET_TAC [PROB_EMBED_BASIC, EXTENSION] 909 >> Q.EXISTS_TAC `[[]]` 910 >> STRIP_TAC 911 >> POP_ASSUM (MP_TAC o Q.SPEC `scons b v`) 912 >> PSET_TAC [PROB_EMBED_BASIC, SHD_SCONS, STL_SCONS, EXTENSION]) 913 >> RW_TAC std_ss [] 914 >> Q.EXISTS_TAC `if b then l1 else l2` 915 >> STRIP_TAC 916 >> POP_ASSUM (MP_TAC o Q.SPEC `scons b v`) 917 >> PSET_TAC [PROB_EMBED_APPEND, PROB_EMBED_TLS, SHD_SCONS, 918 STL_SCONS, EXTENSION]); 919 920val PROB_TWINS_MEASURE = store_thm 921 ("PROB_TWINS_MEASURE", 922 ``!l. 923 (1 / 2):real pow LENGTH (SNOC T l) + (1 / 2) pow LENGTH (SNOC F l) = 924 (1 / 2) pow LENGTH l``, 925 RW_TAC std_ss [LENGTH_SNOC] 926 >> REWRITE_TAC [Q.SPEC `LENGTH (l :bool list)` POW_HALF_TWICE] 927 >> REAL_ARITH_TAC); 928 929val PROB_PREMEASURE_BASIC = store_thm 930 ("PROB_PREMEASURE_BASIC", 931 ``(prob_premeasure [] = 0) /\ (prob_premeasure [[]] = 1) /\ 932 (!b. prob_premeasure [[b]] = 1 / 2)``, 933 RW_TAC real_ss [prob_premeasure_def, LENGTH, pow]); 934 935val PROB_PREMEASURE_POS = store_thm 936 ("PROB_PREMEASURE_POS", 937 ``!l. 0 <= prob_premeasure l``, 938 Induct >- PROVE_TAC [prob_premeasure_def, REAL_ARITH ``(0:real) <= 0``] 939 >> RW_TAC list_ss [prob_premeasure_def] 940 >> PROVE_TAC [REAL_ARITH ``(0:real) < a /\ 0 <= b ==> 0 <= a + b``, 941 POW_HALF_POS]); 942 943val PROB_PREMEASURE_APPEND = store_thm 944 ("PROB_PREMEASURE_APPEND", 945 ``!l1 l2. prob_premeasure (APPEND l1 l2) = prob_premeasure l1 + prob_premeasure l2``, 946 NTAC 2 STRIP_TAC 947 >> Induct_on `l1` 948 >- (RW_TAC list_ss [prob_premeasure_def, APPEND] >> REAL_ARITH_TAC) 949 >> RW_TAC list_ss [prob_premeasure_def, APPEND] 950 >> REAL_ARITH_TAC); 951 952val PROB_PREMEASURE_TLS = store_thm 953 ("PROB_PREMEASURE_TLS", 954 ``!l b. 2 * prob_premeasure (MAP (CONS b) l) = prob_premeasure l``, 955 Induct >- (RW_TAC list_ss [prob_premeasure_def] >> REAL_ARITH_TAC) 956 >> RW_TAC list_ss [prob_premeasure_def, MAP, pow] 957 >> REWRITE_TAC [REAL_ADD_LDISTRIB, REAL_MUL_ASSOC, HALF_CANCEL, 958 REAL_MUL_LID] 959 >> PROVE_TAC []); 960 961val PROB_CANON_PREFS_MONO = store_thm 962 ("PROB_CANON_PREFS_MONO", 963 ``!l b. prob_premeasure (prob_canon_prefs l b) <= prob_premeasure (l :: b)``, 964 STRIP_TAC 965 >> Induct >- RW_TAC list_ss [prob_canon_prefs_def, REAL_LE_REFL] 966 >> REVERSE (RW_TAC list_ss [prob_canon_prefs_def]) 967 >- PROVE_TAC [REAL_LE_REFL] 968 >> Suff `prob_premeasure (l::b) <= prob_premeasure (l::h::b)` 969 >- PROVE_TAC [REAL_LE_TRANS] 970 >> KILL_TAC 971 >> RW_TAC list_ss [prob_premeasure_def] 972 >> ASSUME_TAC (SPEC ``LENGTH (h:bool list)`` POW_HALF_POS) 973 >> PROVE_TAC [REAL_ARITH ``0 < (x:real) ==> a + b <= a + (x + b)``]); 974 975val PROB_CANON_FIND_MONO = store_thm 976 ("PROB_CANON_FIND_MONO", 977 ``!l b. prob_premeasure (prob_canon_find l b) <= prob_premeasure (l :: b)``, 978 STRIP_TAC 979 >> Induct >- RW_TAC list_ss [prob_canon_find_def, REAL_LE_REFL] 980 >> RW_TAC list_ss [prob_canon_find_def] >| 981 [KILL_TAC 982 >> REWRITE_TAC [prob_premeasure_def] 983 >> ASSUME_TAC (SPEC ``LENGTH (l:bool list)`` POW_HALF_POS) 984 >> PROVE_TAC [REAL_ARITH ``0 < (x:real) ==> a <= x + a``], 985 NTAC 2 (POP_ASSUM (K ALL_TAC)) 986 >> POP_ASSUM MP_TAC 987 >> REWRITE_TAC [prob_premeasure_def] 988 >> REAL_ARITH_TAC, 989 PROVE_TAC [PROB_CANON_PREFS_MONO]]); 990 991val PROB_CANON1_MONO = store_thm 992 ("PROB_CANON1_MONO", 993 ``!l. prob_premeasure (prob_canon1 l) <= prob_premeasure l``, 994 REWRITE_TAC [prob_canon1_def] 995 >> Induct >- RW_TAC list_ss [REAL_LE_REFL, FOLDR] 996 >> RW_TAC list_ss [FOLDR] 997 >> Suff `prob_premeasure (h::FOLDR prob_canon_find [] l) 998 <= prob_premeasure (h::l)` 999 >- PROVE_TAC [PROB_CANON_FIND_MONO, REAL_LE_TRANS] 1000 >> PROVE_TAC [prob_premeasure_def, REAL_LE_LADD]); 1001 1002val PROB_CANON_MERGE_MONO = store_thm 1003 ("PROB_CANON_MERGE_MONO", 1004 ``!l b. prob_premeasure (prob_canon_merge l b) <= prob_premeasure (l::b)``, 1005 Induct_on `b` >- RW_TAC real_ss [prob_canon_merge_def, REAL_LE_REFL] 1006 >> RW_TAC real_ss [prob_canon_merge_def, prob_twin_def] 1007 >> RW_TAC std_ss [BUTLAST] 1008 >> Suff `prob_premeasure (l'::b) <= prob_premeasure (SNOC T l'::SNOC F l'::b)` 1009 >- PROVE_TAC [REAL_LE_TRANS] 1010 >> KILL_TAC 1011 >> RW_TAC std_ss [prob_premeasure_def, REAL_ADD_ASSOC, PROB_TWINS_MEASURE, 1012 REAL_LE_REFL]); 1013 1014val PROB_CANON2_MONO = store_thm 1015 ("PROB_CANON2_MONO", 1016 ``!l. prob_premeasure (prob_canon2 l) <= prob_premeasure l``, 1017 REWRITE_TAC [prob_canon2_def] 1018 >> Induct >- RW_TAC list_ss [REAL_LE_REFL, FOLDR] 1019 >> RW_TAC list_ss [FOLDR] 1020 >> Suff `prob_premeasure (h::FOLDR prob_canon_merge [] l) 1021 <= prob_premeasure (h::l)` 1022 >- PROVE_TAC [PROB_CANON_MERGE_MONO, REAL_LE_TRANS] 1023 >> PROVE_TAC [prob_premeasure_def, REAL_LE_LADD]); 1024 1025val PROB_CANON_MONO = store_thm 1026 ("PROB_CANON_MONO", 1027 ``!l. prob_premeasure (prob_canon l) <= prob_premeasure l``, 1028 RW_TAC std_ss [prob_canon_def] 1029 >> PROVE_TAC [PROB_CANON1_MONO, PROB_CANON2_MONO, REAL_LE_TRANS]); 1030 1031val PROB_MEASURE_ALT = store_thm 1032 ("PROB_MEASURE_ALT", 1033 ``!l. prob_measure (prob_embed l) = prob_premeasure (prob_canon l)``, 1034 RW_TAC std_ss [prob_measure_def] 1035 >> HO_MATCH_MP_TAC REAL_INF_MIN 1036 >> RW_TAC std_ss [GSPECIFICATION] 1037 >- PROVE_TAC [PROB_CANON_REP, PROB_CANON_IDEMPOT] 1038 >> Suff `prob_premeasure (prob_canon c) <= prob_premeasure c` 1039 >- PROVE_TAC [PROB_CANON_REP] 1040 >> PROVE_TAC [PROB_CANON_MONO]); 1041 1042val PROB_MEASURE_BASIC = store_thm 1043 ("PROB_MEASURE_BASIC", 1044 ``(prob_measure {} = 0) /\ (prob_measure UNIV = 1) /\ 1045 (!b. prob_measure (halfspace b) = 1 / 2)``, 1046 RW_TAC std_ss [GSYM PROB_EMBED_BASIC, PROB_MEASURE_ALT, 1047 PROB_CANON_BASIC, PROB_PREMEASURE_BASIC]); 1048 1049val PROB_CANONICAL_MEASURE_MAX = store_thm 1050 ("PROB_CANONICAL_MEASURE_MAX", 1051 ``!l. prob_canonical l ==> prob_premeasure l <= 1``, 1052 HO_MATCH_MP_TAC PROB_CANONICAL_INDUCT 1053 >> CONJ_TAC >- (RW_TAC list_ss [prob_premeasure_def] >> REAL_ARITH_TAC) 1054 >> CONJ_TAC >- (RW_TAC list_ss [prob_premeasure_def, pow] >> REAL_ARITH_TAC) 1055 >> RW_TAC list_ss [PROB_PREMEASURE_APPEND] 1056 >> Suff `(2 * prob_premeasure (MAP (CONS T) l) = prob_premeasure l) /\ 1057 (2 * prob_premeasure (MAP (CONS F) l') = prob_premeasure l')` 1058 >- PROVE_TAC [REAL_ARITH ``(2 * a = b) /\ (2 * c = d) /\ b <= 1 /\ d <= 1 1059 ==> a + c <= (1:real)``] 1060 >> PROVE_TAC [PROB_PREMEASURE_TLS]); 1061 1062val PROB_MEASURE_MAX = store_thm 1063 ("PROB_MEASURE_MAX", 1064 ``!l. l IN (subsets prob_algebra) ==> prob_measure l <= 1``, 1065 RW_TAC std_ss [IN_PROB_ALGEBRA] 1066 >> RW_TAC std_ss [PROB_MEASURE_ALT] 1067 >> MP_TAC (Q.SPEC `prob_canon b` PROB_CANONICAL_MEASURE_MAX) 1068 >> RW_TAC std_ss [prob_canonical_def, PROB_CANON_IDEMPOT]); 1069 1070val PROB_PREMEASURE_COMPL = store_thm 1071 ("PROB_PREMEASURE_COMPL", 1072 ``!b. 1073 prob_canonical b ==> 1074 !c. 1075 prob_canonical c ==> 1076 (COMPL (prob_embed b) = prob_embed c) ==> 1077 (prob_premeasure b + prob_premeasure c = 1)``, 1078 HO_MATCH_MP_TAC PROB_CANONICAL_INDUCT 1079 >> CONJ_TAC 1080 >- (PSET_TAC [PROB_PREMEASURE_BASIC, PROB_EMBED_BASIC, EXTENSION] 1081 >> Know `prob_canon c = prob_canon [[]]` 1082 >- PSET_TAC [PROB_CANON_REP, PROB_EMBED_BASIC, EXTENSION] 1083 >> PSET_TAC [PROB_CANON_BASIC, prob_canonical_def, PROB_EMBED_BASIC, 1084 PROB_PREMEASURE_BASIC, REAL_ADD_LID, EXTENSION]) 1085 >> CONJ_TAC 1086 >- (PSET_TAC [PROB_PREMEASURE_BASIC, PROB_EMBED_BASIC, EXTENSION] 1087 >> Know `prob_canon c = prob_canon []` 1088 >- PSET_TAC [PROB_CANON_REP, PROB_EMBED_BASIC, EXTENSION] 1089 >> PSET_TAC [PROB_CANON_BASIC, prob_canonical_def, PROB_EMBED_BASIC, 1090 PROB_PREMEASURE_BASIC, REAL_ADD_RID, EXTENSION]) 1091 >> PSET_TAC [PROB_PREMEASURE_BASIC, PROB_EMBED_BASIC, EXTENSION] 1092 >> NTAC 2 (POP_ASSUM MP_TAC) 1093 >> Q.SPEC_TAC (`c`, `c`) 1094 >> HO_MATCH_MP_TAC PROB_CANONICAL_CASES 1095 >> CONJ_TAC 1096 >- (PSET_TAC [PROB_EMBED_BASIC, PROB_PREMEASURE_BASIC, EXTENSION] 1097 >> Suff `APPEND (MAP (CONS T) b) (MAP (CONS F) b') = [[]]` 1098 >- PROVE_TAC [MEM_NIL_STEP, MEM] 1099 >> PSET_TAC [GSYM PROB_CANONICAL_EMBED_UNIV, EXTENSION]) 1100 >> CONJ_TAC 1101 >- (PSET_TAC [PROB_EMBED_BASIC, PROB_PREMEASURE_BASIC, EXTENSION] 1102 >> Know `APPEND (MAP (CONS T) b) (MAP (CONS F) b') = []` 1103 >- PSET_TAC [GSYM PROB_CANONICAL_EMBED_EMPTY, EXTENSION] 1104 >> RW_TAC std_ss [PROB_PREMEASURE_BASIC, REAL_ADD_LID]) 1105 >> RW_TAC std_ss [] 1106 >> Know `!a b : real. (2 * a + 2 * b = 1 + 1) ==> (a + b = 1)` 1107 >- REAL_ARITH_TAC 1108 >> DISCH_THEN MATCH_MP_TAC 1109 >> PSET_TAC [PROB_EMBED_APPEND, PROB_PREMEASURE_APPEND, PROB_PREMEASURE_TLS, 1110 REAL_ADD_LDISTRIB, EXTENSION] 1111 >> Suff 1112 `(prob_premeasure b + prob_premeasure l1 = 1) /\ 1113 (prob_premeasure b' + prob_premeasure l2 = 1)` 1114 >- REAL_ARITH_TAC 1115 >> CONJ_TAC >| 1116 [Suff `!v. ~(v IN prob_embed b) = v IN prob_embed l1` 1117 >- PROVE_TAC [] 1118 >> STRIP_TAC 1119 >> POP_ASSUM (MP_TAC o Q.SPEC `scons T v`) 1120 >> RW_TAC std_ss [PROB_EMBED_TLS, SHD_SCONS, STL_SCONS], 1121 Suff `!v. ~(v IN prob_embed b') = v IN prob_embed l2` 1122 >- PROVE_TAC [] 1123 >> STRIP_TAC 1124 >> POP_ASSUM (MP_TAC o Q.SPEC `scons F v`) 1125 >> RW_TAC std_ss [PROB_EMBED_TLS, SHD_SCONS, STL_SCONS]]); 1126 1127val PROB_PREMEASURE_ADDITIVE = store_thm 1128 ("PROB_PREMEASURE_ADDITIVE", 1129 ``!b. 1130 prob_canonical b ==> 1131 !c. 1132 prob_canonical c ==> 1133 !d. 1134 prob_canonical d ==> 1135 (prob_embed c INTER prob_embed d = {}) /\ 1136 (prob_embed b = prob_embed c UNION prob_embed d) ==> 1137 (prob_premeasure b = prob_premeasure c + prob_premeasure d)``, 1138 HO_MATCH_MP_TAC PROB_CANONICAL_INDUCT 1139 >> CONJ_TAC 1140 >- (PSET_TAC [PROB_PREMEASURE_BASIC, PROB_EMBED_BASIC, EXTENSION] 1141 >> Know `c = []` >- PSET_TAC [GSYM PROB_CANONICAL_EMBED_EMPTY, EXTENSION] 1142 >> Know `d = []` >- PSET_TAC [GSYM PROB_CANONICAL_EMBED_EMPTY, EXTENSION] 1143 >> RW_TAC real_ss [PROB_PREMEASURE_BASIC]) 1144 >> CONJ_TAC 1145 >- (PSET_TAC [PROB_PREMEASURE_BASIC, PROB_EMBED_BASIC, EXTENSION] 1146 >> MP_TAC (Q.SPEC `c` PROB_PREMEASURE_COMPL) 1147 >> ASM_REWRITE_TAC [] 1148 >> DISCH_THEN (MP_TAC o Q.SPEC `d`) 1149 >> PSET_TAC [EXTENSION] 1150 >> PROVE_TAC []) 1151 >> RW_TAC std_ss [] 1152 >> NTAC 4 (POP_ASSUM MP_TAC) 1153 >> Q.SPEC_TAC (`c`, `c`) 1154 >> HO_MATCH_MP_TAC PROB_CANONICAL_CASES 1155 >> CONJ_TAC 1156 >- (PSET_TAC [PROB_PREMEASURE_BASIC, PROB_EMBED_BASIC, EXTENSION] 1157 >> Suff `d = APPEND (MAP (CONS T) b) (MAP (CONS F) b')` 1158 >- RW_TAC real_ss [] 1159 >> Suff 1160 `prob_canon d = prob_canon (APPEND (MAP (CONS T) b) (MAP (CONS F) b'))` 1161 >- PROVE_TAC [prob_canonical_def] 1162 >> PSET_TAC [PROB_CANON_REP, EXTENSION]) 1163 >> CONJ_TAC 1164 >- (PSET_TAC [PROB_PREMEASURE_BASIC, PROB_EMBED_BASIC, EXTENSION] 1165 >> Suff `APPEND (MAP (CONS T) b) (MAP (CONS F) b') = [[]]` 1166 >- PROVE_TAC [MEM_NIL_STEP, MEM] 1167 >> PSET_TAC [GSYM PROB_CANONICAL_EMBED_UNIV, EXTENSION]) 1168 >> RW_TAC std_ss [] 1169 >> NTAC 3 (POP_ASSUM MP_TAC) 1170 >> Q.SPEC_TAC (`d`, `d`) 1171 >> HO_MATCH_MP_TAC PROB_CANONICAL_CASES 1172 >> CONJ_TAC 1173 >- (PSET_TAC [PROB_PREMEASURE_BASIC, PROB_EMBED_BASIC, EXTENSION] 1174 >> Suff 1175 `APPEND (MAP (CONS T) b) (MAP (CONS F) b') = 1176 APPEND (MAP (CONS T) l1) (MAP (CONS F) l2)` 1177 >- RW_TAC real_ss [] 1178 >> Suff 1179 `prob_canon (APPEND (MAP (CONS T) b) (MAP (CONS F) b')) = 1180 prob_canon (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2))` 1181 >- PSET_TAC [prob_canonical_def, EXTENSION] 1182 >> PSET_TAC [PROB_CANON_REP, EXTENSION]) 1183 >> CONJ_TAC 1184 >- (PSET_TAC [PROB_PREMEASURE_BASIC, PROB_EMBED_BASIC, EXTENSION] 1185 >> Suff `APPEND (MAP (CONS T) b) (MAP (CONS F) b') = [[]]` 1186 >- PROVE_TAC [MEM_NIL_STEP, MEM] 1187 >> PSET_TAC [GSYM PROB_CANONICAL_EMBED_UNIV, EXTENSION]) 1188 >> RW_TAC std_ss [] 1189 >> Know `!a b : real. (2 * a = 2 * b) ==> (a = b)` 1190 >- REAL_ARITH_TAC 1191 >> DISCH_THEN MATCH_MP_TAC 1192 >> RW_TAC std_ss [REAL_ADD_LDISTRIB, PROB_PREMEASURE_APPEND, PROB_PREMEASURE_TLS, 1193 PROB_EMBED_APPEND] 1194 >> Suff 1195 `(prob_premeasure b = prob_premeasure l1 + prob_premeasure l1') /\ 1196 (prob_premeasure b' = prob_premeasure l2 + prob_premeasure l2')` 1197 >- (RW_TAC real_ss [] >> METIS_TAC [REAL_ADD_COMM, REAL_ADD_ASSOC]) 1198 >> CONJ_TAC >| 1199 [Suff 1200 `(prob_embed l1 INTER prob_embed l1' = {}) /\ 1201 (prob_embed b = prob_embed l1 UNION prob_embed l1')` 1202 >- (Q.PAT_X_ASSUM 1203 `!c. 1204 prob_canonical c ==> 1205 !d. 1206 prob_canonical d ==> 1207 (prob_embed c INTER prob_embed d = {}) /\ 1208 (prob_embed b = prob_embed c UNION prob_embed d) ==> 1209 (prob_premeasure b = prob_premeasure c + prob_premeasure d)` 1210 (MP_TAC o Q.SPEC `l1`) 1211 >> RW_TAC std_ss []) 1212 >> CONJ_TAC >| 1213 [POP_ASSUM K_TAC 1214 >> POP_ASSUM MP_TAC 1215 >> RW_TAC std_ss [EXTENSION, IN_INTER, NOT_IN_EMPTY] 1216 >> POP_ASSUM (MP_TAC o Q.SPEC `scons T x`) 1217 >> RW_TAC std_ss [PROB_EMBED_TLS, STL_SCONS, SHD_SCONS, 1218 PROB_EMBED_APPEND, IN_UNION], 1219 POP_ASSUM MP_TAC 1220 >> POP_ASSUM K_TAC 1221 >> RW_TAC std_ss [EXTENSION, IN_UNION] 1222 >> POP_ASSUM (MP_TAC o Q.SPEC `scons T x`) 1223 >> RW_TAC std_ss [PROB_EMBED_TLS, STL_SCONS, SHD_SCONS, 1224 PROB_EMBED_APPEND, IN_UNION]], 1225 Suff 1226 `(prob_embed l2 INTER prob_embed l2' = {}) /\ 1227 (prob_embed b' = prob_embed l2 UNION prob_embed l2')` 1228 >- (Q.PAT_X_ASSUM 1229 `!c. 1230 prob_canonical c ==> 1231 !d. 1232 prob_canonical d ==> 1233 (prob_embed c INTER prob_embed d = {}) /\ 1234 (prob_embed b' = prob_embed c UNION prob_embed d) ==> 1235 (prob_premeasure b' = prob_premeasure c + prob_premeasure d)` 1236 (MP_TAC o Q.SPEC `l2`) 1237 >> RW_TAC std_ss []) 1238 >> CONJ_TAC >| 1239 [POP_ASSUM K_TAC 1240 >> POP_ASSUM MP_TAC 1241 >> RW_TAC std_ss [EXTENSION, IN_INTER, NOT_IN_EMPTY] 1242 >> POP_ASSUM (MP_TAC o Q.SPEC `scons F x`) 1243 >> RW_TAC std_ss [PROB_EMBED_TLS, STL_SCONS, SHD_SCONS, 1244 PROB_EMBED_APPEND, IN_UNION], 1245 POP_ASSUM MP_TAC 1246 >> POP_ASSUM K_TAC 1247 >> RW_TAC std_ss [EXTENSION, IN_UNION] 1248 >> POP_ASSUM (MP_TAC o Q.SPEC `scons F x`) 1249 >> RW_TAC std_ss [PROB_EMBED_TLS, STL_SCONS, SHD_SCONS, 1250 PROB_EMBED_APPEND, IN_UNION]]]); 1251 1252val PROB_MEASURE_ADDITIVE = store_thm 1253 ("PROB_MEASURE_ADDITIVE", 1254 ``additive (space prob_algebra, subsets prob_algebra, prob_measure)``, 1255 RW_TAC std_ss [additive_def, IN_PROB_ALGEBRA, DISJOINT_DEF, 1256 measure_def, measurable_sets_def] 1257 >> Know `(prob_embed b UNION prob_embed b') IN (subsets prob_algebra)` 1258 >- PROVE_TAC [PROB_ALGEBRA_UNION, IN_PROB_ALGEBRA] 1259 >> RW_TAC std_ss [IN_PROB_ALGEBRA] 1260 >> RW_TAC std_ss [PROB_MEASURE_ALT] 1261 >> ASSUME_TAC PROB_PREMEASURE_ADDITIVE 1262 >> POP_ASSUM (MP_TAC o Q.SPEC `prob_canon b''`) 1263 >> RW_TAC std_ss [prob_canonical_def, PROB_CANON_IDEMPOT] 1264 >> POP_ASSUM (MP_TAC o Q.SPEC `prob_canon b`) 1265 >> RW_TAC std_ss [prob_canonical_def, PROB_CANON_IDEMPOT] 1266 >> POP_ASSUM (MP_TAC o Q.SPEC `prob_canon b'`) 1267 >> RW_TAC std_ss [prob_canonical_def, PROB_CANON_IDEMPOT] 1268 >> POP_ASSUM MATCH_MP_TAC 1269 >> RW_TAC std_ss [PROB_CANON_EMBED]); 1270 1271val PROB_MEASURE_POS = store_thm 1272 ("PROB_MEASURE_POS", 1273 ``!l. 0 <= prob_measure (prob_embed l)``, 1274 RW_TAC std_ss [PROB_MEASURE_ALT, PROB_PREMEASURE_POS]); 1275 1276val PROB_MEASURE_POSITIVE = store_thm 1277 ("PROB_MEASURE_POSITIVE", 1278 ``positive (space prob_algebra, subsets prob_algebra, prob_measure)``, 1279 RW_TAC std_ss [positive_def, PROB_MEASURE_BASIC, IN_PROB_ALGEBRA, 1280 measure_def, measurable_sets_def] 1281 >> RW_TAC std_ss [PROB_MEASURE_POS]); 1282 1283val INFINITE_TLS = store_thm 1284 ("INFINITE_TLS", 1285 ``?sel. !s. 1286 INFINITE s ==> INFINITE {TL x | x IN s /\ (HD x : bool = sel s)}``, 1287 Suff 1288 `!s. ?sel. 1289 INFINITE s ==> INFINITE {TL x | x IN s /\ (HD x : bool = sel)}` 1290 >- DISCH_THEN (ACCEPT_TAC o CONV_RULE SKOLEM_CONV) 1291 >> RW_TAC std_ss [] 1292 >> CCONTR_TAC 1293 >> POP_ASSUM MP_TAC 1294 >> DISCH_THEN (MP_TAC o CONV_RULE NOT_EXISTS_CONV) 1295 >> DISCH_THEN (fn th => MP_TAC (Q.SPEC `T` th) >> MP_TAC (Q.SPEC `F` th)) 1296 >> RW_TAC std_ss [] 1297 >> STRIP_TAC 1298 >> Q.PAT_X_ASSUM `~FINITE s` MP_TAC 1299 >> RW_TAC std_ss [] 1300 >> ONCE_REWRITE_TAC [GSYM FINITE_TL] 1301 >> Suff `{TL x | x IN s /\ HD x} UNION {TL x | x IN s /\ ~HD x} = IMAGE TL s` 1302 >- PROVE_TAC [FINITE_UNION] 1303 >> PSET_TAC [EXTENSION] 1304 >> PROVE_TAC []); 1305 1306val PREFIX_SET_UNION_UNIV = store_thm 1307 ("PREFIX_SET_UNION_UNIV", 1308 ``!s : bool list -> bool. 1309 (!a b. a IN s /\ b IN s /\ ~(a = b) ==> ~(IS_PREFIX a b)) /\ 1310 (BIGUNION (IMAGE prefix_set s) = UNIV) ==> 1311 FINITE s``, 1312 MP_TAC INFINITE_TLS 1313 >> RW_TAC std_ss [] 1314 >> CCONTR_TAC 1315 >> POP_ASSUM MP_TAC 1316 >> PURE_REWRITE_TAC [] 1317 >> STRIP_TAC 1318 >> Q.PAT_X_ASSUM `x = UNIV` MP_TAC 1319 >> PSET_TAC [EXTENSION] 1320 >> Suff `?x. !l. l IN s ==> ~(x IN prefix_set l)` >- PROVE_TAC [] 1321 >> Q.EXISTS_TAC 1322 `\n. sel (FUNPOW (\t. {TL x | x IN t /\ (HD x = sel t)}) n s)` 1323 >> RW_TAC std_ss [] 1324 >> NTAC 3 (POP_ASSUM MP_TAC) 1325 >> Q.SPEC_TAC (`s`, `s`) 1326 >> Induct_on `l` 1327 >- (RW_TAC std_ss [] 1328 >> Know `?a. a IN (s DELETE [])` 1329 >- PROVE_TAC [INFINITE_INHAB, INFINITE_DELETE] 1330 >> PSET_TAC [EXTENSION] 1331 >> PROVE_TAC [IS_PREFIX_NIL]) 1332 >> RW_TAC std_ss [prefix_set_def, IN_INTER, IN_o, STL_PARTIAL] 1333 >> RW_TAC std_ss [o_DEF, FUNPOW, IN_HALFSPACE, shd_def] 1334 >> REWRITE_TAC [GSYM IMP_DISJ_THM] 1335 >> RW_TAC std_ss [] 1336 >> Q.PAT_X_ASSUM `!s. P s ==> Q s` 1337 (MATCH_MP_TAC o REWRITE_RULE [AND_IMP_INTRO]) 1338 >> REWRITE_TAC [GSYM CONJ_ASSOC] 1339 >> REVERSE (PSET_TAC [EXTENSION]) 1340 >- (Q.EXISTS_TAC `sel s :: l` 1341 >> RW_TAC std_ss [TL, HD]) 1342 >> Know `~([] IN s)` 1343 >- (STRIP_TAC 1344 >> Q.PAT_X_ASSUM `!a b. P a b` 1345 (MP_TAC o Q.SPECL [`sel (s : bool list -> bool) :: l`, `[]`]) 1346 >> RW_TAC std_ss [IS_PREFIX_NIL]) 1347 >> STRIP_TAC 1348 >> Cases_on `x` >- PROVE_TAC [] 1349 >> Cases_on `x'` >- PROVE_TAC [] 1350 >> REPEAT (POP_ASSUM MP_TAC) 1351 >> RW_TAC std_ss [HD, TL] 1352 >> Q.PAT_X_ASSUM `!a b. P a b` 1353 (MP_TAC o Q.SPECL [`sel (s : bool list -> bool) :: t`, 1354 `sel (s : bool list -> bool) :: t'`]) 1355 >> RW_TAC std_ss [IS_PREFIX]); 1356 1357val IN_PROB_ALGEBRA_CANONICAL = store_thm 1358 ("IN_PROB_ALGEBRA_CANONICAL", 1359 ``!x. x IN (subsets prob_algebra) = ?b. prob_canonical b /\ (x = prob_embed b)``, 1360 RW_TAC std_ss [IN_PROB_ALGEBRA] 1361 >> REVERSE EQ_TAC >- PROVE_TAC [] 1362 >> RW_TAC std_ss [] 1363 >> Q.EXISTS_TAC `prob_canon b` 1364 >> RW_TAC std_ss [prob_canonical_def, PROB_CANON_IDEMPOT, PROB_CANON_EMBED]); 1365 1366val ALGEBRA_COUNTABLE_UNION_UNIV = store_thm 1367 ("ALGEBRA_COUNTABLE_UNION_UNIV", 1368 ``!f : num -> (num -> bool) -> bool. 1369 f IN (UNIV -> subsets prob_algebra) /\ 1370 (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) /\ 1371 (BIGUNION (IMAGE f UNIV) = UNIV) ==> 1372 ?N. !n. N <= n ==> (f n = {})``, 1373 RW_TAC std_ss [IN_FUNSET, IN_UNIV, IN_PROB_ALGEBRA_CANONICAL] 1374 >> Q.PAT_X_ASSUM `!x. ?b. P x b` 1375 (MP_TAC o CONV_RULE (SKOLEM_CONV THENC DEPTH_CONV FORALL_AND_CONV)) 1376 >> RW_TAC std_ss [] 1377 >> Suff `FINITE {n | ~(f n = {})}` 1378 >- (RW_TAC std_ss [FINITE_SUBSET_COUNT, SUBSET_DEF, IN_COUNT, 1379 GSPECIFICATION] 1380 >> Q.EXISTS_TAC `n` 1381 >> PROVE_TAC [NOT_LESS]) 1382 >> Suff `FINITE {l | ?n : num. MEM l (b n)}` 1383 >- (STRIP_TAC 1384 >> MATCH_MP_TAC (INST_TYPE [beta |-> ``:bool list``] FINITE_INJ) 1385 >> Q.EXISTS_TAC `(HD o b)` 1386 >> Q.EXISTS_TAC `{l | ?n. IS_EL l (b n)}` 1387 >> RW_TAC std_ss [] 1388 >> PSET_TAC [INJ_DEF, o_THM, EXTENSION] 1389 >- (POP_ASSUM MP_TAC 1390 >> Cases_on `b x` 1391 >- RW_TAC std_ss [PROB_EMBED_BASIC, NOT_IN_EMPTY] 1392 >> PROVE_TAC [HD, MEM]) 1393 >> Cases_on `b x` >- PROVE_TAC [PROB_EMBED_BASIC, NOT_IN_EMPTY] 1394 >> Cases_on `b y` >- PROVE_TAC [PROB_EMBED_BASIC, NOT_IN_EMPTY] 1395 >> NTAC 3 (POP_ASSUM MP_TAC) 1396 >> RW_TAC std_ss [HD] 1397 >> Suff `?z. z IN f x /\ z IN f y` >- PROVE_TAC [] 1398 >> RW_TAC std_ss [PROB_EMBED_CONS, IN_UNION] 1399 >> PROVE_TAC [PREFIX_SET_POPULATED]) 1400 >> MATCH_MP_TAC PREFIX_SET_UNION_UNIV 1401 >> REVERSE CONJ_TAC 1402 >- (Q.PAT_X_ASSUM `x = UNIV` (ONCE_REWRITE_TAC o wrap o GSYM) 1403 >> POP_ASSUM MP_TAC 1404 >> KILL_TAC 1405 >> RW_TAC std_ss [EXTENSION, IN_BIGUNION, IN_PROB_EMBED] 1406 >> (EQ_TAC >> STRIP_TAC) >| 1407 [POP_ASSUM (MP_TAC o REWRITE_RULE [IN_IMAGE]) 1408 >> RW_TAC std_ss [GSPECIFICATION] 1409 >> Q.EXISTS_TAC `f n` 1410 >> RW_TAC std_ss [IN_IMAGE, IN_UNIV] 1411 >> PROVE_TAC [], 1412 PSET_TAC [EXTENSION] 1413 >> PROVE_TAC []]) 1414 >> RW_TAC std_ss [GSPECIFICATION, GSYM PREFIX_SET_PREFIX_SUBSET, SUBSET_DEF] 1415 >> MP_TAC (Q.SPEC `a` PREFIX_SET_POPULATED) 1416 >> STRIP_TAC 1417 >> Q.EXISTS_TAC `x` 1418 >> RW_TAC std_ss [] 1419 >> STRIP_TAC 1420 >> Know `x IN f n` 1421 >- (RW_TAC std_ss [prob_embed_def, IN_UNIONL, MAP_MEM] 1422 >> PROVE_TAC []) 1423 >> Know `x IN f n'` 1424 >- (RW_TAC std_ss [prob_embed_def, IN_UNIONL, MAP_MEM] 1425 >> PROVE_TAC []) 1426 >> REPEAT STRIP_TAC 1427 >> Q.PAT_X_ASSUM `!m n. P m n` (MP_TAC o Q.SPECL [`n`, `n'`]) 1428 >> REVERSE (RW_TAC std_ss [DISJOINT_DEF, EXTENSION, NOT_IN_EMPTY, IN_INTER]) 1429 >- PROVE_TAC [] 1430 >> STRIP_TAC 1431 >> RW_TAC std_ss [] 1432 >> MP_TAC (Q.SPECL [`a`, `b'`] PREFIX_SET_SUBSET) 1433 >> RW_TAC std_ss [PREFIX_SET_PREFIX_SUBSET, DISJOINT_DEF, EXTENSION, 1434 NOT_IN_EMPTY, IN_INTER] >| 1435 [PROVE_TAC [], 1436 PROVE_TAC [PROB_CANONICAL_PREFIXFREE], 1437 PROVE_TAC [PROB_CANONICAL_PREFIXFREE]]); 1438 1439val PROB_EMBED_TLS_EMPTY = store_thm 1440 ("PROB_EMBED_TLS_EMPTY", 1441 ``!l b. (prob_embed (MAP (CONS b) l) = {}) = (prob_embed l = {})``, 1442 PSET_TAC [EXTENSION] 1443 >> EQ_TAC >| 1444 [RW_TAC std_ss [] 1445 >> POP_ASSUM (MP_TAC o Q.SPEC `scons b x`) 1446 >> RW_TAC std_ss [PROB_EMBED_TLS], 1447 RW_TAC std_ss [] 1448 >> MP_TAC (Q.ISPEC `x : num -> bool` SCONS_SURJ) 1449 >> STRIP_TAC 1450 >> RW_TAC std_ss [] 1451 >> RW_TAC std_ss [PROB_EMBED_TLS]]); 1452 1453val ALGEBRA_COUNTABLE_UNION = store_thm 1454 ("ALGEBRA_COUNTABLE_UNION", 1455 ``!f : num -> (num -> bool) -> bool. 1456 f IN (UNIV -> subsets prob_algebra) /\ 1457 (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) /\ 1458 (BIGUNION (IMAGE f UNIV) IN (subsets prob_algebra)) ==> 1459 ?N. !n. N <= n ==> (f n = {})``, 1460 RW_TAC std_ss [IN_PROB_ALGEBRA] 1461 >> REPEAT (POP_ASSUM MP_TAC) 1462 >> ONCE_REWRITE_TAC [GSYM PROB_CANON_EMBED] 1463 >> Q.SPEC_TAC (`f`, `f`) 1464 >> Know `prob_canonical (prob_canon b)` 1465 >- PROVE_TAC [prob_canonical_def, PROB_CANON_IDEMPOT] 1466 >> Q.SPEC_TAC (`prob_canon b`, `b`) 1467 >> HO_MATCH_MP_TAC PROB_CANONICAL_INDUCT 1468 >> CONJ_TAC 1469 >- (RW_TAC std_ss [PROB_EMBED_BASIC, BIGUNION_EQ_EMPTY, IN_IMAGE, IN_UNIV] 1470 >> Q.EXISTS_TAC `0` 1471 >> RW_TAC arith_ss [] 1472 >> PROVE_TAC []) 1473 >> CONJ_TAC 1474 >- (RW_TAC std_ss [PROB_EMBED_BASIC] 1475 >> PROVE_TAC [ALGEBRA_COUNTABLE_UNION_UNIV]) 1476 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV] 1477 >> Q.PAT_X_ASSUM `!x. f x IN (subsets prob_algebra)` MP_TAC 1478 >> RW_TAC std_ss [IN_PROB_ALGEBRA_CANONICAL] 1479 >> Q.PAT_X_ASSUM `!x. ?b. P x b` 1480 (MP_TAC o CONV_RULE (SKOLEM_CONV THENC DEPTH_CONV FORALL_AND_CONV)) 1481 >> RW_TAC std_ss [] 1482 >> Know 1483 `?b1 b2. !x. b'' x = APPEND (MAP (CONS T) (b1 x)) (MAP (CONS F) (b2 x))` 1484 >- (Suff 1485 `!x. ?b1 b2. b'' x = APPEND (MAP (CONS T) b1) (MAP (CONS F) b2)` 1486 >- DISCH_THEN 1487 (ACCEPT_TAC o CONV_RULE (REDEPTH_CONV (CHANGED_CONV SKOLEM_CONV))) 1488 >> RW_TAC std_ss [] 1489 >> Q.PAT_X_ASSUM `!x. f x = prob_embed (b'' x)` (MP_TAC o Q.SPEC `x`) 1490 >> Q.PAT_X_ASSUM `BIGUNION p = q` MP_TAC 1491 >> Q.PAT_X_ASSUM `prob_canonical p` MP_TAC 1492 >> Q.PAT_X_ASSUM `!x. prob_canonical (b'' x)` (MP_TAC o Q.SPEC `x`) 1493 >> Q.SPEC_TAC (`b'' x`, `B''`) 1494 >> KILL_TAC 1495 >> HO_MATCH_MP_TAC PROB_CANONICAL_CASES 1496 >> CONJ_TAC 1497 >- (RW_TAC std_ss [] 1498 >> Q.EXISTS_TAC `[]` 1499 >> Q.EXISTS_TAC `[]` 1500 >> RW_TAC prob_canon_ss []) 1501 >> REVERSE CONJ_TAC 1502 >- (RW_TAC std_ss [] 1503 >> PROVE_TAC []) 1504 >> RW_TAC std_ss [PROB_EMBED_BASIC] 1505 >> Q.EXISTS_TAC `b` 1506 >> Q.EXISTS_TAC `b'` 1507 >> MATCH_MP_TAC EQ_SYM 1508 >> MATCH_MP_TAC PROB_CANONICAL_UNIV 1509 >> Q.PAT_X_ASSUM `BIGUNION p = q` (ASM_REWRITE_TAC o wrap o GSYM) 1510 >> PSET_TAC [EXTENSION] 1511 >> PROVE_TAC []) 1512 >> RW_TAC std_ss [] 1513 >> RW_TAC std_ss [PROB_EMBED_APPEND, EMPTY_UNION, PROB_EMBED_TLS_EMPTY] 1514 >> Suff 1515 `(?N. !n. N <= n ==> (prob_embed (b1 n) = {})) /\ 1516 (?N. !n. N <= n ==> (prob_embed (b2 n) = {}))` 1517 >- (KILL_TAC 1518 >> RW_TAC std_ss [] 1519 >> Q.EXISTS_TAC `MAX N N'` 1520 >> RW_TAC std_ss [MAX_LE_X]) 1521 >> CONJ_TAC >| 1522 [Q.PAT_X_ASSUM `!f. P f ==> Q f` K_TAC 1523 >> Q.PAT_X_ASSUM `!f. P f ==> Q f` (MP_TAC o Q.SPEC `prob_embed o b1`) 1524 >> RW_TAC std_ss [o_THM, IN_PROB_ALGEBRA, AND_IMP_INTRO, GSYM CONJ_ASSOC] 1525 >> POP_ASSUM MATCH_MP_TAC 1526 >> CONJ_TAC >- PROVE_TAC [] 1527 >> CONJ_TAC 1528 >- (REPEAT STRIP_TAC 1529 >> Q.PAT_X_ASSUM `!m n. P m n` (MP_TAC o Q.SPECL [`m`, `n`]) 1530 >> RW_TAC std_ss [DISJOINT_DEF, PROB_EMBED_APPEND, 1531 EXTENSION, NOT_IN_EMPTY, IN_UNION, IN_INTER] 1532 >> POP_ASSUM (MP_TAC o Q.SPEC `scons T x`) 1533 >> RW_TAC std_ss [PROB_EMBED_TLS]) 1534 >> Q.PAT_X_ASSUM `BIGUNION p = q` MP_TAC 1535 >> ONCE_REWRITE_TAC [EXTENSION] 1536 >> RW_TAC std_ss [IN_BIGUNION_IMAGE, IN_UNIV, o_THM] 1537 >> POP_ASSUM (MP_TAC o Q.SPEC `scons T x`) 1538 >> RW_TAC std_ss [PROB_EMBED_TLS, PROB_EMBED_APPEND, IN_UNION], 1539 Q.PAT_X_ASSUM `!f. P f ==> Q f` (MP_TAC o Q.SPEC `prob_embed o b2`) 1540 >> Q.PAT_X_ASSUM `!f. P f ==> Q f` K_TAC 1541 >> RW_TAC std_ss [o_THM, IN_PROB_ALGEBRA, AND_IMP_INTRO, GSYM CONJ_ASSOC] 1542 >> POP_ASSUM MATCH_MP_TAC 1543 >> CONJ_TAC >- PROVE_TAC [] 1544 >> CONJ_TAC 1545 >- (REPEAT STRIP_TAC 1546 >> Q.PAT_X_ASSUM `!m n. P m n` (MP_TAC o Q.SPECL [`m`, `n`]) 1547 >> RW_TAC std_ss [DISJOINT_DEF, PROB_EMBED_APPEND, 1548 EXTENSION, NOT_IN_EMPTY, IN_UNION, IN_INTER] 1549 >> POP_ASSUM (MP_TAC o Q.SPEC `scons F x`) 1550 >> RW_TAC std_ss [PROB_EMBED_TLS]) 1551 >> Q.PAT_X_ASSUM `BIGUNION p = q` MP_TAC 1552 >> ONCE_REWRITE_TAC [EXTENSION] 1553 >> RW_TAC std_ss [IN_BIGUNION_IMAGE, IN_UNIV, o_THM] 1554 >> POP_ASSUM (MP_TAC o Q.SPEC `scons F x`) 1555 >> RW_TAC std_ss [PROB_EMBED_TLS, PROB_EMBED_APPEND, IN_UNION]]); 1556 1557val PROB_MEASURE_COUNTABLY_ADDITIVE = store_thm 1558 ("PROB_MEASURE_COUNTABLY_ADDITIVE", 1559 ``countably_additive (space prob_algebra, subsets prob_algebra, prob_measure)``, 1560 RW_TAC std_ss [countably_additive_def, measure_def, measurable_sets_def] 1561 >> MP_TAC (Q.SPEC `f` ALGEBRA_COUNTABLE_UNION) 1562 >> RW_TAC std_ss [] 1563 >> Q.PAT_X_ASSUM `BIGUNION p IN q` MP_TAC 1564 >> Know `BIGUNION (IMAGE f UNIV) = BIGUNION (IMAGE f (count N))` 1565 >- ( PSET_TAC [EXTENSION] >> PROVE_TAC [NOT_LESS] ) 1566 >> DISCH_THEN (REWRITE_TAC o wrap) 1567 >> STRIP_TAC 1568 >> (MP_TAC o Q.SPECL [`f`, `N`]) 1569 (ISPEC ``(space prob_algebra, subsets prob_algebra, prob_measure)`` ADDITIVE_SUM) 1570 >> ASSUME_TAC SPACE_SUBSETS_PROB_ALGEBRA 1571 >> RW_TAC std_ss [PROB_ALGEBRA_ALGEBRA, PROB_MEASURE_POSITIVE, 1572 PROB_MEASURE_ADDITIVE, measure_def, measurable_sets_def, m_space_def] 1573 >> POP_ASSUM (REWRITE_TAC o wrap o GSYM) 1574 >> MATCH_MP_TAC SER_0 1575 >> RW_TAC std_ss [o_THM, PROB_MEASURE_BASIC]); 1576 1577val PROB_EMBED_PREFIX_SET = store_thm 1578 ("PROB_EMBED_PREFIX_SET", 1579 ``!l. prob_embed [l] = prefix_set l``, 1580 PSET_TAC [PROB_EMBED_CONS, PROB_EMBED_NIL, EXTENSION]); 1581 1582val PROB_ALGEBRA_PREFIX_SET = store_thm 1583 ("PROB_ALGEBRA_PREFIX_SET", 1584 ``!l. prefix_set l IN (subsets prob_algebra)``, 1585 RW_TAC std_ss [IN_PROB_ALGEBRA, GSYM PROB_EMBED_PREFIX_SET] 1586 >> PROVE_TAC []); 1587 1588val PROB_MEASURE_PREFIX_SET = store_thm 1589 ("PROB_MEASURE_PREFIX_SET", 1590 ``!l. prob_measure (prefix_set l) = (1 / 2) pow (LENGTH l)``, 1591 RW_TAC prob_canon_ss [GSYM PROB_EMBED_PREFIX_SET, PROB_MEASURE_ALT, 1592 prob_premeasure_def, REAL_ADD_RID]); 1593 1594val PREMEASURABLE_PROB_ALGEBRA_STL = store_thm 1595 ("PREMEASURABLE_PROB_ALGEBRA_STL", 1596 ``stl IN premeasurable prob_algebra prob_algebra``, 1597 RW_TAC std_ss [IN_PREMEASURABLE, PROB_ALGEBRA_ALGEBRA, PREIMAGE_def, 1598 SPACE_PROB_ALGEBRA, space_def, subsets_def, IN_FUNSET, IN_UNIV] 1599 >> Suff `{x | stl x IN s} = (s o stl)` 1600 >- PROVE_TAC [PROB_ALGEBRA_STL, PROB_ALGEBRA_UNIV, INTER_COMM, INTER_UNIV] 1601 >> ONCE_REWRITE_TAC [EXTENSION] 1602 >> RW_TAC std_ss [GSPECIFICATION, IN_o]); 1603 1604val PREMEASURABLE_PROB_ALGEBRA_SDROP = store_thm 1605 ("PREMEASURABLE_PROB_ALGEBRA_SDROP", 1606 ``!n. sdrop n IN premeasurable prob_algebra prob_algebra``, 1607 Induct >- RW_TAC std_ss [PROB_ALGEBRA_ALGEBRA, PREMEASURABLE_I, sdrop_def] 1608 >> RW_TAC std_ss [sdrop_def] 1609 >> MATCH_MP_TAC PREMEASURABLE_COMP 1610 >> Q.EXISTS_TAC `prob_algebra` 1611 >> RW_TAC std_ss [PREMEASURABLE_PROB_ALGEBRA_STL]); 1612 1613val PROB_ALGEBRA_SCONS = store_thm 1614 ("PROB_ALGEBRA_SCONS", 1615 ``!p. (!b. (p o scons b) IN (subsets prob_algebra)) = p IN (subsets prob_algebra)``, 1616 RW_TAC std_ss [IN_PROB_ALGEBRA] 1617 >> EQ_TAC 1618 >- (ONCE_REWRITE_TAC [EXTENSION] 1619 >> DISCH_THEN 1620 (fn th => (MP_TAC (Q.SPEC `T` th) >> MP_TAC (Q.SPEC `F` th))) 1621 >> RW_TAC std_ss [IN_o] 1622 >> Q.EXISTS_TAC `APPEND (MAP (CONS T) b'') (MAP (CONS F) b')` 1623 >> RW_TAC std_ss [] 1624 >> MP_TAC (Q.ISPEC `x : num -> bool` SCONS_SURJ) 1625 >> RW_TAC std_ss [] 1626 >> RW_TAC std_ss [PROB_EMBED_TLS, PROB_EMBED_APPEND, IN_UNION] 1627 >> Cases_on `h` 1628 >> PROVE_TAC []) 1629 >> RW_TAC std_ss [] 1630 >> ONCE_REWRITE_TAC [GSYM PROB_CANON_EMBED] 1631 >> Know `prob_canonical (prob_canon b)` 1632 >- PROVE_TAC [prob_canonical_def, PROB_CANON_IDEMPOT] 1633 >> Q.SPEC_TAC (`prob_canon b`, `l`) 1634 >> REWRITE_TAC [PROB_CANON_EMBED] 1635 >> HO_MATCH_MP_TAC PROB_CANONICAL_CASES 1636 >> CONJ_TAC 1637 >- (Q.EXISTS_TAC `[]` 1638 >> PSET_TAC [PROB_EMBED_BASIC, EXTENSION]) 1639 >> CONJ_TAC 1640 >- (Q.EXISTS_TAC `[[]]` 1641 >> PSET_TAC [PROB_EMBED_BASIC, EXTENSION]) 1642 >> PSET_TAC [PROB_EMBED_APPEND, PROB_EMBED_TLS, EXTENSION] 1643 >> Cases_on `b'` 1644 >> PROVE_TAC []); 1645 1646val PREMEASURABLE_PROB_ALGEBRA_SCONS = store_thm 1647 ("PREMEASURABLE_PROB_ALGEBRA_SCONS", 1648 ``!b. scons b IN premeasurable prob_algebra prob_algebra``, 1649 ASSUME_TAC SPACE_PROB_ALGEBRA 1650 >> RW_TAC std_ss [IN_PREMEASURABLE, PROB_ALGEBRA_ALGEBRA, PREIMAGE_def, IN_FUNSET, IN_UNIV] 1651 >> Suff `{x | scons b x IN s} = s o scons b` 1652 >- PROVE_TAC [PROB_ALGEBRA_SCONS, INTER_UNIV] 1653 >> ONCE_REWRITE_TAC [EXTENSION] 1654 >> RW_TAC std_ss [GSPECIFICATION, IN_o]); 1655 1656val PROB_MEASURE_STL = store_thm 1657 ("PROB_MEASURE_STL", 1658 ``!a. a IN (subsets prob_algebra) ==> (prob_measure (a o stl) = prob_measure a)``, 1659 RW_TAC std_ss [] 1660 >> Know `(a o stl) IN (subsets prob_algebra)` >- RW_TAC std_ss [PROB_ALGEBRA_STL] 1661 >> RW_TAC std_ss [GSYM PREIMAGE_ALT] 1662 >> REPEAT (POP_ASSUM MP_TAC) 1663 >> RW_TAC std_ss [IN_PROB_ALGEBRA] 1664 >> RW_TAC std_ss [PROB_MEASURE_ALT] 1665 >> REPEAT (POP_ASSUM MP_TAC) 1666 >> Suff 1667 `!c. 1668 prob_canonical c ==> 1669 !b. 1670 prob_canonical b ==> 1671 (PREIMAGE stl (prob_embed b) = prob_embed c) ==> 1672 (prob_premeasure b = prob_premeasure c)` 1673 >- (DISCH_THEN (MP_TAC o Q.SPEC `prob_canon b'`) 1674 >> RW_TAC std_ss [prob_canonical_def, PROB_CANON_EMBED, 1675 PROB_CANON_IDEMPOT]) 1676 >> HO_MATCH_MP_TAC PROB_CANONICAL_CASES 1677 >> RW_TAC std_ss [PROB_EMBED_BASIC, PROB_PREMEASURE_BASIC, o_DEF] >| 1678 [Suff `b = []` >- RW_TAC std_ss [PROB_PREMEASURE_BASIC] 1679 >> Suff `prob_embed b = {}` >- RW_TAC std_ss [PROB_CANONICAL_EMBED_EMPTY] 1680 >> POP_ASSUM MP_TAC 1681 >> RW_TAC std_ss [EXTENSION, NOT_IN_EMPTY] 1682 >> POP_ASSUM (MP_TAC o Q.SPEC `scons T x`) 1683 >> RW_TAC std_ss [STL_SCONS, IN_PREIMAGE], 1684 Suff `b = [[]]` >- RW_TAC std_ss [PROB_PREMEASURE_BASIC] 1685 >> Suff `prob_embed b = UNIV` >- RW_TAC std_ss [PROB_CANONICAL_EMBED_UNIV] 1686 >> POP_ASSUM MP_TAC 1687 >> RW_TAC std_ss [EXTENSION, IN_UNIV] 1688 >> POP_ASSUM (MP_TAC o Q.SPEC `scons T x`) 1689 >> RW_TAC std_ss [STL_SCONS, IN_PREIMAGE], 1690 Know `l1 = l2` 1691 >- (Suff `prob_canon l1 = prob_canon l2` >- PROVE_TAC [prob_canonical_def] 1692 >> PSET_TAC [PROB_CANON_REP, EXTENSION] 1693 >> POP_ASSUM (fn th => MP_TAC (Q.SPEC `scons T x` th) 1694 >> MP_TAC (Q.SPEC `scons F x` th)) 1695 >> PSET_TAC [SHD_SCONS, STL_SCONS, PROB_EMBED_APPEND, 1696 PROB_EMBED_TLS, EXTENSION]) 1697 >> RW_TAC std_ss [] 1698 >> Know `b = l1` 1699 >- (Suff `prob_canon b = prob_canon l1` >- PROVE_TAC [prob_canonical_def] 1700 >> PSET_TAC [PROB_CANON_REP, EXTENSION] 1701 >> POP_ASSUM (MP_TAC o Q.SPEC `scons T x`) 1702 >> PSET_TAC [SHD_SCONS, STL_SCONS, PROB_EMBED_APPEND, 1703 PROB_EMBED_TLS, EXTENSION]) 1704 >> RW_TAC std_ss [] 1705 >> Know `!a b : real. (2 * a = 2 * b) ==> (a = b)` >- REAL_ARITH_TAC 1706 >> DISCH_THEN MATCH_MP_TAC 1707 >> RW_TAC std_ss [PROB_PREMEASURE_APPEND, PROB_PREMEASURE_TLS, 1708 REAL_ADD_LDISTRIB] 1709 >> REAL_ARITH_TAC]); 1710 1711val PROB_MEASURE_SDROP = store_thm 1712 ("PROB_MEASURE_SDROP", 1713 ``!n a. 1714 a IN (subsets prob_algebra) ==> (prob_measure (a o sdrop n) = prob_measure a)``, 1715 Induct >- RW_TAC std_ss' [sdrop_def, o_DEF, I_THM] 1716 >> RW_TAC bool_ss [sdrop_def, o_ASSOC, PROB_MEASURE_STL, PROB_ALGEBRA_SDROP]); 1717 1718val PROB_PRESERVING_PROB_ALGEBRA_STL = store_thm 1719 ("PROB_PRESERVING_PROB_ALGEBRA_STL", 1720 ``stl IN prob_preserving (space prob_algebra, subsets prob_algebra, prob_measure) 1721 (space prob_algebra, subsets prob_algebra, prob_measure)``, 1722 ASSUME_TAC SPACE_SUBSETS_PROB_ALGEBRA 1723 >> RW_TAC std_ss [PROB_PRESERVING, GSPECIFICATION, EVENTS, PROB, 1724 PREMEASURABLE_PROB_ALGEBRA_STL, PREIMAGE_ALT, 1725 p_space_def, m_space_def] 1726 >> ASSUME_TAC SPACE_PROB_ALGEBRA 1727 >> POP_ORW 1728 >> RW_TAC std_ss [PROB_MEASURE_STL, INTER_UNIV]); 1729 1730val PROB_PRESERVING_PROB_ALGEBRA_SDROP = store_thm 1731 ("PROB_PRESERVING_PROB_ALGEBRA_SDROP", 1732 ``!n. sdrop n IN 1733 prob_preserving (space prob_algebra, subsets prob_algebra, prob_measure) 1734 (space prob_algebra, subsets prob_algebra, prob_measure)``, 1735 ASSUME_TAC SPACE_SUBSETS_PROB_ALGEBRA 1736 >> RW_TAC std_ss [PROB_PRESERVING, GSPECIFICATION, EVENTS, PROB, 1737 PREMEASURABLE_PROB_ALGEBRA_SDROP, PREIMAGE_ALT, 1738 p_space_def, m_space_def] 1739 >> ASSUME_TAC SPACE_PROB_ALGEBRA 1740 >> POP_ORW 1741 >> RW_TAC std_ss [PROB_MEASURE_SDROP, INTER_UNIV]); 1742 1743val MIRROR_MIRROR = store_thm 1744 ("MIRROR_MIRROR", 1745 ``!x. mirror (mirror x) = x``, 1746 RW_TAC std_ss [mirror_def, SHD_SCONS, STL_SCONS, SCONS_SHD_STL]); 1747 1748val MIRROR_o_MIRROR = store_thm 1749 ("MIRROR_o_MIRROR", 1750 ``mirror o mirror = I``, 1751 FUN_EQ_TAC 1752 >> RW_TAC std_ss [o_THM, I_THM, MIRROR_MIRROR]); 1753 1754val MIRROR_SCONS = store_thm 1755 ("MIRROR_SCONS", 1756 ``!b x. mirror (scons b x) = scons (~b) x``, 1757 RW_TAC std_ss [mirror_def, SHD_SCONS, STL_SCONS]); 1758 1759val PREIMAGE_MIRROR_TLS = store_thm 1760 ("PREIMAGE_MIRROR_TLS", 1761 ``!l1 l2. 1762 PREIMAGE mirror (prob_embed (APPEND (MAP (CONS T) l1) (MAP (CONS F) l2))) 1763 = 1764 prob_embed (APPEND (MAP (CONS T) l2) (MAP (CONS F) l1))``, 1765 PSET_TAC [EXTENSION] 1766 >> MP_TAC (Q.ISPEC `x : num -> bool` SCONS_SURJ) 1767 >> RW_TAC std_ss [] 1768 >> RW_TAC std_ss [MIRROR_SCONS, PROB_EMBED_APPEND, IN_UNION, PROB_EMBED_TLS] 1769 >> PROVE_TAC []); 1770 1771val PREMEASURABLE_PROB_ALGEBRA_MIRROR = store_thm 1772 ("PREMEASURABLE_PROB_ALGEBRA_MIRROR", 1773 ``mirror IN premeasurable prob_algebra prob_algebra``, 1774 RW_TAC std_ss [IN_PREMEASURABLE, IN_PROB_ALGEBRA, PROB_ALGEBRA_ALGEBRA, 1775 IN_FUNSET, IN_UNIV, INTER_UNIV, SPACE_PROB_ALGEBRA] 1776 >> Suff 1777 `!b. 1778 prob_canonical b ==> 1779 ?c. PREIMAGE mirror (prob_embed b) = prob_embed c` 1780 >- ( DISCH_THEN (MP_TAC o Q.SPEC `prob_canon b`) \\ 1781 RW_TAC std_ss [prob_canonical_def, PROB_CANON_IDEMPOT, PROB_CANON_EMBED] ) 1782 >> HO_MATCH_MP_TAC PROB_CANONICAL_CASES 1783 >> CONJ_TAC 1784 >- ( Q.EXISTS_TAC `[]` \\ 1785 RW_TAC std_ss [PREIMAGE_EMPTY, PROB_EMBED_BASIC] ) 1786 >> CONJ_TAC 1787 >- ( Q.EXISTS_TAC `[[]]` \\ 1788 RW_TAC std_ss [PREIMAGE_UNIV, PROB_EMBED_BASIC] ) 1789 >> RW_TAC std_ss [PREIMAGE_MIRROR_TLS] 1790 >> PROVE_TAC []); 1791 1792val PROB_ALGEBRA_MIRROR = store_thm 1793 ("PROB_ALGEBRA_MIRROR", 1794 ``!p. p o mirror IN (subsets prob_algebra) = p IN (subsets prob_algebra)``, 1795 MP_TAC PREMEASURABLE_PROB_ALGEBRA_MIRROR 1796 >> RW_TAC std_ss [IN_PREMEASURABLE, PREIMAGE_ALT, INTER_UNIV, SPACE_PROB_ALGEBRA] 1797 >> REVERSE EQ_TAC >- PROVE_TAC [] 1798 >> POP_ASSUM (MP_TAC o Q.SPEC `p o mirror`) 1799 >> RW_TAC std_ss [GSYM o_ASSOC, MIRROR_o_MIRROR, I_o_ID]); 1800 1801val PROB_MEASURE_MIRROR = store_thm 1802 ("PROB_MEASURE_MIRROR", 1803 ``!a. a IN (subsets prob_algebra) ==> (prob_measure (a o mirror) = prob_measure a)``, 1804 RW_TAC std_ss [IN_PROB_ALGEBRA_CANONICAL, GSYM PREIMAGE_ALT] 1805 >> POP_ASSUM MP_TAC 1806 >> Q.SPEC_TAC (`b`, `b`) 1807 >> HO_MATCH_MP_TAC PROB_CANONICAL_CASES 1808 >> CONJ_TAC >- RW_TAC std_ss [PROB_EMBED_BASIC, PREIMAGE_EMPTY] 1809 >> CONJ_TAC >- RW_TAC std_ss [PROB_EMBED_BASIC, PREIMAGE_UNIV] 1810 >> RW_TAC std_ss [PREIMAGE_MIRROR_TLS, PROB_MEASURE_ALT] 1811 >> Know `prob_canonical (APPEND (MAP (CONS T) l2) (MAP (CONS F) l1))` 1812 >- (MP_TAC (Q.SPECL [`l2`, `l1`] PROB_CANONICAL_STEP) 1813 >> Know `~((l2 = [[]]) /\ (l1 = [[]]))` 1814 >- (STRIP_TAC 1815 >> Q.PAT_X_ASSUM `prob_canonical x` MP_TAC 1816 >> RW_TAC prob_canon_ss [prob_canonical_def]) 1817 >> RW_TAC std_ss []) 1818 >> POP_ASSUM MP_TAC 1819 >> RW_TAC std_ss [prob_canonical_def] 1820 >> RW_TAC std_ss [PROB_PREMEASURE_APPEND] 1821 >> KILL_TAC 1822 >> Know `!a b : real. (2 * a = 2 * b) ==> (a = b)` >- REAL_ARITH_TAC 1823 >> DISCH_THEN MATCH_MP_TAC 1824 >> RW_TAC std_ss [REAL_ADD_LDISTRIB, PROB_PREMEASURE_TLS] 1825 >> REAL_ARITH_TAC); 1826 1827val PROB_PRESERVING_PROB_ALGEBRA_MIRROR = store_thm 1828 ("PROB_PRESERVING_PROB_ALGEBRA_MIRROR", 1829 ``mirror IN 1830 prob_preserving (space prob_algebra, subsets prob_algebra, prob_measure) 1831 (space prob_algebra, subsets prob_algebra, prob_measure)``, 1832 ASSUME_TAC SPACE_SUBSETS_PROB_ALGEBRA 1833 >> RW_TAC std_ss [PROB_PRESERVING, GSPECIFICATION, EVENTS, PROB, 1834 PREMEASURABLE_PROB_ALGEBRA_MIRROR, PREIMAGE_ALT, 1835 p_space_def, m_space_def] 1836 >> ASSUME_TAC SPACE_PROB_ALGEBRA 1837 >> POP_ORW 1838 >> RW_TAC std_ss [PROB_MEASURE_MIRROR, INTER_UNIV]); 1839 1840val PREIMAGE_SHD_SING = store_thm 1841 ("PREIMAGE_SHD_SING", 1842 ``!b. PREIMAGE shd {b} = halfspace b``, 1843 RW_TAC std_ss [EXTENSION, IN_HALFSPACE, IN_PREIMAGE, IN_SING]); 1844 1845val PREIMAGE_SHD_CASES = store_thm 1846 ("PREIMAGE_SHD_CASES", 1847 ``!x. 1848 (PREIMAGE shd x = {}) \/ (PREIMAGE shd x = UNIV) \/ 1849 (?b. PREIMAGE shd x = halfspace b)``, 1850 HO_MATCH_MP_TAC BOOL_SET_CASES 1851 >> RW_TAC std_ss [PREIMAGE_EMPTY, PREIMAGE_UNIV, PREIMAGE_SHD_SING] 1852 >> PROVE_TAC []); 1853 1854val PROB_ALGEBRA_SHD = store_thm 1855 ("PROB_ALGEBRA_SHD", 1856 ``!x. (x o shd) IN (subsets prob_algebra)``, 1857 STRIP_TAC 1858 >> MP_TAC (Q.SPEC `x` PREIMAGE_SHD_CASES) 1859 >> RW_TAC std_ss [PREIMAGE_ALT] 1860 >> RW_TAC std_ss [PROB_ALGEBRA_BASIC]); 1861 1862val HALFSPACE_T_UNION_F = store_thm 1863 ("HALFSPACE_T_UNION_F", 1864 ``halfspace T UNION halfspace F = UNIV``, 1865 RW_TAC std_ss [EXTENSION, IN_UNION, IN_UNIV, IN_HALFSPACE]); 1866 1867val EXIST_LONG_PREFIX_SETS = store_thm 1868 ("EXIST_LONG_PREFIX_SETS", 1869 ``!x n. ?l. (LENGTH l = n) /\ x IN prefix_set l``, 1870 REPEAT GEN_TAC 1871 >> Q.SPEC_TAC (`x`, `x`) 1872 >> Induct_on `n` 1873 >- (RW_TAC std_ss [] 1874 >> Q.EXISTS_TAC `[]` 1875 >> RW_TAC std_ss [LENGTH, prefix_set_def, IN_UNIV]) 1876 >> RW_TAC std_ss [] 1877 >> SEQ_CASES_TAC `x` 1878 >> POP_ASSUM (MP_TAC o Q.SPEC `t`) 1879 >> RW_TAC std_ss [] 1880 >> Q.EXISTS_TAC `h :: l` 1881 >> RW_TAC std_ss [LENGTH, prefix_set_def, IN_INTER, IN_o, IN_HALFSPACE, 1882 SHD_SCONS, STL_SCONS]); 1883 1884val PREFIX_SET_APPEND = store_thm 1885 ("PREFIX_SET_APPEND", 1886 ``!s l1 l2. s IN prefix_set (APPEND l1 l2) ==> s IN prefix_set l1``, 1887 Induct_on `l1` >- RW_TAC std_ss [prefix_set_def, IN_UNIV] 1888 >> RW_TAC std_ss [APPEND] 1889 >> SEQ_CASES_TAC `s` 1890 >> POP_ASSUM MP_TAC 1891 >> RW_TAC std_ss [PREFIX_SET_SCONS] 1892 >> PROVE_TAC []); 1893 1894val IS_PREFIX_APPEND1 = store_thm 1895 ("IS_PREFIX_APPEND1", 1896 ``!a b c. IS_PREFIX c (APPEND a b) ==> IS_PREFIX c a``, 1897 Induct >- RW_TAC std_ss [IS_PREFIX] 1898 >> RW_TAC std_ss [] 1899 >> Cases_on `c` 1900 >> POP_ASSUM MP_TAC 1901 >> RW_TAC std_ss [IS_PREFIX, APPEND] 1902 >> PROVE_TAC []); 1903 1904val IS_PREFIX_APPEND2 = store_thm 1905 ("IS_PREFIX_APPEND2", 1906 ``!a b c. IS_PREFIX (APPEND b c) a ==> IS_PREFIX b a \/ IS_PREFIX a b``, 1907 Induct >- RW_TAC std_ss [IS_PREFIX] 1908 >> RW_TAC std_ss [] 1909 >> Cases_on `b` >- RW_TAC std_ss [IS_PREFIX] 1910 >> POP_ASSUM MP_TAC 1911 >> RW_TAC std_ss [IS_PREFIX, APPEND] 1912 >> PROVE_TAC []); 1913 1914val IS_PREFIX_APPENDS = store_thm 1915 ("IS_PREFIX_APPENDS", 1916 ``!a b c. IS_PREFIX (APPEND a c) (APPEND a b) = IS_PREFIX c b``, 1917 Induct >- RW_TAC std_ss [APPEND] 1918 >> RW_TAC std_ss [APPEND, IS_PREFIX]); 1919 1920val PREFIX_SET_UNFIXED_SDROP = store_thm 1921 ("PREFIX_SET_UNFIXED_SDROP", 1922 ``!l n. ?s. s IN prefix_set l /\ ~(sdrop (SUC n) s = s)``, 1923 REPEAT GEN_TAC 1924 >> Induct_on `l` 1925 >- (Q.EXISTS_TAC `FUNPOW (scons T) (SUC n) (scons F s)` 1926 >> RW_TAC std_ss [prefix_set_def, IN_UNIV] 1927 >> ONCE_REWRITE_TAC [FUNPOW_SUC, sdrop_def] 1928 >> RW_TAC std_ss [o_THM, I_THM, STL_SCONS] 1929 >> Suff `!t. ~(sdrop n (FUNPOW (scons T) n (scons F s)) = scons T t)` 1930 >- PROVE_TAC [] 1931 >> GEN_TAC 1932 >> Induct_on `n` >- RW_TAC std_ss [sdrop_def, FUNPOW, I_THM, SCONS_EQ] 1933 >> RW_TAC std_ss [sdrop_def, o_THM, FUNPOW_SUC, STL_SCONS]) 1934 >> POP_ASSUM MP_TAC 1935 >> REPEAT STRIP_TAC 1936 >> Q.EXISTS_TAC `scons h s` 1937 >> RW_TAC bool_ss [prefix_set_def, IN_INTER, IN_HALFSPACE, IN_o, SHD_SCONS, 1938 STL_SCONS] 1939 >> STRIP_TAC 1940 >> Q.PAT_X_ASSUM `~(X = Y)` MP_TAC 1941 >> Know `(stl o sdrop (SUC n)) (scons h s) = stl (scons h s)` 1942 >- RW_TAC std_ss [o_THM] 1943 >> RW_TAC bool_ss [STL_o_SDROP] 1944 >> POP_ASSUM MP_TAC 1945 >> RW_TAC std_ss [sdrop_def, STL_SCONS, o_THM]); 1946 1947val PREFIX_SET_UNFIXED_STL = store_thm 1948 ("PREFIX_SET_UNFIXED_STL", 1949 ``!l. ?s. s IN prefix_set l /\ ~(stl s = s)``, 1950 GEN_TAC 1951 >> MP_TAC (Q.SPECL [`l`, `0`] PREFIX_SET_UNFIXED_SDROP) 1952 >> RW_TAC bool_ss [sdrop_def, I_o_ID]); 1953 1954val SDROP_APPEND = store_thm 1955 ("SDROP_APPEND", 1956 ``!s x y. 1957 s IN prefix_set (APPEND x y) = 1958 s IN prefix_set x /\ sdrop (LENGTH x) s IN prefix_set y``, 1959 Induct_on `x` 1960 >- RW_TAC list_ss [sdrop_def, I_THM, APPEND, LENGTH, prefix_set_def, IN_UNIV] 1961 >> RW_TAC list_ss [sdrop_def, o_THM] 1962 >> SEQ_CASES_TAC `s` 1963 >> FULL_SIMP_TAC std_ss [PREFIX_SET_SCONS, STL_SCONS] 1964 >> PROVE_TAC []); 1965 1966val SDROP_PREFIX_SEQ_APPEND = store_thm 1967 ("SDROP_PREFIX_SEQ_APPEND", 1968 ``!s x y. sdrop (LENGTH x) (prefix_seq (APPEND x y)) = prefix_seq y``, 1969 Induct_on `x` >- RW_TAC list_ss [sdrop_def, I_THM] 1970 >> RW_TAC list_ss [sdrop_def, o_THM, APPEND, prefix_seq_def] 1971 >> FULL_SIMP_TAC std_ss [PREFIX_SET_SCONS, STL_SCONS]); 1972 1973val PREFIX_SET_INJ = store_thm 1974 ("PREFIX_SET_INJ", 1975 ``!a b. (prefix_set a = prefix_set b) = (a = b)``, 1976 Induct 1977 >- (RW_TAC std_ss [PREFIX_SET_BASIC] 1978 >> PROVE_TAC [PREFIX_SET_NIL]) 1979 >> Cases_on `b` >- RW_TAC std_ss [PREFIX_SET_BASIC, PREFIX_SET_NIL] 1980 >> RW_TAC std_ss [] 1981 >> Cases_on `h = h'` 1982 >- (RW_TAC std_ss [] 1983 >> REVERSE EQ_TAC >- RW_TAC std_ss [] 1984 >> SET_EQ_TAC 1985 >> RW_TAC std_ss [] 1986 >> Q.PAT_X_ASSUM `!b. (P b = Q b) = R b` (REWRITE_TAC o wrap o GSYM) 1987 >> SET_EQ_TAC 1988 >> GEN_TAC 1989 >> POP_ASSUM (MP_TAC o Q.SPEC `scons h x`) 1990 >> RW_TAC std_ss [PREFIX_SET_SCONS]) 1991 >> RW_TAC std_ss [] 1992 >> SET_EQ_TAC 1993 >> STRIP_TAC 1994 >> POP_ASSUM (MP_TAC o Q.SPEC `scons h (prefix_seq t)`) 1995 >> RW_TAC std_ss [PREFIX_SET_SCONS, PREFIX_SEQ]); 1996 1997val STL_MIRROR = store_thm 1998 ("STL_MIRROR", 1999 ``!x. stl (mirror x) = stl x``, 2000 GEN_TAC 2001 >> SEQ_CASES_TAC `x` 2002 >> RW_TAC std_ss [STL_SCONS, MIRROR_SCONS]); 2003 2004val MIRROR_NEQ = store_thm 2005 ("MIRROR_NEQ", 2006 ``!x. ~(mirror x = x)``, 2007 GEN_TAC 2008 >> SEQ_CASES_TAC `x` 2009 >> RW_TAC std_ss [MIRROR_SCONS, SCONS_EQ] 2010 >> Cases_on `h` 2011 >> PROVE_TAC []); 2012 2013val PREFIX_SET_ALT = store_thm 2014 ("PREFIX_SET_ALT", 2015 ``!l. prefix_set l = {s | stake (LENGTH l) s = l}``, 2016 Induct 2017 >- (SET_EQ_TAC 2018 >> RW_TAC std_ss [GSPECIFICATION, prefix_set_def, IN_UNIV, LENGTH, 2019 stake_def]) 2020 >> SET_EQ_TAC 2021 >> RW_TAC std_ss [GSPECIFICATION, prefix_set_def, IN_INTER, LENGTH, 2022 stake_def, IN_HALFSPACE, IN_o]); 2023 2024val IMAGE_MIRROR = store_thm 2025 ("IMAGE_MIRROR", 2026 ``IMAGE mirror = PREIMAGE mirror``, 2027 FUN_EQ_TAC 2028 >> SET_EQ_TAC 2029 >> PSET_TAC [] 2030 >> PROVE_TAC [MIRROR_MIRROR]); 2031 2032val _ = export_theory (); 2033