formal_lp/more_arith/arith_int.hl

   1 needs "../formal_lp/hypermap/arith_link.hl";;
   2 needs "arith/nat.hl";;
   3 needs "misc/misc.hl";;
   4 needs "misc/vars.hl";;
   5
   6 (* Based on the code of calc_int.ml *)
   7
   8 module Arith_int :
   9   sig
  10     val my_mk_realintconst : num -> term
  11     val my_dest_realintconst : term -> num
  12     val my_real_int_neg_conv : term -> thm
  13     val my_real_int_add_conv : term -> thm
  14     val my_real_int_sub_conv : term -> thm
  15     val my_real_int_mul_conv : term -> thm
  16   end
  17   = struct
  18
  19 open Misc_vars;;
  20
  21 let test = Arith_misc.test;;
  22
  23 let to_numeral = Arith_nat.NUM_TO_NUMERAL_CONV;;
  24 let from_numeral = Arith_nat.NUMERAL_TO_NUM_CONV;;
  25 let mk_num = Arith_nat.mk_numeral_array;;
  26 let dest_num = Arith_hash.dest_numeral_hash;;
  27 let num_suc = Arith_nat.NUM_SUC_HASH_CONV;;
  28 let num_add = Arith_nat.NUM_ADD_HASH_CONV;;
  29 let num_mul = Arith_nat.NUM_MULT_HASH_CONV;;
  30 let num_gt0 = Arith_nat.NUM_GT0_HASH_CONV;;
  31
  32
  33 let my_mk_realintconst n =
  34   if n >=/ Int 0 then mk_comb(amp_op_real, mk_num n)
  35   else mk_comb(neg_op_real, mk_comb(amp_op_real, mk_num (minus_num n)));;
  36
  37
  38 let my_dest_realintconst tm =
  39   let ltm, rtm = dest_comb tm in
  40     if (ltm = neg_op_real) then
  41       let amp_tm, n_tm = dest_comb rtm in
  42         if (amp_tm = amp_op_real) then
  43           minus_num (dest_num n_tm)
  44         else
  45           failwith "my_dest_realintconst: --(&n) expected"
  46     else
  47       if (ltm = amp_op_real) then
  48         dest_num rtm
  49       else
  50         failwith "my_dest_realintconst: &n expected";;
  51
  52
  53
  54 let is_neg_comb tm = is_comb tm && rator tm = neg_op_real;;
  55
  56
  57 let replace_numerals = (rand o concl o DEPTH_CONV from_numeral);;
  58 let REPLACE_NUMERALS = CONV_RULE (DEPTH_CONV from_numeral);;
  59
  60
  61 let zero_const = replace_numerals `&0`;;
  62
  63
  64 (***************************************)
  65
  66 (* NEG *)
  67
  68 let neg_0 = (REPLACE_NUMERALS o prove)(`-- &0 = &0`, REAL_ARITH_TAC) and
  69     neg_neg = prove(`--(--(&n)) = &n`, REAL_ARITH_TAC);;
  70
  71
  72 let my_real_int_neg_conv tm =
  73   let neg_tm, rtm = dest_comb tm in
  74     if (neg_tm = neg_op_real) then
  75       if (rtm = zero_const) then
  76         neg_0
  77       else
  78         let neg_tm, rtm = dest_comb rtm in
  79         let amp_tm, n_tm = dest_comb rtm in
  80           if (neg_tm = neg_op_real && amp_tm = amp_op_real) then
  81             INST[n_tm, n_var_num] neg_neg
  82           else
  83             failwith "my_real_int_neg_conv: --(--(&n)) expected"
  84     else
  85       failwith "my_real_int_neg_conv: --x expected";;
  86
  87
  88 (*
  89 let tm = `-- -- &12241`;;
  90
  91 (* 1.880 *)
  92 test 100000 REAL_INT_NEG_CONV tm;;
  93 (* 0.292 *)
  94 test 100000 my_real_int_neg_conv tm;;
  95 *)
  96
  97
  98
  99 (***************************************)
 100
 101 (* ADD *)
 102
 103 let pth1 = prove(`(--(&m) + --(&n) = --(&(m + n)))`, REWRITE_TAC[GSYM REAL_OF_NUM_ADD; REAL_NEG_ADD]) and
 104     pth2 = prove(`(--(&m) + &(m + n) = &n)`, REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN REAL_ARITH_TAC) and
 105     pth3 = prove(`(--(&(m + n)) + &m = --(&n))`, REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN REAL_ARITH_TAC) and
 106     pth4 = prove(`(&(m + n) + --(&m) = &n)`, REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN REAL_ARITH_TAC) and
 107     pth5 = prove(`(&m + --(&(m + n)) = --(&n))`, REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN REAL_ARITH_TAC) and
 108     pth6 = prove(`(&m + &n = &(m + n))`, REWRITE_TAC[GSYM REAL_OF_NUM_ADD]);;
 109
 110
 111 let my_real_int_add_conv =
 112   let dest = dest_binop add_op_real in
 113   (fun tm ->
 114     try let l,r = dest tm in
 115         if rator l = neg_op_real then
 116           if rator r = neg_op_real then
 117             let th1 = INST [rand(rand l), m_var_num; rand(rand r), n_var_num] pth1 in
 118             let tm1 = rand(rand(rand(concl th1))) in
 119             let th2 = AP_TERM neg_op_real (AP_TERM amp_op_real (num_add tm1)) in
 120             TRANS th1 th2
 121           else
 122             let m = rand(rand l) and n = rand r in
 123             let m' = dest_num m and n' = dest_num n in
 124             if m' <=/ n' then
 125               let p = mk_num (n' -/ m') in
 126               let th1 = INST [m,m_var_num; p,n_var_num] pth2 in
 127               let th2 = num_add (rand(rand(lhand(concl th1)))) in
 128               let th3 = AP_TERM (rator tm) (AP_TERM amp_op_real (SYM th2)) in
 129               TRANS th3 th1
 130             else
 131               let p = mk_num (m' -/ n') in
 132               let th1 = INST [n,m_var_num; p,n_var_num] pth3 in
 133               let th2 = num_add (rand(rand(lhand(lhand(concl th1))))) in
 134               let th3 = AP_TERM neg_op_real (AP_TERM amp_op_real (SYM th2)) in
 135               let th4 = AP_THM (AP_TERM add_op_real th3) (rand tm) in
 136               TRANS th4 th1
 137         else
 138           if rator r = neg_op_real then
 139             let m = rand l and n = rand(rand r) in
 140             let m' = dest_num m and n' = dest_num n in
 141             if n' <=/ m' then
 142               let p = mk_num (m' -/ n') in
 143               let th1 = INST [n,m_var_num; p,n_var_num] pth4 in
 144               let th2 = num_add (rand(lhand(lhand(concl th1)))) in
 145               let th3 = AP_TERM add_op_real (AP_TERM amp_op_real (SYM th2)) in
 146               let th4 = AP_THM th3 (rand tm) in
 147               TRANS th4 th1
 148             else
 149              let p = mk_num (n' -/ m') in
 150              let th1 = INST [m,m_var_num; p,n_var_num] pth5 in
 151              let th2 = num_add (rand(rand(rand(lhand(concl th1))))) in
 152              let th3 = AP_TERM neg_op_real (AP_TERM amp_op_real (SYM th2)) in
 153              let th4 = AP_TERM (rator tm) th3 in
 154              TRANS th4 th1
 155           else
 156             let th1 = INST [rand l,m_var_num; rand r,n_var_num] pth6 in
 157             let tm1 = rand(rand(concl th1)) in
 158             let th2 = AP_TERM amp_op_real (num_add tm1) in
 159             TRANS th1 th2
 160     with Failure _ -> failwith "my_real_int_add_conv");;
 161
 162
 163 (*
 164 let tm = `&3252375395 + --(&3454570237434)`;;
 165 let tm' = replace_numerals tm;;
 166
 167 (* 1.192 *)
 168 test 1000 REAL_INT_ADD_CONV tm;;
 169 (* 0.224 *)
 170 test 1000 my_real_int_add_conv tm';;
 171 *)
 172
 173
 174 (****************************************)
 175
 176 (* SUB *)
 177
 178 let real_sub' = SPEC_ALL real_sub;;
 179
 180 let my_real_int_sub_conv tm =
 181   let x_tm, y_tm = dest_binop sub_op_real tm in
 182   let th0 = INST[x_tm, x_var_real; y_tm, y_var_real] real_sub' in
 183     if (is_neg_comb y_tm) then
 184       let ltm, rtm = dest_comb(rand(concl th0)) in
 185       let neg_th = my_real_int_neg_conv rtm in
 186       let th1 = AP_TERM ltm neg_th in
 187       let th2 = my_real_int_add_conv (rand(concl th1)) in
 188         TRANS th0 (TRANS th1 th2)
 189     else
 190       let th1 = my_real_int_add_conv (rand(concl th0)) in
 191         TRANS th0 th1;;
 192
 193
 194 (*
 195 let tm = `-- &35252352362346236236 - (-- &12236236363523)`;;
 196 let tm' = replace_numerals tm;;
 197
 198 (* 1.860 *)
 199 test 1000 REAL_INT_SUB_CONV tm;;
 200 (* 0.348 *)
 201 test 1000 my_real_int_sub_conv tm';;
 202 *)
 203
 204
 205
 206
 207 (****************************************)
 208
 209 (* MUL *)
 210
 211
 212 let mul_pp = prove(`&m * &n = &(m * n)`, REWRITE_TAC[REAL_OF_NUM_MUL]);;
 213 let mul_nn = prove(`--(&m) * --(&n) = &(m * n)`, REWRITE_TAC[REAL_NEG_MUL2; mul_pp]) and
 214     mul_np = prove(`--(&m) * &n = --(&(m * n))`, REWRITE_TAC[REAL_MUL_LNEG; mul_pp]) and
 215     mul_pn = prove(`&m * --(&n) = --(&(m * n))`, REWRITE_TAC[REAL_MUL_RNEG; mul_pp]);;
 216
 217
 218 let my_real_int_mul_conv tm =
 219   let l, r = dest_binop mul_op_real tm in
 220     if rator l = neg_op_real then
 221       if rator r = neg_op_real then
 222         let th1 = INST [rand(rand l), m_var_num; rand(rand r), n_var_num] mul_nn in
 223         let tm1 = rand(rand(concl th1)) in
 224         let th2 = AP_TERM amp_op_real (num_mul tm1) in
 225           TRANS th1 th2
 226       else
 227         let th1 = INST [rand(rand l), m_var_num; rand r, n_var_num] mul_np in
 228         let tm1 = rand(rand(rand(concl th1))) in
 229         let th2 = AP_TERM neg_op_real (AP_TERM amp_op_real (num_mul tm1)) in
 230           TRANS th1 th2
 231     else
 232       if rator r = neg_op_real then
 233         let th1 = INST[rand l, m_var_num; rand(rand r), n_var_num] mul_pn in
 234         let tm1 = rand(rand(rand(concl th1))) in
 235         let th2 = AP_TERM neg_op_real (AP_TERM amp_op_real (num_mul tm1)) in
 236           TRANS th1 th2
 237       else
 238         let th1 = INST[rand l, m_var_num; rand r, n_var_num] mul_pp in
 239         let tm1 = rand(rand(concl th1)) in
 240         let th2 = AP_TERM amp_op_real (num_mul tm1) in
 241           TRANS th1 th2;;
 242
 243
 244
 245 (*
 246 let amp x = mk_comb(amp_op_real, x);;
 247 let negate x = mk_comb(neg_op_real, x);;
 248
 249 let x = num_of_string "398537263103485";;
 250 let y = num_of_string "243089539573957";;
 251
 252
 253 let xx = amp (mk_num x) and yy = amp (mk_num y);;
 254 let xxx = amp (mk_numeral x) and yyy = amp (mk_numeral y);;
 255
 256
 257 (* 1.800 *)
 258 test 100 REAL_INT_MUL_CONV (mk_binop mul_op_real (negate xxx) yyy);;
 259
 260 (* 0.108 *)
 261 test 100 my_real_int_mul_conv (mk_binop mul_op_real (negate xx) yy);;
 262
 263 (DEPTH_CONV NUM_TO_NUMERAL_CONV) (concl(REAL_BITS_MUL_CONV (mk_binop mul_op_real xx yy)))
 264
 265 *)
 266
 267
 268
 269 end;;
 270
 271
 272
 273
 274
 275