1(*===========================================================================*) 2(* Theory of sequences and series of real numbers *) 3(*===========================================================================*) 4 5(* 6app load ["hol88Lib", 7 "numLib", 8 "reduceLib", 9 "PairedLambda", 10 "jrhUtils", 11 "netsTheory"]; 12*) 13 14 15open HolKernel Parse boolLib bossLib numLib reduceLib pairLib 16 pairTheory arithmeticTheory numTheory prim_recTheory 17 jrhUtils realTheory realSimps metricTheory netsTheory BasicProvers; 18 19open combinTheory pred_setTheory res_quanTools realSimps RealArith; 20 21infix THEN THENL ORELSE ORELSEC ##; 22 23val _ = new_theory "seq"; 24 25val num_EQ_CONV = Arithconv.NEQ_CONV; 26 27val S_TAC = rpt (POP_ASSUM MP_TAC) >> rpt RESQ_STRIP_TAC; 28val Strip = S_TAC; 29 30fun K_TAC _ = ALL_TAC; 31val KILL_TAC = POP_ASSUM_LIST K_TAC; 32val Know = Q_TAC KNOW_TAC; 33val Suff = Q_TAC SUFF_TAC; 34val POP_ORW = POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]); 35 36val Cond = 37 MATCH_MP_TAC (PROVE [] ``!a b c. a /\ (b ==> c) ==> ((a ==> b) ==> c)``) 38 >> CONJ_TAC; 39 40local 41 val th = prove (``!a b. a /\ (a ==> b) ==> a /\ b``, PROVE_TAC []) 42in 43 val STRONG_CONJ_TAC :tactic = MATCH_MP_TAC th >> CONJ_TAC 44end; 45 46fun wrap a = [a]; 47val Rewr = DISCH_THEN (REWRITE_TAC o wrap); 48val Rewr' = DISCH_THEN (ONCE_REWRITE_TAC o wrap); 49val std_ss' = std_ss ++ boolSimps.ETA_ss 50 51val _ = add_implicit_rewrites pairTheory.pair_rws; 52 53(*---------------------------------------------------------------------------*) 54(* Specialize net theorems to sequences:num->real *) 55(*---------------------------------------------------------------------------*) 56 57val geq = Term `$>= : num->num->bool`; 58 59val _ = hide "-->"; (* hide previous definition in quotient library *) 60 61val tends_num_real = new_infixr_definition("tends_num_real", 62 ���$--> x x0 = (x tends x0)(mtop(mr1), ^geq)���,750); 63 64val SEQ = store_thm("SEQ", 65 ���!x x0. 66 (x --> x0) = 67 !e. &0 < e 68 ==> ?N. !n. n >= N ==> abs(x(n) - x0) < e���, 69 REPEAT GEN_TAC THEN REWRITE_TAC[tends_num_real, SEQ_TENDS, MR1_DEF] THEN 70 GEN_REWR_TAC (RAND_CONV o ONCE_DEPTH_CONV) [ABS_SUB] 71 THEN REFL_TAC); 72 73val SEQ_CONST = store_thm("SEQ_CONST", 74 ���!k. (\x. k) --> k���, 75 REPEAT GEN_TAC THEN REWRITE_TAC[SEQ, REAL_SUB_REFL, ABS_0] THEN 76 GEN_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[]); 77 78val SEQ_ADD = store_thm("SEQ_ADD", 79 ���!x x0 y y0. x --> x0 /\ y --> y0 ==> (\n. x(n) + y(n)) --> (x0 + y0)���, 80 REPEAT GEN_TAC THEN REWRITE_TAC[tends_num_real] THEN 81 MATCH_MP_TAC NET_ADD THEN MATCH_ACCEPT_TAC DORDER_NGE); 82 83val SEQ_MUL = store_thm("SEQ_MUL", 84 ���!x x0 y y0. x --> x0 /\ y --> y0 ==> (\n. x(n) * y(n)) --> (x0 * y0)���, 85 REPEAT GEN_TAC THEN REWRITE_TAC[tends_num_real] THEN 86 MATCH_MP_TAC NET_MUL THEN MATCH_ACCEPT_TAC DORDER_NGE); 87 88val SEQ_NEG = store_thm("SEQ_NEG", 89 ���!x x0. x --> x0 = (\n. ~(x n)) --> ~x0���, 90 REPEAT GEN_TAC THEN REWRITE_TAC[tends_num_real] THEN 91 MATCH_MP_TAC NET_NEG THEN MATCH_ACCEPT_TAC DORDER_NGE); 92 93val SEQ_INV = store_thm("SEQ_INV", 94 ���!x x0. x --> x0 /\ ~(x0 = &0) ==> (\n. inv(x n)) --> inv x0���, 95 REPEAT GEN_TAC THEN REWRITE_TAC[tends_num_real] THEN 96 MATCH_MP_TAC NET_INV THEN MATCH_ACCEPT_TAC DORDER_NGE); 97 98val SEQ_SUB = store_thm("SEQ_SUB", 99 ���!x x0 y y0. x --> x0 /\ y --> y0 ==> (\n. x(n) - y(n)) --> (x0 - y0)���, 100 REPEAT GEN_TAC THEN REWRITE_TAC[tends_num_real] THEN 101 MATCH_MP_TAC NET_SUB THEN MATCH_ACCEPT_TAC DORDER_NGE); 102 103val SEQ_DIV = store_thm("SEQ_DIV", 104 ���!x x0 y y0. x --> x0 /\ y --> y0 /\ ~(y0 = &0) ==> 105 (\n. x(n) / y(n)) --> (x0 / y0)���, 106 REPEAT GEN_TAC THEN REWRITE_TAC[tends_num_real] THEN 107 MATCH_MP_TAC NET_DIV THEN MATCH_ACCEPT_TAC DORDER_NGE); 108 109val SEQ_UNIQ = store_thm("SEQ_UNIQ", 110 ���!x x1 x2. x --> x1 /\ x --> x2 ==> (x1 = x2)���, 111 REPEAT GEN_TAC THEN REWRITE_TAC[tends_num_real] THEN 112 MATCH_MP_TAC MTOP_TENDS_UNIQ THEN 113 MATCH_ACCEPT_TAC DORDER_NGE); 114 115(*---------------------------------------------------------------------------*) 116(* Define convergence and Cauchy-ness *) 117(*---------------------------------------------------------------------------*) 118 119val convergent = new_definition("convergent", 120 ���convergent f = ?l. f --> l���); 121 122val cauchy = new_definition("cauchy", 123 ���cauchy f = !e. &0 < e ==> 124 ?N:num. !m n. m >= N /\ n >= N ==> abs(f(m) - f(n)) < e���); 125 126val lim = new_definition("lim", 127 ���lim f = @l. f --> l���); 128 129val SEQ_LIM = store_thm("SEQ_LIM", 130 ���!f. convergent f = (f --> lim f)���, 131 GEN_TAC THEN REWRITE_TAC[convergent] THEN EQ_TAC THENL 132 [DISCH_THEN(MP_TAC o SELECT_RULE) THEN REWRITE_TAC[lim], 133 DISCH_TAC THEN EXISTS_TAC ���lim f��� THEN POP_ASSUM ACCEPT_TAC]); 134 135(*---------------------------------------------------------------------------*) 136(* Define a subsequence *) 137(*---------------------------------------------------------------------------*) 138 139val subseq = new_definition("subseq", 140 ���subseq f = !m n:num. m < n ==> f m < (f n):num���); 141 142val SUBSEQ_SUC = store_thm("SUBSEQ_SUC", 143 ���!f. subseq f = !n. f(n) < f(SUC n)���, 144 GEN_TAC THEN REWRITE_TAC[subseq] THEN EQ_TAC THEN DISCH_TAC THENL 145 [X_GEN_TAC ���n:num��� THEN POP_ASSUM MATCH_MP_TAC THEN 146 REWRITE_TAC[LESS_SUC_REFL], 147 REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP LESS_ADD_1) THEN 148 REWRITE_TAC[GSYM ADD1] THEN 149 DISCH_THEN(X_CHOOSE_THEN ���p:num��� SUBST1_TAC) THEN 150 SPEC_TAC(���p:num���,���p:num���) THEN INDUCT_TAC THENL 151 [ALL_TAC, 152 MATCH_MP_TAC LESS_TRANS THEN EXISTS_TAC ���f(m + (SUC p)):num���] THEN 153 ASM_REWRITE_TAC[ADD_CLAUSES]]); 154 155(*---------------------------------------------------------------------------*) 156(* Define monotonicity *) 157(*---------------------------------------------------------------------------*) 158 159val mono = new_definition("mono", 160 ���mono f = (!m n:num. m <= n ==> f(m) <= (f n:real)) 161 \/ 162 (!m n. m <= n ==> f(m) >= f(n))���); 163 164val MONO_SUC = store_thm("MONO_SUC", 165 ���!f:num->real. 166 mono f 167 = 168 (!n. f(SUC n) >= f n) \/ (!n. f(SUC n) <= f(n))���, 169GEN_TAC THEN REWRITE_TAC[mono, real_ge] THEN 170 MATCH_MP_TAC(TAUT_CONV ���(a = c) /\ (b = d) ==> (a \/ b = c \/ d)���) 171 THEN CONJ_TAC THEN (EQ_TAC THENL 172 [DISCH_THEN(MP_TAC o GEN ���n:num��� o 173 SPECL [���n:num���, ���SUC n���]) THEN 174 REWRITE_TAC[LESS_EQ_SUC_REFL], 175 DISCH_TAC THEN REPEAT GEN_TAC THEN 176 DISCH_THEN(X_CHOOSE_THEN ���p:num��� SUBST1_TAC 177 o MATCH_MP LESS_EQUAL_ADD) THEN 178 SPEC_TAC(���p:num���,���p:num���) THEN INDUCT_TAC THEN 179 ASM_REWRITE_TAC[ADD_CLAUSES, REAL_LE_REFL] THEN 180 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC ���f(m + p:num):real��� THEN 181 ASM_REWRITE_TAC[]])); 182 183(*---------------------------------------------------------------------------*) 184(* Simpler characterization of bounded sequence *) 185(*---------------------------------------------------------------------------*) 186 187val MAX_LEMMA = store_thm("MAX_LEMMA", 188 ���!s N. ?k. !n:num. n < N ==> abs(s n) < k���, 189 GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[NOT_LESS_0] THEN 190 POP_ASSUM(X_CHOOSE_TAC ���k:real���) THEN 191 DISJ_CASES_TAC (SPECL [���k:real���, ���abs(s(N:num))���] REAL_LET_TOTAL) THENL 192 [EXISTS_TAC ���abs(s(N:num)) + &1���, EXISTS_TAC ���k:real���] THEN 193 X_GEN_TAC ���n:num��� THEN REWRITE_TAC[LESS_THM] THEN 194 DISCH_THEN(DISJ_CASES_THEN2 SUBST1_TAC MP_TAC) THEN 195 TRY(MATCH_MP_TAC REAL_LT_ADD1) THEN ASM_REWRITE_TAC[REAL_LE_REFL] THEN 196 DISCH_THEN(ANTE_RES_THEN ASSUME_TAC) THEN 197 MATCH_MP_TAC REAL_LT_ADD1 THEN 198 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC ���k:real��� THEN 199 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN 200 ASM_REWRITE_TAC[]); 201 202val SEQ_BOUNDED = store_thm("SEQ_BOUNDED", 203 ���!s. bounded(mr1, ^geq) s = ?k. !n. abs(s n) < k���, 204 GEN_TAC THEN REWRITE_TAC[MR1_BOUNDED] THEN 205 REWRITE_TAC[GREATER_EQ, LESS_EQ_REFL] THEN EQ_TAC THENL 206 [DISCH_THEN(X_CHOOSE_THEN ���k:real��� (X_CHOOSE_TAC ���N:num���)) THEN 207 MP_TAC(SPECL [���s:num->real���, ���N:num���] MAX_LEMMA) THEN 208 DISCH_THEN(X_CHOOSE_TAC ���l:real���) THEN 209 DISJ_CASES_TAC (SPECL [���k:real���, ���l:real���] REAL_LE_TOTAL) THENL 210 [EXISTS_TAC ���l:real���, EXISTS_TAC ���k:real���] THEN 211 X_GEN_TAC ���n:num��� THEN MP_TAC(SPECL [���n:num���, ���N:num���] LESS_CASES) THEN 212 DISCH_THEN(DISJ_CASES_THEN(ANTE_RES_THEN ASSUME_TAC)) THEN 213 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LTE_TRANS THEN 214 FIRST_ASSUM(fn th => EXISTS_TAC(rand(concl th)) THEN 215 ASM_REWRITE_TAC[] THEN NO_TAC), 216 DISCH_THEN(X_CHOOSE_TAC ���k:real���) THEN 217 MAP_EVERY EXISTS_TAC [���k:real���, ���0:num���] THEN 218 GEN_TAC THEN ASM_REWRITE_TAC[]]); 219 220val SEQ_BOUNDED_2 = store_thm("SEQ_BOUNDED_2", 221 ���!f k k'. (!n. k <= f(n) /\ f(n) <= k') ==> bounded(mr1, ^geq) f���, 222 REPEAT STRIP_TAC THEN REWRITE_TAC[SEQ_BOUNDED] THEN 223 EXISTS_TAC ���(abs(k) + abs(k')) + &1��� THEN GEN_TAC THEN 224 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC ���abs(k) + abs(k')��� THEN 225 REWRITE_TAC[REAL_LT_ADDR, REAL_LT_01] THEN 226 GEN_REWR_TAC LAND_CONV [abs] THEN 227 COND_CASES_TAC THENL 228 [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC ���abs(k')��� THEN 229 REWRITE_TAC[REAL_LE_ADDL, ABS_POS] THEN 230 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC ���k':real��� THEN 231 ASM_REWRITE_TAC[ABS_LE], 232 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC ���abs(k)��� THEN 233 REWRITE_TAC[REAL_LE_ADDR, ABS_POS] THEN 234 REWRITE_TAC[abs] THEN 235 COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_LE_NEG] THEN 236 SUBGOAL_THEN ���&0 <= f(n:num)��� MP_TAC THENL 237 [MATCH_MP_TAC REAL_LE_TRANS THEN 238 EXISTS_TAC ���k:real��� THEN ASM_REWRITE_TAC[], 239 ASM_REWRITE_TAC[]]]); 240 241(*---------------------------------------------------------------------------*) 242(* Show that every Cauchy sequence is bounded *) 243(*---------------------------------------------------------------------------*) 244 245val SEQ_CBOUNDED = store_thm("SEQ_CBOUNDED", 246 ���!f. cauchy f ==> bounded(mr1, ^geq) f���, 247 GEN_TAC THEN REWRITE_TAC[bounded, cauchy] THEN 248 DISCH_THEN(MP_TAC o SPEC ���&1���) THEN REWRITE_TAC[REAL_LT_01] THEN 249 DISCH_THEN(X_CHOOSE_TAC ���N:num���) THEN 250 MAP_EVERY EXISTS_TAC [���&1���, ���(f:num->real) N���, ���N:num���] THEN 251 REWRITE_TAC[GREATER_EQ, LESS_EQ_REFL] THEN 252 POP_ASSUM(MP_TAC o SPEC ���N:num���) THEN 253 REWRITE_TAC[GREATER_EQ, LESS_EQ_REFL, MR1_DEF]); 254 255(*---------------------------------------------------------------------------*) 256(* Show that a bounded and monotonic sequence converges *) 257(*---------------------------------------------------------------------------*) 258 259val SEQ_ICONV = store_thm("SEQ_ICONV", 260 ���!f. bounded(mr1, ^geq) f /\ (!m n:num. m >= n ==> f(m) >= f(n)) 261 ==> convergent f���, 262GEN_TAC THEN DISCH_TAC THEN 263 MP_TAC (SPEC ���\x:real. ?n:num. x = f(n)��� REAL_SUP) THEN BETA_TAC THEN 264 W(C SUBGOAL_THEN MP_TAC o funpow 2 (fst o dest_imp) o snd) THENL 265 [CONJ_TAC THENL 266 [MAP_EVERY EXISTS_TAC [���f(0:num):real���, ���0:num���] THEN REFL_TAC, 267 POP_ASSUM(MP_TAC o REWRITE_RULE[SEQ_BOUNDED] o CONJUNCT1) THEN 268 DISCH_THEN(X_CHOOSE_TAC ���k:real���) THEN 269 EXISTS_TAC ���k:real��� THEN 270 GEN_TAC THEN DISCH_THEN(X_CHOOSE_THEN ���n:num��� SUBST1_TAC) THEN 271 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC ���abs(f(n:num))��� THEN 272 ASM_REWRITE_TAC[ABS_LE]], ALL_TAC] THEN 273 DISCH_THEN(fn th => REWRITE_TAC[th]) THEN DISCH_TAC THEN 274 REWRITE_TAC[convergent] THEN EXISTS_TAC ���sup(\x. ?n:num. x = f(n))��� THEN 275 REWRITE_TAC[SEQ] THEN X_GEN_TAC ���e:real��� THEN DISCH_TAC THEN 276 FIRST_ASSUM(MP_TAC o assert(is_forall o concl)) THEN 277 DISCH_THEN(MP_TAC o SPEC ���sup(\x. ?n:num. x = f(n)) - e���) THEN 278 REWRITE_TAC[REAL_LT_SUB_RADD, REAL_LT_ADDR] THEN 279 ASM_REWRITE_TAC[] THEN 280 DISCH_THEN(X_CHOOSE_THEN ���x:real��� MP_TAC) THEN 281 ONCE_REWRITE_TAC[CONJ_SYM] THEN 282 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC (X_CHOOSE_THEN ���n:num��� SUBST1_TAC)) THEN 283 ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN REWRITE_TAC[GSYM REAL_LT_SUB_RADD] THEN 284 DISCH_TAC THEN SUBGOAL_THEN ���!n. f(n) <= sup(\x. ?n:num. x = f(n))��� 285 ASSUME_TAC THENL 286 [FIRST_ASSUM(MP_TAC o SPEC ���sup(\x. ?n:num. x = f(n))���) THEN 287 REWRITE_TAC[REAL_LT_REFL] THEN 288 CONV_TAC(ONCE_DEPTH_CONV NOT_EXISTS_CONV) THEN 289 REWRITE_TAC[TAUT_CONV ���~(a /\ b) = a ==> ~b���] THEN 290 REWRITE_TAC[REAL_NOT_LT] THEN 291 CONV_TAC(ONCE_DEPTH_CONV LEFT_IMP_EXISTS_CONV) THEN 292 DISCH_THEN(MP_TAC o GEN ���n:num��� o SPECL [���(f:num->real) n���, ���n:num���]) THEN 293 REWRITE_TAC[], ALL_TAC] THEN 294 EXISTS_TAC ���n:num��� THEN X_GEN_TAC ���m:num��� THEN 295 FIRST_ASSUM(UNDISCH_TAC o assert is_conj o concl) THEN 296 DISCH_THEN(ASSUME_TAC o CONJUNCT2) THEN 297 DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN 298 RULE_ASSUM_TAC(REWRITE_RULE[REAL_LT_SUB_RADD]) THEN 299 RULE_ASSUM_TAC(ONCE_REWRITE_RULE[REAL_ADD_SYM]) THEN 300 RULE_ASSUM_TAC(REWRITE_RULE[GSYM REAL_LT_SUB_RADD]) THEN 301 REWRITE_TAC[real_ge] THEN DISCH_TAC THEN 302 SUBGOAL_THEN ���(sup(\x. ?m:num. x = f(m)) - e) < f(m)��� ASSUME_TAC THENL 303 [MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC ���(f:num->real) n��� THEN 304 ASM_REWRITE_TAC[], ALL_TAC] THEN 305 REWRITE_TAC[abs] THEN COND_CASES_TAC THEN 306 ASM_REWRITE_TAC[REAL_NEG_SUB] THENL 307 [MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC ���&0��� THEN 308 ASM_REWRITE_TAC[] THEN REWRITE_TAC[real_sub] THEN 309 (SUBST1_TAC o REWRITE_RULE[REAL_ADD_RINV] o C SPECL REAL_LE_RADD) 310 [���(f:num->real) m���, ���(sup(\x. ?n:num. x = f(n)))���, 311 ���~(sup(\x. ?n:num. x = f(n)))���] THEN 312 ASM_REWRITE_TAC[], 313 REWRITE_TAC[REAL_LT_SUB_RADD] THEN ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN 314 REWRITE_TAC[GSYM REAL_LT_SUB_RADD] THEN ASM_REWRITE_TAC[]]); 315 316val SEQ_NEG_CONV = store_thm("SEQ_NEG_CONV", 317 ���!f. convergent f = convergent (\n. ~(f n))���, 318 GEN_TAC THEN REWRITE_TAC[convergent] THEN EQ_TAC THEN 319 DISCH_THEN(X_CHOOSE_TAC ���l:real���) THEN 320 EXISTS_TAC ���~l��� THEN POP_ASSUM MP_TAC THEN 321 SUBST1_TAC(SYM(SPEC ���l:real��� REAL_NEGNEG)) THEN 322 REWRITE_TAC[GSYM SEQ_NEG] THEN REWRITE_TAC[REAL_NEGNEG]); 323 324val SEQ_NEG_BOUNDED = store_thm("SEQ_NEG_BOUNDED", 325 ���!f. bounded(mr1, ^geq)(\n. ~(f n)) = bounded(mr1, ^geq) f���, 326 GEN_TAC THEN REWRITE_TAC[SEQ_BOUNDED] THEN BETA_TAC THEN 327 REWRITE_TAC[ABS_NEG]); 328 329val SEQ_BCONV = store_thm("SEQ_BCONV", 330 ���!f. bounded(mr1, ^geq) f /\ mono f ==> convergent f���, 331 GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN 332 REWRITE_TAC[mono] THEN DISCH_THEN DISJ_CASES_TAC THENL 333 [MATCH_MP_TAC SEQ_ICONV THEN ASM_REWRITE_TAC[GREATER_EQ, real_ge], 334 ONCE_REWRITE_TAC[SEQ_NEG_CONV] THEN MATCH_MP_TAC SEQ_ICONV THEN 335 ASM_REWRITE_TAC[SEQ_NEG_BOUNDED] THEN BETA_TAC THEN 336 REWRITE_TAC[GREATER_EQ, real_ge, REAL_LE_NEG] THEN 337 ONCE_REWRITE_TAC[GSYM real_ge] THEN ASM_REWRITE_TAC[]]); 338 339(*---------------------------------------------------------------------------*) 340(* Show that every sequence contains a monotonic subsequence *) 341(*---------------------------------------------------------------------------*) 342 343val SEQ_MONOSUB = store_thm("SEQ_MONOSUB", 344 ���!s:num->real. ?f. subseq f /\ mono(\n. s(f n))���, 345 GEN_TAC THEN 346 ASM_CASES_TAC ���!n. ?p:num. p>n /\ !m. m >= p ==> s(m) <= s(p)��� THENL 347 [(X_CHOOSE_THEN ���f:num->num��� MP_TAC o EXISTENCE o 348 C ISPECL num_Axiom_old) 349 [���@p:num. p>0 /\ (!m. m >= p ==> (s m) <= (s p))���, 350 ���\x. \n:num. @p:num. p > x /\ (!m. m >= p ==> (s m) <= (s p))���] THEN 351 BETA_TAC THEN RULE_ASSUM_TAC 352 (GEN ���n:num��� o SELECT_RULE o SPEC ���n:num���) THEN 353 POP_ASSUM(fn th => DISCH_THEN(ASSUME_TAC o GSYM) THEN 354 MP_TAC(SPEC ���0:num��� th) THEN 355 MP_TAC(GEN ���n:num��� (SPEC ���(f:num->num) n��� th))) THEN 356 ASM_REWRITE_TAC[] THEN POP_ASSUM(K ALL_TAC) THEN REPEAT STRIP_TAC THEN 357 EXISTS_TAC ���f:num->num��� THEN ASM_REWRITE_TAC[SUBSEQ_SUC, GSYM GREATER_DEF] THEN 358 SUBGOAL_THEN ���!(p:num) q. p >= (f q) ==> s(p) <= s(f(q:num))��� MP_TAC THENL 359 [REPEAT GEN_TAC THEN STRUCT_CASES_TAC(SPEC ���q:num��� num_CASES) THEN 360 ASM_REWRITE_TAC[], ALL_TAC] THEN 361 DISCH_THEN(MP_TAC o GEN ���q:num��� o SPECL [���f(SUC q):num���, ���q:num���]) THEN 362 SUBGOAL_THEN ���!q. f(SUC q) >= f(q):num��� (fn th => REWRITE_TAC[th]) THENL 363 [GEN_TAC THEN REWRITE_TAC[GREATER_EQ] THEN MATCH_MP_TAC LESS_IMP_LESS_OR_EQ 364 THEN ASM_REWRITE_TAC[GSYM GREATER_DEF], ALL_TAC] THEN 365 DISCH_TAC THEN REWRITE_TAC[MONO_SUC] THEN DISJ2_TAC THEN 366 BETA_TAC THEN ASM_REWRITE_TAC[], 367 POP_ASSUM(X_CHOOSE_TAC ���N:num��� o CONV_RULE NOT_FORALL_CONV) THEN 368 POP_ASSUM(MP_TAC o CONV_RULE NOT_EXISTS_CONV) THEN 369 REWRITE_TAC[TAUT_CONV ���~(a /\ b) = a ==> ~b���] THEN 370 CONV_TAC(ONCE_DEPTH_CONV NOT_FORALL_CONV) THEN 371 REWRITE_TAC[NOT_IMP, REAL_NOT_LE] THEN DISCH_TAC THEN 372 SUBGOAL_THEN ���!p. p >= SUC N ==> (?m. m > p /\ s(p) < s(m))��� 373 MP_TAC THENL 374 [GEN_TAC THEN REWRITE_TAC[GREATER_EQ, GSYM LESS_EQ] THEN 375 REWRITE_TAC[GSYM GREATER_DEF] THEN DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN 376 REWRITE_TAC[GREATER_EQ, LESS_OR_EQ, RIGHT_AND_OVER_OR, GREATER_DEF] THEN 377 DISCH_THEN(X_CHOOSE_THEN ���m:num��� DISJ_CASES_TAC) THENL 378 [EXISTS_TAC ���m:num��� THEN ASM_REWRITE_TAC[], 379 FIRST_ASSUM(UNDISCH_TAC o assert is_conj o concl) THEN 380 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN 381 ASM_REWRITE_TAC[REAL_LT_REFL]], ALL_TAC] THEN 382 POP_ASSUM(K ALL_TAC) THEN DISCH_TAC THEN 383 (X_CHOOSE_THEN ���f:num->num��� MP_TAC o EXISTENCE o 384 C ISPECL num_Axiom_old) 385 [���@m. m > SUC N /\ s(SUC N) < s(m)���, 386 ���\x:num. \n:num. @m. m > x /\ s(x) < s(m)���] THEN 387 BETA_TAC THEN DISCH_THEN ASSUME_TAC THEN SUBGOAL_THEN 388 ���!n. f(n) >= SUC N /\ 389 f(SUC n) > f(n) /\ s(f n) < s(f(SUC n))��� MP_TAC THENL 390 [INDUCT_TAC THENL 391 [SUBGOAL_THEN ���f(0:num) >= SUC N��� MP_TAC THENL 392 [FIRST_ASSUM(MP_TAC o SPEC ���SUC N���) THEN 393 REWRITE_TAC[GREATER_EQ, LESS_EQ_REFL] THEN 394 DISCH_THEN(MP_TAC o SELECT_RULE) THEN ASM_REWRITE_TAC[] THEN 395 DISCH_THEN(ASSUME_TAC o CONJUNCT1) THEN 396 MATCH_MP_TAC LESS_IMP_LESS_OR_EQ THEN 397 ASM_REWRITE_TAC[GSYM GREATER_DEF], ALL_TAC] THEN 398 DISCH_THEN(fn th => ASSUME_TAC th THEN REWRITE_TAC[th]) THEN 399 FIRST_ASSUM(fn th => REWRITE_TAC[CONJUNCT2 th]) THEN 400 CONV_TAC SELECT_CONV THEN FIRST_ASSUM MATCH_MP_TAC THEN 401 FIRST_ASSUM ACCEPT_TAC, 402 FIRST_ASSUM(UNDISCH_TAC o 403 assert(curry op =3 o length o strip_conj) o concl) THEN 404 DISCH_THEN STRIP_ASSUME_TAC THEN CONJ_TAC THENL 405 [REWRITE_TAC[GREATER_EQ] THEN MATCH_MP_TAC LESS_EQ_TRANS THEN 406 EXISTS_TAC ���(f:num->num) n��� THEN REWRITE_TAC[GSYM GREATER_EQ] THEN 407 CONJ_TAC THEN TRY(FIRST_ASSUM ACCEPT_TAC) THEN 408 REWRITE_TAC[GREATER_EQ] THEN MATCH_MP_TAC LESS_IMP_LESS_OR_EQ THEN 409 REWRITE_TAC[GSYM GREATER_DEF] THEN FIRST_ASSUM ACCEPT_TAC, 410 FIRST_ASSUM(SUBST1_TAC o SPEC ���SUC n��� o CONJUNCT2) THEN 411 CONV_TAC SELECT_CONV THEN FIRST_ASSUM MATCH_MP_TAC THEN 412 REWRITE_TAC[GREATER_EQ] THEN MATCH_MP_TAC LESS_EQ_TRANS THEN 413 EXISTS_TAC ���(f:num->num) n��� THEN 414 REWRITE_TAC[GSYM GREATER_EQ] THEN CONJ_TAC THEN 415 TRY(FIRST_ASSUM ACCEPT_TAC) THEN 416 REWRITE_TAC[GREATER_EQ] THEN MATCH_MP_TAC LESS_IMP_LESS_OR_EQ THEN 417 REWRITE_TAC[GSYM GREATER_DEF] THEN 418 FIRST_ASSUM ACCEPT_TAC]], ALL_TAC] THEN 419 POP_ASSUM_LIST(K ALL_TAC) THEN DISCH_TAC THEN 420 EXISTS_TAC ���f:num->num��� THEN REWRITE_TAC[SUBSEQ_SUC, MONO_SUC] THEN 421 ASM_REWRITE_TAC[GSYM GREATER_DEF] THEN DISJ1_TAC THEN BETA_TAC THEN 422 GEN_TAC THEN REWRITE_TAC[real_ge] THEN 423 MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[]]); 424 425(*---------------------------------------------------------------------------*) 426(* Show that a subsequence of a bounded sequence is bounded *) 427(*---------------------------------------------------------------------------*) 428 429val SEQ_SBOUNDED = store_thm("SEQ_SBOUNDED", 430 ���!s f. bounded(mr1,^geq) s ==> bounded(mr1,^geq) (\n. s(f n))���, 431 REPEAT GEN_TAC THEN REWRITE_TAC[SEQ_BOUNDED] THEN 432 DISCH_THEN(X_CHOOSE_TAC ���k:real���) THEN EXISTS_TAC ���k:real��� THEN 433 GEN_TAC THEN BETA_TAC THEN ASM_REWRITE_TAC[]); 434 435(*---------------------------------------------------------------------------*) 436(* Show we can take subsequential terms arbitrarily far up a sequence *) 437(*---------------------------------------------------------------------------*) 438 439val SEQ_SUBLE = store_thm("SEQ_SUBLE", 440 ���!f. subseq f ==> !n. n <= f(n)���, 441 GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THENL 442 [REWRITE_TAC[GSYM NOT_LESS, NOT_LESS_0], 443 MATCH_MP_TAC LESS_EQ_TRANS THEN EXISTS_TAC ���SUC(f(n:num))��� THEN 444 ASM_REWRITE_TAC[LESS_EQ_MONO] THEN REWRITE_TAC[GSYM LESS_EQ] THEN 445 UNDISCH_TAC ���subseq f��� THEN REWRITE_TAC[SUBSEQ_SUC] THEN 446 DISCH_THEN MATCH_ACCEPT_TAC]); 447 448val SEQ_DIRECT = store_thm("SEQ_DIRECT", 449 ���!f. subseq f ==> !N1 N2. ?n. n >= N1 /\ f(n) >= N2���, 450 GEN_TAC THEN DISCH_TAC THEN REPEAT GEN_TAC THEN 451 DISJ_CASES_TAC (SPECL [���N1:num���, ���N2:num���] LESS_EQ_CASES) THENL 452 [EXISTS_TAC ���N2:num��� THEN ASM_REWRITE_TAC[GREATER_EQ] THEN 453 MATCH_MP_TAC SEQ_SUBLE THEN FIRST_ASSUM ACCEPT_TAC, 454 EXISTS_TAC ���N1:num��� THEN REWRITE_TAC[GREATER_EQ, LESS_EQ_REFL] THEN 455 REWRITE_TAC[GREATER_EQ] THEN MATCH_MP_TAC LESS_EQ_TRANS THEN 456 EXISTS_TAC ���N1:num��� THEN ASM_REWRITE_TAC[] THEN 457 MATCH_MP_TAC SEQ_SUBLE THEN FIRST_ASSUM ACCEPT_TAC]); 458 459(*---------------------------------------------------------------------------*) 460(* Now show that every Cauchy sequence converges *) 461(*---------------------------------------------------------------------------*) 462 463val SEQ_CAUCHY = store_thm("SEQ_CAUCHY", 464 ���!f. cauchy f = convergent f���, 465 GEN_TAC THEN EQ_TAC THENL 466 [DISCH_TAC THEN FIRST_ASSUM(ASSUME_TAC o MATCH_MP SEQ_CBOUNDED) THEN 467 MP_TAC(SPEC ���f:num->real��� SEQ_MONOSUB) THEN 468 DISCH_THEN(X_CHOOSE_THEN ���g:num->num��� STRIP_ASSUME_TAC) THEN 469 SUBGOAL_THEN ���bounded(mr1, ^geq)(\n. f(g(n):num))��� ASSUME_TAC THENL 470 [MATCH_MP_TAC SEQ_SBOUNDED THEN ASM_REWRITE_TAC[], ALL_TAC] THEN 471 SUBGOAL_THEN ���convergent (\n. f(g(n):num))��� MP_TAC THENL 472 [MATCH_MP_TAC SEQ_BCONV THEN ASM_REWRITE_TAC[], ALL_TAC] THEN 473 REWRITE_TAC[convergent] THEN DISCH_THEN(X_CHOOSE_TAC ���l:real���) THEN 474 EXISTS_TAC ���l:real��� THEN REWRITE_TAC[SEQ] THEN 475 X_GEN_TAC ���e:real��� THEN DISCH_TAC THEN 476 UNDISCH_TAC ���(\n. f(g(n):num)) --> l��� THEN REWRITE_TAC[SEQ] THEN 477 DISCH_THEN(MP_TAC o SPEC ���e / &2���) THEN 478 ASM_REWRITE_TAC[REAL_LT_HALF1] THEN BETA_TAC THEN 479 DISCH_THEN(X_CHOOSE_TAC ���N1:num���) THEN 480 UNDISCH_TAC ���cauchy f��� THEN REWRITE_TAC[cauchy] THEN 481 DISCH_THEN(MP_TAC o SPEC ���e / &2���) THEN 482 ASM_REWRITE_TAC[REAL_LT_HALF1] THEN 483 DISCH_THEN(X_CHOOSE_THEN ���N2:num��� ASSUME_TAC) THEN 484 FIRST_ASSUM(MP_TAC o MATCH_MP SEQ_DIRECT) THEN 485 DISCH_THEN(MP_TAC o SPECL [���N1:num���, ���N2:num���]) THEN 486 DISCH_THEN(X_CHOOSE_THEN ���n:num��� STRIP_ASSUME_TAC) THEN 487 EXISTS_TAC ���N2:num��� THEN X_GEN_TAC ���m:num��� THEN DISCH_TAC THEN 488 UNDISCH_TAC ���!n:num. n >= N1 ==> abs(f(g n:num) - l) < (e / &2)��� THEN 489 DISCH_THEN(MP_TAC o SPEC ���n:num���) THEN ASM_REWRITE_TAC[] THEN 490 DISCH_TAC THEN FIRST_ASSUM(UNDISCH_TAC o assert is_forall o concl) THEN 491 DISCH_THEN(MP_TAC o SPECL [���g(n:num):num���, ���m:num���]) THEN 492 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN 493 MATCH_MP_TAC REAL_LET_TRANS THEN 494 SUBGOAL_THEN ���f(m:num) - l = (f(m) - f(g(n:num))) + (f(g n) - l)��� 495 SUBST1_TAC THENL [REWRITE_TAC[REAL_SUB_TRIANGLE], ALL_TAC] THEN 496 EXISTS_TAC ���abs(f(m:num) - f(g(n:num))) + abs(f(g n) - l)��� THEN 497 REWRITE_TAC[ABS_TRIANGLE] THEN 498 SUBST1_TAC(SYM(SPEC ���e:real��� REAL_HALF_DOUBLE)) THEN 499 MATCH_MP_TAC REAL_LT_ADD2 THEN ASM_REWRITE_TAC[] THEN 500 ONCE_REWRITE_TAC[ABS_SUB] THEN ASM_REWRITE_TAC[], 501 502 REWRITE_TAC[convergent] THEN 503 DISCH_THEN(X_CHOOSE_THEN ���l:real��� MP_TAC) THEN 504 REWRITE_TAC[SEQ, cauchy] THEN DISCH_TAC THEN 505 X_GEN_TAC ���e:real��� THEN DISCH_TAC THEN 506 FIRST_ASSUM(UNDISCH_TAC o assert is_forall o concl) THEN 507 DISCH_THEN(MP_TAC o SPEC ���e / &2���) THEN 508 ASM_REWRITE_TAC[REAL_LT_HALF1] THEN 509 DISCH_THEN(X_CHOOSE_TAC ���N:num���) THEN 510 EXISTS_TAC ���N:num��� THEN REPEAT GEN_TAC THEN 511 DISCH_THEN(CONJUNCTS_THEN (ANTE_RES_THEN ASSUME_TAC)) THEN 512 MATCH_MP_TAC REAL_LET_TRANS THEN 513 SUBGOAL_THEN ���f(m:num) - f(n) = (f(m) - l) + (l - f(n))��� 514 SUBST1_TAC THENL [REWRITE_TAC[REAL_SUB_TRIANGLE], ALL_TAC] THEN 515 EXISTS_TAC ���abs(f(m:num) - l) + abs(l - f(n))��� THEN 516 REWRITE_TAC[ABS_TRIANGLE] THEN 517 SUBST1_TAC(SYM(SPEC ���e:real��� REAL_HALF_DOUBLE)) THEN 518 MATCH_MP_TAC REAL_LT_ADD2 THEN ASM_REWRITE_TAC[] THEN 519 ONCE_REWRITE_TAC[ABS_SUB] THEN ASM_REWRITE_TAC[]]); 520 521(*---------------------------------------------------------------------------*) 522(* The limit comparison property for sequences *) 523(*---------------------------------------------------------------------------*) 524 525val SEQ_LE = store_thm("SEQ_LE", 526 ���!f g l m. f --> l /\ g --> m /\ (?N. !n. n >= N ==> f(n) <= g(n)) 527 ==> l <= m���, 528 REPEAT GEN_TAC THEN 529 MP_TAC(ISPEC geq NET_LE) THEN 530 REWRITE_TAC[DORDER_NGE, tends_num_real, GREATER_EQ, LESS_EQ_REFL] THEN 531 DISCH_THEN MATCH_ACCEPT_TAC); 532 533(*---------------------------------------------------------------------------*) 534(* We can displace a convergent series by 1 *) 535(*---------------------------------------------------------------------------*) 536 537val SEQ_SUC = store_thm("SEQ_SUC", 538 ���!f l. f --> l = (\n. f(SUC n)) --> l���, 539 REPEAT GEN_TAC THEN REWRITE_TAC[SEQ, GREATER_EQ] THEN EQ_TAC THEN 540 DISCH_THEN(fn th => X_GEN_TAC ���e:real��� THEN 541 DISCH_THEN(MP_TAC o MATCH_MP th)) THEN BETA_TAC THEN 542 DISCH_THEN(X_CHOOSE_TAC ���N:num���) THENL 543 [EXISTS_TAC ���N:num��� THEN X_GEN_TAC ���n:num��� THEN DISCH_TAC THEN 544 FIRST_ASSUM MATCH_MP_TAC THEN MATCH_MP_TAC LESS_EQ_TRANS THEN 545 EXISTS_TAC ���SUC N��� THEN ASM_REWRITE_TAC[LESS_EQ_MONO, LESS_EQ_SUC_REFL], 546 EXISTS_TAC ���SUC N��� THEN X_GEN_TAC ���n:num��� THEN 547 STRUCT_CASES_TAC (SPEC ���n:num��� num_CASES) THENL 548 [REWRITE_TAC[GSYM NOT_LESS, LESS_0], 549 REWRITE_TAC[LESS_EQ_MONO] THEN DISCH_TAC THEN 550 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]]]); 551 552(*---------------------------------------------------------------------------*) 553(* Prove a sequence tends to zero iff its abs does *) 554(*---------------------------------------------------------------------------*) 555 556val SEQ_ABS = store_thm("SEQ_ABS", 557 ���!f. (\n. abs(f n)) --> &0 = f --> &0���, 558 GEN_TAC THEN REWRITE_TAC[SEQ] THEN 559 BETA_TAC THEN REWRITE_TAC[REAL_SUB_RZERO, ABS_ABS]); 560 561(*---------------------------------------------------------------------------*) 562(* Half this is true for a general limit *) 563(*---------------------------------------------------------------------------*) 564 565val SEQ_ABS_IMP = store_thm("SEQ_ABS_IMP", 566 ���!f l. f --> l ==> (\n. abs(f n)) --> abs(l)���, 567 REPEAT GEN_TAC THEN REWRITE_TAC[tends_num_real] THEN 568 MATCH_ACCEPT_TAC NET_ABS); 569 570(*---------------------------------------------------------------------------*) 571(* Prove that an unbounded sequence's inverse tends to 0 *) 572(*---------------------------------------------------------------------------*) 573 574val SEQ_INV0 = store_thm("SEQ_INV0", 575 ���!f. (!y. ?N. !n. n >= N ==> f(n) > y) 576 ==> 577 (\n. inv(f n)) --> &0���, 578 GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[SEQ, REAL_SUB_RZERO] THEN 579 X_GEN_TAC ���e:real��� THEN DISCH_TAC THEN 580 FIRST_ASSUM(X_CHOOSE_TAC ���N:num��� o SPEC ���inv e���) THEN 581 EXISTS_TAC ���N:num��� THEN X_GEN_TAC ���n:num��� THEN 582 DISCH_THEN(fn th => ASSUME_TAC th THEN ANTE_RES_THEN MP_TAC th) THEN 583 REWRITE_TAC[real_gt] THEN BETA_TAC THEN IMP_RES_TAC REAL_INV_POS THEN 584 SUBGOAL_THEN ���&0 < f(n:num)��� ASSUME_TAC THENL 585 [MATCH_MP_TAC REAL_LT_TRANS THEN EXISTS_TAC ���inv e��� THEN 586 ASM_REWRITE_TAC[] THEN REWRITE_TAC[GSYM real_gt] THEN 587 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[], ALL_TAC] THEN 588 SUBGOAL_THEN ���&0 < inv(f(n:num))��� ASSUME_TAC THENL 589 [MATCH_MP_TAC REAL_INV_POS THEN ASM_REWRITE_TAC[], ALL_TAC] THEN 590 SUBGOAL_THEN ���~(f(n:num) = &0)��� ASSUME_TAC THENL 591 [CONV_TAC(RAND_CONV SYM_CONV) THEN MATCH_MP_TAC REAL_LT_IMP_NE THEN 592 ASM_REWRITE_TAC[], ALL_TAC] THEN DISCH_TAC THEN 593 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP ABS_INV th]) THEN 594 SUBGOAL_THEN ���e = inv(inv e)��� SUBST1_TAC THENL 595 [CONV_TAC SYM_CONV THEN MATCH_MP_TAC REAL_INVINV THEN 596 CONV_TAC(RAND_CONV SYM_CONV) THEN 597 MATCH_MP_TAC REAL_LT_IMP_NE THEN ASM_REWRITE_TAC[], ALL_TAC] THEN 598 MATCH_MP_TAC REAL_LT_INV THEN ASM_REWRITE_TAC[] THEN 599 MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC ���(f:num->real) n��� THEN 600 ASM_REWRITE_TAC[ABS_LE]); 601 602(*---------------------------------------------------------------------------*) 603(* Important limit of c^n for |c| < 1 *) 604(*---------------------------------------------------------------------------*) 605 606val SEQ_POWER_ABS = store_thm("SEQ_POWER_ABS", 607 ���!c. abs(c) < &1 ==> (\n. abs(c) pow n) --> &0���, 608 GEN_TAC THEN DISCH_TAC THEN MP_TAC(SPEC ���c:real��� ABS_POS) THEN 609 REWRITE_TAC[REAL_LE_LT] THEN DISCH_THEN DISJ_CASES_TAC THENL 610 [SUBGOAL_THEN ���!n. abs(c) pow n = inv(inv(abs(c) pow n))��� 611 (fn th => ONCE_REWRITE_TAC[th]) THENL 612 [GEN_TAC THEN CONV_TAC SYM_CONV THEN MATCH_MP_TAC REAL_INVINV THEN 613 MATCH_MP_TAC POW_NZ THEN 614 ASM_REWRITE_TAC[ABS_NZ, ABS_ABS], ALL_TAC] THEN 615 CONV_TAC(EXACT_CONV[X_BETA_CONV ���n:num��� ���inv(abs(c) pow n)���]) THEN 616 MATCH_MP_TAC SEQ_INV0 THEN BETA_TAC THEN X_GEN_TAC ���y:real��� THEN 617 SUBGOAL_THEN ���~(abs(c) = &0)��� (fn th => REWRITE_TAC[MATCH_MP POW_INV th]) THENL 618 [CONV_TAC(RAND_CONV SYM_CONV) THEN MATCH_MP_TAC REAL_LT_IMP_NE THEN 619 ASM_REWRITE_TAC[], ALL_TAC] THEN REWRITE_TAC[real_gt] THEN 620 SUBGOAL_THEN ���&0 < inv(abs c) - &1��� ASSUME_TAC THENL 621 [REWRITE_TAC[REAL_LT_SUB_LADD] THEN REWRITE_TAC[REAL_ADD_LID] THEN 622 ONCE_REWRITE_TAC[GSYM REAL_INV1] THEN MATCH_MP_TAC REAL_LT_INV THEN 623 ASM_REWRITE_TAC[], ALL_TAC] THEN 624 MP_TAC(SPEC ���inv(abs c) - &1��� REAL_ARCH) THEN ASM_REWRITE_TAC[] THEN 625 DISCH_THEN(X_CHOOSE_TAC ���N:num��� o SPEC ���y:real���) THEN 626 EXISTS_TAC ���N:num��� THEN X_GEN_TAC ���n:num��� THEN REWRITE_TAC[GREATER_EQ] THEN 627 DISCH_TAC THEN SUBGOAL_THEN ���y < (&n * (inv(abs c) - &1))��� 628 ASSUME_TAC THENL 629 [MATCH_MP_TAC REAL_LTE_TRANS THEN 630 EXISTS_TAC ���&N * (inv(abs c) - &1)��� THEN ASM_REWRITE_TAC[] THEN 631 FIRST_ASSUM(fn th => GEN_REWR_TAC I [MATCH_MP REAL_LE_RMUL th]) THEN 632 ASM_REWRITE_TAC[REAL_LE], ALL_TAC] THEN 633 MATCH_MP_TAC REAL_LT_TRANS THEN 634 EXISTS_TAC ���&n * (inv(abs c) - &1)��� THEN ASM_REWRITE_TAC[] THEN 635 MATCH_MP_TAC REAL_LTE_TRANS THEN 636 EXISTS_TAC ���&1 + (&n * (inv(abs c) - &1))��� THEN 637 REWRITE_TAC[REAL_LT_ADDL, REAL_LT_01] THEN 638 MATCH_MP_TAC REAL_LE_TRANS THEN 639 EXISTS_TAC ���(&1 + (inv(abs c) - &1)) pow n��� THEN CONJ_TAC THENL 640 [MATCH_MP_TAC POW_PLUS1 THEN ASM_REWRITE_TAC[], 641 ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN REWRITE_TAC[REAL_SUB_ADD] THEN 642 REWRITE_TAC[REAL_LE_REFL]], 643 FIRST_ASSUM(SUBST1_TAC o SYM) THEN REWRITE_TAC[SEQ] THEN 644 GEN_TAC THEN DISCH_TAC THEN EXISTS_TAC ���1:num��� THEN 645 X_GEN_TAC ���n:num��� THEN REWRITE_TAC[GREATER_EQ] THEN BETA_TAC THEN 646 STRUCT_CASES_TAC(SPEC ���n:num��� num_CASES) THENL 647 [REWRITE_TAC[GSYM NOT_LESS, ONE, LESS_0], 648 REWRITE_TAC[POW_0, REAL_SUB_RZERO, ABS_0] THEN 649 REWRITE_TAC[ASSUME ���&0 < e���]]]); 650 651(*---------------------------------------------------------------------------*) 652(* Similar version without the abs *) 653(*---------------------------------------------------------------------------*) 654 655val SEQ_POWER = store_thm("SEQ_POWER", 656 ���!c. abs(c) < &1 ==> (\n. c pow n) --> &0���, 657 GEN_TAC THEN DISCH_TAC THEN 658 ONCE_REWRITE_TAC[GSYM SEQ_ABS] THEN BETA_TAC THEN 659 REWRITE_TAC[GSYM POW_ABS] THEN 660 POP_ASSUM(ACCEPT_TAC o MATCH_MP SEQ_POWER_ABS)); 661 662(*---------------------------------------------------------------------------*) 663(* Useful lemmas about nested intervals and proof by bisection *) 664(*---------------------------------------------------------------------------*) 665 666val NEST_LEMMA = store_thm("NEST_LEMMA", 667 ���!f g. (!n. f(SUC n) >= f(n)) /\ 668 (!n. g(SUC n) <= g(n)) /\ 669 (!n. f(n) <= g(n)) ==> 670 ?l m. l <= m /\ ((!n. f(n) <= l) /\ f --> l) /\ 671 ((!n. m <= g(n)) /\ g --> m)���, 672 REPEAT STRIP_TAC THEN MP_TAC(SPEC ���f:num->real��� MONO_SUC) THEN 673 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN 674 MP_TAC(SPEC ���g:num->real��� MONO_SUC) THEN ASM_REWRITE_TAC[] THEN 675 DISCH_TAC THEN SUBGOAL_THEN ���bounded(mr1,^geq) f��� ASSUME_TAC THENL 676 [MATCH_MP_TAC SEQ_BOUNDED_2 THEN 677 MAP_EVERY EXISTS_TAC [���(f:num->real) 0���, ���(g:num->real) 0���] THEN 678 INDUCT_TAC THEN ASM_REWRITE_TAC[REAL_LE_REFL] THEN CONJ_TAC THENL 679 [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC ���(f:num->real) n��� THEN 680 RULE_ASSUM_TAC(REWRITE_RULE[real_ge]) THEN ASM_REWRITE_TAC[], 681 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC ���g(SUC n):real��� THEN 682 ASM_REWRITE_TAC[] THEN SPEC_TAC(���SUC n���,���m:num���) THEN 683 INDUCT_TAC THEN REWRITE_TAC[REAL_LE_REFL] THEN 684 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC ���g(m:num):real��� THEN 685 ASM_REWRITE_TAC[]], ALL_TAC] THEN 686 SUBGOAL_THEN ���bounded(mr1, ^geq) g��� ASSUME_TAC THENL 687 [MATCH_MP_TAC SEQ_BOUNDED_2 THEN 688 MAP_EVERY EXISTS_TAC [���(f:num->real) 0���, ���(g:num->real) 0���] THEN 689 INDUCT_TAC THEN ASM_REWRITE_TAC[REAL_LE_REFL] THEN CONJ_TAC THENL 690 [MATCH_MP_TAC REAL_LE_TRANS THEN 691 EXISTS_TAC ���(f:num->real) (SUC n)��� THEN 692 ASM_REWRITE_TAC[] THEN SPEC_TAC(���SUC n���,���m:num���) THEN 693 INDUCT_TAC THEN REWRITE_TAC[REAL_LE_REFL] THEN 694 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC ���(f:num->real) m��� THEN 695 RULE_ASSUM_TAC(REWRITE_RULE[real_ge]) THEN ASM_REWRITE_TAC[], 696 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC ���(g:num->real) n��� THEN 697 ASM_REWRITE_TAC[]], ALL_TAC] THEN 698 MP_TAC(SPEC ���f:num->real��� SEQ_BCONV) THEN ASM_REWRITE_TAC[SEQ_LIM] THEN 699 DISCH_TAC THEN MP_TAC(SPEC ���g:num->real��� SEQ_BCONV) THEN 700 ASM_REWRITE_TAC[SEQ_LIM] THEN DISCH_TAC THEN 701 MAP_EVERY EXISTS_TAC [���lim f���, ���lim g���] THEN 702 ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL 703 [MATCH_MP_TAC SEQ_LE THEN 704 MAP_EVERY EXISTS_TAC [���f:num->real���, ���g:num->real���] THEN 705 ASM_REWRITE_TAC[], 706 X_GEN_TAC ���m:num��� THEN 707 GEN_REWR_TAC I [TAUT_CONV ���a = ~~a:bool���] THEN 708 PURE_REWRITE_TAC[REAL_NOT_LE] THEN DISCH_TAC THEN 709 UNDISCH_TAC ���f --> lim f��� THEN REWRITE_TAC[SEQ] THEN 710 DISCH_THEN(MP_TAC o SPEC ���f(m) - lim f���) THEN 711 ASM_REWRITE_TAC[REAL_SUB_LT] THEN 712 DISCH_THEN(X_CHOOSE_THEN ���p:num��� MP_TAC) THEN 713 DISCH_THEN(MP_TAC o SPEC ���p + m:num���) THEN 714 REWRITE_TAC[GREATER_EQ, LESS_EQ_ADD] THEN REWRITE_TAC[abs] THEN 715 SUBGOAL_THEN ���!p:num. lim f <= f(p + m)��� ASSUME_TAC THENL 716 [INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THENL 717 [MATCH_MP_TAC REAL_LT_IMP_LE THEN FIRST_ASSUM ACCEPT_TAC, 718 MATCH_MP_TAC REAL_LE_TRANS THEN 719 EXISTS_TAC ���f(p + m:num):real��� THEN 720 RULE_ASSUM_TAC(REWRITE_RULE[real_ge]) THEN ASM_REWRITE_TAC[]], 721 ASM_REWRITE_TAC[REAL_SUB_LE] THEN 722 REWRITE_TAC[REAL_NOT_LT, real_sub, REAL_LE_RADD] THEN 723 SPEC_TAC(���p:num���,���p:num���) THEN INDUCT_TAC THEN 724 REWRITE_TAC[REAL_LE_REFL, ADD_CLAUSES] THEN 725 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC ���f(p + m:num):real��� THEN 726 RULE_ASSUM_TAC(REWRITE_RULE[real_ge]) THEN ASM_REWRITE_TAC[]], 727 X_GEN_TAC ���m:num��� THEN 728 GEN_REWR_TAC I [TAUT_CONV ���a = ~~a:bool���] THEN 729 PURE_REWRITE_TAC[REAL_NOT_LE] THEN DISCH_TAC THEN 730 UNDISCH_TAC ���g --> lim g��� THEN REWRITE_TAC[SEQ] THEN 731 DISCH_THEN(MP_TAC o SPEC ���lim g - g(m)���) THEN 732 ASM_REWRITE_TAC[REAL_SUB_LT] THEN 733 DISCH_THEN(X_CHOOSE_THEN ���p:num��� MP_TAC) THEN 734 DISCH_THEN(MP_TAC o SPEC ���p + m:num���) THEN 735 REWRITE_TAC[GREATER_EQ, LESS_EQ_ADD] THEN REWRITE_TAC[abs] THEN 736 SUBGOAL_THEN ���!p. g(p + m:num) < lim g��� ASSUME_TAC THENL 737 [INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN 738 MATCH_MP_TAC REAL_LET_TRANS THEN 739 EXISTS_TAC ���g(p + m:num):real��� THEN ASM_REWRITE_TAC[], 740 REWRITE_TAC[REAL_SUB_LE] THEN ASM_REWRITE_TAC[GSYM REAL_NOT_LT] THEN 741 REWRITE_TAC[REAL_NOT_LT, REAL_NEG_SUB] THEN 742 REWRITE_TAC[real_sub, REAL_LE_LADD, REAL_LE_NEG] THEN 743 SPEC_TAC(���p:num���,���p:num���) THEN INDUCT_TAC THEN 744 REWRITE_TAC[REAL_LE_REFL, ADD_CLAUSES] THEN 745 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC ���g(p + m:num):real��� THEN 746 ASM_REWRITE_TAC[]]]); 747 748val NEST_LEMMA_UNIQ = store_thm("NEST_LEMMA_UNIQ", 749 ���!f g. (!n. f(SUC n) >= f(n)) /\ 750 (!n. g(SUC n) <= g(n)) /\ 751 (!n. f(n) <= g(n)) /\ 752 (\n. f(n) - g(n)) --> &0 ==> 753 ?l. ((!n. f(n) <= l) /\ f --> l) /\ 754 ((!n. l <= g(n)) /\ g --> l)���, 755 REPEAT GEN_TAC THEN 756 DISCH_THEN(fn th => STRIP_ASSUME_TAC th THEN MP_TAC th) THEN 757 REWRITE_TAC[CONJ_ASSOC] THEN DISCH_THEN(MP_TAC o CONJUNCT1) THEN 758 REWRITE_TAC[GSYM CONJ_ASSOC] THEN 759 DISCH_THEN(MP_TAC o MATCH_MP NEST_LEMMA) THEN 760 DISCH_THEN(X_CHOOSE_THEN ���l:real��� MP_TAC) THEN 761 DISCH_THEN(X_CHOOSE_THEN ���m:real��� STRIP_ASSUME_TAC) THEN 762 EXISTS_TAC ���l:real��� THEN ASM_REWRITE_TAC[] THEN 763 SUBGOAL_THEN ���l:real = m��� (fn th => ASM_REWRITE_TAC[th]) THEN 764 MP_TAC(SPECL [���f:num->real���, ���l:real���, ���g:num->real���, ���m:real���] SEQ_SUB) THEN 765 ASM_REWRITE_TAC[] THEN 766 DISCH_THEN(MP_TAC o CONJ(ASSUME ���(\n. f(n) - g(n)) --> &0���)) THEN 767 DISCH_THEN(MP_TAC o MATCH_MP SEQ_UNIQ) THEN 768 CONV_TAC(LAND_CONV SYM_CONV) THEN 769 REWRITE_TAC[REAL_SUB_0]); 770 771 772val BOLZANO_LEMMA = store_thm("BOLZANO_LEMMA", 773 ���!P. (!a b c. a <= b /\ b <= c /\ P(a,b) /\ P(b,c) ==> P(a,c)) /\ 774 (!x. ?d. &0 < d /\ !a b. a <= x /\ x <= b /\ (b - a) < d ==> P(a,b)) 775 ==> !a b. a <= b ==> P(a,b)���, 776 REPEAT STRIP_TAC THEN 777 GEN_REWR_TAC I [TAUT_CONV ���a = ~~a:bool���] THEN 778 DISCH_TAC THEN 779 (X_CHOOSE_THEN ���f:num->real#real��� STRIP_ASSUME_TAC o 780 EXISTENCE o BETA_RULE o C ISPECL num_Axiom_old) 781 [���(a:real,(b:real))���, 782 ���\fn (n:num). if P(FST fn,(FST fn + SND fn) / &2) 783 then ((FST fn + SND fn) / &2,SND fn) 784 else (FST fn,(FST fn + SND fn) / &2)���] THEN 785 MP_TAC(SPECL 786 [���\n:num. FST(f(n) :real#real)���, ���\n:num. SND(f(n) :real#real)���] 787 NEST_LEMMA_UNIQ) THEN BETA_TAC THEN 788 SUBGOAL_THEN ���!n:num. FST(f n) <= SND(f n)��� ASSUME_TAC THENL 789 [INDUCT_TAC THEN ASM_REWRITE_TAC[] THEN 790 COND_CASES_TAC THEN REWRITE_TAC[] THENL 791 [MATCH_MP_TAC REAL_MIDDLE2, MATCH_MP_TAC REAL_MIDDLE1] THEN 792 FIRST_ASSUM ACCEPT_TAC, ALL_TAC] THEN REWRITE_TAC[real_ge] THEN 793 SUBGOAL_THEN ���!n:num. FST(f n :real#real) <= FST(f(SUC n))��� 794 ASSUME_TAC THENL 795 [REWRITE_TAC[real_ge] THEN INDUCT_TAC THEN 796 FIRST_ASSUM(fn th => GEN_REWR_TAC (funpow 2 RAND_CONV) [th]) THEN 797 COND_CASES_TAC THEN REWRITE_TAC[REAL_LE_REFL] THEN 798 MATCH_MP_TAC REAL_MIDDLE1 THEN FIRST_ASSUM MATCH_ACCEPT_TAC, ALL_TAC] THEN 799 SUBGOAL_THEN ���!n. ~P(FST((f:num->real#real) n),SND(f n))��� ASSUME_TAC THENL 800 [INDUCT_TAC THEN ASM_REWRITE_TAC[] THEN 801 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN 802 UNDISCH_TAC ���~P(FST((f:num->real#real) n),SND(f n)):bool��� THEN 803 PURE_REWRITE_TAC[IMP_CLAUSES, NOT_CLAUSES] THEN 804 FIRST_ASSUM MATCH_MP_TAC THEN 805 EXISTS_TAC ���(FST(f(n:num)) + SND(f(n))) / &2��� THEN 806 ASM_REWRITE_TAC[] THEN CONJ_TAC THENL 807 [MATCH_MP_TAC REAL_MIDDLE1, MATCH_MP_TAC REAL_MIDDLE2] THEN 808 FIRST_ASSUM MATCH_ACCEPT_TAC, ALL_TAC] THEN 809 SUBGOAL_THEN ���!n:num. SND(f(SUC n) :real#real) <= SND(f n)��� ASSUME_TAC THENL 810 [BETA_TAC THEN INDUCT_TAC THEN 811 FIRST_ASSUM(fn th => GEN_REWR_TAC (LAND_CONV o RAND_CONV) [th]) THEN 812 COND_CASES_TAC THEN REWRITE_TAC[REAL_LE_REFL] THEN 813 MATCH_MP_TAC REAL_MIDDLE2 THEN FIRST_ASSUM MATCH_ACCEPT_TAC, ALL_TAC] THEN 814 SUBGOAL_THEN ���!n:num. SND(f n) - FST(f n) = (b - a) / (&2 pow n)��� 815 ASSUME_TAC THENL 816 [INDUCT_TAC THENL 817 [ASM_REWRITE_TAC[pow, real_div, REAL_INV1, REAL_MUL_RID], ALL_TAC] THEN 818 ASM_REWRITE_TAC[] THEN COND_CASES_TAC THEN REWRITE_TAC[] THEN 819 MATCH_MP_TAC REAL_EQ_LMUL_IMP THEN EXISTS_TAC ���&2��� THEN 820 REWRITE_TAC[REAL_SUB_LDISTRIB] THEN 821 (SUBGOAL_THEN ���~(&2 = &0)��� (fn th => REWRITE_TAC[th] THEN 822 REWRITE_TAC[MATCH_MP REAL_DIV_LMUL th]) THENL 823 [REWRITE_TAC[REAL_INJ] THEN CONV_TAC(RAND_CONV num_EQ_CONV) THEN 824 REWRITE_TAC[], ALL_TAC]) THEN 825 REWRITE_TAC[GSYM REAL_DOUBLE] THEN 826 GEN_REWR_TAC (LAND_CONV o RAND_CONV) [REAL_ADD_SYM] 827 THEN (SUBGOAL_THEN ���!x y z:real. (x + y) - (x + z) = y - z��� 828 (fn th => REWRITE_TAC[th]) 829 THENL 830 [REPEAT GEN_TAC THEN REWRITE_TAC[real_sub, REAL_NEG_ADD] THEN 831 GEN_REWR_TAC RAND_CONV [GSYM REAL_ADD_RID] THEN 832 SUBST1_TAC(SYM(SPEC ���x:real��� REAL_ADD_LINV)) THEN 833 CONV_TAC(AC_CONV(REAL_ADD_ASSOC,REAL_ADD_SYM)), ALL_TAC]) THEN 834 ASM_REWRITE_TAC[REAL_DOUBLE] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN 835 REWRITE_TAC[real_div, GSYM REAL_MUL_ASSOC] THEN 836 AP_TERM_TAC THEN REWRITE_TAC[pow] THEN 837 (SUBGOAL_THEN ���~(&2 = &0) /\ ~(&2 pow n = &0)��� 838 (fn th => REWRITE_TAC[MATCH_MP REAL_INV_MUL th]) THENL 839 [CONJ_TAC THENL [ALL_TAC, MATCH_MP_TAC POW_NZ] THEN 840 REWRITE_TAC[REAL_INJ] THEN 841 CONV_TAC(RAND_CONV num_EQ_CONV) THEN REWRITE_TAC[], 842 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[REAL_MUL_ASSOC] THEN 843 GEN_REWR_TAC (RATOR_CONV o RAND_CONV) 844 [GSYM REAL_MUL_LID] THEN 845 AP_THM_TAC THEN AP_TERM_TAC THEN CONV_TAC SYM_CONV THEN 846 MATCH_MP_TAC REAL_MUL_RINV THEN REWRITE_TAC[REAL_INJ] THEN 847 CONV_TAC(RAND_CONV num_EQ_CONV) THEN REWRITE_TAC[]]), 848 ALL_TAC] THEN 849 FIRST_ASSUM(UNDISCH_TAC o assert (can (find_term is_cond)) o concl) THEN 850 DISCH_THEN(K ALL_TAC) THEN ASM_REWRITE_TAC[] THEN 851 W(C SUBGOAL_THEN (fn t => REWRITE_TAC[t]) o fst o dest_imp o rand o snd) THENL 852 [ONCE_REWRITE_TAC[SEQ_NEG] THEN BETA_TAC THEN 853 ASM_REWRITE_TAC[REAL_NEG_SUB, REAL_NEG_0] THEN 854 REWRITE_TAC[real_div] THEN SUBGOAL_THEN ���~(&2 = &0)��� ASSUME_TAC THENL 855 [REWRITE_TAC[REAL_INJ] THEN CONV_TAC(RAND_CONV num_EQ_CONV) THEN 856 REWRITE_TAC[], ALL_TAC] THEN 857 (MP_TAC o C SPECL SEQ_MUL) 858 [���\n:num. b - a���, ���b - a���, ���\n. (inv (&2 pow n))���, ���&0���] THEN 859 REWRITE_TAC[SEQ_CONST, REAL_MUL_RZERO] THEN BETA_TAC THEN 860 DISCH_THEN MATCH_MP_TAC THEN 861 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP POW_INV th]) THEN 862 ONCE_REWRITE_TAC[GSYM SEQ_ABS] THEN BETA_TAC THEN 863 REWRITE_TAC[GSYM POW_ABS] THEN MATCH_MP_TAC SEQ_POWER_ABS THEN 864 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP ABS_INV th]) THEN 865 REWRITE_TAC[ABS_N] THEN SUBGOAL_THEN ���&0 < &2��� 866 (fn th => ONCE_REWRITE_TAC [GSYM (MATCH_MP REAL_LT_RMUL th)]) THENL 867 [REWRITE_TAC[REAL_LT, num_CONV ���2:num���, LESS_0], ALL_TAC] THEN 868 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP REAL_MUL_LINV th]) THEN 869 REWRITE_TAC[REAL_MUL_LID] THEN REWRITE_TAC[REAL_LT] THEN 870 REWRITE_TAC[num_CONV ���2:num���, LESS_SUC_REFL], 871 DISCH_THEN(X_CHOOSE_THEN ���l:real��� STRIP_ASSUME_TAC) THEN 872 FIRST_ASSUM(X_CHOOSE_THEN ���d:real��� MP_TAC o SPEC ���l:real���) THEN 873 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN 874 UNDISCH_TAC ���(\n:num. SND(f n :real#real)) --> l��� THEN 875 UNDISCH_TAC ���(\n:num. FST(f n :real#real)) --> l��� THEN 876 REWRITE_TAC[SEQ] THEN DISCH_THEN(MP_TAC o SPEC ���d / &2���) THEN 877 ASM_REWRITE_TAC[REAL_LT_HALF1] THEN 878 DISCH_THEN(X_CHOOSE_THEN ���N1:num��� (ASSUME_TAC o BETA_RULE)) THEN 879 DISCH_THEN(MP_TAC o SPEC ���d / &2���) THEN ASM_REWRITE_TAC[REAL_LT_HALF1] THEN 880 DISCH_THEN(X_CHOOSE_THEN ���N2:num��� (ASSUME_TAC o BETA_RULE)) THEN 881 DISCH_THEN(MP_TAC o 882 SPECL [���FST((f:num->real#real) (N1 + N2))���, 883 ���SND((f:num->real#real) (N1 + N2))���]) THEN 884 UNDISCH_TAC ���!n:num. (SND(f n)) - (FST(f n)) = (b - a) / ((& 2) pow n)��� THEN 885 DISCH_THEN(K ALL_TAC) THEN ASM_REWRITE_TAC[] THEN 886 MATCH_MP_TAC REAL_LET_TRANS THEN 887 EXISTS_TAC ���abs(FST(f(N1 + N2:num)) - l) + 888 abs(SND(f(N1 + N2)) - l)��� THEN 889 GEN_REWR_TAC (funpow 2 RAND_CONV) [GSYM REAL_HALF_DOUBLE] THEN 890 CONJ_TAC THENL 891 [GEN_REWR_TAC (RAND_CONV o LAND_CONV) [ABS_SUB] 892 THEN ASM_REWRITE_TAC[abs, REAL_SUB_LE] THEN 893 REWRITE_TAC[real_sub, GSYM REAL_ADD_ASSOC] THEN 894 REWRITE_TAC[(EQT_ELIM o AC_CONV(REAL_ADD_ASSOC,REAL_ADD_SYM)) 895 ���a + (b + (c + d)) = (d + a) + (c + b)���] THEN 896 REWRITE_TAC[REAL_ADD_LINV, REAL_ADD_LID, REAL_LE_REFL], 897 MATCH_MP_TAC REAL_LT_ADD2 THEN 898 CONJ_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN 899 REWRITE_TAC[GREATER_EQ, LESS_EQ_ADD] THEN 900 ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[LESS_EQ_ADD]]]); 901 902(*---------------------------------------------------------------------------*) 903(* Define infinite sums *) 904(*---------------------------------------------------------------------------*) 905 906val sums = new_infixr_definition("sums", 907 ���$sums f s = (\n. sum(0,n) f) --> s���,750); 908 909val summable = new_definition("summable", 910 ���summable f = ?s. f sums s���); 911 912val suminf = new_definition("suminf", 913 ���suminf f = @s. f sums s���); 914 915(*---------------------------------------------------------------------------*) 916(* If summable then it sums to the sum (!) *) 917(*---------------------------------------------------------------------------*) 918 919val SUM_SUMMABLE = store_thm("SUM_SUMMABLE", 920 ���!f l. f sums l ==> summable f���, 921 REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[summable] THEN 922 EXISTS_TAC ���l:real��� THEN POP_ASSUM ACCEPT_TAC); 923 924val SUMMABLE_SUM = store_thm("SUMMABLE_SUM", 925 ���!f. summable f ==> f sums (suminf f)���, 926 GEN_TAC THEN REWRITE_TAC[summable, suminf] THEN 927 DISCH_THEN(CHOOSE_THEN MP_TAC) THEN 928 CONV_TAC(ONCE_DEPTH_CONV ETA_CONV) THEN 929 MATCH_ACCEPT_TAC SELECT_AX); 930 931(*---------------------------------------------------------------------------*) 932(* And the sum is unique *) 933(*---------------------------------------------------------------------------*) 934 935val SUM_UNIQ = store_thm("SUM_UNIQ", 936 ���!f x. f sums x ==> (x = suminf f)���, 937 REPEAT GEN_TAC THEN DISCH_TAC THEN 938 SUBGOAL_THEN ���summable f��� MP_TAC THENL 939 [REWRITE_TAC[summable] THEN EXISTS_TAC ���x:real��� THEN ASM_REWRITE_TAC[], 940 DISCH_THEN(ASSUME_TAC o MATCH_MP SUMMABLE_SUM) THEN 941 MATCH_MP_TAC SEQ_UNIQ THEN 942 EXISTS_TAC ���\n. sum(0,n) f��� THEN ASM_REWRITE_TAC[GSYM sums]]); 943 944(*---------------------------------------------------------------------------*) 945(* Series which is zero beyond a certain point *) 946(*---------------------------------------------------------------------------*) 947 948val SER_0 = store_thm("SER_0", 949 ���!f n. (!m. n <= m ==> (f(m) = &0)) ==> 950 f sums (sum(0,n) f)���, 951 REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[sums, SEQ] THEN 952 X_GEN_TAC ���e:real��� THEN DISCH_TAC THEN EXISTS_TAC ���n:num��� THEN 953 X_GEN_TAC ���m:num��� THEN REWRITE_TAC[GREATER_EQ] THEN 954 DISCH_THEN(X_CHOOSE_THEN ���d:num��� SUBST1_TAC o MATCH_MP LESS_EQUAL_ADD) THEN 955 W(C SUBGOAL_THEN SUBST1_TAC o C (curry mk_eq) ���&0��� o rand o rator o snd) THEN 956 ASM_REWRITE_TAC[] THEN REWRITE_TAC[ABS_ZERO, REAL_SUB_0] THEN 957 BETA_TAC THEN REWRITE_TAC[GSYM SUM_TWO, REAL_ADD_RID_UNIQ] THEN 958 FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP(REWRITE_RULE[GREATER_EQ] SUM_ZERO)) THEN 959 MATCH_ACCEPT_TAC LESS_EQ_REFL); 960 961(*---------------------------------------------------------------------------*) 962(* Summable series of positive terms has limit >(=) any partial sum *) 963(*---------------------------------------------------------------------------*) 964 965val SER_POS_LE = store_thm("SER_POS_LE", 966 ���!f n. summable f /\ (!m. n <= m ==> &0 <= f(m)) 967 ==> sum(0,n) f <= suminf f���, 968 REPEAT GEN_TAC THEN STRIP_TAC THEN 969 FIRST_ASSUM(MP_TAC o MATCH_MP SUMMABLE_SUM) THEN REWRITE_TAC[sums] THEN 970 MP_TAC(SPEC ���sum(0,n) f��� SEQ_CONST) THEN 971 GEN_REWR_TAC I [TAUT_CONV ���a ==> b ==> c = a /\ b ==> c���] THEN 972 MATCH_MP_TAC(REWRITE_RULE[TAUT_CONV ���a /\ b /\ c ==> d = c ==> a /\ b ==> d���] 973 SEQ_LE) THEN BETA_TAC THEN 974 EXISTS_TAC ���n:num��� THEN X_GEN_TAC ���m:num��� THEN REWRITE_TAC[GREATER_EQ] THEN 975 DISCH_THEN(X_CHOOSE_THEN ���d:num��� SUBST1_TAC o MATCH_MP LESS_EQUAL_ADD) THEN 976 REWRITE_TAC[GSYM SUM_TWO, REAL_LE_ADDR] THEN 977 MATCH_MP_TAC SUM_POS_GEN THEN FIRST_ASSUM MATCH_ACCEPT_TAC); 978 979val SER_POS_LT = store_thm("SER_POS_LT", 980 ���!f n. summable f /\ (!m. n <= m ==> &0 < f(m)) 981 ==> sum(0,n) f < suminf f���, 982 REPEAT GEN_TAC THEN STRIP_TAC THEN 983 MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC ���sum(0,n + 1) f��� THEN 984 CONJ_TAC THENL 985 [REWRITE_TAC[GSYM SUM_TWO, REAL_LT_ADDR] THEN 986 REWRITE_TAC[ONE, sum, REAL_ADD_LID, ADD_CLAUSES] THEN 987 FIRST_ASSUM MATCH_MP_TAC THEN MATCH_ACCEPT_TAC LESS_EQ_REFL, 988 MATCH_MP_TAC SER_POS_LE THEN ASM_REWRITE_TAC[] THEN 989 GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN 990 FIRST_ASSUM MATCH_MP_TAC THEN 991 MATCH_MP_TAC LESS_EQ_TRANS THEN EXISTS_TAC ���SUC n��� THEN 992 REWRITE_TAC[LESS_EQ_SUC_REFL] THEN ASM_REWRITE_TAC[ADD1]]); 993 994(*---------------------------------------------------------------------------*) 995(* Theorems about grouping and offsetting (and *not* permuting) terms *) 996(*---------------------------------------------------------------------------*) 997 998val SER_GROUP = store_thm("SER_GROUP", 999 ���!f (k:num). summable f /\ 0 < k ==> 1000 (\n. sum(n * k,k) f) sums (suminf f)���, 1001 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN 1002 DISCH_THEN(MP_TAC o MATCH_MP SUMMABLE_SUM) THEN 1003 REWRITE_TAC[sums, SEQ] THEN BETA_TAC THEN 1004 DISCH_THEN(fn t => X_GEN_TAC ���e:real��� THEN DISCH_THEN(MP_TAC o MATCH_MP t)) THEN 1005 REWRITE_TAC[GREATER_EQ] THEN DISCH_THEN(X_CHOOSE_TAC ���N:num���) THEN 1006 REWRITE_TAC[SUM_GROUP] THEN EXISTS_TAC ���N:num��� THEN 1007 X_GEN_TAC ���n:num��� THEN DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN 1008 MATCH_MP_TAC LESS_EQ_TRANS THEN EXISTS_TAC ���n:num��� THEN 1009 ASM_REWRITE_TAC[] THEN UNDISCH_TAC ���0 < k:num��� THEN 1010 STRUCT_CASES_TAC(SPEC ���k:num��� num_CASES) THEN 1011 REWRITE_TAC[MULT_CLAUSES, LESS_EQ_ADD, LESS_EQ_0] THEN 1012 REWRITE_TAC[LESS_REFL]); 1013 1014val SER_PAIR = store_thm("SER_PAIR", 1015 ���!f. summable f ==> (\n. sum(2 * n,2) f) sums (suminf f)���, 1016 GEN_TAC THEN DISCH_THEN(MP_TAC o C CONJ (SPEC ���1:num��� LESS_0)) THEN 1017 REWRITE_TAC[SYM(num_CONV ���2:num���)] THEN ONCE_REWRITE_TAC[MULT_SYM] THEN 1018 MATCH_ACCEPT_TAC SER_GROUP); 1019 1020val SER_OFFSET = store_thm("SER_OFFSET", 1021 ���!f. summable f ==> !k. (\n. f(n + k)) sums (suminf f - sum(0,k) f)���, 1022 GEN_TAC THEN DISCH_THEN(curry op THEN GEN_TAC o MP_TAC o MATCH_MP SUMMABLE_SUM) THEN 1023 REWRITE_TAC[sums, SEQ] THEN 1024 DISCH_THEN(fn th => GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP th)) THEN 1025 BETA_TAC THEN REWRITE_TAC[GREATER_EQ] THEN DISCH_THEN(X_CHOOSE_TAC ���N:num���) THEN 1026 EXISTS_TAC ���N:num��� THEN X_GEN_TAC ���n:num��� THEN DISCH_TAC THEN 1027 REWRITE_TAC[SUM_OFFSET] THEN 1028 REWRITE_TAC[real_sub, REAL_NEG_ADD, REAL_NEGNEG] THEN 1029 ONCE_REWRITE_TAC[AC(REAL_ADD_ASSOC,REAL_ADD_SYM) 1030 ���(a + b) + (c + d) = (b + d) + (a + c)���] THEN 1031 REWRITE_TAC[REAL_ADD_LINV, REAL_ADD_LID] THEN REWRITE_TAC[GSYM real_sub] THEN 1032 FIRST_ASSUM MATCH_MP_TAC THEN MATCH_MP_TAC LESS_EQ_TRANS THEN 1033 EXISTS_TAC ���n:num��� THEN ASM_REWRITE_TAC[LESS_EQ_ADD]); 1034 1035(*---------------------------------------------------------------------------*) 1036(* Similar version for pairing up terms *) 1037(*---------------------------------------------------------------------------*) 1038 1039val SER_POS_LT_PAIR = store_thm("SER_POS_LT_PAIR", 1040 ���!f n. summable f /\ 1041 (!d. &0 < (f(n + (2 * d))) + f(n + ((2 * d) + 1))) 1042 ==> sum(0,n) f < suminf f���, 1043 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN 1044 DISCH_THEN(MP_TAC o MATCH_MP SUMMABLE_SUM) THEN 1045 REWRITE_TAC[sums, SEQ] THEN BETA_TAC THEN 1046 CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[REAL_NOT_LT] THEN DISCH_TAC THEN 1047 DISCH_THEN(MP_TAC o SPEC ���f(n:num) + f(n + 1)���) THEN 1048 FIRST_ASSUM(MP_TAC o SPEC ���0:num���) THEN 1049 REWRITE_TAC[ADD_CLAUSES, MULT_CLAUSES] THEN 1050 DISCH_TAC THEN ASM_REWRITE_TAC[] THEN 1051 DISCH_THEN(X_CHOOSE_THEN ���N:num��� MP_TAC) THEN 1052 SUBGOAL_THEN ���sum(0,n + 2) f <= sum(0,(2 * (SUC N)) + n) f��� 1053 ASSUME_TAC THENL 1054 [SPEC_TAC(���N:num���,���N:num���) THEN INDUCT_TAC THENL 1055 [REWRITE_TAC[MULT_CLAUSES, ADD_CLAUSES] THEN 1056 GEN_REWR_TAC (RAND_CONV o ONCE_DEPTH_CONV) [ADD_SYM] THEN 1057 MATCH_ACCEPT_TAC REAL_LE_REFL, 1058 ABBREV_TAC ���M = SUC N��� THEN 1059 REWRITE_TAC[MULT_CLAUSES] THEN 1060 REWRITE_TAC[TWO, ADD_CLAUSES] THEN 1061 REWRITE_TAC[GSYM(ONCE_REWRITE_RULE[ADD_SYM] ADD1)] THEN 1062 REWRITE_TAC[SYM TWO] THEN REWRITE_TAC[ADD_CLAUSES] THEN 1063 GEN_REWR_TAC (RATOR_CONV o ONCE_DEPTH_CONV) [ADD1] THEN 1064 (* changed for new term nets. 1065 old: REWRITE_TAC[GSYM ADD_ASSOC, GSYM ADD1, SYM(num_CONV ���2���)] *) 1066 REWRITE_TAC[GSYM ADD_ASSOC] THEN 1067 REWRITE_TAC [GSYM ADD1, SYM TWO] THEN 1068 MATCH_MP_TAC REAL_LE_TRANS THEN 1069 EXISTS_TAC ���sum(0,(2 * M) + n) f��� THEN 1070 ASM_REWRITE_TAC[] THEN REWRITE_TAC[sum] THEN 1071 REWRITE_TAC[GSYM REAL_ADD_ASSOC, REAL_LE_ADDR] THEN 1072 REWRITE_TAC[ADD_CLAUSES] THEN REWRITE_TAC[ADD1] THEN 1073 REWRITE_TAC[GSYM ADD_ASSOC] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN 1074 REWRITE_TAC[GSYM ADD_ASSOC] THEN 1075 ONCE_REWRITE_TAC[SPEC ���1:num��� ADD_SYM] THEN 1076 MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[]], 1077 DISCH_THEN(MP_TAC o SPEC ���(2 * SUC N) + n���) THEN 1078 W(C SUBGOAL_THEN (fn th => REWRITE_TAC[th]) 1079 o funpow 2(fst o dest_imp) o snd) 1080 THENL 1081 [REWRITE_TAC[TWO, MULT_CLAUSES] THEN 1082 ONCE_REWRITE_TAC[AC(ADD_ASSOC,ADD_SYM) 1083 ���(a + (b + c)) + d = b + (a + (c + d:num))���] THEN 1084 REWRITE_TAC[GREATER_EQ, LESS_EQ_ADD], ALL_TAC] THEN 1085 SUBGOAL_THEN ���suminf f + (f(n:num) + f(n + 1)) 1086 <= sum(0,(2 * (SUC N)) + n) f��� 1087 ASSUME_TAC THENL 1088 [MATCH_MP_TAC REAL_LE_TRANS THEN 1089 EXISTS_TAC ���sum(0,n + 2) f��� THEN ASM_REWRITE_TAC[] THEN 1090 MATCH_MP_TAC REAL_LE_TRANS THEN 1091 EXISTS_TAC ���sum(0,n) f + (f(n:num) + f(n + 1))��� THEN 1092 ASM_REWRITE_TAC[REAL_LE_RADD] THEN 1093 MATCH_MP_TAC REAL_EQ_IMP_LE THEN 1094 CONV_TAC(REDEPTH_CONV num_CONV) THEN 1095 REWRITE_TAC[ADD_CLAUSES, sum, REAL_ADD_ASSOC], ALL_TAC] THEN 1096 SUBGOAL_THEN ���suminf f <= sum(0,(2 * (SUC N)) + n) f��� 1097 ASSUME_TAC THENL 1098 [MATCH_MP_TAC REAL_LE_TRANS THEN 1099 EXISTS_TAC ���suminf f + (f(n:num) + f(n + 1))��� THEN 1100 ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_LE_ADDR] THEN 1101 MATCH_MP_TAC REAL_LT_IMP_LE THEN FIRST_ASSUM ACCEPT_TAC, ALL_TAC] THEN 1102 ASM_REWRITE_TAC[abs, REAL_SUB_LE] THEN 1103 REWRITE_TAC[REAL_LT_SUB_RADD] THEN 1104 GEN_REWR_TAC (funpow 2 RAND_CONV) [REAL_ADD_SYM] 1105 THEN ASM_REWRITE_TAC[REAL_NOT_LT]]); 1106 1107(*---------------------------------------------------------------------------*) 1108(* Prove a few composition formulas for series *) 1109(*---------------------------------------------------------------------------*) 1110 1111val SER_ADD = store_thm("SER_ADD", 1112 ���!x x0 y y0. x sums x0 /\ y sums y0 ==> (\n. x(n) + y(n)) sums (x0 + y0)���, 1113 REPEAT GEN_TAC THEN REWRITE_TAC[sums, SUM_ADD] THEN 1114 CONV_TAC((RAND_CONV o EXACT_CONV)[X_BETA_CONV ���n:num��� ���sum(0,n) x���]) THEN 1115 CONV_TAC((RAND_CONV o EXACT_CONV)[X_BETA_CONV ���n:num��� ���sum(0,n) y���]) THEN 1116 MATCH_ACCEPT_TAC SEQ_ADD); 1117 1118val SER_CMUL = store_thm("SER_CMUL", 1119 ���!x x0 c. x sums x0 ==> (\n. c * x(n)) sums (c * x0)���, 1120 REPEAT GEN_TAC THEN REWRITE_TAC[sums, SUM_CMUL] THEN DISCH_TAC THEN 1121 CONV_TAC(EXACT_CONV[X_BETA_CONV ���n:num��� ���sum(0,n) x���]) THEN 1122 CONV_TAC((RATOR_CONV o EXACT_CONV)[X_BETA_CONV ���n:num��� ���c:real���]) THEN 1123 MATCH_MP_TAC SEQ_MUL THEN ASM_REWRITE_TAC[SEQ_CONST]); 1124 1125val SER_NEG = store_thm("SER_NEG", 1126 ���!x x0. x sums x0 ==> (\n. ~(x n)) sums ~x0���, 1127 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[REAL_NEG_MINUS1] THEN 1128 MATCH_ACCEPT_TAC SER_CMUL); 1129 1130val SER_SUB = store_thm("SER_SUB", 1131 ���!x x0 y y0. x sums x0 /\ y sums y0 ==> (\n. x(n) - y(n)) sums (x0 - y0)���, 1132 REPEAT GEN_TAC THEN DISCH_THEN(fn th => MP_TAC (MATCH_MP SER_ADD 1133 (CONJ (CONJUNCT1 th) (MATCH_MP SER_NEG (CONJUNCT2 th))))) THEN 1134 BETA_TAC THEN REWRITE_TAC[real_sub]); 1135 1136val SER_CDIV = store_thm("SER_CDIV", 1137 ���!x x0 c. x sums x0 ==> (\n. x(n) / c) sums (x0 / c)���, 1138 REPEAT GEN_TAC THEN REWRITE_TAC[real_div] THEN 1139 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN 1140 MATCH_ACCEPT_TAC SER_CMUL); 1141 1142(*---------------------------------------------------------------------------*) 1143(* Prove Cauchy-type criterion for convergence of series *) 1144(*---------------------------------------------------------------------------*) 1145 1146val SER_CAUCHY = store_thm("SER_CAUCHY", 1147 ���!f. summable f = 1148 !e. &0 < e ==> ?N. !m n. m >= N ==> abs(sum(m,n) f) < e���, 1149 GEN_TAC THEN REWRITE_TAC[summable, sums] THEN 1150 REWRITE_TAC[GSYM convergent] THEN 1151 REWRITE_TAC[GSYM SEQ_CAUCHY] THEN REWRITE_TAC[cauchy] THEN 1152 AP_TERM_TAC THEN ABS_TAC THEN REWRITE_TAC[GREATER_EQ] THEN BETA_TAC THEN 1153 REWRITE_TAC[TAUT_CONV ���((a ==> b) = (a ==> c)) = a ==> (b = c)���] THEN 1154 DISCH_TAC THEN EQ_TAC THEN DISCH_THEN(X_CHOOSE_TAC ���N:num���) THEN 1155 EXISTS_TAC ���N:num��� THEN REPEAT GEN_TAC THEN DISCH_TAC THENL 1156 [ONCE_REWRITE_TAC[SUM_DIFF] THEN 1157 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN 1158 MATCH_MP_TAC LESS_EQ_TRANS THEN EXISTS_TAC ���m:num��� THEN 1159 ASM_REWRITE_TAC[LESS_EQ_ADD], 1160 DISJ_CASES_THEN MP_TAC (SPECL [���m:num���, ���n:num���] LESS_EQ_CASES) THEN 1161 DISCH_THEN(X_CHOOSE_THEN ���p:num��� SUBST1_TAC o MATCH_MP LESS_EQUAL_ADD) THENL 1162 [ONCE_REWRITE_TAC[ABS_SUB], ALL_TAC] THEN 1163 REWRITE_TAC[GSYM SUM_DIFF] THEN FIRST_ASSUM MATCH_MP_TAC THEN 1164 ASM_REWRITE_TAC[]]); 1165 1166(*---------------------------------------------------------------------------*) 1167(* Show that if a series converges, the terms tend to 0 *) 1168(*---------------------------------------------------------------------------*) 1169 1170val SER_ZERO = store_thm("SER_ZERO", 1171 ���!f. summable f ==> f --> &0���, 1172 GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[SEQ] THEN 1173 X_GEN_TAC ���e:real��� THEN DISCH_TAC THEN 1174 UNDISCH_TAC ���summable f��� THEN REWRITE_TAC[SER_CAUCHY] THEN 1175 DISCH_THEN(fn th => FIRST_ASSUM(MP_TAC o MATCH_MP th)) THEN 1176 DISCH_THEN(X_CHOOSE_THEN ���N:num��� MP_TAC) THEN 1177 DISCH_THEN(curry op THEN (EXISTS_TAC ���N:num��� THEN X_GEN_TAC ���n:num��� THEN DISCH_TAC) 1178 o MP_TAC) THEN DISCH_THEN(MP_TAC o SPECL [���n:num���, ���SUC 0���]) THEN 1179 ASM_REWRITE_TAC[sum, REAL_SUB_RZERO, REAL_ADD_LID, ADD_CLAUSES]); 1180 1181(*---------------------------------------------------------------------------*) 1182(* Now prove the comparison test *) 1183(*---------------------------------------------------------------------------*) 1184 1185val SER_COMPAR = store_thm("SER_COMPAR", 1186 ���!f g. (?N. !n. n >= N ==> abs(f(n)) <= g(n)) /\ summable g ==> 1187 summable f���, 1188 REPEAT GEN_TAC THEN REWRITE_TAC[SER_CAUCHY, GREATER_EQ] THEN 1189 DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC ���N1:num���) MP_TAC) THEN 1190 REWRITE_TAC[SER_CAUCHY, GREATER_EQ] THEN DISCH_TAC THEN 1191 X_GEN_TAC ���e:real��� THEN DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN 1192 DISCH_THEN(X_CHOOSE_TAC ���N2:num���) THEN EXISTS_TAC ���N1 + N2:num��� THEN 1193 REPEAT GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN 1194 EXISTS_TAC ���sum(m,n)(\k. abs(f k))��� THEN REWRITE_TAC[ABS_SUM] THEN 1195 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC ���sum(m,n) g��� THEN CONJ_TAC THENL 1196 [MATCH_MP_TAC SUM_LE THEN BETA_TAC THEN 1197 X_GEN_TAC ���p:num��� THEN DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN 1198 MATCH_MP_TAC LESS_EQ_TRANS THEN EXISTS_TAC ���m:num��� THEN 1199 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC LESS_EQ_TRANS THEN 1200 EXISTS_TAC ���N1 + N2:num��� THEN ASM_REWRITE_TAC[LESS_EQ_ADD], ALL_TAC] THEN 1201 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC ���abs(sum(m,n) g)��� THEN 1202 REWRITE_TAC[ABS_LE] THEN FIRST_ASSUM MATCH_MP_TAC THEN 1203 MATCH_MP_TAC LESS_EQ_TRANS THEN EXISTS_TAC ���N1 + N2:num��� THEN 1204 ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN 1205 REWRITE_TAC[LESS_EQ_ADD]); 1206 1207(*---------------------------------------------------------------------------*) 1208(* And a similar version for absolute convergence *) 1209(*---------------------------------------------------------------------------*) 1210 1211val SER_COMPARA = store_thm("SER_COMPARA", 1212 ���!f g. (?N. !n. n >= N ==> abs(f(n)) <= g(n)) /\ summable g ==> 1213 summable (\k. abs(f k))���, 1214 REPEAT GEN_TAC THEN SUBGOAL_THEN ���!n. abs(f(n)) = abs((\k:num. abs(f k)) n)��� 1215 (fn th => GEN_REWR_TAC (RATOR_CONV o ONCE_DEPTH_CONV) [th]) THENL 1216 [GEN_TAC THEN BETA_TAC THEN REWRITE_TAC[ABS_ABS], 1217 MATCH_ACCEPT_TAC SER_COMPAR]); 1218 1219(*---------------------------------------------------------------------------*) 1220(* Limit comparison property for series *) 1221(*---------------------------------------------------------------------------*) 1222 1223val SER_LE = store_thm("SER_LE", 1224 ���!f g. (!n. f(n) <= g(n)) /\ summable f /\ summable g 1225 ==> suminf f <= suminf g���, 1226 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN 1227 DISCH_THEN(CONJUNCTS_THEN (fn th => ASSUME_TAC th THEN ASSUME_TAC 1228 (REWRITE_RULE[sums] (MATCH_MP SUMMABLE_SUM th)))) THEN 1229 MATCH_MP_TAC SEQ_LE THEN REWRITE_TAC[CONJ_ASSOC] THEN 1230 MAP_EVERY EXISTS_TAC [���\n. sum(0,n) f���, ���\n. sum(0,n) g���] THEN CONJ_TAC THENL 1231 [REWRITE_TAC[GSYM sums] THEN CONJ_TAC THEN 1232 MATCH_MP_TAC SUMMABLE_SUM THEN FIRST_ASSUM ACCEPT_TAC, 1233 EXISTS_TAC ���0:num��� THEN REWRITE_TAC[GREATER_EQ, ZERO_LESS_EQ] THEN 1234 GEN_TAC THEN BETA_TAC THEN MATCH_MP_TAC SUM_LE THEN 1235 GEN_TAC THEN ASM_REWRITE_TAC[ZERO_LESS_EQ]]); 1236 1237val SER_LE2 = store_thm("SER_LE2", 1238 ���!f g. (!n. abs(f n) <= g(n)) /\ summable g ==> 1239 summable f /\ suminf f <= suminf g���, 1240 REPEAT GEN_TAC THEN STRIP_TAC THEN 1241 SUBGOAL_THEN ���summable f��� ASSUME_TAC THENL 1242 [MATCH_MP_TAC SER_COMPAR THEN EXISTS_TAC ���g:num->real��� THEN 1243 ASM_REWRITE_TAC[], ASM_REWRITE_TAC[]] THEN 1244 MATCH_MP_TAC SER_LE THEN ASM_REWRITE_TAC[] THEN 1245 X_GEN_TAC ���n:num��� THEN MATCH_MP_TAC REAL_LE_TRANS THEN 1246 EXISTS_TAC ���abs(f(n:num))��� THEN ASM_REWRITE_TAC[ABS_LE]); 1247 1248(*---------------------------------------------------------------------------*) 1249(* Show that absolute convergence implies normal convergence *) 1250(*---------------------------------------------------------------------------*) 1251 1252val SER_ACONV = store_thm("SER_ACONV", 1253 ���!f. summable (\n. abs(f n)) ==> summable f���, 1254 GEN_TAC THEN REWRITE_TAC[SER_CAUCHY] THEN REWRITE_TAC[SUM_ABS] THEN 1255 DISCH_THEN(curry op THEN (X_GEN_TAC ���e:real��� THEN DISCH_TAC) o MP_TAC) THEN 1256 DISCH_THEN(IMP_RES_THEN (X_CHOOSE_TAC ���N:num���)) THEN 1257 EXISTS_TAC ���N:num��� THEN REPEAT GEN_TAC THEN 1258 DISCH_THEN(ANTE_RES_THEN ASSUME_TAC) THEN MATCH_MP_TAC REAL_LET_TRANS THEN 1259 EXISTS_TAC ���sum(m,n)(\m. abs(f m))��� THEN ASM_REWRITE_TAC[ABS_SUM]); 1260 1261(*---------------------------------------------------------------------------*) 1262(* Absolute value of series *) 1263(*---------------------------------------------------------------------------*) 1264 1265val SER_ABS = store_thm("SER_ABS", 1266 ���!f. summable(\n. abs(f n)) ==> abs(suminf f) <= suminf(\n. abs(f n))���, 1267 GEN_TAC THEN DISCH_TAC THEN 1268 FIRST_ASSUM(MP_TAC o MATCH_MP SUMMABLE_SUM o MATCH_MP SER_ACONV) THEN 1269 POP_ASSUM(MP_TAC o MATCH_MP SUMMABLE_SUM) THEN 1270 REWRITE_TAC[sums] THEN DISCH_TAC THEN 1271 DISCH_THEN(ASSUME_TAC o BETA_RULE o MATCH_MP SEQ_ABS_IMP) THEN 1272 MATCH_MP_TAC SEQ_LE THEN MAP_EVERY EXISTS_TAC 1273 [���\n. abs(sum(0,n)f)���, ���\n. sum(0,n)(\n. abs(f n))���] THEN 1274 ASM_REWRITE_TAC[] THEN EXISTS_TAC ���0:num��� THEN X_GEN_TAC ���n:num��� THEN 1275 DISCH_THEN(K ALL_TAC) THEN BETA_TAC THEN MATCH_ACCEPT_TAC SUM_ABS_LE); 1276 1277(*---------------------------------------------------------------------------*) 1278(* Prove sum of geometric progression (useful for comparison) *) 1279(*---------------------------------------------------------------------------*) 1280 1281val GP_FINITE = store_thm("GP_FINITE", 1282 ���!x. ~(x = &1) ==> 1283 !n. (sum(0,n) (\n. x pow n) = ((x pow n) - &1) / (x - &1))���, 1284 GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THENL 1285 [REWRITE_TAC[sum, pow, REAL_SUB_REFL, REAL_DIV_LZERO], 1286 REWRITE_TAC[sum, pow] THEN BETA_TAC THEN 1287 ASM_REWRITE_TAC[ADD_CLAUSES] THEN 1288 SUBGOAL_THEN ���~(x - &1 = &0)��� ASSUME_TAC THEN 1289 ASM_REWRITE_TAC[REAL_SUB_0] THEN 1290 MP_TAC(GENL [���p:real���, ���q:real���] 1291 (SPECL [���p:real���, ���q:real���, ���x - &1���] REAL_EQ_RMUL)) THEN 1292 ASM_REWRITE_TAC[] THEN DISCH_THEN(fn th => ONCE_REWRITE_TAC[GSYM th]) THEN 1293 REWRITE_TAC[REAL_RDISTRIB] THEN SUBGOAL_THEN 1294 ���!p. (p / (x - &1)) * (x - &1) = p��� (fn th => REWRITE_TAC[th]) THENL 1295 [GEN_TAC THEN MATCH_MP_TAC REAL_DIV_RMUL THEN ASM_REWRITE_TAC[], ALL_TAC] 1296 THEN REWRITE_TAC[REAL_SUB_LDISTRIB] THEN REWRITE_TAC[real_sub] THEN 1297 ONCE_REWRITE_TAC[AC(REAL_ADD_ASSOC,REAL_ADD_SYM) 1298 ���(a + b) + (c + d) = (c + b) + (d + a)���] THEN 1299 REWRITE_TAC[REAL_MUL_RID, REAL_ADD_LINV, REAL_ADD_RID] THEN 1300 AP_THM_TAC THEN AP_TERM_TAC THEN MATCH_ACCEPT_TAC REAL_MUL_SYM]); 1301 1302val GP = store_thm("GP", 1303 ���!x. abs(x) < &1 ==> (\n. x pow n) sums inv(&1 - x)���, 1304 GEN_TAC THEN ASM_CASES_TAC ���x = &1��� THEN 1305 ASM_REWRITE_TAC[ABS_1, REAL_LT_REFL] THEN DISCH_TAC THEN 1306 REWRITE_TAC[sums] THEN 1307 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP GP_FINITE th]) THEN 1308 REWRITE_TAC[REAL_INV_1OVER] THEN REWRITE_TAC[real_div] THEN 1309 GEN_REWR_TAC (LAND_CONV o ABS_CONV) [GSYM REAL_NEG_MUL2] THEN 1310 SUBGOAL_THEN ���~(x - &1 = &0)��� (fn t =>REWRITE_TAC[MATCH_MP REAL_NEG_INV t]) THENL 1311 [ASM_REWRITE_TAC[REAL_SUB_0], ALL_TAC] THEN 1312 REWRITE_TAC[REAL_NEG_SUB, GSYM real_div] THEN 1313 CONV_TAC(EXACT_CONV[X_BETA_CONV ���n:num��� ���&1 - (x pow n)���]) THEN 1314 CONV_TAC(EXACT_CONV[X_BETA_CONV ���n:num��� ���&1 - x���]) THEN 1315 MATCH_MP_TAC SEQ_DIV THEN BETA_TAC THEN REWRITE_TAC[SEQ_CONST] THEN 1316 REWRITE_TAC[REAL_SUB_0] THEN CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN 1317 ASM_REWRITE_TAC[] THEN 1318 GEN_REWR_TAC RAND_CONV [GSYM REAL_SUB_RZERO] 1319 THEN CONV_TAC(EXACT_CONV[X_BETA_CONV ���n:num��� ���x pow n���]) THEN 1320 CONV_TAC(EXACT_CONV[X_BETA_CONV ���n:num��� ���&1���]) THEN 1321 MATCH_MP_TAC SEQ_SUB THEN BETA_TAC THEN REWRITE_TAC[SEQ_CONST] THEN 1322 MATCH_MP_TAC SEQ_POWER THEN FIRST_ASSUM ACCEPT_TAC); 1323 1324(*---------------------------------------------------------------------------*) 1325(* Now prove the ratio test *) 1326(*---------------------------------------------------------------------------*) 1327 1328val ABS_NEG_LEMMA = store_thm("ABS_NEG_LEMMA", 1329 ���!c. c <= &0 ==> !x y. abs(x) <= c * abs(y) ==> (x = &0)���, 1330 GEN_TAC THEN REWRITE_TAC[GSYM REAL_NEG_GE0] THEN DISCH_TAC THEN 1331 REPEAT GEN_TAC THEN MP_TAC(SPECL [���~c���, ���abs(y)���] REAL_LE_MUL) THEN 1332 ASM_REWRITE_TAC[ABS_POS, GSYM REAL_NEG_LMUL, REAL_NEG_GE0] THEN 1333 DISCH_THEN(fn th => DISCH_THEN(MP_TAC o C CONJ th)) THEN 1334 DISCH_THEN(MP_TAC o MATCH_MP REAL_LE_TRANS) THEN CONV_TAC CONTRAPOS_CONV THEN 1335 REWRITE_TAC[ABS_NZ, REAL_NOT_LE]); 1336 1337val SER_RATIO = store_thm("SER_RATIO", 1338 ���!f c (N:num). 1339 c < &1 /\ (!n. n >= N ==> abs(f(SUC n)) <= c * abs(f(n))) 1340 ==> 1341 summable f���, 1342 REPEAT GEN_TAC THEN DISCH_THEN STRIP_ASSUME_TAC THEN 1343 DISJ_CASES_TAC (SPECL [���c:real���, ���&0���] REAL_LET_TOTAL) THENL 1344 [REWRITE_TAC[SER_CAUCHY] THEN X_GEN_TAC ���e:real��� THEN DISCH_TAC THEN 1345 SUBGOAL_THEN ���!n. n >= N ==> (f(SUC n) = &0)��� ASSUME_TAC THENL 1346 [GEN_TAC THEN DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN 1347 MATCH_MP_TAC ABS_NEG_LEMMA THEN FIRST_ASSUM ACCEPT_TAC, ALL_TAC] THEN 1348 SUBGOAL_THEN ���!n. n >= SUC N ==> (f(n) = &0)��� ASSUME_TAC THENL 1349 [GEN_TAC THEN STRUCT_CASES_TAC(SPEC ���n:num��� num_CASES) THENL 1350 [REWRITE_TAC[GREATER_EQ] THEN DISCH_THEN(MP_TAC o MATCH_MP OR_LESS) THEN 1351 REWRITE_TAC[NOT_LESS_0], 1352 REWRITE_TAC[GREATER_EQ, LESS_EQ_MONO] THEN 1353 ASM_REWRITE_TAC[GSYM GREATER_EQ]], ALL_TAC] THEN 1354 EXISTS_TAC ���SUC N��� THEN FIRST_ASSUM(ASSUME_TAC o MATCH_MP SUM_ZERO) THEN 1355 REPEAT GEN_TAC THEN DISCH_THEN(ANTE_RES_THEN (fn th => REWRITE_TAC[th])) THEN 1356 ASM_REWRITE_TAC[ABS_0], 1357 1358 MATCH_MP_TAC SER_COMPAR THEN 1359 EXISTS_TAC ���\n:num. (abs(f N) / c pow N) * (c pow n)��� THEN 1360 CONJ_TAC THENL 1361 [EXISTS_TAC ���N:num��� THEN X_GEN_TAC ���n:num��� THEN 1362 REWRITE_TAC[GREATER_EQ] THEN 1363 DISCH_THEN(X_CHOOSE_THEN ���d:num��� SUBST1_TAC o MATCH_MP LESS_EQUAL_ADD) 1364 THEN BETA_TAC THEN REWRITE_TAC[POW_ADD] THEN REWRITE_TAC[real_div] THEN 1365 ONCE_REWRITE_TAC[AC(REAL_MUL_ASSOC,REAL_MUL_SYM) 1366 ���(a * b) * (c * d) = (a * d) * (b * c)���] THEN 1367 SUBGOAL_THEN ���~(c pow N = &0)��� 1368 (fn th => REWRITE_TAC[MATCH_MP REAL_MUL_LINV th, REAL_MUL_RID]) THENL 1369 [MATCH_MP_TAC POW_NZ THEN CONV_TAC(RAND_CONV SYM_CONV) THEN 1370 MATCH_MP_TAC REAL_LT_IMP_NE THEN ASM_REWRITE_TAC[], ALL_TAC] THEN 1371 SPEC_TAC(���d:num���,���d:num���) THEN INDUCT_TAC THEN 1372 REWRITE_TAC[pow, ADD_CLAUSES, REAL_MUL_RID, REAL_LE_REFL] THEN 1373 MATCH_MP_TAC REAL_LE_TRANS THEN 1374 EXISTS_TAC ���c * abs(f((N:num) + d))��� THEN CONJ_TAC THENL 1375 [FIRST_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[GREATER_EQ, LESS_EQ_ADD], 1376 ONCE_REWRITE_TAC[AC(REAL_MUL_ASSOC,REAL_MUL_SYM) 1377 ���a * (b * c) = b * (a * c)���] THEN 1378 FIRST_ASSUM(fn th => ASM_REWRITE_TAC[MATCH_MP REAL_LE_LMUL th])], 1379 1380 REWRITE_TAC[summable] THEN 1381 EXISTS_TAC ���(abs(f(N:num)) / (c pow N)) * inv(&1 - c)��� THEN 1382 MATCH_MP_TAC SER_CMUL THEN 1383 MATCH_MP_TAC(CONV_RULE(ONCE_DEPTH_CONV ETA_CONV) GP) THEN 1384 ASSUME_TAC(MATCH_MP REAL_LT_IMP_LE (ASSUME ���&0 < c���)) THEN 1385 ASM_REWRITE_TAC[abs]]]); 1386 1387(*---------------------------------------------------------------------------*) 1388(* Useful lemmas for proving inequalities of limits *) 1389(*---------------------------------------------------------------------------*) 1390 1391val LE_SEQ_IMP_LE_LIM = store_thm 1392 ("LE_SEQ_IMP_LE_LIM", 1393 ``!x y f. (!n. x <= f n) /\ f --> y ==> x <= y``, 1394 RW_TAC boolSimps.bool_ss [SEQ] 1395 THEN MATCH_MP_TAC REAL_LE_EPSILON 1396 THEN RW_TAC boolSimps.bool_ss [] 1397 THEN Q.PAT_X_ASSUM `!e. P e` (MP_TAC o Q.SPEC `e`) 1398 THEN RW_TAC boolSimps.bool_ss [] 1399 THEN POP_ASSUM (MP_TAC o Q.SPEC `N`) 1400 THEN Q.PAT_X_ASSUM `!n. P n` (MP_TAC o Q.SPEC `N`) 1401 THEN RW_TAC boolSimps.bool_ss 1402 [GREATER_EQ, LESS_EQ_REFL, abs, REAL_LE_SUB_LADD, REAL_ADD_LID] 1403 THEN simpLib.FULL_SIMP_TAC boolSimps.bool_ss 1404 [REAL_NOT_LE, REAL_NEG_SUB, REAL_LT_SUB_RADD] 1405 THEN PROVE_TAC [REAL_LET_TRANS, REAL_LT_ADDR, REAL_LTE_TRANS, REAL_LE_TRANS, 1406 REAL_LT_LE, REAL_ADD_SYM]); 1407 1408val SEQ_LE_IMP_LIM_LE = store_thm 1409 ("SEQ_LE_IMP_LIM_LE", 1410 ``!x y f. (!n. f n <= x) /\ f --> y ==> y <= x``, 1411 RW_TAC boolSimps.bool_ss [SEQ] 1412 THEN MATCH_MP_TAC REAL_LE_EPSILON 1413 THEN RW_TAC boolSimps.bool_ss [] 1414 THEN Q.PAT_X_ASSUM `!e. P e` (MP_TAC o Q.SPEC `e`) 1415 THEN RW_TAC boolSimps.bool_ss [] 1416 THEN POP_ASSUM (MP_TAC o Q.SPEC `N`) 1417 THEN Q.PAT_X_ASSUM `!n. P n` (MP_TAC o Q.SPEC `N`) 1418 THEN (RW_TAC boolSimps.bool_ss 1419 [GREATER_EQ, LESS_EQ_REFL, abs, REAL_LE_SUB_LADD, REAL_ADD_LID] 1420 THEN simpLib.FULL_SIMP_TAC boolSimps.bool_ss 1421 [REAL_NOT_LE, REAL_NEG_SUB, REAL_LT_SUB_RADD]) 1422 THENL [MATCH_MP_TAC REAL_LE_TRANS 1423 THEN Q.EXISTS_TAC `x` 1424 THEN (CONJ_TAC THEN1 PROVE_TAC [REAL_LE_TRANS]) 1425 THEN PROVE_TAC [REAL_LE_ADDR, REAL_LT_LE], 1426 MATCH_MP_TAC REAL_LE_TRANS 1427 THEN Q.EXISTS_TAC `f N + e` 1428 THEN (CONJ_TAC THEN1 PROVE_TAC [REAL_LT_LE, REAL_ADD_SYM]) 1429 THEN PROVE_TAC [REAL_LE_ADD2, REAL_LE_REFL]]); 1430 1431val SEQ_MONO_LE = store_thm 1432 ("SEQ_MONO_LE", 1433 ``!f x n. (!n. f n <= f (n + 1)) /\ f --> x ==> f n <= x``, 1434 RW_TAC boolSimps.bool_ss [SEQ] 1435 THEN MATCH_MP_TAC REAL_LE_EPSILON 1436 THEN RW_TAC boolSimps.bool_ss [] 1437 THEN Q.PAT_X_ASSUM `!e. P e` (MP_TAC o Q.SPEC `e`) 1438 THEN RW_TAC boolSimps.bool_ss [GREATER_EQ] 1439 THEN MP_TAC (Q.SPECL [`N`, `n`] LESS_EQ_CASES) 1440 THEN (STRIP_TAC 1441 THEN1 (Q.PAT_X_ASSUM `!n. P n` (MP_TAC o Q.SPEC `n`) 1442 THEN RW_TAC boolSimps.bool_ss 1443 [abs, REAL_LE_SUB_LADD, REAL_LT_SUB_RADD, REAL_ADD_LID, 1444 REAL_NEG_SUB] 1445 THENL [PROVE_TAC [REAL_LT_LE, REAL_ADD_SYM], 1446 simpLib.FULL_SIMP_TAC boolSimps.bool_ss [REAL_NOT_LE] 1447 THEN MATCH_MP_TAC REAL_LE_TRANS 1448 THEN Q.EXISTS_TAC `x` 1449 THEN PROVE_TAC [REAL_LT_LE, REAL_LE_ADDR]])) 1450 THEN (SUFF_TAC ``!i : num. f (N - i) <= x + (e : real)`` 1451 THEN1 PROVE_TAC [LESS_EQUAL_DIFF]) 1452 THEN numLib.INDUCT_TAC 1453 THENL [Q.PAT_X_ASSUM `!n. P n` (MP_TAC o Q.SPEC `N`) 1454 THEN RW_TAC boolSimps.bool_ss [abs, LESS_EQ_REFL, SUB_0] 1455 THEN simpLib.FULL_SIMP_TAC boolSimps.bool_ss 1456 [REAL_LT_SUB_RADD, REAL_NEG_SUB, REAL_NOT_LE, REAL_ADD_LID, 1457 REAL_LE_SUB_LADD] 1458 THEN PROVE_TAC 1459 [REAL_LT_LE, REAL_ADD_SYM, REAL_LE_TRANS, REAL_LE_ADDR], 1460 MP_TAC (numLib.ARITH_PROVE 1461 ``(N - i = N - SUC i) \/ (N - i = (N - SUC i) + 1)``) 1462 THEN PROVE_TAC [REAL_LE_REFL, REAL_LE_TRANS]]); 1463 1464val SEQ_LE_MONO = store_thm 1465 ("SEQ_LE_MONO", 1466 ``!f x n. (!n. f (n + 1) <= f n) /\ f --> x ==> x <= f n``, 1467 REPEAT GEN_TAC 1468 THEN MP_TAC (Q.SPECL [`\n. ~f n`, `~x`, `n`] SEQ_MONO_LE) 1469 THEN RW_TAC boolSimps.bool_ss [GSYM SEQ_NEG, REAL_LE_NEG]); 1470 1471(* ****************************************************** *) 1472(* Useful Theorems on Real Sequences from util_probTheory *) 1473(* ****************************************************** *) 1474 1475val mono_increasing_def = Define 1476 `mono_increasing (f:num->real) = !m n. m <= n ==> f m <= f n`; 1477 1478val mono_increasing_suc = store_thm 1479 ("mono_increasing_suc", ``!(f:num->real). mono_increasing f <=> !n. f n <= f (SUC n)``, 1480 RW_TAC std_ss [mono_increasing_def] 1481 >> EQ_TAC 1482 >- RW_TAC real_ss [] 1483 >> RW_TAC std_ss [] 1484 >> Know `?d. n = m + d` >- PROVE_TAC [LESS_EQ_EXISTS] 1485 >> RW_TAC std_ss [] 1486 >> Induct_on `d` >- RW_TAC real_ss [] 1487 >> RW_TAC std_ss [] 1488 >> Q.PAT_X_ASSUM `!n. f n <= f (SUC n)` (MP_TAC o Q.SPEC `m + d`) 1489 >> METIS_TAC [REAL_LE_TRANS, ADD_CLAUSES, LESS_EQ_ADD]); 1490 1491val mono_decreasing_def = Define 1492 `mono_decreasing (f:num->real) = !m n. m <= n ==> f n <= f m`; 1493 1494val mono_decreasing_suc = store_thm 1495 ("mono_decreasing_suc", ``!(f:num->real). mono_decreasing f <=> !n. f (SUC n) <= f n``, 1496 RW_TAC std_ss [mono_decreasing_def] 1497 >> EQ_TAC 1498 >- RW_TAC real_ss [] 1499 >> RW_TAC std_ss [] 1500 >> Know `?d. n = m + d` >- PROVE_TAC [LESS_EQ_EXISTS] 1501 >> RW_TAC std_ss [] 1502 >> Induct_on `d` >- RW_TAC real_ss [] 1503 >> RW_TAC std_ss [] 1504 >> Q.PAT_X_ASSUM `!n. f (SUC n) <= f n` (MP_TAC o Q.SPEC `m + d`) 1505 >> METIS_TAC [REAL_LE_TRANS, ADD_CLAUSES, LESS_EQ_ADD]); 1506 1507val mono_increasing_converges_to_sup = store_thm 1508 ("mono_increasing_converges_to_sup", 1509 ``!f r. mono_increasing f /\ f --> r ==> 1510 (r = sup (IMAGE f UNIV))``, 1511 RW_TAC std_ss [mono_increasing_def] 1512 >> Suff `f --> sup (IMAGE f UNIV)` 1513 >- METIS_TAC [SEQ_UNIQ] 1514 >> RW_TAC std_ss [SEQ] 1515 >> (MP_TAC o Q.ISPECL [`IMAGE (f:num->real) UNIV`,`e:real/2`]) SUP_EPSILON 1516 >> SIMP_TAC std_ss [REAL_LT_HALF1] 1517 >> `!y x z. IMAGE f UNIV x = x IN IMAGE f UNIV` by RW_TAC std_ss [IN_DEF] 1518 >> POP_ORW 1519 >> Know `(?z. !x. x IN IMAGE f UNIV ==> x <= z)` 1520 >- (Q.EXISTS_TAC `r` >> RW_TAC std_ss [IN_IMAGE, IN_UNIV] 1521 >> MATCH_MP_TAC SEQ_MONO_LE 1522 >> RW_TAC std_ss [DECIDE ``!n:num. n <= n + 1``]) 1523 >> SIMP_TAC std_ss [] >> STRIP_TAC >> POP_ASSUM (K ALL_TAC) 1524 >> RW_TAC std_ss [IN_IMAGE, IN_UNIV, GSYM ABS_BETWEEN, GREATER_EQ] 1525 >> Q.EXISTS_TAC `x'` 1526 >> RW_TAC std_ss [REAL_LT_SUB_RADD] 1527 >- (MATCH_MP_TAC REAL_LET_TRANS >> Q.EXISTS_TAC `f x' + e / 2` 1528 >> RW_TAC std_ss [] >> MATCH_MP_TAC REAL_LET_TRANS 1529 >> Q.EXISTS_TAC `f n + e / 2` >> RW_TAC std_ss [REAL_LE_ADD2, REAL_LE_REFL] 1530 >> MATCH_MP_TAC REAL_LT_IADD >> RW_TAC std_ss [REAL_LT_HALF2]) 1531 >> MATCH_MP_TAC REAL_LET_TRANS >> Q.EXISTS_TAC `sup (IMAGE f UNIV)` 1532 >> RW_TAC std_ss [REAL_LT_ADDR] 1533 >> Suff `!y. (\y. y IN IMAGE f UNIV) y ==> y <= sup (IMAGE f UNIV)` 1534 >- METIS_TAC [IN_IMAGE, IN_UNIV] 1535 >> SIMP_TAC std_ss [IN_DEF] 1536 >> MATCH_MP_TAC REAL_SUP_UBOUND_LE 1537 >> `!y x z. IMAGE f UNIV x = x IN IMAGE f UNIV` by RW_TAC std_ss [IN_DEF] 1538 >> POP_ORW 1539 >> RW_TAC std_ss [IN_IMAGE, IN_UNIV] 1540 >> Q.EXISTS_TAC `r` 1541 >> RW_TAC std_ss [] 1542 >> MATCH_MP_TAC SEQ_MONO_LE 1543 >> RW_TAC std_ss [DECIDE ``!n:num. n <= n + 1``]); 1544 1545val INCREASING_SEQ = store_thm 1546 ("INCREASING_SEQ", 1547 ``!f l. 1548 (!n. f n <= f (SUC n)) /\ 1549 (!n. f n <= l) /\ 1550 (!e. 0 < e ==> ?n. l < f n + e) ==> 1551 f --> l``, 1552 RW_TAC std_ss [SEQ, GREATER_EQ] 1553 >> Q.PAT_X_ASSUM `!e. P e` (MP_TAC o Q.SPEC `e`) 1554 >> RW_TAC std_ss [] 1555 >> Q.EXISTS_TAC `n` 1556 >> ONCE_REWRITE_TAC [ABS_SUB] 1557 >> REVERSE (RW_TAC std_ss [abs]) 1558 >- (Q.PAT_X_ASSUM `~x` MP_TAC 1559 >> Q.PAT_X_ASSUM `!n. P n` (MP_TAC o Q.SPEC `n'`) 1560 >> REAL_ARITH_TAC) 1561 >> Know `?d. n' = n + d` >- PROVE_TAC [LESS_EQ_EXISTS] 1562 >> RW_TAC std_ss [] 1563 >> Suff `l < f (n + d) + e` >- REAL_ARITH_TAC 1564 >> NTAC 2 (POP_ASSUM K_TAC) 1565 >> Induct_on `d` >- RW_TAC arith_ss [] 1566 >> RW_TAC std_ss [ADD_CLAUSES] 1567 >> Q.PAT_X_ASSUM `!n. f n <= f (SUC n)` (MP_TAC o Q.SPEC `n + d`) 1568 >> POP_ASSUM MP_TAC 1569 >> REAL_ARITH_TAC); 1570 1571(* TODO: move the following 4 lemmas to arithmeticTheory *) 1572val MAX_LE_X = store_thm 1573 ("MAX_LE_X", 1574 ``!m n k. MAX m n <= k = m <= k /\ n <= k``, 1575 RW_TAC arith_ss [MAX_DEF]); 1576 1577val X_LE_MAX = store_thm 1578 ("X_LE_MAX", 1579 ``!m n k. k <= MAX m n = k <= m \/ k <= n``, 1580 RW_TAC arith_ss [MAX_DEF]); 1581 1582val TRANSFORM_2D_NUM = store_thm 1583 ("TRANSFORM_2D_NUM", 1584 ``!P. (!m n : num. P m n ==> P n m) /\ (!m n. P m (m + n)) ==> (!m n. P m n)``, 1585 Strip 1586 >> Know `m <= n \/ n <= m` >- DECIDE_TAC 1587 >> RW_TAC std_ss [LESS_EQ_EXISTS] 1588 >> PROVE_TAC []); 1589 1590val TRIANGLE_2D_NUM = store_thm 1591 ("TRIANGLE_2D_NUM", 1592 ``!P. (!d n. P n (d + n)) ==> (!m n : num. m <= n ==> P m n)``, 1593 RW_TAC std_ss [LESS_EQ_EXISTS] 1594 >> PROVE_TAC [ADD_COMM]); 1595 1596val SEQ_SANDWICH = store_thm 1597 ("SEQ_SANDWICH", 1598 ``!f g h l. 1599 f --> l /\ h --> l /\ (!n. f n <= g n /\ g n <= h n) ==> g --> l``, 1600 RW_TAC std_ss [SEQ, GREATER_EQ] 1601 >> Q.PAT_X_ASSUM `!e. P e ==> Q e` (MP_TAC o Q.SPEC `e`) 1602 >> Q.PAT_X_ASSUM `!e. P e ==> Q e` (MP_TAC o Q.SPEC `e`) 1603 >> RW_TAC std_ss [] 1604 >> Q.EXISTS_TAC `MAX N N'` 1605 >> RW_TAC std_ss [MAX_LE_X] 1606 >> Q.PAT_X_ASSUM `!e. P e ==> Q e` (MP_TAC o Q.SPEC `n`) 1607 >> Q.PAT_X_ASSUM `!e. P e ==> Q e` (MP_TAC o Q.SPEC `n`) 1608 >> RW_TAC std_ss [] 1609 >> REPEAT (POP_ASSUM MP_TAC) 1610 >> DISCH_THEN (MP_TAC o Q.SPEC `n`) 1611 >> RW_TAC std_ss [abs] 1612 >> REPEAT (POP_ASSUM MP_TAC) 1613 >> REAL_ARITH_TAC); 1614 1615val SER_POS = store_thm 1616 ("SER_POS", 1617 ``!f. summable f /\ (!n. 0 <= f n) ==> 0 <= suminf f``, 1618 RW_TAC std_ss [] 1619 >> MP_TAC (Q.SPECL [`f`, `0`] SER_POS_LE) 1620 >> RW_TAC std_ss [sum]); 1621 1622val SER_POS_MONO = store_thm 1623 ("SER_POS_MONO", 1624 ``!f. (!n. 0 <= f n) ==> mono (\n. sum (0, n) f)``, 1625 RW_TAC std_ss [mono] 1626 >> DISJ1_TAC 1627 >> HO_MATCH_MP_TAC TRIANGLE_2D_NUM 1628 >> Induct >- RW_TAC arith_ss [REAL_LE_REFL] 1629 >> RW_TAC std_ss [ADD_CLAUSES] 1630 >> MATCH_MP_TAC REAL_LE_TRANS 1631 >> Q.EXISTS_TAC `sum (0, d + n) f` 1632 >> RW_TAC real_ss [sum] 1633 >> Q.PAT_X_ASSUM `!n. 0 <= f n` (MP_TAC o Q.SPEC `d + n`) 1634 >> REAL_ARITH_TAC); 1635 1636val POS_SUMMABLE = store_thm 1637 ("POS_SUMMABLE", 1638 ``!f. (!n. 0 <= f n) /\ (?x. !n. sum (0, n) f <= x) ==> summable f``, 1639 RW_TAC std_ss [summable, sums, GSYM convergent] 1640 >> MATCH_MP_TAC SEQ_BCONV 1641 >> RW_TAC std_ss [SER_POS_MONO, netsTheory.MR1_BOUNDED] 1642 >> Q.EXISTS_TAC `x + 1` 1643 >> Q.EXISTS_TAC `N` 1644 >> RW_TAC arith_ss [] 1645 >> RW_TAC std_ss [abs, SUM_POS] 1646 >> Q.PAT_X_ASSUM `!n. P n` (MP_TAC o Q.SPEC `n`) 1647 >> REAL_ARITH_TAC); 1648 1649val SUMMABLE_LE = store_thm 1650 ("SUMMABLE_LE", 1651 ``!f x. summable f /\ (!n. sum (0, n) f <= x) ==> suminf f <= x``, 1652 Strip 1653 >> Suff `0 < suminf f - x ==> F` >- REAL_ARITH_TAC 1654 >> Strip 1655 >> Know `(\n. sum (0, n) f) --> suminf f` 1656 >- RW_TAC std_ss [GSYM sums, SUMMABLE_SUM] 1657 >> RW_TAC std_ss [SEQ] 1658 >> Q.EXISTS_TAC `suminf f - x` 1659 >> RW_TAC std_ss [] 1660 >> Q.EXISTS_TAC `N` 1661 >> Q.PAT_X_ASSUM `!n. P n` (MP_TAC o Q.SPEC `N`) 1662 >> RW_TAC real_ss [] 1663 >> ONCE_REWRITE_TAC [ABS_SUB] 1664 >> Know `0 <= suminf f - sum (0, N) f` 1665 >- (rpt (POP_ASSUM MP_TAC) 1666 >> REAL_ARITH_TAC) 1667 >> RW_TAC std_ss [abs] 1668 >> rpt (POP_ASSUM MP_TAC) 1669 >> REAL_ARITH_TAC); 1670 1671val SUMS_EQ = store_thm 1672 ("SUMS_EQ", 1673 ``!f x. f sums x = summable f /\ (suminf f = x)``, 1674 PROVE_TAC [SUM_SUMMABLE, SUM_UNIQ, summable]); 1675 1676val SUMINF_POS = store_thm 1677 ("SUMINF_POS", 1678 ``!f. (!n. 0 <= f n) /\ summable f ==> 0 <= suminf f``, 1679 RW_TAC std_ss [] 1680 >> Know `0 = sum (0, 0) f` >- RW_TAC std_ss [sum] 1681 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1682 >> MATCH_MP_TAC SER_POS_LE 1683 >> RW_TAC std_ss []); 1684 1685 val SUM_PICK = store_thm 1686 ("SUM_PICK", 1687 ``!n k x. sum (0, n) (\m. if m = k then x else 0) = if k < n then x else 0``, 1688 Induct >- RW_TAC arith_ss [sum] 1689 >> RW_TAC arith_ss [sum, REAL_ADD_RID, REAL_ADD_LID] 1690 >> Suff `F` >- PROVE_TAC [] 1691 >> NTAC 2 (POP_ASSUM MP_TAC) 1692 >> DECIDE_TAC); 1693 1694val SUM_LT = store_thm 1695 ("SUM_LT", 1696 ``!f g m n. 1697 (!r. m <= r /\ r < n + m ==> f r < g r) /\ 0 < n ==> 1698 sum (m,n) f < sum (m,n) g``, 1699 RW_TAC std_ss [] 1700 >> POP_ASSUM MP_TAC 1701 >> Cases_on `n` >- RW_TAC arith_ss [] 1702 >> RW_TAC arith_ss [] 1703 >> Induct_on `n'` >- RW_TAC arith_ss [sum, REAL_ADD_LID] 1704 >> ONCE_REWRITE_TAC [sum] 1705 >> Strip 1706 >> MATCH_MP_TAC REAL_LT_ADD2 1707 >> CONJ_TAC 1708 >- (Q.PAT_X_ASSUM `a ==> b` MATCH_MP_TAC 1709 >> RW_TAC arith_ss []) 1710 >> RW_TAC arith_ss []); 1711 1712val SUM_CONST_R = store_thm 1713 ("SUM_CONST_R", 1714 ``!n r. sum (0,n) (K r) = &n * r``, 1715 Induct >- RW_TAC real_ss [sum] 1716 >> RW_TAC bool_ss [sum, ADD1, K_THM, GSYM REAL_ADD, REAL_ADD_RDISTRIB] 1717 >> RW_TAC real_ss []); 1718 1719val SUMS_ZERO = store_thm 1720 ("SUMS_ZERO", 1721 ``(K 0) sums 0``, 1722 RW_TAC real_ss [sums, SEQ, SUM_CONST_R, abs, REAL_SUB_REFL, REAL_LE_REFL]); 1723 1724val LT_SUC = store_thm 1725 ("LT_SUC", ``!a b. a < SUC b = a < b \/ (a = b)``, DECIDE_TAC); 1726 1727val LE_SUC = store_thm 1728 ("LE_SUC", ``!a b. a <= SUC b = a <= b \/ (a = SUC b)``, DECIDE_TAC); 1729 1730val K_PARTIAL = store_thm 1731 ("K_PARTIAL", ``!x. K x = \z. x``, RW_TAC std_ss [K_DEF]); 1732 1733val HALF_POS = store_thm 1734 ("HALF_POS", ``0:real < 1/2``, 1735 PROVE_TAC [REAL_ARITH ``0:real < 1``, REAL_LT_HALF1]); 1736 1737val HALF_LT_1 = store_thm 1738 ("HALF_LT_1", ``1 / 2 < 1:real``, 1739 ONCE_REWRITE_TAC [GSYM REAL_INV_1OVER, GSYM REAL_INV1] 1740 >> MATCH_MP_TAC REAL_LT_INV 1741 >> RW_TAC arith_ss [REAL_LT]); 1742 1743val HALF_CANCEL = store_thm 1744 ("HALF_CANCEL", ``2 * (1 / 2) = 1:real``, 1745 Suff `2 * inv 2 = 1:real` >- PROVE_TAC [REAL_INV_1OVER] 1746 >> PROVE_TAC [REAL_MUL_RINV, REAL_ARITH ``~(2:real = 0)``]); 1747 1748val X_HALF_HALF = store_thm 1749 ("X_HALF_HALF", ``!x:real. 1/2 * x + 1/2 * x = x``, 1750 STRIP_TAC 1751 >> MATCH_MP_TAC (REAL_ARITH ``(2 * (a:real) = 2 * b) ==> (a = b)``) 1752 >> RW_TAC std_ss [REAL_ADD_LDISTRIB, REAL_MUL_ASSOC, HALF_CANCEL] 1753 >> REAL_ARITH_TAC); 1754 1755val ONE_MINUS_HALF = store_thm 1756 ("ONE_MINUS_HALF", ``(1:real) - 1 / 2 = 1 / 2``, 1757 MP_TAC (Q.SPEC `1` X_HALF_HALF) 1758 >> RW_TAC real_ss [] 1759 >> MATCH_MP_TAC (REAL_ARITH ``((x:real) + 1 / 2 = y + 1 / 2) ==> (x = y)``) 1760 >> RW_TAC std_ss [REAL_SUB_ADD]); 1761 1762(* from util_probTheory, TODO: move to pred_setTheory *) 1763val NUM_2D_BIJ_BIG_SQUARE = store_thm 1764 ("NUM_2D_BIJ_BIG_SQUARE", 1765 ``!(f : num -> num # num) N. 1766 BIJ f UNIV (UNIV CROSS UNIV) ==> 1767 ?k. IMAGE f (count N) SUBSET count k CROSS count k``, 1768 RW_TAC std_ss [IN_CROSS, IN_COUNT, SUBSET_DEF, IN_IMAGE, IN_COUNT] 1769 >> Induct_on `N` >- RW_TAC arith_ss [] 1770 >> Strip 1771 >> Cases_on `f N` 1772 >> REWRITE_TAC [prim_recTheory.LESS_THM] 1773 >> Q.EXISTS_TAC `SUC (MAX k (MAX q r))` 1774 >> Know `!a b. a < SUC b = a <= b` 1775 >- (KILL_TAC 1776 >> DECIDE_TAC) 1777 >> RW_TAC std_ss [] 1778 >> RW_TAC std_ss [] 1779 >> PROVE_TAC [X_LE_MAX, LESS_EQ_REFL, LESS_IMP_LESS_OR_EQ]); 1780 1781(* from util_probTheory, TODO: move to pred_setTheory *) 1782val NUM_2D_BIJ_SMALL_SQUARE = store_thm 1783 ("NUM_2D_BIJ_SMALL_SQUARE", 1784 ``!(f : num -> num # num) k. 1785 BIJ f UNIV (UNIV CROSS UNIV) ==> 1786 ?N. count k CROSS count k SUBSET IMAGE f (count N)``, 1787 Strip 1788 >> (MP_TAC o 1789 Q.SPECL [`f`, `UNIV CROSS UNIV`, `count k CROSS count k`] o 1790 INST_TYPE [``:'a`` |-> ``:num # num``]) BIJ_FINITE_SUBSET 1791 >> RW_TAC std_ss [CROSS_SUBSET, SUBSET_UNIV, FINITE_CROSS, FINITE_COUNT] 1792 >> Q.EXISTS_TAC `N` 1793 >> RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, IN_COUNT] 1794 >> Q.PAT_X_ASSUM `BIJ a b c` MP_TAC 1795 >> RW_TAC std_ss [BIJ_DEF, SURJ_DEF, IN_UNIV, IN_CROSS] 1796 >> POP_ASSUM (MP_TAC o Q.SPEC `x`) 1797 >> RW_TAC std_ss [] 1798 >> Q.EXISTS_TAC `y` 1799 >> RW_TAC std_ss [] 1800 >> Suff `~(N <= y)` >- DECIDE_TAC 1801 >> PROVE_TAC []); 1802 1803val SUMINF_ADD = store_thm 1804 ("SUMINF_ADD", 1805 ``!f g. 1806 summable f /\ summable g ==> 1807 summable (\n. f n + g n) /\ 1808 (suminf f + suminf g = suminf (\n. f n + g n))``, 1809 RW_TAC std_ss [] 1810 >> ( Know `f sums suminf f /\ g sums suminf g` >- PROVE_TAC [SUMMABLE_SUM] 1811 >> STRIP_TAC 1812 >> Know `(\n. f n + g n) sums (suminf f + suminf g)` 1813 >- RW_TAC std_ss [SER_ADD] 1814 >> RW_TAC std_ss [SUMS_EQ] )); 1815 1816val SUMINF_2D = store_thm 1817 ("SUMINF_2D", 1818 ``!f g h. 1819 (!m n. 0 <= f m n) /\ (!n. f n sums g n) /\ summable g /\ 1820 BIJ h UNIV (UNIV CROSS UNIV) ==> 1821 (UNCURRY f o h) sums suminf g``, 1822 RW_TAC std_ss [] 1823 >> RW_TAC std_ss [sums] 1824 >> Know `g sums suminf g` >- PROVE_TAC [SUMMABLE_SUM] 1825 >> Q.PAT_X_ASSUM `!n. P n` MP_TAC 1826 >> RW_TAC std_ss [SUMS_EQ, FORALL_AND_THM] 1827 >> MATCH_MP_TAC INCREASING_SEQ 1828 >> CONJ_TAC 1829 >- (RW_TAC std_ss [sum, o_THM, ADD_CLAUSES] 1830 >> Cases_on `h n` 1831 >> RW_TAC std_ss [UNCURRY_DEF] 1832 >> Q.PAT_X_ASSUM `!m n. 0 <= f m n` (MP_TAC o Q.SPECL [`q`, `r`]) 1833 >> REAL_ARITH_TAC) 1834 >> Know `!m. 0 <= g m` 1835 >- (STRIP_TAC 1836 >> Suff `0 <= suminf (f m)` >- PROVE_TAC [] 1837 >> MATCH_MP_TAC SER_POS 1838 >> PROVE_TAC []) 1839 >> STRIP_TAC 1840 >> CONJ_TAC 1841 >- (RW_TAC std_ss [] 1842 >> MP_TAC (Q.SPECL [`h`, `n`] NUM_2D_BIJ_BIG_SQUARE) 1843 >> ASM_REWRITE_TAC [] 1844 >> STRIP_TAC 1845 >> MATCH_MP_TAC REAL_LE_TRANS 1846 >> Q.EXISTS_TAC `sum (0,k) g` 1847 >> REVERSE CONJ_TAC 1848 >- (MATCH_MP_TAC SER_POS_LE 1849 >> PROVE_TAC []) 1850 >> MATCH_MP_TAC REAL_LE_TRANS 1851 >> Q.EXISTS_TAC `sum (0,k) (\m. sum (0,k) (f m))` 1852 >> REVERSE CONJ_TAC 1853 >- (MATCH_MP_TAC SUM_LE 1854 >> RW_TAC std_ss [] 1855 >> Q.PAT_X_ASSUM `!n. suminf (f n) = g n` (REWRITE_TAC o wrap o GSYM) 1856 >> MATCH_MP_TAC SER_POS_LE 1857 >> PROVE_TAC []) 1858 >> Suff 1859 `!j. 1860 j <= n ==> 1861 (sum (0, j) (UNCURRY f o h) = 1862 sum (0, k) 1863 (\m. sum (0, k) 1864 (\n. if (?i. i < j /\ (h i = (m, n))) then f m n else 0)))` 1865 >- (DISCH_THEN (MP_TAC o Q.SPEC `n`) 1866 >> REWRITE_TAC [LESS_EQ_REFL] 1867 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1868 >> MATCH_MP_TAC SUM_LE 1869 >> RW_TAC std_ss [] 1870 >> MATCH_MP_TAC SUM_LE 1871 >> RW_TAC std_ss [REAL_LE_REFL]) 1872 >> Induct >- RW_TAC arith_ss [sum, SUM_0] 1873 >> RW_TAC std_ss [sum] 1874 >> Q.PAT_X_ASSUM `p ==> q` MP_TAC 1875 >> RW_TAC arith_ss [] 1876 >> Know 1877 `!m n. 1878 (?i. i < SUC j /\ (h i = (m,n))) = 1879 (?i. i < j /\ (h i = (m,n))) \/ (h j = (m, n))` 1880 >- (RW_TAC std_ss [] 1881 >> Suff `!i. i < SUC j = i < j \/ (i = j)` 1882 >- PROVE_TAC [] 1883 >> DECIDE_TAC) 1884 >> DISCH_THEN (REWRITE_TAC o wrap) 1885 >> Know 1886 `!m n. 1887 (if (?i. i < j /\ (h i = (m,n))) \/ (h j = (m,n)) then f m n 1888 else 0) = 1889 (if (?i. i < j /\ (h i = (m,n))) then f m n else 0) + 1890 (if (h j = (m,n)) then f m n else 0)` 1891 >- (Strip 1892 >> Suff `(?i. i < j /\ (h i = (m,n'))) ==> ~(h j = (m,n'))` 1893 >- PROVE_TAC [REAL_ADD_LID, REAL_ADD_RID] 1894 >> RW_TAC std_ss [] 1895 >> Q.PAT_X_ASSUM `BIJ a b c` MP_TAC 1896 >> RW_TAC std_ss [BIJ_DEF, INJ_DEF, IN_UNIV, IN_CROSS] 1897 >> PROVE_TAC [prim_recTheory.LESS_REFL]) 1898 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 1899 >> RW_TAC std_ss [SUM_ADD] 1900 >> POP_ASSUM K_TAC 1901 >> Suff 1902 `(UNCURRY f o h) j = 1903 sum (0,k) 1904 (\m. sum (0,k) (\n. (if h j = (m,n) then f m n else 0)))` 1905 >- (KILL_TAC 1906 >> Q.SPEC_TAC 1907 (`(sum (0,k) 1908 (\m. 1909 sum (0,k) 1910 (\n. if ?i. i < j /\ (h i = (m,n)) then f m n else 0)))`, 1911 `r1`) 1912 >> Q.SPEC_TAC 1913 (`sum (0,k) 1914 (\m. sum (0,k) (\n. (if h j = (m,n) then f m n else 0)))`, 1915 `r2`) 1916 >> RW_TAC std_ss []) 1917 >> Cases_on `h j` 1918 >> RW_TAC std_ss [o_THM, UNCURRY_DEF] 1919 >> Know 1920 `!m n. 1921 (if (q = m) /\ (r = n) then f m n else 0) = 1922 (if (n = r) then if (m = q) then f m n else 0 else 0)` 1923 >- PROVE_TAC [] 1924 >> DISCH_THEN (REWRITE_TAC o wrap) 1925 >> Q.PAT_X_ASSUM `a SUBSET b` MP_TAC 1926 >> RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, IN_COUNT, IN_CROSS] 1927 >> Suff `q < k /\ r < k` 1928 >- RW_TAC std_ss [SUM_PICK] 1929 >> POP_ASSUM (MP_TAC o Q.SPEC `h (j:num)`) 1930 >> Suff `j < n` 1931 >- (RW_TAC std_ss [] 1932 >> PROVE_TAC []) 1933 >> DECIDE_TAC) 1934 >> RW_TAC std_ss [] 1935 >> Know `?M. 0 < M /\ suminf g < sum (0, M) g + e / 2` 1936 >- (Know `g sums suminf g` >- PROVE_TAC [SUMMABLE_SUM] 1937 >> RW_TAC std_ss [sums, SEQ] 1938 >> POP_ASSUM (MP_TAC o Q.SPEC `e / 2`) 1939 >> RW_TAC std_ss [REAL_LT_HALF1, GREATER_EQ] 1940 >> POP_ASSUM (MP_TAC o Q.SPEC `SUC N`) 1941 >> ONCE_REWRITE_TAC [ABS_SUB] 1942 >> Know `sum (0, SUC N) g <= suminf g` 1943 >- (MATCH_MP_TAC SER_POS_LE 1944 >> RW_TAC std_ss []) 1945 >> REVERSE (RW_TAC arith_ss [abs]) 1946 >- (Suff `F` >- PROVE_TAC [] 1947 >> POP_ASSUM K_TAC 1948 >> POP_ASSUM MP_TAC 1949 >> POP_ASSUM MP_TAC 1950 >> REAL_ARITH_TAC) 1951 >> Q.EXISTS_TAC `SUC N` 1952 >> CONJ_TAC >- DECIDE_TAC 1953 >> POP_ASSUM MP_TAC 1954 >> REAL_ARITH_TAC) 1955 >> RW_TAC std_ss [] 1956 >> Suff `?k. sum (0, M) g < sum (0, k) (UNCURRY f o h) + e / 2` 1957 >- (Strip 1958 >> Q.EXISTS_TAC `k` 1959 >> Know 1960 `sum (0, M) g + e / 2 < sum (0, k) (UNCURRY f o h) + (e / 2 + e / 2)` 1961 >- (POP_ASSUM MP_TAC 1962 >> REAL_ARITH_TAC) 1963 >> POP_ASSUM K_TAC 1964 >> POP_ASSUM MP_TAC 1965 >> REWRITE_TAC [REAL_HALF_DOUBLE] 1966 >> REAL_ARITH_TAC) 1967 >> POP_ASSUM K_TAC 1968 >> Know `!m. ?N. g m < sum (0, N) (f m) + (e / 2) / & M` 1969 >- (Know `!m. f m sums g m` 1970 >- RW_TAC std_ss [SUMS_EQ] 1971 >> RW_TAC std_ss [sums, SEQ] 1972 >> POP_ASSUM (MP_TAC o Q.SPECL [`m`, `(e / 2) / & M`]) 1973 >> Know `0 < (e / 2) / & M` 1974 >- RW_TAC arith_ss [REAL_LT_DIV, REAL_NZ_IMP_LT] 1975 >> DISCH_THEN (REWRITE_TAC o wrap) 1976 >> RW_TAC std_ss [GREATER_EQ] 1977 >> POP_ASSUM (MP_TAC o Q.SPEC `N`) 1978 >> ONCE_REWRITE_TAC [ABS_SUB] 1979 >> Know `sum (0, N) (f m) <= g m` 1980 >- (Q.PAT_X_ASSUM `!n. P n = Q n` (REWRITE_TAC o wrap o GSYM) 1981 >> MATCH_MP_TAC SER_POS_LE 1982 >> RW_TAC std_ss []) 1983 >> REVERSE (RW_TAC arith_ss [abs]) 1984 >- (POP_ASSUM K_TAC 1985 >> Suff `F` >- PROVE_TAC [] 1986 >> NTAC 2 (POP_ASSUM MP_TAC) 1987 >> REAL_ARITH_TAC) 1988 >> Q.EXISTS_TAC `N` 1989 >> POP_ASSUM MP_TAC 1990 >> REAL_ARITH_TAC) 1991 >> DISCH_THEN (MP_TAC o CONV_RULE SKOLEM_CONV) 1992 >> RW_TAC std_ss [] 1993 >> Know `?c. M <= c /\ !m. m < M ==> N m <= c` 1994 >- (KILL_TAC 1995 >> Induct_on `M` >- RW_TAC arith_ss [] 1996 >> Strip 1997 >> Q.EXISTS_TAC `MAX (SUC c) (N M)` 1998 >> RW_TAC arith_ss [X_LE_MAX, LT_SUC] 1999 >> PROVE_TAC [LESS_EQ_REFL, LE]) 2000 >> Strip 2001 >> MP_TAC (Q.SPECL [`h`, `c`] NUM_2D_BIJ_SMALL_SQUARE) 2002 >> ASM_REWRITE_TAC [] 2003 >> DISCH_THEN (Q.X_CHOOSE_TAC `k`) 2004 >> Q.EXISTS_TAC `k` 2005 >> MATCH_MP_TAC REAL_LTE_TRANS 2006 >> Q.EXISTS_TAC `sum (0, M) (\m. sum (0, N m) (f m) + e / 2 / &M)` 2007 >> CONJ_TAC 2008 >- (MATCH_MP_TAC SUM_LT 2009 >> RW_TAC arith_ss []) 2010 >> RW_TAC std_ss [SUM_ADD, GSYM K_PARTIAL, SUM_CONST_R] 2011 >> Know `!x:real. & M * (x / & M) = x` 2012 >- (RW_TAC std_ss [real_div] 2013 >> Suff `(& M * inv (& M)) * x = x` 2014 >- PROVE_TAC [REAL_MUL_ASSOC, REAL_MUL_SYM] 2015 >> Suff `~(& M = 0:real)` >- RW_TAC std_ss [REAL_MUL_RINV, REAL_MUL_LID] 2016 >> RW_TAC arith_ss [REAL_INJ]) 2017 >> DISCH_THEN (REWRITE_TAC o wrap) 2018 >> RW_TAC std_ss [REAL_LE_RADD] 2019 >> Suff 2020 `sum (0,M) (\m. sum (0,N m) (f m)) = 2021 sum (0, k) 2022 (\k. 2023 if ?m n. m < M /\ n < N m /\ (h k = (m, n)) then (UNCURRY f o h) k 2024 else 0)` 2025 >- (RW_TAC std_ss [] 2026 >> MATCH_MP_TAC SUM_LE 2027 >> RW_TAC std_ss [o_THM, REAL_LE_REFL] 2028 >> Cases_on `h r` 2029 >> RW_TAC std_ss [UNCURRY_DEF]) 2030 >> NTAC 3 (POP_ASSUM MP_TAC) 2031 >> Q.PAT_X_ASSUM `BIJ h a b` MP_TAC 2032 >> KILL_TAC 2033 >> RW_TAC std_ss [] 2034 >> Induct_on `M` >- RW_TAC arith_ss [sum, SUM_ZERO] 2035 >> RW_TAC arith_ss [sum, LT_SUC] 2036 >> Q.PAT_X_ASSUM `a ==> b` K_TAC 2037 >> Know 2038 `!k'. 2039 (?m n. (m < M \/ (m = M)) /\ n < N m /\ (h k' = (m, n))) = 2040 (?m n. m < M /\ n < N m /\ (h k' = (m, n))) \/ 2041 (?n. n < N M /\ (h k' = (M, n)))` 2042 >- PROVE_TAC [] 2043 >> DISCH_THEN (REWRITE_TAC o wrap) 2044 >> Know 2045 `!k'. 2046 (if (?m n. m < M /\ n < N m /\ (h k' = (m,n))) \/ 2047 (?n. n < N M /\ (h k' = (M,n))) 2048 then UNCURRY f (h k') 2049 else 0) = 2050 (if (?m n. m < M /\ n < N m /\ (h k' = (m,n))) then UNCURRY f (h k') 2051 else 0) + 2052 (if (?n. n < N M /\ (h k' = (M,n))) then UNCURRY f (h k') 2053 else 0)` 2054 >- (STRIP_TAC 2055 >> Suff 2056 `(?m n. m < M /\ n < N m /\ (h k' = (m,n))) ==> 2057 ~(?n. n < N M /\ (h k' = (M,n)))` 2058 >- PROVE_TAC [REAL_ADD_RID, REAL_ADD_LID] 2059 >> Cases_on `h k'` 2060 >> RW_TAC arith_ss []) 2061 >> DISCH_THEN (REWRITE_TAC o wrap) 2062 >> RW_TAC std_ss [SUM_ADD, REAL_EQ_LADD] 2063 >> Know `N M <= c` >- PROVE_TAC [] 2064 >> POP_ASSUM K_TAC 2065 >> Q.SPEC_TAC (`N M`, `l`) 2066 >> Induct >- RW_TAC real_ss [sum, SUM_0] 2067 >> RW_TAC arith_ss [sum, LT_SUC] 2068 >> Q.PAT_X_ASSUM `a ==> b` K_TAC 2069 >> Know 2070 `!k'. 2071 (?n. (n < l \/ (n = l)) /\ (h k' = (M,n))) = 2072 (?n. n < l /\ (h k' = (M,n))) \/ (h k' = (M, l))` 2073 >- PROVE_TAC [] 2074 >> DISCH_THEN (REWRITE_TAC o wrap) 2075 >> Know 2076 `!k'. 2077 (if (?n. n < l /\ (h k' = (M,n))) \/ (h k' = (M, l)) then 2078 UNCURRY f (h k') 2079 else 0) = 2080 (if (?n. n < l /\ (h k' = (M,n))) then UNCURRY f (h k') else 0) + 2081 (if (h k' = (M, l)) then UNCURRY f (h k') else 0)` 2082 >- (STRIP_TAC 2083 >> Suff `(?n. n < l /\ (h k' = (M,n))) ==> ~(h k' = (M, l))` 2084 >- PROVE_TAC [REAL_ADD_LID, REAL_ADD_RID] 2085 >> Cases_on `h k'` 2086 >> RW_TAC arith_ss []) 2087 >> DISCH_THEN (REWRITE_TAC o wrap) 2088 >> RW_TAC std_ss [SUM_ADD, REAL_EQ_LADD] 2089 >> Q.PAT_X_ASSUM `a SUBSET b` MP_TAC 2090 >> RW_TAC std_ss [SUBSET_DEF, IN_CROSS, IN_COUNT, IN_IMAGE] 2091 >> POP_ASSUM (MP_TAC o Q.SPEC `(M, l)`) 2092 >> RW_TAC arith_ss [] 2093 >> Suff `!k'. (h k' = (M, l)) = (k' = x')` 2094 >- (RW_TAC std_ss [SUM_PICK, o_THM] 2095 >> Q.PAT_X_ASSUM `(M,l) = a` (REWRITE_TAC o wrap o GSYM) 2096 >> RW_TAC std_ss [UNCURRY_DEF]) 2097 >> Q.PAT_X_ASSUM `BIJ h a b` MP_TAC 2098 >> RW_TAC std_ss [BIJ_DEF, INJ_DEF, IN_UNIV, IN_CROSS] 2099 >> PROVE_TAC []); 2100 2101val POW_HALF_SER = store_thm 2102 ("POW_HALF_SER", 2103 ``(\n. (1 / 2) pow (n + 1)) sums 1``, 2104 Know `(\n. (1 / 2) pow n) sums inv (1 - (1 / 2))` 2105 >- (MATCH_MP_TAC GP 2106 >> RW_TAC std_ss [abs, HALF_POS, REAL_LT_IMP_LE, HALF_LT_1]) 2107 >> RW_TAC std_ss [ONE_MINUS_HALF, REAL_INV_INV, GSYM REAL_INV_1OVER, 2108 GSYM ADD1, pow] 2109 >> Know `1 = inv 2 * 2:real` 2110 >- RW_TAC arith_ss [REAL_MUL_LINV, REAL_INJ] 2111 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap) 2112 >> HO_MATCH_MP_TAC SER_CMUL 2113 >> RW_TAC std_ss []); 2114 2115val SER_POS_COMPARE = store_thm 2116 ("SER_POS_COMPARE", 2117 ``!f g. 2118 (!n. 0 <= f n) /\ summable g /\ (!n. f n <= g n) ==> 2119 summable f /\ suminf f <= suminf g``, 2120 REVERSE (rpt (STRONG_CONJ_TAC ORELSE STRIP_TAC)) 2121 >- PROVE_TAC [SER_LE] 2122 >> MATCH_MP_TAC SER_COMPAR 2123 >> Q.EXISTS_TAC `g` 2124 >> RW_TAC std_ss [] 2125 >> Q.EXISTS_TAC `0` 2126 >> RW_TAC arith_ss [abs]); 2127 2128val _ = export_theory(); 2129