# HG changeset patch
# User paulson
# Date 990516417 -7200
# Node ID 82406bd816a53d5867bbcafc23e6638f8d1c7dbc
# Parent  92eddd0914a9d4d141823c06f2046e1c1dc83092
nat_diff_split_asm, for the assumptions

diff -r 92eddd0914a9 -r 82406bd816a5 src/HOL/NatArith.thy
--- 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);