1 (* Title: HOL/Integ/int_arith1.ML
3 Authors: Larry Paulson and Tobias Nipkow
5 Simprocs and decision procedure for linear arithmetic.
8 (** Misc ML bindings **)
10 val NCons_Pls = thm"NCons_Pls";
11 val NCons_Min = thm"NCons_Min";
12 val NCons_BIT = thm"NCons_BIT";
13 val number_of_Pls = thm"number_of_Pls";
14 val number_of_Min = thm"number_of_Min";
15 val number_of_BIT = thm"number_of_BIT";
16 val bin_succ_Pls = thm"bin_succ_Pls";
17 val bin_succ_Min = thm"bin_succ_Min";
18 val bin_succ_BIT = thm"bin_succ_BIT";
19 val bin_pred_Pls = thm"bin_pred_Pls";
20 val bin_pred_Min = thm"bin_pred_Min";
21 val bin_pred_BIT = thm"bin_pred_BIT";
22 val bin_minus_Pls = thm"bin_minus_Pls";
23 val bin_minus_Min = thm"bin_minus_Min";
24 val bin_minus_BIT = thm"bin_minus_BIT";
25 val bin_add_Pls = thm"bin_add_Pls";
26 val bin_add_Min = thm"bin_add_Min";
27 val bin_mult_Pls = thm"bin_mult_Pls";
28 val bin_mult_Min = thm"bin_mult_Min";
29 val bin_mult_BIT = thm"bin_mult_BIT";
31 val neg_def = thm "neg_def";
32 val iszero_def = thm "iszero_def";
34 val NCons_Pls_0 = thm"NCons_Pls_0";
35 val NCons_Pls_1 = thm"NCons_Pls_1";
36 val NCons_Min_0 = thm"NCons_Min_0";
37 val NCons_Min_1 = thm"NCons_Min_1";
38 val bin_succ_1 = thm"bin_succ_1";
39 val bin_succ_0 = thm"bin_succ_0";
40 val bin_pred_1 = thm"bin_pred_1";
41 val bin_pred_0 = thm"bin_pred_0";
42 val bin_minus_1 = thm"bin_minus_1";
43 val bin_minus_0 = thm"bin_minus_0";
44 val bin_add_BIT_11 = thm"bin_add_BIT_11";
45 val bin_add_BIT_10 = thm"bin_add_BIT_10";
46 val bin_add_BIT_0 = thm"bin_add_BIT_0";
47 val bin_add_Pls_right = thm"bin_add_Pls_right";
48 val bin_add_Min_right = thm"bin_add_Min_right";
49 val bin_add_BIT_BIT = thm"bin_add_BIT_BIT";
50 val bin_mult_1 = thm"bin_mult_1";
51 val bin_mult_0 = thm"bin_mult_0";
52 val number_of_NCons = thm"number_of_NCons";
53 val number_of_succ = thm"number_of_succ";
54 val number_of_pred = thm"number_of_pred";
55 val number_of_minus = thm"number_of_minus";
56 val number_of_add = thm"number_of_add";
57 val diff_number_of_eq = thm"diff_number_of_eq";
58 val number_of_mult = thm"number_of_mult";
59 val double_number_of_BIT = thm"double_number_of_BIT";
60 val numeral_0_eq_0 = thm"numeral_0_eq_0";
61 val numeral_1_eq_1 = thm"numeral_1_eq_1";
62 val numeral_m1_eq_minus_1 = thm"numeral_m1_eq_minus_1";
63 val mult_minus1 = thm"mult_minus1";
64 val mult_minus1_right = thm"mult_minus1_right";
65 val minus_number_of_mult = thm"minus_number_of_mult";
66 val zero_less_nat_eq = thm"zero_less_nat_eq";
67 val eq_number_of_eq = thm"eq_number_of_eq";
68 val iszero_number_of_Pls = thm"iszero_number_of_Pls";
69 val nonzero_number_of_Min = thm"nonzero_number_of_Min";
70 val iszero_number_of_BIT = thm"iszero_number_of_BIT";
71 val iszero_number_of_0 = thm"iszero_number_of_0";
72 val iszero_number_of_1 = thm"iszero_number_of_1";
73 val less_number_of_eq_neg = thm"less_number_of_eq_neg";
74 val le_number_of_eq = thm"le_number_of_eq";
75 val not_neg_number_of_Pls = thm"not_neg_number_of_Pls";
76 val neg_number_of_Min = thm"neg_number_of_Min";
77 val neg_number_of_BIT = thm"neg_number_of_BIT";
78 val le_number_of_eq_not_less = thm"le_number_of_eq_not_less";
79 val abs_number_of = thm"abs_number_of";
80 val number_of_reorient = thm"number_of_reorient";
81 val add_number_of_left = thm"add_number_of_left";
82 val mult_number_of_left = thm"mult_number_of_left";
83 val add_number_of_diff1 = thm"add_number_of_diff1";
84 val add_number_of_diff2 = thm"add_number_of_diff2";
85 val less_iff_diff_less_0 = thm"less_iff_diff_less_0";
86 val eq_iff_diff_eq_0 = thm"eq_iff_diff_eq_0";
87 val le_iff_diff_le_0 = thm"le_iff_diff_le_0";
89 val NCons_simps = thms"NCons_simps";
90 val bin_arith_extra_simps = thms"bin_arith_extra_simps";
91 val bin_arith_simps = thms"bin_arith_simps";
92 val bin_rel_simps = thms"bin_rel_simps";
94 val zless_imp_add1_zle = thm "zless_imp_add1_zle";
96 val combine_common_factor = thm"combine_common_factor";
97 val eq_add_iff1 = thm"eq_add_iff1";
98 val eq_add_iff2 = thm"eq_add_iff2";
99 val less_add_iff1 = thm"less_add_iff1";
100 val less_add_iff2 = thm"less_add_iff2";
101 val le_add_iff1 = thm"le_add_iff1";
102 val le_add_iff2 = thm"le_add_iff2";
104 val arith_special = thms"arith_special";
106 structure Bin_Simprocs =
108 fun prove_conv tacs sg (hyps: thm list) xs (t, u) =
109 if t aconv u then None
111 let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
112 in Some (Tactic.prove sg xs [] eq (K (EVERY tacs))) end
114 fun prove_conv_nohyps tacs sg = prove_conv tacs sg [];
115 fun prove_conv_nohyps_novars tacs sg = prove_conv tacs sg [] [];
117 fun prep_simproc (name, pats, proc) =
118 Simplifier.simproc (Theory.sign_of (the_context())) name pats proc;
120 fun is_numeral (Const("Numeral.number_of", _) $ w) = true
121 | is_numeral _ = false
123 fun simplify_meta_eq f_number_of_eq f_eq =
124 mk_meta_eq ([f_eq, f_number_of_eq] MRS trans)
126 (*reorientation simprules using ==, for the following simproc*)
127 val meta_zero_reorient = zero_reorient RS eq_reflection
128 val meta_one_reorient = one_reorient RS eq_reflection
129 val meta_number_of_reorient = number_of_reorient RS eq_reflection
131 (*reorientation simplification procedure: reorients (polymorphic)
132 0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
133 fun reorient_proc sg _ (_ $ t $ u) =
135 Const("0", _) => None
136 | Const("1", _) => None
137 | Const("Numeral.number_of", _) $ _ => None
138 | _ => Some (case t of
139 Const("0", _) => meta_zero_reorient
140 | Const("1", _) => meta_one_reorient
141 | Const("Numeral.number_of", _) $ _ => meta_number_of_reorient)
143 val reorient_simproc =
144 prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc)
149 Addsimps arith_special;
150 Addsimprocs [Bin_Simprocs.reorient_simproc];
153 structure Int_Numeral_Simprocs =
156 (*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic in simprocs
157 isn't complicated by the abstract 0 and 1.*)
158 val numeral_syms = [numeral_0_eq_0 RS sym, numeral_1_eq_1 RS sym];
160 (** New term ordering so that AC-rewriting brings numerals to the front **)
162 (*Order integers by absolute value and then by sign. The standard integer
163 ordering is not well-founded.*)
165 (case Int.compare (abs i, abs j) of
166 EQUAL => Int.compare (Int.sign i, Int.sign j)
169 (*This resembles Term.term_ord, but it puts binary numerals before other
173 fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) =
174 (case numterm_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
176 (Const("Numeral.number_of", _) $ v, Const("Numeral.number_of", _) $ w) =
177 num_ord (HOLogic.dest_binum v, HOLogic.dest_binum w)
178 | numterm_ord (Const("Numeral.number_of", _) $ _, _) = LESS
179 | numterm_ord (_, Const("Numeral.number_of", _) $ _) = GREATER
180 | numterm_ord (t, u) =
181 (case Int.compare (size_of_term t, size_of_term u) of
183 let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
184 (case hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)
187 and numterms_ord (ts, us) = list_ord numterm_ord (ts, us)
190 fun numtermless tu = (numterm_ord tu = LESS);
192 (*Defined in this file, but perhaps needed only for simprocs of type nat.*)
193 val num_ss = HOL_ss settermless numtermless;
198 fun mk_numeral T n = HOLogic.number_of_const T $ HOLogic.mk_bin n;
200 (*Decodes a binary INTEGER*)
201 fun dest_numeral (Const("0", _)) = 0
202 | dest_numeral (Const("1", _)) = 1
203 | dest_numeral (Const("Numeral.number_of", _) $ w) =
204 (HOLogic.dest_binum w
205 handle TERM _ => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
206 | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
208 fun find_first_numeral past (t::terms) =
209 ((dest_numeral t, rev past @ terms)
210 handle TERM _ => find_first_numeral (t::past) terms)
211 | find_first_numeral past [] = raise TERM("find_first_numeral", []);
213 val mk_plus = HOLogic.mk_binop "op +";
216 let val T = Term.fastype_of t
217 in Const ("uminus", T --> T) $ t
220 (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
221 fun mk_sum T [] = mk_numeral T 0
222 | mk_sum T [t,u] = mk_plus (t, u)
223 | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
225 (*this version ALWAYS includes a trailing zero*)
226 fun long_mk_sum T [] = mk_numeral T 0
227 | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
229 val dest_plus = HOLogic.dest_bin "op +" Term.dummyT;
231 (*decompose additions AND subtractions as a sum*)
232 fun dest_summing (pos, Const ("op +", _) $ t $ u, ts) =
233 dest_summing (pos, t, dest_summing (pos, u, ts))
234 | dest_summing (pos, Const ("op -", _) $ t $ u, ts) =
235 dest_summing (pos, t, dest_summing (not pos, u, ts))
236 | dest_summing (pos, t, ts) =
237 if pos then t::ts else mk_minus t :: ts;
239 fun dest_sum t = dest_summing (true, t, []);
241 val mk_diff = HOLogic.mk_binop "op -";
242 val dest_diff = HOLogic.dest_bin "op -" Term.dummyT;
244 val mk_times = HOLogic.mk_binop "op *";
247 let val one = mk_numeral T 1
250 | mk (t :: ts) = if t = one then mk ts else mk_times (t, mk ts)
253 (*This version ALWAYS includes a trailing one*)
254 fun long_mk_prod T [] = mk_numeral T 1
255 | long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts);
257 val dest_times = HOLogic.dest_bin "op *" Term.dummyT;
260 let val (t,u) = dest_times t
261 in dest_prod t @ dest_prod u end
262 handle TERM _ => [t];
264 (*DON'T do the obvious simplifications; that would create special cases*)
265 fun mk_coeff (k, t) = mk_times (mk_numeral (Term.fastype_of t) k, t);
267 (*Express t as a product of (possibly) a numeral with other sorted terms*)
268 fun dest_coeff sign (Const ("uminus", _) $ t) = dest_coeff (~sign) t
269 | dest_coeff sign t =
270 let val ts = sort Term.term_ord (dest_prod t)
271 val (n, ts') = find_first_numeral [] ts
272 handle TERM _ => (1, ts)
273 in (sign*n, mk_prod (Term.fastype_of t) ts') end;
275 (*Find first coefficient-term THAT MATCHES u*)
276 fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
277 | find_first_coeff past u (t::terms) =
278 let val (n,u') = dest_coeff 1 t
279 in if u aconv u' then (n, rev past @ terms)
280 else find_first_coeff (t::past) u terms
282 handle TERM _ => find_first_coeff (t::past) u terms;
285 (*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1*)
286 val add_0s = thms "add_0s";
287 val mult_1s = thms "mult_1s";
289 (*To perform binary arithmetic. The "left" rewriting handles patterns
290 created by the simprocs, such as 3 * (5 * x). *)
291 val bin_simps = [numeral_0_eq_0 RS sym, numeral_1_eq_1 RS sym,
292 add_number_of_left, mult_number_of_left] @
293 bin_arith_simps @ bin_rel_simps;
295 (*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms
296 during re-arrangement*)
297 val non_add_bin_simps =
298 bin_simps \\ [add_number_of_left, number_of_add RS sym];
300 (*To evaluate binary negations of coefficients*)
301 val minus_simps = NCons_simps @
302 [numeral_m1_eq_minus_1 RS sym, number_of_minus RS sym,
303 bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
304 bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
306 (*To let us treat subtraction as addition*)
307 val diff_simps = [diff_minus, minus_add_distrib, minus_minus];
309 (*push the unary minus down: - x * y = x * - y *)
310 val minus_mult_eq_1_to_2 =
311 [minus_mult_left RS sym, minus_mult_right] MRS trans |> standard;
313 (*to extract again any uncancelled minuses*)
314 val minus_from_mult_simps =
315 [minus_minus, minus_mult_left RS sym, minus_mult_right RS sym];
317 (*combine unary minus with numeric literals, however nested within a product*)
318 val mult_minus_simps =
319 [mult_assoc, minus_mult_left, minus_mult_eq_1_to_2];
321 (*Apply the given rewrite (if present) just once*)
322 fun trans_tac None = all_tac
323 | trans_tac (Some th) = ALLGOALS (rtac (th RS trans));
325 fun simplify_meta_eq rules =
326 simplify (HOL_basic_ss addeqcongs[eq_cong2] addsimps rules)
329 structure CancelNumeralsCommon =
332 val dest_sum = dest_sum
333 val mk_coeff = mk_coeff
334 val dest_coeff = dest_coeff 1
335 val find_first_coeff = find_first_coeff []
336 val trans_tac = trans_tac
338 ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
339 diff_simps@minus_simps@add_ac))
340 THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@mult_minus_simps))
341 THEN ALLGOALS (simp_tac (HOL_ss addsimps minus_from_mult_simps@
343 val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
344 val simplify_meta_eq = simplify_meta_eq (add_0s@mult_1s)
348 structure EqCancelNumerals = CancelNumeralsFun
349 (open CancelNumeralsCommon
350 val prove_conv = Bin_Simprocs.prove_conv
351 val mk_bal = HOLogic.mk_eq
352 val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
353 val bal_add1 = eq_add_iff1 RS trans
354 val bal_add2 = eq_add_iff2 RS trans
357 structure LessCancelNumerals = CancelNumeralsFun
358 (open CancelNumeralsCommon
359 val prove_conv = Bin_Simprocs.prove_conv
360 val mk_bal = HOLogic.mk_binrel "op <"
361 val dest_bal = HOLogic.dest_bin "op <" Term.dummyT
362 val bal_add1 = less_add_iff1 RS trans
363 val bal_add2 = less_add_iff2 RS trans
366 structure LeCancelNumerals = CancelNumeralsFun
367 (open CancelNumeralsCommon
368 val prove_conv = Bin_Simprocs.prove_conv
369 val mk_bal = HOLogic.mk_binrel "op <="
370 val dest_bal = HOLogic.dest_bin "op <=" Term.dummyT
371 val bal_add1 = le_add_iff1 RS trans
372 val bal_add2 = le_add_iff2 RS trans
375 val cancel_numerals =
376 map Bin_Simprocs.prep_simproc
377 [("inteq_cancel_numerals",
378 ["(l::'a::number_ring) + m = n",
379 "(l::'a::number_ring) = m + n",
380 "(l::'a::number_ring) - m = n",
381 "(l::'a::number_ring) = m - n",
382 "(l::'a::number_ring) * m = n",
383 "(l::'a::number_ring) = m * n"],
384 EqCancelNumerals.proc),
385 ("intless_cancel_numerals",
386 ["(l::'a::{ordered_idom,number_ring}) + m < n",
387 "(l::'a::{ordered_idom,number_ring}) < m + n",
388 "(l::'a::{ordered_idom,number_ring}) - m < n",
389 "(l::'a::{ordered_idom,number_ring}) < m - n",
390 "(l::'a::{ordered_idom,number_ring}) * m < n",
391 "(l::'a::{ordered_idom,number_ring}) < m * n"],
392 LessCancelNumerals.proc),
393 ("intle_cancel_numerals",
394 ["(l::'a::{ordered_idom,number_ring}) + m <= n",
395 "(l::'a::{ordered_idom,number_ring}) <= m + n",
396 "(l::'a::{ordered_idom,number_ring}) - m <= n",
397 "(l::'a::{ordered_idom,number_ring}) <= m - n",
398 "(l::'a::{ordered_idom,number_ring}) * m <= n",
399 "(l::'a::{ordered_idom,number_ring}) <= m * n"],
400 LeCancelNumerals.proc)];
403 structure CombineNumeralsData =
405 val add = op + : int*int -> int
406 val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *)
407 val dest_sum = dest_sum
408 val mk_coeff = mk_coeff
409 val dest_coeff = dest_coeff 1
410 val left_distrib = combine_common_factor RS trans
411 val prove_conv = Bin_Simprocs.prove_conv_nohyps
412 val trans_tac = trans_tac
414 ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
415 diff_simps@minus_simps@add_ac))
416 THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@mult_minus_simps))
417 THEN ALLGOALS (simp_tac (HOL_ss addsimps minus_from_mult_simps@
419 val numeral_simp_tac = ALLGOALS
420 (simp_tac (HOL_ss addsimps add_0s@bin_simps))
421 val simplify_meta_eq = simplify_meta_eq (add_0s@mult_1s)
424 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
426 val combine_numerals =
427 Bin_Simprocs.prep_simproc
428 ("int_combine_numerals",
429 ["(i::'a::number_ring) + j", "(i::'a::number_ring) - j"],
430 CombineNumerals.proc);
434 Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
435 Addsimprocs [Int_Numeral_Simprocs.combine_numerals];
441 fun test s = (Goal s, by (Simp_tac 1));
443 test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)";
445 test "2*u = (u::int)";
446 test "(i + j + 12 + (k::int)) - 15 = y";
447 test "(i + j + 12 + (k::int)) - 5 = y";
449 test "y - b < (b::int)";
450 test "y - (3*b + c) < (b::int) - 2*c";
452 test "(2*x - (u*v) + y) - v*3*u = (w::int)";
453 test "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)";
454 test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)";
455 test "u*v - (x*u*v + (u*v)*4 + y) = (w::int)";
457 test "(i + j + 12 + (k::int)) = u + 15 + y";
458 test "(i + j*2 + 12 + (k::int)) = j + 5 + y";
460 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::int)";
462 test "a + -(b+c) + b = (d::int)";
463 test "a + -(b+c) - b = (d::int)";
465 (*negative numerals*)
466 test "(i + j + -2 + (k::int)) - (u + 5 + y) = zz";
467 test "(i + j + -3 + (k::int)) < u + 5 + y";
468 test "(i + j + 3 + (k::int)) < u + -6 + y";
469 test "(i + j + -12 + (k::int)) - 15 = y";
470 test "(i + j + 12 + (k::int)) - -15 = y";
471 test "(i + j + -12 + (k::int)) - -15 = y";
475 (** Constant folding for multiplication in semirings **)
477 (*We do not need folding for addition: combine_numerals does the same thing*)
479 structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
482 val eq_reflection = eq_reflection
483 val sg_ref = Sign.self_ref (Theory.sign_of (the_context ()))
487 structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
489 val assoc_fold_simproc =
490 Bin_Simprocs.prep_simproc
491 ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"],
492 Semiring_Times_Assoc.proc);
494 Addsimprocs [assoc_fold_simproc];
499 (*** decision procedure for linear arithmetic ***)
501 (*---------------------------------------------------------------------------*)
502 (* Linear arithmetic *)
503 (*---------------------------------------------------------------------------*)
506 Instantiation of the generic linear arithmetic package for int.
509 (* Update parameters of arithmetic prover *)
512 (* reduce contradictory <= to False *)
514 simp_thms @ bin_arith_simps @ bin_rel_simps @ arith_special @
515 [neg_le_iff_le, numeral_0_eq_0, numeral_1_eq_1,
516 minus_zero, diff_minus, left_minus, right_minus,
517 mult_zero_left, mult_zero_right, mult_1, mult_1_right,
518 minus_mult_left RS sym, minus_mult_right RS sym,
519 minus_add_distrib, minus_minus, mult_assoc,
520 of_nat_0, of_nat_1, of_nat_Suc, of_nat_add, of_nat_mult,
521 of_int_0, of_int_1, of_int_add, of_int_mult, int_eq_of_nat,
522 zero_neq_one, zero_less_one, zero_le_one,
523 zero_neq_one RS not_sym, not_one_le_zero, not_one_less_zero];
525 val simprocs = [assoc_fold_simproc, Int_Numeral_Simprocs.combine_numerals]@
526 Int_Numeral_Simprocs.cancel_numerals;
530 val int_arith_setup =
531 [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
532 {add_mono_thms = add_mono_thms,
533 mult_mono_thms = mult_mono_thms,
534 inj_thms = [zle_int RS iffD2,int_int_eq RS iffD2] @ inj_thms,
535 lessD = lessD @ [zless_imp_add1_zle],
536 simpset = simpset addsimps add_rules
538 addcongs [if_weak_cong]}),
539 arith_inj_const ("IntDef.of_nat", HOLogic.natT --> HOLogic.intT),
540 arith_inj_const ("IntDef.int", HOLogic.natT --> HOLogic.intT),
541 arith_discrete ("IntDef.int", true)];
545 val fast_int_arith_simproc =
546 Simplifier.simproc (Theory.sign_of (the_context()))
548 ["(m::'a::{ordered_idom,number_ring}) < n",
549 "(m::'a::{ordered_idom,number_ring}) <= n",
550 "(m::'a::{ordered_idom,number_ring}) = n"] Fast_Arith.lin_arith_prover;
552 Addsimprocs [fast_int_arith_simproc]
556 Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
557 by (fast_arith_tac 1);
558 Goal "!!a::int. [| a < b; c < d |] ==> a-d+ 2 <= b+(-c)";
559 by (fast_arith_tac 1);
560 Goal "!!a::int. [| a < b; c < d |] ==> a+c+ 1 < b+d";
561 by (fast_arith_tac 1);
562 Goal "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c";
563 by (fast_arith_tac 1);
564 Goal "!!a::int. [| a+b <= i+j; a<=b; i<=j |] \
566 by (fast_arith_tac 1);
567 Goal "!!a::int. [| a+b < i+j; a<b; i<j |] \
568 \ ==> a+a - - -1 < j+j - 3";
569 by (fast_arith_tac 1);
570 Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
572 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
574 by (fast_arith_tac 1);
575 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
576 \ ==> a+a+a+a <= l+l+l+l";
577 by (fast_arith_tac 1);
578 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
579 \ ==> a+a+a+a+a <= l+l+l+l+i";
580 by (fast_arith_tac 1);
581 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
582 \ ==> a+a+a+a+a+a <= l+l+l+l+i+l";
583 by (fast_arith_tac 1);
584 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
586 by (fast_arith_tac 1);