legacy/oldfan/fantopology.ml

   1 (* ========================================================================= *)\r
   2 (* Elementary topology in Euclidean space.                                   *)\r
   3 (* ========================================================================= *)\r
   4 \r
   5 parse_as_infix ("open_in",(12,"right"));;\r
   6 parse_as_infix ("closed_in",(12,"right"));;\r
   7 \r
   8 let open_in = new_definition\r
   9   `s open_in u <=>\r
  10         s SUBSET u /\\r
  11         !x. x IN s ==> ?e. &0 < e /\\r
  12                            !x'. x' IN u /\ dist(x',x) < e ==> x' IN s`;;\r
  13 \r
  14 let closed_in = new_definition\r
  15   `s closed_in u <=> s SUBSET u /\ (u DIFF s) open_in u`;;\r
  16 \r
  17 let OPEN_IN_SUBSET = prove\r
  18  (`!s u. s open_in u ==> s SUBSET u`,\r
  19   SIMP_TAC[open_in]);;\r
  20 \r
  21 let OPEN_IN_EMPTY = prove\r
  22  (`!u. {} open_in u`,\r
  23   REWRITE_TAC[open_in; EMPTY_SUBSET; NOT_IN_EMPTY]);;\r
  24 \r
  25 let OPEN_IN_REFL = prove\r
  26  (`!u. u open_in u`,\r
  27   SIMP_TAC[open_in; SUBSET_REFL] THEN MESON_TAC[REAL_LT_01]);;\r
  28 \r
  29 let OPEN_IN_UNIONS = prove\r
  30  (`!u. (!s. s IN f ==> s open_in u) ==> (UNIONS f) open_in u`,\r
  31   REWRITE_TAC[open_in; SUBSET; IN_UNIONS] THEN MESON_TAC[]);;\r
  32 \r
  33 let OPEN_IN_UNION = prove\r
  34  (`!s t u. s open_in u /\ t open_in u ==> (s UNION t) open_in u`,\r
  35   REWRITE_TAC[open_in; IN_UNION; SUBSET] THEN MESON_TAC[]);;\r
  36 \r
  37 let OPEN_IN_INTER = prove\r
  38  (`!s t u. s open_in u /\ t open_in u ==> (s INTER t) open_in u`,\r
  39   REPEAT GEN_TAC THEN REWRITE_TAC[open_in; IN_INTER] THEN MATCH_MP_TAC(TAUT\r
  40    `(a /\ c ==> e) /\ (b /\ d ==> f) ==> (a /\ b) /\ (c /\ d) ==> e /\ f`) THEN\r
  41   CONJ_TAC THENL [SET_TAC[]; ALL_TAC] THEN\r
  42   REWRITE_TAC[AND_FORALL_THM] THEN MATCH_MP_TAC MONO_FORALL THEN\r
  43   GEN_TAC THEN DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN\r
  44   ASM_REWRITE_TAC[] THEN DISCH_THEN(CONJUNCTS_THEN2\r
  45    (X_CHOOSE_TAC `d1:real`) (X_CHOOSE_TAC `d2:real`)) THEN\r
  46   MP_TAC(SPECL [`d1:real`; `d2:real`] REAL_DOWN2) THEN\r
  47   ASM_MESON_TAC[REAL_LT_TRANS]);;\r
  48 \r
  49 let OPEN_IN_SUBOPEN = prove\r
  50  (`!s u. s open_in u <=>\r
  51          !x. x IN s ==> ?t. t open_in u /\ x IN t /\ t SUBSET s`,\r
  52   REPEAT GEN_TAC THEN EQ_TAC THENL\r
  53    [MESON_TAC[SUBSET_REFL]; REWRITE_TAC[open_in; SUBSET] THEN MESON_TAC[]]);;\r
  54 \r
  55 let CLOSED_IN_SUBSET = prove\r
  56  (`!s u. s closed_in u ==> s SUBSET u`,\r
  57   SIMP_TAC[closed_in]);;\r
  58 \r
  59 let CLOSED_IN_EMPTY = prove\r
  60  (`!u. {} closed_in u`,\r
  61   REWRITE_TAC[closed_in; EMPTY_SUBSET; DIFF_EMPTY; OPEN_IN_REFL]);;\r
  62 \r
  63 let CLOSED_IN_REFL = prove\r
  64  (`!u. u closed_in u`,\r
  65   REWRITE_TAC[closed_in; SUBSET_REFL; DIFF_EQ_EMPTY; OPEN_IN_EMPTY]);;\r
  66 \r
  67 let CLOSED_IN_UNION = prove\r
  68  (`!s t u. s closed_in u /\ t closed_in u ==> (s UNION t) closed_in u`,\r
  69   let lemma = prove\r
  70    (`s DIFF (t UNION u) = (s DIFF t) INTER (s DIFF u)`,SET_TAC[]) in\r
  71   SIMP_TAC[closed_in; lemma; OPEN_IN_INTER] THEN SET_TAC[]);;\r
  72 \r
  73 let CLOSED_IN_INTER = prove\r
  74  (`!s t u. s closed_in u /\ t closed_in u ==> (s INTER t) closed_in u`,\r
  75   let lemma = prove\r
  76    (`s DIFF (t INTER u) = (s DIFF t) UNION (s DIFF u)`,SET_TAC[]) in\r
  77   SIMP_TAC[closed_in; lemma; OPEN_IN_UNION] THEN SET_TAC[]);;\r
  78 \r
  79 let CLOSED_IN_INTERS = prove\r
  80  (`!u. ~(f = {}) /\ (!s. s IN f ==> s closed_in u) ==> (INTERS f) closed_in u`,\r
  81   let lemma = prove\r
  82    (`s DIFF (INTERS f) = UNIONS {t | ?u. u IN f /\ (t = s DIFF u)}`,\r
  83     GEN_REWRITE_TAC I [EXTENSION] THEN\r
  84     REWRITE_TAC[IN_DIFF; IN_UNIONS; IN_INTERS; IN_ELIM_THM] THEN\r
  85     MESON_TAC[IN_DIFF]) in\r
  86   REWRITE_TAC[closed_in; lemma] THEN REPEAT STRIP_TAC THEN\r
  87   ASM_SIMP_TAC[OPEN_IN_UNIONS; IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN\r
  88   POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN SET_TAC[]);;\r
  89 \r
  90 let OPEN_IN_CLOSED_IN = prove\r
  91  (`!s u. s SUBSET u ==> (s open_in u <=> (u DIFF s) closed_in u)`,\r
  92   REPEAT GEN_TAC THEN REWRITE_TAC[closed_in; SUBSET_DIFF] THEN\r
  93   REWRITE_TAC[open_in; IN_DIFF; IN_DIFF; SUBSET] THEN MESON_TAC[]);;\r
  94 \r
  95 let OPEN_IN_CLOSED_IN_EQ = prove\r
  96  (`!s u. s open_in u <=> s SUBSET u /\ (u DIFF s) closed_in u`,\r
  97   MESON_TAC[OPEN_IN_CLOSED_IN; OPEN_IN_SUBSET]);;\r
  98 \r
  99 let OPEN_IN_DIFF = prove\r
 100  (`!s t u. s open_in u /\ t closed_in u ==> (s DIFF t) open_in u`,\r
 101   let lemma = prove\r
 102    (`s SUBSET u ==> ((s DIFF t) = s INTER (u DIFF t))`,SET_TAC[]) in\r
 103   SIMP_TAC[OPEN_IN_SUBSET; lemma; closed_in; OPEN_IN_INTER]);;\r
 104 \r
 105 let CLOSED_IN_DIFF = prove\r
 106  (`!s t u. s closed_in u /\ t open_in u ==> (s DIFF t) closed_in u`,\r
 107   let lemma = prove\r
 108    (`s SUBSET u ==> ((s DIFF t) = s INTER (u DIFF t))`,SET_TAC[]) in\r
 109   SIMP_TAC[CLOSED_IN_SUBSET; lemma] THEN\r
 110   SIMP_TAC[CLOSED_IN_INTER; GSYM OPEN_IN_CLOSED_IN; OPEN_IN_SUBSET]);;\r
 111 \r
 112 \r
 113 \r
 114 (* ------------------------------------------------------------------------- *)\r
 115 (* The "universal" versions are what we use most of the time.                *)\r
 116 (* ------------------------------------------------------------------------- *)\r
 117 \r
 118 let open_def_fan = new_definition\r
 119   `open_fan s <=> !x. x IN s ==> ?e. &0 < e /\ !x'. dist(x',x) < e ==> x' IN s`;;\r
 120 \r
 121 let closed_fan = new_definition\r
 122   `closed_fan(s:real^N->bool) <=> open_fan(UNIV DIFF s)`;;\r
 123 \r
 124 let OPEN_IN_FAN = prove\r
 125  (`!s:real^N->bool. open_fan s <=> s open_in UNIV`,\r
 126   REWRITE_TAC[open_def_fan; open_in; SUBSET_UNIV; IN_UNIV]);;\r
 127 \r
 128 \r
 129 let CLOSED_IN_FAN = prove\r
 130  (`!s:real^N->bool. closed_fan s <=> s closed_in UNIV`,\r
 131   REWRITE_TAC[closed_fan; closed_in; SUBSET_UNIV; OPEN_IN_FAN]);;\r
 132 \r
 133 let OPEN_EMPTY_FAN = prove\r
 134  (`open_fan {}`,\r
 135   REWRITE_TAC[OPEN_IN_FAN; OPEN_IN_EMPTY]);;\r
 136 \r
 137 let OPEN_UNIV_FAN = prove\r
 138  (`open_fan(UNIV:real^N->bool)`,\r
 139   REWRITE_TAC[OPEN_IN_FAN; OPEN_IN_REFL]);;\r
 140 \r
 141 let OPEN_UNIONS_FAN = prove\r
 142  (`(!s. s IN f ==> open_fan s) ==> open_fan(UNIONS f)`,\r
 143   REWRITE_TAC[OPEN_IN_FAN; OPEN_IN_UNIONS]);;\r
 144 \r
 145 let OPEN_UNION_FAN = prove\r
 146  (`!s t. open_fan s /\ open_fan t ==> open_fan(s UNION t)`,\r
 147   REWRITE_TAC[OPEN_IN_FAN; OPEN_IN_UNION]);;\r
 148 \r
 149 let OPEN_INTER_FAN = prove\r
 150  (`!s t. open_fan s /\ open_fan t ==> open_fan(s INTER t)`,\r
 151   REWRITE_TAC[OPEN_IN_FAN; OPEN_IN_INTER]);;\r
 152 \r
 153 let OPEN_SUBOPEN_FAN = prove\r
 154  (`!s. open_fan s <=> !x. x IN s ==> ?t. open_fan t /\ x IN t /\ t SUBSET s`, \r
 155 REWRITE_TAC[OPEN_IN_FAN; GSYM OPEN_IN_SUBOPEN]);;\r
 156 \r
 157 let CLOSED_EMPTY_FAN = prove\r
 158  (`closed_fan {}`,\r
 159   REWRITE_TAC[CLOSED_IN_FAN; CLOSED_IN_EMPTY]);;\r
 160 \r
 161 let CLOSED_UNIV_FAN = prove\r
 162  (`closed_fan(UNIV:real^N->bool)`,\r
 163   REWRITE_TAC[CLOSED_IN_FAN; CLOSED_IN_REFL]);;\r
 164 \r
 165 let CLOSED_UNION_FAN = prove\r
 166  (`!s t. closed_fan s /\ closed_fan t ==> closed_fan(s UNION t)`,\r
 167   REWRITE_TAC[CLOSED_IN_FAN; CLOSED_IN_UNION]);;\r
 168 \r
 169 let CLOSED_INTER_FAN = prove\r
 170  (`!s t. closed_fan s /\ closed_fan t ==> closed_fan(s INTER t)`,\r
 171   REWRITE_TAC[CLOSED_IN_FAN; CLOSED_IN_INTER]);;\r
 172 \r
 173 let lemma_closed_inters_fan1 = prove\r
 174    (`s DIFF (INTERS f) = UNIONS {t | ?u. u IN f /\ (t = s DIFF u)}`,\r
 175     GEN_REWRITE_TAC I [EXTENSION] THEN\r
 176     REWRITE_TAC[IN_DIFF; IN_UNIONS; IN_INTERS; IN_ELIM_THM] THEN\r
 177     MESON_TAC[IN_DIFF]);;\r
 178 \r
 179 let CLOSED_INTERS_FAN = prove(\r
 180 `!f. (!s:real^N->bool. s IN f ==> closed_fan s) ==> closed_fan(INTERS f)`,\r
 181    REWRITE_TAC[closed_fan; lemma_closed_inters_fan1] THEN REPEAT STRIP_TAC THEN\r
 182   ASM_SIMP_TAC[OPEN_UNIONS_FAN; IN_ELIM_THM; LEFT_IMP_EXISTS_THM]);;\r
 183 \r
 184 let OPEN_CLOSED_FAN = prove\r
 185  (`!s:real^N->bool. open_fan s <=> closed_fan(UNIV DIFF s)`,\r
 186   SIMP_TAC[OPEN_IN_FAN; CLOSED_IN_FAN; OPEN_IN_CLOSED_IN; SUBSET_UNIV]);;\r
 187 \r
 188 let OPEN_DIFF_FAN = prove\r
 189  (`!s t. open_fan s /\ closed_fan t ==> open_fan(s DIFF t)`,\r
 190   REWRITE_TAC[OPEN_IN_FAN; CLOSED_IN_FAN; OPEN_IN_DIFF]);;\r
 191 \r
 192 let CLOSED_DIFF_FAN = prove\r
 193  (`!s t. closed_fan s /\ open_fan t ==> closed_fan(s DIFF t)`,\r
 194   REWRITE_TAC[OPEN_IN_FAN; CLOSED_IN_FAN; CLOSED_IN_DIFF]);;\r
 195 \r
 196 let OPEN_INTERS_FAN = prove\r
 197  (`!s. FINITE s /\ (!t. t IN s ==> open_fan t) ==> open_fan(INTERS s)`,\r
 198 REWRITE_TAC[GSYM IMP_IMP] THEN MATCH_MP_TAC FINITE_INDUCT_STRONG\r
 199   THEN REWRITE_TAC[INTERS_INSERT; INTERS_0; OPEN_UNIV_FAN; IN_INSERT] THEN\r
 200   MESON_TAC[OPEN_INTER_FAN]);;\r
 201 \r
 202 let CLOSED_UNIONS_FAN = prove\r
 203  (`!s. FINITE s /\ (!t. t IN s ==> closed_fan t) ==> closed_fan(UNIONS s)`,\r
 204   REWRITE_TAC[GSYM IMP_IMP] THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN\r
 205   REWRITE_TAC[UNIONS_INSERT; UNIONS_0; CLOSED_EMPTY_FAN; IN_INSERT] THEN\r
 206   MESON_TAC[CLOSED_UNION_FAN]);;\r
 207 \r
 208 \r
 209 \r
 210 (* ------------------------------------------------------------------------- *)\r
 211 (* Open balls.                                                               *)\r
 212 (* ------------------------------------------------------------------------- *)\r
 213 \r
 214 \r
 215 let ball_fan = new_definition\r
 216   `ball_fan(x,e) = { y | dist(x,y) < e}`;;\r
 217 \r
 218 let IN_BALL_FAN = prove\r
 219  (`!x y e. y IN (ball_fan(x,e)) <=> dist(x,y) < e`,\r
 220   REWRITE_TAC[ball_fan; IN_ELIM_THM]);;\r
 221 \r
 222 let OPEN_BALL_FAN = prove\r
 223  (`!x e. open_fan(ball_fan(x,e))`,\r
 224   REWRITE_TAC[open_def_fan; ball_fan; IN_ELIM_THM] \r
 225   THEN ONCE_REWRITE_TAC[DIST_SYM] THEN\r
 226   MESON_TAC[REAL_SUB_LT; REAL_LT_SUB_LADD; REAL_ADD_SYM; REAL_LET_TRANS;\r
 227             DIST_TRIANGLE_ALT]);;\r
 228 \r
 229 let CENTRE_IN_BALL = prove\r
 230  (`!x e. x IN ball_fan(x,e) <=> &0 < e`,\r
 231   MESON_TAC[IN_BALL_FAN; DIST_REFL]);;\r
 232 \r
 233 let OPEN_CONTAINS_BALL_FAN = prove\r
 234  (`!s. open_fan s <=> !x. x IN s ==> ?e. &0 < e /\ ball_fan(x,e) SUBSET s`,\r
 235   REWRITE_TAC[open_def_fan; SUBSET; IN_BALL_FAN] THEN REWRITE_TAC[DIST_SYM]);;\r
 236 \r
 237 let BALL_EQ_EMPTY_FAN = prove\r
 238  (`!x e. (ball_fan(x,e) = {}) <=> e <= &0`,\r
 239   REWRITE_TAC[EXTENSION; IN_BALL_FAN; NOT_IN_EMPTY; REAL_NOT_LT] THEN\r
 240   MESON_TAC[DIST_POS_LE; REAL_LE_TRANS; DIST_REFL]);;\r
 241 \r
 242 (* ------------------------------------------------------------------------- *)\r
 243 (* Basic "localization" results are handy for connectedness.                 *)\r
 244 (* ------------------------------------------------------------------------- *)\r
 245 \r
 246  let OPEN_IN_OPEN_FAN = prove\r
 247  (`!s:real^N->bool u. s open_in u <=> ?t. open_fan t /\ (s = u INTER t)`,\r
 248   REPEAT GEN_TAC THEN EQ_TAC THENL\r
 249    [REWRITE_TAC[open_in] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC);\r
 250     DISCH_THEN(CHOOSE_THEN(CONJUNCTS_THEN2 MP_TAC SUBST_ALL_TAC)) THEN\r
 251     REWRITE_TAC[open_def_fan; open_in; SUBSET; IN_INTER] THEN MESON_TAC[]] THEN\r
 252   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [RIGHT_IMP_EXISTS_THM] THEN\r
 253   REWRITE_TAC[SKOLEM_THM] THEN DISCH_THEN(X_CHOOSE_TAC `d:real^N->real`) THEN\r
 254   EXISTS_TAC `UNIONS {b | ?x:real^N. (b = ball_fan(x,d x)) /\ x IN s}` THEN\r
 255   CONJ_TAC THENL\r
 256    [MATCH_MP_TAC OPEN_UNIONS_FAN THEN\r
 257     ASM_SIMP_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM; OPEN_BALL_FAN];\r
 258     GEN_REWRITE_TAC I [EXTENSION] THEN\r
 259     REWRITE_TAC[IN_INTER; IN_UNIONS; IN_ELIM_THM] THEN\r
 260     ASM_MESON_TAC[SUBSET; DIST_REFL; DIST_SYM; IN_BALL_FAN]]);;\r
 261 \r
 262 let CLOSED_IN_CLOSED_FAN = prove\r
 263  (`!s:real^N->bool u. s closed_in u <=> ?t. closed_fan t /\ (s = u INTER t)`,\r
 264   REPEAT GEN_TAC THEN REWRITE_TAC[closed_in; closed_fan; OPEN_IN_OPEN_FAN] THEN\r
 265   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [GSYM EXISTS_DIFF] THEN\r
 266   REWRITE_TAC[RIGHT_AND_EXISTS_THM] THEN AP_TERM_TAC THEN ABS_TAC THEN\r
 267   SET_TAC[]);;\r
 268 \r
 269 (* ------------------------------------------------------------------------- *)\r
 270 (* These "transitivity" results are handy too.                               *)\r
 271 (* ------------------------------------------------------------------------- *)\r
 272 \r
 273 let OPEN_IN_TRANS_FAN = prove\r
 274  (`!s t u. s open_in t /\ t open_in u ==> s open_in u`,\r
 275   ASM_MESON_TAC[OPEN_IN_OPEN_FAN; OPEN_INTER_FAN; INTER_ASSOC]);;\r
 276 \r
 277 let OPEN_IN_OPEN_TRANS_FAN = prove\r
 278  (`!s t. s open_in t /\ open_fan t ==> open_fan s`,\r
 279   MESON_TAC[OPEN_IN_FAN; OPEN_IN_TRANS_FAN; OPEN_UNIV_FAN]);;\r
 280 \r
 281 let CLOSED_IN_TRANS_FAN = prove\r
 282  (`!s t u. s closed_in t /\ t closed_in u ==> s closed_in u`,\r
 283   ASM_MESON_TAC[CLOSED_IN_CLOSED_FAN; CLOSED_INTER_FAN; INTER_ASSOC]);;\r
 284 \r
 285 let CLOSED_IN_CLOSED_TRANS_FAN = prove\r
 286  (`!s t. s closed_in t /\ closed_fan t ==> closed_fan s`,\r
 287   MESON_TAC[CLOSED_IN_FAN; CLOSED_IN_TRANS_FAN; CLOSED_UNIV_FAN]);;\r
 288 \r
 289 (* ------------------------------------------------------------------------- *)\r
 290 (* Connectedness.                                                            *)\r
 291 (* ------------------------------------------------------------------------- *)\r
 292 \r
 293 \r
 294 let connected_fan = new_definition\r
 295   `connected_fan s <=>\r
 296       ~(?e1 e2. open_fan e1 /\ open_fan e2 /\ s SUBSET (e1 UNION e2) /\\r
 297                 (e1 INTER e2 INTER s = {}) /\\r
 298                 ~(e1 INTER s = {}) /\ ~(e2 INTER s = {}))`;;\r
 299 \r
 300 (* error in old file*)\r
 301 let CONNECTED_CLOPEN_FAN = prove\r
 302  (`!s. connected_fan s <=>\r
 303       !t. t open_in s /\ t closed_in s ==> (t = {}) \/ (t = s)`,\r
 304   GEN_TAC THEN REWRITE_TAC[connected_fan; OPEN_IN_OPEN_FAN; CLOSED_IN_CLOSED_FAN] THEN  GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o BINDER_CONV) [GSYM EXISTS_DIFF] THEN\r
 305   ONCE_REWRITE_TAC[TAUT `(~a <=> b) <=> (a <=> ~b)`] THEN  REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; GSYM CONJ_ASSOC; DE_MORGAN_THM] THEN\r
 306   ONCE_REWRITE_TAC[TAUT `a /\ b /\ c /\ d <=> b /\ a /\ c /\ d`] THEN  \r
 307 REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN REWRITE_TAC[GSYM closed] THEN\r
 308   ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN AP_TERM_TAC THEN ABS_TAC THEN\r
 309   REWRITE_TAC[LEFT_AND_EXISTS_THM; RIGHT_AND_EXISTS_THM] THEN\r
 310   ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN AP_TERM_TAC THEN ABS_TAC THEN\r
 311   REWRITE_TAC[TAUT `(a /\ b) /\ (c /\ d) /\ e <=> a /\ c /\ b /\ d /\ e`] THEN\r
 312   REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM2; closed_fan]\r
 313 THEN AP_TERM_TAC\r
 314 THEN AP_TERM_TAC\r
 315 THEN SET_TAC[]);;\r
 316 \r
 317 \r
 318 let CONNECTED_EMPTY_FAN = prove\r
 319  (`connected_fan {}`,\r
 320   REWRITE_TAC[connected_fan; INTER_EMPTY]);;\r
 321 \r
 322 \r
 323 (* ------------------------------------------------------------------------- *)\r
 324 (* Limit points.                                                             *)\r
 325 (* ------------------------------------------------------------------------- *)\r
 326 \r
 327 parse_as_infix ("limit_point_of_fan",(12,"right"));;\r
 328 \r
 329 \r
 330 let limit_point_of_fan = new_definition\r
 331  `x limit_point_of_fan s <=>\r
 332         !t. x IN t /\ open_fan t ==> ?y. ~(y = x) /\ y IN s /\ y IN t`;;\r
 333 \r
 334 let LIMPT_APPROACHABLE_FAN = prove\r
 335  (`!x s. x limit_point_of_fan s <=>\r
 336                 !e. &0 < e ==> ?x'. x' IN s /\ ~(x' = x) /\ dist(x',x) < e`,\r
 337   REPEAT GEN_TAC THEN REWRITE_TAC[limit_point_of_fan] THEN\r
 338   MESON_TAC[open_def_fan; DIST_SYM; OPEN_BALL_FAN; CENTRE_IN_BALL; IN_BALL_FAN]);;\r
 339 \r
 340 let LIMPT_APPROACHABLE_LE_FAN = prove\r
 341  (`!x s. x limit_point_of_fan s <=>\r
 342                 !e. &0 < e ==> ?x'. x' IN s /\ ~(x' = x) /\ dist(x',x) <= e`,\r
 343   REPEAT GEN_TAC THEN REWRITE_TAC[LIMPT_APPROACHABLE_FAN] THEN\r
 344   MATCH_MP_TAC(TAUT `(~a <=> ~b) ==> (a <=> b)`) THEN\r
 345   REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; NOT_EXISTS_THM] THEN\r
 346   REWRITE_TAC[TAUT `~(a /\ b /\ c) <=> c ==> ~(a /\ b)`; APPROACHABLE_LT_LE]);;\r
 347 \r
 348 let LIMPT_UNIV_FAN = prove\r
 349  (`!x:real^N. x limit_point_of_fan UNIV`,\r
 350   GEN_TAC THEN REWRITE_TAC[LIMPT_APPROACHABLE_FAN; IN_UNIV] THEN\r
 351   X_GEN_TAC `e:real` THEN DISCH_TAC THEN\r
 352   SUBGOAL_THEN `?c:real^N. norm(c) = e / &2` CHOOSE_TAC THENL\r
 353    [ASM_SIMP_TAC[VECTOR_CHOOSE_SIZE; REAL_HALF; REAL_LT_IMP_LE];\r
 354     ALL_TAC] THEN\r
 355   EXISTS_TAC `x + c:real^N` THEN\r
 356   REWRITE_TAC[dist; VECTOR_EQ_ADDR] THEN ASM_REWRITE_TAC[VECTOR_ADD_SUB] THEN\r
 357   SUBGOAL_THEN `&0 < e / &2 /\ e / &2 < e`\r
 358    (fun th -> ASM_MESON_TAC[th; NORM_0; REAL_LT_REFL]) THEN\r
 359   SIMP_TAC[REAL_LT_LDIV_EQ; REAL_LT_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN\r
 360   UNDISCH_TAC `&0 < e` THEN REAL_ARITH_TAC);;\r
 361 \r
 362 let CLOSED_LIMPT_FAN = prove\r
 363  (`!s. closed_fan s <=> !x. x limit_point_of_fan s ==> x IN s`,\r
 364   REWRITE_TAC[closed_fan] THEN ONCE_REWRITE_TAC[OPEN_SUBOPEN_FAN] THEN\r
 365   REWRITE_TAC[limit_point_of_fan; IN_DIFF; IN_UNIV; SUBSET] THEN MESON_TAC[]);;\r
 366 \r
 367 let LIMPT_SUBSET_FAN = prove\r
 368  (`!x s t. x limit_point_of_fan s /\ s SUBSET t ==> x limit_point_of_fan t`,\r
 369   REWRITE_TAC[limit_point_of_fan; SUBSET] THEN MESON_TAC[]);;\r
 370 \r
 371 let LIMPT_EMPTY_FAN = prove\r
 372  (`!x. ~(x limit_point_of_fan {})`,\r
 373   REWRITE_TAC[LIMPT_APPROACHABLE_FAN; NOT_IN_EMPTY] THEN MESON_TAC[REAL_LT_01]);;\r
 374 \r
 375 let CLOSED_POSITIVE_ORTHANT_FAN = prove\r
 376  (`closed_fan {x:real^N | !i. 1 <= i /\ i <= dimindex(:N)\r
 377                           ==> &0 <= x$i}`,\r
 378   REWRITE_TAC[CLOSED_LIMPT_FAN; LIMPT_APPROACHABLE_FAN] THEN\r
 379   REWRITE_TAC[IN_ELIM_THM] THEN X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN\r
 380   X_GEN_TAC `i:num` THEN STRIP_TAC THEN REWRITE_TAC[GSYM REAL_NOT_LT] THEN\r
 381   DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `--(x:real^N $ i)`) THEN\r
 382   ASM_REWRITE_TAC[REAL_LT_RNEG; REAL_ADD_LID; NOT_EXISTS_THM] THEN\r
 383   X_GEN_TAC `y:real^N` THEN\r
 384   MATCH_MP_TAC(TAUT `(a ==> ~c) ==> ~(a /\ b /\ c)`) THEN DISCH_TAC THEN\r
 385   MATCH_MP_TAC(REAL_ARITH `!b. abs x <= b /\ b <= a ==> ~(a + x < &0)`) THEN\r
 386   EXISTS_TAC `abs((y - x :real^N)$i)` THEN\r
 387   ASM_SIMP_TAC[dist; COMPONENT_LE_NORM] THEN\r
 388   ASM_SIMP_TAC[VECTOR_SUB_COMPONENT; REAL_ARITH\r
 389    `x < &0 /\ &0 <= y ==> abs(x) <= abs(y - x)`]);;\r
 390 \r
 391 (* ------------------------------------------------------------------------- *)\r
 392 (* Interior of a set.                                                        *)\r
 393 (* ------------------------------------------------------------------------- *)\r
 394 \r
 395 let interior_fan = new_definition\r
 396   `interior_fan s = {x | ?t. open_fan t /\ x IN t /\ t SUBSET s}`;;\r
 397 \r
 398 let INTERIOR_EQ_FAN = prove\r
 399  (`!s. (interior_fan s = s) <=> open_fan s`,\r
 400   GEN_TAC THEN REWRITE_TAC[EXTENSION; interior_fan; IN_ELIM_THM] THEN\r
 401   GEN_REWRITE_TAC RAND_CONV [OPEN_SUBOPEN_FAN] THEN MESON_TAC[SUBSET]);;\r
 402 \r
 403 let INTERIOR_OPEN_FAN = prove\r
 404  (`!s. open_fan s ==> (interior_fan s = s)`,\r
 405   MESON_TAC[INTERIOR_EQ_FAN]);;\r
 406 \r
 407 let OPEN_INTERIOR_FAN = prove\r
 408  (`!s. open_fan(interior_fan s)`,\r
 409   GEN_TAC THEN REWRITE_TAC[interior_fan] THEN GEN_REWRITE_TAC I [OPEN_SUBOPEN_FAN] THEN\r
 410   REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN MESON_TAC[]);;\r
 411 \r
 412 let INTERIOR_INTERIOR_FAN = prove\r
 413  (`!s. interior_fan(interior_fan s) = interior_fan s`,\r
 414   MESON_TAC[INTERIOR_EQ_FAN; OPEN_INTERIOR_FAN]);;\r
 415 \r
 416 let INTERIOR_SUBSET_FAN = prove\r
 417  (`!s. (interior_fan s) SUBSET s`,\r
 418   REWRITE_TAC[SUBSET; interior_fan; IN_ELIM_THM] THEN MESON_TAC[]);;\r
 419 \r
 420 let SUBSET_INTERIOR_FAN = prove\r
 421  (`!s t. s SUBSET t ==> (interior_fan s) SUBSET (interior_fan t)`,\r
 422   REWRITE_TAC[interior_fan; SUBSET; IN_ELIM_THM] THEN MESON_TAC[]);;\r
 423 \r
 424 let INTERIOR_MAXIMAL_FAN = prove\r
 425  (`!s t. t SUBSET s /\ open_fan t ==> t SUBSET (interior_fan s)`,\r
 426   REWRITE_TAC[interior_fan; SUBSET; IN_ELIM_THM] THEN MESON_TAC[]);;\r
 427 \r
 428 let INTERIOR_UNIQUE_FAN = prove\r
 429  (`!s t. t SUBSET s /\ open_fan t /\ (!t'. t' SUBSET s /\ open_fan t' ==> t' SUBSET t)\r
 430          ==> (interior_fan s = t)`,\r
 431   MESON_TAC[SUBSET_ANTISYM; INTERIOR_MAXIMAL_FAN; INTERIOR_SUBSET_FAN;\r
 432             OPEN_INTERIOR_FAN]);;\r
 433 \r
 434 let IN_INTERIOR_FAN = prove\r
 435  (`!x s. x IN interior_fan s <=> ?e. &0 < e /\ ball_fan(x,e) SUBSET s`,\r
 436   REWRITE_TAC[interior_fan; IN_ELIM_THM] THEN\r
 437   MESON_TAC[OPEN_CONTAINS_BALL_FAN; SUBSET_TRANS; CENTRE_IN_BALL; OPEN_BALL_FAN]);;\r
 438 \r
 439 (* ------------------------------------------------------------------------- *)\r
 440 (* Closure of a set.                                                         *)\r
 441 (* ------------------------------------------------------------------------- *)\r
 442 \r
 443 let closure_fan = new_definition\r
 444   `closure_fan s = s UNION {x | x limit_point_of_fan s}`;;\r
 445 \r
 446 let CLOSURE_INTERIOR_FAN = prove\r
 447  (`!s:real^N->bool. closure_fan s = UNIV DIFF (interior_fan (UNIV DIFF s))`,\r
 448   REWRITE_TAC[EXTENSION; closure_fan; IN_UNION; IN_DIFF; IN_UNIV; interior_fan;\r
 449               IN_ELIM_THM; limit_point_of_fan; SUBSET] THEN\r
 450   MESON_TAC[]);;\r
 451 \r
 452 let lemma_interior_closure = prove(`!s t. UNIV DIFF (UNIV DIFF t) = t`,SET_TAC[]);;\r
 453 \r
 454 let INTERIOR_CLOSURE_FAN = prove\r
 455  (`!s:real^N->bool. interior_fan s = UNIV DIFF (closure_fan (UNIV DIFF s))`,\r
 456     REWRITE_TAC[CLOSURE_INTERIOR_FAN; lemma_interior_closure]);;\r
 457 \r
 458   let lemma_closed_closure = prove(`UNIV DIFF (UNIV DIFF s) = s`,SET_TAC[]);;\r
 459 \r
 460 let CLOSED_CLOSURE_FAN = prove\r
 461  (`!s. closed_fan(closure_fan s)`,\r
 462    REWRITE_TAC[closed_fan; CLOSURE_INTERIOR_FAN; lemma_closed_closure; OPEN_INTERIOR_FAN]);;\r
 463 \r
 464 let CLOSURE_HULL_FAN = prove\r
 465  (`!s. closure_fan s = closed_fan hull s`,\r
 466   GEN_TAC THEN MATCH_MP_TAC(GSYM HULL_UNIQUE) THEN\r
 467   REWRITE_TAC[CLOSED_CLOSURE_FAN; SUBSET] THEN\r
 468   REWRITE_TAC[closure_fan; IN_UNION; IN_ELIM_THM; CLOSED_LIMPT_FAN] THEN\r
 469   MESON_TAC[limit_point_of_fan]);;\r
 470 \r
 471 let CLOSURE_EQ_FAN = prove\r
 472  (`(closure_fan s = s) <=> closed_fan s`,\r
 473   SIMP_TAC[CLOSURE_HULL_FAN; HULL_EQ; CLOSED_INTERS_FAN]);;\r
 474 \r
 475 let CLOSURE_CLOSED_FAN = prove\r
 476  (`!s. closed_fan s ==> (closure_fan s = s)`,\r
 477   MESON_TAC[CLOSURE_EQ_FAN]);;\r
 478 \r
 479 let CLOSURE_CLOSURE_FAN = prove\r
 480  (`!s. closure_fan (closure_fan s) = closure_fan s`,\r
 481   REWRITE_TAC[CLOSURE_HULL_FAN; HULL_HULL]);;\r
 482 \r
 483 let CLOSURE_SUBSET_FAN = prove\r
 484  (`!s. s SUBSET (closure_fan s)`,\r
 485   REWRITE_TAC[CLOSURE_HULL_FAN; HULL_SUBSET]);;\r
 486 \r
 487 let SUBSET_CLOSURE_FAN = prove\r
 488  (`!s t. s SUBSET t ==> (closure_fan s) SUBSET (closure_fan t)`,\r
 489   REWRITE_TAC[CLOSURE_HULL_FAN; HULL_MONO]);;\r
 490 \r
 491 let CLOSURE_MINIMAL_FAN = prove\r
 492  (`!s t. s SUBSET t /\ closed_fan t ==> (closure_fan s) SUBSET t`,\r
 493   REWRITE_TAC[HULL_MINIMAL; CLOSURE_HULL_FAN]);;\r
 494 \r
 495 let CLOSURE_UNIQUE_FAN = prove\r
 496  (`!s t. s SUBSET t /\ closed_fan t /\\r
 497          (!t'. s SUBSET t' /\ closed_fan t' ==> t SUBSET t')\r
 498          ==> (closure_fan s = t)`,\r
 499   REWRITE_TAC[CLOSURE_HULL_FAN; HULL_UNIQUE]);;\r
 500 \r
 501 (* ------------------------------------------------------------------------- *)\r
 502 (* Frontier (aka boundary).                                                  *)\r
 503 (* ------------------------------------------------------------------------- *)\r
 504 \r
 505 let frontier_fan = new_definition\r
 506   `frontier_fan s = (closure_fan s) DIFF (interior_fan s)`;;\r
 507 \r
 508 let FRONTIER_CLOSED_FAN = prove\r
 509  (`!s. closed_fan(frontier_fan s)`,\r
 510   SIMP_TAC[frontier_fan; CLOSED_DIFF_FAN; CLOSED_CLOSURE_FAN; OPEN_INTERIOR_FAN]);;\r
 511 \r
 512   let frotier_closures_fan = prove(`s DIFF (UNIV DIFF t) = s INTER t`,SET_TAC[]);;\r
 513 \r
 514 let FRONTIER_CLOSURES_FAN = prove\r
 515  (`!s:real^N->bool. frontier_fan s = (closure_fan s) INTER (closure_fan(UNIV DIFF s))`,\r
 516   REWRITE_TAC[frontier_fan; INTERIOR_CLOSURE_FAN; frotier_closures_fan]);;\r
 517 \r
 518 \r
 519 let FRONTIER_STRADDLE_FAN = prove\r
 520  (`!a:real^N s.\r
 521      a IN frontier_fan s <=>\r
 522         !e. &0 < e ==> (?x. x IN s /\ dist(a,x) < e) /\\r
 523                        (?x. ~(x IN s) /\ dist(a,x) < e)`,\r
 524   REPEAT GEN_TAC THEN REWRITE_TAC[FRONTIER_CLOSURES_FAN; IN_INTER] THEN\r
 525   REWRITE_TAC[closure_fan; IN_UNION; IN_ELIM_THM; limit_point_of_fan;\r
 526               IN_UNIV; IN_DIFF] THEN\r
 527   ASM_MESON_TAC[IN_BALL_FAN; SUBSET; OPEN_CONTAINS_BALL_FAN;\r
 528                 CENTRE_IN_BALL; OPEN_BALL_FAN; DIST_REFL]);;\r
 529 \r
 530 let FRONTIER_SUBSET_CLOSED_FAN = prove\r
 531  (`!s. closed_fan s ==> (frontier_fan s) SUBSET s`,\r
 532   MESON_TAC[frontier_fan; CLOSURE_CLOSED_FAN; SUBSET_DIFF]);;\r
 533 \r
 534 \r
 535 \r
 536 \r
 537 \r
 538 (* ------------------------------------------------------------------------- *)\r
 539 (* A variant of nets (slightly non-standard but good for our purposes).      *)\r
 540 (* ------------------------------------------------------------------------- *)\r
 541 \r
 542 let net_tybij_fan = new_type_definition "net_fan" ("mk_net_fan","netord_fan")\r
 543  (prove\r
 544    (`?g:A->A->bool. !x y. (!z. g z x ==> g z y) \/ (!z. g z y ==> g z x)`,\r
 545     EXISTS_TAC `\x:A y:A. F` THEN REWRITE_TAC[]));;\r
 546 \r
 547 let NET_FAN = prove\r
 548  (`!n x y. (!z. netord_fan n z x ==> netord_fan n z y) \/\r
 549            (!z. netord_fan n z y ==> netord_fan n z x)`,\r
 550    REWRITE_TAC[net_tybij_fan; ETA_AX]);;\r
 551 \r
 552 let OLDNET_FAN = prove\r
 553  (`!n x y. netord_fan n x x /\ netord_fan n y y\r
 554            ==> ?z. netord_fan n z z /\\r
 555                    !w. netord_fan n w z ==> netord_fan n w x /\ netord_fan n w y`,\r
 556   MESON_TAC[NET_FAN]);;\r
 557 \r
 558 (* ------------------------------------------------------------------------- *)\r
 559 (* Common nets and the "within" modifier for nets.                           *)\r
 560 (* ------------------------------------------------------------------------- *)\r
 561 \r
 562 parse_as_infix("within_fan",(14,"right"));;\r
 563 parse_as_infix("in_direction_fan",(14,"right"));;\r
 564 \r
 565 let at_fan = new_definition\r
 566   `at_fan a = mk_net_fan(\x y. &0 < dist(x,a) /\ dist(x,a) <= dist(y,a))`;;\r
 567 \r
 568 let at_infinity_fan = new_definition\r
 569   `at_infinity_fan = mk_net_fan(\x y. norm(x) >= norm(y))`;;\r
 570 \r
 571 let sequentially_fan = new_definition\r
 572   `sequentially_fan = mk_net_fan(\m:num n. m >= n)`;;\r
 573 \r
 574 let within_fan = new_definition\r
 575   `net_fan within_fan s = mk_net_fan(\x y. netord_fan net_fan x y /\ x IN s)`;;\r
 576 \r
 577 let in_direction_fan = new_definition\r
 578   `a in_direction_fan v = (at_fan a) within_fan {b | ?c. &0 <= c /\ (b - a = c % v)}`;;\r
 579 \r
 580 (* ------------------------------------------------------------------------- *)\r
 581 (* Prove that they are all nets.                                             *)\r
 582 (* ------------------------------------------------------------------------- *)\r
 583 \r
 584 let NET_PROVE_FAN_TAC[def] =\r
 585   REWRITE_TAC[GSYM FUN_EQ_THM; def] THEN\r
 586   REWRITE_TAC[ETA_AX] THEN\r
 587   ASM_SIMP_TAC[GSYM(CONJUNCT2 net_tybij_fan)];;\r
 588 \r
 589 let AT_FAN = prove\r
 590  (`!a:real^N x y.\r
 591         netord_fan(at_fan a) x y <=> &0 < dist(x,a) /\ dist(x,a) <= dist(y,a)`,\r
 592   GEN_TAC THEN NET_PROVE_FAN_TAC[at_fan] THEN\r
 593   MESON_TAC[REAL_LE_TOTAL; REAL_LE_REFL; REAL_LE_TRANS; REAL_LET_TRANS]);;\r
 594 \r
 595 let AT_INFINITY_FAN = prove\r
 596  (`!a:real^N x y. netord_fan at_infinity_fan x y <=> norm(x) >= norm(y)`,\r
 597   GEN_TAC THEN NET_PROVE_FAN_TAC[at_infinity_fan] THEN\r
 598   REWRITE_TAC[real_ge; REAL_LE_REFL] THEN\r
 599   MESON_TAC[REAL_LE_TOTAL; REAL_LE_REFL; REAL_LE_TRANS]);;\r
 600 \r
 601 let SEQUENTIALLY_FAN = prove\r
 602  (`!m n. netord_fan sequentially_fan m n <=> m >= n`,\r
 603   NET_PROVE_FAN_TAC[sequentially_fan] THEN REWRITE_TAC[GE; LE_REFL] THEN\r
 604   MESON_TAC[LE_CASES; LE_REFL; LE_TRANS]);;\r
 605 \r
 606 let WITHIN_FAN = prove\r
 607  (`!n s x y. netord_fan(n within_fan s) x y <=> netord_fan n x y /\ x IN s`,\r
 608   GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[within_fan; GSYM FUN_EQ_THM] THEN\r
 609   REWRITE_TAC[GSYM(CONJUNCT2 net_tybij_fan); ETA_AX] THEN\r
 610   MESON_TAC[NET_FAN]);;\r
 611 \r
 612 let IN_DIRECTION_FAN = prove\r
 613  (`!a v x y. netord_fan(a in_direction_fan v) x y <=>\r
 614                 &0 < dist(x,a) /\ dist(x,a) <= dist(y,a) /\\r
 615                  ?c. &0 <= c /\ (x - a = c % v)`,\r
 616   REWRITE_TAC[WITHIN_FAN; AT_FAN; in_direction_fan; IN_ELIM_THM; CONJ_ACI]);;\r
 617 \r
 618 let WITHIN_UNIV_FAN = prove\r
 619  (`!x:real^N. at_fan x within_fan UNIV = at_fan x`,\r
 620   REWRITE_TAC[within_fan; at_fan; IN_UNIV] THEN REWRITE_TAC[ETA_AX; net_tybij_fan]);;\r
 621 \r
 622 (* ------------------------------------------------------------------------- *)\r
 623 (* Identify trivial limits, where we can't approach arbitrarily closely.     *)\r
 624 (* ------------------------------------------------------------------------- *)\r
 625 \r
 626 let trivial_limit_fan = new_definition\r
 627   `trivial_limit_fan net_fan <=>\r
 628      (!a:A b. a = b) \/\r
 629      ?a:A b. ~(a = b) /\ !x. ~(netord_fan(net_fan) x a) /\ ~(netord_fan(net_fan) x b)`;;\r
 630 \r
 631 let TRIVIAL_LIMIT_WITHIN_FAN = prove\r
 632  (`!a:real^N. trivial_limit_fan (at_fan a within_fan s) <=> ~(a limit_point_of_fan s)`,\r
 633   REWRITE_TAC[trivial_limit_fan; LIMPT_APPROACHABLE_LE_FAN; WITHIN_FAN; AT_FAN; DIST_NZ] THEN\r
 634   REPEAT GEN_TAC THEN EQ_TAC THENL\r
 635    [DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL\r
 636      [MESON_TAC[REAL_LT_01; REAL_LT_REFL; VECTOR_CHOOSE_DIST;\r
 637                 DIST_REFL; REAL_LT_IMP_LE];\r
 638       DISCH_THEN(X_CHOOSE_THEN `b:real^N` (X_CHOOSE_THEN `c:real^N`\r
 639         STRIP_ASSUME_TAC)) THEN\r
 640       SUBGOAL_THEN `&0 < dist(a,b:real^N) \/ &0 < dist(a,c:real^N)` MP_TAC THEN\r
 641       ASM_MESON_TAC[DIST_TRIANGLE; DIST_SYM; GSYM DIST_NZ; GSYM DIST_EQ_0;\r
 642                     REAL_ARITH `x <= &0 + &0 ==> ~(&0 < x)`]];\r
 643     REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; LEFT_IMP_EXISTS_THM] THEN\r
 644     X_GEN_TAC `e:real` THEN DISCH_TAC THEN DISJ2_TAC THEN\r
 645     EXISTS_TAC `a:real^N` THEN\r
 646     SUBGOAL_THEN `?b:real^N. dist(a,b) = e` MP_TAC THENL\r
 647      [ASM_SIMP_TAC[VECTOR_CHOOSE_DIST; REAL_LT_IMP_LE]; ALL_TAC] THEN\r
 648     MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `b:real^N` THEN\r
 649     DISCH_THEN(SUBST_ALL_TAC o SYM) THEN\r
 650     ASM_MESON_TAC[REAL_NOT_LE; DIST_REFL; DIST_NZ; DIST_SYM]]);;\r
 651 \r
 652 \r
 653 let TRIVIAL_LIMIT_AT_FAN = prove\r
 654  (`!a. ~(trivial_limit_fan (at_fan a))`,\r
 655   ONCE_REWRITE_TAC[GSYM WITHIN_UNIV_FAN] THEN\r
 656   REWRITE_TAC[TRIVIAL_LIMIT_WITHIN_FAN; LIMPT_UNIV_FAN]);;\r
 657 \r
 658 let TRIVIAL_LIMIT_AT_INFINITY_FAN = prove\r
 659  (`~(trivial_limit_fan at_infinity_fan)`,\r
 660   REWRITE_TAC[trivial_limit_fan; AT_INFINITY_FAN; real_ge] THEN\r
 661   MESON_TAC[REAL_LE_REFL; VECTOR_CHOOSE_SIZE; REAL_LT_01; REAL_LT_LE]);;\r
 662 \r
 663 let TRIVIAL_LIMIT_SEQUENTIALLY_FAN = prove\r
 664  (`~(trivial_limit_fan sequentially_fan)`,\r
 665   REWRITE_TAC[trivial_limit_fan; SEQUENTIALLY_FAN] THEN\r
 666   MESON_TAC[GE_REFL; NOT_SUC]);;\r
 667 \r
 668 (* ------------------------------------------------------------------------- *)\r
 669 (* Limits, defined as vacuously true when the limit is trivial.              *)\r
 670 (* ------------------------------------------------------------------------- *)\r
 671 \r
 672 parse_as_infix("-->",(12,"right"));;\r
 673 \r
 674 let lim_fan = new_definition\r
 675   `(f --> l) net_fan <=>\r
 676         trivial_limit_fan net_fan \/\r
 677         !e. &0 < e ==> ?y. (?x.  netord_fan(net_fan) x y) /\\r
 678                            !x. netord_fan(net_fan) x y ==> dist(f(x),l) < e`;;\r
 679 \r
 680 (* ------------------------------------------------------------------------- *)\r
 681 (* Show that they yield usual definitions in the various cases.              *)\r
 682 (* ------------------------------------------------------------------------- *)\r
 683 \r
 684 let LIM_WITHIN_LE_FAN = prove\r
 685  (`!f:real^M->real^N l a s.\r
 686         (f --> l)(at_fan a within_fan s) <=>\r
 687            !e. &0 < e ==> ?d. &0 < d /\\r
 688                               !x. x IN s /\ &0 < dist(x,a) /\ dist(x,a) <= d\r
 689                                    ==> dist(f(x),l) < e`,\r
 690   REPEAT GEN_TAC THEN\r
 691   REWRITE_TAC[lim_fan; AT_FAN; WITHIN_FAN; TRIVIAL_LIMIT_WITHIN_FAN] THEN\r
 692   REWRITE_TAC[LIMPT_APPROACHABLE_LE_FAN; DIST_NZ] THEN EQ_TAC THENL\r
 693    [DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL\r
 694      [ALL_TAC; MATCH_MP_TAC MONO_FORALL] THEN MESON_TAC[REAL_LTE_TRANS];\r
 695     MATCH_MP_TAC(TAUT `(b ==> a ==> c) ==> (a ==> ~b \/ c)`) THEN\r
 696     DISCH_TAC THEN MATCH_MP_TAC MONO_FORALL THEN\r
 697     X_GEN_TAC `e:real` THEN ASM_CASES_TAC `&0 < e` THEN ASM_REWRITE_TAC[] THEN\r
 698     DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN\r
 699     SUBGOAL_THEN `?b:real^M. dist(a,b) = d` MP_TAC THENL\r
 700      [ASM_SIMP_TAC[VECTOR_CHOOSE_DIST; REAL_LT_IMP_LE]; ALL_TAC] THEN\r
 701     MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `b:real^M` THEN\r
 702     DISCH_THEN(SUBST_ALL_TAC o SYM) THEN\r
 703     ASM_MESON_TAC[REAL_NOT_LE; DIST_REFL; DIST_NZ; DIST_SYM]]);;\r
 704 \r
 705 let LIM_WITHIN_FAN = prove\r
 706  (`!f:real^M->real^N l a s.\r
 707       (f --> l) (at_fan a within_fan s) <=>\r
 708         !e. &0 < e\r
 709             ==> ?d. &0 < d /\\r
 710                     !x. x IN s /\ &0 < dist(x,a) /\ dist(x,a) < d\r
 711                     ==> dist(f(x),l) < e`,\r
 712   REWRITE_TAC[LIM_WITHIN_LE_FAN] THEN\r
 713   ONCE_REWRITE_TAC[TAUT `a /\ b /\ c ==> d <=> c ==> a /\ b ==> d`] THEN\r
 714   REWRITE_TAC[APPROACHABLE_LT_LE]);;\r
 715 \r
 716 let LIM_AT_FAN = prove\r
 717  (`!f l:real^N a:real^M.\r
 718       (f --> l) (at_fan a) <=>\r
 719               !e. &0 < e\r
 720                   ==> ?d. &0 < d /\ !x. &0 < dist(x,a) /\ dist(x,a) < d\r
 721                           ==> dist(f(x),l) < e`,\r
 722   ONCE_REWRITE_TAC[GSYM WITHIN_UNIV_FAN] THEN\r
 723   REWRITE_TAC[LIM_WITHIN_FAN; IN_UNIV]);;\r
 724 \r
 725 let LIM_AT_INFINITY_FAN = prove\r
 726  (`!f l. (f --> l) at_infinity_fan <=>\r
 727                !e. &0 < e ==> ?b. !x. norm(x) >= b ==> dist(f(x),l) < e`,\r
 728   REWRITE_TAC[lim_fan; AT_INFINITY_FAN; TRIVIAL_LIMIT_AT_INFINITY_FAN] THEN\r
 729   REPEAT GEN_TAC THEN EQ_TAC THENL [MESON_TAC[REAL_LE_REFL]; ALL_TAC] THEN\r
 730   MATCH_MP_TAC MONO_FORALL THEN\r
 731   MESON_TAC[real_ge; REAL_LE_REFL; VECTOR_CHOOSE_SIZE;\r
 732     REAL_ARITH `&0 <= b \/ (!x. x >= &0 ==> x >= b)`]);;\r
 733 \r
 734 let LIM_SEQUENTIALLY_FAN = prove\r
 735  (`!s l. (s --> l) sequentially_fan <=>\r
 736           !e. &0 < e ==> ?N. !n. N <= n ==> dist(s(n),l) < e`,\r
 737   REWRITE_TAC[lim_fan; SEQUENTIALLY_FAN; GE; LE_REFL; TRIVIAL_LIMIT_SEQUENTIALLY_FAN] THEN\r
 738   MESON_TAC[LE_REFL]);;\r
 739 \r
 740 (* ------------------------------------------------------------------------- *)\r
 741 (* The expected monotonicity property.                                       *)\r
 742 (* ------------------------------------------------------------------------- *)\r
 743 \r
 744 let LIM_WITHIN_SUBSET_FAN = prove\r
 745  (`!f l a s.\r
 746     (f --> l) (at_fan a within_fan s) /\ t SUBSET s ==> (f --> l) (at_fan a within_fan t)`,\r
 747   REWRITE_TAC[LIM_WITHIN_FAN; SUBSET] THEN MESON_TAC[]);;\r
 748 \r
 749 (* ------------------------------------------------------------------------- *)\r
 750 (* Interrelations between restricted and unrestricted limits.                *)\r
 751 (* ------------------------------------------------------------------------- *)\r
 752 \r
 753 let LIM_AT_WITHIN_FAN = prove\r
 754  (`!f l a s. (f --> l)(at_fan a) ==> (f --> l)(at_fan a within_fan s)`,\r
 755   REWRITE_TAC[LIM_AT_FAN; LIM_WITHIN_FAN] THEN MESON_TAC[]);;\r
 756 \r
 757 let LIM_WITHIN_OPEN_FAN = prove\r
 758  (`!f l a:real^M s.\r
 759      a IN s /\ open_fan s ==> ((f --> l)(at_fan a within_fan s) <=> (f --> l)(at_fan a))`,\r
 760   REPEAT STRIP_TAC THEN EQ_TAC THEN SIMP_TAC[LIM_AT_WITHIN_FAN] THEN\r
 761   REWRITE_TAC[LIM_AT_FAN; LIM_WITHIN_FAN] THEN\r
 762   MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `e:real` THEN\r
 763   ASM_CASES_TAC `&0 < e` THEN ASM_REWRITE_TAC[] THEN\r
 764    DISCH_THEN(X_CHOOSE_THEN `d1:real` STRIP_ASSUME_TAC) THEN\r
 765   FIRST_X_ASSUM(MP_TAC o SPEC `a:real^M` o GEN_REWRITE_RULE I [open_def_fan]) THEN\r
 766   ASM_REWRITE_TAC[] THEN\r
 767   DISCH_THEN(X_CHOOSE_THEN `d2:real` STRIP_ASSUME_TAC) THEN\r
 768   MP_TAC(SPECL [`d1:real`; `d2:real`] REAL_DOWN2) THEN ASM_REWRITE_TAC[] THEN\r
 769   ASM_MESON_TAC[REAL_LT_TRANS]);;\r
 770 \r
 771 (* ------------------------------------------------------------------------- *)\r
 772 (* Another limit point characterization.                                     *)\r
 773 (* ------------------------------------------------------------------------- *)\r
 774 \r
 775 let LIMPT_SEQUENTIAL_FAN = prove\r
 776  (`!x:real^N s.\r
 777       x limit_point_of_fan s <=>\r
 778              ?f. (!n. f(n) IN (s DELETE x)) /\ (f --> x) sequentially_fan`,\r
 779   REPEAT GEN_TAC THEN\r
 780   REWRITE_TAC[LIMPT_APPROACHABLE_FAN; LIM_SEQUENTIALLY_FAN; IN_DELETE] THEN\r
 781   EQ_TAC THENL [ALL_TAC; MESON_TAC[GE; LE_REFL]] THEN\r
 782   DISCH_THEN(MP_TAC o GEN `n:num` o SPEC `inv(&n + &1)`) THEN\r
 783   SIMP_TAC[REAL_LT_INV_EQ; REAL_ARITH `&0 <= x ==> &0 < x + &1`; REAL_POS] THEN\r
 784   REWRITE_TAC[SKOLEM_THM] THEN MATCH_MP_TAC MONO_EXISTS THEN\r
 785   X_GEN_TAC `f:num->real^N` THEN REWRITE_TAC[FORALL_AND_THM] THEN\r
 786   STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC FORALL_POS_MONO_1 THEN\r
 787   CONJ_TAC THENL [MESON_TAC[REAL_LT_TRANS]; ALL_TAC] THEN\r
 788   X_GEN_TAC `n:num` THEN EXISTS_TAC `n:num` THEN REWRITE_TAC[GSYM GE] THEN\r
 789   MATCH_MP_TAC SEQ_MONO_LEMMA THEN ASM_REWRITE_TAC[] THEN\r
 790   SIMP_TAC[REAL_LE_INV2; GE; REAL_OF_NUM_LE; REAL_LE_RADD; GE_REFL;\r
 791            REAL_POS; REAL_ARITH `&0 <= x ==> &0 < x + &1`]);;\r
 792 \r
 793 \r
 794 (* ------------------------------------------------------------------------- *)\r
 795 (* Basic arithmetical combining theorems for limits.                         *)\r
 796 (* ------------------------------------------------------------------------- *)\r
 797 \r
 798 let NET_DILEMMA_FAN = prove\r
 799  (`!net. (?a. (?x. netord_fan net_fan x a) /\ (!x. netord_fan net_fan x a ==> P x)) /\\r
 800          (?b. (?x. netord_fan net_fan x b) /\ (!x. netord_fan net_fan x b ==> Q x))\r
 801          ==> ?c. (?x. netord_fan net_fan x c) /\ (!x. netord_fan net_fan x c ==> P x /\ Q x)`,\r
 802   MESON_TAC[NET_FAN]);;\r
 803 \r
 804 let LIM_LINEAR_FAN = prove\r
 805  (`!net_fan:(A)net_fan h f l.\r
 806         (f --> l) net_fan /\ linear h ==> ((\x. h(f x)) --> h l) net_fan`,\r
 807   REPEAT GEN_TAC THEN REWRITE_TAC[lim_fan] THEN\r
 808   ASM_CASES_TAC `trivial_limit_fan (net_fan:(A)net_fan)` THEN ASM_REWRITE_TAC[] THEN\r
 809   STRIP_TAC THEN FIRST_ASSUM(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC o\r
 810     MATCH_MP LINEAR_BOUNDED_POS) THEN\r
 811   X_GEN_TAC `e:real` THEN DISCH_TAC THEN\r
 812   FIRST_X_ASSUM(MP_TAC o SPEC `e / B`) THEN\r
 813   ASM_SIMP_TAC[REAL_LT_DIV; dist; GSYM LINEAR_SUB; REAL_LT_RDIV_EQ] THEN\r
 814   ASM_MESON_TAC[REAL_LET_TRANS; REAL_MUL_SYM]);;\r
 815 \r
 816 let LIM_CONST_FAN = prove\r
 817  (`!net_fan a:real^N. ((\x. a) --> a) net_fan`,\r
 818   SIMP_TAC[lim_fan; DIST_REFL; trivial_limit_fan] THEN MESON_TAC[]);;\r
 819 \r
 820 let LIM_CMUL_FAN = prove\r
 821  (`!f l c. (f --> l) net_fan ==> ((\x. c % f x) --> c % l) net_fan`,\r
 822   REPEAT STRIP_TAC THEN MATCH_MP_TAC LIM_LINEAR_FAN THEN\r
 823   ASM_REWRITE_TAC[REWRITE_RULE[ETA_AX]\r
 824     (MATCH_MP LINEAR_COMPOSE_CMUL LINEAR_ID)]);;\r
 825 \r
 826 let LIM_NEG_FAN = prove\r
 827  (`!f l:real^N. (f --> l) net_fan ==> ((\x. --(f x)) --> --l) net_fan`,\r
 828   REPEAT GEN_TAC THEN REWRITE_TAC[lim_fan; dist] THEN\r
 829   REWRITE_TAC[VECTOR_ARITH `--x - --y = --(x - y:real^N)`; NORM_NEG]);;\r
 830 (* error in old file*)\r
 831 \r
 832 let LIM_ADD_FAN = prove\r
 833  (`!net_fan:(A)net_fan f g l m.\r
 834     (f --> l) net_fan /\ (g --> m) net_fan ==> ((\x. f(x) + g(x)) --> l + m) net_fan`,\r
 835  REPEAT GEN_TAC THEN REWRITE_TAC[lim_fan] THEN\r
 836   ASM_CASES_TAC `trivial_limit_fan (net_fan:(A)net_fan)` THEN\r
 837   ASM_REWRITE_TAC[AND_FORALL_THM] THEN\r
 838   DISCH_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN\r
 839   FIRST_X_ASSUM(MP_TAC o SPEC `e / &2`) THEN ASM_REWRITE_TAC[REAL_HALF] THEN\r
 840   DISCH_THEN(MP_TAC o MATCH_MP NET_DILEMMA_FAN) THEN REWRITE_TAC[MONO_EXISTS] THEN\r
 841  MESON_TAC[REAL_HALF; DIST_TRIANGLE_ADD; REAL_LT_ADD2; REAL_LET_TRANS]);;\r
 842 \r
 843 \r
 844 let LIM_SUB_FAN = prove\r
 845  (`!net_fan:(A)net_fan f g l m.\r
 846     (f --> l) net_fan /\ (g --> m) net_fan ==> ((\x. f(x) - g(x)) --> l - m) net_fan`,\r
 847   REWRITE_TAC[real_sub; VECTOR_SUB] THEN ASM_SIMP_TAC[LIM_ADD_FAN; LIM_NEG_FAN]);;\r
 848 \r
 849 let LIM_NULL_FAN = prove\r
 850  (`!net_fan f l. (f --> l) net_fan <=> ((\x. f(x) - l) --> vec 0) net_fan`,\r
 851   REWRITE_TAC[lim_fan; dist; VECTOR_SUB_RZERO]);;\r
 852 \r
 853 (* ------------------------------------------------------------------------- *)\r
 854 (* We need some non-triviality conditions on these two.                      *)\r
 855 (* ------------------------------------------------------------------------- *)\r
 856 \r
 857 let LIM_NORM_BOUND_FAN = prove\r
 858  (`!f (l:real^N) net_fan:(A)net_fan.\r
 859       ~(trivial_limit_fan net_fan) /\ (f --> l) net_fan /\\r
 860       (?y. (?x. netord_fan net_fan x y) /\ !x. netord_fan net_fan x y ==> norm(f x) <= e)\r
 861       ==> norm(l) <= e`,\r
 862   REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN\r
 863   ASM_REWRITE_TAC[lim_fan] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN\r
 864   STRIP_TAC THEN REWRITE_TAC[GSYM REAL_NOT_LT] THEN\r
 865   ONCE_REWRITE_TAC[GSYM REAL_SUB_LT] THEN DISCH_TAC THEN\r
 866   SUBGOAL_THEN\r
 867    `?x:A. dist(f(x):real^N,l) < norm(l:real^N) - e /\ norm(f x) <= e`\r
 868   (CHOOSE_THEN MP_TAC) THENL [ASM_MESON_TAC[NET_FAN]; ALL_TAC] THEN\r
 869   REWRITE_TAC[REAL_NOT_LT; REAL_LE_SUB_RADD; DE_MORGAN_THM; dist] THEN\r
 870   ASM_MESON_TAC[NORM_TRIANGLE; NORM_SUB; VECTOR_SUB_ADD;\r
 871     REAL_ARITH `nl <= nd + nx /\ nx <= e ==> nl <= nd + e`]);;\r
 872 \r
 873 let LIM_UNIQUE_FAN = prove\r
 874  (`!net_fan:(A)net_fan f l:real^N l'.\r
 875       ~(trivial_limit_fan net_fan) /\ (f --> l) net_fan /\ (f --> l') net_fan ==> (l = l')`,\r
 876   REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN\r
 877   DISCH_THEN(ASSUME_TAC o REWRITE_RULE[VECTOR_SUB_REFL] o MATCH_MP LIM_SUB_FAN) THEN\r
 878   SUBGOAL_THEN `!e. &0 < e ==> norm(l:real^N - l') <= e` MP_TAC THENL\r
 879    [GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC LIM_NORM_BOUND_FAN THEN\r
 880     MAP_EVERY EXISTS_TAC [`\x:A. vec 0 : real^N`; `net_fan:(A)net_fan`] THEN\r
 881     ASM_SIMP_TAC[NORM_0; REAL_LT_IMP_LE] THEN ASM_MESON_TAC[trivial_limit_fan];\r
 882     ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[DIST_NZ; dist] THEN\r
 883     DISCH_TAC THEN DISCH_THEN(MP_TAC o SPEC `norm(l - l':real^N) / &2`) THEN\r
 884     ASM_SIMP_TAC[REAL_LT_RDIV_EQ; REAL_LE_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN\r
 885     UNDISCH_TAC `&0 < norm(l - l':real^N)` THEN REAL_ARITH_TAC]);;\r
 886 \r
 887 (* ------------------------------------------------------------------------- *)\r
 888 (* Limit under bilinear function (surprisingly tedious, but important).      *)\r
 889 (* ------------------------------------------------------------------------- *)\r
 890 \r
 891 let NORM_BOUND_LEMMA_FAN = prove\r
 892  (`!x:real^M y:real^N e.\r
 893         &0 < e\r
 894         ==> ?d. &0 < d /\\r
 895                 !x' y'. norm(x' - x) < d /\ norm(y' - y) < d\r
 896                         ==> norm(x') * norm(y' - y) + norm(x' - x) * norm(y)\r
 897                                 < e`,\r
 898   REPEAT STRIP_TAC THEN\r
 899   EXISTS_TAC `min (&1) (e / &2 / (norm(x:real^M) + norm(y:real^N) + &1))` THEN\r
 900   ASM_SIMP_TAC[REAL_LT_MIN; REAL_LT_DIV; REAL_OF_NUM_LT; NORM_POS_LE; ARITH;\r
 901     REAL_LT_RDIV_EQ; REAL_ARITH `&0 <= x /\ &0 <= y ==> &0 < x + y + &1`] THEN\r
 902   REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC\r
 903    `(norm(x:real^M) + &1) * norm(y' - y) + norm(x' - x) * norm(y:real^N)` THEN\r
 904   CONJ_TAC THENL\r
 905    [REWRITE_TAC[REAL_LE_RADD; GSYM REAL_ADD_RDISTRIB] THEN\r
 906     MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[NORM_POS_LE] THEN\r
 907     ASM_MESON_TAC[NORM_TRIANGLE_SUB; REAL_ARITH\r
 908      `x' <= x + d /\ d < &1 ==> x' <= x + &1`];\r
 909     MATCH_MP_TAC REAL_LET_TRANS THEN\r
 910     EXISTS_TAC `(norm(x:real^M) + norm(y:real^N) + &1) *\r
 911                 (norm(x' - x) + norm(y' - y))` THEN\r
 912     CONJ_TAC THENL [ALL_TAC; REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC] THEN\r
 913     MATCH_MP_TAC(REAL_ARITH\r
 914      `y * xd <= p * xd /\ x * yd <= p * yd\r
 915       ==> x * yd + xd * y <= p * (xd + yd)`) THEN\r
 916     CONJ_TAC THEN MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[NORM_POS_LE] THENL\r
 917      [MP_TAC(ISPEC `x:real^M` NORM_POS_LE);\r
 918       MP_TAC(ISPEC `y:real^N` NORM_POS_LE)] THEN\r
 919     REAL_ARITH_TAC]);;\r
 920 \r
 921 (*let LIM_BILINEAR_FAN = prove\r
 922  (;;\r
 923 g`!net_fan:(A)net_fan (h:real^M->real^N->real^P) f g l m.\r
 924         (f --> l) net_fan /\ (g --> m) net_fan /\ bilinear h\r
 925         ==> ((\x. h (f x) (g x)) --> (h l m)) net_fan`;;\r
 926 ,;;\r
 927  e( REPEAT GEN_TAC THEN REWRITE_TAC[lim_fan] THEN\r
 928   ASM_CASES_TAC `trivial_limit_fan (net_fan:(A)net_fan)` THEN\r
 929   ASM_REWRITE_TAC[AND_FORALL_THM; CONJ_ASSOC] THEN\r
 930   STRIP_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN\r
 931   FIRST_ASSUM(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC o  MATCH_MP\r
 932    BILINEAR_BOUNDED_POS) THEN\r
 933   MP_TAC(ISPECL [`l:real^M`; `m:real^N`; `e / B`] NORM_BOUND_LEMMA_FAN) THEN\r
 934   ASM_SIMP_TAC[REAL_LT_RDIV_EQ; REAL_MUL_LZERO] THEN\r
 935   DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN\r
 936   FIRST_X_ASSUM(MP_TAC o SPEC `d:real`) THEN ASM_REWRITE_TAC[] THEN\r
 937   DISCH_THEN(MP_TAC o MATCH_MP NET_DILEMMA_FAN));;\r
 938   THEN \r
 939 ;;\r
 940 e(REWRITE_TAC[MONO_EXISTS]);;\r
 941 \r
 942 THEN;;\r
 943 \r
 944 e(X_GEN_TAC `c:A`);;\r
 945 MONO_AND;; \r
 946 e(DISCH_TAC);;\r
 947 \r
 948 e( MATCH_MP_TAC MONO_AND);; \r
 949 \r
 950 THEN REWRITE_TAC[] THEN\r
 951   MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `a:A` THEN\r
 952   MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[dist] THEN\r
 953   DISCH_THEN(fun th -> FIRST_X_ASSUM(ASSUME_TAC o C MATCH_MP th)) THEN\r
 954   ONCE_REWRITE_TAC[VECTOR_ARITH\r
 955     `h a b - h c d :real^N = (h a b - h a d) + (h a d - h c d)`] THEN\r
 956   MATCH_MP_TAC NORM_TRIANGLE_LT THEN\r
 957   ASM_SIMP_TAC[GSYM BILINEAR_LSUB; GSYM BILINEAR_RSUB] THEN\r
 958   FIRST_X_ASSUM(fun th ->\r
 959    MP_TAC(SPECL [`(f:A->real^M) a`; `(g:A->real^N) a - m`] th) THEN\r
 960    MP_TAC(SPECL [`(f:A->real^M) a - l`; `m:real^N`] th)) THEN\r
 961   REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC);;\r
 962 *)\r
 963 \r
 964 (* ------------------------------------------------------------------------- *)\r
 965 (* These are special for limits out of the same vector space.                *)\r
 966 (* ------------------------------------------------------------------------- *)\r
 967 \r
 968 let LIM_WITHIN_ID_FAN = prove\r
 969  (`!a s. ((\x. x) --> a) (at_fan a within_fan s)`,\r
 970   REWRITE_TAC[LIM_WITHIN_FAN] THEN MESON_TAC[]);;\r
 971 \r
 972 let LIM_AT_ID_FAN = prove\r
 973  (`!a. ((\x. x) --> a) (at_fan a)`,\r
 974   ONCE_REWRITE_TAC[GSYM WITHIN_UNIV_FAN] THEN REWRITE_TAC[LIM_WITHIN_ID_FAN]);;\r
 975   \r
 976 let LIM_AT_ZERO_FAN = prove\r
 977  (`!f:real^M->real^N l a.\r
 978         (f --> l) (at_fan a) <=> ((\x. f(a + x)) --> l) (at_fan(vec 0))`,\r
 979   REPEAT GEN_TAC THEN REWRITE_TAC[LIM_AT_FAN] THEN\r
 980   AP_TERM_TAC THEN ABS_TAC THEN\r
 981   ASM_CASES_TAC `&0 < e` THEN ASM_REWRITE_TAC[] THEN\r
 982   AP_TERM_TAC THEN ABS_TAC THEN\r
 983   ASM_CASES_TAC `&0 < d` THEN ASM_REWRITE_TAC[] THEN\r
 984   EQ_TAC THEN DISCH_TAC THEN X_GEN_TAC `x:real^M` THENL\r
 985    [FIRST_X_ASSUM(MP_TAC o SPEC `a + x:real^M`) THEN\r
 986     REWRITE_TAC[dist; VECTOR_ADD_SUB; VECTOR_SUB_RZERO];\r
 987     FIRST_X_ASSUM(MP_TAC o SPEC `x - a:real^M`) THEN\r
 988     REWRITE_TAC[dist; VECTOR_SUB_RZERO; VECTOR_SUB_ADD2]]);;\r
 989 \r
 990 (* ------------------------------------------------------------------------- *)\r
 991 (* It's also sometimes useful to extract the limit point from the net.       *)\r
 992 (* ------------------------------------------------------------------------- *)\r
 993 \r
 994 let netlimit_fan = new_definition\r
 995   `netlimit_fan net_fan = @a. !x. ~(netord_fan net_fan x a)`;;\r
 996 \r
 997 let NETLIMIT_WITHIN_FAN = prove\r
 998  (`!a:real^N s. ~(trivial_limit_fan (at_fan a within_fan s))\r
 999                 ==> (netlimit_fan (at_fan a within_fan s) = a)`,\r
1000   REWRITE_TAC[trivial_limit_fan; netlimit_fan; AT_FAN; WITHIN_FAN; DE_MORGAN_THM] THEN\r
1001   REPEAT STRIP_TAC THEN MATCH_MP_TAC SELECT_UNIQUE THEN REWRITE_TAC[] THEN\r
1002   SUBGOAL_THEN\r
1003    `!x:real^N. ~(&0 < dist(x,a) /\ dist(x,a) <= dist(a,a) /\ x IN s)`\r
1004   ASSUME_TAC THENL\r
1005    [ASM_MESON_TAC[DIST_REFL; REAL_NOT_LT]; ASM_MESON_TAC[]]);;\r
1006 \r
1007 (* ------------------------------------------------------------------------- *)\r
1008 (* Useful lemmas on closure and set of possible sequential limits.           *)\r
1009 (* ------------------------------------------------------------------------- *)\r
1010 \r
1011 let CLOSURE_SEQUENTIAL_FAN = prove\r
1012  (`!s l:real^N.\r
1013      l IN closure_fan(s) <=> ?x. (!n. x(n) IN s) /\ (x --> l) sequentially_fan`,\r
1014   REWRITE_TAC[closure_fan; IN_UNION; LIMPT_SEQUENTIAL_FAN; IN_ELIM_THM; IN_DELETE] THEN\r
1015   REPEAT GEN_TAC THEN MATCH_MP_TAC(TAUT\r
1016     `((b ==> c) /\ (~a /\ c ==> b)) /\ (a ==> c) ==> (a \/ b <=> c)`) THEN\r
1017   CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN DISCH_TAC THEN\r
1018   EXISTS_TAC `\n:num. l:real^N` THEN\r
1019   ASM_REWRITE_TAC[LIM_CONST_FAN]);;\r
1020 \r
1021 let CLOSED_SEQUENTIAL_LIMITS_FAN = prove\r
1022  (`!s. closed_fan s <=>\r
1023        !x l. (!n. x(n) IN s) /\ (x --> l) sequentially_fan ==> l IN s`,\r
1024   MESON_TAC[CLOSURE_SEQUENTIAL_FAN; CLOSURE_CLOSED_FAN;\r
1025             CLOSED_LIMPT_FAN; LIMPT_SEQUENTIAL_FAN; IN_DELETE]);;\r
1026 \r
1027 let CLOSURE_APPROACHABLE_FAN = prove\r
1028  (`!x s. x IN closure_fan(s) <=> !e. &0 < e ==> ?y. y IN s /\ dist(y,x) < e`,\r
1029   REWRITE_TAC[closure_fan; LIMPT_APPROACHABLE_FAN; IN_UNION; IN_ELIM_THM] THEN\r
1030   MESON_TAC[DIST_REFL]);;\r
1031 \r
1032 let CLOSED_APPROACHABLE_FAN = prove\r
1033  (`!x s. closed_fan s\r
1034          ==> ((!e. &0 < e ==> ?y. y IN s /\ dist(y,x) < e) <=> x IN s)`,\r
1035   MESON_TAC[CLOSURE_CLOSED_FAN; CLOSURE_APPROACHABLE_FAN]);;\r
1036 \r
1037 (* ------------------------------------------------------------------------- *)\r
1038 (* Closed balls.                                                             *)\r
1039 (* ------------------------------------------------------------------------- *)\r
1040 \r
1041 let cball_fan = new_definition\r
1042   `cball_fan(x,e) = { y | dist(x,y) <= e}`;;\r
1043 \r
1044 let IN_CBALL_FAN = prove\r
1045  (`!x y e. y IN cball_fan(x,e) <=> dist(x,y) <= e`,\r
1046   REWRITE_TAC[cball_fan; IN_ELIM_THM]);;\r
1047 \r
1048 let CLOSED_CBALL_FAN = prove\r
1049  (`!x:real^N e. closed_fan(cball_fan(x,e))`,\r
1050   REWRITE_TAC[CLOSED_SEQUENTIAL_LIMITS_FAN; IN_CBALL_FAN; dist] THEN\r
1051   GEN_TAC THEN GEN_TAC THEN X_GEN_TAC `s:num->real^N` THEN\r
1052   X_GEN_TAC `y:real^N` THEN STRIP_TAC THEN\r
1053   MATCH_MP_TAC(ISPEC `\n. x - (s:num->real^N) n` LIM_NORM_BOUND_FAN) THEN\r
1054   EXISTS_TAC `sequentially_fan` THEN REWRITE_TAC[TRIVIAL_LIMIT_SEQUENTIALLY_FAN] THEN\r
1055   ASM_SIMP_TAC[LIM_SUB_FAN; LIM_CONST_FAN; SEQUENTIALLY_FAN] THEN MESON_TAC[GE_REFL]);;\r
1056 \r
1057 let CENTRE_IN_CBALL_FAN = prove\r
1058  (`!x e. x IN cball_fan(x,e) <=> &0 <= e`,\r
1059   MESON_TAC[IN_CBALL_FAN; DIST_REFL]);;\r
1060 \r
1061 let BALL_SUBSET_CBALL_FAN = prove\r
1062  (`!x e. ball_fan(x,e) SUBSET cball_fan(x,e)`,\r
1063   REWRITE_TAC[IN_BALL_FAN; IN_CBALL_FAN; SUBSET] THEN REAL_ARITH_TAC);;\r
1064 \r
1065 let OPEN_CONTAINS_CBALL_FAN = prove\r
1066  (`!s. open_fan s <=> !x. x IN s ==> ?e. &0 < e /\ cball_fan(x,e) SUBSET s`,\r
1067   GEN_TAC THEN REWRITE_TAC[OPEN_CONTAINS_BALL_FAN] THEN EQ_TAC THENL\r
1068    [ALL_TAC; ASM_MESON_TAC[SUBSET_TRANS; BALL_SUBSET_CBALL_FAN]] THEN\r
1069   MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN MATCH_MP_TAC MONO_IMP THEN\r
1070   REWRITE_TAC[SUBSET; IN_BALL_FAN; IN_CBALL_FAN] THEN\r
1071   DISCH_THEN(X_CHOOSE_THEN `e:real` STRIP_ASSUME_TAC) THEN\r
1072   EXISTS_TAC `e / &2` THEN ASM_REWRITE_TAC[REAL_HALF] THEN\r
1073   SUBGOAL_THEN `e / &2 < e` (fun th -> ASM_MESON_TAC[th; REAL_LET_TRANS]) THEN\r
1074   ASM_SIMP_TAC[REAL_LT_LDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN\r
1075   UNDISCH_TAC `&0 < e` THEN REAL_ARITH_TAC);;\r
1076 \r
1077 let IN_INTERIOR_CBALL_FAN = prove\r
1078  (`!x s. x IN interior_fan s <=> ?e. &0 < e /\ cball_fan(x,e) SUBSET s`,\r
1079   REWRITE_TAC[interior_fan; IN_ELIM_THM] THEN\r
1080   MESON_TAC[OPEN_CONTAINS_CBALL_FAN; SUBSET_TRANS;\r
1081             BALL_SUBSET_CBALL_FAN; CENTRE_IN_BALL; OPEN_BALL_FAN]);;\r
1082 \r
1083 let LIMPT_BALL_FAN = prove\r
1084  (`!x:real^N y e. y limit_point_of_fan ball_fan(x,e) <=> &0 < e /\ y IN cball_fan(x,e)`,\r
1085   REPEAT GEN_TAC THEN ASM_CASES_TAC `&0 < e` THENL\r
1086    [ALL_TAC; ASM_MESON_TAC[LIMPT_EMPTY_FAN; REAL_NOT_LT; BALL_EQ_EMPTY_FAN]] THEN\r
1087   ASM_REWRITE_TAC[] THEN EQ_TAC THENL\r
1088    [MESON_TAC[CLOSED_CBALL_FAN; CLOSED_LIMPT_FAN; LIMPT_SUBSET_FAN; BALL_SUBSET_CBALL_FAN];\r
1089     REWRITE_TAC[IN_CBALL_FAN; LIMPT_APPROACHABLE_FAN; IN_BALL_FAN]] THEN\r
1090   DISCH_TAC THEN X_GEN_TAC `d:real` THEN DISCH_TAC THEN\r
1091   ASM_CASES_TAC `y:real^N = x` THEN ASM_REWRITE_TAC[DIST_NZ] THENL\r
1092    [MP_TAC(SPECL [`d:real`; `e:real`] REAL_DOWN2) THEN\r
1093     ASM_REWRITE_TAC[] THEN\r
1094     GEN_MESON_TAC 0 40 1 [VECTOR_CHOOSE_DIST; DIST_SYM; REAL_LT_IMP_LE];\r
1095     ALL_TAC] THEN\r
1096   MP_TAC(SPECL [`norm(y:real^N - x)`; `d:real`] REAL_DOWN2) THEN\r
1097   RULE_ASSUM_TAC(REWRITE_RULE[DIST_NZ; dist]) THEN ASM_REWRITE_TAC[] THEN\r
1098   DISCH_THEN(X_CHOOSE_THEN `k:real` STRIP_ASSUME_TAC) THEN\r
1099   EXISTS_TAC `(y:real^N) - (k / dist(y,x)) % (y - x)` THEN\r
1100   REWRITE_TAC[dist; VECTOR_ARITH `(y - c % z) - y = --c % z`] THEN\r
1101   REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM; REAL_ABS_NEG] THEN\r
1102   ASM_SIMP_TAC[REAL_DIV_RMUL; REAL_LT_IMP_NZ] THEN\r
1103   REWRITE_TAC[VECTOR_ARITH `x - (y - k % (y - x)) = (&1 - k) % (x - y)`] THEN\r
1104   ASM_SIMP_TAC[REAL_ARITH `&0 < k ==> &0 < abs k`; NORM_MUL] THEN\r
1105   ASM_SIMP_TAC[REAL_ARITH `&0 < k /\ k < d ==> abs k < d`] THEN\r
1106   MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `norm(x:real^N - y)` THEN\r
1107   ASM_REWRITE_TAC[] THEN GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN\r
1108   MATCH_MP_TAC REAL_LT_RMUL THEN CONJ_TAC THENL\r
1109    [ALL_TAC; ASM_MESON_TAC[NORM_SUB]] THEN\r
1110   MATCH_MP_TAC(REAL_ARITH `&0 < k /\ k < &1 ==> abs(&1 - k) < &1`) THEN\r
1111   ASM_SIMP_TAC[REAL_LT_LDIV_EQ; REAL_LT_RDIV_EQ; REAL_MUL_LZERO;\r
1112                REAL_MUL_LID]);;\r
1113 \r
1114 let CLOSURE_BALL_FAN = prove\r
1115  (`!x:real^N e. &0 < e ==> (closure_fan(ball_fan(x,e)) = cball_fan(x,e))`,\r
1116   SIMP_TAC[EXTENSION; closure_fan; IN_ELIM_THM; IN_UNION; LIMPT_BALL_FAN] THEN\r
1117   REWRITE_TAC[IN_BALL_FAN; IN_CBALL_FAN] THEN REAL_ARITH_TAC);;\r
1118 \r
1119 let INTERIOR_CBALL_FAN = prove\r
1120  (`!x:real^N e. &0 <= e ==> (interior_fan(cball_fan(x,e)) = ball_fan(x,e))`,\r
1121   REPEAT STRIP_TAC THEN MATCH_MP_TAC INTERIOR_UNIQUE_FAN THEN\r
1122   REWRITE_TAC[BALL_SUBSET_CBALL_FAN; OPEN_BALL_FAN] THEN\r
1123   X_GEN_TAC `t:real^N->bool` THEN\r
1124   SIMP_TAC[SUBSET; IN_CBALL_FAN; IN_BALL_FAN; REAL_LT_LE] THEN STRIP_TAC THEN\r
1125   X_GEN_TAC `z:real^N` THEN DISCH_TAC THEN DISCH_THEN(SUBST_ALL_TAC o SYM) THEN\r
1126   FIRST_X_ASSUM(MP_TAC o SPEC `z:real^N` o GEN_REWRITE_RULE I [open_def_fan]) THEN\r
1127   ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN `d:real` MP_TAC) THEN\r
1128   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN\r
1129   ASM_CASES_TAC `z:real^N = x` THENL\r
1130    [FIRST_X_ASSUM SUBST_ALL_TAC THEN\r
1131     FIRST_X_ASSUM(X_CHOOSE_TAC `k:real` o MATCH_MP REAL_DOWN) THEN\r
1132     SUBGOAL_THEN `?w:real^N. dist(w,x) = k` STRIP_ASSUME_TAC THENL\r
1133      [ASM_MESON_TAC[VECTOR_CHOOSE_DIST; DIST_SYM; REAL_LT_IMP_LE];\r
1134       ASM_MESON_TAC[REAL_NOT_LE; DIST_REFL; DIST_SYM]];\r
1135     RULE_ASSUM_TAC(REWRITE_RULE[DIST_NZ]) THEN\r
1136     DISCH_THEN(MP_TAC o SPEC `z + ((d / &2) / dist(z,x)) % (z - x:real^N)`) THEN\r
1137     REWRITE_TAC[dist; VECTOR_ADD_SUB; NORM_MUL; REAL_ABS_DIV;\r
1138                 REAL_ABS_NORM; REAL_ABS_NUM] THEN\r
1139     ASM_SIMP_TAC[REAL_DIV_RMUL; GSYM dist; REAL_LT_IMP_NZ] THEN\r
1140     ASM_SIMP_TAC[REAL_LT_LDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN\r
1141     ASM_REWRITE_TAC[REAL_ARITH `abs d < d * &2 <=> &0 < d`] THEN\r
1142     DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN REWRITE_TAC[dist] THEN\r
1143     REWRITE_TAC[VECTOR_ARITH `x - (z + k % (z - x)) = (&1 + k) % (x - z)`] THEN\r
1144     REWRITE_TAC[REAL_NOT_LE; NORM_MUL] THEN\r
1145     GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_LID] THEN\r
1146     ONCE_REWRITE_TAC[NORM_SUB] THEN\r
1147     ASM_SIMP_TAC[REAL_LT_RMUL_EQ; GSYM dist] THEN\r
1148     MATCH_MP_TAC(REAL_ARITH `&0 < x ==> &1 < abs(&1 + x)`) THEN\r
1149     ONCE_REWRITE_TAC[DIST_SYM] THEN\r
1150     ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH]]);;\r
1151 \r
1152 let FRONTIER_BALL_FAN = prove\r
1153  (`!a e. &0 < e\r
1154          ==> (frontier_fan(ball_fan(a,e)) = {x | dist(a,x) = e})`,\r
1155   SIMP_TAC[frontier_fan; CLOSURE_BALL_FAN; INTERIOR_OPEN_FAN; OPEN_BALL_FAN;\r
1156            REAL_LT_IMP_LE] THEN\r
1157   REWRITE_TAC[EXTENSION; IN_DIFF; IN_ELIM_THM; IN_BALL_FAN; IN_CBALL_FAN] THEN\r
1158   REAL_ARITH_TAC);;\r
1159 \r
1160 let FRONTIER_CBALL_FAN = prove\r
1161  (`!a e. &0 < e\r
1162          ==> (frontier_fan(cball_fan(a,e)) = {x | dist(a,x) = e})`,\r
1163   SIMP_TAC[frontier_fan; INTERIOR_CBALL_FAN; CLOSED_CBALL_FAN; CLOSURE_CLOSED_FAN;\r
1164            REAL_LT_IMP_LE] THEN\r
1165   REWRITE_TAC[EXTENSION; IN_DIFF; IN_ELIM_THM; IN_BALL_FAN; IN_CBALL_FAN] THEN\r
1166   REAL_ARITH_TAC);;\r
1167 \r
1168 let SUBSET_BALL_FAN = prove\r
1169  (`!x d e. d <= e ==> ball_fan(x,d) SUBSET ball_fan(x,e)`,\r
1170   REWRITE_TAC[SUBSET; IN_BALL_FAN] THEN MESON_TAC[REAL_LTE_TRANS]);;\r
1171 \r
1172 let SUBSET_CBALL_FAN = prove\r
1173  (`!x d e. d <= e ==> cball_fan(x,d) SUBSET cball_fan(x,e)`,\r
1174   REWRITE_TAC[SUBSET; IN_CBALL_FAN] THEN MESON_TAC[REAL_LE_TRANS]);;\r
1175 \r
1176 (* ------------------------------------------------------------------------- *)\r
1177 (* Boundedness.                                                              *)\r
1178 (* ------------------------------------------------------------------------- *)\r
1179 \r
1180 let bounded_fan = new_definition\r
1181   `bounded_fan s <=> ?a. !x:real^N. x IN s ==> norm(x) <= a`;;\r
1182 \r
1183 let BOUNDED_EMPTY_FAN = prove\r
1184  (`bounded_fan {}`,\r
1185   REWRITE_TAC[bounded_fan; NOT_IN_EMPTY]);;\r
1186 \r
1187 let BOUNDED_SUBSET_FAN = prove\r
1188  (`!s t. bounded_fan t /\ s SUBSET t ==> bounded_fan s`,\r
1189   MESON_TAC[bounded_fan; SUBSET]);;\r
1190 \r
1191 let BOUNDED_CLOSURE_FAN = prove\r
1192  (`!s:real^N->bool. bounded_fan s ==> bounded_fan(closure_fan s)`,\r
1193   REWRITE_TAC[bounded_fan; CLOSURE_SEQUENTIAL_FAN] THEN\r
1194   MESON_TAC[LIM_NORM_BOUND_FAN; TRIVIAL_LIMIT_SEQUENTIALLY_FAN; trivial_limit_fan]);;\r
1195 \r
1196 let BOUNDED_CBALL_FAN = prove\r
1197  (`!x:real^N e. bounded_fan(cball_fan(x,e))`,\r
1198   REPEAT GEN_TAC THEN REWRITE_TAC[bounded_fan] THEN\r
1199   EXISTS_TAC `norm(x:real^N) + e` THEN REWRITE_TAC[IN_CBALL_FAN; dist] THEN\r
1200   MESON_TAC[NORM_SUB; NORM_TRIANGLE_SUB;\r
1201             REAL_ARITH `b <= c + a ==> a <= e ==> b <= c + e`]);;\r
1202 \r
1203 let BOUNDED_BALL_FAN = prove\r
1204  (`!x e. bounded_fan(ball_fan(x,e))`,\r
1205   MESON_TAC[BALL_SUBSET_CBALL_FAN; BOUNDED_CBALL_FAN; BOUNDED_SUBSET_FAN]);;\r
1206 \r
1207 let FINITE_IMP_BOUNDED_FAN = prove\r
1208  (`!s:real^N->bool. FINITE s ==> bounded_fan s`,\r
1209   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN REWRITE_TAC[BOUNDED_EMPTY_FAN] THEN\r
1210   REWRITE_TAC[bounded_fan; IN_INSERT] THEN X_GEN_TAC `x:real^N` THEN GEN_TAC THEN\r
1211   DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `B:real`) STRIP_ASSUME_TAC) THEN\r
1212   EXISTS_TAC `norm(x:real^N) + abs B` THEN REPEAT STRIP_TAC THEN\r
1213   ASM_MESON_TAC[NORM_POS_LE; REAL_ARITH\r
1214    `(y <= b /\ &0 <= x ==> y <= x + abs b) /\ x <= x + abs b`]);;\r
1215 \r
1216 let BOUNDED_UNION_FAN = prove\r
1217  (`!s t. bounded_fan (s UNION t) <=> bounded_fan s /\ bounded_fan t`,\r
1218   REWRITE_TAC[bounded_fan; IN_UNION] THEN MESON_TAC[REAL_LE_MAX]);;\r
1219 \r
1220 let BOUNDED_POS_FAN = prove\r
1221  (`!s. bounded_fan s <=> ?b. &0 < b /\ !x. x IN s ==> norm(x) <= b`,\r
1222   REWRITE_TAC[bounded_fan] THEN\r
1223   MESON_TAC[REAL_ARITH `&0 < &1 + abs(y) /\ (x <= y ==> x <= &1 + abs(y))`]);;\r
1224 \r
1225 let BOUNDED_INTER_FAN = prove\r
1226  (`!s t. bounded_fan s \/ bounded_fan t ==> bounded_fan (s INTER t)`,\r
1227   MESON_TAC[BOUNDED_SUBSET_FAN; INTER_SUBSET]);;\r
1228 \r
1229 (* ------------------------------------------------------------------------- *)\r
1230 (* Compactness (the definition is the one based on convegent subsequences).  *)\r
1231 (* ------------------------------------------------------------------------- *)\r
1232 \r
1233 let compact_fan = new_definition\r
1234   `compact_fan s <=>\r
1235         !f:num->real^N.\r
1236             (!n. f(n) IN s)\r
1237             ==> ?l r. l IN s /\ (!m n:num. m < n ==> r(m) < r(n)) /\\r
1238                       ((f o r) --> l) sequentially_fan`;;\r
1239 \r
1240 let MONOTONE_BIGGER_FAN = prove\r
1241  (`!r. (!m n. m < n ==> r(m) < r(n)) ==> !n:num. n <= r(n)`,\r
1242   GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THEN\r
1243   ASM_MESON_TAC[LE_0; ARITH_RULE `n <= m /\ m < p ==> SUC n <= p`; LT]);;\r
1244 \r
1245 let LIM_SUBSEQUENCE_FAN = prove\r
1246  (`!s r. (!m n. m < n ==> r(m) < r(n)) /\ (s --> l) sequentially_fan\r
1247          ==> (s o r --> l) sequentially_fan`,\r
1248   REWRITE_TAC[LIM_SEQUENTIALLY_FAN; o_THM] THEN\r
1249   MESON_TAC[MONOTONE_BIGGER_FAN; LE_TRANS]);;\r
1250 \r
1251 let MONOTONE_SUBSEQUENCE_FAN = prove\r
1252  (`!s:num->real. ?r:num->num.\r
1253            (!m n. m < n ==> r(m) < r(n)) /\\r
1254            ((!m n. m <= n ==> s(r(m)) <= s(r(n))) \/\r
1255             (!m n. m <= n ==> s(r(n)) <= s(r(m))))`,\r
1256   GEN_TAC THEN\r
1257   ASM_CASES_TAC `!n:num. ?p. n < p /\ !m. p <= m ==> s(m) <= s(p)` THEN\r
1258   POP_ASSUM MP_TAC THEN\r
1259   REWRITE_TAC[NOT_FORALL_THM; NOT_EXISTS_THM; NOT_IMP; DE_MORGAN_THM] THEN\r
1260   REWRITE_TAC[RIGHT_OR_EXISTS_THM; SKOLEM_THM; REAL_NOT_LE; REAL_NOT_LT] THENL\r
1261    [ABBREV_TAC `N = 0`; DISCH_THEN(X_CHOOSE_THEN `N:num` MP_TAC)] THEN\r
1262   DISCH_THEN(X_CHOOSE_THEN `next:num->num` STRIP_ASSUME_TAC) THEN\r
1263   (MP_TAC o prove_recursive_functions_exist num_RECURSION)\r
1264    `(r 0 = next(SUC N)) /\ (!n. r(SUC n) = next(r n))` THEN\r
1265   MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN STRIP_TAC THENL\r
1266    [SUBGOAL_THEN `!m:num n:num. r n <= m ==> s(m) <= s(r n):real`\r
1267     ASSUME_TAC THEN TRY CONJ_TAC THEN TRY DISJ2_TAC THEN\r
1268     GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[LT; LE] THEN\r
1269     ASM_MESON_TAC[REAL_LE_TRANS; REAL_LE_REFL; LT_IMP_LE; LT_TRANS];\r
1270     SUBGOAL_THEN `!n. N < (r:num->num) n` ASSUME_TAC THEN\r
1271     TRY(CONJ_TAC THENL [GEN_TAC; DISJ1_TAC THEN GEN_TAC]) THEN\r
1272     INDUCT_TAC THEN ASM_REWRITE_TAC[LT; LE] THEN\r
1273     TRY STRIP_TAC THEN ASM_REWRITE_TAC[] THEN\r
1274     ASM_MESON_TAC[REAL_LT_REFL; LT_LE; LTE_TRANS; REAL_LE_REFL;\r
1275                   REAL_LT_LE; REAL_LE_TRANS; LT]]);;\r
1276 \r
1277 let CONVERGENT_BOUNDED_INCREASING_FAN = prove\r
1278  (`!s:num->real b. (!m n. m <= n ==> s m <= s n) /\ (!n. abs(s n) <= b)\r
1279                    ==> ?l. !e. &0 < e ==> ?N. !n. N <= n ==> abs(s n - l) < e`,\r
1280   REPEAT STRIP_TAC THEN\r
1281   MP_TAC(SPEC `\x. ?n. (s:num->real) n = x` REAL_COMPLETE) THEN\r
1282   REWRITE_TAC[] THEN ANTS_TAC THENL\r
1283    [ASM_MESON_TAC[REAL_ARITH `abs(x) <= b ==> x <= b`]; ALL_TAC] THEN\r
1284   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `l:real` THEN STRIP_TAC THEN\r
1285   X_GEN_TAC `e:real` THEN STRIP_TAC THEN\r
1286   FIRST_X_ASSUM(MP_TAC o SPEC `l - e`) THEN\r
1287   ASM_MESON_TAC[REAL_ARITH `&0 < e ==> ~(l <= l - e)`;\r
1288       REAL_ARITH `x <= y /\ y <= l /\ ~(x <= l - e) ==> abs(y - l) < e`]);;\r
1289 \r
1290 let CONVERGENT_BOUNDED_MONOTONE_FAN = prove\r
1291  (`!s:num->real b. (!n. abs(s n) <= b) /\\r
1292                    ((!m n. m <= n ==> s m <= s n) \/\r
1293                     (!m n. m <= n ==> s n <= s m))\r
1294                    ==> ?l. !e. &0 < e ==> ?N. !n. N <= n ==> abs(s n - l) < e`,\r
1295   REPEAT STRIP_TAC THENL\r
1296    [ASM_MESON_TAC[CONVERGENT_BOUNDED_INCREASING_FAN]; ALL_TAC] THEN\r
1297   MP_TAC(SPEC `\n. --((s:num->real) n)` CONVERGENT_BOUNDED_INCREASING_FAN) THEN\r
1298   ASM_REWRITE_TAC[REAL_LE_NEG2; REAL_ABS_NEG] THEN\r
1299   ASM_MESON_TAC[REAL_ARITH `abs(x - --l) = abs(--x - l)`]);;\r
1300 \r
1301 let COMPACT_REAL_LEMMA_FAN = prove\r
1302  (`!s b. (!n:num. abs(s n) <= b)\r
1303          ==> ?l r. (!m n:num. m < n ==> r(m) < r(n)) /\\r
1304                    !e. &0 < e ==> ?N. !n. N <= n ==> abs(s(r n) - l) < e`,\r
1305   REPEAT GEN_TAC THEN DISCH_TAC THEN ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN\r
1306   MP_TAC(SPEC `s:num->real` MONOTONE_SUBSEQUENCE_FAN) THEN\r
1307   MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN DISCH_TAC THEN ASM_SIMP_TAC[] THEN\r
1308   MATCH_MP_TAC CONVERGENT_BOUNDED_MONOTONE_FAN THEN ASM_MESON_TAC[]);;\r
1309 \r
1310 let COMPACT_LEMMA_FAN = prove\r
1311  (`!s. bounded_fan s /\ (!n. (x:num->real^N) n IN s)\r
1312        ==> !d. d <= dimindex(:N)\r
1313                ==> ?l:real^N r. (!m n. m < n ==> r m < (r:num->num) n) /\\r
1314                          !e. &0 < e\r
1315                              ==> ?N. !n i. 1 <= i /\ i <= d\r
1316                                            ==> N <= n\r
1317                                                ==> abs(x(r n)$i - l$i) < e`,\r
1318   GEN_TAC THEN REWRITE_TAC[bounded_fan] THEN\r
1319   DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `b:real`) ASSUME_TAC) THEN\r
1320   INDUCT_TAC THENL\r
1321    [REWRITE_TAC[ARITH_RULE `1 <= i /\ i <= 0 <=> F`; CONJ_ASSOC] THEN\r
1322     DISCH_TAC THEN EXISTS_TAC `\n:num. n` THEN REWRITE_TAC[];\r
1323     ALL_TAC] THEN\r
1324   DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o check (is_imp o concl)) THEN\r
1325   ASM_SIMP_TAC[ARITH_RULE `SUC d <= n ==> d <= n`] THEN STRIP_TAC THEN\r
1326   MP_TAC(SPECL [`\n:num. (x:num->real^N) (r n) $ (SUC d)`; `b:real`]\r
1327          COMPACT_REAL_LEMMA_FAN) THEN\r
1328   REWRITE_TAC[] THEN ANTS_TAC THENL\r
1329    [ASM_MESON_TAC[REAL_LE_TRANS; COMPONENT_LE_NORM; ARITH_RULE `1 <= SUC n`];\r
1330     ALL_TAC] THEN\r
1331   DISCH_THEN(X_CHOOSE_THEN `y:real` (X_CHOOSE_THEN `s:num->num`\r
1332         STRIP_ASSUME_TAC)) THEN\r
1333   MAP_EVERY EXISTS_TAC\r
1334    [`(lambda k. if k = SUC d then y else (l:real^N)$k):real^N`;\r
1335     `(r:num->num) o (s:num->num)`] THEN\r
1336   ASM_SIMP_TAC[o_THM] THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN\r
1337   REPEAT(FIRST_ASSUM(C UNDISCH_THEN (MP_TAC o SPEC `e:real`) o concl)) THEN\r
1338   ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_TAC `N1:num`) THEN\r
1339   DISCH_THEN(X_CHOOSE_TAC `N2:num`) THEN EXISTS_TAC `N1 + N2:num` THEN\r
1340   FIRST_ASSUM(fun th -> SIMP_TAC[LAMBDA_BETA; MATCH_MP(ARITH_RULE\r
1341    `SUC d <= n ==> !i. 1 <= i /\ i <= SUC d ==> 1 <= i /\ i <= n`) th]) THEN\r
1342   REWRITE_TAC[LE] THEN REPEAT STRIP_TAC THEN\r
1343   ASM_REWRITE_TAC[] THEN TRY COND_CASES_TAC THEN\r
1344   ASM_MESON_TAC[MONOTONE_BIGGER_FAN; LE_TRANS;\r
1345     ARITH_RULE `N1 + N2 <= n ==> N2 <= n:num /\ N1 <= n`;\r
1346     ARITH_RULE `1 <= i /\ i <= d /\ SUC d <= n\r
1347                 ==> ~(i = SUC d) /\ 1 <= SUC d /\ d <= n /\ i <= n`]);;\r
1348 \r
1349 let BOUNDED_CLOSED_IMP_COMPACT_FAN = prove\r
1350  (`!s:real^N->bool. bounded_fan s /\ closed_fan s ==> compact_fan s`,\r
1351   REPEAT STRIP_TAC THEN REWRITE_TAC[compact_fan] THEN\r
1352   X_GEN_TAC `x:num->real^N` THEN DISCH_TAC THEN\r
1353   MP_TAC(ISPEC `s:real^N->bool` COMPACT_LEMMA_FAN) THEN\r
1354   ASM_REWRITE_TAC[] THEN\r
1355   DISCH_THEN(MP_TAC o SPEC `dimindex(:N)`) THEN\r
1356   REWRITE_TAC[LE_REFL] THEN\r
1357   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `l:real^N` THEN\r
1358   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `r:num->num` THEN ASM_SIMP_TAC[] THEN\r
1359   STRIP_TAC THEN MATCH_MP_TAC(TAUT `(b ==> a) /\ b ==> a /\ b`) THEN\r
1360   REPEAT STRIP_TAC THENL\r
1361    [FIRST_ASSUM(MATCH_MP_TAC o REWRITE_RULE[CLOSED_SEQUENTIAL_LIMITS_FAN]) THEN\r
1362     EXISTS_TAC `(x:num->real^N) o (r:num->num)` THEN\r
1363     ASM_REWRITE_TAC[o_THM];\r
1364     ALL_TAC] THEN\r
1365   REWRITE_TAC[LIM_SEQUENTIALLY_FAN] THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN\r
1366   FIRST_X_ASSUM(MP_TAC o SPEC `e / &2 / &(dimindex(:N))`) THEN\r
1367   ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; DIMINDEX_NONZERO;\r
1368                REAL_HALF; ARITH_RULE `0 < n <=> ~(n = 0)`] THEN\r
1369   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `N:num` THEN\r
1370   REWRITE_TAC[dist] THEN REPEAT STRIP_TAC THEN\r
1371   MATCH_MP_TAC(MATCH_MP (REAL_ARITH `a <= b ==> b < e ==> a < e`)\r
1372                         (SPEC_ALL NORM_LE_L1)) THEN\r
1373   MATCH_MP_TAC REAL_LET_TRANS THEN\r
1374   EXISTS_TAC `sum (1..dimindex(:N))\r
1375                   (\k. e / &2 / &(dimindex(:N)))` THEN\r
1376   CONJ_TAC THENL\r
1377    [MATCH_MP_TAC SUM_LE_NUMSEG THEN\r
1378     SIMP_TAC[o_THM; LAMBDA_BETA; vector_sub] THEN\r
1379     ASM_MESON_TAC[REAL_LT_IMP_LE; LE_TRANS];\r
1380     ASM_SIMP_TAC[SUM_CONST_NUMSEG; ADD_SUB; REAL_DIV_LMUL; REAL_OF_NUM_EQ;\r
1381                  DIMINDEX_NONZERO; REAL_LE_REFL; REAL_LT_LDIV_EQ; ARITH;\r
1382                  REAL_OF_NUM_LT; REAL_ARITH `x < x * &2 <=> &0 < x`]]);;\r
1383 \r
1384 (* ------------------------------------------------------------------------- *)\r
1385 (* Completeness.                                                             *)\r
1386 (* ------------------------------------------------------------------------- *)\r
1387 \r
1388 let cauchy_fan = new_definition\r
1389   `cauchy_fan (s:num->real^N) <=>\r
1390      !e. &0 < e ==> ?N. !m n. m >= N /\ n >= N ==> dist(s m,s n) < e`;;\r
1391 \r
1392 let complete_fan = new_definition\r
1393   `complete_fan s <=>\r
1394      !f:num->real^N. (!n. f n IN s) /\ cauchy_fan f\r
1395                       ==> ?l. l IN s /\ (f --> l) sequentially_fan`;;\r
1396 \r
1397 let CAUCHY_FAN = prove\r
1398  (`!s:num->real^N.\r
1399       cauchy_fan s <=> !e. &0 < e ==> ?N. !n. n >= N ==> dist(s n,s N) < e`,\r
1400   REPEAT GEN_TAC THEN REWRITE_TAC[cauchy_fan; GE] THEN EQ_TAC THENL\r
1401    [MESON_TAC[LE_REFL]; DISCH_TAC] THEN\r
1402   X_GEN_TAC `e:real` THEN DISCH_TAC THEN\r
1403   FIRST_X_ASSUM(MP_TAC o SPEC `e / &2`) THEN ASM_REWRITE_TAC[REAL_HALF] THEN\r
1404   MESON_TAC[DIST_TRIANGLE_HALF_L]);;\r
1405 \r
1406 let CONVERGENT_IMP_CAUCHY_FAN = prove\r
1407  (`!s l. (s --> l) sequentially_fan ==> cauchy_fan s`,\r
1408   REWRITE_TAC[LIM_SEQUENTIALLY_FAN; cauchy_fan] THEN\r
1409   REPEAT GEN_TAC THEN DISCH_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN\r
1410   FIRST_X_ASSUM(MP_TAC o SPEC `e / &2`) THEN\r
1411   ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN\r
1412   ASM_MESON_TAC[GE; LE_REFL; DIST_TRIANGLE_HALF_L]);;\r
1413 \r
1414 let CAUCHY_IMP_BOUNDED_FAN = prove\r
1415  (`!s:num->real^N. cauchy_fan s ==> bounded_fan {y | ?n. y = s n}`,\r
1416   REWRITE_TAC[cauchy_fan; bounded_fan; IN_ELIM_THM] THEN GEN_TAC THEN\r
1417   DISCH_THEN(MP_TAC o SPEC `&1`) THEN REWRITE_TAC[REAL_LT_01] THEN\r
1418   DISCH_THEN(X_CHOOSE_THEN `N:num` (MP_TAC o SPEC `N:num`)) THEN\r
1419   REWRITE_TAC[GE_REFL] THEN DISCH_TAC THEN\r
1420   SUBGOAL_THEN `!n:num. N <= n ==> norm(s n :real^N) <= norm(s N) + &1`\r
1421   ASSUME_TAC THENL\r
1422    [ASM_MESON_TAC[GE; dist; DIST_SYM; NORM_TRIANGLE_SUB;\r
1423                   REAL_ARITH `a <= b + c /\ c < &1 ==> a <= b + &1`];\r
1424     MP_TAC(ISPECL [`\n:num. norm(s n :real^N)`; `0..N`]\r
1425                   UPPER_BOUND_FINITE_SET_REAL) THEN\r
1426     SIMP_TAC[FINITE_NUMSEG; IN_NUMSEG; LE_0; LEFT_IMP_EXISTS_THM] THEN\r
1427     ASM_MESON_TAC[LE_CASES;\r
1428                   REAL_ARITH `x <= a \/ x <= b ==> x <= abs a + abs b`]]);;\r
1429 \r
1430 \r
1431 let COMPACT_IMP_COMPLETE_FAN = prove\r
1432  (`!s:real^N->bool. compact_fan s ==> complete_fan s`,\r
1433   GEN_TAC THEN REWRITE_TAC[complete_fan; compact_fan]\r
1434  THEN  MATCH_MP_TAC MONO_FORALL\r
1435  THEN X_GEN_TAC `f:num->real^N` \r
1436   THEN DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th)THEN\r
1437   ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN\r
1438   DISCH_THEN(X_CHOOSE_THEN `r:num->num` STRIP_ASSUME_TAC) THEN\r
1439   FIRST_X_ASSUM(MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ] LIM_ADD_FAN)) THEN\r
1440   DISCH_THEN(MP_TAC o SPEC `\n. (f:num->real^N)(n) - f(r n)`) THEN\r
1441   DISCH_THEN(MP_TAC o SPEC `vec 0: real^N`) THEN ASM_REWRITE_TAC[o_THM] THEN\r
1442   REWRITE_TAC[VECTOR_ADD_RID; VECTOR_SUB_ADD2; ETA_AX] THEN\r
1443   DISCH_THEN MATCH_MP_TAC THEN\r
1444   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [cauchy_fan]) THEN\r
1445   REWRITE_TAC[GE; lim_fan; SEQUENTIALLY_FAN; dist; VECTOR_SUB_RZERO] THEN\r
1446   SUBGOAL_THEN `!n:num. n <= r(n)` MP_TAC THENL [INDUCT_TAC; ALL_TAC] THEN\r
1447   ASM_MESON_TAC[ LE_TRANS; LE_REFL; LT; LET_TRANS; LE_0; LE_SUC_LT]);;\r
1448 \r
1449 let COMPLETE_UNIV_FAN = prove\r
1450  (`complete_fan(:real^N)`,\r
1451   REWRITE_TAC[complete_fan; IN_UNIV] THEN X_GEN_TAC `x:num->real^N` THEN\r
1452   DISCH_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP CAUCHY_IMP_BOUNDED_FAN) THEN\r
1453   DISCH_THEN(ASSUME_TAC o MATCH_MP BOUNDED_CLOSURE_FAN) THEN\r
1454   MP_TAC(ISPEC `closure_fan {y:real^N | ?n:num. y = x n}`\r
1455                COMPACT_IMP_COMPLETE_FAN) THEN\r
1456   ASM_SIMP_TAC[BOUNDED_CLOSED_IMP_COMPACT_FAN; CLOSED_CLOSURE_FAN; complete_fan] THEN\r
1457   DISCH_THEN(MP_TAC o SPEC `x:num->real^N`) THEN\r
1458   ANTS_TAC THENL [ALL_TAC; MESON_TAC[]] THEN\r
1459   ASM_REWRITE_TAC[closure_fan; IN_ELIM_THM; IN_UNION] THEN MESON_TAC[]);;\r
1460 \r
1461 let COMPLETE_EQ_CLOSED_FAN = prove\r
1462  (`!s:real^N->bool. complete_fan s <=> closed_fan s`,\r
1463   GEN_TAC THEN EQ_TAC THENL\r
1464    [REWRITE_TAC[complete_fan; CLOSED_LIMPT_FAN; LIMPT_SEQUENTIAL_FAN] THEN\r
1465     REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN GEN_TAC THEN\r
1466     REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN MATCH_MP_TAC MONO_FORALL THEN\r
1467     MESON_TAC[CONVERGENT_IMP_CAUCHY_FAN; IN_DELETE; LIM_UNIQUE_FAN;\r
1468               TRIVIAL_LIMIT_SEQUENTIALLY_FAN];\r
1469     REWRITE_TAC[complete_fan; CLOSED_SEQUENTIAL_LIMITS_FAN] THEN DISCH_TAC THEN\r
1470     X_GEN_TAC `f:num->real^N` THEN STRIP_TAC THEN\r
1471     MP_TAC(REWRITE_RULE[complete_fan] COMPLETE_UNIV_FAN) THEN\r
1472     DISCH_THEN(MP_TAC o SPEC `f:num->real^N`) THEN\r
1473     ASM_REWRITE_TAC[IN_UNIV] THEN ASM_MESON_TAC[]]);;\r
1474 \r
1475 let CONVERGENT_EQ_CAUCHY_FAN = prove\r
1476  (`!s. (?l. (s --> l) sequentially_fan) <=> cauchy_fan s`,\r
1477   GEN_TAC THEN EQ_TAC THENL\r
1478    [REWRITE_TAC[LEFT_IMP_EXISTS_THM; CONVERGENT_IMP_CAUCHY_FAN];\r
1479     REWRITE_TAC[REWRITE_RULE[complete_fan; IN_UNIV] COMPLETE_UNIV_FAN]]);;\r
1480 \r
1481 (* ------------------------------------------------------------------------- *)\r
1482 (* Total boundedness.                                                        *)\r
1483 (* ------------------------------------------------------------------------- *)\r
1484 \r
1485 let COMPACT_IMP_TOTALLY_BOUNDED_FAN = prove\r
1486  (`!s:real^N->bool.\r
1487         compact_fan s\r
1488         ==> !e. &0 < e ==> ?k. FINITE k /\ k SUBSET s /\\r
1489                                s SUBSET (UNIONS(IMAGE (\x. ball_fan(x,e)) k))`,\r
1490   GEN_TAC THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN\r
1491   REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; NOT_EXISTS_THM] THEN\r
1492   REWRITE_TAC[TAUT `~(a /\ b /\ c) <=> a /\ b ==> ~c`; SUBSET] THEN\r
1493   DISCH_THEN(X_CHOOSE_THEN `e:real` STRIP_ASSUME_TAC) THEN\r
1494   SUBGOAL_THEN\r
1495    `?x:num->real^N. !n. x(n) IN s /\ !m. m < n ==> ~(dist(x(m),x(n)) < e)`\r
1496   MP_TAC THENL\r
1497    [SUBGOAL_THEN\r
1498      `?x:num->real^N.\r
1499           !n. x(n) = @y. y IN s /\ !m. m < n ==> ~(dist(x(m),y) < e)`\r
1500     MP_TAC THENL\r
1501      [MATCH_MP_TAC(MATCH_MP WF_REC WF_num) THEN SIMP_TAC[]; ALL_TAC] THEN\r
1502     MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `x:num->real^N` THEN\r
1503     DISCH_TAC THEN MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN\r
1504     FIRST_X_ASSUM(SUBST1_TAC o SPEC `n:num`) THEN STRIP_TAC THEN\r
1505     CONV_TAC SELECT_CONV THEN\r
1506     FIRST_X_ASSUM(MP_TAC o SPEC `IMAGE (x:num->real^N) {m | m < n}`) THEN\r
1507     SIMP_TAC[FINITE_IMAGE; FINITE_NUMSEG_LT; NOT_FORALL_THM; NOT_IMP] THEN\r
1508     REWRITE_TAC[IN_UNIONS; IN_IMAGE; IN_ELIM_THM] THEN ASM_MESON_TAC[IN_BALL_FAN];\r
1509     ALL_TAC] THEN\r
1510   REWRITE_TAC[compact_fan; NOT_FORALL_THM] THEN MATCH_MP_TAC MONO_EXISTS THEN\r
1511   X_GEN_TAC `x:num->real^N` THEN  REWRITE_TAC[NOT_IMP; FORALL_AND_THM] THEN\r
1512   STRIP_TAC THEN ASM_REWRITE_TAC[NOT_EXISTS_THM] THEN REPEAT STRIP_TAC THEN\r
1513   FIRST_X_ASSUM(MP_TAC o MATCH_MP CONVERGENT_IMP_CAUCHY_FAN) THEN\r
1514   REWRITE_TAC[cauchy_fan] THEN DISCH_THEN(MP_TAC o SPEC `e:real`) THEN\r
1515   ASM_REWRITE_TAC[o_THM; NOT_EXISTS_THM; NOT_IMP; NOT_FORALL_THM; NOT_IMP] THEN\r
1516   X_GEN_TAC `N:num` THEN MAP_EVERY EXISTS_TAC [`N:num`; `SUC N`] THEN\r
1517   CONJ_TAC THENL [ARITH_TAC; ASM_MESON_TAC[LT]]);;\r
1518 \r
1519 (* ------------------------------------------------------------------------- *)\r
1520 (* Heine-Borel theorem (following Burkill & Burkill vol. 2)                  *)\r
1521 (* ------------------------------------------------------------------------- *)\r
1522 \r
1523 let HEINE_BOREL_LEMMA_FAN = prove\r
1524  (`!s:real^N->bool.\r
1525       compact_fan s\r
1526       ==> !t. s SUBSET (UNIONS t) /\ (!b. b IN t ==> open_fan b)\r
1527               ==> ?e. &0 < e /\\r
1528                       !x. x IN s ==> ?b. b IN t /\ ball_fan(x,e) SUBSET b`,\r
1529   GEN_TAC THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN\r
1530   REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; NOT_EXISTS_THM] THEN\r
1531   DISCH_THEN(CHOOSE_THEN (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN\r
1532   DISCH_THEN(MP_TAC o GEN `n:num` o SPEC `&1 / (&n + &1)`) THEN\r
1533   SIMP_TAC[REAL_LT_DIV; REAL_LT_01; REAL_ARITH `x <= y ==> x < y + &1`;\r
1534    FORALL_AND_THM; REAL_POS; NOT_FORALL_THM; NOT_IMP; SKOLEM_THM; compact_fan] THEN\r
1535   MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN REWRITE_TAC[NOT_EXISTS_THM] THEN\r
1536   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN ASM_REWRITE_TAC[] THEN\r
1537   DISCH_TAC THEN MAP_EVERY X_GEN_TAC [`l:real^N`; `r:num->num`] THEN\r
1538   STRIP_TAC THEN\r
1539   SUBGOAL_THEN `?b:real^N->bool. l IN b /\ b IN t` STRIP_ASSUME_TAC THENL\r
1540    [ASM_MESON_TAC[SUBSET; IN_UNIONS]; ALL_TAC] THEN\r
1541   SUBGOAL_THEN `?e. &0 < e /\ !z:real^N. dist(z,l) < e ==> z IN b`\r
1542   STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[open_def_fan]; ALL_TAC] THEN\r
1543   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [LIM_SEQUENTIALLY_FAN]) THEN\r
1544   DISCH_THEN(MP_TAC o SPEC `e / &2`) THEN\r
1545   SUBGOAL_THEN `&0 < e / &2` (fun th ->\r
1546     REWRITE_TAC[th; o_THM] THEN MP_TAC(GEN_REWRITE_RULE I [REAL_ARCH_INV] th))\r
1547   THENL [ASM_REWRITE_TAC[REAL_HALF]; ALL_TAC] THEN\r
1548   DISCH_THEN(X_CHOOSE_THEN `N1:num` STRIP_ASSUME_TAC) THEN\r
1549   DISCH_THEN(X_CHOOSE_THEN `N2:num` STRIP_ASSUME_TAC) THEN\r
1550   FIRST_X_ASSUM(MP_TAC o SPECL\r
1551    [`(r:num->num)(N1 + N2)`; `b:real^N->bool`]) THEN\r
1552   ASM_REWRITE_TAC[SUBSET] THEN X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN\r
1553   FIRST_X_ASSUM MATCH_MP_TAC THEN MATCH_MP_TAC DIST_TRIANGLE_HALF_R THEN\r
1554   EXISTS_TAC `(f:num->real^N)(r(N1 + N2:num))` THEN CONJ_TAC THENL\r
1555    [ALL_TAC; FIRST_X_ASSUM MATCH_MP_TAC THEN ARITH_TAC] THEN\r
1556   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [IN_BALL_FAN]) THEN\r
1557   MATCH_MP_TAC(REAL_ARITH `a <= b ==> x < a ==> x < b`) THEN\r
1558   MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `inv(&N1)` THEN\r
1559   ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN REWRITE_TAC[real_div; REAL_MUL_LID] THEN\r
1560   MATCH_MP_TAC REAL_LE_INV2 THEN\r
1561   REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_LE; REAL_OF_NUM_LT] THEN\r
1562   ASM_MESON_TAC[ARITH_RULE `(~(n = 0) ==> 0 < n)`; LE_ADD; MONOTONE_BIGGER_FAN;\r
1563                 LT_IMP_LE; LE_TRANS]);;\r
1564 \r
1565 let COMPACT_IMP_HEINE_BOREL_FAN = prove\r
1566  (`!s. compact_fan (s:real^N->bool)\r
1567        ==> !f. (!t. t IN f ==> open_fan t) /\ s SUBSET (UNIONS f)\r
1568                ==> ?f'. f' SUBSET f /\ FINITE f' /\ s SUBSET (UNIONS f')`,\r
1569   REPEAT STRIP_TAC THEN\r
1570   FIRST_ASSUM(MP_TAC o SPEC `f:(real^N->bool)->bool` o\r
1571     MATCH_MP HEINE_BOREL_LEMMA_FAN) THEN ASM_REWRITE_TAC[] THEN\r
1572   DISCH_THEN(X_CHOOSE_THEN `e:real` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN\r
1573   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [RIGHT_IMP_EXISTS_THM] THEN\r
1574   REWRITE_TAC[SKOLEM_THM; SUBSET; IN_BALL_FAN] THEN\r
1575   DISCH_THEN(X_CHOOSE_TAC `B:real^N->real^N->bool`) THEN\r
1576   FIRST_ASSUM(MP_TAC o SPEC `e:real` o\r
1577     MATCH_MP COMPACT_IMP_TOTALLY_BOUNDED_FAN) THEN\r
1578   ASM_REWRITE_TAC[SUBSET; IN_UNIONS; IN_IMAGE; IN_BALL_FAN] THEN\r
1579   REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN\r
1580   REWRITE_TAC[GSYM CONJ_ASSOC; UNWIND_THM2] THEN\r
1581   DISCH_THEN(X_CHOOSE_THEN `k:real^N->bool` STRIP_ASSUME_TAC) THEN\r
1582   EXISTS_TAC `IMAGE (B:real^N->real^N->bool) k` THEN\r
1583   ASM_SIMP_TAC[FINITE_IMAGE; SUBSET; IN_IMAGE; LEFT_IMP_EXISTS_THM] THEN\r
1584   ASM_MESON_TAC[IN_BALL_FAN]);;\r
1585 \r
1586 (* ------------------------------------------------------------------------- *)\r
1587 (* Bolzano-Weierstrass property.                                             *)\r
1588 (* ------------------------------------------------------------------------- *)\r
1589 \r
1590 let HEINE_BOREL_IMP_BOLZANO_WEIERSTRASS_FAN = prove\r
1591  (`!s:real^N->bool.\r
1592         (!f. (!t. t IN f ==> open_fan t) /\ s SUBSET (UNIONS f)\r
1593              ==> ?f'. f' SUBSET f /\ FINITE f' /\ s SUBSET (UNIONS f'))\r
1594         ==> !t. INFINITE t /\ t SUBSET s ==> ?x. x IN s /\ x limit_point_of_fan t`,\r
1595   REWRITE_TAC[RIGHT_IMP_FORALL_THM; limit_point_of_fan] THEN REPEAT GEN_TAC THEN\r
1596   ONCE_REWRITE_TAC[TAUT `a ==> b /\ c ==> d <=> c ==> ~d ==> a ==> ~b`] THEN\r
1597   REWRITE_TAC[NOT_FORALL_THM; NOT_EXISTS_THM; RIGHT_AND_FORALL_THM] THEN\r
1598   DISCH_TAC THEN REWRITE_TAC[SKOLEM_THM] THEN\r
1599   DISCH_THEN(X_CHOOSE_TAC `f:real^N->real^N->bool`) THEN\r
1600   DISCH_THEN(MP_TAC o SPEC\r
1601    `{t:real^N->bool | ?x:real^N. x IN s /\ (t = f x)}`) THEN\r
1602   REWRITE_TAC[INFINITE; SUBSET; IN_ELIM_THM; IN_UNIONS; NOT_IMP] THEN\r
1603   ANTS_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN\r
1604   DISCH_THEN(X_CHOOSE_THEN `g:(real^N->bool)->bool` STRIP_ASSUME_TAC) THEN\r
1605   MATCH_MP_TAC FINITE_SUBSET THEN\r
1606   EXISTS_TAC `{x:real^N | x IN t /\ (f(x):real^N->bool) IN g}` THEN\r
1607   CONJ_TAC THENL\r
1608    [MATCH_MP_TAC FINITE_IMAGE_INJ_GENERAL THEN ASM_MESON_TAC[SUBSET];\r
1609     SIMP_TAC[SUBSET; IN_ELIM_THM] THEN X_GEN_TAC `u:real^N` THEN\r
1610     DISCH_TAC THEN SUBGOAL_THEN `(u:real^N) IN s` ASSUME_TAC THEN\r
1611     ASM_MESON_TAC[SUBSET]]);;\r
1612 \r
1613 (* ------------------------------------------------------------------------- *)\r
1614 (* Complete the chain of compactness variants.                               *)\r
1615 (* ------------------------------------------------------------------------- *)\r
1616 \r
1617 let BOLZANO_WEIERSTRASS_IMP_BOUNDED_FAN = prove\r
1618  (`!s:real^N->bool.\r
1619         (!t. INFINITE t /\ t SUBSET s ==> ?x. x IN s /\ x limit_point_of_fan t)\r
1620         ==> bounded_fan s`,\r
1621   GEN_TAC THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN\r
1622   SIMP_TAC[compact_fan; bounded_fan] THEN\r
1623   REWRITE_TAC[NOT_FORALL_THM; NOT_EXISTS_THM; SKOLEM_THM; NOT_IMP] THEN\r
1624   REWRITE_TAC[REAL_NOT_LE] THEN\r
1625   DISCH_THEN(X_CHOOSE_TAC `beyond:real->real^N`) THEN\r
1626   (MP_TAC o prove_recursive_functions_exist num_RECURSION)\r
1627    `(f(0) = beyond(&0)) /\\r
1628     (!n. f(SUC n) = beyond(norm(f n) + &1):real^N)` THEN\r
1629   DISCH_THEN(X_CHOOSE_THEN `x:num->real^N` STRIP_ASSUME_TAC) THEN\r
1630   EXISTS_TAC `IMAGE (x:num->real^N) UNIV` THEN\r
1631   SUBGOAL_THEN\r
1632    `!m n. m < n ==> norm((x:num->real^N) m) + &1 < norm(x n)`\r
1633   ASSUME_TAC THENL\r
1634    [GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[LT] THEN\r
1635     ASM_MESON_TAC[REAL_LT_TRANS; REAL_ARITH `b < b + &1`];\r
1636     ALL_TAC] THEN\r
1637   SUBGOAL_THEN `!m n. ~(m = n) ==> &1 < dist((x:num->real^N) m,x n)`\r
1638   ASSUME_TAC THENL\r
1639    [REPEAT GEN_TAC THEN REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC\r
1640      (SPECL [`m:num`; `n:num`] LT_CASES) THEN\r
1641     ASM_MESON_TAC[dist; LT_CASES; NORM_TRIANGLE_SUB; NORM_SUB;\r
1642                   REAL_ARITH `x + &1 < y /\ y <= x + d ==> &1 < d`];\r
1643     ALL_TAC] THEN\r
1644   REPEAT CONJ_TAC THENL\r
1645    [ASM_MESON_TAC[INFINITE_IMAGE_INJ; num_INFINITE; DIST_REFL;\r
1646                   REAL_ARITH `~(&1 < &0)`];\r
1647     REWRITE_TAC[SUBSET; IN_IMAGE; IN_UNIV; LEFT_IMP_EXISTS_THM] THEN\r
1648     GEN_TAC THEN INDUCT_TAC THEN ASM_MESON_TAC[];\r
1649     ALL_TAC] THEN\r
1650   X_GEN_TAC `l:real^N` THEN REWRITE_TAC[LIMPT_APPROACHABLE_FAN] THEN\r
1651   REWRITE_TAC[IN_IMAGE; IN_UNIV; LEFT_AND_EXISTS_THM] THEN\r
1652   ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN REWRITE_TAC[UNWIND_THM2] THEN\r
1653   STRIP_TAC THEN FIRST_ASSUM(MP_TAC o SPEC `&1 / &2`) THEN\r
1654   CONV_TAC REAL_RAT_REDUCE_CONV THEN\r
1655   DISCH_THEN(X_CHOOSE_THEN `k:num` STRIP_ASSUME_TAC) THEN\r
1656   FIRST_X_ASSUM(MP_TAC o SPEC `dist((x:num->real^N) k,l)`) THEN\r
1657   ASM_SIMP_TAC[DIST_POS_LT] THEN\r
1658   DISCH_THEN(X_CHOOSE_THEN `m:num` STRIP_ASSUME_TAC) THEN\r
1659   ASM_CASES_TAC `m:num = k` THEN\r
1660   ASM_MESON_TAC[DIST_TRIANGLE_HALF_L; REAL_LT_TRANS; REAL_LT_REFL]);;\r
1661 \r
1662 let SEQUENCE_INFINITE_LEMMA_FAN = prove\r
1663  (`!f l. (!n. ~(f(n) = l)) /\ (f --> l) sequentially_fan\r
1664          ==> INFINITE {y:real^N | ?n. y = f n}`,\r
1665   REWRITE_TAC[INFINITE] THEN REPEAT STRIP_TAC THEN MP_TAC(ISPEC\r
1666    `IMAGE (\y:real^N. dist(y,l)) {y | ?n:num. y = f n}` INF_FINITE) THEN\r
1667   ASM_SIMP_TAC[GSYM MEMBER_NOT_EMPTY; IN_IMAGE; FINITE_IMAGE; IN_ELIM_THM] THEN\r
1668   ASM_MESON_TAC[LIM_SEQUENTIALLY_FAN; LE_REFL; REAL_NOT_LE; DIST_POS_LT]);;\r
1669 \r
1670 let SEQUENCE_UNIQUE_LIMPT_FAN = prove\r
1671  (`!f l. (!n. ~(f(n) = l)) /\ (f --> l) sequentially_fan\r
1672          ==> !l'. l' limit_point_of_fan {y:real^N | ?n. y = f n}\r
1673                   ==> (l' = l)`,\r
1674   REWRITE_TAC[LIMPT_APPROACHABLE_FAN; IN_ELIM_THM; LEFT_AND_EXISTS_THM] THEN\r
1675   ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN REWRITE_TAC[UNWIND_THM2] THEN\r
1676   REPEAT STRIP_TAC THEN ABBREV_TAC `e = dist(l':real^N,l)` THEN\r
1677   SUBGOAL_THEN `~(&0 < e)` (fun th -> ASM_MESON_TAC[th; DIST_POS_LT]) THEN\r
1678   DISCH_TAC THEN\r
1679   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [LIM_SEQUENTIALLY_FAN]) THEN\r
1680   DISCH_THEN(MP_TAC o SPEC `e / &2`) THEN ASM_REWRITE_TAC[REAL_HALF] THEN\r
1681   DISCH_THEN(X_CHOOSE_TAC `N:num`) THEN MP_TAC(ISPEC  \r
1682    `(e / &2) INSERT\r
1683     (IMAGE (\n. if dist((f:num->real^N) n,l') = &0 then e / &2\r
1684                 else dist((f:num->real^N) n,l'))\r
1685            {n | n < N})`\r
1686  INF_FINITE) THEN\r
1687   ASM_SIMP_TAC[FINITE_RULES; FINITE_IMAGE; FINITE_NUMSEG_LT;\r
1688                              NOT_EMPTY_INSERT] THEN\r
1689   ABBREV_TAC(mk_eq(`d:real`,mk_comb(`inf`,  \r
1690    `(e / &2) INSERT\r
1691     (IMAGE (\n. if dist((f:num->real^N) n,l') = &0 then e / &2\r
1692                 else dist((f:num->real^N) n,l'))\r
1693            {n | n < N})`\r
1694 ))) THEN\r
1695   REWRITE_TAC[IN_INSERT; IN_IMAGE; IN_ELIM_THM] THEN\r
1696   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN\r
1697   SUBGOAL_THEN `&0 < d` ASSUME_TAC THENL\r
1698    [FIRST_X_ASSUM(DISJ_CASES_THEN STRIP_ASSUME_TAC) THEN ASM_REWRITE_TAC[] THEN\r
1699     REPEAT COND_CASES_TAC THEN\r
1700     ASM_MESON_TAC[REAL_HALF; REAL_LT_LE; DIST_POS_LE];\r
1701     ALL_TAC] THEN\r
1702   FIRST_X_ASSUM(MP_TAC o SPEC `d:real`) THEN ASM_REWRITE_TAC[] THEN\r
1703   DISCH_THEN(X_CHOOSE_THEN `k:num` STRIP_ASSUME_TAC) THEN\r
1704   DISCH_THEN(fun th -> MP_TAC(SPEC `e / &2` th) THEN\r
1705                    MP_TAC(SPEC `dist((f:num->real^N) k,l')` th)) THEN\r
1706   ASM_REWRITE_TAC[GSYM REAL_NOT_LT; DE_MORGAN_THM] THEN\r
1707   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN\r
1708   REWRITE_TAC[NOT_EXISTS_THM] THEN DISCH_THEN(MP_TAC o SPEC `k:num`) THEN\r
1709   ASM_REWRITE_TAC[DIST_EQ_0; NOT_LT; GSYM REAL_NOT_LE] THEN\r
1710   ASM_MESON_TAC[DIST_TRIANGLE_HALF_R; REAL_LT_REFL; REAL_LTE_TRANS]);;\r
1711 \r
1712 let BOLZANO_WEIERSTRASS_IMP_CLOSED_FAN = prove\r
1713  (`!s:real^N->bool.\r
1714         (!t. INFINITE t /\ t SUBSET s ==> ?x. x IN s /\ x limit_point_of_fan t)\r
1715         ==> closed_fan s`,\r
1716   REPEAT STRIP_TAC THEN REWRITE_TAC[CLOSED_SEQUENTIAL_LIMITS_FAN] THEN\r
1717   MAP_EVERY X_GEN_TAC [`f:num->real^N`; `l:real^N`] THEN\r
1718   DISCH_TAC THEN\r
1719   MAP_EVERY (MP_TAC o ISPECL [`f:num->real^N`; `l:real^N`])\r
1720    [SEQUENCE_UNIQUE_LIMPT_FAN; SEQUENCE_INFINITE_LEMMA_FAN] THEN\r
1721   MATCH_MP_TAC(TAUT\r
1722    `(~d ==> a /\ ~(b /\ c)) ==> (a ==> b) ==> (a ==> c) ==> d`) THEN\r
1723   DISCH_TAC THEN CONJ_TAC THENL [ASM_MESON_TAC[]; STRIP_TAC] THEN\r
1724   FIRST_X_ASSUM(MP_TAC o SPEC `{y:real^N | ?n:num. y = f n}`) THEN\r
1725   ASM_REWRITE_TAC[NOT_IMP] THEN CONJ_TAC THENL\r
1726    [REWRITE_TAC[SUBSET; IN_ELIM_THM];\r
1727     ABBREV_TAC `t = {y:real^N | ?n:num. y = f n}`] THEN\r
1728   ASM_MESON_TAC[]);;\r
1729 \r
1730 (* ------------------------------------------------------------------------- *)\r
1731 (* Hence express everything as an equivalence.                               *)\r
1732 (* ------------------------------------------------------------------------- *)\r
1733 \r
1734 let COMPACT_EQ_HEINE_BOREL_FAN = prove\r
1735  (`!s:real^N->bool.\r
1736         compact_fan s <=>\r
1737            !f. (!t. t IN f ==> open_fan t) /\ s SUBSET (UNIONS f)\r
1738                ==> ?f'. f' SUBSET f /\ FINITE f' /\ s SUBSET (UNIONS f')`,\r
1739   GEN_TAC THEN EQ_TAC THEN SIMP_TAC[COMPACT_IMP_HEINE_BOREL_FAN] THEN\r
1740   DISCH_THEN(MP_TAC o MATCH_MP HEINE_BOREL_IMP_BOLZANO_WEIERSTRASS_FAN) THEN\r
1741   DISCH_TAC THEN MATCH_MP_TAC BOUNDED_CLOSED_IMP_COMPACT_FAN THEN\r
1742   ASM_SIMP_TAC[BOLZANO_WEIERSTRASS_IMP_BOUNDED_FAN;\r
1743                BOLZANO_WEIERSTRASS_IMP_CLOSED_FAN]);;\r
1744 \r
1745 \r
1746 \r
1747 \r
1748 let COMPACT_EQ_BOLZANO_WEIERSTRASS_FAN = prove\r
1749  (`!s:real^N->bool.\r
1750         compact_fan s <=>\r
1751            !t. INFINITE t /\ t SUBSET s ==> ?x. x IN s /\ x limit_point_of_fan t`,\r
1752   GEN_TAC THEN EQ_TAC THENL\r
1753    [SIMP_TAC[COMPACT_EQ_HEINE_BOREL_FAN; HEINE_BOREL_IMP_BOLZANO_WEIERSTRASS_FAN];\r
1754     SIMP_TAC[BOLZANO_WEIERSTRASS_IMP_BOUNDED_FAN; BOLZANO_WEIERSTRASS_IMP_CLOSED_FAN;\r
1755              BOUNDED_CLOSED_IMP_COMPACT_FAN]]);;\r
1756 \r
1757 let COMPACT_EQ_BOUNDED_CLOSED_FAN = prove\r
1758  (`!s:real^N->bool. compact_fan s <=> bounded_fan s /\ closed_fan s`,\r
1759   GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[BOUNDED_CLOSED_IMP_COMPACT_FAN] THEN\r
1760   SIMP_TAC[COMPACT_EQ_BOLZANO_WEIERSTRASS_FAN; BOLZANO_WEIERSTRASS_IMP_BOUNDED_FAN;\r
1761            BOLZANO_WEIERSTRASS_IMP_CLOSED_FAN]);;\r
1762 \r
1763 let COMPACT_IMP_BOUNDED_FAN = prove\r
1764  (`!s. compact_fan s ==> bounded_fan s`,\r
1765   SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED_FAN]);;\r
1766 \r
1767 let COMPACT_IMP_CLOSED_FAN = prove\r
1768  (`!s. compact_fan s ==> closed_fan s`,\r
1769   SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED_FAN]);;\r
1770 \r
1771 (* ------------------------------------------------------------------------- *)\r
1772 (* In particular, some common special cases.                                 *)\r
1773 (* ------------------------------------------------------------------------- *)\r
1774 \r
1775 let COMPACT_EMPTY_FAN = prove\r
1776  (`compact_fan {}`,\r
1777   REWRITE_TAC[compact_fan; NOT_IN_EMPTY]);;\r
1778 \r
1779 let COMPACT_UNION_FAN = prove\r
1780  (`!s t. compact_fan s /\ compact_fan t ==> compact_fan (s UNION t)`,\r
1781   SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED_FAN; BOUNDED_UNION_FAN; CLOSED_UNION_FAN]);;\r
1782 \r
1783 let COMPACT_INTER_FAN = prove\r
1784  (`!s t. compact_fan s /\ compact_fan t ==> compact_fan (s INTER t)`,\r
1785   SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED_FAN; BOUNDED_INTER_FAN; CLOSED_INTER_FAN]);;\r
1786 \r
1787 let COMPACT_INTER_CLOSED_FAN = prove\r
1788  (`!s t. compact_fan s /\ closed_fan t ==> compact_fan (s INTER t)`,\r
1789   SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED_FAN; CLOSED_INTER_FAN] THEN\r
1790   MESON_TAC[BOUNDED_SUBSET_FAN; INTER_SUBSET]);;\r
1791 \r
1792 let CLOSED_INTER_COMPACT_FAN = prove\r
1793  (`!s t. closed_fan s /\ compact_fan t ==> compact_fan (s INTER t)`,\r
1794   MESON_TAC[COMPACT_INTER_CLOSED_FAN; INTER_COMM]);;\r
1795 \r
1796 let FINITE_IMP_CLOSED_FAN = prove\r
1797  (`!s. FINITE s ==> closed_fan s`,\r
1798   MESON_TAC[BOLZANO_WEIERSTRASS_IMP_CLOSED_FAN; INFINITE; FINITE_SUBSET]);;\r
1799 \r
1800 let FINITE_IMP_COMPACT_FAN = prove\r
1801  (`!s. FINITE s ==> compact_fan s`,\r
1802   SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED_FAN; FINITE_IMP_CLOSED_FAN; FINITE_IMP_BOUNDED_FAN]);;\r
1803 \r
1804 let COMPACT_SING_FAN = prove\r
1805  (`!a. compact_fan {a}`,\r
1806   SIMP_TAC[FINITE_IMP_COMPACT_FAN; FINITE_RULES]);;\r
1807 \r
1808 let CLOSED_SING_FAN = prove\r
1809  (`!a. closed_fan {a}`,\r
1810   MESON_TAC[COMPACT_EQ_BOUNDED_CLOSED_FAN; COMPACT_SING_FAN]);;\r
1811 \r
1812 let COMPACT_CBALL_FAN = prove\r
1813  (`!x e. compact_fan(cball_fan(x,e))`,\r
1814   REWRITE_TAC[COMPACT_EQ_BOUNDED_CLOSED_FAN; BOUNDED_CBALL_FAN; CLOSED_CBALL_FAN]);;\r
1815 \r
1816 let COMPACT_FRONTIER_BOUNDED_FAN = prove\r
1817  (`!s. bounded_fan s ==> compact_fan(frontier_fan s)`,\r
1818   SIMP_TAC[frontier_fan; COMPACT_EQ_BOUNDED_CLOSED_FAN;\r
1819            CLOSED_DIFF_FAN; OPEN_INTERIOR_FAN; CLOSED_CLOSURE_FAN] THEN\r
1820   MESON_TAC[SUBSET_DIFF; BOUNDED_SUBSET_FAN; BOUNDED_CLOSURE_FAN]);;\r
1821 \r
1822 let COMPACT_FRONTIER_FAN = prove\r
1823  (`!s. compact_fan s ==> compact_fan (frontier_fan s)`,\r
1824   MESON_TAC[COMPACT_EQ_BOUNDED_CLOSED_FAN; COMPACT_FRONTIER_BOUNDED_FAN]);;\r
1825 \r
1826 let FRONTIER_SUBSET_COMPACT_FAN = prove\r
1827  (`!s. compact_fan s ==> frontier_fan s SUBSET s`,\r
1828   MESON_TAC[FRONTIER_SUBSET_CLOSED_FAN; COMPACT_EQ_BOUNDED_CLOSED_FAN]);;\r
1829 \r
1830 let open_delete_fan = prove(`s DELETE x = s DIFF {x}`,SET_TAC[]);;\r
1831 \r
1832 let OPEN_DELETE_FAN = prove\r
1833  (`!s x. open_fan s ==> open_fan(s DELETE x)`,\r
1834   \r
1835   SIMP_TAC[ open_delete_fan; OPEN_DIFF_FAN; CLOSED_SING_FAN]);;\r
1836 \r
1837 (* ------------------------------------------------------------------------- *)\r
1838 (* Finite intersection property. I could make it an equivalence in fact.     *)\r
1839 (* ------------------------------------------------------------------------- *)\r
1840   let compact_imp_fip_fan = prove(`(s = UNIV DIFF t) <=> (UNIV DIFF s = t)`,SET_TAC[]);;\r
1841 \r
1842 let COMPACT_IMP_FIP_FAN = prove\r
1843  (`!s:real^N->bool f.\r
1844         compact_fan s /\\r
1845         (!t. t IN f ==> closed_fan t) /\\r
1846         (!f'. FINITE f' /\ f' SUBSET f ==> ~(s INTER (INTERS f') = {}))\r
1847         ==> ~(s INTER (INTERS f) = {})`,\r
1848   REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN\r
1849   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [COMPACT_EQ_HEINE_BOREL_FAN]) THEN\r
1850   DISCH_THEN(MP_TAC o SPEC `IMAGE (\t:real^N->bool. UNIV DIFF t) f`) THEN\r
1851   ASM_SIMP_TAC[FORALL_IN_IMAGE] THEN\r
1852   DISCH_THEN(fun th -> REPEAT STRIP_TAC THEN MP_TAC th) THEN\r
1853   ASM_SIMP_TAC[OPEN_DIFF_FAN; CLOSED_DIFF_FAN; OPEN_UNIV_FAN; CLOSED_UNIV_FAN; NOT_IMP] THEN\r
1854   CONJ_TAC THENL\r
1855    [UNDISCH_TAC `(s:real^N->bool) INTER INTERS f = {}` THEN\r
1856     ONCE_REWRITE_TAC[SUBSET; EXTENSION] THEN\r
1857     REWRITE_TAC[IN_UNIONS; EXISTS_IN_IMAGE] THEN SET_TAC[];\r
1858     DISCH_THEN(X_CHOOSE_THEN `g:(real^N->bool)->bool` MP_TAC) THEN\r
1859     FIRST_X_ASSUM(MP_TAC o SPEC `IMAGE (\t:real^N->bool. UNIV DIFF t) g`) THEN\r
1860     ASM_CASES_TAC `FINITE(g:(real^N->bool)->bool)` THEN\r
1861     ASM_SIMP_TAC[FINITE_IMAGE] THEN ONCE_REWRITE_TAC[SUBSET; EXTENSION] THEN\r
1862     REWRITE_TAC[FORALL_IN_IMAGE; IN_INTER; IN_INTERS; IN_IMAGE; IN_DIFF;\r
1863                 IN_UNIV; NOT_IN_EMPTY;  compact_imp_fip_fan; UNWIND_THM1; IN_UNIONS] THEN\r
1864     SET_TAC[]]);;\r
1865 \r
1866 (* ------------------------------------------------------------------------- *)\r
1867 (* Bounded closed nest property (proof does not use Heine-Borel).            *)\r
1868 (* ------------------------------------------------------------------------- *)\r
1869 \r
1870 let BOUNDED_CLOSED_NEST_FAN = prove\r
1871  (`!s. (!n. closed_fan(s n)) /\ (!n. ~(s n = {})) /\\r
1872        (!m n. m <= n ==> s(n) SUBSET s(m)) /\\r
1873        bounded_fan(s 0)\r
1874        ==> ?a:real^N. !n:num. a IN s(n)`,\r
1875   GEN_TAC THEN REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; SKOLEM_THM] THEN\r
1876   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN\r
1877   DISCH_THEN(CONJUNCTS_THEN2\r
1878      (X_CHOOSE_TAC `a:num->real^N`) STRIP_ASSUME_TAC) THEN\r
1879   SUBGOAL_THEN `compact_fan(s 0:real^N->bool)` MP_TAC THENL\r
1880    [ASM_MESON_TAC[BOUNDED_CLOSED_IMP_COMPACT_FAN]; ALL_TAC] THEN\r
1881   REWRITE_TAC[compact_fan] THEN\r
1882   DISCH_THEN(MP_TAC o SPEC `a:num->real^N`) THEN\r
1883   ANTS_TAC THENL [ASM_MESON_TAC[SUBSET; LE_0]; ALL_TAC] THEN\r
1884   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `l:real^N` THEN\r
1885   REWRITE_TAC[LIM_SEQUENTIALLY_FAN; o_THM] THEN\r
1886   DISCH_THEN(X_CHOOSE_THEN `r:num->num` STRIP_ASSUME_TAC) THEN\r
1887   GEN_REWRITE_TAC I [TAUT `p <=> ~(~p)`] THEN\r
1888   GEN_REWRITE_TAC RAND_CONV [NOT_FORALL_THM] THEN\r
1889   DISCH_THEN(X_CHOOSE_THEN `N:num` MP_TAC) THEN\r
1890   MP_TAC(ISPECL [`l:real^N`; `(s:num->real^N->bool) N`]\r
1891                 CLOSED_APPROACHABLE_FAN) THEN\r
1892   ASM_MESON_TAC[SUBSET; LE_REFL; LE_TRANS; LE_CASES; MONOTONE_BIGGER_FAN]);;\r
1893 \r
1894 (* ------------------------------------------------------------------------- *)\r
1895 (* Decreasing case does not even need compactness, just completeness.        *)\r
1896 (* ------------------------------------------------------------------------- *)\r
1897 \r
1898 let DECREASING_CLOSED_NEST_FAN = prove\r
1899  (`!s. (!n. closed_fan(s n)) /\ (!n. ~(s n = {})) /\\r
1900        (!m n. m <= n ==> s(n) SUBSET s(m)) /\\r
1901        (!e. &0 < e ==> ?n. !x y. x IN s(n) /\ y IN s(n) ==> dist(x,y) < e)\r
1902        ==> ?a:real^N. !n:num. a IN s(n)`,\r
1903   GEN_TAC THEN REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; SKOLEM_THM] THEN\r
1904   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN\r
1905   DISCH_THEN(CONJUNCTS_THEN2\r
1906      (X_CHOOSE_TAC `a:num->real^N`) STRIP_ASSUME_TAC) THEN\r
1907   SUBGOAL_THEN `?l:real^N. (a --> l) sequentially_fan` MP_TAC THENL\r
1908    [ASM_MESON_TAC[cauchy_fan; GE; SUBSET; LE_TRANS; LE_REFL;\r
1909                   complete_fan; COMPLETE_UNIV_FAN; IN_UNIV];\r
1910     ASM_MESON_TAC[LIM_SEQUENTIALLY_FAN; CLOSED_APPROACHABLE_FAN;\r
1911                   SUBSET; LE_REFL; LE_TRANS; LE_CASES]]);;\r
1912 \r
1913 (* ------------------------------------------------------------------------- *)\r
1914 (* Strengthen it to the intersection actually being a singleton.             *)\r
1915 (* ------------------------------------------------------------------------- *)\r
1916 \r
1917 let DECREASING_CLOSED_NEST_SING_FAN = prove\r
1918  (`!s. (!n. closed_fan(s n)) /\ (!n. ~(s n = {})) /\\r
1919        (!m n. m <= n ==> s(n) SUBSET s(m)) /\\r
1920        (!e. &0 < e ==> ?n. !x y. x IN s(n) /\ y IN s(n) ==> dist(x,y) < e)\r
1921        ==> ?a:real^N. INTERS {t | ?n:num. t = s n} = {a}`,\r
1922   GEN_TAC THEN DISCH_TAC THEN\r
1923   FIRST_ASSUM(MP_TAC o MATCH_MP DECREASING_CLOSED_NEST_FAN) THEN\r
1924   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `a:real^N` THEN\r
1925   DISCH_TAC THEN REWRITE_TAC[EXTENSION; IN_INTERS; IN_SING; IN_ELIM_THM] THEN\r
1926   ASM_MESON_TAC[DIST_POS_LT; REAL_LT_REFL; SUBSET; LE_CASES]);;\r
1927 \r
1928 (* ------------------------------------------------------------------------- *)\r
1929 (* Define continuity over a net to take in restrictions of the set.          *)\r
1930 (* ------------------------------------------------------------------------- *)\r
1931 \r
1932 parse_as_infix ("continuous_fan",(12,"right"));;\r
1933 \r
1934 let continuous_fan = new_definition\r
1935   `f continuous_fan net_fan <=> (f --> f(netlimit_fan net_fan)) net_fan`;;\r
1936 \r
1937 let CONTINUOUS_WITHIN_FAN = prove\r
1938  (`!f x:real^M. f continuous_fan (at_fan x within_fan s) <=> (f --> f(x)) (at_fan x within_fan s)`,\r
1939 REPEAT GEN_TAC THEN REWRITE_TAC[continuous_fan]\r
1940 THEN ASM_CASES_TAC `trivial_limit_fan(at_fan (x:real^M) within_fan s)` THENL\r
1941    [ASM_REWRITE_TAC[lim_fan]; ASM_SIMP_TAC[NETLIMIT_WITHIN_FAN]]);;\r
1942 \r
1943 let CONTINUOUS_AT_FAN = prove\r
1944  (`!f (x:real^N). f continuous_fan (at_fan x) <=> (f --> f(x)) (at_fan x)`,\r
1945   ONCE_REWRITE_TAC[GSYM WITHIN_UNIV_FAN] THEN\r
1946   REWRITE_TAC[CONTINUOUS_WITHIN_FAN; IN_UNIV]);;\r
1947 \r
1948 (* ------------------------------------------------------------------------- *)\r
1949 (* Derive the epsilon-delta forms, which we often use as "definitions"       *)\r
1950 (* ------------------------------------------------------------------------- *)\r
1951 \r
1952 let continuous_within_fan = prove\r
1953  (`f continuous_fan (at_fan x within_fan s) <=>\r
1954         !e. &0 < e\r
1955             ==> ?d. &0 < d /\\r
1956                     !x'. x' IN s /\ dist(x',x) < d ==> dist(f(x'),f(x)) < e`,\r
1957   REWRITE_TAC[CONTINUOUS_WITHIN_FAN; LIM_WITHIN_FAN] THEN\r
1958   REWRITE_TAC[GSYM DIST_NZ] THEN MESON_TAC[DIST_REFL]);;\r
1959 \r
1960 let continuous_at_fan = prove\r
1961  (`f continuous_fan (at_fan x) <=>\r
1962         !e. &0 < e ==> ?d. &0 < d /\\r
1963                            !x'. dist(x',x) < d ==> dist(f(x'),f(x)) < e`,\r
1964   ONCE_REWRITE_TAC[GSYM WITHIN_UNIV_FAN] THEN\r
1965   REWRITE_TAC[continuous_within_fan; IN_UNIV]);;\r
1966 \r
1967 (* ------------------------------------------------------------------------- *)\r
1968 (* For setwise continuity, just start from the epsilon-delta definitions.    *)\r
1969 (* ------------------------------------------------------------------------- *)\r
1970 \r
1971 parse_as_infix ("continuous_on_fan",(12,"right"));;\r
1972 parse_as_infix ("uniformly_continuous_on_fan",(12,"right"));;\r
1973 \r
1974 let continuous_on_fan = new_definition\r
1975   `f continuous_on_fan s <=>\r
1976         !x. x IN s ==> !e. &0 < e\r
1977                            ==> ?d. &0 < d /\\r
1978                                    !x'. x' IN s /\ dist(x',x) < d\r
1979                                         ==> dist(f(x'),f(x)) < e`;;\r
1980 \r
1981 let uniformly_continuous_on_fan = new_definition\r
1982   `f uniformly_continuous_on_fan s <=>\r
1983         !e. &0 < e\r
1984             ==> ?d. &0 < d /\\r
1985                     !x x'. x IN s /\ x' IN s /\ dist(x',x) < d\r
1986                            ==> dist(f(x'),f(x)) < e`;;\r
1987 \r
1988 (* ------------------------------------------------------------------------- *)\r
1989 (* Some simple consequential lemmas.                                         *)\r
1990 (* ------------------------------------------------------------------------- *)\r
1991 \r
1992 let UNIFORMLY_CONTINUOUS_IMP_CONTINUOUS_FAN = prove\r
1993  (`!f s. f uniformly_continuous_on_fan s ==> f continuous_on_fan s`,\r
1994   REWRITE_TAC[uniformly_continuous_on_fan; continuous_on_fan] THEN MESON_TAC[]);;\r
1995 \r
1996 let CONTINUOUS_AT_IMP_CONTINUOUS_WITHIN_FAN = prove\r
1997  (`!f s x. f continuous_fan (at_fan x) ==> f continuous_fan (at_fan x within_fan s)`,\r
1998   SIMP_TAC[LIM_AT_WITHIN_FAN; CONTINUOUS_AT_FAN; CONTINUOUS_WITHIN_FAN]);;\r
1999 \r
2000 let CONTINUOUS_AT_IMP_CONTINUOUS_ON_FAN = prove\r
2001  (`!f s. (!x. x IN s ==> f continuous_fan (at_fan x)) ==> f continuous_on_fan s`,\r
2002   REWRITE_TAC[continuous_at_fan; continuous_on_fan] THEN MESON_TAC[]);;\r
2003 \r
2004 let CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN_FAN = prove\r
2005  (`!f s. f continuous_on_fan s <=> !x. x IN s ==> f continuous_fan (at_fan x within_fan s)`,\r
2006   REWRITE_TAC[continuous_on_fan; continuous_within_fan]);;\r
2007 \r
2008 let CONTINUOUS_ON_FAN = prove\r
2009  (`!f (s:real^N->bool).\r
2010         f continuous_on_fan s <=> !x. x IN s ==> (f --> f(x)) (at_fan x within_fan s)`,\r
2011   REWRITE_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN_FAN; CONTINUOUS_WITHIN_FAN]);;\r
2012 \r
2013 let CONTINUOUS_ON_EQ_CONTINUOUS_AT_FAN = prove\r
2014  (`!f:real^M->real^N s.\r
2015   open_fan s ==> (f continuous_on_fan s <=> (!x. x IN s ==> f continuous_fan (at_fan x)))`,\r
2016   SIMP_TAC[CONTINUOUS_ON_FAN; CONTINUOUS_AT_FAN; LIM_WITHIN_OPEN_FAN]);;\r
2017 \r
2018 let CONTINUOUS_WITHIN_SUBSET_FAN = prove\r
2019  (`!f s t x. f continuous_fan (at_fan x within_fan s) /\ t SUBSET s\r
2020              ==> f continuous_fan (at_fan x within_fan t)`,\r
2021    REWRITE_TAC[CONTINUOUS_WITHIN_FAN] THEN MESON_TAC[LIM_WITHIN_SUBSET_FAN]);;\r
2022 \r
2023 let CONTINUOUS_ON_SUBSET_FAN = prove\r
2024  (`!f s t. f continuous_on_fan s /\ t SUBSET s ==> f continuous_on_fan t`,\r
2025   REWRITE_TAC[CONTINUOUS_ON_FAN] THEN MESON_TAC[SUBSET; LIM_WITHIN_SUBSET_FAN]);;\r
2026 \r
2027 let CONTINUOUS_ON_INTERIOR_FAN = prove\r
2028  (`!f:real^M->real^N s x.\r
2029         f continuous_on_fan s /\ x IN interior_fan(s) ==> f continuous_fan at_fan x`,\r
2030   REWRITE_TAC[interior_fan; IN_ELIM_THM] THEN\r
2031   MESON_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_AT_FAN; CONTINUOUS_ON_SUBSET_FAN]);;\r
2032 \r
2033 (* ------------------------------------------------------------------------- *)\r
2034 (* Characterization of various kinds of continuity in terms of sequences.    *)\r
2035 (* ------------------------------------------------------------------------- *)\r
2036 \r
2037 let CONTINUOUS_WITHIN_SEQUENTIALLY_FAN = prove\r
2038  (`!f a:real^N.\r
2039         f continuous_fan (at_fan a within_fan s) <=>\r
2040                 !x. (!n. x(n) IN s) /\ (x --> a) sequentially_fan\r
2041                      ==> ((f o x) --> f(a)) sequentially_fan`,\r
2042   REPEAT GEN_TAC THEN REWRITE_TAC[continuous_within_fan] THEN EQ_TAC THENL\r
2043    [REWRITE_TAC[LIM_SEQUENTIALLY_FAN; o_THM] THEN MESON_TAC[]; ALL_TAC] THEN\r
2044   ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN\r
2045   REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; NOT_EXISTS_THM] THEN\r
2046   DISCH_THEN(X_CHOOSE_THEN `e:real` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN\r
2047   DISCH_THEN(MP_TAC o GEN `n:num` o SPEC `&1 / (&n + &1)`) THEN\r
2048   SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; REAL_OF_NUM_LE; REAL_POS; ARITH;\r
2049        REAL_ARITH `&0 <= n ==> &0 < n + &1`; NOT_FORALL_THM; SKOLEM_THM] THEN\r
2050   MATCH_MP_TAC MONO_EXISTS THEN REWRITE_TAC[NOT_IMP; FORALL_AND_THM] THEN\r
2051   X_GEN_TAC `y:num->real^N` THEN REWRITE_TAC[LIM_SEQUENTIALLY_FAN; o_THM] THEN\r
2052   STRIP_TAC THEN CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[LE_REFL]] THEN\r
2053   ASM_REWRITE_TAC[] THEN MATCH_MP_TAC FORALL_POS_MONO_1 THEN\r
2054   CONJ_TAC THENL [ASM_MESON_TAC[REAL_LT_TRANS]; ALL_TAC] THEN\r
2055   X_GEN_TAC `n:num` THEN EXISTS_TAC `n:num` THEN X_GEN_TAC `m:num` THEN\r
2056   DISCH_TAC THEN MATCH_MP_TAC REAL_LTE_TRANS THEN\r
2057   EXISTS_TAC `&1 / (&m + &1)` THEN ASM_REWRITE_TAC[] THEN\r
2058   ASM_SIMP_TAC[REAL_LE_INV2; real_div; REAL_ARITH `&0 <= x ==> &0 < x + &1`;\r
2059                REAL_POS; REAL_MUL_LID; REAL_LE_RADD; REAL_OF_NUM_LE]);;\r
2060 \r
2061 let CONTINUOUS_AT_SEQUENTIALLY_FAN = prove\r
2062  (`!f a:real^N.\r
2063         f continuous_fan (at_fan a) <=>\r
2064               !x. (x --> a) sequentially_fan\r
2065                   ==> ((f o x) --> f(a)) sequentially_fan`,\r
2066   ONCE_REWRITE_TAC[GSYM WITHIN_UNIV_FAN] THEN\r
2067   REWRITE_TAC[CONTINUOUS_WITHIN_SEQUENTIALLY_FAN; IN_UNIV]);;\r
2068 \r
2069 let CONTINUOUS_ON_SEQUENTIALLY_FAN = prove\r
2070  (`!f s:real^N->bool.\r
2071         f continuous_on_fan s <=>\r
2072               !x a. a IN s /\ (!n. x(n) IN s) /\ (x --> a) sequentially_fan\r
2073                     ==> ((f o x) --> f(a)) sequentially_fan`,\r
2074   REWRITE_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN_FAN;\r
2075               CONTINUOUS_WITHIN_SEQUENTIALLY_FAN] THEN MESON_TAC[]);;\r
2076 \r
2077 let UNIFORMLY_CONTINUOUS_ON_SEQUENTIALLY_FAN = prove\r
2078  (`!f s:real^N->bool.\r
2079         f uniformly_continuous_on_fan s <=>\r
2080               !x y. (!n. x(n) IN s) /\ (!n. y(n) IN s) /\\r
2081                     ((\n. x(n) - y(n)) --> vec 0) sequentially_fan\r
2082                     ==> ((\n. f(x(n)) - f(y(n))) --> vec 0) sequentially_fan`,\r
2083   REPEAT GEN_TAC THEN REWRITE_TAC[uniformly_continuous_on_fan] THEN\r
2084   REWRITE_TAC[LIM_SEQUENTIALLY_FAN; dist; VECTOR_SUB_RZERO] THEN\r
2085   EQ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN\r
2086   ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN\r
2087   REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; NOT_EXISTS_THM] THEN\r
2088   DISCH_THEN(X_CHOOSE_THEN `e:real` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN\r
2089   DISCH_THEN(MP_TAC o GEN `n:num` o SPEC `&1 / (&n + &1)`) THEN\r
2090   SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; REAL_OF_NUM_LE; REAL_POS; ARITH;\r
2091        REAL_ARITH `&0 <= n ==> &0 < n + &1`; NOT_FORALL_THM; SKOLEM_THM] THEN\r
2092   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `x:num->real^N` THEN\r
2093   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `y:num->real^N` THEN\r
2094   REWRITE_TAC[NOT_IMP; FORALL_AND_THM] THEN STRIP_TAC THEN\r
2095   ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[NORM_SUB] THEN CONJ_TAC THENL\r
2096    [MATCH_MP_TAC FORALL_POS_MONO_1 THEN\r
2097     CONJ_TAC THENL [ASM_MESON_TAC[REAL_LT_TRANS]; ALL_TAC] THEN\r
2098     X_GEN_TAC `n:num` THEN EXISTS_TAC `n:num` THEN X_GEN_TAC `m:num` THEN\r
2099     DISCH_TAC THEN MATCH_MP_TAC REAL_LTE_TRANS THEN\r
2100     EXISTS_TAC `&1 / (&m + &1)` THEN ASM_REWRITE_TAC[] THEN\r
2101     ASM_SIMP_TAC[REAL_LE_INV2; real_div; REAL_ARITH `&0 <= x ==> &0 < x + &1`;\r
2102                  REAL_POS; REAL_MUL_LID; REAL_LE_RADD; REAL_OF_NUM_LE];\r
2103     EXISTS_TAC `e:real` THEN ASM_REWRITE_TAC[] THEN\r
2104     EXISTS_TAC `\x:num. x` THEN ASM_REWRITE_TAC[LE_REFL]]);;\r
2105 \r
2106 (* ------------------------------------------------------------------------- *)\r
2107 (* Combination results for pointwise continuity.                             *)\r
2108 (* ------------------------------------------------------------------------- *)\r
2109 \r
2110 let CONTINUOUS_CONST_FAN = prove\r
2111  (`!net c. (\x. c) continuous_fan net_fan`,\r
2112   REWRITE_TAC[continuous_fan; LIM_CONST_FAN]);;\r
2113 \r
2114 let CONTINUOUS_CMUL_FAN = prove\r
2115  (`!f c net. f continuous_fan net_fan ==> (\x. c % f(x)) continuous_fan net_fan`,\r
2116   REWRITE_TAC[continuous_fan; LIM_CMUL_FAN]);;\r
2117 \r
2118 let CONTINUOUS_NEG_FAN = prove\r
2119  (`!f net. f continuous_fan net_fan ==> (\x. --(f x)) continuous_fan net_fan`,\r
2120   REWRITE_TAC[continuous_fan; LIM_NEG_FAN]);;\r
2121 \r
2122 let CONTINUOUS_ADD_FAN = prove\r
2123  (`!f g net. f continuous_fan net_fan /\ g continuous_fan net_fan\r
2124            ==> (\x. f(x) + g(x)) continuous_fan net_fan`,\r
2125   REWRITE_TAC[continuous_fan; LIM_ADD_FAN]);;\r
2126 \r
2127 let CONTINUOUS_SUB_FAN = prove\r
2128  (`!f g net. f continuous_fan net_fan /\ g continuous_fan net_fan\r
2129            ==> (\x. f(x) - g(x)) continuous_fan net_fan`,\r
2130   REWRITE_TAC[continuous_fan; LIM_SUB_FAN]);;\r
2131 \r
2132 (* ------------------------------------------------------------------------- *)\r
2133 (* Same thing for setwise continuity.                                        *)\r
2134 (* ------------------------------------------------------------------------- *)\r
2135 \r
2136 let CONTINUOUS_ON_CONST_FAN = prove\r
2137  (`!s c. (\x. c) continuous_on_fan s`,\r
2138   SIMP_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN_FAN; CONTINUOUS_CONST_FAN]);;\r
2139 \r
2140 let CONTINUOUS_ON_CMUL_FAN = prove\r
2141  (`!f c s. f continuous_on_fan s ==> (\x. c % f(x)) continuous_on_fan s`,\r
2142   SIMP_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN_FAN; CONTINUOUS_CMUL_FAN]);;\r
2143 \r
2144 let CONTINUOUS_ON_NEG_FAN = prove\r
2145  (`!f s. f continuous_on_fan s\r
2146          ==> (\x. --(f x)) continuous_on_fan s`,\r
2147   SIMP_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN_FAN; CONTINUOUS_NEG_FAN]);;\r
2148 \r
2149 let CONTINUOUS_ON_ADD_FAN = prove\r
2150  (`!f g s. f continuous_on_fan s /\ g continuous_on_fan s\r
2151            ==> (\x. f(x) + g(x)) continuous_on_fan s`,\r
2152   SIMP_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN_FAN; CONTINUOUS_ADD_FAN]);;\r
2153 \r
2154 let CONTINUOUS_ON_SUB_FAN = prove\r
2155  (`!f g s. f continuous_on_fan s /\ g continuous_on_fan s\r
2156            ==> (\x. f(x) - g(x)) continuous_on_fan s`,\r
2157   SIMP_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN_FAN; CONTINUOUS_SUB_FAN]);;\r
2158 \r
2159 (* ------------------------------------------------------------------------- *)\r
2160 (* Same thing for uniform continuity, using sequential formulations.         *)\r
2161 (* ------------------------------------------------------------------------- *)\r
2162 \r
2163 let UNIFORMLY_CONTINUOUS_ON_CONST_FAN = prove\r
2164  (`!s c. (\x. c) uniformly_continuous_on_fan s`,\r
2165   REWRITE_TAC[UNIFORMLY_CONTINUOUS_ON_SEQUENTIALLY_FAN; o_DEF;\r
2166               VECTOR_SUB_REFL; LIM_CONST_FAN]);;\r
2167 \r
2168 let UNIFORMLY_CONTINUOUS_ON_CMUL_FAN = prove\r
2169  (`!f c s. f uniformly_continuous_on_fan s\r
2170            ==> (\x. c % f(x)) uniformly_continuous_on_fan s`,\r
2171   REPEAT GEN_TAC THEN REWRITE_TAC[UNIFORMLY_CONTINUOUS_ON_SEQUENTIALLY_FAN] THEN\r
2172   REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN\r
2173   DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN\r
2174   ASM_REWRITE_TAC[] THEN\r
2175   DISCH_THEN(MP_TAC o MATCH_MP LIM_CMUL_FAN) THEN\r
2176   ASM_SIMP_TAC[VECTOR_SUB_LDISTRIB; VECTOR_MUL_RZERO]);;\r
2177 \r
2178 let UNIFORMLY_CONTINUOUS_ON_NEG_FAN = prove\r
2179  (`!f s. f uniformly_continuous_on_fan s\r
2180          ==> (\x. --(f x)) uniformly_continuous_on_fan s`,\r
2181   ONCE_REWRITE_TAC[VECTOR_NEG_MINUS1] THEN\r
2182   REWRITE_TAC[UNIFORMLY_CONTINUOUS_ON_CMUL_FAN]);;\r
2183 \r
2184 let UNIFORMLY_CONTINUOUS_ON_ADD_FAN = prove\r
2185  (`!f g s. f uniformly_continuous_on_fan s /\ g uniformly_continuous_on_fan s\r
2186            ==> (\x. f(x) + g(x)) uniformly_continuous_on_fan s`,\r
2187   REPEAT GEN_TAC THEN REWRITE_TAC[UNIFORMLY_CONTINUOUS_ON_SEQUENTIALLY_FAN] THEN\r
2188   REWRITE_TAC[AND_FORALL_THM] THEN\r
2189   REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN\r
2190   DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN\r
2191   ASM_REWRITE_TAC[o_DEF] THEN DISCH_THEN(MP_TAC o MATCH_MP LIM_ADD_FAN) THEN\r
2192   MATCH_MP_TAC EQ_IMP THEN\r
2193   REWRITE_TAC[VECTOR_ADD_LID] THEN AP_THM_TAC THEN BINOP_TAC THEN\r
2194   REWRITE_TAC[FUN_EQ_THM] THEN VECTOR_ARITH_TAC);;\r
2195 \r
2196 let UNIFORMLY_CONTINUOUS_ON_SUB_FAN = prove\r
2197  (`!f g s. f uniformly_continuous_on_fan s /\ g uniformly_continuous_on_fan s\r
2198            ==> (\x. f(x) - g(x)) uniformly_continuous_on_fan s`,\r
2199   REWRITE_TAC[VECTOR_SUB] THEN\r
2200   SIMP_TAC[UNIFORMLY_CONTINUOUS_ON_NEG_FAN; UNIFORMLY_CONTINUOUS_ON_ADD_FAN]);;\r
2201 \r
2202 (* ------------------------------------------------------------------------- *)\r
2203 (* Identity function is continuous in every sense.                           *)\r
2204 (* ------------------------------------------------------------------------- *)\r
2205 \r
2206 let CONTINUOUS_WITHIN_ID_FAN = prove\r
2207  (`!net_fan a s. (\x. x) continuous_fan (at_fan a within_fan s)`,\r
2208   REWRITE_TAC[continuous_within_fan] THEN MESON_TAC[]);;\r
2209 \r
2210 let CONTINUOUS_AT_ID_FAN = prove\r
2211  (`!net_fan s. (\x. x) continuous_fan (at_fan a)`,\r
2212   REWRITE_TAC[continuous_at_fan] THEN MESON_TAC[]);;\r
2213 \r
2214 let CONTINUOUS_ON_ID_FAN = prove\r
2215  (`!s. (\x. x) continuous_on_fan s`,\r
2216   REWRITE_TAC[continuous_on_fan] THEN MESON_TAC[]);;\r
2217 \r
2218 let UNIFORMLY_CONTINUOUS_ON_ID_FAN = prove\r
2219  (`!s. (\x. x) uniformly_continuous_on_fan s`,\r
2220   REWRITE_TAC[uniformly_continuous_on_fan] THEN MESON_TAC[]);;\r
2221 \r
2222 (* ------------------------------------------------------------------------- *)\r
2223 (* Continuity of all kinds is preserved under composition.                   *)\r
2224 (* ------------------------------------------------------------------------- *)\r
2225 \r
2226 let CONTINUOUS_WITHIN_COMPOSE_FAN = prove\r
2227  (`!f g x s. f continuous_fan (at_fan x within_fan s) /\\r
2228              g continuous_fan (at_fan (f x) within_fan IMAGE f s)\r
2229              ==> (g o f) continuous_fan (at_fan x within_fan s)`,\r
2230   REPEAT GEN_TAC THEN REWRITE_TAC[continuous_within_fan; o_THM; IN_IMAGE] THEN\r
2231   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN\r
2232   MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `e:real` THEN\r
2233   ASM_MESON_TAC[]);;\r
2234 \r
2235 let CONTINUOUS_AT_COMPOSE_FAN = prove\r
2236  (`!f g x. f continuous_fan (at_fan x) /\ g continuous_fan (at_fan (f x))\r
2237            ==> (g o f) continuous_fan (at_fan x)`,\r
2238   ONCE_REWRITE_TAC[GSYM WITHIN_UNIV_FAN] THEN\r
2239   MESON_TAC[CONTINUOUS_WITHIN_COMPOSE_FAN; IN_IMAGE; CONTINUOUS_WITHIN_SUBSET_FAN;\r
2240             SUBSET_UNIV; IN_UNIV]);;\r
2241 \r
2242 let CONTINUOUS_ON_COMPOSE_FAN = prove\r
2243  (`!f g s. f continuous_on_fan s /\ g continuous_on_fan (IMAGE f s)\r
2244            ==> (g o f) continuous_on_fan s`,\r
2245   REWRITE_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN_FAN] THEN\r
2246   MESON_TAC[IN_IMAGE; CONTINUOUS_WITHIN_COMPOSE_FAN]);;\r
2247 \r
2248 \r
2249 let UNIFORMLY_CONTINUOUS_ON_COMPOSE_FAN = prove\r
2250  (`!f g s. f uniformly_continuous_on_fan s /\\r
2251            g uniformly_continuous_on_fan (IMAGE f s)\r
2252            ==> (g o f) uniformly_continuous_on_fan s`,\r
2253 (let lemma1 = prove\r
2254    (`(!y. ((?x. (y = f x) /\ P x) /\ Q y ==> R y)) <=>\r
2255      (!x. P x /\ Q (f x) ==> R (f x))`,\r
2256      MESON_TAC[]) in\r
2257   REPEAT GEN_TAC THEN\r
2258   REWRITE_TAC[uniformly_continuous_on_fan; o_THM; IN_IMAGE] THEN\r
2259   ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN REWRITE_TAC[lemma1] THEN\r
2260   ONCE_REWRITE_TAC[TAUT `a /\ b /\ c <=> b /\ a /\ c`] THEN\r
2261   ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN REWRITE_TAC[lemma1] THEN\r
2262   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN\r
2263   MATCH_MP_TAC MONO_FORALL THEN\r
2264   X_GEN_TAC `e:real` THEN ASM_CASES_TAC `&0 < e` THEN ASM_REWRITE_TAC[] THEN\r
2265   ASM_MESON_TAC[]));;\r
2266 \r
2267 (* ------------------------------------------------------------------------- *)\r
2268 (* Continuity in terms of open preimages.                                    *)\r
2269 (* ------------------------------------------------------------------------- *)\r
2270 let CONTINUOUS_AT_OPEN_FAN = prove\r
2271  (`!f:real^M->real^N x.\r
2272      f continuous_fan (at_fan x) <=>\r
2273         !t. open_fan t /\ f(x) IN t\r
2274             ==> ?s. open_fan s /\ x IN s /\\r
2275                     !x'. x' IN s ==> f(x') IN t`,\r
2276   REPEAT GEN_TAC THEN REWRITE_TAC[continuous_at_fan] THEN EQ_TAC THENL\r
2277    [DISCH_TAC THEN X_GEN_TAC `t:real^N->bool` THEN\r
2278     DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN\r
2279     GEN_REWRITE_TAC LAND_CONV [open_def_fan] THEN\r
2280     DISCH_THEN(MP_TAC o SPEC `(f:real^M->real^N) x`) THEN\r
2281     ASM_MESON_TAC[IN_BALL_FAN; DIST_SYM; OPEN_BALL_FAN; CENTRE_IN_BALL];\r
2282     DISCH_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN\r
2283     FIRST_X_ASSUM(MP_TAC o SPEC `ball_fan((f:real^M->real^N) x,e)`) THEN\r
2284     ASM_SIMP_TAC[OPEN_BALL_FAN; CENTRE_IN_BALL] THEN\r
2285     MESON_TAC[open_def_fan; IN_BALL_FAN; REAL_LT_TRANS; DIST_SYM]]);;\r
2286 \r
2287 \r
2288 let CONTINUOUS_ON_OPEN_FAN = prove\r
2289  (`!f:real^M->real^N s.\r
2290       f continuous_on_fan s <=>\r
2291         !t. t open_in (IMAGE f s) ==> {x | x IN s /\ f(x) IN t} open_in s`,\r
2292   REPEAT GEN_TAC THEN REWRITE_TAC[continuous_on_fan] THEN EQ_TAC THENL\r
2293    [REWRITE_TAC[open_in; SUBSET; IN_ELIM_THM] THEN\r
2294     DISCH_TAC THEN X_GEN_TAC `t:real^N->bool` THEN STRIP_TAC THEN\r
2295     CONJ_TAC THENL [ASM_MESON_TAC[DIST_REFL]; ALL_TAC] THEN\r
2296     X_GEN_TAC `x:real^M` THEN STRIP_TAC THEN\r
2297     FIRST_X_ASSUM(MP_TAC o SPEC `(f:real^M->real^N) x`) THEN\r
2298     ASM_REWRITE_TAC[IN_IMAGE] THEN ASM_MESON_TAC[];\r
2299     DISCH_TAC THEN X_GEN_TAC `x:real^M` THEN\r
2300     DISCH_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN\r
2301     FIRST_X_ASSUM(MP_TAC o\r
2302       SPEC `ball_fan((f:real^M->real^N) x,e) INTER (IMAGE f s)`) THEN\r
2303     ANTS_TAC THENL\r
2304      [ASM_MESON_TAC[OPEN_IN_OPEN_FAN; INTER_COMM; OPEN_BALL_FAN]; ALL_TAC] THEN\r
2305     REWRITE_TAC[open_in; SUBSET; IN_INTER; IN_ELIM_THM; IN_BALL_FAN; IN_IMAGE] THEN\r
2306     REWRITE_TAC[AND_FORALL_THM] THEN DISCH_THEN(MP_TAC o SPEC `x:real^M`) THEN\r
2307     ASM_MESON_TAC[DIST_REFL; DIST_SYM]]);;\r
2308 \r
2309 (* ------------------------------------------------------------------------- *)\r
2310 (* Similarly in terms of closed sets.                                        *)\r
2311 (* ------------------------------------------------------------------------- *)\r
2312 \r
2313 let CONTINUOUS_ON_CLOSED_FAN = prove\r
2314  (`!f:real^M->real^N s.\r
2315       f continuous_on_fan s <=>\r
2316         !t. t closed_in (IMAGE f s) ==> {x | x IN s /\ f(x) IN t} closed_in s`,\r
2317   REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[CONTINUOUS_ON_OPEN_FAN] THEN EQ_TAC THEN\r
2318   DISCH_TAC THEN X_GEN_TAC `t:real^N->bool` THEN\r
2319   FIRST_X_ASSUM(MP_TAC o SPEC `IMAGE (f:real^M->real^N) s DIFF t`) THENL\r
2320    [REWRITE_TAC[closed_in]; REWRITE_TAC[OPEN_IN_CLOSED_IN_EQ]] THEN\r
2321   MATCH_MP_TAC(TAUT`d /\ (b <=> e) ==> ((a ==> b) ==> c /\ a ==> d /\ e)`) THEN\r
2322   (CONJ_TAC THENL [SIMP_TAC[SUBSET; IN_ELIM_THM]; ALL_TAC] THEN\r
2323    AP_THM_TAC THEN AP_TERM_TAC THEN\r
2324    REWRITE_TAC[EXTENSION; IN_DIFF; IN_IMAGE; IN_ELIM_THM] THEN MESON_TAC[]));;\r
2325 \r
2326 (* ------------------------------------------------------------------------- *)\r
2327 (* The "global" cases.                                                       *)\r
2328 (* ------------------------------------------------------------------------- *)\r
2329 \r
2330 let CONTINOUS_OPEN_PREIMAGE_FAN = prove\r
2331  (`!f:real^M->real^N s.\r
2332         (!x. f continuous_fan (at_fan x)) /\ s SUBSET (IMAGE f UNIV) /\ open_fan s\r
2333         ==> open_fan {x | f(x) IN s}`,\r
2334   REPEAT STRIP_TAC THEN\r
2335   MP_TAC(SPECL [`f:real^M->real^N`; `(:real^M)`]\r
2336            CONTINUOUS_ON_OPEN_FAN) THEN\r
2337   ASM_SIMP_TAC[CONTINUOUS_AT_IMP_CONTINUOUS_ON_FAN; IN_UNIV; GSYM OPEN_IN_FAN] THEN\r
2338   DISCH_THEN MATCH_MP_TAC THEN\r
2339   UNDISCH_TAC `open_fan(s:real^N->bool)` THEN\r
2340   REWRITE_TAC[open_def_fan; open_in] THEN ASM_MESON_TAC[]);;\r
2341 \r
2342 let OPEN_TRANSLATION_FAN = prove\r
2343  (`!s a:real^N. open_fan s ==> open_fan(IMAGE (\x. a + x) s)`,\r
2344   REPEAT STRIP_TAC THEN\r
2345   MP_TAC(ISPECL [`\x:real^N. x - a`; `s:real^N->bool`]\r
2346          CONTINOUS_OPEN_PREIMAGE_FAN) THEN\r
2347   ASM_SIMP_TAC[CONTINUOUS_SUB_FAN; CONTINUOUS_AT_ID_FAN; CONTINUOUS_CONST_FAN] THEN\r
2348   MATCH_MP_TAC(TAUT `a /\ b = c ==> (a ==> b) ==> c`) THEN\r
2349   CONJ_TAC THENL\r
2350    [REWRITE_TAC[SUBSET]; AP_TERM_TAC THEN REWRITE_TAC[EXTENSION]] THEN\r
2351   REWRITE_TAC[IN_ELIM_THM; IN_IMAGE; IN_UNIV] THEN\r
2352   ASM_MESON_TAC[VECTOR_ARITH `(a + x) - a = x:real^N`;\r
2353                 VECTOR_ARITH `a + (x - a) = x:real^N`]);;\r
2354 \r
2355 (* ------------------------------------------------------------------------- *)\r
2356 (* Preservation of compactness and connectedness under continuous function.  *)\r
2357 (* ------------------------------------------------------------------------- *)\r
2358 \r
2359 let COMPACT_CONTINUOUS_IMAGE_FAN = prove\r
2360  (`!f:real^M->real^N s.\r
2361         f continuous_on_fan s /\ compact_fan s ==> compact_fan(IMAGE f s)`,\r
2362   REPEAT GEN_TAC THEN REWRITE_TAC[continuous_on_fan; compact_fan] THEN\r
2363   STRIP_TAC THEN X_GEN_TAC `y:num->real^N` THEN\r
2364   REWRITE_TAC[IN_IMAGE; SKOLEM_THM; FORALL_AND_THM] THEN\r
2365   DISCH_THEN(X_CHOOSE_THEN `x:num->real^M` STRIP_ASSUME_TAC) THEN\r
2366   FIRST_X_ASSUM(MP_TAC o SPEC `x:num->real^M`) THEN ASM_REWRITE_TAC[] THEN\r
2367   ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN MATCH_MP_TAC MONO_EXISTS THEN\r
2368   X_GEN_TAC `r:num->num` THEN\r
2369   DISCH_THEN(X_CHOOSE_THEN `l:real^M` STRIP_ASSUME_TAC) THEN\r
2370   EXISTS_TAC `(f:real^M->real^N) l` THEN ASM_REWRITE_TAC[] THEN\r
2371   CONJ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN\r
2372   REWRITE_TAC[LIM_SEQUENTIALLY_FAN] THEN\r
2373   FIRST_X_ASSUM(MP_TAC o SPEC `l:real^M`) THEN\r
2374   ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `e:real` THEN\r
2375   DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN\r
2376   DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN\r
2377   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [LIM_SEQUENTIALLY_FAN]) THEN\r
2378   DISCH_THEN(MP_TAC o SPEC `d:real`) THEN ASM_REWRITE_TAC[o_THM] THEN\r
2379   ASM_MESON_TAC[]);;\r
2380 \r
2381 let CONNECTED_CONTINUOUS_IMAGE_FAN = prove\r
2382  (`!f:real^M->real^N s.\r
2383         f continuous_on_fan s /\ connected_fan s ==> connected_fan(IMAGE f s)`,\r
2384   REPEAT GEN_TAC THEN REWRITE_TAC[CONTINUOUS_ON_OPEN_FAN] THEN\r
2385   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN\r
2386   ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN\r
2387   REWRITE_TAC[CONNECTED_CLOPEN_FAN; NOT_FORALL_THM; NOT_IMP; DE_MORGAN_THM] THEN\r
2388   REWRITE_TAC[closed_in] THEN\r
2389   DISCH_THEN(X_CHOOSE_THEN `t:real^N->bool` STRIP_ASSUME_TAC) THEN\r
2390   FIRST_X_ASSUM(fun th -> MP_TAC(SPEC `t:real^N->bool` th) THEN\r
2391     MP_TAC(SPEC `IMAGE (f:real^M->real^N) s DIFF t` th)) THEN\r
2392   ASM_REWRITE_TAC[] THEN\r
2393   SUBGOAL_THEN `{x | x IN s /\ (f:real^M->real^N) x IN IMAGE f s DIFF t} =\r
2394                 s DIFF {x | x IN s /\ f x IN t}`\r
2395   SUBST1_TAC THENL\r
2396    [UNDISCH_TAC `t SUBSET IMAGE (f:real^M->real^N) s` THEN\r
2397     REWRITE_TAC[EXTENSION; IN_IMAGE; IN_DIFF; IN_ELIM_THM; SUBSET] THEN\r
2398     MESON_TAC[];\r
2399     REPEAT STRIP_TAC THEN\r
2400     EXISTS_TAC `{x | x IN s /\ (f:real^M->real^N) x IN t}` THEN\r
2401     ASM_REWRITE_TAC[] THEN POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN\r
2402     REWRITE_TAC[IN_IMAGE; SUBSET; IN_ELIM_THM; NOT_IN_EMPTY; EXTENSION] THEN\r
2403     MESON_TAC[]]);;\r
2404 \r
2405 (* ------------------------------------------------------------------------- *)\r
2406 (* Continuity implies uniform continuity on a compact domain.                *)\r
2407 (* ------------------------------------------------------------------------- *)\r
2408 \r
2409 let COMPACT_UNIFORMLY_CONTINUOUS_FAN = prove\r
2410  (`!f:real^M->real^N s.\r
2411         f continuous_on_fan s /\ compact_fan s ==> f uniformly_continuous_on_fan s`,\r
2412   REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN\r
2413   REWRITE_TAC[continuous_on_fan; RIGHT_IMP_EXISTS_THM; SKOLEM_THM] THEN\r
2414   DISCH_THEN(X_CHOOSE_TAC `d:real^M->real->real`) THEN\r
2415   REWRITE_TAC[uniformly_continuous_on_fan] THEN X_GEN_TAC `e:real` THEN\r
2416   DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o MATCH_MP HEINE_BOREL_LEMMA_FAN) THEN\r
2417   DISCH_THEN(MP_TAC o SPEC\r
2418     `{b | ?x:real^M. x IN s /\ (b = ball_fan(x,d x (e / &2)))}`) THEN\r
2419   REWRITE_TAC[SUBSET; IN_UNIONS; IN_ELIM_THM; IN_BALL_FAN] THEN\r
2420   ANTS_TAC THENL\r
2421    [ASM_MESON_TAC[CENTRE_IN_BALL; REAL_HALF; OPEN_BALL_FAN]; ALL_TAC] THEN\r
2422   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `k:real` THEN STRIP_TAC THEN\r
2423   ASM_REWRITE_TAC[] THEN MAP_EVERY X_GEN_TAC [`u:real^M`; `v:real^M`] THEN\r
2424   STRIP_TAC THEN FIRST_X_ASSUM(fun th -> MP_TAC(SPEC `v:real^M` th) THEN\r
2425     ASM_REWRITE_TAC[] THEN DISCH_THEN(CHOOSE_THEN MP_TAC)) THEN\r
2426   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN\r
2427   DISCH_THEN(fun th ->\r
2428     MP_TAC(SPEC `u:real^M` th) THEN MP_TAC(SPEC `v:real^M` th)) THEN\r
2429   ASM_REWRITE_TAC[DIST_REFL] THEN\r
2430   FIRST_X_ASSUM(X_CHOOSE_THEN `w:real^M` (CONJUNCTS_THEN2 ASSUME_TAC\r
2431     SUBST_ALL_TAC)) THEN\r
2432   REWRITE_TAC[IN_BALL_FAN] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN\r
2433   REPEAT DISCH_TAC THEN MATCH_MP_TAC DIST_TRIANGLE_HALF_L THEN\r
2434   ASM_MESON_TAC[REAL_HALF]);;\r
2435 \r
2436 (* ------------------------------------------------------------------------- *)\r
2437 (* Continuity of inverse function on compact domain.                         *)\r
2438 (* ------------------------------------------------------------------------- *)\r
2439 \r
2440 let CONTINUOUS_ON_INVERSE_FAN = prove\r
2441  (`!f:real^M->real^N g s.\r
2442         f continuous_on_fan s /\ compact_fan s /\ (!x. x IN s ==> (g(f(x)) = x))\r
2443         ==> g continuous_on_fan (IMAGE f s)`,\r
2444   REPEAT STRIP_TAC THEN REWRITE_TAC[CONTINUOUS_ON_CLOSED_FAN] THEN\r
2445   SUBGOAL_THEN `IMAGE g (IMAGE (f:real^M->real^N) s) = s` SUBST1_TAC THENL\r
2446    [REWRITE_TAC[EXTENSION; IN_IMAGE] THEN ASM_MESON_TAC[]; ALL_TAC] THEN\r
2447   X_GEN_TAC `t:real^M->bool` THEN DISCH_TAC THEN\r
2448   REWRITE_TAC[CLOSED_IN_CLOSED_FAN] THEN\r
2449   EXISTS_TAC `IMAGE (f:real^M->real^N) t` THEN CONJ_TAC THENL\r
2450    [ASM_MESON_TAC[COMPACT_EQ_BOUNDED_CLOSED_FAN; BOUNDED_SUBSET_FAN; CLOSED_IN_SUBSET;\r
2451        CONTINUOUS_ON_SUBSET_FAN; CLOSED_IN_CLOSED_TRANS_FAN; COMPACT_CONTINUOUS_IMAGE_FAN];\r
2452     REWRITE_TAC[EXTENSION; IN_INTER; IN_ELIM_THM; IN_IMAGE] THEN\r
2453     ASM_MESON_TAC[CLOSED_IN_SUBSET; SUBSET]]);;\r
2454 \r
2455 (* ------------------------------------------------------------------------- *)\r
2456 (* Topological properties of linear functions.                               *)\r
2457 (* ------------------------------------------------------------------------- *)\r
2458 \r
2459 let LINEAR_LIM_0_FAN = prove\r
2460  (`!f. linear f ==> (f --> vec 0) (at_fan (vec 0))`,\r
2461   REPEAT STRIP_TAC THEN REWRITE_TAC[LIM_AT_FAN] THEN\r
2462   FIRST_X_ASSUM(MP_TAC o MATCH_MP LINEAR_BOUNDED_POS) THEN\r
2463   DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN\r
2464   X_GEN_TAC `e:real` THEN DISCH_TAC THEN EXISTS_TAC `e / B` THEN\r
2465   ASM_SIMP_TAC[REAL_LT_DIV] THEN REWRITE_TAC[dist; VECTOR_SUB_RZERO] THEN\r
2466   ASM_MESON_TAC[REAL_MUL_SYM; REAL_LET_TRANS; REAL_LT_RDIV_EQ]);;\r
2467 (*error in old file*)\r
2468 let LINEAR_CONTINUOUS_AT_FAN = prove\r
2469  (`!f:real^M->real^N a. linear f ==> f continuous_fan (at_fan a)`,\r
2470   REPEAT STRIP_TAC THEN\r
2471   MP_TAC(ISPEC `\x. (f:real^M->real^N) (a + x) - f(a)` LINEAR_LIM_0_FAN) THEN\r
2472   ANTS_TAC THENL\r
2473    [POP_ASSUM MP_TAC THEN SIMP_TAC[linear] THEN\r
2474     REPEAT STRIP_TAC THEN VECTOR_ARITH_TAC;\r
2475    ALL_TAC  THEN\r
2476  REWRITE_TAC[GSYM LIM_NULL_FAN; CONTINUOUS_AT_FAN]THEN\r
2477   GEN_REWRITE_TAC RAND_CONV [LIM_AT_ZERO_FAN] THEN SIMP_TAC[]]);;\r
2478 \r
2479 \r
2480 let LINEAR_CONTINUOUS_WITHIN_FAN = prove\r
2481  (`!f:real^M->real^N s a. linear f ==> f continuous_fan (at_fan x within_fan s)`,\r
2482   SIMP_TAC[CONTINUOUS_AT_IMP_CONTINUOUS_WITHIN_FAN; LINEAR_CONTINUOUS_AT_FAN]);;\r
2483 \r
2484 \r
2485 let LINEAR_CONTINUOUS_ON_FAN = prove\r
2486  (`!f:real^M->real^N s. linear f ==> f continuous_on_fan s`,\r
2487   MESON_TAC[LINEAR_CONTINUOUS_AT_FAN; CONTINUOUS_AT_IMP_CONTINUOUS_ON_FAN]);;\r
2488 \r
2489 (* ------------------------------------------------------------------------- *)\r
2490 (* Topological stuff lifted from and dropped to R                            *)\r
2491 (* ------------------------------------------------------------------------- *)\r
2492 \r
2493 let OPEN_LIFT_FAN = prove\r
2494  (`!s. open_fan(IMAGE lift s) <=>\r
2495         !x. x IN s ==> ?e. &0 < e /\ !x'. abs(x' - x) < e ==> x' IN s`,\r
2496   REWRITE_TAC[open_def_fan; FORALL_LIFT; LIFT_IN_IMAGE_LIFT; DIST_LIFT]);;\r
2497 \r
2498 let BOUNDED_LIFT_FAN = prove\r
2499  (`!s. bounded_fan(IMAGE lift s) <=>  ?a. !x. x IN s ==> abs(x) <= a`,\r
2500   REWRITE_TAC[bounded_fan; FORALL_LIFT; NORM_LIFT; LIFT_IN_IMAGE_LIFT]);;\r
2501 \r
2502 let LIMPT_APPROACHABLE_LIFT_FAN = prove\r
2503  (`!x s. (lift x) limit_point_of_fan (IMAGE lift s) <=>\r
2504          !e. &0 < e ==> ?x'. x' IN s /\ ~(x' = x) /\ abs(x' - x) < e`,\r
2505   REWRITE_TAC[LIMPT_APPROACHABLE_FAN; EXISTS_LIFT; LIFT_IN_IMAGE_LIFT;\r
2506               LIFT_EQ; DIST_LIFT]);;\r
2507 \r
2508 let CLOSED_LIFT_FAN = prove\r
2509  (`!s. closed_fan (IMAGE lift s) <=>\r
2510         !x. (!e. &0 < e ==> ?x'. x' IN s /\ ~(x' = x) /\ abs(x' - x) < e)\r
2511             ==> x IN s`,\r
2512   GEN_TAC THEN REWRITE_TAC[CLOSED_LIMPT_FAN; LIMPT_APPROACHABLE_FAN] THEN\r
2513   ONCE_REWRITE_TAC[FORALL_LIFT] THEN\r
2514   REWRITE_TAC[LIMPT_APPROACHABLE_LIFT_FAN; LIFT_EQ; DIST_LIFT;\r
2515               EXISTS_LIFT; LIFT_IN_IMAGE_LIFT]);;\r
2516 \r
2517 let CONTINUOUS_AT_LIFT_RANGE_FAN = prove\r
2518  (`!f x. (lift o f) continuous_fan (at_fan x) <=>\r
2519                 !e. &0 < e\r
2520                     ==> ?d. &0 < d /\\r
2521                             (!x'. norm(x' - x) < d\r
2522                                   ==> abs(f x' - f x) < e)`,\r
2523   REWRITE_TAC[continuous_at_fan; o_THM; DIST_LIFT] THEN REWRITE_TAC[dist]);;\r
2524 \r
2525 let CONTINUOUS_ON_LIFT_RANGE_FAN = prove\r
2526  (`!f s. (lift o f) continuous_on_fan s <=>\r
2527          !x. x IN s\r
2528              ==> !e. &0 < e\r
2529                      ==> ?d. &0 < d /\\r
2530                              (!x'. x' IN s /\ norm(x' - x) < d\r
2531                                    ==> abs(f x' - f x) < e)`,\r
2532   REWRITE_TAC[continuous_on_fan; o_THM; DIST_LIFT] THEN REWRITE_TAC[dist]);;\r
2533 \r
2534 let CONTINUOUS_AT_LIFT_NORM_FAN = prove\r
2535  (`!x. (lift o norm) continuous_fan (at_fan x)`,\r
2536   REWRITE_TAC[CONTINUOUS_AT_LIFT_RANGE_FAN; NORM_LIFT] THEN\r
2537   MESON_TAC[REAL_ABS_SUB_NORM; REAL_LET_TRANS]);;\r
2538 \r
2539 let CONTINUOUS_ON_LIFT_NORM_FAN = prove\r
2540  (`!s. (lift o norm) continuous_on_fan s`,\r
2541   REWRITE_TAC[CONTINUOUS_ON_LIFT_RANGE_FAN; NORM_LIFT] THEN\r
2542   MESON_TAC[REAL_ABS_SUB_NORM; REAL_LET_TRANS]);;\r
2543 \r
2544 let CONTINUOUS_AT_LIFT_COMPONENT_FAN = prove\r
2545  (`!i a. 1 <= i /\ i <= dimindex(:N)\r
2546          ==> (\x:real^N. lift(x$i)) continuous_fan (at_fan a)`,\r
2547   SIMP_TAC[continuous_at_fan; DIST_LIFT; GSYM VECTOR_SUB_COMPONENT] THEN\r
2548   MESON_TAC[dist; REAL_LET_TRANS; COMPONENT_LE_NORM]);;\r
2549 \r
2550 let CONTINUOUS_ON_LIFT_COMPONENT_FAN = prove\r
2551  (`!i s. 1 <= i /\ i <= dimindex(:N)\r
2552          ==> (\x:real^N. lift(x$i)) continuous_on_fan s`,\r
2553   SIMP_TAC[continuous_on_fan; DIST_LIFT; GSYM VECTOR_SUB_COMPONENT] THEN\r
2554   MESON_TAC[dist; REAL_LET_TRANS; COMPONENT_LE_NORM]);;\r
2555 \r
2556 (* ------------------------------------------------------------------------- *)\r
2557 (* Hence some handy theorems on distance, diameter etc. of/from a set.       *)\r
2558 (* ------------------------------------------------------------------------- *)\r
2559 \r
2560 let BOUNDED_HAS_SUP_FAN = prove\r
2561  (`!s. bounded_fan(IMAGE lift s) /\ ~(s = {})\r
2562        ==> (!x. x IN s ==> x <= sup s) /\\r
2563            (!b. (!x. x IN s ==> x <= b) ==> sup s <= b)`,\r
2564   REWRITE_TAC[BOUNDED_LIFT_FAN; IMAGE_EQ_EMPTY] THEN\r
2565   MESON_TAC[SUP; REAL_ARITH `abs(x) <= a ==> x <= a`]);;\r
2566 \r
2567 let BOUNDED_HAS_INF_FAN = prove\r
2568  (`!s. bounded_fan(IMAGE lift s) /\ ~(s = {})\r
2569        ==> (!x. x IN s ==> inf s <= x) /\\r
2570            (!b. (!x. x IN s ==> b <= x) ==> b <= inf s)`,\r
2571   REWRITE_TAC[BOUNDED_LIFT_FAN; IMAGE_EQ_EMPTY] THEN\r
2572   MESON_TAC[INF; REAL_ARITH `abs(x) <= a ==> --a <= x`]);;\r
2573 \r
2574 let COMPACT_ATTAINS_SUP_FAN = prove\r
2575  (`!s. compact_fan (IMAGE lift s) /\ ~(s = {})\r
2576        ==> ?x. x IN s /\ !y. y IN s ==> y <= x`,\r
2577   REWRITE_TAC[COMPACT_EQ_BOUNDED_CLOSED_FAN] THEN REPEAT STRIP_TAC THEN\r
2578   MP_TAC(SPEC `s:real->bool` BOUNDED_HAS_SUP_FAN) THEN ASM_REWRITE_TAC[] THEN\r
2579   STRIP_TAC THEN EXISTS_TAC `sup s` THEN ASM_REWRITE_TAC[] THEN\r
2580   ASM_MESON_TAC[CLOSED_LIFT_FAN; REAL_ARITH `s <= s - e <=> ~(&0 < e)`;\r
2581                 REAL_ARITH `x <= s /\ ~(x <= s - e) ==> abs(x - s) < e`]);;\r
2582 \r
2583 let COMPACT_ATTAINS_INF_FAN = prove\r
2584  (`!s. compact_fan (IMAGE lift s) /\ ~(s = {})\r
2585        ==> ?x. x IN s /\ !y. y IN s ==> x <= y`,\r
2586   REWRITE_TAC[COMPACT_EQ_BOUNDED_CLOSED_FAN] THEN REPEAT STRIP_TAC THEN\r
2587   MP_TAC(SPEC `s:real->bool` BOUNDED_HAS_INF_FAN) THEN ASM_REWRITE_TAC[] THEN\r
2588   STRIP_TAC THEN EXISTS_TAC `inf s` THEN ASM_REWRITE_TAC[] THEN\r
2589   ASM_MESON_TAC[CLOSED_LIFT_FAN; REAL_ARITH `s + e <= s <=> ~(&0 < e)`;\r
2590                 REAL_ARITH `s <= x /\ ~(s + e <= x) ==> abs(x - s) < e`]);;\r
2591 \r
2592 let CONTINUOUS_ATTAINS_SUP_FAN = prove\r
2593  (`!f:real^N->real s.\r
2594         compact_fan s /\ ~(s = {}) /\ (lift o f) continuous_on_fan s\r
2595         ==> ?x. x IN s /\ !y. y IN s ==> f(y) <= f(x)`,\r
2596   REPEAT STRIP_TAC THEN\r
2597   MP_TAC(SPEC `IMAGE (f:real^N->real) s` COMPACT_ATTAINS_SUP_FAN) THEN\r
2598   ASM_SIMP_TAC[GSYM IMAGE_o; COMPACT_CONTINUOUS_IMAGE_FAN; IMAGE_EQ_EMPTY] THEN\r
2599   MESON_TAC[IN_IMAGE]);;\r
2600 \r
2601 let CONTINUOUS_ATTAINS_INF_FAN = prove\r
2602  (`!f:real^N->real s.\r
2603         compact_fan s /\ ~(s = {}) /\ (lift o f) continuous_on_fan s\r
2604         ==> ?x. x IN s /\ !y. y IN s ==> f(x) <= f(y)`,\r
2605   REPEAT STRIP_TAC THEN\r
2606   MP_TAC(SPEC `IMAGE (f:real^N->real) s` COMPACT_ATTAINS_INF_FAN) THEN\r
2607   ASM_SIMP_TAC[GSYM IMAGE_o; COMPACT_CONTINUOUS_IMAGE_FAN; IMAGE_EQ_EMPTY] THEN\r
2608   MESON_TAC[IN_IMAGE]);;\r
2609 \r
2610 let DISTANCE_ATTAINS_SUP_FAN = prove\r
2611  (`!s a. compact_fan s /\ ~(s = {})\r
2612          ==> ?x. x IN s /\ !y. y IN s ==> dist(a,y) <= dist(a,x)`,\r
2613   REPEAT STRIP_TAC THEN MATCH_MP_TAC CONTINUOUS_ATTAINS_SUP_FAN THEN\r
2614   ASM_REWRITE_TAC[CONTINUOUS_ON_LIFT_RANGE_FAN] THEN REWRITE_TAC[dist] THEN\r
2615   ASM_MESON_TAC[REAL_LET_TRANS; REAL_ABS_SUB_NORM; NORM_NEG;\r
2616                 VECTOR_ARITH `(a - x) - (a - y) = --(x - y):real^N`]);;\r
2617 \r
2618 (* ------------------------------------------------------------------------- *)\r
2619 (* For *minimal* distance, we only need closure, not compactness.            *)\r
2620 (* ------------------------------------------------------------------------- *)\r
2621 \r
2622 let DISTANCE_ATTAINS_INF_FAN = prove\r
2623  (`!s a:real^N.\r
2624         closed_fan s /\ ~(s = {})\r
2625         ==> ?x. x IN s /\ !y. y IN s ==> dist(a,x) <= dist(a,y)`,\r
2626   REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN\r
2627   REWRITE_TAC[GSYM MEMBER_NOT_EMPTY] THEN\r
2628   DISCH_THEN(X_CHOOSE_TAC `b:real^N`) THEN\r
2629   MP_TAC(ISPECL [`\x:real^N. dist(a,x)`; `cball_fan(a:real^N,dist(b,a)) INTER s`]\r
2630                 CONTINUOUS_ATTAINS_INF_FAN) THEN\r
2631   ANTS_TAC THENL\r
2632    [ASM_SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED_FAN; CLOSED_INTER_FAN; BOUNDED_INTER_FAN;\r
2633                  BOUNDED_CBALL_FAN; CLOSED_CBALL_FAN; GSYM MEMBER_NOT_EMPTY] THEN\r
2634     REWRITE_TAC[dist; CONTINUOUS_ON_LIFT_RANGE_FAN; IN_INTER; IN_CBALL_FAN] THEN\r
2635     ASM_MESON_TAC[REAL_LET_TRANS; REAL_ABS_SUB_NORM; NORM_NEG; REAL_LE_REFL;\r
2636             NORM_SUB; VECTOR_ARITH `(a - x) - (a - y) = --(x - y):real^N`];\r
2637     MATCH_MP_TAC MONO_EXISTS THEN REWRITE_TAC[IN_INTER; IN_CBALL_FAN] THEN\r
2638     ASM_MESON_TAC[DIST_SYM; REAL_LE_TOTAL; REAL_LE_TRANS]]);;\r
2639 \r
2640 (* ------------------------------------------------------------------------- *)\r
2641 (* And so we have continuity of inverse.                                     *)\r
2642 (* ------------------------------------------------------------------------- *)\r
2643 \r
2644 let LIM_INV_FAN = prove\r
2645  (`!net_fan:(A)net_fan f l.\r
2646         ((lift o f) --> lift l) net_fan /\ ~(l = &0)\r
2647         ==> ((lift o inv o f) --> lift(inv l)) net_fan`,\r
2648   REPEAT GEN_TAC THEN REWRITE_TAC[lim_fan] THEN\r
2649   ASM_CASES_TAC `trivial_limit_fan(net_fan:(A)net_fan)` THEN ASM_REWRITE_TAC[] THEN\r
2650   REWRITE_TAC[o_THM; DIST_LIFT] THEN STRIP_TAC THEN\r
2651   X_GEN_TAC `e:real` THEN DISCH_TAC THEN\r
2652   FIRST_X_ASSUM(MP_TAC o SPEC `min (abs(l) / &2) ((l pow 2 * e) / &2)`) THEN\r
2653   REWRITE_TAC[REAL_LT_MIN] THEN ANTS_TAC THENL\r
2654    [ASM_SIMP_TAC[GSYM REAL_ABS_NZ; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN\r
2655     MATCH_MP_TAC REAL_LT_DIV THEN REWRITE_TAC[REAL_OF_NUM_LT; ARITH] THEN\r
2656     ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN\r
2657     ASM_SIMP_TAC[REAL_LT_MUL; GSYM REAL_ABS_NZ; REAL_POW_LT];\r
2658     ALL_TAC] THEN\r
2659   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `a:A` THEN\r
2660   MATCH_MP_TAC MONO_AND THEN REWRITE_TAC[] THEN\r
2661   MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `b:A` THEN\r
2662   MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[] THEN\r
2663   SIMP_TAC[REAL_LT_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN STRIP_TAC THEN\r
2664   FIRST_ASSUM(ASSUME_TAC o MATCH_MP (REAL_ARITH\r
2665    `abs(x - l) * &2 < abs l ==> ~(x = &0)`)) THEN\r
2666   ASM_SIMP_TAC[REAL_SUB_INV; REAL_ABS_DIV; REAL_LT_LDIV_EQ;\r
2667                GSYM REAL_ABS_NZ; REAL_ENTIRE] THEN\r
2668   FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH\r
2669    `abs(x - y) * &2 < b * c ==> c * b <= d * &2 ==> abs(y - x) < d`)) THEN\r
2670   ASM_SIMP_TAC[GSYM REAL_MUL_ASSOC; REAL_LE_LMUL_EQ] THEN\r
2671   ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN\r
2672   ASM_SIMP_TAC[REAL_ABS_MUL; REAL_POW_2; REAL_MUL_ASSOC; GSYM REAL_ABS_NZ;\r
2673                REAL_LE_RMUL_EQ] THEN\r
2674   ASM_SIMP_TAC[REAL_ARITH `abs(x - y) * &2 < abs y ==> abs y <= &2 * abs x`]);;\r
2675 \r
2676 let CONTINUOUS_INV_FAN = prove\r
2677  (`!net f. (lift o f) continuous_fan net_fan /\ ~(f(netlimit_fan net_fan) = &0)\r
2678            ==> (lift o inv o f) continuous_fan net_fan`,\r
2679   REWRITE_TAC[continuous_fan; LIM_INV_FAN; o_THM]);;\r
2680 \r
2681 let CONTINUOUS_AT_WITHIN_INV_FAN = prove\r
2682  (`!f s a:real^N.\r
2683         (lift o f) continuous_fan (at_fan a within_fan s) /\ ~(f a = &0)\r
2684         ==> (lift o inv o f) continuous_fan (at_fan a within_fan s)`,\r
2685   REPEAT GEN_TAC THEN\r
2686   ASM_CASES_TAC `trivial_limit_fan (at_fan (a:real^N) within_fan s)` THENL\r
2687    [ASM_REWRITE_TAC[continuous_fan; lim_fan];\r
2688     ASM_SIMP_TAC[NETLIMIT_WITHIN_FAN; CONTINUOUS_INV_FAN]]);;\r
2689 \r
2690 let CONTINUOUS_AT_INV_FAN = prove\r
2691  (`!f a. (lift o f) continuous_fan at_fan a /\ ~(f a = &0)\r
2692          ==> (lift o inv o f) continuous_fan at_fan a`,\r
2693   ONCE_REWRITE_TAC[GSYM WITHIN_UNIV_FAN] THEN\r
2694   REWRITE_TAC[CONTINUOUS_AT_WITHIN_INV_FAN]);;\r
2695 \r
2696 (* ------------------------------------------------------------------------- *)\r
2697 (* Preservation properties for pasted sets.                                  *)\r
2698 (* ------------------------------------------------------------------------- *)\r
2699 \r
2700 let BOUNDED_PASTECART_FAN = prove\r
2701  (`!s:real^M->bool t:real^N->bool.\r
2702      bounded_fan s /\ bounded_fan t ==> bounded_fan {pastecart x y | x IN s /\ y IN t}`,\r
2703   REPEAT GEN_TAC THEN REWRITE_TAC[bounded_fan; IN_ELIM_THM] THEN\r
2704   ASM_MESON_TAC[NORM_PASTECART; REAL_LE_ADD2; REAL_LE_TRANS]);;\r
2705 \r
2706 let CLOSED_PASTECART_FAN = prove\r
2707  (`!s:real^M->bool t:real^N->bool.\r
2708      closed_fan s /\ closed_fan t ==> closed_fan {pastecart x y | x IN s /\ y IN t}`,\r
2709   REPEAT GEN_TAC THEN REWRITE_TAC[CLOSED_SEQUENTIAL_LIMITS_FAN] THEN\r
2710   REWRITE_TAC[LIM_SEQUENTIALLY_FAN; IN_ELIM_THM; dist] THEN STRIP_TAC THEN\r
2711   MAP_EVERY X_GEN_TAC\r
2712    [`z:num->real^(M,N)finite_sum`; `l:real^(M,N)finite_sum`] THEN\r
2713   DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN\r
2714   REWRITE_TAC[SKOLEM_THM; LEFT_IMP_EXISTS_THM] THEN\r
2715   MAP_EVERY X_GEN_TAC [`x:num->real^M`; `y:num->real^N`] THEN\r
2716   REWRITE_TAC[FORALL_AND_THM] THEN STRIP_TAC THEN\r
2717   MAP_EVERY EXISTS_TAC\r
2718    [`fstcart(l:real^(M,N)finite_sum)`; `sndcart(l:real^(M,N)finite_sum)`] THEN\r
2719   REWRITE_TAC[PASTECART_FST_SND] THEN\r
2720   CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THENL\r
2721    [EXISTS_TAC `x:num->real^M`; EXISTS_TAC `y:num->real^N`] THEN\r
2722   ASM_REWRITE_TAC[] THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN\r
2723   FIRST_X_ASSUM(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN\r
2724   MATCH_MP_TAC MONO_EXISTS THEN ASM_REWRITE_TAC[] THEN\r
2725   GEN_TAC THEN MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN\r
2726   MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[] THEN\r
2727   MATCH_MP_TAC(REAL_ARITH `x <= y ==> y < a ==> x < a`) THEN\r
2728   MESON_TAC[NORM_FSTCART; FSTCART_SUB; FSTCART_PASTECART;\r
2729             NORM_SNDCART; SNDCART_SUB; SNDCART_PASTECART]);;\r
2730 \r
2731 let COMPACT_PASTECART_FAN = prove\r
2732  (`!s:real^M->bool t:real^N->bool.\r
2733      compact_fan s /\ compact_fan t ==> compact_fan {pastecart x y | x IN s /\ y IN t}`,\r
2734   SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED_FAN; BOUNDED_PASTECART_FAN; CLOSED_PASTECART_FAN]);;\r
2735 \r
2736 (* ------------------------------------------------------------------------- *)\r
2737 (* Hence some useful properties follow quite easily.                         *)\r
2738 (* ------------------------------------------------------------------------- *)\r
2739 \r
2740 let COMPACT_MULTIPLES_FAN = prove\r
2741  (`!s:real^N->bool c. compact_fan s ==> compact_fan (IMAGE (\x. c % x) s)`,\r
2742   REPEAT STRIP_TAC THEN\r
2743   MATCH_MP_TAC COMPACT_CONTINUOUS_IMAGE_FAN THEN ASM_REWRITE_TAC[] THEN\r
2744   MATCH_MP_TAC CONTINUOUS_AT_IMP_CONTINUOUS_ON_FAN THEN\r
2745   REPEAT STRIP_TAC THEN MATCH_MP_TAC LINEAR_CONTINUOUS_AT_FAN THEN\r
2746   REWRITE_TAC[linear] THEN CONJ_TAC THEN VECTOR_ARITH_TAC);;\r
2747 \r
2748 let COMPACT_NEGATIONS_FAN = prove\r
2749  (`!s:real^N->bool. compact_fan s ==> compact_fan (IMAGE (--) s)`,\r
2750   REPEAT STRIP_TAC THEN\r
2751   MATCH_MP_TAC COMPACT_CONTINUOUS_IMAGE_FAN THEN ASM_REWRITE_TAC[] THEN\r
2752   MATCH_MP_TAC CONTINUOUS_AT_IMP_CONTINUOUS_ON_FAN THEN\r
2753   REPEAT STRIP_TAC THEN MATCH_MP_TAC LINEAR_CONTINUOUS_AT_FAN THEN\r
2754   REWRITE_TAC[linear] THEN CONJ_TAC THEN VECTOR_ARITH_TAC);;\r
2755 \r
2756 let COMPACT_SUMS_FAN = prove\r
2757  (`!s:real^N->bool t.\r
2758         compact_fan s /\ compact_fan t ==> compact_fan {x + y | x IN s /\ y IN t}`,\r
2759   REPEAT STRIP_TAC THEN\r
2760   SUBGOAL_THEN `{x + y | x IN s /\ y IN t} =\r
2761                 IMAGE (\z. fstcart z + sndcart z :real^N)\r
2762                       {pastecart x y | x IN s /\ y IN t}`\r
2763   SUBST1_TAC THENL\r
2764    [REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_IMAGE] THEN\r
2765     GEN_TAC THEN EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN\r
2766     ASM_MESON_TAC[FSTCART_PASTECART; SNDCART_PASTECART; PASTECART_FST_SND];\r
2767     ALL_TAC] THEN\r
2768   MATCH_MP_TAC COMPACT_CONTINUOUS_IMAGE_FAN THEN\r
2769   ASM_SIMP_TAC[COMPACT_PASTECART_FAN] THEN\r
2770   MATCH_MP_TAC CONTINUOUS_AT_IMP_CONTINUOUS_ON_FAN THEN\r
2771   REPEAT STRIP_TAC THEN MATCH_MP_TAC LINEAR_CONTINUOUS_AT_FAN THEN\r
2772   REWRITE_TAC[linear; FSTCART_ADD; FSTCART_CMUL; SNDCART_ADD;\r
2773               SNDCART_CMUL] THEN\r
2774   CONJ_TAC THEN VECTOR_ARITH_TAC);;\r
2775 \r
2776 let COMPACT_DIFFERENCES_FAN = prove\r
2777  (`!s:real^N->bool t.\r
2778         compact_fan s /\ compact_fan t ==> compact_fan {x - y | x IN s /\ y IN t}`,\r
2779   REPEAT STRIP_TAC THEN\r
2780   SUBGOAL_THEN `{x - y | x:real^N IN s /\ y IN t} =\r
2781                 {x + y | x IN s /\ y IN (IMAGE (--) t)}`\r
2782     (fun th -> ASM_SIMP_TAC[th; COMPACT_SUMS_FAN; COMPACT_NEGATIONS_FAN]) THEN\r
2783   REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_IMAGE] THEN\r
2784   ONCE_REWRITE_TAC[VECTOR_ARITH `(x:real^N = --y) <=> (y = --x)`] THEN\r
2785   SIMP_TAC[VECTOR_SUB; GSYM CONJ_ASSOC; UNWIND_THM2] THEN\r
2786   MESON_TAC[VECTOR_NEG_NEG]);;\r
2787 \r
2788 let COMPACT_TRANSLATION_FAN = prove\r
2789  (`!s a:real^N. compact_fan s ==> compact_fan (IMAGE (\x. a + x) s)`,\r
2790   REPEAT STRIP_TAC THEN\r
2791   MP_TAC(ISPECL [`{a:real^N}`; `s:real^N->bool`] COMPACT_SUMS_FAN) THEN\r
2792   ASM_REWRITE_TAC[COMPACT_SING_FAN] THEN\r
2793   MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN\r
2794   REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_SING; IN_IMAGE] THEN MESON_TAC[]);;\r
2795 \r
2796 let COMPACT_AFFINITY_FAN = prove\r
2797  (`!s a:real^N c.\r
2798         compact_fan s ==> compact_fan (IMAGE (\x. a + c % x) s)`,\r
2799   REPEAT STRIP_TAC THEN\r
2800   SUBGOAL_THEN `(\x:real^N. a + c % x) = (\x. a + x) o (\x. c % x)`\r
2801   SUBST1_TAC THENL [REWRITE_TAC[o_DEF]; ALL_TAC] THEN\r
2802   ASM_SIMP_TAC[IMAGE_o; COMPACT_TRANSLATION_FAN; COMPACT_MULTIPLES_FAN]);;\r
2803 \r
2804 (* ------------------------------------------------------------------------- *)\r
2805 (* Hence we get the following.                                               *)\r
2806 (* ------------------------------------------------------------------------- *)\r
2807 \r
2808 let COMPACT_SUP_MAXDISTANCE_FAN = prove\r
2809  (`!s:real^N->bool.\r
2810         compact_fan s /\ ~(s = {})\r
2811         ==> ?x y. x IN s /\ y IN s /\\r
2812                   !u v. u IN s /\ v IN s ==> norm(u - v) <= norm(x - y)`,\r
2813   REPEAT STRIP_TAC THEN\r
2814   MP_TAC(ISPECL [`{x - y:real^N | x IN s /\ y IN s}`; `vec 0:real^N`]\r
2815                 DISTANCE_ATTAINS_SUP_FAN) THEN\r
2816   ANTS_TAC THENL\r
2817    [ASM_SIMP_TAC[COMPACT_DIFFERENCES_FAN] THEN\r
2818     REWRITE_TAC[EXTENSION; IN_ELIM_THM; NOT_IN_EMPTY] THEN\r
2819     ASM_MESON_TAC[MEMBER_NOT_EMPTY];\r
2820     REWRITE_TAC[IN_ELIM_THM; dist; VECTOR_SUB_RZERO; VECTOR_SUB_LZERO;\r
2821                 NORM_NEG] THEN\r
2822     MESON_TAC[]]);;\r
2823 \r
2824 (* ------------------------------------------------------------------------- *)\r
2825 (* We can state this in terms of diameter of a set.                          *)\r
2826 (* ------------------------------------------------------------------------- *)\r
2827 \r
2828 let diameter_fan = new_definition\r
2829   `diameter_fan s =\r
2830         if s = {} then &0\r
2831         else sup {norm(x - y) | x IN s /\ y IN s}`;;\r
2832 \r
2833 let DIAMETER_BOUNDED_FAN = prove\r
2834  (`!s. bounded_fan s\r
2835        ==> (!x:real^N y. x IN s /\ y IN s ==> norm(x - y) <= diameter_fan s) /\\r
2836            (!d. &0 <= d /\ d < diameter_fan s\r
2837                 ==> ?x y. x IN s /\ y IN s /\ norm(x - y) > d)`,\r
2838   GEN_TAC THEN DISCH_TAC THEN\r
2839   ASM_CASES_TAC `s:real^N->bool = {}` THEN\r
2840   ASM_REWRITE_TAC[diameter_fan; NOT_IN_EMPTY; REAL_LET_ANTISYM] THEN\r
2841   MP_TAC(SPEC `{norm(x - y:real^N) | x IN s /\ y IN s}` SUP) THEN\r
2842   ABBREV_TAC `b = sup {norm(x - y:real^N) | x IN s /\ y IN s}` THEN\r
2843   REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN\r
2844   REWRITE_TAC[NOT_IN_EMPTY; real_gt] THEN ANTS_TAC THENL\r
2845    [CONJ_TAC THENL [ASM_MESON_TAC[MEMBER_NOT_EMPTY]; ALL_TAC];\r
2846     MESON_TAC[REAL_NOT_LE]] THEN\r
2847   SIMP_TAC[VECTOR_SUB; LEFT_IMP_EXISTS_THM] THEN\r
2848   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [bounded_fan]) THEN\r
2849   MESON_TAC[REAL_ARITH `x <= y + z /\ y <= b /\ z<= b ==> x <= b + b`;\r
2850             NORM_TRIANGLE; NORM_NEG]);;\r
2851 \r
2852 let DIAMETER_BOUNDED_BOUND_FAN = prove\r
2853  (`!s x y. bounded_fan s /\ x IN s /\ y IN s ==> norm(x - y) <= diameter_fan s`,\r
2854   MESON_TAC[DIAMETER_BOUNDED_FAN]);;\r
2855 \r
2856 let DIAMETER_COMPACT_ATTAINED_FAN = prove\r
2857  (`!s:real^N->bool.\r
2858         compact_fan s /\ ~(s = {})\r
2859         ==> ?x y. x IN s /\ y IN s /\ (norm(x - y) = diameter_fan s)`,\r
2860   GEN_TAC THEN DISCH_TAC THEN\r
2861   FIRST_ASSUM(MP_TAC o MATCH_MP COMPACT_SUP_MAXDISTANCE_FAN) THEN\r
2862   REPEAT(MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC) THEN\r
2863   STRIP_TAC THEN ASM_REWRITE_TAC[] THEN\r
2864   MP_TAC(SPEC `s:real^N->bool` DIAMETER_BOUNDED_FAN) THEN\r
2865   RULE_ASSUM_TAC(REWRITE_RULE[COMPACT_EQ_BOUNDED_CLOSED_FAN]) THEN\r
2866   ASM_REWRITE_TAC[real_gt] THEN STRIP_TAC THEN\r
2867   REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN\r
2868   ASM_MESON_TAC[NORM_POS_LE; REAL_NOT_LT]);;\r
2869 \r
2870 (* ------------------------------------------------------------------------- *)\r
2871 (* Related results with closure as the conclusion.                           *)\r
2872 (* ------------------------------------------------------------------------- *)\r
2873 \r
2874 let CLOSED_MULTIPLES_FAN = prove\r
2875  (`!s:real^N->bool c. closed_fan s ==> closed_fan (IMAGE (\x. c % x) s)`,\r
2876   REPEAT GEN_TAC THEN\r
2877   ASM_CASES_TAC `s :real^N->bool = {}` THEN\r
2878   ASM_REWRITE_TAC[CLOSED_EMPTY_FAN; IMAGE_CLAUSES] THEN\r
2879   ASM_CASES_TAC `c = &0` THENL\r
2880    [SUBGOAL_THEN `IMAGE (\x:real^N. c % x) s = {(vec 0)}`\r
2881      (fun th -> REWRITE_TAC[th; CLOSED_SING_FAN]) THEN\r
2882     ASM_REWRITE_TAC[EXTENSION; IN_IMAGE; IN_SING; VECTOR_MUL_LZERO] THEN\r
2883     ASM_MESON_TAC[MEMBER_NOT_EMPTY];\r
2884     ALL_TAC] THEN\r
2885   REWRITE_TAC[CLOSED_SEQUENTIAL_LIMITS_FAN; IN_IMAGE; SKOLEM_THM] THEN\r
2886   STRIP_TAC THEN X_GEN_TAC `x:num->real^N` THEN X_GEN_TAC `l:real^N` THEN\r
2887   DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN\r
2888   DISCH_THEN(X_CHOOSE_THEN `y:num->real^N` MP_TAC) THEN\r
2889   REWRITE_TAC[FORALL_AND_THM] THEN STRIP_TAC THEN\r
2890   EXISTS_TAC `inv(c) % l :real^N` THEN\r
2891   ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_RINV; VECTOR_MUL_LID] THEN\r
2892   FIRST_X_ASSUM MATCH_MP_TAC THEN EXISTS_TAC `\n:num. inv(c) % x n:real^N` THEN\r
2893   ASM_REWRITE_TAC[] THEN CONJ_TAC THENL\r
2894    [ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID];\r
2895     MATCH_MP_TAC LIM_CMUL_FAN THEN\r
2896     FIRST_ASSUM(fun th -> REWRITE_TAC[SYM(SPEC_ALL th)]) THEN\r
2897     ASM_REWRITE_TAC[ETA_AX]]);;\r
2898 \r
2899 let CLOSED_NEGATIONS_FAN = prove\r
2900  (`!s:real^N->bool. closed_fan s ==> closed_fan (IMAGE (--) s)`,\r
2901   REPEAT GEN_TAC THEN\r
2902   SUBGOAL_THEN `IMAGE (--) s = IMAGE (\x:real^N. --(&1) % x) s`\r
2903   SUBST1_TAC THEN SIMP_TAC[CLOSED_MULTIPLES_FAN] THEN\r
2904   REWRITE_TAC[VECTOR_ARITH `--(&1) % x = --x`] THEN REWRITE_TAC[ETA_AX]);;\r
2905 \r
2906 (* ------------------------------------------------------------------------- *)\r
2907 (* A cute way of denoting open and closed intervals using overloading.       *)\r
2908 (* ------------------------------------------------------------------------- *)\r
2909 \r
2910 let open_interval_fan = new_definition\r
2911   `open_interval_fan(a:real^N,b:real^N) =\r
2912         {x:real^N | !i. 1 <= i /\ i <= dimindex(:N)\r
2913                         ==> a$i < x$i /\ x$i < b$i}`;;\r
2914 \r
2915 let closed_interval_fan = new_definition\r
2916   `closed_interval_fan(l:(real^N#real^N)list) =\r
2917          {x:real^N | !i. 1 <= i /\ i <= dimindex(:N)\r
2918                          ==> FST(HD l)$i <= x$i /\ x$i <= SND(HD l)$i}`;;\r
2919 \r
2920 make_overloadable "interval_fan" `:A`;;\r
2921 \r
2922 overload_interface("interval_fan",`open_interval_fan`);;\r
2923 overload_interface("interval_fan",`closed_interval_fan`);;\r
2924 \r
2925 let interval_fan = prove\r
2926  (`(interval_fan (a,b) = {x:real^N | !i. 1 <= i /\ i <= dimindex(:N)\r
2927                                      ==> a$i < x$i /\ x$i < b$i}) /\\r
2928    (interval_fan [a,b] = {x:real^N | !i. 1 <= i /\ i <= dimindex(:N)\r
2929                                      ==> a$i <= x$i /\ x$i <= b$i})`,\r
2930   REWRITE_TAC[open_interval_fan; closed_interval_fan; HD; FST; SND]);;\r
2931 \r
2932 let IN_INTERVAL_FAN = prove\r
2933  (`(!x:real^N.\r
2934         x IN interval_fan (a,b) <=>\r
2935                 !i. 1 <= i /\ i <= dimindex(:N)\r
2936                     ==> a$i < x$i /\ x$i < b$i) /\\r
2937    (!x:real^N.\r
2938         x IN interval_fan [a,b] <=>\r
2939                 !i. 1 <= i /\ i <= dimindex(:N)\r
2940                     ==> a$i <= x$i /\ x$i <= b$i)`,\r
2941   REWRITE_TAC[interval_fan; IN_ELIM_THM]);;\r
2942 \r
2943 \r
2944 (* ------------------------------------------------------------------------- *)\r
2945 (* Some stuff for half-infinite intervals too; maybe I need a notation?      *)\r
2946 (* ------------------------------------------------------------------------- *)\r
2947 \r
2948 let CLOSED_INTERVAL_LEFT_FAN = prove\r
2949  (`!b:real^N.\r
2950      closed_fan\r
2951         {x:real^N | !i. 1 <= i /\ i <= dimindex(:N) ==> x$i <= b$i}`,\r
2952   REWRITE_TAC[CLOSED_LIMPT_FAN; LIMPT_APPROACHABLE_FAN; IN_ELIM_THM] THEN\r
2953   REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM REAL_NOT_LT] THEN DISCH_TAC THEN\r
2954   FIRST_X_ASSUM(MP_TAC o SPEC `(x:real^N)$i - (b:real^N)$i`) THEN\r
2955   ASM_REWRITE_TAC[REAL_SUB_LT] THEN\r
2956   DISCH_THEN(X_CHOOSE_THEN `z:real^N` MP_TAC) THEN\r
2957   REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN\r
2958   REWRITE_TAC[dist; REAL_NOT_LT] THEN\r
2959   MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `abs((z - x :real^N)$i)` THEN\r
2960   ASM_SIMP_TAC[COMPONENT_LE_NORM] THEN\r
2961   ASM_SIMP_TAC[VECTOR_SUB_COMPONENT] THEN\r
2962   ASM_SIMP_TAC[REAL_ARITH `z <= b /\ b < x ==> x - b <= abs(z - x)`]);;\r
2963 \r
2964 let CLOSED_INTERVAL_RIGHT_FAN = prove\r
2965  (`!a:real^N.\r
2966      closed_fan\r
2967         {x:real^N | !i. 1 <= i /\ i <= dimindex(:N) ==> a$i <= x$i}`,\r
2968   REWRITE_TAC[CLOSED_LIMPT_FAN; LIMPT_APPROACHABLE_FAN; IN_ELIM_THM] THEN\r
2969   REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM REAL_NOT_LT] THEN DISCH_TAC THEN\r
2970   FIRST_X_ASSUM(MP_TAC o SPEC `(a:real^N)$i - (x:real^N)$i`) THEN\r
2971   ASM_REWRITE_TAC[REAL_SUB_LT] THEN\r
2972   DISCH_THEN(X_CHOOSE_THEN `z:real^N` MP_TAC) THEN\r
2973   REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN\r
2974   REWRITE_TAC[dist; REAL_NOT_LT] THEN\r
2975   MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `abs((z - x :real^N)$i)` THEN\r
2976   ASM_SIMP_TAC[COMPONENT_LE_NORM] THEN\r
2977   ASM_SIMP_TAC[VECTOR_SUB_COMPONENT] THEN\r
2978   ASM_SIMP_TAC[REAL_ARITH `x < a /\ a <= z ==> a - x <= abs(z - x)`]);;\r
2979 \r
2980 (* ------------------------------------------------------------------------- *)\r
2981 (* Closure of halfspaces and hyperplanes.                                    *)\r
2982 (* ------------------------------------------------------------------------- *)\r
2983 \r
2984 let LIM_LIFT_DOT_FAN = prove\r
2985  (`!f:real^M->real^N a.\r
2986         (f --> l) net_fan ==> ((lift o (\y. a dot f(y))) --> lift(a dot l)) net_fan`,\r
2987   REPEAT GEN_TAC THEN ASM_CASES_TAC `a = vec 0:real^N` THENL\r
2988    [ASM_REWRITE_TAC[DOT_LZERO; LIFT_NUM; o_DEF; LIM_CONST_FAN]; ALL_TAC] THEN\r
2989   REWRITE_TAC[lim_fan] THEN MATCH_MP_TAC MONO_OR THEN REWRITE_TAC[] THEN\r
2990   DISCH_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN\r
2991   FIRST_X_ASSUM(MP_TAC o SPEC `e / norm(a:real^N)`) THEN\r
2992   ASM_SIMP_TAC[REAL_LT_DIV; NORM_POS_LT; REAL_LT_RDIV_EQ] THEN\r
2993   REWRITE_TAC[dist; o_THM; GSYM LIFT_SUB; GSYM DOT_RSUB; NORM_LIFT] THEN\r
2994   ONCE_REWRITE_TAC[DOT_SYM] THEN\r
2995   MESON_TAC[NORM_CAUCHY_SCHWARZ_ABS; REAL_MUL_SYM; REAL_LET_TRANS]);;\r
2996 \r
2997 let CONTINUOUS_AT_LIFT_DOT_FAN = prove\r
2998  (`!a:real^N x. (lift o (\y. a dot y)) continuous_fan at_fan x`,\r
2999   REPEAT GEN_TAC THEN REWRITE_TAC[CONTINUOUS_AT_FAN; o_THM] THEN\r
3000   MATCH_MP_TAC LIM_LIFT_DOT_FAN THEN REWRITE_TAC[LIM_AT_FAN] THEN MESON_TAC[]);;\r
3001 \r
3002 let CONTINUOUS_ON_LIFT_DOT_FAN = prove\r
3003  (`!s x. (lift o (\y. a dot y)) continuous_on_fan s`,\r
3004   SIMP_TAC[CONTINUOUS_AT_IMP_CONTINUOUS_ON_FAN; CONTINUOUS_AT_LIFT_DOT_FAN]);;\r
3005 \r
3006 let CLOSED_HALFSPACE_LE_FAN = prove\r
3007  (`!a:real^N b. closed_fan {x | a dot x <= b}`,\r
3008   REPEAT GEN_TAC THEN\r
3009   MP_TAC(ISPECL [`(:real^N)`; `a:real^N`] CONTINUOUS_ON_LIFT_DOT_FAN) THEN\r
3010   REWRITE_TAC[CONTINUOUS_ON_CLOSED_FAN; GSYM CLOSED_IN_FAN] THEN\r
3011   DISCH_THEN(MP_TAC o SPEC\r
3012    `IMAGE lift {r | ?x:real^N. (a dot x = r) /\ r <= b}`) THEN\r
3013   ANTS_TAC THENL\r
3014    [ALL_TAC;\r
3015     MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN\r
3016     REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_IMAGE; IN_UNIV] THEN\r
3017     REWRITE_TAC[o_DEF] THEN MESON_TAC[LIFT_DROP]] THEN\r
3018   REWRITE_TAC[CLOSED_IN_CLOSED_FAN] THEN\r
3019   EXISTS_TAC `{x | !i. 1 <= i /\ i <= dimindex(:1)\r
3020                        ==> (x:real^1)$i <= (lift b)$i}` THEN\r
3021   REWRITE_TAC[CLOSED_INTERVAL_LEFT_FAN] THEN\r
3022   SIMP_TAC[EXTENSION; IN_IMAGE; IN_UNIV; IN_ELIM_THM; IN_INTER; IN_INTERVAL_FAN;\r
3023     VEC_COMPONENT; DIMINDEX_1; LAMBDA_BETA; o_THM] THEN\r
3024   SIMP_TAC[ARITH_RULE `1 <= i /\ i <= 1 <=> (i = 1)`] THEN\r
3025   REWRITE_TAC[GSYM drop; LEFT_FORALL_IMP_THM; EXISTS_REFL] THEN\r
3026   MESON_TAC[LIFT_DROP]);;\r
3027 \r
3028 let CLOSED_HALFSPACE_GE_FAN = prove\r
3029  (`!a:real^N b. closed_fan {x | a dot x >= b}`,\r
3030   REWRITE_TAC[REAL_ARITH `a >= b <=> --a <= --b`] THEN\r
3031   REWRITE_TAC[GSYM DOT_LNEG; CLOSED_HALFSPACE_LE_FAN]);;\r
3032 \r
3033 let CLOSED_HYPERPLANE_FAN = prove\r
3034  (`!a b. closed_fan {x | a dot x = b}`,\r
3035   REPEAT GEN_TAC THEN REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN\r
3036   REWRITE_TAC[REAL_ARITH `b <= a dot x <=> a dot x >= b`] THEN\r
3037   REWRITE_TAC[SET_RULE `{x | P x /\ Q x} = {x | P x} INTER {x | Q x}`] THEN\r
3038   SIMP_TAC[CLOSED_INTER_FAN; CLOSED_HALFSPACE_LE_FAN; CLOSED_HALFSPACE_GE_FAN]);;\r
3039 \r
3040 \r
3041 \r
3042 \r