# HG changeset patch
# User paulson
# Date 932563577 -7200
# Node ID 71e9ea2198e08a5f581f3ff112c8d70ea6e698fd
# Parent  8dfea70eb6b7fe845f537f0e126d51135db511a3
a stronger diff_less and no more le_diff_less

diff -r 8dfea70eb6b7 -r 71e9ea2198e0 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Wed Jul 21 15:23:18 1999 +0200
+++ b/src/HOL/Arith.ML	Wed Jul 21 15:26:17 1999 +0200
@@ -462,7 +462,12 @@
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
 by (ALLGOALS Asm_simp_tac);
 qed "diff_is_0_eq";
-Addsimps [diff_is_0_eq RS iffD2];
+
+Goal "(0 = m-n) = (m <= n)";
+by (stac (diff_is_0_eq RS sym) 1);
+by (rtac eq_sym_conv 1);
+qed "zero_is_diff_eq";
+Addsimps [diff_is_0_eq, zero_is_diff_eq];
 
 Goal "(0<n-m) = (m<n)";
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
@@ -1011,9 +1016,9 @@
 (* Elimination of `-' on nat due to John Harrison *)
 Goal "P(a - b::nat) = (!d. (b = a + d --> P 0) & (a = b + d --> P d))";
 by (case_tac "a <= b" 1);
-by (Auto_tac);
+by Auto_tac;
 by (eres_inst_tac [("x","b-a")] allE 1);
-by (Auto_tac);
+by (asm_simp_tac (simpset() addsimps [diff_is_0_eq RS iffD2]) 1);
 qed "nat_diff_split";
 
 (* FIXME: K true should be replaced by a sensible test to speed things up
@@ -1095,16 +1100,12 @@
 by (arith_tac 1);
 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";
+(*Replaces the previous diff_less and le_diff_less, which had the stronger
+  second premise n<=m*)
+Goal "[| 0<n; 0<m |] ==> m - n < m";
 by (arith_tac 1);
 qed "diff_less";
 
-Goal "[| 0<n; n<=m |] ==> m - n < m";
-by (arith_tac 1);
-qed "le_diff_less";
-
-
 
 (** (Anti)Monotonicity of subtraction -- by Stefan Merz **)
 
diff -r 8dfea70eb6b7 -r 71e9ea2198e0 src/HOL/Divides.ML
--- a/src/HOL/Divides.ML	Wed Jul 21 15:23:18 1999 +0200
+++ b/src/HOL/Divides.ML	Wed Jul 21 15:26:17 1999 +0200
@@ -287,7 +287,7 @@
 					   mod_geq]) 1);
 by (etac disjE 1);
  by (asm_simp_tac (simpset() addsimps [mod_less]) 2);
-by (asm_simp_tac (simpset() addsimps [Suc_diff_le, le_diff_less, 
+by (asm_simp_tac (simpset() addsimps [Suc_diff_le, diff_less, 
 				      le_mod_geq]) 1);
 qed "mod_Suc";