1 (* ========================================================================= *)
2 (* Calculation with rational-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 (* Constant for decimal fractions written #xxx.yyy *)
14 (* ------------------------------------------------------------------------- *)
16 let DECIMAL = new_definition
17 `DECIMAL x y = &x / &y`;;
19 (* ------------------------------------------------------------------------- *)
20 (* Various handy lemmas. *)
21 (* ------------------------------------------------------------------------- *)
23 let RAT_LEMMA1 = prove
24 (`~(y1 = &0) /\ ~(y2 = &0) ==>
25 ((x1 / y1) + (x2 / y2) = (x1 * y2 + x2 * y1) * inv(y1) * inv(y2))`,
26 STRIP_TAC THEN REWRITE_TAC[real_div; REAL_ADD_RDISTRIB] THEN BINOP_TAC THENL
27 [REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN AP_TERM_TAC THEN ONCE_REWRITE_TAC
28 [AC REAL_MUL_AC `a * b * c = (b * a) * c`];
29 REWRITE_TAC[REAL_MUL_ASSOC] THEN AP_THM_TAC THEN AP_TERM_TAC] THEN
30 GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_RID] THEN
31 REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN REWRITE_TAC[REAL_EQ_MUL_LCANCEL] THEN
32 DISJ2_TAC THEN CONV_TAC SYM_CONV THEN MATCH_MP_TAC REAL_MUL_RINV THEN
35 let RAT_LEMMA2 = prove
36 (`&0 < y1 /\ &0 < y2 ==>
37 ((x1 / y1) + (x2 / y2) = (x1 * y2 + x2 * y1) * inv(y1) * inv(y2))`,
38 DISCH_TAC THEN MATCH_MP_TAC RAT_LEMMA1 THEN POP_ASSUM MP_TAC THEN
39 ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
40 REWRITE_TAC[DE_MORGAN_THM] THEN STRIP_TAC THEN
41 ASM_REWRITE_TAC[REAL_LT_REFL]);;
43 let RAT_LEMMA3 = prove
44 (`&0 < y1 /\ &0 < y2 ==>
45 ((x1 / y1) - (x2 / y2) = (x1 * y2 - x2 * y1) * inv(y1) * inv(y2))`,
46 DISCH_THEN(MP_TAC o GEN_ALL o MATCH_MP RAT_LEMMA2) THEN
47 REWRITE_TAC[real_div] THEN DISCH_TAC THEN
48 ASM_REWRITE_TAC[real_sub; GSYM REAL_MUL_LNEG]);;
50 let RAT_LEMMA4 = prove
51 (`&0 < y1 /\ &0 < y2 ==> (x1 / y1 <= x2 / y2 <=> x1 * y2 <= x2 * y1)`,
53 (`&0 < y ==> (&0 <= x * y <=> &0 <= x)`,
54 DISCH_TAC THEN EQ_TAC THEN DISCH_TAC THENL
55 [SUBGOAL_THEN `&0 <= x * (y * inv y)` MP_TAC THENL
56 [REWRITE_TAC[REAL_MUL_ASSOC] THEN MATCH_MP_TAC REAL_LE_MUL THEN
57 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_INV THEN
58 MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[];
59 SUBGOAL_THEN `y * inv y = &1` (fun th ->
60 REWRITE_TAC[th; REAL_MUL_RID]) THEN
61 MATCH_MP_TAC REAL_MUL_RINV THEN
62 UNDISCH_TAC `&0 < y` THEN REAL_ARITH_TAC];
63 MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[] THEN
64 MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[]]) in
65 ONCE_REWRITE_TAC[CONJ_SYM] THEN DISCH_TAC THEN
66 ONCE_REWRITE_TAC[REAL_ARITH `a <= b <=> &0 <= b - a`] THEN
67 FIRST_ASSUM(fun th -> REWRITE_TAC[MATCH_MP RAT_LEMMA3 th]) THEN
68 MATCH_MP_TAC EQ_TRANS THEN
69 EXISTS_TAC `&0 <= (x2 * y1 - x1 * y2) * inv y2` THEN
70 REWRITE_TAC[REAL_MUL_ASSOC] THEN CONJ_TAC THEN
71 MATCH_MP_TAC lemma THEN MATCH_MP_TAC REAL_LT_INV THEN
74 let RAT_LEMMA5 = prove
75 (`&0 < y1 /\ &0 < y2 ==> ((x1 / y1 = x2 / y2) <=> (x1 * y2 = x2 * y1))`,
76 REPEAT DISCH_TAC THEN REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN
77 MATCH_MP_TAC(TAUT `(a <=> a') /\ (b <=> b') ==> (a /\ b <=> a' /\ b')`) THEN
78 CONJ_TAC THEN MATCH_MP_TAC RAT_LEMMA4 THEN ASM_REWRITE_TAC[]);;
80 (* ------------------------------------------------------------------------- *)
81 (* Create trivial rational from integer or decimal, and postconvert back. *)
82 (* ------------------------------------------------------------------------- *)
84 let REAL_INT_RAT_CONV =
87 (--(&x) = --(&x) / &1) /\
88 (DECIMAL x y = &x / &y) /\
89 (--(DECIMAL x y) = --(&x) / &y)`,
90 REWRITE_TAC[REAL_DIV_1; DECIMAL] THEN
91 REWRITE_TAC[real_div; REAL_MUL_LNEG]) in
92 TRY_CONV(GEN_REWRITE_CONV I [pth]);;
94 (* ------------------------------------------------------------------------- *)
95 (* Relational operations. *)
96 (* ------------------------------------------------------------------------- *)
98 let REAL_RAT_LE_CONV =
100 (`&0 < y1 ==> &0 < y2 ==> (x1 / y1 <= x2 / y2 <=> x1 * y2 <= x2 * y1)`,
101 REWRITE_TAC[IMP_IMP; RAT_LEMMA4])
102 and x1 = `x1:real` and x2 = `x2:real`
103 and y1 = `y1:real` and y2 = `y2:real`
104 and dest_le = dest_binop `(<=)`
105 and dest_div = dest_binop `(/)` in
106 let RAW_REAL_RAT_LE_CONV tm =
107 let l,r = dest_le tm in
108 let lx,ly = dest_div l
109 and rx,ry = dest_div r in
110 let th0 = INST [lx,x1; ly,y1; rx,x2; ry,y2] pth in
111 let th1 = funpow 2 (MP_CONV REAL_INT_LT_CONV) th0 in
112 let th2 = (BINOP_CONV REAL_INT_MUL_CONV THENC REAL_INT_LE_CONV)
115 BINOP_CONV REAL_INT_RAT_CONV THENC RAW_REAL_RAT_LE_CONV;;
117 let REAL_RAT_LT_CONV =
119 (`&0 < y1 ==> &0 < y2 ==> (x1 / y1 < x2 / y2 <=> x1 * y2 < x2 * y1)`,
120 REWRITE_TAC[IMP_IMP] THEN
121 GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [GSYM REAL_NOT_LE] THEN
122 SIMP_TAC[TAUT `(~a <=> ~b) <=> (a <=> b)`; RAT_LEMMA4])
123 and x1 = `x1:real` and x2 = `x2:real`
124 and y1 = `y1:real` and y2 = `y2:real`
125 and dest_lt = dest_binop `(<)`
126 and dest_div = dest_binop `(/)` in
127 let RAW_REAL_RAT_LT_CONV tm =
128 let l,r = dest_lt tm in
129 let lx,ly = dest_div l
130 and rx,ry = dest_div r in
131 let th0 = INST [lx,x1; ly,y1; rx,x2; ry,y2] pth in
132 let th1 = funpow 2 (MP_CONV REAL_INT_LT_CONV) th0 in
133 let th2 = (BINOP_CONV REAL_INT_MUL_CONV THENC REAL_INT_LT_CONV)
136 BINOP_CONV REAL_INT_RAT_CONV THENC RAW_REAL_RAT_LT_CONV;;
138 let REAL_RAT_GE_CONV =
139 GEN_REWRITE_CONV I [real_ge] THENC REAL_RAT_LE_CONV;;
141 let REAL_RAT_GT_CONV =
142 GEN_REWRITE_CONV I [real_gt] THENC REAL_RAT_LT_CONV;;
144 let REAL_RAT_EQ_CONV =
146 (`&0 < y1 ==> &0 < y2 ==> ((x1 / y1 = x2 / y2) <=> (x1 * y2 = x2 * y1))`,
147 REWRITE_TAC[IMP_IMP; RAT_LEMMA5])
148 and x1 = `x1:real` and x2 = `x2:real`
149 and y1 = `y1:real` and y2 = `y2:real`
150 and dest_eq = dest_binop `(=) :real->real->bool`
151 and dest_div = dest_binop `(/)` in
152 let RAW_REAL_RAT_EQ_CONV tm =
153 let l,r = dest_eq tm in
154 let lx,ly = dest_div l
155 and rx,ry = dest_div r in
156 let th0 = INST [lx,x1; ly,y1; rx,x2; ry,y2] pth in
157 let th1 = funpow 2 (MP_CONV REAL_INT_LT_CONV) th0 in
158 let th2 = (BINOP_CONV REAL_INT_MUL_CONV THENC REAL_INT_EQ_CONV)
161 BINOP_CONV REAL_INT_RAT_CONV THENC RAW_REAL_RAT_EQ_CONV;;
163 (* ------------------------------------------------------------------------- *)
164 (* The unary operations; all easy. *)
165 (* ------------------------------------------------------------------------- *)
167 let REAL_RAT_NEG_CONV =
171 (--(&m / &n) = --(&m) / &n) /\
172 (--(--(&m) / &n) = &m / &n) /\
173 (--(DECIMAL m n) = --(&m) / &n)`,
174 REWRITE_TAC[real_div; REAL_INV_NEG; REAL_MUL_LNEG; REAL_NEG_NEG;
175 REAL_NEG_0; DECIMAL])
177 let conv1 = GEN_REWRITE_CONV I [pth] in
178 fun tm -> try conv1 tm
179 with Failure _ -> try
180 let l,r = dest_comb tm in
181 if l = ptm & is_realintconst r & dest_realintconst r >/ num_0
184 with Failure _ -> failwith "REAL_RAT_NEG_CONV";;
186 let REAL_RAT_ABS_CONV =
189 (abs(--(&n)) = &n) /\
190 (abs(&m / &n) = &m / &n) /\
191 (abs(--(&m) / &n) = &m / &n) /\
192 (abs(DECIMAL m n) = &m / &n) /\
193 (abs(--(DECIMAL m n)) = &m / &n)`,
194 REWRITE_TAC[DECIMAL; REAL_ABS_DIV; REAL_ABS_NEG; REAL_ABS_NUM]) in
195 GEN_REWRITE_CONV I [pth];;
197 let REAL_RAT_INV_CONV =
201 (inv(-- &1) = --(&1)) /\
202 (inv(&1 / &n) = &n) /\
203 (inv(-- &1 / &n) = -- &n)`,
204 REWRITE_TAC[REAL_INV_0; REAL_INV_1; REAL_INV_NEG;
205 REAL_INV_DIV; REAL_DIV_1] THEN
206 REWRITE_TAC[real_div; REAL_INV_NEG; REAL_MUL_RNEG; REAL_INV_1;
209 (`(inv(&n) = &1 / &n) /\
210 (inv(--(&n)) = --(&1) / &n) /\
211 (inv(&m / &n) = &n / &m) /\
212 (inv(--(&m) / &n) = --(&n) / &m) /\
213 (inv(DECIMAL m n) = &n / &m) /\
214 (inv(--(DECIMAL m n)) = --(&n) / &m)`,
215 REWRITE_TAC[DECIMAL; REAL_INV_DIV] THEN
216 REWRITE_TAC[REAL_INV_NEG; real_div; REAL_MUL_RNEG; REAL_MUL_AC;
217 REAL_MUL_LID; REAL_MUL_LNEG; REAL_INV_MUL; REAL_INV_INV]) in
218 GEN_REWRITE_CONV I [pth1] ORELSEC
219 GEN_REWRITE_CONV I [pth2];;
221 (* ------------------------------------------------------------------------- *)
223 (* ------------------------------------------------------------------------- *)
225 let REAL_RAT_ADD_CONV =
227 (`&0 < y1 ==> &0 < y2 ==> &0 < y3 ==>
228 ((x1 * y2 + x2 * y1) * y3 = x3 * y1 * y2)
229 ==> (x1 / y1 + x2 / y2 = x3 / y3)`,
230 REPEAT DISCH_TAC THEN
231 MP_TAC RAT_LEMMA2 THEN
232 ASM_REWRITE_TAC[] THEN
233 DISCH_THEN SUBST1_TAC THEN
234 REWRITE_TAC[GSYM REAL_INV_MUL; GSYM real_div] THEN
235 SUBGOAL_THEN `&0 < y1 * y2 /\ &0 < y3` MP_TAC THENL
236 [ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LT_MUL THEN
238 DISCH_THEN(fun th -> ASM_REWRITE_TAC[MATCH_MP RAT_LEMMA5 th])])
239 and dest_divop = dest_binop `(/)`
240 and dest_addop = dest_binop `(+)`
241 and x1 = `x1:real` and x2 = `x2:real` and x3 = `x3:real`
242 and y1 = `y1:real` and y2 = `y2:real` and y3 = `y3:real` in
243 let RAW_REAL_RAT_ADD_CONV tm =
244 let r1,r2 = dest_addop tm in
245 let x1',y1' = dest_divop r1
246 and x2',y2' = dest_divop r2 in
247 let x1n = dest_realintconst x1' and y1n = dest_realintconst y1'
248 and x2n = dest_realintconst x2' and y2n = dest_realintconst y2' in
249 let x3n = x1n */ y2n +/ x2n */ y1n
250 and y3n = y1n */ y2n in
251 let d = gcd_num x3n y3n in
252 let x3n' = quo_num x3n d and y3n' = quo_num y3n d in
253 let x3n'',y3n'' = if y3n' >/ Int 0 then x3n',y3n'
254 else minus_num x3n',minus_num y3n' in
255 let x3' = mk_realintconst x3n'' and y3' = mk_realintconst y3n'' in
256 let th0 = INST [x1',x1; y1',y1; x2',x2; y2',y2; x3',x3; y3',y3] pth in
257 let th1 = funpow 3 (MP_CONV REAL_INT_LT_CONV) th0 in
258 let tm2,tm3 = dest_eq(fst(dest_imp(concl th1))) in
259 let th2 = (LAND_CONV (BINOP_CONV REAL_INT_MUL_CONV THENC
260 REAL_INT_ADD_CONV) THENC
261 REAL_INT_MUL_CONV) tm2
262 and th3 = (RAND_CONV REAL_INT_MUL_CONV THENC REAL_INT_MUL_CONV) tm3 in
263 MP th1 (TRANS th2 (SYM th3)) in
264 BINOP_CONV REAL_INT_RAT_CONV THENC
265 RAW_REAL_RAT_ADD_CONV THENC TRY_CONV(GEN_REWRITE_CONV I [REAL_DIV_1]);;
267 (* ------------------------------------------------------------------------- *)
269 (* ------------------------------------------------------------------------- *)
271 let REAL_RAT_SUB_CONV =
274 REWRITE_TAC[real_sub]) in
275 GEN_REWRITE_CONV I [pth] THENC
276 RAND_CONV REAL_RAT_NEG_CONV THENC REAL_RAT_ADD_CONV;;
278 (* ------------------------------------------------------------------------- *)
279 (* Multiplication. *)
280 (* ------------------------------------------------------------------------- *)
282 let REAL_RAT_MUL_CONV =
283 let pth_nocancel = prove
284 (`(x1 / y1) * (x2 / y2) = (x1 * x2) / (y1 * y2)`,
285 REWRITE_TAC[real_div; REAL_INV_MUL; REAL_MUL_AC])
286 and pth_cancel = prove
287 (`~(d1 = &0) /\ ~(d2 = &0) /\
288 (d1 * u1 = x1) /\ (d2 * u2 = x2) /\
289 (d2 * v1 = y1) /\ (d1 * v2 = y2)
290 ==> ((x1 / y1) * (x2 / y2) = (u1 * u2) / (v1 * v2))`,
291 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
292 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
293 DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN (SUBST1_TAC o SYM)) THEN
294 ASM_REWRITE_TAC[real_div; REAL_INV_MUL] THEN
295 ONCE_REWRITE_TAC[AC REAL_MUL_AC
296 `((d1 * u1) * (id2 * iv1)) * ((d2 * u2) * id1 * iv2) =
297 (u1 * u2) * (iv1 * iv2) * (id2 * d2) * (id1 * d1)`] THEN
298 ASM_SIMP_TAC[REAL_MUL_LINV; REAL_MUL_RID])
299 and dest_divop = dest_binop `(/)`
300 and dest_mulop = dest_binop `(*)`
301 and x1 = `x1:real` and x2 = `x2:real`
302 and y1 = `y1:real` and y2 = `y2:real`
303 and u1 = `u1:real` and u2 = `u2:real`
304 and v1 = `v1:real` and v2 = `v2:real`
305 and d1 = `d1:real` and d2 = `d2:real` in
306 let RAW_REAL_RAT_MUL_CONV tm =
307 let r1,r2 = dest_mulop tm in
308 let x1',y1' = dest_divop r1
309 and x2',y2' = dest_divop r2 in
310 let x1n = dest_realintconst x1' and y1n = dest_realintconst y1'
311 and x2n = dest_realintconst x2' and y2n = dest_realintconst y2' in
312 let d1n = gcd_num x1n y2n
313 and d2n = gcd_num x2n y1n in
314 if d1n = num_1 & d2n = num_1 then
315 let th0 = INST [x1',x1; y1',y1; x2',x2; y2',y2] pth_nocancel in
316 let th1 = BINOP_CONV REAL_INT_MUL_CONV (rand(concl th0)) in
319 let u1n = quo_num x1n d1n
320 and u2n = quo_num x2n d2n
321 and v1n = quo_num y1n d2n
322 and v2n = quo_num y2n d1n in
323 let u1' = mk_realintconst u1n
324 and u2' = mk_realintconst u2n
325 and v1' = mk_realintconst v1n
326 and v2' = mk_realintconst v2n
327 and d1' = mk_realintconst d1n
328 and d2' = mk_realintconst d2n in
329 let th0 = INST [x1',x1; y1',y1; x2',x2; y2',y2;
330 u1',u1; v1',v1; u2',u2; v2',v2; d1',d1; d2',d2]
332 let th1 = EQT_ELIM(REAL_INT_REDUCE_CONV(lhand(concl th0))) in
333 let th2 = MP th0 th1 in
334 let th3 = BINOP_CONV REAL_INT_MUL_CONV (rand(concl th2)) in
336 BINOP_CONV REAL_INT_RAT_CONV THENC
337 RAW_REAL_RAT_MUL_CONV THENC TRY_CONV(GEN_REWRITE_CONV I [REAL_DIV_1]);;
339 (* ------------------------------------------------------------------------- *)
341 (* ------------------------------------------------------------------------- *)
343 let REAL_RAT_DIV_CONV =
345 (`x / y = x * inv(y)`,
346 REWRITE_TAC[real_div]) in
347 GEN_REWRITE_CONV I [pth] THENC
348 RAND_CONV REAL_RAT_INV_CONV THENC REAL_RAT_MUL_CONV;;
350 (* ------------------------------------------------------------------------- *)
352 (* ------------------------------------------------------------------------- *)
354 let REAL_RAT_POW_CONV =
356 (`(x / y) pow n = (x pow n) / (y pow n)`,
357 REWRITE_TAC[REAL_POW_DIV]) in
358 REAL_INT_POW_CONV ORELSEC
359 (LAND_CONV REAL_INT_RAT_CONV THENC
360 GEN_REWRITE_CONV I [pth] THENC
361 BINOP_CONV REAL_INT_POW_CONV);;
363 (* ------------------------------------------------------------------------- *)
365 (* ------------------------------------------------------------------------- *)
367 let REAL_RAT_MAX_CONV =
368 REWR_CONV real_max THENC
369 RATOR_CONV(RATOR_CONV(RAND_CONV REAL_RAT_LE_CONV)) THENC
370 GEN_REWRITE_CONV I [COND_CLAUSES];;
372 let REAL_RAT_MIN_CONV =
373 REWR_CONV real_min THENC
374 RATOR_CONV(RATOR_CONV(RAND_CONV REAL_RAT_LE_CONV)) THENC
375 GEN_REWRITE_CONV I [COND_CLAUSES];;
377 (* ------------------------------------------------------------------------- *)
379 (* ------------------------------------------------------------------------- *)
381 let REAL_RAT_RED_CONV =
382 let gconv_net = itlist (uncurry net_of_conv)
383 [`x <= y`,REAL_RAT_LE_CONV;
384 `x < y`,REAL_RAT_LT_CONV;
385 `x >= y`,REAL_RAT_GE_CONV;
386 `x > y`,REAL_RAT_GT_CONV;
387 `x:real = y`,REAL_RAT_EQ_CONV;
388 `--x`,CHANGED_CONV REAL_RAT_NEG_CONV;
389 `abs(x)`,REAL_RAT_ABS_CONV;
390 `inv(x)`,REAL_RAT_INV_CONV;
391 `x + y`,REAL_RAT_ADD_CONV;
392 `x - y`,REAL_RAT_SUB_CONV;
393 `x * y`,REAL_RAT_MUL_CONV;
394 `x / y`,CHANGED_CONV REAL_RAT_DIV_CONV;
395 `x pow n`,REAL_RAT_POW_CONV;
396 `max x y`,REAL_RAT_MAX_CONV;
397 `min x y`,REAL_RAT_MIN_CONV]
399 REWRITES_CONV gconv_net;;
401 let REAL_RAT_REDUCE_CONV = DEPTH_CONV REAL_RAT_RED_CONV;;
403 (* ------------------------------------------------------------------------- *)
404 (* Real normalizer dealing with rational constants. *)
405 (* ------------------------------------------------------------------------- *)
407 let REAL_POLY_NEG_CONV,REAL_POLY_ADD_CONV,REAL_POLY_SUB_CONV,
408 REAL_POLY_MUL_CONV,REAL_POLY_POW_CONV,REAL_POLY_CONV =
409 SEMIRING_NORMALIZERS_CONV REAL_POLY_CLAUSES REAL_POLY_NEG_CLAUSES
411 REAL_RAT_ADD_CONV,REAL_RAT_MUL_CONV,REAL_RAT_POW_CONV)
414 (* ------------------------------------------------------------------------- *)
415 (* Extend normalizer to handle "inv" and division by rational constants, and *)
416 (* normalize inside nested "max", "min" and "abs" terms. *)
417 (* ------------------------------------------------------------------------- *)
420 let neg_tm = `(--):real->real`
421 and inv_tm = `inv:real->real`
422 and add_tm = `(+):real->real->real`
423 and sub_tm = `(-):real->real->real`
424 and mul_tm = `(*):real->real->real`
425 and div_tm = `(/):real->real->real`
426 and pow_tm = `(pow):real->num->real`
427 and abs_tm = `abs:real->real`
428 and max_tm = `max:real->real->real`
429 and min_tm = `min:real->real->real`
430 and div_conv = REWR_CONV real_div in
431 let rec REAL_POLY_CONV tm =
432 if not(is_comb tm) or is_ratconst tm then REFL tm else
433 let lop,r = dest_comb tm in
435 let th1 = AP_TERM lop (REAL_POLY_CONV r) in
436 TRANS th1 (REAL_POLY_NEG_CONV (rand(concl th1)))
437 else if lop = inv_tm then
438 let th1 = AP_TERM lop (REAL_POLY_CONV r) in
439 TRANS th1 (TRY_CONV REAL_RAT_INV_CONV (rand(concl th1)))
440 else if lop = abs_tm then
441 AP_TERM lop (REAL_POLY_CONV r)
442 else if not(is_comb lop) then REFL tm else
443 let op,l = dest_comb lop in
445 let th1 = AP_THM (AP_TERM op (REAL_POLY_CONV l)) r in
446 TRANS th1 (TRY_CONV REAL_POLY_POW_CONV (rand(concl th1)))
447 else if op = add_tm or op = mul_tm or op = sub_tm then
448 let th1 = MK_COMB(AP_TERM op (REAL_POLY_CONV l),
450 let fn = if op = add_tm then REAL_POLY_ADD_CONV
451 else if op = mul_tm then REAL_POLY_MUL_CONV
452 else REAL_POLY_SUB_CONV in
453 TRANS th1 (fn (rand(concl th1)))
454 else if op = div_tm then
455 let th1 = div_conv tm in
456 TRANS th1 (REAL_POLY_CONV (rand(concl th1)))
457 else if op = min_tm or op = max_tm then
458 MK_COMB(AP_TERM op (REAL_POLY_CONV l),REAL_POLY_CONV r)
462 (* ------------------------------------------------------------------------- *)
463 (* Basic ring and ideal conversions. *)
464 (* ------------------------------------------------------------------------- *)
466 let REAL_RING,real_ideal_cofactors =
467 let REAL_INTEGRAL = prove
468 (`(!x. &0 * x = &0) /\
469 (!x y z. (x + y = x + z) <=> (y = z)) /\
470 (!w x y z. (w * y + x * z = w * z + x * y) <=> (w = x) \/ (y = z))`,
471 REWRITE_TAC[MULT_CLAUSES; EQ_ADD_LCANCEL] THEN
472 REWRITE_TAC[GSYM REAL_OF_NUM_EQ;
473 GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_MUL] THEN
474 ONCE_REWRITE_TAC[GSYM REAL_SUB_0] THEN
475 REWRITE_TAC[GSYM REAL_ENTIRE] THEN REAL_ARITH_TAC)
476 and REAL_RABINOWITSCH = prove
477 (`!x y:real. ~(x = y) <=> ?z. (x - y) * z = &1`,
479 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM REAL_SUB_0] THEN
480 MESON_TAC[REAL_MUL_RINV; REAL_MUL_LZERO; REAL_ARITH `~(&1 = &0)`])
481 and init = GEN_REWRITE_CONV ONCE_DEPTH_CONV [DECIMAL]
482 and real_ty = `:real` in
485 (rat_of_term,term_of_rat,REAL_RAT_EQ_CONV,
486 `(--):real->real`,`(+):real->real->real`,`(-):real->real->real`,
487 `(inv):real->real`,`(*):real->real->real`,`(/):real->real->real`,
488 `(pow):real->num->real`,
489 REAL_INTEGRAL,REAL_RABINOWITSCH,REAL_POLY_CONV) in
490 (fun tm -> let th = init tm in EQ_MP (SYM th) (pure(rand(concl th)))),
491 (fun tms tm -> if forall (fun t -> type_of t = real_ty) (tm::tms)
494 "real_ideal_cofactors: not all terms have type :real");;
496 (* ------------------------------------------------------------------------- *)
497 (* Conversion for ideal membership. *)
498 (* ------------------------------------------------------------------------- *)
500 let REAL_IDEAL_CONV =
501 let mk_add = mk_binop `( + ):real->real->real`
502 and mk_mul = mk_binop `( * ):real->real->real` in
504 let cfs = real_ideal_cofactors tms tm in
505 let tm' = end_itlist mk_add (map2 mk_mul cfs tms) in
506 let th = REAL_POLY_CONV tm and th' = REAL_POLY_CONV tm' in
509 (* ------------------------------------------------------------------------- *)
510 (* Further specialize GEN_REAL_ARITH and REAL_ARITH (final versions). *)
511 (* ------------------------------------------------------------------------- *)
513 let GEN_REAL_ARITH PROVER =
516 REAL_RAT_EQ_CONV,REAL_RAT_GE_CONV,REAL_RAT_GT_CONV,
517 REAL_POLY_CONV,REAL_POLY_NEG_CONV,REAL_POLY_ADD_CONV,REAL_POLY_MUL_CONV,
521 let init = GEN_REWRITE_CONV ONCE_DEPTH_CONV [DECIMAL]
522 and pure = GEN_REAL_ARITH REAL_LINEAR_PROVER in
523 fun tm -> let th = init tm in EQ_MP (SYM th) (pure(rand(concl th)));;
525 let REAL_ARITH_TAC = CONV_TAC REAL_ARITH;;
527 let ASM_REAL_ARITH_TAC =
528 REPEAT(FIRST_X_ASSUM(MP_TAC o check (not o is_forall o concl))) THEN
531 (* ------------------------------------------------------------------------- *)
532 (* A simple "field" rule. *)
533 (* ------------------------------------------------------------------------- *)
537 TOP_DEPTH_CONV BETA_CONV THENC
538 PURE_REWRITE_CONV[FORALL_SIMP; EXISTS_SIMP; real_div;
539 REAL_INV_INV; REAL_INV_MUL; GSYM REAL_POW_INV] THENC
540 NNFC_CONV THENC DEPTH_BINOP_CONV `(/\)` CONDS_CELIM_CONV THENC
542 ONCE_REWRITE_CONV[REAL_ARITH `x < y <=> x < y /\ ~(x = y)`]
543 and setup_conv = NNF_CONV THENC WEAK_CNF_CONV THENC CONJ_CANON_CONV
544 and core_rule t = try REAL_RING t with Failure _ -> REAL_ARITH t
546 let inv_tm = `inv:real->real`
547 and is_div = is_binop `(/):real->real->real` in
548 fun tm -> (is_div tm or (is_comb tm & rator tm = inv_tm)) &
549 not(is_ratconst(rand tm)) in
550 let BASIC_REAL_FIELD tm =
551 let is_freeinv t = is_inv t & free_in t tm in
552 let itms = setify(map rand (find_terms is_freeinv tm)) in
553 let hyps = map (fun t -> SPEC t REAL_MUL_RINV) itms in
554 let tm' = itlist (fun th t -> mk_imp(concl th,t)) hyps tm in
555 let th1 = setup_conv tm' in
556 let cjs = conjuncts(rand(concl th1)) in
557 let ths = map core_rule cjs in
558 let th2 = EQ_MP (SYM th1) (end_itlist CONJ ths) in
559 rev_itlist (C MP) hyps th2 in
561 let th0 = prenex_conv tm in
562 let tm0 = rand(concl th0) in
563 let avs,bod = strip_forall tm0 in
564 let th1 = setup_conv bod in
565 let ths = map BASIC_REAL_FIELD (conjuncts(rand(concl th1))) in
566 EQ_MP (SYM th0) (GENL avs (EQ_MP (SYM th1) (end_itlist CONJ ths)));;