1 (* Title: HOL/Real/rat_arith0.ML
3 Author: Lawrence C Paulson
4 Copyright 2004 University of Cambridge
6 Simprocs for common factor cancellation & Rational coefficient handling
8 Instantiation of the generic linear arithmetic package for type rat.
12 val rat_mult_strict_left_mono =
13 read_instantiate_sg(sign_of (the_context())) [("a","?a::rat")] mult_strict_left_mono;
15 val rat_mult_left_mono =
16 read_instantiate_sg(sign_of (the_context())) [("a","?a::rat")] mult_left_mono;
19 val rat_number_of_def = thm "rat_number_of_def";
20 val diff_rat_def = thm "diff_rat_def";
22 val rat_numeral_0_eq_0 = thm "rat_numeral_0_eq_0";
23 val rat_numeral_1_eq_1 = thm "rat_numeral_1_eq_1";
24 val add_rat_number_of = thm "add_rat_number_of";
25 val minus_rat_number_of = thm "minus_rat_number_of";
26 val diff_rat_number_of = thm "diff_rat_number_of";
27 val mult_rat_number_of = thm "mult_rat_number_of";
28 val rat_mult_2 = thm "rat_mult_2";
29 val rat_mult_2_right = thm "rat_mult_2_right";
30 val eq_rat_number_of = thm "eq_rat_number_of";
31 val less_rat_number_of = thm "less_rat_number_of";
32 val rat_minus_1_eq_m1 = thm "rat_minus_1_eq_m1";
33 val rat_mult_minus1 = thm "rat_mult_minus1";
34 val rat_mult_minus1_right = thm "rat_mult_minus1_right";
35 val rat_add_number_of_left = thm "rat_add_number_of_left";
36 val rat_mult_number_of_left = thm "rat_mult_number_of_left";
37 val rat_add_number_of_diff1 = thm "rat_add_number_of_diff1";
38 val rat_add_number_of_diff2 = thm "rat_add_number_of_diff2";
40 val rat_add_0_left = thm "rat_add_0_left";
41 val rat_add_0_right = thm "rat_add_0_right";
42 val rat_mult_1_left = thm "rat_mult_1_left";
43 val rat_mult_1_right = thm "rat_mult_1_right";
45 (*Maps 0 to Numeral0 and 1 to Numeral1 and -(Numeral1) to -1*)
47 HOL_ss addsimps [rat_numeral_0_eq_0 RS sym, rat_numeral_1_eq_1 RS sym,
50 fun rename_numerals th =
51 asm_full_simplify rat_numeral_ss (Thm.transfer (the_context ()) th);
54 structure Rat_Numeral_Simprocs =
57 (*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic in simprocs
58 isn't complicated by the abstract 0 and 1.*)
59 val numeral_syms = [rat_numeral_0_eq_0 RS sym, rat_numeral_1_eq_1 RS sym];
63 val ratT = Type("Rational.rat", []);
65 fun mk_numeral n = HOLogic.number_of_const ratT $ HOLogic.mk_bin n;
67 (*Decodes a binary rat constant, or 0, 1*)
68 val dest_numeral = Int_Numeral_Simprocs.dest_numeral;
69 val find_first_numeral = Int_Numeral_Simprocs.find_first_numeral;
71 val zero = mk_numeral 0;
72 val mk_plus = HOLogic.mk_binop "op +";
74 val uminus_const = Const ("uminus", ratT --> ratT);
76 (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
78 | mk_sum [t,u] = mk_plus (t, u)
79 | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
81 (*this version ALWAYS includes a trailing zero*)
82 fun long_mk_sum [] = zero
83 | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
85 val dest_plus = HOLogic.dest_bin "op +" ratT;
87 (*decompose additions AND subtractions as a sum*)
88 fun dest_summing (pos, Const ("op +", _) $ t $ u, ts) =
89 dest_summing (pos, t, dest_summing (pos, u, ts))
90 | dest_summing (pos, Const ("op -", _) $ t $ u, ts) =
91 dest_summing (pos, t, dest_summing (not pos, u, ts))
92 | dest_summing (pos, t, ts) =
93 if pos then t::ts else uminus_const$t :: ts;
95 fun dest_sum t = dest_summing (true, t, []);
97 val mk_diff = HOLogic.mk_binop "op -";
98 val dest_diff = HOLogic.dest_bin "op -" ratT;
100 val one = mk_numeral 1;
101 val mk_times = HOLogic.mk_binop "op *";
105 | mk_prod (t :: ts) = if t = one then mk_prod ts
106 else mk_times (t, mk_prod ts);
108 val dest_times = HOLogic.dest_bin "op *" ratT;
111 let val (t,u) = dest_times t
112 in dest_prod t @ dest_prod u end
113 handle TERM _ => [t];
115 (*DON'T do the obvious simplifications; that would create special cases*)
116 fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts);
118 (*Express t as a product of (possibly) a numeral with other sorted terms*)
119 fun dest_coeff sign (Const ("uminus", _) $ t) = dest_coeff (~sign) t
120 | dest_coeff sign t =
121 let val ts = sort Term.term_ord (dest_prod t)
122 val (n, ts') = find_first_numeral [] ts
123 handle TERM _ => (1, ts)
124 in (sign*n, mk_prod ts') end;
126 (*Find first coefficient-term THAT MATCHES u*)
127 fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
128 | find_first_coeff past u (t::terms) =
129 let val (n,u') = dest_coeff 1 t
130 in if u aconv u' then (n, rev past @ terms)
131 else find_first_coeff (t::past) u terms
133 handle TERM _ => find_first_coeff (t::past) u terms;
136 (*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1*)
137 val add_0s = map rename_numerals [rat_add_0_left, rat_add_0_right];
138 val mult_1s = map rename_numerals [rat_mult_1_left, rat_mult_1_right] @
139 [rat_mult_minus1, rat_mult_minus1_right];
141 (*To perform binary arithmetic*)
143 [rat_numeral_0_eq_0 RS sym, rat_numeral_1_eq_1 RS sym,
144 add_rat_number_of, rat_add_number_of_left, minus_rat_number_of,
145 diff_rat_number_of, mult_rat_number_of, rat_mult_number_of_left] @
146 bin_arith_simps @ bin_rel_simps;
148 (*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms
149 during re-arrangement*)
150 val non_add_bin_simps =
151 bin_simps \\ [rat_add_number_of_left, add_rat_number_of];
153 (*To evaluate binary negations of coefficients*)
154 val rat_minus_simps = NCons_simps @
155 [rat_minus_1_eq_m1, minus_rat_number_of,
156 bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
157 bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
159 (*To let us treat subtraction as addition*)
160 val diff_simps = [diff_rat_def, minus_add_distrib, minus_minus];
162 (*to extract again any uncancelled minuses*)
163 val rat_minus_from_mult_simps =
164 [minus_minus, minus_mult_left RS sym, minus_mult_right RS sym];
166 (*combine unary minus with numeric literals, however nested within a product*)
167 val rat_mult_minus_simps =
168 [mult_assoc, minus_mult_left, minus_mult_commute];
170 (*Apply the given rewrite (if present) just once*)
171 fun trans_tac None = all_tac
172 | trans_tac (Some th) = ALLGOALS (rtac (th RS trans));
174 (*Final simplification: cancel + and * *)
175 val simplify_meta_eq =
176 Int_Numeral_Simprocs.simplify_meta_eq
178 mult_zero_left, mult_zero_right, mult_1, mult_1_right];
180 fun prep_simproc (name, pats, proc) =
181 Simplifier.simproc (Theory.sign_of (the_context ())) name pats proc;
183 structure CancelNumeralsCommon =
186 val dest_sum = dest_sum
187 val mk_coeff = mk_coeff
188 val dest_coeff = dest_coeff 1
189 val find_first_coeff = find_first_coeff []
190 val trans_tac = trans_tac
192 ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
193 rat_minus_simps@add_ac))
194 THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@rat_mult_minus_simps))
196 (simp_tac (HOL_ss addsimps rat_minus_from_mult_simps@
198 val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
199 val simplify_meta_eq = simplify_meta_eq
203 structure EqCancelNumerals = CancelNumeralsFun
204 (open CancelNumeralsCommon
205 val prove_conv = Bin_Simprocs.prove_conv
206 val mk_bal = HOLogic.mk_eq
207 val dest_bal = HOLogic.dest_bin "op =" ratT
208 val bal_add1 = eq_add_iff1 RS trans
209 val bal_add2 = eq_add_iff2 RS trans
212 structure LessCancelNumerals = CancelNumeralsFun
213 (open CancelNumeralsCommon
214 val prove_conv = Bin_Simprocs.prove_conv
215 val mk_bal = HOLogic.mk_binrel "op <"
216 val dest_bal = HOLogic.dest_bin "op <" ratT
217 val bal_add1 = less_add_iff1 RS trans
218 val bal_add2 = less_add_iff2 RS trans
221 structure LeCancelNumerals = CancelNumeralsFun
222 (open CancelNumeralsCommon
223 val prove_conv = Bin_Simprocs.prove_conv
224 val mk_bal = HOLogic.mk_binrel "op <="
225 val dest_bal = HOLogic.dest_bin "op <=" ratT
226 val bal_add1 = le_add_iff1 RS trans
227 val bal_add2 = le_add_iff2 RS trans
230 val cancel_numerals =
232 [("rateq_cancel_numerals",
233 ["(l::rat) + m = n", "(l::rat) = m + n",
234 "(l::rat) - m = n", "(l::rat) = m - n",
235 "(l::rat) * m = n", "(l::rat) = m * n"],
236 EqCancelNumerals.proc),
237 ("ratless_cancel_numerals",
238 ["(l::rat) + m < n", "(l::rat) < m + n",
239 "(l::rat) - m < n", "(l::rat) < m - n",
240 "(l::rat) * m < n", "(l::rat) < m * n"],
241 LessCancelNumerals.proc),
242 ("ratle_cancel_numerals",
243 ["(l::rat) + m <= n", "(l::rat) <= m + n",
244 "(l::rat) - m <= n", "(l::rat) <= m - n",
245 "(l::rat) * m <= n", "(l::rat) <= m * n"],
246 LeCancelNumerals.proc)];
249 structure CombineNumeralsData =
251 val add = op + : int*int -> int
252 val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *)
253 val dest_sum = dest_sum
254 val mk_coeff = mk_coeff
255 val dest_coeff = dest_coeff 1
256 val left_distrib = combine_common_factor RS trans
257 val prove_conv = Bin_Simprocs.prove_conv_nohyps
258 val trans_tac = trans_tac
260 ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
261 diff_simps@rat_minus_simps@add_ac))
262 THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@rat_mult_minus_simps))
263 THEN ALLGOALS (simp_tac (HOL_ss addsimps rat_minus_from_mult_simps@
265 val numeral_simp_tac = ALLGOALS
266 (simp_tac (HOL_ss addsimps add_0s@bin_simps))
267 val simplify_meta_eq =
268 Int_Numeral_Simprocs.simplify_meta_eq (add_0s@mult_1s)
271 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
273 val combine_numerals =
274 prep_simproc ("rat_combine_numerals", ["(i::rat) + j", "(i::rat) - j"], CombineNumerals.proc);
277 (** Declarations for ExtractCommonTerm **)
279 (*this version ALWAYS includes a trailing one*)
280 fun long_mk_prod [] = one
281 | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts);
283 (*Find first term that matches u*)
284 fun find_first past u [] = raise TERM("find_first", [])
285 | find_first past u (t::terms) =
286 if u aconv t then (rev past @ terms)
287 else find_first (t::past) u terms
288 handle TERM _ => find_first (t::past) u terms;
290 (*Final simplification: cancel + and * *)
291 fun cancel_simplify_meta_eq cancel_th th =
292 Int_Numeral_Simprocs.simplify_meta_eq
293 [rat_mult_1_left, rat_mult_1_right]
294 (([th, cancel_th]) MRS trans);
296 (*** Making constant folding work for 0 and 1 too ***)
298 structure RatAbstractNumeralsData =
300 val dest_eq = HOLogic.dest_eq o HOLogic.dest_Trueprop o concl_of
301 val is_numeral = Bin_Simprocs.is_numeral
302 val numeral_0_eq_0 = rat_numeral_0_eq_0
303 val numeral_1_eq_1 = rat_numeral_1_eq_1
304 val prove_conv = Bin_Simprocs.prove_conv_nohyps_novars
305 fun norm_tac simps = ALLGOALS (simp_tac (HOL_ss addsimps simps))
306 val simplify_meta_eq = Bin_Simprocs.simplify_meta_eq
309 structure RatAbstractNumerals = AbstractNumeralsFun (RatAbstractNumeralsData)
311 (*For addition, we already have rules for the operand 0.
312 Multiplication is omitted because there are already special rules for
313 both 0 and 1 as operands. Unary minus is trivial, just have - 1 = -1.
314 For the others, having three patterns is a compromise between just having
315 one (many spurious calls) and having nine (just too many!) *)
318 [("rat_add_eval_numerals",
319 ["(m::rat) + 1", "(m::rat) + number_of v"],
320 RatAbstractNumerals.proc add_rat_number_of),
321 ("rat_diff_eval_numerals",
322 ["(m::rat) - 1", "(m::rat) - number_of v"],
323 RatAbstractNumerals.proc diff_rat_number_of),
324 ("rat_eq_eval_numerals",
325 ["(m::rat) = 0", "(m::rat) = 1", "(m::rat) = number_of v"],
326 RatAbstractNumerals.proc eq_rat_number_of),
327 ("rat_less_eval_numerals",
328 ["(m::rat) < 0", "(m::rat) < 1", "(m::rat) < number_of v"],
329 RatAbstractNumerals.proc less_rat_number_of),
330 ("rat_le_eval_numerals",
331 ["(m::rat) <= 0", "(m::rat) <= 1", "(m::rat) <= number_of v"],
332 RatAbstractNumerals.proc le_number_of_eq_not_less)]
337 Addsimprocs Rat_Numeral_Simprocs.eval_numerals;
338 Addsimprocs Rat_Numeral_Simprocs.cancel_numerals;
339 Addsimprocs [Rat_Numeral_Simprocs.combine_numerals];
343 (** Constant folding for rat plus and times **)
346 structure Rat_Plus_Assoc = Assoc_Fold (Rat_Plus_Assoc_Data);
347 because combine_numerals does the same thing*)
349 structure Rat_Times_Assoc_Data : ASSOC_FOLD_DATA =
352 val eq_reflection = eq_reflection
353 val sg_ref = Sign.self_ref (Theory.sign_of (the_context ()))
354 val T = Rat_Numeral_Simprocs.ratT
355 val plus = Const ("op *", [Rat_Numeral_Simprocs.ratT,Rat_Numeral_Simprocs.ratT] ---> Rat_Numeral_Simprocs.ratT)
359 structure Rat_Times_Assoc = Assoc_Fold (Rat_Times_Assoc_Data);
361 Addsimprocs [Rat_Times_Assoc.conv];
364 (****Common factor cancellation****)
366 (*To quote from Provers/Arith/cancel_numeral_factor.ML:
368 This simproc Cancels common coefficients in balanced expressions:
370 u*#m ~~ u'*#m' == #n*u ~~ #n'*u'
372 where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /)
373 and d = gcd(m,m') and n=m/d and n'=m'/d.
377 open Rat_Numeral_Simprocs
380 val rel_rat_number_of = [eq_rat_number_of, less_rat_number_of,
381 le_number_of_eq_not_less]
383 structure CancelNumeralFactorCommon =
385 val mk_coeff = mk_coeff
386 val dest_coeff = dest_coeff 1
387 val trans_tac = trans_tac
389 ALLGOALS (simp_tac (HOL_ss addsimps rat_minus_from_mult_simps @ mult_1s))
390 THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@rat_mult_minus_simps))
391 THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac))
392 val numeral_simp_tac =
393 ALLGOALS (simp_tac (HOL_ss addsimps rel_rat_number_of@bin_simps))
394 val simplify_meta_eq = simplify_meta_eq
397 structure DivCancelNumeralFactor = CancelNumeralFactorFun
398 (open CancelNumeralFactorCommon
399 val prove_conv = Bin_Simprocs.prove_conv
400 val mk_bal = HOLogic.mk_binop "HOL.divide"
401 val dest_bal = HOLogic.dest_bin "HOL.divide" Rat_Numeral_Simprocs.ratT
402 val cancel = mult_divide_cancel_left RS trans
403 val neg_exchanges = false
406 structure EqCancelNumeralFactor = CancelNumeralFactorFun
407 (open CancelNumeralFactorCommon
408 val prove_conv = Bin_Simprocs.prove_conv
409 val mk_bal = HOLogic.mk_eq
410 val dest_bal = HOLogic.dest_bin "op =" Rat_Numeral_Simprocs.ratT
411 val cancel = mult_cancel_left RS trans
412 val neg_exchanges = false
415 structure LessCancelNumeralFactor = CancelNumeralFactorFun
416 (open CancelNumeralFactorCommon
417 val prove_conv = Bin_Simprocs.prove_conv
418 val mk_bal = HOLogic.mk_binrel "op <"
419 val dest_bal = HOLogic.dest_bin "op <" Rat_Numeral_Simprocs.ratT
420 val cancel = mult_less_cancel_left RS trans
421 val neg_exchanges = true
424 structure LeCancelNumeralFactor = CancelNumeralFactorFun
425 (open CancelNumeralFactorCommon
426 val prove_conv = Bin_Simprocs.prove_conv
427 val mk_bal = HOLogic.mk_binrel "op <="
428 val dest_bal = HOLogic.dest_bin "op <=" Rat_Numeral_Simprocs.ratT
429 val cancel = mult_le_cancel_left RS trans
430 val neg_exchanges = true
433 val rat_cancel_numeral_factors_relations =
435 [("rateq_cancel_numeral_factor",
436 ["(l::rat) * m = n", "(l::rat) = m * n"],
437 EqCancelNumeralFactor.proc),
438 ("ratless_cancel_numeral_factor",
439 ["(l::rat) * m < n", "(l::rat) < m * n"],
440 LessCancelNumeralFactor.proc),
441 ("ratle_cancel_numeral_factor",
442 ["(l::rat) * m <= n", "(l::rat) <= m * n"],
443 LeCancelNumeralFactor.proc)]
445 val rat_cancel_numeral_factors_divide = prep_simproc
446 ("ratdiv_cancel_numeral_factor",
447 ["((l::rat) * m) / n", "(l::rat) / (m * n)",
448 "((number_of v)::rat) / (number_of w)"],
449 DivCancelNumeralFactor.proc)
451 val rat_cancel_numeral_factors =
452 rat_cancel_numeral_factors_relations @
453 [rat_cancel_numeral_factors_divide]
457 Addsimprocs rat_cancel_numeral_factors;
464 fun test s = (Goal s; by (Simp_tac 1));
466 test "0 <= (y::rat) * -2";
467 test "9*x = 12 * (y::rat)";
468 test "(9*x) / (12 * (y::rat)) = z";
469 test "9*x < 12 * (y::rat)";
470 test "9*x <= 12 * (y::rat)";
472 test "-99*x = 132 * (y::rat)";
473 test "(-99*x) / (132 * (y::rat)) = z";
474 test "-99*x < 132 * (y::rat)";
475 test "-99*x <= 132 * (y::rat)";
477 test "999*x = -396 * (y::rat)";
478 test "(999*x) / (-396 * (y::rat)) = z";
479 test "999*x < -396 * (y::rat)";
480 test "999*x <= -396 * (y::rat)";
482 test "(- ((2::rat) * x) <= 2 * y)";
483 test "-99*x = -81 * (y::rat)";
484 test "(-99*x) / (-81 * (y::rat)) = z";
485 test "-99*x <= -81 * (y::rat)";
486 test "-99*x < -81 * (y::rat)";
488 test "-2 * x = -1 * (y::rat)";
489 test "-2 * x = -(y::rat)";
490 test "(-2 * x) / (-1 * (y::rat)) = z";
491 test "-2 * x < -(y::rat)";
492 test "-2 * x <= -1 * (y::rat)";
493 test "-x < -23 * (y::rat)";
494 test "-x <= -23 * (y::rat)";
498 (** Declarations for ExtractCommonTerm **)
501 open Rat_Numeral_Simprocs
504 structure CancelFactorCommon =
506 val mk_sum = long_mk_prod
507 val dest_sum = dest_prod
508 val mk_coeff = mk_coeff
509 val dest_coeff = dest_coeff
510 val find_first = find_first []
511 val trans_tac = trans_tac
512 val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@mult_ac))
515 structure EqCancelFactor = ExtractCommonTermFun
516 (open CancelFactorCommon
517 val prove_conv = Bin_Simprocs.prove_conv
518 val mk_bal = HOLogic.mk_eq
519 val dest_bal = HOLogic.dest_bin "op =" Rat_Numeral_Simprocs.ratT
520 val simplify_meta_eq = cancel_simplify_meta_eq mult_cancel_left
524 structure DivideCancelFactor = ExtractCommonTermFun
525 (open CancelFactorCommon
526 val prove_conv = Bin_Simprocs.prove_conv
527 val mk_bal = HOLogic.mk_binop "HOL.divide"
528 val dest_bal = HOLogic.dest_bin "HOL.divide" Rat_Numeral_Simprocs.ratT
529 val simplify_meta_eq = cancel_simplify_meta_eq mult_divide_cancel_eq_if
532 val rat_cancel_factor =
534 [("rat_eq_cancel_factor", ["(l::rat) * m = n", "(l::rat) = m * n"], EqCancelFactor.proc),
535 ("rat_divide_cancel_factor", ["((l::rat) * m) / n", "(l::rat) / (m * n)"],
536 DivideCancelFactor.proc)];
540 Addsimprocs rat_cancel_factor;
547 fun test s = (Goal s; by (Asm_simp_tac 1));
549 test "x*k = k*(y::rat)";
550 test "k = k*(y::rat)";
551 test "a*(b*c) = (b::rat)";
552 test "a*(b*c) = d*(b::rat)*(x*a)";
555 test "(x*k) / (k*(y::rat)) = (uu::rat)";
556 test "(k) / (k*(y::rat)) = (uu::rat)";
557 test "(a*(b*c)) / ((b::rat)) = (uu::rat)";
558 test "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)";
560 (*FIXME: what do we do about this?*)
561 test "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z";
566 (****Instantiation of the generic linear arithmetic package****)
571 (* reduce contradictory <= to False *)
573 [order_less_irrefl, rat_numeral_0_eq_0, rat_numeral_1_eq_1,
575 add_rat_number_of, minus_rat_number_of, diff_rat_number_of,
576 mult_rat_number_of, eq_rat_number_of, less_rat_number_of];
578 val simprocs = [Rat_Times_Assoc.conv, Rat_Numeral_Simprocs.combine_numerals,
579 rat_cancel_numeral_factors_divide]@
580 Rat_Numeral_Simprocs.cancel_numerals @
581 Rat_Numeral_Simprocs.eval_numerals;
583 val mono_ss = simpset() addsimps
584 [add_mono,add_strict_mono,add_less_le_mono,add_le_less_mono];
586 val add_mono_thms_ordered_field =
587 map (fn s => prove_goal (the_context ()) s
588 (fn prems => [cut_facts_tac prems 1, asm_simp_tac mono_ss 1]))
589 ["(i < j) & (k = l) ==> i + k < j + (l::'a::ordered_field)",
590 "(i = j) & (k < l) ==> i + k < j + (l::'a::ordered_field)",
591 "(i < j) & (k <= l) ==> i + k < j + (l::'a::ordered_field)",
592 "(i <= j) & (k < l) ==> i + k < j + (l::'a::ordered_field)",
593 "(i < j) & (k < l) ==> i + k < j + (l::'a::ordered_field)"];
595 fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var;
597 val rat_mult_mono_thms =
598 [(rat_mult_strict_left_mono,
599 cvar(rat_mult_strict_left_mono, hd(tl(prems_of rat_mult_strict_left_mono)))),
601 cvar(rat_mult_left_mono, hd(tl(prems_of rat_mult_left_mono))))]
603 val simps = [True_implies_equals,
604 inst "a" "(number_of ?v)" right_distrib,
605 divide_1, times_divide_eq_right, times_divide_eq_left,
606 of_int_0, of_int_1, of_int_add, of_int_minus, of_int_diff,
607 of_int_mult, of_int_of_nat_eq, rat_number_of_def];
611 val fast_rat_arith_simproc = Simplifier.simproc (Theory.sign_of(the_context()))
612 "fast_rat_arith" ["(m::rat) < n","(m::rat) <= n", "(m::rat) = n"]
613 Fast_Arith.lin_arith_prover;
615 val nat_inj_thms = [of_nat_le_iff RS iffD2, of_nat_less_iff RS iffD2,
616 of_nat_eq_iff RS iffD2];
618 val int_inj_thms = [of_int_le_iff RS iffD2, of_int_less_iff RS iffD2,
619 of_int_eq_iff RS iffD2];
621 val rat_arith_setup =
622 [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
623 {add_mono_thms = add_mono_thms @ add_mono_thms_ordered_field,
624 mult_mono_thms = mult_mono_thms @ rat_mult_mono_thms,
625 inj_thms = int_inj_thms @ inj_thms,
626 lessD = lessD, (*Can't change LA_Data_Ref.lessD: the rats are dense!*)
627 simpset = simpset addsimps add_rules
629 addsimprocs simprocs}),
630 arith_inj_const("IntDef.of_nat", HOLogic.natT --> Rat_Numeral_Simprocs.ratT),
631 arith_inj_const("IntDef.of_int", HOLogic.intT --> Rat_Numeral_Simprocs.ratT),
632 arith_discrete ("Rational.rat",false),
633 Simplifier.change_simpset_of (op addsimprocs) [fast_rat_arith_simproc]];