1(* ------------------------------------------------------------------------- *) 2(* The (shared) theory of sigma-algebra and other systems of sets (ring, *) 3(* semiring, and dynkin system) used in measureTheory/real_measureTheory *) 4(* *) 5(* Author: Chun Tian (2018-2020) *) 6(* Fondazione Bruno Kessler and University of Trento, Italy *) 7(* ------------------------------------------------------------------------- *) 8(* Based on the work of Tarek Mhamdi, Osman Hasan, Sofiene Tahar [3] *) 9(* HVG Group, Concordia University, Montreal (2013, 2015) *) 10(* *) 11(* With some further additions by M. Qasim & W. Ahmed (2019) *) 12(* ------------------------------------------------------------------------- *) 13(* Based on the work of Joe Hurd [1] (2001) and Aaron Coble [2] (2010) *) 14(* Cambridge University. *) 15(* ------------------------------------------------------------------------- *) 16 17open HolKernel Parse boolLib bossLib; 18 19open arithmeticTheory optionTheory pairTheory combinTheory pred_setTheory 20 pred_setLib numLib realLib seqTheory hurdUtils util_probTheory; 21 22val _ = new_theory "sigma_algebra"; 23 24val DISC_RW_KILL = DISCH_TAC >> ONCE_ASM_REWRITE_TAC [] >> POP_ASSUM K_TAC; 25fun METIS ths tm = prove(tm, METIS_TAC ths); 26val set_ss = std_ss ++ PRED_SET_ss; 27val std_ss' = std_ss ++ boolSimps.ETA_ss; 28 29val _ = hide "S"; 30 31(* ------------------------------------------------------------------------- *) 32(* Basic definitions. *) 33(* ------------------------------------------------------------------------- *) 34 35val _ = type_abbrev_pp ("algebra", ``:('a set) # ('a set set)``); 36 37val space_def = Define 38 `space (x :'a set, y :('a set) set) = x`; 39 40val subsets_def = Define 41 `subsets (x :'a set, y :('a set) set) = y`; 42 43val _ = export_rewrites ["space_def", "subsets_def"]; 44 45val subset_class_def = Define 46 `subset_class sp sts = !x. x IN sts ==> x SUBSET sp`; 47 48Definition algebra_def : 49 algebra a = 50 (subset_class (space a) (subsets a) /\ 51 {} IN subsets a /\ 52 (!s. s IN subsets a ==> space a DIFF s IN subsets a) /\ 53 (!s t. s IN subsets a /\ t IN subsets a ==> s UNION t IN subsets a)) 54End 55 56Definition sigma_algebra_def : 57 sigma_algebra a = 58 (algebra a /\ 59 !c. countable c /\ c SUBSET (subsets a) ==> BIGUNION c IN (subsets a)) 60End 61 62(* The set of measurable mappings, each (f :'a -> 'b) is called A/B-measurable *) 63val measurable_def = Define 64 `measurable a b = {f | sigma_algebra a /\ sigma_algebra b /\ 65 f IN (space a -> space b) /\ 66 !s. s IN subsets b ==> 67 ((PREIMAGE f s) INTER space a) IN subsets a}`; 68 69(* the smallest sigma algebra generated from a set of sets *) 70val sigma_def = Define 71 `sigma sp sts = (sp, BIGINTER {s | sts SUBSET s /\ sigma_algebra (sp, s)})`; 72 73Definition semiring_def : (* [7, p.39] *) 74 semiring r = 75 (subset_class (space r) (subsets r) /\ 76 {} IN (subsets r) /\ 77 (!s t. s IN (subsets r) /\ t IN (subsets r) ==> s INTER t IN (subsets r)) /\ 78 (!s t. s IN (subsets r) /\ t IN (subsets r) ==> 79 ?c. c SUBSET (subsets r) /\ FINITE c /\ disjoint c /\ 80 (s DIFF t = BIGUNION c))) 81End 82 83Definition ring_def : (* see [4] *) 84 ring r = 85 (subset_class (space r) (subsets r) /\ 86 {} IN (subsets r) /\ 87 (!s t. s IN (subsets r) /\ t IN (subsets r) ==> s UNION t IN (subsets r)) /\ 88 (!s t. s IN (subsets r) /\ t IN (subsets r) ==> s DIFF t IN (subsets r))) 89End 90 91(* the smallest ring generated from a set of sets (usually a semiring) *) 92val smallest_ring_def = Define 93 `smallest_ring sp sts = (sp, BIGINTER {s | sts SUBSET s /\ ring (sp, s)})`; 94 95(* named after Eugene B. Dynkin (1924-2014), a Soviet and American mathematician [5] *) 96Definition dynkin_system_def : 97 dynkin_system d = 98 (subset_class (space d) (subsets d) /\ 99 (space d) IN (subsets d) /\ 100 (!s. s IN (subsets d) ==> (space d DIFF s) IN (subsets d)) /\ 101 (!f :num -> 'a set. 102 f IN (UNIV -> (subsets d)) /\ (!i j. i <> j ==> DISJOINT (f i) (f j)) 103 ==> BIGUNION (IMAGE f UNIV) IN (subsets d))) 104End 105 106(* the smallest dynkin system generated from a set of sets, cf. "sigma_def" *) 107val dynkin_def = Define 108 `dynkin sp sts = (sp, BIGINTER {d | sts SUBSET d /\ dynkin_system (sp, d)})`; 109 110(* ------------------------------------------------------------------------- *) 111(* Basic theorems *) 112(* ------------------------------------------------------------------------- *) 113 114Theorem SPACE[simp] : 115 !a. (space a, subsets a) = a 116Proof 117 GEN_TAC >> Cases_on ���a��� >> rw [] 118QED 119 120val ALGEBRA_ALT_INTER = store_thm 121 ("ALGEBRA_ALT_INTER", 122 ``!a. 123 algebra a <=> 124 subset_class (space a) (subsets a) /\ 125 {} IN (subsets a) /\ (!s. s IN (subsets a) ==> (space a DIFF s) IN (subsets a)) /\ 126 !s t. s IN (subsets a) /\ t IN (subsets a) ==> s INTER t IN (subsets a)``, 127 RW_TAC std_ss [algebra_def, subset_class_def] 128 >> EQ_TAC >| 129 [RW_TAC std_ss [] 130 >> Know `s INTER t = space a DIFF ((space a DIFF s) UNION (space a DIFF t))` 131 >- (RW_TAC std_ss [EXTENSION, IN_INTER, IN_DIFF, IN_UNION] 132 >> EQ_TAC 133 >- (RW_TAC std_ss [] >> FULL_SIMP_TAC std_ss [SUBSET_DEF] >> PROVE_TAC []) 134 >> RW_TAC std_ss [] >> ASM_REWRITE_TAC []) 135 >> RW_TAC std_ss [], 136 RW_TAC std_ss [] 137 >> Know `s UNION t = space a DIFF ((space a DIFF s) INTER (space a DIFF t))` 138 >- (RW_TAC std_ss [EXTENSION, IN_INTER, IN_DIFF, IN_UNION] 139 >> EQ_TAC 140 >- (RW_TAC std_ss [] >> FULL_SIMP_TAC std_ss [SUBSET_DEF] >> PROVE_TAC []) 141 >> RW_TAC std_ss [] >> ASM_REWRITE_TAC []) 142 >> RW_TAC std_ss []]); 143 144val ALGEBRA_EMPTY = store_thm 145 ("ALGEBRA_EMPTY", 146 ``!a. algebra a ==> {} IN (subsets a)``, 147 RW_TAC std_ss [algebra_def]); 148 149val ALGEBRA_SPACE = store_thm 150 ("ALGEBRA_SPACE", 151 ``!a. algebra a ==> (space a) IN (subsets a)``, 152 RW_TAC std_ss [algebra_def] 153 >> PROVE_TAC [DIFF_EMPTY]); 154 155val ALGEBRA_COMPL = store_thm 156 ("ALGEBRA_COMPL", 157 ``!a s. algebra a /\ s IN (subsets a) ==> (space a DIFF s) IN (subsets a)``, 158 RW_TAC std_ss [algebra_def]); 159 160val ALGEBRA_UNION = store_thm 161 ("ALGEBRA_UNION", 162 ``!a s t. algebra a /\ s IN (subsets a) /\ t IN (subsets a) ==> s UNION t IN (subsets a)``, 163 RW_TAC std_ss [algebra_def]); 164 165val ALGEBRA_INTER = store_thm 166 ("ALGEBRA_INTER", 167 ``!a s t. algebra a /\ s IN (subsets a) /\ t IN (subsets a) ==> s INTER t IN (subsets a)``, 168 RW_TAC std_ss [ALGEBRA_ALT_INTER]); 169 170val ALGEBRA_DIFF = store_thm 171 ("ALGEBRA_DIFF", 172 ``!a s t. algebra a /\ s IN (subsets a) /\ t IN (subsets a) ==> s DIFF t IN (subsets a)``, 173 rpt STRIP_TAC 174 >> Know `s DIFF t = s INTER (space a DIFF t)` 175 >- (RW_TAC std_ss [EXTENSION, IN_DIFF, IN_INTER] 176 >> FULL_SIMP_TAC std_ss [algebra_def, SUBSET_DEF, subset_class_def] 177 >> PROVE_TAC []) 178 >> RW_TAC std_ss [ALGEBRA_INTER, ALGEBRA_COMPL]); 179 180fun shared_tactics tm = 181 rpt STRIP_TAC >> MATCH_MP_TAC tm >> fs [sigma_algebra_def]; 182 183Theorem SIGMA_ALGEBRA_EMPTY : 184 !a. sigma_algebra a ==> {} IN (subsets a) 185Proof 186 shared_tactics ALGEBRA_EMPTY 187QED 188 189Theorem SIGMA_ALGEBRA_SPACE : 190 !a. sigma_algebra a ==> (space a) IN (subsets a) 191Proof 192 shared_tactics ALGEBRA_SPACE 193QED 194 195Theorem SIGMA_ALGEBRA_COMPL : 196 !a s. sigma_algebra a /\ s IN (subsets a) ==> (space a DIFF s) IN (subsets a) 197Proof 198 shared_tactics ALGEBRA_COMPL 199QED 200 201Theorem SIGMA_ALGEBRA_UNION : 202 !a s t. sigma_algebra a /\ s IN (subsets a) /\ t IN (subsets a) ==> 203 s UNION t IN (subsets a) 204Proof 205 shared_tactics ALGEBRA_UNION 206QED 207 208Theorem SIGMA_ALGEBRA_INTER : 209 !a s t. sigma_algebra a /\ s IN (subsets a) /\ t IN (subsets a) ==> 210 s INTER t IN (subsets a) 211Proof 212 shared_tactics ALGEBRA_INTER 213QED 214 215Theorem SIGMA_ALGEBRA_DIFF : 216 !a s t. sigma_algebra a /\ s IN (subsets a) /\ t IN (subsets a) ==> 217 s DIFF t IN (subsets a) 218Proof 219 shared_tactics ALGEBRA_DIFF 220QED 221 222val ALGEBRA_FINITE_UNION = store_thm 223 ("ALGEBRA_FINITE_UNION", 224 ``!a c. algebra a /\ FINITE c /\ c SUBSET (subsets a) ==> BIGUNION c IN (subsets a)``, 225 RW_TAC std_ss [algebra_def] 226 >> NTAC 2 (POP_ASSUM MP_TAC) 227 >> Q.SPEC_TAC (`c`, `c`) 228 >> HO_MATCH_MP_TAC FINITE_INDUCT 229 >> RW_TAC std_ss [BIGUNION_EMPTY, BIGUNION_INSERT, INSERT_SUBSET]); 230 231val ALGEBRA_INTER_SPACE = store_thm 232 ("ALGEBRA_INTER_SPACE", 233 ``!a s. algebra a /\ s IN subsets a ==> ((space a INTER s = s) /\ (s INTER space a = s))``, 234 RW_TAC std_ss [algebra_def, SUBSET_DEF, IN_INTER, EXTENSION, subset_class_def] 235 >> PROVE_TAC []); 236 237val SIGMA_ALGEBRA_ALT = store_thm 238 ("SIGMA_ALGEBRA_ALT", 239 ``!a. 240 sigma_algebra a <=> 241 algebra a /\ 242 (!f : num -> 'a -> bool. 243 f IN (UNIV -> (subsets a)) ==> BIGUNION (IMAGE f UNIV) IN (subsets a))``, 244 RW_TAC std_ss [sigma_algebra_def] 245 >> EQ_TAC 246 >- (RW_TAC std_ss [COUNTABLE_ALT, IN_FUNSET, IN_UNIV] 247 >> Q.PAT_X_ASSUM `!c. P c ==> Q c` MATCH_MP_TAC 248 >> reverse (RW_TAC std_ss [IN_IMAGE, SUBSET_DEF, IN_UNIV]) 249 >- PROVE_TAC [] 250 >> Q.EXISTS_TAC `f` 251 >> RW_TAC std_ss [] 252 >> PROVE_TAC []) 253 >> RW_TAC std_ss [COUNTABLE_ALT_BIJ] 254 >- PROVE_TAC [ALGEBRA_FINITE_UNION] 255 >> Q.PAT_X_ASSUM `!f. P f` (MP_TAC o Q.SPEC `\n. enumerate c n`) 256 >> RW_TAC std_ss' [IN_UNIV, IN_FUNSET] 257 >> Know `BIGUNION c = BIGUNION (IMAGE (enumerate c) UNIV)` 258 >- (RW_TAC std_ss [EXTENSION, IN_BIGUNION, IN_IMAGE, IN_UNIV] 259 >> Suff `!s. s IN c <=> ?n. (enumerate c n = s)` >- PROVE_TAC [] 260 >> Q.PAT_X_ASSUM `BIJ x y z` MP_TAC 261 >> RW_TAC std_ss [BIJ_DEF, SURJ_DEF, IN_UNIV] 262 >> PROVE_TAC []) 263 >> DISCH_THEN (REWRITE_TAC o wrap) 264 >> POP_ASSUM MATCH_MP_TAC 265 >> Strip 266 >> Suff `enumerate c n IN c` >- PROVE_TAC [SUBSET_DEF] 267 >> Q.PAT_X_ASSUM `BIJ i j k` MP_TAC 268 >> RW_TAC std_ss [BIJ_DEF, SURJ_DEF, IN_UNIV]); 269 270val SIGMA_ALGEBRA_ALT_MONO = store_thm 271 ("SIGMA_ALGEBRA_ALT_MONO", 272 ``!a. 273 sigma_algebra a <=> 274 algebra a /\ 275 (!f : num -> 'a -> bool. 276 f IN (UNIV -> (subsets a)) /\ (f 0 = {}) /\ (!n. f n SUBSET f (SUC n)) ==> 277 BIGUNION (IMAGE f UNIV) IN (subsets a))``, 278 RW_TAC std_ss [SIGMA_ALGEBRA_ALT] 279 >> EQ_TAC >- PROVE_TAC [] 280 >> RW_TAC std_ss [] 281 >> Q.PAT_X_ASSUM `!f. P f` 282 (MP_TAC o Q.SPEC `\n. BIGUNION (IMAGE f (count n))`) 283 >> RW_TAC std_ss [IN_UNIV, IN_FUNSET] 284 >> Know `BIGUNION (IMAGE f UNIV) = 285 BIGUNION (IMAGE (\n. BIGUNION (IMAGE f (count n))) UNIV)` 286 >- (KILL_TAC 287 >> ONCE_REWRITE_TAC [EXTENSION] 288 >> RW_TAC std_ss [IN_BIGUNION, IN_IMAGE, IN_UNIV] 289 >> EQ_TAC 290 >- (RW_TAC std_ss [] 291 >> Q.EXISTS_TAC `BIGUNION (IMAGE f (count (SUC x')))` 292 >> RW_TAC std_ss [IN_BIGUNION, IN_IMAGE, IN_COUNT] 293 >> PROVE_TAC [prim_recTheory.LESS_SUC_REFL]) 294 >> RW_TAC std_ss [] 295 >> POP_ASSUM MP_TAC 296 >> RW_TAC std_ss [IN_BIGUNION, IN_IMAGE, IN_COUNT] 297 >> PROVE_TAC []) 298 >> DISCH_THEN (REWRITE_TAC o wrap) 299 >> POP_ASSUM MATCH_MP_TAC 300 >> reverse (RW_TAC std_ss [SUBSET_DEF, IN_BIGUNION, IN_COUNT, IN_IMAGE, 301 COUNT_ZERO, IMAGE_EMPTY, BIGUNION_EMPTY]) 302 >- (Q.EXISTS_TAC `f x'` 303 >> RW_TAC std_ss [] 304 >> Q.EXISTS_TAC `x'` 305 >> DECIDE_TAC) 306 >> MATCH_MP_TAC ALGEBRA_FINITE_UNION 307 >> POP_ASSUM MP_TAC 308 >> reverse (RW_TAC std_ss [IN_FUNSET, IN_UNIV, SUBSET_DEF, IN_IMAGE]) 309 >- PROVE_TAC [] 310 >> MATCH_MP_TAC IMAGE_FINITE 311 >> RW_TAC std_ss [FINITE_COUNT]); 312 313val SIGMA_ALGEBRA_ALT_DISJOINT = store_thm 314 ("SIGMA_ALGEBRA_ALT_DISJOINT", 315 ``!a. 316 sigma_algebra a <=> 317 algebra a /\ 318 (!f. 319 f IN (UNIV -> (subsets a)) /\ 320 (!m n : num. ~(m = n) ==> DISJOINT (f m) (f n)) ==> 321 BIGUNION (IMAGE f UNIV) IN (subsets a))``, 322 Strip 323 >> EQ_TAC >- RW_TAC std_ss [SIGMA_ALGEBRA_ALT] 324 >> RW_TAC std_ss [SIGMA_ALGEBRA_ALT_MONO, IN_FUNSET, IN_UNIV] 325 >> Q.PAT_X_ASSUM `!f. P f ==> Q f` (MP_TAC o Q.SPEC `\n. f (SUC n) DIFF f n`) 326 >> RW_TAC std_ss [] 327 >> Know 328 `BIGUNION (IMAGE f UNIV) = BIGUNION (IMAGE (\n. f (SUC n) DIFF f n) UNIV)` 329 >- (POP_ASSUM K_TAC 330 >> ONCE_REWRITE_TAC [EXTENSION] 331 >> RW_TAC std_ss [IN_BIGUNION, IN_IMAGE, IN_UNIV, IN_DIFF] 332 >> reverse EQ_TAC 333 >- (RW_TAC std_ss [] 334 >> POP_ASSUM MP_TAC 335 >> RW_TAC std_ss [IN_DIFF] 336 >> PROVE_TAC []) 337 >> RW_TAC std_ss [] 338 >> Induct_on `x'` >- RW_TAC std_ss [NOT_IN_EMPTY] 339 >> RW_TAC std_ss [] 340 >> Cases_on `x IN f x'` >- PROVE_TAC [] 341 >> Q.EXISTS_TAC `f (SUC x') DIFF f x'` 342 >> RW_TAC std_ss [EXTENSION, IN_DIFF] 343 >> PROVE_TAC []) 344 >> DISCH_THEN (REWRITE_TAC o wrap) 345 >> POP_ASSUM MATCH_MP_TAC 346 >> CONJ_TAC >- RW_TAC std_ss [ALGEBRA_DIFF] 347 >> HO_MATCH_MP_TAC TRANSFORM_2D_NUM 348 >> CONJ_TAC >- PROVE_TAC [DISJOINT_SYM] 349 >> RW_TAC arith_ss [] 350 >> Suff `f (SUC m) SUBSET f (m + n)` 351 >- (RW_TAC std_ss [DISJOINT_DEF, EXTENSION, NOT_IN_EMPTY, 352 IN_INTER, IN_DIFF, SUBSET_DEF] 353 >> PROVE_TAC []) 354 >> Cases_on `n` >- PROVE_TAC [ADD_CLAUSES] 355 >> POP_ASSUM K_TAC 356 >> Know `m + SUC n' = SUC m + n'` >- DECIDE_TAC 357 >> DISCH_THEN (REWRITE_TAC o wrap) 358 >> Induct_on `n'` >- RW_TAC arith_ss [SUBSET_REFL] 359 >> MATCH_MP_TAC SUBSET_TRANS 360 >> Q.EXISTS_TAC `f (SUC m + n')` 361 >> PROVE_TAC [ADD_CLAUSES]); 362 363(* Definition 3.1 of [1, p.16] *) 364Theorem SIGMA_ALGEBRA_ALT_SPACE : 365 !a. sigma_algebra a <=> 366 subset_class (space a) (subsets a) /\ 367 space a IN subsets a /\ 368 (!s. s IN subsets a ==> space a DIFF s IN subsets a) /\ 369 (!f :num -> 'a -> bool. 370 f IN (UNIV -> (subsets a)) ==> BIGUNION (IMAGE f UNIV) IN (subsets a)) 371Proof 372 RW_TAC std_ss [SIGMA_ALGEBRA_ALT] 373 >> EQ_TAC >> RW_TAC std_ss [] (* 4 subgoals *) 374 >- fs [algebra_def] 375 >- (MATCH_MP_TAC ALGEBRA_SPACE >> art []) 376 >- (MATCH_MP_TAC ALGEBRA_DIFF >> art [] \\ 377 MATCH_MP_TAC ALGEBRA_SPACE >> art []) 378 >> RW_TAC std_ss [algebra_def] 379 >- (���{} = space a DIFF space a��� by SET_TAC [] >> POP_ORW \\ 380 FIRST_X_ASSUM MATCH_MP_TAC >> art []) 381 >> Q.PAT_X_ASSUM ���!f. P ==> BIGUNION (IMAGE f univ(:num)) IN subsets a��� 382 (MP_TAC o (Q.SPEC ���\n. if n = 0 then s else if n = 1 then t else {}���)) 383 >> simp [IN_FUNSET, IN_UNIV] 384 >> Know ���!n :num. (if n = 0 then s else if n = 1 then t else {}) IN subsets a��� 385 >- (GEN_TAC \\ 386 Cases_on ���n = 0��� >- rw [] \\ 387 Cases_on ���n = 1��� >- rw [] \\ 388 rw [] >> ���{} = space a DIFF space a��� by SET_TAC [] >> POP_ORW \\ 389 FIRST_X_ASSUM MATCH_MP_TAC >> art []) 390 >> RW_TAC std_ss [] 391 >> Suff ���s UNION t = 392 BIGUNION (IMAGE (\n. if n = 0 then s else if n = 1 then t else {}) 393 univ(:num))��� >- rw [] 394 >> RW_TAC std_ss [Once EXTENSION, IN_UNION, IN_BIGUNION_IMAGE, IN_UNIV] 395 >> EQ_TAC >> RW_TAC std_ss [NOT_IN_EMPTY] (* 3 subgoals *) 396 >- (Q.EXISTS_TAC ���0��� >> rw []) 397 >- (Q.EXISTS_TAC ���1��� >> rw []) 398 >> Cases_on ���n = 0��� >- (DISJ1_TAC >> fs []) 399 >> Cases_on ���n = 1��� >- (DISJ2_TAC >> fs []) 400 >> fs [NOT_IN_EMPTY] 401QED 402 403val SIGMA_ALGEBRA_ALGEBRA = store_thm 404 ("SIGMA_ALGEBRA_ALGEBRA", 405 ``!a. sigma_algebra a ==> algebra a``, 406 PROVE_TAC [sigma_algebra_def]); 407 408val SIGMA_ALGEBRA_SIGMA = store_thm 409 ("SIGMA_ALGEBRA_SIGMA", 410 ``!sp sts. subset_class sp sts ==> sigma_algebra (sigma sp sts)``, 411 SIMP_TAC std_ss [subset_class_def] 412 >> NTAC 3 STRIP_TAC 413 >> RW_TAC std_ss [sigma_def, sigma_algebra_def, algebra_def, 414 subsets_def, space_def, IN_BIGINTER, 415 GSPECIFICATION, subset_class_def] 416 >- (POP_ASSUM (MATCH_MP_TAC o REWRITE_RULE [IN_POW, DIFF_SUBSET, UNION_SUBSET, EMPTY_SUBSET] o 417 Q.ISPEC `POW (sp :'a -> bool)`) 418 >> RW_TAC std_ss [SUBSET_DEF, IN_POW, IN_BIGUNION] 419 >> PROVE_TAC []) 420 >> POP_ASSUM (fn th => MATCH_MP_TAC th >> ASSUME_TAC th) 421 >> RW_TAC std_ss [SUBSET_DEF] 422 >> Q.PAT_X_ASSUM `c SUBSET PP` MP_TAC 423 >> CONV_TAC (LAND_CONV (SIMP_CONV (srw_ss()) [SUBSET_DEF])) 424 >> DISCH_THEN (MP_TAC o Q.SPEC `x`) 425 >> ASM_REWRITE_TAC [] 426 >> DISCH_THEN MATCH_MP_TAC 427 >> RW_TAC std_ss [] 428 >> PROVE_TAC [SUBSET_DEF]); 429 430(* power set of any space gives the largest possible algebra and sigma-algebra *) 431val POW_ALGEBRA = store_thm 432 ("POW_ALGEBRA", ``!sp. algebra (sp, POW sp)``, 433 RW_TAC std_ss [algebra_def, IN_POW, space_def, subsets_def, subset_class_def, 434 EMPTY_SUBSET, DIFF_SUBSET, UNION_SUBSET]); 435 436val POW_SIGMA_ALGEBRA = store_thm 437 ("POW_SIGMA_ALGEBRA", ``!sp. sigma_algebra (sp, POW sp)``, 438 RW_TAC std_ss [sigma_algebra_def, IN_POW, space_def, subsets_def, 439 POW_ALGEBRA, SUBSET_DEF, IN_BIGUNION] 440 >> PROVE_TAC []); 441 442val SIGMA_POW = store_thm 443 ("SIGMA_POW", 444 ``!s. sigma s (POW s) = (s,POW s)``, 445 RW_TAC std_ss [sigma_def, PAIR_EQ, EXTENSION, IN_BIGINTER, IN_POW, GSPECIFICATION] 446 >> EQ_TAC 447 >- (RW_TAC std_ss [] >> POP_ASSUM (MP_TAC o Q.SPEC `POW s`) 448 >> METIS_TAC [IN_POW, POW_SIGMA_ALGEBRA, SUBSET_REFL]) 449 >> RW_TAC std_ss [SUBSET_DEF, IN_POW] >> METIS_TAC []); 450 451val UNIV_SIGMA_ALGEBRA = store_thm 452 ("UNIV_SIGMA_ALGEBRA", 453 ``sigma_algebra ((UNIV :'a -> bool),(UNIV :('a -> bool) -> bool))``, 454 Know `(UNIV :('a -> bool) -> bool) = POW (UNIV :'a -> bool)` 455 >- RW_TAC std_ss [EXTENSION, IN_POW, IN_UNIV, SUBSET_UNIV] 456 >> RW_TAC std_ss [POW_SIGMA_ALGEBRA]); 457 458val SIGMA_SUBSET = store_thm 459 ("SIGMA_SUBSET", 460 ``!a b. sigma_algebra b /\ a SUBSET (subsets b) ==> subsets (sigma (space b) a) SUBSET (subsets b)``, 461 RW_TAC std_ss [sigma_def, SUBSET_DEF, IN_BIGINTER, GSPECIFICATION, subsets_def] 462 >> POP_ASSUM (MATCH_MP_TAC o Q.SPEC `subsets b`) 463 >> RW_TAC std_ss [SPACE]); 464 465val SIGMA_SUBSET_SUBSETS = store_thm 466 ("SIGMA_SUBSET_SUBSETS", ``!sp a. a SUBSET subsets (sigma sp a)``, 467 RW_TAC std_ss [sigma_def, IN_BIGINTER, SUBSET_DEF, GSPECIFICATION, subsets_def]); 468 469val IN_SIGMA = store_thm 470 ("IN_SIGMA", ``!sp a x. x IN a ==> x IN subsets (sigma sp a)``, 471 MP_TAC SIGMA_SUBSET_SUBSETS 472 >> RW_TAC std_ss [SUBSET_DEF]); 473 474(* the proof is fully syntactical, `subset_class sp a` (or b) is not needed *) 475val SIGMA_MONOTONE = store_thm 476 ("SIGMA_MONOTONE", 477 ``!sp a b. a SUBSET b ==> (subsets (sigma sp a)) SUBSET (subsets (sigma sp b))``, 478 RW_TAC std_ss [sigma_def, SUBSET_DEF, IN_BIGINTER, GSPECIFICATION, subsets_def]); 479 480(* the sigma of sigma-algebra is itself (stable) *) 481val SIGMA_STABLE_LEMMA = store_thm 482 ("SIGMA_STABLE_LEMMA", 483 ``!sp sts. sigma_algebra (sp,sts) ==> (sigma sp sts = (sp,sts))``, 484 RW_TAC std_ss [sigma_def, GSPECIFICATION, space_def, subsets_def] 485 >> ASM_SET_TAC []); 486 487(* |- !a. sigma_algebra a ==> (sigma (space a) (subsets a) = a) *) 488val SIGMA_STABLE = save_thm 489 ("SIGMA_STABLE", 490 GEN_ALL (REWRITE_RULE [SPACE] 491 (Q.SPECL [`space a`, `subsets a`] SIGMA_STABLE_LEMMA))); 492 493(* This is why ���sigma sp sts��� is "smallest": any sigma-algebra in the middle 494 coincides with it. *) 495Theorem SIGMA_SMALLEST : 496 !sp sts A. sts SUBSET A /\ A SUBSET subsets (sigma sp sts) /\ 497 sigma_algebra (sp,A) ==> (A = subsets (sigma sp sts)) 498Proof 499 RW_TAC std_ss [SET_EQ_SUBSET] 500 >> IMP_RES_TAC SIGMA_STABLE_LEMMA 501 >> ���A = subsets (sigma sp A)��� by PROVE_TAC [subsets_def] 502 >> POP_ORW 503 >> MATCH_MP_TAC SIGMA_MONOTONE >> art [] 504QED 505 506val SIGMA_ALGEBRA = store_thm 507 ("SIGMA_ALGEBRA", 508 ``!p. 509 sigma_algebra p <=> 510 subset_class (space p) (subsets p) /\ 511 {} IN subsets p /\ (!s. s IN subsets p ==> (space p DIFF s) IN subsets p) /\ 512 (!c. countable c /\ c SUBSET subsets p ==> BIGUNION c IN subsets p)``, 513 RW_TAC std_ss [sigma_algebra_def, algebra_def] 514 >> EQ_TAC >- PROVE_TAC [] 515 >> RW_TAC std_ss [] 516 >> Q.PAT_X_ASSUM `!c. P c` (MP_TAC o Q.SPEC `{s; t}`) 517 >> RW_TAC std_ss [COUNTABLE_ALT_BIJ, FINITE_INSERT, FINITE_EMPTY, SUBSET_DEF, 518 BIGUNION_PAIR, IN_INSERT, NOT_IN_EMPTY] 519 >> PROVE_TAC []); 520 521val SIGMA_ALGEBRA_COUNTABLE_UNION = store_thm 522 ("SIGMA_ALGEBRA_COUNTABLE_UNION", 523 ``!a c. sigma_algebra a /\ countable c /\ c SUBSET subsets a ==> BIGUNION c IN subsets a``, 524 PROVE_TAC [sigma_algebra_def]); 525 526val SIGMA_ALGEBRA_ENUM = store_thm 527 ("SIGMA_ALGEBRA_ENUM", 528 ``!a (f : num -> ('a -> bool)). 529 sigma_algebra a /\ f IN (UNIV -> subsets a) ==> BIGUNION (IMAGE f UNIV) IN subsets a``, 530 RW_TAC std_ss [SIGMA_ALGEBRA_ALT]); 531 532val SIGMA_PROPERTY = store_thm 533 ("SIGMA_PROPERTY", 534 ``!sp p a. 535 subset_class sp p /\ {} IN p /\ a SUBSET p /\ 536 (!s. s IN (p INTER subsets (sigma sp a)) ==> (sp DIFF s) IN p) /\ 537 (!c. countable c /\ c SUBSET (p INTER subsets (sigma sp a)) ==> 538 BIGUNION c IN p) ==> 539 subsets (sigma sp a) SUBSET p``, 540 RW_TAC std_ss [] 541 >> Suff `subsets (sigma sp a) SUBSET p INTER subsets (sigma sp a)` 542 >- SIMP_TAC std_ss [SUBSET_INTER] 543 >> Suff `p INTER subsets (sigma sp a) IN {b | a SUBSET b /\ sigma_algebra (sp,b)}` 544 >- (KILL_TAC 545 >> RW_TAC std_ss [sigma_def, GSPECIFICATION, SUBSET_DEF, INTER_DEF, BIGINTER, subsets_def]) 546 >> RW_TAC std_ss [GSPECIFICATION] 547 >- PROVE_TAC [SUBSET_DEF, IN_INTER, IN_SIGMA] 548 >> Know `subset_class sp a` >- PROVE_TAC [subset_class_def, SUBSET_DEF] 549 >> STRIP_TAC 550 >> Know `sigma_algebra (sigma sp a)` >- PROVE_TAC [subset_class_def, SUBSET_DEF, 551 SIGMA_ALGEBRA_SIGMA] 552 >> STRIP_TAC 553 >> RW_TAC std_ss [SIGMA_ALGEBRA, IN_INTER, space_def, subsets_def, SIGMA_ALGEBRA_ALGEBRA, 554 ALGEBRA_EMPTY] 555 >| [PROVE_TAC [subset_class_def, IN_INTER, SUBSET_DEF], 556 (MATCH_MP_TAC o REWRITE_RULE [space_def, subsets_def] o 557 Q.SPEC `(sp, subsets (sigma sp a))`) ALGEBRA_COMPL 558 >> FULL_SIMP_TAC std_ss [sigma_def, sigma_algebra_def, subsets_def], 559 FULL_SIMP_TAC std_ss [sigma_algebra_def] 560 >> Q.PAT_X_ASSUM `!c. P c ==> BIGUNION c IN subsets (sigma sp a)` MATCH_MP_TAC 561 >> FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_INTER]]); 562 563val SIGMA_ALGEBRA_FN = store_thm 564 ("SIGMA_ALGEBRA_FN", 565 ``!a. 566 sigma_algebra a <=> 567 subset_class (space a) (subsets a) /\ 568 {} IN subsets a /\ (!s. s IN subsets a ==> (space a DIFF s) IN subsets a) /\ 569 (!f : num -> 'a -> bool. 570 f IN (UNIV -> subsets a) ==> BIGUNION (IMAGE f UNIV) IN subsets a)``, 571 RW_TAC std_ss [SIGMA_ALGEBRA, IN_FUNSET, IN_UNIV, SUBSET_DEF] 572 >> EQ_TAC 573 >- (RW_TAC std_ss [] 574 >> Q.PAT_X_ASSUM `!c. P c ==> Q c` MATCH_MP_TAC 575 >> RW_TAC std_ss [COUNTABLE_IMAGE_NUM, IN_IMAGE] 576 >> PROVE_TAC []) 577 >> RW_TAC std_ss [COUNTABLE_ENUM] 578 >- RW_TAC std_ss [BIGUNION_EMPTY] 579 >> Q.PAT_X_ASSUM `!f. (!x. P x f) ==> Q f` MATCH_MP_TAC 580 >> POP_ASSUM MP_TAC 581 >> RW_TAC std_ss [IN_IMAGE, IN_UNIV] 582 >> PROVE_TAC []); 583 584val SIGMA_ALGEBRA_FN_BIGINTER = store_thm 585 ("SIGMA_ALGEBRA_FN_BIGINTER", 586 ``!a. 587 sigma_algebra a ==> 588 subset_class (space a) (subsets a) /\ 589 {} IN subsets a /\ 590 (!s. s IN subsets a ==> (space a DIFF s) IN subsets a) /\ 591 (!f : num -> 'a -> bool. f IN (UNIV -> subsets a) ==> BIGINTER (IMAGE f UNIV) IN subsets a)``, 592 RW_TAC std_ss [SIGMA_ALGEBRA, IN_FUNSET, IN_UNIV, SUBSET_DEF] 593 >> ASSUME_TAC (Q.SPECL [`space a`,`(IMAGE (f:num -> 'a -> bool) UNIV)`] DIFF_BIGINTER) 594 >> `!t. t IN IMAGE f UNIV ==> t SUBSET space a` 595 by ( FULL_SIMP_TAC std_ss [IN_IMAGE,sigma_algebra_def,algebra_def,subsets_def, 596 space_def,subset_class_def,IN_UNIV] 597 >> RW_TAC std_ss [] >> METIS_TAC []) 598 >> `IMAGE f UNIV <> {}` by RW_TAC std_ss [IMAGE_EQ_EMPTY,UNIV_NOT_EMPTY] 599 >> FULL_SIMP_TAC std_ss [] 600 >> `BIGUNION (IMAGE (\u. space a DIFF u) (IMAGE f UNIV)) IN subsets a` 601 by (Q.PAT_ASSUM `!c. M ==> BIGUNION c IN subsets a` (MATCH_MP_TAC) 602 >> RW_TAC std_ss [] 603 >- (MATCH_MP_TAC image_countable 604 >> RW_TAC std_ss [COUNTABLE_ENUM] 605 >> Q.EXISTS_TAC `f` 606 >> RW_TAC std_ss []) 607 >> FULL_SIMP_TAC std_ss [IN_IMAGE]) 608 >> METIS_TAC []); 609 610val SIGMA_ALGEBRA_FN_DISJOINT = store_thm 611 ("SIGMA_ALGEBRA_FN_DISJOINT", 612 ``!a. 613 sigma_algebra a <=> 614 subset_class (space a) (subsets a) /\ 615 {} IN subsets a /\ (!s. s IN subsets a ==> (space a DIFF s) IN subsets a) /\ 616 (!s t. s IN subsets a /\ t IN subsets a ==> s UNION t IN subsets a) /\ 617 (!f : num -> 'a -> bool. 618 f IN (UNIV -> subsets a) /\ (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) ==> 619 BIGUNION (IMAGE f UNIV) IN subsets a)``, 620 RW_TAC std_ss [SIGMA_ALGEBRA_ALT_DISJOINT, algebra_def] 621 >> EQ_TAC 622 >> RW_TAC std_ss []); 623 624val PREIMAGE_SIGMA_ALGEBRA = store_thm (* [1, p.16] *) 625 ("PREIMAGE_SIGMA_ALGEBRA", 626 ``!sp A f. sigma_algebra A /\ f IN (sp -> space A) ==> 627 sigma_algebra (sp,IMAGE (\s. PREIMAGE f s INTER sp) (subsets A))``, 628 rpt STRIP_TAC 629 >> RW_TAC std_ss [SIGMA_ALGEBRA_ALT, space_def, subsets_def, algebra_def, subset_class_def] 630 >| [ (* goal 1 (of 5) *) 631 fs [IN_IMAGE, IN_FUNSET], 632 (* goal 2 (of 5) *) 633 fs [IN_IMAGE, IN_FUNSET] \\ 634 Q.EXISTS_TAC `{}` >> REWRITE_TAC [PREIMAGE_EMPTY, INTER_EMPTY] \\ 635 fs [sigma_algebra_def, ALGEBRA_EMPTY], 636 (* goal 3 (of 5) *) 637 fs [IN_IMAGE, IN_FUNSET] \\ 638 Q.EXISTS_TAC `space A DIFF s'` \\ 639 reverse CONJ_TAC 640 >- (MATCH_MP_TAC ALGEBRA_COMPL >> fs [sigma_algebra_def]) \\ 641 RW_TAC std_ss [EXTENSION, IN_PREIMAGE, IN_DIFF, IN_INTER] \\ 642 EQ_TAC >> RW_TAC std_ss [], 643 (* goal 4 (of 5) *) 644 fs [IN_IMAGE, IN_FUNSET] \\ 645 Q.EXISTS_TAC `s' UNION s''` \\ 646 reverse CONJ_TAC 647 >- (MATCH_MP_TAC ALGEBRA_UNION >> fs [sigma_algebra_def]) \\ 648 RW_TAC std_ss [EXTENSION, IN_PREIMAGE, IN_UNION, IN_INTER] \\ 649 EQ_TAC >> RW_TAC std_ss [] >> art [], 650 (* goal 5 (of 5) *) 651 fs [IN_IMAGE, IN_FUNSET, IN_UNIV, SKOLEM_THM] \\ 652 `f' = \x. PREIMAGE f (f'' x) INTER sp` by PROVE_TAC [] >> POP_ORW \\ 653 `!x. f'' x IN subsets A` by PROVE_TAC [] \\ 654 Q.EXISTS_TAC `BIGUNION (IMAGE f'' UNIV)` \\ 655 reverse CONJ_TAC 656 >- (fs [SIGMA_ALGEBRA_FN] \\ 657 FIRST_X_ASSUM MATCH_MP_TAC >> art [IN_FUNSET, IN_UNIV]) \\ 658 RW_TAC std_ss [EXTENSION, IN_BIGUNION_IMAGE, IN_PREIMAGE, IN_UNIV, IN_INTER] \\ 659 EQ_TAC >> RW_TAC std_ss [] >> art [] \\ 660 Q.EXISTS_TAC `x'` >> art [] ]); 661 662val SIGMA_PROPERTY_ALT = store_thm 663 ("SIGMA_PROPERTY_ALT", 664 ``!sp p a. 665 subset_class sp p /\ 666 {} IN p /\ a SUBSET p /\ (!s. s IN (p INTER subsets (sigma sp a)) ==> sp DIFF s IN p) /\ 667 (!f : num -> 'a -> bool. 668 f IN (UNIV -> p INTER subsets (sigma sp a)) ==> BIGUNION (IMAGE f UNIV) IN p) ==> 669 subsets (sigma sp a) SUBSET p``, 670 RW_TAC std_ss [] 671 >> Suff `subsets (sigma sp a) SUBSET p INTER subsets (sigma sp a)` 672 >- SIMP_TAC std_ss [SUBSET_INTER] 673 >> Suff `p INTER subsets (sigma sp a) IN {b | a SUBSET b /\ sigma_algebra (sp, b)}` 674 >- (KILL_TAC 675 >> RW_TAC std_ss [sigma_def, GSPECIFICATION, SUBSET_DEF, INTER_DEF, BIGINTER, subsets_def]) 676 >> RW_TAC std_ss [GSPECIFICATION] 677 >- PROVE_TAC [SUBSET_DEF, IN_INTER, IN_SIGMA] 678 >> POP_ASSUM MP_TAC 679 >> Know `sigma_algebra (sigma sp a)` >- PROVE_TAC [subset_class_def, SUBSET_DEF, 680 SIGMA_ALGEBRA_SIGMA] 681 >> STRIP_TAC 682 >> RW_TAC std_ss [SIGMA_ALGEBRA_FN, IN_INTER, FUNSET_INTER, subsets_def, space_def, 683 SIGMA_ALGEBRA_ALGEBRA, ALGEBRA_EMPTY] 684 >| [PROVE_TAC [subset_class_def, IN_INTER, SUBSET_DEF], 685 (MATCH_MP_TAC o REWRITE_RULE [space_def, subsets_def] o 686 Q.SPEC `(sp, subsets (sigma sp a))`) ALGEBRA_COMPL 687 >> FULL_SIMP_TAC std_ss [sigma_def, sigma_algebra_def, subsets_def], 688 FULL_SIMP_TAC std_ss [(Q.SPEC `(sigma sp a)`) SIGMA_ALGEBRA_FN]]); 689 690(* see SIGMA_PROPERTY_DISJOINT_WEAK_ALT for another version *) 691val SIGMA_PROPERTY_DISJOINT_WEAK = store_thm 692 ("SIGMA_PROPERTY_DISJOINT_WEAK", 693 ``!sp p a. 694 subset_class sp p /\ 695 {} IN p /\ a SUBSET p /\ 696 (!s. s IN (p INTER subsets (sigma sp a)) ==> (sp DIFF s) IN p) /\ 697 (!s t. s IN p /\ t IN p ==> s UNION t IN p) /\ 698 (!f : num -> 'a -> bool. 699 f IN (UNIV -> p INTER subsets (sigma sp a)) /\ 700 (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) ==> 701 BIGUNION (IMAGE f UNIV) IN p) ==> 702 subsets (sigma sp a) SUBSET p``, 703 RW_TAC std_ss [] 704 >> Suff `subsets (sigma sp a) SUBSET p INTER subsets (sigma sp a)` 705 >- SIMP_TAC std_ss [SUBSET_INTER] 706 >> Suff `p INTER subsets (sigma sp a) IN {b | a SUBSET b /\ sigma_algebra (sp, b)}` 707 >- (KILL_TAC 708 >> RW_TAC std_ss [sigma_def, GSPECIFICATION, SUBSET_DEF, INTER_DEF, BIGINTER, subsets_def, space_def]) 709 >> RW_TAC std_ss [GSPECIFICATION] 710 >- PROVE_TAC [SUBSET_DEF, IN_INTER, IN_SIGMA] 711 >> POP_ASSUM MP_TAC 712 >> Know `sigma_algebra (sigma sp a)` >- PROVE_TAC [subset_class_def, SUBSET_DEF, 713 SIGMA_ALGEBRA_SIGMA] 714 >> STRIP_TAC 715 >> RW_TAC std_ss [SIGMA_ALGEBRA_FN_DISJOINT, IN_INTER, FUNSET_INTER, subsets_def, space_def, 716 SIGMA_ALGEBRA_ALGEBRA, ALGEBRA_EMPTY] 717 >| [PROVE_TAC [subset_class_def, IN_INTER, SUBSET_DEF], 718 (MATCH_MP_TAC o REWRITE_RULE [space_def, subsets_def] o 719 Q.SPEC `(sp, subsets (sigma sp a))`) ALGEBRA_COMPL 720 >> FULL_SIMP_TAC std_ss [sigma_def, sigma_algebra_def, subsets_def], 721 (MATCH_MP_TAC o REWRITE_RULE [space_def, subsets_def] o 722 Q.SPEC `(sp, subsets (sigma sp a))`) ALGEBRA_UNION 723 >> FULL_SIMP_TAC std_ss [sigma_def, sigma_algebra_def, subsets_def], 724 FULL_SIMP_TAC std_ss [(Q.SPEC `(sigma sp a)`) SIGMA_ALGEBRA_FN_DISJOINT]]); 725 726val SPACE_SIGMA = store_thm 727 ("SPACE_SIGMA", ``!sp a. space (sigma sp a) = sp``, 728 RW_TAC std_ss [sigma_def, space_def]); 729 730val SIGMA_REDUCE = store_thm 731 ("SIGMA_REDUCE", ``!sp a. (sp, subsets (sigma sp a)) = sigma sp a``, 732 PROVE_TAC [SPACE_SIGMA, SPACE]); 733 734(* note: SEMIRING_SPACE doesn't hold *) 735val SEMIRING_EMPTY = store_thm 736 ("SEMIRING_EMPTY", ``!r. semiring r ==> {} IN (subsets r)``, 737 RW_TAC std_ss [semiring_def]); 738 739val SEMIRING_INTER = store_thm 740 ("SEMIRING_INTER", 741 ``!r s t. semiring r /\ s IN (subsets r) /\ t IN (subsets r) ==> s INTER t IN (subsets r)``, 742 RW_TAC std_ss [semiring_def]); 743 744val SEMIRING_DIFF = store_thm 745 ("SEMIRING_DIFF", 746 ``!r s t. semiring r /\ s IN (subsets r) /\ t IN (subsets r) ==> 747 ?c. c SUBSET (subsets r) /\ FINITE c /\ disjoint c /\ (s DIFF t = BIGUNION c)``, 748 RW_TAC std_ss [semiring_def]); 749 750val SEMIRING_DIFF_ALT = store_thm 751 ("SEMIRING_DIFF_ALT", 752 ``!r s t. semiring r /\ s IN (subsets r) /\ t IN (subsets r) ==> 753 ?f n. (!i. i < n ==> f i IN subsets r) /\ 754 (!i j. i < n /\ j < n /\ i <> j ==> DISJOINT (f i) (f j)) /\ 755 (s DIFF t = BIGUNION (IMAGE f (count n)))``, 756 rpt STRIP_TAC 757 >> MP_TAC (Q.SPECL [`r`, `s`, `t`] SEMIRING_DIFF) 758 >> RW_TAC std_ss [] 759 >> STRIP_ASSUME_TAC (MATCH_MP finite_disjoint_decomposition 760 (CONJ (ASSUME ``FINITE (c :'a set set)``) 761 (ASSUME ``disjoint (c :'a set set)``))) 762 >> Q.EXISTS_TAC `f` 763 >> Q.EXISTS_TAC `n` 764 >> RW_TAC std_ss [] 765 >> PROVE_TAC [SUBSET_DEF]); 766 767val RING_EMPTY = store_thm 768 ("RING_EMPTY", ``!r. ring r ==> {} IN (subsets r)``, 769 RW_TAC std_ss [ring_def]); 770 771val RING_UNION = store_thm 772 ("RING_UNION", 773 ``!r s t. ring r /\ s IN (subsets r) /\ t IN (subsets r) ==> s UNION t IN (subsets r)``, 774 RW_TAC std_ss [ring_def]); 775 776val RING_FINITE_UNION = store_thm 777 ("RING_FINITE_UNION", 778 ``!r c. ring r /\ c SUBSET (subsets r) /\ FINITE c ==> BIGUNION c IN (subsets r)``, 779 GEN_TAC 780 >> Suff `ring r ==> 781 !c. FINITE c ==> c SUBSET (subsets r) /\ FINITE c ==> BIGUNION c IN (subsets r)` 782 >- METIS_TAC [] 783 >> DISCH_TAC 784 >> HO_MATCH_MP_TAC FINITE_INDUCT 785 >> CONJ_TAC 786 >- (RW_TAC std_ss [] >> PROVE_TAC [BIGUNION_EMPTY, RING_EMPTY]) 787 >> rpt STRIP_TAC 788 >> REWRITE_TAC [BIGUNION_INSERT] 789 >> fs [ring_def]); 790 791val RING_FINITE_UNION_ALT = store_thm 792 ("RING_FINITE_UNION_ALT", 793 ``!r f n. ring r /\ (!i. i < n ==> f i IN subsets r) ==> 794 BIGUNION (IMAGE f (count n)) IN (subsets r)``, 795 rpt STRIP_TAC 796 >> MATCH_MP_TAC RING_FINITE_UNION 797 >> ASM_SIMP_TAC std_ss [SUBSET_DEF, IN_IMAGE, IN_COUNT] 798 >> CONJ_TAC >- METIS_TAC [] 799 >> MATCH_MP_TAC IMAGE_FINITE 800 >> REWRITE_TAC [FINITE_COUNT]); 801 802(* NOTE: RING_COMPL doesn't hold because RING_SPACE doesn't hold *) 803val RING_DIFF = store_thm 804 ("RING_DIFF", 805 ``!r s t. ring r /\ s IN (subsets r) /\ t IN (subsets r) ==> s DIFF t IN (subsets r)``, 806 RW_TAC std_ss [ring_def]); 807 808val RING_INTER = store_thm 809 ("RING_INTER", 810 ``!r s t. ring r /\ s IN (subsets r) /\ t IN (subsets r) ==> s INTER t IN (subsets r)``, 811 RW_TAC std_ss [ring_def] 812 >> `s INTER t = s DIFF (s DIFF t)` by SET_TAC [] >> POP_ORW 813 >> Q.PAT_ASSUM `!s t. X ==> s DIFF t IN subsets r` MATCH_MP_TAC >> art [] 814 >> Q.PAT_ASSUM `!s t. X ==> s DIFF t IN subsets r` MATCH_MP_TAC >> art []); 815 816val RING_FINITE_INTER = store_thm 817 ("RING_FINITE_INTER", 818 ``!r f n. ring r /\ 0 < n /\ (!i. i < n ==> f i IN (subsets r)) ==> 819 BIGINTER (IMAGE f (count n)) IN (subsets r)``, 820 Q.X_GEN_TAC `r` 821 >> Suff `ring r ==> 822 !f n. 0 < n ==> (!i. i < n ==> f i IN (subsets r)) 823 ==> BIGINTER (IMAGE f (count n)) IN (subsets r)` >- METIS_TAC [] 824 >> DISCH_TAC 825 >> GEN_TAC >> Induct_on `n` >- RW_TAC arith_ss [] 826 >> RW_TAC arith_ss [] 827 >> Cases_on `n = 0` >- fs [COUNT_SUC, COUNT_ZERO, IMAGE_INSERT, IMAGE_EMPTY, 828 BIGINTER_INSERT] 829 >> `0 < n` by RW_TAC arith_ss [] 830 >> REWRITE_TAC [COUNT_SUC, IMAGE_INSERT, BIGINTER_INSERT] 831 >> `!s t. s IN (subsets r) /\ t IN (subsets r) ==> s INTER t IN (subsets r)` 832 by PROVE_TAC [RING_INTER] 833 >> POP_ASSUM MATCH_MP_TAC 834 >> STRONG_CONJ_TAC 835 >- (Q.PAT_X_ASSUM `!i. i < SUC n ==> f i IN X` (MP_TAC o (Q.SPEC `n`)) \\ 836 RW_TAC arith_ss []) 837 >> DISCH_TAC 838 >> FIRST_X_ASSUM irule >> art [] 839 >> rpt STRIP_TAC >> FIRST_X_ASSUM MATCH_MP_TAC 840 >> RW_TAC arith_ss []); 841 842(* a ring is also a semiring (but not vice versa) *) 843val RING_IMP_SEMIRING = store_thm 844 ("RING_IMP_SEMIRING", ``!r. ring r ==> semiring r``, 845 RW_TAC std_ss [semiring_def] 846 >- PROVE_TAC [ring_def] 847 >- (MATCH_MP_TAC RING_EMPTY >> art []) 848 >- (MATCH_MP_TAC RING_INTER >> art []) 849 >> Q.EXISTS_TAC `{s DIFF t}` 850 >> `s DIFF t IN subsets r` by PROVE_TAC [RING_DIFF] 851 >> SIMP_TAC std_ss [disjoint_sing, BIGUNION_SING, FINITE_SING] 852 >> ASM_SET_TAC []); 853 854(* thus: algebra ==> ring ==> semiring *) 855val ALGEBRA_IMP_RING = store_thm 856 ("ALGEBRA_IMP_RING", ``!a. algebra a ==> ring a``, 857 RW_TAC std_ss [ring_def] 858 >- PROVE_TAC [algebra_def] 859 >- (MATCH_MP_TAC ALGEBRA_EMPTY >> art []) 860 >- (MATCH_MP_TAC ALGEBRA_UNION >> art []) 861 >> MATCH_MP_TAC ALGEBRA_DIFF >> art []); 862 863(* an algebra is also a semiring (but not vice versa) *) 864val ALGEBRA_IMP_SEMIRING = store_thm 865 ("ALGEBRA_IMP_SEMIRING", ``!a. algebra a ==> semiring a``, 866 rpt STRIP_TAC 867 >> MATCH_MP_TAC RING_IMP_SEMIRING 868 >> MATCH_MP_TAC ALGEBRA_IMP_RING 869 >> ASM_REWRITE_TAC []); 870 871(* if the whole space is in the ring, the ring becomes algebra (thus also semiring) *) 872val RING_SPACE_IMP_ALGEBRA = store_thm 873 ("RING_SPACE_IMP_ALGEBRA", 874 ``!r. ring r /\ (space r) IN (subsets r) ==> algebra r``, 875 RW_TAC std_ss [algebra_def, ring_def, subset_class_def]); 876 877(* thus (smallest_ring sp sts) is really a ring, as `POW sp` is a ring. *) 878val SMALLEST_RING = store_thm 879 ("SMALLEST_RING", 880 ``!sp sts. subset_class sp sts ==> ring (smallest_ring sp sts)``, 881 SIMP_TAC std_ss [subset_class_def] 882 >> rpt STRIP_TAC 883 >> RW_TAC std_ss [smallest_ring_def, ring_def, subsets_def, space_def, IN_BIGINTER, 884 GSPECIFICATION, subset_class_def] 885 >> POP_ASSUM (MATCH_MP_TAC o REWRITE_RULE [IN_POW, DIFF_SUBSET, UNION_SUBSET, EMPTY_SUBSET] o 886 (Q.ISPEC `POW (sp :'a -> bool)`)) 887 >> RW_TAC std_ss [SUBSET_DEF, IN_POW, IN_BIGUNION, IN_DIFF, IN_INTER]); 888 889Theorem SPACE_SMALLEST_RING : 890 !sp sts. space (smallest_ring sp sts) = sp 891Proof 892 RW_TAC std_ss [smallest_ring_def, space_def] 893QED 894 895Theorem SMALLEST_RING_SUBSET_SUBSETS : 896 !sp a. a SUBSET subsets (smallest_ring sp a) 897Proof 898 RW_TAC std_ss [smallest_ring_def, subsets_def, 899 IN_BIGINTER, SUBSET_DEF, GSPECIFICATION] 900QED 901 902(* extracted from CARATHEODORY_SEMIRING for `lborel` construction *) 903Theorem SMALLEST_RING_OF_SEMIRING : 904 !sp sts. semiring (sp,sts) ==> 905 subsets (smallest_ring sp sts) = 906 {BIGUNION c | c SUBSET sts /\ FINITE c /\ disjoint c} 907Proof 908 RW_TAC std_ss [smallest_ring_def, subsets_def] 909 >> RW_TAC std_ss [Once EXTENSION, GSPECIFICATION, IN_BIGINTER] 910 >> reverse EQ_TAC >> RW_TAC std_ss [] 911 >- (MATCH_MP_TAC (REWRITE_RULE [subsets_def] 912 (Q.SPEC `(sp,P)` RING_FINITE_UNION)) >> art [] \\ 913 MATCH_MP_TAC SUBSET_TRANS \\ 914 Q.EXISTS_TAC `sts` >> art []) 915 >> POP_ASSUM (MP_TAC o 916 (Q.SPEC `{BIGUNION c | c SUBSET sts /\ FINITE c /\ disjoint c}`)) 917 >> Know `sts SUBSET {BIGUNION c | c SUBSET sts /\ FINITE c /\ disjoint c}` 918 >- (RW_TAC set_ss [SUBSET_DEF] \\ 919 Q.EXISTS_TAC `{x}` >> rw [disjoint_sing]) 920 >> Suff `ring (sp,{BIGUNION c | c SUBSET sts /\ FINITE c /\ disjoint c})` >- rw [] 921 >> Q.ABBREV_TAC `S = {BIGUNION c | c SUBSET sts /\ FINITE c /\ disjoint c}` 922 >> Know `{} IN S` 923 >- (Q.UNABBREV_TAC `S` >> RW_TAC std_ss [GSPECIFICATION] \\ 924 Q.EXISTS_TAC `EMPTY` \\ 925 REWRITE_TAC [BIGUNION_EMPTY, EMPTY_SUBSET, FINITE_EMPTY, disjoint_empty]) 926 >> DISCH_TAC 927 >> Know `sts SUBSET S` 928 >- (RW_TAC std_ss [SUBSET_DEF] \\ 929 Q.UNABBREV_TAC `S` >> SIMP_TAC std_ss [GSPECIFICATION] \\ 930 Q.EXISTS_TAC `{x}` \\ 931 REWRITE_TAC [BIGUNION_SING, FINITE_SING, disjoint_sing] \\ 932 ASM_SET_TAC []) 933 >> DISCH_TAC 934 (* S is stable under disjoint unions *) 935 >> Know `!s t. s IN S /\ t IN S /\ DISJOINT s t ==> s UNION t IN S` 936 >- (Q.UNABBREV_TAC `S` >> RW_TAC std_ss [GSPECIFICATION] \\ 937 Q.EXISTS_TAC `c UNION c'` >> REWRITE_TAC [BIGUNION_UNION] \\ 938 CONJ_TAC >- PROVE_TAC [UNION_SUBSET] \\ 939 CONJ_TAC >- PROVE_TAC [FINITE_UNION] \\ 940 MATCH_MP_TAC disjoint_union >> art [] \\ 941 METIS_TAC [DISJOINT_DEF]) 942 >> DISCH_TAC 943 (* S is stable under finite disjoint unions (not that easy!) *) 944 >> Know `!c. c SUBSET S /\ FINITE c /\ disjoint c ==> BIGUNION c IN S` 945 >- (Suff `!c. FINITE c ==> c SUBSET S /\ disjoint c ==> BIGUNION c IN S` 946 >- METIS_TAC [] \\ 947 HO_MATCH_MP_TAC FINITE_INDUCT \\ 948 CONJ_TAC >- (RW_TAC std_ss [] >> ASM_REWRITE_TAC [BIGUNION_EMPTY]) \\ 949 rpt STRIP_TAC \\ 950 (* BIGUNION (e INSERT c) IN S *) 951 REWRITE_TAC [BIGUNION_INSERT] \\ 952 FIRST_X_ASSUM MATCH_MP_TAC \\ 953 CONJ_TAC >- PROVE_TAC [INSERT_SUBSET] \\ 954 CONJ_TAC >- (FIRST_X_ASSUM MATCH_MP_TAC \\ 955 CONJ_TAC >- PROVE_TAC [INSERT_SUBSET] \\ 956 PROVE_TAC [disjoint_insert_imp]) \\ 957 (* DISJOINT e (BIGUNION c) *) 958 `?f n. (!x. x < n ==> f x IN c) /\ (c = IMAGE f (count n))` 959 by PROVE_TAC [finite_decomposition] \\ 960 ASM_REWRITE_TAC [DISJOINT_DEF] \\ 961 REWRITE_TAC [BIGUNION_IMAGE_OVER_INTER_R] \\ 962 REWRITE_TAC [BIGUNION_EQ_EMPTY] \\ 963 Cases_on `n = 0` >- (DISJ1_TAC >> PROVE_TAC [COUNT_ZERO, IMAGE_EMPTY]) \\ 964 DISJ2_TAC >> REWRITE_TAC [EXTENSION] \\ 965 GEN_TAC >> EQ_TAC >| (* 2 subgoals *) 966 [ (* goal (1 of 2) *) 967 RW_TAC std_ss [IN_IMAGE, IN_COUNT, IN_SING] \\ 968 METIS_TAC [disjoint_insert_notin, DISJOINT_DEF], 969 (* goal (2 of 2) *) 970 RW_TAC std_ss [IN_IMAGE, IN_COUNT, IN_SING] \\ 971 Q.EXISTS_TAC `0` >> RW_TAC arith_ss [] \\ 972 `f 0 IN IMAGE f (count n)` by (FIRST_X_ASSUM MATCH_MP_TAC >> RW_TAC arith_ss []) \\ 973 METIS_TAC [disjoint_insert_notin, DISJOINT_DEF] ]) 974 >> DISCH_TAC 975 (* S is stable under finite intersection (semiring is used) *) 976 >> Know `!s t. s IN S /\ t IN S ==> s INTER t IN S` 977 >- (rpt STRIP_TAC \\ 978 Know `?A. A SUBSET sts /\ FINITE A /\ disjoint A /\ (s = BIGUNION A)` 979 >- (Q.PAT_X_ASSUM `s IN S` MP_TAC \\ 980 Q.UNABBREV_TAC `S` >> RW_TAC std_ss [GSPECIFICATION] \\ 981 Q.EXISTS_TAC `c` >> art []) >> STRIP_TAC \\ 982 Know `?B. B SUBSET sts /\ FINITE B /\ disjoint B /\ (t = BIGUNION B)` 983 >- (Q.PAT_X_ASSUM `t IN S` MP_TAC \\ 984 Q.UNABBREV_TAC `S` >> RW_TAC std_ss [GSPECIFICATION] \\ 985 Q.EXISTS_TAC `c` >> art []) >> STRIP_TAC \\ 986 ASM_REWRITE_TAC [] \\ 987 Q.PAT_X_ASSUM `FINITE A` (STRIP_ASSUME_TAC o (MATCH_MP finite_decomposition)) \\ 988 Q.PAT_X_ASSUM `FINITE B` (STRIP_ASSUME_TAC o (MATCH_MP finite_decomposition)) \\ 989 ASM_REWRITE_TAC [BIGUNION_IMAGE_OVER_INTER_L] \\ 990 REWRITE_TAC [BIGUNION_IMAGE_OVER_INTER_R] \\ 991 FIRST_ASSUM MATCH_MP_TAC \\ 992 reverse CONJ_TAC (* some easy goals *) 993 >- (CONJ_TAC >- (MATCH_MP_TAC IMAGE_FINITE >> REWRITE_TAC [FINITE_COUNT]) \\ 994 MATCH_MP_TAC disjointI \\ 995 NTAC 2 GEN_TAC >> SIMP_TAC std_ss [IN_IMAGE, IN_COUNT] \\ 996 rpt STRIP_TAC \\ 997 Cases_on `i = i'` >- (`a = b` by METIS_TAC []) \\ 998 ASM_REWRITE_TAC [DISJOINT_ALT] \\ 999 GEN_TAC >> SIMP_TAC std_ss [IN_BIGUNION_IMAGE, IN_COUNT, IN_INTER] \\ 1000 rpt STRIP_TAC \\ 1001 DISJ2_TAC >> DISJ1_TAC >> CCONTR_TAC >> fs [] \\ 1002 `x IN f i INTER f i'` by METIS_TAC [IN_INTER] \\ 1003 `~DISJOINT (f i) (f i')` by ASM_SET_TAC [DISJOINT_DEF] \\ 1004 Q.PAT_X_ASSUM `disjoint (IMAGE f (count n))` MP_TAC \\ 1005 RW_TAC std_ss [disjoint_def, IN_IMAGE, IN_COUNT] \\ 1006 Q.EXISTS_TAC `f i` >> Q.EXISTS_TAC `f i'` >> art [] \\ 1007 METIS_TAC []) \\ 1008 (* IMAGE (\i. BIGUNION (IMAGE (\i'. f i INTER f' i') (count n'))) (count n) SUBSET S *) 1009 RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, IN_COUNT] \\ 1010 FIRST_ASSUM MATCH_MP_TAC \\ 1011 reverse CONJ_TAC (* some easy goals *) 1012 >- (CONJ_TAC >- (MATCH_MP_TAC IMAGE_FINITE >> REWRITE_TAC [FINITE_COUNT]) \\ 1013 MATCH_MP_TAC disjointI \\ 1014 NTAC 2 GEN_TAC >> SIMP_TAC std_ss [IN_IMAGE, IN_COUNT] \\ 1015 rpt STRIP_TAC \\ 1016 Cases_on `i' = i''` >- (`a = b` by METIS_TAC []) \\ 1017 ASM_REWRITE_TAC [DISJOINT_ALT] \\ 1018 RW_TAC std_ss [IN_INTER] \\ 1019 CCONTR_TAC >> fs [] \\ 1020 `x IN f' i' INTER f' i''` by PROVE_TAC [IN_INTER] \\ 1021 `~DISJOINT (f' i') (f' i'')` by ASM_SET_TAC [DISJOINT_DEF] \\ 1022 Q.PAT_X_ASSUM `disjoint (IMAGE f' (count n'))` MP_TAC \\ 1023 RW_TAC std_ss [disjoint_def, IN_IMAGE, IN_COUNT] \\ 1024 Q.EXISTS_TAC `f' i'` >> Q.EXISTS_TAC `f' i''` >> art [] \\ 1025 METIS_TAC []) \\ 1026 RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, IN_COUNT] \\ 1027 (* f i INTER f' i' IN S *) 1028 Know `(IMAGE f (count n)) SUBSET sts` 1029 >- (Q.PAT_X_ASSUM `BIGUNION (IMAGE f (count n)) IN S` MP_TAC \\ 1030 Q.UNABBREV_TAC `S` >> SIMP_TAC std_ss [GSPECIFICATION] >> METIS_TAC []) \\ 1031 DISCH_TAC \\ 1032 Know `(IMAGE f' (count n')) SUBSET sts` 1033 >- (Q.PAT_X_ASSUM `BIGUNION (IMAGE f' (count n')) IN S` MP_TAC \\ 1034 Q.UNABBREV_TAC `S` >> SIMP_TAC std_ss [GSPECIFICATION] >> METIS_TAC []) \\ 1035 DISCH_TAC \\ 1036 `f i IN sts /\ f' i' IN sts` by PROVE_TAC [SUBSET_DEF, IN_IMAGE, IN_COUNT] \\ 1037 fs [semiring_def, space_def, subsets_def] \\ 1038 `f i INTER f' i' IN sts` by PROVE_TAC [] \\ 1039 METIS_TAC [SUBSET_DEF]) 1040 >> DISCH_TAC 1041 (* S is stable under (more) finite intersection *) 1042 >> Know `!f n. 0 < n ==> (!i. i < n ==> f i IN S) ==> BIGINTER (IMAGE f (count n)) IN S` 1043 >- (GEN_TAC >> Induct_on `n` >- RW_TAC arith_ss [] \\ 1044 RW_TAC arith_ss [] \\ 1045 Cases_on `n = 0` >- fs [COUNT_SUC, COUNT_ZERO, IMAGE_INSERT, IMAGE_EMPTY, 1046 BIGINTER_INSERT] \\ 1047 `0 < n` by RW_TAC arith_ss [] \\ 1048 REWRITE_TAC [COUNT_SUC, IMAGE_INSERT, BIGINTER_INSERT] \\ 1049 FIRST_X_ASSUM MATCH_MP_TAC \\ 1050 STRONG_CONJ_TAC 1051 >- (Q.PAT_X_ASSUM `!i. i < SUC n ==> f i IN S` (MP_TAC o (Q.SPEC `n`)) \\ 1052 RW_TAC arith_ss []) >> DISCH_TAC \\ 1053 FIRST_X_ASSUM irule >> art [] \\ 1054 rpt STRIP_TAC >> FIRST_X_ASSUM MATCH_MP_TAC \\ 1055 RW_TAC arith_ss []) 1056 >> DISCH_TAC 1057 (* DIFF of sts is in S (semiring is used) *) 1058 >> Know `!s t. s IN sts /\ t IN sts ==> s DIFF t IN S` 1059 >- (rpt STRIP_TAC \\ 1060 fs [semiring_def, subset_class_def, space_def, subsets_def] \\ 1061 `?c. c SUBSET sts /\ FINITE c /\ disjoint c /\ (s DIFF t = BIGUNION c)` by PROVE_TAC [] \\ 1062 Q.UNABBREV_TAC `S` >> SIMP_TAC std_ss [GSPECIFICATION] \\ 1063 Q.EXISTS_TAC `c` >> art []) 1064 >> DISCH_TAC 1065 (* S is stable under diff (semiring is used) *) 1066 >> Know `!s t. s IN S /\ t IN S ==> s DIFF t IN S` 1067 >- (rpt STRIP_TAC \\ 1068 (* assert two finite disjoint sets from s and t *) 1069 Know `?A. A SUBSET sts /\ FINITE A /\ disjoint A /\ (s = BIGUNION A)` 1070 >- (Q.PAT_X_ASSUM `s IN S` MP_TAC \\ 1071 Q.UNABBREV_TAC `S` >> RW_TAC std_ss [GSPECIFICATION] \\ 1072 Q.EXISTS_TAC `c` >> art []) >> STRIP_TAC \\ 1073 Know `?B. B SUBSET sts /\ FINITE B /\ disjoint B /\ (t = BIGUNION B)` 1074 >- (Q.PAT_X_ASSUM `t IN S` MP_TAC \\ 1075 Q.UNABBREV_TAC `S` >> RW_TAC std_ss [GSPECIFICATION] \\ 1076 Q.EXISTS_TAC `c` >> art []) >> STRIP_TAC \\ 1077 ASM_REWRITE_TAC [] \\ 1078 (* decomposite the two sets into two sequences of sets *) 1079 STRIP_ASSUME_TAC (MATCH_MP finite_disjoint_decomposition 1080 (CONJ (ASSUME ``FINITE (A :'a set set)``) 1081 (ASSUME ``disjoint (A :'a set set)``))) \\ 1082 STRIP_ASSUME_TAC (MATCH_MP finite_disjoint_decomposition 1083 (CONJ (ASSUME ``FINITE (B :'a set set)``) 1084 (ASSUME ``disjoint (B :'a set set)``))) \\ 1085 ASM_REWRITE_TAC [] \\ 1086 Know `BIGUNION (IMAGE f (count n)) SUBSET sp` 1087 >- (RW_TAC std_ss [SUBSET_DEF, IN_BIGUNION_IMAGE, IN_COUNT] \\ 1088 Suff `f x' SUBSET sp` >- PROVE_TAC [SUBSET_DEF] \\ 1089 fs [semiring_def, subset_class_def, space_def, subsets_def] \\ 1090 `f x' IN sts` by PROVE_TAC [SUBSET_DEF, IN_IMAGE, IN_COUNT] \\ 1091 METIS_TAC []) >> DISCH_TAC \\ 1092 Know `BIGUNION (IMAGE f' (count n')) SUBSET sp` 1093 >- (RW_TAC std_ss [SUBSET_DEF, IN_BIGUNION_IMAGE, IN_COUNT] \\ 1094 Suff `f' x' SUBSET sp` >- PROVE_TAC [SUBSET_DEF] \\ 1095 fs [semiring_def, subset_class_def, space_def, subsets_def] \\ 1096 `f' x' IN sts` by PROVE_TAC [SUBSET_DEF, IN_IMAGE, IN_COUNT] \\ 1097 METIS_TAC []) >> DISCH_TAC \\ 1098 Cases_on `n = 0` 1099 >- (METIS_TAC [COUNT_ZERO, IMAGE_EMPTY, BIGUNION_EMPTY, EMPTY_DIFF]) \\ 1100 Cases_on `n' = 0` 1101 >- (ASM_REWRITE_TAC [COUNT_ZERO, IMAGE_EMPTY, BIGUNION_EMPTY, DIFF_EMPTY] \\ 1102 METIS_TAC []) \\ 1103 `0 < n /\ 0 < n'` by RW_TAC arith_ss [] \\ 1104 REWRITE_TAC [MATCH_MP GEN_DIFF_INTER 1105 (CONJ (ASSUME ``BIGUNION (IMAGE f (count n)) SUBSET sp``) 1106 (ASSUME ``BIGUNION (IMAGE f' (count n')) SUBSET sp``))] \\ 1107 REWRITE_TAC [MATCH_MP GEN_COMPL_FINITE_UNION (ASSUME ``0:num < n'``)] \\ 1108 REWRITE_TAC [BIGUNION_IMAGE_OVER_INTER_L] \\ 1109 REWRITE_TAC [MATCH_MP BIGINTER_IMAGE_OVER_INTER_R (ASSUME ``0:num < n'``)] \\ 1110 BETA_TAC >> FIRST_ASSUM MATCH_MP_TAC \\ 1111 reverse CONJ_TAC (* some easy goals *) 1112 >- (CONJ_TAC >- (MATCH_MP_TAC IMAGE_FINITE >> REWRITE_TAC [FINITE_COUNT]) \\ 1113 MATCH_MP_TAC disjointI \\ 1114 NTAC 2 GEN_TAC >> SIMP_TAC std_ss [IN_IMAGE, IN_COUNT] \\ 1115 rpt STRIP_TAC \\ 1116 Cases_on `i = i'` >- (`a = b` by METIS_TAC []) \\ 1117 ASM_REWRITE_TAC [DISJOINT_ALT] \\ 1118 GEN_TAC >> SIMP_TAC std_ss [IN_BIGINTER_IMAGE, IN_COUNT] \\ 1119 rpt STRIP_TAC \\ 1120 POP_ASSUM (STRIP_ASSUME_TAC o (fn th => MATCH_MP th (ASSUME ``0:num < n'``))) \\ 1121 Q.EXISTS_TAC `0` >> art [] \\ 1122 SIMP_TAC std_ss [IN_INTER] \\ 1123 DISJ1_TAC >> CCONTR_TAC \\ 1124 fs [IN_INTER] \\ 1125 `x IN f i INTER f i'` by PROVE_TAC [IN_INTER] \\ 1126 ASM_SET_TAC [DISJOINT_DEF]) \\ (* TODO: optimize this last step *) 1127 RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, IN_COUNT] \\ 1128 (* BIGINTER (IMAGE (\i'. f i INTER (sp DIFF f' i')) (count n')) IN S *) 1129 FIRST_X_ASSUM irule >> art [] \\ 1130 rpt STRIP_TAC >> BETA_TAC \\ 1131 `f i IN sts /\ f' i' IN sts` by PROVE_TAC [SUBSET_DEF, IN_IMAGE, IN_COUNT] \\ 1132 Know `f i INTER (sp DIFF f' i') = f i DIFF f' i'` 1133 >- (MATCH_MP_TAC EQ_SYM \\ 1134 MATCH_MP_TAC GEN_DIFF_INTER \\ 1135 fs [semiring_def, subset_class_def, space_def, subsets_def]) \\ 1136 Rewr >> FIRST_X_ASSUM MATCH_MP_TAC >> art []) 1137 >> DISCH_TAC 1138 (* S is stable under finite union (but is still NOT an algebra) *) 1139 >> Know `!s t. s IN S /\ t IN S ==> s UNION t IN S` 1140 >- (rpt STRIP_TAC \\ 1141 STRIP_ASSUME_TAC (Q.SPECL [`s`, `t`] UNION_TO_3_DISJOINT_UNIONS) >> art [] \\ 1142 FIRST_ASSUM MATCH_MP_TAC \\ 1143 CONJ_TAC >| (* 2 subgoals *) 1144 [ (* goal 1 (of 2) *) 1145 FIRST_X_ASSUM MATCH_MP_TAC \\ 1146 CONJ_TAC >- PROVE_TAC [] \\ 1147 CONJ_TAC >- PROVE_TAC [] \\ 1148 ASM_SET_TAC [disjoint_def, DISJOINT_DEF], 1149 (* goal 2 (of 2) *) 1150 CONJ_TAC >- PROVE_TAC [] \\ 1151 ASM_SET_TAC [disjoint_def, DISJOINT_DEF] ]) 1152 >> DISCH_TAC 1153 >> RW_TAC std_ss [ring_def, subset_class_def, space_def, subsets_def] 1154 >> POP_ASSUM MP_TAC >> Q.UNABBREV_TAC `S` 1155 >> RW_TAC std_ss [GSPECIFICATION] 1156 >> RW_TAC std_ss [BIGUNION_SUBSET] 1157 >> `Y IN sts` by METIS_TAC [SUBSET_DEF] 1158 >> METIS_TAC [semiring_def, subset_class_def, space_def, subsets_def] 1159QED 1160 1161val subset_class_POW = store_thm 1162 ("subset_class_POW", ``!sp. subset_class sp (POW sp)``, 1163 RW_TAC std_ss [subset_class_def, IN_POW]); 1164 1165val DYNKIN_SYSTEM_COMPL = store_thm 1166 ("DYNKIN_SYSTEM_COMPL", 1167 ``!d s. dynkin_system d /\ s IN subsets d ==> space d DIFF s IN subsets d``, 1168 RW_TAC std_ss [dynkin_system_def]); 1169 1170val DYNKIN_SYSTEM_SPACE = store_thm 1171 ("DYNKIN_SYSTEM_SPACE", 1172 ``!d. dynkin_system d ==> (space d) IN subsets d``, 1173 PROVE_TAC [dynkin_system_def]); 1174 1175val DYNKIN_SYSTEM_EMPTY = store_thm 1176 ("DYNKIN_SYSTEM_EMPTY", 1177 ``!d. dynkin_system d ==> {} IN subsets d``, 1178 rpt STRIP_TAC 1179 >> REWRITE_TAC [SYM (Q.SPEC `space d` DIFF_EQ_EMPTY)] 1180 >> MATCH_MP_TAC DYNKIN_SYSTEM_COMPL >> art [] 1181 >> PROVE_TAC [dynkin_system_def]); 1182 1183val DYNKIN_SYSTEM_DUNION = store_thm 1184 ("DYNKIN_SYSTEM_DUNION", 1185 ``!d s t. dynkin_system d /\ s IN subsets d /\ t IN subsets d /\ DISJOINT s t 1186 ==> s UNION t IN subsets d``, 1187 rpt STRIP_TAC 1188 >> IMP_RES_TAC DYNKIN_SYSTEM_EMPTY 1189 >> fs [dynkin_system_def] 1190 >> Q.PAT_X_ASSUM `!f. P f` 1191 (MP_TAC o Q.SPEC `\n. if n = 0 then s else if n = 1 then t else {}`) 1192 >> Know 1193 `BIGUNION 1194 (IMAGE (\n : num. (if n = 0 then s else (if n = 1 then t else {}))) 1195 UNIV) = 1196 BIGUNION 1197 (IMAGE (\n : num. (if n = 0 then s else (if n = 1 then t else {}))) 1198 (count 2))` 1199 >- (MATCH_MP_TAC BIGUNION_IMAGE_UNIV >> RW_TAC arith_ss []) 1200 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1201 >> RW_TAC bool_ss [COUNT_SUC, IMAGE_INSERT, TWO, ONE, BIGUNION_INSERT, 1202 COUNT_ZERO, IMAGE_EMPTY, BIGUNION_EMPTY, UNION_EMPTY] 1203 >> ONCE_REWRITE_TAC [UNION_COMM] 1204 >> POP_ASSUM MATCH_MP_TAC 1205 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, DISJOINT_EMPTY] 1206 >- (rpt COND_CASES_TAC >> art []) 1207 >> ASM_REWRITE_TAC [DISJOINT_SYM]); 1208 1209val DYNKIN_SYSTEM_COUNTABLY_DUNION = store_thm 1210 ("DYNKIN_SYSTEM_COUNTABLY_DUNION", 1211 ``!d f. 1212 dynkin_system d /\ f IN (UNIV -> subsets d) /\ 1213 (!i j :num. i <> j ==> DISJOINT (f i) (f j)) ==> 1214 BIGUNION (IMAGE f UNIV) IN subsets d``, 1215 RW_TAC std_ss [dynkin_system_def]); 1216 1217(* Alternative definition of Dynkin system [6], this equivalence proof is not easy *) 1218val DYNKIN_SYSTEM_ALT_MONO = store_thm 1219 ("DYNKIN_SYSTEM_ALT_MONO", 1220 ``!d. dynkin_system d <=> 1221 subset_class (space d) (subsets d) /\ 1222 (space d) IN (subsets d) /\ 1223 (!s t. s IN (subsets d) /\ t IN (subsets d) /\ s SUBSET t ==> (t DIFF s) IN (subsets d)) /\ 1224 (!f :num -> 'a set. 1225 f IN (UNIV -> subsets d) /\ (f 0 = {}) /\ (!n. f n SUBSET f (SUC n)) ==> 1226 BIGUNION (IMAGE f UNIV) IN (subsets d))``, 1227 RW_TAC std_ss [dynkin_system_def] 1228 >> EQ_TAC (* 2 subgoals *) 1229 >| [ (* goal 1 (of 2) *) 1230 RW_TAC std_ss [IN_FUNSET, IN_UNIV] >| 1231 [ (* goal 1.1 (of 2), `t DIFF s IN subsets d` *) 1232 `DISJOINT s (space d DIFF t)` by ASM_SET_TAC [] \\ 1233 Q.PAT_X_ASSUM `!f. P f` 1234 (MP_TAC o Q.SPEC `\n. if n = 0 then s else if n = 1 then (space d DIFF t) else {}`) \\ 1235 Know `BIGUNION 1236 (IMAGE (\n : num. (if n = 0 then s else (if n = 1 then (space d DIFF t) else {}))) 1237 UNIV) = 1238 BIGUNION 1239 (IMAGE (\n : num. (if n = 0 then s else (if n = 1 then (space d DIFF t) else {}))) 1240 (count 2))` 1241 >- (MATCH_MP_TAC BIGUNION_IMAGE_UNIV >> RW_TAC arith_ss []) 1242 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1243 >> RW_TAC bool_ss [COUNT_SUC, IMAGE_INSERT, TWO, ONE, BIGUNION_INSERT, 1244 COUNT_ZERO, IMAGE_EMPTY, BIGUNION_EMPTY, UNION_EMPTY] \\ 1245 Know `t DIFF s = (space d) DIFF ((space d DIFF t) UNION s)` 1246 >- (`s SUBSET space d /\ t SUBSET space d` by PROVE_TAC [subset_class_def] 1247 >> ASM_SET_TAC []) 1248 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) \\ 1249 Q.PAT_ASSUM `!s. s IN subsets d ==> P` MATCH_MP_TAC \\ 1250 POP_ASSUM MATCH_MP_TAC \\ 1251 CONJ_TAC >> rpt STRIP_TAC 1252 >- (rpt COND_CASES_TAC >> PROVE_TAC [DIFF_EQ_EMPTY]) 1253 >> rpt COND_CASES_TAC >> fs [DISJOINT_SYM], 1254 (* goal 1.2 (of 2), `BIGUNION (IMAGE f univ(:num)) IN subsets d` *) 1255 Q.PAT_ASSUM `!f. P f ==> Q f` (MP_TAC o Q.SPEC `\n. f (SUC n) DIFF f n`) \\ 1256 BETA_TAC >> STRIP_TAC \\ 1257 Know `BIGUNION (IMAGE f UNIV) = BIGUNION (IMAGE (\n. f (SUC n) DIFF f n) UNIV)` 1258 >- (POP_ASSUM K_TAC 1259 >> ONCE_REWRITE_TAC [EXTENSION] 1260 >> RW_TAC std_ss [IN_BIGUNION, IN_IMAGE, IN_UNIV, IN_DIFF] 1261 >> reverse EQ_TAC 1262 >- (RW_TAC std_ss [] 1263 >> POP_ASSUM MP_TAC 1264 >> RW_TAC std_ss [IN_DIFF] 1265 >> PROVE_TAC []) 1266 >> RW_TAC std_ss [] 1267 >> Induct_on `x'` >- RW_TAC std_ss [NOT_IN_EMPTY] 1268 >> RW_TAC std_ss [] 1269 >> Cases_on `x IN f x'` >- PROVE_TAC [] 1270 >> Q.EXISTS_TAC `f (SUC x') DIFF f x'` 1271 >> RW_TAC std_ss [EXTENSION, IN_DIFF] 1272 >> PROVE_TAC []) 1273 >> DISCH_THEN (REWRITE_TAC o wrap) \\ 1274 POP_ASSUM MATCH_MP_TAC \\ 1275 CONJ_TAC >| (* 2 subgoals *) 1276 [ (* goal 1.2.1 (of 2) *) 1277 GEN_TAC \\ 1278 Know `f (SUC x) DIFF f x = (space d) DIFF ((space d DIFF f (SUC x)) UNION f x)` 1279 >- (`f x SUBSET space d /\ f (SUC x) SUBSET space d` by PROVE_TAC [subset_class_def] 1280 >> ASM_SET_TAC []) 1281 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) \\ 1282 Q.PAT_ASSUM `!s. s IN subsets d ==> P` MATCH_MP_TAC \\ 1283 `space d DIFF f (SUC x) IN subsets d` by PROVE_TAC [] \\ 1284 `DISJOINT (space d DIFF f (SUC x)) (f x)` by ASM_SET_TAC [] \\ 1285 Q.PAT_X_ASSUM `!f. P f` 1286 (MP_TAC o 1287 Q.SPEC `\n. if n = 0 then (f x) else if n = 1 then (space d DIFF f (SUC x)) else {}`) \\ 1288 Know `BIGUNION 1289 (IMAGE (\n:num. if n = 0 then (f x) else 1290 if n = 1 then (space d DIFF f (SUC x)) else {}) 1291 UNIV) = 1292 BIGUNION 1293 (IMAGE (\n:num. if n = 0 then (f x) else 1294 if n = 1 then (space d DIFF f (SUC x)) else {}) 1295 (count 2))` 1296 >- (MATCH_MP_TAC BIGUNION_IMAGE_UNIV >> RW_TAC arith_ss []) 1297 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1298 >> RW_TAC bool_ss [COUNT_SUC, IMAGE_INSERT, TWO, ONE, BIGUNION_INSERT, 1299 COUNT_ZERO, IMAGE_EMPTY, BIGUNION_EMPTY, UNION_EMPTY] \\ 1300 POP_ASSUM MATCH_MP_TAC \\ 1301 CONJ_TAC >- PROVE_TAC [] \\ 1302 rpt GEN_TAC >> PROVE_TAC [DISJOINT_SYM, DISJOINT_EMPTY], 1303 (* goal 1.2.2 (of 2) *) 1304 HO_MATCH_MP_TAC TRANSFORM_2D_NUM \\ 1305 CONJ_TAC >- PROVE_TAC [DISJOINT_SYM] \\ 1306 RW_TAC arith_ss [] \\ 1307 Suff `f (SUC i) SUBSET f (i + j)` 1308 >- (RW_TAC std_ss [DISJOINT_DEF, EXTENSION, NOT_IN_EMPTY, 1309 IN_INTER, IN_DIFF, SUBSET_DEF] 1310 >> PROVE_TAC []) 1311 >> Cases_on `j` >- PROVE_TAC [ADD_CLAUSES] 1312 >> POP_ASSUM K_TAC 1313 >> Know `i + SUC n = SUC i + n` >- DECIDE_TAC 1314 >> DISCH_THEN (REWRITE_TAC o wrap) 1315 >> Induct_on `n` >- RW_TAC arith_ss [SUBSET_REFL] 1316 >> MATCH_MP_TAC SUBSET_TRANS 1317 >> Q.EXISTS_TAC `f (SUC i + n)` 1318 >> PROVE_TAC [ADD_CLAUSES] ] ], 1319 (* goal 2 (of 2) *) 1320 RW_TAC std_ss [IN_UNIV, IN_FUNSET] >- PROVE_TAC [subset_class_def] \\ 1321 Q.PAT_X_ASSUM `!f. P f` 1322 (MP_TAC o Q.SPEC `\n. BIGUNION (IMAGE f (count n))`) \\ 1323 BETA_TAC >> STRIP_TAC \\ 1324 Know `BIGUNION (IMAGE f UNIV) = 1325 BIGUNION (IMAGE (\n. BIGUNION (IMAGE f (count n))) UNIV)` 1326 >- ( KILL_TAC 1327 >> ONCE_REWRITE_TAC [EXTENSION] 1328 >> RW_TAC std_ss [IN_BIGUNION, IN_IMAGE, IN_UNIV] 1329 >> EQ_TAC 1330 >- (RW_TAC std_ss [] 1331 >> Q.EXISTS_TAC `BIGUNION (IMAGE f (count (SUC x')))` 1332 >> RW_TAC std_ss [IN_BIGUNION, IN_IMAGE, IN_COUNT] 1333 >> PROVE_TAC [prim_recTheory.LESS_SUC_REFL]) 1334 >> RW_TAC std_ss [] 1335 >> POP_ASSUM MP_TAC 1336 >> RW_TAC std_ss [IN_BIGUNION, IN_IMAGE, IN_COUNT] 1337 >> PROVE_TAC [] ) 1338 >> DISCH_THEN (REWRITE_TAC o wrap) \\ 1339 POP_ASSUM MATCH_MP_TAC \\ 1340 SIMP_TAC std_ss [SUBSET_DEF, IN_BIGUNION, IN_COUNT, IN_IMAGE, 1341 COUNT_ZERO, IMAGE_EMPTY, BIGUNION_EMPTY] \\ 1342 reverse CONJ_TAC 1343 >- (RW_TAC std_ss [] \\ 1344 Q.EXISTS_TAC `f x'` >> RW_TAC std_ss [] \\ 1345 Q.EXISTS_TAC `x'` >> DECIDE_TAC) \\ 1346 (* !x. BIGUNION (IMAGE f (count x)) IN subsets d *) 1347 Induct_on `x` 1348 >- (RW_TAC std_ss [SUBSET_DEF, IN_BIGUNION, IN_COUNT, IN_IMAGE, 1349 COUNT_ZERO, IMAGE_EMPTY, BIGUNION_EMPTY] \\ 1350 REWRITE_TAC [Q.SPEC `space d` (GSYM DIFF_EQ_EMPTY)] \\ 1351 Q.PAT_X_ASSUM `!s t. X ==> t DIFF s IN subsets d` MATCH_MP_TAC \\ 1352 ASM_REWRITE_TAC [SUBSET_REFL]) \\ 1353 (* BIGUNION (IMAGE f (count (SUC x))) IN subsets d *) 1354 REWRITE_TAC [COUNT_SUC, IMAGE_INSERT, BIGUNION_INSERT] \\ 1355 `f x SUBSET space d` by PROVE_TAC [subset_class_def] \\ 1356 Know `BIGUNION (IMAGE f (count x)) SUBSET space d` 1357 >- (REWRITE_TAC [BIGUNION_SUBSET] >> GEN_TAC \\ 1358 RW_TAC std_ss [IN_IMAGE] >> PROVE_TAC [subset_class_def]) \\ 1359 DISCH_TAC \\ 1360 `f x UNION (BIGUNION (IMAGE f (count x))) SUBSET space d` by PROVE_TAC [UNION_SUBSET] \\ 1361 POP_ASSUM (MP_TAC o SYM o (MATCH_MP DIFF_DIFF_SUBSET)) \\ 1362 ONCE_REWRITE_TAC [DIFF_UNION] \\ 1363 DISCH_THEN (ONCE_REWRITE_TAC o wrap) \\ 1364 Q.PAT_ASSUM `!s t. X ==> t DIFF s IN subsets d` MATCH_MP_TAC \\ 1365 ASM_REWRITE_TAC [DIFF_SUBSET] \\ 1366 reverse CONJ_TAC >- ASM_SET_TAC [] \\ 1367 Q.PAT_ASSUM `!s t. X ==> t DIFF s IN subsets d` MATCH_MP_TAC >> art [] \\ 1368 CONJ_TAC (* 2 subgoals *) 1369 >- (Q.PAT_ASSUM `!s t. X ==> t DIFF s IN subsets d` MATCH_MP_TAC >> art []) \\ 1370 REWRITE_TAC [SUBSET_DIFF] >> art [] \\ 1371 REWRITE_TAC [DISJOINT_BIGUNION] >> RW_TAC std_ss [IN_IMAGE] \\ 1372 fs [IN_COUNT] ]); 1373 1374val DYNKIN_SYSTEM_INCREASING = store_thm 1375 ("DYNKIN_SYSTEM_INCREASING", 1376 ``!p f. 1377 dynkin_system p /\ f IN (UNIV -> subsets p) /\ (f 0 = {}) /\ 1378 (!n. f n SUBSET f (SUC n)) ==> 1379 BIGUNION (IMAGE f UNIV) IN subsets p``, 1380 RW_TAC std_ss [DYNKIN_SYSTEM_ALT_MONO]); 1381 1382(* The original definition of `closed_cdi`, plus `(space d) IN (subsets d)` *) 1383val DYNKIN_SYSTEM_ALT = store_thm 1384 ("DYNKIN_SYSTEM_ALT", 1385 ``!d. dynkin_system d <=> 1386 subset_class (space d) (subsets d) /\ 1387 (space d) IN (subsets d) /\ 1388 (!s. s IN (subsets d) ==> (space d DIFF s) IN (subsets d)) /\ 1389 (!f :num -> 'a set. 1390 f IN (UNIV -> subsets d) /\ (f 0 = {}) /\ (!n. f n SUBSET f (SUC n)) ==> 1391 BIGUNION (IMAGE f UNIV) IN (subsets d)) /\ 1392 (!f :num -> 'a set. 1393 f IN (UNIV -> (subsets d)) /\ (!i j. i <> j ==> DISJOINT (f i) (f j)) ==> 1394 BIGUNION (IMAGE f UNIV) IN (subsets d))``, 1395 GEN_TAC >> EQ_TAC 1396 >> REWRITE_TAC [dynkin_system_def] >> RW_TAC std_ss [IN_UNIV, IN_FUNSET] 1397 >> Q.PAT_ASSUM `!f. P f ==> Q f` (MP_TAC o Q.SPEC `\n. f (SUC n) DIFF f n`) 1398 >> BETA_TAC >> STRIP_TAC 1399 >> Know `BIGUNION (IMAGE f UNIV) = BIGUNION (IMAGE (\n. f (SUC n) DIFF f n) UNIV)` 1400 >- (POP_ASSUM K_TAC 1401 >> ONCE_REWRITE_TAC [EXTENSION] 1402 >> RW_TAC std_ss [IN_BIGUNION, IN_IMAGE, IN_UNIV, IN_DIFF] 1403 >> reverse EQ_TAC 1404 >- (RW_TAC std_ss [] 1405 >> POP_ASSUM MP_TAC 1406 >> RW_TAC std_ss [IN_DIFF] 1407 >> PROVE_TAC []) 1408 >> RW_TAC std_ss [] 1409 >> Induct_on `x'` >- RW_TAC std_ss [NOT_IN_EMPTY] 1410 >> RW_TAC std_ss [] 1411 >> Cases_on `x IN f x'` >- PROVE_TAC [] 1412 >> Q.EXISTS_TAC `f (SUC x') DIFF f x'` 1413 >> RW_TAC std_ss [EXTENSION, IN_DIFF] 1414 >> PROVE_TAC []) 1415 >> DISCH_THEN (REWRITE_TAC o wrap) 1416 >> POP_ASSUM MATCH_MP_TAC 1417 >> CONJ_TAC (* 2 subgoals *) 1418 >| [ (* goal 1 (of 2) *) 1419 GEN_TAC \\ 1420 Know `f (SUC x) DIFF f x = (space d) DIFF ((space d DIFF f (SUC x)) UNION f x)` 1421 >- (`f x SUBSET space d /\ f (SUC x) SUBSET space d` by PROVE_TAC [subset_class_def] 1422 >> ASM_SET_TAC []) \\ 1423 DISCH_THEN (ONCE_REWRITE_TAC o wrap) \\ 1424 Q.PAT_ASSUM `!s. s IN subsets d ==> P` MATCH_MP_TAC \\ 1425 `space d DIFF f (SUC x) IN subsets d` by PROVE_TAC [] \\ 1426 `DISJOINT (space d DIFF f (SUC x)) (f x)` by ASM_SET_TAC [] \\ 1427 Q.PAT_X_ASSUM `!f. P f` 1428 (MP_TAC o 1429 Q.SPEC `\n. if n = 0 then (f x) else if n = 1 then (space d DIFF f (SUC x)) else {}`) \\ 1430 Know `BIGUNION (IMAGE (\n:num. if n = 0 then (f x) else 1431 if n = 1 then (space d DIFF f (SUC x)) else {}) 1432 UNIV) = 1433 BIGUNION (IMAGE (\n:num. if n = 0 then (f x) else 1434 if n = 1 then (space d DIFF f (SUC x)) else {}) 1435 (count 2))` 1436 >- (MATCH_MP_TAC BIGUNION_IMAGE_UNIV >> RW_TAC arith_ss []) \\ 1437 DISCH_THEN (ONCE_REWRITE_TAC o wrap) \\ 1438 RW_TAC bool_ss [COUNT_SUC, IMAGE_INSERT, TWO, ONE, BIGUNION_INSERT, 1439 COUNT_ZERO, IMAGE_EMPTY, BIGUNION_EMPTY, UNION_EMPTY] \\ 1440 POP_ASSUM MATCH_MP_TAC \\ 1441 CONJ_TAC >- PROVE_TAC [] \\ 1442 rpt GEN_TAC >> PROVE_TAC [DISJOINT_SYM, DISJOINT_EMPTY], 1443 (* goal 2 (of 2) *) 1444 HO_MATCH_MP_TAC TRANSFORM_2D_NUM \\ 1445 CONJ_TAC >- PROVE_TAC [DISJOINT_SYM] \\ 1446 RW_TAC arith_ss [] \\ 1447 Suff `f (SUC i) SUBSET f (i + j)` 1448 >- (RW_TAC std_ss [DISJOINT_DEF, EXTENSION, NOT_IN_EMPTY, 1449 IN_INTER, IN_DIFF, SUBSET_DEF] 1450 >> PROVE_TAC []) \\ 1451 Cases_on `j` >- PROVE_TAC [ADD_CLAUSES] \\ 1452 POP_ASSUM K_TAC \\ 1453 Know `i + SUC n = SUC i + n` >- DECIDE_TAC \\ 1454 DISCH_THEN (REWRITE_TAC o wrap) \\ 1455 Induct_on `n` >- RW_TAC arith_ss [SUBSET_REFL] \\ 1456 MATCH_MP_TAC SUBSET_TRANS \\ 1457 Q.EXISTS_TAC `f (SUC i + n)` \\ 1458 PROVE_TAC [ADD_CLAUSES] ]); 1459 1460val SPACE_DYNKIN = store_thm 1461 ("SPACE_DYNKIN", ``!sp sts. space (dynkin sp sts) = sp``, 1462 RW_TAC std_ss [dynkin_def, space_def]); 1463 1464val DYNKIN_SUBSET = store_thm 1465 ("DYNKIN_SUBSET", 1466 ``!a b. dynkin_system b /\ a SUBSET (subsets b) ==> 1467 subsets (dynkin (space b) a) SUBSET (subsets b)``, 1468 RW_TAC std_ss [dynkin_def, SUBSET_DEF, IN_BIGINTER, GSPECIFICATION, subsets_def] 1469 >> POP_ASSUM (MATCH_MP_TAC o Q.SPEC `subsets b`) 1470 >> RW_TAC std_ss [SPACE]); 1471 1472val DYNKIN_SUBSET_SUBSETS = store_thm 1473 ("DYNKIN_SUBSET_SUBSETS", 1474 ``!sp a. a SUBSET subsets (dynkin sp a)``, 1475 RW_TAC std_ss [dynkin_def, IN_BIGINTER, SUBSET_DEF, GSPECIFICATION, subsets_def]); 1476 1477val IN_DYNKIN = store_thm 1478 ("IN_DYNKIN", 1479 ``!sp a x. x IN a ==> x IN subsets (dynkin sp a)``, 1480 MP_TAC DYNKIN_SUBSET_SUBSETS 1481 >> RW_TAC std_ss [SUBSET_DEF]); 1482 1483val DYNKIN_MONOTONE = store_thm 1484 ("DYNKIN_MONOTONE", 1485 ``!sp a b. a SUBSET b ==> (subsets (dynkin sp a)) SUBSET (subsets (dynkin sp b))``, 1486 RW_TAC std_ss [dynkin_def, SUBSET_DEF, IN_BIGINTER, GSPECIFICATION, subsets_def]); 1487 1488Theorem DYNKIN_STABLE_LEMMA : 1489 !sp sts. dynkin_system (sp,sts) ==> (dynkin sp sts = (sp,sts)) 1490Proof 1491 RW_TAC std_ss [dynkin_def, GSPECIFICATION, space_def, subsets_def] 1492 >> ASM_SET_TAC [] 1493QED 1494 1495(* |- !d. dynkin_system d ==> (dynkin (space d) (subsets d) = d) *) 1496Theorem DYNKIN_STABLE = 1497 GEN_ALL (REWRITE_RULE [SPACE] 1498 (Q.SPECL [`space d`, `subsets d`] DYNKIN_STABLE_LEMMA)); 1499 1500Theorem DYNKIN_SMALLEST : 1501 !sp sts D. sts SUBSET D /\ D SUBSET subsets (dynkin sp sts) /\ 1502 dynkin_system (sp,D) ==> (D = subsets (dynkin sp sts)) 1503Proof 1504 RW_TAC std_ss [SET_EQ_SUBSET] 1505 >> IMP_RES_TAC DYNKIN_STABLE_LEMMA 1506 >> ���D = subsets (dynkin sp D)��� by PROVE_TAC [subsets_def] 1507 >> POP_ORW 1508 >> MATCH_MP_TAC DYNKIN_MONOTONE >> art [] 1509QED 1510 1511val DYNKIN = store_thm 1512 ("DYNKIN", 1513 ``!sp sts. subset_class sp sts ==> 1514 sts SUBSET subsets (dynkin sp sts) /\ 1515 dynkin_system (dynkin sp sts) /\ 1516 subset_class sp (subsets (dynkin sp sts))``, 1517 rpt GEN_TAC 1518 >> Know `!sp sts. subset_class sp sts ==> sts SUBSET subsets (dynkin sp sts) /\ 1519 dynkin_system (dynkin sp sts)` 1520 >- ( RW_TAC std_ss [dynkin_def, GSPECIFICATION, SUBSET_DEF, INTER_DEF, BIGINTER, 1521 subset_class_def, subsets_def, space_def] \\ 1522 RW_TAC std_ss [dynkin_system_def, GSPECIFICATION, IN_BIGINTER, IN_FUNSET, 1523 IN_UNIV, subsets_def, space_def, subset_class_def] \\ 1524 POP_ASSUM (MP_TAC o Q.SPEC `{x | x SUBSET sp}`) \\ 1525 RW_TAC std_ss [GSPECIFICATION] \\ 1526 POP_ASSUM MATCH_MP_TAC \\ 1527 RW_TAC std_ss [SUBSET_DEF] \\ 1528 PROVE_TAC [IN_DIFF, IN_BIGUNION, IN_IMAGE, IN_UNIV] ) 1529 >> SIMP_TAC std_ss [] 1530 >> RW_TAC std_ss [dynkin_system_def, SPACE_DYNKIN]); 1531 1532val SIGMA_PROPERTY_DISJOINT_LEMMA1 = store_thm 1533 ("SIGMA_PROPERTY_DISJOINT_LEMMA1", 1534 ``!sp sts. 1535 algebra (sp,sts) ==> 1536 (!s t. 1537 s IN sts /\ t IN subsets (dynkin sp sts) ==> 1538 s INTER t IN subsets (dynkin sp sts))``, 1539 RW_TAC std_ss [IN_BIGINTER, GSPECIFICATION, dynkin_def, subsets_def] 1540 >> Suff 1541 `t IN 1542 {b | b IN subsets (dynkin sp sts) /\ s INTER b IN subsets (dynkin sp sts)}` 1543 >- RW_TAC std_ss [GSPECIFICATION, IN_BIGINTER, dynkin_def, subsets_def] 1544 >> first_x_assum MATCH_MP_TAC 1545 >> STRONG_CONJ_TAC 1546 >- (RW_TAC std_ss [SUBSET_DEF, GSPECIFICATION, IN_BIGINTER, 1547 dynkin_def, subsets_def] \\ 1548 first_x_assum MATCH_MP_TAC \\ 1549 PROVE_TAC [subsets_def, ALGEBRA_INTER]) 1550 >> `subset_class sp sts` by PROVE_TAC [algebra_def, space_def, subsets_def] 1551 >> RW_TAC std_ss [GSPECIFICATION, SUBSET_DEF, dynkin_system_def, space_def, subsets_def] 1552 >| (* 7 subgoals *) 1553 [ (* goal 1 (of 7) *) 1554 MP_TAC (UNDISCH (Q.SPECL [`sp`, `sts`] DYNKIN)) 1555 >> RW_TAC std_ss [subset_class_def, SUBSET_DEF, GSPECIFICATION] 1556 >> PROVE_TAC [algebra_def, subset_class_def, SUBSET_DEF], 1557 (* goal 2 (of 7) *) 1558 PROVE_TAC [dynkin_system_def, DYNKIN, SPACE_DYNKIN], 1559 (* goal 3 (of 7) *) 1560 `sp IN sts` by PROVE_TAC [ALGEBRA_SPACE, space_def, subsets_def] >> RES_TAC, 1561 (* goal 4 (of 7) *) 1562 Know `(sp DIFF s') = space (dynkin sp sts) DIFF s'` 1563 >- (RW_TAC std_ss [EXTENSION, INTER_DEF, COMPL_DEF, UNION_DEF, GSPECIFICATION, IN_UNIV, 1564 IN_DIFF] 1565 >> PROVE_TAC [SPACE_DYNKIN]) 1566 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1567 >> MATCH_MP_TAC DYNKIN_SYSTEM_COMPL 1568 >> RW_TAC std_ss [DYNKIN], 1569 (* goal 5 (of 7) *) 1570 Know `s INTER (sp DIFF s') = 1571 space (dynkin sp sts) DIFF 1572 (space (dynkin sp sts) DIFF s UNION (s INTER s'))` 1573 >- (RW_TAC std_ss [EXTENSION, INTER_DEF, COMPL_DEF, UNION_DEF, GSPECIFICATION, IN_UNIV, 1574 IN_DIFF] 1575 >> PROVE_TAC [SPACE_DYNKIN]) 1576 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1577 >> MATCH_MP_TAC DYNKIN_SYSTEM_COMPL 1578 >> FULL_SIMP_TAC bool_ss [algebra_def, space_def, subsets_def] 1579 >> RW_TAC std_ss [DYNKIN] 1580 >> MATCH_MP_TAC DYNKIN_SYSTEM_DUNION 1581 >> CONJ_TAC 1582 >- PROVE_TAC [ALGEBRA_EMPTY, DYNKIN, SUBSET_DEF] 1583 >> CONJ_TAC 1584 >- (MATCH_MP_TAC DYNKIN_SYSTEM_COMPL 1585 >> RW_TAC std_ss [DYNKIN]) 1586 >> ASM_REWRITE_TAC [] 1587 >> RW_TAC std_ss [DISJOINT_DEF, COMPL_DEF, INTER_DEF, IN_DIFF, IN_UNIV, GSPECIFICATION, 1588 EXTENSION, NOT_IN_EMPTY] 1589 >> DECIDE_TAC, 1590 (* goal 6 (of 7) *) 1591 Q.PAT_X_ASSUM `f IN x` MP_TAC 1592 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, GSPECIFICATION] 1593 >> MATCH_MP_TAC DYNKIN_SYSTEM_COUNTABLY_DUNION 1594 >> RW_TAC std_ss [DYNKIN, IN_FUNSET, SUBSET_DEF], 1595 (* goal 7 (of 7) *) 1596 Know `s INTER BIGUNION (IMAGE f UNIV) = BIGUNION (IMAGE (\n. s INTER f n) UNIV)` 1597 >- (KILL_TAC 1598 >> RW_TAC std_ss [Once EXTENSION, IN_BIGUNION, GSPECIFICATION, IN_IMAGE, IN_UNIV, 1599 IN_INTER] 1600 >> (EQ_TAC >> RW_TAC std_ss []) >| 1601 [Q.EXISTS_TAC `s INTER f x'` 1602 >> RW_TAC std_ss [IN_INTER] 1603 >> Q.EXISTS_TAC `x'` 1604 >> RW_TAC arith_ss [IN_INTER], 1605 POP_ASSUM (MP_TAC) 1606 >> RW_TAC arith_ss [IN_INTER], 1607 POP_ASSUM (MP_TAC) 1608 >> RW_TAC arith_ss [IN_INTER] 1609 >> Q.EXISTS_TAC `f n` 1610 >> RW_TAC std_ss [] 1611 >> PROVE_TAC []]) 1612 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1613 >> MATCH_MP_TAC DYNKIN_SYSTEM_COUNTABLY_DUNION 1614 >> Q.PAT_X_ASSUM `f IN X` MP_TAC 1615 >> RW_TAC std_ss [DYNKIN, IN_FUNSET, IN_UNIV, GSPECIFICATION] 1616 >> Q.PAT_X_ASSUM `!i j. X i j` (MP_TAC o Q.SPECL [`i`, `j`]) 1617 >> RW_TAC std_ss [DISJOINT_DEF, EXTENSION, IN_INTER, NOT_IN_EMPTY] 1618 >> PROVE_TAC [] ]); 1619 1620(* The smallest dynkin system generated from an algebra is stable under finite intersection *) 1621val SIGMA_PROPERTY_DISJOINT_LEMMA2 = store_thm 1622 ("SIGMA_PROPERTY_DISJOINT_LEMMA2", 1623 ``!sp sts. 1624 algebra (sp,sts) ==> 1625 (!s t. 1626 s IN subsets (dynkin sp sts) /\ t IN subsets (dynkin sp sts) ==> 1627 s INTER t IN subsets (dynkin sp sts))``, 1628 RW_TAC std_ss [] 1629 >> POP_ASSUM MP_TAC 1630 >> SIMP_TAC std_ss [dynkin_def, IN_BIGINTER, GSPECIFICATION, subsets_def] 1631 >> STRIP_TAC >> Q.X_GEN_TAC `P` 1632 >> Suff 1633 `t IN 1634 {b | b IN subsets (dynkin sp sts) /\ s INTER b IN subsets (dynkin sp sts)}` 1635 >- RW_TAC std_ss [GSPECIFICATION, IN_BIGINTER, dynkin_def, subsets_def] 1636 >> `subset_class sp sts` by PROVE_TAC [algebra_def, space_def, subsets_def] 1637 >> Q.PAT_X_ASSUM `!s. P s` MATCH_MP_TAC 1638 >> STRONG_CONJ_TAC 1639 >- (RW_TAC std_ss [SUBSET_DEF, GSPECIFICATION] >| 1640 [PROVE_TAC [DYNKIN, SUBSET_DEF], 1641 PROVE_TAC [SIGMA_PROPERTY_DISJOINT_LEMMA1, INTER_COMM]]) 1642 >> SIMP_TAC std_ss [GSPECIFICATION, SUBSET_DEF, dynkin_system_def, space_def, subsets_def] 1643 >> STRIP_TAC >> rpt CONJ_TAC 1644 >| (* 5 subgoals *) 1645 [ (* goal 1 (of 5) *) 1646 (MP_TAC o UNDISCH o Q.SPECL [`sp`, `sts`]) DYNKIN 1647 >> RW_TAC std_ss [subset_class_def, SUBSET_DEF, GSPECIFICATION] 1648 >> PROVE_TAC [algebra_def, subset_class_def, SUBSET_DEF], 1649 (* goal 2 (of 5) *) 1650 PROVE_TAC [dynkin_system_def, DYNKIN, SPACE_DYNKIN], 1651 (* goal 3 (of 5) *) 1652 `sp IN sts` by PROVE_TAC [ALGEBRA_SPACE, space_def, subsets_def] >> RES_TAC, 1653 (* goal 4 (of 5) *) 1654 Q.X_GEN_TAC `s'` 1655 >> rpt STRIP_TAC 1656 >- PROVE_TAC [dynkin_system_def, DYNKIN, SPACE_DYNKIN] 1657 >> Know `s INTER (sp DIFF s') = 1658 space (dynkin sp sts) DIFF 1659 (space (dynkin sp sts) DIFF s UNION (s INTER s'))` 1660 >- (RW_TAC std_ss [EXTENSION, INTER_DEF, COMPL_DEF, UNION_DEF, GSPECIFICATION, IN_UNIV, 1661 IN_DIFF, SPACE_DYNKIN] 1662 >> DECIDE_TAC) 1663 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1664 >> MATCH_MP_TAC DYNKIN_SYSTEM_COMPL 1665 >> RW_TAC std_ss [DYNKIN] 1666 >> MATCH_MP_TAC DYNKIN_SYSTEM_DUNION 1667 >> CONJ_TAC 1668 >- PROVE_TAC [ALGEBRA_EMPTY, DYNKIN, SUBSET_DEF] 1669 >> CONJ_TAC 1670 >- (MATCH_MP_TAC DYNKIN_SYSTEM_COMPL 1671 >> RW_TAC std_ss [DYNKIN]) 1672 >> ASM_REWRITE_TAC [] 1673 >> RW_TAC std_ss [DISJOINT_DEF, COMPL_DEF, INTER_DEF, IN_DIFF, IN_UNIV, GSPECIFICATION, 1674 EXTENSION, NOT_IN_EMPTY] 1675 >> DECIDE_TAC, 1676 (* goal 5 (of 5) *) 1677 Q.X_GEN_TAC `f` >> rpt STRIP_TAC 1678 >- (Q.PAT_X_ASSUM `f IN x` MP_TAC 1679 >> RW_TAC std_ss [IN_FUNSET, IN_UNIV, GSPECIFICATION] 1680 >> MATCH_MP_TAC DYNKIN_SYSTEM_COUNTABLY_DUNION 1681 >> RW_TAC std_ss [DYNKIN, IN_FUNSET, SUBSET_DEF]) 1682 >> Know 1683 `s INTER BIGUNION (IMAGE f UNIV) = 1684 BIGUNION (IMAGE (\n. s INTER f n) UNIV)` 1685 >- (KILL_TAC 1686 >> RW_TAC std_ss [Once EXTENSION, IN_BIGUNION, GSPECIFICATION, IN_IMAGE, IN_UNIV, 1687 IN_INTER] 1688 >> (EQ_TAC >> RW_TAC std_ss []) >| 1689 [Q.EXISTS_TAC `s INTER f x'` 1690 >> RW_TAC std_ss [IN_INTER] 1691 >> Q.EXISTS_TAC `x'` 1692 >> RW_TAC arith_ss [IN_INTER], 1693 POP_ASSUM (MP_TAC) 1694 >> RW_TAC arith_ss [IN_INTER], 1695 POP_ASSUM (MP_TAC) 1696 >> RW_TAC arith_ss [IN_INTER] 1697 >> Q.EXISTS_TAC `f n` 1698 >> RW_TAC std_ss [] 1699 >> PROVE_TAC []]) 1700 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1701 >> MATCH_MP_TAC DYNKIN_SYSTEM_COUNTABLY_DUNION 1702 >> Q.PAT_X_ASSUM `f IN X` MP_TAC 1703 >> RW_TAC std_ss [DYNKIN, IN_FUNSET, IN_UNIV, GSPECIFICATION] 1704 >> Q.PAT_X_ASSUM `!i j. X i j` (MP_TAC o Q.SPECL [`i`, `j`]) 1705 >> RW_TAC std_ss [DISJOINT_DEF, EXTENSION, IN_INTER, NOT_IN_EMPTY] 1706 >> PROVE_TAC [] ]); 1707 1708(* If an algebra is contained in a dynkin system, then the smallest sigma-algebra generated 1709 from it is also contained in the dynkin system. *) 1710val SIGMA_PROPERTY_DISJOINT_LEMMA = store_thm 1711 ("SIGMA_PROPERTY_DISJOINT_LEMMA", 1712 ``!sp a d. algebra (sp,a) /\ a SUBSET d /\ dynkin_system (sp,d) 1713 ==> subsets (sigma sp a) SUBSET d``, 1714 RW_TAC std_ss [] 1715 >> MATCH_MP_TAC SUBSET_TRANS 1716 >> Q.EXISTS_TAC `subsets (dynkin sp a)` 1717 >> reverse CONJ_TAC 1718 >- (RW_TAC std_ss [SUBSET_DEF, dynkin_def, IN_BIGINTER, 1719 GSPECIFICATION, subsets_def, space_def] 1720 >> PROVE_TAC [SUBSET_DEF]) 1721 >> NTAC 2 (POP_ASSUM K_TAC) 1722 >> Suff `subsets (dynkin sp a) IN {b | a SUBSET b /\ sigma_algebra (sp,b)}` 1723 >- (KILL_TAC 1724 >> RW_TAC std_ss [sigma_def, BIGINTER, SUBSET_DEF, GSPECIFICATION, subsets_def]) 1725 >> `subset_class sp a` by PROVE_TAC [algebra_def, space_def, subsets_def] 1726 >> RW_TAC std_ss [GSPECIFICATION, SIGMA_ALGEBRA_ALT_DISJOINT, 1727 ALGEBRA_ALT_INTER, space_def, subsets_def] >| 1728 [PROVE_TAC [DYNKIN, subsets_def], 1729 PROVE_TAC [DYNKIN, space_def], 1730 PROVE_TAC [ALGEBRA_EMPTY, SUBSET_DEF, DYNKIN, space_def, subsets_def], 1731 PROVE_TAC [DYNKIN, DYNKIN_SYSTEM_COMPL, space_def, SPACE_DYNKIN], 1732 PROVE_TAC [SIGMA_PROPERTY_DISJOINT_LEMMA2], 1733 PROVE_TAC [DYNKIN, DYNKIN_SYSTEM_COUNTABLY_DUNION]]); 1734 1735val SIGMA_PROPERTY_DISJOINT_WEAK_ALT = store_thm (* renamed *) 1736 ("SIGMA_PROPERTY_DISJOINT_WEAK_ALT", 1737 ``!sp p a. 1738 algebra (sp, a) /\ a SUBSET p /\ 1739 subset_class sp p /\ 1740 (!s. s IN p ==> sp DIFF s IN p) /\ 1741 (!f : num -> 'a -> bool. 1742 f IN (UNIV -> p) /\ (f 0 = {}) /\ (!n. f n SUBSET f (SUC n)) ==> 1743 BIGUNION (IMAGE f UNIV) IN p) /\ 1744 (!f : num -> 'a -> bool. 1745 f IN (UNIV -> p) /\ (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) ==> 1746 BIGUNION (IMAGE f UNIV) IN p) ==> 1747 subsets (sigma sp a) SUBSET p``, 1748 RW_TAC std_ss [] 1749 >> MATCH_MP_TAC (Q.SPECL [`sp`, `a`, `p`] SIGMA_PROPERTY_DISJOINT_LEMMA) 1750 >> RW_TAC std_ss [dynkin_system_def, space_def, subsets_def] 1751 >> `sp IN a` by PROVE_TAC [ALGEBRA_SPACE, space_def, subsets_def] 1752 >> PROVE_TAC [SUBSET_DEF]); 1753 1754val SIGMA_PROPERTY_DISJOINT = store_thm 1755 ("SIGMA_PROPERTY_DISJOINT", 1756 ``!sp p a. 1757 algebra (sp,a) /\ a SUBSET p /\ 1758 (!s. s IN (p INTER subsets (sigma sp a)) ==> sp DIFF s IN p) /\ 1759 (!f : num -> 'a -> bool. 1760 f IN (UNIV -> p INTER subsets (sigma sp a)) /\ (f 0 = {}) /\ 1761 (!n. f n SUBSET f (SUC n)) ==> 1762 BIGUNION (IMAGE f UNIV) IN p) /\ 1763 (!f : num -> 'a -> bool. 1764 f IN (UNIV -> p INTER subsets (sigma sp a)) /\ 1765 (!i j. i <> j ==> DISJOINT (f i) (f j)) ==> 1766 BIGUNION (IMAGE f UNIV) IN p) ==> 1767 subsets (sigma sp a) SUBSET p``, 1768 RW_TAC std_ss [IN_FUNSET, IN_UNIV, IN_INTER] 1769 >> Suff `subsets (sigma sp a) SUBSET p INTER subsets (sigma sp a)` 1770 >- (KILL_TAC 1771 >> SIMP_TAC std_ss [SUBSET_INTER]) 1772 >> MATCH_MP_TAC 1773 (Q.SPECL [`sp`, `p INTER subsets (sigma sp a)`, `a`] SIGMA_PROPERTY_DISJOINT_WEAK_ALT) 1774 >> RW_TAC std_ss [SUBSET_INTER, IN_INTER, IN_FUNSET, IN_UNIV] 1775 >| (* 5 subgoals *) 1776 [ (* goal 1 (of 5) *) 1777 REWRITE_TAC [SIGMA_SUBSET_SUBSETS], 1778 (* goal 2 (of 5) *) 1779 REWRITE_TAC [subset_class_def] \\ 1780 RW_TAC std_ss [IN_INTER] \\ 1781 `subset_class sp a` by PROVE_TAC [algebra_def, space_def, subsets_def] \\ 1782 POP_ASSUM (MP_TAC o (MATCH_MP SIGMA_ALGEBRA_SIGMA)) \\ 1783 RW_TAC std_ss [sigma_algebra_def, algebra_def, space_def, subsets_def, SPACE_SIGMA] \\ 1784 fs [subset_class_def], 1785 (* goal (3 of 5) *) 1786 (MP_TAC o Q.SPECL [`sp`,`a`]) SIGMA_ALGEBRA_SIGMA 1787 >> Q.PAT_X_ASSUM `algebra (sp,a)` MP_TAC 1788 >> RW_TAC std_ss [algebra_def, space_def, subsets_def] 1789 >> POP_ASSUM MP_TAC 1790 >> NTAC 3 (POP_ASSUM (K ALL_TAC)) 1791 >> Know `space (sigma sp a) = sp` >- RW_TAC std_ss [sigma_def, space_def] 1792 >> RW_TAC std_ss [SIGMA_ALGEBRA, algebra_def, subsets_def, space_def], 1793 (* goal 4 (of 5) *) 1794 MATCH_MP_TAC SIGMA_ALGEBRA_COUNTABLE_UNION 1795 >> Q.PAT_X_ASSUM `algebra (sp,a)` MP_TAC 1796 >> RW_TAC std_ss [SIGMA_ALGEBRA_SIGMA, COUNTABLE_IMAGE_NUM, SUBSET_DEF, 1797 IN_IMAGE, IN_UNIV, algebra_def, subsets_def, space_def] 1798 >> PROVE_TAC [], 1799 (* goal 5 (of 5) *) 1800 MATCH_MP_TAC SIGMA_ALGEBRA_COUNTABLE_UNION 1801 >> Q.PAT_X_ASSUM `algebra (sp,a)` MP_TAC 1802 >> RW_TAC std_ss [SIGMA_ALGEBRA_SIGMA, COUNTABLE_IMAGE_NUM, SUBSET_DEF, 1803 IN_IMAGE, IN_UNIV, algebra_def, subsets_def, space_def] 1804 >> PROVE_TAC [] ]); 1805 1806(* Every sigma-algebra is a Dynkin system *) 1807val SIGMA_ALGEBRA_IMP_DYNKIN_SYSTEM = store_thm 1808 ("SIGMA_ALGEBRA_IMP_DYNKIN_SYSTEM", ``!a. sigma_algebra a ==> dynkin_system a``, 1809 rpt STRIP_TAC 1810 >> REWRITE_TAC [dynkin_system_def] 1811 >> CONJ_TAC >- PROVE_TAC [SIGMA_ALGEBRA] 1812 >> CONJ_TAC >- PROVE_TAC [sigma_algebra_def, ALGEBRA_SPACE] 1813 >> CONJ_TAC >- PROVE_TAC [SIGMA_ALGEBRA] 1814 >> PROVE_TAC [SIGMA_ALGEBRA_ALT]); 1815 1816(* A Dynkin system d is a sigma-algebra iff it is stable under finite intersections *) 1817val DYNKIN_LEMMA = store_thm 1818 ("DYNKIN_LEMMA", 1819 ``!d. dynkin_system d /\ (!s t. s IN subsets d /\ t IN subsets d ==> s INTER t IN subsets d) 1820 <=> sigma_algebra d``, 1821 GEN_TAC >> reverse EQ_TAC 1822 >- (rpt STRIP_TAC >- IMP_RES_TAC SIGMA_ALGEBRA_IMP_DYNKIN_SYSTEM \\ 1823 MATCH_MP_TAC ALGEBRA_INTER >> PROVE_TAC [sigma_algebra_def]) 1824 >> rpt STRIP_TAC 1825 (* it remains to show that a INTER-stable Dynkin system is sigma-algebra *) 1826 >> REWRITE_TAC [SIGMA_ALGEBRA_ALT, ALGEBRA_ALT_INTER] 1827 >> rpt CONJ_TAC >- PROVE_TAC [dynkin_system_def] 1828 >- PROVE_TAC [DYNKIN_SYSTEM_EMPTY] 1829 >- PROVE_TAC [dynkin_system_def] 1830 >- ASM_REWRITE_TAC [] 1831 (* now the last hard part *) 1832 >> rpt STRIP_TAC 1833 >> `subset_class (space d) (subsets d)` by PROVE_TAC [dynkin_system_def] 1834 >> fs [subset_class_def, IN_FUNSET, IN_UNIV] 1835 >> MP_TAC (Q.SPECL [`space d`, `subsets d`, `f`] SETS_TO_DISJOINT_SETS) 1836 >> RW_TAC std_ss [] 1837 >> POP_ASSUM (REWRITE_TAC o wrap) 1838 >> MATCH_MP_TAC DYNKIN_SYSTEM_COUNTABLY_DUNION 1839 >> fs [IN_FUNSET, IN_UNIV] 1840(* !x. g x IN subsets d *) 1841 >> MP_TAC (Q.SPECL [`subsets d`, `\i. space d DIFF f i`] DINTER_IMP_FINITE_INTER) 1842 >> Know `(\i. space d DIFF f i) IN (UNIV -> subsets d)` 1843 >- (SIMP_TAC std_ss [IN_FUNSET, IN_UNIV] \\ 1844 GEN_TAC >> MATCH_MP_TAC DYNKIN_SYSTEM_COMPL >> art []) 1845 >> RW_TAC std_ss [] 1846 >> STRIP_ASSUME_TAC (Q.SPEC `x` LESS_0_CASES) >- fs [] 1847 >> Q.PAT_X_ASSUM `!n. 0 < n ==> (g n = X)` 1848 (fn th => MP_TAC (MATCH_MP th (ASSUME ``0 < x:num``))) 1849 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1850 >> PROVE_TAC []); 1851 1852val DYNKIN_SUBSET_SIGMA = store_thm 1853 ("DYNKIN_SUBSET_SIGMA", 1854 ``!sp sts. subset_class sp sts ==> subsets (dynkin sp sts) SUBSET subsets (sigma sp sts)``, 1855 rpt STRIP_TAC 1856 >> ASSUME_TAC 1857 (Q.SPEC `sp` (MATCH_MP DYNKIN_MONOTONE (Q.SPECL [`sp`, `sts`] SIGMA_SUBSET_SUBSETS))) 1858 >> Suff `subsets (dynkin sp (subsets (sigma sp sts))) = subsets (sigma sp sts)` 1859 >- PROVE_TAC [] 1860 >> IMP_RES_TAC SIGMA_ALGEBRA_SIGMA 1861 >> IMP_RES_TAC SIGMA_ALGEBRA_IMP_DYNKIN_SYSTEM 1862 >> POP_ASSUM (MP_TAC o (MATCH_MP DYNKIN_STABLE)) 1863 >> REWRITE_TAC [SPACE_SIGMA] 1864 >> DISCH_THEN (ASM_REWRITE_TAC o wrap)); 1865 1866(* if generator is stable under finite intersections, then dynkin(g) = sigma(g) *) 1867val DYNKIN_THM = store_thm 1868 ("DYNKIN_THM", 1869 ``!sp sts. subset_class sp sts /\ (!s t. s IN sts /\ t IN sts ==> s INTER t IN sts) 1870 ==> (dynkin sp sts = sigma sp sts)``, 1871 rpt STRIP_TAC 1872 >> ONCE_REWRITE_TAC [SYM (Q.SPEC `dynkin sp sts` SPACE), 1873 SYM (Q.SPEC `sigma sp sts` SPACE)] 1874 >> REWRITE_TAC [SPACE_DYNKIN, SPACE_SIGMA] 1875 >> SIMP_TAC std_ss [] 1876 >> REWRITE_TAC [SET_EQ_SUBSET] 1877 >> CONJ_TAC >- IMP_RES_TAC DYNKIN_SUBSET_SIGMA 1878 (* goal: subsets (sigma sp sts) SUBSET subsets (dynkin sp sts) *) 1879 >> Suff `sigma_algebra (dynkin sp sts)` 1880 >- (DISCH_TAC \\ 1881 ASSUME_TAC (Q.SPECL [`sp`, `sts`] DYNKIN_SUBSET_SUBSETS) \\ 1882 POP_ASSUM (ASSUME_TAC o (Q.SPEC `sp`) o (MATCH_MP SIGMA_MONOTONE)) \\ 1883 IMP_RES_TAC SIGMA_STABLE \\ 1884 fs [SPACE_DYNKIN]) 1885 (* goal: sigma_algebra (dynkin sp sts) *) 1886 >> REWRITE_TAC [GSYM DYNKIN_LEMMA] 1887 >> CONJ_TAC >- PROVE_TAC [DYNKIN] 1888 (* goal: (dynkin sp sts) is INTER-stable *) 1889 >> Q.ABBREV_TAC `D = \d. (sp, {q | q SUBSET sp /\ q INTER d IN (subsets (dynkin sp sts))})` 1890 >> Suff `!d. d IN subsets (dynkin sp sts) ==> dynkin_system (D d)` 1891 >- (DISCH_TAC \\ 1892 ASSUME_TAC (Q.SPECL [`sp`, `sts`] DYNKIN_SUBSET_SUBSETS) \\ 1893 Know `!g. g IN sts ==> sts SUBSET (subsets (D g))` 1894 >- (REWRITE_TAC [SUBSET_DEF] >> rpt STRIP_TAC \\ 1895 `x INTER g IN sts` by PROVE_TAC [] \\ 1896 Q.UNABBREV_TAC `D` >> BETA_TAC \\ 1897 RW_TAC std_ss [subsets_def, GSPECIFICATION] >- PROVE_TAC [subset_class_def] \\ 1898 PROVE_TAC [DYNKIN_SUBSET_SUBSETS, SUBSET_DEF]) >> DISCH_TAC \\ 1899 Know `!g. g IN sts ==> subsets (dynkin sp sts) SUBSET subsets (D g)` 1900 >- (rpt STRIP_TAC \\ 1901 `sts SUBSET subsets (D g)` by PROVE_TAC [] \\ 1902 POP_ASSUM (MP_TAC o (Q.SPEC `sp`) o (MATCH_MP DYNKIN_MONOTONE)) \\ 1903 `dynkin_system (D g)` by PROVE_TAC [SUBSET_DEF] \\ 1904 POP_ASSUM (MP_TAC o (MATCH_MP DYNKIN_STABLE)) \\ 1905 `space (D g) = sp` by METIS_TAC [space_def] \\ 1906 POP_ASSUM (REWRITE_TAC o wrap) \\ 1907 DISCH_THEN (ASM_REWRITE_TAC o wrap)) >> DISCH_TAC \\ 1908 Know `!g d. g IN sts /\ d IN subsets (dynkin sp sts) ==> 1909 d INTER g IN subsets (dynkin sp sts)` 1910 >- (rpt STRIP_TAC \\ 1911 `d IN subsets (D g)` by PROVE_TAC [SUBSET_DEF] \\ 1912 POP_ASSUM MP_TAC \\ 1913 Q.UNABBREV_TAC `D` >> BETA_TAC \\ 1914 RW_TAC std_ss [subsets_def, GSPECIFICATION]) >> DISCH_TAC \\ 1915 Know `!d. d IN subsets (dynkin sp sts) ==> sts SUBSET subsets (D d)` 1916 >- (rpt STRIP_TAC \\ 1917 REWRITE_TAC [SUBSET_DEF] >> rpt STRIP_TAC \\ 1918 Q.UNABBREV_TAC `D` >> BETA_TAC \\ 1919 RW_TAC std_ss [subsets_def, GSPECIFICATION] >- PROVE_TAC [subset_class_def] \\ 1920 ONCE_REWRITE_TAC [INTER_COMM] \\ 1921 PROVE_TAC []) >> DISCH_TAC \\ 1922 Know `!d. d IN subsets (dynkin sp sts) ==> subsets (dynkin sp sts) SUBSET subsets (D d)` 1923 >- (rpt STRIP_TAC \\ 1924 `sts SUBSET subsets (D d)` by PROVE_TAC [] \\ 1925 POP_ASSUM (MP_TAC o (Q.SPEC `sp`) o (MATCH_MP DYNKIN_MONOTONE)) \\ 1926 `dynkin_system (D d)` by PROVE_TAC [SUBSET_DEF] \\ 1927 POP_ASSUM (MP_TAC o (MATCH_MP DYNKIN_STABLE)) \\ 1928 `space (D d) = sp` by METIS_TAC [space_def] \\ 1929 POP_ASSUM (REWRITE_TAC o wrap) \\ 1930 DISCH_THEN (ASM_REWRITE_TAC o wrap)) >> DISCH_TAC \\ 1931 rpt STRIP_TAC \\ 1932 `subsets (dynkin sp sts) SUBSET subsets (D t)` by PROVE_TAC [] \\ 1933 POP_ASSUM MP_TAC \\ 1934 REWRITE_TAC [SUBSET_DEF] >> rpt STRIP_TAC \\ 1935 `s IN subsets (D t)` by PROVE_TAC [] \\ 1936 POP_ASSUM MP_TAC \\ 1937 Q.UNABBREV_TAC `D` >> BETA_TAC \\ 1938 RW_TAC std_ss [subsets_def, GSPECIFICATION]) 1939 (* !d. d IN subsets (dynkin sp sts) ==> dynkin_system (D d) *) 1940 >> rpt STRIP_TAC 1941 >> REWRITE_TAC [dynkin_system_def] 1942 >> STRONG_CONJ_TAC 1943 >- (FULL_SIMP_TAC std_ss [subset_class_def] \\ 1944 GEN_TAC >> Q.UNABBREV_TAC `D` >> BETA_TAC \\ 1945 RW_TAC std_ss [subsets_def, GSPECIFICATION, space_def]) 1946 >> DISCH_TAC 1947 >> STRONG_CONJ_TAC 1948 >- (Q.UNABBREV_TAC `D` >> BETA_TAC \\ 1949 RW_TAC std_ss [GSPECIFICATION, space_def, subsets_def, SUBSET_REFL] \\ 1950 fs [space_def, subsets_def] \\ 1951 STRIP_ASSUME_TAC (MATCH_MP DYNKIN (ASSUME ``subset_class sp sts``)) \\ 1952 `d SUBSET sp` by PROVE_TAC [subset_class_def] \\ 1953 `sp INTER d = d` by PROVE_TAC [INTER_SUBSET_EQN] \\ 1954 POP_ASSUM (ASM_REWRITE_TAC o wrap)) 1955 >> DISCH_TAC 1956 >> STRONG_CONJ_TAC 1957 >- ((* !s. s IN subsets (D d) ==> space (D d) DIFF s IN subsets (D d) *) 1958 `space (D d) = sp` by METIS_TAC [space_def]\\ 1959 POP_ASSUM (fs o wrap) \\ 1960 rpt STRIP_TAC \\ 1961 Q.UNABBREV_TAC `D` >> fs [subsets_def] \\ 1962 Know `(sp DIFF s) INTER d = sp DIFF ((s INTER d) UNION (sp DIFF d))` >- ASM_SET_TAC [] \\ 1963 DISCH_THEN (REWRITE_TAC o wrap) \\ 1964 `dynkin_system (dynkin sp sts)` by PROVE_TAC [DYNKIN] \\ 1965 MATCH_MP_TAC (REWRITE_RULE [SPACE_DYNKIN] (Q.SPEC `dynkin sp sts` DYNKIN_SYSTEM_COMPL)) \\ 1966 ASM_REWRITE_TAC [] \\ 1967 `DISJOINT (s INTER d) (sp DIFF d)` by ASM_SET_TAC [] \\ 1968 MATCH_MP_TAC (Q.SPEC `dynkin sp sts` DYNKIN_SYSTEM_DUNION) \\ 1969 ASM_REWRITE_TAC [] \\ 1970 MATCH_MP_TAC (REWRITE_RULE [SPACE_DYNKIN] (Q.SPEC `dynkin sp sts` DYNKIN_SYSTEM_COMPL)) \\ 1971 ASM_REWRITE_TAC []) 1972 >> DISCH_TAC 1973 (* final goal *) 1974 >> rpt STRIP_TAC 1975 >> `!i j. i <> i ==> DISJOINT (f i INTER d) (f j INTER d)` by ASM_SET_TAC [] 1976 >> Q.UNABBREV_TAC `D` >> BETA_TAC 1977 >> REWRITE_TAC [subsets_def] 1978 >> RW_TAC std_ss [GSPECIFICATION] 1979 >- (REWRITE_TAC [BIGUNION_SUBSET, IN_IMAGE] \\ 1980 rpt STRIP_TAC >> fs [subsets_def, IN_FUNSET, IN_UNIV]) 1981 >> fs [subsets_def, IN_FUNSET, IN_UNIV] 1982 >> REWRITE_TAC [BIGUNION_OVER_INTER_L] 1983 >> fs [space_def] 1984 >> MATCH_MP_TAC DYNKIN_SYSTEM_COUNTABLY_DUNION 1985 >> CONJ_TAC >- PROVE_TAC [DYNKIN] 1986 >> CONJ_TAC >- (REWRITE_TAC [IN_FUNSET, IN_UNIV] >> PROVE_TAC []) 1987 >> rpt STRIP_TAC 1988 >> `DISJOINT (f i) (f j)` by PROVE_TAC [] 1989 >> BETA_TAC >> ASM_SET_TAC []); 1990 1991 1992(* ------------------------------------------------------------------------- *) 1993(* Some further additions by Concordia HVG (M. Qasim & W. Ahmed) *) 1994(* ------------------------------------------------------------------------- *) 1995 1996(* |- semiring (sp,sts) <=> 1997 subset_class sp sts /\ {} IN sts /\ 1998 (!s t. s IN sts /\ t IN sts ==> s INTER t IN sts) /\ 1999 !s t. 2000 s IN sts /\ t IN sts ==> 2001 ?c. c SUBSET sts /\ FINITE c /\ disjoint c /\ (s DIFF t = BIGUNION c) 2002 *) 2003val semiring_alt = save_thm 2004 ("semiring_alt", 2005 REWRITE_RULE [space_def, subsets_def] (Q.SPEC `(sp,sts)` semiring_def)); 2006 2007Theorem INTER_SPACE_EQ1 : (* was: Int_space_eq1 *) 2008 !sp sts . subset_class sp sts ==> !x. x IN sts ==> (sp INTER x = x) 2009Proof 2010 rpt GEN_TAC THEN SET_TAC [subset_class_def] 2011QED 2012 2013Theorem INTER_SPACE_REDUCE : (* was: Int_space_eq2 *) 2014 !sp sts. subset_class sp sts ==> !x. x IN sts ==> (x INTER sp = x) 2015Proof 2016 rpt GEN_TAC THEN SET_TAC [subset_class_def] 2017QED 2018 2019Theorem SEMIRING_SETS_COLLECT : (* was: sets_Collect_conj *) 2020 !sp sts P Q. semiring (sp, sts) /\ 2021 {x | x IN sp /\ P x} IN sts /\ 2022 {x | x IN sp /\ Q x} IN sts ==> 2023 {x | x IN sp /\ P x /\ Q x} IN sts 2024Proof 2025 rpt GEN_TAC THEN SIMP_TAC std_ss [semiring_def] THEN 2026 rpt STRIP_TAC THEN 2027 FIRST_X_ASSUM (K_TAC o SPECL 2028 [``{x | x IN sp /\ P x}``,``{x | x IN sp /\ Q x}``]) THEN 2029 FIRST_X_ASSUM (MP_TAC o SPECL 2030 [``{x | x IN sp /\ P x}``,``{x | x IN sp /\ Q x}``]) THEN 2031 ASM_SIMP_TAC std_ss [GSPECIFICATION, INTER_DEF] THEN 2032 REWRITE_TAC [SET_RULE ``(A /\ B) /\ A /\ C <=> A /\ B /\ C``] THEN 2033 METIS_TAC[subsets_def] 2034QED 2035 2036(* |- ring (sp,sts) <=> 2037 subset_class sp sts /\ {} IN sts /\ 2038 (!s t. s IN sts /\ t IN sts ==> s UNION t IN sts) /\ 2039 !s t. s IN sts /\ t IN sts ==> s DIFF t IN sts 2040 *) 2041val ring_alt = save_thm 2042 ("ring_alt", 2043 REWRITE_RULE [space_def, subsets_def] (Q.SPEC `(sp,sts)` ring_def)); 2044 2045(* A semiring becomes a ring if it's stable under finite union *) 2046val ring_and_semiring = store_thm 2047 ("ring_and_semiring", 2048 ``!r. ring r <=> 2049 semiring r /\ 2050 !s t. s IN (subsets r) /\ t IN (subsets r) ==> s UNION t IN (subsets r)``, 2051 GEN_TAC >> EQ_TAC >> RW_TAC std_ss [] 2052 >- (MATCH_MP_TAC RING_IMP_SEMIRING >> art []) 2053 >- (MATCH_MP_TAC RING_UNION >> art []) 2054 >> RW_TAC std_ss [ring_def] >> fs [semiring_def] 2055 >> Q.PAT_X_ASSUM `!s t. s IN subsets r /\ t IN subsets r ==> ?c. X` 2056 (MP_TAC o (Q.SPECL [`s`, `t`])) 2057 >> RW_TAC std_ss [] 2058 >> POP_ORW 2059 >> IMP_RES_TAC finite_decomposition_simple 2060 >> Cases_on `n = 0` 2061 >- (fs [COUNT_ZERO, IMAGE_EMPTY, BIGUNION_EMPTY]) 2062 >> `0 < n` by RW_TAC arith_ss [] 2063 >> fs [SUBSET_DEF, IN_IMAGE, IN_COUNT] 2064 >> irule DUNION_IMP_FINITE_UNION >> art [] 2065 >> RW_TAC std_ss []); 2066 2067Theorem RING_FINITE_BIGUNION1 : (* was: finite_Union *) 2068 !X sp sts. ring (sp, sts) /\ FINITE X ==> X SUBSET sts ==> BIGUNION X IN sts 2069Proof 2070 rpt GEN_TAC THEN 2071 REWRITE_TAC [ring_def,subsets_def] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN 2072 SPEC_TAC (``X:('a->bool)->bool``,``X:('a->bool)->bool``) THEN 2073 SET_INDUCT_TAC THENL 2074 [FULL_SIMP_TAC std_ss [semiring_def, BIGUNION_EMPTY], ALL_TAC] THEN 2075 DISCH_TAC THEN REWRITE_TAC [BIGUNION_INSERT] THEN FIRST_ASSUM MATCH_MP_TAC THEN 2076 ASM_SET_TAC [] 2077QED 2078 2079Theorem RING_FINITE_BIGUNION2 : (* was: finite_UN *) 2080 !A N sp sts. ring (sp, sts) /\ FINITE N /\ (!i. i IN N ==> A i IN sts) ==> 2081 BIGUNION {A i | i IN N} IN sts 2082Proof 2083 rpt GEN_TAC THEN 2084 REWRITE_TAC [ring_def,subsets_def] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN 2085 POP_ASSUM MP_TAC THEN SPEC_TAC (``N:'a->bool``,``N:'a->bool``) THEN 2086 SET_INDUCT_TAC THENL 2087 [REWRITE_TAC [SET_RULE ``{A i | i IN {}} = {}``, BIGUNION_EMPTY] THEN 2088 FULL_SIMP_TAC std_ss [semiring_def], ALL_TAC] THEN 2089 DISCH_TAC THEN REWRITE_TAC [IN_INSERT] THEN 2090 REWRITE_TAC [SET_RULE ``BIGUNION {A i | (i = e) \/ i IN s} = 2091 BIGUNION {A e} UNION BIGUNION {A i | i IN s}``] THEN 2092 FIRST_ASSUM MATCH_MP_TAC THEN REWRITE_TAC [BIGUNION_SING] THEN 2093 ASM_SET_TAC [] 2094QED 2095 2096Theorem RING_DIFF_ALT : (* was: Diff *) 2097 !a b sp sts. ring (sp, sts) /\ a IN sts /\ b IN sts ==> a DIFF b IN sts 2098Proof 2099 rpt GEN_TAC THEN REWRITE_TAC [ring_def,subsets_def, semiring_def] THEN 2100 STRIP_TAC THEN 2101 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN 2102 FIRST_ASSUM (MP_TAC o SPECL [``a:'a->bool``,``b:'a->bool``]) THEN 2103 rpt STRIP_TAC THEN FULL_SIMP_TAC std_ss [] THEN 2104 UNDISCH_TAC ``c SUBSET sts:('a->bool)->bool`` THEN 2105 MATCH_MP_TAC RING_FINITE_BIGUNION1 THEN 2106 EXISTS_TAC ``sp:'a->bool`` THEN 2107 FULL_SIMP_TAC std_ss [ring_def, subsets_def, semiring_def] 2108QED 2109 2110Theorem ring_alt_pow_imp : (* was: ring_of_setsI *) 2111 !sp sts. sts SUBSET POW sp /\ {} IN sts /\ 2112 (!a b. a IN sts /\ b IN sts ==> a UNION b IN sts) /\ 2113 (!a b. a IN sts /\ b IN sts ==> a DIFF b IN sts) ==> ring (sp, sts) 2114Proof 2115 REWRITE_TAC [ring_def, subsets_def, semiring_def, subset_class_def, POW_DEF] THEN 2116 REWRITE_TAC [SET_RULE ``sts SUBSET {s | s SUBSET sp} <=> 2117 !x. x IN sts ==> x SUBSET sp``] THEN 2118 rpt STRIP_TAC THEN ASM_SIMP_TAC std_ss [space_def] THENL 2119 [REWRITE_TAC [SET_RULE ``s INTER t = s DIFF (s DIFF t)``] THEN 2120 ASM_SET_TAC [], ALL_TAC] THEN 2121 REWRITE_TAC [disjoint] THEN EXISTS_TAC ``{(s:'a->bool) DIFF t}`` THEN 2122 SIMP_TAC std_ss [BIGUNION_SING, FINITE_SING, IN_SING, SUBSET_DEF] THEN 2123 ASM_SET_TAC [] 2124QED 2125 2126Theorem ring_alt_pow : (* was: ring_of_sets_iff *) 2127 !sp sts. ring (sp, sts) <=> 2128 sts SUBSET POW sp /\ {} IN sts /\ 2129 (!s t. s IN sts /\ t IN sts ==> s UNION t IN sts) /\ 2130 (!s t. s IN sts /\ t IN sts ==> s DIFF t IN sts) 2131Proof 2132 rpt GEN_TAC THEN EQ_TAC THENL 2133 [ALL_TAC, METIS_TAC [ring_alt_pow_imp]] THEN 2134 REWRITE_TAC [ring_def, subsets_def, space_def, semiring_def, subset_class_def, POW_DEF] THEN 2135 REWRITE_TAC [SET_RULE ``sts SUBSET {s | s SUBSET sp} <=> 2136 !x. x IN sts ==> x SUBSET sp``] THEN 2137 rpt STRIP_TAC THEN ASM_SIMP_TAC std_ss [] THEN 2138 MATCH_MP_TAC RING_DIFF_ALT THEN EXISTS_TAC ``sp:'a->bool`` THEN 2139 ASM_SIMP_TAC std_ss [ring_def, space_def, subsets_def, semiring_def, subset_class_def] 2140QED 2141 2142Theorem RING_BIGUNION : (* was: UNION_in_sets *) 2143 !sp sts (A:num->'a->bool) n. 2144 ring (sp,sts) /\ IMAGE A UNIV SUBSET sts ==> 2145 BIGUNION {A i | i < n} IN sts 2146Proof 2147 GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THENL 2148 [SIMP_TAC real_ss [GSPECIFICATION] THEN 2149 REWRITE_TAC [SET_RULE ``{A i | i | F} = {}``] THEN 2150 SIMP_TAC std_ss [BIGUNION_EMPTY, ring_alt, semiring_alt], 2151 ALL_TAC] THEN 2152 FULL_SIMP_TAC std_ss [GSPECIFICATION] THEN 2153 RW_TAC std_ss [ARITH_PROVE ``i < SUC n <=> i < n \/ (i = n)``] THEN 2154 REWRITE_TAC [SET_RULE ``BIGUNION {(A:num->'a->bool) i | i < n \/ (i = n)} = 2155 BIGUNION {A i | i < n} UNION A n``] THEN 2156 FULL_SIMP_TAC std_ss [ring_alt_pow] THEN 2157 FIRST_X_ASSUM MATCH_MP_TAC THEN FULL_SIMP_TAC std_ss [SUBSET_DEF] THEN 2158 FIRST_X_ASSUM MATCH_MP_TAC THEN SET_TAC [] 2159QED 2160 2161Theorem ring_disjointed_sets : (* was: range_disjointed_sets *) 2162 !sp sts A. ring (sp,sts) /\ IMAGE A UNIV SUBSET sts ==> 2163 IMAGE (\n. disjointed A n) UNIV SUBSET sts 2164Proof 2165 RW_TAC std_ss [disjointed] THEN 2166 SIMP_TAC std_ss [IN_IMAGE, SUBSET_DEF, IN_UNIV] THEN 2167 FULL_SIMP_TAC std_ss [GSPECIFICATION, ring_alt_pow] THEN 2168 RW_TAC std_ss [] THEN FIRST_ASSUM MATCH_MP_TAC THEN 2169 KNOW_TAC 2170 ``BIGUNION {(A:num->'a->bool) i | i IN {x | 0 <= x /\ x < n}} IN sts`` THENL 2171 [SIMP_TAC std_ss [GSPECIFICATION] THEN 2172 MATCH_MP_TAC RING_BIGUNION THEN SIMP_TAC std_ss [ring_alt_pow] THEN 2173 METIS_TAC [], DISCH_TAC] THEN 2174 FULL_SIMP_TAC std_ss [GSPECIFICATION, SUBSET_DEF] THEN ASM_SET_TAC [] 2175QED 2176 2177Theorem RING_INSERT : (* was: insert_in_sets *) 2178 !x A sp sts. ring (sp,sts) /\ {x} IN sts /\ A IN sts ==> x INSERT A IN sts 2179Proof 2180 REWRITE_TAC [ring_def, subsets_def, space_def] THEN rpt STRIP_TAC THEN 2181 ONCE_REWRITE_TAC [SET_RULE ``x INSERT A = {x} UNION A``] THEN 2182 ASM_SET_TAC [] 2183QED 2184 2185Theorem RING_SETS_COLLECT_FINITE : (* was: sets_collect_finite_Ex *) 2186 !sp sts s P. ring (sp, sts) /\ 2187 (!i. i IN s ==> {x | x IN sp /\ P i x} IN sts) /\ FINITE s 2188 ==> {x | x IN sp /\ (?i. i IN s /\ P i x)} IN sts 2189Proof 2190 rpt GEN_TAC THEN SIMP_TAC std_ss [ring_def, subsets_def, space_def] THEN 2191 rpt STRIP_TAC THEN 2192 KNOW_TAC ``{x | x IN sp /\ (?i. i IN s /\ P i x)} = 2193 BIGUNION {{x | x IN sp /\ P i x} | i IN s}`` THENL 2194 [SIMP_TAC std_ss [EXTENSION, BIGUNION, GSPECIFICATION] THEN 2195 GEN_TAC THEN EQ_TAC THENL [ALL_TAC, ASM_SET_TAC []] THEN 2196 STRIP_TAC THEN EXISTS_TAC ``{x | x IN sp /\ P i x}`` THEN 2197 CONJ_TAC THENL [ALL_TAC, ASM_SET_TAC []] THEN EXISTS_TAC ``i:'b`` THEN 2198 ASM_SIMP_TAC std_ss [GSPECIFICATION], ALL_TAC] THEN 2199 DISC_RW_KILL THEN 2200 KNOW_TAC ``{{x | x IN sp /\ P i x} | i IN s} SUBSET sts`` THENL 2201 [SIMP_TAC std_ss [SUBSET_DEF, GSPECIFICATION] THEN GEN_TAC THEN 2202 STRIP_TAC THEN ASM_REWRITE_TAC [] THEN FIRST_ASSUM MATCH_MP_TAC THEN 2203 ASM_REWRITE_TAC [], MATCH_MP_TAC RING_FINITE_BIGUNION1] THEN 2204 EXISTS_TAC ``sp:'a->bool`` THEN CONJ_TAC THENL 2205 [FULL_SIMP_TAC std_ss [ring_def, space_def, subsets_def], ALL_TAC] THEN 2206 ONCE_REWRITE_TAC [METIS [] ``{x | x IN sp /\ P i x} = 2207 (\i. {x | x IN sp /\ P i x}) i``] THEN 2208 ONCE_REWRITE_TAC [GSYM IMAGE_DEF] THEN METIS_TAC [IMAGE_FINITE] 2209QED 2210 2211Theorem algebra_alt : (* was: algebra_alt_eq *) 2212 !sp sts. algebra (sp, sts) <=> ring (sp, sts) /\ sp IN sts 2213Proof 2214 rw [] >> EQ_TAC 2215 >- (rw [] >> imp_res_tac ALGEBRA_SPACE \\ 2216 fs [algebra_def,ring_def,space_def,subsets_def] >> rw [] \\ 2217 FULL_SIMP_TAC std_ss [BIGUNION_SING, subset_class_def] \\ 2218 KNOW_TAC ``s SUBSET sp /\ t SUBSET sp ==> 2219 (s DIFF t = sp DIFF ((sp DIFF s) UNION t))`` 2220 >- SET_TAC [] \\ 2221 FULL_SIMP_TAC std_ss []) 2222 >> metis_tac [RING_SPACE_IMP_ALGEBRA, space_def, subsets_def] 2223QED 2224 2225Theorem ALGEBRA_COMPL_SETS : (* was: compl_sets *) 2226 !sp sts a. algebra (sp,sts) /\ a IN sts ==> sp DIFF a IN sts 2227Proof 2228 REWRITE_TAC [algebra_alt, ring_def, subsets_def,space_def] THEN 2229 rpt STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN 2230 POP_ASSUM MP_TAC THEN 2231 FIRST_ASSUM (MP_TAC o SPECL [``sp:'a->bool``,``a:'a->bool``]) THEN 2232 rpt STRIP_TAC THEN FULL_SIMP_TAC std_ss [] THEN 2233 UNDISCH_TAC ``c SUBSET (sts:('a->bool)->bool)`` THEN 2234 MATCH_MP_TAC RING_FINITE_BIGUNION1 THEN 2235 EXISTS_TAC ``sp:'a->bool`` THEN FULL_SIMP_TAC std_ss [ring_def, space_def, subsets_def] 2236QED 2237 2238Theorem algebra_alt_union : (* was: algebra_iff_Un *) 2239 !sp sts. algebra (sp,sts) <=> 2240 sts SUBSET (POW sp) /\ {} IN sts /\ 2241 (!a. a IN sts ==> sp DIFF a IN sts) /\ 2242 (!a b. a IN sts /\ b IN sts ==> a UNION b IN sts) 2243Proof 2244 rpt STRIP_TAC THEN REWRITE_TAC [algebra_def, subsets_def, space_def] THEN 2245 REWRITE_TAC [subset_class_def, POW_DEF] THEN 2246 REWRITE_TAC [SET_RULE ``sts SUBSET {s | s SUBSET sp} <=> 2247 (!x. x IN sts ==> x SUBSET sp)``] 2248QED 2249 2250Theorem algebra_alt_inter : (* was: algebra_iff_Int *) 2251 !sp sts. algebra (sp,sts) <=> sts SUBSET POW sp /\ {} IN sts /\ 2252 (!a. a IN sts ==> sp DIFF a IN sts) /\ 2253 (!a b. a IN sts /\ b IN sts ==> a INTER b IN sts) 2254Proof 2255 rpt STRIP_TAC THEN REWRITE_TAC [algebra_def, subsets_def, space_def] THEN 2256 REWRITE_TAC [subset_class_def, POW_DEF] THEN 2257 REWRITE_TAC [SET_RULE ``sts SUBSET {s | s SUBSET sp} <=> 2258 (!x. x IN sts ==> x SUBSET sp)``] THEN 2259 EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC [] THENL 2260 [rpt STRIP_TAC THEN KNOW_TAC ``a SUBSET sp /\ b SUBSET sp ==> 2261 (a INTER b = sp DIFF ((sp DIFF a) UNION (sp DIFF b)))`` THENL 2262 [SET_TAC [], ALL_TAC] 2263 THEN FULL_SIMP_TAC std_ss [], ALL_TAC] THEN 2264 rpt STRIP_TAC THEN KNOW_TAC ``s SUBSET sp /\ t SUBSET sp ==> 2265 (s UNION t = sp DIFF ((sp DIFF s) INTER (sp DIFF t)))`` THENL 2266 [SET_TAC [], ALL_TAC] THEN 2267 FULL_SIMP_TAC std_ss [] 2268QED 2269 2270Theorem ALGEBRA_SETS_COLLECT_NEG : (* was: sets_Collect_neg *) 2271 !sp sts P. algebra (sp,sts) /\ {x | x IN sp /\ P x} IN sts ==> 2272 {x | x IN sp /\ ~P x} IN sts 2273Proof 2274 rpt GEN_TAC THEN REWRITE_TAC [algebra_def, space_def, subsets_def] THEN 2275 RW_TAC std_ss [subset_class_def] THEN 2276 KNOW_TAC ``{x | x IN sp /\ ~P x} = sp DIFF {x | x IN sp /\ P x}`` THENL 2277 [ALL_TAC, DISC_RW_KILL THEN FULL_SIMP_TAC std_ss []] THEN SET_TAC [] 2278QED 2279 2280Theorem ALGEBRA_SETS_COLLECT_IMP : (* was: sets_Collect_imp *) 2281 !sp sts P Q. algebra (sp,sts) /\ {x | x IN sp /\ P x} IN sts ==> 2282 {x | x IN sp /\ Q x} IN sts ==> 2283 {x | x IN sp /\ (Q x ==> P x)} IN sts 2284Proof 2285 rpt GEN_TAC THEN REWRITE_TAC [algebra_alt, ring_def, space_def, subsets_def] THEN 2286 rpt STRIP_TAC THEN REWRITE_TAC [IMP_DISJ_THM] THEN 2287 REWRITE_TAC [SET_RULE ``{x | x IN sp /\ (~Q x \/ P x)} = 2288 {x | x IN sp /\ ~Q x} UNION {x | x IN sp /\ P x}``] THEN 2289 FIRST_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC std_ss [] THEN 2290 MATCH_MP_TAC ALGEBRA_SETS_COLLECT_NEG THEN 2291 FULL_SIMP_TAC std_ss [algebra_alt, ring_def, space_def, subsets_def] 2292QED 2293 2294Theorem ALGEBRA_SETS_COLLECT_CONST : (* was: sets_Collect_const *) 2295 !sp sts P. algebra (sp,sts) ==> {x | x IN sp /\ P} IN sts 2296Proof 2297 REWRITE_TAC [algebra_alt] THEN rpt STRIP_TAC THEN 2298 Cases_on `P` THENL 2299 [REWRITE_TAC [SET_RULE ``{x | x IN sp /\ T} = sp``] THEN ASM_REWRITE_TAC [], 2300 FULL_SIMP_TAC std_ss [GSPEC_F, ring_def, subsets_def, space_def]] 2301QED 2302 2303Theorem ALGEBRA_SINGLE_SET : (* was: algebra_single_set *) 2304 !X S. X SUBSET S ==> algebra (S, {{}; X; S DIFF X; S}) 2305Proof 2306 RW_TAC std_ss [algebra_def, subsets_def, space_def, subset_class_def] THEN 2307 FULL_SIMP_TAC std_ss [SET_RULE ``x IN {a;b;c;d} <=> 2308 (x = a) \/ (x = b) \/ (x = c) \/ (x = d)``] THEN TRY (ASM_SET_TAC []) 2309QED 2310 2311(* ------------------------------------------------------------------------- *) 2312(* Retricted Algebras *) 2313(* ------------------------------------------------------------------------- *) 2314 2315Theorem ALGEBRA_RESTRICT : (* was: restricted_algebra *) 2316 !sp sts a. algebra (sp,sts) /\ a IN sts ==> 2317 algebra (a,IMAGE (\s. s INTER a) sts) 2318Proof 2319 REWRITE_TAC [algebra_alt, ring_def, space_def, subsets_def, subset_class_def] THEN 2320 rpt STRIP_TAC THEN 2321 FULL_SIMP_TAC std_ss [IMAGE_DEF, GSPECIFICATION] THENL 2322 [REWRITE_TAC [INTER_SUBSET], 2323 EXISTS_TAC ``{}`` THEN ASM_SIMP_TAC std_ss [INTER_EMPTY], 2324 EXISTS_TAC ``(s' UNION s'')`` THEN 2325 CONJ_TAC THENL [SET_TAC [], ALL_TAC] THEN 2326 FULL_SIMP_TAC std_ss [], 2327 EXISTS_TAC ``s' DIFF s''`` THEN CONJ_TAC THENL [SET_TAC [], ALL_TAC] THEN 2328 MATCH_MP_TAC RING_DIFF_ALT THEN EXISTS_TAC ``sp:'a->bool`` THEN 2329 FULL_SIMP_TAC std_ss [ring_def, subsets_def, space_def, subset_class_def], 2330 EXISTS_TAC ``a:'a->bool`` THEN ASM_SET_TAC []] 2331QED 2332 2333Theorem SIGMA_ALGEBRA_RESTRICT : 2334 !sp sts a. sigma_algebra (sp,sts) /\ a IN sts ==> 2335 sigma_algebra (a,IMAGE (\s. s INTER a) sts) 2336Proof 2337 rpt STRIP_TAC 2338 >> rw [SIGMA_ALGEBRA_ALT, algebra_def, subset_class_def, IN_FUNSET] 2339 >| [ (* goal 1 (of 5) *) 2340 REWRITE_TAC [INTER_SUBSET], 2341 (* goal 2 (of 5) *) 2342 Q.EXISTS_TAC ���{}��� >> REWRITE_TAC [INTER_EMPTY] \\ 2343 MATCH_MP_TAC (REWRITE_RULE [subsets_def] 2344 (Q.SPEC ���(sp,sts)��� SIGMA_ALGEBRA_EMPTY)) >> art [], 2345 (* goal 3 (of 5) *) 2346 Q.EXISTS_TAC ���sp DIFF s'��� \\ 2347 CONJ_TAC 2348 >- (fs [SIGMA_ALGEBRA_ALT, algebra_def, subset_class_def] \\ 2349 ASM_SET_TAC []) \\ 2350 MATCH_MP_TAC (REWRITE_RULE [space_def, subsets_def] 2351 (Q.SPEC ���(sp,sts)��� SIGMA_ALGEBRA_COMPL)) >> art [], 2352 (* goal 4 (of 5) *) 2353 Q.EXISTS_TAC ���s' UNION s''��� \\ 2354 CONJ_TAC >- SET_TAC [] \\ 2355 MATCH_MP_TAC (REWRITE_RULE [subsets_def] 2356 (Q.SPEC ���(sp,sts)��� SIGMA_ALGEBRA_UNION)) >> art [], 2357 (* goal 5 (of 5) *) 2358 fs [SKOLEM_THM] \\ 2359 Q.EXISTS_TAC ���BIGUNION (IMAGE f' UNIV)��� \\ 2360 CONJ_TAC >- ASM_SET_TAC [] \\ 2361 fs [SIGMA_ALGEBRA_FN, IN_FUNSET] ] 2362QED 2363 2364Theorem SIGMA_ALGEBRA_RESTRICT_SUBSET : 2365 !sp sts a. sigma_algebra (sp,sts) /\ a IN sts ==> 2366 (IMAGE (\s. s INTER a) sts) SUBSET sts 2367Proof 2368 rw [SUBSET_DEF] 2369 >> MATCH_MP_TAC (REWRITE_RULE [subsets_def] 2370 (Q.SPEC ���(sp,sts)��� SIGMA_ALGEBRA_INTER)) >> art [] 2371QED 2372 2373Theorem sigma_algebra_alt : (* was: sigma_algebra_alt_eq *) 2374 !sp sts. sigma_algebra (sp,sts) <=> 2375 algebra (sp,sts) /\ 2376 !A. IMAGE A UNIV SUBSET sts ==> BIGUNION {A i | i IN univ(:num)} IN sts 2377Proof 2378 rpt GEN_TAC THEN REWRITE_TAC [SIGMA_ALGEBRA_ALT] THEN EQ_TAC THEN 2379 STRIP_TAC THEN ASM_REWRITE_TAC [] THEN X_GEN_TAC ``A:num->'a->bool`` THEN 2380 POP_ASSUM (MP_TAC o SPEC ``A:num->'a->bool``) THEN 2381 SIMP_TAC std_ss [IMAGE_DEF, subsets_def] THEN rpt STRIP_TAC THEN 2382 FIRST_ASSUM MATCH_MP_TAC THEN POP_ASSUM MP_TAC THEN EVAL_TAC THEN 2383 SRW_TAC[] [IN_UNIV,SUBSET_DEF,IN_FUNSET] THEN METIS_TAC[] 2384QED 2385 2386Theorem sigma_algebra_alt_pow : (* was: sigma_algebra_iff2 *) 2387 !sp sts. sigma_algebra (sp,sts) <=> 2388 sts SUBSET POW sp /\ {} IN sts /\ 2389 (!s. s IN sts ==> sp DIFF s IN sts) /\ 2390 (!A. IMAGE A UNIV SUBSET sts ==> 2391 BIGUNION {(A :num->'a->bool) i | i IN UNIV} IN sts) 2392Proof 2393 SIMP_TAC std_ss [sigma_algebra_alt, algebra_def, space_def, subsets_def] THEN 2394 rpt GEN_TAC THEN SIMP_TAC std_ss [subset_class_def, POW_DEF] THEN 2395 EQ_TAC THENL [ASM_SET_TAC [], ALL_TAC] THEN 2396 rpt STRIP_TAC THENL [ASM_SET_TAC [], ASM_SET_TAC [], ASM_SET_TAC [], 2397 ALL_TAC, ASM_SET_TAC []] THEN 2398 SIMP_TAC std_ss [UNION_BINARY] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN 2399 SIMP_TAC std_ss [BINARY_RANGE] THEN ASM_SET_TAC [] 2400QED 2401 2402val lemma = prove ((* was: countable_Union *) 2403 ``!sp sts c. sigma_algebra (sp,sts) /\ countable c /\ c SUBSET sts ==> 2404 BIGUNION c IN sts``, 2405 FULL_SIMP_TAC std_ss [sigma_algebra_def, subsets_def]); 2406 2407Theorem SIGMA_ALGEBRA_COUNTABLE_UN : (* was: countable_UN *) 2408 !sp sts A X. sigma_algebra (sp,sts) /\ IMAGE (A:num->'a->bool) X SUBSET sts ==> 2409 BIGUNION {A x | x IN X} IN sts 2410Proof 2411 REPEAT STRIP_TAC THEN 2412 KNOW_TAC 2413 ``(IMAGE (\i. if i IN X then (A:num->'a->bool) i else {}) UNIV) SUBSET sts`` 2414 THENL [POP_ASSUM MP_TAC THEN 2415 SIMP_TAC std_ss [SUBSET_DEF, IN_IMAGE] THEN REPEAT STRIP_TAC THEN 2416 FULL_SIMP_TAC std_ss [] THEN COND_CASES_TAC THENL [METIS_TAC [], ALL_TAC] THEN 2417 FULL_SIMP_TAC std_ss [sigma_algebra_alt, algebra_def, ring_alt, semiring_alt, 2418 subsets_def], ALL_TAC] THEN DISCH_TAC THEN KNOW_TAC 2419 ``BIGUNION {(\i. if i IN X then (A:num->'a->bool) i else {}) x | x IN UNIV} 2420 IN sts`` 2421 THENL [SIMP_TAC std_ss [] THEN MATCH_MP_TAC lemma THEN 2422 EXISTS_TAC ``sp:'a->bool`` THEN FULL_SIMP_TAC std_ss [] THEN 2423 CONJ_TAC THENL [ALL_TAC, ASM_SET_TAC []] THEN 2424 SIMP_TAC arith_ss [GSYM IMAGE_DEF] THEN 2425 METIS_TAC [COUNTABLE_IMAGE_NUM], DISCH_TAC] THEN KNOW_TAC `` 2426 BIGUNION {(\i. if i IN X then (A:num->'a->bool) i else {}) x | x IN univ(:num)} = 2427 BIGUNION {A x | x IN X}`` THENL [ALL_TAC, METIS_TAC []] THEN 2428 SIMP_TAC std_ss [EXTENSION, IN_BIGUNION, GSPECIFICATION] THEN GEN_TAC THEN 2429 EQ_TAC THEN REPEAT STRIP_TAC THENL 2430 [EXISTS_TAC ``s:'a->bool`` THEN FULL_SIMP_TAC std_ss [] THEN 2431 POP_ASSUM K_TAC THEN POP_ASSUM K_TAC THEN POP_ASSUM MP_TAC THEN 2432 COND_CASES_TAC THEN ASM_SET_TAC [], ALL_TAC] THEN 2433 EXISTS_TAC ``s:'a->bool`` THEN FULL_SIMP_TAC std_ss [IN_UNIV] THEN 2434 EXISTS_TAC ``x':num`` THEN ASM_SET_TAC [] 2435QED 2436 2437Theorem SIGMA_ALGEBRA_COUNTABLE_UN' : (* was: countable_UN' *) 2438 !sp sts A X. sigma_algebra (sp,sts) /\ IMAGE A X SUBSET sts /\ 2439 countable X ==> BIGUNION {A x | x IN X} IN sts 2440Proof 2441 RW_TAC std_ss [] THEN 2442 KNOW_TAC ``(IMAGE (\i. if i IN X then (A:'b->'a->bool) i else {}) UNIV) 2443 SUBSET sts`` THENL 2444 [SIMP_TAC std_ss [SUBSET_DEF, IN_IMAGE, IN_UNIV] THEN RW_TAC std_ss [] THEN 2445 COND_CASES_TAC THENL [ASM_SET_TAC [], FULL_SIMP_TAC std_ss [sigma_algebra_alt_pow]], 2446 DISCH_TAC] THEN 2447 KNOW_TAC ``BIGUNION {(\i. if i IN X then A i else {}) x | x IN UNIV} 2448 IN sts`` THENL 2449 [ALL_TAC, DISCH_TAC THEN 2450 KNOW_TAC `` 2451 BIGUNION {(\i. if i IN X then (A:'b->'a->bool) i else {}) x | x IN univ(:'b)} = 2452 BIGUNION {A x | x IN X}`` THENL [ALL_TAC, METIS_TAC []] THEN 2453 SIMP_TAC std_ss [EXTENSION, IN_BIGUNION, GSPECIFICATION] THEN GEN_TAC THEN 2454 EQ_TAC THEN rpt STRIP_TAC THENL 2455 [EXISTS_TAC ``s:'a->bool`` THEN FULL_SIMP_TAC std_ss [] THEN 2456 POP_ASSUM K_TAC THEN POP_ASSUM K_TAC THEN POP_ASSUM MP_TAC THEN 2457 COND_CASES_TAC THEN ASM_SET_TAC [], ALL_TAC] THEN 2458 EXISTS_TAC ``s:'a->bool`` THEN FULL_SIMP_TAC std_ss [IN_UNIV] THEN 2459 EXISTS_TAC ``x':'b`` THEN FULL_SIMP_TAC std_ss []] THEN 2460 RULE_ASSUM_TAC (SIMP_RULE std_ss [SIGMA_ALGEBRA]) THEN 2461 rpt (POP_ASSUM MP_TAC) THEN REWRITE_TAC [subsets_def] THEN 2462 rpt STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN 2463 ASM_SIMP_TAC std_ss [GSYM IMAGE_DEF] THEN 2464 KNOW_TAC ``countable (IMAGE (A:'b->'a->bool) X)`` THENL 2465 [rw[image_countable], DISCH_TAC] THEN 2466 ONCE_REWRITE_TAC [SET_RULE ``IMAGE (\x. if x IN X then A x else {}) univ(:'b) = 2467 (IMAGE A X) UNION IMAGE (\x. {}) (UNIV DIFF X)``] THEN 2468 MATCH_MP_TAC union_countable THEN CONJ_TAC THENL 2469 [FULL_SIMP_TAC std_ss [COUNTABLE_ALT] THEN 2470 METIS_TAC [], ALL_TAC] THEN 2471 SIMP_TAC std_ss [pred_setTheory.COUNTABLE_ALT] THEN Q.EXISTS_TAC `(\n. {}):num->'a->bool` THEN 2472 SIMP_TAC std_ss [IN_IMAGE] THEN METIS_TAC [] 2473QED 2474 2475Theorem SIGMA_ALGEBRA_COUNTABLE_INT : (* was: countable_INT *) 2476 !sp sts A X. sigma_algebra (sp,sts) /\ IMAGE (A:num->'a->bool) X SUBSET sts /\ 2477 (X <> {}) ==> BIGINTER {(A:num->'a->bool) x | x IN X} IN sts 2478Proof 2479 REPEAT STRIP_TAC THEN FULL_SIMP_TAC std_ss [GSYM MEMBER_NOT_EMPTY] THEN 2480 KNOW_TAC ``!x. x IN X ==> (A:num->'a->bool) x IN sts`` THENL 2481 [ASM_SET_TAC [], DISCH_TAC] THEN 2482 KNOW_TAC ``sp DIFF BIGUNION {sp DIFF (A:num->'a->bool) x | x IN X} IN sts`` THENL 2483 [MATCH_MP_TAC RING_DIFF_ALT THEN EXISTS_TAC ``sp:'a->bool`` THEN 2484 FULL_SIMP_TAC std_ss [sigma_algebra_alt, algebra_alt] THEN 2485 ONCE_REWRITE_TAC [METIS [] ``sp DIFF A x = (\x. sp DIFF A x) x``] THEN 2486 2487 MATCH_MP_TAC SIGMA_ALGEBRA_COUNTABLE_UN THEN EXISTS_TAC ``sp:'a->bool`` THEN 2488 FULL_SIMP_TAC std_ss [sigma_algebra_alt, algebra_alt] THEN 2489 SIMP_TAC std_ss [SUBSET_DEF, IN_IMAGE] THEN REPEAT STRIP_TAC THEN 2490 ASM_REWRITE_TAC [] THEN MATCH_MP_TAC RING_DIFF_ALT THEN EXISTS_TAC ``sp:'a->bool`` THEN 2491 ASM_SET_TAC [], DISCH_TAC] THEN 2492 KNOW_TAC ``BIGINTER {(A:num->'a->bool) x | x IN X} = 2493 sp DIFF BIGUNION {sp DIFF A x | x IN X}`` THENL 2494 [ALL_TAC, METIS_TAC []] THEN SIMP_TAC std_ss [EXTENSION] THEN GEN_TAC THEN 2495 KNOW_TAC ``sts SUBSET POW sp`` THENL 2496 [FULL_SIMP_TAC std_ss [sigma_algebra_alt, algebra_alt, ring_alt, semiring_alt, 2497 subset_class_def] THEN ASM_SET_TAC [POW_DEF], RW_TAC std_ss [POW_DEF]] THEN 2498 EQ_TAC THEN REPEAT STRIP_TAC THENL 2499 [SIMP_TAC std_ss [IN_DIFF] THEN CONJ_TAC THENL [ASM_SET_TAC [], ALL_TAC] THEN 2500 FULL_SIMP_TAC std_ss [BIGINTER, BIGUNION, GSPECIFICATION] THEN GEN_TAC THEN 2501 ASM_CASES_TAC ``x' NOTIN (s:'a->bool)`` THEN ASM_REWRITE_TAC [] THEN 2502 GEN_TAC THEN ASM_CASES_TAC ``x'' NOTIN (X:num->bool)`` THEN 2503 FULL_SIMP_TAC std_ss [SUBSET_DEF, GSPECIFICATION] THEN 2504 SIMP_TAC std_ss [DIFF_DEF, EXTENSION, GSPECIFICATION] THEN 2505 EXISTS_TAC ``x':'a`` THEN FULL_SIMP_TAC std_ss [] THEN 2506 ASM_CASES_TAC ``x' NOTIN (sp:'a->bool)`` THEN FULL_SIMP_TAC std_ss [] THEN 2507 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_SET_TAC [], ALL_TAC] THEN 2508 SIMP_TAC std_ss [BIGINTER, GSPECIFICATION] THEN GEN_TAC THEN 2509 STRIP_TAC THEN ASM_REWRITE_TAC [] THEN POP_ASSUM MP_TAC THEN 2510 POP_ASSUM K_TAC THEN FULL_SIMP_TAC std_ss [IN_DIFF, BIGUNION, GSPECIFICATION] THEN 2511 STRIP_TAC THEN CCONTR_TAC THEN UNDISCH_TAC 2512 ``!s. (!x. s <> sp DIFF (A:num->'a->bool) x \/ x NOTIN X) \/ x' NOTIN s`` THEN 2513 SIMP_TAC std_ss [] THEN EXISTS_TAC ``sp DIFF (A:num->'a->bool) x''`` THEN 2514 CONJ_TAC THENL [METIS_TAC [], ALL_TAC] THEN 2515 ASM_SIMP_TAC std_ss [IN_DIFF]); 2516 2517Theorem SIGMA_ALGEBRA_COUNTABLE_INT' : (* was: countable_INT' *) 2518 !sp sts A X. sigma_algebra (sp,sts) /\ countable X /\ (X <> {}) /\ 2519 IMAGE (A:num->'a->bool) X SUBSET sts ==> 2520 BIGINTER {(A:num->'a->bool) x | x IN X} IN sts 2521Proof 2522 METIS_TAC [SIGMA_ALGEBRA_COUNTABLE_INT] 2523QED 2524 2525(* ------------------------------------------------------------------------- *) 2526(* Initial Sigma Algebra (conributed by HVG concordia) *) 2527(* ------------------------------------------------------------------------- *) 2528 2529Inductive sigma_sets : 2530 (sigma_sets sp st {}) /\ 2531 (!a. st a ==> sigma_sets sp st a) /\ 2532 (!a. sigma_sets sp st a ==> sigma_sets sp st (sp DIFF a)) /\ 2533 (!A. (!i. sigma_sets sp st ((A :num->'a->bool) i)) ==> 2534 sigma_sets sp st (BIGUNION {A i | i IN UNIV})) 2535End 2536 2537val sigma_sets_basic = store_thm ("sigma_sets_basic", 2538 ``!sp st a. a IN st ==> a IN sigma_sets sp st``, 2539 SIMP_TAC std_ss [SPECIFICATION, sigma_sets_rules]); 2540 2541val sigma_sets_empty = store_thm ("sigma_sets_empty", 2542 ``!sp st. {} IN sigma_sets sp st``, 2543 SIMP_TAC std_ss [SPECIFICATION, sigma_sets_rules]); 2544 2545val sigma_sets_compl = store_thm ("sigma_sets_compl", 2546 ``!sp st a. a IN sigma_sets sp st ==> sp DIFF a IN sigma_sets sp st``, 2547 SIMP_TAC std_ss [SPECIFICATION, sigma_sets_rules]); 2548 2549Theorem sigma_sets_BIGUNION : (* was: sigma_sets_union *) 2550 !sp st A. (!i. (A:num->'a->bool) i IN sigma_sets sp st) ==> 2551 BIGUNION {A i | i IN UNIV} IN sigma_sets sp st 2552Proof 2553 SIMP_TAC std_ss [SPECIFICATION, sigma_sets_rules] 2554QED 2555 2556val sigma_sets_subset = store_thm ("sigma_sets_subset", 2557 ``!sp sts st. sigma_algebra (sp,sts) /\ st SUBSET sts ==> 2558 sigma_sets sp st SUBSET sts``, 2559 rpt STRIP_TAC THEN SIMP_TAC std_ss [SPECIFICATION, SUBSET_DEF] THEN 2560 HO_MATCH_MP_TAC sigma_sets_ind THEN FULL_SIMP_TAC std_ss [sigma_algebra_alt, 2561 algebra_alt, ring_def, space_def, subsets_def, subset_class_def] THEN 2562 rpt STRIP_TAC THENL 2563 [ASM_SET_TAC [], 2564 ASM_SET_TAC [], 2565 ONCE_REWRITE_TAC [GSYM SPECIFICATION] THEN MATCH_MP_TAC RING_DIFF_ALT THEN 2566 FULL_SIMP_TAC std_ss [ring_def, subsets_def, space_def, subset_class_def] THEN ASM_SET_TAC [], 2567 ONCE_REWRITE_TAC [GSYM SPECIFICATION] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN 2568 rpt STRIP_TAC THEN ASM_SET_TAC []]); 2569 2570val sigma_sets_into_sp = store_thm ("sigma_sets_into_sp", 2571 ``!sp st. st SUBSET POW sp ==> !x. x IN sigma_sets sp st ==> x SUBSET sp``, 2572 rpt GEN_TAC THEN DISCH_TAC THEN SIMP_TAC std_ss [SPECIFICATION] THEN 2573 HO_MATCH_MP_TAC sigma_sets_ind THEN FULL_SIMP_TAC std_ss [POW_DEF] THEN 2574 rpt STRIP_TAC THEN ASM_SET_TAC []); 2575 2576Theorem sigma_algebra_sigma_sets : 2577 !sp st. st SUBSET POW sp ==> sigma_algebra (sp, sigma_sets sp st) 2578Proof 2579 RW_TAC std_ss [sigma_algebra_alt_pow] THENL 2580 [SIMP_TAC std_ss [SUBSET_DEF] THEN 2581 SIMP_TAC std_ss [POW_DEF, GSPECIFICATION] THEN 2582 METIS_TAC [sigma_sets_into_sp], 2583 METIS_TAC [sigma_sets_empty], 2584 METIS_TAC [sigma_sets_compl], 2585 MATCH_MP_TAC sigma_sets_BIGUNION THEN ASM_SET_TAC []] 2586QED 2587 2588(* NOTE: this indicates that `sigma_sets = sigma` *) 2589Theorem sigma_sets_least_sigma_algebra : 2590 !sp A. A SUBSET POW sp ==> 2591 (sigma_sets sp A = 2592 BIGINTER {B | A SUBSET B /\ sigma_algebra (sp,B)}) 2593Proof 2594 rpt STRIP_TAC THEN 2595 KNOW_TAC ``!B X. A SUBSET B /\ sigma_algebra (sp,B) /\ 2596 X IN sigma_sets sp A ==> X IN B`` THENL 2597 [rpt STRIP_TAC THEN UNDISCH_TAC ``A SUBSET (B:('a->bool)->bool)`` THEN 2598 UNDISCH_TAC ``sigma_algebra (sp, B)`` THEN REWRITE_TAC [AND_IMP_INTRO] THEN 2599 DISCH_THEN (MP_TAC o MATCH_MP sigma_sets_subset) THEN ASM_SET_TAC [], 2600 DISCH_TAC] THEN 2601 KNOW_TAC 2602 ``!X. X IN BIGINTER {B | A SUBSET B /\ sigma_algebra (sp,B)} ==> 2603 !B. A SUBSET B ==> sigma_algebra (sp,B) ==> X IN B`` THENL 2604 [STRIP_TAC THEN ASM_SIMP_TAC std_ss [IN_BIGINTER, GSPECIFICATION], 2605 DISCH_TAC] THEN 2606 SIMP_TAC std_ss [EXTENSION] THEN GEN_TAC THEN EQ_TAC THENL 2607 [DISCH_TAC THEN SIMP_TAC std_ss [IN_BIGINTER, GSPECIFICATION] THEN 2608 rpt STRIP_TAC THEN FULL_SIMP_TAC std_ss [SUBSET_DEF], ALL_TAC] THEN 2609 DISCH_TAC THEN FIRST_X_ASSUM (MP_TAC o SPEC ``x:'a->bool``) THEN 2610 ASM_REWRITE_TAC [] THEN DISCH_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN 2611 rpt CONJ_TAC THENL 2612 [ASM_SIMP_TAC std_ss [SUBSET_DEF, sigma_sets_basic], 2613 ASM_SIMP_TAC std_ss [sigma_algebra_sigma_sets], 2614 ALL_TAC] THEN 2615 FULL_SIMP_TAC std_ss [AND_IMP_INTRO] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN 2616 ASM_SIMP_TAC std_ss [sigma_algebra_sigma_sets] THEN 2617 ASM_SIMP_TAC std_ss [SUBSET_DEF, sigma_sets_basic] 2618QED 2619 2620val sigma_sets_top = store_thm ("sigma_sets_top", 2621 ``!sp A. sp IN sigma_sets sp A``, 2622 METIS_TAC [sigma_sets_compl, sigma_sets_empty, DIFF_EMPTY]); 2623 2624Theorem sigma_sets_union : (* was: sigma_sets_Un *) 2625 !sp st a b. a IN sigma_sets sp st /\ b IN sigma_sets sp st ==> 2626 a UNION b IN sigma_sets sp st 2627Proof 2628 rpt STRIP_TAC THEN REWRITE_TAC [UNION_BINARY] THEN 2629 MATCH_MP_TAC sigma_sets_BIGUNION THEN GEN_TAC THEN 2630 RW_TAC std_ss [binary_def] 2631QED 2632 2633Theorem sigma_sets_BIGINTER : (* was: sigma_sets_Inter *) 2634 !sp st A. st SUBSET POW sp ==> 2635 (!i. (A :num->'a->bool) i IN sigma_sets sp st) ==> 2636 BIGINTER {A i | i IN UNIV} IN sigma_sets sp st 2637Proof 2638 rpt STRIP_TAC THEN 2639 KNOW_TAC ``(!i:num. A i IN sigma_sets sp st) ==> 2640 (!i:num. sp DIFF A i IN sigma_sets sp st)`` THENL 2641 [METIS_TAC [sigma_sets_compl], DISCH_TAC] THEN 2642 KNOW_TAC ``BIGUNION {sp DIFF A i | (i:num) IN UNIV} IN sigma_sets sp st`` THENL 2643 [ONCE_REWRITE_TAC [METIS [] ``sp DIFF A i = (\i. sp DIFF A i) i``] THEN 2644 MATCH_MP_TAC sigma_sets_BIGUNION THEN METIS_TAC [], DISCH_TAC] THEN 2645 KNOW_TAC 2646 ``sp DIFF BIGUNION {sp DIFF A i | (i:num) IN UNIV} IN sigma_sets sp st`` THENL 2647 [MATCH_MP_TAC sigma_sets_compl THEN METIS_TAC [], DISCH_TAC] THEN 2648 KNOW_TAC ``sp DIFF BIGUNION {sp DIFF A i | i IN UNIV} = 2649 BIGINTER {A i | (i:num) IN UNIV}`` THENL 2650 [ALL_TAC, METIS_TAC[]] THEN 2651 SIMP_TAC std_ss [EXTENSION] THEN GEN_TAC THEN EQ_TAC THENL 2652 [SIMP_TAC std_ss [IN_DIFF, IN_BIGUNION, IN_BIGINTER, GSPECIFICATION] THEN 2653 RW_TAC std_ss [] THEN POP_ASSUM K_TAC THEN 2654 POP_ASSUM (MP_TAC o SPEC ``sp DIFF (A:num->'a->bool) i``) THEN 2655 ASM_SET_TAC [], ALL_TAC] THEN 2656 SIMP_TAC std_ss [IN_BIGINTER, IN_DIFF, IN_BIGUNION, GSPECIFICATION] THEN 2657 RW_TAC std_ss [IN_UNIV] THENL 2658 [FIRST_X_ASSUM (MP_TAC o SPEC ``(A:num->'a->bool) i``) THEN 2659 KNOW_TAC ``(?i'. A i = (A:num->'a->bool) i')`` THENL 2660 [METIS_TAC [], DISCH_TAC THEN ASM_REWRITE_TAC []] THEN 2661 SPEC_TAC (``x``,``x``) THEN REWRITE_TAC [GSYM SUBSET_DEF] THEN 2662 UNDISCH_TAC ``st SUBSET POW (sp:'a->bool)`` THEN 2663 DISCH_THEN (MP_TAC o MATCH_MP sigma_sets_into_sp) THEN 2664 METIS_TAC [], ALL_TAC] THEN 2665 ASM_CASES_TAC ``x NOTIN s`` THEN FULL_SIMP_TAC std_ss [] THEN 2666 RW_TAC std_ss [EXTENSION] THEN EXISTS_TAC ``x`` THEN 2667 ASM_SIMP_TAC std_ss [IN_DIFF] THEN DISJ2_TAC THEN 2668 FIRST_X_ASSUM MATCH_MP_TAC THEN METIS_TAC [] 2669QED 2670 2671Theorem sigma_sets_BIGINTER2 : (* was: sigma_sets_INTER *) 2672 !sp st A N. st SUBSET POW sp /\ (!i:num. i IN N ==> A i IN sigma_sets sp st) /\ 2673 (N <> {}) ==> BIGINTER {A i | i IN N} IN sigma_sets sp st 2674Proof 2675 rpt STRIP_TAC THEN 2676 KNOW_TAC ``!i:num. (if i IN N then A i else sp) IN sigma_sets sp st`` THENL 2677 [GEN_TAC THEN COND_CASES_TAC THEN ASM_SIMP_TAC std_ss [] THEN 2678 SIMP_TAC std_ss [sigma_sets_top], DISCH_TAC] THEN 2679 KNOW_TAC ``BIGINTER {(if i IN N then (A:num->'a->bool) i else sp) | i IN UNIV} IN 2680 sigma_sets sp st`` THENL 2681 [ASM_SIMP_TAC std_ss [sigma_sets_BIGINTER], DISCH_TAC] THEN 2682 KNOW_TAC ``BIGINTER {(if i IN N then (A:num->'a->bool) i else sp) | i IN UNIV} = 2683 BIGINTER {A i | i IN N}`` THENL 2684 [ALL_TAC, METIS_TAC []] THEN 2685 UNDISCH_TAC ``st SUBSET POW (sp:'a->bool)`` THEN 2686 DISCH_THEN (MP_TAC o MATCH_MP sigma_sets_into_sp) THEN DISCH_TAC THEN 2687 ASM_SET_TAC [] 2688QED 2689 2690Theorem sigma_sets_fixpoint : (* was: sigma_sets_eq *) 2691 !sp sts. sigma_algebra (sp,sts) ==> (sigma_sets sp sts = sts) 2692Proof 2693 rpt STRIP_TAC THEN EVAL_TAC THEN CONJ_TAC THENL 2694 [MATCH_MP_TAC sigma_sets_subset THEN ASM_SIMP_TAC std_ss [SUBSET_REFL], 2695 SIMP_TAC std_ss [SUBSET_DEF, sigma_sets_basic]] 2696QED 2697 2698Theorem sigma_sets_superset_generator : 2699 !X A. A SUBSET sigma_sets X A 2700Proof 2701 SIMP_TAC std_ss [SUBSET_DEF, sigma_sets_basic] 2702QED 2703 2704(* below are shared theorems moved from (real_)measureTheory *) 2705 2706val IN_MEASURABLE = store_thm 2707 ("IN_MEASURABLE", 2708 ``!a b f. f IN measurable a b <=> 2709 sigma_algebra a /\ sigma_algebra b /\ f IN (space a -> space b) /\ 2710 (!s. s IN subsets b ==> ((PREIMAGE f s)INTER(space a)) IN subsets a)``, 2711 RW_TAC std_ss [measurable_def, GSPECIFICATION]); 2712 2713val MEASURABLE_DIFF_PROPERTY = store_thm 2714 ("MEASURABLE_DIFF_PROPERTY", 2715 ``!a b f. sigma_algebra a /\ sigma_algebra b /\ 2716 f IN (space a -> space b) /\ 2717 (!s. s IN subsets b ==> PREIMAGE f s IN subsets a) ==> 2718 (!s. s IN subsets b ==> 2719 (PREIMAGE f (space b DIFF s) = space a DIFF PREIMAGE f s))``, 2720 RW_TAC std_ss [SIGMA_ALGEBRA, IN_FUNSET, subsets_def, space_def, GSPECIFICATION, 2721 PREIMAGE_DIFF, IN_IMAGE] 2722 >> MATCH_MP_TAC SUBSET_ANTISYM 2723 >> RW_TAC std_ss [SUBSET_DEF, IN_DIFF, IN_PREIMAGE] 2724 >> Q.PAT_X_ASSUM `!s. s IN subsets b ==> PREIMAGE f s IN subsets a` 2725 (MP_TAC o Q.SPEC `space b DIFF s`) 2726 >> Know `x IN PREIMAGE f (space b DIFF s)` 2727 >- RW_TAC std_ss [IN_PREIMAGE, IN_DIFF] 2728 >> PROVE_TAC [subset_class_def, SUBSET_DEF]); 2729 2730val MEASURABLE_BIGUNION_PROPERTY = store_thm 2731 ("MEASURABLE_BIGUNION_PROPERTY", 2732 ``!a b f. sigma_algebra a /\ sigma_algebra b /\ 2733 f IN (space a -> space b) /\ 2734 (!s. s IN subsets b ==> PREIMAGE f s IN subsets a) ==> 2735 (!c. c SUBSET subsets b ==> 2736 (PREIMAGE f (BIGUNION c) = BIGUNION (IMAGE (PREIMAGE f) c)))``, 2737 RW_TAC std_ss [SIGMA_ALGEBRA, IN_FUNSET, subsets_def, space_def, GSPECIFICATION, 2738 PREIMAGE_BIGUNION, IN_IMAGE]); 2739 2740val MEASUBABLE_BIGUNION_LEMMA = store_thm 2741 ("MEASUBABLE_BIGUNION_LEMMA", 2742 ``!a b f. sigma_algebra a /\ sigma_algebra b /\ 2743 f IN (space a -> space b) /\ 2744 (!s. s IN subsets b ==> PREIMAGE f s IN subsets a) ==> 2745 (!c. countable c /\ c SUBSET (IMAGE (PREIMAGE f) (subsets b)) ==> 2746 BIGUNION c IN IMAGE (PREIMAGE f) (subsets b))``, 2747 RW_TAC std_ss [SIGMA_ALGEBRA, IN_FUNSET, IN_IMAGE] 2748 >> Q.EXISTS_TAC `BIGUNION (IMAGE (\x. @x'. x' IN subsets b /\ (PREIMAGE f x' = x)) c)` 2749 >> reverse CONJ_TAC 2750 >- (Q.PAT_X_ASSUM `!c. countable c /\ c SUBSET subsets b ==> BIGUNION c IN subsets b` 2751 MATCH_MP_TAC 2752 >> RW_TAC std_ss [image_countable, SUBSET_DEF, IN_IMAGE] 2753 >> Suff `(\x''. x'' IN subsets b) (@x''. x'' IN subsets b /\ (PREIMAGE f x'' = x'))` 2754 >- RW_TAC std_ss [] 2755 >> MATCH_MP_TAC SELECT_ELIM_THM 2756 >> FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_IMAGE] 2757 >> PROVE_TAC []) 2758 >> RW_TAC std_ss [PREIMAGE_BIGUNION, IMAGE_IMAGE] 2759 >> RW_TAC std_ss [Once EXTENSION, IN_BIGUNION, IN_IMAGE] 2760 >> FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_IMAGE] 2761 >> EQ_TAC 2762 >- (RW_TAC std_ss [] >> Q.EXISTS_TAC `s` >> ASM_REWRITE_TAC [] 2763 >> Q.PAT_X_ASSUM `!x. x IN c ==> ?x'. (x = PREIMAGE f x') /\ x' IN subsets b` 2764 (MP_TAC o Q.SPEC `s`) 2765 >> RW_TAC std_ss [] 2766 >> Q.EXISTS_TAC `PREIMAGE f x'` >> ASM_REWRITE_TAC [] 2767 >> Suff `(\x''. PREIMAGE f x' = PREIMAGE f x'') 2768 (@x''. x'' IN subsets b /\ (PREIMAGE f x'' = PREIMAGE f x'))` 2769 >- METIS_TAC [] 2770 >> MATCH_MP_TAC SELECT_ELIM_THM 2771 >> PROVE_TAC []) 2772 >> RW_TAC std_ss [] 2773 >> Q.EXISTS_TAC `x'` 2774 >> ASM_REWRITE_TAC [] 2775 >> Know `(\x''. x IN PREIMAGE f x'' ==> x IN x') 2776 (@x''. x'' IN subsets b /\ (PREIMAGE f x'' = x'))` 2777 >- (MATCH_MP_TAC SELECT_ELIM_THM 2778 >> RW_TAC std_ss [] 2779 >> PROVE_TAC []) 2780 >> RW_TAC std_ss []); 2781 2782val MEASURABLE_SIGMA_PREIMAGES = store_thm 2783 ("MEASURABLE_SIGMA_PREIMAGES", 2784 ``!a b f. sigma_algebra a /\ sigma_algebra b /\ 2785 f IN (space a -> space b) /\ 2786 (!s. s IN subsets b ==> PREIMAGE f s IN subsets a) ==> 2787 sigma_algebra (space a, IMAGE (PREIMAGE f) (subsets b))``, 2788 RW_TAC std_ss [SIGMA_ALGEBRA, IN_FUNSET, subsets_def, space_def] 2789 >| [FULL_SIMP_TAC std_ss [subset_class_def, GSPECIFICATION, IN_IMAGE] 2790 >> PROVE_TAC [], 2791 RW_TAC std_ss [IN_IMAGE] 2792 >> Q.EXISTS_TAC `{}` 2793 >> RW_TAC std_ss [PREIMAGE_EMPTY], 2794 RW_TAC std_ss [IN_IMAGE, PREIMAGE_DIFF] 2795 >> FULL_SIMP_TAC std_ss [IN_IMAGE] 2796 >> Q.EXISTS_TAC `space b DIFF x` 2797 >> RW_TAC std_ss [PREIMAGE_DIFF] 2798 >> MATCH_MP_TAC SUBSET_ANTISYM 2799 >> RW_TAC std_ss [SUBSET_DEF, IN_DIFF, IN_PREIMAGE] 2800 >> Q.PAT_X_ASSUM `!s. s IN subsets b ==> PREIMAGE f s IN subsets a` 2801 (MP_TAC o Q.SPEC `space b DIFF x`) 2802 >> Know `x' IN PREIMAGE f (space b DIFF x)` 2803 >- RW_TAC std_ss [IN_PREIMAGE, IN_DIFF] 2804 >> PROVE_TAC [subset_class_def, SUBSET_DEF], 2805 (MP_TAC o REWRITE_RULE [IN_FUNSET, SIGMA_ALGEBRA] o Q.SPECL [`a`, `b`, `f`]) 2806 MEASUBABLE_BIGUNION_LEMMA 2807 >> RW_TAC std_ss []]); 2808 2809val MEASURABLE_SIGMA = store_thm 2810 ("MEASURABLE_SIGMA", 2811 ``!f a b sp. 2812 sigma_algebra a /\ 2813 subset_class sp b /\ 2814 f IN (space a -> sp) /\ 2815 (!s. s IN b ==> ((PREIMAGE f s)INTER(space a)) IN subsets a) 2816 ==> 2817 f IN measurable a (sigma sp b)``, 2818 RW_TAC std_ss [] 2819 >> REWRITE_TAC [IN_MEASURABLE] 2820 >> CONJ_TAC >- FULL_SIMP_TAC std_ss [sigma_def, space_def] 2821 >> RW_TAC std_ss [SIGMA_ALGEBRA_SIGMA, SPACE_SIGMA, subsets_def, GSPECIFICATION] 2822 >> Know `subsets (sigma sp b) SUBSET {x' | ((PREIMAGE f x')INTER(space a)) IN subsets a /\ 2823 x' SUBSET sp}` 2824 >- (MATCH_MP_TAC SIGMA_PROPERTY 2825 >> RW_TAC std_ss [subset_class_def, GSPECIFICATION, IN_INTER, EMPTY_SUBSET, 2826 PREIMAGE_EMPTY, PREIMAGE_DIFF, SUBSET_INTER, SIGMA_ALGEBRA, 2827 DIFF_SUBSET, SUBSET_DEF, NOT_IN_EMPTY, IN_DIFF, 2828 PREIMAGE_BIGUNION, IN_BIGUNION] 2829 >| [FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA, INTER_EMPTY], 2830 PROVE_TAC [subset_class_def, SUBSET_DEF], 2831 Know `(PREIMAGE f sp DIFF PREIMAGE f s') INTER space a = 2832 (PREIMAGE f sp INTER space a) DIFF (PREIMAGE f s' INTER space a)` 2833 >- (RW_TAC std_ss [Once EXTENSION, IN_DIFF, IN_INTER, IN_PREIMAGE] >> DECIDE_TAC) 2834 >> RW_TAC std_ss [] 2835 >> Know `PREIMAGE f sp INTER space a = space a` 2836 >- (RW_TAC std_ss [Once EXTENSION, IN_INTER, IN_PREIMAGE] >> METIS_TAC [IN_FUNSET]) 2837 >> FULL_SIMP_TAC std_ss [sigma_algebra_def, ALGEBRA_COMPL], 2838 FULL_SIMP_TAC std_ss [sigma_algebra_def] 2839 >> `BIGUNION (IMAGE (PREIMAGE f) c) INTER space a = 2840 BIGUNION (IMAGE (\x. (PREIMAGE f x) INTER (space a)) c)` 2841 by (RW_TAC std_ss [Once EXTENSION, IN_BIGUNION, IN_INTER, IN_IMAGE] 2842 >> FULL_SIMP_TAC std_ss [IN_FUNSET] 2843 >> EQ_TAC 2844 >- (RW_TAC std_ss [] 2845 >> Q.EXISTS_TAC `PREIMAGE f x' INTER space a` 2846 >> ASM_REWRITE_TAC [IN_INTER] 2847 >> Q.EXISTS_TAC `x'` >> RW_TAC std_ss []) 2848 >> RW_TAC std_ss [] >> METIS_TAC [IN_INTER, IN_PREIMAGE]) 2849 >> RW_TAC std_ss [] 2850 >> Q.PAT_X_ASSUM `!c. countable c /\ c SUBSET subsets a ==> 2851 BIGUNION c IN subsets a` MATCH_MP_TAC 2852 >> RW_TAC std_ss [image_countable, SUBSET_DEF, IN_IMAGE] 2853 >> PROVE_TAC [], 2854 PROVE_TAC []]) 2855 >> RW_TAC std_ss [SUBSET_DEF, GSPECIFICATION]); 2856 2857val MEASURABLE_SUBSET = store_thm 2858 ("MEASURABLE_SUBSET", 2859 ``!a b. measurable a b SUBSET measurable a (sigma (space b) (subsets b))``, 2860 RW_TAC std_ss [SUBSET_DEF] 2861 >> MATCH_MP_TAC MEASURABLE_SIGMA 2862 >> FULL_SIMP_TAC std_ss [IN_MEASURABLE, SIGMA_ALGEBRA, space_def, subsets_def]); 2863 2864val MEASURABLE_LIFT = store_thm 2865 ("MEASURABLE_LIFT", 2866 ``!f a b. 2867 f IN measurable a b ==> f IN measurable a (sigma (space b) (subsets b))``, 2868 PROVE_TAC [MEASURABLE_SUBSET, SUBSET_DEF]); 2869 2870val MEASURABLE_I = store_thm 2871 ("MEASURABLE_I", 2872 ``!a. sigma_algebra a ==> I IN measurable a a``, 2873 RW_TAC std_ss [IN_MEASURABLE, I_THM, PREIMAGE_I, IN_FUNSET, GSPEC_ID, SPACE, SUBSET_REFL] 2874 >> Know `s INTER space a = s` 2875 >- (FULL_SIMP_TAC std_ss [Once EXTENSION, sigma_algebra_def, algebra_def, IN_INTER, 2876 subset_class_def, SUBSET_DEF] 2877 >> METIS_TAC []) 2878 >> RW_TAC std_ss []); 2879 2880(* Theorem 7.4 [7, p.54] *) 2881val MEASURABLE_COMP = store_thm 2882 ("MEASURABLE_COMP", 2883 ``!f g a b c. 2884 f IN measurable a b /\ g IN measurable b c ==> 2885 (g o f) IN measurable a c``, 2886 RW_TAC std_ss [IN_MEASURABLE, GSYM PREIMAGE_COMP, IN_FUNSET, SIGMA_ALGEBRA, space_def, 2887 subsets_def, GSPECIFICATION] 2888 >> `PREIMAGE f (PREIMAGE g s) INTER space a = 2889 PREIMAGE f (PREIMAGE g s INTER space b) INTER space a` 2890 by (RW_TAC std_ss [Once EXTENSION, IN_INTER, IN_PREIMAGE] >> METIS_TAC []) 2891 >> METIS_TAC []); 2892 2893val MEASURABLE_COMP_STRONG = store_thm 2894 ("MEASURABLE_COMP_STRONG", 2895 ``!f g a b c. 2896 f IN measurable a b /\ 2897 sigma_algebra c /\ 2898 g IN (space b -> space c) /\ 2899 (!x. x IN (subsets c) ==> PREIMAGE g x INTER (IMAGE f (space a)) IN subsets b) ==> 2900 (g o f) IN measurable a c``, 2901 RW_TAC bool_ss [IN_MEASURABLE] 2902 >| [FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA, IN_FUNSET] >> PROVE_TAC [], 2903 RW_TAC std_ss [PREIMAGE_ALT] 2904 >> ONCE_REWRITE_TAC [o_ASSOC] 2905 >> ONCE_REWRITE_TAC [GSYM PREIMAGE_ALT] 2906 >> Know `PREIMAGE f (s o g) INTER space a = 2907 PREIMAGE f (s o g INTER (IMAGE f (space a))) INTER space a` 2908 >- (RW_TAC std_ss [GSYM PREIMAGE_ALT] 2909 >> RW_TAC std_ss [Once EXTENSION, IN_PREIMAGE, IN_INTER, IN_IMAGE] 2910 >> EQ_TAC 2911 >> RW_TAC std_ss [] 2912 >> FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_PREIMAGE] 2913 >> Q.EXISTS_TAC `x` 2914 >> Know `g (f x) IN space c` 2915 >- (FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA, subset_class_def, SUBSET_DEF] >> PROVE_TAC []) 2916 >> PROVE_TAC []) 2917 >> STRIP_TAC >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 2918 >> FULL_SIMP_TAC std_ss [PREIMAGE_ALT]]); 2919 2920val MEASURABLE_COMP_STRONGER = store_thm 2921 ("MEASURABLE_COMP_STRONGER", 2922 ``!f g a b c t. 2923 f IN measurable a b /\ 2924 sigma_algebra c /\ 2925 g IN (space b -> space c) /\ 2926 (IMAGE f (space a)) SUBSET t /\ 2927 (!s. s IN subsets c ==> (PREIMAGE g s INTER t) IN subsets b) ==> 2928 (g o f) IN measurable a c``, 2929 RW_TAC bool_ss [IN_MEASURABLE] 2930 >| [FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA, IN_FUNSET] >> PROVE_TAC [], 2931 RW_TAC std_ss [PREIMAGE_ALT] 2932 >> ONCE_REWRITE_TAC [o_ASSOC] 2933 >> ONCE_REWRITE_TAC [GSYM PREIMAGE_ALT] 2934 >> Know `(PREIMAGE (f:'a->'b) (((s : 'c -> bool) o (g :'b -> 'c)) INTER 2935 (t :'b -> bool)) INTER space a = PREIMAGE f (s o g) INTER space a)` 2936 >- (RW_TAC std_ss [GSYM PREIMAGE_ALT] 2937 >> RW_TAC std_ss [Once EXTENSION, IN_PREIMAGE, IN_INTER, IN_IMAGE] 2938 >> EQ_TAC 2939 >> RW_TAC std_ss [] 2940 >> Know `g (f x) IN space c` 2941 >- (FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA, subset_class_def, SUBSET_DEF] >> PROVE_TAC []) 2942 >> STRIP_TAC 2943 >> Know `(f x) IN space b` 2944 >- FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_PREIMAGE, IN_FUNSET] 2945 >> STRIP_TAC 2946 >> Know `x IN space a` 2947 >- FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_PREIMAGE] 2948 >> STRIP_TAC 2949 >> FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_IMAGE] 2950 >> Q.PAT_X_ASSUM `!x. (?x'. (x = f x') /\ x' IN space a) ==> x IN t` MATCH_MP_TAC 2951 >> Q.EXISTS_TAC `x` 2952 >> ASM_REWRITE_TAC []) 2953 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap o GSYM) 2954 >> RW_TAC std_ss [PREIMAGE_ALT] 2955 >> RW_TAC std_ss [GSYM PREIMAGE_ALT, GSYM PREIMAGE_COMP]]); 2956 2957val MEASURABLE_UP_LIFT = store_thm 2958 ("MEASURABLE_UP_LIFT", 2959 ``!sp a b c f. f IN measurable (sp, a) c /\ 2960 sigma_algebra (sp, b) /\ a SUBSET b ==> f IN measurable (sp,b) c``, 2961 RW_TAC std_ss [IN_MEASURABLE, GSPECIFICATION, SUBSET_DEF, IN_FUNSET, space_def, subsets_def]); 2962 2963val MEASURABLE_UP_SUBSET = store_thm 2964 ("MEASURABLE_UP_SUBSET", 2965 ``!sp a b c. a SUBSET b /\ sigma_algebra (sp, b) 2966 ==> measurable (sp, a) c SUBSET measurable (sp, b) c``, 2967 RW_TAC std_ss [MEASURABLE_UP_LIFT, SUBSET_DEF] 2968 >> MATCH_MP_TAC MEASURABLE_UP_LIFT 2969 >> Q.EXISTS_TAC `a` 2970 >> ASM_REWRITE_TAC [SUBSET_DEF]); 2971 2972val MEASURABLE_UP_SIGMA = store_thm 2973 ("MEASURABLE_UP_SIGMA", 2974 ``!a b. measurable a b SUBSET measurable (sigma (space a) (subsets a)) b``, 2975 RW_TAC std_ss [SUBSET_DEF, IN_MEASURABLE, space_def, subsets_def, SPACE_SIGMA] 2976 >- (MATCH_MP_TAC SIGMA_ALGEBRA_SIGMA >> FULL_SIMP_TAC std_ss [SIGMA_ALGEBRA]) 2977 >> PROVE_TAC [SIGMA_SUBSET_SUBSETS, SUBSET_DEF]); 2978 2979(* NOTE: see martingaleTheory for more theorems on ���prod_sets��� *) 2980Theorem MEASURABLE_PROD_SIGMA : 2981 !a a1 a2 f. 2982 sigma_algebra a /\ 2983 (FST o f) IN measurable a a1 /\ 2984 (SND o f) IN measurable a a2 ==> 2985 f IN measurable a (sigma ((space a1) CROSS (space a2)) 2986 (prod_sets (subsets a1) (subsets a2))) 2987Proof 2988 rpt STRIP_TAC 2989 >> MATCH_MP_TAC MEASURABLE_SIGMA 2990 >> FULL_SIMP_TAC std_ss [IN_MEASURABLE] 2991 >> CONJ_TAC 2992 >- (RW_TAC std_ss [subset_class_def, subsets_def, space_def, IN_PROD_SETS] \\ 2993 PROVE_TAC [SIGMA_ALGEBRA, CROSS_SUBSET, SUBSET_DEF, subset_class_def, 2994 subsets_def, space_def]) 2995 >> CONJ_TAC 2996 >- (RW_TAC std_ss [IN_FUNSET, SPACE_SIGMA, IN_CROSS] \\ 2997 FULL_SIMP_TAC std_ss [IN_FUNSET, o_DEF]) 2998 >> RW_TAC std_ss [IN_PROD_SETS] 2999 >> RW_TAC std_ss [PREIMAGE_CROSS] 3000 >> `PREIMAGE (FST o f) t INTER PREIMAGE (SND o f) u INTER space a = 3001 (PREIMAGE (FST o f) t INTER space a) INTER 3002 (PREIMAGE (SND o f) u INTER space a)` 3003 by (RW_TAC std_ss [Once EXTENSION, IN_INTER] >> DECIDE_TAC) 3004 >> PROVE_TAC [sigma_algebra_def, ALGEBRA_INTER] 3005QED 3006 3007(* ------------------------------------------------------------------------- *) 3008(* sigma-algebra of functions [7, p.55] *) 3009(* ------------------------------------------------------------------------- *) 3010 3011(* The smallest sigma-algebra on `sp` that makes `f` measurable *) 3012val sigma_function_def = Define 3013 `sigma_function sp A f = (sp,IMAGE (\s. PREIMAGE f s INTER sp) (subsets A))`; 3014 3015val _ = overload_on ("sigma", ``sigma_function``); 3016 3017val SIGMA_MEASURABLE = store_thm 3018 ("SIGMA_MEASURABLE", 3019 ``!sp A f. sigma_algebra A /\ f IN (sp -> space A) ==> f IN measurable (sigma sp A f) A``, 3020 RW_TAC std_ss [sigma_function_def, space_def, subsets_def, 3021 IN_FUNSET, IN_MEASURABLE, IN_IMAGE] 3022 >- (MATCH_MP_TAC PREIMAGE_SIGMA_ALGEBRA >> art [IN_FUNSET]) 3023 >> Q.EXISTS_TAC `s` >> art []); 3024 3025(* Definition 7.5 of [1, p.51], The smallest sigma-algebra on `sp` that makes all `f` 3026 simultaneously measurable. *) 3027val sigma_functions_def = Define 3028 `sigma_functions sp A f J = 3029 sigma sp (BIGUNION (IMAGE (\i. IMAGE (\s. PREIMAGE (f i) s INTER sp) (subsets (A i))) J))`; 3030 3031val _ = overload_on ("sigma", ``sigma_functions``); 3032 3033(* Lemma 7.5 of [1, p.51] *) 3034val SIGMA_SIMULTANEOUSLY_MEASURABLE = store_thm 3035 ("SIGMA_SIMULTANEOUSLY_MEASURABLE", 3036 ``!sp A f J. (!i. i IN J ==> sigma_algebra (A i)) /\ 3037 (!i. f i IN (sp -> space (A i))) ==> 3038 !i. i IN J ==> f i IN measurable (sigma sp A f J) (A i)``, 3039 RW_TAC std_ss [IN_FUNSET, SPACE_SIGMA, sigma_functions_def, IN_MEASURABLE] 3040 >- (MATCH_MP_TAC SIGMA_ALGEBRA_SIGMA \\ 3041 RW_TAC std_ss [subset_class_def, IN_BIGUNION_IMAGE, IN_IMAGE, IN_PREIMAGE, IN_INTER] \\ 3042 REWRITE_TAC [INTER_SUBSET]) 3043 >> Know `PREIMAGE (f i) s INTER sp IN 3044 (BIGUNION (IMAGE (\i. IMAGE (\s. PREIMAGE (f i) s INTER sp) (subsets (A i))) J))` 3045 >- (RW_TAC std_ss [IN_BIGUNION_IMAGE, IN_IMAGE] \\ 3046 Q.EXISTS_TAC `i` >> art [] \\ 3047 Q.EXISTS_TAC `s` >> art []) >> DISCH_TAC 3048 >> ASSUME_TAC 3049 (Q.SPECL [`sp`, `BIGUNION (IMAGE (\i. IMAGE (\s. PREIMAGE (f i) s INTER sp) 3050 (subsets (A i))) J)`] SIGMA_SUBSET_SUBSETS) 3051 >> PROVE_TAC [SUBSET_DEF]); 3052 3053val _ = export_theory (); 3054 3055(* References: 3056 3057 [1] Hurd, J.: Formal verification of probabilistic algorithms. University of Cambridge (2001). 3058 [2] Coble, A.R.: Anonymity, information, and machine-assisted proof. University of Cambridge (2010). 3059 [3] Mhamdi, T., Hasan, O., Tahar, S.: Formalization of Measure Theory and Lebesgue Integration 3060 for Probabilistic Analysis in HOL. ACM Trans. Embedded Comput. Syst. 12, 1--23 (2013). 3061 [4] Wikipedia: https://en.wikipedia.org/wiki/Ring_of_sets 3062 [5] Wikipedia: https://en.wikipedia.org/wiki/Eugene_Dynkin 3063 [6] Wikipedia: https://en.wikipedia.org/wiki/Dynkin_system 3064 [7] Schilling, R.L.: Measures, Integrals and Martingales (Second Edition). 3065 Cambridge University Press (2017). 3066 *) 3067