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