calc_int.ml

   1 (* ========================================================================= *)
   2 (* Calculation with integer-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 "realax.ml";;
  11
  12 (* ------------------------------------------------------------------------- *)
  13 (* Syntax operations on integer constants of type ":real".                   *)
  14 (* ------------------------------------------------------------------------- *)
  15
  16 let is_realintconst tm =
  17   match tm with
  18     Comb(Const("real_of_num",_),n) -> is_numeral n
  19   | Comb(Const("real_neg",_),Comb(Const("real_of_num",_),n)) ->
  20       is_numeral n & not(dest_numeral n = num_0)
  21   | _ -> false;;
  22
  23 let dest_realintconst tm =
  24   match tm with
  25     Comb(Const("real_of_num",_),n) -> dest_numeral n
  26   | Comb(Const("real_neg",_),Comb(Const("real_of_num",_),n)) ->
  27         let nn = dest_numeral n in
  28         if nn <>/ num_0 then minus_num(dest_numeral n)
  29         else failwith "dest_realintconst"
  30   | _ -> failwith "dest_realintconst";;
  31
  32 let mk_realintconst =
  33   let cast_tm = `real_of_num` and neg_tm = `(--)` in
  34   let mk_numconst n = mk_comb(cast_tm,mk_numeral n) in
  35   fun x -> if x </ num_0 then mk_comb(neg_tm,mk_numconst(minus_num x))
  36            else mk_numconst x;;
  37
  38 let is_ratconst tm =
  39   match tm with
  40     Comb(Comb(Const("real_div",_),p),q) ->
  41         is_realintconst p & is_realintconst q &
  42         (let m = dest_realintconst p and n = dest_realintconst q in
  43          n >/ num_1 & gcd_num m n =/ num_1)
  44   | _ -> is_realintconst tm;;
  45
  46 let rat_of_term tm =
  47   match tm with
  48     Comb(Comb(Const("real_div",_),p),q) ->
  49         let m = dest_realintconst p and n = dest_realintconst q in
  50         if n >/ num_1 & gcd_num m n =/ num_1 then m // n
  51         else failwith "rat_of_term"
  52   | _ -> dest_realintconst tm;;
  53
  54 let term_of_rat =
  55   let div_tm = `(/)` in
  56   fun x ->
  57     let p,q = numdom x in
  58     let ptm = mk_realintconst p in
  59     if q = num_1 then ptm
  60     else mk_comb(mk_comb(div_tm,ptm),mk_realintconst q);;
  61
  62 (* ------------------------------------------------------------------------- *)
  63 (* Some elementary "bootstrapping" lemmas we need below.                     *)
  64 (* ------------------------------------------------------------------------- *)
  65
  66 let REAL_ADD_AC = prove
  67  (`(m + n = n + m) /\
  68    ((m + n) + p = m + (n + p)) /\
  69    (m + (n + p) = n + (m + p))`,
  70   MESON_TAC[REAL_ADD_ASSOC; REAL_ADD_SYM]);;
  71
  72 let REAL_ADD_RINV = prove
  73  (`!x. x + --x = &0`,
  74   MESON_TAC[REAL_ADD_SYM; REAL_ADD_LINV]);;
  75
  76 let REAL_EQ_ADD_LCANCEL = prove
  77  (`!x y z. (x + y = x + z) <=> (y = z)`,
  78   REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
  79   POP_ASSUM(MP_TAC o AP_TERM `(+) (--x)`) THEN
  80   REWRITE_TAC[REAL_ADD_ASSOC; REAL_ADD_LINV; REAL_ADD_LID]);;
  81
  82 let REAL_EQ_ADD_RCANCEL = prove
  83  (`!x y z. (x + z = y + z) <=> (x = y)`,
  84   MESON_TAC[REAL_ADD_SYM; REAL_EQ_ADD_LCANCEL]);;
  85
  86 let REAL_MUL_RZERO = prove
  87  (`!x. x * &0 = &0`,
  88   MESON_TAC[REAL_EQ_ADD_RCANCEL; REAL_ADD_LDISTRIB; REAL_ADD_LID]);;
  89
  90 let REAL_MUL_LZERO = prove
  91  (`!x. &0 * x = &0`,
  92   MESON_TAC[REAL_MUL_SYM; REAL_MUL_RZERO]);;
  93
  94 let REAL_NEG_NEG = prove
  95  (`!x. --(--x) = x`,
  96   MESON_TAC
  97    [REAL_EQ_ADD_RCANCEL; REAL_ADD_LINV; REAL_ADD_SYM; REAL_ADD_LINV]);;
  98
  99 let REAL_MUL_RNEG = prove
 100  (`!x y. x * (--y) = -- (x * y)`,
 101   MESON_TAC[REAL_EQ_ADD_RCANCEL; REAL_ADD_LDISTRIB; REAL_ADD_LINV;
 102             REAL_MUL_RZERO]);;
 103
 104 let REAL_MUL_LNEG = prove
 105  (`!x y. (--x) * y = -- (x * y)`,
 106   MESON_TAC[REAL_MUL_SYM; REAL_MUL_RNEG]);;
 107
 108 let REAL_NEG_ADD = prove
 109  (`!x y. --(x + y) = --x + --y`,
 110   REPEAT GEN_TAC THEN
 111   MATCH_MP_TAC(GEN_ALL(fst(EQ_IMP_RULE(SPEC_ALL REAL_EQ_ADD_RCANCEL)))) THEN
 112   EXISTS_TAC `x + y` THEN REWRITE_TAC[REAL_ADD_LINV] THEN
 113   ONCE_REWRITE_TAC[AC REAL_ADD_AC `(a + b) + (c + d) = (a + c) + (b + d)`] THEN
 114   REWRITE_TAC[REAL_ADD_LINV; REAL_ADD_LID]);;
 115
 116 let REAL_ADD_RID = prove
 117  (`!x. x + &0 = x`,
 118   MESON_TAC[REAL_ADD_SYM; REAL_ADD_LID]);;
 119
 120 let REAL_NEG_0 = prove
 121  (`--(&0) = &0`,
 122   MESON_TAC[REAL_ADD_LINV; REAL_ADD_RID]);;
 123
 124 let REAL_LE_LNEG = prove
 125  (`!x y. --x <= y <=> &0 <= x + y`,
 126   REPEAT GEN_TAC THEN EQ_TAC THEN
 127   DISCH_THEN(MP_TAC o MATCH_MP REAL_LE_LADD_IMP) THENL
 128    [DISCH_THEN(MP_TAC o SPEC `x:real`) THEN
 129     REWRITE_TAC[ONCE_REWRITE_RULE[REAL_ADD_SYM] REAL_ADD_LINV];
 130     DISCH_THEN(MP_TAC o SPEC `--x`) THEN
 131     REWRITE_TAC[REAL_ADD_LINV; REAL_ADD_ASSOC; REAL_ADD_LID;
 132         ONCE_REWRITE_RULE[REAL_ADD_SYM] REAL_ADD_LID]]);;
 133
 134 let REAL_LE_NEG2 = prove
 135  (`!x y. --x <= --y <=> y <= x`,
 136   REPEAT GEN_TAC THEN
 137   GEN_REWRITE_TAC (RAND_CONV o LAND_CONV) [GSYM REAL_NEG_NEG] THEN
 138   REWRITE_TAC[REAL_LE_LNEG] THEN
 139   AP_TERM_TAC THEN MATCH_ACCEPT_TAC REAL_ADD_SYM);;
 140
 141 let REAL_LE_RNEG = prove
 142  (`!x y. x <= --y <=> x + y <= &0`,
 143   REPEAT GEN_TAC THEN
 144   GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [GSYM REAL_NEG_NEG] THEN
 145   REWRITE_TAC[REAL_LE_LNEG; GSYM REAL_NEG_ADD] THEN
 146   GEN_REWRITE_TAC RAND_CONV [GSYM REAL_LE_NEG2] THEN
 147   AP_THM_TAC THEN AP_TERM_TAC THEN
 148   REWRITE_TAC[GSYM REAL_ADD_LINV] THEN
 149   REWRITE_TAC[REAL_NEG_ADD; REAL_NEG_NEG] THEN
 150   MATCH_ACCEPT_TAC REAL_ADD_SYM);;
 151
 152 let REAL_OF_NUM_POW = prove
 153  (`!x n. (&x) pow n = &(x EXP n)`,
 154   GEN_TAC THEN INDUCT_TAC THEN
 155   ASM_REWRITE_TAC[real_pow; EXP; REAL_OF_NUM_MUL]);;
 156
 157 let REAL_POW_NEG = prove
 158  (`!x n. (--x) pow n = if EVEN n then x pow n else --(x pow n)`,
 159   GEN_TAC THEN INDUCT_TAC THEN
 160   ASM_REWRITE_TAC[real_pow; EVEN] THEN
 161   ASM_CASES_TAC `EVEN n` THEN
 162   ASM_REWRITE_TAC[REAL_MUL_RNEG; REAL_MUL_LNEG; REAL_NEG_NEG]);;
 163
 164 let REAL_ABS_NUM = prove
 165  (`!n. abs(&n) = &n`,
 166   REWRITE_TAC[real_abs; REAL_OF_NUM_LE; LE_0]);;
 167
 168 let REAL_ABS_NEG = prove
 169  (`!x. abs(--x) = abs x`,
 170   REWRITE_TAC[real_abs; REAL_LE_RNEG; REAL_NEG_NEG; REAL_ADD_LID] THEN
 171   MESON_TAC[REAL_LE_TOTAL; REAL_LE_ANTISYM; REAL_NEG_0]);;
 172
 173 (* ------------------------------------------------------------------------- *)
 174 (* First, the conversions on integer constants.                              *)
 175 (* ------------------------------------------------------------------------- *)
 176
 177 let REAL_INT_LE_CONV,REAL_INT_LT_CONV,
 178     REAL_INT_GE_CONV,REAL_INT_GT_CONV,REAL_INT_EQ_CONV =
 179   let tth =
 180     TAUT `(F /\ F <=> F) /\ (F /\ T <=> F) /\
 181           (T /\ F <=> F) /\ (T /\ T <=> T)` in
 182   let nth = TAUT `(~T <=> F) /\ (~F <=> T)` in
 183   let NUM2_EQ_CONV = BINOP_CONV NUM_EQ_CONV THENC GEN_REWRITE_CONV I [tth] in
 184   let NUM2_NE_CONV =
 185     RAND_CONV NUM2_EQ_CONV THENC
 186     GEN_REWRITE_CONV I [nth] in
 187   let [pth_le1; pth_le2a; pth_le2b; pth_le3] = (CONJUNCTS o prove)
 188    (`(--(&m) <= &n <=> T) /\
 189      (&m <= &n <=> m <= n) /\
 190      (--(&m) <= --(&n) <=> n <= m) /\
 191      (&m <= --(&n) <=> (m = 0) /\ (n = 0))`,
 192     REWRITE_TAC[REAL_LE_NEG2] THEN
 193     REWRITE_TAC[REAL_LE_LNEG; REAL_LE_RNEG] THEN
 194     REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_LE; LE_0] THEN
 195     REWRITE_TAC[LE; ADD_EQ_0]) in
 196   let REAL_INT_LE_CONV = FIRST_CONV
 197    [GEN_REWRITE_CONV I [pth_le1];
 198     GEN_REWRITE_CONV I [pth_le2a; pth_le2b] THENC NUM_LE_CONV;
 199     GEN_REWRITE_CONV I [pth_le3] THENC NUM2_EQ_CONV] in
 200   let [pth_lt1; pth_lt2a; pth_lt2b; pth_lt3] = (CONJUNCTS o prove)
 201    (`(&m < --(&n) <=> F) /\
 202      (&m < &n <=> m < n) /\
 203      (--(&m) < --(&n) <=> n < m) /\
 204      (--(&m) < &n <=> ~((m = 0) /\ (n = 0)))`,
 205     REWRITE_TAC[pth_le1; pth_le2a; pth_le2b; pth_le3;
 206                 GSYM NOT_LE; real_lt] THEN
 207     CONV_TAC TAUT) in
 208   let REAL_INT_LT_CONV = FIRST_CONV
 209    [GEN_REWRITE_CONV I [pth_lt1];
 210     GEN_REWRITE_CONV I [pth_lt2a; pth_lt2b] THENC NUM_LT_CONV;
 211     GEN_REWRITE_CONV I [pth_lt3] THENC NUM2_NE_CONV] in
 212   let [pth_ge1; pth_ge2a; pth_ge2b; pth_ge3] = (CONJUNCTS o prove)
 213    (`(&m >= --(&n) <=> T) /\
 214      (&m >= &n <=> n <= m) /\
 215      (--(&m) >= --(&n) <=> m <= n) /\
 216      (--(&m) >= &n <=> (m = 0) /\ (n = 0))`,
 217     REWRITE_TAC[pth_le1; pth_le2a; pth_le2b; pth_le3; real_ge] THEN
 218     CONV_TAC TAUT) in
 219   let REAL_INT_GE_CONV = FIRST_CONV
 220    [GEN_REWRITE_CONV I [pth_ge1];
 221     GEN_REWRITE_CONV I [pth_ge2a; pth_ge2b] THENC NUM_LE_CONV;
 222     GEN_REWRITE_CONV I [pth_ge3] THENC NUM2_EQ_CONV] in
 223   let [pth_gt1; pth_gt2a; pth_gt2b; pth_gt3] = (CONJUNCTS o prove)
 224    (`(--(&m) > &n <=> F) /\
 225      (&m > &n <=> n < m) /\
 226      (--(&m) > --(&n) <=> m < n) /\
 227      (&m > --(&n) <=> ~((m = 0) /\ (n = 0)))`,
 228     REWRITE_TAC[pth_lt1; pth_lt2a; pth_lt2b; pth_lt3; real_gt] THEN
 229     CONV_TAC TAUT) in
 230   let REAL_INT_GT_CONV = FIRST_CONV
 231    [GEN_REWRITE_CONV I [pth_gt1];
 232     GEN_REWRITE_CONV I [pth_gt2a; pth_gt2b] THENC NUM_LT_CONV;
 233     GEN_REWRITE_CONV I [pth_gt3] THENC NUM2_NE_CONV] in
 234   let [pth_eq1a; pth_eq1b; pth_eq2a; pth_eq2b] = (CONJUNCTS o prove)
 235    (`((&m = &n) <=> (m = n)) /\
 236      ((--(&m) = --(&n)) <=> (m = n)) /\
 237      ((--(&m) = &n) <=> (m = 0) /\ (n = 0)) /\
 238      ((&m = --(&n)) <=> (m = 0) /\ (n = 0))`,
 239     REWRITE_TAC[GSYM REAL_LE_ANTISYM; GSYM LE_ANTISYM] THEN
 240     REWRITE_TAC[pth_le1; pth_le2a; pth_le2b; pth_le3; LE; LE_0] THEN
 241     CONV_TAC TAUT) in
 242   let REAL_INT_EQ_CONV = FIRST_CONV
 243    [GEN_REWRITE_CONV I [pth_eq1a; pth_eq1b] THENC NUM_EQ_CONV;
 244     GEN_REWRITE_CONV I [pth_eq2a; pth_eq2b] THENC NUM2_EQ_CONV] in
 245   REAL_INT_LE_CONV,REAL_INT_LT_CONV,
 246   REAL_INT_GE_CONV,REAL_INT_GT_CONV,REAL_INT_EQ_CONV;;
 247
 248 let REAL_INT_NEG_CONV =
 249   let pth = prove
 250    (`(--(&0) = &0) /\
 251      (--(--(&x)) = &x)`,
 252     REWRITE_TAC[REAL_NEG_NEG; REAL_NEG_0]) in
 253   GEN_REWRITE_CONV I [pth];;
 254
 255 let REAL_INT_MUL_CONV =
 256   let pth0 = prove
 257    (`(&0 * &x = &0) /\
 258      (&0 * --(&x) = &0) /\
 259      (&x * &0 = &0) /\
 260      (--(&x) * &0 = &0)`,
 261     REWRITE_TAC[REAL_MUL_LZERO; REAL_MUL_RZERO])
 262   and pth1,pth2 = (CONJ_PAIR o prove)
 263    (`((&m * &n = &(m * n)) /\
 264       (--(&m) * --(&n) = &(m * n))) /\
 265      ((--(&m) * &n = --(&(m * n))) /\
 266       (&m * --(&n) = --(&(m * n))))`,
 267     REWRITE_TAC[REAL_MUL_LNEG; REAL_MUL_RNEG; REAL_NEG_NEG] THEN
 268     REWRITE_TAC[REAL_OF_NUM_MUL]) in
 269   FIRST_CONV
 270    [GEN_REWRITE_CONV I [pth0];
 271     GEN_REWRITE_CONV I [pth1] THENC RAND_CONV NUM_MULT_CONV;
 272     GEN_REWRITE_CONV I [pth2] THENC RAND_CONV(RAND_CONV NUM_MULT_CONV)];;
 273
 274 let REAL_INT_ADD_CONV =
 275   let neg_tm = `(--)` in
 276   let amp_tm = `&` in
 277   let add_tm = `(+)` in
 278   let dest = dest_binop `(+)` in
 279   let m_tm = `m:num` and n_tm = `n:num` in
 280   let pth0 = prove
 281    (`(--(&m) + &m = &0) /\
 282      (&m + --(&m) = &0)`,
 283     REWRITE_TAC[REAL_ADD_LINV; REAL_ADD_RINV]) in
 284   let [pth1; pth2; pth3; pth4; pth5; pth6] = (CONJUNCTS o prove)
 285    (`(--(&m) + --(&n) = --(&(m + n))) /\
 286      (--(&m) + &(m + n) = &n) /\
 287      (--(&(m + n)) + &m = --(&n)) /\
 288      (&(m + n) + --(&m) = &n) /\
 289      (&m + --(&(m + n)) = --(&n)) /\
 290      (&m + &n = &(m + n))`,
 291     REWRITE_TAC[GSYM REAL_OF_NUM_ADD; REAL_NEG_ADD] THEN
 292     REWRITE_TAC[REAL_ADD_ASSOC; REAL_ADD_LINV; REAL_ADD_LID] THEN
 293     REWRITE_TAC[REAL_ADD_RINV; REAL_ADD_LID] THEN
 294     ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
 295     REWRITE_TAC[REAL_ADD_ASSOC; REAL_ADD_LINV; REAL_ADD_LID] THEN
 296     REWRITE_TAC[REAL_ADD_RINV; REAL_ADD_LID]) in
 297   GEN_REWRITE_CONV I [pth0] ORELSEC
 298   (fun tm ->
 299     try let l,r = dest tm in
 300         if rator l = neg_tm then
 301           if rator r = neg_tm then
 302             let th1 = INST [rand(rand l),m_tm; rand(rand r),n_tm] pth1 in
 303             let tm1 = rand(rand(rand(concl th1))) in
 304             let th2 = AP_TERM neg_tm (AP_TERM amp_tm (NUM_ADD_CONV tm1)) in
 305             TRANS th1 th2
 306           else
 307             let m = rand(rand l) and n = rand r in
 308             let m' = dest_numeral m and n' = dest_numeral n in
 309             if m' <=/ n' then
 310               let p = mk_numeral (n' -/ m') in
 311               let th1 = INST [m,m_tm; p,n_tm] pth2 in
 312               let th2 = NUM_ADD_CONV (rand(rand(lhand(concl th1)))) in
 313               let th3 = AP_TERM (rator tm) (AP_TERM amp_tm (SYM th2)) in
 314               TRANS th3 th1
 315             else
 316               let p = mk_numeral (m' -/ n') in
 317               let th1 = INST [n,m_tm; p,n_tm] pth3 in
 318               let th2 = NUM_ADD_CONV (rand(rand(lhand(lhand(concl th1))))) in
 319               let th3 = AP_TERM neg_tm (AP_TERM amp_tm (SYM th2)) in
 320               let th4 = AP_THM (AP_TERM add_tm th3) (rand tm) in
 321               TRANS th4 th1
 322         else
 323           if rator r = neg_tm then
 324             let m = rand l and n = rand(rand r) in
 325             let m' = dest_numeral m and n' = dest_numeral n in
 326             if n' <=/ m' then
 327               let p = mk_numeral (m' -/ n') in
 328               let th1 = INST [n,m_tm; p,n_tm] pth4 in
 329               let th2 = NUM_ADD_CONV (rand(lhand(lhand(concl th1)))) in
 330               let th3 = AP_TERM add_tm (AP_TERM amp_tm (SYM th2)) in
 331               let th4 = AP_THM th3 (rand tm) in
 332               TRANS th4 th1
 333             else
 334              let p = mk_numeral (n' -/ m') in
 335              let th1 = INST [m,m_tm; p,n_tm] pth5 in
 336              let th2 = NUM_ADD_CONV (rand(rand(rand(lhand(concl th1))))) in
 337              let th3 = AP_TERM neg_tm (AP_TERM amp_tm (SYM th2)) in
 338              let th4 = AP_TERM (rator tm) th3 in
 339              TRANS th4 th1
 340           else
 341             let th1 = INST [rand l,m_tm; rand r,n_tm] pth6 in
 342             let tm1 = rand(rand(concl th1)) in
 343             let th2 = AP_TERM amp_tm (NUM_ADD_CONV tm1) in
 344             TRANS th1 th2
 345     with Failure _ -> failwith "REAL_INT_ADD_CONV");;
 346
 347 let REAL_INT_SUB_CONV =
 348   GEN_REWRITE_CONV I [real_sub] THENC
 349   TRY_CONV(RAND_CONV REAL_INT_NEG_CONV) THENC
 350   REAL_INT_ADD_CONV;;
 351
 352 let REAL_INT_POW_CONV =
 353   let pth1,pth2 = (CONJ_PAIR o prove)
 354    (`(&x pow n = &(x EXP n)) /\
 355      ((--(&x)) pow n = if EVEN n then &(x EXP n) else --(&(x EXP n)))`,
 356     REWRITE_TAC[REAL_OF_NUM_POW; REAL_POW_NEG]) in
 357   let tth = prove
 358    (`((if T then x:real else y) = x) /\ ((if F then x:real else y) = y)`,
 359     REWRITE_TAC[]) in
 360   let neg_tm = `(--)` in
 361   (GEN_REWRITE_CONV I [pth1] THENC RAND_CONV NUM_EXP_CONV) ORELSEC
 362   (GEN_REWRITE_CONV I [pth2] THENC
 363    RATOR_CONV(RATOR_CONV(RAND_CONV NUM_EVEN_CONV)) THENC
 364    GEN_REWRITE_CONV I [tth] THENC
 365    (fun tm -> if rator tm = neg_tm then RAND_CONV(RAND_CONV NUM_EXP_CONV) tm
 366               else RAND_CONV NUM_EXP_CONV  tm));;
 367
 368 let REAL_INT_ABS_CONV =
 369   let pth = prove
 370    (`(abs(--(&x)) = &x) /\
 371      (abs(&x) = &x)`,
 372     REWRITE_TAC[REAL_ABS_NEG; REAL_ABS_NUM]) in
 373   GEN_REWRITE_CONV I [pth];;
 374
 375 let REAL_INT_RED_CONV =
 376   let gconv_net = itlist (uncurry net_of_conv)
 377     [`x <= y`,REAL_INT_LE_CONV;
 378      `x < y`,REAL_INT_LT_CONV;
 379      `x >= y`,REAL_INT_GE_CONV;
 380      `x > y`,REAL_INT_GT_CONV;
 381      `x:real = y`,REAL_INT_EQ_CONV;
 382      `--x`,CHANGED_CONV REAL_INT_NEG_CONV;
 383      `abs(x)`,REAL_INT_ABS_CONV;
 384      `x + y`,REAL_INT_ADD_CONV;
 385      `x - y`,REAL_INT_SUB_CONV;
 386      `x * y`,REAL_INT_MUL_CONV;
 387      `x pow n`,REAL_INT_POW_CONV]
 388     (basic_net()) in
 389   REWRITES_CONV gconv_net;;
 390
 391 let REAL_INT_REDUCE_CONV = DEPTH_CONV REAL_INT_RED_CONV;;