equal
deleted
inserted
replaced
372 |
372 |
373 goal Arith.thy "!!m::nat. m - n <= m"; |
373 goal Arith.thy "!!m::nat. m - n <= m"; |
374 by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1); |
374 by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1); |
375 by (ALLGOALS Asm_simp_tac); |
375 by (ALLGOALS Asm_simp_tac); |
376 qed "diff_le_self"; |
376 qed "diff_le_self"; |
|
377 Addsimps [diff_le_self]; |
377 |
378 |
378 goal Arith.thy "!!i::nat. i-j-k = i - (j+k)"; |
379 goal Arith.thy "!!i::nat. i-j-k = i - (j+k)"; |
379 by (res_inst_tac [("m","i"),("n","j")] diff_induct 1); |
380 by (res_inst_tac [("m","i"),("n","j")] diff_induct 1); |
380 by (ALLGOALS Asm_simp_tac); |
381 by (ALLGOALS Asm_simp_tac); |
381 qed "diff_diff_left"; |
382 qed "diff_diff_left"; |
602 by (asm_full_simp_tac |
603 by (asm_full_simp_tac |
603 (!simpset addsimps [Suc_diff_n RS sym, le_eq_less_Suc]) 1); |
604 (!simpset addsimps [Suc_diff_n RS sym, le_eq_less_Suc]) 1); |
604 qed "Suc_diff_Suc"; |
605 qed "Suc_diff_Suc"; |
605 |
606 |
606 goal Arith.thy "!! i::nat. i <= n ==> n - (n - i) = i"; |
607 goal Arith.thy "!! i::nat. i <= n ==> n - (n - i) = i"; |
607 by (subgoal_tac "(n-i) + (n - (n-i)) = (n-i) + i" 1); |
608 by (etac rev_mp 1); |
608 by (Full_simp_tac 1); |
609 by (res_inst_tac [("m","n"),("n","i")] diff_induct 1); |
609 by (asm_simp_tac (!simpset addsimps [diff_le_self, add_commute]) 1); |
610 by (ALLGOALS (asm_simp_tac (!simpset addsimps [Suc_diff_le]))); |
610 qed "diff_diff_cancel"; |
611 qed "diff_diff_cancel"; |
611 Addsimps [diff_diff_cancel]; |
612 Addsimps [diff_diff_cancel]; |
612 |
613 |
613 goal Arith.thy "!!k::nat. k <= n ==> m <= n + m - k"; |
614 goal Arith.thy "!!k::nat. k <= n ==> m <= n + m - k"; |
614 by (etac rev_mp 1); |
615 by (etac rev_mp 1); |