1 (* Title: HOL/Real/RealBin.ML
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4 Copyright 1999 University of Cambridge
6 Binary arithmetic for the reals (integer literals only).
9 (** real (coercion from int to real) **)
11 Goal "real (number_of w :: int) = number_of w";
12 by (simp_tac (simpset() addsimps [real_number_of_def]) 1);
14 Addsimps [real_number_of];
16 Goalw [real_number_of_def] "Numeral0 = (0::real)";
17 by (simp_tac (simpset() addsimps [real_of_int_zero RS sym]) 1);
18 qed "real_numeral_0_eq_0";
20 Goalw [real_number_of_def] "Numeral1 = (1::real)";
21 by (stac (real_of_one RS sym) 1);
23 qed "real_numeral_1_eq_1";
27 Goal "(number_of v :: real) + number_of v' = number_of (bin_add v v')";
29 (HOL_ss addsimps [real_number_of_def,
30 real_of_int_add, number_of_add]) 1);
31 qed "add_real_number_of";
33 Addsimps [add_real_number_of];
38 Goalw [real_number_of_def] "- (number_of w :: real) = number_of (bin_minus w)";
40 (HOL_ss addsimps [number_of_minus, real_of_int_minus]) 1);
41 qed "minus_real_number_of";
43 Goalw [real_number_of_def]
44 "(number_of v :: real) - number_of w = number_of (bin_add v (bin_minus w))";
46 (HOL_ss addsimps [diff_number_of_eq, real_of_int_diff]) 1);
47 qed "diff_real_number_of";
49 Addsimps [minus_real_number_of, diff_real_number_of];
52 (** Multiplication **)
54 Goal "(number_of v :: real) * number_of v' = number_of (bin_mult v v')";
56 (HOL_ss addsimps [real_number_of_def, real_of_int_mult,
58 qed "mult_real_number_of";
60 Addsimps [mult_real_number_of];
62 Goal "(2::real) = 1 + 1";
63 by (simp_tac (simpset() addsimps [real_numeral_1_eq_1 RS sym]) 1);
66 (*For specialist use: NOT as default simprules*)
67 Goal "2 * z = (z+z::real)";
68 by (simp_tac (simpset () addsimps [lemma, real_add_mult_distrib]) 1);
71 Goal "z * 2 = (z+z::real)";
72 by (stac real_mult_commute 1 THEN rtac real_mult_2 1);
73 qed "real_mult_2_right";
80 Goal "((number_of v :: real) = number_of v') = \
81 \ iszero (number_of (bin_add v (bin_minus v')))";
83 (HOL_ss addsimps [real_number_of_def,
84 real_of_int_inject, eq_number_of_eq]) 1);
85 qed "eq_real_number_of";
87 Addsimps [eq_real_number_of];
91 (*"neg" is used in rewrite rules for binary comparisons*)
92 Goal "((number_of v :: real) < number_of v') = \
93 \ neg (number_of (bin_add v (bin_minus v')))";
95 (HOL_ss addsimps [real_number_of_def, real_of_int_less_iff,
96 less_number_of_eq_neg]) 1);
97 qed "less_real_number_of";
99 Addsimps [less_real_number_of];
102 (** Less-than-or-equals (<=) **)
104 Goal "(number_of x <= (number_of y::real)) = \
105 \ (~ number_of y < (number_of x::real))";
106 by (rtac (linorder_not_less RS sym) 1);
107 qed "le_real_number_of_eq_not_less";
109 Addsimps [le_real_number_of_eq_not_less];
111 (*** New versions of existing theorems involving 0, 1 ***)
113 Goal "- 1 = (-1::real)";
114 by (simp_tac (simpset() addsimps [real_numeral_1_eq_1 RS sym]) 1);
115 qed "real_minus_1_eq_m1";
117 Goal "-1 * z = -(z::real)";
118 by (simp_tac (simpset() addsimps [real_minus_1_eq_m1 RS sym,
119 real_mult_minus_1]) 1);
120 qed "real_mult_minus1";
122 Goal "z * -1 = -(z::real)";
123 by (stac real_mult_commute 1 THEN rtac real_mult_minus1 1);
124 qed "real_mult_minus1_right";
126 Addsimps [real_mult_minus1, real_mult_minus1_right];
129 (*Maps 0 to Numeral0 and 1 to Numeral1 and -(Numeral1) to -1*)
130 val real_numeral_ss =
131 HOL_ss addsimps [real_numeral_0_eq_0 RS sym, real_numeral_1_eq_1 RS sym,
134 fun rename_numerals th =
135 asm_full_simplify real_numeral_ss (Thm.transfer (the_context ()) th);
138 (** real from type "nat" **)
140 Goal "(0 < real (n::nat)) = (0<n)";
141 by (simp_tac (HOL_ss addsimps [real_of_nat_less_iff,
142 real_of_nat_zero RS sym]) 1);
143 qed "zero_less_real_of_nat_iff";
144 AddIffs [zero_less_real_of_nat_iff];
146 Goal "(0 <= real (n::nat)) = (0<=n)";
147 by (simp_tac (HOL_ss addsimps [real_of_nat_le_iff,
148 real_of_nat_zero RS sym]) 1);
149 qed "zero_le_real_of_nat_iff";
150 AddIffs [zero_le_real_of_nat_iff];
153 (*Like the ones above, for "equals"*)
154 AddIffs [real_of_nat_zero_iff];
156 (** Simplification of arithmetic when nested to the right **)
158 Goal "number_of v + (number_of w + z) = (number_of(bin_add v w) + z::real)";
160 qed "real_add_number_of_left";
162 Goal "number_of v * (number_of w * z) = (number_of(bin_mult v w) * z::real)";
163 by (simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1);
164 qed "real_mult_number_of_left";
166 Goalw [real_diff_def]
167 "number_of v + (number_of w - c) = number_of(bin_add v w) - (c::real)";
168 by (rtac real_add_number_of_left 1);
169 qed "real_add_number_of_diff1";
171 Goal "number_of v + (c - number_of w) = \
172 \ number_of (bin_add v (bin_minus w)) + (c::real)";
173 by (stac (diff_real_number_of RS sym) 1);
175 qed "real_add_number_of_diff2";
177 Addsimps [real_add_number_of_left, real_mult_number_of_left,
178 real_add_number_of_diff1, real_add_number_of_diff2];
181 (*"neg" is used in rewrite rules for binary comparisons*)
182 Goal "real (number_of v :: nat) = \
183 \ (if neg (number_of v) then 0 \
184 \ else (number_of v :: real))";
186 (HOL_ss addsimps [nat_number_of_def, real_of_nat_real_of_int,
187 real_of_nat_neg_int, real_number_of,
188 real_numeral_0_eq_0 RS sym]) 1);
189 qed "real_of_nat_number_of";
190 Addsimps [real_of_nat_number_of];
193 (**** Simprocs for numeric literals ****)
195 (** Combining of literal coefficients in sums of products **)
197 Goal "(x < y) = (x-y < (0::real))";
198 by (simp_tac (simpset() addsimps [real_diff_less_eq]) 1);
199 qed "real_less_iff_diff_less_0";
201 Goal "(x = y) = (x-y = (0::real))";
202 by (simp_tac (simpset() addsimps [real_diff_eq_eq]) 1);
203 qed "real_eq_iff_diff_eq_0";
205 Goal "(x <= y) = (x-y <= (0::real))";
206 by (simp_tac (simpset() addsimps [real_diff_le_eq]) 1);
207 qed "real_le_iff_diff_le_0";
210 (** For combine_numerals **)
212 Goal "i*u + (j*u + k) = (i+j)*u + (k::real)";
213 by (asm_simp_tac (simpset() addsimps [real_add_mult_distrib]) 1);
214 qed "left_real_add_mult_distrib";
217 (** For cancel_numerals **)
219 val rel_iff_rel_0_rls = map (inst "y" "?u+?v")
220 [real_less_iff_diff_less_0, real_eq_iff_diff_eq_0,
221 real_le_iff_diff_le_0] @
223 [real_less_iff_diff_less_0, real_eq_iff_diff_eq_0,
224 real_le_iff_diff_le_0];
226 Goal "!!i::real. (i*u + m = j*u + n) = ((i-j)*u + m = n)";
227 by (asm_simp_tac (simpset() addsimps [real_diff_def, real_add_mult_distrib]@
228 real_add_ac@rel_iff_rel_0_rls) 1);
229 qed "real_eq_add_iff1";
231 Goal "!!i::real. (i*u + m = j*u + n) = (m = (j-i)*u + n)";
232 by (asm_simp_tac (simpset() addsimps [real_diff_def, real_add_mult_distrib]@
233 real_add_ac@rel_iff_rel_0_rls) 1);
234 qed "real_eq_add_iff2";
236 Goal "!!i::real. (i*u + m < j*u + n) = ((i-j)*u + m < n)";
237 by (asm_simp_tac (simpset() addsimps [real_diff_def, real_add_mult_distrib]@
238 real_add_ac@rel_iff_rel_0_rls) 1);
239 qed "real_less_add_iff1";
241 Goal "!!i::real. (i*u + m < j*u + n) = (m < (j-i)*u + n)";
242 by (asm_simp_tac (simpset() addsimps [real_diff_def, real_add_mult_distrib]@
243 real_add_ac@rel_iff_rel_0_rls) 1);
244 qed "real_less_add_iff2";
246 Goal "!!i::real. (i*u + m <= j*u + n) = ((i-j)*u + m <= n)";
247 by (asm_simp_tac (simpset() addsimps [real_diff_def, real_add_mult_distrib]@
248 real_add_ac@rel_iff_rel_0_rls) 1);
249 qed "real_le_add_iff1";
251 Goal "!!i::real. (i*u + m <= j*u + n) = (m <= (j-i)*u + n)";
252 by (asm_simp_tac (simpset() addsimps [real_diff_def, real_add_mult_distrib]
253 @real_add_ac@rel_iff_rel_0_rls) 1);
254 qed "real_le_add_iff2";
257 Addsimps [real_numeral_0_eq_0, real_numeral_1_eq_1];
260 structure Real_Numeral_Simprocs =
263 (*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic in simprocs
264 isn't complicated by the abstract 0 and 1.*)
265 val numeral_syms = [real_numeral_0_eq_0 RS sym, real_numeral_1_eq_1 RS sym];
269 fun mk_numeral n = HOLogic.number_of_const HOLogic.realT $ HOLogic.mk_bin n;
271 (*Decodes a binary real constant, or 0, 1*)
272 fun dest_numeral (Const("0", _)) = 0
273 | dest_numeral (Const("1", _)) = 1
274 | dest_numeral (Const("Numeral.number_of", _) $ w) =
275 (HOLogic.dest_binum w
276 handle TERM _ => raise TERM("Real_Numeral_Simprocs.dest_numeral:1", [w]))
277 | dest_numeral t = raise TERM("Real_Numeral_Simprocs.dest_numeral:2", [t]);
279 fun find_first_numeral past (t::terms) =
280 ((dest_numeral t, rev past @ terms)
281 handle TERM _ => find_first_numeral (t::past) terms)
282 | find_first_numeral past [] = raise TERM("find_first_numeral", []);
284 val zero = mk_numeral 0;
285 val mk_plus = HOLogic.mk_binop "op +";
287 val uminus_const = Const ("uminus", HOLogic.realT --> HOLogic.realT);
289 (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
291 | mk_sum [t,u] = mk_plus (t, u)
292 | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
294 (*this version ALWAYS includes a trailing zero*)
295 fun long_mk_sum [] = zero
296 | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
298 val dest_plus = HOLogic.dest_bin "op +" HOLogic.realT;
300 (*decompose additions AND subtractions as a sum*)
301 fun dest_summing (pos, Const ("op +", _) $ t $ u, ts) =
302 dest_summing (pos, t, dest_summing (pos, u, ts))
303 | dest_summing (pos, Const ("op -", _) $ t $ u, ts) =
304 dest_summing (pos, t, dest_summing (not pos, u, ts))
305 | dest_summing (pos, t, ts) =
306 if pos then t::ts else uminus_const$t :: ts;
308 fun dest_sum t = dest_summing (true, t, []);
310 val mk_diff = HOLogic.mk_binop "op -";
311 val dest_diff = HOLogic.dest_bin "op -" HOLogic.realT;
313 val one = mk_numeral 1;
314 val mk_times = HOLogic.mk_binop "op *";
318 | mk_prod (t :: ts) = if t = one then mk_prod ts
319 else mk_times (t, mk_prod ts);
321 val dest_times = HOLogic.dest_bin "op *" HOLogic.realT;
324 let val (t,u) = dest_times t
325 in dest_prod t @ dest_prod u end
326 handle TERM _ => [t];
328 (*DON'T do the obvious simplifications; that would create special cases*)
329 fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts);
331 (*Express t as a product of (possibly) a numeral with other sorted terms*)
332 fun dest_coeff sign (Const ("uminus", _) $ t) = dest_coeff (~sign) t
333 | dest_coeff sign t =
334 let val ts = sort Term.term_ord (dest_prod t)
335 val (n, ts') = find_first_numeral [] ts
336 handle TERM _ => (1, ts)
337 in (sign*n, mk_prod ts') end;
339 (*Find first coefficient-term THAT MATCHES u*)
340 fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
341 | find_first_coeff past u (t::terms) =
342 let val (n,u') = dest_coeff 1 t
343 in if u aconv u' then (n, rev past @ terms)
344 else find_first_coeff (t::past) u terms
346 handle TERM _ => find_first_coeff (t::past) u terms;
349 (*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1*)
350 val add_0s = map rename_numerals [real_add_zero_left, real_add_zero_right];
351 val mult_1s = map rename_numerals [real_mult_1, real_mult_1_right] @
352 [real_mult_minus1, real_mult_minus1_right];
354 (*To perform binary arithmetic*)
356 [real_numeral_0_eq_0 RS sym, real_numeral_1_eq_1 RS sym,
357 add_real_number_of, real_add_number_of_left, minus_real_number_of,
358 diff_real_number_of, mult_real_number_of, real_mult_number_of_left] @
359 bin_arith_simps @ bin_rel_simps;
361 (*To evaluate binary negations of coefficients*)
362 val real_minus_simps = NCons_simps @
363 [real_minus_1_eq_m1, minus_real_number_of,
364 bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
365 bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
367 (*To let us treat subtraction as addition*)
368 val diff_simps = [real_diff_def, real_minus_add_distrib, real_minus_minus];
370 (*push the unary minus down: - x * y = x * - y
371 val real_minus_mult_eq_1_to_2 =
372 [real_minus_mult_eq1 RS sym, real_minus_mult_eq2] MRS trans |> standard;
373 same as real_minus_mult_commute
376 (*to extract again any uncancelled minuses*)
377 val real_minus_from_mult_simps =
378 [real_minus_minus, real_mult_minus_eq1, real_mult_minus_eq2];
380 (*combine unary minus with numeric literals, however nested within a product*)
381 val real_mult_minus_simps =
382 [real_mult_assoc, real_minus_mult_eq1, real_minus_mult_commute];
384 (*Apply the given rewrite (if present) just once*)
385 fun trans_tac None = all_tac
386 | trans_tac (Some th) = ALLGOALS (rtac (th RS trans));
388 fun prove_conv name tacs sg (hyps: thm list) (t,u) =
389 if t aconv u then None
391 let val ct = cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)))
393 (prove_goalw_cterm [] ct (K tacs)
394 handle ERROR => error
395 ("The error(s) above occurred while trying to prove " ^
396 string_of_cterm ct ^ "\nInternal failure of simproc " ^ name))
399 (*version without the hyps argument*)
400 fun prove_conv_nohyps name tacs sg = prove_conv name tacs sg [];
402 (*Final simplification: cancel + and * *)
403 val simplify_meta_eq =
404 Int_Numeral_Simprocs.simplify_meta_eq
405 [real_add_zero_left, real_add_zero_right,
406 real_mult_0, real_mult_0_right, real_mult_1, real_mult_1_right];
408 fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
409 fun prep_pat s = HOLogic.read_cterm (Theory.sign_of (the_context ())) s;
410 val prep_pats = map prep_pat;
412 structure CancelNumeralsCommon =
415 val dest_sum = dest_sum
416 val mk_coeff = mk_coeff
417 val dest_coeff = dest_coeff 1
418 val find_first_coeff = find_first_coeff []
419 val trans_tac = trans_tac
421 ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
422 real_minus_simps@real_add_ac))
423 THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@real_mult_minus_simps))
425 (simp_tac (HOL_ss addsimps real_minus_from_mult_simps@
426 real_add_ac@real_mult_ac))
427 val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
428 val simplify_meta_eq = simplify_meta_eq
432 structure EqCancelNumerals = CancelNumeralsFun
433 (open CancelNumeralsCommon
434 val prove_conv = prove_conv "realeq_cancel_numerals"
435 val mk_bal = HOLogic.mk_eq
436 val dest_bal = HOLogic.dest_bin "op =" HOLogic.realT
437 val bal_add1 = real_eq_add_iff1 RS trans
438 val bal_add2 = real_eq_add_iff2 RS trans
441 structure LessCancelNumerals = CancelNumeralsFun
442 (open CancelNumeralsCommon
443 val prove_conv = prove_conv "realless_cancel_numerals"
444 val mk_bal = HOLogic.mk_binrel "op <"
445 val dest_bal = HOLogic.dest_bin "op <" HOLogic.realT
446 val bal_add1 = real_less_add_iff1 RS trans
447 val bal_add2 = real_less_add_iff2 RS trans
450 structure LeCancelNumerals = CancelNumeralsFun
451 (open CancelNumeralsCommon
452 val prove_conv = prove_conv "realle_cancel_numerals"
453 val mk_bal = HOLogic.mk_binrel "op <="
454 val dest_bal = HOLogic.dest_bin "op <=" HOLogic.realT
455 val bal_add1 = real_le_add_iff1 RS trans
456 val bal_add2 = real_le_add_iff2 RS trans
459 val cancel_numerals =
461 [("realeq_cancel_numerals",
462 prep_pats ["(l::real) + m = n", "(l::real) = m + n",
463 "(l::real) - m = n", "(l::real) = m - n",
464 "(l::real) * m = n", "(l::real) = m * n"],
465 EqCancelNumerals.proc),
466 ("realless_cancel_numerals",
467 prep_pats ["(l::real) + m < n", "(l::real) < m + n",
468 "(l::real) - m < n", "(l::real) < m - n",
469 "(l::real) * m < n", "(l::real) < m * n"],
470 LessCancelNumerals.proc),
471 ("realle_cancel_numerals",
472 prep_pats ["(l::real) + m <= n", "(l::real) <= m + n",
473 "(l::real) - m <= n", "(l::real) <= m - n",
474 "(l::real) * m <= n", "(l::real) <= m * n"],
475 LeCancelNumerals.proc)];
478 structure CombineNumeralsData =
480 val add = op + : int*int -> int
481 val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *)
482 val dest_sum = dest_sum
483 val mk_coeff = mk_coeff
484 val dest_coeff = dest_coeff 1
485 val left_distrib = left_real_add_mult_distrib RS trans
486 val prove_conv = prove_conv_nohyps "real_combine_numerals"
487 val trans_tac = trans_tac
489 ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
490 diff_simps@real_minus_simps@real_add_ac))
491 THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@real_mult_minus_simps))
492 THEN ALLGOALS (simp_tac (HOL_ss addsimps real_minus_from_mult_simps@
493 real_add_ac@real_mult_ac))
494 val numeral_simp_tac = ALLGOALS
495 (simp_tac (HOL_ss addsimps add_0s@bin_simps))
496 val simplify_meta_eq =
497 Int_Numeral_Simprocs.simplify_meta_eq (add_0s@mult_1s)
500 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
502 val combine_numerals =
503 prep_simproc ("real_combine_numerals",
504 prep_pats ["(i::real) + j", "(i::real) - j"],
505 CombineNumerals.proc);
508 (** Declarations for ExtractCommonTerm **)
510 (*this version ALWAYS includes a trailing one*)
511 fun long_mk_prod [] = one
512 | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts);
514 (*Find first term that matches u*)
515 fun find_first past u [] = raise TERM("find_first", [])
516 | find_first past u (t::terms) =
517 if u aconv t then (rev past @ terms)
518 else find_first (t::past) u terms
519 handle TERM _ => find_first (t::past) u terms;
521 (*Final simplification: cancel + and * *)
522 fun cancel_simplify_meta_eq cancel_th th =
523 Int_Numeral_Simprocs.simplify_meta_eq
524 [real_mult_1, real_mult_1_right]
525 (([th, cancel_th]) MRS trans);
527 (*** Making constant folding work for 0 and 1 too ***)
529 structure RealAbstractNumeralsData =
531 val dest_eq = HOLogic.dest_eq o HOLogic.dest_Trueprop o concl_of
532 val is_numeral = Bin_Simprocs.is_numeral
533 val numeral_0_eq_0 = real_numeral_0_eq_0
534 val numeral_1_eq_1 = real_numeral_1_eq_1
535 val prove_conv = prove_conv_nohyps "real_abstract_numerals"
536 fun norm_tac simps = ALLGOALS (simp_tac (HOL_ss addsimps simps))
537 val simplify_meta_eq = Bin_Simprocs.simplify_meta_eq
540 structure RealAbstractNumerals = AbstractNumeralsFun (RealAbstractNumeralsData)
542 (*For addition, we already have rules for the operand 0.
543 Multiplication is omitted because there are already special rules for
544 both 0 and 1 as operands. Unary minus is trivial, just have - 1 = -1.
545 For the others, having three patterns is a compromise between just having
546 one (many spurious calls) and having nine (just too many!) *)
549 [("real_add_eval_numerals",
550 prep_pats ["(m::real) + 1", "(m::real) + number_of v"],
551 RealAbstractNumerals.proc add_real_number_of),
552 ("real_diff_eval_numerals",
553 prep_pats ["(m::real) - 1", "(m::real) - number_of v"],
554 RealAbstractNumerals.proc diff_real_number_of),
555 ("real_eq_eval_numerals",
556 prep_pats ["(m::real) = 0", "(m::real) = 1", "(m::real) = number_of v"],
557 RealAbstractNumerals.proc eq_real_number_of),
558 ("real_less_eval_numerals",
559 prep_pats ["(m::real) < 0", "(m::real) < 1", "(m::real) < number_of v"],
560 RealAbstractNumerals.proc less_real_number_of),
561 ("real_le_eval_numerals",
562 prep_pats ["(m::real) <= 0", "(m::real) <= 1", "(m::real) <= number_of v"],
563 RealAbstractNumerals.proc le_real_number_of_eq_not_less)]
568 Addsimprocs Real_Numeral_Simprocs.eval_numerals;
569 Addsimprocs Real_Numeral_Simprocs.cancel_numerals;
570 Addsimprocs [Real_Numeral_Simprocs.combine_numerals];
572 (*The Abel_Cancel simprocs are now obsolete*)
573 Delsimprocs [Real_Cancel.sum_conv, Real_Cancel.rel_conv];
579 fun test s = (Goal s; by (Simp_tac 1));
581 test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::real)";
583 test "2*u = (u::real)";
584 test "(i + j + 12 + (k::real)) - 15 = y";
585 test "(i + j + 12 + (k::real)) - 5 = y";
587 test "y - b < (b::real)";
588 test "y - (3*b + c) < (b::real) - 2*c";
590 test "(2*x - (u*v) + y) - v*3*u = (w::real)";
591 test "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::real)";
592 test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::real)";
593 test "u*v - (x*u*v + (u*v)*4 + y) = (w::real)";
595 test "(i + j + 12 + (k::real)) = u + 15 + y";
596 test "(i + j*2 + 12 + (k::real)) = j + 5 + y";
598 test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::real)";
600 test "a + -(b+c) + b = (d::real)";
601 test "a + -(b+c) - b = (d::real)";
603 (*negative numerals*)
604 test "(i + j + -2 + (k::real)) - (u + 5 + y) = zz";
605 test "(i + j + -3 + (k::real)) < u + 5 + y";
606 test "(i + j + 3 + (k::real)) < u + -6 + y";
607 test "(i + j + -12 + (k::real)) - 15 = y";
608 test "(i + j + 12 + (k::real)) - -15 = y";
609 test "(i + j + -12 + (k::real)) - -15 = y";
613 (** Constant folding for real plus and times **)
616 structure Real_Plus_Assoc = Assoc_Fold (Real_Plus_Assoc_Data);
617 because combine_numerals does the same thing*)
619 structure Real_Times_Assoc_Data : ASSOC_FOLD_DATA =
622 val eq_reflection = eq_reflection
623 val sg_ref = Sign.self_ref (Theory.sign_of (the_context ()))
624 val T = HOLogic.realT
625 val plus = Const ("op *", [HOLogic.realT,HOLogic.realT] ---> HOLogic.realT)
626 val add_ac = real_mult_ac
629 structure Real_Times_Assoc = Assoc_Fold (Real_Times_Assoc_Data);
631 Addsimprocs [Real_Times_Assoc.conv];
633 (*Simplification of x-y < 0, etc.*)
634 AddIffs [real_less_iff_diff_less_0 RS sym];
635 AddIffs [real_eq_iff_diff_eq_0 RS sym];
636 AddIffs [real_le_iff_diff_le_0 RS sym];
638 (** <= monotonicity results: needed for arithmetic **)
640 Goal "[| i <= j; (0::real) <= k |] ==> i*k <= j*k";
641 by (auto_tac (claset(),
642 simpset() addsimps [order_le_less, real_mult_less_mono1]));
643 qed "real_mult_le_mono1";
645 Goal "[| i <= j; (0::real) <= k |] ==> k*i <= k*j";
646 by (dtac real_mult_le_mono1 1);
647 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [real_mult_commute])));
648 qed "real_mult_le_mono2";
650 Goal "[| (i::real) <= j; k <= l; 0 <= j; 0 <= k |] ==> i*k <= j*l";
651 by (etac (real_mult_le_mono1 RS order_trans) 1);
653 by (etac real_mult_le_mono2 1);
655 qed "real_mult_le_mono";
657 Addsimps [real_minus_1_eq_m1];