equal
deleted
inserted
replaced
491 by (induct_tac "n" 1); |
491 by (induct_tac "n" 1); |
492 by (ALLGOALS Asm_simp_tac); |
492 by (ALLGOALS Asm_simp_tac); |
493 qed "diff_add_0"; |
493 qed "diff_add_0"; |
494 Addsimps [diff_add_0]; |
494 Addsimps [diff_add_0]; |
495 |
495 |
|
496 |
496 (** Difference distributes over multiplication **) |
497 (** Difference distributes over multiplication **) |
497 |
498 |
498 Goal "!!m::nat. (m - n) * k = (m * k) - (n * k)"; |
499 Goal "!!m::nat. (m - n) * k = (m * k) - (n * k)"; |
499 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
500 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
500 by (ALLGOALS Asm_simp_tac); |
501 by (ALLGOALS Asm_simp_tac); |
673 bd diff_Suc_less_diff 1; |
674 bd diff_Suc_less_diff 1; |
674 by (auto_tac (claset(), simpset() addsimps [leI RS le_imp_less_Suc])); |
675 by (auto_tac (claset(), simpset() addsimps [leI RS le_imp_less_Suc])); |
675 qed "diff_Suc_le_diff"; |
676 qed "diff_Suc_le_diff"; |
676 AddIffs [diff_Suc_le_diff]; |
677 AddIffs [diff_Suc_le_diff]; |
677 |
678 |
|
679 Goal "0 < n ==> (m <= n-1) = (m<n)"; |
|
680 by (exhaust_tac "n" 1); |
|
681 by Auto_tac; |
|
682 by (ALLGOALS trans_tac); |
|
683 qed "le_pred_eq"; |
|
684 |
|
685 Goal "0 < n ==> (m-1 < n) = (m<=n)"; |
|
686 by (exhaust_tac "m" 1); |
|
687 by (auto_tac (claset(), simpset() addsimps [Suc_le_eq])); |
|
688 qed "less_pred_eq"; |
|
689 |
678 |
690 |
679 |
691 |
680 (** (Anti)Monotonicity of subtraction -- by Stefan Merz **) |
692 (** (Anti)Monotonicity of subtraction -- by Stefan Merz **) |
681 |
693 |
682 (* Monotonicity of subtraction in first argument *) |
694 (* Monotonicity of subtraction in first argument *) |