colo12-c703.uibk.ac.at Git - Multivariate Analysis/.git/blob - Multivariate/misc.ml

   1 (* ========================================================================= *)
   2 (* Various convenient background stuff.                                      *)
   3 (*                                                                           *)
   4 (*              (c) Copyright, John Harrison 1998-2008                       *)
   5 (* ========================================================================= *)
   6
   7 prioritize_real();;
   8
   9 (* ------------------------------------------------------------------------- *)
  10 (* A couple of extra tactics used in some proofs below.                      *)
  11 (* ------------------------------------------------------------------------- *)
  12
  13 let ASSERT_TAC tm =
  14   SUBGOAL_THEN tm STRIP_ASSUME_TAC;;
  15
  16 let EQ_TRANS_TAC tm =
  17   MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC tm THEN CONJ_TAC;;
  18
  19 (* ------------------------------------------------------------------------- *)
  20 (* Miscellaneous lemmas.                                                     *)
  21 (* ------------------------------------------------------------------------- *)
  22
  23 let EXISTS_DIFF = prove
  24  (`(?s:A->bool. P(UNIV DIFF s)) <=> (?s. P s)`,
  25   MESON_TAC[prove(`UNIV DIFF (UNIV DIFF s) = s`,SET_TAC[])]);;
  26
  27 let GE_REFL = prove
  28  (`!n:num. n >= n`,
  29   REWRITE_TAC[GE; LE_REFL]);;
  30
  31 let FORALL_SUC = prove
  32  (`(!n. ~(n = 0) ==> P n) <=> (!n. P(SUC n))`,
  33   MESON_TAC[num_CASES; NOT_SUC]);;
  34
  35 let SEQ_MONO_LEMMA = prove
  36  (`!d e. (!n. n >= m ==> d(n) < e(n)) /\ (!n. n >= m ==> e(n) <= e(m))
  37          ==> !n:num. n >= m ==> d(n) < e(m)`,
  38   MESON_TAC[GE; REAL_LTE_TRANS]);;
  39
  40 let REAL_HALF = prove
  41  (`(!e. &0 < e / &2 <=> &0 < e) /\
  42    (!e. e / &2 + e / &2 = e) /\
  43    (!e. &2 * (e / &2) = e)`,
  44   REAL_ARITH_TAC);;
  45
  46 let UPPER_BOUND_FINITE_SET = prove
  47  (`!f:(A->num) s. FINITE(s) ==> ?a. !x. x IN s ==> f(x) <= a`,
  48   GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
  49   REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
  50   MESON_TAC[LE_CASES; LE_REFL; LE_TRANS]);;
  51
  52 let UPPER_BOUND_FINITE_SET_REAL = prove
  53  (`!f:(A->real) s. FINITE(s) ==> ?a. !x. x IN s ==> f(x) <= a`,
  54   GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
  55   REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
  56   MESON_TAC[REAL_LE_TOTAL; REAL_LE_REFL; REAL_LE_TRANS]);;
  57
  58 let LOWER_BOUND_FINITE_SET = prove
  59  (`!f:(A->num) s. FINITE(s) ==> ?a. !x. x IN s ==> a <= f(x)`,
  60   GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
  61   REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
  62   MESON_TAC[LE_CASES; LE_REFL; LE_TRANS]);;
  63
  64 let LOWER_BOUND_FINITE_SET_REAL = prove
  65  (`!f:(A->real) s. FINITE(s) ==> ?a. !x. x IN s ==> a <= f(x)`,
  66   GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
  67   REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
  68   MESON_TAC[REAL_LE_TOTAL; REAL_LE_REFL; REAL_LE_TRANS]);;
  69
  70 let REAL_CONVEX_BOUND2_LT = prove
  71  (`!x y a u v. x < a /\ y < b /\ &0 <= u /\ &0 <= v /\ u + v = &1
  72                ==> u * x + v * y < u * a + v * b`,
  73   REPEAT GEN_TAC THEN ASM_CASES_TAC `u = &0` THENL
  74    [ASM_REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_LID] THEN REPEAT STRIP_TAC;
  75     REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LTE_ADD2 THEN
  76     ASM_SIMP_TAC[REAL_LE_LMUL; REAL_LT_IMP_LE]] THEN
  77   MATCH_MP_TAC REAL_LT_LMUL THEN ASM_REAL_ARITH_TAC);;
  78
  79 let REAL_CONVEX_BOUND_LT = prove
  80  (`!x y a u v. x < a /\ y < a /\ &0 <= u /\ &0 <= v /\ (u + v = &1)
  81                ==> u * x + v * y < a`,
  82   REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LTE_TRANS THEN
  83   EXISTS_TAC `u * a + v * a:real` THEN CONJ_TAC THENL
  84    [ASM_SIMP_TAC[REAL_CONVEX_BOUND2_LT];
  85     MATCH_MP_TAC REAL_EQ_IMP_LE THEN
  86     UNDISCH_TAC `u + v = &1` THEN CONV_TAC REAL_RING]);;
  87
  88 let REAL_CONVEX_BOUND_LE = prove
  89  (`!x y a u v. x <= a /\ y <= a /\ &0 <= u /\ &0 <= v /\ (u + v = &1)
  90                ==> u * x + v * y <= a`,
  91   REPEAT STRIP_TAC THEN
  92   MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `(u + v) * a` THEN
  93   CONJ_TAC THENL [ALL_TAC; ASM_REWRITE_TAC[REAL_LE_REFL; REAL_MUL_LID]] THEN
  94   ASM_SIMP_TAC[REAL_ADD_RDISTRIB; REAL_LE_ADD2; REAL_LE_LMUL]);;
  95
  96 let INFINITE_ENUMERATE = prove
  97  (`!s:num->bool.
  98        INFINITE s
  99        ==> ?r:num->num. (!m n. m < n ==> r(m) < r(n)) /\ (!n. r n IN s)`,
 100   GEN_TAC THEN REWRITE_TAC[INFINITE; num_FINITE; NOT_EXISTS_THM] THEN
 101   REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; NOT_LE; SKOLEM_THM] THEN
 102   DISCH_THEN(X_CHOOSE_TAC `next:num->num`) THEN
 103   (MP_TAC o prove_recursive_functions_exist num_RECURSION)
 104    `(f(0) = next 0) /\ (!n. f(SUC n) = next(f n))` THEN
 105   MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN STRIP_TAC THEN CONJ_TAC THENL
 106    [GEN_TAC; ALL_TAC] THEN
 107   INDUCT_TAC THEN ASM_REWRITE_TAC[LT] THEN ASM_MESON_TAC[LT_TRANS]);;
 108
 109 let APPROACHABLE_LT_LE = prove
 110  (`!P f. (?d. &0 < d /\ !x. f(x) < d ==> P x) =
 111          (?d. &0 < d /\ !x. f(x) <= d ==> P x)`,
 112   let lemma = prove
 113    (`&0 < d ==> x <= d / &2 ==> x < d`,
 114     SIMP_TAC[REAL_LE_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN REAL_ARITH_TAC) in
 115   MESON_TAC[REAL_LT_IMP_LE; lemma; REAL_HALF]);;
 116
 117 let REAL_LE_BETWEEN = prove
 118  (`!a b. a <= b <=> ?x. a <= x /\ x <= b`,
 119   MESON_TAC[REAL_LE_TRANS; REAL_LE_REFL]);;
 120
 121 let REAL_LT_BETWEEN = prove
 122  (`!a b. a < b <=> ?x. a < x /\ x < b`,
 123   REPEAT GEN_TAC THEN EQ_TAC THENL [ALL_TAC; MESON_TAC[REAL_LT_TRANS]] THEN
 124   DISCH_TAC THEN EXISTS_TAC `(a + b) / &2` THEN
 125   SIMP_TAC[REAL_LT_RDIV_EQ; REAL_LT_LDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
 126   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
 127
 128 let TRIANGLE_LEMMA = prove
 129  (`!x y z. &0 <= x /\ &0 <= y /\ &0 <= z /\ x pow 2 <= y pow 2 + z pow 2
 130            ==> x <= y + z`,
 131   REPEAT GEN_TAC THEN
 132   REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
 133   ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
 134   REWRITE_TAC[REAL_NOT_LE] THEN DISCH_TAC THEN
 135   MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `(y + z) pow 2` THEN
 136   ASM_SIMP_TAC[REAL_POW_LT2; REAL_LE_ADD; ARITH_EQ] THEN
 137   ASM_SIMP_TAC[REAL_LE_MUL; REAL_POW_2; REAL_ARITH
 138    `x * x + y * y <= (x + y) * (x + y) <=> &0 <= x * y`]);;
 139
 140 let LAMBDA_SKOLEM = prove
 141  (`(!i. 1 <= i /\ i <= dimindex(:N) ==> ?x. P i x) =
 142    (?x:A^N. !i. 1 <= i /\ i <= dimindex(:N) ==> P i (x$i))`,
 143   REWRITE_TAC[RIGHT_IMP_EXISTS_THM; SKOLEM_THM] THEN EQ_TAC THENL
 144    [DISCH_THEN(X_CHOOSE_TAC `x:num->A`) THEN
 145     EXISTS_TAC `(lambda i. x i):A^N` THEN ASM_SIMP_TAC[LAMBDA_BETA];
 146     DISCH_THEN(X_CHOOSE_TAC `x:A^N`) THEN
 147     EXISTS_TAC `\i. (x:A^N)$i` THEN ASM_REWRITE_TAC[]]);;
 148
 149 let LAMBDA_PAIR = prove
 150  (`(\(x,y). P x y) = (\p. P (FST p) (SND p))`,
 151   REWRITE_TAC[FUN_EQ_THM; FORALL_PAIR_THM] THEN
 152   CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN REWRITE_TAC[]);;
 153
 154 let EPSILON_DELTA_MINIMAL = prove
 155  (`!P:real->A->bool Q.
 156         FINITE {x | Q x} /\
 157         (!d e x. Q x /\ &0 < e /\ e < d ==> P d x ==> P e x) /\
 158         (!x. Q x ==> ?d. &0 < d /\ P d x)
 159         ==> ?d. &0 < d /\ !x. Q x ==> P d x`,
 160   REWRITE_TAC[IMP_IMP] THEN REPEAT STRIP_TAC THEN
 161   ASM_CASES_TAC `{x:A | Q x} = {}` THENL
 162    [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [EXTENSION]) THEN
 163     REWRITE_TAC[NOT_IN_EMPTY; IN_ELIM_THM] THEN
 164     DISCH_TAC THEN EXISTS_TAC `&1` THEN ASM_REWRITE_TAC[REAL_LT_01];
 165     FIRST_X_ASSUM(MP_TAC o
 166      GEN_REWRITE_RULE BINDER_CONV [RIGHT_IMP_EXISTS_THM]) THEN
 167     REWRITE_TAC[SKOLEM_THM; LEFT_IMP_EXISTS_THM] THEN
 168     X_GEN_TAC `d:A->real` THEN DISCH_TAC THEN
 169     EXISTS_TAC `inf(IMAGE d {x:A | Q x})` THEN
 170     ASM_SIMP_TAC[REAL_LT_INF_FINITE; FINITE_IMAGE; IMAGE_EQ_EMPTY] THEN
 171     ASM_SIMP_TAC[FORALL_IN_IMAGE; FORALL_IN_GSPEC] THEN
 172     X_GEN_TAC `a:A` THEN DISCH_TAC THEN
 173     SUBGOAL_THEN
 174      `&0 < inf(IMAGE d {x:A | Q x}) /\ inf(IMAGE d {x | Q x}) <= d a`
 175     MP_TAC THENL
 176      [ASM_SIMP_TAC[REAL_LT_INF_FINITE; REAL_INF_LE_FINITE;
 177                    FINITE_IMAGE; IMAGE_EQ_EMPTY] THEN
 178       REWRITE_TAC[EXISTS_IN_IMAGE; FORALL_IN_IMAGE; IN_ELIM_THM] THEN
 179       ASM_MESON_TAC[REAL_LE_REFL];
 180       REWRITE_TAC[REAL_LE_LT] THEN STRIP_TAC THEN ASM_SIMP_TAC[] THEN
 181       FIRST_X_ASSUM MATCH_MP_TAC THEN
 182       EXISTS_TAC `(d:A->real) a` THEN ASM_SIMP_TAC[]]]);;
 183
 184 (* ------------------------------------------------------------------------- *)
 185 (* A generic notion of "hull" (convex, affine, conic hull and closure).      *)
 186 (* ------------------------------------------------------------------------- *)
 187
 188 parse_as_infix("hull",(21,"left"));;
 189
 190 let hull = new_definition
 191   `P hull s = INTERS {t | P t /\ s SUBSET t}`;;
 192
 193 let HULL_P = prove
 194  (`!P s. P s ==> (P hull s = s)`,
 195   REWRITE_TAC[hull; EXTENSION; IN_INTERS; IN_ELIM_THM] THEN
 196   MESON_TAC[SUBSET]);;
 197
 198 let P_HULL = prove
 199  (`!P s. (!f. (!s. s IN f ==> P s) ==> P(INTERS f)) ==> P(P hull s)`,
 200   REWRITE_TAC[hull] THEN SIMP_TAC[IN_ELIM_THM]);;
 201
 202 let HULL_EQ = prove
 203  (`!P s. (!f. (!s. s IN f ==> P s) ==> P(INTERS f))
 204          ==> ((P hull s = s) <=> P s)`,
 205   MESON_TAC[P_HULL; HULL_P]);;
 206
 207 let HULL_HULL = prove
 208  (`!P s. P hull (P hull s) = P hull s`,
 209   REWRITE_TAC[hull; EXTENSION; IN_INTERS; IN_ELIM_THM; SUBSET] THEN
 210   MESON_TAC[]);;
 211
 212 let HULL_SUBSET = prove
 213  (`!P s. s SUBSET (P hull s)`,
 214   REWRITE_TAC[hull; SUBSET; IN_INTERS; IN_ELIM_THM] THEN MESON_TAC[]);;
 215
 216 let HULL_MONO = prove
 217  (`!P s t. s SUBSET t ==> (P hull s) SUBSET (P hull t)`,
 218    REWRITE_TAC[hull; SUBSET; IN_INTERS; IN_ELIM_THM] THEN MESON_TAC[]);;
 219
 220 let HULL_ANTIMONO = prove
 221  (`!P Q s. P SUBSET Q ==> (Q hull s) SUBSET (P hull s)`,
 222   REWRITE_TAC[SUBSET; hull; IN_INTERS; IN_ELIM_THM] THEN MESON_TAC[IN]);;
 223
 224 let HULL_MINIMAL = prove
 225  (`!P s t. s SUBSET t /\ P t ==> (P hull s) SUBSET t`,
 226   REWRITE_TAC[hull; SUBSET; IN_INTERS; IN_ELIM_THM] THEN MESON_TAC[]);;
 227
 228 let SUBSET_HULL = prove
 229  (`!P s t. P t ==> ((P hull s) SUBSET t <=> s SUBSET t)`,
 230   REWRITE_TAC[hull; SUBSET; IN_INTERS; IN_ELIM_THM] THEN MESON_TAC[]);;
 231
 232 let HULL_UNIQUE = prove
 233  (`!P s t. s SUBSET t /\ P t /\ (!t'. s SUBSET t' /\ P t' ==> t SUBSET t')
 234            ==> (P hull s = t)`,
 235   REPEAT STRIP_TAC THEN MATCH_MP_TAC SUBSET_ANTISYM THEN
 236   REWRITE_TAC[hull; SUBSET; IN_INTERS; IN_ELIM_THM] THEN
 237   ASM_MESON_TAC[SUBSET_HULL; SUBSET]);;
 238
 239 let HULL_UNION_SUBSET = prove
 240  (`!P s t. (P hull s) UNION (P hull t) SUBSET (P hull (s UNION t))`,
 241   SIMP_TAC[UNION_SUBSET; HULL_MONO; SUBSET_UNION]);;
 242
 243 let HULL_UNION = prove
 244  (`!P s t. P hull (s UNION t) = P hull (P hull s UNION P hull t)`,
 245   REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[hull] THEN
 246   AP_TERM_TAC THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM; UNION_SUBSET] THEN
 247   MESON_TAC[SUBSET_HULL]);;
 248
 249 let HULL_UNION_LEFT = prove
 250  (`!P s t:A->bool.
 251         P hull (s UNION t) = P hull (P hull s UNION t)`,
 252   REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[hull] THEN
 253   AP_TERM_TAC THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM; UNION_SUBSET] THEN
 254   MESON_TAC[SUBSET_HULL]);;
 255
 256 let HULL_UNION_RIGHT = prove
 257  (`!P s t:A->bool.
 258         P hull (s UNION t) = P hull (s UNION P hull t)`,
 259   REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[hull] THEN
 260   AP_TERM_TAC THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM; UNION_SUBSET] THEN
 261   MESON_TAC[SUBSET_HULL]);;
 262
 263 let HULL_REDUNDANT_EQ = prove
 264  (`!P a s. a IN (P hull s) <=> (P hull (a INSERT s) = P hull s)`,
 265   REWRITE_TAC[hull] THEN SET_TAC[]);;
 266
 267 let HULL_REDUNDANT = prove
 268  (`!P a s. a IN (P hull s) ==> (P hull (a INSERT s) = P hull s)`,
 269   REWRITE_TAC[HULL_REDUNDANT_EQ]);;
 270
 271 let HULL_INDUCT = prove
 272  (`!P p s. (!x:A. x IN s ==> p x) /\ P {x | p x}
 273            ==> !x. x IN P hull s ==> p x`,
 274   REPEAT GEN_TAC THEN
 275   MP_TAC(ISPECL [`P:(A->bool)->bool`; `s:A->bool`; `{x:A | p x}`]
 276                 HULL_MINIMAL) THEN
 277   REWRITE_TAC[SUBSET; IN_ELIM_THM]);;
 278
 279 let HULL_INC = prove
 280  (`!P s x. x IN s ==> x IN P hull s`,
 281   MESON_TAC[REWRITE_RULE[SUBSET] HULL_SUBSET]);;
 282
 283 let HULL_IMAGE_SUBSET = prove
 284  (`!P f s. P(P hull s) /\ (!s. P s ==> P(IMAGE f s))
 285            ==> P hull (IMAGE f s) SUBSET (IMAGE f (P hull s))`,
 286   REPEAT STRIP_TAC THEN MATCH_MP_TAC HULL_MINIMAL THEN
 287   ASM_SIMP_TAC[IMAGE_SUBSET; HULL_SUBSET]);;
 288
 289 let HULL_IMAGE_GALOIS = prove
 290  (`!P f g s. (!s. P(P hull s)) /\
 291              (!s. P s ==> P(IMAGE f s)) /\ (!s. P s ==> P(IMAGE g s)) /\
 292              (!s t. s SUBSET IMAGE g t <=> IMAGE f s SUBSET t)
 293              ==> P hull (IMAGE f s) = IMAGE f (P hull s)`,
 294   REPEAT STRIP_TAC THEN MATCH_MP_TAC SUBSET_ANTISYM THEN
 295   ASM_SIMP_TAC[HULL_IMAGE_SUBSET] THEN
 296   FIRST_ASSUM(fun th -> GEN_REWRITE_TAC I [GSYM th]) THEN
 297   MATCH_MP_TAC HULL_MINIMAL THEN
 298   ASM_SIMP_TAC[HULL_SUBSET]);;
 299
 300 let HULL_IMAGE = prove
 301  (`!P f s. (!s. P(P hull s)) /\ (!s. P(IMAGE f s) <=> P s) /\
 302            (!x y:A. f x = f y ==> x = y) /\ (!y. ?x. f x = y)
 303            ==> P hull (IMAGE f s) = IMAGE f (P hull s)`,
 304   REPEAT GEN_TAC THEN
 305   REPLICATE_TAC 2 (DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
 306   REWRITE_TAC[BIJECTIVE_LEFT_RIGHT_INVERSE] THEN
 307   DISCH_THEN(X_CHOOSE_THEN `g:A->A` STRIP_ASSUME_TAC) THEN
 308   MATCH_MP_TAC HULL_IMAGE_GALOIS THEN EXISTS_TAC `g:A->A` THEN
 309   ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
 310   X_GEN_TAC `s:A->bool` THEN
 311   FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [GSYM th]) THEN
 312   MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN ASM SET_TAC[]);;
 313
 314 let IS_HULL = prove
 315  (`!P s. (!f. (!s. s IN f ==> P s) ==> P(INTERS f))
 316          ==> (P s <=> ?t. s = P hull t)`,
 317   MESON_TAC[HULL_P; P_HULL]);;
 318
 319 let HULLS_EQ = prove
 320  (`!P s t.
 321         (!f. (!s. s IN f ==> P s) ==> P (INTERS f)) /\
 322         s SUBSET P hull t /\ t SUBSET P hull s
 323         ==> P hull s = P hull t`,
 324   REPEAT STRIP_TAC THEN MATCH_MP_TAC SUBSET_ANTISYM THEN
 325   CONJ_TAC THEN MATCH_MP_TAC HULL_MINIMAL THEN
 326   ASM_SIMP_TAC[P_HULL]);;
 327
 328 let HULL_P_AND_Q = prove
 329  (`!P Q. (!f. (!s. s IN f ==> P s) ==> P(INTERS f)) /\
 330          (!f. (!s. s IN f ==> Q s) ==> Q(INTERS f)) /\
 331          (!s. Q s ==> Q(P hull s))
 332          ==> (\x. P x /\ Q x) hull s = P hull (Q hull s)`,
 333   REPEAT STRIP_TAC THEN
 334   MATCH_MP_TAC HULL_UNIQUE THEN ASM_SIMP_TAC[HULL_INC; SUBSET_HULL] THEN
 335   ASM_MESON_TAC[P_HULL; HULL_SUBSET; SUBSET_TRANS]);;
 336
 337 (* ------------------------------------------------------------------------- *)
 338 (* More variants of the Archimedian property and useful consequences.        *)
 339 (* ------------------------------------------------------------------------- *)
 340
 341 let REAL_ARCH_INV = prove
 342  (`!e. &0 < e <=> ?n. ~(n = 0) /\ &0 < inv(&n) /\ inv(&n) < e`,
 343   GEN_TAC THEN EQ_TAC THENL [ALL_TAC; MESON_TAC[REAL_LT_TRANS]] THEN
 344   DISCH_TAC THEN MP_TAC(SPEC `inv(e)` REAL_ARCH_LT) THEN
 345   MATCH_MP_TAC MONO_EXISTS THEN
 346   ASM_MESON_TAC[REAL_LT_INV2; REAL_INV_INV; REAL_LT_INV_EQ; REAL_LT_TRANS;
 347                 REAL_LT_ANTISYM]);;
 348
 349 let REAL_POW_LBOUND = prove
 350  (`!x n. &0 <= x ==> &1 + &n * x <= (&1 + x) pow n`,
 351   GEN_TAC THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN
 352   INDUCT_TAC THEN
 353   REWRITE_TAC[real_pow; REAL_MUL_LZERO; REAL_ADD_RID; REAL_LE_REFL] THEN
 354   REWRITE_TAC[GSYM REAL_OF_NUM_SUC] THEN
 355   MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `(&1 + x) * (&1 + &n * x)` THEN
 356   ASM_SIMP_TAC[REAL_LE_LMUL; REAL_ARITH `&0 <= x ==> &0 <= &1 + x`] THEN
 357   ASM_SIMP_TAC[REAL_LE_MUL; REAL_POS; REAL_ARITH
 358    `&1 + (n + &1) * x <= (&1 + x) * (&1 + n * x) <=> &0 <= n * x * x`]);;
 359
 360 let REAL_ARCH_POW = prove
 361  (`!x y. &1 < x ==> ?n. y < x pow n`,
 362   REPEAT STRIP_TAC THEN
 363   MP_TAC(SPEC `x - &1` REAL_ARCH) THEN ASM_REWRITE_TAC[REAL_SUB_LT] THEN
 364   DISCH_THEN(MP_TAC o SPEC `y:real`) THEN MATCH_MP_TAC MONO_EXISTS THEN
 365   X_GEN_TAC `n:num` THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LTE_TRANS THEN
 366   EXISTS_TAC `&1 + &n * (x - &1)` THEN
 367   ASM_SIMP_TAC[REAL_ARITH `x < y ==> x < &1 + y`] THEN
 368   ASM_MESON_TAC[REAL_POW_LBOUND; REAL_SUB_ADD2; REAL_ARITH
 369     `&1 < x ==> &0 <= x - &1`]);;
 370
 371 let REAL_ARCH_POW2 = prove
 372  (`!x. ?n. x < &2 pow n`,
 373   SIMP_TAC[REAL_ARCH_POW; REAL_OF_NUM_LT; ARITH]);;
 374
 375 let REAL_ARCH_POW_INV = prove
 376  (`!x y. &0 < y /\ x < &1 ==> ?n. x pow n < y`,
 377   REPEAT STRIP_TAC THEN ASM_CASES_TAC `&0 < x` THENL
 378    [ALL_TAC; ASM_MESON_TAC[REAL_POW_1; REAL_LET_TRANS; REAL_NOT_LT]] THEN
 379   SUBGOAL_THEN `inv(&1) < inv(x)` MP_TAC THENL
 380    [ASM_SIMP_TAC[REAL_LT_INV2]; REWRITE_TAC[REAL_INV_1]] THEN
 381   DISCH_THEN(MP_TAC o SPEC `inv(y)` o MATCH_MP REAL_ARCH_POW) THEN
 382   MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN DISCH_TAC THEN
 383   GEN_REWRITE_TAC BINOP_CONV [GSYM REAL_INV_INV] THEN
 384   ASM_SIMP_TAC[GSYM REAL_POW_INV; REAL_LT_INV; REAL_LT_INV2]);;
 385
 386 let FORALL_POS_MONO = prove
 387  (`!P. (!d e. d < e /\ P d ==> P e) /\ (!n. ~(n = 0) ==> P(inv(&n)))
 388        ==> !e. &0 < e ==> P e`,
 389   MESON_TAC[REAL_ARCH_INV; REAL_LT_TRANS]);;
 390
 391 let FORALL_POS_MONO_1 = prove
 392  (`!P. (!d e. d < e /\ P d ==> P e) /\ (!n. P(inv(&n + &1)))
 393        ==> !e. &0 < e ==> P e`,
 394   REWRITE_TAC[REAL_OF_NUM_SUC; GSYM FORALL_SUC; FORALL_POS_MONO]);;
 395
 396 let REAL_ARCH_RDIV_EQ_0 = prove
 397  (`!x c. &0 <= x /\ &0 <= c /\ (!m. 0 < m ==> &m * x <= c) ==> x = &0`,
 398   SIMP_TAC [GSYM REAL_LE_ANTISYM; GSYM REAL_NOT_LT] THEN REPEAT STRIP_TAC THEN
 399   POP_ASSUM (STRIP_ASSUME_TAC o SPEC `c:real` o MATCH_MP REAL_ARCH) THEN
 400   ASM_CASES_TAC `n=0` THENL
 401    [POP_ASSUM SUBST_ALL_TAC THEN
 402     RULE_ASSUM_TAC (REWRITE_RULE [REAL_MUL_LZERO]) THEN
 403     ASM_MESON_TAC [REAL_LET_ANTISYM];
 404     ASM_MESON_TAC [REAL_LET_ANTISYM; REAL_MUL_SYM; LT_NZ]]);;
 405
 406 (* ------------------------------------------------------------------------- *)
 407 (* Relate max and min to sup and inf.                                        *)
 408 (* ------------------------------------------------------------------------- *)
 409
 410 let REAL_MAX_SUP = prove
 411  (`!x y. max x y = sup {x,y}`,
 412   SIMP_TAC[GSYM REAL_LE_ANTISYM; REAL_SUP_LE_FINITE; REAL_LE_SUP_FINITE;
 413            FINITE_RULES; NOT_INSERT_EMPTY; REAL_MAX_LE; REAL_LE_MAX] THEN
 414   REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN MESON_TAC[REAL_LE_TOTAL]);;
 415
 416 let REAL_MIN_INF = prove
 417  (`!x y. min x y = inf {x,y}`,
 418   SIMP_TAC[GSYM REAL_LE_ANTISYM; REAL_INF_LE_FINITE; REAL_LE_INF_FINITE;
 419            FINITE_RULES; NOT_INSERT_EMPTY; REAL_MIN_LE; REAL_LE_MIN] THEN
 420   REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN MESON_TAC[REAL_LE_TOTAL]);;
 421
 422 (* ------------------------------------------------------------------------- *)
 423 (* Define square root here to decouple it from the existing analysis theory. *)
 424 (* ------------------------------------------------------------------------- *)
 425
 426 let sqrt = new_definition
 427   `sqrt(x) = @y. &0 <= y /\ (y pow 2 = x)`;;
 428
 429 let SQRT_UNIQUE = prove
 430  (`!x y. &0 <= y /\ (y pow 2 = x) ==> (sqrt(x) = y)`,
 431   REPEAT STRIP_TAC THEN REWRITE_TAC[sqrt] THEN MATCH_MP_TAC SELECT_UNIQUE THEN
 432   FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN REWRITE_TAC[REAL_POW_2] THEN
 433   REWRITE_TAC[REAL_ARITH `(x * x = y * y) <=> ((x + y) * (x - y) = &0)`] THEN
 434   REWRITE_TAC[REAL_ENTIRE] THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
 435
 436 let POW_2_SQRT = prove
 437  (`!x. &0 <= x ==> (sqrt(x pow 2) = x)`,
 438   MESON_TAC[SQRT_UNIQUE]);;
 439
 440 let SQRT_0 = prove
 441  (`sqrt(&0) = &0`,
 442   MESON_TAC[SQRT_UNIQUE; REAL_POW_2; REAL_MUL_LZERO; REAL_POS]);;
 443
 444 let SQRT_1 = prove
 445  (`sqrt(&1) = &1`,
 446    MESON_TAC[SQRT_UNIQUE; REAL_POW_2; REAL_MUL_LID; REAL_POS]);;
 447
 448 let POW_2_SQRT_ABS = prove
 449  (`!x. sqrt(x pow 2) = abs(x)`,
 450   GEN_TAC THEN MATCH_MP_TAC SQRT_UNIQUE THEN
 451   REWRITE_TAC[REAL_ABS_POS; REAL_POW_2; GSYM REAL_ABS_MUL] THEN
 452   REWRITE_TAC[real_abs; REAL_LE_SQUARE]);;
 453
 454 (* ------------------------------------------------------------------------- *)
 455 (* Geometric progression.                                                    *)
 456 (* ------------------------------------------------------------------------- *)
 457
 458 let SUM_GP_BASIC = prove
 459  (`!x n. (&1 - x) * sum(0..n) (\i. x pow i) = &1 - x pow (SUC n)`,
 460   GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[SUM_CLAUSES_NUMSEG] THEN
 461   REWRITE_TAC[real_pow; REAL_MUL_RID; LE_0] THEN
 462   ASM_REWRITE_TAC[REAL_ADD_LDISTRIB; real_pow] THEN REAL_ARITH_TAC);;
 463
 464 let SUM_GP_MULTIPLIED = prove
 465  (`!x m n. m <= n
 466            ==> ((&1 - x) * sum(m..n) (\i. x pow i) = x pow m - x pow (SUC n))`,
 467   REPEAT STRIP_TAC THEN ASM_SIMP_TAC
 468    [SUM_OFFSET_0; REAL_POW_ADD; REAL_MUL_ASSOC; SUM_GP_BASIC; SUM_RMUL] THEN
 469   REWRITE_TAC[REAL_SUB_RDISTRIB; GSYM REAL_POW_ADD; REAL_MUL_LID] THEN
 470   ASM_SIMP_TAC[ARITH_RULE `m <= n ==> (SUC(n - m) + m = SUC n)`]);;
 471
 472 let SUM_GP = prove
 473  (`!x m n.
 474         sum(m..n) (\i. x pow i) =
 475                 if n < m then &0
 476                 else if x = &1 then &((n + 1) - m)
 477                 else (x pow m - x pow (SUC n)) / (&1 - x)`,
 478   REPEAT GEN_TAC THEN
 479   DISJ_CASES_TAC(ARITH_RULE `n < m \/ ~(n < m) /\ m <= n:num`) THEN
 480   ASM_SIMP_TAC[SUM_TRIV_NUMSEG] THEN COND_CASES_TAC THENL
 481    [ASM_REWRITE_TAC[REAL_POW_ONE; SUM_CONST_NUMSEG; REAL_MUL_RID]; ALL_TAC] THEN
 482   MATCH_MP_TAC REAL_EQ_LCANCEL_IMP THEN EXISTS_TAC `&1 - x` THEN
 483   ASM_SIMP_TAC[REAL_DIV_LMUL; REAL_SUB_0; SUM_GP_MULTIPLIED]);;
 484
 485 let SUM_GP_OFFSET = prove
 486  (`!x m n. sum(m..m+n) (\i. x pow i) =
 487                 if x = &1 then &n + &1
 488                 else x pow m * (&1 - x pow (SUC n)) / (&1 - x)`,
 489   REPEAT GEN_TAC THEN REWRITE_TAC[SUM_GP; ARITH_RULE `~(m + n < m:num)`] THEN
 490   COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL
 491    [REWRITE_TAC[REAL_OF_NUM_ADD] THEN AP_TERM_TAC THEN ARITH_TAC;
 492     REWRITE_TAC[real_div; real_pow; REAL_POW_ADD] THEN REAL_ARITH_TAC]);;
 493
 494 (* ------------------------------------------------------------------------- *)
 495 (* Segment of natural numbers starting at a specific number.                 *)
 496 (* ------------------------------------------------------------------------- *)
 497
 498 let from = new_definition
 499   `from n = {m:num | n <= m}`;;
 500
 501 let FROM_0 = prove
 502  (`from 0 = (:num)`,
 503   REWRITE_TAC[from; LE_0] THEN SET_TAC[]);;
 504
 505 let FROM_INTER_NUMSEG_GEN = prove
 506  (`!k m n. (from k) INTER (m..n) = (if m < k then k..n else m..n)`,
 507   REPEAT GEN_TAC THEN COND_CASES_TAC THEN POP_ASSUM MP_TAC THEN
 508   REWRITE_TAC[from; IN_ELIM_THM; IN_INTER; IN_NUMSEG; EXTENSION] THEN
 509   ARITH_TAC);;
 510
 511 let FROM_INTER_NUMSEG = prove
 512  (`!k n. (from k) INTER (0..n) = k..n`,
 513   REWRITE_TAC[from; IN_ELIM_THM; IN_INTER; IN_NUMSEG; EXTENSION] THEN
 514   ARITH_TAC);;
 515
 516 let IN_FROM = prove
 517  (`!m n. m IN from n <=> n <= m`,
 518   REWRITE_TAC[from; IN_ELIM_THM]);;
 519
 520 let INFINITE_FROM = prove
 521  (`!n. INFINITE(from n)`,
 522   GEN_TAC THEN
 523   SUBGOAL_THEN `from n = (:num) DIFF {i | i < n}`
 524    (fun th -> SIMP_TAC[th; INFINITE_DIFF_FINITE; FINITE_NUMSEG_LT;
 525    num_INFINITE]) THEN
 526   REWRITE_TAC[EXTENSION; from; IN_DIFF; IN_UNIV; IN_ELIM_THM] THEN ARITH_TAC);;