calc_rat.ml

   1 (* ========================================================================= *)
   2 (* Calculation with rational-valued reals.                                   *)
   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 "real.ml";;
  11
  12 (* ------------------------------------------------------------------------- *)
  13 (* Constant for decimal fractions written #xxx.yyy                           *)
  14 (* ------------------------------------------------------------------------- *)
  15
  16 let DECIMAL = new_definition
  17   `DECIMAL x y = &x / &y`;;
  18
  19 (* ------------------------------------------------------------------------- *)
  20 (* Various handy lemmas.                                                     *)
  21 (* ------------------------------------------------------------------------- *)
  22
  23 let RAT_LEMMA1 = prove
  24  (`~(y1 = &0) /\ ~(y2 = &0) ==>
  25       ((x1 / y1) + (x2 / y2) = (x1 * y2 + x2 * y1) * inv(y1) * inv(y2))`,
  26   STRIP_TAC THEN REWRITE_TAC[real_div; REAL_ADD_RDISTRIB] THEN BINOP_TAC THENL
  27    [REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN AP_TERM_TAC THEN ONCE_REWRITE_TAC
  28      [AC REAL_MUL_AC `a * b * c = (b * a) * c`];
  29     REWRITE_TAC[REAL_MUL_ASSOC] THEN AP_THM_TAC THEN AP_TERM_TAC] THEN
  30   GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_RID] THEN
  31   REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN REWRITE_TAC[REAL_EQ_MUL_LCANCEL] THEN
  32   DISJ2_TAC THEN CONV_TAC SYM_CONV THEN MATCH_MP_TAC REAL_MUL_RINV THEN
  33   ASM_REWRITE_TAC[]);;
  34
  35 let RAT_LEMMA2 = prove
  36  (`&0 < y1 /\ &0 < y2 ==>
  37       ((x1 / y1) + (x2 / y2) = (x1 * y2 + x2 * y1) * inv(y1) * inv(y2))`,
  38   DISCH_TAC THEN MATCH_MP_TAC RAT_LEMMA1 THEN POP_ASSUM MP_TAC THEN
  39   ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
  40   REWRITE_TAC[DE_MORGAN_THM] THEN STRIP_TAC THEN
  41   ASM_REWRITE_TAC[REAL_LT_REFL]);;
  42
  43 let RAT_LEMMA3 = prove
  44  (`&0 < y1 /\ &0 < y2 ==>
  45       ((x1 / y1) - (x2 / y2) = (x1 * y2 - x2 * y1) * inv(y1) * inv(y2))`,
  46   DISCH_THEN(MP_TAC o GEN_ALL o MATCH_MP RAT_LEMMA2) THEN
  47   REWRITE_TAC[real_div] THEN DISCH_TAC THEN
  48   ASM_REWRITE_TAC[real_sub; GSYM REAL_MUL_LNEG]);;
  49
  50 let RAT_LEMMA4 = prove
  51  (`&0 < y1 /\ &0 < y2 ==> (x1 / y1 <= x2 / y2 <=> x1 * y2 <= x2 * y1)`,
  52   let lemma = prove
  53    (`&0 < y ==> (&0 <= x * y <=> &0 <= x)`,
  54     DISCH_TAC THEN EQ_TAC THEN DISCH_TAC THENL
  55      [SUBGOAL_THEN `&0 <= x * (y * inv y)` MP_TAC THENL
  56        [REWRITE_TAC[REAL_MUL_ASSOC] THEN MATCH_MP_TAC REAL_LE_MUL THEN
  57         ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_INV THEN
  58         MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[];
  59         SUBGOAL_THEN `y * inv y = &1` (fun th ->
  60           REWRITE_TAC[th; REAL_MUL_RID]) THEN
  61         MATCH_MP_TAC REAL_MUL_RINV THEN
  62         UNDISCH_TAC `&0 < y` THEN REAL_ARITH_TAC];
  63       MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[] THEN
  64       MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[]]) in
  65   ONCE_REWRITE_TAC[CONJ_SYM] THEN DISCH_TAC THEN
  66   ONCE_REWRITE_TAC[REAL_ARITH `a <= b <=> &0 <= b - a`] THEN
  67   FIRST_ASSUM(fun th -> REWRITE_TAC[MATCH_MP RAT_LEMMA3 th]) THEN
  68   MATCH_MP_TAC EQ_TRANS THEN
  69   EXISTS_TAC `&0 <= (x2 * y1 - x1 * y2) * inv y2` THEN
  70   REWRITE_TAC[REAL_MUL_ASSOC] THEN CONJ_TAC THEN
  71   MATCH_MP_TAC lemma THEN MATCH_MP_TAC REAL_LT_INV THEN
  72   ASM_REWRITE_TAC[]);;
  73
  74 let RAT_LEMMA5 = prove
  75  (`&0 < y1 /\ &0 < y2 ==> ((x1 / y1 = x2 / y2) <=> (x1 * y2 = x2 * y1))`,
  76   REPEAT DISCH_TAC THEN REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN
  77   MATCH_MP_TAC(TAUT `(a <=> a') /\ (b <=> b') ==> (a /\ b <=> a' /\ b')`) THEN
  78   CONJ_TAC THEN MATCH_MP_TAC RAT_LEMMA4 THEN ASM_REWRITE_TAC[]);;
  79
  80 (* ------------------------------------------------------------------------- *)
  81 (* Create trivial rational from integer or decimal, and postconvert back.    *)
  82 (* ------------------------------------------------------------------------- *)
  83
  84 let REAL_INT_RAT_CONV =
  85   let pth = prove
  86    (`(&x = &x / &1) /\
  87      (--(&x) = --(&x) / &1) /\
  88      (DECIMAL x y = &x / &y) /\
  89      (--(DECIMAL x y) = --(&x) / &y)`,
  90     REWRITE_TAC[REAL_DIV_1; DECIMAL] THEN
  91     REWRITE_TAC[real_div; REAL_MUL_LNEG]) in
  92   TRY_CONV(GEN_REWRITE_CONV I [pth]);;
  93
  94 (* ------------------------------------------------------------------------- *)
  95 (* Relational operations.                                                    *)
  96 (* ------------------------------------------------------------------------- *)
  97
  98 let REAL_RAT_LE_CONV =
  99   let pth = prove
 100    (`&0 < y1 ==> &0 < y2 ==> (x1 / y1 <= x2 / y2 <=> x1 * y2 <= x2 * y1)`,
 101     REWRITE_TAC[IMP_IMP; RAT_LEMMA4])
 102   and x1 = `x1:real` and x2 = `x2:real`
 103   and y1 = `y1:real` and y2 = `y2:real`
 104   and dest_le = dest_binop `(<=)`
 105   and dest_div = dest_binop `(/)` in
 106   let RAW_REAL_RAT_LE_CONV tm =
 107     let l,r = dest_le tm in
 108     let lx,ly = dest_div l
 109     and rx,ry = dest_div r in
 110     let th0 = INST [lx,x1; ly,y1; rx,x2; ry,y2] pth in
 111     let th1 = funpow 2 (MP_CONV REAL_INT_LT_CONV) th0 in
 112     let th2 = (BINOP_CONV REAL_INT_MUL_CONV THENC REAL_INT_LE_CONV)
 113               (rand(concl th1)) in
 114     TRANS th1 th2 in
 115    BINOP_CONV REAL_INT_RAT_CONV THENC RAW_REAL_RAT_LE_CONV;;
 116
 117 let REAL_RAT_LT_CONV =
 118   let pth = prove
 119    (`&0 < y1 ==> &0 < y2 ==> (x1 / y1 < x2 / y2 <=> x1 * y2 < x2 * y1)`,
 120     REWRITE_TAC[IMP_IMP] THEN
 121     GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [GSYM REAL_NOT_LE] THEN
 122     SIMP_TAC[TAUT `(~a <=> ~b) <=> (a <=> b)`; RAT_LEMMA4])
 123   and x1 = `x1:real` and x2 = `x2:real`
 124   and y1 = `y1:real` and y2 = `y2:real`
 125   and dest_lt = dest_binop `(<)`
 126   and dest_div = dest_binop `(/)` in
 127   let RAW_REAL_RAT_LT_CONV tm =
 128     let l,r = dest_lt tm in
 129     let lx,ly = dest_div l
 130     and rx,ry = dest_div r in
 131     let th0 = INST [lx,x1; ly,y1; rx,x2; ry,y2] pth in
 132     let th1 = funpow 2 (MP_CONV REAL_INT_LT_CONV) th0 in
 133     let th2 = (BINOP_CONV REAL_INT_MUL_CONV THENC REAL_INT_LT_CONV)
 134               (rand(concl th1)) in
 135     TRANS th1 th2 in
 136    BINOP_CONV REAL_INT_RAT_CONV THENC RAW_REAL_RAT_LT_CONV;;
 137
 138 let REAL_RAT_GE_CONV =
 139   GEN_REWRITE_CONV I [real_ge] THENC REAL_RAT_LE_CONV;;
 140
 141 let REAL_RAT_GT_CONV =
 142   GEN_REWRITE_CONV I [real_gt] THENC REAL_RAT_LT_CONV;;
 143
 144 let REAL_RAT_EQ_CONV =
 145   let pth = prove
 146    (`&0 < y1 ==> &0 < y2 ==> ((x1 / y1 = x2 / y2) <=> (x1 * y2 = x2 * y1))`,
 147     REWRITE_TAC[IMP_IMP; RAT_LEMMA5])
 148   and x1 = `x1:real` and x2 = `x2:real`
 149   and y1 = `y1:real` and y2 = `y2:real`
 150   and dest_eq = dest_binop `(=) :real->real->bool`
 151   and dest_div = dest_binop `(/)` in
 152   let RAW_REAL_RAT_EQ_CONV tm =
 153     let l,r = dest_eq tm in
 154     let lx,ly = dest_div l
 155     and rx,ry = dest_div r in
 156     let th0 = INST [lx,x1; ly,y1; rx,x2; ry,y2] pth in
 157     let th1 = funpow 2 (MP_CONV REAL_INT_LT_CONV) th0 in
 158     let th2 = (BINOP_CONV REAL_INT_MUL_CONV THENC REAL_INT_EQ_CONV)
 159               (rand(concl th1)) in
 160     TRANS th1 th2 in
 161    BINOP_CONV REAL_INT_RAT_CONV THENC RAW_REAL_RAT_EQ_CONV;;
 162
 163 (* ------------------------------------------------------------------------- *)
 164 (* The unary operations; all easy.                                           *)
 165 (* ------------------------------------------------------------------------- *)
 166
 167 let REAL_RAT_NEG_CONV =
 168   let pth = prove
 169    (`(--(&0) = &0) /\
 170      (--(--(&n)) = &n) /\
 171      (--(&m / &n) = --(&m) / &n) /\
 172      (--(--(&m) / &n) = &m / &n) /\
 173      (--(DECIMAL m n) = --(&m) / &n)`,
 174     REWRITE_TAC[real_div; REAL_INV_NEG; REAL_MUL_LNEG; REAL_NEG_NEG;
 175      REAL_NEG_0; DECIMAL])
 176   and ptm = `(--)` in
 177   let conv1 = GEN_REWRITE_CONV I [pth] in
 178   fun tm -> try conv1 tm
 179             with Failure _ -> try
 180                 let l,r = dest_comb tm in
 181                 if l = ptm & is_realintconst r & dest_realintconst r >/ num_0
 182                 then REFL tm
 183                 else fail()
 184             with Failure _ -> failwith "REAL_RAT_NEG_CONV";;
 185
 186 let REAL_RAT_ABS_CONV =
 187   let pth = prove
 188    (`(abs(&n) = &n) /\
 189      (abs(--(&n)) = &n) /\
 190      (abs(&m / &n) = &m / &n) /\
 191      (abs(--(&m) / &n) = &m / &n) /\
 192      (abs(DECIMAL m n) = &m / &n) /\
 193      (abs(--(DECIMAL m n)) = &m / &n)`,
 194     REWRITE_TAC[DECIMAL; REAL_ABS_DIV; REAL_ABS_NEG; REAL_ABS_NUM]) in
 195   GEN_REWRITE_CONV I [pth];;
 196
 197 let REAL_RAT_INV_CONV =
 198   let pth1 = prove
 199    (`(inv(&0) = &0) /\
 200      (inv(&1) = &1) /\
 201      (inv(-- &1) = --(&1)) /\
 202      (inv(&1 / &n) = &n) /\
 203      (inv(-- &1 / &n) = -- &n)`,
 204     REWRITE_TAC[REAL_INV_0; REAL_INV_1; REAL_INV_NEG;
 205                 REAL_INV_DIV; REAL_DIV_1] THEN
 206     REWRITE_TAC[real_div; REAL_INV_NEG; REAL_MUL_RNEG; REAL_INV_1;
 207                 REAL_MUL_RID])
 208   and pth2 = prove
 209    (`(inv(&n) = &1 / &n) /\
 210      (inv(--(&n)) = --(&1) / &n) /\
 211      (inv(&m / &n) = &n / &m) /\
 212      (inv(--(&m) / &n) = --(&n) / &m) /\
 213      (inv(DECIMAL m n) = &n / &m) /\
 214      (inv(--(DECIMAL m n)) = --(&n) / &m)`,
 215     REWRITE_TAC[DECIMAL; REAL_INV_DIV] THEN
 216     REWRITE_TAC[REAL_INV_NEG; real_div; REAL_MUL_RNEG; REAL_MUL_AC;
 217       REAL_MUL_LID; REAL_MUL_LNEG; REAL_INV_MUL; REAL_INV_INV]) in
 218   GEN_REWRITE_CONV I [pth1] ORELSEC
 219   GEN_REWRITE_CONV I [pth2];;
 220
 221 (* ------------------------------------------------------------------------- *)
 222 (* Addition.                                                                 *)
 223 (* ------------------------------------------------------------------------- *)
 224
 225 let REAL_RAT_ADD_CONV =
 226   let pth = prove
 227    (`&0 < y1 ==> &0 < y2 ==> &0 < y3 ==>
 228      ((x1 * y2 + x2 * y1) * y3 = x3 * y1 * y2)
 229      ==> (x1 / y1 + x2 / y2 = x3 / y3)`,
 230     REPEAT DISCH_TAC THEN
 231     MP_TAC RAT_LEMMA2 THEN
 232     ASM_REWRITE_TAC[] THEN
 233     DISCH_THEN SUBST1_TAC THEN
 234     REWRITE_TAC[GSYM REAL_INV_MUL; GSYM real_div] THEN
 235     SUBGOAL_THEN `&0 < y1 * y2 /\ &0 < y3` MP_TAC THENL
 236      [ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LT_MUL THEN
 237       ASM_REWRITE_TAC[];
 238       DISCH_THEN(fun th -> ASM_REWRITE_TAC[MATCH_MP RAT_LEMMA5 th])])
 239   and dest_divop = dest_binop `(/)`
 240   and dest_addop = dest_binop `(+)`
 241   and x1 = `x1:real` and x2 = `x2:real` and x3 = `x3:real`
 242   and y1 = `y1:real` and y2 = `y2:real` and y3 = `y3:real` in
 243   let RAW_REAL_RAT_ADD_CONV tm =
 244     let r1,r2 = dest_addop tm in
 245     let x1',y1' = dest_divop r1
 246     and x2',y2' = dest_divop r2 in
 247     let x1n = dest_realintconst x1' and y1n = dest_realintconst y1'
 248     and x2n = dest_realintconst x2' and y2n = dest_realintconst y2' in
 249     let x3n = x1n */ y2n +/ x2n */ y1n
 250     and y3n = y1n */ y2n in
 251     let d = gcd_num x3n y3n in
 252     let x3n' = quo_num x3n d and y3n' = quo_num y3n d in
 253     let x3n'',y3n'' = if y3n' >/ Int 0 then x3n',y3n'
 254                       else minus_num x3n',minus_num y3n' in
 255     let x3' = mk_realintconst x3n'' and y3' = mk_realintconst y3n'' in
 256     let th0 = INST [x1',x1; y1',y1; x2',x2; y2',y2; x3',x3; y3',y3] pth in
 257     let th1 = funpow 3 (MP_CONV REAL_INT_LT_CONV) th0 in
 258     let tm2,tm3 = dest_eq(fst(dest_imp(concl th1))) in
 259     let th2 = (LAND_CONV (BINOP_CONV REAL_INT_MUL_CONV THENC
 260                           REAL_INT_ADD_CONV) THENC
 261                REAL_INT_MUL_CONV) tm2
 262     and th3 = (RAND_CONV REAL_INT_MUL_CONV THENC REAL_INT_MUL_CONV) tm3 in
 263     MP th1 (TRANS th2 (SYM th3)) in
 264    BINOP_CONV REAL_INT_RAT_CONV THENC
 265    RAW_REAL_RAT_ADD_CONV THENC TRY_CONV(GEN_REWRITE_CONV I [REAL_DIV_1]);;
 266
 267 (* ------------------------------------------------------------------------- *)
 268 (* Subtraction.                                                              *)
 269 (* ------------------------------------------------------------------------- *)
 270
 271 let REAL_RAT_SUB_CONV =
 272   let pth = prove
 273    (`x - y = x + --y`,
 274     REWRITE_TAC[real_sub]) in
 275   GEN_REWRITE_CONV I [pth] THENC
 276   RAND_CONV REAL_RAT_NEG_CONV THENC REAL_RAT_ADD_CONV;;
 277
 278 (* ------------------------------------------------------------------------- *)
 279 (* Multiplication.                                                           *)
 280 (* ------------------------------------------------------------------------- *)
 281
 282 let REAL_RAT_MUL_CONV =
 283   let pth_nocancel = prove
 284    (`(x1 / y1) * (x2 / y2) = (x1 * x2) / (y1 * y2)`,
 285     REWRITE_TAC[real_div; REAL_INV_MUL; REAL_MUL_AC])
 286   and pth_cancel = prove
 287    (`~(d1 = &0) /\ ~(d2 = &0) /\
 288      (d1 * u1 = x1) /\ (d2 * u2 = x2) /\
 289      (d2 * v1 = y1) /\ (d1 * v2 = y2)
 290      ==> ((x1 / y1) * (x2 / y2) = (u1 * u2) / (v1 * v2))`,
 291     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 292     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 293     DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN (SUBST1_TAC o SYM)) THEN
 294     ASM_REWRITE_TAC[real_div; REAL_INV_MUL] THEN
 295     ONCE_REWRITE_TAC[AC REAL_MUL_AC
 296      `((d1 * u1) * (id2 * iv1)) * ((d2 * u2) * id1 * iv2) =
 297       (u1 * u2) * (iv1 * iv2) * (id2 * d2) * (id1 * d1)`] THEN
 298     ASM_SIMP_TAC[REAL_MUL_LINV; REAL_MUL_RID])
 299   and dest_divop = dest_binop `(/)`
 300   and dest_mulop = dest_binop `(*)`
 301   and x1 = `x1:real` and x2 = `x2:real`
 302   and y1 = `y1:real` and y2 = `y2:real`
 303   and u1 = `u1:real` and u2 = `u2:real`
 304   and v1 = `v1:real` and v2 = `v2:real`
 305   and d1 = `d1:real` and d2 = `d2:real` in
 306   let RAW_REAL_RAT_MUL_CONV tm =
 307     let r1,r2 = dest_mulop tm in
 308     let x1',y1' = dest_divop r1
 309     and x2',y2' = dest_divop r2 in
 310     let x1n = dest_realintconst x1' and y1n = dest_realintconst y1'
 311     and x2n = dest_realintconst x2' and y2n = dest_realintconst y2' in
 312     let d1n = gcd_num x1n y2n
 313     and d2n = gcd_num x2n y1n in
 314     if d1n = num_1 & d2n = num_1 then
 315       let th0 = INST [x1',x1; y1',y1; x2',x2; y2',y2] pth_nocancel in
 316       let th1 = BINOP_CONV REAL_INT_MUL_CONV (rand(concl th0)) in
 317       TRANS th0 th1
 318     else
 319       let u1n = quo_num x1n d1n
 320       and u2n = quo_num x2n d2n
 321       and v1n = quo_num y1n d2n
 322       and v2n = quo_num y2n d1n in
 323       let u1' = mk_realintconst u1n
 324       and u2' = mk_realintconst u2n
 325       and v1' = mk_realintconst v1n
 326       and v2' = mk_realintconst v2n
 327       and d1' = mk_realintconst d1n
 328       and d2' = mk_realintconst d2n in
 329       let th0 = INST [x1',x1; y1',y1; x2',x2; y2',y2;
 330                       u1',u1; v1',v1; u2',u2; v2',v2; d1',d1; d2',d2]
 331                      pth_cancel in
 332       let th1 = EQT_ELIM(REAL_INT_REDUCE_CONV(lhand(concl th0))) in
 333       let th2 = MP th0 th1 in
 334       let th3 = BINOP_CONV REAL_INT_MUL_CONV (rand(concl th2)) in
 335       TRANS th2 th3 in
 336    BINOP_CONV REAL_INT_RAT_CONV THENC
 337    RAW_REAL_RAT_MUL_CONV THENC TRY_CONV(GEN_REWRITE_CONV I [REAL_DIV_1]);;
 338
 339 (* ------------------------------------------------------------------------- *)
 340 (* Division.                                                                 *)
 341 (* ------------------------------------------------------------------------- *)
 342
 343 let REAL_RAT_DIV_CONV =
 344   let pth = prove
 345    (`x / y = x * inv(y)`,
 346     REWRITE_TAC[real_div]) in
 347   GEN_REWRITE_CONV I [pth] THENC
 348   RAND_CONV REAL_RAT_INV_CONV THENC REAL_RAT_MUL_CONV;;
 349
 350 (* ------------------------------------------------------------------------- *)
 351 (* Powers.                                                                   *)
 352 (* ------------------------------------------------------------------------- *)
 353
 354 let REAL_RAT_POW_CONV =
 355   let pth = prove
 356    (`(x / y) pow n = (x pow n) / (y pow n)`,
 357     REWRITE_TAC[REAL_POW_DIV]) in
 358   REAL_INT_POW_CONV ORELSEC
 359   (LAND_CONV REAL_INT_RAT_CONV THENC
 360    GEN_REWRITE_CONV I [pth] THENC
 361    BINOP_CONV REAL_INT_POW_CONV);;
 362
 363 (* ------------------------------------------------------------------------- *)
 364 (* Max and min.                                                              *)
 365 (* ------------------------------------------------------------------------- *)
 366
 367 let REAL_RAT_MAX_CONV =
 368   REWR_CONV real_max THENC
 369   RATOR_CONV(RATOR_CONV(RAND_CONV REAL_RAT_LE_CONV)) THENC
 370   GEN_REWRITE_CONV I [COND_CLAUSES];;
 371
 372 let REAL_RAT_MIN_CONV =
 373   REWR_CONV real_min THENC
 374   RATOR_CONV(RATOR_CONV(RAND_CONV REAL_RAT_LE_CONV)) THENC
 375   GEN_REWRITE_CONV I [COND_CLAUSES];;
 376
 377 (* ------------------------------------------------------------------------- *)
 378 (* Everything.                                                               *)
 379 (* ------------------------------------------------------------------------- *)
 380
 381 let REAL_RAT_RED_CONV =
 382   let gconv_net = itlist (uncurry net_of_conv)
 383     [`x <= y`,REAL_RAT_LE_CONV;
 384      `x < y`,REAL_RAT_LT_CONV;
 385      `x >= y`,REAL_RAT_GE_CONV;
 386      `x > y`,REAL_RAT_GT_CONV;
 387      `x:real = y`,REAL_RAT_EQ_CONV;
 388      `--x`,CHANGED_CONV REAL_RAT_NEG_CONV;
 389      `abs(x)`,REAL_RAT_ABS_CONV;
 390      `inv(x)`,REAL_RAT_INV_CONV;
 391      `x + y`,REAL_RAT_ADD_CONV;
 392      `x - y`,REAL_RAT_SUB_CONV;
 393      `x * y`,REAL_RAT_MUL_CONV;
 394      `x / y`,CHANGED_CONV REAL_RAT_DIV_CONV;
 395      `x pow n`,REAL_RAT_POW_CONV;
 396      `max x y`,REAL_RAT_MAX_CONV;
 397      `min x y`,REAL_RAT_MIN_CONV]
 398     (basic_net()) in
 399   REWRITES_CONV gconv_net;;
 400
 401 let REAL_RAT_REDUCE_CONV = DEPTH_CONV REAL_RAT_RED_CONV;;
 402
 403 (* ------------------------------------------------------------------------- *)
 404 (* Real normalizer dealing with rational constants.                          *)
 405 (* ------------------------------------------------------------------------- *)
 406
 407 let REAL_POLY_NEG_CONV,REAL_POLY_ADD_CONV,REAL_POLY_SUB_CONV,
 408     REAL_POLY_MUL_CONV,REAL_POLY_POW_CONV,REAL_POLY_CONV =
 409   SEMIRING_NORMALIZERS_CONV REAL_POLY_CLAUSES REAL_POLY_NEG_CLAUSES
 410    (is_ratconst,
 411     REAL_RAT_ADD_CONV,REAL_RAT_MUL_CONV,REAL_RAT_POW_CONV)
 412    (<);;
 413
 414 (* ------------------------------------------------------------------------- *)
 415 (* Extend normalizer to handle "inv" and division by rational constants, and *)
 416 (* normalize inside nested "max", "min" and "abs" terms.                     *)
 417 (* ------------------------------------------------------------------------- *)
 418
 419 let REAL_POLY_CONV =
 420   let neg_tm = `(--):real->real`
 421   and inv_tm = `inv:real->real`
 422   and add_tm = `(+):real->real->real`
 423   and sub_tm = `(-):real->real->real`
 424   and mul_tm = `(*):real->real->real`
 425   and div_tm = `(/):real->real->real`
 426   and pow_tm = `(pow):real->num->real`
 427   and abs_tm = `abs:real->real`
 428   and max_tm = `max:real->real->real`
 429   and min_tm = `min:real->real->real`
 430   and div_conv = REWR_CONV real_div in
 431   let rec REAL_POLY_CONV tm =
 432     if not(is_comb tm) or is_ratconst tm then REFL tm else
 433     let lop,r = dest_comb tm in
 434     if lop = neg_tm then
 435       let th1 = AP_TERM lop (REAL_POLY_CONV r) in
 436       TRANS th1 (REAL_POLY_NEG_CONV (rand(concl th1)))
 437     else if lop = inv_tm then
 438       let th1 = AP_TERM lop (REAL_POLY_CONV r) in
 439       TRANS th1 (TRY_CONV REAL_RAT_INV_CONV (rand(concl th1)))
 440     else if lop = abs_tm then
 441       AP_TERM lop (REAL_POLY_CONV r)
 442     else if not(is_comb lop) then REFL tm else
 443     let op,l = dest_comb lop in
 444     if op = pow_tm then
 445       let th1 = AP_THM (AP_TERM op (REAL_POLY_CONV l)) r in
 446       TRANS th1 (TRY_CONV REAL_POLY_POW_CONV (rand(concl th1)))
 447     else if op = add_tm or op = mul_tm or op = sub_tm then
 448       let th1 = MK_COMB(AP_TERM op (REAL_POLY_CONV l),
 449                         REAL_POLY_CONV r) in
 450       let fn = if op = add_tm then REAL_POLY_ADD_CONV
 451                else if op = mul_tm then REAL_POLY_MUL_CONV
 452                else REAL_POLY_SUB_CONV in
 453       TRANS th1 (fn (rand(concl th1)))
 454     else if op = div_tm then
 455       let th1 = div_conv tm in
 456       TRANS th1 (REAL_POLY_CONV (rand(concl th1)))
 457     else if op = min_tm or op = max_tm then
 458       MK_COMB(AP_TERM op (REAL_POLY_CONV l),REAL_POLY_CONV r)
 459     else REFL tm in
 460   REAL_POLY_CONV;;
 461
 462 (* ------------------------------------------------------------------------- *)
 463 (* Basic ring and ideal conversions.                                         *)
 464 (* ------------------------------------------------------------------------- *)
 465
 466 let REAL_RING,real_ideal_cofactors =
 467   let REAL_INTEGRAL = prove
 468    (`(!x. &0 * x = &0) /\
 469      (!x y z. (x + y = x + z) <=> (y = z)) /\
 470      (!w x y z. (w * y + x * z = w * z + x * y) <=> (w = x) \/ (y = z))`,
 471     REWRITE_TAC[MULT_CLAUSES; EQ_ADD_LCANCEL] THEN
 472     REWRITE_TAC[GSYM REAL_OF_NUM_EQ;
 473                 GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_MUL] THEN
 474     ONCE_REWRITE_TAC[GSYM REAL_SUB_0] THEN
 475     REWRITE_TAC[GSYM REAL_ENTIRE] THEN REAL_ARITH_TAC)
 476   and REAL_RABINOWITSCH = prove
 477    (`!x y:real. ~(x = y) <=> ?z. (x - y) * z = &1`,
 478     REPEAT GEN_TAC THEN
 479     GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM REAL_SUB_0] THEN
 480     MESON_TAC[REAL_MUL_RINV; REAL_MUL_LZERO; REAL_ARITH `~(&1 = &0)`])
 481   and init = GEN_REWRITE_CONV ONCE_DEPTH_CONV [DECIMAL]
 482   and real_ty = `:real` in
 483   let pure,ideal =
 484     RING_AND_IDEAL_CONV
 485         (rat_of_term,term_of_rat,REAL_RAT_EQ_CONV,
 486          `(--):real->real`,`(+):real->real->real`,`(-):real->real->real`,
 487          `(inv):real->real`,`(*):real->real->real`,`(/):real->real->real`,
 488          `(pow):real->num->real`,
 489          REAL_INTEGRAL,REAL_RABINOWITSCH,REAL_POLY_CONV) in
 490   (fun tm -> let th = init tm in EQ_MP (SYM th) (pure(rand(concl th)))),
 491   (fun tms tm -> if forall (fun t -> type_of t = real_ty) (tm::tms)
 492                  then ideal tms tm
 493                  else failwith
 494                    "real_ideal_cofactors: not all terms have type :real");;
 495
 496 (* ------------------------------------------------------------------------- *)
 497 (* Conversion for ideal membership.                                          *)
 498 (* ------------------------------------------------------------------------- *)
 499
 500 let REAL_IDEAL_CONV =
 501   let mk_add = mk_binop `( + ):real->real->real`
 502   and mk_mul = mk_binop `( * ):real->real->real` in
 503   fun tms tm ->
 504     let cfs = real_ideal_cofactors tms tm in
 505     let tm' = end_itlist mk_add (map2 mk_mul cfs tms) in
 506     let th = REAL_POLY_CONV tm and th' = REAL_POLY_CONV tm' in
 507     TRANS th (SYM th');;
 508
 509 (* ------------------------------------------------------------------------- *)
 510 (* Further specialize GEN_REAL_ARITH and REAL_ARITH (final versions).        *)
 511 (* ------------------------------------------------------------------------- *)
 512
 513 let GEN_REAL_ARITH PROVER =
 514   GEN_REAL_ARITH
 515    (term_of_rat,
 516     REAL_RAT_EQ_CONV,REAL_RAT_GE_CONV,REAL_RAT_GT_CONV,
 517     REAL_POLY_CONV,REAL_POLY_NEG_CONV,REAL_POLY_ADD_CONV,REAL_POLY_MUL_CONV,
 518     PROVER);;
 519
 520 let REAL_ARITH =
 521   let init = GEN_REWRITE_CONV ONCE_DEPTH_CONV [DECIMAL]
 522   and pure = GEN_REAL_ARITH REAL_LINEAR_PROVER in
 523   fun tm -> let th = init tm in EQ_MP (SYM th) (pure(rand(concl th)));;
 524
 525 let REAL_ARITH_TAC = CONV_TAC REAL_ARITH;;
 526
 527 let ASM_REAL_ARITH_TAC =
 528   REPEAT(FIRST_X_ASSUM(MP_TAC o check (not o is_forall o concl))) THEN
 529   REAL_ARITH_TAC;;
 530
 531 (* ------------------------------------------------------------------------- *)
 532 (* A simple "field" rule.                                                    *)
 533 (* ------------------------------------------------------------------------- *)
 534
 535 let REAL_FIELD =
 536   let prenex_conv =
 537     TOP_DEPTH_CONV BETA_CONV THENC
 538     PURE_REWRITE_CONV[FORALL_SIMP; EXISTS_SIMP; real_div;
 539                       REAL_INV_INV; REAL_INV_MUL; GSYM REAL_POW_INV] THENC
 540     NNFC_CONV THENC DEPTH_BINOP_CONV `(/\)` CONDS_CELIM_CONV THENC
 541     PRENEX_CONV THENC
 542     ONCE_REWRITE_CONV[REAL_ARITH `x < y <=> x < y /\ ~(x = y)`]
 543   and setup_conv = NNF_CONV THENC WEAK_CNF_CONV THENC CONJ_CANON_CONV
 544   and core_rule t = try REAL_RING t with Failure _ -> REAL_ARITH t
 545   and is_inv =
 546     let inv_tm = `inv:real->real`
 547     and is_div = is_binop `(/):real->real->real` in
 548     fun tm -> (is_div tm or (is_comb tm & rator tm = inv_tm)) &
 549               not(is_ratconst(rand tm)) in
 550   let BASIC_REAL_FIELD tm =
 551     let is_freeinv t = is_inv t & free_in t tm in
 552     let itms = setify(map rand (find_terms is_freeinv tm)) in
 553     let hyps = map (fun t -> SPEC t REAL_MUL_RINV) itms in
 554     let tm' = itlist (fun th t -> mk_imp(concl th,t)) hyps tm in
 555     let th1 = setup_conv tm' in
 556     let cjs = conjuncts(rand(concl th1)) in
 557     let ths = map core_rule cjs in
 558     let th2 = EQ_MP (SYM th1) (end_itlist CONJ ths) in
 559     rev_itlist (C MP) hyps th2 in
 560   fun tm ->
 561     let th0 = prenex_conv tm in
 562     let tm0 = rand(concl th0) in
 563     let avs,bod = strip_forall tm0 in
 564     let th1 = setup_conv bod in
 565     let ths = map BASIC_REAL_FIELD (conjuncts(rand(concl th1))) in
 566     EQ_MP (SYM th0) (GENL avs (EQ_MP (SYM th1) (end_itlist CONJ ths)));;