(* ------------------------------------------------------------------ *)
(*
   Topological Spaces, Metric Spaces,
   Connectedness, Totally bounded spaces, compactness,
   Hausdorff property, completeness, properties of Euclidean space,
   Author: Thomas Hales 2004
*)
(* ------------------------------------------------------------------ *)
(* prioritize_real (or num) *)
(* ------------------------------------------------------------------ *)
(* Logical Preliminaries *)
(* ------------------------------------------------------------------ *)
let Q_ELIM_THM = prove_by_refinement(
  `!P Q R . (?(u:B). (?(x:A). (u = P x) /\ (Q x)) /\ (R u)) <=>
    (?x. (Q x) /\ R( P x))`,
  (* {{{ proof *)
  [
  DISCH_ALL_TAC;
  MESON_TAC[];
  ]);;
 
let EQ_EMPTY = prove_by_refinement(
  `!P. ({(x:A) | P x} = {}) <=> (!x. ~P x)`,
  (* {{{ proof *)
  [
  DISCH_ALL_TAC;
  EQ_TAC;
  DISCH_TAC;
  (USE 0 (fun t-> AP_THM t `x:A`));
  USE 0 (REWRITE_RULE[IN_ELIM_THM';
 
let min_finite = prove_by_refinement(
  `!X.  (
FINITE X) /\ (~(X = 
EMPTY )) ==>
     (?delta. (X delta) /\ (!x. (X x) ==> (delta <=. x)))`,
  (* {{{ proof *)
  [
  TYPE_THEN `(!X k. 
FINITE X /\ (~(X = 
EMPTY )) /\ (X 
HAS_SIZE k) ==> (?delta. X delta /\ (!x. X x ==> delta <= x))) ==>(!X. 
FINITE X /\ (~(X = 
EMPTY )) ==> (?delta. X delta /\ (!x. X x ==> delta <= x)))` SUBGOAL_TAC ;
  DISCH_TAC;
  DISCH_ALL_TAC;
  TYPE_THEN `X` (USE 0 o SPEC);
  TYPE_THEN `
CARD X` (USE 0 o SPEC);
  UND 0;
  DISCH_THEN IMATCH_MP_TAC ;
  ASM_REWRITE_TAC[
HAS_SIZE ];
  DISCH_THEN IMATCH_MP_TAC ;
  CONV_TAC (quant_left_CONV "k");
  INDUCT_TAC;
  REWRITE_TAC[
HAS_SIZE_0];
  DISCH_ALL_TAC;
  ASM_REWRITE_TAC[
EMPTY];
  ASM_MESON_TAC[];
  DISCH_ALL_TAC;
  USE 3(REWRITE_RULE[
HAS_SIZE]);
  TYPE_THEN `X 
DELETE (
CHOICE X)` (USE 0 o SPEC);
  ASM_CASES_TAC `k=0`;
  REWR 3;
  USE 3 (REWRITE_RULE [ARITH_RULE `SUC 0=1`]);
  TYPE_THEN `
SING X` SUBGOAL_TAC ;
  IMATCH_MP_TAC  
CARD_SING_CONV;
  ASM_MESON_TAC [
HAS_SIZE];
  REWRITE_TAC[
SING];
  DISCH_TAC ;
  CHO 5;
  TYPE_THEN `x` EXISTS_TAC ;
  ASM_REWRITE_TAC[REWRITE_RULE[
IN] 
IN_SING ];
  REAL_ARITH_TAC;
  TYPE_THEN `
FINITE (X 
DELETE CHOICE X) /\ ~(X 
DELETE CHOICE X = {}) /\ (X 
DELETE CHOICE X 
HAS_SIZE k ) ` SUBGOAL_TAC;
  REWRITE_TAC[
FINITE_DELETE;
HAS_SIZE ];
  ASM_REWRITE_TAC[];
  REWR 3;
  IMATCH_MP_TAC  (TAUT `(a /\ b) ==> (b /\ a)`);
  SUBCONJ_TAC;
  IMATCH_MP_TAC  (ARITH_RULE `(SUC x = SUC y) ==> (x = y)`);
  COPY 3;
  UND 3;
  DISCH_THEN (fun t-> REWRITE_TAC[GSYM t]);
  IMATCH_MP_TAC  
CARD_DELETE_CHOICE;
  ASM_REWRITE_TAC[];
  IMATCH_MP_TAC  (TAUT `(b ==> ~a ) ==> (a ==> ~b)`);
  DISCH_THEN (fun t-> ASM_REWRITE_TAC[t;
CARD_CLAUSES]);
  DISCH_TAC;
  REWR 0;
  CHO 0;
  ALL_TAC; (* "ccx" *)
  TYPE_THEN `if (delta < (
CHOICE X)) then delta else (
CHOICE X)` EXISTS_TAC;
  (* REWRITE_TAC[min_real]; *)
  COND_CASES_TAC ;
  CONJ_TAC;
  UND 0;
  REWRITE_TAC[
DELETE;
IN ;IN_ELIM_THM' ];
  MESON_TAC[];
  GEN_TAC;
  UND 0;
  REWRITE_TAC[
DELETE;
IN ;IN_ELIM_THM' ];
  DISCH_ALL_TAC;
  TYPE_THEN  `x = 
CHOICE X` ASM_CASES_TAC ;
  ASM_REWRITE_TAC[];
  UND 6;
  REAL_ARITH_TAC;
  ASM_MESON_TAC[];
  SUBCONJ_TAC;
  IMATCH_MP_TAC  (REWRITE_RULE[
IN ] 
CHOICE_DEF);
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  DISCH_ALL_TAC;
  TYPE_THEN `x = 
CHOICE X` ASM_CASES_TAC ;
  ASM_REWRITE_TAC[];
  REAL_ARITH_TAC;
  UND 0;
    REWRITE_TAC[
DELETE;
IN ;IN_ELIM_THM' ];
  DISCH_ALL_TAC;
  TYPE_THEN `x` (USE 11 o SPEC);
  REWR 11;
  UND 11;
  UND 6;
  REAL_ARITH_TAC;
  ]);;
 
let min_finite_delta = prove_by_refinement(
  `!c X.  (
FINITE X) /\ ( !x. (X x) ==> (c <. x) ) ==>
     (?delta. (c <. delta) /\ (!x. (X x) ==> (delta <=. x)))`,
  (* {{{ proof *)
  [
  DISCH_ALL_TAC;
  TYPE_THEN `~(X = 
EMPTY)` ASM_CASES_TAC;
  JOIN 0 2;
  USE 0 (MATCH_MP 
min_finite);
  CHO 0;
  TYPE_THEN `delta` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  ASM_MESON_TAC[];
  REWR 2;
  ASM_REWRITE_TAC[
EMPTY];
  TYPE_THEN `c +. (&.1)` EXISTS_TAC;
  REAL_ARITH_TAC;
  ]);;
 
let union_closed_interval = prove_by_refinement(
  `!a b c. (a <=. b) /\ (b <=. c) ==>
    ({x | a <= x /\ x < b} 
UNION {x | b <= x /\ x <= c} =
     { x | a <= x /\ x <= c})`,
  (* {{{ proof *)
  [
  DISCH_ALL_TAC;
  REWRITE_TAC[
UNION;
IN;IN_ELIM_THM'];
  IMATCH_MP_TAC  
EQ_EXT ;
  REWRITE_TAC[IN_ELIM_THM'];
  UND 0;
  UND 1;
  REAL_ARITH_TAC;
  ]);;
 
let euclid_add_closure = prove_by_refinement(
  `!f g n. (euclid n f) /\ (euclid n g) ==> (euclid n (f + g))`,
(* {{{ *)
  [
  REWRITE_TAC[euclid;euclid_plus];
  ASM_MESON_TAC[REAL_ARITH `&0 +. (&.0) = (&.0)`];
  ]);;
 
let euclid_neg_closure = prove_by_refinement(
  `!f n. (euclid n f) ==> (euclid n (-- f))`,
(* {{{ *)
  [
  REWRITE_TAC[euclid;euclid_neg];
  DISCH_ALL_TAC;
  ASM_REWRITE_TAC[REAL_ARITH `(--x = &.0) <=> (x = &.0)`];
  ]);;
 
let euclid_sub_closure = prove_by_refinement(
  `!f g n. (euclid n f ) /\ (euclid n g) ==> (euclid n (f - g))`,
(* {{{ *)
  [
  REWRITE_TAC[euclid;euclid_minus];
  ASM_MESON_TAC[REAL_ARITH `&.0 -. (&.0) = (&.0)`];
  ]);;
 
let neg_dim = prove_by_refinement(
  `!f n. (euclid n f) = (euclid n (--f))`,
(* {{{ *)
  [
  REPEAT GEN_TAC;
  EQ_TAC;
  REWRITE_TAC[
euclid_neg_closure];
  REWRITE_TAC[euclid;euclid_neg];
  DISCH_ALL_TAC;
  ONCE_REWRITE_TAC[REAL_ARITH `(x = &.0) <=> (--x = &.0)`];
  ASM_REWRITE_TAC[];
  ]);;
 
let euclidean_add_closure = prove_by_refinement(
 `!f g. (euclidean f) /\ (euclidean g) ==> (euclidean (f+g))`,
(* {{{ *)
  [
  REWRITE_TAC[euclidean];
  DISCH_ALL_TAC;
  UNDISCH_FIND_THEN `euclid` CHOOSE_TAC;
  UNDISCH_FIND_THEN `(?)` CHOOSE_TAC;
  EXISTS_TAC `n+|n'`;
  ASSUME_TAC (ARITH_RULE `n <=| n+n'`);
  ASSUME_TAC (ARITH_RULE `n' <=| n+n'`);
  ASM_MESON_TAC[
euclid_add_closure;
euclid_updim];
  ]);;
 
let euclidean_sub_closure = prove_by_refinement(
  `!f g. (euclidean f) /\ (euclidean g) ==> (euclidean (f-g))`,
(* {{{ *)
  [
  REWRITE_TAC[euclidean];
  DISCH_ALL_TAC;
  UNDISCH_FIND_THEN `euclid` CHOOSE_TAC;
  UNDISCH_FIND_THEN `(?)` CHOOSE_TAC;
  EXISTS_TAC `n+|n'`;
  ASSUME_TAC (ARITH_RULE `n <=| n+n'`);
  ASSUME_TAC (ARITH_RULE `n' <=| n+n'`);
  ASM_MESON_TAC[
euclid_sub_closure;
euclid_updim];
  ]);;
 
let euclid_lzero = prove_by_refinement(
  `!f. euclid0 + f = f`,
(* {{{ *)
  [
  REWRITE_TAC[euclid_plus;euclid0;REAL_ARITH `&.0+a=a`];
  ACCEPT_TAC (INST_TYPE [(`:num`,`:A`);(`:real`,`:B`)] ETA_AX);
  ]);;
 
let euclid_rzero = prove_by_refinement(
  `!f. f + euclid0  = f`,
(* {{{ *)
  [
  REWRITE_TAC[euclid_plus;euclid0;REAL_ARITH `a+(&.0)=a`];
  ACCEPT_TAC (INST_TYPE [(`:num`,`:A`);(`:real`,`:B`)] ETA_AX);
  ]);;
 
let euclid_neg_sum = prove_by_refinement(
  `!x y .  euclid_minus (--x) (--y) = -- (euclid_minus x y)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[euclid_neg;euclid_minus];
  DISCH_ALL_TAC;
  IMATCH_MP_TAC  
EQ_EXT;
  BETA_TAC;
  REAL_ARITH_TAC;
  ]);;
 
let dot_euclid = prove_by_refinement(
 `!p f g. (euclid p f) /\ (euclid p g) ==>
   (dot f g = sum (0,p) (\i. (f i)* (g i)))`,
(* {{{ *)
  [
  REWRITE_TAC[dot];
    LET_TAC;
  REPEAT GEN_TAC;
  ABBREV_TAC `(P:num->bool) = \m. (euclid m f) /\ (euclid m g)`;
  DISCH_ALL_TAC;
  SUBGOAL_TAC `(P:num->bool) (p:num)`;
  EXPAND_TAC "P";
 
let dot_updim = prove_by_refinement (
 `!f g m n. (m <=|n) /\ (euclid m f) /\ (euclid m g) ==>
   (dot f g = sum (0,n) (\i. (f i)* (g i)))`,
(* {{{ *)
 [
 REPEAT GEN_TAC;
 DISCH_ALL_TAC;
   SUBGOAL_TAC `(euclid n f) /\ (euclid n g)`;
 ASM_MESON_TAC[
euclid_updim];
 MATCH_ACCEPT_TAC 
dot_euclid]
);;
 
let dot_nonneg = prove_by_refinement(
 `!f. (&.0 <= (dot f f))`,
(* {{{ *)
 [
 REWRITE_TAC[dot];
   LET_TAC;
 GEN_TAC;
 SUBGOAL_TAC `(!n. (&.0 <=. (\(i:num). f i *. f i) n))`;
 BETA_TAC;
 REWRITE_TAC[
REAL_LE_SQUARE];
 ASSUME_TAC(SPEC `\i. (f:num->real) i *. f i` 
SUM_POS);
 ASM_MESON_TAC[]]);;
 
let dot_comm = prove_by_refinement(
  `!f g. (dot f g = dot g f)`,
(* {{{ *)
 [
 REWRITE_TAC[dot];
 REWRITE_TAC[REAL_ARITH `a*.b = b*.a`;TAUT `a/\b <=> b/\a`]
 ]);;
 
let dot_neg = prove_by_refinement(
  `!f g. (dot (--f) g) = --. (dot f g)`,
(* {{{ *)
 [
 REWRITE_TAC[dot];
   LET_TAC;
  REWRITE_TAC [GSYM 
neg_dim];
  ONCE_REWRITE_TAC[GSYM 
SUM_NEG];
  REWRITE_TAC[euclid_neg];
  REPEAT GEN_TAC;
  AP_TERM_TAC;
  MATCH_MP_TAC 
EQ_EXT;
  BETA_TAC;
  GEN_TAC;
  REWRITE_TAC[REAL_ARITH `(--x) * y = --. (x *y)`];
 ]);;
 
let dot_scale = prove_by_refinement(
 `!n f g s. (euclid n f) /\ (euclid n g) ==>
  (dot (s *# f) g = s *. (dot f g))`,
(* {{{ *)
 [
 REWRITE_TAC[euclid_scale];
 REPEAT GEN_TAC;
   DISCH_THEN (fun th -> ASSUME_TAC th THEN ASSUME_TAC (MATCH_MP 
dot_euclid th));
   SUBGOAL_THEN (`euclid n (\ (i:num). (s *. f i) ) /\ (euclid n g)`) ASSUME_TAC;
 ASM_REWRITE_TAC[];
 ASSUME_TAC(REWRITE_RULE[euclid_scale](SPECL [`n:num`;`s:real`;`f:num->real`] 
euclid_scale_closure));
 ASM_MESON_TAC[];
 IMP_RES_THEN ASSUME_TAC 
dot_euclid;
 ASM_REWRITE_TAC[];
 REWRITE_TAC[GSYM 
SUM_CMUL];
 AP_TERM_TAC;
 MATCH_MP_TAC 
EQ_EXT;
 GEN_TAC;
 BETA_TAC;
 REWRITE_TAC[REAL_ARITH `a*.(b*.c) = (a*b)*c`];
 ]);;
 
let dot_scale_euclidean = prove_by_refinement(
  `!f g s. (euclidean f) /\ (euclidean g) ==>
  (dot (s *# f) g = s *. (dot f g))`,
(* {{{ *)
 [
 REWRITE_TAC[euclidean];
 DISCH_ALL_TAC;
 REPEAT (UNDISCH_FIND_THEN  `euclid` (CHOOSE_THEN MP_TAC));
 DISCH_ALL_TAC;
 ASSUME_TAC (ARITH_RULE `(n' <=| n+n')`);
 ASSUME_TAC (ARITH_RULE `(n <=| n+n')`);
 SUBGOAL_TAC `euclid (n+|n') f /\ euclid (n+n') g`;
 ASM_MESON_TAC[
euclid_updim];
 MESON_TAC[
dot_scale];
 ]);;
 
let dot_linear = prove_by_refinement(
 `!n f g h. (euclid n f) /\ (euclid n g) /\ (euclid n h) ==>
    ((dot (f + g) h ) = (dot f h) +. (dot g h))`,
(* {{{ *)
  [
  DISCH_ALL_TAC;
  SUBGOAL_TAC `euclid n (f+g)`;
  ASM_MESON_TAC[
euclid_add_closure];
  DISCH_TAC;
  MP_TAC (SPECL [`n:num`;`f:num->real`;`h:num->real`] 
dot_euclid);
  MP_TAC (SPECL [`n:num`;`g:num->real`;`h:num->real`] 
dot_euclid);
  MP_TAC (SPECL [`n:num`;`(f+g):num->real`;`h:num->real`] 
dot_euclid);  ASM_REWRITE_TAC[];
  DISCH_ALL_TAC;
  ASM_REWRITE_TAC[];
  REWRITE_TAC[GSYM 
SUM_ADD];
  AP_TERM_TAC;
  MATCH_MP_TAC 
EQ_EXT THEN GEN_TAC THEN BETA_TAC;
  REWRITE_TAC[euclid_plus];
  REWRITE_TAC[REAL_ARITH `(a+.b)*.c = a*c + b*c`];
  ]);;
 
let dot_minus_linear = prove_by_refinement(
 `!n f g h. (euclid n f) /\ (euclid n g) /\ (euclid n h) ==>
    ((dot (f - g) h ) = (dot f h) -. (dot g h))`,
(* {{{ *)
  [
  DISCH_ALL_TAC;
  SUBGOAL_TAC `euclid n (f-g)`;
  ASM_MESON_TAC[
euclid_sub_closure];
  DISCH_TAC;
  MP_TAC (SPECL [`n:num`;`f:num->real`;`h:num->real`] 
dot_euclid);
  MP_TAC (SPECL [`n:num`;`g:num->real`;`h:num->real`] 
dot_euclid);
  MP_TAC (SPECL [`n:num`;`(f-g):num->real`;`h:num->real`] 
dot_euclid);
  ASM_REWRITE_TAC[];
  DISCH_ALL_TAC;
  ASM_REWRITE_TAC[];
  REWRITE_TAC[GSYM 
SUM_SUB];
  AP_TERM_TAC;
  MATCH_MP_TAC 
EQ_EXT THEN GEN_TAC THEN BETA_TAC;
  REWRITE_TAC[euclid_minus];
  REWRITE_TAC[REAL_ARITH `(a-.b)*.c = a*c - b*c`];
  ]);;
 
let dot_linear_euclidean = prove_by_refinement(
 `!f g h. (euclidean f) /\ (euclidean g) /\ (euclidean h) ==>
    ((dot (f + g) h ) = (dot f h) +. (dot g h))`,
(* {{{ *)
  [
  REWRITE_TAC[euclidean];
  DISCH_ALL_TAC;
  REPEAT (UNDISCH_FIND_THEN `euclid` (CHOOSE_THEN MP_TAC));
  DISCH_ALL_TAC;
  SUBGOAL_TAC `(euclid (n+n'+n'') f)`;
  ASM_MESON_TAC[ARITH_RULE `n <=| n+n'+n''`;
euclid_updim];
  SUBGOAL_TAC `(euclid (n+n'+n'') g)`;
  ASM_MESON_TAC[ARITH_RULE `n' <=| n+n'+n''`;
euclid_updim];
  SUBGOAL_TAC `(euclid (n+n'+n'') h)`;
  ASM_MESON_TAC[ARITH_RULE `n'' <=| n+n'+n''`;
euclid_updim];
  MESON_TAC[
dot_linear]]);;
 
let dot_minus_linear_euclidean = prove_by_refinement(
 `!f g h. (euclidean f) /\ (euclidean g) /\ (euclidean h) ==>
    ((dot (f - g) h ) = (dot f h) -. (dot g h))`,
(* {{{ *)
  [
  REWRITE_TAC[euclidean];
  DISCH_ALL_TAC;
  REPEAT (UNDISCH_FIND_THEN `euclid` (CHOOSE_THEN MP_TAC));
  DISCH_ALL_TAC;
  SUBGOAL_TAC `(euclid (n+n'+n'') f)`;
  ASM_MESON_TAC[ARITH_RULE `n <=| n+n'+n''`;
euclid_updim];
  SUBGOAL_TAC `(euclid (n+n'+n'') g)`;
  ASM_MESON_TAC[ARITH_RULE `n' <=| n+n'+n''`;
euclid_updim];
  SUBGOAL_TAC `(euclid (n+n'+n'') h)`;
  ASM_MESON_TAC[ARITH_RULE `n'' <=| n+n'+n''`;
euclid_updim];
  MESON_TAC[
dot_minus_linear];
]);;
 
let dot_rzero = prove_by_refinement(
  `!f. (dot f euclid0) = &.0`,
(* {{{ *)
   [
     REWRITE_TAC[dot;euclid0];
     LET_TAC;
     GEN_TAC;
     SUBGOAL_THEN `(\ (i:num). (f i *. (&.0))) = (\ (r:num). (&.0))` (fun t -> REWRITE_TAC[t]);
   REWRITE_TAC[REAL_ARITH `a*.(&.0) = (&.0)`];
   MESON_TAC[
SUM_0];
   ]);;
 
let dot_zero = prove_by_refinement(
  `!f n. (euclid n f) /\ (dot f f = (&.0)) ==> (f = euclid0)`,
(* {{{ *)
   [
   DISCH_ALL_TAC;
   UNDISCH_TAC `dot f f = (&.0)`;
   MP_TAC (SPECL [`n:num`;`f:num->real`;`f:num->real`] 
dot_euclid);
   ASM_REWRITE_TAC[];
   DISCH_THEN (fun th -> REWRITE_TAC[th]);
   REWRITE_TAC[euclid0];
   DISCH_TAC;
   MATCH_MP_TAC 
EQ_EXT;
   GEN_TAC THEN BETA_TAC;
   DISJ_CASES_TAC (ARITH_RULE `x <| n \/ (n <=| x)`);
   CLEAN_ASSUME_TAC (ARITH_RULE `(x <|n) ==> (SUC x <=| n)`);
   CLEAN_THEN (SPECL [`SUC x`;`n:num`] 
LE_EXISTS) CHOOSE_TAC;
   UNDISCH_TAC `sum(0,n) (\ (i:num). f i *. f i) = (&.0)`;
   ASM_REWRITE_TAC[];
   REWRITE_TAC[GSYM 
SUM_TWO;sum;ARITH_RULE `0+| x = x`];
   SUBGOAL_TAC `!a b. (&.0 <=. sum(a,b) (\ (i:num). f i *. f i))`;
   REPEAT GEN_TAC;
   MP_TAC (SPEC `\ (i:num). f i *. f i` 
SUM_POS);
   BETA_TAC;
   REWRITE_TAC[
REAL_LE_SQUARE];
   MESON_TAC[];
   DISCH_ALL_TAC;
   IMP_RES_THEN MP_TAC (REAL_ARITH `(a+.b = &.0) ==> ((&.0 <=. b) ==> (a <=. (&.0)))`);
   ASM_REWRITE_TAC[];
   DISCH_TAC;
   IMP_RES_THEN MP_TAC (REAL_ARITH `(a+b <=. &.0) ==> ((&.0 <=. a) ==> (b <=. (&.0)))`);
   ASM_REWRITE_TAC[];
   ABBREV_TAC `a = (f:num->real) x`;
   MESON_TAC[
REAL_LE_SQUARE;REAL_ARITH `a <=. (&.0) /\ (&.0 <=. a) ==> (a = (&.0))`;
REAL_ENTIRE];
   UNDISCH_TAC `euclid n f`;
   REWRITE_TAC[euclid];
   ASM_MESON_TAC[];
   ]);;
 
let cauchy_schwartz = prove_by_refinement(
  `!f g. (euclidean f) /\ (euclidean g) ==>
   ((abs(dot f g)) <=. (norm f)*. (norm g))`,
(* {{{ *)
  [
  DISCH_ALL_TAC;
  DISJ_CASES_TAC (TAUT `(f = euclid0 ) \/ ~(f = euclid0)`);
  ASM_REWRITE_TAC[
dot_lzero;norm;
SQRT_0;REAL_ARITH`&.0 *. x = (&.0)`];
  REWRITE_TAC[
ABS_0;REAL_ARITH `x <=. x`];
  SUBGOAL_THEN `!a b. (dot (a *# f + b *# g) (a *# f + b *# g)) = a*a*(dot f f) + (&.2)*a*b*(dot f g) + b*b*(dot g g)` ASSUME_TAC;
  REPEAT GEN_TAC;
  ASM_SIMP_TAC[
euclidean_scale_closure;
euclidean_add_closure;
dot_linear_euclidean;
dot_linear2_euclidean;
dot_scale_euclidean;
dot_scale2_euclidean];
  REWRITE_TAC[
REAL_MUL_AC;
REAL_ADD_AC;REAL_ADD_LDISTRIB];
  MATCH_MP_TAC (REAL_ARITH`(b+. c=e) ==> (a+b+c+d = a+ e+d)`);
  REWRITE_TAC[GSYM REAL_LDISTRIB];
  REPEAT AP_TERM_TAC;
  MATCH_MP_TAC (REAL_ARITH `(a=b)==> (a+.b = a*(&.2))`);
  REWRITE_TAC[
dot_comm];
  FIRST_ASSUM (fun th -> ASSUME_TAC (SPECL[` --. (dot f g)`;`dot f f`] th));
  CLEAN_THEN (SPEC `(--.(dot f g)) *# f + (dot f f)*# g` 
dot_nonneg) ASSUME_TAC;
  REWRITE_TAC[norm];
  ASSUME_TAC(SPEC `f:num->real` 
dot_nonneg);
  ASSUME_TAC(SPEC `g:num->real` 
dot_nonneg);
  ASM_SIMP_TAC[GSYM 
SQRT_MUL];
  REWRITE_TAC[GSYM 
POW_2_SQRT_ABS;
POW_2];
  MATCH_MP_TAC 
SQRT_MONO_LE;
  REWRITE_TAC[
REAL_LE_SQUARE];
  SUBGOAL_TAC `&.0 <. dot f f`;
  MATCH_MP_TAC (REAL_ARITH `~(x = &.0) /\ (&.0 <=. x) ==> (&.0 <. x)`);
  ASM_REWRITE_TAC[];
  ASM_MESON_TAC[
dot_zero_euclidean];
  REPEAT (UNDISCH_FIND_TAC `(<=.)` );
  ABBREV_TAC `a = dot f f`;
  ABBREV_TAC `b = dot f g`;
  ABBREV_TAC `c = dot g g`;
  POP_ASSUM_LIST (fun t -> ALL_TAC);
  REWRITE_TAC[REAL_ARITH `(&.2 *. x = x + x)`;
REAL_ADD_AC];
  REWRITE_TAC[REAL_ARITH `(a *. ((--. b)*.c) = --. (a *. (b*.c)))/\ (--. ((--. a) *. b) = a *.b )`];
  REWRITE_TAC[REAL_ARITH `(--. b) *. a*. b + b*.b*.a = (&.0)`];
  REWRITE_TAC[REAL_ARITH `x +. (&.0) = x`];
  REWRITE_TAC[REAL_ARITH `(&.0 <=. (a*.a*.c +. (--.b)*.a*.b)) <=> (a*b*b <=. a*a*c)`];
  DISCH_ALL_TAC;
  MATCH_MP_TAC (SPEC `a:real` 
REAL_LE_LCANCEL_IMP);
  ASM_REWRITE_TAC[];
  ]);;
 
let metric_subspace = prove_by_refinement(
  `!X Y d. (Y 
SUBSET (X:A->bool)) /\ (metric_space (X,d)) ==>
    (metric_space (Y,d))`,
(* {{{ *)
  [
  REWRITE_TAC[
SUBSET;metric_space;
IN];
  DISCH_ALL_TAC;
  DISCH_ALL_TAC;
  UNDISCH_FIND_THEN `( /\ )` (fun t -> MP_TAC (SPECL[`x:A`;`y:A`;`z:A`] t));
  ASM_SIMP_TAC[];
  ]);;
 
let metric_euclidean = prove_by_refinement(
  `metric_space (euclidean,d_euclid)`,
(* {{{ *)
  [
  REWRITE_TAC[metric_space;d_euclid];
  DISCH_ALL_TAC;
  CONJ_TAC;
  REWRITE_TAC[
norm_nonneg];
  CONJ_TAC;
  EQ_TAC;
  REWRITE_TAC[norm];
  ONCE_REWRITE_TAC[REAL_ARITH `(&.0 = x) <=> (x = (&.0))`];
  ASM_SIMP_TAC[
dot_nonneg;
SQRT_EQ_0];
  DISCH_TAC;
  SUBGOAL_TAC `x - y = euclid0`;
  ASM_MESON_TAC[
dot_zero_euclidean;
euclidean_sub_closure];
  REWRITE_TAC[euclid_minus;euclid0];
  DISCH_TAC THEN (MATCH_MP_TAC 
EQ_EXT);
  X_GEN_TAC `n:num`;
  FIRST_ASSUM  (fun t -> ASSUME_TAC (BETA_RULE (AP_THM t `n:num`)));
  ASM_MESON_TAC [REAL_ARITH `(a = b) <=> (a-.b = (&.0))`];
  DISCH_THEN (fun t->REWRITE_TAC[t]);
  SUBGOAL_THEN `(y:num->real) - y = euclid0` (fun t-> REWRITE_TAC[t]);
  REWRITE_TAC[euclid0;euclid_minus];
  MATCH_MP_TAC 
EQ_EXT;
  GEN_TAC THEN BETA_TAC;
  REAL_ARITH_TAC;
  REWRITE_TAC[norm;
dot_lzero;
SQRT_0];
  CONJ_TAC;
  SUBGOAL_THEN `x - y = (euclid_neg (y-x))` ASSUME_TAC;
  REWRITE_TAC[euclid_neg;euclid_minus];
  MATCH_MP_TAC 
EQ_EXT THEN GEN_TAC THEN BETA_TAC;
  REAL_ARITH_TAC;
  ASM_MESON_TAC[
norm_neg];
  SUBGOAL_THEN `(x-z) = euclid_plus(x - y)  (y-z)` (fun t -> REWRITE_TAC[t]);
  REWRITE_TAC[euclid_plus;euclid_minus];
  MATCH_MP_TAC 
EQ_EXT THEN GEN_TAC THEN BETA_TAC THEN REAL_ARITH_TAC;
  ASM_SIMP_TAC[
norm_triangle;
euclidean_sub_closure;
euclidean_sub_closure];
  ]);;
 
let euclid1_abs = prove_by_refinement(
  `!x y. (euclid 1 x) /\ (euclid 1 y) ==>
     ((d_euclid x y) = (abs ((x 0) -. (y 0))))`,
  (* {{{ proof *)
  [
  REWRITE_TAC[d_euclid;norm];
  DISCH_ALL_TAC;
  SUBGOAL_TAC `euclid 1 (x - y)`;
  ASM_MESON_TAC[
euclid_sub_closure];
  DISCH_TAC;
  ASSUME_TAC (
prove(`1 <= 1`,ARITH_TAC));
  MP_TAC (SPECL[`(x-y):num->real`;`(x-y):num->real`;`1`;`1`] 
dot_updim);
  ASM_REWRITE_TAC[];
  DISCH_THEN (fun t-> REWRITE_TAC[t]);
  REWRITE_TAC[
prove(`1 = SUC 0`,ARITH_TAC)];
  REWRITE_TAC[sum];
  REWRITE_TAC[REAL_ARITH `&.0 + x = x`];
  REWRITE_TAC[ARITH_RULE `0 +| 0 = 0`];
  REWRITE_TAC[euclid_minus];
  ASM_MESON_TAC[REAL_POW_2;
POW_2_SQRT_ABS];
  ]);;
 
let euclid1_dirac = prove_by_refinement(
  `!x. euclid 1 x <=> (x = (x 0) *# (
dirac_delta 0))`,
  (* {{{ proof *)
  [
  DISCH_ALL_TAC;
  REWRITE_TAC[euclid; euclid_scale;
dirac_delta ];
  EQ_TAC;
  DISCH_ALL_TAC;
  IMATCH_MP_TAC  
EQ_EXT;
  X_GEN_TAC `n:num`;
  BETA_TAC;
  COND_CASES_TAC;
  REDUCE_TAC;
  ASM_REWRITE_TAC[];
  REDUCE_TAC;
  ASM_SIMP_TAC[ARITH_RULE  `(~(0=m))==>(1<=| m)`];
  DISCH_ALL_TAC;
  DISCH_ALL_TAC;
  USE 1 (MATCH_MP (ARITH_RULE `1<= m ==> (~(0=m))`));
  ASM ONCE_REWRITE_TAC[];
  ASM_REWRITE_TAC[];
  REDUCE_TAC ;
  ]);;
 
let proj_euclid1 = prove_by_refinement(
  `!i x. euclid 1 (proj i x)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[proj;euclid];
  REPEAT GEN_TAC;
  COND_CASES_TAC;
  ASM_REWRITE_TAC[];
  ARITH_TAC;
  ARITH_TAC;
  ]);;
 
let d_euclid_n = prove_by_refinement(
  `!n x y. ((euclid n x) /\ (euclid n y)) ==> ((d_euclid x y) =
     sqrt(sum (0,n) (\i. (x i - y i) * (x i - y i))))`,
  (* {{{ proof *)
  [
  REPEAT GEN_TAC;
  REWRITE_TAC[d_euclid;norm];
  DISCH_ALL_TAC;
  ASSUME_TAC (ARITH_RULE `n <=| n`);
  SUBGOAL_TAC `euclid n (x - y)`;
  ASM_SIMP_TAC[
euclid_sub_closure];
  DISCH_TAC;
  CLEAN_ASSUME_TAC (SPECL[`(x-y):num->real`;`(x-y):num->real`;`n:num`;`n:num`]
dot_updim);
  ASM_REWRITE_TAC[euclid_minus];
  ]);;
 
let norm_n = prove_by_refinement(
  `!n x. ((euclid n x) ) ==> ((norm x) =
     sqrt(sum (0,n) (\i. (x i ) * (x i ))))`,
  (* {{{ proof *)
  [
  REPEAT GEN_TAC;
  TYPEL_THEN [`x`;`x`;`n`;`n`] (fun t-> SIMP_TAC  [norm;ISPECL t 
dot_updim;ARITH_RULE `n <=| n`;]);
  ]);;
 
let proj_contraction = prove_by_refinement(
  `!n x y i. (euclid n x) /\ (euclid n y) ==>
     abs (x i - (y i)) <=. d_euclid x y`,
  (* {{{ proof *)
  [
  DISCH_ALL_TAC;
  MATCH_MP_TAC 
REAL_POW_2_LE;
  REWRITE_TAC[
REAL_ABS_POS];
  CONJ_TAC;
  ASM_MESON_TAC[
d_euclid_pos];
  ASM_SIMP_TAC[SPEC `n:num` 
d_euclid_n];
  REWRITE_TAC[
REAL_POW2_ABS];
  SUBGOAL_TAC `euclid n (x - y)`; (* why does MESON fail here??? *)
  MATCH_MP_TAC 
euclid_sub_closure;
  ASM_MESON_TAC[];
  DISCH_TAC;
  SUBGOAL_TAC `&.0 <=. sum (0,n) (\i. (x i - y i)*. (x i - y i))`;
  MATCH_MP_TAC 
SUM_POS_GEN;
  DISCH_ALL_TAC THEN BETA_TAC;
  REWRITE_TAC[
REAL_LE_SQUARE];
  SIMP_TAC[
SQRT_POW_2];
  DISCH_TAC;
  ASM_CASES_TAC `n <=| i`;
  MATCH_MP_TAC (REAL_ARITH `(x = (&.0)) /\ (&.0 <=. y) ==> (x <=. y)`);
  ASM_REWRITE_TAC[];
  REWRITE_TAC[REAL_PROP_ZERO_POW];
  NUM_REDUCE_TAC;
  ASM_MESON_TAC[euclid;euclid_minus];
  MP_TAC (ARITH_RULE `~(n <=| i) ==> (i < n) /\ (n = (SUC i) + (n-i-1))`);
  ASM_REWRITE_TAC[] THEN DISCH_ALL_TAC;
  ASM ONCE_REWRITE_TAC[];
  REWRITE_TAC[GSYM 
SUM_TWO];
  MATCH_MP_TAC (REAL_ARITH `(a <=. b) /\ (&.0 <=. c)   ==> (a <=. (b +c))`);
  CONJ_TAC;
  REWRITE_TAC[
sum_DEF];
  REWRITE_TAC[ARITH_RULE `0 +| i = i`];
  MATCH_MP_TAC (REAL_ARITH `(a = c) /\ (&.0 <=. b) ==> (a <=. b+c)`);
  REWRITE_TAC[REAL_POW_2];
  MP_TAC (SPECL [`0:num`;`i:num`;`(x:num->real)- y`] 
REAL_SUM_SQUARE_POS);
  BETA_TAC;
  REWRITE_TAC[euclid_minus];
  MP_TAC (SPECL [`SUC i`;`(n:num)-i-1`;`(x:num->real)- y`] 
REAL_SUM_SQUARE_POS);
  BETA_TAC;
  REWRITE_TAC[euclid_minus];
  ]);;
 
let D_EUCLID_BOUND = prove_by_refinement(
  `!n x y eps. ((euclid n x) /\ (euclid n y) /\
     (!i. (abs (x i -. y i) <=. eps))) ==>
    ( d_euclid x y <=. sqrt(&.n)*. eps )`,
  (* {{{ proof *)
  [
  DISCH_ALL_TAC;
  SQUARE_TAC;
  SUBCONJ_TAC;
  JOIN 0 1;
  USE 0 (MATCH_MP 
d_euclid_pos);
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  WITH 2 (SPEC `0`);
  USE 4 (MATCH_MP (REAL_ARITH `abs (x) <=. eps ==> &.0 <=. eps`));
  SUBCONJ_TAC;
  ALL_TAC;
  REWRITE_TAC[
REAL_MUL_NN];
  DISJ1_TAC;
  CONJ_TAC;
  MATCH_MP_TAC 
SQRT_POS_LE ;
  REDUCE_TAC;
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  ASM_SIMP_TAC[
d_euclid_pow2];
  SUBGOAL_TAC `!i. ((x:num->real) i -. y i) *. (x i -. y i) <=. eps* eps`;
  GEN_TAC;
  ALL_TAC;
  USE 2 (SPEC `i:num`);
  ABBREV_TAC `t = x i - (y:num->real) i`;
  UND 2;
  REWRITE_TAC[
ABS_SQUARE_LE];
  REWRITE_TAC[
REAL_POW_MUL];
  ASSUME_TAC (REWRITE_RULE[] ((REDUCE_CONV `&.0 <= &.n`)));
  USE 6 (REWRITE_RULE[GSYM 
SQRT_POW2]);
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  ALL_TAC;
  MATCH_MP_TAC 
SUM_BOUND;
  GEN_TAC;
  DISCH_TAC;
  BETA_TAC;
  REWRITE_TAC[
POW_2];
  ASM_MESON_TAC[];
  ]);;
 
let metric_translate = prove_by_refinement(
  `!n x y z . (euclid n x) /\ (euclid n y) /\ (euclid n z) ==>
   (d_euclid (x + z) (y + z) = d_euclid x y)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[d_euclid;norm];
  DISCH_ALL_TAC;
  TYPE_THEN `euclid n (euclid_minus x y)` SUBGOAL_TAC;
  ASM_SIMP_TAC[
euclid_sub_closure];
  DISCH_TAC;
  TYPE_THEN `euclid n (euclid_minus (euclid_plus x z) (euclid_plus y z))` SUBGOAL_TAC;
  ASM_SIMP_TAC[
euclid_sub_closure; 
euclid_add_closure];
  DISCH_ALL_TAC;
  ASM_SIMP_TAC[SPEC `n:num` 
dot_euclid];
  TYPE_THEN `(x + z) - (y + z) = ((x:num->real) - y)` SUBGOAL_TAC;
  IMATCH_MP_TAC  
EQ_EXT;
  X_GEN_TAC `i:num`;
  REWRITE_TAC[euclid_minus;euclid_plus];
  REAL_ARITH_TAC;
  DISCH_THEN (fun t-> REWRITE_TAC[t]);
  ]);;
 
let metric_translate_LEFT = prove_by_refinement(
  `!n x y z . (euclid n x) /\ (euclid n y) /\ (euclid n z) ==>
   (d_euclid (z + x ) (z + y) = d_euclid x y)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[d_euclid;norm];
  DISCH_ALL_TAC;
  TYPE_THEN `euclid n (euclid_minus x y)` SUBGOAL_TAC;
  ASM_SIMP_TAC[
euclid_sub_closure];
  DISCH_TAC;
  TYPE_THEN `euclid n (euclid_minus (euclid_plus z x) (euclid_plus z y))` SUBGOAL_TAC;
  ASM_SIMP_TAC[
euclid_sub_closure; 
euclid_add_closure];
  DISCH_ALL_TAC;
  ASM_SIMP_TAC[SPEC `n:num` 
dot_euclid];
  TYPE_THEN `(z + x) - (z + y) = ((x:num->real) - y)` SUBGOAL_TAC;
  IMATCH_MP_TAC  
EQ_EXT;
  X_GEN_TAC `i:num`;
  REWRITE_TAC[euclid_minus;euclid_plus];
  REAL_ARITH_TAC;
  DISCH_THEN (fun t-> REWRITE_TAC[t]);
  ]);;
 
let norm_scale = prove_by_refinement(
  `!t t' x . (euclidean x) ==>
   (d_euclid (t *# x) (t' *# x) =
        ||. (t - t') * norm(x))`,
  (* {{{ proof *)
  [
  REWRITE_TAC[euclidean];
  LEFT_TAC "n";
 
let closed_UNIV = prove_by_refinement(
  `!(U:(A->bool)->bool). (topology_ U ==> closed_ U (
UNIONS U))`,
  (* {{{ proof *)
  [
  DISCH_ALL_TAC;
  ASM_SIMP_TAC[
open_closed];
  REWRITE_TAC[closed;open_DEF];
  TYPE_THEN `a = 
UNIONS U` ABBREV_TAC;
  USE 0 (REWRITE_RULE[topology]);
  CONJ_TAC;
  MESON_TAC[
SUBSET];
  USE 0 (CONV_RULE (quant_right_CONV "V"));
  USE 0 (CONV_RULE (quant_right_CONV "B"));
  USE 0 (CONV_RULE (quant_right_CONV "A"));
  
AND 0;
  UND 2;
  MESON_TAC[
DIFF_EQ_EMPTY];
  ]);;
 
let closed_inter = prove_by_refinement (
  `!U V. (topology_ (U:(A->bool)->bool)) /\ (!a. (V a) ==> (closed_ U a))
    /\ ~(V = 
EMPTY)
     ==> (closed_ U (
INTERS V))`,
  (* {{{ proof *)
  [
  REWRITE_TAC[closed];
  DISCH_ALL_TAC;
  CONJ_TAC;
  MATCH_MP_TAC  
INTERS_SUBSET2;
  USE 2 (REWRITE_RULE[ 
EMPTY_EXISTS]);
  USE 2 (REWRITE_RULE[
IN]);
  CHO 2;
  EXISTS_TAC `u:A->bool`;
  ASM_MESON_TAC[ ];
  ABBREV_TAC `VCOMP = 
IMAGE ((
DIFF) (
UNIONS (U:(A->bool)->bool))) V`;
  UNDISCH_FIND_THEN `VCOMP` (fun t -> ASSUME_TAC (GSYM t));
  SUBGOAL_THEN `(VCOMP:(A->bool)->bool) 
SUBSET U` ASSUME_TAC;
  ASM_REWRITE_TAC[
SUBSET;
IN_ELIM_THM;
IMAGE];
  REWRITE_TAC[
IN];
  GEN_TAC;
  ASM_MESON_TAC[open_DEF];
  SUBGOAL_THEN `open_ U (
UNIONS (VCOMP:(A->bool)->bool))` ASSUME_TAC;
  ASM_MESON_TAC[topology;open_DEF];
  SUBGOAL_THEN ` (
UNIONS U 
DIFF INTERS V)= (
UNIONS (VCOMP:(A->bool)->bool))` (fun t-> (REWRITE_TAC[t]));
  ASM_REWRITE_TAC[
UNIONS_INTERS];
  UNDISCH_FIND_TAC `(open_)`;
  REWRITE_TAC[];
  ]);;
 
let open_nbd = prove_by_refinement(
  `!U (A:A->bool). (topology_ U) ==>
    ((U A) = (!x. ?B. (A x ) ==> ((B 
SUBSET A) /\ (B x) /\ (U B))))`,
  (* {{{ proof *)
  [
  DISCH_ALL_TAC;
  EQ_TAC;
  DISCH_ALL_TAC;
  GEN_TAC;
  EXISTS_TAC `A:A->bool`;
  ASM_MESON_TAC[
SUBSET];
  CONV_TAC (quant_left_CONV "B");
  DISCH_THEN CHOOSE_TAC;
  USE 1 (CONV_RULE NAME_CONFLICT_CONV);
  TYPE_THEN `
UNIONS (
IMAGE B A)  = A` SUBGOAL_TAC;
  MATCH_MP_TAC  
SUBSET_ANTISYM;
  CONJ_TAC;
  MATCH_MP_TAC  
UNIONS_SUBSET;
  REWRITE_TAC[
IN_IMAGE];
  ASM_MESON_TAC[
IN];
  REWRITE_TAC[
SUBSET;
IN_UNIONS;
IN_IMAGE];
  DISCH_ALL_TAC;
  NAME_CONFLICT_TAC;
  CONV_TAC (quant_left_CONV "x'");
  CONV_TAC (quant_left_CONV "x'");
  EXISTS_TAC `x:A`;
  TYPE_THEN `B x` EXISTS_TAC ;
  ASM_REWRITE_TAC[];
  ASM_MESON_TAC[
IN];
  (* on 1*)
  TYPE_THEN `(
IMAGE B A) 
SUBSET U` SUBGOAL_TAC;
  REWRITE_TAC[
SUBSET;
IN_IMAGE;];
  REWRITE_TAC[
IN];
  NAME_CONFLICT_TAC;
  GEN_TAC;
  DISCH_THEN CHOOSE_TAC;
  ASM_REWRITE_TAC[];
  ASM_MESON_TAC[];
  TYPE_THEN `W = 
IMAGE B A` ABBREV_TAC;
  KILL 2;
  ASM_MESON_TAC[topology];
  ]);;
 
let open_inters = prove_by_refinement(
  `!U (V:(A->bool)->bool). (topology_ U) /\ (V 
SUBSET U) /\
    (
FINITE V) /\ ~(V = 
EMPTY)  ==>
                        (U (
INTERS V))`,
  (* {{{ proof *)
  [
  REP_GEN_TAC;
  DISCH_ALL_TAC;
  TYPE_THEN `(?n. V 
HAS_SIZE n)` SUBGOAL_TAC;
  REWRITE_TAC[
HAS_SIZE];
  ASM_MESON_TAC[];
  DISCH_ALL_TAC;
  UND 0;
  UND 1;
  UND 2;
  UND 3;
  UND 4;
  CONV_TAC (quant_left_CONV "n");
  TYPE_THEN `V` SPEC2_TAC ;
  TYPE_THEN `U` SPEC2_TAC ;
  CONV_TAC (quant_left_CONV "n");
  CONV_TAC (quant_left_CONV "n");
  INDUCT_TAC;
  DISCH_ALL_TAC;
  ASM_MESON_TAC[
HAS_SIZE_0];
  DISCH_ALL_TAC;
  TYPE_THEN `U` (USE 0 o SPEC);
  USE 5 (REWRITE_RULE[
HAS_SIZE_SUC;
EMPTY_EXISTS]);
  
AND 5;
  CHO 6;
  TYPE_THEN `u` (USE 5 o SPEC);
  REWR 5;
  TYPE_THEN `V 
DELETE u` (USE  0 o SPEC);
  REWR 0;
  TYPE_THEN `V={u}` ASM_CASES_TAC;
  ASM_REWRITE_TAC[
inters_singleton];
  UND 6;
  UND 2;
  REWRITE_TAC [
SUBSET;
IN];
  MESON_TAC[];
  ALL_TAC; (* oi1 *)
  USE 0 (REWRITE_RULE[
delete_empty]);
  REWR 0;
  USE 0 (REWRITE_RULE[
FINITE_DELETE]);
  REWR 0;
  TYPE_THEN `V 
DELETE u 
SUBSET U ` SUBGOAL_TAC;
  ASM_MESON_TAC[
DELETE_SUBSET;
SUBSET_TRANS];
  DISCH_ALL_TAC;
  REWR 0;
  ALL_TAC; (* oi2 *)
  COPY 6;
  USE 9 (REWRITE_RULE[
IN]);
  USE 9 (MATCH_MP 
delete_inters);
  ASM_REWRITE_TAC[];
  USE 1 (REWRITE_RULE[topology]);
  TYPEL_THEN [`(
INTERS (V 
DELETE u))`;`u`;`U`] (USE 1 o ISPECL);
  
AND 1;
  
AND 1;
  UND 11;
  DISCH_THEN MATCH_MP_TAC ;
  ASM_REWRITE_TAC[];
  UND 6;
  UND 2;
  REWRITE_TAC [
SUBSET;
IN];
  ASM_MESON_TAC[];
  ]);;
 
let open_ball_nonempty = prove_by_refinement(
 `!(X:A->bool) d a r. (metric_space (X,d)) /\ (&.0 <. r) /\ (X a) ==>
    (a 
IN (open_ball(X,d) a r))`,
 (* {{{ proof *)
 [
 REWRITE_TAC[metric_space;
IN_ELIM_THM;open_ball];
 DISCH_ALL_TAC;
 UNDISCH_FIND_THEN `( /\ )` (ASSUME_TAC o (SPECL [`a:A`;`a:A`;`a:A`]));
 ASM_MESON_TAC[];
 ]);;
 
let open_ball_center = prove_by_refinement(
 `!(X:A->bool) d a b r. (metric_space (X,d)) /\
      (a 
IN (open_ball (X,d) b r)) ==>
     (?r'. (&.0 <. r') /\
         ((open_ball(X,d) a r') 
SUBSET (open_ball(X,d) b r)))`,
(* {{{ proof *)
 [
 REWRITE_TAC[metric_space;open_ball];
 DISCH_ALL_TAC;
 EXISTS_TAC `r -. (d (a:A) (b:A))`;
 REWRITE_TAC[
SUBSET;
IN_ELIM_THM];
 UNDISCH_FIND_TAC `(
IN)`;
 REWRITE_TAC[
IN_ELIM_THM];
 DISCH_ALL_TAC;
 CONJ_TAC;
 REWRITE_TAC[REAL_ARITH `(&.0 < r -. s)= (s <. r)`];
 ASM_MESON_TAC[];
 GEN_TAC;
 ASM_REWRITE_TAC[];
 REWRITE_TAC[REAL_ARITH `(u <. v-.w) <=> (w +. u <. v)`];
 DISCH_ALL_TAC;
 ASM_REWRITE_TAC[];
 UNDISCH_FIND_TAC `(!)`;
 DISCH_THEN (fun t-> (MP_TAC (SPECL [`b:A`;`a:A`;`x:A`] t)));
 ASM_REWRITE_TAC[];
 ASM_MESON_TAC[
REAL_LET_TRANS;
REAL_LTE_TRANS];
 ]);;
 
let open_ball_neg_radius = prove_by_refinement(
  `!(X:A->bool) d a r. metric_space(X,d) /\ (r <. (&.0)) ==>
    (
EMPTY = open_ball(X,d) a r)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[open_ball;metric_space];
  DISCH_ALL_TAC;
  MATCH_MP_TAC 
EQ_EXT;
  GEN_TAC;
  REWRITE_TAC[
EMPTY;
IN_ELIM_THM];
  FIRST_ASSUM  (fun t -> MP_TAC (SPECL [`a:A`;`x:A`;`a:A`] t));
  ASSUME_TAC (REAL_ARITH `!d r. ~((d <. r) /\ (r <. (&.0)) /\ (&.0 <=. d))`);
  ASM_MESON_TAC[];
  ]);;
 
let open_ball_inter = prove_by_refinement(
 `!(X:A->bool) d a b c r r'. (metric_space (X,d)) /\ (X a) /\ (X b) /\
  (c 
IN (open_ball(X,d) a r 
INTER (open_ball(X,d) b r'))) ==>
  (?r''. (&.0 <. r'') /\ (open_ball(X,d) c r'') 
SUBSET
    (open_ball(X,d) a r 
INTER (open_ball(X,d) b r')))`,
  (* {{{ proof *)
  [
  DISCH_ALL_TAC;
    UNDISCH_FIND_THEN `(
INTER)` (fun t-> MP_TAC (REWRITE_RULE[
IN_INTER] t) THEN DISCH_ALL_TAC);
  SUBGOAL_TAC `(X:A->bool) (c:A)`;
  ASM_MESON_TAC[
SUBSET;
open_ball_subset;
IN];
  DISCH_TAC;
  MP_TAC (SPECL[`X:A->bool`;`d:A->A->real`;`c:A`;`b:A`;`r':real`] 
open_ball_center) THEN (ASM_REWRITE_TAC[]) THEN (DISCH_THEN CHOOSE_TAC);
  MP_TAC (SPECL[`X:A->bool`;`d:A->A->real`;`c:A`;`a:A`;`r:real`] 
open_ball_center) THEN (ASM_REWRITE_TAC[]) THEN (DISCH_THEN CHOOSE_TAC);
  REWRITE_TAC[
SUBSET_INTER];
  EXISTS_TAC `(if (r'' <. r''') then (r'') else (r'''))`;
  COND_CASES_TAC;
  ASM_MESON_TAC[
open_ball_nest;
SUBSET_TRANS];
  IMP_RES_THEN DISJ_CASES_TAC (REAL_ARITH `(~(r'' <. r''')) ==> ((r''' <. r'') \/ (r'''=r''))`);
  ASM_MESON_TAC[
open_ball_nest;
SUBSET_TRANS];
  ASM_MESON_TAC[];
  ]);;
 
let BALL_DIST = prove_by_refinement(
  `!X d x y (z:A) r. metric_space(X,d) /\ open_ball(X,d) z r x /\
  open_ball(X,d) z r y ==> d x y <. (&.2 * r)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[metric_space;open_ball;IN_ELIM_THM'];
  DISCH_ALL_TAC;
  USE 0 (SPECL [`x:A`;`z:A`;`y:A`]);
  REWR 0;
  UND 0 THEN DISCH_ALL_TAC;
  UND 9;
  UND 6;
  ASM_REWRITE_TAC[];
  UND 3;
  REAL_ARITH_TAC;
  ]);;
 
let BALL_DIST_CLOSED = prove_by_refinement(
  `!X d x y (z:A) r. metric_space(X,d) /\ closed_ball(X,d) z r x /\
  closed_ball(X,d) z r y ==> d x y <=. (&.2 * r)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[metric_space;closed_ball;IN_ELIM_THM'];
  DISCH_ALL_TAC;
  USE 0 (SPECL [`x:A`;`z:A`;`y:A`]);
  REWR 0;
  UND 0 THEN DISCH_ALL_TAC;
  UND 9;
  UND 6;
  ASM_REWRITE_TAC[];
  UND 3;
  REAL_ARITH_TAC;
  ]);;
 
let ball_symm = prove_by_refinement(
  `!X d (x:A) y r. metric_space(X,d) /\ (X x) /\ (X y) ==>
       (open_ball(X,d) x r y = open_ball(X,d) y r x)`,
  (* {{{ proof *)
  [
  DISCH_ALL_TAC;
  REWRITE_TAC [open_ball;IN_ELIM_THM'];
  ASM_REWRITE_TAC[];
  ASM_MESON_TAC [
metric_space_symm];
  ]);;
 
let ball_subset_ball = prove_by_refinement(
  `!X d (x:A) z r. metric_space(X,d) /\
       (open_ball(X,d) x r z ) ==>
    (open_ball(X,d) z r 
SUBSET (open_ball(X,d) x (&.2 * r)))`,
  (* {{{ proof *)
  [
    DISCH_ALL_TAC;
    REWRITE_TAC[
SUBSET;
IN];
    DISCH_ALL_TAC;
    REWRITE_TAC[open_ball;IN_ELIM_THM'];
    TYPE_THEN `X z /\ X x' /\ X x` SUBGOAL_TAC ;
    UND 2;
    UND 1;
    REWRITE_TAC[open_ball;IN_ELIM_THM'];
    MESON_TAC[];
    DISCH_ALL_TAC;
    TYPE_THEN `open_ball(X,d) z r x` SUBGOAL_TAC;
    ASM_MESON_TAC[
ball_symm];
    ASM_MESON_TAC[
BALL_DIST];
  ]);;
 
let top_of_metric_unions = prove_by_refinement(
 `!(X:A->bool) d. (metric_space (X,d)) ==>
    (X = 
UNIONS (top_of_metric (X,d)))`,
  (* {{{ proof *)
 [
 REPEAT GEN_TAC;
 DISCH_TAC;
 MATCH_MP_TAC 
SUBSET_ANTISYM THEN CONJ_TAC;
 REWRITE_TAC[
SUBSET];
 REWRITE_TAC[
IN_UNIONS;top_of_metric];
 DISCH_ALL_TAC;
 EXISTS_TAC `open_ball(X,d) (x:A) (&.1)`;
 UNDISCH_TAC `(x:A) 
IN X` THEN (REWRITE_TAC[
IN_ELIM_THM]);
 DISCH_ALL_TAC;
 CONJ_TAC;
 EXISTS_TAC `{(open_ball(X,d) (x:A) (&.1))}`;
 REWRITE_TAC[GSYM 
UNIONS_1;
INSERT_SUBSET;
EMPTY_SUBSET];
 REWRITE_TAC[open_balls;
IN_ELIM_THM];
 MESON_TAC[];
 REWRITE_TAC[
IN_ELIM_THM;open_ball];
 UNDISCH_FIND_TAC `(
IN)`;
 ASM_REWRITE_TAC[
IN];
 DISCH_TAC;
 ASM_REWRITE_TAC[];
 UNDISCH_FIND_TAC `metric_space`;
 REWRITE_TAC[metric_space];
 DISCH_THEN (fun t -> MP_TAC (ISPECL [`x:A`;`x:A`;`x:A`] t));
 ASM_MESON_TAC[REAL_ARITH `(&.0) <. (&.1)`];
 MATCH_MP_TAC 
UNIONS_SUBSET;
 GEN_TAC;
 REWRITE_TAC[top_of_metric;
IN_ELIM_THM];
 DISCH_THEN CHOOSE_TAC;
 ASM_REWRITE_TAC[];
 MATCH_MP_TAC 
UNIONS_SUBSET;
 X_GEN_TAC `B:A->bool`;
 DISCH_TAC;
 SUBGOAL_TAC `(B:A->bool) 
IN open_balls (X,d)`;
 ASM SET_TAC[];
 REWRITE_TAC[open_balls;
IN_ELIM_THM];
 DISCH_THEN (CHOOSE_THEN MP_TAC);
 DISCH_THEN (CHOOSE_THEN ASSUME_TAC);
 ASM_REWRITE_TAC[];
 REWRITE_TAC[open_ball;
SUBSET;
IN_ELIM_THM];
 MESON_TAC[
IN];
 ]);;
 
let top_of_metric_nbd = prove_by_refinement(
 `!(X:A->bool) d A. (metric_space (X,d)) ==>
     ((top_of_metric (X,d) A) <=> ((A 
SUBSET X) /\
    (!a. (a 
IN A) ==>
    (?r. (&.0 <. r) /\ (open_ball(X,d) a r 
SUBSET A)))))`,
(* {{{ proof *)
 [
 (DISCH_ALL_TAC);
 EQ_TAC;
 REWRITE_TAC[top_of_metric;
IN_ELIM_THM];
 DISCH_THEN (CHOOSE_THEN MP_TAC);
 DISCH_ALL_TAC;
 CONJ_TAC;
 IMP_RES_THEN ASSUME_TAC 
top_of_metric_unions;
 ASM_REWRITE_TAC[];
 IMP_RES_THEN ASSUME_TAC 
top_of_metric_open;
 ASM ONCE_REWRITE_TAC[];
 MATCH_MP_TAC 
UNIONS_UNIONS;
 ASM_MESON_TAC[
SUBSET_TRANS;
top_of_metric_open_balls];
 DISCH_ALL_TAC THEN (ASM_REWRITE_TAC[]);
 REWRITE_TAC[
IN_UNIONS;
UNIONS_SUBSET];
 UNDISCH_FIND_TAC `(
IN)`;
 ASM_REWRITE_TAC[];
 REWRITE_TAC[
IN_UNIONS];
 DISCH_THEN (CHOOSE_THEN ASSUME_TAC);
 SUBGOAL_TAC `(t 
IN open_balls (X:A->bool,d))`;
 ASM_MESON_TAC[
SUBSET];
 REWRITE_TAC[open_balls;
IN_ELIM_THM];
 REPEAT (DISCH_THEN (CHOOSE_THEN MP_TAC));
 DISCH_TAC;
 MP_TAC (SPECL[`(X:A->bool)`; `d:A->A->real`;`a:A`;`x:A`;`r:real`] 
open_ball_center);
 ASM_REWRITE_TAC[];
 SUBGOAL_TAC `(a:A) 
IN open_ball(X,d) x r`;
 ASM_MESON_TAC[];
 DISCH_TAC THEN (ASM_REWRITE_TAC[]);
 DISCH_THEN CHOOSE_TAC;
 EXISTS_TAC `r':real`;
 ASM_REWRITE_TAC[];
 (* to here *)
 SUBGOAL_TAC `!s. ((s:A->bool) 
IN F') ==> (s 
SUBSET (
UNIONS F'))`;
 SET_TAC[];
 ASM_MESON_TAC[
SUBSET_TRANS] ; (*second direction: *)
 DISCH_THEN (fun t -> ASSUME_TAC (CONJUNCT1 t) THEN MP_TAC (CONJUNCT2 t));
 DISCH_THEN (fun t -> MP_TAC (REWRITE_RULE[
RIGHT_IMP_EXISTS_THM] t));
 REWRITE_TAC[
SKOLEM_THM];
 DISCH_THEN CHOOSE_TAC;
 REWRITE_TAC[top_of_metric;
IN_ELIM_THM];
 EXISTS_TAC `
IMAGE (\b. (open_ball(X,d) b (r b))) (A:A->bool)`;
 CONJ_TAC;
 REWRITE_TAC[
IMAGE;
SUBSET];
 REWRITE_TAC[
IN_ELIM_THM;open_balls];
 MESON_TAC[
IN];
 REWRITE_TAC[
IMAGE];
 GEN_REWRITE_TAC I [
EXTENSION];
 X_GEN_TAC `a:A`;
 REWRITE_TAC[
IN_UNIONS];
 REWRITE_TAC[
IN_ELIM_THM];
 EQ_TAC;
 DISCH_TAC;
 EXISTS_TAC `open_ball (X,d) (a:A) (r a)`;
 CONJ_TAC;
 EXISTS_TAC `a:A`;
 ASM_REWRITE_TAC[];
 REWRITE_TAC[
IN;open_ball];
 REWRITE_TAC[
IN_ELIM_THM];
 ASM_MESON_TAC[
metric_space_zero;
IN;
SUBSET];  (* last: *)
 DISCH_THEN (CHOOSE_THEN MP_TAC);
 DISCH_ALL_TAC;
 UNDISCH_FIND_TAC `(?)` ;
 DISCH_THEN (CHOOSE_THEN MP_TAC);
 DISCH_ALL_TAC;
 UNDISCH_FIND_TAC `(!)`;
 DISCH_THEN (fun t -> MP_TAC(SPEC `x:A` t));
 ASM_REWRITE_TAC[];
 DISCH_ALL_TAC;
 ASM_MESON_TAC[
SUBSET;
IN];
 ]);;
 
let top_of_metric_inter = prove_by_refinement(
 `!(X:A->bool) d. (metric_space (X,d)) ==>
   (!A B. (top_of_metric (X,d) A) /\ (top_of_metric (X,d) B) ==>
      (top_of_metric (X,d) (A 
INTER B)))`,
(* {{{ proof *)
 [
 DISCH_ALL_TAC;
 DISCH_ALL_TAC;
 IMP_RES_THEN ASSUME_TAC (SPECL [`X:A->bool`;`d:A->A->real`] 
top_of_metric_nbd);
 UNDISCH_TAC `(top_of_metric (X,d) (B:A->bool))`;
 UNDISCH_TAC `(top_of_metric (X,d) (A:A->bool))`;
 ASM_REWRITE_TAC[];
 DISCH_ALL_TAC;
 DISCH_ALL_TAC;
 CONJ_TAC;
 ASM SET_TAC[];
 DISCH_ALL_TAC;
 UNDISCH_FIND_THEN `(
INTER)` (fun t-> (MP_TAC (REWRITE_RULE[
IN_INTER]t)) THEN DISCH_ALL_TAC );
 UNDISCH_FIND_THEN `(
IN)` (fun t-> ANTE_RES_THEN MP_TAC t);
 UNDISCH_FIND_THEN `(
IN)` (fun t-> ANTE_RES_THEN MP_TAC t);
 DISCH_THEN CHOOSE_TAC;
 DISCH_THEN CHOOSE_TAC;
 EXISTS_TAC `if (r<. r') then r else r'`;
 COND_CASES_TAC;
 ASM_REWRITE_TAC[
SUBSET_INTER];
 ASM_MESON_TAC[
open_ball_nest;
SUBSET_TRANS];
 MP_TAC (ARITH_RULE `~(r<.r') ==> ((r'<. r) \/ (r'=r))`) THEN (ASM_REWRITE_TAC[]);
 DISCH_THEN DISJ_CASES_TAC;
 ASM_REWRITE_TAC[
SUBSET_INTER];
 ASM_MESON_TAC[
open_ball_nest;
SUBSET_TRANS];
 ASM_MESON_TAC[
SUBSET_INTER];
 ]);;
 
let top_of_metric_union = prove_by_refinement(
  `!(X:A->bool) d. (metric_space(X,d)) ==>
   (!V. (V 
SUBSET top_of_metric(X,d)) ==>
      (top_of_metric(X,d) (
UNIONS V)))`,
(* {{{ proof *)
  [
  DISCH_ALL_TAC;
  MP_TAC (SPECL[`X:A->bool`;`d:A->A->real`] 
top_of_metric_nbd);
  ASM_REWRITE_TAC[];
  DISCH_THEN (fun t-> REWRITE_TAC[t]);
  DISCH_ALL_TAC;
  CONJ_TAC;
  ASM_MESON_TAC[
UNIONS_UNIONS;
top_of_metric_unions];
  GEN_TAC;
  REWRITE_TAC[
IN_UNIONS];
  DISCH_THEN (CHOOSE_THEN MP_TAC);
  DISCH_ALL_TAC;
  SUBGOAL_TAC `(top_of_metric (X,d)) (t:A->bool)`;
  ASM_MESON_TAC[
IN;
SUBSET];
  MP_TAC (SPECL[`X:A->bool`;`d:A->A->real`] 
top_of_metric_nbd);
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  ASM_REWRITE_TAC[];
  DISCH_ALL_TAC;
  UNDISCH_FIND_THEN `(!)` (fun t -> MP_TAC (SPEC `a:A` t));
  ASM_REWRITE_TAC[];
  DISCH_THEN CHOOSE_TAC;
  EXISTS_TAC `r:real`;
  ASM_REWRITE_TAC[];
  ASM SET_TAC[
UNIONS];
  ]);;
 
let closed_ball_closed = prove_by_refinement(
  `!X d (x:A) r. (metric_space (X,d)) ==>
     (closed_ (top_of_metric(X,d)) (closed_ball(X,d) x r))`,
  (* {{{ proof *)
  [
  DISCH_ALL_TAC;
  TYPE_THEN `X x`  ASM_CASES_TAC ;
  REWRITE_TAC[closed];
  ASM_SIMP_TAC [GSYM 
top_of_metric_unions];
  SUBCONJ_TAC;
  REWRITE_TAC[closed_ball;
SUBSET;
IN;IN_ELIM_THM'];
  MESON_TAC[];
  DISCH_ALL_TAC;
  REWRITE_TAC[open_DEF];
  COPY 0;
  USE 0 (MATCH_MP 
top_of_metric_top);
  ONCE_ASM_SIMP_TAC[
open_nbd];
  GEN_TAC;
  TYPE_THEN `open_ball(X,d) x' (d x x' -. r)` EXISTS_TAC;
  TYPE_THEN `R = (d x x' -. r)` ABBREV_TAC;
  DISCH_ALL_TAC;
  TYPE_THEN `X x'` SUBGOAL_TAC;
  USE 5 (REWRITE_RULE[INR 
IN_DIFF]);
  ASM_REWRITE_TAC[];
  DISCH_ALL_TAC;
  SUBCONJ_TAC;
  REWRITE_TAC[
DIFF_SUBSET;
open_ball_subset;
INTER;
EQ_EMPTY;IN_ELIM_THM'];
  X_GEN_TAC `y:A`;
  REWRITE_TAC[
IN];
  ASM_REWRITE_TAC[open_ball;closed_ball];
  REWRITE_TAC[IN_ELIM_THM';
 
let open_ball_nbd = prove_by_refinement(
  `!X d C x. ?e. (metric_space((X:A->bool),d)) /\ (C x) /\
    (top_of_metric (X,d) C) ==>
   ((&.0 < e) /\ (open_ball (X,d) x e 
SUBSET C))`,
  (* {{{ proof *)
  [
  DISCH_ALL_TAC;
  RIGHT_TAC "e";
 
let image_top = prove_by_refinement(
 `!(U:(A->bool)->bool) (f:(A->bool)->(B->bool)).
    ((topology_ U) /\ (
EMPTY = f 
EMPTY) /\
    (!a b. (a 
IN U) /\ (b 
IN U) ==>
      (((f a) 
INTER (f b)) = f (a 
INTER b))) /\
    (!V. (V 
SUBSET U) ==> (
UNIONS (
IMAGE f V) =f (
UNIONS V) )))
    ==> (topology_ (
IMAGE f U))`,
  (* {{{ proof *)
 [
 REWRITE_TAC[topology];
 DISCH_ALL_TAC;
 DISCH_ALL_TAC;
 CONJ_TAC;
 REWRITE_TAC[
IMAGE;
IN];
 REWRITE_TAC[
IN_ELIM_THM];
 ASM_MESON_TAC[];
 CONJ_TAC;
 REWRITE_TAC[
IMAGE;
IN];
 REWRITE_TAC[
IN_ELIM_THM];
 DISCH_ALL_TAC;
 REPEAT (UNDISCH_FIND_THEN `(?)` CHOOSE_TAC);
 ASM_REWRITE_TAC[];
 EXISTS_TAC `(x:A->bool) 
INTER x'`;
 ASM_SIMP_TAC[
IN];
 DISCH_THEN (fun t-> MP_TAC (MATCH_MP 
SUBSET_PREIMAGE t));
 DISCH_THEN CHOOSE_TAC;
 ASM_REWRITE_TAC[];
 ASM_SIMP_TAC[];
 REWRITE_TAC[
IMAGE;
IN_ELIM_THM];
 EXISTS_TAC `
UNIONS (Z:(A->bool)->bool)`;
 ASM_SIMP_TAC[
IN];
 ]);;
 
let induced_top_top = prove_by_refinement(
  `!U (C:A->bool). (topology_ U) ==> (topology_ (induced_top U C))`,
  (* {{{ proof *)
  [
  REPEAT GEN_TAC;
  DISCH_TAC;
  REWRITE_TAC[induced_top];
  MATCH_MP_TAC 
image_top;
  ASM_REWRITE_TAC[];
  CONJ_TAC;
  SET_TAC[];
  CONJ_TAC;
  SET_TAC[];
  REWRITE_TAC[
UNIONS_INTER];
  DISCH_ALL_TAC;
  AP_TERM_TAC;
  AP_THM_TAC;
  AP_TERM_TAC;
  MATCH_MP_TAC 
EQ_EXT THEN BETA_TAC;
  SET_TAC[];
  ]);;
 
let gen_subspace = prove_by_refinement(
  `!(X:A->bool) Y d. (Y 
SUBSET X) /\ (metric_space(X,d)) ==>
     (induced_top (top_of_metric(X,d)) Y =
         gen (induced_top (open_balls(X,d)) Y))`,
(* {{{ proof *)
  [
  DISCH_ALL_TAC;
  REWRITE_TAC[induced_top];
  REWRITE_TAC[
EXTENSION];
  X_GEN_TAC `B:A->bool`;
  REWRITE_TAC[
IN_IMAGE];
  EQ_TAC;
  DISCH_THEN (X_CHOOSE_TAC `C:A->bool`);
  FIRST_ASSUM MP_TAC;
  REWRITE_TAC[top_of_metric];
  REWRITE_TAC[
IN_ELIM_THM];
  DISCH_ALL_TAC;
  UNDISCH_FIND_TAC `(?)`;
  DISCH_THEN (CHOOSE_TAC);
  UNDISCH_FIND_TAC `(
INTER)`;
  ASM_REWRITE_TAC[
UNIONS_INTER];
  REWRITE_TAC[gen;
IN_ELIM_THM];
  EXISTS_TAC `
IMAGE ((
INTER) Y) (F':(A->bool)->bool)`;
  CONJ_TAC;
  REWRITE_TAC[
INTER_THM];
  MATCH_MP_TAC 
IMAGE_SUBSET;
  ASM_REWRITE_TAC[];
  REFL_TAC;
  REWRITE_TAC[gen;
IN_ELIM_THM];
  DISCH_THEN (CHOOSE_THEN MP_TAC);
  DISCH_ALL_TAC;
  IMP_RES_THEN MP_TAC 
SUBSET_PREIMAGE;
  DISCH_THEN CHOOSE_TAC;
  EXISTS_TAC `
UNIONS (Z:(A->bool)->bool)`;
  CONJ_TAC;
  REWRITE_TAC[
UNIONS_INTER];
  UNDISCH_FIND_THEN `(
UNIONS)` (fun t -> REWRITE_TAC[t]);
  AP_TERM_TAC;
  UNDISCH_FIND_TAC `(
SUBSET)`;
  REWRITE_TAC[
INTER_THM];
  ASM_MESON_TAC[];
  REWRITE_TAC[top_of_metric;
IN_ELIM_THM];
  ASM_MESON_TAC[];
  ]);;
 
let gen_induced = prove_by_refinement(
 `!(X:A->bool) Y d. (Y 
SUBSET X) /\ (metric_space (X,d)) ==>
    (gen (open_balls(Y,d)) = gen (induced_top (open_balls(X,d)) Y))`,
(* {{{ proof *)
 [
 DISCH_ALL_TAC;
 MATCH_MP_TAC 
gen_subset;
 CONJ_TAC;
 REWRITE_TAC[induced_top;
SUBSET;open_balls];
 REWRITE_TAC [
IN_IMAGE];
 X_GEN_TAC `A:(A->bool)`;
 REWRITE_TAC[
IN_ELIM_THM];
 REPEAT (DISCH_THEN (CHOOSE_THEN MP_TAC));
 DISCH_TAC;
 ASM_REWRITE_TAC[];
 ASM_CASES_TAC `(Y:A->bool) (x:A)`;
 CONV_TAC (relabel_bound_conv);
 EXISTS_TAC `open_ball (X,d) (x:A) r`;
 CONJ_TAC;
 MATCH_MP_TAC 
open_ball_intersect;
 ASM_MESON_TAC[
IN];
 MESON_TAC[];
 EXISTS_TAC `open_ball (X,d) (x:A) (--. (&.1))`;
 CONJ_TAC;
 ASM_MESON_TAC[
IN;
INTER_EMPTY;
open_ball_empty;
open_ball_neg_radius;REAL_ARITH `(--.(&.1) <. (&.0))`];
 MESON_TAC[];  (* end of first half *)
 REWRITE_TAC[induced_top;
IN_IMAGE];
 GEN_TAC;
 DISCH_THEN (CHOOSE_THEN MP_TAC);
 NAME_CONFLICT_TAC;
 REWRITE_TAC[
IN;open_balls];
 REWRITE_TAC[IN_ELIM_THM'];
 NAME_CONFLICT_TAC;
 DISCH_ALL_TAC;
 ASM_REWRITE_TAC[];
 FIRST_ASSUM (CHOOSE_THEN ASSUME_TAC);
 FIRST_ASSUM (CHOOSE_THEN ASSUME_TAC);
 SUBGOAL_TAC `!(a:A). (a 
IN x 
INTER Y) ==> (?r. ((&.0) <. r) /\ open_ball(Y,d) a r 
SUBSET (x 
INTER Y))`;
 DISCH_ALL_TAC;
 TYPEL_THEN [`X`;`d`;`a`;`x'`;`r'`] (fun t -> (CLEAN_ASSUME_TAC (ISPECL t 
open_ball_center)));
 SUBGOAL_TAC `(a:A) 
IN open_ball(X,d) x' r'`;
 ASM_MESON_TAC[
IN_INTER];
 DISCH_THEN (fun t -> ANTE_RES_THEN (MP_TAC) t);
 DISCH_THEN (CHOOSE_TAC);
 EXISTS_TAC `r'':real`;
 ASM_REWRITE_TAC[
SUBSET_INTER;
open_ball_subset];
 ASM_MESON_TAC[
open_ball_subspace;
SUBSET_TRANS];
 DISCH_THEN (fun t -> MP_TAC (REWRITE_RULE[
RIGHT_IMP_EXISTS_THM;
SKOLEM_THM] t));
 DISCH_THEN CHOOSE_TAC;
 EXISTS_TAC `
IMAGE (\t. open_ball(Y,d) t (r t) ) ((x:A->bool) 
INTER Y)`;
 REWRITE_TAC[
SUBSET_INTER];
 CONJ_TAC;
 REWRITE_TAC[
SUBSET;IN_ELIM_THM'];
 REWRITE_TAC[
IN_IMAGE];
 GEN_TAC;
 MESON_TAC[];
 MATCH_MP_TAC 
SUBSET_ANTISYM;
 CONJ_TAC;
 REWRITE_TAC[
SUBSET];
 GEN_TAC;
 REWRITE_TAC[
IN_UNIONS];
 DISCH_TAC;
 EXISTS_TAC `open_ball (Y,d) (x'':A) (r x'')`;
 REWRITE_TAC[
IN_IMAGE];
 CONJ_TAC;
 NAME_CONFLICT_TAC;
 EXISTS_TAC `x'':A`;
 ASM_REWRITE_TAC[];
 MATCH_MP_TAC 
open_ball_nonempty;
 ASM_SIMP_TAC[
metric_subspace];
 ASM_MESON_TAC[
IN_INTER;
IN;
metric_subspace];
 MATCH_MP_TAC 
UNIONS_SUBSET;
 GEN_TAC;
 REWRITE_TAC[
IN_IMAGE];
 DISCH_THEN CHOOSE_TAC;
 ASM_MESON_TAC[];
 ]);;
 
let metric_continuous_continuous = prove_by_refinement(
  `!f X Y dX dY. (
IMAGE f X 
SUBSET Y) /\ (metric_space(X,dX)) /\ (metric_space(Y,dY))
    ==>
   (continuous (f:A->B) (top_of_metric(X,dX)) (top_of_metric(Y,dY))
   <=> (metric_continuous f (X,dX) (Y,dY)))`,
  (* {{{ proof *)
  [
  DISCH_ALL_TAC;
  EQ_TAC;
  REWRITE_TAC[continuous;metric_continuous];
  DISCH_TAC;
  GEN_TAC;
  ASM_CASES_TAC `(x:A) 
IN X` THENL[ALL_TAC;ASM_SIMP_TAC[
metric_continuous_pt_domain]];
  REWRITE_TAC[metric_continuous_pt];
  GEN_TAC;
  SUBGOAL_TAC `(open_ball (Y,dY) ((f:A->B) x) epsilon) 
IN (top_of_metric(Y,dY))`;
  MATCH_MP_TAC (prove_by_refinement(`!(x:A) B. (?A. (x 
IN A /\ A 
SUBSET B)) ==> (x 
IN B)`,[SET_TAC[]]));
  EXISTS_TAC `open_balls((Y:B->bool),dY)`;
  REWRITE_TAC[
top_of_metric_open_balls];
  REWRITE_TAC[open_balls;IN_ELIM_THM'];
  MESON_TAC[];
  DISCH_THEN (ANTE_RES_THEN ASSUME_TAC);
  REWRITE_TAC[GSYM 
RIGHT_IMP_EXISTS_THM];
  DISCH_TAC;
  SUBGOAL_TAC `(x:A) 
IN preimage (
UNIONS (top_of_metric (X,dX))) f (open_ball (Y,dY) ((f:A->B) x) epsilon)`;
  REWRITE_TAC[
in_preimage];
  SUBGOAL_TAC `(Y:B->bool) ((f:A->B) x )`;
  UNDISCH_FIND_TAC `
IMAGE`;
  UNDISCH_TAC `(x:A) 
IN X`;
  REWRITE_TAC[
SUBSET;
IMAGE];
  REWRITE_TAC[IN_ELIM_THM'];
  NAME_CONFLICT_TAC;
  REWRITE_TAC[
IN];
  MESON_TAC[];
  ASM_MESON_TAC[
top_of_metric_unions;
open_ball_nonempty];
  ABBREV_TAC `B = preimage (
UNIONS (top_of_metric (X,dX))) (f:A->B) (open_ball (Y,dY) (f x) epsilon)`;
  DISCH_TAC;
  SUBGOAL_TAC `?r. (&.0 <. r) /\ (open_ball(X,dX) (x:A) r 
SUBSET B)`;
  ASSUME_TAC 
top_of_metric_nbd;
  ASM_MESON_TAC[
IN];
  DISCH_THEN CHOOSE_TAC;
  EXISTS_TAC `r:real`;
  ASM_REWRITE_TAC[];
  GEN_TAC;
  DISCH_ALL_TAC;
  SUBGOAL_TAC `y:A 
IN B`;
  MATCH_MP_TAC (prove_by_refinement(`!(x:A) B. (?A. (x 
IN A /\ A 
SUBSET B)) ==> (x 
IN B)`,[SET_TAC[]]));
  EXISTS_TAC `open_ball(X,dX) (x:A) r`;
  ASM_REWRITE_TAC[];
  REWRITE_TAC[open_ball;IN_ELIM_THM'];
  ASM_MESON_TAC[
IN];
  UNDISCH_FIND_TAC `preimage`;
  DISCH_THEN (fun t-> REWRITE_TAC[GSYM t]);
  REWRITE_TAC[
in_preimage];
  REWRITE_TAC[open_ball;IN_ELIM_THM'];
  MESON_TAC[]; (* first half done *)
  REWRITE_TAC[metric_continuous];
  DISCH_TAC;
  REWRITE_TAC[continuous];
  GEN_TAC;
  DISCH_TAC;
  REWRITE_TAC[
IN];
  ASM_SIMP_TAC[
top_of_metric_nbd];
  ASM_SIMP_TAC[GSYM 
top_of_metric_unions];
  CONJ_TAC;
  REWRITE_TAC[
SUBSET;
in_preimage];
  MESON_TAC[];
  GEN_TAC;
  DISCH_THEN (fun t -> ASSUME_TAC t THEN (MP_TAC (REWRITE_RULE[
in_preimage] t)));
  DISCH_ALL_TAC;
  SUBGOAL_TAC `?eps. (&.0 <. eps) /\ (open_ball(Y,dY) ((f:A->B) a) eps 
SUBSET v)`;
  UNDISCH_FIND_TAC `v 
IN top_of_metric (Y,dY)`;
  REWRITE_TAC[
IN];
  ASM_SIMP_TAC[
top_of_metric_nbd];
  DISCH_THEN CHOOSE_TAC;
  FIRST_ASSUM (fun t -> MP_TAC (SPEC `a:A` t));
  REWRITE_TAC[metric_continuous_pt];
  DISCH_THEN (fun t-> MP_TAC (SPEC `eps:real` t));
  DISCH_THEN (CHOOSE_THEN MP_TAC);
  ASM_REWRITE_TAC[];
  DISCH_ALL_TAC;
  EXISTS_TAC `delta:real`;
  ASM_REWRITE_TAC[
SUBSET];
  REWRITE_TAC[
in_preimage;open_ball];
  REWRITE_TAC[IN_ELIM_THM'];
  X_GEN_TAC `y:A`;
  DISCH_ALL_TAC;
  CONJ_TAC THENL [(ASM_REWRITE_TAC[
IN]);ALL_TAC];
  FIRST_ASSUM (fun t -> (MP_TAC (SPEC `y:A` t)));
  ASM_REWRITE_TAC[
IN];
  UNDISCH_FIND_TAC `open_ball`;
  REWRITE_TAC[open_ball];
  DISCH_THEN (fun t  -> (MP_TAC (CONJUNCT2 t)));
  REWRITE_TAC[
SUBSET];
  DISCH_THEN (fun t-> (MP_TAC (SPEC `(f:A->B) y` t)));
  ASM_REWRITE_TAC[IN_ELIM_THM'];
  SUBGOAL_TAC `!x. (X x) ==> (Y ((f:A->B) x))`;
  UNDISCH_FIND_TAC `
IMAGE`;
  REWRITE_TAC[
SUBSET;
IN_IMAGE];
  NAME_CONFLICT_TAC;
  ASM_MESON_TAC[
IN];
  ASM_MESON_TAC[
IN];
  ]);;
 
let metric_cont = prove_by_refinement(
  `!U X d f. (metric_space(X,d)) /\ (topology_ U) ==>
    ((continuous (f:A->B) U (top_of_metric(X,d))) =
      (!(x:B) r. U (preimage (
UNIONS U) f (open_ball (X,d) x r))))`,
  (* {{{ proof *)
  [
  DISCH_ALL_TAC;
  EQ_TAC;
  DISCH_ALL_TAC;
  DISCH_ALL_TAC;
  USE 2 (REWRITE_RULE[continuous;
IN]);
  UND 2 THEN (DISCH_THEN MATCH_MP_TAC );
  ASM_MESON_TAC [
open_ball_open];
  REWRITE_TAC[continuous;
IN];
  DISCH_ALL_TAC;
  REWRITE_TAC[top_of_metric;IN_ELIM_THM' ];
  DISCH_ALL_TAC;
  CHO 3;
  
AND 3;
  ASM_REWRITE_TAC[];
  REWRITE_TAC[
preimage_unions];
  IMATCH_MP_TAC  
top_unions ;
  ASM_REWRITE_TAC[
IMAGE;
SUBSET;
IN;IN_ELIM_THM' ];
  NAME_CONFLICT_TAC;
  REWRITE_TAC[Q_ELIM_THM'];
  USE 4 (REWRITE_RULE[
SUBSET;
IN]);
  DISCH_ALL_TAC;
  TYPE_THEN `x'` (USE 4 o SPEC);
  REWR 4;
  USE 4 (REWRITE_RULE[open_balls;IN_ELIM_THM' ]);
  CHO 4;
  CHO 4;
  ASM_MESON_TAC[];
  ]);;
 
let continuous_sum = prove_by_refinement(
  `!U (f:A->(num->real)) g n. (topology_ U) /\
   (continuous f U (top_of_metric(euclid n,d_euclid))) /\
   (continuous g U (top_of_metric(euclid n,d_euclid))) /\
   (
IMAGE f (
UNIONS U) 
SUBSET (euclid n)) /\
   (
IMAGE g (
UNIONS U) 
SUBSET (euclid n)) ==>
   (continuous (\t. (f t + g t))  U (top_of_metric(euclid n,d_euclid)))`,
  (* {{{ proof *)
  [
  ASSUME_TAC 
metric_euclid;
  DISCH_ALL_TAC;
  ASM_SIMP_TAC[
metric_cont];
  DISCH_ALL_TAC;
  ONCE_ASM_SIMP_TAC[
open_nbd];
  X_GEN_TAC `t:A`;
  RIGHT_TAC "B";
 
let converge_cauchy = prove_by_refinement(
  `!X d f. metric_space(X,d) /\ (sequence X f) /\ (converge((X:A->bool),d) f)
    ==> cauchy_seq(X,d) f`,
  (* {{{ proof *)
  [
  REWRITE_TAC[converge;metric_space];
  DISCH_ALL_TAC;
  REWRITE_TAC[cauchy_seq];
  ASM_REWRITE_TAC[];
  FIRST_ASSUM CHOOSE_TAC;
  GEN_TAC;
  UNDISCH_FIND_TAC `(
IN)`;
  DISCH_ALL_TAC;
  FIRST_ASSUM (fun t-> MP_TAC (SPEC `eps/(&.2)` t));
  DISCH_THEN CHOOSE_TAC;
  EXISTS_TAC `n:num`;
  REPEAT GEN_TAC;
  DISCH_ALL_TAC;
  SUBGOAL_TAC ` (&.0 <. (eps/(&.2)))`;
  MATCH_MP_TAC 
REAL_LT_DIV;
  ASM_REWRITE_TAC[];
  REAL_ARITH_TAC;
  DISCH_THEN (ANTE_RES_THEN ASSUME_TAC);
  UNDISCH_TAC `n <=| i`;
  DISCH_THEN (ANTE_RES_THEN ASSUME_TAC);
  UNDISCH_TAC `n <=| j`;
  DISCH_THEN (ANTE_RES_THEN ASSUME_TAC);
  FIRST_ASSUM (fun t-> MP_TAC (SPECL [`(f:num->A) i`;`x:A`;`(f:num->A) j`] t));
  UNDISCH_FIND_TAC `sequence`;
  REWRITE_TAC[sequence;
SUBSET;
IN_IMAGE;
IN_UNIV];
  NAME_CONFLICT_TAC;
  REWRITE_TAC[
IN];
  DISCH_TAC;
  SUBGOAL_TAC `X ((f:num->A) i) /\ X x /\ X (f j)`;
  ASM_MESON_TAC[
IN];
  DISCH_THEN (fun t->REWRITE_TAC[t]);
  DISCH_ALL_TAC;
  ASM_MESON_TAC[
REAL_LET_TRANS;
REAL_LT_ADD2;
REAL_HALF_DOUBLE];
  ]);;
 
let cauchy_seq_cauchy = prove_by_refinement(
  `!f. (cauchy_seq(euclid 1,d_euclid) f) ==> (cauchy (\x. (f x 0)))`,
  (* {{{ proof *)
  [
  GEN_TAC;
  REWRITE_TAC[cauchy_seq;cauchy;sequence;
SUBSET;
IN_IMAGE;
IN_UNIV];
  REWRITE_TAC[
IN];
  NAME_CONFLICT_TAC;
  DISCH_ALL_TAC;
  GEN_TAC;
  DISCH_TAC;
  FIRST_ASSUM (fun t -> MP_TAC (SPEC `e':real` t));
  DISCH_THEN CHOOSE_TAC;
  EXISTS_TAC `n':num`;
  REPEAT GEN_TAC;
  REWRITE_TAC[ARITH_RULE `a >=| b <=> b <=| a`];
  SUBGOAL_TAC `euclid 1 (f (m':num)) /\ euclid 1 (f (n'':num))`;
  ASM_MESON_TAC[];
  ASM_MESON_TAC[
euclid1_abs];
  ]);;
 
let complete_real = prove_by_refinement(
  `complete (euclid 1,d_euclid)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[complete;converge];
  GEN_TAC;
  DISCH_THEN (fun t-> ASSUME_TAC t THEN MP_TAC t);
  DISCH_THEN (fun t -> MP_TAC (MATCH_MP 
cauchy_seq_cauchy t));
  REWRITE_TAC[
SEQ_CAUCHY;
SEQ_LIM;
tends_num_real;
SEQ_TENDS];
  ABBREV_TAC `z = lim (\x. f x 0)`;
  REWRITE_TAC[
MR1_DEF];
  DISCH_TAC;
  ABBREV_TAC `c = \j. (if (j=0) then (z:real) else (&.0))`;
  EXISTS_TAC `(c:num->real)`;
  SUBGOAL_TAC `c 
IN (euclid 1)`;
  REWRITE_TAC[
IN;euclid];
  EXPAND_TAC "c";
 
let proj_cauchy = prove_by_refinement(
  `!i f n. cauchy_seq (euclid n,d_euclid) f ==>
     (cauchy_seq (euclid 1,d_euclid) ((proj i) o f))`,
  (* {{{ proof *)
  [
  REWRITE_TAC[cauchy_seq];
  DISCH_ALL_TAC;
  SUBGOAL_TAC `sequence (euclid 1) (proj (i:num) o f)`;
  REWRITE_TAC[sequence;
SUBSET;
IN_IMAGE;
o_DEF;
IN_UNIV];
  NAME_CONFLICT_TAC;
  MESON_TAC[
IN;
proj_euclid1];
  DISCH_TAC;
  ASM_REWRITE_TAC[];
  GEN_TAC;
  FIRST_ASSUM (fun t -> CHOOSE_TAC (SPEC `eps:real` t));
  EXISTS_TAC `n':num`;
  DISCH_ALL_TAC;
  FIRST_ASSUM (fun t-> MP_TAC(SPECL [`i':num`;`j:num`] t));
  UNDISCH_FIND_THEN `d_euclid` (fun t-> ALL_TAC);
  ASM_REWRITE_TAC[];
  MATCH_MP_TAC (REAL_ARITH `a <=. b ==> (b <. eps ==> a <. eps)`);
  REWRITE_TAC[
o_DEF;
proj_d_euclid];
  MATCH_MP_TAC 
proj_contraction;
  EXISTS_TAC `n:num`;
  ASM_MESON_TAC[
sequence_in];
  ]);;
 
let complete_euclid = prove_by_refinement(
  `!n. complete (euclid n,d_euclid)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[complete;
IN];
  REPEAT GEN_TAC;
  DISCH_ALL_TAC;
  IMP_RES_THEN MP_TAC 
proj_cauchy;
  DISCH_TAC;
  SUBGOAL_TAC `!i. converge (euclid 1,d_euclid) (proj i o f)`;
  GEN_TAC;
  ASM_MESON_TAC[complete;
complete_real];
  REWRITE_TAC[converge;
IN];
  DISCH_THEN (fun t-> MP_TAC (ONCE_REWRITE_RULE[
SKOLEM_THM] t));
  DISCH_THEN (X_CHOOSE_TAC `L:num->(num->real)`);
  EXISTS_TAC `(\j. ((L:num->num->real) j 0))`;
  SUBCONJ_TAC;
  REWRITE_TAC[euclid];
  GEN_TAC;
  FIRST_ASSUM (fun t->(MP_TAC (SPEC `m:num` t)));
  DISCH_ALL_TAC;
  FIRST_ASSUM (fun t-> (MP_TAC (SPEC `abs((L:num->num->real) m 0)` t)));
  DISCH_THEN CHOOSE_TAC;
  PROOF_BY_CONTR_TAC;
  ASSUME_TAC (REAL_ARITH `!x. ~(x=(&.0)) ==> (&.0 <. abs(x))`);
  UNDISCH_FIND_TAC `d_euclid`;
  ASM_SIMP_TAC[];
  REWRITE_TAC[GSYM 
EXISTS_NOT_THM];
  EXISTS_TAC `(n:num)+n'`;
  REWRITE_TAC[
o_DEF];
  REWRITE_TAC[ARITH_RULE `n' <=| n+| n'`];
  MATCH_MP_TAC(REAL_ARITH `(x = y) ==> ~(x<y)`);
  ALL_TAC; (* #buffer "CE1"; *)
  SUBGOAL_TAC `euclid 1 (proj m (f (n +| n')))`;
  REWRITE_TAC[
proj_euclid1];
  ASM_SIMP_TAC[
euclid1_abs];
  DISCH_TAC;
  MATCH_MP_TAC (REAL_ARITH `(&.0 = x) ==> (abs(u - x) = abs(u))`);
  REWRITE_TAC[proj];
  SUBGOAL_TAC `euclid n (f (n+| n'))`;
  ASM_MESON_TAC[cauchy_seq;
sequence_in];
  REWRITE_TAC[euclid];
  DISCH_THEN (fun t->  ASM_SIMP_TAC[t]);
  ALL_TAC; (* #buffer "CE2"; *)
  DISCH_TAC;
  GEN_TAC;
  CONV_TAC (quant_right_CONV "n");
  DISCH_TAC;
  USE 2 (CONV_RULE (quant_left_CONV "eps"));
  USE 2 (CONV_RULE (quant_left_CONV "eps"));
  USE 2 (SPEC `eps/(&.1 +. &. n)`);
  USE 2 (CONV_RULE (quant_left_CONV "n'"));
  USE 2 (CONV_RULE (quant_left_CONV "n'"));
  CHO 2;
  SUBGOAL_TAC `&.0 <. eps/ (&.1 +. &.n)`;
  MATCH_MP_TAC 
REAL_LT_DIV;
  ASM_REWRITE_TAC[REAL_OF_NUM_ADD;
REAL_OF_NUM_LT];
  ARITH_TAC;
  DISCH_THEN (fun t-> (USE 2 (REWRITE_RULE[t])));
  SUBGOAL_TAC `!i j. euclid 1 ((proj i o f) (j:num))`;
  ASM_MESON_TAC[cauchy_seq;
sequence_in];
  DISCH_TAC;
  SUBGOAL_TAC `!i. euclid n (f (i:num))`;
  GEN_TAC;
  ASM_MESON_TAC[cauchy_seq;
sequence_in];
  DISCH_TAC;
  ASM_SIMP_TAC[
d_euclid_n];
  SUBGOAL_TAC `!(j:num). ?c. !i. (c <=| i) ==> ||. (L j 0 -. f i j) <. eps/(&.1 + &. n)`;
  CONV_TAC (quant_left_CONV "c");
  EXISTS_TAC `n':num->num`;
  REPEAT GEN_TAC;
  USE 2 ((SPEC `j:num`));
  UND 2;
  DISCH_ALL_TAC;
  USE 8 (SPEC `i:num`);
  UND 8;
  ASM_REWRITE_TAC[];
  ASM_SIMP_TAC[
euclid1_abs];
  REWRITE_TAC[proj;
o_DEF];
  CONV_TAC (quant_left_CONV "c");
  DISCH_THEN CHOOSE_TAC;
  ABBREV_TAC `t = (\u. (if (u <| n) then (c u) else (0)))`;
  SUBGOAL_TAC `?M. (!j. (t:num->num) j <=| M)`;
  MATCH_MP_TAC 
max_num_sequence;
  EXISTS_TAC `n:num`;
  GEN_TAC;
  EXPAND_TAC "t";
 
let complete_closed = prove_by_refinement(
  `!n S. (closed_ (top_of_metric (euclid n,d_euclid)) S) /\
    (S 
SUBSET (euclid n)) ==>
     (complete (S,d_euclid))`,
  (* {{{ proof *)
  [
  REWRITE_TAC[complete];
  REPEAT GEN_TAC;
  DISCH_ALL_TAC;
  GEN_TAC;
  DISCH_TAC;
  USE 0 (MATCH_MP 
closed_open);
  UND 0;
  SIMP_TAC[GSYM 
top_of_metric_unions;
metric_euclid];
  DISCH_TAC;
  SUBGOAL_TAC `cauchy_seq(euclid n,d_euclid) f`;
  ASM_MESON_TAC[
subset_cauchy];
  DISCH_TAC;
  SUBGOAL_TAC `converge(euclid n,d_euclid) f`;
  ASM_MESON_TAC[
complete_euclid;complete];
  REWRITE_TAC[converge];
  DISCH_THEN CHOOSE_TAC;
  EXISTS_TAC `(x:num->real)`;
  ASM_REWRITE_TAC[];
  PROOF_BY_CONTR_TAC;
  SUBGOAL_TAC `~(x 
IN S) ==> (x 
IN (euclid n 
DIFF S))`;
  ASM SET_TAC[];
  DISCH_TAC;
  H_MATCH_MP (HYP "6") (HYP "5");
  USE 0 (REWRITE_RULE[open_DEF]);
  USE 0 (REWRITE_RULE[(MATCH_MP (CONV_RULE (quant_right_CONV "A") 
top_of_metric_nbd) (SPEC `n:num` 
metric_euclid))]);
  USE 0 (CONV_RULE (quant_left_CONV "a"));
  USE 0 (SPEC `x:num->real`);
  UND 0;
  ASM_REWRITE_TAC[
SUBSET_DIFF];
  ALL_TAC; (* #CC1; *)
  PROOF_BY_CONTR_TAC;
  USE 0 (REWRITE_RULE[]);
  CHO 0;
  USE 0 (REWRITE_RULE[
SUBSET;IN_ELIM_THM';
 
let totally_bounded_subset = prove_by_refinement(
  `!(X:A->bool) d S. (metric_space (X,d)) /\ (totally_bounded(X,d))
      /\ (S 
SUBSET X)  ==>
     (totally_bounded (S,d)) `,
  (* {{{ proof *)
  [
  REPEAT GEN_TAC;
  REWRITE_TAC[totally_bounded];
  DISCH_ALL_TAC;
  GEN_TAC;
  USE 1 (SPEC `eps/(&.2)`);
  CHO 1;
  CONV_TAC (quant_right_CONV "B");
  DISCH_TAC;
  SUBGOAL_TAC `&.0 <. eps ==> &.0 <. eps/(&.2)`;
  DISCH_THEN (fun t-> MP_TAC (ONCE_REWRITE_RULE[GSYM 
REAL_HALF_DOUBLE] t));
  REWRITE_TAC[
REAL_DIV_LZERO];
  REAL_ARITH_TAC;
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  (UND 1) THEN (ASM_REWRITE_TAC[]) THEN DISCH_ALL_TAC;
  SUBGOAL_TAC `!b. ?s. (?t. (t 
IN (b:A->bool) 
INTER S)) ==> (s 
IN b 
INTER S)`;
  GEN_TAC;
  CONV_TAC (quant_left_CONV "t");
  MESON_TAC[
IN];
  CONV_TAC (quant_left_CONV "s");
  DISCH_THEN CHOOSE_TAC;
  ALL_TAC; (* #set "TB1"; *)
  EXISTS_TAC `
IMAGE (\c. (open_ball ((S:A->bool),d) ((s) c) eps)) (B:(A->bool)->bool)`;
  CONJ_TAC;
  MATCH_MP_TAC 
FINITE_IMAGE;
  ASM_REWRITE_TAC[];
  CONJ_TAC;
  GEN_TAC;
  REWRITE_TAC[
IMAGE;IN_ELIM_THM'];
  NAME_CONFLICT_TAC;
  DISCH_THEN (X_CHOOSE_TAC `c:A->bool`);
  ASM_MESON_TAC[];
  MATCH_MP_TAC 
EQ_EXT;
  X_GEN_TAC `u:A`;
  EQ_TAC;
  DISCH_TAC;
  SUBGOAL_TAC `(X:A->bool) (u:A)`;
  ASM_MESON_TAC[
SUBSET;
IN];
  ASM_REWRITE_TAC[];
  REWRITE_TAC[REWRITE_RULE[
IN] 
IN_UNIONS];
  DISCH_THEN (X_CHOOSE_TAC `b':A->bool`);
  USE 7 (SPEC `b':A->bool`);
  REWRITE_TAC[
IMAGE];
  REWRITE_TAC[IN_ELIM_THM'];
  CONV_TAC (quant_left_CONV "x");
  CONV_TAC (quant_left_CONV "x");
  EXISTS_TAC `b':A->bool`;
  EXISTS_TAC `open_ball((S:A->bool),d) (s (b':A->bool)) eps`;
  ASM_REWRITE_TAC[
IN];
  REWRITE_TAC[open_ball];
  REWRITE_TAC[IN_ELIM_THM'];
  ALL_TAC; (* #set "TB2"; *)
  SUBGOAL_TAC `(u:A) 
IN (b' 
INTER S)`;
  REWRITE_TAC[
IN_INTER];
  ASM_MESON_TAC[
IN];
  UND 7;
  CONV_TAC (quant_left_CONV "t");
  CONV_TAC (quant_left_CONV "t");
  EXISTS_TAC `u:A`;
  DISCH_TAC;
  DISCH_TAC;
  SUBGOAL_TAC `(S:A->bool) ((s:(A->bool)->A) b')`;
  UND 7;
  ASM_REWRITE_TAC[];
  REWRITE_TAC[
IN_INTER];
  MESON_TAC[
IN];
  DISCH_TAC;
  ASM_REWRITE_TAC[];
  SUBGOAL_TAC `(b':A->bool) ((s:(A->bool)->A) b')`;
  UND 11;
  UND 7;
  REWRITE_TAC[
IN_INTER];
  ASM_MESON_TAC[
IN];
  ALL_TAC; (* #set "TB3"; *)
  DISCH_TAC;
  
AND 9;
  USE 5 (SPEC `b':A->bool`);
  H_MATCH_MP (HYP "5") (HYP "13");
  CHO 14;
  ABBREV_TAC `v = (s:(A->bool)->A) b'`;
  COPY 9;
  UND 9;
  UND 12;
  ASM_REWRITE_TAC[];
  REWRITE_TAC[open_ball;IN_ELIM_THM'];
  DISCH_ALL_TAC;
  SUBGOAL_TAC `(X x) /\ ((X:A->bool) u) /\ (X v)`;
  ASM_REWRITE_TAC[];
  ASM_MESON_TAC[
SUBSET;
IN];
  DISCH_ALL_TAC;
  USE 0 (REWRITE_RULE[metric_space]);
  COPY 16;
  KILL 1;
  KILL 7;
  KILL 11;
  UND 21;
  KILL 6;
  UND 14;
  DISCH_THEN (fun t-> ASSUME_TAC t THEN (REWRITE_TAC[t]));
  REWRITE_TAC[open_ball;IN_ELIM_THM'];
  DISCH_ALL_TAC;
  USE 0 (SPECL [`v:A`;`x:A`;`u:A`]);
  UND 0;
  ASM_REWRITE_TAC[];
  DISCH_ALL_TAC;
  USE 22 (MATCH_MP (REAL_ARITH `(a <=. b + c) ==> !e. (b + c <. e ==> (a <. e))`));
  USE 22 (SPEC `eps:real`);
  UND 22 THEN (DISCH_THEN (MATCH_MP_TAC));
  ASM_REWRITE_TAC[];
  UND 11;
  UND 17;
  MP_TAC (SPEC `eps:real` 
REAL_HALF_DOUBLE);
  REAL_ARITH_TAC;
  REWRITE_TAC[
IMAGE;IN_ELIM_THM'];
  REWRITE_TAC[
UNIONS;IN_ELIM_THM'];
  CONV_TAC (quant_left_CONV "x");
  CONV_TAC (quant_left_CONV "x");
  NAME_CONFLICT_TAC;
  CONV_TAC (quant_left_CONV "x'");
  X_GEN_TAC `c:A->bool`;
  CONV_TAC (quant_left_CONV "u'");
  GEN_TAC;
  DISCH_ALL_TAC;
  UND 10;
  ASM_REWRITE_TAC[];
  REWRITE_TAC[open_ball;IN_ELIM_THM'];
  MESON_TAC[];
  ]);;
 
let integer_cube_finite = prove_by_refinement(
  `!n N. 
FINITE { f | (euclid n f) /\
       (!i. (?j. (abs(f i) = &.j) /\ (j <=| N)))}`,
  (* {{{ proof *)
  [
  REP_GEN_TAC;
  ABBREV_TAC `fs = 
FUN {m | m <| n} {x |  ?j. (abs x = &.j) /\ (j <=| N)}`;
  ABBREV_TAC `gs = { f | (euclid n f) /\ (!i. (?j. (abs(f i) = &.j) /\ (j <=| N)))}`;
  SUBGOAL_TAC `
FINITE (fs:(num->real)->bool)`;
  EXPAND_TAC "fs";
 
let totally_bounded_cube = prove_by_refinement(
  `!n N. totally_bounded
        ({x | euclid n x /\ (!i. abs(x i) <=. (&.N))},d_euclid)`,
  (* {{{ proof *)
  [
  REP_GEN_TAC;
  REWRITE_TAC[totally_bounded];
  GEN_TAC;
  CONV_TAC (quant_right_CONV "B");
  DISCH_TAC;
  ABBREV_TAC `cent = {x | euclid n x /\ (!i. (?j. abs(x i) = (eps/(&.n+. &.1))*(&.j)) /\ (abs(x i) <=. (&.N) ) ) }`;
  SUBGOAL_TAC `&.0 <. (&.n +. &.1)`;
  REDUCE_TAC;
  ARITH_TAC;
  DISCH_TAC;
  ABBREV_TAC `s = eps/(&.n +. &.1)`;
  SUBGOAL_TAC `&.0 < s`;
  EXPAND_TAC "s";
 
let center_FINITE = prove_by_refinement(
  `!X d  . metric_space ((X:A->bool),d) /\ (totally_bounded (X,d))
   ==> (!eps. (&.0 < eps) ==> (?C. (C 
SUBSET X) /\ (
FINITE C) /\ (X = 
UNIONS (
IMAGE (\x. open_ball(X,d) x eps) C))))`,
  (* {{{ proof *)
  [
  REWRITE_TAC[totally_bounded];
  DISCH_ALL_TAC;
  DISCH_ALL_TAC;
  USE 1 (SPEC `eps:real`);
  CHO 1;
  REWR 1;
  
AND 1;
  
AND 1;
  USE 4 (CONV_RULE ((quant_left_CONV "x")));
  USE 4 (CONV_RULE ((quant_left_CONV "x")));
  CHO 4;
  ABBREV_TAC `C'={z | (X (z:A)) /\ (?b. (B (b:A->bool)) /\ (z = x b))}`;
  EXISTS_TAC `C':A->bool`;
  SUBCONJ_TAC;
  EXPAND_TAC"C'";
 
let open_ball_dist = prove_by_refinement(
  `!X d x y r. (open_ball(X,d) x r y) ==> (d (x:A) y <. r)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[open_ball;IN_ELIM_THM'];
  DISCH_ALL_TAC;
  ASM_REWRITE_TAC[];
  ]);;
 
let totally_bounded_bounded = prove_by_refinement(
  `!(X:A->bool) d. metric_space(X,d) /\ totally_bounded (X,d) ==>
    (?a r. X 
SUBSET (open_ball(X,d) a r))`,
  (* {{{ proof *)
  [
  DISCH_ALL_TAC;
  COPY 0;
  JOIN 0 1;
  USE 0 (MATCH_MP 
center_FINITE);
  USE 0 (SPEC `&.1`);
  USE 0 (CONV_RULE REDUCE_CONV);
  CHO 0;
  EXISTS_TAC `
CHOICE (X:A->bool)`;
  ASM_CASES_TAC `(X:A->bool) = 
EMPTY`;
  ASM_REWRITE_TAC[
EMPTY_SUBSET];
  USE 1 (MATCH_MP 
CHOICE_DEF);
  UND 0 THEN DISCH_ALL_TAC;
  ABBREV_TAC `(dset:real->bool) = 
IMAGE (\c. (d (
CHOICE (X:A->bool)) (c:A))) C`;
  SUBGOAL_TAC `
FINITE (dset:real->bool)`;
  EXPAND_TAC"dset";
 
let subsequence_rec = prove_by_refinement(
  `!(X:A->bool) d f C s n r.
   metric_space(X,d) /\ (totally_bounded(X,d)) /\ (sequence X f) /\
   (C 
SUBSET X) /\ (&.0 < r) /\
   (~FINITE{j| C (f j)} /\ C(f s) /\ (!x y. (C x /\ C y) ==>
       d x y <. r*twopow(--: (&:n)))) ==>
   (? C' s'. ((C' 
SUBSET C) /\ (s < s') /\
   (~FINITE{j| C' (f j)} /\ C'(f s') /\ (!x y. (C' x /\ C' y) ==>
        d x y <. r*twopow(--: (&:(SUC n)))))))`,
  (* {{{ proof *)
  [
  DISCH_ALL_TAC;
  USE 1 (REWRITE_RULE[totally_bounded]);
  USE 1 (SPEC `r*twopow(--: (&:(n+| 2)))`);
  CHO 1;
  ASSUME_TAC 
twopow_pos;
  USE 8 (SPEC `--: (&: (n+| 2))`);
  ALL_TAC; (* ## need a few lines here to match Z8 with Z1. *)
  COPY 4;
  JOIN 9 8;
  USE 8 (MATCH_MP 
REAL_LT_MUL);
  REWR 1;
  UND 1 THEN DISCH_ALL_TAC;
  ALL_TAC ; (* "sr1"  OK TO HERE *)
  ASSUME_TAC (ISPECL [`UNIV:num->bool`;`f:num->A`;`B:(A->bool)->bool`;`C:A->bool`] 
INFINITE_PIGEONHOLE);
  UND 11;
  ASM_SIMP_TAC[
UNIV];
  H_REWRITE_RULE[HYP "10"] (HYP "3");
  ASM_REWRITE_TAC [];
  DISCH_THEN CHOOSE_TAC;
  EXISTS_TAC `C 
INTER (b:A->bool)`;
  CONV_TAC (quant_right_CONV "s'");
  SUBCONJ_TAC;
  REWRITE_TAC[
INTER_SUBSET];
  DISCH_TAC;
  
AND 12;
  ASM_REWRITE_TAC[];
  SUBGOAL_TAC `~(
FINITE ({i | (C 
INTER b) ((f:num->A) i)} 
INTER {i | s <| i}))`;
  PROOF_BY_CONTR_TAC;
  (USE 15) (REWRITE_RULE[]);
  USE 15 (MATCH_MP 
num_above_finite);
  UND 12;
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  ABBREV_TAC `J = ({i | (C 
INTER b) ((f:num->A) i)} 
INTER {i | s <| i})`;
  EXISTS_TAC `
CHOICE (J:num->bool)`; (* ok to here *)
  SUBGOAL_TAC `J (
CHOICE (J:num->bool))`;
  MATCH_MP_TAC (REWRITE_RULE [
IN] 
CHOICE_DEF);
  PROOF_BY_CONTR_TAC;
  USE 17 (REWRITE_RULE[]);
  H_REWRITE_RULE[(HYP "17")] (HYP "15");
  UND 18;
  REWRITE_TAC[
FINITE_RULES];
  ALL_TAC; (* "sr2" *)
  ABBREV_TAC `s' = (
CHOICE (J:num->bool))`;
  EXPAND_TAC "J";
 
let cauchy_subseq = prove_by_refinement(
  `!(X:A->bool) d f. ((metric_space(X,d))/\(totally_bounded(X,d)) /\
        (sequence X f)) ==>
     (?ss. (subseq ss) /\ (cauchy_seq(X,d) (f o ss)))`,
  (* {{{ proof *)
  [
  DISCH_ALL_TAC;
  COPY 0 THEN COPY 1;
  JOIN 4 3;
  USE 3 (MATCH_MP 
totally_bounded_bounded);
  CHO 3;
  CHO 3;
  ALL_TAC; (* {{{ xxx *)
  ALL_TAC; (* make r pos *)
  ASSUME_TAC (REAL_ARITH `r <. (&.1 + abs(r))`);
  ASSUME_TAC (REAL_ARITH `&.0 <. (&.1 + abs(r))`);
  ABBREV_TAC (`r' = &.1 +. abs(r)`);
  SUBGOAL_TAC `open_ball(X,d) a r 
SUBSET open_ball(X,d) (a:A) r'`;
  ASM_SIMP_TAC[
open_ball_nest];
  DISCH_TAC;
  JOIN 3 7;
  USE 3 (MATCH_MP 
SUBSET_TRANS);
  KILL 6;
  KILL 4;
  ALL_TAC; (* "cs1" *)
  SUBGOAL_TAC `( !(x:A) y.  (X x) /\ (X y) ==> (d x y <. &.2 *. r'))`;
  DISCH_ALL_TAC;
  USE 3 (REWRITE_RULE[
SUBSET;
IN]);
  COPY 3;
  USE 7 (SPEC `x:A`);
  USE 3 (SPEC `y:A`);
  H_MATCH_MP (HYP "3") (HYP "6");
  H_MATCH_MP (HYP "7") (HYP "4");
  JOIN 9 8;
  JOIN 0 8;
  USE 0 (MATCH_MP 
BALL_DIST);
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  ABBREV_TAC `cond = (\ ((C:A->bool),(s:num)) n. ~FINITE{j| C (f j)} /\ (C(f s)) /\ (!x y. (C x /\ C y) ==> d x y <. (&.2*.r')*. twopow(--: (&:n))))`;
  ABBREV_TAC `R = (&.2)*r'`;
  ALL_TAC ; (* 0 case of recursio *)
  ALL_TAC; (* cs2 *)
  SUBGOAL_TAC ` (X 
SUBSET X) /\ (cond ((X:A->bool),0) 0)`;
  REWRITE_TAC[
SUBSET_REFL];
  EXPAND_TAC "cond";
 
let convergent_subseq = prove_by_refinement(
  `!(X:A->bool) d f. metric_space(X,d) /\ (totally_bounded(X,d)) /\
     (complete (X,d)) /\ (sequence X f)  ==>
     ((?(ss:num->num). (subseq ss) /\ (converge (X,d) (f o ss))))`,
  (* {{{ proof *)
  [
  DISCH_ALL_TAC;
    TYPE_THEN `?ss. (subseq ss) /\ (cauchy_seq(X,d) (f o ss))` SUBGOAL_TAC;
  ASM_MESON_TAC[
cauchy_subseq];
  DISCH_ALL_TAC;
  CHO 4;
  EXISTS_TAC `ss:num->num`;
  USE 2 (REWRITE_RULE[complete]);
  ASM_REWRITE_TAC[];
  ASM_MESON_TAC[];
  ]);;
 
let countable_dense = prove_by_refinement(
  `!(X:A->bool) d. (metric_space(X,d)) /\ (totally_bounded(X,d)) ==>
     ?Z. (
COUNTABLE Z) /\ (dense (top_of_metric(X,d)) Z)`,
  (* {{{ proof *)
  [
  DISCH_ALL_TAC;
  TYPE_THEN `!r. ?z. (
COUNTABLE z) /\ (z 
SUBSET X) /\ (X = 
UNIONS (
IMAGE (\x. open_ball(X,d) x (twopow(--: (&:r)))) z))` SUBGOAL_TAC;
  GEN_TAC;
  COPY 0;
  COPY 1;
  JOIN 2 3;
  USE 2 (MATCH_MP 
center_FINITE);
  USE 2 (SPEC `twopow (--: (&:r))`);
  H_MATCH_MP (HYP "2") (THM (SPEC `(--: (&:r))` 
twopow_pos));
  X_CHO 3 `z:A->bool`;
  EXISTS_TAC `z:A->bool`;
  ASM_REWRITE_TAC[];
  ASM_SIMP_TAC[
FINITE_COUNTABLE];
  ASM_MESON_TAC[];
  CONV_TAC (quant_left_CONV "z");
  DISCH_THEN CHOOSE_TAC;
  TYPE_THEN  `
UNIONS (
IMAGE z (UNIV:num->bool))` EXISTS_TAC;
  CONJ_TAC;
  MATCH_MP_TAC  
COUNTABLE_UNIONS;
  CONJ_TAC;
  MATCH_MP_TAC  (ISPEC `UNIV:num->bool` 
COUNTABLE_IMAGE);
  REWRITE_TAC[
NUM_COUNTABLE];
  TYPE_THEN `z` EXISTS_TAC ;
  SET_TAC[];
  GEN_TAC;
  REWRITE_TAC[
IN_IMAGE;
IN_UNIV];
  ASM_MESON_TAC[ ];
  TYPE_THEN `U = top_of_metric (X,d)` ABBREV_TAC;
  TYPE_THEN `Z = 
UNIONS (
IMAGE z 
UNIV)` ABBREV_TAC;
  TYPE_THEN `topology_ U /\ (Z 
SUBSET (
UNIONS U))` SUBGOAL_TAC;
  EXPAND_TAC "U";
 
let metric_hausdorff = prove_by_refinement(
  `! (X:A->bool) d. (metric_space(X,d))==>
    (hausdorff (top_of_metric(X,d)))`,
  (* {{{ proof *)
  [
  DISCH_ALL_TAC;
  REWRITE_TAC[hausdorff;];
  ASM_SIMP_TAC [GSYM 
top_of_metric_unions];
  DISCH_ALL_TAC;
  COPY 0;
  USE 4 (REWRITE_RULE[metric_space]);
  TYPEL_THEN [`x`;`y`;`x`] (USE 4 o SPECL);
  REWR 4;
  TYPE_THEN  `r = d x y` ABBREV_TAC;
  SUBGOAL_TAC `&.0 <. r`;
  UND 4;
  ARITH_TAC;
  DISCH_TAC;
  TYPE_THEN  `open_ball(X,d) x (r/(&.2))`   EXISTS_TAC;
  TYPE_THEN  `open_ball(X,d) y (r/(&.2))`   EXISTS_TAC;
  ALL_TAC; (* mh1 *)
  KILL 4;
  ASM_SIMP_TAC[
open_ball_open];
  COPY 6;
  USE 4 (ONCE_REWRITE_RULE[GSYM 
REAL_LT_HALF1]);
  ASM_SIMP_TAC[REWRITE_RULE[
IN] 
open_ball_nonempty];
  PROOF_BY_CONTR_TAC;
  USE 7 (REWRITE_RULE[
EMPTY_EXISTS]);
  CHO 7;
  USE 7 (REWRITE_RULE[
IN_INTER]);
  USE 7 (REWRITE_RULE[
IN]);
  ALL_TAC; (* mh2 *)
  
AND 7;
  COPY 7;
  COPY 8;
  USE 7 (MATCH_MP 
open_ball_dist);
  USE 8 (MATCH_MP 
open_ball_dist);
  USE 0 (REWRITE_RULE[metric_space]);
  COPY 0;
  TYPEL_THEN [`x`;`u`;`y`] (fun t-> (USE 0 (ISPECL t)));
  TYPEL_THEN [`y`;`u`;`y`] (fun t-> (USE 11 (ISPECL t)));
  UND 11;
  UND 0;
  ASM_REWRITE_TAC[];
  TYPE_THEN `X u` SUBGOAL_TAC;
  ASM_MESON_TAC[ 
open_ball_subset;
IN;
SUBSET];
  DISCH_THEN (REWRT_TAC);
  DISCH_ALL_TAC;
  UND 14;
  UND 0;
  DISCH_THEN (fun t-> REWRITE_TAC[GSYM t]);
  JOIN 7 8;
  USE 0 (MATCH_MP (REAL_ARITH `(a <. c) /\ (b < c) ==> b+a < c + c`));
  USE 0 (CONV_RULE REDUCE_CONV);
  ASM_MESON_TAC[
real_lt];
  ]);;
 
let closed_compact = prove_by_refinement(
  `!U K (S:A->bool). ((topology_ U) /\ (compact U K) /\
     (closed_ U S) /\ (S 
SUBSET K)) ==> (compact U S)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[compact];
  DISCH_ALL_TAC;
  DISCH_ALL_TAC;
  SUBCONJ_TAC;
  ASM_MESON_TAC[ 
SUBSET_TRANS];
  DISCH_ALL_TAC;
  DISCH_ALL_TAC;
  TYPE_THEN `A = 
UNIONS U 
DIFF S` ABBREV_TAC;
  TYPE_THEN `open_ U A` SUBGOAL_TAC ;
  ASM_MESON_TAC[ 
closed_open];
  TYPE_THEN `V' = (A 
INSERT V)` ABBREV_TAC;
  DISCH_ALL_TAC;
  TYPE_THEN `V'` (USE 2 o SPEC);
  ALL_TAC; (* cc1 *)
  TYPE_THEN `K 
SUBSET UNIONS V'` SUBGOAL_TAC;
  EXPAND_TAC "V'";
 
let compact_closed = prove_by_refinement(
  `!U (K:A->bool). (topology_ U) /\ (hausdorff U) /\ (compact U K) ==>
     (closed_ U K)`,
  (* {{{ proof *)
  [
   REWRITE_TAC[hausdorff;compact;closed];
  DISCH_ALL_TAC;
  ASM_REWRITE_TAC[open_DEF];
  ONCE_ASM_SIMP_TAC[
open_nbd];
  TYPE_THEN `C = 
UNIONS U 
DIFF K` ABBREV_TAC;
  GEN_TAC;
  CONV_TAC (quant_right_CONV "B");
  DISCH_ALL_TAC;
  (* cc1 *)
  TYPE_THEN `!y. (K y) ==> (?A B. (U A /\ U B /\ A x /\ B y /\ (A 
INTER B = {})))` SUBGOAL_TAC;
  DISCH_ALL_TAC;
  UND 1;
  DISCH_THEN MATCH_MP_TAC;
  CONJ_TAC;
  UND 5;
  EXPAND_TAC "C";
 
let compact_totally_bounded = prove_by_refinement(
  `!(X:A->bool) d.( metric_space(X,d)) /\ (compact (top_of_metric(X,d)) X)
    ==> (totally_bounded (X,d))`,
  (* {{{ proof *)
  [
  REWRITE_TAC[totally_bounded;compact];
  DISCH_ALL_TAC;
  DISCH_ALL_TAC;
  CONV_TAC (quant_right_CONV "B");
  DISCH_TAC;
  TYPE_THEN `
IMAGE (\x. open_ball(X,d) x eps) X` (USE 2 o SPEC);
  TYPE_THEN `X 
SUBSET UNIONS (
IMAGE (\x. open_ball (X,d) x eps) X)` SUBGOAL_TAC;
  (REWRITE_TAC[
SUBSET;
IN_UNIONS;
IN_IMAGE]);
  GEN_TAC;
  NAME_CONFLICT_TAC;
  REWRITE_TAC[
IN];
  DISCH_TAC;
  CONV_TAC (quant_left_CONV "x'");
  CONV_TAC (quant_left_CONV "x'");
  TYPE_THEN `x` EXISTS_TAC;
  TYPE_THEN `open_ball (X,d) x eps` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  ASM_MESON_TAC[
open_ball_nonempty;
IN];
  DISCH_TAC;
  REWR 2;
  ALL_TAC; (* ctb1 *)
  TYPE_THEN `
IMAGE (\x. open_ball (X,d) x eps) X 
SUBSET top_of_metric (X,d)` SUBGOAL_TAC;
  TYPE_THEN `
IMAGE (\x. open_ball (X,d) x eps) X 
SUBSET open_balls(X,d)` SUBGOAL_TAC;
  REWRITE_TAC[
SUBSET;
IN_IMAGE;open_balls;IN_ELIM_THM'];
  MESON_TAC[
IN];
  MESON_TAC[
SUBSET_TRANS;
top_of_metric_open_balls];
  DISCH_TAC;
  REWR 2;
  CHO 2;
  TYPE_THEN `W` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  CONJ_TAC;
  DISCH_ALL_TAC;
  
AND 2;
  USE  7 (REWRITE_RULE [
SUBSET;
IN_IMAGE]);
  ASM_MESON_TAC[
IN];
  MATCH_MP_TAC  
SUBSET_ANTISYM;
  ASM_REWRITE_TAC[];
  TYPE_THEN `W 
SUBSET top_of_metric (X,d)` SUBGOAL_TAC;
  ASM_MESON_TAC[
SUBSET_TRANS];
  DISCH_ALL_TAC;
  USE 6 (MATCH_MP 
UNIONS_UNIONS);
  ASM_MESON_TAC[
top_of_metric_unions];
  ]);;
 
let cauchy_subseq_sublemma = prove_by_refinement(
  `!(X:A->bool) d f. ((metric_space(X,d))/\(totally_bounded(X,d)) /\
        (sequence X f)) ==>
    (?R Cn sn cond.
       (&0 < R) /\
       (!x y. X x /\ X y ==> d x y < R) /\
       (cond (X,0) 0) /\
       (sn 0 = 0) /\ (Cn 0 = X) /\
       (!n. Cn n 
SUBSET X /\ cond (Cn n,sn n) n) /\
       (!n. Cn (SUC n) 
SUBSET Cn n /\ sn n <| sn (SUC n)) /\
       (((\ (C,s). \n.
            (~FINITE {j | C (f j)}) /\
            (C (f s)) /\
           (!x y. (C x /\ C y) ==> d x y < R * (twopow (--: (&:n))))) =
       cond)
    ))`,
  (* {{{ proof *)
  [
  DISCH_ALL_TAC;
  COPY 0 THEN COPY 1;
  JOIN 4 3;
  USE 3 (MATCH_MP 
totally_bounded_bounded);
  CHO 3;
  CHO 3;
  ALL_TAC; (* {{{ xxx *)
  ALL_TAC; (* make r pos *)
  ASSUME_TAC (REAL_ARITH `r <. (&.1 + abs(r))`);
  ASSUME_TAC (REAL_ARITH `&.0 <. (&.1 + abs(r))`);
  ABBREV_TAC (`r' = &.1 +. abs(r)`);
  SUBGOAL_TAC `open_ball(X,d) a r 
SUBSET open_ball(X,d) (a:A) r'`;
  ASM_SIMP_TAC[
open_ball_nest];
  DISCH_TAC;
  JOIN 3 7;
  USE 3 (MATCH_MP 
SUBSET_TRANS);
  KILL 6;
  KILL 4;
  ALL_TAC; (* "cs1" *)
  SUBGOAL_TAC `( !(x:A) y.  (X x) /\ (X y) ==> (d x y <. &.2 *. r'))`;
  DISCH_ALL_TAC;
  USE 3 (REWRITE_RULE[
SUBSET;
IN]);
  COPY 3;
  USE 7 (SPEC `x:A`);
  USE 3 (SPEC `y:A`);
  H_MATCH_MP (HYP "3") (HYP "6");
  H_MATCH_MP (HYP "7") (HYP "4");
  JOIN 9 8;
  JOIN 0 8;
  USE 0 (MATCH_MP 
BALL_DIST);
  ASM_REWRITE_TAC[];
  DISCH_TAC;
  ABBREV_TAC `cond = (\ ((C:A->bool),(s:num)) n. ~FINITE{j| C (f j)} /\ (C(f s)) /\ (!x y. (C x /\ C y) ==> d x y <. (&.2*.r')*. twopow(--: (&:n))))`;
  ABBREV_TAC `R = (&.2)*r'`;
  ALL_TAC ; (* 0 case of recursio *)
  ALL_TAC; (* cs2 *)
  SUBGOAL_TAC ` (X 
SUBSET X) /\ (cond ((X:A->bool),0) 0)`;
  REWRITE_TAC[
SUBSET_REFL];
  EXPAND_TAC "cond";
 
let subseq_cauchy = prove_by_refinement(
  `!(X:A->bool) d f s. (metric_space(X,d)) /\
    (cauchy_seq (X,d) f) /\ (subseq s) /\
    (converge(X,d) (f o s)) ==> (converge(X,d) f)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[cauchy_seq;converge;
sequence_in];
  DISCH_ALL_TAC;
  CHO 4;
  TYPE_THEN `x` EXISTS_TAC ;
  ASM_REWRITE_TAC[];
  DISCH_ALL_TAC;
  
AND 4;
  TYPE_THEN `eps/(&.2)` (USE 2 o SPEC);
  TYPE_THEN `eps/(&.2)` (USE 4 o SPEC);
  CHO 4;
  CHO 2;
  CONV_TAC (quant_right_CONV "n");
  DISCH_ALL_TAC;
  USE 2 (REWRITE_RULE[
REAL_LT_HALF1]);
  USE 4 (REWRITE_RULE[
REAL_LT_HALF1]);
  REWR 2;
  REWR 4;
  TYPE_THEN `n'` EXISTS_TAC ;
  DISCH_ALL_TAC;
  TYPE_THEN `n +| n'` (USE 4 o SPEC);
  USE 4 (REWRITE_RULE[ARITH_RULE `n  <=| n +| n'`]);
  TYPE_THEN `s(n +| n')` (USE 2 o SPEC);
  TYPE_THEN `i` (USE 2 o SPEC);
  TYPE_THEN `n' <=| s (n +| n')` SUBGOAL_TAC;
  USE 3 (MATCH_MP 
SEQ_SUBLE);
  TYPE_THEN `n +| n'` (USE 3 o SPEC);
  ASM_MESON_TAC[ 
LE_TRANS; ARITH_RULE `n' <=| n +| n'`];
  DISCH_TAC;
  REWR 2;
  USE 4 (REWRITE_RULE[
o_DEF]);
  (* save_goal"sc1"; *)
  TYPEL_THEN [`X`;`d`;`x`;`f (s(n +| n'))`;`f i`] (fun t-> ASSUME_TAC (ISPECL t 
metric_space_triangle));
  USE 5 (REWRITE_RULE[
IN]);
  REWR 9;
  USE 1 (MATCH_MP 
sequence_in);
  REWR 9;
  UND 9;
  UND 4;
  UND 2;
  MP_TAC (SPEC `eps:real` 
REAL_HALF_DOUBLE);
  TYPE_THEN `a = d (f (s (n +| n'))) (f i)` ABBREV_TAC ;
  TYPE_THEN `b = d x (f (s (n +| n')))` ABBREV_TAC ;
  TYPE_THEN `c = d x (f i)` ABBREV_TAC ;
  REAL_ARITH_TAC;
  ]);;
 
let compact_complete = prove_by_refinement(
  `!(X:A->bool) d. metric_space(X,d) /\
     (compact (top_of_metric(X,d)) X) ==>
     (complete(X,d))`,
  (* {{{ proof *)
  [
  REWRITE_TAC [complete];
  DISCH_ALL_TAC;
  DISCH_ALL_TAC;
  COPY 0;
  COPY 1;
  JOIN 3 4;
  USE 3 (MATCH_MP 
compact_totally_bounded);
  COPY 2;
  USE 4 (REWRITE_RULE[cauchy_seq]);
  
AND 4;
  COPY 0;
  COPY 3;
  COPY 5;
  JOIN 7 8;
  JOIN 6 7;
  USE 6 (MATCH_MP 
cauchy_subseq_sublemma);
  CHO 6;
  CHO 6;
  CHO 6;
  CHO 6;
  (
AND 6);
  (
AND 6);
  (
AND 6);
  (
AND 6);
  (
AND 6);
  (
AND 6);
  (
AND 6);
  ALL_TAC ; (* cc1 *)
  MATCH_MP_TAC 
subseq_cauchy;
  TYPE_THEN `sn` EXISTS_TAC;
  ASM_REWRITE_TAC [converge];
  SUBCONJ_TAC;
  REWRITE_TAC[
SUBSEQ_SUC];
  ASM_MESON_TAC[ ];
  DISCH_ALL_TAC;
  TYPE_THEN `~(
INTERS {z | ?n. z = closed_ball(X,d) (f (sn n)) (R* twopow(--: (&:n)))} =
EMPTY)` SUBGOAL_TAC;
  PROOF_BY_CONTR_TAC ;
  REWR 15;
  TYPEL_THEN [`top_of_metric(X,d)`;`{z | ?n. z = closed_ball (X,d) (f(sn n)) (R * twopow (--: (&:n)))}`] (fun t-> ASSUME_TAC (ISPECL t 
finite_inters));
  REWR 16;
  TYPE_THEN `topology_ (top_of_metric (X,d)) /\ compact (top_of_metric (X,d)) (
UNIONS (top_of_metric (X,d))) /\ (!u. {z | ?n. z = closed_ball (X,d) (f(sn n)) (R * twopow (--: (&:n)))} u ==> closed_ (top_of_metric (X,d)) u)` SUBGOAL_TAC ;
  ASM_SIMP_TAC[GSYM 
top_of_metric_unions;];
  ASM_SIMP_TAC[
top_of_metric_top];
  REWRITE_TAC[IN_ELIM_THM'];
  ASM_MESON_TAC[
closed_ball_closed];
  DISCH_TAC;
  REWR 16;
  CHO 16;
  ALL_TAC ; (* cc2 *)
  TYPE_THEN `{z | ?n. z = closed_ball (X,d) (f (sn n)) (R * twopow (--: (&:n)))} = 
IMAGE (\n. closed_ball (X,d) (f (sn n)) (R * twopow (--: (&:n)))) (
UNIV)` SUBGOAL_TAC ;
  MATCH_MP_TAC  
EQ_EXT;
  GEN_TAC ;
  REWRITE_TAC[IN_ELIM_THM';
 
let complete_compact = prove_by_refinement(
  `!(X:A->bool) d . (metric_space(X,d)) /\ (totally_bounded(X,d)) /\
  (complete (X,d)) ==> (compact (top_of_metric(X,d)) X)`,
  (* {{{ proof *)
  [
  DISCH_ALL_TAC;
  REWRITE_TAC[compact];
  CONJ_TAC ;
  UND 0;
  SIMP_TAC[GSYM   
top_of_metric_unions ];
  REWRITE_TAC[
SUBSET_REFL];
  GEN_TAC;
  DISCH_ALL_TAC;
  TYPE_THEN `(?V'. (V' 
SUBSET V) /\ (X 
SUBSET (
UNIONS V')) /\ (
COUNTABLE V'))` SUBGOAL_TAC ;
  IMATCH_MP_TAC  
countable_cover;
  TYPE_THEN `d` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  DISCH_THEN (CHOOSE_THEN MP_TAC);
  DISCH_ALL_TAC;
  ALL_TAC; (* ASM_MESON_TAC[]; *)
  ALL_TAC; (* DISCH_THEN (CHOOSE_THEN MP_TAC); *)
  ALL_TAC; (* DISCH_ALL_TAC;  *)
  USE 7 (REWRITE_RULE[
COUNTABLE;
GE_C;
UNIV]);
  IN_OUT_TAC;
  CHO 0;
  TYPE_THEN `B = \i. (
IMAGE f { u | (u <=| i )  /\ V' (f u)}) ` ABBREV_TAC ;
  TYPE_THEN `?i . 
UNIONS (B i ) = X ` ASM_CASES_TAC;
  CHO 9;
  TYPE_THEN `B i ` EXISTS_TAC;
  EXPAND_TAC "B";
 
let compact_uniformly_continuous = prove_by_refinement(
  `!f X dX Y dY. metric_continuous f (X,dX) (Y,dY) /\ (metric_space(X,dX))
    /\ (metric_space(Y,dY)) /\ (compact(top_of_metric(X,dX)) X) /\
    (
IMAGE f X 
SUBSET Y) ==>
    uniformly_continuous (f:A->B) ((X:A->bool),dX) ((Y:B->bool),dY)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[uniformly_continuous;metric_continuous;metric_continuous_pt];
  DISCH_ALL_TAC;
  GEN_TAC;
  LEFT 0 "epsilon";
 
let image_compact = prove_by_refinement(
  `!U V (f:A->B) K. (continuous f U V ) /\
      (compact U K) /\ (
IMAGE f K 
SUBSET (
UNIONS V))
  ==> (compact V (
IMAGE f K))`,
  (* {{{ proof *)
  [
  DISCH_ALL_TAC;
  REWRITE_TAC[compact];
  ASM_REWRITE_TAC[];
  DISCH_ALL_TAC;
  TYPE_THEN `cov = 
IMAGE (\v. preimage (
UNIONS U) f v ) V'`  ABBREV_TAC ;
  TYPE_THEN `cov 
SUBSET U` SUBGOAL_TAC ;
  EXPAND_TAC "cov";
 
let neg_continuous = prove_by_refinement(
  `!n. metric_continuous (euclid_neg) (euclid n,d_euclid) (euclid n,d_euclid)`,
  (* {{{ proof *)
  [
  DISCH_ALL_TAC;
  REWRITE_TAC[metric_continuous;metric_continuous_pt];
  DISCH_ALL_TAC;
  RIGHT_TAC "delta";
 
let continuous_comp = prove_by_refinement(
  `!(f:A->B) (g:B->C) U V W.
      continuous f U V /\ continuous g V W /\
      (
IMAGE f (
UNIONS U) 
SUBSET (
UNIONS V)) ==>
     continuous (g o f) U W`,
  (* {{{ proof *)
  [
  REWRITE_TAC[continuous;
IN;preimage];
  DISCH_ALL_TAC;
  X_GEN_TAC `w :C->bool`;
  DISCH_TAC;
  TYPE_THEN `w ` (USE  1 o SPEC);
  REWR 1;
  TYPE_THEN `{x | 
UNIONS V x /\ w (g x)}` (USE 0 o SPEC);
  REWR 0;
  USE 0 (REWRITE_RULE[IN_ELIM_THM' ]);
  REWRITE_TAC[
o_DEF ];
  TYPE_THEN `U {x | 
UNIONS U x /\ 
UNIONS V (f x) /\ w (g (f x))} = U {x | 
UNIONS U x /\ w (g (f x))}` SUBGOAL_TAC;
  AP_TERM_TAC;
  IMATCH_MP_TAC  
EQ_EXT;
  DISCH_ALL_TAC;
  REWRITE_TAC[IN_ELIM_THM'];
  IMATCH_MP_TAC  (TAUT `(a ==> b) ==> ((a /\ b /\ c) <=> (a /\ c ))`);
  TYPE_THEN  `UU = 
UNIONS U ` ABBREV_TAC;
  TYPE_THEN `VV = 
UNIONS V` ABBREV_TAC ;
  USE 2 (REWRITE_RULE[
SUBSET;
IN_IMAGE ]);
  ASM_MESON_TAC[
IN];
  DISCH_THEN (fun  t-> (USE 0 ( REWRITE_RULE[t])));
  ASM_REWRITE_TAC[];
  ]);;
 
let compact_max = prove_by_refinement(
  `!(f:A->(num->real)) U K.
       (continuous f U (top_of_metric(euclid 1,d_euclid))) /\
       (
IMAGE f K 
SUBSET (euclid 1)) /\
        (compact U K) /\ ~(K=
EMPTY)==>
     (?x. K x /\ (!y. (K y) ==> (f y 0 <= f x 0)))`,
  (* {{{ proof *)
  [
  DISCH_ALL_TAC;
  COPY 2;
  COPY 1;
  TYPE_THEN `euclid 1 = 
UNIONS (top_of_metric (euclid 1,d_euclid))` SUBGOAL_TAC;
  MESON_TAC[
top_of_metric_unions;
metric_euclid];
  DISCH_THEN (fun t-> USE 5 (ONCE_REWRITE_RULE[t]));
  JOIN 4 5;
  COPY 0;
  JOIN 0 4;
  WITH  0 (MATCH_MP 
image_compact);
  UND 4;
  ASM_SIMP_TAC[
compact_euclid];
  DISCH_ALL_TAC;
  TYPE_THEN `P = (
IMAGE (coord 0) (
IMAGE f K))` ABBREV_TAC ;
  TYPE_THEN `(?s. !y. (?x. P x /\ y <. x) <=> y <. s)` SUBGOAL_TAC;
  IMATCH_MP_TAC  
REAL_SUP_EXISTS;
  CONJ_TAC;
  USE 3 (REWRITE_RULE[
EMPTY_EXISTS;
IN ]);
  CHO 3;
  TYPE_THEN `f u 0` EXISTS_TAC;
  EXPAND_TAC "P";
 
let bicont_homeomorphism = prove_by_refinement(
  `!f U V. (
BIJ (f:A->B) (
UNIONS U) (
UNIONS V)) /\ (continuous f U V) /\
    (continuous (
INV  f (
UNIONS U) (
UNIONS V)) V U) ==>
     (homeomorphism f U V)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[homeomorphism];
  DISCH_ALL_TAC;
  ASM_REWRITE_TAC[];
  DISCH_ALL_TAC;
  UND 2;
  REWRITE_TAC[continuous;
IN;preimage ];
  DISCH_ALL_TAC;
  TYPE_THEN `A` (USE 2 o SPEC);
  REWR 2;
  TYPE_THEN `{x | 
UNIONS V x /\ A (
INV f (
UNIONS U) (
UNIONS V) x)}= (
IMAGE f A) ` SUBGOAL_TAC;
  IMATCH_MP_TAC  
EQ_EXT ;
  X_GEN_TAC `t:B`;
  REWRITE_TAC[IN_ELIM_THM';
 
let interval_closed_ball = prove_by_refinement(
   `!a b . ? x r. (a <=. b) ==>
   ({x | euclid 1 x /\ a <= x 0 /\ x 0 <= b} =
    (closed_ball(euclid 1,d_euclid)) x r)`,
  (* {{{ proof *)
  [
  DISCH_ALL_TAC;
  TYPE_THEN `((a +b)/(&.2)) *# (
dirac_delta 0)` EXISTS_TAC;
  TYPE_THEN `((b -a)/(&.2))` EXISTS_TAC;
  DISCH_ALL_TAC;
  IMATCH_MP_TAC  
EQ_EXT;
  REWRITE_TAC[closed_ball;IN_ELIM_THM'];
  DISCH_ALL_TAC;
  IMATCH_MP_TAC  (TAUT `(a ==> (b <=> d /\ c))  ==> (a /\ b <=> d /\ a /\ c)`);
  DISCH_ALL_TAC;
  TYPE_THEN `z = ((a + b) / &2 *# 
dirac_delta 0)` ABBREV_TAC;
  TYPE_THEN `euclid 1 z` SUBGOAL_TAC;
  EXPAND_TAC "z";
 
let interval_euclid1_bounded = prove_by_refinement(
  `!a b. metric_bounded
    ({x | euclid 1 x /\ a <= x 0 /\ x 0 <= b},d_euclid)`,
  (* {{{ proof *)
  [
  DISCH_ALL_TAC;
  REWRITE_TAC[metric_bounded];
  ASSUME_TAC 
interval_closed_ball;
  TYPEL_THEN [`a`;`b`] (USE 0 o SPECL);
  CHO 0;
  CHO 0;
  ASM_CASES_TAC `a <=. b`;
  REWR 0;
  ASM_REWRITE_TAC[];
  TYPE_THEN `x` EXISTS_TAC;
  TYPE_THEN `r + (&.1) ` EXISTS_TAC;
  REWRITE_TAC[open_ball;
SUBSET;
IN ;IN_ELIM_THM' ];
  DISCH_ALL_TAC;
  ASM_REWRITE_TAC[];
  UND 2;
  REWRITE_TAC[closed_ball;IN_ELIM_THM' ];
  DISCH_ALL_TAC;
  ASM_REWRITE_TAC[];
  UND 4;
  ASM_SIMP_TAC[
euclid1_abs ];
  TYPE_THEN  `t = x 0` ABBREV_TAC;
  TYPE_THEN `s = x' 0` ABBREV_TAC;
  DISCH_ALL_TAC;
  TYPE_THEN `&.0 <=. r` SUBGOAL_TAC;
  UND 6;
  REAL_ARITH_TAC;
  DISCH_ALL_TAC;
  REDUCE_TAC;
  ASM_REWRITE_TAC[];
  UND 6;
  UND 7;
  REAL_ARITH_TAC ;
  TYPE_THEN `{x | euclid 1 x /\ a <= x 0 /\ x 0 <= b} = 
EMPTY` SUBGOAL_TAC;
  REWRITE_TAC[
EQ_EMPTY;IN_ELIM_THM' ];
  GEN_TAC;
  TYPE_THEN `t = x 0 ` ABBREV_TAC;
  KILL 2;
  IMATCH_MP_TAC  (TAUT `~(b /\ C) ==> ~( a /\ b/\ C)`);
  UND 1;
  REAL_ARITH_TAC;
  DISCH_THEN (fun t-> REWRITE_TAC[t]);
  REWRITE_TAC[
EMPTY_SUBSET];
  ]);;
 
let half_open = prove_by_refinement(
  `!a. top_of_metric(
UNIV,d_real ) { x | x <. a}`,
  (* {{{ proof *)
  [
  GEN_TAC;
  ASSUME_TAC 
open_nbd ;
  TYPEL_THEN [`top_of_metric (
UNIV,d_real)`;` {x | x < a}`] (USE 0 o ISPECL);
  USE 0 (SIMP_RULE[
top_of_metric_top;
metric_real ]);
  ASM_REWRITE_TAC[];
  GEN_TAC;
  TYPE_THEN `open_ball (
UNIV,d_real) x (a - x)` EXISTS_TAC;
  REWRITE_TAC[IN_ELIM_THM'];
  DISCH_ALL_TAC;
  CONJ_TAC;
  REWRITE_TAC[open_ball;d_real ;
IN;IN_ELIM_THM';
 
let half_open_above = prove_by_refinement(
  `!a. top_of_metric(
UNIV,d_real ) { x | a <. x}`,
  (* {{{ proof *)
  [
  GEN_TAC;
  ASSUME_TAC 
open_nbd ;
  TYPEL_THEN [`top_of_metric (
UNIV,d_real)`;` {x | a <. x}`] (USE 0 o ISPECL);
  USE 0 (SIMP_RULE[
top_of_metric_top;
metric_real ]);
  ASM_REWRITE_TAC[];
  GEN_TAC;
  TYPE_THEN `open_ball (
UNIV,d_real) x (x -. a)` EXISTS_TAC;
  REWRITE_TAC[IN_ELIM_THM'];
  DISCH_ALL_TAC;
  CONJ_TAC;
  REWRITE_TAC[open_ball;d_real ;
IN;IN_ELIM_THM';
 
let joinf_cont = prove_by_refinement(
  `!U a  (f:real -> A) g.
   (continuous f (top_of_metric(
UNIV,d_real)) U) /\
   (continuous g (top_of_metric(
UNIV,d_real)) U) /\
   (f a = (g a)) ==>
   ( (continuous (joinf f g a) (top_of_metric(
UNIV,d_real)) U))`,
  (* {{{ proof *)
  [
  REWRITE_TAC[continuous];
  DISCH_ALL_TAC;
  DISCH_ALL_TAC;
  REWRITE_TAC[
IN ];
  ASSUME_TAC 
open_nbd;
  TYPEL_THEN [`top_of_metric (
UNIV,d_real)`;`(preimage (
UNIONS (top_of_metric (
UNIV,d_real))) (joinf f g a) v)`] (USE 4 o ISPECL);
  USE 4 (SIMP_RULE [
top_of_metric_top;
metric_real  ]);
  ASM_REWRITE_TAC[];
  GEN_TAC;
  REWRITE_TAC[
subset_preimage];
  RIGHT_TAC "B";
 
let connected_unions = prove_by_refinement(
  `!U (Z1:A->bool) Z2. (connected U Z1) /\ (connected U Z2) /\
    ~(Z1 
INTER Z2 = 
EMPTY) ==> (connected U (Z1 
UNION Z2))`,
  (* {{{ proof *)
  [
  REWRITE_TAC[connected];
  DISCH_ALL_TAC;
  DISCH_ALL_TAC;
  SUBCONJ_TAC;
  REWRITE_TAC[
UNION;
SUBSET;
IN;IN_ELIM_THM'   ];
  ASM_MESON_TAC[
SUBSET ;
IN];
  DISCH_TAC ;
  DISCH_ALL_TAC;
  TYPEL_THEN [`A`;`B`] (USE 1 o SPECL);
  REWR 1;
  TYPEL_THEN [`A`;`B`] (USE 3 o SPECL);
  REWR 3;
  WITH 9 (REWRITE_RULE[
union_subset]);
  REWR 1;
  REWR 3;
  IMATCH_MP_TAC (TAUT  `(~b ==> a)   ==> (a \/ b)`);
  DISCH_ALL_TAC;
  USE 11 (REWRITE_RULE[
union_subset]);
  (* start a case *)
  USE 4 (REWRITE_RULE[
EMPTY_EXISTS]);
  CHO 4;
  USE 4 (REWRITE_RULE[
IN;
INTER;IN_ELIM_THM'  ]);
  REWRITE_TAC[
union_subset];
  TYPE_THEN `~((Z1 
SUBSET A) /\ (Z2 
SUBSET B))` SUBGOAL_TAC;
  DISCH_ALL_TAC;
  USE 8 (REWRITE_RULE[
EQ_EMPTY]);
  USE 8 (REWRITE_RULE[
INTER;
IN;IN_ELIM_THM' ]);
  ASM_MESON_TAC[
SUBSET;
IN];
  TYPE_THEN `~((Z2 
SUBSET A) /\ (Z1 
SUBSET B))` SUBGOAL_TAC;
  DISCH_ALL_TAC;
  USE 8 (REWRITE_RULE[
EQ_EMPTY]);
  USE 8 (REWRITE_RULE[
INTER;
IN;IN_ELIM_THM' ]);
  ASM_MESON_TAC[
SUBSET;
IN];
  ASM_MESON_TAC[];
  ]);;
 
let component_trans = prove_by_refinement(
  `!U (x:A) y z. (component U x y) /\ (component U y z) ==>
   (component U x z)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[component_DEF];
  DISCH_ALL_TAC;
  CHO 0;
  CHO 1;
  TYPE_THEN `connected U (Z 
UNION Z')` SUBGOAL_TAC;
  IMATCH_MP_TAC 
connected_unions;
  ASM_REWRITE_TAC[];
  REWRITE_TAC[
EMPTY_EXISTS ];
  REWRITE_TAC[
IN;
INTER;IN_ELIM_THM' ];
  TYPE_THEN `y` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  DISCH_ALL_TAC;
  TYPE_THEN `Z 
UNION Z'` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  REWRITE_TAC[
UNION;
IN;IN_ELIM_THM' ];
  ASM_REWRITE_TAC[];
  ]);;
 
let connect_real = prove_by_refinement(
  `!a b. connected (top_of_metric (
UNIV,d_real))
    {x | a <=. x /\ x <=. b }`,
  (* {{{ proof *)
  [
  DISCH_ALL_TAC;
  REWRITE_TAC[connected];
  ASSUME_TAC 
metric_real;
  ASM_SIMP_TAC[GSYM 
top_of_metric_unions];
  SUBCONJ_TAC;
  REWRITE_TAC[
UNIV;
SUBSET;
IN ];
  DISCH_TAC;
  DISCH_ALL_TAC;
  TYPE_THEN `\ (u ,v ). ( u <. a) \/ (b <. v) \/ ({x | u <=. x /\ x <=. v } 
SUBSET A) \/ ({x | u <=. x /\ x <=. v } 
SUBSET B)` (fun t-> ASSUME_TAC (SPEC t 
BOLZANO_LEMMA ));
  UND 6;
  GBETA_TAC ;
  IMATCH_MP_TAC  (TAUT `((b ==> c ) /\ a ) ==> ((a ==> b) ==> c  )`);
  CONJ_TAC;
  DISCH_ALL_TAC;
  TYPEL_THEN [`a`;`b`] ((USE 6 o SPECL));
  USE 6 (REWRITE_RULE[ARITH_RULE `~(a <. a)`]);
  ASM_CASES_TAC `a <=. b`;
  REWR 6;
  TYPE_THEN `{x | a <=. x /\ x <=. b} = 
EMPTY ` SUBGOAL_TAC;
  IMATCH_MP_TAC  
EQ_EXT;
  REWRITE_TAC[IN_ELIM_THM';
 
let const_continuous = prove_by_refinement(
  `!U V y. (topology_ U)  ==>
    (continuous (\ (x:A). (y:B)) U V)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[continuous];
  DISCH_ALL_TAC;
  REWRITE_TAC[
IN];
  DISCH_ALL_TAC;
  REWRITE_TAC[preimage;
IN ];
  TYPE_THEN `v y` ASM_CASES_TAC ;
  ASM_REWRITE_TAC[
IN_ELIM_THM];
  USE 0 (MATCH_MP 
top_univ);
  TYPE_THEN`t = 
UNIONS U`  ABBREV_TAC;
  UND 0;
  MATCH_MP_TAC(TAUT `(a <=> b) ==> a ==> b`);
  AP_TERM_TAC;
  REWRITE_TAC[
EXTENSION; 
IN_ELIM_THM; 
IN];
  USE 0 (MATCH_MP 
open_EMPTY);
  USE 0 (REWRITE_RULE[open_DEF ;
EMPTY]);
  ASM_REWRITE_TAC[];
  SUBGOAL_THEN `{x:A | F} = \x. F` SUBST1_TAC;
  REWRITE_TAC[
EXTENSION; 
IN; 
IN_ELIM_THM];
  ASM_REWRITE_TAC[]
  ]);;
 
let path_trans = prove_by_refinement(
  `!U x y (z:A). (
path_component U x y) /\ (
path_component U y z) ==>
  (
path_component U x z)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[
path_component];
  DISCH_ALL_TAC;
  CHO 0;
  CHO 0;
  CHO 0;
  CHO 1;
  CHO 1;
  CHO 1;
  TYPE_THEN `joinf f (f' o ((+.) (a' -. b))) b` EXISTS_TAC;
  TYPE_THEN `a` EXISTS_TAC;
  TYPE_THEN `b' +. (b - a')` EXISTS_TAC;
  CONJ_TAC; (* start of continuity *)
  IMATCH_MP_TAC  
joinf_cont;
  ASM_REWRITE_TAC[];
  CONJ_TAC;
  IMATCH_MP_TAC  
continuous_comp;
  TYPE_THEN `(top_of_metric (
UNIV,d_real))` EXISTS_TAC;
  ASM_REWRITE_TAC [
top_of_metric_top;  
metric_real;  
metric_euclidean;  
metric_euclid;  
metric_hausdorff;  GSYM 
top_of_metric_unions;  
open_ball_open;];
  REWRITE_TAC[
add_cont];
  ASM_SIMP_TAC [
top_of_metric_top;  
metric_real;  
metric_euclidean;  
metric_euclid;  
metric_hausdorff;  GSYM 
top_of_metric_unions;  
open_ball_open;];
  REWRITE_TAC[
SUBSET;
UNIV;
IN;IN_ELIM_THM'];
  REWRITE_TAC[
o_DEF];
  REDUCE_TAC;
  ASM_REWRITE_TAC[]; (* end of continuity *)
  CONJ_TAC; (* start real ineq *)
  
AND 1;
  
AND 1;
  
AND 0;
  
AND 0;
  UND 5;
  UND 3;
  REAL_ARITH_TAC; (* end of real ineq *)
  CONJ_TAC;
  REWRITE_TAC[joinf;
o_DEF];
  ASM_REWRITE_TAC[]; (* end of JOIN statement *)
  CONJ_TAC; (* next JOIN statement *)
  REWRITE_TAC[joinf;
o_DEF];
  TYPE_THEN `~(b' +. b -. a' <. b)` SUBGOAL_TAC;
  TYPE_THEN `(a' <. b') /\ (a <. b)` SUBGOAL_TAC;
  ASM_REWRITE_TAC[];
  REAL_ARITH_TAC;
  DISCH_THEN (fun t-> REWRITE_TAC[t]);
  TYPE_THEN ` a' -. b +. b' +. b -. a' = b'` SUBGOAL_TAC;
  REAL_ARITH_TAC ;
    DISCH_THEN (fun t-> REWRITE_TAC[t]);
  ASM_REWRITE_TAC[]; (* end of next joinf *)
  TYPE_THEN `(a <=. b) /\ (b <=. (b' + b - a'))` SUBGOAL_TAC; (* subreal *)
  TYPE_THEN `(a' <. b') /\ (a <. b)` SUBGOAL_TAC;
  ASM_REWRITE_TAC[];
  REAL_ARITH_TAC;
  DISCH_TAC; (* end of subreal *)
  USE 2 (MATCH_MP 
union_closed_interval);
  UND 2;
  DISCH_THEN (fun t-> REWRITE_TAC[GSYM t]);
  REWRITE_TAC[
IMAGE_UNION;
union_subset];
  CONJ_TAC; (* start of FIRST interval *)
  TYPE_THEN `
IMAGE (joinf f (f' o (+.) (a' -. b)) b) {t | a <=. t /\ t <. b} = 
IMAGE f {t | a <=. t /\ t <. b}` SUBGOAL_TAC;
  REWRITE_TAC[joinf;
IMAGE;
IN_IMAGE ];
  IMATCH_MP_TAC  
EQ_EXT;
  X_GEN_TAC `t:A`;
  REWRITE_TAC[IN_ELIM_THM'];
  EQ_TAC;
  DISCH_ALL_TAC;
  CHO 2;
  UND 2;
  DISCH_ALL_TAC;
  REWR 4;
  ASM_MESON_TAC[];
  DISCH_ALL_TAC;
  CHO 2;
  UND 2;
  DISCH_ALL_TAC;
 TYPE_THEN `x'` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  DISCH_THEN (fun t-> REWRITE_TAC[t]); (* FIRST interval still *)
  TYPE_THEN `
IMAGE f {t | a <=. t /\ t <. b} 
SUBSET IMAGE f {t | a <=. t /\ t <=. b} ` SUBGOAL_TAC;
  REWRITE_TAC[
SUBSET;
IN_IMAGE ;IN_ELIM_THM'];
  GEN_TAC;
  DISCH_THEN (CHOOSE_THEN MP_TAC);
  MESON_TAC[REAL_ARITH `a <. b ==> a<=. b`];
  KILL 1;
  UND 0;
  DISCH_ALL_TAC;
  JOIN 0 5;
  USE 0 (MATCH_MP 
SUBSET_TRANS );
  ASM_REWRITE_TAC[]; (* end of FIRST interval *)
  (* lc 1*)
  TYPE_THEN `
IMAGE (joinf f (f' o (+.) (a' -. b)) b) {t | b <=. t /\ t <=. b' + b -. a'}  = 
IMAGE f' {t | a' <=. t /\ t <=. b'}` SUBGOAL_TAC;
  REWRITE_TAC[joinf;
IMAGE;
IN_IMAGE ];
  IMATCH_MP_TAC  
EQ_EXT;
  REWRITE_TAC[IN_ELIM_THM'];
  NAME_CONFLICT_TAC ;
  X_GEN_TAC `t:A`;
  EQ_TAC;
  DISCH_ALL_TAC;
  CHO 2;
  UND 2;
  DISCH_ALL_TAC;
  TYPE_THEN `~(x' <. b)` SUBGOAL_TAC;
  UND 2;
  REAL_ARITH_TAC ;
  DISCH_TAC ;
  REWR 4;
  USE 4 (REWRITE_RULE[
o_DEF]);
  TYPE_THEN `a' -. b +. x'` EXISTS_TAC; (* * *)
  ASM_REWRITE_TAC[];
  TYPE_THEN `(a' <. b') /\ (a <. b) /\ (b <=. x') /\ (x' <=. b' +. b -. a')` SUBGOAL_TAC;
  ASM_REWRITE_TAC[];
  REAL_ARITH_TAC;
  DISCH_ALL_TAC;
  CHO 2;
  UND 2;
  DISCH_ALL_TAC;
  TYPE_THEN `x' +. b -. a'` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  SUBCONJ_TAC;
  UND 2;
  UND 3;
  REAL_ARITH_TAC;
  DISCH_ALL_TAC;
  TYPE_THEN `~(x' +. b -. a' <. b)` SUBGOAL_TAC;
  UND 5;
  REAL_ARITH_TAC ;
  DISCH_THEN (fun t-> REWRITE_TAC[t]);
  REWRITE_TAC[
o_DEF];
  AP_TERM_TAC;
  REAL_ARITH_TAC ;
  DISCH_THEN (fun t -> REWRITE_TAC [t]);
  ASM_REWRITE_TAC[];
  ]);;
 
let path_eq_conn = prove_by_refinement(
  `!U (x:A). (loc_path_conn U) /\ (topology_ U) ==>
    (
path_component U x = component U x)`,
  (* {{{ proof *)
  [
  DISCH_ALL_TAC;
  MATCH_MP_TAC 
EQ_EXT;
  X_GEN_TAC `y:A`;
  EQ_TAC ;
  REWRITE_TAC[
path_component];
  DISCH_ALL_TAC;
  CHO 2;
  CHO 2;
  CHO 2;
  UND 2 THEN DISCH_ALL_TAC;
  REWRITE_TAC[component_DEF];
  TYPE_THEN `
IMAGE f {t | a <= t /\ t <= b}` EXISTS_TAC;
  CONJ_TAC;
  IMATCH_MP_TAC  
connect_image ;
  NAME_CONFLICT_TAC;
  TYPE_THEN `(top_of_metric (
UNIV,d_real))` EXISTS_TAC ;
  ASM_REWRITE_TAC[
connect_real ];
  REWRITE_TAC[
IMAGE;
IN;IN_ELIM_THM' ];
  CONJ_TAC;
  TYPE_THEN `a` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  UND 3;
  REAL_ARITH_TAC ;
  TYPE_THEN `b` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  UND 3;
  REAL_ARITH_TAC;
  REWRITE_TAC[component_DEF];
  DISCH_ALL_TAC;
  CHO 2;
  UND 2 THEN DISCH_ALL_TAC;
  USE 2 (REWRITE_RULE[connected]);
  UND 2 THEN DISCH_ALL_TAC;
  TYPE_THEN `
path_component U x` (USE 5 o SPEC);
  TYPE_THEN `A = 
path_component U x` ABBREV_TAC;
  TYPE_THEN `B = 
UNIONS (
IMAGE (\z. (
path_component U z)) (Z 
DIFF A))` ABBREV_TAC ;
  TYPE_THEN `B` (USE 5 o SPEC);
  TYPE_THEN `U A /\ U B /\ (A 
INTER B = {}) /\ Z 
SUBSET A 
UNION B` SUBGOAL_TAC;
  WITH  0 (REWRITE_RULE[loc_path_conn]);
  TYPE_THEN `(
UNIONS U)` (USE 8 o SPEC);
  TYPE_THEN `x` (USE   8 o SPEC);
  UND 8;
  ASM_SIMP_TAC[
induced_top_unions];
  ASM_SIMP_TAC[
top_univ];
  TYPE_THEN `
UNIONS U x` SUBGOAL_TAC;
  USE 2 (REWRITE_RULE[
SUBSET;
IN;]);
  ASM_MESON_TAC[];
  DISCH_ALL_TAC;
  REWR 8;
  ASM_REWRITE_TAC[];
  (* dd *)
  CONJ_TAC;
  EXPAND_TAC "B";
 
let open_ball_star = prove_by_refinement(
  `!x r y t n. (open_ball(euclid n,d_euclid) x r y) /\
    (&.0 <=. t) /\ (t <=. &.1) ==>
   (open_ball(euclid n,d_euclid) x r ((t *# x + (&.1-t)*#y)))`,
 
let open_ball_path = prove_by_refinement(
  `!x r y n. (open_ball(euclid n,d_euclid) x r y) ==>
    (
path_component
      (top_of_metric(open_ball(euclid n,d_euclid) x r,d_euclid)) y x)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[
path_component ;];
  DISCH_ALL_TAC;
  TYPE_THEN `(\t. (t *# x + (&.1 - t) *# y))` EXISTS_TAC;
  EXISTS_TAC `&.0`;
  EXISTS_TAC `&.1`;
  REDUCE_TAC;
  TYPE_THEN `top_of_metric (open_ball (euclid n,d_euclid) x r,d_euclid) = (induced_top(top_of_metric(euclid n,d_euclid)) (open_ball (euclid n,d_euclid) x r))` SUBGOAL_TAC;
  ASM_MESON_TAC[
open_ball_subset;
metric_euclid;
top_of_metric_induced ];
  DISCH_TAC ;
  TYPE_THEN `euclid n x /\ euclid n y` SUBGOAL_TAC;
  USE 0 (REWRITE_RULE[open_ball;IN_ELIM_THM' ]);
  ASM_REWRITE_TAC[];
  DISCH_ALL_TAC;
  CONJ_TAC;
  ASM_REWRITE_TAC[];
  IMATCH_MP_TAC 
continuous_induced;
  ASM_SIMP_TAC [
top_of_metric_top;
metric_euclid;
open_ball_open];
  IMATCH_MP_TAC  
continuous_lin_combo ;
  ASM_REWRITE_TAC[];
  CONJ_TAC;
  REWRITE_TAC[euclid_plus;euclid_scale];
  IMATCH_MP_TAC  
EQ_EXT THEN BETA_TAC ;
  REDUCE_TAC;
  CONJ_TAC;
  REWRITE_TAC[euclid_plus;euclid_scale];
  IMATCH_MP_TAC  
EQ_EXT THEN BETA_TAC ;
  REDUCE_TAC;
  REWRITE_TAC[
SUBSET;
IN_IMAGE;Q_ELIM_THM'' ];
  REWRITE_TAC[
IN;IN_ELIM_THM'];
  TYPE_THEN `(
UNIONS (top_of_metric (open_ball (euclid n,d_euclid) x r,d_euclid))) = (open_ball(euclid n,d_euclid) x r)` SUBGOAL_TAC;
  IMATCH_MP_TAC  (GSYM 
top_of_metric_unions);
  IMATCH_MP_TAC  
metric_subspace;
  ASM_MESON_TAC[
metric_euclid;
open_ball_subset];
  DISCH_THEN (fun t->REWRITE_TAC[t]);
  ASM_MESON_TAC [
open_ball_star];
  ]);;