277 |
277 |
278 |
278 |
279 structure CombineNumeralsData = |
279 structure CombineNumeralsData = |
280 struct |
280 struct |
281 val add = op + : int*int -> int |
281 val add = op + : int*int -> int |
282 val mk_sum = long_mk_sum (*to work for e.g. # 2*x + # 3*x *) |
282 val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *) |
283 val dest_sum = dest_sum |
283 val dest_sum = dest_sum |
284 val mk_coeff = mk_coeff |
284 val mk_coeff = mk_coeff |
285 val dest_coeff = dest_coeff 1 |
285 val dest_coeff = dest_coeff 1 |
286 val left_distrib = left_zadd_zmult_distrib RS trans |
286 val left_distrib = left_zadd_zmult_distrib RS trans |
287 val prove_conv = prove_conv_nohyps "int_combine_numerals" |
287 val prove_conv = prove_conv_nohyps "int_combine_numerals" |
316 print_depth 22; |
316 print_depth 22; |
317 set timing; |
317 set timing; |
318 set trace_simp; |
318 set trace_simp; |
319 fun test s = (Goal s; by (Simp_tac 1)); |
319 fun test s = (Goal s; by (Simp_tac 1)); |
320 |
320 |
321 test "l + # 2 + # 2 + # 2 + (l + # 2) + (oo + # 2) = (uu::int)"; |
321 test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)"; |
322 |
322 |
323 test "# 2*u = (u::int)"; |
323 test "2*u = (u::int)"; |
324 test "(i + j + # 12 + (k::int)) - # 15 = y"; |
324 test "(i + j + 12 + (k::int)) - 15 = y"; |
325 test "(i + j + # 12 + (k::int)) - # 5 = y"; |
325 test "(i + j + 12 + (k::int)) - 5 = y"; |
326 |
326 |
327 test "y - b < (b::int)"; |
327 test "y - b < (b::int)"; |
328 test "y - (# 3*b + c) < (b::int) - # 2*c"; |
328 test "y - (3*b + c) < (b::int) - 2*c"; |
329 |
329 |
330 test "(# 2*x - (u*v) + y) - v*# 3*u = (w::int)"; |
330 test "(2*x - (u*v) + y) - v*3*u = (w::int)"; |
331 test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u*# 4 = (w::int)"; |
331 test "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)"; |
332 test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u = (w::int)"; |
332 test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)"; |
333 test "u*v - (x*u*v + (u*v)*# 4 + y) = (w::int)"; |
333 test "u*v - (x*u*v + (u*v)*4 + y) = (w::int)"; |
334 |
334 |
335 test "(i + j + # 12 + (k::int)) = u + # 15 + y"; |
335 test "(i + j + 12 + (k::int)) = u + 15 + y"; |
336 test "(i + j*# 2 + # 12 + (k::int)) = j + # 5 + y"; |
336 test "(i + j*2 + 12 + (k::int)) = j + 5 + y"; |
337 |
337 |
338 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)"; |
338 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)"; |
339 |
339 |
340 test "a + -(b+c) + b = (d::int)"; |
340 test "a + -(b+c) + b = (d::int)"; |
341 test "a + -(b+c) - b = (d::int)"; |
341 test "a + -(b+c) - b = (d::int)"; |
342 |
342 |
343 (*negative numerals*) |
343 (*negative numerals*) |
344 test "(i + j + # -2 + (k::int)) - (u + # 5 + y) = zz"; |
344 test "(i + j + -2 + (k::int)) - (u + 5 + y) = zz"; |
345 test "(i + j + # -3 + (k::int)) < u + # 5 + y"; |
345 test "(i + j + -3 + (k::int)) < u + 5 + y"; |
346 test "(i + j + # 3 + (k::int)) < u + # -6 + y"; |
346 test "(i + j + 3 + (k::int)) < u + -6 + y"; |
347 test "(i + j + # -12 + (k::int)) - # 15 = y"; |
347 test "(i + j + -12 + (k::int)) - 15 = y"; |
348 test "(i + j + # 12 + (k::int)) - # -15 = y"; |
348 test "(i + j + 12 + (k::int)) - -15 = y"; |
349 test "(i + j + # -12 + (k::int)) - # -15 = y"; |
349 test "(i + j + -12 + (k::int)) - -15 = y"; |
350 *) |
350 *) |
351 |
351 |
352 |
352 |
353 (** Constant folding for integer plus and times **) |
353 (** Constant folding for integer plus and times **) |
354 |
354 |
453 end; |
453 end; |
454 |
454 |
455 (* Some test data |
455 (* Some test data |
456 Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d"; |
456 Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d"; |
457 by (fast_arith_tac 1); |
457 by (fast_arith_tac 1); |
458 Goal "!!a::int. [| a < b; c < d |] ==> a-d+ # 2 <= b+(-c)"; |
458 Goal "!!a::int. [| a < b; c < d |] ==> a-d+ 2 <= b+(-c)"; |
459 by (fast_arith_tac 1); |
459 by (fast_arith_tac 1); |
460 Goal "!!a::int. [| a < b; c < d |] ==> a+c+ Numeral1 < b+d"; |
460 Goal "!!a::int. [| a < b; c < d |] ==> a+c+ Numeral1 < b+d"; |
461 by (fast_arith_tac 1); |
461 by (fast_arith_tac 1); |
462 Goal "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c"; |
462 Goal "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c"; |
463 by (fast_arith_tac 1); |
463 by (fast_arith_tac 1); |
464 Goal "!!a::int. [| a+b <= i+j; a<=b; i<=j |] \ |
464 Goal "!!a::int. [| a+b <= i+j; a<=b; i<=j |] \ |
465 \ ==> a+a <= j+j"; |
465 \ ==> a+a <= j+j"; |
466 by (fast_arith_tac 1); |
466 by (fast_arith_tac 1); |
467 Goal "!!a::int. [| a+b < i+j; a<b; i<j |] \ |
467 Goal "!!a::int. [| a+b < i+j; a<b; i<j |] \ |
468 \ ==> a+a - - # -1 < j+j - # 3"; |
468 \ ==> a+a - - -1 < j+j - 3"; |
469 by (fast_arith_tac 1); |
469 by (fast_arith_tac 1); |
470 Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k"; |
470 Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k"; |
471 by (arith_tac 1); |
471 by (arith_tac 1); |
472 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
472 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
473 \ ==> a <= l"; |
473 \ ==> a <= l"; |
480 by (fast_arith_tac 1); |
480 by (fast_arith_tac 1); |
481 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
481 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
482 \ ==> a+a+a+a+a+a <= l+l+l+l+i+l"; |
482 \ ==> a+a+a+a+a+a <= l+l+l+l+i+l"; |
483 by (fast_arith_tac 1); |
483 by (fast_arith_tac 1); |
484 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
484 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
485 \ ==> # 6*a <= # 5*l+i"; |
485 \ ==> 6*a <= 5*l+i"; |
486 by (fast_arith_tac 1); |
486 by (fast_arith_tac 1); |
487 *) |
487 *) |