(* ========================================================================= *) (* A. H. Stone's theorem: a metric space is paracompact. *) (* *) (* HOL Light port of HOL88 proof written on 23rd June 1994. *) (* ========================================================================= *) let OPEN_BALL_INSIDE_POW2 = prove( `!m:(A)metric. !x s. x IN s /\ open(mtop m) s ==> ?n. ball(m)(x,inv(&2 pow n)) SUBSET s`, REPEAT GEN_TAC THEN DISCH_THEN (X_CHOOSE_THEN `e:real` STRIP_ASSUME_TAC o MATCH_MP OPEN_BALL_INSIDE) THEN IMP_RES_THEN (X_CHOOSE_TAC `n:num`) REAL_LE_POW12 THEN EXISTS_TAC `n:num` THEN MATCH_MP_TAC SUBSET_TRANS THEN EXISTS_TAC `ball(m)(x:A,e)` THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[SUBSET; IN; ball] THEN GEN_TAC THEN BETA_TAC THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `inv(&2 pow n)` THEN ASM_REWRITE_TAC[]);; let OPEN_BALL_INSIDE_SUC2 = prove( `!m:(A)metric. ball(m)(x,inv(&2 pow n)) SUBSET s ==> ball(m)(x,&3 * inv(&2 pow(SUC(SUC n)))) SUBSET s`, GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC SUBSET_TRANS THEN EXISTS_TAC `ball(m)(x:A,inv(&2 pow n))` THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[SUBSET] THEN GEN_TAC THEN REWRITE_TAC[IN; ball] THEN BETA_TAC THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LT_TRANS THEN EXISTS_TAC `&3 * inv(&2 pow(SUC(SUC n)))` THEN ASM_REWRITE_TAC[] THEN GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [GSYM REAL_POW2_ADD_SUC] THEN REWRITE_TAC[REAL_DOUBLE] THEN GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [GSYM REAL_POW2_ADD_SUC] THEN REWRITE_TAC[REAL_DOUBLE; REAL_MUL_ASSOC] THEN MATCH_MP_TAC REAL_LT_RMUL_IMP THEN CONJ_TAC THENL [REWRITE_TAC[REAL_MUL; REAL_LT] THEN CONV_TAC ARITH_CONV; MATCH_MP_TAC REAL_INV_POS THEN REWRITE_TAC[REAL_POS_POW2]]);; let OPEN_BALL_INSIDE_3POW2 = prove( `!m:(A)metric. !x s. x IN s /\ open(mtop m) s ==> ?n. ball(m)(x,&3 * inv(&2 pow n)) SUBSET s`, REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP OPEN_BALL_INSIDE_POW2) THEN DISCH_THEN(X_CHOOSE_TAC `n:num`) THEN EXISTS_TAC `SUC(SUC n)` THEN MATCH_MP_TAC OPEN_BALL_INSIDE_SUC2 THEN ASM_REWRITE_TAC[]);; let OPEN_BALL_X = prove( `!m:(A)metric. !n x. x IN ball(m)(x,inv(&2 pow n))`, REPEAT GEN_TAC THEN REWRITE_TAC[IN; ball] THEN BETA_TAC THEN REWRITE_TAC[METRIC_SAME] THEN MATCH_MP_TAC REAL_INV_POS THEN REWRITE_TAC[REAL_POS_POW2]);; let FINITE_PAIRBOUNDS = prove( `!P V N. (!i s s'. P(V(s,i):B) /\ P(V(s',i)) ==> (s:A = s') /\ i <= N) ==> FINITE { u | ?s n:num. (u = V(s,n)) /\ P(u) }`, REPEAT STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `IMAGE (\n:num. @u:B. ?s:A. (u = V(s,n)) /\ P(u)) {n | n <= N}` THEN CONJ_TAC THENL [MATCH_MP_TAC FINITE_IMAGE THEN REWRITE_TAC[FINITE_INSEG]; REWRITE_TAC[SUBSET; IN_IMAGE] THEN REWRITE_TAC[IN_ELIM_THM] THEN X_GEN_TAC `u:B` THEN ONCE_REWRITE_TAC[CONJ_SYM] THEN DISCH_THEN(X_CHOOSE_THEN `s:A` (X_CHOOSE_THEN `n:num` (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC))) THEN EXISTS_TAC `n:num` THEN BETA_TAC THEN CONJ_TAC THENL [FIRST_ASSUM(UNDISCH_TAC o assert is_forall o concl) THEN DISCH_THEN(MP_TAC o SPECL [`n:num`; `s:A`; `s:A`]) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[]; CONV_TAC SYM_CONV THEN MATCH_MP_TAC SELECT_UNIQUE THEN GEN_TAC THEN BETA_TAC THEN EQ_TAC THEN DISCH_TAC THENL [FIRST_ASSUM(X_CHOOSE_THEN `t:A` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN AP_TERM_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN FIRST_ASSUM(UNDISCH_TAC o assert is_forall o concl) THEN DISCH_THEN(MP_TAC o SPECL [`n:num`; `t:A`; `s:A`]) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[]; EXISTS_TAC `s:A` THEN ASM_REWRITE_TAC[]]]]);; (* ------------------------------------------------------------------------ *) (* Show that we can wellorder a cover by an irreflexive wellorder. *) (* ------------------------------------------------------------------------ *) let STONE_WO = prove( `!C:(A->bool)->bool. COVER(C) ==> ?(<<). (!x. ~(x << x)) /\ (!x y z. x << y /\ y << z ==> x << z) /\ (!x y. ~(x = y) ==> x << y \/ y << x) /\ (!x. ?u. x IN u /\ u IN C /\ ~(?v. v << u /\ x IN v /\ v IN C))`, GEN_TAC THEN REWRITE_TAC[COVER] THEN DISCH_THEN(MP_TAC o REWRITE_RULE[EXTENSION]) THEN REWRITE_TAC[IN_UNIONS_ALT; IN_UNIV] THEN DISCH_TAC THEN MP_TAC(ISPEC `\x:A->bool. T` WO) THEN DISCH_THEN(X_CHOOSE_THEN `l:(A->bool)#(A->bool)->bool` STRIP_ASSUME_TAC) THEN EXISTS_TAC `\x y. (less l)(x:A->bool,y)` THEN BETA_TAC THEN REPEAT CONJ_TAC THENL [REWRITE_TAC[less]; REPEAT STRIP_TAC THEN IMP_RES_THEN MATCH_MP_TAC WOSET_TRANS_LE THEN EXISTS_TAC `y:A->bool` THEN ASM_REWRITE_TAC[] THEN RULE_ASSUM_TAC(REWRITE_RULE[less]) THEN ASM_REWRITE_TAC[]; REPEAT GEN_TAC THEN DISCH_TAC THEN IMP_RES_THEN(MP_TAC o SPECL [`x:A->bool`; `y:A->bool`]) WOSET_TOTAL_LT THEN ASM_REWRITE_TAC[]; GEN_TAC THEN IMP_RES_THEN(MP_TAC o SPEC `\u:A->bool. x IN u /\ u IN C`) WOSET_WELL_CONTRAPOS THEN BETA_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN `u:A->bool` STRIP_ASSUME_TAC) THEN EXISTS_TAC `u:A->bool` THEN ASM_REWRITE_TAC[] THEN CONV_TAC NOT_EXISTS_CONV THEN ASM_REWRITE_TAC[TAUT `~(a /\ b /\ c) = a ==> ~(b /\ c)`]]);; (* ------------------------------------------------------------------------ *) (* The theorem. *) (* ------------------------------------------------------------------------ *) let STONE = prove( `!m:(A)metric. PARACOMPACT(mtop m)`, REWRITE_TAC[PARACOMPACT; OPEN_COVER] THEN REPEAT STRIP_TAC THEN IMP_RES_THEN(X_CHOOSE_THEN `(<<):(A->bool)->(A->bool)->bool` STRIP_ASSUME_TAC) STONE_WO THEN FIRST_ASSUM(X_CHOOSE_THEN `min:A->(A->bool)` MP_TAC o CONV_RULE SKOLEM_CONV) THEN PURE_REWRITE_TAC[FORALL_AND_THM] THEN STRIP_TAC THEN MP_TAC(ISPEC `\V (s,i). UNIONS { b | ?c. (b = ball(m)(c,inv(&2 pow i))) /\ (s:A->bool = min(c:A)) /\ (!t j. t IN C /\ j < i ==> ~(c IN V(t:A->bool,j))) /\ (ball(m)(c, &3 / (&2 pow i)) SUBSET s) }` (MATCH_MP WF_EREC (ISPEC `SND:(A->bool)#num->num` WF_MEASURE))) THEN REWRITE_TAC[measure] THEN ANTS_TAC THENL [REWRITE_TAC[FORALL_PAIR_THM] THEN REWRITE_TAC[SND] THEN CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN SIMP_TAC[]; DISCH_THEN(MP_TAC o EXISTENCE) THEN DISCH_THEN(X_CHOOSE_THEN `V:(A->bool)#num->(A->bool)` MP_TAC) THEN DISCH_THEN(MP_TAC o GEN_ALL o SPEC `s:A->bool,i:num`) THEN CONV_TAC(ONCE_DEPTH_CONV PAIRED_BETA_CONV) THEN DISCH_TAC] THEN SUBGOAL_THEN `!(s:A->bool) (i:num) (x:A). x IN V(s,i) = ?c. x IN ball(m)(c,inv(&2 pow i)) /\ (s = min c) /\ (!t j. t IN C /\ j < i ==> ~(c IN (V(t,j)))) /\ ball(m)(c,&3 * (inv(&2 pow i))) SUBSET s` ASSUME_TAC THENL [REPEAT GEN_TAC THEN FIRST_ASSUM(fun t -> GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [t]) THEN REWRITE_TAC[real_div; IN_UNIONS_ALT] THEN REWRITE_TAC[IN_ELIM_THM] THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [EXISTS_TAC `c:A` THEN REPEAT CONJ_TAC THEN ASM_REWRITE_TAC[] THEN EVERY_ASSUM(fun t -> try SUBST1_TAC(SYM t) with Failure _ -> ALL_TAC) THEN FIRST_ASSUM MATCH_ACCEPT_TAC; EXISTS_TAC `ball(m)(c:A,inv(&2 pow i))` THEN CONJ_TAC THENL [FIRST_ASSUM MATCH_ACCEPT_TAC; EXISTS_TAC `c:A`] THEN REWRITE_TAC[] THEN REPEAT CONJ_TAC THEN FIRST_ASSUM MATCH_ACCEPT_TAC]; ALL_TAC] THEN SUBGOAL_THEN `!s n. open(mtop m) ((V:(A->bool)#num->(A->bool))(s,n))` ASSUME_TAC THENL [REPEAT GEN_TAC THEN ONCE_ASM_REWRITE_TAC[] THEN MATCH_MP_TAC OPEN_UNIONS THEN REWRITE_TAC[IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[OPEN_BALL]; ALL_TAC] THEN SUBGOAL_THEN `!(s:A->bool) (n:num). V(s,n) SUBSET s` ASSUME_TAC THENL [REPEAT GEN_TAC THEN ONCE_ASM_REWRITE_TAC[] THEN REWRITE_TAC[SUBSET; IN_UNIONS_ALT] THEN REWRITE_TAC[IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN UNDISCH_TAC `(x:A) IN s'` THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[IN; ball] THEN BETA_TAC THEN DISCH_TAC THEN REWRITE_TAC[real_div] THEN MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `inv(&2 pow n)` THEN ASM_REWRITE_TAC[] THEN GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_LID] THEN MATCH_MP_TAC REAL_LE_RMUL_IMP THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LT_IMP_LE THEN MATCH_MP_TAC REAL_INV_POS THEN STRUCT_CASES_TAC (SPEC `n:num` num_CASES) THENL [REWRITE_TAC[pow]; MATCH_MP_TAC POW_POS_LT]; ALL_TAC] THEN REWRITE_TAC[REAL_LE; REAL_LT] THEN NUM_REDUCE_TAC; ALL_TAC] THEN SUBGOAL_THEN `!x:A. ?(s:A->bool) (n:num). x IN V(s,n)` ASSUME_TAC THENL [GEN_TAC THEN SUBGOAL_THEN `?n. ball(m)(x:A,&3 * inv(&2 pow n)) SUBSET (min x)` MP_TAC THENL [MATCH_MP_TAC OPEN_BALL_INSIDE_3POW2 THEN ASM_REWRITE_TAC[] THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]; DISCH_THEN(X_CHOOSE_THEN `N:num` ASSUME_TAC) THEN ASM_CASES_TAC `!t j:num. t IN C /\ j < N ==> ~((x:A) IN V(t:A->bool,j))` THENL [ONCE_ASM_REWRITE_TAC[] THEN MAP_EVERY EXISTS_TAC [`(min:A->A->bool) x`; `N:num`; `x:A`] THEN REWRITE_TAC[OPEN_BALL_X] THEN CONJ_TAC THEN FIRST_ASSUM MATCH_ACCEPT_TAC; FIRST_ASSUM(X_CHOOSE_THEN `t:A->bool` MP_TAC o CONV_RULE NOT_FORALL_CONV) THEN DISCH_THEN(X_CHOOSE_THEN `j:num` MP_TAC o CONV_RULE NOT_FORALL_CONV) THEN REWRITE_TAC[NOT_IMP] THEN STRIP_TAC THEN MAP_EVERY EXISTS_TAC [`t:A->bool`; `j:num`] THEN FIRST_ASSUM MATCH_ACCEPT_TAC]]; ALL_TAC] THEN SUBGOAL_THEN `!(x1:A) (s1:A->bool) x2 s2 (i:num). x1 IN V(s1,i) /\ x2 IN V(s2,i) /\ ~(s1 = s2) ==> (mdist m)(x1,x2) > inv(&2 pow i)` ASSUME_TAC THENL [REPEAT GEN_TAC THEN ONCE_ASM_REWRITE_TAC[] THEN DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_THEN `c1:A` STRIP_ASSUME_TAC) MP_TAC) THEN DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_THEN `c2:A` STRIP_ASSUME_TAC) MP_TAC) THEN UNDISCH_TAC `s1 = (min:A->A->bool) c1` THEN DISCH_THEN SUBST_ALL_TAC THEN UNDISCH_TAC `s2 = (min:A->A->bool) c2` THEN DISCH_THEN SUBST_ALL_TAC THEN DISCH_THEN(ANTE_RES_THEN DISJ_CASES_TAC) THEN UNDISCH_TAC `!x:A. ~(?v. v << (min x :A->bool) /\ x IN v /\ v IN C)` THENL [DISCH_THEN(MP_TAC o SPEC `c2:A`) THEN DISCH_THEN(MP_TAC o CONV_RULE NOT_EXISTS_CONV) THEN DISCH_THEN(MP_TAC o SPEC `(min:A->A->bool) c1`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN SUBGOAL_THEN `(mdist m)(c1:A,c2) >= &3 * inv(&2 pow i)` ASSUME_TAC THENL [POP_ASSUM MP_TAC THEN CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[REAL_NOT_LE; real_ge] THEN DISCH_TAC THEN UNDISCH_TAC `ball(m)(c1:A,&3 * (inv(&2 pow i))) SUBSET (min c1)` THEN REWRITE_TAC[SUBSET; IN; ball] THEN BETA_TAC THEN DISCH_THEN MATCH_MP_TAC THEN ASM_REWRITE_TAC[]; ALL_TAC]; DISCH_THEN(MP_TAC o SPEC `c1:A`) THEN DISCH_THEN(MP_TAC o CONV_RULE NOT_EXISTS_CONV) THEN DISCH_THEN(MP_TAC o SPEC `(min:A->A->bool) c2`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN SUBGOAL_THEN `(mdist m)(c1:A,c2) >= &3 * inv(&2 pow i)` ASSUME_TAC THENL [POP_ASSUM MP_TAC THEN CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[REAL_NOT_LE; real_ge] THEN DISCH_TAC THEN UNDISCH_TAC `ball(m)(c2:A,&3 * (inv(&2 pow i))) SUBSET (min c2)` THEN REWRITE_TAC[SUBSET; IN; ball] THEN BETA_TAC THEN ONCE_REWRITE_TAC[METRIC_SYM] THEN DISCH_THEN MATCH_MP_TAC THEN ASM_REWRITE_TAC[]; ALL_TAC]] THEN POP_ASSUM MP_TAC THEN CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[real_gt; real_ge; REAL_NOT_LT; REAL_NOT_LE] THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `(mdist m)(c1:A,x1) + (mdist m)(x1,x2) + (mdist m)(x2,c2)` THEN (CONJ_TAC THENL [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `(mdist m)(c1:A,x1) + (mdist m)(x1,c2)` THEN REWRITE_TAC[REAL_LE_LADD; METRIC_TRIANGLE]; REWRITE_TAC[SYM(NUM_REDUCE_CONV `1 + 1 + 1`)] THEN REWRITE_TAC[GSYM REAL_ADD; REAL_RDISTRIB; REAL_MUL_LID] THEN MATCH_MP_TAC REAL_LTE_ADD2 THEN CONJ_TAC THENL [UNDISCH_TAC `x1 IN ball(m)(c1:A,inv(&2 pow i))` THEN REWRITE_TAC[IN; ball] THEN BETA_TAC THEN REWRITE_TAC[]; MATCH_MP_TAC REAL_LE_ADD2 THEN ASM_REWRITE_TAC[] THEN UNDISCH_TAC `x2 IN ball(m)(c2:A,inv(&2 pow i))` THEN REWRITE_TAC[IN; ball] THEN BETA_TAC THEN DISCH_TAC THEN ONCE_REWRITE_TAC[METRIC_SYM] THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[]]]); ALL_TAC] THEN SUBGOAL_THEN `!i:num. !s:A->bool. s IN C \/ (V(s,i) = EMPTY:A->bool)` ASSUME_TAC THENL [REPEAT GEN_TAC THEN ASM_CASES_TAC `(s:A->bool) IN C` THEN ONCE_ASM_REWRITE_TAC[] THEN REWRITE_TAC[] THEN GEN_REWRITE_TAC I [EXTENSION] THEN REWRITE_TAC[IN_UNIONS_ALT; NOT_IN_EMPTY] THEN GEN_TAC THEN CONV_TAC NOT_EXISTS_CONV THEN GEN_TAC THEN REWRITE_TAC[DE_MORGAN_THM] THEN DISJ2_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN CONV_TAC NOT_EXISTS_CONV THEN GEN_TAC THEN REWRITE_TAC[DE_MORGAN_THM] THEN DISJ2_TAC THEN DISJ1_TAC THEN DISCH_TAC THEN UNDISCH_TAC `~((s:A->bool) IN C)` THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN SUBGOAL_THEN `!i j k l (x:A) (s:A->bool) (t:A->bool). ball(m)(x,inv(&2 pow k)) SUBSET V(t,j) /\ ~(ball(m)(x,inv(&2 pow l)) INTER V(s,i) = EMPTY) /\ j < i ==> inv(&2 pow k) <= inv(&2 pow i) + inv(&2 pow l)` ASSUME_TAC THENL [REPEAT GEN_TAC THEN REWRITE_TAC[EXTENSION; NOT_IN_EMPTY] THEN CONV_TAC(ONCE_DEPTH_CONV NOT_FORALL_CONV) THEN REWRITE_TAC[] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_THEN `y:A` MP_TAC) ASSUME_TAC) THEN REWRITE_TAC[IN_INTER] THEN ONCE_ASM_REWRITE_TAC[] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (X_CHOOSE_THEN `c:A` MP_TAC)) THEN STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `(mdist m)(x:A,c)` THEN CONJ_TAC THENL [UNDISCH_TAC `!t j. t IN C /\ j < i:num ==> ~((c:A) IN (V(t:A->bool,j)))` THEN DISCH_THEN(MP_TAC o SPECL [`t:A->bool`; `j:num`]) THEN REWRITE_TAC[ASSUME `j < i:num`] THEN FIRST_ASSUM (DISJ_CASES_TAC o SPECL [`j:num`; `t:A->bool`]) THENL [REWRITE_TAC[ASSUME `(t:A->bool) IN C`] THEN CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[REAL_NOT_LE] THEN DISCH_TAC THEN UNDISCH_TAC `ball(m)(x:A,inv(&2 pow k)) SUBSET V(t:A->bool,j:num)` THEN REWRITE_TAC[SUBSET; ASSUME `s = (min:A->A->bool) c`] THEN DISCH_THEN MATCH_MP_TAC THEN REWRITE_TAC[IN] THEN REWRITE_TAC[ball] THEN BETA_TAC THEN FIRST_ASSUM MATCH_ACCEPT_TAC; UNDISCH_TAC `ball(m)(x:A,inv(&2 pow k)) SUBSET V(t:A->bool,j:num)` THEN REWRITE_TAC[ASSUME `V(t:A->bool,j:num):A->bool = {}`] THEN REWRITE_TAC[SUBSET_EMPTY; EXTENSION; NOT_IN_EMPTY] THEN DISCH_THEN(MP_TAC o SPEC `x:A`) THEN REWRITE_TAC[OPEN_BALL_X]]; MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `(mdist m)(x:A,y) + (mdist m)(y,c)` THEN REWRITE_TAC[METRIC_TRIANGLE] THEN GEN_REWRITE_TAC RAND_CONV [REAL_ADD_SYM] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN RULE_ASSUM_TAC(BETA_RULE o REWRITE_RULE[IN; ball]) THEN CONJ_TAC THENL [ALL_TAC; ONCE_REWRITE_TAC[METRIC_SYM]] THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN FIRST_ASSUM MATCH_ACCEPT_TAC]; ALL_TAC] THEN EXISTS_TAC `{ u:A->bool | ?(s:A->bool) (n:num). u = V(s,n) }` THEN REPEAT CONJ_TAC THENL [REWRITE_TAC[COVER] THEN GEN_REWRITE_TAC I [EXTENSION] THEN X_GEN_TAC `x:A` THEN REWRITE_TAC[IN_UNIV; IN_UNIONS_ALT] THEN UNDISCH_TAC `!x:A. ?s n. x IN (V(s:A->bool,n:num))` THEN DISCH_THEN(MP_TAC o SPEC `x:A`) THEN DISCH_THEN(X_CHOOSE_THEN `s:A->bool` (X_CHOOSE_THEN `n:num` ASSUME_TAC)) THEN EXISTS_TAC `V(s:A->bool,n:num):A->bool` THEN CONJ_TAC THENL [FIRST_ASSUM MATCH_ACCEPT_TAC; REWRITE_TAC[IN_ELIM_THM] THEN MAP_EVERY EXISTS_TAC [`s:A->bool`; `n:num`] THEN REFL_TAC]; REWRITE_TAC[IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN ONCE_ASM_REWRITE_TAC[] THEN FIRST_ASSUM MATCH_ACCEPT_TAC; REWRITE_TAC[REFINES] THEN REWRITE_TAC[IN_ELIM_THM] THEN GEN_TAC THEN DISCH_THEN(X_CHOOSE_THEN `s:A->bool` (X_CHOOSE_THEN `n:num` SUBST1_TAC)) THEN FIRST_ASSUM(DISJ_CASES_TAC o SPECL [`n:num`; `s:A->bool`]) THENL [EXISTS_TAC `s:A->bool` THEN CONJ_TAC THEN FIRST_ASSUM MATCH_ACCEPT_TAC; UNDISCH_TAC `COVER(C:(A->bool)->bool)` THEN REWRITE_TAC[COVER] THEN REWRITE_TAC[EXTENSION; IN_UNIV; IN_UNIONS_ALT] THEN DISCH_THEN(X_CHOOSE_THEN `t:A->bool` STRIP_ASSUME_TAC o SPEC_ALL) THEN EXISTS_TAC `t:A->bool` THEN REWRITE_TAC[ASSUME `V(s:A->bool,n:num):A->bool = {}`] THEN REWRITE_TAC[EMPTY_SUBSET] THEN FIRST_ASSUM MATCH_ACCEPT_TAC]; REWRITE_TAC[LOCALLY_FINITE] THEN X_GEN_TAC `x:A`] THEN EVERY_ASSUM(fun th -> let t = concl th in if is_forall t & is_eq(snd(strip_forall t)) then (UNDISCH_TAC t THEN DISCH_THEN(K ALL_TAC)) else ALL_TAC) THEN UNDISCH_TAC `!x:A. ?s n. x IN (V(s:A->bool,n:num))` THEN DISCH_THEN(MP_TAC o SPEC `x:A`) THEN DISCH_THEN(X_CHOOSE_THEN `t:A->bool` (X_CHOOSE_TAC `j:num`)) THEN MP_TAC(SPECL [`m:(A)metric`; `x:A`; `V(t:A->bool,j:num):A->bool`] OPEN_BALL_INSIDE_POW2) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN `k:num` ASSUME_TAC) THEN SUBGOAL_THEN `!i s. i > SUC(j + k) ==> (ball(m)(x:A,inv(&2 pow (SUC k))) INTER V(s:A->bool,i) = EMPTY)` ASSUME_TAC THENL [REPEAT STRIP_TAC THEN FIRST_ASSUM(UNDISCH_TAC o assert (prefix< 3 o length o fst o strip_forall) o concl) THEN DISCH_THEN(MP_TAC o SPECL [`i:num`; `j:num`; `k:num`; `SUC k`; `x:A`; `s:A->bool`; `t:A->bool`]) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[TAUT `(~a /\ b ==> c) = b /\ ~c ==> a`] THEN DISCH_THEN MATCH_MP_TAC THEN REWRITE_TAC[REAL_NOT_LE] THEN CONJ_TAC THENL [UNDISCH_TAC `i > SUC(j + k)` THEN CONV_TAC ARITH_CONV; REWRITE_TAC[REAL_POW2_SUB_SUC; GSYM REAL_LT_SUB_LADD] THEN MATCH_MP_TAC REAL_LT_INV2 THEN REWRITE_TAC[REAL_POS_POW2] THEN REWRITE_TAC[REAL_LT_POW2] THEN UNDISCH_TAC `i > SUC(j + k)` THEN CONV_TAC ARITH_CONV]; ALL_TAC] THEN SUBGOAL_THEN `!(i:num) s s'. ~(ball(m)(x:A,inv(&2 pow (SUC i))) INTER V(s:A->bool,i) = EMPTY) /\ ~(ball(m)(x:A,inv(&2 pow (SUC i))) INTER V(s':A->bool,i) = EMPTY) ==> (s = s')` ASSUME_TAC THENL [REPEAT GEN_TAC THEN CONV_TAC CONTRAPOS_CONV THEN DISCH_TAC THEN REWRITE_TAC[EXTENSION; NOT_IN_EMPTY; IN_INTER] THEN CONV_TAC(ONCE_DEPTH_CONV NOT_FORALL_CONV) THEN REWRITE_TAC[] THEN DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_THEN `x1:A` STRIP_ASSUME_TAC) (X_CHOOSE_THEN `x2:A` STRIP_ASSUME_TAC)) THEN UNDISCH_TAC `!(x1:A) (s1:A->bool) x2 s2 (i:num). x1 IN V(s1,i) /\ x2 IN V(s2,i) /\ ~(s1 = s2) ==> (mdist m)(x1,x2) > inv(&2 pow i)` THEN DISCH_THEN(MP_TAC o SPECL [`x1:A`; `s:A->bool`; `x2:A`; `s':A->bool`]) THEN DISCH_THEN(MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[real_gt; REAL_NOT_LT] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `(mdist m)(x1:A,x) + (mdist m)(x,x2)` THEN REWRITE_TAC[METRIC_TRIANGLE] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `inv(&2 pow (SUC i)) + inv(&2 pow (SUC i))` THEN CONJ_TAC THENL [RULE_ASSUM_TAC(BETA_RULE o REWRITE_RULE[IN; ball]) THEN MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[METRIC_SYM] THEN ASM_REWRITE_TAC[]; REWRITE_TAC[REAL_POW2_ADD_SUC; REAL_LE_REFL]]; ALL_TAC] THEN SUBGOAL_THEN `!(i:num) s s'. ~(ball(m)(x:A,inv(&2 pow (SUC(SUC(j + k))))) INTER V(s:A->bool,i) = EMPTY) /\ ~(ball(m)(x:A,inv(&2 pow (SUC(SUC(j + k))))) INTER V(s':A->bool,i) = EMPTY) ==> (s = s') /\ i <= SUC(j + k)` ASSUME_TAC THENL [REPEAT GEN_TAC THEN DISCH_TAC THEN SUBGOAL_THEN `i <= SUC(j + k)` ASSUME_TAC THENL [GEN_REWRITE_TAC I [TAUT `a = ~ ~a`] THEN PURE_REWRITE_TAC[NOT_LE; GSYM GT] THEN DISCH_THEN(ANTE_RES_THEN (MP_TAC o SPEC `s:A->bool`)) THEN FIRST_ASSUM(MP_TAC o CONJUNCT1); ASM_REWRITE_TAC[] THEN FIRST_ASSUM MATCH_MP_TAC THEN EXISTS_TAC `i:num` THEN FIRST_ASSUM(UNDISCH_TAC o assert is_conj o concl) THEN MATCH_MP_TAC(TAUT `(a ==> b) /\ (c ==> d) ==> a /\ c ==> b /\ d`) THEN CONJ_TAC] THEN REWRITE_TAC[EXTENSION; NOT_IN_EMPTY; IN_INTER] THEN CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[] THEN DISCH_THEN(fun th -> X_GEN_TAC `y:A` THEN MP_TAC(SPEC `y:A` th)) THEN CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[] THEN REWRITE_TAC[TAUT `a /\ c ==> b /\ c = c ==> a ==> b`] THEN DISCH_TAC THEN REWRITE_TAC[IN; ball] THEN BETA_TAC THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `inv(&2 pow (SUC(SUC(j + k))))` THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_INV THEN ASM_REWRITE_TAC[REAL_POS_POW2; REAL_LE_POW2] THEN TRY(UNDISCH_TAC `i <= SUC(j + k)`) THEN CONV_TAC ARITH_CONV; ALL_TAC] THEN EXISTS_TAC `ball(m)(x:A,inv(&2 pow (SUC(SUC(j + k)))))` THEN CONJ_TAC THENL [REWRITE_TAC[neigh; re_subset] THEN EXISTS_TAC `ball(m)(x:A,inv(&2 pow (SUC(SUC(j + k)))))` THEN REWRITE_TAC[OPEN_BALL; REWRITE_RULE[IN] OPEN_BALL_X]; MP_TAC(ISPECL [`\u. ~(ball(m)(x:A,inv(&2 pow (SUC(SUC(j + k))))) INTER u = EMPTY)`; `V:(A->bool)#num->A->bool`; `SUC(j + k)`] FINITE_PAIRBOUNDS) THEN BETA_TAC THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(TAUT `(a = b) ==> a ==> b`) THEN AP_TERM_TAC THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN REWRITE_TAC[NOT_IN_EMPTY; IN_INTER] THEN MESON_TAC[]]);;