src/HOL/Arith.ML
changeset 4672 9d55bc687e1e
parent 4423 a129b817b58a
child 4686 74a12e86b20b
     1.1 --- a/src/HOL/Arith.ML	Tue Mar 03 15:09:04 1998 +0100
     1.2 +++ b/src/HOL/Arith.ML	Tue Mar 03 15:11:26 1998 +0100
     1.3 @@ -437,6 +437,10 @@
     1.4                         addsplits [expand_if]) 1);
     1.5  qed "if_Suc_diff_n";
     1.6  
     1.7 +goal Arith.thy "Suc(m)-n <= Suc(m-n)";
     1.8 +by (simp_tac (simpset() addsimps [if_Suc_diff_n] addsplits [expand_if]) 1);
     1.9 +qed "diff_Suc_le_Suc_diff";
    1.10 +
    1.11  goal Arith.thy "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)";
    1.12  by (res_inst_tac [("m","k"),("n","i")] diff_induct 1);
    1.13  by (ALLGOALS (Clarify_tac THEN' Simp_tac THEN' TRY o Blast_tac));
    1.14 @@ -611,8 +615,7 @@
    1.15  qed "add_less_imp_less_diff";
    1.16  
    1.17  goal Arith.thy "!! n. n <= m ==> Suc m - n = Suc (m - n)";
    1.18 -by (rtac Suc_diff_n 1);
    1.19 -by (asm_full_simp_tac (simpset() addsimps [le_eq_less_Suc]) 1);
    1.20 +by (asm_full_simp_tac (simpset() addsimps [Suc_diff_n, le_eq_less_Suc]) 1);
    1.21  qed "Suc_diff_le";
    1.22  
    1.23  goal Arith.thy "!! n. Suc i <= n ==> Suc (n - Suc i) = n - i";