metricScript.sml
1(*===========================================================================*)
2(* Metric spaces, including metric on real line *)
3(* ========================================================================= *)
4(* Formalization of general topological and metric spaces in HOL Light *)
5(* *)
6(* (c) Copyright, John Harrison 1998-2017 *)
7(* (c) Copyright, Marco Maggesi 2014-2017 *)
8(* (c) Copyright, Andrea Gabrielli 2016-2017 *)
9(* ========================================================================= *)
10
11Theory metric
12Ancestors
13 arithmetic num pair quotient pred_set real real_sigma cardinal
14 topology
15Libs
16 boolSimps simpLib mesonLib metisLib jrhUtils pairLib
17 pred_setLib RealArith tautLib realSimps hurdUtils
18
19fun METIS ths tm = prove(tm,METIS_TAC ths);
20val ASM_REAL_ARITH_TAC = REAL_ASM_ARITH_TAC;
21
22(* ------------------------------------------------------------------------- *)
23(* Handy lemmas switching between versions of limit arguments. *)
24(* (originally from hol-light's misc.ml, line 747-772) *)
25(* ------------------------------------------------------------------------- *)
26
27Theorem FORALL_POS_MONO :
28 !P. (!d e:real. d < e /\ P d ==> P e) /\ (!n. ~(n = 0) ==> P(inv(&n)))
29 ==> !e. &0 < e ==> P e
30Proof
31 MESON_TAC[REAL_ARCH_INV, REAL_LT_TRANS]
32QED
33
34Theorem FORALL_SUC :
35 (!n. n <> 0 ==> P n) <=> !n. P (SUC n)
36Proof
37 MESON_TAC[num_CASES, NOT_SUC]
38QED
39
40Theorem FORALL_POS_MONO_1 :
41 !P. (!d e. d < e /\ P d ==> P e) /\ (!n. P(inv(&n + &1)))
42 ==> !e. &0 < e ==> P e
43Proof
44 GEN_TAC >> REWRITE_TAC [REAL_OF_NUM_SUC]
45 >> STRIP_TAC
46 >> MATCH_MP_TAC FORALL_POS_MONO
47 >> ASM_REWRITE_TAC []
48 >> ASM_SIMP_TAC std_ss [FORALL_SUC]
49QED
50
51Theorem FORALL_POS_MONO_EQ :
52 !P. (!d e. d < e /\ P d ==> P e)
53 ==> ((!e. &0 < e ==> P e) <=> (!n. ~(n = 0) ==> P(inv(&n))))
54Proof
55 MESON_TAC[REAL_ARCH_INV, REAL_LT_INV_EQ, REAL_LT_TRANS, NOT_ZERO,
56 REAL_OF_NUM_LT]
57QED
58
59Theorem FORALL_POS_MONO_1_EQ :
60 !P. (!d e. d < e /\ P d ==> P e)
61 ==> ((!e. &0 < e ==> P e) <=> (!n. P(inv(&n + &1))))
62Proof
63 GEN_TAC THEN
64 DISCH_THEN(SUBST1_TAC o MATCH_MP FORALL_POS_MONO_EQ) THEN
65 SIMP_TAC std_ss [REAL_OF_NUM_SUC, GSYM FORALL_SUC]
66QED
67
68(*---------------------------------------------------------------------------*)
69(* Characterize an (alpha)metric *)
70(*---------------------------------------------------------------------------*)
71
72Definition ismet :
73 ismet (m :'a # 'a -> real) =
74 ((!x y. (m(x,y) = &0) <=> (x = y)) /\
75 (!x y z. m(y,z) <= m(x,y) + m(x,z)))
76End
77
78val metric_tydef = new_type_definition
79 ("metric",
80 prove (“?m:('a#'a->real). ismet m”,
81 EXISTS_TAC “\(x:'a,(y:'a)). if (x = y) then &0 else &1” THEN
82 REWRITE_TAC[ismet] THEN
83 CONV_TAC(ONCE_DEPTH_CONV PAIRED_BETA_CONV) THEN
84 CONJ_TAC THEN REPEAT GEN_TAC THENL
85 [BOOL_CASES_TAC “x:'a = y” THEN REWRITE_TAC[REAL_10],
86 REPEAT COND_CASES_TAC THEN
87 ASM_REWRITE_TAC[REAL_ADD_LID, REAL_ADD_RID, REAL_LE_REFL, REAL_LE_01]
88 THEN GEN_REWR_TAC LAND_CONV [GSYM REAL_ADD_LID] THEN
89 TRY(MATCH_MP_TAC REAL_LE_ADD2) THEN
90 REWRITE_TAC[REAL_LE_01, REAL_LE_REFL] THEN
91 FIRST_ASSUM(UNDISCH_TAC o assert is_neg o concl) THEN
92 EVERY_ASSUM(SUBST1_TAC o SYM) THEN REWRITE_TAC[]]));
93
94val metric_tybij = define_new_type_bijections
95 {name="metric_tybij",
96 ABS="metric", REP="dist", tyax=metric_tydef};
97
98(*---------------------------------------------------------------------------*)
99(* Derive the metric properties *)
100(*---------------------------------------------------------------------------*)
101
102Theorem METRIC_ISMET:
103 !m:('a)metric. ismet (dist m)
104Proof
105 GEN_TAC THEN REWRITE_TAC[metric_tybij]
106QED
107
108Theorem METRIC_ZERO:
109 !m:('a)metric. !x y. ((dist m)(x,y) = &0) = (x = y)
110Proof
111 REPEAT GEN_TAC THEN ASSUME_TAC(SPEC “m:('a)metric” METRIC_ISMET) THEN
112 RULE_ASSUM_TAC(REWRITE_RULE[ismet]) THEN ASM_REWRITE_TAC[]
113QED
114
115Theorem METRIC_SAME:
116 !m:('a)metric. !x. (dist m)(x,x) = &0
117Proof
118 REPEAT GEN_TAC THEN REWRITE_TAC[METRIC_ZERO]
119QED
120
121Theorem METRIC_POS:
122 !m:('a)metric. !x y. &0 <= (dist m)(x,y)
123Proof
124 REPEAT GEN_TAC THEN ASSUME_TAC(SPEC “m:('a)metric” METRIC_ISMET) THEN
125 RULE_ASSUM_TAC(REWRITE_RULE[ismet]) THEN
126 FIRST_ASSUM(MP_TAC o
127 SPECL [“x:'a”, “y:'a”, “y:'a”] o CONJUNCT2) THEN
128 REWRITE_TAC[REWRITE_RULE[]
129 (SPECL [“m:('a)metric”, “y:'a”, “y:'a”]
130 METRIC_ZERO)]
131 THEN CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[REAL_NOT_LE] THEN
132 DISCH_THEN(MP_TAC o MATCH_MP REAL_LT_ADD2 o W CONJ) THEN
133 REWRITE_TAC[REAL_ADD_LID]
134QED
135
136Theorem METRIC_SYM:
137 !m:('a)metric. !x y. (dist m)(x,y) = (dist m)(y,x)
138Proof
139 REPEAT GEN_TAC THEN ASSUME_TAC(SPEC “m:('a)metric” METRIC_ISMET) THEN
140 RULE_ASSUM_TAC(REWRITE_RULE[ismet]) THEN FIRST_ASSUM
141 (MP_TAC o GENL [“y:'a”, “z:'a”] o SPECL [“z:'a”, “y:'a”, “z:'a”] o CONJUNCT2)
142 THEN REWRITE_TAC[METRIC_SAME, REAL_ADD_RID] THEN
143 DISCH_TAC THEN ASM_REWRITE_TAC[GSYM REAL_LE_ANTISYM]
144QED
145
146Theorem METRIC_TRIANGLE:
147 !m:('a)metric. !x y z. (dist m)(x,z) <= (dist m)(x,y) + (dist m)(y,z)
148Proof
149 REPEAT GEN_TAC THEN ASSUME_TAC(SPEC “m:('a)metric” METRIC_ISMET) THEN
150 RULE_ASSUM_TAC(REWRITE_RULE[ismet]) THEN
151 GEN_REWR_TAC (RAND_CONV o LAND_CONV) [METRIC_SYM] THEN
152 ASM_REWRITE_TAC[]
153QED
154
155Theorem METRIC_NZ:
156 !m:('a)metric. !x y. ~(x = y) ==> &0 < (dist m)(x,y)
157Proof
158 REPEAT GEN_TAC THEN
159 SUBST1_TAC(SYM(SPECL [“m:('a)metric”, “x:'a”, “y:'a”] METRIC_ZERO)) THEN
160 ONCE_REWRITE_TAC[TAUT ‘~a ==> b <=> b \/ a’] THEN
161 CONV_TAC(RAND_CONV SYM_CONV) THEN
162 REWRITE_TAC[GSYM REAL_LE_LT, METRIC_POS]
163QED
164
165(*---------------------------------------------------------------------------*)
166(* Get a bounded metric (<1) from any metric *)
167(*---------------------------------------------------------------------------*)
168
169val bmetric_tm = “(dist m)(x,y) / (1 + (dist m)(x,y))”;
170
171Definition bounded_metric_def :
172 bounded_metric (m :'a metric) = metric (\(x,y). ^bmetric_tm)
173End
174
175(* NOTE: This lemma is useful when showing the metric is monotone w.r.t. x or y *)
176Theorem bounded_metric_alt :
177 !m x y. ^bmetric_tm = 1 - inv (1 + dist m (x,y))
178Proof
179 rw [FUN_EQ_THM]
180 >> Q.ABBREV_TAC ‘z = 1 + dist m (x,y)’
181 >> Know ‘0 < z’
182 >- (MATCH_MP_TAC REAL_LTE_TRANS \\
183 Q.EXISTS_TAC ‘1’ >> rw [Abbr ‘z’, METRIC_POS])
184 >> DISCH_TAC
185 >> ‘z <> 0’ by PROVE_TAC [REAL_LT_IMP_NE]
186 >> Know ‘dist m (x,y) = z - 1’
187 >- (Q.UNABBREV_TAC ‘z’ >> REAL_ARITH_TAC)
188 >> Rewr'
189 >> rw [real_div, REAL_SUB_LDISTRIB, REAL_MUL_RINV]
190QED
191
192Theorem bounded_metric_ismet :
193 !m. ismet (\(x,y). ^bmetric_tm)
194Proof
195 rw [ismet]
196 >- (fs [REAL_DIV_ZERO] \\
197 EQ_TAC >> rw [METRIC_ZERO] \\
198 Suff ‘0 < 1 + dist m (x,y)’ >- PROVE_TAC [REAL_LT_IMP_NE] \\
199 MATCH_MP_TAC REAL_LTE_TRANS \\
200 Q.EXISTS_TAC ‘1’ >> rw [METRIC_POS])
201 >> Know ‘!a b. 0 < 1 + dist m (a,b)’
202 >- (rpt GEN_TAC \\
203 MATCH_MP_TAC REAL_LTE_TRANS \\
204 Q.EXISTS_TAC ‘1’ >> rw [METRIC_POS])
205 >> DISCH_TAC
206 >> REWRITE_TAC [bounded_metric_alt]
207 >> ‘1 - inv (1 + dist m (x,y)) + (1 - inv (1 + dist m (x,z))) =
208 1 - (inv (1 + dist m (x,y)) + inv (1 + dist m (x,z)) - 1)’ by REAL_ARITH_TAC
209 >> POP_ORW
210 >> RW_TAC std_ss [REAL_LE_SUB_CANCEL1, REAL_LE_SUB_RADD]
211 (* applying METRIC_TRIANGLE *)
212 >> MATCH_MP_TAC REAL_LE_TRANS
213 >> Q.EXISTS_TAC ‘inv (1 + dist m (x,y) + dist m (x,z)) + 1’
214 >> reverse CONJ_TAC
215 >- (REWRITE_TAC [REAL_LE_RADD] \\
216 MATCH_MP_TAC REAL_LE_INV2 \\
217 rw [REAL_LE_LADD, GSYM REAL_ADD_ASSOC] \\
218 METIS_TAC [METRIC_SYM, METRIC_TRIANGLE])
219 >> Q.ABBREV_TAC ‘a = dist m (x,y)’
220 >> Q.ABBREV_TAC ‘b = dist m (x,z)’
221 >> ‘1 + a <> 0 /\ 1 + b <> 0’ by METIS_TAC [REAL_LT_IMP_NE]
222 (* LHS simplification *)
223 >> Know ‘inv (1 + a) = (1 + b) * inv ((1 + a) * (1 + b))’
224 >- (rw [REAL_INV_MUL, REAL_MUL_ASSOC] \\
225 ‘(1 + b) * inv (1 + a) * inv (1 + b) =
226 (1 + b) * inv (1 + b) * inv (1 + a)’ by REAL_ARITH_TAC >> POP_ORW \\
227 rw [REAL_MUL_RINV]) >> Rewr'
228 >> Know ‘inv (1 + b) = (1 + a) * inv ((1 + a) * (1 + b))’
229 >- (rw [REAL_INV_MUL, REAL_MUL_ASSOC, REAL_MUL_RINV])
230 >> Rewr'
231 >> rw [GSYM REAL_ADD_RDISTRIB, REAL_ARITH “1 + b + (1 + a) = 2 + a + (b :real)”]
232 >> Know ‘0 < 1 + a + b’
233 >- (MATCH_MP_TAC REAL_LTE_TRANS \\
234 Q.EXISTS_TAC ‘1’ >> rw [Abbr ‘a’, Abbr ‘b’, GSYM REAL_ADD_ASSOC] \\
235 MATCH_MP_TAC REAL_LE_ADD >> rw [METRIC_POS])
236 >> DISCH_TAC
237 >> Know ‘inv (1 + a + b) + 1 = (1 + (1 + a + b)) * inv (1 + a + b)’
238 >- (REWRITE_TAC [Once REAL_ADD_RDISTRIB, REAL_MUL_LID] \\
239 ‘1 + a + b <> 0’ by PROVE_TAC [REAL_LT_IMP_NE] \\
240 rw [REAL_MUL_RINV])
241 >> Rewr'
242 >> REWRITE_TAC [REAL_ARITH “1 + (1 + a + b) = 2 + a + (b :real)”]
243 >> Know ‘0 < 2 + a + b’
244 >- (MATCH_MP_TAC REAL_LTE_TRANS \\
245 Q.EXISTS_TAC ‘2’ >> rw [Abbr ‘a’, Abbr ‘b’, GSYM REAL_ADD_ASSOC] \\
246 MATCH_MP_TAC REAL_LE_ADD >> rw [METRIC_POS])
247 >> DISCH_TAC
248 >> ASM_SIMP_TAC std_ss [REAL_LE_LMUL]
249 >> MATCH_MP_TAC REAL_LE_INV2
250 >> rw [REAL_ADD_LDISTRIB, REAL_ADD_RDISTRIB, REAL_ADD_ASSOC]
251 >> REWRITE_TAC [REAL_ARITH “1 + b + a + a * b = 1 + a + b + a * (b :real)”]
252 >> rw [REAL_LE_ADDR, Abbr ‘a’, Abbr ‘b’]
253 >> MATCH_MP_TAC REAL_LE_MUL >> rw [METRIC_POS]
254QED
255
256Theorem bounded_metric_thm :
257 !m x y. dist (bounded_metric m) (x,y) = ^bmetric_tm
258Proof
259 rw [bounded_metric_def]
260 >> ‘dist (metric (\(x,y). ^bmetric_tm)) = (\(x,y). ^bmetric_tm)’
261 by (rw [GSYM metric_tybij, bounded_metric_ismet])
262 >> rw []
263QED
264
265Theorem bounded_metric_lt_1 :
266 !(m :'a metric) x y. dist (bounded_metric m) (x,y) < 1
267Proof
268 rw [bounded_metric_thm]
269 >> Know ‘0 < 1 + dist m (q,r)’
270 >- (MATCH_MP_TAC REAL_LTE_TRANS \\
271 Q.EXISTS_TAC ‘1’ >> rw [METRIC_POS])
272 >> DISCH_TAC
273 >> ‘1 + dist m (q,r) <> 0’ by rw [REAL_LT_IMP_NE]
274 >> MATCH_MP_TAC REAL_LT_1
275 >> rw [METRIC_POS]
276QED
277
278(*---------------------------------------------------------------------------*)
279(* Now define metric topology and prove equivalent definition of "open" *)
280(*---------------------------------------------------------------------------*)
281
282Definition mtop :
283 mtop (m :'a metric) =
284 topology (\S'. !x. S' x ==> ?e. &0 < e /\ !y. (dist m)(x,y) < e ==> S' y)
285End
286
287(* for HOL Light compatibility *)
288Overload mtopology[inferior] = “mtop”
289Overload mdist[inferior] = “dist”
290
291(* NOTE: HOL4's ‘mspace’ definition is different with HOL-Light *)
292Definition mspace :
293 mspace m = topspace (mtop m)
294End
295
296(* |- !m. topspace (mtop m) = mspace m *)
297Theorem TOPSPACE_MTOPOLOGY = GEN_ALL (GSYM mspace)
298
299Theorem mtop_istopology :
300 !m:('a)metric.
301 istopology (\S'. !x. S' x ==>
302 ?e. &0 < e /\
303 (!y. (dist m)(x,y) < e ==> S' y))
304Proof
305 GEN_TAC THEN
306 SIMP_TAC bool_ss [istopology, EMPTY_DEF, UNIV_DEF, BIGUNION_applied,
307 INTER_applied, SUBSET_applied, IN_DEF] THEN
308 REVERSE (REPEAT STRIP_TAC) THENL (* 2 subgoals *)
309 [ (* goal 1 (of 2) *)
310 RES_TAC >> Q.EXISTS_TAC `e` >> ASM_REWRITE_TAC [] \\
311 rpt STRIP_TAC \\
312 Q.EXISTS_TAC `s` >> ASM_REWRITE_TAC [] >> RES_TAC,
313 (* goal 2 (of 2) *)
314 RES_TAC \\
315 REPEAT_TCL DISJ_CASES_THEN MP_TAC
316 (SPECL [“e:real”, “e':real”] REAL_LT_TOTAL) >|
317 [ (* goal 2.1 (of 3) *)
318 DISCH_THEN SUBST_ALL_TAC THEN EXISTS_TAC “e':real” THEN
319 ASM_REWRITE_TAC [] THEN GEN_TAC THEN
320 DISCH_TAC >> PROVE_TAC [],
321 (* goal 2.2 (of 3) *)
322 DISCH_THEN(curry op THEN (EXISTS_TAC “e:real”) o MP_TAC) THEN
323 ASM_REWRITE_TAC [] THEN
324 DISCH_THEN (fn th2 => GEN_TAC THEN DISCH_THEN (fn th1 =>
325 ASSUME_TAC th1 THEN ASSUME_TAC (MATCH_MP REAL_LT_TRANS (CONJ th1 th2))))
326 >> PROVE_TAC [],
327 (* goal 2.3 (of 3) *)
328 DISCH_THEN(curry op THEN (EXISTS_TAC “e':real”) o MP_TAC) THEN
329 ASM_REWRITE_TAC [] THEN
330 DISCH_THEN (fn th2 => GEN_TAC THEN DISCH_THEN(fn th1 =>
331 ASSUME_TAC th1 THEN ASSUME_TAC (MATCH_MP REAL_LT_TRANS (CONJ th1 th2))))
332 >> PROVE_TAC [] ] ]
333QED
334
335Theorem MTOP_OPEN:
336 !S' (m:('a)metric). open_in(mtop m) S' =
337 (!x. S' x ==> ?e. &0 < e /\ (!y. (dist m(x,y)) < e ==> S' y))
338Proof
339 GEN_TAC THEN REWRITE_TAC[mtop] THEN
340 REWRITE_TAC[REWRITE_RULE[topology_tybij] mtop_istopology] THEN
341 BETA_TAC THEN REWRITE_TAC[]
342QED
343
344Theorem MTOP_OPEN' :
345 !m s. open_in(mtop m) s <=>
346 !x. x IN s ==> ?e. 0 < e /\ !y. dist m (x,y) < e ==> y IN s
347Proof
348 RW_TAC std_ss [IN_APP, MTOP_OPEN]
349QED
350
351(*---------------------------------------------------------------------------*)
352(* Define open ball in metric space + prove basic properties *)
353(*---------------------------------------------------------------------------*)
354
355Definition ball :
356 B(m)(x,e) = \y. (dist m)(x,y) < e
357End
358
359(* for HOL Light compatibility *)
360Overload mball[inferior] = “B”;
361
362Theorem BALL_OPEN:
363 !m:('a)metric. !x e. &0 < e ==> open_in(mtop(m))(B(m)(x,e))
364Proof
365 REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[MTOP_OPEN] THEN
366 X_GEN_TAC “z:'a” THEN REWRITE_TAC[ball] THEN BETA_TAC THEN
367 DISCH_THEN(ASSUME_TAC o ONCE_REWRITE_RULE[GSYM REAL_SUB_LT]) THEN
368 EXISTS_TAC “e - dist(m:('a)metric)(x,z)” THEN ASM_REWRITE_TAC[] THEN
369 X_GEN_TAC “y:'a” THEN REWRITE_TAC[REAL_LT_SUB_LADD] THEN
370 ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN DISCH_TAC THEN
371 MATCH_MP_TAC REAL_LET_TRANS THEN
372 EXISTS_TAC “dist(m)(x:'a,z) + dist(m)(z,y)” THEN
373 ASM_REWRITE_TAC[METRIC_TRIANGLE]
374QED
375
376(* NOTE: In HOL-Light, a metric m is a pair whose FST (‘mspace m’) is equal to
377 ‘topspace (mtop m)’. But in HOL4, this ‘mspace m’ is always UNIV.
378
379 However, HOL4 users can construct a subtopology generated by ‘mtop m’ but is
380 restricted to ‘sp = mspace m’ from HOL-Light, i.e. ‘subtopology (mtop m) sp’.
381
382 Adding this theorem into [simp] is not a good idea.
383 *)
384Theorem TOPSPACE_MTOP :
385 topspace (mtop m) = UNIV
386Proof
387 simp[topspace, EXTENSION] >> csimp[IN_DEF] >> qx_gen_tac ‘x’ >>
388 qexists_tac ‘B(m)(x,1)’ >> simp[BALL_OPEN] >>
389 simp[ball, METRIC_SAME]
390QED
391
392Theorem MSPACE :
393 !m. mspace m = UNIV
394Proof
395 REWRITE_TAC [mspace, TOPSPACE_MTOP]
396QED
397
398Theorem BALL_NEIGH:
399 !m:('a)metric. !x e. &0 < e ==> neigh(mtop(m))(B(m)(x,e),x)
400Proof
401 REPEAT GEN_TAC THEN DISCH_TAC THEN
402 REWRITE_TAC[neigh] THEN EXISTS_TAC “B(m)(x:'a,e)” THEN
403 REWRITE_TAC[SUBSET_REFL, TOPSPACE_MTOP, SUBSET_UNIV] THEN CONJ_TAC THENL
404 [MATCH_MP_TAC BALL_OPEN,
405 REWRITE_TAC[ball] THEN BETA_TAC THEN REWRITE_TAC[METRIC_SAME]] THEN
406 POP_ASSUM ACCEPT_TAC
407QED
408
409(*---------------------------------------------------------------------------*)
410(* HOL-Light compatibile theorems (MDIST_) *)
411(*---------------------------------------------------------------------------*)
412
413Theorem MDIST_REFL = METRIC_SAME
414Theorem MDIST_SYM = METRIC_SYM
415Theorem MDIST_TRIANGLE = METRIC_TRIANGLE
416
417Theorem MDIST_TRIANGLE_SUB :
418 !m x y z. mdist m (x,y) - mdist m (y,z) <= mdist m (x,z)
419Proof
420 RW_TAC std_ss [REAL_LE_SUB_RADD]
421 >> ‘dist m (y,z) = dist m (z,y)’ by rw [METRIC_SYM] >> POP_ORW
422 >> rw [MDIST_TRIANGLE]
423QED
424
425Theorem MDIST_POS_LE = METRIC_POS
426Theorem MDIST_POS_LT = METRIC_NZ
427Theorem MDIST_EQ_0 = METRIC_ZERO
428
429Theorem MDIST_POS_EQ :
430 !m x y. 0 < dist m (x,y) <=> x <> y
431Proof
432 METIS_TAC [MDIST_POS_LT, MDIST_REFL, REAL_LT_REFL]
433QED
434
435Theorem mtopology :
436 !m. mtopology (m:'a metric) =
437 topology {u | u SUBSET mspace m /\
438 !x:'a. x IN u ==> ?r. &0 < r /\ mball m (x,r) SUBSET u}
439Proof
440 rw [mtop, MSPACE, ball]
441 >> AP_TERM_TAC
442 >> rw [Once EXTENSION, IN_APP, SUBSET_DEF]
443QED
444
445Theorem mball :
446 !m x r. mball m (x:'a,r) =
447 {y | x IN mspace m /\ y IN mspace m /\ mdist m (x,y) < r}
448Proof
449 rw [MSPACE, ball, Once EXTENSION]
450QED
451
452Theorem IS_TOPOLOGY_METRIC_TOPOLOGY :
453 !m. istopology {u | u SUBSET mspace m /\
454 !x:'a. x IN u ==> ?r. &0 < r /\ mball m (x,r) SUBSET u}
455Proof
456 GEN_TAC
457 >> Q_TAC SUFF_TAC
458 ‘{u | u SUBSET mspace m /\
459 !x:'a. x IN u ==> ?r. &0 < r /\ mball m (x,r) SUBSET u} =
460 (\S'. !x. S' x ==> ?e. 0 < e /\ !y. dist m (x,y) < e ==> S' y)’
461 >- (DISCH_THEN (ONCE_REWRITE_TAC o wrap) \\
462 REWRITE_TAC [mtop_istopology])
463 >> rw [MSPACE, ball, SUBSET_DEF, IN_APP, Once EXTENSION]
464QED
465
466Theorem OPEN_IN_MTOPOLOGY :
467 !(m:'a metric) u.
468 open_in (mtopology m) u <=>
469 u SUBSET mspace m /\
470 (!x. x IN u ==> ?r. &0 < r /\ mball m (x,r) SUBSET u)
471Proof
472 rw [MTOP_OPEN, MSPACE, ball, SUBSET_DEF, IN_APP]
473QED
474
475Theorem IN_MBALL :
476 !m x (y:'a) r.
477 y IN mball m (x,r) <=>
478 x IN mspace m /\ y IN mspace m /\ mdist m (x,y) < r
479Proof
480 rw [mball]
481QED
482
483Theorem CENTRE_IN_MBALL :
484 !m (x:'a) r. &0 < r /\ x IN mspace m ==> x IN mball m (x,r)
485Proof
486 SIMP_TAC std_ss[IN_MBALL, MDIST_REFL, real_gt]
487QED
488
489Theorem CENTRE_IN_MBALL_EQ :
490 !m (x:'a) r. x IN mball m (x,r) <=> x IN mspace m /\ &0 < r
491Proof
492 REPEAT GEN_TAC THEN REWRITE_TAC[IN_MBALL] THEN
493 ASM_CASES_TAC “(x:'a) IN mspace m” THEN ASM_REWRITE_TAC[] THEN
494 ASM_SIMP_TAC std_ss[MDIST_REFL]
495QED
496
497Theorem MBALL_SUBSET_MSPACE :
498 !m (x:'a) r. mball m (x,r) SUBSET mspace m
499Proof
500 SIMP_TAC std_ss[SUBSET_DEF, IN_MBALL]
501QED
502
503Theorem MBALL_EMPTY :
504 !m (x:'a) r. r <= &0 ==> mball m (x,r) = {}
505Proof
506 REWRITE_TAC [IN_MBALL, Once EXTENSION, NOT_IN_EMPTY] THEN
507 MESON_TAC[MDIST_POS_LE, REAL_ARITH “!x. ~(r <= &0 /\ &0 <= x /\ x < r)”]
508QED
509
510Theorem OPEN_IN_MBALL :
511 !m (x:'a) r. open_in (mtopology m) (mball m (x,r))
512Proof
513 REPEAT GEN_TAC THEN ASM_CASES_TAC “&0 < (r:real)” THENL
514 [ALL_TAC, ASM_SIMP_TAC std_ss[MBALL_EMPTY, GSYM REAL_NOT_LT, OPEN_IN_EMPTY]] THEN
515 REWRITE_TAC[OPEN_IN_MTOPOLOGY, MBALL_SUBSET_MSPACE, IN_MBALL, SUBSET_DEF]
516 >> Q.X_GEN_TAC ‘y’ >> STRIP_TAC
517 >> ASM_REWRITE_TAC[]
518 >> EXISTS_TAC “r - mdist m (x:'a,y)” >> CONJ_TAC
519 >- ASM_REAL_ARITH_TAC
520 >> Q.X_GEN_TAC ‘z’
521 >> STRIP_TAC
522 >> ASM_REWRITE_TAC[]
523 >> TRANS_TAC REAL_LET_TRANS “mdist m (x:'a,y) + mdist m (y,z)”
524 >> ASM_SIMP_TAC std_ss[MDIST_TRIANGLE]
525 >> ASM_REAL_ARITH_TAC
526QED
527
528(*---------------------------------------------------------------------------*)
529(* Characterize limit point in a metric topology *)
530(*---------------------------------------------------------------------------*)
531
532Theorem MTOP_LIMPT:
533 !m:('a)metric x S'.
534 limpt(mtop m) x S' <=>
535 !e. &0 < e ==> ?y. ~(x = y) /\ S' y /\ (dist m)(x,y) < e
536Proof
537 REPEAT GEN_TAC THEN REWRITE_TAC[limpt] THEN EQ_TAC THENL
538 [STRIP_TAC THEN
539 Q.X_GEN_TAC ‘e’ THEN STRIP_TAC THEN
540 FIRST_X_ASSUM (Q.SPEC_THEN ‘B(m)(x,e)’ MP_TAC) THEN
541 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP BALL_NEIGH th]) THEN
542 REWRITE_TAC[ball] THEN BETA_TAC THEN DISCH_THEN ACCEPT_TAC,
543 STRIP_TAC THEN CONJ_TAC THEN1 ASM_REWRITE_TAC[TOPSPACE_MTOP,IN_UNIV] THEN
544 GEN_TAC THEN REWRITE_TAC[neigh] THEN
545 DISCH_THEN(X_CHOOSE_THEN “P:'a->bool”
546 (CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC)) THEN
547 REWRITE_TAC[MTOP_OPEN] THEN
548 DISCH_THEN(MP_TAC o SPEC “x:'a”) THEN ASM_REWRITE_TAC[] THEN
549 DISCH_THEN(X_CHOOSE_THEN “e:real” (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
550 FIRST_ASSUM(UNDISCH_TAC o assert is_forall o concl) THEN
551 DISCH_THEN(MP_TAC o SPEC “e:real”) THEN ASM_REWRITE_TAC[] THEN
552 DISCH_THEN(X_CHOOSE_THEN “y:'a” STRIP_ASSUME_TAC) THEN
553 DISCH_THEN(MP_TAC o SPEC “y:'a”) THEN ASM_REWRITE_TAC[] THEN
554 DISCH_TAC THEN EXISTS_TAC “y:'a” THEN ASM_REWRITE_TAC[] THEN
555 UNDISCH_TAC “(P:'a->bool) SUBSET N” THEN
556 REWRITE_TAC[SUBSET_applied] THEN DISCH_THEN MATCH_MP_TAC THEN
557 FIRST_ASSUM ACCEPT_TAC
558 ]
559QED
560
561Theorem MTOP_LIMPT' :
562 !m x s. limpt(mtop m) x s <=>
563 !e. 0 < e ==> ?y. x <> y /\ y IN s /\ dist m (x,y) < e
564Proof
565 RW_TAC std_ss [IN_APP, MTOP_LIMPT]
566QED
567
568(*---------------------------------------------------------------------------*)
569(* Define the usual metric on the real line *)
570(*---------------------------------------------------------------------------*)
571
572Theorem ISMET_R1:
573 ismet (\(x,y). abs(y - x:real))
574Proof
575 REWRITE_TAC[ismet] THEN CONV_TAC(ONCE_DEPTH_CONV PAIRED_BETA_CONV) THEN
576 CONJ_TAC THEN REPEAT GEN_TAC THENL
577 [REWRITE_TAC[ABS_ZERO, REAL_SUB_0] THEN
578 CONV_TAC(RAND_CONV SYM_CONV) THEN REFL_TAC,
579 SUBST1_TAC(SYM(SPECL [“x:real”, “y:real”] REAL_NEG_SUB)) THEN
580 REWRITE_TAC[ABS_NEG] THEN
581 SUBGOAL_THEN “z - y:real = (x - y) + (z - x)”
582 (fn th => SUBST1_TAC th THEN MATCH_ACCEPT_TAC ABS_TRIANGLE) THEN
583 REWRITE_TAC[real_sub] THEN
584 ONCE_REWRITE_TAC[AC(REAL_ADD_ASSOC,REAL_ADD_SYM)
585 “(a + b) + (c + d) = (d + a) + (c + b):real”] THEN
586 REWRITE_TAC[REAL_ADD_LINV, REAL_ADD_LID]]
587QED
588
589Definition mr1 :
590 mr1 = metric(\(x,y). abs(y - x))
591End
592
593Theorem MR1_DEF:
594 !x y. (dist mr1)(x,y) = abs(y - x)
595Proof
596 REPEAT GEN_TAC THEN REWRITE_TAC[mr1, REWRITE_RULE[metric_tybij] ISMET_R1]
597 THEN CONV_TAC(ONCE_DEPTH_CONV PAIRED_BETA_CONV) THEN REFL_TAC
598QED
599
600Theorem MR1_ADD:
601 !x d. (dist mr1)(x,x + d) = abs(d)
602Proof
603 REPEAT GEN_TAC THEN REWRITE_TAC[MR1_DEF, REAL_ADD_SUB]
604QED
605
606Theorem MR1_SUB:
607 !x d. (dist mr1)(x,x - d) = abs(d)
608Proof
609 REPEAT GEN_TAC THEN REWRITE_TAC[MR1_DEF, REAL_SUB_SUB, ABS_NEG]
610QED
611
612Theorem MR1_ADD_POS:
613 !x d. &0 <= d ==> ((dist mr1)(x,x + d) = d)
614Proof
615 REPEAT GEN_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[MR1_ADD, abs]
616QED
617
618Theorem MR1_SUB_LE:
619 !x d. &0 <= d ==> ((dist mr1)(x,x - d) = d)
620Proof
621 REPEAT GEN_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[MR1_SUB, abs]
622QED
623
624Theorem MR1_ADD_LT:
625 !x d. &0 < d ==> ((dist mr1)(x,x + d) = d)
626Proof
627 REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP REAL_LT_IMP_LE) THEN
628 MATCH_ACCEPT_TAC MR1_ADD_POS
629QED
630
631Theorem MR1_SUB_LT:
632 !x d. &0 < d ==> ((dist mr1)(x,x - d) = d)
633Proof
634 REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP REAL_LT_IMP_LE) THEN
635 MATCH_ACCEPT_TAC MR1_SUB_LE
636QED
637
638Theorem MR1_BETWEEN1:
639 !x y z. x < z /\ (dist mr1)(x,y) < (z - x) ==> y < z
640Proof
641 REPEAT GEN_TAC THEN REWRITE_TAC[MR1_DEF, ABS_BETWEEN1]
642QED
643
644(*---------------------------------------------------------------------------*)
645(* Every real is a limit point of the real line *)
646(*---------------------------------------------------------------------------*)
647
648Theorem MR1_LIMPT:
649 !x. limpt(mtop mr1) x univ(:real)
650Proof
651 GEN_TAC THEN REWRITE_TAC[MTOP_LIMPT, UNIV_DEF] THEN
652 X_GEN_TAC “e:real” THEN DISCH_TAC THEN
653 EXISTS_TAC “x + (e / &2)” THEN
654 REWRITE_TAC[MR1_ADD] THEN
655 SUBGOAL_THEN “&0 <= (e / &2)” ASSUME_TAC THENL
656 [MATCH_MP_TAC REAL_LT_IMP_LE THEN
657 ASM_REWRITE_TAC[REAL_LT_HALF1], ALL_TAC] THEN
658 ASM_REWRITE_TAC[abs, REAL_LT_HALF2] THEN
659 CONV_TAC(RAND_CONV SYM_CONV) THEN
660 REWRITE_TAC[REAL_ADD_RID_UNIQ] THEN
661 CONV_TAC(RAND_CONV SYM_CONV) THEN
662 MATCH_MP_TAC REAL_LT_IMP_NE THEN
663 ASM_REWRITE_TAC[REAL_LT_HALF1]
664QED
665
666(* ------------------------------------------------------------------------- *)
667(* Metric function for R^1. *)
668(* ------------------------------------------------------------------------- *)
669
670(* new definition based on metricTheory *)
671Definition dist_def :
672 real_dist = dist mr1
673End
674
675(* old definition (now becomes a theorem) *)
676Theorem dist :
677 !x y. real_dist(x:real,y:real) = abs(x - y)
678Proof
679 RW_TAC std_ss [dist_def, MR1_DEF]
680 >> REAL_ARITH_TAC
681QED
682
683Overload dist = “real_dist”;
684
685Theorem DIST_REFL:
686 !x. dist(x,x) = &0
687Proof
688 SIMP_TAC std_ss [dist] THEN REAL_ARITH_TAC
689QED
690
691Theorem DIST_SYM:
692 !x y. dist(x,y) = dist(y,x)
693Proof
694 SIMP_TAC std_ss [dist] THEN REAL_ARITH_TAC
695QED
696
697Theorem DIST_TRIANGLE:
698 !x:real y z. dist(x,z) <= dist(x,y) + dist(y,z)
699Proof
700 SIMP_TAC std_ss [dist] THEN REAL_ARITH_TAC
701QED
702
703Theorem DIST_TRIANGLE_ALT:
704 !x y z. dist(y,z) <= dist(x,y) + dist(x,z)
705Proof
706 SIMP_TAC std_ss [dist] THEN REAL_ARITH_TAC
707QED
708
709Theorem DIST_EQ_0:
710 !x y. (dist(x,y) = 0:real) <=> (x = y)
711Proof
712 SIMP_TAC std_ss [dist] THEN REAL_ARITH_TAC
713QED
714
715Theorem DIST_POS_LT:
716 !x y. ~(x = y) ==> &0 < dist(x,y)
717Proof
718 SIMP_TAC std_ss [dist] THEN REAL_ARITH_TAC
719QED
720
721Theorem DIST_NZ:
722 !x y. ~(x = y) <=> &0 < dist(x,y)
723Proof
724 SIMP_TAC std_ss [dist] THEN REAL_ARITH_TAC
725QED
726
727Theorem DIST_TRIANGLE_LE:
728 !x y z e. dist(x,z) + dist(y,z) <= e ==> dist(x,y) <= e
729Proof
730 SIMP_TAC std_ss [dist] THEN REAL_ARITH_TAC
731QED
732
733Theorem DIST_TRIANGLE_LT:
734 !x y z e. dist(x,z) + dist(y,z) < e ==> dist(x,y) < e
735Proof
736 SIMP_TAC std_ss [dist] THEN REAL_ARITH_TAC
737QED
738
739Theorem DIST_TRIANGLE_HALF_L:
740 !x1 x2 y. dist(x1,y) < e / &2 /\ dist(x2,y) < e / &2 ==> dist(x1,x2) < e
741Proof
742 REPEAT STRIP_TAC THEN KNOW_TAC `` dist (x1,y) + dist (x2,y) < e`` THENL
743 [METIS_TAC [REAL_LT_ADD2, REAL_HALF_DOUBLE],
744 DISCH_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN
745 EXISTS_TAC ``dist (x1,y) + dist (x2,y)`` THEN
746 METIS_TAC [DIST_TRIANGLE, DIST_SYM]]
747QED
748
749Theorem DIST_TRIANGLE_HALF_R:
750 !x1 x2 y. dist(y,x1) < e / &2 /\ dist(y,x2) < e / &2 ==> dist(x1,x2) < e
751Proof
752 REPEAT STRIP_TAC THEN KNOW_TAC `` dist (y, x1) + dist (y, x2) < e`` THENL
753 [METIS_TAC [REAL_LT_ADD2, REAL_HALF_DOUBLE],
754 DISCH_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN
755 EXISTS_TAC ``dist (y, x1) + dist (y, x2)`` THEN
756 METIS_TAC [DIST_TRIANGLE, DIST_SYM]]
757QED
758
759Theorem DIST_TRIANGLE_ADD:
760 !x x' y y'. dist(x + y,x' + y') <= dist(x,x') + dist(y,y')
761Proof
762 SIMP_TAC std_ss [dist] THEN REAL_ARITH_TAC
763QED
764
765Theorem DIST_ADD :
766 !x y c. dist (x + c,y + c) = dist (x,y)
767Proof
768 RW_TAC std_ss [dist] >> REAL_ARITH_TAC
769QED
770
771Theorem DIST_MUL:
772 !x y c. dist(c * x,c * y) = abs(c) * dist(x,y)
773Proof
774 REWRITE_TAC[dist, GSYM ABS_MUL] THEN REAL_ARITH_TAC
775QED
776
777Theorem DIST_TRIANGLE_ADD_HALF:
778 !x x' y y':real.
779 dist(x,x') < e / &2 /\ dist(y,y') < e / &2 ==> dist(x + y,x' + y') < e
780Proof
781 REPEAT STRIP_TAC THEN KNOW_TAC `` dist (x, x') + dist (y, y') < e`` THENL
782 [METIS_TAC [REAL_LT_ADD2, REAL_HALF_DOUBLE],
783 DISCH_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN
784 EXISTS_TAC ``dist (x, x') + dist (y, y')`` THEN
785 METIS_TAC [DIST_TRIANGLE_ADD, DIST_SYM]]
786QED
787
788Theorem DIST_LE_0:
789 !x y. dist(x,y) <= &0 <=> (x = y)
790Proof
791 SIMP_TAC std_ss [dist] THEN REAL_ARITH_TAC
792QED
793
794Theorem DIST_POS_LE:
795 !x y. &0 <= dist(x,y)
796Proof
797 METIS_TAC [DIST_EQ_0, DIST_NZ, REAL_LE_LT]
798QED
799
800Theorem DIST_EQ:
801 !w x y z. (dist(w,x) = dist(y,z)) <=> (dist(w,x) pow 2 = dist(y,z) pow 2)
802Proof
803 REPEAT GEN_TAC THEN EQ_TAC THENL [RW_TAC std_ss [],
804 DISCH_TAC THEN MATCH_MP_TAC POW_EQ THEN EXISTS_TAC ``1:num`` THEN
805 RW_TAC arith_ss [DIST_POS_LE]]
806QED
807
808Theorem DIST_0:
809 !x. (dist(x,0) = abs(x)) /\ (dist(0,x) = abs(x))
810Proof
811 RW_TAC arith_ss [dist, REAL_SUB_RZERO, REAL_SUB_LZERO, ABS_NEG]
812QED
813
814Theorem REAL_CHOOSE_DIST:
815 !x e. &0 <= e ==> (?y. dist (x,y) = e)
816Proof
817 REPEAT STRIP_TAC THEN EXISTS_TAC ``x - e:real`` THEN
818 ASM_REWRITE_TAC [dist, REAL_SUB_SUB2, ABS_REFL]
819QED
820
821(* ------------------------------------------------------------------------- *)
822(* F_sigma and G_delta sets in a topological space (ported from HOL Light) *)
823(* ------------------------------------------------------------------------- *)
824
825(* The countable intersection class (general version)
826
827 The leading letter G is from the German word "Gebiet" meaning "region".
828 The greek letter "delta" stands for a countable intersection (in German,
829 "Durchschnitt"). See [1, p.310] (bibitem is at the bottom of this file.)
830
831 NOTE: the part ‘relative_to topspace top’ is necessary when ‘topspace top’
832 is not UNIV, because "a countable intersection of something" includes "a
833 countable intersection of nothing", and ‘BIGINTER {} = UNIV’, which may
834 go beyond the scope of ‘topspace top’. -- Chun Tian, 28 nov 2021
835 *)
836Definition gdelta_in :
837 gdelta_in (top:'a topology) =
838 (COUNTABLE INTERSECTION_OF open_in top) relative_to topspace top
839End
840
841(* The countable union class (general version)
842
843 The leading letter F is from the French word "ferme" meaning "closed".
844 The greek letter "sigma" stands for a countable union or sum (in German,
845 "Summe").
846 *)
847Definition fsigma_in :
848 fsigma_in (top:'a topology) = COUNTABLE UNION_OF closed_in top
849End
850
851Theorem FSIGMA_IN_ASCENDING :
852 !top s:'a->bool.
853 fsigma_in top s <=>
854 ?c. (!n. closed_in top (c n)) /\
855 (!n. c n SUBSET c(n + 1)) /\
856 UNIONS {c n | n IN univ(:num)} = s
857Proof
858 REWRITE_TAC[fsigma_in] THEN
859 SIMP_TAC std_ss [COUNTABLE_UNION_OF_ASCENDING, CLOSED_IN_EMPTY, CLOSED_IN_UNION] THEN
860 REWRITE_TAC[ADD1]
861QED
862
863Theorem GDELTA_IN_ALT :
864 !top s:'a->bool.
865 gdelta_in top s <=>
866 s SUBSET topspace top /\ (COUNTABLE INTERSECTION_OF open_in top) s
867Proof
868 SIMP_TAC std_ss [COUNTABLE_INTERSECTION_OF_RELATIVE_TO_ALT, gdelta_in,
869 OPEN_IN_TOPSPACE, simpLib.AC CONJ_ASSOC CONJ_COMM]
870QED
871
872Theorem FSIGMA_IN_SUBSET :
873 !top s:'a->bool. fsigma_in top s ==> s SUBSET topspace top
874Proof
875 GEN_TAC THEN SIMP_TAC std_ss [fsigma_in, FORALL_UNION_OF, UNIONS_SUBSET] THEN
876 SIMP_TAC std_ss [CLOSED_IN_SUBSET]
877QED
878
879Theorem GDELTA_IN_SUBSET :
880 !top s:'a->bool. gdelta_in top s ==> s SUBSET topspace top
881Proof
882 SIMP_TAC std_ss [GDELTA_IN_ALT]
883QED
884
885Theorem CLOSED_IMP_FSIGMA_IN :
886 !top s:'a->bool. closed_in top s ==> fsigma_in top s
887Proof
888 SIMP_TAC std_ss [fsigma_in, COUNTABLE_UNION_OF_INC]
889QED
890
891Theorem OPEN_IMP_GDELTA_IN :
892 !top s:'a->bool. open_in top s ==> gdelta_in top s
893Proof
894 REPEAT STRIP_TAC THEN REWRITE_TAC[gdelta_in] THEN
895 FIRST_ASSUM(SUBST1_TAC o MATCH_MP (SET_RULE ``s SUBSET u ==> s = u INTER s``) o
896 MATCH_MP OPEN_IN_SUBSET) THEN
897 MATCH_MP_TAC RELATIVE_TO_INC THEN
898 ASM_SIMP_TAC std_ss [COUNTABLE_INTERSECTION_OF_INC]
899QED
900
901Theorem FSIGMA_IN_EMPTY :
902 !top:'a topology. fsigma_in top {}
903Proof
904 SIMP_TAC std_ss [CLOSED_IMP_FSIGMA_IN, CLOSED_IN_EMPTY]
905QED
906
907Theorem GDELTA_IN_EMPTY :
908 !top:'a topology. gdelta_in top {}
909Proof
910 SIMP_TAC std_ss [OPEN_IMP_GDELTA_IN, OPEN_IN_EMPTY]
911QED
912
913Theorem FSIGMA_IN_TOPSPACE :
914 !top:'a topology. fsigma_in top (topspace top)
915Proof
916 SIMP_TAC std_ss [CLOSED_IMP_FSIGMA_IN, CLOSED_IN_TOPSPACE]
917QED
918
919Theorem GDELTA_IN_TOPSPACE :
920 !top:'a topology. gdelta_in top (topspace top)
921Proof
922 SIMP_TAC std_ss [OPEN_IMP_GDELTA_IN, OPEN_IN_TOPSPACE]
923QED
924
925Theorem FSIGMA_IN_UNIONS :
926 !top t:('a->bool)->bool.
927 COUNTABLE t /\ (!s. s IN t ==> fsigma_in top s)
928 ==> fsigma_in top (UNIONS t)
929Proof
930 REWRITE_TAC[fsigma_in, COUNTABLE_UNION_OF_UNIONS]
931QED
932
933Theorem FSIGMA_IN_UNION :
934 !top s t:'a->bool.
935 fsigma_in top s /\ fsigma_in top t ==> fsigma_in top (s UNION t)
936Proof
937 REWRITE_TAC[fsigma_in, COUNTABLE_UNION_OF_UNION]
938QED
939
940Theorem FSIGMA_IN_INTER :
941 !top s t:'a->bool.
942 fsigma_in top s /\ fsigma_in top t ==> fsigma_in top (s INTER t)
943Proof
944 GEN_TAC THEN REWRITE_TAC[fsigma_in] THEN
945 MATCH_MP_TAC COUNTABLE_UNION_OF_INTER THEN
946 REWRITE_TAC[CLOSED_IN_INTER]
947QED
948
949Theorem GDELTA_IN_INTERS :
950 !top t:('a->bool)->bool.
951 COUNTABLE t /\ ~(t = {}) /\ (!s. s IN t ==> gdelta_in top s)
952 ==> gdelta_in top (INTERS t)
953Proof
954 REWRITE_TAC[GDELTA_IN_ALT] THEN REPEAT STRIP_TAC THEN
955 ASM_SIMP_TAC std_ss [INTERS_SUBSET] THEN
956 ASM_SIMP_TAC std_ss [COUNTABLE_INTERSECTION_OF_INTERS]
957QED
958
959Theorem GDELTA_IN_INTER :
960 !top s t:'a->bool.
961 gdelta_in top s /\ gdelta_in top t ==> gdelta_in top (s INTER t)
962Proof
963 SIMP_TAC std_ss [GSYM INTERS_2, GDELTA_IN_INTERS, COUNTABLE_INSERT, COUNTABLE_EMPTY,
964 NOT_INSERT_EMPTY, FORALL_IN_INSERT, NOT_IN_EMPTY]
965QED
966
967Theorem GDELTA_IN_UNION :
968 !top s t:'a->bool.
969 gdelta_in top s /\ gdelta_in top t ==> gdelta_in top (s UNION t)
970Proof
971 SIMP_TAC std_ss [GDELTA_IN_ALT, UNION_SUBSET] THEN
972 MESON_TAC[COUNTABLE_INTERSECTION_OF_UNION, OPEN_IN_UNION]
973QED
974
975Theorem FSIGMA_IN_DIFF :
976 !top s t:'a->bool.
977 fsigma_in top s /\ gdelta_in top t ==> fsigma_in top (s DIFF t)
978Proof
979 GEN_TAC THEN SUBGOAL_THEN
980 ``!s:'a->bool. gdelta_in top s ==> fsigma_in top (topspace top DIFF s)``
981 ASSUME_TAC THENL
982 [ (* goal 1 (of 2) *)
983 SIMP_TAC std_ss [fsigma_in, gdelta_in, FORALL_RELATIVE_TO] THEN
984 SIMP_TAC std_ss [FORALL_INTERSECTION_OF, DIFF_INTERS, SET_RULE
985 ``s DIFF (s INTER t) = s DIFF t``] THEN
986 REPEAT STRIP_TAC THEN MATCH_MP_TAC COUNTABLE_UNION_OF_UNIONS THEN
987 ASM_SIMP_TAC std_ss [SIMPLE_IMAGE, COUNTABLE_IMAGE, FORALL_IN_IMAGE] THEN
988 ASM_SIMP_TAC std_ss [COUNTABLE_UNION_OF_INC, CLOSED_IN_DIFF,
989 CLOSED_IN_TOPSPACE],
990 (* goal 2 (of 2) *)
991 REPEAT STRIP_TAC THEN
992 SUBGOAL_THEN ``s DIFF t:'a->bool = s INTER (topspace top DIFF t)``
993 (fn th => SUBST1_TAC th THEN ASM_SIMP_TAC std_ss [FSIGMA_IN_INTER]) THEN
994 FIRST_ASSUM(MP_TAC o MATCH_MP FSIGMA_IN_SUBSET) THEN ASM_SET_TAC[] ]
995QED
996
997Theorem GDELTA_IN_DIFF :
998 !top s t:'a->bool.
999 gdelta_in top s /\ fsigma_in top t ==> gdelta_in top (s DIFF t)
1000Proof
1001 GEN_TAC THEN SUBGOAL_THEN
1002 ``!s:'a->bool. fsigma_in top s ==> gdelta_in top (topspace top DIFF s)``
1003 ASSUME_TAC THENL
1004 [ (* goal 1 (of 2) *)
1005 SIMP_TAC std_ss [fsigma_in, gdelta_in, FORALL_UNION_OF, DIFF_UNIONS] THEN
1006 REPEAT STRIP_TAC THEN MATCH_MP_TAC RELATIVE_TO_INC THEN
1007 MATCH_MP_TAC COUNTABLE_INTERSECTION_OF_INTERS THEN
1008 ASM_SIMP_TAC std_ss [SIMPLE_IMAGE, COUNTABLE_IMAGE, FORALL_IN_IMAGE] THEN
1009 ASM_SIMP_TAC std_ss [COUNTABLE_INTERSECTION_OF_INC, OPEN_IN_DIFF,
1010 OPEN_IN_TOPSPACE],
1011 (* goal 2 (of 2) *)
1012 REPEAT STRIP_TAC THEN
1013 SUBGOAL_THEN ``s DIFF t:'a->bool = s INTER (topspace top DIFF t)``
1014 (fn th => SUBST1_TAC th THEN ASM_SIMP_TAC std_ss [GDELTA_IN_INTER]) THEN
1015 FIRST_ASSUM(MP_TAC o MATCH_MP GDELTA_IN_SUBSET) THEN ASM_SET_TAC[] ]
1016QED
1017
1018Theorem GDELTA_IN_FSIGMA_IN :
1019 !top s:'a->bool.
1020 gdelta_in top s <=>
1021 s SUBSET topspace top /\ fsigma_in top (topspace top DIFF s)
1022Proof
1023 REPEAT GEN_TAC THEN EQ_TAC THEN
1024 SIMP_TAC std_ss [GDELTA_IN_SUBSET, FSIGMA_IN_DIFF, FSIGMA_IN_TOPSPACE] THEN
1025 STRIP_TAC THEN FIRST_ASSUM(SUBST1_TAC o MATCH_MP (SET_RULE
1026 ``s SUBSET u ==> s = u DIFF (u DIFF s)``)) THEN
1027 ASM_SIMP_TAC std_ss [GDELTA_IN_DIFF, GDELTA_IN_TOPSPACE]
1028QED
1029
1030Theorem FSIGMA_IN_GDELTA_IN :
1031 !top s:'a->bool.
1032 fsigma_in top s <=>
1033 s SUBSET topspace top /\ gdelta_in top (topspace top DIFF s)
1034Proof
1035 REPEAT GEN_TAC THEN EQ_TAC THEN
1036 SIMP_TAC std_ss [FSIGMA_IN_SUBSET, GDELTA_IN_DIFF, GDELTA_IN_TOPSPACE] THEN
1037 STRIP_TAC THEN FIRST_ASSUM(SUBST1_TAC o MATCH_MP (SET_RULE
1038 ``s SUBSET u ==> s = u DIFF (u DIFF s)``)) THEN
1039 ASM_SIMP_TAC std_ss [FSIGMA_IN_DIFF, FSIGMA_IN_TOPSPACE]
1040QED
1041
1042Theorem GDELTA_IN_DESCENDING :
1043 !top s:'a->bool.
1044 gdelta_in top s <=>
1045 ?c. (!n. open_in top (c n)) /\
1046 (!n. c(n + 1) SUBSET c n) /\
1047 INTERS {c n | n IN univ(:num)} = s
1048Proof
1049 REPEAT GEN_TAC THEN REWRITE_TAC[GDELTA_IN_FSIGMA_IN] THEN
1050 REWRITE_TAC[FSIGMA_IN_ASCENDING] THEN EQ_TAC THENL
1051 [ (* goal 1 (of 2) *)
1052 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC
1053 (Q.X_CHOOSE_THEN `c:num->'a->bool` STRIP_ASSUME_TAC)),
1054 (* goal 2 (of 2) *)
1055 DISCH_THEN(Q.X_CHOOSE_THEN `c:num->'a->bool` STRIP_ASSUME_TAC) THEN
1056 CONJ_TAC THENL
1057 [ FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN MATCH_MP_TAC INTERS_SUBSET THEN
1058 ASM_SIMP_TAC std_ss [OPEN_IN_SUBSET, FORALL_IN_GSPEC] THEN SET_TAC[],
1059 ALL_TAC ] ] THEN
1060 Q.EXISTS_TAC `\n. topspace top DIFF (c:num->'a->bool) n` THEN
1061 ASM_SIMP_TAC std_ss [OPEN_IN_DIFF, CLOSED_IN_DIFF, OPEN_IN_TOPSPACE,
1062 CLOSED_IN_TOPSPACE, SET_RULE ``s SUBSET t ==> u DIFF t SUBSET u DIFF s``]
1063 THENL
1064 [ (* goal 1 (of 2) *)
1065 FIRST_X_ASSUM(MP_TAC o MATCH_MP (SET_RULE
1066 ``u = t DIFF s ==> s SUBSET t ==> s = t DIFF u``)) THEN
1067 ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN
1068 REWRITE_TAC[DIFF_UNIONS],
1069 (* goal 2 (of 2) *)
1070 FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN REWRITE_TAC[DIFF_INTERS] ] THEN
1071 SIMP_TAC std_ss [SET_RULE ``{g y | y IN {f x | x IN s}} = {g(f x) | x IN s}``] THEN
1072 SIMP_TAC std_ss [SET_RULE ``s = t INTER s <=> s SUBSET t``] THEN
1073 MATCH_MP_TAC INTERS_SUBSET THEN
1074 ASM_SIMP_TAC std_ss [OPEN_IN_SUBSET, FORALL_IN_GSPEC] THEN SET_TAC[]
1075QED
1076
1077Theorem FSIGMA_IN_RELATIVE_TO :
1078 !top s:'a->bool.
1079 (fsigma_in top relative_to s) = fsigma_in (subtopology top s)
1080Proof
1081 REWRITE_TAC[fsigma_in, COUNTABLE_UNION_OF_RELATIVE_TO] THEN
1082 REWRITE_TAC[CLOSED_IN_RELATIVE_TO]
1083QED
1084
1085Theorem FSIGMA_IN_RELATIVE_TO_TOPSPACE :
1086 !top:'a topology. fsigma_in top relative_to (topspace top) = fsigma_in top
1087Proof
1088 rw [FSIGMA_IN_RELATIVE_TO, SUBTOPOLOGY_TOPSPACE]
1089QED
1090
1091Theorem FSIGMA_IN_SUBTOPOLOGY :
1092 !top u s:'a->bool.
1093 fsigma_in (subtopology top u) s <=>
1094 ?t. fsigma_in top t /\ s = t INTER u
1095Proof
1096 REPEAT GEN_TAC THEN REWRITE_TAC[GSYM FSIGMA_IN_RELATIVE_TO] THEN
1097 REWRITE_TAC[relative_to] THEN MESON_TAC[INTER_COMM]
1098QED
1099
1100Theorem GDELTA_IN_RELATIVE_TO :
1101 !top s:'a->bool.
1102 (gdelta_in top relative_to s) = gdelta_in (subtopology top s)
1103Proof
1104 REWRITE_TAC[gdelta_in, RELATIVE_TO_RELATIVE_TO] THEN
1105 ONCE_REWRITE_TAC[COUNTABLE_INTERSECTION_OF_RELATIVE_TO] THEN
1106 REWRITE_TAC[OPEN_IN_RELATIVE_TO] THEN
1107 REWRITE_TAC[SUBTOPOLOGY_SUBTOPOLOGY, TOPSPACE_SUBTOPOLOGY] THEN
1108 SIMP_TAC std_ss [SET_RULE ``s INTER (u INTER s) = u INTER s``]
1109QED
1110
1111Theorem GDELTA_IN_SUBTOPOLOGY :
1112 !top u s:'a->bool.
1113 gdelta_in (subtopology top u) s <=>
1114 ?t. gdelta_in top t /\ s = t INTER u
1115Proof
1116 REPEAT GEN_TAC THEN REWRITE_TAC[GSYM GDELTA_IN_RELATIVE_TO] THEN
1117 REWRITE_TAC[relative_to] THEN MESON_TAC[INTER_COMM]
1118QED
1119
1120Theorem FSIGMA_IN_FSIGMA_SUBTOPOLOGY :
1121 !top s t:'a->bool.
1122 fsigma_in top s
1123 ==> (fsigma_in (subtopology top s) t <=>
1124 fsigma_in top t /\ t SUBSET s)
1125Proof
1126 REPEAT STRIP_TAC THEN REWRITE_TAC[FSIGMA_IN_SUBTOPOLOGY] THEN
1127 EQ_TAC THEN STRIP_TAC THEN ASM_SIMP_TAC std_ss [INTER_SUBSET, FSIGMA_IN_INTER] THEN
1128 Q.EXISTS_TAC `t:'a->bool` THEN ASM_REWRITE_TAC[] THEN ASM_SET_TAC[]
1129QED
1130
1131Theorem GDELTA_IN_GDELTA_SUBTOPOLOGY :
1132 !top s t:'a->bool.
1133 gdelta_in top s
1134 ==> (gdelta_in (subtopology top s) t <=>
1135 gdelta_in top t /\ t SUBSET s)
1136Proof
1137 REPEAT STRIP_TAC THEN REWRITE_TAC[GDELTA_IN_SUBTOPOLOGY] THEN
1138 EQ_TAC THEN STRIP_TAC THEN ASM_SIMP_TAC std_ss [INTER_SUBSET, GDELTA_IN_INTER] THEN
1139 Q.EXISTS_TAC `t:'a->bool` THEN ASM_REWRITE_TAC[] THEN ASM_SET_TAC[]
1140QED
1141
1142(* ------------------------------------------------------------------------- *)
1143(* Metrizable spaces (ported from HOL Light) *)
1144(* ------------------------------------------------------------------------- *)
1145
1146Definition metrizable_space :
1147 metrizable_space top = ?m. top = mtopology m
1148End
1149
1150Theorem METRIZABLE_SPACE_MTOPOLOGY :
1151 !m. metrizable_space (mtopology m)
1152Proof
1153 REWRITE_TAC[metrizable_space] THEN MESON_TAC[]
1154QED
1155
1156Theorem FORALL_METRIC_TOPOLOGY :
1157 !P. (!m:'a metric. P (mtopology m) (mspace m)) <=>
1158 !top. metrizable_space top ==> P top (topspace top)
1159Proof
1160 SIMP_TAC std_ss [metrizable_space, LEFT_IMP_EXISTS_THM, Once TOPSPACE_MTOPOLOGY]
1161QED
1162
1163Theorem FORALL_METRIZABLE_SPACE :
1164 !P. (!top. metrizable_space top ==> P top (topspace top)) <=>
1165 (!m:'a metric. P (mtopology m) (mspace m))
1166Proof
1167 REWRITE_TAC[FORALL_METRIC_TOPOLOGY]
1168QED
1169
1170Theorem EXISTS_METRIZABLE_SPACE :
1171 !P. (?top. metrizable_space top /\ P top (topspace top)) <=>
1172 (?m:'a metric. P (mtopology m) (mspace m))
1173Proof
1174 SIMP_TAC pure_ss [MESON[] ``(?(x :'a metric). P x) <=> ~(!x. ~P x)``] THEN
1175 SIMP_TAC pure_ss [FORALL_METRIC_TOPOLOGY] THEN MESON_TAC[]
1176QED
1177
1178(* key result *)
1179Theorem CLOSED_IMP_GDELTA_IN :
1180 !top s:'a->bool.
1181 metrizable_space top /\ closed_in top s ==> gdelta_in top s
1182Proof
1183 SIMP_TAC std_ss [IMP_CONJ, RIGHT_FORALL_IMP_THM, FORALL_METRIZABLE_SPACE] THEN
1184 REPEAT STRIP_TAC THEN
1185 ASM_CASES_TAC ``s:'a->bool = {}`` THEN ASM_REWRITE_TAC[GDELTA_IN_EMPTY] THEN
1186 SUBGOAL_THEN
1187 ``s:'a->bool =
1188 INTERS
1189 {{x | x IN mspace m /\
1190 ?y. y IN s /\ mdist m (x,y) < inv(&n + &1)} | n IN univ(:num)}``
1191 SUBST1_TAC THENL
1192 [ (* goal 1 (of 2) *)
1193 GEN_REWRITE_TAC I empty_rewrites [EXTENSION] THEN Q.X_GEN_TAC `x:'a` THEN
1194 RW_TAC std_ss [INTERS_GSPEC, IN_UNIV, GSPECIFICATION] THEN EQ_TAC THENL
1195 [ (* goal 1.1 (of 2) *)
1196 DISCH_TAC THEN Q.X_GEN_TAC `n:num` THEN
1197 SUBGOAL_THEN ``(x:'a) IN mspace m`` ASSUME_TAC THENL
1198 [ ASM_MESON_TAC[CLOSED_IN_SUBSET, SUBSET_DEF, TOPSPACE_MTOPOLOGY],
1199 ASM_REWRITE_TAC[] THEN Q.EXISTS_TAC `x:'a` THEN
1200 ASM_SIMP_TAC std_ss [MDIST_REFL, REAL_LT_INV_EQ] THEN rw [] ],
1201 (* goal 1.2 (of 2) *)
1202 ASM_CASES_TAC ``(x:'a) IN mspace m`` THEN ASM_REWRITE_TAC[] THEN
1203 Q.ABBREV_TAC ‘P = \e. ?y. y IN s /\ dist m (x,y) < e’ \\
1204 ASM_SIMP_TAC std_ss [] \\
1205 Q_TAC KNOW_TAC ‘(!n. P (inv (&n + 1))) <=> (!e. 0 < e ==> P e)’
1206 >- (ONCE_REWRITE_TAC [EQ_SYM_EQ] \\
1207 MATCH_MP_TAC FORALL_POS_MONO_1_EQ \\
1208 rw [Abbr ‘P’] >> Q.EXISTS_TAC ‘y’ >> METIS_TAC [REAL_LT_TRANS]) \\
1209 DISCH_THEN (ONCE_REWRITE_TAC o wrap) \\
1210 rw [Abbr ‘P’] \\
1211 FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I empty_rewrites [closed_in]) THEN
1212 REWRITE_TAC[OPEN_IN_MTOPOLOGY, NOT_FORALL_THM, NOT_IMP] THEN
1213 DISCH_THEN(MP_TAC o SPEC ``x:'a`` o CONJUNCT2 o CONJUNCT2) THEN
1214 ASM_REWRITE_TAC[IN_DIFF, TOPSPACE_MTOPOLOGY, SUBSET_DEF, IN_MBALL] THEN
1215 ASM_MESON_TAC[CLOSED_IN_SUBSET, SUBSET_DEF, TOPSPACE_MTOPOLOGY] ],
1216 (* goal 2 (of 2) *)
1217 MATCH_MP_TAC GDELTA_IN_INTERS THEN
1218 SIMP_TAC std_ss [SIMPLE_IMAGE, COUNTABLE_IMAGE, NUM_COUNTABLE] THEN
1219 REWRITE_TAC[IMAGE_EQ_EMPTY, FORALL_IN_IMAGE, UNIV_NOT_EMPTY, IN_UNIV] THEN
1220 Q.X_GEN_TAC `n:num` THEN MATCH_MP_TAC OPEN_IMP_GDELTA_IN THEN
1221 SIMP_TAC std_ss [OPEN_IN_MTOPOLOGY, SUBSET_RESTRICT] THEN
1222 Q.X_GEN_TAC `x:'a` \\
1223 RW_TAC std_ss [GSPECIFICATION] \\
1224 Q.EXISTS_TAC `inv(&n + &1) - mdist m (x:'a,y)` THEN
1225 ASM_SIMP_TAC std_ss [SUBSET_DEF, IN_MBALL, REAL_SUB_LT, GSPECIFICATION] THEN
1226 Q.X_GEN_TAC `z:'a` THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
1227 Q.EXISTS_TAC `y:'a` THEN ASM_REWRITE_TAC[] THEN
1228 ONCE_REWRITE_TAC [METRIC_SYM] \\
1229 MATCH_MP_TAC REAL_LET_TRANS \\
1230 Q.EXISTS_TAC ‘dist m (y,x) + dist m (x,z)’ >> REWRITE_TAC [METRIC_TRIANGLE] \\
1231 ‘y IN mspace m’ (* not really used (in HOL4) *)
1232 by ASM_MESON_TAC[CLOSED_IN_SUBSET, SUBSET_DEF, TOPSPACE_MTOPOLOGY] \\
1233 METIS_TAC [REAL_LT_SUB_LADD, METRIC_SYM, REAL_ADD_COMM] ]
1234QED
1235
1236Theorem OPEN_IMP_FSIGMA_IN :
1237 !top s:'a->bool.
1238 metrizable_space top /\ open_in top s ==> fsigma_in top s
1239Proof
1240 REPEAT STRIP_TAC THEN
1241 ASM_SIMP_TAC std_ss [FSIGMA_IN_GDELTA_IN, OPEN_IN_SUBSET] THEN
1242 MATCH_MP_TAC CLOSED_IMP_GDELTA_IN THEN
1243 ASM_SIMP_TAC std_ss [CLOSED_IN_DIFF, CLOSED_IN_TOPSPACE]
1244QED
1245
1246(*---------------------------------------------------------------------------*)
1247(* Euclidean metric on 2-D real plane (univ(:real) CROSS univ(:real)) *)
1248(*---------------------------------------------------------------------------*)
1249
1250val mr2_tm =
1251 “(\((x1,x2),(y1,y2)). sqrt ((x1 - y1) pow 2 + (x2 - y2) pow 2) :real)”;
1252
1253Theorem MR2_lemma1[local] :
1254 !x1 x2 z1 z2. ^mr2_tm ((x1,x2),(z1,z2)) = ^mr2_tm ((x1-z1,x2-z2),(0,0))
1255Proof
1256 rw []
1257QED
1258
1259Theorem MR2_lemma2[local] :
1260 !x1 x2 y1 y2. ^mr2_tm ((x1+y1,x2+y2),(0,0)) <=
1261 ^mr2_tm ((x1,x2),(0,0)) + ^mr2_tm ((y1,y2),(0,0))
1262Proof
1263 rw []
1264 >> CCONTR_TAC >> fs [real_lte]
1265 >> Know ‘(sqrt (x1 pow 2 + x2 pow 2) + sqrt (y1 pow 2 + y2 pow 2)) pow 2 <
1266 (sqrt ((x1 + y1) pow 2 + (x2 + y2) pow 2)) pow 2’
1267 >- (MATCH_MP_TAC REAL_POW_LT2 >> rw [] \\
1268 MATCH_MP_TAC REAL_LE_ADD \\
1269 CONJ_TAC \\ (* 2 subgoals, same tactics *)
1270 MATCH_MP_TAC SQRT_POS_LE >> MATCH_MP_TAC REAL_LE_ADD >> rw [REAL_LE_POW2])
1271 >> KILL_TAC
1272 >> REWRITE_TAC [GSYM real_lte]
1273 >> Know ‘sqrt ((x1 + y1) pow 2 + (x2 + y2) pow 2) pow 2 =
1274 (x1 + y1) pow 2 + (x2 + y2) pow 2’
1275 >- (MATCH_MP_TAC SQRT_POW_2 \\
1276 MATCH_MP_TAC REAL_LE_ADD >> rw [REAL_LE_POW2])
1277 >> Rewr'
1278 >> GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) empty_rewrites [ADD_POW_2]
1279 >> Know ‘sqrt (x1 pow 2 + x2 pow 2) pow 2 = x1 pow 2 + x2 pow 2’
1280 >- (MATCH_MP_TAC SQRT_POW_2 \\
1281 MATCH_MP_TAC REAL_LE_ADD >> rw [REAL_LE_POW2])
1282 >> Rewr'
1283 >> Know ‘sqrt (y1 pow 2 + y2 pow 2) pow 2 = y1 pow 2 + y2 pow 2’
1284 >- (MATCH_MP_TAC SQRT_POW_2 \\
1285 MATCH_MP_TAC REAL_LE_ADD >> rw [REAL_LE_POW2])
1286 >> Rewr'
1287 >> REWRITE_TAC [ADD_POW_2]
1288 >> Suff ‘x1 * y1 + x2 * y2 <= sqrt (x1 pow 2 + x2 pow 2) * sqrt (y1 pow 2 + y2 pow 2)’
1289 >- REAL_ARITH_TAC
1290 >> Know ‘sqrt (x1 pow 2 + x2 pow 2) * sqrt (y1 pow 2 + y2 pow 2) =
1291 sqrt ((x1 pow 2 + x2 pow 2) * (y1 pow 2 + y2 pow 2))’
1292 >- (MATCH_MP_TAC EQ_SYM \\
1293 MATCH_MP_TAC SQRT_MUL \\
1294 CONJ_TAC \\ (* 2 subgoals, same tactics *)
1295 MATCH_MP_TAC REAL_LE_ADD >> rw [REAL_LE_POW2])
1296 >> Rewr'
1297 >> CCONTR_TAC >> fs [real_lte]
1298 >> Know ‘(sqrt ((x1 pow 2 + x2 pow 2) * (y1 pow 2 + y2 pow 2))) pow 2 <
1299 (x1 * y1 + x2 * y2) pow 2’
1300 >- (MATCH_MP_TAC REAL_POW_LT2 >> rw [] \\
1301 MATCH_MP_TAC SQRT_POS_LE \\
1302 MATCH_MP_TAC REAL_LE_MUL \\
1303 CONJ_TAC >> MATCH_MP_TAC REAL_LE_ADD >> rw [REAL_LE_POW2])
1304 >> KILL_TAC
1305 >> REWRITE_TAC [GSYM real_lte]
1306 >> Know ‘sqrt ((x1 pow 2 + x2 pow 2) * (y1 pow 2 + y2 pow 2)) pow 2 =
1307 (x1 pow 2 + x2 pow 2) * (y1 pow 2 + y2 pow 2)’
1308 >- (MATCH_MP_TAC SQRT_POW_2 \\
1309 MATCH_MP_TAC REAL_LE_MUL \\
1310 CONJ_TAC >> MATCH_MP_TAC REAL_LE_ADD >> rw [REAL_LE_POW2])
1311 >> Rewr'
1312 >> rw [ADD_POW_2, POW_MUL, REAL_ADD_LDISTRIB, REAL_ADD_RDISTRIB]
1313 >> Suff ‘2 * (x1 * x2 * y1 * y2) <= x1 pow 2 * y2 pow 2 + x2 pow 2 * y1 pow 2’
1314 >- REAL_ARITH_TAC
1315 >> Know ‘0 <= (x1 * y2 - x2 * y1) pow 2’ >- rw [REAL_LE_POW2]
1316 >> ONCE_REWRITE_TAC [POW_2]
1317 >> REAL_ARITH_TAC
1318QED
1319
1320Theorem MR2_lemma3[local] :
1321 !x1 x2 y1 y2. ^mr2_tm ((x1,x2),(y1,y2)) = ^mr2_tm ((y1,y2),(x1,x2))
1322Proof
1323 rw []
1324 >> Know ‘(x1 - y1) pow 2 = (y1 - x1) pow 2’
1325 >- (REWRITE_TAC [POW_2] >> REAL_ARITH_TAC)
1326 >> Rewr'
1327 >> Know ‘(x2 - y2) pow 2 = (y2 - x2) pow 2’
1328 >- (REWRITE_TAC [POW_2] >> REAL_ARITH_TAC)
1329 >> Rewr
1330QED
1331
1332Theorem ISMET_R2 :
1333 ismet ^mr2_tm
1334Proof
1335 Q.ABBREV_TAC ‘d = ^mr2_tm’
1336 >> RW_TAC std_ss [ismet] (* 2 subgoals *)
1337 >- (Q.UNABBREV_TAC ‘d’ \\
1338 Cases_on ‘x’ >> Cases_on ‘y’ >> simp [] \\
1339 reverse EQ_TAC >- rw [SQRT_0, pow_rat] \\
1340 STRIP_TAC >> rename1 ‘x1 = x2 /\ y1 = y2’ >>
1341 Cases_on ‘x1 = x2’ >> gvs[pow_rat] >| (* 2 subgoals *)
1342 [ (* goal 1 (of 2) *)
1343 CCONTR_TAC >>
1344 Suff ‘0 < (y1 - y2) pow 2’
1345 >- (METIS_TAC [SQRT_POS_LT, REAL_LT_IMP_NE]) \\
1346 simp[],
1347 (* goal 2 (of 2) *)
1348 Suff ‘0 < (x1 - x2) pow 2 + (y1 - y2) pow 2’
1349 >- (METIS_TAC [SQRT_POS_LT, REAL_LT_IMP_NE]) \\
1350 irule REAL_LTE_TRANS >> qexists_tac ‘(x1 - x2) pow 2’ >> simp[]
1351 ])
1352 >> Cases_on ‘x’ >> Cases_on ‘y’ >> Cases_on ‘z’
1353 >> rename1 ‘d ((x1,x2),(z1,z2)) <= d ((y1,y2),(x1,x2)) + d ((y1,y2),(z1,z2))’
1354 >> Know ‘d ((x1,x2),z1,z2) = d ((x1-z1,x2-z2),(0,0))’
1355 >- METIS_TAC [MR2_lemma1]
1356 >> Rewr'
1357 >> ‘x1 - z1 = x1 - y1 + (y1 - z1)’ by REAL_ARITH_TAC >> POP_ORW
1358 >> ‘x2 - z2 = x2 - y2 + (y2 - z2)’ by REAL_ARITH_TAC >> POP_ORW
1359 >> Know ‘d ((y1,y2),(x1,x2)) = d ((x1,x2),(y1,y2))’
1360 >- METIS_TAC [MR2_lemma3]
1361 >> Rewr'
1362 >> Know ‘d ((x1 - y1 + (y1 - z1),x2 - y2 + (y2 - z2)),(0,0)) <=
1363 d ((x1 - y1,x2 - y2),(0,0)) + d ((y1 - z1,y2 - z2),(0,0))’
1364 >- METIS_TAC [MR2_lemma2]
1365 >> Suff ‘d ((x1 - y1,x2 - y2),0,0) + d ((y1 - z1,y2 - z2),0,0) =
1366 d ((x1,x2),y1,y2) + d ((y1,y2),z1,z2)’ >- rw []
1367 >> METIS_TAC [MR2_lemma1]
1368QED
1369
1370Definition mr2 :
1371 mr2 = metric ^mr2_tm
1372End
1373
1374Theorem MR2_DEF :
1375 !x1 x2 y1 y2. (dist mr2) ((x1,x2),(y1,y2)) =
1376 sqrt ((x1 - y1) pow 2 + (x2 - y2) pow 2)
1377Proof
1378 rw [mr2, REWRITE_RULE [metric_tybij] ISMET_R2]
1379QED
1380
1381Theorem MR2_MIRROR :
1382 !x1 x2 y1 y2. (dist mr2) ((-x1,-x2),(-y1,-y2)) = (dist mr2) ((x1,x2),(y1,y2))
1383Proof
1384 rw [MR2_DEF, REAL_ARITH “-x - -y = -(x - y)”]
1385QED
1386
1387(* ------------------------------------------------------------------------- *)
1388(* Continuous functions on metric spaces. *)
1389(* ------------------------------------------------------------------------- *)
1390
1391Theorem METRIC_CONTINUOUS_MAP :
1392 !m m' (f :'a -> 'b).
1393 continuous_map (mtopology m,mtopology m') f <=>
1394 (!x. x IN mspace m ==> f x IN mspace m') /\
1395 (!a e. &0 < e /\ a IN mspace m
1396 ==> (?d. &0 < d /\
1397 (!x. x IN mspace m /\ mdist m (a,x) < d
1398 ==> mdist m' (f a, f x) < e)))
1399Proof
1400 REPEAT GEN_TAC THEN REWRITE_TAC[continuous_map, TOPSPACE_MTOPOLOGY] THEN
1401 EQ_TAC THEN SIMP_TAC std_ss[] THENL
1402 [ (* goal 1 (of 2) *)
1403 rpt STRIP_TAC THEN
1404 Q.PAT_X_ASSUM ‘!u. open_in (mtop m') u ==> P’
1405 (MP_TAC o SPEC “mball m' (f (a:'a):'b,e)”) THEN
1406 REWRITE_TAC[OPEN_IN_MBALL] THEN
1407 simp [OPEN_IN_MTOPOLOGY, SUBSET_DEF, IN_MBALL] THEN
1408 DISCH_THEN (MP_TAC o SPEC “a:'a”) THEN ASM_SIMP_TAC std_ss[MDIST_REFL],
1409 (* goal 2 (of 2) *)
1410 rw [OPEN_IN_MTOPOLOGY, SUBSET_DEF, IN_MBALL, MSPACE] THEN
1411 ASM_MESON_TAC[] ]
1412QED
1413
1414Theorem CONTINUOUS_MAP_TO_METRIC :
1415 !t m (f :'a -> 'b).
1416 continuous_map (t,mtopology m) f <=>
1417 (!x. x IN topspace t
1418 ==> (!r. &0 < r
1419 ==> (?u. open_in t u /\
1420 x IN u /\
1421 (!y. y IN u ==> f y IN mball m (f x,r)))))
1422Proof
1423 rpt GEN_TAC
1424 >> REWRITE_TAC[CONTINUOUS_MAP_EQ_TOPCONTINUOUS_AT, topcontinuous_at,
1425 TOPSPACE_MTOPOLOGY]
1426 >> EQ_TAC
1427 >- (rw [] \\
1428 Q.PAT_X_ASSUM ‘!x. P’ (MP_TAC o Q.SPEC ‘x’) >> rw [] \\
1429 POP_ASSUM MATCH_MP_TAC \\
1430 ASM_SIMP_TAC std_ss[OPEN_IN_MBALL, CENTRE_IN_MBALL])
1431 >> rw [] >- rw [MSPACE] (* A shortcut *)
1432 >> Q.PAT_X_ASSUM ‘!x. P’ (MP_TAC o Q.SPEC ‘x’) >> rw []
1433 >> fs [OPEN_IN_MTOPOLOGY]
1434 >> Q.PAT_X_ASSUM ‘!x. x IN v ==> _’ (MP_TAC o Q.SPEC ‘f x’) >> rw []
1435 >> Q.PAT_X_ASSUM ‘!r. 0 < r ==> _’ (MP_TAC o Q.SPEC ‘r’)
1436 >> rw [IN_MBALL]
1437 >> Q.EXISTS_TAC ‘u’ >> rw []
1438 >> Suff ‘f y IN mball m (f x,r)’ >- METIS_TAC [SUBSET_DEF]
1439 >> Q.PAT_X_ASSUM ‘!y. y IN u ==> _’ (MP_TAC o Q.SPEC ‘y’)
1440 >> rw [IN_MBALL]
1441QED
1442
1443Theorem CONTINUOUS_MAP_FROM_METRIC :
1444 !m top (f :'a -> 'b).
1445 continuous_map (mtopology m,top) f <=>
1446 IMAGE f (mspace m) SUBSET topspace top /\
1447 !a. a IN mspace m
1448 ==> !u. open_in top u /\ f(a) IN u
1449 ==> ?d. &0 < d /\
1450 !x. x IN mspace m /\ mdist m (a,x) < d
1451 ==> f x IN u
1452Proof
1453 REPEAT GEN_TAC THEN REWRITE_TAC[CONTINUOUS_MAP, TOPSPACE_MTOPOLOGY] THEN
1454 ASM_CASES_TAC “IMAGE (f :'a -> 'b) (mspace m) SUBSET topspace top” THEN
1455 ASM_REWRITE_TAC[OPEN_IN_MTOPOLOGY] THEN EQ_TAC THEN DISCH_TAC THENL
1456 [ (* goal 1 (of 2) *)
1457 X_GEN_TAC “a :'a” THEN DISCH_TAC THEN
1458 X_GEN_TAC “u :'b set” THEN STRIP_TAC THEN
1459 FIRST_X_ASSUM(MP_TAC o SPEC “u :'b set”) THEN
1460 ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o SPEC “a :'a” o CONJUNCT2) THEN
1461 simp [SUBSET_DEF, IN_MBALL],
1462 (* goal 2 (of 2) *)
1463 X_GEN_TAC “u :'b set” THEN DISCH_TAC THEN
1464 simp [SUBSET_RESTRICT] THEN
1465 X_GEN_TAC “a :'a” THEN STRIP_TAC THEN
1466 FIRST_X_ASSUM(MP_TAC o SPEC “a :'a”) THEN ASM_REWRITE_TAC[] THEN
1467 DISCH_THEN(MP_TAC o SPEC “u :'b set”) THEN ASM_REWRITE_TAC[] THEN
1468 simp [SUBSET_DEF, IN_MBALL] ]
1469QED
1470
1471(*---------------------------------------------------------------------------*)
1472(* closed ball in metric space + prove basic properties *)
1473(* (ported from HOL-Light's Multivariate/metric.ml) *)
1474(*---------------------------------------------------------------------------*)
1475
1476Theorem CLOSED_IN_METRIC :
1477 !m (c :'a set).
1478 closed_in (mtopology m) c <=>
1479 c SUBSET mspace m /\
1480 (!x. x IN mspace m DIFF c ==> ?r. &0 < r /\ DISJOINT c (mball m (x,r)))
1481Proof
1482 rw[closed_in, OPEN_IN_MTOPOLOGY, DISJOINT_DEF, TOPSPACE_MTOPOLOGY]
1483 >> MP_TAC MBALL_SUBSET_MSPACE >> ASM_SET_TAC[]
1484QED
1485
1486Definition mcball :
1487 mcball m (x :'a,r) =
1488 {y | x IN mspace m /\ y IN mspace m /\ mdist m (x,y) <= r}
1489End
1490
1491Theorem IN_MCBALL :
1492 !m (x :'a) r y.
1493 y IN mcball m (x,r) <=>
1494 x IN mspace m /\ y IN mspace m /\ mdist m (x,y) <= r
1495Proof
1496 rw [mcball]
1497QED
1498
1499Theorem CENTRE_IN_MCBALL :
1500 !m (x :'a) r. &0 <= r /\ x IN mspace m ==> x IN mcball m (x,r)
1501Proof
1502 SIMP_TAC std_ss[IN_MCBALL, MDIST_REFL]
1503QED
1504
1505Theorem CENTRE_IN_MCBALL_EQ :
1506 !m (x :'a) r. x IN mcball m (x,r) <=> x IN mspace m /\ &0 <= r
1507Proof
1508 REPEAT GEN_TAC THEN REWRITE_TAC[IN_MCBALL] THEN
1509 ASM_CASES_TAC “(x :'a) IN mspace m” THEN ASM_SIMP_TAC std_ss[MDIST_REFL]
1510QED
1511
1512Theorem MCBALL_EQ_EMPTY :
1513 !m (x :'a) r. mcball m (x,r) = {} <=> ~(x IN mspace m) \/ r < &0
1514Proof
1515 REPEAT GEN_TAC THEN
1516 rw [Once EXTENSION, IN_MCBALL, NOT_IN_EMPTY] THEN
1517 ASM_MESON_TAC[REAL_NOT_LT, REAL_LE_TRANS, MDIST_POS_LE, MDIST_REFL]
1518QED
1519
1520Theorem MCBALL_EMPTY :
1521 !m (x :'a) r. r < &0 ==> mcball m (x,r) = {}
1522Proof
1523 SIMP_TAC std_ss[MCBALL_EQ_EMPTY]
1524QED
1525
1526Theorem MCBALL_EMPTY_ALT :
1527 !m (x :'a) r. ~(x IN mspace m) ==> mcball m (x,r) = {}
1528Proof
1529 SIMP_TAC std_ss[MCBALL_EQ_EMPTY]
1530QED
1531
1532Theorem MCBALL_SUBSET_MSPACE :
1533 !m (x :'a) r. mcball m (x,r) SUBSET (mspace m)
1534Proof
1535 rw [mcball, SUBSET_DEF]
1536QED
1537
1538Theorem MBALL_SUBSET_MCBALL :
1539 !m (x :'a) r. mball m (x,r) SUBSET mcball m (x,r)
1540Proof
1541 SIMP_TAC std_ss[SUBSET_DEF, IN_MBALL, IN_MCBALL, REAL_LT_IMP_LE]
1542QED
1543
1544Theorem MCBALL_SUBSET :
1545 !m x (y :'a) a b. y IN mspace m /\ mdist m (x,y) + a <= b
1546 ==> mcball m (x,a) SUBSET mcball m (y,b)
1547Proof
1548 REPEAT GEN_TAC THEN ASM_CASES_TAC “(x :'a) IN mspace m” THENL
1549 [STRIP_TAC, rw [MCBALL_EMPTY_ALT]] THEN
1550 simp [SUBSET_DEF, IN_MCBALL] \\
1551 Q.X_GEN_TAC ‘z’ \\
1552 STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
1553 Suff `mdist m (y,z) <= mdist m (x,y) + mdist m (x,z)` >- REAL_ASM_ARITH_TAC \\
1554 ASM_MESON_TAC[MDIST_SYM, MDIST_TRIANGLE]
1555QED
1556
1557Theorem MCBALL_SUBSET_CONCENTRIC :
1558 !m (x :'a) a b. a <= b ==> mcball m (x,a) SUBSET mcball m (x,b)
1559Proof
1560 SIMP_TAC std_ss[SUBSET_DEF, IN_MCBALL] THEN MESON_TAC[REAL_LE_TRANS]
1561QED
1562
1563Theorem CLOSED_IN_MCBALL :
1564 !(m :'a metric) x r. closed_in (mtopology m) (mcball m (x,r))
1565Proof
1566 RW_TAC std_ss [CLOSED_IN_METRIC, MCBALL_SUBSET_MSPACE, IN_MCBALL,
1567 DE_MORGAN_THM, REAL_NOT_LE, IN_DIFF]
1568 >> rename1 ‘y IN mspace m’
1569 >- (simp [MCBALL_EMPTY_ALT] \\
1570 Q.EXISTS_TAC ‘1’ >> rw [])
1571 >> Q.EXISTS_TAC ‘mdist m (x,y) - r’
1572 >> rw [REAL_SUB_LT]
1573 >> simp [Once EXTENSION, DISJOINT_DEF, NOT_IN_EMPTY, IN_MBALL, IN_MCBALL]
1574 >> Q.X_GEN_TAC ‘z’
1575 >> Cases_on ‘z IN mspace m’ >> rw []
1576 >> Cases_on ‘x IN mspace m’ >> rw []
1577 >> STRONG_DISJ_TAC
1578 >> simp [real_lt]
1579 >> Know ‘dist m (x,y) - r <= dist m (y,z) <=>
1580 dist m (x,y) - dist m (y,z) <= r’ >- REAL_ARITH_TAC
1581 >> Rewr'
1582 >> Q_TAC (TRANS_TAC REAL_LE_TRANS) ‘dist m (x,z)’ >> art []
1583 >> rw [MDIST_TRIANGLE_SUB]
1584QED
1585
1586Theorem MDIST_LE_0 :
1587 !m x y. dist m (x,y) <= 0 <=> dist m (x,y) = 0
1588Proof
1589 rpt GEN_TAC
1590 >> reverse EQ_TAC >- rw []
1591 >> rw [REAL_LE_LT]
1592 >> PROVE_TAC [REAL_LET_ANTISYM, METRIC_POS]
1593QED
1594
1595Theorem MCBALL_TRIVIAL :
1596 !m x. mcball m (x,0) = {x}
1597Proof
1598 rw [Once EXTENSION, IN_MCBALL, MSPACE]
1599 >> rename1 ‘_ <=> y = x’
1600 >> simp [MDIST_LE_0, METRIC_ZERO]
1601 >> PROVE_TAC []
1602QED
1603
1604Theorem MCBALL_SING :
1605 !m x e. e = 0 ==> mcball m (x,e) = {x}
1606Proof
1607 rw [MCBALL_TRIVIAL]
1608QED
1609
1610(* ------------------------------------------------------------------------- *)
1611(* More general infimum of distance between two sets. *)
1612(* ------------------------------------------------------------------------- *)
1613
1614(* This is a generalized ‘setdist’ with a metric parameter d *)
1615Definition set_dist_def :
1616 set_dist (d :'a metric) ((s,t) :'a set # 'a set) =
1617 if (s = {}) \/ (t = {}) then (0 :real)
1618 else inf {dist d (x,y) | x IN s /\ y IN t}
1619End
1620
1621Theorem SET_DIST_EMPTY :
1622 (!t. set_dist m({},t) = &0) /\ (!s. set_dist m(s,{}) = &0)
1623Proof
1624 REWRITE_TAC[set_dist_def]
1625QED
1626
1627Theorem SET_DIST_POS_LE :
1628 !s t. &0 <= set_dist m(s,t)
1629Proof
1630 REPEAT GEN_TAC THEN REWRITE_TAC[set_dist_def] THEN
1631 COND_CASES_TAC THEN REWRITE_TAC[REAL_LE_REFL] THEN
1632 MATCH_MP_TAC REAL_LE_INF THEN
1633 SIMP_TAC std_ss [FORALL_IN_GSPEC, MDIST_POS_LE] THEN
1634 SIMP_TAC std_ss [EXTENSION, GSPECIFICATION, EXISTS_PROD] THEN ASM_SET_TAC[]
1635QED
1636
1637Theorem SET_DIST_SUBSETS_EQ :
1638 !s t s' t'.
1639 s' SUBSET s /\ t' SUBSET t /\
1640 (!x y. x IN s /\ y IN t
1641 ==> ?x' y'. x' IN s' /\ y' IN t' /\ dist m(x',y') <= dist m(x,y))
1642 ==> (set_dist m(s',t') = set_dist m(s,t))
1643Proof
1644 REPEAT STRIP_TAC THEN
1645 ASM_CASES_TAC ``s:'a->bool = {}`` THENL
1646 [ASM_CASES_TAC ``s':'a->bool = {}`` THEN
1647 ASM_REWRITE_TAC[SET_DIST_EMPTY] THEN ASM_SET_TAC[],
1648 ALL_TAC] THEN
1649 ASM_CASES_TAC ``t:'a->bool = {}`` THENL
1650 [ASM_CASES_TAC ``t':'a->bool = {}`` THEN
1651 ASM_REWRITE_TAC[SET_DIST_EMPTY] THEN ASM_SET_TAC[],
1652 ALL_TAC] THEN
1653 ASM_CASES_TAC ``s':'a->bool = {}`` THENL [ASM_SET_TAC[], ALL_TAC] THEN
1654 ASM_CASES_TAC ``t':'a->bool = {}`` THENL [ASM_SET_TAC[], ALL_TAC] THEN
1655 ASM_REWRITE_TAC[set_dist_def] THEN MATCH_MP_TAC INF_EQ THEN
1656 SIMP_TAC std_ss [FORALL_IN_GSPEC] THEN
1657 CONJ_TAC >- (SIMP_TAC std_ss [EXTENSION, GSPECIFICATION,
1658 EXISTS_PROD, NOT_IN_EMPTY] \\
1659 fs [GSYM MEMBER_NOT_EMPTY] \\
1660 rename1 `a IN s'` >> Q.EXISTS_TAC `a` \\
1661 rename1 `b IN t'` >> Q.EXISTS_TAC `b` \\
1662 ASM_REWRITE_TAC []) \\
1663 CONJ_TAC >- (Q.EXISTS_TAC `0` >> rw [MDIST_POS_LE, mspace]) \\
1664 CONJ_TAC >- (SIMP_TAC std_ss [EXTENSION, GSPECIFICATION,
1665 EXISTS_PROD, NOT_IN_EMPTY] \\
1666 fs [GSYM MEMBER_NOT_EMPTY] \\
1667 rename1 `a IN s` >> Q.EXISTS_TAC `a` \\
1668 rename1 `b IN t` >> Q.EXISTS_TAC `b` \\
1669 ASM_REWRITE_TAC []) \\
1670 CONJ_TAC >- (Q.EXISTS_TAC `0` >> rw [MDIST_POS_LE, mspace]) \\
1671 ASM_MESON_TAC[SUBSET_DEF, REAL_LE_TRANS]
1672QED
1673
1674Theorem REAL_LE_SET_DIST :
1675 !s t:'a->bool d.
1676 ~(s = {}) /\ ~(t = {}) /\
1677 (!x y. x IN s /\ y IN t ==> d <= dist m(x,y))
1678 ==> d <= set_dist m(s,t)
1679Proof
1680 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[set_dist_def] THEN
1681 MP_TAC(ISPEC ``{dist m(x:'a,y) | x IN s /\ y IN t}`` INF) THEN
1682 SIMP_TAC std_ss [FORALL_IN_GSPEC] THEN
1683 KNOW_TAC ``{dist m(x,y) | x IN s /\ y IN t} <> {} /\
1684 (?b. !x y. x IN s /\ y IN t ==> b <= dist m(x,y))`` THENL
1685 [CONJ_TAC THENL
1686 [SIMP_TAC std_ss [EXTENSION, GSPECIFICATION, EXISTS_PROD] THEN
1687 ASM_SET_TAC[],
1688 Q.EXISTS_TAC ‘d’ >> rw []],
1689 DISCH_TAC THEN ASM_REWRITE_TAC []] THEN
1690 ASM_MESON_TAC[]
1691QED
1692
1693Theorem SET_DIST_LE_DIST :
1694 !s t x y. x IN s /\ y IN t ==> set_dist m(s,t) <= dist m(x,y)
1695Proof
1696 REPEAT GEN_TAC THEN REWRITE_TAC[set_dist_def] THEN
1697 COND_CASES_TAC THENL [ASM_SET_TAC[], ALL_TAC] THEN
1698 MP_TAC(ISPEC ``{dist m(x,y) | x IN s /\ y IN t}`` INF) THEN
1699 SIMP_TAC std_ss [FORALL_IN_GSPEC] THEN
1700 KNOW_TAC ``{dist m(x,y) | x IN s /\ y IN t} <> {} /\
1701 (?b. !x y. x IN s /\ y IN t ==> b <= dist m(x,y))`` THENL
1702 [CONJ_TAC THENL
1703 [SIMP_TAC std_ss [EXTENSION, GSPECIFICATION, EXISTS_PROD] THEN
1704 ASM_SET_TAC[],
1705 Q.EXISTS_TAC ‘0’ >> simp[MDIST_POS_LE]],
1706 DISCH_TAC THEN ASM_REWRITE_TAC []] THEN
1707 ASM_MESON_TAC[]
1708QED
1709
1710Theorem REAL_LE_SET_DIST_EQ :
1711 !d s t:'a->bool.
1712 d <= set_dist m(s,t) <=>
1713 (!x y. x IN s /\ y IN t ==> d <= dist m(x,y)) /\
1714 ((s = {}) \/ (t = {}) ==> d <= &0)
1715Proof
1716 REPEAT GEN_TAC THEN MAP_EVERY ASM_CASES_TAC
1717 [``s:'a->bool = {}``, ``t:'a->bool = {}``] THEN
1718 ASM_REWRITE_TAC[SET_DIST_EMPTY, NOT_IN_EMPTY] THEN
1719 ASM_MESON_TAC[REAL_LE_SET_DIST, SET_DIST_LE_DIST, REAL_LE_TRANS]
1720QED
1721
1722Theorem REAL_SET_DIST_LT_EXISTS :
1723 !s t:'a->bool b.
1724 ~(s = {}) /\ ~(t = {}) /\ set_dist m(s,t) < b
1725 ==> ?x y. x IN s /\ y IN t /\ dist m(x,y) < b
1726Proof
1727 REWRITE_TAC[GSYM REAL_NOT_LE, REAL_LE_SET_DIST_EQ] THEN MESON_TAC[]
1728QED
1729
1730Theorem SET_DIST_REFL :
1731 !s:'a->bool. set_dist m(s,s) = &0
1732Proof
1733 GEN_TAC THEN REWRITE_TAC[GSYM REAL_LE_ANTISYM, SET_DIST_POS_LE] THEN
1734 ASM_CASES_TAC ``s:'a->bool = {}`` THENL
1735 [ASM_REWRITE_TAC[set_dist_def, REAL_LE_REFL], ALL_TAC] THEN
1736 ASM_MESON_TAC[SET_DIST_LE_DIST, MEMBER_NOT_EMPTY, MDIST_REFL]
1737QED
1738
1739Theorem SET_DIST_SYM :
1740 !s t. set_dist m(s,t) = set_dist m(t,s)
1741Proof
1742 REPEAT GEN_TAC THEN REWRITE_TAC[set_dist_def] THEN ONCE_REWRITE_TAC [DISJ_SYM] THEN
1743 COND_CASES_TAC THEN ONCE_REWRITE_TAC [DISJ_SYM] THEN ASM_SIMP_TAC std_ss [] THEN
1744 AP_TERM_TAC THEN SIMP_TAC std_ss [EXTENSION, GSPECIFICATION, EXISTS_PROD] THEN
1745 METIS_TAC[MDIST_SYM]
1746QED
1747
1748Theorem SET_DIST_TRIANGLE :
1749 !s a t:'a->bool.
1750 set_dist m(s,t) <= set_dist m(s,{a}) + set_dist m({a},t)
1751Proof
1752 REPEAT STRIP_TAC THEN ASM_CASES_TAC ``s:'a->bool = {}`` THEN
1753 ASM_REWRITE_TAC[SET_DIST_EMPTY, REAL_ADD_LID, SET_DIST_POS_LE] THEN
1754 ASM_CASES_TAC ``t:'a->bool = {}`` THEN
1755 ASM_REWRITE_TAC[SET_DIST_EMPTY, REAL_ADD_RID, SET_DIST_POS_LE] THEN
1756 ONCE_REWRITE_TAC[GSYM REAL_LE_SUB_RADD] THEN
1757 MATCH_MP_TAC REAL_LE_SET_DIST THEN
1758 ASM_SIMP_TAC std_ss [NOT_INSERT_EMPTY, IN_SING, CONJ_EQ_IMP,
1759 RIGHT_FORALL_IMP_THM, UNWIND_FORALL_THM2] THEN
1760 X_GEN_TAC ``x:'a`` THEN DISCH_TAC THEN
1761 ONCE_REWRITE_TAC[REAL_ARITH ``x - y <= z <=> x - z <= y:real``] THEN
1762 MATCH_MP_TAC REAL_LE_SET_DIST THEN
1763 ASM_REWRITE_TAC[NOT_INSERT_EMPTY, IN_SING, CONJ_EQ_IMP,
1764 RIGHT_FORALL_IMP_THM, UNWIND_FORALL_THM2] THEN
1765 X_GEN_TAC ``y:'a`` THEN REPEAT STRIP_TAC THEN
1766 REWRITE_TAC[REAL_LE_SUB_RADD] THEN MATCH_MP_TAC REAL_LE_TRANS THEN
1767 EXISTS_TAC ``dist m(x:'a,y')`` THEN
1768 ASM_SIMP_TAC std_ss [SET_DIST_LE_DIST] THEN
1769 rename1 ‘z IN t’ THEN
1770 Q.PAT_X_ASSUM ‘y = a’ (fs o wrap o SYM) \\
1771 ONCE_REWRITE_TAC [REAL_ADD_COMM] \\
1772 REWRITE_TAC [MDIST_TRIANGLE]
1773QED
1774
1775Theorem SET_DIST_SINGS :
1776 !x y. set_dist m({x},{y}) = dist m(x,y)
1777Proof
1778 REWRITE_TAC[set_dist_def, NOT_INSERT_EMPTY] THEN
1779 ONCE_REWRITE_TAC [METIS [] ``dist m(x,y) = (\x y. dist m(x,y)) x y``] THEN
1780 KNOW_TAC ``!f:'a->'a->real x y a b. {f x y | x IN {a} /\ y IN {b}} = {f a b}`` THENL
1781 [SIMP_TAC std_ss [EXTENSION, GSPECIFICATION, EXISTS_PROD] THEN SET_TAC [],
1782 DISCH_TAC] THEN ASM_REWRITE_TAC [] THEN
1783 SIMP_TAC std_ss [INF_INSERT_FINITE, FINITE_EMPTY]
1784QED
1785
1786Theorem SET_DIST_LIPSCHITZ :
1787 !s x (y :'a). abs(set_dist m({x},s) - set_dist m({y},s)) <= dist m(x,y)
1788Proof
1789 REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM SET_DIST_SINGS] THEN
1790 REWRITE_TAC[REAL_ARITH
1791 ``abs(x - y) <= z <=> x <= z + y /\ y <= z + x:real``] THEN
1792 MESON_TAC[SET_DIST_TRIANGLE, SET_DIST_SYM]
1793QED
1794
1795Theorem SET_DIST_SUBSET_RIGHT :
1796 !s t u:'a->bool.
1797 ~(t = {}) /\ t SUBSET u ==> set_dist m(s,u) <= set_dist m(s,t)
1798Proof
1799 REPEAT STRIP_TAC THEN
1800 MAP_EVERY ASM_CASES_TAC [``s:'a->bool = {}``, ``u:'a->bool = {}``] THEN
1801 ASM_SIMP_TAC std_ss [SET_DIST_EMPTY, SET_DIST_POS_LE, REAL_LE_REFL] THEN
1802 ASM_REWRITE_TAC[set_dist_def] THEN MATCH_MP_TAC REAL_LE_INF_SUBSET THEN
1803 ASM_SIMP_TAC std_ss [FORALL_IN_GSPEC, SUBSET_DEF, EXISTS_PROD, GSPECIFICATION] THEN
1804 REPEAT(CONJ_TAC THENL
1805 [ASM_SIMP_TAC std_ss [EXTENSION, EXISTS_PROD, GSPECIFICATION] THEN ASM_SET_TAC[],
1806 ALL_TAC]) \\
1807 Q.EXISTS_TAC ‘0’ >> rw [MDIST_POS_LE]
1808QED
1809
1810Theorem SET_DIST_SUBSET_LEFT :
1811 !s t u:'a->bool.
1812 ~(s = {}) /\ s SUBSET t ==> set_dist m(t,u) <= set_dist m(s,u)
1813Proof
1814 MESON_TAC[SET_DIST_SUBSET_RIGHT, SET_DIST_SYM]
1815QED
1816
1817Theorem SET_DIST_UNIQUE :
1818 !s t a b:'a d.
1819 a IN s /\ b IN t /\ (dist m(a,b) = d) /\
1820 (!x y. x IN s /\ y IN t ==> dist m(a,b) <= dist m(x,y))
1821 ==> (set_dist m(s,t) = d)
1822Proof
1823 REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN CONJ_TAC THENL
1824 [ASM_MESON_TAC[SET_DIST_LE_DIST],
1825 MATCH_MP_TAC REAL_LE_SET_DIST THEN ASM_SET_TAC[]]
1826QED
1827
1828Theorem SET_DIST_UNIV :
1829 (!s. set_dist m(s,univ(:'a)) = &0) /\
1830 (!t. set_dist m(univ(:'a),t) = &0)
1831Proof
1832 GEN_REWR_TAC (RAND_CONV o ONCE_DEPTH_CONV) [SET_DIST_SYM] THEN
1833 REWRITE_TAC[] THEN X_GEN_TAC ``s:'a->bool`` THEN
1834 ASM_CASES_TAC ``s:'a->bool = {}`` THEN ASM_REWRITE_TAC[SET_DIST_EMPTY] THEN
1835 MATCH_MP_TAC SET_DIST_UNIQUE THEN
1836 SIMP_TAC std_ss [IN_UNIV, MDIST_EQ_0, RIGHT_EXISTS_AND_THM] THEN
1837 ASM_REWRITE_TAC[UNWIND_THM1, MDIST_REFL, MDIST_POS_LE, MEMBER_NOT_EMPTY]
1838QED
1839
1840Theorem SET_DIST_ZERO :
1841 !s t:'a->bool. ~(DISJOINT s t) ==> (set_dist m(s,t) = &0)
1842Proof
1843 REPEAT STRIP_TAC THEN MATCH_MP_TAC SET_DIST_UNIQUE THEN
1844 KNOW_TAC ``?a. a IN s /\ a IN t /\ (dist m(a,a) = 0) /\
1845 !x y. x IN s /\ y IN t ==> dist m(a,a) <= dist m(x,y)`` THENL
1846 [ALL_TAC, METIS_TAC []] THEN
1847 ONCE_REWRITE_TAC[TAUT `p /\ q /\ r /\ s <=> r /\ p /\ q /\ s`] THEN
1848 REWRITE_TAC[MDIST_EQ_0, UNWIND_THM2, MDIST_REFL, MDIST_POS_LE] THEN
1849 ASM_SET_TAC[]
1850QED
1851
1852Theorem SET_DIST_LE_SING :
1853 !s t x:'a. x IN s ==> set_dist m(s,t) <= set_dist m({x},t)
1854Proof
1855 REPEAT STRIP_TAC THEN MATCH_MP_TAC SET_DIST_SUBSET_LEFT THEN ASM_SET_TAC[]
1856QED
1857
1858Theorem SET_DIST_SING_IN_SET :
1859 !x s. x IN s ==> (set_dist m({x},s) = &0)
1860Proof
1861 rpt STRIP_TAC
1862 >> MATCH_MP_TAC SET_DIST_ZERO
1863 >> rw [DISJOINT_ALT]
1864QED
1865
1866Theorem SET_DIST_EQ_0_CLOSED :
1867 !s x. closed_in (mtop m) s ==> (set_dist m({x},s) = &0 <=> (s = {}) \/ x IN s)
1868Proof
1869 rpt STRIP_TAC
1870 >> reverse EQ_TAC
1871 >- (STRIP_TAC >- rw [SET_DIST_EMPTY] \\
1872 MATCH_MP_TAC SET_DIST_ZERO \\
1873 rw [DISJOINT_ALT])
1874 >> DISCH_TAC
1875 >> Cases_on ‘s = {}’ >> rw []
1876 >> fs [CLOSED_IN_METRIC, MSPACE]
1877 >> CCONTR_TAC
1878 >> Q.PAT_X_ASSUM ‘!x. x NOTIN s ==> _’ (MP_TAC o Q.SPEC ‘x’) >> rw []
1879 >> STRONG_DISJ_TAC
1880 >> rw [DISJOINT_ALT, IN_MBALL, MSPACE]
1881 >> fs [set_dist_def]
1882 >> qabbrev_tac ‘p = {dist m (x',y) | x' = x /\ y IN s}’
1883 (* applying INF_CLOSE *)
1884 >> Know ‘?x. x IN p /\ x < inf p + r’
1885 >- (MATCH_MP_TAC INF_CLOSE >> art [] \\
1886 fs [GSYM MEMBER_NOT_EMPTY] \\
1887 rename1 ‘y IN s’ \\
1888 Q.EXISTS_TAC ‘dist m (x,y)’ >> rw [Abbr ‘p’] \\
1889 Q.EXISTS_TAC ‘y’ >> art [])
1890 >> rw [Abbr ‘p’]
1891 >> Q.EXISTS_TAC ‘y’ >> art []
1892QED
1893
1894(* ------------------------------------------------------------------------- *)
1895(* closed ball based on a set *)
1896(* ------------------------------------------------------------------------- *)
1897
1898(* Unlike the usual closed ball (cball) generated from a single point, this
1899 version generates it from a set of points.
1900 *)
1901Definition set_mcball_def :
1902 set_mcball m s e = {x | set_dist m({x},s) <= e}
1903End
1904
1905(* NOTE: Usually ‘0 < e’ is assumed, but the lemma also holds when ‘e <= 0’. *)
1906Theorem closed_in_set_mcball :
1907 !m s e. closed_in (mtop m) (set_mcball m s e)
1908Proof
1909 rw [CLOSED_IN_METRIC, MSPACE, set_mcball_def, GSYM real_lt]
1910 >> qabbrev_tac ‘d = set_dist m ({x},s)’
1911 >> qabbrev_tac ‘r = d - e’
1912 >> ‘0 < r’ by simp [Abbr ‘r’, REAL_SUB_LT]
1913 >> Q.EXISTS_TAC ‘r’ >> art []
1914 >> simp [DISJOINT_ALT, IN_MBALL]
1915 >> Q.X_GEN_TAC ‘y’ >> rw [MSPACE, real_lt]
1916 (* applying SET_DIST_LIPSCHITZ *)
1917 >> MP_TAC (Q.SPECL [‘s’, ‘x’, ‘y’] SET_DIST_LIPSCHITZ)
1918 >> qabbrev_tac ‘r' = dist m (x,y)’
1919 >> qabbrev_tac ‘d' = set_dist m ({y},s)’
1920 >> simp []
1921 >> Cases_on ‘0 <= d - d'’
1922 >- (‘abs (d - d') = d - d'’ by rw [ABS_REFL] \\
1923 rw [Abbr ‘r’] \\
1924 Q_TAC (TRANS_TAC REAL_LE_TRANS) ‘d - d'’ >> simp [] \\
1925 simp [REAL_LE_SUB_CANCEL1])
1926 >> fs [GSYM real_lt]
1927 >> ‘abs (d - d') = -(d - d')’ by rw [ABS_EQ_NEG]
1928 >> POP_ORW
1929 >> rw [REAL_NEG_SUB]
1930 >> fs [REAL_ARITH “a - b < 0 <=> a < (b :real)”, Abbr ‘r’, REAL_SUB_LT]
1931 >> ‘d < e’ by PROVE_TAC [REAL_LTE_TRANS]
1932 >> PROVE_TAC [REAL_LT_ANTISYM]
1933QED
1934
1935(* ------------------------------------------------------------------------- *)
1936(* Lipschitz continuous functions *)
1937(* ------------------------------------------------------------------------- *)
1938
1939Definition Lipschitz_condition_def :
1940 Lipschitz_condition (E1,E2) k f <=>
1941 !x y. dist E2 (f x,f y) <= k * dist E1 (x,y)
1942End
1943
1944(* Definition 13.8 [1, p.249] (or [2]), cf. topologyTheory.continuous_map *)
1945Definition Lipschitz_continuous_map :
1946 Lipschitz_continuous_map (E1,E2) f <=>
1947 ?k. 0 < k /\ Lipschitz_condition (E1,E2) k f
1948End
1949
1950(* |- !E1 E2 f.
1951 Lipschitz_continuous_map (E1,E2) f <=>
1952 ?k. 0 < k /\ !x y. dist E2 (f x,f y) <= k * dist E1 (x,y)
1953 *)
1954Theorem Lipschitz_continuous_map_def =
1955 Lipschitz_continuous_map |> REWRITE_RULE [Lipschitz_condition_def]
1956
1957Theorem Lipschitz_continuous_map_const :
1958 !E1 E2 c. Lipschitz_continuous_map (E1,E2) (\x. c)
1959Proof
1960 rw [Lipschitz_continuous_map_def, MDIST_REFL]
1961 >> Q.EXISTS_TAC ‘1’ >> simp [MDIST_POS_LE]
1962QED
1963
1964Theorem Lipschitz_continuous_map_imp_continuous_map :
1965 !E1 E2 f. Lipschitz_continuous_map (E1,E2) f ==>
1966 continuous_map (mtop E1,mtop E2) f
1967Proof
1968 rw [Lipschitz_continuous_map_def, METRIC_CONTINUOUS_MAP, MSPACE]
1969 >> ‘k <> 0’ by rw [REAL_LT_IMP_NE]
1970 >> Q.EXISTS_TAC ‘e / k’ >> rw [REAL_LT_DIV]
1971 >> Q_TAC (TRANS_TAC REAL_LET_TRANS) ‘k * dist E1 (a,x)’ >> art []
1972QED
1973
1974(* cf. CONTINUOUS_MAP_COMPOSE *)
1975Theorem Lipschitz_continuous_map_compose :
1976 !top1 top2 top3 f g. Lipschitz_continuous_map (top1,top2) f /\
1977 Lipschitz_continuous_map (top2,top3) g ==>
1978 Lipschitz_continuous_map (top1,top3) (g o f)
1979Proof
1980 rw [Lipschitz_continuous_map_def]
1981 >> Q.EXISTS_TAC ‘k * k'’
1982 >> rw [REAL_LT_MUL]
1983 >> ‘k * k' * dist top1 (x,y) = k' * (k * dist top1 (x,y))’ by REAL_ARITH_TAC
1984 >> POP_ORW
1985 >> Q_TAC (TRANS_TAC REAL_LE_TRANS) ‘k' * dist top2 (f x,f y)’
1986 >> simp []
1987QED
1988
1989(* Another form of SET_DIST_LIPSCHITZ *)
1990Theorem Lipschitz_continuous_map_set_dist :
1991 !E s. Lipschitz_continuous_map (E,mr1) (\x. set_dist E ({x},s))
1992Proof
1993 rw [Lipschitz_continuous_map_def]
1994 >> Q.EXISTS_TAC ‘1’
1995 >> rw [GSYM dist_def, dist, SET_DIST_LIPSCHITZ]
1996QED
1997
1998(* Lemma 13.10 [1, p.249] *)
1999Theorem Lipschitz_continuous_map_exists :
2000 !E A e. 0 < e ==>
2001 ?f. Lipschitz_continuous_map (E,mr1) f /\
2002 (!x. 0 <= f x /\ f x <= 1) /\
2003 (!x. x IN A ==> f x = 1) /\
2004 (!x. e <= set_dist E ({x},A) ==> f x = 0)
2005Proof
2006 rw [Lipschitz_continuous_map, IN_FUNSET]
2007 >> qabbrev_tac ‘g :real -> real = \x. max 0 (min 1 x)’
2008 >> ‘!x. 0 <= g x /\ g x <= 1’
2009 by rw [Abbr ‘g’, REAL_LE_MAX, REAL_LE_MIN, REAL_MIN_LE, REAL_MAX_LE]
2010 >> Know ‘!x. 0 <= x /\ x <= 1 ==> g x = x’
2011 >- (RW_TAC real_ss [Abbr ‘g’, max_def, min_def] >| (* 2 subgoals *)
2012 [ (* goal 1 (of 2) *)
2013 rw [GSYM REAL_LE_ANTISYM],
2014 (* goal 2 (of 2) *)
2015 fs [GSYM real_lt] \\
2016 Cases_on ‘1 <= x’ >> fs [] \\
2017 rw [GSYM REAL_LE_ANTISYM, REAL_LT_IMP_LE] ])
2018 >> DISCH_TAC
2019 >> ‘!x. 1 <= x ==> g x = 1’ by rw [Abbr ‘g’, min_def]
2020 >> qabbrev_tac ‘f = \x. 1 - g (set_dist E ({x},A) / e)’
2021 >> Q.EXISTS_TAC ‘f’ >> simp [mspace]
2022 >> Know ‘!x. 0 <= f x /\ f x <= 1’
2023 >- (Q.X_GEN_TAC ‘x’ \\
2024 simp [Abbr ‘f’, REAL_SUB_LE] \\
2025 qmatch_abbrev_tac ‘1 - g y <= 1’ \\
2026 Q.PAT_X_ASSUM ‘!x. 0 <= g x /\ g x <= 1’ (MP_TAC o Q.SPEC ‘y’) \\
2027 REAL_ARITH_TAC)
2028 >> DISCH_TAC
2029 >> ‘!x. x IN A ==> f x = 1’ by rw [Abbr ‘f’, SET_DIST_SING_IN_SET]
2030 >> simp []
2031 >> Know ‘!x. e <= set_dist E ({x},A) ==> f x = 0’
2032 >- (rw [Abbr ‘f’] \\
2033 FIRST_X_ASSUM MATCH_MP_TAC \\
2034 qmatch_abbrev_tac ‘1 <= z / e’ \\
2035 MATCH_MP_TAC REAL_LE_RDIV >> rw [])
2036 >> simp [] >> DISCH_TAC
2037 (* ?k. Lipschitz_condition (E,mr1) k f *)
2038 >> simp [Lipschitz_condition_def, GSYM dist_def, dist, mspace]
2039 >> ‘e <> 0’ by rw [REAL_LT_IMP_NE]
2040 >> Q.EXISTS_TAC ‘1 / e’ >> rw [Abbr ‘f’]
2041 >> qabbrev_tac ‘a = g (set_dist E ({x},A) / e)’
2042 >> qabbrev_tac ‘b = g (set_dist E ({y},A) / e)’
2043 >> simp [REAL_ARITH “1 - a - (1 - b) = b - (a :real)”]
2044 (* stage work *)
2045 >> Cases_on ‘x IN A’
2046 >- (simp [Abbr ‘a’, SET_DIST_SING_IN_SET] \\
2047 ‘abs b = b’ by rw [ABS_REFL, Abbr ‘b’] >> POP_ORW \\
2048 qunabbrev_tac ‘b’ \\
2049 Cases_on ‘y IN A’ >- rw [SET_DIST_SING_IN_SET, MDIST_POS_LE] \\
2050 qmatch_abbrev_tac ‘e * g (z / e) <= _’ \\
2051 ‘0 <= z’ by rw [Abbr ‘z’, SET_DIST_POS_LE] \\
2052 Cases_on ‘e <= z’
2053 >- (‘1 <= z / e’ by rw [REAL_LE_LDIV_EQ_NEG] \\
2054 ‘g (z / e) = 1’ by rw [] >> rw [] \\
2055 Q_TAC (TRANS_TAC REAL_LE_TRANS) ‘z’ >> art [] \\
2056 simp [Abbr ‘z’, Once SET_DIST_SYM] \\
2057 MATCH_MP_TAC SET_DIST_LE_DIST >> rw []) \\
2058 fs [GSYM real_lt] \\
2059 ‘z / e < 1’ by rw [REAL_LT_LDIV_EQ] \\
2060 Know ‘g (z / e) = z / e’
2061 >- (FIRST_X_ASSUM MATCH_MP_TAC >> rw [REAL_LT_IMP_LE]) >> Rewr' \\
2062 simp [Abbr ‘z’, Once SET_DIST_SYM] \\
2063 MATCH_MP_TAC SET_DIST_LE_DIST >> rw [])
2064 >> Cases_on ‘y IN A’
2065 >- (rw [Abbr ‘b’, SET_DIST_SING_IN_SET, MDIST_POS_LE] \\
2066 ‘abs a = a’ by rw [ABS_REFL, Abbr ‘a’] >> POP_ORW \\
2067 qunabbrev_tac ‘a’ \\
2068 qmatch_abbrev_tac ‘e * g (z / e) <= _’ \\
2069 ‘0 <= z’ by rw [Abbr ‘z’, SET_DIST_POS_LE] \\
2070 Cases_on ‘e <= z’
2071 >- (‘1 <= z / e’ by rw [REAL_LE_LDIV_EQ_NEG] \\
2072 ‘g (z / e) = 1’ by rw [] >> rw [] \\
2073 Q_TAC (TRANS_TAC REAL_LE_TRANS) ‘z’ >> art [] \\
2074 simp [Abbr ‘z’] \\
2075 MATCH_MP_TAC SET_DIST_LE_DIST >> rw []) \\
2076 fs [GSYM real_lt] \\
2077 ‘z / e < 1’ by rw [REAL_LT_LDIV_EQ] \\
2078 Know ‘g (z / e) = z / e’
2079 >- (FIRST_X_ASSUM MATCH_MP_TAC >> rw [REAL_LT_IMP_LE]) >> Rewr' \\
2080 simp [Abbr ‘z’] \\
2081 MATCH_MP_TAC SET_DIST_LE_DIST >> rw [])
2082 (* applying SET_DIST_LIPSCHITZ *)
2083 >> rw [Abbr ‘a’, Abbr ‘b’]
2084 >> qmatch_abbrev_tac ‘e * abs (g (z1 / e) - g (z2 / e)) <= _’
2085 >> ‘0 <= z1 /\ 0 <= z2’ by rw [Abbr ‘z1’, Abbr ‘z2’, SET_DIST_POS_LE]
2086 >> Cases_on ‘e <= z1’
2087 >- (‘1 <= z1 / e’ by rw [REAL_LE_LDIV_EQ_NEG] \\
2088 ‘g (z1 / e) = 1’ by rw [] >> POP_ORW \\
2089 Cases_on ‘e <= z2’
2090 >- (‘1 <= z2 / e’ by rw [REAL_LE_LDIV_EQ_NEG] \\
2091 ‘g (z2 / e) = 1’ by rw [] >> POP_ORW \\
2092 simp [MDIST_POS_LE]) \\
2093 fs [GSYM real_lt] \\
2094 ‘z2 / e < 1’ by rw [REAL_LT_LDIV_EQ] \\
2095 Know ‘g (z2 / e) = z2 / e’
2096 >- (FIRST_X_ASSUM MATCH_MP_TAC >> rw [REAL_LT_IMP_LE]) >> Rewr' \\
2097 ‘0 < 1 - z2 / e’ by rw [REAL_SUB_LT] \\
2098 ‘abs (1 - z2 / e) = 1 - z2 / e’ by rw [ABS_REFL, REAL_LT_IMP_LE] \\
2099 POP_ORW \\
2100 simp [REAL_SUB_LDISTRIB, Abbr ‘z2’] \\
2101 Q_TAC (TRANS_TAC REAL_LE_TRANS) ‘z1 - set_dist E ({x},A)’ \\
2102 simp [REAL_LE_SUB_CANCEL2, Abbr ‘z1’] \\
2103 rw [Once MDIST_SYM] \\
2104 qmatch_abbrev_tac ‘(a :real) - b <= _’ \\
2105 Q_TAC (TRANS_TAC REAL_LE_TRANS) ‘abs (a - b)’ >> rw [ABS_LE] \\
2106 simp [Abbr ‘a’, Abbr ‘b’, SET_DIST_LIPSCHITZ])
2107 >> fs [GSYM real_lt]
2108 >> Cases_on ‘e <= z2’
2109 >- (‘1 <= z2 / e’ by rw [REAL_LE_LDIV_EQ_NEG] \\
2110 ‘g (z2 / e) = 1’ by rw [] >> POP_ORW \\
2111 ‘z1 / e < 1’ by rw [REAL_LT_LDIV_EQ] \\
2112 Know ‘g (z1 / e) = z1 / e’
2113 >- (FIRST_X_ASSUM MATCH_MP_TAC >> rw [REAL_LT_IMP_LE]) >> Rewr' \\
2114 ‘z1 / e - 1 < 0’ by rw [REAL_LT_SUB_RADD] \\
2115 ‘abs (z1 / e - 1) = -(z1 / e - 1)’ by rw [ABS_EQ_NEG] >> POP_ORW \\
2116 REWRITE_TAC [REAL_NEG_SUB] \\
2117 simp [REAL_SUB_LDISTRIB, Abbr ‘z1’] \\
2118 Q_TAC (TRANS_TAC REAL_LE_TRANS) ‘z2 - set_dist E ({y},A)’ \\
2119 simp [REAL_LE_SUB_CANCEL2, Abbr ‘z2’] \\
2120 qmatch_abbrev_tac ‘(a :real) - b <= _’ \\
2121 Q_TAC (TRANS_TAC REAL_LE_TRANS) ‘abs (a - b)’ >> rw [ABS_LE] \\
2122 simp [Abbr ‘a’, Abbr ‘b’, SET_DIST_LIPSCHITZ])
2123 >> fs [GSYM real_lt]
2124 >> ‘z1 / e < 1 /\ z2 / e < 1’ by rw [REAL_LT_LDIV_EQ]
2125 >> Know ‘g (z1 / e) = z1 / e’
2126 >- (FIRST_X_ASSUM MATCH_MP_TAC >> rw [REAL_LT_IMP_LE])
2127 >> Rewr'
2128 >> Know ‘g (z2 / e) = z2 / e’
2129 >- (FIRST_X_ASSUM MATCH_MP_TAC >> rw [REAL_LT_IMP_LE])
2130 >> Rewr'
2131 >> rw [REAL_DIV_SUB, ABS_DIV]
2132 >> ‘abs e = e’ by rw [ABS_REFL, REAL_LT_IMP_LE] >> POP_ORW
2133 >> simp [Abbr ‘z1’, Abbr ‘z2’]
2134 >> rw [Once MDIST_SYM, SET_DIST_LIPSCHITZ]
2135QED
2136
2137val _ = remove_ovl_mapping "B" {Name = "B", Thy = "metric"};
2138
2139(* END *)
2140
2141(* References:
2142
2143 [1] Klenke, A.: Probability Theory: A Comprehensive Course. Second Edition.
2144 Springer Science & Business Media, London (2013).
2145 [2] https://en.wikipedia.org/wiki/Lipschitz_continuity
2146 *)