new lemmas int_diff_cases

--- a/src/HOL/Integ/IntDef.thy	Wed Mar 02 00:56:41 2005 +0100
+++ b/src/HOL/Integ/IntDef.thy	Wed Mar 02 10:02:21 2005 +0100
@@ -836,6 +836,13 @@
      "[|!! n. P (int n);  !!n. P (- (int (Suc n))) |] ==> P z"
   by (cases z) auto
 
+text{*Contributed by Brian Huffman*}
+theorem int_diff_cases [case_names diff]:
+assumes prem: "!!m n. z = int m - int n ==> P" shows "P"
+ apply (rule_tac z=z in int_cases)
+  apply (rule_tac m=n and n=0 in prem, simp)
+ apply (rule_tac m=0 and n="Suc n" in prem, simp)
+done
 
 lemma of_nat_nat: "0 \<le> z ==> of_nat (nat z) = of_int z"
 apply (cases z)