1 needs "../formal_lp/arith/arith_hash2.hl";;
3 (* Based on the code of calc_int.ml *)
5 let test = Arith_hash2.test;;
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;;
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`;;
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`;;
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)));;
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)
47 failwith "my_dest_realintconst: --(&n) expected"
49 if (ltm = amp_op_real) then
52 failwith "my_dest_realintconst: &n expected";;
56 let is_neg_comb tm = is_comb tm && rator tm = neg_op_real;;
59 let replace_numerals = (rand o concl o DEPTH_CONV from_numeral);;
60 let REPLACE_NUMERALS = CONV_RULE (DEPTH_CONV from_numeral);;
63 let zero_const = replace_numerals `&0`;;
66 (***************************************)
70 let neg_0 = (REPLACE_NUMERALS o prove)(`-- &0 = &0`, REAL_ARITH_TAC) and
71 neg_neg = prove(`--(--(&n)) = &n`, REAL_ARITH_TAC);;
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
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
85 failwith "my_real_int_neg_conv: --(--(&n)) expected"
87 failwith "my_real_int_neg_conv: --x expected";;
91 let tm = `-- -- &12241`;;
94 test 100000 REAL_INT_NEG_CONV tm;;
96 test 100000 my_real_int_neg_conv tm;;
101 (***************************************)
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]);;
113 let my_real_int_add_conv =
114 let dest = dest_binop plus_op_real in
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
124 let m = rand(rand l) and n = rand r in
125 let m' = dest_num m and n' = dest_num n in
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
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
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
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
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
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
162 with Failure _ -> failwith "my_real_int_add_conv");;
166 let tm = `&3252375395 + --(&3454570237434)`;;
167 let tm' = replace_numerals tm;;
170 test 1000 REAL_INT_ADD_CONV tm;;
172 test 1000 my_real_int_add_conv tm';;
176 (****************************************)
180 let real_sub' = SPEC_ALL real_sub;;
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)
192 let th1 = my_real_int_add_conv (rand(concl th0)) in
197 let tm = `-- &35252352362346236236 - (-- &12236236363523)`;;
198 let tm' = replace_numerals tm;;
201 test 1000 REAL_INT_SUB_CONV tm;;
203 test 1000 my_real_int_sub_conv tm';;
209 (****************************************)
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]);;
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
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
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
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
248 let amp x = mk_comb(amp_op_real, x);;
249 let negate x = mk_comb(neg_op_real, x);;
251 let x = num_of_string "398537263103485";;
252 let y = num_of_string "243089539573957";;
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);;
260 test 100 REAL_INT_MUL_CONV (mk_binop mul_op_real (negate xxx) yyy);;
263 test 100 my_real_int_mul_conv (mk_binop mul_op_real (negate xx) yy);;
265 (DEPTH_CONV NUM_TO_NUMERAL_CONV) (concl(REAL_BITS_MUL_CONV (mk_binop mul_op_real xx yy)))