1(*===========================================================================*) 2(* Theory of Moore-Smith covergence nets, and special cases like sequences *) 3(*===========================================================================*) 4 5(* 6app load ["hol88Lib", 7 "numLib", 8 "reduceLib", 9 "pairTheory", 10 "PairedLambda", 11 "jrhUtils", 12 "metricTheory"]; 13*) 14 15(* 16*) 17open HolKernel Parse boolLib hol88Lib numLib reduceLib pairLib 18 pairTheory arithmeticTheory numTheory prim_recTheory 19 jrhUtils realTheory topologyTheory metricTheory; 20 21val re_subset = REWRITE_RULE [pred_setTheory.SPECIFICATION] 22 pred_setTheory.SUBSET_DEF 23 24val _ = new_theory "nets"; 25val _ = ParseExtras.temp_loose_equality() 26 27val _ = Parse.reveal "B"; 28 29val num_EQ_CONV = Arithconv.NEQ_CONV; 30 31(*---------------------------------------------------------------------------*) 32(* Basic definitions: directed set, net, bounded net, pointwise limit *) 33(*---------------------------------------------------------------------------*) 34 35val dorder = new_definition("dorder", 36 ���dorder (g:'a->'a->bool) = 37 !x y. g x x /\ g y y ==> ?z. g z z /\ (!w. g w z ==> g w x /\ g w y)���); 38 39val tends = new_infixr_definition("tends", 40 ���($tends s l)(top,g) = 41 !N:'a->bool. neigh(top)(N,l) ==> 42 ?n:'b. g n n /\ !m:'b. g m n ==> N(s m)���, 750); 43 44val bounded = new_definition("bounded", 45 ���bounded(m:('a)metric,(g:'b->'b->bool)) f = 46 ?k x N. g N N /\ (!n. g n N ==> (dist m)(f(n),x) < k)���); 47 48val tendsto = new_definition("tendsto", 49 ���tendsto(m:('a)metric,x) y z = 50 &0 < (dist m)(x,y) /\ (dist m)(x,y) <= (dist m)(x,z)���); 51 52val DORDER_LEMMA = store_thm("DORDER_LEMMA", 53 ���!g:'a->'a->bool. 54 dorder g ==> 55 !P Q. (?n. g n n /\ (!m. g m n ==> P m)) /\ 56 (?n. g n n /\ (!m. g m n ==> Q m)) 57 ==> (?n. g n n /\ (!m. g m n ==> P m /\ Q m))���, 58 GEN_TAC THEN REWRITE_TAC[dorder] THEN DISCH_TAC THEN REPEAT GEN_TAC THEN 59 DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_THEN ���N1:'a��� STRIP_ASSUME_TAC) 60 (X_CHOOSE_THEN ���N2:'a��� STRIP_ASSUME_TAC)) THEN 61 FIRST_ASSUM(MP_TAC o SPECL [���N1:'a���, ���N2:'a���]) THEN 62 REWRITE_TAC[ASSUME ���(g:'a->'a->bool) N1 N1���,ASSUME ���(g:'a->'a->bool) N2 N2���] THEN 63 DISCH_THEN(X_CHOOSE_THEN ���n:'a��� STRIP_ASSUME_TAC) THEN 64 EXISTS_TAC ���n:'a��� THEN ASM_REWRITE_TAC[] THEN 65 X_GEN_TAC ���m:'a��� THEN DISCH_TAC THEN 66 CONJ_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN 67 FIRST_ASSUM(UNDISCH_TAC o 68 assert(is_conj o snd o dest_imp o snd o dest_forall) o concl) THEN 69 DISCH_THEN(MP_TAC o SPEC ���m:'a���) THEN ASM_REWRITE_TAC[] THEN 70 DISCH_TAC THEN ASM_REWRITE_TAC[]); 71 72(*---------------------------------------------------------------------------*) 73(* Following tactic is useful in the following proofs *) 74(*---------------------------------------------------------------------------*) 75 76fun DORDER_THEN tac th = 77 let val findpr = snd o dest_imp o body o rand o rand o body o rand 78 val (t1,t2) = case map (rand o rand o body o rand) 79 (strip_conj (concl th)) of 80 [t1, t2] => (t1, t2) 81 | _ => raise Match 82 val dog = (rator o rator o rand o rator o body) t1 83 val thl = map ((uncurry X_BETA_CONV) o (I ## rand) o dest_abs) [t1,t2] 84 val th1 = CONV_RULE(EXACT_CONV thl) th 85 val th2 = MATCH_MP DORDER_LEMMA (ASSUME ���dorder ^dog���) 86 val th3 = MATCH_MP th2 th1 87 val th4 = CONV_RULE(EXACT_CONV(map SYM thl)) th3 in 88 tac th4 end; 89 90(*---------------------------------------------------------------------------*) 91(* Show that sequences and pointwise limits in a metric space are directed *) 92(*---------------------------------------------------------------------------*) 93 94val DORDER_NGE = store_thm("DORDER_NGE", 95 ���dorder ($>= :num->num->bool)���, 96 REWRITE_TAC[dorder, GREATER_EQ, LESS_EQ_REFL] THEN 97 REPEAT GEN_TAC THEN 98 DISJ_CASES_TAC(SPECL [���x:num���, ���y:num���] LESS_EQ_CASES) THENL 99 [EXISTS_TAC ���y:num���, EXISTS_TAC ���x:num���] THEN 100 GEN_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN 101 MATCH_MP_TAC LESS_EQ_TRANS THENL 102 [EXISTS_TAC ���y:num���, EXISTS_TAC ���x:num���] THEN 103 ASM_REWRITE_TAC[]); 104 105val DORDER_TENDSTO = store_thm("DORDER_TENDSTO", 106 ���!m:('a)metric. !x. dorder(tendsto(m,x))���, 107 REPEAT GEN_TAC THEN REWRITE_TAC[dorder, tendsto] THEN 108 MAP_EVERY X_GEN_TAC [���u:'a���, ���v:'a���] THEN 109 REWRITE_TAC[REAL_LE_REFL] THEN 110 DISCH_THEN STRIP_ASSUME_TAC THEN ASM_REWRITE_TAC[] THEN 111 DISJ_CASES_TAC(SPECL [���(dist m)(x:'a,v)���, ���(dist m)(x:'a,u)���] REAL_LE_TOTAL) 112 THENL [EXISTS_TAC ���v:'a���, EXISTS_TAC ���u:'a���] THEN ASM_REWRITE_TAC[] THEN 113 GEN_TAC THEN DISCH_THEN STRIP_ASSUME_TAC THEN ASM_REWRITE_TAC[] THEN 114 MATCH_MP_TAC REAL_LE_TRANS THEN FIRST_ASSUM 115 (fn th => (EXISTS_TAC o rand o concl) th THEN ASM_REWRITE_TAC[] THEN NO_TAC)); 116 117(*---------------------------------------------------------------------------*) 118(* Simpler characterization of limit in a metric topology *) 119(*---------------------------------------------------------------------------*) 120 121val MTOP_TENDS = store_thm("MTOP_TENDS", 122 ���!d g. !x:'b->'a. !x0. (x tends x0)(mtop(d),g) = 123 !e. &0 < e ==> ?n. g n n /\ !m. g m n ==> dist(d)(x(m),x0) < e���, 124 REPEAT GEN_TAC THEN REWRITE_TAC[tends] THEN EQ_TAC THEN DISCH_TAC THENL 125 [GEN_TAC THEN DISCH_TAC THEN 126 FIRST_ASSUM(MP_TAC o SPEC ���B(d)(x0:'a,e)���) THEN 127 W(C SUBGOAL_THEN MP_TAC o funpow 2 (rand o rator) o snd) THENL 128 [MATCH_MP_TAC BALL_NEIGH THEN ASM_REWRITE_TAC[], ALL_TAC] THEN 129 DISCH_THEN(fn th => REWRITE_TAC[th]) THEN REWRITE_TAC[ball] THEN 130 BETA_TAC THEN 131 GEN_REWR_TAC (RAND_CONV o ONCE_DEPTH_CONV) [METRIC_SYM] THEN REWRITE_TAC[], 132 GEN_TAC THEN REWRITE_TAC[neigh] THEN 133 DISCH_THEN(X_CHOOSE_THEN ���P:'a->bool��� STRIP_ASSUME_TAC) THEN 134 UNDISCH_TAC ���open_in(mtop(d)) (P:'a->bool)��� THEN 135 REWRITE_TAC[MTOP_OPEN] THEN DISCH_THEN(MP_TAC o SPEC ���x0:'a���) THEN 136 ASM_REWRITE_TAC[] THEN 137 DISCH_THEN(X_CHOOSE_THEN ���d:real��� STRIP_ASSUME_TAC) THEN 138 FIRST_ASSUM(MP_TAC o SPEC ���d:real���) THEN 139 REWRITE_TAC[ASSUME ���&0 < d���] THEN 140 DISCH_THEN(X_CHOOSE_THEN ���n:'b��� STRIP_ASSUME_TAC) THEN 141 EXISTS_TAC ���n:'b��� THEN ASM_REWRITE_TAC[] THEN 142 GEN_TAC THEN DISCH_TAC THEN 143 UNDISCH_TAC ���(P:'a->bool) SUBSET N��� THEN 144 REWRITE_TAC[re_subset] THEN DISCH_TAC THEN 145 REPEAT(FIRST_ASSUM MATCH_MP_TAC) THEN 146 ONCE_REWRITE_TAC[METRIC_SYM] THEN 147 FIRST_ASSUM MATCH_MP_TAC THEN FIRST_ASSUM ACCEPT_TAC]); 148 149(*---------------------------------------------------------------------------*) 150(* Prove that a net in a metric topology cannot converge to different limits *) 151(*---------------------------------------------------------------------------*) 152 153val MTOP_TENDS_UNIQ = store_thm("MTOP_TENDS_UNIQ", 154 ���!g d. dorder (g:'b->'b->bool) ==> 155 (x tends x0)(mtop(d),g) /\ (x tends x1)(mtop(d),g) ==> (x0:'a = x1)���, 156 REPEAT GEN_TAC THEN DISCH_TAC THEN 157 REWRITE_TAC[MTOP_TENDS] THEN 158 CONV_TAC(ONCE_DEPTH_CONV AND_FORALL_CONV) THEN 159 REWRITE_TAC[TAUT_CONV ���(a ==> b) /\ (a ==> c) = a ==> b /\ c���] THEN 160 CONV_TAC CONTRAPOS_CONV THEN DISCH_TAC THEN 161 CONV_TAC NOT_FORALL_CONV THEN 162 EXISTS_TAC ���dist(d:('a)metric)(x0,x1) / &2��� THEN 163 W(C SUBGOAL_THEN ASSUME_TAC o rand o rator o rand o snd) THENL 164 [REWRITE_TAC[REAL_LT_HALF1] THEN MATCH_MP_TAC METRIC_NZ THEN 165 FIRST_ASSUM ACCEPT_TAC, ALL_TAC] THEN 166 ASM_REWRITE_TAC[] THEN DISCH_THEN(DORDER_THEN MP_TAC) THEN 167 DISCH_THEN(X_CHOOSE_THEN ���N:'b��� (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN 168 DISCH_THEN(MP_TAC o SPEC ���N:'b���) THEN ASM_REWRITE_TAC[] THEN 169 BETA_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP REAL_LT_ADD2) THEN 170 REWRITE_TAC[REAL_HALF_DOUBLE, REAL_NOT_LT] THEN 171 GEN_REWR_TAC(RAND_CONV o LAND_CONV) [METRIC_SYM] THEN 172 MATCH_ACCEPT_TAC METRIC_TRIANGLE); 173 174(*---------------------------------------------------------------------------*) 175(* Simpler characterization of limit of a sequence in a metric topology *) 176(*---------------------------------------------------------------------------*) 177 178val geq = Term`$>= : num->num->bool`; 179 180val SEQ_TENDS = store_thm("SEQ_TENDS", 181 ���!d:('a)metric. !x x0. (x tends x0)(mtop(d), ^geq) = 182 !e. &0 < e ==> ?N. !n. ^geq n N ==> dist(d)(x(n),x0) < e���, 183 REPEAT GEN_TAC THEN REWRITE_TAC[MTOP_TENDS, GREATER_EQ, LESS_EQ_REFL]); 184 185(*---------------------------------------------------------------------------*) 186(* And of limit of function between metric spaces *) 187(*---------------------------------------------------------------------------*) 188 189val LIM_TENDS = store_thm("LIM_TENDS", 190 ���!m1:('a)metric. !m2:('b)metric. !f x0 y0. 191 limpt(mtop m1) x0 UNIV ==> 192 ((f tends y0)(mtop(m2),tendsto(m1,x0)) = 193 !e. &0 < e ==> 194 ?d. &0 < d /\ !x. &0 < (dist m1)(x,x0) /\ (dist m1)(x,x0) <= d ==> 195 (dist m2)(f(x),y0) < e)���, 196 REPEAT GEN_TAC THEN DISCH_TAC THEN 197 REWRITE_TAC[MTOP_TENDS, tendsto] THEN 198 AP_TERM_TAC THEN ABS_TAC THEN 199 ASM_CASES_TAC ���&0 < e��� THEN ASM_REWRITE_TAC[] THEN 200 REWRITE_TAC[REAL_LE_REFL] THEN EQ_TAC THENL 201 [DISCH_THEN(X_CHOOSE_THEN ���z:'a��� STRIP_ASSUME_TAC) THEN 202 EXISTS_TAC ���(dist m1)(x0:'a,z)��� THEN ASM_REWRITE_TAC[] THEN 203 GEN_TAC THEN DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN 204 ASM_REWRITE_TAC[] THEN 205 SUBST1_TAC(ISPECL [���m1:('a)metric���, ���x0:'a���, ���x:'a���] METRIC_SYM) THEN 206 ASM_REWRITE_TAC[], 207 DISCH_THEN(X_CHOOSE_THEN ���d:real��� STRIP_ASSUME_TAC) THEN 208 UNDISCH_TAC ���limpt(mtop m1) (x0:'a) UNIV��� THEN 209 REWRITE_TAC[MTOP_LIMPT] THEN 210 DISCH_THEN(MP_TAC o SPEC ���d:real���) THEN ASM_REWRITE_TAC[] THEN 211 REWRITE_TAC[pred_setTheory.UNIV_DEF] THEN 212 DISCH_THEN(X_CHOOSE_THEN ���y:'a��� STRIP_ASSUME_TAC) THEN 213 EXISTS_TAC ���y:'a��� THEN CONJ_TAC THENL 214 [MATCH_MP_TAC METRIC_NZ THEN ASM_REWRITE_TAC[], ALL_TAC] THEN 215 X_GEN_TAC ���x:'a��� THEN DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN 216 ONCE_REWRITE_TAC[METRIC_SYM] THEN ASM_REWRITE_TAC[] THEN 217 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC ���(dist m1)(x0:'a,y)��� THEN 218 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN 219 FIRST_ASSUM ACCEPT_TAC]); 220 221(*---------------------------------------------------------------------------*) 222(* Similar, more conventional version, is also true at a limit point *) 223(*---------------------------------------------------------------------------*) 224 225val LIM_TENDS2 = store_thm("LIM_TENDS2", 226 ���!m1:('a)metric. !m2:('b)metric. !f x0 y0. 227 limpt(mtop m1) x0 UNIV ==> 228 ((f tends y0)(mtop(m2),tendsto(m1,x0)) = 229 !e. &0 < e ==> 230 ?d. &0 < d /\ !x. &0 < (dist m1)(x,x0) /\ (dist m1)(x,x0) < d ==> 231 (dist m2)(f(x),y0) < e)���, 232 REPEAT GEN_TAC THEN DISCH_TAC THEN 233 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP LIM_TENDS th]) THEN 234 AP_TERM_TAC THEN ABS_TAC THEN AP_TERM_TAC THEN 235 EQ_TAC THEN DISCH_THEN(X_CHOOSE_THEN ���d:real��� STRIP_ASSUME_TAC) THENL 236 [EXISTS_TAC ���d:real��� THEN ASM_REWRITE_TAC[] THEN 237 GEN_TAC THEN DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN 238 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[], 239 EXISTS_TAC ���d / &2��� THEN ASM_REWRITE_TAC[REAL_LT_HALF1] THEN 240 GEN_TAC THEN DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN 241 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LET_TRANS THEN 242 EXISTS_TAC ���d / &2��� THEN ASM_REWRITE_TAC[REAL_LT_HALF2]]); 243 244(*---------------------------------------------------------------------------*) 245(* Simpler characterization of boundedness for the real line *) 246(*---------------------------------------------------------------------------*) 247 248val MR1_BOUNDED = store_thm("MR1_BOUNDED", 249 ���!(g:'a->'a->bool) f. bounded(mr1,g) f = 250 ?k N. g N N /\ (!n. g n N ==> abs(f n) < k)���, 251 REPEAT GEN_TAC THEN REWRITE_TAC[bounded, MR1_DEF] THEN 252 (CONV_TAC o LAND_CONV o RAND_CONV o ABS_CONV) SWAP_EXISTS_CONV 253 THEN CONV_TAC(ONCE_DEPTH_CONV SWAP_EXISTS_CONV) THEN 254 AP_TERM_TAC THEN ABS_TAC THEN 255 CONV_TAC(REDEPTH_CONV EXISTS_AND_CONV) THEN 256 AP_TERM_TAC THEN EQ_TAC THEN 257 DISCH_THEN(X_CHOOSE_THEN ���k:real��� MP_TAC) THENL 258 [DISCH_THEN(X_CHOOSE_TAC ���x:real���) THEN 259 EXISTS_TAC ���abs(x) + k��� THEN GEN_TAC THEN DISCH_TAC THEN 260 SUBST1_TAC 261 (SYM(SPECL [���(f:'a->real) n���, ���x:real���] REAL_SUB_ADD)) THEN 262 MATCH_MP_TAC REAL_LET_TRANS THEN 263 EXISTS_TAC ���abs((f:'a->real) n - x) + abs(x)��� THEN 264 REWRITE_TAC[ABS_TRIANGLE] THEN 265 GEN_REWR_TAC RAND_CONV [REAL_ADD_SYM] THEN 266 REWRITE_TAC[REAL_LT_RADD] THEN 267 ONCE_REWRITE_TAC[ABS_SUB] THEN 268 FIRST_ASSUM MATCH_MP_TAC THEN FIRST_ASSUM ACCEPT_TAC, 269 DISCH_TAC THEN MAP_EVERY EXISTS_TAC [���k:real���, ���&0���] THEN 270 ASM_REWRITE_TAC[REAL_SUB_LZERO, ABS_NEG]]); 271 272(*---------------------------------------------------------------------------*) 273(* Firstly, prove useful forms of null and bounded nets *) 274(*---------------------------------------------------------------------------*) 275 276val NET_NULL = store_thm("NET_NULL", 277 ���!g:'a->'a->bool. !x x0. 278 (x tends x0)(mtop(mr1),g) = ((\n. x(n) - x0) tends &0)(mtop(mr1),g)���, 279 REPEAT GEN_TAC THEN REWRITE_TAC[MTOP_TENDS] THEN BETA_TAC THEN 280 REWRITE_TAC[MR1_DEF, REAL_SUB_LZERO] THEN EQUAL_TAC THEN 281 REWRITE_TAC[REAL_NEG_SUB]); 282 283val NET_CONV_BOUNDED = store_thm("NET_CONV_BOUNDED", 284 ���!g:'a->'a->bool. !x x0. 285 (x tends x0)(mtop(mr1),g) ==> bounded(mr1,g) x���, 286 REPEAT GEN_TAC THEN REWRITE_TAC[MTOP_TENDS, bounded] THEN 287 DISCH_THEN(MP_TAC o SPEC ���&1���) THEN 288 REWRITE_TAC[REAL_LT, ONE, LESS_0] THEN 289 REWRITE_TAC[GSYM(ONE)] THEN 290 DISCH_THEN(X_CHOOSE_THEN ���N:'a��� STRIP_ASSUME_TAC) THEN 291 MAP_EVERY EXISTS_TAC [���&1���, ���x0:real���, ���N:'a���] THEN 292 ASM_REWRITE_TAC[]); 293 294val NET_CONV_NZ = store_thm("NET_CONV_NZ", 295 ���!g:'a->'a->bool. !x x0. 296 (x tends x0)(mtop(mr1),g) /\ ~(x0 = &0) ==> 297 ?N. g N N /\ (!n. g n N ==> ~(x n = &0))���, 298 REPEAT GEN_TAC THEN REWRITE_TAC[MTOP_TENDS, bounded] THEN 299 DISCH_THEN(CONJUNCTS_THEN2 (MP_TAC o SPEC ���abs(x0)���) ASSUME_TAC) THEN 300 ASM_REWRITE_TAC[GSYM ABS_NZ] THEN 301 DISCH_THEN(X_CHOOSE_THEN ���N:'a��� (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN 302 DISCH_TAC THEN EXISTS_TAC ���N:'a��� THEN ASM_REWRITE_TAC[] THEN 303 GEN_TAC THEN DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN 304 CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[] THEN 305 DISCH_THEN SUBST1_TAC THEN 306 REWRITE_TAC[MR1_DEF, REAL_SUB_RZERO, REAL_LT_REFL]); 307 308val NET_CONV_IBOUNDED = store_thm("NET_CONV_IBOUNDED", 309 ���!g:'a->'a->bool. !x x0. 310 (x tends x0)(mtop(mr1),g) /\ ~(x0 = &0) ==> 311 bounded(mr1,g) (\n. inv(x n))���, 312 REPEAT GEN_TAC THEN REWRITE_TAC[MTOP_TENDS, MR1_BOUNDED, MR1_DEF] THEN 313 BETA_TAC THEN REWRITE_TAC[ABS_NZ] THEN 314 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN 315 DISCH_THEN(MP_TAC o SPEC ���abs(x0) / &2���) THEN 316 ASM_REWRITE_TAC[REAL_LT_HALF1] THEN 317 DISCH_THEN(X_CHOOSE_THEN ���N:'a��� STRIP_ASSUME_TAC) THEN 318 MAP_EVERY EXISTS_TAC [���&2 / abs(x0)���, ���N:'a���] THEN 319 ASM_REWRITE_TAC[] THEN X_GEN_TAC ���n:'a��� THEN 320 DISCH_THEN(ANTE_RES_THEN ASSUME_TAC) THEN 321 SUBGOAL_THEN ���(abs(x0) / & 2) < abs(x(n:'a))��� ASSUME_TAC THENL 322 [SUBST1_TAC(SYM(SPECL [���abs(x0) / &2���, ���abs(x0) / &2���, ���abs(x(n:'a))���] 323 REAL_LT_LADD)) THEN 324 REWRITE_TAC[REAL_HALF_DOUBLE] THEN 325 MATCH_MP_TAC REAL_LET_TRANS THEN 326 EXISTS_TAC ���abs(x0 - x(n:'a)) + abs(x(n))��� THEN 327 ASM_REWRITE_TAC[REAL_LT_RADD] THEN 328 SUBST1_TAC(SYM(AP_TERM ���abs��� 329 (SPECL [���x0:real���, ���x(n:'a):real���] REAL_SUB_ADD))) THEN 330 MATCH_ACCEPT_TAC ABS_TRIANGLE, ALL_TAC] THEN 331 SUBGOAL_THEN ���&0 < abs(x(n:'a))��� ASSUME_TAC THENL 332 [MATCH_MP_TAC REAL_LT_TRANS THEN EXISTS_TAC ���abs(x0) / &2��� THEN 333 ASM_REWRITE_TAC[REAL_LT_HALF1], ALL_TAC] THEN 334 SUBGOAL_THEN ���&2 / abs(x0) = inv(abs(x0) / &2)��� SUBST1_TAC THENL 335 [MATCH_MP_TAC REAL_RINV_UNIQ THEN REWRITE_TAC[real_div] THEN 336 ONCE_REWRITE_TAC[AC(REAL_MUL_ASSOC,REAL_MUL_SYM) 337 ���(a * b) * (c * d) = (d * a) * (b * c)���] THEN 338 SUBGOAL_THEN ���~(abs(x0) = &0) /\ ~(&2 = &0)��� 339 (fn th => CONJUNCTS_THEN(SUBST1_TAC o MATCH_MP REAL_MUL_LINV) th 340 THEN REWRITE_TAC[REAL_MUL_LID]) THEN 341 CONJ_TAC THENL 342 [ASM_REWRITE_TAC[ABS_NZ, ABS_ABS], 343 REWRITE_TAC[REAL_INJ] THEN CONV_TAC(RAND_CONV num_EQ_CONV) THEN 344 REWRITE_TAC[]], ALL_TAC] THEN 345 SUBGOAL_THEN ���~(x(n:'a) = &0)��� (SUBST1_TAC o MATCH_MP ABS_INV) THENL 346 [ASM_REWRITE_TAC[ABS_NZ], ALL_TAC] THEN 347 MATCH_MP_TAC REAL_LT_INV THEN ASM_REWRITE_TAC[REAL_LT_HALF1]); 348 349(*---------------------------------------------------------------------------*) 350(* Now combining theorems for null nets *) 351(*---------------------------------------------------------------------------*) 352 353val NET_NULL_ADD = store_thm("NET_NULL_ADD", 354 ���!g:'a->'a->bool. dorder g ==> 355 !x y. (x tends &0)(mtop(mr1),g) /\ (y tends &0)(mtop(mr1),g) ==> 356 ((\n. x(n) + y(n)) tends &0)(mtop(mr1),g)���, 357 GEN_TAC THEN DISCH_TAC THEN REPEAT GEN_TAC THEN 358 REWRITE_TAC[MTOP_TENDS, MR1_DEF, REAL_SUB_LZERO, ABS_NEG] THEN 359 DISCH_THEN(curry op THEN (X_GEN_TAC ���e:real��� THEN DISCH_TAC) o 360 MP_TAC o end_itlist CONJ o map (SPEC ���e / &2���) o CONJUNCTS) THEN 361 ASM_REWRITE_TAC[REAL_LT_HALF1] THEN 362 DISCH_THEN(DORDER_THEN (X_CHOOSE_THEN ���N:'a��� STRIP_ASSUME_TAC)) THEN 363 EXISTS_TAC ���N:'a��� THEN ASM_REWRITE_TAC[] THEN 364 GEN_TAC THEN DISCH_THEN(ANTE_RES_THEN ASSUME_TAC) THEN 365 BETA_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN 366 EXISTS_TAC ���abs(x(m:'a)) + abs(y(m:'a))��� THEN 367 REWRITE_TAC[ABS_TRIANGLE] THEN RULE_ASSUM_TAC BETA_RULE THEN 368 GEN_REWR_TAC RAND_CONV [GSYM REAL_HALF_DOUBLE] THEN 369 MATCH_MP_TAC REAL_LT_ADD2 THEN ASM_REWRITE_TAC[]); 370 371val NET_NULL_MUL = store_thm("NET_NULL_MUL", 372 ���!g:'a->'a->bool. dorder g ==> 373 !x y. bounded(mr1,g) x /\ (y tends &0)(mtop(mr1),g) ==> 374 ((\n. x(n) * y(n)) tends &0)(mtop(mr1),g)���, 375 GEN_TAC THEN DISCH_TAC THEN 376 REPEAT GEN_TAC THEN REWRITE_TAC[MR1_BOUNDED] THEN 377 REWRITE_TAC[MTOP_TENDS, MR1_DEF, REAL_SUB_LZERO, ABS_NEG] THEN 378 DISCH_THEN(curry op THEN (X_GEN_TAC ���e:real��� THEN DISCH_TAC) o MP_TAC) THEN 379 CONV_TAC(LAND_CONV LEFT_AND_EXISTS_CONV) THEN 380 DISCH_THEN(X_CHOOSE_THEN ���k:real��� MP_TAC) THEN 381 DISCH_THEN(ASSUME_TAC o uncurry CONJ o (I ## SPEC ���e / k���) o CONJ_PAIR) THEN 382 SUBGOAL_THEN ���&0 < k��� ASSUME_TAC THENL 383 [FIRST_ASSUM(X_CHOOSE_THEN ���N:'a��� 384 (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) o CONJUNCT1) THEN 385 DISCH_THEN(MP_TAC o SPEC ���N:'a���) THEN ASM_REWRITE_TAC[] THEN 386 DISCH_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN 387 EXISTS_TAC ���abs(x(N:'a))��� THEN ASM_REWRITE_TAC[ABS_POS], ALL_TAC] THEN 388 FIRST_ASSUM(UNDISCH_TAC o assert is_conj o concl) THEN 389 SUBGOAL_THEN ���&0 < e / k��� ASSUME_TAC THENL 390 [FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP REAL_LT_RDIV_0 th] THEN 391 ASM_REWRITE_TAC[] THEN NO_TAC), ALL_TAC] THEN ASM_REWRITE_TAC[] THEN 392 DISCH_THEN(DORDER_THEN(X_CHOOSE_THEN ���N:'a��� STRIP_ASSUME_TAC)) THEN 393 EXISTS_TAC ���N:'a��� THEN ASM_REWRITE_TAC[] THEN 394 GEN_TAC THEN DISCH_THEN(ANTE_RES_THEN (ASSUME_TAC o BETA_RULE)) THEN 395 SUBGOAL_THEN ���e = k * (e / k)��� SUBST1_TAC THENL 396 [CONV_TAC SYM_CONV THEN MATCH_MP_TAC REAL_DIV_LMUL THEN 397 DISCH_THEN SUBST_ALL_TAC THEN UNDISCH_TAC ���&0 < &0��� THEN 398 REWRITE_TAC[REAL_LT_REFL], ALL_TAC] THEN BETA_TAC THEN 399 REWRITE_TAC[ABS_MUL] THEN MATCH_MP_TAC REAL_LT_MUL2 THEN 400 ASM_REWRITE_TAC[ABS_POS]); 401 402val NET_NULL_CMUL = store_thm("NET_NULL_CMUL", 403 ���!g:'a->'a->bool. !k x. 404 (x tends &0)(mtop(mr1),g) ==> ((\n. k * x(n)) tends &0)(mtop(mr1),g)���, 405 REPEAT GEN_TAC THEN REWRITE_TAC[MTOP_TENDS, MR1_DEF] THEN 406 BETA_TAC THEN REWRITE_TAC[REAL_SUB_LZERO, ABS_NEG] THEN 407 DISCH_THEN(curry op THEN (X_GEN_TAC ���e:real��� THEN DISCH_TAC) o MP_TAC) THEN 408 ASM_CASES_TAC ���k = &0��� THENL 409 [DISCH_THEN(MP_TAC o SPEC ���&1���) THEN 410 REWRITE_TAC[REAL_LT, ONE, LESS_SUC_REFL] THEN 411 DISCH_THEN(X_CHOOSE_THEN ���N:'a��� STRIP_ASSUME_TAC) THEN 412 EXISTS_TAC ���N:'a��� THEN 413 ASM_REWRITE_TAC[REAL_MUL_LZERO, abs, REAL_LE_REFL], 414 DISCH_THEN(MP_TAC o SPEC ���e / abs(k)���) THEN 415 SUBGOAL_THEN ���&0 < e / abs(k)��� ASSUME_TAC THENL 416 [REWRITE_TAC[real_div] THEN MATCH_MP_TAC REAL_LT_MUL THEN 417 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_INV_POS THEN 418 ASM_REWRITE_TAC[GSYM ABS_NZ], ALL_TAC] THEN 419 ASM_REWRITE_TAC[] THEN 420 DISCH_THEN(X_CHOOSE_THEN ���N:'a��� STRIP_ASSUME_TAC) THEN 421 EXISTS_TAC ���N:'a��� THEN ASM_REWRITE_TAC[] THEN 422 GEN_TAC THEN DISCH_THEN(ANTE_RES_THEN ASSUME_TAC) THEN 423 SUBGOAL_THEN ���e = abs(k) * (e / abs(k))��� SUBST1_TAC THENL 424 [CONV_TAC SYM_CONV THEN MATCH_MP_TAC REAL_DIV_LMUL THEN 425 ASM_REWRITE_TAC[ABS_ZERO], ALL_TAC] THEN 426 REWRITE_TAC[ABS_MUL] THEN 427 SUBGOAL_THEN ���&0 < abs k��� (fn th => REWRITE_TAC[MATCH_MP REAL_LT_LMUL th]) 428 THEN ASM_REWRITE_TAC[GSYM ABS_NZ]]); 429 430(*---------------------------------------------------------------------------*) 431(* Now real arithmetic theorems for convergent nets *) 432(*---------------------------------------------------------------------------*) 433 434val NET_ADD = store_thm("NET_ADD", 435 ���!g:'a->'a->bool. dorder g ==> 436 !x x0 y y0. (x tends x0)(mtop(mr1),g) /\ (y tends y0)(mtop(mr1),g) ==> 437 ((\n. x(n) + y(n)) tends (x0 + y0))(mtop(mr1),g)���, 438 REPEAT GEN_TAC THEN DISCH_TAC THEN REPEAT GEN_TAC THEN 439 ONCE_REWRITE_TAC[NET_NULL] THEN 440 DISCH_THEN(fn th => FIRST_ASSUM(MP_TAC o C MATCH_MP th o MATCH_MP NET_NULL_ADD)) 441 THEN MATCH_MP_TAC(TAUT_CONV ���(a = b) ==> a ==> b���) THEN EQUAL_TAC THEN 442 BETA_TAC THEN REWRITE_TAC[real_sub, REAL_NEG_ADD] THEN 443 CONV_TAC(AC_CONV(REAL_ADD_ASSOC,REAL_ADD_SYM))); 444 445val NET_NEG = store_thm("NET_NEG", 446 ���!g:'a->'a->bool. dorder g ==> 447 (!x x0. (x tends x0)(mtop(mr1),g) = 448 ((\n. ~(x n)) tends ~x0)(mtop(mr1),g))���, 449 GEN_TAC THEN DISCH_TAC THEN REPEAT GEN_TAC THEN 450 REWRITE_TAC[MTOP_TENDS, MR1_DEF] THEN BETA_TAC THEN 451 REWRITE_TAC[REAL_SUB_NEG2] THEN 452 GEN_REWR_TAC (RAND_CONV o ONCE_DEPTH_CONV) [ABS_SUB] 453 THEN REFL_TAC); 454 455val NET_SUB = store_thm("NET_SUB", 456 ���!g:'a->'a->bool. dorder g ==> 457 !x x0 y y0. (x tends x0)(mtop(mr1),g) /\ (y tends y0)(mtop(mr1),g) ==> 458 ((\n. x(n) - y(n)) tends (x0 - y0))(mtop(mr1),g)���, 459 GEN_TAC THEN DISCH_TAC THEN REPEAT GEN_TAC THEN DISCH_TAC THEN 460 REWRITE_TAC[real_sub] THEN 461 CONV_TAC(EXACT_CONV[X_BETA_CONV ���n:'a��� ���-(y (n:'a))���]) THEN 462 FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP NET_ADD) THEN 463 ASM_REWRITE_TAC[] THEN 464 FIRST_ASSUM(fn th => ONCE_REWRITE_TAC[GSYM(MATCH_MP NET_NEG th)]) THEN 465 ASM_REWRITE_TAC[]); 466 467val NET_MUL = store_thm("NET_MUL", 468 ���!g:'a->'a->bool. dorder g ==> 469 !x y x0 y0. (x tends x0)(mtop(mr1),g) /\ (y tends y0)(mtop(mr1),g) ==> 470 ((\n. x(n) * y(n)) tends (x0 * y0))(mtop(mr1),g)���, 471 REPEAT GEN_TAC THEN DISCH_TAC THEN 472 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[NET_NULL] THEN 473 DISCH_TAC THEN BETA_TAC THEN 474 SUBGOAL_THEN ���!a b c d. (a * b) - (c * d) = 475 (a * (b - d)) + ((a - c) * d)��� 476 (fn th => ONCE_REWRITE_TAC[th]) THENL 477 [REPEAT GEN_TAC THEN 478 REWRITE_TAC[real_sub, REAL_LDISTRIB, REAL_RDISTRIB, GSYM REAL_ADD_ASSOC] 479 THEN AP_TERM_TAC THEN 480 REWRITE_TAC[GSYM REAL_NEG_LMUL, GSYM REAL_NEG_RMUL] THEN 481 REWRITE_TAC[REAL_ADD_ASSOC, REAL_ADD_LINV, REAL_ADD_LID], ALL_TAC] THEN 482 CONV_TAC(EXACT_CONV[X_BETA_CONV ���n:'a��� ���x(n:'a) * (y(n) - y0)���]) THEN 483 CONV_TAC(EXACT_CONV[X_BETA_CONV ���n:'a��� ���(x(n:'a) - x0) * y0���]) THEN 484 FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP NET_NULL_ADD) THEN 485 GEN_REWR_TAC (RAND_CONV o ONCE_DEPTH_CONV) [REAL_MUL_SYM] THEN 486 (CONV_TAC o EXACT_CONV o map (X_BETA_CONV ���n:'a���)) 487 [���y(n:'a) - y0���, ���x(n:'a) - x0���] THEN 488 CONJ_TAC THENL 489 [FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP NET_NULL_MUL) THEN 490 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC NET_CONV_BOUNDED THEN 491 EXISTS_TAC ���x0:real��� THEN ONCE_REWRITE_TAC[NET_NULL] THEN 492 ASM_REWRITE_TAC[], 493 MATCH_MP_TAC NET_NULL_CMUL THEN ASM_REWRITE_TAC[]]); 494 495val NET_INV = store_thm("NET_INV", 496 ���!g:'a->'a->bool. dorder g ==> 497 !x x0. (x tends x0)(mtop(mr1),g) /\ ~(x0 = &0) ==> 498 ((\n. inv(x(n))) tends inv x0)(mtop(mr1),g)���, 499 GEN_TAC THEN DISCH_TAC THEN REPEAT GEN_TAC THEN 500 DISCH_THEN(fn th => STRIP_ASSUME_TAC th THEN 501 MP_TAC(CONJ (MATCH_MP NET_CONV_IBOUNDED th) 502 (MATCH_MP NET_CONV_NZ th))) THEN 503 REWRITE_TAC[MR1_BOUNDED] THEN 504 CONV_TAC(ONCE_DEPTH_CONV LEFT_AND_EXISTS_CONV) THEN 505 DISCH_THEN(X_CHOOSE_THEN ���k:real��� MP_TAC) THEN 506 DISCH_THEN(DORDER_THEN MP_TAC) THEN BETA_TAC THEN 507 DISCH_THEN(MP_TAC o C CONJ(ASSUME ���(x tends x0)(mtop mr1,(g:'a->'a->bool))���)) THEN 508 ONCE_REWRITE_TAC[NET_NULL] THEN 509 REWRITE_TAC[MTOP_TENDS, MR1_DEF, REAL_SUB_LZERO, ABS_NEG] THEN BETA_TAC 510 THEN DISCH_THEN(curry op THEN (X_GEN_TAC ���e:real��� THEN DISCH_TAC) o MP_TAC) THEN 511 CONV_TAC(ONCE_DEPTH_CONV RIGHT_AND_FORALL_CONV) THEN 512 DISCH_THEN(ASSUME_TAC o SPEC ���e * (abs(x0) * (inv k))���) THEN 513 SUBGOAL_THEN ���&0 < k��� ASSUME_TAC THENL 514 [FIRST_ASSUM(MP_TAC o CONJUNCT1) THEN 515 DISCH_THEN(X_CHOOSE_THEN ���N:'a��� (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN 516 DISCH_THEN(MP_TAC o SPEC ���N:'a���) THEN ASM_REWRITE_TAC[] THEN 517 DISCH_THEN(ASSUME_TAC o CONJUNCT1) THEN 518 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC ���abs(inv(x(N:'a)))��� THEN 519 ASM_REWRITE_TAC[ABS_POS], ALL_TAC] THEN 520 SUBGOAL_THEN ���&0 < e * (abs(x0) * inv k)��� ASSUME_TAC THENL 521 [REPEAT(MATCH_MP_TAC REAL_LT_MUL THEN CONJ_TAC) THEN 522 ASM_REWRITE_TAC[GSYM ABS_NZ] THEN 523 MATCH_MP_TAC REAL_INV_POS THEN ASM_REWRITE_TAC[], ALL_TAC] THEN 524 FIRST_ASSUM(UNDISCH_TAC o assert is_conj o concl) THEN 525 ASM_REWRITE_TAC[] THEN DISCH_THEN(DORDER_THEN MP_TAC) THEN 526 DISCH_THEN(X_CHOOSE_THEN ���N:'a��� (CONJUNCTS_THEN ASSUME_TAC)) THEN 527 EXISTS_TAC ���N:'a��� THEN ASM_REWRITE_TAC[] THEN 528 X_GEN_TAC ���n:'a��� THEN DISCH_THEN(ANTE_RES_THEN STRIP_ASSUME_TAC) THEN 529 RULE_ASSUM_TAC BETA_RULE THEN POP_ASSUM_LIST(MAP_EVERY STRIP_ASSUME_TAC) THEN 530 SUBGOAL_THEN ���inv(x n) - inv x0 = 531 inv(x n) * (inv x0 * (x0 - x(n:'a)))��� SUBST1_TAC THENL 532 [REWRITE_TAC[REAL_SUB_LDISTRIB] THEN 533 REWRITE_TAC[MATCH_MP REAL_MUL_LINV (ASSUME ���~(x0 = &0)���)] THEN 534 REWRITE_TAC[REAL_MUL_RID] THEN REPEAT AP_TERM_TAC THEN 535 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN 536 REWRITE_TAC[MATCH_MP REAL_MUL_RINV (ASSUME ���~(x(n:'a) = &0)���)] THEN 537 REWRITE_TAC[REAL_MUL_RID], ALL_TAC] THEN 538 REWRITE_TAC[ABS_MUL] THEN ONCE_REWRITE_TAC[ABS_SUB] THEN 539 SUBGOAL_THEN ���e = e * ((abs(inv x0) * abs(x0)) * (inv k * k))��� 540 SUBST1_TAC THENL 541 [REWRITE_TAC[GSYM ABS_MUL] THEN 542 REWRITE_TAC[MATCH_MP REAL_MUL_LINV (ASSUME ���~(x0 = &0)���)] THEN 543 REWRITE_TAC[MATCH_MP REAL_MUL_LINV 544 (GSYM(MATCH_MP REAL_LT_IMP_NE (ASSUME ���&0 < k���)))] THEN 545 REWRITE_TAC[REAL_MUL_RID] THEN 546 REWRITE_TAC[abs, REAL_LE, LESS_OR_EQ, ONE, LESS_SUC_REFL] THEN 547 REWRITE_TAC[SYM ONE, REAL_MUL_RID], ALL_TAC] THEN 548 ONCE_REWRITE_TAC[AC(REAL_MUL_ASSOC,REAL_MUL_SYM) 549 ���a * ((b * c) * (d * e)) = e * (b * (a * (c * d)))���] THEN 550 REWRITE_TAC[GSYM ABS_MUL] THEN 551 MATCH_MP_TAC ABS_LT_MUL2 THEN ASM_REWRITE_TAC[] THEN 552 REWRITE_TAC[ABS_MUL] THEN SUBGOAL_THEN ���&0 < abs(inv x0)��� 553 (fn th => ASM_REWRITE_TAC[MATCH_MP REAL_LT_LMUL th]) THEN 554 REWRITE_TAC[GSYM ABS_NZ] THEN 555 MATCH_MP_TAC REAL_INV_NZ THEN ASM_REWRITE_TAC[]); 556 557val NET_DIV = store_thm("NET_DIV", 558 ���!g:'a->'a->bool. dorder g ==> 559 !x x0 y y0. (x tends x0)(mtop(mr1),g) /\ 560 (y tends y0)(mtop(mr1),g) /\ ~(y0 = &0) ==> 561 ((\n. x(n) / y(n)) tends (x0 / y0))(mtop(mr1),g)���, 562 GEN_TAC THEN DISCH_TAC THEN REPEAT GEN_TAC THEN DISCH_TAC THEN 563 REWRITE_TAC[real_div] THEN 564 CONV_TAC(EXACT_CONV[X_BETA_CONV ���n:'a��� ���inv(y(n:'a))���]) THEN 565 FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP NET_MUL) THEN 566 ASM_REWRITE_TAC[] THEN 567 FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP NET_INV) THEN 568 ASM_REWRITE_TAC[]); 569 570val NET_ABS = store_thm("NET_ABS", 571 ���!g x x0. (x tends x0)(mtop(mr1),g) ==> 572 ((\n:'a. abs(x n)) tends abs(x0))(mtop(mr1),g)���, 573 REPEAT GEN_TAC THEN REWRITE_TAC[MTOP_TENDS] THEN 574 DISCH_TAC THEN X_GEN_TAC ���e:real��� THEN 575 DISCH_THEN(fn th => POP_ASSUM(MP_TAC o C MATCH_MP th)) THEN 576 DISCH_THEN(X_CHOOSE_THEN ���N:'a��� STRIP_ASSUME_TAC) THEN 577 EXISTS_TAC ���N:'a��� THEN ASM_REWRITE_TAC[] THEN 578 X_GEN_TAC ���n:'a��� THEN DISCH_TAC THEN BETA_TAC THEN 579 MATCH_MP_TAC REAL_LET_TRANS THEN 580 EXISTS_TAC ���dist(mr1)(x(n:'a),x0)��� THEN CONJ_TAC THENL 581 [REWRITE_TAC[MR1_DEF, ABS_SUB_ABS], 582 FIRST_ASSUM MATCH_MP_TAC THEN FIRST_ASSUM ACCEPT_TAC]); 583 584(*---------------------------------------------------------------------------*) 585(* Comparison between limits *) 586(*---------------------------------------------------------------------------*) 587 588val NET_LE = store_thm("NET_LE", 589 ���!g:'a->'a->bool. dorder g ==> 590 !x x0 y y0. (x tends x0)(mtop(mr1),g) /\ 591 (y tends y0)(mtop(mr1),g) /\ 592 (?N. g N N /\ !n. g n N ==> x(n) <= y(n)) 593 ==> x0 <= y0���, 594 GEN_TAC THEN DISCH_TAC THEN REPEAT GEN_TAC THEN DISCH_TAC THEN 595 GEN_REWR_TAC I [TAUT_CONV ���a = ~~a:bool���] THEN 596 PURE_ONCE_REWRITE_TAC[REAL_NOT_LE] THEN 597 ONCE_REWRITE_TAC[GSYM REAL_SUB_LT] THEN DISCH_TAC THEN 598 FIRST_ASSUM(UNDISCH_TAC o assert is_conj o concl) THEN 599 REWRITE_TAC[CONJ_ASSOC] THEN 600 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN 601 REWRITE_TAC[MTOP_TENDS] THEN 602 DISCH_THEN(MP_TAC o end_itlist CONJ o 603 map (SPEC ���(x0 - y0) / &2���) o CONJUNCTS) THEN 604 ASM_REWRITE_TAC[REAL_LT_HALF1] THEN 605 DISCH_THEN(DORDER_THEN MP_TAC) THEN 606 FIRST_ASSUM(UNDISCH_TAC o assert is_exists o concl) THEN 607 DISCH_THEN(fn th1 => DISCH_THEN (fn th2 => MP_TAC(CONJ th1 th2))) THEN 608 DISCH_THEN(DORDER_THEN MP_TAC) THEN 609 DISCH_THEN(X_CHOOSE_THEN ���N:'a��� (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN 610 BETA_TAC THEN DISCH_THEN(MP_TAC o SPEC ���N:'a���) THEN ASM_REWRITE_TAC[] THEN 611 REWRITE_TAC[MR1_DEF] THEN ONCE_REWRITE_TAC[ABS_SUB] THEN 612 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN 613 REWRITE_TAC[REAL_NOT_LE] THEN MATCH_MP_TAC ABS_BETWEEN2 THEN 614 MAP_EVERY EXISTS_TAC [���y0:real���, ���x0:real���] THEN 615 ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[GSYM REAL_SUB_LT] THEN 616 FIRST_ASSUM ACCEPT_TAC); 617 618val _ = export_theory(); 619