# HG changeset patch
# User paulson
# Date 1109754141 -3600
# Node ID f5f4f89a3b84d15d833ff1c433412a9c676da2d3
# Parent  2901b1f6ba64955ce4e04b3e729dfd484a3efbe7
new lemmas int_diff_cases

diff -r 2901b1f6ba64 -r f5f4f89a3b84 src/HOL/Integ/IntDef.thy
--- 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)