498 ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac); |
498 ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac); |
499 *) |
499 *) |
500 |
500 |
501 (* Some test data |
501 (* Some test data |
502 Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d"; |
502 Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d"; |
503 by(fast_arith_tac 1); |
503 by (fast_arith_tac 1); |
504 Goal "!!a::int. [| a < b; c < d |] ==> a-d+ #2 <= b+(-c)"; |
504 Goal "!!a::int. [| a < b; c < d |] ==> a-d+ #2 <= b+(-c)"; |
505 by(fast_arith_tac 1); |
505 by (fast_arith_tac 1); |
506 Goal "!!a::int. [| a < b; c < d |] ==> a+c+ #1 < b+d"; |
506 Goal "!!a::int. [| a < b; c < d |] ==> a+c+ #1 < b+d"; |
507 by(fast_arith_tac 1); |
507 by (fast_arith_tac 1); |
508 Goal "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c"; |
508 Goal "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c"; |
509 by(fast_arith_tac 1); |
509 by (fast_arith_tac 1); |
510 Goal "!!a::int. [| a+b <= i+j; a<=b; i<=j |] \ |
510 Goal "!!a::int. [| a+b <= i+j; a<=b; i<=j |] \ |
511 \ ==> a+a <= j+j"; |
511 \ ==> a+a <= j+j"; |
512 by(fast_arith_tac 1); |
512 by (fast_arith_tac 1); |
513 Goal "!!a::int. [| a+b < i+j; a<b; i<j |] \ |
513 Goal "!!a::int. [| a+b < i+j; a<b; i<j |] \ |
514 \ ==> a+a - - #-1 < j+j - #3"; |
514 \ ==> a+a - - #-1 < j+j - #3"; |
515 by(fast_arith_tac 1); |
515 by (fast_arith_tac 1); |
516 Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k"; |
516 Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k"; |
517 by(arith_tac 1); |
517 by (arith_tac 1); |
518 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
518 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
519 \ ==> a <= l"; |
519 \ ==> a <= l"; |
520 by(fast_arith_tac 1); |
520 by (fast_arith_tac 1); |
521 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
521 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
522 \ ==> a+a+a+a <= l+l+l+l"; |
522 \ ==> a+a+a+a <= l+l+l+l"; |
523 by(fast_arith_tac 1); |
523 by (fast_arith_tac 1); |
524 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
524 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
525 \ ==> a+a+a+a+a <= l+l+l+l+i"; |
525 \ ==> a+a+a+a+a <= l+l+l+l+i"; |
526 by(fast_arith_tac 1); |
526 by (fast_arith_tac 1); |
527 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
527 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
528 \ ==> a+a+a+a+a+a <= l+l+l+l+i+l"; |
528 \ ==> a+a+a+a+a+a <= l+l+l+l+i+l"; |
529 by(fast_arith_tac 1); |
529 by (fast_arith_tac 1); |
530 *) |
530 *) |
531 |
531 |
532 (*---------------------------------------------------------------------------*) |
532 (*---------------------------------------------------------------------------*) |
533 (* End of linear arithmetic *) |
533 (* End of linear arithmetic *) |
534 (*---------------------------------------------------------------------------*) |
534 (*---------------------------------------------------------------------------*) |
546 Addsimps [add_integ_of_left, mult_integ_of_left]; |
546 Addsimps [add_integ_of_left, mult_integ_of_left]; |
547 |
547 |
548 (** Simplification of inequalities involving numerical constants **) |
548 (** Simplification of inequalities involving numerical constants **) |
549 |
549 |
550 Goal "(w <= z + #1) = (w<=z | w = z + #1)"; |
550 Goal "(w <= z + #1) = (w<=z | w = z + #1)"; |
551 by(arith_tac 1); |
551 by (arith_tac 1); |
552 qed "zle_add1_eq"; |
552 qed "zle_add1_eq"; |
553 |
553 |
554 Goal "(w <= z - #1) = (w<z)"; |
554 Goal "(w <= z - #1) = (w<z)"; |
555 by(arith_tac 1); |
555 by (arith_tac 1); |
556 qed "zle_diff1_eq"; |
556 qed "zle_diff1_eq"; |
557 Addsimps [zle_diff1_eq]; |
557 Addsimps [zle_diff1_eq]; |
558 |
558 |
559 (*2nd premise can be proved automatically if v is a literal*) |
559 (*2nd premise can be proved automatically if v is a literal*) |
560 Goal "[| w <= z; #0 <= v |] ==> w <= z + v"; |
560 Goal "[| w <= z; #0 <= v |] ==> w <= z + v"; |
561 by(fast_arith_tac 1); |
561 by (fast_arith_tac 1); |
562 qed "zle_imp_zle_zadd"; |
562 qed "zle_imp_zle_zadd"; |
563 |
563 |
564 Goal "w <= z ==> w <= z + #1"; |
564 Goal "w <= z ==> w <= z + #1"; |
565 by(fast_arith_tac 1); |
565 by (fast_arith_tac 1); |
566 qed "zle_imp_zle_zadd1"; |
566 qed "zle_imp_zle_zadd1"; |
567 |
567 |
568 (*2nd premise can be proved automatically if v is a literal*) |
568 (*2nd premise can be proved automatically if v is a literal*) |
569 Goal "[| w < z; #0 <= v |] ==> w < z + v"; |
569 Goal "[| w < z; #0 <= v |] ==> w < z + v"; |
570 by(fast_arith_tac 1); |
570 by (fast_arith_tac 1); |
571 qed "zless_imp_zless_zadd"; |
571 qed "zless_imp_zless_zadd"; |
572 |
572 |
573 Goal "w < z ==> w < z + #1"; |
573 Goal "w < z ==> w < z + #1"; |
574 by(fast_arith_tac 1); |
574 by (fast_arith_tac 1); |
575 qed "zless_imp_zless_zadd1"; |
575 qed "zless_imp_zless_zadd1"; |
576 |
576 |
577 Goal "(w < z + #1) = (w<=z)"; |
577 Goal "(w < z + #1) = (w<=z)"; |
578 by(arith_tac 1); |
578 by (arith_tac 1); |
579 qed "zle_add1_eq_le"; |
579 qed "zle_add1_eq_le"; |
580 Addsimps [zle_add1_eq_le]; |
580 Addsimps [zle_add1_eq_le]; |
581 |
581 |
582 Goal "(z = z + w) = (w = #0)"; |
582 Goal "(z = z + w) = (w = #0)"; |
583 by(arith_tac 1); |
583 by (arith_tac 1); |
584 qed "zadd_left_cancel0"; |
584 qed "zadd_left_cancel0"; |
585 Addsimps [zadd_left_cancel0]; |
585 Addsimps [zadd_left_cancel0]; |
586 |
586 |
587 (*LOOPS as a simprule!*) |
587 (*LOOPS as a simprule!*) |
588 Goal "[| w + v < z; #0 <= v |] ==> w < z"; |
588 Goal "[| w + v < z; #0 <= v |] ==> w < z"; |
589 by(fast_arith_tac 1); |
589 by (fast_arith_tac 1); |
590 qed "zless_zadd_imp_zless"; |
590 qed "zless_zadd_imp_zless"; |
591 |
591 |
592 (*LOOPS as a simprule! Analogous to Suc_lessD*) |
592 (*LOOPS as a simprule! Analogous to Suc_lessD*) |
593 Goal "w + #1 < z ==> w < z"; |
593 Goal "w + #1 < z ==> w < z"; |
594 by(fast_arith_tac 1); |
594 by (fast_arith_tac 1); |
595 qed "zless_zadd1_imp_zless"; |
595 qed "zless_zadd1_imp_zless"; |
596 |
596 |
597 Goal "w + #-1 = w - #1"; |
597 Goal "w + #-1 = w - #1"; |
598 by (Simp_tac 1); |
598 by (Simp_tac 1); |
599 qed "zplus_minus1_conv"; |
599 qed "zplus_minus1_conv"; |