src/HOL/Arith.ML

 Addsimps  [le_add_diff_inverse, le_add_diff_inverse2];
 
 
 (*** More results about difference ***)
 
-Goal "n < Suc(m) ==> Suc(m)-n = Suc(m-n)";
+Goal "n <= m ==> Suc(m)-n = Suc(m-n)";
 by (etac rev_mp 1);
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
 by (ALLGOALS Asm_simp_tac);
-qed "Suc_diff_n";
+qed "Suc_diff_le";
 
 Goal "m - n < Suc(m)";
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
 by (etac less_SucE 3);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq])));

 Addsimps [diff_Suc_less];
 
 Goal "i<n ==> n - Suc i < n - i";
 by (exhaust_tac "n" 1);
 by Safe_tac;
-by (asm_simp_tac (simpset() addsimps [Suc_diff_n]) 1);
+by (asm_simp_tac (simpset() addsimps [le_eq_less_Suc, Suc_diff_le]) 1);
 qed "diff_Suc_less_diff";
 
 Goal "m - n <= Suc m - n";
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
 by (ALLGOALS Asm_simp_tac);

 qed "diff_commute";
 
 Goal "!!i j k:: nat. k<=j --> j<=i --> i - (j - k) = i - j + k";
 by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
 by (ALLGOALS Asm_simp_tac);
-by (asm_simp_tac
-    (simpset() addsimps [Suc_diff_n, le_imp_less_Suc, le_Suc_eq]) 1);
+by (asm_simp_tac (simpset() addsimps [Suc_diff_le, le_Suc_eq]) 1);
 qed_spec_mp "diff_diff_right";
 
 Goal "!!i j k:: nat. k<=j --> (i + j) - k = i + (j - k)";
 by (res_inst_tac [("m","j"),("n","k")] diff_induct 1);
 by (ALLGOALS Asm_simp_tac);

 by (res_inst_tac [("x","j - i")] exI 1);
 by (asm_simp_tac (simpset() addsimps [add_diff_inverse, less_not_sym]) 1);
 qed "less_imp_add_positive";
 
 Goal "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
-by (simp_tac (simpset() addsimps [leI, Suc_le_eq, 
-				  le_imp_less_Suc RS Suc_diff_n]) 1);
-qed "if_Suc_diff_n";
+by (simp_tac (simpset() addsimps [leI, Suc_le_eq, Suc_diff_le]) 1);
+qed "if_Suc_diff_le";
 
 Goal "Suc(m)-n <= Suc(m-n)";
-by (simp_tac (simpset() addsimps [if_Suc_diff_n]) 1);
+by (simp_tac (simpset() addsimps [if_Suc_diff_le]) 1);
 qed "diff_Suc_le_Suc_diff";
 
 Goal "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)";
 by (res_inst_tac [("m","k"),("n","i")] diff_induct 1);
 by (ALLGOALS (Clarify_tac THEN' Simp_tac THEN' TRY o Blast_tac));

 val add_commute_k = read_instantiate [("n","k")] add_commute;
 by (asm_simp_tac (simpset() addsimps ([add_commute_k])) 1);
 qed "diff_cancel2";
 Addsimps [diff_cancel2];
 
-(*From Clemens Ballarin*)
+(*From Clemens Ballarin, proof by lcp*)
 Goal "!!n::nat. [| k<=n; n<=m |] ==> (m-k) - (n-k) = m-n";
-by (subgoal_tac "k<=n --> n<=m --> (m-k) - (n-k) = m-n" 1);
-by (Asm_full_simp_tac 1);
-by (induct_tac "k" 1);
-by (Simp_tac 1);
-(* Induction step *)
-by (subgoal_tac "Suc na <= m --> n <= m --> Suc na <= n --> \
-\                Suc (m - Suc na) - Suc (n - Suc na) = m-n" 1);
-by (Asm_full_simp_tac 1);
-by (blast_tac (claset() addIs [le_trans]) 1);
-by (auto_tac (claset() addIs [Suc_leD], simpset() delsimps [diff_Suc_Suc]));
-by (asm_full_simp_tac (simpset() delsimps [Suc_less_eq] 
-		       addsimps [le_imp_less_Suc RS Suc_diff_n RS sym]) 1);
+by (REPEAT (etac rev_mp 1));
+by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
+by (ALLGOALS Asm_simp_tac);
+(*a confluence problem*)
+by (asm_simp_tac (simpset() addsimps [Suc_diff_le, le_Suc_eq]) 1);
 qed "diff_right_cancel";
 
 Goal "!!n::nat. n - (n+m) = 0";
 by (induct_tac "n" 1);
 by (ALLGOALS Asm_simp_tac);

 by (dtac diff_less_mono 1);
 by (rtac le_add2 1);
 by (Asm_full_simp_tac 1);
 qed "add_less_imp_less_diff";
 
-Goal "n <= m ==> Suc m - n = Suc (m - n)";
-by (asm_full_simp_tac (simpset() addsimps [le_imp_less_Suc RS Suc_diff_n]) 1);
-qed "Suc_diff_le";
-
 Goal "Suc i <= n ==> Suc (n - Suc i) = n - i";
-by (asm_full_simp_tac
-    (simpset() addsimps [Suc_diff_n RS sym, le_eq_less_Suc]) 1);
+by (asm_simp_tac (simpset() addsimps [Suc_diff_le RS sym]) 1);
 qed "Suc_diff_Suc";
 
 Goal "!! i::nat. i <= n ==> n - (n - i) = i";
 by (etac rev_mp 1);
 by (res_inst_tac [("m","n"),("n","i")] diff_induct 1);

 Goal "0 < n ==> (m-1 < n) = (m<=n)";
 by (exhaust_tac "m" 1);
 by (auto_tac (claset(), simpset() addsimps [Suc_le_eq]));
 qed "less_pred_eq";
 
+(*In ordinary notation: if 0<n and n<=m then m-n < m *)
+Goal "[| 0<n; ~ m<n |] ==> m - n < m";
+by (subgoal_tac "0<n --> ~ m<n --> m - n < m" 1);
+by (Blast_tac 1);
+by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
+by (ALLGOALS(asm_simp_tac(simpset() addsimps [diff_less_Suc])));
+qed "diff_less";
+
+Goal "[| 0<n; n<=m |] ==> m - n < m";
+by (asm_simp_tac (simpset() addsimps [diff_less, not_less_iff_le]) 1);
+qed "le_diff_less";
+
 
 
 (** (Anti)Monotonicity of subtraction -- by Stefan Merz **)
 
 (* Monotonicity of subtraction in first argument *)

 by (case_tac "n <= na" 1);
 by (subgoal_tac "m <= na" 1);
 by (asm_simp_tac (simpset() addsimps [Suc_diff_le]) 1);
 by (fast_tac (claset() addEs [le_trans]) 1);
 by (dtac not_leE 1);
-by (asm_simp_tac (simpset() addsimps [if_Suc_diff_n]) 1);
+by (asm_simp_tac (simpset() addsimps [if_Suc_diff_le]) 1);
 qed_spec_mp "diff_le_mono2";