1(* interactive mode 2loadPath := ["../ho_prover","../subtypes","../rsa"] @ !loadPath; 3app load ["bossLib","realLib","transcTheory","subtypeTheory", 4 "formalizeUseful","extra_boolTheory", 5 "boolContext","extra_pred_setTools","sumTheory"]; 6 7open HolKernel Parse boolLib bossLib realTheory realLib 8 formalizeUseful subtypeTheory extra_numTheory transcTheory 9 pred_setTheory arithmeticTheory seqTheory combinTheory pairTheory 10 extra_pred_setTheory extra_boolTheory extra_pred_setTools 11 sumTheory; 12 13 14loadPath := ["../subtypes"] @ !loadPath; 15app load ["bossLib","realLib","transcTheory","subtypeTheory", 16 "formalizeUseful","extra_boolTheory", 17 "extra_pred_setTheory","sumTheory"]; 18 19quietdec := true; 20*) 21 22open HolKernel Parse boolLib bossLib realTheory realLib 23 formalizeUseful subtypeTheory extra_numTheory transcTheory 24 pred_setTheory arithmeticTheory seqTheory combinTheory pairTheory 25 extra_pred_setTheory extra_boolTheory real_sigmaTheory 26 sumTheory limTheory listTheory rich_listTheory; 27 28(* interactive mode 29quietdec := false; 30*) 31 32val _ = new_theory "extra_real"; 33 34(* ------------------------------------------------------------------------- *) 35(* Tools. *) 36(* ------------------------------------------------------------------------- *) 37 38val Reverse = Tactical.REVERSE; 39val REVERSE = Tactical.REVERSE; 40val Strip = rpt (POP_ASSUM MP_TAC) >> rpt STRIP_TAC; 41val Simplify = RW_TAC arith_ss; 42val Suff = PARSE_TAC SUFF_TAC; 43val Know = PARSE_TAC KNOW_TAC; 44val Rewr = DISCH_THEN (REWRITE_TAC o wrap); 45val Rewr' = DISCH_THEN (ONCE_REWRITE_TAC o wrap); 46val STRONG_DISJ_TAC = CONV_TAC (REWR_CONV (GSYM IMP_DISJ_THM)) >> STRIP_TAC; 47val Cond = 48 DISCH_THEN 49 (fn mp_th => 50 let 51 val cond = fst (dest_imp (concl mp_th)) 52 in 53 KNOW_TAC cond >| [ALL_TAC, DISCH_THEN (MP_TAC o MP mp_th)] 54 end); 55 56val POP_ORW = POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]); 57 58(* ------------------------------------------------------------------------- *) 59(* Definitions. *) 60(* ------------------------------------------------------------------------- *) 61 62val inf_def = Define `inf p = ~(sup (IMAGE $~ p))`; 63 64val zreal_def = Define `zreal (x : real) = (x = 0)`; 65val nzreal_def = Define `nzreal (x : real) = ~(x = 0)`; 66val posreal_def = Define `posreal (x : real) = 0 < x`; 67val nnegreal_def = Define `nnegreal (x : real) = 0 <= x`; 68val negreal_def = Define `negreal (x : real) = 0 < ~x`; 69val nposreal_def = Define `nposreal (x : real) = 0 <= ~x`; 70 71(* ------------------------------------------------------------------------- *) 72(* Theorems. *) 73(* ------------------------------------------------------------------------- *) 74 75val INF_DEF_ALT = store_thm 76 ("INF_DEF_ALT", 77 ``!p. inf p = ~(sup (\r. ~r IN p))``, 78 RW_TAC std_ss [] 79 >> PURE_REWRITE_TAC [inf_def, IMAGE_DEF] 80 >> Suff `{~x | x IN p} = (\r:real. ~r IN p)` 81 >- RW_TAC std_ss [] 82 >> RW_TAC std_ss [EXTENSION] 83 >> RW_TAC std_ss [GSPECIFICATION, SPECIFICATION] 84 >> PROVE_TAC [REAL_NEGNEG]); 85 86val REAL_LE_EQ = store_thm 87 ("REAL_LE_EQ", 88 ``!(x:real) y. x <= y /\ y <= x ==> (x = y)``, 89 REAL_ARITH_TAC); 90 91val REAL_SUP_EXISTS_UNIQUE = store_thm 92 ("REAL_SUP_EXISTS_UNIQUE", 93 ``!P. (?(x:real). P x) /\ (?z. !x. P x ==> x <= z) 94 ==> (?!s. !y. (?x. P x /\ y < x) = y < s)``, 95 REPEAT STRIP_TAC 96 >> CONV_TAC EXISTS_UNIQUE_CONV 97 >> RW_TAC std_ss [] >| 98 [ASSUME_TAC (SPEC ``P:real->bool`` REAL_SUP_LE) 99 >> PROVE_TAC [], 100 Suff `~((s:real) < s') /\ ~(s' < s)` 101 >- (KILL_TAC >> REAL_ARITH_TAC) 102 >> REPEAT STRIP_TAC >| 103 [Suff `!(x:real). P x ==> ~(s < x)` >- PROVE_TAC [] 104 >> REPEAT STRIP_TAC 105 >> Suff `~((s:real) < s)` >- PROVE_TAC [] 106 >> KILL_TAC 107 >> REAL_ARITH_TAC, 108 Suff `!(x:real). P x ==> ~(s' < x)` >- PROVE_TAC [] 109 >> REPEAT STRIP_TAC 110 >> Suff `~((s':real) < s')` >- PROVE_TAC [] 111 >> KILL_TAC 112 >> REAL_ARITH_TAC]]); 113 114val REAL_SUP_MAX = store_thm 115 ("REAL_SUP_MAX", 116 ``!P z. P z /\ (!x. P x ==> x <= z) ==> (sup P = z)``, 117 REPEAT STRIP_TAC 118 >> Know `!(y:real). (?x. P x /\ y < x) = y < z` 119 >- (STRIP_TAC 120 >> EQ_TAC >| 121 [REPEAT STRIP_TAC 122 >> PROVE_TAC [REAL_ARITH ``(y:real) < x /\ x <= z ==> y < z``], 123 PROVE_TAC []]) 124 >> STRIP_TAC 125 >> Know `!y. (?x. P x /\ y < x) = y < sup P` 126 >- PROVE_TAC [REAL_SUP_LE] 127 >> STRIP_TAC 128 >> Know `(?(x:real). P x) /\ (?z. !x. P x ==> x <= z)` 129 >- PROVE_TAC [] 130 >> STRIP_TAC 131 >> ASSUME_TAC ((SPEC ``P:real->bool`` o CONV_RULE 132 (DEPTH_CONV EXISTS_UNIQUE_CONV)) REAL_SUP_EXISTS_UNIQUE) 133 >> RES_TAC); 134 135val REAL_INF_MIN = store_thm 136 ("REAL_INF_MIN", 137 ``!p z. z IN p /\ (!x. x IN p ==> z <= x) ==> (inf p = z)``, 138 RW_TAC std_ss [SPECIFICATION] 139 >> MP_TAC (SPECL [``(\r. (p:real->bool) (~r))``, ``~(z:real)``] 140 REAL_SUP_MAX) 141 >> RW_TAC std_ss [REAL_NEGNEG, INF_DEF_ALT, SPECIFICATION] 142 >> Suff `!x. p ~x ==> x <= ~z` 143 >- PROVE_TAC [REAL_ARITH ``~~(x:real) = x``] 144 >> REPEAT STRIP_TAC 145 >> Suff `z <= ~x` >- (KILL_TAC >> REAL_ARITH_TAC) 146 >> PROVE_TAC []); 147 148val HALF_POS = store_thm 149 ("HALF_POS", 150 ``0 < 1/2``, 151 PROVE_TAC [REAL_ARITH ``0:real < 1``, REAL_LT_HALF1]); 152 153val HALF_CANCEL = store_thm 154 ("HALF_CANCEL", 155 ``2 * (1 / 2) = 1``, 156 Suff `2 * inv 2 = 1` >- PROVE_TAC [REAL_INV_1OVER] 157 >> PROVE_TAC [REAL_MUL_RINV, REAL_ARITH ``~(2:real = 0)``]); 158 159val POW_HALF_POS = store_thm 160 ("POW_HALF_POS", 161 ``!n. 0 < (1/2) pow n``, 162 STRIP_TAC 163 >> Cases_on `n` >- PROVE_TAC [REAL_ARITH ``0:real < 1``, pow] 164 >> PROVE_TAC [HALF_POS, POW_POS_LT]); 165 166val POW_HALF_MONO = store_thm 167 ("POW_HALF_MONO", 168 ``!m n. m <= n ==> (1/2) pow n <= (1/2) pow m``, 169 REPEAT STRIP_TAC 170 >> Induct_on `n` >| 171 [STRIP_TAC 172 >> Know `m:num = 0` >- DECIDE_TAC 173 >> PROVE_TAC [REAL_ARITH ``a:real <= a``], 174 Cases_on `m = SUC n` >- PROVE_TAC [REAL_ARITH ``a:real <= a``] 175 >> ONCE_REWRITE_TAC [pow] 176 >> STRIP_TAC 177 >> Know `m:num <= n` >- DECIDE_TAC 178 >> STRIP_TAC 179 >> Suff `2 * ((1/2) * (1/2) pow n) <= 2 * (1/2) pow m` 180 >- PROVE_TAC [REAL_ARITH ``0:real < 2``, REAL_LE_LMUL] 181 >> Suff `(1/2) pow n <= 2 * (1/2) pow m` 182 >- (KILL_TAC 183 >> PROVE_TAC [GSYM REAL_MUL_ASSOC, HALF_CANCEL, REAL_MUL_LID]) 184 >> PROVE_TAC [REAL_ARITH ``!x y. 0:real < x /\ x <= y ==> x <= 2 * y``, 185 POW_HALF_POS]]); 186 187val POW_HALF_TWICE = store_thm 188 ("POW_HALF_TWICE", 189 ``!n. (1 / 2) pow n = 2 * (1 / 2) pow (SUC n)``, 190 RW_TAC std_ss [pow, REAL_MUL_ASSOC] 191 >> PROVE_TAC [HALF_CANCEL, REAL_MUL_LID]); 192 193val X_HALF_HALF = store_thm 194 ("X_HALF_HALF", 195 ``!x. 1/2 * x + 1/2 * x = x``, 196 STRIP_TAC 197 >> MATCH_MP_TAC (REAL_ARITH ``(2 * (a:real) = 2 * b) ==> (a = b)``) 198 >> RW_TAC std_ss [REAL_ADD_LDISTRIB, REAL_MUL_ASSOC, HALF_CANCEL] 199 >> REAL_ARITH_TAC); 200 201val REAL_SUP_LE_X = store_thm 202 ("REAL_SUP_LE_X", 203 ``!P x. (?r. P r) /\ (!r. P r ==> r <= x) ==> sup P <= x``, 204 RW_TAC real_ss [] 205 >> Suff `~(x < sup P)` >- REAL_ARITH_TAC 206 >> STRIP_TAC 207 >> MP_TAC (SPEC ``P:real->bool`` REAL_SUP_LE) 208 >> RW_TAC real_ss [] >| 209 [PROVE_TAC [], 210 PROVE_TAC [], 211 EXISTS_TAC ``x:real`` 212 >> RW_TAC real_ss [] 213 >> PROVE_TAC [real_lte]]); 214 215val REAL_X_LE_SUP = store_thm 216 ("REAL_X_LE_SUP", 217 ``!P x. (?r. P r) /\ (?z. !r. P r ==> r <= z) /\ (?r. P r /\ x <= r) 218 ==> x <= sup P``, 219 RW_TAC real_ss [] 220 >> Suff `!y. P y ==> y <= sup P` >- PROVE_TAC [REAL_LE_TRANS] 221 >> MATCH_MP_TAC REAL_SUP_UBOUND_LE 222 >> PROVE_TAC []); 223 224val REAL_INVINV_ALL = store_thm 225 ("REAL_INVINV_ALL", 226 ``!x. inv (inv x) = x``, 227 STRIP_TAC 228 >> Reverse (Cases_on `x = 0`) >- RW_TAC std_ss [REAL_INVINV] 229 >> RW_TAC std_ss [REAL_INV_0]); 230 231val ABS_BETWEEN_LE = store_thm 232 ("ABS_BETWEEN_LE", 233 ``!x y d. 0 <= d /\ x - d <= y /\ y <= x + d = abs (y - x) <= d``, 234 RW_TAC std_ss [abs] >| 235 [EQ_TAC >- REAL_ARITH_TAC 236 >> STRIP_TAC 237 >> Know `0 <= d` >- PROVE_TAC [REAL_LE_TRANS] 238 >> STRIP_TAC 239 >> RW_TAC std_ss [] >| 240 [Suff `x <= y` 241 >- (POP_ASSUM MP_TAC >> KILL_TAC >> REAL_ARITH_TAC) 242 >> Q.PAT_ASSUM `0 <= y - x` MP_TAC 243 >> KILL_TAC 244 >> REAL_ARITH_TAC, 245 Q.PAT_ASSUM `y - x <= d` MP_TAC 246 >> KILL_TAC 247 >> REAL_ARITH_TAC], 248 EQ_TAC >- REAL_ARITH_TAC 249 >> Know `y - x <= 0` >- PROVE_TAC [REAL_NOT_LE, REAL_LT_LE] 250 >> STRIP_TAC 251 >> Know `~0 <= ~(y - x)` >- PROVE_TAC [REAL_LE_NEG] 252 >> KILL_TAC 253 >> REWRITE_TAC [REAL_NEG_SUB, REAL_NEG_0] 254 >> NTAC 2 STRIP_TAC 255 >> Know `0 <= d` >- PROVE_TAC [REAL_LE_TRANS] 256 >> STRIP_TAC 257 >> RW_TAC std_ss [] >| 258 [Q.PAT_ASSUM `x - y <= d` MP_TAC 259 >> KILL_TAC 260 >> REAL_ARITH_TAC, 261 Suff `y <= x` 262 >- (POP_ASSUM MP_TAC >> KILL_TAC >> REAL_ARITH_TAC) 263 >> Q.PAT_ASSUM `0 <= x - y` MP_TAC 264 >> KILL_TAC 265 >> REAL_ARITH_TAC]]); 266 267val ONE_MINUS_HALF = store_thm 268 ("ONE_MINUS_HALF", 269 ``1 - 1 / 2 = 1 / 2``, 270 MP_TAC (Q.SPEC `1` X_HALF_HALF) 271 >> RW_TAC real_ss [] 272 >> MATCH_MP_TAC (REAL_ARITH ``(x + 1 / 2 = y + 1 / 2) ==> (x = y)``) 273 >> RW_TAC std_ss [REAL_SUB_ADD]); 274 275val HALF_LT_1 = store_thm 276 ("HALF_LT_1", 277 ``1 / 2 < 1``, 278 ONCE_REWRITE_TAC [GSYM REAL_INV_1OVER, GSYM REAL_INV1] 279 >> MATCH_MP_TAC REAL_LT_INV 280 >> RW_TAC arith_ss [REAL_LT]); 281 282val REAL_POW = store_thm 283 ("REAL_POW", 284 ``!m n. &m pow n = &(m EXP n)``, 285 STRIP_TAC 286 >> Induct >- RW_TAC real_ss [pow, EXP] 287 >> RW_TAC real_ss [pow, EXP, REAL_MUL]); 288 289val POW_HALF_EXP = store_thm 290 ("POW_HALF_EXP", 291 ``!n. (1 / 2) pow n = inv (&(2 EXP n))``, 292 RW_TAC std_ss [GSYM REAL_POW, GSYM REAL_INV_1OVER] 293 >> ONCE_REWRITE_TAC [EQ_SYM_EQ] 294 >> MATCH_MP_TAC POW_INV 295 >> REAL_ARITH_TAC); 296 297val REAL_LE_INV_LE = store_thm 298 ("REAL_LE_INV_LE", 299 ``!x y. 0 < x /\ x <= y ==> inv y <= inv x``, 300 RW_TAC std_ss [] 301 >> Know `0 < inv x` >- PROVE_TAC [REAL_INV_POS] 302 >> STRIP_TAC 303 >> Suff `~(inv x < inv y)` >- PROVE_TAC [REAL_NOT_LT] 304 >> STRIP_TAC 305 >> Know `inv (inv y) < inv (inv x)` >- PROVE_TAC [REAL_LT_INV] 306 >> RW_TAC std_ss [REAL_INVINV_ALL, REAL_NOT_LT]); 307 308val INV_SUC_POS = store_thm 309 ("INV_SUC_POS", 310 ``!n. 0 < 1 / & (SUC n)``, 311 RW_TAC real_ss [GSYM REAL_INV_1OVER, REAL_LT_INV_EQ, REAL_LT]); 312 313val INV_SUC_MAX = store_thm 314 ("INV_SUC_MAX", 315 ``!n. 1 / & (SUC n) <= 1``, 316 REWRITE_TAC [GSYM REAL_INV_1OVER] 317 >> Induct 318 >- RW_TAC std_ss [GSYM ONE, REAL_INV1, REAL_LE_REFL] 319 >> Suff `inv (& (SUC (SUC n))) <= inv (& (SUC n))` 320 >- PROVE_TAC [REAL_LE_TRANS] 321 >> Suff `inv (& (SUC (SUC n))) < inv (& (SUC n))` >- REAL_ARITH_TAC 322 >> MATCH_MP_TAC REAL_LT_INV 323 >> RW_TAC arith_ss [REAL_LT]); 324 325val INV_SUC = store_thm 326 ("INV_SUC", 327 ``!n. 0 < 1 / & (SUC n) /\ 1 / & (SUC n) <= 1``, 328 PROVE_TAC [INV_SUC_POS, INV_SUC_MAX]) 329 330val ABS_UNIT_INTERVAL = store_thm 331 ("ABS_UNIT_INTERVAL", 332 ``!x y. 0 <= x /\ x <= 1 /\ 0 <= y /\ y <= 1 ==> abs (x - y) <= 1``, 333 REAL_ARITH_TAC); 334 335val REAL_LE_LT_MUL = store_thm 336 ("REAL_LE_LT_MUL", 337 ``!x y : real. 0 <= x /\ 0 < y ==> 0 <= x * y``, 338 rpt STRIP_TAC 339 >> MP_TAC (Q.SPECL [`0`, `x`, `y`] REAL_LE_RMUL) 340 >> RW_TAC std_ss [REAL_MUL_LZERO]); 341 342val REAL_LT_LE_MUL = store_thm 343 ("REAL_LT_LE_MUL", 344 ``!x y : real. 0 < x /\ 0 <= y ==> 0 <= x * y``, 345 PROVE_TAC [REAL_LE_LT_MUL, REAL_MUL_SYM]); 346 347val REAL_INV_NEG = store_thm 348 ("REAL_INV_NEG", 349 ``!x. 0 < ~x ==> 0 < ~inv x``, 350 rpt STRIP_TAC 351 >> Know `~(x = 0)` >- (POP_ASSUM MP_TAC >> REAL_ARITH_TAC) 352 >> RW_TAC std_ss [REAL_NEG_INV] 353 >> PROVE_TAC [REAL_INV_POS]); 354 355val IN_ZREAL = store_thm 356 ("IN_ZREAL", 357 ``!x. x IN zreal = (x = 0)``, 358 RW_TAC std_ss [zreal_def, SPECIFICATION]); 359 360val IN_NZREAL = store_thm 361 ("IN_NZREAL", 362 ``!x. x IN nzreal = ~(x = 0)``, 363 RW_TAC std_ss [nzreal_def, SPECIFICATION]); 364 365val IN_POSREAL = store_thm 366 ("IN_POSREAL", 367 ``!x. x IN posreal = 0 < x``, 368 RW_TAC std_ss [posreal_def, SPECIFICATION]); 369 370val IN_NNEGREAL = store_thm 371 ("IN_NNEGREAL", 372 ``!x. x IN nnegreal = 0 <= x``, 373 RW_TAC std_ss [nnegreal_def, SPECIFICATION]); 374 375val IN_NEGREAL = store_thm 376 ("IN_NEGREAL", 377 ``!x. x IN negreal = 0 < ~x``, 378 RW_TAC std_ss [negreal_def, SPECIFICATION]); 379 380val IN_NPOSREAL = store_thm 381 ("IN_NPOSREAL", 382 ``!x. x IN nposreal = 0 <= ~x``, 383 RW_TAC std_ss [nposreal_def, SPECIFICATION]); 384 385val POSREAL_ALT = store_thm 386 ("POSREAL_ALT", 387 ``posreal = nnegreal INTER nzreal``, 388 RW_TAC std_ss [SET_EQ, IN_INTER, IN_POSREAL, IN_NNEGREAL, IN_NZREAL] 389 >> REAL_ARITH_TAC); 390 391val NEGREAL_ALT = store_thm 392 ("NEGREAL_ALT", 393 ``negreal = nposreal INTER nzreal``, 394 RW_TAC std_ss [SET_EQ, IN_INTER, IN_NEGREAL, IN_NPOSREAL, IN_NZREAL] 395 >> REAL_ARITH_TAC); 396 397val REAL_ZERO_SUBTYPE = store_thm 398 ("REAL_ZERO_SUBTYPE", 399 ``0 IN zreal``, 400 RW_TAC std_ss [IN_ZREAL, SPECIFICATION]); 401 402val REAL_OF_NUM_SUBTYPE = store_thm 403 ("REAL_OF_NUM_SUBTYPE", 404 ``real_of_num IN ((UNIV -> nnegreal) INTER (gtnum 0 -> posreal))``, 405 RW_TAC std_ss [IN_INTER, IN_FUNSET, IN_NNEGREAL, REAL_POS, IN_GTNUM, 406 IN_ZREAL, IN_POSREAL] 407 >> Suff `~(& x = 0)` 408 >- (Know `0 <= & x` >- RW_TAC std_ss [REAL_POS] 409 >> REAL_ARITH_TAC) 410 >> Cases_on `x` >- DECIDE_TAC 411 >> RW_TAC std_ss [REAL] 412 >> Know `0 <= & n` >- RW_TAC std_ss [REAL_POS] 413 >> REAL_ARITH_TAC); 414 415val NEG_SUBTYPE = store_thm 416 ("NEG_SUBTYPE", 417 ``real_neg IN 418 ((negreal -> posreal) INTER (posreal -> negreal) INTER 419 (nnegreal -> nposreal) INTER (nposreal -> nnegreal) INTER 420 (nzreal -> nzreal) INTER (zreal -> zreal))``, 421 RW_TAC std_ss [IN_FUNSET, IN_NEGREAL, IN_POSREAL, IN_INTER, 422 IN_NPOSREAL, IN_NNEGREAL, IN_NZREAL, IN_ZREAL] 423 >> TRY (POP_ASSUM MP_TAC) 424 >> REAL_ARITH_TAC); 425 426val INV_SUBTYPE = store_thm 427 ("INV_SUBTYPE", 428 ``inv IN 429 ((nzreal -> nzreal) INTER (posreal -> posreal) INTER 430 (negreal -> negreal))``, 431 RW_TAC std_ss [IN_NZREAL, REAL_INV_NZ, IN_FUNSET, IN_INTER, IN_POSREAL, 432 IN_NEGREAL, REAL_INV_POS, REAL_INV_NEG] 433 >> REAL_ARITH_TAC); 434 435val SQRT_SUBTYPE = store_thm 436 ("SQRT_SUBTYPE", 437 ``sqrt IN ((nnegreal -> nnegreal) INTER (posreal -> posreal))``, 438 RW_TAC std_ss [IN_INTER, IN_FUNSET, IN_NNEGREAL, SQRT_POS_LE, IN_POSREAL, 439 SQRT_POS_LT]); 440 441val REAL_ADD_SUBTYPE = store_thm 442 ("REAL_ADD_SUBTYPE", 443 ``!x. $+ IN ((posreal -> nnegreal -> posreal) INTER 444 (nnegreal -> posreal -> posreal) INTER 445 (nnegreal -> nnegreal -> nnegreal) INTER 446 (negreal -> nposreal -> negreal) INTER 447 (nposreal -> negreal -> negreal) INTER 448 (nposreal -> nposreal -> nposreal) INTER 449 (zreal -> x -> x) INTER 450 (x -> zreal -> x))``, 451 RW_TAC std_ss [IN_FUNSET, IN_NEGREAL, IN_POSREAL, IN_INTER, 452 IN_NPOSREAL, IN_NNEGREAL, IN_NZREAL, IN_ZREAL] 453 >> REPEAT (POP_ASSUM MP_TAC) 454 >> REAL_ARITH_TAC); 455 456val REAL_SUB_SUBTYPE = store_thm 457 ("REAL_SUB_SUBTYPE", 458 ``!x. $- IN ((posreal -> nposreal -> posreal) INTER 459 (nnegreal -> negreal -> posreal) INTER 460 (nnegreal -> nposreal -> nnegreal) INTER 461 (negreal -> nnegreal -> negreal) INTER 462 (nposreal -> posreal -> negreal) INTER 463 (nposreal -> nnegreal -> nposreal) INTER 464 (x -> zreal -> x))``, 465 RW_TAC std_ss [IN_FUNSET, IN_NEGREAL, IN_POSREAL, IN_INTER, 466 IN_NPOSREAL, IN_NNEGREAL, IN_NZREAL, IN_ZREAL, 467 REAL_SUB_RZERO] 468 >> REPEAT (POP_ASSUM MP_TAC) 469 >> REAL_ARITH_TAC); 470 471val REAL_MULT_SUBTYPE = store_thm 472 ("REAL_MULT_SUBTYPE", 473 ``$* IN ((posreal -> nnegreal -> nnegreal) INTER 474 (nnegreal -> posreal -> nnegreal) INTER 475 (posreal -> posreal -> posreal) INTER 476 (negreal -> nposreal -> nnegreal) INTER 477 (nposreal -> negreal -> nnegreal) INTER 478 (negreal -> negreal -> posreal) INTER 479 (posreal -> nposreal -> nposreal) INTER 480 (nnegreal -> negreal -> nposreal) INTER 481 (posreal -> negreal -> negreal) INTER 482 (negreal -> nnegreal -> nposreal) INTER 483 (nposreal -> posreal -> nposreal) INTER 484 (negreal -> posreal -> negreal) INTER 485 (zreal -> UNIV -> zreal) INTER 486 (UNIV -> zreal -> zreal) INTER 487 (nzreal -> nzreal -> nzreal))``, 488 RW_TAC std_ss [IN_FUNSET, IN_NEGREAL, IN_POSREAL, IN_INTER, 489 IN_NPOSREAL, IN_NNEGREAL, IN_NZREAL, IN_ZREAL, 490 REAL_ENTIRE, IN_UNIV] 491 >> PROVE_TAC [REAL_LE_MUL, REAL_LT_MUL, REAL_NEGNEG, REAL_MUL_LNEG, 492 REAL_MUL_RNEG, REAL_LE_LT_MUL, REAL_LT_LE_MUL]); 493 494val REAL_DIV_SUBTYPE = store_thm 495 ("REAL_DIV_SUBTYPE", 496 ``$/ IN ((nnegreal -> posreal -> nnegreal) INTER 497 (posreal -> posreal -> posreal) INTER 498 (nposreal -> negreal -> nnegreal) INTER 499 (negreal -> negreal -> posreal) INTER 500 (nnegreal -> negreal -> nposreal) INTER 501 (posreal -> negreal -> negreal) INTER 502 (nposreal -> posreal -> nposreal) INTER 503 (negreal -> posreal -> negreal) INTER 504 (zreal -> nzreal -> zreal) INTER 505 (nzreal -> nzreal -> nzreal))``, 506 MP_TAC INV_SUBTYPE 507 >> MP_TAC REAL_MULT_SUBTYPE 508 >> RW_TAC std_ss [IN_FUNSET, IN_INTER, real_div, IN_UNIV]); 509 510val REAL_MULT_EQ_CANCEL = store_thm 511 ("REAL_MULT_EQ_CANCEL", 512 ``!x y z : real. ~(x = 0) ==> ((x * y = z) = (y = inv x * z))``, 513 Strip 514 >> Suff `(x * y = z) = (x = 0) \/ (y = inv x * z)` >- PROVE_TAC [] 515 >> REWRITE_TAC [GSYM REAL_EQ_MUL_LCANCEL] 516 >> RW_TAC std_ss [REAL_MUL_ASSOC, REAL_MUL_RINV] 517 >> RW_TAC real_ss []); 518 519val REAL_MULT_LE_CANCEL = store_thm 520 ("REAL_MULT_LE_CANCEL", 521 ``!x y z : real. 0 < x ==> ((x * y <= z) = (y <= inv x * z))``, 522 Strip 523 >> Suff `(x * y <= z) = (x * y <= x * (inv x * z))` 524 >- PROVE_TAC [REAL_LE_LMUL] 525 >> RW_TAC std_ss [REAL_MUL_ASSOC, REAL_MUL_RINV, REAL_LT_IMP_NE] 526 >> RW_TAC real_ss []); 527 528val INV_DIFF_SUC = store_thm 529 ("INV_DIFF_SUC", 530 ``!n : num. 0 < n ==> (1 / &n - 1 / (&n + 1) = 1 / &(n * (n + 1)))``, 531 RW_TAC std_ss [GSYM REAL_INV_1OVER] 532 >> Know `~(&n = 0) /\ ~(&n + 1 = 0)` 533 >- RW_TAC arith_ss [REAL_LT_NZ, REAL_NZ_IMP_LT, GSYM REAL] 534 >> RW_TAC std_ss [REAL_SUB_INV2] 535 >> Know `&n + 1 - &n = 1` >- REAL_ARITH_TAC 536 >> RW_TAC std_ss [GSYM REAL_INV_1OVER] 537 >> RW_TAC std_ss [GSYM REAL, REAL_MUL, GSYM ADD1]); 538 539val SUMS_EQ = store_thm 540 ("SUMS_EQ", 541 ``!f x. f sums x = summable f /\ (suminf f = x)``, 542 PROVE_TAC [SUM_SUMMABLE, SUM_UNIQ, summable]); 543 544val SER_POS = store_thm 545 ("SER_POS", 546 ``!f. summable f /\ (!n. 0 <= f n) ==> 0 <= suminf f``, 547 RW_TAC std_ss [] 548 >> MP_TAC (Q.SPECL [`f`, `0`] SER_POS_LE) 549 >> RW_TAC std_ss [sum]); 550 551val SER_POS_MONO = store_thm 552 ("SER_POS_MONO", 553 ``!f. (!n. 0 <= f n) ==> mono (\n. sum (0, n) f)``, 554 RW_TAC std_ss [mono] 555 >> DISJ1_TAC 556 >> HO_MATCH_MP_TAC TRIANGLE_2D_NUM 557 >> Induct >- RW_TAC arith_ss [REAL_LE_REFL] 558 >> RW_TAC std_ss [ADD_CLAUSES] 559 >> MATCH_MP_TAC REAL_LE_TRANS 560 >> Q.EXISTS_TAC `sum (0, d + n) f` 561 >> RW_TAC real_ss [sum] 562 >> Q.PAT_ASSUM `!n. 0 <= f n` (MP_TAC o Q.SPEC `d + n`) 563 >> REAL_ARITH_TAC); 564 565val POS_SUMMABLE = store_thm 566 ("POS_SUMMABLE", 567 ``!f. (!n. 0 <= f n) /\ (?x. !n. sum (0, n) f <= x) ==> summable f``, 568 RW_TAC std_ss [summable, sums, GSYM convergent] 569 >> MATCH_MP_TAC SEQ_BCONV 570 >> RW_TAC std_ss [SER_POS_MONO, netsTheory.MR1_BOUNDED] 571 >> Q.EXISTS_TAC `x + 1` 572 >> Q.EXISTS_TAC `N` 573 >> RW_TAC arith_ss [] 574 >> RW_TAC std_ss [abs, SUM_POS] 575 >> Q.PAT_ASSUM `!n. P n` (MP_TAC o Q.SPEC `n`) 576 >> REAL_ARITH_TAC); 577 578val SUMMABLE_LE = store_thm 579 ("SUMMABLE_LE", 580 ``!f x. summable f /\ (!n. sum (0, n) f <= x) ==> suminf f <= x``, 581 Strip 582 >> Suff `0 < suminf f - x ==> F` >- REAL_ARITH_TAC 583 >> Strip 584 >> Know `(\n. sum (0, n) f) --> suminf f` 585 >- RW_TAC std_ss [GSYM sums, SUMMABLE_SUM] 586 >> RW_TAC std_ss [SEQ] 587 >> Q.EXISTS_TAC `suminf f - x` 588 >> RW_TAC std_ss [] 589 >> Q.EXISTS_TAC `N` 590 >> Q.PAT_X_ASSUM `!n. P n` (MP_TAC o Q.SPEC `N`) 591 >> RW_TAC real_ss [] 592 >> ONCE_REWRITE_TAC [ABS_SUB] 593 >> Know `0 <= suminf f - sum (0, N) f` 594 >- (rpt (POP_ASSUM MP_TAC) 595 >> REAL_ARITH_TAC) 596 >> RW_TAC std_ss [abs] 597 >> rpt (POP_ASSUM MP_TAC) 598 >> REAL_ARITH_TAC); 599 600val LE_INF = store_thm 601 ("LE_INF", 602 ``!p r. (?x. x IN p) /\ (!x. x IN p ==> r <= x) ==> r <= inf p``, 603 RW_TAC std_ss [INF_DEF_ALT, SPECIFICATION] 604 >> POP_ASSUM MP_TAC 605 >> ONCE_REWRITE_TAC [GSYM REAL_NEGNEG] 606 >> Q.SPEC_TAC (`~r`, `r`) 607 >> RW_TAC real_ss [REAL_NEGNEG, REAL_LE_NEG] 608 >> MATCH_MP_TAC REAL_SUP_LE_X 609 >> RW_TAC std_ss [] 610 >> PROVE_TAC [REAL_NEGNEG]); 611 612val INF_LE = store_thm 613 ("INF_LE", 614 ``!p r. 615 (?z. !x. x IN p ==> z <= x) /\ (?x. x IN p /\ x <= r) ==> inf p <= r``, 616 RW_TAC std_ss [INF_DEF_ALT, SPECIFICATION] 617 >> POP_ASSUM MP_TAC 618 >> ONCE_REWRITE_TAC [GSYM REAL_NEGNEG] 619 >> Q.SPEC_TAC (`~r`, `r`) 620 >> RW_TAC real_ss [REAL_NEGNEG, REAL_LE_NEG] 621 >> MATCH_MP_TAC REAL_X_LE_SUP 622 >> RW_TAC std_ss [] 623 >> PROVE_TAC [REAL_NEGNEG, REAL_LE_NEG]); 624 625val REAL_LE_EPSILON = store_thm 626 ("REAL_LE_EPSILON", 627 ``!x y : real. (!e. 0 < e ==> x <= y + e) ==> x <= y``, 628 RW_TAC std_ss [] 629 >> Suff `~(0 < x - y)` >- REAL_ARITH_TAC 630 >> STRIP_TAC 631 >> Q.PAT_X_ASSUM `!e. P e` MP_TAC 632 >> RW_TAC std_ss [] 633 >> Know `!a b c : real. ~(a <= b + c) = c < a - b` >- REAL_ARITH_TAC 634 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 635 >> PROVE_TAC [REAL_DOWN]); 636 637val SER_POS_COMPARE = store_thm 638 ("SER_POS_COMPARE", 639 ``!f g. 640 (!n. 0 <= f n) /\ summable g /\ (!n. f n <= g n) ==> 641 summable f /\ suminf f <= suminf g``, 642 Reverse (rpt (STRONG_CONJ_TAC ORELSE STRIP_TAC)) 643 >- PROVE_TAC [SER_LE] 644 >> MATCH_MP_TAC SER_COMPAR 645 >> Q.EXISTS_TAC `g` 646 >> RW_TAC std_ss [] 647 >> Q.EXISTS_TAC `0` 648 >> RW_TAC arith_ss [abs]); 649 650val INF_GREATER = store_thm 651 ("INF_GREATER", 652 ``!p z. 653 (?x. x IN p) /\ inf p < z ==> 654 (?x. x IN p /\ x < z)``, 655 RW_TAC std_ss [] 656 >> Suff `~(!x. x IN p ==> ~(x < z))` >- PROVE_TAC [] 657 >> REWRITE_TAC [GSYM real_lte] 658 >> STRIP_TAC 659 >> Q.PAT_X_ASSUM `inf p < z` MP_TAC 660 >> RW_TAC std_ss [GSYM real_lte] 661 >> MATCH_MP_TAC LE_INF 662 >> PROVE_TAC []); 663 664val INF_CLOSE = store_thm 665 ("INF_CLOSE", 666 ``!p e. 667 (?x. x IN p) /\ 0 < e ==> (?x. x IN p /\ x < inf p + e)``, 668 RW_TAC std_ss [] 669 >> MATCH_MP_TAC INF_GREATER 670 >> CONJ_TAC >- PROVE_TAC [] 671 >> POP_ASSUM MP_TAC 672 >> REAL_ARITH_TAC); 673 674val SUMINF_POS = store_thm 675 ("SUMINF_POS", 676 ``!f. (!n. 0 <= f n) /\ summable f ==> 0 <= suminf f``, 677 RW_TAC std_ss [] 678 >> Know `0 = sum (0, 0) f` >- RW_TAC std_ss [sum] 679 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 680 >> MATCH_MP_TAC SER_POS_LE 681 >> RW_TAC std_ss []); 682 683val POW_HALF_SER = store_thm 684 ("POW_HALF_SER", 685 ``(\n. (1 / 2) pow (n + 1)) sums 1``, 686 Know `(\n. (1 / 2) pow n) sums inv (1 - (1 / 2))` 687 >- (MATCH_MP_TAC GP 688 >> RW_TAC std_ss [abs, HALF_POS, REAL_LT_IMP_LE, HALF_LT_1]) 689 >> RW_TAC std_ss [ONE_MINUS_HALF, REAL_INV_INV, GSYM REAL_INV_1OVER, 690 GSYM ADD1, pow] 691 >> Know `1 = inv 2 * 2` 692 >- RW_TAC arith_ss [REAL_MUL_LINV, REAL_INJ] 693 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 694 >> HO_MATCH_MP_TAC SER_CMUL 695 >> RW_TAC std_ss []); 696 697val SUMINF_ADD = store_thm 698 ("SUMINF_ADD", 699 ``!f g. 700 summable f /\ summable g ==> 701 summable (\n. f n + g n) /\ 702 (suminf f + suminf g = suminf (\n. f n + g n))``, 703 RW_TAC std_ss [] \\ 704 ( Know `f sums suminf f /\ g sums suminf g` >- PROVE_TAC [SUMMABLE_SUM] 705 >> STRIP_TAC 706 >> Know `(\n. f n + g n) sums (suminf f + suminf g)` 707 >- RW_TAC std_ss [SER_ADD] 708 >> RW_TAC std_ss [SUMS_EQ] )); 709 710val ABS_TRIANGLE = store_thm 711 ("ABS_TRIANGLE", 712 ``!x y z. abs (x - z) <= abs (x - y) + abs (y - z)``, 713 RW_TAC std_ss [abs] 714 >> rpt (POP_ASSUM MP_TAC) 715 >> REAL_ARITH_TAC); 716 717val ABS_TRANS = store_thm 718 ("ABS_TRANS", 719 ``!x y z e. abs (x - y) + abs (y - z) < e ==> abs (x - z) < e``, 720 rpt GEN_TAC 721 >> MP_TAC (Q.SPECL [`x`, `y`, `z`] ABS_TRIANGLE) 722 >> REAL_ARITH_TAC); 723 724val INCREASING_SEQ = store_thm 725 ("INCREASING_SEQ", 726 ``!f l. 727 (!n. f n <= f (SUC n)) /\ 728 (!n. f n <= l) /\ 729 (!e. 0 < e ==> ?n. l < f n + e) ==> 730 f --> l``, 731 RW_TAC std_ss [SEQ, GREATER_EQ] 732 >> Q.PAT_X_ASSUM `!e. P e` (MP_TAC o Q.SPEC `e`) 733 >> RW_TAC std_ss [] 734 >> Q.EXISTS_TAC `n` 735 >> ONCE_REWRITE_TAC [ABS_SUB] 736 >> Reverse (RW_TAC std_ss [abs]) 737 >- (Q.PAT_X_ASSUM `~x` MP_TAC 738 >> Q.PAT_X_ASSUM `!n. P n` (MP_TAC o Q.SPEC `n'`) 739 >> REAL_ARITH_TAC) 740 >> Know `?d. n' = n + d` >- PROVE_TAC [LESS_EQ_EXISTS] 741 >> RW_TAC std_ss [] 742 >> Suff `l < f (n + d) + e` >- REAL_ARITH_TAC 743 >> NTAC 2 (POP_ASSUM K_TAC) 744 >> Induct_on `d` >- RW_TAC arith_ss [] 745 >> RW_TAC std_ss [ADD_CLAUSES] 746 >> Q.PAT_X_ASSUM `!n. f n <= f (SUC n)` (MP_TAC o Q.SPEC `n + d`) 747 >> POP_ASSUM MP_TAC 748 >> REAL_ARITH_TAC); 749 750val SUM_PICK = store_thm 751 ("SUM_PICK", 752 ``!n k x. sum (0, n) (\m. if m = k then x else 0) = if k < n then x else 0``, 753 Induct >- RW_TAC arith_ss [sum] 754 >> RW_TAC arith_ss [sum, REAL_ADD_RID, REAL_ADD_LID] 755 >> Suff `F` >- PROVE_TAC [] 756 >> NTAC 2 (POP_ASSUM MP_TAC) 757 >> DECIDE_TAC); 758 759val SUM_LT = store_thm 760 ("SUM_LT", 761 ``!f g m n. 762 (!r. m <= r /\ r < n + m ==> f r < g r) /\ 0 < n ==> 763 sum (m,n) f < sum (m,n) g``, 764 RW_TAC std_ss [] 765 >> POP_ASSUM MP_TAC 766 >> Cases_on `n` >- RW_TAC arith_ss [] 767 >> RW_TAC arith_ss [] 768 >> Induct_on `n'` >- RW_TAC arith_ss [sum, REAL_ADD_LID] 769 >> ONCE_REWRITE_TAC [sum] 770 >> Strip 771 >> MATCH_MP_TAC REAL_LT_ADD2 772 >> CONJ_TAC 773 >- (Q.PAT_X_ASSUM `a ==> b` MATCH_MP_TAC 774 >> RW_TAC arith_ss []) 775 >> RW_TAC arith_ss []); 776 777val SUM_CONST = store_thm 778 ("SUM_CONST", 779 ``!n r. sum (0,n) (K r) = &n * r``, 780 Induct >- RW_TAC real_ss [sum] 781 >> RW_TAC bool_ss [sum, ADD1, K_THM, GSYM REAL_ADD, REAL_ADD_RDISTRIB] 782 >> RW_TAC real_ss []); 783 784val SUMINF_2D = store_thm 785 ("SUMINF_2D", 786 ``!f g h. 787 (!m n. 0 <= f m n) /\ (!n. f n sums g n) /\ summable g /\ 788 BIJ h UNIV (UNIV CROSS UNIV) ==> 789 (UNCURRY f o h) sums suminf g``, 790 RW_TAC std_ss [] 791 >> RW_TAC std_ss [sums] 792 >> Know `g sums suminf g` >- PROVE_TAC [SUMMABLE_SUM] 793 >> Q.PAT_X_ASSUM `!n. P n` MP_TAC 794 >> RW_TAC std_ss [SUMS_EQ, FORALL_AND_THM] 795 >> MATCH_MP_TAC INCREASING_SEQ 796 >> CONJ_TAC 797 >- (RW_TAC std_ss [sum, o_THM, ADD_CLAUSES] 798 >> Cases_on `h n` 799 >> RW_TAC std_ss [UNCURRY_DEF] 800 >> Q.PAT_X_ASSUM `!m n. 0 <= f m n` (MP_TAC o Q.SPECL [`q`, `r`]) 801 >> REAL_ARITH_TAC) 802 >> Know `!m. 0 <= g m` 803 >- (STRIP_TAC 804 >> Suff `0 <= suminf (f m)` >- PROVE_TAC [] 805 >> MATCH_MP_TAC SER_POS 806 >> PROVE_TAC []) 807 >> STRIP_TAC 808 >> CONJ_TAC 809 >- (RW_TAC std_ss [] 810 >> MP_TAC (Q.SPECL [`h`, `n`] NUM_2D_BIJ_BIG_SQUARE) 811 >> ASM_REWRITE_TAC [] 812 >> STRIP_TAC 813 >> MATCH_MP_TAC REAL_LE_TRANS 814 >> Q.EXISTS_TAC `sum (0,k) g` 815 >> Reverse CONJ_TAC 816 >- (MATCH_MP_TAC SER_POS_LE 817 >> PROVE_TAC []) 818 >> MATCH_MP_TAC REAL_LE_TRANS 819 >> Q.EXISTS_TAC `sum (0,k) (\m. sum (0,k) (f m))` 820 >> Reverse CONJ_TAC 821 >- (MATCH_MP_TAC SUM_LE 822 >> RW_TAC std_ss [] 823 >> Q.PAT_X_ASSUM `!n. suminf (f n) = g n` (REWRITE_TAC o wrap o GSYM) 824 >> MATCH_MP_TAC SER_POS_LE 825 >> PROVE_TAC []) 826 >> Suff 827 `!j. 828 j <= n ==> 829 (sum (0, j) (UNCURRY f o h) = 830 sum (0, k) 831 (\m. sum (0, k) 832 (\n. if (?i. i < j /\ (h i = (m, n))) then f m n else 0)))` 833 >- (DISCH_THEN (MP_TAC o Q.SPEC `n`) 834 >> REWRITE_TAC [LESS_EQ_REFL] 835 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 836 >> MATCH_MP_TAC SUM_LE 837 >> RW_TAC std_ss [] 838 >> MATCH_MP_TAC SUM_LE 839 >> RW_TAC std_ss [REAL_LE_REFL]) 840 >> Induct >- RW_TAC arith_ss [sum, SUM_0] 841 >> RW_TAC std_ss [sum] 842 >> Q.PAT_X_ASSUM `p ==> q` MP_TAC 843 >> RW_TAC arith_ss [] 844 >> Know 845 `!m n. 846 (?i. i < SUC j /\ (h i = (m,n))) = 847 (?i. i < j /\ (h i = (m,n))) \/ (h j = (m, n))` 848 >- (RW_TAC std_ss [] 849 >> Suff `!i. i < SUC j = i < j \/ (i = j)` 850 >- PROVE_TAC [] 851 >> DECIDE_TAC) 852 >> DISCH_THEN (REWRITE_TAC o wrap) 853 >> Know 854 `!m n. 855 (if (?i. i < j /\ (h i = (m,n))) \/ (h j = (m,n)) then f m n 856 else 0) = 857 (if (?i. i < j /\ (h i = (m,n))) then f m n else 0) + 858 (if (h j = (m,n)) then f m n else 0)` 859 >- (Strip 860 >> Suff `(?i. i < j /\ (h i = (m,n'))) ==> ~(h j = (m,n'))` 861 >- PROVE_TAC [REAL_ADD_LID, REAL_ADD_RID] 862 >> RW_TAC std_ss [] 863 >> Q.PAT_X_ASSUM `BIJ a b c` MP_TAC 864 >> RW_TAC std_ss [BIJ_DEF, INJ_DEF, IN_UNIV, IN_CROSS] 865 >> PROVE_TAC [prim_recTheory.LESS_REFL]) 866 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 867 >> RW_TAC std_ss [SUM_ADD] 868 >> POP_ASSUM K_TAC 869 >> Suff 870 `(UNCURRY f o h) j = 871 sum (0,k) 872 (\m. sum (0,k) (\n. (if h j = (m,n) then f m n else 0)))` 873 >- (KILL_TAC 874 >> Q.SPEC_TAC 875 (`(sum (0,k) 876 (\m. 877 sum (0,k) 878 (\n. if ?i. i < j /\ (h i = (m,n)) then f m n else 0)))`, 879 `r1`) 880 >> Q.SPEC_TAC 881 (`sum (0,k) 882 (\m. sum (0,k) (\n. (if h j = (m,n) then f m n else 0)))`, 883 `r2`) 884 >> RW_TAC std_ss []) 885 >> Cases_on `h j` 886 >> RW_TAC std_ss [o_THM, UNCURRY_DEF] 887 >> Know 888 `!m n. 889 (if (q = m) /\ (r = n) then f m n else 0) = 890 (if (n = r) then if (m = q) then f m n else 0 else 0)` 891 >- PROVE_TAC [] 892 >> DISCH_THEN (REWRITE_TAC o wrap) 893 >> Q.PAT_X_ASSUM `a SUBSET b` MP_TAC 894 >> RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, IN_COUNT, IN_CROSS] 895 >> Suff `q < k /\ r < k` 896 >- RW_TAC std_ss [SUM_PICK] 897 >> POP_ASSUM (MP_TAC o Q.SPEC `h (j:num)`) 898 >> Suff `j < n` 899 >- (RW_TAC std_ss [] 900 >> PROVE_TAC []) 901 >> DECIDE_TAC) 902 >> RW_TAC std_ss [] 903 >> Know `?M. 0 < M /\ suminf g < sum (0, M) g + e / 2` 904 >- (Know `g sums suminf g` >- PROVE_TAC [SUMMABLE_SUM] 905 >> RW_TAC std_ss [sums, SEQ] 906 >> POP_ASSUM (MP_TAC o Q.SPEC `e / 2`) 907 >> RW_TAC std_ss [REAL_LT_HALF1, GREATER_EQ] 908 >> POP_ASSUM (MP_TAC o Q.SPEC `SUC N`) 909 >> ONCE_REWRITE_TAC [ABS_SUB] 910 >> Know `sum (0, SUC N) g <= suminf g` 911 >- (MATCH_MP_TAC SER_POS_LE 912 >> RW_TAC std_ss []) 913 >> Reverse (RW_TAC arith_ss [abs]) 914 >- (Suff `F` >- PROVE_TAC [] 915 >> POP_ASSUM K_TAC 916 >> POP_ASSUM MP_TAC 917 >> POP_ASSUM MP_TAC 918 >> REAL_ARITH_TAC) 919 >> Q.EXISTS_TAC `SUC N` 920 >> CONJ_TAC >- DECIDE_TAC 921 >> POP_ASSUM MP_TAC 922 >> REAL_ARITH_TAC) 923 >> RW_TAC std_ss [] 924 >> Suff `?k. sum (0, M) g < sum (0, k) (UNCURRY f o h) + e / 2` 925 >- (Strip 926 >> Q.EXISTS_TAC `k` 927 >> Know 928 `sum (0, M) g + e / 2 < sum (0, k) (UNCURRY f o h) + (e / 2 + e / 2)` 929 >- (POP_ASSUM MP_TAC 930 >> REAL_ARITH_TAC) 931 >> POP_ASSUM K_TAC 932 >> POP_ASSUM MP_TAC 933 >> REWRITE_TAC [REAL_HALF_DOUBLE] 934 >> REAL_ARITH_TAC) 935 >> POP_ASSUM K_TAC 936 >> Know `!m. ?N. g m < sum (0, N) (f m) + (e / 2) / & M` 937 >- (Know `!m. f m sums g m` 938 >- RW_TAC std_ss [SUMS_EQ] 939 >> RW_TAC std_ss [sums, SEQ] 940 >> POP_ASSUM (MP_TAC o Q.SPECL [`m`, `(e / 2) / & M`]) 941 >> Know `0 < (e / 2) / & M` 942 >- RW_TAC arith_ss [REAL_LT_DIV, REAL_NZ_IMP_LT] 943 >> DISCH_THEN (REWRITE_TAC o wrap) 944 >> RW_TAC std_ss [GREATER_EQ] 945 >> POP_ASSUM (MP_TAC o Q.SPEC `N`) 946 >> ONCE_REWRITE_TAC [ABS_SUB] 947 >> Know `sum (0, N) (f m) <= g m` 948 >- (Q.PAT_X_ASSUM `!n. P n = Q n` (REWRITE_TAC o wrap o GSYM) 949 >> MATCH_MP_TAC SER_POS_LE 950 >> RW_TAC std_ss []) 951 >> Reverse (RW_TAC arith_ss [abs]) 952 >- (POP_ASSUM K_TAC 953 >> Suff `F` >- PROVE_TAC [] 954 >> NTAC 2 (POP_ASSUM MP_TAC) 955 >> REAL_ARITH_TAC) 956 >> Q.EXISTS_TAC `N` 957 >> POP_ASSUM MP_TAC 958 >> REAL_ARITH_TAC) 959 >> DISCH_THEN (MP_TAC o CONV_RULE SKOLEM_CONV) 960 >> RW_TAC std_ss [] 961 >> Know `?c. M <= c /\ !m. m < M ==> N m <= c` 962 >- (KILL_TAC 963 >> Induct_on `M` >- RW_TAC arith_ss [] 964 >> Strip 965 >> Q.EXISTS_TAC `MAX (SUC c) (N M)` 966 >> RW_TAC arith_ss [X_LE_MAX, LT_SUC] 967 >> PROVE_TAC [LESS_EQ_REFL, LE]) 968 >> Strip 969 >> MP_TAC (Q.SPECL [`h`, `c`] NUM_2D_BIJ_SMALL_SQUARE) 970 >> ASM_REWRITE_TAC [] 971 >> DISCH_THEN (Q.X_CHOOSE_TAC `k`) 972 >> Q.EXISTS_TAC `k` 973 >> MATCH_MP_TAC REAL_LTE_TRANS 974 >> Q.EXISTS_TAC `sum (0, M) (\m. sum (0, N m) (f m) + e / 2 / &M)` 975 >> CONJ_TAC 976 >- (MATCH_MP_TAC SUM_LT 977 >> RW_TAC arith_ss []) 978 >> RW_TAC std_ss [SUM_ADD, GSYM K_PARTIAL, SUM_CONST] 979 >> Know `!x. & M * (x / & M) = x` 980 >- (RW_TAC std_ss [real_div] 981 >> Suff `(& M * inv (& M)) * x = x` 982 >- PROVE_TAC [REAL_MUL_ASSOC, REAL_MUL_SYM] 983 >> Suff `~(& M = 0)` >- RW_TAC std_ss [REAL_MUL_RINV, REAL_MUL_LID] 984 >> RW_TAC arith_ss [REAL_INJ]) 985 >> DISCH_THEN (REWRITE_TAC o wrap) 986 >> RW_TAC std_ss [REAL_LE_RADD] 987 >> Suff 988 `sum (0,M) (\m. sum (0,N m) (f m)) = 989 sum (0, k) 990 (\k. 991 if ?m n. m < M /\ n < N m /\ (h k = (m, n)) then (UNCURRY f o h) k 992 else 0)` 993 >- (RW_TAC std_ss [] 994 >> MATCH_MP_TAC SUM_LE 995 >> RW_TAC std_ss [o_THM, REAL_LE_REFL] 996 >> Cases_on `h r` 997 >> RW_TAC std_ss [UNCURRY_DEF]) 998 >> NTAC 3 (POP_ASSUM MP_TAC) 999 >> Q.PAT_X_ASSUM `BIJ h a b` MP_TAC 1000 >> KILL_TAC 1001 >> RW_TAC std_ss [] 1002 >> Induct_on `M` >- RW_TAC arith_ss [sum, SUM_ZERO] 1003 >> RW_TAC arith_ss [sum, LT_SUC] 1004 >> Q.PAT_X_ASSUM `a ==> b` K_TAC 1005 >> Know 1006 `!k'. 1007 (?m n. (m < M \/ (m = M)) /\ n < N m /\ (h k' = (m, n))) = 1008 (?m n. m < M /\ n < N m /\ (h k' = (m, n))) \/ 1009 (?n. n < N M /\ (h k' = (M, n)))` 1010 >- PROVE_TAC [] 1011 >> DISCH_THEN (REWRITE_TAC o wrap) 1012 >> Know 1013 `!k'. 1014 (if (?m n. m < M /\ n < N m /\ (h k' = (m,n))) \/ 1015 (?n. n < N M /\ (h k' = (M,n))) 1016 then UNCURRY f (h k') 1017 else 0) = 1018 (if (?m n. m < M /\ n < N m /\ (h k' = (m,n))) then UNCURRY f (h k') 1019 else 0) + 1020 (if (?n. n < N M /\ (h k' = (M,n))) then UNCURRY f (h k') 1021 else 0)` 1022 >- (STRIP_TAC 1023 >> Suff 1024 `(?m n. m < M /\ n < N m /\ (h k' = (m,n))) ==> 1025 ~(?n. n < N M /\ (h k' = (M,n)))` 1026 >- PROVE_TAC [REAL_ADD_RID, REAL_ADD_LID] 1027 >> Cases_on `h k'` 1028 >> RW_TAC arith_ss []) 1029 >> DISCH_THEN (REWRITE_TAC o wrap) 1030 >> RW_TAC std_ss [SUM_ADD, REAL_EQ_LADD] 1031 >> Know `N M <= c` >- PROVE_TAC [] 1032 >> POP_ASSUM K_TAC 1033 >> Q.SPEC_TAC (`N M`, `l`) 1034 >> Induct >- RW_TAC real_ss [sum, SUM_0] 1035 >> RW_TAC arith_ss [sum, LT_SUC] 1036 >> Q.PAT_X_ASSUM `a ==> b` K_TAC 1037 >> Know 1038 `!k'. 1039 (?n. (n < l \/ (n = l)) /\ (h k' = (M,n))) = 1040 (?n. n < l /\ (h k' = (M,n))) \/ (h k' = (M, l))` 1041 >- PROVE_TAC [] 1042 >> DISCH_THEN (REWRITE_TAC o wrap) 1043 >> Know 1044 `!k'. 1045 (if (?n. n < l /\ (h k' = (M,n))) \/ (h k' = (M, l)) then 1046 UNCURRY f (h k') 1047 else 0) = 1048 (if (?n. n < l /\ (h k' = (M,n))) then UNCURRY f (h k') else 0) + 1049 (if (h k' = (M, l)) then UNCURRY f (h k') else 0)` 1050 >- (STRIP_TAC 1051 >> Suff `(?n. n < l /\ (h k' = (M,n))) ==> ~(h k' = (M, l))` 1052 >- PROVE_TAC [REAL_ADD_LID, REAL_ADD_RID] 1053 >> Cases_on `h k'` 1054 >> RW_TAC arith_ss []) 1055 >> DISCH_THEN (REWRITE_TAC o wrap) 1056 >> RW_TAC std_ss [SUM_ADD, REAL_EQ_LADD] 1057 >> Q.PAT_X_ASSUM `a SUBSET b` MP_TAC 1058 >> RW_TAC std_ss [SUBSET_DEF, IN_CROSS, IN_COUNT, IN_IMAGE] 1059 >> POP_ASSUM (MP_TAC o Q.SPEC `(M, l)`) 1060 >> RW_TAC arith_ss [] 1061 >> Suff `!k'. (h k' = (M, l)) = (k' = x')` 1062 >- (RW_TAC std_ss [SUM_PICK, o_THM] 1063 >> Q.PAT_X_ASSUM `(M,l) = a` (REWRITE_TAC o wrap o GSYM) 1064 >> RW_TAC std_ss [UNCURRY_DEF]) 1065 >> Q.PAT_X_ASSUM `BIJ h a b` MP_TAC 1066 >> RW_TAC std_ss [BIJ_DEF, INJ_DEF, IN_UNIV, IN_CROSS] 1067 >> PROVE_TAC []); 1068 1069val REAL_INV_INJ = store_thm 1070 ("REAL_INV_INJ", 1071 ``!x y. (inv x = inv y) = (x = y)``, 1072 RW_TAC std_ss [] 1073 >> Reverse EQ_TAC >- RW_TAC std_ss [] 1074 >> RW_TAC std_ss [] 1075 >> ONCE_REWRITE_TAC [GSYM REAL_INV_INV] 1076 >> RW_TAC std_ss []); 1077 1078val POW_HALF_SMALL = store_thm 1079 ("POW_HALF_SMALL", 1080 ``!e. 0 < e ==> ?n. (1 / 2) pow n < e``, 1081 RW_TAC std_ss [] 1082 >> MP_TAC (Q.SPEC `1 / 2` SEQ_POWER) 1083 >> RW_TAC std_ss [abs, HALF_LT_1, HALF_POS, REAL_LT_IMP_LE, SEQ] 1084 >> POP_ASSUM (MP_TAC o Q.SPEC `e`) 1085 >> RW_TAC std_ss [REAL_SUB_RZERO, POW_HALF_POS, REAL_LT_IMP_LE, 1086 GREATER_EQ] 1087 >> PROVE_TAC [LESS_EQ_REFL]); 1088 1089val LOG2_SUC = store_thm 1090 ("LOG2_SUC", 1091 ``!n t. 1092 0 < n /\ 2 * log2 (n + 1) <= t ==> 1093 (1 / 2) pow t <= 1 / &n - 1 / (&n + 1)``, 1094 REPEAT STRIP_TAC 1095 >> RW_TAC std_ss [INV_DIFF_SUC, POW_HALF_EXP, GSYM REAL_INV_1OVER] 1096 >> MATCH_MP_TAC REAL_LE_INV_LE 1097 >> REPEAT STRIP_TAC 1098 >- (MATCH_MP_TAC REAL_NZ_IMP_LT 1099 >> RW_TAC arith_ss [GSYM ADD1, MULT]) 1100 >> RW_TAC std_ss [REAL_LE] 1101 >> Suff `(n + 1) * (n + 1) <= 2 EXP t` 1102 >- (Suff `n * (n + 1) <= (n + 1) * (n + 1)` >- DECIDE_TAC 1103 >> RW_TAC std_ss [GSYM ADD1, MULT] 1104 >> DECIDE_TAC) 1105 >> Suff `(n + 1) EXP 2 <= (2 EXP log2 (n + 1)) EXP 2` 1106 >- (RW_TAC bool_ss [TWO, EXP, EXP_1, EXP_MULT] 1107 >> POP_ASSUM MP_TAC 1108 >> ONCE_REWRITE_TAC [MULT_COMM] 1109 >> RW_TAC std_ss [GSYM TWO] 1110 >> MATCH_MP_TAC LESS_EQ_TRANS 1111 >> Q.EXISTS_TAC `2 EXP (2 * log2 (n + 1))` 1112 >> CONJ_TAC >- RW_TAC std_ss [] 1113 >> MATCH_MP_TAC EXP1_MONO_LE 1114 >> RW_TAC arith_ss []) 1115 >> MATCH_MP_TAC EXP2_MONO_LE 1116 >> MP_TAC (Q.SPEC `n + 1` LOG2_LOWER) 1117 >> RW_TAC arith_ss []); 1118 1119val LE_SEQ_IMP_LE_LIM = store_thm 1120 ("LE_SEQ_IMP_LE_LIM", 1121 ``!x y f. (!n. x <= f n) /\ f --> y ==> x <= y``, 1122 RW_TAC std_ss [SEQ] 1123 >> MATCH_MP_TAC REAL_LE_EPSILON 1124 >> RW_TAC std_ss [] 1125 >> Q.PAT_X_ASSUM `!e. P e` (MP_TAC o Q.SPEC `e`) 1126 >> RW_TAC std_ss [] 1127 >> POP_ASSUM (MP_TAC o Q.SPEC `N`) 1128 >> Q.PAT_X_ASSUM `!n. P n` (MP_TAC o Q.SPEC `N`) 1129 >> RW_TAC arith_ss [abs] 1130 >> REPEAT (POP_ASSUM MP_TAC) 1131 >> REAL_ARITH_TAC); 1132 1133val SER_POS_COMPAR = store_thm 1134 ("SER_POS_COMPAR", 1135 ``!f g. (!n. 0 <= f n) /\ summable g /\ (!n. f n <= g n) ==> summable f``, 1136 PROVE_TAC [SER_POS_COMPARE]); 1137 1138val SUM_SUMINF = store_thm 1139 ("SUM_SUMINF", 1140 ``!p f n. 1141 (summable (\m. if m < n then f m else 0) ==> 1142 p (suminf (\m. if m < n then f m else 0))) ==> 1143 p (sum (0, n) f)``, 1144 RW_TAC std_ss [] 1145 >> Suff `(\m. (if m < n then f m else 0)) sums (sum (0, n) f)` 1146 >- (RW_TAC std_ss [SUMS_EQ] 1147 >> PROVE_TAC []) 1148 >> Suff `sum (0, n) f = sum (0, n) (\m. (if m < n then f m else 0))` 1149 >- (Rewr 1150 >> MATCH_MP_TAC SER_0 1151 >> RW_TAC arith_ss []) 1152 >> MATCH_MP_TAC SUM_EQ 1153 >> RW_TAC arith_ss []); 1154 1155val SUMS_PICK = store_thm 1156 ("SUMS_PICK", 1157 ``!k x. (\n. if n = k then x else 0) sums x``, 1158 RW_TAC std_ss [] 1159 >> Know `sum (0, SUC k) (\n. if n = k then x else 0) = x` 1160 >- RW_TAC arith_ss [SUM_PICK] 1161 >> DISCH_THEN (CONV_TAC o RAND_CONV o ONCE_REWRITE_CONV o wrap o SYM) 1162 >> MATCH_MP_TAC SER_0 1163 >> RW_TAC arith_ss []); 1164 1165val SUM_REORDER_LE = store_thm 1166 ("SUM_REORDER_LE", 1167 ``!f n1 n2 j1 j2. 1168 (!n. 0 <= f n) /\ INJ j1 (count n1) UNIV /\ 1169 IMAGE j1 (count n1) SUBSET IMAGE j2 (count n2) ==> 1170 sum (0, n1) (f o j1) <= sum (0, n2) (f o j2)``, 1171 Induct_on `n1` 1172 >- (RW_TAC std_ss [sum, COUNT_ZERO, EMPTY_SUBSET, IMAGE_EMPTY] 1173 >> Suff `!n. 0 <= (f o j2) n` >- RW_TAC std_ss [SUM_POS] 1174 >> RW_TAC std_ss [o_THM]) 1175 >> RW_TAC std_ss [sum, o_THM, INSERT_SUBSET, COUNT_SUC, IMAGE_INSERT, 1176 IN_IMAGE, IN_COUNT] 1177 >> MATCH_MP_TAC REAL_LE_TRANS 1178 >> Q.EXISTS_TAC 1179 `f (j1 n1) + sum (0,n2) ((\a. if a = j1 n1 then 0 else f a) o j2)` 1180 >> CONJ_TAC 1181 >- (CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [REAL_ADD_COMM])) 1182 >> RW_TAC std_ss [REAL_LE_LADD] 1183 >> Know 1184 `sum (0, n1) (f o j1) = 1185 sum (0, n1) ((\a. (if a = j2 x then 0 else f a)) o j1)` 1186 >- (MATCH_MP_TAC SUM_EQ 1187 >> RW_TAC arith_ss [o_THM] 1188 >> Suff `F` >- PROVE_TAC [] 1189 >> Q.PAT_X_ASSUM `INJ j1 X Y` MP_TAC 1190 >> RW_TAC std_ss [INJ_DEF, IN_INSERT, IN_COUNT, IN_UNIV] 1191 >> PROVE_TAC [prim_recTheory.LESS_NOT_EQ]) 1192 >> Rewr 1193 >> Q.PAT_X_ASSUM `!f n2. P f n2` MATCH_MP_TAC 1194 >> RW_TAC std_ss [REAL_LE_REFL] 1195 >> Q.PAT_X_ASSUM `INJ j1 X Y` MP_TAC 1196 >> RW_TAC bool_ss [INJ_DEF, IN_INSERT, IN_COUNT, IN_UNIV]) 1197 >> MATCH_MP_TAC REAL_LE_TRANS 1198 >> Q.EXISTS_TAC 1199 `f (j1 n1) + sum (0, n2) (\i. if i = x then 0 else f (j2 i))` 1200 >> CONJ_TAC 1201 >- (RW_TAC std_ss [REAL_LE_LADD] 1202 >> MATCH_MP_TAC SUM_LE 1203 >> RW_TAC arith_ss [o_THM, REAL_LE_REFL]) 1204 >> Know 1205 `f o j2 = 1206 (\i. (if i = x then 0 else f (j2 i)) + 1207 (if i = x then f (j2 i) else 0))` 1208 >- (FUN_EQ_TAC 1209 >> RW_TAC real_ss [o_THM]) 1210 >> Rewr 1211 >> CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [REAL_ADD_COMM])) 1212 >> RW_TAC real_ss [SUM_ADD, SUM_PICK, REAL_LE_LADD, REAL_LE_REFL]); 1213 1214val SER_BIJ_COMPRESS1 = store_thm 1215 ("SER_BIJ_COMPRESS1", 1216 ``!f h s. 1217 (!n. 0 <= f n) /\ summable f /\ BIJ h UNIV s /\ 1218 (!n. ~(n IN s) ==> (f n = 0)) ==> 1219 (f o h) sums suminf f``, 1220 RW_TAC std_ss [sums, SEQ] 1221 >> ONCE_REWRITE_TAC [ABS_SUB] 1222 >> RW_TAC std_ss [abs] 1223 >> Know `!n. sum (0, n) (f o h) <= suminf f` 1224 >- (Know `!n. ?N. !m. m < n ==> h m < N` 1225 >- (Induct >- RW_TAC arith_ss [] 1226 >> POP_ASSUM MP_TAC 1227 >> STRIP_TAC 1228 >> Q.EXISTS_TAC `SUC (MAX N (h n))` 1229 >> STRIP_TAC 1230 >> DISCH_THEN (MP_TAC o REWRITE_RULE [LT_SUC]) 1231 >> Know `!a b. a < SUC b = a <= b` 1232 >- (Cases >> STRIP_TAC >> KILL_TAC >> DECIDE_TAC) 1233 >> RW_TAC std_ss [X_LE_MAX] 1234 >> PROVE_TAC [LESS_IMP_LESS_OR_EQ, LESS_EQ_REFL]) 1235 >> DISCH_THEN (MP_TAC o CONV_RULE SKOLEM_CONV) 1236 >> STRIP_TAC 1237 >> STRIP_TAC 1238 >> MATCH_MP_TAC REAL_LE_TRANS 1239 >> Q.EXISTS_TAC `sum (0, N n) f` 1240 >> REVERSE CONJ_TAC 1241 >- (MATCH_MP_TAC SER_POS_LE 1242 >> RW_TAC std_ss []) 1243 >> Know `sum (0, N n) f = sum (0, N n) (f o I)` 1244 >- RW_TAC std_ss [I_o_ID] 1245 >> Rewr 1246 >> MATCH_MP_TAC SUM_REORDER_LE 1247 >> Q.PAT_X_ASSUM `BIJ h X Y` MP_TAC 1248 >> RW_TAC std_ss [INJ_DEF, BIJ_DEF, IN_UNIV, IN_COUNT, SUBSET_DEF, 1249 I_THM, IN_IMAGE] 1250 >> PROVE_TAC []) 1251 >> STRIP_TAC 1252 >> Know `!n. 0 <= suminf f - sum (0, n) (f o h)` 1253 >- (STRIP_TAC 1254 >> POP_ASSUM (MP_TAC o Q.SPEC `n`) 1255 >> REAL_ARITH_TAC) 1256 >> Rewr 1257 >> Know `f sums suminf f` >- PROVE_TAC [SUMMABLE_SUM] 1258 >> RW_TAC std_ss [sums, SEQ] 1259 >> POP_ASSUM (MP_TAC o Q.SPEC `e`) 1260 >> RW_TAC std_ss [GREATER_EQ] 1261 >> (MP_TAC o 1262 Q.SPECL [`h`, `s`, `count N INTER s`] o 1263 INST_TYPE [alpha |-> ``:num``]) 1264 BIJ_FINITE_SUBSET 1265 >> Know `FINITE (count N INTER s)` 1266 >- PROVE_TAC [FINITE_COUNT, FINITE_INTER, INTER_COMM] 1267 >> Rewr 1268 >> RW_TAC std_ss [INTER_SUBSET, IN_INTER] 1269 >> Q.EXISTS_TAC `N'` 1270 >> RW_TAC std_ss [] 1271 >> Suff `suminf f - e < sum (0, n) (f o h)` >- REAL_ARITH_TAC 1272 >> MATCH_MP_TAC REAL_LTE_TRANS 1273 >> Q.EXISTS_TAC `sum (0, N) f` 1274 >> CONJ_TAC 1275 >- (Q.PAT_X_ASSUM `!n. P n ==> Q n < e` (MP_TAC o Q.SPEC `N`) 1276 >> ONCE_REWRITE_TAC [ABS_SUB] 1277 >> RW_TAC arith_ss [abs] 1278 >- (POP_ASSUM MP_TAC 1279 >> REAL_ARITH_TAC) 1280 >> Suff `F` >- PROVE_TAC [] 1281 >> POP_ASSUM K_TAC 1282 >> POP_ASSUM MP_TAC 1283 >> Suff `sum (0, N) f <= suminf f` >- REAL_ARITH_TAC 1284 >> MATCH_MP_TAC SER_POS_LE 1285 >> RW_TAC std_ss []) 1286 >> Know 1287 `sum (0, N) f = 1288 sum (0, N) ((\x. sum_CASE x f (K 0)) o 1289 (\n. if n IN s then INL n else INR n))` 1290 >- (MATCH_MP_TAC SUM_EQ 1291 >> RW_TAC std_ss [sum_case_def, o_THM, K_DEF]) 1292 >> Rewr 1293 >> Know 1294 `sum (0, n) (f o h) = 1295 sum (0, n + N) 1296 ((\x. sum_CASE x f (K 0)) o 1297 (\i. if i < n then INL (h i) else INR (i - n)))` 1298 >- (KILL_TAC 1299 >> REVERSE (Induct_on `N`) 1300 >- RW_TAC arith_ss [sum, o_THM, ADD_CLAUSES, K_THM, REAL_ADD_RID] 1301 >> RW_TAC arith_ss [] 1302 >> MATCH_MP_TAC SUM_EQ 1303 >> RW_TAC arith_ss [sum_case_def, o_THM]) 1304 >> Rewr 1305 >> MATCH_MP_TAC SUM_REORDER_LE 1306 >> Q.PAT_X_ASSUM `BIJ h X Y` MP_TAC 1307 >> ASM_SIMP_TAC (srw_ss()) [sumTheory.FORALL_SUM] 1308 >> BasicProvers.NORM_TAC std_ss [SUBSET_DEF, IN_IMAGE, INJ_DEF, IN_UNIV, 1309 IN_COUNT, INJ_DEF, BIJ_DEF, SURJ_DEF] >| 1310 [Q.PAT_X_ASSUM `!x. P x` (MP_TAC o Q.SPEC `n'`) 1311 >> RW_TAC std_ss [] 1312 >> Q.EXISTS_TAC `y` 1313 >> RW_TAC std_ss [] 1314 >> Suff `y < n` >- RW_TAC arith_ss [] 1315 >> Q.PAT_X_ASSUM `!n. P n ==> Q n` (MP_TAC o Q.SPEC `y`) 1316 >> RW_TAC std_ss [IN_COUNT] 1317 >> POP_ASSUM MP_TAC 1318 >> Q.PAT_X_ASSUM `N' <= n` MP_TAC 1319 >> KILL_TAC 1320 >> DECIDE_TAC, 1321 Q.EXISTS_TAC `n' + n` 1322 >> RW_TAC arith_ss []]); 1323 1324val SER_BIJ_COMPRESS2 = store_thm 1325 ("SER_BIJ_COMPRESS2", 1326 ``!f h s. 1327 (!n. 0 <= f n) /\ summable (f o h) /\ BIJ h UNIV s /\ 1328 (!n. ~(n IN s) ==> (f n = 0)) ==> 1329 f sums suminf (f o h)``, 1330 RW_TAC std_ss [sums, SEQ] 1331 >> ONCE_REWRITE_TAC [ABS_SUB] 1332 >> RW_TAC std_ss [abs] 1333 >> Know `!n. sum (0, n) f <= suminf (f o h)` 1334 >- (STRIP_TAC 1335 >> (MP_TAC o 1336 Q.SPECL [`h`, `s`, `count n INTER s`] o 1337 INST_TYPE [alpha |-> ``:num``]) 1338 BIJ_FINITE_SUBSET 1339 >> Know `FINITE (count n INTER s)` 1340 >- PROVE_TAC [FINITE_COUNT, FINITE_INTER, INTER_COMM] 1341 >> Rewr 1342 >> RW_TAC std_ss [INTER_SUBSET, IN_INTER] 1343 >> MATCH_MP_TAC REAL_LE_TRANS 1344 >> Q.EXISTS_TAC `sum (0, N) (f o h)` 1345 >> REVERSE CONJ_TAC 1346 >- (MATCH_MP_TAC SER_POS_LE 1347 >> RW_TAC std_ss [o_THM]) 1348 >> Know 1349 `sum (0, n) f = 1350 sum (0, n) ((\x. sum_CASE x f (K 0)) o 1351 (\n. if n IN s then INL n else INR n))` 1352 >- (MATCH_MP_TAC SUM_EQ 1353 >> RW_TAC std_ss [sum_case_def, o_THM, K_DEF]) 1354 >> Rewr 1355 >> Know 1356 `sum (0, N) (f o h) = 1357 sum (0, N + n) 1358 ((\x. sum_CASE x f (K 0)) o 1359 (\i. if i < N then INL (h i) else INR (i - N)))` 1360 >- (KILL_TAC 1361 >> REVERSE (Induct_on `n`) 1362 >- RW_TAC arith_ss [sum, o_THM, ADD_CLAUSES, K_THM, REAL_ADD_RID] 1363 >> RW_TAC arith_ss [] 1364 >> MATCH_MP_TAC SUM_EQ 1365 >> RW_TAC arith_ss [sum_case_def, o_THM]) 1366 >> Rewr 1367 >> MATCH_MP_TAC SUM_REORDER_LE 1368 >> ASM_SIMP_TAC (srw_ss()) [sumTheory.FORALL_SUM] 1369 >> Q.PAT_X_ASSUM `BIJ h X Y` MP_TAC 1370 >> BasicProvers.NORM_TAC std_ss [SUBSET_DEF, IN_IMAGE, INJ_DEF, IN_UNIV, 1371 IN_COUNT, INJ_DEF, BIJ_DEF, SURJ_DEF] >| 1372 [Q.PAT_X_ASSUM `!x. P x` (MP_TAC o Q.SPEC `n'`) 1373 >> RW_TAC std_ss [] 1374 >> Q.EXISTS_TAC `y` 1375 >> Suff `y < N` >- RW_TAC arith_ss [] 1376 >> Q.PAT_X_ASSUM `!n'. N <= n' ==> P n'` (MP_TAC o Q.SPEC `y`) 1377 >> RW_TAC std_ss [IN_COUNT] 1378 >> POP_ASSUM MP_TAC 1379 >> KILL_TAC 1380 >> DECIDE_TAC, 1381 Q.EXISTS_TAC `n' + N` 1382 >> RW_TAC arith_ss []]) 1383 >> STRIP_TAC 1384 >> Know `!n. 0 <= suminf (f o h) - sum (0, n) f` 1385 >- (STRIP_TAC 1386 >> POP_ASSUM (MP_TAC o Q.SPEC `n`) 1387 >> REAL_ARITH_TAC) 1388 >> Rewr 1389 >> Know `(f o h) sums suminf (f o h)` >- PROVE_TAC [SUMMABLE_SUM] 1390 >> RW_TAC std_ss [sums, SEQ] 1391 >> POP_ASSUM (MP_TAC o Q.SPEC `e`) 1392 >> RW_TAC std_ss [GREATER_EQ] 1393 >> Know `!n. ?N. !m. m < n ==> h m < N` 1394 >- (Induct >- RW_TAC arith_ss [] 1395 >> POP_ASSUM MP_TAC 1396 >> STRIP_TAC 1397 >> Q.EXISTS_TAC `SUC (MAX N' (h n))` 1398 >> STRIP_TAC 1399 >> DISCH_THEN (MP_TAC o REWRITE_RULE [LT_SUC]) 1400 >> Know `!a b. a < SUC b = a <= b` 1401 >- (Cases >> STRIP_TAC >> KILL_TAC >> DECIDE_TAC) 1402 >> RW_TAC std_ss [X_LE_MAX] 1403 >> PROVE_TAC [LESS_IMP_LESS_OR_EQ, LESS_EQ_REFL]) 1404 >> DISCH_THEN (MP_TAC o CONV_RULE SKOLEM_CONV) 1405 >> STRIP_TAC 1406 >> Q.EXISTS_TAC `N' N` 1407 >> RW_TAC std_ss [] 1408 >> Suff `suminf (f o h) - e < sum (0, n) f` >- REAL_ARITH_TAC 1409 >> MATCH_MP_TAC REAL_LTE_TRANS 1410 >> Q.EXISTS_TAC `sum (0, N) (f o h)` 1411 >> CONJ_TAC 1412 >- (Suff `suminf (f o h) - sum (0, N) (f o h) < e` >- REAL_ARITH_TAC 1413 >> Q.PAT_X_ASSUM `!n. N <= n ==> P n` (MP_TAC o Q.SPEC `N`) 1414 >> ONCE_REWRITE_TAC [ABS_SUB] 1415 >> RW_TAC arith_ss [abs] 1416 >> Suff `F` >- PROVE_TAC [] 1417 >> POP_ASSUM K_TAC 1418 >> POP_ASSUM MP_TAC 1419 >> Suff `sum (0, N) (f o h) <= suminf (f o h)` >- REAL_ARITH_TAC 1420 >> MATCH_MP_TAC SER_POS_LE 1421 >> RW_TAC std_ss [o_THM]) 1422 >> Know `sum (0, n) f = sum (0, n) (f o I)` 1423 >- RW_TAC std_ss [I_o_ID] 1424 >> Rewr 1425 >> MATCH_MP_TAC SUM_REORDER_LE 1426 >> Q.PAT_X_ASSUM `BIJ h X Y` MP_TAC 1427 >> RW_TAC std_ss [INJ_DEF, BIJ_DEF, IN_UNIV, IN_COUNT, SUBSET_DEF, 1428 I_THM, IN_IMAGE] 1429 >> Q.PAT_X_ASSUM `N' N <= n` MP_TAC 1430 >> Suff `h x' < N' N` >- (KILL_TAC >> DECIDE_TAC) 1431 >> PROVE_TAC []); 1432 1433val SER_BIJ_COMPRESS = store_thm 1434 ("SER_BIJ_COMPRESS", 1435 ``!f h s l. 1436 (!n. 0 <= f n) /\ BIJ h UNIV s /\ (!n. ~(n IN s) ==> (f n = 0)) ==> 1437 ((f o h) sums l = f sums l)``, 1438 RW_TAC std_ss [SUMS_EQ] 1439 >> EQ_TAC >| 1440 [STRIP_TAC 1441 >> REWRITE_TAC [GSYM SUMS_EQ] 1442 >> RW_TAC std_ss [] 1443 >> PROVE_TAC [SER_BIJ_COMPRESS2], 1444 STRIP_TAC 1445 >> REWRITE_TAC [GSYM SUMS_EQ] 1446 >> RW_TAC std_ss [] 1447 >> PROVE_TAC [SER_BIJ_COMPRESS1]]); 1448 1449val SER_BIJ = store_thm 1450 ("SER_BIJ", 1451 ``!f g h l. 1452 (!n. 0 <= f n) /\ BIJ h UNIV UNIV ==> 1453 ((f o h) sums l = f sums l)``, 1454 RW_TAC std_ss [] 1455 >> MATCH_MP_TAC SER_BIJ_COMPRESS 1456 >> Q.EXISTS_TAC `UNIV` 1457 >> RW_TAC std_ss [IN_UNIV]); 1458 1459val SUMS_ZERO = store_thm 1460 ("SUMS_ZERO", 1461 ``(K 0) sums 0``, 1462 RW_TAC real_ss [sums, SEQ, SUM_CONST, abs, REAL_SUB_REFL, REAL_LE_REFL]); 1463 1464val REAL_MUL_IDEMPOT = store_thm 1465 ("REAL_MUL_IDEMPOT", 1466 ``!r : real. (r * r = r) = (r = 0) \/ (r = 1)``, 1467 GEN_TAC 1468 >> Reverse EQ_TAC 1469 >- (RW_TAC real_ss [] >> RW_TAC std_ss [REAL_MUL_LZERO, REAL_MUL_LID]) 1470 >> RW_TAC std_ss [] 1471 >> Know `r * r = 1 * r` >- RW_TAC real_ss [] 1472 >> RW_TAC std_ss [REAL_EQ_RMUL]); 1473 1474val GP_REC = store_thm 1475 ("GP_REC", 1476 ``!a b x : real. abs b < 1 /\ (x = a + b * x) ==> (x = a / (1 - b))``, 1477 RW_TAC std_ss [] 1478 >> Know `x * (1 - b) = a` 1479 >- (RW_TAC std_ss [REAL_SUB_LDISTRIB, REAL_MUL_RID] 1480 >> ONCE_REWRITE_TAC [REAL_MUL_SYM] 1481 >> POP_ASSUM MP_TAC 1482 >> REAL_ARITH_TAC) 1483 >> POP_ASSUM K_TAC 1484 >> Know `~(1 - b = 0)` 1485 >- (POP_ASSUM MP_TAC 1486 >> RW_TAC real_ss [abs] 1487 >> REPEAT (POP_ASSUM MP_TAC) 1488 >> REAL_ARITH_TAC) 1489 >> POP_ASSUM K_TAC 1490 >> REPEAT STRIP_TAC 1491 >> Suff `x * (1 - b) = (a / (1 - b)) * (1 - b)` 1492 >- (POP_ASSUM K_TAC 1493 >> RW_TAC std_ss [REAL_EQ_RMUL]) 1494 >> RW_TAC std_ss [real_div, GSYM REAL_INV_1OVER, GSYM REAL_MUL_ASSOC, 1495 REAL_MUL_LINV, REAL_MUL_RID]); 1496 1497val REAL_DIV_EQ = store_thm 1498 ("REAL_DIV_EQ", 1499 ``!a b c d : real. 1500 ~(b = 0) /\ ~(d = 0) /\ (a * d = c * b) ==> (a / b = c / d)``, 1501 RW_TAC std_ss [real_div] 1502 >> Suff `(a * inv b) * b = (c * inv d) * b` 1503 >- RW_TAC std_ss [REAL_EQ_RMUL] 1504 >> RW_TAC std_ss [GSYM REAL_MUL_ASSOC, REAL_MUL_LINV, REAL_MUL_RID] 1505 >> Suff `a * d = (c * (inv d * b)) * d` 1506 >- RW_TAC std_ss [REAL_EQ_RMUL] 1507 >> Know `inv d * b = b * inv d` >- PROVE_TAC [REAL_MUL_SYM] 1508 >> Rewr 1509 >> RW_TAC std_ss [GSYM REAL_MUL_ASSOC, REAL_MUL_LINV, REAL_MUL_RID]); 1510 1511val REAL_DIV_ADD = store_thm 1512 ("REAL_DIV_ADD", 1513 ``!x y z : real. x / z + y / z = (x + y) / z``, 1514 RW_TAC std_ss [real_div, GSYM REAL_ADD_RDISTRIB]); 1515 1516val REAL_DIV_MUL = store_thm 1517 ("REAL_DIV_MUL", 1518 ``!x y z. ~(x = 0) /\ ~(z = 0) ==> ((x * y) / (x * z) = y / z)``, 1519 PROVE_TAC [REAL_DIV_MUL2]); 1520 1521val REAL_LDIV_EQ = store_thm 1522 ("REAL_LDIV_EQ", 1523 ``!x y z. ~(y = 0) /\ (x = y * z) ==> (x / y = z)``, 1524 REPEAT STRIP_TAC 1525 >> Know `z = z / 1` >- RW_TAC std_ss [REAL_OVER1] 1526 >> Rewr' 1527 >> MATCH_MP_TAC REAL_DIV_EQ 1528 >> RW_TAC real_ss [] 1529 >> REAL_ARITH_TAC); 1530 1531val ADD1_HALF_MULT = store_thm 1532 ("ADD1_HALF_MULT", 1533 ``!x y. x + (1 / 2) * y = (1 / 2) * (2 * x + y)``, 1534 RW_TAC std_ss [REAL_ADD_LDISTRIB, REAL_MUL_ASSOC] 1535 >> Know `(1 / 2) * 2 = 2 * (1 / 2)` >- PROVE_TAC [REAL_MUL_SYM] 1536 >> Rewr 1537 >> RW_TAC std_ss [HALF_CANCEL, REAL_MUL_LID]); 1538 1539val ADD2_HALF_MULT = store_thm 1540 ("ADD2_HALF_MULT", 1541 ``!x y. (1 / 2) * y + x = (1 / 2) * (y + 2 * x)``, 1542 PROVE_TAC [ADD1_HALF_MULT, REAL_ADD_SYM]); 1543 1544val HALF_CANCEL_REV = store_thm 1545 ("HALF_CANCEL_REV", 1546 ``(1 / 2) * 2 = 1``, 1547 PROVE_TAC [HALF_CANCEL, REAL_MUL_SYM]); 1548 1549val HALF_CANCEL_MULT = store_thm 1550 ("HALF_CANCEL_MULT", 1551 ``!x. 2 * ((1 / 2) * x) = x``, 1552 RW_TAC std_ss [HALF_CANCEL, REAL_MUL_ASSOC, REAL_MUL_LID]); 1553 1554val HALF_CANCEL_MULT_REV = store_thm 1555 ("HALF_CANCEL_MULT_REV", 1556 ``!x. (1 / 2) * (2 * x) = x``, 1557 RW_TAC std_ss [HALF_CANCEL_REV, REAL_MUL_ASSOC, REAL_MUL_LID]); 1558 1559val ABS_EQ = store_thm 1560 ("ABS_EQ", 1561 ``!x y. (!e. 0 < e ==> abs (x - y) < e) ==> (x = y)``, 1562 RW_TAC std_ss [] 1563 >> MATCH_MP_TAC SEQ_UNIQ 1564 >> Q.EXISTS_TAC `\n. x` 1565 >> RW_TAC std_ss [SEQ_CONST] 1566 >> RW_TAC std_ss [SEQ]); 1567 1568val SEQ_SANDWICH = store_thm 1569 ("SEQ_SANDWICH", 1570 ``!f g h l. 1571 f --> l /\ h --> l /\ (!n. f n <= g n /\ g n <= h n) ==> g --> l``, 1572 RW_TAC std_ss [SEQ, GREATER_EQ] 1573 >> Q.PAT_X_ASSUM `!e. P e ==> Q e` (MP_TAC o Q.SPEC `e`) 1574 >> Q.PAT_X_ASSUM `!e. P e ==> Q e` (MP_TAC o Q.SPEC `e`) 1575 >> RW_TAC std_ss [] 1576 >> Q.EXISTS_TAC `MAX N N'` 1577 >> RW_TAC std_ss [MAX_LE_X] 1578 >> Q.PAT_X_ASSUM `!e. P e ==> Q e` (MP_TAC o Q.SPEC `n`) 1579 >> Q.PAT_X_ASSUM `!e. P e ==> Q e` (MP_TAC o Q.SPEC `n`) 1580 >> RW_TAC std_ss [] 1581 >> REPEAT (POP_ASSUM MP_TAC) 1582 >> DISCH_THEN (MP_TAC o Q.SPEC `n`) 1583 >> RW_TAC std_ss [abs] 1584 >> REPEAT (POP_ASSUM MP_TAC) 1585 >> REAL_ARITH_TAC); 1586 1587val POW_LE_1 = store_thm 1588 ("POW_LE_1", 1589 ``!p n. 0 < p /\ p <= 1 ==> p pow n <= 1``, 1590 STRIP_TAC 1591 >> Induct 1592 >> RW_TAC std_ss [pow, REAL_LE_REFL] 1593 >> MATCH_MP_TAC REAL_LE_TRANS 1594 >> Q.EXISTS_TAC `p * 1` 1595 >> Reverse CONJ_TAC >- RW_TAC real_ss [] 1596 >> RW_TAC std_ss [REAL_LE_LMUL]); 1597 1598val POW_LE_1_MONO = store_thm 1599 ("POW_LE_1_MONO", 1600 ``!p m n. 0 < p /\ p <= 1 /\ m <= n ==> p pow n <= p pow m``, 1601 RW_TAC std_ss [] 1602 >> POP_ASSUM MP_TAC 1603 >> Q.SPEC_TAC (`n`, `n`) 1604 >> Q.SPEC_TAC (`m`, `m`) 1605 >> HO_MATCH_MP_TAC TRIANGLE_2D_NUM 1606 >> Induct >- RW_TAC real_ss [REAL_LE_REFL] 1607 >> RW_TAC std_ss [ADD_CLAUSES, pow] 1608 >> MATCH_MP_TAC REAL_LE_TRANS 1609 >> Q.EXISTS_TAC `1 * p pow (d + m)` 1610 >> Reverse CONJ_TAC >- RW_TAC real_ss [] 1611 >> RW_TAC std_ss [REAL_LE_RMUL, REAL_POW_LT]); 1612 1613val REAL_LE_MUL_EPSILON = store_thm 1614 ("REAL_LE_MUL_EPSILON", 1615 ``!x y. (!z. 0 < z /\ z < 1 ==> z * x <= y) ==> 1616 x <= y``, 1617 REPEAT STRIP_TAC 1618 >> Cases_on `x = 0` 1619 >- (Q.PAT_X_ASSUM `!z. P z` (MP_TAC o Q.SPEC `1/2`) >> RW_TAC real_ss [REAL_HALF_BETWEEN]) 1620 >> Cases_on `0 < x` 1621 >- (MATCH_MP_TAC REAL_LE_EPSILON 1622 >> RW_TAC std_ss [GSYM REAL_LE_SUB_RADD] 1623 >> Cases_on `e < x` 1624 >- (MATCH_MP_TAC REAL_LE_TRANS 1625 >> Q.EXISTS_TAC `(1-(e/x))*x` 1626 >> CONJ_TAC 1627 >- (RW_TAC real_ss [REAL_SUB_RDISTRIB] >> METIS_TAC [REAL_DIV_RMUL, REAL_LE_REFL]) 1628 >> Q.PAT_X_ASSUM `!z. P z` MATCH_MP_TAC 1629 >> RW_TAC real_ss [REAL_LT_SUB_RADD, REAL_LT_ADDR, REAL_LT_DIV, REAL_LT_SUB_LADD, REAL_LT_1, REAL_LT_IMP_LE]) 1630 >> FULL_SIMP_TAC std_ss [REAL_NOT_LT] 1631 >> MATCH_MP_TAC REAL_LE_TRANS 1632 >> Q.EXISTS_TAC `0` 1633 >> RW_TAC real_ss [REAL_LE_SUB_RADD] 1634 >> MATCH_MP_TAC REAL_LE_TRANS 1635 >> Q.EXISTS_TAC `(1/2)*x` 1636 >> RW_TAC real_ss [REAL_LE_MUL, REAL_LT_IMP_LE]) 1637 >> MATCH_MP_TAC REAL_LE_TRANS 1638 >> Q.EXISTS_TAC `(1/2)*x` 1639 >> RW_TAC real_ss [] 1640 >> RW_TAC std_ss [Once (GSYM REAL_LE_NEG), GSYM REAL_MUL_RNEG] 1641 >> Suff `1/2 * ~x <= 1 * ~x` >- RW_TAC real_ss [] 1642 >> METIS_TAC [REAL_NEG_GT0, REAL_LT_TOTAL, REAL_LE_REFL, REAL_HALF_BETWEEN, REAL_LE_RMUL]); 1643 1644(* ------------------------------------------------------------------------- *) 1645(* ----- Defining real-valued power, log, and log base 2 functions --------- *) 1646(* ------------------------------------------------------------------------- *) 1647 1648val _ = set_fixity "powr" (Infixr 700); 1649 1650val powr_def = Define 1651 `x powr a = exp (a * ln x)`; 1652 1653val logr_def = Define 1654 `logr a x = ln x / ln a`; 1655 1656val lg_def = Define 1657 `lg x = logr 2 x`; 1658 1659 1660val lg_1 = store_thm 1661 ("lg_1", 1662 ``lg 1 = 0``, 1663 RW_TAC real_ss [lg_def, logr_def, LN_1]); 1664 1665 1666val logr_1 = store_thm 1667 ("logr_1", 1668 ``!b. logr b 1 = 0``, 1669 RW_TAC real_ss [logr_def, LN_1]); 1670 1671 1672val lg_nonzero = store_thm 1673 ("lg_nonzero", 1674 ``!x. (~(x = 0)) /\ (0 <= x) ==> 1675 ((~(lg x = 0)) = (~(x = 1)))``, 1676 RW_TAC std_ss [REAL_ARITH ``(~(x = 0)) /\ (0 <= x) = 0 < x``] 1677 >> RW_TAC std_ss [GSYM lg_1] 1678 >> RW_TAC std_ss [lg_def, logr_def, real_div, REAL_EQ_RMUL, REAL_INV_EQ_0] 1679 >> (MP_TAC o Q.SPECL [`2`, `1`]) LN_INJ >> RW_TAC real_ss [LN_1] 1680 >> RW_TAC std_ss [GSYM LN_1] 1681 >> MATCH_MP_TAC LN_INJ 1682 >> RW_TAC real_ss []); 1683 1684val lg_mul = store_thm 1685 ("lg_mul", 1686 ``!x y. 0 < x /\ 0 < y ==> (lg (x * y) = lg x + lg y)``, 1687 RW_TAC real_ss [lg_def, logr_def, LN_MUL]); 1688 1689val logr_mul = store_thm 1690 ("logr_mul", 1691 ``!b x y. 0 < x /\ 0 < y ==> (logr b (x * y) = logr b x + logr b y)``, 1692 RW_TAC real_ss [logr_def, LN_MUL]); 1693 1694val lg_2 = store_thm 1695 ("lg_2", 1696 ``lg 2 = 1``, 1697 RW_TAC real_ss [lg_def, logr_def] 1698 >> MATCH_MP_TAC REAL_DIV_REFL 1699 >> (ASSUME_TAC o Q.SPECL [`1`, `2`]) LN_MONO_LT 1700 >> FULL_SIMP_TAC real_ss [LN_1] 1701 >> ONCE_REWRITE_TAC [EQ_SYM_EQ] 1702 >> MATCH_MP_TAC REAL_LT_IMP_NE 1703 >> ASM_REWRITE_TAC []); 1704 1705val lg_inv = store_thm 1706 ("lg_inv", 1707 ``!x. 0 < x ==> (lg (inv x) = ~ lg x)``, 1708 RW_TAC real_ss [lg_def, logr_def, LN_INV, real_div]); 1709 1710 1711val logr_inv = store_thm 1712 ("logr_inv", 1713 ``!b x. 0 < x ==> (logr b (inv x) = ~ logr b x)``, 1714 RW_TAC real_ss [logr_def, LN_INV, real_div]); 1715 1716 1717val logr_div = store_thm 1718 ("logr_div", 1719 ``!b x y. 0 < x /\ 0 < y ==> 1720 (logr b (x/y) = logr b x - logr b y)``, 1721 RW_TAC real_ss [real_div, logr_mul, logr_inv, GSYM real_sub]); 1722 1723 1724val neg_lg = store_thm 1725 ("neg_lg", 1726 ``!x. 0 < x ==> ((~(lg x)) = lg (inv x))``, 1727 RW_TAC real_ss [lg_def, logr_def, real_div] 1728 >> `~(ln x * inv (ln 2)) = (~ ln x) * inv (ln 2)` by REAL_ARITH_TAC 1729 >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 1730 >> RW_TAC real_ss [REAL_EQ_RMUL] 1731 >> DISJ2_TAC >> ONCE_REWRITE_TAC [EQ_SYM_EQ] >> MATCH_MP_TAC LN_INV 1732 >> RW_TAC std_ss []); 1733 1734val neg_logr = store_thm 1735 ("neg_logr", 1736 ``!b x. 0 < x ==> ((~(logr b x)) = logr b (inv x))``, 1737 RW_TAC real_ss [logr_def, real_div] 1738 >> `~(ln x * inv (ln b)) = (~ ln x) * inv (ln b)` by REAL_ARITH_TAC 1739 >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 1740 >> RW_TAC real_ss [REAL_EQ_RMUL] 1741 >> DISJ2_TAC >> ONCE_REWRITE_TAC [EQ_SYM_EQ] >> MATCH_MP_TAC LN_INV 1742 >> RW_TAC std_ss []); 1743 1744 1745val lg_pow = store_thm 1746 ("lg_pow", 1747 ``!n. lg (2 pow n) = &n``, 1748 RW_TAC real_ss [lg_def, logr_def, LN_POW] 1749 >> `~(ln 2 = 0)` 1750 by (ONCE_REWRITE_TAC [EQ_SYM_EQ] >> MATCH_MP_TAC REAL_LT_IMP_NE 1751 >> MATCH_MP_TAC REAL_LET_TRANS >> Q.EXISTS_TAC `ln 1` >> RW_TAC real_ss [LN_POS, LN_MONO_LT]) 1752 >> RW_TAC real_ss [real_div, GSYM REAL_MUL_ASSOC, REAL_MUL_RINV]); 1753 1754 1755(* ------------------------------------------------------------------------- *) 1756(* --------------------- exp is a convex function -------------------------- *) 1757(* ------------------------------------------------------------------------- *) 1758 1759val convex_fn = Define 1760 `convex_fn = {f | !x y t. (0 <= t /\ t <= 1) ==> f (t * x + (1 - t) * y) <= t * f x + (1 - t) * f y}`; 1761 1762val concave_fn = Define 1763 `concave_fn = {f | (\x. ~ (f x)) IN convex_fn}`; 1764 1765val exp_convex_lemma1 = store_thm 1766 ("exp_convex_lemma1", 1767 ``!t. (t + (1 - t) * exp 0 - exp ((1 - t) * 0) = 0) /\ 1768 (t * exp 0 + (1 - t) - exp (t * 0) = 0)``, 1769 RW_TAC real_ss [EXP_0] >> REAL_ARITH_TAC); 1770 1771val exp_convex_lemma2 = store_thm 1772 ("exp_convex_lemma2", 1773 ``!t x. ((\x. (1 - t) * exp x - exp ((1 - t) * x)) diffl (\x. (1-t) * exp x - (1 - t)*exp ((1-t)*x)) x) x``, 1774 RW_TAC std_ss [] 1775 >> `(\x. (1 - t) * exp x - exp ((1 - t) * x)) = 1776 (\x. (\x. (1 - t) * exp x) x - (\x. exp ((1 - t) * x)) x)` 1777 by RW_TAC std_ss [FUN_EQ_THM] 1778 >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 1779 >> `((1 - t) * exp x - (1 - t) * exp ((1 - t) * x)) = 1780 (\x. (1 - t) * exp x) x - (\x. (1-t) * exp ((1- t) * x)) x` 1781 by RW_TAC std_ss [] 1782 >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 1783 >> Suff `((\x. (1 - t) * exp x) diffl (\x. (1 - t) * exp x) x) x /\ 1784 ((\x. exp ((1 - t) * x)) diffl (\x. (1 - t) * exp ((1 - t) * x)) x) x` 1785 >- METIS_TAC [DIFF_SUB] 1786 >> CONJ_TAC 1787 >- (`(\x. (1 - t) * exp x) x = 0 * exp x + (exp x) * (\x. 1 - t) x` by RW_TAC real_ss [REAL_MUL_COMM] 1788 >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 1789 >> Q.ABBREV_TAC `foo = (0 * exp x + exp x * (\x. 1 - t) x)` 1790 >> `(\x. (1 - t) * exp x) = (\x. (\x. 1 - t) x * exp x)` by RW_TAC std_ss [FUN_EQ_THM] 1791 >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 1792 >> Q.UNABBREV_TAC `foo` 1793 >> MATCH_MP_TAC DIFF_MUL 1794 >> RW_TAC std_ss [DIFF_CONST, DIFF_EXP]) 1795 >> `(\x. exp ((1 - t) * x)) = (\x. exp ((\x. (1-t)*x) x))` by RW_TAC std_ss [FUN_EQ_THM] 1796 >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 1797 >> `(\x. (1 - t) * exp ((1 - t) * x)) x = exp ((\x. (1-t)*x) x) * (1-t)` 1798 by RW_TAC real_ss [REAL_MUL_COMM] 1799 >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 1800 >> Suff `((\x. (1 - t) * x) diffl (1-t)) x` >- METIS_TAC [DIFF_COMPOSITE] 1801 >> `(1 - t) = (1 - t) * 1` by RW_TAC real_ss [] 1802 >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 1803 >> `(\x. (1 - t) * 1 * x) = (\x. (1-t) * (\x. x) x)` by RW_TAC real_ss [FUN_EQ_THM] 1804 >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 1805 >> MATCH_MP_TAC DIFF_CMUL 1806 >> RW_TAC std_ss [DIFF_X]); 1807 1808val exp_convex_lemma3 = store_thm 1809 ("exp_convex_lemma3", 1810 ``!t x. (\x. (1-t) * exp x - exp ((1-t)*x)) contl x``, 1811 METIS_TAC [DIFF_CONT, exp_convex_lemma2]); 1812 1813val exp_convex_lemma4 = store_thm 1814 ("exp_convex_lemma4", 1815 ``!x. 0 < x /\ 0 < t /\ t < 1 ==> 0 < (\x. (1-t) * exp x - (1 - t)*exp ((1-t)*x)) x``, 1816 RW_TAC real_ss [REAL_LT_SUB_LADD] >> MATCH_MP_TAC REAL_LT_LMUL_IMP 1817 >> RW_TAC real_ss [REAL_LT_SUB_LADD, EXP_MONO_LT, REAL_SUB_RDISTRIB] 1818 >> RW_TAC real_ss [REAL_LT_SUB_RADD, REAL_LT_ADDR] >> MATCH_MP_TAC REAL_LT_MUL 1819 >> RW_TAC real_ss []); 1820 1821val exp_convex_lemma5 = store_thm 1822 ("exp_convex_lemma5", 1823 ``!f f' i j. (!x. (f diffl f' x) x) /\ 1824 (!x. f contl x) /\ 1825 (0 <= i /\ i < j) /\ 1826 (!x. i < x /\ x < j ==> 0 < f' x) ==> 1827 f i < f j``, 1828 REPEAT STRIP_TAC 1829 >> MATCH_MP_TAC REAL_LET_TRANS >> Q.EXISTS_TAC `0 + f i` >> CONJ_TAC >- RW_TAC real_ss [] 1830 >> RW_TAC real_ss [GSYM REAL_LT_SUB_LADD] 1831 >> `?l z. i < z /\ z < j /\ (f diffl l) z /\ (f j - f i = (j - i) * l)` 1832 by (MATCH_MP_TAC MVT >> METIS_TAC [differentiable]) 1833 >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 1834 >> MATCH_MP_TAC REAL_LT_MUL 1835 >> RW_TAC real_ss [REAL_LT_SUB_LADD] 1836 >> `l = f' z` 1837 by (MATCH_MP_TAC DIFF_UNIQ >> Q.EXISTS_TAC `f` >> Q.EXISTS_TAC `z` >> RW_TAC std_ss []) 1838 >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 1839 >> Q.PAT_X_ASSUM `!x. i < x /\ x < j ==> 0 < f' x` MATCH_MP_TAC >> RW_TAC std_ss []); 1840 1841val exp_convex_lemma6 = store_thm 1842 ("exp_convex_lemma6", 1843 ``!x y t. 0 < t /\ t < 1 /\ x < y ==> 1844 exp (t * x + (1 - t) * y) <= t * exp x + (1 - t) * exp y``, 1845 REPEAT STRIP_TAC 1846 >> Q.ABBREV_TAC `z = y - x` 1847 >> `0 < z` by (Q.UNABBREV_TAC `z` >> RW_TAC real_ss [REAL_LT_SUB_LADD]) 1848 >> Suff `exp (t * x + (1 - t) * (x+z)) <= t * exp x + (1 - t) * exp (x+z)` 1849 >- (Q.UNABBREV_TAC `z` >> RW_TAC real_ss []) 1850 >> `t * x + (1 - t) * (x + z) = x + (1 - t) * z` by REAL_ARITH_TAC 1851 >> ASM_REWRITE_TAC [] >> POP_ASSUM (K ALL_TAC) 1852 >> PURE_REWRITE_TAC [transcTheory.EXP_ADD] 1853 >> `t * exp x + (1 - t) * (exp x * exp z) = exp x * (t + (1 - t) * exp z)` 1854 by REAL_ARITH_TAC 1855 >> ASM_REWRITE_TAC [] >> POP_ASSUM (K ALL_TAC) 1856 >> MATCH_MP_TAC REAL_LE_LMUL_IMP >> CONJ_TAC >- SIMP_TAC std_ss [EXP_POS_LE] 1857 >> MATCH_MP_TAC REAL_LE_TRANS >> Q.EXISTS_TAC `0 + exp ((1 - t) * z)` >> CONJ_TAC >- RW_TAC real_ss [] 1858 >> ONCE_REWRITE_TAC [GSYM REAL_LE_SUB_LADD] 1859 >> MATCH_MP_TAC REAL_LT_IMP_LE 1860 >> MATCH_MP_TAC REAL_LET_TRANS >> Q.EXISTS_TAC `t + (1 - t) * exp 0 - exp ((1 - t) * 0)` 1861 >> CONJ_TAC >- RW_TAC real_ss [exp_convex_lemma1] 1862 >> `t + (1 - t) * exp 0 - exp ((1 - t) * 0) = ((1 - t) * exp 0 - exp ((1 - t) * 0)) + t` 1863 by REAL_ARITH_TAC >> ASM_REWRITE_TAC [] >> POP_ASSUM (K ALL_TAC) 1864 >> ONCE_REWRITE_TAC [REAL_LT_ADD_SUB] 1865 >> `t + (1 - t) * exp z - exp ((1 - t) * z) - t = (1 - t) * exp z - exp ((1 - t) * z)` 1866 by REAL_ARITH_TAC 1867 >> ASM_REWRITE_TAC [] >> POP_ASSUM (K ALL_TAC) 1868 >> Q.ABBREV_TAC `f = (\x. (1-t) * exp x - exp ((1-t)*x))` 1869 >> Suff `f 0 < f z` >- (Q.UNABBREV_TAC `f` >> RW_TAC std_ss []) 1870 >> MATCH_MP_TAC exp_convex_lemma5 1871 >> Q.EXISTS_TAC `(\x. (1-t) * exp x - (1 - t)*exp ((1-t)*x))` 1872 >> Q.UNABBREV_TAC `f` 1873 >> RW_TAC real_ss [exp_convex_lemma2, exp_convex_lemma3, exp_convex_lemma4]); 1874 1875val exp_convex = store_thm 1876 ("exp_convex", 1877 ``exp IN convex_fn``, 1878 RW_TAC std_ss [convex_fn, EXTENSION, MEM, NOT_IN_EMPTY, GSPECIFICATION] 1879 >> Cases_on `t = 0` >- RW_TAC real_ss [] 1880 >> Cases_on `t = 1` >- RW_TAC real_ss [] 1881 >> `0 < t /\ t < 1` by METIS_TAC [REAL_LT_LE] 1882 >> Cases_on `x = y` >- RW_TAC real_ss [] 1883 >> (MP_TAC o Q.SPECL [`x`, `y`]) REAL_LT_TOTAL >> RW_TAC std_ss [] 1884 >- (MATCH_MP_TAC exp_convex_lemma6 >> RW_TAC std_ss []) 1885 >> Q.ABBREV_TAC `t' = 1 - t` 1886 >> `t = 1 - t'` by (Q.UNABBREV_TAC `t'` >> REAL_ARITH_TAC) 1887 >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 1888 >> `0 < t'` by (Q.UNABBREV_TAC `t'` >> RW_TAC real_ss [REAL_LT_SUB_LADD]) 1889 >> `t' < 1` by (Q.UNABBREV_TAC `t'` >> RW_TAC real_ss [REAL_LT_SUB_RADD, REAL_LT_ADDR]) 1890 >> ONCE_REWRITE_TAC [REAL_ADD_COMM] 1891 >> MATCH_MP_TAC exp_convex_lemma6 >> RW_TAC std_ss []); 1892 1893(* ------------------------------------------------------------------------- *) 1894(* ------------ ln and lg are concave on (0,infty] ------------------------- *) 1895(* ------------------------------------------------------------------------- *) 1896 1897val pos_convex_fn = Define 1898 `pos_convex_fn = {f | !x y t. (0 < x /\ 0 < y /\ 0 <= t /\ t <= 1) ==> 1899 f (t * x + (1 - t) * y) <= t * f x + (1 - t) * f y}`; 1900 1901val pos_concave_fn = Define 1902 `pos_concave_fn = {f | (\x. ~ (f x)) IN pos_convex_fn}`; 1903 1904val pos_concave_ln = store_thm 1905 ("pos_concave_ln", 1906 ``ln IN pos_concave_fn``, 1907 RW_TAC std_ss [pos_concave_fn, pos_convex_fn, EXTENSION, MEM, NOT_IN_EMPTY, GSPECIFICATION] 1908 >> Cases_on `t = 0` >- RW_TAC real_ss [] 1909 >> Cases_on `t = 1` >- RW_TAC real_ss [] 1910 >> `0 < t /\ t < 1` by RW_TAC std_ss [REAL_LT_LE] 1911 >> `t * ~ln x + (1 - t) * ~ln y = ~ (t * ln x + (1 - t)* ln y)` by REAL_ARITH_TAC 1912 >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 1913 >> RW_TAC std_ss [REAL_LE_NEG, ln] 1914 >> MATCH_MP_TAC SELECT_ELIM_THM 1915 >> RW_TAC std_ss [] >- (MATCH_MP_TAC EXP_TOTAL 1916 >> MATCH_MP_TAC REAL_LT_ADD >> CONJ_TAC >> MATCH_MP_TAC REAL_LT_MUL 1917 >> RW_TAC real_ss [GSYM REAL_LT_ADD_SUB]) 1918 >> Suff `(\v. t * v + (1 - t) * (@u. exp u = y) <= x') (@u. exp u = x)` 1919 >- RW_TAC std_ss [] 1920 >> MATCH_MP_TAC SELECT_ELIM_THM 1921 >> RW_TAC std_ss [] >- (MATCH_MP_TAC EXP_TOTAL >> RW_TAC std_ss []) 1922 >> Suff `(\v. t * x'' + (1 - t) * v <= x') (@u. exp u = y)` 1923 >- RW_TAC std_ss [] 1924 >> MATCH_MP_TAC SELECT_ELIM_THM 1925 >> RW_TAC std_ss [] >- (MATCH_MP_TAC EXP_TOTAL >> RW_TAC std_ss []) 1926 >> ONCE_REWRITE_TAC [GSYM EXP_MONO_LE] 1927 >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 1928 >> MP_TAC exp_convex >> RW_TAC std_ss [convex_fn, EXTENSION, MEM, NOT_IN_EMPTY, GSPECIFICATION]); 1929 1930val pos_concave_lg = store_thm 1931 ("pos_concave_lg", 1932 ``lg IN pos_concave_fn``, 1933 RW_TAC std_ss [lg_def, logr_def, pos_concave_fn, pos_convex_fn, EXTENSION, MEM, NOT_IN_EMPTY, GSPECIFICATION] 1934 >> `~(ln (t * x + (1 - t) * y) / ln 2) = 1935 (inv (ln 2))*(~(ln (t * x + (1 - t) * y)))` by (RW_TAC real_ss [real_div] >> REAL_ARITH_TAC) 1936 >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 1937 >> `t * ~(ln x / ln 2) + (1 - t) * ~(ln y / ln 2) = 1938 (inv (ln 2)) * (t * ~ ln x + (1-t) * ~ln y)` by (RW_TAC real_ss [real_div] >> REAL_ARITH_TAC) 1939 >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 1940 >> MATCH_MP_TAC REAL_LE_LMUL_IMP 1941 >> CONJ_TAC >- (RW_TAC real_ss [REAL_LE_INV_EQ] >> MATCH_MP_TAC LN_POS >> RW_TAC real_ss []) 1942 >> MP_TAC pos_concave_ln 1943 >> RW_TAC std_ss [pos_concave_fn, pos_convex_fn, EXTENSION, MEM, NOT_IN_EMPTY, GSPECIFICATION]); 1944 1945 1946val pos_concave_logr = store_thm 1947 ("pos_concave_logr", 1948 ``!b. 1 <= b ==> (logr b) IN pos_concave_fn``, 1949 RW_TAC std_ss [logr_def, pos_concave_fn, pos_convex_fn, EXTENSION, MEM, NOT_IN_EMPTY, GSPECIFICATION] 1950 >> `~(ln (t * x + (1 - t) * y) / ln b) = 1951 (inv (ln b))*(~(ln (t * x + (1 - t) * y)))` by (RW_TAC real_ss [real_div] >> REAL_ARITH_TAC) 1952 >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 1953 >> `t * ~(ln x / ln b) + (1 - t) * ~(ln y / ln b) = 1954 (inv (ln b)) * (t * ~ ln x + (1-t) * ~ln y)` by (RW_TAC real_ss [real_div] >> REAL_ARITH_TAC) 1955 >> POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]) 1956 >> MATCH_MP_TAC REAL_LE_LMUL_IMP 1957 >> CONJ_TAC >- (RW_TAC real_ss [REAL_LE_INV_EQ] >> MATCH_MP_TAC LN_POS >> RW_TAC real_ss []) 1958 >> MP_TAC pos_concave_ln 1959 >> RW_TAC std_ss [pos_concave_fn, pos_convex_fn, EXTENSION, MEM, NOT_IN_EMPTY, GSPECIFICATION]); 1960 1961(* ------------------------------------------------------------------------- *) 1962(* ---- jensen's inequality ------------ *) 1963(* ------------------------------------------------------------------------- *) 1964 1965val jensen_convex_SIGMA = store_thm 1966 ("jensen_convex_SIGMA", 1967 ``!s. FINITE s ==> 1968 !f g g'. (SIGMA g s = 1) /\ 1969 (!x. x IN s ==> 0 <= g x /\ g x <= 1) /\ 1970 f IN convex_fn ==> 1971 f (SIGMA (\x. g x * g' x) s) <= SIGMA (\x. g x * f (g' x)) s``, 1972 Suff `!s. FINITE s ==> 1973 (\s. !f g g'. (SIGMA g s = 1) /\ 1974 (!x. x IN s ==> 0 <= g x /\ g x <= 1) /\ 1975 f IN convex_fn ==> 1976 f (SIGMA (\x. g x * g' x) s) <= SIGMA (\x. g x * f (g' x)) s) s` 1977 >- RW_TAC std_ss [] 1978 >> MATCH_MP_TAC FINITE_INDUCT 1979 >> RW_TAC real_ss [REAL_SUM_IMAGE_THM, DELETE_NON_ELEMENT, IN_INSERT, DISJ_IMP_THM, FORALL_AND_THM] 1980 >> Cases_on `g e = 0` >- FULL_SIMP_TAC real_ss [] 1981 >> Cases_on `g e = 1` 1982 >- ( FULL_SIMP_TAC real_ss [] 1983 >> Know `!s. FINITE s ==> 1984 (\s. !g. (SIGMA g s = 0) /\ (!x. x IN s ==> 0 <= g x /\ g x <= 1) ==> 1985 (!x. x IN s ==> (g x = 0))) s` 1986 >- (MATCH_MP_TAC FINITE_INDUCT 1987 >> RW_TAC real_ss [REAL_SUM_IMAGE_THM, DELETE_NON_ELEMENT, IN_INSERT, DISJ_IMP_THM, 1988 FORALL_AND_THM, NOT_IN_EMPTY] (* 2 sub-goals *) 1989 >- (Know `!(x:real) y. 0 <= x /\ 0 <= y /\ (x + y = 0) ==> ((x = 0) /\ (y = 0))` 1990 >- REAL_ARITH_TAC 1991 >> PROVE_TAC [REAL_SUM_IMAGE_POS]) 1992 >> 1993 ( Know `!(x:real) y. 0 <= x /\ 0 <= y /\ (x + y = 0) ==> ((x = 0) /\ (y = 0))` 1994 >- REAL_ARITH_TAC 1995 >> Q.PAT_X_ASSUM `!g. (SIGMA g s' = 0) /\ (!x. x IN s' ==> 0 <= g x /\ g x <= 1) ==> 1996 !x. x IN s' ==> (g x = 0)` 1997 (MP_TAC o Q.SPEC `g'`) 1998 >> PROVE_TAC [REAL_SUM_IMAGE_POS] )) 1999 >> Know `!x:real. (1 + x = 1) = (x = 0)` >- REAL_ARITH_TAC 2000 >> STRIP_TAC >> FULL_SIMP_TAC real_ss [] 2001 >> POP_ASSUM (K ALL_TAC) 2002 >> (ASSUME_TAC o UNDISCH o Q.SPEC `s`) REAL_SUM_IMAGE_IN_IF 2003 >> POP_ORW 2004 >> DISCH_TAC 2005 >> POP_ASSUM (ASSUME_TAC o UNDISCH_ALL o (REWRITE_RULE [GSYM AND_IMP_INTRO]) o 2006 (Q.SPEC `g`) o UNDISCH o (Q.SPEC `s`)) 2007 >> `(\x. (if x IN s then (\x. g x * g' x) x else 0)) = (\x. 0)` 2008 by RW_TAC real_ss [FUN_EQ_THM] 2009 >> POP_ORW 2010 >> `(\x. (if x IN s then (\x. g x * f (g' x)) x else 0)) = (\x. 0)` 2011 by RW_TAC real_ss [FUN_EQ_THM] 2012 >> POP_ORW 2013 >> Suff `SIGMA (\x. 0) s = 0` >- RW_TAC real_ss [] 2014 >> (MP_TAC o Q.SPECL [`(\x. 0)`, `0`] o 2015 UNDISCH o Q.SPEC `s`) REAL_SUM_IMAGE_FINITE_CONST 2016 >> RW_TAC real_ss []) 2017 2018 >> Suff `(SIGMA (\x. g x * g' x) s = (1 - g e) * SIGMA (\x. (g x / (1 - g e)) * g' x) s) /\ 2019 (SIGMA (\x. g x * f(g' x)) s = (1 - g e) * SIGMA (\x. (g x / (1 - g e)) * f(g' x)) s)` 2020 >- (RW_TAC std_ss [] >> FULL_SIMP_TAC std_ss [convex_fn, GSPECIFICATION] 2021 >> Q.PAT_X_ASSUM `!f' g'' g'''. 2022 (SIGMA g'' s = 1) /\ 2023 (!x. x IN s ==> 0 <= g'' x /\ g'' x <= 1) /\ 2024 (!x y t. 2025 0 <= t /\ t <= 1 ==> 2026 f' (t * x + (1 - t) * y) <= t * f' x + (1 - t) * f' y) ==> 2027 f' (SIGMA (\x. g'' x * g''' x) s) <= 2028 SIGMA (\x. g'' x * f' (g''' x)) s` (MP_TAC o Q.SPECL [`f`, `(\x. g x / (1 - g e))`, `g'`]) 2029 >> RW_TAC std_ss [] 2030 >> Q.PAT_X_ASSUM `!x y t. P` 2031 (MP_TAC o Q.SPECL [`g' e`, `SIGMA (\x. g x / (1 - g e) * g' x) s`, `g e`]) 2032 >> RW_TAC std_ss [] 2033 >> MATCH_MP_TAC REAL_LE_TRANS 2034 >> Q.EXISTS_TAC `g e * f (g' e) + (1 - g e) * f (SIGMA (\x. g x / (1 - g e) * g' x) s)` 2035 >> RW_TAC real_ss [REAL_LE_LADD] 2036 >> Cases_on `g e = 1` >- RW_TAC real_ss [] 2037 >> Know `0 < 1 - g e` 2038 >- (Q.PAT_X_ASSUM `g e <= 1` MP_TAC >> Q.PAT_X_ASSUM `~ (g e = 1)` MP_TAC >> REAL_ARITH_TAC) 2039 >> STRIP_TAC 2040 >> Suff `f (SIGMA (\x. g x / (1 - g e) * g' x) s) <= 2041 SIGMA (\x. g x / (1 - g e) * f (g' x)) s` 2042 >- PROVE_TAC [REAL_LE_LMUL] 2043 >> Q.PAT_X_ASSUM `(SIGMA (\x. g x / (1 - g e)) s = 1) /\ 2044 (!x. x IN s ==> 0 <= g x / (1 - g e) /\ g x / (1 - g e) <= 1) ==> 2045 f (SIGMA (\x. g x / (1 - g e) * g' x) s) <= 2046 SIGMA (\x. g x / (1 - g e) * f (g' x)) s` MATCH_MP_TAC 2047 >> CONJ_TAC 2048 >- ((MP_TAC o Q.SPECL [`g`, `inv (1- g e)`] o UNDISCH o Q.SPEC `s`) REAL_SUM_IMAGE_CMUL 2049 >> RW_TAC real_ss [real_div] >> ASM_REWRITE_TAC [Once REAL_MUL_COMM] 2050 >> RW_TAC std_ss [Once REAL_MUL_COMM, GSYM real_div] 2051 >> Suff `SIGMA g s = 1 * (1 - g e)` 2052 >- PROVE_TAC [REAL_EQ_LDIV_EQ] 2053 >> Q.PAT_X_ASSUM `g e + SIGMA g s = 1` MP_TAC 2054 >> REAL_ARITH_TAC) 2055 >> RW_TAC std_ss [] >- PROVE_TAC [REAL_LE_DIV, REAL_LT_IMP_LE] 2056 >> Suff `g x <= 1 * (1 - g e)` >- PROVE_TAC [REAL_LE_LDIV_EQ] 2057 >> Suff `g e + g x <= 1` >- REAL_ARITH_TAC 2058 >> Q.PAT_X_ASSUM `g e + SIGMA g s = 1` (fn thm => ONCE_REWRITE_TAC [GSYM thm]) 2059 >> MATCH_MP_TAC REAL_LE_ADD2 2060 >> PROVE_TAC [REAL_LE_REFL, REAL_SUM_IMAGE_POS_MEM_LE]) 2061 >> Know `~(1-g e = 0)` >- (POP_ASSUM MP_TAC >> REAL_ARITH_TAC) 2062 >> RW_TAC real_ss [(REWRITE_RULE [Once EQ_SYM_EQ] o UNDISCH o Q.SPEC `s`) REAL_SUM_IMAGE_CMUL, 2063 REAL_MUL_ASSOC, REAL_DIV_LMUL]); 2064 2065val jensen_concave_SIGMA = store_thm 2066 ("jensen_concave_SIGMA", 2067 ``!s. FINITE s ==> 2068 !f g g'. (SIGMA g s = 1) /\ 2069 (!x. x IN s ==> 0 <= g x /\ g x <= 1) /\ 2070 f IN concave_fn ==> 2071 SIGMA (\x. g x * f (g' x)) s <= f (SIGMA (\x. g x * g' x) s)``, 2072 REPEAT STRIP_TAC 2073 >> ONCE_REWRITE_TAC [GSYM REAL_LE_NEG2] 2074 >> RW_TAC std_ss [(REWRITE_RULE [Once EQ_SYM_EQ]) REAL_SUM_IMAGE_NEG] 2075 >> Suff `(\x. ~ f x) (SIGMA (\x. g x * g' x) s) <= 2076 SIGMA (\x. g x * (\x. ~ f x) (g' x)) s` 2077 >- RW_TAC real_ss [] 2078 >> Q.ABBREV_TAC `f' = (\x. ~f x)` 2079 >> (MATCH_MP_TAC o UNDISCH o Q.SPEC `s`) jensen_convex_SIGMA 2080 >> Q.UNABBREV_TAC `f'` 2081 >> FULL_SIMP_TAC std_ss [concave_fn, GSPECIFICATION]); 2082 2083val jensen_pos_convex_SIGMA = store_thm 2084 ("jensen_pos_convex_SIGMA", 2085 ``!s. FINITE s ==> 2086 !f g g'. (SIGMA g s = 1) /\ 2087 (!x. x IN s ==> 0 <= g x /\ g x <= 1) /\ 2088 (!x. x IN s ==> (0 < g x ==> 0 < g' x)) /\ 2089 f IN pos_convex_fn ==> 2090 f (SIGMA (\x. g x * g' x) s) <= SIGMA (\x. g x * f (g' x)) s``, 2091 Suff `!s. FINITE s ==> 2092 (\s. !f g g'. (SIGMA g s = 1) /\ 2093 (!x. x IN s ==> 0 <= g x /\ g x <= 1) /\ 2094 (!x. x IN s ==> (0 < g x ==> 0 < g' x)) /\ 2095 f IN pos_convex_fn ==> 2096 f (SIGMA (\x. g x * g' x) s) <= SIGMA (\x. g x * f (g' x)) s) s` 2097 >- RW_TAC std_ss [] 2098 >> MATCH_MP_TAC FINITE_INDUCT 2099 >> RW_TAC real_ss [REAL_SUM_IMAGE_THM, DELETE_NON_ELEMENT, IN_INSERT, DISJ_IMP_THM, FORALL_AND_THM] 2100 >> Cases_on `g e = 0` >- FULL_SIMP_TAC real_ss [] 2101 >> Cases_on `g e = 1` 2102 >- ( FULL_SIMP_TAC real_ss [] 2103 >> Know `!s. FINITE s ==> 2104 (\s. !g. (SIGMA g s = 0) /\ (!x. x IN s ==> 0 <= g x /\ g x <= 1) ==> 2105 (!x. x IN s ==> (g x = 0))) s` 2106 >- (MATCH_MP_TAC FINITE_INDUCT 2107 >> RW_TAC real_ss [REAL_SUM_IMAGE_THM, DELETE_NON_ELEMENT, IN_INSERT, DISJ_IMP_THM, 2108 FORALL_AND_THM, NOT_IN_EMPTY] (* 2 sub-goals *) 2109 >- (Know `!(x:real) y. 0 <= x /\ 0 <= y /\ (x + y = 0) ==> ((x = 0) /\ (y = 0))` 2110 >- REAL_ARITH_TAC 2111 >> PROVE_TAC [REAL_SUM_IMAGE_POS]) 2112 >> 2113 ( Know `!(x:real) y. 0 <= x /\ 0 <= y /\ (x + y = 0) ==> ((x = 0) /\ (y = 0))` 2114 >- REAL_ARITH_TAC 2115 >> Q.PAT_X_ASSUM `!g. (SIGMA g s' = 0) /\ (!x. x IN s' ==> 0 <= g x /\ g x <= 1) ==> 2116 !x. x IN s' ==> (g x = 0)` 2117 (MP_TAC o Q.SPEC `g''`) 2118 >> PROVE_TAC [REAL_SUM_IMAGE_POS] )) 2119 >> Know `!x:real. (1 + x = 1) = (x = 0)` >- REAL_ARITH_TAC 2120 >> STRIP_TAC >> FULL_SIMP_TAC real_ss [] 2121 >> POP_ASSUM (K ALL_TAC) 2122 >> (ASSUME_TAC o UNDISCH o Q.SPEC `s`) REAL_SUM_IMAGE_IN_IF 2123 >> POP_ORW 2124 >> DISCH_TAC 2125 >> POP_ASSUM (ASSUME_TAC o UNDISCH_ALL o REWRITE_RULE [GSYM AND_IMP_INTRO] o 2126 (Q.SPEC `g`) o UNDISCH o (Q.SPEC `s`)) 2127 >> `(\x. (if x IN s then (\x. g x * g' x) x else 0)) = (\x. 0)` 2128 by RW_TAC real_ss [FUN_EQ_THM] 2129 >> POP_ORW 2130 >> `(\x. (if x IN s then (\x. g x * f (g' x)) x else 0)) = (\x. 0)` 2131 by RW_TAC real_ss [FUN_EQ_THM] 2132 >> POP_ORW 2133 >> Suff `SIGMA (\x. 0) s = 0` >- RW_TAC real_ss [] 2134 >> (MP_TAC o Q.SPECL [`(\x. 0)`, `0`] o 2135 UNDISCH o Q.SPEC `s`) REAL_SUM_IMAGE_FINITE_CONST 2136 >> RW_TAC real_ss []) 2137 >> Suff `(SIGMA (\x. g x * g' x) s = (1 - g e) * SIGMA (\x. (g x / (1 - g e)) * g' x) s) /\ 2138 (SIGMA (\x. g x * f(g' x)) s = (1 - g e) * SIGMA (\x. (g x / (1 - g e)) * f(g' x)) s)` 2139 >- (RW_TAC std_ss [] >> FULL_SIMP_TAC std_ss [pos_convex_fn, GSPECIFICATION] 2140 >> Q.PAT_X_ASSUM `!f' g'' g'''. 2141 (SIGMA g'' s = 1) /\ 2142 (!x. x IN s ==> 0 <= g'' x /\ g'' x <= 1) /\ 2143 (!x. x IN s ==> 0 < g'' x ==> 0 < g''' x) /\ 2144 (!x y t. 2145 0 < x /\ 0 < y /\ 0 <= t /\ t <= 1 ==> 2146 f' (t * x + (1 - t) * y) <= t * f' x + (1 - t) * f' y) ==> 2147 f' (SIGMA (\x. g'' x * g''' x) s) <= 2148 SIGMA (\x. g'' x * f' (g''' x)) s` (MP_TAC o Q.SPECL [`f`, `(\x. g x / (1 - g e))`, `g'`]) 2149 >> RW_TAC std_ss [] 2150 >> Know `0 < 1 - g e` 2151 >- (Q.PAT_X_ASSUM `g e <= 1` MP_TAC >> Q.PAT_X_ASSUM `~ (g e = 1)` MP_TAC >> REAL_ARITH_TAC) 2152 >> STRIP_TAC 2153 >> Know `SIGMA (\x. g x / (1 - g e)) s = 1` 2154 >- ((MP_TAC o Q.SPECL [`g`, `inv (1- g e)`] o UNDISCH o Q.SPEC `s`) REAL_SUM_IMAGE_CMUL 2155 >> RW_TAC real_ss [real_div] >> ASM_REWRITE_TAC [Once REAL_MUL_COMM] 2156 >> RW_TAC std_ss [Once REAL_MUL_COMM, GSYM real_div] 2157 >> Suff `SIGMA g s = 1 * (1 - g e)` 2158 >- PROVE_TAC [REAL_EQ_LDIV_EQ] 2159 >> Q.PAT_X_ASSUM `g e + SIGMA g s = 1` MP_TAC 2160 >> REAL_ARITH_TAC) 2161 >> STRIP_TAC 2162 >> FULL_SIMP_TAC std_ss [] 2163 >> Cases_on `s = {}` >- FULL_SIMP_TAC real_ss [REAL_SUM_IMAGE_THM] 2164 >> Know `0 < SIGMA (\x. g x / (1 - g e) * g' x) s` 2165 >- ( RW_TAC std_ss [REAL_LT_LE] 2166 >- ((MATCH_MP_TAC o UNDISCH o REWRITE_RULE [GSYM AND_IMP_INTRO] o 2167 Q.SPECL [`(\x. g x / (1 - g e) * g' x)`,`s`]) REAL_SUM_IMAGE_POS 2168 >> RW_TAC real_ss [] >> Cases_on `g x = 0` >- RW_TAC real_ss [] 2169 >> MATCH_MP_TAC REAL_LE_MUL 2170 >> Reverse CONJ_TAC >- PROVE_TAC [REAL_LT_IMP_LE, REAL_LT_LE] 2171 >> RW_TAC real_ss [] >> MATCH_MP_TAC REAL_LE_DIV 2172 >> RW_TAC real_ss [] >> PROVE_TAC [REAL_LT_IMP_LE]) 2173 >> Q.PAT_X_ASSUM `SIGMA (\x. g x * g' x) s = 2174 (1 - g e) * SIGMA (\x. g x / (1 - g e) * g' x) s` 2175 (MP_TAC o REWRITE_RULE [Once REAL_MUL_COMM] o GSYM) 2176 >> RW_TAC std_ss [GSYM REAL_EQ_RDIV_EQ] 2177 >> RW_TAC std_ss [real_div, REAL_ENTIRE, REAL_INV_EQ_0, REAL_LT_IMP_NE] 2178 >> SPOSE_NOT_THEN STRIP_ASSUME_TAC 2179 >> Know `!s. FINITE s ==> 2180 (\s. !g g'. (!x. x IN s ==> 0 <= g x) /\ (!x. x IN s ==> 0 < g x ==> 0 < g' x) /\ 2181 (SIGMA (\x. g x * g' x) s = 0) ==> 2182 (!x. x IN s ==> (g x = 0))) s` 2183 >- ( REPEAT (POP_ASSUM (K ALL_TAC)) 2184 >> MATCH_MP_TAC FINITE_INDUCT 2185 >> RW_TAC std_ss [REAL_SUM_IMAGE_THM, NOT_IN_EMPTY, DELETE_NON_ELEMENT, 2186 IN_INSERT, Once DISJ_IMP_THM, Once FORALL_AND_THM] 2187 >- ( SPOSE_NOT_THEN STRIP_ASSUME_TAC 2188 >> Cases_on `SIGMA (\x. g x * g' x) s = 0` 2189 >- ( FULL_SIMP_TAC real_ss [REAL_ENTIRE] \\ 2190 PROVE_TAC [REAL_LT_IMP_NE, REAL_LT_LE] ) 2191 >> `0 < g e * g' e + SIGMA (\x. g x * g' x) s` 2192 by (MATCH_MP_TAC REAL_LT_ADD 2193 >> CONJ_TAC 2194 >- (MATCH_MP_TAC REAL_LT_MUL >> PROVE_TAC [REAL_LT_LE]) 2195 >> RW_TAC std_ss [REAL_LT_LE] 2196 >> (MATCH_MP_TAC o UNDISCH o REWRITE_RULE [GSYM AND_IMP_INTRO] o 2197 Q.SPECL [`(\x. g x * g' x)`,`s`]) REAL_SUM_IMAGE_POS 2198 >> RW_TAC std_ss [] 2199 >> Cases_on `g x = 0` >- RW_TAC real_ss [] 2200 >> PROVE_TAC [REAL_LE_MUL, REAL_LT_IMP_LE, REAL_LT_LE]) 2201 >> PROVE_TAC [REAL_LT_IMP_NE] ) 2202 >> Cases_on `SIGMA (\x. g x * g' x) s = 0` 2203 >- METIS_TAC [] 2204 >> Cases_on `g e = 0` 2205 >- FULL_SIMP_TAC real_ss [] 2206 >> `0 < g e * g' e + SIGMA (\x. g x * g' x) s` 2207 by (MATCH_MP_TAC REAL_LT_ADD 2208 >> CONJ_TAC 2209 >- (MATCH_MP_TAC REAL_LT_MUL >> METIS_TAC [REAL_LT_LE]) 2210 >> RW_TAC std_ss [REAL_LT_LE] 2211 >> (MATCH_MP_TAC o UNDISCH o REWRITE_RULE [GSYM AND_IMP_INTRO] o 2212 Q.SPECL [`(\x. g x * g' x)`,`s`]) REAL_SUM_IMAGE_POS 2213 >> RW_TAC std_ss [] 2214 >> Cases_on `g x' = 0` >- RW_TAC real_ss [] 2215 >> PROVE_TAC [REAL_LE_MUL, REAL_LT_IMP_LE, REAL_LT_LE]) 2216 >> METIS_TAC [REAL_LT_IMP_NE] ) 2217 >> DISCH_TAC 2218 >> POP_ASSUM (ASSUME_TAC o UNDISCH o Q.SPEC `s`) 2219 >> FULL_SIMP_TAC std_ss [IMP_CONJ_THM, Once FORALL_AND_THM] 2220 >> POP_ASSUM (ASSUME_TAC o UNDISCH_ALL o REWRITE_RULE [GSYM AND_IMP_INTRO] o 2221 (Q.SPECL [`g`,`g'`])) 2222 >> (ASSUME_TAC o Q.SPECL [`(\x. if x IN s then g x else 0)`, `0`] o 2223 UNDISCH o Q.SPEC `s`) REAL_SUM_IMAGE_FINITE_CONST 2224 >> `SIGMA (\x. (if x IN s then g x else 0)) s = SIGMA g s` 2225 by METIS_TAC [GSYM REAL_SUM_IMAGE_IN_IF] 2226 >> FULL_SIMP_TAC real_ss [] ) 2227 >> DISCH_TAC 2228 >> Q.PAT_X_ASSUM `!x y t. P` 2229 (MP_TAC o Q.SPECL [`g' e`, `SIGMA (\x. g x / (1 - g e) * g' x) s`, `g e`]) 2230 >> Know `0 < g' e` >- METIS_TAC [REAL_LT_LE] 2231 >> RW_TAC std_ss [] 2232 >> MATCH_MP_TAC REAL_LE_TRANS 2233 >> Q.EXISTS_TAC `g e * f (g' e) + (1 - g e) * f (SIGMA (\x. g x / (1 - g e) * g' x) s)` 2234 >> RW_TAC real_ss [REAL_LE_LADD] 2235 >> Suff `f (SIGMA (\x. g x / (1 - g e) * g' x) s) <= 2236 SIGMA (\x. g x / (1 - g e) * f (g' x)) s` 2237 >- PROVE_TAC [REAL_LE_LMUL] 2238 >> Q.PAT_X_ASSUM `(!x. x IN s ==> 0 <= g x / (1 - g e) /\ g x / (1 - g e) <= 1) /\ 2239 (!x. x IN s ==> 0 < g x / (1 - g e) ==> 0 < g' x) ==> 2240 f (SIGMA (\x. g x / (1 - g e) * g' x) s) <= 2241 SIGMA (\x. g x / (1 - g e) * f (g' x)) s` MATCH_MP_TAC 2242 >> RW_TAC std_ss [] (* 3 sub-goals *) 2243 >| [PROVE_TAC [REAL_LE_DIV, REAL_LT_IMP_LE], 2244 Suff `g x <= 1 * (1 - g e)` >- PROVE_TAC [REAL_LE_LDIV_EQ] 2245 >> Suff `g e + g x <= 1` >- REAL_ARITH_TAC 2246 >> Q.PAT_X_ASSUM `g e + SIGMA g s = 1` (fn thm => ONCE_REWRITE_TAC [GSYM thm]) 2247 >> MATCH_MP_TAC REAL_LE_ADD2 2248 >> PROVE_TAC [REAL_LE_REFL, REAL_SUM_IMAGE_POS_MEM_LE], 2249 Cases_on `g x = 0` >- FULL_SIMP_TAC real_ss [] 2250 >> PROVE_TAC [REAL_LT_LE] ]) 2251 >> Know `~(1-g e = 0)` >- (POP_ASSUM MP_TAC >> REAL_ARITH_TAC) 2252 >> RW_TAC real_ss [(REWRITE_RULE [Once EQ_SYM_EQ] o UNDISCH o Q.SPEC `s`) REAL_SUM_IMAGE_CMUL, 2253 REAL_MUL_ASSOC, REAL_DIV_LMUL]); 2254 2255val jensen_pos_concave_SIGMA = store_thm 2256 ("jensen_pos_concave_SIGMA", 2257 ``!s. FINITE s ==> 2258 !f g g'. (SIGMA g s = 1) /\ 2259 (!x. x IN s ==> 0 <= g x /\ g x <= 1) /\ 2260 (!x. x IN s ==> (0 < g x ==> 0 < g' x)) /\ 2261 f IN pos_concave_fn ==> 2262 SIGMA (\x. g x * f (g' x)) s <= f (SIGMA (\x. g x * g' x) s)``, 2263 REPEAT STRIP_TAC 2264 >> ONCE_REWRITE_TAC [GSYM REAL_LE_NEG2] 2265 >> RW_TAC std_ss [(REWRITE_RULE [Once EQ_SYM_EQ]) REAL_SUM_IMAGE_NEG] 2266 >> Suff `(\x. ~ f x) (SIGMA (\x. g x * g' x) s) <= 2267 SIGMA (\x. g x * (\x. ~ f x) (g' x)) s` 2268 >- RW_TAC real_ss [] 2269 >> Q.ABBREV_TAC `f' = (\x. ~f x)` 2270 >> (MATCH_MP_TAC o UNDISCH o Q.SPEC `s`) jensen_pos_convex_SIGMA 2271 >> Q.UNABBREV_TAC `f'` 2272 >> FULL_SIMP_TAC std_ss [pos_concave_fn, GSPECIFICATION]); 2273 2274val _ = export_theory (); 2275