1(* ------------------------------------------------------------------------- *) 2(* Useful Theorems, some are taken from various theories by Hurd and Coble *) 3(* Authors: Tarek Mhamdi, Osman Hasan, Sofiene Tahar *) 4(* HVG Group, Concordia University, Montreal *) 5(* *) 6(* Extended by Chun Tian (2019-2020) *) 7(* Fondazione Bruno Kessler and University of Trento, Italy *) 8(* ------------------------------------------------------------------------- *) 9 10open HolKernel Parse boolLib bossLib; 11 12open metisLib pairTheory combinTheory pred_setTheory pred_setLib jrhUtils 13 arithmeticTheory realTheory realLib transcTheory seqTheory numLib 14 real_sigmaTheory numpairTheory hurdUtils RealArith fcpTheory fcpLib; 15 16val _ = new_theory "util_prob"; 17 18fun METIS ths tm = prove(tm, METIS_TAC ths); 19 20(* ------------------------------------------------------------------------- *) 21 22val _ = set_fixity "->" (Infixr 250); 23val _ = overload_on ("->", 24 ``FUNSET :'a set -> 'b set -> ('a -> 'b) set``); 25 26val _ = overload_on ("-->", (* "Pi" in Isabelle's FuncSet.thy *) 27 ``DFUNSET :'a set -> ('a -> 'b set) -> ('a -> 'b) set``); 28 29(* RIGHTWARDS ARROW *) 30val _ = Unicode.unicode_version {u = UTF8.chr 0x2192, tmnm = "->"}; 31 32(* LONG RIGHTWARDS ARROW *) 33val _ = Unicode.unicode_version {u = UTF8.chr 0x27F6, tmnm = "-->"}; 34 35val _ = TeX_notation {hol = "->", TeX = ("\\HOLTokenMap{}", 1)}; 36val _ = TeX_notation {hol = UTF8.chr 0x2192, TeX = ("\\HOLTokenMap{}", 1)}; 37val _ = TeX_notation {hol = "-->", TeX = ("\\HOLTokenLongmap{}", 1)}; 38val _ = TeX_notation {hol = UTF8.chr 0x27F6, TeX = ("\\HOLTokenLongmap{}", 1)}; 39 40Theorem PAIRED_BETA_THM : 41 !f z. UNCURRY f z = f (FST z) (SND z) 42Proof 43 STRIP_TAC >> Cases >> RW_TAC std_ss [] 44QED 45 46Theorem IN_o : 47 !x f s. x IN (s o f) <=> f x IN s 48Proof 49 RW_TAC std_ss [SPECIFICATION, o_THM] 50QED 51 52val prod_sets_def = Define ` 53 prod_sets a b = {s CROSS t | s IN a /\ t IN b}`; 54 55Theorem IN_PROD_SETS[simp] : 56 !s a b. s IN prod_sets a b <=> ?t u. (s = t CROSS u) /\ t IN a /\ u IN b 57Proof 58 RW_TAC std_ss [prod_sets_def, GSPECIFICATION, UNCURRY] 59 >> EQ_TAC >- PROVE_TAC [] 60 >> RW_TAC std_ss [] 61 >> Q.EXISTS_TAC `(t,u)` 62 >> RW_TAC std_ss [] 63QED 64 65(* ���FCP_CONCAT s t��� is in place of ���(a,b)��� (pair), thus ���fcp_pair a b��� is ���a CROSS b��� *) 66val fcp_cross_def = Define (* cf. CROSS_DEF *) 67 ���fcp_cross A B = {FCP_CONCAT a b | a IN A /\ b IN B}���; 68 69Theorem IN_FCP_CROSS : (* cf. IN_CROSS *) 70 !s a b. s IN fcp_cross a b <=> ?t u. (s = FCP_CONCAT t u) /\ t IN a /\ u IN b 71Proof 72 RW_TAC std_ss [fcp_cross_def, GSPECIFICATION, UNCURRY] 73 >> EQ_TAC >- PROVE_TAC [] 74 >> RW_TAC std_ss [] 75 >> Q.EXISTS_TAC `(t,u)` 76 >> RW_TAC std_ss [] 77QED 78 79(* high dimensional space are made by lower dimensional spaces *) 80Theorem fcp_cross_UNIV : 81 FINITE univ(:'b) /\ FINITE univ(:'c) ==> 82 fcp_cross univ(:'a['b]) univ(:'a['c]) = univ(:'a['b + 'c]) 83Proof 84 rw [Once EXTENSION, IN_UNIV, GSPECIFICATION, IN_FCP_CROSS] 85 >> Q.EXISTS_TAC ���FCP i. x ' (i + dimindex(:'c))��� 86 >> Q.EXISTS_TAC ���FCP i. x ' i��� 87 >> rw [FCP_CONCAT_def, CART_EQ, index_sum, FCP_BETA] 88QED 89 90val fcp_prod_def = Define (* cf. prod_sets_def *) 91 ���fcp_prod a b = {fcp_cross s t | s IN a /\ t IN b}���; 92 93Theorem IN_FCP_PROD : 94 !s A B. s IN fcp_prod A B <=> ?a b. (s = fcp_cross a b) /\ a IN A /\ b IN B 95Proof 96 RW_TAC std_ss [fcp_prod_def, GSPECIFICATION, UNCURRY] 97 >> EQ_TAC >- PROVE_TAC [] 98 >> RW_TAC std_ss [] 99 >> Q.EXISTS_TAC `(a,b)` 100 >> RW_TAC std_ss [] 101QED 102 103Theorem FCP_BIGUNION_CROSS : 104 !f s t. fcp_cross (BIGUNION (IMAGE f s)) t = BIGUNION (IMAGE (\n. fcp_cross (f n) t) s) 105Proof 106 rw [Once EXTENSION, IN_BIGUNION_IMAGE, IN_FCP_CROSS] 107 >> EQ_TAC >> rpt STRIP_TAC 108 >- (rename1 ���z IN s��� >> Q.EXISTS_TAC ���z��� >> art [] \\ 109 rename1 ���x = FCP_CONCAT c u��� \\ 110 qexistsl_tac [���c���,���u���] >> art []) 111 >> rename1 ���x = FCP_CONCAT c u��� 112 >> qexistsl_tac [���c���,���u���] >> art [] 113 >> Q.EXISTS_TAC ���n��� >> art [] 114QED 115 116Theorem FCP_CROSS_BIGUNION : 117 !f s t. fcp_cross t (BIGUNION (IMAGE f s)) = BIGUNION (IMAGE (\n. fcp_cross t (f n)) s) 118Proof 119 rw [Once EXTENSION, IN_BIGUNION_IMAGE, IN_FCP_CROSS] 120 >> EQ_TAC >> rpt STRIP_TAC 121 >- (rename1 ���z IN s��� >> Q.EXISTS_TAC ���z��� >> art [] \\ 122 rename1 ���x = FCP_CONCAT c u��� \\ 123 qexistsl_tac [���c���,���u���] >> art []) 124 >> rename1 ���x = FCP_CONCAT c u��� 125 >> qexistsl_tac [���c���,���u���] >> art [] 126 >> Q.EXISTS_TAC ���n��� >> art [] 127QED 128 129Theorem FCP_CROSS_DIFF : 130 !(X :'a['b] set) s (t :'a['c] set). 131 FINITE univ(:'b) /\ FINITE univ(:'c) ==> 132 fcp_cross (X DIFF s) t = (fcp_cross X t) DIFF (fcp_cross s t) 133Proof 134 rw [Once EXTENSION, IN_FCP_CROSS, IN_DIFF] 135 >> EQ_TAC >> rpt STRIP_TAC (* 3 subgoals *) 136 >| [ (* goal 1 (of 3) *) 137 rename1 ���c IN X��� >> qexistsl_tac [���c���,���u���] >> art [], 138 (* goal 2 (of 3) *) 139 rename1 ���c IN X��� \\ 140 rename1 ���x <> FCP_CONCAT c' u' \/ c' NOTIN s \/ u' NOTIN t��� \\ 141 STRONG_DISJ_TAC >> DISJ1_TAC \\ 142 CCONTR_TAC >> fs [] \\ 143 Q.PAT_X_ASSUM ���x = FCP_CONCAT c' u'��� K_TAC \\ 144 Suff ���c = c'��� >- METIS_TAC [] \\ 145 PROVE_TAC [FCP_CONCAT_11], 146 (* goal 3 (of 3) *) 147 rename1 ���x = FCP_CONCAT c u��� \\ 148 qexistsl_tac [���c���,���u���] >> art [] >> PROVE_TAC [] ] 149QED 150 151Theorem FCP_CROSS_DIFF' : 152 !(s :'a['b] set) (X :'a['c] set) t. 153 FINITE univ(:'b) /\ FINITE univ(:'c) ==> 154 fcp_cross s (X DIFF t) = (fcp_cross s X) DIFF (fcp_cross s t) 155Proof 156 rw [Once EXTENSION, IN_FCP_CROSS, IN_DIFF] 157 >> EQ_TAC >> rpt STRIP_TAC (* 3 subgoals *) 158 >| [ (* goal 1 (of 3) *) 159 rename1 ���c IN s��� >> qexistsl_tac [���c���,���u���] >> art [], 160 (* goal 2 (of 3) *) 161 rename1 ���c IN s��� \\ 162 rename1 ���x <> FCP_CONCAT c' u' \/ c' NOTIN s \/ u' NOTIN t��� \\ 163 STRONG_DISJ_TAC >> DISJ2_TAC \\ 164 CCONTR_TAC >> fs [] \\ 165 Q.PAT_X_ASSUM ���x = FCP_CONCAT c' u'��� K_TAC \\ 166 Suff ���u = u'��� >- METIS_TAC [] \\ 167 PROVE_TAC [FCP_CONCAT_11], 168 (* goal 3 (of 3) *) 169 rename1 ���x = FCP_CONCAT c u��� \\ 170 qexistsl_tac [���c���,���u���] >> art [] >> PROVE_TAC [] ] 171QED 172 173Theorem FCP_SUBSET_CROSS : 174 !(a :'a['b] set) b (c :'a['c] set) d. 175 a SUBSET b /\ c SUBSET d ==> (fcp_cross a c) SUBSET (fcp_cross b d) 176Proof 177 rpt STRIP_TAC 178 >> rw [SUBSET_DEF, IN_FCP_CROSS] 179 >> qexistsl_tac [���t���, ���u���] >> art [] 180 >> PROVE_TAC [SUBSET_DEF] 181QED 182 183Theorem FCP_INTER_CROSS : 184 !(a :'a['b] set) (b :'a['c] set) c d. 185 FINITE univ(:'b) /\ FINITE univ(:'c) ==> 186 (fcp_cross a b) INTER (fcp_cross c d) = fcp_cross (a INTER c) (b INTER d) 187Proof 188 rw [Once EXTENSION, IN_INTER, IN_FCP_CROSS] 189 >> EQ_TAC >> rpt STRIP_TAC (* 3 subgoals *) 190 >| [ (* goal 1 (of 3) *) 191 fs [] >> qexistsl_tac [���t���, ���u���] >> art [] \\ 192 PROVE_TAC [FCP_CONCAT_11], 193 (* goal 2 (of 3) *) 194 qexistsl_tac [���t���, ���u���] >> art [], 195 (* goal 3 (of 3) *) 196 qexistsl_tac [���t���, ���u���] >> art [] ] 197QED 198 199(* see also LISP ... *) 200val pair_operation_def = Define 201 ���pair_operation (cons :'a -> 'b -> 'c) car cdr = 202 ((!a b. (car (cons a b) = a) /\ (cdr (cons a b) = b)) /\ 203 (!a b c d. (cons a b = cons c d) <=> (a = c) /\ (b = d)))���; 204 205(* two sample pair operations: comma (pairTheory) and FCP_CONCAT (fcpTheory) *) 206Theorem pair_operation_pair : 207 pair_operation (pair$, :'a -> 'b -> 'a # 'b) 208 (FST :'a # 'b -> 'a) (SND :'a # 'b -> 'b) 209Proof 210 rw [pair_operation_def] 211QED 212 213Theorem pair_operation_FCP_CONCAT : 214 FINITE univ(:'b) /\ FINITE univ(:'c) ==> 215 pair_operation (FCP_CONCAT :'a['b] -> 'a['c] -> 'a['b + 'c]) 216 (FCP_FST :'a['b + 'c] -> 'a['b]) 217 (FCP_SND :'a['b + 'c] -> 'a['c]) 218Proof 219 DISCH_TAC 220 >> ASM_SIMP_TAC std_ss [pair_operation_def] 221 >> reverse CONJ_TAC >- METIS_TAC [FCP_CONCAT_11] 222 >> rpt GEN_TAC 223 >> PROVE_TAC [FCP_CONCAT_THM] 224QED 225 226val general_cross_def = Define 227 ���general_cross (cons :'a -> 'b -> 'c) A B = {cons a b | a IN A /\ b IN B}���; 228 229Theorem IN_general_cross : 230 !cons s A B. s IN (general_cross cons A B) <=> 231 ?a b. s = cons a b /\ a IN A /\ b IN B 232Proof 233 RW_TAC std_ss [general_cross_def, GSPECIFICATION] 234 >> EQ_TAC >> rpt STRIP_TAC 235 >- (Cases_on ���x��� >> fs [] >> qexistsl_tac [���q���,���r���] >> art []) 236 >> Q.EXISTS_TAC ���(a,b)��� >> rw [] 237QED 238 239(* alternative definition of pred_set$CROSS *) 240Theorem CROSS_ALT : 241 !A B. A CROSS B = general_cross pair$, A B 242Proof 243 RW_TAC std_ss [Once EXTENSION, IN_CROSS, IN_general_cross] 244 >> EQ_TAC >> rw [] >> fs [] 245 >> qexistsl_tac [���FST x���,���SND x���] >> rw [PAIR] 246QED 247 248(* alternative definition of fcp_cross *) 249Theorem fcp_cross_alt : 250 !A B. fcp_cross A B = general_cross FCP_CONCAT A B 251Proof 252 RW_TAC std_ss [Once EXTENSION, IN_FCP_CROSS, IN_general_cross] 253QED 254 255val general_prod_def = Define 256 ���general_prod (cons :'a -> 'b -> 'c) A B = 257 {general_cross cons a b | a IN A /\ b IN B}���; 258 259Theorem IN_general_prod : 260 !(cons :'a -> 'b -> 'c) s A B. 261 s IN general_prod cons A B <=> ?a b. (s = general_cross cons a b) /\ a IN A /\ b IN B 262Proof 263 RW_TAC std_ss [general_prod_def, GSPECIFICATION, UNCURRY] 264 >> EQ_TAC >> rpt STRIP_TAC 265 >- (qexistsl_tac [���FST x���, ���SND x���] >> art []) 266 >> Q.EXISTS_TAC `(a,b)` 267 >> RW_TAC std_ss [] 268QED 269 270(* alternative definition of prod_sets *) 271Theorem prod_sets_alt : 272 !A B. prod_sets A B = general_prod pair$, A B 273Proof 274 RW_TAC std_ss [Once EXTENSION, IN_PROD_SETS, IN_general_prod, GSYM CROSS_ALT] 275QED 276 277(* alternative definition of fcp_prod *) 278Theorem fcp_prod_alt : 279 !A B. fcp_prod A B = general_prod FCP_CONCAT A B 280Proof 281 RW_TAC std_ss [Once EXTENSION, IN_FCP_PROD, IN_general_prod, GSYM fcp_cross_alt] 282QED 283 284Theorem general_BIGUNION_CROSS : 285 !(cons :'a -> 'b -> 'c) f (s :'index set) t. 286 (general_cross cons (BIGUNION (IMAGE f s)) t = 287 BIGUNION (IMAGE (\n. general_cross cons (f n) t) s)) 288Proof 289 rw [Once EXTENSION, IN_BIGUNION_IMAGE, IN_general_cross] 290 >> EQ_TAC >> rpt STRIP_TAC 291 >- (rename1 ���z IN s��� >> Q.EXISTS_TAC ���z��� >> art [] \\ 292 qexistsl_tac [���a���,���b���] >> art []) 293 >> qexistsl_tac [���a���,���b���] >> art [] 294 >> Q.EXISTS_TAC ���n��� >> art [] 295QED 296 297Theorem general_CROSS_BIGUNION : 298 !(cons :'a -> 'b -> 'c) f (s :'index set) t. 299 (general_cross cons t (BIGUNION (IMAGE f s)) = 300 BIGUNION (IMAGE (\n. general_cross cons t (f n)) s)) 301Proof 302 rw [Once EXTENSION, IN_BIGUNION_IMAGE, IN_general_cross] 303 >> EQ_TAC >> rpt STRIP_TAC 304 >- (rename1 ���z IN s��� >> Q.EXISTS_TAC ���z��� >> art [] \\ 305 qexistsl_tac [���a���,���b���] >> art []) 306 >> qexistsl_tac [���a���,���b���] >> art [] 307 >> Q.EXISTS_TAC ���n��� >> art [] 308QED 309 310Theorem general_CROSS_DIFF : 311 !(cons :'a -> 'b -> 'c) car cdr (X :'a set) s (t :'b set). 312 pair_operation cons car cdr ==> 313 (general_cross cons (X DIFF s) t = 314 (general_cross cons X t) DIFF (general_cross cons s t)) 315Proof 316 rw [Once EXTENSION, IN_general_cross, IN_DIFF] 317 >> EQ_TAC >> rpt STRIP_TAC (* 3 subgoals *) 318 >| [ (* goal 1 (of 3) *) 319 qexistsl_tac [���a���,���b���] >> art [], 320 (* goal 2 (of 3) *) 321 STRONG_DISJ_TAC >> DISJ1_TAC \\ 322 CCONTR_TAC >> fs [] \\ 323 Q.PAT_X_ASSUM ���x = cons a' b'��� K_TAC \\ 324 Suff ���a = a'��� >- METIS_TAC [] \\ 325 METIS_TAC [pair_operation_def], 326 (* goal 3 (of 3) *) 327 qexistsl_tac [���a���,���b���] >> art [] >> PROVE_TAC [] ] 328QED 329 330Theorem general_CROSS_DIFF' : 331 !(cons :'a -> 'b -> 'c) car cdr (s :'a set) (X :'b set) t. 332 pair_operation cons car cdr ==> 333 (general_cross cons s (X DIFF t) = 334 (general_cross cons s X) DIFF (general_cross cons s t)) 335Proof 336 rw [Once EXTENSION, IN_general_cross, IN_DIFF] 337 >> EQ_TAC >> rpt STRIP_TAC (* 3 subgoals *) 338 >| [ (* goal 1 (of 3) *) 339 qexistsl_tac [���a���,���b���] >> art [], 340 (* goal 2 (of 3) *) 341 STRONG_DISJ_TAC >> DISJ2_TAC \\ 342 CCONTR_TAC >> fs [] \\ 343 Q.PAT_X_ASSUM ���x = cons a' b'��� K_TAC \\ 344 Suff ���b = b'��� >- METIS_TAC [] \\ 345 METIS_TAC [pair_operation_def], 346 (* goal 3 (of 3) *) 347 qexistsl_tac [���a���,���b���] >> art [] >> PROVE_TAC [] ] 348QED 349 350Theorem general_SUBSET_CROSS : 351 !(cons :'a -> 'b -> 'c) (a :'a set) b (c :'b set) d. 352 a SUBSET b /\ c SUBSET d ==> 353 (general_cross cons a c) SUBSET (general_cross cons b d) 354Proof 355 rpt STRIP_TAC 356 >> rw [SUBSET_DEF, IN_general_cross] 357 >> qexistsl_tac [���a'���, ���b'���] >> art [] 358 >> PROVE_TAC [SUBSET_DEF] 359QED 360 361Theorem general_INTER_CROSS : 362 !(cons :'a -> 'b -> 'c) car cdr (a :'a set) (b :'b set) c d. 363 pair_operation cons car cdr ==> 364 ((general_cross cons a b) INTER (general_cross cons c d) = 365 general_cross cons (a INTER c) (b INTER d)) 366Proof 367 rw [Once EXTENSION, IN_INTER, IN_general_cross] 368 >> EQ_TAC >> rpt STRIP_TAC (* 3 subgoals *) 369 >| [ (* goal 1 (of 3) *) 370 fs [] >> rename1 ���x = cons s t��� \\ 371 qexistsl_tac [���s���, ���t���] >> art [] \\ 372 METIS_TAC [pair_operation_def], 373 (* goal 2 (of 3) *) 374 qexistsl_tac [���a'���, ���b'���] >> art [], 375 (* goal 3 (of 3) *) 376 qexistsl_tac [���a'���, ���b'���] >> art [] ] 377QED 378 379(* ------------------------------------------------------------------------- *) 380(* ----- Defining real-valued power, log, and log base 2 functions --------- *) 381(* ------------------------------------------------------------------------- *) 382 383val _ = set_fixity "powr" (Infixr 700); 384val _ = overload_on ("powr", ``$rpow``); (* transcTheory *) 385 386val logr_def = Define `logr a x = ln x / ln a`; 387val lg_def = Define `lg x = logr 2 x`; 388 389val lg_1 = store_thm 390 ("lg_1", ``lg 1 = 0``, 391 RW_TAC real_ss [lg_def, logr_def, LN_1]); 392 393val logr_1 = store_thm 394 ("logr_1", ``!b. logr b 1 = 0``, 395 RW_TAC real_ss [logr_def, LN_1]); 396 397val lg_nonzero = store_thm 398 ("lg_nonzero", ``!x. x <> 0 /\ 0 <= x ==> (lg x <> 0 <=> x <> 1)``, 399 RW_TAC std_ss [REAL_ARITH ``x <> 0 /\ 0 <= x <=> 0 < x``] 400 >> RW_TAC std_ss [GSYM lg_1] 401 >> RW_TAC std_ss [lg_def, logr_def, real_div, REAL_EQ_RMUL, REAL_INV_EQ_0] 402 >> (MP_TAC o Q.SPECL [`2`, `1`]) LN_INJ >> RW_TAC real_ss [LN_1] 403 >> RW_TAC std_ss [GSYM LN_1] 404 >> MATCH_MP_TAC LN_INJ 405 >> RW_TAC real_ss []); 406 407val lg_mul = store_thm 408 ("lg_mul", ``!x y. 0 < x /\ 0 < y ==> (lg (x * y) = lg x + lg y)``, 409 RW_TAC real_ss [lg_def, logr_def, LN_MUL]); 410 411val logr_mul = store_thm 412 ("logr_mul", ``!b x y. 0 < x /\ 0 < y ==> (logr b (x * y) = logr b x + logr b y)``, 413 RW_TAC real_ss [logr_def, LN_MUL]); 414 415val lg_2 = store_thm 416 ("lg_2", ``lg 2 = 1``, 417 RW_TAC real_ss [lg_def, logr_def] 418 >> MATCH_MP_TAC REAL_DIV_REFL 419 >> (ASSUME_TAC o Q.SPECL [`1`, `2`]) LN_MONO_LT 420 >> FULL_SIMP_TAC real_ss [LN_1] 421 >> ONCE_REWRITE_TAC [EQ_SYM_EQ] 422 >> MATCH_MP_TAC REAL_LT_IMP_NE 423 >> ASM_REWRITE_TAC []); 424 425val lg_inv = store_thm 426 ("lg_inv", ``!x. 0 < x ==> (lg (inv x) = ~lg x)``, 427 RW_TAC real_ss [lg_def, logr_def, LN_INV, real_div]); 428 429val logr_inv = store_thm 430 ("logr_inv", ``!b x. 0 < x ==> (logr b (inv x) = ~ logr b x)``, 431 RW_TAC real_ss [logr_def, LN_INV, real_div]); 432 433val logr_div = store_thm 434 ("logr_div", ``!b x y. 0 < x /\ 0 < y ==> (logr b (x/y) = logr b x - logr b y)``, 435 RW_TAC real_ss [real_div, logr_mul, logr_inv, GSYM real_sub]); 436 437val neg_lg = store_thm 438 ("neg_lg", ``!x. 0 < x ==> ((~(lg x)) = lg (inv x))``, 439 RW_TAC real_ss [lg_def, logr_def, real_div] 440 >> `~(ln x * inv (ln 2)) = (~ ln x) * inv (ln 2)` by REAL_ARITH_TAC 441 >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 442 >> RW_TAC real_ss [REAL_EQ_RMUL] 443 >> DISJ2_TAC >> ONCE_REWRITE_TAC [EQ_SYM_EQ] >> MATCH_MP_TAC LN_INV 444 >> RW_TAC std_ss []); 445 446val neg_logr = store_thm 447 ("neg_logr", ``!b x. 0 < x ==> ((~(logr b x)) = logr b (inv x))``, 448 RW_TAC real_ss [logr_def, real_div] 449 >> `~(ln x * inv (ln b)) = (~ ln x) * inv (ln b)` by REAL_ARITH_TAC 450 >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 451 >> RW_TAC real_ss [REAL_EQ_RMUL] 452 >> DISJ2_TAC >> ONCE_REWRITE_TAC [EQ_SYM_EQ] >> MATCH_MP_TAC LN_INV 453 >> RW_TAC std_ss []); 454 455val lg_pow = store_thm 456 ("lg_pow", ``!n. lg (2 pow n) = &n``, 457 RW_TAC real_ss [lg_def, logr_def, LN_POW] 458 >> `~(ln 2 = 0)` 459 by (ONCE_REWRITE_TAC [EQ_SYM_EQ] >> MATCH_MP_TAC REAL_LT_IMP_NE 460 >> MATCH_MP_TAC REAL_LET_TRANS >> Q.EXISTS_TAC `ln 1` 461 >> RW_TAC real_ss [LN_POS, LN_MONO_LT]) 462 >> RW_TAC real_ss [real_div, GSYM REAL_MUL_ASSOC, REAL_MUL_RINV]); 463 464(********************************************************************************************) 465 466val NUM_2D_BIJ = store_thm 467 ("NUM_2D_BIJ", 468 ``?f. 469 BIJ f ((UNIV : num -> bool) CROSS (UNIV : num -> bool)) 470 (UNIV : num -> bool)``, 471 MATCH_MP_TAC BIJ_INJ_SURJ 472 >> reverse CONJ_TAC 473 >- (Q.EXISTS_TAC `FST` 474 >> RW_TAC std_ss [SURJ_DEF, IN_UNIV, IN_CROSS] 475 >> Q.EXISTS_TAC `(x, 0)` 476 >> RW_TAC std_ss [FST]) 477 >> Q.EXISTS_TAC `UNCURRY ind_type$NUMPAIR` 478 >> RW_TAC std_ss [INJ_DEF, IN_UNIV, IN_CROSS] 479 >> Cases_on `x` 480 >> Cases_on `y` 481 >> POP_ASSUM MP_TAC 482 >> RW_TAC std_ss [UNCURRY_DEF, ind_typeTheory.NUMPAIR_INJ]); 483 484val NUM_2D_BIJ_INV = store_thm 485 ("NUM_2D_BIJ_INV", 486 ``?f. 487 BIJ f (UNIV : num -> bool) 488 ((UNIV : num -> bool) CROSS (UNIV : num -> bool))``, 489 PROVE_TAC [NUM_2D_BIJ, BIJ_SYM]); 490 491val NUM_2D_BIJ_NZ = store_thm 492 ("NUM_2D_BIJ_NZ", 493 ``?f. 494 BIJ f ((UNIV : num -> bool) CROSS ((UNIV : num -> bool) DIFF {0})) 495 (UNIV : num -> bool)``, 496 MATCH_MP_TAC BIJ_INJ_SURJ 497 >> reverse CONJ_TAC 498 >- (Q.EXISTS_TAC `FST` 499 >> RW_TAC std_ss [SURJ_DEF, IN_UNIV, IN_CROSS,DIFF_DEF,GSPECIFICATION,IN_UNIV,IN_SING] 500 >> Q.EXISTS_TAC `(x, 1)` 501 >> RW_TAC std_ss [FST]) 502 >> Q.EXISTS_TAC `UNCURRY ind_type$NUMPAIR` 503 >> RW_TAC std_ss [INJ_DEF, IN_UNIV, IN_CROSS] 504 >> Cases_on `x` 505 >> Cases_on `y` 506 >> POP_ASSUM MP_TAC 507 >> RW_TAC std_ss [UNCURRY_DEF, ind_typeTheory.NUMPAIR_INJ]); 508 509val NUM_2D_BIJ_NZ_INV = store_thm 510 ("NUM_2D_BIJ_NZ_INV", 511 ``?f. 512 BIJ f (UNIV : num -> bool) 513 ((UNIV : num -> bool) CROSS ((UNIV : num -> bool) DIFF {0}))``, 514 PROVE_TAC [NUM_2D_BIJ_NZ, BIJ_SYM]); 515 516val NUM_2D_BIJ_NZ_ALT = store_thm 517 ("NUM_2D_BIJ_NZ_ALT", 518 ``?f. 519 BIJ f ((UNIV : num -> bool) CROSS (UNIV : num -> bool)) 520 ((UNIV : num -> bool) DIFF {0})``, 521 MATCH_MP_TAC BIJ_INJ_SURJ 522 >> reverse CONJ_TAC 523 >- (Q.EXISTS_TAC `(\(x,y). x + 1:num)` 524 >> RW_TAC std_ss [SURJ_DEF, IN_UNIV, IN_CROSS] 525 >- (Cases_on `x` >> RW_TAC std_ss [DIFF_DEF,GSPECIFICATION,IN_UNIV,IN_SING]) 526 >> Q.EXISTS_TAC `(x-1,1)` 527 >> RW_TAC std_ss [] 528 >> MATCH_MP_TAC SUB_ADD 529 >> FULL_SIMP_TAC real_ss [DIFF_DEF,GSPECIFICATION,IN_UNIV,IN_SING]) 530 >> Q.EXISTS_TAC `UNCURRY ind_type$NUMPAIR` 531 >> RW_TAC std_ss [INJ_DEF, IN_UNIV, IN_CROSS] 532 >- ( Cases_on `x` 533 >> RW_TAC std_ss [UNCURRY_DEF, ind_typeTheory.NUMPAIR_INJ,DIFF_DEF, 534 GSPECIFICATION,IN_UNIV,IN_SING] 535 >> RW_TAC real_ss [ind_typeTheory.NUMPAIR]) 536 >> Cases_on `x` 537 >> Cases_on `y` 538 >> POP_ASSUM MP_TAC 539 >> RW_TAC std_ss [UNCURRY_DEF, ind_typeTheory.NUMPAIR_INJ]); 540 541val NUM_2D_BIJ_NZ_ALT_INV = store_thm 542 ("NUM_2D_BIJ_NZ_ALT_INV", 543 ``?f. 544 BIJ f ((UNIV : num -> bool) DIFF {0}) 545 ((UNIV : num -> bool) CROSS (UNIV : num -> bool))``, 546 PROVE_TAC [NUM_2D_BIJ_NZ_ALT, BIJ_SYM]); 547 548val NUM_2D_BIJ_NZ_ALT2 = store_thm 549 ("NUM_2D_BIJ_NZ_ALT2", 550 ``?f. 551 BIJ f (((UNIV : num -> bool) DIFF {0}) CROSS ((UNIV : num -> bool) DIFF {0})) 552 (UNIV : num -> bool)``, 553 MATCH_MP_TAC BIJ_INJ_SURJ 554 >> reverse CONJ_TAC 555 >- (Q.EXISTS_TAC `(\(x,y). x - 1:num)` 556 >> RW_TAC std_ss [SURJ_DEF, IN_UNIV, IN_CROSS] 557 >> Q.EXISTS_TAC `(x+1,1)` 558 >> RW_TAC std_ss [DIFF_DEF,GSPECIFICATION,IN_UNIV,IN_SING] 559 ) 560 >> Q.EXISTS_TAC `UNCURRY ind_type$NUMPAIR` 561 >> RW_TAC std_ss [INJ_DEF, IN_UNIV, IN_CROSS] 562 >> Cases_on `x` 563 >> Cases_on `y` 564 >> POP_ASSUM MP_TAC 565 >> RW_TAC std_ss [UNCURRY_DEF, ind_typeTheory.NUMPAIR_INJ]); 566 567val NUM_2D_BIJ_NZ_ALT2_INV = store_thm 568 ("NUM_2D_BIJ_NZ_ALT2_INV", 569 ``?f. 570 BIJ f (UNIV : num -> bool) 571 (((UNIV : num -> bool) DIFF {0}) CROSS ((UNIV : num -> bool) DIFF {0}))``, 572 PROVE_TAC [NUM_2D_BIJ_NZ_ALT2, BIJ_SYM]); 573 574(* Two concrete NUM_2D_BIJ lemmas using numpairTheory *) 575val NUM_2D_BIJ_nfst_nsnd = store_thm 576 ("NUM_2D_BIJ_nfst_nsnd", ``BIJ (\n. (nfst n, nsnd n)) UNIV (UNIV CROSS UNIV)``, 577 REWRITE_TAC [BIJ_ALT, IN_CROSS, IN_FUNSET, IN_UNIV] 578 >> BETA_TAC >> GEN_TAC >> Cases_on `y` 579 >> SIMP_TAC std_ss [EXISTS_UNIQUE_ALT] 580 >> Q.EXISTS_TAC `npair q r` 581 >> GEN_TAC >> STRIP_ASSUME_TAC (Q.SPEC `x'` npair_cases) 582 >> POP_ASSUM (REWRITE_TAC o wrap) 583 >> REWRITE_TAC [nfst_npair, nsnd_npair, npair_11]); 584 585val NUM_2D_BIJ_npair = store_thm 586 ("NUM_2D_BIJ_npair", ``BIJ (UNCURRY npair) (UNIV CROSS UNIV) UNIV``, 587 REWRITE_TAC [BIJ_ALT, IN_CROSS, IN_FUNSET, IN_UNIV, UNCURRY] 588 >> GEN_TAC >> SIMP_TAC std_ss [EXISTS_UNIQUE_ALT] 589 >> Q.EXISTS_TAC `nfst y, nsnd y` 590 >> GEN_TAC >> STRIP_ASSUME_TAC (Q.SPEC `y` npair_cases) 591 >> POP_ASSUM (REWRITE_TAC o wrap) 592 >> REWRITE_TAC [nfst_npair, nsnd_npair, npair_11] 593 >> Cases_on `x'` >> SIMP_TAC std_ss []); 594 595val finite_enumeration_of_sets_has_max_non_empty = store_thm 596 ("finite_enumeration_of_sets_has_max_non_empty", 597 ``!f s. FINITE s /\ (!x. f x IN s) /\ 598 (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) ==> 599 ?N. !n:num. n >= N ==> (f n = {})``, 600 `!s. FINITE s ==> 601 (\s. !f. (!x. f x IN {} INSERT s) /\ 602 (~({} IN s)) /\ 603 (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) ==> 604 ?N. !n:num. n >= N ==> (f n = {})) s` 605 by (MATCH_MP_TAC FINITE_INDUCT 606 >> RW_TAC std_ss [NOT_IN_EMPTY, IN_INSERT] 607 >> Q.PAT_X_ASSUM `!f. (!x. (f x = {}) \/ f x IN s) /\ ~({} IN s) /\ 608 (!m n. ~(m = n) ==> DISJOINT (f m) (f n)) ==> 609 ?N:num. !n. n >= N ==> (f n = {})` 610 (MP_TAC o Q.SPEC `(\x. if f x = e then {} else f x)`) 611 >> `(!x. ((\x. (if f x = e then {} else f x)) x = {}) \/ 612 (\x. (if f x = e then {} else f x)) x IN s) /\ ~({} IN s)` 613 by METIS_TAC [] 614 >> ASM_SIMP_TAC std_ss [] 615 >> `(!m n. ~(m = n) ==> DISJOINT (if f m = e then {} else f m) 616 (if f n = e then {} else f n))` 617 by (RW_TAC std_ss [IN_DISJOINT, NOT_IN_EMPTY] 618 >> METIS_TAC [IN_DISJOINT]) 619 >> ASM_SIMP_TAC std_ss [] 620 >> RW_TAC std_ss [] 621 >> Cases_on `?n. f n = e` 622 >- (FULL_SIMP_TAC std_ss [] 623 >> Cases_on `n < N` 624 >- (Q.EXISTS_TAC `N` 625 >> RW_TAC std_ss [GREATER_EQ] 626 >> `~(n' = n)` 627 by METIS_TAC [LESS_LESS_EQ_TRANS, 628 DECIDE ``!m (n:num). m < n ==> ~(m=n)``] 629 >> Cases_on `f n' = f n` 630 >- (`DISJOINT (f n') (f n)` by METIS_TAC [] 631 >> FULL_SIMP_TAC std_ss [IN_DISJOINT, EXTENSION, NOT_IN_EMPTY] 632 >> METIS_TAC []) 633 >> Q.PAT_X_ASSUM 634 `!n'. n' >= N ==> ((if f n' = f n then {} else f n') = {})` 635 (MP_TAC o Q.SPEC `n'`) 636 >> ASM_SIMP_TAC std_ss [GREATER_EQ]) 637 >> Q.EXISTS_TAC `SUC n` 638 >> RW_TAC std_ss [GREATER_EQ] 639 >> FULL_SIMP_TAC std_ss [NOT_LESS] 640 >> `~(n' = n)` 641 by METIS_TAC [LESS_LESS_EQ_TRANS, 642 DECIDE ``!n:num. n < SUC n``, 643 DECIDE ``!m (n:num). m < n ==> ~(m=n)``] 644 >> Cases_on `f n' = f n` 645 >- (`DISJOINT (f n') (f n)` by METIS_TAC [] 646 >> FULL_SIMP_TAC std_ss [IN_DISJOINT, EXTENSION, NOT_IN_EMPTY] 647 >> METIS_TAC []) 648 >> `N <= n'` by METIS_TAC [LESS_EQ_IMP_LESS_SUC, 649 LESS_LESS_EQ_TRANS, 650 LESS_IMP_LESS_OR_EQ] 651 >> Q.PAT_X_ASSUM 652 `!n'. n' >= N ==> ((if f n' = f n then {} else f n') = {})` 653 (MP_TAC o Q.SPEC `n'`) 654 >> ASM_SIMP_TAC std_ss [GREATER_EQ]) 655 >> METIS_TAC []) 656 >> REPEAT STRIP_TAC 657 >> Cases_on `{} IN s` 658 >- (Q.PAT_X_ASSUM `!s. FINITE s ==> P` (MP_TAC o Q.SPEC `s DELETE {}`) 659 >> RW_TAC std_ss [FINITE_DELETE, IN_INSERT, IN_DELETE]) 660 >> METIS_TAC [IN_INSERT]); 661 662val PREIMAGE_REAL_COMPL1 = store_thm 663 ("PREIMAGE_REAL_COMPL1", ``!c:real. COMPL {x | c < x} = {x | x <= c}``, 664 RW_TAC real_ss [COMPL_DEF,UNIV_DEF,DIFF_DEF,EXTENSION] 665 >> RW_TAC real_ss [GSPECIFICATION,GSYM real_lte,SPECIFICATION]); 666 667val PREIMAGE_REAL_COMPL2 = store_thm 668 ("PREIMAGE_REAL_COMPL2", ``!c:real. COMPL {x | c <= x} = {x | x < c}``, 669 RW_TAC real_ss [COMPL_DEF,UNIV_DEF,DIFF_DEF,EXTENSION] 670 >> RW_TAC real_ss [GSPECIFICATION,GSYM real_lt,SPECIFICATION]); 671 672val PREIMAGE_REAL_COMPL3 = store_thm 673 ("PREIMAGE_REAL_COMPL3", ``!c:real. COMPL {x | x <= c} = {x | c < x}``, 674 RW_TAC real_ss [COMPL_DEF,UNIV_DEF,DIFF_DEF,EXTENSION] 675 >> RW_TAC real_ss [GSPECIFICATION,GSYM real_lt,SPECIFICATION]); 676 677val PREIMAGE_REAL_COMPL4 = store_thm 678 ("PREIMAGE_REAL_COMPL4", ``!c:real. COMPL {x | x < c} = {x | c <= x}``, 679 RW_TAC real_ss [COMPL_DEF,UNIV_DEF,DIFF_DEF,EXTENSION] 680 >> RW_TAC real_ss [GSPECIFICATION,GSYM real_lte,SPECIFICATION]); 681 682val GBIGUNION_IMAGE = store_thm 683 ("GBIGUNION_IMAGE", 684 ``!s p n. {s | ?n. p s n} = BIGUNION (IMAGE (\n. {s | p s n}) UNIV)``, 685 RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_BIGUNION_IMAGE, IN_UNIV]); 686 687(* ********************************************* *) 688(* Useful Theorems on Real Numbers *) 689(* ********************************************* *) 690 691val POW_HALF_POS = store_thm 692 ("POW_HALF_POS", 693 ``!n. 0:real < (1/2) pow n``, 694 STRIP_TAC 695 >> Cases_on `n` >- PROVE_TAC [REAL_ARITH ``0:real < 1``, pow] 696 >> PROVE_TAC [HALF_POS, POW_POS_LT]); 697 698val POW_HALF_SMALL = store_thm 699 ("POW_HALF_SMALL", 700 ``!e:real. 0 < e ==> ?n. (1 / 2) pow n < e``, 701 RW_TAC std_ss [] 702 >> MP_TAC (Q.SPEC `1 / 2` SEQ_POWER) 703 >> RW_TAC std_ss [abs, HALF_LT_1, HALF_POS, REAL_LT_IMP_LE, SEQ] 704 >> POP_ASSUM (MP_TAC o Q.SPEC `e`) 705 >> RW_TAC std_ss [REAL_SUB_RZERO, POW_HALF_POS, REAL_LT_IMP_LE, 706 GREATER_EQ] 707 >> PROVE_TAC [LESS_EQ_REFL]); 708 709val POW_HALF_MONO = store_thm 710 ("POW_HALF_MONO", 711 ``!m n. m <= n ==> ((1:real)/2) pow n <= (1/2) pow m``, 712 REPEAT STRIP_TAC 713 >> Induct_on `n` >| 714 [STRIP_TAC 715 >> Know `m:num = 0` >- DECIDE_TAC 716 >> PROVE_TAC [REAL_ARITH ``a:real <= a``], 717 Cases_on `m = SUC n` >- PROVE_TAC [REAL_ARITH ``a:real <= a``] 718 >> ONCE_REWRITE_TAC [pow] 719 >> STRIP_TAC 720 >> Know `m:num <= n` >- DECIDE_TAC 721 >> STRIP_TAC 722 >> Suff `(2:real) * ((1/2) * (1/2) pow n) <= 2 * (1/2) pow m` 723 >- PROVE_TAC [REAL_ARITH ``0:real < 2``, REAL_LE_LMUL] 724 >> Suff `((1:real)/2) pow n <= 2 * (1/2) pow m` 725 >- (KILL_TAC 726 >> PROVE_TAC [GSYM REAL_MUL_ASSOC, HALF_CANCEL, REAL_MUL_LID]) 727 >> PROVE_TAC [REAL_ARITH ``!x y. 0:real < x /\ x <= y ==> x <= 2 * y``, 728 POW_HALF_POS]]); 729 730val REAL_LE_LT_MUL = store_thm 731 ("REAL_LE_LT_MUL", 732 ``!x y : real. 0 <= x /\ 0 < y ==> 0 <= x * y``, 733 rpt STRIP_TAC 734 >> MP_TAC (Q.SPECL [`0`, `x`, `y`] REAL_LE_RMUL) 735 >> RW_TAC std_ss [REAL_MUL_LZERO]); 736 737val REAL_LT_LE_MUL = store_thm 738 ("REAL_LT_LE_MUL", 739 ``!x y : real. 0 < x /\ 0 <= y ==> 0 <= x * y``, 740 PROVE_TAC [REAL_LE_LT_MUL, REAL_MUL_SYM]); 741 742val REAL_MUL_IDEMPOT = store_thm 743 ("REAL_MUL_IDEMPOT", 744 ``!r: real. (r * r = r) <=> (r = 0) \/ (r = 1)``, 745 GEN_TAC 746 >> reverse EQ_TAC 747 >- (RW_TAC real_ss [] >> RW_TAC std_ss [REAL_MUL_LZERO, REAL_MUL_LID]) 748 >> RW_TAC std_ss [] 749 >> Know `r * r = 1 * r` >- RW_TAC real_ss [] 750 >> RW_TAC std_ss [REAL_EQ_RMUL]); 751 752val REAL_SUP_LE_X = store_thm 753 ("REAL_SUP_LE_X", 754 ``!P x:real. (?r. P r) /\ (!r. P r ==> r <= x) ==> sup P <= x``, 755 RW_TAC real_ss [] 756 >> Suff `~(x < sup P)` >- REAL_ARITH_TAC 757 >> STRIP_TAC 758 >> MP_TAC (SPEC ``P:real->bool`` REAL_SUP_LE) 759 >> RW_TAC real_ss [] >| 760 [PROVE_TAC [], 761 PROVE_TAC [], 762 EXISTS_TAC ``x:real`` 763 >> RW_TAC real_ss [] 764 >> PROVE_TAC [real_lte]]); 765 766val REAL_X_LE_SUP = store_thm 767 ("REAL_X_LE_SUP", 768 ``!P x:real. (?r. P r) /\ (?z. !r. P r ==> r <= z) /\ (?r. P r /\ x <= r) 769 ==> x <= sup P``, 770 RW_TAC real_ss [] 771 >> Suff `!y. P y ==> y <= sup P` >- PROVE_TAC [REAL_LE_TRANS] 772 >> MATCH_MP_TAC REAL_SUP_UBOUND_LE 773 >> PROVE_TAC []); 774 775val INF_DEF_ALT = store_thm (* c.f. "inf_alt" in seqTheory *) 776 ("INF_DEF_ALT", 777 ``!p. inf p = ~(sup (\r. ~r IN p)):real``, 778 RW_TAC std_ss [] 779 >> PURE_REWRITE_TAC [inf_def, IMAGE_DEF] 780 >> Suff `(\r. p (-r)) = (\r. -r IN p)` 781 >- RW_TAC std_ss [] 782 >> RW_TAC std_ss [FUN_EQ_THM,SPECIFICATION]); 783 784val LE_INF = store_thm 785 ("LE_INF", 786 ``!p r:real. (?x. x IN p) /\ (!x. x IN p ==> r <= x) ==> r <= inf p``, 787 RW_TAC std_ss [INF_DEF_ALT, SPECIFICATION] 788 >> POP_ASSUM MP_TAC 789 >> ONCE_REWRITE_TAC [GSYM REAL_NEGNEG] 790 >> Q.SPEC_TAC (`~r`, `r`) 791 >> RW_TAC real_ss [REAL_NEGNEG, REAL_LE_NEG] 792 >> MATCH_MP_TAC REAL_SUP_LE_X 793 >> RW_TAC std_ss [] 794 >> PROVE_TAC [REAL_NEGNEG]); 795 796val INF_LE = store_thm 797 ("INF_LE", 798 ``!p r:real. 799 (?z. !x. x IN p ==> z <= x) /\ (?x. x IN p /\ x <= r) ==> inf p <= r``, 800 RW_TAC std_ss [INF_DEF_ALT, SPECIFICATION] 801 >> POP_ASSUM MP_TAC 802 >> ONCE_REWRITE_TAC [GSYM REAL_NEGNEG] 803 >> Q.SPEC_TAC (`~r`, `r`) 804 >> RW_TAC real_ss [REAL_NEGNEG, REAL_LE_NEG] 805 >> MATCH_MP_TAC REAL_X_LE_SUP 806 >> RW_TAC std_ss [] 807 >> PROVE_TAC [REAL_NEGNEG, REAL_LE_NEG]); 808 809val INF_GREATER = store_thm 810 ("INF_GREATER", 811 ``!p z:real. 812 (?x. x IN p) /\ inf p < z ==> 813 (?x. x IN p /\ x < z)``, 814 RW_TAC std_ss [] 815 >> Suff `~(!x. x IN p ==> ~(x < z))` >- PROVE_TAC [] 816 >> REWRITE_TAC [GSYM real_lte] 817 >> STRIP_TAC 818 >> Q.PAT_X_ASSUM `inf p < z` MP_TAC 819 >> RW_TAC std_ss [GSYM real_lte] 820 >> MATCH_MP_TAC LE_INF 821 >> PROVE_TAC []); 822 823val INF_CLOSE = store_thm 824 ("INF_CLOSE", 825 ``!p e:real. 826 (?x. x IN p) /\ 0 < e ==> (?x. x IN p /\ x < inf p + e)``, 827 RW_TAC std_ss [] 828 >> MATCH_MP_TAC INF_GREATER 829 >> CONJ_TAC >- PROVE_TAC [] 830 >> POP_ASSUM MP_TAC 831 >> REAL_ARITH_TAC); 832 833Theorem REAL_NEG_NZ : 834 !x:real. x < 0 ==> x <> 0 835Proof 836 GEN_TAC >> DISCH_TAC 837 >> MATCH_MP_TAC REAL_LT_IMP_NE 838 >> ASM_REWRITE_TAC [] 839QED 840 841val REAL_LT_LMUL_0_NEG = store_thm 842 ("REAL_LT_LMUL_0_NEG",``!x y:real. 0 < x * y /\ x < 0 ==> y < 0``, 843 RW_TAC real_ss [] 844 >> SPOSE_NOT_THEN ASSUME_TAC 845 >> FULL_SIMP_TAC real_ss [REAL_NOT_LT, GSYM REAL_NEG_GT0] 846 >> METIS_TAC [REAL_MUL_LNEG, REAL_LT_IMP_LE, REAL_LE_MUL, 847 REAL_NEG_GE0, REAL_NOT_LT]); 848 849val REAL_LT_RMUL_0_NEG = store_thm 850 ("REAL_LT_RMUL_0_NEG",``!x y:real. 0 < x * y /\ y < 0 ==> x < 0``, 851 RW_TAC real_ss [] 852 >> SPOSE_NOT_THEN ASSUME_TAC 853 >> FULL_SIMP_TAC real_ss [REAL_NOT_LT,GSYM REAL_NEG_GT0] 854 >> METIS_TAC [REAL_MUL_RNEG, REAL_LT_IMP_LE, REAL_LE_MUL, REAL_NEG_GE0, REAL_NOT_LT]); 855 856val REAL_LT_LMUL_NEG_0 = store_thm 857 ("REAL_LT_LMUL_NEG_0",``!x y:real. x * y < 0 /\ 0 < x ==> y < 0``, 858 RW_TAC real_ss [] 859 >> METIS_TAC [REAL_NEG_GT0, REAL_NEG_RMUL, REAL_LT_LMUL_0]); 860 861val REAL_LT_RMUL_NEG_0 = store_thm 862 ("REAL_LT_RMUL_NEG_0",``!x y:real. x * y < 0 /\ 0 < y ==> x < 0``, 863 RW_TAC real_ss [] 864 >> METIS_TAC [REAL_NEG_GT0, REAL_NEG_LMUL, REAL_LT_RMUL_0]); 865 866val REAL_LT_LMUL_NEG_0_NEG = store_thm 867 ("REAL_LT_LMUL_NEG_0_NEG",``!x y:real. x * y < 0 /\ x < 0 ==> 0 < y``, 868 RW_TAC real_ss [] 869 >> METIS_TAC [REAL_NEG_GT0, REAL_NEG_LMUL, REAL_LT_LMUL_0]); 870 871val REAL_LT_RMUL_NEG_0_NEG = store_thm 872 ("REAL_LT_RMUL_NEG_0_NEG",``!x y:real. x * y < 0 /\ y < 0 ==> 0 < x``, 873 RW_TAC real_ss [] 874 >> METIS_TAC [REAL_NEG_GT0, REAL_NEG_RMUL, REAL_LT_RMUL_0]); 875 876val REAL_LT_RDIV_EQ_NEG = store_thm 877 ("REAL_LT_RDIV_EQ_NEG", ``!x y z. z < 0:real ==> (y / z < x <=> x * z < y)``, 878 RW_TAC real_ss [] 879 >> `0<-z` by RW_TAC real_ss [REAL_NEG_GT0] 880 >> `z<>0` by (METIS_TAC [REAL_LT_IMP_NE]) 881 >>EQ_TAC 882 >- (RW_TAC real_ss [] 883 >> `y/z*(-z) < x*(-z)` by METIS_TAC [GSYM REAL_LT_RMUL] 884 >> FULL_SIMP_TAC real_ss [] 885 >> METIS_TAC [REAL_DIV_RMUL, REAL_LT_NEG]) 886 >> RW_TAC real_ss [] 887 >> `-y < x*(-z)` by FULL_SIMP_TAC real_ss [REAL_LT_NEG] 888 >> `-y * inv(-z) < x` by METIS_TAC [GSYM REAL_LT_LDIV_EQ, real_div] 889 >> METIS_TAC [REAL_NEG_INV, REAL_NEG_MUL2, GSYM real_div]); 890 891val REAL_LE_RDIV_EQ_NEG = store_thm 892 ("REAL_LE_RDIV_EQ_NEG", ``!x y z. z < 0:real ==> (y / z <= x <=> x * z <= y)``, 893 RW_TAC real_ss [] 894 >> `0 < -z` by RW_TAC real_ss [REAL_NEG_GT0] 895 >> `z <> 0` by (METIS_TAC [REAL_LT_IMP_NE]) 896 >>EQ_TAC 897 >- (RW_TAC real_ss [] 898 >> `y / z * (-z) <= x * (-z)` by METIS_TAC [GSYM REAL_LE_RMUL] 899 >> FULL_SIMP_TAC real_ss [] 900 >> METIS_TAC [REAL_DIV_RMUL,REAL_LE_NEG]) 901 >> RW_TAC real_ss [] 902 >> `-y <= x * (-z)` by FULL_SIMP_TAC real_ss [REAL_LE_NEG] 903 >> `-y * inv (-z) <= x` by METIS_TAC [GSYM REAL_LE_LDIV_EQ, real_div] 904 >> METIS_TAC [REAL_NEG_INV, REAL_NEG_MUL2, GSYM real_div]); 905 906val POW_POS_EVEN = store_thm 907 ("POW_POS_EVEN",``!x:real. x < 0 ==> ((0 < x pow n) <=> (EVEN n))``, 908 Induct_on `n` 909 >- RW_TAC std_ss [pow,REAL_LT_01,EVEN] 910 >> RW_TAC std_ss [pow,EVEN] 911 >> EQ_TAC 912 >- METIS_TAC [REAL_LT_ANTISYM, REAL_LT_RMUL_0_NEG, REAL_MUL_COMM] 913 >> RW_TAC std_ss [] 914 >> `x pow n <= 0` by METIS_TAC [real_lt] 915 >> `x pow n <> 0` by METIS_TAC [POW_NZ, REAL_LT_IMP_NE] 916 >> `x pow n < 0` by METIS_TAC [REAL_LT_LE] 917 >> METIS_TAC [REAL_NEG_GT0, REAL_NEG_MUL2, REAL_LT_MUL]); 918 919val POW_NEG_ODD = store_thm 920 ("POW_NEG_ODD",``!x:real. x < 0 ==> ((x pow n < 0) <=> (ODD n))``, 921 Induct_on `n` 922 >- RW_TAC std_ss [pow,GSYM real_lte,REAL_LE_01] 923 >> RW_TAC std_ss [pow,ODD] 924 >> EQ_TAC 925 >- METIS_TAC [REAL_LT_RMUL_NEG_0_NEG, REAL_MUL_COMM, REAL_LT_ANTISYM] 926 >> RW_TAC std_ss [] 927 >> `0 <= x pow n` by METIS_TAC [real_lt] 928 >> `x pow n <> 0` by METIS_TAC [POW_NZ, REAL_LT_IMP_NE] 929 >> `0 < x pow n` by METIS_TAC [REAL_LT_LE] 930 >> METIS_TAC [REAL_NEG_GT0, REAL_MUL_LNEG, REAL_LT_MUL]); 931 932val LOGR_MONO_LE = store_thm 933 ("LOGR_MONO_LE",``!x:real y b. 0 < x /\ 0 < y /\ 1 < b ==> (logr b x <= logr b y <=> x <= y)``, 934 RW_TAC std_ss [logr_def,real_div] 935 >> `0 < ln b` by METIS_TAC [REAL_LT_01, LN_1, REAL_LT_TRANS, LN_MONO_LT] 936 >> METIS_TAC [REAL_LT_INV_EQ, REAL_LE_RMUL, LN_MONO_LE]); 937 938val LOGR_MONO_LE_IMP = store_thm 939 ("LOGR_MONO_LE_IMP",``!x:real y b. 0 < x /\ x <= y /\ 1 <= b ==> (logr b x <= logr b y)``, 940 RW_TAC std_ss [logr_def,real_div] 941 >> `0 <= ln b` by METIS_TAC [REAL_LT_01, LN_1, REAL_LTE_TRANS, LN_MONO_LE] 942 >> METIS_TAC [REAL_LE_INV_EQ, REAL_LE_RMUL_IMP, LN_MONO_LE, REAL_LTE_TRANS]); 943 944Theorem REAL_MAX_REDUCE : 945 !x y :real. x <= y \/ x < y ==> (max x y = y) /\ (max y x = y) 946Proof 947 PROVE_TAC [REAL_LT_IMP_LE, REAL_MAX_ACI, max_def] 948QED 949 950Theorem REAL_MIN_REDUCE : 951 !x y :real. x <= y \/ x < y ==> (min x y = x) /\ (min y x = x) 952Proof 953 PROVE_TAC [REAL_LT_IMP_LE, REAL_MIN_ACI, min_def] 954QED 955 956Theorem REAL_LT_MAX_BETWEEN : 957 !x b d :real. x < max b d /\ b <= x ==> x < d 958Proof 959 RW_TAC std_ss [max_def] 960 >> fs [real_lte] 961QED 962 963Theorem REAL_MIN_LE_BETWEEN : 964 !x a c :real. min a c <= x /\ x < a ==> c <= x 965Proof 966 RW_TAC std_ss [min_def] 967 >> PROVE_TAC [REAL_LET_ANTISYM] 968QED 969 970Theorem REAL_ARCH_INV_SUC : (* was: reals_Archimedean *) 971 !x:real. 0 < x ==> ?n. inv &(SUC n) < x 972Proof 973 RW_TAC real_ss [REAL_INV_1OVER] THEN SIMP_TAC real_ss [REAL_LT_LDIV_EQ] THEN 974 ONCE_REWRITE_TAC [REAL_MUL_SYM] THEN 975 ASM_SIMP_TAC real_ss [GSYM REAL_LT_LDIV_EQ] THEN 976 MP_TAC (ISPEC ``1 / x:real`` SIMP_REAL_ARCH) THEN STRIP_TAC THEN 977 Q.EXISTS_TAC `n` THEN FULL_SIMP_TAC real_ss [real_div] THEN 978 RULE_ASSUM_TAC (ONCE_REWRITE_RULE [GSYM REAL_LT_INV_EQ]) THEN 979 REWRITE_TAC [ADD1, GSYM add_ints] THEN REAL_ASM_ARITH_TAC 980QED 981 982Theorem REAL_ARCH_INV' : (* was: ex_inverse_of_nat_less *) 983 !x:real. 0 < x ==> ?n. inv (&n) < x 984Proof 985 RW_TAC std_ss [] THEN FIRST_ASSUM (MP_TAC o MATCH_MP REAL_ARCH_INV_SUC) THEN 986 METIS_TAC [] 987QED 988 989Theorem ADD_POW_2 : 990 !x y :real. (x + y) pow 2 = x pow 2 + y pow 2 + 2 * x * y 991Proof 992 RW_TAC real_ss [REAL_ADD_LDISTRIB, REAL_ADD_RDISTRIB, REAL_ADD_ASSOC, POW_2, 993 GSYM REAL_DOUBLE] 994 >> REAL_ARITH_TAC 995QED 996 997Theorem HARMONIC_SERIES_POW_2 : 998 summable (\n. inv (&(SUC n) pow 2)) 999Proof 1000 MATCH_MP_TAC POS_SUMMABLE 1001 >> CONJ_TAC >- rw [] 1002 >> Q.EXISTS_TAC `2` 1003 >> GEN_TAC 1004 >> Cases_on `n` >- rw [sum] 1005 >> MATCH_MP_TAC REAL_LE_TRANS 1006 >> Q.EXISTS_TAC `1 + sum (1,n') (\n. inv (&n) - inv (&SUC n))` 1007 >> CONJ_TAC 1008 >- (Know `sum (0,SUC n') (\n. inv (&SUC n pow 2)) = 1009 sum (0,1) (\n. inv (&SUC n pow 2)) + sum (1,n') (\n. inv (&SUC n pow 2))` 1010 >- (MATCH_MP_TAC EQ_SYM \\ 1011 MP_TAC (Q.SPECL [`\n. inv (&SUC n pow 2)`, `1`, `n'`] SUM_TWO) \\ 1012 RW_TAC arith_ss [ADD1]) >> Rewr' \\ 1013 Know `sum (0,1) (\n. inv (&SUC n pow 2)) = 1` 1014 >- (REWRITE_TAC [sum, ONE] >> rw []) >> Rewr' \\ 1015 REWRITE_TAC [REAL_LE_LADD] \\ 1016 MATCH_MP_TAC SUM_LE \\ 1017 RW_TAC real_ss [REAL_INV_1OVER] \\ 1018 `&r <> 0` by RW_TAC real_ss [] \\ 1019 `&SUC r <> 0` by RW_TAC real_ss [] \\ 1020 ASM_SIMP_TAC real_ss [REAL_SUB_RAT] \\ 1021 `&SUC r - &r = 1` by METIS_TAC [REAL, REAL_ADD_SUB] >> POP_ORW \\ 1022 ASM_SIMP_TAC std_ss [POW_2, GSYM REAL_INV_1OVER] \\ 1023 `0 < &SUC r * &SUC r` by rw [] \\ 1024 Know `0 < &(r * SUC r)` 1025 >- (rw [] >> `0 = r * 0` by RW_TAC arith_ss [] >> POP_ORW \\ 1026 rw [LT_MULT_LCANCEL]) >> DISCH_TAC \\ 1027 MATCH_MP_TAC REAL_LT_IMP_LE \\ 1028 ASM_SIMP_TAC real_ss [REAL_INV_LT_ANTIMONO] \\ 1029 `SUC r ** 2 = SUC r * SUC r` by RW_TAC arith_ss [] >> POP_ORW \\ 1030 RW_TAC arith_ss [LT_MULT_RCANCEL]) 1031 >> `2 = 1 + (1 :real)` by RW_TAC real_ss [] >> POP_ORW 1032 >> REWRITE_TAC [REAL_LE_LADD] 1033 >> Q.ABBREV_TAC `f = \n. -inv (&n)` 1034 >> Know `!n. inv (&n) - inv (&SUC n) = f (SUC n) - f n` 1035 >- (RW_TAC real_ss [Abbr `f`] \\ 1036 REAL_ASM_ARITH_TAC) >> Rewr' 1037 >> REWRITE_TAC [SUM_CANCEL] 1038 >> rw [Abbr `f`, REAL_SUB_NEG2, REAL_LE_SUB_RADD, REAL_LE_ADDR] 1039QED 1040 1041(* ********************************************* *) 1042(* The mininal element in num sets *) 1043(* ********************************************* *) 1044 1045val minimal_def = Define 1046 `minimal p = @(n:num). p n /\ (!m. m < n ==> ~(p m))`; 1047 1048val MINIMAL_EXISTS0 = store_thm 1049 ("MINIMAL_EXISTS0", ``(?(n:num). P n) = (?n. P n /\ (!m. m < n ==> ~(P m)))``, 1050 reverse EQ_TAC >- PROVE_TAC [] 1051 >> RW_TAC std_ss [] 1052 >> CCONTR_TAC 1053 >> Suff `!n. ~P n` >- PROVE_TAC [] 1054 >> STRIP_TAC 1055 >> completeInduct_on `n'` 1056 >> PROVE_TAC []); 1057 1058val MINIMAL_EXISTS = store_thm 1059 ("MINIMAL_EXISTS", 1060 ``!P. (?n. P n) = (P (minimal P) /\ !n. n < minimal P ==> ~P n)``, 1061 REWRITE_TAC [MINIMAL_EXISTS0, boolTheory.EXISTS_DEF] 1062 >> CONV_TAC (DEPTH_CONV BETA_CONV) 1063 >> REWRITE_TAC [GSYM minimal_def]); 1064 1065val MINIMAL_EXISTS_IMP = store_thm 1066 ("MINIMAL_EXISTS_IMP", 1067 ``!P. (?n : num. P n) ==> ?m. (P m /\ !n. n < m ==> ~P n)``, 1068 PROVE_TAC [MINIMAL_EXISTS]); 1069 1070val MINIMAL_EQ_IMP = store_thm 1071 ("MINIMAL_EQ_IMP", 1072 ``!m p. (p m) /\ (!n. n < m ==> ~p n) ==> (m = minimal p)``, 1073 RW_TAC std_ss [] 1074 >> MP_TAC (Q.SPEC `p` MINIMAL_EXISTS) 1075 >> Know `?n. p n` >- PROVE_TAC [] 1076 >> RW_TAC std_ss [] 1077 >> Suff `~(m < minimal p) /\ ~(minimal p < m)` >- DECIDE_TAC 1078 >> PROVE_TAC []); 1079 1080val MINIMAL_SUC = store_thm 1081 ("MINIMAL_SUC", 1082 ``!n p. 1083 (SUC n = minimal p) /\ p (SUC n) <=> 1084 ~p 0 /\ (n = minimal (p o SUC)) /\ p (SUC n)``, 1085 RW_TAC std_ss [] 1086 >> EQ_TAC >| 1087 [RW_TAC std_ss [] >| 1088 [Know `0 < SUC n` >- DECIDE_TAC 1089 >> PROVE_TAC [MINIMAL_EXISTS], 1090 MATCH_MP_TAC MINIMAL_EQ_IMP 1091 >> RW_TAC std_ss [o_THM] 1092 >> Know `SUC n' < SUC n` >- DECIDE_TAC 1093 >> PROVE_TAC [MINIMAL_EXISTS]], 1094 RW_TAC std_ss [] 1095 >> MATCH_MP_TAC MINIMAL_EQ_IMP 1096 >> RW_TAC std_ss [] 1097 >> Cases_on `n` >- RW_TAC std_ss [] 1098 >> Suff `~((p o SUC) n')` >- RW_TAC std_ss [o_THM] 1099 >> Know `n' < minimal (p o SUC)` >- DECIDE_TAC 1100 >> PROVE_TAC [MINIMAL_EXISTS]]); 1101 1102val MINIMAL_EQ = store_thm 1103 ("MINIMAL_EQ", 1104 ``!p m. p m /\ (m = minimal p) <=> p m /\ (!n. n < m ==> ~p n)``, 1105 RW_TAC std_ss [] 1106 >> reverse EQ_TAC >- PROVE_TAC [MINIMAL_EQ_IMP] 1107 >> RW_TAC std_ss [] 1108 >> Know `?n. p n` >- PROVE_TAC [] 1109 >> RW_TAC std_ss [MINIMAL_EXISTS]); 1110 1111val MINIMAL_SUC_IMP = store_thm 1112 ("MINIMAL_SUC_IMP", 1113 ``!n p. p (SUC n) /\ ~p 0 /\ (n = minimal (p o SUC)) ==> (SUC n = minimal p)``, 1114 PROVE_TAC [MINIMAL_SUC]); 1115 1116(* ------------------------------------------------------------------------- *) 1117(* Disjoint subsets (from HVG's lebesgue_measureTheory) *) 1118(* ------------------------------------------------------------------------- *) 1119 1120Theorem DISJOINT_RESTRICT_L : 1121 !s t c. DISJOINT s t ==> DISJOINT (s INTER c) (t INTER c) 1122Proof SET_TAC [] 1123QED 1124 1125Theorem DISJOINT_RESTRICT_R : 1126 !s t c. DISJOINT s t ==> DISJOINT (c INTER s) (c INTER t) 1127Proof SET_TAC [] 1128QED 1129 1130Theorem DISJOINT_CROSS_L : 1131 !s t c. DISJOINT s t ==> DISJOINT (s CROSS c) (t CROSS c) 1132Proof 1133 RW_TAC std_ss [DISJOINT_ALT, CROSS_DEF, Once EXTENSION, IN_INTER, 1134 NOT_IN_EMPTY, GSPECIFICATION] 1135QED 1136 1137Theorem DISJOINT_CROSS_R : 1138 !s t c. DISJOINT s t ==> DISJOINT (c CROSS s) (c CROSS t) 1139Proof 1140 RW_TAC std_ss [DISJOINT_ALT, CROSS_DEF, Once EXTENSION, IN_INTER, 1141 NOT_IN_EMPTY, GSPECIFICATION] 1142QED 1143 1144Theorem SUBSET_RESTRICT_L : 1145 !r s t. s SUBSET t ==> (s INTER r) SUBSET (t INTER r) 1146Proof SET_TAC [] 1147QED 1148 1149Theorem SUBSET_RESTRICT_R : 1150 !r s t. s SUBSET t ==> (r INTER s) SUBSET (r INTER t) 1151Proof SET_TAC [] 1152QED 1153 1154Theorem SUBSET_RESTRICT_DIFF : 1155 !r s t. s SUBSET t ==> (r DIFF t) SUBSET (r DIFF s) 1156Proof SET_TAC [] 1157QED 1158 1159Theorem SUBSET_INTER_SUBSET_L : 1160 !r s t. s SUBSET t ==> (s INTER r) SUBSET t 1161Proof SET_TAC [] 1162QED 1163 1164Theorem SUBSET_INTER_SUBSET_R : 1165 !r s t. s SUBSET t ==> (r INTER s) SUBSET t 1166Proof SET_TAC [] 1167QED 1168 1169Theorem SUBSET_MONO_DIFF : 1170 !r s t. s SUBSET t ==> (s DIFF r) SUBSET (t DIFF r) 1171Proof SET_TAC [] 1172QED 1173 1174Theorem SUBSET_DIFF_SUBSET : 1175 !r s t. s SUBSET t ==> (s DIFF r) SUBSET t 1176Proof SET_TAC [] 1177QED 1178 1179Theorem SUBSET_DIFF_DISJOINT : 1180 !s1 s2 s3. (s1 SUBSET (s2 DIFF s3)) ==> DISJOINT s1 s3 1181Proof 1182 PROVE_TAC [SUBSET_DIFF] 1183QED 1184 1185val disjoint_def = Define 1186 `disjoint A = !a b. a IN A /\ b IN A /\ (a <> b) ==> DISJOINT a b`; 1187 1188(* |- !A. disjoint A <=> !a b. a IN A /\ b IN A /\ a <> b ==> (a INTER b = {} ) *) 1189val disjoint = save_thm 1190 ("disjoint", REWRITE_RULE [DISJOINT_DEF] disjoint_def); 1191 1192val disjointI = store_thm 1193 ("disjointI", 1194 ``!A. (!a b . a IN A ==> b IN A ==> (a <> b) ==> DISJOINT a b) ==> disjoint A``, 1195 METIS_TAC [disjoint_def]); 1196 1197val disjointD = store_thm 1198 ("disjointD", 1199 ``!A a b. disjoint A ==> a IN A ==> b IN A ==> (a <> b) ==> DISJOINT a b``, 1200 METIS_TAC [disjoint_def]); 1201 1202val disjoint_empty = store_thm 1203 ("disjoint_empty", ``disjoint {}``, 1204 SET_TAC [disjoint_def]); 1205 1206val disjoint_union = store_thm 1207 ("disjoint_union", 1208 ``!A B. disjoint A /\ disjoint B /\ (BIGUNION A INTER BIGUNION B = {}) ==> 1209 disjoint (A UNION B)``, 1210 SET_TAC [disjoint_def]); 1211 1212val disjoint_sing = store_thm 1213 ("disjoint_sing", ``!a. disjoint {a}``, 1214 SET_TAC [disjoint_def]); 1215 1216val disjoint_same = store_thm 1217 ("disjoint_same", ``!s t. (s = t) ==> disjoint {s; t}``, 1218 RW_TAC std_ss [IN_INSERT, IN_SING, disjoint_def]); 1219 1220val disjoint_two = store_thm 1221 ("disjoint_two", ``!s t. s <> t /\ DISJOINT s t ==> disjoint {s; t}``, 1222 RW_TAC std_ss [IN_INSERT, IN_SING, disjoint_def] >- art [] 1223 >> ASM_REWRITE_TAC [DISJOINT_SYM]); 1224 1225val disjoint_image = store_thm (* new *) 1226 ("disjoint_image", 1227 ``!f. (!i j. i <> j ==> DISJOINT (f i) (f j)) ==> disjoint (IMAGE f UNIV)``, 1228 rpt STRIP_TAC 1229 >> MATCH_MP_TAC disjointI 1230 >> RW_TAC std_ss [IN_IMAGE, IN_UNIV] 1231 >> METIS_TAC []); 1232 1233val disjoint_insert_imp = store_thm (* new *) 1234 ("disjoint_insert_imp", 1235 ``!e c. disjoint (e INSERT c) ==> disjoint c``, 1236 RW_TAC std_ss [disjoint_def] 1237 >> FIRST_ASSUM MATCH_MP_TAC 1238 >> METIS_TAC [IN_INSERT]); 1239 1240val disjoint_insert_notin = store_thm (* new *) 1241 ("disjoint_insert_notin", 1242 ``!e c. disjoint (e INSERT c) /\ e NOTIN c ==> !s. s IN c ==> DISJOINT e s``, 1243 RW_TAC std_ss [disjoint_def] 1244 >> FIRST_ASSUM MATCH_MP_TAC 1245 >> METIS_TAC [IN_INSERT]); 1246 1247val disjoint_insert = store_thm (* new *) 1248 ("disjoint_insert", 1249 ``!e c. disjoint c /\ (!x. x IN c ==> DISJOINT x e) ==> disjoint (e INSERT c)``, 1250 rpt STRIP_TAC 1251 >> Know `e INSERT c = {e} UNION c` >- SET_TAC [] >> Rewr' 1252 >> MATCH_MP_TAC disjoint_union 1253 >> art [disjoint_sing, BIGUNION_SING] 1254 >> ASM_SET_TAC []); 1255 1256val disjoint_restrict = store_thm (* new *) 1257 ("disjoint_restrict", 1258 ``!e c. disjoint c ==> disjoint (IMAGE ($INTER e) c)``, 1259 RW_TAC std_ss [disjoint_def, IN_IMAGE, o_DEF] 1260 >> MATCH_MP_TAC DISJOINT_RESTRICT_R 1261 >> FIRST_X_ASSUM MATCH_MP_TAC >> art [] 1262 >> CCONTR_TAC >> fs []); 1263 1264(* ------------------------------------------------------------------------- *) 1265(* Binary Unions *) 1266(* ------------------------------------------------------------------------- *) 1267 1268Definition binary_def : 1269 binary a b = (\x:num. if x = 0 then a else b) 1270End 1271 1272Theorem BINARY_RANGE : (* was: range_binary_eq *) 1273 !a b. IMAGE (binary a b) UNIV = {a;b} 1274Proof 1275 RW_TAC std_ss [IMAGE_DEF, binary_def] THEN 1276 SIMP_TAC std_ss [EXTENSION, GSPECIFICATION, SET_RULE 1277 ``x IN {a;b} <=> (x = a) \/ (x = b)``] THEN 1278 GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL 1279 [METIS_TAC [], METIS_TAC [IN_UNIV], 1280 EXISTS_TAC ``1:num`` THEN ASM_SIMP_TAC arith_ss [IN_UNIV]] 1281QED 1282 1283Theorem UNION_BINARY : (* was: Un_range_binary *) 1284 !a b. a UNION b = BIGUNION {binary a b i | i IN UNIV} 1285Proof 1286 SIMP_TAC arith_ss [GSYM IMAGE_DEF] THEN 1287 REWRITE_TAC [METIS [ETA_AX] ``(\i. binary a b i) = binary a b``] THEN 1288 SIMP_TAC std_ss [BINARY_RANGE] THEN SET_TAC [] 1289QED 1290 1291Theorem INTER_BINARY : (* was: Int_range_binary *) 1292 !a b. a INTER b = BIGINTER {binary a b i | i IN UNIV} 1293Proof 1294 SIMP_TAC arith_ss [GSYM IMAGE_DEF] THEN 1295 REWRITE_TAC [METIS [ETA_AX] ``(\i. binary a b i) = binary a b``] THEN 1296 SIMP_TAC std_ss [BINARY_RANGE] THEN SET_TAC [] 1297QED 1298 1299(* ------------------------------------------------------------------------- *) 1300(* Some lemmas needed by CARATHEODORY in measureTheory (author: Chun Tian) *) 1301(* ------------------------------------------------------------------------- *) 1302 1303val DINTER_IMP_FINITE_INTER = store_thm 1304 ("DINTER_IMP_FINITE_INTER", 1305 ``!sts f. (!s t. s IN sts /\ t IN sts ==> s INTER t IN sts) /\ 1306 f IN (UNIV -> sts) 1307 ==> !n. 0 < n ==> BIGINTER (IMAGE f (count n)) IN sts``, 1308 rpt GEN_TAC 1309 >> STRIP_TAC 1310 >> Induct_on `n` 1311 >> RW_TAC arith_ss [] 1312 >> fs [IN_FUNSET, IN_UNIV] 1313 >> STRIP_ASSUME_TAC (Q.SPEC `n` LESS_0_CASES) 1314 >- RW_TAC std_ss [COUNT_SUC, COUNT_ZERO, IMAGE_INSERT, IMAGE_EMPTY, 1315 BIGINTER_INSERT, IMAGE_EMPTY, BIGINTER_EMPTY, INTER_UNIV] 1316 >> fs [COUNT_SUC]); 1317 1318(* Dual lemma of above, used in "ring_and_semiring" *) 1319val DUNION_IMP_FINITE_UNION = store_thm 1320 ("DUNION_IMP_FINITE_UNION", 1321 ``!sts f. (!s t. s IN sts /\ t IN sts ==> s UNION t IN sts) ==> 1322 !n. 0 < n /\ (!i. i < n ==> f i IN sts) ==> 1323 BIGUNION (IMAGE f (count n)) IN sts``, 1324 rpt GEN_TAC 1325 >> STRIP_TAC 1326 >> Induct_on `n` 1327 >> RW_TAC arith_ss [] 1328 >> fs [IN_FUNSET, IN_UNIV] 1329 >> STRIP_ASSUME_TAC (Q.SPEC `n` LESS_0_CASES) 1330 >- RW_TAC std_ss [COUNT_SUC, COUNT_ZERO, IMAGE_INSERT, IMAGE_EMPTY, 1331 BIGUNION_INSERT, IMAGE_EMPTY, BIGUNION_EMPTY, UNION_EMPTY] 1332 >> fs [COUNT_SUC]); 1333 1334val GEN_DIFF_INTER = store_thm 1335 ("GEN_DIFF_INTER", 1336 ``!sp s t. s SUBSET sp /\ t SUBSET sp ==> (s DIFF t = s INTER (sp DIFF t))``, 1337 rpt STRIP_TAC 1338 >> ASM_SET_TAC []); 1339 1340val GEN_COMPL_UNION = store_thm 1341 ("GEN_COMPL_UNION", 1342 ``!sp s t. s SUBSET sp /\ t SUBSET sp ==> 1343 (sp DIFF (s UNION t) = (sp DIFF s) INTER (sp DIFF t))``, 1344 rpt STRIP_TAC 1345 >> ASM_SET_TAC []) 1346 1347val GEN_COMPL_INTER = store_thm 1348 ("GEN_COMPL_INTER", 1349 ``!sp s t. s SUBSET sp /\ t SUBSET sp ==> 1350 (sp DIFF (s INTER t) = (sp DIFF s) UNION (sp DIFF t))``, 1351 rpt STRIP_TAC 1352 >> ASM_SET_TAC []) 1353 1354val COMPL_BIGINTER_IMAGE = store_thm 1355 ("COMPL_BIGINTER_IMAGE", 1356 ``!f. COMPL (BIGINTER (IMAGE f univ(:num))) = BIGUNION (IMAGE (COMPL o f) univ(:num))``, 1357 RW_TAC std_ss [EXTENSION, IN_COMPL, IN_BIGINTER_IMAGE, IN_BIGUNION_IMAGE, IN_UNIV]); 1358 1359val COMPL_BIGUNION_IMAGE = store_thm 1360 ("COMPL_BIGUNION_IMAGE", 1361 ``!f. COMPL (BIGUNION (IMAGE f univ(:num))) = BIGINTER (IMAGE (COMPL o f) univ(:num))``, 1362 RW_TAC std_ss [EXTENSION, IN_COMPL, IN_BIGINTER_IMAGE, IN_BIGUNION_IMAGE, IN_UNIV]); 1363 1364val GEN_COMPL_BIGINTER_IMAGE = store_thm 1365 ("GEN_COMPL_BIGINTER_IMAGE", 1366 ``!sp f. (!n. f n SUBSET sp) ==> 1367 (sp DIFF (BIGINTER (IMAGE f univ(:num))) = 1368 BIGUNION (IMAGE (\n. sp DIFF (f n)) univ(:num)))``, 1369 RW_TAC std_ss [EXTENSION, IN_DIFF, IN_BIGINTER_IMAGE, IN_BIGUNION_IMAGE, IN_UNIV] 1370 >> EQ_TAC >> rpt STRIP_TAC >> art [] 1371 >- (Q.EXISTS_TAC `y` >> art []) 1372 >> Q.EXISTS_TAC `n` >> art []); 1373 1374val GEN_COMPL_BIGUNION_IMAGE = store_thm 1375 ("GEN_COMPL_BIGUNION_IMAGE", 1376 ``!sp f. (!n. f n SUBSET sp) ==> 1377 (sp DIFF (BIGUNION (IMAGE f univ(:num))) = 1378 BIGINTER (IMAGE (\n. sp DIFF (f n)) univ(:num)))``, 1379 RW_TAC std_ss [EXTENSION, IN_DIFF, IN_BIGINTER_IMAGE, IN_BIGUNION_IMAGE, IN_UNIV] 1380 >> EQ_TAC >> rpt STRIP_TAC >> art [] 1381 >> METIS_TAC []); 1382 1383val COMPL_BIGINTER = store_thm 1384 ("COMPL_BIGINTER", 1385 ``!c. COMPL (BIGINTER c) = BIGUNION (IMAGE COMPL c)``, 1386 RW_TAC std_ss [EXTENSION, IN_COMPL, IN_BIGINTER, IN_BIGUNION_IMAGE]); 1387 1388val COMPL_BIGUNION = store_thm 1389 ("COMPL_BIGUNION", 1390 ``!c. c <> {} ==> (COMPL (BIGUNION c) = BIGINTER (IMAGE COMPL c))``, 1391 RW_TAC std_ss [NOT_IN_EMPTY, EXTENSION, IN_COMPL, IN_BIGUNION, IN_BIGINTER_IMAGE] 1392 >> EQ_TAC >> rpt STRIP_TAC 1393 >> PROVE_TAC []); 1394 1395val GEN_COMPL_BIGINTER = store_thm 1396 ("GEN_COMPL_BIGINTER", 1397 ``!sp c. (!x. x IN c ==> x SUBSET sp) ==> 1398 (sp DIFF (BIGINTER c) = BIGUNION (IMAGE (\x. sp DIFF x) c))``, 1399 RW_TAC std_ss [EXTENSION, IN_DIFF, IN_BIGINTER, IN_BIGUNION_IMAGE] 1400 >> EQ_TAC >> rpt STRIP_TAC >> art [] 1401 >- (Q.EXISTS_TAC `P` >> art []) 1402 >> Q.EXISTS_TAC `x'` >> art []); 1403 1404val GEN_COMPL_BIGUNION = store_thm 1405 ("GEN_COMPL_BIGUNION", 1406 ``!sp c. c <> {} /\ (!x. x IN c ==> x SUBSET sp) ==> 1407 (sp DIFF (BIGUNION c) = BIGINTER (IMAGE (\x. sp DIFF x) c))``, 1408 RW_TAC std_ss [EXTENSION, IN_DIFF, IN_BIGINTER, IN_BIGUNION, IN_BIGINTER_IMAGE, 1409 NOT_IN_EMPTY] 1410 >> EQ_TAC >> rpt STRIP_TAC >> art [] 1411 >> METIS_TAC []); 1412 1413val GEN_COMPL_FINITE_UNION = store_thm 1414 ("GEN_COMPL_FINITE_UNION", 1415 ``!sp f n. 0 < n ==> (sp DIFF BIGUNION (IMAGE f (count n)) = 1416 BIGINTER (IMAGE (\i. sp DIFF f i) (count n)))``, 1417 NTAC 2 GEN_TAC 1418 >> Induct_on `n` 1419 >> RW_TAC arith_ss [] 1420 >> STRIP_ASSUME_TAC (Q.SPEC `n` LESS_0_CASES) 1421 >- RW_TAC std_ss [COUNT_SUC, COUNT_ZERO, IMAGE_INSERT, IMAGE_EMPTY, BIGINTER_SING, 1422 BIGUNION_INSERT, IMAGE_EMPTY, BIGUNION_EMPTY, UNION_EMPTY] 1423 >> fs [COUNT_SUC] 1424 >> ONCE_REWRITE_TAC [UNION_COMM] 1425 >> ASM_REWRITE_TAC [DIFF_UNION] 1426 >> REWRITE_TAC [DIFF_INTER] 1427 >> Suff `(BIGINTER (IMAGE (\i. sp DIFF f i) (count n)) DIFF f n) SUBSET sp` 1428 >- (KILL_TAC >> DISCH_THEN (ASSUME_TAC o (MATCH_MP SUBSET_INTER2)) >> ASM_SET_TAC []) 1429 >> MATCH_MP_TAC SUBSET_TRANS 1430 >> Q.EXISTS_TAC `BIGINTER (IMAGE (\i. sp DIFF f i) (count n))` 1431 >> REWRITE_TAC [DIFF_SUBSET] 1432 >> REWRITE_TAC [SUBSET_DEF, IN_BIGINTER_IMAGE, IN_COUNT] >> BETA_TAC 1433 >> RW_TAC std_ss [IN_DIFF] 1434 >> RES_TAC); 1435 1436val BIGINTER_PAIR = store_thm 1437 ("BIGINTER_PAIR", 1438 ``!s t. BIGINTER {s; t} = s INTER t``, 1439 RW_TAC std_ss [EXTENSION, IN_BIGINTER, IN_INTER, IN_INSERT, NOT_IN_EMPTY] 1440 >> PROVE_TAC []); 1441 1442val DIFF_INTER_PAIR = store_thm 1443 ("DIFF_INTER_PAIR", 1444 ``!sp x y. sp DIFF (x INTER y) = (sp DIFF x) UNION (sp DIFF y)``, 1445 rpt GEN_TAC 1446 >> REWRITE_TAC [REWRITE_RULE [BIGINTER_PAIR] (Q.SPECL [`sp`, `{x; y}`] DIFF_BIGINTER1)] 1447 >> REWRITE_TAC [EXTENSION, IN_UNION, IN_BIGUNION_IMAGE] 1448 >> BETA_TAC 1449 >> GEN_TAC >> EQ_TAC >> rpt STRIP_TAC 1450 >| [ fs [IN_INSERT] >> PROVE_TAC [], 1451 Q.EXISTS_TAC `x` >> ASM_REWRITE_TAC [IN_INSERT], 1452 Q.EXISTS_TAC `y` >> ASM_REWRITE_TAC [IN_INSERT] ]); 1453 1454val GEN_COMPL_FINITE_INTER = store_thm 1455 ("GEN_COMPL_FINITE_INTER", 1456 ``!sp f n. 0 < n ==> (sp DIFF BIGINTER (IMAGE f (count n)) = 1457 BIGUNION (IMAGE (\i. sp DIFF f i) (count n)))``, 1458 NTAC 2 GEN_TAC 1459 >> Induct_on `n` 1460 >> RW_TAC arith_ss [] 1461 >> STRIP_ASSUME_TAC (Q.SPEC `n` LESS_0_CASES) 1462 >- RW_TAC std_ss [COUNT_SUC, COUNT_ZERO, IMAGE_INSERT, IMAGE_EMPTY, BIGINTER_SING, 1463 BIGUNION_INSERT, IMAGE_EMPTY, BIGUNION_EMPTY, UNION_EMPTY] 1464 >> fs [COUNT_SUC] 1465 >> ASM_REWRITE_TAC [DIFF_INTER_PAIR]); 1466 1467(* This proof is provided by Thomas Tuerk, needed by SETS_TO_DISJOINT_SETS *) 1468val BIGUNION_IMAGE_COUNT_IMP_UNIV = store_thm 1469 ("BIGUNION_IMAGE_COUNT_IMP_UNIV", 1470 ``!f g. (!n. BIGUNION (IMAGE g (count n)) = BIGUNION (IMAGE f (count n))) ==> 1471 (BIGUNION (IMAGE f UNIV) = BIGUNION (IMAGE g UNIV))``, 1472 (* proof *) 1473 `!f g. (!n. BIGUNION (IMAGE g (count n)) = BIGUNION (IMAGE f (count n))) ==> 1474 (BIGUNION (IMAGE f UNIV) SUBSET BIGUNION (IMAGE g UNIV))` 1475 suffices_by PROVE_TAC [SUBSET_ANTISYM] 1476 >> REWRITE_TAC [SUBSET_DEF] 1477 >> REPEAT STRIP_TAC 1478 >> rename1 `e IN BIGUNION _` 1479 >> Know `?n. e IN BIGUNION (IMAGE f (count n))` 1480 >- (FULL_SIMP_TAC std_ss [IN_BIGUNION, IN_IMAGE, PULL_EXISTS, IN_COUNT] \\ 1481 rename1 `e IN f n'` \\ 1482 Q.EXISTS_TAC `SUC n'` \\ 1483 Q.EXISTS_TAC `n'` \\ 1484 ASM_SIMP_TAC arith_ss []) 1485 >> STRIP_TAC 1486 >> `e IN BIGUNION (IMAGE g (count n))` by PROVE_TAC [] 1487 >> FULL_SIMP_TAC std_ss [IN_BIGUNION, IN_IMAGE, PULL_EXISTS, IN_UNIV] 1488 >> METIS_TAC []); 1489 1490val BIGUNION_OVER_INTER_L = store_thm 1491 ("BIGUNION_OVER_INTER_L", 1492 ``!f d. BIGUNION (IMAGE f univ(:num)) INTER d = 1493 BIGUNION (IMAGE (\i. f i INTER d) univ(:num))``, 1494 rpt GEN_TAC 1495 >> REWRITE_TAC [EXTENSION] 1496 >> GEN_TAC >> EQ_TAC 1497 >| [ (* goal 1 (of 2) *) 1498 RW_TAC std_ss [IN_BIGUNION, IN_INTER, IN_IMAGE] \\ 1499 `x IN (f x' INTER d)` by PROVE_TAC [IN_INTER] \\ 1500 Q.EXISTS_TAC `f x' INTER d` >> art [] \\ 1501 Q.EXISTS_TAC `x'` >> art [], 1502 (* goal 2 (of 2) *) 1503 RW_TAC std_ss [IN_BIGUNION, IN_INTER, IN_IMAGE] >| 1504 [ fs [IN_INTER] >> Q.EXISTS_TAC `f i` >> ASM_REWRITE_TAC [] \\ 1505 Q.EXISTS_TAC `i` >> REWRITE_TAC [], 1506 PROVE_TAC [IN_INTER] ] ]); 1507 1508val BIGUNION_OVER_INTER_R = store_thm 1509 ("BIGUNION_OVER_INTER_R", 1510 ``!f d. d INTER BIGUNION (IMAGE f univ(:num)) = 1511 BIGUNION (IMAGE (\i. d INTER f i) univ(:num))``, 1512 rpt GEN_TAC 1513 >> REWRITE_TAC [EXTENSION] 1514 >> GEN_TAC >> EQ_TAC 1515 >| [ (* goal 1 (of 2) *) 1516 RW_TAC std_ss [IN_BIGUNION, IN_INTER, IN_IMAGE, IN_UNIV] \\ 1517 `x IN (d INTER f x')` by PROVE_TAC [IN_INTER] \\ 1518 Q.EXISTS_TAC `d INTER f x'` >> art [] \\ 1519 Q.EXISTS_TAC `x'` >> art [], 1520 (* goal 2 (of 2) *) 1521 RW_TAC std_ss [IN_BIGUNION, IN_INTER, IN_IMAGE, IN_UNIV] >| 1522 [ fs [IN_INTER] >> Q.EXISTS_TAC `f i` >> ASM_REWRITE_TAC [] \\ 1523 Q.EXISTS_TAC `i` >> REWRITE_TAC [], 1524 PROVE_TAC [IN_INTER] ] ]); 1525 1526val BIGUNION_OVER_DIFF = store_thm 1527 ("BIGUNION_OVER_DIFF", 1528 ``!f d. BIGUNION (IMAGE f univ(:num)) DIFF d = 1529 BIGUNION (IMAGE (\i. f i DIFF d) univ(:num))``, 1530 rpt GEN_TAC 1531 >> REWRITE_TAC [EXTENSION] 1532 >> GEN_TAC >> EQ_TAC 1533 >| [ (* goal 1 (of 2) *) 1534 RW_TAC std_ss [IN_BIGUNION, IN_DIFF, IN_IMAGE, IN_UNIV] \\ 1535 `x IN (f x' DIFF d)` by PROVE_TAC [IN_DIFF] \\ 1536 Q.EXISTS_TAC `f x' DIFF d` >> art [] \\ 1537 Q.EXISTS_TAC `x'` >> art [], 1538 (* goal 2 (of 2) *) 1539 RW_TAC std_ss [IN_BIGUNION, IN_DIFF, IN_IMAGE, IN_UNIV] >| 1540 [ fs [IN_DIFF] >> Q.EXISTS_TAC `f i` >> art [] \\ 1541 Q.EXISTS_TAC `i` >> REWRITE_TAC [], 1542 PROVE_TAC [IN_DIFF] ] ]); 1543 1544val BIGUNION_IMAGE_OVER_INTER_L = store_thm 1545 ("BIGUNION_IMAGE_OVER_INTER_L", 1546 ``!f n d. BIGUNION (IMAGE f (count n)) INTER d = 1547 BIGUNION (IMAGE (\i. f i INTER d) (count n))``, 1548 rpt GEN_TAC 1549 >> REWRITE_TAC [EXTENSION] 1550 >> GEN_TAC >> EQ_TAC 1551 >| [ RW_TAC std_ss [IN_BIGUNION, IN_INTER, IN_IMAGE] \\ 1552 `x IN (f x' INTER d)` by PROVE_TAC [IN_INTER] \\ 1553 Q.EXISTS_TAC `f x' INTER d` >> art [] \\ 1554 Q.EXISTS_TAC `x'` >> art [], 1555 RW_TAC std_ss [IN_BIGUNION, IN_INTER, IN_IMAGE] >| 1556 [ fs [IN_INTER] >> Q.EXISTS_TAC `f i` >> art [] \\ 1557 Q.EXISTS_TAC `i` >> art [], 1558 PROVE_TAC [IN_INTER] ] ]); 1559 1560val BIGUNION_IMAGE_OVER_INTER_R = store_thm 1561 ("BIGUNION_IMAGE_OVER_INTER_R", 1562 ``!f n d. d INTER BIGUNION (IMAGE f (count n)) = 1563 BIGUNION (IMAGE (\i. d INTER f i) (count n))``, 1564 rpt GEN_TAC 1565 >> ONCE_REWRITE_TAC [INTER_COMM] 1566 >> REWRITE_TAC [BIGUNION_IMAGE_OVER_INTER_L]); 1567 1568val BIGINTER_IMAGE_OVER_INTER_L = store_thm 1569 ("BIGINTER_IMAGE_OVER_INTER_L", 1570 ``!f n d. 0 < n ==> 1571 (BIGINTER (IMAGE f (count n)) INTER d = 1572 BIGINTER (IMAGE (\i. f i INTER d) (count n)))``, 1573 rpt STRIP_TAC 1574 >> REWRITE_TAC [EXTENSION] 1575 >> GEN_TAC >> EQ_TAC 1576 >| [ RW_TAC std_ss [IN_BIGINTER_IMAGE, IN_INTER, IN_COUNT], 1577 RW_TAC std_ss [IN_BIGINTER_IMAGE, IN_INTER, IN_COUNT] >> RES_TAC ]); 1578 1579val BIGINTER_IMAGE_OVER_INTER_R = store_thm 1580 ("BIGINTER_IMAGE_OVER_INTER_R", 1581 ``!f n d. 0 < n ==> 1582 (d INTER BIGINTER (IMAGE f (count n)) = 1583 BIGINTER (IMAGE (\i. d INTER f i) (count n)))``, 1584 rpt STRIP_TAC 1585 >> ONCE_REWRITE_TAC [INTER_COMM] 1586 >> MATCH_MP_TAC BIGINTER_IMAGE_OVER_INTER_L >> art []); 1587 1588(* any finite set can be decomposed into a finite sequence of sets *) 1589val finite_decomposition_simple = store_thm (* new *) 1590 ("finite_decomposition_simple", 1591 ``!c. FINITE c ==> ?f n. (!x. x < n ==> f x IN c) /\ (c = IMAGE f (count n))``, 1592 GEN_TAC 1593 >> REWRITE_TAC [FINITE_BIJ_COUNT_EQ] 1594 >> rpt STRIP_TAC 1595 >> rename1 `BIJ f (count n) c` 1596 >> Q.EXISTS_TAC `f` 1597 >> Q.EXISTS_TAC `n` 1598 >> CONJ_TAC >- (rpt STRIP_TAC >> PROVE_TAC [BIJ_DEF, INJ_DEF, IN_COUNT]) 1599 >> PROVE_TAC [BIJ_IMAGE]); 1600 1601(* any finite set can be decomposed into a finite (non-repeated) sequence of sets *) 1602val finite_decomposition = store_thm (* new *) 1603 ("finite_decomposition", 1604 ``!c. FINITE c ==> 1605 ?f n. (!x. x < n ==> f x IN c) /\ (c = IMAGE f (count n)) /\ 1606 (!i j. i < n /\ j < n /\ i <> j ==> f i <> f j)``, 1607 GEN_TAC 1608 >> REWRITE_TAC [FINITE_BIJ_COUNT_EQ] 1609 >> rpt STRIP_TAC 1610 >> rename1 `BIJ f (count n) c` 1611 >> Q.EXISTS_TAC `f` 1612 >> Q.EXISTS_TAC `n` 1613 >> CONJ_TAC >- (rpt STRIP_TAC >> PROVE_TAC [BIJ_DEF, INJ_DEF, IN_COUNT]) 1614 >> CONJ_TAC >- PROVE_TAC [BIJ_IMAGE] 1615 >> rpt STRIP_TAC 1616 >> fs [BIJ_ALT, IN_FUNSET, IN_COUNT] 1617 >> METIS_TAC []); 1618 1619(* any finite disjoint set can be decomposed into a finite pair-wise 1620 disjoint sequence of sets *) 1621val finite_disjoint_decomposition = store_thm (* new *) 1622 ("finite_disjoint_decomposition", 1623 ``!c. FINITE c /\ disjoint c ==> 1624 ?f n. (!i. i < n ==> f i IN c) /\ (c = IMAGE f (count n)) /\ 1625 (!i j. i < n /\ j < n /\ i <> j ==> f i <> f j) /\ 1626 (!i j. i < n /\ j < n /\ i <> j ==> DISJOINT (f i) (f j))``, 1627 GEN_TAC 1628 >> REWRITE_TAC [FINITE_BIJ_COUNT_EQ] 1629 >> rpt STRIP_TAC 1630 >> rename1 `BIJ f (count n) c` 1631 >> Q.EXISTS_TAC `f` 1632 >> Q.EXISTS_TAC `n` 1633 >> STRONG_CONJ_TAC 1634 >- (rpt STRIP_TAC >> PROVE_TAC [BIJ_DEF, INJ_DEF, IN_COUNT]) 1635 >> DISCH_TAC 1636 >> CONJ_TAC >- PROVE_TAC [BIJ_IMAGE] 1637 >> STRONG_CONJ_TAC 1638 >- (rpt STRIP_TAC \\ 1639 fs [BIJ_ALT, IN_FUNSET, IN_COUNT] >> METIS_TAC []) 1640 >> rpt STRIP_TAC 1641 >> fs [disjoint_def] 1642 >> FIRST_X_ASSUM MATCH_MP_TAC 1643 >> METIS_TAC []); 1644 1645val countable_disjoint_decomposition = store_thm (* new *) 1646 ("countable_disjoint_decomposition", 1647 ``!c. FINITE c /\ disjoint c ==> 1648 ?f n. (!i. i < n ==> f i IN c) /\ (!i. n <= i ==> (f i = {})) /\ 1649 (c = IMAGE f (count n)) /\ 1650 (BIGUNION c = BIGUNION (IMAGE f univ(:num))) /\ 1651 (!i j. i < n /\ j < n /\ i <> j ==> f i <> f j) /\ 1652 (!i j. i < n /\ j < n /\ i <> j ==> DISJOINT (f i) (f j))``, 1653 rpt STRIP_TAC 1654 >> STRIP_ASSUME_TAC 1655 (MATCH_MP finite_disjoint_decomposition 1656 (CONJ (ASSUME ``FINITE (c :'a set set)``) 1657 (ASSUME ``disjoint (c :'a set set)``))) 1658 >> Q.EXISTS_TAC `\i. if i < n then f i else {}` 1659 >> Q.EXISTS_TAC `n` 1660 >> BETA_TAC 1661 >> CONJ_TAC >- METIS_TAC [] 1662 >> CONJ_TAC >- METIS_TAC [NOT_LESS] 1663 >> CONJ_TAC 1664 >- (art [] >> MATCH_MP_TAC IMAGE_CONG >> RW_TAC std_ss [IN_COUNT]) 1665 >> reverse CONJ_TAC >- METIS_TAC [] 1666 >> art [] >> KILL_TAC 1667 >> SIMP_TAC std_ss [Once EXTENSION, IN_BIGUNION_IMAGE, IN_COUNT, IN_UNIV] 1668 >> GEN_TAC >> EQ_TAC >> rpt STRIP_TAC 1669 >| [ Q.EXISTS_TAC `x'` >> METIS_TAC [], 1670 Cases_on `i < n` >- (Q.EXISTS_TAC `i` >> METIS_TAC []) \\ 1671 fs [NOT_IN_EMPTY] ]); 1672 1673(* any union of two sets can be decomposed into 3 disjoint unions *) 1674val UNION_TO_3_DISJOINT_UNIONS = store_thm (* new *) 1675 ("UNION_TO_3_DISJOINT_UNIONS", 1676 ``!s t. (s UNION t = (s DIFF t) UNION (s INTER t) UNION (t DIFF s)) /\ 1677 disjoint {(s DIFF t); (s INTER t); (t DIFF s)}``, 1678 NTAC 2 GEN_TAC 1679 >> CONJ_TAC >- SET_TAC [] 1680 >> REWRITE_TAC [disjoint_def, DISJOINT_DEF] 1681 >> RW_TAC std_ss [IN_INSERT] 1682 >> ASM_SET_TAC []); 1683 1684val BIGUNION_IMAGE_BIGUNION_IMAGE_UNIV = store_thm 1685 ("BIGUNION_IMAGE_BIGUNION_IMAGE_UNIV", 1686 ``!f. BIGUNION (IMAGE (\n. BIGUNION (IMAGE (f n) univ(:num))) univ(:num)) = 1687 BIGUNION (IMAGE (UNCURRY f) univ(:num # num))``, 1688 GEN_TAC 1689 >> RW_TAC std_ss [EXTENSION, IN_BIGUNION_IMAGE, IN_UNIV, IN_CROSS, UNCURRY] 1690 >> EQ_TAC >> STRIP_TAC 1691 >- (Q.EXISTS_TAC `(n, x')` >> art [FST, SND]) 1692 >> Q.EXISTS_TAC `FST x'` 1693 >> Q.EXISTS_TAC `SND x'` >> art []); 1694 1695val BIGUNION_IMAGE_UNIV_CROSS_UNIV = store_thm 1696 ("BIGUNION_IMAGE_UNIV_CROSS_UNIV", 1697 ``!f (h :num -> num # num). BIJ h UNIV (UNIV CROSS UNIV) ==> 1698 (BIGUNION (IMAGE (UNCURRY f) univ(:num # num)) = 1699 BIGUNION (IMAGE (UNCURRY f o h) univ(:num)))``, 1700 rpt STRIP_TAC 1701 >> RW_TAC std_ss [EXTENSION, IN_BIGUNION_IMAGE, IN_UNIV, IN_CROSS, UNCURRY, o_DEF] 1702 >> fs [BIJ_ALT, IN_FUNSET, IN_UNIV] 1703 >> EQ_TAC >> STRIP_TAC 1704 >- (Q.PAT_X_ASSUM `!y. ?!x. y = h x` (MP_TAC o (Q.SPEC `x'`)) >> METIS_TAC []) 1705 >> Q.EXISTS_TAC `h x'` >> art []); 1706 1707 1708(* ------------------------------------------------------------------------- *) 1709(* Three series of lemmas on bigunion-equivalent sequences of sets *) 1710(* ------------------------------------------------------------------------- *) 1711 1712(* 1. for any sequence of sets, there is an increasing sequence of the same bigunion. *) 1713val SETS_TO_INCREASING_SETS = store_thm 1714 ("SETS_TO_INCREASING_SETS", 1715 ``!f :num->'a set. 1716 ?g. (g 0 = f 0) /\ (!n. g n = BIGUNION (IMAGE f (count (SUC n)))) /\ 1717 (!n. g n SUBSET g (SUC n)) /\ 1718 (BIGUNION (IMAGE f UNIV) = BIGUNION (IMAGE g UNIV))``, 1719 rpt STRIP_TAC 1720 >> Q.EXISTS_TAC `\n. BIGUNION (IMAGE f (count (SUC n)))` 1721 >> BETA_TAC 1722 >> RW_TAC bool_ss [] 1723 >| [ (* goal 1 (of 3) *) 1724 REWRITE_TAC [COUNT_SUC, COUNT_ZERO, IMAGE_SING, BIGUNION_SING], 1725 (* goal 2 (of 3) *) 1726 `count (SUC (SUC n)) = (SUC n) INSERT (count (SUC n))` 1727 by PROVE_TAC [COUNT_SUC] >> POP_ORW \\ 1728 REWRITE_TAC [IMAGE_INSERT, BIGUNION_INSERT] \\ 1729 REWRITE_TAC [SUBSET_UNION], 1730 (* goal 3 (of 3) *) 1731 MATCH_MP_TAC BIGUNION_IMAGE_COUNT_IMP_UNIV \\ 1732 Induct_on `n` >- REWRITE_TAC [COUNT_ZERO, IMAGE_EMPTY, BIGUNION_EMPTY] \\ 1733 `count (SUC n) = n INSERT (count n)` by PROVE_TAC [COUNT_SUC] \\ 1734 POP_ORW >> REWRITE_TAC [IMAGE_INSERT, BIGUNION_INSERT] \\ 1735 POP_ASSUM (REWRITE_TAC o wrap) \\ 1736 BETA_TAC \\ 1737 Cases_on `n = 0` >> fs [COUNT_SUC, COUNT_ZERO, IMAGE_SING, BIGUNION_SING] \\ 1738 REWRITE_TAC [GSYM UNION_ASSOC, UNION_IDEMPOT] ]); 1739 1740(* another version with `g 0 = {}` *) 1741val SETS_TO_INCREASING_SETS' = store_thm 1742 ("SETS_TO_INCREASING_SETS'", 1743 ``!f :num -> 'a set. 1744 ?g. (g 0 = {}) /\ (!n. g n = BIGUNION (IMAGE f (count n))) /\ 1745 (!n. g n SUBSET g (SUC n)) /\ 1746 (BIGUNION (IMAGE f UNIV) = BIGUNION (IMAGE g UNIV))``, 1747 rpt STRIP_TAC 1748 >> Q.EXISTS_TAC `\n. BIGUNION (IMAGE f (count n))` 1749 >> BETA_TAC 1750 >> RW_TAC bool_ss [] 1751 >| [ (* goal 1 (of 3) *) 1752 REWRITE_TAC [COUNT_ZERO, IMAGE_EMPTY, BIGUNION_EMPTY], 1753 (* goal 2 (of 3) *) 1754 `count (SUC n) = n INSERT (count n)` by PROVE_TAC [COUNT_SUC] \\ 1755 POP_ORW >> REWRITE_TAC [IMAGE_INSERT, BIGUNION_INSERT] \\ 1756 REWRITE_TAC [SUBSET_UNION], 1757 (* goal 3 (of 3) *) 1758 REWRITE_TAC [EXTENSION] \\ 1759 GEN_TAC >> SIMP_TAC std_ss [IN_BIGUNION_IMAGE, IN_UNIV, IN_COUNT] \\ 1760 EQ_TAC >> RW_TAC std_ss [] >| 1761 [ Q.EXISTS_TAC `SUC x'` \\ 1762 Q.EXISTS_TAC `x'` >> ASM_SIMP_TAC arith_ss [], 1763 Q.EXISTS_TAC `x'` >> art [] ] ]); 1764 1765(* 2. (hard) for any sequence of sets in a space, there is a disjoint family with 1766 the same bigunion. This lemma is needed by DYNKIN_LEMMA *) 1767val SETS_TO_DISJOINT_SETS = store_thm 1768 ("SETS_TO_DISJOINT_SETS", 1769 ``!sp sts f. (!s. s IN sts ==> s SUBSET sp) /\ (!n. f n IN sts) ==> 1770 ?g. (g 0 = f 0) /\ 1771 (!n. 0 < n ==> (g n = f n INTER (BIGINTER (IMAGE (\i. sp DIFF f i) (count n))))) /\ 1772 (!i j :num. i <> j ==> DISJOINT (g i) (g j)) /\ 1773 (BIGUNION (IMAGE f UNIV) = BIGUNION (IMAGE g UNIV))``, 1774 rpt STRIP_TAC 1775 >> Q.EXISTS_TAC `\n. if n = 0:num then f n 1776 else f n INTER (BIGINTER (IMAGE (\i. sp DIFF f i) (count n)))` 1777 >> BETA_TAC >> SIMP_TAC arith_ss [] 1778 >> CONJ_TAC >> RW_TAC arith_ss [] 1779 >| [ (* goal 1 (of 4) 1780 `DISJOINT (f 0) (f j INTER BIGINTER (IMAGE (\i. sp DIFF f i) (count j)))` *) 1781 `0 IN (count j)` by PROVE_TAC [NOT_ZERO_LT_ZERO, IN_COUNT] \\ 1782 POP_ASSUM (MP_TAC o SYM o (MATCH_MP INSERT_DELETE)) \\ 1783 DISCH_THEN (ONCE_REWRITE_TAC o wrap) \\ 1784 REWRITE_TAC [IMAGE_INSERT, BIGINTER_INSERT] >> BETA_TAC \\ 1785 REWRITE_TAC [INTER_ASSOC] \\ 1786 `f j INTER (sp DIFF f 0) = (sp DIFF f 0) INTER f j` by PROVE_TAC [INTER_COMM] \\ 1787 POP_ASSUM (ONCE_REWRITE_TAC o wrap) \\ 1788 REWRITE_TAC [DIFF_INTER, DISJOINT_DIFF], 1789 (* goal 2 (of 4), 1790 `DISJOINT (f i INTER BIGINTER (IMAGE (\i. sp DIFF f i) (count i))) (f 0)` *) 1791 `0 IN (count i)` by PROVE_TAC [NOT_ZERO_LT_ZERO, IN_COUNT] \\ 1792 POP_ASSUM (MP_TAC o SYM o (MATCH_MP INSERT_DELETE)) \\ 1793 DISCH_THEN (ONCE_REWRITE_TAC o wrap) \\ 1794 REWRITE_TAC [IMAGE_INSERT, BIGINTER_INSERT] >> BETA_TAC \\ 1795 REWRITE_TAC [INTER_ASSOC] \\ 1796 `f i INTER (sp DIFF f 0) = (sp DIFF f 0) INTER f i` by PROVE_TAC [INTER_COMM] \\ 1797 POP_ASSUM (ONCE_REWRITE_TAC o wrap) \\ 1798 REWRITE_TAC [DIFF_INTER, DISJOINT_DIFF], 1799 (* goal 3 (of 4), 1800 `DISJOINT (f i INTER BIGINTER (IMAGE (\i. sp DIFF f i) (count i))) 1801 (f j INTER BIGINTER (IMAGE (\i. sp DIFF f i) (count j)))` *) 1802 STRIP_ASSUME_TAC (Q.SPECL [`i`, `j`] LESS_LESS_CASES) >| (* 2 subgoals *) 1803 [ (* goal 3.1 (of 2) *) 1804 ONCE_REWRITE_TAC [DISJOINT_SYM] \\ 1805 MATCH_MP_TAC DISJOINT_SUBSET \\ 1806 Q.EXISTS_TAC `f i` >> REWRITE_TAC [INTER_SUBSET] \\ 1807 `i IN (count j)` by PROVE_TAC [IN_COUNT] \\ 1808 POP_ASSUM (MP_TAC o SYM o (MATCH_MP INSERT_DELETE)) \\ 1809 DISCH_THEN (ONCE_REWRITE_TAC o wrap) \\ 1810 REWRITE_TAC [IMAGE_INSERT, BIGINTER_INSERT] >> BETA_TAC \\ 1811 REWRITE_TAC [INTER_ASSOC] \\ 1812 `f j INTER (sp DIFF f i) = (sp DIFF f i) INTER f j` by PROVE_TAC [INTER_COMM] \\ 1813 POP_ASSUM (ONCE_REWRITE_TAC o wrap) \\ 1814 REWRITE_TAC [DIFF_INTER, DISJOINT_DIFF], 1815 (* goal 3.2 (of 2) *) 1816 MATCH_MP_TAC DISJOINT_SUBSET \\ 1817 Q.EXISTS_TAC `f j` >> REWRITE_TAC [INTER_SUBSET] \\ 1818 `j IN (count i)` by PROVE_TAC [IN_COUNT] \\ 1819 POP_ASSUM (MP_TAC o SYM o (MATCH_MP INSERT_DELETE)) \\ 1820 DISCH_THEN (ONCE_REWRITE_TAC o wrap) \\ 1821 REWRITE_TAC [IMAGE_INSERT, BIGINTER_INSERT] >> BETA_TAC \\ 1822 REWRITE_TAC [INTER_ASSOC] \\ 1823 `f i INTER (sp DIFF f j) = (sp DIFF f j) INTER f i` by PROVE_TAC [INTER_COMM] \\ 1824 POP_ASSUM (ONCE_REWRITE_TAC o wrap) \\ 1825 REWRITE_TAC [DIFF_INTER, DISJOINT_DIFF] ], 1826 (* goal 4 (of 4) *) 1827 MATCH_MP_TAC BIGUNION_IMAGE_COUNT_IMP_UNIV \\ 1828 Induct_on `n` >- REWRITE_TAC [COUNT_ZERO, IMAGE_EMPTY, BIGUNION_EMPTY] \\ 1829 REWRITE_TAC [COUNT_SUC, IMAGE_INSERT, BIGUNION_INSERT] \\ 1830 POP_ASSUM (REWRITE_TAC o wrap) >> BETA_TAC \\ 1831 Cases_on `n = 0` >> fs [] (* now ``n <> 0`` *) \\ 1832 REWRITE_TAC [Once UNION_COMM, INTER_OVER_UNION] \\ 1833 GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) empty_rewrites [UNION_COMM] \\ 1834 Suff `BIGUNION (IMAGE f (count n)) UNION (BIGINTER (IMAGE (\i. sp DIFF f i) (count n))) = sp` 1835 >- (DISCH_THEN (REWRITE_TAC o wrap) \\ 1836 REWRITE_TAC [INTER_SUBSET_EQN, UNION_SUBSET] \\ 1837 reverse CONJ_TAC >- PROVE_TAC [] \\ 1838 REWRITE_TAC [BIGUNION_SUBSET, IN_IMAGE] >> PROVE_TAC []) \\ 1839 (* BIGUNION (IMAGE f (count n)) UNION BIGINTER (IMAGE (\i. sp DIFF f i) (count n)) = sp *) 1840 `0 < n` by PROVE_TAC [NOT_ZERO_LT_ZERO] \\ 1841 POP_ASSUM (REWRITE_TAC o wrap o GSYM o (MATCH_MP GEN_COMPL_FINITE_UNION)) \\ 1842 Suff `BIGUNION (IMAGE f (count n)) SUBSET sp` >- ASM_SET_TAC [] \\ 1843 REWRITE_TAC [BIGUNION_SUBSET, IN_IMAGE] >> PROVE_TAC [] ]); 1844 1845(* A specific version without sts and sp *) 1846val SETS_TO_DISJOINT_SETS' = store_thm 1847 ("SETS_TO_DISJOINT_SETS'", 1848 ``!f. ?g. (g 0 = f 0) /\ 1849 (!n. 0 < n ==> (g n = f n INTER (BIGINTER (IMAGE (COMPL o f) (count n))))) /\ 1850 (!i j :num. i <> j ==> DISJOINT (g i) (g j)) /\ 1851 (BIGUNION (IMAGE f UNIV) = BIGUNION (IMAGE g UNIV))``, 1852 GEN_TAC 1853 >> STRIP_ASSUME_TAC (Q.SPECL [`UNIV`, `UNIV`, `f`] SETS_TO_DISJOINT_SETS) 1854 >> fs [SUBSET_UNIV, o_DEF, COMPL_DEF] 1855 >> Q.EXISTS_TAC `g` >> art []); 1856 1857(* 3. (hard) for any sequence of (straightly) increasing sets, there is a disjoint 1858 family with the same bigunion. *) 1859val INCREASING_TO_DISJOINT_SETS = store_thm 1860 ("INCREASING_TO_DISJOINT_SETS", 1861 ``!f :num -> 'a set. (!n. f n SUBSET f (SUC n)) ==> 1862 ?g. (g 0 = f 0) /\ (!n. 0 < n ==> (g n = f n DIFF f (PRE n))) /\ 1863 (!i j :num. i <> j ==> DISJOINT (g i) (g j)) /\ 1864 (BIGUNION (IMAGE f UNIV) = BIGUNION (IMAGE g UNIV))``, 1865 rpt STRIP_TAC 1866 >> Q.EXISTS_TAC `\n. if n = (0 :num) then f n else f n DIFF f (PRE n)` 1867 >> BETA_TAC 1868 (* preliminaries *) 1869 >> Know `!n. 0 < n ==> f 0 SUBSET (f n)` 1870 >- (Induct_on `n` >- RW_TAC arith_ss [] \\ 1871 RW_TAC arith_ss [] \\ 1872 Cases_on `n = 0` >- art [] \\ 1873 IMP_RES_TAC NOT_ZERO_LT_ZERO >> RES_TAC \\ 1874 MATCH_MP_TAC SUBSET_TRANS >> Q.EXISTS_TAC `f n` >> art []) 1875 >> DISCH_TAC 1876 >> Know `!n. 0 < n ==> f 0 SUBSET (f (PRE n))` 1877 >- (Induct_on `n` >- RW_TAC arith_ss [] \\ 1878 RW_TAC arith_ss [] \\ 1879 Cases_on `n = 0` >- art [SUBSET_REFL] \\ 1880 IMP_RES_TAC NOT_ZERO_LT_ZERO >> RES_TAC) 1881 >> DISCH_TAC 1882 >> Know `!i j. i < j ==> f (SUC i) SUBSET (f j)` 1883 >- (GEN_TAC >> Induct_on `j` >- RW_TAC arith_ss [] \\ 1884 STRIP_TAC \\ 1885 fs [GSYM LESS_EQ_IFF_LESS_SUC, LESS_OR_EQ] \\ 1886 MATCH_MP_TAC SUBSET_TRANS >> Q.EXISTS_TAC `f j` \\ 1887 CONJ_TAC >- RES_TAC >> art []) 1888 >> DISCH_TAC 1889 >> Know `!n. 0 < n ==> f (PRE n) SUBSET f n` 1890 >- (rpt STRIP_TAC \\ 1891 Q.PAT_X_ASSUM `!n. f n SUBSET f (SUC n)` (STRIP_ASSUME_TAC o (Q.SPEC `PRE n`)) \\ 1892 PROVE_TAC [SUC_PRE]) 1893 >> DISCH_TAC 1894 >> Know `!i j. i < j ==> f i SUBSET f (PRE j)` 1895 >- (GEN_TAC >> Induct_on `j` >- RW_TAC arith_ss [] \\ 1896 STRIP_TAC \\ 1897 fs [GSYM LESS_EQ_IFF_LESS_SUC, LESS_OR_EQ] \\ 1898 MATCH_MP_TAC SUBSET_TRANS >> Q.EXISTS_TAC `f (PRE j)` \\ 1899 CONJ_TAC >- RES_TAC \\ 1900 Cases_on `j = 0` >- (RW_TAC arith_ss [SUBSET_REFL]) \\ 1901 IMP_RES_TAC NOT_ZERO_LT_ZERO >> RES_TAC) 1902 >> DISCH_TAC 1903 >> RW_TAC arith_ss [] 1904 >| [ (* goal 1 (of 4): DISJOINT (f 0) (f (SUC j) DIFF f j) *) 1905 MATCH_MP_TAC SUBSET_DIFF_DISJOINT \\ 1906 Q.EXISTS_TAC `f j` \\ 1907 IMP_RES_TAC NOT_ZERO_LT_ZERO \\ 1908 `f j DIFF (f j DIFF f (PRE j)) = f (PRE j)` 1909 by PROVE_TAC [DIFF_DIFF_SUBSET] >> POP_ORW >> RES_TAC, 1910 (* goal 2 (of 4): DISJOINT (f (SUC i) DIFF f i) (f 0) *) 1911 ONCE_REWRITE_TAC [DISJOINT_SYM] \\ 1912 MATCH_MP_TAC SUBSET_DIFF_DISJOINT \\ 1913 Q.EXISTS_TAC `f i` \\ 1914 IMP_RES_TAC NOT_ZERO_LT_ZERO \\ 1915 `f i DIFF (f i DIFF f (PRE i)) = f (PRE i)` 1916 by PROVE_TAC [DIFF_DIFF_SUBSET] >> POP_ORW \\ 1917 IMP_RES_TAC NOT_ZERO_LT_ZERO >> RES_TAC, 1918 (* goal 3 (of 4): DISJOINT (f (SUC i) DIFF f i) (f (SUC j) DIFF f j) *) 1919 STRIP_ASSUME_TAC (Q.SPECL [`i`, `j`] LESS_LESS_CASES) >| (* 2 subgoals *) 1920 [ (* goal 3.1 (of 2) *) 1921 ONCE_REWRITE_TAC [DISJOINT_SYM] \\ 1922 MATCH_MP_TAC DISJOINT_SUBSET \\ 1923 Q.EXISTS_TAC `f i` >> REWRITE_TAC [DIFF_SUBSET] \\ 1924 ONCE_REWRITE_TAC [DISJOINT_SYM] \\ 1925 MATCH_MP_TAC SUBSET_DIFF_DISJOINT \\ 1926 Q.EXISTS_TAC `f j` \\ 1927 IMP_RES_TAC NOT_ZERO_LT_ZERO \\ 1928 `f j DIFF (f j DIFF f (PRE j)) = f (PRE j)` 1929 by PROVE_TAC [DIFF_DIFF_SUBSET] >> POP_ORW >> RES_TAC, 1930 (* goal 3.2 (of 2) *) 1931 MATCH_MP_TAC DISJOINT_SUBSET \\ 1932 Q.EXISTS_TAC `f j` >> REWRITE_TAC [DIFF_SUBSET] \\ 1933 ONCE_REWRITE_TAC [DISJOINT_SYM] \\ 1934 MATCH_MP_TAC SUBSET_DIFF_DISJOINT \\ 1935 Q.EXISTS_TAC `f i` \\ 1936 IMP_RES_TAC NOT_ZERO_LT_ZERO \\ 1937 `f i DIFF (f i DIFF f (PRE i)) = f (PRE i)` 1938 by PROVE_TAC [DIFF_DIFF_SUBSET] >> POP_ORW >> RES_TAC ], 1939 (* goal 4 (of 4): BIGUNION (IMAGE f univ(:num)) = ... *) 1940 MATCH_MP_TAC BIGUNION_IMAGE_COUNT_IMP_UNIV \\ 1941 Induct_on `n` >- REWRITE_TAC [COUNT_ZERO, IMAGE_EMPTY, BIGUNION_EMPTY] \\ 1942 REWRITE_TAC [COUNT_SUC, IMAGE_INSERT, BIGUNION_INSERT] \\ 1943 POP_ASSUM (REWRITE_TAC o wrap) >> BETA_TAC \\ 1944 Cases_on `n = 0` >> fs [] (* now ``n <> 0`` *) \\ 1945 RW_TAC arith_ss [EXTENSION, IN_UNION, IN_BIGUNION_IMAGE, IN_COUNT, IN_DIFF] \\ 1946 EQ_TAC >> rpt STRIP_TAC >| (* 4 subgoals *) 1947 [ DISJ1_TAC >> art [], 1948 DISJ2_TAC >> Q.EXISTS_TAC `x'` >> art [], 1949 Cases_on `x IN f (PRE n)` >- (DISJ2_TAC >> Q.EXISTS_TAC `PRE n` \\ 1950 ASM_SIMP_TAC arith_ss []) \\ 1951 DISJ1_TAC >> art [], 1952 DISJ2_TAC >> Q.EXISTS_TAC `x'` >> art [] ] ]); 1953 1954(* Surprisingly, this variant of INCREASING_TO_DISJOINT_SETS cannot be 1955 easily proved without using the non-trivial SETS_TO_DISJOINT_SETS *) 1956val INCREASING_TO_DISJOINT_SETS' = store_thm 1957 ("INCREASING_TO_DISJOINT_SETS'", 1958 ``!f :num -> 'a set. (f 0 = {}) /\ (!n. f n SUBSET f (SUC n)) ==> 1959 ?g. (!n. g n = f (SUC n) DIFF f n) /\ 1960 (!i j :num. i <> j ==> DISJOINT (g i) (g j)) /\ 1961 (BIGUNION (IMAGE f UNIV) = BIGUNION (IMAGE g UNIV))``, 1962 rpt STRIP_TAC 1963 >> Q.EXISTS_TAC `\n. f (SUC n) DIFF f n` 1964 >> BETA_TAC 1965 (* preliminaries *) 1966 >> Know `!i j. i < j ==> f i SUBSET f j` 1967 >- (GEN_TAC >> Induct_on `j` >- RW_TAC arith_ss [] \\ 1968 STRIP_TAC \\ 1969 MATCH_MP_TAC SUBSET_TRANS >> Q.EXISTS_TAC `f j` >> art [] \\ 1970 fs [GSYM LESS_EQ_IFF_LESS_SUC, LESS_OR_EQ]) 1971 >> DISCH_TAC 1972 >> Know `!i j. i < j ==> f (SUC i) SUBSET f j` 1973 >- (GEN_TAC >> Induct_on `j` >- RW_TAC arith_ss [] \\ 1974 STRIP_TAC \\ 1975 Cases_on `i = j` >- PROVE_TAC [SUBSET_REFL] \\ 1976 MATCH_MP_TAC SUBSET_TRANS >> Q.EXISTS_TAC `f j` >> art [] \\ 1977 fs [GSYM LESS_EQ_IFF_LESS_SUC, LESS_OR_EQ]) 1978 >> DISCH_TAC 1979 >> RW_TAC arith_ss [] (* 2 subgoals *) 1980 >| [ (* goal 1 (of 2): DISJOINT (f (SUC i) DIFF f i) (f (SUC j) DIFF f j) *) 1981 STRIP_ASSUME_TAC (Q.SPECL [`i`, `j`] LESS_LESS_CASES) >| (* 2 subgoals *) 1982 [ (* goal 1.1 (of 2) *) 1983 ONCE_REWRITE_TAC [DISJOINT_SYM] \\ 1984 MATCH_MP_TAC DISJOINT_SUBSET \\ 1985 Q.EXISTS_TAC `f (SUC i)` >> REWRITE_TAC [DIFF_SUBSET] \\ 1986 ONCE_REWRITE_TAC [DISJOINT_SYM] \\ 1987 MATCH_MP_TAC SUBSET_DIFF_DISJOINT \\ 1988 Q.EXISTS_TAC `f (SUC j)` \\ 1989 `f (SUC j) DIFF (f (SUC j) DIFF f j) = f j` 1990 by PROVE_TAC [DIFF_DIFF_SUBSET] >> POP_ORW >> RES_TAC, 1991 (* goal 1.2 (of 2) *) 1992 MATCH_MP_TAC DISJOINT_SUBSET \\ 1993 Q.EXISTS_TAC `f (SUC j)` >> REWRITE_TAC [DIFF_SUBSET] \\ 1994 ONCE_REWRITE_TAC [DISJOINT_SYM] \\ 1995 MATCH_MP_TAC SUBSET_DIFF_DISJOINT \\ 1996 Q.EXISTS_TAC `f (SUC i)` \\ 1997 `f (SUC i) DIFF (f (SUC i) DIFF f i) = f i` 1998 by PROVE_TAC [DIFF_DIFF_SUBSET] >> POP_ORW >> RES_TAC ], 1999 (* goal 2 (of 2): BIGUNION (IMAGE f univ(:num)) = ... *) 2000 STRIP_ASSUME_TAC (Q.SPEC `f` SETS_TO_DISJOINT_SETS') >> art [] \\ 2001 RW_TAC std_ss [EXTENSION, IN_BIGUNION_IMAGE, IN_UNIV, IN_DIFF] \\ 2002 EQ_TAC >> rpt STRIP_TAC >| (* 2 subgoals *) 2003 [ (* goal 2.1 (of 2) *) 2004 Cases_on `x' = 0` >- PROVE_TAC [NOT_IN_EMPTY] \\ 2005 IMP_RES_TAC NOT_ZERO_LT_ZERO \\ 2006 Q.EXISTS_TAC `PRE x'` \\ 2007 `SUC (PRE x') = x'` by PROVE_TAC [SUC_PRE] >> POP_ORW \\ 2008 Q.PAT_X_ASSUM `x IN g x'` MP_TAC \\ 2009 Q.PAT_X_ASSUM `!n. 0 < n ==> X` 2010 (fn th => REWRITE_TAC [MATCH_MP th (ASSUME ``0:num < x'``)]) \\ 2011 RW_TAC std_ss [IN_INTER, IN_BIGINTER_IMAGE, IN_COUNT, o_DEF, IN_COMPL] \\ 2012 FIRST_X_ASSUM MATCH_MP_TAC >> RW_TAC arith_ss [], 2013 (* goal 2.2 (of 2) *) 2014 Q.EXISTS_TAC `SUC n` \\ 2015 `0 < SUC n` by REWRITE_TAC [prim_recTheory.LESS_0] \\ 2016 Q.PAT_X_ASSUM `!n. 0 < n ==> X` 2017 (fn th => REWRITE_TAC [MATCH_MP th (ASSUME ``0:num < SUC n``)]) \\ 2018 RW_TAC std_ss [IN_INTER, IN_BIGINTER_IMAGE, IN_COUNT, o_DEF, IN_COMPL] \\ 2019 fs [GSYM LESS_EQ_IFF_LESS_SUC, LESS_OR_EQ] \\ 2020 CCONTR_TAC >> fs [] \\ 2021 `x IN f n` by PROVE_TAC [SUBSET_DEF] ] ]); 2022 2023(* ------------------------------------------------------------------------- *) 2024(* Other types of disjointness definitions (from Concordia HVG) *) 2025(* ------------------------------------------------------------------------- *) 2026 2027(* This is not more general than disjoint_def *) 2028val disjoint_family_on = new_definition ("disjoint_family_on", 2029 ``disjoint_family_on a s = 2030 (!m n. m IN s /\ n IN s /\ (m <> n) ==> (a m INTER a n = {}))``); 2031 2032val disjoint_family = new_definition ("disjoint_family", 2033 ``disjoint_family A = disjoint_family_on A UNIV``); 2034 2035(* This is the way to convert a family of sets into a disjoint family *) 2036(* of sets, cf. SETS_TO_DISJOINT_SETS -- Chun Tian *) 2037val disjointed = new_definition ("disjointed", 2038 ``!A n. disjointed A n = 2039 A n DIFF BIGUNION {A i | i IN {x:num | 0 <= x /\ x < n}}``); 2040 2041val disjointed_subset = store_thm ("disjointed_subset", 2042 ``!A n. disjointed A n SUBSET A n``, 2043 RW_TAC std_ss [disjointed] THEN ASM_SET_TAC []); 2044 2045val disjoint_family_disjoint = store_thm ("disjoint_family_disjoint", 2046 ``!A. disjoint_family (disjointed A)``, 2047 SIMP_TAC std_ss [disjoint_family, disjoint_family_on, IN_UNIV] THEN 2048 RW_TAC std_ss [disjointed, EXTENSION, GSPECIFICATION, IN_INTER] THEN 2049 SIMP_TAC std_ss [NOT_IN_EMPTY, IN_DIFF, IN_BIGUNION] THEN 2050 ASM_CASES_TAC ``(x NOTIN A (m:num) \/ ?s. x IN s /\ s IN {A i | i < m})`` THEN 2051 ASM_REWRITE_TAC [] THEN RW_TAC std_ss [] THEN 2052 ASM_CASES_TAC ``x NOTIN A (n:num)`` THEN FULL_SIMP_TAC std_ss [] THEN 2053 FULL_SIMP_TAC std_ss [GSPECIFICATION] THEN 2054 ASM_CASES_TAC ``m < n:num`` THENL [METIS_TAC [], ALL_TAC] THEN 2055 `n < m:num` by ASM_SIMP_TAC arith_ss [] THEN METIS_TAC []); 2056 2057val finite_UN_disjointed_eq = prove ( 2058 ``!A n. BIGUNION {disjointed A i | i IN {x | 0 <= x /\ x < n}} = 2059 BIGUNION {A i | i IN {x | 0 <= x /\ x < n}}``, 2060 GEN_TAC THEN INDUCT_TAC THENL 2061 [FULL_SIMP_TAC real_ss [GSPECIFICATION] THEN SET_TAC [], ALL_TAC] THEN 2062 FULL_SIMP_TAC real_ss [GSPECIFICATION] THEN 2063 GEN_REWR_TAC (LAND_CONV o ONCE_DEPTH_CONV) 2064 [ARITH_PROVE ``i < SUC n <=> i < n \/ (i = n)``] THEN 2065 REWRITE_TAC [SET_RULE ``BIGUNION {(A:num->'a->bool) i | i < n \/ (i = n)} = 2066 BIGUNION {A i | i < n} UNION A n``] THEN 2067 ASM_REWRITE_TAC [disjointed] THEN SIMP_TAC std_ss [GSPECIFICATION] THEN 2068 SIMP_TAC std_ss [UNION_DEF] THEN 2069 REWRITE_TAC [ARITH_PROVE ``i < SUC n <=> i < n \/ (i = n)``] THEN 2070 REWRITE_TAC [SET_RULE ``BIGUNION {(A:num->'a->bool) i | i < n \/ (i = n)} = 2071 BIGUNION {A i | i < n} UNION A n``] THEN 2072 SET_TAC []); 2073 2074val atLeast0LessThan = prove ( 2075 ``{x:num | 0 <= x /\ x < n} = {x | x < n}``, 2076 SIMP_TAC arith_ss [EXTENSION, GSPECIFICATION]); 2077 2078val UN_UN_finite_eq = prove ( 2079 ``!A. 2080 BIGUNION {BIGUNION {A i | i IN {x | 0 <= x /\ x < n}} | n IN univ(:num)} = 2081 BIGUNION {A n | n IN UNIV}``, 2082 SIMP_TAC std_ss [atLeast0LessThan] THEN 2083 RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_BIGUNION, IN_UNIV] THEN 2084 EQ_TAC THEN RW_TAC std_ss [] THENL 2085 [POP_ASSUM (MP_TAC o Q.SPEC `x`) THEN ASM_REWRITE_TAC [] THEN 2086 RW_TAC std_ss [] THEN METIS_TAC [], ALL_TAC] THEN 2087 Q.EXISTS_TAC `BIGUNION {A i | i IN {x | 0 <= x /\ x < SUC n}}` THEN 2088 RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_BIGUNION, IN_UNIV] THENL 2089 [ALL_TAC, METIS_TAC []] THEN Q.EXISTS_TAC `A n` THEN 2090 FULL_SIMP_TAC std_ss [] THEN Q.EXISTS_TAC `n` THEN 2091 SIMP_TAC arith_ss []); 2092 2093val UN_finite_subset = prove ( 2094 ``!A C. (!n. BIGUNION {A i | i IN {x | 0 <= x /\ x < n}} SUBSET C) ==> 2095 BIGUNION {A n | n IN univ(:num)} SUBSET C``, 2096 RW_TAC std_ss [] THEN ONCE_REWRITE_TAC [GSYM UN_UN_finite_eq] THEN 2097 FULL_SIMP_TAC std_ss [SUBSET_DEF] THEN RW_TAC std_ss [] THEN 2098 FIRST_X_ASSUM MATCH_MP_TAC THEN 2099 FULL_SIMP_TAC std_ss [EXTENSION, GSPECIFICATION, IN_BIGUNION, IN_UNIV] THEN 2100 POP_ASSUM (MP_TAC o Q.SPEC `x`) THEN ASM_REWRITE_TAC [] THEN STRIP_TAC THEN 2101 Q.EXISTS_TAC `n` THEN Q.EXISTS_TAC `s'` THEN METIS_TAC []); 2102 2103val UN_finite2_subset = prove ( 2104 ``!A B n k. 2105 (!n. BIGUNION {A i | i IN {x | 0 <= x /\ x < n}} SUBSET 2106 BIGUNION {B i | i IN {x | 0 <= x /\ x < n + k}}) ==> 2107 BIGUNION {A n | n IN univ(:num)} SUBSET BIGUNION {B n | n IN univ(:num)}``, 2108 RW_TAC std_ss [] THEN MATCH_MP_TAC UN_finite_subset THEN 2109 ONCE_REWRITE_TAC [GSYM UN_UN_finite_eq] THEN 2110 FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_BIGUNION, GSPECIFICATION, IN_UNIV] THEN 2111 RW_TAC std_ss [] THEN FIRST_X_ASSUM (MP_TAC o Q.SPECL [`n`,`x`]) THEN 2112 Q_TAC SUFF_TAC `(?s. x IN s /\ ?i. (s = A i) /\ i < n)` THENL 2113 [ALL_TAC, METIS_TAC []] THEN DISCH_TAC THEN ASM_REWRITE_TAC [] THEN 2114 STRIP_TAC THEN Q.EXISTS_TAC `BIGUNION {B i | i < n + k}` THEN 2115 CONJ_TAC THENL [ALL_TAC, METIS_TAC []] THEN 2116 SIMP_TAC std_ss [IN_BIGUNION, GSPECIFICATION] THEN METIS_TAC []); 2117 2118val UN_finite2_eq = prove ( 2119 ``!A B k. 2120 (!n. BIGUNION {A i | i IN {x | 0 <= x /\ x < n}} = 2121 BIGUNION {B i | i IN {x | 0 <= x /\ x < n + k}}) ==> 2122 (BIGUNION {A n | n IN univ(:num)} = BIGUNION {B n | n IN univ(:num)})``, 2123 RW_TAC std_ss [] THEN MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL 2124 [MATCH_MP_TAC UN_finite2_subset THEN REWRITE_TAC [atLeast0LessThan] THEN 2125 METIS_TAC [SUBSET_REFL], ALL_TAC] THEN 2126 FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_BIGUNION, IN_UNIV, GSPECIFICATION] THEN 2127 RW_TAC std_ss [] THEN FIRST_X_ASSUM (MP_TAC o Q.SPEC `SUC n`) THEN 2128 GEN_REWR_TAC LAND_CONV [EXTENSION] THEN 2129 DISCH_THEN (MP_TAC o Q.SPEC `x`) THEN 2130 SIMP_TAC std_ss [SUBSET_DEF, IN_BIGUNION, IN_UNIV, GSPECIFICATION] THEN 2131 Q_TAC SUFF_TAC `?s. x IN s /\ ?i. (s = B i) /\ i < SUC n + k` THENL 2132 [ALL_TAC, 2133 Q.EXISTS_TAC `B n` THEN ASM_REWRITE_TAC [] THEN 2134 Q.EXISTS_TAC `n` THEN SIMP_TAC arith_ss []] THEN 2135 DISCH_TAC THEN ASM_REWRITE_TAC [] THEN RW_TAC std_ss [] THEN 2136 METIS_TAC []); 2137 2138Theorem BIGUNION_disjointed : (* was: UN_disjointed_eq *) 2139 !A. BIGUNION {disjointed A i | i IN UNIV} = BIGUNION {A i | i IN UNIV} 2140Proof 2141 GEN_TAC THEN MATCH_MP_TAC UN_finite2_eq THEN 2142 Q.EXISTS_TAC `0` THEN RW_TAC arith_ss [GSPECIFICATION] THEN 2143 ASSUME_TAC finite_UN_disjointed_eq THEN 2144 FULL_SIMP_TAC arith_ss [GSPECIFICATION] 2145QED 2146 2147(******************************************************************************) 2148(* liminf and limsup [1, p.74] [2, p.76] - the set-theoretic version *) 2149(******************************************************************************) 2150 2151(* this lemma is provided by Konrad Slind *) 2152val set_ss = arith_ss ++ PRED_SET_ss; 2153 2154val lemma = Q.prove 2155 (`!P. ~(?N. INFINITE N /\ !n. N n ==> P n) <=> !N. N SUBSET P ==> FINITE N`, 2156 rw_tac set_ss [EQ_IMP_THM, SUBSET_DEF, IN_DEF] 2157 >- (`FINITE P \/ ?n. P n /\ ~P n` by metis_tac [] 2158 >> imp_res_tac SUBSET_FINITE 2159 >> full_simp_tac std_ss [SUBSET_DEF, IN_DEF]) 2160 >- metis_tac[]); 2161 2162(* TODO: use above lemma to simplify this proof with the following hints: 2163 2164 "From this and the original assumption, you should be able to get that P is finite, 2165 so has a maximum element." -- Konrad Slind, Feb 17, 2019. 2166 *) 2167val infinitely_often_lemma = store_thm 2168 ("infinitely_often_lemma", 2169 ``!P. ~(?N. INFINITE N /\ !n:num. n IN N ==> P n) <=> ?m. !n. m <= n ==> ~(P n)``, 2170 GEN_TAC 2171 >> `!N. (!n. n IN N ==> P n) <=> N SUBSET P` by PROVE_TAC [SUBSET_DEF, IN_APP] 2172 >> ASM_REWRITE_TAC [] 2173 >> SIMP_TAC std_ss [] 2174 >> reverse EQ_TAC >> rpt STRIP_TAC 2175 >| [ (* goal 1 (of 2) *) 2176 Cases_on `~(N SUBSET P)` >- art [] >> fs [] \\ 2177 Suff `FINITE P` >- PROVE_TAC [SUBSET_FINITE_I] \\ 2178 Know `P SUBSET {n | ~(m <= n)}` 2179 >- (RW_TAC std_ss [SUBSET_DEF, GSPECIFICATION, IN_APP] \\ 2180 METIS_TAC []) \\ 2181 DISCH_TAC \\ 2182 Suff `FINITE {n | ~(m <= n)}` >- PROVE_TAC [SUBSET_FINITE_I] \\ 2183 REWRITE_TAC [FINITE_WEAK_ENUMERATE] \\ 2184 Q.EXISTS_TAC `I` \\ 2185 Q.EXISTS_TAC `m` \\ 2186 RW_TAC arith_ss [I_THM, GSPECIFICATION], 2187 (* goal 2 (of 2) *) 2188 POP_ASSUM (MP_TAC o (Q.SPEC `P`)) \\ 2189 RW_TAC std_ss [SUBSET_REFL] \\ 2190 IMP_RES_TAC finite_decomposition_simple \\ 2191 Q.EXISTS_TAC `SUC (MAX_SET P)` \\ 2192 Q.X_GEN_TAC `m` >> DISCH_TAC \\ 2193 CCONTR_TAC >> fs [EXTENSION, IN_IMAGE, IN_COUNT, IN_APP] \\ 2194 `P <> {}` by METIS_TAC [IN_APP, NOT_IN_EMPTY] \\ 2195 `!y. y IN P ==> y <= MAX_SET P` by PROVE_TAC [MAX_SET_DEF] \\ 2196 `m <= MAX_SET P` by PROVE_TAC [IN_APP] \\ 2197 `MAX_SET P < m` by RW_TAC arith_ss [] \\ 2198 FULL_SIMP_TAC arith_ss [] ]); 2199 2200(* this proof is provided by Konrad Slind, slightly shorter than mine. *) 2201val infinity_bound_lemma = store_thm 2202 ("infinity_bound_lemma", 2203 ``!N m. INFINITE N ==> ?n:num. m <= n /\ n IN N``, 2204 spose_not_then strip_assume_tac 2205 >> `FINITE (count m)` by metis_tac [FINITE_COUNT] 2206 >> `N SUBSET (count m)` 2207 by (rw_tac set_ss [SUBSET_DEF] 2208 >> `~(m <= x)` by metis_tac [] 2209 >> decide_tac) 2210 >> metis_tac [SUBSET_FINITE]); 2211 2212(* TODO: restate this lemma by real_topologyTheory.from *) 2213val tail_not_empty = store_thm 2214 ("tail_not_empty", ``!A m:num. {A n | m <= n} <> {}``, 2215 RW_TAC std_ss [Once EXTENSION, NOT_IN_EMPTY, GSPECIFICATION] 2216 >> Q.EXISTS_TAC `(SUC m)` >> RW_TAC arith_ss []); 2217 2218val tail_countable = store_thm 2219 ("tail_countable", ``!A m:num. countable {A n | m <= n}``, 2220 rpt GEN_TAC 2221 >> Suff `{A n | m <= n} = IMAGE A {n | m <= n}` 2222 >- PROVE_TAC [COUNTABLE_IMAGE_NUM] 2223 >> RW_TAC std_ss [EXTENSION, IN_IMAGE, GSPECIFICATION]); 2224 2225val _ = export_theory (); 2226 2227(* References: 2228 2229 [1] Schilling, R.L.: Measures, Integrals and Martingales. Cambridge University Press (2005). 2230 [2] Chung, K.L.: A Course in Probability Theory, Third Edition. Academic Press (2001). 2231 *) 2232