# HG changeset patch
# User paulson
# Date 955631882 -7200
# Node ID 2f2d2b4215d60e07648716199bf386d4b0c96dd8
# Parent  5de7634465040bd525005589350e9d63aa503702
added some new iff-lemmas; removed some obsolete thms

diff -r 5de763446504 -r 2f2d2b4215d6 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Thu Apr 13 15:16:32 2000 +0200
+++ b/src/HOL/Arith.ML	Thu Apr 13 15:18:02 2000 +0200
@@ -426,7 +426,7 @@
 by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "diff_add_assoc";
 
-Goal "k <= (j::nat) --> (j + i) - k = i + (j - k)";
+Goal "k <= (j::nat) --> (j + i) - k = (j - k) + i";
 by (asm_simp_tac (simpset() addsimps [add_commute, diff_add_assoc]) 1);
 qed_spec_mp "diff_add_assoc2";
 
@@ -1050,10 +1050,6 @@
 by (arith_tac 1);
 qed "diff_less_mono";
 
-Goal "a+b < (c::nat) ==> a < c-b";
-by (arith_tac 1);
-qed "add_less_imp_less_diff";
-
 Goal "(i < j-k) = (i+k < (j::nat))";
 by (arith_tac 1);
 qed "less_diff_conv";
@@ -1079,10 +1075,6 @@
 by (arith_tac 1);
 qed "le_add_diff";
 
-Goal "[| 0<k; j<i |] ==> j+k-i < k";
-by (arith_tac 1);
-qed "add_diff_less";
-
 Goal "m-1 < n ==> m <= n";
 by (arith_tac 1);
 qed "pred_less_imp_le";
@@ -1115,8 +1107,7 @@
 by (arith_tac 1);
 qed "diff_less";
 
-
-(*** Reducting subtraction to addition ***)
+(*** Reducing subtraction to addition ***)
 
 Goal "n<=(l::nat) --> Suc l - n + m = Suc (l - n + m)";
 by (simp_tac (simpset() addsplits [nat_diff_split]) 1);
@@ -1138,6 +1129,20 @@
 by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
 qed "diff_right_cancel";
 
+(** Simplification of relational expressions involving subtraction **)
+
+Goal "[| k <= m;  k <= (n::nat) |] ==> (m-k = n-k) = (m=n)";
+by (auto_tac (claset(), simpset() addsplits [nat_diff_split']));
+qed "eq_diff_iff";
+
+Goal "[| k <= m;  k <= (n::nat) |] ==> (m-k < n-k) = (m<n)";
+by (auto_tac (claset(), simpset() addsplits [nat_diff_split']));
+qed "less_diff_iff";
+
+Goal "[| k <= m;  k <= (n::nat) |] ==> (m-k <= n-k) = (m<=n)";
+by (auto_tac (claset(), simpset() addsplits [nat_diff_split']));
+qed "le_diff_iff";
+
 
 (** (Anti)Monotonicity of subtraction -- by Stephan Merz **)