equal
deleted
inserted
replaced
435 goal Arith.thy "Suc(m)-n = (if m<n then 0 else Suc(m-n))"; |
435 goal Arith.thy "Suc(m)-n = (if m<n then 0 else Suc(m-n))"; |
436 by (simp_tac (simpset() addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n] |
436 by (simp_tac (simpset() addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n] |
437 addsplits [expand_if]) 1); |
437 addsplits [expand_if]) 1); |
438 qed "if_Suc_diff_n"; |
438 qed "if_Suc_diff_n"; |
439 |
439 |
|
440 goal Arith.thy "Suc(m)-n <= Suc(m-n)"; |
|
441 by (simp_tac (simpset() addsimps [if_Suc_diff_n] addsplits [expand_if]) 1); |
|
442 qed "diff_Suc_le_Suc_diff"; |
|
443 |
440 goal Arith.thy "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)"; |
444 goal Arith.thy "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)"; |
441 by (res_inst_tac [("m","k"),("n","i")] diff_induct 1); |
445 by (res_inst_tac [("m","k"),("n","i")] diff_induct 1); |
442 by (ALLGOALS (Clarify_tac THEN' Simp_tac THEN' TRY o Blast_tac)); |
446 by (ALLGOALS (Clarify_tac THEN' Simp_tac THEN' TRY o Blast_tac)); |
443 qed "zero_induct_lemma"; |
447 qed "zero_induct_lemma"; |
444 |
448 |
609 by (rtac le_add2 1); |
613 by (rtac le_add2 1); |
610 by (Asm_full_simp_tac 1); |
614 by (Asm_full_simp_tac 1); |
611 qed "add_less_imp_less_diff"; |
615 qed "add_less_imp_less_diff"; |
612 |
616 |
613 goal Arith.thy "!! n. n <= m ==> Suc m - n = Suc (m - n)"; |
617 goal Arith.thy "!! n. n <= m ==> Suc m - n = Suc (m - n)"; |
614 by (rtac Suc_diff_n 1); |
618 by (asm_full_simp_tac (simpset() addsimps [Suc_diff_n, le_eq_less_Suc]) 1); |
615 by (asm_full_simp_tac (simpset() addsimps [le_eq_less_Suc]) 1); |
|
616 qed "Suc_diff_le"; |
619 qed "Suc_diff_le"; |
617 |
620 |
618 goal Arith.thy "!! n. Suc i <= n ==> Suc (n - Suc i) = n - i"; |
621 goal Arith.thy "!! n. Suc i <= n ==> Suc (n - Suc i) = n - i"; |
619 by (asm_full_simp_tac |
622 by (asm_full_simp_tac |
620 (simpset() addsimps [Suc_diff_n RS sym, le_eq_less_Suc]) 1); |
623 (simpset() addsimps [Suc_diff_n RS sym, le_eq_less_Suc]) 1); |