1 (* ========================================================================= *)
2 (* Calculation with integer-valued reals. *)
4 (* John Harrison, University of Cambridge Computer Laboratory *)
6 (* (c) Copyright, University of Cambridge 1998 *)
7 (* (c) Copyright, John Harrison 1998-2007 *)
8 (* ========================================================================= *)
12 (* ------------------------------------------------------------------------- *)
13 (* Syntax operations on integer constants of type ":real". *)
14 (* ------------------------------------------------------------------------- *)
16 let is_realintconst tm =
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)
23 let dest_realintconst tm =
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";;
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))
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;;
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;;
58 let ptm = mk_realintconst p in
60 else mk_comb(mk_comb(div_tm,ptm),mk_realintconst q);;
62 (* ------------------------------------------------------------------------- *)
63 (* Some elementary "bootstrapping" lemmas we need below. *)
64 (* ------------------------------------------------------------------------- *)
66 let REAL_ADD_AC = prove
68 ((m + n) + p = m + (n + p)) /\
69 (m + (n + p) = n + (m + p))`,
70 MESON_TAC[REAL_ADD_ASSOC; REAL_ADD_SYM]);;
72 let REAL_ADD_RINV = prove
74 MESON_TAC[REAL_ADD_SYM; REAL_ADD_LINV]);;
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]);;
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]);;
86 let REAL_MUL_RZERO = prove
88 MESON_TAC[REAL_EQ_ADD_RCANCEL; REAL_ADD_LDISTRIB; REAL_ADD_LID]);;
90 let REAL_MUL_LZERO = prove
92 MESON_TAC[REAL_MUL_SYM; REAL_MUL_RZERO]);;
94 let REAL_NEG_NEG = prove
97 [REAL_EQ_ADD_RCANCEL; REAL_ADD_LINV; REAL_ADD_SYM; REAL_ADD_LINV]);;
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;
104 let REAL_MUL_LNEG = prove
105 (`!x y. (--x) * y = -- (x * y)`,
106 MESON_TAC[REAL_MUL_SYM; REAL_MUL_RNEG]);;
108 let REAL_NEG_ADD = prove
109 (`!x y. --(x + y) = --x + --y`,
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]);;
116 let REAL_ADD_RID = prove
118 MESON_TAC[REAL_ADD_SYM; REAL_ADD_LID]);;
120 let REAL_NEG_0 = prove
122 MESON_TAC[REAL_ADD_LINV; REAL_ADD_RID]);;
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]]);;
134 let REAL_LE_NEG2 = prove
135 (`!x y. --x <= --y <=> y <= x`,
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);;
141 let REAL_LE_RNEG = prove
142 (`!x y. x <= --y <=> x + y <= &0`,
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);;
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]);;
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]);;
164 let REAL_ABS_NUM = prove
166 REWRITE_TAC[real_abs; REAL_OF_NUM_LE; LE_0]);;
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]);;
173 (* ------------------------------------------------------------------------- *)
174 (* First, the conversions on integer constants. *)
175 (* ------------------------------------------------------------------------- *)
177 let REAL_INT_LE_CONV,REAL_INT_LT_CONV,
178 REAL_INT_GE_CONV,REAL_INT_GT_CONV,REAL_INT_EQ_CONV =
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
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
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
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
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
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;;
248 let REAL_INT_NEG_CONV =
252 REWRITE_TAC[REAL_NEG_NEG; REAL_NEG_0]) in
253 GEN_REWRITE_CONV I [pth];;
255 let REAL_INT_MUL_CONV =
258 (&0 * --(&x) = &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
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)];;
274 let REAL_INT_ADD_CONV =
275 let neg_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
281 (`(--(&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
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
307 let m = rand(rand l) and n = rand r in
308 let m' = dest_numeral m and n' = dest_numeral n in
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
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
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
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
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
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
345 with Failure _ -> failwith "REAL_INT_ADD_CONV");;
347 let REAL_INT_SUB_CONV =
348 GEN_REWRITE_CONV I [real_sub] THENC
349 TRY_CONV(RAND_CONV REAL_INT_NEG_CONV) THENC
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
358 (`((if T then x:real else y) = x) /\ ((if F then x:real else y) = y)`,
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));;
368 let REAL_INT_ABS_CONV =
370 (`(abs(--(&x)) = &x) /\
372 REWRITE_TAC[REAL_ABS_NEG; REAL_ABS_NUM]) in
373 GEN_REWRITE_CONV I [pth];;
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]
389 REWRITES_CONV gconv_net;;
391 let REAL_INT_REDUCE_CONV = DEPTH_CONV REAL_INT_RED_CONV;;