415 Goal "!!i j k::nat. i<=j ==> (j-i=k) = (j=k+i)"; |
415 Goal "!!i j k::nat. i<=j ==> (j-i=k) = (j=k+i)"; |
416 by Safe_tac; |
416 by Safe_tac; |
417 by (ALLGOALS Asm_simp_tac); |
417 by (ALLGOALS Asm_simp_tac); |
418 qed "le_imp_diff_is_add"; |
418 qed "le_imp_diff_is_add"; |
419 |
419 |
420 Goal "m < Suc(n) ==> m-n = 0"; |
420 Goal "(m-n = 0) = (m <= n)"; |
421 by (etac rev_mp 1); |
421 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
422 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
422 by (ALLGOALS (asm_simp_tac (simpset() addsimps [le_eq_less_Suc]))); |
423 by (asm_simp_tac (simpset() addsimps [less_Suc_eq]) 1); |
423 qed "diff_is_0_eq"; |
424 by (ALLGOALS Asm_simp_tac); |
424 Addsimps [diff_is_0_eq RS iffD2]; |
425 qed "less_imp_diff_is_0"; |
|
426 |
425 |
427 Goal "m-n = 0 --> n-m = 0 --> m=n"; |
426 Goal "m-n = 0 --> n-m = 0 --> m=n"; |
428 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
427 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
429 by (REPEAT(Simp_tac 1 THEN TRY(atac 1))); |
428 by (REPEAT(Simp_tac 1 THEN TRY(atac 1))); |
430 qed_spec_mp "diffs0_imp_equal"; |
429 qed_spec_mp "diffs0_imp_equal"; |
439 by (res_inst_tac [("x","j - i")] exI 1); |
438 by (res_inst_tac [("x","j - i")] exI 1); |
440 by (asm_simp_tac (simpset() addsimps [add_diff_inverse, less_not_sym]) 1); |
439 by (asm_simp_tac (simpset() addsimps [add_diff_inverse, less_not_sym]) 1); |
441 qed "less_imp_add_positive"; |
440 qed "less_imp_add_positive"; |
442 |
441 |
443 Goal "Suc(m)-n = (if m<n then 0 else Suc(m-n))"; |
442 Goal "Suc(m)-n = (if m<n then 0 else Suc(m-n))"; |
444 by (simp_tac (simpset() addsimps [less_imp_diff_is_0, |
443 by (simp_tac (simpset() addsimps [leI, Suc_le_eq, |
445 not_less_eq, Suc_diff_n]) 1); |
444 le_imp_less_Suc RS Suc_diff_n]) 1); |
446 qed "if_Suc_diff_n"; |
445 qed "if_Suc_diff_n"; |
447 |
446 |
448 Goal "Suc(m)-n <= Suc(m-n)"; |
447 Goal "Suc(m)-n <= Suc(m-n)"; |
449 by (simp_tac (simpset() addsimps [if_Suc_diff_n]) 1); |
448 by (simp_tac (simpset() addsimps [if_Suc_diff_n]) 1); |
450 qed "diff_Suc_le_Suc_diff"; |
449 qed "diff_Suc_le_Suc_diff"; |
483 \ Suc (m - Suc na) - Suc (n - Suc na) = m-n" 1); |
482 \ Suc (m - Suc na) - Suc (n - Suc na) = m-n" 1); |
484 by (Asm_full_simp_tac 1); |
483 by (Asm_full_simp_tac 1); |
485 by (blast_tac (claset() addIs [le_trans]) 1); |
484 by (blast_tac (claset() addIs [le_trans]) 1); |
486 by (auto_tac (claset() addIs [Suc_leD], simpset() delsimps [diff_Suc_Suc])); |
485 by (auto_tac (claset() addIs [Suc_leD], simpset() delsimps [diff_Suc_Suc])); |
487 by (asm_full_simp_tac (simpset() delsimps [Suc_less_eq] |
486 by (asm_full_simp_tac (simpset() delsimps [Suc_less_eq] |
488 addsimps [Suc_diff_n RS sym, le_eq_less_Suc]) 1); |
487 addsimps [le_imp_less_Suc RS Suc_diff_n RS sym]) 1); |
489 qed "diff_right_cancel"; |
488 qed "diff_right_cancel"; |
490 |
489 |
491 Goal "!!n::nat. n - (n+m) = 0"; |
490 Goal "!!n::nat. n - (n+m) = 0"; |
492 by (induct_tac "n" 1); |
491 by (induct_tac "n" 1); |
493 by (ALLGOALS Asm_simp_tac); |
492 by (ALLGOALS Asm_simp_tac); |
621 by (rtac le_add2 1); |
620 by (rtac le_add2 1); |
622 by (Asm_full_simp_tac 1); |
621 by (Asm_full_simp_tac 1); |
623 qed "add_less_imp_less_diff"; |
622 qed "add_less_imp_less_diff"; |
624 |
623 |
625 Goal "n <= m ==> Suc m - n = Suc (m - n)"; |
624 Goal "n <= m ==> Suc m - n = Suc (m - n)"; |
626 by (asm_full_simp_tac (simpset() addsimps [Suc_diff_n, le_eq_less_Suc]) 1); |
625 by (asm_full_simp_tac (simpset() addsimps [le_imp_less_Suc RS Suc_diff_n]) 1); |
627 qed "Suc_diff_le"; |
626 qed "Suc_diff_le"; |
628 |
627 |
629 Goal "Suc i <= n ==> Suc (n - Suc i) = n - i"; |
628 Goal "Suc i <= n ==> Suc (n - Suc i) = n - i"; |
630 by (asm_full_simp_tac |
629 by (asm_full_simp_tac |
631 (simpset() addsimps [Suc_diff_n RS sym, le_eq_less_Suc]) 1); |
630 (simpset() addsimps [Suc_diff_n RS sym, le_eq_less_Suc]) 1); |
648 |
647 |
649 Goal "!!i::nat. 0<k ==> j<i --> j+k-i < k"; |
648 Goal "!!i::nat. 0<k ==> j<i --> j+k-i < k"; |
650 by (res_inst_tac [("m","j"),("n","i")] diff_induct 1); |
649 by (res_inst_tac [("m","j"),("n","i")] diff_induct 1); |
651 by (ALLGOALS Asm_simp_tac); |
650 by (ALLGOALS Asm_simp_tac); |
652 qed_spec_mp "add_diff_less"; |
651 qed_spec_mp "add_diff_less"; |
|
652 |
|
653 |
|
654 Goal "m-1 < n ==> m <= n"; |
|
655 by (exhaust_tac "m" 1); |
|
656 by (auto_tac (claset(), simpset() addsimps [Suc_le_eq])); |
|
657 qed "pred_less_imp_le"; |
|
658 |
|
659 Goal "j<=i ==> i - j < Suc i - j"; |
|
660 by (REPEAT (etac rev_mp 1)); |
|
661 by (res_inst_tac [("m","i"),("n","j")] diff_induct 1); |
|
662 by Auto_tac; |
|
663 qed "diff_less_Suc_diff"; |
|
664 |
|
665 Goal "i - j <= Suc i - j"; |
|
666 by (res_inst_tac [("m","i"),("n","j")] diff_induct 1); |
|
667 by Auto_tac; |
|
668 qed "diff_le_Suc_diff"; |
|
669 AddIffs [diff_le_Suc_diff]; |
|
670 |
|
671 Goal "n - Suc i <= n - i"; |
|
672 by (case_tac "i<n" 1); |
|
673 bd diff_Suc_less_diff 1; |
|
674 by (auto_tac (claset(), simpset() addsimps [leI RS le_imp_less_Suc])); |
|
675 qed "diff_Suc_le_diff"; |
|
676 AddIffs [diff_Suc_le_diff]; |
653 |
677 |
654 |
678 |
655 |
679 |
656 (** (Anti)Monotonicity of subtraction -- by Stefan Merz **) |
680 (** (Anti)Monotonicity of subtraction -- by Stefan Merz **) |
657 |
681 |