netsScript.sml
1(*===========================================================================*)
2(* Theory of Moore-Smith convergence nets, and special cases like sequences *)
3(*===========================================================================*)
4
5Theory nets
6Ancestors
7 pred_set pair combin arithmetic num prim_rec relation real topology
8 metric cardinal
9Libs
10 numLib reduceLib pairLib mesonLib realLib hurdUtils jrhUtils tautLib
11
12val _ = Parse.reveal "B";
13
14val NUM_EQ_CONV = Arithconv.NEQ_CONV;
15val DISC_RW_KILL = DISCH_TAC THEN ONCE_ASM_REWRITE_TAC [] THEN
16 POP_ASSUM K_TAC;
17
18val ASM_REAL_ARITH_TAC = REAL_ASM_ARITH_TAC;
19
20(* !x. P x ==> Q x) ==> (!x. P x) ==> !x. Q x *)
21Theorem MONO_FORALL = MONO_ALL
22
23Theorem REAL_HALF :
24 (!e. &0 < e / &2 <=> &0 < e) /\
25 (!e. e / &2 + e / &2 = e) /\
26 (!e. &2 * (e / &2) = e)
27Proof
28 REAL_ARITH_TAC
29QED
30
31(*---------------------------------------------------------------------------*)
32(* Basic definitions: directed order, net, bounded net, pointwise limit [1] *)
33(*---------------------------------------------------------------------------*)
34
35(* NOTE: According to [1], the property ‘!w. g w z ==> g w x /\ g w y’ is called
36 "composition property".
37 *)
38Definition dorder :
39 dorder (g:'a->'a->bool) =
40 !x y. g x x /\ g y y ==> ?z. g z z /\ (!w. g w z ==> g w x /\ g w y)
41End
42
43val _ = set_fixity "tends" (Infixr 750);
44
45(* A general function (s :'b -> 'a) tends to l (w.r.t. top and g) if for all
46 neigh N of l, "eventually" g(m) IN N.
47 *)
48Definition tends :
49 (s tends l) (top,g) =
50 !N:'a->bool. neigh(top)(N,l) ==>
51 ?n:'b. g n n /\ !m:'b. g m n ==> N(s m)
52End
53
54Definition bounded :
55 bounded(m:('a)metric,(g:'b->'b->bool)) f =
56 ?k x N. g N N /\ (!n. g n N ==> (dist m)(f(n),x) < k)
57End
58
59(* ‘tendsto (m,x)’ is a dorder defined on a metric. See also DORDER_TENDSTO.
60
61 NOTE: The net ‘at’ is defined by ‘tendsto’.
62 *)
63Definition tendsto :
64 tendsto(m:('a)metric,x) y z =
65 (&0 < (dist m)(x,y) /\ (dist m)(x,y) <= (dist m)(x,z))
66End
67
68Theorem DORDER_LEMMA:
69 !g:'a->'a->bool.
70 dorder g ==>
71 !P Q. (?n. g n n /\ (!m. g m n ==> P m)) /\
72 (?n. g n n /\ (!m. g m n ==> Q m))
73 ==> (?n. g n n /\ (!m. g m n ==> P m /\ Q m))
74Proof
75 GEN_TAC THEN REWRITE_TAC[dorder] THEN DISCH_TAC THEN REPEAT GEN_TAC THEN
76 DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_THEN “N1:'a” STRIP_ASSUME_TAC)
77 (X_CHOOSE_THEN “N2:'a” STRIP_ASSUME_TAC)) THEN
78 FIRST_ASSUM(MP_TAC o SPECL [“N1:'a”, “N2:'a”]) THEN
79 REWRITE_TAC[ASSUME “(g:'a->'a->bool) N1 N1”,ASSUME “(g:'a->'a->bool) N2 N2”] THEN
80 DISCH_THEN(X_CHOOSE_THEN “n:'a” STRIP_ASSUME_TAC) THEN
81 EXISTS_TAC “n:'a” THEN ASM_REWRITE_TAC[] THEN
82 X_GEN_TAC “m:'a” THEN DISCH_TAC THEN
83 CONJ_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
84 FIRST_ASSUM(UNDISCH_TAC o
85 assert(is_conj o snd o dest_imp o snd o dest_forall) o concl) THEN
86 DISCH_THEN(MP_TAC o SPEC “m:'a”) THEN ASM_REWRITE_TAC[] THEN
87 DISCH_TAC THEN ASM_REWRITE_TAC[]
88QED
89
90(*---------------------------------------------------------------------------*)
91(* Following tactic is useful in the following proofs *)
92(*---------------------------------------------------------------------------*)
93
94fun DORDER_THEN tac th =
95 let val findpr = snd o dest_imp o body o rand o rand o body o rand
96 val (t1,t2) = case map (rand o rand o body o rand)
97 (strip_conj (concl th)) of
98 [t1, t2] => (t1, t2)
99 | _ => raise Match
100 val dog = (rator o rator o rand o rator o body) t1
101 val thl = map ((uncurry X_BETA_CONV) o (I ## rand) o dest_abs) [t1,t2]
102 val th1 = CONV_RULE(EXACT_CONV thl) th
103 val th2 = MATCH_MP DORDER_LEMMA (ASSUME “dorder ^dog”)
104 val th3 = MATCH_MP th2 th1
105 val th4 = CONV_RULE(EXACT_CONV(map SYM thl)) th3 in
106 tac th4 end;
107
108(*---------------------------------------------------------------------------*)
109(* Show that sequences and pointwise limits in a metric space are directed *)
110(*---------------------------------------------------------------------------*)
111
112Theorem DORDER_NGE:
113 dorder ($>= :num->num->bool)
114Proof
115 REWRITE_TAC[dorder, GREATER_EQ, LESS_EQ_REFL] THEN
116 REPEAT GEN_TAC THEN
117 DISJ_CASES_TAC(SPECL [“x:num”, “y:num”] LESS_EQ_CASES) THENL
118 [EXISTS_TAC “y:num”, EXISTS_TAC “x:num”] THEN
119 GEN_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
120 MATCH_MP_TAC LESS_EQ_TRANS THENL
121 [EXISTS_TAC “y:num”, EXISTS_TAC “x:num”] THEN
122 ASM_REWRITE_TAC[]
123QED
124
125Theorem DORDER_TENDSTO:
126 !m:('a)metric. !x. dorder(tendsto(m,x))
127Proof
128 REPEAT GEN_TAC THEN REWRITE_TAC[dorder, tendsto] THEN
129 MAP_EVERY X_GEN_TAC [“u:'a”, “v:'a”] THEN
130 REWRITE_TAC[REAL_LE_REFL] THEN
131 DISCH_THEN STRIP_ASSUME_TAC THEN ASM_REWRITE_TAC[] THEN
132 DISJ_CASES_TAC(SPECL [“(dist m)(x:'a,v)”, “(dist m)(x:'a,u)”] REAL_LE_TOTAL)
133 THENL [EXISTS_TAC “v:'a”, EXISTS_TAC “u:'a”] THEN ASM_REWRITE_TAC[] THEN
134 GEN_TAC THEN DISCH_THEN STRIP_ASSUME_TAC THEN ASM_REWRITE_TAC[] THEN
135 MATCH_MP_TAC REAL_LE_TRANS THEN FIRST_ASSUM
136 (fn th => (EXISTS_TAC o rand o concl) th THEN ASM_REWRITE_TAC[] THEN NO_TAC)
137QED
138
139(*---------------------------------------------------------------------------*)
140(* Simpler characterization of limit in a metric topology *)
141(*---------------------------------------------------------------------------*)
142
143Theorem MTOP_TENDS :
144 !d g. !x:'b->'a. !x0. (x tends x0)(mtop(d),g) <=>
145 !e. &0 < e ==> ?n. g n n /\ !m. g m n ==> dist(d)(x(m),x0) < e
146Proof
147 REPEAT GEN_TAC THEN REWRITE_TAC[tends] THEN EQ_TAC THEN DISCH_TAC THENL
148 [GEN_TAC THEN DISCH_TAC THEN
149 FIRST_ASSUM(MP_TAC o SPEC “B(d)(x0:'a,e)”) THEN
150 W(C SUBGOAL_THEN MP_TAC o funpow 2 (rand o rator) o snd) THENL
151 [MATCH_MP_TAC BALL_NEIGH THEN ASM_REWRITE_TAC[], ALL_TAC] THEN
152 DISCH_THEN(fn th => REWRITE_TAC[th]) THEN REWRITE_TAC[ball] THEN
153 BETA_TAC THEN
154 GEN_REWR_TAC (RAND_CONV o ONCE_DEPTH_CONV) [METRIC_SYM] THEN REWRITE_TAC[],
155 GEN_TAC THEN REWRITE_TAC[neigh] THEN
156 DISCH_THEN(X_CHOOSE_THEN “P:'a->bool” STRIP_ASSUME_TAC) THEN
157 UNDISCH_TAC “open_in(mtop(d)) (P:'a->bool)” THEN
158 REWRITE_TAC[MTOP_OPEN] THEN DISCH_THEN(MP_TAC o SPEC “x0:'a”) THEN
159 ASM_REWRITE_TAC[] THEN
160 DISCH_THEN(X_CHOOSE_THEN “d:real” STRIP_ASSUME_TAC) THEN
161 FIRST_ASSUM(MP_TAC o SPEC “d:real”) THEN
162 REWRITE_TAC[ASSUME “&0 < d”] THEN
163 DISCH_THEN(X_CHOOSE_THEN “n:'b” STRIP_ASSUME_TAC) THEN
164 EXISTS_TAC “n:'b” THEN ASM_REWRITE_TAC[] THEN
165 GEN_TAC THEN DISCH_TAC THEN
166 UNDISCH_TAC “(P:'a->bool) SUBSET N” THEN
167 REWRITE_TAC[SUBSET_applied] THEN DISCH_TAC THEN
168 REPEAT(FIRST_ASSUM MATCH_MP_TAC) THEN
169 ONCE_REWRITE_TAC[METRIC_SYM] THEN
170 FIRST_ASSUM MATCH_MP_TAC THEN FIRST_ASSUM ACCEPT_TAC]
171QED
172
173(*---------------------------------------------------------------------------*)
174(* Prove that a net in a metric topology cannot converge to different limits *)
175(*---------------------------------------------------------------------------*)
176
177Theorem MTOP_TENDS_UNIQ :
178 !g d. dorder (g:'b->'b->bool) ==>
179 (x tends x0)(mtop(d),g) /\ (x tends x1)(mtop(d),g) ==> (x0:'a = x1)
180Proof
181 REPEAT GEN_TAC THEN DISCH_TAC THEN
182 REWRITE_TAC[MTOP_TENDS] THEN
183 CONV_TAC(ONCE_DEPTH_CONV AND_FORALL_CONV) THEN
184 REWRITE_TAC[TAUT ‘(a ==> b) /\ (a ==> c) <=> a ==> b /\ c’] THEN
185 CONV_TAC CONTRAPOS_CONV THEN DISCH_TAC THEN
186 CONV_TAC NOT_FORALL_CONV THEN
187 EXISTS_TAC “dist(d:('a)metric)(x0,x1) / &2” THEN
188 W(C SUBGOAL_THEN ASSUME_TAC o rand o rator o rand o snd) THENL
189 [REWRITE_TAC[REAL_LT_HALF1] THEN MATCH_MP_TAC METRIC_NZ THEN
190 FIRST_ASSUM ACCEPT_TAC, ALL_TAC] THEN
191 ASM_REWRITE_TAC[] THEN DISCH_THEN(DORDER_THEN MP_TAC) THEN
192 DISCH_THEN(X_CHOOSE_THEN “N:'b” (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
193 DISCH_THEN(MP_TAC o SPEC “N:'b”) THEN ASM_REWRITE_TAC[] THEN
194 BETA_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP REAL_LT_ADD2) THEN
195 REWRITE_TAC[REAL_HALF_DOUBLE, REAL_NOT_LT] THEN
196 GEN_REWR_TAC(RAND_CONV o LAND_CONV) [METRIC_SYM] THEN
197 MATCH_ACCEPT_TAC METRIC_TRIANGLE
198QED
199
200(*---------------------------------------------------------------------------*)
201(* Simpler characterization of limit of a sequence in a metric topology *)
202(*---------------------------------------------------------------------------*)
203
204val geq = Term`$>= : num->num->bool`;
205
206Theorem SEQ_TENDS:
207 !d:('a)metric. !x x0. (x tends x0)(mtop(d), ^geq) =
208 !e. &0 < e ==> ?N. !n. ^geq n N ==> dist(d)(x(n),x0) < e
209Proof
210 REPEAT GEN_TAC THEN REWRITE_TAC[MTOP_TENDS, GREATER_EQ, LESS_EQ_REFL]
211QED
212
213(*---------------------------------------------------------------------------*)
214(* And of limit of function between metric spaces *)
215(*---------------------------------------------------------------------------*)
216
217Theorem LIM_TENDS:
218 !m1:('a)metric. !m2:('b)metric. !f x0 y0.
219 limpt(mtop m1) x0 UNIV ==>
220 ((f tends y0)(mtop(m2),tendsto(m1,x0)) =
221 !e. &0 < e ==>
222 ?d. &0 < d /\ !x. &0 < (dist m1)(x,x0) /\ (dist m1)(x,x0) <= d ==>
223 (dist m2)(f(x),y0) < e)
224Proof
225 REPEAT GEN_TAC THEN DISCH_TAC THEN
226 REWRITE_TAC[MTOP_TENDS, tendsto] THEN
227 AP_TERM_TAC THEN ABS_TAC THEN
228 ASM_CASES_TAC “&0 < e” THEN ASM_REWRITE_TAC[] THEN
229 REWRITE_TAC[REAL_LE_REFL] THEN EQ_TAC THENL
230 [DISCH_THEN(X_CHOOSE_THEN “z:'a” STRIP_ASSUME_TAC) THEN
231 EXISTS_TAC “(dist m1)(x0:'a,z)” THEN ASM_REWRITE_TAC[] THEN
232 GEN_TAC THEN DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
233 ASM_REWRITE_TAC[] THEN
234 SUBST1_TAC(ISPECL [“m1:('a)metric”, “x0:'a”, “x:'a”] METRIC_SYM) THEN
235 ASM_REWRITE_TAC[],
236 DISCH_THEN(X_CHOOSE_THEN “d:real” STRIP_ASSUME_TAC) THEN
237 UNDISCH_TAC “limpt(mtop m1) (x0:'a) UNIV” THEN
238 REWRITE_TAC[MTOP_LIMPT] THEN
239 DISCH_THEN(MP_TAC o SPEC “d:real”) THEN ASM_REWRITE_TAC[] THEN
240 REWRITE_TAC[UNIV_DEF] THEN
241 DISCH_THEN(X_CHOOSE_THEN “y:'a” STRIP_ASSUME_TAC) THEN
242 EXISTS_TAC “y:'a” THEN CONJ_TAC THENL
243 [MATCH_MP_TAC METRIC_NZ THEN ASM_REWRITE_TAC[], ALL_TAC] THEN
244 X_GEN_TAC “x:'a” THEN DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
245 ONCE_REWRITE_TAC[METRIC_SYM] THEN ASM_REWRITE_TAC[] THEN
246 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC “(dist m1)(x0:'a,y)” THEN
247 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN
248 FIRST_ASSUM ACCEPT_TAC]
249QED
250
251(*---------------------------------------------------------------------------*)
252(* Similar, more conventional version, is also true at a limit point *)
253(*---------------------------------------------------------------------------*)
254
255Theorem LIM_TENDS2:
256 !m1:('a)metric. !m2:('b)metric. !f x0 y0.
257 limpt(mtop m1) x0 UNIV ==>
258 ((f tends y0)(mtop(m2),tendsto(m1,x0)) =
259 !e. &0 < e ==>
260 ?d. &0 < d /\ !x. &0 < (dist m1)(x,x0) /\ (dist m1)(x,x0) < d ==>
261 (dist m2)(f(x),y0) < e)
262Proof
263 REPEAT GEN_TAC THEN DISCH_TAC THEN
264 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP LIM_TENDS th]) THEN
265 AP_TERM_TAC THEN ABS_TAC THEN AP_TERM_TAC THEN
266 EQ_TAC THEN DISCH_THEN(X_CHOOSE_THEN “d:real” STRIP_ASSUME_TAC) THENL
267 [EXISTS_TAC “d:real” THEN ASM_REWRITE_TAC[] THEN
268 GEN_TAC THEN DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
269 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[],
270 EXISTS_TAC “d / &2” THEN ASM_REWRITE_TAC[REAL_LT_HALF1] THEN
271 GEN_TAC THEN DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
272 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LET_TRANS THEN
273 EXISTS_TAC “d / &2” THEN ASM_REWRITE_TAC[REAL_LT_HALF2]]
274QED
275
276(*---------------------------------------------------------------------------*)
277(* Simpler characterization of boundedness for the real line *)
278(*---------------------------------------------------------------------------*)
279
280Theorem MR1_BOUNDED:
281 !(g:'a->'a->bool) f. bounded(mr1,g) f =
282 ?k N. g N N /\ (!n. g n N ==> abs(f n) < k)
283Proof
284 REPEAT GEN_TAC THEN REWRITE_TAC[bounded, MR1_DEF] THEN
285 (CONV_TAC o LAND_CONV o RAND_CONV o ABS_CONV) SWAP_EXISTS_CONV
286 THEN CONV_TAC(ONCE_DEPTH_CONV SWAP_EXISTS_CONV) THEN
287 AP_TERM_TAC THEN ABS_TAC THEN
288 CONV_TAC(REDEPTH_CONV EXISTS_AND_CONV) THEN
289 AP_TERM_TAC THEN EQ_TAC THEN
290 DISCH_THEN(X_CHOOSE_THEN “k:real” MP_TAC) THENL
291 [DISCH_THEN(X_CHOOSE_TAC “x:real”) THEN
292 EXISTS_TAC “abs(x) + k” THEN GEN_TAC THEN DISCH_TAC THEN
293 SUBST1_TAC
294 (SYM(SPECL [“(f:'a->real) n”, “x:real”] REAL_SUB_ADD)) THEN
295 MATCH_MP_TAC REAL_LET_TRANS THEN
296 EXISTS_TAC “abs((f:'a->real) n - x) + abs(x)” THEN
297 REWRITE_TAC[ABS_TRIANGLE] THEN
298 GEN_REWR_TAC RAND_CONV [REAL_ADD_SYM] THEN
299 REWRITE_TAC[REAL_LT_RADD] THEN
300 ONCE_REWRITE_TAC[ABS_SUB] THEN
301 FIRST_ASSUM MATCH_MP_TAC THEN FIRST_ASSUM ACCEPT_TAC,
302 DISCH_TAC THEN MAP_EVERY EXISTS_TAC [“k:real”, “&0”] THEN
303 ASM_REWRITE_TAC[REAL_SUB_LZERO, ABS_NEG]]
304QED
305
306(*---------------------------------------------------------------------------*)
307(* Firstly, prove useful forms of null and bounded nets *)
308(*---------------------------------------------------------------------------*)
309
310Theorem NET_NULL:
311 !g:'a->'a->bool. !x x0.
312 (x tends x0)(mtop(mr1),g) = ((\n. x(n) - x0) tends &0)(mtop(mr1),g)
313Proof
314 REPEAT GEN_TAC THEN REWRITE_TAC[MTOP_TENDS] THEN BETA_TAC THEN
315 REWRITE_TAC[MR1_DEF, REAL_SUB_LZERO] THEN EQUAL_TAC THEN
316 REWRITE_TAC[REAL_NEG_SUB]
317QED
318
319Theorem NET_CONV_BOUNDED:
320 !g:'a->'a->bool. !x x0.
321 (x tends x0)(mtop(mr1),g) ==> bounded(mr1,g) x
322Proof
323 REPEAT GEN_TAC THEN REWRITE_TAC[MTOP_TENDS, bounded] THEN
324 DISCH_THEN(MP_TAC o SPEC “&1”) THEN
325 REWRITE_TAC[REAL_LT, ONE, LESS_0] THEN
326 REWRITE_TAC[GSYM(ONE)] THEN
327 DISCH_THEN(X_CHOOSE_THEN “N:'a” STRIP_ASSUME_TAC) THEN
328 MAP_EVERY EXISTS_TAC [“&1”, “x0:real”, “N:'a”] THEN
329 ASM_REWRITE_TAC[]
330QED
331
332Theorem NET_CONV_NZ:
333 !g:'a->'a->bool. !x x0.
334 (x tends x0)(mtop(mr1),g) /\ ~(x0 = &0) ==>
335 ?N. g N N /\ (!n. g n N ==> ~(x n = &0))
336Proof
337 REPEAT GEN_TAC THEN REWRITE_TAC[MTOP_TENDS, bounded] THEN
338 DISCH_THEN(CONJUNCTS_THEN2 (MP_TAC o SPEC “abs(x0)”) ASSUME_TAC) THEN
339 ASM_REWRITE_TAC[GSYM ABS_NZ] THEN
340 DISCH_THEN(X_CHOOSE_THEN “N:'a” (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
341 DISCH_TAC THEN EXISTS_TAC “N:'a” THEN ASM_REWRITE_TAC[] THEN
342 GEN_TAC THEN DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
343 CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[] THEN
344 DISCH_THEN SUBST1_TAC THEN
345 REWRITE_TAC[MR1_DEF, REAL_SUB_RZERO, REAL_LT_REFL]
346QED
347
348Theorem NET_CONV_IBOUNDED:
349 !g:'a->'a->bool. !x x0.
350 (x tends x0)(mtop(mr1),g) /\ ~(x0 = &0) ==>
351 bounded(mr1,g) (\n. inv(x n))
352Proof
353 REPEAT GEN_TAC THEN REWRITE_TAC[MTOP_TENDS, MR1_BOUNDED, MR1_DEF] THEN
354 BETA_TAC THEN REWRITE_TAC[ABS_NZ] THEN
355 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
356 DISCH_THEN(MP_TAC o SPEC “abs(x0) / &2”) THEN
357 ASM_REWRITE_TAC[REAL_LT_HALF1] THEN
358 DISCH_THEN(X_CHOOSE_THEN “N:'a” STRIP_ASSUME_TAC) THEN
359 MAP_EVERY EXISTS_TAC [“&2 / abs(x0)”, “N:'a”] THEN
360 ASM_REWRITE_TAC[] THEN X_GEN_TAC “n:'a” THEN
361 DISCH_THEN(ANTE_RES_THEN ASSUME_TAC) THEN
362 SUBGOAL_THEN “(abs(x0) / & 2) < abs(x(n:'a))” ASSUME_TAC THENL
363 [SUBST1_TAC(SYM(SPECL [“abs(x0) / &2”, “abs(x0) / &2”, “abs(x(n:'a))”]
364 REAL_LT_LADD)) THEN
365 REWRITE_TAC[REAL_HALF_DOUBLE] THEN
366 MATCH_MP_TAC REAL_LET_TRANS THEN
367 EXISTS_TAC “abs(x0 - x(n:'a)) + abs(x(n))” THEN
368 ASM_REWRITE_TAC[REAL_LT_RADD] THEN
369 SUBST1_TAC(SYM(AP_TERM “abs”
370 (SPECL [“x0:real”, “x(n:'a):real”] REAL_SUB_ADD))) THEN
371 MATCH_ACCEPT_TAC ABS_TRIANGLE, ALL_TAC] THEN
372 SUBGOAL_THEN “&0 < abs(x(n:'a))” ASSUME_TAC THENL
373 [MATCH_MP_TAC REAL_LT_TRANS THEN EXISTS_TAC “abs(x0) / &2” THEN
374 ASM_REWRITE_TAC[REAL_LT_HALF1], ALL_TAC] THEN
375 SUBGOAL_THEN “&2 / abs(x0) = inv(abs(x0) / &2)” SUBST1_TAC THENL
376 [MATCH_MP_TAC REAL_RINV_UNIQ THEN REWRITE_TAC[real_div] THEN
377 ONCE_REWRITE_TAC[AC(REAL_MUL_ASSOC,REAL_MUL_SYM)
378 “(a * b) * (c * d) = (d * a) * (b * c)”] THEN
379 SUBGOAL_THEN “~(abs(x0) = &0) /\ ~(&2 = &0)”
380 (fn th => CONJUNCTS_THEN(SUBST1_TAC o MATCH_MP REAL_MUL_LINV) th
381 THEN REWRITE_TAC[REAL_MUL_LID]) THEN
382 CONJ_TAC THENL
383 [ASM_REWRITE_TAC[ABS_NZ, ABS_ABS],
384 REWRITE_TAC[REAL_INJ] THEN CONV_TAC(RAND_CONV NUM_EQ_CONV) THEN
385 REWRITE_TAC[]], ALL_TAC] THEN
386 SUBGOAL_THEN “~(x(n:'a) = &0)” (SUBST1_TAC o MATCH_MP ABS_INV) THENL
387 [ASM_REWRITE_TAC[ABS_NZ], ALL_TAC] THEN
388 MATCH_MP_TAC REAL_LT_INV THEN ASM_REWRITE_TAC[REAL_LT_HALF1]
389QED
390
391(*---------------------------------------------------------------------------*)
392(* Now combining theorems for null nets *)
393(*---------------------------------------------------------------------------*)
394
395Theorem NET_NULL_ADD:
396 !g:'a->'a->bool. dorder g ==>
397 !x y. (x tends &0)(mtop(mr1),g) /\ (y tends &0)(mtop(mr1),g) ==>
398 ((\n. x(n) + y(n)) tends &0)(mtop(mr1),g)
399Proof
400 GEN_TAC THEN DISCH_TAC THEN REPEAT GEN_TAC THEN
401 REWRITE_TAC[MTOP_TENDS, MR1_DEF, REAL_SUB_LZERO, ABS_NEG] THEN
402 DISCH_THEN(curry op THEN (X_GEN_TAC “e:real” THEN DISCH_TAC) o
403 MP_TAC o end_itlist CONJ o map (SPEC “e / &2”) o CONJUNCTS) THEN
404 ASM_REWRITE_TAC[REAL_LT_HALF1] THEN
405 DISCH_THEN(DORDER_THEN (X_CHOOSE_THEN “N:'a” STRIP_ASSUME_TAC)) THEN
406 EXISTS_TAC “N:'a” THEN ASM_REWRITE_TAC[] THEN
407 GEN_TAC THEN DISCH_THEN(ANTE_RES_THEN ASSUME_TAC) THEN
408 BETA_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN
409 EXISTS_TAC “abs(x(m:'a)) + abs(y(m:'a))” THEN
410 REWRITE_TAC[ABS_TRIANGLE] THEN RULE_ASSUM_TAC BETA_RULE THEN
411 GEN_REWR_TAC RAND_CONV [GSYM REAL_HALF_DOUBLE] THEN
412 MATCH_MP_TAC REAL_LT_ADD2 THEN ASM_REWRITE_TAC[]
413QED
414
415Theorem NET_NULL_MUL:
416 !g:'a->'a->bool. dorder g ==>
417 !x y. bounded(mr1,g) x /\ (y tends &0)(mtop(mr1),g) ==>
418 ((\n. x(n) * y(n)) tends &0)(mtop(mr1),g)
419Proof
420 GEN_TAC THEN DISCH_TAC THEN
421 REPEAT GEN_TAC THEN REWRITE_TAC[MR1_BOUNDED] THEN
422 REWRITE_TAC[MTOP_TENDS, MR1_DEF, REAL_SUB_LZERO, ABS_NEG] THEN
423 DISCH_THEN(curry op THEN (X_GEN_TAC “e:real” THEN DISCH_TAC) o MP_TAC) THEN
424 CONV_TAC(LAND_CONV LEFT_AND_EXISTS_CONV) THEN
425 DISCH_THEN(X_CHOOSE_THEN “k:real” MP_TAC) THEN
426 DISCH_THEN(ASSUME_TAC o uncurry CONJ o (I ## SPEC “e / k”) o CONJ_PAIR) THEN
427 SUBGOAL_THEN “&0 < k” ASSUME_TAC THENL
428 [FIRST_ASSUM(X_CHOOSE_THEN “N:'a”
429 (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) o CONJUNCT1) THEN
430 DISCH_THEN(MP_TAC o SPEC “N:'a”) THEN ASM_REWRITE_TAC[] THEN
431 DISCH_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN
432 EXISTS_TAC “abs(x(N:'a))” THEN ASM_REWRITE_TAC[ABS_POS], ALL_TAC] THEN
433 FIRST_ASSUM(UNDISCH_TAC o assert is_conj o concl) THEN
434 SUBGOAL_THEN “&0 < e / k” ASSUME_TAC THENL
435 [FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP REAL_LT_RDIV_0 th] THEN
436 ASM_REWRITE_TAC[] THEN NO_TAC), ALL_TAC] THEN ASM_REWRITE_TAC[] THEN
437 DISCH_THEN(DORDER_THEN(X_CHOOSE_THEN “N:'a” STRIP_ASSUME_TAC)) THEN
438 EXISTS_TAC “N:'a” THEN ASM_REWRITE_TAC[] THEN
439 GEN_TAC THEN DISCH_THEN(ANTE_RES_THEN (ASSUME_TAC o BETA_RULE)) THEN
440 SUBGOAL_THEN “e = k * (e / k)” SUBST1_TAC THENL
441 [CONV_TAC SYM_CONV THEN MATCH_MP_TAC REAL_DIV_LMUL THEN
442 DISCH_THEN SUBST_ALL_TAC THEN UNDISCH_TAC “&0 < &0” THEN
443 REWRITE_TAC[REAL_LT_REFL], ALL_TAC] THEN BETA_TAC THEN
444 REWRITE_TAC[ABS_MUL] THEN MATCH_MP_TAC REAL_LT_MUL2 THEN
445 ASM_REWRITE_TAC[ABS_POS]
446QED
447
448Theorem NET_NULL_CMUL:
449 !g:'a->'a->bool. !k x.
450 (x tends &0)(mtop(mr1),g) ==> ((\n. k * x(n)) tends &0)(mtop(mr1),g)
451Proof
452 REPEAT GEN_TAC THEN REWRITE_TAC[MTOP_TENDS, MR1_DEF] THEN
453 BETA_TAC THEN REWRITE_TAC[REAL_SUB_LZERO, ABS_NEG] THEN
454 DISCH_THEN(curry op THEN (X_GEN_TAC “e:real” THEN DISCH_TAC) o MP_TAC) THEN
455 ASM_CASES_TAC “k = &0” THENL
456 [DISCH_THEN(MP_TAC o SPEC “&1”) THEN
457 REWRITE_TAC[REAL_LT, ONE, LESS_SUC_REFL] THEN
458 DISCH_THEN(X_CHOOSE_THEN “N:'a” STRIP_ASSUME_TAC) THEN
459 EXISTS_TAC “N:'a” THEN
460 ASM_REWRITE_TAC[REAL_MUL_LZERO, abs, REAL_LE_REFL],
461 DISCH_THEN(MP_TAC o SPEC “e / abs(k)”) THEN
462 SUBGOAL_THEN “&0 < e / abs(k)” ASSUME_TAC THENL
463 [REWRITE_TAC[real_div] THEN MATCH_MP_TAC REAL_LT_MUL THEN
464 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_INV_POS THEN
465 ASM_REWRITE_TAC[GSYM ABS_NZ], ALL_TAC] THEN
466 ASM_REWRITE_TAC[] THEN
467 DISCH_THEN(X_CHOOSE_THEN “N:'a” STRIP_ASSUME_TAC) THEN
468 EXISTS_TAC “N:'a” THEN ASM_REWRITE_TAC[] THEN
469 GEN_TAC THEN DISCH_THEN(ANTE_RES_THEN ASSUME_TAC) THEN
470 SUBGOAL_THEN “e = abs(k) * (e / abs(k))” SUBST1_TAC THENL
471 [CONV_TAC SYM_CONV THEN MATCH_MP_TAC REAL_DIV_LMUL THEN
472 ASM_REWRITE_TAC[ABS_ZERO], ALL_TAC] THEN
473 REWRITE_TAC[ABS_MUL] THEN
474 SUBGOAL_THEN “&0 < abs k” (fn th => REWRITE_TAC[MATCH_MP REAL_LT_LMUL th])
475 THEN ASM_REWRITE_TAC[GSYM ABS_NZ]]
476QED
477
478(*---------------------------------------------------------------------------*)
479(* Now real arithmetic theorems for convergent nets *)
480(*---------------------------------------------------------------------------*)
481
482Theorem NET_ADD:
483 !g:'a->'a->bool. dorder g ==>
484 !x x0 y y0. (x tends x0)(mtop(mr1),g) /\ (y tends y0)(mtop(mr1),g) ==>
485 ((\n. x(n) + y(n)) tends (x0 + y0))(mtop(mr1),g)
486Proof
487 REPEAT GEN_TAC THEN DISCH_TAC THEN REPEAT GEN_TAC THEN
488 ONCE_REWRITE_TAC[NET_NULL] THEN
489 DISCH_THEN(fn th => FIRST_ASSUM(MP_TAC o C MATCH_MP th o MATCH_MP NET_NULL_ADD))
490 THEN MATCH_MP_TAC(TAUT ‘(a = b) ==> a ==> b’) THEN EQUAL_TAC THEN
491 BETA_TAC THEN REWRITE_TAC[real_sub, REAL_NEG_ADD] THEN
492 CONV_TAC(AC_CONV(REAL_ADD_ASSOC,REAL_ADD_SYM))
493QED
494
495Theorem NET_NEG:
496 !g:'a->'a->bool. dorder g ==>
497 (!x x0. (x tends x0)(mtop(mr1),g) =
498 ((\n. ~(x n)) tends ~x0)(mtop(mr1),g))
499Proof
500 GEN_TAC THEN DISCH_TAC THEN REPEAT GEN_TAC THEN
501 REWRITE_TAC[MTOP_TENDS, MR1_DEF] THEN BETA_TAC THEN
502 REWRITE_TAC[REAL_SUB_NEG2] THEN
503 GEN_REWR_TAC (RAND_CONV o ONCE_DEPTH_CONV) [ABS_SUB]
504 THEN REFL_TAC
505QED
506
507Theorem NET_SUB:
508 !g:'a->'a->bool. dorder g ==>
509 !x x0 y y0. (x tends x0)(mtop(mr1),g) /\ (y tends y0)(mtop(mr1),g) ==>
510 ((\n. x(n) - y(n)) tends (x0 - y0))(mtop(mr1),g)
511Proof
512 GEN_TAC THEN DISCH_TAC THEN REPEAT GEN_TAC THEN DISCH_TAC THEN
513 REWRITE_TAC[real_sub] THEN
514 CONV_TAC(EXACT_CONV[X_BETA_CONV “n:'a” “-(y (n:'a))”]) THEN
515 FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP NET_ADD) THEN
516 ASM_REWRITE_TAC[] THEN
517 FIRST_ASSUM(fn th => ONCE_REWRITE_TAC[GSYM(MATCH_MP NET_NEG th)]) THEN
518 ASM_REWRITE_TAC[]
519QED
520
521Theorem NET_MUL:
522 !g:'a->'a->bool. dorder g ==>
523 !x y x0 y0. (x tends x0)(mtop(mr1),g) /\ (y tends y0)(mtop(mr1),g) ==>
524 ((\n. x(n) * y(n)) tends (x0 * y0))(mtop(mr1),g)
525Proof
526 REPEAT GEN_TAC THEN DISCH_TAC THEN
527 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[NET_NULL] THEN
528 DISCH_TAC THEN BETA_TAC THEN
529 SUBGOAL_THEN “!a b c d. (a * b) - (c * d) =
530 (a * (b - d)) + ((a - c) * d)”
531 (fn th => ONCE_REWRITE_TAC[th]) THENL
532 [REPEAT GEN_TAC THEN
533 REWRITE_TAC[real_sub, REAL_LDISTRIB, REAL_RDISTRIB, GSYM REAL_ADD_ASSOC]
534 THEN AP_TERM_TAC THEN
535 REWRITE_TAC[GSYM REAL_NEG_LMUL, GSYM REAL_NEG_RMUL] THEN
536 REWRITE_TAC[REAL_ADD_ASSOC, REAL_ADD_LINV, REAL_ADD_LID], ALL_TAC] THEN
537 CONV_TAC(EXACT_CONV[X_BETA_CONV “n:'a” “x(n:'a) * (y(n) - y0)”]) THEN
538 CONV_TAC(EXACT_CONV[X_BETA_CONV “n:'a” “(x(n:'a) - x0) * y0”]) THEN
539 FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP NET_NULL_ADD) THEN
540 GEN_REWR_TAC (RAND_CONV o ONCE_DEPTH_CONV) [REAL_MUL_SYM] THEN
541 (CONV_TAC o EXACT_CONV o map (X_BETA_CONV “n:'a”))
542 [“y(n:'a) - y0”, “x(n:'a) - x0”] THEN
543 CONJ_TAC THENL
544 [FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP NET_NULL_MUL) THEN
545 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC NET_CONV_BOUNDED THEN
546 EXISTS_TAC “x0:real” THEN ONCE_REWRITE_TAC[NET_NULL] THEN
547 ASM_REWRITE_TAC[],
548 MATCH_MP_TAC NET_NULL_CMUL THEN ASM_REWRITE_TAC[]]
549QED
550
551Theorem NET_INV:
552 !g:'a->'a->bool. dorder g ==>
553 !x x0. (x tends x0)(mtop(mr1),g) /\ ~(x0 = &0) ==>
554 ((\n. inv(x(n))) tends inv x0)(mtop(mr1),g)
555Proof
556 GEN_TAC THEN DISCH_TAC THEN REPEAT GEN_TAC THEN
557 DISCH_THEN(fn th => STRIP_ASSUME_TAC th THEN
558 MP_TAC(CONJ (MATCH_MP NET_CONV_IBOUNDED th)
559 (MATCH_MP NET_CONV_NZ th))) THEN
560 REWRITE_TAC[MR1_BOUNDED] THEN
561 CONV_TAC(ONCE_DEPTH_CONV LEFT_AND_EXISTS_CONV) THEN
562 DISCH_THEN(X_CHOOSE_THEN “k:real” MP_TAC) THEN
563 DISCH_THEN(DORDER_THEN MP_TAC) THEN BETA_TAC THEN
564 DISCH_THEN(MP_TAC o C CONJ(ASSUME “(x tends x0)(mtop mr1,(g:'a->'a->bool))”)) THEN
565 ONCE_REWRITE_TAC[NET_NULL] THEN
566 REWRITE_TAC[MTOP_TENDS, MR1_DEF, REAL_SUB_LZERO, ABS_NEG] THEN BETA_TAC
567 THEN DISCH_THEN(curry op THEN (X_GEN_TAC “e:real” THEN DISCH_TAC) o MP_TAC) THEN
568 CONV_TAC(ONCE_DEPTH_CONV RIGHT_AND_FORALL_CONV) THEN
569 DISCH_THEN(ASSUME_TAC o SPEC “e * (abs(x0) * (inv k))”) THEN
570 SUBGOAL_THEN “&0 < k” ASSUME_TAC THENL
571 [FIRST_ASSUM(MP_TAC o CONJUNCT1) THEN
572 DISCH_THEN(X_CHOOSE_THEN “N:'a” (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
573 DISCH_THEN(MP_TAC o SPEC “N:'a”) THEN ASM_REWRITE_TAC[] THEN
574 DISCH_THEN(ASSUME_TAC o CONJUNCT1) THEN
575 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC “abs(inv(x(N:'a)))” THEN
576 ASM_REWRITE_TAC[ABS_POS], ALL_TAC] THEN
577 SUBGOAL_THEN “&0 < e * (abs(x0) * inv k)” ASSUME_TAC THENL
578 [REPEAT(MATCH_MP_TAC REAL_LT_MUL THEN CONJ_TAC) THEN
579 ASM_REWRITE_TAC[GSYM ABS_NZ] THEN
580 MATCH_MP_TAC REAL_INV_POS THEN ASM_REWRITE_TAC[], ALL_TAC] THEN
581 FIRST_ASSUM(UNDISCH_TAC o assert is_conj o concl) THEN
582 ASM_REWRITE_TAC[] THEN DISCH_THEN(DORDER_THEN MP_TAC) THEN
583 DISCH_THEN(X_CHOOSE_THEN “N:'a” (CONJUNCTS_THEN ASSUME_TAC)) THEN
584 EXISTS_TAC “N:'a” THEN ASM_REWRITE_TAC[] THEN
585 X_GEN_TAC “n:'a” THEN DISCH_THEN(ANTE_RES_THEN STRIP_ASSUME_TAC) THEN
586 RULE_ASSUM_TAC BETA_RULE THEN POP_ASSUM_LIST(MAP_EVERY STRIP_ASSUME_TAC) THEN
587 SUBGOAL_THEN “inv(x n) - inv x0 =
588 inv(x n) * (inv x0 * (x0 - x(n:'a)))” SUBST1_TAC THENL
589 [REWRITE_TAC[REAL_SUB_LDISTRIB] THEN
590 REWRITE_TAC[MATCH_MP REAL_MUL_LINV (ASSUME “~(x0 = &0)”)] THEN
591 REWRITE_TAC[REAL_MUL_RID] THEN REPEAT AP_TERM_TAC THEN
592 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
593 REWRITE_TAC[MATCH_MP REAL_MUL_RINV (ASSUME “~(x(n:'a) = &0)”)] THEN
594 REWRITE_TAC[REAL_MUL_RID], ALL_TAC] THEN
595 REWRITE_TAC[ABS_MUL] THEN ONCE_REWRITE_TAC[ABS_SUB] THEN
596 SUBGOAL_THEN “e = e * ((abs(inv x0) * abs(x0)) * (inv k * k))”
597 SUBST1_TAC THENL
598 [REWRITE_TAC[GSYM ABS_MUL] THEN
599 REWRITE_TAC[MATCH_MP REAL_MUL_LINV (ASSUME “~(x0 = &0)”)] THEN
600 REWRITE_TAC[MATCH_MP REAL_MUL_LINV
601 (GSYM(MATCH_MP REAL_LT_IMP_NE (ASSUME “&0 < k”)))] THEN
602 REWRITE_TAC[REAL_MUL_RID] THEN
603 REWRITE_TAC[abs, REAL_LE, LESS_OR_EQ, ONE, LESS_SUC_REFL] THEN
604 REWRITE_TAC[SYM ONE, REAL_MUL_RID], ALL_TAC] THEN
605 ONCE_REWRITE_TAC[AC(REAL_MUL_ASSOC,REAL_MUL_SYM)
606 “a * ((b * c) * (d * e)) = e * (b * (a * (c * d)))”] THEN
607 REWRITE_TAC[GSYM ABS_MUL] THEN
608 MATCH_MP_TAC ABS_LT_MUL2 THEN ASM_REWRITE_TAC[] THEN
609 REWRITE_TAC[ABS_MUL] THEN SUBGOAL_THEN “&0 < abs(inv x0)”
610 (fn th => ASM_REWRITE_TAC[MATCH_MP REAL_LT_LMUL th]) THEN
611 REWRITE_TAC[GSYM ABS_NZ] THEN
612 MATCH_MP_TAC REAL_INV_NZ THEN ASM_REWRITE_TAC[]
613QED
614
615Theorem NET_DIV:
616 !g:'a->'a->bool. dorder g ==>
617 !x x0 y y0. (x tends x0)(mtop(mr1),g) /\
618 (y tends y0)(mtop(mr1),g) /\ ~(y0 = &0) ==>
619 ((\n. x(n) / y(n)) tends (x0 / y0))(mtop(mr1),g)
620Proof
621 GEN_TAC THEN DISCH_TAC THEN REPEAT GEN_TAC THEN DISCH_TAC THEN
622 REWRITE_TAC[real_div] THEN
623 CONV_TAC(EXACT_CONV[X_BETA_CONV “n:'a” “inv(y(n:'a))”]) THEN
624 FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP NET_MUL) THEN
625 ASM_REWRITE_TAC[] THEN
626 FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP NET_INV) THEN
627 ASM_REWRITE_TAC[]
628QED
629
630Theorem NET_ABS:
631 !g x x0. (x tends x0)(mtop(mr1),g) ==>
632 ((\n:'a. abs(x n)) tends abs(x0))(mtop(mr1),g)
633Proof
634 REPEAT GEN_TAC THEN REWRITE_TAC[MTOP_TENDS] THEN
635 DISCH_TAC THEN X_GEN_TAC “e:real” THEN
636 DISCH_THEN(fn th => POP_ASSUM(MP_TAC o C MATCH_MP th)) THEN
637 DISCH_THEN(X_CHOOSE_THEN “N:'a” STRIP_ASSUME_TAC) THEN
638 EXISTS_TAC “N:'a” THEN ASM_REWRITE_TAC[] THEN
639 X_GEN_TAC “n:'a” THEN DISCH_TAC THEN BETA_TAC THEN
640 MATCH_MP_TAC REAL_LET_TRANS THEN
641 EXISTS_TAC “dist(mr1)(x(n:'a),x0)” THEN CONJ_TAC THENL
642 [REWRITE_TAC[MR1_DEF, ABS_SUB_ABS],
643 FIRST_ASSUM MATCH_MP_TAC THEN FIRST_ASSUM ACCEPT_TAC]
644QED
645
646(*---------------------------------------------------------------------------*)
647(* Comparison between limits *)
648(*---------------------------------------------------------------------------*)
649
650Theorem NET_LE:
651 !g:'a->'a->bool. dorder g ==>
652 !x x0 y y0. (x tends x0)(mtop(mr1),g) /\
653 (y tends y0)(mtop(mr1),g) /\
654 (?N. g N N /\ !n. g n N ==> x(n) <= y(n))
655 ==> x0 <= y0
656Proof
657 GEN_TAC THEN DISCH_TAC THEN REPEAT GEN_TAC THEN DISCH_TAC THEN
658 GEN_REWR_TAC I [TAUT ‘a = ~~a:bool’] THEN
659 PURE_ONCE_REWRITE_TAC[REAL_NOT_LE] THEN
660 ONCE_REWRITE_TAC[GSYM REAL_SUB_LT] THEN DISCH_TAC THEN
661 FIRST_ASSUM(UNDISCH_TAC o assert is_conj o concl) THEN
662 REWRITE_TAC[CONJ_ASSOC] THEN
663 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
664 REWRITE_TAC[MTOP_TENDS] THEN
665 DISCH_THEN(MP_TAC o end_itlist CONJ o
666 map (SPEC “(x0 - y0) / &2”) o CONJUNCTS) THEN
667 ASM_REWRITE_TAC[REAL_LT_HALF1] THEN
668 DISCH_THEN(DORDER_THEN MP_TAC) THEN
669 FIRST_ASSUM(UNDISCH_TAC o assert is_exists o concl) THEN
670 DISCH_THEN(fn th1 => DISCH_THEN (fn th2 => MP_TAC(CONJ th1 th2))) THEN
671 DISCH_THEN(DORDER_THEN MP_TAC) THEN
672 DISCH_THEN(X_CHOOSE_THEN “N:'a” (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
673 BETA_TAC THEN DISCH_THEN(MP_TAC o SPEC “N:'a”) THEN ASM_REWRITE_TAC[] THEN
674 REWRITE_TAC[MR1_DEF] THEN ONCE_REWRITE_TAC[ABS_SUB] THEN
675 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
676 REWRITE_TAC[REAL_NOT_LE] THEN MATCH_MP_TAC ABS_BETWEEN2 THEN
677 MAP_EVERY EXISTS_TAC [“y0:real”, “x0:real”] THEN
678 ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[GSYM REAL_SUB_LT] THEN
679 FIRST_ASSUM ACCEPT_TAC
680QED
681
682(* ------------------------------------------------------------------------- *)
683(* Net As Type *)
684(* ------------------------------------------------------------------------- *)
685
686Definition isnet :
687 isnet g <=> !x y. (!z. g z x ==> g z y) \/ (!z. g z y ==> g z x)
688End
689
690val net_tydef = new_type_definition
691 ("net",
692 prove (``?(g:'a->'a->bool). isnet g``,
693 EXISTS_TAC ``\x:'a y:'a. F`` THEN REWRITE_TAC[isnet]));
694
695val net_ty_bij = define_new_type_bijections
696 {name="net_tybij",
697 ABS="mk_net", REP="netord",tyax=net_tydef};
698
699Theorem net_tybij[allow_rebind]:
700 (!a. mk_net (netord a) = a) /\
701 (!r. (!x y. (!z. r z x ==> r z y) \/ (!z. r z y ==> r z x)) <=>
702 (netord (mk_net r) = r))
703Proof
704 SIMP_TAC std_ss [net_ty_bij, GSYM isnet]
705QED
706
707Theorem NET :
708 !n x y. (!z. netord n z x ==> netord n z y) \/
709 (!z. netord n z y ==> netord n z x)
710Proof
711 REWRITE_TAC[net_tybij, ETA_AX]
712QED
713
714Theorem OLDNET :
715 !n x y. netord n x x /\ netord n y y
716 ==> ?z. netord n z z /\
717 !w. netord n w z ==> netord n w x /\ netord n w y
718Proof
719 MESON_TAC[NET]
720QED
721
722Theorem NET_DILEMMA :
723 !net. (?a. (?x. netord net x a) /\ (!x. netord net x a ==> P x)) /\
724 (?b. (?x. netord net x b) /\ (!x. netord net x b ==> Q x))
725 ==> ?c. (?x. netord net x c) /\ (!x. netord net x c ==> P x /\ Q x)
726Proof
727 MESON_TAC[NET]
728QED
729
730(* NOTE: It seems that purpose of “g x x” in dorder for “at a”, is to make
731 sure ‘x <> a’, or 0 < mdist m (x,a).
732 *)
733Theorem DORDER_NET :
734 !net. dorder (netord net)
735Proof
736 RW_TAC std_ss [dorder, OLDNET]
737QED
738
739(* ------------------------------------------------------------------------- *)
740(* Common nets and the "within" modifier for nets. *)
741(* ------------------------------------------------------------------------- *)
742
743val _ = set_fixity "within" (Infix(NONASSOC, 450));
744val _ = set_fixity "in_direction" (Infix(NONASSOC, 450));
745
746(* HOL-Light: (atpointof top a) = mk_net({u | open_in top u /\ a IN u},{a})
747
748 NOTE: HOL-Light's “atpointof” takes a (general) topology, while here HOL4
749 takes a metric (therefore only works for metrizable topology).
750 *)
751Definition atpointof_def[nocompute]:
752 atpointof m a = mk_net (tendsto (m,a))
753End
754
755(* HOL-Light: at a = atpointof euclidean a *)
756Definition at_DEF :
757 at z = atpointof mr1 z
758End
759
760(* The previous "definition" now (again) becomes a theorem. *)
761Theorem at_def :
762 !z. at z = mk_net (tendsto (mr1,z))
763Proof
764 RW_TAC std_ss [at_DEF, atpointof_def]
765QED
766
767Theorem atpointof :
768 !m a. atpointof m a =
769 mk_net (\x y. 0 < mdist m (x,a) /\ mdist m (x,a) <= mdist m (y,a))
770Proof
771 RW_TAC std_ss [atpointof_def]
772 >> AP_TERM_TAC
773 >> RW_TAC std_ss [FUN_EQ_THM, tendsto]
774 >> PROVE_TAC [METRIC_SYM]
775QED
776
777(* |- !a. at a = mk_net (\x y. 0 < dist (x,a) /\ dist (x,a) <= dist (y,a)) *)
778Theorem at = atpointof |> ISPEC “mr1”
779 |> REWRITE_RULE [GSYM at_DEF, GSYM dist_def]
780
781(* HOL-Light: at_infinity = mk_net({{x | b <= norm x} | b IN (:real)},{}) *)
782Definition at_infinity[nocompute]:
783 at_infinity = mk_net(\x y. abs(x) >= abs(y))
784End
785
786(* HOL-Light: at_posinfinity = mk_net({{x | a <= x} | a IN (:real)},{}) *)
787Definition at_posinfinity[nocompute]:
788 at_posinfinity = mk_net(\x y:real. x >= y)
789End
790
791(* HOL-Light: at_neginfinity = mk_net({{x | x <= a} | a IN (:real)},{}) *)
792Definition at_neginfinity[nocompute]:
793 at_neginfinity = mk_net(\x y:real. x <= y)
794End
795
796(* HOL-Light: sequentially = mk_net({from n | n IN (:num)},{}) *)
797Definition sequentially[nocompute]:
798 sequentially = mk_net(\m:num n. m >= n)
799End
800
801(* HOL-Light's definition:
802
803let within = new_definition
804 `net within s = mk_net (netfilter net relative_to s,netlimits net)`;;
805 *)
806Definition within[nocompute]:
807 (net within s) = mk_net(\x y. netord net x y /\ x IN s)
808End
809
810Definition in_direction[nocompute]:
811 (a in_direction v) = ((at a) within {b | ?c. &0 <= c /\ (b - a = c * v)})
812End
813
814(* ------------------------------------------------------------------------- *)
815(* Prove that they are all nets. *)
816(* ------------------------------------------------------------------------- *)
817
818fun NET_PROVE_TAC [def] =
819 SIMP_TAC std_ss [GSYM FUN_EQ_THM, def] THEN
820 REWRITE_TAC [ETA_AX] THEN
821 ASM_SIMP_TAC std_ss [GSYM(CONJUNCT2 net_tybij)];
822
823(* NOTE: Most of the time, user only need to use this theorem instead of the
824 definition(s) of “atpointof”.
825 *)
826Theorem ATPOINTOF :
827 !m a x y.
828 netord(atpointof m a) x y <=>
829 0 < mdist m (x,a) /\ mdist m (x,a) <= mdist m (y,a)
830Proof
831 NTAC 2 GEN_TAC THEN NET_PROVE_TAC[atpointof] THEN
832 METIS_TAC[REAL_LE_TOTAL, REAL_LE_REFL, REAL_LE_TRANS, REAL_LET_TRANS]
833QED
834
835(* |- !a x y.
836 netord (at a) x y <=> 0 < dist (x,a) /\ dist (x,a) <= dist (y,a)
837 *)
838Theorem AT = ATPOINTOF |> ISPEC “mr1”
839 |> REWRITE_RULE [GSYM at_DEF, GSYM dist_def]
840
841Theorem tendsto_alt_atpointof :
842 !m a. tendsto (m,a) = netord (atpointof m a)
843Proof
844 rw [FUN_EQ_THM, tendsto, ATPOINTOF]
845 >> METIS_TAC [MDIST_SYM]
846QED
847
848(* Connection between HOL4's “tendsto” and HOL-Light's “at”, cf. [at_def]
849
850 |- !a. tendsto (mr1,a) = netord (at a)
851 *)
852Theorem tendsto_mr1 = tendsto_alt_atpointof |> ISPEC “mr1”
853 |> REWRITE_RULE [GSYM at_DEF]
854
855Theorem AT_INFINITY:
856 !x y. netord at_infinity x y <=> abs(x) >= abs(y)
857Proof
858 NET_PROVE_TAC[at_infinity] THEN
859 REWRITE_TAC[real_ge, REAL_LE_REFL] THEN
860 MESON_TAC[REAL_LE_TOTAL, REAL_LE_REFL, REAL_LE_TRANS]
861QED
862
863Theorem AT_POSINFINITY:
864 !x y. netord at_posinfinity x y <=> x >= y
865Proof
866 NET_PROVE_TAC[at_posinfinity] THEN
867 REWRITE_TAC[real_ge, REAL_LE_REFL] THEN
868 MESON_TAC[REAL_LE_TOTAL, REAL_LE_REFL, REAL_LE_TRANS]
869QED
870
871Theorem AT_NEGINFINITY:
872 !x y. netord at_neginfinity x y <=> x <= y
873Proof
874 NET_PROVE_TAC[at_neginfinity] THEN
875 REWRITE_TAC[real_ge, REAL_LE_REFL] THEN
876 MESON_TAC[REAL_LE_TOTAL, REAL_LE_REFL, REAL_LE_TRANS]
877QED
878
879Theorem SEQUENTIALLY:
880 !m n. netord sequentially m n <=> m >= n
881Proof
882 NET_PROVE_TAC[sequentially] THEN REWRITE_TAC[GREATER_EQ, LESS_EQ_REFL] THEN
883 MESON_TAC[LESS_EQ_CASES, LESS_EQ_REFL, LESS_EQ_TRANS]
884QED
885
886Theorem WITHIN:
887 !n s x y. netord(n within s) x y <=> netord n x y /\ x IN s
888Proof
889 GEN_TAC THEN GEN_TAC THEN SIMP_TAC std_ss [within, GSYM FUN_EQ_THM] THEN
890 REWRITE_TAC[GSYM(CONJUNCT2 net_tybij), ETA_AX] THEN
891 METIS_TAC[NET]
892QED
893
894Theorem IN_DIRECTION:
895 !a v x y. netord(a in_direction v) x y <=>
896 &0 < dist(x,a) /\ dist(x,a) <= dist(y,a) /\
897 ?c. &0 <= c /\ (x - a = c * v)
898Proof
899 SIMP_TAC std_ss [WITHIN, AT, in_direction, GSPECIFICATION] THEN METIS_TAC []
900QED
901
902Theorem NET_WITHIN_UNIV :
903 !net. (net within UNIV) = net
904Proof
905 RW_TAC std_ss [within, IN_UNIV, SF ETA_ss, net_tybij]
906QED
907
908Theorem WITHIN_UNIV :
909 !x. (at x within UNIV) = at x
910Proof
911 REWRITE_TAC [NET_WITHIN_UNIV]
912QED
913
914Theorem WITHIN_WITHIN:
915 !net s t. ((net within s) within t) = (net within (s INTER t))
916Proof
917 ONCE_REWRITE_TAC[within] THEN
918 REWRITE_TAC[WITHIN, IN_INTER, GSYM CONJ_ASSOC]
919QED
920
921(* ------------------------------------------------------------------------- *)
922(* It's also sometimes useful to extract the limit point from the net. *)
923(* ------------------------------------------------------------------------- *)
924
925(* NOTE: adding “x <> a” after “!x.” will break proof of NETLIMIT_ATPOINTOF. *)
926Definition netlimit_def :
927 netlimit net = @a. !x. ~(netord net x a)
928End
929
930(* NOTE: The definition of “netlimits” must be alighed with “netlimit”. *)
931Definition netlimits_def :
932 netlimits net = {a | !x. ~(netord net x a)}
933End
934
935(* NOTE: This theorem is the definition of “netlimit” in HOL-Light *)
936Theorem netlimit :
937 !n. netlimit n = (@x. x IN netlimits n)
938Proof
939 rw [netlimit_def, netlimits_def]
940QED
941
942Theorem NETLIMIT_ATPOINTOF :
943 !m a. netlimit(atpointof m a) = a
944Proof
945 RW_TAC std_ss [netlimit_def, ATPOINTOF]
946 >> SELECT_ELIM_TAC
947 >> CONJ_TAC
948 >- (Q.EXISTS_TAC ‘a’ \\
949 rw [MDIST_REFL, REAL_NOT_LE, MDIST_POS_LT])
950 >> rw [REAL_NOT_LE, MDIST_POS_EQ]
951 >> CCONTR_TAC
952 >> Q.PAT_X_ASSUM ‘!x. P’ (MP_TAC o Q.SPEC ‘x’)
953 >> simp [REAL_NOT_LT, MDIST_REFL, MDIST_POS_LE, MDIST_POS_LT]
954QED
955
956(* |- !a. netlimit (at a) = a *)
957Theorem NETLIMIT_AT = NETLIMIT_ATPOINTOF |> ISPEC “mr1”
958 |> REWRITE_RULE [GSYM at_DEF]
959
960Theorem NETLIMITS_ATPOINTOF :
961 !m a. netlimits (atpointof m a) = {a}
962Proof
963 rw [netlimits_def, ATPOINTOF, MDIST_POS_EQ, REAL_NOT_LE]
964 >> rw [Once EXTENSION]
965 >> reverse EQ_TAC >- rw [MDIST_REFL, MDIST_POS_EQ]
966 >> rpt STRIP_TAC
967 >> CCONTR_TAC
968 >> Q.PAT_X_ASSUM ‘!x. P’ (MP_TAC o Q.SPEC ‘x’)
969 >> simp [REAL_NOT_LT, MDIST_REFL, MDIST_POS_LE]
970QED
971
972(* |- !a. netlimits (at a) = {a} *)
973Theorem NETLIMITS_AT = NETLIMITS_ATPOINTOF |> ISPEC “mr1”
974 |> REWRITE_RULE [GSYM at_DEF]
975
976Theorem NETLIMITS_SEQUENTIALLY :
977 netlimits sequentially = {}
978Proof
979 rw [Once EXTENSION, NOT_IN_EMPTY, netlimits_def, SEQUENTIALLY, GREATER_EQ]
980 >> Q.EXISTS_TAC ‘x’ >> simp []
981QED
982
983Theorem NETLIMITS_AT_POSINFINITY :
984 netlimits at_posinfinity = {}
985Proof
986 rw [Once EXTENSION, NOT_IN_EMPTY, netlimits_def, AT_POSINFINITY, real_ge]
987 >> Q.EXISTS_TAC ‘x’ >> simp []
988QED
989
990Theorem NETLIMITS_AT_NEGINFINITY :
991 netlimits at_neginfinity = {}
992Proof
993 rw [Once EXTENSION, NOT_IN_EMPTY, netlimits_def, AT_NEGINFINITY]
994 >> Q.EXISTS_TAC ‘x’ >> simp []
995QED
996
997Theorem NETLIMITS_AT_INFINITY :
998 netlimits at_infinity = {}
999Proof
1000 rw [Once EXTENSION, NOT_IN_EMPTY, netlimits_def, AT_INFINITY, real_ge]
1001 >> Q.EXISTS_TAC ‘x’ >> simp []
1002QED
1003
1004(* NOTE: This lemma shows that “within” makes netlimits potentially larger. *)
1005Theorem NETLIMITS_WITHIN_lemma1[local] :
1006 netlimits net SUBSET netlimits (net within s)
1007Proof
1008 rw [SUBSET_DEF, netlimits_def, WITHIN]
1009QED
1010
1011Theorem NETLIMITS_WITHIN_lemma2[local] :
1012 (!x. (!y. ~netord net y x \/ y NOTIN s) ==> x IN netlimits net) ==>
1013 netlimits (net within s) SUBSET netlimits net
1014Proof
1015 rpt STRIP_TAC
1016 >> simp [SUBSET_DEF, Once netlimits_def, WITHIN]
1017QED
1018
1019Theorem NETLIMITS_WITHIN_lemma3[local] :
1020 (!x. (!y. ~netord net y x \/ y NOTIN s) ==> x IN netlimits net) <=>
1021 (!x. x NOTIN netlimits net ==> ?y. y IN s /\ netord net y x)
1022Proof
1023 METIS_TAC []
1024QED
1025
1026(* NOTE: This definition is the exact condition for “NETLIMITS_WITHIN” to hold. *)
1027Definition net_condition_def :
1028 net_condition net s =
1029 !x. x NOTIN netlimits net ==> ?y. y IN s /\ netord net y x
1030End
1031
1032Theorem NET_CONDITION_MONO :
1033 !net s t. net_condition net s /\ s SUBSET t ==> net_condition net t
1034Proof
1035 rw [net_condition_def, SUBSET_DEF]
1036 >> METIS_TAC []
1037QED
1038
1039Theorem NET_CONDITION_UNION :
1040 !net s t. net_condition net s /\ net_condition net s ==>
1041 net_condition net (s UNION t)
1042Proof
1043 rw [net_condition_def]
1044 >> ‘?y. y IN s /\ netord net y x’ by PROVE_TAC []
1045 >> Q.EXISTS_TAC ‘y’ >> art []
1046QED
1047
1048Theorem NET_CONDITION_UNIV[simp] :
1049 net_condition net UNIV
1050Proof
1051 rw [net_condition_def, netlimits_def]
1052QED
1053
1054(* NOTE: This is key theorem for which the “net_condition” is defined. *)
1055Theorem NETLIMITS_WITHIN :
1056 !net s. net_condition net s ==> netlimits (net within s) = netlimits net
1057Proof
1058 RW_TAC std_ss [net_condition_def]
1059 >> MATCH_MP_TAC SUBSET_ANTISYM
1060 >> REWRITE_TAC [NETLIMITS_WITHIN_lemma1]
1061 >> MATCH_MP_TAC NETLIMITS_WITHIN_lemma2
1062 >> ASM_REWRITE_TAC [NETLIMITS_WITHIN_lemma3]
1063QED
1064
1065Theorem NET_CONDITION_ATPOINTOF :
1066 !m a s. limpt (mtop m) a s ==> net_condition (atpointof m a) s
1067Proof
1068 rw [ATPOINTOF, net_condition_def, NETLIMITS_ATPOINTOF, MTOP_LIMPT']
1069 >> qabbrev_tac ‘e = dist m (x,a)’
1070 >> ‘0 < e’ by simp [Abbr ‘e’, MDIST_POS_LT]
1071 >> Q.PAT_X_ASSUM ‘!e. 0 < e ==> _’ (MP_TAC o Q.SPEC ‘e’) >> rw []
1072 >> Q.EXISTS_TAC ‘y’
1073 >> simp [MDIST_REFL, MDIST_POS_LE, MDIST_POS_LT, REAL_LT_IMP_LE, Once MDIST_SYM]
1074QED
1075
1076Theorem NET_CONDITION_AT_lemma[local] :
1077 !a s. net_condition (at a) s ==> limpt (mtop mr1) a s
1078Proof
1079 rw [AT, net_condition_def, NETLIMITS_AT, MTOP_LIMPT', GSYM dist_def]
1080 (* NOTE: this subgoal property doesn't hold for metric space in general *)
1081 >> Know ‘?x. x <> a /\ dist (a,x) = e / 2’
1082 >- (Q.EXISTS_TAC ‘a - e / 2’ \\
1083 simp [dist, REAL_SUB_SUB2] \\
1084 ‘0 < e / 2’ by simp [REAL_HALF] \\
1085 simp [ABS_REDUCE, REAL_LT_IMP_LE] \\
1086 REAL_ASM_ARITH_TAC)
1087 >> STRIP_TAC
1088 >> Q.PAT_X_ASSUM ‘!x. x <> a ==> _’ (MP_TAC o Q.SPEC ‘x’) >> rw []
1089 >> Q.EXISTS_TAC ‘y’
1090 >> FULL_SIMP_TAC std_ss [GSYM DIST_NZ]
1091 >> simp [Once DIST_SYM]
1092 >> Q_TAC (TRANS_TAC REAL_LET_TRANS) ‘dist (x,a)’ >> art []
1093 >> simp [Once DIST_SYM]
1094QED
1095
1096(* |- !a s. net_condition (at a) s <=> limpt (mtop mr1) a s *)
1097Theorem NET_CONDITION_AT :
1098 !a s. net_condition (at a) s <=> limpt (mtop mr1) a s
1099Proof
1100 rpt GEN_TAC
1101 >> EQ_TAC >- REWRITE_TAC [NET_CONDITION_AT_lemma]
1102 >> REWRITE_TAC [at_DEF, NET_CONDITION_ATPOINTOF]
1103QED
1104
1105Theorem NETLIMITS_ATPOINTOF_WITHIN :
1106 !m a s. limpt (mtop m) a s ==>
1107 netlimits ((atpointof m a) within s) = netlimits (atpointof m a)
1108Proof
1109 rpt STRIP_TAC
1110 >> MATCH_MP_TAC NETLIMITS_WITHIN
1111 >> MATCH_MP_TAC NET_CONDITION_ATPOINTOF >> art []
1112QED
1113
1114(* |- !a s.
1115 net_condition (at a) s ==>
1116 netlimits (at a within s) = netlimits (at a)
1117 *)
1118Theorem NETLIMITS_AT_WITHIN =
1119 NETLIMITS_ATPOINTOF_WITHIN |> ISPEC “mr1”
1120 |> REWRITE_RULE [GSYM at_DEF, GSYM NET_CONDITION_AT]
1121
1122(* NOTE: The original NETLIMIT_WITHIN is still below *)
1123Theorem NETLIMIT_WITHIN_NEW :
1124 !a s. net_condition (at a) s ==> netlimit (at a within s) = a
1125Proof
1126 rpt STRIP_TAC
1127 >> ASM_SIMP_TAC std_ss [netlimit, NETLIMITS_WITHIN]
1128 >> REWRITE_TAC [GSYM netlimit, NETLIMIT_AT]
1129QED
1130
1131(* ------------------------------------------------------------------------- *)
1132(* netfilter (compatible with HOL-Light) *)
1133(* ------------------------------------------------------------------------- *)
1134
1135(* NOTE: “x NOTIN netlimits net” is necessary for EVENTUALLY_ATPOINTOF below.
1136 And also, if it's replaced by “T” then “netfilter net <> {}” holds, making
1137 the first part of “eventually” (below, unchangable) meaningless.
1138 *)
1139Definition netfilter_def :
1140 netfilter net = {{y | netord net y x} | x | x NOTIN netlimits net}
1141End
1142
1143Theorem EMPTY_NOTIN_NETFILTER :
1144 !net. {} NOTIN netfilter net
1145Proof
1146 simp [netfilter_def, netlimits_def, Once EXTENSION] >> METIS_TAC []
1147QED
1148
1149(* NOTE: This is the theorem [NET] of HOL-Light *)
1150Theorem NETFILTER :
1151 !n s t. s IN netfilter n /\ t IN netfilter n ==> s INTER t IN netfilter n
1152Proof
1153 rpt GEN_TAC
1154 >> simp [netfilter_def]
1155 >> DISCH_THEN (CONJUNCTS_THEN2
1156 (Q.X_CHOOSE_THEN ‘u’ STRIP_ASSUME_TAC)
1157 (Q.X_CHOOSE_THEN ‘v’ STRIP_ASSUME_TAC))
1158 >> ‘s INTER t = {y | netord n y u /\ netord n y v}’ by ASM_SET_TAC []
1159 >> POP_ORW
1160 (* applying NET here! *)
1161 >> STRIP_ASSUME_TAC (Q.SPECL [‘n’, ‘u’, ‘v’] NET)
1162 >| [ (* goal 1 (of 2) *)
1163 Q.EXISTS_TAC ‘u’ >> ASM_SET_TAC [],
1164 (* goal 2 (of 2) *)
1165 Q.EXISTS_TAC ‘v’ >> ASM_SET_TAC [] ]
1166QED
1167
1168Theorem NETFILTER_AT_POSINFINITY :
1169 netfilter at_posinfinity = {{x | a <= x} | a IN univ(:real)}
1170Proof
1171 simp [netfilter_def, NETLIMITS_AT_POSINFINITY, AT_POSINFINITY, real_ge]
1172QED
1173
1174Theorem NETFILTER_AT_NEGINFINITY :
1175 netfilter at_neginfinity = {{x | x <= a} | a IN univ(:real)}
1176Proof
1177 simp [netfilter_def, NETLIMITS_AT_NEGINFINITY, AT_NEGINFINITY]
1178QED
1179
1180Theorem NETFILTER_AT_INFINITY :
1181 netfilter at_infinity = {{x | b <= abs x} | b IN univ(:real)}
1182Proof
1183 simp [netfilter_def, NETLIMITS_AT_INFINITY, AT_INFINITY, real_ge]
1184 >> rw [Once EXTENSION]
1185 >> EQ_TAC >> rw []
1186 >- (Q.EXISTS_TAC ‘abs x'’ >> REFL_TAC)
1187 >> Cases_on ‘0 <= b’
1188 >- (Q.EXISTS_TAC ‘abs b’ >> simp [ABS_REDUCE])
1189 >> fs [REAL_NOT_LE]
1190 >> Know ‘!x. b <= abs x <=> 0 <= abs x’
1191 >- (Q.X_GEN_TAC ‘x’ \\
1192 EQ_TAC >> rw [] \\
1193 Q_TAC (TRANS_TAC REAL_LE_TRANS) ‘0’ >> simp [ABS_POS, REAL_LT_IMP_LE])
1194 >> Rewr'
1195 >> Q.EXISTS_TAC ‘0’ >> simp [ABS_0]
1196QED
1197
1198Theorem NETFILTER_SEQUENTIALLY :
1199 netfilter sequentially = {from n | n IN univ(:num)}
1200Proof
1201 simp [netfilter_def, NETLIMITS_SEQUENTIALLY, SEQUENTIALLY,
1202 GREATER_EQ, from_def]
1203QED
1204
1205Theorem NETFILTER_ATPOINTOF :
1206 !m a. netfilter (atpointof m a) =
1207 {{y | 0 < dist m (y,a) /\ dist m (y,a) <= dist m (x,a)} | x | x <> a}
1208Proof
1209 simp [netfilter_def, NETLIMITS_ATPOINTOF, ATPOINTOF, MDIST_POS_EQ]
1210QED
1211
1212(* |- !a. netfilter (at a) =
1213 {{y | 0 < dist (y,a) /\ dist (y,a) <= dist (x,a)} | x | x <> a}
1214 *)
1215Theorem NETFILTER_AT =
1216 NETFILTER_ATPOINTOF |> ISPEC “mr1”
1217 |> REWRITE_RULE [GSYM dist_def, GSYM at_DEF]
1218
1219(* NOTE: This theorem is HOL-Light's WITHIN *)
1220Theorem NETFILTER_WITHIN :
1221 !net s. net_condition net s ==>
1222 (netfilter (net within s) = netfilter net relative_to s)
1223Proof
1224 rw [netfilter_def, WITHIN, RELATIVE_TO, NETLIMITS_WITHIN]
1225 >> rw [Once EXTENSION]
1226 >> EQ_TAC >> rw []
1227 >- (rename1 ‘x NOTIN netlimits net’ \\
1228 Q.EXISTS_TAC ‘{y | netord net y x}’ \\
1229 reverse CONJ_TAC >- (Q.EXISTS_TAC ‘x’ >> art []) \\
1230 SET_TAC [])
1231 >> rename1 ‘x NOTIN netlimits net’
1232 >> Q.EXISTS_TAC ‘x’ >> art []
1233 >> SET_TAC []
1234QED
1235
1236(* ------------------------------------------------------------------------- *)
1237(* Some property holds "sufficiently close" to the limit point (eventually). *)
1238(* ------------------------------------------------------------------------- *)
1239(* Identify trivial limits, where we can't approach arbitrarily closely. *)
1240(* ------------------------------------------------------------------------- *)
1241
1242(* old (existing) definitions diverged from HOL-Light *)
1243Definition trivial_limit :
1244 trivial_limit net <=>
1245 (!(a:'a) b. a = b) \/
1246 ?(a:'a) b. ~(a = b) /\ !x. ~(netord(net) x a) /\ ~(netord(net) x b)
1247End
1248
1249Definition eventually :
1250 eventually p net <=>
1251 trivial_limit net \/
1252 ?y. (?x. netord net x y) /\ (!x. netord net x y ==> p x)
1253End
1254
1255(* new definitions (compatible with HOL-Light)
1256Definition eventually_def :
1257 eventually (P :'a -> bool) net <=>
1258 netfilter net = {} \/
1259 ?u. u IN netfilter net /\
1260 !x. x IN u DIFF netlimits net ==> P x
1261End
1262
1263Definition trivial_limit_def :
1264 trivial_limit net = eventually (\x. F) net
1265End
1266 *)
1267
1268(* ------------------------------------------------------------------------- *)
1269
1270Theorem NONTRIVIAL_LIMIT_WITHIN :
1271 !net s. trivial_limit net ==> trivial_limit(net within s)
1272Proof
1273 REWRITE_TAC[trivial_limit, WITHIN] THEN MESON_TAC[]
1274QED
1275
1276Theorem TRIVIAL_LIMIT_AT_INFINITY :
1277 ~(trivial_limit at_infinity)
1278Proof
1279 REWRITE_TAC[trivial_limit, AT_INFINITY, real_ge] THEN
1280 MESON_TAC[REAL_LE_REFL, REAL_CHOOSE_SIZE, REAL_LT_01, REAL_LT_LE]
1281QED
1282
1283Theorem TRIVIAL_LIMIT_AT_POSINFINITY :
1284 ~(trivial_limit at_posinfinity)
1285Proof
1286 REWRITE_TAC[trivial_limit, AT_POSINFINITY, DE_MORGAN_THM] THEN
1287 CONJ_TAC THENL
1288 [DISCH_THEN(MP_TAC o SPECL [``&0:real``, ``&1:real``]) THEN REAL_ARITH_TAC,
1289 ALL_TAC] THEN
1290 REWRITE_TAC[DE_MORGAN_THM, NOT_EXISTS_THM, real_ge, REAL_NOT_LE] THEN
1291 MESON_TAC[REAL_LT_TOTAL, REAL_LT_ANTISYM]
1292QED
1293
1294Theorem TRIVIAL_LIMIT_AT_NEGINFINITY :
1295 ~(trivial_limit at_neginfinity)
1296Proof
1297 REWRITE_TAC[trivial_limit, AT_NEGINFINITY, DE_MORGAN_THM] THEN
1298 CONJ_TAC THENL
1299 [DISCH_THEN(MP_TAC o SPECL [``&0:real``, ``&1:real``]) THEN REAL_ARITH_TAC,
1300 ALL_TAC] THEN
1301 REWRITE_TAC[DE_MORGAN_THM, NOT_EXISTS_THM, real_ge, REAL_NOT_LE] THEN
1302 MESON_TAC[REAL_LT_TOTAL, REAL_LT_ANTISYM]
1303QED
1304
1305Theorem TRIVIAL_LIMIT_SEQUENTIALLY :
1306 ~(trivial_limit sequentially)
1307Proof
1308 REWRITE_TAC[trivial_limit, SEQUENTIALLY] THEN
1309 MESON_TAC[GREATER_EQ, LESS_EQ_REFL, SUC_NOT]
1310QED
1311
1312Theorem EVENTUALLY_FALSE :
1313 !net. eventually (\x. F) net <=> trivial_limit net
1314Proof
1315 REWRITE_TAC[eventually] THEN MESON_TAC[]
1316QED
1317
1318Theorem EVENTUALLY_TRUE :
1319 !net. eventually (\x. T) net <=> T
1320Proof
1321 REWRITE_TAC[eventually, trivial_limit] THEN MESON_TAC[]
1322QED
1323
1324Theorem EVENTUALLY_HAPPENS :
1325 !net p. eventually p net ==> trivial_limit net \/ ?x. p x
1326Proof
1327 REWRITE_TAC[eventually] THEN MESON_TAC[]
1328QED
1329
1330Theorem NOT_EVENTUALLY :
1331 !net p. (!x. ~(p x)) /\ ~(trivial_limit net) ==> ~(eventually p net)
1332Proof
1333 REWRITE_TAC[eventually] THEN MESON_TAC[]
1334QED
1335
1336Theorem ALWAYS_EVENTUALLY :
1337 !net p. (!x. p x) ==> eventually p net
1338Proof
1339 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[eventually, trivial_limit] THEN
1340 MESON_TAC[]
1341QED
1342
1343Theorem EVENTUALLY_SEQUENTIALLY :
1344 !p. eventually p sequentially <=> ?N. !n. N <= n ==> p n
1345Proof
1346 REWRITE_TAC[eventually, SEQUENTIALLY, GREATER_EQ, LESS_EQ_REFL,
1347 TRIVIAL_LIMIT_SEQUENTIALLY] THEN MESON_TAC[LESS_EQ_REFL]
1348QED
1349
1350Theorem EVENTUALLY_AT_INFINITY :
1351 !p. eventually p at_infinity <=> ?b. !x. abs(x) >= b ==> p x
1352Proof
1353 SIMP_TAC std_ss [eventually, AT_INFINITY, TRIVIAL_LIMIT_AT_INFINITY] THEN
1354 REPEAT GEN_TAC THEN EQ_TAC THENL [MESON_TAC[REAL_LE_REFL], ALL_TAC] THEN
1355 MESON_TAC[real_ge, REAL_LE_REFL, REAL_CHOOSE_SIZE,
1356 REAL_ARITH ``&0 <= b:real \/ (!x. x >= &0 ==> x >= b)``]
1357QED
1358
1359Theorem EVENTUALLY_AT_POSINFINITY :
1360 !p. eventually p at_posinfinity <=> ?b. !x. x >= b ==> p x
1361Proof
1362 REWRITE_TAC[eventually, TRIVIAL_LIMIT_AT_POSINFINITY, AT_POSINFINITY] THEN
1363 MESON_TAC[REAL_ARITH ``x >= x``]
1364QED
1365
1366Theorem EVENTUALLY_AT_NEGINFINITY :
1367 !p. eventually p at_neginfinity <=> ?b. !x. x <= b ==> p x
1368Proof
1369 REWRITE_TAC[eventually, TRIVIAL_LIMIT_AT_NEGINFINITY, AT_NEGINFINITY] THEN
1370 MESON_TAC[REAL_LE_REFL]
1371QED
1372
1373Theorem EVENTUALLY_AT_INFINITY_POS :
1374 !p:real->bool.
1375 eventually p at_infinity <=> ?b. &0 < b /\ !x. abs x >= b ==> p x
1376Proof
1377 GEN_TAC THEN REWRITE_TAC[EVENTUALLY_AT_INFINITY, real_ge] THEN
1378 MESON_TAC[REAL_ARITH ``&0 < abs b + &1 /\ (abs b + &1 <= x ==> b <= x:real)``]
1379QED
1380
1381(* ------------------------------------------------------------------------- *)
1382(* Combining theorems for "eventually". *)
1383(* ------------------------------------------------------------------------- *)
1384
1385Theorem EVENTUALLY_AND :
1386 !net:('a net) p q.
1387 eventually (\x. p x /\ q x) net <=>
1388 eventually p net /\ eventually q net
1389Proof
1390 REPEAT GEN_TAC THEN REWRITE_TAC[eventually] THEN
1391 ASM_CASES_TAC ``trivial_limit(net:('a net))`` THEN ASM_REWRITE_TAC[] THEN
1392 EQ_TAC THEN SIMP_TAC std_ss [NET_DILEMMA] THENL [MESON_TAC [], ALL_TAC] THEN
1393 DISCH_TAC THEN MATCH_MP_TAC NET_DILEMMA THEN METIS_TAC []
1394QED
1395
1396Theorem EVENTUALLY_MONO :
1397 !net:('a net) p q.
1398 (!x. p x ==> q x) /\ eventually p net
1399 ==> eventually q net
1400Proof
1401 REWRITE_TAC[eventually] THEN MESON_TAC[]
1402QED
1403
1404Theorem EVENTUALLY_MP :
1405 !net:('a net) p q.
1406 eventually (\x. p x ==> q x) net /\ eventually p net
1407 ==> eventually q net
1408Proof
1409 REWRITE_TAC[GSYM EVENTUALLY_AND] THEN
1410 REWRITE_TAC[eventually] THEN MESON_TAC[]
1411QED
1412
1413Theorem EVENTUALLY_FORALL :
1414 !net:('a net) p s:'b->bool.
1415 FINITE s /\ ~(s = {})
1416 ==> (eventually (\x. !a. a IN s ==> p a x) net <=>
1417 !a. a IN s ==> eventually (p a) net)
1418Proof
1419 GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[GSYM AND_IMP_INTRO] THEN
1420 KNOW_TAC ``!s:'b->bool. (s <> ({} :'b -> bool) ==>
1421 (eventually (\(x :'a). !(a :'b). a IN s ==> (p :'b -> 'a -> bool) a x)
1422 (net :'a net) <=> !(a :'b). a IN s ==> eventually (p a) net)) =
1423 (\s. s <> ({} :'b -> bool) ==>
1424 (eventually (\(x :'a). !(a :'b). a IN s ==> (p :'b -> 'a -> bool) a x)
1425 (net :'a net) <=> !(a :'b). a IN s ==> eventually (p a) net)) s`` THENL
1426 [FULL_SIMP_TAC std_ss [], ALL_TAC] THEN DISC_RW_KILL THEN
1427 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
1428 SIMP_TAC std_ss [FORALL_IN_INSERT, EVENTUALLY_AND, ETA_AX] THEN
1429 SIMP_TAC std_ss [GSYM RIGHT_FORALL_IMP_THM] THEN
1430 MAP_EVERY X_GEN_TAC [``t:'b->bool``, ``b:'b``] THEN
1431 ASM_CASES_TAC ``t:'b->bool = {}`` THEN
1432 ASM_SIMP_TAC std_ss [NOT_IN_EMPTY, EVENTUALLY_TRUE] THEN METIS_TAC []
1433QED
1434
1435Theorem FORALL_EVENTUALLY :
1436 !net:('a net) p s:'b->bool.
1437 FINITE s /\ ~(s = {})
1438 ==> ((!a. a IN s ==> eventually (p a) net) <=>
1439 eventually (\x. !a. a IN s ==> p a x) net)
1440Proof
1441 SIMP_TAC std_ss [EVENTUALLY_FORALL]
1442QED
1443
1444(* NOTE: This theorem is trivial (by NET_WITHIN_UNIV and MSPACE) in HOL4.
1445 The original HOL-Light version is:
1446
1447 |- !top a:A. (atpointof top a) within (topspace top) = atpointof top a
1448 *)
1449Theorem ATPOINTOF_WITHIN_TOPSPACE :
1450 !m a. ((atpointof m a) within (mspace m)) = atpointof m a
1451Proof
1452 rw [NET_WITHIN_UNIV, MSPACE]
1453QED
1454
1455Theorem NETLIMIT_WITHIN :
1456 !a:real s. ~(trivial_limit (at a within s))
1457 ==> (netlimit (at a within s) = a)
1458Proof
1459 REWRITE_TAC[trivial_limit, netlimit_def, AT, WITHIN, DE_MORGAN_THM] THEN
1460 REPEAT STRIP_TAC THEN MATCH_MP_TAC SELECT_UNIQUE THEN REWRITE_TAC[] THEN
1461 SUBGOAL_THEN
1462 ``!x:real. ~(&0 < dist(x,a) /\ dist(x,a) <= dist(a,a) /\ x IN s)``
1463 ASSUME_TAC THENL
1464 [ ASM_MESON_TAC[DIST_REFL, REAL_NOT_LT], ASM_MESON_TAC[] ]
1465QED
1466
1467(* ------------------------------------------------------------------------- *)
1468(* Limits in a topological space (from HOL-Light's Multivariate/metric.ml) *)
1469(* ------------------------------------------------------------------------- *)
1470
1471Definition limit :
1472 limit top (f:'a->'b) l net <=>
1473 l IN topspace top /\
1474 (!u. open_in top u /\ l IN u ==> eventually (\x. f x IN u) net)
1475End
1476
1477(* Connection between HOL-Light's ‘limit’ and HOL4's ‘tends’
1478
1479 NOTE: The net with ‘limit’ must be reflexive, which is not assumed in general.
1480 Further more, the net cannot be trivial, and ‘l IN topspace top’ must be
1481 assumed because it's not included with ‘f tends l’.
1482 *)
1483Theorem tends_imp_limit :
1484 !top f l net. ~trivial_limit net /\ l IN topspace top ==>
1485 (f tends l) (top,netord net) ==> limit top (f:'a->'b) l net
1486Proof
1487 rw [limit, tends, eventually, OPEN_NEIGH]
1488 >> Q.PAT_X_ASSUM ‘!x. u x ==> _’ (MP_TAC o Q.SPEC ‘l’)
1489 >> POP_ASSUM MP_TAC
1490 >> rw [IN_APP]
1491 >> Q.PAT_X_ASSUM ‘!N. neigh top (N,l) ==> _’ (MP_TAC o Q.SPEC ‘N’) >> rw []
1492 >> Q.EXISTS_TAC ‘n’
1493 >> CONJ_TAC >- (Q.EXISTS_TAC ‘n’ >> art [])
1494 >> rpt STRIP_TAC
1495 >> ‘f x IN N’ by rw [IN_APP]
1496 >> ‘f x IN u’ by PROVE_TAC [SUBSET_DEF] >> fs [IN_APP]
1497QED
1498
1499Theorem limit_alt_tends :
1500 !top f l net. ~trivial_limit net /\ l IN topspace top /\
1501 (!x y. netord net x y ==> netord net y y) ==>
1502 (limit top (f:'a->'b) l net <=> (f tends l) (top,netord net))
1503Proof
1504 rpt STRIP_TAC
1505 >> reverse EQ_TAC >- rw [tends_imp_limit]
1506 >> rw [limit, tends, reflexive_def, neigh]
1507 >> Q.PAT_X_ASSUM ‘!u. open_in top u /\ l IN u ==> _’ (MP_TAC o Q.SPEC ‘P’)
1508 >> rw [IN_APP, eventually]
1509 >> Q.EXISTS_TAC ‘y’
1510 >> CONJ_TAC
1511 >- (FIRST_X_ASSUM MATCH_MP_TAC \\
1512 Q.EXISTS_TAC ‘x’ >> art [])
1513 >> rpt STRIP_TAC
1514 >> ‘f m IN P’ by rw [IN_APP]
1515 >> ‘f m IN N’ by PROVE_TAC [SUBSET_DEF] >> fs [IN_APP]
1516QED
1517
1518(* END *)
1519
1520(* References:
1521
1522 [1] Moore, E.H., Smith, H.L.: A General Theory of Limits. American Journal of
1523 Mathematics. 44, 102-121 (1922).
1524 [2] Kelley, J.L.: General Topology. Springer Science & Business Media (1975).
1525 [3] https://en.wikipedia.org/wiki/Net_(mathematics)
1526 [4] Schilling, R.L.: Measures, Integrals and Martingales (2nd Edition).
1527 Cambridge University Press (2017).
1528 *)