topologyScript.sml
1(* ========================================================================= *)
2(* General Topology in Euclidean space (from hol-light's topology.ml) *)
3(* *)
4(* (c) Copyright, John Harrison 1998-2017 *)
5(* (c) Copyright, Valentina Bruno 2010 *)
6(* (c) Copyright, Marco Maggesi 2014-2017 *)
7(* (c) Copyright, Andrea Gabrielli 2016-2017 *)
8(* ========================================================================= *)
9(* Basic Set Theory (using predicates as sets) (from hol-light's sets.ml) *)
10(* *)
11(* (c) Copyright, University of Cambridge 1998 *)
12(* (c) Copyright, John Harrison 1998-2016 *)
13(* (c) Copyright, Marco Maggesi 2012-2017 *)
14(* (c) Copyright, Andrea Gabrielli 2012-2017 *)
15(* ========================================================================= *)
16(* General topological and metric spaces (from hol-light's metric.ml) *)
17(* *)
18(* (c) Copyright, John Harrison 1998-2017 *)
19(* (c) Copyright, Marco Maggesi 2014-2017 *)
20(* (c) Copyright, Andrea Gabrielli 2016-2017 *)
21(* ========================================================================= *)
22
23(* NOTE: this script is loaded after "integerTheory" and before "realTheory".
24 General topology theorems without using real numbers should be put here.
25
26 See src/real/analysis/real_topologyTheory for Elementary Topology of
27 (one-dimensional) Euclidean space.
28 *)
29Theory topology
30Ancestors
31 pair combin pred_set arithmetic relation cardinal
32Libs
33 boolSimps simpLib mesonLib metisLib pairLib tautLib hurdUtils
34
35
36fun METIS ths tm = prove(tm,METIS_TAC ths);
37
38val DISC_RW_KILL = DISCH_TAC THEN ONCE_ASM_REWRITE_TAC [] THEN
39 POP_ASSUM K_TAC;
40
41(* Begin of minimal hol-light compatibility layer *)
42Theorem IMP_CONJ = cardinalTheory.CONJ_EQ_IMP
43Theorem IMP_IMP = boolTheory.AND_IMP_INTRO
44Theorem EQ_IMP = boolTheory.EQ_IMPLIES
45
46Theorem FINITE_SUBSET = pred_setTheory.SUBSET_FINITE_I
47
48val REPLICATE_TAC = NTAC;
49val ANTS_TAC = impl_tac;
50
51Theorem LEFT_AND_EXISTS_THM = GSYM LEFT_EXISTS_AND_THM
52Theorem RIGHT_AND_EXISTS_THM = GSYM RIGHT_EXISTS_AND_THM
53
54Theorem FORALL_UNWIND_THM2 :
55 !P (a :'a). (!x. x = a ==> P x) <=> P a
56Proof
57 METIS_TAC []
58QED
59
60Theorem FORALL_UNWIND_THM1 :
61 !P (a :'a). (!x. a = x ==> P x) <=> P a
62Proof
63 REPEAT GEN_TAC THEN CONV_TAC(LAND_CONV(ONCE_DEPTH_CONV SYM_CONV)) THEN
64 MATCH_ACCEPT_TAC FORALL_UNWIND_THM2
65QED
66
67val SUBSET_DIFF = DIFF_SUBSET; (* |- !s t. s DIFF t SUBSET s *)
68(* End of minimal hol-light compatibility layer *)
69
70(*---------------------------------------------------------------------------*)
71(* Characterize an (alpha)topology *)
72(*---------------------------------------------------------------------------*)
73
74(* localized notion of open sets (one set being open in another) *)
75Definition istopology :
76 istopology L =
77 ({} IN L /\
78 (!s t. s IN L /\ t IN L ==> (s INTER t) IN L) /\
79 (!k. k SUBSET L ==> (BIGUNION k) IN L))
80End
81
82Theorem EXISTS_istopology[local]:
83 ?t. istopology t
84Proof
85 EXISTS_TAC ``univ(:'a set)``
86 >> REWRITE_TAC [istopology, IN_UNIV]
87QED
88
89val topology_tydef = new_type_definition
90 ("topology", EXISTS_istopology);
91
92val topology_tybij = define_new_type_bijections
93 {name="topology_tybij",
94 ABS="topology", REP="open_in",tyax=topology_tydef};
95
96Theorem ISTOPOLOGY_OPEN_IN: !top. istopology (open_in top)
97Proof
98 PROVE_TAC [topology_tybij]
99QED
100
101Theorem TOPOLOGY_EQ:
102 !top1 top2. (top1 = top2) <=> !s. (open_in top1) s <=> (open_in top2) s
103Proof
104 REPEAT GEN_TAC THEN simp[GSYM FUN_EQ_THM] THEN
105 REWRITE_TAC[ETA_AX] THEN PROVE_TAC[topology_tybij]
106QED
107
108(* global (abstract) notion of open sets *)
109Definition open_DEF[nocompute]: open (s :'a topology) = (open_in s) UNIV
110End
111
112(* ------------------------------------------------------------------------- *)
113(* Infer the "universe" from union of all sets in the topology. *)
114(* ------------------------------------------------------------------------- *)
115
116Definition topspace[nocompute]:
117 topspace top = BIGUNION {s | (open_in top) s}
118End
119
120(* the "universe" of global topology is the universe itself *)
121Theorem open_topspace: !top. open top ==> (topspace top = UNIV)
122Proof
123 GEN_TAC >> REWRITE_TAC [open_DEF]
124 >> DISCH_TAC >> REWRITE_TAC [EXTENSION]
125 >> REWRITE_TAC [topspace, IN_UNIV, IN_BIGUNION]
126 >> GEN_TAC >> Q.EXISTS_TAC `UNIV`
127 >> REWRITE_TAC [IN_UNIV, GSPECIFICATION]
128 >> Q.EXISTS_TAC `UNIV` >> BETA_TAC
129 >> ASM_SIMP_TAC std_ss []
130QED
131
132(* ------------------------------------------------------------------------- *)
133(* Main properties of open sets. *)
134(* ------------------------------------------------------------------------- *)
135
136Theorem OPEN_IN_CLAUSES:
137 !top.
138 open_in top {} /\
139 (!s t. open_in top s /\ open_in top t ==> open_in top (s INTER t)) /\
140 (!k. (!s. s IN k ==> open_in top s) ==> open_in top (BIGUNION k))
141Proof
142 SIMP_TAC std_ss [IN_DEF, SUBSET_DEF,
143 SIMP_RULE std_ss [istopology, IN_DEF, SUBSET_DEF] ISTOPOLOGY_OPEN_IN]
144QED
145
146Theorem OPEN_IN_SUBSET:
147 !top s. open_in top s ==> s SUBSET (topspace top)
148Proof
149 REWRITE_TAC[topspace] THEN SET_TAC[]
150QED
151
152Theorem OPEN_IN_EMPTY:
153 !top. open_in top {}
154Proof
155 REWRITE_TAC[OPEN_IN_CLAUSES]
156QED
157
158Theorem OPEN_IN_INTER:
159 !top s t. open_in top s /\ open_in top t ==> open_in top (s INTER t)
160Proof
161 REWRITE_TAC[OPEN_IN_CLAUSES]
162QED
163
164Theorem OPEN_IN_BIGUNION:
165 !top k. (!s. s IN k ==> open_in top s) ==> open_in top (BIGUNION k)
166Proof
167 REWRITE_TAC[OPEN_IN_CLAUSES]
168QED
169
170Theorem OPEN_IN_UNIONS[local] = OPEN_IN_BIGUNION
171
172Theorem BIGUNION_2:
173 !s t. BIGUNION {s;t} = s UNION t
174Proof
175 SET_TAC[]
176QED
177
178Theorem OPEN_IN_UNION:
179 !top s t. open_in top s /\ open_in top t ==> open_in top (s UNION t)
180Proof
181 REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM BIGUNION_2] THEN
182 MATCH_MP_TAC OPEN_IN_BIGUNION THEN REPEAT (POP_ASSUM MP_TAC) THEN SET_TAC[]
183QED
184
185Theorem OPEN_IN_TOPSPACE:
186 !top. open_in top (topspace top)
187Proof
188 SIMP_TAC std_ss [topspace, OPEN_IN_BIGUNION, GSPECIFICATION]
189QED
190
191Theorem OPEN_IN_BIGINTER:
192 !top s:('a->bool)->bool.
193 FINITE s /\ ~(s = {}) /\ (!t. t IN s ==> open_in top t)
194 ==> open_in top (BIGINTER s)
195Proof
196 GEN_TAC THEN REWRITE_TAC[GSYM AND_IMP_INTRO] THEN
197 KNOW_TAC ``!s. (s <> {} ==> (!t. t IN s ==> open_in top t) ==>
198 open_in top (BIGINTER s)) =
199 (\s. s <> {} ==> (!t. t IN s ==> open_in top t) ==>
200 open_in top (BIGINTER s)) s`` THENL
201 [FULL_SIMP_TAC std_ss [], ALL_TAC] THEN DISC_RW_KILL THEN
202 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
203 REWRITE_TAC[BIGINTER_INSERT, AND_IMP_INTRO, NOT_INSERT_EMPTY,
204 FORALL_IN_INSERT] THEN
205 SIMP_TAC std_ss [GSYM RIGHT_FORALL_IMP_THM] THEN
206 MAP_EVERY X_GEN_TAC [``f:('a->bool)->bool``, ``s:'a->bool``] THEN
207 ASM_CASES_TAC ``f:('a->bool)->bool = {}`` THEN
208 ASM_SIMP_TAC std_ss [BIGINTER_EMPTY, INTER_UNIV] THEN REPEAT STRIP_TAC THEN
209 MATCH_MP_TAC OPEN_IN_INTER THEN ASM_SIMP_TAC std_ss []
210QED
211
212Theorem OPEN_IN_INTERS[local] = OPEN_IN_BIGINTER
213
214Theorem OPEN_IN_SUBOPEN:
215 !top s:'a->bool.
216 open_in top s <=>
217 !x. x IN s ==> ?t. open_in top t /\ x IN t /\ t SUBSET s
218Proof
219 REPEAT GEN_TAC THEN EQ_TAC THENL [PROVE_TAC[SUBSET_REFL], ALL_TAC] THEN
220 SIMP_TAC std_ss [GSYM RIGHT_EXISTS_IMP_THM, SKOLEM_THM] THEN
221 REWRITE_TAC[DECIDE ``a ==> b /\ c <=> (a ==> b) /\ (a ==> c)``] THEN
222 SIMP_TAC std_ss [FORALL_AND_THM, GSYM LEFT_EXISTS_IMP_THM] THEN
223 ONCE_REWRITE_TAC[GSYM FORALL_IN_IMAGE] THEN REPEAT STRIP_TAC THEN
224 FIRST_X_ASSUM(MP_TAC o MATCH_MP OPEN_IN_BIGUNION) THEN
225 MATCH_MP_TAC EQ_IMPLIES THEN AP_TERM_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN
226 SET_TAC[]
227QED
228
229(*---------------------------------------------------------------------------*)
230(* Characterize a neighbourhood of a point relative to a topology *)
231(*---------------------------------------------------------------------------*)
232
233Definition neigh:
234 neigh(top)(N,(x:'a)) = ?P. (open_in top) P /\ P SUBSET N /\ P x /\
235 N SUBSET topspace top
236End
237
238Theorem neigh_def :
239 !top N x. neigh top (N,x) <=>
240 ?P. open_in top P /\ P SUBSET N /\ x IN P /\ N SUBSET topspace top
241Proof
242 REWRITE_TAC [neigh, IN_APP]
243QED
244
245(*---------------------------------------------------------------------------*)
246(* Prove various properties / characterizations of open sets *)
247(*---------------------------------------------------------------------------*)
248
249Theorem OPEN_OWN_NEIGH:
250 !A top. !x:'a. open_in(top) A /\ A x ==> neigh(top)(A,x)
251Proof
252 REPEAT STRIP_TAC THEN REWRITE_TAC[neigh] THEN Q.EXISTS_TAC ‘A’ THEN
253 simp[SUBSET_REFL, OPEN_IN_SUBSET]
254QED
255
256Theorem OPEN_UNOPEN :
257 !S' top. open_in(top) S' <=>
258 (BIGUNION {P | open_in(top) P /\ P SUBSET S'} = S')
259Proof
260 rpt GEN_TAC >> EQ_TAC >|
261 [ DISCH_TAC THEN ONCE_REWRITE_TAC[SET_EQ_SUBSET] THEN
262 ASM_SIMP_TAC (srw_ss()) [BIGUNION_applied, SUBSET_applied] THEN
263 CONJ_TAC THEN GEN_TAC THENL [
264 DISCH_THEN(Q.X_CHOOSE_THEN `s` STRIP_ASSUME_TAC) THEN
265 FIRST_ASSUM MATCH_MP_TAC THEN
266 FULL_SIMP_TAC (srw_ss()) [IN_DEF],
267 DISCH_TAC THEN EXISTS_TAC ``S':'a->bool`` THEN
268 ASM_SIMP_TAC(srw_ss())[IN_DEF]
269 ],
270 DISCH_THEN(SUBST1_TAC o SYM) THEN
271 MATCH_MP_TAC OPEN_IN_BIGUNION THEN
272 SIMP_TAC (srw_ss()) [] ]
273QED
274
275Theorem OPEN_SUBOPEN:
276 !S' top. open_in(top) S' <=>
277 !x:'a. S' x ==> ?P. P x /\ open_in(top) P /\ P SUBSET S'
278Proof
279 REPEAT GEN_TAC THEN EQ_TAC THENL [
280 DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
281 EXISTS_TAC “S':'a->bool” THEN ASM_REWRITE_TAC[SUBSET_REFL],
282 DISCH_TAC THEN C SUBGOAL_THEN SUBST1_TAC
283 ``S' = BIGUNION { P | open_in(top) P /\ P SUBSET S'}`` THENL
284 [ONCE_REWRITE_TAC[SET_EQ_SUBSET] THEN CONJ_TAC THENL
285 [ONCE_REWRITE_TAC[SUBSET_applied] THEN
286 ASM_SIMP_TAC (srw_ss()) [] THEN
287 ASM_SIMP_TAC (srw_ss()) [IN_DEF],
288 SIMP_TAC (srw_ss()) [SUBSET_applied] THEN REPEAT STRIP_TAC THEN
289 FULL_SIMP_TAC (srw_ss()) [IN_DEF]],
290 MATCH_MP_TAC OPEN_IN_BIGUNION THEN
291 SIMP_TAC (srw_ss()) []]]
292QED
293
294Theorem OPEN_NEIGH:
295 !A top.
296 open_in(top) A <=> !x:'a. A x ==> ?N. neigh(top)(N,x) /\ N SUBSET A
297Proof
298 REPEAT GEN_TAC THEN EQ_TAC THENL [
299 REPEAT STRIP_TAC THEN simp[neigh, PULL_EXISTS] THEN
300 REPEAT (Q.EXISTS_TAC ‘A’) THEN simp[OPEN_IN_SUBSET]
301 ,
302 DISCH_TAC THEN ONCE_REWRITE_TAC[OPEN_SUBOPEN] THEN REPEAT STRIP_TAC THEN
303 first_assum $ drule_then strip_assume_tac THEN gs[neigh] THEN
304 metis_tac[SUBSET_TRANS]
305 ]
306QED
307
308Theorem OPEN_NEIGH' :
309 !A top. open_in(top) A <=> !x. x IN A ==> ?N. neigh(top)(N,x) /\ N SUBSET A
310Proof
311 REWRITE_TAC [OPEN_NEIGH, IN_APP]
312QED
313
314(*---------------------------------------------------------------------------*)
315(* Characterize closed sets in a topological space *)
316(*---------------------------------------------------------------------------*)
317
318Definition closed_in:
319 closed_in top s <=>
320 s SUBSET (topspace top) /\ open_in top (topspace top DIFF s)
321End
322
323(* global (abstract) notion of closed sets *)
324Definition closed_DEF: closed (s :'a topology) = (closed_in s) UNIV
325End
326
327Theorem closed_topspace: !top. closed top ==> (topspace top = UNIV)
328Proof
329 GEN_TAC >> REWRITE_TAC [closed_DEF, closed_in]
330 >> REWRITE_TAC [UNIV_SUBSET]
331 >> STRIP_TAC >> ASM_REWRITE_TAC []
332QED
333
334(* original definition of "closed_in" in HOL4 *)
335Theorem CLOSED_IN_OPEN_IN_COMPL:
336 !top. closed top ==> (!s. closed_in top s = open_in top (COMPL s))
337Proof
338 rpt STRIP_TAC
339 >> IMP_RES_TAC closed_topspace
340 >> ASM_REWRITE_TAC [closed_in, GSYM COMPL_DEF, SUBSET_UNIV]
341QED
342
343Theorem CLOSED_IN_SUBSET:
344 !top s. closed_in top s ==> s SUBSET (topspace top)
345Proof
346 PROVE_TAC[closed_in]
347QED
348
349Theorem CLOSED_IN_EMPTY[simp]: !top. closed_in top {}
350Proof
351 REWRITE_TAC[closed_in, EMPTY_SUBSET, DIFF_EMPTY, OPEN_IN_TOPSPACE]
352QED
353
354Theorem CLOSED_IN_TOPSPACE[simp]: !top. closed_in top (topspace top)
355Proof
356 REWRITE_TAC[closed_in, SUBSET_REFL, DIFF_EQ_EMPTY, OPEN_IN_EMPTY]
357QED
358
359Theorem CLOSED_IN_UNION:
360 !top s t. closed_in top s /\ closed_in top t ==> closed_in top (s UNION t)
361Proof
362 SIMP_TAC std_ss [closed_in, UNION_SUBSET, OPEN_IN_INTER,
363 SET_RULE “u DIFF (s UNION t) = (u DIFF s) INTER (u DIFF t)”]
364QED
365
366Theorem CLOSED_IN_BIGINTER:
367 !top k:('a->bool)->bool.
368 k <> {} /\ (!s. s IN k ==> closed_in top s) ==> closed_in top (BIGINTER k)
369Proof
370 REPEAT GEN_TAC THEN REWRITE_TAC[closed_in] THEN REPEAT STRIP_TAC THENL
371 [REPEAT (POP_ASSUM MP_TAC) THEN SET_TAC[], ALL_TAC] THEN
372 SUBGOAL_THEN “topspace top DIFF BIGINTER k :'a->bool =
373 BIGUNION {topspace top DIFF s | s IN k}” SUBST1_TAC
374 THENL [ALL_TAC,
375 MATCH_MP_TAC OPEN_IN_BIGUNION THEN REPEAT (POP_ASSUM MP_TAC) THEN
376 SET_TAC[]
377 ] THEN simp[Once EXTENSION] THEN
378 KNOW_TAC
379 “{topspace top DIFF s | s IN k} = IMAGE (\s. topspace top DIFF s) k” THENL
380 [FULL_SIMP_TAC std_ss [GSYM IMAGE_DEF], ALL_TAC] THEN DISC_RW_KILL THEN
381 REWRITE_TAC [IN_BIGUNION, IN_BIGINTER] THEN
382 simp[PULL_EXISTS] THEN METIS_TAC[]
383QED
384
385Theorem CLOSED_IN_INTER:
386 !top s t. closed_in top s /\ closed_in top t ==> closed_in top (s INTER t)
387Proof
388 REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM BIGINTER_2] THEN
389 MATCH_MP_TAC CLOSED_IN_BIGINTER THEN REPEAT (POP_ASSUM MP_TAC) THEN
390 SET_TAC[]
391QED
392
393Theorem OPEN_IN_CLOSED_IN_EQ:
394 !top s. open_in top s <=>
395 s SUBSET topspace top /\ closed_in top (topspace top DIFF s)
396Proof
397 REWRITE_TAC[closed_in, SET_RULE ``(u DIFF s) SUBSET u``] THEN
398 REWRITE_TAC[SET_RULE ``u DIFF (u DIFF s) = u INTER s``] THEN
399 PROVE_TAC[OPEN_IN_SUBSET, SET_RULE ``s SUBSET t ==> (t INTER s = s)``]
400QED
401
402Theorem OPEN_IN_CLOSED_IN:
403 !top s. s SUBSET topspace top
404 ==> (open_in top s <=> closed_in top (topspace top DIFF s))
405Proof
406 SIMP_TAC std_ss [OPEN_IN_CLOSED_IN_EQ]
407QED
408
409Theorem OPEN_IN_DIFF:
410 !top s t:'a->bool.
411 open_in top s /\ closed_in top t ==> open_in top (s DIFF t)
412Proof
413 REPEAT STRIP_TAC THEN
414 SUBGOAL_THEN ``s DIFF t :'a->bool = s INTER (topspace top DIFF t)``
415 SUBST1_TAC THENL
416 [FIRST_X_ASSUM(MP_TAC o MATCH_MP OPEN_IN_SUBSET) THEN SET_TAC[],
417 MATCH_MP_TAC OPEN_IN_INTER THEN PROVE_TAC[closed_in]]
418QED
419
420Theorem CLOSED_IN_DIFF:
421 !top s t:'a->bool.
422 closed_in top s /\ open_in top t ==> closed_in top (s DIFF t)
423Proof
424 REPEAT STRIP_TAC THEN
425 SUBGOAL_THEN ``s DIFF t :'a->bool = s INTER (topspace top DIFF t)``
426 SUBST1_TAC THENL
427 [FIRST_X_ASSUM(MP_TAC o MATCH_MP CLOSED_IN_SUBSET) THEN SET_TAC[],
428 MATCH_MP_TAC CLOSED_IN_INTER THEN PROVE_TAC[OPEN_IN_CLOSED_IN_EQ]]
429QED
430
431Theorem CLOSED_IN_BIGUNION:
432 !top s. FINITE s /\ (!t. t IN s ==> closed_in top t)
433 ==> closed_in top (BIGUNION s)
434Proof
435 GEN_TAC THEN REWRITE_TAC[GSYM AND_IMP_INTRO] THEN
436 KNOW_TAC ``!s. ((!t. t IN s ==> closed_in top t) ==>
437 closed_in top (BIGUNION s)) =
438 (\s. (!t. t IN s ==> closed_in top t) ==>
439 closed_in top (BIGUNION s)) s`` THENL
440 [FULL_SIMP_TAC std_ss [], ALL_TAC] THEN DISC_RW_KILL THEN
441 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
442 REWRITE_TAC[BIGUNION_INSERT, BIGUNION_EMPTY, CLOSED_IN_EMPTY, IN_INSERT] THEN
443 PROVE_TAC[CLOSED_IN_UNION]
444QED
445
446(*---------------------------------------------------------------------------*)
447(* Define limit point in topological space *)
448(*---------------------------------------------------------------------------*)
449
450Definition limpt:
451 limpt(top) x S' <=>
452 x IN topspace top /\
453 !N:'a->bool. neigh(top)(N,x) ==> ?y. ~(x = y) /\ S' y /\ N y
454End
455
456(* Alternative characterisation without needing neigh, but using IN, rather
457 than application. x is a limit point in A if any neighbour set U containing
458 x, also contains a different point y of A, i.e. x has neighbour points at
459 any "close" distance.
460 *)
461Theorem limpt_thm:
462 !top x A. limpt top (x :'a) A <=>
463 x IN topspace top /\
464 !U. open_in(top) U /\ x IN U ==> ?y. y IN U /\ y IN A /\ y <> x
465Proof
466 rw[limpt, neigh, PULL_EXISTS] >> EQ_TAC >>
467 rw[] >> fs[IN_DEF]
468 >- metis_tac[SUBSET_REFL, OPEN_IN_SUBSET]
469 >> metis_tac[SUBSET_DEF, IN_DEF]
470QED
471
472(*---------------------------------------------------------------------------*)
473(* Prove that a set is closed iff it contains all its limit points *)
474(*---------------------------------------------------------------------------*)
475
476Theorem CLOSED_LIMPT:
477 !top. closed top ==>
478 !S'. closed_in(top) S' <=> !x:'a. limpt(top) x S' ==> S' x
479Proof
480 GEN_TAC >> DISCH_TAC
481 >> IMP_RES_TAC closed_topspace
482 >> GEN_TAC >> CONV_TAC (ONCE_DEPTH_CONV CONTRAPOS_CONV)
483 >> REWRITE_TAC[closed_in, limpt]
484 >> ASM_REWRITE_TAC [SUBSET_UNIV, GSYM COMPL_DEF, IN_UNIV]
485 >> CONV_TAC(ONCE_DEPTH_CONV NOT_FORALL_CONV)
486 >> ‘!x. S' x = ~COMPL S' x’ by rw [COMPL_applied, IN_APP]
487 >> ASM_REWRITE_TAC []
488 >> SPEC_TAC(“COMPL(S':'a->bool)”,“S':'a->bool”)
489 >> GEN_TAC >> REWRITE_TAC [NOT_IMP]
490 >> CONV_TAC (ONCE_DEPTH_CONV NOT_EXISTS_CONV)
491 >> REWRITE_TAC [DE_MORGAN_THM]
492 >> REWRITE_TAC [OPEN_NEIGH, SUBSET_applied]
493 >> AP_TERM_TAC >> ABS_TAC
494 >> ASM_CASES_TAC “(S':'a->bool) x” >> ASM_REWRITE_TAC []
495 >> METIS_TAC[]
496QED
497
498(* ------------------------------------------------------------------------- *)
499(* A generic notion of "hull" (convex, affine, conic hull and closure). *)
500(* ------------------------------------------------------------------------- *)
501
502(* HOL-Light: parse_as_infix("hull",(21,"left"));; *)
503val _ = set_fixity "hull" (Infix(NONASSOC, 499));
504
505Definition hull[nocompute]:
506 P hull s = BIGINTER {t | P t /\ s SUBSET t}
507End
508
509Theorem HULL_P:
510 !P s. P s ==> (P hull s = s)
511Proof
512 SIMP_TAC std_ss [hull, EXTENSION, IN_BIGINTER, GSPECIFICATION] THEN
513 MESON_TAC[SUBSET_DEF]
514QED
515
516Theorem P_HULL:
517 !P s. (!f. (!s. s IN f ==> P s) ==> P(BIGINTER f)) ==> P(P hull s)
518Proof
519 REWRITE_TAC[hull] THEN SIMP_TAC std_ss [GSPECIFICATION]
520QED
521
522Theorem HULL_EQ:
523 !P s. (!f. (!s. s IN f ==> P s) ==> P(BIGINTER f))
524 ==> ((P hull s = s) <=> P s)
525Proof
526 MESON_TAC[P_HULL, HULL_P]
527QED
528
529Theorem HULL_HULL:
530 !P s. P hull (P hull s) = P hull s
531Proof
532 SIMP_TAC std_ss [hull, EXTENSION, IN_BIGINTER, GSPECIFICATION, SUBSET_DEF] >>
533 METIS_TAC[]
534QED
535
536Theorem HULL_SUBSET:
537 !P s. s SUBSET (P hull s)
538Proof
539 SIMP_TAC std_ss [hull,SUBSET_DEF,IN_BIGINTER,GSPECIFICATION] >> MESON_TAC[]
540QED
541
542Theorem HULL_MONO:
543 !P s t. s SUBSET t ==> (P hull s) SUBSET (P hull t)
544Proof
545 SIMP_TAC std_ss [hull, SUBSET_DEF, IN_BIGINTER, GSPECIFICATION] THEN
546 METIS_TAC[]
547QED
548
549Theorem HULL_ANTIMONO:
550 !P Q s. P SUBSET Q ==> (Q hull s) SUBSET (P hull s)
551Proof
552 SIMP_TAC std_ss [SUBSET_DEF, hull, IN_BIGINTER, GSPECIFICATION] THEN
553 MESON_TAC[IN_DEF]
554QED
555
556Theorem HULL_MINIMAL:
557 !P s t. s SUBSET t /\ P t ==> (P hull s) SUBSET t
558Proof
559 SIMP_TAC std_ss [hull,SUBSET_DEF,IN_BIGINTER,GSPECIFICATION] >> METIS_TAC[]
560QED
561
562Theorem SUBSET_HULL:
563 !P s t. P t ==> ((P hull s) SUBSET t <=> s SUBSET t)
564Proof
565 SIMP_TAC std_ss [hull,SUBSET_DEF,IN_BIGINTER,GSPECIFICATION] >> METIS_TAC[]
566QED
567
568Theorem HULL_UNIQUE:
569 !P s t. s SUBSET t /\ P t /\ (!t'. s SUBSET t' /\ P t' ==> t SUBSET t')
570 ==> (P hull s = t)
571Proof
572 REPEAT STRIP_TAC THEN MATCH_MP_TAC SUBSET_ANTISYM THEN
573 SIMP_TAC std_ss [hull, SUBSET_DEF, IN_BIGINTER, GSPECIFICATION] THEN
574 ASM_MESON_TAC[SUBSET_HULL, SUBSET_DEF]
575QED
576
577Theorem HULL_UNION_SUBSET:
578 !P s t. (P hull s) UNION (P hull t) SUBSET (P hull (s UNION t))
579Proof
580 SIMP_TAC std_ss [UNION_SUBSET, HULL_MONO, SUBSET_UNION]
581QED
582
583Theorem HULL_UNION:
584 !P s t. P hull (s UNION t) = P hull ((P hull s) UNION (P hull t))
585Proof
586 REPEAT STRIP_TAC >> ONCE_REWRITE_TAC[hull] >>
587 AP_TERM_TAC >> SIMP_TAC std_ss [EXTENSION, GSPECIFICATION, UNION_SUBSET] >>
588 METIS_TAC[SUBSET_HULL]
589QED
590
591Theorem HULL_UNION_LEFT:
592 !P s t:'a->bool.
593 P hull (s UNION t) = P hull ((P hull s) UNION t)
594Proof
595 REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[hull] THEN
596 AP_TERM_TAC THEN SIMP_TAC std_ss [EXTENSION, GSPECIFICATION, UNION_SUBSET] >>
597 METIS_TAC[SUBSET_HULL]
598QED
599
600Theorem HULL_UNION_RIGHT:
601 !P s t:'a->bool.
602 P hull (s UNION t) = P hull (s UNION (P hull t))
603Proof
604 REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[hull] THEN
605 AP_TERM_TAC THEN SIMP_TAC std_ss [EXTENSION, GSPECIFICATION, UNION_SUBSET] >>
606 MESON_TAC[SUBSET_HULL]
607QED
608
609Theorem HULL_REDUNDANT_EQ:
610 !P a s. a IN (P hull s) <=> (P hull (a INSERT s) = P hull s)
611Proof
612 REWRITE_TAC[hull] THEN SET_TAC[]
613QED
614
615Theorem HULL_REDUNDANT:
616 !P a s. a IN (P hull s) ==> (P hull (a INSERT s) = P hull s)
617Proof
618 REWRITE_TAC[HULL_REDUNDANT_EQ]
619QED
620
621Theorem HULL_INDUCT:
622 !P p s. (!x:'a. x IN s ==> p x) /\ P {x | p x}
623 ==> !x. x IN P hull s ==> p x
624Proof
625 REPEAT GEN_TAC THEN
626 MP_TAC(ISPECL [``P:('a->bool)->bool``, ``s:'a->bool``, ``{x:'a | p x}``]
627 HULL_MINIMAL) THEN
628 SIMP_TAC std_ss [SUBSET_DEF, GSPECIFICATION]
629QED
630
631Theorem HULL_INC:
632 !P s x. x IN s ==> x IN P hull s
633Proof
634 MESON_TAC[REWRITE_RULE[SUBSET_DEF] HULL_SUBSET]
635QED
636
637Theorem HULL_IMAGE_SUBSET:
638 !P f s. (P (P hull s)) /\ (!s. P s ==> P(IMAGE f s))
639 ==> (P hull (IMAGE f s)) SUBSET ((IMAGE f (P hull s)))
640Proof
641 REPEAT STRIP_TAC THEN MATCH_MP_TAC HULL_MINIMAL THEN
642 ASM_SIMP_TAC std_ss [IMAGE_SUBSET, HULL_SUBSET]
643QED
644
645Theorem HULL_IMAGE_GALOIS:
646 !P f g s. (!s. P(P hull s)) /\
647 (!s. P s ==> P(IMAGE f s)) /\ (!s. P s ==> P(IMAGE g s)) /\
648 (!s t. s SUBSET IMAGE g t <=> IMAGE f s SUBSET t) ==>
649 P hull (IMAGE f s) = IMAGE f (P hull s)
650Proof
651 REPEAT STRIP_TAC THEN MATCH_MP_TAC SUBSET_ANTISYM THEN
652 ASM_SIMP_TAC std_ss [HULL_IMAGE_SUBSET] THEN
653 first_assum (REWRITE_TAC o single o GSYM) THEN
654 MATCH_MP_TAC HULL_MINIMAL THEN
655 ASM_SIMP_TAC std_ss [HULL_SUBSET]
656QED
657
658Theorem HULL_IMAGE:
659 !P f s. (!s. P(P hull s)) /\ (!s. P(IMAGE f s) <=> P s) /\
660 (!x y:'a. (f x = f y) ==> (x = y)) /\ (!y. ?x. f x = y) ==>
661 P hull (IMAGE f s) = IMAGE f (P hull s)
662Proof
663 REPEAT GEN_TAC THEN STRIP_TAC THEN
664 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
665 REWRITE_TAC [AND_IMP_INTRO] THEN
666 SIMP_TAC std_ss [SET_RULE ``!f. (!x y. (f x = f y) ==> (x = y)) /\
667 (!y. ?x. f x = y) <=> ?g. (!y. f (g y) = y) /\ !x. g (f x) = x``] THEN
668 DISCH_THEN(X_CHOOSE_THEN ``g:'a->'a`` STRIP_ASSUME_TAC) THEN
669 MATCH_MP_TAC HULL_IMAGE_GALOIS THEN EXISTS_TAC ``g:'a->'a`` THEN
670 ASM_REWRITE_TAC[] >> CONJ_TAC >| [ALL_TAC,
671 REPEAT (POP_ASSUM MP_TAC) >> SET_TAC[]
672 ] THEN X_GEN_TAC ``s:'a->bool`` THEN
673 FIRST_X_ASSUM(CONV_TAC o RAND_CONV o REWR_CONV o GSYM) THEN
674 MATCH_MP_TAC EQ_IMPLIES THEN AP_TERM_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN
675 SET_TAC[]
676QED
677
678Theorem IS_HULL:
679 !P s. (!f. (!s. s IN f ==> P s) ==> P(BIGINTER f))
680 ==> (P s <=> ?t. s = P hull t)
681Proof
682 MESON_TAC[HULL_P, P_HULL]
683QED
684
685Theorem HULLS_EQ:
686 !P s t.
687 (!f. (!s. s IN f ==> P s) ==> P (BIGINTER f)) /\
688 s SUBSET (P hull t) /\ t SUBSET (P hull s)
689 ==> (P hull s = P hull t)
690Proof
691 REPEAT STRIP_TAC THEN MATCH_MP_TAC SUBSET_ANTISYM THEN
692 CONJ_TAC THEN MATCH_MP_TAC HULL_MINIMAL THEN
693 ASM_SIMP_TAC std_ss [P_HULL]
694QED
695
696Theorem HULL_P_AND_Q:
697 !P Q. (!f. (!s. s IN f ==> P s) ==> P(BIGINTER f)) /\
698 (!f. (!s. s IN f ==> Q s) ==> Q(BIGINTER f)) /\
699 (!s. Q s ==> Q(P hull s))
700 ==> ((\x. P x /\ Q x) hull s = P hull (Q hull s))
701Proof
702 REPEAT STRIP_TAC THEN
703 MATCH_MP_TAC HULL_UNIQUE THEN ASM_SIMP_TAC std_ss [HULL_INC, SUBSET_HULL] THEN
704 ASM_MESON_TAC[P_HULL, HULL_SUBSET, SUBSET_TRANS]
705QED
706
707(* ------------------------------------------------------------------------- *)
708(* Subspace topology (from real_topologyTheory) *)
709(* ------------------------------------------------------------------------- *)
710
711Definition subtopology :
712 subtopology top u = topology {s INTER u | open_in top s}
713End
714
715Theorem ISTOPOLOGY_SUBTOPOLOGY :
716 !top u:'a->bool. istopology {s INTER u | open_in top s}
717Proof
718 REWRITE_TAC[istopology, SET_RULE
719 ``{s INTER u | open_in top s} =
720 IMAGE (\s. s INTER u) {s | open_in top s}``] THEN
721 SIMP_TAC std_ss [GSYM AND_IMP_INTRO, FORALL_IN_IMAGE, RIGHT_FORALL_IMP_THM] >>
722 SIMP_TAC std_ss [SUBSET_IMAGE, IN_IMAGE, GSPECIFICATION, SUBSET_DEF] THEN
723 REPEAT GEN_TAC THEN REPEAT CONJ_TAC THENL [
724 EXISTS_TAC ``{}:'a->bool`` THEN REWRITE_TAC[OPEN_IN_EMPTY, INTER_EMPTY],
725 SIMP_TAC std_ss [
726 SET_RULE ``(s INTER u) INTER (t INTER u) = (s INTER t) INTER u``] THEN
727 ASM_MESON_TAC[OPEN_IN_INTER],
728 X_GEN_TAC ``f:('a->bool)->bool`` THEN
729 DISCH_THEN (X_CHOOSE_TAC ``g:('a->bool)->bool``) THEN
730 EXISTS_TAC ``BIGUNION g :'a->bool`` THEN
731 ASM_SIMP_TAC std_ss [OPEN_IN_BIGUNION, INTER_BIGUNION] THEN SET_TAC[]]
732QED
733
734Theorem OPEN_IN_SUBTOPOLOGY :
735 !top u s. open_in (subtopology top u) s <=>
736 ?t. open_in top t /\ (s = t INTER u)
737Proof
738 REWRITE_TAC[subtopology] THEN
739 SIMP_TAC std_ss [
740 REWRITE_RULE[CONJUNCT2 topology_tybij] ISTOPOLOGY_SUBTOPOLOGY] THEN
741 simp[] THEN METIS_TAC []
742QED
743
744Theorem TOPSPACE_SUBTOPOLOGY[simp]:
745 !top u. topspace(subtopology top u) = topspace top INTER u
746Proof
747 REWRITE_TAC[topspace, OPEN_IN_SUBTOPOLOGY, INTER_BIGUNION] THEN
748 REPEAT STRIP_TAC THEN AP_TERM_TAC THEN simp[Once EXTENSION] THEN
749 METIS_TAC []
750QED
751
752Theorem CLOSED_IN_SUBTOPOLOGY :
753 !top u s. closed_in (subtopology top u) s <=>
754 ?t:'a->bool. closed_in top t /\ (s = t INTER u)
755Proof
756 REWRITE_TAC[closed_in, TOPSPACE_SUBTOPOLOGY] THEN
757 SIMP_TAC std_ss [SUBSET_INTER,OPEN_IN_SUBTOPOLOGY,GSYM RIGHT_EXISTS_AND_THM]>>
758 REPEAT STRIP_TAC THEN EQ_TAC THEN
759 DISCH_THEN(X_CHOOSE_THEN ``t:'a->bool`` STRIP_ASSUME_TAC) THEN
760 EXISTS_TAC ``topspace top DIFF t :'a->bool`` THEN
761 ASM_SIMP_TAC std_ss [CLOSED_IN_TOPSPACE, OPEN_IN_DIFF, CLOSED_IN_DIFF,
762 OPEN_IN_TOPSPACE] THEN
763 REPEAT (POP_ASSUM MP_TAC) THEN SET_TAC[]
764QED
765
766Theorem OPEN_IN_SUBTOPOLOGY_EMPTY[simp]:
767 !top s. open_in (subtopology top {}) s <=> (s = {})
768Proof
769 REWRITE_TAC[OPEN_IN_SUBTOPOLOGY, INTER_EMPTY] THEN
770 MESON_TAC[OPEN_IN_EMPTY]
771QED
772
773Theorem CLOSED_IN_SUBTOPOLOGY_EMPTY[simp]:
774 !top s. closed_in (subtopology top {}) s <=> (s = {})
775Proof
776 REWRITE_TAC[CLOSED_IN_SUBTOPOLOGY, INTER_EMPTY] THEN
777 MESON_TAC[CLOSED_IN_EMPTY]
778QED
779
780Theorem OPEN_IN_SUBTOPOLOGY_REFL[simp]:
781 !top u:'a->bool. open_in (subtopology top u) u <=> u SUBSET topspace top
782Proof
783 REPEAT GEN_TAC THEN REWRITE_TAC[OPEN_IN_SUBTOPOLOGY] THEN EQ_TAC THENL
784 [REPEAT STRIP_TAC THEN ONCE_ASM_REWRITE_TAC[] THEN
785 MATCH_MP_TAC(SET_RULE ``s SUBSET u ==> s INTER t SUBSET u``) THEN
786 ASM_SIMP_TAC std_ss [OPEN_IN_SUBSET],
787 DISCH_TAC THEN EXISTS_TAC ``topspace top:'a->bool`` THEN
788 REWRITE_TAC[OPEN_IN_TOPSPACE] THEN REPEAT (POP_ASSUM MP_TAC) THEN SET_TAC[]]
789QED
790
791Theorem CLOSED_IN_SUBTOPOLOGY_REFL[simp]:
792 !top u:'a->bool. closed_in (subtopology top u) u <=> u SUBSET topspace top
793Proof
794 REPEAT GEN_TAC THEN REWRITE_TAC[CLOSED_IN_SUBTOPOLOGY] THEN EQ_TAC THENL
795 [REPEAT STRIP_TAC THEN ONCE_ASM_REWRITE_TAC[] THEN
796 MATCH_MP_TAC(SET_RULE ``s SUBSET u ==> s INTER t SUBSET u``) THEN
797 ASM_SIMP_TAC std_ss [CLOSED_IN_SUBSET],
798 DISCH_TAC THEN EXISTS_TAC ``topspace top:'a->bool`` THEN
799 REWRITE_TAC[CLOSED_IN_TOPSPACE] THEN REPEAT (POP_ASSUM MP_TAC) THEN
800 SET_TAC[]]
801QED
802
803Theorem SUBTOPOLOGY_SUPERSET :
804 !top s:'a->bool. topspace top SUBSET s ==> (subtopology top s = top)
805Proof
806 REPEAT GEN_TAC THEN SIMP_TAC std_ss [TOPOLOGY_EQ, OPEN_IN_SUBTOPOLOGY] THEN
807 DISCH_TAC THEN X_GEN_TAC ``u:'a->bool`` THEN EQ_TAC THENL
808 [DISCH_THEN(CHOOSE_THEN(CONJUNCTS_THEN2 MP_TAC SUBST1_TAC)) THEN
809 DISCH_THEN(fn th => MP_TAC th THEN
810 ASSUME_TAC(MATCH_MP OPEN_IN_SUBSET th)) THEN
811 MATCH_MP_TAC EQ_IMPLIES THEN AP_TERM_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN
812 SET_TAC[],
813 DISCH_TAC THEN EXISTS_TAC ``u:'a->bool`` THEN
814 FIRST_ASSUM(MP_TAC o MATCH_MP OPEN_IN_SUBSET) THEN
815 REPEAT (POP_ASSUM MP_TAC) THEN SET_TAC[]]
816QED
817
818Theorem SUBTOPOLOGY_TOPSPACE[simp]:
819 !top. subtopology top (topspace top) = top
820Proof
821 SIMP_TAC std_ss [SUBTOPOLOGY_SUPERSET, SUBSET_REFL]
822QED
823
824Theorem SUBTOPOLOGY_UNIV[simp]:
825 !top. subtopology top UNIV = top
826Proof
827 SIMP_TAC std_ss [SUBTOPOLOGY_SUPERSET, SUBSET_UNIV]
828QED
829
830Theorem OPEN_IN_IMP_SUBSET :
831 !top s t. open_in (subtopology top s) t ==> t SUBSET s
832Proof
833 REWRITE_TAC[OPEN_IN_SUBTOPOLOGY] THEN SET_TAC[]
834QED
835
836Theorem CLOSED_IN_IMP_SUBSET :
837 !top s t. closed_in (subtopology top s) t ==> t SUBSET s
838Proof
839 REWRITE_TAC[closed_in, TOPSPACE_SUBTOPOLOGY] THEN SET_TAC[]
840QED
841
842Theorem OPEN_IN_SUBTOPOLOGY_UNION :
843 !top s t u:'a->bool.
844 open_in (subtopology top t) s /\ open_in (subtopology top u) s
845 ==> open_in (subtopology top (t UNION u)) s
846Proof
847 REPEAT GEN_TAC THEN REWRITE_TAC[OPEN_IN_SUBTOPOLOGY] THEN
848 DISCH_THEN(CONJUNCTS_THEN2
849 (X_CHOOSE_THEN ``s':'a->bool`` STRIP_ASSUME_TAC)
850 (X_CHOOSE_THEN ``t':'a->bool`` STRIP_ASSUME_TAC)) THEN
851 EXISTS_TAC ``s' INTER t':'a->bool`` >> ASM_SIMP_TAC std_ss [OPEN_IN_INTER] >>
852 REPEAT (POP_ASSUM MP_TAC) THEN SET_TAC[]
853QED
854
855Theorem CLOSED_IN_SUBTOPOLOGY_UNION :
856 !top s t u:'a->bool.
857 closed_in (subtopology top t) s /\ closed_in (subtopology top u) s
858 ==> closed_in (subtopology top (t UNION u)) s
859Proof
860 REPEAT GEN_TAC THEN REWRITE_TAC[CLOSED_IN_SUBTOPOLOGY] THEN
861 DISCH_THEN(CONJUNCTS_THEN2
862 (X_CHOOSE_THEN ``s':'a->bool`` STRIP_ASSUME_TAC)
863 (X_CHOOSE_THEN ``t':'a->bool`` STRIP_ASSUME_TAC)) THEN
864 EXISTS_TAC ``s' INTER t':'a->bool`` >> ASM_SIMP_TAC std_ss [CLOSED_IN_INTER]>>
865 REPEAT (POP_ASSUM MP_TAC) THEN SET_TAC[]
866QED
867
868Theorem SUBTOPOLOGY_SUBTOPOLOGY[simp] :
869 !top s t:'a->bool.
870 subtopology (subtopology top s) t = subtopology top (s INTER t)
871Proof
872 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[subtopology] THEN
873 REWRITE_TAC[OPEN_IN_SUBTOPOLOGY] THEN
874 SIMP_TAC std_ss [SET_RULE ``{f x | ?y. P y /\ x = g y} = {f(g y) | P y}``] THEN
875 REWRITE_TAC[INTER_ASSOC]
876QED
877
878(* ------------------------------------------------------------------------- *)
879(* HOL Light compatibility layer (sets.ml) *)
880(* ------------------------------------------------------------------------- *)
881
882(* moved here from util_probTheory *)
883Theorem EXT_SKOLEM_THM :
884 !P Q. (!x. x IN P ==> ?y. Q x y) <=> ?f. !x. x IN P ==> Q x (f x)
885Proof
886 rpt STRIP_TAC
887 >> reverse EQ_TAC >> rpt STRIP_TAC
888 >- (Q.EXISTS_TAC `f x` \\
889 FIRST_X_ASSUM MATCH_MP_TAC >> rw [])
890 >> fs [GSYM RIGHT_EXISTS_IMP_THM, SKOLEM_THM]
891 >> Q.EXISTS_TAC `f` >> rw []
892QED
893
894(* applied version, used in ‘example/probability’ *)
895Theorem EXT_SKOLEM_THM' = REWRITE_RULE [IN_APP] EXT_SKOLEM_THM
896
897(* HOL Light compatibility layer (sets.ml) *)
898Overload UNIONS[inferior] = “BIGUNION”
899Overload INTERS[inferior] = “BIGINTER”
900
901Theorem COUNTABLE_SUBSET_NUM = COUNTABLE_NUM
902Theorem FINITE_IMAGE = IMAGE_FINITE
903Theorem IN_INTERS = IN_BIGINTER
904Theorem IN_UNIONS = IN_BIGUNION
905Theorem INTER_UNIONS = INTER_BIGUNION
906Theorem INTERS_0 = BIGINTER_EMPTY
907Theorem INTERS_1 = BIGINTER_SING
908Theorem INTERS_2 = BIGINTER_2
909Theorem INTERS_INSERT = BIGINTER_INSERT
910Theorem UNIONS_0 = BIGUNION_EMPTY
911Theorem UNIONS_1 = BIGUNION_SING
912Theorem UNIONS_2 = BIGUNION_2
913Theorem UNIONS_UNION = BIGUNION_UNION
914Theorem UNIONS_INSERT = BIGUNION_INSERT
915Theorem UNIONS_SUBSET = BIGUNION_SUBSET
916
917Theorem EMPTY_GSPEC :
918 {x | F} = {}
919Proof SET_TAC[]
920QED
921
922Theorem UNIV_GSPEC :
923 {x | T} = UNIV
924Proof SET_TAC[]
925QED
926
927Theorem SING_GSPEC :
928 (!a. {x | x = a} = {a}) /\ (!a. {x | a = x} = {a})
929Proof SET_TAC[]
930QED
931
932Theorem IN_GSPEC :
933 !s. {x | x IN s} = s
934Proof SET_TAC[]
935QED
936
937Theorem SUBSET_RESTRICT :
938 !s P. {x | x IN s /\ P x} SUBSET s
939Proof SET_TAC []
940QED
941
942(* This version is considered as "applied" as ‘COMPL’ itself doesn't appear:
943
944 |- !s. univ(:'a) DIFF (univ(:'a) DIFF s) = s
945 *)
946Theorem COMPL_COMPL_applied = REWRITE_RULE [COMPL_DEF] COMPL_COMPL
947
948(* |- !f s. {f x | x IN s} = IMAGE f s *)
949Theorem SIMPLE_IMAGE = GSYM IMAGE_DEF
950
951Theorem UNIONS_IMAGE :
952 !f s. UNIONS (IMAGE f s) = {y | ?x. x IN s /\ y IN f x}
953Proof
954 rpt GEN_TAC
955 >> rw [Once EXTENSION]
956 >> EQ_TAC >> rw [] >> rename1 ‘x IN f t’
957 >- (Q.EXISTS_TAC ‘t’ >> rw [])
958 >> Q.EXISTS_TAC ‘f t’ >> rw []
959 >> Q.EXISTS_TAC ‘t’ >> rw []
960QED
961
962Theorem INTERS_IMAGE :
963 !f s. INTERS (IMAGE f s) = {y | !x. x IN s ==> y IN f x}
964Proof
965 rpt GEN_TAC
966 >> rw [Once EXTENSION]
967 >> EQ_TAC >> rw [] >> rename1 ‘x IN f t’
968 >- (FIRST_X_ASSUM MATCH_MP_TAC \\
969 Q.EXISTS_TAC ‘t’ >> rw [])
970 >> FIRST_X_ASSUM MATCH_MP_TAC >> rw []
971QED
972
973Theorem DIFF_INTERS :
974 !u s. u DIFF INTERS s = UNIONS {u DIFF t | t IN s}
975Proof
976 rpt GEN_TAC
977 >> rw [Once EXTENSION]
978 >> EQ_TAC >> rw []
979 >- (Q.EXISTS_TAC ‘u DIFF P’ >> rw [] \\
980 Q.EXISTS_TAC ‘P’ >> rw [])
981 >- fs []
982 >> Q.EXISTS_TAC ‘t’ >> fs []
983QED
984
985Theorem INTERS_GSPEC :
986 (!P f. INTERS {f x | P x} = {a | !x. P x ==> a IN (f x)}) /\
987 (!P f. INTERS {f x y | P x y} = {a | !x y. P x y ==> a IN (f x y)}) /\
988 (!P f. INTERS {f x y z | P x y z} =
989 {a | !x y z. P x y z ==> a IN (f x y z)})
990Proof
991 rpt STRIP_TAC >> GEN_REWRITE_TAC I empty_rewrites [EXTENSION] \\
992 rw [IN_INTERS] >> MESON_TAC []
993QED
994
995Theorem UNIONS_GSPEC :
996 (!P f. UNIONS {f x | P x} = {a | ?x. P x /\ a IN (f x)}) /\
997 (!P f. UNIONS {f x y | P x y} = {a | ?x y. P x y /\ a IN (f x y)}) /\
998 (!P f. UNIONS {f x y z | P x y z} =
999 {a | ?x y z. P x y z /\ a IN (f x y z)})
1000Proof
1001 rpt STRIP_TAC >> GEN_REWRITE_TAC I empty_rewrites [EXTENSION] \\
1002 rw [IN_UNIONS] >> MESON_TAC []
1003QED
1004
1005Theorem INTER_INTERS :
1006 (!f s:'a->bool. s INTER INTERS f =
1007 if f = {} then s else INTERS {s INTER t | t IN f}) /\
1008 (!f s:'a->bool. INTERS f INTER s =
1009 if f = {} then s else INTERS {t INTER s | t IN f})
1010Proof
1011 CONJ_ASM1_TAC
1012 >- (rpt STRIP_TAC THEN COND_CASES_TAC THEN
1013 ASM_SIMP_TAC std_ss [INTERS_0, INTER_UNIV, INTERS_GSPEC] THEN
1014 rw [Once EXTENSION, IN_INTERS] \\
1015 EQ_TAC >> rw [] \\
1016 fs [GSYM MEMBER_NOT_EMPTY] >> PROVE_TAC [])
1017 >> POP_ASSUM (ACCEPT_TAC o (ONCE_REWRITE_RULE [INTER_COMM]))
1018QED
1019
1020Theorem INTERS_UNIONS :
1021 !s. INTERS s = UNIV DIFF (UNIONS {UNIV DIFF t | t IN s})
1022Proof
1023 REWRITE_TAC[GSYM DIFF_INTERS] THEN SET_TAC[]
1024QED
1025
1026Theorem UNIONS_INTERS :
1027 !s. UNIONS s = UNIV DIFF (INTERS {UNIV DIFF t | t IN s})
1028Proof
1029 GEN_TAC
1030 >> rw [Once EXTENSION]
1031 >> EQ_TAC >> rw []
1032 >- (rename1 ‘x IN t’ \\
1033 Q.EXISTS_TAC ‘univ(:'a) DIFF t’ \\
1034 rw [] >> Q.EXISTS_TAC ‘t’ >> rw [])
1035 >> fs []
1036 >> Q.EXISTS_TAC ‘t’ >> rw []
1037QED
1038
1039(* NOTE: HOL4's BIGINTER_SUBSET doesn't have ‘u <> {}’ *)
1040Theorem INTERS_SUBSET :
1041 !u s:'a->bool.
1042 ~(u = {}) /\ (!t. t IN u ==> t SUBSET s) ==> INTERS u SUBSET s
1043Proof
1044 SET_TAC[]
1045QED
1046
1047(* essentially same as HOL4's BIGINTER_SUBSET but looks more reasonable *)
1048Theorem INTERS_SUBSET_STRONG :
1049 !u s:'a->bool. (?t. t IN u /\ t SUBSET s) ==> INTERS u SUBSET s
1050Proof
1051 SET_TAC[]
1052QED
1053
1054Theorem DIFF_UNIONS :
1055 !u s. u DIFF UNIONS s = u INTER INTERS {u DIFF t | t IN s}
1056Proof
1057 SIMP_TAC std_ss [INTERS_GSPEC] THEN SET_TAC[]
1058QED
1059
1060Theorem DIFF_UNIONS_NONEMPTY :
1061 !u s. ~(s = {}) ==> u DIFF UNIONS s = INTERS {u DIFF t | t IN s}
1062Proof
1063 SIMP_TAC std_ss [INTERS_GSPEC] THEN SET_TAC[]
1064QED
1065
1066Theorem EXISTS_SUBSET_IMAGE :
1067 !P (f :'a->'b) s.
1068 (?t. t SUBSET IMAGE f s /\ P t) <=> (?t. t SUBSET s /\ P (IMAGE f t))
1069Proof
1070 REWRITE_TAC[SUBSET_IMAGE] THEN MESON_TAC[]
1071QED
1072
1073Theorem FORALL_SUBSET_IMAGE :
1074 !P (f :'a->'b) s.
1075 (!t. t SUBSET IMAGE f s ==> P t) <=>
1076 (!t. t SUBSET s ==> P(IMAGE f t))
1077Proof
1078 REWRITE_TAC[SUBSET_IMAGE] THEN MESON_TAC[]
1079QED
1080
1081Theorem SUBSET_IMAGE_INJ :
1082 !(f :'a->'b) s t.
1083 s SUBSET (IMAGE f t) <=>
1084 ?u. u SUBSET t /\
1085 (!x y. x IN u /\ y IN u ==> (f x = f y <=> x = y)) /\
1086 s = IMAGE f u
1087Proof
1088 REPEAT GEN_TAC THEN EQ_TAC THENL [ALL_TAC, MESON_TAC[IMAGE_SUBSET]] THEN
1089 DISCH_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP (SET_RULE
1090 “s SUBSET IMAGE f t ==> !x. x IN s ==> ?y. y IN t /\ f y = x”)) THEN
1091 REWRITE_TAC[SURJECTIVE_ON_RIGHT_INVERSE] THEN
1092 DISCH_THEN(X_CHOOSE_TAC “g:'b->'a”) THEN
1093 EXISTS_TAC “IMAGE (g :'b->'a) s” THEN ASM_SET_TAC[]
1094QED
1095
1096Theorem EXISTS_SUBSET_IMAGE_INJ :
1097 !P (f :'a->'b) s.
1098 (?t. t SUBSET IMAGE f s /\ P t) <=>
1099 (?t. t SUBSET s /\
1100 (!x y. x IN t /\ y IN t ==> (f x = f y <=> x = y)) /\
1101 P (IMAGE f t))
1102Proof
1103 REWRITE_TAC[SUBSET_IMAGE_INJ] THEN METIS_TAC []
1104QED
1105
1106Theorem FORALL_SUBSET_IMAGE_INJ :
1107 !P (f :'a->'b) s.
1108 (!t. t SUBSET IMAGE f s ==> P t) <=>
1109 (!t. t SUBSET s /\
1110 (!x y. x IN t /\ y IN t ==> (f x = f y <=> x = y))
1111 ==> P(IMAGE f t))
1112Proof
1113 REPEAT GEN_TAC THEN
1114 qabbrev_tac ‘Q = \t. t SUBSET IMAGE f s ==> P t’ \\
1115 qabbrev_tac ‘R = \t. t SUBSET s /\
1116 (!x y. x IN t /\ y IN t ==> (f x = f y <=> x = y)) ==>
1117 P (IMAGE f t)’ \\
1118 ‘$! Q <=> ~(?t. ~Q t)’ by rw [Abbr ‘Q’] >> POP_ORW \\
1119 ‘$! R <=> ~(?t. ~R t)’ by rw [Abbr ‘R’] >> POP_ORW \\
1120 simp[Abbr ‘Q’, Abbr ‘R’, NOT_IMP, EXISTS_SUBSET_IMAGE_INJ, GSYM CONJ_ASSOC]
1121QED
1122
1123Theorem EXISTS_FINITE_SUBSET_IMAGE_INJ :
1124 !P (f :'a->'b) s.
1125 (?t. FINITE t /\ t SUBSET IMAGE f s /\ P t) <=>
1126 (?t. FINITE t /\ t SUBSET s /\
1127 (!x y. x IN t /\ y IN t ==> (f x = f y <=> x = y)) /\
1128 P (IMAGE f t))
1129Proof
1130 ONCE_REWRITE_TAC[TAUT `p /\ q /\ r <=> q /\ p /\ r`] THEN
1131 REPEAT GEN_TAC THEN SIMP_TAC std_ss[EXISTS_SUBSET_IMAGE_INJ] THEN
1132 AP_TERM_TAC THEN ABS_TAC THEN MESON_TAC[FINITE_IMAGE_INJ_EQ]
1133QED
1134
1135Theorem FORALL_FINITE_SUBSET_IMAGE_INJ :
1136 !P (f :'a->'b) s.
1137 (!t. FINITE t /\ t SUBSET IMAGE f s ==> P t) <=>
1138 (!t. FINITE t /\ t SUBSET s /\
1139 (!x y. x IN t /\ y IN t ==> (f x = f y <=> x = y))
1140 ==> P(IMAGE f t))
1141Proof
1142 REPEAT GEN_TAC THEN
1143 qabbrev_tac ‘Q = \t. FINITE t /\ t SUBSET IMAGE f s ==> P t’ \\
1144 qabbrev_tac ‘R = \t. FINITE t /\ t SUBSET s /\
1145 (!x y. x IN t /\ y IN t ==> (f x = f y <=> x = y)) ==>
1146 P (IMAGE f t)’ \\
1147 ‘$! Q <=> ~(?t. ~Q t)’ by rw [Abbr ‘Q’] >> POP_ORW \\
1148 ‘$! R <=> ~(?t. ~R t)’ by rw [Abbr ‘R’] >> POP_ORW \\
1149 simp[Abbr ‘Q’, Abbr ‘R’, NOT_IMP, EXISTS_FINITE_SUBSET_IMAGE_INJ, GSYM CONJ_ASSOC]
1150QED
1151
1152Theorem EXISTS_FINITE_SUBSET_IMAGE :
1153 !P (f :'a->'b) s.
1154 (?t. FINITE t /\ t SUBSET IMAGE f s /\ P t) <=>
1155 (?t. FINITE t /\ t SUBSET s /\ P (IMAGE f t))
1156Proof
1157 REPEAT GEN_TAC THEN EQ_TAC THENL
1158 [REWRITE_TAC[EXISTS_FINITE_SUBSET_IMAGE_INJ] THEN MESON_TAC[],
1159 MESON_TAC[FINITE_IMAGE, IMAGE_SUBSET]]
1160QED
1161
1162Theorem FORALL_FINITE_SUBSET_IMAGE :
1163 !P (f :'a->'b) s.
1164 (!t. FINITE t /\ t SUBSET IMAGE f s ==> P t) <=>
1165 (!t. FINITE t /\ t SUBSET s ==> P(IMAGE f t))
1166Proof
1167 REPEAT GEN_TAC THEN
1168 qabbrev_tac ‘Q = \t. FINITE t /\ t SUBSET IMAGE f s ==> P t’ \\
1169 qabbrev_tac ‘R = \t. FINITE t /\ t SUBSET s ==> P (IMAGE f t)’ \\
1170 ‘$! Q <=> ~(?t. ~Q t)’ by rw [Abbr ‘Q’] >> POP_ORW \\
1171 ‘$! R <=> ~(?t. ~R t)’ by rw [Abbr ‘R’] >> POP_ORW \\
1172 simp[Abbr ‘Q’, Abbr ‘R’, NOT_IMP, GSYM CONJ_ASSOC, EXISTS_FINITE_SUBSET_IMAGE]
1173QED
1174
1175(* ------------------------------------------------------------------------- *)
1176(* Pairwise property over sets and lists (from real_topologyTheory) *)
1177(* ------------------------------------------------------------------------- *)
1178
1179val _ = hide "pairwise"; (* pred_setTheory *)
1180
1181(* NOTE: this definition is HOL-Light compatible, originally from "sets.ml". *)
1182Definition pairwise[nocompute]:
1183 pairwise r s <=> !x y. x IN s /\ y IN s /\ ~(x = y) ==> r x y
1184End
1185
1186Overload pairwiseD = “topology$pairwise”
1187Overload pairwiseN[local] = “pred_set$pairwise”
1188
1189(* connection between pairwiseD and pairwiseN, originally by Michael Norrish *)
1190Theorem pairwiseD_alt_pairwiseN :
1191 !R. pairwiseD R = pairwiseN (RC R)
1192Proof
1193 RW_TAC std_ss [FUN_EQ_THM, pairwise, pairwise_def, RC_DEF]
1194 >> METIS_TAC []
1195QED
1196
1197Theorem PAIRWISE_EMPTY :
1198 !r. pairwise r {} <=> T
1199Proof
1200 rw [pairwiseD_alt_pairwiseN, pairwise_EMPTY]
1201QED
1202
1203Theorem PAIRWISE_SING :
1204 !r x. pairwise r {x} <=> T
1205Proof
1206 REWRITE_TAC[pairwise, IN_SING] THEN MESON_TAC[]
1207QED
1208
1209Theorem PAIRWISE_IMP :
1210 !P Q s.
1211 pairwise P s /\
1212 (!x y. x IN s /\ y IN s /\ P x y /\ ~(x = y) ==> Q x y)
1213 ==> pairwise Q s
1214Proof
1215 REWRITE_TAC[pairwise] THEN SET_TAC[]
1216QED
1217
1218Theorem PAIRWISE_MONO :
1219 !r s t. pairwise r s /\ t SUBSET s ==> pairwise r t
1220Proof
1221 REWRITE_TAC[pairwise] THEN SET_TAC[]
1222QED
1223
1224Theorem PAIRWISE_AND :
1225 !R R' s. pairwise R s /\ pairwise R' s <=>
1226 pairwise (\x y. R x y /\ R' x y) s
1227Proof
1228 REWRITE_TAC[pairwise] THEN SET_TAC[]
1229QED
1230
1231Theorem PAIRWISE_INSERT :
1232 !r x s.
1233 pairwise r (x INSERT s) <=>
1234 (!y. y IN s /\ ~(y = x) ==> r x y /\ r y x) /\
1235 pairwise r s
1236Proof
1237 REWRITE_TAC[pairwise, IN_INSERT] THEN MESON_TAC[]
1238QED
1239
1240Theorem PAIRWISE_IMAGE :
1241 !r f. pairwise r (IMAGE f s) <=>
1242 pairwise (\x y. ~(f x = f y) ==> r (f x) (f y)) s
1243Proof
1244 REWRITE_TAC[pairwise, IN_IMAGE] THEN MESON_TAC[]
1245QED
1246
1247Theorem PAIRWISE_UNION :
1248 !R s t. pairwise R (s UNION t) <=>
1249 pairwise R s /\ pairwise R t /\
1250 (!x y. x IN s DIFF t /\ y IN t DIFF s ==> R x y /\ R y x)
1251Proof
1252 REWRITE_TAC[pairwise] THEN SET_TAC[]
1253QED
1254
1255(* ------------------------------------------------------------------------- *)
1256(* Useful idioms for being a suitable union/intersection of somethings. *)
1257(* (ported from HOL Light's sets.ml) *)
1258(* ------------------------------------------------------------------------- *)
1259
1260(* original priority in HOL-Light:
1261 parse_as_infix("UNION_OF",(20,"right"));;
1262 parse_as_infix("INTERSECTION_OF",(20,"right"));;
1263 *)
1264val _ = set_fixity "UNION_OF" (Infixr 601);
1265val _ = set_fixity "INTERSECTION_OF" (Infixr 601);
1266
1267Definition UNION_OF :
1268 P UNION_OF Q = \s. ?u. P u /\ (!c. c IN u ==> Q c) /\ UNIONS u = s
1269End
1270
1271Definition INTERSECTION_OF :
1272 P INTERSECTION_OF Q = \s. ?u. P u /\ (!c. c IN u ==> Q c) /\ INTERS u = s
1273End
1274
1275Theorem UNION_OF_INC :
1276 !P Q s:'a->bool. P {s} /\ Q s ==> (P UNION_OF Q) s
1277Proof
1278 REPEAT STRIP_TAC THEN SIMP_TAC std_ss [UNION_OF] THEN
1279 Q.EXISTS_TAC `{s:'a->bool}` THEN ASM_SIMP_TAC std_ss [UNIONS_1, IN_SING]
1280QED
1281
1282Theorem INTERSECTION_OF_INC :
1283 !P Q s:'a->bool. P {s} /\ Q s ==> (P INTERSECTION_OF Q) s
1284Proof
1285 REPEAT STRIP_TAC THEN SIMP_TAC std_ss [INTERSECTION_OF] THEN
1286 Q.EXISTS_TAC `{s:'a->bool}` THEN ASM_SIMP_TAC std_ss [INTERS_1, IN_SING]
1287QED
1288
1289Theorem UNION_OF_MONO :
1290 !P Q Q' s:'a->bool.
1291 (P UNION_OF Q) s /\ (!x. Q x ==> Q' x) ==> (P UNION_OF Q') s
1292Proof
1293 SIMP_TAC std_ss [UNION_OF] THEN MESON_TAC[]
1294QED
1295
1296Theorem INTERSECTION_OF_MONO :
1297 !P Q Q' s:'a->bool.
1298 (P INTERSECTION_OF Q) s /\ (!x. Q x ==> Q' x)
1299 ==> (P INTERSECTION_OF Q') s
1300Proof
1301 SIMP_TAC std_ss [INTERSECTION_OF] THEN MESON_TAC[]
1302QED
1303
1304Theorem FORALL_UNION_OF :
1305 (!s. (P UNION_OF Q) s ==> R s) <=>
1306 (!t. P t /\ (!c. c IN t ==> Q c) ==> R(UNIONS t))
1307Proof
1308 SIMP_TAC std_ss [UNION_OF] THEN MESON_TAC[]
1309QED
1310
1311Theorem FORALL_INTERSECTION_OF :
1312 (!s. (P INTERSECTION_OF Q) s ==> R s) <=>
1313 (!t. P t /\ (!c. c IN t ==> Q c) ==> R(INTERS t))
1314Proof
1315 SIMP_TAC std_ss [INTERSECTION_OF] THEN MESON_TAC[]
1316QED
1317
1318Theorem UNION_OF_EMPTY :
1319 !P Q:('a->bool)->bool. P {} ==> (P UNION_OF Q) {}
1320Proof
1321 REPEAT STRIP_TAC THEN SIMP_TAC std_ss [UNION_OF] THEN
1322 Q.EXISTS_TAC `{}:('a->bool)->bool` THEN
1323 ASM_SIMP_TAC std_ss [UNIONS_0, NOT_IN_EMPTY]
1324QED
1325
1326Theorem INTERSECTION_OF_EMPTY :
1327 !P Q:('a->bool)->bool. P {} ==> (P INTERSECTION_OF Q) UNIV
1328Proof
1329 REPEAT STRIP_TAC THEN SIMP_TAC std_ss [INTERSECTION_OF] THEN
1330 Q.EXISTS_TAC `{}:('a->bool)->bool` THEN
1331 ASM_SIMP_TAC std_ss [INTERS_0, NOT_IN_EMPTY]
1332QED
1333
1334(* ------------------------------------------------------------------------- *)
1335(* The ARBITRARY and FINITE cases of UNION_OF / INTERSECTION_OF *)
1336(* ------------------------------------------------------------------------- *)
1337
1338Definition ARBITRARY[simp] :
1339 ARBITRARY (s:('a->bool)->bool) <=> T
1340End
1341
1342Theorem ARBITRARY_UNION_OF_ALT :
1343 !B s:'a->bool.
1344 (ARBITRARY UNION_OF B) s <=>
1345 !x. x IN s ==> ?u. u IN B /\ x IN u /\ u SUBSET s
1346Proof
1347 GEN_TAC THEN SIMP_TAC std_ss [FORALL_AND_THM, TAUT
1348 `(p <=> q) <=> (p ==> q) /\ (q ==> p)`] THEN
1349 SIMP_TAC std_ss [FORALL_UNION_OF, ARBITRARY] THEN
1350 CONJ_TAC THENL [SET_TAC[], ALL_TAC] THEN
1351 Q.X_GEN_TAC `s:'a->bool` THEN DISCH_TAC THEN
1352 SIMP_TAC std_ss [ARBITRARY, UNION_OF] THEN
1353 Q.EXISTS_TAC `{u:'a->bool | u IN B /\ u SUBSET s}` THEN ASM_SET_TAC[]
1354QED
1355
1356Theorem ARBITRARY_UNION_OF_EMPTY :
1357 !P:('a->bool)->bool. (ARBITRARY UNION_OF P) {}
1358Proof
1359 SIMP_TAC std_ss [UNION_OF_EMPTY, ARBITRARY]
1360QED
1361
1362Theorem ARBITRARY_INTERSECTION_OF_EMPTY :
1363 !P:('a->bool)->bool. (ARBITRARY INTERSECTION_OF P) UNIV
1364Proof
1365 SIMP_TAC std_ss [INTERSECTION_OF_EMPTY, ARBITRARY]
1366QED
1367
1368Theorem ARBITRARY_UNION_OF_INC :
1369 !P s:'a->bool. P s ==> (ARBITRARY UNION_OF P) s
1370Proof
1371 SIMP_TAC std_ss [UNION_OF_INC, ARBITRARY]
1372QED
1373
1374Theorem ARBITRARY_INTERSECTION_OF_INC :
1375 !P s:'a->bool. P s ==> (ARBITRARY INTERSECTION_OF P) s
1376Proof
1377 SIMP_TAC std_ss [INTERSECTION_OF_INC, ARBITRARY]
1378QED
1379
1380Theorem ARBITRARY_UNION_OF_COMPLEMENT :
1381 !P s. (ARBITRARY UNION_OF P) s <=>
1382 (ARBITRARY INTERSECTION_OF (\s. P(univ(:'a) DIFF s))) (univ(:'a) DIFF s)
1383Proof
1384 REPEAT GEN_TAC THEN SIMP_TAC std_ss [UNION_OF, INTERSECTION_OF] THEN
1385 EQ_TAC THEN
1386 DISCH_THEN(Q.X_CHOOSE_THEN `u:('a->bool)->bool` STRIP_ASSUME_TAC) THEN
1387 Q.EXISTS_TAC `IMAGE (\c. univ(:'a) DIFF c) u` THEN
1388 ASM_SIMP_TAC std_ss [ARBITRARY, FORALL_IN_IMAGE, COMPL_COMPL_applied] THEN
1389 ONCE_REWRITE_TAC [UNIONS_INTERS, INTERS_UNIONS] THEN
1390 SIMP_TAC std_ss [SET_RULE ``{f y | y IN IMAGE g s} = IMAGE (\x. f(g x)) s``] THEN
1391 ASM_SIMP_TAC std_ss [IMAGE_ID, COMPL_COMPL_applied]
1392QED
1393
1394Theorem ARBITRARY_INTERSECTION_OF_COMPLEMENT :
1395 !P s. (ARBITRARY INTERSECTION_OF P) s <=>
1396 (ARBITRARY UNION_OF (\s. P(univ(:'a) DIFF s))) (univ(:'a) DIFF s)
1397Proof
1398 SIMP_TAC std_ss [ARBITRARY_UNION_OF_COMPLEMENT] THEN
1399 SIMP_TAC std_ss [ETA_AX, COMPL_COMPL_applied]
1400QED
1401
1402Theorem ARBITRARY_UNION_OF_IDEMPOT :
1403 !P:('a->bool)->bool.
1404 ARBITRARY UNION_OF ARBITRARY UNION_OF P = ARBITRARY UNION_OF P
1405Proof
1406 GEN_TAC THEN SIMP_TAC std_ss [FUN_EQ_THM] THEN Q.X_GEN_TAC `s:'a->bool` THEN
1407 EQ_TAC THEN SIMP_TAC std_ss [ARBITRARY_UNION_OF_INC] THEN
1408 SIMP_TAC std_ss [UNION_OF, LEFT_IMP_EXISTS_THM] THEN
1409 Q.X_GEN_TAC `u:('a->bool)->bool` THEN
1410 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1411 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC (SUBST1_TAC o SYM)) THEN
1412 rw [EXT_SKOLEM_THM] \\
1413 Q.EXISTS_TAC
1414 `IMAGE SND {(s,t) | s IN u /\ t IN (f:('a->bool)->('a->bool)->bool) s}` THEN
1415 ASM_SIMP_TAC std_ss [ARBITRARY] THEN
1416 SIMP_TAC std_ss [FORALL_IN_IMAGE, FORALL_IN_GSPEC] THEN
1417 CONJ_TAC THENL [ASM_SET_TAC[], SIMP_TAC std_ss [UNIONS_IMAGE]] THEN
1418 SIMP_TAC std_ss [EXISTS_IN_GSPEC] THEN ASM_SET_TAC[]
1419QED
1420
1421Theorem ARBITRARY_INTERSECTION_OF_IDEMPOT :
1422 !P:('a->bool)->bool.
1423 ARBITRARY INTERSECTION_OF ARBITRARY INTERSECTION_OF P =
1424 ARBITRARY INTERSECTION_OF P
1425Proof
1426 RW_TAC (std_ss ++ ETA_ss) [FUN_EQ_THM, COMPL_COMPL_applied,
1427 ARBITRARY_INTERSECTION_OF_COMPLEMENT]
1428 >> SIMP_TAC std_ss [ARBITRARY_UNION_OF_IDEMPOT]
1429QED
1430
1431Theorem ARBITRARY_UNION_OF_UNIONS :
1432 !P u:('a->bool)->bool.
1433 (!s. s IN u ==> (ARBITRARY UNION_OF P) s)
1434 ==> (ARBITRARY UNION_OF P) (UNIONS u)
1435Proof
1436 REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC [GSYM ARBITRARY_UNION_OF_IDEMPOT] THEN
1437 ONCE_REWRITE_TAC [UNION_OF] THEN SIMP_TAC std_ss [] THEN
1438 Q.EXISTS_TAC `u:('a->bool)->bool` THEN ASM_SIMP_TAC std_ss [ARBITRARY]
1439QED
1440
1441Theorem ARBITRARY_UNION_OF_UNION :
1442 !P s t. (ARBITRARY UNION_OF P) s /\ (ARBITRARY UNION_OF P) t
1443 ==> (ARBITRARY UNION_OF P) (s UNION t)
1444Proof
1445 REPEAT STRIP_TAC THEN SIMP_TAC std_ss [GSYM UNIONS_2] THEN
1446 MATCH_MP_TAC ARBITRARY_UNION_OF_UNIONS THEN
1447 ASM_SIMP_TAC std_ss [ARBITRARY, FORALL_IN_INSERT] THEN
1448 SIMP_TAC std_ss [ARBITRARY, NOT_IN_EMPTY]
1449QED
1450
1451Theorem ARBITRARY_INTERSECTION_OF_INTERS :
1452 !P u:('a->bool)->bool.
1453 (!s. s IN u ==> (ARBITRARY INTERSECTION_OF P) s)
1454 ==> (ARBITRARY INTERSECTION_OF P) (INTERS u)
1455Proof
1456 REPEAT STRIP_TAC THEN
1457 ONCE_REWRITE_TAC [GSYM ARBITRARY_INTERSECTION_OF_IDEMPOT] THEN
1458 ONCE_REWRITE_TAC [INTERSECTION_OF] THEN SIMP_TAC std_ss [] THEN
1459 Q.EXISTS_TAC `u:('a->bool)->bool` THEN ASM_SIMP_TAC std_ss [ARBITRARY]
1460QED
1461
1462Theorem ARBITRARY_INTERSECTION_OF_INTER :
1463 !P s t. (ARBITRARY INTERSECTION_OF P) s /\ (ARBITRARY INTERSECTION_OF P) t
1464 ==> (ARBITRARY INTERSECTION_OF P) (s INTER t)
1465Proof
1466 REPEAT STRIP_TAC THEN SIMP_TAC std_ss [GSYM INTERS_2] THEN
1467 MATCH_MP_TAC ARBITRARY_INTERSECTION_OF_INTERS THEN
1468 ASM_SIMP_TAC std_ss [ARBITRARY, FORALL_IN_INSERT] THEN
1469 SIMP_TAC std_ss [ARBITRARY, NOT_IN_EMPTY]
1470QED
1471
1472Theorem ARBITRARY_UNION_OF_INTER_EQ :
1473 !P:('a->bool)->bool.
1474 (!s t. (ARBITRARY UNION_OF P) s /\ (ARBITRARY UNION_OF P) t
1475 ==> (ARBITRARY UNION_OF P) (s INTER t)) <=>
1476 (!s t. P s /\ P t ==> (ARBITRARY UNION_OF P) (s INTER t))
1477Proof
1478 GEN_TAC THEN
1479 EQ_TAC THENL [MESON_TAC[ARBITRARY_UNION_OF_INC], DISCH_TAC] THEN
1480 REPEAT GEN_TAC THEN
1481 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) empty_rewrites [UNION_OF] THEN
1482 SIMP_TAC std_ss [] THEN DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
1483 ASM_SIMP_TAC std_ss [INTER_UNIONS] THEN
1484 REPLICATE_TAC 2
1485 (MATCH_MP_TAC ARBITRARY_UNION_OF_UNIONS THEN
1486 ASM_SIMP_TAC std_ss [SIMPLE_IMAGE, ARBITRARY, FORALL_IN_IMAGE] THEN
1487 REPEAT STRIP_TAC)
1488QED
1489
1490Theorem ARBITRARY_UNION_OF_INTER :
1491 !P:('a->bool)->bool.
1492 (!s t. P s /\ P t ==> P(s INTER t))
1493 ==> (!s t. (ARBITRARY UNION_OF P) s /\ (ARBITRARY UNION_OF P) t
1494 ==> (ARBITRARY UNION_OF P) (s INTER t))
1495Proof
1496 RW_TAC std_ss [ARBITRARY_UNION_OF_INTER_EQ,
1497 ARBITRARY_UNION_OF_INC]
1498QED
1499
1500Theorem ARBITRARY_INTERSECTION_OF_UNION_EQ :
1501 !P:('a->bool)->bool.
1502 (!s t. (ARBITRARY INTERSECTION_OF P) s /\
1503 (ARBITRARY INTERSECTION_OF P) t
1504 ==> (ARBITRARY INTERSECTION_OF P) (s UNION t)) <=>
1505 (!s t. P s /\ P t ==> (ARBITRARY INTERSECTION_OF P) (s UNION t))
1506Proof
1507 ONCE_REWRITE_TAC [ARBITRARY_INTERSECTION_OF_COMPLEMENT] THEN
1508 SIMP_TAC std_ss [SET_RULE
1509 ``UNIV DIFF (s UNION t) = (UNIV DIFF s) INTER (UNIV DIFF t)``] THEN
1510 SIMP_TAC std_ss [MESON[COMPL_COMPL_applied] ``(!s. P(UNIV DIFF s)) <=> (!s. P s)``] THEN
1511 SIMP_TAC std_ss [ARBITRARY_UNION_OF_INTER_EQ] THEN
1512 SIMP_TAC std_ss [SET_RULE
1513 ``s INTER t = UNIV DIFF ((UNIV DIFF s) UNION (UNIV DIFF t))``] THEN
1514 SIMP_TAC std_ss [MESON[COMPL_COMPL_applied] ``(!s. P(UNIV DIFF s)) <=> (!s. P s)``] THEN
1515 SIMP_TAC std_ss [COMPL_COMPL_applied]
1516QED
1517
1518Theorem ARBITRARY_INTERSECTION_OF_UNION :
1519 !P:('a->bool)->bool.
1520 (!s t. P s /\ P t ==> P(s UNION t))
1521 ==> (!s t. (ARBITRARY INTERSECTION_OF P) s /\
1522 (ARBITRARY INTERSECTION_OF P) t
1523 ==> (ARBITRARY INTERSECTION_OF P) (s UNION t))
1524Proof
1525 SIMP_TAC std_ss [ARBITRARY_INTERSECTION_OF_UNION_EQ] THEN
1526 MESON_TAC[ARBITRARY_INTERSECTION_OF_INC]
1527QED
1528
1529Theorem FINITE_UNION_OF_EMPTY :
1530 !P:('a->bool)->bool. (FINITE UNION_OF P) {}
1531Proof
1532 SIMP_TAC std_ss [UNION_OF_EMPTY, FINITE_EMPTY]
1533QED
1534
1535Theorem FINITE_INTERSECTION_OF_EMPTY :
1536 !P:('a->bool)->bool. (FINITE INTERSECTION_OF P) UNIV
1537Proof
1538 SIMP_TAC std_ss [INTERSECTION_OF_EMPTY, FINITE_EMPTY]
1539QED
1540
1541Theorem FINITE_UNION_OF_INC :
1542 !P s:'a->bool. P s ==> (FINITE UNION_OF P) s
1543Proof
1544 SIMP_TAC std_ss [UNION_OF_INC, FINITE_SING]
1545QED
1546
1547Theorem FINITE_INTERSECTION_OF_INC :
1548 !P s:'a->bool. P s ==> (FINITE INTERSECTION_OF P) s
1549Proof
1550 SIMP_TAC std_ss [INTERSECTION_OF_INC, FINITE_SING]
1551QED
1552
1553Theorem FINITE_UNION_OF_COMPLEMENT :
1554 !P s. (FINITE UNION_OF P) s <=>
1555 (FINITE INTERSECTION_OF (\s. P(univ(:'a) DIFF s))) (univ(:'a) DIFF s)
1556Proof
1557 REPEAT GEN_TAC THEN SIMP_TAC std_ss [UNION_OF, INTERSECTION_OF] THEN
1558 EQ_TAC THEN
1559 DISCH_THEN(Q.X_CHOOSE_THEN `u:('a->bool)->bool` STRIP_ASSUME_TAC) THEN
1560 Q.EXISTS_TAC `IMAGE (\c. univ(:'a) DIFF c) u` THEN
1561 ASM_SIMP_TAC std_ss [FINITE_IMAGE, FORALL_IN_IMAGE, COMPL_COMPL_applied] THEN
1562 ONCE_REWRITE_TAC [UNIONS_INTERS, INTERS_UNIONS] THEN
1563 SIMP_TAC std_ss [SET_RULE ``{f y | y IN IMAGE g s} = IMAGE (\x. f(g x)) s``] THEN
1564 ASM_SIMP_TAC std_ss [IMAGE_ID, COMPL_COMPL_applied]
1565QED
1566
1567Theorem FINITE_INTERSECTION_OF_COMPLEMENT :
1568 !P s. (FINITE INTERSECTION_OF P) s <=>
1569 (FINITE UNION_OF (\s. P(univ(:'a) DIFF s))) (univ(:'a) DIFF s)
1570Proof
1571 SIMP_TAC std_ss [FINITE_UNION_OF_COMPLEMENT] THEN
1572 SIMP_TAC (std_ss ++ ETA_ss) [COMPL_COMPL_applied]
1573QED
1574
1575Theorem FINITE_UNION_OF_IDEMPOT :
1576 !P:('a->bool)->bool.
1577 FINITE UNION_OF FINITE UNION_OF P = FINITE UNION_OF P
1578Proof
1579 GEN_TAC THEN SIMP_TAC std_ss [FUN_EQ_THM] THEN Q.X_GEN_TAC `s:'a->bool` THEN
1580 EQ_TAC THEN SIMP_TAC std_ss [FINITE_UNION_OF_INC] THEN
1581 SIMP_TAC std_ss [UNION_OF, LEFT_IMP_EXISTS_THM] THEN
1582 Q.X_GEN_TAC `u:('a->bool)->bool` THEN
1583 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1584 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC (SUBST1_TAC o SYM)) THEN
1585 rw [EXT_SKOLEM_THM] \\
1586 Q.EXISTS_TAC
1587 `IMAGE SND {(s,t) | s IN u /\ t IN (f:('a->bool)->('a->bool)->bool) s}` THEN
1588
1589 ASM_SIMP_TAC std_ss [FINITE_IMAGE, FINITE_PRODUCT_DEPENDENT] THEN
1590 SIMP_TAC std_ss [FORALL_IN_IMAGE, FORALL_IN_GSPEC] THEN
1591 CONJ_TAC THENL [ASM_SET_TAC[], SIMP_TAC std_ss [UNIONS_IMAGE]] THEN
1592 SIMP_TAC std_ss [EXISTS_IN_GSPEC] THEN ASM_SET_TAC[]
1593QED
1594
1595Theorem FINITE_INTERSECTION_OF_IDEMPOT :
1596 !P:('a->bool)->bool.
1597 FINITE INTERSECTION_OF FINITE INTERSECTION_OF P =
1598 FINITE INTERSECTION_OF P
1599Proof
1600 RW_TAC (std_ss ++ ETA_ss) [FUN_EQ_THM, COMPL_COMPL_applied,
1601 FINITE_INTERSECTION_OF_COMPLEMENT] THEN
1602 SIMP_TAC std_ss [FINITE_UNION_OF_IDEMPOT]
1603QED
1604
1605Theorem FINITE_UNION_OF_UNIONS :
1606 !P u:('a->bool)->bool.
1607 FINITE u /\ (!s. s IN u ==> (FINITE UNION_OF P) s)
1608 ==> (FINITE UNION_OF P) (UNIONS u)
1609Proof
1610 REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC [GSYM FINITE_UNION_OF_IDEMPOT] THEN
1611 ONCE_REWRITE_TAC [UNION_OF] THEN SIMP_TAC std_ss [] THEN
1612 Q.EXISTS_TAC `u:('a->bool)->bool` THEN ASM_SIMP_TAC std_ss []
1613QED
1614
1615Theorem FINITE_UNION_OF_UNION :
1616 !P s t. (FINITE UNION_OF P) s /\ (FINITE UNION_OF P) t
1617 ==> (FINITE UNION_OF P) (s UNION t)
1618Proof
1619 REPEAT STRIP_TAC THEN SIMP_TAC std_ss [GSYM UNIONS_2] THEN
1620 MATCH_MP_TAC FINITE_UNION_OF_UNIONS THEN
1621 ASM_SIMP_TAC std_ss [FINITE_INSERT, FORALL_IN_INSERT] THEN
1622 SIMP_TAC std_ss [FINITE_EMPTY, NOT_IN_EMPTY]
1623QED
1624
1625Theorem FINITE_INTERSECTION_OF_INTERS :
1626 !P u:('a->bool)->bool.
1627 FINITE u /\ (!s. s IN u ==> (FINITE INTERSECTION_OF P) s)
1628 ==> (FINITE INTERSECTION_OF P) (INTERS u)
1629Proof
1630 REPEAT STRIP_TAC THEN
1631 ONCE_REWRITE_TAC [GSYM FINITE_INTERSECTION_OF_IDEMPOT] THEN
1632 ONCE_REWRITE_TAC [INTERSECTION_OF] THEN SIMP_TAC std_ss [] THEN
1633 Q.EXISTS_TAC `u:('a->bool)->bool` THEN ASM_SIMP_TAC std_ss []
1634QED
1635
1636Theorem FINITE_INTERSECTION_OF_INTER :
1637 !P s t. (FINITE INTERSECTION_OF P) s /\ (FINITE INTERSECTION_OF P) t
1638 ==> (FINITE INTERSECTION_OF P) (s INTER t)
1639Proof
1640 REPEAT STRIP_TAC THEN SIMP_TAC std_ss [GSYM INTERS_2] THEN
1641 MATCH_MP_TAC FINITE_INTERSECTION_OF_INTERS THEN
1642 ASM_SIMP_TAC std_ss [FINITE_INSERT, FORALL_IN_INSERT] THEN
1643 SIMP_TAC std_ss [FINITE_EMPTY, NOT_IN_EMPTY]
1644QED
1645
1646Theorem FINITE_UNION_OF_INTER_EQ :
1647 !P:('a->bool)->bool.
1648 (!s t. (FINITE UNION_OF P) s /\ (FINITE UNION_OF P) t
1649 ==> (FINITE UNION_OF P) (s INTER t)) <=>
1650 (!s t. P s /\ P t ==> (FINITE UNION_OF P) (s INTER t))
1651Proof
1652 GEN_TAC THEN
1653 EQ_TAC THENL [MESON_TAC[FINITE_UNION_OF_INC], DISCH_TAC] THEN
1654 REPEAT GEN_TAC THEN
1655 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) empty_rewrites [UNION_OF] THEN
1656 SIMP_TAC std_ss [] THEN DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
1657 ASM_SIMP_TAC std_ss [INTER_UNIONS] THEN
1658 REPLICATE_TAC 2
1659 (MATCH_MP_TAC FINITE_UNION_OF_UNIONS THEN
1660 ASM_SIMP_TAC std_ss [SIMPLE_IMAGE, FINITE_IMAGE, FORALL_IN_IMAGE] THEN
1661 REPEAT STRIP_TAC)
1662QED
1663
1664Theorem FINITE_UNION_OF_INTER :
1665 !P:('a->bool)->bool.
1666 (!s t. P s /\ P t ==> P(s INTER t))
1667 ==> (!s t. (FINITE UNION_OF P) s /\ (FINITE UNION_OF P) t
1668 ==> (FINITE UNION_OF P) (s INTER t))
1669Proof
1670 SIMP_TAC std_ss [FINITE_UNION_OF_INTER_EQ] THEN
1671 MESON_TAC[FINITE_UNION_OF_INC]
1672QED
1673
1674Theorem FINITE_INTERSECTION_OF_UNION_EQ :
1675 !P:('a->bool)->bool.
1676 (!s t. (FINITE INTERSECTION_OF P) s /\
1677 (FINITE INTERSECTION_OF P) t
1678 ==> (FINITE INTERSECTION_OF P) (s UNION t)) <=>
1679 (!s t. P s /\ P t ==> (FINITE INTERSECTION_OF P) (s UNION t))
1680Proof
1681 ONCE_REWRITE_TAC [FINITE_INTERSECTION_OF_COMPLEMENT] THEN
1682 SIMP_TAC std_ss [SET_RULE
1683 ``UNIV DIFF (s UNION t) = (UNIV DIFF s) INTER (UNIV DIFF t)``] THEN
1684 SIMP_TAC std_ss [MESON[COMPL_COMPL_applied] ``(!s. P(UNIV DIFF s)) <=> (!s. P s)``] THEN
1685 SIMP_TAC std_ss [FINITE_UNION_OF_INTER_EQ] THEN
1686 SIMP_TAC std_ss [SET_RULE
1687 ``s INTER t = UNIV DIFF ((UNIV DIFF s) UNION (UNIV DIFF t))``] THEN
1688 SIMP_TAC std_ss [MESON[COMPL_COMPL_applied] ``(!s. P(UNIV DIFF s)) <=> (!s. P s)``] THEN
1689 SIMP_TAC std_ss [COMPL_COMPL_applied]
1690QED
1691
1692Theorem FINITE_INTERSECTION_OF_UNION :
1693 !P:('a->bool)->bool.
1694 (!s t. P s /\ P t ==> P(s UNION t))
1695 ==> (!s t. (FINITE INTERSECTION_OF P) s /\
1696 (FINITE INTERSECTION_OF P) t
1697 ==> (FINITE INTERSECTION_OF P) (s UNION t))
1698Proof
1699 SIMP_TAC std_ss [FINITE_INTERSECTION_OF_UNION_EQ] THEN
1700 MESON_TAC[FINITE_INTERSECTION_OF_INC]
1701QED
1702
1703Theorem COUNTABLE_UNION_OF_EMPTY :
1704 !P:('a->bool)->bool. (COUNTABLE UNION_OF P) {}
1705Proof
1706 SIMP_TAC std_ss [UNION_OF_EMPTY, COUNTABLE_EMPTY]
1707QED
1708
1709Theorem COUNTABLE_INTERSECTION_OF_EMPTY :
1710 !P:('a->bool)->bool. (COUNTABLE INTERSECTION_OF P) UNIV
1711Proof
1712 SIMP_TAC std_ss [INTERSECTION_OF_EMPTY, COUNTABLE_EMPTY]
1713QED
1714
1715Theorem COUNTABLE_UNION_OF_INC :
1716 !P s:'a->bool. P s ==> (COUNTABLE UNION_OF P) s
1717Proof
1718 SIMP_TAC std_ss [UNION_OF_INC, COUNTABLE_SING]
1719QED
1720
1721Theorem COUNTABLE_INTERSECTION_OF_INC :
1722 !P s:'a->bool. P s ==> (COUNTABLE INTERSECTION_OF P) s
1723Proof
1724 SIMP_TAC std_ss [INTERSECTION_OF_INC, COUNTABLE_SING]
1725QED
1726
1727Theorem COUNTABLE_UNION_OF_COMPLEMENT :
1728 !P s. (COUNTABLE UNION_OF P) s <=>
1729 (COUNTABLE INTERSECTION_OF (\s. P(univ(:'a) DIFF s))) (univ(:'a) DIFF s)
1730Proof
1731 REPEAT GEN_TAC THEN SIMP_TAC std_ss [UNION_OF, INTERSECTION_OF] THEN
1732 EQ_TAC THEN
1733 DISCH_THEN(Q.X_CHOOSE_THEN `u:('a->bool)->bool` STRIP_ASSUME_TAC) THEN
1734 Q.EXISTS_TAC `IMAGE (\c. univ(:'a) DIFF c) u` THEN
1735 ASM_SIMP_TAC std_ss [COUNTABLE_IMAGE, FORALL_IN_IMAGE, COMPL_COMPL_applied] THEN
1736 ONCE_REWRITE_TAC[UNIONS_INTERS, INTERS_UNIONS] THEN
1737 Q.ABBREV_TAC ‘g = \c. univ(:'a) DIFF c’ \\
1738 ASM_SIMP_TAC std_ss [] \\
1739 ‘{g t | t | t IN IMAGE g u} = IMAGE (\x. g (g x)) u’
1740 by (rw [Once EXTENSION] >> METIS_TAC []) \\
1741 rw [Abbr ‘g’, IMAGE_ID, COMPL_COMPL_applied]
1742QED
1743
1744Theorem COUNTABLE_INTERSECTION_OF_COMPLEMENT :
1745 !P s. (COUNTABLE INTERSECTION_OF P) s <=>
1746 (COUNTABLE UNION_OF (\s. P(univ(:'a) DIFF s))) (univ(:'a) DIFF s)
1747Proof
1748 REWRITE_TAC[COUNTABLE_UNION_OF_COMPLEMENT] THEN
1749 SIMP_TAC (std_ss ++ ETA_ss) [COMPL_COMPL_applied]
1750QED
1751
1752Theorem COUNTABLE_UNION_OF_EXPLICIT :
1753 !P s:'a->bool.
1754 P {}
1755 ==> ((COUNTABLE UNION_OF P) s <=>
1756 ?t. (!n. P(t n)) /\ UNIONS {t n | n IN univ(:num)} = s)
1757Proof
1758 REPEAT STRIP_TAC THEN EQ_TAC THEN
1759 SIMP_TAC std_ss [UNION_OF, LEFT_IMP_EXISTS_THM] THENL
1760 [ (* goal 1 (of 2) *)
1761 Q.X_GEN_TAC `u:('a->bool)->bool` THEN
1762 ASM_CASES_TAC ``u:('a->bool)->bool = {}`` THENL
1763 [ (* goal 1.1 (of 2) *)
1764 ASM_REWRITE_TAC[UNIONS_0] THEN
1765 DISCH_THEN(SUBST1_TAC o SYM o last o CONJUNCTS) THEN
1766 Q.EXISTS_TAC `(\n. {}):num->'a->bool` THEN
1767 ASM_SIMP_TAC std_ss [UNIONS_GSPEC, NOT_IN_EMPTY, EMPTY_GSPEC],
1768 (* goal 1.2 (of 2) *)
1769 STRIP_TAC THEN
1770 MP_TAC(Q.ISPEC `u:('a->bool)->bool` COUNTABLE_AS_IMAGE) THEN
1771 RW_TAC std_ss [] >> fs [IN_IMAGE] \\
1772 Q.EXISTS_TAC ‘f’ >> ASM_SET_TAC[] ],
1773 (* goal 2 (of 2) *)
1774 Q.X_GEN_TAC `t:num->'a->bool` THEN STRIP_TAC THEN
1775 Q.EXISTS_TAC `{t n:'a->bool | n IN univ(:num)}` THEN
1776 ASM_REWRITE_TAC[FORALL_IN_GSPEC] THEN
1777 rw [SIMPLE_IMAGE, COUNTABLE_IMAGE, COUNTABLE_SUBSET_NUM] THEN
1778 ASM_REWRITE_TAC [] ]
1779QED
1780
1781Theorem COUNTABLE_UNION_OF_ASCENDING :
1782 !P s:'a->bool.
1783 P {} /\ (!t u. P t /\ P u ==> P(t UNION u))
1784 ==> ((COUNTABLE UNION_OF P) s <=>
1785 ?t. (!n. P(t n)) /\
1786 (!n. t n SUBSET t(SUC n)) /\
1787 UNIONS {t n | n IN univ(:num)} = s)
1788Proof
1789 REPEAT STRIP_TAC THEN
1790 ASM_SIMP_TAC std_ss [COUNTABLE_UNION_OF_EXPLICIT, IN_UNIV] THEN
1791 reverse EQ_TAC >- METIS_TAC [] \\
1792 DISCH_THEN(Q.X_CHOOSE_THEN `t:num->'a->bool` STRIP_ASSUME_TAC) THEN
1793 Q.EXISTS_TAC `(\n. UNIONS {t m | m <= n}):num->'a->bool` THEN
1794 RULE_ASSUM_TAC(REWRITE_RULE[FORALL_IN_IMAGE, IN_UNIV]) THEN
1795 REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL
1796 [ (* goal 1 (of 3) *)
1797 Induct_on ‘n’ >> rw [LE]
1798 >- (‘BIGUNION {t m | m = 0} = t 0’ by rw [Once EXTENSION] \\
1799 POP_ASSUM (ASM_REWRITE_TAC o wrap)) \\
1800 SIMP_TAC std_ss [SET_RULE ``{f x | P x \/ Q x} = {f x | P x} UNION {f x | Q x}``,
1801 SET_RULE ``{f x | x = a} = {f a}``, UNIONS_UNION] THEN
1802 ASM_SIMP_TAC std_ss [UNIONS_1] \\
1803 FIRST_X_ASSUM MATCH_MP_TAC >> fs [],
1804 (* goal 2 (of 3) *)
1805 RW_TAC std_ss [UNIONS_GSPEC, LE] THEN SET_TAC[],
1806 (* goal 3 (of 3) *)
1807 FIRST_X_ASSUM(SUBST1_TAC o SYM o last o CONJUNCTS) THEN
1808 SIMP_TAC std_ss [UNIONS_GSPEC, IN_UNIV] \\
1809 rw [Once EXTENSION] \\
1810 EQ_TAC >> rw [] >- (Q.EXISTS_TAC ‘m’ >> rw []) \\
1811 qexistsl_tac [‘n’, ‘n’] >> rw [] ]
1812QED
1813
1814Theorem COUNTABLE_UNION_OF_IDEMPOT :
1815 !P:('a->bool)->bool.
1816 COUNTABLE UNION_OF COUNTABLE UNION_OF P = COUNTABLE UNION_OF P
1817Proof
1818 GEN_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN Q.X_GEN_TAC `s:'a->bool` THEN
1819 EQ_TAC THEN REWRITE_TAC[COUNTABLE_UNION_OF_INC] THEN
1820 SIMP_TAC std_ss [UNION_OF, LEFT_IMP_EXISTS_THM] THEN
1821 Q.X_GEN_TAC `u:('a->bool)->bool` THEN
1822 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1823 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC (SUBST1_TAC o SYM)) THEN
1824 rw [EXT_SKOLEM_THM] \\
1825 Q.EXISTS_TAC
1826 `IMAGE SND {s,t | s IN u /\ t IN (f:('a->bool)->('a->bool)->bool) s}` THEN
1827 ASM_SIMP_TAC std_ss [COUNTABLE_IMAGE, COUNTABLE_PRODUCT_DEPENDENT] THEN
1828 REWRITE_TAC[FORALL_IN_IMAGE, FORALL_IN_GSPEC] THEN
1829 rw [] >- METIS_TAC [SND] \\
1830 REWRITE_TAC[UNIONS_IMAGE] THEN
1831 REWRITE_TAC[EXISTS_IN_GSPEC] THEN ASM_SET_TAC[]
1832QED
1833
1834Theorem COUNTABLE_INTERSECTION_OF_IDEMPOT :
1835 !P:('a->bool)->bool.
1836 COUNTABLE INTERSECTION_OF COUNTABLE INTERSECTION_OF P =
1837 COUNTABLE INTERSECTION_OF P
1838Proof
1839 RW_TAC (std_ss ++ ETA_ss)
1840 [COMPL_COMPL_applied, FUN_EQ_THM, COUNTABLE_INTERSECTION_OF_COMPLEMENT] THEN
1841 REWRITE_TAC[COUNTABLE_UNION_OF_IDEMPOT]
1842QED
1843
1844Theorem COUNTABLE_UNION_OF_UNIONS :
1845 !P u:('a->bool)->bool.
1846 COUNTABLE u /\ (!s. s IN u ==> (COUNTABLE UNION_OF P) s)
1847 ==> (COUNTABLE UNION_OF P) (UNIONS u)
1848Proof
1849 REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM COUNTABLE_UNION_OF_IDEMPOT] THEN
1850 ONCE_REWRITE_TAC[UNION_OF] THEN SIMP_TAC std_ss [] THEN
1851 Q.EXISTS_TAC `u:('a->bool)->bool` THEN ASM_REWRITE_TAC[]
1852QED
1853
1854Theorem COUNTABLE_UNION_OF_UNION :
1855 !P s t. (COUNTABLE UNION_OF P) s /\ (COUNTABLE UNION_OF P) t
1856 ==> (COUNTABLE UNION_OF P) (s UNION t)
1857Proof
1858 REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM UNIONS_2] THEN
1859 MATCH_MP_TAC COUNTABLE_UNION_OF_UNIONS THEN
1860 ASM_REWRITE_TAC[COUNTABLE_INSERT, FORALL_IN_INSERT] THEN
1861 REWRITE_TAC[COUNTABLE_EMPTY, NOT_IN_EMPTY]
1862QED
1863
1864Theorem COUNTABLE_INTERSECTION_OF_INTERS :
1865 !P u:('a->bool)->bool.
1866 COUNTABLE u /\ (!s. s IN u ==> (COUNTABLE INTERSECTION_OF P) s)
1867 ==> (COUNTABLE INTERSECTION_OF P) (INTERS u)
1868Proof
1869 REPEAT STRIP_TAC THEN
1870 ONCE_REWRITE_TAC[GSYM COUNTABLE_INTERSECTION_OF_IDEMPOT] THEN
1871 ONCE_REWRITE_TAC[INTERSECTION_OF] THEN SIMP_TAC std_ss [] THEN
1872 Q.EXISTS_TAC `u:('a->bool)->bool` THEN ASM_REWRITE_TAC[]
1873QED
1874
1875Theorem COUNTABLE_INTERSECTION_OF_INTER :
1876 !P s t. (COUNTABLE INTERSECTION_OF P) s /\ (COUNTABLE INTERSECTION_OF P) t
1877 ==> (COUNTABLE INTERSECTION_OF P) (s INTER t)
1878Proof
1879 REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM INTERS_2] THEN
1880 MATCH_MP_TAC COUNTABLE_INTERSECTION_OF_INTERS THEN
1881 ASM_REWRITE_TAC[COUNTABLE_INSERT, FORALL_IN_INSERT] THEN
1882 REWRITE_TAC[COUNTABLE_EMPTY, NOT_IN_EMPTY]
1883QED
1884
1885Theorem COUNTABLE_UNION_OF_INTER_EQ :
1886 !P:('a->bool)->bool.
1887 (!s t. (COUNTABLE UNION_OF P) s /\ (COUNTABLE UNION_OF P) t
1888 ==> (COUNTABLE UNION_OF P) (s INTER t)) <=>
1889 (!s t. P s /\ P t ==> (COUNTABLE UNION_OF P) (s INTER t))
1890Proof
1891 GEN_TAC THEN
1892 EQ_TAC THENL [MESON_TAC[COUNTABLE_UNION_OF_INC], DISCH_TAC] THEN
1893 REPEAT GEN_TAC THEN
1894 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) empty_rewrites [UNION_OF] THEN
1895 SIMP_TAC std_ss [] THEN DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
1896 ASM_REWRITE_TAC[INTER_UNIONS] THEN
1897 REPLICATE_TAC 2
1898 (MATCH_MP_TAC COUNTABLE_UNION_OF_UNIONS THEN
1899 ASM_SIMP_TAC std_ss [SIMPLE_IMAGE, COUNTABLE_IMAGE, FORALL_IN_IMAGE] THEN
1900 REPEAT STRIP_TAC)
1901QED
1902
1903Theorem COUNTABLE_UNION_OF_INTER :
1904 !P:('a->bool)->bool.
1905 (!s t. P s /\ P t ==> P(s INTER t))
1906 ==> (!s t. (COUNTABLE UNION_OF P) s /\ (COUNTABLE UNION_OF P) t
1907 ==> (COUNTABLE UNION_OF P) (s INTER t))
1908Proof
1909 REWRITE_TAC[COUNTABLE_UNION_OF_INTER_EQ] THEN
1910 MESON_TAC[COUNTABLE_UNION_OF_INC]
1911QED
1912
1913Theorem COUNTABLE_INTERSECTION_OF_UNION_EQ :
1914 !P:('a->bool)->bool.
1915 (!s t. (COUNTABLE INTERSECTION_OF P) s /\
1916 (COUNTABLE INTERSECTION_OF P) t
1917 ==> (COUNTABLE INTERSECTION_OF P) (s UNION t)) <=>
1918 (!s t. P s /\ P t ==> (COUNTABLE INTERSECTION_OF P) (s UNION t))
1919Proof
1920 ONCE_REWRITE_TAC[COUNTABLE_INTERSECTION_OF_COMPLEMENT] THEN
1921 REWRITE_TAC[SET_RULE
1922 ``UNIV DIFF (s UNION t) = (UNIV DIFF s) INTER (UNIV DIFF t)``] THEN
1923 SIMP_TAC std_ss [MESON[COMPL_COMPL_applied] ``(!s. P(UNIV DIFF s)) <=> (!s. P s)``] THEN
1924 SIMP_TAC std_ss [COUNTABLE_UNION_OF_INTER_EQ] THEN
1925 REWRITE_TAC[SET_RULE
1926 ``s INTER t = UNIV DIFF ((UNIV DIFF s) UNION (UNIV DIFF t))``] THEN
1927 SIMP_TAC std_ss [MESON[COMPL_COMPL_applied] ``(!s. P(UNIV DIFF s)) <=> (!s. P s)``] THEN
1928 REWRITE_TAC[COMPL_COMPL_applied]
1929QED
1930
1931Theorem COUNTABLE_INTERSECTION_OF_UNION :
1932 !P:('a->bool)->bool.
1933 (!s t. P s /\ P t ==> P(s UNION t))
1934 ==> (!s t. (COUNTABLE INTERSECTION_OF P) s /\
1935 (COUNTABLE INTERSECTION_OF P) t
1936 ==> (COUNTABLE INTERSECTION_OF P) (s UNION t))
1937Proof
1938 REWRITE_TAC[COUNTABLE_INTERSECTION_OF_UNION_EQ] THEN
1939 MESON_TAC[COUNTABLE_INTERSECTION_OF_INC]
1940QED
1941
1942Theorem COUNTABLE_INTERSECTION_OF_UNIONS_NONEMPTY :
1943 !P u:('a->bool)->bool.
1944 (!s t. P s /\ P t ==> P (s UNION t)) /\
1945 FINITE u /\ ~(u = {}) /\
1946 (!s. s IN u ==> (COUNTABLE INTERSECTION_OF P) s)
1947 ==> (COUNTABLE INTERSECTION_OF P) (UNIONS u)
1948Proof
1949 REWRITE_TAC[IMP_CONJ, RIGHT_FORALL_IMP_THM] THEN
1950 rpt GEN_TAC THEN DISCH_TAC THEN
1951 RULE_ASSUM_TAC(REWRITE_RULE[IMP_IMP, RIGHT_IMP_FORALL_THM]) THEN
1952 Q.SPEC_TAC (‘u’, ‘u’) \\
1953 HO_MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
1954 SIMP_TAC std_ss [FORALL_IN_INSERT, NOT_INSERT_EMPTY] THEN
1955 qx_genl_tac [`s:'a->bool`, `u:('a->bool)->bool`] THEN
1956 ASM_CASES_TAC ``u:('a->bool)->bool = {}`` THEN
1957 ASM_SIMP_TAC std_ss [UNIONS_1] THEN REWRITE_TAC[UNIONS_INSERT] THEN
1958 REPEAT STRIP_TAC THEN
1959 FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP COUNTABLE_INTERSECTION_OF_UNION) THEN
1960 ASM_SIMP_TAC std_ss []
1961QED
1962
1963Theorem COUNTABLE_INTERSECTION_OF_UNIONS :
1964 !P u:('a->bool)->bool.
1965 (COUNTABLE INTERSECTION_OF P) {} /\
1966 (!s t. P s /\ P t ==> P (s UNION t)) /\
1967 FINITE u /\
1968 (!s. s IN u ==> (COUNTABLE INTERSECTION_OF P) s)
1969 ==> (COUNTABLE INTERSECTION_OF P) (UNIONS u)
1970Proof
1971 REPEAT GEN_TAC THEN
1972 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1973 ASM_CASES_TAC ``u:('a->bool)->bool = {}`` THEN
1974 ASM_REWRITE_TAC[UNIONS_0] THEN STRIP_TAC THEN
1975 MATCH_MP_TAC COUNTABLE_INTERSECTION_OF_UNIONS_NONEMPTY THEN
1976 ASM_REWRITE_TAC[]
1977QED
1978
1979Theorem COUNTABLE_UNION_OF_INTERS_NONEMPTY :
1980 !P u:('a->bool)->bool.
1981 (!s t. P s /\ P t ==> P (s INTER t)) /\
1982 FINITE u /\ ~(u = {}) /\
1983 (!s. s IN u ==> (COUNTABLE UNION_OF P) s)
1984 ==> (COUNTABLE UNION_OF P) (INTERS u)
1985Proof
1986 REWRITE_TAC[IMP_CONJ, RIGHT_FORALL_IMP_THM] THEN
1987 rpt GEN_TAC THEN DISCH_TAC THEN
1988 RULE_ASSUM_TAC(REWRITE_RULE[IMP_IMP, RIGHT_IMP_FORALL_THM]) THEN
1989 Q.SPEC_TAC (‘u’, ‘u’) \\
1990 HO_MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
1991 REWRITE_TAC[FORALL_IN_INSERT, NOT_INSERT_EMPTY] THEN
1992 qx_genl_tac [`s:'a->bool`, `u:('a->bool)->bool`] THEN
1993 ASM_CASES_TAC ``u:('a->bool)->bool = {}`` THEN
1994 ASM_SIMP_TAC std_ss [INTERS_1] THEN REWRITE_TAC[INTERS_INSERT] THEN
1995 REPEAT STRIP_TAC THEN
1996 FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP COUNTABLE_UNION_OF_INTER) THEN
1997 ASM_SIMP_TAC std_ss []
1998QED
1999
2000Theorem COUNTABLE_UNION_OF_INTERS :
2001 !P u:('a->bool)->bool.
2002 (COUNTABLE UNION_OF P) univ(:'a) /\
2003 (!s t. P s /\ P t ==> P (s INTER t)) /\
2004 FINITE u /\
2005 (!s. s IN u ==> (COUNTABLE UNION_OF P) s)
2006 ==> (COUNTABLE UNION_OF P) (INTERS u)
2007Proof
2008 REPEAT GEN_TAC THEN
2009 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
2010 ASM_CASES_TAC ``u:('a->bool)->bool = {}`` THEN
2011 ASM_REWRITE_TAC[INTERS_0] THEN STRIP_TAC THEN
2012 MATCH_MP_TAC COUNTABLE_UNION_OF_INTERS_NONEMPTY THEN
2013 ASM_REWRITE_TAC[]
2014QED
2015
2016Theorem COUNTABLE_DISJOINT_UNION_OF_IDEMPOT :
2017 !P:('a->bool)->bool.
2018 ((COUNTABLE INTER pairwise DISJOINT) UNION_OF
2019 (COUNTABLE INTER pairwise DISJOINT) UNION_OF P) =
2020 (COUNTABLE INTER pairwise DISJOINT) UNION_OF P
2021Proof
2022 GEN_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN Q.X_GEN_TAC `s:'a->bool` THEN
2023 reverse EQ_TAC
2024 >- (MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] UNION_OF_INC) THEN
2025 rw [INTER_DEF, IN_APP, COUNTABLE_SING, PAIRWISE_SING]) \\
2026 SIMP_TAC std_ss [SET_RULE ``s INTER t = \x. s x /\ t x``] \\
2027 SIMP_TAC std_ss [UNION_OF, LEFT_IMP_EXISTS_THM] THEN
2028 Q.X_GEN_TAC `u:('a->bool)->bool` THEN
2029 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
2030 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC (SUBST1_TAC o SYM)) THEN
2031 rw [EXT_SKOLEM_THM] \\
2032 Q.EXISTS_TAC
2033 `IMAGE SND {s,t | s IN u /\ t IN (f:('a->bool)->('a->bool)->bool) s}` THEN
2034 ASM_SIMP_TAC std_ss [COUNTABLE_IMAGE, COUNTABLE_PRODUCT_DEPENDENT] THEN
2035 SIMP_TAC std_ss [FORALL_IN_IMAGE, FORALL_IN_GSPEC] THEN
2036 REWRITE_TAC[UNIONS_IMAGE, EXISTS_IN_GSPEC, PAIRWISE_IMAGE] THEN
2037 CONJ_TAC THENL [REWRITE_TAC[pairwise], ASM_SET_TAC[]] THEN
2038 SIMP_TAC std_ss [IMP_CONJ, RIGHT_FORALL_IMP_THM, FORALL_IN_GSPEC] THEN
2039 MAP_EVERY (fn x => Q.X_GEN_TAC x THEN DISCH_TAC)
2040 [`s1:'a->bool`, `t1:'a->bool`, `s2:'a->bool`, `t2:'a->bool`] THEN
2041 DISCH_THEN(K ALL_TAC) THEN ASM_CASES_TAC ``s2:'a->bool = s1`` THEN
2042 RULE_ASSUM_TAC(REWRITE_RULE[pairwise]) THENL
2043 [ ASM_MESON_TAC[], ASM_SET_TAC[] ]
2044QED
2045
2046(* ------------------------------------------------------------------------- *)
2047(* A somewhat cheap but handy way of getting localized forms of various *)
2048(* topological concepts (open, closed, borel, fsigma, gdelta etc.) *)
2049(* ------------------------------------------------------------------------- *)
2050
2051val _ = set_fixity "relative_to" (Infixl 500);
2052
2053Definition relative_to :
2054 (P relative_to s) t = ?u. P u /\ s INTER u = t
2055End
2056
2057Theorem RELATIVE_TO_UNIV :
2058 !P s. (P relative_to univ(:'a)) s <=> P s
2059Proof
2060 REWRITE_TAC[relative_to, INTER_UNIV] THEN MESON_TAC[]
2061QED
2062
2063Theorem RELATIVE_TO_IMP_SUBSET :
2064 !P s t. (P relative_to s) t ==> t SUBSET s
2065Proof
2066 REWRITE_TAC[relative_to] THEN SET_TAC[]
2067QED
2068
2069Theorem FORALL_RELATIVE_TO :
2070 (!s. (P relative_to u) s ==> Q s) <=>
2071 (!s. P s ==> Q(u INTER s))
2072Proof
2073 REWRITE_TAC[relative_to] THEN MESON_TAC[]
2074QED
2075
2076Theorem RELATIVE_TO_INC :
2077 !P u s. P s ==> (P relative_to u) (u INTER s)
2078Proof
2079 REWRITE_TAC[relative_to] THEN MESON_TAC[]
2080QED
2081
2082Theorem RELATIVE_TO :
2083 (P relative_to u) = {u INTER s | P s}
2084Proof
2085 rw [Once EXTENSION, relative_to, IN_APP]
2086 >> SET_TAC []
2087QED
2088
2089Theorem RELATIVE_TO_RELATIVE_TO :
2090 !P:('a->bool)->bool s t.
2091 P relative_to s relative_to t = P relative_to (s INTER t)
2092Proof
2093 rw [Once EXTENSION, RELATIVE_TO]
2094 >> EQ_TAC >> rw [] >> rename1 ‘P u’
2095 >- (Q.EXISTS_TAC ‘u’ >> METIS_TAC [INTER_ASSOC, INTER_COMM])
2096 >> Q.EXISTS_TAC ‘s INTER u’
2097 >> CONJ_TAC >- METIS_TAC [INTER_ASSOC, INTER_COMM]
2098 >> Q.EXISTS_TAC ‘u’ >> rw []
2099QED
2100
2101Theorem RELATIVE_TO_COMPL :
2102 !P u s:'a->bool.
2103 s SUBSET u
2104 ==> ((P relative_to u) (u DIFF s) <=>
2105 ((\c. P(UNIV DIFF c)) relative_to u) s)
2106Proof
2107 rpt STRIP_TAC >> REWRITE_TAC [relative_to]
2108 >> EQ_TAC >> rw []
2109 >- (rename1 ‘P w’ \\
2110 Q.EXISTS_TAC ‘univ(:'a) DIFF w’ >> rw [COMPL_COMPL_applied] \\
2111 ASM_SET_TAC [])
2112 >> rename1 ‘u INTER w SUBSET u’
2113 >> Q.EXISTS_TAC ‘univ(:'a) DIFF w’ >> rw []
2114 >> ASM_SET_TAC []
2115QED
2116
2117Theorem RELATIVE_TO_SUBSET :
2118 !P s t:'a->bool. s SUBSET t /\ P s ==> (P relative_to t) s
2119Proof
2120 REPEAT STRIP_TAC THEN REWRITE_TAC[relative_to] THEN
2121 Q.EXISTS_TAC `s:'a->bool` THEN ASM_SET_TAC[]
2122QED
2123
2124Theorem RELATIVE_TO_SUBSET_TRANS :
2125 !P u s t:'a->bool.
2126 (P relative_to u) s /\ s SUBSET t /\ t SUBSET u ==> (P relative_to t) s
2127Proof
2128 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN
2129 REWRITE_TAC[relative_to] THEN
2130 HO_MATCH_MP_TAC MONO_EXISTS THEN ASM_SET_TAC[]
2131QED
2132
2133Theorem RELATIVE_TO_MONO :
2134 !P Q.
2135 (!s. P s ==> Q s) ==> !u. (P relative_to u) s ==> (Q relative_to u) s
2136Proof
2137 REWRITE_TAC[relative_to] THEN MESON_TAC[]
2138QED
2139
2140Theorem RELATIVE_TO_SUBSET_INC :
2141 !P u s:'a->bool.
2142 s SUBSET u /\ P s ==> (P relative_to u) s
2143Proof
2144 REWRITE_TAC[relative_to] THEN
2145 MESON_TAC[SET_RULE ``s SUBSET u ==> u INTER s = s``]
2146QED
2147
2148Theorem RELATIVE_TO_INTER :
2149 !P s. (!c d:'a->bool. P c /\ P d ==> P(c INTER d))
2150 ==> !c d. (P relative_to s) c /\ (P relative_to s) d
2151 ==> (P relative_to s) (c INTER d)
2152Proof
2153 REPEAT GEN_TAC THEN DISCH_TAC THEN REPEAT GEN_TAC THEN
2154 REWRITE_TAC[relative_to] THEN DISCH_THEN(CONJUNCTS_THEN2
2155 (Q.X_CHOOSE_THEN `c':'a->bool` (STRIP_ASSUME_TAC o GSYM))
2156 (Q.X_CHOOSE_THEN `d':'a->bool` (STRIP_ASSUME_TAC o GSYM))) THEN
2157 Q.EXISTS_TAC `c' INTER d':'a->bool` THEN
2158 ASM_SIMP_TAC std_ss [] THEN ASM_SET_TAC[]
2159QED
2160
2161Theorem RELATIVE_TO_UNION :
2162 !P s. (!c d:'a->bool. P c /\ P d ==> P(c UNION d))
2163 ==> !c d. (P relative_to s) c /\ (P relative_to s) d
2164 ==> (P relative_to s) (c UNION d)
2165Proof
2166 REPEAT GEN_TAC THEN DISCH_TAC THEN REPEAT GEN_TAC THEN
2167 REWRITE_TAC[relative_to] THEN DISCH_THEN(CONJUNCTS_THEN2
2168 (Q.X_CHOOSE_THEN `c':'a->bool` (STRIP_ASSUME_TAC o GSYM))
2169 (Q.X_CHOOSE_THEN `d':'a->bool` (STRIP_ASSUME_TAC o GSYM))) THEN
2170 Q.EXISTS_TAC `c' UNION d':'a->bool` THEN
2171 ASM_SIMP_TAC std_ss [] THEN ASM_SET_TAC[]
2172QED
2173
2174Theorem ARBITRARY_UNION_OF_RELATIVE_TO :
2175 !P u:'a->bool.
2176 ((ARBITRARY UNION_OF P) relative_to u) =
2177 (ARBITRARY UNION_OF (P relative_to u))
2178Proof
2179 REWRITE_TAC[FUN_EQ_THM] THEN
2180 REPEAT STRIP_TAC THEN SIMP_TAC std_ss [UNION_OF, relative_to] THEN
2181 EQ_TAC THENL
2182 [ (* goal 1 (of 2) *)
2183 DISCH_THEN(Q.X_CHOOSE_THEN `t:'a->bool`
2184 (CONJUNCTS_THEN2 MP_TAC (SUBST1_TAC o SYM))) THEN
2185 DISCH_THEN(Q.X_CHOOSE_THEN `f:('a->bool)->bool`
2186 (STRIP_ASSUME_TAC o GSYM)) THEN
2187 Q.EXISTS_TAC `{u INTER c | (c:'a->bool) IN f}` THEN
2188 ASM_REWRITE_TAC[INTER_UNIONS] THEN
2189 ASM_SIMP_TAC std_ss [SIMPLE_IMAGE, ARBITRARY, FORALL_IN_IMAGE] THEN
2190 ASM_MESON_TAC[],
2191 (* goal 2 (of 2) *)
2192 DISCH_THEN(Q.X_CHOOSE_THEN `f:('a->bool)->bool` STRIP_ASSUME_TAC) THEN
2193 Q.PAT_X_ASSUM ‘!c. c IN f ==> _’ MP_TAC \\
2194 rw [EXT_SKOLEM_THM] \\
2195 rename1 ‘!c. c IN f ==> P (g c) /\ u INTER g c = c’ \\
2196 Q.EXISTS_TAC `UNIONS (IMAGE (g:('a->bool)->('a->bool)) f)` THEN
2197 CONJ_TAC THENL [ALL_TAC, ASM_SET_TAC[]] THEN
2198 Q.EXISTS_TAC `IMAGE (g:('a->bool)->('a->bool)) f` THEN
2199 ASM_SIMP_TAC std_ss [ARBITRARY, FORALL_IN_IMAGE] ]
2200QED
2201
2202Theorem FINITE_UNION_OF_RELATIVE_TO :
2203 !P u:'a->bool.
2204 ((FINITE UNION_OF P) relative_to u) =
2205 (FINITE UNION_OF (P relative_to u))
2206Proof
2207 REWRITE_TAC[FUN_EQ_THM] THEN
2208 REPEAT STRIP_TAC THEN SIMP_TAC std_ss [UNION_OF, relative_to]
2209 THEN EQ_TAC THENL
2210 [ (* goal 1 (of 2) *)
2211 DISCH_THEN(Q.X_CHOOSE_THEN `t:'a->bool`
2212 (CONJUNCTS_THEN2 MP_TAC (SUBST1_TAC o SYM))) THEN
2213 DISCH_THEN(Q.X_CHOOSE_THEN `f:('a->bool)->bool`
2214 (STRIP_ASSUME_TAC o GSYM)) THEN
2215 Q.EXISTS_TAC `{u INTER c | (c:'a->bool) IN f}` THEN
2216 ASM_REWRITE_TAC[INTER_UNIONS] THEN
2217 ASM_SIMP_TAC std_ss [SIMPLE_IMAGE, FINITE_IMAGE, FORALL_IN_IMAGE] THEN
2218 ASM_MESON_TAC[],
2219 (* goal 2 (of 2) *)
2220 DISCH_THEN(Q.X_CHOOSE_THEN `f:('a->bool)->bool` STRIP_ASSUME_TAC) THEN
2221 Q.PAT_X_ASSUM ‘!c. c IN f ==> _’ MP_TAC \\
2222 rw [EXT_SKOLEM_THM] \\
2223 rename1 ‘!c. c IN f ==> P (g c) /\ u INTER g c = c’ \\
2224 Q.EXISTS_TAC `UNIONS (IMAGE (g:('a->bool)->('a->bool)) f)` THEN
2225 CONJ_TAC THENL [ALL_TAC, ASM_SET_TAC[]] THEN
2226 Q.EXISTS_TAC `IMAGE (g:('a->bool)->('a->bool)) f` THEN
2227 ASM_SIMP_TAC std_ss [FINITE_IMAGE, FORALL_IN_IMAGE] ]
2228QED
2229
2230Theorem COUNTABLE_UNION_OF_RELATIVE_TO :
2231 !P u:'a->bool.
2232 ((COUNTABLE UNION_OF P) relative_to u) =
2233 (COUNTABLE UNION_OF (P relative_to u))
2234Proof
2235 REWRITE_TAC[FUN_EQ_THM] THEN
2236 REPEAT STRIP_TAC THEN SIMP_TAC std_ss [UNION_OF, relative_to]
2237 THEN EQ_TAC THENL
2238 [ (* goal 1 (of 2) *)
2239 DISCH_THEN(Q.X_CHOOSE_THEN `t:'a->bool`
2240 (CONJUNCTS_THEN2 MP_TAC (SUBST1_TAC o SYM))) THEN
2241 DISCH_THEN(Q.X_CHOOSE_THEN `f:('a->bool)->bool`
2242 (STRIP_ASSUME_TAC o GSYM)) THEN
2243 Q.EXISTS_TAC `{u INTER c | (c:'a->bool) IN f}` THEN
2244 ASM_REWRITE_TAC[INTER_UNIONS] THEN
2245 ASM_SIMP_TAC std_ss [SIMPLE_IMAGE, COUNTABLE_IMAGE, FORALL_IN_IMAGE] THEN
2246 ASM_MESON_TAC[],
2247 (* goal 2 (of 2) *)
2248 DISCH_THEN(Q.X_CHOOSE_THEN `f:('a->bool)->bool` STRIP_ASSUME_TAC) THEN
2249 Q.PAT_X_ASSUM ‘!c. c IN f ==> _’ MP_TAC \\
2250 rw [EXT_SKOLEM_THM] \\
2251 rename1 ‘!c. c IN f ==> P (g c) /\ u INTER g c = c’ \\
2252 Q.EXISTS_TAC `UNIONS (IMAGE (g:('a->bool)->('a->bool)) f)` THEN
2253 CONJ_TAC THENL [ALL_TAC, ASM_SET_TAC[]] THEN
2254 Q.EXISTS_TAC `IMAGE (g:('a->bool)->('a->bool)) f` THEN
2255 ASM_SIMP_TAC std_ss [COUNTABLE_IMAGE, FORALL_IN_IMAGE] ]
2256QED
2257
2258Theorem ARBITRARY_INTERSECTION_OF_RELATIVE_TO :
2259 !P u:'a->bool.
2260 ((ARBITRARY INTERSECTION_OF P) relative_to u) =
2261 ((ARBITRARY INTERSECTION_OF (P relative_to u)) relative_to u)
2262Proof
2263 REPEAT GEN_TAC THEN GEN_REWRITE_TAC I empty_rewrites [FUN_EQ_THM] THEN
2264 Q.X_GEN_TAC `s:'a->bool` THEN REWRITE_TAC[INTERSECTION_OF, relative_to] THEN
2265 BETA_TAC THEN EQ_TAC THENL
2266 [ (* goal 1 (of 2) *)
2267 DISCH_THEN(Q.X_CHOOSE_THEN `t:'a->bool`
2268 (CONJUNCTS_THEN2 MP_TAC (SUBST1_TAC o SYM))) THEN
2269 DISCH_THEN(Q.X_CHOOSE_THEN `f:('a->bool)->bool`
2270 (STRIP_ASSUME_TAC o GSYM)) THEN
2271 Q.EXISTS_TAC `INTERS {u INTER c | (c:'a->bool) IN f}` THEN CONJ_TAC THENL
2272 [ (* goal 1.1 (of 2) *)
2273 Q.EXISTS_TAC `{u INTER c | (c:'a->bool) IN f}` THEN
2274 ASM_SIMP_TAC std_ss [ARBITRARY, SIMPLE_IMAGE, FORALL_IN_IMAGE] THEN
2275 ASM_MESON_TAC[],
2276 (* goal 1.2 (of 2) *)
2277 ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[INTER_INTERS] THEN
2278 SIMP_TAC std_ss [SIMPLE_IMAGE, IMAGE_EQ_EMPTY, INTERS_IMAGE, FORALL_IN_IMAGE,
2279 SET_RULE ``u INTER (u INTER s) = u INTER s``] ],
2280 (* goal 2 (of 2) *)
2281 DISCH_THEN(Q.X_CHOOSE_THEN `t:'a->bool`
2282 (CONJUNCTS_THEN2 MP_TAC (SUBST1_TAC o SYM))) THEN
2283 DISCH_THEN(Q.X_CHOOSE_THEN `f:('a->bool)->bool` STRIP_ASSUME_TAC) THEN
2284 Q.PAT_X_ASSUM ‘!c. c IN f ==> _’ MP_TAC \\
2285 rw [EXT_SKOLEM_THM] \\
2286 rename1 ‘!c. c IN f ==> P (g c) /\ u INTER g c = c’ \\
2287 Q.EXISTS_TAC `INTERS (IMAGE (g:('a->bool)->('a->bool)) f)` THEN
2288 CONJ_TAC THENL [ALL_TAC, ASM_SET_TAC[]] THEN
2289 Q.EXISTS_TAC `IMAGE (g:('a->bool)->('a->bool)) f` THEN
2290 ASM_SIMP_TAC std_ss [ARBITRARY, FORALL_IN_IMAGE] ]
2291QED
2292
2293Theorem FINITE_INTERSECTION_OF_RELATIVE_TO :
2294 !P u:'a->bool.
2295 ((FINITE INTERSECTION_OF P) relative_to u) =
2296 ((FINITE INTERSECTION_OF (P relative_to u)) relative_to u)
2297Proof
2298 REPEAT GEN_TAC THEN GEN_REWRITE_TAC I empty_rewrites [FUN_EQ_THM] THEN
2299 Q.X_GEN_TAC `s:'a->bool` THEN REWRITE_TAC[INTERSECTION_OF, relative_to] THEN
2300 BETA_TAC THEN EQ_TAC THENL
2301 [ (* goal 1 (of 2) *)
2302 DISCH_THEN(Q.X_CHOOSE_THEN `t:'a->bool`
2303 (CONJUNCTS_THEN2 MP_TAC (SUBST1_TAC o SYM))) THEN
2304 DISCH_THEN(Q.X_CHOOSE_THEN `f:('a->bool)->bool`
2305 (STRIP_ASSUME_TAC o GSYM)) THEN
2306 Q.EXISTS_TAC `INTERS {u INTER c | (c:'a->bool) IN f}` THEN CONJ_TAC THENL
2307 [ (* goal 1.1 (of 2) *)
2308 Q.EXISTS_TAC `{u INTER c | (c:'a->bool) IN f}` THEN
2309 ASM_SIMP_TAC std_ss [FINITE_IMAGE, SIMPLE_IMAGE, FORALL_IN_IMAGE] THEN
2310 ASM_MESON_TAC[],
2311 (* goal 1.2 (of 2) *)
2312 ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[INTER_INTERS] THEN
2313 SIMP_TAC std_ss [SIMPLE_IMAGE, IMAGE_EQ_EMPTY, INTERS_IMAGE, FORALL_IN_IMAGE,
2314 SET_RULE ``u INTER (u INTER s) = u INTER s``] ],
2315 (* goal 2 (of 2) *)
2316 DISCH_THEN(Q.X_CHOOSE_THEN `t:'a->bool`
2317 (CONJUNCTS_THEN2 MP_TAC (SUBST1_TAC o SYM))) THEN
2318 DISCH_THEN(Q.X_CHOOSE_THEN `f:('a->bool)->bool` STRIP_ASSUME_TAC) THEN
2319 Q.PAT_X_ASSUM ‘!c. c IN f ==> _’ MP_TAC \\
2320 rw [EXT_SKOLEM_THM] \\
2321 rename1 ‘!c. c IN f ==> P (g c) /\ u INTER g c = c’ \\
2322 Q.EXISTS_TAC `INTERS (IMAGE (g:('a->bool)->('a->bool)) f)` THEN
2323 CONJ_TAC THENL [ALL_TAC, ASM_SET_TAC[]] THEN
2324 Q.EXISTS_TAC `IMAGE (g:('a->bool)->('a->bool)) f` THEN
2325 ASM_SIMP_TAC std_ss [FINITE_IMAGE, FORALL_IN_IMAGE] ]
2326QED
2327
2328Theorem COUNTABLE_INTERSECTION_OF_RELATIVE_TO :
2329 !P u:'a->bool.
2330 ((COUNTABLE INTERSECTION_OF P) relative_to u) =
2331 ((COUNTABLE INTERSECTION_OF (P relative_to u)) relative_to u)
2332Proof
2333 REPEAT GEN_TAC THEN GEN_REWRITE_TAC I empty_rewrites [FUN_EQ_THM] THEN
2334 Q.X_GEN_TAC `s:'a->bool` THEN REWRITE_TAC[INTERSECTION_OF, relative_to] THEN
2335 BETA_TAC THEN EQ_TAC THENL
2336 [ (* goal 1 (of 2) *)
2337 DISCH_THEN(Q.X_CHOOSE_THEN `t:'a->bool`
2338 (CONJUNCTS_THEN2 MP_TAC (SUBST1_TAC o SYM))) THEN
2339 DISCH_THEN(Q.X_CHOOSE_THEN `f:('a->bool)->bool`
2340 (STRIP_ASSUME_TAC o GSYM)) THEN
2341 Q.EXISTS_TAC `INTERS {u INTER c | (c:'a->bool) IN f}` THEN CONJ_TAC THENL
2342 [ Q.EXISTS_TAC `{u INTER c | (c:'a->bool) IN f}` THEN
2343 ASM_SIMP_TAC std_ss [COUNTABLE_IMAGE, SIMPLE_IMAGE, FORALL_IN_IMAGE] THEN
2344 ASM_MESON_TAC[],
2345 ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[INTER_INTERS] THEN
2346 ASM_SIMP_TAC std_ss [SIMPLE_IMAGE, IMAGE_EQ_EMPTY, INTERS_IMAGE, FORALL_IN_IMAGE,
2347 SET_RULE ``u INTER (u INTER s) = u INTER s``] ],
2348 DISCH_THEN(Q.X_CHOOSE_THEN `t:'a->bool`
2349 (CONJUNCTS_THEN2 MP_TAC (SUBST1_TAC o SYM))) THEN
2350 DISCH_THEN(Q.X_CHOOSE_THEN `f:('a->bool)->bool` STRIP_ASSUME_TAC) THEN
2351 Q.PAT_X_ASSUM ‘!c. c IN f ==> _’ MP_TAC \\
2352 rw [EXT_SKOLEM_THM] \\
2353 rename1 ‘!c. c IN f ==> P (g c) /\ u INTER g c = c’ \\
2354 Q.EXISTS_TAC `INTERS (IMAGE (g:('a->bool)->('a->bool)) f)` THEN
2355 CONJ_TAC THENL [ALL_TAC, ASM_SET_TAC[]] THEN
2356 Q.EXISTS_TAC `IMAGE (g:('a->bool)->('a->bool)) f` THEN
2357 ASM_SIMP_TAC std_ss [COUNTABLE_IMAGE, FORALL_IN_IMAGE] ]
2358QED
2359
2360Theorem FINITE_INTERSECTION_OF_RELATIVE_TO_ALT :
2361 !P u s:'a->bool.
2362 P u ==> ((FINITE INTERSECTION_OF P relative_to u) s <=>
2363 (FINITE INTERSECTION_OF P) s /\ s SUBSET u)
2364Proof
2365 REPEAT STRIP_TAC THEN EQ_TAC THEN SIMP_TAC std_ss [RELATIVE_TO_SUBSET_INC] THEN
2366 Q.SPEC_TAC(`s:'a->bool`,`s:'a->bool`) THEN
2367 SIMP_TAC std_ss [FORALL_RELATIVE_TO, FORALL_INTERSECTION_OF] THEN
2368 REWRITE_TAC[INTER_SUBSET, GSYM INTERS_INSERT] THEN
2369 REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_INTERSECTION_OF_INTERS THEN
2370 ASM_REWRITE_TAC[FINITE_INSERT, FORALL_IN_INSERT] THEN
2371 ASM_SIMP_TAC std_ss [FINITE_INTERSECTION_OF_INC]
2372QED
2373
2374Theorem COUNTABLE_INTERSECTION_OF_RELATIVE_TO_ALT :
2375 !P u s:'a->bool.
2376 P u ==> ((COUNTABLE INTERSECTION_OF P relative_to u) s <=>
2377 (COUNTABLE INTERSECTION_OF P) s /\ s SUBSET u)
2378Proof
2379 REPEAT STRIP_TAC THEN EQ_TAC THEN SIMP_TAC std_ss [RELATIVE_TO_SUBSET_INC] THEN
2380 Q.SPEC_TAC(`s:'a->bool`,`s:'a->bool`) THEN
2381 SIMP_TAC std_ss [FORALL_RELATIVE_TO, FORALL_INTERSECTION_OF] THEN
2382 REWRITE_TAC[INTER_SUBSET, GSYM INTERS_INSERT] THEN
2383 REPEAT STRIP_TAC THEN MATCH_MP_TAC COUNTABLE_INTERSECTION_OF_INTERS THEN
2384 ASM_REWRITE_TAC[COUNTABLE_INSERT, FORALL_IN_INSERT] THEN
2385 ASM_SIMP_TAC std_ss [COUNTABLE_INTERSECTION_OF_INC]
2386QED
2387
2388Theorem ARBITRARY_UNION_OF_NONEMPTY_FINITE_INTERSECTION :
2389 !u:('a->bool)->bool.
2390 ARBITRARY UNION_OF ((\s. FINITE s /\ ~(s = {})) INTERSECTION_OF u) =
2391 ARBITRARY UNION_OF (FINITE INTERSECTION_OF u relative_to UNIONS u)
2392Proof
2393 GEN_TAC THEN MATCH_MP_TAC SUBSET_ANTISYM THEN
2394 REWRITE_TAC[REWRITE_RULE[IN_APP] SUBSET_DEF] THEN
2395 CONJ_TAC THEN Q.X_GEN_TAC `s:'a->bool` THENL
2396 [ (* goal 1 (of 2) *)
2397 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] UNION_OF_MONO) THEN
2398 REWRITE_TAC[FORALL_INTERSECTION_OF] THEN Q.X_GEN_TAC `t:('a->bool)->bool` THEN
2399 STRIP_TAC THEN REWRITE_TAC[INTERSECTION_OF, relative_to] THEN
2400 Q.EXISTS_TAC `INTERS t:'a->bool` THEN
2401 CONJ_TAC THENL [ASM_MESON_TAC[], ASM_SET_TAC[]],
2402 (* goal 2 (of 2) *)
2403 GEN_REWRITE_TAC (RAND_CONV o RATOR_CONV) empty_rewrites
2404 [GSYM ARBITRARY_UNION_OF_IDEMPOT] THEN
2405 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] UNION_OF_MONO) THEN
2406 SIMP_TAC std_ss [FORALL_RELATIVE_TO, FORALL_INTERSECTION_OF] THEN
2407 Q.X_GEN_TAC `t:('a->bool)->bool` THEN STRIP_TAC THEN
2408 ASM_CASES_TAC ``t:('a->bool)->bool = {}`` THENL
2409 [ (* goal 2.1 (of 2) *)
2410 ASM_REWRITE_TAC[INTERS_0, INTER_UNIV] THEN
2411 MATCH_MP_TAC ARBITRARY_UNION_OF_UNIONS THEN
2412 Q.X_GEN_TAC `r:'a->bool` THEN DISCH_TAC THEN
2413 MATCH_MP_TAC UNION_OF_INC THEN
2414 REWRITE_TAC[ARBITRARY] THEN MATCH_MP_TAC INTERSECTION_OF_INC THEN
2415 REWRITE_TAC[NOT_INSERT_EMPTY, FINITE_SING] THEN
2416 fs [IN_APP],
2417 (* goal 2.2 (of 2) *)
2418 MATCH_MP_TAC UNION_OF_INC THEN
2419 SIMP_TAC std_ss [ARBITRARY, INTERSECTION_OF] THEN
2420 Q.EXISTS_TAC `t:('a->bool)->bool` THEN ASM_SET_TAC[] ] ]
2421QED
2422
2423Theorem OPEN_IN_RELATIVE_TO :
2424 !top s:'a->bool.
2425 (open_in top relative_to s) = open_in (subtopology top s)
2426Proof
2427 REWRITE_TAC[relative_to, OPEN_IN_SUBTOPOLOGY, FUN_EQ_THM] THEN
2428 MESON_TAC[INTER_COMM]
2429QED
2430
2431Theorem CLOSED_IN_RELATIVE_TO :
2432 !top s:'a->bool.
2433 (closed_in top relative_to s) = closed_in (subtopology top s)
2434Proof
2435 REWRITE_TAC[relative_to, CLOSED_IN_SUBTOPOLOGY, FUN_EQ_THM] THEN
2436 MESON_TAC[INTER_COMM]
2437QED
2438
2439(* ------------------------------------------------------------------------- *)
2440(* Continuous maps (ported from HOL-Light's Multivariate/metric.ml) *)
2441(* ------------------------------------------------------------------------- *)
2442
2443Definition continuous_map :
2444 continuous_map (top,top') (f :'a -> 'b) <=>
2445 (!x. x IN topspace top ==> f x IN topspace top') /\
2446 (!u. open_in top' u
2447 ==> open_in top {x | x IN topspace top /\ f x IN u})
2448End
2449
2450Theorem CONTINUOUS_MAP :
2451 !top top' f.
2452 continuous_map (top,top') f <=>
2453 (IMAGE f (topspace top) SUBSET topspace top' /\
2454 !u. open_in top' u
2455 ==> open_in top {x | x IN topspace top /\ f x IN u})
2456Proof
2457 SIMP_TAC std_ss[continuous_map, SUBSET_DEF, FORALL_IN_IMAGE]
2458QED
2459
2460Theorem CONTINUOUS_MAP_IMAGE_SUBSET_TOPSPACE :
2461 !top top' (f :'a->'b). continuous_map (top,top') f
2462 ==> IMAGE f (topspace top) SUBSET topspace top'
2463Proof
2464 SIMP_TAC std_ss[continuous_map] THEN SET_TAC[]
2465QED
2466
2467Theorem CONTINUOUS_MAP_ON_EMPTY :
2468 !top top' (f :'a->'b). topspace top = {} ==> continuous_map(top,top') f
2469Proof
2470 SIMP_TAC std_ss[continuous_map, NOT_IN_EMPTY, EMPTY_GSPEC, OPEN_IN_EMPTY]
2471QED
2472
2473Theorem CONTINUOUS_MAP_INTO_EMPTY :
2474 !top top' (f :'a->'b).
2475 topspace top' = {}
2476 ==> (continuous_map(top,top') f <=> topspace top = {})
2477Proof
2478 REPEAT STRIP_TAC THEN EQ_TAC THEN REWRITE_TAC[CONTINUOUS_MAP_ON_EMPTY] THEN
2479 DISCH_THEN(MP_TAC o MATCH_MP CONTINUOUS_MAP_IMAGE_SUBSET_TOPSPACE) THEN
2480 ASM_SET_TAC[]
2481QED
2482
2483Theorem CONTINUOUS_MAP_CLOSED_IN :
2484 !top top' f:'a->'b.
2485 continuous_map (top,top') f <=>
2486 (!x. x IN topspace top ==> f x IN topspace top') /\
2487 (!c. closed_in top' c
2488 ==> closed_in top {x | x IN topspace top /\ f x IN c})
2489Proof
2490 REPEAT GEN_TAC THEN REWRITE_TAC[continuous_map] THEN
2491 MATCH_MP_TAC(TAUT `(p ==> (q <=> r)) ==> (p /\ q <=> p /\ r)`) THEN
2492 DISCH_TAC THEN EQ_TAC THEN DISCH_TAC THEN
2493 (* 2 subgoals, same tactics *)
2494 X_GEN_TAC “t:'b->bool” THEN DISCH_TAC THEN
2495 FIRST_X_ASSUM(MP_TAC o SPEC “topspace top' DIFF t:'b->bool”) THEN
2496 ASM_SIMP_TAC std_ss[OPEN_IN_DIFF, CLOSED_IN_DIFF, OPEN_IN_TOPSPACE,
2497 CLOSED_IN_TOPSPACE] THEN
2498 GEN_REWRITE_TAC LAND_CONV empty_rewrites[closed_in, OPEN_IN_CLOSED_IN_EQ] THEN
2499 SIMP_TAC std_ss[SUBSET_RESTRICT] THEN MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
2500 ASM_SET_TAC[]
2501QED
2502
2503Theorem OPEN_IN_CONTINUOUS_MAP_PREIMAGE :
2504 !f:'a->'b top top' u.
2505 continuous_map (top,top') f /\ open_in top' u
2506 ==> open_in top {x | x IN topspace top /\ f x IN u}
2507Proof
2508 REWRITE_TAC[continuous_map] THEN SET_TAC[]
2509QED
2510
2511Theorem CLOSED_IN_CONTINUOUS_MAP_PREIMAGE :
2512 !f:'a->'b top top' c.
2513 continuous_map (top,top') f /\ closed_in top' c
2514 ==> closed_in top {x | x IN topspace top /\ f x IN c}
2515Proof
2516 REWRITE_TAC[CONTINUOUS_MAP_CLOSED_IN] THEN SET_TAC[]
2517QED
2518
2519Theorem OPEN_IN_CONTINUOUS_MAP_PREIMAGE_GEN :
2520 !f:'a->'b top top' u v.
2521 continuous_map (top,top') f /\ open_in top u /\ open_in top' v
2522 ==> open_in top {x | x IN u /\ f x IN v}
2523Proof
2524 REPEAT STRIP_TAC THEN
2525 SUBGOAL_THEN “{x | x IN u /\ (f:'a->'b) x IN v} =
2526 u INTER {x | x IN topspace top /\ f x IN v}”
2527 SUBST1_TAC THENL
2528 [ REPEAT(FIRST_X_ASSUM(MP_TAC o MATCH_MP OPEN_IN_SUBSET)) THEN SET_TAC[],
2529 MATCH_MP_TAC OPEN_IN_INTER THEN ASM_REWRITE_TAC[] THEN
2530 MATCH_MP_TAC OPEN_IN_CONTINUOUS_MAP_PREIMAGE THEN
2531 ASM_MESON_TAC[] ]
2532QED
2533
2534Theorem CLOSED_IN_CONTINUOUS_MAP_PREIMAGE_GEN :
2535 !f:'a->'b top top' u v.
2536 continuous_map (top,top') f /\ closed_in top u /\ closed_in top' v
2537 ==> closed_in top {x | x IN u /\ f x IN v}
2538Proof
2539 REPEAT STRIP_TAC THEN
2540 SUBGOAL_THEN “{x | x IN u /\ (f:'a->'b) x IN v} =
2541 u INTER {x | x IN topspace top /\ f x IN v}”
2542 SUBST1_TAC THENL
2543 [ REPEAT(FIRST_X_ASSUM(MP_TAC o MATCH_MP CLOSED_IN_SUBSET)) THEN SET_TAC[],
2544 MATCH_MP_TAC CLOSED_IN_INTER THEN ASM_REWRITE_TAC[] THEN
2545 MATCH_MP_TAC CLOSED_IN_CONTINUOUS_MAP_PREIMAGE THEN
2546 ASM_MESON_TAC[] ]
2547QED
2548
2549Theorem CONTINUOUS_MAP_ID :
2550 !top:'a topology. continuous_map (top,top) (\x. x)
2551Proof
2552 SIMP_TAC std_ss[continuous_map] THEN REPEAT GEN_TAC THEN
2553 MATCH_MP_TAC(MESON[] “(P x ==> x = y) ==> P x ==> P y”) THEN
2554 REWRITE_TAC[SET_RULE “u = {x | x IN s /\ x IN u} <=> u SUBSET s”] THEN
2555 REWRITE_TAC[OPEN_IN_SUBSET]
2556QED
2557
2558Theorem TOPOLOGY_FINER_CONTINUOUS_ID :
2559 !top top':'a topology.
2560 topspace top' = topspace top
2561 ==> ((!s. open_in top s ==> open_in top' s) <=>
2562 continuous_map (top',top) (\x. x))
2563Proof
2564 REWRITE_TAC[continuous_map] THEN
2565 SIMP_TAC std_ss[OPEN_IN_SUBSET, SET_RULE
2566 “u SUBSET s ==> {x | x IN s /\ x IN u} = u”]
2567QED
2568
2569Theorem CONTINUOUS_MAP_CONST :
2570 !(top1:'a topology) (top2:'b topology) c.
2571 continuous_map (top1,top2) (\x. c) <=>
2572 topspace top1 = {} \/ c IN topspace top2
2573Proof
2574 REPEAT GEN_TAC THEN REWRITE_TAC[continuous_map] THEN
2575 ASM_CASES_TAC “topspace top1:'a->bool = {}” THEN
2576 ASM_SIMP_TAC std_ss[NOT_IN_EMPTY, EMPTY_GSPEC, OPEN_IN_EMPTY] THEN
2577 (* one subgoal left *)
2578 ASM_CASES_TAC “(c:'b) IN topspace top2” THEN ASM_REWRITE_TAC[] THENL
2579 [ALL_TAC, ASM_SET_TAC[]] THEN
2580 X_GEN_TAC “u:'b->bool” THEN
2581 ASM_CASES_TAC “(c:'b) IN u” THEN
2582 ASM_SIMP_TAC std_ss[EMPTY_GSPEC, OPEN_IN_EMPTY] THEN
2583 (* one subgoal left *)
2584 REWRITE_TAC[SET_RULE “{x | x IN s} = s”, OPEN_IN_TOPSPACE]
2585QED
2586
2587Theorem CONTINUOUS_MAP_COMPOSE :
2588 !top top' top'' (f:'a->'b) (g:'b->'c).
2589 continuous_map (top,top') f /\ continuous_map (top',top'') g
2590 ==> continuous_map (top,top'') (g o f)
2591Proof
2592 REPEAT GEN_TAC THEN REWRITE_TAC[continuous_map, o_THM] THEN STRIP_TAC THEN
2593 CONJ_TAC THENL [ASM_SET_TAC[], X_GEN_TAC “u:'c->bool”] THEN
2594 SUBGOAL_THEN
2595 “{x:'a | x IN topspace top /\ (g:'b->'c) (f x) IN u} =
2596 {x:'a | x IN topspace top /\ f x IN {y | y IN topspace top' /\ g y IN u}}”
2597 SUBST1_TAC THENL [ASM_SET_TAC[], ASM_SIMP_TAC std_ss[] ]
2598QED
2599
2600(* |- (!x. P x ==> Q x) ==> (!x. P x) ==> !x. Q x *)
2601val MONO_FORALL = MONO_ALL;
2602
2603Theorem CONTINUOUS_MAP_EQ :
2604 !top top' f (g:'a->'b).
2605 (!x. x IN topspace top ==> f x = g x) /\ continuous_map (top,top') f
2606 ==> continuous_map (top,top') g
2607Proof
2608 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
2609 REWRITE_TAC[continuous_map] THEN
2610 MATCH_MP_TAC MONO_AND THEN CONJ_TAC THENL [ASM_SET_TAC[], ALL_TAC] THEN
2611 HO_MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN
2612 MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
2613 ASM_SET_TAC[]
2614QED
2615
2616Theorem RESTRICTION_CONTINUOUS_MAP :
2617 !top top' (f:'a->'b) s.
2618 topspace top SUBSET s
2619 ==> (continuous_map (top,top') (RESTRICTION s f) <=>
2620 continuous_map (top,top') f)
2621Proof
2622 REPEAT GEN_TAC THEN DISCH_TAC THEN EQ_TAC THEN
2623 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] CONTINUOUS_MAP_EQ) THEN
2624 REWRITE_TAC[RESTRICTION] THEN ASM_SET_TAC[]
2625QED
2626
2627Theorem CONTINUOUS_MAP_IN_SUBTOPOLOGY :
2628 !top top' s f:'a->'b.
2629 continuous_map (top,subtopology top' s) f <=>
2630 continuous_map (top,top') f /\ IMAGE f (topspace top) SUBSET s
2631Proof
2632 REPEAT GEN_TAC THEN
2633 REWRITE_TAC[continuous_map, TOPSPACE_SUBTOPOLOGY, IN_INTER,
2634 OPEN_IN_SUBTOPOLOGY] THEN
2635 EQ_TAC THEN SIMP_TAC std_ss[] THENL
2636 [ (* goal 1 (of 2) *)
2637 STRIP_TAC THEN CONJ_TAC THENL [ALL_TAC, ASM_SET_TAC[]] THEN
2638 rpt STRIP_TAC THEN
2639 SUBGOAL_THEN
2640 “{x:'a | x IN topspace top /\ f x:'b IN u} =
2641 {x | x IN topspace top /\ f x IN u INTER s}”
2642 (fn th => REWRITE_TAC[th])
2643 >- (Q.PAT_X_ASSUM ‘!x. x IN topspace top ==> _’ MP_TAC \\
2644 SET_TAC []) \\
2645 FIRST_X_ASSUM MATCH_MP_TAC THEN EXISTS_TAC “u:'b->bool” THEN
2646 ASM_REWRITE_TAC[],
2647 (* goal 2 (of 2) *)
2648 STRIP_TAC THEN
2649 CONJ_TAC THENL [ASM_SET_TAC[], ALL_TAC] THEN
2650 rpt STRIP_TAC THEN
2651 POP_ORW THEN
2652 SUBGOAL_THEN
2653 “{x:'a | x IN topspace top /\ f x:'b IN t INTER s} =
2654 {x | x IN topspace top /\ f x IN t}”
2655 (fn th => ASM_SIMP_TAC std_ss[th]) THEN
2656 ASM_SET_TAC[] ]
2657QED
2658
2659Theorem CONTINUOUS_MAP_FROM_SUBTOPOLOGY :
2660 !top top' (f:'a->'b) s.
2661 continuous_map (top,top') f
2662 ==> continuous_map (subtopology top s,top') f
2663Proof
2664 SIMP_TAC std_ss[continuous_map, TOPSPACE_SUBTOPOLOGY, IN_INTER] THEN
2665 REPEAT GEN_TAC THEN STRIP_TAC THEN X_GEN_TAC “u:'b->bool” THEN
2666 REPEAT STRIP_TAC THEN REWRITE_TAC[OPEN_IN_SUBTOPOLOGY] THEN
2667 EXISTS_TAC “{x | x IN topspace top /\ (f:'a->'b) x IN u}” THEN
2668 ASM_SIMP_TAC std_ss[] THEN SET_TAC[]
2669QED
2670
2671Theorem CONTINUOUS_MAP_INTO_FULLTOPOLOGY :
2672 !top top' (f:'a->'b) t.
2673 continuous_map (top,subtopology top' t) f
2674 ==> continuous_map (top,top') f
2675Proof
2676 SIMP_TAC std_ss[CONTINUOUS_MAP_IN_SUBTOPOLOGY]
2677QED
2678
2679Theorem CONTINUOUS_MAP_INTO_SUBTOPOLOGY :
2680 !top top' (f:'a->'b) t.
2681 continuous_map (top,top') f /\
2682 IMAGE f (topspace top) SUBSET t
2683 ==> continuous_map (top,subtopology top' t) f
2684Proof
2685 SIMP_TAC std_ss[CONTINUOUS_MAP_IN_SUBTOPOLOGY]
2686QED
2687
2688Theorem CONTINUOUS_MAP_FROM_SUBTOPOLOGY_MONO :
2689 !top top' f s t.
2690 continuous_map (subtopology top t,top') f /\ s SUBSET t
2691 ==> continuous_map (subtopology top s,top') f
2692Proof
2693 MESON_TAC[CONTINUOUS_MAP_FROM_SUBTOPOLOGY, SUBTOPOLOGY_SUBTOPOLOGY,
2694 SET_RULE “s SUBSET t ==> t INTER s = s”]
2695QED
2696
2697(* ------------------------------------------------------------------------- *)
2698(* Pointwise continuity in topological spaces. *)
2699(* (ported from HOL-Light's Multivariate/metric.ml) *)
2700(* ------------------------------------------------------------------------- *)
2701
2702Definition topcontinuous_at :
2703 topcontinuous_at top top' (f :'a -> 'b) x <=>
2704 x IN topspace top /\
2705 (!x. x IN topspace top ==> f x IN topspace top') /\
2706 (!v. open_in top' v /\ f x IN v
2707 ==> (?u. open_in top u /\ x IN u /\ (!y. y IN u ==> f y IN v)))
2708End
2709
2710Theorem OPEN_IN_SUBSET_TOPSPACE :
2711 !top s. open_in top s ==> s SUBSET topspace top
2712Proof
2713 rw [SUBSET_DEF, topspace]
2714 >> Q.EXISTS_TAC ‘s’ >> art []
2715QED
2716
2717(*
2718Theorem TOPCONTINUOUS_AT_ATPOINTOF :
2719 !top top' (f:'a->'b) x.
2720 topcontinuous_at top top' f x <=>
2721 x IN topspace top /\
2722 (!x. x IN topspace top ==> f x IN topspace top') /\
2723 limit top' f (f x) (atpointof top x)`,
2724 REPEAT GEN_TAC THEN REWRITE_TAC[topcontinuous_at] THEN
2725 MATCH_MP_TAC(TAUT
2726 `(p /\ q ==> (r <=> s)) ==> (p /\ q /\ r <=> p /\ q /\ s)`) THEN
2727 STRIP_TAC THEN ASM_SIMP_TAC[LIMIT_ATPOINTOF] THEN
2728 AP_TERM_TAC THEN ABS_TAC THEN SET_TAC[]);;
2729 *)
2730
2731Theorem CONTINUOUS_MAP_EQ_TOPCONTINUOUS_AT :
2732 !top top' f.
2733 continuous_map (top,top') f <=>
2734 !x. x IN topspace top ==> topcontinuous_at top top' f x
2735Proof
2736 rw [continuous_map, topcontinuous_at]
2737 >> reverse EQ_TAC >> rw [] (* 3 subgoals *)
2738 >- (Q.PAT_X_ASSUM ‘!x. x IN topspace top ==> _’ (MP_TAC o Q.SPEC ‘x’) >> rw [])
2739 >- (rw [OPEN_NEIGH] \\
2740 Q.PAT_X_ASSUM ‘!x. x IN topspace top ==> _’ (MP_TAC o Q.SPEC ‘x’) >> rw [] \\
2741 POP_ASSUM (MP_TAC o Q.SPEC ‘u’) >> rw [] \\
2742 rename1 ‘x IN N’ \\
2743 Q.EXISTS_TAC ‘N’ \\
2744 ‘N SUBSET topspace top’ by PROVE_TAC [OPEN_IN_SUBSET_TOPSPACE] \\
2745 reverse CONJ_TAC
2746 >- (POP_ASSUM MP_TAC >> rw [SUBSET_DEF]) \\
2747 rw [neigh] \\
2748 Q.EXISTS_TAC ‘N’ >> fs [IN_APP])
2749 >> Q.PAT_X_ASSUM ‘!u. open_in top' u ==> _’ (MP_TAC o Q.SPEC ‘v’) >> rw []
2750 >> Q.EXISTS_TAC ‘{x | x IN topspace top /\ f x IN v}’ >> rw []
2751QED
2752
2753(* ------------------------------------------------------------------------- *)
2754(* Derived set (set of limit points). *)
2755(* (ported from HOL-Light's Multivariate/metric.ml) *)
2756(* ------------------------------------------------------------------------- *)
2757
2758(* parse_as_infix("derived_set_of",(21,"right"));; *)
2759val _ = set_fixity "derived_set_of" (Infixr 602);
2760
2761Definition derived_set_of :
2762 top derived_set_of s =
2763 {(x :'a) | x IN topspace top /\
2764 !t. x IN t /\ open_in top t ==>
2765 ?y. ~(y = x) /\ y IN s /\ y IN t}
2766End
2767
2768Theorem DERIVED_SET_OF_RESTRICT :
2769 !top (s :'a set).
2770 top derived_set_of s = top derived_set_of (topspace top INTER s)
2771Proof
2772 rw [derived_set_of, Once EXTENSION] THEN
2773 MESON_TAC[REWRITE_RULE[SUBSET_DEF] OPEN_IN_SUBSET]
2774QED
2775
2776Theorem IN_DERIVED_SET_OF :
2777 !top s (x :'a).
2778 x IN top derived_set_of s <=>
2779 x IN topspace top /\
2780 (!t. x IN t /\ open_in top t ==> ?y. ~(y = x) /\ y IN s /\ y IN t)
2781Proof
2782 rw [derived_set_of]
2783QED
2784
2785Theorem DERIVED_SET_OF_SUBSET_TOPSPACE :
2786 !top (s :'a set). top derived_set_of s SUBSET topspace top
2787Proof
2788 REWRITE_TAC[derived_set_of] THEN SET_TAC[]
2789QED
2790
2791Theorem DERIVED_SET_OF_SUBTOPOLOGY :
2792 !top u (s :'a set).
2793 (subtopology top u) derived_set_of s =
2794 u INTER top derived_set_of (u INTER s)
2795Proof
2796 REPEAT GEN_TAC THEN GEN_REWRITE_TAC I empty_rewrites[EXTENSION] THEN
2797 REWRITE_TAC[derived_set_of, OPEN_IN_SUBTOPOLOGY, TOPSPACE_SUBTOPOLOGY] THEN
2798 simp[RIGHT_AND_EXISTS_THM, LEFT_IMP_EXISTS_THM] THEN
2799 ASM_SET_TAC[]
2800QED
2801
2802Theorem DERIVED_SET_OF_SUBSET_SUBTOPOLOGY :
2803 !top s (t :'a set). (subtopology top s) derived_set_of t SUBSET s
2804Proof
2805 SIMP_TAC std_ss[DERIVED_SET_OF_SUBTOPOLOGY, INTER_SUBSET]
2806QED
2807
2808Theorem DERIVED_SET_OF_EMPTY :
2809 !(top:'a topology). top derived_set_of {} = {}
2810Proof
2811 REWRITE_TAC[EXTENSION, IN_DERIVED_SET_OF, NOT_IN_EMPTY] THEN
2812 MESON_TAC[OPEN_IN_TOPSPACE]
2813QED
2814
2815Theorem DERIVED_SET_OF_MONO :
2816 !top s (t :'a set).
2817 s SUBSET t ==> top derived_set_of s SUBSET top derived_set_of t
2818Proof
2819 REWRITE_TAC[derived_set_of] THEN SET_TAC[]
2820QED
2821
2822Theorem DERIVED_SET_OF_UNION :
2823 !top s (t :'a set).
2824 top derived_set_of (s UNION t) =
2825 top derived_set_of s UNION top derived_set_of t
2826Proof
2827 REPEAT GEN_TAC THEN
2828 SIMP_TAC std_ss[GSYM SUBSET_ANTISYM_EQ, UNION_SUBSET, DERIVED_SET_OF_MONO,
2829 SUBSET_UNION] THEN
2830 REWRITE_TAC[SUBSET_DEF, IN_DERIVED_SET_OF, IN_UNION] THEN
2831 X_GEN_TAC “x :'a” THEN
2832 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
2833 ASM_REWRITE_TAC[] THEN GEN_REWRITE_TAC I empty_rewrites[GSYM CONTRAPOS_THM] THEN
2834 SIMP_TAC std_ss[DE_MORGAN_THM, NOT_FORALL_THM, NOT_IMP] THEN
2835 DISCH_THEN(CONJUNCTS_THEN2
2836 (X_CHOOSE_TAC “u :'a set”) (X_CHOOSE_TAC “v :'a set”)) THEN
2837 EXISTS_TAC “u INTER (v :'a set)” THEN
2838 ASM_SIMP_TAC std_ss[OPEN_IN_INTER, IN_INTER] THEN ASM_MESON_TAC[]
2839QED
2840
2841Theorem DERIVED_SET_OF_UNIONS :
2842 !top (f :('a set) set).
2843 FINITE f
2844 ==> top derived_set_of (UNIONS f) =
2845 UNIONS {top derived_set_of s | s IN f}
2846Proof
2847 GEN_TAC THEN HO_MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
2848 SIMP_TAC std_ss[UNIONS_0, NOT_IN_EMPTY, UNIONS_INSERT, DERIVED_SET_OF_EMPTY,
2849 DERIVED_SET_OF_UNION, SIMPLE_IMAGE, IMAGE_CLAUSES]
2850QED
2851
2852Theorem DERIVED_SET_OF_TOPSPACE :
2853 !(top :'a topology).
2854 top derived_set_of (topspace top) =
2855 {x | x IN topspace top /\ ~open_in top {x}}
2856Proof
2857 GEN_TAC THEN simp[EXTENSION, derived_set_of] THEN
2858 X_GEN_TAC “a :'a” THEN ASM_CASES_TAC “(a :'a) IN topspace top” THEN
2859 ASM_REWRITE_TAC[] THEN EQ_TAC THEN DISCH_TAC THENL
2860 [DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC “{a :'a}”) THEN ASM_SET_TAC[],
2861 X_GEN_TAC “u :'a set” THEN STRIP_TAC THEN
2862 ASM_CASES_TAC “u = {a :'a}” THENL [ASM_MESON_TAC[], ALL_TAC] THEN
2863 FIRST_ASSUM(MP_TAC o MATCH_MP OPEN_IN_SUBSET) THEN ASM_SET_TAC[]]
2864QED
2865
2866Theorem OPEN_IN_INTER_DERIVED_SET_OF_SUBSET :
2867 !top s (t :'a set).
2868 open_in top s
2869 ==> s INTER top derived_set_of t SUBSET top derived_set_of (s INTER t)
2870Proof
2871 REPEAT STRIP_TAC THEN REWRITE_TAC[derived_set_of] THEN
2872 simp [SUBSET_DEF, IN_INTER] THEN
2873 X_GEN_TAC “x :'a” THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
2874 X_GEN_TAC “u :'a set” THEN STRIP_TAC THEN
2875 FIRST_X_ASSUM(MP_TAC o SPEC “s INTER (u :'a set)”) THEN
2876 ASM_SIMP_TAC std_ss[OPEN_IN_INTER, IN_INTER] THEN MESON_TAC[]
2877QED
2878
2879Theorem OPEN_IN_INTER_DERIVED_SET_OF_EQ :
2880 !top s (t :'a set).
2881 open_in top s
2882 ==> s INTER top derived_set_of t =
2883 s INTER top derived_set_of (s INTER t)
2884Proof
2885 SIMP_TAC std_ss[GSYM SUBSET_ANTISYM_EQ, INTER_SUBSET, SUBSET_INTER] THEN
2886 SIMP_TAC std_ss[OPEN_IN_INTER_DERIVED_SET_OF_SUBSET] THEN REPEAT STRIP_TAC THEN
2887 MATCH_MP_TAC(SET_RULE “s SUBSET t ==> u INTER s SUBSET t”) THEN
2888 MATCH_MP_TAC DERIVED_SET_OF_MONO THEN SET_TAC[]
2889QED
2890
2891(* ------------------------------------------------------------------------- *)
2892(* Closure with respect to a topological space. *)
2893(* (ported from HOL-Light's Multivariate/metric.ml) *)
2894(* ------------------------------------------------------------------------- *)
2895
2896(* parse_as_infix("closure_of",(21,"right"));; *)
2897val _ = set_fixity "closure_of" (Infixr 602);
2898
2899Definition closure_of :
2900 top closure_of s =
2901 {(x :'a) | x IN topspace top /\
2902 !t. x IN t /\ open_in top t ==> ?y. y IN s /\ y IN t}
2903End
2904
2905Theorem CLOSURE_OF_RESTRICT :
2906 !top (s:'a->bool). top closure_of s = top closure_of (topspace top INTER s)
2907Proof
2908 rw [closure_of, Once EXTENSION, IN_INTER]
2909 >> MESON_TAC[REWRITE_RULE[SUBSET_DEF] OPEN_IN_SUBSET]
2910QED
2911
2912Theorem IN_CLOSURE_OF :
2913 !top s (x :'a).
2914 x IN top closure_of s <=>
2915 x IN topspace top /\
2916 (!t. x IN t /\ open_in top t ==> ?y. y IN s /\ y IN t)
2917Proof
2918 rw [closure_of]
2919QED
2920
2921Theorem CLOSURE_OF :
2922 !top (s :'a set).
2923 top closure_of s =
2924 topspace top INTER (s UNION top derived_set_of s)
2925Proof
2926 REPEAT GEN_TAC THEN REWRITE_TAC[EXTENSION] THEN
2927 Q.X_GEN_TAC ‘x’ THEN
2928 REWRITE_TAC[IN_CLOSURE_OF, IN_DERIVED_SET_OF, IN_UNION, IN_INTER] THEN
2929 Cases_on ‘x IN topspace top’ THEN ASM_REWRITE_TAC[] THEN
2930 MESON_TAC[]
2931QED
2932
2933Theorem CLOSURE_OF_ALT :
2934 !top (s :'a set).
2935 top closure_of s = topspace top INTER s UNION top derived_set_of s
2936Proof
2937 REPEAT GEN_TAC THEN REWRITE_TAC[CLOSURE_OF] THEN
2938 MP_TAC(Q.SPECL [`top`, `s`] DERIVED_SET_OF_SUBSET_TOPSPACE) THEN
2939 SET_TAC[]
2940QED
2941
2942Theorem DERIVED_SET_OF_SUBSET_CLOSURE_OF :
2943 !top (s :'a set). top derived_set_of s SUBSET top closure_of s
2944Proof
2945 REWRITE_TAC[CLOSURE_OF, SUBSET_INTER, DERIVED_SET_OF_SUBSET_TOPSPACE] THEN
2946 SIMP_TAC std_ss[SUBSET_UNION]
2947QED
2948
2949Theorem CLOSURE_OF_SUBTOPOLOGY :
2950 !top u (s :'a set).
2951 (subtopology top u) closure_of s = u INTER (top closure_of (u INTER s))
2952Proof
2953 SIMP_TAC std_ss[CLOSURE_OF, TOPSPACE_SUBTOPOLOGY, DERIVED_SET_OF_SUBTOPOLOGY] THEN
2954 SET_TAC[]
2955QED
2956
2957Theorem CLOSURE_OF_EMPTY :
2958 !top. top closure_of ({} :'a set) = {}
2959Proof
2960 REWRITE_TAC[EXTENSION, IN_CLOSURE_OF, NOT_IN_EMPTY] THEN
2961 MESON_TAC[OPEN_IN_TOPSPACE]
2962QED
2963
2964Theorem CLOSURE_OF_TOPSPACE :
2965 !(top :'a topology). top closure_of topspace top = topspace top
2966Proof
2967 REWRITE_TAC[EXTENSION, IN_CLOSURE_OF] THEN MESON_TAC[]
2968QED
2969
2970Theorem CLOSURE_OF_UNIV :
2971 !top. top closure_of UNIV = topspace top
2972Proof
2973 REWRITE_TAC[closure_of] THEN SET_TAC[]
2974QED
2975
2976Theorem CLOSURE_OF_SUBSET_TOPSPACE :
2977 !top (s :'a set). top closure_of s SUBSET topspace top
2978Proof
2979 REWRITE_TAC[closure_of] THEN SET_TAC[]
2980QED
2981
2982Theorem CLOSURE_OF_SUBSET_SUBTOPOLOGY :
2983 !top s (t :'a set). (subtopology top s) closure_of t SUBSET s
2984Proof
2985 REWRITE_TAC[TOPSPACE_SUBTOPOLOGY, closure_of] THEN SET_TAC[]
2986QED
2987
2988Theorem CLOSURE_OF_MONO :
2989 !top s (t :'a set).
2990 s SUBSET t ==> top closure_of s SUBSET top closure_of t
2991Proof
2992 REWRITE_TAC[closure_of] THEN SET_TAC[]
2993QED
2994
2995Theorem CLOSURE_OF_SUBTOPOLOGY_SUBSET :
2996 !top s (u :'a set).
2997 (subtopology top u) closure_of s SUBSET (top closure_of s)
2998Proof
2999 REPEAT GEN_TAC THEN REWRITE_TAC[CLOSURE_OF_SUBTOPOLOGY] THEN
3000 MATCH_MP_TAC(SET_RULE “t SUBSET u ==> s INTER t SUBSET u”) THEN
3001 MATCH_MP_TAC CLOSURE_OF_MONO THEN REWRITE_TAC[INTER_SUBSET]
3002QED
3003
3004Theorem CLOSURE_OF_SUBTOPOLOGY_MONO :
3005 !top s t (u :'a set).
3006 t SUBSET u
3007 ==> (subtopology top t) closure_of s SUBSET
3008 (subtopology top u) closure_of s
3009Proof
3010 REPEAT STRIP_TAC THEN REWRITE_TAC[CLOSURE_OF_SUBTOPOLOGY] THEN
3011 MATCH_MP_TAC(SET_RULE
3012 “s SUBSET s' /\ t SUBSET t' ==> s INTER t SUBSET s' INTER t'”) THEN
3013 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC CLOSURE_OF_MONO THEN
3014 ASM_SET_TAC[]
3015QED
3016
3017Theorem CLOSURE_OF_UNION :
3018 !top s (t :'a set).
3019 top closure_of (s UNION t) = top closure_of s UNION top closure_of t
3020Proof
3021 REWRITE_TAC[CLOSURE_OF, DERIVED_SET_OF_UNION] THEN SET_TAC[]
3022QED
3023
3024Theorem CLOSURE_OF_UNIONS :
3025 !top (f :('a set) set).
3026 FINITE f
3027 ==> top closure_of (UNIONS f) = UNIONS {top closure_of s | s IN f}
3028Proof
3029 GEN_TAC THEN HO_MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
3030 SIMP_TAC std_ss[UNIONS_0, NOT_IN_EMPTY, UNIONS_INSERT, CLOSURE_OF_EMPTY,
3031 CLOSURE_OF_UNION, SIMPLE_IMAGE, IMAGE_CLAUSES]
3032QED
3033
3034Theorem CLOSURE_OF_SUBSET :
3035 !top (s :'a set). s SUBSET topspace top ==> s SUBSET top closure_of s
3036Proof
3037 REWRITE_TAC[CLOSURE_OF] THEN SET_TAC[]
3038QED
3039
3040Theorem CLOSURE_OF_SUBSET_INTER :
3041 !top (s :'a set). topspace top INTER s SUBSET top closure_of s
3042Proof
3043 REWRITE_TAC[CLOSURE_OF] THEN SET_TAC[]
3044QED
3045
3046Theorem CLOSURE_OF_SUBSET_EQ :
3047 !top (s :'a set).
3048 s SUBSET topspace top /\ top closure_of s SUBSET s <=> closed_in top s
3049Proof
3050 REPEAT GEN_TAC THEN ASM_CASES_TAC “s :'a set SUBSET topspace top” THEN
3051 simp[closed_in, SUBSET_DEF, closure_of] THEN
3052 GEN_REWRITE_TAC RAND_CONV empty_rewrites[OPEN_IN_SUBOPEN] THEN
3053 MP_TAC(ISPEC “top :'a topology” OPEN_IN_SUBSET) THEN ASM_SET_TAC[]
3054QED
3055
3056Theorem CLOSURE_OF_EQ :
3057 !top (s :'a set). top closure_of s = s <=> closed_in top s
3058Proof
3059 REPEAT GEN_TAC THEN
3060 ASM_CASES_TAC “(s :'a set) SUBSET topspace top” THENL
3061 [ASM_MESON_TAC[SUBSET_ANTISYM_EQ, CLOSURE_OF_SUBSET, CLOSURE_OF_SUBSET_EQ],
3062 ASM_MESON_TAC[CLOSED_IN_SUBSET, CLOSURE_OF_SUBSET_TOPSPACE]]
3063QED
3064
3065Theorem CLOSED_IN_CONTAINS_DERIVED_SET :
3066 !top (s :'a set).
3067 closed_in top s <=>
3068 top derived_set_of s SUBSET s /\ s SUBSET topspace top
3069Proof
3070 REPEAT GEN_TAC THEN REWRITE_TAC[GSYM CLOSURE_OF_SUBSET_EQ, CLOSURE_OF] THEN
3071 MP_TAC(ISPECL [“top :'a topology”, “s :'a set”]
3072 DERIVED_SET_OF_SUBSET_TOPSPACE) THEN
3073 SET_TAC[]
3074QED
3075
3076Theorem DERIVED_SET_SUBSET_GEN :
3077 !top (s :'a set).
3078 top derived_set_of s SUBSET s <=>
3079 closed_in top (topspace top INTER s)
3080Proof
3081 REWRITE_TAC[CLOSED_IN_CONTAINS_DERIVED_SET, INTER_SUBSET] THEN
3082 REWRITE_TAC[GSYM DERIVED_SET_OF_RESTRICT, SUBSET_INTER] THEN
3083 REWRITE_TAC[DERIVED_SET_OF_SUBSET_TOPSPACE]
3084QED
3085
3086Theorem DERIVED_SET_SUBSET :
3087 !top (s :'a set).
3088 s SUBSET topspace top
3089 ==> (top derived_set_of s SUBSET s <=> closed_in top s)
3090Proof
3091 SIMP_TAC std_ss[CLOSED_IN_CONTAINS_DERIVED_SET]
3092QED
3093
3094Theorem CLOSED_IN_DERIVED_SET :
3095 !top s (t :'a set).
3096 closed_in (subtopology top t) s <=>
3097 s SUBSET topspace top /\ s SUBSET t /\
3098 !x. x IN top derived_set_of s /\ x IN t ==> x IN s
3099Proof
3100 REPEAT GEN_TAC THEN REWRITE_TAC[CLOSED_IN_CONTAINS_DERIVED_SET] THEN
3101 REWRITE_TAC[TOPSPACE_SUBTOPOLOGY, SUBSET_INTER] THEN
3102 REWRITE_TAC[DERIVED_SET_OF_SUBTOPOLOGY] THEN
3103 ASM_CASES_TAC “t INTER (s :'a set) = s” THEN ASM_REWRITE_TAC[] THEN
3104 ASM_SET_TAC[]
3105QED
3106
3107Theorem CLOSED_IN_INTER_CLOSURE_OF :
3108 !top s (t :'a set).
3109 closed_in (subtopology top s) t <=> s INTER top closure_of t = t
3110Proof
3111 REPEAT GEN_TAC THEN REWRITE_TAC[CLOSURE_OF, CLOSED_IN_DERIVED_SET] THEN
3112 MP_TAC(ISPECL [“top :'a topology”, “t :'a set”]
3113 DERIVED_SET_OF_SUBSET_TOPSPACE) THEN
3114 SET_TAC[]
3115QED
3116
3117Theorem CLOSURE_OF_CLOSED_IN :
3118 !top (s :'a set). closed_in top s ==> top closure_of s = s
3119Proof
3120 REWRITE_TAC[CLOSURE_OF_EQ]
3121QED
3122
3123Theorem CLOSED_IN_CLOSURE_OF :
3124 !top (s :'a set). closed_in top (top closure_of s)
3125Proof
3126 REPEAT GEN_TAC THEN
3127 Q.SUBGOAL_THEN
3128 `top closure_of s =
3129 topspace top DIFF
3130 UNIONS {t | open_in top t /\ DISJOINT s t}`
3131 SUBST1_TAC THENL
3132 [ REWRITE_TAC[closure_of, UNIONS_GSPEC] THEN SET_TAC[],
3133 MATCH_MP_TAC CLOSED_IN_DIFF THEN REWRITE_TAC[CLOSED_IN_TOPSPACE] THEN
3134 SIMP_TAC std_ss[OPEN_IN_UNIONS, FORALL_IN_GSPEC] ]
3135QED
3136
3137Theorem CLOSURE_OF_CLOSURE_OF :
3138 !top (s :'a set). top closure_of (top closure_of s) = top closure_of s
3139Proof
3140 REWRITE_TAC[CLOSURE_OF_EQ, CLOSED_IN_CLOSURE_OF]
3141QED
3142
3143Theorem CLOSURE_OF_HULL :
3144 !top (s :'a set).
3145 s SUBSET topspace top ==> top closure_of s = (closed_in top) hull s
3146Proof
3147 REPEAT STRIP_TAC THEN CONV_TAC SYM_CONV THEN MATCH_MP_TAC HULL_UNIQUE THEN
3148 ASM_SIMP_TAC std_ss[CLOSURE_OF_SUBSET, CLOSED_IN_CLOSURE_OF] THEN
3149 ASM_MESON_TAC[CLOSURE_OF_EQ, CLOSURE_OF_MONO]
3150QED
3151
3152Theorem CLOSURE_OF_MINIMAL :
3153 !top s (t :'a set).
3154 s SUBSET t /\ closed_in top t ==> (top closure_of s) SUBSET t
3155Proof
3156 ASM_MESON_TAC[CLOSURE_OF_EQ, CLOSURE_OF_MONO]
3157QED
3158
3159Theorem CLOSURE_OF_MINIMAL_EQ :
3160 !top s (t :'a set).
3161 s SUBSET topspace top /\ closed_in top t
3162 ==> ((top closure_of s) SUBSET t <=> s SUBSET t)
3163Proof
3164 MESON_TAC[SUBSET_TRANS, CLOSURE_OF_SUBSET, CLOSURE_OF_MINIMAL]
3165QED
3166
3167Theorem CLOSURE_OF_UNIQUE :
3168 !top s t. s SUBSET t /\ closed_in top t /\
3169 (!t'. s SUBSET t' /\ closed_in top t' ==> t SUBSET t')
3170 ==> top closure_of s = t
3171Proof
3172 REPEAT STRIP_TAC THEN
3173 W(MP_TAC o PART_MATCH (lhand o rand) CLOSURE_OF_HULL o lhand o snd) THEN
3174 ANTS_TAC THENL
3175 [ASM_MESON_TAC[CLOSED_IN_SUBSET, SUBSET_TRANS],
3176 DISCH_THEN SUBST1_TAC] THEN
3177 MATCH_MP_TAC HULL_UNIQUE THEN ASM_REWRITE_TAC[]
3178QED
3179
3180Theorem FORALL_IN_CLOSURE_OF_GEN :
3181 !top P (s :'a set).
3182 (!x. x IN s ==> P x) /\
3183 closed_in top {x | x IN top closure_of s /\ P x}
3184 ==> (!x. x IN top closure_of s ==> P x)
3185Proof
3186 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[CLOSURE_OF_RESTRICT] THEN
3187 STRIP_TAC THEN
3188 REWRITE_TAC[SET_RULE
3189 “(!x. x IN s ==> P x) <=> s SUBSET {x | x IN s /\ P x}”] THEN
3190 MATCH_MP_TAC CLOSURE_OF_MINIMAL THEN ASM_REWRITE_TAC[] THEN
3191 MP_TAC(ISPECL [“top :'a topology”, “topspace top INTER (s :'a set)”]
3192 CLOSURE_OF_SUBSET) THEN
3193 ASM_SET_TAC[]
3194QED
3195
3196Theorem FORALL_IN_CLOSURE_OF :
3197 !top P (s :'a set).
3198 (!x. x IN s ==> P x) /\
3199 closed_in top {x | x IN topspace top /\ P x}
3200 ==> (!x. x IN top closure_of s ==> P x)
3201Proof
3202 REPEAT GEN_TAC THEN STRIP_TAC THEN
3203 MATCH_MP_TAC FORALL_IN_CLOSURE_OF_GEN THEN ASM_REWRITE_TAC[] THEN
3204 SUBGOAL_THEN “{x:'a | x IN top closure_of s /\ P x} =
3205 top closure_of s INTER {x | x IN topspace top /\ P x}”
3206 (fn th => ASM_SIMP_TAC std_ss[th, CLOSED_IN_INTER, CLOSED_IN_CLOSURE_OF]) THEN
3207 MP_TAC(ISPECL [“top :'a topology”, “s :'a set”] CLOSURE_OF_SUBSET_TOPSPACE) THEN
3208 SET_TAC[]
3209QED
3210
3211Theorem FORALL_IN_CLOSURE_OF_UNIV :
3212 !top P (s :'a set).
3213 (!x. x IN s ==> P x) /\ closed_in top {x | P x}
3214 ==> !x. x IN top closure_of s ==> P x
3215Proof
3216 REWRITE_TAC[SET_RULE “(!x. x IN s ==> P x) <=> s SUBSET {x | P x}”] THEN
3217 SIMP_TAC std_ss[CLOSURE_OF_MINIMAL]
3218QED
3219
3220Theorem CLOSURE_OF_EQ_EMPTY_GEN :
3221 !top (s :'a set).
3222 top closure_of s = {} <=> DISJOINT (topspace top) s
3223Proof
3224 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[CLOSURE_OF_RESTRICT, DISJOINT_DEF] THEN
3225 EQ_TAC THEN SIMP_TAC std_ss[CLOSURE_OF_EMPTY] THEN
3226 MATCH_MP_TAC(SET_RULE “t SUBSET s ==> s = {} ==> t = {}”) THEN
3227 MATCH_MP_TAC CLOSURE_OF_SUBSET THEN REWRITE_TAC[INTER_SUBSET]
3228QED
3229
3230Theorem CLOSURE_OF_EQ_EMPTY :
3231 !top (s :'a set).
3232 s SUBSET topspace top ==> (top closure_of s = {} <=> s = {})
3233Proof
3234 REWRITE_TAC[CLOSURE_OF_EQ_EMPTY_GEN] THEN SET_TAC[]
3235QED
3236
3237Theorem OPEN_IN_INTER_CLOSURE_OF_SUBSET :
3238 !top s (t :'a set).
3239 open_in top s
3240 ==> s INTER top closure_of t SUBSET top closure_of (s INTER t)
3241Proof
3242 REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o SPEC “t :'a set” o MATCH_MP
3243 OPEN_IN_INTER_DERIVED_SET_OF_SUBSET) THEN
3244 REWRITE_TAC[CLOSURE_OF] THEN SET_TAC[]
3245QED
3246
3247Theorem CLOSURE_OF_OPEN_IN_INTER_CLOSURE_OF :
3248 !top s (t :'a set).
3249 open_in top s
3250 ==> top closure_of (s INTER top closure_of t) =
3251 top closure_of (s INTER t)
3252Proof
3253 REPEAT STRIP_TAC THEN MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL
3254 [MATCH_MP_TAC CLOSURE_OF_MINIMAL THEN
3255 REWRITE_TAC[CLOSED_IN_CLOSURE_OF] THEN
3256 ASM_SIMP_TAC std_ss[OPEN_IN_INTER_CLOSURE_OF_SUBSET],
3257 MATCH_MP_TAC CLOSURE_OF_MONO THEN
3258 MP_TAC(ISPECL [“top :'a topology”, “topspace top INTER (t :'a set)”]
3259 CLOSURE_OF_SUBSET) THEN
3260 REWRITE_TAC[INTER_SUBSET, GSYM CLOSURE_OF_RESTRICT] THEN
3261 FIRST_ASSUM(MP_TAC o MATCH_MP OPEN_IN_SUBSET) THEN
3262 SET_TAC[]]
3263QED
3264
3265Theorem OPEN_IN_INTER_CLOSURE_OF_EQ :
3266 !top s (t :'a set).
3267 open_in top s
3268 ==> s INTER top closure_of t = s INTER top closure_of (s INTER t)
3269Proof
3270 SIMP_TAC std_ss[GSYM SUBSET_ANTISYM_EQ, INTER_SUBSET, SUBSET_INTER] THEN
3271 SIMP_TAC std_ss[OPEN_IN_INTER_CLOSURE_OF_SUBSET] THEN REPEAT STRIP_TAC THEN
3272 MATCH_MP_TAC(SET_RULE “s SUBSET t ==> u INTER s SUBSET t”) THEN
3273 MATCH_MP_TAC CLOSURE_OF_MONO THEN SET_TAC[]
3274QED
3275
3276Theorem OPEN_IN_INTER_CLOSURE_OF_EQ_EMPTY :
3277 !top s (t :'a set).
3278 open_in top s ==> (s INTER top closure_of t = {} <=> s INTER t = {})
3279Proof
3280 REPEAT STRIP_TAC THEN
3281 FIRST_ASSUM(SUBST1_TAC o SPEC “t :'a set” o
3282 MATCH_MP OPEN_IN_INTER_CLOSURE_OF_EQ) THEN
3283 EQ_TAC THEN SIMP_TAC std_ss[CLOSURE_OF_EMPTY, INTER_EMPTY] THEN
3284 MATCH_MP_TAC(SET_RULE
3285 “s INTER t SUBSET c ==> s INTER c = {} ==> s INTER t = {}”) THEN
3286 MATCH_MP_TAC CLOSURE_OF_SUBSET THEN
3287 FIRST_ASSUM(MP_TAC o MATCH_MP OPEN_IN_SUBSET) THEN SET_TAC[]
3288QED
3289
3290Theorem CLOSURE_OF_OPEN_IN_INTER_SUPERSET :
3291 !top s (t :'a set).
3292 open_in top s /\ s SUBSET top closure_of t
3293 ==> top closure_of (s INTER t) = top closure_of s
3294Proof
3295 REPEAT STRIP_TAC THEN
3296 FIRST_ASSUM(SUBST1_TAC o SYM o SPEC “t :'a set” o
3297 MATCH_MP CLOSURE_OF_OPEN_IN_INTER_CLOSURE_OF) THEN
3298 AP_TERM_TAC THEN ASM_SET_TAC[]
3299QED
3300
3301Theorem CLOSURE_OF_OPEN_IN_SUBTOPOLOGY_INTER_CLOSURE_OF :
3302 !top s t (u :'a set).
3303 open_in (subtopology top u) s /\ t SUBSET u
3304 ==> top closure_of (s INTER top closure_of t) =
3305 top closure_of (s INTER t)
3306Proof
3307 REPEAT STRIP_TAC THEN MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL
3308 [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I empty_rewrites[OPEN_IN_SUBTOPOLOGY]) THEN
3309 DISCH_THEN(X_CHOOSE_THEN “v :'a set”
3310 (CONJUNCTS_THEN2 ASSUME_TAC SUBST1_TAC)) THEN
3311 FIRST_ASSUM(MP_TAC o SPEC “t :'a set” o
3312 MATCH_MP CLOSURE_OF_OPEN_IN_INTER_CLOSURE_OF) THEN
3313 ASM_SIMP_TAC std_ss[SET_RULE
3314 “t SUBSET u ==> (v INTER u) INTER t = v INTER t”] THEN
3315 DISCH_THEN(SUBST1_TAC o SYM) THEN
3316 MATCH_MP_TAC CLOSURE_OF_MONO THEN SET_TAC[],
3317 MATCH_MP_TAC CLOSURE_OF_MONO THEN
3318 MP_TAC(ISPECL [“top :'a topology”, “topspace top INTER (t :'a set)”]
3319 CLOSURE_OF_SUBSET) THEN
3320 REWRITE_TAC[GSYM CLOSURE_OF_RESTRICT, INTER_SUBSET] THEN
3321 FIRST_ASSUM(MP_TAC o MATCH_MP OPEN_IN_SUBSET) THEN
3322 REWRITE_TAC[TOPSPACE_SUBTOPOLOGY] THEN SET_TAC[]]
3323QED
3324
3325Theorem CLOSURE_OF_SUBTOPOLOGY_OPEN :
3326 !top u (s :'a set).
3327 open_in top u \/ s SUBSET u
3328 ==> (subtopology top u) closure_of s = u INTER top closure_of s
3329Proof
3330 REWRITE_TAC[SET_RULE “s SUBSET u <=> u INTER s = s”] THEN
3331 REPEAT STRIP_TAC THEN REWRITE_TAC[CLOSURE_OF_SUBTOPOLOGY] THEN
3332 ASM_MESON_TAC[OPEN_IN_INTER_CLOSURE_OF_EQ]
3333QED
3334
3335(* ------------------------------------------------------------------------- *)
3336(* Interior with respect to a topological space. *)
3337(* (ported from HOL-Light's Multivariate/metric.ml) *)
3338(* ------------------------------------------------------------------------- *)
3339
3340(* parse_as_infix("interior_of",(21,"right"));; *)
3341val _ = set_fixity "interior_of" (Infixr 602);
3342
3343Definition interior_of :
3344 top interior_of s = {x | ?t. open_in top t /\ x IN t /\ t SUBSET s}
3345End
3346
3347Theorem INTERIOR_OF_RESTRICT :
3348 !top (s :'a set).
3349 top interior_of s = top interior_of (topspace top INTER s)
3350Proof
3351 rw [interior_of, Once EXTENSION, SUBSET_INTER]
3352 >> MESON_TAC[OPEN_IN_SUBSET]
3353QED
3354
3355Theorem INTERIOR_OF_EQ :
3356 !top (s :'a set). (top interior_of s = s) <=> open_in top s
3357Proof
3358 rw [Once EXTENSION, interior_of]
3359 >> GEN_REWRITE_TAC RAND_CONV empty_rewrites[OPEN_IN_SUBOPEN]
3360 >> MESON_TAC[SUBSET_DEF]
3361QED
3362
3363Theorem INTERIOR_OF_OPEN_IN :
3364 !top (s :'a set). open_in top s ==> top interior_of s = s
3365Proof
3366 MESON_TAC[INTERIOR_OF_EQ]
3367QED
3368
3369Theorem INTERIOR_OF_EMPTY :
3370 !(top :'a topology). top interior_of {} = {}
3371Proof
3372 REWRITE_TAC[INTERIOR_OF_EQ, OPEN_IN_EMPTY]
3373QED
3374
3375Theorem INTERIOR_OF_TOPSPACE :
3376 !(top :'a topology). top interior_of (topspace top) = topspace top
3377Proof
3378 REWRITE_TAC[INTERIOR_OF_EQ, OPEN_IN_TOPSPACE]
3379QED
3380
3381Theorem OPEN_IN_INTERIOR_OF :
3382 !top (s :'a set). open_in top (top interior_of s)
3383Proof
3384 REPEAT GEN_TAC THEN REWRITE_TAC[interior_of] THEN
3385 GEN_REWRITE_TAC I empty_rewrites[OPEN_IN_SUBOPEN]
3386 >> rw [SUBSET_DEF]
3387 >> Q.EXISTS_TAC ‘t’ >> art []
3388 >> Q.X_GEN_TAC ‘y’
3389 >> STRIP_TAC
3390 >> Q.EXISTS_TAC ‘t’ >> rw []
3391QED
3392
3393Theorem INTERIOR_OF_INTERIOR_OF :
3394 !top (s :'a set). top interior_of top interior_of s = top interior_of s
3395Proof
3396 REWRITE_TAC[INTERIOR_OF_EQ, OPEN_IN_INTERIOR_OF]
3397QED
3398
3399Theorem INTERIOR_OF_SUBSET :
3400 !top (s :'a set). top interior_of s SUBSET s
3401Proof
3402 REWRITE_TAC[interior_of] THEN SET_TAC[]
3403QED
3404
3405Theorem INTERIOR_OF_SUBSET_CLOSURE_OF :
3406 !top (s :'a set). top interior_of s SUBSET top closure_of s
3407Proof
3408 REPEAT GEN_TAC THEN
3409 ONCE_REWRITE_TAC[INTERIOR_OF_RESTRICT, CLOSURE_OF_RESTRICT] THEN
3410 Q_TAC (TRANS_TAC SUBSET_TRANS) `topspace top INTER s` THEN
3411 SIMP_TAC std_ss[INTERIOR_OF_SUBSET, CLOSURE_OF_SUBSET, INTER_SUBSET]
3412QED
3413
3414Theorem SUBSET_INTERIOR_OF_EQ :
3415 !top (s :'a set). s SUBSET top interior_of s <=> open_in top s
3416Proof
3417 SIMP_TAC std_ss[GSYM INTERIOR_OF_EQ, GSYM SUBSET_ANTISYM_EQ, INTERIOR_OF_SUBSET]
3418QED
3419
3420Theorem INTERIOR_OF_MONO :
3421 !top s (t :'a set).
3422 s SUBSET t ==> top interior_of s SUBSET top interior_of t
3423Proof
3424 REWRITE_TAC[interior_of] THEN SET_TAC[]
3425QED
3426
3427Theorem INTERIOR_OF_MAXIMAL :
3428 !top s (t :'a set).
3429 t SUBSET s /\ open_in top t ==> t SUBSET top interior_of s
3430Proof
3431 REWRITE_TAC[interior_of] THEN SET_TAC[]
3432QED
3433
3434Theorem INTERIOR_OF_MAXIMAL_EQ :
3435 !top s (t :'a set).
3436 open_in top t ==> (t SUBSET top interior_of s <=> t SUBSET s)
3437Proof
3438 MESON_TAC[INTERIOR_OF_MAXIMAL, SUBSET_TRANS, INTERIOR_OF_SUBSET]
3439QED
3440
3441Theorem INTERIOR_OF_UNIQUE :
3442 !top s (t :'a set).
3443 t SUBSET s /\ open_in top t /\
3444 (!t'. t' SUBSET s /\ open_in top t' ==> t' SUBSET t)
3445 ==> top interior_of s = t
3446Proof
3447 MESON_TAC[SUBSET_ANTISYM, INTERIOR_OF_MAXIMAL, INTERIOR_OF_SUBSET,
3448 OPEN_IN_INTERIOR_OF]
3449QED
3450
3451Theorem INTERIOR_OF_SUBSET_TOPSPACE :
3452 !top (s :'a set). top interior_of s SUBSET topspace top
3453Proof
3454 rw [SUBSET_DEF, interior_of]
3455 >> METIS_TAC[REWRITE_RULE[SUBSET_DEF] OPEN_IN_SUBSET]
3456QED
3457
3458Theorem INTERIOR_OF_SUBSET_SUBTOPOLOGY :
3459 !top s (t :'a set). (subtopology top s) interior_of t SUBSET s
3460Proof
3461 REPEAT STRIP_TAC THEN MP_TAC
3462 (Q.ISPEC `subtopology top s` INTERIOR_OF_SUBSET_TOPSPACE) THEN
3463 SIMP_TAC std_ss[TOPSPACE_SUBTOPOLOGY, SUBSET_INTER]
3464QED
3465
3466Theorem INTERIOR_OF_INTER :
3467 !top s (t :'a set).
3468 top interior_of (s INTER t) = top interior_of s INTER top interior_of t
3469Proof
3470 REPEAT GEN_TAC THEN
3471 REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ, SUBSET_INTER] THEN
3472 SIMP_TAC std_ss[INTERIOR_OF_MONO, INTER_SUBSET] THEN
3473 SIMP_TAC std_ss[INTERIOR_OF_MAXIMAL_EQ, OPEN_IN_INTERIOR_OF, OPEN_IN_INTER] THEN
3474 MATCH_MP_TAC(SET_RULE
3475 “s SUBSET s' /\ t SUBSET t' ==> s INTER t SUBSET s' INTER t'”) THEN
3476 REWRITE_TAC[INTERIOR_OF_SUBSET]
3477QED
3478
3479Theorem INTERIOR_OF_INTERS_SUBSET :
3480 !top f:('a->bool)->bool.
3481 top interior_of (INTERS f) SUBSET
3482 INTERS {top interior_of s | s IN f}
3483Proof
3484 REWRITE_TAC[SUBSET_DEF, interior_of, INTERS_GSPEC]
3485 >> rw [IN_INTERS]
3486 >> simp []
3487 >> Q.EXISTS_TAC ‘t’ >> rw []
3488QED
3489
3490Theorem UNION_INTERIOR_OF_SUBSET :
3491 !top s (t :'a set).
3492 top interior_of s UNION top interior_of t
3493 SUBSET top interior_of (s UNION t)
3494Proof
3495 SIMP_TAC std_ss[UNION_SUBSET, INTERIOR_OF_MONO, SUBSET_UNION]
3496QED
3497
3498Theorem INTERIOR_OF_EQ_EMPTY :
3499 !top (s :'a set).
3500 top interior_of s = {} <=>
3501 !t. open_in top t /\ t SUBSET s ==> t = {}
3502Proof
3503 MESON_TAC[INTERIOR_OF_MAXIMAL_EQ, SUBSET_EMPTY,
3504 OPEN_IN_INTERIOR_OF, INTERIOR_OF_SUBSET]
3505QED
3506
3507Theorem INTERIOR_OF_EQ_EMPTY_ALT :
3508 !top (s :'a set).
3509 top interior_of s = {} <=>
3510 !t. open_in top t /\ ~(t = {}) ==> ~(t DIFF s = {})
3511Proof
3512 GEN_TAC THEN REWRITE_TAC[INTERIOR_OF_EQ_EMPTY] THEN SET_TAC[]
3513QED
3514
3515Theorem INTERIOR_OF_UNIONS_OPEN_IN_SUBSETS :
3516 !top (s :'a set).
3517 UNIONS {t | open_in top t /\ t SUBSET s} = top interior_of s
3518Proof
3519 REPEAT GEN_TAC THEN CONV_TAC SYM_CONV THEN
3520 MATCH_MP_TAC INTERIOR_OF_UNIQUE THEN
3521 simp [OPEN_IN_UNIONS] >> SET_TAC []
3522QED
3523
3524Theorem INTERIOR_OF_COMPLEMENT :
3525 !top (s :'a set).
3526 top interior_of (topspace top DIFF s) =
3527 topspace top DIFF top closure_of s
3528Proof
3529 REWRITE_TAC[interior_of, closure_of] THEN
3530 rw [Once EXTENSION, SUBSET_DEF] THEN
3531 MESON_TAC[REWRITE_RULE[SUBSET_DEF] OPEN_IN_SUBSET]
3532QED
3533
3534Theorem INTERIOR_OF_CLOSURE_OF :
3535 !top (s :'a set).
3536 top interior_of s =
3537 topspace top DIFF top closure_of (topspace top DIFF s)
3538Proof
3539 REPEAT GEN_TAC THEN
3540 REWRITE_TAC[GSYM INTERIOR_OF_COMPLEMENT] THEN
3541 GEN_REWRITE_TAC LAND_CONV empty_rewrites[INTERIOR_OF_RESTRICT] THEN
3542 AP_TERM_TAC THEN SET_TAC[]
3543QED
3544
3545Theorem CLOSURE_OF_INTERIOR_OF :
3546 !top (s :'a set).
3547 top closure_of s =
3548 topspace top DIFF top interior_of (topspace top DIFF s)
3549Proof
3550 REWRITE_TAC[INTERIOR_OF_COMPLEMENT] THEN
3551 REWRITE_TAC[SET_RULE “s = t DIFF (t DIFF s) <=> s SUBSET t”] THEN
3552 REWRITE_TAC[CLOSURE_OF_SUBSET_TOPSPACE]
3553QED
3554
3555Theorem CLOSURE_OF_COMPLEMENT :
3556 !top (s :'a set).
3557 top closure_of (topspace top DIFF s) =
3558 topspace top DIFF top interior_of s
3559Proof
3560 REWRITE_TAC[interior_of, closure_of] THEN
3561 rw [Once EXTENSION, SUBSET_DEF] THEN
3562 MESON_TAC[REWRITE_RULE[SUBSET_DEF] OPEN_IN_SUBSET]
3563QED
3564
3565Theorem INTERIOR_OF_EQ_EMPTY_COMPLEMENT :
3566 !top (s :'a set).
3567 top interior_of s = {} <=>
3568 top closure_of (topspace top DIFF s) = topspace top
3569Proof
3570 REPEAT GEN_TAC THEN MP_TAC(ISPECL
3571 [“top :'a topology”, “s :'a set”] INTERIOR_OF_SUBSET_TOPSPACE) THEN
3572 REWRITE_TAC[CLOSURE_OF_COMPLEMENT] THEN SET_TAC[]
3573QED
3574
3575Theorem CLOSURE_OF_EQ_UNIV :
3576 !top (s :'a set).
3577 top closure_of s = topspace top <=>
3578 top interior_of (topspace top DIFF s) = {}
3579Proof
3580 REPEAT GEN_TAC THEN MP_TAC(ISPECL
3581 [“top :'a topology”, “s :'a set”] CLOSURE_OF_SUBSET_TOPSPACE) THEN
3582 REWRITE_TAC[INTERIOR_OF_COMPLEMENT] THEN SET_TAC[]
3583QED
3584
3585Theorem INTERIOR_OF_SUBTOPOLOGY_SUBSET :
3586 !top s (u :'a set).
3587 u INTER top interior_of s SUBSET (subtopology top u) interior_of s
3588Proof
3589 simp[SUBSET_DEF, IN_INTER, interior_of, OPEN_IN_SUBTOPOLOGY] THEN
3590 REPEAT GEN_TAC THEN SIMP_TAC bool_ss[LEFT_AND_EXISTS_THM] THEN
3591 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
3592 HO_MATCH_MP_TAC MONO_EXISTS THEN
3593 SIMP_TAC std_ss[TAUT `(p /\ q) /\ r <=> q /\ p /\ r`] THEN
3594 ASM_SET_TAC[]
3595QED
3596
3597Theorem INTERIOR_OF_SUBTOPOLOGY_SUBSETS :
3598 !top s t (u :'a set).
3599 t SUBSET u
3600 ==> t INTER (subtopology top u) interior_of s SUBSET
3601 (subtopology top t) interior_of s
3602Proof
3603 REPEAT STRIP_TAC THEN FIRST_ASSUM(SUBST1_TAC o MATCH_MP (SET_RULE
3604 “t SUBSET u ==> t = u INTER t”)) THEN
3605 REWRITE_TAC[GSYM SUBTOPOLOGY_SUBTOPOLOGY] THEN
3606 FIRST_ASSUM(SUBST1_TAC o MATCH_MP (SET_RULE “t SUBSET u ==> u INTER t = t”)) THEN
3607 REWRITE_TAC[INTERIOR_OF_SUBTOPOLOGY_SUBSET]
3608QED
3609
3610Theorem INTERIOR_OF_SUBTOPOLOGY_MONO :
3611 !top s t (u :'a set).
3612 s SUBSET t /\ t SUBSET u
3613 ==> (subtopology top u) interior_of s SUBSET
3614 (subtopology top t) interior_of s
3615Proof
3616 REPEAT GEN_TAC THEN
3617 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
3618 MATCH_MP_TAC(SET_RULE
3619 “i SUBSET s /\ t INTER i SUBSET i'
3620 ==> s SUBSET t ==> i SUBSET i'”) THEN
3621 ASM_SIMP_TAC std_ss[INTERIOR_OF_SUBSET, INTERIOR_OF_SUBTOPOLOGY_SUBSETS]
3622QED
3623
3624Theorem INTERIOR_OF_SUBTOPOLOGY_OPEN :
3625 !top u (s :'a set).
3626 open_in top u
3627 ==> (subtopology top u) interior_of s = u INTER top interior_of s
3628Proof
3629 REPEAT STRIP_TAC THEN REWRITE_TAC[INTERIOR_OF_CLOSURE_OF] THEN
3630 ASM_SIMP_TAC std_ss[CLOSURE_OF_SUBTOPOLOGY_OPEN] THEN
3631 REWRITE_TAC[TOPSPACE_SUBTOPOLOGY] THEN
3632 REWRITE_TAC[SET_RULE “s INTER t DIFF u = t INTER (s DIFF u)”] THEN
3633 ASM_SIMP_TAC std_ss[GSYM OPEN_IN_INTER_CLOSURE_OF_EQ] THEN SET_TAC[]
3634QED
3635
3636Theorem DENSE_INTERSECTS_OPEN :
3637 !top (s :'a set).
3638 top closure_of s = topspace top <=>
3639 !t. open_in top t /\ ~(t = {}) ==> ~(s INTER t = {})
3640Proof
3641 REWRITE_TAC[CLOSURE_OF_INTERIOR_OF] THEN
3642 SIMP_TAC std_ss[INTERIOR_OF_SUBSET_TOPSPACE,
3643 SET_RULE “s SUBSET u ==> (u DIFF s = u <=> s = {})”] THEN
3644 REWRITE_TAC[INTERIOR_OF_EQ_EMPTY_ALT] THEN
3645 SIMP_TAC std_ss[OPEN_IN_SUBSET, SET_RULE
3646 “t SUBSET u ==> (~(t DIFF (u DIFF s) = {}) <=> ~(s INTER t = {}))”]
3647QED
3648
3649Theorem INTERIOR_OF_CLOSED_IN_UNION_EMPTY_INTERIOR_OF :
3650 !top s (t :'a set).
3651 closed_in top s /\ top interior_of t = {}
3652 ==> top interior_of (s UNION t) = top interior_of s
3653Proof
3654 REPEAT STRIP_TAC THEN REWRITE_TAC[INTERIOR_OF_CLOSURE_OF] THEN
3655 AP_TERM_TAC THEN
3656 REWRITE_TAC[SET_RULE “u DIFF (s UNION t) = (u DIFF s) INTER (u DIFF t)”] THEN
3657 W(MP_TAC o PART_MATCH (rand o rand) CLOSURE_OF_OPEN_IN_INTER_CLOSURE_OF o
3658 lhand o snd) THEN
3659 ASM_SIMP_TAC std_ss[CLOSURE_OF_COMPLEMENT, OPEN_IN_DIFF, OPEN_IN_TOPSPACE] THEN
3660 DISCH_THEN(SUBST1_TAC o SYM) THEN
3661 REWRITE_TAC[GSYM CLOSURE_OF_COMPLEMENT] THEN
3662 AP_TERM_TAC THEN SET_TAC[]
3663QED
3664
3665Theorem INTERIOR_OF_UNION_EQ_EMPTY :
3666 !top s (t :'a set).
3667 closed_in top s \/ closed_in top t
3668 ==> (top interior_of (s UNION t) = {} <=>
3669 top interior_of s = {} /\ top interior_of t = {})
3670Proof
3671 GEN_TAC THEN HO_MATCH_MP_TAC(MESON[]
3672 “(!x y. R x y ==> R y x) /\ (!x y. P x ==> R x y)
3673 ==> (!x y. P x \/ P y ==> R x y)”) THEN
3674 CONJ_TAC THENL [REWRITE_TAC[Once UNION_COMM] THEN SET_TAC[], ALL_TAC] THEN
3675 REPEAT STRIP_TAC THEN MATCH_MP_TAC(TAUT
3676 `(p ==> r) /\ (r ==> (p <=> q)) ==> (p <=> q /\ r)`) THEN
3677 ASM_SIMP_TAC std_ss[INTERIOR_OF_CLOSED_IN_UNION_EMPTY_INTERIOR_OF] THEN
3678 MATCH_MP_TAC(SET_RULE “s SUBSET t ==> t = {} ==> s = {}”) THEN
3679 SIMP_TAC std_ss[INTERIOR_OF_MONO, SUBSET_UNION]
3680QED
3681
3682(* ------------------------------------------------------------------------- *)
3683(* Frontier (aka boundary) with respect to topological space. *)
3684(* (ported from HOL-Light's Multivariate/metric.ml) *)
3685(* ------------------------------------------------------------------------- *)
3686
3687(* parse_as_infix("frontier_of",(21,"right"));; *)
3688val _ = set_fixity "frontier_of" (Infixr 602);
3689
3690Definition frontier_of :
3691 top frontier_of s = top closure_of s DIFF top interior_of s
3692End
3693
3694Theorem FRONTIER_OF_CLOSURES :
3695 !top s. top frontier_of s =
3696 top closure_of s INTER top closure_of (topspace top DIFF s)
3697Proof
3698 REPEAT GEN_TAC THEN CONV_TAC SYM_CONV THEN
3699 REWRITE_TAC[frontier_of, CLOSURE_OF_COMPLEMENT] THEN
3700 MATCH_MP_TAC(SET_RULE “s SUBSET u ==> s INTER (u DIFF t) = s DIFF t”) THEN
3701 REWRITE_TAC[CLOSURE_OF_SUBSET_TOPSPACE]
3702QED
3703
3704Theorem INTERIOR_OF_UNION_FRONTIER_OF :
3705 !top (s :'a set).
3706 top interior_of s UNION top frontier_of s = top closure_of s
3707Proof
3708 REPEAT GEN_TAC THEN REWRITE_TAC[frontier_of] THEN
3709 MP_TAC(Q.SPECL [`top`, `s`] INTERIOR_OF_SUBSET_CLOSURE_OF) THEN
3710 SET_TAC[]
3711QED
3712
3713Theorem FRONTIER_OF_RESTRICT :
3714 !top (s :'a set). top frontier_of s = top frontier_of (topspace top INTER s)
3715Proof
3716 REPEAT GEN_TAC THEN REWRITE_TAC[FRONTIER_OF_CLOSURES] THEN
3717 BINOP_TAC THEN GEN_REWRITE_TAC LAND_CONV empty_rewrites[CLOSURE_OF_RESTRICT] THEN
3718 AP_TERM_TAC THEN SET_TAC[]
3719QED
3720
3721Theorem CLOSED_IN_FRONTIER_OF :
3722 !top (s :'a set). closed_in top (top frontier_of s)
3723Proof
3724 SIMP_TAC std_ss[FRONTIER_OF_CLOSURES, CLOSED_IN_INTER, CLOSED_IN_CLOSURE_OF]
3725QED
3726
3727Theorem FRONTIER_OF_SUBSET_TOPSPACE :
3728 !top (s :'a set). top frontier_of s SUBSET topspace top
3729Proof
3730 SIMP_TAC std_ss[CLOSED_IN_SUBSET, CLOSED_IN_FRONTIER_OF]
3731QED
3732
3733Theorem FRONTIER_OF_SUBSET_SUBTOPOLOGY :
3734 !top s (t :'a set). (subtopology top s) frontier_of t SUBSET s
3735Proof
3736 MESON_TAC[TOPSPACE_SUBTOPOLOGY, FRONTIER_OF_SUBSET_TOPSPACE, SUBSET_INTER]
3737QED
3738
3739Theorem FRONTIER_OF_SUBTOPOLOGY_SUBSET :
3740 !top s (u :'a set).
3741 u INTER (subtopology top u) frontier_of s SUBSET (top frontier_of s)
3742Proof
3743 REPEAT GEN_TAC THEN REWRITE_TAC[frontier_of] THEN MATCH_MP_TAC(SET_RULE
3744 “s SUBSET s' /\ u INTER t' SUBSET t
3745 ==> u INTER (s DIFF t) SUBSET s' DIFF t'”) THEN
3746 REWRITE_TAC[CLOSURE_OF_SUBTOPOLOGY_SUBSET, INTERIOR_OF_SUBTOPOLOGY_SUBSET]
3747QED
3748
3749Theorem FRONTIER_OF_SUBTOPOLOGY_MONO :
3750 !top s t (u :'a set).
3751 s SUBSET t /\ t SUBSET u
3752 ==> (subtopology top t) frontier_of s SUBSET
3753 (subtopology top u) frontier_of s
3754Proof
3755 REPEAT STRIP_TAC THEN REWRITE_TAC[frontier_of] THEN MATCH_MP_TAC(SET_RULE
3756 “s SUBSET s' /\ t' SUBSET t ==> s DIFF t SUBSET s' DIFF t'”) THEN
3757 ASM_SIMP_TAC std_ss[CLOSURE_OF_SUBTOPOLOGY_MONO, INTERIOR_OF_SUBTOPOLOGY_MONO]
3758QED
3759
3760Theorem CLOPEN_IN_EQ_FRONTIER_OF :
3761 !top (s :'a set).
3762 closed_in top s /\ open_in top s <=>
3763 s SUBSET topspace top /\ top frontier_of s = {}
3764Proof
3765 REPEAT GEN_TAC THEN
3766 REWRITE_TAC[FRONTIER_OF_CLOSURES, OPEN_IN_CLOSED_IN_EQ] THEN
3767 ASM_CASES_TAC “(s :'a set) SUBSET topspace top” THEN ASM_REWRITE_TAC[] THEN
3768 EQ_TAC THENL [SIMP_TAC std_ss[CLOSURE_OF_CLOSED_IN] THEN SET_TAC[], DISCH_TAC] THEN
3769 ASM_SIMP_TAC std_ss[GSYM CLOSURE_OF_SUBSET_EQ, SUBSET_DIFF] THEN
3770 MATCH_MP_TAC(SET_RULE
3771 “c INTER c' = {} /\
3772 s SUBSET c /\ (u DIFF s) SUBSET c' /\ c SUBSET u /\ c' SUBSET u
3773 ==> c SUBSET s /\ c' SUBSET (u DIFF s)”) THEN
3774 ASM_SIMP_TAC std_ss[CLOSURE_OF_SUBSET, SUBSET_DIFF, CLOSURE_OF_SUBSET_TOPSPACE]
3775QED
3776
3777Theorem FRONTIER_OF_EQ_EMPTY :
3778 !top (s :'a set).
3779 s SUBSET topspace top
3780 ==> (top frontier_of s = {} <=> closed_in top s /\ open_in top s)
3781Proof
3782 SIMP_TAC std_ss[CLOPEN_IN_EQ_FRONTIER_OF]
3783QED
3784
3785Theorem FRONTIER_OF_OPEN_IN :
3786 !top (s :'a set).
3787 open_in top s ==> top frontier_of s = top closure_of s DIFF s
3788Proof
3789 SIMP_TAC std_ss[frontier_of, INTERIOR_OF_OPEN_IN]
3790QED
3791
3792Theorem FRONTIER_OF_OPEN_IN_STRADDLE_INTER :
3793 !top s (u :'a set).
3794 open_in top u /\ ~(u INTER top frontier_of s = {})
3795 ==> ~(u INTER s = {}) /\ ~(u DIFF s = {})
3796Proof
3797 REPEAT GEN_TAC THEN
3798 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
3799 SIMP_TAC std_ss[FRONTIER_OF_CLOSURES, INTER_ASSOC] THEN
3800 DISCH_THEN(MP_TAC o MATCH_MP (SET_RULE
3801 “~(s INTER t INTER u = {})
3802 ==> ~(s INTER t = {}) /\ ~(s INTER u = {})”)) THEN
3803 MATCH_MP_TAC MONO_AND THEN CONJ_TAC THEN
3804 W(MP_TAC o PART_MATCH (lhand o rand) OPEN_IN_INTER_CLOSURE_OF_EQ_EMPTY o
3805 rand o lhand o snd) THEN
3806 ASM_SET_TAC[]
3807QED
3808
3809Theorem FRONTIER_OF_SUBSET_CLOSED_IN :
3810 !top (s :'a set). closed_in top s ==> (top frontier_of s) SUBSET s
3811Proof
3812 REWRITE_TAC[GSYM CLOSURE_OF_SUBSET_EQ, frontier_of] THEN SET_TAC[]
3813QED
3814
3815Theorem FRONTIER_OF_EMPTY :
3816 !top. top frontier_of {} = {}
3817Proof
3818 REWRITE_TAC[FRONTIER_OF_CLOSURES, CLOSURE_OF_EMPTY, INTER_EMPTY]
3819QED
3820
3821Theorem FRONTIER_OF_TOPSPACE :
3822 !(top :'a topology). top frontier_of topspace top = {}
3823Proof
3824 SIMP_TAC std_ss[FRONTIER_OF_EQ_EMPTY, SUBSET_REFL] THEN
3825 REWRITE_TAC[OPEN_IN_TOPSPACE, CLOSED_IN_TOPSPACE]
3826QED
3827
3828Theorem FRONTIER_OF_SUBSET_EQ :
3829 !top (s :'a set).
3830 s SUBSET topspace top
3831 ==> ((top frontier_of s) SUBSET s <=> closed_in top s)
3832Proof
3833 REPEAT STRIP_TAC THEN EQ_TAC THEN SIMP_TAC std_ss[FRONTIER_OF_SUBSET_CLOSED_IN] THEN
3834 REWRITE_TAC[FRONTIER_OF_CLOSURES] THEN
3835 ASM_REWRITE_TAC[GSYM CLOSURE_OF_SUBSET_EQ] THEN
3836 ONCE_REWRITE_TAC[SET_RULE “s INTER t = s DIFF (s DIFF t)”] THEN
3837 DISCH_THEN(MATCH_MP_TAC o MATCH_MP (SET_RULE
3838 “s DIFF t SUBSET u ==> t SUBSET u ==> s SUBSET u”)) THEN
3839 MATCH_MP_TAC(SET_RULE
3840 “!u. u DIFF s SUBSET d /\ c SUBSET u ==> c DIFF d SUBSET s”) THEN
3841 EXISTS_TAC “(topspace top) :'a set” THEN
3842 REWRITE_TAC[CLOSURE_OF_SUBSET_TOPSPACE] THEN
3843 MATCH_MP_TAC CLOSURE_OF_SUBSET THEN SET_TAC[]
3844QED
3845
3846(* ------------------------------------------------------------------------- *)
3847(* HOL-Light's “derived_set_of” and HOL4's “limpt” *)
3848(* ------------------------------------------------------------------------- *)
3849
3850Theorem derived_set_of_alt_limpt :
3851 !top s. top derived_set_of s = {x | limpt top x s}
3852Proof
3853 rw [derived_set_of, limpt, Once EXTENSION]
3854 >> reverse EQ_TAC >> rw []
3855 >- (‘neigh top (t,x)’ by METIS_TAC [OPEN_OWN_NEIGH, IN_APP] \\
3856 Q.PAT_X_ASSUM ‘!N. neigh top (N,x) ==> _’ (MP_TAC o Q.SPEC ‘t’) >> rw [] \\
3857 Q.EXISTS_TAC ‘y’ >> rw [IN_APP])
3858 >> qabbrev_tac ‘u = top interior_of N’
3859 >> ‘open_in top u’ by PROVE_TAC [OPEN_IN_INTERIOR_OF]
3860 >> ‘u SUBSET N’ by PROVE_TAC [INTERIOR_OF_SUBSET]
3861 >> fs [neigh]
3862 >> ‘P SUBSET u’ by PROVE_TAC [INTERIOR_OF_MAXIMAL]
3863 >> ‘x IN u’ by METIS_TAC [SUBSET_DEF, IN_APP]
3864 >> Q.PAT_X_ASSUM ‘!t. x IN t /\ open_in top t ==> _’ (MP_TAC o Q.SPEC ‘u’)
3865 >> rw []
3866 >> ‘y IN N’ by METIS_TAC [SUBSET_DEF]
3867 >> Q.EXISTS_TAC ‘y’ >> fs [IN_APP]
3868QED
3869
3870Theorem limpt_alt :
3871 !top x s. limpt top x s <=> x IN top derived_set_of s
3872Proof
3873 simp [derived_set_of_alt_limpt]
3874QED
3875
3876Theorem limpt_mono :
3877 !top x s t. limpt top x s /\ s SUBSET t ==> limpt top x t
3878Proof
3879 rw [limpt_alt]
3880 >> Suff ‘top derived_set_of s SUBSET top derived_set_of t’ >- rw [SUBSET_DEF]
3881 >> MATCH_MP_TAC DERIVED_SET_OF_MONO >> art []
3882QED
3883
3884(* ------------------------------------------------------------------------- *)
3885(* Compact sets and compact topological spaces (from HOL-Light's metric.ml) *)
3886(* ------------------------------------------------------------------------- *)
3887
3888Definition compact_in :
3889 compact_in top s <=>
3890 s SUBSET topspace top /\
3891 (!U. (!u. u IN U ==> open_in top u) /\ s SUBSET UNIONS U
3892 ==> (?V. FINITE V /\ V SUBSET U /\ s SUBSET UNIONS V))
3893End
3894
3895Definition compact_space :
3896 compact_space (top :'a topology) <=> compact_in top (topspace top)
3897End
3898
3899Theorem COMPACT_SPACE_ALT :
3900 !(top :'a topology).
3901 compact_space top <=>
3902 !U. (!u. u IN U ==> open_in top u) /\
3903 topspace top SUBSET UNIONS U
3904 ==> ?V. FINITE V /\ V SUBSET U /\ topspace top SUBSET UNIONS V
3905Proof
3906 REWRITE_TAC[compact_space, compact_in, SUBSET_REFL]
3907QED
3908
3909Theorem COMPACT_SPACE :
3910 !(top :'a topology).
3911 compact_space top <=>
3912 !U. (!u. u IN U ==> open_in top u) /\
3913 UNIONS U = topspace top
3914 ==> ?V. FINITE V /\ V SUBSET U /\ UNIONS V = topspace top
3915Proof
3916 GEN_TAC THEN REWRITE_TAC[COMPACT_SPACE_ALT] THEN
3917 SIMP_TAC std_ss[GSYM SUBSET_ANTISYM_EQ, UNIONS_SUBSET] THEN
3918 AP_TERM_TAC THEN ABS_TAC THEN
3919 MESON_TAC[SUBSET_DEF, OPEN_IN_SUBSET]
3920QED
3921
3922Theorem COMPACT_IN_ABSOLUTE :
3923 !top (s :'a set).
3924 compact_in (subtopology top s) s <=> compact_in top s
3925Proof
3926 rw[compact_in] THEN
3927 simp[TOPSPACE_SUBTOPOLOGY, SUBSET_INTER, SUBSET_REFL] THEN
3928 simp[OPEN_IN_SUBTOPOLOGY, SET_RULE
3929 “(!x. x IN s ==> ?y. P y /\ x = f y) <=> s SUBSET IMAGE f {y | P y}”] THEN
3930 simp[IMP_CONJ, FORALL_SUBSET_IMAGE] THEN
3931 simp[EXISTS_FINITE_SUBSET_IMAGE] THEN
3932 simp[GSYM SIMPLE_IMAGE, GSYM INTER_UNIONS] THEN
3933 simp[SUBSET_INTER, SUBSET_REFL] THEN SET_TAC[]
3934QED
3935
3936Theorem COMPACT_IN_SUBSPACE :
3937 !top (s :'a set).
3938 compact_in top s <=>
3939 s SUBSET topspace top /\ compact_space (subtopology top s)
3940Proof
3941 rw[compact_space, COMPACT_IN_ABSOLUTE, TOPSPACE_SUBTOPOLOGY] THEN
3942 ONCE_REWRITE_TAC[TAUT `p /\ q <=> ~(p ==> ~q)`] THEN
3943 qabbrev_tac ‘t = topspace top’ \\
3944 Know ‘(s SUBSET t ==> ~compact_in (subtopology top s) (t INTER s)) <=>
3945 (s SUBSET t ==> ~compact_in (subtopology top s) s)’
3946 >- METIS_TAC [SET_RULE “s SUBSET t ==> t INTER s = s”] >> Rewr' \\
3947 REWRITE_TAC[COMPACT_IN_ABSOLUTE] THEN
3948 REWRITE_TAC[TAUT `(p <=> ~(q ==> ~p)) <=> (p ==> q)`] THEN
3949 SIMP_TAC std_ss[Abbr ‘t’, compact_in]
3950QED
3951
3952Theorem COMPACT_SPACE_SUBTOPOLOGY :
3953 !top (s :'a set). compact_in top s ==> compact_space (subtopology top s)
3954Proof
3955 SIMP_TAC std_ss[COMPACT_IN_SUBSPACE]
3956QED
3957
3958Theorem COMPACT_IN_SUBTOPOLOGY :
3959 !top s (t :'a set).
3960 compact_in (subtopology top s) t <=> compact_in top t /\ t SUBSET s
3961Proof
3962 REPEAT GEN_TAC THEN
3963 REWRITE_TAC[COMPACT_IN_SUBSPACE, SUBTOPOLOGY_SUBTOPOLOGY] THEN
3964 REWRITE_TAC[TOPSPACE_SUBTOPOLOGY, SUBSET_INTER] THEN
3965 ASM_CASES_TAC “(t :'a set) SUBSET s” THEN ASM_REWRITE_TAC[] THEN
3966 METIS_TAC [SET_RULE “t SUBSET s ==> s INTER t = t”]
3967QED
3968
3969Theorem COMPACT_IN_SUBSET_TOPSPACE :
3970 !top (s :'a set). compact_in top s ==> s SUBSET topspace top
3971Proof
3972 SIMP_TAC std_ss[compact_in]
3973QED
3974
3975Theorem COMPACT_IN_CONTRACTIVE :
3976 !top (top' :'a topology).
3977 topspace top' = topspace top /\
3978 (!u. open_in top u ==> open_in top' u)
3979 ==> !s. compact_in top' s ==> compact_in top s
3980Proof
3981 REPEAT GEN_TAC THEN STRIP_TAC THEN GEN_TAC THEN
3982 REWRITE_TAC[compact_in] THEN MATCH_MP_TAC MONO_AND THEN CONJ_TAC THENL
3983 [ASM_SET_TAC[], HO_MATCH_MP_TAC MONO_FORALL THEN ASM_SET_TAC[]]
3984QED
3985
3986Theorem COMPACT_SPACE_CONTRACTIVE :
3987 !top (top' :'a topology).
3988 topspace top' = topspace top /\
3989 (!u. open_in top u ==> open_in top' u)
3990 ==> compact_space top' ==> compact_space top
3991Proof
3992 SIMP_TAC std_ss[compact_space] THEN MESON_TAC[COMPACT_IN_CONTRACTIVE]
3993QED
3994
3995Theorem FINITE_IMP_COMPACT_IN :
3996 !top (s :'a set). s SUBSET topspace top /\ FINITE s ==> compact_in top s
3997Proof
3998 SIMP_TAC std_ss[compact_in] \\
3999 rpt STRIP_TAC \\
4000 EXISTS_TAC “IMAGE (\(x :'a). @u. u IN U /\ x IN u) s” THEN
4001 CONJ_TAC >- (MATCH_MP_TAC FINITE_IMAGE >> art []) \\
4002 ASM_SET_TAC []
4003QED
4004
4005Theorem COMPACT_IN_EMPTY :
4006 !(top :'a topology). compact_in top {}
4007Proof
4008 GEN_TAC THEN MATCH_MP_TAC FINITE_IMP_COMPACT_IN THEN
4009 REWRITE_TAC[FINITE_EMPTY, EMPTY_SUBSET]
4010QED
4011
4012Theorem COMPACT_SPACE_TOPSPACE_EMPTY :
4013 !(top :'a topology). topspace top = {} ==> compact_space top
4014Proof
4015 MESON_TAC[SUBTOPOLOGY_TOPSPACE, COMPACT_IN_EMPTY, compact_space]
4016QED
4017
4018Theorem FINITE_IMP_COMPACT_IN_EQ :
4019 !top (s :'a set).
4020 FINITE s ==> (compact_in top s <=> s SUBSET topspace top)
4021Proof
4022 MESON_TAC[COMPACT_IN_SUBSET_TOPSPACE, FINITE_IMP_COMPACT_IN]
4023QED
4024
4025Theorem COMPACT_IN_SING :
4026 !top (a :'a). compact_in top {a} <=> a IN topspace top
4027Proof
4028 SIMP_TAC std_ss[FINITE_IMP_COMPACT_IN_EQ, FINITE_SING, SING_SUBSET]
4029QED
4030
4031Theorem CLOSED_COMPACT_IN :
4032 !top k (c :'a set). compact_in top k /\ c SUBSET k /\ closed_in top c
4033 ==> compact_in top c
4034Proof
4035 rpt GEN_TAC
4036 >> REWRITE_TAC [compact_in] >> STRIP_TAC
4037 >> CONJ_TAC >- ASM_SET_TAC []
4038 >> rpt STRIP_TAC
4039 >> Q.PAT_X_ASSUM ‘!U. _ ==> ?V. FINITE V /\ _’
4040 (MP_TAC o Q.SPEC ‘(topspace top DIFF c) INSERT U’)
4041 >> ANTS_TAC
4042 >- (qabbrev_tac ‘t = topspace top’ \\
4043 ‘open_in top t’ by rw [OPEN_IN_TOPSPACE, Abbr ‘t’] \\
4044 reverse CONJ_TAC
4045 >- (rw [SUBSET_DEF] \\
4046 Cases_on ‘x IN c’
4047 >- (Q.PAT_X_ASSUM ‘c SUBSET BIGUNION U’ MP_TAC \\
4048 rw [SUBSET_DEF] \\
4049 POP_ASSUM (MP_TAC o Q.SPEC ‘x’) >> rw [] \\
4050 Q.EXISTS_TAC ‘s’ >> rw []) \\
4051 Q.EXISTS_TAC ‘t DIFF c’ >> simp [] \\
4052 ASM_SET_TAC []) \\
4053 rw [] >- (MATCH_MP_TAC OPEN_IN_DIFF >> art []) \\
4054 Q.PAT_X_ASSUM ‘c SUBSET BIGUNION U’ MP_TAC \\
4055 rw [SUBSET_DEF])
4056 >> STRIP_TAC
4057 >> Q.EXISTS_TAC ‘V DELETE (topspace top DIFF c)’
4058 >> ASM_REWRITE_TAC[FINITE_DELETE]
4059 >> CONJ_TAC >- ASM_SET_TAC []
4060 >> REWRITE_TAC[SUBSET_DEF, IN_UNIONS, IN_DELETE]
4061 >> ASM_SET_TAC []
4062QED
4063
4064Theorem CLOSED_IN_COMPACT_SPACE :
4065 !top (s :'a set).
4066 compact_space top /\ closed_in top s ==> compact_in top s
4067Proof
4068 REWRITE_TAC[compact_space] THEN REPEAT STRIP_TAC THEN
4069 MATCH_MP_TAC CLOSED_COMPACT_IN THEN EXISTS_TAC “topspace (top :'a topology)” THEN
4070 ASM_MESON_TAC[CLOSED_IN_SUBSET]
4071QED
4072
4073(* ----------------------------------------------------------------------
4074 Topological bases (c.f. HOL Light's "metric.ML")
4075 ---------------------------------------------------------------------- *)
4076
4077Theorem EMPTY_IN_ARBITRARY_UNION_OF[simp]:
4078 ∅ ∈ ARBITRARY UNION_OF P
4079Proof
4080 dsimp[UNION_OF, IN_DEF]
4081QED
4082
4083Theorem BIGUNION_IN_ARBITRARY_UNION_OF:
4084 A ⊆ ARBITRARY UNION_OF P ⇒ BIGUNION A ∈ ARBITRARY UNION_OF P
4085Proof
4086 rw[IN_DEF] >> irule ARBITRARY_UNION_OF_UNIONS >>
4087 gvs[SUBSET_DEF, IN_DEF]
4088QED
4089
4090Theorem ISTOPOLOGY_BASE_ALT:
4091 istopology (ARBITRARY UNION_OF P) ⇔
4092 ∀s t. s ∈ ARBITRARY UNION_OF P ∧ t ∈ ARBITRARY UNION_OF P ⇒
4093 s ∩ t ∈ ARBITRARY UNION_OF P
4094Proof
4095 simp[istopology] >> qmatch_abbrev_tac ‘Pp ∧ Qq ⇔ Pp’ >>
4096 ‘Qq’ suffices_by simp[EQ_IMP_THM] >>
4097 rw[Abbr‘Pp’, Abbr‘Qq’, BIGUNION_IN_ARBITRARY_UNION_OF]
4098QED
4099
4100Theorem ISTOPOLOGY_BASE_EQ:
4101 istopology (ARBITRARY UNION_OF P) ⇔
4102 ∀s t. s ∈ P ∧ t ∈ P ⇒ s ∩ t ∈ ARBITRARY UNION_OF P
4103Proof
4104 simp[ISTOPOLOGY_BASE_ALT, ARBITRARY_UNION_OF_INTER_EQ, IN_DEF]
4105QED
4106
4107Theorem ISTOPOLOGY_BASE:
4108 (∀s t. s ∈ B ∧ t ∈ B ⇒ s ∩ t ∈ B) ⇒
4109 istopology (ARBITRARY UNION_OF B)
4110Proof
4111 simp[ISTOPOLOGY_BASE_EQ] >> simp[ARBITRARY_UNION_OF_INC, IN_DEF]
4112QED
4113
4114Theorem OPEN_IN_TOPOLOGY_BASE:
4115 open_in top = ARBITRARY UNION_OF B ⇔
4116 (∀v. v ∈ B ⇒ open_in top v) ∧
4117 ∀u x. open_in top u /\ x ∈ u ⇒ ∃v. v ∈ B ∧ x ∈ v /\ v ⊆ u
4118Proof
4119 rw[EQ_IMP_THM]
4120 >- gvs[ARBITRARY_UNION_OF_INC, IN_DEF]
4121 >- (gvs[ARBITRARY, UNION_OF] >> irule_at Any SUBSET_BIGUNION_I >>
4122 gvs[IN_DEF] >> metis_tac[]) >>
4123 simp[FUN_EQ_THM, EQ_IMP_THM, FORALL_AND_THM, FORALL_UNION_OF] >> conj_tac
4124 >- (rw[UNION_OF, ARBITRARY] >> rename [‘open_in top u’] >>
4125 qexists ‘{ v | v ∈ B ∧ v ⊆ u}’ >> simp[IN_DEF] >> ASM_SET_TAC[]) >>
4126 rw[] >> irule OPEN_IN_UNIONS >> ASM_SET_TAC[]
4127QED
4128
4129Theorem TOPOLOGY_BASE_UNIQUE:
4130 (∀s. s ∈ P ⇒ open_in top s) ∧
4131 (∀u x. open_in top u ∧ x ∈ u ⇒ ∃b. b ∈ P ∧ x ∈ b ∧ b ⊆ u) ⇒
4132 topology (ARBITRARY UNION_OF P) = top
4133Proof
4134 rpt strip_tac >>
4135 match_mp_tac (MESON[topology_tybij] “open_in top = P ⇒ topology P = top”) >>
4136 simp[OPEN_IN_TOPOLOGY_BASE]
4137QED
4138
4139
4140(* References:
4141
4142 [1] J. L. Kelley, General Topology. Springer Science & Business Media, 1975.
4143
4144 *)