# HG changeset patch
# User paulson
# Date 904654990 -7200
# Node ID 8a458866637c8f898591b89903802816a11f215e
# Parent  9d11f2d39b1325436aabdae5455197dc44a37291
changed Suc_diff_n to Suc_diff_le, with premise n <= m instead of n < Suc(m)

diff -r 9d11f2d39b13 -r 8a458866637c src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Tue Sep 01 10:25:05 1998 +0200
+++ b/src/HOL/Arith.ML	Tue Sep 01 15:03:10 1998 +0200
@@ -331,11 +331,11 @@
 
 (*** 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);
@@ -372,7 +372,7 @@
 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";
@@ -388,8 +388,7 @@
 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)";
@@ -440,12 +439,11 @@
 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)";
@@ -471,20 +469,13 @@
 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";
@@ -622,13 +613,8 @@
 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";
@@ -687,6 +673,18 @@
 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 **)
@@ -707,5 +705,5 @@
 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";