formal_lp/old/arith/arith_hash_int.hl

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