1 (* Title: HOL/nat_simprocs.ML
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4 Copyright 2000 University of Cambridge
6 Simprocs for nat numerals.
9 Goal "number_of v + (number_of v' + (k::nat)) = \
10 \ (if neg (number_of v) then number_of v' + k \
11 \ else if neg (number_of v') then number_of v + k \
12 \ else number_of (bin_add v v') + k)";
14 qed "nat_number_of_add_left";
17 (** For combine_numerals **)
19 Goal "i*u + (j*u + k) = (i+j)*u + (k::nat)";
20 by (asm_simp_tac (simpset() addsimps [add_mult_distrib]) 1);
21 qed "left_add_mult_distrib";
24 (** For cancel_numerals **)
26 Goal "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)";
27 by (asm_simp_tac (simpset() addsplits [nat_diff_split]
28 addsimps [add_mult_distrib]) 1);
29 qed "nat_diff_add_eq1";
31 Goal "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))";
32 by (asm_simp_tac (simpset() addsplits [nat_diff_split]
33 addsimps [add_mult_distrib]) 1);
34 qed "nat_diff_add_eq2";
36 Goal "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)";
37 by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
38 addsimps [add_mult_distrib]));
39 qed "nat_eq_add_iff1";
41 Goal "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)";
42 by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
43 addsimps [add_mult_distrib]));
44 qed "nat_eq_add_iff2";
46 Goal "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)";
47 by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
48 addsimps [add_mult_distrib]));
49 qed "nat_less_add_iff1";
51 Goal "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)";
52 by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
53 addsimps [add_mult_distrib]));
54 qed "nat_less_add_iff2";
56 Goal "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)";
57 by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
58 addsimps [add_mult_distrib]));
59 qed "nat_le_add_iff1";
61 Goal "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)";
62 by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
63 addsimps [add_mult_distrib]));
64 qed "nat_le_add_iff2";
67 (** For cancel_numeral_factors **)
69 Goal "(Numeral0::nat) < k ==> (k*m <= k*n) = (m<=n)";
71 qed "nat_mult_le_cancel1";
73 Goal "(Numeral0::nat) < k ==> (k*m < k*n) = (m<n)";
75 qed "nat_mult_less_cancel1";
77 Goal "(Numeral0::nat) < k ==> (k*m = k*n) = (m=n)";
79 qed "nat_mult_eq_cancel1";
81 Goal "(Numeral0::nat) < k ==> (k*m) div (k*n) = (m div n)";
83 qed "nat_mult_div_cancel1";
86 (** For cancel_factor **)
88 Goal "(k*m <= k*n) = ((0::nat) < k --> m<=n)";
90 qed "nat_mult_le_cancel_disj";
92 Goal "(k*m < k*n) = ((0::nat) < k & m<n)";
94 qed "nat_mult_less_cancel_disj";
96 Goal "(k*m = k*n) = (k = (0::nat) | m=n)";
98 qed "nat_mult_eq_cancel_disj";
100 Goal "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)";
101 by (simp_tac (simpset() addsimps [nat_mult_div_cancel1]) 1);
102 qed "nat_mult_div_cancel_disj";
105 structure Nat_Numeral_Simprocs =
110 fun mk_numeral n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_bin n;
112 (*Decodes a unary or binary numeral to a NATURAL NUMBER*)
113 fun dest_numeral (Const ("0", _)) = 0
114 | dest_numeral (Const ("Suc", _) $ t) = 1 + dest_numeral t
115 | dest_numeral (Const("Numeral.number_of", _) $ w) =
116 (BasisLibrary.Int.max (0, HOLogic.dest_binum w)
117 handle TERM _ => raise TERM("Nat_Numeral_Simprocs.dest_numeral:1", [w]))
118 | dest_numeral t = raise TERM("Nat_Numeral_Simprocs.dest_numeral:2", [t]);
120 fun find_first_numeral past (t::terms) =
121 ((dest_numeral t, t, rev past @ terms)
122 handle TERM _ => find_first_numeral (t::past) terms)
123 | find_first_numeral past [] = raise TERM("find_first_numeral", []);
125 val zero = mk_numeral 0;
126 val mk_plus = HOLogic.mk_binop "op +";
128 (*Thus mk_sum[t] yields t+Numeral0; longer sums don't have a trailing zero*)
130 | mk_sum [t,u] = mk_plus (t, u)
131 | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
133 (*this version ALWAYS includes a trailing zero*)
134 fun long_mk_sum [] = zero
135 | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
137 val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
139 (*extract the outer Sucs from a term and convert them to a binary numeral*)
140 fun dest_Sucs (k, Const ("Suc", _) $ t) = dest_Sucs (k+1, t)
141 | dest_Sucs (0, t) = t
142 | dest_Sucs (k, t) = mk_plus (mk_numeral k, t);
145 let val (t,u) = dest_plus t
146 in dest_sum t @ dest_sum u end
147 handle TERM _ => [t];
149 fun dest_Sucs_sum t = dest_sum (dest_Sucs (0,t));
152 (** Other simproc items **)
154 val trans_tac = Int_Numeral_Simprocs.trans_tac;
156 val prove_conv = Int_Numeral_Simprocs.prove_conv;
158 val bin_simps = [add_nat_number_of, nat_number_of_add_left,
159 diff_nat_number_of, le_nat_number_of_eq_not_less,
160 less_nat_number_of, mult_nat_number_of,
161 thm "Let_number_of", nat_number_of] @
162 bin_arith_simps @ bin_rel_simps;
164 fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
165 fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ()))
167 val prep_pats = map prep_pat;
170 (*** CancelNumerals simprocs ***)
172 val one = mk_numeral 1;
173 val mk_times = HOLogic.mk_binop "op *";
177 | mk_prod (t :: ts) = if t = one then mk_prod ts
178 else mk_times (t, mk_prod ts);
180 val dest_times = HOLogic.dest_bin "op *" HOLogic.natT;
183 let val (t,u) = dest_times t
184 in dest_prod t @ dest_prod u end
185 handle TERM _ => [t];
187 (*DON'T do the obvious simplifications; that would create special cases*)
188 fun mk_coeff (k,t) = mk_times (mk_numeral k, t);
190 (*Express t as a product of (possibly) a numeral with other factors, sorted*)
192 let val ts = sort Term.term_ord (dest_prod t)
193 val (n, _, ts') = find_first_numeral [] ts
194 handle TERM _ => (1, one, ts)
195 in (n, mk_prod ts') end;
197 (*Find first coefficient-term THAT MATCHES u*)
198 fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
199 | find_first_coeff past u (t::terms) =
200 let val (n,u') = dest_coeff t
201 in if u aconv u' then (n, rev past @ terms)
202 else find_first_coeff (t::past) u terms
204 handle TERM _ => find_first_coeff (t::past) u terms;
207 (*Simplify Numeral1*n and n*Numeral1 to n*)
208 val add_0s = map rename_numerals [add_0, add_0_right];
209 val mult_1s = map rename_numerals [mult_1, mult_1_right];
211 (*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*)
212 val simplify_meta_eq =
213 Int_Numeral_Simprocs.simplify_meta_eq
214 [numeral_0_eq_0, numeral_1_eq_1, add_0, add_0_right,
215 mult_0, mult_0_right, mult_1, mult_1_right];
218 (** Restricted version of dest_Sucs_sum for nat_combine_numerals:
219 Simprocs never apply unless the original expression contains at least one
220 numeral in a coefficient position.
223 fun is_numeral (Const("Numeral.number_of", _) $ w) = true
224 | is_numeral _ = false;
226 fun prod_has_numeral t = exists is_numeral (dest_prod t);
228 fun restricted_dest_Sucs_sum t =
229 let val ts = dest_Sucs_sum t
230 in if exists prod_has_numeral ts then ts
231 else raise TERM("Nat_Numeral_Simprocs.restricted_dest_Sucs_sum", ts)
235 (*** Applying CancelNumeralsFun ***)
237 structure CancelNumeralsCommon =
240 val dest_sum = dest_Sucs_sum
241 val mk_coeff = mk_coeff
242 val dest_coeff = dest_coeff
243 val find_first_coeff = find_first_coeff []
244 val trans_tac = trans_tac
245 val norm_tac = ALLGOALS
246 (simp_tac (HOL_ss addsimps add_0s@mult_1s@
247 [add_0, Suc_eq_add_numeral_1]@add_ac))
248 THEN ALLGOALS (simp_tac
249 (HOL_ss addsimps bin_simps@add_ac@mult_ac))
250 val numeral_simp_tac = ALLGOALS
251 (simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps))
252 val simplify_meta_eq = simplify_meta_eq
256 structure EqCancelNumerals = CancelNumeralsFun
257 (open CancelNumeralsCommon
258 val prove_conv = prove_conv "nateq_cancel_numerals"
259 val mk_bal = HOLogic.mk_eq
260 val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
261 val bal_add1 = nat_eq_add_iff1 RS trans
262 val bal_add2 = nat_eq_add_iff2 RS trans
265 structure LessCancelNumerals = CancelNumeralsFun
266 (open CancelNumeralsCommon
267 val prove_conv = prove_conv "natless_cancel_numerals"
268 val mk_bal = HOLogic.mk_binrel "op <"
269 val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT
270 val bal_add1 = nat_less_add_iff1 RS trans
271 val bal_add2 = nat_less_add_iff2 RS trans
274 structure LeCancelNumerals = CancelNumeralsFun
275 (open CancelNumeralsCommon
276 val prove_conv = prove_conv "natle_cancel_numerals"
277 val mk_bal = HOLogic.mk_binrel "op <="
278 val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT
279 val bal_add1 = nat_le_add_iff1 RS trans
280 val bal_add2 = nat_le_add_iff2 RS trans
283 structure DiffCancelNumerals = CancelNumeralsFun
284 (open CancelNumeralsCommon
285 val prove_conv = prove_conv "natdiff_cancel_numerals"
286 val mk_bal = HOLogic.mk_binop "op -"
287 val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT
288 val bal_add1 = nat_diff_add_eq1 RS trans
289 val bal_add2 = nat_diff_add_eq2 RS trans
293 val cancel_numerals =
295 [("nateq_cancel_numerals",
296 prep_pats ["(l::nat) + m = n", "(l::nat) = m + n",
297 "(l::nat) * m = n", "(l::nat) = m * n",
298 "Suc m = n", "m = Suc n"],
299 EqCancelNumerals.proc),
300 ("natless_cancel_numerals",
301 prep_pats ["(l::nat) + m < n", "(l::nat) < m + n",
302 "(l::nat) * m < n", "(l::nat) < m * n",
303 "Suc m < n", "m < Suc n"],
304 LessCancelNumerals.proc),
305 ("natle_cancel_numerals",
306 prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n",
307 "(l::nat) * m <= n", "(l::nat) <= m * n",
308 "Suc m <= n", "m <= Suc n"],
309 LeCancelNumerals.proc),
310 ("natdiff_cancel_numerals",
311 prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)",
312 "(l::nat) * m - n", "(l::nat) - m * n",
313 "Suc m - n", "m - Suc n"],
314 DiffCancelNumerals.proc)];
317 (*** Applying CombineNumeralsFun ***)
319 structure CombineNumeralsData =
321 val add = op + : int*int -> int
322 val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *)
323 val dest_sum = restricted_dest_Sucs_sum
324 val mk_coeff = mk_coeff
325 val dest_coeff = dest_coeff
326 val left_distrib = left_add_mult_distrib RS trans
328 Int_Numeral_Simprocs.prove_conv_nohyps "nat_combine_numerals"
329 val trans_tac = trans_tac
330 val norm_tac = ALLGOALS
331 (simp_tac (HOL_ss addsimps add_0s@mult_1s@
332 [add_0, Suc_eq_add_numeral_1]@add_ac))
333 THEN ALLGOALS (simp_tac
334 (HOL_ss addsimps bin_simps@add_ac@mult_ac))
335 val numeral_simp_tac = ALLGOALS
336 (simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps))
337 val simplify_meta_eq = simplify_meta_eq
340 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
342 val combine_numerals =
343 prep_simproc ("nat_combine_numerals",
344 prep_pats ["(i::nat) + j", "Suc (i + j)"],
345 CombineNumerals.proc);
348 (*** Applying CancelNumeralFactorFun ***)
350 structure CancelNumeralFactorCommon =
352 val mk_coeff = mk_coeff
353 val dest_coeff = dest_coeff
354 val trans_tac = trans_tac
355 val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps
356 [Suc_eq_add_numeral_1]@mult_1s))
357 THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@mult_ac))
358 val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
359 val simplify_meta_eq = simplify_meta_eq
362 structure DivCancelNumeralFactor = CancelNumeralFactorFun
363 (open CancelNumeralFactorCommon
364 val prove_conv = prove_conv "natdiv_cancel_numeral_factor"
365 val mk_bal = HOLogic.mk_binop "Divides.op div"
366 val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.natT
367 val cancel = nat_mult_div_cancel1 RS trans
368 val neg_exchanges = false
371 structure EqCancelNumeralFactor = CancelNumeralFactorFun
372 (open CancelNumeralFactorCommon
373 val prove_conv = prove_conv "nateq_cancel_numeral_factor"
374 val mk_bal = HOLogic.mk_eq
375 val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
376 val cancel = nat_mult_eq_cancel1 RS trans
377 val neg_exchanges = false
380 structure LessCancelNumeralFactor = CancelNumeralFactorFun
381 (open CancelNumeralFactorCommon
382 val prove_conv = prove_conv "natless_cancel_numeral_factor"
383 val mk_bal = HOLogic.mk_binrel "op <"
384 val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT
385 val cancel = nat_mult_less_cancel1 RS trans
386 val neg_exchanges = true
389 structure LeCancelNumeralFactor = CancelNumeralFactorFun
390 (open CancelNumeralFactorCommon
391 val prove_conv = prove_conv "natle_cancel_numeral_factor"
392 val mk_bal = HOLogic.mk_binrel "op <="
393 val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT
394 val cancel = nat_mult_le_cancel1 RS trans
395 val neg_exchanges = true
398 val cancel_numeral_factors =
400 [("nateq_cancel_numeral_factors",
401 prep_pats ["(l::nat) * m = n", "(l::nat) = m * n"],
402 EqCancelNumeralFactor.proc),
403 ("natless_cancel_numeral_factors",
404 prep_pats ["(l::nat) * m < n", "(l::nat) < m * n"],
405 LessCancelNumeralFactor.proc),
406 ("natle_cancel_numeral_factors",
407 prep_pats ["(l::nat) * m <= n", "(l::nat) <= m * n"],
408 LeCancelNumeralFactor.proc),
409 ("natdiv_cancel_numeral_factors",
410 prep_pats ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
411 DivCancelNumeralFactor.proc)];
415 (*** Applying ExtractCommonTermFun ***)
417 (*this version ALWAYS includes a trailing one*)
418 fun long_mk_prod [] = one
419 | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts);
421 (*Find first term that matches u*)
422 fun find_first past u [] = raise TERM("find_first", [])
423 | find_first past u (t::terms) =
424 if u aconv t then (rev past @ terms)
425 else find_first (t::past) u terms
426 handle TERM _ => find_first (t::past) u terms;
428 (*Final simplification: cancel + and * *)
429 fun cancel_simplify_meta_eq cancel_th th =
430 Int_Numeral_Simprocs.simplify_meta_eq [zmult_1, zmult_1_right]
431 (([th, cancel_th]) MRS trans);
433 structure CancelFactorCommon =
435 val mk_sum = long_mk_prod
436 val dest_sum = dest_prod
437 val mk_coeff = mk_coeff
438 val dest_coeff = dest_coeff
439 val find_first = find_first []
440 val trans_tac = trans_tac
441 val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@mult_ac))
444 structure EqCancelFactor = ExtractCommonTermFun
445 (open CancelFactorCommon
446 val prove_conv = prove_conv "nat_eq_cancel_factor"
447 val mk_bal = HOLogic.mk_eq
448 val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
449 val simplify_meta_eq = cancel_simplify_meta_eq nat_mult_eq_cancel_disj
452 structure LessCancelFactor = ExtractCommonTermFun
453 (open CancelFactorCommon
454 val prove_conv = prove_conv "nat_less_cancel_factor"
455 val mk_bal = HOLogic.mk_binrel "op <"
456 val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT
457 val simplify_meta_eq = cancel_simplify_meta_eq nat_mult_less_cancel_disj
460 structure LeCancelFactor = ExtractCommonTermFun
461 (open CancelFactorCommon
462 val prove_conv = prove_conv "nat_leq_cancel_factor"
463 val mk_bal = HOLogic.mk_binrel "op <="
464 val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT
465 val simplify_meta_eq = cancel_simplify_meta_eq nat_mult_le_cancel_disj
468 structure DivideCancelFactor = ExtractCommonTermFun
469 (open CancelFactorCommon
470 val prove_conv = prove_conv "nat_divide_cancel_factor"
471 val mk_bal = HOLogic.mk_binop "Divides.op div"
472 val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.natT
473 val simplify_meta_eq = cancel_simplify_meta_eq nat_mult_div_cancel_disj
478 [("nat_eq_cancel_factor",
479 prep_pats ["(l::nat) * m = n", "(l::nat) = m * n"],
480 EqCancelFactor.proc),
481 ("nat_less_cancel_factor",
482 prep_pats ["(l::nat) * m < n", "(l::nat) < m * n"],
483 LessCancelFactor.proc),
484 ("nat_le_cancel_factor",
485 prep_pats ["(l::nat) * m <= n", "(l::nat) <= m * n"],
486 LeCancelFactor.proc),
487 ("nat_divide_cancel_factor",
488 prep_pats ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
489 DivideCancelFactor.proc)];
494 Addsimprocs Nat_Numeral_Simprocs.cancel_numerals;
495 Addsimprocs [Nat_Numeral_Simprocs.combine_numerals];
496 Addsimprocs Nat_Numeral_Simprocs.cancel_numeral_factors;
497 Addsimprocs Nat_Numeral_Simprocs.cancel_factor;
504 fun test s = (Goal s; by (Simp_tac 1));
507 test "l +( 2) + (2) + 2 + (l + 2) + (oo + 2) = (uu::nat)";
508 test "(2*length xs < 2*length xs + j)";
509 test "(2*length xs < length xs * 2 + j)";
510 test "2*u = (u::nat)";
511 test "2*u = Suc (u)";
512 test "(i + j + 12 + (k::nat)) - 15 = y";
513 test "(i + j + 12 + (k::nat)) - 5 = y";
514 test "Suc u - 2 = y";
515 test "Suc (Suc (Suc u)) - 2 = y";
516 test "(i + j + 2 + (k::nat)) - 1 = y";
517 test "(i + j + Numeral1 + (k::nat)) - 2 = y";
519 test "(2*x + (u*v) + y) - v*3*u = (w::nat)";
520 test "(2*x*u*v + 5 + (u*v)*4 + y) - v*u*4 = (w::nat)";
521 test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::nat)";
522 test "Suc (Suc (2*x*u*v + u*4 + y)) - u = w";
523 test "Suc ((u*v)*4) - v*3*u = w";
524 test "Suc (Suc ((u*v)*3)) - v*3*u = w";
526 test "(i + j + 12 + (k::nat)) = u + 15 + y";
527 test "(i + j + 32 + (k::nat)) - (u + 15 + y) = zz";
528 test "(i + j + 12 + (k::nat)) = u + 5 + y";
530 test "(i + j + 12 + k) = Suc (u + y)";
531 test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + 41 + k)";
532 test "(i + j + 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))";
533 test "Suc (Suc (Suc (Suc (Suc (u + y))))) - 5 = v";
534 test "(i + j + 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))";
535 test "2*y + 3*z + 2*u = Suc (u)";
536 test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = Suc (u)";
537 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::nat)";
538 test "6 + 2*y + 3*z + 4*u = Suc (vv + 2*u + z)";
539 test "(2*n*m) < (3*(m*n)) + (u::nat)";
541 (*negative numerals: FAIL*)
542 test "(i + j + -23 + (k::nat)) < u + 15 + y";
543 test "(i + j + 3 + (k::nat)) < u + -15 + y";
544 test "(i + j + -12 + (k::nat)) - 15 = y";
545 test "(i + j + 12 + (k::nat)) - -15 = y";
546 test "(i + j + -12 + (k::nat)) - -15 = y";
549 test "k + 3*k = (u::nat)";
550 test "Suc (i + 3) = u";
551 test "Suc (i + j + 3 + k) = u";
552 test "k + j + 3*k + j = (u::nat)";
553 test "Suc (j*i + i + k + 5 + 3*k + i*j*4) = (u::nat)";
554 test "(2*n*m) + (3*(m*n)) = (u::nat)";
555 (*negative numerals: FAIL*)
556 test "Suc (i + j + -3 + k) = u";
558 (*cancel_numeral_factors*)
559 test "9*x = 12 * (y::nat)";
560 test "(9*x) div (12 * (y::nat)) = z";
561 test "9*x < 12 * (y::nat)";
562 test "9*x <= 12 * (y::nat)";
565 test "x*k = k*(y::nat)";
566 test "k = k*(y::nat)";
567 test "a*(b*c) = (b::nat)";
568 test "a*(b*c) = d*(b::nat)*(x*a)";
570 test "x*k < k*(y::nat)";
571 test "k < k*(y::nat)";
572 test "a*(b*c) < (b::nat)";
573 test "a*(b*c) < d*(b::nat)*(x*a)";
575 test "x*k <= k*(y::nat)";
576 test "k <= k*(y::nat)";
577 test "a*(b*c) <= (b::nat)";
578 test "a*(b*c) <= d*(b::nat)*(x*a)";
580 test "(x*k) div (k*(y::nat)) = (uu::nat)";
581 test "(k) div (k*(y::nat)) = (uu::nat)";
582 test "(a*(b*c)) div ((b::nat)) = (uu::nat)";
583 test "(a*(b*c)) div (d*(b::nat)*(x*a)) = (uu::nat)";
587 (*** Prepare linear arithmetic for nat numerals ***)
591 (* reduce contradictory <= to False *)
593 [add_nat_number_of, diff_nat_number_of, mult_nat_number_of,
594 eq_nat_number_of, less_nat_number_of, le_nat_number_of_eq_not_less,
595 le_Suc_number_of,le_number_of_Suc,
596 less_Suc_number_of,less_number_of_Suc,
597 Suc_eq_number_of,eq_number_of_Suc,
598 mult_0, mult_0_right, mult_Suc, mult_Suc_right,
599 eq_number_of_0, eq_0_number_of, less_0_number_of,
600 nat_number_of, thm "Let_number_of", if_True, if_False];
602 val simprocs = [Nat_Times_Assoc.conv,
603 Nat_Numeral_Simprocs.combine_numerals]@
604 Nat_Numeral_Simprocs.cancel_numerals;
608 val nat_simprocs_setup =
609 [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
610 {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
611 inj_thms = inj_thms, lessD = lessD,
612 simpset = simpset addsimps add_rules
613 addsimps basic_renamed_arith_simps
614 addsimprocs simprocs})];