realax.ml

   1 (* ========================================================================= *)
   2 (* Theory of real numbers.                                                   *)
   3 (*                                                                           *)
   4 (*       John Harrison, University of Cambridge Computer Laboratory          *)
   5 (*                                                                           *)
   6 (*            (c) Copyright, University of Cambridge 1998                    *)
   7 (*              (c) Copyright, John Harrison 1998-2007                       *)
   8 (* ========================================================================= *)
   9
  10 needs "lists.ml";;
  11
  12 (* ------------------------------------------------------------------------- *)
  13 (* The main infix overloaded operations                                      *)
  14 (* ------------------------------------------------------------------------- *)
  15
  16 parse_as_infix("++",(16,"right"));;
  17 parse_as_infix("**",(20,"right"));;
  18 parse_as_infix("<<=",(12,"right"));;
  19 parse_as_infix("===",(10,"right"));;
  20
  21 parse_as_infix ("treal_mul",(20,"right"));;
  22 parse_as_infix ("treal_add",(16,"right"));;
  23 parse_as_infix ("treal_le",(12,"right"));;
  24 parse_as_infix ("treal_eq",(10,"right"));;
  25
  26 make_overloadable "+" `:A->A->A`;;
  27 make_overloadable "-" `:A->A->A`;;
  28 make_overloadable "*" `:A->A->A`;;
  29 make_overloadable "/" `:A->A->A`;;
  30 make_overloadable "<" `:A->A->bool`;;
  31 make_overloadable "<=" `:A->A->bool`;;
  32 make_overloadable ">" `:A->A->bool`;;
  33 make_overloadable ">=" `:A->A->bool`;;
  34 make_overloadable "--" `:A->A`;;
  35 make_overloadable "pow" `:A->num->A`;;
  36 make_overloadable "inv" `:A->A`;;
  37 make_overloadable "abs" `:A->A`;;
  38 make_overloadable "max" `:A->A->A`;;
  39 make_overloadable "min" `:A->A->A`;;
  40 make_overloadable "&" `:num->A`;;
  41
  42 do_list overload_interface
  43  ["+",`(+):num->num->num`; "-",`(-):num->num->num`;
  44   "*",`(*):num->num->num`; "<",`(<):num->num->bool`;
  45   "<=",`(<=):num->num->bool`; ">",`(>):num->num->bool`;
  46   ">=",`(>=):num->num->bool`];;
  47
  48 let prioritize_num() = prioritize_overload(mk_type("num",[]));;
  49
  50 (* ------------------------------------------------------------------------- *)
  51 (* Absolute distance function on the naturals.                               *)
  52 (* ------------------------------------------------------------------------- *)
  53
  54 let dist = new_definition
  55   `dist(m,n) = (m - n) + (n - m)`;;
  56
  57 (* ------------------------------------------------------------------------- *)
  58 (* Some easy theorems.                                                       *)
  59 (* ------------------------------------------------------------------------- *)
  60
  61 let DIST_REFL = prove
  62  (`!n. dist(n,n) = 0`,
  63   REWRITE_TAC[dist; SUB_REFL; ADD_CLAUSES]);;
  64
  65 let DIST_LZERO = prove
  66  (`!n. dist(0,n) = n`,
  67   REWRITE_TAC[dist; SUB_0; ADD_CLAUSES]);;
  68
  69 let DIST_RZERO = prove
  70  (`!n. dist(n,0) = n`,
  71   REWRITE_TAC[dist; SUB_0; ADD_CLAUSES]);;
  72
  73 let DIST_SYM = prove
  74  (`!m n. dist(m,n) = dist(n,m)`,
  75   REWRITE_TAC[dist] THEN MATCH_ACCEPT_TAC ADD_SYM);;
  76
  77 let DIST_LADD = prove
  78  (`!m p n. dist(m + n,m + p) = dist(n,p)`,
  79   REWRITE_TAC[dist; SUB_ADD_LCANCEL]);;
  80
  81 let DIST_RADD = prove
  82  (`!m p n. dist(m + p,n + p) = dist(m,n)`,
  83   REWRITE_TAC[dist; SUB_ADD_RCANCEL]);;
  84
  85 let DIST_LADD_0 = prove
  86  (`!m n. dist(m + n,m) = n`,
  87   REWRITE_TAC[dist; ADD_SUB2; ADD_SUBR2; ADD_CLAUSES]);;
  88
  89 let DIST_RADD_0 = prove
  90  (`!m n. dist(m,m + n) = n`,
  91   ONCE_REWRITE_TAC[DIST_SYM] THEN MATCH_ACCEPT_TAC DIST_LADD_0);;
  92
  93 let DIST_LMUL = prove
  94  (`!m n p. m * dist(n,p) = dist(m * n,m * p)`,
  95   REWRITE_TAC[dist; LEFT_ADD_DISTRIB; LEFT_SUB_DISTRIB]);;
  96
  97 let DIST_RMUL = prove
  98  (`!m n p. dist(m,n) * p = dist(m * p,n * p)`,
  99   REWRITE_TAC[dist; RIGHT_ADD_DISTRIB; RIGHT_SUB_DISTRIB]);;
 100
 101 let DIST_EQ_0 = prove
 102  (`!m n. (dist(m,n) = 0) <=> (m = n)`,
 103   REWRITE_TAC[dist; ADD_EQ_0; SUB_EQ_0; LE_ANTISYM]);;
 104
 105 (* ------------------------------------------------------------------------- *)
 106 (* Simplifying theorem about the distance operation.                         *)
 107 (* ------------------------------------------------------------------------- *)
 108
 109 let DIST_ELIM_THM = prove
 110  (`P(dist(x,y)) <=> !d. ((x = y + d) ==> P(d)) /\ ((y = x + d) ==> P(d))`,
 111   DISJ_CASES_TAC(SPECL [`x:num`; `y:num`] LE_CASES) THEN
 112   POP_ASSUM(X_CHOOSE_THEN `e:num` SUBST1_TAC o REWRITE_RULE[LE_EXISTS]) THEN
 113   REWRITE_TAC[dist; ADD_SUB; ADD_SUB2; ADD_SUBR; ADD_SUBR2] THEN
 114   REWRITE_TAC[ADD_CLAUSES; EQ_ADD_LCANCEL] THEN
 115   GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [EQ_SYM_EQ] THEN
 116   REWRITE_TAC[GSYM ADD_ASSOC; EQ_ADD_LCANCEL_0; ADD_EQ_0] THEN
 117   ASM_CASES_TAC `e = 0` THEN ASM_REWRITE_TAC[] THEN
 118   EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 119   FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);;
 120
 121 (* ------------------------------------------------------------------------- *)
 122 (* Now some more theorems.                                                   *)
 123 (* ------------------------------------------------------------------------- *)
 124
 125 let DIST_LE_CASES,DIST_ADDBOUND,DIST_TRIANGLE,DIST_ADD2,DIST_ADD2_REV =
 126   let DIST_ELIM_TAC =
 127     let conv =
 128       HIGHER_REWRITE_CONV[SUB_ELIM_THM; COND_ELIM_THM; DIST_ELIM_THM] false in
 129     CONV_TAC conv THEN TRY GEN_TAC THEN CONJ_TAC THEN
 130     DISCH_THEN(fun th -> SUBST_ALL_TAC th THEN
 131                          (let l,r = dest_eq (concl th) in
 132                           if is_var l & not (vfree_in l r) then ALL_TAC
 133                           else ASSUME_TAC th)) in
 134   let DIST_ELIM_TAC' =
 135     REPEAT STRIP_TAC THEN REPEAT DIST_ELIM_TAC THEN
 136     REWRITE_TAC[GSYM NOT_LT; LT_EXISTS] THEN
 137     DISCH_THEN(CHOOSE_THEN SUBST_ALL_TAC) THEN POP_ASSUM MP_TAC THEN
 138     CONV_TAC(LAND_CONV NUM_CANCEL_CONV) THEN
 139     REWRITE_TAC[ADD_CLAUSES; NOT_SUC] in
 140   let DIST_LE_CASES = prove
 141    (`!m n p. dist(m,n) <= p <=> (m <= n + p) /\ (n <= m + p)`,
 142     REPEAT GEN_TAC THEN REPEAT DIST_ELIM_TAC THEN
 143     REWRITE_TAC[GSYM ADD_ASSOC; LE_ADD; LE_ADD_LCANCEL])
 144   and DIST_ADDBOUND = prove
 145    (`!m n. dist(m,n) <= m + n`,
 146     REPEAT GEN_TAC THEN DIST_ELIM_TAC THENL
 147      [ONCE_REWRITE_TAC[ADD_SYM]; ALL_TAC] THEN
 148     REWRITE_TAC[ADD_ASSOC; LE_ADDR])
 149   and [DIST_TRIANGLE; DIST_ADD2; DIST_ADD2_REV] = (CONJUNCTS o prove)
 150    (`(!m n p. dist(m,p) <= dist(m,n) + dist(n,p)) /\
 151      (!m n p q. dist(m + n,p + q) <= dist(m,p) + dist(n,q)) /\
 152      (!m n p q. dist(m,p) <= dist(m + n,p + q) + dist(n,q))`,
 153     DIST_ELIM_TAC') in
 154   DIST_LE_CASES,DIST_ADDBOUND,DIST_TRIANGLE,DIST_ADD2,DIST_ADD2_REV;;
 155
 156 let DIST_TRIANGLE_LE = prove
 157  (`!m n p q. dist(m,n) + dist(n,p) <= q ==> dist(m,p) <= q`,
 158   REPEAT STRIP_TAC THEN MATCH_MP_TAC LE_TRANS THEN
 159   EXISTS_TAC `dist(m,n) + dist(n,p)` THEN ASM_REWRITE_TAC[DIST_TRIANGLE]);;
 160
 161 let DIST_TRIANGLES_LE = prove
 162  (`!m n p q r s.
 163         dist(m,n) <= r /\ dist(p,q) <= s ==> dist(m,p) <= dist(n,q) + r + s`,
 164   REPEAT STRIP_TAC THEN MATCH_MP_TAC DIST_TRIANGLE_LE THEN
 165   EXISTS_TAC `n:num` THEN GEN_REWRITE_TAC RAND_CONV [ADD_SYM] THEN
 166   REWRITE_TAC[GSYM ADD_ASSOC] THEN MATCH_MP_TAC LE_ADD2 THEN
 167   ASM_REWRITE_TAC[] THEN MATCH_MP_TAC DIST_TRIANGLE_LE THEN
 168   EXISTS_TAC `q:num` THEN GEN_REWRITE_TAC RAND_CONV [ADD_SYM] THEN
 169   REWRITE_TAC[LE_ADD_LCANCEL] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN
 170   ASM_REWRITE_TAC[]);;
 171
 172 (* ------------------------------------------------------------------------- *)
 173 (* Useful lemmas about bounds.                                               *)
 174 (* ------------------------------------------------------------------------- *)
 175
 176 let BOUNDS_LINEAR = prove
 177  (`!A B C. (!n. A * n <= B * n + C) <=> A <= B`,
 178   REPEAT GEN_TAC THEN EQ_TAC THENL
 179    [CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[NOT_LE] THEN
 180     DISCH_THEN(CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[LT_EXISTS]) THEN
 181     REWRITE_TAC[RIGHT_ADD_DISTRIB; LE_ADD_LCANCEL] THEN
 182     DISCH_THEN(MP_TAC o SPEC `SUC C`) THEN
 183     REWRITE_TAC[NOT_LE; MULT_CLAUSES; ADD_CLAUSES; LT_SUC_LE] THEN
 184     REWRITE_TAC[ADD_ASSOC; LE_ADDR];
 185     DISCH_THEN(CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[LE_EXISTS]) THEN
 186     REWRITE_TAC[RIGHT_ADD_DISTRIB; GSYM ADD_ASSOC; LE_ADD]]);;
 187
 188 let BOUNDS_LINEAR_0 = prove
 189  (`!A B. (!n. A * n <= B) <=> (A = 0)`,
 190   REPEAT GEN_TAC THEN MP_TAC(SPECL [`A:num`; `0`; `B:num`] BOUNDS_LINEAR) THEN
 191   REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES; LE]);;
 192
 193 let BOUNDS_DIVIDED = prove
 194  (`!P. (?B. !n. P(n) <= B) <=>
 195        (?A B. !n. n * P(n) <= A * n + B)`,
 196   GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL
 197    [MAP_EVERY EXISTS_TAC [`B:num`; `0`] THEN
 198     GEN_TAC THEN REWRITE_TAC[ADD_CLAUSES] THEN
 199     GEN_REWRITE_TAC RAND_CONV [MULT_SYM] THEN
 200     ASM_REWRITE_TAC[LE_MULT_LCANCEL];
 201     EXISTS_TAC `P(0) + A + B` THEN GEN_TAC THEN
 202     MP_TAC(SPECL [`n:num`; `(P:num->num) n`; `P(0) + A + B`]
 203      LE_MULT_LCANCEL) THEN
 204     ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[LE_ADD] THEN
 205     DISCH_THEN(SUBST1_TAC o SYM) THEN
 206     MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `A * n + B` THEN
 207     ASM_REWRITE_TAC[] THEN REWRITE_TAC[LEFT_ADD_DISTRIB] THEN
 208     GEN_REWRITE_TAC RAND_CONV [ADD_SYM] THEN
 209     GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [MULT_SYM] THEN
 210     REWRITE_TAC[GSYM ADD_ASSOC; LE_ADD_LCANCEL] THEN
 211     MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `B * n` THEN
 212     REWRITE_TAC[LE_ADD] THEN UNDISCH_TAC `~(n = 0)` THEN
 213     SPEC_TAC(`n:num`,`n:num`) THEN INDUCT_TAC THEN
 214     ASM_REWRITE_TAC[MULT_CLAUSES; LE_ADD]]);;
 215
 216 let BOUNDS_NOTZERO = prove
 217  (`!P A B. (P 0 0 = 0) /\ (!m n. P m n <= A * (m + n) + B) ==>
 218        (?B. !m n. P m n <= B * (m + n))`,
 219   REPEAT STRIP_TAC THEN EXISTS_TAC `A + B` THEN
 220   REPEAT GEN_TAC THEN ASM_CASES_TAC `m + n = 0` THENL
 221    [RULE_ASSUM_TAC(REWRITE_RULE[ADD_EQ_0]) THEN ASM_REWRITE_TAC[LE_0];
 222     MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `A * (m + n) + B` THEN
 223     ASM_REWRITE_TAC[] THEN REWRITE_TAC[RIGHT_ADD_DISTRIB; LE_ADD_LCANCEL] THEN
 224     UNDISCH_TAC `~(m + n = 0)` THEN SPEC_TAC(`m + n`,`p:num`) THEN
 225     INDUCT_TAC THEN REWRITE_TAC[MULT_CLAUSES; LE_ADD]]);;
 226
 227 let BOUNDS_IGNORE = prove
 228  (`!P Q. (?B. !i. P(i) <= Q(i) + B) <=>
 229          (?B N. !i. N <= i ==> P(i) <= Q(i) + B)`,
 230   REPEAT GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL
 231    [EXISTS_TAC `B:num` THEN ASM_REWRITE_TAC[];
 232     POP_ASSUM MP_TAC THEN SPEC_TAC(`B:num`,`B:num`) THEN
 233     SPEC_TAC(`N:num`,`N:num`) THEN INDUCT_TAC THENL
 234      [REWRITE_TAC[LE_0] THEN GEN_TAC THEN DISCH_TAC THEN
 235       EXISTS_TAC `B:num` THEN ASM_REWRITE_TAC[];
 236       GEN_TAC THEN DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
 237       EXISTS_TAC `B + P(N:num)` THEN X_GEN_TAC `i:num` THEN
 238       DISCH_TAC THEN ASM_CASES_TAC `SUC N <= i` THENL
 239        [MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `Q(i:num) + B` THEN
 240         REWRITE_TAC[LE_ADD; ADD_ASSOC] THEN FIRST_ASSUM MATCH_MP_TAC THEN
 241         ASM_REWRITE_TAC[];
 242         UNDISCH_TAC `~(SUC N <= i)` THEN REWRITE_TAC[NOT_LE; LT] THEN
 243         ASM_REWRITE_TAC[GSYM NOT_LE] THEN DISCH_THEN SUBST1_TAC THEN
 244         REWRITE_TAC[ADD_ASSOC] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
 245         REWRITE_TAC[LE_ADD]]]]);;
 246
 247 (* ------------------------------------------------------------------------- *)
 248 (* Define type of nearly additive functions.                                 *)
 249 (* ------------------------------------------------------------------------- *)
 250
 251 let is_nadd = new_definition
 252   `is_nadd x <=> (?B. !m n. dist(m * x(n),n * x(m)) <= B * (m + n))`;;
 253
 254 let is_nadd_0 = prove
 255  (`is_nadd (\n. 0)`,
 256   REWRITE_TAC[is_nadd; MULT_CLAUSES; DIST_REFL; LE_0]);;
 257
 258 let nadd_abs,nadd_rep =
 259   new_basic_type_definition "nadd" ("mk_nadd","dest_nadd") is_nadd_0;;
 260
 261 override_interface ("fn",`dest_nadd`);;
 262 override_interface ("afn",`mk_nadd`);;
 263
 264 (* ------------------------------------------------------------------------- *)
 265 (* Properties of nearly-additive functions.                                  *)
 266 (* ------------------------------------------------------------------------- *)
 267
 268 let NADD_CAUCHY = prove
 269  (`!x. ?B. !m n. dist(m * fn x n,n * fn x m) <= B * (m + n)`,
 270   REWRITE_TAC[GSYM is_nadd; nadd_rep; nadd_abs; ETA_AX]);;
 271
 272 let NADD_BOUND = prove
 273  (`!x. ?A B. !n. fn x n <= A * n + B`,
 274   GEN_TAC THEN X_CHOOSE_TAC `B:num` (SPEC `x:nadd` NADD_CAUCHY) THEN
 275   MAP_EVERY EXISTS_TAC [`B + fn x 1`; `B:num`] THEN GEN_TAC THEN
 276   POP_ASSUM(MP_TAC o SPECL [`n:num`; `1`]) THEN
 277   REWRITE_TAC[DIST_LE_CASES; MULT_CLAUSES] THEN
 278   DISCH_THEN(MP_TAC o CONJUNCT2) THEN
 279   REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB; MULT_CLAUSES] THEN
 280   REWRITE_TAC[ADD_AC; MULT_AC]);;
 281
 282 let NADD_MULTIPLICATIVE = prove
 283  (`!x. ?B. !m n. dist(fn x (m * n),m * fn x n) <= B * m + B`,
 284   GEN_TAC THEN X_CHOOSE_TAC `B:num` (SPEC `x:nadd` NADD_CAUCHY) THEN
 285   EXISTS_TAC `B + fn x 0` THEN REPEAT GEN_TAC THEN
 286   ASM_CASES_TAC `n = 0` THENL
 287    [MATCH_MP_TAC (LE_IMP DIST_ADDBOUND) THEN
 288     ASM_REWRITE_TAC[MULT_CLAUSES; RIGHT_ADD_DISTRIB; MULT_AC] THEN
 289     REWRITE_TAC[LE_EXISTS] THEN CONV_TAC(ONCE_DEPTH_CONV NUM_CANCEL_CONV) THEN
 290     REWRITE_TAC[GSYM EXISTS_REFL]; UNDISCH_TAC `~(n = 0)`] THEN
 291   REWRITE_TAC[TAUT `(~a ==> b) <=> a \/ b`; GSYM LE_MULT_LCANCEL;
 292               DIST_LMUL] THEN
 293   REWRITE_TAC[MULT_ASSOC] THEN GEN_REWRITE_TAC
 294    (LAND_CONV o RAND_CONV o RAND_CONV o LAND_CONV) [MULT_SYM] THEN
 295   POP_ASSUM(MATCH_MP_TAC o LE_IMP) THEN
 296   REWRITE_TAC[LE_EXISTS; RIGHT_ADD_DISTRIB; LEFT_ADD_DISTRIB; MULT_AC] THEN
 297   CONV_TAC(ONCE_DEPTH_CONV NUM_CANCEL_CONV) THEN
 298   REWRITE_TAC[GSYM EXISTS_REFL]);;
 299
 300 let NADD_ADDITIVE = prove
 301  (`!x. ?B. !m n. dist(fn x (m + n),fn x m + fn x n) <= B`,
 302   GEN_TAC THEN X_CHOOSE_TAC `B:num` (SPEC `x:nadd` NADD_CAUCHY) THEN
 303   EXISTS_TAC `3 * B + fn x 0` THEN REPEAT GEN_TAC THEN
 304   ASM_CASES_TAC `m + n = 0` THENL
 305    [RULE_ASSUM_TAC(REWRITE_RULE[ADD_EQ_0]) THEN ONCE_REWRITE_TAC[DIST_SYM] THEN
 306     ASM_REWRITE_TAC[ADD_CLAUSES; DIST_LADD_0; LE_ADDR];
 307     MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `3 * B` THEN
 308     REWRITE_TAC[LE_ADD] THEN UNDISCH_TAC `~(m + n = 0)`] THEN
 309   REWRITE_TAC[TAUT `(~a ==> b) <=> a \/ b`; GSYM LE_MULT_LCANCEL] THEN
 310   REWRITE_TAC[DIST_LMUL; LEFT_ADD_DISTRIB] THEN
 311   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o LAND_CONV) [RIGHT_ADD_DISTRIB] THEN
 312   MATCH_MP_TAC(LE_IMP DIST_ADD2) THEN
 313   SUBGOAL_THEN `(m + n) * 3 * B = B * (m + m + n) + B * (n + m + n)`
 314   SUBST1_TAC THENL
 315    [REWRITE_TAC[SYM(REWRITE_CONV [ARITH] `1 + 1 + 1`)] THEN
 316     REWRITE_TAC[RIGHT_ADD_DISTRIB; LEFT_ADD_DISTRIB; MULT_CLAUSES] THEN
 317     REWRITE_TAC[MULT_AC] THEN CONV_TAC NUM_CANCEL_CONV THEN REFL_TAC;
 318     MATCH_MP_TAC LE_ADD2 THEN ASM_REWRITE_TAC[]]);;
 319
 320 let NADD_SUC = prove
 321  (`!x. ?B. !n. dist(fn x (SUC n),fn x n) <= B`,
 322   GEN_TAC THEN X_CHOOSE_TAC `B:num` (SPEC `x:nadd` NADD_ADDITIVE) THEN
 323   EXISTS_TAC `B + fn x 1` THEN GEN_TAC THEN
 324   MATCH_MP_TAC(LE_IMP DIST_TRIANGLE) THEN
 325   EXISTS_TAC `fn x n + fn x 1` THEN
 326   ASM_REWRITE_TAC[ADD1] THEN MATCH_MP_TAC LE_ADD2 THEN
 327   ASM_REWRITE_TAC[DIST_LADD_0; LE_REFL]);;
 328
 329 let NADD_DIST_LEMMA = prove
 330  (`!x. ?B. !m n. dist(fn x (m + n),fn x m) <= B * n`,
 331   GEN_TAC THEN X_CHOOSE_TAC `B:num` (SPEC `x:nadd` NADD_SUC) THEN
 332   EXISTS_TAC `B:num` THEN GEN_TAC THEN
 333   INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; DIST_REFL; LE_0] THEN
 334   MATCH_MP_TAC(LE_IMP DIST_TRIANGLE) THEN
 335   EXISTS_TAC `fn x (m + n)` THEN
 336   REWRITE_TAC[ADD1; LEFT_ADD_DISTRIB] THEN
 337   GEN_REWRITE_TAC RAND_CONV [ADD_SYM] THEN
 338   MATCH_MP_TAC LE_ADD2 THEN ASM_REWRITE_TAC[GSYM ADD1; MULT_CLAUSES]);;
 339
 340 let NADD_DIST = prove
 341  (`!x. ?B. !m n. dist(fn x m,fn x n) <= B * dist(m,n)`,
 342   GEN_TAC THEN X_CHOOSE_TAC `B:num` (SPEC `x:nadd` NADD_DIST_LEMMA) THEN
 343   EXISTS_TAC `B:num` THEN REPEAT GEN_TAC THEN
 344   DISJ_CASES_THEN MP_TAC (SPECL [`m:num`; `n:num`] LE_CASES) THEN
 345   DISCH_THEN(CHOOSE_THEN SUBST1_TAC o ONCE_REWRITE_RULE[LE_EXISTS]) THENL
 346    [ONCE_REWRITE_TAC[DIST_SYM]; ALL_TAC] THEN
 347   ASM_REWRITE_TAC[DIST_LADD_0]);;
 348
 349 let NADD_ALTMUL = prove
 350  (`!x y. ?A B. !n. dist(n * fn x (fn y n),fn x n * fn y n) <= A * n + B`,
 351   REPEAT GEN_TAC THEN X_CHOOSE_TAC `B:num` (SPEC `x:nadd` NADD_CAUCHY) THEN
 352   MP_TAC(SPEC `y:nadd` NADD_BOUND) THEN
 353   DISCH_THEN(X_CHOOSE_THEN `M:num` (X_CHOOSE_TAC `L:num`)) THEN
 354   MAP_EVERY EXISTS_TAC [`B * (1 + M)`; `B * L`] THEN GEN_TAC THEN
 355   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o RAND_CONV) [MULT_SYM] THEN
 356   MATCH_MP_TAC LE_TRANS THEN  EXISTS_TAC `B * (n + fn y n)` THEN
 357   ASM_REWRITE_TAC[] THEN REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
 358   REWRITE_TAC[MULT_CLAUSES; GSYM ADD_ASSOC; LE_ADD_LCANCEL] THEN
 359   ASM_REWRITE_TAC[GSYM LEFT_ADD_DISTRIB; GSYM MULT_ASSOC; LE_MULT_LCANCEL]);;
 360
 361 (* ------------------------------------------------------------------------- *)
 362 (* Definition of the equivalence relation and proof that it *is* one.        *)
 363 (* ------------------------------------------------------------------------- *)
 364
 365 override_interface ("===",`(nadd_eq):nadd->nadd->bool`);;
 366
 367 let nadd_eq = new_definition
 368   `x === y <=> ?B. !n. dist(fn x n,fn y n) <= B`;;
 369
 370 let NADD_EQ_REFL = prove
 371  (`!x. x === x`,
 372   GEN_TAC THEN REWRITE_TAC[nadd_eq; DIST_REFL; LE_0]);;
 373
 374 let NADD_EQ_SYM = prove
 375  (`!x y. x === y <=> y === x`,
 376   REPEAT GEN_TAC THEN REWRITE_TAC[nadd_eq] THEN
 377   GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [DIST_SYM] THEN REFL_TAC);;
 378
 379 let NADD_EQ_TRANS = prove
 380  (`!x y z. x === y /\ y === z ==> x === z`,
 381   REPEAT GEN_TAC THEN REWRITE_TAC[nadd_eq] THEN
 382   DISCH_THEN(CONJUNCTS_THEN2
 383     (X_CHOOSE_TAC `B1:num`) (X_CHOOSE_TAC `B2:num`)) THEN
 384   EXISTS_TAC `B1 + B2` THEN X_GEN_TAC `n:num` THEN
 385   MATCH_MP_TAC (LE_IMP DIST_TRIANGLE) THEN EXISTS_TAC `fn y n` THEN
 386   MATCH_MP_TAC LE_ADD2 THEN ASM_REWRITE_TAC[]);;
 387
 388 (* ------------------------------------------------------------------------- *)
 389 (* Injection of the natural numbers.                                         *)
 390 (* ------------------------------------------------------------------------- *)
 391
 392 override_interface ("&",`nadd_of_num:num->nadd`);;
 393
 394 let nadd_of_num = new_definition
 395   `&k = afn(\n. k * n)`;;
 396
 397 let NADD_OF_NUM = prove
 398  (`!k. fn(&k) = \n. k * n`,
 399   REWRITE_TAC[nadd_of_num; GSYM nadd_rep; is_nadd] THEN
 400   REWRITE_TAC[DIST_REFL; LE_0; MULT_AC]);;
 401
 402 let NADD_OF_NUM_WELLDEF = prove
 403  (`!m n. (m = n) ==> &m === &n`,
 404   REPEAT GEN_TAC THEN DISCH_THEN SUBST1_TAC THEN
 405   MATCH_ACCEPT_TAC NADD_EQ_REFL);;
 406
 407 let NADD_OF_NUM_EQ = prove
 408  (`!m n. (&m === &n) <=> (m = n)`,
 409   REPEAT GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[NADD_OF_NUM_WELLDEF] THEN
 410   REWRITE_TAC[nadd_eq; NADD_OF_NUM] THEN
 411   REWRITE_TAC[GSYM DIST_RMUL; BOUNDS_LINEAR_0; DIST_EQ_0]);;
 412
 413 (* ------------------------------------------------------------------------- *)
 414 (* Definition of (reflexive) ordering and the only special property needed.  *)
 415 (* ------------------------------------------------------------------------- *)
 416
 417 override_interface ("<<=",`nadd_le:nadd->nadd->bool`);;
 418
 419 let nadd_le = new_definition
 420   `x <<= y <=> ?B. !n. fn x n <= fn y n + B`;;
 421
 422 let NADD_LE_WELLDEF_LEMMA = prove
 423  (`!x x' y y'. x === x' /\ y === y' /\ x <<= y ==> x' <<= y'`,
 424   REPEAT GEN_TAC THEN REWRITE_TAC[nadd_eq; nadd_le] THEN
 425   REWRITE_TAC[DIST_LE_CASES; FORALL_AND_THM] THEN
 426   DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `B1:num`) MP_TAC) THEN
 427   DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `B2:num`) MP_TAC) THEN
 428   DISCH_THEN(X_CHOOSE_TAC `B:num`) THEN
 429   EXISTS_TAC `(B2 + B) + B1` THEN X_GEN_TAC `n:num` THEN
 430   FIRST_ASSUM(MATCH_MP_TAC o LE_IMP o CONJUNCT2) THEN
 431   REWRITE_TAC[ADD_ASSOC; LE_ADD_RCANCEL] THEN
 432   FIRST_ASSUM(MATCH_MP_TAC o LE_IMP) THEN ASM_REWRITE_TAC[LE_ADD_RCANCEL]);;
 433
 434 let NADD_LE_WELLDEF = prove
 435  (`!x x' y y'. x === x' /\ y === y' ==> (x <<= y <=> x' <<= y')`,
 436   REPEAT STRIP_TAC THEN EQ_TAC THEN DISCH_TAC THEN
 437   MATCH_MP_TAC NADD_LE_WELLDEF_LEMMA THEN ASM_REWRITE_TAC[] THENL
 438    [MAP_EVERY EXISTS_TAC [`x:nadd`; `y:nadd`];
 439     MAP_EVERY EXISTS_TAC [`x':nadd`; `y':nadd`] THEN
 440     ONCE_REWRITE_TAC[NADD_EQ_SYM]] THEN
 441   ASM_REWRITE_TAC[]);;
 442
 443 let NADD_LE_REFL = prove
 444  (`!x. x <<= x`,
 445   REWRITE_TAC[nadd_le; LE_ADD]);;
 446
 447 let NADD_LE_TRANS = prove
 448  (`!x y z. x <<= y /\ y <<= z ==> x <<= z`,
 449   REPEAT GEN_TAC THEN REWRITE_TAC[nadd_le] THEN
 450   DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `B1:num`) MP_TAC) THEN
 451   DISCH_THEN(X_CHOOSE_TAC `B2:num`) THEN
 452   EXISTS_TAC `B2 + B1` THEN GEN_TAC THEN
 453   FIRST_ASSUM(MATCH_MP_TAC o LE_IMP) THEN
 454   ASM_REWRITE_TAC[ADD_ASSOC; LE_ADD_RCANCEL]);;
 455
 456 let NADD_LE_ANTISYM = prove
 457  (`!x y. x <<= y /\ y <<= x <=> (x === y)`,
 458   REPEAT GEN_TAC THEN REWRITE_TAC[nadd_le; nadd_eq; DIST_LE_CASES] THEN
 459   EQ_TAC THENL
 460    [DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `B1:num`)
 461       (X_CHOOSE_TAC `B2:num`)) THEN
 462     EXISTS_TAC `B1 + B2` THEN GEN_TAC THEN CONJ_TAC THEN
 463     FIRST_ASSUM(MATCH_MP_TAC o LE_IMP) THEN
 464     ASM_REWRITE_TAC[ADD_ASSOC; LE_ADD_RCANCEL; LE_ADD; LE_ADDR];
 465     DISCH_THEN(X_CHOOSE_TAC `B:num`) THEN
 466     CONJ_TAC THEN EXISTS_TAC `B:num` THEN ASM_REWRITE_TAC[]]);;
 467
 468 let NADD_LE_TOTAL_LEMMA = prove
 469  (`!x y. ~(x <<= y) ==> !B. ?n. ~(n = 0) /\ fn y n + B < fn x n`,
 470   REPEAT GEN_TAC THEN REWRITE_TAC[nadd_le; NOT_FORALL_THM; NOT_EXISTS_THM] THEN
 471   REWRITE_TAC[NOT_LE] THEN DISCH_TAC THEN GEN_TAC THEN
 472   POP_ASSUM(X_CHOOSE_TAC `n:num` o SPEC `B + fn x 0`) THEN
 473   EXISTS_TAC `n:num` THEN POP_ASSUM MP_TAC THEN
 474   ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[NOT_LT; ADD_ASSOC; LE_ADDR] THEN
 475   CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[NOT_LT] THEN
 476   DISCH_THEN(MATCH_MP_TAC o LE_IMP) THEN REWRITE_TAC[ADD_ASSOC; LE_ADD]);;
 477
 478 let NADD_LE_TOTAL = prove
 479  (`!x y. x <<= y \/ y <<= x`,
 480   REPEAT GEN_TAC THEN GEN_REWRITE_TAC I [TAUT `a <=> ~ ~ a`] THEN
 481   X_CHOOSE_TAC `B1:num` (SPEC `x:nadd` NADD_CAUCHY) THEN
 482   X_CHOOSE_TAC `B2:num` (SPEC `y:nadd` NADD_CAUCHY) THEN
 483   PURE_ONCE_REWRITE_TAC[DE_MORGAN_THM] THEN
 484   DISCH_THEN(MP_TAC o end_itlist CONJ o
 485     map (MATCH_MP NADD_LE_TOTAL_LEMMA) o CONJUNCTS) THEN
 486   REWRITE_TAC[AND_FORALL_THM] THEN DISCH_THEN(MP_TAC o SPEC `B1 + B2`) THEN
 487   REWRITE_TAC[RIGHT_AND_EXISTS_THM] THEN REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
 488   DISCH_THEN(X_CHOOSE_THEN `m:num` (X_CHOOSE_THEN `n:num` MP_TAC)) THEN
 489   DISCH_THEN(MP_TAC o MATCH_MP
 490     (ITAUT `(~a /\ b) /\ (~c /\ d) ==> ~(c \/ ~b) /\ ~(a \/ ~d)`)) THEN
 491   REWRITE_TAC[NOT_LT; GSYM LE_MULT_LCANCEL] THEN REWRITE_TAC[NOT_LE] THEN
 492   DISCH_THEN(MP_TAC o MATCH_MP LT_ADD2) THEN REWRITE_TAC[NOT_LT] THEN
 493   REWRITE_TAC[LEFT_ADD_DISTRIB] THEN
 494   ONCE_REWRITE_TAC[AC ADD_AC
 495     `(a + b + c) + (d + e + f) = (d + b + e) + (a + c + f)`] THEN
 496   MATCH_MP_TAC LE_ADD2 THEN REWRITE_TAC[GSYM RIGHT_ADD_DISTRIB] THEN
 497   CONJ_TAC THEN GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [MULT_SYM] THEN
 498   RULE_ASSUM_TAC(REWRITE_RULE[DIST_LE_CASES]) THEN ASM_REWRITE_TAC[]);;
 499
 500 let NADD_ARCH = prove
 501  (`!x. ?n. x <<= &n`,
 502   REWRITE_TAC[nadd_le; NADD_OF_NUM; NADD_BOUND]);;
 503
 504 let NADD_OF_NUM_LE = prove
 505  (`!m n. (&m <<= &n) <=> m <= n`,
 506   REPEAT GEN_TAC THEN REWRITE_TAC[nadd_le; NADD_OF_NUM] THEN
 507   REWRITE_TAC[BOUNDS_LINEAR]);;
 508
 509 (* ------------------------------------------------------------------------- *)
 510 (* Addition.                                                                 *)
 511 (* ------------------------------------------------------------------------- *)
 512
 513 override_interface ("++",`nadd_add:nadd->nadd->nadd`);;
 514
 515 let nadd_add = new_definition
 516   `x ++ y = afn(\n. fn x n + fn y n)`;;
 517
 518 let NADD_ADD = prove
 519  (`!x y. fn(x ++ y) = \n. fn x n + fn y n`,
 520   REPEAT GEN_TAC THEN
 521   REWRITE_TAC[nadd_add; GSYM nadd_rep; is_nadd] THEN
 522   X_CHOOSE_TAC `B1:num` (SPEC `x:nadd` NADD_CAUCHY) THEN
 523   X_CHOOSE_TAC `B2:num` (SPEC `y:nadd` NADD_CAUCHY) THEN
 524   EXISTS_TAC `B1 + B2` THEN MAP_EVERY X_GEN_TAC [`m:num`; `n:num`] THEN
 525   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [LEFT_ADD_DISTRIB] THEN
 526   MATCH_MP_TAC (LE_IMP DIST_ADD2) THEN REWRITE_TAC[RIGHT_ADD_DISTRIB] THEN
 527   MATCH_MP_TAC LE_ADD2 THEN ASM_REWRITE_TAC[]);;
 528
 529 let NADD_ADD_WELLDEF = prove
 530  (`!x x' y y'. x === x' /\ y === y' ==> (x ++ y === x' ++ y')`,
 531   REPEAT GEN_TAC THEN REWRITE_TAC[nadd_eq; NADD_ADD] THEN
 532   DISCH_THEN(CONJUNCTS_THEN2
 533     (X_CHOOSE_TAC `B1:num`) (X_CHOOSE_TAC `B2:num`)) THEN
 534   EXISTS_TAC `B1 + B2` THEN X_GEN_TAC `n:num` THEN
 535   MATCH_MP_TAC (LE_IMP DIST_ADD2) THEN
 536   MATCH_MP_TAC LE_ADD2 THEN ASM_REWRITE_TAC[]);;
 537
 538 (* ------------------------------------------------------------------------- *)
 539 (* Basic properties of addition.                                             *)
 540 (* ------------------------------------------------------------------------- *)
 541
 542 let NADD_ADD_SYM = prove
 543  (`!x y. (x ++ y) === (y ++ x)`,
 544   REPEAT GEN_TAC THEN REWRITE_TAC[nadd_add] THEN
 545   GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [ADD_SYM] THEN
 546   REWRITE_TAC[NADD_EQ_REFL]);;
 547
 548 let NADD_ADD_ASSOC = prove
 549  (`!x y z. (x ++ (y ++ z)) === ((x ++ y) ++ z)`,
 550   REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[nadd_add] THEN
 551   REWRITE_TAC[NADD_ADD; ADD_ASSOC; NADD_EQ_REFL]);;
 552
 553 let NADD_ADD_LID = prove
 554  (`!x. (&0 ++ x) === x`,
 555   GEN_TAC THEN REWRITE_TAC[nadd_eq; NADD_ADD; NADD_OF_NUM] THEN
 556   REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES; DIST_REFL; LE_0]);;
 557
 558 let NADD_ADD_LCANCEL = prove
 559  (`!x y z. (x ++ y) === (x ++ z) ==> y === z`,
 560   REPEAT GEN_TAC THEN REWRITE_TAC[nadd_eq; NADD_ADD; DIST_LADD]);;
 561
 562 let NADD_LE_ADD = prove
 563  (`!x y. x <<= (x ++ y)`,
 564   REPEAT GEN_TAC THEN REWRITE_TAC[nadd_le; NADD_ADD] THEN
 565   EXISTS_TAC `0` THEN REWRITE_TAC[ADD_CLAUSES; LE_ADD]);;
 566
 567 let NADD_LE_EXISTS = prove
 568  (`!x y. x <<= y ==> ?d. y === x ++ d`,
 569   REPEAT GEN_TAC THEN REWRITE_TAC[nadd_le] THEN
 570   DISCH_THEN(X_CHOOSE_THEN `B:num` MP_TAC) THEN
 571   REWRITE_TAC[LE_EXISTS; SKOLEM_THM] THEN
 572   DISCH_THEN(X_CHOOSE_THEN `d:num->num` (ASSUME_TAC o GSYM)) THEN
 573   EXISTS_TAC `afn d` THEN REWRITE_TAC[nadd_eq; NADD_ADD] THEN
 574   EXISTS_TAC `B:num` THEN X_GEN_TAC `n:num` THEN
 575   SUBGOAL_THEN `fn(afn d) = d` SUBST1_TAC THENL
 576    [REWRITE_TAC[GSYM nadd_rep; is_nadd] THEN
 577     X_CHOOSE_TAC `B1:num` (SPEC `x:nadd` NADD_CAUCHY) THEN
 578     X_CHOOSE_TAC `B2:num` (SPEC `y:nadd` NADD_CAUCHY) THEN
 579     EXISTS_TAC `B1 + (B2 + B)` THEN REPEAT GEN_TAC THEN
 580     MATCH_MP_TAC(LE_IMP DIST_ADD2_REV) THEN
 581     MAP_EVERY EXISTS_TAC [`m * fn x n`; `n * fn x m`] THEN
 582     ONCE_REWRITE_TAC[RIGHT_ADD_DISTRIB] THEN
 583     GEN_REWRITE_TAC RAND_CONV [ADD_SYM] THEN
 584     MATCH_MP_TAC LE_ADD2 THEN ASM_REWRITE_TAC[] THEN
 585     ONCE_REWRITE_TAC[ADD_SYM] THEN
 586     ASM_REWRITE_TAC[GSYM LEFT_ADD_DISTRIB] THEN
 587     GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [LEFT_ADD_DISTRIB] THEN
 588     MATCH_MP_TAC(LE_IMP DIST_ADD2) THEN REWRITE_TAC[RIGHT_ADD_DISTRIB] THEN
 589     GEN_REWRITE_TAC RAND_CONV [ADD_SYM] THEN MATCH_MP_TAC LE_ADD2 THEN
 590     ONCE_REWRITE_TAC[ADD_SYM] THEN ASM_REWRITE_TAC[] THEN
 591     GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [MULT_SYM] THEN
 592     REWRITE_TAC[GSYM DIST_LMUL; DIST_ADDBOUND; LE_MULT_LCANCEL];
 593     ASM_REWRITE_TAC[DIST_RADD_0; LE_REFL]]);;
 594
 595 let NADD_OF_NUM_ADD = prove
 596  (`!m n. &m ++ &n === &(m + n)`,
 597   REWRITE_TAC[nadd_eq; NADD_OF_NUM; NADD_ADD] THEN
 598   REWRITE_TAC[RIGHT_ADD_DISTRIB; DIST_REFL; LE_0]);;
 599
 600 (* ------------------------------------------------------------------------- *)
 601 (* Multiplication.                                                           *)
 602 (* ------------------------------------------------------------------------- *)
 603
 604 override_interface ("**",`nadd_mul:nadd->nadd->nadd`);;
 605
 606 let nadd_mul = new_definition
 607   `x ** y = afn(\n. fn x (fn y n))`;;
 608
 609 let NADD_MUL = prove
 610  (`!x y. fn(x ** y) = \n. fn x (fn y n)`,
 611   REPEAT GEN_TAC THEN
 612   REWRITE_TAC[nadd_mul; GSYM nadd_rep; is_nadd] THEN
 613   X_CHOOSE_TAC `B:num` (SPEC `y:nadd` NADD_CAUCHY) THEN
 614   X_CHOOSE_TAC `C:num` (SPEC `x:nadd` NADD_DIST) THEN
 615   X_CHOOSE_TAC `D:num` (SPEC `x:nadd` NADD_MULTIPLICATIVE) THEN
 616   MATCH_MP_TAC BOUNDS_NOTZERO THEN
 617   REWRITE_TAC[MULT_CLAUSES; DIST_REFL] THEN
 618   MAP_EVERY EXISTS_TAC [`D + C * B`; `D + D`] THEN
 619   REPEAT GEN_TAC THEN MATCH_MP_TAC LE_TRANS THEN
 620   EXISTS_TAC `(D * m + D) + (D * n + D) + C * B * (m + n)` THEN CONJ_TAC THENL
 621    [MATCH_MP_TAC (LE_IMP DIST_TRIANGLE) THEN
 622     EXISTS_TAC `fn x (m * fn y n)` THEN
 623     MATCH_MP_TAC LE_ADD2 THEN
 624     ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[] THEN
 625     MATCH_MP_TAC (LE_IMP DIST_TRIANGLE) THEN
 626     EXISTS_TAC `fn x (n * fn y m)` THEN
 627     MATCH_MP_TAC LE_ADD2 THEN
 628     ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[] THEN
 629     MATCH_MP_TAC LE_TRANS THEN
 630     EXISTS_TAC `C * dist(m * fn y n,n * fn y m)` THEN
 631     ASM_REWRITE_TAC[LE_MULT_LCANCEL];
 632     MATCH_MP_TAC EQ_IMP_LE THEN
 633     REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB; MULT_ASSOC; ADD_AC]]);;
 634
 635 (* ------------------------------------------------------------------------- *)
 636 (* Properties of multiplication.                                             *)
 637 (* ------------------------------------------------------------------------- *)
 638
 639 let NADD_MUL_SYM = prove
 640  (`!x y. (x ** y) === (y ** x)`,
 641   REPEAT GEN_TAC THEN REWRITE_TAC[nadd_eq; NADD_MUL] THEN
 642   X_CHOOSE_THEN `A1:num` MP_TAC (SPECL [`x:nadd`; `y:nadd`] NADD_ALTMUL) THEN
 643   DISCH_THEN(X_CHOOSE_TAC `B1:num`) THEN
 644   X_CHOOSE_THEN `A2:num` MP_TAC (SPECL [`y:nadd`; `x:nadd`] NADD_ALTMUL) THEN
 645   DISCH_THEN(X_CHOOSE_TAC `B2:num`) THEN REWRITE_TAC[BOUNDS_DIVIDED] THEN
 646   REWRITE_TAC[DIST_LMUL] THEN MAP_EVERY EXISTS_TAC [`A1 + A2`; `B1 + B2`] THEN
 647   GEN_TAC THEN REWRITE_TAC[RIGHT_ADD_DISTRIB] THEN
 648   ONCE_REWRITE_TAC[AC ADD_AC `(a + b) + (c + d) = (a + c) + (b + d)`] THEN
 649   MATCH_MP_TAC (LE_IMP DIST_TRIANGLE) THEN
 650   EXISTS_TAC `fn x n * fn y n` THEN
 651   MATCH_MP_TAC LE_ADD2 THEN ASM_REWRITE_TAC[] THEN
 652   ONCE_REWRITE_TAC [DIST_SYM] THEN
 653   GEN_REWRITE_TAC (LAND_CONV o funpow 2 RAND_CONV) [MULT_SYM] THEN
 654   ASM_REWRITE_TAC[]);;
 655
 656 let NADD_MUL_ASSOC = prove
 657  (`!x y z. (x ** (y ** z)) === ((x ** y) ** z)`,
 658   REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[nadd_mul] THEN
 659   REWRITE_TAC[NADD_MUL; NADD_EQ_REFL]);;
 660
 661 let NADD_MUL_LID = prove
 662  (`!x. (&1 ** x) === x`,
 663   REWRITE_TAC[NADD_OF_NUM; nadd_mul; MULT_CLAUSES] THEN
 664   REWRITE_TAC[nadd_abs; NADD_EQ_REFL; ETA_AX]);;
 665
 666 let NADD_LDISTRIB = prove
 667  (`!x y z. x ** (y ++ z) === (x ** y) ++ (x ** z)`,
 668   REPEAT GEN_TAC THEN REWRITE_TAC[nadd_eq] THEN
 669   REWRITE_TAC[NADD_ADD; NADD_MUL] THEN
 670   X_CHOOSE_TAC `B:num` (SPEC `x:nadd` NADD_ADDITIVE) THEN
 671   EXISTS_TAC `B:num` THEN ASM_REWRITE_TAC[]);;
 672
 673 let NADD_MUL_WELLDEF_LEMMA = prove
 674  (`!x y y'. y === y' ==> (x ** y) === (x ** y')`,
 675   REPEAT GEN_TAC THEN REWRITE_TAC[nadd_eq; NADD_MUL] THEN
 676   DISCH_THEN(X_CHOOSE_TAC `B1:num`) THEN
 677   X_CHOOSE_TAC `B2:num` (SPEC `x:nadd` NADD_DIST) THEN
 678   EXISTS_TAC `B2 * B1` THEN X_GEN_TAC `n:num` THEN
 679   MATCH_MP_TAC LE_TRANS THEN
 680   EXISTS_TAC `B2 * dist(fn y n,fn y' n)` THEN
 681   ASM_REWRITE_TAC[LE_MULT_LCANCEL]);;
 682
 683 let NADD_MUL_WELLDEF = prove
 684  (`!x x' y y'. x === x' /\ y === y'
 685                ==> (x ** y) === (x' ** y')`,
 686   REPEAT GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC NADD_EQ_TRANS THEN
 687   EXISTS_TAC `x' ** y` THEN CONJ_TAC THENL
 688    [MATCH_MP_TAC NADD_EQ_TRANS THEN EXISTS_TAC `y ** x'` THEN
 689     REWRITE_TAC[NADD_MUL_SYM] THEN MATCH_MP_TAC NADD_EQ_TRANS THEN
 690     EXISTS_TAC `y ** x` THEN REWRITE_TAC[NADD_MUL_SYM]; ALL_TAC] THEN
 691   MATCH_MP_TAC NADD_MUL_WELLDEF_LEMMA THEN ASM_REWRITE_TAC[]);;
 692
 693 let NADD_OF_NUM_MUL = prove
 694  (`!m n. &m ** &n === &(m * n)`,
 695   REWRITE_TAC[nadd_eq; NADD_OF_NUM; NADD_MUL] THEN
 696   REWRITE_TAC[MULT_ASSOC; DIST_REFL; LE_0]);;
 697
 698 (* ------------------------------------------------------------------------- *)
 699 (* A few handy lemmas.                                                       *)
 700 (* ------------------------------------------------------------------------- *)
 701
 702 let NADD_LE_0 = prove
 703  (`!x. &0 <<= x`,
 704   GEN_TAC THEN
 705   REWRITE_TAC[nadd_le; NADD_OF_NUM; MULT_CLAUSES; LE_0]);;
 706
 707 let NADD_EQ_IMP_LE = prove
 708  (`!x y. x === y ==> x <<= y`,
 709   REPEAT GEN_TAC THEN
 710   REWRITE_TAC[nadd_eq; nadd_le; DIST_LE_CASES] THEN
 711   DISCH_THEN(X_CHOOSE_TAC `B:num`) THEN EXISTS_TAC `B:num` THEN
 712   ASM_REWRITE_TAC[]);;
 713
 714 let NADD_LE_LMUL = prove
 715  (`!x y z. y <<= z ==> (x ** y) <<= (x ** z)`,
 716   REPEAT GEN_TAC THEN
 717   DISCH_THEN(X_CHOOSE_TAC `d:nadd` o MATCH_MP NADD_LE_EXISTS) THEN
 718   MATCH_MP_TAC NADD_LE_TRANS THEN
 719   EXISTS_TAC `x ** y ++ x ** d` THEN REWRITE_TAC[NADD_LE_ADD] THEN
 720   MATCH_MP_TAC NADD_EQ_IMP_LE THEN
 721   MATCH_MP_TAC NADD_EQ_TRANS THEN
 722   EXISTS_TAC `x ** (y ++ d)` THEN
 723   ONCE_REWRITE_TAC[NADD_EQ_SYM] THEN
 724   REWRITE_TAC[NADD_LDISTRIB] THEN
 725   MATCH_MP_TAC NADD_MUL_WELLDEF THEN
 726   ASM_REWRITE_TAC[NADD_EQ_REFL]);;
 727
 728 let NADD_LE_RMUL = prove
 729  (`!x y z. x <<= y ==> (x ** z) <<= (y ** z)`,
 730   MESON_TAC[NADD_LE_LMUL; NADD_LE_WELLDEF; NADD_MUL_SYM]);;
 731
 732 let NADD_LE_RADD = prove
 733  (`!x y z. x ++ z <<= y ++ z <=> x <<= y`,
 734   REPEAT GEN_TAC THEN REWRITE_TAC[nadd_le; NADD_ADD] THEN
 735   GEN_REWRITE_TAC (LAND_CONV o funpow 2 BINDER_CONV o RAND_CONV)
 736     [ADD_SYM] THEN
 737   REWRITE_TAC[ADD_ASSOC; LE_ADD_RCANCEL] THEN
 738   GEN_REWRITE_TAC (LAND_CONV o funpow 2 BINDER_CONV o RAND_CONV)
 739     [ADD_SYM] THEN REFL_TAC);;
 740
 741 let NADD_LE_LADD = prove
 742  (`!x y z. x ++ y <<= x ++ z <=> y <<= z`,
 743   MESON_TAC[NADD_LE_RADD; NADD_ADD_SYM; NADD_LE_WELLDEF]);;
 744
 745 let NADD_RDISTRIB = prove
 746  (`!x y z. (x ++ y) ** z === x ** z ++ y ** z`,
 747   MESON_TAC[NADD_LDISTRIB; NADD_MUL_SYM; NADD_ADD_WELLDEF;
 748     NADD_EQ_TRANS; NADD_EQ_REFL; NADD_EQ_SYM]);;
 749
 750 (* ------------------------------------------------------------------------- *)
 751 (* The Archimedean property in a more useful form.                           *)
 752 (* ------------------------------------------------------------------------- *)
 753
 754 let NADD_ARCH_MULT = prove
 755  (`!x k. ~(x === &0) ==> ?N. &k <<= &N ** x`,
 756   REPEAT GEN_TAC THEN REWRITE_TAC[nadd_eq; nadd_le; NOT_EXISTS_THM] THEN
 757   X_CHOOSE_TAC `B:num` (SPEC `x:nadd` NADD_CAUCHY) THEN
 758   DISCH_THEN(MP_TAC o SPEC `B + k`) THEN
 759   REWRITE_TAC[NOT_FORALL_THM; NADD_OF_NUM] THEN
 760   REWRITE_TAC[MULT_CLAUSES; DIST_RZERO; NOT_LE] THEN
 761   DISCH_THEN(X_CHOOSE_TAC `N:num`) THEN
 762   MAP_EVERY EXISTS_TAC [`N:num`; `B * N`] THEN X_GEN_TAC `i:num` THEN
 763   REWRITE_TAC[NADD_MUL; NADD_OF_NUM] THEN
 764   MATCH_MP_TAC(GEN_ALL(fst(EQ_IMP_RULE(SPEC_ALL LE_ADD_RCANCEL)))) THEN
 765   EXISTS_TAC `B * i` THEN
 766   REWRITE_TAC[GSYM ADD_ASSOC; GSYM LEFT_ADD_DISTRIB] THEN
 767   MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `i * fn x N` THEN
 768   RULE_ASSUM_TAC(REWRITE_RULE[DIST_LE_CASES]) THEN ASM_REWRITE_TAC[] THEN
 769   REWRITE_TAC[GSYM RIGHT_ADD_DISTRIB] THEN
 770   GEN_REWRITE_TAC RAND_CONV [MULT_SYM] THEN
 771   REWRITE_TAC[LE_MULT_RCANCEL] THEN DISJ1_TAC THEN
 772   MATCH_MP_TAC LT_IMP_LE THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
 773   FIRST_ASSUM ACCEPT_TAC);;
 774
 775 let NADD_ARCH_ZERO = prove
 776  (`!x k. (!n. &n ** x <<= k) ==> (x === &0)`,
 777   REPEAT GEN_TAC THEN CONV_TAC CONTRAPOS_CONV THEN DISCH_TAC THEN
 778   REWRITE_TAC[NOT_FORALL_THM] THEN
 779   X_CHOOSE_TAC `p:num` (SPEC `k:nadd` NADD_ARCH) THEN
 780   FIRST_ASSUM(MP_TAC o MATCH_MP NADD_ARCH_MULT) THEN
 781   DISCH_THEN(X_CHOOSE_TAC `N:num` o SPEC `p:num`) THEN
 782   EXISTS_TAC `N + 1` THEN DISCH_TAC THEN UNDISCH_TAC `~(x === &0)` THEN
 783   REWRITE_TAC[GSYM NADD_LE_ANTISYM; NADD_LE_0] THEN
 784   MATCH_MP_TAC(GEN_ALL(fst(EQ_IMP_RULE(SPEC_ALL NADD_LE_RADD)))) THEN
 785   EXISTS_TAC `&N ** x` THEN MATCH_MP_TAC NADD_LE_TRANS THEN
 786   EXISTS_TAC `k:nadd` THEN CONJ_TAC THENL
 787    [SUBGOAL_THEN `&(N + 1) ** x === x ++ &N ** x` MP_TAC THENL
 788      [ONCE_REWRITE_TAC[ADD_SYM] THEN
 789       MATCH_MP_TAC NADD_EQ_TRANS THEN
 790       EXISTS_TAC `&1 ** x ++ &N ** x` THEN CONJ_TAC THENL
 791        [MATCH_MP_TAC NADD_EQ_TRANS THEN
 792         EXISTS_TAC `(&1 ++ &N) ** x` THEN CONJ_TAC THENL
 793          [MESON_TAC[NADD_OF_NUM_ADD; NADD_MUL_WELLDEF; NADD_EQ_REFL;
 794             NADD_EQ_SYM];
 795           MESON_TAC[NADD_RDISTRIB; NADD_MUL_SYM; NADD_EQ_SYM; NADD_EQ_TRANS]];
 796         MESON_TAC[NADD_ADD_WELLDEF; NADD_EQ_REFL; NADD_MUL_LID]];
 797       ASM_MESON_TAC[NADD_LE_WELLDEF; NADD_EQ_REFL]];
 798     ASM_MESON_TAC[NADD_LE_TRANS; NADD_LE_WELLDEF; NADD_EQ_REFL;
 799       NADD_ADD_LID]]);;
 800
 801 let NADD_ARCH_LEMMA = prove
 802  (`!x y z. (!n. &n ** x <<= &n ** y ++ z) ==> x <<= y`,
 803   REPEAT STRIP_TAC THEN
 804   DISJ_CASES_TAC(SPECL [`x:nadd`; `y:nadd`] NADD_LE_TOTAL) THEN
 805   ASM_REWRITE_TAC[] THEN
 806   FIRST_ASSUM(X_CHOOSE_TAC `d:nadd` o MATCH_MP NADD_LE_EXISTS) THEN
 807   MATCH_MP_TAC NADD_EQ_IMP_LE THEN
 808   MATCH_MP_TAC NADD_EQ_TRANS THEN EXISTS_TAC `y ++ d` THEN
 809   ASM_REWRITE_TAC[] THEN
 810   MATCH_MP_TAC NADD_EQ_TRANS THEN EXISTS_TAC `y ++ &0` THEN CONJ_TAC THENL
 811    [MATCH_MP_TAC NADD_ADD_WELLDEF THEN REWRITE_TAC[NADD_EQ_REFL] THEN
 812     MATCH_MP_TAC NADD_ARCH_ZERO THEN EXISTS_TAC `z:nadd` THEN
 813     ASM_MESON_TAC[NADD_MUL_WELLDEF; NADD_LE_WELLDEF; NADD_LDISTRIB;
 814       NADD_LE_LADD; NADD_EQ_REFL];
 815     ASM_MESON_TAC[NADD_ADD_LID; NADD_ADD_WELLDEF; NADD_EQ_TRANS;
 816       NADD_ADD_SYM]]);;
 817
 818 (* ------------------------------------------------------------------------- *)
 819 (* Completeness.                                                             *)
 820 (* ------------------------------------------------------------------------- *)
 821
 822 let NADD_COMPLETE = prove
 823  (`!P. (?x. P x) /\ (?M. !x. P x ==> x <<= M) ==>
 824        ?M. (!x. P x ==> x <<= M) /\
 825            !M'. (!x. P x ==> x <<= M') ==> M <<= M'`,
 826   GEN_TAC THEN DISCH_THEN
 827     (CONJUNCTS_THEN2 (X_CHOOSE_TAC `a:nadd`) (X_CHOOSE_TAC `m:nadd`)) THEN
 828   SUBGOAL_THEN
 829     `!n. ?r. (?x. P x /\ &r <<= &n ** x) /\
 830              !r'. (?x. P x /\ &r' <<= &n ** x) ==> r' <= r` MP_TAC THENL
 831    [GEN_TAC THEN REWRITE_TAC[GSYM num_MAX] THEN CONJ_TAC THENL
 832      [MAP_EVERY EXISTS_TAC [`0`; `a:nadd`] THEN ASM_REWRITE_TAC[NADD_LE_0];
 833       X_CHOOSE_TAC `N:num` (SPEC `m:nadd` NADD_ARCH) THEN
 834       EXISTS_TAC `n * N` THEN X_GEN_TAC `p:num` THEN
 835       DISCH_THEN(X_CHOOSE_THEN `w:nadd` STRIP_ASSUME_TAC) THEN
 836       ONCE_REWRITE_TAC[GSYM NADD_OF_NUM_LE] THEN
 837       MATCH_MP_TAC NADD_LE_TRANS THEN EXISTS_TAC `&n ** w` THEN
 838       ASM_REWRITE_TAC[] THEN MATCH_MP_TAC NADD_LE_TRANS THEN
 839       EXISTS_TAC `&n ** &N` THEN CONJ_TAC THENL
 840        [MATCH_MP_TAC NADD_LE_LMUL THEN MATCH_MP_TAC NADD_LE_TRANS THEN
 841         EXISTS_TAC `m:nadd` THEN ASM_REWRITE_TAC[] THEN
 842         FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
 843         MATCH_MP_TAC NADD_EQ_IMP_LE THEN
 844         MATCH_ACCEPT_TAC NADD_OF_NUM_MUL]];
 845     ONCE_REWRITE_TAC[SKOLEM_THM] THEN
 846     DISCH_THEN(X_CHOOSE_THEN `r:num->num`
 847      (fun th -> let th1,th2 = CONJ_PAIR(SPEC `n:num` th) in
 848                 MAP_EVERY (MP_TAC o GEN `n:num`) [th1; th2])) THEN
 849     DISCH_THEN(MP_TAC o GEN `n:num` o SPECL [`n:num`; `SUC(r(n:num))`]) THEN
 850     REWRITE_TAC[LE_SUC_LT; LT_REFL; NOT_EXISTS_THM] THEN
 851     DISCH_THEN(ASSUME_TAC o GENL [`n:num`; `x:nadd`] o MATCH_MP
 852      (ITAUT `(a \/ b) /\ ~(c /\ b) ==> c ==> a`) o CONJ
 853       (SPECL [`&n ** x`; `&(SUC(r(n:num)))`] NADD_LE_TOTAL) o SPEC_ALL) THEN
 854     DISCH_TAC] THEN
 855   SUBGOAL_THEN `!n i. i * r(n) <= n * r(i) + n` ASSUME_TAC THENL
 856    [REPEAT GEN_TAC THEN
 857     FIRST_ASSUM(X_CHOOSE_THEN `x:nadd` STRIP_ASSUME_TAC o SPEC `n:num`) THEN
 858     ONCE_REWRITE_TAC[GSYM NADD_OF_NUM_LE] THEN
 859     MATCH_MP_TAC NADD_LE_TRANS THEN
 860     EXISTS_TAC `&i ** &n ** x` THEN CONJ_TAC THENL
 861      [MATCH_MP_TAC NADD_LE_TRANS THEN
 862       EXISTS_TAC `&i ** &(r(n:num))` THEN CONJ_TAC THENL
 863        [MATCH_MP_TAC NADD_EQ_IMP_LE THEN
 864         ONCE_REWRITE_TAC[NADD_EQ_SYM] THEN MATCH_ACCEPT_TAC NADD_OF_NUM_MUL;
 865         MATCH_MP_TAC NADD_LE_LMUL THEN ASM_REWRITE_TAC[]];
 866       MATCH_MP_TAC NADD_LE_TRANS THEN
 867       EXISTS_TAC `&n ** &(SUC(r(i:num)))` THEN CONJ_TAC THENL
 868        [MATCH_MP_TAC NADD_LE_TRANS THEN EXISTS_TAC `&n ** &i ** x` THEN
 869         CONJ_TAC THENL
 870          [MATCH_MP_TAC NADD_EQ_IMP_LE THEN
 871           MATCH_MP_TAC NADD_EQ_TRANS THEN
 872           EXISTS_TAC `(&i ** &n) ** x` THEN
 873           REWRITE_TAC[NADD_MUL_ASSOC] THEN
 874           MATCH_MP_TAC NADD_EQ_TRANS THEN
 875           EXISTS_TAC `(&n ** &i) ** x` THEN
 876           REWRITE_TAC[ONCE_REWRITE_RULE[NADD_EQ_SYM] NADD_MUL_ASSOC] THEN
 877           MATCH_MP_TAC NADD_MUL_WELLDEF THEN
 878           REWRITE_TAC[NADD_MUL_SYM; NADD_EQ_REFL];
 879           MATCH_MP_TAC NADD_LE_LMUL THEN
 880           FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]];
 881         ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[GSYM MULT_SUC] THEN
 882         MATCH_MP_TAC NADD_EQ_IMP_LE THEN
 883         REWRITE_TAC[NADD_OF_NUM_MUL]]]; ALL_TAC] THEN
 884   EXISTS_TAC `afn r` THEN SUBGOAL_THEN `fn(afn r) = r` ASSUME_TAC THENL
 885    [REWRITE_TAC[GSYM nadd_rep] THEN REWRITE_TAC[is_nadd; DIST_LE_CASES] THEN
 886     EXISTS_TAC `1` THEN REWRITE_TAC[MULT_CLAUSES] THEN
 887     REWRITE_TAC[FORALL_AND_THM] THEN
 888     GEN_REWRITE_TAC RAND_CONV [SWAP_FORALL_THM] THEN
 889     GEN_REWRITE_TAC (LAND_CONV o funpow 2 BINDER_CONV o
 890       funpow 2 RAND_CONV) [ADD_SYM] THEN
 891     REWRITE_TAC[] THEN MAP_EVERY X_GEN_TAC [`i:num`; `n:num`] THEN
 892     MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `n * r(i:num) + n` THEN
 893     ASM_REWRITE_TAC[ADD_ASSOC; LE_ADD]; ALL_TAC] THEN
 894   CONJ_TAC THENL
 895    [X_GEN_TAC `x:nadd` THEN DISCH_TAC THEN
 896     MATCH_MP_TAC NADD_ARCH_LEMMA THEN
 897     EXISTS_TAC `&2` THEN X_GEN_TAC `n:num` THEN
 898     MATCH_MP_TAC NADD_LE_TRANS THEN
 899     EXISTS_TAC `&(SUC(r(n:num)))` THEN CONJ_TAC THENL
 900      [FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
 901       ASM_REWRITE_TAC[nadd_le; NADD_ADD; NADD_MUL; NADD_OF_NUM] THEN
 902       ONCE_REWRITE_TAC[ADD_SYM] THEN
 903       REWRITE_TAC[ADD1; RIGHT_ADD_DISTRIB] THEN
 904       REWRITE_TAC[MULT_2; MULT_CLAUSES; ADD_ASSOC; LE_ADD_RCANCEL] THEN
 905       REWRITE_TAC[GSYM ADD_ASSOC] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
 906       ONCE_REWRITE_TAC[BOUNDS_IGNORE] THEN
 907       MAP_EVERY EXISTS_TAC [`0`; `n:num`] THEN
 908       X_GEN_TAC `i:num` THEN DISCH_TAC THEN
 909       GEN_REWRITE_TAC LAND_CONV [MULT_SYM] THEN
 910       MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `n * r(i:num) + n` THEN
 911       ASM_REWRITE_TAC[LE_ADD_LCANCEL; ADD_CLAUSES]];
 912     X_GEN_TAC `z:nadd` THEN DISCH_TAC THEN
 913     MATCH_MP_TAC NADD_ARCH_LEMMA THEN EXISTS_TAC `&1` THEN
 914     X_GEN_TAC `n:num` THEN MATCH_MP_TAC NADD_LE_TRANS THEN
 915     EXISTS_TAC `&(r(n:num)) ++ &1` THEN CONJ_TAC THENL
 916      [ASM_REWRITE_TAC[nadd_le; NADD_ADD; NADD_MUL; NADD_OF_NUM] THEN
 917       EXISTS_TAC `0` THEN REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES] THEN
 918       GEN_TAC THEN GEN_REWRITE_TAC (RAND_CONV o LAND_CONV) [MULT_SYM] THEN
 919       ASM_REWRITE_TAC[];
 920       REWRITE_TAC[NADD_LE_RADD] THEN
 921       FIRST_ASSUM(X_CHOOSE_THEN `x:nadd` MP_TAC o SPEC `n:num`) THEN
 922       DISCH_THEN STRIP_ASSUME_TAC THEN
 923       MATCH_MP_TAC NADD_LE_TRANS THEN EXISTS_TAC `&n ** x` THEN
 924       ASM_REWRITE_TAC[] THEN MATCH_MP_TAC NADD_LE_LMUL THEN
 925       FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]]]);;
 926
 927 (* ------------------------------------------------------------------------- *)
 928 (* A bit more on nearly-multiplicative functions.                            *)
 929 (* ------------------------------------------------------------------------- *)
 930
 931 let NADD_UBOUND = prove
 932  (`!x. ?B N. !n. N <= n ==> fn x n <= B * n`,
 933   GEN_TAC THEN X_CHOOSE_THEN `A1:num`
 934     (X_CHOOSE_TAC `A2:num`) (SPEC `x:nadd` NADD_BOUND) THEN
 935   EXISTS_TAC `A1 + A2` THEN EXISTS_TAC `1` THEN
 936   REPEAT STRIP_TAC THEN MATCH_MP_TAC LE_TRANS THEN
 937   EXISTS_TAC `A1 * n + A2` THEN ASM_REWRITE_TAC[] THEN
 938   REWRITE_TAC[RIGHT_ADD_DISTRIB; LE_ADD_LCANCEL] THEN
 939   GEN_REWRITE_TAC LAND_CONV [GSYM(el 3 (CONJUNCTS MULT_CLAUSES))] THEN
 940   ASM_REWRITE_TAC[LE_MULT_LCANCEL]);;
 941
 942 let NADD_NONZERO = prove
 943  (`!x. ~(x === &0) ==> ?N. !n. N <= n ==> ~(fn x n = 0)`,
 944   GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP NADD_ARCH_MULT) THEN
 945   DISCH_THEN(MP_TAC o SPEC `1`) THEN
 946   REWRITE_TAC[nadd_le; NADD_MUL; NADD_OF_NUM; MULT_CLAUSES] THEN
 947   DISCH_THEN(X_CHOOSE_THEN `A1:num` (X_CHOOSE_TAC `A2:num`)) THEN
 948   EXISTS_TAC `A2 + 1` THEN X_GEN_TAC `n:num` THEN REPEAT DISCH_TAC THEN
 949   FIRST_ASSUM(UNDISCH_TAC o check is_forall o concl) THEN
 950   REWRITE_TAC[NOT_FORALL_THM; NOT_LE; GSYM LE_SUC_LT; ADD1] THEN
 951   EXISTS_TAC `n:num` THEN ASM_REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES]);;
 952
 953 let NADD_LBOUND = prove
 954  (`!x. ~(x === &0) ==> ?A N. !n. N <= n ==> n <= A * fn x n`,
 955   GEN_TAC THEN DISCH_TAC THEN
 956   FIRST_ASSUM(X_CHOOSE_TAC `N:num` o MATCH_MP NADD_NONZERO) THEN
 957   FIRST_ASSUM(MP_TAC o MATCH_MP NADD_ARCH_MULT) THEN
 958   DISCH_THEN(MP_TAC o SPEC `1`) THEN
 959   REWRITE_TAC[nadd_le; NADD_MUL; NADD_OF_NUM; MULT_CLAUSES] THEN
 960   DISCH_THEN(X_CHOOSE_THEN `A1:num` (X_CHOOSE_TAC `A2:num`)) THEN
 961   EXISTS_TAC `A1 + A2` THEN EXISTS_TAC `N:num` THEN GEN_TAC THEN
 962   DISCH_THEN(ANTE_RES_THEN ASSUME_TAC) THEN
 963   MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `A1 * fn x n + A2` THEN
 964   ASM_REWRITE_TAC[RIGHT_ADD_DISTRIB; LE_ADD_LCANCEL] THEN
 965   GEN_REWRITE_TAC LAND_CONV [GSYM(el 3 (CONJUNCTS MULT_CLAUSES))] THEN
 966   REWRITE_TAC[LE_MULT_LCANCEL] THEN DISJ2_TAC THEN
 967   REWRITE_TAC[GSYM(REWRITE_CONV[ARITH_SUC] `SUC 0`)] THEN
 968   ASM_REWRITE_TAC[GSYM NOT_LT; LT]);;
 969
 970 (* ------------------------------------------------------------------------- *)
 971 (* Auxiliary function for the multiplicative inverse.                        *)
 972 (* ------------------------------------------------------------------------- *)
 973
 974 let nadd_rinv = new_definition
 975  `nadd_rinv(x) = \n. (n * n) DIV (fn x n)`;;
 976
 977 let NADD_MUL_LINV_LEMMA0 = prove
 978  (`!x. ~(x === &0) ==> ?A B. !n. nadd_rinv x n <= A * n + B`,
 979   GEN_TAC THEN DISCH_TAC THEN ONCE_REWRITE_TAC[BOUNDS_IGNORE] THEN
 980   FIRST_ASSUM(MP_TAC o MATCH_MP NADD_LBOUND) THEN
 981   DISCH_THEN(X_CHOOSE_THEN `A:num` (X_CHOOSE_TAC `N:num`)) THEN
 982   MAP_EVERY EXISTS_TAC [`A:num`; `0`; `SUC N`] THEN
 983   GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[ADD_CLAUSES] THEN
 984   MP_TAC(SPECL [`nadd_rinv x n`; `A * n`; `n:num`] LE_MULT_RCANCEL) THEN
 985   UNDISCH_TAC `SUC N <= n` THEN ASM_CASES_TAC `n = 0` THEN
 986   ASM_REWRITE_TAC[LE; NOT_SUC] THEN DISCH_TAC THEN
 987   DISCH_THEN(SUBST1_TAC o SYM) THEN
 988   MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `nadd_rinv x n * A * fn x n` THEN
 989   ASM_REWRITE_TAC[LE_MULT_LCANCEL] THEN CONJ_TAC THENL
 990    [DISJ2_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN MATCH_MP_TAC LE_TRANS THEN
 991     EXISTS_TAC `SUC N` THEN ASM_REWRITE_TAC[LE; LE_REFL];
 992     GEN_REWRITE_TAC LAND_CONV [MULT_SYM] THEN
 993     REWRITE_TAC[GSYM MULT_ASSOC; LE_MULT_LCANCEL] THEN
 994     DISJ2_TAC THEN ASM_CASES_TAC `fn x n = 0` THEN
 995     ASM_REWRITE_TAC[MULT_CLAUSES; LE_0; nadd_rinv] THEN
 996     FIRST_ASSUM(MP_TAC o MATCH_MP DIVISION) THEN
 997     DISCH_THEN(fun t -> GEN_REWRITE_TAC RAND_CONV [CONJUNCT1(SPEC_ALL t)]) THEN
 998     GEN_REWRITE_TAC LAND_CONV [MULT_SYM] THEN REWRITE_TAC[LE_ADD]]);;
 999
1000 let NADD_MUL_LINV_LEMMA1 = prove
1001  (`!x n. ~(fn x n = 0) ==> dist(fn x n * nadd_rinv(x) n, n * n) <= fn x n`,
1002   REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP DIVISION) THEN
1003   DISCH_THEN(CONJUNCTS_THEN2 SUBST1_TAC ASSUME_TAC o SPEC `n * n`) THEN
1004   REWRITE_TAC[nadd_rinv] THEN
1005   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o LAND_CONV) [MULT_SYM] THEN
1006   REWRITE_TAC[DIST_RADD_0] THEN MATCH_MP_TAC LT_IMP_LE THEN
1007   FIRST_ASSUM MATCH_ACCEPT_TAC);;
1008
1009 let NADD_MUL_LINV_LEMMA2 = prove
1010  (`!x. ~(x === &0) ==> ?N. !n. N <= n ==>
1011          dist(fn x n * nadd_rinv(x) n, n * n) <= fn x n`,
1012   GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP NADD_NONZERO) THEN
1013   DISCH_THEN(X_CHOOSE_TAC `N:num`) THEN EXISTS_TAC `N:num` THEN
1014   REPEAT STRIP_TAC THEN MATCH_MP_TAC NADD_MUL_LINV_LEMMA1 THEN
1015   FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);;
1016
1017 let NADD_MUL_LINV_LEMMA3 = prove
1018  (`!x. ~(x === &0) ==> ?N. !m n. N <= n ==>
1019         dist(m * fn x m * fn x n * nadd_rinv(x) n,
1020              m * fn x m * n * n) <= m * fn x m * fn x n`,
1021   GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP NADD_MUL_LINV_LEMMA2) THEN
1022   DISCH_THEN(X_CHOOSE_TAC `N:num`) THEN EXISTS_TAC `N:num` THEN
1023   REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM DIST_LMUL; MULT_ASSOC] THEN
1024   REWRITE_TAC[LE_MULT_LCANCEL] THEN DISJ2_TAC THEN
1025   FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);;
1026
1027 let NADD_MUL_LINV_LEMMA4 = prove
1028  (`!x. ~(x === &0) ==> ?N. !m n. N <= m /\ N <= n ==>
1029         (fn x m * fn x n) * dist(m * nadd_rinv(x) n,n * nadd_rinv(x) m) <=
1030           (m * n) * dist(m * fn x n,n * fn x m) + (fn x m * fn x n) * (m + n)`,
1031   GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP NADD_MUL_LINV_LEMMA3) THEN
1032   DISCH_THEN(X_CHOOSE_TAC `N:num`) THEN EXISTS_TAC `N:num` THEN
1033   REPEAT STRIP_TAC THEN REWRITE_TAC[DIST_LMUL; LEFT_ADD_DISTRIB] THEN
1034   GEN_REWRITE_TAC (RAND_CONV o LAND_CONV) [DIST_SYM] THEN
1035   MATCH_MP_TAC DIST_TRIANGLES_LE THEN CONJ_TAC THENL
1036    [ANTE_RES_THEN(MP_TAC o SPEC `m:num`) (ASSUME `N <= n`);
1037     ANTE_RES_THEN(MP_TAC o SPEC `n:num`) (ASSUME `N <= m`)] THEN
1038   MATCH_MP_TAC EQ_IMP THEN REWRITE_TAC[MULT_AC]);;
1039
1040 let NADD_MUL_LINV_LEMMA5 = prove
1041  (`!x. ~(x === &0) ==> ?B N. !m n. N <= m /\ N <= n ==>
1042         (fn x m * fn x n) * dist(m * nadd_rinv(x) n,n * nadd_rinv(x) m) <=
1043         B * (m * n) * (m + n)`,
1044   GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP NADD_MUL_LINV_LEMMA4) THEN
1045   DISCH_THEN(X_CHOOSE_TAC `N1:num`) THEN
1046   X_CHOOSE_TAC `B1:num` (SPEC `x:nadd` NADD_CAUCHY) THEN
1047   X_CHOOSE_THEN `B2:num` (X_CHOOSE_TAC `N2:num`)
1048     (SPEC `x:nadd` NADD_UBOUND) THEN
1049   EXISTS_TAC `B1 + B2 * B2` THEN EXISTS_TAC `N1 + N2` THEN
1050   REPEAT STRIP_TAC THEN MATCH_MP_TAC LE_TRANS THEN
1051   EXISTS_TAC `(m * n) * dist(m * fn x n,n * fn x m) +
1052               (fn x m * fn x n) * (m + n)` THEN
1053   CONJ_TAC THENL
1054    [FIRST_ASSUM MATCH_MP_TAC THEN CONJ_TAC THEN
1055     MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `N1 + N2` THEN
1056     ASM_REWRITE_TAC[LE_ADD; LE_ADDR];
1057     REWRITE_TAC[RIGHT_ADD_DISTRIB] THEN MATCH_MP_TAC LE_ADD2] THEN
1058   CONJ_TAC THENL
1059    [GEN_REWRITE_TAC RAND_CONV [MULT_SYM] THEN
1060     GEN_REWRITE_TAC RAND_CONV [GSYM MULT_ASSOC] THEN
1061     GEN_REWRITE_TAC (funpow 2 RAND_CONV) [MULT_SYM] THEN
1062     ASM_REWRITE_TAC[LE_MULT_LCANCEL];
1063     ONCE_REWRITE_TAC[AC MULT_AC
1064       `(a * b) * (c * d) * e = ((a * c) * (b * d)) * e`] THEN
1065     REWRITE_TAC[LE_MULT_RCANCEL] THEN DISJ1_TAC THEN
1066     MATCH_MP_TAC LE_MULT2 THEN CONJ_TAC THEN
1067     FIRST_ASSUM MATCH_MP_TAC THEN
1068     MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `N1 + N2` THEN
1069     ASM_REWRITE_TAC[LE_ADD; LE_ADDR]]);;
1070
1071 let NADD_MUL_LINV_LEMMA6 = prove
1072  (`!x. ~(x === &0) ==> ?B N. !m n. N <= m /\ N <= n ==>
1073         (m * n) * dist(m * nadd_rinv(x) n,n * nadd_rinv(x) m) <=
1074         B * (m * n) * (m + n)`,
1075   GEN_TAC THEN DISCH_TAC THEN
1076   FIRST_ASSUM(MP_TAC o MATCH_MP NADD_MUL_LINV_LEMMA5) THEN
1077   DISCH_THEN(X_CHOOSE_THEN `B1:num` (X_CHOOSE_TAC `N1:num`)) THEN
1078   FIRST_ASSUM(MP_TAC o MATCH_MP NADD_LBOUND) THEN
1079   DISCH_THEN(X_CHOOSE_THEN `B2:num` (X_CHOOSE_TAC `N2:num`)) THEN
1080   EXISTS_TAC `B1 * B2 * B2` THEN EXISTS_TAC `N1 + N2` THEN
1081   REPEAT STRIP_TAC THEN MATCH_MP_TAC LE_TRANS THEN
1082   EXISTS_TAC `(B2 * B2) * (fn x m * fn x n) *
1083               dist (m * nadd_rinv x n,n * nadd_rinv x m)` THEN
1084   CONJ_TAC THENL
1085    [REWRITE_TAC[MULT_ASSOC; LE_MULT_RCANCEL] THEN DISJ1_TAC THEN
1086     ONCE_REWRITE_TAC[AC MULT_AC `((a * b) * c) * d = (a * c) * (b * d)`] THEN
1087     MATCH_MP_TAC LE_MULT2 THEN CONJ_TAC THEN FIRST_ASSUM MATCH_MP_TAC;
1088     ONCE_REWRITE_TAC[AC MULT_AC
1089       `(a * b * c) * (d * e) * f = (b * c) * (a * (d * e) * f)`] THEN
1090     REWRITE_TAC[LE_MULT_LCANCEL] THEN DISJ2_TAC THEN
1091     FIRST_ASSUM MATCH_MP_TAC THEN CONJ_TAC] THEN
1092   MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `N1 + N2` THEN
1093   ASM_REWRITE_TAC[LE_ADD; LE_ADDR]);;
1094
1095 let NADD_MUL_LINV_LEMMA7 = prove
1096  (`!x. ~(x === &0) ==> ?B N. !m n. N <= m /\ N <= n ==>
1097         dist(m * nadd_rinv(x) n,n * nadd_rinv(x) m) <= B * (m + n)`,
1098   GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP NADD_MUL_LINV_LEMMA6) THEN
1099   DISCH_THEN(X_CHOOSE_THEN `B:num` (X_CHOOSE_TAC `N:num`)) THEN
1100   MAP_EVERY EXISTS_TAC [`B:num`; `N + 1`] THEN
1101   MAP_EVERY X_GEN_TAC [`m:num`; `n:num`] THEN STRIP_TAC THEN
1102   SUBGOAL_THEN `N <= m /\ N <= n` MP_TAC THENL
1103    [CONJ_TAC THEN MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `N + 1` THEN
1104     ASM_REWRITE_TAC[LE_ADD];
1105     DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
1106     ONCE_REWRITE_TAC[AC MULT_AC `a * b * c = b * a * c`] THEN
1107     REWRITE_TAC[LE_MULT_LCANCEL] THEN
1108     DISCH_THEN(DISJ_CASES_THEN2 MP_TAC ACCEPT_TAC) THEN
1109     CONV_TAC CONTRAPOS_CONV THEN DISCH_THEN(K ALL_TAC) THEN
1110     ONCE_REWRITE_TAC[GSYM(CONJUNCT1 LE)] THEN
1111     REWRITE_TAC[NOT_LE; GSYM LE_SUC_LT] THEN
1112     REWRITE_TAC[EQT_ELIM(REWRITE_CONV[ARITH] `SUC 0 = 1 * 1`)] THEN
1113     MATCH_MP_TAC LE_MULT2 THEN CONJ_TAC THEN
1114     MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `N + 1` THEN
1115     ASM_REWRITE_TAC[LE_ADDR]]);;
1116
1117 let NADD_MUL_LINV_LEMMA7a = prove
1118  (`!x. ~(x === &0) ==> !N. ?A B. !m n. m <= N ==>
1119         dist(m * nadd_rinv(x) n,n * nadd_rinv(x) m) <= A * n + B`,
1120   GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP NADD_MUL_LINV_LEMMA0) THEN
1121   DISCH_THEN(X_CHOOSE_THEN `A0:num` (X_CHOOSE_TAC `B0:num`)) THEN
1122   INDUCT_TAC THENL
1123    [MAP_EVERY EXISTS_TAC [`nadd_rinv x 0`; `0`] THEN
1124     REPEAT GEN_TAC THEN REWRITE_TAC[LE] THEN DISCH_THEN SUBST1_TAC THEN
1125     REWRITE_TAC[MULT_CLAUSES; DIST_LZERO; ADD_CLAUSES] THEN
1126     GEN_REWRITE_TAC RAND_CONV [MULT_SYM] THEN MATCH_ACCEPT_TAC LE_REFL;
1127     FIRST_ASSUM(X_CHOOSE_THEN `A:num` (X_CHOOSE_TAC `B:num`)) THEN
1128     EXISTS_TAC `A + (nadd_rinv(x)(SUC N) + SUC N * A0)` THEN
1129     EXISTS_TAC `SUC N * B0 + B` THEN
1130     REPEAT GEN_TAC THEN REWRITE_TAC[LE] THEN
1131     DISCH_THEN(DISJ_CASES_THEN2 SUBST1_TAC ASSUME_TAC) THENL
1132      [MATCH_MP_TAC LE_TRANS THEN
1133       EXISTS_TAC `SUC N * nadd_rinv x n + n * nadd_rinv x (SUC N)` THEN
1134       REWRITE_TAC[DIST_ADDBOUND] THEN REWRITE_TAC[RIGHT_ADD_DISTRIB] THEN
1135       ONCE_REWRITE_TAC[AC ADD_AC
1136         `(a + b + c) + d + e = (c + d) + (b + a + e)`] THEN
1137       MATCH_MP_TAC LE_ADD2 THEN CONJ_TAC THENL
1138        [REWRITE_TAC[GSYM MULT_ASSOC; GSYM LEFT_ADD_DISTRIB] THEN
1139         ASM_REWRITE_TAC[LE_MULT_LCANCEL];
1140         GEN_REWRITE_TAC LAND_CONV [MULT_SYM] THEN
1141         MATCH_ACCEPT_TAC LE_ADD];
1142       MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `A * n + B` THEN CONJ_TAC THENL
1143        [FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
1144         REWRITE_TAC[ADD_ASSOC; LE_ADD_RCANCEL] THEN
1145         REWRITE_TAC[RIGHT_ADD_DISTRIB; GSYM ADD_ASSOC; LE_ADD]]]]);;
1146
1147 let NADD_MUL_LINV_LEMMA8 = prove
1148  (`!x. ~(x === &0) ==>
1149         ?B. !m n. dist(m * nadd_rinv(x) n,n * nadd_rinv(x) m) <= B * (m + n)`,
1150   GEN_TAC THEN DISCH_TAC THEN
1151   FIRST_ASSUM(MP_TAC o MATCH_MP NADD_MUL_LINV_LEMMA7) THEN
1152   DISCH_THEN(X_CHOOSE_THEN `B0:num` (X_CHOOSE_TAC `N:num`)) THEN
1153   FIRST_ASSUM(MP_TAC o SPEC `N:num` o MATCH_MP NADD_MUL_LINV_LEMMA7a) THEN
1154   DISCH_THEN(X_CHOOSE_THEN `A:num` (X_CHOOSE_TAC `B:num`)) THEN
1155   MATCH_MP_TAC BOUNDS_NOTZERO THEN REWRITE_TAC[DIST_REFL] THEN
1156   EXISTS_TAC `A + B0` THEN EXISTS_TAC `B:num` THEN REPEAT GEN_TAC THEN
1157   DISJ_CASES_THEN2 ASSUME_TAC MP_TAC (SPECL [`N:num`; `m:num`] LE_CASES) THENL
1158    [DISJ_CASES_THEN2 ASSUME_TAC MP_TAC (SPECL [`N:num`; `n:num`] LE_CASES)
1159     THENL
1160      [MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `B0 * (m + n)` THEN CONJ_TAC THENL
1161        [FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
1162         GEN_REWRITE_TAC (RAND_CONV o funpow 2 LAND_CONV) [ADD_SYM] THEN
1163         REWRITE_TAC[RIGHT_ADD_DISTRIB; GSYM ADD_ASSOC; LE_ADD]];
1164       DISCH_THEN(ANTE_RES_THEN ASSUME_TAC) THEN
1165       MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `A * m + B` THEN
1166       ONCE_REWRITE_TAC[DIST_SYM] THEN
1167       ASM_REWRITE_TAC[LE_ADD_RCANCEL] THEN
1168       REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB; GSYM ADD_ASSOC;
1169         LE_ADD]];
1170     DISCH_THEN(ANTE_RES_THEN ASSUME_TAC) THEN
1171     MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `A * n + B` THEN
1172     ASM_REWRITE_TAC[LE_ADD_RCANCEL] THEN
1173     GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [ADD_SYM] THEN
1174     REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB; GSYM ADD_ASSOC;
1175       LE_ADD]]);;
1176
1177 (* ------------------------------------------------------------------------- *)
1178 (* Now the multiplicative inverse proper.                                    *)
1179 (* ------------------------------------------------------------------------- *)
1180
1181 let nadd_inv = new_definition
1182   `nadd_inv(x) = if x === &0 then &0 else afn(nadd_rinv x)`;;
1183
1184 override_interface ("inv",`nadd_inv:nadd->nadd`);;
1185
1186 let NADD_INV = prove
1187  (`!x. fn(nadd_inv x) = if x === &0 then (\n. 0) else nadd_rinv x`,
1188   GEN_TAC THEN REWRITE_TAC[nadd_inv] THEN
1189   ASM_CASES_TAC `x === &0` THEN ASM_REWRITE_TAC[NADD_OF_NUM; MULT_CLAUSES] THEN
1190   REWRITE_TAC[GSYM nadd_rep; is_nadd] THEN
1191   MATCH_MP_TAC NADD_MUL_LINV_LEMMA8 THEN POP_ASSUM ACCEPT_TAC);;
1192
1193 let NADD_MUL_LINV = prove
1194  (`!x. ~(x === &0) ==> inv(x) ** x === &1`,
1195   GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[nadd_eq; NADD_MUL] THEN
1196   ONCE_REWRITE_TAC[BOUNDS_DIVIDED] THEN
1197   X_CHOOSE_THEN `A1:num` (X_CHOOSE_TAC `B1:num`)
1198    (SPECL [`inv(x)`; `x:nadd`] NADD_ALTMUL) THEN
1199   REWRITE_TAC[DIST_LMUL; NADD_OF_NUM; MULT_CLAUSES] THEN
1200   FIRST_ASSUM(X_CHOOSE_TAC `N:num` o MATCH_MP NADD_MUL_LINV_LEMMA2) THEN
1201   X_CHOOSE_THEN `A':num` (X_CHOOSE_TAC `B':num`)
1202     (SPEC `x:nadd` NADD_BOUND) THEN
1203   SUBGOAL_THEN `?A2 B2. !n. dist(fn x n * nadd_rinv x n,n * n) <= A2 * n + B2`
1204   STRIP_ASSUME_TAC THENL
1205    [EXISTS_TAC `A':num` THEN ONCE_REWRITE_TAC[BOUNDS_IGNORE] THEN
1206     MAP_EVERY EXISTS_TAC [`B':num`; `N:num`] THEN REPEAT STRIP_TAC THEN
1207     MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `fn x n` THEN ASM_REWRITE_TAC[] THEN
1208     FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
1209     MAP_EVERY EXISTS_TAC [`A1 + A2`; `B1 + B2`] THEN
1210     GEN_TAC THEN MATCH_MP_TAC DIST_TRIANGLE_LE THEN
1211     EXISTS_TAC `fn (inv x) n * fn x n` THEN
1212     REWRITE_TAC[RIGHT_ADD_DISTRIB] THEN
1213     ONCE_REWRITE_TAC[AC ADD_AC `(a + b) + c + d = (a + c) + (b + d)`] THEN
1214     MATCH_MP_TAC LE_ADD2 THEN ASM_REWRITE_TAC[] THEN
1215     GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o LAND_CONV) [MULT_SYM] THEN
1216     ASM_REWRITE_TAC[NADD_INV]]);;
1217
1218 let NADD_INV_0 = prove
1219  (`inv(&0) === &0`,
1220   REWRITE_TAC[nadd_inv; NADD_EQ_REFL]);;
1221
1222 (* ------------------------------------------------------------------------- *)
1223 (* Welldefinedness follows from already established principles because if    *)
1224 (* x = y then y' = y' 1 = y' (x' x) = y' (x' y) = (y' y) x' = 1 x' = x'      *)
1225 (* ------------------------------------------------------------------------- *)
1226
1227 let NADD_INV_WELLDEF = prove
1228  (`!x y. x === y ==> inv(x) === inv(y)`,
1229   let TAC tm ths =
1230     MATCH_MP_TAC NADD_EQ_TRANS THEN EXISTS_TAC tm THEN
1231     CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC ths] in
1232   REPEAT STRIP_TAC THEN
1233   ASM_CASES_TAC `x === &0` THENL
1234    [SUBGOAL_THEN `y === &0` ASSUME_TAC THENL
1235      [ASM_MESON_TAC[NADD_EQ_TRANS; NADD_EQ_SYM];
1236       ASM_REWRITE_TAC[nadd_inv; NADD_EQ_REFL]];
1237     SUBGOAL_THEN `~(y === &0)` ASSUME_TAC THENL
1238      [ASM_MESON_TAC[NADD_EQ_TRANS; NADD_EQ_SYM]; ALL_TAC]] THEN
1239   TAC `inv(y) ** &1`
1240       [NADD_MUL_SYM; NADD_MUL_LID; NADD_EQ_TRANS] THEN
1241   TAC `inv(y) ** (inv(x) ** x)`
1242       [NADD_MUL_LINV; NADD_MUL_WELLDEF; NADD_EQ_REFL] THEN
1243   TAC `inv(y) ** (inv(x) ** y)`
1244       [NADD_MUL_WELLDEF; NADD_EQ_REFL; NADD_EQ_SYM] THEN
1245   TAC `(inv(y) ** y) ** inv(x)`
1246       [NADD_MUL_ASSOC; NADD_MUL_SYM; NADD_EQ_TRANS;
1247        NADD_MUL_WELLDEF; NADD_EQ_REFL] THEN
1248   ASM_MESON_TAC[NADD_MUL_LINV; NADD_MUL_WELLDEF; NADD_EQ_REFL;
1249     NADD_MUL_LID; NADD_EQ_TRANS; NADD_EQ_SYM]);;
1250
1251 (* ------------------------------------------------------------------------- *)
1252 (* Definition of the new type.                                               *)
1253 (* ------------------------------------------------------------------------- *)
1254
1255 let hreal_tybij =
1256   define_quotient_type "hreal" ("mk_hreal","dest_hreal") `(===)`;;
1257
1258 do_list overload_interface
1259  ["+",`hreal_add:hreal->hreal->hreal`;
1260   "*",`hreal_mul:hreal->hreal->hreal`;
1261   "<=",`hreal_le:hreal->hreal->bool`];;
1262
1263 do_list override_interface
1264  ["&",`hreal_of_num:num->hreal`;
1265   "inv",`hreal_inv:hreal->hreal`];;
1266
1267 let hreal_of_num,hreal_of_num_th =
1268   lift_function (snd hreal_tybij) (NADD_EQ_REFL,NADD_EQ_TRANS)
1269   "hreal_of_num" NADD_OF_NUM_WELLDEF;;
1270
1271 let hreal_add,hreal_add_th =
1272   lift_function (snd hreal_tybij) (NADD_EQ_REFL,NADD_EQ_TRANS)
1273   "hreal_add" NADD_ADD_WELLDEF;;
1274
1275 let hreal_mul,hreal_mul_th =
1276   lift_function (snd hreal_tybij) (NADD_EQ_REFL,NADD_EQ_TRANS)
1277   "hreal_mul" NADD_MUL_WELLDEF;;
1278
1279 let hreal_le,hreal_le_th =
1280   lift_function (snd hreal_tybij) (NADD_EQ_REFL,NADD_EQ_TRANS)
1281   "hreal_le" NADD_LE_WELLDEF;;
1282
1283 let hreal_inv,hreal_inv_th =
1284   lift_function (snd hreal_tybij) (NADD_EQ_REFL,NADD_EQ_TRANS)
1285   "hreal_inv" NADD_INV_WELLDEF;;
1286
1287 let HREAL_COMPLETE =
1288   let th1 = ASSUME `(P:nadd->bool) = (\x. Q(mk_hreal((===) x)))` in
1289   let th2 = BETA_RULE(AP_THM th1 `x:nadd`) in
1290   let th3 = lift_theorem hreal_tybij
1291               (NADD_EQ_REFL,NADD_EQ_SYM,NADD_EQ_TRANS)
1292               [hreal_of_num_th; hreal_add_th; hreal_mul_th; hreal_le_th; th2]
1293               (SPEC_ALL NADD_COMPLETE) in
1294   let th4 = MATCH_MP (DISCH_ALL th3) (REFL `\x. Q(mk_hreal((===) x)):bool`) in
1295   CONV_RULE(GEN_ALPHA_CONV `P:hreal->bool`) (GEN_ALL th4);;
1296
1297 let [HREAL_OF_NUM_EQ; HREAL_OF_NUM_LE; HREAL_OF_NUM_ADD; HREAL_OF_NUM_MUL;
1298      HREAL_LE_REFL; HREAL_LE_TRANS; HREAL_LE_ANTISYM; HREAL_LE_TOTAL;
1299      HREAL_LE_ADD; HREAL_LE_EXISTS; HREAL_ARCH; HREAL_ADD_SYM; HREAL_ADD_ASSOC;
1300      HREAL_ADD_LID; HREAL_ADD_LCANCEL; HREAL_MUL_SYM; HREAL_MUL_ASSOC;
1301      HREAL_MUL_LID; HREAL_ADD_LDISTRIB; HREAL_MUL_LINV; HREAL_INV_0] =
1302   map (lift_theorem hreal_tybij
1303          (NADD_EQ_REFL,NADD_EQ_SYM,NADD_EQ_TRANS)
1304              [hreal_of_num_th; hreal_add_th; hreal_mul_th;
1305               hreal_le_th; hreal_inv_th])
1306  [NADD_OF_NUM_EQ; NADD_OF_NUM_LE; NADD_OF_NUM_ADD; NADD_OF_NUM_MUL;
1307   NADD_LE_REFL; NADD_LE_TRANS; NADD_LE_ANTISYM; NADD_LE_TOTAL; NADD_LE_ADD;
1308   NADD_LE_EXISTS; NADD_ARCH; NADD_ADD_SYM; NADD_ADD_ASSOC; NADD_ADD_LID;
1309   NADD_ADD_LCANCEL; NADD_MUL_SYM; NADD_MUL_ASSOC; NADD_MUL_LID; NADD_LDISTRIB;
1310   NADD_MUL_LINV; NADD_INV_0];;
1311
1312 (* ------------------------------------------------------------------------- *)
1313 (* Consequential theorems needed later.                                      *)
1314 (* ------------------------------------------------------------------------- *)
1315
1316 let HREAL_LE_EXISTS_DEF = prove
1317  (`!m n. m <= n <=> ?d. n = m + d`,
1318   REPEAT GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[HREAL_LE_EXISTS] THEN
1319   DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN REWRITE_TAC[HREAL_LE_ADD]);;
1320
1321 let HREAL_EQ_ADD_LCANCEL = prove
1322  (`!m n p. (m + n = m + p) <=> (n = p)`,
1323   REPEAT GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[HREAL_ADD_LCANCEL] THEN
1324   DISCH_THEN SUBST1_TAC THEN REFL_TAC);;
1325
1326 let HREAL_EQ_ADD_RCANCEL = prove
1327  (`!m n p. (m + p = n + p) <=> (m = n)`,
1328   ONCE_REWRITE_TAC[HREAL_ADD_SYM] THEN REWRITE_TAC[HREAL_EQ_ADD_LCANCEL]);;
1329
1330 let HREAL_LE_ADD_LCANCEL = prove
1331  (`!m n p. (m + n <= m + p) <=> (n <= p)`,
1332   REWRITE_TAC[HREAL_LE_EXISTS_DEF; GSYM HREAL_ADD_ASSOC;
1333     HREAL_EQ_ADD_LCANCEL]);;
1334
1335 let HREAL_LE_ADD_RCANCEL = prove
1336  (`!m n p. (m + p <= n + p) <=> (m <= n)`,
1337   ONCE_REWRITE_TAC[HREAL_ADD_SYM] THEN MATCH_ACCEPT_TAC HREAL_LE_ADD_LCANCEL);;
1338
1339 let HREAL_ADD_RID = prove
1340  (`!n. n + &0 = n`,
1341   ONCE_REWRITE_TAC[HREAL_ADD_SYM] THEN MATCH_ACCEPT_TAC HREAL_ADD_LID);;
1342
1343 let HREAL_ADD_RDISTRIB = prove
1344  (`!m n p. (m + n) * p = m * p + n * p`,
1345   ONCE_REWRITE_TAC[HREAL_MUL_SYM] THEN MATCH_ACCEPT_TAC HREAL_ADD_LDISTRIB);;
1346
1347 let HREAL_MUL_LZERO = prove
1348  (`!m. &0 * m = &0`,
1349   GEN_TAC THEN MP_TAC(SPECL [`&0`; `&1`; `m:hreal`] HREAL_ADD_RDISTRIB) THEN
1350   REWRITE_TAC[HREAL_ADD_LID] THEN
1351   GEN_REWRITE_TAC (funpow 2 LAND_CONV) [GSYM HREAL_ADD_LID] THEN
1352   REWRITE_TAC[HREAL_EQ_ADD_RCANCEL] THEN
1353   DISCH_THEN(ACCEPT_TAC o SYM));;
1354
1355 let HREAL_MUL_RZERO = prove
1356  (`!m. m * &0 = &0`,
1357   ONCE_REWRITE_TAC[HREAL_MUL_SYM] THEN MATCH_ACCEPT_TAC HREAL_MUL_LZERO);;
1358
1359 let HREAL_ADD_AC = prove
1360  (`(m + n = n + m) /\
1361    ((m + n) + p = m + (n + p)) /\
1362    (m + (n + p) = n + (m + p))`,
1363   REWRITE_TAC[HREAL_ADD_ASSOC; EQT_INTRO(SPEC_ALL HREAL_ADD_SYM)] THEN
1364   AP_THM_TAC THEN AP_TERM_TAC THEN MATCH_ACCEPT_TAC HREAL_ADD_SYM);;
1365
1366 let HREAL_LE_ADD2 = prove
1367  (`!a b c d. a <= b /\ c <= d ==> a + c <= b + d`,
1368   REPEAT GEN_TAC THEN REWRITE_TAC[HREAL_LE_EXISTS_DEF] THEN
1369   DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `d1:hreal`)
1370     (X_CHOOSE_TAC `d2:hreal`)) THEN
1371   EXISTS_TAC `d1 + d2` THEN ASM_REWRITE_TAC[HREAL_ADD_AC]);;
1372
1373 let HREAL_LE_MUL_RCANCEL_IMP = prove
1374  (`!a b c. a <= b ==> a * c <= b * c`,
1375   REPEAT GEN_TAC THEN REWRITE_TAC[HREAL_LE_EXISTS_DEF] THEN
1376   DISCH_THEN(X_CHOOSE_THEN `d:hreal` SUBST1_TAC) THEN
1377   EXISTS_TAC `d * c` THEN REWRITE_TAC[HREAL_ADD_RDISTRIB]);;
1378
1379 (* ------------------------------------------------------------------------- *)
1380 (* Define operations on representatives of signed reals.                     *)
1381 (* ------------------------------------------------------------------------- *)
1382
1383 let treal_of_num = new_definition
1384   `treal_of_num n = (&n, &0)`;;
1385
1386 let treal_neg = new_definition
1387   `treal_neg ((x:hreal),(y:hreal)) = (y,x)`;;
1388
1389 let treal_add = new_definition
1390   `(x1,y1) treal_add (x2,y2) = (x1 + x2, y1 + y2)`;;
1391
1392 let treal_mul = new_definition
1393   `(x1,y1) treal_mul (x2,y2) = ((x1 * x2) + (y1 * y2),(x1 * y2) + (y1 * x2))`;;
1394
1395 let treal_le = new_definition
1396   `(x1,y1) treal_le (x2,y2) <=> x1 + y2 <= x2 + y1`;;
1397
1398 let treal_inv = new_definition
1399   `treal_inv(x,y) = if x = y then (&0, &0)
1400                     else if y <= x then (inv(@d. x = y + d), &0)
1401                     else (&0, inv(@d. y = x + d))`;;
1402
1403 (* ------------------------------------------------------------------------- *)
1404 (* Define the equivalence relation and prove it *is* one.                    *)
1405 (* ------------------------------------------------------------------------- *)
1406
1407 let treal_eq = new_definition
1408   `(x1,y1) treal_eq (x2,y2) <=> (x1 + y2 = x2 + y1)`;;
1409
1410 let TREAL_EQ_REFL = prove
1411  (`!x. x treal_eq x`,
1412   REWRITE_TAC[FORALL_PAIR_THM; treal_eq]);;
1413
1414 let TREAL_EQ_SYM = prove
1415  (`!x y. x treal_eq y <=> y treal_eq x`,
1416   REWRITE_TAC[FORALL_PAIR_THM; treal_eq; EQ_SYM_EQ]);;
1417
1418 let TREAL_EQ_TRANS = prove
1419  (`!x y z. x treal_eq y /\ y treal_eq z ==> x treal_eq z`,
1420   REWRITE_TAC[FORALL_PAIR_THM; treal_eq] THEN REPEAT GEN_TAC THEN
1421   DISCH_THEN(MP_TAC o MK_COMB o (AP_TERM `(+)` F_F I) o CONJ_PAIR) THEN
1422   GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [HREAL_ADD_SYM] THEN
1423   REWRITE_TAC[GSYM HREAL_ADD_ASSOC; HREAL_EQ_ADD_LCANCEL] THEN
1424   REWRITE_TAC[HREAL_ADD_ASSOC; HREAL_EQ_ADD_RCANCEL] THEN
1425   DISCH_THEN(MATCH_ACCEPT_TAC o ONCE_REWRITE_RULE[HREAL_ADD_SYM]));;
1426
1427 (* ------------------------------------------------------------------------- *)
1428 (* Useful to avoid unnecessary use of the equivalence relation.              *)
1429 (* ------------------------------------------------------------------------- *)
1430
1431 let TREAL_EQ_AP = prove
1432  (`!x y. (x = y) ==> x treal_eq y`,
1433   SIMP_TAC[TREAL_EQ_REFL]);;
1434
1435 (* ------------------------------------------------------------------------- *)
1436 (* Commutativity properties for injector.                                    *)
1437 (* ------------------------------------------------------------------------- *)
1438
1439 let TREAL_OF_NUM_EQ = prove
1440  (`!m n. (treal_of_num m treal_eq treal_of_num n) <=> (m = n)`,
1441   REWRITE_TAC[treal_of_num; treal_eq; HREAL_OF_NUM_EQ; HREAL_ADD_RID]);;
1442
1443 let TREAL_OF_NUM_LE = prove
1444  (`!m n. (treal_of_num m treal_le treal_of_num n) <=> m <= n`,
1445   REWRITE_TAC[treal_of_num; treal_le; HREAL_OF_NUM_LE; HREAL_ADD_RID]);;
1446
1447 let TREAL_OF_NUM_ADD = prove
1448  (`!m n. (treal_of_num m treal_add treal_of_num n) treal_eq
1449          (treal_of_num(m + n))`,
1450   REWRITE_TAC[treal_of_num; treal_eq; treal_add;
1451    HREAL_OF_NUM_ADD; HREAL_ADD_RID; ADD_CLAUSES]);;
1452
1453 let TREAL_OF_NUM_MUL = prove
1454  (`!m n. (treal_of_num m treal_mul treal_of_num n) treal_eq
1455          (treal_of_num(m * n))`,
1456   REWRITE_TAC[treal_of_num; treal_eq; treal_mul;
1457    HREAL_OF_NUM_MUL; HREAL_MUL_RZERO; HREAL_MUL_LZERO; HREAL_ADD_RID;
1458    HREAL_ADD_LID; HREAL_ADD_RID; MULT_CLAUSES]);;
1459
1460 (* ------------------------------------------------------------------------- *)
1461 (* Strong forms of equality are useful to simplify welldefinedness proofs.   *)
1462 (* ------------------------------------------------------------------------- *)
1463
1464 let TREAL_ADD_SYM_EQ = prove
1465  (`!x y. x treal_add y = y treal_add x`,
1466   REWRITE_TAC[FORALL_PAIR_THM; treal_add; PAIR_EQ; HREAL_ADD_SYM]);;
1467
1468 let TREAL_MUL_SYM_EQ = prove
1469  (`!x y. x treal_mul y = y treal_mul x`,
1470   REWRITE_TAC[FORALL_PAIR_THM; treal_mul; HREAL_MUL_SYM; HREAL_ADD_SYM]);;
1471
1472 (* ------------------------------------------------------------------------- *)
1473 (* Prove the properties of operations on representatives.                    *)
1474 (* ------------------------------------------------------------------------- *)
1475
1476 let TREAL_ADD_SYM = prove
1477  (`!x y. (x treal_add y) treal_eq (y treal_add x)`,
1478   REPEAT GEN_TAC THEN MATCH_MP_TAC TREAL_EQ_AP THEN
1479   MATCH_ACCEPT_TAC TREAL_ADD_SYM_EQ);;
1480
1481 let TREAL_ADD_ASSOC = prove
1482  (`!x y z. (x treal_add (y treal_add z)) treal_eq
1483            ((x treal_add y) treal_add z)`,
1484   SIMP_TAC[FORALL_PAIR_THM; TREAL_EQ_AP; treal_add; HREAL_ADD_ASSOC]);;
1485
1486 let TREAL_ADD_LID = prove
1487  (`!x. ((treal_of_num 0) treal_add x) treal_eq x`,
1488   REWRITE_TAC[FORALL_PAIR_THM; treal_of_num; treal_add; treal_eq;
1489               HREAL_ADD_LID]);;
1490
1491 let TREAL_ADD_LINV = prove
1492  (`!x. ((treal_neg x) treal_add x) treal_eq (treal_of_num 0)`,
1493   REWRITE_TAC[FORALL_PAIR_THM; treal_neg; treal_add; treal_eq; treal_of_num;
1494               HREAL_ADD_LID; HREAL_ADD_RID; HREAL_ADD_SYM]);;
1495
1496 let TREAL_MUL_SYM = prove
1497  (`!x y. (x treal_mul y) treal_eq (y treal_mul x)`,
1498   SIMP_TAC[TREAL_EQ_AP; TREAL_MUL_SYM_EQ]);;
1499
1500 let TREAL_MUL_ASSOC = prove
1501  (`!x y z. (x treal_mul (y treal_mul z)) treal_eq
1502            ((x treal_mul y) treal_mul z)`,
1503   SIMP_TAC[FORALL_PAIR_THM; TREAL_EQ_AP; treal_mul; HREAL_ADD_LDISTRIB;
1504            HREAL_ADD_RDISTRIB; GSYM HREAL_MUL_ASSOC; HREAL_ADD_AC]);;
1505
1506 let TREAL_MUL_LID = prove
1507  (`!x. ((treal_of_num 1) treal_mul x) treal_eq x`,
1508   SIMP_TAC[FORALL_PAIR_THM; treal_of_num; treal_mul; treal_eq] THEN
1509   REWRITE_TAC[HREAL_MUL_LZERO; HREAL_MUL_LID; HREAL_ADD_LID; HREAL_ADD_RID]);;
1510
1511 let TREAL_ADD_LDISTRIB = prove
1512  (`!x y z. (x treal_mul (y treal_add z)) treal_eq
1513            ((x treal_mul y) treal_add (x treal_mul z))`,
1514   SIMP_TAC[FORALL_PAIR_THM; TREAL_EQ_AP; treal_mul; treal_add;
1515            HREAL_ADD_LDISTRIB; PAIR_EQ; HREAL_ADD_AC]);;
1516
1517 let TREAL_LE_REFL = prove
1518  (`!x. x treal_le x`,
1519   REWRITE_TAC[FORALL_PAIR_THM; treal_le; HREAL_LE_REFL]);;
1520
1521 let TREAL_LE_ANTISYM = prove
1522  (`!x y. x treal_le y /\ y treal_le x <=> (x treal_eq y)`,
1523   REWRITE_TAC[FORALL_PAIR_THM; treal_le; treal_eq; HREAL_LE_ANTISYM]);;
1524
1525 let TREAL_LE_TRANS = prove
1526  (`!x y z. x treal_le y /\ y treal_le z ==> x treal_le z`,
1527   REWRITE_TAC[FORALL_PAIR_THM; treal_le] THEN REPEAT GEN_TAC THEN
1528   DISCH_THEN(MP_TAC o MATCH_MP HREAL_LE_ADD2) THEN
1529   GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [HREAL_ADD_SYM] THEN
1530   REWRITE_TAC[GSYM HREAL_ADD_ASSOC; HREAL_LE_ADD_LCANCEL] THEN
1531   REWRITE_TAC[HREAL_ADD_ASSOC; HREAL_LE_ADD_RCANCEL] THEN
1532   DISCH_THEN(MATCH_ACCEPT_TAC o ONCE_REWRITE_RULE[HREAL_ADD_SYM]));;
1533
1534 let TREAL_LE_TOTAL = prove
1535  (`!x y. x treal_le y \/ y treal_le x`,
1536   REWRITE_TAC[FORALL_PAIR_THM; treal_le; HREAL_LE_TOTAL]);;
1537
1538 let TREAL_LE_LADD_IMP = prove
1539  (`!x y z. (y treal_le z) ==> (x treal_add y) treal_le (x treal_add z)`,
1540   REWRITE_TAC[FORALL_PAIR_THM; treal_le; treal_add] THEN
1541   REWRITE_TAC[GSYM HREAL_ADD_ASSOC; HREAL_LE_ADD_LCANCEL] THEN
1542   ONCE_REWRITE_TAC[HREAL_ADD_SYM] THEN
1543   REWRITE_TAC[GSYM HREAL_ADD_ASSOC; HREAL_LE_ADD_LCANCEL]);;
1544
1545 let TREAL_LE_MUL = prove
1546  (`!x y. (treal_of_num 0) treal_le x /\ (treal_of_num 0) treal_le y
1547          ==> (treal_of_num 0) treal_le (x treal_mul y)`,
1548   REWRITE_TAC[FORALL_PAIR_THM; treal_of_num; treal_le; treal_mul] THEN
1549   REPEAT GEN_TAC THEN REWRITE_TAC[HREAL_ADD_LID; HREAL_ADD_RID] THEN
1550   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1551   DISCH_THEN(CHOOSE_THEN SUBST1_TAC o MATCH_MP HREAL_LE_EXISTS) THEN
1552   REWRITE_TAC[HREAL_ADD_LDISTRIB; HREAL_LE_ADD_LCANCEL;
1553     GSYM HREAL_ADD_ASSOC] THEN
1554   GEN_REWRITE_TAC RAND_CONV [HREAL_ADD_SYM] THEN
1555   ASM_REWRITE_TAC[HREAL_LE_ADD_LCANCEL] THEN
1556   MATCH_MP_TAC HREAL_LE_MUL_RCANCEL_IMP THEN ASM_REWRITE_TAC[]);;
1557
1558 let TREAL_INV_0 = prove
1559  (`treal_inv (treal_of_num 0) treal_eq (treal_of_num 0)`,
1560   REWRITE_TAC[treal_inv; treal_eq; treal_of_num]);;
1561
1562 let TREAL_MUL_LINV = prove
1563  (`!x. ~(x treal_eq treal_of_num 0) ==>
1564         (treal_inv(x) treal_mul x) treal_eq (treal_of_num 1)`,
1565   REWRITE_TAC[FORALL_PAIR_THM] THEN
1566   MAP_EVERY X_GEN_TAC [`x:hreal`; `y:hreal`] THEN
1567   PURE_REWRITE_TAC[treal_eq; treal_of_num; treal_mul; treal_inv] THEN
1568   PURE_REWRITE_TAC[HREAL_ADD_LID; HREAL_ADD_RID] THEN DISCH_TAC THEN
1569   PURE_ASM_REWRITE_TAC[COND_CLAUSES] THEN COND_CASES_TAC THEN
1570   PURE_REWRITE_TAC[treal_mul; treal_eq] THEN
1571   REWRITE_TAC[HREAL_ADD_LID; HREAL_ADD_RID;
1572               HREAL_MUL_LZERO; HREAL_MUL_RZERO] THENL
1573    [ALL_TAC;
1574     DISJ_CASES_THEN MP_TAC(SPECL [`x:hreal`; `y:hreal`] HREAL_LE_TOTAL) THEN
1575     ASM_REWRITE_TAC[] THEN DISCH_TAC] THEN
1576   FIRST_ASSUM(MP_TAC o MATCH_MP HREAL_LE_EXISTS) THEN
1577   DISCH_THEN(MP_TAC o SELECT_RULE) THEN
1578   DISCH_THEN(fun th -> ASSUME_TAC (SYM th) THEN
1579                        GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [th]) THEN
1580   REWRITE_TAC[HREAL_ADD_LDISTRIB] THEN
1581   GEN_REWRITE_TAC RAND_CONV [HREAL_ADD_SYM] THEN
1582   AP_TERM_TAC THEN MATCH_MP_TAC HREAL_MUL_LINV THEN
1583   DISCH_THEN SUBST_ALL_TAC THEN
1584   FIRST_ASSUM(UNDISCH_TAC o check is_eq o concl) THEN
1585   ASM_REWRITE_TAC[HREAL_ADD_RID] THEN
1586   PURE_ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN ASM_REWRITE_TAC[]);;
1587
1588 (* ------------------------------------------------------------------------- *)
1589 (* Show that the operations respect the equivalence relation.                *)
1590 (* ------------------------------------------------------------------------- *)
1591
1592 let TREAL_OF_NUM_WELLDEF = prove
1593  (`!m n. (m = n) ==> (treal_of_num m) treal_eq (treal_of_num n)`,
1594   REPEAT GEN_TAC THEN DISCH_THEN SUBST1_TAC THEN
1595   MATCH_ACCEPT_TAC TREAL_EQ_REFL);;
1596
1597 let TREAL_NEG_WELLDEF = prove
1598  (`!x1 x2. x1 treal_eq x2 ==> (treal_neg x1) treal_eq (treal_neg x2)`,
1599   REWRITE_TAC[FORALL_PAIR_THM; treal_neg; treal_eq] THEN REPEAT STRIP_TAC THEN
1600   ONCE_REWRITE_TAC[HREAL_ADD_SYM] THEN ASM_REWRITE_TAC[]);;
1601
1602 let TREAL_ADD_WELLDEFR = prove
1603  (`!x1 x2 y. x1 treal_eq x2 ==> (x1 treal_add y) treal_eq (x2 treal_add y)`,
1604   REWRITE_TAC[FORALL_PAIR_THM; treal_add; treal_eq] THEN
1605   REWRITE_TAC[HREAL_EQ_ADD_RCANCEL; HREAL_ADD_ASSOC] THEN
1606   ONCE_REWRITE_TAC[HREAL_ADD_SYM] THEN
1607   REWRITE_TAC[HREAL_EQ_ADD_RCANCEL; HREAL_ADD_ASSOC]);;
1608
1609 let TREAL_ADD_WELLDEF = prove
1610  (`!x1 x2 y1 y2. x1 treal_eq x2 /\ y1 treal_eq y2 ==>
1611      (x1 treal_add y1) treal_eq (x2 treal_add y2)`,
1612   REPEAT GEN_TAC THEN DISCH_TAC THEN
1613   MATCH_MP_TAC TREAL_EQ_TRANS THEN EXISTS_TAC `x1 treal_add y2` THEN
1614   CONJ_TAC THENL [ONCE_REWRITE_TAC[TREAL_ADD_SYM_EQ]; ALL_TAC] THEN
1615   MATCH_MP_TAC TREAL_ADD_WELLDEFR THEN ASM_REWRITE_TAC[]);;
1616
1617 let TREAL_MUL_WELLDEFR = prove
1618  (`!x1 x2 y. x1 treal_eq x2 ==> (x1 treal_mul y) treal_eq (x2 treal_mul y)`,
1619   REWRITE_TAC[FORALL_PAIR_THM; treal_mul; treal_eq] THEN REPEAT GEN_TAC THEN
1620   ONCE_REWRITE_TAC[AC HREAL_ADD_AC
1621     `(a + b) + (c + d) = (a + d) + (b + c)`] THEN
1622   REWRITE_TAC[GSYM HREAL_ADD_RDISTRIB] THEN DISCH_TAC THEN
1623   ASM_REWRITE_TAC[] THEN AP_TERM_TAC THEN
1624   ONCE_REWRITE_TAC[HREAL_ADD_SYM] THEN POP_ASSUM SUBST1_TAC THEN REFL_TAC);;
1625
1626 let TREAL_MUL_WELLDEF = prove
1627  (`!x1 x2 y1 y2. x1 treal_eq x2 /\ y1 treal_eq y2 ==>
1628      (x1 treal_mul y1) treal_eq (x2 treal_mul y2)`,
1629   REPEAT GEN_TAC THEN DISCH_TAC THEN
1630   MATCH_MP_TAC TREAL_EQ_TRANS THEN EXISTS_TAC `x1 treal_mul y2` THEN
1631   CONJ_TAC THENL [ONCE_REWRITE_TAC[TREAL_MUL_SYM_EQ]; ALL_TAC] THEN
1632   MATCH_MP_TAC TREAL_MUL_WELLDEFR THEN ASM_REWRITE_TAC[]);;
1633
1634 let TREAL_EQ_IMP_LE = prove
1635  (`!x y. x treal_eq y ==> x treal_le y`,
1636   SIMP_TAC[FORALL_PAIR_THM; treal_eq; treal_le; HREAL_LE_REFL]);;
1637
1638 let TREAL_LE_WELLDEF = prove
1639  (`!x1 x2 y1 y2. x1 treal_eq x2 /\ y1 treal_eq y2 ==>
1640      (x1 treal_le y1 <=> x2 treal_le y2)`,
1641   REPEAT (STRIP_TAC ORELSE EQ_TAC) THENL
1642    [MATCH_MP_TAC TREAL_LE_TRANS THEN EXISTS_TAC `y1:hreal#hreal` THEN
1643     CONJ_TAC THENL
1644      [MATCH_MP_TAC TREAL_LE_TRANS THEN EXISTS_TAC `x1:hreal#hreal` THEN
1645       ASM_REWRITE_TAC[] THEN MATCH_MP_TAC TREAL_EQ_IMP_LE THEN
1646       ONCE_REWRITE_TAC[TREAL_EQ_SYM];
1647       MATCH_MP_TAC TREAL_EQ_IMP_LE];
1648     MATCH_MP_TAC TREAL_LE_TRANS THEN EXISTS_TAC `y2:hreal#hreal` THEN
1649     CONJ_TAC THENL
1650      [MATCH_MP_TAC TREAL_LE_TRANS THEN EXISTS_TAC `x2:hreal#hreal` THEN
1651       ASM_REWRITE_TAC[] THEN MATCH_MP_TAC TREAL_EQ_IMP_LE;
1652       MATCH_MP_TAC TREAL_EQ_IMP_LE THEN ONCE_REWRITE_TAC[TREAL_EQ_SYM]]] THEN
1653   ASM_REWRITE_TAC[]);;
1654
1655 let TREAL_INV_WELLDEF = prove
1656  (`!x y. x treal_eq y ==> (treal_inv x) treal_eq (treal_inv y)`,
1657   let lemma = prove
1658    (`(@d. x = x + d) = &0`,
1659     MATCH_MP_TAC SELECT_UNIQUE THEN BETA_TAC THEN
1660     GEN_TAC THEN GEN_REWRITE_TAC (funpow 2 LAND_CONV) [GSYM HREAL_ADD_RID] THEN
1661     REWRITE_TAC[HREAL_EQ_ADD_LCANCEL] THEN
1662     MATCH_ACCEPT_TAC EQ_SYM_EQ) in
1663   REWRITE_TAC[FORALL_PAIR_THM] THEN
1664   MAP_EVERY X_GEN_TAC [`x1:hreal`; `x2:hreal`; `y1:hreal`; `y2:hreal`] THEN
1665   PURE_REWRITE_TAC[treal_eq; treal_inv] THEN
1666   ASM_CASES_TAC `x1 :hreal = x2` THEN
1667   ASM_CASES_TAC `y1 :hreal = y2` THEN ASM_REWRITE_TAC[] THEN
1668   REWRITE_TAC[TREAL_EQ_REFL] THEN
1669   DISCH_THEN(MP_TAC o GEN_REWRITE_RULE RAND_CONV [HREAL_ADD_SYM]) THEN
1670   REWRITE_TAC[HREAL_EQ_ADD_LCANCEL; HREAL_EQ_ADD_RCANCEL] THEN DISCH_TAC THEN
1671   ASM_REWRITE_TAC[HREAL_LE_REFL; lemma; HREAL_INV_0;TREAL_EQ_REFL] THEN
1672   ASM_CASES_TAC `x2 <= x1` THEN ASM_REWRITE_TAC[] THENL
1673    [FIRST_ASSUM(ASSUME_TAC o SYM o SELECT_RULE o MATCH_MP HREAL_LE_EXISTS) THEN
1674     UNDISCH_TAC `x1 + y2 = x2 + y1` THEN
1675     FIRST_ASSUM(SUBST1_TAC o SYM) THEN
1676     REWRITE_TAC[HREAL_EQ_ADD_LCANCEL; GSYM HREAL_ADD_ASSOC] THEN
1677     DISCH_THEN(SUBST1_TAC o SYM) THEN
1678     REWRITE_TAC[ONCE_REWRITE_RULE[HREAL_ADD_SYM] HREAL_LE_ADD] THEN
1679     GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o RAND_CONV o BINDER_CONV o
1680       LAND_CONV) [HREAL_ADD_SYM] THEN
1681     REWRITE_TAC[HREAL_EQ_ADD_LCANCEL; TREAL_EQ_REFL];
1682     DISJ_CASES_THEN MP_TAC
1683       (SPECL [`x1:hreal`; `x2:hreal`] HREAL_LE_TOTAL) THEN
1684     ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1685     FIRST_ASSUM(ASSUME_TAC o SYM o SELECT_RULE o MATCH_MP HREAL_LE_EXISTS) THEN
1686     UNDISCH_TAC `x1 + y2 = x2 + y1` THEN
1687     FIRST_ASSUM(SUBST1_TAC o SYM) THEN
1688     REWRITE_TAC[HREAL_EQ_ADD_LCANCEL; GSYM HREAL_ADD_ASSOC] THEN
1689     DISCH_THEN SUBST1_TAC THEN
1690     REWRITE_TAC[ONCE_REWRITE_RULE[HREAL_ADD_SYM] HREAL_LE_ADD] THEN
1691     COND_CASES_TAC THENL
1692      [UNDISCH_TAC `(@d. x2 = x1 + d) + y1 <= y1:hreal` THEN
1693       GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM HREAL_ADD_LID] THEN
1694       REWRITE_TAC[ONCE_REWRITE_RULE[HREAL_ADD_SYM] HREAL_LE_ADD_LCANCEL] THEN
1695       DISCH_TAC THEN SUBGOAL_THEN `(@d. x2 = x1 + d) = &0` MP_TAC THENL
1696        [ASM_REWRITE_TAC[GSYM HREAL_LE_ANTISYM] THEN
1697         GEN_REWRITE_TAC RAND_CONV [GSYM HREAL_ADD_LID] THEN
1698         REWRITE_TAC[HREAL_LE_ADD];
1699         DISCH_THEN SUBST_ALL_TAC THEN
1700         UNDISCH_TAC `x1 + & 0 = x2` THEN
1701         ASM_REWRITE_TAC[HREAL_ADD_RID]];
1702       GEN_REWRITE_TAC (funpow 3 RAND_CONV o BINDER_CONV o LAND_CONV)
1703         [HREAL_ADD_SYM] THEN
1704       REWRITE_TAC[HREAL_EQ_ADD_LCANCEL; TREAL_EQ_REFL]]]);;
1705
1706 (* ------------------------------------------------------------------------- *)
1707 (* Now define the quotient type -- the reals at last!                        *)
1708 (* ------------------------------------------------------------------------- *)
1709
1710 let real_tybij =
1711   define_quotient_type "real" ("mk_real","dest_real") `(treal_eq)`;;
1712
1713 let real_of_num,real_of_num_th =
1714   lift_function (snd real_tybij) (TREAL_EQ_REFL,TREAL_EQ_TRANS)
1715   "real_of_num" TREAL_OF_NUM_WELLDEF;;
1716
1717 let real_neg,real_neg_th =
1718   lift_function (snd real_tybij) (TREAL_EQ_REFL,TREAL_EQ_TRANS)
1719   "real_neg" TREAL_NEG_WELLDEF;;
1720
1721 let real_add,real_add_th =
1722   lift_function (snd real_tybij) (TREAL_EQ_REFL,TREAL_EQ_TRANS)
1723   "real_add" TREAL_ADD_WELLDEF;;
1724
1725 let real_mul,real_mul_th =
1726   lift_function (snd real_tybij) (TREAL_EQ_REFL,TREAL_EQ_TRANS)
1727   "real_mul" TREAL_MUL_WELLDEF;;
1728
1729 let real_le,real_le_th =
1730   lift_function (snd real_tybij) (TREAL_EQ_REFL,TREAL_EQ_TRANS)
1731   "real_le" TREAL_LE_WELLDEF;;
1732
1733 let real_inv,real_inv_th =
1734   lift_function (snd real_tybij) (TREAL_EQ_REFL,TREAL_EQ_TRANS)
1735   "real_inv" TREAL_INV_WELLDEF;;
1736
1737 let [REAL_ADD_SYM; REAL_ADD_ASSOC; REAL_ADD_LID; REAL_ADD_LINV;
1738      REAL_MUL_SYM; REAL_MUL_ASSOC; REAL_MUL_LID;
1739      REAL_ADD_LDISTRIB;
1740      REAL_LE_REFL; REAL_LE_ANTISYM; REAL_LE_TRANS; REAL_LE_TOTAL;
1741      REAL_LE_LADD_IMP; REAL_LE_MUL;
1742      REAL_INV_0; REAL_MUL_LINV;
1743      REAL_OF_NUM_EQ; REAL_OF_NUM_LE; REAL_OF_NUM_ADD; REAL_OF_NUM_MUL] =
1744   map
1745     (lift_theorem real_tybij (TREAL_EQ_REFL,TREAL_EQ_SYM,TREAL_EQ_TRANS)
1746       [real_of_num_th; real_neg_th; real_add_th;
1747        real_mul_th; real_le_th; real_inv_th])
1748     [TREAL_ADD_SYM; TREAL_ADD_ASSOC; TREAL_ADD_LID; TREAL_ADD_LINV;
1749      TREAL_MUL_SYM; TREAL_MUL_ASSOC; TREAL_MUL_LID;
1750      TREAL_ADD_LDISTRIB;
1751      TREAL_LE_REFL; TREAL_LE_ANTISYM; TREAL_LE_TRANS; TREAL_LE_TOTAL;
1752      TREAL_LE_LADD_IMP; TREAL_LE_MUL;
1753      TREAL_INV_0; TREAL_MUL_LINV;
1754      TREAL_OF_NUM_EQ; TREAL_OF_NUM_LE; TREAL_OF_NUM_ADD; TREAL_OF_NUM_MUL];;
1755
1756 (* ------------------------------------------------------------------------- *)
1757 (* Set up a friendly interface.                                              *)
1758 (* ------------------------------------------------------------------------- *)
1759
1760 parse_as_prefix "--";;
1761 parse_as_infix ("/",(22,"left"));;
1762 parse_as_infix ("pow",(24,"left"));;
1763
1764 do_list overload_interface
1765  ["+",`real_add:real->real->real`; "-",`real_sub:real->real->real`;
1766   "*",`real_mul:real->real->real`; "/",`real_div:real->real->real`;
1767   "<",`real_lt:real->real->bool`; "<=",`real_le:real->real->bool`;
1768   ">",`real_gt:real->real->bool`; ">=",`real_ge:real->real->bool`;
1769   "--",`real_neg:real->real`; "pow",`real_pow:real->num->real`;
1770   "inv",`real_inv:real->real`; "abs",`real_abs:real->real`;
1771   "max",`real_max:real->real->real`; "min",`real_min:real->real->real`;
1772   "&",`real_of_num:num->real`];;
1773
1774 let prioritize_real() = prioritize_overload(mk_type("real",[]));;
1775
1776 (* ------------------------------------------------------------------------- *)
1777 (* Additional definitions.                                                   *)
1778 (* ------------------------------------------------------------------------- *)
1779
1780 let real_sub = new_definition
1781   `x - y = x + --y`;;
1782
1783 let real_lt = new_definition
1784   `x < y <=> ~(y <= x)`;;
1785
1786 let real_ge = new_definition
1787   `x >= y <=> y <= x`;;
1788
1789 let real_gt = new_definition
1790   `x > y <=> y < x`;;
1791
1792 let real_abs = new_definition
1793   `abs(x) = if &0 <= x then x else --x`;;
1794
1795 let real_pow = new_recursive_definition num_RECURSION
1796   `(x pow 0 = &1) /\
1797    (!n. x pow (SUC n) = x * (x pow n))`;;
1798
1799 let real_div = new_definition
1800   `x / y = x * inv(y)`;;
1801
1802 let real_max = new_definition
1803   `real_max m n = if m <= n then n else m`;;
1804
1805 let real_min = new_definition
1806   `real_min m n = if m <= n then m else n`;;
1807
1808 (*----------------------------------------------------------------------------*)
1809 (* Derive the supremum property for an arbitrary bounded nonempty set         *)
1810 (*----------------------------------------------------------------------------*)
1811
1812 let REAL_HREAL_LEMMA1 = prove
1813  (`?r:hreal->real.
1814        (!x. &0 <= x <=> ?y. x = r y) /\
1815        (!y z. y <= z <=> r y <= r z)`,
1816   EXISTS_TAC `\y. mk_real((treal_eq)(y,hreal_of_num 0))` THEN
1817   REWRITE_TAC[GSYM real_le_th] THEN
1818   REWRITE_TAC[treal_le; HREAL_ADD_LID; HREAL_ADD_RID] THEN
1819   GEN_TAC THEN EQ_TAC THENL
1820    [MP_TAC(INST [`dest_real x`,`r:hreal#hreal->bool`] (snd real_tybij)) THEN
1821     REWRITE_TAC[fst real_tybij] THEN
1822     DISCH_THEN(X_CHOOSE_THEN `p:hreal#hreal` MP_TAC) THEN
1823     DISCH_THEN(MP_TAC o AP_TERM `mk_real`) THEN
1824     REWRITE_TAC[fst real_tybij] THEN DISCH_THEN SUBST1_TAC THEN
1825     REWRITE_TAC[GSYM real_of_num_th; GSYM real_le_th] THEN
1826     SUBST1_TAC(GSYM(ISPEC `p:hreal#hreal` PAIR)) THEN
1827     PURE_REWRITE_TAC[treal_of_num; treal_le] THEN
1828     PURE_REWRITE_TAC[HREAL_ADD_LID; HREAL_ADD_RID] THEN
1829     DISCH_THEN(X_CHOOSE_THEN `d:hreal` SUBST1_TAC o
1830       MATCH_MP HREAL_LE_EXISTS) THEN
1831     EXISTS_TAC `d:hreal` THEN AP_TERM_TAC THEN
1832     ONCE_REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `q:hreal#hreal` THEN
1833     SUBST1_TAC(GSYM(ISPEC `q:hreal#hreal` PAIR)) THEN
1834     PURE_REWRITE_TAC[treal_eq] THEN
1835     GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [HREAL_ADD_SYM] THEN
1836     REWRITE_TAC[GSYM HREAL_ADD_ASSOC; HREAL_EQ_ADD_LCANCEL] THEN
1837     REWRITE_TAC[HREAL_ADD_RID];
1838     DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN
1839     REWRITE_TAC[GSYM real_of_num_th; GSYM real_le_th] THEN
1840     REWRITE_TAC[treal_of_num; treal_le] THEN
1841     REWRITE_TAC[HREAL_ADD_LID; HREAL_ADD_RID] THEN
1842     GEN_REWRITE_TAC RAND_CONV [GSYM HREAL_ADD_LID] THEN
1843     REWRITE_TAC[HREAL_LE_ADD]]);;
1844
1845 let REAL_HREAL_LEMMA2 = prove
1846  (`?h r. (!x:hreal. h(r x) = x) /\
1847          (!x. &0 <= x ==> (r(h x) = x)) /\
1848          (!x:hreal. &0 <= r x) /\
1849          (!x y. x <= y <=> r x <= r y)`,
1850   STRIP_ASSUME_TAC REAL_HREAL_LEMMA1 THEN
1851   EXISTS_TAC `\x:real. @y:hreal. x = r y` THEN
1852   EXISTS_TAC `r:hreal->real` THEN
1853   ASM_REWRITE_TAC[BETA_THM] THEN
1854   SUBGOAL_THEN `!y z. ((r:hreal->real) y = r z) <=> (y = z)` ASSUME_TAC THENL
1855    [ASM_REWRITE_TAC[GSYM REAL_LE_ANTISYM; GSYM HREAL_LE_ANTISYM]; ALL_TAC] THEN
1856   ASM_REWRITE_TAC[GEN_REWRITE_RULE (LAND_CONV o BINDER_CONV) [EQ_SYM_EQ]
1857     (SPEC_ALL SELECT_REFL); GSYM EXISTS_REFL] THEN
1858   GEN_TAC THEN DISCH_THEN(ACCEPT_TAC o SYM o SELECT_RULE));;
1859
1860 let REAL_COMPLETE_SOMEPOS = prove
1861  (`!P. (?x. P x /\ &0 <= x) /\
1862        (?M. !x. P x ==> x <= M)
1863        ==> ?M. (!x. P x ==> x <= M) /\
1864                !M'. (!x. P x ==> x <= M') ==> M <= M'`,
1865   REPEAT STRIP_TAC THEN STRIP_ASSUME_TAC REAL_HREAL_LEMMA2 THEN
1866   MP_TAC(SPEC `\y:hreal. (P:real->bool)(r y)` HREAL_COMPLETE) THEN
1867   BETA_TAC THEN
1868   W(C SUBGOAL_THEN MP_TAC o funpow 2 (fst o dest_imp) o snd) THENL
1869    [CONJ_TAC THENL
1870      [EXISTS_TAC `(h:real->hreal) x` THEN
1871       UNDISCH_TAC `(P:real->bool) x` THEN
1872       MATCH_MP_TAC(TAUT `(b <=> a) ==> a ==> b`) THEN
1873       AP_TERM_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
1874       EXISTS_TAC `(h:real->hreal) M` THEN
1875       X_GEN_TAC `y:hreal` THEN DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
1876       ASM_REWRITE_TAC[] THEN
1877       MATCH_MP_TAC(TAUT `(b <=> a) ==> a ==> b`) THEN
1878       AP_TERM_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
1879       MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `x:real` THEN
1880       ASM_REWRITE_TAC[] THEN FIRST_ASSUM MATCH_MP_TAC THEN
1881       ASM_REWRITE_TAC[]];
1882     MATCH_MP_TAC(TAUT `(b ==> c) ==> a ==> (a ==> b) ==> c`) THEN
1883     DISCH_THEN(X_CHOOSE_THEN `B:hreal` STRIP_ASSUME_TAC)] THEN
1884   EXISTS_TAC `(r:hreal->real) B` THEN CONJ_TAC THENL
1885    [X_GEN_TAC `z:real` THEN DISCH_TAC THEN
1886     DISJ_CASES_TAC(SPECL [`&0`; `z:real`] REAL_LE_TOTAL) THENL
1887      [ANTE_RES_THEN(SUBST1_TAC o SYM) (ASSUME `&0 <= z`) THEN
1888       FIRST_ASSUM(fun th -> GEN_REWRITE_TAC I [GSYM th]) THEN
1889       FIRST_ASSUM MATCH_MP_TAC THEN
1890       UNDISCH_TAC `(P:real->bool) z` THEN
1891       MATCH_MP_TAC(TAUT `(b <=> a) ==> a ==> b`) THEN
1892       AP_TERM_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
1893       ASM_REWRITE_TAC[];
1894       MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&0` THEN
1895       ASM_REWRITE_TAC[]];
1896     X_GEN_TAC `C:real` THEN DISCH_TAC THEN
1897     SUBGOAL_THEN `B:hreal <= (h(C:real))` MP_TAC THENL
1898      [FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
1899       SUBGOAL_THEN `(r:hreal->real)(h C) = C` (fun th -> ASM_REWRITE_TAC[th]);
1900       ASM_REWRITE_TAC[] THEN MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC] THEN
1901     FIRST_ASSUM MATCH_MP_TAC THEN
1902     MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `x:real` THEN
1903     ASM_REWRITE_TAC[] THEN FIRST_ASSUM MATCH_MP_TAC THEN
1904     ASM_REWRITE_TAC[]]);;
1905
1906 let REAL_COMPLETE = prove
1907  (`!P. (?x. P x) /\
1908        (?M. !x. P x ==> x <= M)
1909        ==> ?M. (!x. P x ==> x <= M) /\
1910                !M'. (!x. P x ==> x <= M') ==> M <= M'`,
1911   let lemma = prove
1912    (`y = (y - x) + x`,
1913     REWRITE_TAC[real_sub; GSYM REAL_ADD_ASSOC; REAL_ADD_LINV] THEN
1914     ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN REWRITE_TAC[REAL_ADD_LID]) in
1915   REPEAT STRIP_TAC THEN
1916   DISJ_CASES_TAC (SPECL [`&0`; `x:real`] REAL_LE_TOTAL) THENL
1917    [MATCH_MP_TAC REAL_COMPLETE_SOMEPOS THEN CONJ_TAC THENL
1918      [EXISTS_TAC `x:real`; EXISTS_TAC `M:real`] THEN
1919     ASM_REWRITE_TAC[];
1920     FIRST_ASSUM(MP_TAC o MATCH_MP REAL_LE_LADD_IMP) THEN
1921     DISCH_THEN(MP_TAC o SPEC `--x`) THEN
1922     REWRITE_TAC[REAL_ADD_LINV] THEN
1923     ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN REWRITE_TAC[REAL_ADD_LID] THEN
1924     DISCH_TAC THEN
1925     MP_TAC(SPEC `\y. P(y + x) :bool` REAL_COMPLETE_SOMEPOS) THEN
1926     BETA_TAC THEN
1927     W(C SUBGOAL_THEN MP_TAC o funpow 2 (fst o dest_imp) o snd) THENL
1928      [CONJ_TAC THENL
1929        [EXISTS_TAC `&0` THEN ASM_REWRITE_TAC[REAL_LE_REFL; REAL_ADD_LID];
1930         EXISTS_TAC `M + --x` THEN GEN_TAC THEN
1931         DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
1932         DISCH_THEN(MP_TAC o SPEC `--x` o MATCH_MP REAL_LE_LADD_IMP) THEN
1933         DISCH_THEN(MP_TAC o ONCE_REWRITE_RULE[REAL_ADD_SYM]) THEN
1934         REWRITE_TAC[GSYM REAL_ADD_ASSOC] THEN
1935         REWRITE_TAC[ONCE_REWRITE_RULE[REAL_ADD_SYM] REAL_ADD_LINV] THEN
1936         REWRITE_TAC[ONCE_REWRITE_RULE[REAL_ADD_SYM] REAL_ADD_LID]];
1937       MATCH_MP_TAC(TAUT `(b ==> c) ==> a ==> (a ==> b) ==> c`) THEN
1938       DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC)] THEN
1939     EXISTS_TAC `B + x` THEN CONJ_TAC THENL
1940      [GEN_TAC THEN GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [lemma] THEN
1941       DISCH_THEN(ANTE_RES_THEN
1942         (MP_TAC o SPEC `x:real` o MATCH_MP REAL_LE_LADD_IMP)) THEN
1943       ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
1944       REWRITE_TAC[real_sub; GSYM REAL_ADD_ASSOC; REAL_ADD_LINV] THEN
1945       REWRITE_TAC[ONCE_REWRITE_RULE[REAL_ADD_SYM] REAL_ADD_LID] THEN
1946       REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
1947       ASM_REWRITE_TAC[];
1948       REPEAT STRIP_TAC THEN SUBGOAL_THEN `B <= M' - x` MP_TAC THENL
1949        [FIRST_ASSUM MATCH_MP_TAC THEN X_GEN_TAC `z:real` THEN DISCH_TAC THEN
1950         SUBGOAL_THEN `z + x <= M'` MP_TAC THENL
1951          [FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
1952           DISCH_THEN(MP_TAC o SPEC `--x` o MATCH_MP REAL_LE_LADD_IMP) THEN
1953           ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
1954           REWRITE_TAC[real_sub] THEN MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN
1955           AP_TERM_TAC THEN REWRITE_TAC[GSYM REAL_ADD_ASSOC] THEN
1956           REWRITE_TAC[ONCE_REWRITE_RULE[REAL_ADD_SYM] REAL_ADD_LINV] THEN
1957           REWRITE_TAC[ONCE_REWRITE_RULE[REAL_ADD_SYM] REAL_ADD_LID]];
1958          DISCH_THEN(MP_TAC o SPEC `x:real` o MATCH_MP REAL_LE_LADD_IMP) THEN
1959          MATCH_MP_TAC EQ_IMP THEN BINOP_TAC THENL
1960           [MATCH_ACCEPT_TAC REAL_ADD_SYM;
1961            ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN REWRITE_TAC[real_sub] THEN
1962            REWRITE_TAC[GSYM REAL_ADD_ASSOC; REAL_ADD_LINV] THEN
1963            REWRITE_TAC[ONCE_REWRITE_RULE[REAL_ADD_SYM] REAL_ADD_LID]]]]]);;
1964
1965 do_list reduce_interface
1966  ["+",`hreal_add:hreal->hreal->hreal`;
1967   "*",`hreal_mul:hreal->hreal->hreal`;
1968   "<=",`hreal_le:hreal->hreal->bool`;
1969   "inv",`hreal_inv:hreal->hreal`];;
1970
1971 do_list remove_interface ["**"; "++"; "<<="; "==="; "fn"; "afn"];;