--- 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);