1.1 --- a/src/HOL/Arith.ML	Thu Aug 20 16:49:47 1998 +0200
     1.2 +++ b/src/HOL/Arith.ML	Thu Aug 20 16:58:28 1998 +0200
     1.3 @@ -417,12 +417,11 @@
     1.4  by (ALLGOALS Asm_simp_tac);
     1.5  qed "le_imp_diff_is_add";
     1.6  
     1.7 -Goal "m < Suc(n) ==> m-n = 0";
     1.8 -by (etac rev_mp 1);
     1.9 +Goal "(m-n = 0) = (m <= n)";
    1.10  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.11 -by (asm_simp_tac (simpset() addsimps [less_Suc_eq]) 1);
    1.12 -by (ALLGOALS Asm_simp_tac);
    1.13 -qed "less_imp_diff_is_0";
    1.14 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [le_eq_less_Suc])));
    1.15 +qed "diff_is_0_eq";
    1.16 +Addsimps [diff_is_0_eq RS iffD2];
    1.17  
    1.18  Goal "m-n = 0  -->  n-m = 0  -->  m=n";
    1.19  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.20 @@ -441,8 +440,8 @@
    1.21  qed "less_imp_add_positive";
    1.22  
    1.23  Goal "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
    1.24 -by (simp_tac (simpset() addsimps [less_imp_diff_is_0,
    1.25 -				  not_less_eq, Suc_diff_n]) 1);
    1.26 +by (simp_tac (simpset() addsimps [leI, Suc_le_eq, 
    1.27 +				  le_imp_less_Suc RS Suc_diff_n]) 1);
    1.28  qed "if_Suc_diff_n";
    1.29  
    1.30  Goal "Suc(m)-n <= Suc(m-n)";
    1.31 @@ -485,7 +484,7 @@
    1.32  by (blast_tac (claset() addIs [le_trans]) 1);
    1.33  by (auto_tac (claset() addIs [Suc_leD], simpset() delsimps [diff_Suc_Suc]));
    1.34  by (asm_full_simp_tac (simpset() delsimps [Suc_less_eq] 
    1.35 -		       addsimps [Suc_diff_n RS sym, le_eq_less_Suc]) 1);
    1.36 +		       addsimps [le_imp_less_Suc RS Suc_diff_n RS sym]) 1);
    1.37  qed "diff_right_cancel";
    1.38  
    1.39  Goal "!!n::nat. n - (n+m) = 0";
    1.40 @@ -623,7 +622,7 @@
    1.41  qed "add_less_imp_less_diff";
    1.42  
    1.43  Goal "n <= m ==> Suc m - n = Suc (m - n)";
    1.44 -by (asm_full_simp_tac (simpset() addsimps [Suc_diff_n, le_eq_less_Suc]) 1);
    1.45 +by (asm_full_simp_tac (simpset() addsimps [le_imp_less_Suc RS Suc_diff_n]) 1);
    1.46  qed "Suc_diff_le";
    1.47  
    1.48  Goal "Suc i <= n ==> Suc (n - Suc i) = n - i";
    1.49 @@ -652,6 +651,31 @@
    1.50  qed_spec_mp "add_diff_less";
    1.51  
    1.52  
    1.53 +Goal "m-1 < n ==> m <= n";
    1.54 +by (exhaust_tac "m" 1);
    1.55 +by (auto_tac (claset(), simpset() addsimps [Suc_le_eq]));
    1.56 +qed "pred_less_imp_le";
    1.57 +
    1.58 +Goal "j<=i ==> i - j < Suc i - j";
    1.59 +by (REPEAT (etac rev_mp 1));
    1.60 +by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
    1.61 +by Auto_tac;
    1.62 +qed "diff_less_Suc_diff";
    1.63 +
    1.64 +Goal "i - j <= Suc i - j";
    1.65 +by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
    1.66 +by Auto_tac;
    1.67 +qed "diff_le_Suc_diff";
    1.68 +AddIffs [diff_le_Suc_diff];
    1.69 +
    1.70 +Goal "n - Suc i <= n - i";
    1.71 +by (case_tac "i<n" 1);
    1.72 +bd diff_Suc_less_diff 1;
    1.73 +by (auto_tac (claset(), simpset() addsimps [leI RS le_imp_less_Suc]));
    1.74 +qed "diff_Suc_le_diff";
    1.75 +AddIffs [diff_Suc_le_diff];
    1.76 +
    1.77 +
    1.78  
    1.79  (** (Anti)Monotonicity of subtraction -- by Stefan Merz **)
    1.80