nat_diff_split_asm, for the assumptions

--- a/src/HOL/NatArith.thy	Mon May 21 14:53:30 2001 +0200
+++ b/src/HOL/NatArith.thy	Tue May 22 09:26:57 2001 +0200
@@ -12,10 +12,16 @@
 (*elimination of `-' on nat*)
 lemma nat_diff_split:
     "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
-  by (cases "a < b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2])
+  by (cases "a<b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2])
+
+(*elimination of `-' on nat in assumptions*)
+lemma nat_diff_split_asm:
+    "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
+  by (simp split: nat_diff_split)
 
 ML {*
  val nat_diff_split = thm "nat_diff_split";
+ val nat_diff_split_asm = thm "nat_diff_split_asm";
 
 (* TODO: use this for force_tac in Provers/clasip.ML *)
 fun add_arith cs = cs addafter ("arith_tac", arith_tac);